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

aver/checker/
mod.rs
