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    /// GH-1595: When `true`, the harness has been verified by a green
389    /// `cargo kani` run in CI (e.g. apr-cookbook `kani-gate`). Lifts the
390    /// D3 strategy weight to 1.0 for non-exhaustive strategies because
391    /// the runtime witness supplants the static-readiness signal.
392    #[serde(default)]
393    pub actually_verified: Option<bool>,
394}
395
396#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
397#[serde(rename_all = "snake_case")]
398pub enum KaniStrategy {
399    Exhaustive,
400    StubFloat,
401    Compositional,
402    BoundedInt,
403}
404
405impl std::fmt::Display for KaniStrategy {
406    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
407        let s = match self {
408            Self::Exhaustive => "exhaustive",
409            Self::StubFloat => "stub_float",
410            Self::Compositional => "compositional",
411            Self::BoundedInt => "bounded_int",
412        };
413        write!(f, "{s}")
414    }
415}
416
417/// Phase 7: Lean 4 theorem proving metadata for a proof obligation.
418#[derive(Debug, Clone, Serialize, Deserialize)]
419pub struct LeanProof {
420    /// Lean 4 theorem name (e.g., `Softmax.partition_of_unity`).
421    pub theorem: String,
422    /// Lean 4 module path (e.g., `ProvableContracts.Softmax`).
423    #[serde(default)]
424    pub module: Option<String>,
425    /// Current status of the Lean proof.
426    #[serde(default)]
427    pub status: LeanStatus,
428    /// Lean-level theorem dependencies.
429    #[serde(default)]
430    pub depends_on: Vec<String>,
431    /// Mathlib import paths required.
432    #[serde(default)]
433    pub mathlib_imports: Vec<String>,
434    /// Free-form notes (e.g., "Proof over reals; f32 gap addressed separately").
435    #[serde(default)]
436    pub notes: Option<String>,
437}
438
439/// Status of a Lean 4 proof.
440#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)]
441#[serde(rename_all = "kebab-case")]
442pub enum LeanStatus {
443    /// Proof is complete and type-checks.
444    Proved,
445    /// Proof uses `sorry` (axiomatized, not yet proved).
446    #[default]
447    Sorry,
448    /// Work in progress.
449    Wip,
450    /// Obligation is not amenable to Lean proof (e.g., performance).
451    NotApplicable,
452}
453
454impl std::fmt::Display for LeanStatus {
455    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
456        let s = match self {
457            Self::Proved => "proved",
458            Self::Sorry => "sorry",
459            Self::Wip => "wip",
460            Self::NotApplicable => "not-applicable",
461        };
462        write!(f, "{s}")
463    }
464}
465
466/// Phase 7: Verification summary across all obligations in a contract.
467#[derive(Debug, Clone, Serialize, Deserialize)]
468pub struct VerificationSummary {
469    pub total_obligations: u32,
470    #[serde(default)]
471    pub l2_property_tested: u32,
472    #[serde(default)]
473    pub l3_kani_proved: u32,
474    #[serde(default)]
475    pub l4_lean_proved: u32,
476    #[serde(default)]
477    pub l4_sorry_count: u32,
478    #[serde(default)]
479    pub l4_not_applicable: u32,
480}
481
482/// QA gate definition for certeza integration.
483///
484/// Legacy diagnostic contracts (e.g.
485/// `decode-hot-path-prefix-cache-diagnostic-v1`) ship a `qa_gate:` block
486/// with only `must_pass:` / `integration:` / `regression_protection:` — no
487/// `id:` or `name:`. All schema fields default so those parse cleanly.
488#[derive(Debug, Clone, Default, Serialize, Deserialize)]
489pub struct QaGate {
490    #[serde(default)]
491    pub id: String,
492    #[serde(default)]
493    pub name: String,
494    #[serde(default)]
495    pub description: Option<String>,
496    #[serde(default)]
497    pub checks: Vec<String>,
498    #[serde(default)]
499    pub pass_criteria: Option<String>,
500    #[serde(default)]
501    pub falsification: Option<String>,
502}
503
504/// A type-level invariant (Meyer's class invariant).
505///
506/// Asserts a predicate that must hold for every instance of `type_name`
507/// at every stable state — after construction and after every public method.
508#[derive(Debug, Clone, Serialize, Deserialize)]
509pub struct TypeInvariant {
510    pub name: String,
511    /// Rust type name (e.g., `ValidatedTensor`).
512    #[serde(rename = "type")]
513    pub type_name: String,
514    /// Rust boolean expression over `self` (e.g., `!self.dims.is_empty()`).
515    pub predicate: String,
516    #[serde(default)]
517    pub description: Option<String>,
518}
519
520/// Coq verification specification for a contract.
521#[derive(Debug, Clone, Serialize, Deserialize)]
522pub struct CoqSpec {
523    /// Coq module name (e.g., `SoftmaxSpec`).
524    pub module: String,
525    /// Coq import statements.
526    #[serde(default)]
527    pub imports: Vec<String>,
528    /// Coq definitions generated from equations.
529    #[serde(default)]
530    pub definitions: Vec<CoqDefinition>,
531    /// Links from proof obligations to Coq lemmas.
532    #[serde(default)]
533    pub obligations: Vec<CoqObligation>,
534}
535
536/// A Coq definition derived from a contract equation.
537#[derive(Debug, Clone, Serialize, Deserialize)]
538pub struct CoqDefinition {
539    pub name: String,
540    pub statement: String,
541}
542
543/// A link between a proof obligation and a Coq lemma.
544#[derive(Debug, Clone, Serialize, Deserialize)]
545pub struct CoqObligation {
546    /// References a proof obligation property or ID.
547    pub links_to: String,
548    /// Coq lemma name.
549    pub coq_lemma: String,
550    /// Current status of the Coq proof.
551    #[serde(default = "coq_status_default")]
552    pub status: String,
553}
554
555fn coq_status_default() -> String {
556    "stub".to_string()
557}
558
559/// Accepts `equations:` as either a map (canonical) or a list-of-dicts
560/// with an `id` field (legacy pre-APR-MONO diagnostic contracts like
561/// `decode-hot-path-prefix-cache-diagnostic-v1`). The list form promotes
562/// each entry's `id` to the map key; entries without `id` fall back to
563/// `equation_{N}` so parsing never silently drops data.
564fn deserialize_equations<'de, D>(d: D) -> Result<BTreeMap<String, Equation>, D::Error>
565where
566    D: serde::Deserializer<'de>,
567{
568    use serde::de::Error;
569    use serde_yaml::Value;
570
571    let value = Value::deserialize(d)?;
572    match value {
573        Value::Null => Ok(BTreeMap::new()),
574        Value::Mapping(_) => serde_yaml::from_value(value).map_err(D::Error::custom),
575        Value::Sequence(items) => {
576            let mut out = BTreeMap::new();
577            for (i, mut item) in items.into_iter().enumerate() {
578                let key = match &mut item {
579                    Value::Mapping(m) => m
580                        .remove(Value::String("id".into()))
581                        .and_then(|v| v.as_str().map(ToString::to_string))
582                        .unwrap_or_else(|| format!("equation_{i}")),
583                    _ => format!("equation_{i}"),
584                };
585                let eq: Equation = serde_yaml::from_value(item).map_err(D::Error::custom)?;
586                out.insert(key, eq);
587            }
588            Ok(out)
589        }
590        other => Err(D::Error::custom(format!(
591            "`equations:` must be a map or a list; got {other:?}"
592        ))),
593    }
594}
595
596#[cfg(test)]
597#[path = "types_tests.rs"]
598mod tests;
provable_contracts/schema/types.rs

provable_contracts/schema/
types.rs
