synth_verify/

translation_validator.rs

//! Translation Validator - Proves equivalence between WASM and ARM code
//!
//! This module implements SMT-based translation validation inspired by Alive2.
//! For each synthesis rule WASM → ARM, we prove that the ARM code has
//! semantically equivalent behavior to the WASM code.
//!
//! # Verification Approach
//!
//! 1. Create symbolic inputs for both WASM and ARM
//! 2. Encode WASM semantics as SMT formula phi_wasm
//! 3. Encode ARM semantics as SMT formula phi_arm
//! 4. Assert: phi_wasm(inputs) == phi_arm(inputs)
//! 5. Check satisfiability - if UNSAT, then equivalence is proven
//!
//! # Example
//!
//! For the rule: WASM `i32.add` -> ARM `ADD Rd, Rn, Rm`
//!
//! We prove: forall a,b. i32.add(a, b) == ADD(a, b)

use crate::arm_semantics::{ArmSemantics, ArmState};
use crate::solver::{CheckOutcome, new_solver};
use crate::term::{BV, Bool};
use crate::wasm_semantics::WasmSemantics;
use synth_core::WasmOp;
use synth_synthesis::{ArmOp, Reg, SynthesisRule};
use thiserror::Error;

/// Verification error types
#[derive(Debug, Error)]
pub enum VerificationError {
    #[error("Translation is incorrect: counterexample found")]
    CounterexampleFound {
        wasm_result: String,
        arm_result: String,
        inputs: Vec<String>,
    },

    #[error("Verification timeout after {0}ms")]
    Timeout(u64),

    #[error("Unsupported operation: {0}")]
    UnsupportedOperation(String),

    #[error("SMT solver error: {0}")]
    SolverError(String),

    #[error("Invalid synthesis rule: {0}")]
    InvalidRule(String),
}

/// Result of translation validation
#[derive(Debug, Clone, PartialEq)]
pub enum ValidationResult {
    /// Translation is provably correct
    Verified,

    /// Counterexample found - translation is incorrect
    Invalid { counterexample: Vec<(String, i64)> },

    /// Verification inconclusive (timeout or unsupported operations)
    Unknown { reason: String },
}

/// Module facts that define the WASM-side `call_indirect` trap condition
/// (VCR-VER-002, #166): what the SPEC demands for the dispatched table, to be
/// checked against the guards the selector actually resolved into the
/// `ArmOp::CallIndirect` pseudo-op.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CallIndirectSpec {
    /// The dispatched table's element count (compile-time, per #642).
    pub table_size: u32,
    /// Whether the table may contain uninitialized (null) slots — if so, the
    /// lowering MUST carry the #664 null check.
    pub may_have_null_slot: bool,
    /// `Some(expected_type_id)` when the table is heterogeneous and WASM's
    /// §4.4.8 type check must be discharged at RUNTIME (#676); `None` when
    /// the closed-world verdict discharges it at compile time.
    pub heterogeneous_expected_type: Option<u32>,
}

/// Translation validator over the configured SMT engine (see
/// [`crate::solver::new_solver`]: ordeal by default, optionally
/// cross-checked against Z3 when `SYNTH_SOLVER_DIFF=1`).
pub struct TranslationValidator {
    wasm_encoder: WasmSemantics,
    arm_encoder: ArmSemantics,
    timeout_ms: u64,
}

impl Default for TranslationValidator {
    fn default() -> Self {
        Self::new()
    }
}

impl TranslationValidator {
    /// Create a new translation validator
    pub fn new() -> Self {
        Self {
            wasm_encoder: WasmSemantics::new(),
            arm_encoder: ArmSemantics::new(),
            timeout_ms: 30000, // 30 seconds default
        }
    }

    /// Set verification timeout in milliseconds
    pub fn set_timeout(&mut self, timeout_ms: u64) {
        self.timeout_ms = timeout_ms;
    }

    /// Verify a synthesis rule
    ///
    /// Proves that the ARM code generated by the rule has equivalent semantics
    /// to the WASM code matched by the pattern.
    pub fn verify_rule(&self, rule: &SynthesisRule) -> Result<ValidationResult, VerificationError> {
        // Extract WASM operation from pattern
        let wasm_op = match &rule.pattern {
            synth_synthesis::Pattern::WasmInstr(op) => op,
            _ => {
                return Err(VerificationError::UnsupportedOperation(
                    "Only single WASM instruction patterns are supported".to_string(),
                ));
            }
        };

        // Extract ARM operations from replacement
        let arm_ops = match &rule.replacement {
            synth_synthesis::Replacement::ArmInstr(op) => vec![op.clone()],
            synth_synthesis::Replacement::ArmSequence(ops) => ops.clone(),
            _ => {
                return Err(VerificationError::UnsupportedOperation(
                    "Only ARM instruction replacements are supported".to_string(),
                ));
            }
        };

        // VCR-VER-002 (#166): PARTIAL ops (they trap on some inputs) MUST go
        // through the trap-preservation VC — a value-only proof over a total
        // model cannot see a dropped trap, and for div/rem the value-only
        // query is not even well-posed (SMT bvsdiv is total where WASM
        // traps). The trap VC subsumes the value obligation where the value
        // is modeled (div/rem: trap clause AND guarded value clause).
        if Self::is_trap_gated_op(wasm_op) {
            return self.verify_trap_preservation(wasm_op, &arm_ops);
        }

        self.verify_equivalence(wasm_op, &arm_ops)
    }

    /// The partial-op surface whose lowerings are MANDATORILY routed through
    /// the trap-preservation VC by [`Self::verify_rule`].
    fn is_trap_gated_op(wasm_op: &WasmOp) -> bool {
        matches!(
            wasm_op,
            WasmOp::I32DivS
                | WasmOp::I32DivU
                | WasmOp::I32RemS
                | WasmOp::I32RemU
                // i64 div/rem (#756): field-derived trap-condition VC (the
                // pseudo-op carries the guard as an `elide_*` boolean; the
                // 64-bit quotient is not modeled, so no value clause).
                | WasmOp::I64DivS
                | WasmOp::I64DivU
                | WasmOp::I64RemS
                | WasmOp::I64RemU
                | WasmOp::Unreachable
                | WasmOp::I32Load { .. }
                | WasmOp::I32Load8S { .. }
                | WasmOp::I32Load8U { .. }
                | WasmOp::I32Load16S { .. }
                | WasmOp::I32Load16U { .. }
                | WasmOp::I32Store { .. }
                | WasmOp::I32Store8 { .. }
                | WasmOp::I32Store16 { .. }
                | WasmOp::I32TruncF32S
                | WasmOp::I32TruncF32U
                // f64→i32 trunc (#756): D-register domain guard, condition-only
                // VC. NOT `I64TruncF64S/U` / `I64TruncF32S/U`: since #869 the
                // shipping `select_with_stack` DOES lower them (i64 domain
                // guard + #782 decompose), but they are never expressed as a
                // `SynthesisRule` (this gate's input), and the symbolic ARM
                // exec model does not yet interpret the F64 compare/decompose
                // chain their guard rides on — a gate entry here would
                // false-red, not protect. Their trap behavior is
                // EXECUTION-gated instead (the #869 differential runs every
                // NaN/±inf/2^63/-2^63/2^64 trap row on both sides); the
                // symbolic wiring is the named #756-class residual.
                | WasmOp::I32TruncF64S
                | WasmOp::I32TruncF64U
        )
    }

    /// Verify equivalence between a WASM operation and ARM operations
    pub fn verify_equivalence(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
    ) -> Result<ValidationResult, VerificationError> {
        self.verify_equivalence_parameterized(wasm_op, arm_ops, &[])
    }

    /// Verify equivalence with concrete parameter values
    pub fn verify_equivalence_parameterized(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
        concrete_params: &[(usize, i64)],
    ) -> Result<ValidationResult, VerificationError> {
        let mut solver = new_solver();

        // Create inputs - some symbolic, some concrete
        let num_inputs = self.get_num_inputs(wasm_op);
        let mut inputs: Vec<BV> = Vec::new();

        for i in 0..num_inputs {
            let input = if let Some((_, value)) = concrete_params.iter().find(|(idx, _)| *idx == i)
            {
                // Concrete value
                BV::from_i64(*value, 32)
            } else {
                // Symbolic value
                BV::new_const(format!("input_{}", i), 32)
            };
            inputs.push(input);
        }

        // Encode WASM semantics
        let wasm_result = self.wasm_encoder.encode_op(wasm_op, &inputs);

        // Encode ARM semantics
        let arm_result = self.encode_arm_sequence(arm_ops, &inputs)?;

        // Assert that results are NOT equal
        // If this is UNSAT, then the results are always equal (proven correct)
        // If this is SAT, we found a counterexample
        solver.assert(&wasm_result.eq(&arm_result).not());

        match solver.check() {
            CheckOutcome::Unsat => {
                // Proven correct - no inputs exist where results differ
                Ok(ValidationResult::Verified)
            }

            CheckOutcome::Sat => {
                // Found counterexample: read the differing inputs back from
                // the model (symbolic inputs only — concrete params have no
                // model entry). Values are reported unsigned, as before.
                let mut counterexample = Vec::new();
                for (i, input) in inputs.iter().enumerate() {
                    if let Some(value) = solver.value(input)
                        && let Ok(int_val) = i64::try_from(value)
                    {
                        counterexample.push((format!("input_{}", i), int_val));
                    }
                }

                Ok(ValidationResult::Invalid { counterexample })
            }

            CheckOutcome::Unknown(reason) => {
                // Verification inconclusive
                Ok(ValidationResult::Unknown {
                    reason: format!("SMT solver returned unknown: {reason}"),
                })
            }
        }
    }

    /// Encode a sequence of ARM operations
    fn encode_arm_sequence(
        &self,
        arm_ops: &[ArmOp],
        inputs: &[BV],
    ) -> Result<BV, VerificationError> {
        let mut state = ArmState::new_symbolic();

        // Initialize input registers
        for (i, input) in inputs.iter().enumerate() {
            let reg = match i {
                0 => Reg::R0,
                1 => Reg::R1,
                2 => Reg::R2,
                _ => {
                    return Err(VerificationError::UnsupportedOperation(format!(
                        "Too many inputs: {}",
                        inputs.len()
                    )));
                }
            };
            state.set_reg(&reg, input.clone());
        }

        // Execute ARM operations
        for arm_op in arm_ops {
            self.arm_encoder.encode_op(arm_op, &mut state);
        }

        // Extract result from R0 (ARM calling convention)
        Ok(self.arm_encoder.extract_result(&state, &Reg::R0))
    }

    /// Verify operation for all parameter values in a range
    pub fn verify_parameterized_range<F>(
        &self,
        wasm_op: &WasmOp,
        create_arm_ops: F,
        param_index: usize,
        range: std::ops::Range<i64>,
    ) -> Result<ValidationResult, VerificationError>
    where
        F: Fn(i64) -> Vec<ArmOp>,
    {
        for value in range {
            let arm_ops = create_arm_ops(value);
            let result =
                self.verify_equivalence_parameterized(wasm_op, &arm_ops, &[(param_index, value)])?;

            match result {
                ValidationResult::Verified => continue,
                ValidationResult::Invalid { counterexample } => {
                    return Ok(ValidationResult::Invalid {
                        counterexample: counterexample
                            .into_iter()
                            .map(|(k, v)| (format!("{} (param={})", k, value), v))
                            .collect(),
                    });
                }
                ValidationResult::Unknown { reason } => {
                    return Ok(ValidationResult::Unknown {
                        reason: format!("Failed at param={}: {}", value, reason),
                    });
                }
            }
        }

        Ok(ValidationResult::Verified)
    }

