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 error;
37pub mod explain;
38pub mod extract;
39pub mod flux_gen;
40pub mod fuzz_gen;
41pub mod generate;
42pub mod graph;
43pub mod infer;
44pub mod invariant_gen;
45pub mod kani_gen;
46pub mod kernels;
47pub mod latex;
48pub mod lean_gen;
49pub mod lint;
50pub mod mirai_gen;
51pub mod obligation_matrix;
52pub mod pipeline;
53pub mod probar_gen;
54pub mod proof_status;
55pub mod query;
56pub mod readme_gen;
57pub mod reverse_coverage;
58pub mod roofline;
59pub mod scaffold;
60pub mod schema;
61pub mod scoring;
62pub mod tla_gen;
63pub mod traits;