fips205-source/rust-toolchain.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"
reproducibility: commit Cargo.lock + pin rust-toolchain (review round 2) 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> 2026-07-24 17:08:47 +00:00			`# 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"`