aver/diagnostics/
why.rs

1//! File-local "why" summary: per-function justification signals plus
2//! aggregate line counts. Shared by CLI `aver why` and the playground
3//! Why panel — single analysis, two renderers.
4//!
5//! Runtime-neutral: walks parsed items without touching the VM or the
6//! filesystem.
7
8use std::collections::{HashMap, HashSet};
9
10use serde::Serialize;
11
12use crate::ast::{DecisionBlock, FnDef, TopLevel};
13use crate::checker::{collect_verify_coverage_warnings, merge_verify_blocks};
14
15#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)]
16#[serde(rename_all = "lowercase")]
17pub enum Justification {
18    /// Description + verify (or description alone for effectful fns), no
19    /// coverage gaps.
20    Justified,
21    /// At least one signal present but incomplete.
22    Partial,
23    /// No description, no verify, no decision impact.
24    Unjustified,
25}
26
27impl Justification {
28    pub fn priority(self) -> u8 {
29        match self {
30            Justification::Unjustified => 0,
31            Justification::Partial => 1,
32            Justification::Justified => 2,
33        }
34    }
35}
36
37#[derive(Clone, Debug, Serialize)]
38pub struct FnDetail {
39    pub name: String,
40    pub lines: usize,
41    pub has_description: bool,
42    pub is_effectful: bool,
43    pub verify_cases: usize,
44    pub has_coverage_gaps: bool,
45    pub has_decision_impact: bool,
46    pub level: Justification,
47    pub missing: Vec<&'static str>,
48}
49
50impl FnDetail {
51    fn compute_level(
52        has_description: bool,
53        is_effectful: bool,
54        verify_cases: usize,
55        has_coverage_gaps: bool,
56        has_decision_impact: bool,
57    ) -> Justification {
58        let has_verify = verify_cases > 0;
59        if is_effectful {
60            if has_description {
61                return Justification::Justified;
62            }
63        } else if has_description && has_verify && !has_coverage_gaps {
64            return Justification::Justified;
65        }
66        if has_description || has_verify || has_decision_impact {
67            Justification::Partial
68        } else {
69            Justification::Unjustified
70        }
71    }
72
73    fn compute_missing(
74        has_description: bool,
75        is_effectful: bool,
76        verify_cases: usize,
77        has_coverage_gaps: bool,
78    ) -> Vec<&'static str> {
79        let mut missing = Vec::new();
80        if !has_description {
81            missing.push("no description");
82        }
83        if is_effectful {
84            if !has_description {
85                missing.push("effectful — verify with Oracle or replay");
86            }
87        } else if verify_cases == 0 {
88            missing.push("no verify");
89        } else if has_coverage_gaps {
90            missing.push("verify has gaps");
91        }
92        missing
93    }
94}
95
96#[derive(Clone, Debug, Serialize)]
97pub struct DecisionSummary {
98    pub name: String,
99    pub date: String,
100    pub reason_prefix: String,
101}
102
103#[derive(Clone, Debug, Serialize)]
104pub struct WhySummary {
105    pub file_label: String,
106    pub total_lines: usize,
107    pub justified_lines: usize,
108    pub partial_lines: usize,
109    pub unjustified_lines: usize,
110    pub has_module_intent: bool,
111    pub decisions: Vec<DecisionSummary>,
112    pub functions: Vec<FnDetail>,
113}
114
115/// Compute the why summary for a single parsed file. Pure function.
116pub fn summarize(items: &[TopLevel], source: &str, file_label: impl Into<String>) -> WhySummary {
117    let total_lines = source.lines().count();
118
119    let decisions: Vec<&DecisionBlock> = items
120        .iter()
121        .filter_map(|item| match item {
122            TopLevel::Decision(d) => Some(d),
123            _ => None,
124        })
125        .collect();
126
127    let impact_symbols: HashSet<String> = decisions
128        .iter()
129        .flat_map(|d| d.impacts.iter().map(|i| i.node.text().to_string()))
130        .collect();
131
132    let merged_verify = merge_verify_blocks(items);
133    let mut verify_cases_per_fn: HashMap<String, usize> = HashMap::new();
134    for vb in &merged_verify {
135        *verify_cases_per_fn.entry(vb.fn_name.clone()).or_default() += vb.cases.len();
136    }
137
138    let coverage_warnings = collect_verify_coverage_warnings(items);
139    let fns_with_coverage_gaps: HashSet<String> = coverage_warnings
140        .iter()
141        .filter_map(|w| {
142            w.message
143                .strip_prefix("verify examples for ")
144                .or_else(|| {
145                    w.message
146                        .strip_prefix("verify examples for recursive function ")
147                })
148                .and_then(|rest| rest.split_whitespace().next())
149                .map(|s| s.to_string())
150        })
151        .collect();
152
153    let has_module_intent = items
154        .iter()
155        .any(|item| matches!(item, TopLevel::Module(m) if !m.intent.is_empty()));
156
157    let fns: Vec<&FnDef> = items
158        .iter()
159        .filter_map(|item| match item {
160            TopLevel::FnDef(fd) => Some(fd),
161            _ => None,
162        })
163        .collect();
164
165    let mut functions = Vec::new();
166    let mut justified_lines = 0usize;
167    let mut partial_lines = 0usize;
168    let mut unjustified_lines = 0usize;
169
170    for (i, fd) in fns.iter().enumerate() {
171        let fn_start = fd.line;
172        let fn_end = if i + 1 < fns.len() {
173            fns[i + 1].line.saturating_sub(1)
174        } else {
175            next_toplevel_line_after(items, fd.line).unwrap_or(total_lines)
176        };
177        let fn_lines = fn_end.saturating_sub(fn_start).max(1);
178
179        let has_decision_impact = impact_symbols.contains(&fd.name)
180            || impact_symbols
181                .iter()
182                .any(|s: &String| fd.name.starts_with(s.as_str()));
183
184        let verify_cases = verify_cases_per_fn.get(&fd.name).copied().unwrap_or(0);
185        let has_description = fd.desc.is_some();
186        let is_effectful = !fd.effects.is_empty();
187        let has_coverage_gaps = fns_with_coverage_gaps.contains(&fd.name);
188
189        let level = FnDetail::compute_level(
190            has_description,
191            is_effectful,
192            verify_cases,
193            has_coverage_gaps,
194            has_decision_impact,
195        );
196        let missing = FnDetail::compute_missing(
197            has_description,
198            is_effectful,
199            verify_cases,
200            has_coverage_gaps,
201        );
202
203        match level {
204            Justification::Justified => justified_lines += fn_lines,
205            Justification::Partial => partial_lines += fn_lines,
206            Justification::Unjustified => unjustified_lines += fn_lines,
207        }
208
209        functions.push(FnDetail {
210            name: fd.name.clone(),
211            lines: fn_lines,
212            has_description,
213            is_effectful,
214            verify_cases,
215            has_coverage_gaps,
216            has_decision_impact,
217            level,
218            missing,
219        });
220    }
221
222    let non_fn_lines =
223        total_lines.saturating_sub(justified_lines + partial_lines + unjustified_lines);
224    if has_module_intent {
225        justified_lines += non_fn_lines;
226    } else {
227        unjustified_lines += non_fn_lines;
228    }
229
230    let decision_summaries: Vec<DecisionSummary> = decisions
231        .iter()
232        .map(|d| {
233            let reason_prefix: String = d.reason.chars().take(60).collect();
234            let reason_prefix = if d.reason.len() > 60 {
235                format!("{}...", reason_prefix.trim_end())
236            } else {
237                reason_prefix
238            };
239            DecisionSummary {
240                name: d.name.clone(),
241                date: d.date.clone(),
242                reason_prefix,
243            }
244        })
245        .collect();
246
247    WhySummary {
248        file_label: file_label.into(),
249        total_lines,
250        justified_lines,
251        partial_lines,
252        unjustified_lines,
253        has_module_intent,
254        decisions: decision_summaries,
255        functions,
256    }
257}
258
259fn next_toplevel_line_after(items: &[TopLevel], after_line: usize) -> Option<usize> {
260    let mut min_line: Option<usize> = None;
261    for item in items {
262        let line = match item {
263            TopLevel::FnDef(fd) => fd.line,
264            TopLevel::Verify(v) => v.line,
265            TopLevel::Decision(d) => d.line,
266            TopLevel::TypeDef(_) | TopLevel::Module(_) | TopLevel::Stmt(_) => continue,
267        };
268        if line > after_line {
269            min_line = Some(match min_line {
270                Some(cur) if line < cur => line,
271                Some(cur) => cur,
272                None => line,
273            });
274        }
275    }
276    min_line.map(|l| l.saturating_sub(1))
277}
aver/diagnostics/why.rs

aver/diagnostics/
why.rs
