provable_contracts/schema/
types.rs

1use serde::{Deserialize, Serialize};
2use std::collections::BTreeMap;
3
4pub use super::composition::{ShapeContract, ShapeExpr};
5pub use super::kind::ContractKind;
6
7/// A complete YAML kernel contract.
8///
9/// This is the root type for the contract schema defined in
10/// `docs/specifications/pv-spec.md` Section 3.
11#[derive(Debug, Clone, Default, Serialize, Deserialize)]
12pub struct Contract {
13    pub metadata: Metadata,
14    /// Equations are optional — kaizen, pipeline, and registry contracts
15    /// may define only `proof_obligations` without mathematical equations.
16    #[serde(default)]
17    pub equations: BTreeMap<String, Equation>,
18    #[serde(default)]
19    pub proof_obligations: Vec<ProofObligation>,
20    #[serde(default)]
21    pub kernel_structure: Option<KernelStructure>,
22    #[serde(default)]
23    pub simd_dispatch: BTreeMap<String, BTreeMap<String, String>>,
24    #[serde(default)]
25    pub enforcement: BTreeMap<String, EnforcementRule>,
26    #[serde(default)]
27    pub falsification_tests: Vec<FalsificationTest>,
28    #[serde(default)]
29    pub kani_harnesses: Vec<KaniHarness>,
30    #[serde(default)]
31    pub qa_gate: Option<QaGate>,
32    /// Phase 7: Lean 4 verification summary across all obligations.
33    #[serde(default)]
34    pub verification_summary: Option<VerificationSummary>,
35    /// Type-level invariants (Meyer's class invariants).
36    #[serde(default)]
37    pub type_invariants: Vec<TypeInvariant>,
38    /// Coq verification specification.
39    #[serde(default)]
40    pub coq_spec: Option<CoqSpec>,
41}
42
43impl Contract {
44    /// Back-compat: `metadata.registry: true` OR `metadata.kind: registry`.
45    pub fn is_registry(&self) -> bool {
46        self.metadata.registry || self.metadata.kind == ContractKind::Registry
47    }
48
49    /// The effective kind, honoring the legacy `registry: true` flag.
50    pub fn kind(&self) -> ContractKind {
51        if self.metadata.registry && self.metadata.kind == ContractKind::Kernel {
52            ContractKind::Registry
53        } else {
54            self.metadata.kind
55        }
56    }
57
58    /// True iff this contract must satisfy PROVABILITY-001 (kernel only).
59    pub fn requires_proofs(&self) -> bool {
60        self.kind() == ContractKind::Kernel
61    }
62
63    /// Enforce the provability invariant: kernel contracts MUST have
64    /// `proof_obligations`, `falsification_tests`, and `kani_harnesses`.
65    /// Returns a list of violations. Empty list = contract is valid.
66    pub fn provability_violations(&self) -> Vec<String> {
67        if !self.requires_proofs() {
68            return vec![];
69        }
70        let mut violations = Vec::new();
71        if self.proof_obligations.is_empty() {
72            violations.push("Kernel contract has no proof_obligations".into());
73        }
74        if self.falsification_tests.is_empty() {
75            violations.push("Kernel contract has no falsification_tests".into());
76        }
77        if self.kani_harnesses.is_empty() {
78            violations.push("Kernel contract has no kani_harnesses".into());
79        }
80        if self.falsification_tests.len() < self.proof_obligations.len() {
81            violations.push(format!(
82                "falsification_tests ({}) < proof_obligations ({})",
83                self.falsification_tests.len(),
84                self.proof_obligations.len(),
85            ));
86        }
87        violations
88    }
89}
90
91/// Contract metadata block.
92#[derive(Debug, Clone, Default, Serialize, Deserialize)]
93pub struct Metadata {
94    pub version: String,
95    #[serde(default)]
96    pub created: Option<String>,
97    #[serde(default)]
98    pub author: Option<String>,
99    pub description: String,
100    #[serde(default)]
101    pub references: Vec<String>,
102    /// Contract dependencies — other contracts this one composes.
103    /// Values are contract stems (e.g. "silu-kernel-v1").
104    #[serde(default)]
105    pub depends_on: Vec<String>,
106    /// Legacy registry flag — prefer `metadata.kind: registry` for new contracts.
107    #[serde(default)]
108    pub registry: bool,
109    /// Contract kind. Defaults to [`ContractKind::Kernel`].
110    #[serde(default)]
111    pub kind: ContractKind,
112    /// Per-contract enforcement level (Section 17, Gap 1).
113    /// `basic` → schema valid; `standard` → + falsification + kani;
114    /// `strict` → + all bindings implemented; `proven` → + Lean 4 proved.
115    #[serde(default)]
116    pub enforcement_level: Option<EnforcementLevel>,
117    /// Once set, the contract cannot drop below this verification level
118    /// without an explicit `pv unlock` (Section 17, Gap 5).
119    #[serde(default)]
120    pub locked_level: Option<String>,
121}
122
123/// Per-contract enforcement level (gradual enforcement, Section 17).
124#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
125#[serde(rename_all = "lowercase")]
126pub enum EnforcementLevel {
127    /// Schema valid, has equations.
128    Basic,
129    /// + falsification tests + Kani harnesses.
130    Standard,
131    /// + all bindings implemented + `#[contract]` annotations.
132    Strict,
133    /// + Lean 4 proved (no sorry).
134    Proven,
135}
136
137/// A mathematical equation extracted from a paper (Phase 1 output).
138#[derive(Debug, Clone, Default, Serialize, Deserialize)]
139pub struct Equation {
140    pub formula: String,
141    #[serde(default)]
142    pub domain: Option<String>,
143    #[serde(default)]
144    pub codomain: Option<String>,
145    #[serde(default)]
146    pub invariants: Vec<String>,
147    /// Rust preconditions — compiled to `debug_assert!()` by `build.rs`.
148    #[serde(default)]
149    pub preconditions: Vec<String>,
150    /// Rust postconditions — compiled to `debug_assert!()` by `build.rs`.
151    #[serde(default)]
152    pub postconditions: Vec<String>,
153    /// Lean 4 theorem name that proves this equation correct.
154    /// Example: "ProvableContracts.Theorems.Softmax.PartitionOfUnity"
155    #[serde(default)]
156    pub lean_theorem: Option<String>,
157    /// Compositional verification: what this equation requires from upstream.
158    /// References a guarantees block from another contract/equation.
159    #[serde(default)]
160    pub assumes: Option<ShapeContract>,
161    /// Compositional verification: what this equation provides to downstream.
162    /// Must be satisfiable by any downstream equation that assumes it.
163    #[serde(default)]
164    pub guarantees: Option<ShapeContract>,
165}
166
167/// A proof obligation derived from an equation.
168///
169/// 26 obligation types: 19 property types plus 7 Design by Contract
170/// types (`precondition`, `postcondition`, `frame`, `loop_invariant`,
171/// `loop_variant`, `old_state`, `subcontract`).
172#[derive(Debug, Clone, Default, Serialize, Deserialize)]
173pub struct ProofObligation {
174    #[serde(rename = "type")]
175    pub obligation_type: ObligationType,
176    pub property: String,
177    #[serde(default)]
178    pub formal: Option<String>,
179    #[serde(default)]
180    pub tolerance: Option<f64>,
181    #[serde(default)]
182    pub applies_to: Option<AppliesTo>,
183    /// Phase 7: Lean 4 theorem proving metadata.
184    #[serde(default)]
185    pub lean: Option<LeanProof>,
186    /// Postcondition only: links to a precondition obligation ID.
187    #[serde(default)]
188    pub requires: Option<String>,
189    /// Loop invariant/variant only: references a `kernel_structure.phases[]` name.
190    #[serde(default)]
191    pub applies_to_phase: Option<String>,
192    /// Subcontract only: contract stem being refined (must be in `metadata.depends_on`).
193    #[serde(default)]
194    pub parent_contract: Option<String>,
195}
196
197#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)]
198#[serde(rename_all = "lowercase")]
199pub enum ObligationType {
200    #[default]
201    Invariant,
202    Equivalence,
203    Bound,
204    Monotonicity,
205    Idempotency,
206    Linearity,
207    Symmetry,
208    Associativity,
209    Conservation,
210    Ordering,
211    Completeness,
212    Soundness,
213    Involution,
214    Determinism,
215    Roundtrip,
216    #[serde(rename = "state_machine")]
217    StateMachine,
218    Classification,
219    Independence,
220    Termination,
221    // Eiffel DbC types (Meyer 1997)
222    Precondition,
223    Postcondition,
224    Frame,
225    #[serde(rename = "loop_invariant")]
226    LoopInvariant,
227    #[serde(rename = "loop_variant")]
228    LoopVariant,
229    #[serde(rename = "old_state")]
230    OldState,
231    Subcontract,
232}
233
234impl std::fmt::Display for ObligationType {
235    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
236        let s = match self {
237            Self::Invariant => "invariant",
238            Self::Equivalence => "equivalence",
239            Self::Bound => "bound",
240            Self::Monotonicity => "monotonicity",
241            Self::Idempotency => "idempotency",
242            Self::Linearity => "linearity",
243            Self::Symmetry => "symmetry",
244            Self::Associativity => "associativity",
245            Self::Conservation => "conservation",
246            Self::Ordering => "ordering",
247            Self::Completeness => "completeness",
248            Self::Soundness => "soundness",
249            Self::Involution => "involution",
250            Self::Determinism => "determinism",
251            Self::Roundtrip => "roundtrip",
252            Self::StateMachine => "state_machine",
253            Self::Classification => "classification",
254            Self::Independence => "independence",
255            Self::Termination => "termination",
256            Self::Precondition => "precondition",
257            Self::Postcondition => "postcondition",
258            Self::Frame => "frame",
259            Self::LoopInvariant => "loop_invariant",
260            Self::LoopVariant => "loop_variant",
261            Self::OldState => "old_state",
262            Self::Subcontract => "subcontract",
263        };
264        write!(f, "{s}")
265    }
266}
267
268#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
269#[serde(rename_all = "lowercase")]
270pub enum AppliesTo {
271    All,
272    Scalar,
273    Simd,
274    Converter,
275    /// Algorithm-specific target (e.g., "degree", "bce", "huber").
276    #[serde(other)]
277    Other,
278}
279
280/// Kernel phase decomposition.
281#[derive(Debug, Clone, Serialize, Deserialize)]
282pub struct KernelStructure {
283    pub phases: Vec<KernelPhase>,
284}
285
286#[derive(Debug, Clone, Serialize, Deserialize)]
287pub struct KernelPhase {
288    pub name: String,
289    pub description: String,
290    #[serde(default)]
291    pub invariant: Option<String>,
292}
293
294/// An enforcement rule from the contract.
295#[derive(Debug, Clone, Serialize, Deserialize)]
296pub struct EnforcementRule {
297    pub description: String,
298    #[serde(default)]
299    pub check: Option<String>,
300    #[serde(default)]
301    pub severity: Option<String>,
302    #[serde(default)]
303    pub reference: Option<String>,
304}
305
306/// A Popperian falsification test.
307///
308/// Each makes a falsifiable prediction about the implementation.
309/// If the prediction is wrong, the test identifies root cause.
310#[derive(Debug, Clone, Default, Serialize, Deserialize)]
311pub struct FalsificationTest {
312    pub id: String,
313    pub rule: String,
314    pub prediction: String,
315    #[serde(default)]
316    pub test: Option<String>,
317    pub if_fails: String,
318}
319
320/// A Kani bounded model checking harness definition.
321///
322/// Corresponds to Phase 6 (Verify) of the pipeline.
323#[derive(Debug, Clone, Default, Serialize, Deserialize)]
324pub struct KaniHarness {
325    pub id: String,
326    pub obligation: String,
327    #[serde(default)]
328    pub property: Option<String>,
329    #[serde(default)]
330    pub bound: Option<u32>,
331    #[serde(default)]
332    pub strategy: Option<KaniStrategy>,
333    #[serde(default)]
334    pub solver: Option<String>,
335    #[serde(default)]
336    pub harness: Option<String>,
337}
338
339#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
340#[serde(rename_all = "snake_case")]
341pub enum KaniStrategy {
342    Exhaustive,
343    StubFloat,
344    Compositional,
345    BoundedInt,
346}
347
348impl std::fmt::Display for KaniStrategy {
349    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
350        let s = match self {
351            Self::Exhaustive => "exhaustive",
352            Self::StubFloat => "stub_float",
353            Self::Compositional => "compositional",
354            Self::BoundedInt => "bounded_int",
355        };
356        write!(f, "{s}")
357    }
358}
359
360/// Phase 7: Lean 4 theorem proving metadata for a proof obligation.
361#[derive(Debug, Clone, Serialize, Deserialize)]
362pub struct LeanProof {
363    /// Lean 4 theorem name (e.g., `Softmax.partition_of_unity`).
364    pub theorem: String,
365    /// Lean 4 module path (e.g., `ProvableContracts.Softmax`).
366    #[serde(default)]
367    pub module: Option<String>,
368    /// Current status of the Lean proof.
369    #[serde(default)]
370    pub status: LeanStatus,
371    /// Lean-level theorem dependencies.
372    #[serde(default)]
373    pub depends_on: Vec<String>,
374    /// Mathlib import paths required.
375    #[serde(default)]
376    pub mathlib_imports: Vec<String>,
377    /// Free-form notes (e.g., "Proof over reals; f32 gap addressed separately").
378    #[serde(default)]
379    pub notes: Option<String>,
380}
381
382/// Status of a Lean 4 proof.
383#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)]
384#[serde(rename_all = "kebab-case")]
385pub enum LeanStatus {
386    /// Proof is complete and type-checks.
387    Proved,
388    /// Proof uses `sorry` (axiomatized, not yet proved).
389    #[default]
390    Sorry,
391    /// Work in progress.
392    Wip,
393    /// Obligation is not amenable to Lean proof (e.g., performance).
394    NotApplicable,
395}
396
397impl std::fmt::Display for LeanStatus {
398    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
399        let s = match self {
400            Self::Proved => "proved",
401            Self::Sorry => "sorry",
402            Self::Wip => "wip",
403            Self::NotApplicable => "not-applicable",
404        };
405        write!(f, "{s}")
406    }
407}
408
409/// Phase 7: Verification summary across all obligations in a contract.
410#[derive(Debug, Clone, Serialize, Deserialize)]
411pub struct VerificationSummary {
412    pub total_obligations: u32,
413    #[serde(default)]
414    pub l2_property_tested: u32,
415    #[serde(default)]
416    pub l3_kani_proved: u32,
417    #[serde(default)]
418    pub l4_lean_proved: u32,
419    #[serde(default)]
420    pub l4_sorry_count: u32,
421    #[serde(default)]
422    pub l4_not_applicable: u32,
423}
424
425/// QA gate definition for certeza integration.
426#[derive(Debug, Clone, Serialize, Deserialize)]
427pub struct QaGate {
428    pub id: String,
429    pub name: String,
430    #[serde(default)]
431    pub description: Option<String>,
432    #[serde(default)]
433    pub checks: Vec<String>,
434    #[serde(default)]
435    pub pass_criteria: Option<String>,
436    #[serde(default)]
437    pub falsification: Option<String>,
438}
439
440/// A type-level invariant (Meyer's class invariant).
441///
442/// Asserts a predicate that must hold for every instance of `type_name`
443/// at every stable state — after construction and after every public method.
444#[derive(Debug, Clone, Serialize, Deserialize)]
445pub struct TypeInvariant {
446    pub name: String,
447    /// Rust type name (e.g., `ValidatedTensor`).
448    #[serde(rename = "type")]
449    pub type_name: String,
450    /// Rust boolean expression over `self` (e.g., `!self.dims.is_empty()`).
451    pub predicate: String,
452    #[serde(default)]
453    pub description: Option<String>,
454}
455
456/// Coq verification specification for a contract.
457#[derive(Debug, Clone, Serialize, Deserialize)]
458pub struct CoqSpec {
459    /// Coq module name (e.g., `SoftmaxSpec`).
460    pub module: String,
461    /// Coq import statements.
462    #[serde(default)]
463    pub imports: Vec<String>,
464    /// Coq definitions generated from equations.
465    #[serde(default)]
466    pub definitions: Vec<CoqDefinition>,
467    /// Links from proof obligations to Coq lemmas.
468    #[serde(default)]
469    pub obligations: Vec<CoqObligation>,
470}
471
472/// A Coq definition derived from a contract equation.
473#[derive(Debug, Clone, Serialize, Deserialize)]
474pub struct CoqDefinition {
475    pub name: String,
476    pub statement: String,
477}
478
479/// A link between a proof obligation and a Coq lemma.
480#[derive(Debug, Clone, Serialize, Deserialize)]
481pub struct CoqObligation {
482    /// References a proof obligation property or ID.
483    pub links_to: String,
484    /// Coq lemma name.
485    pub coq_lemma: String,
486    /// Current status of the Coq proof.
487    #[serde(default = "coq_status_default")]
488    pub status: String,
489}
490
491fn coq_status_default() -> String {
492    "stub".to_string()
493}
494
495#[cfg(test)]
496#[path = "types_tests.rs"]
497mod tests;
provable_contracts/schema/types.rs

provable_contracts/schema/
types.rs
