provable_contracts/schema/
validator.rs

1use std::collections::HashSet;
2
3use crate::error::{Severity, Violation};
4use crate::schema::types::{Contract, ContractKind};
5
6/// Validate a parsed contract for completeness and consistency.
7///
8/// Returns a list of violations. If any violation has
9/// [`Severity::Error`], the contract is considered invalid.
10///
11/// Validation is kind-aware: non-kernel contracts (registries, model-family
12/// schemas, reference documents) are validated only for metadata consistency;
13/// the provability invariant, equations, and proof/kani/falsification checks
14/// only apply to `ContractKind::Kernel`.
15pub fn validate_contract(contract: &Contract) -> Vec<Violation> {
16    let mut violations = Vec::new();
17
18    validate_metadata(contract, &mut violations);
19
20    // Kernel-only checks: these enforce the provability invariant and
21    // require equations + proof obligations + tests + Kani harnesses.
22    if contract.kind() == ContractKind::Kernel && !contract.is_registry() {
23        validate_equations(contract, &mut violations);
24        validate_provability_invariant(contract, &mut violations);
25        validate_proof_obligations(contract, &mut violations);
26        validate_falsification_tests(contract, &mut violations);
27        validate_kani_harnesses(contract, &mut violations);
28        validate_qa_gate(contract, &mut violations);
29    } else {
30        // Non-kernel kinds (registry, model-family, schema): still validate
31        // any proof obligations/falsification/kani data that IS present, so
32        // mistakes are caught even on exempt contracts.
33        validate_proof_obligations(contract, &mut violations);
34        validate_falsification_tests(contract, &mut violations);
35        validate_kani_harnesses(contract, &mut violations);
36    }
37
38    violations
39}
40
41/// Enforce the provability invariant: kernel contracts (non-registry) MUST have
42/// `proof_obligations`, `falsification_tests`, and `kani_harnesses`.
43fn validate_provability_invariant(contract: &Contract, violations: &mut Vec<Violation>) {
44    for v in contract.provability_violations() {
45        violations.push(Violation {
46            severity: Severity::Error,
47            rule: "PROVABILITY-001".to_string(),
48            message: v,
49            location: None,
50        });
51    }
52}
53
54fn validate_metadata(contract: &Contract, violations: &mut Vec<Violation>) {
55    if contract.metadata.references.is_empty() {
56        violations.push(Violation {
57            severity: Severity::Error,
58            rule: "SCHEMA-001".to_string(),
59            message: "metadata.references must not be empty — \
60                      every contract must cite its source paper(s)"
61                .to_string(),
62            location: Some("metadata.references".to_string()),
63        });
64    }
65
66    if contract.metadata.version.is_empty() {
67        violations.push(Violation {
68            severity: Severity::Error,
69            rule: "SCHEMA-002".to_string(),
70            message: "metadata.version must not be empty".to_string(),
71            location: Some("metadata.version".to_string()),
72        });
73    }
74}
75
76fn validate_equations(contract: &Contract, violations: &mut Vec<Violation>) {
77    if contract.equations.is_empty() {
78        violations.push(Violation {
79            severity: Severity::Error,
80            rule: "SCHEMA-003".to_string(),
81            message: "equations must contain at least one equation".to_string(),
82            location: Some("equations".to_string()),
83        });
84    }
85
86    for (name, eq) in &contract.equations {
87        if eq.formula.is_empty() {
88            violations.push(Violation {
89                severity: Severity::Error,
90                rule: "SCHEMA-004".to_string(),
91                message: format!("equations.{name}.formula must not be empty"),
92                location: Some(format!("equations.{name}.formula")),
93            });
94        }
95    }
96}
97
98fn validate_proof_obligations(contract: &Contract, violations: &mut Vec<Violation>) {
99    use crate::schema::types::ObligationType;
100
101    let mut seen_ids = HashSet::new();
102    for (i, ob) in contract.proof_obligations.iter().enumerate() {
103        if ob.property.is_empty() {
104            violations.push(Violation {
105                severity: Severity::Error,
106                rule: "SCHEMA-005".to_string(),
107                message: format!("proof_obligations[{i}].property must not be empty"),
108                location: Some(format!("proof_obligations[{i}].property")),
109            });
110        }
111        if let Some(ref formal) = ob.formal {
112            if !seen_ids.insert(formal.clone()) {
113                violations.push(Violation {
114                    severity: Severity::Warning,
115                    rule: "SCHEMA-006".to_string(),
116                    message: format!("Duplicate formal predicate: {formal}"),
117                    location: Some(format!("proof_obligations[{i}].formal")),
118                });
119            }
120        }
121
122        // DbC field/type constraints
123        if ob.requires.is_some() && ob.obligation_type != ObligationType::Postcondition {
124            violations.push(Violation {
125                severity: Severity::Error,
126                rule: "SCHEMA-014".to_string(),
127                message: format!(
128                    "proof_obligations[{i}].requires is only valid on \
129                     postcondition obligations (found on {})",
130                    ob.obligation_type
131                ),
132                location: Some(format!("proof_obligations[{i}].requires")),
133            });
134        }
135
136        if ob.applies_to_phase.is_some()
137            && ob.obligation_type != ObligationType::LoopInvariant
138            && ob.obligation_type != ObligationType::LoopVariant
139        {
140            violations.push(Violation {
141                severity: Severity::Error,
142                rule: "SCHEMA-015".to_string(),
143                message: format!(
144                    "proof_obligations[{i}].applies_to_phase is only valid on \
145                     loop_invariant or loop_variant obligations (found on {})",
146                    ob.obligation_type
147                ),
148                location: Some(format!("proof_obligations[{i}].applies_to_phase")),
149            });
150        }
151
152        if ob.parent_contract.is_some() && ob.obligation_type != ObligationType::Subcontract {
153            violations.push(Violation {
154                severity: Severity::Error,
155                rule: "SCHEMA-016".to_string(),
156                message: format!(
157                    "proof_obligations[{i}].parent_contract is only valid on \
158                     subcontract obligations (found on {})",
159                    ob.obligation_type
160                ),
161                location: Some(format!("proof_obligations[{i}].parent_contract")),
162            });
163        }
164
165        // Subcontract parent_contract must be in depends_on
166        if let Some(ref parent) = ob.parent_contract {
167            if ob.obligation_type == ObligationType::Subcontract
168                && !contract.metadata.depends_on.contains(parent)
169            {
170                violations.push(Violation {
171                    severity: Severity::Error,
172                    rule: "SCHEMA-017".to_string(),
173                    message: format!(
174                        "proof_obligations[{i}].parent_contract \"{parent}\" \
175                         must be listed in metadata.depends_on"
176                    ),
177                    location: Some(format!("proof_obligations[{i}].parent_contract")),
178                });
179            }
180        }
181    }
182}
183
184fn validate_falsification_tests(contract: &Contract, violations: &mut Vec<Violation>) {
185    let mut ids = HashSet::new();
186    for test in &contract.falsification_tests {
187        if !ids.insert(&test.id) {
188            violations.push(Violation {
189                severity: Severity::Error,
190                rule: "SCHEMA-007".to_string(),
191                message: format!("Duplicate falsification test ID: {}", test.id),
192                location: Some(format!("falsification_tests.{}", test.id)),
193            });
194        }
195        if test.prediction.is_empty() {
196            violations.push(Violation {
197                severity: Severity::Error,
198                rule: "SCHEMA-008".to_string(),
199                message: format!(
200                    "falsification_tests.{}.prediction must not be empty — \
201                     every test must make a falsifiable prediction",
202                    test.id
203                ),
204                location: Some(format!("falsification_tests.{}.prediction", test.id)),
205            });
206        }
207        if test.if_fails.is_empty() {
208            violations.push(Violation {
209                severity: Severity::Warning,
210                rule: "SCHEMA-009".to_string(),
211                message: format!(
212                    "falsification_tests.{}.if_fails is empty — \
213                     should describe root cause diagnosis",
214                    test.id
215                ),
216                location: Some(format!("falsification_tests.{}.if_fails", test.id)),
217            });
218        }
219    }
220}
221
222fn validate_kani_harnesses(contract: &Contract, violations: &mut Vec<Violation>) {
223    let mut ids = HashSet::new();
224    for harness in &contract.kani_harnesses {
225        if !ids.insert(&harness.id) {
226            violations.push(Violation {
227                severity: Severity::Error,
228                rule: "SCHEMA-010".to_string(),
229                message: format!("Duplicate Kani harness ID: {}", harness.id),
230                location: Some(format!("kani_harnesses.{}", harness.id)),
231            });
232        }
233        if harness.obligation.is_empty() {
234            violations.push(Violation {
235                severity: Severity::Error,
236                rule: "SCHEMA-011".to_string(),
237                message: format!(
238                    "kani_harnesses.{}.obligation must not be empty — \
239                     every harness must reference a proof obligation",
240                    harness.id
241                ),
242                location: Some(format!("kani_harnesses.{}.obligation", harness.id)),
243            });
244        }
245        if harness.bound.is_none() {
246            violations.push(Violation {
247                severity: Severity::Warning,
248                rule: "SCHEMA-012".to_string(),
249                message: format!(
250                    "kani_harnesses.{}.bound not specified — \
251                     Kani requires an unwind bound",
252                    harness.id
253                ),
254                location: Some(format!("kani_harnesses.{}.bound", harness.id)),
255            });
256        }
257    }
258}
259
260fn validate_qa_gate(contract: &Contract, violations: &mut Vec<Violation>) {
261    if contract.qa_gate.is_none() {
262        violations.push(Violation {
263            severity: Severity::Warning,
264            rule: "SCHEMA-013".to_string(),
265            message: "No qa_gate defined — contract should define a \
266                      certeza quality gate"
267                .to_string(),
268            location: Some("qa_gate".to_string()),
269        });
270    }
271}
272
273#[cfg(test)]
274mod tests {
275    include!("validator_tests.rs");
276}
provable_contracts/schema/validator.rs

provable_contracts/schema/
validator.rs
