Function codegen_program_with_proven 

pub fn codegen_program_with_proven(
    stmts: &[Stmt<'_>],
    registry: &TypeRegistry,
    policies: &PolicyRegistry,
    interner: &Interner,
    type_env: &TypeEnv,
    cfg: &OptimizationConfig,
    module_name: &str,
    proven: Option<&str>,
) -> String

Like codegen_program, but bundles an extracted math/logic module into the output. proven is the body of a Rust module — functions, check_* property fns, a World/holds model-checker — produced by the Forge’s extraction with NO fn main. It is emitted as pub mod <module_name> { … } right after the prelude (before user_types), followed by use <module_name>::*; so a bare call in the imperative program below — e.g. double(21) — resolves into it. Naming the module (rather than dumping items at crate root) keeps multiple proven modules reachable and avoids polluting the imperative namespace. When proven is None/blank the output is byte-identical to codegen_program.