Skip to main content

batuta/bug_hunter/
contracts.rs

1//! Contract Verification Gap Analysis (BH-26)
2//!
3//! Analyzes provable-contracts binding registries and contract YAML files
4//! to find verification gaps: unimplemented bindings, partial bindings,
5//! and contracts with insufficient proof obligation coverage.
6
7use super::{DefectCategory, Finding, FindingEvidence, FindingSeverity, HuntMode};
8use serde::Deserialize;
9use std::path::Path;
10
11// ============================================================================
12// Serde types mirroring provable-contracts format (no cross-crate dep)
13// ============================================================================
14
15#[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
57// ============================================================================
58// Public API
59// ============================================================================
60
61/// Discover the provable-contracts directory.
62///
63/// Checks explicit path first, then auto-discovers `../provable-contracts/contracts/`.
64pub 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    // Auto-discover in parent directory (canonicalize to resolve ".")
74    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
84/// Analyze contract verification gaps.
85///
86/// Produces `BH-CONTRACT-NNNN` findings for:
87/// 1. Bindings with status `not_implemented` or `partial`
88/// 2. Contract YAMLs with no binding reference
89/// 3. Contracts where <50% of proof obligations have falsification tests
90pub 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    // Collect bound contract names from all binding registries
96    let mut bound_contracts: std::collections::HashSet<String> = std::collections::HashSet::new();
97
98    // Check 1: Binding gap analysis
99    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    // Check 2: Unbound contracts
107    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            // Check 3: Proof obligation coverage
135            analyze_obligation_coverage(&entry, file_name, &mut findings, &mut finding_id);
136        }
137    }
138
139    findings
140}
141
142// ============================================================================
143// Internal helpers
144// ============================================================================
145
146fn 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 &registry.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    /// Filter findings by title substring — reduces repeated filter chains.
266    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        // Create a contract YAML with no binding
374        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        // No binding.yaml exists, so orphan-kernel-v1.yaml is unbound
390        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    // ===== Falsification tests =====
431
432    #[test]
433    fn test_falsify_malformed_binding_yaml() {
434        // Malformed YAML → gracefully ignored (0 findings from that file)
435        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        // Should not panic, just skip the malformed file
443        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        // Contract YAML with invalid structure → no obligation findings
450        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        // Should get unbound finding but no obligation crash
456        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        // Exactly 50% coverage → should NOT trigger (threshold is <50%)
481        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        // 0 obligations → should NOT trigger (early return)
511        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        // Bound contract with low obligation coverage → BOTH bound + low coverage
537        let dir = tempfile::tempdir().expect("tempdir creation failed");
538        // Create contract with low obligation coverage
539        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        // Create binding that references this contract
561        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        // Should NOT be unbound (it has a binding)
575        let unbound = by_title(&findings, "Unbound");
576        assert_eq!(unbound.len(), 0, "Bound contract should not be flagged as unbound");
577        // SHOULD still get low obligation coverage
578        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        // Bindings with status "implemented" → 0 findings
591        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        // Verify suspiciousness values are set correctly for min_suspiciousness filtering
621        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        // not_implemented = High severity → suspiciousness 0.8
647        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        // partial = Medium severity → suspiciousness 0.6
653        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}