Map the Singular registry to Cardano KERI

As a KERI integrator, I need to see which layer admits an identity, keeps its live carrier until conviction and completes permanent retirement. As a relying party, I must not mistake an active registry key for a consumable checkpoint.

This page maps the current Lean model and its simulators. It does not establish production validator, builder or deployment conformance. The preprod V1 baseline is a separate implementation. Start with the runnable identity examples or the Registry design for the full premises.

Bound sources and acceptance boundary

The public Singular dependency is commit d69ab005c3b710aeebf033d3c5cd08c56feb5643, tree 2979dcfc58b092313b0ce7fa0493722539b9ea65. Registry.lean imports its economic booking and fold judgments; RegistryAgreement.lean binds the projection. Checkpoint.lean governs the funded lifecycle and associated system; CheckpointCertificate.lean executes the receipt interface.

There is no owner exit (#493): no parking and no revival; a carrier is live until it is convicted. The correspondence register keeps other open model obligations. The earlier mapping is retained in the historical source.

Registration and termination boundary

flowchart LR
  Admission[KERI admission] --> Booking[Complete booking]
  Booking --> Fold[Imported accepted fold]
  Fold --> Carrier[Active carrier]
  Carrier --> Conviction[Duplicity and pending custody]
  Conviction --> Request[Exact termination request]
  Request --> Completion[Consuming fold: burn and retire]

The Registry adapter uses actual imported transactions, including their inputs, outputs, assets and validity intervals. KERI still owns its application admission and custody metadata. Registration creates the active carrier and permanent binding only after an accepted fold. Termination completes only when an accepted fold consumes the associated pending request.

Owner story	Model responsibility	Remaining implementation boundary
Register once	Actual booking/fold plus KERI inception; unique permanent binding	Concrete inception/receipt verification and transaction mapping
Convict	Concrete Checkpoint duplicity; pending state; exact booking association	Evidence codec and actual on-chain custody
Complete retirement	Stored-context replay and exact consumed request; burn only at fold	Transaction construction and chain confirmation
Read eligibility	Present, mature, unpoisoned, unfrozen checkpoint	Exact token/canonical registry and consuming transaction checks
Recover a registration request	Imported generic recovery transaction	Broader KERI recovery obligations

Value and authorization

The refund address is chosen by whoever pays the registration and no step changes it. There is no close. Conviction pays the conviction bond to the convictor and returns the held freeze bond and pool to the refund address.

Termination booking splits Mc into Mr + tip for the request and Mc - Mr - tip for the booker. The booker pays its booking fee separately. The actual fold accounting does not guarantee that Mr returns to that booker. Self-fold accounting names the recipient and requires all its stated output, fee and matching-booking premises.

Registry's coarse evidence predicates and Checkpoint's concrete evidence are not interchangeable. The associated system combines local Checkpoint evidence with a replayed accepted Registry origin and receipt. A same-context receipt for another request cannot complete the selected identity.

Registry identity and lookup

An active key remains active while its carrier is live or termination is pending. The reader must classify the holding before treating it as eligible. The model's integer token counter is not a Cardano asset-name specification. Exact identity, canonical registry selection and validity extensions remain in consumer authentication. A provider failure must not become evidence of absence.

Public upstream requirements for registration, termination and reading remain separate from this pinned model execution and from KERI deployment evidence.

What can be checked now

Play the Registry simulator for complete transactions and the Checkpoint simulator for local stories and associated receipt journeys. Fresh Lean corpora are compared with the independent JavaScript cores, CLI results and embedded pages. Full states and addressed flows are compared, not only accepted/refused counts.

Kernel proofs, finite executions, model mutations and fabricated checker controls remain distinct evidence. This mapping does not close broader request lifecycle, consumer authentication or production correspondence. Every production invariant still needs its bound story and both implementation test layers.