code/bugfind/TOOLCHAIN.md

bugfind toolchain (Rust -> Charon -> Aeneas -> Lean), built 2026-10-14

Everything lives under /apps/development/rlhf/toolchains/; source bugfind/env.sh sets HOME, RUSTUP_HOME, CARGO_HOME, OPAMROOT, ELAN_HOME, TMPDIR, XDG_* there. One command rebuilds from scratch (idempotent): bash bugfind/setup_toolchain.sh. Nothing under align/ imports bugfind/.

Component	Version / commit	Where
rustup	1.29.1	toolchains/cargo/bin/rustup (no default toolchain except stable, see below)
Rust nightly for Charon	nightly-2026-09-17 (+ rustc-dev, llvm-tools, rust-src, miri) from Charon's rust-toolchain	toolchains/rustup
Charon	b05c4774638599608f26b777b6bc49120446365a (2026-10-12), the commit pinned by Aeneas' charon-pin; submodule crates/minirust @ c0b555e5	toolchains/src/aeneas/charon/bin/{charon,charon-driver} (debug build)
Aeneas	6c2788d1366f09d69fd55b2b9be71cd17d28a9ab (2026-10-14, master)	toolchains/src/aeneas/bin/aeneas
OCaml / opam / dune	5.3.0 (vanilla), opam 2.6.1 (sandboxing disabled: no bwrap), dune 3.24.2	toolchains/opam (switch 5.3.0)
gmp	6.3.0, private prefix (the box has libgmp.so but no gmp.h; avoided a system dnf install)	toolchains/local
elan	4.2.4	toolchains/elan
Lean	leanprover/lean4:v4.35.0-rc4 (Aeneas' backends/lean/lean-toolchain; the task text said "~4.31", the pin is now 4.35.0-rc4)	toolchains/elan/toolchains
Aeneas Lean lib	lake build Aeneas AeneasMeta OK (1790 jobs); Mathlib v4.35.0-rc4 (rev 1f414401) via the Mathlib cache (9004 oleans)	toolchains/src/aeneas/backends/lean/.lake (8 GB)
System rustc/cargo	1.88.0 (Amazon Linux package), used only for mutant differential harnesses and the baseline arms	/usr/bin

Disk: toolchains/ is 28 GB (src 19 GB incl. Charon target/, rustup 3 GB, elan 3 GB, opam 1.5 GB). /home free space did not decrease because of this work except for one incident: Charon's miri sysroot goes to $HOME/.cache/charon regardless of XDG_CACHE_HOME (112 MB landed in /home once); it was moved to toolchains/home/.cache and env.sh now redirects HOME. Pre-existing `/.cargo(57 MB) and~/.elan(946 MB) on/homebelong to other work and were not touched.rustup toolchain install stable(1.99.0) was added as rustup's default so thatcargo`-installed tools (Kani, cargo-fuzz) can build.

Smoke test (bugfind/smoke/run_smoke.sh) : PASSES

smoke/tiny (4 integer functions; avg_buggy computes (a + b) / 2 in u32 and overflows) -> charon cargo --preset=aeneas -> tiny.llbc -> aeneas -backend lean -> Tiny.lean (4 functions translated, 0.6 s) -> lean compiles it against the Aeneas library, plus Check.lean with three kernel-checked theorems: the overflow witness avg_buggy 4294967295#u32 4294967295#u32 = fail Error.integerOverflow (simp +decide [...]), the conditional spec of avg_buggy, and total correctness of abs_diff (step*). Wall time of the whole script: ~15 s once Charon's dependencies are cached.

Things that bit, so the next person does not rediscover them

• make setup-charon needs git submodule update --init in charon/ (minirust) or the build fails on miniutil.
• Aeneas' make must not run with MAKEFLAGS=-j* (parallel dune build calls fight over _build/.lock); env.sh therefore does not set it.
• charon-ml's own make build-dev wants odoc; it is not needed, Aeneas builds charon-ml through dune.
• Lean module-style files need lean --root=<dir> -o X.olean X.lean (plain lake env lean -o refuses files outside the package root).
• pkill -f <pattern> self-matches the invoking shell when the pattern is in the command line; kill by PID.
• Aeneas can crash with an OCaml exception (not just [Error]) on real crates (e.g. webpki 0.22.1, translate_ExpandAdt_one_branch); translating the whole crate is therefore the wrong unit for real-world items; see bench/translate_items.py.

One-command setup and the host-safety wrapper

cd /apps/development/rlhf/align-wt/bench
/apps/development/rlhf/align/.venv/bin/python /apps/development/rlhf/align/scripts/hostguard.py run --cores 4 --mem-gb 16 --label setup --wait -- bash bugfind/setup_toolchain.sh

(idempotent; pins: Aeneas 6c2788d1, Charon b05c4774 read from Aeneas' charon-pin, Lean v4.35.0-rc4 from backends/lean/lean-toolchain, opam switch 5.3.0.) EVERY build / translate / cargo / lean / test command here runs through hostguard.py run --cores 4 --mem-gb 16 --label <x> --wait --, strictly one at a time (2026-10-15 crash: unbounded cargo/rustc/charon/lake). source bugfind/env.sh first; per-item timeouts are in the drivers.

Pipeline commands (all serial, under hostguard)

Step	Command (after source bugfind/env.sh; eval "$(opam env --switch=5.3.0 --set-switch)")	Output
(re)generate kernels	python -I bench/make_kernels.py	bench/kernels/<k>/{meta.json,pre,post}
witness replay on original Rust	python -I bench/witness_replay.py (rustup stable rustc 1.99.0 as recorded per ledger line, debug-assertions + overflow-checks)	bench/ledger/witness_ledger.jsonl
Charon -> Aeneas -> Lean compile, pre and post	python -I bench/translate_kernels.py	bugfind_data/out/kernel_translate.jsonl (Lean sha256 per item)
advisory items (changed fn of the real crate)	python -I bench/translate_items.py advisory_candidates.jsonl --out ... --jobs 1	advisory_translate.jsonl
mutants	python -I bench/translate_items.py mutants.jsonl --mutants --jobs 1 --timeout 300 --out ...	mutant_translate.jsonl
merge + funnel	python -I bench/build_items.py (no heavy work)	bench/items/*.jsonl, bench/items/SUMMARY.json
baselines sweep	bash baselines/sweep.sh CPU_SECONDS ARMS OUT.jsonl	bench/ledger/baseline_sweep_*.jsonl

Baselines: proptest, cargo-fuzz, Kani (installed 2026-10-19, all under /apps)

Tool	Version	Where	Note
proptest	crate proptest = "1" pulled per harness	CARGO_HOME registry	harness uses stable rustc 1.99.0 (rustup)
cargo-fuzz	0.13.2	toolchains/cargo/bin	runs with RUSTUP_TOOLCHAIN=nightly-2026-09-17 (libFuzzer needs nightly)
Kani	kani-verifier 0.68.0, bundle kani-0.68.0 (485 MB) + its pinned nightly nightly-2026-08-21	KANI_HOME=$TC/kani, rustup under $TC/rustup	export KANI_HOME=$TC/kani before cargo kani; /apps was at 97% (145 GB free) so the install was kept small

Equal-budget protocol and the shared property bank are in baselines/README.md; provenance of the bank in baselines/bank/README_PROVENANCE.md. Kani caveat (observed on the smoke crate): an unwinding-assertion failure on a loop (gcd) prints VERIFICATION:- FAILED and is NOT a bug; every flag from every arm must be replayed on the unmodified Rust (witness ledger rule) before it is credited.