assura 0.2.0

use super::*;

// `assura audit [path]` -- scan and verify a Rust project
// ---------------------------------------------------------------------------

/// Configuration for the `assura audit` command.
pub(crate) struct AuditOptions<'a> {
    pub(crate) path: &'a str,
    pub(crate) depth: &'a str,
    pub(crate) format: &'a str,
    pub(crate) focus: Option<&'a str>,
    pub(crate) max_functions: Option<usize>,
    pub(crate) timeout_ms: u64,
    pub(crate) unsafe_only: bool,
}

pub(crate) fn run_audit(opts: AuditOptions<'_>) {
    let AuditOptions {
        path,
        depth,
        format,
        focus,
        max_functions,
        timeout_ms: _timeout_ms,
        unsafe_only,
    } = opts;
    // Phase 1: Discover Rust source files
    let root = Path::new(path);
    let cargo_toml = root.join("Cargo.toml");
    if !cargo_toml.exists() {
        eprintln!("Error: no Cargo.toml found at {}", root.display());
        eprintln!("Run `assura audit` from a Cargo workspace root.");
        process::exit(2);
    }

    // Discover src directories: support workspaces and single crates
    let src_dirs = discover_workspace_src_dirs(root);
    if src_dirs.is_empty() {
        eprintln!("Error: no src/ directories found at {}", root.display());
        process::exit(2);
    }

    let mut rs_files = Vec::new();
    for src_dir in &src_dirs {
        rs_files.extend(discover_rs_files(src_dir));
    }
    rs_files.sort();
    rs_files.dedup();

    if rs_files.is_empty() {
        eprintln!("No .rs files found in scanned directories");
        process::exit(1);
    }

    // Phase 2: Extract all function signatures
    let mut all_sigs: Vec<(String, RustFnSig)> = Vec::new();
    for rs_file in &rs_files {
        let rel_path = rs_file
            .strip_prefix(root)
            .unwrap_or(rs_file.as_path())
            .to_string_lossy()
            .to_string();

        let source = match fs::read_to_string(rs_file) {
            Ok(s) => s,
            Err(_) => continue,
        };

        let sigs = extract_rust_fn_signatures(&source);
        for sig in sigs {
            if !sig.is_pub {
                continue;
            }
            if unsafe_only && !source.contains("unsafe") {
                continue;
            }
            if let Some(pattern) = focus {
                let qname = format!("{}::{}", rel_path, sig.name);
                if !qname.contains(pattern) && !sig.name.contains(pattern) {
                    continue;
                }
            }
            all_sigs.push((rel_path.clone(), sig));
        }
    }

    if let Some(max) = max_functions {
        all_sigs.truncate(max);
    }

    if all_sigs.is_empty() {
        eprintln!("No matching public functions found.");
        process::exit(1);
    }

    let is_json = format == "json";

    if !is_json {
        eprintln!(
            "Scanning {} ... found {} public functions in {} files",
            root.display(),
            all_sigs.len(),
            rs_files.len()
        );
    }

    // Phase 3: Generate skeleton contracts (using lenient type mapping)
    use assura_codegen::type_map::rust_type_to_assura_lenient;

    let mut assura_source = String::new();
    assura_source.push_str("// Auto-generated by: assura audit\n");
    assura_source.push_str("// Review and refine before relying on results.\n\n");

    let mut skipped_all_unknown = 0u32;

    for (file_path, sig) in &all_sigs {
        let module_path = derive_rust_module_path(file_path);
        let rust_path = format!("{module_path}::{}", sig.name);

        // Map params and return type using lenient mapper
        let mapped_params: Vec<(String, String)> = sig
            .params
            .iter()
            .map(|(name, ty)| (name.clone(), rust_type_to_assura_lenient(ty)))
            .collect();
        let mapped_ret = rust_type_to_assura_lenient(&sig.return_type);

        // Skip functions where ALL params + return are Unknown (nothing to verify)
        let all_unknown = mapped_params.iter().all(|(_, ty)| ty == "Unknown")
            && (mapped_ret == "Unknown" || mapped_ret == "Unit");
        if all_unknown && !mapped_params.is_empty() {
            skipped_all_unknown += 1;
            continue;
        }

        assura_source.push_str(&format!("bind \"{}\" as {} {{\n", rust_path, sig.name));

        if !mapped_params.is_empty() {
            assura_source.push_str("    input(");
            let params: Vec<String> = mapped_params
                .iter()
                .map(|(name, ty)| format!("{name}: {ty}"))
                .collect();
            assura_source.push_str(&params.join(", "));
            assura_source.push_str(")\n");
        }

        if mapped_ret != "Unit" && mapped_ret != "Unknown" {
            assura_source.push_str(&format!("    output(result: {mapped_ret})\n"));
        }

        // Generate clauses based on depth and parameter types
        let mut has_clause = false;

        for (name, aty) in &mapped_params {
            if aty == "Unknown" {
                continue;
            }
            // Index parameters: non-negative bound
            if (aty == "Nat" || aty == "Int")
                && (name.contains("index")
                    || name.contains("offset")
                    || name.contains("idx")
                    || name.contains("pos")
                    || name.contains("len")
                    || name.contains("size")
                    || name.contains("count")
                    || name.contains("capacity"))
            {
                assura_source.push_str(&format!("    requires {{ {name} >= 0 }}\n"));
                has_clause = true;
            }
            // Slice/list/string parameters: non-empty check (medium+)
            if (depth == "medium" || depth == "deep")
                && (aty.starts_with("List") || aty == "Bytes" || aty == "String")
            {
                assura_source.push_str(&format!("    requires {{ length({name}) > 0 }}\n"));
                has_clause = true;
            }
        }

        // For Nat return types, add non-negative ensures
        if mapped_ret == "Nat" {
            assura_source.push_str("    ensures { result >= 0 }\n");
            has_clause = true;
        }

        // If no clauses yet, add a trivial ensures so SMT has something to check
        if !has_clause {
            assura_source.push_str("    ensures { true }\n");
        }

        assura_source.push_str("}\n\n");
    }

    if skipped_all_unknown > 0 && !is_json {
        eprintln!(
            "Skipped {} functions with all-unknown signatures",
            skipped_all_unknown
        );
    }

    // Phase 4: Verify each bind declaration individually
    //
    // We compile each bind separately so that a function with unknown types
    // does not prevent verification of functions with clean types. This is
    // the key design choice: one bad signature does not kill the whole audit.
    let bind_blocks: Vec<&str> = assura_source.split("\nbind ").skip(1).collect();

    let contract_count = bind_blocks.len();
    if !is_json {
        eprintln!(
            "Generating contracts ... {} skeleton contracts",
            contract_count
        );
        eprintln!("Verifying ...");
    }

    let mut findings: Vec<AuditFinding> = Vec::new();
    let mut verified_count = 0u32;
    let mut error_count = 0u32;
    let mut skipped_errors = 0u32;

    let config = CompilerConfig::default();

    for block in &bind_blocks {
        let single_source = format!("bind {block}");

        let output = assura_pipeline::compile_full(&single_source, "audit.assura", &config);

        if output.has_errors {
            // This bind had resolution/type errors; skip it silently
            skipped_errors += 1;
            continue;
        }

        for r in &output.verification {
            match r {
                assura_smt::VerificationResult::Verified { .. } => {
                    verified_count += 1;
                }
                assura_smt::VerificationResult::Counterexample { model, .. } => {
                    findings.push(AuditFinding {
                        function: r.clause_desc().to_string(),
                        clause: "counterexample".to_string(),
                        severity: "warning".to_string(),
                        message: "Counterexample found".to_string(),
                        counterexample: Some(model.clone()),
                    });
                }
                assura_smt::VerificationResult::Timeout { .. } => {
                    findings.push(AuditFinding {
                        function: r.clause_desc().to_string(),
                        clause: "timeout".to_string(),
                        severity: "info".to_string(),
                        message: "Solver timed out".to_string(),
                        counterexample: None,
                    });
                }
                assura_smt::VerificationResult::Unknown { reason, .. } => {
                    findings.push(AuditFinding {
                        function: r.clause_desc().to_string(),
                        clause: "unknown".to_string(),
                        severity: "info".to_string(),
                        message: format!("Solver result unknown: {reason}"),
                        counterexample: None,
                    });
                }
            }
        }
    }

    if skipped_errors > 0 && !is_json {
        error_count = skipped_errors;
        eprintln!("Skipped {} contracts with type errors", skipped_errors);
    }

    // Phase 5: Output results
    if is_json {
        let report = serde_json::json!({
            "functions_scanned": all_sigs.len(),
            "files_scanned": rs_files.len(),
            "verified": verified_count,
            "findings": findings.len(),
            "errors": error_count,
            "results": findings.iter().map(|f| serde_json::json!({
                "function": f.function,
                "clause": f.clause,
                "severity": f.severity,
                "message": f.message,
                "counterexample": f.counterexample,
            })).collect::<Vec<_>>(),
        });
        println!("{}", serde_json::to_string_pretty(&report).unwrap());
    } else {
        println!();
        println!(
            "AUDIT SUMMARY: {} functions, {} verified, {} findings, {} errors",
            all_sigs.len(),
            verified_count,
            findings.len(),
            error_count
        );

        if !findings.is_empty() {
            println!();
            println!("FINDINGS:");
            for f in &findings {
                let sev = match f.severity.as_str() {
                    "warning" => "WARNING",
                    "error" => "ERROR",
                    _ => "INFO",
                };
                println!("  [{sev}] {}  ({})", f.function, f.clause);
                println!("    {}", f.message);
                if let Some(cex) = &f.counterexample {
                    for line in cex.lines() {
                        println!("    | {line}");
                    }
                }
                println!();
            }
        }

        if findings.is_empty() && error_count == 0 {
            println!("  All verified contracts passed.");
        }
    }

    if !findings.is_empty() {
        process::exit(1);
    }
}

