lungo documentation

How to define a semantic model

Give a Lake package its own specification kinds and claim relations, which lungo carries into every package without any change to lungo.

In this section

This guide shows how a team defines its own vocabulary of specifications and claims, such as a cost model, a security level or a regulatory property, in a Lake package of its own. Other projects then state claims in that vocabulary, and lungo reports them as it reports its own.

The worked example is lungo-rs/examples/semantic-model. Acme’s package acme defines a cost model, and the inventory program proves that its lookups stay within it.

Choose a namespace

Specification kinds, claim relations, roles and facility identifiers are namespaced strings. Each is two or more .-separated segments of lowercase letters, digits and _, with - also allowed after the first segment, and each segment starts with a letter: acme.cost-model, acme.cost-bound, bank.audit.reviewed.

The lungo namespace is lungo’s own: only the kinds and relations lungo defines exist in it (lungo.decides, lungo.contract, …), and any other lungo.* string is an error. Every other namespace belongs to whoever uses it. Pick one that names your organization or domain.

Define the model in its own package

The model is ordinary Lean: definitions that say what your kinds mean, registered with @[lungo_spec] under your namespace. The package requires lungo’s Lean library for the attribute:

# acme/lakefile.toml
name = "acme"
version = "0.1.0"
defaultTargets = ["Acme"]

[[require]]
name = "lungo"
path = "../../../lean"

[[lean_lib]]
name = "Acme"

import Lungo

namespace Acme

/-- `steps` never exceeds `bound`. -/
def CostBound {α : Type} (steps : α → Nat) (bound : α → Nat) : Prop := ∀ a, steps a ≤ bound a

/-- At most `k` steps per unit of size, and `k` more: linear in `size`. -/
@[lungo_spec "acme.cost-model"]
def Linear {α : Type} (size : α → Nat) (k : Nat) (steps : α → Nat) : Prop :=
  CostBound steps fun a => k * size a + k

end Acme

A claim relation needs no declaration. It is the string a claim gives, and what it means is whatever your package documents. Write that meaning down next to the model, as the docstrings above do.

Claim against it

A project that uses the model requires the package and states claims with your relation, citing your specifications:

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

[[require]]
name = "acme"
path = "../acme"

import Lungo
import Acme

namespace Inventory

/-- The steps looking `sku` up takes. -/
def lookupSteps (sku : String) (items : List Item) : Nat := (lookupCounted sku items).2

/-- A lookup examines each item at most once: linear in the inventory's size. -/
@[lungo_claim "acme.cost-bound" subject lookupSteps spec Acme.Linear]
theorem lookup_linear (sku : String) : Acme.Linear List.length 1 (lookupSteps sku) := by
  ...

Run lake update once after adding the requirement, and commit the manifest: lungo builds never fetch or update dependencies.

What lungo checks, and what it does not

For a relation of your own, lungo checks everything that does not depend on what the relation means:

  • the relation is a well-formed namespaced string;
  • the evidence is a theorem, and its proof is checked by Lean’s kernel like any other;
  • every subject exists, is a definition rather than a theorem, and is mentioned in the statement;
  • every specification is registered with @[lungo_spec] and is mentioned in the statement;
  • the trust policy (deny-sorry, deny-axioms) applies to the evidence.

It does not check the statement’s shape. For lungo.* relations, lungo requires a shape (for example, lungo.decides must state f … = true ↔ P …). For yours, the statement can be anything that mentions its subjects and specifications. To keep claims under your relation uniform, give the relation a definition and cite it as the specification, as acme.cost-bound claims cite Acme.Linear. The statement then says, in your terms, exactly what is proved.

No part of lungo needs to change: the records, assurance.json, the generated packages and the lungo command carry your kinds as they are.

See it reported

lungo assurance Inventory.lookupSteps

Inventory.lookupSteps
  == Claims ==
    [proved] acme.cost-bound Inventory.lookup_linear (of Acme.Linear)
  …

lungo assurance --claim-kind acme.cost-bound lists the exports with such a claim. A require-claims policy is satisfied by a proved claim under any relation. In every generated package, the claim’s relation is acme.cost-bound and the specification’s kind is acme.cost-model, with package acme: the package that declares it, not the one that cites it.

Ship the model and check it stays the same

The model’s package can be generated on its own, for code that needs it at run time:

# acme/lungo.toml
project = "."

Every package that cites Acme.Linear then carries a fingerprint of the definition it was proved against, covering Acme.CostBound and anything else of Acme’s it unfolds to. Compose their documents with Acme’s to check that they all mean the same model; see how to compose assurance across packages.

See also