A Lean library, lungo (in lungo-rs, lean/), for stating what a program’s exports do:
specifications (@[lungo_spec]), claims linking an export to the theorem proving it
(@[lungo_claim]), host facilities and the assumptions claims make of them
(@[lungo_facility], @[lungo_operation], @[lungo_assumption]), and roles
(@[lungo_role]). Helpers for contracts, behavioral models, state machines, traces and
protocols, runtime monitors and async programs come with it. A project requires it from Lake.
lungo reads these records from the compiled environment, checks them again (a record written
without its attribute is held to the same rules, LNG0701–LNG0707, LNG0709), and carries them
into every output as assurance.json. Every generated package exposes the document in its
language: __meta::assurance() in Rust, <id>_assurance_json() in C, Assurance() in Go,
ASSURANCE in Python and TypeScript, assurance in Swift.
deny-sorry and deny-axioms also apply to the theorems claims cite (LNG0601).
[assurance] in lungo.toml (and Builder::require_claims, Builder::forbid_assumption):
exports that must each carry a proved claim (LNG0602), and assumptions or facilities nothing may
rest on (LNG0603).
[lean] assurance-modules (--assurance-module, Builder::assurance_module): modules lungo
reads claims from without linking them into the program.
lungo assurance reports, for each export, its claims, trust, assumptions and facilities;
filters them; checks the policy (exit status 2); and composes documents of several packages,
refusing a record two of them describe differently (--compose, LNG0708, exit status 3).
lungo inspect reports an export’s claims, trust, assumptions and facilities, the claims a
theorem is evidence for, and the claims citing a specification. Both commands show an
assumption by what it says (its definition), not by its type alone.
Facilities
Host externs are now the operations of facilities, declared in Lean. The host-externs
setting and --host-extern are removed: an extern the host implements is marked
@[lungo_operation F], F a declaration marked @[lungo_facility "ns.name"].
Each facility is installed on its own: Set<Facility> in Go, set_<facility> in Python,
set<Facility> in Swift, load({ facilities: { … } }) in TypeScript,
<id>_implement_<facility>_<operation> in C. SetHost, set_host, setHost,
load({ host }) and <id>_implement_<operation> are removed. A call before every facility
is installed fails naming the facility and an operation (MissingFacilityError in Go, Python
and TypeScript, LungoMissingFacility in Swift; C ends the process).
In Rust, rust_extern maps only facility operations: mapping any other extern is an error
(LNG0706), as is an operation the runtime or an @[export] implements.
Async programs
An export returning Lungo.Async.Program Op α (Op registered with @[lungo_facility]) is
an async function in every language, taking a handler that performs each operation: an async fn with a handler trait in Rust, a context.Context and handler in Go, a coroutine in Python,
async throws in Swift, a promise with an AbortSignal in TypeScript, and steps
(lungo_step, lungo_resume, lungo_async_cancel) in C. An error of the handler, or
cancellation, abandons the program and releases it.
Compatibility
Runtime C ABI 2: programs generated by this lungo need its runtime (lungo_abi_v2).
Plugin protocol 3: the request carries facilities and async_facilities instead of
host_externs, and the assurance document; lungo writes assurance.json into every output,
and refuses a generator that writes it.
manifest.json no longer carries trust: it is in assurance.json.
Projects requiring one Lean package by path no longer race when built at once (Cargo’s
parallel build scripts): a build holds a lock on each package it builds.