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