provable_contracts/schema/
kind.rs

1//! Contract kinds — declare which validation rules apply to a YAML file.
2
3use serde::{Deserialize, Serialize};
4
5/// The kind of contract artifact. Determines which validation rules apply.
6///
7/// - `Kernel` (default): a mathematical kernel contract — the provability
8///   invariant applies (must have `proof_obligations`, `falsification_tests`,
9///   `kani_harnesses`).
10/// - `Registry`: a data registry (lookup tables, enum definitions, config
11///   bounds) — exempt from provability, validated for `metadata` + entries.
12/// - `ModelFamily`: architecture metadata (`HuggingFace` family descriptors,
13///   size variants, vendor) — exempt from provability, validated for
14///   `metadata` fields. Custom top-level fields are preserved but not
15///   enforced by the kernel schema.
16/// - `ModelFamilyVariant`: a concrete size variant of a model family
17///   (e.g. Llama 370M sovereign). Freezes hyperparameters (vocab, hidden
18///   dim, layer count) and delta-dispatches invariants from the parent
19///   family. Exempt from provability.
20/// - `Tokenizer`: a concrete tokenizer contract — vocab bounds, required
21///   special tokens, round-trip gate, normalization form. Exempt from
22///   provability (gates are byte-exact tests, not Kani harnesses).
23/// - `TrainingLoop`: a training-loop contract — loss schedule, optimizer
24///   config, gradient-clipping policy, checkpoint cadence. Exempt from
25///   provability; validated for `metadata` + schedule fields.
26/// - `PretrainingCorpus`: a pretraining-corpus contract — dataset source,
27///   license, total-bytes bound, shard layout. Exempt from provability.
28/// - `TrainingPreconditionGate`: a hard precondition gate that must be
29///   satisfied before training starts (e.g. Chinchilla compute-optimal
30///   token/parameter ratio, GPU memory floor, dataset checksum). Exempt
31///   from provability; validated for `metadata` + gate-formula fields.
32/// - `CorpusAssembly`: a multi-source corpus assembly pipeline contract —
33///   declares input shards, dedup strategy, license-merge policy, and
34///   output manifest. Exempt from provability.
35/// - `Pattern`: a cross-cutting verification pattern (threading safety,
36///   async safety, compute parity) that applies across multiple kernels.
37///   Exempt from the kernel provability invariant but still validated for
38///   metadata and any proof/falsification data present.
39/// - `Schema`: a generic reference/schema document — exempt from provability,
40///   validated only for `metadata.id`, `metadata.version`, `metadata.description`,
41///   and `metadata.references`.
42/// - `Kaizen`: an improvement record — a dated, ticketed statement that a
43///   specific waste was removed, pinned by a `baseline:` → `target:` delta.
44///   Exempt from the kernel provability invariant (a kaizen record is a
45///   measurement, not a theorem) but held to its OWN falsifiability rules by
46///   `validate_kaizen` (KAIZEN-001..006): it must name itself, declare a
47///   status from a closed vocabulary, state something that can fail, and — if
48///   it pins a baseline/target — actually claim a movement, in a direction
49///   that does not contradict its own cost metrics.
50#[derive(
51    Debug, Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize,
52)]
53#[serde(rename_all = "kebab-case")]
54pub enum ContractKind {
55    #[default]
56    Kernel,
57    Registry,
58    ModelFamily,
59    ModelFamilyVariant,
60    Tokenizer,
61    TrainingLoop,
62    PretrainingCorpus,
63    TrainingPreconditionGate,
64    CorpusAssembly,
65    Pattern,
66    Schema,
67    /// A kaizen improvement record (`contracts/*/kaizen/*.yaml`). See the
68    /// module docs above and `schema::kaizen` for the KAIZEN-001..006 rules.
69    Kaizen,
70    /// A head-to-head BEAT benchmark: a committed, CI-wired claim that aprender
71    /// beats an incumbent (sklearn / PyTorch / Unsloth / Ollama) on a canonical
72    /// task, with a pinned baseline that fails CI on regression. The measurement
73    /// backbone for the four-pillar "replace AND beat" mission (PMAT-741).
74    BeatBenchmark,
75}
76
77impl std::fmt::Display for ContractKind {
78    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
79        let s = match self {
80            Self::Kernel => "kernel",
81            Self::Registry => "registry",
82            Self::ModelFamily => "model-family",
83            Self::ModelFamilyVariant => "model-family-variant",
84            Self::Tokenizer => "tokenizer",
85            Self::TrainingLoop => "training-loop",
86            Self::PretrainingCorpus => "pretraining-corpus",
87            Self::TrainingPreconditionGate => "training-precondition-gate",
88            Self::CorpusAssembly => "corpus-assembly",
89            Self::Pattern => "pattern",
90            Self::Schema => "schema",
91            Self::Kaizen => "kaizen",
92            Self::BeatBenchmark => "beat-benchmark",
93        };
94        write!(f, "{s}")
95    }
96}
97
98#[cfg(test)]
99mod beat_benchmark_tests {
100    use super::*;
101    use crate::error::Severity;
102    use crate::schema::{parse_contract_str, validate_contract};
103
104    /// BeatBenchmark serde round-trips through its kebab-case "beat-benchmark".
105    #[test]
106    fn beat_benchmark_kind_round_trips() {
107        assert_eq!(ContractKind::BeatBenchmark.to_string(), "beat-benchmark");
108        let k: ContractKind = serde_yaml::from_str("beat-benchmark").unwrap();
109        assert_eq!(k, ContractKind::BeatBenchmark);
110    }
111
112    /// The pilot beat contract (contracts/beat-sklearn-iris-v1.yaml) parses as a
113    /// BeatBenchmark and validates with zero Error-severity violations (PMAT-741).
114    #[test]
115    fn pilot_beat_contract_validates() {
116        let yaml = include_str!("../../../../contracts/beat-sklearn-iris-v1.yaml");
117        let contract = parse_contract_str(yaml).expect("pilot beat contract parses");
118        assert_eq!(contract.kind(), ContractKind::BeatBenchmark);
119        let errors: Vec<_> = validate_contract(&contract)
120            .into_iter()
121            .filter(|v| v.severity == Severity::Error)
122            .collect();
123        assert!(
124            errors.is_empty(),
125            "pilot beat contract has errors: {errors:?}"
126        );
127    }
128}
provable_contracts/schema/kind.rs

provable_contracts/schema/
kind.rs
