P1 Tour: Capability Monotonicity

P1 is the keystone safety property of Chio. Stated informally: a delegated capability can never grant more authority than its parent. This page traces P1 through every assurance layer the proof manifest names for it: the informal claim and TLA+ context, the Lean 4 statement and proof, the Aeneas-extracted equivalence theorem, the public Kani harness on production Rust, and the differential test that runs the spec against the impl on random inputs.

Where P1 Sits in the Pyramid

P1 sits at the top of the assurance pyramid: hand-written Lean proof, plus Aeneas equivalence to extracted Rust, plus a Kani harness on the production normalized AST, plus a differential test on the public capability struct, plus a TLA+ refinement invariant on the cross-authority protocol.

Reading the pyramid from top to bottom the same property gets progressively closer to the executable Rust binary. Lean is the narrowest, strongest layer; the differential test is broader and weaker but exercises the actual Rust code on random inputs. P1 is the only property in the manifest that today populates every applicable lane at the top three tiers.

The Informal Claim

Plain English: when authority A holds a capability and delegates it to authority B, the resulting child capability can only be narrower than A's. B cannot widen the server set, the tool set, the operation set, the constraint set, the invocation budget, the per-call monetary budget, the total monetary budget, or the DPoP requirement. B cannot extend the validity window past A's expiry.

The threat model: a malicious or compromised intermediate authority tries to amplify the authority it received from a trusted issuer. Without P1, an intermediary could rewrite a capability that says { tool: "search", max_invocations: 10 } into one that says { tool: "*", max_invocations: 10000 } and present it to a downstream tool server. P1 says: the downstream verify path rejects every such rewrite.

The cross-reference is 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. Both functions return false for any rewrite that widens any axis. Every protocol adapter must call the kernel core through chio_kernel_core::evaluate; the gate scripts/check-adapter-no-bypass.sh fails the build if any adapter sidesteps that path.

The TLA+ Context

At the cross-authority protocol level, P1 manifests as the named invariant AttenuationPreserving in formal/tla/RevocationPropagation.tla:

AttenuationPreserving ==
    \A a \in ProcSet, c \in CapSet :
        /\ depth[a][c] \in 0..DEPTH_MAX
        /\ (state[a][c] = "attenuated" => depth[a][c] > 0)

The invariant is structural: depth stays inside 0..DEPTH_MAX and any capability in the attenuated state must have been delegated at least once. From formal/MAPPING.md it constrains crates/chio-core-types/src/capability.rs (ChioScope::is_subset_of) and crates/chio-kernel-core/src/normalized.rs and is bounded by DEPTH_MAX rather than any audited assumption.

Apalache checks the conjunction SafetyInv = DomainsOK ∧ NoAllowAfterRevoke ∧ MonotoneLog ∧ AttenuationPreserving on the PR safety lane. The lane runs to computation length 16 with the model config at formal/tla/MCRevocationPropagation.cfg; a clean run prints Checker reports no error and exit code OK.

The Lean 4 Proof

The headline Lean theorem lives at formal/lean4/Chio/Chio/Spec/Properties.lean:24 with the identifier Chio.Spec.capability_monotonicity.

/-- P1: Capability monotonicity -- if a child scope is a subset of a parent
    scope, then every grant in the child is covered by some grant in the
    parent.

    This is the core Chio safety property: delegation can only attenuate,
    never amplify. -/
theorem capability_monotonicity (parent child : ChioScope)
    (h : child.isSubsetOf parent = true) :
    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 structure of the statement: take two ChioScope values parent and child; assume the boolean child.isSubsetOf parent evaluates to true; conclude that for every grant g in child.grants there exists a witness grant pg in parent.grants such that g.isSubsetOf pg is also true. The proof is three tactics: introduce the bound variable and the membership hypothesis, unfold the definition of ChioScope.isSubsetOf (which is List.all child.grants (g => List.any parent.grants (pg => g.isSubsetOf pg))), and apply the List.any_eq_true and List.all_eq_true elimination lemmas to recover the witness.

The supporting lemmas live in formal/lean4/Chio/Chio/Proofs/Monotonicity.lean:

• scope_subset_of_grants_subset · bridges grant-wise subset assumptions into ChioScope subset truth.
• reduced_budget_is_subset · tightening max_invocations downward is attenuation.
• added_constraint_is_subset · adding a constraint makes the grant strictly more restrictive.
• wildcard_subsumes · parent wildcard tool name covers any concrete child name.
• delegation_chain_integrity · transitive subset across multi-hop delegation.

The two adjacent P1 theorems in the same file pin the boundary cases: empty_scope_monotonicity (the empty scope is a subset of any parent) and scope_budgets_nonnegative (every explicit invocation budget is non-negative because budgets are Nat). All three carry claimClass: bounded_model in formal/theorem-inventory.json and are root-imported via Chio.lean.

