synth-verify 0.6.0

//! 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::wasm_semantics::WasmSemantics;
use synth_core::WasmOp;
use synth_synthesis::{ArmOp, Reg, SynthesisRule};
use thiserror::Error;
use z3::ast::BV;
use z3::{SatResult, Solver};

/// 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 using Z3 SMT solver.
///
/// Z3 0.19 uses thread-local context -- no lifetime parameters needed.
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 solver = Solver::new();

        // 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() {
            SatResult::Unsat => {
                // Proven correct - no inputs exist where results differ
                Ok(ValidationResult::Verified)
            }

            SatResult::Sat => {
                // Found counterexample
                let model = solver.get_model().ok_or_else(|| {
                    VerificationError::SolverError("SAT but no model available".to_string())
                })?;

                let mut counterexample = Vec::new();
                for (i, input) in inputs.iter().enumerate() {
                    if let Some(value) = model.eval(input, true)
                        && let Some(int_val) = value.as_i64()
                    {
                        counterexample.push((format!("input_{}", i), int_val));
                    }
                }

                Ok(ValidationResult::Invalid { counterexample })
            }

            SatResult::Unknown => {
                // Verification inconclusive
                Ok(ValidationResult::Unknown {
                    reason: "SMT solver returned unknown".to_string(),
                })
            }
        }
    }

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

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

    #[test]
    fn test_verify_add_correct() {
        with_z3_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_z3_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_z3_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_z3_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_z3_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_z3_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
    }
}