provable_contracts/lib.rs
1//! # provable-contracts
2//!
3//! Papers to Math to Contracts in Code.
4//!
5//! A Rust library for converting peer-reviewed research papers into
6//! mathematically provable kernel implementations via YAML contract
7//! intermediaries with Kani bounded model checking verification.
8//!
9//! ## Modules
10//!
11//! - [`schema`] — Parse and validate YAML kernel contracts
12//! - [`scaffold`] — Generate Rust trait stubs + failing tests from contracts
13//! - [`kani`] — Generate `#[kani::proof]` harnesses from contracts
14//! - [`probar`] — Generate probar property-based tests from contracts
15//! - [`audit`] — Trace paper→equation→contract→test→proof chain
16//! - [`binding`] — Map contract equations to implementation functions
17//! - [`diff`] — Detect drift between contract versions
18//! - [`coverage`] — Cross-contract obligation coverage report
19//! - [`generate`] — End-to-end codegen to disk
20//! - [`graph`] — Contract dependency graph and cycle detection
21//! - [`latex`] — LaTeX conversion for contract math notation
22//! - [`book_gen`] — mdBook page generation for contracts
23//! - [`lean_gen`] — Lean 4 definition and theorem stub generation
24//! - [`lint`] — Contract quality gate: validate + audit + score in one pass
25//! - [`kernels`] — Scalar, AVX2, and PTX kernel implementations
26
27pub mod audit;
28pub(crate) mod auto_exempt;
29pub mod binding;
30pub mod book_gen;
31pub mod build_helper;
32pub mod codegen;
33pub mod coq_gen;
34pub mod coverage;
35pub mod diff;
36pub mod doc_integrity;
37pub mod error;
38pub mod explain;
39pub mod extract;
40pub mod flux_gen;
41pub mod fuzz_gen;
42pub mod generate;
43pub mod graph;
44pub mod infer;
45pub mod invariant_gen;
46pub mod kani_gen;
47pub mod kernels;
48pub mod latex;
49pub mod lean_gen;
50pub mod lint;
51pub mod mirai_gen;
52pub mod obligation_matrix;
53pub mod pipeline;
54pub mod probar_gen;
55pub mod proof_status;
56pub mod query;
57pub mod readme_gen;
58pub mod reverse_coverage;
59pub mod roofline;
60pub mod scaffold;
61pub mod schema;
62pub mod scoring;
63pub mod tla_gen;
64pub mod traits;