Play the simulation

Open the playable Singular simulator. It is one self-contained page: no framework, no network, no server. Everything it computes it computes in front of you.

The page is a transcription of the frozen Lean model into JavaScript, so that a reader can play what the proofs are about. Where the two disagree the Lean is right and the page is a defect — which is exactly what the corpus replay on the page is for.

The active engine now mirrors permanent permanent contract. Earlier absence, deletion and terminal-attestation journeys are retired; their encodings are refusal controls.

What you can do

Follow a journey. Seven stories: register a name, retire it permanently, and refuse each of the five excluded encodings. The retirement story also attempts to reuse the terminal key and observes key-exists. Registration mints an active token; retirement consumes it and leaves the key terminal.

Step with ⏮ ◀ ▶ ⏭. Stepping back unwinds the tokens as well as the leaf, so you can watch a witness appear and disappear. Where a story reaches a point that admits more than one continuation, the branches are offered and taking one does not destroy the other.

Try it yourself. Free play gives you the seven historical encodings: two supported edges and five refusals, a key, an owner, an output and a deposit, and a choice of approval: matching, right policy but wrong tuple, another policy, or none at all. The third and fourth are obviously refused. The second is the interesting one — an approval minted under the registry's own pinned policy, for a real request, that does not match this request's edge, key, owner and destination. It is refused, and a model that checked only the policy would admit it.

Read what is refused, by name. Seven encoded operations against four possible leaves give twenty-eight combinations. Two are admissible transitions; twenty-six are refused. Unsupported tags return edge-inadmissible before approval or trie effects. Supported tags still check the matching approval, leaf and active-token presence. Synthetic absent leaves are unreachable from permanent contract genesis and are shown as invalid-context controls.

See the naming instance. Switch to Naming — permanent retirement. The same engine registers and retires a name, then refuses terminal witnessing.

What the page proves, and what it does not

flowchart TD
    L["Lean model<br/>36 proved statements"] -->|Export| C["corpus.json<br/>29 replayable cases"]
    C --> B["Browser loads corpus<br/>and handwritten core.mjs"]
    B --> R["Replay and compare<br/>Actual answers with Lean"]
    R --> Verdict["Agreement: these inputs match<br/>Mismatch: a page defect"]

Every case in the corpus carries its input — the state before and the request — not just the answer, so the page recomputes each one from scratch and compares. The header line on the page reports the count it actually reproduced against the count it was given; a page that silently skipped cases would show a smaller denominator, and one that skipped all of them would show zero rather than passing.

That establishes agreement on the exported inputs. It is not a proof of equivalence: a transcription can agree on every corpus row and still diverge on the next one. The proofs are in the Lean; the page is evidence that what you are playing is the thing that was proved about, over the cases the model itself chose to export.

One caveat a reader should have, stated plainly. The Lean model, the corpus generator and this transcription were written by the same author. Agreement between them is therefore weaker evidence than agreement between independent implementations would be: a misunderstanding held while writing the model is very likely to be held again while transcribing it. The corpus replay catches transcription slips, which is what it is for. It cannot catch a shared misreading of the specification. The independent check on that is the audit of the Lean statements against the interface, not this page.

Reproduce the checks

From a source checkout, inside the development shell:

just model        # compile the Lean, regenerate the corpus, check the axioms
just simulator    # rebuild the page, replay every row, then prove the gate can fail
just browser      # drive the built page in a pinned Chromium

just simulator runs three commands. node simulator/build.mjs --check rebuilds the standalone page from its sources and fails if the committed index.html differs, so the page you play is the page in the repository. node simulator/gate.mjs replays the corpus outside the browser and reports what it covered:

The command reports computed row counts and labels each corpus section as executed behavior or inspected evidence. Registry cases and codecs are executed; request-exit payment rows, composed transaction rows, naming and lifecycle observations are inspected Lean evidence. This page has no request-exit engine. Five laws have applicable finite transition examples. Terminal immutability and terminal-attestation soundness retain Lean proofs but have no admitted-transition example with their terminal hypotheses; the page reports them as proved only.

node simulator/gate.mjs --selftest then seeds a defect and requires the gate to reject it. A checker that has never been seen to fail is not evidence, so the failing run is part of the passing one.

just browser loads the built page in Chromium, serves nothing but index.html — every other request returns 404, which is how the page's self-containment is checked rather than asserted — plays the journeys, drives free play including the wrong-tuple approval, reads the refusal table and verifies the naming journey. A page error or an outbound network request fails the run.

Where the model itself is

The executable model · the statements · the generated corpus · what each statement says · how the model was read back.

The page models states, leaves, tokens and approvals. It does not execute validators, check signatures, build transactions or hold funds. Payment rows are inspected model output; they are not transfers of funds. Nothing here establishes that the compiled validator agrees with the model.