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// Proof-carrying specialization (VCR-PERF-002 / #494 Phase 2): value-range
45// facts ⇒ dead conditional-branch elision, each site behind a per-elision
46// ordeal obligation. Backend-agnostic (rewrites the WasmOp stream), so it is
47// always available like `wasm_semantics`.
48pub mod fact_spec;
49
50// ARM semantics (behind the arm feature)
51#[cfg(feature = "arm")]
52pub mod arm_semantics;
53
54// Translation validator (requires arm for the existing concrete implementation)
55#[cfg(feature = "arm")]
56pub mod translation_validator;
57
58// Validator-pattern prototype (issue #76 — CompCert-style certifying
59// validator scaffolding; see docs/validator-pattern.md).
60#[cfg(feature = "arm")]
61pub mod validator_pattern;
62
63// Property-based testing (requires arm: exercises the ARM synthesis rules)
64#[cfg(feature = "arm")]
65pub mod properties;
66
67#[cfg(feature = "arm")]
68pub use properties::CompilerProperties;
69
70#[cfg(feature = "arm")]
71pub use arm_semantics::{ArmSemantics, ArmState};
72pub use fact_spec::{FactSpecResult, specialize_function};
73pub use solver::{BvSolver, CheckOutcome, OrdealSolver, new_solver};
74pub use term::{BV, Bool};
75#[cfg(feature = "arm")]
76pub use translation_validator::{TranslationValidator, ValidationResult, VerificationError};
77#[cfg(feature = "arm")]
78pub use validator_pattern::{
79    CertifiedSelection, SolverResultKind, ValidationError as PatternValidationError, Validator,
80    Witness, Z3ArmValidator,
81};
82pub use wasm_semantics::WasmSemantics;
83
84/// Run verification operations in a configured context.
85///
86/// With the default (ordeal) engine this is a plain call — the pure-Rust
87/// solver needs no global context. With the `z3-solver` feature compiled in,
88/// it additionally configures the Z3 thread-local context (30-second timeout,
89/// model generation) so the differential oracle is ready.
90pub fn with_verification_context<F, R>(f: F) -> R
91where
92    F: FnOnce() -> R + Send + Sync,
93    R: Send + Sync,
94{
95    #[cfg(feature = "z3-solver")]
96    {
97        with_z3_context(f)
98    }
99    #[cfg(not(feature = "z3-solver"))]
100    {
101        f()
102    }
103}
104
105/// Run verification operations with a configured Z3 context.
106///
107/// Z3 0.19 uses thread-local context — this function configures it
108/// with a 30-second timeout and model generation enabled.
109#[cfg(feature = "z3-solver")]
110pub fn with_z3_context<F, R>(f: F) -> R
111where
112    F: FnOnce() -> R + Send + Sync,
113    R: Send + Sync,
114{
115    let mut cfg = z3::Config::new();
116    cfg.set_timeout_msec(30000); // 30 second timeout
117    cfg.set_model_generation(true);
118    z3::with_z3_config(&cfg, f)
119}
120
121/// Create a Z3 solver with default configuration (differential-oracle use)
122#[cfg(feature = "z3-solver")]
123pub fn create_solver() -> z3::Solver {
124    z3::Solver::new()
125}
126
127#[cfg(test)]
128mod tests {
129    use super::*;
130
131    #[test]
132    fn test_default_solver_decides() {
133        with_verification_context(|| {
134            let mut solver = new_solver();
135            let x = BV::new_const("x", 32);
136            solver.assert(&x.eq(&x).not());
137            assert_eq!(solver.check(), CheckOutcome::Unsat);
138        });
139    }
140
141    #[cfg(feature = "z3-solver")]
142    #[test]
143    fn test_z3_context_creation() {
144        with_z3_context(|| {
145            let solver = create_solver();
146            assert_eq!(solver.check(), z3::SatResult::Sat);
147        });
148    }
149}
synth_verify/lib.rs

synth_verify/
lib.rs
