Lean 4 Proofs

The proof tree lives under formal/lean4/Chio/. The proof manifest declares 37 root modules, the theorem inventory records 165 entries across 24 of those files, and the gate refuses to pass unless every inventory entry elaborates, every one of them is reachable by import from the root, and the set of axioms in the elaborated environment is exactly the one the manifest allows.

leanprover/lean4:v4.28.0

Why Lean 4

• Tactic-based proofs. Most Chio theorems decompose under unfold plus structural induction. The tactic syntax stays close to the proof outline a reviewer would write by hand.
• Mathlib for general math. Order-theoretic lemmas, list and set utilities, and arithmetic combinators are mature.
• Property-proof support. Definitional unfolding, type-class inference, and elaboration let property statements track executable Rust closely.

Project layout

formal/lean4/Chio/ holds Chio.lean (the root module that imports everything), lakefile.lean, lean-toolchain, the Chio/ namespace tree in eight directories, and the two Aeneas output trees whose headers name their generator, FormalAeneas/ and FormalEconomy/.

The manifest's root_modules array is the list the gate consumes. Every entry below is under formal/lean4/Chio/ and every one of them must elaborate:

root_modules = [
  "formal/lean4/Chio/Chio.lean",
  "formal/lean4/Chio/Chio/Json/Value.lean",
  "formal/lean4/Chio/Chio/Json/Canonical.lean",
  "formal/lean4/Chio/Chio/Json/Hash.lean",
  "formal/lean4/Chio/Chio/Json/Fixtures.lean",
  "formal/lean4/Chio/Chio/Core/Capability.lean",
  "formal/lean4/Chio/Chio/Core/Scope.lean",
  "formal/lean4/Chio/Chio/Core/Receipt.lean",
  "formal/lean4/Chio/Chio/Core/MerkleWalk.lean",
  "formal/lean4/Chio/Chio/Core/Revocation.lean",
  "formal/lean4/Chio/Chio/Core/Protocol.lean",
  "formal/lean4/Chio/Chio/Economy/Conversion.lean",
  "formal/lean4/Chio/Chio/Spec/Properties.lean",
  "formal/lean4/Chio/Chio/Proofs/Monotonicity.lean",
  "formal/lean4/Chio/Chio/Proofs/CanonicalInjective.lean",
  "formal/lean4/Chio/Chio/Proofs/Receipt.lean",
  "formal/lean4/Chio/Chio/Proofs/MerkleWalk.lean",
  "formal/lean4/Chio/Chio/Proofs/Revocation.lean",
  "formal/lean4/Chio/Chio/Proofs/Evaluation.lean",
  "formal/lean4/Chio/Chio/Proofs/Protocol.lean",
  "formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean",
  "formal/lean4/Chio/Chio/Proofs/AeneasGeneratedEquivalence.lean",
  "formal/lean4/Chio/Chio/Proofs/FormalClosure.lean",
  "formal/lean4/Chio/Chio/Proofs/AttenuationWitness.lean",
  "formal/lean4/Chio/Chio/Proofs/HandshakeNegotiation.lean",
  "formal/lean4/Chio/Chio/Proofs/SiblingSumBudget.lean",
  "formal/lean4/Chio/Chio/Proofs/ReservationLedger.lean",
  "formal/lean4/Chio/Chio/Guards/WasmBoundary.lean",
  "formal/lean4/Chio/Chio/Proofs/DeliveryContract.lean",
  "formal/lean4/Chio/Chio/Proofs/FindingStatusFreshness.lean",
  "formal/lean4/Chio/Chio/Capability/Delegation.lean",
  "formal/lean4/Chio/Chio/Treaty/Intersection.lean",
  "formal/lean4/Chio/Chio/Treaty/PredicateLang.lean",
  "formal/lean4/Chio/Chio/Treaty/IntersectionSyntactic.lean",
  "formal/lean4/Chio/Chio/Treaty/IntersectionLegacy.lean",
  "formal/lean4/Chio/Chio/Treaty/BridgeEquivalence.lean",
  "formal/lean4/Chio/Chio/Treaty/BilateralAccept.lean",
]

