brrr-lint 0.1.0

//! FST011: Effect checker.
//!
//! Detects effect-related issues in F* code:
//!
//! F* Effect Hierarchy (lattice with TWO branches):
//! ```text
//!                    Tot (pure total)
//!                   /                \
//!                  /                  \
//!               GTot                 Pure
//!           (ghost total)       (pre/post, may diverge)
//!                |                    |
//!              Ghost                 Div
//!           (erased)            (divergent)
//!                |                 /    \
//!              Lemma             ST     Exn
//!                              (state) (exceptions)
//!                                 \    /
//!                                  All
//!                               (combined)
//!                                   |
//!                                  ML
//!                            (unrestricted)
//! ```
//!
//! Key rules:
//! - Ghost branch (erased at extraction): Tot -> GTot -> Ghost/Lemma
//! - Computational branch (extracted): Tot -> Pure -> Div -> ST/Exn -> All -> ML
//! - Ghost and Pure are on SEPARATE branches - Ghost cannot call Pure
//! - ST and Exn can both call Div (divergence is a sub-effect of both)
//!
//! Checks:
//! 1. `admit()` usage - bypasses verification
//! 2. `magic()` usage - produces arbitrary values unsafely
//! 3. `unsafe_coerce` usage - bypasses type safety
//! 4. Overly permissive ML effect when more restrictive would suffice
//! 5. Tot function calling effectful code
//! 6. Ghost in computational (non-ghost) context

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

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

/// F* Effect hierarchy.
///
/// Effects are ordered from most restrictive (Tot) to least restrictive (ML).
/// The ordering determines what effects a function can call.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Effect {
    /// Pure total - always terminates, no side effects, no ghost
    Tot,
    /// Ghost total - ghost computation that terminates
    GTot,
    /// Pure with pre/post conditions
    Pure,
    /// Ghost computation (erased at extraction)
    Ghost,
    /// Lemma - special ghost for proofs (equivalent to Ghost for hierarchy)
    Lemma,
    /// Divergent - may not terminate
    Div,
    /// Stateful - heap operations
    ST,
    /// Exception - may raise exceptions
    Exn,
    /// All effects - state + exceptions + divergence
    All,
    /// ML - unrestricted effects (OCaml-like)
    ML,
}

impl Effect {
    /// Parse an effect from its string representation.
    ///
    /// Returns None for unrecognized effect names.
    pub fn from_str(s: &str) -> Option<Self> {
        match s {
            "Tot" => Some(Effect::Tot),
            "GTot" => Some(Effect::GTot),
            "Pure" => Some(Effect::Pure),
            "Ghost" => Some(Effect::Ghost),
            "Lemma" => Some(Effect::Lemma),
            "Div" | "Dv" => Some(Effect::Div),
            "ST" | "Stack" | "STATE" | "State" => Some(Effect::ST),
            "Exn" | "Ex" => Some(Effect::Exn),
            "All" => Some(Effect::All),
            "ML" => Some(Effect::ML),
            _ => None,
        }
    }

    /// Returns the hierarchy level of this effect.
    ///
    /// Lower values are more restrictive. Used for effect compatibility checks.
    fn level(&self) -> u8 {
        match self {
            Effect::Tot => 0,
            Effect::GTot => 1,
            Effect::Pure => 2,
            Effect::Ghost | Effect::Lemma => 3,
            Effect::Div => 4,
            Effect::ST => 5,
            Effect::Exn => 5,
            Effect::All => 6,
            Effect::ML => 7,
        }
    }

    /// Check if this effect can call a function with the given effect.
    ///
    /// Effect compatibility rules (based on F* effect lattice):
    /// - Tot can only call Tot (most restrictive)
    /// - GTot can call Tot, GTot (ghost-compatible only)
    /// - Pure can call Tot, Pure (computational branch)
    /// - Ghost/Lemma can call Tot, GTot, Ghost, Lemma (ghost branch only)
    /// - Div can call Tot, Pure, Div
    /// - ST can call Tot, Pure, Div, ST (state effects)
    /// - Exn can call Tot, Pure, Div, Exn (exception effects)
    /// - All can call anything except ML
    /// - ML can call anything (least restrictive)
    pub fn can_call(&self, callee: Effect) -> bool {
        match (self, callee) {
            // Tot is the most restrictive - can only call Tot
            (Effect::Tot, Effect::Tot) => true,
            (Effect::Tot, _) => false,

            // GTot can call Tot and GTot (ghost-compatible)
            (Effect::GTot, Effect::Tot) => true,
            (Effect::GTot, Effect::GTot) => true,
            (Effect::GTot, _) => false,

            // Pure can call Tot and Pure
            (Effect::Pure, Effect::Tot) => true,
            (Effect::Pure, Effect::Pure) => true,
            (Effect::Pure, _) => false,

            // Ghost/Lemma can call ghost-compatible effects
            (Effect::Ghost | Effect::Lemma, Effect::Tot) => true,
            (Effect::Ghost | Effect::Lemma, Effect::GTot) => true,
            (Effect::Ghost | Effect::Lemma, Effect::Ghost) => true,
            (Effect::Ghost | Effect::Lemma, Effect::Lemma) => true,
            (Effect::Ghost | Effect::Lemma, _) => false,

            // Div can call Tot, Pure, Div
            (Effect::Div, Effect::Tot) => true,
            (Effect::Div, Effect::Pure) => true,
            (Effect::Div, Effect::Div) => true,
            (Effect::Div, _) => false,

            // ST can call Tot, Pure, Div, ST
            (Effect::ST, Effect::Tot) => true,
            (Effect::ST, Effect::Pure) => true,
            (Effect::ST, Effect::Div) => true,
            (Effect::ST, Effect::ST) => true,
            (Effect::ST, _) => false,

            // Exn can call Tot, Pure, Div, Exn
            // (Div is a sub-effect of Exn - exceptions may also diverge)
            (Effect::Exn, Effect::Tot) => true,
            (Effect::Exn, Effect::Pure) => true,
            (Effect::Exn, Effect::Div) => true,
            (Effect::Exn, Effect::Exn) => true,
            (Effect::Exn, _) => false,

            // All can call anything except ML
            (Effect::All, Effect::ML) => false,
            (Effect::All, _) => true,

            // ML can call anything
            (Effect::ML, _) => true,
        }
    }

    /// Check if this effect is a ghost effect (erased at extraction).
    pub fn is_ghost(&self) -> bool {
        matches!(self, Effect::GTot | Effect::Ghost | Effect::Lemma)
    }

    /// Check if this effect is computational (not ghost).
    pub fn is_computational(&self) -> bool {
        !self.is_ghost() && *self != Effect::Tot
    }

    /// Human-readable name for error messages.
    pub fn display_name(&self) -> &'static str {
        match self {
            Effect::Tot => "Tot",
            Effect::GTot => "GTot",
            Effect::Pure => "Pure",
            Effect::Ghost => "Ghost",
            Effect::Lemma => "Lemma",
            Effect::Div => "Div",
            Effect::ST => "ST",
            Effect::Exn => "Exn",
            Effect::All => "All",
            Effect::ML => "ML",
        }
    }
}

impl PartialOrd for Effect {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.level().cmp(&other.level()))
    }
}

impl Ord for Effect {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        self.level().cmp(&other.level())
    }
}

