Lean 4 Proofs
Read Chio's machine-checked statements, trace each premise and assumption, and reproduce the Lean gate from the public source.
On this page
Lean proves capability attenuation over the ChioScope model: when a child scope passes the subset check, every child grant has a covering parent grant.
The same discipline covers evaluation, revocation, receipts, and protocol decisions. Each theorem rests on named definitions, explicit premises, and at most one approved project axiom, a symbolic hash. Aeneas, Kani, and differential tests connect selected statements to the Rust that runs, and the assumption register names the contracts outside every proof.
A theorem states its inputs, premises, and conclusion
The Lean kernel checks each proof against the definitions in Chio/Core and Chio/Spec. capability_monotonicity assumes child.isSubsetOf parent and concludes that every child grant has a covering parent grant. P1: Capability Monotonicity.
A Lean claim reaches as far as its definitions, premises, and implementation link
Read the statement before the proof. Four parts decide how far a theorem reaches:
- Definitions and inputs. The values and operations the model represents.
- Premises. The facts that must already hold for the conclusion to apply.
- Conclusion and proof. What follows, and which definitions, lemmas, or assumptions support it.
- Implementation connection. The extracted function, projection, harness, or test that ties the statement to deployed code.
The Theorem Inventory lists every named statement with its property mapping. Its model-class label is a starting point for inspection; the domain is in the statement, and a theorem over Nat or lists may quantify over arbitrary values or lengths.
A theorem covers its model. A Mirrors docstring or a mapping row locates the related Rust, and a token-hash mirror check detects the drift it compares; semantic equivalence comes from other lanes. Aeneas Pipeline proves generated scalar equivalence for registered helpers, and the P1 Kani harness separates ordinary Rust from its bounded Kani branch.
Capability monotonicity follows from the subset definition
The P1 walkthrough shows a parent wildcard grant covering two invoke grants and refusing a new delegate operation. The headline theorem states the accepted relationship in general.
/-- 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 takes three steps:
intro g h_mem. Choose an arbitrary child grant and the fact that it belongs to the child list.- Unfold the scope predicate. Expose the hypothesis that every child grant passes an any-parent coverage check.
- Apply the list lemmas. Extract the selected grant's successful check, then obtain the parent witness and its membership fact.
The proof is short because the subset definition asks for exactly that witness. ToolGrant.isSubsetOf checks server identity, wildcard-or-exact tool coverage, operation membership, invocation caps, and retained constraints. The Rust scope carries further fields and grant kinds that this model leaves out.
Inspect the scope predicate, grant predicate, and type
/-- 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))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/-- 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, LawfulBEqComplete Rust scope refinement needs more than this theorem. For a scalar part of attenuation, the generated invocation-cap theorem supplies a separate implementation connection.
One approved axiom stands in for collision-resistant hashing
Chio's one approved project axiom is Chio.Json.hash_collision_resistant. It postulates a SymbolicHash: an output type, a digest over canonical bytes, and injectivity of that digest. The symbolic receipt proofs use that structure to establish binding relationships.
Inspect the approved name and symbolic hash declaration
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",
]structure SymbolicHash where
Output : Type
digest : CanonicalBytes → Output
injective : ∀ left right, digest left = digest right → left = right
axiom hash_collision_resistant : SymbolicHashSHA-256 compresses its inputs, so its contract is computational collision resistance, which literal injectivity idealizes. That obligation stays outside Lean as ASSUME-SHA256: a receipt theorem built on the symbolic axiom covers the symbolic hash, and a SHA-256 implementation rests on the external assumption.
The similarly named receipt_id_collision_resistant is a theorem: equal modeled receipt identifiers imply equal content and policy hashes. It derives from the stronger identifier-input binding result, and the theorem's dependency output lists the assumptions it uses.
“One approved project axiom” counts the declarations audited in Chio's project modules. The imported Lean environment carries its own standard-library axioms, and a deployment has trusted dependencies beyond this one.
Evaluation, revocation, receipt, and protocol statements keep their premises explicit
Each family proves specific branches of a pure model under premises the statement names. The source file holds the complete premises.
| Family | Modeled result | Source |
|---|---|---|
| Evaluation | evalToolCall returns allow, or deny with a reason | Evaluation.lean |
| Revocation | revoke marks its target and keeps existing revocations | Revocation.lean |
| Receipts | Membership, consistency, signing, immutability, identifier binding | Receipt.lean |
| Protocol closure | Admission requires the attenuation fact; DPoP needs matching fields and freshness | FormalClosure.lean |
In evaluation, the expired-denial theorem assumes the modeled signature check passed, the validity window started, and the clock reached expiry. The invalid-signature and time branches deny under their stated premises, and the revoked-token theorem proves a non-allow result even when a preceding check produces the denial. When signature, time, revocation, and scope premises all hold, the model returns allow.
Totality means the pure result is always allow or a reasoned deny; latency and availability are runtime properties outside it. These statements execute no IO, database, network transport, or subprocess.
The receipt proofs support five conclusions about the symbolic model. The Ed25519 implementation, serialization, persistence, and tool effects need their own evidence, and Receipts connects the record to a mediated call.
- Membership. A path produced for a receipt in the modeled tree verifies against that tree's root.
- Checkpoint consistency. Two results for the same sequence in one modeled checkpoint-store function have the same root; distributed agreement is a separate property.
- Sign then verify. The symbolic signing and verification functions agree on an unchanged body.
- Body immutability. Changing the body while reusing the original symbolic signature fails modeled verification.
- Identifier binding. Equal symbolic identifiers bind the modeled input fields through canonical encoding and the symbolic hash axiom.
Revocation proofs make the store and the presented chain explicit: a successful check implies that neither the token nor a presented ancestor is marked revoked in that store. Snapshot, propagation, freshness, and persistence belong to the Rust and protocol evidence, which also covers timely delivery of a remote revocation.
The closure model combines facts for attenuation, subject continuity, expiry, depth, and revocation. Its delegation theorem proves that admission requires the attenuation fact, and its DPoP theorem exposes a conjunction of matching-field and freshness facts. Computing each fact from an untrusted runtime request is the producer's job, which implementation evidence covers.
The path-prefix examples in FormalClosure.lean operate on lists of path segments. They reject app against application, and app against an already normalized etc/passwd. A correct filesystem parser and normalizer remain a separate implementation obligation.
One gate builds the proofs and audits what they assume
The Lean gate runs before every release is tagged, and the proof report records its result against the tag's source commit. Check it for the binary you run:
chio release verify --evidence formalbinary /usr/local/bin/chio chio 0.2.0 aarch64-apple-darwin
checksum matches SHA256SUMS for v0.2.0
signed by release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal proof report bound to v0.2.0, every gate passed
lean root-imported theorems checked
aeneas production extraction and equivalence
kani public PR lane
apalache positive and negative invariants
creusot core contracts
diff-tests scope, canonical JSON, receipts, treaties
timing dudect threshold
verifiedThe gate checks fixture drift, runs lake build, scans shipped Chio source for a literal sorry, runs the assumption-audit regressions, and validates the registries and the imported environment. A passing library build covers the second stage only, so the lean line reports the whole gate. Maintainers run it from source, with the pinned Lean toolchain, as Qualification: formal gates describes; the first run downloads and builds the Lean dependencies.
The environment helper imports Chio, FormalAeneas.Funs, and FormalEconomy.Funs, requires every audited project module to be present, and attributes each axiom and opaque declaration to its module. The gate compares project axioms with the approved list and opaque declarations with the generated-Repr allowlist, then checks names, property mappings, and prohibited source controls.
The theorem-name check reads named declarations from each registered source file, while the rootImported field stays registry metadata. Keep the build and environment audit with those records when you report a result; Failure Modes explains each refusal.
Find the definition, proof, and generated input
Chio/CoreandChio/Spec. Model types, executable definitions, and primary property statements.Chio/Proofs. Supporting statements for authority, evidence, protocol decisions, and generated equivalence.Chio/Json. Canonical values and rendering, fixtures, and the symbolic hash axiom.- Capability, Guards, Treaty, and Economy. Domain models and statements; the theorem inventory lists each registered claim.
FormalAeneasandFormalEconomy. Committed generated Lean snapshots that the equivalence module consumes.Chio.leanandlakefile.lean. Project imports and the default Chio, FormalAeneas, and FormalEconomy build targets.
The proof manifest's root_modules array is a declared file list; the root imports and the elaborated module audit determine what Lean loads. Treaty/ReceiptPredicate.lean, for example, is imported by Chio.lean and absent from that array.
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",
]leanprover/lean4:v4.28.0To add a claim, keep its definitions and premises, import its module, add the inventory and property-mapping entries the claim needs, and run the full gate. Then establish the implementation and deployment evidence that the published statement requires.