Architecture — lungo documentation

lungo makes Lean code available to programs in Rust, C, Go, Python, Swift, Objective-C and TypeScript without asking Lean to be anything but Lean. This page explains how the pieces fit together and why they are arranged this way.

Lean compiles Lean

The obvious way to translate Lean into Rust would be to read Lean source, or Lean’s elaborated terms, and translate them. lungo does neither. Lean source is extended by macros, notations and elaborators that only Lean can run, and elaborated terms still contain proofs, types, type classes and definitions by well-founded recursion, whose executable meaning Lean’s compiler decides. A translator working at that level would have to reimplement a large part of Lean, and would sooner or later disagree with it.

Instead, lungo lets Lean do everything up to the point where Lean’s own compiler hands its output to a backend. Lake builds the project with the exact toolchain it pins, so the project’s syntax extensions run, its proofs are checked by Lean’s kernel, and its definitions are compiled by Lean’s compiler, exactly as for a native Lean build. lungo starts from the compiled program: a small, first-order, imperative intermediate language with explicit reference counting, which is what a backend has to implement anyway. Everything above it stays Lean’s responsibility.

This is also why a Lean project needs no annotations or changes to be used from Rust, and why invalid Lean or a false proof fails the Rust build: they fail the Lean build first. What a project may add, through lungo’s Lean library, says something about its code (what is proved of an export, what the host provides and is assumed to do); it never changes what the code computes.

The pipeline

build.rs / lungo ──► lake build ──► worker ──► Bridge IR + interface ──► verifier ──► generators
                     (Lean)         (Lean)                                (Rust)       (Rust)

Lake elaborates, checks and compiles the root modules. lungo only reads what Lake produces; it never parses Lean source.
The worker is a Lean program, compiled against the project’s toolchain, that loads the compiled environment, selects the program (the root modules’ code, their initializers, everything they call) and encodes it as Bridge IR together with metadata: exported declarations and their types, extern symbols, source locations and trust information. Its assurance pass reads the project’s claims, specifications, facilities and assumptions (see below). It runs as a separate process, so the build survives it crashing or hanging.
The verifier checks the Bridge IR independently of the worker that produced it.
The generators write the program and its interface in each requested language (see below), and lungo writes the program’s assurance document, assurance.json, the same in every output.
Publication replaces each output directory atomically, and in build.rs tells Cargo which files to watch.

The same library runs from build.rs and from the lungo command, so the command line always sees what the build sees.

One program, many languages

Generating code for a language has two parts, which lungo keeps apart:

Execution: the compiled program, instruction by instruction, with Lean’s reference counting and object layout. There are two: Rust (the compiler layer of a Rust crate) and C (compiled by the host language’s C toolchain: cgo, Xcode, a Python build, clang for WebAssembly). Both run on the same runtime, lungo’s Rust port of Lean’s runtime; C calls it through its C ABI (lungo.h), as Lean’s own C backend calls libleanrt.
Projection: the API of the exported declarations in the language’s own terms: Rust structs and enums, Go structs and sealed interfaces, Python dataclasses, Swift structs and indirect enums, TypeScript objects and tagged unions, C values with typed accessors.

The description every projection starts from is the program’s interface: the exported functions with their types, the types they use, the facilities the host implements (each an interface with a method per operation), the async facilities whose operations the program’s async exports ask a handler to perform, and the entry point, with the program’s assurance document alongside. It is to lungo what the FileDescriptorSet is to protoc: a generator is a function from it to files, whether it is built in or a plugin (lungo-gen-<language>) receiving it as JSON.

Rust keeps its own projection, which converts Lean objects directly. Every other language crosses a single boundary: the program’s C entry points take their arguments and return their results in one binary encoding, the wire format, and each language’s support library encodes and decodes it. One call is one crossing, however deep the value; recursive types, arbitrary-precision numbers and polymorphic functions are handled by the one codec in the runtime, driven by a table of the program’s types. Values a language cannot hold as data (Lean closures, opaque values, IO.Errors) cross as handles, and functions of the host language cross into Lean as callbacks.

