aver/diagnostics/
model.rs

1//! Canonical diagnostic data model.
2//!
3//! Runtime-neutral and wasm-safe — no `colored`, no file IO, no VM.
4//! Shared between CLI (`src/main/tty_render.rs`), LSP (`aver-lsp`),
5//! and playground (`src/playground.rs`).
6
7use serde::Serialize;
8
9pub const SCHEMA_VERSION: u32 = 1;
10
11#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)]
12#[serde(rename_all = "lowercase")]
13pub enum Severity {
14    Error,
15    Warning,
16    Fail,
17    Hint,
18}
19
20#[derive(Clone, Debug, Serialize)]
21pub struct Span {
22    pub file: String,
23    pub line: usize,
24    pub col: usize,
25}
26
27#[derive(Clone, Debug, Serialize)]
28pub struct SourceLine {
29    pub line_num: usize,
30    pub text: String,
31}
32
33#[derive(Clone, Debug, Serialize)]
34pub struct Underline {
35    pub col: usize,
36    pub len: usize,
37    pub label: String,
38}
39
40#[derive(Clone, Debug, Serialize)]
41pub struct AnnotatedRegion {
42    pub source_lines: Vec<SourceLine>,
43    #[serde(skip_serializing_if = "Option::is_none")]
44    pub underline: Option<Underline>,
45}
46
47impl AnnotatedRegion {
48    pub fn single(source_lines: Vec<SourceLine>, underline: Option<Underline>) -> Vec<Self> {
49        vec![Self {
50            source_lines,
51            underline,
52        }]
53    }
54}
55
56#[derive(Clone, Debug, Serialize)]
57pub struct RelatedSpan {
58    pub span: Span,
59    pub label: String,
60}
61
62#[derive(Clone, Debug, Default, Serialize)]
63pub struct Repair {
64    #[serde(skip_serializing_if = "Option::is_none")]
65    pub primary: Option<String>,
66    #[serde(skip_serializing_if = "Vec::is_empty")]
67    pub alternatives: Vec<String>,
68    #[serde(skip_serializing_if = "Option::is_none")]
69    pub example: Option<String>,
70}
71
72impl Repair {
73    pub fn primary(text: impl Into<String>) -> Self {
74        Self {
75            primary: Some(text.into()),
76            alternatives: Vec::new(),
77            example: None,
78        }
79    }
80
81    pub fn is_empty(&self) -> bool {
82        self.primary.is_none() && self.alternatives.is_empty() && self.example.is_none()
83    }
84}
85
86#[derive(Clone, Debug, Serialize)]
87pub struct Diagnostic {
88    pub severity: Severity,
89    pub slug: &'static str,
90    pub summary: String,
91    pub span: Span,
92    #[serde(skip_serializing_if = "Option::is_none")]
93    pub fn_name: Option<String>,
94    #[serde(skip_serializing_if = "Option::is_none")]
95    pub intent: Option<String>,
96    #[serde(skip_serializing_if = "Vec::is_empty")]
97    pub fields: Vec<(&'static str, String)>,
98    #[serde(skip_serializing_if = "Option::is_none")]
99    pub conflict: Option<String>,
100    #[serde(skip_serializing_if = "Repair::is_empty")]
101    pub repair: Repair,
102    #[serde(skip_serializing_if = "Vec::is_empty")]
103    pub regions: Vec<AnnotatedRegion>,
104    #[serde(skip_serializing_if = "Vec::is_empty")]
105    pub related: Vec<RelatedSpan>,
106    /// `true` when this diagnostic was raised by a case `aver verify
107    /// --hostile` injected through boundary-value expansion (a binding
108    /// the user did not write in the law's `given` clause). Lets tooling
109    /// (CI dashboards, IDE filters, LSP code actions) cleanly separate
110    /// "the law I already had stopped passing" from "hostile expansion
111    /// found a boundary value that breaks it". Default `false`; only
112    /// the hostile-aware verify pipeline sets it.
113    #[serde(skip_serializing_if = "is_false", default)]
114    pub from_hostile: bool,
115}
116
117fn is_false(b: &bool) -> bool {
118    !*b
119}
120
121impl Diagnostic {
122    pub fn is_warning(&self) -> bool {
123        matches!(self.severity, Severity::Warning)
124    }
125
126    pub fn is_error(&self) -> bool {
127        matches!(self.severity, Severity::Error | Severity::Fail)
128    }
129}
130
131#[derive(Clone, Debug, Serialize)]
132pub struct AnalysisReport {
133    pub schema_version: u32,
134    pub kind: &'static str,
135    pub file_label: String,
136    #[serde(skip_serializing_if = "Vec::is_empty")]
137    pub diagnostics: Vec<Diagnostic>,
138    /// File-local justification summary — present when the caller opts
139    /// in via `AnalyzeOptions::include_why_summary`.
140    #[serde(skip_serializing_if = "Option::is_none")]
141    pub why_summary: Option<crate::diagnostics::why::WhySummary>,
142    /// File-local context summary (module shape, functions, types,
143    /// decisions) — present when `include_context_summary` is set.
144    #[serde(skip_serializing_if = "Option::is_none")]
145    pub context_summary: Option<crate::diagnostics::context::ContextSummary>,
146    /// Per-verify-block pass/fail/skip counts — present when
147    /// `include_verify_run` is set. Diagnostics list carries the failing
148    /// case details; `verify_summary` gives the scorecard.
149    #[serde(skip_serializing_if = "Option::is_none")]
150    pub verify_summary: Option<VerifySummary>,
151}
152
153/// Per-block verify results. Mirrors what `aver verify` used to emit as
154/// `block-result` NDJSON events — now folded into the analysis bundle
155/// so a single record per file carries failures + scorecard.
156#[derive(Clone, Debug, Serialize)]
157pub struct VerifySummary {
158    pub blocks: Vec<VerifyBlockResult>,
159}
160
161/// One formatter rule firing on one location. Emitted by
162/// `try_format_source` alongside the rewritten text, then folded into a
163/// canonical `needs-format` [`Diagnostic`] by the factory.
164///
165/// `rule` is a stable slug ("bad-operator-spacing", "effect-order",
166/// "verify-block-order", …) consumed by LSP `code`, docs, and CI rules.
167/// `before`/`after` are optional short snippets for teaching; long
168/// rewrites can omit them.
169#[derive(Clone, Debug, Serialize)]
170pub struct FormatViolation {
171    pub line: usize,
172    pub col: usize,
173    pub rule: &'static str,
174    pub message: String,
175    #[serde(skip_serializing_if = "Option::is_none")]
176    pub before: Option<String>,
177    #[serde(skip_serializing_if = "Option::is_none")]
178    pub after: Option<String>,
179}
180
181#[derive(Clone, Debug, Serialize)]
182pub struct VerifyBlockResult {
183    pub name: String,
184    pub passed: usize,
185    pub failed: usize,
186    /// Combined skipped count (`when`-driven plus base-fail-driven).
187    /// Kept for back-compat with consumers that don't care about the
188    /// distinction; the split lives in the two fields below.
189    pub skipped: usize,
190    pub total: usize,
191    /// Cases that originated from the user's declared `given` list (or
192    /// the `verify` cases-form values they wrote literally). Always
193    /// populated under `--hostile`; under a non-hostile run, equal to
194    /// `passed/failed` and `hostile_*` are zero.
195    #[serde(skip_serializing_if = "is_zero", default)]
196    pub declared_passed: usize,
197    #[serde(skip_serializing_if = "is_zero", default)]
198    pub declared_failed: usize,
199    /// Cases injected by `aver verify --hostile` boundary expansion.
200    /// `hostile_failed > 0 && declared_failed == 0` is the canonical
201    /// "your law passed on the values you wrote but breaks on the
202    /// boundary" signal — encode the missing precondition as `when`,
203    /// or drop the `law` form to a `verify` cases-form example.
204    #[serde(skip_serializing_if = "is_zero", default)]
205    pub hostile_passed: usize,
206    #[serde(skip_serializing_if = "is_zero", default)]
207    pub hostile_failed: usize,
208    /// Cases skipped because the user's `when` predicate evaluated
209    /// to false. Subset of `skipped`. When this equals `skipped` and
210    /// no hostile profiles ran, the law is vacuously-under-hostile.
211    #[serde(skip_serializing_if = "is_zero", default)]
212    pub skipped_by_when: usize,
213    /// Cases skipped because the same `case_expr` already failed in
214    /// its un-effected base world. Aver doesn't run the VM for these
215    /// — they would only re-confirm the same counter-example under
216    /// harder worlds. Subset of `skipped`.
217    #[serde(skip_serializing_if = "is_zero", default)]
218    pub skipped_after_base_fail: usize,
219}
220
221fn is_zero(n: &usize) -> bool {
222    *n == 0
223}
224
225impl AnalysisReport {
226    pub fn new(file_label: impl Into<String>) -> Self {
227        Self {
228            schema_version: SCHEMA_VERSION,
229            kind: "analysis",
230            file_label: file_label.into(),
231            diagnostics: Vec::new(),
232            why_summary: None,
233            context_summary: None,
234            verify_summary: None,
235        }
236    }
237
238    pub fn with_diagnostics(file_label: impl Into<String>, diagnostics: Vec<Diagnostic>) -> Self {
239        Self {
240            schema_version: SCHEMA_VERSION,
241            kind: "analysis",
242            file_label: file_label.into(),
243            diagnostics,
244            why_summary: None,
245            context_summary: None,
246            verify_summary: None,
247        }
248    }
249
250    pub fn to_json(&self) -> String {
251        serde_json::to_string(self).unwrap_or_else(|_| "{}".to_string())
252    }
253}
254
255/// Minimal JSON string escaping. Kept as a standalone helper so legacy
256/// per-record CLI JSON (bit-for-bit parity with 0.9.x) can build output
257/// without pulling serde into every format string.
258pub fn json_escape(s: &str) -> String {
259    let mut out = String::with_capacity(s.len() + 2);
260    out.push('"');
261    for ch in s.chars() {
262        match ch {
263            '"' => out.push_str("\\\""),
264            '\\' => out.push_str("\\\\"),
265            '\n' => out.push_str("\\n"),
266            '\r' => out.push_str("\\r"),
267            '\t' => out.push_str("\\t"),
268            c => out.push(c),
269        }
270    }
271    out.push('"');
272    out
273}
aver/diagnostics/model.rs

aver/diagnostics/
model.rs
