What the words mean: the bond, the tip, the two min-ADAs, the phases, and the rooms a leaf moves through
What can happen next Follow the story or try a proposed move. The cast groups interests; evidence and transaction inputs determine acceptance. A move from a visited step opens a branch.
what the machine refuses now
The scene KERI, the registry and its checkpoints, the inbox, the readers and payees · every step plays on it; click an actor to act as them
The theorems · sampled contract checks and complete-result Lean replay · open a lamp for its exact scope
Evidence by hand the Env: what the plugin and the policy would verify over the bytes, decided by you
The registry in numbers the UTxO, the leaves, the checkpoints, the inbox and its phases
Value over the play bonds locked in checkpoints request value + retained min-ADA application payments (bond returns, booking premiums) · the current branch
Who holds what by component; every payment named by the flow
What this is and is not
This is an executable transcription of Registry.stepFn and the pinned public Singular transaction judgments. The registry holds absent, active or permanently retired keys. There is no owner exit: a carrier stays live until it is convicted. Conviction preserves custody pending booking; only a consuming fold retires the key and burns its token. Requests and transactions carry full value, routing and custody observations.
Evidence is a finite table of model predicates. This page does not construct KERI signatures, prove arbitrary uploaded histories reachable, submit transactions, or establish production conformance. Concrete checkpoint key states and duplicity have a separate model; no key encoding equivalence is asserted here. Transaction assembly uses model fixtures, with every proposal judged by the same core.
Wire version 3 represents safe integers as JSON numbers and larger integers as canonical decimal strings, with exact arithmetic throughout. The chart uses scaled coordinates; the numbers and exported data remain exact. A theorem lamp checks a stated finite observation. The Lean parity lamp lights only for a complete input in the embedded corpus. Exported interactive expectations are simulator results, not new Lean oracle output. Run the self-test.