Module trap 

Trap-preservation obligations (VCR-VER-002, synth #166 / ordeal#59).

WASM operations like div_s, load/store, call_indirect, unreachable, and the float→int truncations (iN.trunc_fM_s/u) are partial: they trap on some inputs. A validator that proves only value equivalence over a total model cannot see a lowering that drops a trap — deleting a trapping guard looks value-equal (synth#633/#666/#665/#642/#709). This module is the thin synth-facing layer over ordeal::trap: it maps synth’s WasmOps to trap conditions built over synth’s own BV/Bool terms, and exposes the trap-preservation gate so “the trap survived the lowering” becomes a checkable obligation.

Boundary (unchanged from ordeal#59)

ordeal classifies operand/pointer bits — it never models op values (those are consumer-supplied) and does no floating-point arithmetic. Every builder here is a Bool/BV over the existing closed QF_BV fragment. A verdict of TrapVerdict::Preserved is an ordeal Unsat whose LRAT certificate is re-checked before it is returned, so soundness is that of the normal certificate-checked pipeline.

Which VC for which op class

• div/rem — the ARM lowering carries a value (the quotient/remainder), so the full prove_trap_equivalence (trap clause and guarded value clause) applies.
• load/store, call_indirect, unreachable — synth models no memory contents nor table values, so these use prove_trap_condition_equivalence (trap clause only). This is the ordeal#59 agreement.
• float→int trunc (i32/i64.trunc_f{32,64}_{s,u}, Phase B) — the trap predicate is a pure bit-pattern classifier over the float OPERAND’s bits (NaN/±∞ exponent patterns + sign-split monotonic magnitude thresholds, ordeal 0.9.1’s trap_trunc; floats enter as BV32/BV64, no FP theory). synth’s QF_BV model carries no float→int value function, so this class uses prove_trap_condition_equivalence (trap clause only) — exactly the #709 soundness surface: ARM VCVT saturates where WASM traps, so a lowering that keeps the saturated value but drops the guard is the bug shape this clause rejects.

Structs

CallIndirect

The operands of a call_indirect trap check (WASM §4.4.8) — the synth-BV mirror of ordeal::trap::CallIndirect.

DefineOrTrap

A value paired with the condition under which the op traps instead of producing it — the synth-BV/Bool mirror of ordeal::trap::DefineOrTrap. value is the op’s result (e.g. the ARM quotient); may_trap is one of the trap-condition builders below.

Enums

DivOp

Which division/remainder op, for trap_div.

FpFmt

An IEEE-754 binary interchange format, for the trunc-trap classifiers.

IntTarget

The integer target of a truncation, for fp_trunc_out_of_range.

TrapVerdict

The verdict of a trap-preservation gate.

TypeTrap

The type-check mode of a call_indirect, per its table — the synth-BV mirror of ordeal::trap::TypeTrap.

Functions

div_op

Map a division/remainder WasmOp (i32 or i64) to its DivOp; None for any non-div/rem op.

prove_trap_condition_equivalence

Trap-clause-only gate (orig.may_trap ⇔ opt.may_trap) — for ops whose value synth does not model (load/store, call_indirect, unreachable, float→int trunc). TrapVerdict::Preserved ⟹ the lowering neither drops nor spuriously adds the trap.

prove_trap_equivalence

Full trap-preservation gate (trap clause and guarded value clause) — for ops whose value synth models (div/rem). TrapVerdict::Preserved ⟹ the lowering preserves both traps and values.

trap_always

Trap condition for unreachable: an unconditional trap.

trap_call_indirect

Trap condition for call_indirect: bounds ∨ null-slot ∨ type.

trap_div

Trap condition for a div/rem op: divide-by-zero (all four) plus INT_MIN / -1 signed overflow (div_s ONLY). The width is taken from dividend — pass 32-bit terms for i32 ops, 64-bit for i64.

trap_mem_oob

Trap condition for an OOB load/store: a size-byte access at addr exceeds mem_bound (addr + size >u mem_bound, wraparound-safe). addr, size, and mem_bound must share a width; mem_bound is synth’s symbolic native-pointer linear-memory extent.

trap_trunc

Trap condition for iN.trunc_fM_s/u (WASM float→int truncation, #709): NaN ∨ ±∞ ∨ out-of-range classified purely over the float operand’s bit pattern (bits is the BV32/BV64 the float travels as — no FP theory). Pass the triple from trunc_op. bits must be exactly fmt.total_bits() wide (32 for f32, 64 for f64) — a width mismatch is an internal bug, so it panics loud rather than returning an ill-sorted term.

trunc_op

Map a float→int truncation WasmOp to its (float format, integer target, signedness) triple; None for any non-trunc op. Covers all six trunc variants synth’s decoder produces (i64.trunc_f32_s/u are not WasmOp variants; the raw trap_trunc builder still covers those shapes if they ever land).