simplex

Use when Rust source under `src/` changes and the Lean proof project needs re-derived types/functions — covers the pipeline, which files are generated vs hand-maintained, and the expected noise.

Use when bumping the pinned Charon or Aeneas release tag in this repo — walks the coupled set of values that must move together, the regeneration/build sequence, and the known drift points enforcement catches.

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.