1use std::collections::HashMap;
10
11use serde::Deserialize;
12
13#[derive(Debug, Deserialize)]
15pub struct ContractFile {
16 pub contract: ContractMeta,
18 pub invariants: Vec<Invariant>,
20 pub verification: VerificationTargets,
22}
23
24#[derive(Debug, Deserialize)]
26pub struct ContractMeta {
27 pub name: String,
29 pub version: String,
31 pub module: String,
33 pub description: String,
35}
36
37#[derive(Debug, Deserialize)]
39pub struct Invariant {
40 pub id: String,
42 pub name: String,
44 pub description: String,
46 pub preconditions: Vec<String>,
48 pub postconditions: Vec<String>,
50 pub equation: String,
52 pub module_path: String,
54 pub test_binding: String,
56}
57
58#[derive(Debug, Deserialize)]
60pub struct VerificationTargets {
61 pub unit_tests: Vec<String>,
63 pub coverage_target: u32,
65 pub mutation_target: u32,
67 pub complexity_max_cyclomatic: u32,
69 pub complexity_max_cognitive: u32,
71}
72
73#[derive(Debug)]
75pub struct VerificationResult {
76 pub contract_name: String,
78 pub total_invariants: usize,
80 pub verified_bindings: usize,
82 pub missing_bindings: Vec<String>,
84 pub invariant_status: HashMap<String, InvariantStatus>,
86}
87
88#[derive(Debug, Clone)]
90pub struct InvariantStatus {
91 pub id: String,
93 pub name: String,
95 pub test_found: bool,
97 pub test_binding: String,
99}
100
101impl VerificationResult {
102 #[must_use]
104 pub fn all_verified(&self) -> bool {
105 self.missing_bindings.is_empty()
106 }
107
108 #[must_use]
110 pub fn report(&self) -> String {
111 use std::fmt::Write;
112 let mut out = String::new();
113 let _ = writeln!(
114 out,
115 "Contract: {} ({}/{})",
116 self.contract_name, self.verified_bindings, self.total_invariants,
117 );
118
119 for status in self.invariant_status.values() {
120 let mark = if status.test_found { "✓" } else { "✗" };
121 let _ = writeln!(out, " [{mark}] {} — {}", status.id, status.name,);
122 }
123
124 if !self.missing_bindings.is_empty() {
125 let _ = writeln!(out, "\nMissing bindings:");
126 for b in &self.missing_bindings {
127 let _ = writeln!(out, " - {b}");
128 }
129 }
130
131 out
132 }
133}
134
135pub fn parse_contract(yaml_content: &str) -> Result<ContractFile, String> {
137 serde_yaml_ng::from_str(yaml_content).map_err(|e| format!("YAML parse error: {e}"))
138}
139
140pub fn verify_bindings(contract: &ContractFile, known_tests: &[String]) -> VerificationResult {
145 let mut status = HashMap::new();
146 let mut missing = Vec::new();
147 let mut verified = 0;
148
149 for inv in &contract.invariants {
150 let found = known_tests.iter().any(|t| t.contains(&inv.test_binding));
151
152 if found {
153 verified += 1;
154 } else {
155 missing.push(format!("{}: {} (expected: {})", inv.id, inv.name, inv.test_binding,));
156 }
157
158 status.insert(
159 inv.id.clone(),
160 InvariantStatus {
161 id: inv.id.clone(),
162 name: inv.name.clone(),
163 test_found: found,
164 test_binding: inv.test_binding.clone(),
165 },
166 );
167 }
168
169 VerificationResult {
170 contract_name: contract.contract.name.clone(),
171 total_invariants: contract.invariants.len(),
172 verified_bindings: verified,
173 missing_bindings: missing,
174 invariant_status: status,
175 }
176}
177
178#[cfg(test)]
179mod tests {
180 use super::*;
181
182 const TEST_YAML: &str = include_str!("../../contracts/agent-loop-v1.yaml");
183
184 #[test]
185 fn test_parse_contract() {
186 let contract = parse_contract(TEST_YAML).expect("parse failed");
187 assert_eq!(contract.contract.name, "agent-loop-v1");
188 assert_eq!(contract.contract.version, "1.0.0");
189 assert_eq!(contract.contract.module, "batuta::agent");
190 assert!(!contract.invariants.is_empty());
191 }
192
193 #[test]
194 fn test_invariant_count() {
195 let contract = parse_contract(TEST_YAML).expect("parse failed");
196 assert_eq!(
197 contract.invariants.len(),
198 16,
199 "expected 16 invariants (8 loop + 4 pool/sanitization + 4 tool)"
200 );
201 }
202
203 #[test]
204 fn test_invariant_ids() {
205 let contract = parse_contract(TEST_YAML).expect("parse failed");
206 let ids: Vec<&str> = contract.invariants.iter().map(|i| i.id.as_str()).collect();
207 assert!(ids.contains(&"INV-001"));
208 assert!(ids.contains(&"INV-007"));
209 }
210
211 #[test]
212 fn test_invariant_fields_populated() {
213 let contract = parse_contract(TEST_YAML).expect("parse failed");
214 for inv in &contract.invariants {
215 assert!(!inv.name.is_empty(), "{} has empty name", inv.id);
216 assert!(!inv.description.is_empty(), "{} has empty description", inv.id);
217 assert!(!inv.preconditions.is_empty(), "{} has no preconditions", inv.id);
218 assert!(!inv.postconditions.is_empty(), "{} has no postconditions", inv.id);
219 assert!(!inv.equation.is_empty(), "{} has empty equation", inv.id);
220 assert!(!inv.module_path.is_empty(), "{} has empty module_path", inv.id);
221 assert!(!inv.test_binding.is_empty(), "{} has empty test_binding", inv.id);
222 }
223 }
224
225 #[test]
226 fn test_verification_targets() {
227 let contract = parse_contract(TEST_YAML).expect("parse failed");
228 assert_eq!(contract.verification.coverage_target, 95);
229 assert_eq!(contract.verification.mutation_target, 80);
230 assert_eq!(contract.verification.complexity_max_cyclomatic, 30);
231 assert_eq!(contract.verification.complexity_max_cognitive, 25);
232 assert!(!contract.verification.unit_tests.is_empty());
233 }
234
235 #[test]
236 fn test_verify_all_bindings_found() {
237 let contract = parse_contract(TEST_YAML).expect("parse failed");
238
239 let known_tests: Vec<String> =
241 contract.invariants.iter().map(|i| i.test_binding.clone()).collect();
242
243 let result = verify_bindings(&contract, &known_tests);
244 assert!(result.all_verified());
245 assert_eq!(result.verified_bindings, contract.invariants.len());
246 }
247
248 #[test]
249 fn test_verify_missing_binding() {
250 let contract = parse_contract(TEST_YAML).expect("parse failed");
251
252 let result = verify_bindings(&contract, &[]);
254 assert!(!result.all_verified());
255 assert_eq!(result.verified_bindings, 0);
256 assert_eq!(result.missing_bindings.len(), contract.invariants.len());
257 }
258
259 #[test]
260 fn test_verify_partial_bindings() {
261 let contract = parse_contract(TEST_YAML).expect("parse failed");
262
263 let known_tests = vec![contract.invariants[0].test_binding.clone()];
265
266 let result = verify_bindings(&contract, &known_tests);
267 assert!(!result.all_verified());
268 assert_eq!(result.verified_bindings, 1);
269 }
270
271 #[test]
272 fn test_report_format() {
273 let contract = parse_contract(TEST_YAML).expect("parse failed");
274 let result = verify_bindings(&contract, &[]);
275 let report = result.report();
276 assert!(report.contains("agent-loop-v1"));
277 assert!(report.contains("Missing bindings"));
278 }
279
280 #[test]
281 fn test_report_all_pass() {
282 let contract = parse_contract(TEST_YAML).expect("parse failed");
283 let known_tests: Vec<String> =
284 contract.invariants.iter().map(|i| i.test_binding.clone()).collect();
285 let result = verify_bindings(&contract, &known_tests);
286 let report = result.report();
287 assert!(!report.contains("Missing bindings"));
288 }
289
290 #[test]
292 fn test_contract_equations_have_code_bindings() {
293 let contract = parse_contract(TEST_YAML).expect("parse failed");
294
295 let bound_equations = [
299 "loop_termination", "capability_match", "guard_budget", ];
303
304 for inv in &contract.invariants {
305 let eq_lines: Vec<&str> =
306 inv.equation.lines().map(str::trim).filter(|l| !l.is_empty()).collect();
307 assert!(!eq_lines.is_empty(), "{}: empty equation", inv.id);
309 }
310
311 let bound_count = contract
313 .invariants
314 .iter()
315 .filter(|inv| {
316 bound_equations.iter().any(|eq| {
317 inv.equation.contains(eq)
318 || inv.module_path.contains("record_cost")
319 || inv.module_path.contains("run_agent_loop")
320 || inv.module_path.contains("capability_matches")
321 })
322 })
323 .count();
324
325 assert!(bound_count >= 3, "expected >= 3 #[contract] bindings, got {bound_count}");
326 }
327
328 #[test]
331 fn test_all_contract_bindings_exist() {
332 let contract = parse_contract(TEST_YAML).expect("parse failed");
333
334 let existing_tests = [
337 "agent::guard::tests::test_iteration_limit",
338 "agent::guard::tests::test_counters",
339 "agent::runtime::tests::test_capability_denied_handled",
340 "agent::guard::tests::test_pingpong_detection",
341 "agent::guard::tests::test_cost_budget",
342 "agent::guard::tests::test_consecutive_max_tokens",
343 "agent::runtime::tests::test_conversation_stored_in_memory",
344 "agent::pool::tests::test_pool_capacity_limit",
345 "agent::pool::tests::test_pool_fan_out_fan_in",
346 "agent::pool::tests::test_pool_join_all",
347 "agent::tool::tests::test_sanitize_output_system_injection",
348 "agent::tool::spawn::tests::test_spawn_tool_depth_limit",
349 "agent::tool::network::tests::test_blocked_host",
350 "agent::tool::inference::tests::test_inference_tool_timeout",
351 "agent::runtime::tests_advanced::test_sovereign_privacy_blocks_network",
352 "agent::guard::tests::test_token_budget_exhausted",
353 ];
354
355 let known: Vec<String> = existing_tests.iter().map(|s| (*s).to_string()).collect();
356 let result = verify_bindings(&contract, &known);
357
358 assert!(result.all_verified(), "Missing bindings:\n{}", result.report());
359 }
360}