lazy_static! {
    /// Pattern for admit() - bypasses verification
    static ref ADMIT_PATTERN: Regex = Regex::new(r"\badmit\s*\(\s*\)").unwrap();

    /// Pattern for magic() - produces arbitrary values
    static ref MAGIC_PATTERN: Regex = Regex::new(r"\bmagic\s*\(\s*\)").unwrap();

    /// Pattern for unsafe_coerce - bypasses type safety
    static ref UNSAFE_COERCE: Regex = Regex::new(r"\bunsafe_coerce\b").unwrap();

    /// Pattern for ML effect annotation
    static ref ML_EFFECT: Regex = Regex::new(r"\bML\b").unwrap();

    /// Pattern for extract-related context (ML is acceptable here)
    static ref EXTRACT_CONTEXT: Regex = Regex::new(r"\b(?:extract|extraction|noextract|inline_for_extraction)\b").unwrap();

    /// Pattern for assume_val - bypasses specification checking
    static ref ASSUME_VAL: Regex = Regex::new(r"\bassume\s+val\b").unwrap();

    /// Pattern for assume (expr) - bypasses verification of a condition
    /// Note: Must NOT match `assume val` which is handled separately
    static ref ASSUME_EXPR: Regex = Regex::new(r"\bassume\s*\(").unwrap();

    /// Pattern for finding column position of a pattern match
    static ref ADMIT_COLUMN: Regex = Regex::new(r"\badmit\s*\(").unwrap();
    static ref MAGIC_COLUMN: Regex = Regex::new(r"\bmagic\s*\(").unwrap();

    /// Pattern for effect annotation in function signatures.
    /// Matches: -> Tot, -> GTot, -> Pure, -> Ghost, -> ST, etc.
    static ref EFFECT_ANNOTATION: Regex = Regex::new(
        r"(?:->|:)\s*(Tot|GTot|Pure|Ghost|Lemma|ST|Stack|STATE|State|Exn|Ex|Div|Dv|All|ML)\b"
    ).unwrap();

    /// Pattern for function call detection.
    /// Matches: function_name (...) or function_name arg or function_name "string"
    static ref FUNCTION_CALL: Regex = Regex::new(
        r#"\b([a-z_][a-zA-Z0-9_']*)\s*(?:\(|[a-z_0-9"])"#
    ).unwrap();

    /// Pattern for ghost annotation on let bindings.
    static ref GHOST_LET: Regex = Regex::new(r"\bghost\s+let\b").unwrap();

    /// Pattern for inline_for_extraction (computational context).
    static ref INLINE_EXTRACTION: Regex = Regex::new(r"\binline_for_extraction\b").unwrap();

    /// Pattern for unqualified identifier reference (not preceded by a dot).
    /// Used for ghost binding detection where we need to find variable references,
    /// not just function calls.
    static ref UNQUALIFIED_IDENT: Regex = Regex::new(r"\b([a-z_][a-zA-Z0-9_']*)\b").unwrap();

    /// Known built-in functions that are Tot (pure).
    static ref TOT_BUILTINS: std::collections::HashSet<&'static str> = {
        let mut s = std::collections::HashSet::new();
        // Arithmetic operators (as functions)
        for name in &["op_Addition", "op_Subtraction", "op_Multiply", "op_Division",
                      "op_Modulus", "op_Plus", "op_Minus"] {
            s.insert(*name);
        }
        // Comparison operators
        for name in &["op_Equality", "op_disEquality", "op_LessThan", "op_GreaterThan",
                      "op_LessThanOrEqual", "op_GreaterThanOrEqual"] {
            s.insert(*name);
        }
        // Boolean operators
        for name in &["op_Negation", "op_AmpAmp", "op_BarBar", "not"] {
            s.insert(*name);
        }
        // List operations (Tot) - FStar.List.Tot
        for name in &["hd", "tl", "length", "rev", "append", "mem", "nth", "map", "filter",
                      "fold_left", "fold_right", "for_all", "existsb", "find", "index",
                      "splitAt", "split", "unzip", "zip", "assoc", "concat", "flatten"] {
            s.insert(*name);
        }
        // Option operations (Tot)
        for name in &["Some", "None", "is_Some", "is_None"] {
            s.insert(*name);
        }
        // Tuple operations (Tot)
        for name in &["fst", "snd", "dfst", "dsnd"] {
            s.insert(*name);
        }
        // Basic combinators (Tot)
        for name in &["id", "const", "compose", "on"] {
            s.insert(*name);
        }
        // Normalization functions (Tot - type-level computation)
        for name in &["normalize_term", "normalize", "norm", "norm_spec", "reveal_opaque"] {
            s.insert(*name);
        }
        // Sequence operations (FStar.Seq - Tot)
        for name in &["create", "init", "empty", "seq_length", "seq_index", "upd",
                      "slice", "append", "cons", "snoc", "head", "tail", "last",
                      "seq_to_list", "seq_of_list", "equal"] {
            s.insert(*name);
        }
        // Classical logic (Tot/GTot)
        for name in &["squash", "return_squash", "get_proof", "bind_squash"] {
            s.insert(*name);
        }
        s
    };

    /// Known effectful functions (not Tot).
    /// Includes both simple names and last component of qualified names.
    static ref EFFECTFUL_FUNCTIONS: HashMap<&'static str, Effect> = {
        let mut m = HashMap::new();
        // IO effects (FStar.IO)
        m.insert("print_string", Effect::ML);
        m.insert("print_newline", Effect::ML);
        m.insert("print_int", Effect::ML);
        m.insert("print_any", Effect::ML);
        m.insert("prerr_string", Effect::ML);
        m.insert("read_line", Effect::ML);
        m.insert("input_line", Effect::ML);
        m.insert("input_int", Effect::ML);
        m.insert("input_float", Effect::ML);
        m.insert("debug_print_string", Effect::ML);
        // Reference operations (FStar.Ref, FStar.ST)
        m.insert("alloc", Effect::ST);
        m.insert("read", Effect::ST);
        m.insert("write", Effect::ST);
        m.insert("op_Bang", Effect::ST);
        m.insert("op_Colon_Equals", Effect::ST);
        m.insert("recall", Effect::ST);
        m.insert("witness_token", Effect::ST);
        m.insert("recall_token", Effect::ST);
        // HyperStack operations
        m.insert("get", Effect::ST);
        m.insert("push_frame", Effect::ST);
        m.insert("pop_frame", Effect::ST);
        m.insert("salloc", Effect::ST);
        m.insert("sfree", Effect::ST);
        // Buffer operations (LowStar.Buffer, Lib.Buffer)
        m.insert("malloc", Effect::ST);
        m.insert("free", Effect::ST);
        m.insert("blit", Effect::ST);
        m.insert("fill", Effect::ST);
        m.insert("index", Effect::ST);  // mutable index
        m.insert("upd", Effect::ST);    // mutable update
        m.insert("sub", Effect::ST);
        m.insert("offset", Effect::ST);
        // Exception operations (FStar.Exn)
        m.insert("raise", Effect::Exn);
        m.insert("try_with", Effect::Exn);
        m.insert("failwith", Effect::Exn);
        // Ghost operations (FStar.Ghost)
        m.insert("reveal", Effect::Ghost);
        m.insert("hide", Effect::Ghost);
        m.insert("elim_pure", Effect::Ghost);
        m
    };

    /// Pattern for qualified function names (e.g., FStar.IO.print_string)
    /// Captures the last component of the qualified name.
    static ref QUALIFIED_CALL: Regex = Regex::new(
        r"\b(?:[A-Z][\w']*\.)+([a-z_][\w']*)\b"
    ).unwrap();
}

