Struct Contract 

pub struct Contract {

    pub metadata: Metadata,
    pub equations: BTreeMap<String, Equation>,
    pub proof_obligations: Vec<ProofObligation>,
    pub kernel_structure: Option<KernelStructure>,
    pub simd_dispatch: BTreeMap<String, BTreeMap<String, String>>,
    pub enforcement: BTreeMap<String, EnforcementRule>,
    pub falsification_tests: Vec<FalsificationTest>,
    pub kani_harnesses: Vec<KaniHarness>,
    pub qa_gate: Option<QaGate>,
    pub verification_summary: Option<VerificationSummary>,
    pub type_invariants: Vec<TypeInvariant>,
    pub coq_spec: Option<CoqSpec>,
    pub beat: Option<Beat>,
    pub stories: Vec<CruxStory>,
    pub falsification: Option<Value>,
    pub falsification_conditions: Option<Value>,
    pub unknown_top_level_keys: Vec<String>,
    pub kaizen_record: Option<KaizenRecord>,
    pub strict_yaml_error: Option<String>,
}

A complete YAML kernel contract.

This is the root type for the contract schema defined in docs/specifications/pv-spec.md Section 3.

Fields

metadata: Metadata

equations: BTreeMap<String, Equation>

Equations are optional — kaizen, pipeline, and registry contracts may define only proof_obligations without mathematical equations.

Accepts both map form (equations: { silu: { formula: ... } }, the canonical schema) and sequence form (equations: [{ id: silu, formula: ... }], used by several diagnostic/methodology contracts predating APR-MONO). The sequence form promotes each item’s id field to the map key.

proof_obligations: Vec<ProofObligation>

kernel_structure: Option<KernelStructure>

simd_dispatch: BTreeMap<String, BTreeMap<String, String>>

enforcement: BTreeMap<String, EnforcementRule>

falsification_tests: Vec<FalsificationTest>

kani_harnesses: Vec<KaniHarness>

qa_gate: Option<QaGate>

verification_summary: Option<VerificationSummary>

Phase 7: Lean 4 verification summary across all obligations.

type_invariants: Vec<TypeInvariant>

Type-level invariants (Meyer’s class invariants).

coq_spec: Option<CoqSpec>

Coq verification specification.

beat: Option<Beat>

BEAT-benchmark parameters (PMAT-741) — present on metadata.kind: beat-benchmark contracts; pins a machine-measured incumbent baseline so CI fails when aprender regresses below it on the incumbent’s canonical task.

stories: Vec<CruxStory>

CRUX master-registry story rows (contracts/crux-competitive-research-ux-v1.yaml).

THIS is the list the competitive-research programme actually sorts by. aprender#2555 originally range-checked only metadata.demand_score and justified it as “the ranking signal the whole programme sorts by” — but MEASURED, nothing in the repo reads metadata.demand_score; the 250 rows below are what §12.1 of docs/specifications/crux-competitive-research-ux-workflows.md maps to pmat work priority. They were entirely ungated. Validating them is what makes that justification true.

falsification: Option<Value>

Legacy free-form top-level falsification: block.

400 contracts in contracts/ carry this key, every one of them holding a structured list (shapes seen in the wild: {condition, action, severity}, {name, description, check}, {id, assertion, test_harness}). Contract is not deny_unknown_fields, so before this field existed serde dropped all of it silently — the same mechanism as #2465 (test_harness) and #2504. contracts/publish-workspace-v1.yaml is the canonical victim: four FALSIFY-PUB-* entries live here and pv status reported “Falsification tests: 0” while the file read as governance.

It is deliberately serde_yaml::Value: the block is NOT falsification_tests and must never be counted as one — it is captured so that tooling can SEE it and report the contract as inert. Migrating these entries into real falsification_tests is contract-by-contract work, not a schema change.

falsification_conditions: Option<Value>

Legacy free-form top-level falsification_conditions: block — the same silent-drop class as Contract::falsification, used by 12 contracts. Kept as a distinct field (not a serde alias) so a contract carrying both keys still parses instead of failing on a duplicate field.

unknown_top_level_keys: Vec<String>

Top-level YAML keys that are not fields of Contract, captured verbatim by crate::schema::parse_contract_str.

The schema deliberately tolerates unknown top-level keys — model-family, spec and registry YAMLs carry downstream-owned blocks (see parse_contract_with_kind_model_family), and 1224 of the 1726 contracts pv lint walks have at least one. deny_unknown_fields is therefore not an option. Instead the validator uses this list to reject the two shapes that are never legitimate: a top-level kind: (SCHEMA-018) and a near-miss misspelling of a real block name (SCHEMA-019).

Not serialized: it is a parse artifact, not contract content.

kaizen_record: Option<KaizenRecord>

The kaizen-record blocks (contract:, kaizen:, baseline:, target:, …) captured by a second parse pass when — and only when — metadata.kind is kaizen.

Kept OUT of the serde surface of Contract on purpose. The corpus carries status:, version:, invariants: and files: at top level on documents of several kinds with incompatible shapes, so promoting them to real Contract fields would change how all 1726 contracts parse in order to validate 46 kaizen records. Scoping the second pass to kind: kaizen means a type mismatch in some unrelated contract’s status: can never reach this struct.

Not serialized: it is a parse artifact, not contract content.

strict_yaml_error: Option<String>

The error a strict YAML reader produced on a document this schema nonetheless accepted, captured by crate::schema::parse_contract_str. None is the healthy case.

The derived deserializer skips unknown subtrees without reading them, so a contract can parse cleanly here and be rejected by yq, PyYAML, or a serde_yaml::Value round-trip. SCHEMA-020 turns that divergence into an error instead of leaving it to be discovered downstream.

Not serialized: it is a parse artifact, not contract content.

Implementations

impl Contract

pub fn is_registry(&self) -> bool

Back-compat: metadata.registry: true OR metadata.kind: registry.

pub fn kind(&self) -> ContractKind

The effective kind, honoring the legacy registry: true flag.

pub fn requires_proofs(&self) -> bool

True iff this contract must satisfy PROVABILITY-001 (kernel only).

pub fn legacy_falsification_entries(&self) -> usize

How many entries sit in the legacy top-level falsification: / falsification_conditions: blocks — content the schema captures but does NOT count as falsification_tests.

A non-zero result together with an empty falsification_tests is the inert-contract signature (#2504): the file reads as enforced and enforces nothing. pv status reports it so the reader is never told “Falsification tests: 0” without being told where the entries went.

pub fn provability_violations(&self) -> Vec<String>

Enforce the provability invariant: kernel contracts MUST have proof_obligations, falsification_tests, and kani_harnesses. Returns a list of violations. Empty list = contract is valid.

Trait Implementations

impl Clone for Contract

fn clone(&self) -> Contract

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Contract

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Contract

fn default() -> Contract

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Contract

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Serialize for Contract

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.