Module translation_validator 

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)

Structs

TranslationValidator

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

Enums

ValidationResult

Result of translation validation

VerificationError

Verification error types