1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
//! # provable-contracts
//!
//! Papers to Math to Contracts in Code.
//!
//! A Rust library for converting peer-reviewed research papers into
//! mathematically provable kernel implementations via YAML contract
//! intermediaries with Kani bounded model checking verification.
//!
//! ## Modules
//!
//! - [`schema`] — Parse and validate YAML kernel contracts
//! - [`scaffold`] — Generate Rust trait stubs + failing tests from contracts
//! - [`kani`] — Generate `#[kani::proof]` harnesses from contracts
//! - [`probar`] — Generate probar property-based tests from contracts
//! - [`audit`] — Trace paper→equation→contract→test→proof chain
//! - [`binding`] — Map contract equations to implementation functions
//! - [`diff`] — Detect drift between contract versions
//! - [`coverage`] — Cross-contract obligation coverage report
//! - [`generate`] — End-to-end codegen to disk
//! - [`graph`] — Contract dependency graph and cycle detection
//! - [`latex`] — LaTeX conversion for contract math notation
//! - [`book_gen`] — mdBook page generation for contracts
//! - [`lean_gen`] — Lean 4 definition and theorem stub generation
//! - [`kernels`] — Scalar, AVX2, and PTX kernel implementations