P1: Capability Monotonicity

One uncovered grant rejects the whole child scope

The parent holds one grant: invoke on any tool at server example. A child can select hello_world or search from that authority. The tool wildcard adds no operation, so a hello_world delegate grant has no parent witness.

The predicate asks the same question of every child grant, and one parent grant can cover several. One uncovered grant fails the whole proposed scope; the predicate never drops it and approves the rest. The same rule decides each change below in the Lean grant model:

Removing the delegate grant makes this child scope pass. The predicate is one step of issuance and use, beside the identity, signature, validity, and delegation checks in Capabilities. Coverage is decided grant by grant; whether several accepted child grants fit one shared spending ledger is budget conservation, held by the reservations in Budgets & Metering.

The theorem turns acceptance into a witness for every child grant

The premise is that child.isSubsetOf parent returns true. The conclusion is that every grant in the child has a covering grant in the parent.

Here $\sqsubseteq$ reads isSubsetOf returning true, on scopes at the left and on single grants at the right. The proof unfolds the predicate and reads its all over the child against any over the parent:

/-- 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 scope quantifies over Lean lists with Nat invocation caps. The inventory's bounded_model label describes this modeling scope and sets no maximum list length or numeric bound on the statement.

The model's ToolGrant checks exact server identity, wildcard-or-exact tool coverage, operation membership, retained constraints, and invocation caps. Monetary caps, DPoP requirements, resource grants, and prompt grants sit outside it, and the inventory entry records the theorem without a full Rust refinement proof. The implementation evidence follows.

import Chio.Spec.Properties
open Chio.Core

def grant (tool : String)
    (operation : Operation) :
    ToolGrant :=
  { serverId := "example",
    toolName := tool,
    operations := [operation],
    constraints := [],
    maxInvocations := none }

def parent : ChioScope :=
  { grants := [grant "*" .invoke] }
def allowed : ChioScope :=
  { grants := [
      grant "hello_world" .invoke,
      grant "search" .invoke] }
def widened : ChioScope :=
  { grants := allowed.grants ++
      [grant "hello_world" .delegate] }

example :
    allowed.isSubsetOf parent = true :=
  by decide
example :
    widened.isSubsetOf parent = false :=
  by decide

Extraction ties the invocation-cap rule to compiled Rust decisions

The P1 row in the proof manifest registers five evidence kinds. Registration supplies the navigation; each kind reasons about its own object:

• lean_root_imported. Named Lean statements over modeled scopes. Check the premise, conclusion, imports, and assumption audit at the revision you cite.
• rust_projection. Pure scalar predicates used by Rust authority checks. Check which callers use the predicate and how they project their values.
• aeneas_equivalence. Generated Rust-to-Lean scalar functions and their equivalence theorems. Check authenticated extraction, generated definitions, machine-value projections, and theorem assumptions.
• public_kani. Registered bounded Rust harnesses. Check input restrictions, cfg(kani) branches, unwind settings, and completed verdicts.
• differential_test. Reference and Rust decisions on explicit and generated inputs. Check input generation, conversion, comparisons, and retained regression cases.

A rootImported flag is a registry declaration; a successful proof run and the assumptions it relies on make it evidence. The tightest implementation link is extraction. The scalar invocation-cap check isolates one authority rule: a capped parent must have a capped child whose value does not exceed it, and the production extraction registry maps optional_u32_cap_is_subset to generated Lean.

The generated theorem assumes the extracted computation returns ok true and the parent's cap is present, and concludes that the child cap is present and at or below the parent's. Its proof uses generated-to-mirror equality and an ordinary-value attenuation bridge, which binds this machine-value decision to the mathematical result more tightly than a handwritten model alone. The production gate authenticates its extraction toolchain and compares generated artifacts; the equivalence gate then builds and elaborates the named module.

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

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

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

Kani and differential tests check two different builds of the Rust comparison

The public Kani lane includes explicit scope rejection harnesses for a removed cap, widened values, and mismatched server identity, each with a deliberately constrained shape. Other registered harnesses exercise scalar attenuation and chain-step relationships. The harness source and public registry are part of the result: read the exact harness before taking its name as coverage of arbitrary scopes.

In NormalizedToolGrant::is_subset_of, cfg(kani) selects is_subset_of_bounded_kani. The ordinary runtime branch uses general iteration and the Kani branch uses bounded operation, constraint, and monetary helpers, so a harness calling the same public method runs a different function body. The registered runner's default unwind is 8, with unwinding checks enabled only for the exceptions the registry names, so a pass leaves loops beyond that bound unexplored. Keep that setting with the verdict; Failure Modes separates a property failure from insufficient unwinding.

The scope differential tests take the ordinary build. A separate reference specification runs against the public capability types and the normalized kernel representation, compiled natively. Explicit cases check caps, currencies, constraints, DPoP, and wildcard direction, and generated pairs exercise further comparisons, shrinking a divergent input when the property fails:

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 input generators and conversions define what the comparison sampled. A pass is a native test result for those inputs.

Four lanes carry P1, and the release records each one

The native scope comparison, the Lean gate, production extraction, and the public Kani lane all run before every release is tagged. The strict proof report records each lane's result against the tag's source commit. Check them for the binary you run:

chio release verify --evidence formal

binary     /usr/local/bin/chio  chio 0.2.0  aarch64-apple-darwin
checksum   matches SHA256SUMS for v0.2.0
signed by  release.yml on backbay-labs/chio, issuer token.actions.githubusercontent.com
provenance SLSA v1, 5 subjects, tag v0.2.0
formal     proof report bound to v0.2.0, every gate passed
           lean        root-imported theorems checked
           aeneas      production extraction and equivalence
           kani        public PR lane
           apalache    positive and negative invariants
           creusot     core contracts
           diff-tests  scope, canonical JSON, receipts, treaties
           timing      dudect threshold
verified

These lanes cover more than P1, and each line stands for its own object: a passing scope comparison leaves a failed or unexecuted Lean, extraction, or Kani lane incomplete, which is why the report binds all of them to one source. Verification Evidence explains the report, and Qualification: formal gates runs the four lanes from source.

Each result holds at its own boundary

The scope theorem gives every modeled child grant a parent witness when the modeled predicate accepts. The generated optional-cap theorem preserves an explicit parent cap for the accepted extracted computation under its stated premises. Kani and differential checks show that the executed harnesses or cases satisfy their assertions, within their input and build restrictions.

Signatures, chain verification, correct normalization, required mediation, and persistent accounting carry the evidence assigned to those boundaries, as do complete ChioScope refinement, the correctness of every caller, and durable spending conservation. The adapter no-bypass gate checks registered source structures and mediation contracts; an effect outside the mediation boundary is outside the theorem too.

The revocation-propagation model's AttenuationPreserving invariant is a separate claim. It checks that modeled delegation depth stays within DEPTH_MAX and that an attenuated capability has positive depth, comparing no tool grants, operations, or caps. It joins the model's other conditions in SafetyInv, its Apalache results apply to the selected model, constants, and computation length, and the P1 row registers no TLA evidence kind; TLA+ and Apalache carries that claim.

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

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

Next: follow another operating-system claim