### Setup Charon Dependency

Source: https://github.com/aeneasverif/aeneas/blob/main/README.md

Automates the setup of the Charon project dependency, downloading and building it using rustup or nix.

```bash
make setup-charon
```

--------------------------------

### Install Project Dependencies

Source: https://github.com/aeneasverif/aeneas/blob/main/README.md

Installs all necessary OCaml packages for the Aeneas project using opam.

```bash
opam install calendar core_unix domainslib easy_logging menhir \
  ocamlformat.0.27.0 ocamlgraph odoc ppx_deriving ppx_deriving_yojson \
  progress unionFind visitors yojson zarith
```

--------------------------------

### Lean Tactic Proof Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

Shows a typical structure for a tactic proof in Lean, using 'unfold' and 'step*' tactics.

```lean
by unfold ...; step*; ...
```

--------------------------------

### ML-KEM KeyGen Doc-Comment Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/formalizing-crypto-specs.instructions.md

Include a doc-comment that quotes the relevant RFC pseudocode verbatim for easy reviewer verification. This example shows how to format the doc-comment for Algorithm 16 of FIPS 203.

```lean
/- ML-KEM KeyGen — FIPS 203, Algorithm 16
    ```
      (ek, dk) ← ML-KEM.KeyGen()
      z ← B32
      ek ← ByteEncode₁₂(t̂) ‖ ρ
      dk ← ...
      ``` -/
def mlkem.keygen ...
```

--------------------------------

### Setup Aeneas Simplification Lemmas

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

Activates specific simplification lemmas for Aeneas, particularly for managing `getElem!` and `set!` operations. This setup deactivates lemmas that convert `getElem!` to safer but more verbose alternatives.

```lean
#setup_aeneas_simps

-- Now getElem! is the preferred access pattern
```

--------------------------------

### Full Agent Prompt Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

This is a comprehensive prompt for an agent operating in separate-clone mode. It details the steps for invoking skills, performing initial builds, and using lean-lsp-mcp tools for proof checking.

```markdown
Fix the inner loop sorry in `/path/to/clone/MyModule.lean`.

## Step 1: Invoke Skills
As your FIRST action, invoke these skills (use the `skill` tool):
1. `aeneas-lean-core` — translation model, spec patterns, pitfalls
2. `aeneas-tactics-quickref` — which tactic for which goal
3. `lean-lsp-mcp` — mandatory tooling for proof checking

## Step 2: ⛔ HARD REQUIREMENT — Initial build + lean-lsp-mcp tools ONLY
As your VERY FIRST action after reading skills, run `lake build` in the Lean
project directory to pre-compile .olean caches. This is required because the
lean-lsp-mcp LSP server will time out on first use if caches are stale.

After the initial build, do ALL proof checking via lean-lsp-mcp tools
(`lean_goal`, `lean_diagnostic_messages`, `lean_multi_attempt`, etc.).
Edit the file on disk, then use `lean_goal` and `lean_diagnostic_messages`
to inspect the result.
Do NOT use `lake build` for iterative proof development — only as (1) the initial
build and (2) a single final verification. Iterative `lake build` = REJECTED.

## The Sorry
`my_function_loop0_loop0_spec` at line ~421.

```

--------------------------------

### Aeneas Lean Proof Setup Template

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-crypto-verification.instructions.md

Sets up the Aeneas environment for Lean proofs, including importing necessary libraries, defining custom code and specifications, and registering crypto constants.

```lean
import Aeneas
import MyProject.Code
import MyProject.Spec
import MyProject.Properties.Basic

open Aeneas Std Result

#setup_aeneas_simps

-- Simpler cast spec when values fit in target type
attribute [-step] UScalar.cast.step_spec
attribute [local step] UScalar.cast_inBounds_spec

-- Register crypto constants for all tactics
@[simp, scalar_tac_simps, bvify_simps, agrind =]
theorem Q_val : Q.val = 3329 := by decide
```

--------------------------------

### Setup for Inhabited Types

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-crypto-verification.instructions.md

Enables specific Aeneas simplification rules for array access patterns.

```lean
#setup_aeneas_simps  -- enables getElem!/set! patterns
```

--------------------------------

### Run lean --profile on a theorem

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/lean-lsp-mcp.instructions.md

