brrr-lint 0.1.0

//! FST014: Test generator for F* code.
//!
//! Analyzes F* code and suggests test cases based on:
//! - Type signatures (generate valid inputs)
//! - Refinement types (boundary values)
//! - Collection types (edge cases)
//! - Integer bounds (min/max values)
//!
//! This rule produces informational suggestions to help developers write
//! comprehensive tests for their F* functions by identifying test-worthy
//! patterns in signatures.
//!
//! The rule is careful to avoid false positives by skipping:
//! - Specification modules (Spec.* or *.Spec.*) which are pure math, not runtime code
//! - Lemma declarations (they ARE the proofs/tests in F*)
//! - Ghost/erased functions (not extractable to runtime code)
//! - Functions with names containing "lemma" (proof helpers)

use lazy_static::lazy_static;
use regex::Regex;
use std::path::PathBuf;

use super::parser::{parse_fstar_file, BlockType};
use super::rules::{Diagnostic, DiagnosticSeverity, Range, Rule, RuleCode};

lazy_static! {
    /// Function signature with parameters: val name : params -> return_type
    static ref FUNC_SIGNATURE: Regex = Regex::new(
        r"val\s+(\w+)\s*:(.+)->"
    ).unwrap();

    /// Refinement type pattern: name:base{constraint}
    /// Examples: x:nat{x > 0}, n:int{n >= 0 /\ n < 100}
    static ref REFINEMENT: Regex = Regex::new(
        r"(\w+)\s*:\s*(\w+)\s*\{([^}]+)\}"
    ).unwrap();

    /// Simple refinement without parameter name: base{constraint}
    static ref SIMPLE_REFINEMENT: Regex = Regex::new(
        r"\b(\w+)\s*\{([^}]+)\}"
    ).unwrap();

    /// List parameter type
    static ref LIST_PARAM: Regex = Regex::new(r"\blist\s+\w+").unwrap();

    /// Sequence parameter types (Seq.seq, seq)
    static ref SEQ_PARAM: Regex = Regex::new(r"\b[Ss]eq\.seq\s+\w+|\bseq\s+\w+").unwrap();

    /// Option type
    static ref OPTION_PARAM: Regex = Regex::new(r"\boption\s+\w+").unwrap();

    /// UInt32 type patterns
    static ref UINT32: Regex = Regex::new(r"\b(?:U32\.t|UInt32\.t|uint32)\b").unwrap();

    /// UInt64 type patterns
    static ref UINT64: Regex = Regex::new(r"\b(?:U64\.t|UInt64\.t|uint64)\b").unwrap();

    /// UInt8 type patterns (byte)
    static ref UINT8: Regex = Regex::new(r"\b(?:U8\.t|UInt8\.t|uint8|byte)\b").unwrap();

    /// UInt16 type patterns
    static ref UINT16: Regex = Regex::new(r"\b(?:U16\.t|UInt16\.t|uint16)\b").unwrap();

    /// Signed Int32 type patterns
    static ref INT32: Regex = Regex::new(r"\b(?:I32\.t|Int32\.t|int32)\b").unwrap();

    /// Natural number type
    static ref NAT: Regex = Regex::new(r"\bnat\b").unwrap();

    /// Positive integer type
    static ref POS: Regex = Regex::new(r"\bpos\b").unwrap();

    /// General int type
    static ref INT_TYPE: Regex = Regex::new(r"\bint\b").unwrap();

    /// String type
    static ref STRING_TYPE: Regex = Regex::new(r"\bstring\b").unwrap();

    /// Boolean type
    static ref BOOL_TYPE: Regex = Regex::new(r"\bbool\b").unwrap();

    /// Buffer/array types that need length testing
    static ref BUFFER_TYPE: Regex = Regex::new(r"\b(?:buffer|lbuffer|B\.buffer)\s+\w+").unwrap();

    /// Comparison operators in refinements for boundary detection
    static ref COMPARE_LT: Regex = Regex::new(r"(\w+)\s*<\s*(\d+)").unwrap();
    static ref COMPARE_LE: Regex = Regex::new(r"(\w+)\s*<=\s*(\d+)").unwrap();
    static ref COMPARE_GT: Regex = Regex::new(r"(\w+)\s*>\s*(\d+)").unwrap();
    static ref COMPARE_GE: Regex = Regex::new(r"(\w+)\s*>=\s*(\d+)").unwrap();
    static ref COMPARE_EQ: Regex = Regex::new(r"(\w+)\s*==?\s*(\d+)").unwrap();

    /// Lemma return type: the signature ends with or contains "-> Lemma" or ": Lemma"
    /// This covers patterns like:
    ///   val foo : x:int -> Lemma (ensures ...)
    ///   val foo : x:int -> Lemma (requires ...) (ensures ...)
    ///   val foo : Lemma (...)
    static ref LEMMA_RETURN: Regex = Regex::new(r"\bLemma\b").unwrap();

    /// GTot effect: ghost total computation, not extractable
    static ref GTOT_EFFECT: Regex = Regex::new(r"\bGTot\b").unwrap();

    /// Ghost.erased type: erased at extraction, not testable
    static ref GHOST_ERASED: Regex = Regex::new(r"\b(?:Ghost\.erased|erased)\b").unwrap();
}

