Function compile_program_full_with_proven 

pub fn compile_program_full_with_proven(
    source: &str,
    proven: Option<&str>,
) -> Result<CompileOutput, ParseError>

Like compile_program_full, but bundles an extracted math/logic module (proven) into the generated Rust — the imperative half of a mixed document. The module is emitted as pub mod proven { … } use proven::*; so the imperative program can call its functions / check_* predicates by name. None (or a blank module) yields output byte-identical to compile_program_full.