Theorem Inventory

Find a registered Lean theorem by name, property, or source file, and read the model boundary it carries.

On this page

Each of the 165 theorem entries in Chio's published source inventory appears here with its Lean name, source file, property mapping, and claim class.

Search an exact identifier, a property such as P1, a claim class, or a source filename. The prose under each theorem is the inventory's note; the linked source holds the formal statement and proof.

Reading an entry

A theorem names a proposition over particular definitions and inputs. Its property mapping names the architectural claim it supports, and its claim class names the kind of evidence. The statement and its implementation connection set how far that evidence reaches.

Claim class	Inspect	Boundary
`bounded_model`	The Lean model, quantified inputs, and premises	The model's actual domain, which may use unbounded `Nat` and lists; the deployed Rust has separate evidence
`aeneas_equivalence`	Whether the row is a mirror fact or a generated machine-value theorem	The extracted functions; runtime callers and effects have separate evidence
`symbolic_crypto`	The symbolic hash or verification model and its assumptions	The symbolic model; the cryptographic primitive and its implementation have separate evidence

The rootImported and optional status fields are registry declarations. A verification result also needs a successful gate run at the intended source revision. An entry without a status field reads “not recorded”, exactly as the inventory leaves it.

Capability monotonicity entry

The headline P1 entry is spec.capability_monotonicity. Its premise is that the child scope passes the modeled subset check, and its conclusion is that a parent grant covers every child grant.

formal/lean4/Chio/Chio/Spec/Properties.lean18-30lean

/-- 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 theorem is conditional: it proves grant coverage when child.isSubsetOf parent = true, and it says nothing about a proposed child that fails the check. The source statement quantifies over the Lean ChioScope model; runtime scope normalization, delegation admission, and other effects have their own evidence.

The optional-cap mirror theorem is a narrower fact about preserving a parent's numeric cap. The generated-equivalence module supplies the extraction-side proof step for registered helpers. Continue with P1: Capability Monotonicity or the Lean proof walkthrough.

Symbolic-hash axiom

The inventory lists its one assumed axiom apart from the theorem entries. Chio.Json.hash_collision_resistant supplies a SymbolicHash: an output type, a digest function over canonical bytes, and an injectivity proof. The formal development assumes that structure, and SHA-256 itself stays an external contract.

The Lean declaration and the approved axiom list must agree with the inventory's assumption row. SHA-256 hashing is the contract ASSUME-SHA256.

Inspect the approved axiom and its inventory record

formal/proof-manifest.toml197-201toml

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

formal/theorem-inventory.json4-16json

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

Capability algebra

Scope coverage, attenuation and delegation facts over the declared Lean capability model.

core.scope.empty_isSubsetOf

Structural empty-scope attenuation lemma over the bounded ChioScope model.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Core.ChioScope.empty_isSubsetOf
Statement & proof: Core/Scope.lean

core.tool_grant.isSubsetOf_refl

Reflexivity lemma for ToolGrant subset in the bounded capability model.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Core.ToolGrant.isSubsetOf_refl
Statement & proof: Core/Scope.lean

spec.capability_monotonicity

Primary attenuation theorem over ChioScope grants only; no Rust refinement proof yet.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Spec.capability_monotonicity
Statement & proof: Spec/Properties.lean

spec.empty_scope_monotonicity

Shows the empty scope is always a valid attenuation in the bounded model.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Spec.empty_scope_monotonicity
Statement & proof: Spec/Properties.lean

spec.scope_budgets_nonnegative

Budget theorem is about Nat-valued maxInvocations in the reduced model only.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Spec.scope_budgets_nonnegative
Statement & proof: Spec/Properties.lean

proof.list_isSubsetOf_trans

Helper theorem for subset transitivity over bounded lists.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.list_isSubsetOf_trans
Statement & proof: Proofs/Monotonicity.lean

proof.scope_subset_of_grants_subset

Bridges grant-wise subset assumptions into ChioScope subset truth.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.scope_subset_of_grants_subset
Statement & proof: Proofs/Monotonicity.lean

proof.wildcard_subsumes

Bounded wildcard-subsumption theorem for tool-name matching.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.wildcard_subsumes
Statement & proof: Proofs/Monotonicity.lean

proof.reduced_budget_is_subset

Budget-tightening attenuation theorem over maxInvocations only.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.reduced_budget_is_subset
Statement & proof: Proofs/Monotonicity.lean

proof.added_constraint_is_subset

Additional constraint makes a ToolGrant more restrictive in the bounded model.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.added_constraint_is_subset
Statement & proof: Proofs/Monotonicity.lean

proof.delegation_chain_integrity

Covers presented delegation-chain narrowing, not full runtime graph acyclicity.

Properties: P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_chain_integrity
Statement & proof: Proofs/Monotonicity.lean

theorem.attenuation.witness_soundness

Chain-binding soundness: a v2 capability token is admitted by the verifier iff its attenuation_proof.parent_scope_hash matches the trust-root scope hash (direct issue) or the last delegation link's signed scope_hash (delegated chain). The root-imported, sorry-free theorem is exercised by the nightly Lean gate; the Rust shell is exercised by crates/tooling/chio-conformance/tests/attenuation_witness_rejects_inflated_parent_scope.rs and the protocol-side check is implemented in chio_core_types::capability::CapabilityToken::validate_chain_binding.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.AttenuationWitness.witness_soundness
Statement & proof: Proofs/AttenuationWitness.lean

theorem.budget.sibling_sum_soundness

