synth_verify/
traits.rs

1//! Verification traits for backend-agnostic translation validation
2//!
3//! These traits allow any backend to provide SMT semantics for its target
4//! instruction set. The translation validator is generic over source and
5//! target semantics.
6//!
7//! Semantics encode into the solver-agnostic [`crate::term::BV`] terms, so
8//! implementations are independent of the SMT engine behind
9//! [`crate::solver::BvSolver`].
10
11use crate::term::BV;
12
13/// Encodes source (WASM) operation semantics as SMT formulas
14pub trait SourceSemantics {
15    /// Encode a source operation, returning the result as a bitvector
16    fn encode_op(&self, op_name: &str, inputs: &[BV]) -> Option<BV>;
17}
18
19/// Encodes target (ARM, RISC-V, etc.) operation semantics as SMT formulas
20pub trait TargetSemantics {
21    /// The target state type (registers, flags, memory)
22    type State;
23
24    /// Create a fresh symbolic state
25    fn fresh_state(&self) -> Self::State;
26
27    /// Apply a target operation to the state, returning updated state
28    fn apply_op(&self, state: &Self::State, op_name: &str, inputs: &[BV]) -> Option<Self::State>;
29
30    /// Extract the result bitvector from a state (e.g. read Rd register)
31    fn extract_result(&self, state: &Self::State, result_loc: &str) -> Option<BV>;
32}
synth_verify/traits.rs

synth_verify/
traits.rs
