Aeneas Verification Toolchain

Aeneas is a tool that translates Rust programs into pure Lean code via the LLBC (Low-Level Borrow Calculus) intermediate representation. This enables formal verification of Rust code within the Lean proof assistant.

Key technical concepts include:

• LLBC: An intermediate representation between Rust MIR and Lean that captures ownership, borrowing, and lifetime information.
• Result monad: The error monad used in all generated code. Success is represented by ok v, and errors (panics, overflows, out-of-bounds) are represented by fail. All generated functions return Result T.
• Backward continuation: A function returned alongside a borrowed value to propagate updates back to the original owner (used for &mut T). In Lean, this appears as an extra return value: Result (T × (T → Result OriginalType)).
• ControlFlow: An inductive type used for loop translation. Use ControlFlow.cont x to continue a loop with new state, or ControlFlow.done y to break with a result.
• loop (fixed-point operator): The combinator used to translate Rust loops. Its signature is loop (body : α → Result (ControlFlow α β)) (x : α) : Result β. You can reason about it using loop.spec or loop.spec_decr_nat.

Certain actions are strictly banned to protect the integrity of the shared codebase and system resources.

Banned Git Commands

NEVER run the following commands:

• git checkout
• git restore
• git stash
• git reset

Reasoning: These commands can silently destroy uncommitted changes made by other agents. Even reverting a file you own is dangerous because it may revert to a HEAD state that lacks changes from a different agent.

Banned Sub-agent Spawning

Agents must NEVER spawn sub-agents that run heavy processes (e.g., Lean LSP, builds, solvers).

• Resource Exhaustion: Sub-agents bypass the supervisor's budget control.
• File Conflicts: Sub-agents may bypass the supervisor's file ownership tracking.
• Loss of Control: The supervisor cannot observe or manage sub-agents spawned by other agents.

Note: Lightweight sub-agents (e.g., explore agents for searching) are permitted.

When reviewing or writing specifications, ensure postconditions express full functional correctness (FC), not just structural properties. A postcondition that only describes metadata (e.g., index advanced, flags preserved, or res.length = n) without specifying the actual computed values is critically weak and insufficient for callers to derive their own FC.

Key Requirements:

• Relate to Pure Spec: The postcondition must relate the output to the pure specification function (e.g., output = Spec.SHAKE128(input)[offset..offset+len]).
• Strength for Callers: Trace the call chain. If an outer loop or caller requires both the length and the element-wise values of a slice, the inner loop's postcondition must provide both.
• Avoid Weak Patterns: Reject postconditions that are only length-based, vacuously true (True or fun _ => True), or missing existential quantifiers for length combined with functional properties.

When working with Rust constants or globals translated by Aeneas, you must treat pure and monadic constants differently to enable automation.

Pure Constants

If a constant is not in the Result monad, mark it with appropriate attributes so automation can use it:

• Use @[simp], @[agrind], @[scalar_tac_simps], or @[bvify_simps].
• Use @[simp_lists_simps] if the constant involves lists or arrays.

Monadic Constants (in the Result monad)

Treat monadic constants as functions by proving a @[step] theorem. This involves a two-step process:

1. Prove a raw equation using native_decide.
2. Prove the step form using the equation and WP.spec_ok.

Once these are defined, the step and step* tactics will handle the constant automatically.

// 1. Prove a raw equation
theorem MyConst_eq : MyConst = ok value := by native_decide

// 2. Prove the step form
@[step] theorem MyConst : MyConst ⦃ fun res => res = value ⦄ := by 
  rw [MyConst_eq]
  simp [WP.spec_ok]

To prevent destroying the work of other parallel agents, adhere to these strict workspace constraints:

Git Safety (CRITICAL):

• NEVER run git checkout, git restore, git stash, git reset, or any command that reverts or discards file changes. Other agents have uncommitted work on disk; reverting will destroy their work silently.
• NEVER commit or push without explicit user approval.

File Modification Rules:

• In same-clone mode: ONLY modify the specific target file (e.g., /path/to/MyModule.lean). NEVER edit any other .lean file, as other agents are working on them in parallel. Use local private axiom and TODO comments for cross-file requirements.
• In separate-clone mode: Your primary task is the target file, but you MAY modify other files in your clone (e.g., shared defs, axiom files, bridge lemmas) if necessary. The supervisor handles merging across clones.