Add a fuzzer for hax/aeneas

[karthikbhargavan]

What this adds

A source-level fuzzer for the Aeneas Rust→Lean translation, under a
self-contained fuzz/ directory, plus a CI workflow that runs it on a schedule.

It mutates the tests/src seed corpus (14 seeded mutators + a borrow-weighted
generator), packs functions into crates, drives them through
rustc → charon → aeneas, and classifies each outcome — crash,
wrong-rejection (rustc accepts but aeneas rejects), or optional Lean
elaboration failure — with dedup against a committed findings DB. A
native-vs-Lean semantic differential (fuzz/semdiff/) is included for
catching miscompilations.

Running in CI (self-hosted nix runners)

.github/workflows/fuzz-nightly.yml mirrors ci.yml:

• nix build .#aeneas yields result/bin/aeneas and a pin-matched
  result/bin/charon (the flake symlinks charon into the aeneas output;
  flake.lock/charon-pin are the pin, already enforced by the
  check-charon-pin flake check) — nothing to pin by hand.
• The harness builds and runs inside nix develop --command (Rust via rustup,
  elan for the optional Lean oracle).
• run --ci exit contract: exit 3 iff a NEW (non-deduped,
  non-expected-reject) finding was recorded versus the committed
  fuzz/findings/db.json. Known bugs and feature-gate rejections keep the job
  green. So CI goes red exactly when a change introduces a new
  crash/miscompilation. The seed is derived from the run id and logged, so any
  red run reproduces locally.
• Lanes: nightly (fork, fast crash/reject, ~25 min) + weekly (fork, longer
  ~90 min) + workflow_dispatch (time_budget, seed, oracle_scope=lean).

What it has already surfaced

Run against both the fork toolchain and upstream main during development
(details in fuzz/FINDINGS.md):

• N1 — two assert! of the same bool → "no bottoms" (InterpExpressions.ml:55),
  both targets. Filed as Crash: two assert! of the same boolean aborts translation ("no bottoms in the value") #28.
• N3 — a closure reading a captured &mut → SymbolicToPureValues.ml:366
  (fork toolchain only; likely a version delta). Filed as Crash: a closure that reads through a captured &mut aborts translation (SymbolicToPureValues.ml:366) #40.
• Deduped to existing issues: N2 → upstream Could not match the contexts AeneasVerif/aeneas#930/Bug: for loop with conditional break and code after it: "Could not match the contexts" AeneasVerif/aeneas#1206, N4 → upstream bug: Matching on chars throws an Uncaught exception AeneasVerif/aeneas#797,
  F4/F6 → Crash: returning a borrowed value from inside a loop aborts whole-crate translation (reorder_loop_outputs) #22/Inverted can_end guard in eliminate_shared_loans mutates frozen abstractions; valid programs rejected #24, from_fn → Error with reference produced by a closure AeneasVerif/aeneas#804. The db.json baseline records all of
  these so they don't re-flag.

Scope / notes

• CI is fork-only — it guards this repo's own changes. The fork-vs-upstream
  differential is a local/manual activity (fuzz/setup/build_upstream.sh).
• The Phase-3 pure-IR stage differential (pure-eval/, stage-diff/) needs
  the fork-only -dump-pure-ir feature and is not in this PR; it lives on
  the dump-pure-ir branch. This PR is buildable on main (harness cargo test:
  50 unit + 6 integration green here).
• Scheduled workflows only fire from the default branch, so this must merge
  to main for the nightly/weekly lanes to run.

Before it goes live (maintainer)

• Confirm the self-hosted nix runner ([self-hosted, linux, nix]) is
  available for this repo, and do a first manual workflow_dispatch run to
  validate the environment (rustup/elan in nix develop, artifact upload).
• New findings are not auto-committed — they upload as artifacts for a
  maintainer to triage and commit into db.json + repro dirs.

🤖 Generated with Claude Code