Glossary
The terms these docs use, each defined in a sentence or two, with the page that covers it.
Each term has one meaning across the docs. Code names are written as they appear in lema-lang.
| Term | Meaning | See |
|---|---|---|
| Accepted | Stored with a kernel receipt, or with an acceptance note checked_through a declaration that has one. Only submit (also called import) and publish accept objects. | How acceptance works |
| Actor | An identity the operator registers with lema actor add, authenticated by a local bearer token. It keeps cooperating actors apart; it does not stop a hostile local user. | Store records |
| Alias | A name in aliases.json that points at {id, role?, generation}. Aliases are outside object identity and move only with an expectation or an explicit overwrite. | Store records |
| Artifact | A program built from an accepted closure into the runtime output’s artifacts/, and checked again before every run. Its behaviour is tested; no proof receipt is issued for what it outputs. | Execution manifests |
| Assumed | Trusted without proof: the Lean kernel and compiler, the Rust acceptance path, leanc and clang, Linux, glibc and the operator. | Checked, tested and assumed |
| Axiom policy | The axioms a store allows above the fixed floor, set by lema init and kept for the store’s life. The default is propext, Quot.sound and Classical.choice. | Axiom policy |
| Backend | How an artifact is built and run: lean (Run.olean under lean --run) or lean-native (an executable linked by leanc). The rust backend is on hold. | Execution manifests |
| Binding map | A record that selects a project’s roots and exported names, by object ID. | Store records |
| Bundle | A lema.bundle/v1 record that names a set of accepted objects once. elaborate’s receive binds its exports as Received.* names. | Store records |
| Capability | A primitive in lean/cap/LemaCap.lean through which an app reaches the outside: an HTTPS exchange, an atomic file operation, a credential operation or the clock. Each takes and returns bytes, except the clock, which returns a UInt64. | Capabilities |
| Change report | A lema.change-report/v1 view, computed by identity, of what a revision, a reference move or a pair of snapshots changes, with the evidence each change needs. | Store records |
| Checked | Accepted by kernel replay with the pinned Lean 4.34.1 kernel, within the store’s axiom policy above the fixed floor. | Checked, tested and assumed |
| Client | A lema command that sends one request to the server’s socket and prints the result. | The lema command |
| Closure | An object together with every object it depends on, directly or not. Acceptance, export and releases work on closures. | Objects and identity |
| Contract | What must be true of an implementation, stored as a statement or a definition. In Core v2 a Contract has pre, next and post. It is not an object kind. | Program core |
| Contract syntax | The read-only text in which view shows stored statements (law) and definitions (def): a small subset of Lean’s term syntax. | Contract syntax |
| Draft | The untrusted objects elaborate builds from restricted Lean. Nothing in a draft counts until submit accepts it. | Server methods |
| Elaborate | The method that turns restricted Lean, with accepted objects bound as Received.* names, into a draft. | Server methods |
| Execution manifest | A lema.exec/v1 file that names an accepted program’s roots, entry, source pieces, profiles and backends, from which lema build makes an artifact. | Execution manifests |
| Fixed floor | The axioms and constants refused whatever a store’s policy says: sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, any _native axiom and any unsafe constant. | Axiom policy |
| Generation | A counter on an alias or a project reference: 1 at creation, one more at each move, never reused. An expectation with a generation detects a move from A to B and back to A. | Store records |
| Guarantee record | A lema.guarantee/v1 record of one Std.Guarantee.IR profile receipt that executable computed. A revision can cite it as evidence. | Store records |
| HALTED latch | A file, <output>/HALTED or <shared_lock>.HALTED, written when a native call faults. Every native call is refused while one exists. | Runtime configuration |
| ID | An object’s identity, sha256("LEMA-TYPED-CORE-v3\0" ‖ canonical JSON), written as 64 lowercase hex digits. Records have IDs in hash domains of their own. | Objects and identity |
| Idempotency key | An optional request field. A retry with the same key and the same request returns the first response and applies nothing again. | Server methods |
| Implementation | A definition that computes what a contract describes. In Core v2 an Impl is a step function over private state. It is not an object kind. | Program core |
| Kernel replay | Re-adding each declaration of a closure to the Lean kernel (addDeclCore) from its canonical objects, with no source. It is the only way objects are accepted. | How acceptance works |
| Law | The contract syntax’s form for a theorem’s statement, law name binders : statement. The proof is not shown. | Contract syntax |
| Ledger | <output>/ledger.jsonl: a reservation line before and a completion line after every native call. | Runtime configuration |
| Method | A request name the server answers, such as elaborate or ref.publish. A command is a subcommand of lema. | Server methods |
| Namespace | The object that fixes Lean’s version and git hash, and so the meaning of Init. Every other object names it. | Objects and identity |
| Object | A canonical typed value with schema lema.core/v3, of one of nine kinds: namespace, external, statement, template, proof, satisfaction, declaration, record or family. | Objects and identity |
| Obligation | An open claim a revision carries until an accepted theorem of its statement, or an authorized waiver, discharges it. | Store records |
| Policy | A lema.policy/v1 record that says who may publish, adopt, reset or waive on a project reference, and what a revision must meet (require, protect). | Store records |
| Profile | A Std.Guarantee.IR static check over compiled IR: NoCopySliceCall, NoBigIntPrimitives or NoBoxOrCtorInCycles. Profiles are not part of object identity. | Execution manifests |
| Project reference | A name in refs.json that points at {policy, revision, generation}, also called a ref. It moves only under its active policy. | Store records |
| Publish | The method that runs elaborate and then submit inside the server, so a client never holds the draft. | Server methods |
| Receipt | A store-local record of an object’s acceptance: the checker, the axiom footprint and the module. It is never copied from another store. | Objects and identity |
Received.* binding | A Lean alias in a draft for an accepted object, given by ID. A received object is reused by identity, never re-created. | Restricted Lean |
| Release | A lema.release/v1 record that pins one artifact to the store’s accepted closure, its receipts and a deployment configuration’s digest. | Store records |
| Restricted Lean | The Lean that Lema takes as source: no imports, no unsafe or partial declarations, and inductive families of the single self-recursive kind only. | Restricted Lean |
| Revision | A record of a move from one snapshot to another, with its intent, evidence and open obligations. | Store records |
| Runtime configuration | The lema.runtime-linux/v2 (or v1) file that names the pinned Lean distribution, the output directory and the shared lock. | Runtime configuration |
| Satisfaction | The object kind that binds a statement, a template and proofs, with realizations that resolve each citation to a concrete declaration. | Objects and identity |
| Server | lema serve: the process that owns one store and answers one JSON request per connection on a Unix socket. | Server methods |
| Shim | The Rust code in crates/lema-cap behind each capability primitive, which enforces origins, limits and credentials. Its behaviour is tested. | Capabilities |
| Snapshot | A record of what a project selects: a binding map, with authoring bundles and assets by digest. | Store records |
| Store | A directory of objects, receipts, aliases, history and records, written by one process at a time under an exclusive lock. | Objects and identity |
| Submit | The method that kernel-replays a draft’s closure and accepts it whole or not at all. import is the same method. | Server methods |
| Tested | Run and observed: compiled code, executables, sockets, OS behaviour and the store’s Rust rules. | Checked, tested and assumed |
Written against lema-lang at commit 5a94951, 17 Oct 2026.