Translation validation: verify refinement with traps as first-class state (Alive2 encoding), not value-equivalence + guards

[avrabe]

Ask

Move trap-preservation from guards around the validator to the validator's encoding itself: verify refinement, not value-equivalence, with traps as a first-class component of the abstract state. This is Alive2's central design decision, and it is the named, published answer to the exact class loom shipped five times (#273/#274/#276/#278/#281).

Why the current shape leaves the hole open

The Z3 translation validator proves value equivalence over a model in which every Wasm operation is total — traps are unmodelled. trap_gate.rs says so directly, and that is why an identity rewrite (x * 0 → 0, dropping a dead div result, constant-condition select) could be certified equivalent while deleting a mandatory trap.

The current defence is sound but structural: a recursive trap-freedom guard (is_no_trap_expr / is_forwardable_expr) gates ~25 fold sites, with trap_backstop.rs calling into trap_gate. That is a per-rule allowlist. The residual risk is exactly the one the research names: a new rewrite added tomorrow is trap-unsafe by default and only safe if its author remembers the guard. The oracle still cannot see traps; we are relying on the guard never being forgotten.

The prior art (this is not new theory)

Alive2: Bounded Translation Validation for LLVM — Lopes, Lee, Hur, Liu, Regehr, PLDI 2021 (paper, repo).

The load-bearing decision: the correctness relation is refinement, not equality — a transformation may only eliminate non-determinism/UB, never introduce it, degenerating to equivalence only when no UB exists. UB, poison and undef are modelled as first-class parts of the abstract state, so an optimization that removes a mandatory error condition is a refinement violation and is rejected by construction — no allowlist required.

Empirical warrant, and the part that should interest us most: running Alive2 over LLVM's own unit tests found 47 new bugs (28 fixed) and forced 8 patches to the LLVM Language Reference. Building a trap-faithful encoding is itself what exposed that the specification was underspecified. That is our recurring fault class, and it means this work pays off twice.

Concretely

1. Encode trap as state. Extend the validator's abstract state with an explicit trap/⊥ component per Wasm trapping op (div/rem by zero, INT_MIN / -1, OOB load/store, unreachable, indirect-call type mismatch).
2. Switch the relation to refinement. optimized ⊑ original: for every input, if the original traps the optimized may do anything; if the original does not trap, the optimized must not trap and must agree on values. Deleting a reachable trap becomes unprovable — the encoding rejects it without any syntactic guard.
3. Then demote the guards to a backstop. Keep is_no_trap_expr as defence-in-depth, but stop it being the primary mechanism.
4. Relationship to Systemic trap-preservation gate (#257 for traps): verify trap-equivalence via ordeal trap-semantics #279. The systemic trap-gate issue is the certificate-checked checker; this issue is the encoding it should be checking. They compose: refinement encoding = the right property; ordeal certificate = independently re-checkable evidence for it.

Honest note

This is a real piece of work, not a config change, and Alive2 is bounded (it validates within bounds, not a whole-compiler proof). The claim here is only that it converts a class of "green but wrong" into "unprovable", which is exactly the trade we want.

[avrabe]

Triage — accepted as the durable, correct architecture for the trap class; this is a roadmap-level methodology change, not a fold-site fix. Strongly agree with the framing.

Confirmed against the tree

• verify.rs models every Wasm op as total — traps unmodelled (trap_gate.rs documents this directly).
• The current defence is exactly the allowlist you describe: 7 guard call sites (is_no_trap_expr / is_forwardable_expr / trap_backstop::*) protecting the trapping fold sites. Sound today, but trap-unsafe-by-default for any rewrite added tomorrow — the residual risk is real and it's the 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 #288 lesson in a different dress (a safety mechanism that depends on the author remembering it).

Why this is the right cure (and fits loom's charter exactly)

loom's stated philosophy is "if we cannot prove it correct, we must not do it." Refinement-with-trap-as-first-class-state converts the entire class from "green but wrong" (certified value-equal while dropping a mandatory trap) into "unprovable" (deleting a reachable trap is a refinement violation, rejected by construction). That is precisely the trade the charter demands — the guard allowlist becomes defence-in-depth, not the primary mechanism.

The strategic sequencing point (important)

This should be done as part of the Tier-2 verify.rs → ordeal migration, not after it. That migration is now unblocked (ordeal#70 symbolic-index arrays shipped in 0.11.0; loom is on 0.17.0). It would be waste to port the total-model, value-equivalence encoding onto ordeal and then re-architect it to refinement. The two are one piece of work:

• Systemic trap-preservation gate (#257 for traps): verify trap-equivalence via ordeal trap-semantics #279 (closed) delivered the certificate-checked checker (ordeal, re-checkable LRAT evidence).
• Translation validation: verify refinement with traps as first-class state (Alive2 encoding), not value-equivalence + guards #300 is the encoding that checker should evaluate: optimized ⊑ original with an explicit trap/⊥ component per trapping op (÷0, INT_MIN/-1, OOB load/store, unreachable, indirect-call type mismatch).
• Together: refinement encoding = the right property; ordeal certificate = independently re-checkable evidence for it.

The 'pays off twice' warrant

The Alive2 result (47 LLVM bugs, 8 LangRef patches, surfaced by building the trap-faithful encoding) is directly relevant: a trap-faithful Wasm refinement encoding is likely to expose where our own optimization specs are underspecified — the recurring fault's root, not just its symptoms.

Disposition

Landing this as a design decision + verify.rs architecture requirement (refinement-based translation validation; trap as first-class abstract state), linked to the trap hazards (UCA-5 "ISLE folds trapping op to constant", UCA-21 "Z3 omits trap condition") — the same hazards the guard allowlist mitigates today. It becomes the defining shape of the Tier-2 migration: port to ordeal and switch equality→refinement in the same effort, keeping the 7 guards as backstop. This is an epic (bounded validator, per-op trap state, refinement relation, differential vs the current encoding) — I'll draft the phased plan as the migration's design doc. Not a quick change; correctly the most important verifier work on the board.

Honest scope caveat noted and agreed: bounded validation, not whole-compiler proof — the win is the class-level 'wrong→unprovable' conversion.