37 entries. Exactly one .lean file under formal/lean4/Chio/Chio/ is absent from that array, Treaty/ReceiptPredicate.lean, and it carries no inventory entry either.

Theorems are not confined to the Core, Spec, and Proofs lanes: 6 of the 24 files carrying inventory entries sit outside them, against 18 inside. Chio/Capability/Delegation.lean is a further case. It holds delegate_no_widen, attenuation_monotone, revocation_is_cut, and compose_preserves_algebra, each with a row in formal/MAPPING.md:356-359 naming the Rust it constrains, and none of the four has an entry in formal/theorem-inventory.json. The runtime form of the first is the Kani harness verify_delegate_no_widen (formal/MAPPING.md:314).

The one axiom

The manifest's allowed_axioms array has a single entry, and the gate requires the set of axiom-kind declarations in the elaborated Lean environment to equal it exactly:

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",
]

That axiom lives in formal/lean4/Chio/Chio/Json/Hash.lean and postulates a structure, not a proposition: a hash output type, a digest function on canonical bytes, and injectivity of that function.

structure SymbolicHash where
  Output : Type
  digest : CanonicalBytes → Output
  injective : ∀ left right, digest left = digest right → left = right

axiom hash_collision_resistant : SymbolicHash

The rest of the file builds on it: HashVal abbreviates hash_collision_resistant.Output and digest applies the postulated function to the canonical bytes of a JSON value. Every symbolic-crypto theorem in the tree bottoms out here. The manifest comment registers the axiom one-to-one as ASSUME-SHA256, and formal/proof-manifest.toml:247 restates the boundary for the Merkle walk in the same words: hash collision resistance remains ASSUME-SHA256.

P1: capability monotonicity

The theorem and its three tactics

P1 says a child capability's bounds are tighter than its parent's. Lean states it over the ChioScope model: if a child scope is a subset of a parent scope, every grant in the child is covered by some grant in the parent. The theorem is Chio.Spec.capability_monotonicity, inventory id spec.capability_monotonicity:

/-- 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)

The proof is three tactics. intro g h_mem introduces an arbitrary grant g from the child and a hypothesis that it is in the child's grant list. unfold ChioScope.isSubsetOf at h rewrites the subset hypothesis into its List.all and List.any form. The final line composes two standard list lemmas: List.all_eq_true.mp h g h_mem extracts the per-grant statement that parent.grants.any (fun p => g.isSubsetOf p) holds, and List.any_eq_true.mp unpacks that into a witness grant pg in parent.grants with g.isSubsetOf pg = true.

This theorem is about the Lean model. It does not by itself say anything about the Rust; the Aeneas equivalence theorems and the Kani harnesses are what reach the executable code.

The definitions it unfolds

Scope subset is a per-grant existence check:

/-- Mirrors: ChioScope::is_subset_of in crates/core/chio-core-types/src/capability/scope.rs.

    Returns true if every grant in `child` is covered by some grant in `parent`. -/
def ChioScope.isSubsetOf (child parent : ChioScope) : Bool :=
  child.grants.all (fun cg =>
    parent.grants.any (fun pg => cg.isSubsetOf pg))

Grant subset is the conjunction of five attenuation rules: same server, wildcard-or-equal tool name, operations subset, budget tightening, and constraint superset.

def ToolGrant.isSubsetOf (child parent : ToolGrant) : Bool :=
  -- Same server
  child.serverId == parent.serverId
  -- Tool name match (wildcard or exact)
  && (parent.toolName == "*" || child.toolName == parent.toolName)
  -- Operations subset
  && child.operations.isSubsetOf parent.operations
  -- Invocation budget
  && (match parent.maxInvocations with
      | none => true  -- parent uncapped, any child is fine
      | some parentMax =>
        match child.maxInvocations with
        | none => false  -- child uncapped but parent is capped
        | some childMax => childMax ≤ parentMax)
  -- Constraints: parent's constraints must all appear in child
  && parent.constraints.isSubsetOf child.constraints

