Crate synth_verify 

Formal Verification for Synth Compiler

This crate provides SMT-based translation validation and property-based testing to formally verify the correctness of WebAssembly-to-native synthesis.

Architecture

The verification system proves that synthesized native code has semantically equivalent behavior to the input WASM code, discharging the QF_BV queries through a thin solver trait (solver::BvSolver, #553):

• Default engine: ordeal — pure Rust, certificate-checked (every Unsat verdict carries an LRAT proof validated by the trusted ordeal-lrat checker). No C++ toolchain required.
• Differential oracle (feature z3-solver): Z3, the former engine. With both backends compiled in and SYNTH_SOLVER_DIFF=1, every query runs through both — a verdict disagreement is a hard error; an ordeal Unknown falls through to Z3’s verdict.

Backend-Agnostic Traits

SourceSemantics and TargetSemantics traits allow any backend to provide SMT semantics. The ARM semantics are one implementation, behind the arm feature. All semantics encode into the solver-agnostic term::BV / term::Bool terms.

Translation Validation

For each synthesis rule WASM → target, we construct SMT formulas:

• φ_wasm: Semantics of WASM operations
• φ_target: Semantics of generated target operations
• Prove: ∀inputs. φ_wasm(inputs) ⟺ φ_target(inputs)

Re-exports

pub use properties::CompilerProperties;

pub use arm_semantics::ArmSemantics;

pub use arm_semantics::ArmState;

pub use solver::BvSolver;

pub use solver::CheckOutcome;

pub use solver::OrdealSolver;

pub use solver::new_solver;

pub use term::BV;

pub use term::Bool;

pub use translation_validator::TranslationValidator;

pub use translation_validator::ValidationResult;

pub use translation_validator::VerificationError;

pub use validator_pattern::CertifiedSelection;

pub use validator_pattern::SolverResultKind;

pub use validator_pattern::ValidationError as PatternValidationError;

pub use validator_pattern::Validator;

pub use validator_pattern::Witness;

pub use validator_pattern::Z3ArmValidator;

pub use wasm_semantics::WasmSemantics;

Modules

arm_semantics

ARM Semantics Encoding to SMT

properties

Property-Based Testing for Compiler Correctness

solver

The thin solver trait behind which the SMT engines sit (#553).

term

Solver-agnostic bitvector / boolean term types (#553).

traits

Verification traits for backend-agnostic translation validation

translation_validator

Translation Validator - Proves equivalence between WASM and ARM code

validator_pattern

Validator-Pattern Verification (Issue #76)

wasm_semantics

WASM Semantics Encoding to SMT

Functions

with_verification_context

Run verification operations in a configured context.