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;
use crate::wasm_semantics::WasmSemantics;
use synth_core::WasmOp;
use synth_synthesis::{ArmOp, Reg, SynthesisRule};
use thiserror::Error;

/// Whether a div/rem ARM lowering carries its trap guard: synth guards a
/// divide with a `Cmp`/branch/`Udf` sequence, so the presence of a `Udf`
/// (the `undefined`/trap instruction) is the structural signal that the
/// divide-by-zero (and, for signed, overflow) trap is still enforced. Its
/// absence means the guard was dropped — the #633/#666/#642 shape.
/// (VCR-VER-002, #166.)
fn arm_sequence_has_trap_guard(arm_ops: &[ArmOp]) -> bool {
    arm_ops.iter().any(|op| matches!(op, ArmOp::Udf { .. }))
}

/// 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 },
}

/// 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(),
                ));
            }
        };

        self.verify_equivalence(wasm_op, &arm_ops)
    }

    /// 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 a
    /// div/rem lowering — that the ARM sequence preserves the WASM op's trap
    /// (`÷0`, plus `INT_MIN/-1` for the signed ops) *and* its value, discharged
    /// by [`crate::trap::prove_trap_equivalence`].
    ///
    /// The WASM trap condition is derivable from the operands. The ARM
    /// lowering's trap condition is derived **structurally** from `arm_ops`:
    /// synth guards a divide with a `Cmp`/branch/`Udf` sequence (see
    /// `synth_synthesis::contracts::division`), so a `Udf` in the sequence ⇒
    /// the guard is present and the lowering traps on the same condition; its
    /// absence ⇒ the guard was dropped (the #633/#666/#642 shape) and the
    /// lowering never traps — which this gate reports `Invalid`.
    ///
    /// # Soundness scope
    ///
    /// Sound in the **reject** direction: a div/rem lowering with no `Udf` is
    /// reported `Invalid`, catching the whole trap-drop class. Presence of a
    /// `Udf` is a *necessary* structural signal but does not by itself prove the
    /// guard fires on *exactly* `÷0 ∨ overflow`.
    ///
    // VCR-VER-002 follow-on: fully AUTO-deriving `opt.may_trap` from the shipped
    // lowering (rather than the structural `Udf`-presence proxy) needs a
    // `may_trap` flag threaded through the `ArmState` exec model so the
    // encoder's `Cmp`/`Bne`/`Udf` expansion produces a derived trap term — or,
    // equivalently, decoding the emitted guard bytes in `expansion_validator`.
    // Until then the other partial-op classes (load/store, call_indirect,
    // unreachable) have no ARM trap term on this value-only path and remain
    // gated at the unit level (`tests/trap_preservation.rs`), not here.
    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 arm_value = self.encode_arm_sequence(arm_ops, &inputs)?;

        let orig = crate::trap::DefineOrTrap {
            value: wasm_value,
            may_trap: crate::trap::trap_div(div_op, &dividend, &divisor),
        };
        let arm_may_trap = if arm_sequence_has_trap_guard(arm_ops) {
            crate::trap::trap_div(div_op, &dividend, &divisor)
        } else {
            crate::term::Bool::from_bool(false)
        };
        let opt = crate::trap::DefineOrTrap {
            value: arm_value,
            may_trap: arm_may_trap,
        };

        Ok(match crate::trap::prove_trap_equivalence(&orig, &opt) {
            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::{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:?}"),
            }
        });
    }

    #[test]
    fn div_lowering_with_guard_preserves_the_trap() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            // Guarded divide: CMP divisor,#0 ; UDF (trap) ; UDIV. The structural
            // Udf ⇒ the ÷0 trap is enforced; value matches WASM ⇒ Verified.
            let arm_ops = [
                ArmOp::Cmp {
                    rn: Reg::R1,
                    op2: Operand2::Imm(0),
                },
                ArmOp::Udf { imm: 0 },
                ArmOp::Udiv {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                },
            ];
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivU, &arm_ops)
                .unwrap();
            assert_eq!(result, ValidationResult::Verified);
        });
    }

    #[test]
    fn signed_div_guard_preserves_both_zero_and_overflow_traps() {
        with_verification_context(|| {
            let validator = TranslationValidator::new();
            let arm_ops = [
                ArmOp::Udf { imm: 0 }, // structural guard present
                ArmOp::Sdiv {
                    rd: Reg::R0,
                    rn: Reg::R0,
                    rm: Reg::R1,
                },
            ];
            let result = validator
                .verify_div_rem_trap_preservation(&WasmOp::I32DivS, &arm_ops)
                .unwrap();
            assert_eq!(result, 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
    }
}