/// Type of test suggestion.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum TestType {
    /// Test boundary values (min, max, off-by-one)
    BoundaryValue,
    /// Test edge cases (empty, singleton, etc.)
    EdgeCase,
    /// Property-based testing suggestion
    PropertyBased,
    /// Test based on refinement type constraints
    RefinementBased,
    /// Test for integer overflow/underflow
    IntegerBounds,
}

impl std::fmt::Display for TestType {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            TestType::BoundaryValue => write!(f, "boundary"),
            TestType::EdgeCase => write!(f, "edge-case"),
            TestType::PropertyBased => write!(f, "property"),
            TestType::RefinementBased => write!(f, "refinement"),
            TestType::IntegerBounds => write!(f, "int-bounds"),
        }
    }
}

/// A single test suggestion.
#[derive(Debug, Clone)]
pub struct TestSuggestion {
    /// Name of the function this test is for
    pub function_name: String,
    /// Type of test being suggested
    pub test_type: TestType,
    /// Human-readable description of what to test
    pub description: String,
    /// Example test values in F* syntax
    pub example_values: Vec<String>,
}

impl TestSuggestion {
    fn new(
        function_name: &str,
        test_type: TestType,
        description: &str,
        examples: Vec<&str>,
    ) -> Self {
        Self {
            function_name: function_name.to_string(),
            test_type,
            description: description.to_string(),
            example_values: examples.into_iter().map(String::from).collect(),
        }
    }
}

/// FST014: Test Generator Rule
///
/// Analyzes function signatures and suggests appropriate test cases.
/// Produces hints (not warnings) to guide test development.
pub struct TestGeneratorRule;

impl TestGeneratorRule {
    pub fn new() -> Self {
        Self
    }

    /// Analyze a function signature and generate test suggestions.
    fn analyze_function(&self, name: &str, signature: &str) -> Vec<TestSuggestion> {
        let mut suggestions = Vec::new();

        // Check for list/seq parameters - suggest empty and singleton tests
        self.check_collection_types(name, signature, &mut suggestions);

        // Check for option type - suggest None and Some tests
        self.check_option_type(name, signature, &mut suggestions);

        // Check for unsigned integer types - suggest boundary values
        self.check_unsigned_int_types(name, signature, &mut suggestions);

        // Check for signed integer types
        self.check_signed_int_types(name, signature, &mut suggestions);

        // Check for nat/pos types
        self.check_nat_pos_types(name, signature, &mut suggestions);

        // Check for refinement types - extract boundaries
        self.check_refinement_types(name, signature, &mut suggestions);

        // Check for string type - suggest empty and special chars
        self.check_string_type(name, signature, &mut suggestions);

        // Check for bool type - suggest both values
        self.check_bool_type(name, signature, &mut suggestions);

        // Check for buffer types - suggest length edge cases
        self.check_buffer_type(name, signature, &mut suggestions);

        suggestions
    }

