Code stored by identity

Why every object is identified by a hash of its canonical form, and what that does and does not keep stable when code changes.

A Lema store does not hold source files. It holds objects: statements, templates, proofs, declarations and a few other kinds. Each object’s ID is the SHA-256 of its canonical form. Names, the contract syntax and the Lean source an author wrote are all views of those objects. The rules themselves are in docs/identity.md.

One canonical value, one ID

An ID is sha256("LEMA-TYPED-CORE-v3\0" ‖ canonical(value)), written as lowercase hex. The canonical form is JSON with sorted ASCII keys, no whitespace, shortest decimal integers and a fixed set of string escapes. Every object carries "schema":"lema.core/v3" and the ID of a namespace object, which fixes the Lean that gives Init its meaning:

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

Two rules make each ID mean one thing.

The first rule is that validation refuses and never normalizes. Any encoding freedom is a refusal: keys out of order, a slot numbering that could be chosen two ways, unsorted realizations. So the same object cannot be written two ways, and two meanings cannot be merged into one ID. The rule came from experience. Under the first encoding, nothing enforced the order of a satisfaction’s realizations, so one logical satisfaction could carry two IDs.

The second rule is that identity belongs to the kernel term after elaboration. Binder names and elaborator metadata are erased, so renaming a bound variable changes nothing. Two terms that are definitionally equal but written differently stay different objects, because the store does not try to decide meaning.

Some things are left out of identity on purpose. The checker binary, the host and the store’s axiom policy are not in any ID. Under the first encoding the checker and the axiom ceiling were, and moving the checker from one machine to another re-addressed 1,655 objects (decision 0027). Today the checker is recorded in receipts, which are local to a store, and the axiom ceiling is the store’s policy.

Names and files as views

No object holds a declaration’s name. In the reuse run of 16 Oct 2026 (docs/research/minimal-reuse.md), twice_id was renamed double_id in its source and submitted again. Every object was identical, nothing new was stored, and the only change was a new alias. A consumer written against the new name, bound through that alias, elaborated to exactly the objects of the consumer written against the old one.

Presentation works the same way. The server’s view method renders a stored statement in the contract syntax, and the Lean an agent wrote is one more way to produce the same objects. Neither one is the object.

Separate statement, template and proof objects

A definition or theorem is not stored as one blob. It is split into parts that change for different reasons:

• the statement, which is its type;
• the template, which is its value with every maximal proof subterm cut out and replaced by a numbered slot, {"tag":"slot","index":0} and so on (a theorem’s whole value is a proof, so its template is one slot);
• one proof object per slot, holding the proof’s term, type and context;
• a satisfaction, which binds the statement, template and proofs, and resolves citations through sorted realizations;
• the declaration, which names its satisfaction.

Inside statements, templates and proofs, citations are indirect. A definition is cited by the ID of its template, and a theorem by the ID of its statement. Only the satisfaction’s realizations say which concrete declaration a citation means. Slots carry no type, so a proof can change inside a definition without changing the definition’s template.

The split exists because in a dependent type theory, proofs sit inside ordinary values. A structure such as Std.Map.Order carries proof fields, and a bounds-checked array access carries a proof that the index is in range. If a definition were hashed whole, re-proving one of those embedded facts would give it a new ID and change every object that cites it.

What survives an edit

The reuse run measured what one proof-only edit changes. implA_law (∀ x, implA x = x) was re-proved with a different term. Then the consumer par_twice, which cites it, was rebound to the new proof:

The statement, template and proof of par_twice kept their IDs, because par_twice cites implA_law by its unchanged statement. Only the binding chain moved: the consumer’s satisfaction now realizes the new declaration. Rebinding the consumer cost one replay of its own declaration through the pinned Lean 4.34.1 kernel. Every later submission that used the generic theorem twice_id imported it from its module. None replayed it again, apart from the final reverify, which was an audit.

Two consequences follow.

No consumer moves to a new proof by itself. The old par_twice stays accepted and bound to the old proof, and the alias reuse.par_twice decides which of the two declarations the name means. Bindings are concrete because Lean’s kernel may unfold theorems when it reduces Acc.rec. Which proof is bound can therefore affect whether a dependent replays, so replay is always of a concrete binding. The API has no rebind method. To rebind, you elaborate and submit the consumer again.

Records and families are concrete too. Their kernel names derive from their own IDs. A record or family that cites a declaration whose binding changes gets a new ID, and so does everything that cites the record or family. The stability above holds only along dependency chains that do not pass through a record or family.

Aliases outside identity

An alias maps a name to {id[, role], generation} in the store’s aliases.json. Aliases are store records, and objects never cite them, so moving an alias re-addresses nothing. A client sees a new target only when it looks the name up again and binds the new ID.

Objects never change but names do, so alias moves are guarded. Every move names what it expects the alias to hold (expect), or says overwrite: true explicitly. Generations count moves and are never reused, so an expectation with a generation detects a name that went from A to B and back to A. The replace method moves an alias between implementations only with an accepted replacement claim. Move an alias safely gives the steps.

What content addressing does not give you

Content addressing leaves several things to other parts of the system:

• Equivalence. implA and implB compute the same function and have different IDs. An ID says which term, not what the term means.
• Trust. An ID says nothing about whether an object was checked. Acceptance is per store, receipts are never copied from another store, and objects that move between stores are replayed again (How acceptance works).
• Stability across rule changes. There is one running encoding, so a change to the identity rules re-addresses every object, and the accepted objects are rebuilt from source with no migration. When decision 0030 replaced expression trees with shared expressions, every ID changed. A new Lean source revision has the same effect, because every object carries the namespace that names it.
• Stability through records and families, as described above.

The objects reference lists every kind and field, and Reuse a proof by identity lets you make these edits yourself.