/// Strip comments and string literals from a line to avoid false positives.
///
/// Removes:
/// - Single-line block comments: `(* ... *)`
/// - Line comments: `// ...`
/// - String literals: `"..."`
///
/// This is a best-effort approach for single-line analysis.
/// Multi-line comments spanning multiple lines are NOT handled (would require
/// tracking state across lines).
fn strip_comments_and_strings(line: &str) -> String {
    let mut result = String::with_capacity(line.len());
    let chars: Vec<char> = line.chars().collect();
    let len = chars.len();
    let mut i = 0;

    while i < len {
        // Check for string literal start
        if chars[i] == '"' {
            // Skip until closing quote (handle escape sequences)
            i += 1;
            while i < len {
                if chars[i] == '\\' && i + 1 < len {
                    i += 2; // Skip escaped char
                } else if chars[i] == '"' {
                    i += 1;
                    break;
                } else {
                    i += 1;
                }
            }
            // Replace string content with placeholder to preserve spacing
            result.push_str("\"\"");
        }
        // Check for block comment start: (*
        else if chars[i] == '(' && i + 1 < len && chars[i + 1] == '*' {
            // Skip until closing *)
            i += 2;
            let mut depth = 1;
            while i < len && depth > 0 {
                if chars[i] == '(' && i + 1 < len && chars[i + 1] == '*' {
                    depth += 1;
                    i += 2;
                } else if chars[i] == '*' && i + 1 < len && chars[i + 1] == ')' {
                    depth -= 1;
                    i += 2;
                } else {
                    i += 1;
                }
            }
            // Comment stripped, add a space to separate tokens
            result.push(' ');
        }
        // Check for line comment: //
        else if chars[i] == '/' && i + 1 < len && chars[i + 1] == '/' {
            // Skip rest of line
            break;
        }
        // Regular character
        else {
            result.push(chars[i]);
            i += 1;
        }
    }

    result
}

/// Check if a line is entirely within a comment.
///
/// Returns true if the line starts with a comment opener and has no code after,
/// or is empty/whitespace.
fn is_comment_line(line: &str) -> bool {
    let trimmed = line.trim();
    if trimmed.is_empty() {
        return true;
    }

    // Line comment - everything after // is comment
    if trimmed.starts_with("//") {
        return true;
    }

    // Lines that start with * and are continuation of multi-line comments
    if (trimmed.starts_with('*') && !trimmed.starts_with("**") && !trimmed.starts_with("*)"))
        || trimmed.starts_with("*)")
    {
        return true;
    }

    // Block comment that starts and ends on the same line - check if there's code after
    if trimmed.starts_with("(*") {
        // Find matching *) and check if there's code after
        let after_comment = strip_comments_and_strings(trimmed);
        // If only whitespace remains after stripping, it's a comment line
        return after_comment.trim().is_empty();
    }

    false
}

/// Extract the effect annotation from a declaration block.
///
/// Looks for effect annotations in the function signature (e.g., `-> Tot int`).
/// Returns None if no explicit effect annotation is found.
fn extract_function_effect(block: &DeclarationBlock) -> Option<Effect> {
    let text = block.lines.join("");
    EFFECT_ANNOTATION
        .captures(&text)
        .and_then(|c| c.get(1))
        .and_then(|m| Effect::from_str(m.as_str()))
}

/// Check if a declaration block is an explicit `ghost let` binding.
///
/// Only matches explicit `ghost let` patterns, NOT functions that merely
/// have `Ghost.erased` parameters or GTot effect. This distinction is
/// critical to avoid false positives:
/// - `Ghost.erased` parameters are type-level erasure markers, not ghost bindings
/// - GTot functions can be called from specification positions (requires/ensures)
/// - `inline_for_extraction` functions with `#t:limb_t` erased params are valid
/// - Only actual ghost VALUE bindings (`ghost let x = ...`) cannot be used computationally
///
/// The old `erased` keyword matching caused massive false positives:
/// - 621 in hacl-star (matched `Ghost.erased` in val parameter types)
/// - 2762 in everparse (same pattern, more prevalent)
fn is_explicit_ghost_let(block: &DeclarationBlock) -> bool {
    let text = block.lines.join("");
    GHOST_LET.is_match(&text)
}

/// Check if a declaration block is marked for extraction (computational).
fn is_extraction_binding(block: &DeclarationBlock) -> bool {
    let text = block.lines.join("");
    INLINE_EXTRACTION.is_match(&text)
}

/// Extract ONLY unqualified identifier references from a code block.
///
/// This is used for ghost binding checking where we need to find any
/// reference to a local ghost binding. Unlike `extract_function_calls`,
/// this finds ALL identifier references, not just function calls.
///
/// Returns identifiers that are:
/// - NOT preceded by a dot (qualified references like Module.name are excluded)
/// - NOT keywords
/// - NOT type constructors (starting with uppercase)
fn extract_unqualified_function_calls(block: &DeclarationBlock) -> Vec<(String, usize)> {
    let mut identifiers = Vec::new();

    for (idx, line) in block.lines.iter().enumerate() {
        let line_num = block.start_line + idx;

        // Skip comment lines
        let trimmed = line.trim();
        if trimmed.starts_with("(*") || trimmed.starts_with("//") {
            continue;
        }

        // Strip inline comments and strings to avoid false positives
        let code_only = strip_comments_and_strings(line);

        // Find all unqualified identifiers (not preceded by a dot)
        for caps in UNQUALIFIED_IDENT.captures_iter(&code_only) {
            if let Some(m) = caps.get(1) {
                let name = m.as_str();
                let start = m.start();

                // Check if this is a qualified reference (preceded by a dot)
                let is_qualified = start > 0 && code_only.as_bytes().get(start - 1) == Some(&b'.');

                // Skip keywords, type constructors, and qualified references
                if !is_keyword(name)
                    && !name
                        .chars()
                        .next()
                        .map(|c| c.is_uppercase())
                        .unwrap_or(false)
                    && !is_qualified
                {
                    // Avoid duplicates on same line
                    if !identifiers.iter().any(|(n, l)| n == name && *l == line_num) {
                        identifiers.push((name.to_string(), line_num));
                    }
                }
            }
        }
    }

    identifiers
}

/// Extract function calls from a code block.
///
/// Returns a vector of (function_name, line_number) pairs.
/// For qualified names like FStar.IO.print_string, returns just "print_string".
fn extract_function_calls(block: &DeclarationBlock) -> Vec<(String, usize)> {
    let mut calls = Vec::new();

    for (idx, line) in block.lines.iter().enumerate() {
        let line_num = block.start_line + idx;

        // Skip comment lines
        let trimmed = line.trim();
        if trimmed.starts_with("(*") || trimmed.starts_with("//") {
            continue;
        }

        // Strip inline comments to avoid false positives
        let code_only = strip_comments_and_strings(line);

        // Find qualified function calls (e.g., FStar.IO.print_string)
        for caps in QUALIFIED_CALL.captures_iter(&code_only) {
            if let Some(m) = caps.get(1) {
                let name = m.as_str();
                if !is_keyword(name) {
                    calls.push((name.to_string(), line_num));
                }
            }
        }

        // Find simple function calls
        for caps in FUNCTION_CALL.captures_iter(&code_only) {
            if let Some(m) = caps.get(1) {
                let name = m.as_str();
                // Skip keywords and type constructors (start with uppercase)
                if !is_keyword(name)
                    && !name
                        .chars()
                        .next()
                        .map(|c| c.is_uppercase())
                        .unwrap_or(false)
                {
                    // Avoid duplicates from qualified call detection
                    if !calls.iter().any(|(n, l)| n == name && *l == line_num) {
                        calls.push((name.to_string(), line_num));
                    }
                }
            }
        }
    }

    calls
}

