Restricted Lean

What the Lean source sent to elaborate and publish may contain, and how the server turns it into a draft of objects.

The elaborate and publish methods take Lean 4.34.1 source and return canonical objects. Not every Lean file can be turned into objects: the exporter, the canonical validator, kernel replay by the pinned Lean 4.34.1 kernel and, for code that will run, the executable vocabulary each refuse some constructs. This page lists what each one refuses and where the rule lives in the repository.

Rules are enforced by code. Conventions, listed at the end, are what the repository’s own sources do without anything checking them.

How source is processed

1. The server checks the bindings before any native call (Store::draft_bindings in crates/lema-store/src/bundle.rs). Every Received.* binding must name an object accepted in this store, with a role that object has. A name bound twice, an unknown bundle, a target that is not accepted or a role its object lacks is refused without a native call.
2. It installs the received objects as Lean modules (LemaCodebase and LemaDelta.d<hash>), replaying any that no module holds yet.
3. It writes one Lean file and elaborates it in the sandbox. The file is the header, one Lean alias per binding, set_option Elab.async false, the source, and the lema_export command (export_inner in crates/lema-check/src/engine.rs).
4. The exporter (lean/codebase/Exporter.lean) walks every constant to export and everything they reach, refuses what it cannot export, and writes a lema.checked-export/v3 table.
5. The Rust builder (lema_core::build) turns the table into canonical objects and returns the draft: objects, names (each draft name to {id, role?}), and received_bundles when the request had receive.

The draft is untrusted. The exporter runs in the same process as the source, so its output is whatever the source makes it. Only submit (or publish, which submits in the server) accepts objects, by source-free kernel replay.

The generated file has this shape. Angle brackets mark the parts that vary.

import LemaCodebase
import LemaDelta.d<hash>
run_cmd Lean.modifyEnv fun env => Lean.addAlias env `Received.<name> `LemaStored.h<id>
set_option Elab.async false
<source>
lema_export

When the request receives nothing, the header is import Lean followed by the exporter’s text instead of the module imports.

Request fields

publish takes the same fields, plus aliases (draft names to alias, each with {expect} or {overwrite: true}), an optional idempotency_key and an optional authoring record. The server methods reference has the responses.

The header and imports

The source has no import lines. The server writes the header itself, and the source comes after it, where Lean does not accept import. engine.rs describes the source as restricted Lean “which must not import anything beyond Lean”.

Lean is in scope for the exporter, but its constants cannot be used: every constant the draft uses and neither defines nor receives becomes an external object, and an external must come from Init or a module under Init (see Externals).

Names and the prefix

• With prefix, every local constant under the prefix is exported, except Lean’s internal names (such as _unsafe_rec) and unsafe or partial implementations. roots adds names. The exporter then follows every constant they reach, including the types of inferred proof slots; a family and its constructors, recursor and projections are exported together.
• Names are views. The draft’s names maps each name the draft defines to its object ID, with a role for a family’s or record’s members. Init externals and received names are not listed.
• The contract view shows published names without the LemaDraft. prefix.

Received bindings

A binding makes an accepted object visible to the source under a Received.* name. The server adds a Lean alias from that name to the object’s kernel constant, so the draft refers to the accepted object by identity and never re-creates it.

• bindings maps Received.<a dotted identifier> to {id, role?}.
• receive binds every export of a bundle: an export N becomes Received.<as>.N, or Received.N without as. rename changes N. A name bound twice, by two receives or by a receive and an explicit binding, is an error that names both sources.

A declaration is bound by its plain ID, with no role. A record or family is bound by its ID and one of its roles:

A family’s casesOn and recOn are separate declarations, bound by their own IDs. An excerpt of lean/json/grammar-bindings.json:

{
  "Received.Value": {
    "id": "5c917509b9ff99e27154727b64601f146939fa9fab235e4325620760d1d886ae",
    "role": "type"
  },
  "Received.arrNil": {
    "id": "5c917509b9ff99e27154727b64601f146939fa9fab235e4325620760d1d886ae",
    "role": "ctor:4"
  },
  "Received.decode": {
    "id": "a3a0fee4d8225d714a4dcbf0ce63766a020cb4c73f21f53228cae77609963f45"
  }
}

Seeds

Records and families are nominal: each carries a seed in its identity, so two structurally equal families with different seeds are different objects (case D2 of crates/lema-core/tests/identity.rs). For each inductive type the draft defines, the seed is seeds[name] if the request gives one (64 lowercase hex digits), and otherwise:

sha256("lema.seed/v1\0" ‖ seed_salt ‖ "\0" ‖ name)

(family_seeds in crates/lema-cli/src/main.rs.) The same salt and name give the same seed, so elaborating the same source again gives the same IDs. lean/core/seeds.json holds the seeds of the accepted Core v1 Prog and Impl, so that Core v2 elaborates them as the same objects.

Declarations

Unsafe declarations and partial def are never exported, and an exported declaration that reaches one is refused. sorry is refused because sorryAx is below the fixed floor.

An inductive type must be a single self-recursive family. The exporter refuses, with these messages:

• a nested family: “it occurs inside another type, such as a List; only single self-recursive families are supported: use spine constructors”;
• a mutual group: “only single self-recursive families are supported”;
• an indexed family: “only parameters are supported”;
• fewer than 1 or more than 64 constructors: “1 to 64 are supported”.