    /// VCR-VER-002 (#166): mandatory **trap-preservation** obligation for the
    /// partial-op lowerings whose ARM trap condition synth can DERIVE from the
    /// emitted sequence. The ARM side is no longer a structural `Udf`-presence
    /// proxy: [`ArmSemantics::encode_sequence_br`] threads a `may_trap` term
    /// through the exec model — guard branches condition it, `UDF` execution
    /// accumulates it — so a dropped, inverted, or wrong-register guard
    /// derives a trap condition that fails the VC.
    ///
    /// # Covered classes (LIVE, derived ARM trap term)
    ///
    /// | class | VC | operand convention |
    /// |---|---|---|
    /// | i32 div/rem | full ([`crate::trap::prove_trap_equivalence`]: trap AND guarded value) | dividend R0, divisor R1, result R0 |
    /// | i64 div/rem | trap-condition only (field-derived; 64-bit quotient not modeled) | divisor R2:R3 (`rmlo`/`rmhi`), guards from the pseudo-op's `elide_*` fields |
    /// | `unreachable` | trap-condition only | none |
    /// | i32 load/store (all widths) | trap-condition only (no memory-contents model) | address R0 (+ store value R1), linear-memory size R10 |
    /// | `i32.trunc_f32_s/u` | trap-condition only (no float→int value model) | operand S0, result R0 |
    /// | `i32.trunc_f64_s/u` | trap-condition only (no float→int value model) | operand D0, bound scratch D1, result R0 |
    ///
    /// `call_indirect` goes through
    /// [`Self::verify_call_indirect_trap_preservation`] (it needs module
    /// facts as the spec side).
    ///
    /// # i64 div/rem trust boundary (like `call_indirect`)
    ///
    /// ARM32 has no 64-bit divide instruction: the shipped lowering emits an
    /// `ArmOp::I64Div{S,U}`/`I64Rem{S,U}` PSEUDO-OP whose result registers the
    /// exec-model leaves symbolic (no `bvsdiv` term) and whose trap guards are
    /// carried as `elide_zero_guard`/`elide_overflow_guard` boolean FIELDS.
    /// The gate certifies the SELECTOR's guard-elision decision: the ARM trap
    /// term is CONSTRUCTED from those fields (a set `elide_*` deletes the
    /// corresponding clause), so a lowering that elides a guard whose fact was
    /// not discharged is reported `Invalid`. The encoder's expansion of the
    /// pseudo-op into `ORRS`/`BNE`/`UDF`/library-call bytes is separately
    /// execution-gated (the i64 div/rem CI oracles).
    ///
    /// # Held out, honestly
    ///
    /// - **`i64.trunc_f64_s/u`** — the selector loud-declines it (i64 register
    ///   pairs on 32-bit ARM are unsupported), so there is NO shipped lowering
    ///   to derive an ARM trap term from. The trap CLASSIFIER for these ops
    ///   (`trap_trunc(F64, I64, …)`, incl. the item-4 2^63/-2^63/2^64
    ///   boundaries) is unit-gated in `tests/trap_preservation.rs`.
    pub fn verify_trap_preservation(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
    ) -> Result<ValidationResult, VerificationError> {
        match wasm_op {
            WasmOp::I32DivS | WasmOp::I32DivU | WasmOp::I32RemS | WasmOp::I32RemU => {
                self.verify_div_rem_trap_preservation(wasm_op, arm_ops)
            }
            // i64 rem_u/rem_s carry a REAL value model now (native
            // `BvTerm::Urem`/`bvsrem` — VCR-VER, #825/#836): the VC asserts
            // both the ÷0 trap AND the 64-bit remainder value, so a lowering
            // that computes the wrong remainder — or writes it to the wrong
            // register pair — is rejected. i64 div still leaves its 64-bit
            // quotient symbolic (the full quotient value VC is not well-posed
            // in QF_BV at that width), so it stays trap-condition-only.
            WasmOp::I64RemU | WasmOp::I64RemS => {
                self.verify_i64_rem_value_preservation(wasm_op, arm_ops)
            }
            WasmOp::I64DivS | WasmOp::I64DivU => {
                self.verify_i64_div_rem_trap_preservation(wasm_op, arm_ops)
            }
            WasmOp::Unreachable => {
                let (_state, arm_trap) = self.derive_arm_state(arm_ops, &[], None)?;
                Ok(Self::condition_verdict(
                    &crate::trap::trap_always(),
                    &arm_trap,
                ))
            }
            WasmOp::I32Load { offset, .. }
            | WasmOp::I32Load8S { offset, .. }
            | WasmOp::I32Load8U { offset, .. }
            | WasmOp::I32Load16S { offset, .. }
            | WasmOp::I32Load16U { offset, .. }
            | WasmOp::I32Store { offset, .. }
            | WasmOp::I32Store8 { offset, .. }
            | WasmOp::I32Store16 { offset, .. } => {
                let size: u64 = match wasm_op {
                    WasmOp::I32Load8S { .. }
                    | WasmOp::I32Load8U { .. }
                    | WasmOp::I32Store8 { .. } => 1,
                    WasmOp::I32Load16S { .. }
                    | WasmOp::I32Load16U { .. }
                    | WasmOp::I32Store16 { .. } => 2,
                    _ => 4,
                };
                self.verify_mem_trap_preservation(arm_ops, *offset, size)
            }
            WasmOp::I32TruncF32S | WasmOp::I32TruncF32U => {
                let signed = matches!(wasm_op, WasmOp::I32TruncF32S);
                self.verify_trunc_f32_trap_preservation(arm_ops, signed)
            }
            WasmOp::I32TruncF64S | WasmOp::I32TruncF64U => {
                let signed = matches!(wasm_op, WasmOp::I32TruncF64S);
                self.verify_trunc_f64_trap_preservation(arm_ops, signed)
            }
            other => Err(VerificationError::UnsupportedOperation(format!(
                "trap-preservation gate does not cover {other:?} \
                 (i64.trunc_f64 has no shipped lowering — the selector declines \
                 it; its classifier is unit-gated — see method docs)"
            ))),
        }
    }

    /// i32 div/rem trap preservation (VCR-VER-002, #166): full VC — the trap
    /// clause AND the guarded value clause — with the ARM trap term DERIVED
    /// from the emitted guard structure by the branch-taking executor.
    /// Operands: dividend = `input_0` (R0), divisor = `input_1` (R1),
    /// result in R0.
    ///
    /// The VALUE term comes from the straight-line pass
    /// ([`ArmSemantics::encode_sequence_value_straightline`]) whenever the
    /// sequence's branch structure is value-dead
    /// ([`ArmSemantics::branch_spans_are_value_dead`] — true for every
    /// shipped div/rem guard shape): on such sequences every non-trapping
    /// path produces the same registers as straight-line execution, and the
    /// resulting ite-free SDIV/UDIV/MLS terms stay STRUCTURALLY aligned with
    /// the WASM encoding — an `ite(guard, …)` wrapper on a divider/multiplier
    /// operand un-shares the circuits and sends the UNSAT value proof off a
    /// CDCL cliff. Non-conforming shapes fall back to the guarded
    /// (if-converted) post-state value — sound, potentially slow.
    pub fn verify_div_rem_trap_preservation(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
    ) -> Result<ValidationResult, VerificationError> {
        let Some(div_op) = crate::trap::div_op(wasm_op) else {
            return Err(VerificationError::UnsupportedOperation(format!(
                "trap-preservation gate applies to div/rem only, got {wasm_op:?}"
            )));
        };
        // This method models 32-bit operands only; `div_op` also maps the i64
        // variants (VCR-VER-002 follow-on: i64 needs 64-bit operand terms +
        // the register-pair ARM value model).
        if !matches!(
            wasm_op,
            WasmOp::I32DivS | WasmOp::I32DivU | WasmOp::I32RemS | WasmOp::I32RemU
        ) {
            return Err(VerificationError::UnsupportedOperation(format!(
                "trap-preservation gate currently supports i32 div/rem only, got {wasm_op:?}"
            )));
        }

        // Symbolic operands, matching `verify_equivalence_parameterized`'s
        // naming: dividend = input_0 (R0), divisor = input_1 (R1).
        let dividend = BV::new_const("input_0", 32);
        let divisor = BV::new_const("input_1", 32);
        let inputs = vec![dividend.clone(), divisor.clone()];

        let wasm_value = self.wasm_encoder.encode_op(wasm_op, &inputs);
        let (state, arm_may_trap) = self.derive_arm_state(arm_ops, &inputs, None)?;
        let arm_value = if ArmSemantics::branch_spans_are_value_dead(arm_ops) {
            // Ite-free value term, structurally aligned with the WASM side
            // (see the method doc for the soundness argument).
            let mut vstate = ArmState::new_symbolic();
            Self::seed_inputs(&mut vstate, &inputs)?;
            self.arm_encoder
                .encode_sequence_value_straightline(arm_ops, &mut vstate)
                .map_err(VerificationError::UnsupportedOperation)?;
            self.arm_encoder.extract_result(&vstate, &Reg::R0)
        } else {
            self.arm_encoder.extract_result(&state, &Reg::R0)
        };

        let orig = crate::trap::DefineOrTrap {
            value: wasm_value,
            may_trap: crate::trap::trap_div(div_op, &dividend, &divisor),
        };
        let opt = crate::trap::DefineOrTrap {
            value: arm_value,
            may_trap: arm_may_trap,
        };

        Ok(Self::trap_verdict_to_result(
            crate::trap::prove_trap_equivalence(&orig, &opt),
        ))
    }

    /// i32 load/store OOB trap preservation (VCR-VER-002, #166 / #377):
    /// trap-condition-only VC (synth models no memory contents). The WASM
    /// side is ordeal's wraparound-safe bound check on the effective address
    /// (`addr + offset + size >u mem_size`, exact 33-bit arithmetic); the ARM
    /// side is DERIVED from the emitted software-bounds guard. Operand
    /// convention: address = `input_0` (R0), store value (if any) = `input_1`
    /// (R1), linear-memory size = R10 (the shipped ABI register).
    pub fn verify_mem_trap_preservation(
        &self,
        arm_ops: &[ArmOp],
        offset: u32,
        access_size: u64,
    ) -> Result<ValidationResult, VerificationError> {
        let addr = BV::new_const("input_0", 32);
        let value = BV::new_const("input_1", 32);
        let inputs = vec![addr.clone(), value];

        let mut state = ArmState::new_symbolic();
        // The WASM-side bound is THE SAME symbol the ARM guard compares
        // against: R10 = linear-memory size in bytes (shipped ABI).
        let mem_bound = state.get_reg(&Reg::R10).clone();
        Self::seed_inputs(&mut state, &inputs)?;
        self.arm_encoder
            .encode_sequence_br(arm_ops, &mut state)
            .map_err(VerificationError::UnsupportedOperation)?;
        let arm_trap = state.may_trap.clone();

        // WASM Core: ea = addr + offset (exact), trap iff ea + size > bound.
        // Folding the static offset into the size operand keeps ordeal's
        // 33-bit zero-extended arithmetic exact: zext(addr) + zext(off+size).
        let static_bytes = offset as u64 + access_size;
        let wasm_trap = if static_bytes > u32::MAX as u64 {
            // offset + size alone exceeds the 32-bit bound: every access traps.
            crate::trap::trap_always()
        } else {
            crate::trap::trap_mem_oob(&addr, &BV::from_u64(static_bytes, 32), &mem_bound)
        };

        Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
    }

