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>,
}

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.

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.

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