/// Check if a name is an F* keyword.
fn is_keyword(name: &str) -> bool {
    matches!(
        name,
        "let"
            | "rec"
            | "in"
            | "if"
            | "then"
            | "else"
            | "match"
            | "with"
            | "fun"
            | "function"
            | "val"
            | "type"
            | "and"
            | "open"
            | "module"
            | "assume"
            | "assert"
            | "requires"
            | "ensures"
            | "decreases"
            | "forall"
            | "exists"
            | "true"
            | "false"
            | "not"
            | "begin"
            | "end"
            | "private"
            | "unfold"
            | "inline_for_extraction"
            | "noextract"
            | "irreducible"
            | "noeq"
            | "abstract"
    )
}

/// FST011: Effect Checker
///
/// Analyzes F* effect usage for potential issues including verification
/// bypasses, overly permissive effect annotations, and effect hierarchy violations.
pub struct EffectCheckerRule;

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

    /// Find the column position of a regex match in a line.
    fn find_column(line: &str, pattern: &Regex) -> usize {
        pattern.find(line).map(|m| m.start() + 1).unwrap_or(1)
    }

    /// Check for admit() usage.
    ///
    /// `admit()` bypasses the verification of the current goal, accepting
    /// it as true without proof. This is dangerous in production code.
    fn check_admit(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);

            if ADMIT_PATTERN.is_match(&code_only) {
                let col = Self::find_column(line, &ADMIT_COLUMN);
                diagnostics.push(Diagnostic {
                    rule: RuleCode::FST011,
                    severity: DiagnosticSeverity::Warning,
                    file: file.clone(),
                    range: Range::point(line_num, col),
                    message: "`admit()` bypasses verification - remove before production. \
                              Consider proving the goal or using `assume` with documentation."
                        .to_string(),
                    fix: None,
                });
            }
        }

        diagnostics
    }

    /// Check for magic() usage.
    ///
    /// `magic()` produces a value of any type without justification.
    /// This completely undermines the type system and verification.
    fn check_magic(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);

            if MAGIC_PATTERN.is_match(&code_only) {
                let col = Self::find_column(line, &MAGIC_COLUMN);
                diagnostics.push(Diagnostic {
                    rule: RuleCode::FST011,
                    severity: DiagnosticSeverity::Error,
                    file: file.clone(),
                    range: Range::point(line_num, col),
                    message: "`magic()` produces arbitrary values of any type - \
                              this completely bypasses type safety and verification!"
                        .to_string(),
                    fix: None,
                });
            }
        }

        diagnostics
    }

    /// Check for unsafe_coerce usage.
    ///
    /// `unsafe_coerce` forces a type conversion without proof,
    /// potentially leading to runtime errors or undefined behavior.
    fn check_unsafe_coerce(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);

            if UNSAFE_COERCE.is_match(&code_only) {
                if let Some(m) = UNSAFE_COERCE.find(line) {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST011,
                        severity: DiagnosticSeverity::Error,
                        file: file.clone(),
                        range: Range::point(line_num, m.start() + 1),
                        message:
                            "`unsafe_coerce` bypasses type safety - use with extreme caution. \
                                  Consider using a proper type refinement or coercion lemma."
                                .to_string(),
                        fix: None,
                    });
                }
            }
        }

        diagnostics
    }

    /// Check for overly permissive ML effect.
    ///
    /// The ML effect allows arbitrary side effects including divergence,
    /// state, and exceptions. Often a more restrictive effect would suffice.
    fn check_ml_effect(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);
            let trimmed = code_only.trim();

            // Check for ML effect
            if ML_EFFECT.is_match(&code_only) {
                // Skip if in extraction context (ML is expected there)
                if EXTRACT_CONTEXT.is_match(&code_only) {
                    continue;
                }

                // Skip if this is a type definition or effect definition
                if trimmed.starts_with("type ") || trimmed.starts_with("effect ") {
                    continue;
                }

                if let Some(m) = ML_EFFECT.find(line) {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST011,
                        severity: DiagnosticSeverity::Info,
                        file: file.clone(),
                        range: Range::point(line_num, m.start() + 1),
                        message: "ML effect is overly permissive - allows divergence, state, \
                                  and exceptions. Consider using Tot, ST, or a custom effect."
                            .to_string(),
                        fix: None,
                    });
                }
            }
        }

        diagnostics
    }

    /// Check for assume val declarations.
    ///
    /// `assume val` declarations are axioms that bypass verification.
    /// They should be documented and minimized.
    fn check_assume_val(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);

            if ASSUME_VAL.is_match(&code_only) {
                if let Some(m) = ASSUME_VAL.find(line) {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST011,
                        severity: DiagnosticSeverity::Info,
                        file: file.clone(),
                        range: Range::point(line_num, m.start() + 1),
                        message: "`assume val` is an axiom that bypasses verification. \
                                  Ensure this assumption is sound and documented."
                            .to_string(),
                        fix: None,
                    });
                }
            }
        }

        diagnostics
    }

    /// Check for assume (expr) usage.
    ///
    /// `assume (condition)` tells F* to accept a condition as true without proof.
    /// This bypasses verification for that specific condition and can hide bugs.
    /// Unlike `assume val` which declares an external axiom, `assume (expr)` is
    /// typically used inline to work around verification failures.
    fn check_assume_expr(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        for (line_idx, line) in content.lines().enumerate() {
            let line_num = line_idx + 1;

            // Skip lines that are entirely comments
            if is_comment_line(line) {
                continue;
            }

            // Strip inline comments and strings to avoid false positives
            let code_only = strip_comments_and_strings(line);

            // Check for assume (expr) but NOT assume val (handled separately)
            if ASSUME_EXPR.is_match(&code_only) && !ASSUME_VAL.is_match(&code_only) {
                if let Some(m) = ASSUME_EXPR.find(line) {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST011,
                        severity: DiagnosticSeverity::Warning,
                        file: file.clone(),
                        range: Range::point(line_num, m.start() + 1),
                        message: "`assume (...)` bypasses verification for a specific condition. \
                                  Consider proving this property or documenting why it's safe."
                            .to_string(),
                        fix: None,
                    });
                }
            }
        }

        diagnostics
    }

    /// Check for Tot functions calling effectful code.
    ///
    /// A function annotated with Tot effect must only call other Tot functions.
    /// Calling effectful functions (ST, Exn, ML, etc.) from Tot is an error.
    fn check_tot_calling_effectful(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();
        let (_, blocks) = parse_fstar_file(content);

        // Build map of function name -> effect from val declarations
        // In F*, val declares the signature (with effect), let provides implementation
        let mut function_effects: HashMap<String, Effect> = HashMap::new();
        for block in &blocks {
            if let Some(eff) = extract_function_effect(block) {
                for name in &block.names {
                    function_effects.insert(name.clone(), eff);
                }
            }
        }

        // Check each let block for calls to effectful functions
        // Look up the effect from the corresponding val declaration
        for block in &blocks {
            // Only check let blocks (where actual code is)
            if !matches!(
                block.block_type,
                BlockType::Let | BlockType::UnfoldLet | BlockType::InlineLet
            ) {
                continue;
            }

            // Get the effect for this function from the map (from val) or from the block itself
            let caller_effect = block
                .name()
                .and_then(|n| function_effects.get(n).copied())
                .or_else(|| extract_function_effect(block));

            // Only check Tot functions
            if caller_effect != Some(Effect::Tot) {
                continue;
            }

            // Extract all function calls from this block
            let calls = extract_function_calls(block);

            for (callee_name, line_num) in calls {
                // Check if callee has a known effect
                let callee_effect = function_effects
                    .get(&callee_name)
                    .copied()
                    .or_else(|| EFFECTFUL_FUNCTIONS.get(callee_name.as_str()).copied());

                if let Some(callee_eff) = callee_effect {
                    // Tot cannot call effectful functions
                    if !Effect::Tot.can_call(callee_eff) {
                        diagnostics.push(Diagnostic {
                            rule: RuleCode::FST011,
                            severity: DiagnosticSeverity::Error,
                            file: file.clone(),
                            range: Range::point(line_num, 1),
                            message: format!(
                                "Tot function `{}` calls `{}` which has {} effect. \
                                 Tot functions can only call other Tot functions.",
                                block.name().unwrap_or("unknown"),
                                callee_name,
                                callee_eff.display_name()
                            ),
                            fix: None,
                        });
                    }
                }
            }
        }

        diagnostics
    }

    /// Check for Ghost values used in computational (non-ghost) context.
    ///
    /// Ghost values are erased at extraction and cannot be used in
    /// computational code that will be extracted to OCaml.
    ///
    /// IMPORTANT: This check is intentionally conservative to avoid false positives:
    /// - Only flags UNQUALIFIED calls (not Module.name references to other modules)
    /// - Only flags explicit `ghost let` bindings, not GTot-effect functions
    /// - F* itself enforces ghost/computational boundaries at compile time
    ///
    /// The main purpose is to catch obvious mistakes early, not to replicate F*'s checker.
    fn check_ghost_in_computational_context(
        &self,
        file: &PathBuf,
        content: &str,
    ) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();
        let (_, blocks) = parse_fstar_file(content);

        // Track ONLY explicit ghost bindings (from `ghost let` pattern)
        // We intentionally do NOT track GTot-effect functions because:
        // 1. GTot functions can be called from specification positions in inline_for_extraction
        // 2. F* already enforces ghost/computational boundaries
        // 3. Including GTot causes massive false positives (621 in hacl-star, 2762 in everparse)
        let mut ghost_bindings: HashMap<String, usize> = HashMap::new();
        for block in &blocks {
            // Only track explicit `ghost let` bindings, not just any GTot effect
            if is_explicit_ghost_let(block) {
                for name in &block.names {
                    ghost_bindings.insert(name.clone(), block.start_line);
                }
            }
        }

        // If no explicit ghost let bindings, nothing to check
        if ghost_bindings.is_empty() {
            return diagnostics;
        }

        // Check computational functions for ghost value usage
        for block in &blocks {
            // Skip non-function blocks
            if !matches!(
                block.block_type,
                BlockType::Let | BlockType::InlineLet | BlockType::UnfoldLet
            ) {
                continue;
            }

            // Check if this is marked for extraction (computational context)
            let is_computational = is_extraction_binding(block);

            // Skip ghost blocks - they can use ghost values
            if is_explicit_ghost_let(block) {
                continue;
            }

            // If marked for extraction, check for ghost value usage
            // Only check UNQUALIFIED calls - qualified calls (Module.name) refer to other modules
            if is_computational {
                let calls = extract_unqualified_function_calls(block);

                for (callee_name, line_num) in calls {
                    if ghost_bindings.contains_key(&callee_name) {
                        diagnostics.push(Diagnostic {
                            rule: RuleCode::FST011,
                            severity: DiagnosticSeverity::Error,
                            file: file.clone(),
                            range: Range::point(line_num, 1),
                            message: format!(
                                "Ghost binding `{}` used in computational context (inline_for_extraction). \
                                 Ghost values are erased at extraction and cannot be used in extracted code.",
                                callee_name
                            ),
                            fix: None,
                        });
                    }
                }
            }
        }

        diagnostics
    }
}

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

