Skip to main content Module schema Copy item path Source pub use super::composition::ShapeContract ;pub use super::composition::ShapeExpr ;composition 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. AppliesTo BeatOutcome The outcome of evaluating a measured value against a Beatapr 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 CONTRACT_TOP_LEVEL_FIELDS Every top-level key Contract deserializes, in declaration order. is_contract_yaml Is path a .yaml file the contract schema owns? parse_contract Parse a YAML contract file into a Contract parse_contract_str Parse a YAML contract from a string. validate_contract Validate a parsed contract for completeness and consistency.