P1 Tour

The evidence P1 carries

Each row of the property matrix is id|name|evidence kinds|proof ids, and the evidence field is the whole of what a property claims. The matrix assigns no order to the kinds, so the table below is the matrix order and not a ranking. The TLA+ invariant discussed further down is a model of the cross-authority protocol; the matrix does not list a TLA evidence kind for P1.

The lanes target different objects. lean_root_imported proves statements about a Lean model; differential_test runs the production Rust against a separately written reference on generated inputs. The manifest scopes the two directions against each other at formal/proof-manifest.toml:238: Lean assets are release evidence only when root-imported, sorry-free and mapped to a property row, while :239 records Creusot and Kani as the required strict-CI lanes for production implementation linkage.

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. The verification path rejects rewrites that widen an evaluated axis.

The cross-reference is crates/core/chio-core-types/src/capability/scope.rs in ChioScope::is_subset_of and crates/kernel/chio-kernel-core/src/normalized.rs in NormalizedScope::is_subset_of. Both functions return false for rewrites that widen an evaluated axis. The adapter check requires protocol adapters to 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 has been delegated at least once. formal/MAPPING.md:55 pins it to four Rust call sites: ChioScope::is_subset_of, NormalizedScope::is_subset_of, validate_delegation_chain in capability/attenuation.rs, and ChioKernel::validate_delegation_admission. The same row records the assumption column as n/a (structural; bounded by DEPTH_MAX), so the bound is a model parameter and not an entry in the audited assumption registry.

Apalache does not check AttenuationPreserving on its own. The PR safety lane checks the six-way conjunction SafetyInv, which the spec defines as:

SafetyInv ==
    /\ DomainsOK
    /\ NoAllowAfterRevoke
    /\ MonotoneLog
    /\ AttenuationPreserving
    /\ RevocationFreshness
    /\ RevocationStateCoupled

A counterexample to any one conjunct fails the whole invariant, so a clean run reports all six and attributes the result to none of them individually. The lane runs to computation length 6 with the model config at formal/tla/MCRevocationPropagation.cfg, whose own INVARIANT SafetyInv line selects it.

The Lean 4 proof

The P1 Lean theorem is Chio.Spec.capability_monotonicity in formal/lean4/Chio/Chio/Spec/Properties.lean. It is the first proof id in P1's matrix row, where it appears as 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) :
    ∀ 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 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 matrix row names 6 proof ids for P1, and formal/theorem-inventory.json resolves each to a Lean name and a file:

Every one is rootImported: true, which is what makes it release evidence under the manifest note at formal/proof-manifest.toml:238. None of the six carries an explicit status field; the inventory writes one only where it has something to say, and reserves assumed for its single axiom entry.

Two further theorems in Spec/Properties.lean map to P1 without being cited in the matrix row: 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). Two more sit in Proofs/Monotonicity.lean alongside the cited three: wildcard_subsumes, which maps to P1, and delegation_chain_integrity, which the inventory maps to P5 rather than P1 and which P5's own matrix row cites.

The Aeneas extraction

The Aeneas production lane extracts a functional Lean model from two registered Rust sources, the first of which is crates/kernel/chio-kernel-core/src/formal_aeneas.rs. The registry header names the module that carries the equivalence theorems and the snapshot the extraction is compared against:

schema = "chio.aeneas-production.v1"
status = "generated_equivalence"
owner = "formal-verification"
source = "crates/kernel/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/AeneasGeneratedEquivalence.lean"
artifact_report = "target/formal/aeneas-production/equivalence-artifacts.json"
negative_registry = "formal/aeneas/negative-tests.toml"
vendor_manifest = "formal/lean4/vendor/aeneas/VENDOR.toml"
vendor_release_tag = "build-2026.04.22.215158-38d10a22642d75d051e14006cc6e45055381f10e"
snapshot_layout = "emitted_module_path"
snapshot_normalization = "identity"
generated_snapshot = [
  "formal/lean4/Chio/FormalAeneas/Funs.lean",
  "formal/lean4/Chio/FormalAeneas/Types.lean",
]

