assura-codegen 0.3.0

use super::*;
use assura_ast::Spanned;

// =======================================================================
// T119: Cranelift backend configuration
// =======================================================================

#[test]
fn backend_default_is_rustc() {
    let config = super::BackendConfig::default();
    assert_eq!(config.backend, super::CodegenBackend::Rustc);
}

#[test]
fn backend_cranelift_fast_dev() {
    let config = super::BackendConfig {
        backend: super::CodegenBackend::Cranelift,
        opt_level: 0,
        debug_info: true,
        target: super::CompileTarget::Native,
        ..Default::default()
    };
    assert_eq!(config.backend, super::CodegenBackend::Cranelift);
    assert_eq!(config.opt_level, 0);
}

fn codegen_with_config_ok(source: &str, config: super::BackendConfig) -> super::GeneratedProject {
    let file = assura_parser::parse_unwrap(source);
    let resolved = assura_resolve::resolve(&file).expect("resolve failed");
    let typed = assura_types::type_check(resolved).expect("type check failed");
    super::codegen_with_config(&typed, &config)
}

#[test]
fn cranelift_generates_cargo_config() {
    let source = "contract Add { requires(a: Int, b: Int) ensures(result: Int) }";
    let project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            backend: super::CodegenBackend::Cranelift,
            opt_level: 0,
            debug_info: true,
            target: super::CompileTarget::Native,
            ..Default::default()
        },
    );
    let cargo_config = project
        .files
        .iter()
        .find(|(path, _)| path == ".cargo/config.toml")
        .expect(".cargo/config.toml should be generated for Cranelift backend");
    assert!(
        cargo_config.1.contains("codegen-backend = \"cranelift\""),
        "config.toml should select cranelift backend"
    );
}

#[test]
fn cranelift_output_differs_from_rustc() {
    let source = "contract Add { requires(a: Int, b: Int) ensures(result: Int) }";
    let rustc_project = codegen_ok(source);
    let cranelift_project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            backend: super::CodegenBackend::Cranelift,
            opt_level: 0,
            debug_info: true,
            target: super::CompileTarget::Native,
            ..Default::default()
        },
    );
    assert!(
        cranelift_project.files.len() > rustc_project.files.len(),
        "Cranelift should produce .cargo/config.toml that Rustc does not"
    );
}

#[test]
fn rustc_has_no_cargo_config() {
    let source = "contract Add { requires(a: Int, b: Int) ensures(result: Int) }";
    let project = codegen_ok(source);
    assert!(
        !project
            .files
            .iter()
            .any(|(path, _)| path.contains("config.toml")),
        "Rustc backend should not produce .cargo/config.toml"
    );
}

#[test]
fn cranelift_adds_repr_c_to_structs() {
    let source = "type Point { x: Int, y: Int }
contract UsePoint { requires(p: Point) ensures(result: Int) }";
    let project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            backend: super::CodegenBackend::Cranelift,
            opt_level: 0,
            debug_info: true,
            target: super::CompileTarget::Native,
            ..Default::default()
        },
    );
    let lib = project
        .files
        .iter()
        .find(|(p, _)| p.ends_with(".rs"))
        .unwrap();
    assert!(
        lib.1.contains("#[repr(C)]"),
        "Cranelift codegen should add #[repr(C)] to structs:\n{}",
        lib.1
    );

    // Rustc backend should NOT have #[repr(C)]
    let rustc_project = codegen_ok(source);
    let rustc_lib = &rustc_project.files[0].1;
    assert!(
        !rustc_lib.contains("#[repr(C)]"),
        "Rustc codegen should not have #[repr(C)]"
    );
}

#[test]
fn cranelift_adds_no_mangle_extern_c() {
    let source = "contract Add { requires(a: Int, b: Int) ensures(result: Int) }";
    let project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            backend: super::CodegenBackend::Cranelift,
            opt_level: 0,
            debug_info: true,
            target: super::CompileTarget::Native,
            ..Default::default()
        },
    );
    let lib = project
        .files
        .iter()
        .find(|(p, _)| p.ends_with(".rs"))
        .unwrap();
    assert!(
        lib.1.contains("#[no_mangle]"),
        "Cranelift codegen should add #[no_mangle]:\n{}",
        lib.1
    );
    assert!(
        lib.1.contains("extern \"C\" fn"),
        "Cranelift codegen should use extern \"C\" fn:\n{}",
        lib.1
    );
}

#[test]
fn cranelift_skips_proptest() {
    // Must use input() clause to trigger proptest generation
    let source = "contract Add { input(a: Int, b: Int) requires(a > 0) ensures(result == a + b) ensures(result: Int) }";
    let rustc_project = codegen_ok(source);
    let rustc_lib = &rustc_project.files[0].1;
    let cranelift_project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            backend: super::CodegenBackend::Cranelift,
            opt_level: 0,
            debug_info: true,
            target: super::CompileTarget::Native,
            ..Default::default()
        },
    );
    let cl_lib = cranelift_project
        .files
        .iter()
        .find(|(p, _)| p.ends_with(".rs"))
        .unwrap();
    assert!(
        rustc_lib.contains("proptest"),
        "Rustc codegen should include proptest"
    );
    assert!(
        !cl_lib.1.contains("proptest"),
        "Cranelift codegen should skip proptest for fast dev builds"
    );
}

// =======================================================================
// Generated Rust compilation tests
// =======================================================================

/// Verify generated Rust for a contract parses as valid Rust syntax.
fn assert_generated_rust_valid(source: &str) {
    let project = codegen_ok(source);
    let lib = &project.files[0].1;
    syn::parse_file(lib).unwrap_or_else(|e| {
        panic!("generated Rust is not valid syntax:\n{lib}\n\nerror: {e}");
    });
}

#[test]
fn generated_rust_contract_is_valid() {
    assert_generated_rust_valid(
        r#"
contract SafeDivision {
  input(a: Int, b: Int)
  output(result: Int)
  requires { b != 0 }
  ensures { result * b == a }
  effects { pure }
}
"#,
    );
}

#[test]
fn generated_rust_fn_is_valid() {
    assert_generated_rust_valid(
        r#"
fn clamp(x: Int, lo: Int, hi: Int) -> Int
  requires { lo <= hi }
  ensures { result >= lo && result <= hi }
{
  if x < lo then lo else if x > hi then hi else x
}
"#,
    );
}

#[test]
fn generated_rust_service_is_valid() {
    let source = std::fs::read_to_string("../assura-cli/../../tests/fixtures/service_full.assura")
        .unwrap_or_else(|_| {
            std::fs::read_to_string("tests/fixtures/service_full.assura")
                .expect("cannot find service_full fixture")
        });
    let project = codegen_ok(&source);
    let lib = &project.files[0].1;
    syn::parse_file(lib).unwrap_or_else(|e| {
        panic!("service generated Rust is not valid:\n{lib}\n\nerror: {e}");
    });
}

#[test]
fn generated_rust_demo_libwebp_is_valid() {
    let source = std::fs::read_to_string("../assura-cli/../../demos/libwebp-huffman.assura")
        .unwrap_or_else(|_| {
            // Fallback path when running from workspace root
            std::fs::read_to_string("demos/libwebp-huffman.assura")
                .expect("cannot find libwebp demo")
        });
    let project = codegen_ok(&source);
    let lib = &project.files[0].1;
    syn::parse_file(lib).unwrap_or_else(|e| {
        panic!("libwebp generated Rust is not valid:\n{lib}\n\nerror: {e}");
    });
}

#[test]
fn codegen_with_config_produces_profile() {
    let config = super::BackendConfig {
        backend: super::CodegenBackend::Rustc,
        opt_level: 3,
        debug_info: true,
        target: super::CompileTarget::Native,
        ..Default::default()
    };
    let project = {
        let file = assura_parser::parse_unwrap("");
        let resolved = assura_resolve::resolve(&file).expect("resolve failed");
        let typed = assura_types::type_check(resolved).expect("type check failed");
        super::codegen_with_config(&typed, &config)
    };
    assert!(project.cargo_toml.contains("opt-level = 3"));
    assert!(project.cargo_toml.contains("debug = true"));
}

#[test]
fn pattern_to_rust_constructor_with_fields() {
    use assura_ast::Pattern;
    let pat = Pattern::Constructor {
        name: "Some".into(),
        fields: vec![Pattern::Ident("x".into())],
    };
    assert_eq!(super::pattern_to_rust(&pat), "Some(x)");
}

#[test]
fn pattern_to_rust_constructor_no_fields() {
    use assura_ast::Pattern;
    let pat = Pattern::Constructor {
        name: "None".into(),
        fields: vec![],
    };
    assert_eq!(super::pattern_to_rust(&pat), "None");
}

#[test]
fn pattern_to_rust_nested_constructor() {
    use assura_ast::Pattern;
    let pat = Pattern::Constructor {
        name: "Ok".into(),
        fields: vec![Pattern::Constructor {
            name: "Some".into(),
            fields: vec![Pattern::Ident("v".into())],
        }],
    };
    assert_eq!(super::pattern_to_rust(&pat), "Ok(Some(v))");
}

#[test]
fn pattern_to_rust_tuple_nested() {
    use assura_ast::Pattern;
    let pat = Pattern::Tuple(vec![
        Pattern::Ident("a".into()),
        Pattern::Tuple(vec![Pattern::Ident("b".into()), Pattern::Wildcard]),
    ]);
    assert_eq!(super::pattern_to_rust(&pat), "(a, (b, _))");
}

// =======================================================================
// Interface trait generation tests (T062)
// =======================================================================

#[test]
fn interface_block_generates_trait() {
    let mut code = String::new();
    let body = vec![
        Clause {
            kind: ClauseKind::Other("method".into()),
            body: Spanned::no_span(Expr::Ident("process".into())),
            effect_variables: vec![],
        },
        Clause {
            kind: ClauseKind::Other("method".into()),
            body: Spanned::no_span(Expr::Ident("validate".into())),
            effect_variables: vec![],
        },
    ];
    super::generate_interface_trait("Processor", &body, &mut code);
    assert!(
        code.contains("pub trait Processor"),
        "should generate trait: {code}"
    );
    assert!(
        code.contains("fn process(&self)"),
        "should have process method: {code}"
    );
    assert!(
        code.contains("fn validate(&self)"),
        "should have validate method: {code}"
    );
}

#[test]
fn interface_with_extends_generates_supertrait() {
    let mut code = String::new();
    let body = vec![
        Clause {
            kind: ClauseKind::Other("extends".into()),
            body: Spanned::no_span(Expr::Ident("Base".into())),
            effect_variables: vec![],
        },
        Clause {
            kind: ClauseKind::Other("method".into()),
            body: Spanned::no_span(Expr::Ident("extra".into())),
            effect_variables: vec![],
        },
    ];
    super::generate_interface_trait("Extended", &body, &mut code);
    assert!(
        code.contains("pub trait Extended: Base"),
        "should have supertrait bound: {code}"
    );
}

#[test]
fn interface_with_invariant_generates_provided_method() {
    let mut code = String::new();
    let body = vec![Clause {
        kind: ClauseKind::Invariant,
        body: Spanned::no_span(Expr::BinOp {
            lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
            op: BinOp::Gt,
            rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
        }),
        effect_variables: vec![],
    }];
    super::generate_interface_trait("Positive", &body, &mut code);
    assert!(
        code.contains("fn check_invariant"),
        "should generate invariant check: {code}"
    );
    assert!(
        code.contains("debug_assert!"),
        "should contain debug_assert: {code}"
    );
}

