Creusot Contracts

What Creusot Does

A function annotated with #[requires(..)] and #[ensures(..)] is lowered to a Why3 verification condition; chio's harness, configured in why3find.json, dispatches it to whichever of four pinned SMT backends can discharge it: alt-ergo, z3, cvc5, and cvc4. Specifications are written in Pearlite, Creusot's specification language embedded in Rust attributes. The @ suffix visible below (now@, result@) projects a Rust integer onto its logical view, a mathematical integer with no wraparound, so a spec can write remaining@ - cost@ without the runtime type's finite width getting in the way. Having no extraction step means there is nothing to keep in sync the way Aeneas's equivalence theorems keep an extracted Lean model in sync with handwritten Lean; the obligation is stated about the exact function annotated. But that guarantee is only as good as which function gets annotated, and Chio's seven are not the production entry points; they are a hand-mirrored twin of them, as the coverage section below shows.

How It's Wired

The manifest is formal/rust-verification/creusot-contracts.toml, schema chio.creusot-contracts.v1, status core_contracts_required_for_strict_ci. Its covered_symbols array concatenates eleven production chio_kernel_core symbols with six contract-function names prefixed by the crate that holds them:

schema = "chio.creusot-contracts.v1"
status = "core_contracts_required_for_strict_ci"
owner = "formal-verification"
strict_smoke_command = "./scripts/check-creusot-smoke.sh"
strict_core_command = "./scripts/check-creusot-core.sh"

covered_symbols = [
  "chio_kernel_core::capability_verify::verify_capability",
  "chio_kernel_core::evaluate::evaluate",
  "chio_kernel_core::receipts::sign_receipt",
  "chio_kernel_core::normalized::NormalizedScope::is_subset_of",
  # ... 7 more: verify_capability_with_trusted, both resolve_*_grants
  # helpers, three more Normalized*Grant variants, and
  # NormalizedEvaluationVerdict::try_from_evaluation.
  "formal/rust-verification/creusot-core::time_window_valid_contract",
  # ... plus five more "creusot-core::*_contract" entries, one short
  # of the seven contract functions in lib.rs below.
]

contract_goals = [
  # ... five goal statements, then, verbatim:
  "proof-facing Creusot wrappers verify pure branch conditions shared with chio-kernel-core::formal_core",
]

Shared, not identical, a distinction the coverage table below specifies. The seven annotations themselves live in a second crate, deliberately isolated from the rest of chio. Its Cargo.toml declares its own empty [workspace], outside chio's main workspace, with one dependency, creusot-std, pinned to a git revision, so the pinned Creusot toolchain only ever compiles this small crate instead of Chio's full dependency graph. The crate's functions are shown below:

use creusot_std::prelude::*;

#[ensures(result == (issued_at@ <= now@ && now@ < expires_at@))]
pub fn time_window_valid_contract(now: u64, issued_at: u64, expires_at: u64) -> bool {
    issued_at <= now && now < expires_at
}

#[requires(cost@ <= remaining@)]
#[ensures(result@ == remaining@ - cost@)]
#[ensures(result@ <= remaining@)]
pub fn budget_commit_remaining_contract(remaining: u64, cost: u64) -> u64 {
    remaining - cost
}

#[ensures(result == (!parent_has_cap || (child_has_cap && child_value@ <= parent_value@)))]
pub fn optional_u32_cap_subset_contract(
    child_has_cap: bool,
    child_value: u32,
    parent_has_cap: bool,
    parent_value: u32,
) -> bool {
    !parent_has_cap || (child_has_cap && child_value <= parent_value)
}

#[ensures(result == (!parent_requires_true || child_requires_true))]
pub fn required_true_preserved_contract(
    parent_requires_true: bool,
    child_requires_true: bool,
) -> bool {
    !parent_requires_true || child_requires_true
}

#[ensures(result == (!dpop_required || (proof_present && proof_valid && nonce_fresh)))]
pub fn dpop_admits_contract(
    dpop_required: bool,
    proof_present: bool,
    proof_valid: bool,
    nonce_fresh: bool,
) -> bool {
    !dpop_required || (proof_present && proof_valid && nonce_fresh)
}

#[ensures(result == (token_revoked || ancestor_revoked))]
pub fn revocation_snapshot_denies_contract(token_revoked: bool, ancestor_revoked: bool) -> bool {
    token_revoked || ancestor_revoked
}

#[ensures(result == (
    capability_matches
        && request_matches
        && verdict_matches
        && policy_hash_matches
        && evidence_class_matches
))]
pub fn receipt_fields_coupled_contract(
    capability_matches: bool,
    request_matches: bool,
    verdict_matches: bool,
    policy_hash_matches: bool,
    evidence_class_matches: bool,
) -> bool {
    capability_matches
        && request_matches
        && verdict_matches
        && policy_hash_matches
        && evidence_class_matches
}

