Contextfulv0.23.0

Docs / Specification

contract assurance · 80-formal.md · 81-engineering.md · 82-consumer.md · 83-gate.md · guide · card

The formal model

Two Lean 4 packages stand beside the engine: one specifying the policy core, and one holding an executable state machine of the store’s lease, compare-and-swap and fence protocol, its invariants stated as theorems. The nightly formal stage checks both, and one differential harness ties each model to the code it describes: the policy model to both builds of the decision module, the protocol model to the store’s two lease paths.

The two models, the checks over them, and where each meets the engine:

Flowchart diagram Flowchart, left to right. 14 nodes, 15 edges. specification text → decision models [Layer, Placement, Authority, Allowlist]; → protocol model [lease, compare-and-swap, fence] formal/inventory.toml → assumption audit [required constants] Lean packages: decision models → elaborated environment [lake build]; → reference binary [compiled] Lean packages: protocol model → bounded invariant check [3 nodes, 4 lease generations]; → assumption audit [invariant theorems]; → protocol executable [lean_exe] Lean packages: elaborated environment → assumption audit [assumption footprints] Lean packages: reference binary → differential harness [decisions] Lean packages: protocol executable → differential harness [protocol traces] Rust engine: native decision module → differential harness [decisions] Rust engine: WebAssembly decision module → differential harness [decisions] Rust engine: Rust storage layer → differential harness [protocol traces] gate: formal stage: assumption audit → audit report [row verdicts] gate: formal stage: differential harness gate: formal stage: bounded invariant check Lean packages lake build compiled lean_exe decision models protocol model elaborated environment reference binary protocol executable Rust engine native decision module WebAssembly decisionmodule Rust storage layer gate: formal stage assumption audit differential harness bounded invariant check Layer, Placement, Authority,Allowlist lease, compare-and-swap,fence required constants assumption footprints row verdicts decisions decisions decisions 3 nodes, 4 lease generations invariant theorems protocol traces protocol traces specification text formal/inventory.toml audit report

model

The Lean policy package and the Lean protocol state machine, their pins, and the definitions theorems and checks range over.

prove

The theorem inventory: layer composition, placement, the evidence floor, the proof targets over the authority mapping, and the mediation relation over statement execution.

audit-assumptions

The assumption allowlist, the transitive footprint audit over the elaborated environment, the inventory and the report.

  • assumptiontestAn assumption is a declaration the Lean kernel accepts without proof: the set #print axioms reports for a constant, which the audit reads through collectAxioms.
  • allowlisttestThe assumption allowlist holds 2 entries, propext and Quot.sound, and every theorem’s footprint is a subset of it.
    Whybecause no required constant draws on Classical.choice
  • transitive-audittestEach required constant’s assumption footprint is read transitively off the elaborated environment, naming every assumption reached.
  • verdict-inputtestA verdict is a function of the elaborated environment and the inventory alone; source text, declaration counts and the build’s exit status decide nothing.
    Whybecause elaboration reports a hole as a warning and exits zero, and a character pattern misses a hole spelled in parentheses
  • assumption-outside-allowlisttestAn assumption in a footprint and absent from the allowlist raises AssumptionOutsideAllowlist, printing the constant and the assumption.
    WhyA-assurance#assurance-claims-carry
  • hole-assumptiontestA footprint containing the hole assumption raises ProofHoleAssumption, naming the declaration, whatever its syntax spells.
    WhyA-assurance#assurance-claims-carry
  • native-evaluation-assumptiontestA footprint containing a per-declaration native-evaluation assumption raises NativeEvaluationAssumption, naming the declaration that minted it.
    WhyA-assurance#assurance-claims-carry
  • inventorytestformal/inventory.toml holds one row per required constant — name, module, expected statement text, admitted assumptions, binding, negative space — edited apart from the declarations satisfying it.
  • missing-constanttestA required constant absent from the elaborated environment raises TheoremConstantMissing.
    WhyA-assurance#assurance-claims-carry
  • statement-drifttestA required constant whose elaborated statement differs from its expected text raises TheoremStatementDrift, printing both.
    WhyA-assurance#assurance-claims-carry
  • inventory-changetestA change to a required statement lands in the commit carrying the proof it admits.
  • allowlist-admissiontestAn assumption joins the allowlist through an A-assurance section naming it, and each inventory row admitting it cites that section in a record field.
    WhyA-assurance#assurance-claims-carry
  • reporttestThe report names the commit, the resolved toolchain, the allowlist and inventory revision applied, and for each required constant its statement match and the assumptions it reaches.
  • check-commandtestcontextful formal check elaborates the package, matches every inventory row, audits every footprint, writes the report, and exits non-zero naming the first failing constant.

recheck

Rebuilding and re-auditing from pinned source in a credential-free environment.

  • two-phasetestA recheck rebuilds the package from the commit’s own source and pinned toolchain into an empty artifact directory, fetching nothing, and re-runs the audit against the rebuilt environment.
  • credential-freetestA recheck environment exposing a token, a signing key or a registry login raises RecheckEnvironmentCredentialed, naming the variable or file carrying it.
    WhyA-assurance#assurance-claims-carry
  • report-mismatchtestA recheck whose per-constant statement text or assumption set differs from the first phase’s raises RecheckReportMismatch, naming the constant.
    Whybecause .olean output is not byte-reproducible across hosts and paths, while the per-constant report is the fact under check
  • wall-timetestA recheck completes within 600 s.

scope-claim

The sentence the assurance claim is allowed to be: named decisions, named specifications and trusted dependencies.

unsettled: Which translator, external models and refinement scope does a claim name once a theorem reaches the Rust decision functions through translated code? owner: build affects: assurance.scope-claim

differential-test

The executable reference models, the case generators, the minimized counterexample corpus and the command running them.

Shapes

One inventory row:

[constant.composed_sound]
module    = "Contextful.Layer"
statement = "∀ {ls : List Layer} {r : RowId}, composed ls r = true → ∀ l ∈ ls, l r = true"
assumptions    = ["propext", "Quot.sound"]
binding   = "engine/policy/src/relation.rs::compose_layers"
negative  = """
Leaves open: that the required members were present in the list; that a member
performs removal rather than a test; that an execution reaches the fold ahead of
an effect.
"""