| # 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. |
|
|
