aver/
checker.rs

1use colored::Colorize;
2
3use crate::ast::{DecisionBlock, Expr, FnBody, FnDef, Stmt, TopLevel, VerifyBlock};
4use crate::interpreter::{Interpreter, aver_repr};
5use crate::value::RuntimeError;
6
7pub struct VerifyResult {
8    #[allow(dead_code)]
9    pub fn_name: String,
10    pub passed: usize,
11    pub failed: usize,
12    #[allow(dead_code)]
13    pub failures: Vec<(String, String, String)>, // (expr_src, expected, actual)
14}
15
16pub struct ModuleCheckFindings {
17    pub errors: Vec<String>,
18    pub warnings: Vec<String>,
19}
20
21pub fn run_verify(block: &VerifyBlock, interp: &mut Interpreter) -> VerifyResult {
22    let mut passed = 0;
23    let mut failed = 0;
24    let mut failures = Vec::new();
25
26    println!("Verify: {}", block.fn_name.cyan());
27
28    for (left_expr, right_expr) in &block.cases {
29        let case_str = format!("{} == {}", expr_to_str(left_expr), expr_to_str(right_expr));
30
31        let left_result = interp.eval_expr(left_expr);
32        let right_result = interp.eval_expr(right_expr);
33
34        match (left_result, right_result) {
35            (Ok(left_val), Ok(right_val)) => {
36                if interp.aver_eq(&left_val, &right_val) {
37                    passed += 1;
38                    println!("  {} {}", "✓".green(), case_str);
39                } else {
40                    failed += 1;
41                    println!("  {} {}", "✗".red(), case_str);
42                    let expected = aver_repr(&right_val);
43                    let actual = aver_repr(&left_val);
44                    println!("      expected: {}", expected);
45                    println!("      got:      {}", actual);
46                    failures.push((case_str, expected, actual));
47                }
48            }
49            // `?` in a verify case hitting Err produces ErrProp — treat as test failure.
50            (Err(RuntimeError::ErrProp(err_val)), _) | (_, Err(RuntimeError::ErrProp(err_val))) => {
51                failed += 1;
52                println!("  {} {}", "✗".red(), case_str);
53                println!("      ? hit Result.Err({})", aver_repr(&err_val));
54                failures.push((
55                    case_str,
56                    String::new(),
57                    format!("? hit Result.Err({})", aver_repr(&err_val)),
58                ));
59            }
60            (Err(e), _) | (_, Err(e)) => {
61                failed += 1;
62                println!("  {} {}", "✗".red(), case_str);
63                println!("      error: {}", e);
64                failures.push((case_str, String::new(), format!("ERROR: {}", e)));
65            }
66        }
67    }
68
69    let total = passed + failed;
70    if failed == 0 {
71        println!("  {}", format!("{}/{} passed", passed, total).green());
72    } else {
73        println!("  {}", format!("{}/{} passed", passed, total).red());
74    }
75
76    VerifyResult {
77        fn_name: block.fn_name.clone(),
78        passed,
79        failed,
80        failures,
81    }
82}
83
84pub fn index_decisions(items: &[TopLevel]) -> Vec<&DecisionBlock> {
85    items
86        .iter()
87        .filter_map(|item| {
88            if let TopLevel::Decision(d) = item {
89                Some(d)
90            } else {
91                None
92            }
93        })
94        .collect()
95}
96
97/// Returns true if a function requires a ? description annotation.
98/// All functions except main() require one.
99fn fn_needs_desc(f: &FnDef) -> bool {
100    f.name != "main"
101}
102
103/// Missing verify warning policy:
104/// - skip `main`
105/// - skip effectful functions (tested through replay/recording flow)
106/// - skip trivial pure pass-through wrappers
107/// - require verify for the rest (pure, non-trivial logic)
108fn fn_needs_verify(f: &FnDef) -> bool {
109    if f.name == "main" {
110        return false;
111    }
112    if !f.effects.is_empty() {
113        return false;
114    }
115    !is_trivial_passthrough_wrapper(f)
116}
117
118fn is_trivial_passthrough_wrapper(f: &FnDef) -> bool {
119    let param_names: Vec<&str> = f.params.iter().map(|(name, _)| name.as_str()).collect();
120
121    match f.body.as_ref() {
122        FnBody::Expr(expr) => expr_is_passthrough(expr, &param_names),
123        FnBody::Block(stmts) => {
124            if stmts.len() != 1 {
125                return false;
126            }
127            match &stmts[0] {
128                Stmt::Expr(expr) => expr_is_passthrough(expr, &param_names),
129                Stmt::Binding(_, _, _) => false,
130            }
131        }
132    }
133}
134
135fn expr_is_passthrough(expr: &Expr, param_names: &[&str]) -> bool {
136    match expr {
137        // `fn id(x) = x`
138        Expr::Ident(name) => param_names.len() == 1 && name == param_names[0],
139        // `fn wrap(a,b) = inner(a,b)` (no argument transformation)
140        Expr::FnCall(_, args) => args_match_params(args, param_names),
141        // `fn some(x) = Option.Some(x)` style
142        Expr::Constructor(_, Some(arg)) => {
143            if param_names.len() != 1 {
144                return false;
145            }
146            matches!(arg.as_ref(), Expr::Ident(name) if name == param_names[0])
147        }
148        _ => false,
149    }
150}
151
152fn args_match_params(args: &[Expr], param_names: &[&str]) -> bool {
153    if args.len() != param_names.len() {
154        return false;
155    }
156    args.iter()
157        .zip(param_names.iter())
158        .all(|(arg, expected)| matches!(arg, Expr::Ident(name) if name == *expected))
159}
160
161pub fn check_module_intent(items: &[TopLevel]) -> ModuleCheckFindings {
162    let mut errors = Vec::new();
163    let mut warnings = Vec::new();
164
165    let verified_fns: std::collections::HashSet<&str> = items
166        .iter()
167        .filter_map(|item| {
168            if let TopLevel::Verify(v) = item {
169                Some(v.fn_name.as_str())
170            } else {
171                None
172            }
173        })
174        .collect();
175
176    for item in items {
177        match item {
178            TopLevel::Module(m) => {
179                if m.intent.is_empty() {
180                    warnings.push(format!("Module '{}' has no intent block", m.name));
181                }
182            }
183            TopLevel::FnDef(f) => {
184                if f.desc.is_none() && fn_needs_desc(f) {
185                    warnings.push(format!("Function '{}' has no description (?)", f.name));
186                }
187                if fn_needs_verify(f) && !verified_fns.contains(f.name.as_str()) {
188                    errors.push(format!("Function '{}' has no verify block", f.name));
189                }
190            }
191            _ => {}
192        }
193    }
194
195    ModuleCheckFindings { errors, warnings }
196}
197
198#[cfg(test)]
199mod tests {
200    use super::*;
201    use crate::lexer::Lexer;
202    use crate::parser::Parser;
203
204    fn parse_items(src: &str) -> Vec<TopLevel> {
205        let mut lexer = Lexer::new(src);
206        let tokens = lexer.tokenize().expect("lex failed");
207        let mut parser = Parser::new(tokens);
208        parser.parse().expect("parse failed")
209    }
210
211    #[test]
212    fn no_verify_warning_for_effectful_function() {
213        let items = parse_items(
214            r#"
215fn log(x: Int) -> Unit
216    ! [Console]
217    = Console.print(x)
218"#,
219        );
220        let findings = check_module_intent(&items);
221        assert!(
222            !findings
223                .warnings
224                .iter()
225                .any(|w| w.contains("no verify block"))
226                && !findings
227                    .errors
228                    .iter()
229                    .any(|e| e.contains("no verify block")),
230            "unexpected findings: errors={:?}, warnings={:?}",
231            findings.errors,
232            findings.warnings
233        );
234    }
235
236    #[test]
237    fn no_verify_warning_for_trivial_passthrough_wrapper() {
238        let items = parse_items(
239            r#"
240fn passthrough(x: Int) -> Int
241    = inner(x)
242"#,
243        );
244        let findings = check_module_intent(&items);
245        assert!(
246            !findings
247                .warnings
248                .iter()
249                .any(|w| w.contains("no verify block"))
250                && !findings
251                    .errors
252                    .iter()
253                    .any(|e| e.contains("no verify block")),
254            "unexpected findings: errors={:?}, warnings={:?}",
255            findings.errors,
256            findings.warnings
257        );
258    }
259
260    #[test]
261    fn verify_error_for_pure_non_trivial_logic() {
262        let items = parse_items(
263            r#"
264fn add1(x: Int) -> Int
265    = x + 1
266"#,
267        );
268        let findings = check_module_intent(&items);
269        assert!(
270            findings
271                .errors
272                .iter()
273                .any(|e| e == "Function 'add1' has no verify block"),
274            "expected verify error, got errors={:?}, warnings={:?}",
275            findings.errors,
276            findings.warnings
277        );
278    }
279}
280
281pub fn expr_to_str(expr: &crate::ast::Expr) -> String {
282    use crate::ast::Expr;
283    use crate::ast::Literal;
284
285    match expr {
286        Expr::Literal(lit) => match lit {
287            Literal::Int(i) => i.to_string(),
288            Literal::Float(f) => f.to_string(),
289            Literal::Str(s) => format!("\"{}\"", s),
290            Literal::Bool(b) => if *b { "true" } else { "false" }.to_string(),
291        },
292        Expr::Ident(name) => name.clone(),
293        Expr::FnCall(fn_expr, args) => {
294            let fn_str = expr_to_str(fn_expr);
295            let args_str = args.iter().map(expr_to_str).collect::<Vec<_>>().join(", ");
296            format!("{}({})", fn_str, args_str)
297        }
298        Expr::Constructor(name, arg) => match arg {
299            None => name.clone(),
300            Some(a) => format!("{}({})", name, expr_to_str(a)),
301        },
302        Expr::BinOp(op, left, right) => {
303            use crate::ast::BinOp;
304            let op_str = match op {
305                BinOp::Add => "+",
306                BinOp::Sub => "-",
307                BinOp::Mul => "*",
308                BinOp::Div => "/",
309                BinOp::Eq => "==",
310                BinOp::Neq => "!=",
311                BinOp::Lt => "<",
312                BinOp::Gt => ">",
313                BinOp::Lte => "<=",
314                BinOp::Gte => ">=",
315            };
316            format!("{} {} {}", expr_to_str(left), op_str, expr_to_str(right))
317        }
318        Expr::InterpolatedStr(parts) => {
319            use crate::ast::StrPart;
320            let mut inner = String::new();
321            for part in parts {
322                match part {
323                    StrPart::Literal(s) => inner.push_str(s),
324                    StrPart::Parsed(e) => {
325                        inner.push('{');
326                        inner.push_str(&expr_to_str(e));
327                        inner.push('}');
328                    }
329                }
330            }
331            format!("\"{}\"", inner)
332        }
333        Expr::List(elements) => {
334            let parts: Vec<String> = elements.iter().map(expr_to_str).collect();
335            format!("[{}]", parts.join(", "))
336        }
337        Expr::Tuple(items) => {
338            let parts: Vec<String> = items.iter().map(expr_to_str).collect();
339            format!("({})", parts.join(", "))
340        }
341        Expr::MapLiteral(entries) => {
342            let parts = entries
343                .iter()
344                .map(|(key, value)| format!("{} => {}", expr_to_str(key), expr_to_str(value)))
345                .collect::<Vec<_>>();
346            format!("{{{}}}", parts.join(", "))
347        }
348        Expr::ErrorProp(inner) => format!("{}?", expr_to_str(inner)),
349        Expr::Attr(obj, field) => format!("{}.{}", expr_to_str(obj), field),
350        Expr::Pipe(left, right) => format!("{} |> {}", expr_to_str(left), expr_to_str(right)),
351        Expr::RecordCreate { type_name, fields } => {
352            let flds: Vec<String> = fields
353                .iter()
354                .map(|(name, expr)| format!("{} = {}", name, expr_to_str(expr)))
355                .collect();
356            format!("{}({})", type_name, flds.join(", "))
357        }
358        Expr::RecordUpdate {
359            type_name,
360            base,
361            updates,
362        } => {
363            let upds: Vec<String> = updates
364                .iter()
365                .map(|(name, expr)| format!("{} = {}", name, expr_to_str(expr)))
366                .collect();
367            format!(
368                "{}.update({}, {})",
369                type_name,
370                expr_to_str(base),
371                upds.join(", ")
372            )
373        }
374        Expr::TailCall(boxed) => {
375            let (target, args) = boxed.as_ref();
376            let a = args.iter().map(expr_to_str).collect::<Vec<_>>().join(", ");
377            format!("<tail-call:{}>({})", target, a)
378        }
379        Expr::Resolved(_) => "<resolved>".to_string(),
380        Expr::Match { subject, arms, .. } => {
381            let s = expr_to_str(subject);
382            let arms_str: Vec<String> = arms
383                .iter()
384                .map(|arm| format!("{:?} -> {}", arm.pattern, expr_to_str(&arm.body)))
385                .collect();
386            format!("match {} {}", s, arms_str.join(", "))
387        }
388    }
389}
aver/checker.rs

aver/
checker.rs
