Struct TranslationValidator 

pub struct TranslationValidator { /* private fields */ }

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).

Implementations

impl TranslationValidator

pub fn new() -> Self

Create a new translation validator

pub fn set_timeout(&mut self, timeout_ms: u64)

Set verification timeout in milliseconds

pub fn verify_rule( &self, rule: &SynthesisRule, ) -> Result<ValidationResult, VerificationError>

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_equivalence( &self, wasm_op: &WasmOp, arm_ops: &[ArmOp], ) -> Result<ValidationResult, VerificationError>

Verify equivalence between a WASM operation and ARM operations

pub fn verify_equivalence_parameterized( &self, wasm_op: &WasmOp, arm_ops: &[ArmOp], concrete_params: &[(usize, i64)], ) -> Result<ValidationResult, VerificationError>

Verify equivalence with concrete parameter values

pub fn verify_parameterized_range<F>( &self, wasm_op: &WasmOp, create_arm_ops: F, param_index: usize, range: Range<i64>, ) -> Result<ValidationResult, VerificationError>

where F: Fn(i64) -> Vec<ArmOp>,

Verify operation for all parameter values in a range

pub fn verify_div_rem_trap_preservation( &self, wasm_op: &WasmOp, arm_ops: &[ArmOp], ) -> Result<ValidationResult, VerificationError>

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.

pub fn verify_rules( &self, rules: &[SynthesisRule], ) -> Vec<(String, Result<ValidationResult, VerificationError>)>

Batch verify multiple synthesis rules

Trait Implementations

impl Default for TranslationValidator

fn default() -> Self

Returns the “default value” for a type.