Execution manifests

The lema.exec/v1 record that names a program over accepted objects, its fields, entry kinds, IR profiles and the checks a build applies.

An execution manifest describes a program over an accepted closure: which accepted objects are its roots, which source files compile them, how its entry point is called, which IR profiles must hold, and which backends build it. lema build, lema run and lema test read it, so a new program needs no Rust code of its own. The format is defined in crates/lema-http/src/exec.rs and docs/architecture.md (“Execution manifests”); the committed manifests are in lean/exec/.

A manifest is a build input record, not an object. No object cites it and it never changes an object’s ID.

Shape

{"schema": "lema.exec/v1",
 "doc"?: "<text>",
 "entry": {"kind": "vectors" | "cli" | "app" | "worker", "root": "<a root's name>"},
 "roots": {"<name>": "<accepted ID>", …},            // 1 to 64
 "seeds"?: {"<family name>": "<64 hex>", …},          // the families the roots reach
 "pieces": [{"source": "<path under lean/>.lean", "whole": <bool>}, …],
 "received"?: {"<alias>": "<source name>", …},        // Received.<alias> in the pieces
 "profiles"?: {"<Std.Guarantee.IR profile>": ["<root>", …], …},
 "backends": ["lean" | "lean-native", …],             // the first is lema build's default
 "seconds"?: <1 to 600>,                              // a run's limit (default 120)
 "policy"?: {"inventory_sha256": "<64 hex>"},         // the reviewed IR inventory
 "expect"?: {"output_sha256": "<64 hex>"}}            // vectors and app only

Fields

A manifest file is at most 1 MiB. Every field is validated before any native call: an unknown field, kind, profile or backend, a root that is not a name or has no ID, an entry or profile root that is not a root, a bad piece path, and expect on a cli or worker entry are refused, as is the parked rust backend (“the Rust backend is parked (decision 0029)”).

Manifest ID

id = sha256("LEMA-EXEC-v1\0" ‖ canonical(manifest))

The canonical JSON is the same as for objects (Objects and identity), in a hash domain of its own. Arrays keep their order, which is meaningful for pieces and backends. A built artifact holds the manifest’s canonical bytes as exec.json, bound to this ID.

Entry kinds

The build tool’s fixed bridge (LemaExecMain) calls the entry and does the program’s I/O. It reads the fixed files input and args of the run’s work directory and writes output there. The entry’s declared type must be exactly the kind’s: the bridge pins it with _root_.rfl, so no coercion can be inserted.

An app entry is built against a capability artifact (--cap) and runs in the application sandbox (--deployment). A worker entry is refused with “the worker entry kind (a host-served app) is declared but not implemented yet”.

A run reads at most 64 MiB of input and 1 MiB of arguments in all, and returns at most 64 MiB of output.

Profiles

A profile is a named static check (Std.Guarantee.IR) over the captured Lean.IR of the roots’ closure (crates/lema-check/src/guarantee.rs). A cycle is a strongly connected component of the call graph with more than one function or a self-call; its iteration code is its functions and what they reach through functions with parameters.

lean_byte_array_copy_slice is ByteArray.copySlice, which extract, append and fastAppend reach.

For NoBigIntPrimitives, an arbitrary-precision operation is an extern whose C symbol starts lean_nat_ or lean_int_, and a conversion is a symbol ending _of_nat, _to_nat, _of_int, _to_int or _to_int_sint. Nat fuel is flagged.

For NoBoxOrCtorInCycles, an allocation site is a constructor with fields, a box of a uint64, usize, float or float32, a reset or reuse, a closure (pap), a string literal, a Nat literal from 2^32, or a call to an extern that builds a new object on every call (ByteArray.emptyWithCapacity, Array.mk, Array.toList, ByteArray.copySlice and others).

A profile’s verdict is holds, violated (with witnesses and their call paths) or unsupported (the check cannot decide, for example an ap in a cycle’s iteration code). In a manifest, requested means required: anything but holds refuses the build. The executable method reports a profile without requiring it.

Build checks

lema build makes one sandboxed Lean call that elaborates, as one module Run, the compiler settings, the tool’s own code (the bridge, the IR capture lean/exec/Capture.lean, the startup listing lean/exec/Startup.lean), the pieces in order with their Received.* names mapped, and the entry’s part of the bridge. It writes Run.olean (and Run.c for lean-native) and exports the roots. Then, before any artifact is written:

1. Same compilation: each root compiled to exactly its accepted ID, and the roots’ closure equals the accepted closure object for object.
2. Executable vocabulary: the captured Lean.IR closure of the roots has no finding (rules).
3. Startup surface: every constant a native executable evaluates when it starts is reached by the roots or is the tool’s own code. An unreached constant is refused by name; it must become a root with its accepted ID, or be cut from the pieces. A piece that mentions a tool namespace (LemaCodebase, LemaExecMain, LemaExecCapture, LemaExecStartup, LemaExecIr, LemaRunner) is refused before any native call.
4. Profiles: one receipt per requested profile over its roots, all holds.
5. Policy: with policy, the captured inventory’s digest must equal inventory_sha256; otherwise no artifact is written and the inventory is kept for review. Without it, the build records the inventory (inventory.json) and the vocabulary result.