    /// `i32.trunc_f32_s/u` trap preservation (VCR-VER-002, #166 / #709):
    /// trap-condition-only VC (synth's QF_BV model carries no float→int
    /// value function). The WASM side is ordeal 0.9.1's bit-pattern trunc
    /// classifier (`NaN ∨ ±∞ ∨ out-of-range`); the ARM side is DERIVED from
    /// the emitted domain guard (`F32Const` bound + ordered VFP compare +
    /// `Cmp`/branch/`Udf`), with the ordered compares given real bit-pattern
    /// semantics in the executor. Operand convention: float operand = S0.
    pub fn verify_trunc_f32_trap_preservation(
        &self,
        arm_ops: &[ArmOp],
        signed: bool,
    ) -> Result<ValidationResult, VerificationError> {
        use synth_synthesis::rules::VfpReg;
        let bits = BV::new_const("input_0", 32);

        let mut state = ArmState::new_symbolic();
        state.set_vfp_reg(&VfpReg::S0, bits.clone());
        self.arm_encoder
            .encode_sequence_br(arm_ops, &mut state)
            .map_err(VerificationError::UnsupportedOperation)?;
        let arm_trap = state.may_trap.clone();

        let wasm_trap = crate::trap::trap_trunc(
            &bits,
            crate::trap::FpFmt::F32,
            crate::trap::IntTarget::I32,
            signed,
        );

        Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
    }

    /// i64 div/rem trap preservation (VCR-VER-002, #756): field-derived
    /// trap-condition-only VC. ARM32 has no 64-bit divide, so the shipped
    /// lowering emits a single `ArmOp::I64Div{S,U}`/`I64Rem{S,U}` pseudo-op
    /// whose 64-bit quotient the exec-model leaves symbolic (no `bvsdiv`
    /// term — the full value VC is not well-posed) and whose trap guards are
    /// carried as `elide_*` boolean FIELDS. The WASM spec side is ordeal's
    /// 64-bit `trap_div` over symbolic divisor bits (`rmlo:rmhi` = R2:R3); the
    /// ARM side is CONSTRUCTED from the pseudo-op's fields — a set `elide_*`
    /// deletes the corresponding clause — so a lowering that elides a guard
    /// (÷0 for all four, INT64_MIN/-1 overflow for `div_s`) whose fact was not
    /// discharged derives a weaker trap term and is reported `Invalid`.
    pub fn verify_i64_div_rem_trap_preservation(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
    ) -> Result<ValidationResult, VerificationError> {
        let Some(div_op) = crate::trap::div_op(wasm_op) else {
            return Err(VerificationError::UnsupportedOperation(format!(
                "i64 trap-preservation gate applies to div/rem only, got {wasm_op:?}"
            )));
        };
        if !matches!(
            wasm_op,
            WasmOp::I64DivS | WasmOp::I64DivU | WasmOp::I64RemS | WasmOp::I64RemU
        ) {
            return Err(VerificationError::UnsupportedOperation(format!(
                "i64 trap-preservation gate supports i64 div/rem only, got {wasm_op:?}"
            )));
        }

        // The shipped lowering is a single pseudo-op; find it in the sequence
        // (the selector emits exactly one, possibly amid dead ops).
        let (elide_zero, elide_overflow) =
            Self::i64_div_rem_guard_fields(arm_ops).ok_or_else(|| {
                VerificationError::UnsupportedOperation(format!(
                    "i64 trap gate needs an I64Div/I64Rem pseudo-op in the sequence, \
                     got {arm_ops:?}"
                ))
            })?;

        // WASM spec side: full 64-bit trap condition (÷0 ∨, for div_s only,
        // INT64_MIN/-1 overflow). The dividend/divisor symbols name the
        // register pairs the pseudo-op reads (rnlo:rnhi = R0:R1 dividend,
        // rmlo:rmhi = R2:R3 divisor).
        let dividend = BV::new_const("input_dividend_i64", 64);
        let divisor = BV::new_const("input_divisor_i64", 64);
        let wasm_trap = crate::trap::trap_div(div_op, &dividend, &divisor);

        // ARM side: reconstruct the SAME 64-bit trap term but with each clause
        // CONDITIONALLY present per the pseudo-op's elision fields. A dropped
        // guard => a strictly weaker term => the equivalence VC is Sat.
        let arm_trap =
            Self::i64_arm_trap_from_fields(div_op, &dividend, &divisor, elide_zero, elide_overflow);

        Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
    }

    /// i64 `rem_u`/`rem_s` **value + trap** preservation (VCR-VER, #825/#836).
    ///
    /// Unlike [`Self::verify_i64_div_rem_trap_preservation`] (trap-only, used
    /// for div where the 64-bit quotient value VC is not well-posed), this
    /// gate asserts the FULL obligation for remainder: on the non-trapping
    /// path the ARM register pair `R0:R1` must equal the native 64-bit
    /// unsigned/signed remainder of the operands, AND the ÷0 trap must be
    /// preserved. It is what makes the [`ArmSemantics`] `I64RemU` model —
    /// which now builds a real `BvTerm::Urem` term (ordeal 0.12) instead of
    /// HAVOC — actually load-bearing: a wrong remainder computation, or one
    /// that writes the answer to the wrong register pair, is now `Invalid`.
    ///
    /// # Operand / result convention (the shipped ABI, NOT the op's fields)
    ///
    /// The value is READ from the FIXED ABI return registers `R0` (low) /
    /// `R1` (high) and the operands are SEEDED at the FIXED ABI argument
    /// registers — dividend `R0:R1`, divisor `R2:R3`. Reading the op's own
    /// `rd*` fields (or seeding its own `rn*`/`rm*`) would make the VC
    /// vacuous (read tracks write); anchoring on the ABI is exactly what lets
    /// a pseudo-op whose destination deviates from `R0:R1` be REJECTED.
    ///
    /// # Trap-guarded value (why not a raw `==`)
    ///
    /// A bare `arm_value == wasm_value` would also assert the value on the ÷0
    /// path, where WASM has no value and SMT-LIB `bvurem`-by-0 = the dividend
    /// (total) — a spurious obligation. Routing through
    /// [`crate::trap::DefineOrTrap`] + [`crate::trap::prove_trap_equivalence`]
    /// guards the value clause under non-trap. The single branch-free
    /// pseudo-op keeps the value ite-free, so no straight-line rewrite is
    /// needed (unlike the i32 guarded-div machinery).
    pub fn verify_i64_rem_value_preservation(
        &self,
        wasm_op: &WasmOp,
        arm_ops: &[ArmOp],
    ) -> Result<ValidationResult, VerificationError> {
        let Some(div_op) = crate::trap::div_op(wasm_op) else {
            return Err(VerificationError::UnsupportedOperation(format!(
                "i64 rem value gate applies to rem only, got {wasm_op:?}"
            )));
        };
        if !matches!(wasm_op, WasmOp::I64RemU | WasmOp::I64RemS) {
            return Err(VerificationError::UnsupportedOperation(format!(
                "i64 rem value gate supports i64 rem_u/rem_s only, got {wasm_op:?}"
            )));
        }

        // Require the pseudo-op to be present and read its ÷0 guard-elision
        // field (the selector emits exactly one). The ARM trap term is
        // reconstructed from this field — NOT from `encode_sequence_br`'s
        // `may_trap`, which is `false` for a bare pseudo-op (it carries no
        // expanded `UDF`) — exactly as the i64 trap-only VC does. A lowering
        // that elides the ÷0 guard without discharging `divisor != 0` yields a
        // strictly weaker ARM trap and is rejected.
        let Some((elide_zero, _elide_overflow)) = Self::i64_div_rem_guard_fields(arm_ops) else {
            return Err(VerificationError::UnsupportedOperation(format!(
                "i64 rem value gate needs an I64Rem pseudo-op in the sequence, \
                 got {arm_ops:?}"
            )));
        };

        // Four independent 32-bit half-symbols. Seed them at the FIXED ABI
        // argument registers: dividend lo:hi = R0:R1, divisor lo:hi = R2:R3.
        let dividend_lo = BV::new_const("input_dividend_lo", 32);
        let dividend_hi = BV::new_const("input_dividend_hi", 32);
        let divisor_lo = BV::new_const("input_divisor_lo", 32);
        let divisor_hi = BV::new_const("input_divisor_hi", 32);

        let mut state = ArmState::new_symbolic();
        state.set_reg(&Reg::R0, dividend_lo.clone());
        state.set_reg(&Reg::R1, dividend_hi.clone());
        state.set_reg(&Reg::R2, divisor_lo.clone());
        state.set_reg(&Reg::R3, divisor_hi.clone());
        self.arm_encoder
            .encode_sequence_br(arm_ops, &mut state)
            .map_err(VerificationError::UnsupportedOperation)?;

        // ARM result read from the FIXED ABI return pair R0:R1 (concat puts
        // self in the HIGH bits).
        let arm_lo = self.arm_encoder.extract_result(&state, &Reg::R0);
        let arm_hi = self.arm_encoder.extract_result(&state, &Reg::R1);
        let arm_value = arm_hi.concat(&arm_lo); // 64-bit R1:R0

        // WASM spec side: the 64-bit remainder of the SAME operand symbols.
        // Both sides feed identical concats, so the valid case is structural.
        let dividend = dividend_hi.concat(&dividend_lo); // 64-bit
        let divisor = divisor_hi.concat(&divisor_lo); // 64-bit
        let wasm_value = match wasm_op {
            WasmOp::I64RemU => dividend.bvurem(&divisor),
            WasmOp::I64RemS => dividend.bvsrem(&divisor),
            _ => unreachable!("guarded above"),
        };
        let wasm_trap = crate::trap::trap_div(div_op, &dividend, &divisor);

        // ARM trap: rem's only trap is ÷0; present iff the guard was NOT
        // elided. rem carries no overflow clause, so `elide_overflow=false`.
        let arm_may_trap = Self::i64_arm_trap_from_fields(
            div_op, &dividend, &divisor, elide_zero, /* elide_overflow */ false,
        );

        let orig = crate::trap::DefineOrTrap {
            value: wasm_value,
            may_trap: wasm_trap,
        };
        let opt = crate::trap::DefineOrTrap {
            value: arm_value,
            may_trap: arm_may_trap,
        };

        Ok(Self::trap_verdict_to_result(
            crate::trap::prove_trap_equivalence(&orig, &opt),
        ))
    }

    /// Locate the i64 div/rem pseudo-op in a sequence and read its guard-elision
    /// fields as `(elide_zero, elide_overflow)`. `div_u`/`rem_s`/`rem_u` have no
    /// overflow guard, so their `elide_overflow` is reported `false`
    /// (the clause is not part of their WASM trap condition anyway).
    fn i64_div_rem_guard_fields(arm_ops: &[ArmOp]) -> Option<(bool, bool)> {
        arm_ops.iter().find_map(|op| match op {
            ArmOp::I64DivS {
                elide_zero_guard,
                elide_overflow_guard,
                ..
            } => Some((*elide_zero_guard, *elide_overflow_guard)),
            ArmOp::I64DivU {
                elide_zero_guard, ..
            }
            | ArmOp::I64RemS {
                elide_zero_guard, ..
            }
            | ArmOp::I64RemU {
                elide_zero_guard, ..
            } => Some((*elide_zero_guard, false)),
            _ => None,
        })
    }

