The treasury checks Alice's exact holding
The treasury fixes its network, release, registry seed and Alice's AID before seeing a candidate. Follow registration through rotations, pending custody and the consuming termination fold. Change one candidate field to see why it is refused.
These are finite model observations. References after registration are fixture observations; a current ledger observer is still required. This is not a Cardano byte decoder or production conformance evidence. Not for mainnet.
The treasury's fixed context and exact asset
Inspect the candidate or try a changed holding
The trusted context and interpretation remain fixed. Edit only the holding below. Unsupported input is reported separately from refusal.
Sampled consumer property ledger
Each row checks a finite witness from this complete journey and its candidate controls. Universal statements are proved in Lean; production conformance remains open.
Connected state and transaction evidence
Connected system journeys Registration receipt → retained output → pending request → consuming fold
Play the actual system events with their fixed registration origin and complete transaction observations. The local stories below show the Checkpoint Step facet. These finite examples do not establish production conformance.
System properties exhibited by this event
Full state, stored origin, pending entry and both flows
Inspect or try the next command
Edited commands start from the displayed state. Start or a replay control returns to the recorded journey. Unsupported input is reported separately from a model refusal.
What the words mean: the three pots, W, and the states a checkpoint moves through
What can happen next the story's continuations, and every move the machine would accept from here · everyone here is anyone with an interest; every move is a public transaction, and the tag says what it must carry: only public KERI data, or a signature by the key holders · a move from a visited step opens a branch
what the machine refuses now
The scene KERI, the Cardano UTxO, the readers and payees · every step plays on it; click an actor to act as them
The theorems · T1–T16 of CheckpointGoals.lean: one checker row per theorem, folded into fourteen lamps (T11 and T13 were never stated) · a lamp lights when this step shows one of its theorems; every row is checked on every step · click to read
Evidence by hand the Env: what the validator would verify over the bytes, decided by you
The checkpoint in numbers the datum, the three sums, the treasury's verdict and its conjuncts
Value over the play conviction bond D freeze bond B pool · arrows are flows · the current branch
Who holds what lovelace, by component; every payment named by the flow
What this is and is not
A transcription of lean/CardanoKeri/Checkpoint.lean: the states, the actions (exactly the redeemers), the evidence as a table of decisions, value as three components that never mix, the consumer's state-side check. The theorems of CheckpointGoals.lean run as properties on every step. Each story is a tree: the trunk and the branches the story implies; ‹ and › walk it as an editor walks its history; click any node of the tree to jump there.
Not here: cryptography (keys are an epoch counter; evidence is a row you decide), validity (D-027, reserved), the consumer's own threshold check, UTxO mechanics, delegation, record trees, hunter bounties. A Lean Nat is unbounded; this page represents it exactly up to 2^53 − 1 and refuses anything else by name.