Expand description
Verification traits for backend-agnostic translation validation
These traits allow any backend to provide SMT semantics for its target instruction set. The translation validator is generic over source and target semantics.
Semantics encode into the solver-agnostic crate::term::BV terms, so
implementations are independent of the SMT engine behind
crate::solver::BvSolver.
Traitsยง
- Source
Semantics - Encodes source (WASM) operation semantics as SMT formulas
- Target
Semantics - Encodes target (ARM, RISC-V, etc.) operation semantics as SMT formulas