aver/checker/
mod.rs

1mod coverage;
2mod cse;
3mod independence;
4mod intent;
5#[cfg(feature = "runtime")]
6mod law;
7mod module_effects;
8mod naming;
9mod perf;
10mod traversal;
11mod verify;
12mod verify_effects;
13
14use crate::ast::{
15    Expr, Literal, Pattern, SourceSpan, Spanned, TopLevel, TypeDef, VerifyBlock, VerifyKind,
16};
17
18// -- Structured verify results ------------------------------------------------
19
20#[derive(Debug, Clone)]
21pub enum VerifyCaseOutcome {
22    Pass,
23    Skipped,
24    /// Hostile-profile case for a `case_expr` whose un-effected base
25    /// case already failed. Aver doesn't run the VM for these — the
26    /// counter-example is the base failure itself; the per-profile
27    /// follow-ups would only re-confirm the same case under harder
28    /// worlds. Distinct from `Skipped` (which is `when`-driven and
29    /// drives the vacuous-under-hostile warning).
30    SkippedAfterBaseFail,
31    Mismatch {
32        expected: String,
33        actual: String,
34    },
35    RuntimeError {
36        error: String,
37    },
38    UnexpectedErr {
39        err_repr: String,
40    },
41}
42
43#[derive(Debug, Clone)]
44pub struct VerifyCaseResult {
45    pub outcome: VerifyCaseOutcome,
46    pub span: Option<SourceSpan>,
47    pub case_expr: String,
48    pub case_index: usize,
49    pub case_total: usize,
50    pub law_context: Option<VerifyLawContext>,
51    /// `true` for cases injected by `aver verify --hostile` boundary
52    /// expansion (a binding the user did not declare). Drives differential
53    /// reporting: a hostile-only failure means the claim is not universal,
54    /// so it isn't a law — either encode the missing precondition with
55    /// `when`, or downgrade from `law` form to `verify` (cases form,
56    /// example/scenario semantics) with the values you actually meant.
57    pub from_hostile: bool,
58    /// Display label for the effect-side hostile profile, e.g.
59    /// `"Time.now/frozen + Random.int/min"`. `None` when the case wasn't
60    /// effect-hostile-expanded (declared, value-hostile-only, or fns
61    /// without applicable classified effects). Reporting prepends this to
62    /// the diagnostic so the user sees which adversarial world broke the
63    /// law: "Time.now/frozen + Random.int/min: assumed deadline > now".
64    pub hostile_profile: Option<String>,
65}
66
67#[derive(Debug, Clone)]
68pub struct VerifyLawContext {
69    pub givens: Vec<(String, String)>, // (name, value_repr)
70    pub law_expr: String,
71}
72
73pub struct VerifyResult {
74    pub fn_name: String,
75    pub block_label: String, // "add" or "sort spec isSorted"
76    pub passed: usize,
77    pub failed: usize,
78    pub skipped: usize,
79    pub case_results: Vec<VerifyCaseResult>,
80    // Legacy field — kept temporarily for existing consumers
81    pub failures: Vec<(String, String, String)>, // (expr_src, expected, actual)
82}
83
84pub struct ModuleCheckFindings {
85    pub errors: Vec<CheckFinding>,
86    pub warnings: Vec<CheckFinding>,
87}
88
89pub(crate) type FnSigSummary = (Vec<crate::types::Type>, crate::types::Type, Vec<String>);
90pub(crate) type FnSigMap = std::collections::HashMap<String, FnSigSummary>;
91
92#[derive(Debug, Clone, PartialEq, Eq)]
93pub struct FindingSpan {
94    pub line: usize,
95    pub col: usize,
96    pub len: usize,
97    pub label: String,
98}
99
100#[derive(Debug, Clone, PartialEq, Eq)]
101pub struct CheckFinding {
102    pub line: usize,
103    pub module: Option<String>,
104    pub file: Option<String>,
105    pub fn_name: Option<String>,
106    pub message: String,
107    pub extra_spans: Vec<FindingSpan>,
108}
109
110fn module_name_for_items(items: &[TopLevel]) -> Option<String> {
111    items.iter().find_map(|item| {
112        if let TopLevel::Module(m) = item {
113            Some(m.name.clone())
114        } else {
115            None
116        }
117    })
118}
119
120fn dotted_name(expr: &Spanned<Expr>) -> Option<String> {
121    match &expr.node {
122        Expr::Ident(name) => Some(name.clone()),
123        Expr::Attr(base, field) => {
124            let mut prefix = dotted_name(base)?;
125            prefix.push('.');
126            prefix.push_str(field);
127            Some(prefix)
128        }
129        _ => None,
130    }
131}
132
133fn normalize_constructor_tag(path: &str) -> Option<String> {
134    let mut parts = path.split('.').collect::<Vec<_>>();
135    if parts.len() < 2 {
136        return None;
137    }
138    let variant = parts.pop()?;
139    let type_name = parts.pop()?;
140    Some(crate::visibility::member_key(type_name, variant))
141}
142
143fn constructor_tag_from_pattern(pattern: &Pattern) -> Option<String> {
144    match pattern {
145        Pattern::Constructor(path, _) => normalize_constructor_tag(path),
146        _ => None,
147    }
148}
149
150fn constructor_tag_from_expr(expr: &Spanned<Expr>) -> Option<String> {
151    match &expr.node {
152        Expr::Attr(_, _) => normalize_constructor_tag(&dotted_name(expr)?),
153        Expr::FnCall(callee, _) => normalize_constructor_tag(&dotted_name(callee)?),
154        Expr::Constructor(name, _) => normalize_constructor_tag(name),
155        _ => None,
156    }
157}
158
159fn expr_is_result_err_case(expr: &Spanned<Expr>) -> bool {
160    match &expr.node {
161        Expr::FnCall(callee, _) => dotted_name(callee)
162            .and_then(|path| normalize_constructor_tag(&path))
163            .is_some_and(|tag| tag == "Result.Err"),
164        Expr::Constructor(name, _) => {
165            normalize_constructor_tag(name).is_some_and(|tag| tag == "Result.Err")
166        }
167        _ => false,
168    }
169}
170
171fn expr_is_result_ok_case(expr: &Spanned<Expr>) -> bool {
172    match &expr.node {
173        Expr::FnCall(callee, _) => dotted_name(callee)
174            .and_then(|path| normalize_constructor_tag(&path))
175            .is_some_and(|tag| tag == "Result.Ok"),
176        Expr::Constructor(name, _) => {
177            normalize_constructor_tag(name).is_some_and(|tag| tag == "Result.Ok")
178        }
179        _ => false,
180    }
181}
182
183fn expr_is_option_none_case(expr: &Spanned<Expr>) -> bool {
184    match &expr.node {
185        Expr::Attr(_, _) => dotted_name(expr)
186            .and_then(|path| normalize_constructor_tag(&path))
187            .is_some_and(|tag| tag == "Option.None"),
188        Expr::Constructor(name, None) => {
189            normalize_constructor_tag(name).is_some_and(|tag| tag == "Option.None")
190        }
191        _ => false,
192    }
193}
194
195fn expr_is_option_some_case(expr: &Spanned<Expr>) -> bool {
196    match &expr.node {
197        Expr::FnCall(callee, _) => dotted_name(callee)
198            .and_then(|path| normalize_constructor_tag(&path))
199            .is_some_and(|tag| tag == "Option.Some"),
200        Expr::Constructor(name, _) => {
201            normalize_constructor_tag(name).is_some_and(|tag| tag == "Option.Some")
202        }
203        _ => false,
204    }
205}
206
207fn expr_is_bool_case(expr: &Spanned<Expr>, expected: bool) -> bool {
208    matches!(&expr.node, Expr::Literal(Literal::Bool(value)) if *value == expected)
209}
210
211fn expr_is_empty_list_case(expr: &Spanned<Expr>) -> bool {
212    matches!(&expr.node, Expr::List(items) if items.is_empty())
213}
214
215fn expr_is_non_empty_list_case(expr: &Spanned<Expr>) -> bool {
216    matches!(&expr.node, Expr::List(items) if !items.is_empty())
217}
218
219fn expr_is_empty_string_case(expr: &Spanned<Expr>) -> bool {
220    matches!(&expr.node, Expr::Literal(Literal::Str(value)) if value.is_empty())
221}
222
223fn expr_is_int_literal_case(expr: &Spanned<Expr>, expected: i64) -> bool {
224    matches!(&expr.node, Expr::Literal(Literal::Int(value)) if *value == expected)
225}
226
227fn verify_cases_block_is_well_formed(block: &VerifyBlock) -> bool {
228    matches!(block.kind, VerifyKind::Cases)
229        && !block.cases.is_empty()
230        && block.cases.iter().all(|(left, right)| {
231            verify_case_calls_target(left, &block.fn_name)
232                && !verify_case_calls_target(right, &block.fn_name)
233        })
234}
235
236fn local_sum_type_constructors(items: &[TopLevel], type_name: &str) -> Option<Vec<String>> {
237    items.iter().find_map(|item| match item {
238        TopLevel::TypeDef(TypeDef::Sum { name, variants, .. }) if name == type_name => Some(
239            variants
240                .iter()
241                .map(|variant| crate::visibility::member_key(name, &variant.name))
242                .collect(),
243        ),
244        _ => None,
245    })
246}
247
248fn callee_is_target(callee: &Spanned<Expr>, fn_name: &str) -> bool {
249    matches!(&callee.node, Expr::Ident(name) if name == fn_name)
250}
251
252// Re-export from verify submodule
253use verify::collect_target_call_args;
254use verify::verify_case_calls_target;
255
256// Public re-exports so external callers don't break
257pub use coverage::{collect_verify_coverage_warnings, collect_verify_coverage_warnings_in};
258pub use cse::{collect_cse_warnings, collect_cse_warnings_in};
259pub use independence::{collect_independence_warnings, collect_independence_warnings_in};
260pub use intent::{
261    check_module_intent, check_module_intent_with_sigs, check_module_intent_with_sigs_in,
262    index_decisions,
263};
264#[cfg(feature = "runtime")]
265pub use law::{collect_verify_law_dependency_warnings, collect_verify_law_dependency_warnings_in};
266pub use module_effects::{collect_module_effects_warnings, collect_module_effects_warnings_in};
267pub use naming::{collect_naming_warnings, collect_naming_warnings_in};
268pub use perf::{collect_perf_warnings, collect_perf_warnings_in};
269pub use traversal::collect_traversal_warnings_in;
270pub use verify::{expr_to_str, merge_verify_blocks};
271pub use verify_effects::{
272    collect_plain_cases_effectful_warnings, collect_plain_cases_effectful_warnings_in,
273};
aver/checker/mod.rs

aver/checker/
mod.rs
