File size: 1,795 Bytes
4951e76 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 | # Bounded-checker baselines (Phase 5, Part A arms)
Arms: Kani (bounded model checking), proptest (property-based testing), cargo-fuzz (libFuzzer).
All three consume ONE shared property bank (`bank/*.json`, same format the prover / reviewer arms use), so recall
differences cannot come from different properties.
Equal-CPU protocol: each (item, arm) gets the same `--cpu-seconds` budget of CPU time on one core
(`RLIMIT_CPU` on the whole process group plus a wall-clock backstop of 3x). Compilation time is reported separately
and is NOT charged to the budget (the prover arm's Lean elaboration is likewise reported separately); the budget
covers search only. Set `--cpu-seconds` identically across arms in the pre-registration.
Layout
- `property_bank.py` bank schema + validation + the always-on "no panic / no overflow" implicit property.
- `gen_harness.py` emits a Kani / proptest / cargo-fuzz project for one item from the bank.
- `run_baselines.py` runs the arms under the budget, emits one JSON result line per (item, arm).
- `bank/smoke.json` properties for the smoke crate (`../smoke/tiny`) and an example for the mutant corpus.
Status: all three arms run end to end through `run_baselines.py` (proptest + cargo-fuzz on the 23 kernel banks / smoke, Kani on the smoke crate; Kani handles
scalar-argument properties only, vec/option-argument properties are skipped for Kani). `--revision post` runs the same bank against the fixed
revision (negative control / spec gate). `bank/<kernel>.json` are the 23 kernel banks (blind authored; see `bank/README_PROVENANCE.md`);
`bench/ledger/baseline_sweep_proptest.jsonl` is the proptest sweep (4 CPU-s per property) on pre and post.
Harness calls use the fully qualified `lib::fn(...)` so argument names cannot shadow the function.
|