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    /// IEEE 754 tolerance: codegen emits `>=` instead of `>` for boundaries (GH-67).
158    #[serde(default)]
159    pub float_tolerance: Option<f64>,
160    /// Compositional verification: what this equation requires from upstream.
161    /// References a guarantees block from another contract/equation.
162    #[serde(default)]
163    pub assumes: Option<ShapeContract>,
164    /// Compositional verification: what this equation provides to downstream.
165    /// Must be satisfiable by any downstream equation that assumes it.
166    #[serde(default)]
167    pub guarantees: Option<ShapeContract>,
168}
169
170/// A proof obligation derived from an equation.
171///
172/// 26 obligation types: 19 property types plus 7 Design by Contract
173/// types (`precondition`, `postcondition`, `frame`, `loop_invariant`,
174/// `loop_variant`, `old_state`, `subcontract`).
175#[derive(Debug, Clone, Default, Serialize, Deserialize)]
176pub struct ProofObligation {
177    #[serde(rename = "type")]
178    pub obligation_type: ObligationType,
179    pub property: String,
180    #[serde(default)]
181    pub formal: Option<String>,
182    #[serde(default)]
183    pub tolerance: Option<f64>,
184    #[serde(default)]
185    pub applies_to: Option<AppliesTo>,
186    /// Phase 7: Lean 4 theorem proving metadata.
187    #[serde(default)]
188    pub lean: Option<LeanProof>,
189    /// Postcondition only: links to a precondition obligation ID.
190    #[serde(default)]
191    pub requires: Option<String>,
192    /// Loop invariant/variant only: references a `kernel_structure.phases[]` name.
193    #[serde(default)]
194    pub applies_to_phase: Option<String>,
195    /// Subcontract only: contract stem being refined (must be in `metadata.depends_on`).
196    #[serde(default)]
197    pub parent_contract: Option<String>,
198}
199
200#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)]
201#[serde(rename_all = "lowercase")]
202pub enum ObligationType {
203    #[default]
204    Invariant,
205    Equivalence,
206    Bound,
207    Monotonicity,
208    Idempotency,
209    Linearity,
210    Symmetry,
211    Associativity,
212    Conservation,
213    Ordering,
214    Completeness,
215    Soundness,
216    Involution,
217    Determinism,
218    Roundtrip,
219    #[serde(rename = "state_machine")]
220    StateMachine,
221    Classification,
222    Independence,
223    Termination,
224    // Eiffel DbC types (Meyer 1997)
225    Precondition,
226    Postcondition,
227    Frame,
228    #[serde(rename = "loop_invariant")]
229    LoopInvariant,
230    #[serde(rename = "loop_variant")]
231    LoopVariant,
232    #[serde(rename = "old_state")]
233    OldState,
234    Subcontract,
235}
236
237impl std::fmt::Display for ObligationType {
238    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
239        let s = match self {
240            Self::Invariant => "invariant",
241            Self::Equivalence => "equivalence",
242            Self::Bound => "bound",
243            Self::Monotonicity => "monotonicity",
244            Self::Idempotency => "idempotency",
245            Self::Linearity => "linearity",
246            Self::Symmetry => "symmetry",
247            Self::Associativity => "associativity",
248            Self::Conservation => "conservation",
249            Self::Ordering => "ordering",
250            Self::Completeness => "completeness",
251            Self::Soundness => "soundness",
252            Self::Involution => "involution",
253            Self::Determinism => "determinism",
254            Self::Roundtrip => "roundtrip",
255            Self::StateMachine => "state_machine",
256            Self::Classification => "classification",
257            Self::Independence => "independence",
258            Self::Termination => "termination",
259            Self::Precondition => "precondition",
260            Self::Postcondition => "postcondition",
261            Self::Frame => "frame",
262            Self::LoopInvariant => "loop_invariant",
263            Self::LoopVariant => "loop_variant",
264            Self::OldState => "old_state",
265            Self::Subcontract => "subcontract",
266        };
267        write!(f, "{s}")
268    }
269}
270
271#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
272#[serde(rename_all = "lowercase")]
273pub enum AppliesTo {
274    All,
275    Scalar,
276    Simd,
277    Converter,
278    /// Algorithm-specific target (e.g., "degree", "bce", "huber").
279    #[serde(other)]
280    Other,
281}
282
283/// Kernel phase decomposition.
284#[derive(Debug, Clone, Serialize, Deserialize)]
285pub struct KernelStructure {
286    pub phases: Vec<KernelPhase>,
287}
288
289#[derive(Debug, Clone, Serialize, Deserialize)]
290pub struct KernelPhase {
291    pub name: String,
292    pub description: String,
293    #[serde(default)]
294    pub invariant: Option<String>,
295}
296
297/// An enforcement rule from the contract.
298#[derive(Debug, Clone, Serialize, Deserialize)]
299pub struct EnforcementRule {
300    pub description: String,
301    #[serde(default)]
302    pub check: Option<String>,
303    #[serde(default)]
304    pub severity: Option<String>,
305    #[serde(default)]
306    pub reference: Option<String>,
307}
308
309/// A Popperian falsification test.
310///
311/// Each makes a falsifiable prediction about the implementation.
312/// If the prediction is wrong, the test identifies root cause.
313#[derive(Debug, Clone, Default, Serialize, Deserialize)]
314pub struct FalsificationTest {
315    pub id: String,
316    pub rule: String,
317    pub prediction: String,
318    #[serde(default)]
319    pub test: Option<String>,
320    pub if_fails: String,
321}
322
323/// A Kani bounded model checking harness definition.
324///
325/// Corresponds to Phase 6 (Verify) of the pipeline.
326#[derive(Debug, Clone, Default, Serialize, Deserialize)]
327pub struct KaniHarness {
328    pub id: String,
329    pub obligation: String,
330    #[serde(default)]
331    pub property: Option<String>,
332    #[serde(default)]
333    pub bound: Option<u32>,
334    #[serde(default)]
335    pub strategy: Option<KaniStrategy>,
336    #[serde(default)]
337    pub solver: Option<String>,
338    #[serde(default)]
339    pub harness: Option<String>,
340}
341
342#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
343#[serde(rename_all = "snake_case")]
344pub enum KaniStrategy {
345    Exhaustive,
346    StubFloat,
347    Compositional,
348    BoundedInt,
349}
350
351impl std::fmt::Display for KaniStrategy {
352    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
353        let s = match self {
354            Self::Exhaustive => "exhaustive",
355            Self::StubFloat => "stub_float",
356            Self::Compositional => "compositional",
357            Self::BoundedInt => "bounded_int",
358        };
359        write!(f, "{s}")
360    }
361}
362
363/// Phase 7: Lean 4 theorem proving metadata for a proof obligation.
364#[derive(Debug, Clone, Serialize, Deserialize)]
365pub struct LeanProof {
366    /// Lean 4 theorem name (e.g., `Softmax.partition_of_unity`).
367    pub theorem: String,
368    /// Lean 4 module path (e.g., `ProvableContracts.Softmax`).
369    #[serde(default)]
370    pub module: Option<String>,
371    /// Current status of the Lean proof.
372    #[serde(default)]
373    pub status: LeanStatus,
374    /// Lean-level theorem dependencies.
375    #[serde(default)]
376    pub depends_on: Vec<String>,
377    /// Mathlib import paths required.
378    #[serde(default)]
379    pub mathlib_imports: Vec<String>,
380    /// Free-form notes (e.g., "Proof over reals; f32 gap addressed separately").
381    #[serde(default)]
382    pub notes: Option<String>,
383}
384
385/// Status of a Lean 4 proof.
386#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)]
387#[serde(rename_all = "kebab-case")]
388pub enum LeanStatus {
389    /// Proof is complete and type-checks.
390    Proved,
391    /// Proof uses `sorry` (axiomatized, not yet proved).
392    #[default]
393    Sorry,
394    /// Work in progress.
395    Wip,
396    /// Obligation is not amenable to Lean proof (e.g., performance).
397    NotApplicable,
398}
399
400impl std::fmt::Display for LeanStatus {
401    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
402        let s = match self {
403            Self::Proved => "proved",
404            Self::Sorry => "sorry",
405            Self::Wip => "wip",
406            Self::NotApplicable => "not-applicable",
407        };
408        write!(f, "{s}")
409    }
410}
411
412/// Phase 7: Verification summary across all obligations in a contract.
413#[derive(Debug, Clone, Serialize, Deserialize)]
414pub struct VerificationSummary {
415    pub total_obligations: u32,
416    #[serde(default)]
417    pub l2_property_tested: u32,
418    #[serde(default)]
419    pub l3_kani_proved: u32,
420    #[serde(default)]
421    pub l4_lean_proved: u32,
422    #[serde(default)]
423    pub l4_sorry_count: u32,
424    #[serde(default)]
425    pub l4_not_applicable: u32,
426}
427
428/// QA gate definition for certeza integration.
429#[derive(Debug, Clone, Serialize, Deserialize)]
430pub struct QaGate {
431    pub id: String,
432    pub name: String,
433    #[serde(default)]
434    pub description: Option<String>,
435    #[serde(default)]
436    pub checks: Vec<String>,
437    #[serde(default)]
438    pub pass_criteria: Option<String>,
439    #[serde(default)]
440    pub falsification: Option<String>,
441}
442
443/// A type-level invariant (Meyer's class invariant).
444///
445/// Asserts a predicate that must hold for every instance of `type_name`
446/// at every stable state — after construction and after every public method.
447#[derive(Debug, Clone, Serialize, Deserialize)]
448pub struct TypeInvariant {
449    pub name: String,
450    /// Rust type name (e.g., `ValidatedTensor`).
451    #[serde(rename = "type")]
452    pub type_name: String,
453    /// Rust boolean expression over `self` (e.g., `!self.dims.is_empty()`).
454    pub predicate: String,
455    #[serde(default)]
456    pub description: Option<String>,
457}
458
459/// Coq verification specification for a contract.
460#[derive(Debug, Clone, Serialize, Deserialize)]
461pub struct CoqSpec {
462    /// Coq module name (e.g., `SoftmaxSpec`).
463    pub module: String,
464    /// Coq import statements.
465    #[serde(default)]
466    pub imports: Vec<String>,
467    /// Coq definitions generated from equations.
468    #[serde(default)]
469    pub definitions: Vec<CoqDefinition>,
470    /// Links from proof obligations to Coq lemmas.
471    #[serde(default)]
472    pub obligations: Vec<CoqObligation>,
473}
474
475/// A Coq definition derived from a contract equation.
476#[derive(Debug, Clone, Serialize, Deserialize)]
477pub struct CoqDefinition {
478    pub name: String,
479    pub statement: String,
480}
481
482/// A link between a proof obligation and a Coq lemma.
483#[derive(Debug, Clone, Serialize, Deserialize)]
484pub struct CoqObligation {
485    /// References a proof obligation property or ID.
486    pub links_to: String,
487    /// Coq lemma name.
488    pub coq_lemma: String,
489    /// Current status of the Coq proof.
490    #[serde(default = "coq_status_default")]
491    pub status: String,
492}
493
494fn coq_status_default() -> String {
495    "stub".to_string()
496}
497
498#[cfg(test)]
499#[path = "types_tests.rs"]
500mod tests;
provable_contracts/schema/types.rs

provable_contracts/schema/
types.rs
