Module codegen 

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

Reads contract YAML files and generates a Rust module with assertion functions that can be called from production code. Zero cost in release.

Also generates Lean 4 obligation stubs for unproved theorems.

Structs

GeneratedContract

Generated contract enforcement code for a single contract.

Functions

generate_all

Generate code for all contracts in a directory (recursive).

generate_from_contract

Generate Rust assertion code from a contract’s equations.

write_rust_module

Write generated Rust code to a file.