Struct Z3ArmValidator 

pub struct Z3ArmValidator;

Z3-backed validator for the WASM → ARM selection pattern.

For each call the validator:

1. Allocates symbolic 32-bit inputs (a limb pair per i64 operand).
2. Builds the WASM op’s reference result from those inputs.
3. Builds the ARM sequence’s result by symbolically executing it.
4. Asserts the negation of equivalence and checks satisfiability: unsat ⇒ equivalent for all inputs (accept), sat ⇒ counterexample (reject).

The validator is trusted code: it is the small, auditable piece that replaces ~150 per-op Rocq proofs. Every formula it builds is 32-bit bitvector arithmetic that a reviewer can check by hand.

Implementations

impl Z3ArmValidator

pub fn new() -> Self

Construct a fresh validator. Callers should wrap any sequence of validate calls in crate::with_verification_context (a no-op for the default ordeal engine; configures Z3’s thread-local context when the differential oracle is compiled in).

Trait Implementations

impl Default for Z3ArmValidator

fn default() -> Self

Returns the “default value” for a type.

impl Validator<WasmOp, ArmOp> for Z3ArmValidator

fn validate( &self, sel: &CertifiedSelection<WasmOp, ArmOp>, ) -> Result<Witness, ValidationError>

Validate sel. Returns Ok(Witness) iff the selection is semantically equivalent to the source op.