An export returning an async program (Lungo.Async.Program) returns its first step: its value, or the operation it asks the host to perform and a resumption. The host performs the operation in its own asynchronous terms and resumes the program with the answer, getting the next step. The runtime keeps each waiting program under its resumption, which can be used once: resumed, or given up when the caller is cancelled or the handler fails. Each language turns this into its own async functions.

A process has one runtime: the generated packages of any number of programs share it, and it is prebuilt for every platform and distributed with each release, so that no one using Go, Python, Swift or TypeScript compiles Rust. See the runtime distribution.

lungo’s Lean library

A Lean project that wants to say more than its code requires lungo’s Lean library (lungo-rs/lean, the Lake package lungo, released with lungo under the same version). It has two layers. The first is ordinary Lean: specification helpers (contracts, behavioral models, state machines, traces and protocols, runtime monitors) and async programs, which a program may run. The second is a set of attributes (@[lungo_claim], @[lungo_spec], @[lungo_facility], @[lungo_operation], @[lungo_assumption], @[lungo_role]) that run while the project is compiled.

An attribute checks what it is given and writes a record: a definition next to the declaration it describes, in a fixed form, with no compiled code. The records travel with the module’s compiled environment, so the worker reads them without running anything. Its assurance pass does not trust them: it checks each one again against the environment (a claim’s evidence is a theorem, its statement mentions its subjects and has its relation’s shape, an operation is an extern, an async facility’s answers are fixed by its operations), finds the assumptions a claim’s statement takes as hypotheses, reads the axioms its proof depends on, and fingerprints every record. Problems are errors with codes of their own (LNG07xx), and a record written by hand is held to the same rules.

The attribute modules need Lean’s own elaborator, which no program should carry. They are therefore link barriers: the program’s linked modules stop at them, so a program importing the library carries only code it runs, and adding a claim changes none of the program’s compiled code. Modules named as assurance modules are loaded only for their records, typically laws kept out of the program; nothing of them is linked either. A program that uses a value only a module it does not link would initialize is refused (LNG0710).

What the pass finds becomes the program’s assurance document, assurance.json, written into every generated output and embedded in each language’s package (see formal assurance and the assurance document).

Two layers of generated code

The compiler layer is mechanical and not meant to be read or called: it mirrors Lean’s compiled program, including its reference counting and in-place updates, with Lean’s runtime object layout. The facade is the part designed for people: Lean structures become Rust structs, Nat becomes an unbounded Nat, IO becomes Result, and conversions happen at the boundary. Keeping them apart lets the compiler layer stay faithful to Lean while the facade stays idiomatic Rust.

The Lake project is the configuration

A Lake project already says what it is made of: its package name and its default targets, the libraries and executables lake build builds. lungo reads both instead of asking for them again. By default it compiles the root modules of the default targets, as Lake itself resolves them (so a lakefile.lean computing its targets is understood as well as a lakefile.toml), exports what those modules define, and names the generated module after the package. A build.rs therefore needs only the project’s location, and a crate includes the result by the package’s name with lungo::include_lean!, much as a crate generating gRPC code with tonic compiles .proto files and includes them by package with include_proto!.

What Lean cannot know, the application configures: which Rust traits generated types derive, attributes for libraries such as serde, and which Lean types are provided by Rust types that already exist, such as those another lungo build generated. These settings name Lean declarations, and one that names nothing is an error rather than a silent no-op, so configuration cannot drift away from the Lean code it shapes.

Why the toolchain is pinned exactly

Lean’s compiler output is not a stable format; it changes between releases. The worker is therefore built for one toolchain, and its adapter to the compiler’s data structures is validated for that release. A project pinning an unsupported toolchain is rejected before anything is compiled, rather than translated by an adapter that might misread it. Supporting a new Lean release means adding an adapter for it.

Builds are reproducible and offline

A Cargo build must not change the project, download anything, or depend on where it runs. lungo never installs toolchains or fetches Lake dependencies during a build (the manifest must be committed and dependencies present), never writes into the Lean project, and writes output that contains no machine-specific paths. Its output depends only on the inputs recorded in its build key, so an unchanged project reuses the previous output, and two builds of the same project produce the same files.