The Aeneas Extraction

The Aeneas production lane extracts a functional Lean model from crates/chio-kernel-core/src/formal_aeneas.rs. Of the fifteen extracted symbols listed in formal/aeneas/production.toml, the P1-relevant ones are optional_u32_cap_is_subset, required_true_is_preserved, and monetary_cap_is_subset_by_parts.

schema = "chio.aeneas-production.v1"
status = "production_extraction"
source = "crates/chio-kernel-core/src/formal_aeneas.rs"
command = "./scripts/check-aeneas-production.sh"
equivalence_command = "./scripts/check-aeneas-equivalence.sh"
equivalence_module = "formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean"

extracted_symbols = [
  "classify_time_window_code",
  "time_window_valid",
  "exact_or_wildcard_covers_by_flags",
  "prefix_wildcard_or_exact_covers_by_flags",
  "optional_u32_cap_is_subset",
  "required_true_is_preserved",
  "monetary_cap_is_subset_by_parts",
  "budget_precheck",
  "budget_commit",
  "dpop_freshness_valid",
  "dpop_admits",
  "nonce_admits",
  "guard_step_allows",
  "revocation_snapshot_denies",
  "receipt_fields_coupled",
]

The corresponding equivalence theorem in formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean:108 anchors the extracted optional_u32_cap_is_subset to its handwritten Lean counterpart and to the manifest's P1 row via the inventory id proof.aeneas_optionalCapIsSubset_preserves_parent_cap:

theorem aeneas_optionalCapIsSubset_preserves_parent_cap
    (childHasCap parentHasCap : Bool)
    (childValue parentValue : Nat)
    (h_subset :
      AeneasMirror.optionalCapIsSubset childHasCap childValue parentHasCap parentValue = true)
    (h_parent : parentHasCap = true) :
    childHasCap = true /\ childValue <= parentValue := by
  cases childHasCap <;> cases parentHasCap <;>
    simp [AeneasMirror.optionalCapIsSubset] at h_subset h_parent
  exact h_subset

The theorem reads: if the Aeneas-extracted optionalCapIsSubset accepts a (child, parent) pair and the parent has the cap set, then the child has the cap set and the child value is at or below the parent value. The proof is one tactic line: case-split on the two booleans and discharge each via simp on the unfolded Aeneas mirror definition.

Six other equivalence theorems in the same file pin the rest of the manifest's required Aeneas equivalences for P1 through P10: aeneas_monetaryCapIsSubset_preserves_parent_cap (P1, monetary axes), aeneas_revocationSnapshot_equiv_model (P2), aeneas_dpopAdmits_equiv_model (P8), aeneas_receiptCoupling_equiv_model (P4), and the boolean-coverage theorems for the wildcard and prefix matchers.

The gate at scripts/check-aeneas-equivalence.sh (1) confirms every expected symbol from production.toml appears as a def <name> in the generated target/formal/aeneas-production/lean/Funs.lean, (2) confirms BudgetCommitResult is inTypes.lean, (3) writes SHA-256 digests of the Rust source and the generated Lean files to target/formal/aeneas-production/equivalence-artifacts.json, and (4) elaborates Chio.Proofs.AeneasEquivalence via lake build. A clean run prints Aeneas equivalence gate passed.

The Kani Harness

The Kani public lane symbolically checks the same property on the production normalized AST. The harness for P1 is verify_delegation_chain_step at crates/chio-kernel-core/src/kani_public_harnesses.rs:505. The MAPPING.md row pins it 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; it discharges P1, P3, and P5.

The harness drives 22 symbolic axes through one_step_attenuation_predicate and asserts five distinct facts. The opening axis declarations and the load-bearing predicate call:

