intent_ir/
audit.rs

1//! Audit Bridge — trace maps and coverage analysis.
2//!
3//! Cross-references IR constructs with their originating spec items
4//! via `SourceTrace` to produce:
5//! - Trace maps: which IR constructs implement each spec requirement
6//! - Coverage summaries: how much of the spec is compiled and verified
7
8use std::fmt;
9
10use serde::{Deserialize, Serialize};
11
12use crate::types::*;
13use crate::verify::Obligation;
14
15/// A complete audit report for a module.
16#[derive(Debug, Clone, Serialize)]
17pub struct AuditReport {
18    pub module_name: String,
19    pub entries: Vec<AuditEntry>,
20    pub summary: CoverageSummary,
21    pub verify_error_count: usize,
22    pub obligations: Vec<Obligation>,
23}
24
25/// One spec-level item and its IR trace.
26#[derive(Debug, Clone, Serialize)]
27pub struct AuditEntry {
28    pub kind: SpecItemKind,
29    pub name: String,
30    pub line: usize,
31    pub parts: Vec<TracePart>,
32    /// Obligations that reference this item.
33    pub related_obligations: Vec<String>,
34}
35
36/// What kind of spec item this entry represents.
37#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
38pub enum SpecItemKind {
39    Entity,
40    Action,
41    Invariant,
42    EdgeCases,
43}
44
45/// A single spec sub-item mapped to IR.
46#[derive(Debug, Clone, Serialize)]
47pub struct TracePart {
48    /// Spec-level label (e.g., "field:balance", "requires[0]", "property:atomic").
49    pub label: String,
50    /// IR-level description.
51    pub ir_desc: String,
52    /// 1-based source line number.
53    pub line: usize,
54}
55
56/// Coverage statistics for the module.
57#[derive(Debug, Clone, Serialize)]
58pub struct CoverageSummary {
59    pub entities: usize,
60    pub fields: usize,
61    pub actions: usize,
62    pub params: usize,
63    pub preconditions: usize,
64    pub postconditions: usize,
65    pub properties: usize,
66    pub invariants: usize,
67    pub edge_guards: usize,
68}
69
70impl CoverageSummary {
71    pub fn total(&self) -> usize {
72        self.entities
73            + self.fields
74            + self.actions
75            + self.params
76            + self.preconditions
77            + self.postconditions
78            + self.properties
79            + self.invariants
80            + self.edge_guards
81    }
82}
83
84/// Generate an audit report by walking the IR module and cross-referencing
85/// with verification results.
86pub fn generate_audit(
87    source: &str,
88    module: &Module,
89    verify_errors: &[crate::verify::VerifyError],
90    obligations: &[Obligation],
91) -> AuditReport {
92    let line_index = build_line_index(source);
93    let mut entries = Vec::new();
94
95    // Structs (from entities)
96    for s in &module.structs {
97        let mut parts = Vec::new();
98        for f in &s.fields {
99            parts.push(TracePart {
100                label: format!("field:{}", f.name),
101                ir_desc: format!("{}: {}", f.name, format_ir_type(&f.ty)),
102                line: offset_to_line(&line_index, f.trace.span.start),
103            });
104        }
105        entries.push(AuditEntry {
106            kind: SpecItemKind::Entity,
107            name: s.name.clone(),
108            line: offset_to_line(&line_index, s.trace.span.start),
109            parts,
110            related_obligations: vec![],
111        });
112    }
113
114    // Functions (from actions)
115    for func in &module.functions {
116        let mut parts = Vec::new();
117        for p in &func.params {
118            parts.push(TracePart {
119                label: format!("param:{}", p.name),
120                ir_desc: format!("{}: {}", p.name, format_ir_type(&p.ty)),
121                line: offset_to_line(&line_index, p.trace.span.start),
122            });
123        }
124        for (i, pre) in func.preconditions.iter().enumerate() {
125            parts.push(TracePart {
126                label: format!("requires[{}]", i),
127                ir_desc: "precondition".into(),
128                line: offset_to_line(&line_index, pre.trace.span.start),
129            });
130        }
131        for (i, post) in func.postconditions.iter().enumerate() {
132            let (trace, desc) = match post {
133                Postcondition::Always { trace, .. } => (trace, "postcondition"),
134                Postcondition::When { trace, .. } => (trace, "conditional postcondition"),
135            };
136            parts.push(TracePart {
137                label: format!("ensures[{}]", i),
138                ir_desc: desc.into(),
139                line: offset_to_line(&line_index, trace.span.start),
140            });
141        }
142        for prop in &func.properties {
143            parts.push(TracePart {
144                label: format!("property:{}", prop.key),
145                ir_desc: format!("{}: {}", prop.key, format_prop_value(&prop.value)),
146                line: offset_to_line(&line_index, prop.trace.span.start),
147            });
148        }
149
150        let related: Vec<String> = obligations
151            .iter()
152            .filter(|o| o.action == func.name)
153            .map(|o| o.to_string())
154            .collect();
155
156        entries.push(AuditEntry {
157            kind: SpecItemKind::Action,
158            name: func.name.clone(),
159            line: offset_to_line(&line_index, func.trace.span.start),
160            parts,
161            related_obligations: related,
162        });
163    }
164
165    // Invariants
166    for inv in &module.invariants {
167        let related: Vec<String> = obligations
168            .iter()
169            .filter(|o| o.invariant == inv.name)
170            .map(|o| o.to_string())
171            .collect();
172
173        entries.push(AuditEntry {
174            kind: SpecItemKind::Invariant,
175            name: inv.name.clone(),
176            line: offset_to_line(&line_index, inv.trace.span.start),
177            parts: vec![],
178            related_obligations: related,
179        });
180    }
181
182    // Edge guards
183    if !module.edge_guards.is_empty() {
184        let first_line = offset_to_line(&line_index, module.edge_guards[0].trace.span.start);
185        let mut parts = Vec::new();
186        for (i, guard) in module.edge_guards.iter().enumerate() {
187            parts.push(TracePart {
188                label: format!("guard[{}]", i),
189                ir_desc: format!("when ... => {}", guard.action),
190                line: offset_to_line(&line_index, guard.trace.span.start),
191            });
192        }
193        entries.push(AuditEntry {
194            kind: SpecItemKind::EdgeCases,
195            name: "edge_cases".into(),
196            line: first_line,
197            parts,
198            related_obligations: vec![],
199        });
200    }
201
202    let summary = CoverageSummary {
203        entities: module.structs.len(),
204        fields: module.structs.iter().map(|s| s.fields.len()).sum(),
205        actions: module.functions.len(),
206        params: module.functions.iter().map(|f| f.params.len()).sum(),
207        preconditions: module.functions.iter().map(|f| f.preconditions.len()).sum(),
208        postconditions: module
209            .functions
210            .iter()
211            .map(|f| f.postconditions.len())
212            .sum(),
213        properties: module.functions.iter().map(|f| f.properties.len()).sum(),
214        invariants: module.invariants.len(),
215        edge_guards: module.edge_guards.len(),
216    };
217
218    AuditReport {
219        module_name: module.name.clone(),
220        entries,
221        summary,
222        verify_error_count: verify_errors.len(),
223        obligations: obligations.to_vec(),
224    }
225}
226
227// ── Display implementations ────────────────────────────────
228
229impl fmt::Display for SpecItemKind {
230    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
231        match self {
232            SpecItemKind::Entity => write!(f, "Entity"),
233            SpecItemKind::Action => write!(f, "Action"),
234            SpecItemKind::Invariant => write!(f, "Invariant"),
235            SpecItemKind::EdgeCases => write!(f, "EdgeCases"),
236        }
237    }
238}
239
240impl AuditReport {
241    /// Format as a trace map (for `intent audit`).
242    pub fn format_trace_map(&self) -> String {
243        let mut out = format!("{} — Audit Trace Map\n", self.module_name);
244
245        for entry in &self.entries {
246            out.push('\n');
247            let ir_kind = match entry.kind {
248                SpecItemKind::Entity => "Struct",
249                SpecItemKind::Action => "Function",
250                SpecItemKind::Invariant => "Invariant",
251                SpecItemKind::EdgeCases => "Guards",
252            };
253
254            if entry.kind == SpecItemKind::EdgeCases {
255                out.push_str(&format!("  EdgeCases -> {ir_kind}\n"));
256            } else {
257                out.push_str(&format!("  {} {} -> {ir_kind}", entry.kind, entry.name,));
258                out.push_str(&format!("  [L{}]\n", entry.line));
259            }
260
261            let total = entry.parts.len() + entry.related_obligations.len();
262            for (i, part) in entry.parts.iter().enumerate() {
263                let is_last = i == total - 1;
264                let prefix = if is_last { "└──" } else { "├──" };
265                out.push_str(&format!(
266                    "    {prefix} {}: {}  [L{}]\n",
267                    part.label, part.ir_desc, part.line,
268                ));
269            }
270
271            for (i, ob) in entry.related_obligations.iter().enumerate() {
272                let is_last = entry.parts.len() + i == total - 1;
273                let prefix = if is_last { "└──" } else { "├──" };
274                out.push_str(&format!("    {prefix} obligation: {ob}\n"));
275            }
276        }
277
278        out.push_str(&format!(
279            "\nCoverage: {total} spec items compiled",
280            total = self.summary.total(),
281        ));
282        if self.verify_error_count == 0 {
283            out.push_str(", verification clean\n");
284        } else {
285            out.push_str(&format!(
286                ", {} verification error(s)\n",
287                self.verify_error_count
288            ));
289        }
290        if !self.obligations.is_empty() {
291            out.push_str(&format!(
292                "Obligations: {} identified\n",
293                self.obligations.len()
294            ));
295        }
296
297        out
298    }
299
300    /// Format as a coverage summary (for `intent coverage`).
301    pub fn format_coverage(&self) -> String {
302        let s = &self.summary;
303        let mut out = format!("{} — Coverage Summary\n\n", self.module_name);
304
305        out.push_str(&format!(
306            "  Entities:       {:>3} ({} fields)\n",
307            s.entities, s.fields,
308        ));
309        out.push_str(&format!(
310            "  Actions:        {:>3} ({} params, {} requires, {} ensures, {} properties)\n",
311            s.actions, s.params, s.preconditions, s.postconditions, s.properties,
312        ));
313        out.push_str(&format!("  Invariants:     {:>3}\n", s.invariants));
314        out.push_str(&format!("  Edge guards:    {:>3}\n", s.edge_guards));
315        out.push_str("  ─────────────────────────────\n");
316        out.push_str(&format!(
317            "  Total:          {:>3} spec items compiled\n",
318            s.total(),
319        ));
320
321        out.push('\n');
322        if self.verify_error_count == 0 {
323            out.push_str("  Verification:   clean (0 errors)\n");
324        } else {
325            out.push_str(&format!(
326                "  Verification:   {} error(s)\n",
327                self.verify_error_count,
328            ));
329        }
330
331        if self.obligations.is_empty() {
332            out.push_str("  Obligations:    none\n");
333        } else {
334            out.push_str(&format!(
335                "  Obligations:    {} identified\n",
336                self.obligations.len(),
337            ));
338            for ob in &self.obligations {
339                out.push_str(&format!("    - {ob}\n"));
340            }
341        }
342
343        out
344    }
345}
346
347// ── Helpers ────────────────────────────────────────────────
348
349/// Build a line-start index: `line_starts[i]` is the byte offset where line `i+1` begins.
350fn build_line_index(source: &str) -> Vec<usize> {
351    let mut starts = vec![0];
352    for (i, ch) in source.char_indices() {
353        if ch == '\n' {
354            starts.push(i + 1);
355        }
356    }
357    starts
358}
359
360/// Convert a byte offset to a 1-based line number.
361fn offset_to_line(line_starts: &[usize], offset: usize) -> usize {
362    match line_starts.binary_search(&offset) {
363        Ok(i) => i + 1,
364        Err(i) => i,
365    }
366}
367
368fn format_ir_type(ty: &IrType) -> String {
369    match ty {
370        IrType::Named(n) => n.clone(),
371        IrType::Struct(n) => n.clone(),
372        IrType::List(inner) => format!("List<{}>", format_ir_type(inner)),
373        IrType::Set(inner) => format!("Set<{}>", format_ir_type(inner)),
374        IrType::Map(k, v) => {
375            format!("Map<{}, {}>", format_ir_type(k), format_ir_type(v))
376        }
377        IrType::Optional(inner) => format!("{}?", format_ir_type(inner)),
378        IrType::Union(variants) => variants.join(" | "),
379        IrType::Decimal(p) => format!("Decimal({p})"),
380    }
381}
382
383fn format_prop_value(v: &PropertyValue) -> String {
384    match v {
385        PropertyValue::Bool(b) => b.to_string(),
386        PropertyValue::Int(n) => n.to_string(),
387        PropertyValue::String(s) => format!("\"{s}\""),
388        PropertyValue::Ident(i) => i.clone(),
389    }
390}
intent_ir/audit.rs

intent_ir/
audit.rs