    /// Check for list and sequence parameters.
    fn check_collection_types(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if LIST_PARAM.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test with empty list and singleton",
                vec!["[]", "[x]", "[x; y]"],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::PropertyBased,
                "Property: list operations preserve length invariants",
                vec!["List.length result == f (List.length input)"],
            ));
        }

        if SEQ_PARAM.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test with empty sequence and singleton",
                vec!["Seq.empty", "Seq.create 1 x", "Seq.append s1 s2"],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::PropertyBased,
                "Property: sequence length after operations",
                vec!["Seq.length result == expected_len"],
            ));
        }
    }

    /// Check for option type parameters.
    fn check_option_type(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if OPTION_PARAM.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test with None and Some cases",
                vec!["None", "Some x"],
            ));
        }
    }

    /// Check for unsigned integer types (U8, U16, U32, U64).
    fn check_unsigned_int_types(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if UINT8.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test uint8 boundaries",
                vec!["0uy", "1uy", "127uy", "128uy", "255uy"],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::IntegerBounds,
                "Test uint8 overflow conditions",
                vec!["255uy + 1uy wraps to 0uy"],
            ));
        }

        if UINT16.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test uint16 boundaries",
                vec!["0us", "1us", "0x7FFFus", "0x8000us", "0xFFFFus"],
            ));
        }

        if UINT32.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test uint32 boundaries",
                vec!["0ul", "1ul", "0x7FFFFFFFul", "0x80000000ul", "0xFFFFFFFFul"],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::IntegerBounds,
                "Test uint32 overflow conditions",
                vec!["max_uint32 + 1ul wraps", "0ul - 1ul underflows"],
            ));
        }

        if UINT64.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test uint64 boundaries",
                vec![
                    "0uL",
                    "1uL",
                    "0x7FFFFFFFFFFFFFFFuL",
                    "0x8000000000000000uL",
                    "0xFFFFFFFFFFFFFFFFuL",
                ],
            ));
        }
    }

    /// Check for signed integer types.
    fn check_signed_int_types(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if INT32.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test int32 boundaries (including negative)",
                vec!["0l", "1l", "-1l", "0x7FFFFFFFl (max)", "-0x80000000l (min)"],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::IntegerBounds,
                "Test int32 overflow/underflow",
                vec!["max_int32 + 1l overflows", "min_int32 - 1l underflows"],
            ));
        }
    }

    /// Check for nat and pos types.
    fn check_nat_pos_types(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if POS.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test pos (positive int) boundary",
                vec!["1", "2", "large positive value"],
            ));
        } else if NAT.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test nat (non-negative) boundary",
                vec!["0", "1", "large natural number"],
            ));
        } else if INT_TYPE.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test int with positive, zero, and negative",
                vec!["0", "1", "-1", "large positive", "large negative"],
            ));
        }
    }

    /// Check for refinement types and extract boundary conditions.
    fn check_refinement_types(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        // Check for explicit refinement patterns
        for caps in REFINEMENT.captures_iter(signature) {
            let param_name = caps.get(1).map(|m| m.as_str()).unwrap_or("x");
            let base_type = caps.get(2).map(|m| m.as_str()).unwrap_or("int");
            let constraint = caps.get(3).map(|m| m.as_str()).unwrap_or("");

            let boundaries = self.extract_boundaries_from_constraint(constraint);

            if !boundaries.is_empty() {
                suggestions.push(TestSuggestion::new(
                    name,
                    TestType::RefinementBased,
                    &format!(
                        "Test refinement boundaries for {}:{} where {}",
                        param_name, base_type, constraint
                    ),
                    boundaries.iter().map(|s| s.as_str()).collect(),
                ));
            } else {
                suggestions.push(TestSuggestion::new(
                    name,
                    TestType::RefinementBased,
                    &format!(
                        "Test refinement constraint: {} satisfies {{{}}}",
                        param_name, constraint
                    ),
                    vec![
                        "value at constraint boundary",
                        "value clearly satisfying",
                        "value near limit",
                    ],
                ));
            }
        }

        // Also check simple refinements without parameter names
        for caps in SIMPLE_REFINEMENT.captures_iter(signature) {
            // Skip if already matched by REFINEMENT
            let full_match = caps.get(0).map(|m| m.as_str()).unwrap_or("");
            if REFINEMENT.is_match(full_match) {
                continue;
            }

            let base_type = caps.get(1).map(|m| m.as_str()).unwrap_or("int");
            let constraint = caps.get(2).map(|m| m.as_str()).unwrap_or("");

            // Skip if constraint looks like a type parameter
            if constraint
                .chars()
                .all(|c| c.is_alphabetic() || c == ' ' || c == '_')
            {
                continue;
            }

            let boundaries = self.extract_boundaries_from_constraint(constraint);

            if !boundaries.is_empty() {
                suggestions.push(TestSuggestion::new(
                    name,
                    TestType::RefinementBased,
                    &format!("Test {} refinement: {{{}}}", base_type, constraint),
                    boundaries.iter().map(|s| s.as_str()).collect(),
                ));
            }
        }
    }

    /// Extract boundary test values from a constraint expression.
    fn extract_boundaries_from_constraint(&self, constraint: &str) -> Vec<String> {
        let mut boundaries = Vec::new();

        // Look for < N patterns: test N-1 (valid), N (invalid boundary)
        for caps in COMPARE_LT.captures_iter(constraint) {
            if let Some(val) = caps.get(2) {
                if let Ok(n) = val.as_str().parse::<i64>() {
                    if n > 0 {
                        boundaries.push(format!("{} (at limit)", n - 1));
                    }
                    boundaries.push(format!("{} (boundary)", n));
                }
            }
        }

        // Look for <= N patterns: test N (valid boundary), N+1 (invalid)
        for caps in COMPARE_LE.captures_iter(constraint) {
            if let Some(val) = caps.get(2) {
                if let Ok(n) = val.as_str().parse::<i64>() {
                    boundaries.push(format!("{} (at limit)", n));
                    boundaries.push(format!("{} (past limit)", n + 1));
                }
            }
        }

        // Look for > N patterns: test N+1 (valid), N (invalid boundary)
        for caps in COMPARE_GT.captures_iter(constraint) {
            if let Some(val) = caps.get(2) {
                if let Ok(n) = val.as_str().parse::<i64>() {
                    boundaries.push(format!("{} (boundary)", n));
                    boundaries.push(format!("{} (at limit)", n + 1));
                }
            }
        }

        // Look for >= N patterns: test N (valid boundary), N-1 (invalid)
        for caps in COMPARE_GE.captures_iter(constraint) {
            if let Some(val) = caps.get(2) {
                if let Ok(n) = val.as_str().parse::<i64>() {
                    if n > 0 {
                        boundaries.push(format!("{} (below limit)", n - 1));
                    }
                    boundaries.push(format!("{} (at limit)", n));
                }
            }
        }

        boundaries
    }

    /// Check for string type parameters.
    fn check_string_type(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if STRING_TYPE.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test string edge cases",
                vec![
                    "\"\"",
                    "\"a\"",
                    "\"longer string\"",
                    "string with special chars",
                ],
            ));
        }
    }

    /// Check for boolean type parameters.
    fn check_bool_type(&self, name: &str, signature: &str, suggestions: &mut Vec<TestSuggestion>) {
        if BOOL_TYPE.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test both boolean values",
                vec!["true", "false"],
            ));
        }
    }

    /// Check for buffer types.
    fn check_buffer_type(
        &self,
        name: &str,
        signature: &str,
        suggestions: &mut Vec<TestSuggestion>,
    ) {
        if BUFFER_TYPE.is_match(signature) {
            suggestions.push(TestSuggestion::new(
                name,
                TestType::EdgeCase,
                "Test buffer length edge cases",
                vec![
                    "empty buffer (len=0)",
                    "single element (len=1)",
                    "typical size",
                    "maximum expected size",
                ],
            ));

            suggestions.push(TestSuggestion::new(
                name,
                TestType::BoundaryValue,
                "Test buffer index boundaries",
                vec!["index 0", "index len-1", "ensure no out-of-bounds access"],
            ));
        }
    }
}