    /// Build the ARM-side i64 trap term from the guard-elision fields: start
    /// from the full WASM trap condition and DELETE each clause the pseudo-op
    /// elides. The ÷0 clause is `divisor == 0`; the overflow clause (`div_s`
    /// only) is `dividend == INT64_MIN ∧ divisor == -1`.
    fn i64_arm_trap_from_fields(
        div_op: crate::trap::DivOp,
        dividend: &BV,
        divisor: &BV,
        elide_zero: bool,
        elide_overflow: bool,
    ) -> Bool {
        let zero = BV::from_u64(0, 64);
        let div_by_zero = divisor.eq(&zero);

        // The ÷0 clause is present iff not elided.
        let mut clauses: Vec<Bool> = Vec::new();
        if !elide_zero {
            clauses.push(div_by_zero);
        }

        // The overflow clause is only part of div_s's WASM condition; for the
        // other three it is not in `trap_div` at all, so never add it.
        if matches!(div_op, crate::trap::DivOp::DivS) && !elide_overflow {
            let int_min = BV::from_i64(i64::MIN, 64);
            let neg_one = BV::from_i64(-1, 64);
            let overflow = Bool::and(&[&dividend.eq(&int_min), &divisor.eq(&neg_one)]);
            clauses.push(overflow);
        }

        if clauses.is_empty() {
            Bool::from_bool(false)
        } else {
            let refs: Vec<&Bool> = clauses.iter().collect();
            Bool::or(&refs)
        }
    }

    /// `i32.trunc_f64_s/u` trap preservation (VCR-VER-002, #166 / #709 / #756):
    /// trap-condition-only VC (synth's QF_BV model carries no float→int value
    /// function). The WASM side is ordeal's bit-pattern trunc classifier over
    /// the f64 operand (`NaN ∨ ±∞ ∨ out-of-range`); the ARM side is DERIVED
    /// from the emitted DOUBLE-precision domain guard (`F64Const` bound +
    /// ordered `VCMP.F64` compare + `Cmp`/branch/`Udf`), with the ordered f64
    /// compares given real bit-pattern semantics in the executor. Operand
    /// convention: f64 operand = D0 (a 64-bit BV), bound scratch = D1.
    pub fn verify_trunc_f64_trap_preservation(
        &self,
        arm_ops: &[ArmOp],
        signed: bool,
    ) -> Result<ValidationResult, VerificationError> {
        use synth_synthesis::rules::VfpReg;
        let bits = BV::new_const("input_0", 64);

        let mut state = ArmState::new_symbolic();
        state.set_vfp_reg(&VfpReg::D0, bits.clone());
        self.arm_encoder
            .encode_sequence_br(arm_ops, &mut state)
            .map_err(VerificationError::UnsupportedOperation)?;
        let arm_trap = state.may_trap.clone();

        let wasm_trap = crate::trap::trap_trunc(
            &bits,
            crate::trap::FpFmt::F64,
            crate::trap::IntTarget::I32,
            signed,
        );

        Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
    }

    /// `call_indirect` trap preservation (VCR-VER-002, #166 / #642 #664 #676):
    /// trap-condition-only VC. The WASM-side spec comes from MODULE FACTS the
    /// caller supplies ([`CallIndirectSpec`]); the ARM side is derived from
    /// the `ArmOp::CallIndirect` pseudo-op's guard fields (`table_size`,
    /// `null_check`, `type_check`) through the SAME pinned ordeal builder —
    /// a selector that resolves the wrong table size, drops the null check on
    /// a table with uninitialized slots (#664), or skips the runtime type
    /// check on a heterogeneous table (#676) is reported `Invalid`.
    ///
    /// # Trust boundary
    ///
    /// This certifies the SELECTOR's guard resolution at the pseudo-op level;
    /// the encoder's expansion of those fields into `CMP`/`BLO`/`UDF`/`BLX`
    /// bytes is separately execution-gated (the unicorn call_indirect CI
    /// jobs). Statically-discharged clauses are modeled by a provably
    /// non-null slot term (`slot | 1`), keeping ordeal's builder the single
    /// spec source.
    pub fn verify_call_indirect_trap_preservation(
        &self,
        arm_op: &ArmOp,
        spec: &CallIndirectSpec,
    ) -> Result<ValidationResult, VerificationError> {
        let ArmOp::CallIndirect {
            table_size,
            null_check,
            type_check,
            ..
        } = arm_op
        else {
            return Err(VerificationError::UnsupportedOperation(format!(
                "call_indirect trap gate needs the CallIndirect pseudo-op, got {arm_op:?}"
            )));
        };

        let index = BV::new_const("input_0", 32);
        let slot = BV::new_const("slot_ptr", 32);
        let nonnull_slot = slot.bvor(BV::from_u64(1, 32));
        let actual_ty = BV::new_const("slot_type_id", 32);

        let build = |size: u32, may_null: bool, expected: Option<u32>| {
            let expected_bv = expected.map(|e| BV::from_u64(e as u64, 32));
            let size_bv = BV::from_u64(size as u64, 32);
            let slot_term = if may_null { &slot } else { &nonnull_slot };
            let type_trap = match &expected_bv {
                Some(e) => crate::trap::TypeTrap::Runtime {
                    actual_type_id: &actual_ty,
                    expected_id: e,
                },
                None => crate::trap::TypeTrap::StaticallyDischarged,
            };
            crate::trap::trap_call_indirect(&crate::trap::CallIndirect {
                index: &index,
                table_size: &size_bv,
                slot_ptr: slot_term,
                type_trap,
            })
        };

        let wasm_trap = build(
            spec.table_size,
            spec.may_have_null_slot,
            spec.heterogeneous_expected_type,
        );
        let arm_trap = build(
            *table_size,
            *null_check,
            type_check.as_ref().map(|(expected, _)| *expected),
        );

        Ok(Self::condition_verdict(&wasm_trap, &arm_trap))
    }

    /// Seed integer operand registers (R0..R2) and run the branch-taking
    /// executor, returning the post-state and the DERIVED trap condition.
    fn derive_arm_state(
        &self,
        arm_ops: &[ArmOp],
        inputs: &[BV],
        vfp_s0: Option<&BV>,
    ) -> Result<(ArmState, Bool), VerificationError> {
        let mut state = ArmState::new_symbolic();
        Self::seed_inputs(&mut state, inputs)?;
        if let Some(bits) = vfp_s0 {
            state.set_vfp_reg(&synth_synthesis::rules::VfpReg::S0, bits.clone());
        }
        self.arm_encoder
            .encode_sequence_br(arm_ops, &mut state)
            .map_err(VerificationError::UnsupportedOperation)?;
        let trap = state.may_trap.clone();
        Ok((state, trap))
    }

    fn seed_inputs(state: &mut ArmState, inputs: &[BV]) -> Result<(), VerificationError> {
        for (i, input) in inputs.iter().enumerate() {
            let reg = match i {
                0 => Reg::R0,
                1 => Reg::R1,
                2 => Reg::R2,
                _ => {
                    return Err(VerificationError::UnsupportedOperation(format!(
                        "Too many inputs: {}",
                        inputs.len()
                    )));
                }
            };
            state.set_reg(&reg, input.clone());
        }
        Ok(())
    }

    /// Run the trap-condition-only VC and map the verdict.
    fn condition_verdict(wasm_trap: &Bool, arm_trap: &Bool) -> ValidationResult {
        Self::trap_verdict_to_result(crate::trap::prove_trap_condition_equivalence(
            wasm_trap, arm_trap,
        ))
    }

    fn trap_verdict_to_result(verdict: crate::trap::TrapVerdict) -> ValidationResult {
        match verdict {
            crate::trap::TrapVerdict::Preserved => ValidationResult::Verified,
            crate::trap::TrapVerdict::Dropped(model) => ValidationResult::Invalid {
                counterexample: model
                    .into_iter()
                    .filter_map(|(n, v)| i64::try_from(v).ok().map(|x| (n, x)))
                    .collect(),
            },
            crate::trap::TrapVerdict::Unknown => ValidationResult::Unknown {
                reason: "trap-preservation VC returned Unknown (conservative reject)".to_string(),
            },
        }
    }

    /// Get number of inputs required for a WASM operation
    fn get_num_inputs(&self, wasm_op: &WasmOp) -> usize {
        use WasmOp::*;
        match wasm_op {
            // Binary operations
            I32Add | I32Sub | I32Mul | I32DivS | I32DivU | I32RemS | I32RemU | I32And | I32Or
            | I32Xor | I32Shl | I32ShrS | I32ShrU | I32Rotl | I32Rotr | I32Eq | I32Ne | I32LtS
            | I32LtU | I32LeS | I32LeU | I32GtS | I32GtU | I32GeS | I32GeU => 2,

            // Unary operations
            I32Clz | I32Ctz | I32Popcnt | I32Eqz => 1,

            // Constants
            I32Const(_) => 0,

            // Memory operations
            I32Load { .. } => 1,  // address
            I32Store { .. } => 2, // address + value

            // Control flow
            LocalGet(_) | GlobalGet(_) => 0,
            LocalSet(_) | GlobalSet(_) | LocalTee(_) => 1,
            Br(_) | BrIf(_) | Return => 0,

            // Other operations
            Drop => 1,
            Select => 3, // condition + two values
            Nop | Unreachable | Block | Loop | If | Else | End => 0,

            // Default for unknown
            _ => 0,
        }
    }

