| name | writing-aeneas-compatible-rust |
| description | Use when adding or modifying Rust code under `src/` — covers the constraints that keep the state machine translatable to Lean via Charon + Aeneas, and what to do when you need something Aeneas can't translate. |
Writing Aeneas-compatible Rust
The consensus state machine must round-trip cleanly through charon → aeneas → Lean. Aeneas translates a large but not complete subset of Rust. Code that works fine for cargo build may still break make lean or produce Lean that can't be proven about.
Non-negotiables
| Rule | Why |
|---|
#![no_std] with extern crate alloc | Aeneas models alloc collections but not std I/O / threading / time. |
BTreeMap / BTreeSet over HashMap / HashSet | Deterministic iteration is required for formal proofs; Aeneas' HashMap support is limited. |
No closures in iterator chains on hashbrown maps | Known Aeneas limitation — closures in `.iter().filter( |
No unsafe, no FFI, no async | Aeneas rejects or silently skips. |
No std::time / std::sync / threads | Model time as a View (u64) and actions as events; I/O belongs outside the state machine. |
| Keep the state machine pure | Consensus::handle_event(Event) -> Vec<Action> is the interface. No side effects inside. |
Preferred patterns
- Types are data.
PeerId, View, BlockHash are newtypes over fixed-size arrays or u64. Avoid traits with associated types unless Aeneas handles them (basic Ord/PartialOrd/Eq are fine).
- Options over sentinels.
Vote.block_hash: Option<BlockHash> encodes the dummy block / timeout cleanly — Aeneas translates Option well.
- Explicit matches over
if let chains in complex cases — translates to cleaner Lean.
- Small, total functions. Aeneas proofs get harder as functions grow or panic conditionally.
When you need something Aeneas can't translate
- Put it in a module marked opaque — Aeneas emits an
axiom in *External_Template.lean, and you fill the corresponding *External.lean by hand. Good for e.g. cryptographic hashing primitives.
- Keep the opaque surface tiny. Every opaque function is an unverified trust boundary.
- Regenerate and fill the hole — see the
regenerating-lean-proofs skill for the workflow around *External.lean.
Early warning signs
- Aeneas warning "Found an unknown type declaration with region parameters" on your type → likely an unusual lifetime pattern; simplify or make opaque.
- Charon succeeds but
make lean fails at step 2 with a named function — that function hit a translation limit. Check for closures, complex generics, or trait objects.
cargo test passes but lake build produces a type mismatch in Funs.lean → Aeneas translated something surprising; read the generated Lean for that function and adjust the Rust to be more direct.
Known patch-worthy upstream bugs
See the aeneas-patches block in scripts/gen_lean.sh for patches currently applied to Aeneas output. If you hit a new translation issue that looks upstream-ish, check there first — it may be a known issue with a workaround or already-fixed in a newer Aeneas (see updating-aeneas-charon).
Verification loop
After any non-trivial change:
cargo clippy --all-targets --all-features -- -D warningscargo testmake lean — catches translation breakagecd proof && lake build — catches Lean-level type issues in the regenerated code- Commit Rust + regenerated
proof/Simplex/{Types,Funs}.lean together.
