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