feat(formal): implement full SMT-LIB support and remove stubs in `smt.rs`

`smt.rs` currently acts as a scaffolding layer between the verifier and Z3. many helper functions are stubbed (they always return `true`), and the encoding logic is narrowly tailored to a handful of ERC-20 selectors. this makes results *unsound*: the solver can declare **SAT** for specifications that should be **UNSAT**, and vice-versa.