A family’s casesOn and recOn are exported as generated helpers, which replay regenerates and compares.

Size bounds

The exporter’s proof-marking walk over a definition’s or theorem’s value visits at most 200,000 nodes (skeletonBound): “a definition’s skeleton has more than 200000 nodes”. Validation applies the same bound to every template term, counted as a tree with binder domains included.

Other bounds apply to every object. An object is at most 16 MiB as canonical JSON; an expression value has at most 2^20 nodes and its tree is at most 256 deep; a string literal has at most 65,536 code points. The objects reference lists them all.

Externals

Every constant the draft uses that it neither defines nor receives becomes an external object. The exporter refuses:

• an external from a module outside Init and Init.*: “non-Init external”;
• an unsafe external;
• an external whose axiom footprint is below the fixed floor.

Validation refuses an external object whose module is outside Init, and replay checks each external against the running Lean.

Axioms

Every exported constant’s axiom footprint must stay above the fixed floor and, at replay, within the store’s axiom policy. The floor is sorryAx, Lean.ofReduceBool, Lean.ofReduceNat, Lean.trustCompiler, any axiom with a _native name component, and unsafe constants. native_decide adds a _native axiom in Lean 4.34.1, so a proof that uses it is refused. The exporter refuses floor axioms at export; replay audits the footprint again. The axiom policy reference has the details.

Evaluation in proofs

Proofs by computation are evaluated by the kernel at replay. These results were measured on the pinned Lean 4.34.1 and are recorded in lean/core/rules.md and lean/data/Evaluate.lean:

Every native call runs with a 4 GiB memory cap. A lookup in a 100,000-entry table passed in a bare file but failed when exported (“excessive memory consumption detected”); a module with a 10,000-entry lookup was elaborated, replayed and checked again by reverify through the API. A kernel that runs out of a resource gives an inconclusive result, never a refusal.

Received families

A received family has only the helpers stored with it: its recursor, casesOn and recOn. Some elaborations therefore differ from the same source with the family local (docs/architecture.md, “Authoring”):

• A match with a catch-all arm (_ or a variable) does not elaborate: Lean 4.34.1 builds it from the family’s ctorIdx, which a received family lacks.
• cases and injection on an equation between constructors do not work: they need noConfusion.
• The sizeOf helpers of a type with a field of a received family use Lean’s default size for that field.
• There is no brecOn, so recursion over a received family by match is unavailable. Recursion goes through the recursor, bound with the role generated:rec: lean/core/Transport.lean uses Received.progRec, and Text in lean/json/Grammar.lean is defined by the received family’s recursor.

A draft can declare structures and inductive types with fields of a received type: replay registers each installed family’s compiler metadata (no code and no kernel constant). Regenerating the missing helpers is scheduled after the Stage 4 gate (decision 0032).

Received structures

Replay registers a received record with the structure metadata Lean gives a structure compiled from source: fields named f0, f1 and so on, reducible projections, and a flat constructor. Field labels are not stored.

Parents, default values and classes are not mirrored. A received class is used through its projections applied to an instance.

Code that calls received definitions

Received definitions are installed with no compiled code, so Lean’s compiler cannot compile code that calls them. The repository’s sources that receive definitions put their bodies in a noncomputable section (for example lean/std/Map.lean, lean/std/Sha256.lean, lean/json/Check.lean). It adds no axiom and skips no kernel check.

Code that will run is compiled from source, not from received objects. The executable method takes no bindings or receive. An execution manifest’s pieces are rewritten with noncomputable section as section and noncomputable def as def before they are compiled, and a piece with whole: false is cut at the line /-! End of the execution slice (crates/lema-http/src/artifact.rs).

Code that will run

The executable method and lema build compile the roots and check the compiled Lean.IR closure of each root against the executable vocabulary (crates/lema-check/src/vocabulary.rs). Each refusal names its rule and the call path from the root.

The IR capture (lean/exec/Capture.lean) also refuses a compile with any local @[extern], @[implemented_by] or @[csimp] declaration, any theorem of the form @f = @g between constants, any sorry, any @[export] declaration, and local initializers. Every root must be a function compiled in the same call, so a root with no compiled code is refused; there are 1 to 64 roots.

Consequences:

• ByteArray.toList reads with get!, so code that calls it is refused. LemaDraft.Bytes.view (lean/data/Bytes.lean) is the list view for specifications, with bridge lemmas such as view_getElem?.
• Classical.ofNonempty is a lean_sorry extern, refused by the extern rule.
• Text in running code is bytes. lean/std/Sha256Exec.lean writes ok and FAIL as ASCII byte values.

Conventions

These are what the repository’s sources do. Nothing enforces them.

• set_option autoImplicit false at the top of a source file. Every file in lean/core/ has it; many in lean/std/ do not.
• prefix set to LemaDraft, with the source in namespace LemaDraft.
• seed_salt set to the source’s path (lean/core, lean/std/Sha256Spec, lean/json/Json).
• Library files written in received form (lean/std/Hmac.lean, Sha256.lean) are checked locally by reading Received. as LemaDraft.Std..
• Short direct proofs over received declarations. Received declarations lack the source elaborator’s metadata, and lean/core/README.md records that such proofs worked better than simp-heavy ones.