This guide shows how to check that two or more packages generated by lungo agree about what they share, so that a claim one package proves against another package’s specification still means what it meant when it was proved.
Why composition needs checking
A claim can cite a specification from another Lake package. In the semantic-model example
(lungo-rs/examples/semantic-model), the inventory program proves that its lookups cost what
Acme’s model Acme.Linear allows, and Acme’s own package is generated and shipped separately:
inventory ──claims against──▶ Acme.Linear ◀──declares── acme
Each package carries its own assurance.json, generated from the Lean sources it was built
from. If Acme later changes Linear, or a definition Linear uses, a new Acme package and the old inventory package both
mention Acme.Linear, but no longer mean the same thing by it. The inventory’s claim was proved
against the old definition. Nothing in either package is wrong on its own; only comparing them
shows it.
What is compared
Every specification, claim, facility and assumption in an assurance document has a name, the
package that declares it, and a fingerprint: the SHA-256 of a canonical text of its Lean
declaration, of every definition of the Lake workspace’s packages that it uses, transitively,
and of the Lean version that elaborated it.
| Record | Its own text covers |
|---|---|
| Specification | its type and, for a definition, its value |
| Claim | its statement, subjects and specifications |
| Facility | its type, and for an async facility the types of its operations |
| Assumption | its type and, for a definition, its value |
The canonical text has no binder names or source positions, so reformatting or renaming a bound
variable does not change a fingerprint; changing what a declaration says does. So does changing
anything it uses that a workspace package declares: Acme.Linear unfolds to Acme.CostBound, so
changing Acme.CostBound changes Acme.Linear’s fingerprint too, and composition reports it.
Lean’s own definitions are covered by the Lean version instead. How each fingerprint is computed is
in assurance.json.
Composition takes every record that at least two documents describe, by kind and name, and requires all of them to give the same package and fingerprint. Records only one document has are not compared.
Compose documents
Pass each document with --compose:
lungo assurance --compose gen/inventory/assurance.json --compose gen/acme/assurance.json
composition: 2 documents agree on every record they share
When a record differs, lungo reports it as LNG0708 with what
each document says, and exits with status 3:
error[LNG0708]: the specification Acme.Linear is described differently:
gen/inventory/assurance.json: package acme, fingerprint 3c1e…
gen/acme/assurance.json: package acme, fingerprint 9b70…
A document lungo cannot read, or one of a schema version it does not read, is
LNG0711 (exit status 1).
Run outside a project (no --config or --project, and no lungo.toml in the current
directory), lungo assurance --compose only compares the documents it is given, and needs at
least two.
Compose against the project
Inside a project, the project’s own document, built from the Lean sources as they are now, is compared with each document given:
cd examples/semantic-model
lungo assurance --compose vendor/acme/assurance.json
The report of the project’s exports is printed as usual, and the composition result follows.
With --format json, mismatches are listed under composition in the report. --policy and
--compose can be combined: a policy violation exits with status 2 and takes precedence over a
composition mismatch (status 3).
Check it in CI
Compose the documents of every package you ship together, and fail on a non-zero status:
lungo generate --go_out=gen/inventory
lungo --config acme/lungo.toml generate --go_out=gen/acme
lungo assurance --compose gen/inventory/assurance.json --compose gen/acme/assurance.json
Both documents must come from the same Lean version: the version is part of every fingerprint, so documents built with different toolchains disagree on every record they share.
When the check fails, regenerate the packages from the same sources, then check the claims again. A changed specification means each claim against it has to be proved again, which building the dependent package does.