impl Default for TestGeneratorRule {
    fn default() -> Self {
        Self::new()
    }
}

impl TestGeneratorRule {
    /// Check if a module name indicates a specification module.
    /// Spec modules contain pure mathematical definitions, not extractable code.
    /// Examples: Spec.SHA2, Hacl.Spec.Bignum.Addition, Spec.Agile.Hash
    fn is_spec_module(module_name: &str) -> bool {
        // Module starts with "Spec." or contains ".Spec."
        module_name.starts_with("Spec.")
            || module_name.contains(".Spec.")
            // Also skip ".Lemmas" modules - they are collections of proofs
            || module_name.ends_with(".Lemmas")
            || module_name.contains(".Lemmas.")
    }

    /// Check if a function signature indicates a lemma (proof) declaration.
    /// Lemmas in F* are proofs themselves -- suggesting tests for proofs is nonsensical.
    /// Pattern: `val name : ... -> Lemma (...)` or `val name : ... -> Lemma (...) (...)`
    fn is_lemma_signature(signature: &str) -> bool {
        // The return type contains "Lemma" as a standalone word.
        // We look after the last "->" for the return type, but Lemma can also
        // appear in multi-line signatures, so also check the whole thing.
        LEMMA_RETURN.is_match(signature)
    }

    /// Check if a signature uses only ghost/erased types (not extractable).
    /// GTot is the ghost computation effect, Ghost.erased wraps erased values.
    fn is_ghost_function(signature: &str) -> bool {
        // Function returns in GTot effect (ghost total computation)
        GTOT_EFFECT.is_match(signature)
            // Or the return type is Ghost.erased / erased
            || GHOST_ERASED.is_match(signature)
    }