The equivalence module is Proofs/AeneasGeneratedEquivalence.lean, and the registry's status is generated_equivalence. The symbols are declared per target rather than in one flat list; the target that carries P1 is decision_core, which pairs every extracted function with a named theorem:

name = "decision_core"
source = "kernel_core"
status = "generated_equivalence"
types = [
  "BudgetCommitResult",
]
functions = [
  "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",
]
equivalence_theorems = [
  "classify_time_window_code|Chio.Proofs.generated_classify_time_window_code_eq_mirror",
  "time_window_valid|Chio.Proofs.generated_time_window_valid_eq_mirror",
  "exact_or_wildcard_covers_by_flags|Chio.Proofs.generated_exact_or_wildcard_covers_by_flags_eq_mirror",
  "prefix_wildcard_or_exact_covers_by_flags|Chio.Proofs.generated_prefix_wildcard_or_exact_covers_by_flags_eq_mirror",
  "optional_u32_cap_is_subset|Chio.Proofs.generated_optional_u32_cap_is_subset_eq_mirror",
  "required_true_is_preserved|Chio.Proofs.generated_required_true_is_preserved_eq_mirror",
  "monetary_cap_is_subset_by_parts|Chio.Proofs.generated_monetary_cap_is_subset_by_parts_eq_mirror",
  "budget_precheck|Chio.Proofs.generated_budget_precheck_eq_mirror",
  "budget_commit|Chio.Proofs.generated_budget_commit_eq_mirror",
  "dpop_freshness_valid|Chio.Proofs.generated_dpop_freshness_valid_eq_mirror",
  "dpop_admits|Chio.Proofs.generated_dpop_admits_eq_mirror",
  "nonce_admits|Chio.Proofs.generated_nonce_admits_eq_mirror",
  "guard_step_allows|Chio.Proofs.generated_guard_step_allows_eq_mirror",
  "revocation_snapshot_denies|Chio.Proofs.generated_revocation_snapshot_denies_eq_mirror",
  "receipt_fields_coupled|Chio.Proofs.generated_receipt_fields_coupled_eq_mirror",

Three of those functions carry P1 weight: optional_u32_cap_is_subset (invocation cap), monetary_cap_is_subset_by_parts (cost caps), and required_true_is_preserved (the DPoP-required flag). The theorem P1's matrix row actually cites is proof.generated_optional_u32_cap_is_subset_preserves_parent_cap, which is stated over the generated Chio.AeneasProduction definition rather than over a handwritten mirror:

theorem generated_optional_u32_cap_is_subset_preserves_parent_cap
    (childHasCap parentHasCap : Bool)
    (childValue parentValue : U32)
    (subsetGenerated :
      Chio.AeneasProduction.optional_u32_cap_is_subset
        childHasCap childValue parentHasCap parentValue = ok true)
    (parentPresent : parentHasCap = true) :
    childHasCap = true ∧ childValue.val <= parentValue.val := by
  rw [generated_optional_u32_cap_is_subset_eq_mirror] at subsetGenerated
  injection subsetGenerated with subsetMirror
  exact aeneas_optionalCapIsSubset_preserves_parent_cap
    childHasCap parentHasCap childValue.val parentValue.val subsetMirror parentPresent

The theorem reads: if the generated optional_u32_cap_is_subset returns ok true for 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 rewrites through the generated-to-mirror equality and then applies the handwritten bridge aeneas_optionalCapIsSubset_preserves_parent_cap in Proofs/AeneasEquivalence.lean. The inventory records that relationship in its own words: the handwritten bridge is a Derived ordinary-value attenuation bridge and the generated theorem is its generated-code successor.

The scope of the lane is narrower than the module is wide. Proofs/AeneasEquivalence.lean declares fourteen theorems and the inventory registers seven of them; the seven cover P1, P2, P3, P4 and P8, one each except for P3, which takes three. The seven unregistered ones, including the monetary-cap counterpart aeneas_monetaryCapIsSubset_preserves_parent_cap, elaborate in the same build but are cited by no property row.

Two gates run this lane. scripts/check-aeneas-production.sh drives Charon and Aeneas over each registered source and then requires every function in the target to appear as a def <name> in the generated Funs.lean and every registered type as a structure <name> in Types.lean (check-aeneas-production.sh:294-301). It ends by calling scripts/check-aeneas-equivalence.sh, which checks the vendored Aeneas digest against formal/lean4/vendor/aeneas/VENDOR.toml, requires every equivalence_theorems row to resolve to a declared theorem carrying a #print axioms report, requires the module to be root-imported exactly once from Chio.lean, then elaborates Chio.Proofs.AeneasGeneratedEquivalence and fails on any sorryAx in the log. A clean run prints Aeneas generated equivalence gate passed (check-aeneas-equivalence.sh:346).

The Kani harness

The Kani public lane checks a bounded symbolic model of the same attenuation step. The harness is verify_delegation_chain_step in crates/kernel/chio-kernel-core/src/kani_public_harnesses.rs, and formal/MAPPING.md:304 pins it to optional_u32_cap_is_subset, monetary_cap_is_subset_by_parts, required_true_is_preserved and time_window_valid in chio_kernel_core::formal_core.

The harness draws 22 symbolic axes and passes all 22 to one_step_attenuation_predicate, a pure conjunction over identity coverage, operations subset, constraints superset, the three cap-subset checks and DPoP preservation. It then discharges five numbered groups of assertions:

• Reflexivity. A step where the child equals the parent on every axis satisfies the predicate.
• Scope-side rejection. If the predicate accepts, every constituent leg holds, so no axis widened.
• Strict-widening witnesses. One axis at a time, a widened child drives the predicate to false.
• Expiry monotonicity. A single step may not lengthen the validity window; a child valid at now implies its parent is.
• Runtime binding. Two NormalizedToolGrant values built from the same symbolic axes are run through the production NormalizedToolGrant::is_subset_of, which must agree with the synthetic predicate.

The fifth group is what binds the synthetic predicate to shipped code. Without it, a regression that flipped a subset check from parent.contains(child) to child.contains(parent) on the constraint axis would leave the synthetic predicate untouched and the harness would still pass.

The lane runs at --default-unwind 8, which scripts/check-kani-public-core.sh:216-222 applies to every harness in the lane. That bound is enough here because the loops in this harness are fixed-shape; the symbolic state comes from the bool and u8-widened slots, not from loop iterations.

Three sibling harnesses in the same lane cover neighbouring P1 shapes: verify_scope_intersection_associative (transitivity and reflexivity of optional_u32_cap_is_subset), public_normalized_scope_subset_rejects_widened_child and public_normalized_scope_subset_rejects_value_widened_child. The second of those is quoted in full on the Kani harnesses page.

The differential test

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

The headline P1 test sits inside a proptest! block in formal/diff-tests/tests/scope_diff.rs, which is what makes the in arb_paired_scope_pair() argument syntax legal:

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 arb_paired_scope_pair generator produces two structurally identical values, one as a SpecChioScope and one as a production chio_core::capability::ChioScope, so the two implementations see the same input with no conversion gap. The default sample count is 256 per property, read from PROPTEST_CASES at scope_diff.rs:28-42. On a divergence proptest shrinks toward a minimal failing input and writes a seed to a tests/<name>.proptest-regressions file beside the test. One such file is committed today, for canonical_json_diff.

The same file pins eight attenuation rules as standalone properties at scope_diff.rs:632-811: the empty scope is a subset of any scope, subset is reflexive, removing a grant produces a subset, removing an operation produces a subset, reducing max_invocations produces a subset, a wildcard tool name subsumes any specific one, different servers never produce a subset, and subset is transitive across a grandparent chain. These are asserted on the spec side alone, so they catch the reference drifting from its own intent while the _spec_matches_impl properties catch the two sides drifting apart.

The crate also ships normalized variants that target NormalizedScope::is_subset_of in chio-kernel-core, so the generated inputs exercise both production capability-AST layers rather than only the outer one.

What the tour establishes and what it does not

What each of P1's five evidence kinds actually says:

• lean_root_imported. capability_monotonicity is a theorem about the Lean model of capability scopes: under the Lean definition of isSubsetOf, every accepted child grant has a parent witness. The Lean kernel type-checked it, and the placeholder scan in scripts/check-formal-proofs.sh:22-40 fails the gate on a literal sorry anywhere in the shipped modules. Its claim class in the inventory is bounded_model.
• aeneas_equivalence. generated_optional_u32_cap_is_subset_preserves_parent_cap says the function Aeneas extracted from formal_aeneas.rs has the attenuation property, stated over the generated definition rather than a transcription of it. The gate pins the SHA-256 of the Rust source and of the generated Lean, so an edit that changes the extraction is observable.
• public_kani. verify_delegation_chain_step says that over its bounded symbolic state space, 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. Kani is a bounded model checker, so a clean run means no counterexample within those bounds.
• differential_test. scope_subset_spec_matches_impl says the reference spec and the production implementation agree on the subset verdict for the inputs drawn. Agreement is not correctness: a bug shared by both sides passes.
• rust_projection. P1 is the only property whose row names this kind. It covers the scalar projection functions the production backends call, which is why covered_rust_symbols lists the chio_kernel_core::normalized::*::is_subset_of family alongside formal_core helpers.

What none of the five establishes:

• The Lean theorem is over a Lean model. It does not witness the Rust binary running on a real CPU. The Aeneas equivalence and the Kani harness narrow that gap over the registered symbols; the differential test exercises the shipped Rust on generated inputs. Together they cover the decision surface, not the kernel.
• The property is stated about ChioScope::is_subset_of and NormalizedScope::is_subset_of, not about every kernel path that calls them. The gate at scripts/check-adapter-no-bypass.sh fails the build if a protocol adapter sidesteps the kernel evaluate path, which is a structural check rather than a property proof.
• The TLA+ side is a model of the cross-authority protocol, and the property matrix does not list a TLA evidence kind for P1 at all. AttenuationPreserving bounds delegation depth inside 0..DEPTH_MAX in that model; it is a conjunct of an aggregate invariant, not a per-property gate.
• Side channels are outside the Lean and Kani lanes. Timing on the byte-equality path is covered separately by the dudect harnesses at crates/kernel/chio-kernel-core/tests/dudect/. Power and electromagnetic side channels are covered by nothing here.
• Concrete Ed25519, SHA-256, canonical JSON, TLS, OS clock, SQLite, chain and hosted-registry implementations are audited assumptions. The manifest lists them first in excluded_surfaces. See Assumptions and TCB.

Reproduce

Every command below is a gate_commands entry in formal/proof-manifest.toml, run from the source root:

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

# Aeneas extraction, then the generated-equivalence gate it calls
./scripts/check-aeneas-production.sh

# The generated-equivalence gate on its own
./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

The last of those is the only one that runs on a bare Rust toolchain. The others need Lean and lake, the pinned Charon and Aeneas binaries, and cargo-kani respectively; each script checks for its own toolchain and exits with a message naming what is missing. scripts/check-kani-public-core.sh --list prints the lane's harness names without invoking Kani.

The Apalache safety lane is separate, because its shard budget is measured in hours. The gate wrapper is:

./scripts/check-apalache-positive.sh   --invariant SafetyInv   --length 6   --timeout-seconds 10800   --config formal/tla/MCRevocationPropagation.cfg   formal/tla/RevocationPropagation.tla

Those arguments are the revocation-propagation row of the safety matrix in .github/workflows/apalache-safety.yml:150-155. For an invariant run the wrapper does not pass the name through to apalache-mc; the checker takes it from the config file's own INVARIANT SafetyInv line, and the wrapper uses --invariant to validate the run's evidence afterwards.

See also

• Theorem Inventory · the per-theorem table including P1 supporting lemmas 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 public Kani-harness inventory 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.