synth_verify/
lib.rs

1//! Formal Verification for Synth Compiler
2//!
3//! This crate provides SMT-based translation validation and property-based testing
4//! to formally verify the correctness of WebAssembly-to-native synthesis.
5//!
6//! # Architecture
7//!
8//! The verification system proves that synthesized native code has
9//! semantically equivalent behavior to the input WASM code, discharging the
10//! QF_BV queries through a thin solver trait ([`solver::BvSolver`], #553):
11//!
12//! - **Default engine:** [`ordeal`] — pure Rust, certificate-checked
13//!   (every `Unsat` verdict carries an LRAT proof validated by the trusted
14//!   `ordeal-lrat` checker). No C++ toolchain required.
15//! - **Differential oracle** (feature `z3-solver`): Z3, the former engine.
16//!   With both backends compiled in and `SYNTH_SOLVER_DIFF=1`, every query
17//!   runs through both — a verdict disagreement is a hard error; an ordeal
18//!   `Unknown` falls through to Z3's verdict.
19//!
20//! ## Backend-Agnostic Traits
21//!
22//! `SourceSemantics` and `TargetSemantics` traits allow any backend to provide
23//! SMT semantics. The ARM semantics are one implementation, behind the `arm`
24//! feature. All semantics encode into the solver-agnostic [`term::BV`] /
25//! [`term::Bool`] terms.
26//!
27//! ## Translation Validation
28//!
29//! For each synthesis rule WASM → target, we construct SMT formulas:
30//! - φ_wasm: Semantics of WASM operations
31//! - φ_target: Semantics of generated target operations
32//! - Prove: ∀inputs. φ_wasm(inputs) ⟺ φ_target(inputs)
33
34// Solver-agnostic terms + the thin solver trait (always available)
35pub mod solver;
36pub mod term;
37
38// Verification traits (always available)
39pub mod traits;
40
41// WASM semantics — source language for all backends (always available)
42pub mod wasm_semantics;
43
44// ARM semantics (behind the arm feature)
45#[cfg(feature = "arm")]
46pub mod arm_semantics;
47
48// Translation validator (requires arm for the existing concrete implementation)
49#[cfg(feature = "arm")]
50pub mod translation_validator;
51
52// Validator-pattern prototype (issue #76 — CompCert-style certifying
53// validator scaffolding; see docs/validator-pattern.md).
54#[cfg(feature = "arm")]
55pub mod validator_pattern;
56
57// Property-based testing (requires arm: exercises the ARM synthesis rules)
58#[cfg(feature = "arm")]
59pub mod properties;
60
61#[cfg(feature = "arm")]
62pub use properties::CompilerProperties;
63
64#[cfg(feature = "arm")]
65pub use arm_semantics::{ArmSemantics, ArmState};
66pub use solver::{BvSolver, CheckOutcome, OrdealSolver, new_solver};
67pub use term::{BV, Bool};
68#[cfg(feature = "arm")]
69pub use translation_validator::{TranslationValidator, ValidationResult, VerificationError};
70#[cfg(feature = "arm")]
71pub use validator_pattern::{
72    CertifiedSelection, SolverResultKind, ValidationError as PatternValidationError, Validator,
73    Witness, Z3ArmValidator,
74};
75pub use wasm_semantics::WasmSemantics;
76
77/// Run verification operations in a configured context.
78///
79/// With the default (ordeal) engine this is a plain call — the pure-Rust
80/// solver needs no global context. With the `z3-solver` feature compiled in,
81/// it additionally configures the Z3 thread-local context (30-second timeout,
82/// model generation) so the differential oracle is ready.
83pub fn with_verification_context<F, R>(f: F) -> R
84where
85    F: FnOnce() -> R + Send + Sync,
86    R: Send + Sync,
87{
88    #[cfg(feature = "z3-solver")]
89    {
90        with_z3_context(f)
91    }
92    #[cfg(not(feature = "z3-solver"))]
93    {
94        f()
95    }
96}
97
98/// Run verification operations with a configured Z3 context.
99///
100/// Z3 0.19 uses thread-local context — this function configures it
101/// with a 30-second timeout and model generation enabled.
102#[cfg(feature = "z3-solver")]
103pub fn with_z3_context<F, R>(f: F) -> R
104where
105    F: FnOnce() -> R + Send + Sync,
106    R: Send + Sync,
107{
108    let mut cfg = z3::Config::new();
109    cfg.set_timeout_msec(30000); // 30 second timeout
110    cfg.set_model_generation(true);
111    z3::with_z3_config(&cfg, f)
112}
113
114/// Create a Z3 solver with default configuration (differential-oracle use)
115#[cfg(feature = "z3-solver")]
116pub fn create_solver() -> z3::Solver {
117    z3::Solver::new()
118}
119
120#[cfg(test)]
121mod tests {
122    use super::*;
123
124    #[test]
125    fn test_default_solver_decides() {
126        with_verification_context(|| {
127            let mut solver = new_solver();
128            let x = BV::new_const("x", 32);
129            solver.assert(&x.eq(&x).not());
130            assert_eq!(solver.check(), CheckOutcome::Unsat);
131        });
132    }
133
134    #[cfg(feature = "z3-solver")]
135    #[test]
136    fn test_z3_context_creation() {
137        with_z3_context(|| {
138            let solver = create_solver();
139            assert_eq!(solver.check(), z3::SatResult::Sat);
140        });
141    }
142}
synth_verify/lib.rs

synth_verify/
lib.rs
