aprender-contracts 0.34.0

Papers to Math to Contracts in Code — YAML contract parsing, validation, scaffold generation, and Kani harness codegen for provable Rust kernels
Documentation

aprender-contracts

Crates.io docs.rs CI License: MIT

Provable contracts for the Aprender ML framework — YAML contract parsing, validation, lint reporting, and falsification scaffolding. 968 contract files validated, 1,371 tests.

Previously published as provable-contracts.

Install

[dependencies]
aprender-contracts = "0.29"

Or with cargo-add:

cargo add aprender-contracts

Quick Start

use aprender_contracts::{ContractLoader, LintReport};

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Load and validate all contracts in a directory
    let loader = ContractLoader::from_dir("contracts/")?;
    let report: LintReport = loader.lint()?;

    if report.has_errors() {
        eprintln!("{report}");
        std::process::exit(1);
    }

    println!("All {} contracts valid.", report.contract_count());
    Ok(())
}
use aprender_contracts::FalsificationTest;

// Generate falsification scaffold for a contract
let contract = loader.get("linear-regression-v1")?;
let tests: Vec<FalsificationTest> = contract.falsification_tests();
for test in &tests {
    println!("Precondition: {}", test.precondition);
    println!("Postcondition: {}", test.postcondition);
}

Key Types

Type Description
ContractLoader Loads and indexes YAML contracts from a directory tree
LintReport Aggregated lint results: errors, warnings, contract count
FalsificationTest A single (precondition, postcondition) pair for Kani harness generation
ContractSchema Parsed representation of one YAML contract file

Features

  • YAML contract parsing with JSON Schema validation
  • Lint rules: missing falsification conditions, placeholder preconditions, schema conformance
  • Falsification test scaffolding for Kani harness generation
  • Used by apr qa to enforce 405 provable contracts across all 70 crates

Documentation

License

MIT. See LICENSE.