Use `lean_profile_proof` to get per-line timing information for a specific theorem in a Lean file. This tool is useful for identifying performance bottlenecks in slow proofs but should be used sparingly due to its performance impact.

```shell
lean_profile_proof(file_path="path/to/your/file.lean", line=42)
```

--------------------------------

### Initial Lean Project Build

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/lean-lsp-mcp.instructions.md

Run this command once at the start of a new verification task or after significant project changes (like git merges or branch switches) to pre-compile all .olean files. This prevents timeouts on the first MCP tool call by ensuring the LSP can load files instantly. Subsequent edits are handled incrementally by the LSP.

```bash
cd <lean_project_path> && lake build
```

--------------------------------

### Example of Explicit File Conflict Check

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/agent-fleet-management.instructions.md

Demonstrates how to explicitly state the outcome of a file conflict check before launching agents. This helps ensure that mutual dependencies are identified and handled.

```lean
"CT.lean imports Defs.lean, MulBS.lean imports MatDefs.lean — no mutual
dependencies, safe to parallelize."
```

--------------------------------

### Setup Aeneas Simplifications

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/crypto-verification.md

Use `#setup_aeneas_simps` to configure simplifications for inhabited types and array operations. This deactivates certain lemmas and activates others for cleaner specifications.

```lean
#setup_aeneas_simps
```

--------------------------------

### List Reasoning for Crypto Arrays with agrind

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/crypto-verification.md

Attempt to use `agrind` first for reasoning about array operations with `get` and `set`, as it handles many patterns automatically.

```lean
-- Try this first
agrind
```

--------------------------------

### Reporting Weak Axiom with Suggested Fix

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

When a proof agent discovers a weak axiom, it must report the issue immediately, identify the axiom, explain the missing property, and suggest a strengthened postcondition. This example shows the format for reporting and suggesting a fix for an axiom.

```lean
axiom my_module.external_fn.spec (key : KeyType) (input : Array U16 8#usize) :
  my_module.external_fn key input ⦃ fun out =>
    out = specExternalFn key input ⦄
```

--------------------------------

### Automating Proofs with `step*` and `agrind`

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

Leverage `step*` to automate proof obligations by registering local lemmas with `agrind`. This progressively refolds the proof script.

```lean
attribute [local agrind] my_lemma1 my_lemma2
```

```lean
-- Using step* to do most of the work
theorem list_nth_mut1_spec'' {T: Type} [Inhabited T] (l : CList T) (i : U32)
  (h : i.val < l.toList.length) :
  list_nth_mut1 l i ⦃ x back =>
    x = l.toList[i.val]! ∧
    ∀ x', (back x').toList = l.toList.set i.val x' ⦄ := by
  unfold list_nth_mut1 list_nth_mut1_loop
  /- `step*` repeatedly applies `step`, while doing a case disjunction whenever it
      encounters a branching. Note that one can automatically generate the corresponding
      proof script by using `step*?`. -/
  step*
  simp_all
```

--------------------------------

### Step*? Workflow for Proof Development

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

Explains the `step*?` workflow for developing proofs, involving expansion via `lean_code_actions` and subsequent refinement.

```text
### Use step*? to develop proofs

See the `lean-lsp-mcp` skill file for the full step*? workflow.
In short: write `step*?` → `lean_code_actions` on that line to read the expanded
script → copy it into your proof → fix sub-goals → collapse back to `step*` if possible.
```

--------------------------------

### Public Loop Spec (starts at 0)

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/proof-patterns.instructions.md

A public `@[step]` wrapper that instantiates `spec_gen` at `start = 0`. It derives the final postcondition from the raw postcondition.

```lean
@[step]
theorem my_loop.spec (out a : Slice Std.U16) (hlen : out.length = a.length) :
  my_loop { start := 0#usize, «end» := out.len } out a ⦃ fun res =>
    res.length = out.length ∧
    ∀ j, j < res.length →
      res[j] = f (a[j]) (out[j]) ⦄ := by
  apply WP.spec_mono
  · apply my_loop.spec_gen <;> agrind   -- instantiate spec_gen at start=0
  · intro res ⟨h1, h2⟩; split_conjs <;> agrind   -- derive final postcondition
```

--------------------------------

