Module schema 

Re-exports

pub use super::composition::ShapeContract;

pub use super::composition::ShapeExpr;

Modules

composition

Structs

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.

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

ContractKind

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

EnforcementLevel

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

KaniStrategy

LeanStatus

Status of a Lean 4 proof.

ObligationType

Functions

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.