1use super::{DefectCategory, Finding, FindingEvidence, FindingSeverity, HuntMode};
8use serde::Deserialize;
9use std::path::Path;
10
11#[derive(Deserialize)]
16struct BindingRegistry {
17 target_crate: String,
18 bindings: Vec<KernelBinding>,
19}
20
21#[derive(Deserialize)]
22struct KernelBinding {
23 contract: String,
24 equation: String,
25 status: String,
26 notes: Option<String>,
27 module_path: Option<String>,
28}
29
30#[derive(Deserialize)]
31struct ContractFile {
32 metadata: ContractMetadata,
33 #[serde(default)]
34 proof_obligations: Vec<ProofObligation>,
35 #[serde(default)]
36 falsification_tests: Vec<FalsificationTest>,
37}
38
39#[derive(Deserialize)]
40struct ContractMetadata {
41 version: Option<String>,
42 description: Option<String>,
43}
44
45#[derive(Deserialize)]
46struct ProofObligation {
47 property: Option<String>,
48 #[serde(rename = "type")]
49 obligation_type: Option<String>,
50}
51
52#[derive(Deserialize)]
53struct FalsificationTest {
54 name: Option<String>,
55}
56
57pub fn discover_contracts_dir(
65 project_path: &Path,
66 explicit_path: Option<&Path>,
67) -> Option<std::path::PathBuf> {
68 if let Some(p) = explicit_path {
69 if p.exists() {
70 return Some(p.to_path_buf());
71 }
72 }
73 let resolved = project_path.canonicalize().ok()?;
75 let parent = resolved.parent()?;
76 let auto_path = parent.join("provable-contracts").join("contracts");
77 if auto_path.is_dir() {
78 Some(auto_path)
79 } else {
80 None
81 }
82}
83
84pub fn analyze_contract_gaps(contracts_dir: &Path, _project_path: &Path) -> Vec<Finding> {
91 contract_pre_analyze!(contracts_dir);
92 let mut findings = Vec::new();
93 let mut finding_id = 0u32;
94
95 let mut bound_contracts: std::collections::HashSet<String> = std::collections::HashSet::new();
97
98 let binding_pattern = format!("{}/**/binding.yaml", contracts_dir.display());
100 if let Ok(entries) = glob::glob(&binding_pattern) {
101 for entry in entries.flatten() {
102 analyze_binding_file(&entry, &mut findings, &mut finding_id, &mut bound_contracts);
103 }
104 }
105
106 let contract_pattern = format!("{}/*.yaml", contracts_dir.display());
108 if let Ok(entries) = glob::glob(&contract_pattern) {
109 for entry in entries.flatten() {
110 let file_name = entry.file_name().and_then(|n| n.to_str()).unwrap_or("");
111 if file_name == "binding.yaml" || !file_name.ends_with(".yaml") {
112 continue;
113 }
114 if !bound_contracts.contains(file_name) {
115 finding_id += 1;
116 findings.push(
117 Finding::new(
118 format!("BH-CONTRACT-{:04}", finding_id),
119 &entry,
120 1,
121 format!("Unbound contract: {}", file_name),
122 )
123 .with_description(
124 "Contract YAML has no binding reference in any binding.yaml registry",
125 )
126 .with_severity(FindingSeverity::Medium)
127 .with_category(DefectCategory::ContractGap)
128 .with_suspiciousness(0.5)
129 .with_discovered_by(HuntMode::Analyze)
130 .with_evidence(FindingEvidence::contract_binding(file_name, "none", "unbound")),
131 );
132 }
133
134 analyze_obligation_coverage(&entry, file_name, &mut findings, &mut finding_id);
136 }
137 }
138
139 findings
140}
141
142fn analyze_binding_file(
147 path: &Path,
148 findings: &mut Vec<Finding>,
149 finding_id: &mut u32,
150 bound_contracts: &mut std::collections::HashSet<String>,
151) {
152 let Ok(content) = std::fs::read_to_string(path) else {
153 return;
154 };
155 let Ok(registry) = serde_yaml_ng::from_str::<BindingRegistry>(&content) else {
156 return;
157 };
158
159 for binding in ®istry.bindings {
160 bound_contracts.insert(binding.contract.clone());
161
162 let (severity, suspiciousness, desc) = match binding.status.as_str() {
163 "not_implemented" => (
164 FindingSeverity::High,
165 0.8,
166 format!(
167 "Binding `{}::{}` has no implementation{}",
168 binding.contract,
169 binding.equation,
170 binding.notes.as_deref().map(|n| format!(" — {}", n)).unwrap_or_default()
171 ),
172 ),
173 "partial" => (
174 FindingSeverity::Medium,
175 0.6,
176 format!(
177 "Binding `{}::{}` is partially implemented{}",
178 binding.contract,
179 binding.equation,
180 binding.notes.as_deref().map(|n| format!(" — {}", n)).unwrap_or_default()
181 ),
182 ),
183 _ => continue,
184 };
185
186 *finding_id += 1;
187 findings.push(
188 Finding::new(
189 format!("BH-CONTRACT-{:04}", finding_id),
190 path,
191 1,
192 format!(
193 "Contract gap: {} — {} ({})",
194 binding.contract, binding.equation, binding.status
195 ),
196 )
197 .with_description(desc)
198 .with_severity(severity)
199 .with_category(DefectCategory::ContractGap)
200 .with_suspiciousness(suspiciousness)
201 .with_discovered_by(HuntMode::Analyze)
202 .with_evidence(FindingEvidence::contract_binding(
203 &binding.contract,
204 &binding.equation,
205 &binding.status,
206 )),
207 );
208 }
209}
210
211fn analyze_obligation_coverage(
212 path: &Path,
213 file_name: &str,
214 findings: &mut Vec<Finding>,
215 finding_id: &mut u32,
216) {
217 let Ok(content) = std::fs::read_to_string(path) else {
218 return;
219 };
220 let Ok(contract) = serde_yaml_ng::from_str::<ContractFile>(&content) else {
221 return;
222 };
223
224 let total_obligations = contract.proof_obligations.len();
225 let total_tests = contract.falsification_tests.len();
226 if total_obligations == 0 {
227 return;
228 }
229
230 let coverage_ratio = total_tests as f64 / total_obligations as f64;
231 if coverage_ratio < 0.5 {
232 *finding_id += 1;
233 findings.push(
234 Finding::new(
235 format!("BH-CONTRACT-{:04}", finding_id),
236 path,
237 1,
238 format!(
239 "Low obligation coverage: {} ({}/{})",
240 file_name, total_tests, total_obligations
241 ),
242 )
243 .with_description(format!(
244 "Only {:.0}% of proof obligations have falsification tests",
245 coverage_ratio * 100.0
246 ))
247 .with_severity(FindingSeverity::Low)
248 .with_category(DefectCategory::ContractGap)
249 .with_suspiciousness(0.4)
250 .with_discovered_by(HuntMode::Analyze)
251 .with_evidence(FindingEvidence::contract_binding(
252 file_name,
253 "obligations",
254 format!("{}/{}", total_tests, total_obligations),
255 )),
256 );
257 }
258}
259
260#[cfg(test)]
261mod tests {
262 use super::*;
263 use std::io::Write;
264
265 fn by_title<'a>(findings: &'a [Finding], pattern: &str) -> Vec<&'a Finding> {
267 findings.iter().filter(|f| f.title.contains(pattern)).collect()
268 }
269
270 #[test]
271 fn test_parse_binding_registry() {
272 let yaml = r#"
273version: "1.0.0"
274target_crate: aprender
275bindings:
276 - contract: softmax-kernel-v1.yaml
277 equation: softmax
278 status: implemented
279 module_path: "aprender::nn::softmax"
280 - contract: matmul-kernel-v1.yaml
281 equation: matmul
282 status: not_implemented
283 notes: "No public function"
284"#;
285 let registry: BindingRegistry =
286 serde_yaml_ng::from_str(yaml).expect("yaml deserialize failed");
287 assert_eq!(registry.target_crate, "aprender");
288 assert_eq!(registry.bindings.len(), 2);
289 assert_eq!(registry.bindings[0].status, "implemented");
290 assert_eq!(registry.bindings[1].status, "not_implemented");
291 }
292
293 #[test]
294 fn test_analyze_bindings_not_implemented() {
295 let dir = tempfile::tempdir().expect("tempdir creation failed");
296 let crate_dir = dir.path().join("aprender");
297 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
298 let binding_path = crate_dir.join("binding.yaml");
299 {
300 let mut f = std::fs::File::create(&binding_path).expect("file open failed");
301 write!(
302 f,
303 r#"
304target_crate: aprender
305bindings:
306 - contract: matmul-kernel-v1.yaml
307 equation: matmul
308 status: not_implemented
309 notes: "Missing"
310"#
311 )
312 .expect("unexpected failure");
313 }
314
315 let findings = analyze_contract_gaps(dir.path(), dir.path());
316 let not_impl = by_title(&findings, "not_implemented");
317 assert!(!not_impl.is_empty());
318 assert_eq!(not_impl[0].severity, FindingSeverity::High);
319 assert!((not_impl[0].suspiciousness - 0.8).abs() < 0.01);
320 }
321
322 #[test]
323 fn test_analyze_bindings_partial() {
324 let dir = tempfile::tempdir().expect("tempdir creation failed");
325 let crate_dir = dir.path().join("test_crate");
326 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
327 let binding_path = crate_dir.join("binding.yaml");
328 {
329 let mut f = std::fs::File::create(&binding_path).expect("file open failed");
330 write!(
331 f,
332 r#"
333target_crate: test_crate
334bindings:
335 - contract: attn-kernel-v1.yaml
336 equation: attention
337 status: partial
338 notes: "Only supports 2D"
339"#
340 )
341 .expect("unexpected failure");
342 }
343
344 let findings = analyze_contract_gaps(dir.path(), dir.path());
345 let partial = by_title(&findings, "partial");
346 assert!(!partial.is_empty());
347 assert_eq!(partial[0].severity, FindingSeverity::Medium);
348 assert!((partial[0].suspiciousness - 0.6).abs() < 0.01);
349 }
350
351 #[test]
352 fn test_discover_explicit_path() {
353 let dir = tempfile::tempdir().expect("tempdir creation failed");
354 let contracts = dir.path().join("my-contracts");
355 std::fs::create_dir_all(&contracts).expect("mkdir failed");
356
357 let result = discover_contracts_dir(dir.path(), Some(&contracts));
358 assert!(result.is_some());
359 assert_eq!(result.expect("operation failed"), contracts);
360 }
361
362 #[test]
363 fn test_discover_explicit_path_missing() {
364 let outer = tempfile::tempdir().expect("tempdir creation failed");
365 std::fs::create_dir(outer.path().join("p")).expect("mkdir failed");
366 let inner = outer.path().join("p");
367 assert!(discover_contracts_dir(&inner, Some(&inner.join("x"))).is_none());
368 }
369
370 #[test]
371 fn test_unbound_contract_detection() {
372 let dir = tempfile::tempdir().expect("tempdir creation failed");
373 let contract_path = dir.path().join("orphan-kernel-v1.yaml");
375 {
376 let mut f = std::fs::File::create(&contract_path).expect("file open failed");
377 write!(
378 f,
379 r#"
380metadata:
381 version: "1.0.0"
382 description: "Orphan kernel"
383proof_obligations: []
384falsification_tests: []
385"#
386 )
387 .expect("unexpected failure");
388 }
389 let findings = analyze_contract_gaps(dir.path(), dir.path());
391 let unbound = by_title(&findings, "Unbound");
392 assert!(!unbound.is_empty());
393 assert_eq!(unbound[0].severity, FindingSeverity::Medium);
394 }
395
396 #[test]
397 fn test_obligation_coverage_low() {
398 let dir = tempfile::tempdir().expect("tempdir creation failed");
399 let contract_path = dir.path().join("test-kernel-v1.yaml");
400 {
401 let mut f = std::fs::File::create(&contract_path).expect("file open failed");
402 write!(
403 f,
404 r#"
405metadata:
406 version: "1.0.0"
407 description: "Test"
408proof_obligations:
409 - type: invariant
410 property: "shape"
411 - type: associativity
412 property: "assoc"
413 - type: linearity
414 property: "linear"
415 - type: equivalence
416 property: "simd"
417falsification_tests:
418 - name: "test_shape"
419"#
420 )
421 .expect("unexpected failure");
422 }
423
424 let findings = analyze_contract_gaps(dir.path(), dir.path());
425 let low_cov = by_title(&findings, "Low obligation coverage");
426 assert!(!low_cov.is_empty());
427 assert_eq!(low_cov[0].severity, FindingSeverity::Low);
428 }
429
430 #[test]
433 fn test_falsify_malformed_binding_yaml() {
434 let dir = tempfile::tempdir().expect("tempdir creation failed");
436 let crate_dir = dir.path().join("broken");
437 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
438 std::fs::write(crate_dir.join("binding.yaml"), "{{{{not valid yaml at all!!!!")
439 .expect("unexpected failure");
440
441 let findings = analyze_contract_gaps(dir.path(), dir.path());
442 let binding_findings = by_title(&findings, "Contract gap:");
444 assert_eq!(binding_findings.len(), 0);
445 }
446
447 #[test]
448 fn test_falsify_malformed_contract_yaml() {
449 let dir = tempfile::tempdir().expect("tempdir creation failed");
451 std::fs::write(dir.path().join("bad-kernel-v1.yaml"), "not: a: valid: contract: [")
452 .expect("unexpected failure");
453
454 let findings = analyze_contract_gaps(dir.path(), dir.path());
455 let unbound = by_title(&findings, "Unbound");
457 assert_eq!(unbound.len(), 1);
458 let obligation = by_title(&findings, "obligation");
459 assert_eq!(obligation.len(), 0);
460 }
461
462 #[test]
463 fn test_falsify_empty_bindings_list() {
464 let dir = tempfile::tempdir().expect("tempdir creation failed");
465 let crate_dir = dir.path().join("empty");
466 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
467 {
468 let mut f =
469 std::fs::File::create(crate_dir.join("binding.yaml")).expect("file open failed");
470 write!(f, "target_crate: empty\nbindings: []\n").expect("write failed");
471 }
472
473 let findings = analyze_contract_gaps(dir.path(), dir.path());
474 let binding_findings = by_title(&findings, "Contract gap:");
475 assert_eq!(binding_findings.len(), 0);
476 }
477
478 #[test]
479 fn test_falsify_obligation_coverage_exact_50pct() {
480 let dir = tempfile::tempdir().expect("tempdir creation failed");
482 let contract_path = dir.path().join("exact50-kernel-v1.yaml");
483 {
484 let mut f = std::fs::File::create(&contract_path).expect("file open failed");
485 write!(
486 f,
487 r#"
488metadata:
489 version: "1.0.0"
490 description: "Boundary test"
491proof_obligations:
492 - type: invariant
493 property: "shape"
494 - type: associativity
495 property: "assoc"
496falsification_tests:
497 - name: "test_shape"
498"#
499 )
500 .expect("unexpected failure");
501 }
502
503 let findings = analyze_contract_gaps(dir.path(), dir.path());
504 let low_cov = by_title(&findings, "Low obligation coverage");
505 assert_eq!(low_cov.len(), 0, "50% is at threshold, not below");
506 }
507
508 #[test]
509 fn test_falsify_obligation_coverage_zero_obligations() {
510 let dir = tempfile::tempdir().expect("tempdir creation failed");
512 let contract_path = dir.path().join("noobs-kernel-v1.yaml");
513 {
514 let mut f = std::fs::File::create(&contract_path).expect("file open failed");
515 write!(
516 f,
517 r#"
518metadata:
519 version: "1.0.0"
520 description: "No obligations"
521proof_obligations: []
522falsification_tests:
523 - name: "test_something"
524"#
525 )
526 .expect("unexpected failure");
527 }
528
529 let findings = analyze_contract_gaps(dir.path(), dir.path());
530 let low_cov = by_title(&findings, "Low obligation coverage");
531 assert_eq!(low_cov.len(), 0, "0 obligations → no coverage finding");
532 }
533
534 #[test]
535 fn test_falsify_bound_contract_still_gets_obligation_check() {
536 let dir = tempfile::tempdir().expect("tempdir creation failed");
538 let contract_path = dir.path().join("matmul-kernel-v1.yaml");
540 {
541 let mut f = std::fs::File::create(&contract_path).expect("file open failed");
542 write!(
543 f,
544 r#"
545metadata:
546 version: "1.0.0"
547 description: "Matmul"
548proof_obligations:
549 - type: invariant
550 property: "shape"
551 - type: associativity
552 property: "assoc"
553 - type: commutativity
554 property: "commute"
555falsification_tests: []
556"#
557 )
558 .expect("unexpected failure");
559 }
560 let crate_dir = dir.path().join("test_crate");
562 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
563 {
564 let mut f =
565 std::fs::File::create(crate_dir.join("binding.yaml")).expect("file open failed");
566 write!(
567 f,
568 "target_crate: test_crate\nbindings:\n - contract: matmul-kernel-v1.yaml\n equation: matmul\n status: implemented\n"
569 )
570 .expect("unexpected failure");
571 }
572
573 let findings = analyze_contract_gaps(dir.path(), dir.path());
574 let unbound = by_title(&findings, "Unbound");
576 assert_eq!(unbound.len(), 0, "Bound contract should not be flagged as unbound");
577 let low_cov = by_title(&findings, "Low obligation coverage");
579 assert_eq!(low_cov.len(), 1, "Bound contract should still get obligation check");
580 }
581
582 #[test]
583 fn test_falsify_discover_nonexistent_parent() {
584 let result = discover_contracts_dir(Path::new("/nonexistent/path/xyz"), None);
585 assert!(result.is_none());
586 }
587
588 #[test]
589 fn test_falsify_implemented_bindings_not_flagged() {
590 let dir = tempfile::tempdir().expect("tempdir creation failed");
592 let crate_dir = dir.path().join("good_crate");
593 std::fs::create_dir_all(&crate_dir).expect("mkdir failed");
594 {
595 let mut f =
596 std::fs::File::create(crate_dir.join("binding.yaml")).expect("file open failed");
597 write!(
598 f,
599 r#"
600target_crate: good_crate
601bindings:
602 - contract: softmax-kernel-v1.yaml
603 equation: softmax
604 status: implemented
605 - contract: matmul-kernel-v1.yaml
606 equation: matmul
607 status: implemented
608"#
609 )
610 .expect("unexpected failure");
611 }
612
613 let findings = analyze_contract_gaps(dir.path(), dir.path());
614 let gaps = by_title(&findings, "Contract gap:");
615 assert_eq!(gaps.len(), 0, "Implemented bindings should not be flagged");
616 }
617
618 #[test]
619 fn test_contract_findings_suspiciousness_values() {
620 let dir = tempfile::tempdir().expect("tempdir creation failed");
622 let binding_dir = dir.path().join("aprender");
623 std::fs::create_dir_all(&binding_dir).expect("mkdir failed");
624 std::fs::write(
625 binding_dir.join("binding.yaml"),
626 r#"
627target_crate: aprender
628bindings:
629 - contract: kernel-v1.yaml
630 equation: eq1
631 status: not_implemented
632 - contract: kernel-v2.yaml
633 equation: eq2
634 status: partial
635"#,
636 )
637 .expect("unexpected failure");
638
639 let findings = analyze_contract_gaps(dir.path(), dir.path());
640 let not_impl = by_title(&findings, "not_implemented");
641 let partial = by_title(&findings, "partial");
642
643 assert!(!not_impl.is_empty(), "Should find not_implemented binding");
644 assert!(!partial.is_empty(), "Should find partial binding");
645
646 assert!(
648 (not_impl[0].suspiciousness - 0.8).abs() < 0.01,
649 "not_implemented should have 0.8 suspiciousness, got {}",
650 not_impl[0].suspiciousness
651 );
652 assert!(
654 (partial[0].suspiciousness - 0.6).abs() < 0.01,
655 "partial should have 0.6 suspiciousness, got {}",
656 partial[0].suspiciousness
657 );
658 }
659}