### Generated Step Theorem Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

An example of a theorem generated by `step_array_spec`. It proves that indexing into `const_array` with `i` succeeds and the element `x` satisfies `x.val = i.val`, given `i.val < 8`.

```lean
-- This generates (roughly):
-- @[step] theorem const_array_spec (i : Usize) (_ : i.val < 8) :
--   Array.index_usize const_array i ⦃ x => x.val = i.val ⦄
```

--------------------------------

### Montgomery/Barrett Reduction Pattern

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-crypto-verification.instructions.md

Example of proving modular equivalence and bounds for reduction operations.

```lean
-- Prove modular equivalence in ZMod
have hMod : (result.val : ZMod q) = (input.val : ZMod q) * montgomery_factor := by
  have ⟨ hMont, _ ⟩ := mont_reduce_spec q R R_inv input.val ...
  zify at h_intermediate_eq
  zify
  simp [h_intermediate_eq, hMont, Int.mul_emod]

-- Prove bounds in Nat/Int
have hBounds : result.val ≤ bound := by
  have hB := bounds_lemma input.val (by scalar_tac)
  zify at h_intermediate_eq
  scalar_tac
```

--------------------------------

### Scaffolding with `agrind` after `step*`

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

Immediately after using `step*`, scaffold each resulting sub-goal with `· agrind`. This is the mandatory first step before inspecting or attempting other tactics.

```lean
step*
· agrind -- goal 1
· agrind -- goal 2
· agrind -- goal 3
· agrind -- goal 4
```

--------------------------------

### Run Aeneas Backend

Source: https://github.com/aeneasverif/aeneas/blob/main/README.md

Execute the Aeneas binary with the desired backend and LLBC file. Use --help for detailed options.

```bash
./bin/aeneas -backend {fstar|coq|lean|hol4} [OPTIONS] LLBC_FILE
```

--------------------------------

### Bit-Vector Reasoning with bv_tac and bvify

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/crypto-verification.md

Utilize `bv_tac` and `bvify` for efficient direct bit-vector goal handling. This approach avoids special setup and is effective for bitwise operations.

```lean
-- Direct bit-vector decision
have h : (some bv expression) = (expected) := by bv_tac 32

-- Lifting to bit-vectors then deciding
bvify 32
bv_tac 32

-- The reverse trick (two cases):
-- Case 1: can't lift goal to bv → prove bv equivalent, convert back to Nat
have h_bv : (bv_equivalent_of_goal) := by bv_tac 32
natify at h_bv
simp_scalar at h_bv   -- then use h_bv

-- Case 2: can't lift hypothesis to bv → write bv equivalent, prove via natify
have h_bv : (bv_equivalent_of_hyp) := by natify; simp [original_hyp]

```

--------------------------------

### Specification Theorem with Backward Function

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

An example of a specification theorem in Lean that includes postconditions for both the result and the backward function, demonstrating how to handle functions returning mutable borrows.

```Lean
@[step]
theorem function_name.spec (param1 : U32) (param2 : Slice U16)
    (hpre : param1.val < param2.length) :
    function_name param1 param2 ⦃ (result : U32) (back : U32 → Slice U16) =>
      postcondition_on_result ∧
      postcondition_on_backward_function back ⦄ := by ...
```

--------------------------------

### Overcoming `agrind` Limitations with `simp [*]`

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

When `agrind` alone fails, try prepending `simp [*]` to the tactic. This can resolve goals that `agrind` cannot handle due to current limitations.

```lean
-- If this fails:
agrind
-- Try this:
simp [*]; agrind
```

--------------------------------

### Create a new Lean project

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/aeneas-overview.md

Use 'lake new' to create a new Lean project. Navigate into the project directory.

```bash
lake new my_proofs
cd my_proofs
```

--------------------------------

### Nat Subtraction Pitfall Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

Demonstrates the potential pitfall of using Nat subtraction in Lean specifications, where subtraction is truncated at 0. This can lead to unintended semantics if not handled carefully.

```lean
-- DANGER: this might not mean what you think!
theorem my_spec (n : Nat) : some_function n ⦃ r => r = n - 1 ⦄
-- When n = 0, this says r = 0, which might not be the intended semantics
```

--------------------------------

### Build the Full Lean Project

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/getting-started.md

