1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
//! Per-obligation verification matrix.
//!
//! Shows L2/L3/L4 status for each proof obligation across all contracts.
use serde::{Deserialize, Serialize};
use crate::proof_status::ProofLevel;
use crate::schema::Contract;
/// Verification status for a single obligation across all proof levels.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ObligationStatus {
/// Human-readable obligation property name
pub property: String,
/// Obligation type (invariant, bound, equivalence, etc.)
pub obligation_type: String,
/// Whether at least one falsification test covers this obligation
pub l2_tested: bool,
/// Whether at least one Kani harness covers this obligation
pub l3_kani: bool,
/// Whether the obligation has a Lean proof with status "proved"
pub l4_lean: bool,
/// Highest achieved level for this specific obligation
pub max_level: ProofLevel,
}
/// Per-contract obligation verification matrix.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ContractObligationMatrix {
/// Contract file stem (e.g. "softmax-kernel-v1")
pub stem: String,
/// Per-obligation verification status entries
pub obligations: Vec<ObligationStatus>,
}
/// Build per-obligation verification matrices for a list of contracts.
///
/// For each contract, determines per-obligation coverage:
/// - **L2**: A falsification test covers this obligation (index-based or rule match)
/// - **L3**: A Kani harness references this obligation (property match)
/// - **L4**: The obligation has a `lean` field with `status: proved`
pub fn obligation_matrix(contracts: &[(String, &Contract)]) -> Vec<ContractObligationMatrix> {
contracts
.iter()
.map(|(stem, contract)| {
let obligations = contract
.proof_obligations
.iter()
.enumerate()
.map(|(idx, ob)| {
let prop_lower = ob.property.to_lowercase();
// L2: check if any falsification test covers this obligation.
// Strategy: index-based (obligation i covered if i < test count),
// plus rule-text matching against the property name.
let l2_tested = idx < contract.falsification_tests.len()
|| contract.falsification_tests.iter().any(|ft| {
let rule_lower = ft.rule.to_lowercase();
prop_lower.contains(&rule_lower) || rule_lower.contains(&prop_lower)
});
// L3: check if any Kani harness covers this obligation.
// Match by property text overlap or by harness property containing
// key words from the obligation property.
let l3_kani = contract.kani_harnesses.iter().any(|kh| {
if let Some(ref kh_prop) = kh.property {
let kh_lower = kh_prop.to_lowercase();
property_words_match(&prop_lower, &kh_lower)
} else {
false
}
});
// L4: obligation has lean proof with status proved
let l4_lean = ob
.lean
.as_ref()
.is_some_and(|lp| lp.status == crate::schema::LeanStatus::Proved);
let max_level = if l4_lean {
ProofLevel::L4
} else if l3_kani {
ProofLevel::L3
} else if l2_tested {
ProofLevel::L2
} else {
ProofLevel::L1
};
ObligationStatus {
property: ob.property.clone(),
obligation_type: ob.obligation_type.to_string(),
l2_tested,
l3_kani,
l4_lean,
max_level,
}
})
.collect();
ContractObligationMatrix {
stem: stem.clone(),
obligations,
}
})
.collect()
}
/// Format per-obligation matrices as a human-readable table.
pub fn format_obligation_table(matrices: &[ContractObligationMatrix]) -> String {
let mut out = String::new();
out.push_str("\nObligation Status Matrix\n");
out.push_str("========================\n");
for matrix in matrices {
if matrix.obligations.is_empty() {
continue;
}
// Compute max property width (capped at 40 for readability)
let max_prop_width = matrix
.obligations
.iter()
.map(|o| o.property.len())
.max()
.unwrap_or(20)
.min(40);
out.push_str(&format!("Contract: {}\n", matrix.stem));
out.push_str(&format!(
" {:<width$} | L2 Test | L3 Kani | L4 Lean | Status\n",
"Obligation",
width = max_prop_width
));
out.push_str(&format!(" {}\n", "-".repeat(max_prop_width + 39)));
for ob in &matrix.obligations {
let check = "\u{2713}";
let cross = "\u{2717}";
let l2 = if ob.l2_tested { check } else { cross };
let l3 = if ob.l3_kani { check } else { cross };
let l4 = if ob.l4_lean { check } else { cross };
let prop_display = truncate(&ob.property, max_prop_width);
out.push_str(&format!(
" {:<width$} | {} | {} | {} | {}\n",
prop_display,
l2,
l3,
l4,
ob.max_level,
width = max_prop_width
));
}
out.push('\n');
}
out
}
/// Check whether two property descriptions share significant words.
///
/// Splits both strings into words (>= 3 chars, excluding stop words) and
pub fn truncate(s: &str, max: usize) -> &str {
if s.len() <= max {
s
} else {
&s[..max]
}
}
/// returns true if at least one non-trivial word overlaps.
pub fn property_words_match(a: &str, b: &str) -> bool {
let stop_words: &[&str] = &[
"the", "for", "and", "all", "are", "with", "from", "that", "this", "has", "not", "any",
"each", "into",
];
let words_a: Vec<&str> = a
.split(|c: char| !c.is_alphanumeric())
.filter(|w| w.len() >= 3 && !stop_words.contains(w))
.collect();
words_a.iter().any(|wa| {
b.split(|c: char| !c.is_alphanumeric())
.filter(|w| w.len() >= 3 && !stop_words.contains(w))
.any(|wb| wa == &wb)
})
}
// Tests for obligation_matrix are in proof_status_tests.rs
// (included via proof_status.rs #[path] directive)