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

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

call_indirect goes through Self::verify_call_indirect_trap_preservation (it needs module facts as the spec side).

Held out, honestly

• i64 div/rem — needs 64-bit operand terms + the register-pair ARM value model; still gated at the unit level (tests/trap_preservation.rs) and by the CI execution oracles.
• i32.trunc_f64_s/u — the guard drives f64 (D-register) compares, which the 32-bit VFP register model does not carry yet; unit-gated (trap_trunc classifier) + the m4f CI execution oracle.

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

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_mem_trap_preservation( &self, arm_ops: &[ArmOp], offset: u32, access_size: u64, ) -> Result<ValidationResult, VerificationError>

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_trunc_f32_trap_preservation( &self, arm_ops: &[ArmOp], signed: bool, ) -> Result<ValidationResult, VerificationError>

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_call_indirect_trap_preservation( &self, arm_op: &ArmOp, spec: &CallIndirectSpec, ) -> Result<ValidationResult, VerificationError>

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