Theorem Inventory

The axiom

Two registries have to agree on what the Lean tree assumes. The manifest's allowed_axioms list is the approved set:

allowed_axioms = [
  # Symbolic collision resistance over the image of the mechanized canonical
  # UTF-8 renderer. This is the Lean idealization registered as ASSUME-SHA256.
  "Chio.Json.hash_collision_resistant",
]

The inventory carries the matching row in its assumptions array, which is separate from the theorems array the rest of this catalog draws on:

"assumptions": [
  {
    "id": "assume.hash.collision_resistant",
    "leanName": "Chio.Json.hash_collision_resistant",
    "file": "formal/lean4/Chio/Chio/Json/Hash.lean",
    "kind": "axiom",
    "rootImported": true,
    "claimClass": "symbolic_crypto",
    "status": "assumed",
    "mapsTo": ["P4", "P7"],
    "notes": "Symbolic hash collision resistance over the image of the mechanized canonical UTF-8 renderer. This is the sole explicit root-imported Lean axiom and is registered one-to-one as ASSUME-SHA256; concrete SHA-256 remains outside Lean."
  }
],

The declaration is axiom hash_collision_resistant : SymbolicHash at formal/lean4/Chio/Chio/Json/Hash.lean. SymbolicHash is a structure bundling an output type, a digest function over canonical bytes, and a proof that the digest is injective, so assuming an inhabitant of it is assuming collision resistance over the image of the mechanized canonical renderer. Concrete SHA-256 stays outside Lean, and the inventory registers the axiom one-to-one against ASSUME-SHA256 in formal/assumptions.toml.

scripts/check-formal-proofs.sh holds the two lists together in both directions. It rejects the tree when the inventory's assumption Lean names differ from allowed_axioms, and it elaborates the root module and rejects the tree again when the set of axioms the Lean environment reports differs from the same list. An axiom added to the source without an entry in both registries stops the gate.

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:

/-- 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) :
    ∀ g, g ∈ child.grants →
      ∃ pg, pg ∈ 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

Every inventory row whose file is Proofs/Receipt.lean, plus the field-coupling row in Proofs/Protocol.lean. The two collision-resistance rows here are theorems, discharged over the symbolic hash the axiom above supplies.

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, and none of them holds over an Aeneas extraction, a Kani harness, or a Creusot contract. The manifest states the standing of this lane directly: the treaty PredicateLang is a bounded post-validation abstraction over production-shaped federation inputs, and its Lean abstraction anchors are drift tripwires rather than a Rust refinement proof.

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

Six rows, one per named invariant in formal/tla/RevocationPropagation.tla. The five safety names are the leaves of the aggregate SafetyInv, which conjoins them with the domain invariant DomainsOK; RevocationEventuallySeen is the liveness property and is checked separately. The mapping file labels the third column Assumption discharge and defines it as which audited assumptions the property relies on, so nothing in it is a retirement.

No row in this table records a discharge. Every id in it sits in required_assumption_ids at formal/assumptions.toml, retired_assumption_ids and retired_assumptions there are both empty, and so is discharged_assumptions in formal/proof-manifest.toml. The registry states the bar an invariant would have to clear: retiring an assumption takes named model evidence and a concrete implementation-refinement gate over the affected production boundary, and abstract invariants and manual mirror hashes are not sufficient by themselves.

The scope of the SQLite entry is worth reading in the registry's own words, because it is narrower than the invariant above it suggests. ASSUME-SQLITE-ATOMICITY assumes atomic committed updates for revocation, budget, receipt and registry state per single-row write. Cross-row crash recovery, ordering and conservation are not assumed or discharged and remain outside the current formal claim boundary. The manifest says the same thing from the other side about the invariant that comes closest: ReceiptBeforeAllow proves the abstract persist-before-publish ordering and its production replay exercises the native happy path, and it does not discharge concrete cross-row crash recovery, which remains excluded until implementation trace validation and crash-reopen conservation gates establish refinement. See Assumptions and TCB for the registry in full.

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 MonotoneLogApalache, ReceiptBeforeAllow, RevocationCutCompleteness, KernelTransitionCancelSafe, and PostAdmissionDropGuard.

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 revocation-propagation invariants in detail.