Sibling-sum budget enforcement: when the BudgetRegistry admits a child, the running sum after admission is bounded by the parent's share. This rejects cross-hop amplification where two siblings jointly oversubscribe their parent's budget. The root-imported, sorry-free theorem is exercised by the nightly Lean gate; the Rust shell is exercised by crates/tooling/chio-conformance/tests/budget_split_rejects_oversubscribed_siblings.rs and the cross-hop case by crates/tooling/chio-conformance/tests/budget_split_cross_hop_rejects_amplification.rs. The protocol-side check is implemented in chio_kernel_core::budget_split::BudgetSplit::try_admit_child.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.SiblingSumBudget.sibling_sum_soundness
Statement & proof: Proofs/SiblingSumBudget.lean

Revocation

Revocation-store model facts. Evaluator and protocol entries below also map to P2; search P2 to see them together.

proof.revoke_marks_capability_revoked

Revoke operation marks the target capability id revoked in the bounded revocation-store model.

Properties: P2. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.revoke_marks_capability_revoked
Statement & proof: Proofs/Revocation.lean

proof.revoke_preserves_existing_revocation

Adding a revocation does not clear prior revoked capability ids in the bounded revocation-store model.

Properties: P2. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.revoke_preserves_existing_revocation
Statement & proof: Proofs/Revocation.lean

proof.checkRevocation_revoked_token_errors

A revoked token returns an error in the bounded revocation check.

Properties: P2. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.checkRevocation_revoked_token_errors
Statement & proof: Proofs/Revocation.lean

proof.checkRevocation_revoked_ancestor_never_ok

A delegation chain with a revoked ancestor cannot pass the bounded revocation check.

Properties: P2. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.checkRevocation_revoked_ancestor_never_ok
Statement & proof: Proofs/Revocation.lean

proof.checkRevocation_ok_implies_not_revoked

A successful bounded revocation check implies neither token nor presented ancestor is revoked.

Properties: P2. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.checkRevocation_ok_implies_not_revoked
Statement & proof: Proofs/Revocation.lean

Evaluation

Allow and denial properties of the Lean evaluator, including time, signature, scope and revocation checks.

proof.evalToolCall_total

The bounded evaluator always returns either allow or deny.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_total
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_invalid_signature_denies

Invalid capability signatures deny in the bounded evaluator.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_invalid_signature_denies
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_not_yet_valid_denies

Capabilities before their validity window deny in the bounded evaluator.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_not_yet_valid_denies
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_expired_denies

Expired capabilities deny in the bounded evaluator.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_expired_denies
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_revoked_token_never_allows

A revoked token cannot produce allow in the bounded evaluator.

Properties: P2, P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_revoked_token_never_allows
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_revoked_ancestor_never_allows

A revoked presented ancestor cannot produce allow in the bounded evaluator.

Properties: P2, P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_revoked_ancestor_never_allows
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_out_of_scope_denies

Out-of-scope tool calls deny in the bounded evaluator.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_out_of_scope_denies
Statement & proof: Proofs/Evaluation.lean

proof.evalToolCall_all_checks_pass_allow

The bounded evaluator allows when signature, time, revocation, and scope checks all pass.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.evalToolCall_all_checks_pass_allow
Statement & proof: Proofs/Evaluation.lean

Canonical data, receipts and Merkle evidence

Canonical rendering, modeled receipts and proof traversal. Read each claim class and the explicit symbolic-hash assumption with the statement.

proof.escape_string_inj

A checked decoder proves that Chio's C0, DEL, and C1 escaping, short escapes, quotes, reverse solidus, and literal Unicode scalar rendering are injective.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.escape_string_inj
Statement & proof: Proofs/CanonicalInjective.lean

proof.render_int_inj

Canonical sign and decimal-digit rendering is injective across the signed i64 and unsigned u64 modeled range.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.render_int_inj
Statement & proof: Proofs/CanonicalInjective.lean

proof.sorted_assoc_ext

Strictly UTF-16-sorted unique object entries are determined by their canonical rendering.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.sorted_assoc_ext
Statement & proof: Proofs/CanonicalInjective.lean

proof.canonical_inj

A proved injective Unicode-scalar-to-UTF-8 boundary plus deterministic lexical recovery and structural parsing establish canonical byte injectivity for normalized integers, scalar strings, and arbitrary finite arrays and objects.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.canonical_inj
Statement & proof: Proofs/CanonicalInjective.lean

proof.receipt_id_input_collision_resistant

Equal symbolic identifiers bind an injective named-object projection of all 20 ChioReceiptIdInput fields. The projection follows UTF-16 field-key order and Rust serde omission rules. Compound action, decision, actor-chain, evidence, metadata, and key values must inhabit bounded JValue; production serde correspondence remains ASSUME-CANONICAL-JSON.

Properties: P4, P7. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.receipt_id_input_collision_resistant
Statement & proof: Proofs/Receipt.lean

proof.receipt_id_collision_resistant

Equal symbolic receipt identifiers imply equal modeled content and policy hashes as a corollary of full 20-field projection binding plus the audited hash collision-resistance idealization.

Properties: P4, P7. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.receipt_id_collision_resistant
Statement & proof: Proofs/Receipt.lean

proof.applyProof_append

Helper theorem for symbolic Merkle-proof composition.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.applyProof_append
Statement & proof: Proofs/Receipt.lean

proof.membership_proof_sound

Merkle inclusion soundness under the symbolic ReceiptTree hash model.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.membership_proof_sound
Statement & proof: Proofs/Receipt.lean

