spec_checker/lib.rs
1//! M10: Spec proof checker. Spec §14.
2//!
3//! Specs are properties attached to a function signature. The checker
4//! tries to prove a spec holds for every input that satisfies the
5//! quantifier constraints, and reports one of:
6//!
7//! - `proved` — the property holds (by randomized search across N trials,
8//! or by an SMT prover when one is available).
9//! - `counterexample` — concrete inputs that falsify the property.
10//! - `inconclusive` — the search couldn't decide one way or the other.
11//!
12//! ### Strategies
13//!
14//! - **Randomized** (default, pure-Rust). Generates inputs from a
15//! deterministic seed, checks the property by actually running the
16//! target function in the Lex VM. Reports `proved` after surviving
17//! 1000 trials by default. This is honest about the method via
18//! `evidence.method = "randomized"`.
19//! - **SMT-LIB export**. The spec can be lowered to SMT-LIB text for
20//! pasting into an external Z3 (`z3 -smt2 file.smt`). We don't link
21//! libz3 here to keep the dep surface light; that's a follow-up
22//! feature flag.
23//!
24//! ### Spec DSL
25//!
26//! ```text
27//! spec clamp {
28//! forall x :: Int, lo :: Int, hi :: Int where lo <= hi:
29//! let r := clamp(x, lo, hi)
30//! (r >= lo) and (r <= hi)
31//! }
32//! ```
33
34mod ast;
35mod parser;
36mod checker;
37mod gate;
38mod smt;
39
40pub use ast::{Quantifier, Spec, SpecExpr, SpecOp, SpecType};
41pub use checker::{check_spec, CheckResult, Evidence, ProofStatus};
42pub use gate::{evaluate_gate, evaluate_gate_compiled, evaluate_gate_compiled_traced, GateVerdict};
43pub use parser::{parse_spec, SpecParseError};
44pub use smt::to_smtlib;