#[kani::proof]
fn verify_delegation_chain_step() {
    // Symbolic axes for the parent/child grant pair produced by one
    // delegation step. Caps are bounded to u8 ranges to keep the search
    // space aligned with the rest of this module.
    let server_parent_is_wildcard = kani::any::<bool>();
    let server_parent_equals_child = kani::any::<bool>();
    let tool_parent_is_wildcard = kani::any::<bool>();
    let tool_parent_equals_child = kani::any::<bool>();
    let operations_child_subset = kani::any::<bool>();
    let constraints_child_superset = kani::any::<bool>();
    let parent_has_inv_cap = kani::any::<bool>();
    let parent_inv_cap = u32::from(kani::any::<u8>());
    let child_has_inv_cap = kani::any::<bool>();
    let child_inv_cap = u32::from(kani::any::<u8>());
    // ... (per-call cost, total cost, dpop axes elided) ...
    let attenuates = one_step_attenuation_predicate(
        server_parent_is_wildcard,
        server_parent_equals_child,
        tool_parent_is_wildcard,
        tool_parent_equals_child,
        operations_child_subset,
        constraints_child_superset,
        parent_has_inv_cap,
        parent_inv_cap,
        child_has_inv_cap,
        child_inv_cap,
        // ... ten more axes elided ...
    );

The harness then asserts five facts. Quoted from the same file:

// (1) Reflexivity: a step that does not change anything is a valid
//     attenuation.
let reflexive = one_step_attenuation_predicate(/* child = parent */);
assert!(reflexive);

// (2) Scope-side rejection: if the predicate accepts the step, then
//     every constituent must hold (no widening on any axis).
if attenuates {
    assert!(server_parent_is_wildcard || server_parent_equals_child);
    assert!(tool_parent_is_wildcard || tool_parent_equals_child);
    assert!(operations_child_subset);
    assert!(constraints_child_superset);
    assert!(!parent_has_inv_cap || (child_has_inv_cap && child_inv_cap <= parent_inv_cap));
    // ... per-call, total-cost, dpop assertions elided ...
}

// (3) Strict-widening rejection witnesses: dropping a parent invocation
//     cap or flipping dpop_required to false drives the predicate to
//     false.
let widen_inv_unbounded = /* parent has cap, child drops cap */;
assert!(!widen_inv_unbounded);
let widen_dpop = /* parent dpop required, child drops dpop */;
assert!(!widen_dpop);

// (4) Expiry monotonicity: child_expires_at <= parent_expires_at and
//     time_window_valid(now, issued_at, child_expires_at) implies
//     time_window_valid(now, issued_at, parent_expires_at).
kani::assume(child_expires_at <= parent_expires_at);
let parent_valid = time_window_valid(now, issued_at, parent_expires_at);
let child_valid = time_window_valid(now, issued_at, child_expires_at);
if child_valid {
    assert!(parent_valid);
}

// (5) Bind the synthetic predicate to runtime subset wiring: build two
//     NormalizedToolGrants from the symbolic axes and assert the
//     production NormalizedToolGrant::is_subset_of agrees.

Step 5 is the load-bearing one for P1 on production code. Without it a regression that flipped a subset check from parent.contains(child) to child.contains(parent) on the constraint axis would not show up in the synthetic predicate and the harness would still pass. Step 5 makes the production NormalizedToolGrant::is_subset_of and the synthetic predicate agree on every accepted step.

Wall clock per the timing block at formal/rust-verification/kani-public-harnesses.toml:47-62: 1 second on cargo-kani 0.67.0, hot cache, aarch64-apple-darwin. The bound --default-unwind 8 is enough because every loop in the harness is fixed-shape; the symbolic state space comes from the bool and u8-widened-to-u32 slots, not from loop iterations.

Three sibling Kani harnesses also discharge P1's axes: verify_scope_intersection_associative (transitivity of optional-cap subset), public_normalized_scope_subset_rejects_widened_child, and public_normalized_scope_subset_rejects_value_widened_child.

The Differential Test

The differential lane runs the reference spec at formal/diff-tests/src/spec.rs against the production Rust on randomly generated input pairs. The reference spec reimplements the subset logic without calling into chio_core, so a drift between spec and impl produces a divergent verdict.

From formal/diff-tests/tests/scope_diff.rs the headline P1 test:

/// Core differential test: scope subset produces the same result in
/// spec and impl.
#[test]
fn scope_subset_spec_matches_impl(
    ((spec_a, impl_a), (spec_b, impl_b)) in arb_paired_scope_pair()
) {
    let spec_result = spec_a.is_subset_of(&spec_b);
    let impl_result = impl_a.is_subset_of(&impl_b);

    prop_assert_eq!(
        spec_result, impl_result,
        "Scope subset mismatch!\n  spec: {}\n  impl: {}\n  child grants: {}\n  parent grants: {}",
        spec_result, impl_result, spec_a.grants.len(), spec_b.grants.len()
    );
}

The same file ships the bounded P1-shaped invariants that proptest generates inputs for directly, so a regression that breaks one of the algebraic facts also surfaces as a property violation:

/// P1: Empty scope is a subset of any scope.
#[test]
fn empty_scope_is_subset(scope in arb_spec_scope()) { /* ... */ }

/// P3: Removing a grant from a scope produces a subset.
#[test]
fn remove_grant_is_subset(scope in arb_spec_scope(), idx in any::<usize>()) { /* ... */ }

/// P5: Reducing max_invocations produces a subset.
#[test]
fn reduce_budget_is_subset(grant in arb_spec_tool_grant()) { /* ... */ }

/// P6: Wildcard tool name subsumes any specific tool name.
#[test]
fn wildcard_subsumes(server_idx in 0usize..10, tool_idx in 0usize..10) { /* ... */ }

/// P8: Monotonicity -- child <= parent <= grandparent implies child <=
///     grandparent (transitivity).
#[test]
fn subset_transitivity(scope in arb_spec_scope()) { /* ... */ }

Default sample count is 256 per property; override via PROPTEST_CASES. On a divergence, proptest shrinks toward a minimal failing input and writes a regression seed under formal/diff-tests/proptest-regressions/ so subsequent runs replay that seed first.

The arb_paired_scope_pair generator produces two structurally identical values, one as a SpecChioScope and one as a production chio_core::capability::ChioScope; the matched pair drives spec and impl through the same input without any conversion gap. The same crate ships normalized variants that target NormalizedScope::is_subset_of in chio-kernel-core, so every layer of the production capability AST gets exercised.

What This Tour Proves and What It Does Not

Honest accounting of what the five lanes together establish:

• Lean 4 proof. capability_monotonicity is a theorem about the bounded Lean model of capability scopes. It says: under the Lean definition of isSubsetOf, every accepted child has a parent witness. The Lean kernel type-checked the proof; the placeholder scan in scripts/check-formal-proofs.sh confirms no sorry ships.
• Aeneas equivalence. aeneas_optionalCapIsSubset_preserves_parent_cap says: the function the Aeneas pipeline extracted from formal_aeneas.rs implements the same boolean predicate as the handwritten Lean mirror. The extraction gate fixes the SHA-256 of the Rust source so a silent edit that changes the extraction is observable.
• Kani harness. verify_delegation_chain_step says: across the bounded symbolic state space (22 axes, unwind 8), every accepted attenuation step satisfies the no-widening predicate axis-by-axis, and the production NormalizedToolGrant::is_subset_of agrees with the synthetic predicate on accepted steps. The symbolic state size is large enough to exercise every branch but small enough to terminate in 1 second.
• Differential test. scope_subset_spec_matches_impl says: on 256 randomly generated input pairs (configurable), the reference spec and the production impl agree on the subset verdict. Plus five property-shaped tests for the bounded P1 algebra (empty, transitivity, reduce-budget, wildcard, removed-grant).
• TLA+ invariant. AttenuationPreserving says: across the cross-authority protocol, depth stays in the bounded range and any attenuated capability has been delegated at least once. Apalache discharges this on the safety lane to length 16.

What the tour does not prove:

• The Lean theorem is over a bounded Lean model. It does not witness the Rust binary running on a real CPU. The Aeneas equivalence and the Kani harness narrow the gap; the differential test exercises actual Rust on random inputs; the TLA+ invariant pins the protocol shape. Together they cover the decision surface, not the entire kernel.
• P1 is proven about ChioScope::is_subset_of and NormalizedScope::is_subset_of. It is not proven about every place in the kernel that calls those functions; the adapter no-bypass gate at scripts/check-adapter-no-bypass.sh fails the build if any protocol adapter sidesteps the kernel's evaluate path, but that is a structural check, not a property proof.
• Side channels are out of scope for the Lean and Kani lanes. Timing leaks on the byte-equality path are covered separately by the dudect harnesses at crates/chio-kernel-core/tests/dudect/. Power and electromagnetic side channels are not covered.
• Concrete Ed25519, SHA-256, canonical JSON, TLS, OS clock, SQLite, chain, and hosted-registry implementations are audited assumptions, not proven. See Assumptions and TCB.

Run P1 End to End

The five P1-touching gates, in order:

# Lean root build: includes Chio.Spec.capability_monotonicity
./scripts/check-formal-proofs.sh

# Aeneas extraction: writes target/formal/aeneas-production/lean/Funs.lean
./scripts/check-aeneas-production.sh

# Aeneas-Lean equivalence: elaborates Chio.Proofs.AeneasEquivalence
./scripts/check-aeneas-equivalence.sh

# Kani public lane: includes verify_delegation_chain_step
./scripts/check-kani-public-core.sh

# Differential tests: includes scope_subset_spec_matches_impl
cargo test -p chio-formal-diff-tests

And the TLA+ safety lane separately, since Apalache wall clock runs in hours:

apalache check \
  --inv=SafetyInv \
  --config=formal/tla/MCRevocationPropagation.cfg \
  formal/tla/RevocationPropagation.tla

Where to Go Next

• Theorem Inventory · the per-theorem table including every P1 supporting lemma and its claim class.
• Lean 4 Proofs · the file-by-file proof structure and the build flow.
• Aeneas Pipeline · the extraction pipeline plus the rest of the equivalence theorems.
• Kani Harnesses · the full inventory of public Kani harnesses and per-harness wall clocks.
• Differential Tests · the proptest generators and the per-property test layout.
• TLA+ Specs · the cross-authority protocol model and the Apalache lanes.
• Failure Modes · what happens when a P1 gate fails and how to triage.