/// A finding from the audit.
pub(crate) struct AuditFinding {
    function: String,
    clause: String,
    severity: String,
    message: String,
    counterexample: Option<String>,
}

/// Recursively discover all .rs files under a directory.
/// Discover src/ directories from a Cargo project root.
///
/// If `Cargo.toml` has a `[workspace]` section with `members`, scan each
/// member's `src/` directory. Supports glob patterns like `crates/*`.
/// If it's a single-crate project, return `root/src/` if it exists.
pub(crate) fn discover_workspace_src_dirs(root: &Path) -> Vec<std::path::PathBuf> {
    let cargo_toml = root.join("Cargo.toml");
    let content = match fs::read_to_string(&cargo_toml) {
        Ok(c) => c,
        Err(_) => return Vec::new(),
    };

    let mut src_dirs = Vec::new();

    // Check for workspace members
    let mut in_workspace = false;
    let mut in_members = false;
    for line in content.lines() {
        let trimmed = line.trim();
        if trimmed == "[workspace]" {
            in_workspace = true;
            continue;
        }
        if trimmed.starts_with('[') && trimmed != "[workspace]" {
            if in_workspace {
                in_workspace = false;
                in_members = false;
            }
            continue;
        }
        if in_workspace {
            if trimmed.starts_with("members") && trimmed.contains('[') {
                in_members = true;
            }
            if in_members {
                // Extract member paths from members = ["crates/*", "tools/*"]
                for segment in trimmed.split('"') {
                    let seg = segment.trim().trim_matches(',').trim();
                    if seg.is_empty()
                        || seg.starts_with('[')
                        || seg.starts_with(']')
                        || seg.contains('=')
                        || seg == "members"
                    {
                        continue;
                    }
                    // Expand glob patterns like crates/*
                    if seg.contains('*') {
                        let prefix = seg.trim_end_matches("/*").trim_end_matches("\\*");
                        let pattern_dir = root.join(prefix);
                        if let Ok(entries) = fs::read_dir(&pattern_dir) {
                            for entry in entries.flatten() {
                                let member_src = entry.path().join("src");
                                if member_src.is_dir() {
                                    src_dirs.push(member_src);
                                }
                            }
                        }
                    } else {
                        let member_src = root.join(seg).join("src");
                        if member_src.is_dir() {
                            src_dirs.push(member_src);
                        }
                    }
                }
                if trimmed.contains(']') {
                    in_members = false;
                }
            }
        }
    }

    // Fallback: single-crate project with src/
    if src_dirs.is_empty() {
        let src_dir = root.join("src");
        if src_dir.is_dir() {
            src_dirs.push(src_dir);
        }
    }

    src_dirs.sort();
    src_dirs
}

