Chio/Docs

Lean 4 Proofs

Lean 4 is the proof assistant chio uses for the capability algebra, the bounded evaluator, the revocation store, the symbolic receipt model, and the protocol-level closure theorems. The project lives at formal/lean4/Chio/. Every theorem reachable from Chio.lean is listed in formal/theorem-inventory.json with rootImported: true; the Lean kernel has type-checked each one without sorry.

Toolchain pin

The Lean toolchain is pinned at leanprover/lean4:v4.28.0-rc1 in formal/lean4/Chio/lean-toolchain. lake build picks it up and downloads the matching toolchain on first run.

Why Lean 4

Three properties of Lean 4 carry weight for chio.

  • 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.
  • Good ergonomics for property proofs. Definitional unfolding, type-class inference, and the elaborator make property statements feel close to executable Rust.

Project Layout

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

formal/lean4/Chio/ 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

The proof manifest names every root module the gate must consume:

formal/proof-manifest.toml
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",
]

P1: Capability Monotonicity

The headline theorem is Chio.Spec.capability_monotonicity in Spec/Properties.lean. It says: 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. Delegation can only attenuate, never amplify.

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 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/chio-core-types/src/capability.rs in ChioScope::is_subset_of and crates/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 that the bounded evaluator is total and that every denial path is covered. Eight theorems together establish the fail-closed property P3 over the bounded model.

  • evalToolCall_total · the evaluator always returns either allow or deny; no third state.
  • 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.

Every theorem has 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 holds the canonical 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:

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:

formal/lean4/Chio/Chio/Core/Scope.lean
/-- 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:

formal/lean4/Chio/Chio/Core/Scope.lean
/-- 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:

formal/lean4/Chio/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 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:

formal/lean4/Chio/Chio/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 machinery; no Mathlib import is needed for the headline 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 full Lean lane is one command:

reproduce lean lane
cd formal/lean4/Chio
lake build
lake build stdout (excerpt)
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

On first run, lake reads the toolchain pin and downloads leanprover/lean4:v4.28.0-rc1. Subsequent runs are cached. The full build elaborates and type-checks every theorem in the inventory.

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

  • Every theorem in theorem-inventory.json must exist in the elaborated environment.
  • Every theorem must have rootImported: true via import-graph closure from Chio.lean.
  • The set of declared axioms must equal allowed_axioms in the manifest. Today that set has exactly one entry, Chio.Core.verifyCapabilitySignature.

Where Lean Output Corresponds to Rust

formal/MAPPING.md is the cross-reference. Every named Kani harness and every named 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.

Adding a new theorem

To add a new Lean theorem to the bounded model: write the statement, prove it, add the row to theorem-inventory.json with the right claimClass and mapsTo property IDs, and re-run the gate. The gate fails the build if the entry is missing or if the theorem fails to elaborate.

Next

Lean 4 Proofs · Chio Docs