Theorem Inventory

Every theorem reachable from formal/lean4/Chio/Chio.lean appears below, copied verbatim from formal/theorem-inventory.json. The inventory schema is chio.theorem-inventory.v1. Each row names the Lean identifier, the file it lives in, the claim class, and the property IDs from the proof manifest that it helps discharge.

Axioms

The inventory contains exactly one explicit axiom. It is the signature-verification predicate over the trusted-key set.

The axiom is the only allowed one. The proof manifest's allowed_axioms list contains exactly this entry. Any new axiom would have to be added there in the same PR or the gate fails.

Capability Algebra Theorems

The capability algebra is the heart of chio's attenuation story. P1 (capability monotonicity) is the headline property: a child capability can only be a subset of its parent, never wider.

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 fourteen rows spread across four files. The headline row is spec.capability_monotonicity; every other P1 row either supports it (subset transitivity, wildcard subsumption, budget tightening, added constraints) 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.

Aeneas Equivalence Theorems

These theorems live in Proofs/AeneasEquivalence.lean. Each one says: the Aeneas-extracted Lean mirror of a function in crates/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

Public Kani Harnesses

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

Status

Every theorem in the inventory above is rootImported: true. That means each one is reachable from the canonical 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.