Function compile_to_rust_with_proven 

pub fn compile_to_rust_with_proven(
    source: &str,
    proven: &str,
) -> Result<String, ParseError>

Compile imperative LOGOS to Rust with an extracted math/logic module bundled in. proven is a main-less Rust module body (the Forge’s extraction); it is emitted as pub mod proven { … } use proven::*; so the imperative program can call its functions / check_* predicates by name. See compile_program_full_with_proven.