proof.membership_proof_verifies

Executable verification theorem for symbolic membership proofs.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.membership_proof_verifies
Statement & proof: Proofs/Receipt.lean

proof.stepFoldLoop_eq_directedProofLoop_map

Inductive equivalence between the executable hash fold and the direction-tagged proof decoder at the same bounded fuel.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.stepFoldLoop_eq_directedProofLoop_map
Statement & proof: Proofs/MerkleWalk.lean

proof.stepFold_eq_directedProof_map

The checked inclusion walk and direction-tagged proof decoder agree on invalid geometry, carry levels, path consumption, and trailing-path rejection.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.stepFold_eq_directedProof_map
Statement & proof: Proofs/MerkleWalk.lean

proof.stepFold_eq_applyProof

A successfully decoded index-directed audit path produces exactly the existing Receipt.applyProof result.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.stepFold_eq_applyProof
Statement & proof: Proofs/MerkleWalk.lean

proof.stepFold_membership_sound_if_geometry_agrees

Conditional composition of the index-directed fold with membership_proof_sound. The separate bounded geometry theorem discharges traversal shape for the supported domain.

Properties: P4, P7. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.stepFold_membership_sound_if_geometry_agrees
Statement & proof: Proofs/MerkleWalk.lean

proof.boundedWalkGeometry_decodes

All 36 carry-last-node geometries through eight leaves decode to a direction-tagged proof whose application reaches the declared symbolic root.

Properties: P4, P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.boundedWalkGeometry_decodes
Statement & proof: Proofs/MerkleWalk.lean

proof.bounded_stepFold_sound

The checked fold reaches the declared symbolic root for every leaf index at every tree size from one through eight. Hashing remains under ASSUME-SHA256.

Properties: P4, P7. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.bounded_stepFold_sound
Statement & proof: Proofs/MerkleWalk.lean

proof.checkpoint_consistency

Checkpoint consistency over the bounded checkpoint-store model.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.checkpoint_consistency
Statement & proof: Proofs/Receipt.lean

proof.receipt_sign_then_verify

Receipt signature theorem over the symbolic sign/verify model, not Ed25519 implementation proofs.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.receipt_sign_then_verify
Statement & proof: Proofs/Receipt.lean

proof.receipt_immutability

Tampering theorem under the symbolic receipt-signature model.

Properties: P4. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.receipt_immutability
Statement & proof: Proofs/Receipt.lean

Protocol decisions and lifecycle models

Admission, guard composition, budgets, lineage, delivery, reservation transitions and finding-status decisions. These rows retain their individual model boundaries.

proof.admitSession_invalid_dpop_rejects

DPoP-required admission rejects invalid DPoP evidence in the bounded pure admission model.

Properties: P3, P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.admitSession_invalid_dpop_rejects
Statement & proof: Proofs/Protocol.lean

proof.admitSession_invalid_anchor_rejects

Session-anchor-required admission rejects invalid continuation anchors in the bounded pure admission model.

Properties: P3, P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.admitSession_invalid_anchor_rejects
Statement & proof: Proofs/Protocol.lean

proof.budgetPrecheck_commit_preserves_bounds

Successful bounded budget commits cannot increase remaining invocation or unit counters.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.budgetPrecheck_commit_preserves_bounds
Statement & proof: Proofs/Protocol.lean

proof.budgetCommit_none_when_precheck_fails

Exhausted bounded budget prechecks fail closed with no commit state.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.budgetCommit_none_when_precheck_fails
Statement & proof: Proofs/Protocol.lean

proof.budgetTwoCommit_preserves_bounds

Two accepted sequential bounded budget commits cannot increase remaining counters.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.budgetTwoCommit_preserves_bounds
Statement & proof: Proofs/Protocol.lean

proof.clusterOverrun_bound_is_explicit

Clustered mode proof is limited to the explicit max-cost-per-node overrun bound.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.clusterOverrun_bound_is_explicit
Statement & proof: Proofs/Protocol.lean

proof.governedApproval_required_without_token_fails

Governed actions that require approval fail without a valid approval token in the bounded model.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.governedApproval_required_without_token_fails
Statement & proof: Proofs/Protocol.lean

proof.governedApproval_valid_token_passes

A valid approval token satisfies the bounded governed-approval model.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.governedApproval_valid_token_passes
Statement & proof: Proofs/Protocol.lean

proof.dpop_required_missing_proof_rejects

A grant requiring DPoP rejects when no proof is presented in the bounded nonce model.

Properties: P3, P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.dpop_required_missing_proof_rejects
Statement & proof: Proofs/Protocol.lean

proof.dpop_required_invalid_proof_rejects

A grant requiring DPoP rejects invalid presented proof evidence in the bounded nonce model.

Properties: P3, P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.dpop_required_invalid_proof_rejects
Statement & proof: Proofs/Protocol.lean

proof.dpop_reused_nonce_rejects

A live DPoP nonce cannot be admitted a second time in the bounded replay-cache model.

Properties: P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.dpop_reused_nonce_rejects
Statement & proof: Proofs/Protocol.lean

proof.revocationSnapshot_revoked_token_denies

A projected snapshot that marks the presented token revoked denies in the bounded model.

Properties: P2, P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.revocationSnapshot_revoked_token_denies
Statement & proof: Proofs/Protocol.lean

proof.revocationSnapshot_revoked_ancestor_denies

A projected snapshot that marks a presented ancestor revoked denies in the bounded model.

