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

intent_ir/
audit.rs
