How programs reach the outside world

Why Lema applications touch the network, files, credentials and clock only through four flat-byte primitives, and what stays assumed.

A Lema application does not call the operating system itself. This is the child task of lean/cap/FanFiles.lean, the example application. It writes a file, reads it back and reports whether the bytes match.

/-- Task 1: write `fan/<i>`, read it back, report. -/
def child (input : ByteArray) : Received.Prog AppCmd AppReply ByteArray :=
  Received.call (AppCmd.file (fileRequest 1 (path (index input)) (contents (index input)))) fun written =>
  Received.call (AppCmd.file (fileRequest 2 (path (index input)) ByteArray.empty)) fun read =>
  Received.ret (line (index input) (okWith written ByteArray.empty && okWith read (contents (index input))))

child is a value: a program that issues two file commands and continues from their replies. Something else answers those commands, and the place where that happens is the line between Lema and the outside world.

Applications are pure programs

An application is a task table, Nat → ByteArray → Prog AppCmd AppReply ByteArray. Task 0 applied to the run’s input is the main program, and its result is the run’s output. The commands are defined in lean/cap/AppCmd.lean:

An application is a Prog value of the Program core. So what it does can be stated as theorems over a contract for these commands, and those theorems are proved and accepted like any other.

The trusted runner, lean/cap/Runner.lean, answers the commands. It is platform code in namespace LemaRunner, about 70 lines of definitions, and it is not a Lema object. It maps each capability command to a primitive, and each ticket command to a Lean task on a dedicated thread. When a program returns, the runner waits for every child it left running. It allows at most 48 sub-programs running at once and 8 levels of nesting. A start past either bound runs nothing, and the await for its ticket answers refused. The runner is total: it uses structural recursion on Prog, with no partial or unsafe definition. It is meant to realise the scheduling theorems of lean/core/Tickets.lean. That it does is tested by a boundary conformance suite (crates/lema-cap/tests/runner.rs), not proved.

The executable vocabulary keeps the runner the only way out. The capability primitives, and Lean’s task and reference externs, are admitted only on calls from the runner’s own compiled code, and that code’s Lean.IR is pinned by digest. An application root that reaches a primitive is refused. An application’s closure cannot even name one, because the exporter refuses any external constant from outside Lean’s Init.

The Flat-Byte FFI rule

The whole boundary is four primitives in lean/cap/LemaCap.lean:

@[extern "lema_cap_https_exchange_lean"]
opaque primHttpsExchange (request : @& ByteArray) : IO ByteArray

@[extern "lema_cap_atomic_file_op_lean"]
opaque primAtomicFileOp (request : @& ByteArray) : IO ByteArray

@[extern "lema_cap_credential_op_lean"]
opaque primCredentialOp (request : @& ByteArray) : IO ByteArray

@[extern "lema_cap_clock_now_ms_lean"]
opaque primClockNowMs : IO UInt64

The rule comes from decision 0031. A capability primitive takes and returns only a flat byte buffer (@& ByteArray → IO ByteArray) or a fixed-width word (UInt64). A primitive never raises. Every failure is an outcome tag inside the response frame, whose format is in crates/lema-cap/FRAMES.md.

lean/cap/glue.c, 50 lines, is the only code that touches lean.h. It uses lean_sarray_cptr, lean_sarray_size, lean_alloc_sarray with a byte copy, lean_box_uint64 and lean_io_result_mk_ok. It builds or inspects no other Lean value: no constructors, closures, strings or tasks.

Everything typed sits above that line, in Lema, where it can be proved:

• the frame codecs (lean/cap/Frames.lean), with bijection and trailing-byte refusal theorems;
• HTTP/1.1 (lean/cap/Http1.lean): rendered requests and response parsing with Content-Length, chunked and close framing, proved against its own serialisers;
• object storage, which has no primitive: S3 is HTTPS signed in Lema (lean/cap/S3.lean), with a theorem that the bytes sent are the bytes signed;
• SigV4 signing (lean/std/SigV4.lean), where signing with the derived key is proved equal to signing with the secret;
• the operation record (lean/cap/Record.lean), with a crash model proved sound for every schedule.