impl Rule for EffectCheckerRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST011
    }

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

        diagnostics.extend(self.check_admit(file, content));
        diagnostics.extend(self.check_magic(file, content));
        diagnostics.extend(self.check_unsafe_coerce(file, content));
        diagnostics.extend(self.check_ml_effect(file, content));
        diagnostics.extend(self.check_assume_val(file, content));
        diagnostics.extend(self.check_assume_expr(file, content));
        diagnostics.extend(self.check_tot_calling_effectful(file, content));
        diagnostics.extend(self.check_ghost_in_computational_context(file, content));

        diagnostics
    }
}

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

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

    // ===========================================
    // Effect enum tests
    // ===========================================

    #[test]
    fn test_effect_from_str() {
        assert_eq!(Effect::from_str("Tot"), Some(Effect::Tot));
        assert_eq!(Effect::from_str("GTot"), Some(Effect::GTot));
        assert_eq!(Effect::from_str("Pure"), Some(Effect::Pure));
        assert_eq!(Effect::from_str("Ghost"), Some(Effect::Ghost));
        assert_eq!(Effect::from_str("Lemma"), Some(Effect::Lemma));
        assert_eq!(Effect::from_str("Div"), Some(Effect::Div));
        assert_eq!(Effect::from_str("Dv"), Some(Effect::Div));
        assert_eq!(Effect::from_str("ST"), Some(Effect::ST));
        assert_eq!(Effect::from_str("Stack"), Some(Effect::ST));
        assert_eq!(Effect::from_str("STATE"), Some(Effect::ST));
        assert_eq!(Effect::from_str("Exn"), Some(Effect::Exn));
        assert_eq!(Effect::from_str("Ex"), Some(Effect::Exn));
        assert_eq!(Effect::from_str("All"), Some(Effect::All));
        assert_eq!(Effect::from_str("ML"), Some(Effect::ML));
        assert_eq!(Effect::from_str("Unknown"), None);
    }

    #[test]
    fn test_effect_ordering() {
        assert!(Effect::Tot < Effect::GTot);
        assert!(Effect::GTot < Effect::Pure);
        assert!(Effect::Pure < Effect::Ghost);
        assert!(Effect::Ghost < Effect::Div);
        assert!(Effect::Div < Effect::All);
        assert!(Effect::All < Effect::ML);
    }

    #[test]
    fn test_effect_can_call_tot() {
        // Tot can only call Tot
        assert!(Effect::Tot.can_call(Effect::Tot));
        assert!(!Effect::Tot.can_call(Effect::GTot));
        assert!(!Effect::Tot.can_call(Effect::Pure));
        assert!(!Effect::Tot.can_call(Effect::Ghost));
        assert!(!Effect::Tot.can_call(Effect::ST));
        assert!(!Effect::Tot.can_call(Effect::ML));
    }

    #[test]
    fn test_effect_can_call_gtot() {
        // GTot can call Tot and GTot
        assert!(Effect::GTot.can_call(Effect::Tot));
        assert!(Effect::GTot.can_call(Effect::GTot));
        assert!(!Effect::GTot.can_call(Effect::Pure));
        assert!(!Effect::GTot.can_call(Effect::Ghost));
        assert!(!Effect::GTot.can_call(Effect::ST));
    }

    #[test]
    fn test_effect_can_call_ghost() {
        // Ghost can call Tot, GTot, Ghost, Lemma
        assert!(Effect::Ghost.can_call(Effect::Tot));
        assert!(Effect::Ghost.can_call(Effect::GTot));
        assert!(Effect::Ghost.can_call(Effect::Ghost));
        assert!(Effect::Ghost.can_call(Effect::Lemma));
        assert!(!Effect::Ghost.can_call(Effect::Pure));
        assert!(!Effect::Ghost.can_call(Effect::ST));
    }

    #[test]
    fn test_effect_can_call_st() {
        // ST can call Tot, Pure, Div, ST
        assert!(Effect::ST.can_call(Effect::Tot));
        assert!(Effect::ST.can_call(Effect::Pure));
        assert!(Effect::ST.can_call(Effect::Div));
        assert!(Effect::ST.can_call(Effect::ST));
        assert!(!Effect::ST.can_call(Effect::Ghost));
        assert!(!Effect::ST.can_call(Effect::Exn));
        assert!(!Effect::ST.can_call(Effect::ML));
    }

    #[test]
    fn test_effect_can_call_ml() {
        // ML can call anything
        assert!(Effect::ML.can_call(Effect::Tot));
        assert!(Effect::ML.can_call(Effect::GTot));
        assert!(Effect::ML.can_call(Effect::Pure));
        assert!(Effect::ML.can_call(Effect::Ghost));
        assert!(Effect::ML.can_call(Effect::ST));
        assert!(Effect::ML.can_call(Effect::Exn));
        assert!(Effect::ML.can_call(Effect::All));
        assert!(Effect::ML.can_call(Effect::ML));
    }

    #[test]
    fn test_effect_is_ghost() {
        assert!(Effect::GTot.is_ghost());
        assert!(Effect::Ghost.is_ghost());
        assert!(Effect::Lemma.is_ghost());
        assert!(!Effect::Tot.is_ghost());
        assert!(!Effect::Pure.is_ghost());
        assert!(!Effect::ST.is_ghost());
        assert!(!Effect::ML.is_ghost());
    }

    // ===========================================
    // Existing tests (admit, magic, etc.)
    // ===========================================

    #[test]
    fn test_admit_detected() {
        let rule = EffectCheckerRule::new();
        let content = "let lemma_foo () : Lemma True = admit()";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("admit()")));
        assert!(diags
            .iter()
            .any(|d| d.severity == DiagnosticSeverity::Warning));
    }

    #[test]
    fn test_admit_in_comment_ignored() {
        let rule = EffectCheckerRule::new();
        let content = "(* TODO: remove admit() later *)";
        let diags = rule.check(&make_path(), content);
        assert!(diags.is_empty());
    }

    #[test]
    fn test_magic_detected() {
        let rule = EffectCheckerRule::new();
        let content = "let bad_value : int = magic()";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("magic()")));
        assert!(diags
            .iter()
            .any(|d| d.severity == DiagnosticSeverity::Error));
    }

    #[test]
    fn test_unsafe_coerce_detected() {
        let rule = EffectCheckerRule::new();
        let content = "let coerced = unsafe_coerce x";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("unsafe_coerce")));
        assert!(diags
            .iter()
            .any(|d| d.severity == DiagnosticSeverity::Error));
    }

    #[test]
    fn test_ml_effect_detected() {
        let rule = EffectCheckerRule::new();
        let content = "val foo : int -> ML int";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("ML effect")));
        assert!(diags.iter().any(|d| d.severity == DiagnosticSeverity::Info));
    }

    #[test]
    fn test_ml_effect_in_extraction_context() {
        let rule = EffectCheckerRule::new();
        let content = "inline_for_extraction let foo : int -> ML int = fun x -> x";
        let diags = rule.check(&make_path(), content);
        // Should not warn about ML in extraction context
        assert!(!diags.iter().any(|d| d.message.contains("ML effect")));
    }

    #[test]
    fn test_assume_val_detected() {
        let rule = EffectCheckerRule::new();
        let content = "assume val external_function : int -> int";
        let diags = rule.check(&make_path(), content);
        assert!(diags.iter().any(|d| d.message.contains("assume val")));
        assert!(diags.iter().any(|d| d.severity == DiagnosticSeverity::Info));
    }

    #[test]
    fn test_clean_code_no_warnings() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

