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/// - `Pattern`: a cross-cutting verification pattern (threading safety,
29///   async safety, compute parity) that applies across multiple kernels.
30///   Exempt from the kernel provability invariant but still validated for
31///   metadata and any proof/falsification data present.
32/// - `Schema`: a generic reference/schema document — exempt from provability,
33///   validated only for `metadata.id`, `metadata.version`, `metadata.description`,
34///   and `metadata.references`.
35#[derive(
36    Debug, Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize,
37)]
38#[serde(rename_all = "kebab-case")]
39pub enum ContractKind {
40    #[default]
41    Kernel,
42    Registry,
43    ModelFamily,
44    ModelFamilyVariant,
45    Tokenizer,
46    TrainingLoop,
47    PretrainingCorpus,
48    Pattern,
49    Schema,
50}
51
52impl std::fmt::Display for ContractKind {
53    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
54        let s = match self {
55            Self::Kernel => "kernel",
56            Self::Registry => "registry",
57            Self::ModelFamily => "model-family",
58            Self::ModelFamilyVariant => "model-family-variant",
59            Self::Tokenizer => "tokenizer",
60            Self::TrainingLoop => "training-loop",
61            Self::PretrainingCorpus => "pretraining-corpus",
62            Self::Pattern => "pattern",
63            Self::Schema => "schema",
64        };
65        write!(f, "{s}")
66    }
67}
provable_contracts/schema/kind.rs

provable_contracts/schema/
kind.rs