Properties: P2, P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.revocationSnapshot_revoked_ancestor_denies
Statement & proof: Proofs/Protocol.lean

proof.guardPipeline_deny_dominates

A guard deny forces the final bounded guard-composition decision to deny.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.guardPipeline_deny_dominates
Statement & proof: Proofs/Protocol.lean

proof.guardPipeline_error_dominates

A guard error forces the final bounded guard-composition decision to deny.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.guardPipeline_error_dominates
Statement & proof: Proofs/Protocol.lean

proof.guardPipeline_allow_requires_core_authorized

The bounded guard pipeline can allow only if core authorization already passed.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.guardPipeline_allow_requires_core_authorized
Statement & proof: Proofs/Protocol.lean

proof.wasm_guest_output_confinement

For Chio's bounded core-module dispatch model, executions with the same typed guest output make the same pipeline decision. This is not a proof of wasmtime internals or full engine information-flow non-interference.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Guards.WasmBoundary.guest_output_confinement
Statement & proof: Guards/WasmBoundary.lean

proof.wasm_no_allow_amplification

No typed wasm guest output can turn coreAuthorized=false into an allowed bounded pipeline result, including when the guard is advisory.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Guards.WasmBoundary.no_allow_amplification
Statement & proof: Guards/WasmBoundary.lean

proof.wasm_resource_exhaustion_fail_closed

Fuel exhaustion, memory exhaustion, and traps map to deny for blocking guards in the bounded dispatch model, subject to ASSUME-WASM-ENGINE.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Guards.WasmBoundary.resource_exhaustion_fail_closed
Statement & proof: Guards/WasmBoundary.lean

proof.wasm_advisory_mode_nonblocking

Advisory wasm guards are non-blocking by design: denies, malformed verdicts, traps, and resource exhaustion all contribute allow at this guard layer. Core authorization still dominates the final pipeline.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Guards.WasmBoundary.advisory_mode_is_nonblocking_by_design
Statement & proof: Guards/WasmBoundary.lean

proof.receiptFieldsCoupled_preserves_all_fields

A coupled receipt body preserves capability, request, verdict, policy hash, and evidence class.

Properties: P4. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.receiptFieldsCoupled_preserves_all_fields
Statement & proof: Proofs/Protocol.lean

proof.observed_parent_edge_sound

Observed local parent edges imply a parent request existed in the same authenticated session.

Properties: P6. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.observed_parent_edge_sound
Statement & proof: Proofs/Protocol.lean

proof.verified_receipt_lineage_sound

Verified receipt lineage requires both receipts, trusted kernel signature, and signed linkage in the bounded model.

Properties: P7. Claim class: symbolic_crypto. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.verified_receipt_lineage_sound
Statement & proof: Proofs/Protocol.lean

proof.session_continuity_sound

Verified session continuity requires a valid session anchor and continuation artifact in the bounded model.

Properties: P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.session_continuity_sound
Statement & proof: Proofs/Protocol.lean

proof.capability_lineage_consistency_sound

Verified call-chain consistency requires subject and parent capability references to agree in the bounded model.

Properties: P9. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.capability_lineage_consistency_sound
Statement & proof: Proofs/Protocol.lean

proof.report_truthfulness_asserted_not_verified

Report/export surfaces cannot upgrade asserted lineage to verified in the bounded label model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.report_truthfulness_asserted_not_verified
Statement & proof: Proofs/Protocol.lean

proof.report_truthfulness_observed_not_verified

Report/export surfaces cannot upgrade observed lineage to verified in the bounded label model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.report_truthfulness_observed_not_verified
Statement & proof: Proofs/Protocol.lean

proof.registry_publish_requires_valid_signature

The bounded certification registry ignores invalidly signed published records.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.registry_publish_requires_valid_signature
Statement & proof: Proofs/Protocol.lean

proof.registry_resolve_published_valid_record

A validly signed published certification record resolves from the bounded registry model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.registry_resolve_published_valid_record
Statement & proof: Proofs/Protocol.lean

proof.registry_revoke_deactivates_published_record

Revoking a published record makes that artifact inactive in the bounded registry model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.registry_revoke_deactivates_published_record
Statement & proof: Proofs/Protocol.lean

proof.delegation_step_allow_requires_attenuation

A semantically admitted delegation step requires attenuation.

Properties: P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_step_allow_requires_attenuation
Statement & proof: Proofs/FormalClosure.lean

proof.delegation_step_allow_requires_subject_continuity

A semantically admitted delegation step requires subject continuity.

Properties: P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_step_allow_requires_subject_continuity
Statement & proof: Proofs/FormalClosure.lean

proof.delegation_step_allow_requires_expiry_monotonicity

A semantically admitted delegation step requires expiry monotonicity.

Properties: P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_step_allow_requires_expiry_monotonicity
Statement & proof: Proofs/FormalClosure.lean

proof.delegation_revoked_ancestor_denies

A revoked ancestor denies a delegation step in the bounded semantic model.

Properties: P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_revoked_ancestor_denies
Statement & proof: Proofs/FormalClosure.lean

proof.delegation_max_depth_failure_denies

Delegation max-depth failure denies in the bounded semantic model.

Properties: P3, P5. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.delegation_max_depth_failure_denies
Statement & proof: Proofs/FormalClosure.lean

proof.dpop_binding_allows_only_when_all_fields_match

DPoP binding admits only when every modeled binding field matches.

