Skip to main content

provable_contracts/
binding.rs

1//! Binding registry — maps contract equations to implementations.
2//!
3//! A `BindingRegistry` connects kernel contract equations (defined in
4//! YAML) to the actual Rust functions that implement them in a target
5//! crate (e.g. aprender). This enables:
6//!
7//! - **Audit**: `pv audit --binding` reports which obligations have
8//!   implementations and which are gaps.
9//! - **Wired tests**: `pv probar --binding` generates property tests
10//!   that call real functions instead of `unimplemented!()`.
11
12use std::path::Path;
13
14use serde::{Deserialize, Serialize};
15
16use crate::error::{ContractError, Severity, Violation};
17
18/// Top-level binding registry parsed from YAML.
19#[derive(Debug, Clone, Serialize, Deserialize)]
20pub struct BindingRegistry {
21    pub version: String,
22    pub target_crate: String,
23    /// Developer-declared critical path functions (Section 28).
24    /// CD2 completeness = `critical_path` entries with bindings / len.
25    #[serde(default)]
26    pub critical_path: Vec<String>,
27    #[serde(default)]
28    pub bindings: Vec<KernelBinding>,
29}
30
31/// A single binding: one contract equation mapped to one implementation.
32#[derive(Debug, Clone, Serialize, Deserialize)]
33pub struct KernelBinding {
34    /// Contract YAML filename (e.g. "softmax-kernel-v1.yaml").
35    pub contract: String,
36    /// Equation name within the contract (e.g. "softmax").
37    pub equation: String,
38    /// Full Rust module path (e.g. `aprender::nn::functional::softmax`).
39    #[serde(default)]
40    pub module_path: Option<String>,
41    /// Function or method name.
42    #[serde(default)]
43    pub function: Option<String>,
44    /// Full Rust signature string.
45    #[serde(default)]
46    pub signature: Option<String>,
47    /// Implementation status.
48    pub status: ImplStatus,
49    /// Free-form notes.
50    #[serde(default)]
51    pub notes: Option<String>,
52    /// This entry binds a cuda-oxide `#[kernel]` beside the equation's CPU reference (ONT-4c4, #4069): the
53    /// ontology joins the two by the shared equation. BINDING-006 keys on it, so an equation holds at most one
54    /// reference and one kernel, and [`BindingRegistry::find_binding`] never returns the kernel entry.
55    #[serde(default, skip_serializing_if = "std::ops::Not::not")]
56    pub kernel: bool,
57}
58
59/// Implementation status of a binding.
60#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
61#[serde(rename_all = "snake_case")]
62pub enum ImplStatus {
63    /// Fully implemented and ready for use.
64    Implemented,
65    /// Partially implemented with known gaps.
66    Partial,
67    /// Not yet implemented.
68    NotImplemented,
69    /// Planned but not started — skipped by enforcement checks.
70    Pending,
71}
72
73/// Display implementation status as a `snake_case` string
74impl std::fmt::Display for ImplStatus {
75    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
76        let s = match self {
77            Self::Implemented => "implemented",
78            Self::Partial => "partial",
79            Self::NotImplemented => "not_implemented",
80            Self::Pending => "pending",
81        };
82        write!(f, "{s}")
83    }
84}
85
86/// Parse a binding registry YAML file.
87///
88/// # Errors
89///
90/// Returns [`ContractError::Io`] if the file cannot be read,
91/// or [`ContractError::Yaml`] if the YAML is malformed.
92pub fn parse_binding(path: &Path) -> Result<BindingRegistry, ContractError> {
93    let content = std::fs::read_to_string(path)?;
94    parse_binding_str(&content)
95}
96
97/// Parse a binding registry from a YAML string.
98pub fn parse_binding_str(yaml: &str) -> Result<BindingRegistry, ContractError> {
99    let registry: BindingRegistry = serde_yaml::from_str(yaml)?;
100    Ok(registry)
101}
102
103/// Normalize a contract identifier by stripping `.yaml`/`.yml` extension.
104///
105/// Both binding entries (`contract: foo-v1.yaml`) and file stems (`foo-v1`)
106/// are normalized to the bare stem so comparisons work regardless of whether
107/// the caller used a filename or stem.
108pub fn normalize_contract_id(id: &str) -> &str {
109    id.strip_suffix(".yaml")
110        .or_else(|| id.strip_suffix(".yml"))
111        .unwrap_or(id)
112}
113
114impl BindingRegistry {
115    /// Find all bindings matching a contract (normalizes both sides).
116    pub fn bindings_for(&self, contract_id: &str) -> Vec<&KernelBinding> {
117        let needle = normalize_contract_id(contract_id);
118        self.bindings
119            .iter()
120            .filter(|b| normalize_contract_id(&b.contract) == needle)
121            .collect()
122    }
123
124    /// Find a specific binding by contract + equation (normalizes contract).
125    pub fn find_binding(&self, contract_id: &str, equation: &str) -> Option<&KernelBinding> {
126        let needle = normalize_contract_id(contract_id);
127        self.bindings.iter().find(|b| {
128            !b.kernel && normalize_contract_id(&b.contract) == needle && b.equation == equation
129        })
130    }
131
132    /// L5 verification: return a copy of this registry in which every binding
133    /// marked `implemented` whose `function` is NOT actually defined in the
134    /// source tree under `source_root` is downgraded to `not_implemented`.
135    ///
136    /// This turns the L5 predicate "all bindings **verified** as implemented"
137    /// (see [`crate::proof_status`]) into a fact instead of a self-declared YAML
138    /// flag: a binding only survives as `implemented` if a real `fn <function>`
139    /// exists in source. Rename or delete the function and the binding is
140    /// downgraded, dropping the contract below L5 — the check is falsifiable.
141    ///
142    /// The source tree is scanned once (all `.rs` files, skipping build/vcs
143    /// dirs) and the resulting function-name set is reused for every binding.
144    #[must_use]
145    pub fn verified(&self, source_root: &Path) -> BindingRegistry {
146        let fn_names = collect_fn_names(source_root);
147        let bindings = self
148            .bindings
149            .iter()
150            .map(|b| {
151                let mut b = b.clone();
152                if b.status == ImplStatus::Implemented && !b.function_defined_in(&fn_names) {
153                    b.status = ImplStatus::NotImplemented;
154                }
155                b
156            })
157            .collect();
158        BindingRegistry {
159            version: self.version.clone(),
160            target_crate: self.target_crate.clone(),
161            critical_path: self.critical_path.clone(),
162            bindings,
163        }
164    }
165}
166
167impl KernelBinding {
168    /// True when this binding's `function` is present in the given set of
169    /// function names discovered in source. A binding with no `function` field
170    /// cannot be verified and returns `false`.
171    #[must_use]
172    pub fn function_defined_in(&self, fn_names: &std::collections::HashSet<String>) -> bool {
173        self.function
174            .as_deref()
175            .is_some_and(|f| fn_names.contains(f))
176    }
177}
178
179/// Collect every Rust function name (`fn <name>`) defined in `.rs` files under
180/// `root`, skipping `target/`, `.git/`, `.lake/`, and `node_modules/`. Used by
181/// [`BindingRegistry::verified`] to check bindings point to real code.
182#[must_use]
183pub fn collect_fn_names(root: &Path) -> std::collections::HashSet<String> {
184    let mut names = std::collections::HashSet::new();
185    let mut stack = vec![root.to_path_buf()];
186    while let Some(dir) = stack.pop() {
187        let Ok(entries) = std::fs::read_dir(&dir) else {
188            continue;
189        };
190        for entry in entries.flatten() {
191            let path = entry.path();
192            if path.is_dir() {
193                let skip = matches!(
194                    path.file_name().and_then(|n| n.to_str()),
195                    Some("target" | ".git" | ".lake" | "node_modules")
196                );
197                if !skip {
198                    stack.push(path);
199                }
200            } else if path.extension().is_some_and(|e| e == "rs") {
201                if let Ok(content) = std::fs::read_to_string(&path) {
202                    extract_fn_names(&content, &mut names);
203                }
204            }
205        }
206    }
207    names
208}
209
210/// Extract `fn <name>` identifiers from a Rust source string into `names`.
211fn extract_fn_names(content: &str, names: &mut std::collections::HashSet<String>) {
212    for line in content.lines() {
213        let mut rest = line;
214        while let Some(pos) = rest.find("fn ") {
215            // Require `fn ` to start a word (preceded by start/space) to avoid
216            // matching identifiers like `my_fn `.
217            let ok_boundary = pos == 0
218                || rest[..pos]
219                    .chars()
220                    .next_back()
221                    .is_some_and(|c| !c.is_alphanumeric() && c != '_');
222            let after = &rest[pos + 3..];
223            if ok_boundary {
224                let name: String = after
225                    .chars()
226                    .take_while(|c| c.is_alphanumeric() || *c == '_')
227                    .collect();
228                if !name.is_empty() {
229                    names.insert(name);
230                }
231            }
232            rest = after;
233        }
234    }
235}
236
237/// Validate a binding registry's OWN shape (rules BINDING-001..006).
238///
239/// # Why pv validates its own artifact
240///
241/// `contracts/binding.yaml` and `contracts/aprender/binding.yaml` are pv's
242/// output and pv's input: `pv audit --binding` reports coverage from them and
243/// `pv probar --binding` generates property tests that call the functions they
244/// name. Until now `pv validate` could not read either — both failed with
245/// ``missing field `metadata` ``, because the single-file surface parsed
246/// everything as a `Contract` while `is_contract_yaml` had already excluded
247/// them BY NAME from the directory surface. The tool's own manifest was the
248/// one file it could not check.
249///
250/// The rules below are the ones a registry can be wrong about in a way that
251/// silently degrades a downstream gate: an unnamed target crate, an entry that
252/// binds nothing, two entries claiming the same equation, and — the one that
253/// matters most — a binding that says `implemented` while naming nothing a
254/// reader could go and look at.
255#[must_use]
256pub fn validate_binding_registry(registry: &BindingRegistry) -> Vec<Violation> {
257    let mut violations = Vec::new();
258    let err = |rule: &str, message: String, location: String| Violation {
259        severity: Severity::Error,
260        rule: rule.to_string(),
261        message,
262        location: Some(location),
263    };
264
265    if registry.version.trim().is_empty() {
266        violations.push(err(
267            "BINDING-001",
268            "binding registry has no `version:` — every consumer of this file records \
269             which version of the mapping it audited against"
270                .to_string(),
271            "version".to_string(),
272        ));
273    }
274    if registry.target_crate.trim().is_empty() {
275        violations.push(err(
276            "BINDING-002",
277            "binding registry has no `target_crate:` — a mapping from equations to \
278             functions is meaningless without saying which crate those functions live in"
279                .to_string(),
280            "target_crate".to_string(),
281        ));
282    }
283    if registry.bindings.is_empty() {
284        violations.push(err(
285            "BINDING-003",
286            "binding registry declares no `bindings:` — `pv audit --binding` would \
287             report 0/0 coverage, which reads as clean"
288                .to_string(),
289            "bindings".to_string(),
290        ));
291    }
292
293    let mut seen: std::collections::HashSet<(String, String, bool)> =
294        std::collections::HashSet::new();
295    for (i, binding) in registry.bindings.iter().enumerate() {
296        validate_one_binding(i, binding, &mut seen, &mut violations);
297    }
298    violations
299}
300
301/// BINDING-004/005/006 for a single entry.
302fn validate_one_binding(
303    index: usize,
304    binding: &KernelBinding,
305    seen: &mut std::collections::HashSet<(String, String, bool)>,
306    violations: &mut Vec<Violation>,
307) {
308    let at = |field: &str| format!("bindings[{index}].{field}");
309    let err = |rule: &str, message: String, location: String| Violation {
310        severity: Severity::Error,
311        rule: rule.to_string(),
312        message,
313        location: Some(location),
314    };
315
316    if binding.contract.trim().is_empty() {
317        violations.push(err(
318            "BINDING-004",
319            format!(
320                "bindings[{index}] names no `contract:` — the entry binds an equation to nothing"
321            ),
322            at("contract"),
323        ));
324    }
325    if binding.equation.trim().is_empty() {
326        violations.push(err(
327            "BINDING-004",
328            format!(
329                "bindings[{index}] names no `equation:` — `bindings_for()` matches on the \
330                 contract/equation pair, so an entry without one can never be found"
331            ),
332            at("equation"),
333        ));
334    }
335
336    // BINDING-005: an entry claiming an implementation must name where it is.
337    //
338    // `module_path` + `function` is the usual answer. `notes` is accepted as
339    // the other one because five entries in `contracts/binding.yaml` are
340    // discharged by a shell guard rather than a Rust function
341    // (`scripts/check_pr_review_receipt.sh`) and say so at length. What is
342    // rejected is the entry that claims `implemented` and points at NOTHING —
343    // an implementation claim no reader can go and check.
344    let claims_implementation = matches!(
345        binding.status,
346        ImplStatus::Implemented | ImplStatus::Partial
347    );
348    let names_rust = binding.module_path.is_some() && binding.function.is_some();
349    let names_evidence = binding
350        .notes
351        .as_deref()
352        .is_some_and(|n| !n.trim().is_empty());
353    if claims_implementation && !names_rust && !names_evidence {
354        violations.push(err(
355            "BINDING-005",
356            format!(
357                "bindings[{index}] ({}::{}) is `status: {}` but names neither a \
358                 `module_path:`+`function:` nor any `notes:` saying what discharges it — \
359                 an implementation claim nobody can go and look at",
360                binding.contract, binding.equation, binding.status
361            ),
362            at("status"),
363        ));
364    }
365
366    // BINDING-006: one equation, one binding. `find_binding` returns the FIRST
367    // match, so a duplicate silently decides which implementation is audited.
368    // A `kernel: true` entry is keyed apart: it is the equation's #[kernel], graded
369    // by the kernel shapes against the reference, and `find_binding` skips it.
370    let key = (
371        normalize_contract_id(&binding.contract).to_string(),
372        binding.equation.clone(),
373        binding.kernel,
374    );
375    if !seen.insert(key) {
376        violations.push(err(
377            "BINDING-006",
378            format!(
379                "duplicate binding for {}::{} — `find_binding()` returns the first match, \
380                 so the second entry is audited by nothing and can drift unnoticed",
381                binding.contract, binding.equation
382            ),
383            at("equation"),
384        ));
385    }
386}
387
388#[cfg(test)]
389mod tests {
390    use super::*;
391
392    #[test]
393    fn parse_minimal_binding() {
394        let yaml = r#"
395version: "1.0.0"
396target_crate: aprender
397bindings: []
398"#;
399        let reg = parse_binding_str(yaml).unwrap();
400        assert_eq!(reg.version, "1.0.0");
401        assert_eq!(reg.target_crate, "aprender");
402        assert!(reg.bindings.is_empty());
403    }
404
405    #[test]
406    fn parse_binding_with_entries() {
407        let yaml = r#"
408version: "1.0.0"
409target_crate: aprender
410bindings:
411  - contract: softmax-kernel-v1.yaml
412    equation: softmax
413    module_path: "aprender::nn::functional::softmax"
414    function: softmax
415    signature: "fn softmax(x: &Tensor, dim: i32) -> Tensor"
416    status: implemented
417  - contract: activation-kernel-v1.yaml
418    equation: silu
419    status: not_implemented
420    notes: "Not yet available"
421"#;
422        let reg = parse_binding_str(yaml).unwrap();
423        assert_eq!(reg.bindings.len(), 2);
424        assert_eq!(reg.bindings[0].equation, "softmax");
425        assert_eq!(reg.bindings[0].status, ImplStatus::Implemented);
426        assert!(reg.bindings[0].module_path.is_some());
427        assert_eq!(reg.bindings[1].equation, "silu");
428        assert_eq!(reg.bindings[1].status, ImplStatus::NotImplemented);
429        assert!(reg.bindings[1].module_path.is_none());
430    }
431
432    #[test]
433    fn parse_partial_status() {
434        let yaml = r#"
435version: "1.0.0"
436target_crate: test
437bindings:
438  - contract: test.yaml
439    equation: f
440    module_path: "test::f"
441    function: f
442    status: partial
443    notes: "Only scalar path"
444"#;
445        let reg = parse_binding_str(yaml).unwrap();
446        assert_eq!(reg.bindings[0].status, ImplStatus::Partial);
447    }
448
449    #[test]
450    fn impl_status_display() {
451        assert_eq!(ImplStatus::Implemented.to_string(), "implemented");
452        assert_eq!(ImplStatus::Partial.to_string(), "partial");
453        assert_eq!(ImplStatus::NotImplemented.to_string(), "not_implemented");
454        assert_eq!(ImplStatus::Pending.to_string(), "pending");
455    }
456
457    #[test]
458    fn parse_invalid_binding_yaml() {
459        let result = parse_binding_str("not: [valid: {{");
460        assert!(result.is_err());
461    }
462
463    #[test]
464    fn parse_binding_from_file() {
465        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
466            .join("../../contracts/aprender/binding.yaml");
467        let reg = parse_binding(&path).unwrap();
468        assert_eq!(reg.target_crate, "aprender");
469        assert!(!reg.bindings.is_empty());
470    }
471
472    #[test]
473    fn parse_binding_nonexistent_file() {
474        let result = parse_binding(std::path::Path::new("/nonexistent/binding.yaml"));
475        assert!(result.is_err());
476    }
477
478    // ── L5 binding-verification feature ──
479
480    #[test]
481    fn extract_fn_names_finds_definitions() {
482        let mut names = std::collections::HashSet::new();
483        extract_fn_names(
484            "pub fn to_anthropic(m: &Message) -> Value {\n  async fn helper() {}\n",
485            &mut names,
486        );
487        assert!(names.contains("to_anthropic"));
488        assert!(names.contains("helper"));
489    }
490
491    #[test]
492    fn extract_fn_names_respects_word_boundary() {
493        let mut names = std::collections::HashSet::new();
494        // `my_fn foo` must NOT register `foo` (the `fn ` is inside `my_fn `).
495        extract_fn_names("let my_fn foo = 1;", &mut names);
496        assert!(!names.contains("foo"));
497    }
498
499    #[test]
500    fn function_defined_in_checks_membership() {
501        let names: std::collections::HashSet<String> =
502            ["to_anthropic".to_string()].into_iter().collect();
503        let bound = KernelBinding {
504            contract: "c-v1.yaml".into(),
505            equation: "e".into(),
506            module_path: None,
507            function: Some("to_anthropic".into()),
508            signature: None,
509            status: ImplStatus::Implemented,
510            notes: None,
511            kernel: false,
512        };
513        assert!(bound.function_defined_in(&names));
514
515        let missing = KernelBinding {
516            function: Some("does_not_exist".into()),
517            ..bound.clone()
518        };
519        assert!(!missing.function_defined_in(&names));
520
521        // No function field → cannot be verified.
522        let no_fn = KernelBinding {
523            function: None,
524            ..bound
525        };
526        assert!(!no_fn.function_defined_in(&names));
527    }
528
529    #[test]
530    fn verified_downgrades_phantom_implemented_bindings() {
531        // A temp source tree with exactly one real function.
532        let dir = std::env::temp_dir().join(format!("bindver_{}", std::process::id()));
533        let _ = std::fs::create_dir_all(&dir);
534        std::fs::write(dir.join("lib.rs"), "pub fn real_one() {}\n").unwrap();
535
536        let reg = BindingRegistry {
537            version: "1.0.0".into(),
538            target_crate: "t".into(),
539            critical_path: vec![],
540            bindings: vec![
541                KernelBinding {
542                    contract: "c-v1.yaml".into(),
543                    equation: "a".into(),
544                    module_path: None,
545                    function: Some("real_one".into()),
546                    signature: None,
547                    status: ImplStatus::Implemented,
548                    notes: None,
549                    kernel: false,
550                },
551                KernelBinding {
552                    contract: "c-v1.yaml".into(),
553                    equation: "b".into(),
554                    module_path: None,
555                    function: Some("phantom".into()),
556                    signature: None,
557                    status: ImplStatus::Implemented,
558                    notes: None,
559                    kernel: false,
560                },
561            ],
562        };
563
564        let v = reg.verified(&dir);
565        // Real fn stays implemented; phantom is downgraded.
566        assert_eq!(v.bindings[0].status, ImplStatus::Implemented);
567        assert_eq!(v.bindings[1].status, ImplStatus::NotImplemented);
568        let _ = std::fs::remove_dir_all(&dir);
569    }
570}