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    ///
17    /// Accepts both map form (`equations: { silu: { formula: ... } }`, the
18    /// canonical schema) and sequence form (`equations: [{ id: silu,
19    /// formula: ... }]`, used by several diagnostic/methodology contracts
20    /// predating APR-MONO). The sequence form promotes each item's `id`
21    /// field to the map key.
22    #[serde(default, deserialize_with = "deserialize_equations")]
23    pub equations: BTreeMap<String, Equation>,
24    #[serde(default)]
25    pub proof_obligations: Vec<ProofObligation>,
26    #[serde(default)]
27    pub kernel_structure: Option<KernelStructure>,
28    #[serde(default)]
29    pub simd_dispatch: BTreeMap<String, BTreeMap<String, String>>,
30    #[serde(default)]
31    pub enforcement: BTreeMap<String, EnforcementRule>,
32    #[serde(default)]
33    pub falsification_tests: Vec<FalsificationTest>,
34    #[serde(default)]
35    pub kani_harnesses: Vec<KaniHarness>,
36    #[serde(default)]
37    pub qa_gate: Option<QaGate>,
38    /// Phase 7: Lean 4 verification summary across all obligations.
39    #[serde(default)]
40    pub verification_summary: Option<VerificationSummary>,
41    /// Type-level invariants (Meyer's class invariants).
42    #[serde(default)]
43    pub type_invariants: Vec<TypeInvariant>,
44    /// Coq verification specification.
45    #[serde(default)]
46    pub coq_spec: Option<CoqSpec>,
47}
48
49impl Contract {
50    /// Back-compat: `metadata.registry: true` OR `metadata.kind: registry`.
51    pub fn is_registry(&self) -> bool {
52        self.metadata.registry || self.metadata.kind == ContractKind::Registry
53    }
54
55    /// The effective kind, honoring the legacy `registry: true` flag.
56    pub fn kind(&self) -> ContractKind {
57        if self.metadata.registry && self.metadata.kind == ContractKind::Kernel {
58            ContractKind::Registry
59        } else {
60            self.metadata.kind
61        }
62    }
63
64    /// True iff this contract must satisfy PROVABILITY-001 (kernel only).
65    pub fn requires_proofs(&self) -> bool {
66        self.kind() == ContractKind::Kernel
67    }
68
69    /// Enforce the provability invariant: kernel contracts MUST have
70    /// `proof_obligations`, `falsification_tests`, and `kani_harnesses`.
71    /// Returns a list of violations. Empty list = contract is valid.
72    pub fn provability_violations(&self) -> Vec<String> {
73        if !self.requires_proofs() {
74            return vec![];
75        }
76        let mut violations = Vec::new();
77        if self.proof_obligations.is_empty() {
78            violations.push("Kernel contract has no proof_obligations".into());
79        }
80        if self.falsification_tests.is_empty() {
81            violations.push("Kernel contract has no falsification_tests".into());
82        }
83        if self.kani_harnesses.is_empty() {
84            violations.push("Kernel contract has no kani_harnesses".into());
85        }
86        if self.falsification_tests.len() < self.proof_obligations.len() {
87            violations.push(format!(
88                "falsification_tests ({}) < proof_obligations ({})",
89                self.falsification_tests.len(),
90                self.proof_obligations.len(),
91            ));
92        }
93        violations
94    }
95}
96
97/// Contract metadata block.
98#[derive(Debug, Clone, Default, Serialize, Deserialize)]
99pub struct Metadata {
100    pub version: String,
101    #[serde(default)]
102    pub created: Option<String>,
103    #[serde(default)]
104    pub author: Option<String>,
105    pub description: String,
106    #[serde(default)]
107    pub references: Vec<String>,
108    /// Contract dependencies — other contracts this one composes.
109    /// Values are contract stems (e.g. "silu-kernel-v1").
110    #[serde(default)]
111    pub depends_on: Vec<String>,
112    /// Legacy registry flag — prefer `metadata.kind: registry` for new contracts.
113    #[serde(default)]
114    pub registry: bool,
115    /// Contract kind. Defaults to [`ContractKind::Kernel`].
116    #[serde(default)]
117    pub kind: ContractKind,
118    /// Per-contract enforcement level (Section 17, Gap 1).
119    /// `basic` → schema valid; `standard` → + falsification + kani;
120    /// `strict` → + all bindings implemented; `proven` → + Lean 4 proved.
121    #[serde(default)]
122    pub enforcement_level: Option<EnforcementLevel>,
123    /// Once set, the contract cannot drop below this verification level
124    /// without an explicit `pv unlock` (Section 17, Gap 5).
125    #[serde(default)]
126    pub locked_level: Option<String>,
127}
128
129/// Per-contract enforcement level (gradual enforcement, Section 17).
130#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
131#[serde(rename_all = "lowercase")]
132pub enum EnforcementLevel {
133    /// Schema valid, has equations.
134    Basic,
135    /// + falsification tests + Kani harnesses.
136    Standard,
137    /// + all bindings implemented + `#[contract]` annotations.
138    Strict,
139    /// + Lean 4 proved (no sorry).
140    Proven,
141}
142
143/// A mathematical equation extracted from a paper (Phase 1 output).
144#[derive(Debug, Clone, Default, Serialize, Deserialize)]
145pub struct Equation {
146    /// Default-empty so diagnostic/methodology contracts that use prose
147    /// requirements instead of a formula (e.g.
148    /// `decode-hot-path-prefix-cache-diagnostic-v1`) still parse.
149    #[serde(default)]
150    pub formula: String,
151    #[serde(default)]
152    pub domain: Option<String>,
153    #[serde(default)]
154    pub codomain: Option<String>,
155    #[serde(default)]
156    pub invariants: Vec<String>,
157    /// Rust preconditions — compiled to `debug_assert!()` by `build.rs`.
158    #[serde(default)]
159    pub preconditions: Vec<String>,
160    /// Rust postconditions — compiled to `debug_assert!()` by `build.rs`.
161    #[serde(default)]
162    pub postconditions: Vec<String>,
163    /// Lean 4 theorem name that proves this equation correct.
164    /// Example: "ProvableContracts.Theorems.Softmax.PartitionOfUnity"
165    #[serde(default)]
166    pub lean_theorem: Option<String>,
167    /// IEEE 754 tolerance: codegen emits `>=` instead of `>` for boundaries (GH-67).
168    #[serde(default)]
169    pub float_tolerance: Option<f64>,
170    /// Compositional verification: what this equation requires from upstream.
171    /// References a guarantees block from another contract/equation.
172    #[serde(default)]
173    pub assumes: Option<ShapeContract>,
174    /// Compositional verification: what this equation provides to downstream.
175    /// Must be satisfiable by any downstream equation that assumes it.
176    #[serde(default)]
177    pub guarantees: Option<ShapeContract>,
178}
179
180/// A proof obligation derived from an equation.
181///
182/// 26 obligation types: 19 property types plus 7 Design by Contract
183/// types (`precondition`, `postcondition`, `frame`, `loop_invariant`,
184/// `loop_variant`, `old_state`, `subcontract`).
185#[derive(Debug, Clone, Default, Serialize, Deserialize)]
186pub struct ProofObligation {
187    /// Obligation category. Defaults to `Invariant` for legacy contracts
188    /// that predate the DbC split (e.g. `eval-harness-humaneval-v1`,
189    /// `publish-manifest-v1`) which ship with just `property:`/`formal:`.
190    #[serde(rename = "type", default)]
191    pub obligation_type: ObligationType,
192    /// Human-readable statement of what must hold. Alias `statement`
193    /// accepted for legacy diagnostic contracts (e.g.
194    /// `decode-hot-path-prefix-cache-diagnostic-v1`) whose POs predate
195    /// the canonical `property:` naming.
196    #[serde(default, alias = "statement")]
197    pub property: String,
198    /// Formal predicate (Rust/Lean syntax). Alias `verification` accepted
199    /// for legacy contracts that ship a shell/pmat-query check instead of
200    /// a formal predicate.
201    #[serde(default, alias = "verification")]
202    pub formal: Option<String>,
203    #[serde(default)]
204    pub tolerance: Option<f64>,
205    #[serde(default)]
206    pub applies_to: Option<AppliesTo>,
207    /// Phase 7: Lean 4 theorem proving metadata.
208    #[serde(default)]
209    pub lean: Option<LeanProof>,
210    /// Postcondition only: links to a precondition obligation ID.
211    #[serde(default)]
212    pub requires: Option<String>,
213    /// Loop invariant/variant only: references a `kernel_structure.phases[]` name.
214    #[serde(default)]
215    pub applies_to_phase: Option<String>,
216    /// Subcontract only: contract stem being refined (must be in `metadata.depends_on`).
217    #[serde(default)]
218    pub parent_contract: Option<String>,
219}
220
221#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)]
222#[serde(rename_all = "lowercase")]
223pub enum ObligationType {
224    #[default]
225    Invariant,
226    Equivalence,
227    Bound,
228    Monotonicity,
229    Idempotency,
230    Linearity,
231    Symmetry,
232    Associativity,
233    Conservation,
234    Ordering,
235    Completeness,
236    Soundness,
237    Involution,
238    Determinism,
239    Roundtrip,
240    #[serde(rename = "state_machine")]
241    StateMachine,
242    Classification,
243    Independence,
244    Termination,
245    /// Memory/IO safety obligation (bounds checks, non-null, etc.). Legacy
246    /// pre-APR-MONO contracts (e.g. `apr-cli-publish-extra-v1`) used this
247    /// spelling; kept for back-compat alongside the 26 other types.
248    Safety,
249    /// Liveness property (eventually-happens). Same legacy contract
250    /// (`apr-cli-publish-extra-v1`) uses this for progress obligations;
251    /// kept for back-compat.
252    Liveness,
253    // Eiffel DbC types (Meyer 1997)
254    Precondition,
255    Postcondition,
256    Frame,
257    #[serde(rename = "loop_invariant")]
258    LoopInvariant,
259    #[serde(rename = "loop_variant")]
260    LoopVariant,
261    #[serde(rename = "old_state")]
262    OldState,
263    Subcontract,
264}
265
266impl std::fmt::Display for ObligationType {
267    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
268        let s = match self {
269            Self::Invariant => "invariant",
270            Self::Equivalence => "equivalence",
271            Self::Bound => "bound",
272            Self::Monotonicity => "monotonicity",
273            Self::Idempotency => "idempotency",
274            Self::Linearity => "linearity",
275            Self::Symmetry => "symmetry",
276            Self::Associativity => "associativity",
277            Self::Conservation => "conservation",
278            Self::Ordering => "ordering",
279            Self::Completeness => "completeness",
280            Self::Soundness => "soundness",
281            Self::Involution => "involution",
282            Self::Determinism => "determinism",
283            Self::Roundtrip => "roundtrip",
284            Self::StateMachine => "state_machine",
285            Self::Classification => "classification",
286            Self::Independence => "independence",
287            Self::Termination => "termination",
288            Self::Safety => "safety",
289            Self::Liveness => "liveness",
290            Self::Precondition => "precondition",
291            Self::Postcondition => "postcondition",
292            Self::Frame => "frame",
293            Self::LoopInvariant => "loop_invariant",
294            Self::LoopVariant => "loop_variant",
295            Self::OldState => "old_state",
296            Self::Subcontract => "subcontract",
297        };
298        write!(f, "{s}")
299    }
300}
301
302#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
303#[serde(rename_all = "lowercase")]
304pub enum AppliesTo {
305    All,
306    Scalar,
307    Simd,
308    Converter,
309    /// Algorithm-specific target (e.g., "degree", "bce", "huber").
310    #[serde(other)]
311    Other,
312}
313
314/// Kernel phase decomposition.
315#[derive(Debug, Clone, Serialize, Deserialize)]
316pub struct KernelStructure {
317    pub phases: Vec<KernelPhase>,
318}
319
320#[derive(Debug, Clone, Serialize, Deserialize)]
321pub struct KernelPhase {
322    pub name: String,
323    pub description: String,
324    #[serde(default)]
325    pub invariant: Option<String>,
326}
327
328/// An enforcement rule from the contract.
329#[derive(Debug, Clone, Serialize, Deserialize)]
330pub struct EnforcementRule {
331    pub description: String,
332    #[serde(default)]
333    pub check: Option<String>,
334    #[serde(default)]
335    pub severity: Option<String>,
336    #[serde(default)]
337    pub reference: Option<String>,
338}
339
340/// A Popperian falsification test.
341///
342/// Each makes a falsifiable prediction about the implementation.
343/// If the prediction is wrong, the test identifies root cause.
344#[derive(Debug, Clone, Default, Serialize, Deserialize)]
345pub struct FalsificationTest {
346    pub id: String,
347    /// What the test asserts. Alias `description` accepted for legacy
348    /// pre-APR-MONO contracts that used the `description:` field name.
349    /// `name:` is NOT aliased because several legacy contracts (e.g.
350    /// `publish-manifest-v1`) ship both `name:` (a slug) and
351    /// `description:` (prose) side-by-side; aliasing both collapses to
352    /// a `duplicate field` error.
353    #[serde(default, alias = "description")]
354    pub rule: String,
355    /// The predicted outcome if the rule holds. Alias `expected` accepted
356    /// for legacy contracts (e.g. `expected: exit 0`, `expected: "PASS"`).
357    /// Defaulted because diagnostic contracts often encode prediction
358    /// inside the rule text alone.
359    #[serde(default, alias = "expected")]
360    pub prediction: String,
361    /// How to run the test. Alias `command` accepted for legacy contracts
362    /// (e.g. shell snippets under `command: |`).
363    #[serde(default, alias = "command")]
364    pub test: Option<String>,
365    /// What failure means. Alias `fails_if` accepted for legacy contracts.
366    /// Defaulted because several legacy diagnostic contracts omit it.
367    #[serde(default, alias = "fails_if")]
368    pub if_fails: String,
369}
370
371/// A Kani bounded model checking harness definition.
372///
373/// Corresponds to Phase 6 (Verify) of the pipeline.
374#[derive(Debug, Clone, Default, Serialize, Deserialize)]
375pub struct KaniHarness {
376    pub id: String,
377    pub obligation: String,
378    #[serde(default)]
379    pub property: Option<String>,
380    #[serde(default)]
381    pub bound: Option<u32>,
382    #[serde(default)]
383    pub strategy: Option<KaniStrategy>,
384    #[serde(default)]
385    pub solver: Option<String>,
386    #[serde(default)]
387    pub harness: Option<String>,
388}
389
390#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
391#[serde(rename_all = "snake_case")]
392pub enum KaniStrategy {
393    Exhaustive,
394    StubFloat,
395    Compositional,
396    BoundedInt,
397}
398
399impl std::fmt::Display for KaniStrategy {
400    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
401        let s = match self {
402            Self::Exhaustive => "exhaustive",
403            Self::StubFloat => "stub_float",
404            Self::Compositional => "compositional",
405            Self::BoundedInt => "bounded_int",
406        };
407        write!(f, "{s}")
408    }
409}
410
411/// Phase 7: Lean 4 theorem proving metadata for a proof obligation.
412#[derive(Debug, Clone, Serialize, Deserialize)]
413pub struct LeanProof {
414    /// Lean 4 theorem name (e.g., `Softmax.partition_of_unity`).
415    pub theorem: String,
416    /// Lean 4 module path (e.g., `ProvableContracts.Softmax`).
417    #[serde(default)]
418    pub module: Option<String>,
419    /// Current status of the Lean proof.
420    #[serde(default)]
421    pub status: LeanStatus,
422    /// Lean-level theorem dependencies.
423    #[serde(default)]
424    pub depends_on: Vec<String>,
425    /// Mathlib import paths required.
426    #[serde(default)]
427    pub mathlib_imports: Vec<String>,
428    /// Free-form notes (e.g., "Proof over reals; f32 gap addressed separately").
429    #[serde(default)]
430    pub notes: Option<String>,
431}
432
433/// Status of a Lean 4 proof.
434#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)]
435#[serde(rename_all = "kebab-case")]
436pub enum LeanStatus {
437    /// Proof is complete and type-checks.
438    Proved,
439    /// Proof uses `sorry` (axiomatized, not yet proved).
440    #[default]
441    Sorry,
442    /// Work in progress.
443    Wip,
444    /// Obligation is not amenable to Lean proof (e.g., performance).
445    NotApplicable,
446}
447
448impl std::fmt::Display for LeanStatus {
449    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
450        let s = match self {
451            Self::Proved => "proved",
452            Self::Sorry => "sorry",
453            Self::Wip => "wip",
454            Self::NotApplicable => "not-applicable",
455        };
456        write!(f, "{s}")
457    }
458}
459
460/// Phase 7: Verification summary across all obligations in a contract.
461#[derive(Debug, Clone, Serialize, Deserialize)]
462pub struct VerificationSummary {
463    pub total_obligations: u32,
464    #[serde(default)]
465    pub l2_property_tested: u32,
466    #[serde(default)]
467    pub l3_kani_proved: u32,
468    #[serde(default)]
469    pub l4_lean_proved: u32,
470    #[serde(default)]
471    pub l4_sorry_count: u32,
472    #[serde(default)]
473    pub l4_not_applicable: u32,
474}
475
476/// QA gate definition for certeza integration.
477///
478/// Legacy diagnostic contracts (e.g.
479/// `decode-hot-path-prefix-cache-diagnostic-v1`) ship a `qa_gate:` block
480/// with only `must_pass:` / `integration:` / `regression_protection:` — no
481/// `id:` or `name:`. All schema fields default so those parse cleanly.
482#[derive(Debug, Clone, Default, Serialize, Deserialize)]
483pub struct QaGate {
484    #[serde(default)]
485    pub id: String,
486    #[serde(default)]
487    pub name: String,
488    #[serde(default)]
489    pub description: Option<String>,
490    #[serde(default)]
491    pub checks: Vec<String>,
492    #[serde(default)]
493    pub pass_criteria: Option<String>,
494    #[serde(default)]
495    pub falsification: Option<String>,
496}
497
498/// A type-level invariant (Meyer's class invariant).
499///
500/// Asserts a predicate that must hold for every instance of `type_name`
501/// at every stable state — after construction and after every public method.
502#[derive(Debug, Clone, Serialize, Deserialize)]
503pub struct TypeInvariant {
504    pub name: String,
505    /// Rust type name (e.g., `ValidatedTensor`).
506    #[serde(rename = "type")]
507    pub type_name: String,
508    /// Rust boolean expression over `self` (e.g., `!self.dims.is_empty()`).
509    pub predicate: String,
510    #[serde(default)]
511    pub description: Option<String>,
512}
513
514/// Coq verification specification for a contract.
515#[derive(Debug, Clone, Serialize, Deserialize)]
516pub struct CoqSpec {
517    /// Coq module name (e.g., `SoftmaxSpec`).
518    pub module: String,
519    /// Coq import statements.
520    #[serde(default)]
521    pub imports: Vec<String>,
522    /// Coq definitions generated from equations.
523    #[serde(default)]
524    pub definitions: Vec<CoqDefinition>,
525    /// Links from proof obligations to Coq lemmas.
526    #[serde(default)]
527    pub obligations: Vec<CoqObligation>,
528}
529
530/// A Coq definition derived from a contract equation.
531#[derive(Debug, Clone, Serialize, Deserialize)]
532pub struct CoqDefinition {
533    pub name: String,
534    pub statement: String,
535}
536
537/// A link between a proof obligation and a Coq lemma.
538#[derive(Debug, Clone, Serialize, Deserialize)]
539pub struct CoqObligation {
540    /// References a proof obligation property or ID.
541    pub links_to: String,
542    /// Coq lemma name.
543    pub coq_lemma: String,
544    /// Current status of the Coq proof.
545    #[serde(default = "coq_status_default")]
546    pub status: String,
547}
548
549fn coq_status_default() -> String {
550    "stub".to_string()
551}
552
553/// Accepts `equations:` as either a map (canonical) or a list-of-dicts
554/// with an `id` field (legacy pre-APR-MONO diagnostic contracts like
555/// `decode-hot-path-prefix-cache-diagnostic-v1`). The list form promotes
556/// each entry's `id` to the map key; entries without `id` fall back to
557/// `equation_{N}` so parsing never silently drops data.
558fn deserialize_equations<'de, D>(d: D) -> Result<BTreeMap<String, Equation>, D::Error>
559where
560    D: serde::Deserializer<'de>,
561{
562    use serde::de::Error;
563    use serde_yaml::Value;
564
565    let value = Value::deserialize(d)?;
566    match value {
567        Value::Null => Ok(BTreeMap::new()),
568        Value::Mapping(_) => serde_yaml::from_value(value).map_err(D::Error::custom),
569        Value::Sequence(items) => {
570            let mut out = BTreeMap::new();
571            for (i, mut item) in items.into_iter().enumerate() {
572                let key = match &mut item {
573                    Value::Mapping(m) => m
574                        .remove(Value::String("id".into()))
575                        .and_then(|v| v.as_str().map(ToString::to_string))
576                        .unwrap_or_else(|| format!("equation_{i}")),
577                    _ => format!("equation_{i}"),
578                };
579                let eq: Equation = serde_yaml::from_value(item).map_err(D::Error::custom)?;
580                out.insert(key, eq);
581            }
582            Ok(out)
583        }
584        other => Err(D::Error::custom(format!(
585            "`equations:` must be a map or a list; got {other:?}"
586        ))),
587    }
588}
589
590#[cfg(test)]
591#[path = "types_tests.rs"]
592mod tests;
provable_contracts/schema/types.rs

provable_contracts/schema/
types.rs