Properties: P8. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.dpop_binding_allows_only_when_all_fields_match
Statement & proof: Proofs/FormalClosure.lean

proof.path_prefix_rejects_sibling_prefix

Path-prefix model rejects sibling-prefix cases.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.path_prefix_rejects_sibling_prefix
Statement & proof: Proofs/FormalClosure.lean

proof.path_prefix_rejects_normalized_traversal_escape

Path-prefix model rejects normalized traversal escape cases.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.path_prefix_rejects_normalized_traversal_escape
Statement & proof: Proofs/FormalClosure.lean

theorem.handshake.negotiation_safety

Fail-closed admission soundness over the whole CurrentSchema domain: checkCurrentSchema admits only when the presented schema is the current Chio-owned one (any non-current schema is rejected before signature, time, floor, or budget checks). The theorem quantifies over all inputs and rules out admitting anything unrecognized, but the model is bounded to a two-constructor schema enum: it does NOT mechanize the wider hot-path verifier (chain-binding, signature, crypto floor, budgets) and does not model alternate Chio-owned capability schema rungs (none are exposed pre-release).

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.HandshakeNegotiation.negotiation_admit_only_current
Statement & proof: Proofs/HandshakeNegotiation.lean

theorem.budget.reservation_conservation

Pure reservation folds preserve reserved = outstanding + committed + released + retained, with admitted child reserves bounded by sibling_sum_soundness. Apalache interleavings, the Kani and Creusot transition witnesses, the debug journal replay, and the stateful real-store test provide independent evidence for the defect family a6d26dbc4, c201afbd0, 84e98b9d0, and 58abf33d2. Scalar admission is linked; production ledger linkage is not established.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.ReservationLedger.ledger_conservation
Statement & proof: Proofs/ReservationLedger.lean

theorem.budget.reservation_terminal_unique

A finalized pure ledger is absorbing: it cannot reserve again or receive a second positive terminal disposition. Committed and released amount buckets may both be non-zero after partial realization, while the trace still has one terminal hold classification. The theorem is model-level; concrete hold terminality is checked by the debug journal replay and stateful real-store test, not by a production refinement proof.

Properties: P1. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.ReservationLedger.ledger_terminal_unique
Statement & proof: Proofs/ReservationLedger.lean

proof.delivery_contract.settlement_admission_sound

Over finite requirement, evidence, and opaque digest domains, settlement admission implies Allow and proves every required finding purchase is verified and every required output digest matches. The M3 Rust linkage covers the digest comparison; the finding-purchase dimension is the explicit M4 composition boundary. This is not a Rust refinement proof and does not model SHA-256, canonical JSON, signatures, persistence, payment rails, or external settlement.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.DeliveryContract.settlement_admission_requires_verified_evidence
Statement & proof: Proofs/DeliveryContract.lean

proof.delivery_contract.allow_requires_evidence

An Allow in the bounded delivery finalizer implies that any required finding purchase is verified and any required expected and observed digest identities are equal.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.DeliveryContract.allow_requires_verified_evidence
Statement & proof: Proofs/DeliveryContract.lean

proof.delivery_contract.denied_after_delivery_no_settlement

Every reachable deniedAfterDelivery result in the bounded model carries a blocked settlement gate, matching the M3 DeniedAfterDelivery and ContractualZeroCharge boundary without modeling the external rail.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.DeliveryContract.denied_after_delivery_cannot_settle
Statement & proof: Proofs/DeliveryContract.lean

proof.finding_status_epoch_advance_is_strict

A verified signed status epoch advances the durable floor only when its map epoch is strictly greater. Cryptographic and SQLite correctness remain outside this bounded model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.FindingStatusFreshness.epoch_advance_is_strict
Statement & proof: Proofs/FindingStatusFreshness.lean

proof.finding_status_non_inclusion_not_expired

An admitted portable non-inclusion decision has checked_at at or before the signed status epoch valid_until bound.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.FindingStatusFreshness.admitted_non_inclusion_not_past_valid_until
Statement & proof: Proofs/FindingStatusFreshness.lean

proof.finding_status_pending_is_sticky

A local pending retraction cannot be cleared by a contradictory non-inclusion proof in the bounded decision model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.FindingStatusFreshness.pending_never_accepts_non_inclusion
Statement & proof: Proofs/FindingStatusFreshness.lean

proof.finding_status_retracted_is_sticky

A local retracted observation cannot be cleared by a contradictory non-inclusion proof in the bounded decision model.

Properties: P10. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Proofs.FindingStatusFreshness.retracted_never_accepts_non_inclusion
Statement & proof: Proofs/FindingStatusFreshness.lean

Treaties and cross-operator admission

Predicate intersection, bilateral acceptance, amendment refinement and bridge models. The treaty abstraction's drift checks do not establish Rust refinement.

proof.treaty_admission_iff_predicate_intersection

Public bounded treaty model showing bilateral admission is equivalent to the conjunction of syntactic treaty, left-polity, and right-polity predicates over the production-shaped admission projection.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.treaty_admission_iff_predicate_intersection
Statement & proof: Treaty/Intersection.lean

proof.treaty_admission_stable_under_ladder_floor

Public bounded treaty model showing a satisfied governance-mode floor leaves the fail-closed syntactic admission decision unchanged.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.treaty_admission_stable_under_ladder_floor
Statement & proof: Treaty/Intersection.lean

Public bounded amendment model equating admissibility with semantic backward refinement on the candidate's explicit admission domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.amendment_admissible_iff_backward_refinement
Statement & proof: Treaty/Intersection.lean

