lungo documentation

Formal assurance

What a generated package can say about its exports: claims proved in Lean, the assumptions they rest on, and how to read them.

In this section

A Lean proof is only as useful to the users of a generated package as what they can learn about it. lungo carries, into every package it generates, an account of what the program’s Lean code proves about each export, what each proof assumes of the host, and what lungo trusts to run the code: the package’s assurance document. This page describes the concepts the document is made of, how to read a claim, and what lungo checks and what it does not.

The parts of an assured program

A Lean project states them with the attributes of lungo’s Lean library:

  • Implementation. An executable definition the program exports, such as Sorting.sort. It is what runs, in every language.
  • Specification. A declaration saying what an implementation should do, without being one: a contract, a relation, a model, a state machine, a protocol (@[lungo_spec "lungo.contract"]). A specification that is a logical object, such as a contract whose fields are propositions, should be noncomputable: it has no code to run, and lungo exports only definitions Lean compiles.
  • Claim. A theorem, checked by Lean’s kernel, registered as evidence that its subjects (implementations) stand in a relation to its specifications: @[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]. A claim is exactly its statement; the relation names what kind of statement it is, and for lungo’s own relations its shape is checked.
  • Facility. A group of operations the host implements, in the host’s language: @[extern] declarations marked @[lungo_operation C], or the operations of an async facility. Lean sees only their types.
  • Assumption. A proposition about a facility that no proof can establish, because the host’s implementation is outside Lean (@[lungo_assumption C]). A claim taking an assumption as a hypothesis is conditional on it.
  • Oracle. An export used to test code written by hand: a slow, clear, proved definition (@[lungo_role "lungo.oracle"]) that another implementation is compared with.
  • Monitor. An executable checker a host feeds events into at run time, proved to accept exactly the traces a protocol allows (lungo.monitors).

Reading a claim

A claim’s status is proved when its evidence is a theorem the kernel checked that depends on no sorry, and incomplete when it depends on sorry (the default policy refuses that build, see below). A proved claim says that its statement is true. It says it about the Lean definitions, and lungo runs those definitions as Lean compiled them (see trust and verification for what that adds to the chain).

A proved claim with assumptions holds on every host whose facilities satisfy them, and on no other host is anything promised. Consider the clock example (examples/clock):

@[lungo_facility "timing.clock"]
structure Clock

@[extern "timing_ticks_per_second", lungo_operation Clock]
opaque ticksPerSecond (u : Unit) : Nat

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

def toTicks (seconds : Nat) : Nat := seconds * ticksPerSecond ()
def toSeconds (ticks : Nat) : Nat := ticks / ticksPerSecond ()

@[lungo_claim "lungo.roundtrip" subject toTicks toSeconds]
theorem toSeconds_toTicks (h : Ticks) (seconds : Nat) : toSeconds (toTicks seconds) = seconds :=
  Nat.mul_div_cancel seconds h

The package reports the claim as proved, with the assumption Timing.Ticks, and so does every export it is about. A host whose clock ticks a thousand times a second gets back the seven seconds it put in. A host whose ticksPerSecond answers 0 breaks the assumption: the program still runs, and the same round trip of seven seconds gives 0. The claim is not wrong — it never spoke about that host. The example’s C test runs both hosts:

round trip of 7 s: 7 s; deadline in 5 s, after 2.5 s: 2 s left
round trip of 7 s: 0 s; deadline in 5 s, after 2.5 s: 0 s left

Installing an implementation of a facility proves nothing about it. An assumption is an obligation on whoever writes the host code, stated where they can read it: in the generated documentation of the facility’s installer, and in the assurance document of every export whose claims rest on it.

lungo finds a claim’s assumptions in its statement: they are the registered assumptions among the constants in the types of its leading ∀ binders, as written. State an assumption as a hypothesis ((h : Ticks) → …); one hidden inside another definition is not found.

The trust base

What a reader of a proved claim relies on is the trusted base of every lungo program — the Lean toolchain, the worker’s adapter, the backends, the runtime distribution — and, for that claim:

  • the axioms its evidence depends on, listed in the document (evidence_trust); a claim built on an axiom beyond Lean’s propext, Classical.choice and Quot.sound is refused when the trust policy denies axioms;
  • its assumptions, which the host makes true or not.

What lungo checks

  • The records, twice. Each attribute checks its declaration when Lean elaborates it. The worker then reads every record from the compiled environment and checks it again, recomputing every fact a claim rests on: that the evidence is a theorem, that its statement mentions each subject and specification, that it has the shape its lungo.* relation requires, which axioms it depends on and which assumptions it takes. A record written by hand instead of by its attribute gains nothing: it is read and checked the same way, and one not in the canonical form is refused (LNG0701 to LNG0707).
  • The evidence. A claim resting on sorry is refused unless deny_sorry is off, and then it is reported incomplete; deny_axioms refuses evidence using non-standard axioms (LNG0601).
  • The policy. [assurance] in lungo.toml, or the same Builder settings, can require every selected export to carry a proved claim (LNG0602) and forbid assumptions or whole facilities (LNG0603).
  • Composition. Every record carries the Lake package declaring it and a fingerprint of its meaning (its own Lean terms and every definition of the workspace’s packages it reaches), so lungo assurance --compose can check that separately generated packages mean the same thing by a name they share (LNG0708).
  • Facilities at run time. A program refuses to run until the host has installed every facility it needs, naming the one missing.

What lungo does not check

  • The host’s implementation of a facility. Whether it satisfies the facility’s assumptions is the host’s responsibility; lungo only reports which claims depend on them.
  • That a pure operation is pure. An operation whose Lean type is not IO is a function to Lean, and Lean may evaluate a call with fixed arguments once and keep the value: a clock whose ticksPerSecond () changed while the program runs would not be seen to change. An operation that can answer differently must have an IO (or EIO) type.
  • That a statement means what its author intended. A claim proves its statement; the specification is only as good as what it says. Read the statement: the document carries it.
  • Relations of other namespaces. A relation such as acme.cost-bound is a package’s own; lungo checks its spelling and carries it, and gives it no shape.

Annotations and the generated program

Claims, specifications, roles and assumptions do not change the program: they add records, not code. Two things can still differ when a project starts importing Lungo:

  • Lean’s compiler reuses specializations compiled in any module the environment holds, and importing Lungo brings in the parts of Lean its attributes need. A specialization such as List.toString at a type may then come from a Lean module rather than the project’s own. lungo generates the code wherever it comes from, so the program behaves the same; only where its code is placed differs. A value such a module computes when it is initialized cannot be used, since the attribute modules are never linked (LNG0710).
  • A declaration given @[lungo_facility] or @[lungo_operation] does change the program: it turns an extern into an operation the host must provide.