pub(crate) fn discover_rs_files(dir: &Path) -> Vec<std::path::PathBuf> {
    let mut files = Vec::new();
    if let Ok(entries) = fs::read_dir(dir) {
        for entry in entries.flatten() {
            let path = entry.path();
            if path.is_dir() {
                files.extend(discover_rs_files(&path));
            } else if path.extension().is_some_and(|ext| ext == "rs") {
                files.push(path);
            }
        }
    }
    files.sort();
    files
}

// ---------------------------------------------------------------------------

#[cfg(test)]
mod tests {
    use super::*;
    use tempfile::TempDir;

    // ---- discover_rs_files ----

    #[test]
    fn discover_rs_files_empty_dir() {
        let tmp = TempDir::new().unwrap();
        let files = discover_rs_files(tmp.path());
        assert!(files.is_empty());
    }

    #[test]
    fn discover_rs_files_finds_rs_only() {
        let tmp = TempDir::new().unwrap();
        fs::write(tmp.path().join("main.rs"), "fn main() {}").unwrap();
        fs::write(tmp.path().join("readme.md"), "# readme").unwrap();
        fs::write(tmp.path().join("data.json"), "{}").unwrap();

        let files = discover_rs_files(tmp.path());
        assert_eq!(files.len(), 1);
        assert!(files[0].file_name().unwrap() == "main.rs");
    }