An app entry adds checks: the compiled Prog, AppCmd, AppReply and Awaited must be the identities the runner was reviewed for, each of the 15 constructor names the runner dispatches on must resolve to its reviewed role, and the runner’s compiled IR must equal its pin. A standalone build compiles the executed module apart from the same pieces and requires every declaration in it to have the same Lean.IR text as in the checked compile, except main and main._boxed, which have fixed texts.

Pieces may hold declarations the roots do not reach. They are compiled into the module and nothing checks them; functions among them never run. The IR capture and the startup listing come from the process that elaborated the pieces, so these checks guard against honest mistakes, not a hostile piece: pieces are reviewed source.

Backends

An artifact (lema.exec-artifact/v1) holds Run.olean, inventory.json, closure.json, startup.json and exec.json, plus Run.c, Launcher.c and worker for lean-native. Its key binds the manifest ID, the entry, the backend, the toolchain and every checker, and lema run checks every binding again before it runs. An app entry produces lema.exec-app-artifact/v1, and a standalone build also lema.cap-app/v1.

Commands

lema build --manifest FILE --store DIR --runtime CONFIG --name NAME [--backend lean|lean-native] [--lean DIR] [--cap NAME] [--standalone]
lema run   --runtime CONFIG --artifact NAME [--release ID --store DIR --deployment FILE] [--manifest FILE] [--input FILE] [ARG ... | -- ARG ...]
lema run   --runtime CONFIG --artifact NAME --deployment DIR [--release ID --store DIR] [--manifest FILE] [--input FILE]
lema test  --manifest FILE --store DIR --runtime CONFIG --name NAME [--lean DIR] [--input FILE] [--cap NAME --deployment DIR] [ARG ... | -- ARG ...]

lema test builds every listed backend (artifacts <name>-<backend>), runs each once, and compares the outputs byte for byte, and with expect if the manifest has one. Its report is labelled tested. A run past seconds is a supervision fault and latches the runtime output, like any native call. The CLI reference lists every flag.

Evidence

The roots are checked: the store accepted them by kernel replay with the pinned Lean 4.34.1 kernel, and their receipts are the store’s. Everything about running them is tested execution, and no proof receipt is issued for executed output. The Lean compiler, the interpreter, the C compiler, the linker, the Lean runtime and the OS are assumed. For vectors and cli entries the executed module still imports Lean, because the exporter and the capture share its compilation.

Committed manifests

Example

lean/exec/sha256-vectors.json, verbatim. Sha256Spec.primes is a root because the whole specification is compiled and a native executable evaluates that constant at startup, though the entry does not reach it. The seed of Sha256Spec.State is the one publish derives from the salt lean/std/Sha256Spec.

{
  "schema": "lema.exec/v1",
  "doc": "Std.Sha256Spec's built-in vectors (lean/std/Sha256Exec.lean, report): one line per vector, the computed digest in hex and ok or FAIL. Sha256Spec.primes is a root because the whole specification is compiled and a native executable evaluates that constant at startup. Tested, not checked.",
  "entry": {"kind": "vectors", "root": "LemaDraft.Std.Sha256Exec.report"},
  "roots": {
    "LemaDraft.Std.Sha256Exec.report": "bb7485939d39dc8491500e529c17159333d7055132d8f5f461834b16ed96d200",
    "LemaDraft.Std.Sha256Spec.digest": "6e10cfbfa300ad372e777214525edc422c8a062a394de671aa3a1e36fbc6771b",
    "LemaDraft.Std.Sha256Spec.primes": "5af750af67badf65e8d41aea064c540384befe257742db3009d7c37d38871f4d"
  },
  "seeds": {"LemaDraft.Std.Sha256Spec.State": "5fef29f8204bdec70dbab76b393c5ed1d2dfddf25f67b495bc4823dc743c27bf"},
  "pieces": [
    {"source": "std/Sha256Spec.lean", "whole": true},
    {"source": "std/Sha256Exec.lean", "whole": true}
  ],
  "received": {
    "digest": "LemaDraft.Std.Sha256Spec.digest",
    "msg448": "LemaDraft.Std.Sha256Spec.msg448"
  },
  "profiles": {
    "NoCopySliceCall": [
      "LemaDraft.Std.Sha256Exec.report",
      "LemaDraft.Std.Sha256Spec.digest",
      "LemaDraft.Std.Sha256Spec.primes"
    ]
  },
  "backends": ["lean", "lean-native"],
  "seconds": 300,
  "expect": {"output_sha256": "5d56254e114e8d5bad83c62e6dc89b43b4bdaf9a93df60a2298162dbe62547dc"}
}

lema test --manifest lean/exec/sha256-vectors.json --store $STORE --runtime $CONFIG --name sha-vectors

The store must hold the published specification and lean/std/Sha256Exec.lean. The output is nine lines, each a digest in hex followed by ok or FAIL; Sha256Spec checks eight of the nine digests by kernel reduction, all but the 896-bit message’s.