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 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.

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.