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.