trap_gate systemic trap-equivalence gate (#284/#279) is never called by any pass — inert; trap-soundness still rests on the is_no_trap stopgaps it claims to supersede

[avrabe]

Summary

The systemic trap-equivalence gate added in #284 (commit a1f3daf, "feat(#279): systemic trap-equivalence gate … supersedes is_no_trap stopgaps") — loom-core/src/trap_gate.rs — is never called by any optimization pass or the verify path. It is dead code. #279 was closed on the belief this gate is now the systemic authority, but it provides zero runtime protection; actual trap-soundness still rests entirely on the per-pass is_no_trap static guards that #273/#274/#276/#278/#281 each added by hand.

Evidence (loom 1.2.0 @ a1f3daf)

The module doc asserts it is active authority:

//! Systemic trap-equivalence gate (issue #279).
//! This module is the durable cure: a trap-equivalence obligation … supersedes the per-pass is_no_trap stopgaps

But the only reference to trap_gate anywhere outside its own file is the module declaration:

loom-core/src/lib.rs:15425:  pub mod trap_gate;

Every public entry point has 0 external callers (grep across loom-core/src + loom-cli/src, excluding trap_gate.rs and its own #[test]s):
check_div_transform, check_mem_transform, check_select_discard, check_trap_equivalence_under, prove_under_premises, signed_div_value, mem_bound_from_pages — none referenced.

What the optimize/verify path actually consults for trap-safety is Summary::is_no_trap (verify.rs:464, lib.rs:8842/8919/13631, summary.rs) — the ad-hoc stopgaps the gate claims to supersede. The gate's 13 #[test]s exercise it in isolation, so it compiles and CI is green, but no pass ever calls it.

Why it matters

• False claim / false-closed: Systemic trap-preservation gate (#257 for traps): verify trap-equivalence via ordeal trap-semantics #279 is closed as "systemic gate delivered"; the delivered gate is inert. The "supersedes the per-pass stopgaps … this gate is the authority" claim is not true at runtime.
• Latent soundness risk: the value of a systemic gate is catching trap-eliminating folds that no hand-written stopgap covers — exactly the constant-folding eliminates the mandatory div_s(INT_MIN,-1) overflow trap — optimized module returns INT_MIN where the original traps (i32 + i64) #273–constant-condition select fold drops the non-selected arm, eliminating its trap (WASM select is eager) — distinct from #278 #281 failure mode. Because the gate is never invoked, a future fold not guarded by an is_no_trap check would ship a silent trap-elimination miscompile, and the mechanism advertised to catch the whole class would not fire. If anyone removes an is_no_trap stopgap trusting the gate, soundness regresses silently.

Current output soundness is intact (verified: OOB-load/store, div/rem-by-0, INT_MIN/-1 folds all still trap after loom optimize — the is_no_trap stopgaps hold). This report is about the inert safety-critical gate and its overstated claim, not a current miscompile.

Suggested action

Wire trap_gate into the passes it was built for (div/mem/select-discard transforms) so it actually gates those folds, or downgrade the module/commit claims and reopen #279 until the systemic gate is on the runtime path.

[avrabe]

Triage — confirmed, actionable, safety-relevant. Reproduced against main @ 7475943:

check_div_transform:        0 external refs
check_mem_transform:        0 external refs
check_select_discard:       0 external refs
check_trap_equivalence_under: 0 external refs

(grep across loom-core/src + loom-cli/src, excluding trap_gate.rs and its #[cfg(test)].) The only trap_gate refs outside the module are the pub mod declaration and one test-only use (prove_under_premises, exercised by a #231 invariant test). The gate is dead code on the runtime path; your report is accurate, and current output-soundness holding is purely down to the is_no_trap/static-exclusion stopgaps.

#279 reopened (it was false-closed).

Fix design (additive backstop, not a capability change): the per-fold static guards stay as the feature-independent floor; trap_gate is wired in at the div/rem, load/store, and select-discard fold sites as a proof backstop — when a trap-relevant fold fires under the verification feature, the gate must prove trap-and-value equivalence Unsat, else the fold reverts. This makes the gate the advertised authority (catches any future static-guard gap) with no behavioral change when proofs pass and none at all when the feature is off. Tests will assert the gate is actually invoked on the runtime path (closing the exact gap this issue found). Targeting v1.2.2.

[avrabe]

Fix up for review: #289 (branch fix/288-wire-trap-gate).

trap_gate is now on the runtime path as an additive, feature-gated backstop — the static guards are untouched (feature-independent floor); under verification the new trap_backstop::accept_div_const_folds is called inside the constant_folding pass and reverts any div/rem const-fold ordeal can't prove trap-free (LRAT cert re-checked). Routed: div_s, div_u, rem_u.

Anti-regression (the exact gap this issue found): test_288_backstop_blocks_trapping_div_fold bypasses the static guard in-test and asserts the gate blocks div_s(INT_MIN,-1) / div_u(x,0) — so the gate, not the stopgap, is proven to be the authority; test_288_backstop_observes_and_accepts_safe_div_fold proves it's consulted on the live path.

Documented gaps (honest, static guard remains sole authority):

• rem_s — NOT routed: ordeal's trap_div over-approximates rem_s(INT_MIN,-1) as trapping, but WASM defines it as 0 (no trap — only div_s has the overflow trap). Routing it would falsely revert a valid fold. Filed trap_div overflow clause is div-only: rem_s(INT_MIN,-1) is falsely modeled as trapping ordeal#84 for a divisor-zero-only trap_rem predicate; pinned by a trap_gate test until fixed.
• 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 (loads excluded from is_pure_pusher) → no live fold to back-check; check_mem_transform stays covered by its own unit tests.
• select-arm-discard (constant-condition select fold drops the non-selected arm, eliminating its trap (WASM select is eager) — distinct from #278 #281): fold lives in rewrite_pure below the ordeal/instruction boundary; arm trap condition not reconstructable there.

rivet: TEST-TRAP-GATE-RUNTIME-PATH added (mitigates UCA-5/UCA-21, tag v122). Builds green (default + --features verification: 480 pass; --no-default-features compiles+green). For review — not auto-merging (safety-critical).