Execute the Lake build command to compile the entire Lean project, including generated code and custom proofs.

```bash
cd proofs && lake build
```

--------------------------------

### Build the Aeneas Project

Source: https://github.com/aeneasverif/aeneas/blob/main/README.md

Compiles the Aeneas project from the top directory.

```bash
make
```

--------------------------------

### General Goal Solving with `simp [*]; agrind`

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

As a last resort when other tactics fail, try `simp [*]; agrind`. If still stuck, carefully inspect the goal and consider introducing a `have` statement for a key intermediate fact or strengthening preconditions.

```lean
-- Last resort tactic
simp [*]; agrind
```

--------------------------------

### Backward Continuation Pattern Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

Illustrates the backward continuation pattern used when a Rust function returns a mutable borrow. The Lean translation returns a tuple containing the value and a function to propagate updates.

```Lean
def choose {T : Type} (b : Bool) (x : T) (y : T) :
  Result (T × (T → T × T)) :=
  if b then ok (x, fun z => (z, y))
  else ok (y, fun z => (x, z))
```

--------------------------------

### Lean Result Error Monad Example

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/aeneas-overview.md

All translated functions return `Result T` to model potential runtime failures like panics or overflow. The `do` notation and `massert` combinators are used for sequencing computations and conditional assertions.

```lean
def sum_three (a b c : U32) : Result U32 := do
  let ab ← a + b
  ab + c
```

--------------------------------

### Debugging Tactics: Previewing Step

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tips-and-tricks.md

Allows previewing the expanded proof script of the `step` tactic without committing the changes.

```Lean
step*?   -- prints the expanded proof script without committing to it
```

--------------------------------

### Configure Simp for Inhabited Types with getElem!

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tips-and-tricks.md

Use `#setup_aeneas_simps` at the top of your file to configure `simp` to prefer `getElem!` and `set!` over `getElem`/`set` for inhabited types. This optimizes array access and modification.

```lean
#setup_aeneas_simps   -- put at top of file
```

--------------------------------

### Using `do` Notation for Algorithmic RFC Specifications

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/formalizing-crypto-specs.instructions.md

Employ `do` notation (Id monad) when translating algorithmic sections of RFCs into Lean. This example shows a typical implementation of an NTT (Number Theoretic Transform) using `do` notation and range notations.

```lean
def ntt (f : Polynomial) := Id.run do
  let mut f := f
  let mut i := 1
  for h0: len in [128 : >1 : /= 2] do
    for h1: start in [0 : 256 : 2*len] do
      let zeta := ζ ^ (bitRev 7 i)
      i := i + 1
      for h: j in [start : start+len] do
        let t := zeta * f[j + len]
        f := f.set (j + len) (f[j] - t)
        f := f.set j         (f[j] + t)
  pure f
```

--------------------------------

### Build and Check Warnings

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

Build the module and verify that there are no errors. Acceptable warnings are limited to 'declaration uses \'sorry\''. Address all other warnings, including those around sorry'd proofs.

```bash
# After building, check warning output for:
# "This simp argument is unused" — remove from simp only [...]
# "Too many ids provided" — reduce binders in step as ⟨...⟩
# "unused variable" — remove or prefix with _
# "'...' tactic does nothing" / "is never executed" — remove dead tactic
# "Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice" — replace <;> with ;
```

--------------------------------

### Aeneas Error Reporting Macro Selection Guide

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-compiler-dev.instructions.md

A decision tree to help select the appropriate Aeneas macro for reporting problems, including internal errors, sanity checks, user-facing errors, warnings, option unwrapping, and fallback code generation.

```ocaml
Need to report a problem?
├─ Is this an unreachable code path?
│  → [%internal_error] span
│
├─ Is this an internal invariant that should always hold?
│  → [%sanity_check] span condition
│
├─ Is this a user-facing error (bad input, unsupported feature)?
│  → [%craise] span "message"
│  → [%cassert] span condition "message"
│
├─ Is this a non-fatal warning?
│  → [%warn] span "message"
│
├─ Need to unwrap an Option?
│  ├─ Internal lookup (should never be None)?
│  │  → [%silent_unwrap] span opt
│  └─ Could legitimately be None?
│     → [%unwrap_with_span] span opt "what was expected"
│
└─ In the extraction phase, need to output fallback code?
   → [%admit_raise] span "message" fmt
```