open FStar.All

val add : int -> int -> Tot int
let add x y = x + y

val factorial : nat -> Tot nat
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.is_empty(),
            "Expected no diagnostics, got: {:?}",
            diags
        );
    }

    // ===========================================
    // Effect hierarchy analysis tests
    // ===========================================

    #[test]
    fn test_tot_calling_effectful_detected() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

val effectful_fn : int -> ST int
let effectful_fn x = x + 1

val pure_fn : int -> Tot int
let pure_fn x = effectful_fn x
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags
                .iter()
                .any(|d| d.message.contains("Tot function") && d.message.contains("ST effect")),
            "Expected Tot-calling-effectful diagnostic, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_tot_calling_tot_ok() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

val helper : int -> Tot int
let helper x = x + 1

val main_fn : int -> Tot int
let main_fn x = helper x
"#;
        let diags = rule.check(&make_path(), content);
        // Should only have no Tot-calling-effectful errors
        assert!(
            !diags
                .iter()
                .any(|d| d.message.contains("Tot function") && d.message.contains("effect")),
            "Should not report Tot calling Tot as error"
        );
    }

    #[test]
    fn test_tot_calling_known_effectful() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

val pure_fn : int -> Tot int
let pure_fn x = print_string "hello"; x
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags
                .iter()
                .any(|d| d.message.contains("Tot function") && d.message.contains("print_string")),
            "Expected Tot-calling-ML diagnostic for print_string"
        );
    }

    #[test]
    fn test_ml_can_call_anything() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

val effectful_fn : int -> ST int
let effectful_fn x = x + 1