Public bounded amendment model showing a failed finite refinement check produces a rejected verdict.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.amendment_without_refinement_rejected
Statement & proof: Treaty/Intersection.lean

proof.freestanding_accept_set_theorem

Bounded bilateral DSSE accept-set model showing acceptance is exactly issuer-key trust, kernel-key trust, and fail-closed predicate satisfaction over the admission projection. Signature verification remains abstracted.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.BilateralAccept.freestanding_accept_set_theorem
Statement & proof: Treaty/BilateralAccept.lean

proof.essential_preserved_chain

Bounded syntactic-constitution model showing essential admission preservation composes across amendment chains.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.essential_preserved_chain
Statement & proof: Treaty/PredicateLang.lean

proof.containsPredicate_preserved_chain

Bounded syntactic-constitution model showing designated non-amendable predicate presence is trajectory-invariant under preserving amendments.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.containsPredicate_preserved_chain
Statement & proof: Treaty/PredicateLang.lean

proof.anchor_admission_iff_lane_quorum_satisfied

Bounded lane-quorum model showing anchor admission is exactly the deduplicated declared-lane quorum check with undeclared contributors rejected.

Properties: P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.anchor_admission_iff_lane_quorum_satisfied
Statement & proof: Treaty/PredicateLang.lean

proof.anchor_admission_rejects_undeclared_lane

Bounded lane-quorum model showing a witness with undeclared contributing lanes fails closed before quorum counting.

Properties: P7. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.anchor_admission_rejects_undeclared_lane
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.unsupported_denies

Any predicate containing unsupported syntax denies before Boolean evaluation, including under unrestricted negation.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.unsupported_predicate_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.undefined_denies

A supported predicate whose projected runtime field is unavailable denies before Boolean evaluation.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.undefined_predicate_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.negated_unknown_atom_denies

A direct negative regression theorem prevents an unknown atom from becoming true through negation.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.negated_unknown_atom_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.negated_unknown_mode_denies

An unavailable governance mode remains denied when a mode predicate is negated.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.negated_unknown_mode_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.runtime_policy_exact

The bounded runtime admission constitution accepts exactly when every registered production-shaped gate is supported, defined, and true. Parsing, hashing, signatures, and store lookup are outside this theorem.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.runtime_admission_policy_exact
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.action_missing_denies

An invocation action absent from the ladder intersection fails the modeled action-class gate.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.action_class_missing_from_intersection_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.signer_count_denies

A bilateral invocation without exactly two signer ids fails the modeled signer gate.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.signer_count_mismatch_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.signer_reuse_denies

A bilateral invocation whose deduplicated signer list is not a pair fails the modeled signer gate.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.signer_alias_reuse_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.predicate.signer_scope_denies

A signer outside the treaty participant list fails the modeled signer gate.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.signer_outside_scope_denies
Statement & proof: Treaty/PredicateLang.lean

treaty.bridge.fragment_completeness

Finite predicate checking is equivalent to semantic refinement on the exact verifier-owned admission domain. It makes no completeness claim outside that domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.refinesOn_complete_on_fragment
Statement & proof: Treaty/PredicateLang.lean

treaty.bridge.constitution_domain_completeness

The finite constitution checker is a complete decision procedure for refinement on its explicit admission domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.refinesOnConstitution_complete_on_fragment
Statement & proof: Treaty/PredicateLang.lean

treaty.syntactic.decision_exact

The amendment constructor returns a checked delta exactly when finite-domain refinement holds; callers do not supply its proof result.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.ConstitutionalDeltaSyn.ofDecide_isSome_iff
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.syntactic.admission_iff_intersection

Syntactic bilateral admission is equivalent to the fail-closed conjunction of treaty, left-polity, and right-polity predicates.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.synTreaty_admission_iff_predicate_intersection
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.syntactic.ladder_floor_stable

A satisfied governance-mode floor leaves syntactic treaty admission unchanged.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.synTreaty_admission_stable_under_ladder_floor
Statement & proof: Treaty/IntersectionSyntactic.lean

Amendment admissibility is equivalent to semantic backward refinement on the candidate's explicit admission domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.synAmendment_admissible_iff_backward_refinement
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.syntactic.failed_check_rejected

A failed finite refinement decision produces a rejected amendment verdict.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.synAmendment_without_refinement_rejected
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.bridge.pointwise

Syntactic constitution admission agrees pointwise with admission after lifting to the comparison-only closure representation.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.bridge_pointwise
Statement & proof: Treaty/BridgeEquivalence.lean

Domain-scoped backward refinement is equivalent in the syntactic and lifted closure representations.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.bridge_refinement_on_iff
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.bridge.global_iff

Global backward refinement is equivalent in the syntactic and lifted closure representations.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.bridge_global_iff
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.bridge.soundness

Global syntactic refinement transports to the lifted closure representation.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.bridge_soundness
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.bridge.decidable_soundness

A successful finite constitution decision transports to closure refinement on exactly the checked admission domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.bridge_decidable_soundness
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.bridge.equivalence_admits

Lifting a syntactic bilateral treaty to closures preserves admission for every production-shaped input projection.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.toClosure_treatyAdmits_agrees
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.bridge.equivalence_verdict

The syntactic finite decision and the lifted closure candidate produce the same amendment verdict.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.toClosure_amendmentVerdict_agrees
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.predicate.constitution_domain_exact