--------------------------------

### Unicode Identifier Escaping for Hat Notation

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/formalizing-crypto-specs.instructions.md

Use Lean's escaped identifier syntax `«»` for variables with hats (e.g., f̂, t̂, k̂) to match RFC notation. This example demonstrates its use in variable assignments and function parameters.

```lean
-- «f̂» = U+00AB, f, U+0302 (combining circumflex), U+00BB
def ntt (f : Poly) : Poly := Id.run do
  let mut «f̂» := f              -- f̂ ← f
  for h : j in [0 : 256] do
    «f̂» := «f̂».set ⟨j, by agrind⟩ (...)
  return «f̂»

def multiplyNTTs («f̂» «ĝ» : Poly) : Poly := ...
```

--------------------------------

### List Reasoning: Automatic vs. Manual

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

Use `agrind` for automatic list get/set operations. If performance is an issue, switch to manual proofs using `cases` and `simp_lists`.

```lean
-- Automatic approach (try first)
agrind

-- Manual fallback (if agrind is too slow)
cases h_idx
· simp_lists
· simp_lists [*]
```

--------------------------------

### Attribute Management Cheatsheet

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-tactics-quickref.instructions.md

Demonstrates how to set up Aeneas simplifier lemmas and register custom lemmas for specific tactics like simp_scalar, simp_lists, and agrind. Also shows how to register constants for all tactics.

```lean
-- Setup for crypto/array proofs
#setup_aeneas_simps
```

```lean
-- Swap to simpler cast spec
attribute [-step] UScalar.cast.step_spec
attribute [local step] UScalar.cast_inBounds_spec
```

```lean
-- Register lemma for specific tactic
attribute [local simp_scalar_simps] my_lemma
attribute [local simp_lists_simps] my_lemma
attribute [local agrind] my_lemma
```

```lean
-- Register constant for all tactics
@[simp, scalar_tac_simps, bvify_simps, agrind =]
theorem MY_CONST_val : MY_CONST.val = 42 := by decide
```

--------------------------------

### Auxiliary Function and Theorem Structure for Decomposition

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

Example structure for defining auxiliary functions, fold theorems, and auxiliary specifications when decomposing large functions. This pattern is used when a function exceeds 30 lines of Lean code and can be split into smaller, manageable parts.

```lean
private def setup_phase (params : U32) (buf : Slice U16) : Result (Slice U16) :=
do
  ...

-- Fold theorem (to be proved)
private theorem fold_setup_phase ... :
  (do /- lines 15-25 inline -/ f result) = (do let r ← setup_phase params buf; f r) :=
  sorry

-- Auxiliary spec
@[local step]
theorem setup_phase.spec ... :
  setup_phase params buf ⦃ res => ... ⦄ :=
  sorry

-- Main theorem (uses auxiliary specs via step)
@[step]
theorem main_function.spec ... :
  main_function ... ⦃ res => ... ⦄ :=
  sorry
```

--------------------------------

### Aeneas Monadic Code Structure

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/proof-strategies.md

This is an example of Aeneas-generated code using the `Result` error monad with `do` notation. Key patterns include monadic bind (`←`), pure let binding (`:=`), explicit success (`ok`), failure (`fail`), and monadic assert (`massert`).

```lean
def my_function (x : U32) (y : U32) : Result U32 := do
  let z ← x + y          -- monadic bind; may fail on overflow
  let w ← z * 2#u32      -- another potentially-failing operation
  ok w                    -- explicit success
```

--------------------------------

### Mandatory lean-lsp-mcp Usage for Proof Agents

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/launching-proof-agents.instructions.md

Details the required `lean-lsp-mcp` workflow, including an initial `lake build` and subsequent use of MCP tools for proof development. Avoids `lake build` for iteration to prevent timeouts.

