Crate provable_contracts 

provable-contracts — compatibility facade

This crate was renamed to aprender-contracts during the APR-MONO consolidation. It stays on crates.io so existing dependents keep compiling: it re-exports the real crate’s public surface verbatim and adds nothing of its own.

# migrate at your convenience; no source change is needed either way
aprender-contracts = "0.63"

The promise, and how it is held

Every path that resolved through provable_contracts::… at 0.3.1 resolves to the same item today. That is checked, not hoped: the 28 example programs published inside provable-contracts 0.3.1 are vendored verbatim under compat/0.3.1/ and compiled against this crate by scripts/check_facade_compat.sh in CI. They call into 20 of the re-exported modules by name, so a drifted signature — not merely a removed export — fails the build.

Bound by contracts/provable-contracts-facade-v1.yaml.

Modules

audit

Audit trail generator — traceability chain.

binding

Binding registry — maps contract equations to implementations.

book_gen

mdBook page generation for contracts.

build_helper

Build script helper for consuming crates.

codegen

Code generation from YAML contracts → Rust debug_assert!() checks.

coq_gen

Coq theorem stub generation from YAML contracts.

coverage

Cross-contract obligation coverage report.

diff

Contract diff — detect drift between contract versions.

doc_integrity

Document integrity validation for Markdown and SVG files.

error

explain

Contract explanation — chain-of-thought narrative for any contract.

extract

PyTorch kernel extraction — reads Python source, extracts equations.

flux_gen

Flux refinement type annotation generation.

fuzz_gen

Coverage-guided fuzz target generation.

generate

End-to-end codegen — generates all artifacts to disk.

graph

Contract dependency graph — composition via depends_on.

infer

Contract inference engine.

invariant_gen

Type invariant code generation.

kani_gen

Kani harness generator — Phase 6 of the pipeline.

kernels

Kernel implementations: scalar reference, AVX2 SIMD, and CUDA PTX.

latex

LaTeX conversion utilities for contract math notation.

lean_gen

Lean 4 code generator — Phase 7 of the pipeline.

lint

Contract quality gate: validate + audit + score in one pass.

mirai_gen

MIRAI abstract interpretation annotation generation.

obligation_matrix

Per-obligation verification matrix.

pipeline

Pipeline contract support — cross-repo compositional verification.

probar_gen

Probar property-test generator — Phase 5 of the pipeline.

proof_status

Proof status report — cross-contract proof level assessment.

query

Contract query engine with BM25 semantic search.

readme_gen

Deterministic README.md and CI workflow generation for consumer projects.

reverse_coverage

Reverse coverage: detect public functions without contract bindings.

roofline

Runtime roofline model derived from contract YAML.

scaffold

Scaffold generator — Phase 3 of the pipeline.

schema

scoring

Contract and codebase scoring.

tla_gen

TLA+ system-level model checking specification generation.

traits

Auto-generated contract traits for compiler-enforced binding verification.