#[test]
fn interface_contract_generates_trait() {
    // Contract with an `interface` clause should produce a trait, not a module
    let source = r#"
contract Sortable {
  interface: true
  method: compare
  method: swap
}
"#;
    let project = codegen_ok(source);
    let lib = &project.files[0].1;
    assert!(
        lib.contains("trait Sortable"),
        "interface contract should generate trait: {lib}"
    );
    assert!(
        !lib.contains("mod contract_sortable"),
        "interface contract should NOT generate module: {lib}"
    );
}

#[test]
fn implements_contract_generates_impl_block() {
    // Contract with `implements` clause should generate struct + impl.
    // With 2 contracts this triggers multi-file mode.
    let source = r#"
contract Sortable {
  interface: true
  method: compare
}

contract MySorter {
  implements: Sortable
  method: compare
  requires { x > 0 }
}
"#;
    let project = codegen_ok(source);

    // Multi-file mode: lib.rs has mod declarations, contract files have contents
    let find_file = |name: &str| -> &str {
        &project
            .files
            .iter()
            .find(|(p, _)| p == name)
            .unwrap_or_else(|| {
                panic!(
                    "missing file {name}: files={:?}",
                    project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
                )
            })
            .1
    };

    let lib = find_file("src/lib.rs");
    assert!(
        lib.contains("pub mod contract_sortable;"),
        "lib.rs should declare sortable module: {lib}"
    );
    assert!(
        lib.contains("pub mod contract_mysorter;"),
        "lib.rs should declare mysorter module: {lib}"
    );

    let sortable = find_file("src/contract_sortable.rs");
    assert!(
        sortable.contains("trait Sortable"),
        "sortable module should contain trait: {sortable}"
    );

    let mysorter = find_file("src/contract_mysorter.rs");
    assert!(
        mysorter.contains("struct MySorter"),
        "mysorter module should contain struct: {mysorter}"
    );
    assert!(
        mysorter.contains("impl Sortable for MySorter"),
        "mysorter module should contain impl block: {mysorter}"
    );
}

