Store records

The records a store keeps beside its objects, such as aliases, bundles, revisions, policies and releases, with their fields and IDs.

A store holds objects, which are identified by their content and accepted by kernel replay. It also holds records above object identity: names, selections, history, decisions and releases. No object cites a record, so a record never changes an object’s ID, and records are outside the identity rules that crates/lema-core/tests/identity.rs pins. None of them is a kernel check. The rules below are store rules, tested without a runtime; the code is in crates/lema-store/src/.

Overview

<ab> is the first two hex digits of the ID.

Content IDs

A record’s content ID is the SHA-256 of a hash domain of its own followed by the record’s canonical JSON:

id = sha256("LEMA-<KIND>-v1\0" ‖ canonical(record))

The domains are LEMA-BUNDLE-v1, LEMA-BINDING-MAP-v1, LEMA-AUTHORING-v1, LEMA-SNAPSHOT-v1, LEMA-REVISION-v1, LEMA-POLICY-v1, LEMA-GUARANTEE-v1, LEMA-MERGE-v1, LEMA-REVIEW-v1, LEMA-CHANGE-REPORT-v1 and LEMA-RELEASE-v1, each followed by a zero byte. They differ from each other and from the objects’ LEMA-TYPED-CORE-v3, so a record can never have an object’s ID.

These rules hold for the stored records with a content ID: bundles, project records and releases. A change report shares the canonical form and the bounds.

• Fields are exact, and unknown fields are refused. Lists are sorted with no repeats, except the parents of a revision or a merge record, whose order is meaningful. Empty optional fields are absent, except a policy’s require.axioms, where [] means no axiom and is kept. A record in any other form is refused, never repaired.
• Every list, every text and the whole record have a maximum size.
• A record is written once. Its creation is a history.jsonl line: "event": "record" with kind and id for project records, "bundle" for bundles, "release" for releases. Every read re-checks the bytes, the ID and the rules.
• A creation request’s lists are sorted before hashing, and a repeated item is refused, never merged. The same content in any order gives the same record.
• Every object a project record names must be accepted; an obligation’s statement, clients and dependencies need only be stored. Every record it names must already be stored, so the revision graph has no cycles.
• Every record but a policy carries namespace, the namespace object’s ID. A policy carries one only when it has protect gates.

Two kinds of text recur. A path is relative: /-separated components of ASCII letters, digits and ._-+@, none empty, . or .., at most 256 bytes. An actor ID is 1 to 128 bytes of ASCII letters, digits and ._@-, starting with a letter or digit.

Aliases

aliases.json maps a name to {id, role?, generation}.

A name is 1 to 512 bytes with no control characters. Aliases are never removed, so a generation is never reused, and an expectation with a generation detects a move from A to B and back to A. Every move names what it expects the alias to hold, or overwrite: true (server methods). Each request’s changes are one history line, {"event", "changes": [{name, target, generation, previous, overwrite?}], …}, written before aliases.json is replaced. Moving an alias safely is the move an alias guide.

Bundles

A bundle names a set of accepted objects once. elaborate’s receive binds its exports as Received.* names, which builds exactly the objects that the same bindings written by hand build.

A bundle record is at most 4 MiB. bundle.create resolves from_aliases once: the record holds the IDs the aliases named then, and later alias moves do not change it. Using bundles is the name a set of objects with a bundle guide.

Binding maps

A binding map selects a project’s roots and exported names.

At most 8 MiB. Renaming an export changes the binding map, not the objects. binding-map.create also takes from_aliases and alias_prefix, read once.

Authoring bundles

An authoring bundle keeps original source, source-to-object mappings and notes.

At most 16 MiB. authoring.create always writes unchecked: the stored source is not claimed to reconstruct anything. Only publish with authoring writes elaborated, which records that this server elaborated exactly these inputs into the mapped objects in that call. inputs_sha256 is sha256("LEMA-ELABORATION-INPUTS-v1\0" ‖ canonical JSON) of the request’s source, roots, prefix, bindings, receive, seeds and seed_salt. It is a record of what happened, not a re-check.

Snapshots

A snapshot is a binding map plus separately referenced authoring material and assets.

At most 4 MiB. The store holds only an asset’s digest and size, never its bytes. Editing documentation changes the snapshot and not the binding map, and two histories that reach one state share its snapshot ID.

