How to enforce trust and assurance policies

This guide shows how to make the build fail when an exported Lean declaration, or the proof of a claim about one, depends on unproven or unchecked code; how to require that exports carry proved claims and that nothing rests on an assumption you do not accept; and how to audit what exports depend on.

Choose the policies

Three policies apply to every exported declaration, and the first two also to the evidence of every claim (the theorem proving it):

Enable the ones you need in build.rs:

fn main() -> lungo_build::Result<()> {
    lungo_build::configure().deny_axioms(true).deny_unsafe(true).compile_lean("lean")
}

A violation fails with LNG0601 and lists each export with the offending dependencies:

error[LNG0601]: exported declarations violate the configured trust policy:
  Formal.step depends on `sorry` (deny_sorry)
  the claim Formal.step_implements depends on `sorry` (deny_sorry)

Remove the dependency in Lean, or stop exporting the declaration (for a claim, finish its proof or remove its @[lungo_claim]).

deny_sorry is on by default; turn it off only for work in progress (.deny_sorry(false)). With it off, a claim whose proof uses sorry is reported with the status incomplete, never proved.

Require proved claims

To make the build fail when an export carries no proved claim, select the exports by path (. selects every export; any other path the export it names and every export in it as a namespace):

fn main() -> lungo_build::Result<()> {
    lungo_build::configure().require_claims("Formal.step").require_claims("Formal.run").compile_lean("lean")
}

An export selected without a proved claim fails with LNG0602:

error[LNG0602]: the export Formal.run has no proved claim (`require-claims` selects it with "Formal.run"); state what it does with `@[lungo_claim]` on a theorem about it

A path that selects no export is a configuration error.

Forbid assumptions

A claim may be proved under an assumption about a host facility (see how to declare facilities and assumptions). To refuse what rests on an assumption you do not accept, forbid it by its Lean name; forbidding a facility forbids all its assumptions, and every export that calls its operations:

lungo_build::configure().forbid_assumption("Timing.Ticks").compile_lean("lean")

A proved claim assuming it, or an export needing a forbidden facility, fails with LNG0603. A name that is neither an assumption nor a facility of the program is a configuration error.

For the lungo command, the same settings are the [assurance] table of lungo.toml:

[assurance]
require-claims = ["Formal.step", "Formal.run"]
forbid-assumptions = ["Timing.Ticks"]

and lungo assurance --policy checks them without generating anything, exiting with status 2 when they are not met.

Audit without failing

To see the dependencies of every export without enforcing a policy, read assurance.json in the build output (the trust of each export, with its claims, assumptions and facilities; see the assurance document), list the exports with an issue with lungo assurance --trust-issue <issue> (sorry, axioms, unsafe, partial, facility, no-claim, incomplete, assumption), inspect one declaration with lungo inspect <name>, or read the metadata at run time:

for d in formal::__meta::declarations() {
    println!("{}: axioms {:?}, claims {:?}", d.lean_name, d.trust.axioms, d.assurance.claims);
}

partial definitions and extern dependencies are reported but not governed by a policy: they are ordinary parts of executable Lean code.