#[test]
fn forall_ensures_generates_iter_all() {
    let project = codegen_ok(
        r#"
contract AllPositive {
    input(values: List<Int>)
    requires { forall v in values: v > 0 }
    ensures  { forall v in result: v > 0 }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains(".iter().all("),
        "forall in ensures should generate .iter().all(): {lib}"
    );
    assert!(
        lib.contains(&format!("{RESULT_VAR}.iter().all(")),
        "result in forall ensures should map to result var: {lib}"
    );
}

#[test]
fn exists_ensures_generates_iter_any() {
    let project = codegen_ok(
        r#"
contract HasPositive {
    input(values: List<Int>)
    ensures  { exists v in result: v > 0 }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains(".iter().any("),
        "exists in ensures should generate .iter().any(): {lib}"
    );
}

#[test]
fn raw_forall_tokens_converted() {
    // Test the raw_tokens_to_rust helper directly
    let tokens: Vec<String> = vec!["forall", "v", "in", "items", ":", "v", ">", "0"]
        .into_iter()
        .map(String::from)
        .collect();
    let result = raw_tokens_to_rust(&tokens);
    assert!(
        result.contains(".iter().all("),
        "raw forall tokens should produce .iter().all(): {result}"
    );
    assert!(result.contains("|v|"), "should bind variable v: {result}");
}

#[test]
fn raw_exists_tokens_converted() {
    let tokens: Vec<String> = vec!["exists", "x", "in", "data", ":", "x", "==", "target"]
        .into_iter()
        .map(String::from)
        .collect();
    let result = raw_tokens_to_rust(&tokens);
    assert!(
        result.contains(".iter().any("),
        "raw exists tokens should produce .iter().any(): {result}"
    );
}

#[test]
fn raw_result_keyword_replaced() {
    let tokens: Vec<String> = vec!["result", ">=", "0"]
        .into_iter()
        .map(String::from)
        .collect();
    let result = raw_tokens_to_rust(&tokens);
    assert!(
        result.contains(RESULT_VAR),
        "result keyword in raw tokens should become result var: {result}"
    );
}

#[test]
fn enum_generates_exhaustiveness_check() {
    let project = codegen_ok(
        r#"
enum Color {
    Red,
    Green,
    Blue,
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("__exhaustive_check_color"),
        "enum should generate exhaustiveness check function: {lib}"
    );
    assert!(
        lib.contains("Color::Red =>"),
        "exhaustiveness check should cover Red variant: {lib}"
    );
    assert!(
        lib.contains("Color::Green =>"),
        "exhaustiveness check should cover Green variant: {lib}"
    );
    assert!(
        lib.contains("Color::Blue =>"),
        "exhaustiveness check should cover Blue variant: {lib}"
    );
    // Should NOT have a wildcard arm
    assert!(
        !lib.contains("_ =>"),
        "exhaustiveness check must not have a wildcard arm: {lib}"
    );
}

#[test]
fn enum_with_data_generates_exhaustiveness_check() {
    let project = codegen_ok(
        r#"
enum Value {
    Num(Int),
    Text(String),
    Empty,
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("__exhaustive_check_value"),
        "data enum should generate exhaustiveness check: {lib}"
    );
    assert!(
        lib.contains("Value::Num(_)"),
        "data variant should use wildcard field: {lib}"
    );
    assert!(
        lib.contains("Value::Empty =>"),
        "unit variant should be covered: {lib}"
    );
}

#[test]
fn extract_input_params_single_cast() {
    // Top-level Cast: input(a as Int) at top level
    let mut params = Vec::new();
    let body = Spanned::no_span(Expr::Cast {
        expr: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        ty: "Int".into(),
    });
    extract_input_params(&body, &mut params);
    assert_eq!(params.len(), 1);
    assert_eq!(params[0].0, "a");
}

#[test]
fn extract_input_params_single_ident() {
    let mut params = Vec::new();
    let body = Spanned::no_span(Expr::Ident("x".into()));
    extract_input_params(&body, &mut params);
    assert_eq!(params.len(), 1);
    assert_eq!(params[0], ("x".to_string(), "i64".to_string()));
}

#[test]
fn extract_input_params_raw_as() {
    let mut params = Vec::new();
    let tokens = vec![
        "a".into(),
        "as".into(),
        "Int".into(),
        ",".into(),
        "b".into(),
        "as".into(),
        "String".into(),
    ];
    let body = Spanned::no_span(Expr::Raw(tokens));
    extract_input_params(&body, &mut params);
    assert_eq!(params.len(), 2);
    assert_eq!(params[0].0, "a");
    assert_eq!(params[1].0, "b");
}

#[test]
fn extract_input_params_raw_bare_idents() {
    let mut params = Vec::new();
    let tokens = vec!["buf".into(), ",".into(), "n".into()];
    let body = Spanned::no_span(Expr::Raw(tokens));
    extract_input_params(&body, &mut params);
    assert_eq!(params.len(), 2);
    assert_eq!(params[0].0, "buf");
    assert_eq!(params[1].0, "n");
}

#[test]
fn extract_output_type_ident() {
    let body = Spanned::no_span(Expr::Ident("Int".into()));
    let ty = extract_output_type(&body);
    assert_eq!(ty, "i64");
}

#[test]
fn extract_output_type_raw_as() {
    let tokens = vec!["result".into(), "as".into(), "Bool".into()];
    let body = Spanned::no_span(Expr::Raw(tokens));
    let ty = extract_output_type(&body);
    assert_eq!(ty, "bool");
}

#[test]
fn extract_output_name_cast() {
    // output(value: Nat) -> Cast { expr: Ident("value"), ty: "Nat" }
    let body = Spanned::no_span(Expr::Cast {
        expr: Box::new(Spanned::no_span(Expr::Ident("value".into()))),
        ty: "Nat".into(),
    });
    assert_eq!(extract_output_name(&body), Some("value".into()));
}

#[test]
fn extract_output_name_result_is_none() {
    // output(result: Int) -> result is already aliased, no extra binding needed
    let body = Spanned::no_span(Expr::Cast {
        expr: Box::new(Spanned::no_span(Expr::Ident("result".into()))),
        ty: "Int".into(),
    });
    assert_eq!(extract_output_name(&body), None);
}

#[test]
fn extract_output_name_call_with_cast() {
    // output(value: Nat) parsed as Call { func: "output", args: [Cast] }
    let body = Spanned::no_span(Expr::Call {
        func: Box::new(Spanned::no_span(Expr::Ident("output".into()))),
        args: vec![Spanned::no_span(Expr::Cast {
            expr: Box::new(Spanned::no_span(Expr::Ident("segment".into()))),
            ty: "FtsSegment".into(),
        })],
    });
    assert_eq!(extract_output_name(&body), Some("segment".into()));
}

#[test]
fn contract_named_output_binds_variable() {
    let project = codegen_ok(
        r#"
contract SafeAccess {
    input(buffer: Bytes, index: Nat)
    output(value: Nat)
    requires { index >= 0 }
    ensures  { value >= 0 }
    effects  { pure }
}
"#,
    );
    let lib = &project.files[0].1;
    // The generated code must bind `value` from result var so ensures can reference it
    assert!(
        lib.contains(&format!("let value = {RESULT_VAR}.clone()")),
        "generated code must bind output variable name: {lib}"
    );
}

#[test]
fn extract_output_name_raw_colon() {
    // output(value : Nat) parsed as Raw tokens ["value", ":", "Nat"]
    let tokens = vec!["value".into(), ":".into(), "Nat".into()];
    let body = Spanned::no_span(Expr::Raw(tokens));
    assert_eq!(extract_output_name(&body), Some("value".into()));
}

#[test]
fn extract_output_name_ident_only_is_none() {
    // output(Nat) - type only, no named binding
    let body = Spanned::no_span(Expr::Ident("Nat".into()));
    assert_eq!(extract_output_name(&body), None);
}

#[test]
fn contract_effects_generates_doc_comment() {
    let project = codegen_ok(
        r#"
contract Alloc {
    effects  { io }
    requires { true }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("/// Effects:"),
        "effects clause should produce doc comment"
    );
}

#[test]
fn contract_modifies_generates_doc_comment() {
    let project = codegen_ok(
        r#"
contract Mutator {
    modifies { buffer }
    requires { true }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("/// Modifies:"),
        "modifies clause should produce doc comment"
    );
}

#[test]
fn contract_requires_generates_doc_comment() {
    let project = codegen_ok(
        r#"
contract Bounded {
    requires { true }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("/// Requires:"),
        "requires clause should produce doc comment: {lib}"
    );
}

#[test]
fn service_operation_requires_generates_doc_comment() {
    let project = codegen_ok(
        r#"
service Validator {
    states: Idle -> Busy

    operation Validate {
        requires { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("/// Requires:"),
        "requires clause in service operation should produce doc comment: {lib}"
    );
}

#[test]
fn service_operation_modifies_generates_doc_comment() {
    let project = codegen_ok(
        r#"
service Storage {
    states: Empty -> Full

    operation Store {
        modifies { buffer }
        requires { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("/// Modifies:"),
        "modifies clause in service operation should produce doc comment: {lib}"
    );
}

#[test]
fn service_operation_invariant_generates_debug_assert() {
    let project = codegen_ok(
        r#"
service Counter {
    states: Ready -> Done

    operation Increment {
        invariant { true }
        requires  { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    // requires produces one debug_assert, invariant produces another
    let assert_count = lib.matches("debug_assert!").count();
    assert!(
        assert_count >= 2,
        "should have debug_assert for both requires and invariant, got {assert_count}: {lib}"
    );
}

#[test]
fn contract_invariant_generates_debug_assert() {
    let project = codegen_ok(
        r#"
contract Stable {
    invariant { true }
    requires  { true }
}
"#,
    );
    let lib = &project.files[0].1;
    // requires produces one debug_assert, invariant produces another
    let assert_count = lib.matches("debug_assert!").count();
    assert!(
        assert_count >= 2,
        "should have debug_assert for both requires and invariant, got {assert_count}"
    );
}

// S008: Typestate codegen tests

#[test]
fn s008_typestate_marker_structs_generated() {
    let project = codegen_ok(
        r#"
service Door {
    states: Locked -> Unlocked -> Open
    operation Unlock {
        requires { self.state == Locked }
        ensures { self.state == Unlocked }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("pub struct Locked"),
        "should generate Locked marker struct: {lib}"
    );
    assert!(
        lib.contains("pub struct Unlocked"),
        "should generate Unlocked marker struct: {lib}"
    );
    assert!(
        lib.contains("pub struct Open"),
        "should generate Open marker struct: {lib}"
    );
    // Should NOT generate enum State
    assert!(
        !lib.contains("enum State"),
        "typestate should not generate enum State: {lib}"
    );
}

#[test]
fn s008_typestate_generic_struct_with_phantom() {
    let project = codegen_ok(
        r#"
service Door {
    states: Locked -> Unlocked
    operation Unlock {
        requires { self.state == Locked }
        ensures { self.state == Unlocked }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("struct Door<State>"),
        "service struct should be generic: {lib}"
    );
    assert!(
        lib.contains("PhantomData<State>"),
        "struct should contain PhantomData: {lib}"
    );
}

#[test]
fn s008_typestate_constructor_on_initial_state() {
    let project = codegen_ok(
        r#"
service Workflow {
    states: Pending -> Active -> Complete
    operation Activate {
        requires { self.state == Pending }
        ensures { self.state == Active }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("impl Workflow<Pending>"),
        "new() should be on initial state impl block: {lib}"
    );
    assert!(
        lib.contains("fn new()"),
        "should generate constructor: {lib}"
    );
}

#[test]
fn s008_typestate_transition_consumes_self() {
    let project = codegen_ok(
        r#"
service Conn {
    states: Idle -> Active -> Closed
    operation Open {
        requires { self.state == Idle }
        ensures { self.state == Active }
    }
    operation Close {
        requires { self.state == Active }
        ensures { self.state == Closed }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    // Open should be on impl Conn<Idle> and return Conn<Active>
    assert!(
        lib.contains("impl Conn<Idle>"),
        "Open should be in Idle impl: {lib}"
    );
    assert!(
        lib.contains("fn Open(self) -> Conn<Active>"),
        "Open should consume self and return Conn<Active>: {lib}"
    );
    // Close should be on impl Conn<Active> and return Conn<Closed>
    assert!(
        lib.contains("impl Conn<Active>"),
        "Close should be in Active impl: {lib}"
    );
    assert!(
        lib.contains("fn Close(self) -> Conn<Closed>"),
        "Close should consume self and return Conn<Closed>: {lib}"
    );
}

#[test]
fn s008_typestate_stateless_service_unchanged() {
    let project = codegen_ok(
        r#"
service Simple {
    operation DoWork {
        requires { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    // Stateless service should NOT have PhantomData or marker structs
    assert!(
        !lib.contains("PhantomData"),
        "stateless service should not use PhantomData: {lib}"
    );
    assert!(
        lib.contains("struct Simple"),
        "stateless service should have simple struct: {lib}"
    );
    assert!(
        lib.contains("fn new()"),
        "stateless service should have constructor: {lib}"
    );
}

#[test]
fn s008_typestate_query_uses_ref_self() {
    let project = codegen_ok(
        r#"
service Store {
    states: Ready -> Done
    query GetCount {
        output(count: Nat)
    }
}
"#,
    );
    let lib = &project.files[0].1;
    // Query without state guard goes in generic impl
    assert!(
        lib.contains("impl<S> Store<S>"),
        "state-independent query should be in generic impl: {lib}"
    );
    assert!(lib.contains("&self"), "query should use &self: {lib}");
}

// S009: Proptest generation tests

#[test]
fn s009_proptest_generated_for_contract_with_requires_ensures() {
    let project = codegen_ok(
        r#"
contract SafeDivision {
    input(a: Int, b: Int)
    requires { b != 0 }
    ensures { result * b + (a % b) == a }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("proptest!"),
        "should generate proptest macro: {lib}"
    );
    assert!(
        lib.contains("prop_assert!"),
        "ensures should become prop_assert: {lib}"
    );
    assert!(
        lib.contains("#[cfg(test)]"),
        "proptest module should be gated: {lib}"
    );
}

#[test]
fn s009_proptest_refines_strategy_for_neq_zero() {
    let project = codegen_ok(
        r#"
contract Div {
    input(a: Int, b: Int)
    requires { b != 0 }
    ensures { true }
}
"#,
    );
    let lib = &project.files[0].1;
    // #710: b != 0 should use prop_filter to preserve negative domain
    assert!(
        lib.contains("prop_filter") && lib.contains("!= 0"),
        "b != 0 should use prop_filter for full signed domain: {lib}"
    );
    // Should NOT have prop_assume for b since it was refined
    assert!(
        !lib.contains("prop_assume!"),
        "refined requires should not produce prop_assume: {lib}"
    );
}

#[test]
fn s009_proptest_unrefined_requires_becomes_prop_assume() {
    let project = codegen_ok(
        r#"
contract Complex {
    input(x: Int)
    requires { x * x > 10 }
    ensures { true }
}
"#,
    );
    let lib = &project.files[0].1;
    // Complex requires can't be refined, should become prop_assume
    assert!(
        lib.contains("prop_assume!"),
        "complex requires should become prop_assume: {lib}"
    );
}

#[test]
fn s009_proptest_not_generated_without_ensures() {
    let project = codegen_ok(
        r#"
contract NoEnsures {
    input(x: Int)
    requires { x > 0 }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        !lib.contains("proptest!"),
        "contract without ensures should not generate proptest: {lib}"
    );
}

#[test]
fn s009_proptest_not_generated_without_input() {
    let project = codegen_ok(
        r#"
contract NoInput {
    ensures { true }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        !lib.contains("proptest!"),
        "contract without input should not generate proptest: {lib}"
    );
}

#[test]
fn s009_cargo_toml_has_proptest_dev_dependency() {
    let project = codegen_ok(
        r#"
contract Testable {
    input(x: Int)
    ensures { true }
}
"#,
    );
    assert!(
        project.cargo_toml.contains("proptest"),
        "Cargo.toml should include proptest dev-dependency: {}",
        project.cargo_toml
    );
    assert!(
        project.cargo_toml.contains("[dev-dependencies]"),
        "should have dev-dependencies section: {}",
        project.cargo_toml
    );
}

#[test]
fn s009_cargo_toml_no_proptest_when_not_needed() {
    let project = codegen_ok(
        r#"
contract NotTestable {
    requires { true }
}
"#,
    );
    assert!(
        !project.cargo_toml.contains("proptest"),
        "Cargo.toml should not include proptest when no testable contracts: {}",
        project.cargo_toml
    );
}

// R002: Multi-file codegen tests

#[test]
fn single_contract_stays_in_lib_rs() {
    // A file with only one contract should produce a single lib.rs
    let project = codegen_ok(
        r#"
contract OnlyOne {
    input(x: Int)
    requires { x > 0 }
}
"#,
    );
    assert_eq!(project.files.len(), 1, "single contract = single file");
    assert_eq!(project.files[0].0, "src/lib.rs");
    assert!(
        project.files[0].1.contains("pub mod contract_onlyone"),
        "single contract should have inline module in lib.rs"
    );
}

#[test]
fn multi_contract_generates_separate_files() {
    let project = codegen_ok(
        r#"
type Point {
    x: Int
    y: Int
}

contract Alpha {
    input(a: Int)
    requires { a > 0 }
}

contract Beta {
    input(b: Int)
    ensures { result > 0 }
}
"#,
    );
    // Should produce: lib.rs, contract_alpha.rs, contract_beta.rs
    assert_eq!(
        project.files.len(),
        3,
        "two contracts = 3 files: {:?}",
        project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
    );

    let find_file = |name: &str| -> &str {
        &project
            .files
            .iter()
            .find(|(p, _)| p == name)
            .unwrap_or_else(|| {
                panic!(
                    "missing {name}: {:?}",
                    project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
                )
            })
            .1
    };

    let lib = find_file("src/lib.rs");
    // Shared types stay in lib.rs
    assert!(lib.contains("struct Point"), "shared type in lib.rs");
    // Module declarations for contracts
    assert!(
        lib.contains("pub mod contract_alpha;"),
        "lib.rs declares alpha module"
    );
    assert!(
        lib.contains("pub mod contract_beta;"),
        "lib.rs declares beta module"
    );
    // Contracts themselves should NOT be in lib.rs
    assert!(
        !lib.contains("pub fn check(a: i64)"),
        "contract body should not be inline in lib.rs"
    );

    let alpha = find_file("src/contract_alpha.rs");
    assert!(alpha.contains("use super::*"), "module imports parent");
    assert!(
        alpha.contains("pub fn check(a: i64)"),
        "alpha has check fn: {alpha}"
    );

    let beta = find_file("src/contract_beta.rs");
    assert!(
        beta.contains("pub fn check(b: i64)"),
        "beta has check fn: {beta}"
    );
}

#[test]
fn multi_file_with_service() {
    let project = codegen_ok(
        r#"
contract Guard {
    input(x: Int)
    requires { x >= 0 }
}

service Counter {
    states: Idle -> Running -> Done
    operation Start {
        requires: true
        effects: io
    }
}
"#,
    );
    // contract + service = 2 modules -> multi-file
    assert_eq!(
        project.files.len(),
        3,
        "contract + service = 3 files: {:?}",
        project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
    );

    let find_file = |name: &str| -> &str {
        &project
            .files
            .iter()
            .find(|(p, _)| p == name)
            .unwrap_or_else(|| {
                panic!(
                    "missing {name}: {:?}",
                    project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
                )
            })
            .1
    };

    let lib = find_file("src/lib.rs");
    assert!(lib.contains("pub mod contract_guard;"));
    assert!(lib.contains("pub mod counter;"));

    let guard = find_file("src/contract_guard.rs");
    assert!(guard.contains("pub fn check"));

    let counter = find_file("src/counter.rs");
    assert!(counter.contains("struct Counter"));
    // S008: typestate encoding generates marker structs, not enum State
    assert!(
        counter.contains("pub struct Idle"),
        "should contain state marker struct: {counter}"
    );
}

#[test]
fn multi_file_shared_types_not_duplicated() {
    // Types, enums, and externs stay in lib.rs, not in contract files
    let project = codegen_ok(
        r#"
type MyData {
    value: Int
}

enum Status {
    Active,
    Inactive
}

contract First {
    input(x: Int)
    requires { x > 0 }
}

contract Second {
    input(y: Int)
    ensures { result > 0 }
}
"#,
    );

    let find_file = |name: &str| -> &str {
        &project
            .files
            .iter()
            .find(|(p, _)| p == name)
            .unwrap_or_else(|| {
                panic!(
                    "missing {name}: {:?}",
                    project.files.iter().map(|(p, _)| p).collect::<Vec<_>>()
                )
            })
            .1
    };

    let lib = find_file("src/lib.rs");
    assert!(
        lib.contains("struct MyData"),
        "shared type in lib.rs: {lib}"
    );
    assert!(lib.contains("enum Status"), "shared enum in lib.rs: {lib}");

    let first = find_file("src/contract_first.rs");
    assert!(
        !first.contains("struct MyData"),
        "type should not be in contract file"
    );
    assert!(
        !first.contains("enum Status"),
        "enum should not be in contract file"
    );
}

// --- P004: Error handling codegen tests ---

#[test]
fn contract_with_errors_generates_error_enum() {
    let project = codegen_ok(
        r#"
contract SafeDivision {
    input  { a: Int, b: Int }
    output { result: Int }
    errors { DivByZero, Overflow }
    requires { b != 0 }
    ensures  { result * b == a }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("SafeDivisionError"),
        "should generate error enum: {lib}"
    );
    assert!(
        lib.contains("DivByZero"),
        "should contain DivByZero variant: {lib}"
    );
    assert!(
        lib.contains("Overflow"),
        "should contain Overflow variant: {lib}"
    );
    assert!(
        lib.contains("thiserror::Error"),
        "should derive thiserror::Error: {lib}"
    );
}

#[test]
fn contract_with_errors_returns_result() {
    let project = codegen_ok(
        r#"
contract Validator {
    input  { data: Int }
    output { result: Bool }
    errors { InvalidInput }
    ensures { result == true }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(lib.contains("Result<"), "should return Result type: {lib}");
    assert!(
        lib.contains("ValidatorError"),
        "should reference error type: {lib}"
    );
    assert!(
        lib.contains(&format!("Ok({RESULT_VAR})")),
        "should wrap result in Ok: {lib}"
    );
}

#[test]
fn contract_without_errors_no_result_type() {
    let project = codegen_ok(
        r#"
contract Simple {
    input  { x: Int }
    output { result: Int }
    requires { x > 0 }
    ensures  { result > 0 }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        !lib.contains("Result<"),
        "should not use Result without errors: {lib}"
    );
    assert!(
        !lib.contains("thiserror"),
        "should not include thiserror: {lib}"
    );
}

#[test]
fn extract_error_variants_from_raw() {
    let body = Spanned::no_span(Expr::Raw(vec![
        "DivByZero".into(),
        ",".into(),
        "Overflow".into(),
    ]));
    let variants = extract_error_variants(&body);
    assert_eq!(variants, vec!["DivByZero", "Overflow"]);
}

#[test]
fn extract_error_variants_from_ident() {
    let body = Spanned::no_span(Expr::Ident("SingleError".into()));
    let variants = extract_error_variants(&body);
    assert_eq!(variants, vec!["SingleError"]);
}

#[test]
fn generate_error_enum_output() {
    let mut code = String::new();
    generate_error_enum("Parser", &["BadInput".into(), "TooLong".into()], &mut code);
    assert!(code.contains("pub enum ParserError"));
    assert!(code.contains("BadInput"));
    assert!(code.contains("TooLong"));
    assert!(code.contains("thiserror::Error"));
}

#[test]
fn errors_clause_adds_thiserror_dep() {
    let project = codegen_ok(
        r#"
contract WithErrors {
    input  { x: Int }
    errors { SomeError }
    requires { x > 0 }
}
"#,
    );
    assert!(
        project.cargo_toml.contains("thiserror"),
        "Cargo.toml should include thiserror: {}",
        project.cargo_toml
    );
}

#[test]
fn no_errors_no_thiserror_dep() {
    let project = codegen_ok(
        r#"
contract NoErrors {
    input  { x: Int }
    requires { x > 0 }
}
"#,
    );
    assert!(
        !project.cargo_toml.contains("thiserror"),
        "Cargo.toml should not include thiserror: {}",
        project.cargo_toml
    );
}

// --- WASM target tests ---

fn codegen_wasm(source: &str) -> GeneratedProject {
    let file = assura_parser::parse_unwrap(source);
    let resolved = assura_resolve::resolve(&file).expect("resolve failed");
    let typed = assura_types::type_check(resolved).expect("type check failed");
    let config = BackendConfig {
        target: CompileTarget::Wasm,
        ..BackendConfig::default()
    };
    codegen_with_config(&typed, &config)
}

#[test]
fn wasm_target_cargo_toml_has_comment() {
    let project = codegen_wasm("");
    assert!(
        project.cargo_toml.contains("wasm32-wasip1"),
        "WASM Cargo.toml should mention wasm32-wasip1: {}",
        project.cargo_toml
    );
}

#[test]
fn native_target_no_wasm_comment() {
    let project = codegen_ok("");
    assert!(
        !project.cargo_toml.contains("wasm32-wasip1"),
        "Native Cargo.toml should not mention wasm32-wasip1"
    );
}

#[test]
fn compile_target_from_str() {
    assert_eq!(
        CompileTarget::from_str_loose("native"),
        Some(CompileTarget::Native)
    );
    assert_eq!(
        CompileTarget::from_str_loose("wasm"),
        Some(CompileTarget::Wasm)
    );
    assert_eq!(
        CompileTarget::from_str_loose("wasm32-wasi"),
        Some(CompileTarget::Wasm)
    );
    assert_eq!(
        CompileTarget::from_str_loose("wasm32-wasip1"),
        Some(CompileTarget::Wasm)
    );
    assert_eq!(CompileTarget::from_str_loose("unknown"), None);
}

#[test]
fn compile_target_rust_target() {
    assert_eq!(CompileTarget::Native.rust_target(), None);
    assert_eq!(CompileTarget::Wasm.rust_target(), Some("wasm32-wasip1"));
}

// --- Bind codegen tests ---

#[test]
fn bind_generates_checked_wrapper() {
    let project = codegen_ok(
        r#"
bind "std::cmp::max" as safe_max {
    input(a: Int, b: Int)
    output(result: Int)
    requires a >= 0
    ensures result >= a
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("fn safe_max"),
        "should generate safe_max fn: {lib}"
    );
    assert!(
        lib.contains("std::cmp::max("),
        "should call the bound Rust function: {lib}"
    );
    assert!(
        lib.contains("debug_assert!"),
        "should have contract assertions: {lib}"
    );
}

#[test]
fn bind_with_requires_and_ensures() {
    let project = codegen_ok(
        r#"
bind "my_crate::divide" as safe_divide {
    input(a: Int, b: Int)
    output(result: Int)
    requires b != 0
    ensures result * b == a
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("fn safe_divide"),
        "should generate safe_divide fn: {lib}"
    );
    assert!(
        lib.contains("my_crate::divide("),
        "should call the bound Rust function: {lib}"
    );
}

#[test]
fn collect_type_refs_from_nested_exprs() {
    use assura_ast::*;
    let mut out = std::collections::HashSet::new();

    // Type ref inside a Match arm body
    let expr = Spanned::no_span(Expr::Match {
        scrutinee: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        arms: vec![MatchArm {
            pattern: Pattern::Wildcard,
            body: Spanned::no_span(Expr::Call {
                func: Box::new(Spanned::no_span(Expr::Ident("MyType".into()))),
                args: vec![],
            }),
        }],
    });
    collect_type_refs_from_expr(&expr, &mut out);
    assert!(
        out.contains("MyType"),
        "should find type ref in Match arm body, got: {out:?}"
    );

    // Type ref inside a Let body
    out.clear();
    let expr = Spanned::no_span(Expr::Let {
        name: "x".into(),
        value: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("1".into())))),
        body: Box::new(Spanned::no_span(Expr::Ident("SomeType".into()))),
    });
    collect_type_refs_from_expr(&expr, &mut out);
    assert!(
        out.contains("SomeType"),
        "should find type ref in Let body, got: {out:?}"
    );

    // Type ref inside a Tuple
    out.clear();
    let expr = Spanned::no_span(Expr::Tuple(vec![
        Spanned::no_span(Expr::Ident("x".into())),
        Spanned::no_span(Expr::Ident("CustomStruct".into())),
    ]));
    collect_type_refs_from_expr(&expr, &mut out);
    assert!(
        out.contains("CustomStruct"),
        "should find type ref in Tuple, got: {out:?}"
    );
}

#[test]
fn feature_max_missing_value_emits_compile_error() {
    // A feature_max referenced but with no extractable value should
    // produce compile_error! in the generated code, not a silent "0".
    let source = r#"
feature_max UNKNOWN_CONST

contract UseConst {
    input(x: Int)
    requires { x <= UNKNOWN_CONST }
}
"#;
    let code = codegen_ok(source);
    let lib = &code.files[0].1;
    assert!(
        lib.contains("compile_error!"),
        "missing feature_max value should produce compile_error!, got:\n{lib}"
    );
}

// -------------------------------------------------------------------
// Issue #54: catch-all wildcard elimination tests
// -------------------------------------------------------------------

#[test]
fn extract_output_type_recurses_into_call_args() {
    // Previously a Tuple arg inside Call was silently skipped via _ => {}
    let body = Spanned::no_span(Expr::Call {
        func: Box::new(Spanned::no_span(Expr::Ident("output".into()))),
        args: vec![Spanned::no_span(Expr::Tuple(vec![Spanned::no_span(
            Expr::Cast {
                expr: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
                ty: "Int".into(),
            },
        )]))],
    });
    let ty = extract_output_type(&body);
    assert_eq!(ty, "i64", "should recurse into Tuple inside Call args");
}

#[test]
fn extract_error_variants_from_block() {
    // Previously Block fell through to _ => vec![]
    let body = Spanned::no_span(Expr::Block(vec![
        Spanned::no_span(Expr::Ident("ErrA".into())),
        Spanned::no_span(Expr::Ident("ErrB".into())),
    ]));
    let variants = extract_error_variants(&body);
    assert_eq!(variants, vec!["ErrA", "ErrB"]);
}

#[test]
fn extract_error_variants_from_list() {
    let body = Spanned::no_span(Expr::List(vec![
        Spanned::no_span(Expr::Ident("X".into())),
        Spanned::no_span(Expr::Ident("Y".into())),
    ]));
    let variants = extract_error_variants(&body);
    assert_eq!(variants, vec!["X", "Y"]);
}

#[test]
fn extract_error_variants_non_ident_returns_empty() {
    // BinOp cannot contain error variant names
    let body = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: assura_ast::BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    let variants = extract_error_variants(&body);
    assert!(variants.is_empty());
}

#[test]
fn generate_trait_method_unsupported_emits_compile_error() {
    // Previously unsupported Expr variants got a silent comment
    let body = Spanned::no_span(Expr::Literal(assura_ast::Literal::Int("42".into())));
    let mut code = String::new();
    generate_trait_method(&body, &mut code);
    assert!(
        code.contains("compile_error!"),
        "unsupported trait method body should emit compile_error!, got:\n{code}"
    );
}

#[test]
fn generate_block_effects_clause_explicit() {
    // Previously Effects fell through to _ => debug comment
    let clauses = vec![Clause {
        kind: ClauseKind::Effects,
        body: Spanned::no_span(Expr::Raw(vec!["io".into()])),
        effect_variables: vec![],
    }];
    let mut code = String::new();
    generate_block(&BlockKind::Feature, "test", &clauses, &mut code);
    assert!(
        code.contains("// Effects:"),
        "Effects clause should produce a line comment (not trailing ///), got:\n{code}"
    );
}

// -----------------------------------------------------------------
// G007: resolve_ordering_variant + codegen Ordering constant
// -----------------------------------------------------------------

#[test]
fn resolve_ordering_acquire() {
    let body = Spanned::no_span(Expr::Ident("acquire".into()));
    assert_eq!(resolve_ordering_variant(&body), Some("Acquire"));
}

#[test]
fn resolve_ordering_seq_cst() {
    let body = Spanned::no_span(Expr::Ident("seq_cst".into()));
    assert_eq!(resolve_ordering_variant(&body), Some("SeqCst"));
}

#[test]
fn resolve_ordering_raw_tokens() {
    let body = Spanned::no_span(Expr::Raw(vec!["release".into()]));
    assert_eq!(resolve_ordering_variant(&body), Some("Release"));
}

#[test]
fn resolve_ordering_unknown() {
    let body = Spanned::no_span(Expr::Ident("bogus".into()));
    assert_eq!(resolve_ordering_variant(&body), None);
}

#[test]
fn codegen_ordering_constant_in_block() {
    let clauses = vec![Clause {
        kind: ClauseKind::Ordering,
        body: Spanned::no_span(Expr::Ident("acquire".into())),
        effect_variables: vec![],
    }];
    let mut code = String::new();
    generate_block(&BlockKind::Feature, "test", &clauses, &mut code);
    assert!(
        code.contains("std::sync::atomic::Ordering::Acquire"),
        "ordering clause should emit Ordering constant, got:\n{code}"
    );
}

#[test]
fn codegen_codec_registry_dispatch() {
    use assura_ast::CodecEntry;
    let cr = CodecRegistryDecl {
        name: "ImageFormats".into(),
        output_type: vec!["ImageOutput".into()],
        codecs: vec![
            CodecEntry {
                name: "Png".into(),
                magic: MagicPattern::Bytes {
                    bytes: vec![0x89, 0x50, 0x4E, 0x47],
                    prefix: false,
                },
                decoder: "decode_png".into(),
                contracts: vec![],
            },
            CodecEntry {
                name: "Bmp".into(),
                magic: MagicPattern::Bytes {
                    bytes: vec![0x42, 0x4D],
                    prefix: true,
                },
                decoder: "decode_bmp".into(),
                contracts: vec![],
            },
        ],
    };
    let mut code = String::new();
    generate_codec_registry(&cr, &mut code);
    assert!(
        code.contains("pub fn dispatch_imageformats"),
        "should generate dispatch function, got:\n{code}"
    );
    assert!(
        code.contains("decode_png(data)"),
        "should call decode_png, got:\n{code}"
    );
    assert!(
        code.contains("decode_bmp(data)"),
        "should call decode_bmp, got:\n{code}"
    );
    assert!(
        code.contains("0x89"),
        "should check magic bytes, got:\n{code}"
    );
}

#[test]
fn codegen_codec_registry_probe() {
    use assura_ast::CodecEntry;
    let cr = CodecRegistryDecl {
        name: "Probed".into(),
        output_type: vec!["Out".into()],
        codecs: vec![CodecEntry {
            name: "Hdr".into(),
            magic: MagicPattern::Probe("is_hdr_format".into()),
            decoder: "decode_hdr".into(),
            contracts: vec![],
        }],
    };
    let mut code = String::new();
    generate_codec_registry(&cr, &mut code);
    assert!(
        code.contains("is_hdr_format(data)"),
        "should call probe function, got:\n{code}"
    );
}

#[test]
fn multi_file_includes_codec_registry() {
    // In multi-file mode, CodecRegistry should generate into shared lib.rs
    let project = codegen_ok(
        r#"
contract Guard {
    input(x: Int)
    requires { x >= 0 }
}

contract Shield {
    input(y: Int)
    ensures { result > 0 }
}

codec_registry ImageFormats {
    output: ImageOutput,
    codec Png {
        magic: [0x89, 0x50, 0x4E, 0x47]
        decoder: decode_png
    }
    codec Jpeg {
        magic: [0xFF, 0xD8]
        decoder: decode_jpeg
    }
}
"#,
    );
    // 2 contracts -> multi-file mode (lib.rs + 2 contract files)
    assert!(project.files.len() >= 3, "expected multi-file output");

    let lib_rs = project
        .files
        .iter()
        .find(|(p, _)| p == "src/lib.rs")
        .expect("missing src/lib.rs");
    assert!(
        lib_rs.1.contains("dispatch_imageformats") || lib_rs.1.contains("decode_png"),
        "lib.rs should contain codec registry dispatch, got:\n{}",
        &lib_rs.1[..lib_rs.1.len().min(500)]
    );
}

// =========================================================================
// #178 Regression: generated Rust must suppress all warning categories
// =========================================================================

/// Verify that generated code includes `#![allow(...)]` covering all warning
/// categories that Assura codegen is known to trigger: dead_code,
/// unused_variables, unused_parens, non_camel_case_types, unreachable_code.
#[test]
fn test_demo_codegen_warning_free() {
    // Use a contract with a SCREAMING_CASE constant (triggers non_camel_case_types
    // if not suppressed) and arithmetic in requires (triggers unused_parens).
    let src = r#"
        contract BoundsCheck {
            input { x: Int, MAX_SIZE: Nat }
            requires { (x + 1) >= 0 }
            ensures { result <= MAX_SIZE }
        }
    "#;
    let proj = codegen_ok(src);
    let (_, lib_rs) = proj
        .files
        .iter()
        .find(|(p, _)| p.ends_with(".rs"))
        .expect("no .rs file in generated project");

    // The allow attribute must cover all five warning categories
    for cat in &[
        "dead_code",
        "unused_variables",
        "unused_parens",
        "non_camel_case_types",
        "unreachable_code",
    ] {
        assert!(
            lib_rs.contains(cat),
            "generated code must #![allow({cat})] but it was missing"
        );
    }
}

// -----------------------------------------------------------------------
// expr.rs unit tests: is_numeric_expr
// -----------------------------------------------------------------------

#[test]
fn is_numeric_ident() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Ident("x".into()))));
}

#[test]
fn is_numeric_int_literal() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Literal(
        Literal::Int("42".into())
    ))));
}

#[test]
fn is_numeric_float_literal() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Literal(
        Literal::Float("3.14".into())
    ))));
}

#[test]
fn is_numeric_str_literal_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::Literal(
        Literal::Str("hello".into())
    ))));
}

#[test]
fn is_numeric_bool_literal_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::Literal(
        Literal::Bool(true)
    ))));
}

#[test]
fn is_numeric_field_access() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Field(
        Box::new(Spanned::no_span(Expr::Ident("obj".into()))),
        "count".into()
    ))));
}

#[test]
fn is_numeric_arithmetic_binop() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    })));
    assert!(is_numeric_expr(&Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Mod,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    })));
}

#[test]
fn is_numeric_logical_binop_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
        op: BinOp::And,
        rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(false)))),
    })));
}

