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/// - `Pattern`: a cross-cutting verification pattern (threading safety,
17/// async safety, compute parity) that applies across multiple kernels.
18/// Exempt from the kernel provability invariant but still validated for
19/// metadata and any proof/falsification data present.
20/// - `Schema`: a generic reference/schema document — exempt from provability,
21/// validated only for `metadata.id`, `metadata.version`, `metadata.description`,
22/// and `metadata.references`.
23#[derive(
24 Debug, Clone, Copy, Default, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize,
25)]
26#[serde(rename_all = "kebab-case")]
27pub enum ContractKind {
28 #[default]
29 Kernel,
30 Registry,
31 ModelFamily,
32 Pattern,
33 Schema,
34}
35
36impl std::fmt::Display for ContractKind {
37 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
38 let s = match self {
39 Self::Kernel => "kernel",
40 Self::Registry => "registry",
41 Self::ModelFamily => "model-family",
42 Self::Pattern => "pattern",
43 Self::Schema => "schema",
44 };
45 write!(f, "{s}")
46 }
47}