Revisions

A revision goes from its first parent’s after-snapshot, or from the empty state, to after.

At most 1 MiB. An obligation is {claim, statement?, clients?, assumptions?, depends?}: a claim of 1 to 4,096 bytes, the statement object it names (if any), and up to 256 client IDs, assumption texts (each at most 1,024 bytes) and dependency IDs.

Obligations are inherited. Each obligation open in any parent is either listed again, exactly, or discharged. by must be an accepted theorem whose statement is the obligation’s statement, matched by identity; an obligation without a statement can only be waived. An obligation cannot be both open and discharged, and only one some parent has open can be discharged. Bringing a waiver into a project reference needs an actor in the active policy’s waive list.

Policies

A policy decides who may move a project reference and what a revision must meet.

At most 256 KiB. An absent or empty reset or waive means nobody.

A gate protects an implementation export by identity.

review lists reviewers (1 to 256 {actor, authority}, authority delegated or steward, sorted by actor), and optionally adopt (the authority an adoption needs), distinct: true (a reviewer’s approval does not count for its own move) and display: true (only approvals bound to the approval view they read count). A steward’s review meets a delegated requirement.

Project references

refs.json maps a reference name to {policy, revision, generation}.

A name follows the alias rules. A reference moves only through ref.create, ref.publish and ref.adopt, through the same engine as aliases: one history line per request, with the actor and the decision. It never takes an overwrite, and every move names the revision, generation and policy version it expects. Setting one up is the set up a project reference guide.

Actors

actors.json (lema.actors/v1) maps an actor ID to {operator, token_sha256}. lema actor add writes it with the server stopped and shows the token once. An operator may create project references. A token authenticates the bearer of a token the operator issued, and nothing more: every client of a local store runs as the store’s OS user, who can also read and write the store’s files. Tokens are not rotated or revoked in this version.

Reviews

A review records one reviewer’s decision on one move of a project reference.

At most 256 KiB. Each review.create also appends the decision to the history, even when the record exists already, so a reviewer’s latest decision on a transition is defined. An approval never stands in for missing evidence.

Guarantee records

A guarantee record stores one Std.Guarantee.IR receipt that executable computed with profiles, for a revision to cite as evidence. No method takes one from a client.

At most 64 KiB. Its receipt’s own claim is “tested, not proved”: a static check of the captured Lean.IR closure of the roots, which reads what the elaborating process reported.

Merge records

A merge record stores the three-way comparison of two or more lines against their common base.

At most 16 MiB. A conflict is on an export, asset, source or note, and is a collision, delete-update, update-update, rename-rename or bundle conflict. Immutable objects are never merged; a conflict is between bindings. The merge revision itself is a revision.create with the merged snapshot, the same parents in the same order, and the base. Merging is the report on a change and merge two lines guide.

Change reports

A change report says what moving from one snapshot to another changes, computed by identity from the two snapshots’ binding maps, assets and authoring bundles, never from source text. It is a computed view and is not stored; the same store state gives the same report and the same ID. It is at most 16 MiB.

Missing evidence becomes an open obligation in the revision format. The store has no deprecation record, so a removal always stays open until an authorized waiver closes it.

Releases

A release is an immutable record of what a deployment runs: one artifact pinned to the store’s accepted closure and to a deployment configuration’s digest. release.create checks the artifact against the tool’s rules and pins before it writes the record. A release adds no claim of its own: its proof receipts are the store’s kernel receipts, and the artifact and its IR receipts are tested.

program.artifact is the artifact’s ID, the SHA-256 of its canonical key. program.binary is {backend, file, sha256}. A record is at most 8 MiB.

The deployment digest is sha256("LEMA-DEPLOYMENT-v1\0" ‖ canonical(input)), over an input with schema lema.release-deployment/v1: the capability configuration as given and the digest of each trust anchor it names. Credential files are never opened, so no secret value enters the input or the release.

A release is never changed. A withdrawal is a record releases/<ab>/<id>.withdrawn.json (lema.release-withdrawal/v1) and a history line, and either one withdraws it; a withdrawn release cannot be selected. A supersession is a history line, and a superseded release can still be selected, as a rollback. Selection takes a release ID, never a name, and needs the release’s creation line in this store’s history. Withdrawal and supersession stay local to one store. Releasing is the release an artifact guide.