The Lean library

lungo’s Lean library is the Lake package lungo, released with lungo at lungo’s version (its sources are lean/ in lungo-rs). A project imports it to state what lungo carries into the packages it generates (formal assurance): the attributes write records the worker reads, and the helper modules hold the definitions claims are usually stated with.

Requiring the library

From a checkout or a vendored copy, by path:

# lakefile.toml
[[require]]
name = "lungo"
path = "../lungo-rs/lean"

From the lungo-rs repository, at the tag of the lungo you generate with:

[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v1.88.0"
subDir = "lean"

Run lake update once and commit lake-manifest.json: lungo’s builds never fetch dependencies. The library pins the same Lean toolchain as lungo (leanprover/lean4:v4.34.1).

Then import Lungo. It imports two parts:

• Lungo.Core: Lungo.Registry and the helper modules below. They import only Init and declare no initializers, so a program carries exactly the code of them it calls.
• Lungo.Attr: the attributes. They need Lean’s elaborator and run only while the project is compiled; lungo never links them, or the parts of Lean they import, into a program.

The records the attributes write are versioned by Lungo.Registry.schemaVersion (1). lungo refuses a library whose version it does not read (LNG0709).

Kinds

A specification kind, a claim relation, a role and a facility identifier are namespaced strings: two or more .-separated segments of lowercase letters, digits and _ (and - after the first segment), each starting with a letter — lungo.decides, acme.cost-bound, timing.clock.

The lungo namespace is lungo’s own and holds only these:

Any other namespace belongs to whoever defines it: lungo checks its spelling, carries it into every package and gives it no meaning. A package can define its own relations and kinds this way (examples/semantic-model defines acme.cost-bound) with no change to lungo.

Attributes

Every attribute is global: local and scoped uses are refused, and so is giving one to a declaration of another module (a record is read where its declaration is). A declaration gets each attribute once. Each writes one record, the internal constant decl._lungo_<kind>; the worker checks every record again when it reads the compiled project (LNG0701–LNG0707).

@[lungo_spec "kind"]

Marks a specification of the given kind. Any declaration can be one. A specification that is a logical object — a contract, a relation, a protocol — is best noncomputable, so it is not exported.

@[lungo_spec "lungo.contract"]
noncomputable def SortsAscending : Contract (List Nat) (List Nat) := sortedPermutation fun a b => decide (a ≤ b)

@[lungo_claim "relation" subject f … spec S …]

On the theorem that proves the claim: its subjects f … stand in relation to its specifications S …. subject is followed by one or more declarations; spec and the specifications are optional.

@[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]
theorem sort_satisfies : Satisfies sort SortsAscending := …

Checks: the declaration is a theorem; each subject exists, is not a theorem and is mentioned by the statement; each specification has @[lungo_spec] and is mentioned by the statement; none is named twice; and for a lungo.* relation, the statement has the shape the relation requires. Only the statement is read, never the proof. The assumptions a claim is conditional on are not declared: lungo finds them among the types of the statement’s leading ∀ binders.

@[lungo_facility "ns.name"]

Names a facility the host provides, by its identifier. It is given to any declaration that is not a theorem — usually an empty structure — or to an instance of Lungo.Async.Interface Op, which makes an async facility whose operations are the constructors of Op.

@[lungo_facility "timing.clock"]
structure Clock

inductive StoreOp where
  | get (key : String)
  | put (key value : String)

@[lungo_facility "store.kv"]
instance storeOps : Lungo.Async.Interface StoreOp where
  Ret
    | .get _ => Option String
    | .put _ _ => Unit

For an async facility, Op must be an inductive type without parameters or indices, no field of a constructor may be a proof or a type, and what each constructor answers (Ret) must reduce to a type that does not depend on the constructor’s fields (LNG0707).

@[lungo_operation C]

On an @[extern] declaration: it is an operation of the facility C, which the host implements. Write @[extern "symbol"] first; the attribute applies after the declaration is compiled.

@[extern "timing_now", lungo_operation Clock]
opaque now (u : Unit) : IO Nat

Checks: C has @[lungo_facility] and is not an async facility; the declaration has @[extern]. lungo further requires an operation to have a C entry and not to be implemented by the runtime or by an @[export] (LNG0706). An operation whose Lean type is not IO or EIO is a function to Lean, which may evaluate a call once and keep the value: the host’s implementation must answer the same for the same arguments.

@[lungo_assumption C]

On a proposition (or a family of them, or a class in Prop): it is assumed, never proved, of the host’s implementation of the facility C. A claim taking it as a hypothesis is conditional on it.

@[lungo_assumption Clock]
def Ticks : Prop := 0 < ticksPerSecond ()

@[lungo_role "role"]

On a definition a program runs (not a theorem): what it is for. lungo.oracle marks a reference implementation other code is tested against; lungo.monitor, lungo.model and lungo.implementation are lungo’s other roles.

Relations

A claim under one of lungo’s relations must state it in its shape, so the relation means the same in every package. The shape is read from the statement after its leading ∀s; f mentions every subject means each subject occurs in f.

Helper modules

Lungo.Spec.Contract

• Contract α β with pre : α → Prop and post : α → β → Prop; Satisfies f c: every input meeting pre gives an output meeting post.
• ExceptContract α ε β adds refuses : α → ε → Prop; SatisfiesExcept f c for a function returning Except ε β: it returns an output meeting post, or refuses as refuses allows.
• Contract.Strengthens strong weak and satisfies_weaken; Contract.seq and satisfies_comp for two functions in sequence.

Lungo.Spec.Model

• BehavioralModel β with admits : β → Prop; Refines impl spec: every behaviour impl admits, spec admits.
• BehavioralModel.ofFunction f, ofRelation r, function_refines_relation, inter and refines_inter; refines_refl and refines_trans.

Lungo.Spec.State

• StateSpec σ ι ο with init, invariant and step : σ → ι → ο → σ → Prop.
• For an executable step exec : σ → ι → ο × σ: StateSpec.Preserves s exec (initial states satisfy the invariant and every step keeps it) and StateSpec.Implements s exec (from states satisfying the invariant, every step is one step allows).
• StateSpec.run exec, preserves_run and reachable_invariant: a preserved invariant holds over every run from an initial state.

Lungo.Trace

• Protocol ε: the traces it allowed, closed under prefixes; Protocol.any, always p, ofSteps start next, both, Within and within_trans.
• Reducer ε σ with start and step : σ → ε → Option σ; Reducer.run, Reducer.protocol and accepts_iff.
• ReducerRefines r p (every trace r accepts, p allows) and refines_of_invariant, which proves it from an invariant linking states to the traces that reach them.
• Hyperproperty ε and Noninterference r low observe, for properties over several traces.

Lungo.Monitor

• Monitor ε σ with start and step : σ → ε → Except String σ: a host feeds events one at a time; an error is a violation and its reason.
• Monitor.run, Accepts, and Sound m p: m accepts exactly the traces p allows.
• Monitors with their soundness: ofPredicate (ofPredicate_sound), ofReducer (ofReducer_sound), and both (both_sound).

Lungo.Async

• Interface Op with Ret : Op → Type, what each operation answers.
• Program Op α: done value or call op resume; a Monad, with Program.perform op. An export returning a Program is an async function in every language, taking a handler that performs the operations.
• Program.run handler: interprets a program in any monad, so claims can run it against a model of the host.
• Exchange, Admits p exchanges a, trace answer p, and the theorems admits_trace, run_id, admits_unique and admits_bind.

The library’s own tests

lake build LungoTest checks, with #guard_msgs, every refusal of every attribute.