#[test]
fn is_numeric_negation() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::UnaryOp {
        op: UnaryOp::Neg,
        expr: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
    })));
}

#[test]
fn is_numeric_not_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::UnaryOp {
        op: UnaryOp::Not,
        expr: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
    })));
}

#[test]
fn is_numeric_old_delegates() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Old(Box::new(
        Spanned::no_span(Expr::Ident("x".into()))
    )))));
}

#[test]
fn is_numeric_call() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Call {
        func: Box::new(Spanned::no_span(Expr::Ident("foo".into()))),
        args: vec![],
    })));
}

#[test]
fn is_numeric_index() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Index {
        expr: Box::new(Spanned::no_span(Expr::Ident("arr".into()))),
        index: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
    })));
}

#[test]
fn is_numeric_forall_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::Forall {
        var: "x".into(),
        domain: Box::new(Spanned::no_span(Expr::Ident("items".into()))),
        body: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
    })));
}

#[test]
fn is_numeric_list_false() {
    assert!(!is_numeric_expr(&Spanned::no_span(Expr::List(vec![]))));
}

#[test]
fn is_numeric_let_delegates() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::Let {
        name: "x".into(),
        value: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("1".into())))),
        body: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
    })));
}

#[test]
fn is_numeric_if_delegates_to_then() {
    assert!(is_numeric_expr(&Spanned::no_span(Expr::If {
        cond: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
        then_branch: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("1".into())))),
        else_branch: None,
    })));
}

