Objects and identity

The canonical object kinds a store holds, their exact fields, how each ID is computed, and how receipts record acceptance.

A store holds canonical typed objects. Each object is a JSON value with an exact set of fields, and its ID is the SHA-256 of its canonical encoding. docs/identity.md is the authoritative specification, implemented in crates/lema-core/src/model.rs and crates/lema-core/src/closure.rs. The Lean exporter in lean/codebase/ produces objects, and the decoder there replays them through the pinned Lean 4.34.1 kernel.

Object IDs

id = sha256("LEMA-TYPED-CORE-v3\0" ‖ canonical(value))

The ID is written as 64 lowercase hex digits. It is defined on the parsed value, so whitespace, key order and string escapes in the input do not change it.

• Validation refuses; it never normalizes. The builder emits canonical form and validation refuses every other encoding, so no value is rewritten and two meanings can never share an ID.
• Identity is of the kernel term, not of its meaning up to definitional equality. Two definitionally equal but different terms are different objects.
• Binder names and mdata are erased, universe parameters are positional, and a definition’s reducibility hint is its kind (regular, abbrev or opaque) without the height.
• These differences stay identity on purpose: definitionally equal but different terms, different nominal seeds, constructor order, and different proof terms for one statement.
• There is one running encoding. A change of these rules re-addresses every object, and accepted objects are rebuilt from their sources; no migration tool is kept.

crates/lema-core/tests/identity.rs pins identities, with the cases listed in docs/identity.md §9:

Canonical JSON

Parsing is strict. It refuses duplicate keys; numbers that are not integers or not finite, and integers with a leading zero or a negative zero (01, -0); strings that are not Unicode scalar sequences; input that is not UTF-8; and trailing content.

The canonical encoding of a value:

For every value within the bounds below, this equals Python’s json.dumps(sort_keys=True, separators=(',',':'), ensure_ascii=False, allow_nan=False). Lean’s own Json.compress is not canonical (it writes tab, backspace and form feed as \u escapes), so exports are parsed and re-encoded before hashing.

Bounds

Validation refuses an object beyond these bounds, so every implementation accepts the same objects.

Raising a bound admits new objects and re-addresses none.

Object kinds

Every object has schema, kind and namespace (the namespace object’s ID), except the namespace object, which has no namespace. No object has an assumptions field: axiom footprints are derived at replay and recorded in receipts.

namespace

The namespace object is fixed by the code (model::namespace). Every other object’s namespace field holds its ID.

{"base":"Init","encoding":"lema-core-v3","kind":"namespace","lean_githash":"5045d0056413266e57c625dcd7c365b10e377c52","lean_version":"4.34.1","schema":"lema.core/v3"}

Two builds of the same Lean source revision on different hosts share a namespace. Before replay, the decoder checks that the running Lean’s version and githash are the namespace’s. A closure holds objects of one namespace only, and a store, module cache or artifact from another encoding is refused. The checker binary and the distribution are not part of the namespace; receipts record them. The axiom ceiling is not part of it either; it is store policy.

external

statement

template

A slot is {"tag":"slot","index":i}, with no type, so a template does not change when a proof inside it does. Slots are numbered 0 to n−1 in the order a pre-order walk meets them (children in ascending key order), each used once. The exporter marks every maximal subterm whose type is a proposition, in value positions only; slots never appear in binder domains, let types, statements or proofs, and replay checks that the marking is exactly the maximal proof subterms.

proof

satisfaction

declaration

Replay installs a declaration as LemaStored.h<id>, and a generated helper under its family (LemaStored.h<family id>.casesOn).

record

Field labels are not stored; m is the constructor’s num_fields.

family

Each entry of a record or family has role, kind (inductive, constructor, recursor, definition or theorem), levels and type, plus the kernel fields of its kind (num_params and ctors; induct, cidx, num_params and num_fields; num_params, num_indices, num_motives, num_minors, k and rules). Records and families have no top-level num_params: the inductive entry carries it. A recursor’s num_indices is always 0.

Expression values

Every expression position (a statement’s type, a template’s term, a proof’s context entries, type and term, and a record or family entry’s type, value and recursor rules’ rhs) holds its own expression value. Nothing is shared between positions.

An expression value is a non-empty JSON array of nodes. The last node is the root, and a node’s children are indices of earlier nodes. Validation refuses it unless no two nodes are equal and the nodes are the tree’s distinct subterms in post-order of first occurrence, children visited in ascending key order (app: argument then function). One tree has exactly one encoding.

f x x is:

[{"levels":[],"ref":{"id":"<x>"},"tag":"const"},
 {"levels":[],"ref":{"id":"<f>"},"tag":"const"},
 {"argument":0,"function":1,"tag":"app"},
 {"argument":0,"function":2,"tag":"app"}]

Validation, replay and digests are linear in the nodes and never expand a tree, which can be exponentially larger than its value.

References and citations

A constant reference is {"id": …}, {"id": …, "role": …}, or {"self": role} inside a family’s own entries. Which ID a reference holds depends on where it appears.

Citing a declaration ID from a statement, template or proof is refused. Statements, templates and proofs are semantic objects; satisfactions and declarations are bindings; records and families are nominal and concrete, because their kernel names derive from their own IDs.

Realizations

A satisfaction’s realizations resolve its citations to concrete declarations:

"realizations": [{"of": "<template or statement ID>", "declaration": "<declaration ID>"}]

