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 expansion_validator::ExpansionError;

pub use expansion_validator::ExpansionWitness;

pub use expansion_validator::covered_i64_pseudo_selections;

pub use expansion_validator::validate_expansion;

pub use fact_spec::FactSpecResult;

pub use fact_spec::specialize_function;

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::CallIndirectSpec;

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

addr

Static-data addressing validation (VCR-VER-003, synth #777 / #757).

arm_semantics

ARM Semantics Encoding to SMT

expansion_validator

Expansion-level certifying validation for the i64 pseudo-ops (#667 move 2).

fact_spec

Proof-carrying specialization — VCR-PERF-002 / #494 Phase 2: the single-elision prototype (value-range facts ⇒ dead conditional-branch elision, the gust_mix clamp shape).

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

trap

Trap-preservation obligations (VCR-VER-002, synth #166 / ordeal#59).

validator_pattern

Validator-Pattern Verification (Issue #76)

wasm_semantics

WASM Semantics Encoding to SMT

Structs

AddrMismatch

A single reloc that reads the wrong byte.

DataSegment

One active WASM data segment: its linear-memory offset and its bytes, in declaration order. The packed .data blob stores these bytes verbatim (4-aligned per segment) under __synth_wasm_seg_K; index K in the segment list is the K in the symbol name.

RelocResolution

The retargeting the compiler emitted for one static-data relocation: it now points at __synth_wasm_seg_{seg_index} + addend. seg_index is the K from the emitted symbol name; addend is the emitted in-place REL addend (= original_access_addr - seg[K].linmem_off). This is the value read back from what the compiler produced — NEVER recomputed by the validator (that would mirror-pin the check and make it vacuous).

Enums

AddrVerdict

The verdict of the addressing gate.

Functions

resolve_owner

Resolve an access address c to its owning segment index under a chosen tie-break policy, mirroring main.rs’s .rposition() / .position() search. last_wins = true is the CORRECT WASM overwrite semantics (.rposition()); last_wins = false is the #757 miscompile (.position()). Returns the segment index and the addend c - seg.linmem_off, or None if c is in no segment. Exposed so the red-first gate can toggle the policy as an argument (no source revert), and so callers can build resolutions the same way the compiler does.

validate_reloc_resolutions

The per-compilation addressing gate. For every emitted RelocResolution, assert the packed byte it serves equals the runtime-image byte at the original access address. See the module docs for the invariant.

with_verification_context

Run verification operations in a configured context.