// -----------------------------------------------------------------------
// expr.rs unit tests: expr_to_rust
// -----------------------------------------------------------------------

#[test]
fn expr_to_rust_int_literal() {
    let e = Spanned::no_span(Expr::Literal(Literal::Int("42".into())));
    assert_eq!(expr_to_rust(&e), "42");
}

#[test]
fn expr_to_rust_str_literal() {
    let e = Spanned::no_span(Expr::Literal(Literal::Str("hello".into())));
    assert_eq!(expr_to_rust(&e), "\"hello\"");
}

#[test]
fn expr_to_rust_bool_literal() {
    assert_eq!(
        expr_to_rust(&Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
        "true"
    );
    assert_eq!(
        expr_to_rust(&Spanned::no_span(Expr::Literal(Literal::Bool(false)))),
        "false"
    );
}

#[test]
fn expr_to_rust_result_keyword() {
    let e = Spanned::no_span(Expr::Ident("result".into()));
    assert_eq!(expr_to_rust(&e), RESULT_VAR);
}

#[test]
fn expr_to_rust_normal_ident() {
    let e = Spanned::no_span(Expr::Ident("foo".into()));
    assert_eq!(expr_to_rust(&e), "foo");
}

#[test]
fn expr_to_rust_field_access() {
    let e = Spanned::no_span(Expr::Field(
        Box::new(Spanned::no_span(Expr::Ident("obj".into()))),
        "len".into(),
    ));
    assert_eq!(expr_to_rust(&e), "obj.len");
}

#[test]
fn expr_to_rust_method_call() {
    let e = Spanned::no_span(Expr::MethodCall {
        receiver: Box::new(Spanned::no_span(Expr::Ident("v".into()))),
        method: "push".into(),
        args: vec![Spanned::no_span(Expr::Literal(Literal::Int("1".into())))],
    });
    assert_eq!(expr_to_rust(&e), "v.push(1)");
}

#[test]
fn expr_to_rust_function_call() {
    let e = Spanned::no_span(Expr::Call {
        func: Box::new(Spanned::no_span(Expr::Ident("f".into()))),
        args: vec![
            Spanned::no_span(Expr::Ident("a".into())),
            Spanned::no_span(Expr::Ident("b".into())),
        ],
    });
    assert_eq!(expr_to_rust(&e), "f(a, b)");
}

#[test]
fn expr_to_rust_index() {
    let e = Spanned::no_span(Expr::Index {
        expr: Box::new(Spanned::no_span(Expr::Ident("arr".into()))),
        index: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
    });
    assert_eq!(expr_to_rust(&e), "arr[0]");
}

#[test]
fn expr_to_rust_arithmetic() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    assert_eq!(expr_to_rust(&e), "(a + b)");
}

#[test]
fn expr_to_rust_implies() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("p".into()))),
        op: BinOp::Implies,
        rhs: Box::new(Spanned::no_span(Expr::Ident("q".into()))),
    });
    assert_eq!(expr_to_rust(&e), "(!p || q)");
}

#[test]
fn expr_to_rust_in_operator() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        op: BinOp::In,
        rhs: Box::new(Spanned::no_span(Expr::Ident("set".into()))),
    });
    assert_eq!(expr_to_rust(&e), "set.contains(&x)");
}

#[test]
fn expr_to_rust_not_in_operator() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        op: BinOp::NotIn,
        rhs: Box::new(Spanned::no_span(Expr::Ident("set".into()))),
    });
    assert_eq!(expr_to_rust(&e), "!set.contains(&x)");
}

#[test]
fn expr_to_rust_concat() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Concat,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    assert_eq!(expr_to_rust(&e), "[a, b].concat()");
}