```text
### MANDATORY: Use lean-lsp-mcp tools — NOT lake build

⚠️ INITIAL BUILD REQUIRED: Before your VERY FIRST use of any lean-lsp-mcp tool,
run `lake build` in the Lean project directory. The LSP server has a cold-start
timeout issue — if `.olean` caches are missing or stale (after git merge, branch
switch, or fresh clone), the first MCP tool call will time out. Running `lake build`
once at the start pre-compiles all dependencies so the LSP can load them instantly.

After this initial build, DO NOT use `lake build` to iterate on proofs. Use the
lean-lsp-mcp tools (see the `lean-lsp-mcp` skill file for full reference).

The tools (`lean_goal`, `lean_diagnostic_messages`, `lean_multi_attempt`, etc.)
are available directly in your tool palette. If they are not available, ask the
user to install lean-lsp-mcp (see the `lean-lsp-mcp` skill file). Whenever you get
"Error: Not connected", the MCP server likely crashed and is restarting — wait
a couple of minutes and retry.

Workflow:
  1. Run `lake build` ONCE at session start (initial build)
  2. edit file on disk → lean_goal → lean_multi_attempt → edit → repeat
  3. Only use `lake build` again at the very end to confirm the final result.

⛔ NEVER run `lake clean` or delete `.lake/`. This forces a full rebuild (30+ min). Fix root causes instead.
```

--------------------------------

### Configure Lean Project with lakefile.lean

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/getting-started.md

Set up the Lake build system for your Lean project, including specifying the Aeneas dependency.

```lean
import Lake
open Lake DSL

require aeneas from "/path/to/aeneas/backends/lean"

package «my-crate» {}

@[default_target]
lean_lib «MyCrate»
```

--------------------------------

### Avoid `step* <;> tactic` and `all_goals tactic`

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-tactics-quickref.instructions.md

Never use `step* <;> ...`, `all_goals ...`, or `step* <;> all_goals ...`. These patterns lead to slow re-elaboration and destroy interactive feedback. Use focused `·` blocks instead.

```lean
-- ⛔ BAD: editing any tactic after <;> replays the full step*
step* <;> scalar_tac
```

```lean
-- ⛔ ALSO BAD: same problem even with all_goals
step* <;> all_goals agrind
```

```lean
-- ⛔ ALSO BAD: standalone all_goals — all goals become one elaboration unit
step*
all_goals scalar_tac
```

```lean
-- ✅ GOOD: each goal is independently checkpointed
step*
· scalar_tac          -- goal 1: independently elaborated
· agrind              -- goal 2: independently elaborated
· simp [*]; scalar_tac -- goal 3: independently elaborated
```

--------------------------------

### Use `calc` for Equational Chains in Arithmetic Proofs

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

Employ the `calc` command for proving equational chains in arithmetic goals. This provides a structured way to build up equalities step by step, often used in conjunction with `simp_scalar`.

```lean
calc a * b % (2^16)
    _ = a * b % (2^16) := rfl
    _ = (a * b) - (2^16) * ((a * b) / 2^16) := by simp_scalar
    _ = ... := by simp_scalar
```

--------------------------------

### Avoid Early Case Splits on Parameters in Step Proofs

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-lean-core.instructions.md

Demonstrates the correct way to handle parameter case splits in step proofs. Avoid splitting on parameters at the top level; instead, perform case splits locally within specific sub-goals that require concrete values.

```lean
-- BAD: duplicates the entire proof N times
theorem my_fn.spec (p : Spec.Crypto.parameterSet) ... := by
  cases p <;> (unfold my_fn; step*; ...)

-- GOOD: case split only where needed
theorem my_fn.spec (p : Spec.Crypto.parameterSet) ... := by
  unfold my_fn
  step*
  · cases p <;> simp_all [Spec.Crypto.n, Spec.Crypto.k] <;> scalar_tac  -- only this sub-goal needs it
  step*
```

--------------------------------

### Copy Lean Toolchain File

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/getting-started.md

Copy the Aeneas Lean toolchain configuration file to your project's proofs directory.

```bash
cp /path/to/aeneas/backends/lean/lean-toolchain proofs/lean-toolchain
```

--------------------------------

### Apply step theorem

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tactics-reference.md

Use the basic `step` tactic to apply a matching theorem tagged with `@[step]`. This is the primary method for making progress on goals involving monadic function calls.

```lean
step
```

--------------------------------

### Slice GetElem Instance

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tips-and-tricks.md

Shows how Slice's `GetElem` instance delegates to List's `getElem`.

