Theorem Inventory

Axioms

The inventory contains one explicit axiom. It assumes receipt content-addressing: distinct canonical receipt-ID inputs do not collide.

It is a Lean axiom because the bounded receipt model treats the receipt ID as an opaque string with no modeled canonicalizer or hash; mechanizing injectivity would require a Lean model of the JCS serializer, a model of the hash, and a collision-resistance assumption on that hash (ASSUME-SHA256). The proof manifest's allowed_axioms list contains this entry, and any new axiom must be added there in the same PR or the gate fails.

Capability Algebra Theorems

P1 (capability monotonicity) proves, over the bounded capability algebra model, that a child capability is a subset of its parent.

The headline theorem statement is short. Verbatim from Spec/Properties.lean:

/-- P1: Capability monotonicity -- if a child scope is a subset of a parent
    scope, then every grant in the child is covered by some grant in the
    parent.

    This is the core Chio safety property: delegation can only attenuate,
    never amplify. -/
theorem capability_monotonicity (parent child : ChioScope)
    (h : child.isSubsetOf parent = true) :
    forall g, g in child.grants ->
      exists pg, pg in parent.grants /\ g.isSubsetOf pg = true := by
  intro g h_mem
  unfold ChioScope.isSubsetOf at h
  exact List.any_eq_true.mp (List.all_eq_true.mp h g h_mem)

P1: capability_monotonicity in this catalog

P1 says a child capability's bounds are tighter than its parent's; delegation attenuates and never amplifies. This catalog records P1 in thirteen rows spread across six files. The headline row is spec.capability_monotonicity; every other P1 row either supports it (subset transitivity, wildcard subsumption, budget tightening, added constraints, the attenuation witness, the sibling-sum budget law) or pins a corner case (empty scope, reflexivity, non-negative budgets). Verbatim from formal/theorem-inventory.json:

{
  "id": "spec.capability_monotonicity",
  "leanName": "Chio.Spec.capability_monotonicity",
  "file": "formal/lean4/Chio/Chio/Spec/Properties.lean",
  "kind": "theorem",
  "rootImported": true,
  "claimClass": "bounded_model",
  "mapsTo": ["P1"],
  "notes": "Primary attenuation theorem over ChioScope grants only; no Rust refinement proof yet."
}

Field by field:

• id · stable inventory ID. The gate scripts/check-formal-proofs.sh fails if any ID is renamed without an accompanying entry change.
• leanName · the fully qualified Lean identifier. The gate elaborates the root module and asserts this name resolves.
• file · path relative to the repo root. P1 sits under Spec/ rather than Proofs/ because the theorem statement is the Chio spec, not a derived helper.
• rootImported · true means the gate checks the import graph closure from Chio.lean reaches this file. A theorem that elaborates but is not root-imported fails the gate.
• claimClass · bounded_model. The theorem reasons about the Lean ChioScope definition, not the Rust binary. The Aeneas equivalence theorem aeneas_optionalCapIsSubset_preserves_parent_cap (also tagged P1) is what ties the bounded model to the executable code.
• mapsTo · the property IDs from the proof manifest this row helps discharge. P1 is the only one here.

Continue the tour at Lean 4 Proofs: P1 the canonical proof or jump back to the P1 Tour.

Revocation Theorems

Revocation surfaces in two places: the bounded revocation-store model, and the projected snapshot used by the evaluator.

Evaluation Theorems

The bounded evaluator covers signature, time, scope, and revocation checks. P3 is the master fail-closed property.

Receipt Theorems

Receipt theorems live across two files. The Merkle and signing theorems are in Proofs/Receipt.lean; the field-coupling theorem is in Proofs/Protocol.lean.

Protocol-Layer Theorems

Theorems in Proofs/Protocol.lean and Proofs/FormalClosure.lean cover guard-pipeline composition, DPoP nonce admission, budget commits, governed approvals, session continuity, lineage soundness, registry behavior, path-prefix safety, and report truthfulness.

Treaty and Bilateral Accept Theorems

The Treaty lane covers cross-organization governance: bilateral treaty admission, constitutional amendment refinement, syntactic predicate-chain preservation, and the bilateral DSSE accept set. These theorems live in Treaty/Intersection.lean, Treaty/PredicateLang.lean, and Treaty/BilateralAccept.lean, all imported from Chio.lean. The explanation of the systems modeled by these theorems is in Papers; this table is the catalog entry, copied verbatim from formal/theorem-inventory.json.

All nine rows are rootImported: true with status proved, claim class bounded_model: each holds over the bounded Lean treaty and predicate-language models described above, not yet over an Aeneas extraction or a Kani harness. No Treaty theorem currently has an Aeneas equivalence proof, a Kani harness, or a Creusot contract. Those implementation links are currently absent.

Aeneas Equivalence Theorems

These theorems live in Proofs/AeneasEquivalence.lean. Each one says: the Aeneas-extracted Lean mirror of a function in crates/kernel/chio-kernel-core/src/formal_aeneas.rs is equivalent to the handwritten model the rest of the proofs depend on. The class is aeneas_equivalence.

Proof-to-Rust Mapping

formal/MAPPING.md is the cross-reference from named TLA+ invariants and Kani harnesses to the Rust call sites they constrain. The script scripts/check-mapping.sh greps the source for each name and fails the build if any appear in source but not in the mapping.

TLA+ Invariants

Two more Apalache specs sit alongside RevocationPropagation.tla. formal/tla/DelegationDepthBound.tla carries three named safety invariants ( DepthBoundedByRoot, AttenuatedAtEachStep, and RevokedSubtreeNotObservable ) and the kernel-state-subset lane under formal/apalache/ adds four more: MonotoneLogApalache, ReceiptBeforeAllow (the named evidence for RETIRED-SQLITE-CROSS-ROW), RevocationCutCompleteness, and KernelTransitionCancelSafe.

Public Kani Harnesses

Source: crates/kernel/chio-kernel-core/src/kani_public_harnesses.rs. The mapping script extracts function names following a #[kani::proof] attribute and checks that each appears in the table below.

Status

Each theorem in the inventory above is rootImported: true. That means it is reachable from the root module formal/lean4/Chio/Chio.lean and the Lean kernel has type-checked it without sorry placeholders. The gate scripts/check-formal-proofs.sh rejects any theorem that drops out of the root import graph or that introduces a sorry.

Next

• Aeneas Pipeline · how the equivalence theorems are produced and checked.
• Lean 4 Proofs · per-file structure of the proofs in this inventory.
• Kani Harnesses · full per-harness inventory with wall clocks.
• TLA+ Specs · the four named invariants in detail.