val ml_fn : int -> ML int
let ml_fn x = effectful_fn x
"#;
        let diags = rule.check(&make_path(), content);
        // ML should be able to call ST without error
        assert!(
            !diags
                .iter()
                .any(|d| d.message.contains("ml_fn") && d.message.contains("effect")),
            "ML should be able to call any effect"
        );
    }

    // ===========================================
    // Ghost in computational context tests
    // ===========================================

    #[test]
    fn test_ghost_in_extraction_context_detected() {
        use super::parse_fstar_file;

        let rule = EffectCheckerRule::new();
        // Use explicit 'ghost let' pattern - this is what the check looks for
        // to avoid false positives from GTot effect functions
        let content = r#"
module Test

ghost let ghost_val = 42

inline_for_extraction let extracted_fn () = ghost_val + 1
"#;
        // Debug: check what blocks are parsed
        let (_, blocks) = parse_fstar_file(content);
        eprintln!("Parsed {} blocks:", blocks.len());
        for block in &blocks {
            eprintln!(
                "  {:?} names={:?} lines={:?}",
                block.block_type,
                block.names,
                block.lines.len()
            );
            eprintln!("    lines: {:?}", block.lines);
            if is_explicit_ghost_let(block) {
                eprintln!("    -> is_explicit_ghost_let=true");
            }
            if is_extraction_binding(block) {
                eprintln!("    -> is_extraction_binding=true");
                let calls = extract_unqualified_function_calls(block);
                eprintln!("    -> unqualified calls: {:?}", calls);
            }
        }

        let diags = rule.check(&make_path(), content);
        eprintln!("Got {} diagnostics:", diags.len());
        for d in &diags {
            eprintln!("  {:?}: {}", d.rule, d.message);
        }

        assert!(
            diags.iter().any(|d| d.message.contains("Ghost binding")
                && d.message.contains("computational context")),
            "Expected ghost-in-computational-context diagnostic, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_ghost_in_ghost_context_ok() {
        let rule = EffectCheckerRule::new();
        // Ghost bindings CAN use other ghost bindings
        let content = r#"
module Test

ghost let ghost_val = 42

ghost let another_ghost = ghost_val + 1
"#;
        let diags = rule.check(&make_path(), content);
        // Ghost can use ghost - no errors about ghost bindings
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "Ghost using ghost should be OK"
        );
    }

    #[test]
    fn test_gtot_function_not_flagged_to_avoid_false_positives() {
        let rule = EffectCheckerRule::new();
        // GTot functions are NOT flagged when called from inline_for_extraction
        // because:
        // 1. GTot functions can be called from specification positions (requires/ensures)
        // 2. F* itself enforces ghost/computational boundaries at compile time
        // 3. The old behavior caused 621+ false positives in hacl-star
        let content = r#"
module Test

val ghost_fn : int -> GTot int
let ghost_fn x = x + 1

inline_for_extraction let extracted_fn (x:int) = ghost_fn x + 1
"#;
        let diags = rule.check(&make_path(), content);
        // Should NOT flag GTot function calls - F* compiler handles this
        assert!(
            !diags
                .iter()
                .any(|d| d.message.contains("Ghost binding")),
            "GTot functions should NOT be flagged (F* handles this), got: {:?}",
            diags
        );
    }

    #[test]
    fn test_qualified_ghost_reference_not_flagged() {
        let rule = EffectCheckerRule::new();
        // Qualified references (Module.name) should NOT be flagged because
        // they refer to other modules, not local ghost bindings
        let content = r#"
module Test

ghost let state = 42

inline_for_extraction let extracted_fn () =
  (* Even if there's a local 'state' ghost, this refers to another module *)
  EverCrypt.Hash.state
"#;
        let diags = rule.check(&make_path(), content);
        // Qualified references should not match local ghost bindings
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding") && d.message.contains("state")),
            "Qualified references should not be flagged, got: {:?}",
            diags
        );
    }

    // ===========================================
    // Effect extraction tests
    // ===========================================

    #[test]
    fn test_extract_function_effect() {
        let block = DeclarationBlock {
            block_type: BlockType::Let,
            names: vec!["foo".to_string()],
            lines: vec!["val foo : int -> Tot int\n".to_string()],
            start_line: 1,
            has_push_options: false,
            has_pop_options: false,
            references: std::collections::HashSet::new(),
        };
        assert_eq!(extract_function_effect(&block), Some(Effect::Tot));
    }

    #[test]
    fn test_extract_function_effect_st() {
        let block = DeclarationBlock {
            block_type: BlockType::Val,
            names: vec!["stateful".to_string()],
            lines: vec!["val stateful : int -> ST int\n".to_string()],
            start_line: 1,
            has_push_options: false,
            has_pop_options: false,
            references: std::collections::HashSet::new(),
        };
        assert_eq!(extract_function_effect(&block), Some(Effect::ST));
    }

    #[test]
    fn test_extract_function_effect_none() {
        let block = DeclarationBlock {
            block_type: BlockType::Let,
            names: vec!["foo".to_string()],
            lines: vec!["let foo x = x + 1\n".to_string()],
            start_line: 1,
            has_push_options: false,
            has_pop_options: false,
            references: std::collections::HashSet::new(),
        };
        assert_eq!(extract_function_effect(&block), None);
    }

    // ===========================================
    // Edge case tests for false positive prevention
    // ===========================================

    #[test]
    fn test_assume_expr_detected() {
        let rule = EffectCheckerRule::new();
        let content = "let x = assume (B.disjoint a b); foo ()";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("assume (...")),
            "Expected assume(expr) diagnostic, got: {:?}",
            diags
        );
        assert!(diags
            .iter()
            .any(|d| d.severity == DiagnosticSeverity::Warning));
    }

    #[test]
    fn test_assume_expr_squash_pattern() {
        let rule = EffectCheckerRule::new();
        let content = "let _ : squash (SZ.fits_u64) = assume (SZ.fits_u64)";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("assume (...")),
            "Should detect assume in squash pattern"
        );
    }

    #[test]
    fn test_admit_in_inline_comment_not_flagged() {
        let rule = EffectCheckerRule::new();
        let content = "let x = y + z // TODO: use admit() here later";
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("admit()")),
            "Should not flag admit() in inline comment"
        );
    }

    #[test]
    fn test_admit_in_block_comment_not_flagged() {
        let rule = EffectCheckerRule::new();
        let content = "let x = y + z (* admit() is bad *)";
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("admit()")),
            "Should not flag admit() in inline block comment"
        );
    }

    #[test]
    fn test_admit_in_string_not_flagged() {
        let rule = EffectCheckerRule::new();
        let content = r#"let msg = "Do not use admit() in production""#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("admit()")),
            "Should not flag admit() in string literal"
        );
    }

    #[test]
    fn test_magic_in_string_not_flagged() {
        let rule = EffectCheckerRule::new();
        let content = r#"let msg = "magic() is dangerous""#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("magic()")),
            "Should not flag magic() in string literal"
        );
    }

    #[test]
    fn test_admit_smt_queries_option_not_flagged() {
        let rule = EffectCheckerRule::new();
        let content = r#"#set-options "--admit_smt_queries true""#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("admit()")),
            "Should not flag --admit_smt_queries option"
        );
    }

    #[test]
    fn test_code_after_block_comment_detected() {
        let rule = EffectCheckerRule::new();
        let content = "(* comment *) let x = admit()";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("admit()")),
            "Should detect admit() after block comment on same line"
        );
    }

    #[test]
    fn test_nested_block_comment_handling() {
        let rule = EffectCheckerRule::new();
        let content = "let x = y (* outer (* inner *) outer *) + admit()";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("admit()")),
            "Should detect admit() with nested comments"
        );
    }

    #[test]
    fn test_assume_val_not_double_reported() {
        let rule = EffectCheckerRule::new();
        let content = "assume val foo : int -> int";
        let diags = rule.check(&make_path(), content);
        let assume_count = diags
            .iter()
            .filter(|d| d.message.contains("assume"))
            .count();
        assert_eq!(
            assume_count, 1,
            "assume val should only be reported once, not by both checks"
        );
    }

    #[test]
    fn test_escaped_string_handling() {
        let rule = EffectCheckerRule::new();
        let content = r#"let msg = "escaped \" quote admit()""#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("admit()")),
            "Should handle escaped quotes in strings"
        );
    }

    #[test]
    fn test_strip_comments_and_strings_helper() {
        assert_eq!(strip_comments_and_strings("let x = 1"), "let x = 1");
        assert_eq!(
            strip_comments_and_strings("let x = 1 // comment"),
            "let x = 1 "
        );
        assert_eq!(
            strip_comments_and_strings("let x = 1 (* comment *)"),
            "let x = 1  "
        );
        assert_eq!(
            strip_comments_and_strings(r#"let x = "string""#),
            "let x = \"\""
        );
        // Nested comments: outer comment replaced with space, then original space before "code"
        assert_eq!(
            strip_comments_and_strings("(* outer (* inner *) outer *) code"),
            "  code"
        );
    }

    #[test]
    fn test_real_world_hacl_pattern() {
        let rule = EffectCheckerRule::new();
        let content = r#"
let nat32_to_le_bytes (n:nat32) : b:seq4 nat8 {
  le_bytes_to_nat32 b == n} =
  let b = four_to_seq_LE (nat_to_four 8 n) in
  assume (le_bytes_to_nat32 b == n);
  b
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("assume (...")),
            "Should detect assume pattern from real hacl-star code"
        );
    }

    #[test]
    fn test_module_qualified_admit_detected() {
        let rule = EffectCheckerRule::new();
        let content = "let x = FStar.Tactics.admit()";
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("admit()")),
            "Should detect module-qualified admit()"
        );
    }

    // ===========================================
    // Effect hierarchy bug fix tests
    // ===========================================

    #[test]
    fn test_exn_can_call_div_bug_fix() {
        // Bug fix: Exn should be able to call Div (divergence is a sub-effect)
        assert!(Effect::Exn.can_call(Effect::Tot));
        assert!(Effect::Exn.can_call(Effect::Pure));
        assert!(Effect::Exn.can_call(Effect::Div), "BUG FIX: Exn should be able to call Div");
        assert!(Effect::Exn.can_call(Effect::Exn));
        assert!(!Effect::Exn.can_call(Effect::ST), "Exn cannot call ST");
        assert!(!Effect::Exn.can_call(Effect::Ghost), "Exn cannot call Ghost");
    }

    #[test]
    fn test_all_effect_comprehensive() {
        // All can call everything except ML
        assert!(Effect::All.can_call(Effect::Tot));
        assert!(Effect::All.can_call(Effect::GTot));
        assert!(Effect::All.can_call(Effect::Pure));
        assert!(Effect::All.can_call(Effect::Ghost));
        assert!(Effect::All.can_call(Effect::Div));
        assert!(Effect::All.can_call(Effect::ST));
        assert!(Effect::All.can_call(Effect::Exn));
        assert!(Effect::All.can_call(Effect::All));
        assert!(!Effect::All.can_call(Effect::ML), "All cannot call ML");
    }

    #[test]
    fn test_ghost_pure_branches_separate() {
        // Ghost and Pure are on separate branches
        assert!(!Effect::Ghost.can_call(Effect::Pure), "Ghost cannot call Pure");
        assert!(!Effect::Pure.can_call(Effect::Ghost), "Pure cannot call Ghost");
        assert!(!Effect::Pure.can_call(Effect::GTot), "Pure cannot call GTot");
    }

    #[test]
    fn test_div_hierarchy() {
        // Div can call Tot, Pure, Div only
        assert!(Effect::Div.can_call(Effect::Tot));
        assert!(Effect::Div.can_call(Effect::Pure));
        assert!(Effect::Div.can_call(Effect::Div));
        assert!(!Effect::Div.can_call(Effect::GTot));
        assert!(!Effect::Div.can_call(Effect::Ghost));
        assert!(!Effect::Div.can_call(Effect::ST));
        assert!(!Effect::Div.can_call(Effect::Exn));
    }

    #[test]
    fn test_st_hierarchy() {
        // ST can call Tot, Pure, Div, ST
        assert!(Effect::ST.can_call(Effect::Tot));
        assert!(Effect::ST.can_call(Effect::Pure));
        assert!(Effect::ST.can_call(Effect::Div));
        assert!(Effect::ST.can_call(Effect::ST));
        assert!(!Effect::ST.can_call(Effect::GTot));
        assert!(!Effect::ST.can_call(Effect::Ghost));
        assert!(!Effect::ST.can_call(Effect::Exn));
        assert!(!Effect::ST.can_call(Effect::ML));
    }

    #[test]
    fn test_qualified_effectful_print_string() {
        let rule = EffectCheckerRule::new();
        let content = r#"
module Test

val pure_fn : int -> Tot int
let pure_fn x = FStar.IO.print_string "hello"; x
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("Tot function") && d.message.contains("print_string")),
            "Qualified FStar.IO.print_string should be detected in Tot context, got: {:?}",
            diags
        );
    }

    // ===========================================
    // Ghost/erased false positive regression tests
    // ===========================================

    #[test]
    fn test_ghost_erased_param_in_val_not_flagged() {
        let rule = EffectCheckerRule::new();
        // Real pattern from hacl-star: Ghost.erased in val parameter type
        // This should NOT cause the function name to be tracked as a ghost binding.
        // The old `erased` keyword matching caused 621 false positives in hacl-star.
        let content = r#"
module Test

val mod_precomp: len:Ghost.erased _ -> BS.bn_mod_slow_ctx_st t_limbs len
let mod_precomp len ctx a res = something len

inline_for_extraction noextract
let use_mod_precomp () = mod_precomp len ctx a res
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "Ghost.erased parameter type must NOT cause ghost binding false positive, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_inline_for_extraction_with_erased_implicit_param_not_flagged() {
        let rule = EffectCheckerRule::new();
        // Real pattern from hacl-star bignum: inline_for_extraction with #t:limb_t
        // The #t parameter is implicit/erased but the function IS extracted.
        let content = r#"
module Test

inline_for_extraction noextract
val bn_sub:
    #t:limb_t
  -> aLen:size_t
  -> a:lbignum t aLen
  -> bLen:size_t
  -> b:lbignum t bLen
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h -> live h a /\ live h b /\ live h res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1)