    /// Batch verify multiple synthesis rules
    pub fn verify_rules(
        &self,
        rules: &[SynthesisRule],
    ) -> Vec<(String, Result<ValidationResult, VerificationError>)> {
        rules
            .iter()
            .map(|rule| {
                let result = self.verify_rule(rule);
                (rule.name.clone(), result)
            })
            .collect()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::with_verification_context;
    use synth_synthesis::rules::Condition;
    use synth_synthesis::{Cost, Operand2, Pattern, Replacement};

    fn create_test_rule(wasm_op: WasmOp, arm_op: ArmOp) -> SynthesisRule {
        SynthesisRule {
            name: format!("{:?}", wasm_op),
            priority: 0,
            pattern: Pattern::WasmInstr(wasm_op),
            replacement: Replacement::ArmInstr(arm_op),
            cost: Cost {
                cycles: 1,
                code_size: 4,
                registers: 2,
            },
        }
    }

    // --- VCR-VER-002 (#166): div/rem trap-preservation wired into the validator ---

    #[test]
    fn div_lowering_without_guard_is_rejected_as_trap_drop() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // Bare UDIV — the value is right but the ÷0 guard is missing
            // (the #633/#666 shape). The trap-preservation gate must reject it.
            let arm_ops = [ArmOp::Udiv {
                rd: Reg::R0,
                rn: Reg::R0,
                rm: Reg::R1,
            }];
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivU, &arm_ops)
                .unwrap();
            match result {
                ValidationResult::Invalid { counterexample } => {
                    // The counterexample must exhibit the dropped trap: divisor 0.
                    let divisor = counterexample.iter().find(|(n, _)| n == "input_1");
                    assert_eq!(
                        divisor.map(|(_, v)| *v),
                        Some(0),
                        "trap-drop counterexample must set the divisor to 0"
                    );
                }
                other => panic!("unguarded div must be Invalid, got {other:?}"),
            }
        });
    }

    /// The SHIPPED ÷0 guard shape (instruction_selector.rs I32DivU /
    /// optimizer_bridge.rs DivU): CMP divisor,#0 ; BNE +0 (skip the UDF) ;
    /// UDF ; UDIV. The derived trap term is (divisor == 0) — exactly WASM's.
    fn shipped_divu_guard() -> Vec<ArmOp> {
        vec![
            ArmOp::Cmp {
                rn: Reg::R1,
                op2: Operand2::Imm(0),
            },
            ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 0,
            },
            ArmOp::Udf { imm: 0 },
            ArmOp::Udiv {
                rd: Reg::R0,
                rn: Reg::R0,
                rm: Reg::R1,
            },
        ]
    }

    /// The SHIPPED div_s DOUBLE guard (optimizer_bridge.rs DivS): the ÷0
    /// guard plus the INT_MIN/-1 overflow guard (MOVW/MOVT 0x80000000 into
    /// R12 ; CMP dividend ; BNE +3 ; CMN divisor,#1 ; BNE +0 ; UDF #1).
    fn shipped_divs_double_guard() -> Vec<ArmOp> {
        vec![
            ArmOp::Cmp {
                rn: Reg::R1,
                op2: Operand2::Imm(0),
            },
            ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 0,
            },
            ArmOp::Udf { imm: 0 },
            ArmOp::Movw {
                rd: Reg::R12,
                imm16: 0,
            },
            ArmOp::Movt {
                rd: Reg::R12,
                imm16: 0x8000,
            },
            ArmOp::Cmp {
                rn: Reg::R0,
                op2: Operand2::Reg(Reg::R12),
            },
            ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 3,
            },
            ArmOp::Cmn {
                rn: Reg::R1,
                op2: Operand2::Imm(1),
            },
            ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 0,
            },
            ArmOp::Udf { imm: 1 },
            ArmOp::Sdiv {
                rd: Reg::R0,
                rn: Reg::R0,
                rm: Reg::R1,
            },
        ]
    }

    #[test]
    fn div_lowering_with_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivU, &shipped_divu_guard())
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// The derived gate is STRICTER than the retired Udf-presence proxy: a
    /// guard with the branch polarity inverted (BEQ instead of BNE — the UDF
    /// fires exactly when the divide is fine) still contains a Udf, so the
    /// proxy called it Verified; the derived trap term is (divisor != 0),
    /// which fails the VC.
    #[test]
    fn div_guard_with_inverted_polarity_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let mut arm_ops = shipped_divu_guard();
            arm_ops[1] = ArmOp::BCondOffset {
                cond: Condition::EQ,
                offset: 0,
            };
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivU, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "inverted guard polarity must be Invalid, got {result:?}"
            );
        });
    }

    #[test]
    fn signed_div_double_guard_preserves_both_zero_and_overflow_traps() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivS, &shipped_divs_double_guard())
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// RED-FIRST for the div_s overflow class (#633-shape at i32): stripping
    /// ONLY the INT_MIN/-1 overflow guard keeps a Udf in the sequence (the ÷0
    /// guard), so the retired structural proxy called this Verified. The
    /// derived trap term is only (divisor == 0), and the VC finds the dropped
    /// overflow trap with the INT_MIN/-1 counterexample.
    #[test]
    fn signed_div_with_overflow_guard_stripped_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [
                ArmOp::Cmp {
                    rn: Reg::R1,
                    op2: Operand2::Imm(0),
                },
                ArmOp::BCondOffset {
                    cond: Condition::NE,
                    offset: 0,
                },
                ArmOp::Udf { imm: 0 },
                ArmOp::Sdiv {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                },
            ];
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivS, &arm_ops)
                .unwrap();
            match result {
                ValidationResult::Invalid { counterexample } => {
                    let get = |n: &str| {
                        counterexample
                            .iter()
                            .find(|(name, _)| name == n)
                            .map(|(_, v)| *v)
                    };
                    assert_eq!(
                        get("input_0"),
                        Some(i32::MIN as u32 as i64),
                        "dropped overflow trap must exhibit dividend INT_MIN: {counterexample:?}"
                    );
                    assert_eq!(
                        get("input_1"),
                        Some(u32::MAX as i64),
                        "dropped overflow trap must exhibit divisor -1: {counterexample:?}"
                    );
                }
                other => panic!("overflow-guard-stripped div_s must be Invalid, got {other:?}"),
            }
        });
    }

    /// rem_s carries ONLY the ÷0 guard — WASM rem_s(INT_MIN, -1) is 0, not a
    /// trap — and the derived gate agrees.
    #[test]
    fn rems_single_zero_guard_is_exactly_right() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [
                ArmOp::Cmp {
                    rn: Reg::R1,
                    op2: Operand2::Imm(0),
                },
                ArmOp::BCondOffset {
                    cond: Condition::NE,
                    offset: 0,
                },
                ArmOp::Udf { imm: 0 },
                ArmOp::Sdiv {
                    rd: Reg::R2,
                    rn: Reg::R0,
                    rm: Reg::R1,
                },
                ArmOp::Mls {
                    rd: Reg::R0,
                    rn: Reg::R2,
                    rm: Reg::R1,
                    ra: Reg::R0,
                },
            ];
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32RemS, &arm_ops)
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    // --- unreachable (LIVE, #665 class) ---

    #[test]
    fn unreachable_udf_lowering_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&WasmOp::Unreachable, &[ArmOp::Udf { imm: 0 }])
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn unreachable_lowered_to_nop_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // The #665 shape: unreachable silently became a no-op.
            let result = validator
                .verify_trap_preservation(&WasmOp::Unreachable, &[ArmOp::Nop])
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "trap-dropping unreachable lowering must be Invalid, got {result:?}"
            );
        });
    }

    // --- i32 load/store OOB (LIVE, #377/#752 class) ---

    /// The SHIPPED software-bounds lowering at the gate's register
    /// convention (address = R0 = `input_0`): the guard prefix comes from
    /// `InstructionSelector::software_bounds_guard` — THE function every
    /// emission site calls, public precisely so this gate pins the real
    /// shipped shape and no hand-maintained mirror can drift (the VCR-ORACLE
    /// lesson) — composed with the trailing access op per the generators'
    /// documented contract (`result.last() is Ldr/Ldrb/.../Str
    /// [R11, addr, #offset]`, pinned by the selector unit tests). The full
    /// selector is not used directly because it homes a bare op's address in
    /// an allocator-chosen register, not the gate's `input_0`.
    fn shipped_software_bounds_ops(wasm_op: &WasmOp) -> Vec<ArmOp> {
        use synth_synthesis::instruction_selector::InstructionSelector;
        use synth_synthesis::rules::MemAddr;
        let (offset, size) = match wasm_op {
            WasmOp::I32Load { offset, .. } | WasmOp::I32Store { offset, .. } => (*offset, 4u32),
            WasmOp::I32Load16S { offset, .. }
            | WasmOp::I32Load16U { offset, .. }
            | WasmOp::I32Store16 { offset, .. } => (*offset, 2),
            WasmOp::I32Load8S { offset, .. }
            | WasmOp::I32Load8U { offset, .. }
            | WasmOp::I32Store8 { offset, .. } => (*offset, 1),
            other => panic!("not a guarded i32 access: {other:?}"),
        };
        let addr = MemAddr::reg_imm(Reg::R11, Reg::R0, offset as i32);
        let access = match wasm_op {
            WasmOp::I32Load { .. } => ArmOp::Ldr { rd: Reg::R0, addr },
            WasmOp::I32Load8S { .. } => ArmOp::Ldrsb { rd: Reg::R0, addr },
            WasmOp::I32Load8U { .. } => ArmOp::Ldrb { rd: Reg::R0, addr },
            WasmOp::I32Load16S { .. } => ArmOp::Ldrsh { rd: Reg::R0, addr },
            WasmOp::I32Load16U { .. } => ArmOp::Ldrh { rd: Reg::R0, addr },
            WasmOp::I32Store { .. } => ArmOp::Str { rd: Reg::R1, addr },
            WasmOp::I32Store8 { .. } => ArmOp::Strb { rd: Reg::R1, addr },
            WasmOp::I32Store16 { .. } => ArmOp::Strh { rd: Reg::R1, addr },
            other => panic!("not a guarded i32 access: {other:?}"),
        };
        let mut ops = InstructionSelector::software_bounds_guard(Reg::R0, offset as i32, size);
        ops.push(access);
        ops
    }

    /// RED-FIRST: a load with the bounds guard stripped derives trap = false
    /// and is rejected against the WASM OOB condition.
    #[test]
    fn load_without_bounds_guard_is_rejected() {
        use synth_synthesis::rules::MemAddr;
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [ArmOp::Ldr {
                rd: Reg::R0,
                addr: MemAddr::reg_imm(Reg::R11, Reg::R0, 0),
            }];
            let result = validator
                .verify_trap_preservation(
                    &WasmOp::I32Load {
                        offset: 0,
                        align: 2,
                    },
                    &arm_ops,
                )
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "guard-stripped load must be Invalid, got {result:?}"
            );
        });
    }

    /// A byte load's shipped guard is exact for size 1 / offset 0 (it was the
    /// ONE class the old ADD-computed guard already got right) and stays
    /// Verified under the #752 wraparound-safe shape.
    #[test]
    fn byte_load_software_bounds_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(
                    &WasmOp::I32Load8U {
                        offset: 0,
                        align: 0,
                    },
                    &shipped_software_bounds_ops(&WasmOp::I32Load8U {
                        offset: 0,
                        align: 0,
                    }),
                )
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// #752 CLOSED (was the pinned `word_load_software_bounds_guard_wraps_at_
    /// address_top` finding): the old shape computed `addr + (offset+size-1)`
    /// in WRAPPING 32-bit arithmetic, so at `addr >= 0x1_0000_0000 -
    /// (offset+size-1)` the end address wrapped small, the BLO guard passed,
    /// and the access escaped below the linear-memory base — the derived gate
    /// exhibited the dropped-trap counterexample at `addr >= 0xFFFF_FFFD`.
    /// The shipped guard is now the wraparound-safe SUB-from-bound shape
    /// (`software_bounds_guard`): this asserts the WHOLE class Verified, i.e.
    /// the divergence is unsatisfiable for EVERY addr including the top of
    /// the address space.
    #[test]
    fn word_load_software_bounds_guard_survives_the_address_top_752() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(
                    &WasmOp::I32Load {
                        offset: 0,
                        align: 2,
                    },
                    &shipped_software_bounds_ops(&WasmOp::I32Load {
                        offset: 0,
                        align: 2,
                    }),
                )
                .unwrap();
            assert_eq!(
                result,
                ValidationResult::Verified,
                "the #752 wraparound divergence must be closed for every addr"
            );
        });
    }

    /// #752: every guarded access width and a non-zero static offset verify —
    /// the wrap escape was specifically the multi-byte / non-zero-offset
    /// class, so gate the whole family (loads via the shipped selector).
    #[test]
    fn all_load_widths_software_bounds_guard_verify_752() {
        let cases: Vec<WasmOp> = vec![
            WasmOp::I32Load {
                offset: 4,
                align: 2,
            },
            WasmOp::I32Load8S {
                offset: 3,
                align: 0,
            },
            WasmOp::I32Load8U {
                offset: 1,
                align: 0,
            },
            WasmOp::I32Load16S {
                offset: 2,
                align: 1,
            },
            WasmOp::I32Load16U {
                offset: 0,
                align: 1,
            },
        ];
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for wasm_op in &cases {
                let result = validator
                    .verify_trap_preservation(wasm_op, &shipped_software_bounds_ops(wasm_op))
                    .unwrap();
                assert_eq!(result, ValidationResult::Verified, "{wasm_op:?}");
            }
        });
    }

    /// #752: the store guards use the same `software_bounds_guard` prefix —
    /// all three widths, with non-zero static offsets on the subword forms.
    #[test]
    fn store_software_bounds_guard_verifies_752() {
        let cases: Vec<WasmOp> = vec![
            WasmOp::I32Store {
                offset: 0,
                align: 2,
            },
            WasmOp::I32Store8 {
                offset: 5,
                align: 0,
            },
            WasmOp::I32Store16 {
                offset: 3,
                align: 1,
            },
        ];
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for wasm_op in &cases {
                let result = validator
                    .verify_trap_preservation(wasm_op, &shipped_software_bounds_ops(wasm_op))
                    .unwrap();
                assert_eq!(result, ValidationResult::Verified, "{wasm_op:?}");
            }
        });
    }

    /// #752: a static offset past the SUBW imm12 reach takes the MOVW
    /// materialization arm of the guard — Verified, i.e. the register-built
    /// constant is derived with the same exactness as the immediate form.
    #[test]
    fn large_offset_software_bounds_guard_verifies_752() {
        let wasm_op = WasmOp::I32Load {
            offset: 0x2000,
            align: 2,
        };
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&wasm_op, &shipped_software_bounds_ops(&wasm_op))
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// #752: `offset + size > u32::MAX` can never be in bounds — the guard
    /// degenerates to an unconditional UDF and the gate agrees with WASM's
    /// always-trap on the class.
    #[test]
    fn offset_overflow_software_bounds_guard_always_traps_752() {
        let wasm_op = WasmOp::I32Load {
            offset: u32::MAX,
            align: 2,
        };
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&wasm_op, &shipped_software_bounds_ops(&wasm_op))
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// REGRESSION PIN (the #752 finding itself): the RETIRED ADD-computed
    /// guard shape must stay Invalid, with the counterexample at the top of
    /// the address space — proving the gate still catches the wraparound
    /// class if anything ever re-emits it.
    #[test]
    fn retired_add_computed_guard_stays_invalid_at_the_address_top_752() {
        use synth_synthesis::rules::{Condition, MemAddr, Operand2};
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [
                ArmOp::Add {
                    rd: Reg::R12,
                    rn: Reg::R0,
                    op2: Operand2::Imm(3), // offset 0 + size 4 - 1
                },
                ArmOp::Cmp {
                    rn: Reg::R12,
                    op2: Operand2::Reg(Reg::R10),
                },
                ArmOp::BCondOffset {
                    cond: Condition::LO,
                    offset: 0,
                },
                ArmOp::Udf { imm: 0 },
                ArmOp::Ldr {
                    rd: Reg::R0,
                    addr: MemAddr::reg_imm(Reg::R11, Reg::R0, 0),
                },
            ];
            let result = validator
                .verify_trap_preservation(
                    &WasmOp::I32Load {
                        offset: 0,
                        align: 2,
                    },
                    &arm_ops,
                )
                .unwrap();
            match result {
                ValidationResult::Invalid { counterexample } => {
                    let addr = counterexample
                        .iter()
                        .find(|(n, _)| n == "input_0")
                        .map(|(_, v)| *v)
                        .expect("counterexample must assign the address");
                    assert!(
                        addr >= 0xFFFF_FFFD,
                        "the divergence is the 32-bit end-address wrap at the top \
                         of the address space, got addr {addr:#x}"
                    );
                }
                other => panic!("the retired wrapping guard must stay Invalid, got {other:?}"),
            }
        });
    }

    /// The gate is satisfiable by more than one correct guard: the issue's
    /// reference shape (trap iff bound < k, else iff addr >u bound - k,
    /// k = offset+size) also verifies — the mem-OOB class gate is not pinned
    /// to the shipped shape.
    #[test]
    fn wraparound_safe_bounds_guard_verifies() {
        use synth_synthesis::rules::MemAddr;
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let k = 4; // offset 0, size 4
            let arm_ops = [
                // CMP R10, #k ; BHS +0 ; UDF   — bound < k ⇒ every access traps
                ArmOp::Cmp {
                    rn: Reg::R10,
                    op2: Operand2::Imm(k),
                },
                ArmOp::BCondOffset {
                    cond: Condition::HS,
                    offset: 0,
                },
                ArmOp::Udf { imm: 0 },
                // SUB R12, R10, #k ; CMP addr, R12 ; BLS +0 ; UDF — exact on
                // the bound >= k path (no wrap possible)
                ArmOp::Sub {
                    rd: Reg::R12,
                    rn: Reg::R10,
                    op2: Operand2::Imm(k),
                },
                ArmOp::Cmp {
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R12),
                },
                ArmOp::BCondOffset {
                    cond: Condition::LS,
                    offset: 0,
                },
                ArmOp::Udf { imm: 0 },
                ArmOp::Ldr {
                    rd: Reg::R0,
                    addr: MemAddr::reg_imm(Reg::R11, Reg::R0, 0),
                },
            ];
            let result = validator
                .verify_trap_preservation(
                    &WasmOp::I32Load {
                        offset: 0,
                        align: 2,
                    },
                    &arm_ops,
                )
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    // --- i32.trunc_f32_s/u (LIVE, #709 class) ---

    /// The SHIPPED trunc domain-guard shape (instruction_selector.rs
    /// I32TruncF32S/U): per bound, F32Const scratch ; ordered compare into
    /// R0 ; CMP R0,#0 ; BNE +0 (in-range skips) ; UDF — then the VCVT.
    /// Operand in S0, bound scratch S1 (the gate's register convention).
    fn shipped_trunc_f32_guard(signed: bool) -> Vec<ArmOp> {
        use synth_synthesis::rules::VfpReg;
        let (hi, lo) = if signed {
            (2147483648.0_f32, -2147483648.0_f32)
        } else {
            (4294967296.0_f32, -1.0_f32)
        };
        let mut ops = Vec::new();
        let guard = |ops: &mut Vec<ArmOp>, bound: f32, upper: bool| {
            ops.push(ArmOp::F32Const {
                sd: VfpReg::S1,
                value: bound,
            });
            let cmp = if upper {
                ArmOp::F32Lt {
                    rd: Reg::R0,
                    sn: VfpReg::S0,
                    sm: VfpReg::S1,
                }
            } else if signed {
                ArmOp::F32Ge {
                    rd: Reg::R0,
                    sn: VfpReg::S0,
                    sm: VfpReg::S1,
                }
            } else {
                ArmOp::F32Gt {
                    rd: Reg::R0,
                    sn: VfpReg::S0,
                    sm: VfpReg::S1,
                }
            };
            ops.push(cmp);
            ops.push(ArmOp::Cmp {
                rn: Reg::R0,
                op2: Operand2::Imm(0),
            });
            ops.push(ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 0,
            });
            ops.push(ArmOp::Udf { imm: 0 });
        };
        guard(&mut ops, hi, true);
        guard(&mut ops, lo, false);
        if signed {
            ops.push(ArmOp::I32TruncF32S {
                rd: Reg::R0,
                sm: VfpReg::S0,
            });
        } else {
            ops.push(ArmOp::I32TruncF32U {
                rd: Reg::R0,
                sm: VfpReg::S0,
            });
        }
        ops
    }

    #[test]
    fn trunc_f32_s_domain_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF32S, &shipped_trunc_f32_guard(true))
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn trunc_f32_u_domain_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF32U, &shipped_trunc_f32_guard(false))
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// RED-FIRST for the #709 class: the bare saturating VCVT (guards
    /// stripped) never traps — rejected with a counterexample.
    #[test]
    fn trunc_f32_without_domain_guard_is_rejected() {
        use synth_synthesis::rules::VfpReg;
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [ArmOp::I32TruncF32S {
                rd: Reg::R0,
                sm: VfpReg::S0,
            }];
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF32S, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "guard-stripped trunc must be Invalid, got {result:?}"
            );
        });
    }

    /// Half a domain guard (upper bound only) drops the lower-bound trap.
    #[test]
    fn trunc_f32_with_only_upper_guard_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let mut arm_ops = shipped_trunc_f32_guard(true);
            // Strip the second (lower-bound) guard: 5 ops per guard block.
            arm_ops.drain(5..10);
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF32S, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "upper-only trunc guard must be Invalid, got {result:?}"
            );
        });
    }

    // --- i32.trunc_f64_s/u (LIVE, #709/#756 class, D-register guard) ---

    /// The SHIPPED f64 trunc domain-guard shape (instruction_selector.rs
    /// I32TruncF64S/U, lines 3158-3220): per bound, F64Const scratch into D1 ;
    /// ordered VCMP.F64 into R0 ; CMP R0,#0 ; BNE +0 (in-range skips) ; UDF —
    /// then the VCVT. Operand in D0, bound scratch D1. Upper bound uses F64Lt,
    /// lower uses F64Gt (STRICT — both false on NaN, so NaN traps at the first
    /// guard). Bounds are the exact selector constants.
    fn shipped_trunc_f64_guard(signed: bool) -> Vec<ArmOp> {
        use synth_synthesis::rules::VfpReg;
        let (hi, lo) = if signed {
            (2147483648.0_f64, -2147483649.0_f64) // 2^31, -(2^31)-1
        } else {
            (4294967296.0_f64, -1.0_f64) // 2^32, -1.0
        };
        let mut ops = Vec::new();
        let guard = |ops: &mut Vec<ArmOp>, bound: f64, upper: bool| {
            ops.push(ArmOp::F64Const {
                dd: VfpReg::D1,
                value: bound,
            });
            let cmp = if upper {
                ArmOp::F64Lt {
                    rd: Reg::R0,
                    dn: VfpReg::D0,
                    dm: VfpReg::D1,
                }
            } else {
                ArmOp::F64Gt {
                    rd: Reg::R0,
                    dn: VfpReg::D0,
                    dm: VfpReg::D1,
                }
            };
            ops.push(cmp);
            ops.push(ArmOp::Cmp {
                rn: Reg::R0,
                op2: Operand2::Imm(0),
            });
            ops.push(ArmOp::BCondOffset {
                cond: Condition::NE,
                offset: 0,
            });
            ops.push(ArmOp::Udf { imm: 0 });
        };
        guard(&mut ops, hi, true); // x < hi (also traps NaN)
        guard(&mut ops, lo, false); // x > lo
        if signed {
            ops.push(ArmOp::I32TruncF64S {
                rd: Reg::R0,
                dm: VfpReg::D0,
            });
        } else {
            ops.push(ArmOp::I32TruncF64U {
                rd: Reg::R0,
                dm: VfpReg::D0,
            });
        }
        ops
    }

    #[test]
    fn trunc_f64_s_domain_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF64S, &shipped_trunc_f64_guard(true))
                .unwrap();
            assert_eq!(
                result,
                ValidationResult::Verified,
                "GREEN: correct f64→i32_s domain guard must be Verified (Unsat)"
            );
        });
    }

    #[test]
    fn trunc_f64_u_domain_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF64U, &shipped_trunc_f64_guard(false))
                .unwrap();
            assert_eq!(
                result,
                ValidationResult::Verified,
                "GREEN: correct f64→i32_u domain guard must be Verified (Unsat)"
            );
        });
    }

    /// RED-FIRST for the f64 #709 class: the bare saturating VCVT (guards
    /// stripped) never traps — rejected with a counterexample (Sat).
    #[test]
    fn trunc_f64_without_domain_guard_is_rejected() {
        use synth_synthesis::rules::VfpReg;
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [ArmOp::I32TruncF64S {
                rd: Reg::R0,
                dm: VfpReg::D0,
            }];
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF64S, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "RED: guard-stripped f64 trunc must be Invalid (Sat), got {result:?}"
            );
        });
    }

    /// RED-FIRST: half an f64 domain guard (upper bound only) drops the
    /// lower-bound (NaN-negative-overflow) trap — must be caught.
    #[test]
    fn trunc_f64_with_only_upper_guard_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let mut arm_ops = shipped_trunc_f64_guard(true);
            // Strip the second (lower-bound) guard: 5 ops per guard block.
            arm_ops.drain(5..10);
            let result = validator
                .verify_trap_preservation(&WasmOp::I32TruncF64S, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "RED: upper-only f64 trunc guard must be Invalid (Sat), got {result:?}"
            );
        });
    }

    // --- i64 div/rem (LIVE at the pseudo-op guard-field level, #756) ---

    /// The SHIPPED i64 div/rem pseudo-op (instruction_selector.rs 5556-5604):
    /// register pairs R0:R1 (dividend) / R2:R3 (divisor), result R0:R1, with
    /// both guard-elision fields `false` (full guards). `elide_zero`/
    /// `elide_overflow` override the fields to model a dropped guard.
    fn shipped_i64_div_rem(op: &WasmOp, elide_zero: bool, elide_overflow: bool) -> Vec<ArmOp> {
        let arm = match op {
            WasmOp::I64DivS => ArmOp::I64DivS {
                rdlo: Reg::R0,
                rdhi: Reg::R1,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: elide_zero,
                elide_overflow_guard: elide_overflow,
            },
            WasmOp::I64DivU => ArmOp::I64DivU {
                rdlo: Reg::R0,
                rdhi: Reg::R1,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: elide_zero,
            },
            WasmOp::I64RemS => ArmOp::I64RemS {
                rdlo: Reg::R0,
                rdhi: Reg::R1,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: elide_zero,
            },
            WasmOp::I64RemU => ArmOp::I64RemU {
                rdlo: Reg::R0,
                rdhi: Reg::R1,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: elide_zero,
            },
            _ => unreachable!("shipped_i64_div_rem: not an i64 div/rem op"),
        };
        vec![arm]
    }

    #[test]
    fn i64_div_rem_all_four_full_guards_preserve_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [
                WasmOp::I64DivU,
                WasmOp::I64DivS,
                WasmOp::I64RemU,
                WasmOp::I64RemS,
            ] {
                let arm_ops = shipped_i64_div_rem(&op, false, false);
                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
                assert_eq!(
                    result,
                    ValidationResult::Verified,
                    "GREEN: {op:?} with full guards must be Verified (Unsat)"
                );
            }
        });
    }

    /// RED-FIRST: dropping the ÷0 guard (elide_zero_guard = true) on ANY of the
    /// four i64 div/rem ops must be caught — the shipped fields say the guard
    /// was elided without a discharged divisor-nonzero fact.
    #[test]
    fn i64_div_rem_dropped_zero_guard_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [
                WasmOp::I64DivU,
                WasmOp::I64DivS,
                WasmOp::I64RemU,
                WasmOp::I64RemS,
            ] {
                let arm_ops = shipped_i64_div_rem(&op, true, false);
                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
                assert!(
                    matches!(result, ValidationResult::Invalid { .. }),
                    "RED: {op:?} with the ÷0 guard dropped must be Invalid (Sat), got {result:?}"
                );
            }
        });
    }

    /// RED-FIRST: dropping ONLY the INT64_MIN/-1 overflow guard on div_s (÷0
    /// still present) is a partial #633-class drop — must be caught.
    #[test]
    fn i64_div_s_dropped_overflow_guard_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = shipped_i64_div_rem(&WasmOp::I64DivS, false, true);
            let result = validator
                .verify_trap_preservation(&WasmOp::I64DivS, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "RED: i64.div_s with the overflow guard dropped must be Invalid (Sat), got {result:?}"
            );
        });
    }

    /// RED-FIRST: dropping BOTH div_s guards is the fully-unguarded shape.
    #[test]
    fn i64_div_s_dropped_both_guards_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = shipped_i64_div_rem(&WasmOp::I64DivS, true, true);
            let result = validator
                .verify_trap_preservation(&WasmOp::I64DivS, &arm_ops)
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "RED: i64.div_s with both guards dropped must be Invalid (Sat), got {result:?}"
            );
        });
    }

    /// NON-VACUITY control for the div_s overflow clause: the OVERFLOW-only
    /// drop and the correct full guard must give OPPOSITE verdicts. Proves the
    /// gate discriminates on the overflow field, not just ÷0.
    #[test]
    fn i64_div_s_overflow_field_is_load_bearing() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let full = validator
                .verify_trap_preservation(
                    &WasmOp::I64DivS,
                    &shipped_i64_div_rem(&WasmOp::I64DivS, false, false),
                )
                .unwrap();
            let overflow_dropped = validator
                .verify_trap_preservation(
                    &WasmOp::I64DivS,
                    &shipped_i64_div_rem(&WasmOp::I64DivS, false, true),
                )
                .unwrap();
            assert_eq!(full, ValidationResult::Verified);
            assert!(matches!(overflow_dropped, ValidationResult::Invalid { .. }));
            assert_ne!(
                full, overflow_dropped,
                "non-vacuity: the overflow-guard field must change the verdict"
            );
        });
    }

    /// NON-VACUITY dump (run with `--nocapture`): prints the raw
    /// Preserved/Dropped verdict for the shipped-vs-dropped-guard shapes of the
    /// two newly-live classes, so the gate's discrimination is visible, not
    /// merely asserted. A gate that printed the SAME verdict on both rows would
    /// be vacuous.
    #[test]
    fn dump_756_non_vacuity_verdicts() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let raw = |r: &ValidationResult| match r {
                ValidationResult::Verified => "Verified/Unsat (trap PRESERVED)",
                ValidationResult::Invalid { .. } => "Invalid/Sat  (trap DROPPED — caught)",
                ValidationResult::Unknown { .. } => "Unknown",
            };
            println!("\n=== #756 live trap-preservation non-vacuity ===");
            for (op, oflow_field) in [
                (WasmOp::I64DivU, false),
                (WasmOp::I64DivS, true),
                (WasmOp::I64RemU, false),
                (WasmOp::I64RemS, false),
            ] {
                let green = validator
                    .verify_trap_preservation(&op, &shipped_i64_div_rem(&op, false, false))
                    .unwrap();
                let red = validator
                    .verify_trap_preservation(&op, &shipped_i64_div_rem(&op, true, false))
                    .unwrap();
                println!(
                    "  {op:?}: full-guards -> {} | drop-÷0 -> {}",
                    raw(&green),
                    raw(&red)
                );
                assert_ne!(
                    green, red,
                    "{op:?}: green and red must differ (non-vacuous)"
                );
                if oflow_field {
                    let red_o = validator
                        .verify_trap_preservation(&op, &shipped_i64_div_rem(&op, false, true))
                        .unwrap();
                    println!("  {op:?}: drop-overflow -> {}", raw(&red_o));
                    assert_ne!(green, red_o);
                }
            }
            for (op, sgn) in [(WasmOp::I32TruncF64S, true), (WasmOp::I32TruncF64U, false)] {
                let green = validator
                    .verify_trap_preservation(&op, &shipped_trunc_f64_guard(sgn))
                    .unwrap();
                let bare = if sgn {
                    vec![ArmOp::I32TruncF64S {
                        rd: Reg::R0,
                        dm: synth_synthesis::rules::VfpReg::D0,
                    }]
                } else {
                    vec![ArmOp::I32TruncF64U {
                        rd: Reg::R0,
                        dm: synth_synthesis::rules::VfpReg::D0,
                    }]
                };
                let red = validator.verify_trap_preservation(&op, &bare).unwrap();
                println!(
                    "  {op:?}: domain-guard -> {} | bare-VCVT -> {}",
                    raw(&green),
                    raw(&red)
                );
                assert_ne!(
                    green, red,
                    "{op:?}: green and red must differ (non-vacuous)"
                );
            }
            println!("=== all rows discriminate: gate is non-vacuous ===\n");
        });
    }

    // --- i64 rem VALUE model (VCR-VER, #825/#836): native BvTerm::Urem ---
    //
    // The i64 rem_u/rem_s VC now asserts the VALUE, not just the trap. Under
    // the old HAVOC model the register result was an unconstrained fresh
    // symbol, so ANY lowering (correct, wrong-remainder, wrong-destination)
    // trivially satisfied a value-only obligation — the model proved nothing.
    // These tests pin the value model as load-bearing.

    /// Build an i64 rem pseudo-op with a chosen DESTINATION register pair. The
    /// shipped ABI is `rd = R0:R1`; a lowering that writes elsewhere leaves
    /// R0:R1 unrelated to the remainder and must be REJECTED by the value VC.
    fn i64_rem_with_dest(op: &WasmOp, rdlo: Reg, rdhi: Reg) -> Vec<ArmOp> {
        let arm = match op {
            WasmOp::I64RemU => ArmOp::I64RemU {
                rdlo,
                rdhi,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: false,
            },
            WasmOp::I64RemS => ArmOp::I64RemS {
                rdlo,
                rdhi,
                rnlo: Reg::R0,
                rnhi: Reg::R1,
                rmlo: Reg::R2,
                rmhi: Reg::R3,
                elide_zero_guard: false,
            },
            _ => unreachable!("i64_rem_with_dest: not an i64 rem op"),
        };
        vec![arm]
    }

    /// GREEN: the shipped rem_u/rem_s lowering (`rd = R0:R1`) computes the
    /// correct 64-bit remainder into the ABI return pair — the value+trap VC
    /// must be Verified.
    #[test]
    fn i64_rem_shipped_value_is_verified() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
                let arm_ops = shipped_i64_div_rem(&op, false, false);
                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
                assert_eq!(
                    result,
                    ValidationResult::Verified,
                    "GREEN: {op:?} shipped lowering (correct value + ÷0 guard) must be Verified"
                );
            }
        });
    }

    /// RED / NON-VACUITY (the key gate): a lowering that writes the remainder
    /// to the WRONG destination pair (`rd = R2:R3` instead of the ABI `R0:R1`)
    /// leaves R0:R1 holding the (unrelated) input operands, so the ABI return
    /// pair is NOT the remainder. Under the old HAVOC model this was ACCEPTED
    /// (the result symbol was unconstrained); the native `BvTerm::Urem` value
    /// model now REJECTS it. This is the accepted-under-havoc → rejected-now
    /// discriminator.
    #[test]
    fn i64_rem_wrong_destination_register_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
                let arm_ops = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
                let result = validator.verify_trap_preservation(&op, &arm_ops).unwrap();
                assert!(
                    matches!(result, ValidationResult::Invalid { .. }),
                    "RED: {op:?} writing the remainder to R2:R3 (not the ABI R0:R1) \
                     leaves R0:R1 non-remainder — must be Invalid, got {result:?}"
                );
            }
        });
    }

    /// RED / NON-VACUITY on the ARITHMETIC, not just the register file: a
    /// lowering that computes the remainder with the WRONG SIGNEDNESS —
    /// `rem_u` lowered to the signed pseudo-op, or `rem_s` to the unsigned one
    /// — writes to the correct ABI pair `R0:R1` and preserves the ÷0 trap, so
    /// the destination check above cannot see it. Only a real value model can:
    /// `bvurem` and `bvsrem` differ exactly when an operand's sign bit is set.
    ///
    /// This is the strictly stronger discriminator. It fails under HAVOC (both
    /// sides unconstrained ⟹ Verified) and under any model that got the value
    /// "shape" right but the operation wrong, and the counterexamples it
    /// produces are the expected ones (a negative dividend for `rem_u`-as-
    /// `rem_s`, a negative divisor for `rem_s`-as-`rem_u`).
    #[test]
    fn i64_rem_wrong_signedness_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // (spec op, lowering op) — same ABI destination, wrong arithmetic.
            for (spec, lowered) in [
                (WasmOp::I64RemU, WasmOp::I64RemS),
                (WasmOp::I64RemS, WasmOp::I64RemU),
            ] {
                let arm_ops = i64_rem_with_dest(&lowered, Reg::R0, Reg::R1);
                let result = validator.verify_trap_preservation(&spec, &arm_ops).unwrap();
                assert!(
                    matches!(result, ValidationResult::Invalid { .. }),
                    "RED: {spec:?} lowered as {lowered:?} computes the wrong remainder \
                     into the right registers — must be Invalid, got {result:?}"
                );
            }
        });
    }

    /// NON-VACUITY control: the correct-destination and wrong-destination
    /// lowerings must give OPPOSITE verdicts. A gate that returned the same
    /// verdict for both (as the HAVOC model did — both trivially valued) would
    /// be vacuous.
    #[test]
    fn i64_rem_destination_field_is_load_bearing() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
                let correct = validator
                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R0, Reg::R1))
                    .unwrap();
                let wrong = validator
                    .verify_trap_preservation(&op, &i64_rem_with_dest(&op, Reg::R2, Reg::R3))
                    .unwrap();
                assert_eq!(correct, ValidationResult::Verified, "{op:?} correct dest");
                assert!(
                    matches!(wrong, ValidationResult::Invalid { .. }),
                    "{op:?} wrong dest"
                );
                assert_ne!(
                    correct, wrong,
                    "non-vacuity: {op:?} destination register must change the verdict"
                );
            }
        });
    }

    /// EVIDENCE that the value model closed a real gap: the OLD trap-only VC
    /// (`verify_i64_div_rem_trap_preservation`, still present for div) ACCEPTS
    /// the wrong-destination rem lowering — it never reads the value — whereas
    /// the NEW value VC (`verify_i64_rem_value_preservation`, dispatched by
    /// `verify_trap_preservation`) REJECTS it. Opposite verdicts from the two
    /// gates on the same input is the accepted-under-havoc → rejected-now
    /// proof, made concrete rather than merely narrated.
    #[test]
    fn i64_rem_value_model_closes_a_trap_only_gap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            for op in [WasmOp::I64RemU, WasmOp::I64RemS] {
                let wrong = i64_rem_with_dest(&op, Reg::R2, Reg::R3);
                // Old trap-only path: value/destination invisible → accepted.
                let trap_only = validator
                    .verify_i64_div_rem_trap_preservation(&op, &wrong)
                    .unwrap();
                assert_eq!(
                    trap_only,
                    ValidationResult::Verified,
                    "the trap-ONLY VC is blind to the wrong destination (this is the \
                     havoc-era gap): {op:?} expected Verified, got {trap_only:?}"
                );
                // New value+trap path: destination is load-bearing → rejected.
                let value = validator.verify_trap_preservation(&op, &wrong).unwrap();
                assert!(
                    matches!(value, ValidationResult::Invalid { .. }),
                    "the value VC catches it: {op:?} expected Invalid, got {value:?}"
                );
                assert_ne!(trap_only, value, "the two gates must disagree ({op:?})");
            }
        });
    }

    // --- call_indirect (LIVE at the pseudo-op guard level, #642/#664/#676) ---

    fn call_indirect_pseudo(
        table_size: u32,
        null_check: bool,
        type_check: Option<(u32, u32)>,
    ) -> ArmOp {
        ArmOp::CallIndirect {
            rd: Reg::R0,
            type_idx: 0,
            table_index_reg: Reg::R0,
            table_size,
            table_byte_offset: 0,
            null_check,
            type_check,
        }
    }

    #[test]
    fn call_indirect_matching_guards_preserve_the_traps() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // Homogeneous table, all slots initialized: bounds clause only.
            let result = validator
                .verify_call_indirect_trap_preservation(
                    &call_indirect_pseudo(8, false, None),
                    &CallIndirectSpec {
                        table_size: 8,
                        may_have_null_slot: false,
                        heterogeneous_expected_type: None,
                    },
                )
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
            // Null-slot table + runtime type check, guards resolved.
            let result = validator
                .verify_call_indirect_trap_preservation(
                    &call_indirect_pseudo(8, true, Some((3, 32))),
                    &CallIndirectSpec {
                        table_size: 8,
                        may_have_null_slot: true,
                        heterogeneous_expected_type: Some(3),
                    },
                )
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    /// RED-FIRST for the #664 class: table has uninitialized slots but the
    /// selector resolved `null_check: false` — the null trap is dropped.
    #[test]
    fn call_indirect_dropped_null_check_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_call_indirect_trap_preservation(
                    &call_indirect_pseudo(8, false, None),
                    &CallIndirectSpec {
                        table_size: 8,
                        may_have_null_slot: true,
                        heterogeneous_expected_type: None,
                    },
                )
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "dropped null check must be Invalid, got {result:?}"
            );
        });
    }

    /// RED-FIRST for the #642 class: the selector resolved the WRONG table
    /// size — indices in the gap escape the bounds trap.
    #[test]
    fn call_indirect_wrong_table_size_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_call_indirect_trap_preservation(
                    &call_indirect_pseudo(16, false, None),
                    &CallIndirectSpec {
                        table_size: 8,
                        may_have_null_slot: false,
                        heterogeneous_expected_type: None,
                    },
                )
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "wrong bounds size must be Invalid, got {result:?}"
            );
        });
    }

    /// RED-FIRST for the #676 class: heterogeneous table but the runtime
    /// type check was dropped.
    #[test]
    fn call_indirect_dropped_type_check_is_rejected() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let result = validator
                .verify_call_indirect_trap_preservation(
                    &call_indirect_pseudo(8, true, None),
                    &CallIndirectSpec {
                        table_size: 8,
                        may_have_null_slot: true,
                        heterogeneous_expected_type: Some(3),
                    },
                )
                .unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "dropped type check must be Invalid, got {result:?}"
            );
        });
    }

    // --- verify_rule routes partial ops through the trap VC (mandatory) ---

    #[test]
    fn verify_rule_routes_partial_ops_through_the_trap_gate() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // A bare-UDIV rule: value-plausible, trap-dropping. verify_rule
            // must report Invalid (via the trap VC), not silently value-check.
            let rule = SynthesisRule {
                name: "i32.div_u → bare UDIV (trap-dropping)".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32DivU),
                replacement: Replacement::ArmInstr(ArmOp::Udiv {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                }),
                cost: Cost {
                    cycles: 1,
                    code_size: 4,
                    registers: 2,
                },
            };
            let result = validator.verify_rule(&rule).unwrap();
            assert!(
                matches!(result, ValidationResult::Invalid { .. }),
                "verify_rule must reject the trap-dropping div rule, got {result:?}"
            );

            // The guarded shape goes green through the same entry point.
            let rule = SynthesisRule {
                name: "i32.div_u → guarded UDIV".into(),
                priority: 0,
                pattern: Pattern::WasmInstr(WasmOp::I32DivU),
                replacement: Replacement::ArmSequence(shipped_divu_guard()),
                cost: Cost {
                    cycles: 4,
                    code_size: 10,
                    registers: 2,
                },
            };
            assert_eq!(
                validator.verify_rule(&rule).unwrap(),
                ValidationResult::Verified
            );
        });
    }

    #[test]
    fn trap_preservation_gate_rejects_non_div_ops() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let err = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32Add, &[])
                .unwrap_err();
            assert!(matches!(err, VerificationError::UnsupportedOperation(_)));
            // i64 div/rem is a div op but this method models 32-bit only —
            // it must Err rather than build wrong-width terms.
            let err64 = validator
                .verify_div_rem_trap_preservation(&WasmOp::I64DivU, &[])
                .unwrap_err();
            assert!(matches!(err64, VerificationError::UnsupportedOperation(_)));
        });
    }

    #[test]
    fn test_verify_add_correct() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            let rule = create_test_rule(
                WasmOp::I32Add,
                ArmOp::Add {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );

            let result = validator.verify_rule(&rule).unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn test_verify_sub_correct() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            let rule = create_test_rule(
                WasmOp::I32Sub,
                ArmOp::Sub {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );

            let result = validator.verify_rule(&rule).unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn test_verify_mul_correct() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            let rule = create_test_rule(
                WasmOp::I32Mul,
                ArmOp::Mul {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                },
            );

            let result = validator.verify_rule(&rule).unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn test_verify_and_correct() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            let rule = create_test_rule(
                WasmOp::I32And,
                ArmOp::And {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );

            let result = validator.verify_rule(&rule).unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn test_verify_incorrect_rule() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            // INCORRECT rule: WASM i32.add -> ARM SUB (should find counterexample)
            let rule = create_test_rule(
                WasmOp::I32Add,
                ArmOp::Sub {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );

            let result = validator.verify_rule(&rule).unwrap();

            match result {
                ValidationResult::Invalid { counterexample } => {
                    assert!(!counterexample.is_empty());
                }
                _ => panic!("Expected counterexample but got: {:?}", result),
            }
        });
    }

    #[test]
    fn test_verify_bitwise_ops() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();

            // Test OR
            let or_rule = create_test_rule(
                WasmOp::I32Or,
                ArmOp::Orr {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );
            assert_eq!(
                validator.verify_rule(&or_rule).unwrap(),
                ValidationResult::Verified
            );

            // Test XOR
            let xor_rule = create_test_rule(
                WasmOp::I32Xor,
                ArmOp::Eor {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    op2: Operand2::Reg(Reg::R1),
                },
            );
            assert_eq!(
                validator.verify_rule(&xor_rule).unwrap(),
                ValidationResult::Verified
            );
        });
    }

    #[test]
    fn test_verify_shift_ops() {
        // Note: Shift operations require concrete immediate values in ARM
        // but use register operands in WASM. Verification requires
        // modeling the shift amount modulo operation.
        // TODO: Implement shift verification with proper modulo handling
    }
}