Crate spec_checker 

M10: Spec proof checker. Spec §14.

Specs are properties attached to a function signature. The checker tries to prove a spec holds for every input that satisfies the quantifier constraints, and reports one of:

• proved — the property holds (by randomized search across N trials, or by an SMT prover when one is available).
• counterexample — concrete inputs that falsify the property.
• inconclusive — the search couldn’t decide one way or the other.

Strategies

• Randomized (default, pure-Rust). Generates inputs from a deterministic seed, checks the property by actually running the target function in the Lex VM. Reports proved after surviving 1000 trials by default. This is honest about the method via evidence.method = "randomized".
• SMT-LIB export. The spec can be lowered to SMT-LIB text for pasting into an external Z3 (z3 -smt2 file.smt). We don’t link libz3 here to keep the dep surface light; that’s a follow-up feature flag.

Spec DSL

spec clamp {
  forall x :: Int, lo :: Int, hi :: Int where lo <= hi:
    let r := clamp(x, lo, hi)
    (r >= lo) and (r <= hi)
}

Structs

CheckResult

Evidence

Quantifier

Spec

SpecParseError

Enums

GateVerdict

Verdict returned by evaluate_gate.

ProofStatus

SpecExpr

SpecOp

SpecType

Functions

check_spec

Check a spec against a Lex program. The program must define the function the spec refers to (by name).

evaluate_gate

Evaluate every spec against bindings and return the first non-Allow verdict (or Allow if all pass). lex_source supplies the host program — any SpecExpr::Call in a spec’s body resolves to a function in this program.

evaluate_gate_compiled

Same as evaluate_gate but takes already-compiled bytecode. Use when gating at high frequency: compile the program once, evaluate many actions against it.

evaluate_gate_compiled_traced

Like evaluate_gate_compiled but additionally threads a caller-supplied tracer into every Vm the spec body spins up for SpecExpr::Call (#199).

parse_spec

to_smtlib