mirror of
https://github.com/saymrwulf/fips205-source.git
synced 2026-09-03 19:53:49 +00:00
mrwulf
797b4ef263
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>
6 lines
340 B
TOML
6 lines
340 B
TOML
# Pinned to the exact nightly the Charon/Aeneas transpiler uses (see
|
|
# aeneas-toolchain/aeneas/charon/rust-toolchain). This aligns `charon cargo`
|
|
# extraction and the `cargo test` differential harness on one compiler, and
|
|
# documents the toolchain for reproducible regeneration of the Lean model.
|
|
[toolchain]
|
|
channel = "nightly-2026-06-01"
|