Module schema 

Re-exports

pub use artifact::classify_artifact;

pub use artifact::validate_artifact;

pub use artifact::ArtifactKind;

pub use super::composition::ShapeContract;

pub use super::composition::ShapeExpr;

pub use super::kaizen::KaizenRecord;

pub use super::kaizen::KAIZEN_STATUSES;

Modules

artifact

What a .yaml file under contracts/ actually IS, and how to validate it.

composition

kaizen

Kaizen improvement records (metadata.kind: kaizen).

Structs

Beat

Parameters of a head-to-head BEAT benchmark (metadata.kind: beat-benchmark, PMAT-741): a falsifiable, CI-wired claim that aprender meets-or-beats an incumbent (scikit-learn / PyTorch / Unsloth / Ollama·llama.cpp) on the incumbent’s own canonical task — the measurement backbone of the four-pillar “replace AND beat” mission. Required-shape is enforced by validate_beat_benchmark in the validator (BEAT-001..007).

Contract

A complete YAML kernel contract.

CoqDefinition

A Coq definition derived from a contract equation.

CoqObligation

A link between a proof obligation and a Coq lemma.

CoqSpec

Coq verification specification for a contract.

CruxStory

One row of the CRUX master registry’s stories: list.

EnforcementRule

An enforcement rule from the contract.

Equation

A mathematical equation extracted from a paper (Phase 1 output).

FalsificationTest

A Popperian falsification test.

KaniHarness

A Kani bounded model checking harness definition.

KernelPhase

KernelStructure

Kernel phase decomposition.

LeanProof

Phase 7: Lean 4 theorem proving metadata for a proof obligation.

Metadata

Contract metadata block.

ProofObligation

A proof obligation derived from an equation.

QaGate

QA gate definition for certeza integration.

TypeInvariant

A type-level invariant (Meyer’s class invariant).

VerificationSummary

Phase 7: Verification summary across all obligations in a contract.

Enums

AppliesTo

BeatOutcome

The outcome of evaluating a measured value against a Beat’s pinned threshold — the falsifiable verdict at the heart of apr beat-run.

ContractKind

The kind of contract artifact. Determines which validation rules apply.

EnforcementLevel

Per-contract enforcement level (gradual enforcement, Section 17).

IntakeStatus

Intake status of a CRUX competitive-research story (metadata.intake_status).

KaniStrategy

LeanStatus

Status of a Lean 4 proof.

ObligationType

Constants

CONTRACT_TOP_LEVEL_FIELDS

Every top-level key Contract deserializes, in declaration order.

Functions

is_contract_yaml

Is path a .yaml file the contract schema owns?

parse_contract

Parse a YAML contract file into a Contract struct.

parse_contract_str

Parse a YAML contract from a string.

validate_contract

Validate a parsed contract for completeness and consistency.