provable_contracts/schema/
types.rs

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

provable_contracts/schema/
types.rs
