Lean 4 Proofs

Why Lean 4

Chio uses Lean 4 for the following properties.

• Tactic-based proofs. Most chio theorems decompose cleanly 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

The project is laid out under formal/lean4/Chio/ with a single namespace tree:

formal/lean4/Chio/
  Chio.lean                       # root module: imports everything
  lakefile.lean                   # lake configuration
  lean-toolchain                  # leanprover/lean4:v4.28.0-rc1
  Chio/
    Core/
      Capability.lean             # capability tokens, scopes, grants
      Scope.lean                  # ChioScope and ToolGrant subset algebra
      Receipt.lean                # symbolic receipt + Merkle model
      Revocation.lean             # bounded revocation-store model
      Protocol.lean               # protocol state and admission
    Spec/
      Properties.lean             # P1 capability_monotonicity and friends
    Proofs/
      Monotonicity.lean           # P1 attenuation theorems
      Receipt.lean                # P4 receipt theorems (symbolic crypto)
      Revocation.lean             # P2 revocation theorems
      Evaluation.lean             # P3 evaluator totality and denial paths
      Protocol.lean               # P3, P4, P6, P7, P8, P9, P10 protocol theorems
      AeneasEquivalence.lean      # 7 Aeneas-extracted equivalence theorems
      FormalClosure.lean          # P5 delegation, DPoP binding, path-prefix
      AttenuationWitness.lean     # P1 attenuation-witness soundness
      HandshakeNegotiation.lean   # P3 handshake negotiation safety
      SiblingSumBudget.lean       # P1 sibling-sum budget law
    Capability/
      Delegation.lean             # recursive-delegation theorems
    Treaty/
      Intersection.lean           # bilateral treaty predicate intersection
      PredicateLang.lean          # treaty predicate language
      BilateralAccept.lean        # bilateral federation accept sets

The proof manifest lists the root modules consumed by the gate:

root_modules = [
  "formal/lean4/Chio/Chio.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/Revocation.lean",
  "formal/lean4/Chio/Chio/Core/Protocol.lean",
  "formal/lean4/Chio/Chio/Spec/Properties.lean",
  "formal/lean4/Chio/Chio/Proofs/Monotonicity.lean",
  "formal/lean4/Chio/Chio/Proofs/Receipt.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/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/Capability/Delegation.lean",
  "formal/lean4/Chio/Chio/Treaty/Intersection.lean",
  "formal/lean4/Chio/Chio/Treaty/PredicateLang.lean",
  "formal/lean4/Chio/Chio/Treaty/BilateralAccept.lean",
]

Beyond the Core, Spec, and Proofs lanes, four more root modules carry theorems. Chio/Capability/Delegation.lean holds the recursive-delegation theorems delegate_no_widen, attenuation_monotone, revocation_is_cut, and compose_preserves_algebra, each cross-referenced in formal/MAPPING.md to the Kani harness verify_delegate_no_widen and the Rust symbols chio_core_types::capability::delegate and validate_delegation_chain. Chio/Proofs/AttenuationWitness.lean and Chio/Proofs/SiblingSumBudget.lean add two more P1 theorems (attenuation-witness soundness and the sibling-sum budget law), and Chio/Proofs/HandshakeNegotiation.lean adds a P3 handshake-negotiation safety theorem. The treaty lane ( Chio/Treaty/Intersection.lean, Chio/Treaty/PredicateLang.lean, and Chio/Treaty/BilateralAccept.lean ) models the bilateral-federation treaty predicates behind the governance surface.

P1: Capability Monotonicity

The P1 theorem is Chio.Spec.capability_monotonicity in Spec/Properties.lean. It proves capability attenuation over the ChioScope model: if a child scope is a subset of a parent scope, each child grant is covered by a parent grant. It does not by itself prove the Rust implementation; the Aeneas and Kani checks cover related Rust paths.

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

The proof structure: unfold the definition of subset, then apply the elimination lemmas for List.all and List.any to recover a witness grant in the parent. The full proof, including the recursive descent into grant fields, lives in supporting lemmas in Proofs/Monotonicity.lean:

• list_isSubsetOf_trans · subset transitivity over bounded lists.
• scope_subset_of_grants_subset · bridges grant-wise subset assumptions into ChioScope subset truth.
• wildcard_subsumes · wildcard tool-name matching coverage.
• reduced_budget_is_subset · budget-tightening is attenuation.
• added_constraint_is_subset · adding a constraint makes a grant strictly more restrictive.

The Rust implementation that this theorem mirrors lives at crates/core/chio-core-types/src/capability.rs in ChioScope::is_subset_of and crates/kernel/chio-kernel-core/src/normalized.rs in NormalizedScope::is_subset_of. The TLA+ AttenuationPreserving invariant (see TLA+ Specs) and the Kani verify_scope_intersection_associative and verify_delegation_chain_step harnesses constrain the same Rust path.

Evaluation Theorems

Proofs/Evaluation.lean proves evaluator totality and the listed denial paths over the bounded evaluator model. Eight theorems establish P3 for that model; they do not establish totality for the complete Rust runtime.

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

These theorems have claimClass: bounded_model. They reason about the Lean evaluator function, not the Rust one. The Aeneas equivalence theorems plus the Kani public harnesses bridge the bounded model to the executable code.

Revocation Theorems

Proofs/Revocation.lean contains the bounded revocation-store theorems for 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 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 six theorems with claimClass: symbolic_crypto. They are over a symbolic Merkle/sign/verify model, not over Ed25519 or SHA-256 implementations.