```Lean
instance : GetElem (Slice α) Nat α (fun a i => i < a.val.length) where
  getElem a i h := getElem a.val i h   -- a.val is the underlying List
```

--------------------------------

### Use Lean's `while` for RFC `while` Loops

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/formalizing-crypto-specs.instructions.md

Use Lean's `while` construct within `Id.run do` for RFC `while` loops, as it compiles to a total function without requiring a termination proof. Use the dependent form when the loop guard is needed for bounds proofs.

```lean
-- Use the dependent form `while h : j < 256 do ...` when the loop guard `j < 256` is needed as a bound proof inside the body.
```

--------------------------------

### Generate LLBC File with Charon

Source: https://github.com/aeneasverif/aeneas/blob/main/README.md

Use this command to generate the serialized .llbc file from your crate. Ensure you are inside the crate directory.

```bash
charon cargo --preset=aeneas
```

--------------------------------

### Inspect Proof Goals with lean_goal

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/lean-lsp-mcp.instructions.md

Use `lean_goal` to inspect the current proof state. Call it on `sorry` lines to see what needs to be proved, or on tactic lines to view the state before and after the tactic executes. Omit `column` to see both `goals_before` and `goals_after`.

```shell
lean_goal(file_path="MyProject/Properties/Foo.lean", line=42)
```

--------------------------------

### Define a Lean Theorem with Aeneas Tactics

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/getting-started.md

Write a Lean theorem that utilizes Aeneas tactics like `#setup_aeneas_simps` and the `step` tactic for verification.

```lean
import Aeneas
import MyCrate.Code.Funs

open MyCrate

#setup_aeneas_simps

-- Suppose the generated code contains:
--   def add_overflow (a : U32) (b : U32) : Result U32 := a + b

@[step]
theorem add_overflow_spec (a b : U32) (h : a.val + b.val ≤ U32.max) :
  add_overflow a b ⦃ c => c.val = a.val + b.val ⦄ := by
  unfold add_overflow
  step
```

--------------------------------

### List Get/Set Reasoning Tactics

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tips-and-tricks.md

Provides tactics for reasoning about List get/set operations, preferring `agrind` for performance.

```Lean
-- Try agrind first; if it fails, try grind (slower but more list lemmas)
agrind
-- If too slow, go manual
cases h_idx <;> simp_lists [*]
```

--------------------------------

### YAML Frontmatter for Skill Files

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/skill-file-authoring.instructions.md

Every skill file must begin with this YAML frontmatter block, including 'name' and 'description' fields. These are required for detection by Copilot CLI and Claude Code.

```yaml
---
name: kebab-case-name
description: One-line description of what this skill covers
---
```

--------------------------------

### Measure Per-File Build Time with Lake

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/skills/aeneas-tactics-quickref.instructions.md

Use this script to measure the elaboration time of individual Lean files. Ensure all dependencies are compiled first. The `time` command output format may vary by shell.

```bash
cd <project-lean-root>
lake build   # ensure all dependencies are compiled
find Properties -name "*.lean" | sort | while read f; do
  printf "%s: " "$f"
  { time lake env lean "$f" ; } 2>&1 | grep "^real"
done
```

--------------------------------

### Run Aeneas to generate Lean files

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/aeneas-overview.md

Use the Aeneas binary to translate the .llbc file into Lean files. Options include splitting files and specifying an output directory.

```bash
./bin/aeneas -backend lean [OPTIONS] YOUR_CRATE.llbc
```

--------------------------------

### Structure Arithmetic Proofs with `have` and `calc` in Lean

Source: https://github.com/aeneasverif/aeneas/blob/main/documentation/tips-and-tricks.md

Organize multi-step arithmetic proofs using chained `have` statements, each provable by `simp_scalar`, or use `calc` blocks for equational reasoning. Provide additional lemmas or mark them for `simp_scalar` if needed.

```lean
have h1 : a * b < 2^32 := by simp_scalar
have h2 : (a * b) / q < q := by simp_scalar
have h3 : (a * b) % q = a * b - q * ((a * b) / q) := by simp_scalar
simp only [h3]; simp_scalar
```

```lean
calc a * b % (2^16)
    _ = (a * b) - (2^16) * ((a * b) / 2^16) := by simp_scalar
    _ = ... := by simp_scalar
```