assurance.json

Every output lungo writes — the Rust module, each language’s package, each plugin’s output — carries the program’s assurance document as assurance.json: what its Lean code claims and proves of each export, the assumptions those claims rest on, the facilities each export needs, and what each export trusts. The document is built once per program and written byte for byte the same into every output; each language reads the same text (see in each language). Formal assurance explains the concepts.

The document is pretty-printed JSON (two-space indentation) ending with a newline. A field whose value is absent is null, never omitted. Every lungo reader — Rust, Go, Python, Swift and TypeScript — refuses a document of another schema_version, one with a field it does not know, and one missing a field (a nullable one included: it must be present as null), at any depth.

Top level

A program that uses none of the library has library: null and empty record arrays; its exports are still listed, with their trust.

Provenance

Records

Every record of the four kinds below carries:

Specifications

@[lungo_spec] declarations: name, kind (such as lungo.contract or acme.cost-model), statement (the declaration’s type, as Lean prints it), definition (its body, as Lean prints it, when the declaration is a definition; otherwise null), and the common fields.

Facilities

@[lungo_facility] declarations.

Assumptions

@[lungo_assumption] declarations: name, facility (the facility’s Lean name), statement (the declaration’s type, as Lean prints it), definition (its body when it is a definition, otherwise null), and the common fields. An assumption defined as a proposition has the type Prop, so its definition is what it says: lungo assurance and lungo inspect print the definition when there is one, the type otherwise.

Claims

@[lungo_claim] theorems. A claim’s name is its evidence theorem’s.

Roles

@[lungo_role] declarations: name, role (such as lungo.oracle), and exported (whether the program exports the declaration). Roles carry no fingerprint or source.

Exports

One per exported declaration.

Order and determinism

The document is a function of the compiled project and the toolchain: generating it twice, or from another directory, gives the same bytes, and it holds no path of the machine.

• specifications, facilities, assumptions, claims, roles and exports are sorted by name, comparing the names’ bytes (so Polyglot.Scaler comes before Polyglot.fetchInterface).
• The operations of an extern facility are sorted by name; those of an async facility are in the operation type’s constructor order.
• A claim’s assumptions, its evidence’s axioms, a facility’s assumptions, and an export’s assumptions and facilities are sorted. A claim’s subjects and specifications keep the attribute’s order; an export’s claims follow the order of claims.

Fingerprints

A fingerprint identifies what a record means, so two documents can be checked to agree on a name they share (lungo assurance --compose, LNG0708). It covers the record’s own Lean expressions and, transitively, the definitions of every constant they use that a package of the Lake workspace declares; the toolchain’s constants (Lean’s Init, Std, Lean) are covered by the Lean version, which every fingerprint names.

The worker writes a canonical text of each expression: its distinct subterms once each, in post order, without binder names or metadata, with universe parameters numbered by position, constants by name, after a header naming the record kind. A record’s canonical text covers:

The worker also describes, once each, every workspace constant the records use, directly or through another such constant: a definition by its type and value; a theorem, an opaque constant or an axiom by its type (a proof’s or an opaque implementation’s content does not change what it states); an inductive type by its type and its constructors’; each with the workspace constants it uses in turn. lungo digests these definitions over that graph, so a definition’s digest changes when anything it uses changes. Definitions that use each other (a strongly connected component of the graph, such as mutually recursive functions) are digested together:

component = SHA-256( "lungo-assurance-1 definitions\nlean <lean_version>\n"
                     + for each member, by name: "member <name>\n<canonical text>\n"
                       + for each constant it uses outside the component, by name:
                         "uses <name> <digest>\n" )
digest(member) = SHA-256( component + "\n" + <name> )

A record’s fingerprint is then:

SHA-256( "lungo-assurance-1\nlean <lean_version>\n" + <canonical text>
         + for each workspace constant the record uses directly, by name:
           "\nuses <name> <digest>" )

Each is written as 64 lowercase hexadecimal digits. Renaming a binder or reformatting does not change a fingerprint, nor does the record’s own name or source position. Changing the statement, the definition, any definition of the workspace it reaches — such as a helper a specification unfolds to — or the Lean version does. A claim names its subjects as constants, so its fingerprint also changes when a subject’s definition does.

In each language

A plugin receives the document in its request (assurance) and must not write assurance.json itself: lungo writes it into every output (plugins).

lungo assurance reports the document of a project, filtered and checked against the policy, and lungo assurance --compose composes documents (the lungo command).