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