Exact constitution refinement on the explicit production-shaped admission domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.PredicateLang.refinesOnConstitution_iff
Statement & proof: Treaty/PredicateLang.lean

treaty.paper.admission_iff_intersection

Preserves the six-conjunct treaty intersection over the production-shaped admission projection.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.IntersectionSyntactic.treaty_admission_iff_predicate_intersection
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.paper.ladder_floor_stable

A satisfied governance-mode floor reduces to the bounded treaty decision.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.IntersectionSyntactic.treaty_admission_stable_under_ladder_floor
Statement & proof: Treaty/IntersectionSyntactic.lean

Amendment admissibility is equivalent to exact no-widening on the supplied finite domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.IntersectionSyntactic.amendment_admissible_iff_bounded_refinement
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.paper.failed_amendment_rejected

Preserves fail-closed amendment rejection after a failed finite refinement decision.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.IntersectionSyntactic.amendment_without_refinement_rejected
Statement & proof: Treaty/IntersectionSyntactic.lean

treaty.paper.polity_admission_agrees

Pointwise equivalence between syntactic polity admission and the comparison-only closure model.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.BridgeEquivalence.Legacy.polity_admission_agrees
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.paper.treaty_admission_agrees

Pointwise equivalence between syntactic treaty admission and the comparison-only closure model.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.BridgeEquivalence.Legacy.treaty_admission_agrees
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.paper.mode_admission_agrees

Pointwise equivalence after composing both treaty models with the same governance-mode floor.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.BridgeEquivalence.Legacy.treaty_admission_under_mode_agrees
Statement & proof: Treaty/BridgeEquivalence.lean

treaty.paper.bounded_amendment_sound

A checked syntactic delta establishes closure refinement only on the exact supplied domain.

Properties: P3. Claim class: bounded_model. Registry rootImported: true. Registry status: proved.

Lean name: Chio.Treaty.BridgeEquivalence.Legacy.bounded_amendment_sound
Statement & proof: Treaty/BridgeEquivalence.lean

Aeneas and model equivalence

Two proof steps: ordinary-value mirror facts and generated-machine-value equivalence. A row in the mirror module alone is not the extraction-to-model connection.

proof.aeneas_timeWindowValid_equiv_model

Derived ordinary-value bridge to CapabilityToken.isValidAt; proof.generated_time_window_valid_eq_model is the generated-code successor.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_timeWindowValid_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_optionalCapIsSubset_preserves_parent_cap

Derived ordinary-value attenuation bridge; proof.generated_optional_u32_cap_is_subset_preserves_parent_cap is the generated-code successor.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_optionalCapIsSubset_preserves_parent_cap
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_budgetCommit_equiv_model

Derived ordinary-value budget bridge; proof.generated_budget_commit_eq_model is the generated-code successor. Store mutation and reservation-ledger transitions remain outside this theorem.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_budgetCommit_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_dpopAdmits_equiv_model

Derived ordinary-value DPoP bridge; proof.generated_dpop_admits_eq_model is the generated-code successor. Cryptographic verification and nonce-store mutation remain outside this theorem.

Properties: P8. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_dpopAdmits_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_revocationSnapshot_equiv_model

Derived ordinary-value revocation bridge; proof.generated_revocation_snapshot_denies_eq_model is the generated-code successor. Storage and snapshot freshness remain outside this theorem.

Properties: P2. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_revocationSnapshot_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_guardStep_equiv_model

Derived ordinary-value guard bridge; proof.generated_guard_step_allows_eq_model is the generated-code successor. Runtime error attribution remains outside this theorem.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_guardStep_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.aeneas_receiptCoupling_equiv_model

Derived ordinary-value receipt bridge; proof.generated_receipt_fields_coupled_eq_model is the generated-code successor. Body construction, canonicalization, and cryptography remain runtime-owned.

Properties: P4. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.aeneas_receiptCoupling_equiv_model
Statement & proof: Proofs/AeneasEquivalence.lean

proof.generated_inclusion_step_eq_model

The authenticated generated machine-integer inclusion step projects exactly to the checked Lean Merkle-walk model for every U64 input. Hashing remains outside this scalar theorem.

Properties: P4, P7. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_inclusion_step_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_ledger_is_terminal_eq_model

The generated terminal-state predicate agrees with the bounded reservation ledger model under the exact U64 projection. Runtime store linkage remains outside this theorem.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_ledger_is_terminal_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_ledger_apply_eq_model

The generated checked-arithmetic transition projects to the bounded reservation ledger model for every operation and U64 input. Runtime store linkage remains outside this theorem.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_ledger_apply_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_classify_time_window_code_eq_mirror

The generated machine-integer time-window classifier projects to the ordinary-value classifier.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_classify_time_window_code_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_time_window_valid_eq_mirror

The generated machine-integer validity predicate agrees with its ordinary-value semantics.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_time_window_valid_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_exact_or_wildcard_covers_by_flags_eq_mirror

The generated exact-or-wildcard decision agrees with its ordinary-value semantics.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_exact_or_wildcard_covers_by_flags_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_prefix_wildcard_or_exact_covers_by_flags_eq_mirror

The generated prefix-wildcard decision agrees with its ordinary-value semantics.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_prefix_wildcard_or_exact_covers_by_flags_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_optional_u32_cap_is_subset_eq_mirror

The generated bounded optional-cap comparison agrees with the Nat projection.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_optional_u32_cap_is_subset_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_required_true_is_preserved_eq_mirror

