updating-aeneas-charon

name	updating-aeneas-charon
description	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.

Updating Aeneas / Charon versions

Charon and Aeneas publish nightly pre-release tags; this repo pins specific ones for reproducibility. Aeneas bumps are the hard case because three values must stay in lockstep and a fourth (the patch list) often needs pruning.

Coupled values

#	File	Value
1	scripts/gen_lean.sh	AENEAS_TAG — the 40-hex suffix is the Aeneas release commit
2	proof/lakefile.toml	rev — must equal that 40-hex hash
3	scripts/gen_lean.sh	LEAN_TOOLCHAIN constant
4	proof/lean-toolchain	must equal LEAN_TOOLCHAIN exactly

Charon has its own tag (CHARON_TAG) and is independently versioned — don't force it to move in lockstep with Aeneas.

Workflow

1. Pick new CHARON_TAG and/or AENEAS_TAG from the GitHub release pages of AeneasVerif/charon and AeneasVerif/aeneas.
2. Update AENEAS_TAG in scripts/gen_lean.sh and the matching rev in proof/lakefile.toml.
3. If the new Aeneas release ships a different Lean toolchain (check backends/lean/lean-toolchain in the Aeneas tarball), update both LEAN_TOOLCHAIN in scripts/gen_lean.sh and proof/lean-toolchain to match.
4. Review the aeneas-patches block (Step 4 in gen_lean.sh) — remove patches for bugs now fixed upstream, add new ones if the release introduces them. If the list is unchanged, make a no-op whitespace touch so blockwatch sees the review.
5. Run make lean-bootstrap (downloads the pinned binaries) then cd proof && lake update && lake build.
6. If lake build fails, inspect the failure — either a new Aeneas bug needs a patch in Step 4, or the Lean toolchain is wrong.

What enforcement catches (and what it doesn't)

• blockwatch (affects): forces aeneas-tag, aeneas-rev, lean-toolchain, and aeneas-patches to all appear in the same diff.
• blockwatch (line-pattern): rejects malformed CHARON_TAG / AENEAS_TAG / LEAN_TOOLCHAIN / rev values (truncated hash, wrong shape).
• scripts/check_versions.sh (pre-commit hook + gen_lean.sh preflight): asserts that the actual values agree — AENEAS_TAG suffix == lakefile.toml rev, and proof/lean-toolchain == LEAN_TOOLCHAIN.
• Not caught statically: proof/lake-manifest.json drift (regenerated by lake update) and whether the committed proof/Simplex/{Types,Funs}.lean match a fresh make lean run. CI's lean-proof job catches the latter by building.

Common mistakes

• Bumping AENEAS_TAG but forgetting rev in lakefile.toml — blockwatch blocks the commit, check_versions.sh catches the value mismatch.
• Skipping lake update after changing rev — lake-manifest.json stays on the old hash; build may still work locally due to cache but CI will diverge.
• Leaving stale patches in Step 4 when upstream has fixed them — Lean compilation often still works but the Funs.lean/Types.lean post-processing becomes a no-op that quietly drifts. Check each patch on every bump.
• Assuming a Charon bump is independent — it usually is, but a Charon version that emits LLBC a newer Aeneas doesn't understand (or vice versa) will surface as an Aeneas error on step 2.