The types themselves are in Chio/Core/Capability.lean:

/-- Mirrors: ToolGrant in crates/core/chio-core-types/src/capability/scope.rs. -/
structure ToolGrant where
  serverId : ServerId
  toolName : ToolName
  operations : List Operation
  constraints : List Constraint
  maxInvocations : Option Nat
  deriving Repr, BEq, ReflBEq, LawfulBEq

The in-source Mirrors: docstrings name the Rust file by full path, so the Lean model and its Rust counterpart can be opened side by side without guessing: crates/core/chio-core-types/src/capability/scope.rs holds ChioScope, ToolGrant, and their is_subset_of implementations. A docstring is a comment, not a checked link; cargo xtask check formal-mirrors is the gate that compares normalized token hashes between the two sides, and formal/proof-manifest.toml:246 records that matching hashes do not prove semantic equivalence.

5 supporting P1 lemmas live in Chio/Proofs/Monotonicity.lean: list_isSubsetOf_trans (subset transitivity over bounded lists), scope_subset_of_grants_subset (grant-wise subset to scope subset), wildcard_subsumes, reduced_budget_is_subset, and added_constraint_is_subset. The sixth entry in that file, delegation_chain_integrity, maps to P5 instead. Reflexivity and the empty-scope case are theorems in Core/Scope.lean itself. The P1 statement needs no Mathlib import; the wider tree imports Mathlib for arithmetic and ordering lemmas elsewhere.

Continue at Aeneas Pipeline: P1 extraction equivalence or jump back to the P1 Tour.

Evaluation theorems

Proofs/Evaluation.lean carries 8 theorems, all claim class bounded_model and all mapping to P3. They establish totality and the denial paths over the bounded evaluator, not over the Rust runtime.

• evalToolCall_total · the evaluator returns either allow or deny in the bounded model.
• evalToolCall_invalid_signature_denies
• evalToolCall_not_yet_valid_denies · a capability before its validity window denies.
• evalToolCall_expired_denies · a capability past its expiry denies.
• evalToolCall_revoked_token_never_allows · also maps to P2.
• evalToolCall_revoked_ancestor_never_allows · also maps to P2.
• evalToolCall_out_of_scope_denies
• evalToolCall_all_checks_pass_allow · the matching positive theorem.

The two revocation theorems in this file are two of the four ids formal/MAPPING.md:92-99 cross-references to the TLA+ invariant NoAllowAfterRevoke; the other two are the snapshot theorems in Proofs/Protocol.lean (see TLA+ Specs).

Revocation theorems

Proofs/Revocation.lean carries 5 theorems, all mapping to P2:

• revoke_marks_capability_revoked · the revoke operation marks the target capability id as revoked in the bounded store.
• revoke_preserves_existing_revocation · adding a revocation does not clear prior revoked ids.
• checkRevocation_revoked_token_errors
• checkRevocation_revoked_ancestor_never_ok
• checkRevocation_ok_implies_not_revoked · a successful revocation check implies neither the token nor any presented ancestor is revoked.

The complementary protocol-layer theorems are in Proofs/Protocol.lean: revocationSnapshot_revoked_token_denies and revocationSnapshot_revoked_ancestor_denies. These work on a projected snapshot, the shape that sits between the kernel and the bounded model.

Receipt theorems

Proofs/Receipt.lean carries 8 theorems, every one with claim class symbolic_crypto. They are over a symbolic Merkle, sign, and verify model, not over Ed25519 or SHA-256 implementations.