Two gate scripts run against it. check-creusot-smoke.sh is a toolchain canary: it scaffolds a disposable cargo creusot new project pinned to the same revision and proves it, showing nothing about chio's logic, only that the toolchain still works. check-creusot-core.sh runs the contract proof inside creusot-core itself. Both fold into ./scripts/check-rust-verification-gates.sh, which also validates both Kani tomls and, unless CHIO_RUST_VERIFICATION_METADATA_ONLY=1 is set, requires both toolchains before running the checks. The manifest lists creusot in its top-level primary_toolchain array alongside lean4, kani, and aeneas, and marks its lane required, the same tier as both Kani lanes; Aeneas, by contrast, splits into separate pilot and production tiers.

What It Covers

Each contract carries a single #[ensures] (one also a #[requires]) and mirrors a helper in chio-kernel-core::formal_core, the same pure branch-logic hub Aeneas extracts and Kani symbolically executes:

The table has three documented gaps. covered_symbols names six of these seven contracts; revocation_snapshot_denies_contract exists and is proved but is absent from the array, and nothing mechanically checks the crate and the toml against each other. Only three of the seven twins are called from production code at all, by capability_verify.rs (time window) and normalized.rs (the two subset flags); the other four are not imported by evaluate.rs or receipts.rs, and formal_core.rs itself carries a blanket #![allow(dead_code)] consistent with that. And the eleven production symbols named alongside these contracts (verify_capability, evaluate, sign_receipt, the Normalized*Grant::is_subset_of family) correspond to these contracts only by shared branch logic: chio-kernel-core has no Creusot dependency, and none of those files carry a single #[requires]/#[ensures] themselves. The correspondence is upheld by hand, keeping formal_core.rs and creusot-core/src/lib.rs in the same shape. Lean's Core/Scope.lean carries Mirrors: comments rather than being generated. Five of the seven bodies are shape-identical to their twin, and the time-window and budget contracts restate their twin's logic in a different shape. No mechanical equivalence check relates this mirror crate to the production functions.

Relation to Other Evidence

Chio runs six evidence lanes: Lean 4, Aeneas, Creusot, Kani, TLA+ with Apalache, and differential tests (see Formal Assurance Overview for the complete map). Creusot and Kani are the two lanes the manifest marks required for Rust refinement specifically, and the four that touch formal_core.rs touch it differently: Aeneas mechanically extracts the file via Charon into Lean, checked by explicit equivalence theorems; Kani's public harnesses live inside chio-kernel-core and symbolically execute the mirrored functions up to a bounded unwind; Lean hand-writes an independent model in a different logic entirely; Creusot proves deductive contracts over a hand-mirrored twin in its own isolated crate. This is the most indirect link to the running binary of the four. No lane establishes Chio's claims alone; the property matrix draws on more than one lane per property so no single lane's blind spot defines the claim.

Reproducing Locally

With cargo-creusot on PATH, run these two commands. Without it, the metadata check still validates the manifest's shape. Per-solver proof time is recorded in why3find.json; the pinned profile has all four backends closing chio's obligations in well under a second each (cvc5 0.473s, z3 0.165s, alt-ergo 0.232s, cvc4 0.506s).

# Schema and coverage check only, no toolchain required
CHIO_RUST_VERIFICATION_METADATA_ONLY=1 ./scripts/check-rust-verification-gates.sh

# Toolchain canary, then the real lane
./scripts/check-creusot-smoke.sh
./scripts/check-creusot-core.sh

Limits

• Hand-mirrored functions · seven contract functions in an isolated crate, not annotations on chio-kernel-core itself, and the link between them rests on discipline, not a checked equivalence.
• A known registry gap · covered_symbols names six of the seven contract functions today.
• Not a per-PR gate · the strict lane runs nightly and again at release-qualification, not on every pull request.
• Four of seven twins are unwired · budget_commit, dpop_admits, revocation_snapshot_denies, and receipt_fields_coupled are not called anywhere else in chio-kernel-core.
• Cryptography remains assumed · none of these contracts touch Ed25519 or SHA-256; see Assumptions and TCB.
• Contracts, not the binary · a green run proves the seven annotated functions satisfy their contracts, nothing about the kernel binary as a whole.

Next

• Aeneas Pipeline · the extraction lane Creusot deliberately has no equivalent of.
• Kani Harnesses · the other required strict-CI Rust refinement lane.
• Assumptions and TCB · what stays audited underneath every proof lane, including this one.