Seven lean/cap modules (Frames, Capability, Http1, Record, CredentialModel, S3 and S3Model) were accepted through the API on 17 Oct 2026, published together with the libraries they receive (30,178 objects). All 916 theorems in those modules have receipts from the pinned Lean 4.34.1 kernel within propext and Quot.sound.

What the shims enforce

Behind glue.c is crates/lema-cap, a Rust static library built on rustls 0.23.45 with ring, and webpki-roots 1.0.9. Its shims enforce the deployment configuration that LEMA_CAP_CONFIG names:

• approved origins only, each with its host, port, connect addresses, trust roots, and request, response and deadline limits;
• TLS with host-name verification, and no redirects or retries;
• whole-file operations strictly inside one state directory, with atomic writes (temporary file, fsync, rename, directory fsync);
• credentials the program never holds. A bearer secret is a header the shim adds only on requests to its own origin. For SigV4, primCredentialOp returns the access key ID and the signing key for one date, region and service. It first checks that the region and service are the configured ones, and that the date is the UTC date of an instant within 15 minutes of the shim’s clock. The long-lived secret never enters the program, a frame or a diagnostic.

All of this is tested in crates/lema-cap/tests, not proved. The tests cover every HTTPS outcome against a local TLS fixture, deadlines against slow peers, path refusals, atomic writes under injected failures and kills, and signing keys against AWS’s published examples and an independent HMAC. The shims bind a program only if that program can reach the outside solely through the primitives. For an execution manifest’s app entry, the vocabulary check and the fixed runner provide that. The application sandbox shares the host’s network namespace, so code outside that check could reach services that listen only on the host’s loopback.

Development and production

An app entry has two builds. For development, lema build --cap builds an artifact that runs the checked compile under lean --run, with --load-dynlib naming the capability library libLemaCap.so. That is the only --load-dynlib the runtime admits, and only for the content-pinned library that lema cap-build produced.

For production, lema build --standalone compiles an executed module that imports only Init and LemaCap. It is compiled separately from the import Lean compile that checks the roots, and linked with the pinned leanc against LemaCap.c, glue.c and liblema_cap.a. The build ties the two compiles together. Every declaration of the executed module except its fixed main must have the checked compile’s Lean.IR text. Below Lean.IR, the link is assumed. Compiling apart keeps the binary small: a one-line Init-only program linked by leanc measured about 4.3 MiB, against about 116 MiB with import Lean (16 Oct 2026).

Both builds run in an application sandbox with four threads, a 400% CPU quota, at most 64 tasks and 4 GiB of memory. Build a capability app has the commands.

Checked, tested and assumed at the boundary

Decision 0031 sums up the result: theorems about Lema programs over their capability models are checked, and that the binary realises them rests on the assumed and tested parts. Checked, tested and assumed explains the words.

Why this design

The alternative, option A in decision 0031, kept new applications under lema-host, a Rust host that ran Lean workers over a pipe. Protocol framing, operation-record journaling, recovery from an unknown storage outcome and request signing would then have lived in Rust code with no proofs. Under the chosen option B they are Lema code with theorems. What Lema cannot prove (TLS, sockets, fsync) sits behind four byte-level calls that are tested at their frames. lema-host and its apps are now retired (decision 0033).

Flat bytes also keep the native boundary small. Decision 0031 adopted the rule to remove the risk of maintaining code against lean.h. Glue that never builds or inspects a Lean value beyond byte arrays and the IO result needs only five functions of Lean’s C interface. A third option stays open: a capability that needs its credentials kept out of the application’s process can be served by a helper process behind the same Lema signature. And because the Rust backend is on hold (decision 0029), production binaries come from Lean’s own compiler through leanc.