#[test]
fn expr_to_rust_numeric_comparison_casts() {
    // Ordering comparisons on numeric exprs get i128::from() casts
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Lt,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    let result = expr_to_rust(&e);
    assert!(result.contains("i128::from(a)"), "got: {result}");
    assert!(result.contains("i128::from(b)"), "got: {result}");
}

#[test]
fn expr_to_rust_equality_no_cast() {
    // Equality doesn't get i128 casts
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Eq,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    assert_eq!(expr_to_rust(&e), "(a == b)");
}

#[test]
fn expr_to_rust_unary_neg() {
    let e = Spanned::no_span(Expr::UnaryOp {
        op: UnaryOp::Neg,
        expr: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
    });
    assert_eq!(expr_to_rust(&e), "(-x)");
}

#[test]
fn expr_to_rust_unary_not() {
    let e = Spanned::no_span(Expr::UnaryOp {
        op: UnaryOp::Not,
        expr: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
    });
    assert_eq!(expr_to_rust(&e), "(!true)");
}

#[test]
fn expr_to_rust_old() {
    let e = Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(Expr::Ident(
        "x".into(),
    )))));
    assert_eq!(expr_to_rust(&e), format!("{OLD_VAR_PREFIX}x"));
}

#[test]
fn expr_to_rust_forall() {
    let e = Spanned::no_span(Expr::Forall {
        var: "x".into(),
        domain: Box::new(Spanned::no_span(Expr::Ident("items".into()))),
        body: Box::new(Spanned::no_span(Expr::BinOp {
            lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
            op: BinOp::Gt,
            rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
        })),
    });
    let result = expr_to_rust(&e);
    assert!(result.contains(".iter().all(|x|"), "got: {result}");
}

#[test]
fn expr_to_rust_exists() {
    let e = Spanned::no_span(Expr::Exists {
        var: "x".into(),
        domain: Box::new(Spanned::no_span(Expr::Ident("items".into()))),
        body: Box::new(Spanned::no_span(Expr::BinOp {
            lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
            op: BinOp::Eq,
            rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
        })),
    });
    let result = expr_to_rust(&e);
    assert!(result.contains(".iter().any(|x|"), "got: {result}");
}

#[test]
fn expr_to_rust_if_else() {
    let e = Spanned::no_span(Expr::If {
        cond: Box::new(Spanned::no_span(Expr::Ident("cond".into()))),
        then_branch: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("1".into())))),
        else_branch: Some(Box::new(Spanned::no_span(Expr::Literal(Literal::Int(
            "2".into(),
        ))))),
    });
    let result = expr_to_rust(&e);
    assert!(result.contains("if cond"), "got: {result}");
    assert!(result.contains("else"), "got: {result}");
}

#[test]
fn expr_to_rust_if_no_else() {
    let e = Spanned::no_span(Expr::If {
        cond: Box::new(Spanned::no_span(Expr::Ident("cond".into()))),
        then_branch: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("1".into())))),
        else_branch: None,
    });
    let result = expr_to_rust(&e);
    assert!(result.contains("if cond"), "got: {result}");
    assert!(!result.contains("else"), "got: {result}");
}

#[test]
fn expr_to_rust_list() {
    let e = Spanned::no_span(Expr::List(vec![
        Spanned::no_span(Expr::Literal(Literal::Int("1".into()))),
        Spanned::no_span(Expr::Literal(Literal::Int("2".into()))),
    ]));
    assert_eq!(expr_to_rust(&e), "vec![1, 2]");
}

#[test]
fn expr_to_rust_cast() {
    let e = Spanned::no_span(Expr::Cast {
        expr: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        ty: "Int".into(),
    });
    let result = expr_to_rust(&e);
    assert!(result.contains("as i64"), "got: {result}");
}

#[test]
fn expr_to_rust_let_binding() {
    let e = Spanned::no_span(Expr::Let {
        name: "x".into(),
        value: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("5".into())))),
        body: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
    });
    assert_eq!(expr_to_rust(&e), "{ let x = 5; x }");
}

#[test]
fn expr_to_rust_tuple() {
    let e = Spanned::no_span(Expr::Tuple(vec![
        Spanned::no_span(Expr::Ident("a".into())),
        Spanned::no_span(Expr::Ident("b".into())),
    ]));
    assert_eq!(expr_to_rust(&e), "(a, b)");
}

#[test]
fn expr_to_rust_range() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
        op: BinOp::Range,
        rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("10".into())))),
    });
    assert_eq!(expr_to_rust(&e), "(0 .. 10)");
}

// -----------------------------------------------------------------------
// expr.rs unit tests: old_var_name
// -----------------------------------------------------------------------

#[test]
fn old_var_name_ident() {
    assert_eq!(
        old_var_name(&Spanned::no_span(Expr::Ident("x".into()))),
        "x"
    );
}

#[test]
fn old_var_name_field() {
    let e = Spanned::no_span(Expr::Field(
        Box::new(Spanned::no_span(Expr::Ident("buf".into()))),
        "len".into(),
    ));
    assert_eq!(old_var_name(&e), "buf_len");
}

#[test]
fn old_var_name_call() {
    let e = Spanned::no_span(Expr::Call {
        func: Box::new(Spanned::no_span(Expr::Ident("size".into()))),
        args: vec![],
    });
    assert_eq!(old_var_name(&e), "size");
}

#[test]
fn old_var_name_method_call() {
    let e = Spanned::no_span(Expr::MethodCall {
        receiver: Box::new(Spanned::no_span(Expr::Ident("v".into()))),
        method: "len".into(),
        args: vec![],
    });
    assert_eq!(old_var_name(&e), "v_len");
}

#[test]
fn old_var_name_index() {
    let e = Spanned::no_span(Expr::Index {
        expr: Box::new(Spanned::no_span(Expr::Ident("arr".into()))),
        index: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
    });
    assert_eq!(old_var_name(&e), "arr_idx");
}

#[test]
fn old_var_name_binop() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    assert_eq!(old_var_name(&e), "a_add_b");
}

#[test]
fn old_var_name_unary() {
    let e = Spanned::no_span(Expr::UnaryOp {
        op: UnaryOp::Neg,
        expr: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
    });
    assert_eq!(old_var_name(&e), "neg_x");
}

#[test]
fn old_var_name_literal() {
    assert_eq!(
        old_var_name(&Spanned::no_span(Expr::Literal(Literal::Int("42".into())))),
        "lit_42"
    );
    assert_eq!(
        old_var_name(&Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
        "lit_true"
    );
}

#[test]
fn old_var_name_old_delegates() {
    let e = Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(Expr::Ident(
        "z".into(),
    )))));
    assert_eq!(old_var_name(&e), "z");
}

#[test]
fn old_var_name_ghost() {
    let e = Spanned::no_span(Expr::Ghost(Box::new(Spanned::no_span(Expr::Ident(
        "g".into(),
    )))));
    assert_eq!(old_var_name(&e), "ghost_g");
}

#[test]
fn old_var_name_list_tuple() {
    assert_eq!(old_var_name(&Spanned::no_span(Expr::List(vec![]))), "list");
    assert_eq!(
        old_var_name(&Spanned::no_span(Expr::Tuple(vec![]))),
        "tuple"
    );
}

#[test]
fn old_var_name_raw_tokens() {
    let e = Spanned::no_span(Expr::Raw(vec!["tok".into()]));
    assert_eq!(old_var_name(&e), "tok");
    let e2 = Spanned::no_span(Expr::Raw(vec![]));
    assert_eq!(old_var_name(&e2), "raw");
}

#[test]
fn old_var_name_block() {
    let e = Spanned::no_span(Expr::Block(vec![Spanned::no_span(Expr::Ident(
        "first".into(),
    ))]));
    assert_eq!(old_var_name(&e), "first");
    let e2 = Spanned::no_span(Expr::Block(vec![]));
    assert_eq!(old_var_name(&e2), "block");
}

// -----------------------------------------------------------------------
// expr.rs unit tests: has_deep_field_access
// -----------------------------------------------------------------------

#[test]
fn deep_field_access_simple_var() {
    assert!(!has_deep_field_access("x"));
}

#[test]
fn deep_field_access_method_chain() {
    assert!(!has_deep_field_access("items.iter().all()"));
}

#[test]
fn deep_field_access_struct_field() {
    assert!(has_deep_field_access("state.head"));
}

#[test]
fn deep_field_access_nested_field() {
    assert!(has_deep_field_access("state.head.extra.max"));
}

#[test]
fn deep_field_access_result_field() {
    assert!(has_deep_field_access(&format!("{RESULT_VAR}.value")));
}

#[test]
fn deep_field_access_result_method_ok() {
    assert!(!has_deep_field_access(&format!("{RESULT_VAR}.len()")));
}

#[test]
fn deep_field_access_mixed_method_and_field() {
    assert!(has_deep_field_access("data.header"));
}

#[test]
fn deep_field_access_no_dots() {
    assert!(!has_deep_field_access("simple_var + 1"));
}

// -----------------------------------------------------------------------
// RustStmt::Assert rendering (replaces generate_debug_assert)
// -----------------------------------------------------------------------

#[test]
fn debug_assert_simple() {
    let mut code = String::new();
    crate::hir::render_stmt(
        &crate::hir::RustStmt::Assert {
            cond: "x > 0".into(),
            label: "requires".into(),
        },
        &mut code,
        1,
    );
    assert!(code.contains("debug_assert!(x > 0"), "got: {code}");
    assert!(code.contains("requires:"), "got: {code}");
}

#[test]
fn debug_assert_multiline() {
    let mut code = String::new();
    crate::hir::render_stmt(
        &crate::hir::RustStmt::Assert {
            cond: "match x {\n  1 => true\n}".into(),
            label: "ensures".into(),
        },
        &mut code,
        1,
    );
    assert!(code.contains("debug_assert!({"), "got: {code}");
}

#[test]
fn debug_assert_deep_field_becomes_comment() {
    let mut code = String::new();
    crate::hir::render_stmt(
        &crate::hir::RustStmt::Assert {
            cond: "state.head.extra > 0".into(),
            label: "invariant".into(),
        },
        &mut code,
        1,
    );
    assert!(
        code.starts_with("    //"),
        "deep field should be comment: {code}"
    );
    assert!(!code.contains("debug_assert!"), "got: {code}");
}

#[test]
fn debug_assert_indented() {
    let mut code = String::new();
    crate::hir::render_stmt(
        &crate::hir::RustStmt::Assert {
            cond: "x > 0".into(),
            label: "requires".into(),
        },
        &mut code,
        2,
    );
    assert!(code.starts_with("        debug_assert!"), "got: {code}");
}

#[test]
fn debug_assert_indented_deep_field_comment() {
    let mut code = String::new();
    crate::hir::render_stmt(
        &crate::hir::RustStmt::Assert {
            cond: "a.b.c > 0".into(),
            label: "inv".into(),
        },
        &mut code,
        3,
    );
    assert!(code.starts_with("            //"), "got: {code}");
}

// -----------------------------------------------------------------------
// expr.rs unit tests: collect_old_exprs
// -----------------------------------------------------------------------

#[test]
fn collect_old_exprs_none() {
    let e = Spanned::no_span(Expr::Ident("x".into()));
    assert!(collect_old_exprs(&e).is_empty());
}

#[test]
fn collect_old_exprs_single() {
    let e = Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(Expr::Ident(
        "x".into(),
    )))));
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].0, "x");
    assert_eq!(result[0].1, "x");
}

#[test]
fn collect_old_exprs_in_binop() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("a".into()),
        ))))),
        op: BinOp::Lt,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].0, "a");
}