    #[test]
    fn discover_rs_files_recursive() {
        let tmp = TempDir::new().unwrap();
        fs::write(tmp.path().join("lib.rs"), "").unwrap();
        let sub = tmp.path().join("util");
        fs::create_dir(&sub).unwrap();
        fs::write(sub.join("helpers.rs"), "").unwrap();
        let deep = sub.join("inner");
        fs::create_dir(&deep).unwrap();
        fs::write(deep.join("deep.rs"), "").unwrap();

        let files = discover_rs_files(tmp.path());
        assert_eq!(files.len(), 3);
        let names: Vec<_> = files
            .iter()
            .map(|f| f.file_name().unwrap().to_str().unwrap().to_string())
            .collect();
        assert!(names.contains(&"lib.rs".to_string()));
        assert!(names.contains(&"helpers.rs".to_string()));
        assert!(names.contains(&"deep.rs".to_string()));
    }

    #[test]
    fn discover_rs_files_sorted() {
        let tmp = TempDir::new().unwrap();
        fs::write(tmp.path().join("z.rs"), "").unwrap();
        fs::write(tmp.path().join("a.rs"), "").unwrap();
        fs::write(tmp.path().join("m.rs"), "").unwrap();

        let files = discover_rs_files(tmp.path());
        assert_eq!(files.len(), 3);
        let names: Vec<_> = files
            .iter()
            .map(|f| f.file_name().unwrap().to_str().unwrap().to_string())
            .collect();
        assert_eq!(names, vec!["a.rs", "m.rs", "z.rs"]);
    }

    #[test]
    fn discover_rs_files_nonexistent_dir() {
        let files = discover_rs_files(Path::new("/nonexistent/path/that/does/not/exist"));
        assert!(files.is_empty());
    }

    // ---- discover_workspace_src_dirs ----

    #[test]
    fn workspace_src_dirs_no_cargo_toml() {
        let tmp = TempDir::new().unwrap();
        let dirs = discover_workspace_src_dirs(tmp.path());
        assert!(dirs.is_empty());
    }

