feat(verify): VCR-VER-002 — trap-preservation gate over ordeal::trap (#166)

[avrabe]

VCR-VER-002 — trap-preservation as an oracle-gated obligation

Consumes ordeal 0.9.0's new ordeal::trap module in synth-verify so a lowering that drops a WASM trap (div-by-zero/overflow guard, OOB bounds check, call_indirect bounds/null/type, unreachable) can no longer pass value-only equivalence. Systematic end of the per-op soundness whack-a-mole (#633/#666/#665/#642/#709).

Refs #166, #242, ordeal#59.

What landed, per step

• Step 1 — bump. synth-verify ordeal 0.4 → 0.9 (API-compatible; all 53 unit tests unchanged). No ordeal pin in MODULE.bazel to touch.
• Step 2 — synth_verify::trap wrapper. Thin synth-facing layer over ordeal::trap: div_op(WasmOp)->DivOp + trap_div, trap_mem_oob, trap_call_indirect (both TypeTrap::Runtime and StaticallyDischarged — synth's closed-world homogeneous tables use the latter, matching ArmOp::CallIndirect.type_check == None), trap_always. prove_trap_equivalence (full VC) / prove_trap_condition_equivalence (trap-clause only) return a TrapVerdict {Preserved | Dropped(model) | Unknown}; Preserved re-checks the LRAT certificate before returning. Added Bool::from_ordeal (pub(crate)).
• Step 3 — RED-FIRST GATE (tests/trap_preservation.rs, 6 tests). Non-vacuity proof: for every op class a trap-DROPPING lowering is CAUGHT and a trap-PRESERVING lowering accepted.
• Step 4 — validator method. TranslationValidator::verify_div_rem_trap_preservation — a dedicated always-checks method gating i32 div/rem on the full VC, with the ARM trap condition derived structurally from the Udf guard (sound in the reject direction). Kept as a separate method (folding into verify_equivalence would wrongly reject the legitimate value-only div rules, since the guard is an encoder-expansion artifact). See the live-path gap below.
• Step 5 — rivet + claims. VCR-VER-002 roadmap entry (status in-progress). Pinned SYNTH-VCR-VER-002-STATUS in claims.yaml; claim_check 18/18.

Red-first gate output (Sat-on-drop / Unsat-on-preserve)

running 6 tests
test unreachable_elision_is_caught_and_preservation_accepted ... ok
test call_indirect_statically_discharged_drop_is_caught_and_preservation_accepted ... ok
test call_indirect_runtime_type_drop_is_caught_and_preservation_accepted ... ok
test load_store_oob_bounds_drop_is_caught_and_preservation_accepted ... ok
test signed_div_overflow_only_drop_is_caught ... ok
test div_rem_all_four_ops_catch_the_drop_and_accept_preservation ... ok
test result: ok. 6 passed; 0 failed

Op classes that catch the drop: div/rem (all four ops, full trap+value VC; drop caught with a divisor==0 counterexample; partial signed-overflow-only drop caught), load/store OOB (bounds-removal caught), call_indirect (both TypeTrap modes: runtime type-check drop #676-shape AND all-guards drop; closed-world bounds+null drop), unreachable (trap elision caught).

Validator method (--features arm): div_lowering_without_guard_is_rejected_as_trap_drop (bare UDIV — the #633/#666 shape — rejected with divisor==0), div_lowering_with_guard_preserves_the_trap, signed_div_guard_preserves_both_zero_and_overflow_traps, trap_preservation_gate_rejects_non_div_ops (incl. i64 rejection), all green.

Wired vs documented follow-on (honest scope)

• In place now: a dedicated, unit-tested verify_div_rem_trap_preservation that ALWAYS checks the trap conjunct for i32 div/rem; sound in the reject direction (no Udf guard ⇒ Invalid, catching the thumb-2: i64.div_s(INT64_MIN, -1) silently returns INT64_MIN instead of trapping (overflow guard missing on i64 path; i32 path has it) #633/rv32: i32.rem_s(INT_MIN,-1) spuriously traps — div_s overflow ebreak guard wrongly copied into rem_s (irem_s must return 0) #666/thumb-2: call_indirect emits no bounds-check and no type-check — OOB/wrong-type index does an uncontrolled indirect branch instead of trapping (WASM 4.4.8) #642 class).
• NOT yet on the live path: the validator's live entry points (verify_rule → verify_equivalence → verify_equivalence_parameterized) remain value-only and do not yet invoke the new method — so verify_rule on an unguarded div does not yet reject. Making it a live-path conjunct requires updating the value-only div-rule fixtures (comprehensive_verification.rs) to carry the guard; deferred.
• Documented follow-on (why in-progress): the validator's ARM side is value-only (ArmState has no trap flag) and the div guard is an encoder-expansion artifact, so div/rem uses a structural Udf-presence proxy (not a full proof the guard fires on exactly div0∨overflow), i32-only; and load/store/call_indirect/unreachable have no ARM trap term on this path — they stay unit-gated. Closing the gap needs a may_trap flag threaded through ArmState, or decoding the emitted guard bytes in expansion_validator.

Gates

cargo fmt --check (exit 0), cargo clippy --workspace --all-targets -D warnings (exit 0), cargo test --workspace (all green), claim_check.py 18/18 — all green.

DO NOT MERGE — maintainer gates and will re-run the red-first gate.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 95.55556% with 8 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-verify/src/translation_validator.rs	96.52%	4 Missing ⚠️
crates/synth-verify/src/trap.rs	93.54%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!