#[test]
fn collect_old_exprs_deduplicates() {
    // old(x) + old(x) should produce only one entry
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("x".into()),
        ))))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("x".into()),
        ))))),
    });
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 1);
}

#[test]
fn collect_old_exprs_multiple_different() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("x".into()),
        ))))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("y".into()),
        ))))),
    });
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 2);
}

#[test]
fn collect_old_exprs_in_if() {
    let e = Spanned::no_span(Expr::If {
        cond: Box::new(Spanned::no_span(Expr::Literal(Literal::Bool(true)))),
        then_branch: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("a".into()),
        ))))),
        else_branch: Some(Box::new(Spanned::no_span(Expr::Old(Box::new(
            Spanned::no_span(Expr::Ident("b".into())),
        ))))),
    });
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 2);
}

#[test]
fn collect_old_exprs_in_list() {
    let e = Spanned::no_span(Expr::List(vec![
        Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(Expr::Ident(
            "x".into(),
        ))))),
        Spanned::no_span(Expr::Ident("y".into())),
    ]));
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 1);
    assert_eq!(result[0].0, "x");
}

#[test]
fn collect_old_exprs_in_let() {
    let e = Spanned::no_span(Expr::Let {
        name: "tmp".into(),
        value: Box::new(Spanned::no_span(Expr::Old(Box::new(Spanned::no_span(
            Expr::Ident("v".into()),
        ))))),
        body: Box::new(Spanned::no_span(Expr::Ident("tmp".into()))),
    });
    let result = collect_old_exprs(&e);
    assert_eq!(result.len(), 1);
}

// -----------------------------------------------------------------------
// expr.rs unit tests: raw_tokens_to_rust
// -----------------------------------------------------------------------

#[test]
fn raw_tokens_empty() {
    assert_eq!(raw_tokens_to_rust(&[]), "");
}

#[test]
fn raw_tokens_result_replacement() {
    let tokens: Vec<String> = vec!["result".into(), ">".into(), "0".into()];
    let result = raw_tokens_to_rust(&tokens);
    assert!(result.contains(RESULT_VAR), "got: {result}");
}

#[test]
fn raw_tokens_typestate_annotation() {
    let tokens: Vec<String> = vec!["conn".into(), "@".into(), "Connected".into()];
    let result = raw_tokens_to_rust(&tokens);
    assert!(result.contains("typestate"), "got: {result}");
    assert!(result.contains("true"), "got: {result}");
}

// -----------------------------------------------------------------------
// expr.rs unit tests: match expression codegen
// -----------------------------------------------------------------------

#[test]
fn expr_to_rust_match_with_constructor_patterns() {
    use assura_ast::{MatchArm, Pattern, Spanned};
    let e = Spanned::no_span(Expr::Match {
        scrutinee: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        arms: vec![
            MatchArm {
                pattern: Pattern::Constructor {
                    name: "Some".into(),
                    fields: vec![Pattern::Ident("v".into())],
                },
                body: Spanned::no_span(Expr::Ident("v".into())),
            },
            MatchArm {
                pattern: Pattern::Wildcard,
                body: Spanned::no_span(Expr::Literal(Literal::Int("0".into()))),
            },
        ],
    });
    let result = expr_to_rust(&e);
    assert!(result.contains("match x"), "got: {result}");
    assert!(result.contains("Some(v) => v"), "got: {result}");
    assert!(result.contains("_ => 0"), "got: {result}");
}

#[test]
fn expr_to_rust_match_adds_wildcard_fallback() {
    use assura_ast::{MatchArm, Pattern};
    // Match with only constructor patterns (no wildcard/ident) gets a fallback
    let e = Spanned::no_span(Expr::Match {
        scrutinee: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
        arms: vec![MatchArm {
            pattern: Pattern::Constructor {
                name: "None".into(),
                fields: vec![],
            },
            body: Spanned::no_span(Expr::Literal(Literal::Int("0".into()))),
        }],
    });
    let result = expr_to_rust(&e);
    assert!(
        result.contains("_ => unreachable!"),
        "should add wildcard fallback: {result}"
    );
}

// -----------------------------------------------------------------------
// block.rs unit tests: format_rust
// -----------------------------------------------------------------------

#[test]
fn format_rust_valid_code() {
    let code = "fn main(){let x=1;}";
    let formatted = format_rust(code);
    // prettyplease should format it properly
    assert!(formatted.contains("fn main()"), "got: {formatted}");
    assert!(!formatted.contains("WARNING"), "got: {formatted}");
}

#[test]
fn format_rust_invalid_code_returns_original() {
    let code = "this is not valid rust @@@ ###";
    let formatted = format_rust(code);
    assert!(
        formatted.contains("WARNING"),
        "should contain WARNING comment: {formatted}"
    );
    assert!(
        formatted.contains(code),
        "should preserve original code: {formatted}"
    );
}

// -----------------------------------------------------------------------
// block.rs unit tests: generate_block
// -----------------------------------------------------------------------

#[test]
fn generate_block_feature_compile_time_only() {
    let mut code = String::new();
    let clauses = vec![Clause {
        kind: ClauseKind::Other("priority".into()),
        body: Spanned::no_span(Expr::Literal(Literal::Str("high".into()))),
        effect_variables: vec![],
    }];
    generate_block(&BlockKind::Feature, "safety", &clauses, &mut code);
    assert!(
        code.contains("compile-time feature flag"),
        "feature with only Other clauses should be compile-time: {code}"
    );
}

#[test]
fn generate_block_table_smt_verified() {
    let mut code = String::new();
    generate_block(&BlockKind::Table, "mappings", &[], &mut code);
    assert!(
        code.contains("compile-time verified by SMT"),
        "table should note SMT verification: {code}"
    );
}

#[test]
fn generate_block_generic_with_ensures() {
    let mut code = String::new();
    let clauses = vec![Clause {
        kind: ClauseKind::Ensures,
        body: Spanned::no_span(Expr::Literal(Literal::Bool(true))),
        effect_variables: vec![],
    }];
    generate_block(&BlockKind::Feature, "test_feat", &clauses, &mut code);
    assert!(
        code.contains("pub mod block_test_feat"),
        "should generate module: {code}"
    );
    assert!(
        code.contains("debug_assert!(true)"),
        "should generate assertion: {code}"
    );
}

#[test]
fn generate_block_ordering_clause() {
    let mut code = String::new();
    let clauses = vec![Clause {
        kind: ClauseKind::Ordering,
        body: Spanned::no_span(Expr::Ident("seq_cst".into())),
        effect_variables: vec![],
    }];
    generate_block(&BlockKind::Feature, "atomic_ops", &clauses, &mut code);
    assert!(
        code.contains("Ordering::SeqCst"),
        "should resolve ordering variant: {code}"
    );
}

#[test]
fn generate_block_must_not_clause() {
    let mut code = String::new();
    let clauses = vec![Clause {
        kind: ClauseKind::MustNot,
        body: Spanned::no_span(Expr::Literal(Literal::Bool(false))),
        effect_variables: vec![],
    }];
    generate_block(&BlockKind::Feature, "constraint", &clauses, &mut code);
    assert!(
        code.contains("debug_assert!(!(false))"),
        "must_not should negate: {code}"
    );
}

// -----------------------------------------------------------------------
// decl.rs unit tests: generate_bind (via full pipeline)
// -----------------------------------------------------------------------

#[test]
fn bind_generates_wrapper_function() {
    let project = codegen_ok(
        r#"
bind "std::cmp::max" as max_val {
    input(a: Int, b: Int)
    output(result: Int)
    requires { true }
    ensures { result >= a }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("fn max_val"),
        "should generate bind wrapper: {lib}"
    );
    assert!(
        lib.contains("debug_assert!"),
        "should generate contract assertions: {lib}"
    );
}

#[test]
fn extern_generates_unsafe_when_trusted() {
    let project = codegen_ok(
        r#"
extern fn raw_alloc(size: Nat) -> Bytes
    trust: untrusted
    requires { size > 0 }
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("unsafe fn raw_alloc"),
        "untrusted extern should be unsafe: {lib}"
    );
}

#[test]
fn fn_def_generates_todo_body() {
    let project = codegen_ok(
        r#"
fn compute(x: Int) -> Int
    effects: pure
"#,
    );
    let lib = &project.files[0].1;
    assert!(lib.contains("fn compute"), "should generate fn: {lib}");
    assert!(lib.contains("todo!"), "fn body should have todo!: {lib}");
}

// -----------------------------------------------------------------------
// service.rs unit tests: extract_state_comparison
// -----------------------------------------------------------------------

#[test]
fn extract_state_self_state_eq() {
    let body = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Field(
            Box::new(Spanned::no_span(Expr::Ident("self".into()))),
            "state".into(),
        ))),
        op: BinOp::Eq,
        rhs: Box::new(Spanned::no_span(Expr::Ident("Connected".into()))),
    });
    assert_eq!(
        extract_state_comparison(&body),
        Some("Connected".to_string())
    );
}

#[test]
fn extract_state_non_state_field() {
    // self.name == X is NOT a state comparison
    let body = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Field(
            Box::new(Spanned::no_span(Expr::Ident("self".into()))),
            "name".into(),
        ))),
        op: BinOp::Eq,
        rhs: Box::new(Spanned::no_span(Expr::Ident("X".into()))),
    });
    assert_eq!(extract_state_comparison(&body), None);
}

#[test]
fn extract_state_non_eq_op() {
    let body = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Field(
            Box::new(Spanned::no_span(Expr::Ident("self".into()))),
            "state".into(),
        ))),
        op: BinOp::Neq,
        rhs: Box::new(Spanned::no_span(Expr::Ident("Closed".into()))),
    });
    assert_eq!(extract_state_comparison(&body), None);
}

#[test]
fn extract_state_not_a_binop() {
    let body = Spanned::no_span(Expr::Ident("something".into()));
    assert_eq!(extract_state_comparison(&body), None);
}

// -----------------------------------------------------------------------
// service.rs unit tests: method_pre_state
// -----------------------------------------------------------------------

#[test]
fn method_pre_state_with_state_guard() {
    let clauses = vec![Clause {
        kind: ClauseKind::Requires,
        body: Spanned::no_span(Expr::BinOp {
            lhs: Box::new(Spanned::no_span(Expr::Field(
                Box::new(Spanned::no_span(Expr::Ident("self".into()))),
                "state".into(),
            ))),
            op: BinOp::Eq,
            rhs: Box::new(Spanned::no_span(Expr::Ident("Running".into()))),
        }),
        effect_variables: vec![],
    }];
    assert_eq!(method_pre_state(&clauses), Some("Running".to_string()));
}

#[test]
fn method_pre_state_without_state_guard() {
    let clauses = vec![Clause {
        kind: ClauseKind::Requires,
        body: Spanned::no_span(Expr::BinOp {
            lhs: Box::new(Spanned::no_span(Expr::Ident("x".into()))),
            op: BinOp::Gt,
            rhs: Box::new(Spanned::no_span(Expr::Literal(Literal::Int("0".into())))),
        }),
        effect_variables: vec![],
    }];
    assert_eq!(method_pre_state(&clauses), None);
}

