Aeneas Pipeline

Aeneas is a translator from Rust to a pure functional model in a proof assistant. Chio runs two Aeneas lanes: a small pilot over hand-shaped reference functions in formal/aeneas/verified_core.rs, and a production extraction over the proof-facing helpers in crates/chio-kernel-core/src/formal_aeneas.rs. Both extract to Lean 4, paired with explicit equivalence theorems in Proofs/AeneasEquivalence.lean.

What Aeneas Does

Aeneas takes Rust source and produces a translation in a proof assistant. The translation drops effectful machinery (async, IO, unsafe blocks) and represents the remaining pure logic as functional definitions plus pre/postcondition propositions.

The toolchain is two-stage. Charon is a Rust front-end that emits a stable IR called LLBC. Aeneas then consumes LLBC and produces the proof-assistant output. Both are pinned in chio CI; the pilot's promotion criteria require the pin to move deliberately:

schema = "chio.aeneas-pilot.v1"
status = "active_pilot"
owner = "formal-verification"
source = "formal/aeneas/verified_core.rs"
check_command = "./scripts/check-aeneas-pilot.sh"

extracted_symbols = [
  "time_window_valid",
  "dpop_subset",
  "budget_precheck",
  "governed_approval_passes",
  "evaluate_signature_time_scope",
  "report_may_use_verified_label",
]

promotion_criteria = [
  "Charon and Aeneas versions are pinned together in CI",
  "Aeneas extracts the pure chio-kernel-core decision modules without unsupported Rust features",
  "Generated Lean imports are compared against the handwritten Chio.Core and Chio.Proofs modules",
  "Any missing external model is listed in formal/assumptions.toml or added as an Aeneas Lean model",
]

The Pilot Lane

The pilot extracts a handful of functions whose only purpose is to give Aeneas easy targets. The source is formal/aeneas/verified_core.rs: no external crates, no async, no unsafe, no heap allocation, no IO. This file mirrors the proof-facing shape of the chio decision helpers and is used as the first extraction lane before promoting to production crate modules.

The full pilot file is short:

pub enum Decision {
    Allow,
    Deny,
}

pub fn time_window_valid(now: u64, issued_at: u64, expires_at: u64) -> bool {
    issued_at <= now && now < expires_at
}

pub fn dpop_subset(parent_required: bool, child_required: bool) -> bool {
    !parent_required || child_required
}

pub fn budget_precheck(
    remaining_invocations: u64,
    remaining_units: u64,
    invocation_cost: u64,
    unit_cost: u64,
) -> bool {
    invocation_cost <= remaining_invocations && unit_cost <= remaining_units
}

pub fn governed_approval_passes(
    approval_required: bool,
    approval_token_valid: bool,
) -> bool {
    !approval_required || approval_token_valid
}

pub fn evaluate_signature_time_scope(
    signature_valid: bool,
    scope_match: bool,
    now: u64,
    issued_at: u64,
    expires_at: u64,
) -> Decision {
    if !signature_valid {
        Decision::Deny
    } else if !time_window_valid(now, issued_at, expires_at) {
        Decision::Deny
    } else if !scope_match {
        Decision::Deny
    } else {
        Decision::Allow
    }
}

pub fn report_may_use_verified_label(label: u8) -> bool {
    label == 2
}

The pilot is a load-bearing test of the pipeline itself. If Aeneas cannot extract these six functions cleanly, no production Rust will extract either. The check command is ./scripts/check-aeneas-pilot.sh.

The Production Lane

The production lane extracts from a real chio module. Source: crates/chio-kernel-core/src/formal_aeneas.rs. Configuration:

schema = "chio.aeneas-production.v1"
status = "production_extraction"
owner = "formal-verification"
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"
artifact_report = "target/formal/aeneas-production/equivalence-artifacts.json"

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

Fifteen extracted symbols cover the algebra surface chio cares about: time windows, scope coverage flags, optional caps, monetary caps, budget commits, DPoP nonce admission, guard step composition, revocation denial, and receipt field coupling.

End-to-End Pipeline

The end-to-end shape is:

• Rust source under chio-kernel-core/src/formal_aeneas.rs is written in a deliberately constrained subset (no async, no traits with associated types beyond what Aeneas supports, no heap allocation in extracted symbols).
• Charon translates the source to LLBC.
• Aeneas consumes LLBC and emits Lean 4 modules.
• The handwritten module Chio.Proofs.AeneasEquivalence imports the extracted output and proves equivalence to the handwritten model.
• The downstream proofs (in Proofs/Monotonicity.lean, Proofs/Evaluation.lean, and so on) only depend on the handwritten model. The Aeneas equivalence theorem is the bridge that ties their conclusions to the executed Rust.

Equivalence Theorems

The seven Aeneas equivalence theorems are the load-bearing link from the extracted model to the handwritten one. They live in formal/lean4/Chio/Chio/Proofs/AeneasEquivalence.lean.

Each is rootImported: true in the inventory and claimClass: aeneas_equivalence. The gate ./scripts/check-aeneas-equivalence.sh runs the equivalence module under lake build and confirms all seven theorems are proven without sorry.

P1: capability_monotonicity in this tool

