fix(#288): wire trap_gate onto the runtime path (additive trap backstop)

[avrabe]

Summary

trap_gate (the systemic trap-equivalence gate, #279/#284) was dead code — its transform-checking entry points (check_div_transform, check_mem_transform, check_select_discard) had zero callers. Trap soundness therefore rested entirely on the per-fold static guards (#273/#274/#276/#278/#281); the gate provided zero runtime protection (#288, #279 false-closed on the belief it was the authority).

This PR wires the certificate-checked gate onto the constant_folding runtime path as an additive proof backstop, gated behind the verification feature.

What was wired

• New loom_core::trap_backstop module. For every div/rem-on-constants fold that fires in constant_folding, ordeal must prove the op was trap-free (orig.may_trap ⇔ false, LRAT certificate re-checked) via the new trap_gate::check_div_discard. A non-accepted verdict reverts that function's fold.
• Routed kinds: div_s, div_u, rem_u — ordeal's trap_div models their trap condition exactly (concrete constant operands ⇒ no symbolic slack).
• The backstop runs after the fold, before the Z3 value validator — which cannot see traps over its total model, the exact reason the five miscompiles slipped through.

Additive-backstop design (no capability change)

Every existing static guard is kept untouched (the is_simple_pure_instr div/rem exclusion, the div_s(INT_MIN,-1) const-fold refusal in rewrite_pure, the vacuum may-trap-load keep, the select is_no_trap_expr guard). When a guard holds, no trapping fold fires and behavior is unchanged. The backstop only catches a trapping fold that slipped a guard. With the verification feature off, trap_backstop is compiled out entirely and behavior is byte-identical.

Documented remaining gaps (static guard stays sole authority)

• rem_s is deliberately not routed: ordeal's trap_div over-approximates it — it shares the INT_MIN/-1 overflow disjunct with div_s, but per the WASM spec rem_s(INT_MIN,-1) does not trap (result 0). Routing it would falsely reject a genuinely-safe fold and revert a valid optimization (a capability regression). Its exact static constant-folding eliminates the mandatory div_s(INT_MIN,-1) overflow trap — optimized module returns INT_MIN where the original traps (i32 + i64) #273 guard (which folds it to 0) remains authority. Pinned by trap_gate::tests::rem_s_int_min_is_over_approximated_rejected so a future ordeal fix is noticed. (Filed as tool friction against ordeal in spirit — the disjunct is spurious for rem.)
• mem-discard (constant-folding eliminates a trapping operand via zero-annihilation (x*0, 0*x, x&0) — deletes OOB-load/div traps (distinct from #273/#274) #278): the vacuum load; drop fold never fires (is_pure_pusher excludes loads), so there is no live fold to back-check at that site. check_mem_transform stays exercised by its own unit tests only — loom carries no symbolic memory bound at the instruction layer to feed it soundly on a live fold.
• select-arm-discard (constant-condition select fold drops the non-selected arm, eliminating its trap (WASM select is eager) — distinct from #278 #281): the fold lives in loom-shared's rewrite_pure, below the ordeal dependency boundary, and the discarded arm is a value term whose trap condition loom does not reconstruct at the instruction layer. Its static is_no_trap_expr guard remains sole authority.

Per the conservatism rule, sites that cannot be modeled soundly with the existing API + a small clearly-correct helper were left on their static guard and documented rather than modeled dubiously.

Anti-regression tests (the point of #288)

• test_288_backstop_observes_and_accepts_safe_div_fold — the gate observes the 20/4 fold fire and accepts it.
• test_288_backstop_blocks_trapping_div_fold — a constructed div_s(INT_MIN,-1) and div_u(x,0) fold is blocked by the gate with the static guard bypassed in-test, proving the gate (not the static guard) is the runtime authority.
• test_288_constant_folding_pass_keeps_safe_fold — end-to-end, the pass with the backstop live still folds a trap-free const div (no over-blocking).
• New check_div_discard unit tests: accept trap-free, reject overflow, reject ÷0, pin the rem_s over-approximation.

rivet

Adds TEST-TRAP-GATE-RUNTIME-PATH (verifies REQ-1/REQ-6, mitigates UCA-5/UCA-21, verifies CC-4/CC-20; release tag v122). rivet validate → PASS.

Build / test results (macOS homebrew Z3, isolated target dir), honestly stated

• cargo test --release -p loom-core (default = includes verification): test result: ok. 480 passed; 0 failed; 2 ignored (lib suite) — all green.
• cargo test --release -p loom-core --features verification: test result: ok. 480 passed; 0 failed; 2 ignored — all green.
• cargo test --release -p loom-core --no-default-features (backstop compiled out, proves byte-identical path compiles + passes): all green.
• cargo clippy --release -p loom-core --features verification: clean; cargo fmt --all applied.

Do not merge — for user review.

Fixes #288
Refs #279

🤖 Generated with Claude Code