let bn_sub #t aLen a bLen b res =
  let c0 = bn_sub_eq_len bLen a0 b res0 in
  c0
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "inline_for_extraction with implicit params must NOT be flagged, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_erased_in_inline_let_annotation_not_flagged() {
        let rule = EffectCheckerRule::new();
        // Pattern from hacl-star: [@inline_let] with Ghost.erased in closures
        let content = r#"
module Test

inline_for_extraction noextract
let bn_sub_carry #t aLen a c_in res =
  push_frame ();
  let c = create 1ul c_in in
  [@inline_let]
  let footprint (i:size_nat{i <= v aLen}) : GTot (l:B.loc{B.loc_disjoint l (loc res)}) = loc c in
  [@inline_let]
  let spec h = S.bn_sub_carry_f (as_seq h a) in
  let h0 = ST.get () in
  fill_elems4 h0 aLen res refl footprint spec
  (fun i -> c.(0ul) <- subborrow_st c.(0ul) t1 (uint #t 0) res_i);
  pop_frame ()
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "GTot annotations inside inline_for_extraction must NOT trigger ghost binding warning, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_everparse_ghost_erased_param_not_flagged() {
        let rule = EffectCheckerRule::new();
        // Real pattern from everparse: Ghost.erased parameters in val + inline_for_extraction
        let content = r#"
module Test

val to_field: len:Ghost.erased _ -> MA.bn_to_field_st t_limbs len
val from_field: len:Ghost.erased _ -> MA.bn_from_field_st t_limbs len
val add: len:Ghost.erased _ -> MA.bn_field_add_st t_limbs len

inline_for_extraction noextract
let use_fields (len:Ghost.erased _) =
  let r1 = to_field len in
  let r2 = add len in
  r1
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "Ghost.erased parameters in everparse patterns must NOT be flagged, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_actual_ghost_let_still_detected_in_extraction_context() {
        let rule = EffectCheckerRule::new();
        // Actual ghost let binding SHOULD still be detected
        let content = r#"
module Test

ghost let secret_value = 42

inline_for_extraction let extracted_fn () = secret_value + 1
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            diags.iter().any(|d| d.message.contains("Ghost binding") && d.message.contains("secret_value")),
            "Actual ghost let binding must still be detected in extraction context, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_erased_keyword_in_type_position_not_flagged() {
        let rule = EffectCheckerRule::new();
        // The word "erased" as a type in a record or parameter should not
        // cause the declaration to be treated as a ghost binding
        let content = r#"
module Test

val mk_concrete_ops:
    a_t:inttype
  -> len:size_t
  -> to: Ghost.erased (to_comm_monoid a_t len ctx_len) ->
  concrete_ops a_t len ctx_len

inline_for_extraction noextract
let use_concrete_ops a_t len to =
  mk_concrete_ops a_t len to
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("Ghost binding")),
            "Ghost.erased in type position must NOT trigger ghost binding warning, got: {:?}",
            diags
        );
    }

    #[test]
    fn test_tot_builtins_not_flagged() {
        let rule = EffectCheckerRule::new();
        // normalize_term, fst, snd are Tot - should not be flagged
        let content = r#"
module Test

val pure_fn : (int * int) -> Tot int
let pure_fn p = fst p + snd p
"#;
        let diags = rule.check(&make_path(), content);
        assert!(
            !diags.iter().any(|d| d.message.contains("fst") && d.message.contains("effect")),
            "fst should not be flagged as effectful"
        );
    }
}