    /// Check if a function name suggests it is a lemma/proof helper.
    fn is_lemma_name(name: &str) -> bool {
        let lower = name.to_ascii_lowercase();
        lower.contains("lemma")
            || lower.contains("_lem_")
            || lower.ends_with("_lem")
    }

    /// Extract the module name from the raw file content.
    /// The module declaration is always in the header (first non-comment line),
    /// e.g. "module Hacl.Spec.Bignum.Addition"
    fn extract_module_name_from_content(content: &str) -> Option<String> {
        for line in content.lines() {
            let trimmed = line.trim();
            // Skip empty lines and comments
            if trimmed.is_empty() || trimmed.starts_with("(*") || trimmed.starts_with("//") {
                continue;
            }
            if let Some(rest) = trimmed.strip_prefix("module") {
                let name = rest.trim();
                if !name.is_empty() {
                    return Some(name.to_string());
                }
            }
            // Module declaration must appear very early; stop after first real line
            break;
        }
        None
    }
}

impl Rule for TestGeneratorRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST014
    }

    fn check(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        let (_, blocks) = parse_fstar_file(content);

        // Skip entire spec modules -- they are pure mathematical specifications,
        // not runtime-extractable code. Testing them makes no sense.
        if let Some(ref module_name) = Self::extract_module_name_from_content(content) {
            if Self::is_spec_module(module_name) {
                return diagnostics;
            }
        }

        // Also skip based on file path heuristics for files without module declarations
        if let Some(file_name) = file.file_name().and_then(|f| f.to_str()) {
            let lower = file_name.to_ascii_lowercase();
            if lower.starts_with("spec.") || lower.contains(".spec.") {
                return diagnostics;
            }
        }

        for block in &blocks {
            // Only analyze val declarations (function signatures)
            if block.block_type != BlockType::Val {
                continue;
            }

            // Join block lines to get full signature
            let signature = block.lines.join(" ");

            // Skip lemma declarations -- lemmas ARE the tests/proofs in F*.
            // Suggesting "write a test for this proof" is nonsensical.
            if Self::is_lemma_signature(&signature) {
                continue;
            }

            // Skip ghost/erased functions -- they are erased at extraction time
            // and cannot be tested at runtime.
            if Self::is_ghost_function(&signature) {
                continue;
            }

            for name in &block.names {
                // Skip internal functions (starting with underscore)
                if name.starts_with('_') {
                    continue;
                }

                // Skip functions whose names indicate they are lemma/proof helpers
                if Self::is_lemma_name(name) {
                    continue;
                }

                let suggestions = self.analyze_function(name, &signature);

                // Generate one diagnostic per test type to avoid overwhelming output
                let mut seen_types = std::collections::HashSet::new();

                for sugg in suggestions {
                    // Only show one suggestion per test type per function
                    if seen_types.contains(&sugg.test_type) {
                        continue;
                    }
                    seen_types.insert(sugg.test_type);

                    let examples_str = if sugg.example_values.len() <= 3 {
                        sugg.example_values.join(", ")
                    } else {
                        format!(
                            "{}, ... ({} more)",
                            sugg.example_values[..2].join(", "),
                            sugg.example_values.len() - 2
                        )
                    };

                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST014,
                        severity: DiagnosticSeverity::Info,
                        file: file.clone(),
                        range: Range::point(block.start_line, 1),
                        message: format!(
                            "[{}] Test `{}`: {} (e.g., {})",
                            sugg.test_type, sugg.function_name, sugg.description, examples_str
                        ),
                        fix: None,
                    });
                }
            }
        }

        diagnostics
    }
}

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

    fn make_path() -> PathBuf {
        PathBuf::from("test.fst")
    }

    fn make_spec_path() -> PathBuf {
        PathBuf::from("Spec.SHA2.fst")
    }

    // ---------------------------------------------------------------
    // Core suggestion tests (non-spec, non-lemma functions)
    // ---------------------------------------------------------------

    #[test]
    fn test_list_parameter_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval process_list : list int -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("empty list")));
        assert!(diags.iter().any(|d| d.message.contains("edge-case")));
    }

    #[test]
    fn test_seq_parameter_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval process_seq : Seq.seq int -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("empty sequence") || d.message.contains("Seq.empty")));
    }

    #[test]
    fn test_uint32_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval hash_value : U32.t -> U32.t\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("uint32") && d.message.contains("boundary")));
        assert!(diags
            .iter()
            .any(|d| d.message.contains("0ul") || d.message.contains("0xFFFFFFFF")));
    }

    #[test]
    fn test_uint64_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval process_large : UInt64.t -> bool\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("uint64")));
    }

    #[test]
    fn test_refinement_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval bounded_access : i:nat{i < 100} -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("refinement")));
        assert!(diags
            .iter()
            .any(|d| d.message.contains("99") || d.message.contains("100")));
    }

    #[test]
    fn test_nat_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval factorial : nat -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("nat") || d.message.contains("non-negative")));
        assert!(diags.iter().any(|d| d.message.contains("0")));
    }

    #[test]
    fn test_pos_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval divide : int -> pos -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("pos") || d.message.contains("positive")));
        assert!(diags.iter().any(|d| d.message.contains("1")));
    }

    #[test]
    fn test_option_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval maybe_process : option int -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("None") && d.message.contains("Some")));
    }

    #[test]
    fn test_bool_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval toggle : bool -> bool\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("true") && d.message.contains("false")));
    }

    #[test]
    fn test_string_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval parse_input : string -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("string") && d.message.contains("edge")));
    }

    #[test]
    fn test_buffer_type_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval read_buffer : buffer U8.t -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags
            .iter()
            .any(|d| d.message.contains("buffer") && d.message.contains("length")));
    }

    #[test]
    fn test_internal_function_skipped() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval _internal_helper : int -> int\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.is_empty());
    }

    #[test]
    fn test_multiple_refinement_boundaries() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval bounded_range : x:int{x >= 10 /\\ x < 100} -> bool\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("refinement")));
    }

    #[test]
    fn test_complex_signature() {
        let rule = TestGeneratorRule::new();
        let content =
            "module Test\n\nval complex_func : list (option U32.t) -> n:nat{n > 0} -> Seq.seq bool -> result\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.len() >= 3,
            "Expected multiple suggestions for complex signature"
        );
    }

    #[test]
    fn test_extract_boundaries_lt() {
        let rule = TestGeneratorRule::new();
        let boundaries = rule.extract_boundaries_from_constraint("x < 100");
        assert!(boundaries.iter().any(|b| b.contains("99")));
        assert!(boundaries.iter().any(|b| b.contains("100")));
    }

    #[test]
    fn test_extract_boundaries_ge() {
        let rule = TestGeneratorRule::new();
        let boundaries = rule.extract_boundaries_from_constraint("x >= 5");
        assert!(boundaries.iter().any(|b| b.contains("4")));
        assert!(boundaries.iter().any(|b| b.contains("5")));
    }

    #[test]
    fn test_no_suggestions_for_let_blocks() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nlet helper x = x + 1\n";
        let diags = rule.check(&make_path(), content);
        assert!(diags.is_empty());
    }

    // ---------------------------------------------------------------
    // Severity test: all diagnostics should be Info, not Hint
    // ---------------------------------------------------------------

    #[test]
    fn test_severity_is_info() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval process : U32.t -> U32.t\n";
        let diags = rule.check(&make_path(), content);
        assert!(!diags.is_empty(), "Should produce at least one suggestion");
        for d in &diags {
            assert_eq!(
                d.severity,
                DiagnosticSeverity::Info,
                "FST014 should use Info severity, not Hint"
            );
        }
    }

    // ---------------------------------------------------------------
    // False-positive filtering: spec modules
    // ---------------------------------------------------------------

    #[test]
    fn test_skip_spec_module_by_declaration() {
        let rule = TestGeneratorRule::new();
        let content = "module Spec.SHA2\n\nval hash : nat -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Spec.* modules should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_hacl_spec_module() {
        let rule = TestGeneratorRule::new();
        let content = "module Hacl.Spec.Bignum.Addition\n\nval bn_add : nat -> nat -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "*.Spec.* modules should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_spec_module_by_filename() {
        let rule = TestGeneratorRule::new();
        // No module declaration, but file name starts with Spec.
        let content = "val hash : nat -> nat\n";
        let diags = rule.check(&make_spec_path(), content);
        assert!(
            diags.is_empty(),
            "Spec.* files should produce zero suggestions even without module decl"
        );
    }

    #[test]
    fn test_skip_lemmas_module() {
        let rule = TestGeneratorRule::new();
        let content = "module Hacl.Spec.Montgomery.Lemmas\n\nval foo : pos -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "*.Lemmas modules should produce zero suggestions"
        );
    }

    // ---------------------------------------------------------------
    // False-positive filtering: lemma declarations
    // ---------------------------------------------------------------

    #[test]
    fn test_skip_lemma_declaration() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval add_comm : a:nat -> b:nat -> Lemma (a + b == b + a)\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Lemma declarations should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_lemma_with_requires_ensures() {
        let rule = TestGeneratorRule::new();
        let content = concat!(
            "module Test\n\n",
            "val mont_reduction_lemma : pbits:pos -> rLen:pos -> n:pos -> mu:nat -> c:nat -> Lemma\n",
            "  (requires c < n * n)\n",
            "  (ensures mont_reduction pbits rLen n mu c < n)\n"
        );
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Lemma (requires/ensures) should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_lemma_named_function() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval bn_add_lemma : nat -> nat -> bool\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Functions named *_lemma should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_lemma_named_function_loop() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval bn_add_lemma_loop : nat -> nat -> bool\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Functions with 'lemma' in name should produce zero suggestions"
        );
    }

    // ---------------------------------------------------------------
    // False-positive filtering: ghost/erased functions
    // ---------------------------------------------------------------

    #[test]
    fn test_skip_gtot_function() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval ghost_fn : nat -> GTot nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "GTot functions should produce zero suggestions, got {}",
            diags.len()
        );
    }

    #[test]
    fn test_skip_ghost_erased() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval erased_fn : Ghost.erased nat -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Ghost.erased functions should produce zero suggestions, got {}",
            diags.len()
        );
    }

    // ---------------------------------------------------------------
    // Non-spec modules should still produce suggestions
    // ---------------------------------------------------------------

    #[test]
    fn test_non_spec_module_produces_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Hacl.Bignum.Addition\n\nval bn_add : nat -> nat -> nat\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.is_empty(),
            "Non-spec modules should still produce suggestions"
        );
    }

    #[test]
    fn test_non_lemma_function_produces_suggestions() {
        let rule = TestGeneratorRule::new();
        let content = "module Test\n\nval compute_hash : U32.t -> U32.t\n";
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.is_empty(),
            "Non-lemma functions should produce suggestions"
        );
    }

    // ---------------------------------------------------------------
    // Helper method unit tests
    // ---------------------------------------------------------------

    #[test]
    fn test_is_spec_module() {
        assert!(TestGeneratorRule::is_spec_module("Spec.SHA2"));
        assert!(TestGeneratorRule::is_spec_module("Spec.Agile.Hash"));
        assert!(TestGeneratorRule::is_spec_module("Hacl.Spec.Bignum.Addition"));
        assert!(TestGeneratorRule::is_spec_module("Hacl.Spec.Montgomery.Lemmas"));
        assert!(TestGeneratorRule::is_spec_module("Foo.Bar.Lemmas"));
        assert!(TestGeneratorRule::is_spec_module("Foo.Lemmas.Helper"));

        assert!(!TestGeneratorRule::is_spec_module("Hacl.Bignum.Addition"));
        assert!(!TestGeneratorRule::is_spec_module("Test"));
        assert!(!TestGeneratorRule::is_spec_module("MyModule.SpecHelper"));
    }

    #[test]
    fn test_is_lemma_signature() {
        assert!(TestGeneratorRule::is_lemma_signature("a:nat -> b:nat -> Lemma (a + b == b + a)"));
        assert!(TestGeneratorRule::is_lemma_signature(
            "pbits:pos -> Lemma (requires c < n) (ensures r < n)"
        ));
        assert!(TestGeneratorRule::is_lemma_signature("Lemma (true)"));

        assert!(!TestGeneratorRule::is_lemma_signature("nat -> nat"));
        assert!(!TestGeneratorRule::is_lemma_signature("U32.t -> U32.t"));
    }

    #[test]
    fn test_is_ghost_function() {
        assert!(TestGeneratorRule::is_ghost_function("nat -> GTot nat"));
        assert!(TestGeneratorRule::is_ghost_function("Ghost.erased nat -> nat"));
        assert!(TestGeneratorRule::is_ghost_function("x:erased int -> int"));

        assert!(!TestGeneratorRule::is_ghost_function("nat -> nat"));
        assert!(!TestGeneratorRule::is_ghost_function("U32.t -> bool"));
    }

    #[test]
    fn test_is_lemma_name() {
        assert!(TestGeneratorRule::is_lemma_name("bn_add_lemma"));
        assert!(TestGeneratorRule::is_lemma_name("bn_add_lemma_loop"));
        assert!(TestGeneratorRule::is_lemma_name("mont_reduction_lemma_step"));
        assert!(TestGeneratorRule::is_lemma_name("foo_lem_bar"));
        assert!(TestGeneratorRule::is_lemma_name("foo_lem"));

        assert!(!TestGeneratorRule::is_lemma_name("bn_add"));
        assert!(!TestGeneratorRule::is_lemma_name("hash_value"));
        assert!(!TestGeneratorRule::is_lemma_name("process"));
    }
}