provable_contracts/schema/
parser.rs

1use std::path::Path;
2
3use crate::error::ContractError;
4use crate::schema::types::Contract;
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/// Parse a YAML contract from a string.
21pub fn parse_contract_str(yaml: &str) -> Result<Contract, ContractError> {
22    let contract: Contract = serde_yaml::from_str(yaml)?;
23    Ok(contract)
24}
25
26#[cfg(test)]
27mod tests {
28    use super::*;
29
30    const MINIMAL_CONTRACT: &str = r#"
31metadata:
32  version: "1.0.0"
33  description: "Test contract"
34  references:
35    - "Test paper (2024)"
36equations:
37  test_eq:
38    formula: "f(x) = x + 1"
39proof_obligations: []
40falsification_tests: []
41"#;
42
43    #[test]
44    fn parse_minimal_contract() {
45        let contract = parse_contract_str(MINIMAL_CONTRACT).unwrap();
46        assert_eq!(contract.metadata.version, "1.0.0");
47        assert_eq!(contract.metadata.description, "Test contract");
48        assert_eq!(contract.equations.len(), 1);
49        assert!(contract.equations.contains_key("test_eq"));
50    }
51
52    #[test]
53    fn parse_contract_with_all_fields() {
54        let yaml = r#"
55metadata:
56  version: "1.0.0"
57  created: "2026-02-18"
58  author: "Test Author"
59  description: "Full contract"
60  references:
61    - "Paper A (2024)"
62    - "Paper B (2025)"
63equations:
64  softmax:
65    formula: "σ(x)_i = exp(x_i - max(x)) / Σ exp(x_j - max(x))"
66    domain: "x ∈ ℝ^n, n ≥ 1"
67    codomain: "σ(x) ∈ (0,1)^n"
68    invariants:
69      - "sum(output) = 1.0"
70      - "output_i > 0"
71proof_obligations:
72  - type: invariant
73    property: "Output sums to 1"
74    formal: "|sum(softmax(x)) - 1.0| < ε"
75    tolerance: 1.0e-6
76    applies_to: all
77  - type: equivalence
78    property: "SIMD matches scalar"
79    tolerance: 8.0
80    applies_to: simd
81kernel_structure:
82  phases:
83    - name: find_max
84      description: "Find max element"
85      invariant: "max >= all elements"
86    - name: exp_subtract
87      description: "Compute exp(x_i - max)"
88      invariant: "all values in (0, 1]"
89simd_dispatch:
90  softmax:
91    scalar: "softmax_scalar"
92    avx2: "softmax_avx2"
93enforcement:
94  normalization:
95    description: "Output sums to 1.0"
96    check: "contract_tests::FALSIFY-SM-001"
97    severity: "ERROR"
98falsification_tests:
99  - id: FALSIFY-SM-001
100    rule: "Normalization"
101    prediction: "sum(output) ≈ 1.0"
102    test: "proptest with random vectors"
103    if_fails: "Missing max-subtraction trick"
104kani_harnesses:
105  - id: KANI-SM-001
106    obligation: SM-INV-001
107    property: "Softmax sums to 1.0"
108    bound: 16
109    strategy: stub_float
110    solver: cadical
111    harness: verify_softmax_normalization
112qa_gate:
113  id: F-SM-001
114  name: "Softmax Contract"
115  checks:
116    - "normalization"
117  pass_criteria: "All falsification tests pass"
118  falsification: "Introduce off-by-one in max reduction"
119"#;
120
121        let contract = parse_contract_str(yaml).unwrap();
122        assert_eq!(contract.metadata.version, "1.0.0");
123        assert_eq!(contract.metadata.references.len(), 2);
124        assert_eq!(contract.equations.len(), 1);
125        assert_eq!(contract.proof_obligations.len(), 2);
126        assert!(contract.kernel_structure.is_some());
127        let ks = contract.kernel_structure.unwrap();
128        assert_eq!(ks.phases.len(), 2);
129        assert_eq!(contract.simd_dispatch.len(), 1);
130        assert_eq!(contract.enforcement.len(), 1);
131        assert_eq!(contract.falsification_tests.len(), 1);
132        assert_eq!(contract.falsification_tests[0].id, "FALSIFY-SM-001");
133        assert_eq!(contract.kani_harnesses.len(), 1);
134        assert_eq!(contract.kani_harnesses[0].bound, Some(16));
135        assert!(contract.qa_gate.is_some());
136    }
137
138    #[test]
139    fn parse_invalid_yaml_returns_error() {
140        let result = parse_contract_str("not: [valid: yaml: {{");
141        assert!(result.is_err());
142    }
143
144    #[test]
145    fn parse_missing_metadata_returns_error() {
146        let yaml = r#"
147equations:
148  test:
149    formula: "f(x) = x"
150"#;
151        let result = parse_contract_str(yaml);
152        assert!(result.is_err());
153    }
154
155    #[test]
156    fn parse_obligation_types() {
157        let yaml = r#"
158metadata:
159  version: "1.0.0"
160  description: "type test"
161equations:
162  f:
163    formula: "f(x) = x"
164proof_obligations:
165  - type: invariant
166    property: "test"
167    if_fails: ""
168  - type: equivalence
169    property: "test"
170  - type: bound
171    property: "test"
172  - type: monotonicity
173    property: "test"
174  - type: idempotency
175    property: "test"
176  - type: linearity
177    property: "test"
178  - type: symmetry
179    property: "test"
180  - type: associativity
181    property: "test"
182  - type: conservation
183    property: "test"
184falsification_tests: []
185"#;
186        let contract = parse_contract_str(yaml).unwrap();
187        assert_eq!(contract.proof_obligations.len(), 9);
188    }
189
190    #[test]
191    fn parse_dbc_obligation_types() {
192        use crate::schema::types::ObligationType;
193
194        let yaml = r#"
195metadata:
196  version: "1.0.0"
197  description: "DbC type test"
198  depends_on: ["parent-v1"]
199equations:
200  f:
201    formula: "f(x) = x"
202proof_obligations:
203  - type: precondition
204    property: "input finite"
205    formal: "isFinite(x)"
206  - type: postcondition
207    property: "output bounded"
208    requires: "PRE-001"
209  - type: frame
210    property: "input unchanged"
211  - type: loop_invariant
212    property: "max tracks true max"
213    applies_to_phase: "find_max"
214  - type: loop_variant
215    property: "remaining decreasing"
216    applies_to_phase: "accumulate"
217  - type: old_state
218    property: "cache grows"
219  - type: subcontract
220    property: "refines parent"
221    parent_contract: "parent-v1"
222falsification_tests: []
223"#;
224        let contract = parse_contract_str(yaml).unwrap();
225        assert_eq!(contract.proof_obligations.len(), 7);
226        assert_eq!(
227            contract.proof_obligations[0].obligation_type,
228            ObligationType::Precondition
229        );
230        assert_eq!(
231            contract.proof_obligations[1].obligation_type,
232            ObligationType::Postcondition
233        );
234        assert_eq!(
235            contract.proof_obligations[1].requires.as_deref(),
236            Some("PRE-001")
237        );
238        assert_eq!(
239            contract.proof_obligations[2].obligation_type,
240            ObligationType::Frame
241        );
242        assert_eq!(
243            contract.proof_obligations[3].obligation_type,
244            ObligationType::LoopInvariant
245        );
246        assert_eq!(
247            contract.proof_obligations[3].applies_to_phase.as_deref(),
248            Some("find_max")
249        );
250        assert_eq!(
251            contract.proof_obligations[4].obligation_type,
252            ObligationType::LoopVariant
253        );
254        assert_eq!(
255            contract.proof_obligations[5].obligation_type,
256            ObligationType::OldState
257        );
258        assert_eq!(
259            contract.proof_obligations[6].obligation_type,
260            ObligationType::Subcontract
261        );
262        assert_eq!(
263            contract.proof_obligations[6].parent_contract.as_deref(),
264            Some("parent-v1")
265        );
266    }
267
268    #[test]
269    fn parse_contract_with_kind_model_family() {
270        use crate::schema::types::ContractKind;
271
272        // A realistic aprender model-family YAML: metadata + custom
273        // top-level fields. No equations, no proof obligations — should
274        // parse and validate cleanly as kind: model-family.
275        let yaml = r#"
276metadata:
277  version: "1.0.0"
278  description: "Google BERT architecture family metadata"
279  kind: model-family
280  references:
281    - "https://arxiv.org/abs/1810.04805"
282    - "https://huggingface.co/google-bert"
283# Custom top-level fields ignored by the kernel schema,
284# consumed by the downstream crate that owns the file.
285family: bert
286display_name: "Google BERT"
287vendor: Google
288architectures:
289  - BertModel
290  - BertForMaskedLM
291size_variants:
292  base:
293    parameters: "110M"
294    hidden_dim: 768
295"#;
296        let contract = parse_contract_str(yaml).unwrap();
297        assert_eq!(contract.kind(), ContractKind::ModelFamily);
298        assert!(!contract.requires_proofs());
299        assert!(!contract.is_registry());
300        // Validates cleanly — no kernel-specific checks fire.
301        let violations = crate::schema::validate_contract(&contract);
302        let errors: Vec<_> = violations
303            .iter()
304            .filter(|v| v.severity == crate::error::Severity::Error)
305            .collect();
306        assert!(
307            errors.is_empty(),
308            "model-family YAML should validate with no errors, got: {errors:?}",
309        );
310    }
311
312    #[test]
313    fn parse_contract_defaults_to_kernel_kind() {
314        use crate::schema::types::ContractKind;
315
316        let contract = parse_contract_str(MINIMAL_CONTRACT).unwrap();
317        assert_eq!(contract.kind(), ContractKind::Kernel);
318        assert!(contract.requires_proofs());
319    }
320
321    #[test]
322    fn parse_kani_strategies() {
323        use crate::schema::types::KaniStrategy;
324
325        let yaml = r#"
326metadata:
327  version: "1.0.0"
328  description: "kani test"
329equations:
330  f:
331    formula: "f(x) = x"
332kani_harnesses:
333  - id: K1
334    obligation: OBL-1
335    strategy: exhaustive
336  - id: K2
337    obligation: OBL-2
338    strategy: stub_float
339  - id: K3
340    obligation: OBL-3
341    strategy: compositional
342falsification_tests: []
343"#;
344        let contract = parse_contract_str(yaml).unwrap();
345        assert_eq!(contract.kani_harnesses.len(), 3);
346        assert_eq!(
347            contract.kani_harnesses[0].strategy,
348            Some(KaniStrategy::Exhaustive)
349        );
350        assert_eq!(
351            contract.kani_harnesses[1].strategy,
352            Some(KaniStrategy::StubFloat)
353        );
354        assert_eq!(
355            contract.kani_harnesses[2].strategy,
356            Some(KaniStrategy::Compositional)
357        );
358    }
359}
provable_contracts/schema/parser.rs

provable_contracts/schema/
parser.rs
