# 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 `/home` belong to other work and were not touched.
`rustup toolchain install stable` (1.99.0) was added as rustup's default so that `cargo`-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 `timeout`s 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.