#[test]
fn method_pre_state_empty_clauses() {
    assert_eq!(method_pre_state(&[]), None);
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: map_type_tokens
// -----------------------------------------------------------------------

#[test]
fn map_type_tokens_empty() {
    let tokens: Vec<String> = vec![];
    assert_eq!(map_type_tokens(&tokens), "()");
}

#[test]
fn map_type_tokens_single() {
    let tokens: Vec<String> = vec!["Int".into()];
    assert_eq!(map_type_tokens(&tokens), "i64");
}

#[test]
fn map_type_tokens_generic() {
    let tokens: Vec<String> = vec!["List".into(), "<".into(), "Int".into(), ">".into()];
    let result = map_type_tokens(&tokens);
    assert!(result.contains("Vec"), "got: {result}");
    assert!(result.contains("i64"), "got: {result}");
}

#[test]
fn map_type_tokens_nested_generic() {
    let tokens: Vec<String> = vec![
        "Map".into(),
        "<".into(),
        "String".into(),
        ",".into(),
        "List".into(),
        "<".into(),
        "Int".into(),
        ">".into(),
        ">".into(),
    ];
    let result = map_type_tokens(&tokens);
    assert!(result.contains("BTreeMap"), "got: {result}");
    assert!(result.contains("Vec"), "got: {result}");
    assert!(result.contains("i64"), "got: {result}");
}

#[test]
fn map_type_tokens_strips_taint() {
    // "Int @ taint : high" should stop at @ and produce just i64
    let tokens: Vec<String> = vec![
        "Int".into(),
        "@".into(),
        "taint".into(),
        ":".into(),
        "high".into(),
    ];
    assert_eq!(map_type_tokens(&tokens), "i64");
}

#[test]
fn map_type_tokens_union_error() {
    // "Int | Error" -> "Result<i64, Error>"
    let tokens: Vec<String> = vec!["Int".into(), "|".into(), "Error".into()];
    let result = map_type_tokens(&tokens);
    assert!(result.contains("Result"), "got: {result}");
    assert!(result.contains("i64"), "got: {result}");
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: smart_join_type_tokens
// -----------------------------------------------------------------------

#[test]
fn smart_join_simple() {
    let tokens = vec!["i64"];
    assert_eq!(smart_join_type_tokens(&tokens), "i64");
}

#[test]
fn smart_join_generic_no_extra_spaces() {
    // smart_join removes space AFTER < but not BEFORE <
    let tokens = vec!["Vec", "<", "i64", ">"];
    let result = smart_join_type_tokens(&tokens);
    // No space after < or before >
    assert!(result.contains("<i64>"), "got: {result}");
}

#[test]
fn smart_join_reference() {
    let tokens = vec!["&", "str"];
    assert_eq!(smart_join_type_tokens(&tokens), "&str");
}

#[test]
fn smart_join_mut_ref() {
    let tokens = vec!["&", "mut", "i64"];
    assert_eq!(smart_join_type_tokens(&tokens), "&mut i64");
}

#[test]
fn smart_join_tuple() {
    let tokens = vec!["(", "i64", ",", "bool", ")"];
    assert_eq!(smart_join_type_tokens(&tokens), "(i64, bool)");
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: is_const_name, is_user_type_name
// -----------------------------------------------------------------------

#[test]
fn is_const_name_screaming_snake() {
    assert!(is_const_name("MAX_SIZE"));
    assert!(is_const_name("TOTAL_TABLE_SIZE"));
}

#[test]
fn is_const_name_not_const() {
    assert!(!is_const_name("Int"));
    assert!(!is_const_name("maxSize"));
    assert!(!is_const_name(""));
    assert!(!is_const_name("NOUNDERSCORES"));
}

#[test]
fn is_user_type_name_custom() {
    assert!(is_user_type_name("Point"));
    assert!(is_user_type_name("HuffmanTable"));
}

#[test]
fn is_user_type_name_builtins_excluded() {
    assert!(!is_user_type_name("Int"));
    assert!(!is_user_type_name("Bool"));
    assert!(!is_user_type_name("List"));
    assert!(!is_user_type_name("Option"));
    assert!(!is_user_type_name("Result"));
}

#[test]
fn is_user_type_name_lowercase_excluded() {
    assert!(!is_user_type_name("lowercase"));
    assert!(!is_user_type_name(""));
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: extract_base_type_from_refined
// -----------------------------------------------------------------------

#[test]
fn extract_base_type_standard() {
    let tokens: Vec<String> = vec![
        "n".into(),
        ":".into(),
        "Int".into(),
        "|".into(),
        "n".into(),
        ">".into(),
        "0".into(),
    ];
    assert_eq!(extract_base_type_from_refined(&tokens), "i64");
}

#[test]
fn extract_base_type_nat() {
    let tokens: Vec<String> = vec![
        "x".into(),
        ":".into(),
        "Nat".into(),
        "|".into(),
        "x".into(),
        "<".into(),
        "256".into(),
    ];
    assert_eq!(extract_base_type_from_refined(&tokens), "u64");
}

#[test]
fn extract_base_type_fallback() {
    let tokens: Vec<String> = vec!["something".into()];
    assert_eq!(extract_base_type_from_refined(&tokens), "i64");
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: expr_to_rust_static
// -----------------------------------------------------------------------

#[test]
fn expr_to_rust_static_literal() {
    let e = Spanned::no_span(Expr::Literal(Literal::Int("100".into())));
    assert_eq!(expr_to_rust_static(&e), "100");
}

#[test]
fn expr_to_rust_static_binop() {
    let e = Spanned::no_span(Expr::BinOp {
        lhs: Box::new(Spanned::no_span(Expr::Ident("a".into()))),
        op: BinOp::Add,
        rhs: Box::new(Spanned::no_span(Expr::Ident("b".into()))),
    });
    assert_eq!(expr_to_rust_static(&e), "(a + b)");
}

// -----------------------------------------------------------------------
// types_gen.rs unit tests: generate_cargo_toml_impl
// -----------------------------------------------------------------------

#[test]
fn cargo_toml_default_config() {
    let config = BackendConfig::default();
    let toml = generate_cargo_toml_impl("my_crate", &config, false, false);
    assert!(toml.contains("name = \"my_crate\""), "got: {toml}");
    assert!(toml.contains("edition = \"2024\""), "got: {toml}");
    // Default config: opt_level=2, debug_info=false => no [profile.release]
    assert!(!toml.contains("[profile.release]"), "got: {toml}");
}

#[test]
fn cargo_toml_with_proptest() {
    let config = BackendConfig::default();
    let toml = generate_cargo_toml_impl("test_crate", &config, true, false);
    assert!(toml.contains("proptest"), "got: {toml}");
    assert!(toml.contains("[dev-dependencies]"), "got: {toml}");
}

#[test]
fn cargo_toml_with_thiserror() {
    let config = BackendConfig::default();
    let toml = generate_cargo_toml_impl("err_crate", &config, false, true);
    assert!(toml.contains("thiserror"), "got: {toml}");
}

#[test]
fn cargo_toml_cranelift_backend() {
    let config = BackendConfig {
        backend: CodegenBackend::Cranelift,
        ..Default::default()
    };
    let toml = generate_cargo_toml_impl("fast_crate", &config, false, false);
    assert!(toml.contains("Cranelift"), "got: {toml}");
}

#[test]
fn cargo_toml_wasm_target() {
    let config = BackendConfig {
        target: CompileTarget::Wasm,
        ..Default::default()
    };
    let toml = generate_cargo_toml_impl("wasm_crate", &config, false, false);
    assert!(toml.contains("cdylib"), "got: {toml}");
    assert!(toml.contains("wasm32-wasip1"), "got: {toml}");
}

#[test]
fn cargo_toml_custom_opt_level() {
    let config = BackendConfig {
        opt_level: 3,
        debug_info: true,
        ..Default::default()
    };
    let toml = generate_cargo_toml_impl("opt_crate", &config, false, false);
    assert!(toml.contains("opt-level = 3"), "got: {toml}");
    assert!(toml.contains("debug = true"), "got: {toml}");
}

// -----------------------------------------------------------------------
// features.rs unit tests: selected feature generators
// -----------------------------------------------------------------------

#[test]
fn feature_ghost_erasure_compile_time() {
    let code = crate::features::compile_time_ghost_erasure("test_fn");
    assert!(
        code.contains("ghost"),
        "ghost erasure should mention ghost: {code}"
    );
}

#[test]
fn feature_constant_time_annotation() {
    let code = crate::features::generate_constant_time_annotation("crypto_op");
    assert!(
        code.contains("constant_time"),
        "should mention constant_time: {code}"
    );
}

#[test]
fn feature_callback_reentrancy_guard() {
    let code = crate::features::generate_callback_reentrancy_guard("on_event");
    assert!(
        code.contains("__REENTRANT_ON_EVENT"),
        "should generate reentrancy guard: {code}"
    );
    assert!(
        code.contains("reentrant call"),
        "should contain reentrant check: {code}"
    );
}

#[test]
fn feature_opaque_function() {
    let code = crate::features::generate_opaque_function("internal");
    assert!(code.contains("opaque"), "should mark as opaque: {code}");
}

#[test]
fn feature_deterministic_annotation() {
    let code = crate::features::generate_deterministic_annotation("pure_fn");
    assert!(
        code.contains("deterministic"),
        "should mention deterministic: {code}"
    );
}

// -----------------------------------------------------------------------
// service.rs: full pipeline tests for service codegen
// -----------------------------------------------------------------------

#[test]
fn service_stateless_generates_impl() {
    let project = codegen_ok(
        r#"
service Calculator {
    operation add {
        requires { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("mod calculator"),
        "should generate service module: {lib}"
    );
    assert!(lib.contains("pub fn new()"), "should generate new(): {lib}");
}

#[test]
fn service_with_query_generates_immutable_method() {
    let project = codegen_ok(
        r#"
service DataStore {
    query count {
        requires { true }
    }
}
"#,
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("fn count"),
        "should generate query method: {lib}"
    );
}

#[test]
fn runtime_checks_via_codegen_with_config() {
    let source = "contract SafeDiv {\n  requires(a: Int, b: Int)\n  requires { b != 0 }\n  ensures(result: Int)\n  ensures { true }\n}";
    let project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            runtime_checks: true,
            ..Default::default()
        },
    );
    let lib = &project.files[0].1;
    assert!(
        lib.contains("contract_violation"),
        "runtime_checks=true should produce contract_violation: {lib}"
    );
    assert!(
        !lib.contains("debug_assert!"),
        "runtime_checks=true should NOT use debug_assert!: {lib}"
    );
}

#[test]
fn multi_file_ir_bodies_propagate_to_per_contract_files() {
    let source = "\
contract Alpha {\n  requires(x: Int)\n  requires { x > 0 }\n  ensures(result: Int)\n  ensures { true }\n}
contract Beta {\n  requires(y: Int)\n  requires { y >= 0 }\n  ensures(result: Int)\n  ensures { true }\n}";
    let mut ir_bodies = std::collections::HashMap::new();
    ir_bodies.insert("Alpha".to_string(), "x + 1".to_string());
    ir_bodies.insert("Beta".to_string(), "y * 2".to_string());
    let project = codegen_with_config_ok(
        source,
        super::BackendConfig {
            ir_bodies,
            ..Default::default()
        },
    );
    // Multi-file mode: lib.rs + contract_alpha.rs + contract_beta.rs
    assert!(
        project.files.len() >= 3,
        "should produce multi-file output: got {} files",
        project.files.len()
    );
    let alpha_file = project
        .files
        .iter()
        .find(|(name, _)| name.contains("alpha"))
        .expect("should have alpha contract file");
    assert!(
        alpha_file.1.contains("x + 1"),
        "Alpha's IR body should be injected: {}",
        alpha_file.1
    );
    let beta_file = project
        .files
        .iter()
        .find(|(name, _)| name.contains("beta"))
        .expect("should have beta contract file");
    assert!(
        beta_file.1.contains("y * 2"),
        "Beta's IR body should be injected: {}",
        beta_file.1
    );
}