• applyProof_append · symbolic Merkle proof composition.
• membership_proof_sound · Merkle inclusion soundness.
• membership_proof_verifies · executable verification theorem.
• checkpoint_consistency · checkpoint consistency over the bounded checkpoint store.
• receipt_sign_then_verify · over the symbolic sign/verify model, not Ed25519.
• receipt_immutability · 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 and Proofs/FormalClosure.lean cover the rest: 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.

The closure file Proofs/FormalClosure.lean proves the semantic delegation-step theorems that make P5 hold:

• 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

P1: capability_monotonicity in this tool

P1 says a child capability's bounds are tighter than its parent's. Lean 4 contains the statement: if a child ChioScope is a subset of a parent, every grant in the child is covered by some grant in the parent. Verbatim from formal/lean4/Chio/Chio/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)

The proof is three tactics. intro g h_mem introduces an arbitrary grant g from the child and a hypothesis that it's in the child's grant list. unfold ChioScope.isSubsetOf at h rewrites the subset hypothesis into its List.all / 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 with pg in parent.grants and g.isSubsetOf pg = true.

The supporting definitions are in Chio/Core/Scope.lean. The scope subset is a per-grant existence check:

/-- Mirrors: ChioScope::is_subset_of in capability.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))

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

/-- Mirrors: ToolGrant::is_subset_of in capability.rs.

    A child grant is a subset when:
    - It targets the same server.
    - Parent tool is "*" (wildcard) or matches child tool.
    - Child operations are a subset of parent operations.
    - If parent has an invocation cap, child must too and child <= parent.
    - Every parent constraint appears in child (child is more restrictive). -/
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 capability and grant types are defined in Chio/Core/Capability.lean:

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

/-- Mirrors: ChioScope in capability.rs -/
structure ChioScope where
  grants : List ToolGrant
  deriving Repr, BEq, ReflBEq, LawfulBEq

The in-source Mirrors: comments name the Rust file by basename (capability.rs). They predate the crate-directory reorganization; the file they point at now lives at crates/core/chio-core-types/src/capability.rs.

Five supporting bound-comparison lemmas live in Chio/Proofs/Monotonicity.lean and discharge the structural pieces P1 leans on under the hood. Reflexivity is in Core/Scope.lean:

/-- Empty scope is a subset of any scope. -/
theorem ChioScope.empty_isSubsetOf (parent : ChioScope) :
    ChioScope.isSubsetOf ChioScope.empty parent = true := by
  unfold ChioScope.isSubsetOf ChioScope.empty
  simp [List.all]

/-- Reflexivity: a scope is a subset of itself. -/
theorem ToolGrant.isSubsetOf_refl (g : ToolGrant) :
    g.isSubsetOf g = true := by
  cases g with
  | mk serverId toolName operations constraints maxInvocations =>
    unfold ToolGrant.isSubsetOf
    simp [List.isSubsetOf]
    cases maxInvocations with
    | none => simp
    | some n => simp

Transitivity over the subset relation, the bridge from grant-wise subset truth to scope subset truth, and the wildcard/budget/constraint attenuation lemmas are all in Chio/Proofs/Monotonicity.lean: list_isSubsetOf_trans, scope_subset_of_grants_subset, wildcard_subsumes, reduced_budget_is_subset, and added_constraint_is_subset. The proofs rely on Lean's standard list combinators (List.all, List.any, List.isSubsetOf as defined locally in Core/Scope.lean) plus beq_iff_eq from the standardLawfulBEq support; no Mathlib import is needed for the P1 statement. The wider proof base imports Mathlib for arithmetic and ordering lemmas elsewhere.

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

Reproducing

With Lean and elan installed, the Lean check is one command:

cd formal/lean4/Chio
lake build

info: leanprover/lean4:v4.28.0-rc1: trusting cached toolchain
Build completed successfully.
  Chio.Core.Capability                 OK
  Chio.Core.Scope                      OK
  Chio.Core.Receipt                    OK
  Chio.Core.Revocation                 OK
  Chio.Core.Protocol                   OK
  Chio.Spec.Properties                 OK
  Chio.Proofs.Monotonicity             OK
  Chio.Proofs.Receipt                  OK
  Chio.Proofs.Revocation               OK
  Chio.Proofs.Evaluation               OK
  Chio.Proofs.Protocol                 OK
  Chio.Proofs.AeneasEquivalence        OK
  Chio.Proofs.FormalClosure            OK
  Chio.Proofs.AttenuationWitness       OK
  Chio.Proofs.HandshakeNegotiation     OK
  Chio.Proofs.SiblingSumBudget         OK
  Chio.Capability.Delegation           OK
  Chio.Treaty.Intersection             OK
  Chio.Treaty.PredicateLang            OK
  Chio.Treaty.BilateralAccept          OK

On first run, lake reads the toolchain pin and downloads leanprover/lean4:v4.28.0-rc1. Subsequent runs use the cache. The build elaborates and type-checks the theorems in the inventory.

The CI gate ./scripts/check-formal-proofs.sh wraps this with three additional checks:

• Each theorem in theorem-inventory.json must exist in the elaborated environment.
• Each theorem must have rootImported: true via import-graph closure from Chio.lean.
• The set of declared axioms must equal allowed_axioms in the manifest. The current set has one entry, Chio.Proofs.receipt_id_collision_resistant.

Where Lean Output 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. The Lean theorems are listed in the informational cross-reference section beneath the TLA+ table.

For example, the Kani harness verify_delegation_chain_step points to 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 theorems in the inventory.
• Aeneas Pipeline · the Rust-to-Lean equivalence theorems.
• Kani Harnesses · the bounded model-checking lane on production Rust.