provable_contracts/schema/
parser.rs

1use std::path::Path;
2
3use crate::error::ContractError;
4use crate::schema::types::{Contract, CONTRACT_TOP_LEVEL_FIELDS};
5
6/// Parse a YAML contract file into a [`Contract`] struct.
7///
8/// This is the entry point for Phase 2 validation. The parser
9/// deserializes the YAML and performs structural checks.
10///
11/// # Errors
12///
13/// Returns [`ContractError::Io`] if the file cannot be read,
14/// or [`ContractError::Yaml`] if the YAML is malformed.
15pub fn parse_contract(path: &Path) -> Result<Contract, ContractError> {
16    let content = std::fs::read_to_string(path)?;
17    parse_contract_str(&content)
18}
19
20/// Files under `contracts/` that are NOT `Contract` documents.
21///
22/// `contracts/binding.yaml` is a `BindingRegistry` (equation → implementing
23/// function), not a contract. It has no `metadata:` block, so parsing it as a
24/// `Contract` fails with ``missing field `metadata` `` — which is exactly how
25/// `cargo test -p aprender-contracts --test validate_contracts` failed 3 of its
26/// 10 tests on `main` while `pv lint contracts/` reported zero errors: the two
27/// walkers disagreed about what a contract file is.
28const NON_CONTRACT_FILENAMES: [&str; 2] = ["binding.yaml", "binding.yml"];
29
30/// Is `path` a `.yaml` file the contract schema owns?
31///
32/// The single source of truth for "which files under `contracts/` are
33/// contracts". `pv lint`'s directory walker and the `validate_contracts`
34/// integration test both call it, so neither can drift into walking a file the
35/// other skips. Directory-level exclusions (`kaizen/`, `legacy/`,
36/// `pipelines/`, `publish-manifests/`) are a separate concern and stay with the
37/// recursive walker in `lint::gates`.
38#[must_use]
39pub fn is_contract_yaml(path: &Path) -> bool {
40    if path.extension().and_then(|e| e.to_str()) != Some("yaml") {
41        return false;
42    }
43    let Some(name) = path.file_name().and_then(|n| n.to_str()) else {
44        return false;
45    };
46    !name.starts_with('.') && !NON_CONTRACT_FILENAMES.contains(&name)
47}
48
49/// Parse a YAML contract from a string.
50///
51/// Two passes on purpose. `Contract` is intentionally NOT
52/// `#[serde(deny_unknown_fields)]` — 1224 of the 1726 contracts `pv lint`
53/// walks carry a downstream-owned top-level block (`family:`, `sections:`,
54/// `surface:`, …) and denying them would stop ~71% of the corpus from parsing
55/// in one commit. But serde's tolerance is also what let a top-level `kind:`
56/// (119 contracts) and a misspelled `falsification:` block vanish without a
57/// sound. So the second pass reads the raw mapping and records which top-level
58/// keys serde did not consume, in [`Contract::unknown_top_level_keys`]; the
59/// validator turns the never-legitimate ones into errors (SCHEMA-018 /
60/// SCHEMA-019) and leaves the rest alone.
61///
62/// # Errors
63///
64/// Returns [`ContractError::Yaml`] if the YAML is malformed or does not match
65/// the contract schema.
66pub fn parse_contract_str(yaml: &str) -> Result<Contract, ContractError> {
67    let mut contract: Contract = serde_yaml::from_str(yaml)?;
68    contract.unknown_top_level_keys = unknown_top_level_keys(yaml);
69    contract.strict_yaml_error = strict_yaml_error(yaml);
70    Ok(contract)
71}
72
73/// Top-level mapping keys of `yaml` that are not fields of [`Contract`].
74///
75/// Deliberately deserializes into `BTreeMap<String, IgnoredAny>` rather than
76/// `serde_yaml::Value`: `IgnoredAny` drains each value without building it, so
77/// this pass reads ONLY the top-level key names and cannot be derailed by
78/// anything nested. That matters — `contracts/apr-cli-commands-v1.yaml` defines
79/// `subcommands:` twice inside `commands:`, which makes a strict
80/// `serde_yaml::Value` parse fail; capturing keys through `Value` silently
81/// returned "no unknown keys" for that file and its top-level
82/// `kind: CLICommandContract` went unreported. A `BTreeMap` also just
83/// overwrites a duplicate top-level key instead of erroring.
84///
85/// Returns an empty list when the document is not a mapping at all — that case
86/// is already a hard parse error above, so this never masks one.
87fn unknown_top_level_keys(yaml: &str) -> Vec<String> {
88    use serde::de::IgnoredAny;
89    use std::collections::BTreeMap;
90
91    let Ok(map) = serde_yaml::from_str::<BTreeMap<String, IgnoredAny>>(yaml) else {
92        return Vec::new();
93    };
94    map.into_keys()
95        .filter(|k| !CONTRACT_TOP_LEVEL_FIELDS.contains(&k.as_str()))
96        .collect()
97}
98
99/// The error a STRICT reader gets on YAML the contract schema accepted.
100///
101/// `Contract`'s derived deserializer walks only the fields it knows and skips
102/// the rest, so a document can be well-formed to it and malformed to anyone
103/// else. The one shape this catches today is a duplicate mapping key: YAML
104/// requires keys to be unique, and every consumer that builds a real map (a
105/// `serde_yaml::Value`, `yq`, a Python `dict`) keeps exactly one of them and
106/// throws the other away without a word.
107///
108/// `None` means the document round-trips through a strict reader.
109fn strict_yaml_error(yaml: &str) -> Option<String> {
110    serde_yaml::from_str::<serde_yaml::Value>(yaml)
111        .err()
112        .map(|e| e.to_string())
113}
114
115#[cfg(test)]
116mod tests {
117    use super::*;
118
119    const MINIMAL_CONTRACT: &str = r#"
120metadata:
121  version: "1.0.0"
122  description: "Test contract"
123  references:
124    - "Test paper (2024)"
125equations:
126  test_eq:
127    formula: "f(x) = x + 1"
128proof_obligations: []
129falsification_tests: []
130"#;
131
132    #[test]
133    fn parse_minimal_contract() {
134        let contract = parse_contract_str(MINIMAL_CONTRACT).unwrap();
135        assert_eq!(contract.metadata.version, "1.0.0");
136        assert_eq!(contract.metadata.description, "Test contract");
137        assert_eq!(contract.equations.len(), 1);
138        assert!(contract.equations.contains_key("test_eq"));
139    }
140
141    #[test]
142    fn parse_contract_with_all_fields() {
143        let yaml = r#"
144metadata:
145  version: "1.0.0"
146  created: "2026-02-18"
147  author: "Test Author"
148  description: "Full contract"
149  references:
150    - "Paper A (2024)"
151    - "Paper B (2025)"
152equations:
153  softmax:
154    formula: "σ(x)_i = exp(x_i - max(x)) / Σ exp(x_j - max(x))"
155    domain: "x ∈ ℝ^n, n ≥ 1"
156    codomain: "σ(x) ∈ (0,1)^n"
157    invariants:
158      - "sum(output) = 1.0"
159      - "output_i > 0"
160proof_obligations:
161  - type: invariant
162    property: "Output sums to 1"
163    formal: "|sum(softmax(x)) - 1.0| < ε"
164    tolerance: 1.0e-6
165    applies_to: all
166  - type: equivalence
167    property: "SIMD matches scalar"
168    tolerance: 8.0
169    applies_to: simd
170kernel_structure:
171  phases:
172    - name: find_max
173      description: "Find max element"
174      invariant: "max >= all elements"
175    - name: exp_subtract
176      description: "Compute exp(x_i - max)"
177      invariant: "all values in (0, 1]"
178simd_dispatch:
179  softmax:
180    scalar: "softmax_scalar"
181    avx2: "softmax_avx2"
182enforcement:
183  normalization:
184    description: "Output sums to 1.0"
185    check: "contract_tests::FALSIFY-SM-001"
186    severity: "ERROR"
187falsification_tests:
188  - id: FALSIFY-SM-001
189    rule: "Normalization"
190    prediction: "sum(output) ≈ 1.0"
191    test: "proptest with random vectors"
192    if_fails: "Missing max-subtraction trick"
193kani_harnesses:
194  - id: KANI-SM-001
195    obligation: SM-INV-001
196    property: "Softmax sums to 1.0"
197    bound: 16
198    strategy: stub_float
199    solver: cadical
200    harness: verify_softmax_normalization
201qa_gate:
202  id: F-SM-001
203  name: "Softmax Contract"
204  checks:
205    - "normalization"
206  pass_criteria: "All falsification tests pass"
207  falsification: "Introduce off-by-one in max reduction"
208"#;
209
210        let contract = parse_contract_str(yaml).unwrap();
211        assert_eq!(contract.metadata.version, "1.0.0");
212        assert_eq!(contract.metadata.references.len(), 2);
213        assert_eq!(contract.equations.len(), 1);
214        assert_eq!(contract.proof_obligations.len(), 2);
215        assert!(contract.kernel_structure.is_some());
216        let ks = contract.kernel_structure.unwrap();
217        assert_eq!(ks.phases.len(), 2);
218        assert_eq!(contract.simd_dispatch.len(), 1);
219        assert_eq!(contract.enforcement.len(), 1);
220        assert_eq!(contract.falsification_tests.len(), 1);
221        assert_eq!(contract.falsification_tests[0].id, "FALSIFY-SM-001");
222        assert_eq!(contract.kani_harnesses.len(), 1);
223        assert_eq!(contract.kani_harnesses[0].bound, Some(16));
224        assert!(contract.qa_gate.is_some());
225    }
226
227    #[test]
228    fn parse_invalid_yaml_returns_error() {
229        let result = parse_contract_str("not: [valid: yaml: {{");
230        assert!(result.is_err());
231    }
232
233    #[test]
234    fn parse_missing_metadata_returns_error() {
235        let yaml = r#"
236equations:
237  test:
238    formula: "f(x) = x"
239"#;
240        let result = parse_contract_str(yaml);
241        assert!(result.is_err());
242    }
243
244    #[test]
245    fn parse_obligation_types() {
246        let yaml = r#"
247metadata:
248  version: "1.0.0"
249  description: "type test"
250equations:
251  f:
252    formula: "f(x) = x"
253proof_obligations:
254  - type: invariant
255    property: "test"
256    if_fails: ""
257  - type: equivalence
258    property: "test"
259  - type: bound
260    property: "test"
261  - type: monotonicity
262    property: "test"
263  - type: idempotency
264    property: "test"
265  - type: linearity
266    property: "test"
267  - type: symmetry
268    property: "test"
269  - type: associativity
270    property: "test"
271  - type: conservation
272    property: "test"
273falsification_tests: []
274"#;
275        let contract = parse_contract_str(yaml).unwrap();
276        assert_eq!(contract.proof_obligations.len(), 9);
277    }
278
279    #[test]
280    fn parse_dbc_obligation_types() {
281        use crate::schema::types::ObligationType;
282
283        let yaml = r#"
284metadata:
285  version: "1.0.0"
286  description: "DbC type test"
287  depends_on: ["parent-v1"]
288equations:
289  f:
290    formula: "f(x) = x"
291proof_obligations:
292  - type: precondition
293    property: "input finite"
294    formal: "isFinite(x)"
295  - type: postcondition
296    property: "output bounded"
297    requires: "PRE-001"
298  - type: frame
299    property: "input unchanged"
300  - type: loop_invariant
301    property: "max tracks true max"
302    applies_to_phase: "find_max"
303  - type: loop_variant
304    property: "remaining decreasing"
305    applies_to_phase: "accumulate"
306  - type: old_state
307    property: "cache grows"
308  - type: subcontract
309    property: "refines parent"
310    parent_contract: "parent-v1"
311falsification_tests: []
312"#;
313        let contract = parse_contract_str(yaml).unwrap();
314        assert_eq!(contract.proof_obligations.len(), 7);
315        assert_eq!(
316            contract.proof_obligations[0].obligation_type,
317            ObligationType::Precondition
318        );
319        assert_eq!(
320            contract.proof_obligations[1].obligation_type,
321            ObligationType::Postcondition
322        );
323        assert_eq!(
324            contract.proof_obligations[1].requires.as_deref(),
325            Some("PRE-001")
326        );
327        assert_eq!(
328            contract.proof_obligations[2].obligation_type,
329            ObligationType::Frame
330        );
331        assert_eq!(
332            contract.proof_obligations[3].obligation_type,
333            ObligationType::LoopInvariant
334        );
335        assert_eq!(
336            contract.proof_obligations[3].applies_to_phase.as_deref(),
337            Some("find_max")
338        );
339        assert_eq!(
340            contract.proof_obligations[4].obligation_type,
341            ObligationType::LoopVariant
342        );
343        assert_eq!(
344            contract.proof_obligations[5].obligation_type,
345            ObligationType::OldState
346        );
347        assert_eq!(
348            contract.proof_obligations[6].obligation_type,
349            ObligationType::Subcontract
350        );
351        assert_eq!(
352            contract.proof_obligations[6].parent_contract.as_deref(),
353            Some("parent-v1")
354        );
355    }
356
357    #[test]
358    fn parse_contract_with_kind_model_family() {
359        use crate::schema::types::ContractKind;
360
361        // A realistic aprender model-family YAML: metadata + custom
362        // top-level fields. No equations, no proof obligations — should
363        // parse and validate cleanly as kind: model-family.
364        let yaml = r#"
365metadata:
366  version: "1.0.0"
367  description: "Google BERT architecture family metadata"
368  kind: model-family
369  references:
370    - "https://arxiv.org/abs/1810.04805"
371    - "https://huggingface.co/google-bert"
372# Custom top-level fields ignored by the kernel schema,
373# consumed by the downstream crate that owns the file.
374family: bert
375display_name: "Google BERT"
376vendor: Google
377architectures:
378  - BertModel
379  - BertForMaskedLM
380size_variants:
381  base:
382    parameters: "110M"
383    hidden_dim: 768
384"#;
385        let contract = parse_contract_str(yaml).unwrap();
386        assert_eq!(contract.kind(), ContractKind::ModelFamily);
387        assert!(!contract.requires_proofs());
388        assert!(!contract.is_registry());
389        // Validates cleanly — no kernel-specific checks fire.
390        let violations = crate::schema::validate_contract(&contract);
391        let errors: Vec<_> = violations
392            .iter()
393            .filter(|v| v.severity == crate::error::Severity::Error)
394            .collect();
395        assert!(
396            errors.is_empty(),
397            "model-family YAML should validate with no errors, got: {errors:?}",
398        );
399    }
400
401    #[test]
402    fn parse_contract_defaults_to_kernel_kind() {
403        use crate::schema::types::ContractKind;
404
405        let contract = parse_contract_str(MINIMAL_CONTRACT).unwrap();
406        assert_eq!(contract.kind(), ContractKind::Kernel);
407        assert!(contract.requires_proofs());
408    }
409
410    #[test]
411    fn parse_kani_strategies() {
412        use crate::schema::types::KaniStrategy;
413
414        let yaml = r#"
415metadata:
416  version: "1.0.0"
417  description: "kani test"
418equations:
419  f:
420    formula: "f(x) = x"
421kani_harnesses:
422  - id: K1
423    obligation: OBL-1
424    strategy: exhaustive
425  - id: K2
426    obligation: OBL-2
427    strategy: stub_float
428  - id: K3
429    obligation: OBL-3
430    strategy: compositional
431falsification_tests: []
432"#;
433        let contract = parse_contract_str(yaml).unwrap();
434        assert_eq!(contract.kani_harnesses.len(), 3);
435        assert_eq!(
436            contract.kani_harnesses[0].strategy,
437            Some(KaniStrategy::Exhaustive)
438        );
439        assert_eq!(
440            contract.kani_harnesses[1].strategy,
441            Some(KaniStrategy::StubFloat)
442        );
443        assert_eq!(
444            contract.kani_harnesses[2].strategy,
445            Some(KaniStrategy::Compositional)
446        );
447    }
448}
provable_contracts/schema/parser.rs

provable_contracts/schema/
parser.rs
