feat(verify): VCR-VER-002 Phase B — float→int trunc trap class via ordeal 0.9.1 (#166)

[avrabe]

VCR-VER-002 Phase B — the float→int truncation trap class (#166, ordeal#59/TR-020)

Follows #723 (Phase A). ordeal 0.9.1 adds trap_trunc: the WASM iN.trunc_fM_s/u trap predicate (NaN ∨ ±∞ ∨ out-of-range) classified purely over the float operand's bit pattern — exponent-field patterns + sign-split monotonic magnitude threshold compares. Floats enter as BV32/BV64; no FP theory, pure QF_BV, LRAT-certified pipeline unchanged. This is exactly the #709 soundness surface: ARM VCVT saturates where WASM must trap, so a lowering that keeps the saturated value and drops the guard is value-equal and invisible to a value-only VC.

Wrapper (crates/synth-verify/src/trap.rs)

• trunc_op(WasmOp) → Option<(FpFmt, IntTarget, bool)> — maps all six decoder-reachable trunc variants (i32/i64.trunc_f{32,64}_{s,u}; i64.trunc_f32_* are not WasmOp variants, the raw builder still covers those shapes).
• trap_trunc(bits, fmt, target, signed) — ordeal's classifier over synth BV/Bool, loud width assert. Trap-clause-only VC class (synth models no float→int value function).
• Cargo pin 0.9 → 0.9.1 (trap_trunc is 0.9.1-only; the lockfile already resolved 0.9.1 since feat(verify): VCR-VER-002 — trap-preservation gate over ordeal::trap (#166) #723 — no lock change).

Red-first gate (tests/trap_preservation.rs, 6 → 11 tests) — which drops are caught

direction	result
guard-dropping lowering (may_trap=false), all six variants	CAUGHT — Dropped/Sat, counterexample validated as genuinely trapping against the real-float reference
signedness-confused guard (unsigned range check on i32.trunc_f32_s — NaN/∞ kept, thresholds wrong: the partial-drop VCVT shape)	CAUGHT — Sat, counterexample separates signed from unsigned trapping
guard-preserving lowering, all six variants	accepted — Preserved/Unsat, LRAT certificate re-checked
wrong-expectation control (claiming NaN doesn't trap at a ground input)	CAUGHT — non-vacuity of the ground gate

Classifier-encoding check (the ordeal#59 ask; synth's #709 table is the reference oracle)

The 31-row #709 boundary table evaluated two ways, every row self-checked against the real-float reference so the table cannot drift:

1. directly via ordeal::eval on the classifier — i32.trunc_f32_s: NaN / +∞ / −∞ / 3e9 / −3e9 trap, 2^31 (0x4F000000) TRAPS, −2^31 (0xCF000000) in-range, 2.5 in-range; i32.trunc_f32_u: −1.0 traps, 0.5 / −0.0 in-range, 2^32 traps; plus f64 and i64-target boundary anchors (largest-below-threshold floats, ±2^63, 2^64, −(2^31+1), …).
2. through the certificate-checked pipeline on the synth wrapper: at ground inputs, trap_trunc(const) ⇔ expected proven valid per pattern (certified Unsat).

Roadmap / claims

VCR-VER-002 title + description updated (Phase B landed, LANDED item 5); status stays proposed — the live-validator wiring gap is unchanged (trunc, like load/store / call_indirect / unreachable, is gated at the unit level pending the exec-model trap flag). claims.yaml SYNTH-VCR-VER-002-STATUS text updated verbatim; claim_check 18/18.

Gates

• cargo test -p synth-verify + --test trap_preservation (11/11) green
• cargo test --workspace green (119 test binaries, 0 failures)
• cargo clippy --workspace --all-targets -- -D warnings clean, cargo fmt --check clean
• python3 scripts/claim_check.py claims.yaml — 18/18 claims hold

Refs #166, #242, ordeal#59. Follows #723.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 94.11765% with 1 line in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-verify/src/trap.rs	94.11%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!