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
i64 div/rem	trap-condition only (field-derived; 64-bit quotient not modeled)	divisor R2:R3 (rmlo/rmhi), guards from the pseudo-op’s elide_* fields
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
i32.trunc_f64_s/u	trap-condition only (no float→int value model)	operand D0, bound scratch D1, result R0

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

i64 div/rem trust boundary (like call_indirect)

ARM32 has no 64-bit divide instruction: the shipped lowering emits an ArmOp::I64Div{S,U}/I64Rem{S,U} PSEUDO-OP whose result registers the exec-model leaves symbolic (no bvsdiv term) and whose trap guards are carried as elide_zero_guard/elide_overflow_guard boolean FIELDS. The gate certifies the SELECTOR’s guard-elision decision: the ARM trap term is CONSTRUCTED from those fields (a set elide_* deletes the corresponding clause), so a lowering that elides a guard whose fact was not discharged is reported Invalid. The encoder’s expansion of the pseudo-op into ORRS/BNE/UDF/library-call bytes is separately execution-gated (the i64 div/rem CI oracles).

Held out, honestly

• i64.trunc_f64_s/u — the selector loud-declines it (i64 register pairs on 32-bit ARM are unsupported), so there is NO shipped lowering to derive an ARM trap term from. The trap CLASSIFIER for these ops (trap_trunc(F64, I64, …), incl. the item-4 2^63/-2^63/2^64 boundaries) is unit-gated in tests/trap_preservation.rs.

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

i64 div/rem trap preservation (VCR-VER-002, #756): field-derived trap-condition-only VC. ARM32 has no 64-bit divide, so the shipped lowering emits a single ArmOp::I64Div{S,U}/I64Rem{S,U} pseudo-op whose 64-bit quotient the exec-model leaves symbolic (no bvsdiv term — the full value VC is not well-posed) and whose trap guards are carried as elide_* boolean FIELDS. The WASM spec side is ordeal’s 64-bit trap_div over symbolic divisor bits (rmlo:rmhi = R2:R3); the ARM side is CONSTRUCTED from the pseudo-op’s fields — a set elide_* deletes the corresponding clause — so a lowering that elides a guard (÷0 for all four, INT64_MIN/-1 overflow for div_s) whose fact was not discharged derives a weaker trap term and is reported Invalid.

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

i64 rem_u/rem_s value + trap preservation (VCR-VER, #825/#836).

Unlike Self::verify_i64_div_rem_trap_preservation (trap-only, used for div where the 64-bit quotient value VC is not well-posed), this gate asserts the FULL obligation for remainder: on the non-trapping path the ARM register pair R0:R1 must equal the native 64-bit unsigned/signed remainder of the operands, AND the ÷0 trap must be preserved. It is what makes the ArmSemantics I64RemU model — which now builds a real BvTerm::Urem term (ordeal 0.12) instead of HAVOC — actually load-bearing: a wrong remainder computation, or one that writes the answer to the wrong register pair, is now Invalid.

Operand / result convention (the shipped ABI, NOT the op’s fields)

The value is READ from the FIXED ABI return registers R0 (low) / R1 (high) and the operands are SEEDED at the FIXED ABI argument registers — dividend R0:R1, divisor R2:R3. Reading the op’s own rd* fields (or seeding its own rn*/rm*) would make the VC vacuous (read tracks write); anchoring on the ABI is exactly what lets a pseudo-op whose destination deviates from R0:R1 be REJECTED.

Trap-guarded value (why not a raw ==)

A bare arm_value == wasm_value would also assert the value on the ÷0 path, where WASM has no value and SMT-LIB bvurem-by-0 = the dividend (total) — a spurious obligation. Routing through crate::trap::DefineOrTrap + crate::trap::prove_trap_equivalence guards the value clause under non-trap. The single branch-free pseudo-op keeps the value ite-free, so no straight-line rewrite is needed (unlike the i32 guarded-div machinery).

pub fn verify_trunc_f64_trap_preservation( &self, arm_ops: &[ArmOp], signed: bool, ) -> Result<ValidationResult, VerificationError>

i32.trunc_f64_s/u trap preservation (VCR-VER-002, #166 / #709 / #756): trap-condition-only VC (synth’s QF_BV model carries no float→int value function). The WASM side is ordeal’s bit-pattern trunc classifier over the f64 operand (NaN ∨ ±∞ ∨ out-of-range); the ARM side is DERIVED from the emitted DOUBLE-precision domain guard (F64Const bound + ordered VCMP.F64 compare + Cmp/branch/Udf), with the ordered f64 compares given real bit-pattern semantics in the executor. Operand convention: f64 operand = D0 (a 64-bit BV), bound scratch = D1.

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.