External review round 2 (GPT B1.5) flagged that no Cargo.lock was committed
and the extraction toolchain was undocumented. Fixes:
- Un-ignore and commit Cargo.lock (this is a verification-pinned snapshot, not
a library — a locked dependency graph is part of the reproducible artifact).
- Add rust-toolchain.toml pinning nightly-2026-06-01, the exact channel the
Charon/Aeneas transpiler uses, so `charon cargo` extraction and the `cargo
test` differential harness agree on one compiler.
Verified: re-running verification/extract.sh against this tree reproduces
gen/SlhVerify/{Types,Funs}.lean BYTE-IDENTICALLY (sha256 unchanged) — these
additions do not perturb the extracted Lean model.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
