Content addressing

A declaration’s identity in Rainbow is the hash of what it says. As the environment module puts it: “Names are navigation aliases, never identity.”

Declaration ids

kernel/add-declaration computes the id from the declaration’s kind, universe parameters, type, value, transparency, dependencies and schema version (source). That map is written in the canonical encoding of canonical.clj, a deterministic, type-tagged serialisation that sorts map entries and set members, and hashed with SHA-256 into an id such as "sha256:3506a443...".

A constant in a term is [:const "sha256:..." levels], so an id depends on the ids of everything the declaration uses. When a declaration arrives with an id attached, the kernel recomputes it and rejects a mismatch, so a checkpoint or bundle cannot pass a proof off as a different declaration.

An inductive block is hashed from its descriptor with parameter and field names replaced by positions, and each member gets the hash of the block id and its key.

Aliases

An alias is a symbol such as nnrat/add-zero-right. A declaration can have several, and neither aliases nor provenance are part of its id. Adding existing content under a new alias adds the alias. An alias that already names a different id is rejected with :kernel/alias-conflict.

Environments and checkpoints

An environment id hashes the sorted ids of its declarations and inductive blocks. A checkpoint id hashes the whole checkpoint. Loading a checkpoint recomputes its id, sends each declaration back through the kernel and requires the recorded environment id.

On 12 October 2026, 256 checkpoints held 525,504 copies of 2,634 distinct declarations. So the repository stores each declaration once, in artifacts/store/declarations.edn.gz, and a checkpoint refers to the SHA-256 of the stored text. The store is not trusted: a missing or altered entry gives a checkpoint whose id does not match, and it is rejected.

What content ids give you

Two people who build the same declaration get the same id, whatever they named it. A kernel that receives a proof recomputes every id itself. When lein reproduce rebuilds a checkpoint, equal ids mean the same declarations. Altered content no longer matches its id. A later declaration depends on exactly the statement and proof it refers to, and renaming a file cannot shift it.

The ids rely on the JDK’s SHA-256, part of the trusted base.