How to state claims about exports

This guide shows how to say, in Lean, what an exported definition is proved to do, so that every generated package carries it: a claim is a theorem registered with @[lungo_claim], naming the exports it is about (its subjects) and the specifications it relates them to. The examples are the sort and session crates in lungo-rs’s examples directory.

Require lungo’s Lean library

The attributes are in lungo’s Lean library, the Lake package lungo in the lean directory of lungo-rs, released with lungo at lungo’s version. Require it from the project’s lakefile:

# lakefile.toml
[[require]]
name = "lungo"
git = "https://github.com/machinefabric/lungo-rs"
rev = "v<lungo version>"
subDir = "lean"

(or path = "…/lungo-rs/lean" for a checkout), run lake update once, commit the manifest, and import Lungo where claims are stated. A library of another schema version than the lungo you build with is refused (LNG0709). The attributes add records only: the compiled program is the same with or without them.

Mark the specifications

A specification is the declaration a claim relates its subjects to: a contract, a model, a state machine, a protocol. Give it @[lungo_spec "<kind>"]:

import Lungo

namespace Sorting

open Lungo.Spec

/-- Numbers in ascending order: the output is ordered and a permutation of the input. -/
@[lungo_spec "lungo.contract"]
noncomputable def SortsAscending : Contract (List Nat) (List Nat) where
  pre _ := True
  post xs ys := ys.Pairwise (fun a b => decide (a ≤ b)) ∧ ys.Perm xs

lungo’s kinds are lungo.relation, lungo.contract, lungo.model, lungo.state, lungo.protocol and lungo.property; any other namespace is a package’s own (acme.cost-model), carried without interpretation. The library’s helpers for writing specifications are Lungo.Spec.Contract, Lungo.Spec.BehavioralModel, Lungo.Spec.StateSpec, Lungo.Trace.Protocol and Lungo.Monitor (see lungo’s Lean library).

Make a specification that is only logical noncomputable: a contract or a protocol has nothing to run, and a computable definition of the root modules is exported like any other. An executable model (a reference implementation) can stay computable and be exported.

State the claim

Prove the theorem, then register it with the relation, the subjects after subject and the specifications after spec:

def sort (xs : List Nat) : List Nat := xs.mergeSort fun a b => decide (a ≤ b)

@[lungo_claim "lungo.satisfies" subject sort spec SortsAscending]
theorem sort_satisfies : Satisfies sort SortsAscending := by
  intro xs _
  refine ⟨List.pairwise_mergeSort ?_ ?_ xs, List.mergeSort_perm xs _⟩
  · intro a b c hab hbc; simp only [decide_eq_true_eq] at *; omega
  · intro a b; simp only [Bool.or_eq_true, decide_eq_true_eq]; omega

The attribute checks that the declaration is a theorem, that every subject is a definition (not a theorem) its statement mentions, that every specification has @[lungo_spec] and is mentioned, and, for lungo’s own relations, that the statement has the relation’s shape (after its leading ∀s):

A relation in another namespace (acme.cost-bound) is a package’s own: its shape is not checked. Anything the attribute refuses is an error in Lean; lungo checks the records it reads again, so a record written without the attribute is held to the same rules (LNG0701–LNG0705).

The session example claims that its step function implements a declarative state machine:

@[lungo_spec "lungo.state"]
noncomputable def Spec : StateSpec Sess Op Bool where
  init s := s = { isOpen := false, count := 0 }
  invariant _ := True
  step s op accepted s' := …

@[lungo_claim "lungo.preserves" subject step spec Spec]
theorem step_implements : Spec.Implements step := by …

Make assumptions explicit

When a claim holds only if the host behaves (its clock ticks, its store keeps what it is given), state that as an assumption (@[lungo_assumption], see how to declare facilities and assumptions) and take it as a hypothesis of the theorem:

@[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 claim is still proved; it is reported as conditional on Timing.Ticks, in every package. An assumption is a proposition, never an axiom, so a proof can only use it as a hypothesis, where the report sees it.

Require claims in the build

Make the build fail when an export lacks a proved claim:

// build.rs
fn main() -> lungo_build::Result<()> {
    lungo_build::configure().require_claims("Sorting.sort").require_claims("Sorting.rank").compile_lean("lean")
}

# lungo.toml
[assurance]
require-claims = ["Sorting.sort", "Sorting.rank"]

A path selects the export it names and every export in it as a namespace; "." selects every export. An export it selects that is the subject of no proved claim fails the build with LNG0602; a path selecting nothing is a configuration error.

The trust policy applies to the evidence too: a claim whose theorem depends on sorry fails the build under deny_sorry (on by default) with LNG0601, and deny_axioms refuses evidence resting on non-standard axioms. With deny_sorry(false) such a claim is reported incomplete, and does not count as proved for require-claims. forbid-assumptions refuses claims resting on an assumption (LNG0603).

Keep laws out of the program

Theorems about exports can live in a module the program does not import, such as a Laws module that imports the program. Name it as an assurance module: lungo loads it for its records, and never compiles it into the program.

# lungo.toml
[lean]
assurance-modules = ["Formal.Laws"]

(Builder::assurance_module("Formal.Laws"), or --assurance-module Formal.Laws). A root module cannot also be an assurance module: its records are read anyway. A program that would need a value only an assurance module’s initialization computes is refused (LNG0710).

Read the claims back

lungo assurance reports each export’s claims, what its proofs do not cover, and what its claims assume:

$ lungo assurance Sorting.rank
program sorting: Lean 4.34.1 (…), lungo 1.88.0, assurance schema 1

Sorting.rank
  == Claims ==
    [proved] lungo.satisfies Sorting.rank_satisfies (of Sorting.RanksByScore)
    [proved] lungo.law Sorting.rank_stable
  == Trust ==
    (none)
  == Assumptions ==
    (none)
  == Facilities ==
    (none)

--format json writes it for tools; --claim-kind, --facility, --assumption and --trust-issue select exports; --policy checks the policies and exits with status 2 on a violation (see the lungo command). lungo check counts the claims, and lungo inspect <declaration> shows them for one declaration.

Every generated package carries the same records as assurance.json (see the assurance document), and reads them natively:

let claim = sort::__meta::assurance().claim("Sorting.sort_satisfies").unwrap();
assert_eq!(claim.status, lungo::ClaimStatus::Proved);
assert_eq!(claim.specifications, ["Sorting.SortsAscending"]);