    #[test]
    fn workspace_src_dirs_single_crate() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[package]\nname = \"my-crate\"\nversion = \"0.1.0\"\n",
        )
        .unwrap();
        let src = tmp.path().join("src");
        fs::create_dir(&src).unwrap();
        fs::write(src.join("lib.rs"), "").unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 1);
        assert_eq!(dirs[0], src);
    }

    #[test]
    fn workspace_src_dirs_single_crate_no_src() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[package]\nname = \"my-crate\"\n",
        )
        .unwrap();
        let dirs = discover_workspace_src_dirs(tmp.path());
        assert!(dirs.is_empty());
    }

    #[test]
    fn workspace_src_dirs_workspace_with_explicit_members() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\"crate-a\", \"crate-b\"]\n",
        )
        .unwrap();

        let a_src = tmp.path().join("crate-a").join("src");
        fs::create_dir_all(&a_src).unwrap();
        fs::write(a_src.join("lib.rs"), "").unwrap();

        let b_src = tmp.path().join("crate-b").join("src");
        fs::create_dir_all(&b_src).unwrap();
        fs::write(b_src.join("lib.rs"), "").unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 2);
        assert!(dirs.contains(&a_src));
        assert!(dirs.contains(&b_src));
    }

    #[test]
    fn workspace_src_dirs_workspace_with_glob() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\"crates/*\"]\n",
        )
        .unwrap();

        let crates_dir = tmp.path().join("crates");
        fs::create_dir(&crates_dir).unwrap();

        let alpha_src = crates_dir.join("alpha").join("src");
        fs::create_dir_all(&alpha_src).unwrap();
        fs::write(alpha_src.join("lib.rs"), "").unwrap();

        let beta_src = crates_dir.join("beta").join("src");
        fs::create_dir_all(&beta_src).unwrap();
        fs::write(beta_src.join("lib.rs"), "").unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 2);
        assert!(dirs.contains(&alpha_src));
        assert!(dirs.contains(&beta_src));
    }

    #[test]
    fn workspace_src_dirs_workspace_skips_member_without_src() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\"has-src\", \"no-src\"]\n",
        )
        .unwrap();

        let has_src = tmp.path().join("has-src").join("src");
        fs::create_dir_all(&has_src).unwrap();
        fs::write(has_src.join("lib.rs"), "").unwrap();

        fs::create_dir_all(tmp.path().join("no-src")).unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 1);
        assert_eq!(dirs[0], has_src);
    }

    #[test]
    fn workspace_src_dirs_multiline_members() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\n    \"lib-a\",\n    \"lib-b\",\n]\n",
        )
        .unwrap();

        let a_src = tmp.path().join("lib-a").join("src");
        fs::create_dir_all(&a_src).unwrap();
        fs::write(a_src.join("lib.rs"), "").unwrap();

        let b_src = tmp.path().join("lib-b").join("src");
        fs::create_dir_all(&b_src).unwrap();
        fs::write(b_src.join("lib.rs"), "").unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 2);
        assert!(dirs.contains(&a_src));
        assert!(dirs.contains(&b_src));
    }

    #[test]
    fn workspace_src_dirs_result_is_sorted() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\"zzz\", \"aaa\"]\n",
        )
        .unwrap();

        let z_src = tmp.path().join("zzz").join("src");
        fs::create_dir_all(&z_src).unwrap();
        let a_src = tmp.path().join("aaa").join("src");
        fs::create_dir_all(&a_src).unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 2);
        assert!(dirs[0] < dirs[1]);
    }

    #[test]
    fn workspace_src_dirs_other_section_after_workspace() {
        let tmp = TempDir::new().unwrap();
        fs::write(
            tmp.path().join("Cargo.toml"),
            "[workspace]\nmembers = [\"core\"]\n\n[dependencies]\nserde = \"1\"\n",
        )
        .unwrap();

        let core_src = tmp.path().join("core").join("src");
        fs::create_dir_all(&core_src).unwrap();

        let dirs = discover_workspace_src_dirs(tmp.path());
        assert_eq!(dirs.len(), 1);
        assert_eq!(dirs[0], core_src);
    }

    // ---- AuditFinding ----

    #[test]
    fn audit_finding_with_counterexample() {
        let finding = AuditFinding {
            function: "my_crate::process".to_string(),
            clause: "counterexample".to_string(),
            severity: "warning".to_string(),
            message: "Counterexample found".to_string(),
            counterexample: Some("x = 0, y = -1".to_string()),
        };
        assert_eq!(finding.function, "my_crate::process");
        assert_eq!(finding.clause, "counterexample");
        assert_eq!(finding.severity, "warning");
        assert_eq!(finding.counterexample.as_deref(), Some("x = 0, y = -1"));
    }

    #[test]
    fn audit_finding_without_counterexample() {
        let finding = AuditFinding {
            function: "module::timeout_fn".to_string(),
            clause: "timeout".to_string(),
            severity: "info".to_string(),
            message: "Solver timed out".to_string(),
            counterexample: None,
        };
        assert!(finding.counterexample.is_none());
        assert_eq!(finding.severity, "info");
    }

    // ---- AuditOptions ----

    #[test]
    fn audit_options_all_fields() {
        let opts = AuditOptions {
            path: "/tmp/project",
            depth: "medium",
            format: "json",
            focus: Some("my_fn"),
            max_functions: Some(10),
            timeout_ms: 5000,
            unsafe_only: true,
        };
        assert_eq!(opts.path, "/tmp/project");
        assert_eq!(opts.depth, "medium");
        assert_eq!(opts.format, "json");
        assert_eq!(opts.focus, Some("my_fn"));
        assert_eq!(opts.max_functions, Some(10));
        assert_eq!(opts.timeout_ms, 5000);
        assert!(opts.unsafe_only);
    }

    #[test]
    fn audit_options_minimal() {
        let opts = AuditOptions {
            path: ".",
            depth: "shallow",
            format: "human",
            focus: None,
            max_functions: None,
            timeout_ms: 30000,
            unsafe_only: false,
        };
        assert_eq!(opts.path, ".");
        assert!(opts.focus.is_none());
        assert!(opts.max_functions.is_none());
        assert!(!opts.unsafe_only);
    }

    // ---- Generated contract quality ----

    #[test]
    fn generated_bind_with_primitives_compiles_and_verifies() {
        // Simulate the audit flow: generate a bind from Rust signature,
        // compile it, and verify it produces results (not 0 verified).
        use assura_codegen::type_map::rust_type_to_assura_lenient;

        let params = vec![
            ("x".to_string(), "i64".to_string()),
            ("y".to_string(), "u32".to_string()),
        ];
        let ret = "bool";

        let mapped_params: Vec<String> = params
            .iter()
            .map(|(name, ty)| format!("{}: {}", name, rust_type_to_assura_lenient(ty)))
            .collect();
        let mapped_ret = rust_type_to_assura_lenient(ret);

        let source = format!(
            "bind \"test::my_fn\" as my_fn {{\n    input({})\n    output(result: {})\n    ensures {{ true }}\n}}\n",
            mapped_params.join(", "),
            mapped_ret
        );

        let output = assura_pipeline::compile_full(
            &source,
            "audit_test.assura",
            &assura_config::CompilerConfig::default(),
        );

        // Must not have errors
        assert!(
            !output.has_errors,
            "Generated bind should compile without errors. Diagnostics: {:?}",
            output
                .diagnostics
                .iter()
                .map(|d| &d.message)
                .collect::<Vec<_>>()
        );
        // Must have at least one verification result
        assert!(
            !output.verification.is_empty(),
            "Expected at least one verification result"
        );
    }

    #[test]
    fn generated_bind_with_unknown_types_skipped_cleanly() {
        use assura_codegen::type_map::rust_type_to_assura_lenient;

        // A function with all-unknown params should be skipped
        let params = vec![
            ("config".to_string(), "Config".to_string()),
            ("handler".to_string(), "Arc<Handler>".to_string()),
        ];

        let all_unknown = params
            .iter()
            .all(|(_, ty)| rust_type_to_assura_lenient(ty) == "Unknown");

        assert!(
            all_unknown,
            "Both Config and Arc<Handler> should map to Unknown"
        );
    }

    #[test]
    fn lenient_mapper_preserves_verifiable_params() {
        use assura_codegen::type_map::rust_type_to_assura_lenient;

        // Mixed params: some known, some unknown
        let params = vec![
            ("count".to_string(), "usize".to_string()),
            ("name".to_string(), "String".to_string()),
            ("config".to_string(), "Config".to_string()),
        ];

        let mapped: Vec<String> = params
            .iter()
            .map(|(_, ty)| rust_type_to_assura_lenient(ty))
            .collect();

        assert_eq!(mapped, vec!["Nat", "String", "Unknown"]);

        // Not all unknown, so this function should NOT be skipped
        let all_unknown = mapped.iter().all(|ty| ty == "Unknown");
        assert!(!all_unknown);
    }
}