spec_checker/
checker.rs

1//! Randomized checker that drives the Lex VM with generated inputs.
2
3use crate::ast::*;
4use indexmap::IndexMap;
5use lex_ast::canonicalize_program;
6use lex_bytecode::{compile_program, vm::Vm, Value};
7use lex_runtime::{DefaultHandler, Policy};
8use lex_syntax::parse_source;
9use serde::{Deserialize, Serialize};
10
11#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
12#[serde(rename_all = "snake_case")]
13pub enum ProofStatus { Proved, Counterexample, Inconclusive }
14
15#[derive(Debug, Clone, Serialize, Deserialize)]
16pub struct Evidence {
17    pub method: String,
18    pub trials: u32,
19    /// On counterexample, the failing input.
20    #[serde(default, skip_serializing_if = "Option::is_none")]
21    pub counterexample: Option<IndexMap<String, serde_json::Value>>,
22    /// On inconclusive, why we couldn't decide.
23    #[serde(default, skip_serializing_if = "Option::is_none")]
24    pub note: Option<String>,
25}
26
27#[derive(Debug, Clone, Serialize, Deserialize)]
28pub struct CheckResult {
29    pub spec_id: String,
30    pub status: ProofStatus,
31    pub evidence: Evidence,
32}
33
34/// Check a spec against a Lex program. The program must define the
35/// function the spec refers to (by name).
36///
37/// `trials`: number of random samples for the randomized strategy.
38/// Recommended ≥ 1000 for honest "proved" claims; small numbers (e.g. 10)
39/// are useful for fast smoke tests.
40pub fn check_spec(spec: &Spec, lex_source: &str, trials: u32) -> CheckResult {
41    let spec_id = spec_id(spec);
42    let prog = match parse_source(lex_source) {
43        Ok(p) => p,
44        Err(e) => return inconclusive(spec_id, format!("parse: {e}")),
45    };
46    let stages = canonicalize_program(&prog);
47    if let Err(errs) = lex_types::check_program(&stages) {
48        return inconclusive(spec_id, format!("typecheck: {errs:?}"));
49    }
50    let bc = compile_program(&stages);
51
52    // Skip Float-only specs in the randomized strategy: float spaces are
53    // huge and counterexamples don't generalize. Report inconclusive
54    // honestly per spec §14.5.
55    if spec.quantifiers.iter().any(|q| q.ty == SpecType::Float) {
56        return CheckResult {
57            spec_id,
58            status: ProofStatus::Inconclusive,
59            evidence: Evidence {
60                method: "randomized".into(),
61                trials: 0,
62                counterexample: None,
63                note: Some("randomized search inconclusive on Float quantifiers; use SMT (see to_smtlib)".into()),
64            },
65        };
66    }
67
68    let mut rng = DetRng::new(seed_from_spec(spec));
69    let policy = Policy::permissive();
70
71    for trial in 0..trials {
72        let mut bindings = IndexMap::new();
73        let mut skip = false;
74        for q in &spec.quantifiers {
75            let v = sample(&q.ty, &mut rng);
76            bindings.insert(q.name.clone(), v);
77            // Apply per-quantifier constraint.
78            if let Some(c) = &q.constraint {
79                match eval(c, &bindings, &bc, &policy) {
80                    Ok(Value::Bool(true)) => {}
81                    Ok(Value::Bool(false)) => { skip = true; break; }
82                    Ok(_) => return inconclusive(spec_id, format!("constraint did not return Bool (trial {trial})")),
83                    Err(e) => return inconclusive(spec_id, format!("constraint eval failed: {e}")),
84                }
85            }
86        }
87        if skip { continue; }
88
89        match eval(&spec.body, &bindings, &bc, &policy) {
90            Ok(Value::Bool(true)) => continue,
91            Ok(Value::Bool(false)) => {
92                return CheckResult {
93                    spec_id,
94                    status: ProofStatus::Counterexample,
95                    evidence: Evidence {
96                        method: "randomized".into(),
97                        trials: trial + 1,
98                        counterexample: Some(bindings_to_json(&bindings)),
99                        note: None,
100                    },
101                };
102            }
103            Ok(other) => return inconclusive(spec_id, format!("body returned non-bool: {other:?}")),
104            Err(e) => return inconclusive(spec_id, format!("body eval failed: {e}")),
105        }
106    }
107
108    CheckResult {
109        spec_id,
110        status: ProofStatus::Proved,
111        evidence: Evidence {
112            method: "randomized".into(),
113            trials,
114            counterexample: None,
115            note: Some(format!("survived {trials} random trials; not a deductive proof")),
116        },
117    }
118}
119
120fn inconclusive(spec_id: String, note: impl Into<String>) -> CheckResult {
121    CheckResult {
122        spec_id,
123        status: ProofStatus::Inconclusive,
124        evidence: Evidence {
125            method: "randomized".into(),
126            trials: 0,
127            counterexample: None,
128            note: Some(note.into()),
129        },
130    }
131}
132
133fn spec_id(spec: &Spec) -> String {
134    use sha2::{Digest, Sha256};
135    let v = serde_json::to_value(spec).unwrap();
136    let s = lex_ast::canon_json::to_canonical_string(&v);
137    let mut h = Sha256::new();
138    h.update(s.as_bytes());
139    let r = h.finalize();
140    let mut hex = String::with_capacity(64);
141    for b in r { hex.push_str(&format!("{:02x}", b)); }
142    hex
143}
144
145fn seed_from_spec(spec: &Spec) -> u64 {
146    use sha2::{Digest, Sha256};
147    let mut h = Sha256::new();
148    h.update(spec.name.as_bytes());
149    let r = h.finalize();
150    u64::from_le_bytes(r[..8].try_into().unwrap())
151}
152
153/// Tiny deterministic xorshift RNG, no external dep.
154struct DetRng { state: u64 }
155impl DetRng {
156    fn new(seed: u64) -> Self { Self { state: seed.max(1) } }
157    fn next_u64(&mut self) -> u64 {
158        let mut x = self.state;
159        x ^= x << 13;
160        x ^= x >> 7;
161        x ^= x << 17;
162        self.state = x;
163        x
164    }
165    fn next_i64_in(&mut self, lo: i64, hi: i64) -> i64 {
166        if hi <= lo { return lo; }
167        let span = (hi - lo) as u64;
168        lo + (self.next_u64() % span) as i64
169    }
170}
171
172fn sample(ty: &SpecType, rng: &mut DetRng) -> Value {
173    match ty {
174        SpecType::Int => Value::Int(rng.next_i64_in(-1000, 1001)),
175        SpecType::Float => {
176            let n = rng.next_u64() as f64;
177            Value::Float((n / u64::MAX as f64) * 2000.0 - 1000.0)
178        }
179        SpecType::Bool => Value::Bool(rng.next_u64() & 1 == 0),
180        SpecType::Str => {
181            let n = rng.next_u64() % 6;
182            Value::Str(("ab".repeat(n as usize)).chars().take(n as usize).collect())
183        }
184    }
185}
186
187fn eval(
188    e: &SpecExpr,
189    bindings: &IndexMap<String, Value>,
190    bc: &lex_bytecode::Program,
191    policy: &Policy,
192) -> Result<Value, String> {
193    match e {
194        SpecExpr::IntLit { value } => Ok(Value::Int(*value)),
195        SpecExpr::FloatLit { value } => Ok(Value::Float(*value)),
196        SpecExpr::BoolLit { value } => Ok(Value::Bool(*value)),
197        SpecExpr::StrLit { value } => Ok(Value::Str(value.clone())),
198        SpecExpr::Var { name } => bindings.get(name).cloned()
199            .ok_or_else(|| format!("unbound spec var `{name}`")),
200        SpecExpr::Let { name, value, body } => {
201            let v = eval(value, bindings, bc, policy)?;
202            let mut next = bindings.clone();
203            next.insert(name.clone(), v);
204            eval(body, &next, bc, policy)
205        }
206        SpecExpr::Not { expr } => match eval(expr, bindings, bc, policy)? {
207            Value::Bool(b) => Ok(Value::Bool(!b)),
208            other => Err(format!("not on non-bool: {other:?}")),
209        },
210        SpecExpr::BinOp { op, lhs, rhs } => {
211            let a = eval(lhs, bindings, bc, policy)?;
212            let b = eval(rhs, bindings, bc, policy)?;
213            apply_binop(*op, a, b)
214        }
215        SpecExpr::Call { func, args } => {
216            // Materialize args.
217            let mut argv = Vec::new();
218            for a in args { argv.push(eval(a, bindings, bc, policy)?); }
219            // Run the Lex function with a fresh VM (cheap: program is shared).
220            let handler = DefaultHandler::new(policy.clone());
221            let mut vm = Vm::with_handler(bc, Box::new(handler));
222            vm.call(func, argv).map_err(|e| format!("call `{func}`: {e}"))
223        }
224    }
225}
226
227fn apply_binop(op: SpecOp, a: Value, b: Value) -> Result<Value, String> {
228    use SpecOp::*;
229    match (op, &a, &b) {
230        (Add, Value::Int(x), Value::Int(y)) => Ok(Value::Int(x + y)),
231        (Sub, Value::Int(x), Value::Int(y)) => Ok(Value::Int(x - y)),
232        (Mul, Value::Int(x), Value::Int(y)) => Ok(Value::Int(x * y)),
233        (Div, Value::Int(x), Value::Int(y)) if *y != 0 => Ok(Value::Int(x / y)),
234        (Mod, Value::Int(x), Value::Int(y)) if *y != 0 => Ok(Value::Int(x % y)),
235        (Add, Value::Float(x), Value::Float(y)) => Ok(Value::Float(x + y)),
236        (Sub, Value::Float(x), Value::Float(y)) => Ok(Value::Float(x - y)),
237        (Mul, Value::Float(x), Value::Float(y)) => Ok(Value::Float(x * y)),
238        (Div, Value::Float(x), Value::Float(y)) => Ok(Value::Float(x / y)),
239        (Eq, x, y) => Ok(Value::Bool(x == y)),
240        (Neq, x, y) => Ok(Value::Bool(x != y)),
241        (Lt, Value::Int(x), Value::Int(y)) => Ok(Value::Bool(x < y)),
242        (Le, Value::Int(x), Value::Int(y)) => Ok(Value::Bool(x <= y)),
243        (Gt, Value::Int(x), Value::Int(y)) => Ok(Value::Bool(x > y)),
244        (Ge, Value::Int(x), Value::Int(y)) => Ok(Value::Bool(x >= y)),
245        (Lt, Value::Float(x), Value::Float(y)) => Ok(Value::Bool(x < y)),
246        (Le, Value::Float(x), Value::Float(y)) => Ok(Value::Bool(x <= y)),
247        (Gt, Value::Float(x), Value::Float(y)) => Ok(Value::Bool(x > y)),
248        (Ge, Value::Float(x), Value::Float(y)) => Ok(Value::Bool(x >= y)),
249        (And, Value::Bool(x), Value::Bool(y)) => Ok(Value::Bool(*x && *y)),
250        (Or, Value::Bool(x), Value::Bool(y)) => Ok(Value::Bool(*x || *y)),
251        _ => Err(format!("invalid binop {op:?} on {a:?}, {b:?}")),
252    }
253}
254
255fn bindings_to_json(b: &IndexMap<String, Value>) -> IndexMap<String, serde_json::Value> {
256    let mut out = IndexMap::new();
257    for (k, v) in b { out.insert(k.clone(), value_to_json(v)); }
258    out
259}
260
261fn value_to_json(v: &Value) -> serde_json::Value { v.to_json() }
spec_checker/checker.rs

spec_checker/
checker.rs
