Runtime configuration

The file that names the pinned Lean, the output directory and the shared lock, and the limits every native call runs under.

A runtime configuration is a small JSON file owned by the operator. It names locations, plus an optional call budget; every other limit is fixed in the code (crates/lema-check/src/pins.rs). lema serve, check-runtime, build, run, test, cap-build and the release commands that read artifacts each take one with --runtime CONFIG. Writing one is covered in write a runtime configuration.

Format

{"schema":"lema.runtime-linux/v2","distribution":"/home/me/.lema/toolchains/lean-4.34.1-linux-x86_64","output":"/home/me/.lema/evidence","shared_lock":"/home/me/.lema/native.lock"}

This is the form scripts/cloud-setup.sh writes, with the user’s home directory in place of /home/me.

The file is read by lema_check::parse_config, with these rules:

• It is at most 16,384 bytes, with exactly these fields; an unknown or repeated field is refused. A v1 file with call_budget is refused.
• Every path is absolute and has no .. component.
• The configuration file, the distribution, the output and the lock must each be a real file or directory (not a symlink) of the right kind, owned by root or the running user, and not writable by group or others. Every parent directory must be the same, except that a root-owned sticky directory such as /tmp is allowed.
• The output and the distribution must not overlap. Neither the lock nor the configuration file may be inside the distribution.
• The whole distribution is checked against the pinned manifest when the configuration is loaded: every file is hashed, about 3 GB.

Loading records the configuration’s SHA-256 and the identities (device and inode) of the output directory and the lock file. A later call is refused if the configuration’s contents change, or if the output or the lock is replaced.

Decision 0033 plans to drop call budgets from configurations. At HEAD 5a94951, call_budget is still read and enforced.

The output directory

The output directory must exist before the first call and must not be writable by group or others; README.md and the setup script create it with mode 0700. A native call named CALL writes:

<output>/
  ledger.jsonl            one reserve line before and one complete line after every native call
  HALTED                  this output's HALTED latch, present only after a fault
  CALL-reserved.json      the call's record, written before it runs
  CALL.log                its merged standard output and standard error, at most 16 MiB
  CALL-result.json        its record, written after it runs
  work/CALL/              its work directory (mode 0700), the only writable path in its sandbox
  modules/                the module cache: LemaCodebase and LemaDelta.d<hash> modules
  artifacts/NAME/         built artifacts (build, test, cap-build, the retired http-build)

A call name is 1 to 100 bytes of ASCII letters, digits, - and _, and is used once per output. work/ and artifacts/ are created with mode 0700 when missing. modules/ and artifacts/ are read-only inside every sandbox.

The ledger

<output>/ledger.jsonl holds one JSON object per line. The runtime reads it before every call, and refuses the call while any reservation has no completion or resolution, or any completion carries a fault that is not resolved.

unit is the call’s systemd scope, lema-native-<hex>.scope. host is the observed host state: host_kind, mem_total, mem_available, memory_pressure_some_avg10 and cpu_pressure_some_avg10. A line with any other event makes the ledger unreadable, and every call is then refused. info reports the number of reservations as native_calls_used.

HALTED latches

There are two latch files. While either exists, every native call is refused.

A call faults on a timeout, a late completion, log overflow, incomplete capture, a reaping failure, a scope that never appeared, or a change to the distribution during the call. A scope that cannot be confirmed gone is a host-wide fault.

The latch holds one line, CALL: FAULT. It is written before the ledger’s completion line, so a fault stops later calls even if that line cannot be written. Clearing a latch is described in recover from a HALTED latch.

Decision 0033 plans for a call-level fault to fail only its own call, while cleanup failures still halt the host. At HEAD every fault latches the output it happened in.

The shared lock

A call takes an exclusive flock on shared_lock and keeps it until the call is complete. A call waits up to 10 minutes for it, then fails with native lock busy. Configurations that name the same lock file run their calls one at a time: scripts/cloud-setup.sh derives every configuration it writes from $LEMA_HOME/native.lock. Calls under other lock files are still seen, because a call is refused while any lema-native-* systemd user unit is live.

Checks before every call

Under the lock, before the reservation, the runtime checks:

1. Neither latch exists.
2. The ledger has no open reservation and no unresolved fault.
3. The call budget, if any, is not used up.
4. The configuration’s contents are unchanged, every path is still protected, and the output and lock are the same files.
5. The pinned host files have their digests, and the user manager has the cpu, memory and pids cgroup controllers (requirements).
6. No lema-native-* scope is live.
7. The distribution’s metadata (device, inode, size, times, mode, link count and owner of every entry) equals the snapshot taken when it was verified.
8. At least 4 GiB is free on the output’s file system and on the lock’s.
9. The host is quiet: Linux on x86_64, at least 6 GiB available, memory pressure and CPU pressure within their limits.

Per-call limits

Each native call runs as systemd-run --user in a transient scope, inside bubblewrap. The values are constants in pins.rs.

The wall time is 120 seconds for check-runtime, 300 for elaborate and 600 for reverify and executable.

A linked native executable has no counterpart of Lean’s --memory=4096. Its memory is bounded only by the scope’s 4 GiB without swap, so exhaustion ends the scope instead of raising a Lean error.

The memory floor

Before every call, /proc/meminfo’s MemAvailable must be at least 6 GiB (MIN_AVAILABLE, 6 × 1024³ bytes). The same check refuses a memory pressure above 10.0 or a CPU pressure above 40.0, each the some avg10 value of /proc/pressure/memory and /proc/pressure/cpu. A refusal reads:

host pressure; native execution refused (available BYTES, memory avg10 VALUE, cpu avg10 VALUE)

lema check-runtime exits with code 75 for this refusal only when the machine’s total memory is at least 7 GiB, the floor plus 1 GiB; below that the machine can never pass, and the exit code is 1. Decision 0033 plans to drop the CPU-pressure refusal and turn the memory floor into a bounded wait. At HEAD both are refusals.

Related

• Requirements and environment variables
• The lema command
• Recover from a HALTED latch