Function generate_from_contract 

pub fn generate_from_contract(
    name: &str,
    contract: &Contract,
) -> GeneratedContract

Generate Rust assertion code from a contract’s equations.

For each equation with preconditions or postconditions, generates:

pub fn check_gemv_preconditions(a_len: usize, rows: usize, cols: usize) {
    debug_assert!(a_len == rows * cols, "Pre: a.len() == rows * cols");
}