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

provable_contracts/schema/
types.rs