The generated required-flag decision agrees with its ordinary-value semantics.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_required_true_is_preserved_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_monetary_cap_is_subset_by_parts_eq_mirror

The generated bounded monetary-cap comparison agrees with the Nat projection.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_monetary_cap_is_subset_by_parts_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_budget_precheck_eq_mirror

The generated budget precheck agrees with the ordinary-value budget decision.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_budget_precheck_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_budget_commit_eq_mirror

The generated checked subtraction result projects to the ordinary-value budget commit.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_budget_commit_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_dpop_freshness_valid_eq_mirror

The generated saturating timestamp checks agree with their bounded Nat projection.

Properties: P8. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_dpop_freshness_valid_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_dpop_admits_eq_mirror

The generated DPoP admission decision agrees with its ordinary-value semantics.

Properties: P8. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_dpop_admits_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_nonce_admits_eq_mirror

The generated nonce admission decision agrees with its ordinary-value semantics.

Properties: P8. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_nonce_admits_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_guard_step_allows_eq_mirror

The generated one-step guard conjunction agrees with its ordinary-value semantics.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_guard_step_allows_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_revocation_snapshot_denies_eq_mirror

The generated revocation snapshot decision agrees with its ordinary-value semantics.

Properties: P2. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_revocation_snapshot_denies_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_receipt_fields_coupled_eq_mirror

The generated receipt-field conjunction agrees with its ordinary-value semantics.

Properties: P4. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_receipt_fields_coupled_eq_mirror
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_time_window_valid_eq_model

The generated bounded validity predicate composes with the CapabilityToken model under explicit scalar projections.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_time_window_valid_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_optional_u32_cap_is_subset_preserves_parent_cap

A successful generated optional-cap check preserves the present parent cap and cannot widen its value.

Properties: P1. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_optional_u32_cap_is_subset_preserves_parent_cap
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_budget_commit_eq_model

The generated checked budget commit projects to the handwritten budgetCommit model.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_budget_commit_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_dpop_admits_eq_model

The generated DPoP admission decision composes with the handwritten session-admission model.

Properties: P8. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_dpop_admits_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_guard_step_allows_eq_model

The generated one-step guard decision composes with the handwritten guard-pipeline model.

Properties: P3. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_guard_step_allows_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_revocation_snapshot_denies_eq_model

The generated revocation snapshot decision composes with the handwritten denial model.

Properties: P2. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_revocation_snapshot_denies_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

proof.generated_receipt_fields_coupled_eq_model

The generated receipt-field conjunction composes with the handwritten receipt integrity model.

Properties: P4. Claim class: aeneas_equivalence. Registry rootImported: true. Registry status: not recorded.

Lean name: Chio.Proofs.generated_receipt_fields_coupled_eq_model
Statement & proof: Proofs/AeneasGeneratedEquivalence.lean

Property-to-implementation mapping

The formal mapping connects named model properties and harnesses to Rust symbols and required assumptions. It separates manually reviewed model connections from equivalence proofs. A source hash detects drift, and accepting a new hash records review; refinement comes from an equivalence proof.

TLA+ and Apalache mappings

Start with the named invariant, its selected model configuration, and the assumptions in its mapping row. The revocation model's entries include NoAllowAfterRevoke, MonotoneLog, AttenuationPreserving, RevocationFreshness, and RevocationStateCoupled. The liveness property RevocationEventuallySeen depends on model fairness and is checked separately from the safety conjunction.

The mapping column named “Assumption discharge” identifies dependencies; a listed dependency stays in force. The mapped storage contract, for example, covers single-row committed writes, and cross-row crash recovery lies outside it. Read TLA+ Specs and the storage assumption with the model result.

Kani harness mappings

The public harness registry selects the lane, source, unwind policy, and named harness. The mapping's Kani section supplies the target Rust symbols. These records sit apart from the Lean inventory above.

public_normalized_scope_subset_rejects_widened_child concerns the public normalized-scope subset operation, and public_sign_receipt_refuses_content_hash_mismatch exercises receipt signing's content-hash rejection. Read a harness's inputs and assertions before interpreting a pass; Kani Harnesses explains the lane and its bounds.

The mapping checker enforces selected model names, mandatory invariant membership, public Kani names, and registered concurrency harness mappings. It checks cross-references; equivalence between two models, or between a model and Rust, comes from a proof.

Registration and proof runs

Four records answer different questions about a theorem:

Inventory entry. A declared Lean name, source file, claim class, property mapping, and optional status. It carries no execution result.
Successful formal gate. The configured Lean build, sorry checks, declaration and property-map checks, and the axiom and opaque environment audit completed for that checkout.
Implementation evidence. The extraction, equivalence, contract, harness, or runtime check that connects a model result to the production boundary.
Source-bound proof report. Recorded modes, gate outcomes, and source identities. Checking its structure does not replay those gates.

The formal gate requires theorem rows to declare rootImported: true and finds the named theorem declarations in their stated files. That inventory check is lexical, and the flag is a declaration; the Lean build and the elaborated assumption audit are the stages that load the modules.

To check the evidence your release carries, use the formal Quickstart. To interpret an existing report, read Verification Evidence, and when a stage fails, keep its output for Failure Modes.

Next: follow a theorem into its evidence

Lean 4 ProofsRead how definitions, premises, and the approved axiom shape each statement.Aeneas PipelineTrace generated Rust semantics into an equivalence theorem.Assumptions & TCBRead the deployment contracts each claim still needs.

PreviousP1: Capability Monotonicity NextAssumptions & TCB