• receipt_id_input_collision_resistant · status proved, maps to P4 and P7.
• receipt_id_collision_resistant · status proved, maps to P4 and P7. This is the theorem the axiom callout above distinguishes from Chio.Json.hash_collision_resistant.
• applyProof_append · symbolic Merkle proof composition.
• membership_proof_sound · Merkle inclusion soundness.
• membership_proof_verifies · the executable verification theorem.
• checkpoint_consistency · checkpoint consistency over the bounded checkpoint store.
• receipt_sign_then_verify · over the symbolic sign and verify model, not Ed25519.
• receipt_immutability · the tampering theorem under the symbolic model.

receiptFieldsCoupled_preserves_all_fields in Proofs/Protocol.lean is the bounded-model coupling theorem that says a coupled receipt body preserves capability, request, verdict, policy hash, and evidence class.

Protocol and closure

Proofs/Protocol.lean carries more inventory entries than any other file in the tree, 26 of them. With Proofs/FormalClosure.lean it covers guard pipeline composition, DPoP nonce admission and binding, budget commits, governed approvals, session continuity, lineage soundness, registry behavior, path-prefix safety, and report truthfulness.

Two patterns recur:

• Deny dominates. guardPipeline_deny_dominates and guardPipeline_error_dominates establish that any single guard's deny or error verdict forces the pipeline to deny. The matching positive theorem, guardPipeline_allow_requires_core_authorized, says the pipeline can only allow if core authorization already passed.
• No upgrade. The report truthfulness theorems say that report or export surfaces cannot relabel asserted or observed lineage as verified.

Proofs/FormalClosure.lean carries 8 entries. Five of them are the semantic delegation-step theorems behind P5:

• delegation_step_allow_requires_attenuation
• delegation_step_allow_requires_subject_continuity
• delegation_step_allow_requires_expiry_monotonicity
• delegation_revoked_ancestor_denies
• delegation_max_depth_failure_denies · also maps to P3.

The other three in the same file are dpop_binding_allows_only_when_all_fields_match (P8), path_prefix_rejects_sibling_prefix and path_prefix_rejects_normalized_traversal_escape (both P3).

Reproduce

With elan installed, the build is one command from the project root:

cd formal/lean4/Chio
lake build

On first run lake reads the toolchain pin and downloads the matching Lean. Subsequent runs use the cache. That command elaborates and type-checks the tree, and nothing more. The gate around it is ./scripts/check-formal-proofs.sh, which runs six steps in order:

• Canonical JSON fixture drift, via scripts/generate-lean-json-fixtures.py --check (check-formal-proofs.sh:8-9).
• lake build itself, which fails the script if lake is not on PATH (:11-20).
• A literal sorry scan over every shipped .lean file. One hit fails the build (:22-41).
• The elaborated assumption-audit regression suite (:43-44).
• Manifest and inventory agreement: the inventory's assumption entries must match allowed_axioms name for name (:185-189), every assumption entry must be marked kind: axiom and rootImported (:383-386), and every theorem entry must be rootImported (:430-431).
• The environment axiom check: the set of axiom-kind declarations Lean actually elaborated must equal allowed_axioms, and the script reports both directions of the difference (:344-353). A separate check refuses an abbrev that shadows an approved axiom name (:468-498).

No captured output accompanies these commands here: the build needs a Lean toolchain download and the gate needs the elaborated environment alongside it.

Where Lean corresponds to Rust

formal/MAPPING.md is the cross-reference. Each named Kani harness and TLA+ invariant has a row pointing at the Rust call site it constrains, and the Lean theorems appear in the informational cross-reference section beneath the TLA+ table.

For example, the Kani harness verify_delegation_chain_step points at chio_kernel_core::formal_core::optional_u32_cap_is_subset, monetary_cap_is_subset_by_parts, required_true_is_preserved, and time_window_valid. The Lean delegation-step theorems in FormalClosure.lean are the proof-side mirror.

Next

• Theorem Inventory · the full table of 165 entries.
• Aeneas Pipeline · the Rust-to-Lean equivalence theorems.
• Kani Harnesses · the bounded model-checking lane on production Rust.