The cited set is the template and statement IDs referenced in the satisfaction’s statement type, its template term, and each proof’s context, type and term (header links such as a template’s own statement field do not count). The realizations must:

1. be sorted by of, unique, and cover exactly the cited set;
2. map a template key to a definition declaration whose template is that key;
3. map a statement key to a theorem declaration whose statement is that key;
4. never give one key two declarations (two theorems of one statement, or two definitions of one template).

Replay expands citations through the realizations, so replay is always of a concrete binding.

What stays stable

Contracts, implementations and laws

These are roles, not kinds. A contract is a statement or a definition: a Core v2 Contract value or a Prop-valued predicate is a declaration of flavor definition. An implementation is a definition. A law is the contract view’s keyword for a theorem’s statement. Which role an object plays is decided by the statements that use it, not by a field.

Example

crates/lema-store/fixtures/evolve/draft.json is an elaborate result of crates/lema-store/fixtures/evolve/Evolve.lean, kept as an untrusted draft for offline tests and never submitted. This is the closure of def AlwaysTrue : Prop := True in it, five objects, copied verbatim. Each ID is the SHA-256 of the domain and the line shown.

{"binding":"1f01b92beba5bb782c2c84da7b07568d9e30c64d10111746b7d90c3e3a7cbbb3","flavor":"definition","hints":"regular","kind":"declaration","namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","proofs":[],"schema":"lema.core/v3","statement":"7960956845e971aa489678be5daf6a4481f3676135dccd88b1f8459da05ae11a","template":"c2cc2d38d695d5018e92c7001b5474647bd16be69998969d4bac1fce0dcf4cb5"}

{"kind":"statement","levels":0,"namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","schema":"lema.core/v3","type":[{"level":{"tag":"zero"},"tag":"sort"}]}

{"flavor":"definition","hints":"regular","kind":"template","levels":0,"namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","schema":"lema.core/v3","statement":"7960956845e971aa489678be5daf6a4481f3676135dccd88b1f8459da05ae11a","term":[{"levels":[],"ref":{"id":"e213b1eec05f5ac08d19e3b9eb4f60376d386dcd83f1e7ebf146a4fa2032bcd3"},"tag":"const"}]}

{"kind":"external","module":"Init.Prelude","name":"True","namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","schema":"lema.core/v3"}

{"kind":"satisfaction","namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","proofs":[],"realizations":[],"schema":"lema.core/v3","statement":"7960956845e971aa489678be5daf6a4481f3676135dccd88b1f8459da05ae11a","template":"c2cc2d38d695d5018e92c7001b5474647bd16be69998969d4bac1fce0dcf4cb5","value_sha256":"d83b1f09b0dfe5b985388dd5256e5c724c72bf2bbb7be1362920c610aa968f5e"}

The same file has theorem both_refines : BothTrue → AlwaysTrue := fun h => h.1. Its statement cites AlwaysTrue by template c2cc2d38…4cb5 and BothTrue by template 8b02b633…cb24; its template term is the single slot [{"index":0,"tag":"slot"}]; and its satisfaction resolves both citations:

{"kind":"satisfaction","namespace":"4305157d7b8a5e7c6cf71c00d66e3b127164368b5ae8e167f6428057a795cc8a","proofs":["a7bbe0d7e05cd77a0ba8f0ed2745d0862ec2d60473d5f63713ffb97977aa3d23"],"realizations":[{"declaration":"d5ee2de30a8ea7e4d2de617437d3d4e3ad814f3f5967ece2ccc077dd2aeb46e8","of":"8b02b633d187cc72b018686b561c0e6f2bb241dea7a00cc409ca6c2d7ac8cb24"},{"declaration":"5daa2818c98e0ad9887a37440528cacd2be34e46a592cb461ae5011bc5842ba3","of":"c2cc2d38d695d5018e92c7001b5474647bd16be69998969d4bac1fce0dcf4cb5"}],"schema":"lema.core/v3","statement":"315b30dff99e92122280544ff7d6c6baac92d281ed24ea7af754764a34aea42f","template":"632eb1f426752438263d8bdb19170344144a76e920e86c85b31f8772c11ff9eb","value_sha256":"0a6c6e05577fa324eab79960678cba16d7687e8edd56708989bedf536c77694c"}

Receipts and acceptance

A receipt is a store-local record, not part of identity. It is written when kernel replay accepts an object, and it is never copied from another store’s files: objects transferred between stores are replayed again, or accepted from the receipts of a cached module that this checker’s replay produced.

Declarations, records, families and externals get receipts. Statements, templates, proofs and satisfactions do not, because their footprint depends on the binding; each is accepted only through a declaration of the submission’s closure that uses it directly, as its statement, template, binding or one of its proofs. The store records an acceptance note for it instead: {object, namespace, accepted_with, checked_through, checked_at}, where checked_through names that declaration. The namespace object is accepted the same way, through any declaration, record or family of the closure.

An object that nothing in the submission checks is refused before any native call, and so is an external without a kernel receipt. A submission is accepted whole or not at all. “Accepted” means stored with a kernel receipt, or with an acceptance note checked_through a declaration that has one.

Receipts read from a module are re-checked against the store’s own policy and the fixed floor. Lean does not re-check imported declarations and reads their axioms from the module’s recorded table. Between full replays, acceptance therefore also rests on the integrity of modules the pinned checker wrote. lema reverify replays everything accepted from scratch, without modules, and compares every footprint with its receipt. The axiom policy reference describes the footprint checks, and store records the records that sit above the identity format.