P1 says a child capability's bounds are tighter than its parent's. Aeneas's contribution is mechanical: it extracts the bound-comparison helpers from the production Rust source so the downstream Lean equivalence theorem can compare extracted code against the handwritten model. The Rust function that drives P1 in production is ToolGrant::is_subset_of in crates/chio-core-types/src/capability.rs. Its bound-comparison primitive, optional_u32_cap_is_subset, lives in the proof-facing helper module that Aeneas reads from.

That symbol is listed verbatim in the production extraction config:

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

Three of those symbols carry P1 weight directly: optional_u32_cap_is_subset (invocation cap), monetary_cap_is_subset_by_parts (cost cap), and required_true_is_preserved (DPoP-required and similar boolean flags). The other extracted symbols cover P2, P3, P4, and P8 and are listed here because the Aeneas extraction is one config block per file; the per-symbol property attribution lives in the equivalence theorems that consume each extracted symbol.

The Aeneas-side mirror lives under the AeneasMirror namespace in Chio/Proofs/AeneasEquivalence.lean. For P1, the mirror is the optional-cap subset definition and its attendant equivalence theorem:

def optionalCapIsSubset
    (childHasCap : Bool)
    (childValue : Nat)
    (parentHasCap : Bool)
    (parentValue : Nat) : Bool :=
  !parentHasCap || (childHasCap && childValue <= parentValue)

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 says: if the parent has a cap and the Aeneas-extracted subset check accepts, then the child must also have a cap and its value must be bounded by the parent's. The proof case-splits on the boolean flags, simplifies the definition under each combination, and discharges the surviving goal directly from the subset hypothesis. The companion theorem for monetary caps, aeneas_monetaryCapIsSubset_preserves_parent_cap, has the same shape and is cited under the same P1 row in the inventory.

Why this matters: the bounded-model proofs in Proofs/Monotonicity.lean only know about the handwritten Lean definitions. The Aeneas equivalence theorems are what tie those proofs to the running Rust. A future change to optional_u32_cap_is_subset in the Rust source that altered its decision table would re-extract a different Lean definition, and aeneas_optionalCapIsSubset_preserves_parent_cap would either fail to elaborate or fail to prove. The gate ./scripts/check-aeneas-equivalence.sh enforces this on every PR.

Continue the tour at Kani Harnesses: P1 supporting harness or jump back to the P1 Tour.

Reproducing Locally

The full reproduction is three commands plus the prerequisites. Charon, Aeneas, and Lean 4 each pin to a specific version under tools/.

# Lean toolchain pin (handled by lake)
cat formal/lean4/Chio/lean-toolchain
# leanprover/lean4:v4.28.0-rc1

# Pilot lane: extract verified_core.rs, build resulting Lean
./scripts/check-aeneas-pilot.sh

# Production lane: extract chio-kernel-core/src/formal_aeneas.rs
./scripts/check-aeneas-production.sh

# Equivalence: build the handwritten equivalence module
./scripts/check-aeneas-equivalence.sh

# Or: run the full Lean lane (every theorem in the inventory)
cd formal/lean4/Chio && lake build

Building Chio.Proofs.AeneasEquivalence
[7/7] proven without sorry
  proof.aeneas_timeWindowValid_equiv_model            OK
  proof.aeneas_optionalCapIsSubset_preserves_parent   OK
  proof.aeneas_budgetCommit_equiv_model               OK
  proof.aeneas_dpopAdmits_equiv_model                 OK
  proof.aeneas_revocationSnapshot_equiv_model         OK
  proof.aeneas_guardStep_equiv_model                  OK
  proof.aeneas_receiptCoupling_equiv_model            OK
EXITCODE: 0

The artifact report at target/formal/aeneas-production/equivalence-artifacts.json records, per extracted symbol, the byte count of the LLBC, the line count of the resulting Lean, and the list of equivalence theorems that consume it.

Limits

Aeneas does not handle all of Rust. The main constraints visible in the chio extraction are:

• No async · The future monad is not part of the LLBC encoding. Extracted symbols must be synchronous.
• No IO or syscalls · File handles, sockets, and timers are excluded. The pure decision core is the only thing in scope.
• Limited trait support · Extracted code uses traits sparingly and prefers concrete types or enums over generic interfaces. The pilot file's Decision enum is a worked example.
• No heap allocation in extracted symbols · The production lane extracts numeric and boolean helpers; string-heavy or vec-heavy code stays out of the lane.
• Bounded recursion · Recursion that the termination checker cannot establish needs a manual termination proof; the chio extraction prefers iteration where it can.

These constraints explain why the manifest's excluded_surfaces list says: "Aeneas extraction from async, IO, SQLite, crypto, and string-heavy production modules outside crates/chio-kernel-core/src/formal_aeneas.rs". Anything outside that file is out of the Aeneas lane by design.

Extending the Extraction

Adding a new extracted symbol to the production lane is a four-step PR:

• Write the function in crates/chio-kernel-core/src/formal_aeneas.rs using the constrained subset described above.
• Add the symbol to extracted_symbols in formal/aeneas/production.toml.
• Write a handwritten Lean model for the same logic in the appropriate file under Chio/Core/ or Chio/Proofs/.
• Add an equivalence theorem to Proofs/AeneasEquivalence.lean and a corresponding row to theorem-inventory.json.

Next

• Theorem Inventory · the full table including the seven Aeneas equivalence theorems.
• Lean 4 Proofs · the proof structure that consumes the equivalence theorems.
• Kani Harnesses · the bounded model-checking lane that runs alongside Aeneas.