Expand description
The three registry books: Artifact, Asset,
Resident census. The load-bearing line is the Claim/Artifact split —
an unverified result is testimony, and Artifact::verify is the only
door between the two (player–referee in the type). The registry is a
value, not a store: state lives with the caller and is rebuilt from
the Ledger.
The part crates/kernel/spec/Registry.lean specifies this module.
Structs§
- Artifact
- A verified product. Private fields: the only constructor demands
verification evidence of a kind in
completion::CITABLE. - Claim
- Testimony: a result nobody has verified yet. Claims never enter the registry; they only carry what to verify.
- Registry
- The three books. Keys are canonical locator spellings (Display is the canonical form by the locator round-trip law).
- Resident
Id - Non-empty resident identity; the
role@building.ngrammar tightens with city::resident.
Enums§
- Register
Verdict - Deliberately exhaustive registration verdict.