brrr-lint 0.1.0

//! FST002: Interface declaration order verification.
//!
//! Port of reorder_fsti.py.
//!
//! Addresses F* Error 233: "Expected the definition of X to precede Y"
//! by detecting when .fsti declarations are not in the same order
//! as the implementation (.fst).
//!
//! CRITICAL FEATURES:
//! 1. Forward Reference Detection: Refuses to reorder if it would create
//!    forward references (type A uses type B, but B would come after A)
//! 2. Mutual Recursion: Types connected by 'and' are treated as atomic groups
//! 3. Dependency Analysis: Builds dependency graph from type/val signatures
//! 4. Module Header Preservation: module, open, friend statements stay at top
//! 5. FSTI-only declarations: Types defined only in .fsti are properly ordered
//! 6. Orphan Declaration Detection: Warns when .fsti declares something not in .fst
//! 7. Typo Detection: Suggests corrections when names are similar but not matching

use std::collections::{HashMap, HashSet};
use std::path::PathBuf;

use lazy_static::lazy_static;
use regex::Regex;

use super::parser::{
    build_dependency_graph, get_definition_order, parse_fstar_file, BlockType, DeclarationBlock,
};

lazy_static! {
    // Token patterns for validation
    static ref VAL_PATTERN: Regex = Regex::new(r"\bval\s+").unwrap();
    static ref TYPE_PATTERN: Regex = Regex::new(r"\btype\s+").unwrap();
    static ref LET_PATTERN: Regex = Regex::new(r"\blet\s+").unwrap();
    static ref MODULE_PATTERN: Regex = Regex::new(r"\bmodule\s+([A-Z][\w.]*)").unwrap();
}
use super::rules::{Diagnostic, DiagnosticSeverity, Edit, Fix, FixConfidence, FixSafetyLevel, Range, Rule, RuleCode};

/// Compute Levenshtein edit distance between two strings.
/// Returns the minimum number of single-character edits (insertions, deletions, substitutions)
/// required to transform one string into the other.
fn levenshtein_distance(a: &str, b: &str) -> usize {
    let a_chars: Vec<char> = a.chars().collect();
    let b_chars: Vec<char> = b.chars().collect();
    let m = a_chars.len();
    let n = b_chars.len();

    if m == 0 {
        return n;
    }
    if n == 0 {
        return m;
    }

    // Use two rows for space efficiency
    let mut prev_row: Vec<usize> = (0..=n).collect();
    let mut curr_row: Vec<usize> = vec![0; n + 1];

    for i in 1..=m {
        curr_row[0] = i;
        for j in 1..=n {
            let cost = if a_chars[i - 1] == b_chars[j - 1] {
                0
            } else {
                1
            };
            curr_row[j] = (prev_row[j] + 1) // deletion
                .min(curr_row[j - 1] + 1) // insertion
                .min(prev_row[j - 1] + cost); // substitution
        }
        std::mem::swap(&mut prev_row, &mut curr_row);
    }

    prev_row[n]
}

/// Find potential typo matches for a name in a set of candidates.
/// Returns the best match if the edit distance is <= threshold.
fn find_typo_match<'a>(
    name: &str,
    candidates: &'a HashSet<String>,
    threshold: usize,
) -> Option<(&'a str, usize)> {
    let mut best_match: Option<(&str, usize)> = None;

    for candidate in candidates {
        if candidate == name {
            continue;
        }
        // Skip if lengths differ too much
        let len_diff = (name.len() as isize - candidate.len() as isize).unsigned_abs();
        if len_diff > threshold {
            continue;
        }

        let dist = levenshtein_distance(name, candidate);
        if dist <= threshold {
            match best_match {
                None => best_match = Some((candidate.as_str(), dist)),
                Some((_, best_dist)) if dist < best_dist => {
                    best_match = Some((candidate.as_str(), dist))
                }
                _ => {}
            }
        }
    }

    best_match
}

/// Result of analyzing interface/implementation consistency.
#[derive(Debug, Default)]
pub struct InterfaceConsistencyResult {
    /// Declarations in .fsti with no corresponding definition in .fst.
    /// Each entry is (name, potential_typo_match, line_number).
    pub orphan_declarations: Vec<(String, Option<String>, usize)>,
    /// Potential typo matches: (fsti_name, fst_name, edit_distance).
    pub typo_matches: Vec<(String, String, usize)>,
}

/// Analyze consistency between .fsti declarations and .fst definitions.
/// Returns orphan declarations and potential typos.
///
/// CRITICAL: Only `val` declarations are checked for orphans. In F*, it is
/// completely normal for .fsti files to contain interface-only definitions:
/// - `let` type aliases (e.g., `let bn_add_eq_len_st (t:limb_t) = ...`)
/// - `type` definitions (abstract or concrete types)
/// - `class` definitions
/// - `effect` definitions
/// - `assume val`/`assume type` declarations
/// - `unfold let` / `inline_for_extraction let` definitions
///
/// These are part of the public API and do NOT need .fst implementations.
/// Only `val` declarations require a corresponding `let` in the .fst file.
pub fn analyze_interface_consistency(
    fsti_content: &str,
    fst_content: &str,
) -> InterfaceConsistencyResult {
    let (_, fsti_blocks) = parse_fstar_file(fsti_content);
    let fst_order = get_definition_order(fst_content);

    // Build set of .fst definition names
    let fst_names_set: HashSet<String> = fst_order.into_iter().collect();

    // Build set of .fsti VAL declaration names with line numbers.
    // Only val declarations need .fst implementations; let/type/class/etc.
    // are interface-only by design in F*.
    let mut fsti_val_names_with_lines: Vec<(String, usize)> = Vec::new();
    for block in &fsti_blocks {
        if block.block_type == BlockType::Val {
            for name in &block.names {
                fsti_val_names_with_lines.push((name.clone(), block.start_line));
            }
        }
    }

    let mut result = InterfaceConsistencyResult::default();

    // Find orphan val declarations and potential typos
    for (fsti_name, line) in &fsti_val_names_with_lines {
        if !fst_names_set.contains(fsti_name) {
            // This val has no corresponding let in .fst
            // Check for typo match in .fst names
            let typo_match = find_typo_match(fsti_name, &fst_names_set, 2);

            if let Some((match_name, dist)) = typo_match {
                result
                    .typo_matches
                    .push((fsti_name.clone(), match_name.to_string(), dist));
                result.orphan_declarations.push((
                    fsti_name.clone(),
                    Some(match_name.to_string()),
                    *line,
                ));
            } else {
                result
                    .orphan_declarations
                    .push((fsti_name.clone(), None, *line));
            }
        }
    }

    result
}

/// FST002: Interface declaration order.
pub struct ReorderInterfaceRule;

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

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

/// Check if a given order satisfies all dependencies (no forward references).
///
/// CRITICAL: Also checks for dependencies that are NOT in the order list at all.
/// This catches the bug where FSTI-only declarations would be placed at the END,
/// after declarations that depend on them.
fn check_order_valid(
    order: &[String],
    deps: &HashMap<String, HashSet<String>>,
    all_declared_names: Option<&HashSet<String>>,
) -> (bool, Vec<String>) {
    let mut violations = Vec::new();
    let name_to_position: HashMap<&str, usize> = order
        .iter()
        .enumerate()
        .map(|(i, name)| (name.as_str(), i))
        .collect();
    let order_set: HashSet<&str> = order.iter().map(|s| s.as_str()).collect();

    for name in order {
        if let Some(name_deps) = deps.get(name) {
            let name_pos = name_to_position[name.as_str()];
            for dep in name_deps {
                // Check if dependency is a valid declared name
                let is_valid_dep = all_declared_names
                    .map(|names| names.contains(dep))
                    .unwrap_or(true);

                if !is_valid_dep {
                    continue;
                }

                if !order_set.contains(dep.as_str()) {
                    // CRITICAL: Dependency is NOT in the order list at all!
                    violations.push(format!(
                        "'{}' references '{}', but '{}' is not in order \
                         (FSTI-only declaration that would be placed at END)",
                        name, dep, dep
                    ));
                } else if let Some(&dep_pos) = name_to_position.get(dep.as_str()) {
                    if dep_pos > name_pos {
                        violations.push(format!(
                            "'{}' references '{}', but '{}' comes after '{}'",
                            name, dep, dep, name
                        ));
                    }
                }
            }
        }
    }

    (violations.is_empty(), violations)
}

/// Topological sort with preference-based selection.
/// Tries to follow preferred_order while respecting dependencies.
fn topological_sort_with_preference(
    names: &[String],
    deps: &HashMap<String, HashSet<String>>,
    preferred_order: &[String],
) -> Result<Vec<String>, Vec<String>> {
    let name_set: HashSet<&str> = names.iter().map(|s| s.as_str()).collect();

    // Filter dependencies to only include names we're sorting
    let mut filtered_deps: HashMap<&str, HashSet<&str>> = HashMap::new();
    for name in names {
        let mut local_deps = HashSet::new();
        if let Some(name_deps) = deps.get(name) {
            for dep in name_deps {
                if name_set.contains(dep.as_str()) {
                    local_deps.insert(dep.as_str());
                }
            }
        }
        filtered_deps.insert(name.as_str(), local_deps);
    }

    // Kahn's algorithm with preference-based selection
    let mut in_degree: HashMap<&str, usize> = names.iter().map(|n| (n.as_str(), 0)).collect();

    // Calculate in-degrees: for each dependency, increment the in-degree of the dependent
    for name in names {
        for dep in filtered_deps.get(name.as_str()).unwrap_or(&HashSet::new()) {
            if let Some(degree) = in_degree.get_mut(name.as_str()) {
                *degree += 1;
            }
        }
    }

    // Build preferred position map
    let preferred_position: HashMap<&str, usize> = preferred_order
        .iter()
        .enumerate()
        .map(|(i, name)| (name.as_str(), i))
        .collect();

    let get_priority = |name: &str| -> usize {
        preferred_position
            .get(name)
            .copied()
            .unwrap_or(preferred_order.len())
    };

    // Queue: names with no dependencies (in-degree 0)
    let mut available: Vec<&str> = names
        .iter()
        .filter(|n| in_degree.get(n.as_str()) == Some(&0))
        .map(|s| s.as_str())
        .collect();
    available.sort_by_key(|n| get_priority(n));

    let mut result = Vec::new();

    while let Some(current) = available.first().cloned() {
        available.remove(0);
        result.push(current.to_string());

        // "Remove" current: decrease in-degree of dependents
        for name in names {
            if filtered_deps
                .get(name.as_str())
                .map(|d| d.contains(current))
                .unwrap_or(false)
            {
                if let Some(degree) = in_degree.get_mut(name.as_str()) {
                    *degree = degree.saturating_sub(1);
                    if *degree == 0 && !result.contains(&name.to_string()) {
                        available.push(name.as_str());
                        available.sort_by_key(|n| get_priority(n));
                    }
                }
            }
        }
    }

    if result.len() != names.len() {
        // Cycle detected
        let remaining: Vec<&str> = names
            .iter()
            .filter(|n| !result.contains(&n.to_string()))
            .map(|s| s.as_str())
            .collect();
        return Err(vec![format!(
            "Cycle detected involving: {}",
            remaining.join(", ")
        )]);
    }

    Ok(result)
}

/// Reorder .fsti content to fix forward reference errors.
///
/// IMPORTANT: This rule only suggests reordering when the CURRENT .fsti order
/// has forward reference problems (would cause F* Error 233). It does NOT
/// suggest changes just because the order differs from the .fst file.
///
/// Rationale: The .fsti is the PUBLIC INTERFACE and may intentionally have
/// a different organization (e.g., type aliases at the top for readability).
/// The .fst implementation order should not dictate interface organization.
pub fn reorder_fsti_content(
    fsti_content: &str,
    _fst_content: &str,
) -> Result<(String, Vec<(String, usize, usize)>, bool), Vec<String>> {
    // Parse .fsti file (we no longer need .fst order - see docstring above)
    let (fsti_header, fsti_blocks) = parse_fstar_file(fsti_content);

    // Build dependency graph for .fsti
    let deps = build_dependency_graph(&fsti_blocks);

    // Map blocks by their primary name
    let mut block_by_name: HashMap<&str, &DeclarationBlock> = HashMap::new();
    for block in &fsti_blocks {
        for name in &block.names {
            if !block_by_name.contains_key(name.as_str()) {
                block_by_name.insert(name.as_str(), block);
            }
        }
    }

    // Get set of .fsti declaration names
    let mut fsti_names_set: HashSet<String> = HashSet::new();
    for block in &fsti_blocks {
        fsti_names_set.extend(block.names.iter().cloned());
    }

    // Get the CURRENT .fsti order (preserving original order)
    let current_fsti_order: Vec<String> = fsti_blocks
        .iter()
        .flat_map(|b| b.names.iter().cloned())
        .collect();

    // CRITICAL FIX: First check if the CURRENT .fsti order is valid
    // If there are no forward references in the current order, we should NOT
    // suggest any changes - the .fsti organization is intentional and valid.
    let (current_is_valid, current_violations) =
        check_order_valid(&current_fsti_order, &deps, Some(&fsti_names_set));

    if current_is_valid {
        // Current .fsti order has no forward references - it's valid!
        // Don't suggest reordering just because it differs from .fst
        return Ok((fsti_content.to_string(), Vec::new(), false));
    }

    // Current order has forward references - we need to fix it
    // Use topological sort with .fsti's current order as preference (to minimize changes)
    let fsti_all_names: Vec<String> = fsti_names_set.iter().cloned().collect();
    let relevant_order = match topological_sort_with_preference(
        &fsti_all_names,
        &deps,
        &current_fsti_order, // Use current .fsti order as preference, not .fst order
    ) {
        Ok(sorted) => sorted,
        Err(_) => return Err(current_violations),
    };

    // Track original positions
    let mut original_positions: HashMap<&str, usize> = HashMap::new();
    for (idx, block) in fsti_blocks.iter().enumerate() {
        for name in &block.names {
            if !original_positions.contains_key(name.as_str()) {
                original_positions.insert(name.as_str(), idx);
            }
        }
    }

    // Build reordered block list
    let mut reordered_blocks: Vec<&DeclarationBlock> = Vec::new();
    let mut used_block_indices: HashSet<usize> = HashSet::new();
    let mut movements: Vec<(String, usize, usize)> = Vec::new();

    // First pass: add blocks in computed order
    let mut new_position = 0;
    for name in &relevant_order {
        if let Some(&block) = block_by_name.get(name.as_str()) {
            let block_idx = fsti_blocks
                .iter()
                .position(|b| std::ptr::eq(b, block))
                .unwrap_or(0);
            if !used_block_indices.contains(&block_idx) {
                reordered_blocks.push(block);
                used_block_indices.insert(block_idx);

                // Record movement for primary name
                let primary = block
                    .names
                    .first()
                    .map(|s| s.as_str())
                    .unwrap_or(name.as_str());
                let old_pos = original_positions.get(primary).copied().unwrap_or(0);
                if old_pos != new_position {
                    movements.push((primary.to_string(), old_pos, new_position));
                }
                new_position += 1;
            }
        }
    }

    // Second pass: add remaining blocks not in order
    for (idx, block) in fsti_blocks.iter().enumerate() {
        if !used_block_indices.contains(&idx) {
            reordered_blocks.push(block);
            used_block_indices.insert(idx);

            if let Some(primary) = block.names.first() {
                let old_pos = original_positions
                    .get(primary.as_str())
                    .copied()
                    .unwrap_or(0);
                movements.push((primary.clone(), old_pos, new_position));
            }
            new_position += 1;
        }
    }

    // Construct reordered content
    let mut reordered_lines: Vec<String> = fsti_header.clone();

    // Ensure separation between header and first block
    if !reordered_lines.is_empty() && !reordered_blocks.is_empty() {
        if let Some(last) = reordered_lines.last() {
            if !last.trim().is_empty() {
                reordered_lines.push("\n".to_string());
            }
        }
    }

    for block in &reordered_blocks {
        reordered_lines.extend(block.lines.iter().cloned());
    }

    // Check if order actually changed
    let original_order: Vec<&str> = fsti_blocks
        .iter()
        .flat_map(|b| b.names.iter().map(|s| s.as_str()))
        .collect();
    let new_order: Vec<&str> = reordered_blocks
        .iter()
        .flat_map(|b| b.names.iter().map(|s| s.as_str()))
        .collect();

    let changed = original_order != new_order;

    Ok((reordered_lines.concat(), movements, changed))
}

impl Rule for ReorderInterfaceRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST002
    }

    fn check(&self, _file: &PathBuf, _content: &str) -> Vec<Diagnostic> {
        // This rule requires pair checking
        vec![]
    }

    fn requires_pair(&self) -> bool {
        true
    }

    fn check_pair(
        &self,
        _fst_file: &PathBuf,
        fst_content: &str,
        fsti_file: &PathBuf,
        fsti_content: &str,
    ) -> Vec<Diagnostic> {
        let mut diagnostics = Vec::new();

        // First, check for orphan declarations and typos
        let consistency = analyze_interface_consistency(fsti_content, fst_content);

        // Report potential typos (highest priority - likely bugs)
        for (fsti_name, fst_name, distance) in &consistency.typo_matches {
            let message = format!(
                "Possible typo: `{}` declared in interface but `{}` defined in implementation \
                 (edit distance: {}). Did you mean `{}`?",
                fsti_name, fst_name, distance, fst_name
            );
            // Find line number for this declaration
            let line = consistency
                .orphan_declarations
                .iter()
                .find(|(n, _, _)| n == fsti_name)
                .map(|(_, _, l)| *l)
                .unwrap_or(1);

            diagnostics.push(Diagnostic {
                rule: RuleCode::FST002,
                severity: DiagnosticSeverity::Warning,
                file: fsti_file.clone(),
                range: Range::point(line, 1),
                message,
                fix: None,
            });
        }

        // Report orphan declarations (without typo matches)
        for (name, typo_match, line) in &consistency.orphan_declarations {
            if typo_match.is_none() {
                let message = format!(
                    "Orphan declaration: `{}` is declared in interface but has no \
                     implementation in .fst. Is this intentional (assume val/type) \
                     or is the implementation missing?",
                    name
                );
                diagnostics.push(Diagnostic {
                    rule: RuleCode::FST002,
                    severity: DiagnosticSeverity::Warning,
                    file: fsti_file.clone(),
                    range: Range::point(*line, 1),
                    message,
                    fix: None,
                });
            }
        }

        // Then check for ordering issues (forward references)
        match reorder_fsti_content(fsti_content, fst_content) {
            Ok((reordered_content, movements, changed)) => {
                if !changed {
                    return diagnostics;
                }

                // CRITICAL SAFETY CHECK: Validate the reordering before offering a fix
                let fsti_path = fsti_file.to_string_lossy();
                let validation_warnings =
                    validate_reorder(fsti_content, &reordered_content, &fsti_path);

                // Check for critical warnings - if any, DO NOT offer a fix
                let critical_warnings: Vec<_> = validation_warnings
                    .iter()
                    .filter(|w| w.severity == ReorderWarningSeverity::Critical)
                    .collect();

                if !critical_warnings.is_empty() {
                    // Report the issue but WITHOUT a fix - it's too dangerous
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST002,
                        severity: DiagnosticSeverity::Error,
                        file: fsti_file.clone(),
                        range: Range::point(1, 1),
                        message: format!(
                            "Interface has forward reference issues, but AUTOFIX IS BLOCKED due to {} critical validation error(s). \
                             Manual intervention required.",
                            critical_warnings.len()
                        ),
                        fix: None, // NO FIX - validation failed
                    });

                    // Report each critical validation error
                    for warning in critical_warnings {
                        diagnostics.push(Diagnostic {
                            rule: RuleCode::FST002,
                            severity: DiagnosticSeverity::Error,
                            file: fsti_file.clone(),
                            range: Range::point(1, 1),
                            message: format!("Validation failed: {}", warning.message),
                            fix: None,
                        });
                    }

                    return diagnostics;
                }

                // Create main diagnostic with fix (validation passed)
                let message = format!(
                    "Interface has forward reference issues. {} declaration{} need{} reordering to fix F* Error 233.",
                    movements.len(),
                    if movements.len() == 1 { "" } else { "s" },
                    if movements.len() == 1 { "s" } else { "" }
                );

                let fsti_lines: Vec<&str> = fsti_content.lines().collect();

                // Determine confidence and safety based on validation results and movement count
                // - If many declarations move (>5), use Medium confidence
                // - If few declarations move and no validation warnings, use High confidence
                let has_validation_warnings = !validation_warnings.is_empty();
                let (confidence, is_safe, unsafe_reason) = if movements.len() > 10 {
                    (
                        FixConfidence::Low,
                        false,
                        Some(format!(
                            "Many declarations ({}) will be reordered. Manual review strongly recommended.",
                            movements.len()
                        )),
                    )
                } else if movements.len() > 5 || has_validation_warnings {
                    (
                        FixConfidence::Medium,
                        false,
                        Some(format!(
                            "Moderate reordering ({} declarations). Please review before applying.",
                            movements.len()
                        )),
                    )
                } else {
                    // Small number of movements, no warnings - relatively safe
                    (FixConfidence::High, true, None)
                };

                let fix = Fix {
                    message: "Reorder declarations to fix forward references".to_string(),
                    edits: vec![Edit {
                        file: fsti_file.clone(),
                        range: Range::new(1, 1, fsti_lines.len() + 1, 1),
                        new_text: reordered_content,
                    }],
                    confidence,
                    is_safe,
                    unsafe_reason,
                    // Reordering is not safe to auto-apply without review
                    safety_level: FixSafetyLevel::Caution,
                    reversible: true,  // Can be undone with inverse reordering
                    requires_review: true,  // Order changes need human review
                };

                let first_line = movements.first().map(|(_, old, _)| *old + 1).unwrap_or(1);

                diagnostics.push(Diagnostic {
                    rule: RuleCode::FST002,
                    severity: DiagnosticSeverity::Error,
                    file: fsti_file.clone(),
                    range: Range::point(first_line, 1),
                    message,
                    fix: Some(fix),
                });

                // Add warning if many declarations are moving
                if movements.len() > 10 {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST002,
                        severity: DiagnosticSeverity::Warning,
                        file: fsti_file.clone(),
                        range: Range::point(1, 1),
                        message: format!(
                            "WARNING: {} declarations will move. Review the changes carefully before applying.",
                            movements.len()
                        ),
                        fix: None,
                    });
                }

                // Add detail diagnostics for each movement
                for (name, old_pos, new_pos) in &movements {
                    let direction = if new_pos > old_pos { "down" } else { "up" };
                    let detail_message = format!(
                        "`{}` needs to move {} (position {} -> {})",
                        name, direction, old_pos, new_pos
                    );
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST002,
                        severity: DiagnosticSeverity::Info,
                        file: fsti_file.clone(),
                        range: Range::point(old_pos + 1, 1),
                        message: detail_message,
                        fix: None,
                    });
                }

                // Add any non-critical validation warnings as info
                for warning in validation_warnings
                    .iter()
                    .filter(|w| w.severity != ReorderWarningSeverity::Critical)
                {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST002,
                        severity: DiagnosticSeverity::Info,
                        file: fsti_file.clone(),
                        range: Range::point(1, 1),
                        message: format!("Validation note: {}", warning.message),
                        fix: None,
                    });
                }

                diagnostics
            }
            Err(errors) => {
                // Report errors
                for err in errors {
                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST002,
                        severity: DiagnosticSeverity::Error,
                        file: fsti_file.clone(),
                        range: Range::point(1, 1),
                        message: format!("Cannot reorder: {}", err),
                        fix: None,
                    });
                }
                diagnostics
            }
        }
    }
}

/// Validation warning from reordering.
#[derive(Debug, Clone)]
pub struct ReorderValidationWarning {
    pub message: String,
    pub severity: ReorderWarningSeverity,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ReorderWarningSeverity {
    Critical,
    Warning,
    Info,
}

/// Compute a content hash of all non-whitespace characters.
/// This is used to verify that reordering didn't lose or duplicate content.
fn compute_content_hash(content: &str) -> u64 {
    use std::collections::hash_map::DefaultHasher;
    use std::hash::{Hash, Hasher};

    let mut hasher = DefaultHasher::new();

    // Hash all non-whitespace characters in sequence
    let non_ws: String = content.chars().filter(|c| !c.is_whitespace()).collect();
    non_ws.hash(&mut hasher);
    hasher.finish()
}

/// Extract all declaration names from content for verification.
fn extract_all_declaration_names(content: &str) -> Vec<String> {
    let (_, blocks) = parse_fstar_file(content);
    let mut names = Vec::new();
    for block in &blocks {
        names.extend(block.names.iter().cloned());
    }
    names
}

/// Count occurrences of each declaration name.
fn count_declaration_names(names: &[String]) -> HashMap<String, usize> {
    let mut counts = HashMap::new();
    for name in names {
        *counts.entry(name.clone()).or_insert(0) += 1;
    }
    counts
}

/// Validate that reordering didn't lose or duplicate content.
///
/// CRITICAL SAFETY CHECKS:
/// 1. Content hash verification - non-whitespace content must be preserved
/// 2. Declaration name verification - every name must appear exactly once
/// 3. Line count sanity check - shouldn't change dramatically
/// 4. Module declaration preservation - must not be lost
/// 5. Token counts - val, type, let counts must match
/// 6. Character-level verification - all non-whitespace chars preserved
///
/// This is a safety net to catch reordering bugs before corrupting files.
pub fn validate_reorder(
    original_content: &str,
    reordered_content: &str,
    _fsti_path: &str,
) -> Vec<ReorderValidationWarning> {
    let mut warnings = Vec::new();

    // ========================================================================
    // CHECK 1: NON-WHITESPACE CHARACTER COUNT VERIFICATION
    // The total count of non-whitespace characters must match.
    // If it doesn't, content was lost or duplicated.
    // ========================================================================
    let orig_non_ws: String = original_content
        .chars()
        .filter(|c| !c.is_whitespace())
        .collect();
    let new_non_ws: String = reordered_content
        .chars()
        .filter(|c| !c.is_whitespace())
        .collect();

    if orig_non_ws.len() != new_non_ws.len() {
        warnings.push(ReorderValidationWarning {
            message: format!(
                "CRITICAL: Non-whitespace character count mismatch: {} -> {} (delta: {}). \
                 Content was lost or duplicated during reordering. FIX REFUSED.",
                orig_non_ws.len(),
                new_non_ws.len(),
                new_non_ws.len() as i64 - orig_non_ws.len() as i64
            ),
            severity: ReorderWarningSeverity::Critical,
        });
    }

    // ========================================================================
    // CHECK 2: DECLARATION NAME VERIFICATION (CRITICAL)
    // Every declaration name must appear exactly once in both versions.
    // This catches:
    // - Lost declarations (name disappeared)
    // - Duplicated declarations (name appears twice)
    // - Name corruption (name changed)
    // ========================================================================
    let orig_names = extract_all_declaration_names(original_content);
    let new_names = extract_all_declaration_names(reordered_content);

    let orig_counts = count_declaration_names(&orig_names);
    let new_counts = count_declaration_names(&new_names);

    // Check for lost declarations
    for (name, &orig_count) in &orig_counts {
        let new_count = new_counts.get(name).copied().unwrap_or(0);
        if new_count == 0 {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "CRITICAL: Declaration '{}' was LOST during reordering! \
                     Original had {} occurrence(s), reordered has none. FIX REFUSED.",
                    name, orig_count
                ),
                severity: ReorderWarningSeverity::Critical,
            });
        } else if new_count != orig_count {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "CRITICAL: Declaration '{}' count changed: {} -> {}. \
                     Possible duplication or loss. FIX REFUSED.",
                    name, orig_count, new_count
                ),
                severity: ReorderWarningSeverity::Critical,
            });
        }
    }

    // Check for new declarations that shouldn't exist
    for (name, &new_count) in &new_counts {
        if !orig_counts.contains_key(name) {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "CRITICAL: Declaration '{}' appeared {} time(s) in reordered content \
                     but was NOT in original! Possible content corruption. FIX REFUSED.",
                    name, new_count
                ),
                severity: ReorderWarningSeverity::Critical,
            });
        }
    }

    // ========================================================================
    // CHECK 3: LINE COUNT SANITY CHECK
    // Reordering shouldn't dramatically change line count.
    // Small changes (blank lines) are OK, large changes indicate problems.
    // ========================================================================
    let orig_lines: Vec<&str> = original_content.lines().collect();
    let new_lines: Vec<&str> = reordered_content.lines().collect();

    let orig_count = orig_lines.len();
    let new_count = new_lines.len();

    let line_delta = (new_count as i64 - orig_count as i64).abs();
    if line_delta > 10 {
        warnings.push(ReorderValidationWarning {
            message: format!(
                "Line count changed significantly: {} -> {} (delta: {}). \
                 This may indicate content was lost or duplicated.",
                orig_count, new_count, line_delta
            ),
            severity: ReorderWarningSeverity::Warning,
        });
    }

    // ========================================================================
    // CHECK 4: MODULE DECLARATION PRESERVATION (CRITICAL)
    // The module declaration MUST be preserved exactly.
    // ========================================================================
    let orig_module = MODULE_PATTERN
        .captures(original_content)
        .and_then(|c| c.get(1).map(|m| m.as_str()));
    let new_module = MODULE_PATTERN
        .captures(reordered_content)
        .and_then(|c| c.get(1).map(|m| m.as_str()));

    match (orig_module, new_module) {
        (Some(orig), None) => {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "CRITICAL: Module declaration '{}' was LOST! FIX REFUSED.",
                    orig
                ),
                severity: ReorderWarningSeverity::Critical,
            });
        }
        (Some(orig), Some(new)) if orig != new => {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "CRITICAL: Module name changed from '{}' to '{}'! FIX REFUSED.",
                    orig, new
                ),
                severity: ReorderWarningSeverity::Critical,
            });
        }
        _ => {}
    }

    // ========================================================================
    // CHECK 5: TOKEN COUNTS VERIFICATION
    // The count of val, type, let keywords should match.
    // This is a secondary check to catch edge cases.
    // ========================================================================
    let token_checks = [
        (&*VAL_PATTERN, "val"),
        (&*TYPE_PATTERN, "type"),
        (&*LET_PATTERN, "let"),
    ];

    for (pattern, name) in token_checks {
        let orig_matches = pattern.find_iter(original_content).count();
        let new_matches = pattern.find_iter(reordered_content).count();

        if orig_matches != new_matches {
            warnings.push(ReorderValidationWarning {
                message: format!(
                    "{} keyword count changed: {} -> {} (delta: {})",
                    name,
                    orig_matches,
                    new_matches,
                    new_matches as i64 - orig_matches as i64
                ),
                severity: ReorderWarningSeverity::Warning,
            });
        }
    }

    // ========================================================================
    // CHECK 6: CHARACTER-BY-CHARACTER VERIFICATION
    // Sort all non-whitespace characters and compare.
    // If the sorted sequences differ, content was changed.
    // ========================================================================
    let mut orig_chars: Vec<char> = original_content
        .chars()
        .filter(|c| !c.is_whitespace())
        .collect();
    let mut new_chars: Vec<char> = reordered_content
        .chars()
        .filter(|c| !c.is_whitespace())
        .collect();

    orig_chars.sort();
    new_chars.sort();

    if orig_chars != new_chars {
        // Find the first differing position for diagnostics
        let diff_pos = orig_chars
            .iter()
            .zip(new_chars.iter())
            .position(|(a, b)| a != b);

        warnings.push(ReorderValidationWarning {
            message: format!(
                "CRITICAL: Character-level content mismatch! \
                 First difference at sorted position {:?}. \
                 Original has {} non-ws chars, reordered has {}. FIX REFUSED.",
                diff_pos,
                orig_chars.len(),
                new_chars.len()
            ),
            severity: ReorderWarningSeverity::Critical,
        });
    }

    warnings
}

/// Pre-flight validation for reordering.
/// Returns Ok(()) if safe to proceed, Err with reasons if not.
pub fn preflight_reorder_check(
    original_content: &str,
) -> Result<PreflightReport, Vec<String>> {
    let (header, blocks) = parse_fstar_file(original_content);

    let mut errors = Vec::new();
    let mut report = PreflightReport {
        total_declarations: 0,
        declaration_names: Vec::new(),
        has_module_declaration: false,
        header_lines: header.len(),
        block_count: blocks.len(),
    };

    // Check 1: Must have a module declaration
    let has_module = header.iter().any(|line| line.trim().starts_with("module "));
    report.has_module_declaration = has_module;
    if !has_module {
        errors.push("No module declaration found in header".to_string());
    }

    // Check 2: Extract all declaration names
    let mut all_names = Vec::new();
    for block in &blocks {
        all_names.extend(block.names.iter().cloned());
    }
    report.declaration_names = all_names.clone();
    report.total_declarations = all_names.len();

    // Check 3: Verify no duplicate declaration names (within a block is OK for mutual recursion)
    let mut seen_in_blocks: HashMap<String, usize> = HashMap::new();
    for (block_idx, block) in blocks.iter().enumerate() {
        for name in &block.names {
            if let Some(prev_block) = seen_in_blocks.get(name) {
                if *prev_block != block_idx {
                    errors.push(format!(
                        "Declaration '{}' appears in multiple blocks (blocks {} and {})",
                        name, prev_block, block_idx
                    ));
                }
            } else {
                seen_in_blocks.insert(name.clone(), block_idx);
            }
        }
    }

    // Check 4: Verify parser didn't produce suspicious results
    let parse_errors = super::parser::validate_parsing(&blocks);
    for err in parse_errors {
        if err.severity == super::parser::ParseErrorSeverity::Error {
            errors.push(format!("Parse error at line {}: {}", err.line, err.message));
        }
    }

    if errors.is_empty() {
        Ok(report)
    } else {
        Err(errors)
    }
}

/// Pre-flight report with information about the file.
#[derive(Debug, Clone)]
pub struct PreflightReport {
    pub total_declarations: usize,
    pub declaration_names: Vec<String>,
    pub has_module_declaration: bool,
    pub header_lines: usize,
    pub block_count: usize,
}

/// Dry-run result showing what would change.
#[derive(Debug, Clone)]
pub struct DryRunResult {
    /// Declarations that would move, with their old and new positions.
    pub movements: Vec<MovementInfo>,
    /// Total number of declarations.
    pub total_declarations: usize,
    /// Whether any changes would be made.
    pub has_changes: bool,
    /// Warning level based on how many declarations move.
    pub warning_level: DryRunWarningLevel,
    /// Validation warnings from comparing original and reordered.
    pub validation_warnings: Vec<ReorderValidationWarning>,
}

/// Information about a single declaration movement.
#[derive(Debug, Clone)]
pub struct MovementInfo {
    pub name: String,
    pub old_position: usize,
    pub new_position: usize,
    pub direction: MovementDirection,
    /// How many positions the declaration moves.
    pub distance: usize,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum MovementDirection {
    Up,
    Down,
    NoChange,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DryRunWarningLevel {
    /// No changes needed.
    None,
    /// Minor changes (1-3 declarations move).
    Low,
    /// Moderate changes (4-10 declarations move).
    Medium,
    /// Many changes (>10 declarations move) - review carefully!
    High,
}

/// Perform a dry-run of reordering to see what would change.
pub fn dry_run_reorder(
    fsti_content: &str,
    fst_content: &str,
) -> Result<DryRunResult, Vec<String>> {
    // First, do pre-flight check
    let preflight = preflight_reorder_check(fsti_content)?;

    // Attempt reordering
    match reorder_fsti_content(fsti_content, fst_content) {
        Ok((reordered_content, movements_raw, changed)) => {
            // Validate the reordering
            let validation_warnings =
                validate_reorder(fsti_content, &reordered_content, "dry-run");

            // Check for critical warnings - if any, this is an error
            let critical_count = validation_warnings
                .iter()
                .filter(|w| w.severity == ReorderWarningSeverity::Critical)
                .count();

            if critical_count > 0 {
                let error_msgs: Vec<String> = validation_warnings
                    .iter()
                    .filter(|w| w.severity == ReorderWarningSeverity::Critical)
                    .map(|w| w.message.clone())
                    .collect();
                return Err(error_msgs);
            }

            // Convert raw movements to detailed movement info
            let movements: Vec<MovementInfo> = movements_raw
                .iter()
                .map(|(name, old_pos, new_pos)| {
                    let direction = if new_pos > old_pos {
                        MovementDirection::Down
                    } else if new_pos < old_pos {
                        MovementDirection::Up
                    } else {
                        MovementDirection::NoChange
                    };
                    let distance = (*new_pos as i64 - *old_pos as i64).unsigned_abs() as usize;
                    MovementInfo {
                        name: name.clone(),
                        old_position: *old_pos,
                        new_position: *new_pos,
                        direction,
                        distance,
                    }
                })
                .collect();

            // Determine warning level
            let moving_count = movements
                .iter()
                .filter(|m| m.direction != MovementDirection::NoChange)
                .count();

            let warning_level = if !changed || moving_count == 0 {
                DryRunWarningLevel::None
            } else if moving_count <= 3 {
                DryRunWarningLevel::Low
            } else if moving_count <= 10 {
                DryRunWarningLevel::Medium
            } else {
                DryRunWarningLevel::High
            };

            Ok(DryRunResult {
                movements,
                total_declarations: preflight.total_declarations,
                has_changes: changed,
                warning_level,
                validation_warnings,
            })
        }
        Err(errors) => Err(errors),
    }
}

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

    #[test]
    fn test_validate_reorder_no_changes() {
        let content = r#"module Test

val foo: int -> int
val bar: int -> int
"#;
        let warnings = validate_reorder(content, content, "Test.fsti");
        assert!(warnings.is_empty());
    }

    #[test]
    fn test_validate_reorder_lost_module_legacy() {
        // Legacy test - lost module should trigger critical warning
        let original = r#"module Test

val foo: int -> int
"#;
        let reordered = r#"
val foo: int -> int
"#;
        let warnings = validate_reorder(original, reordered, "Test.fsti");
        // Either the module check or character count mismatch should trigger
        let has_critical = warnings
            .iter()
            .any(|w| w.severity == ReorderWarningSeverity::Critical);
        assert!(
            has_critical,
            "Lost module should trigger critical warning. Got: {:?}",
            warnings
        );
    }

    #[test]
    fn test_validate_reorder_lost_declaration_legacy() {
        // Legacy test - lost declaration should trigger critical warning
        let original = r#"module Test

val foo: int -> int
val bar: int -> int
"#;
        let reordered = r#"module Test

val foo: int -> int
"#;
        let warnings = validate_reorder(original, reordered, "Test.fsti");
        // The new validation checks declaration names and character counts
        let has_critical = warnings
            .iter()
            .any(|w| w.severity == ReorderWarningSeverity::Critical);
        assert!(
            has_critical,
            "Lost declaration should trigger critical warning. Got: {:?}",
            warnings
        );
    }

    #[test]
    fn test_correct_order_no_change() {
        let fst_content = r#"
module Test

let foo x = x + 1
let bar x = foo x
"#;
        let fsti_content = r#"
module Test

val foo: int -> int
val bar: int -> int
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (_, _, changed) = result.unwrap();
        assert!(!changed);
    }

    #[test]
    fn test_different_order_no_forward_ref_is_valid() {
        // NEW BEHAVIOR: Different order without forward references is VALID
        // The .fsti organization is intentional and doesn't need to match .fst
        let fst_content = r#"
module Test

let foo x = x + 1
let bar x = foo x
"#;
        // bar comes before foo (different from .fst) but NO forward reference
        // bar doesn't USE foo, so this order is valid
        let fsti_content = r#"
module Test

val bar: int -> int
val foo: int -> int
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (_, movements, changed) = result.unwrap();
        // Should NOT change - no forward references in .fsti
        assert!(!changed, "Expected no change when there are no forward references");
        assert!(movements.is_empty());
    }

    #[test]
    fn test_fsti_only_types_at_top_is_valid() {
        // Type aliases at top of .fsti (not in .fst) is a valid pattern
        let fst_content = r#"
module Test

let foo x = x + 1
"#;
        // t_limbs is only in .fsti (type alias), comes before foo
        // This is intentional organization - types first, then functions
        let fsti_content = r#"
module Test

let t_limbs = int

val foo: t_limbs -> t_limbs
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (_, movements, changed) = result.unwrap();
        // Should NOT change - t_limbs at top is valid (no forward ref)
        assert!(!changed, "FSTI-only types at top should be valid");
        assert!(movements.is_empty());
    }

    #[test]
    fn test_forward_reference_needs_fix() {
        // This is the case where we DO need to fix - actual forward reference
        let fst_content = r#"
module Test

type mytype = int
let foo (x: mytype) = x
"#;
        // foo uses mytype, but mytype comes AFTER foo - this is a forward reference error
        let fsti_content = r#"
module Test

val foo: mytype -> mytype
type mytype = int
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (reordered, movements, changed) = result.unwrap();
        // Should change - forward reference detected
        assert!(changed, "Expected change when there is a forward reference");
        assert!(!movements.is_empty());
        // mytype should now come before foo
        let mytype_pos = reordered.find("type mytype");
        let foo_pos = reordered.find("val foo");
        assert!(mytype_pos.is_some() && foo_pos.is_some());
        assert!(mytype_pos.unwrap() < foo_pos.unwrap(), "mytype should come before foo");
    }

    #[test]
    fn test_dependency_respected() {
        let fst_content = r#"
module Test

type mytype = int
val uses_mytype: mytype -> int
"#;
        // mytype should come before uses_mytype due to dependency
        let fsti_content = r#"
module Test

val uses_mytype: mytype -> int
type mytype = int
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (reordered, _, changed) = result.unwrap();
        assert!(changed);
        // mytype should now come before uses_mytype
        let mytype_pos = reordered.find("type mytype");
        let uses_pos = reordered.find("val uses_mytype");
        assert!(mytype_pos.is_some() && uses_pos.is_some());
        assert!(mytype_pos.unwrap() < uses_pos.unwrap());
    }

    // ==================== NEW TESTS FOR FALSE NEGATIVE DETECTION ====================

    #[test]
    fn test_levenshtein_distance_identical() {
        assert_eq!(levenshtein_distance("hello", "hello"), 0);
    }

    #[test]
    fn test_levenshtein_distance_single_char_diff() {
        // Single character substitution
        assert_eq!(levenshtein_distance("baz", "bar"), 1);
        assert_eq!(levenshtein_distance("cat", "car"), 1);
    }

    #[test]
    fn test_levenshtein_distance_insertion() {
        // Missing underscore
        assert_eq!(levenshtein_distance("parser_kindnz", "parser_kind_nz"), 1);
    }

    #[test]
    fn test_levenshtein_distance_deletion() {
        assert_eq!(levenshtein_distance("hello", "helo"), 1);
    }

    #[test]
    fn test_levenshtein_distance_multiple_edits() {
        assert_eq!(levenshtein_distance("kitten", "sitting"), 3);
    }

    #[test]
    fn test_levenshtein_distance_empty() {
        assert_eq!(levenshtein_distance("", "abc"), 3);
        assert_eq!(levenshtein_distance("abc", ""), 3);
        assert_eq!(levenshtein_distance("", ""), 0);
    }

    #[test]
    fn test_find_typo_match_exact_match_excluded() {
        let candidates: HashSet<String> = ["foo", "bar", "baz"]
            .iter()
            .map(|s| s.to_string())
            .collect();
        // "foo" should not match itself
        let result = find_typo_match("foo", &candidates, 2);
        assert!(result.is_none() || result.unwrap().0 != "foo");
    }

    #[test]
    fn test_find_typo_match_finds_close_match() {
        let candidates: HashSet<String> = ["parser_kind_nz", "foo", "bar"]
            .iter()
            .map(|s| s.to_string())
            .collect();
        let result = find_typo_match("parser_kindnz", &candidates, 2);
        assert!(result.is_some());
        let (match_name, dist) = result.unwrap();
        assert_eq!(match_name, "parser_kind_nz");
        assert_eq!(dist, 1);
    }

    #[test]
    fn test_find_typo_match_no_match_above_threshold() {
        let candidates: HashSet<String> = ["completely", "different", "names"]
            .iter()
            .map(|s| s.to_string())
            .collect();
        let result = find_typo_match("parser_kindnz", &candidates, 2);
        assert!(result.is_none());
    }

    #[test]
    fn test_analyze_interface_consistency_orphan_detection() {
        let fsti_content = r#"
module Test

val foo: int -> int
val orphan_decl: int -> int
"#;
        let fst_content = r#"
module Test

let foo x = x + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // Should find orphan_decl as orphan
        assert!(!result.orphan_declarations.is_empty());
        assert!(result
            .orphan_declarations
            .iter()
            .any(|(name, _, _)| name == "orphan_decl"));
    }

    #[test]
    fn test_analyze_interface_consistency_typo_detection() {
        let fsti_content = r#"
module Test

val foo: int -> int
val parser_kindnz: int -> int
"#;
        let fst_content = r#"
module Test

let foo x = x + 1
let parser_kind_nz x = x * 2
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // Should detect typo
        assert!(!result.typo_matches.is_empty());
        let typo = result.typo_matches.iter().find(|(fsti, _, _)| fsti == "parser_kindnz");
        assert!(typo.is_some());
        let (_, fst_name, dist) = typo.unwrap();
        assert_eq!(fst_name, "parser_kind_nz");
        assert_eq!(*dist, 1);
    }

    #[test]
    fn test_analyze_interface_consistency_no_issues() {
        let fsti_content = r#"
module Test

val foo: int -> int
val bar: int -> int
"#;
        let fst_content = r#"
module Test

let foo x = x + 1
let bar x = x * 2
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // No orphans, no typos
        assert!(result.orphan_declarations.is_empty());
        assert!(result.typo_matches.is_empty());
    }

    #[test]
    fn test_analyze_interface_consistency_similar_names_not_typo() {
        // Names that are similar but too different (edit distance > threshold)
        let fsti_content = r#"
module Test

val process_data: int -> int
"#;
        let fst_content = r#"
module Test

let handle_request x = x + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // process_data and handle_request are too different (edit distance >> 2)
        assert!(result.typo_matches.is_empty());
        // But process_data should be flagged as orphan
        assert!(result
            .orphan_declarations
            .iter()
            .any(|(name, typo_match, _)| name == "process_data" && typo_match.is_none()));
    }

    // ==================== FALSE POSITIVE REDUCTION TESTS ====================

    #[test]
    fn test_interface_only_let_type_aliases_not_orphans() {
        // In F*, .fsti commonly defines type aliases via `let` that have no .fst counterpart.
        // These are interface-only definitions and should NOT be flagged as orphans.
        // This is a CRITICAL pattern in hacl-star (e.g., bn_add_eq_len_st in Hacl.Bignum.fsti).
        let fsti_content = r#"
module Test

let bn_add_eq_len_st (t:int) (len:int) =
    int -> int -> int

val bn_add_eq_len: int -> bn_add_eq_len_st int int
"#;
        let fst_content = r#"
module Test

let bn_add_eq_len x a b = a + b
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // bn_add_eq_len_st is a let type alias in .fsti - NOT an orphan
        assert!(
            !result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "bn_add_eq_len_st"),
            "Interface-only let type alias should NOT be flagged as orphan"
        );
        // bn_add_eq_len is a val with implementation - not orphan
        assert!(result.orphan_declarations.is_empty());
    }

    #[test]
    fn test_interface_only_type_definitions_not_orphans() {
        // Abstract types in .fsti without .fst counterpart should not be orphans
        let fsti_content = r#"
module Test

type abstract_key

val encrypt: abstract_key -> int -> int
"#;
        let fst_content = r#"
module Test

let encrypt k x = x + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // abstract_key is a type in .fsti only - NOT an orphan
        assert!(
            !result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "abstract_key"),
            "Interface-only type definition should NOT be flagged as orphan"
        );
    }

    #[test]
    fn test_interface_only_class_not_orphan() {
        // Class definitions in .fsti are interface-only by design
        let fsti_content = r#"
module Test

class bn (t:int) = {
  len: int;
  add: int -> int;
}

val mk_runtime_bn: int -> bn int
"#;
        let fst_content = r#"
module Test

let mk_runtime_bn t = { len = 0; add = fun x -> x }
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        assert!(
            !result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "bn"),
            "Interface-only class definition should NOT be flagged as orphan"
        );
    }

    #[test]
    fn test_interface_only_inline_let_not_orphan() {
        // inline_for_extraction let definitions in .fsti are common type aliases
        let fsti_content = r#"
module Test

inline_for_extraction let meta_len (t:int) = int

val mk_runtime: meta_len int -> int
"#;
        let fst_content = r#"
module Test

let mk_runtime len = len + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        assert!(
            !result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "meta_len"),
            "Interface-only inline_for_extraction let should NOT be flagged as orphan"
        );
    }

    #[test]
    fn test_qualified_names_no_false_dependencies() {
        // When .fsti references S.bn_add (qualified), it should NOT create a
        // dependency on the locally declared bn_add. This was a major source
        // of false forward-reference warnings in hacl-star.
        let fst_content = r#"
module Test

type mytype = int
let bn_add x = x + 1
"#;
        // bn_add_st references S.bn_add in its body (qualified), and bn_add is
        // declared later. Without the qualified-name fix, this would falsely
        // appear as a forward reference.
        let fsti_content = r#"
module Test

let bn_add_st (t:int) =
    int -> S.bn_add int

val bn_add: int -> int
"#;

        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (_, movements, changed) = result.unwrap();
        // Should NOT suggest reordering - S.bn_add is qualified, not a local ref
        assert!(
            !changed,
            "Qualified name S.bn_add should not create false dependency on local bn_add. \
             Movements: {:?}",
            movements
        );
    }

    #[test]
    fn test_many_interface_only_defs_no_warnings() {
        // Simulates a typical hacl-star .fsti with many type aliases
        // None of these should generate orphan warnings
        let fsti_content = r#"
module Test

let add_st (t:int) (len:int) =
    int -> int -> int

let sub_st (t:int) (len:int) =
    int -> int -> int

let mul_st (t:int) =
    int -> int -> int

type config_t = int

val add: int -> add_st int int
val sub: int -> sub_st int int
val mul: int -> mul_st int
"#;
        let fst_content = r#"
module Test

let add t a b = a + b
let sub t a b = a - b
let mul t a b = a * b
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // No type aliases should be flagged
        assert!(
            result.orphan_declarations.is_empty(),
            "Interface-only type aliases should not generate orphan warnings. \
             Got: {:?}",
            result.orphan_declarations
        );
        assert!(result.typo_matches.is_empty());
    }

    #[test]
    fn test_val_orphan_still_detected() {
        // Val declarations WITHOUT .fst implementation should still be flagged
        let fsti_content = r#"
module Test

val foo: int -> int
val missing_impl: int -> int
"#;
        let fst_content = r#"
module Test

let foo x = x + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // missing_impl is a val with no let in .fst - should be orphan
        assert!(
            result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "missing_impl"),
            "Val without implementation should still be flagged as orphan"
        );
    }

    #[test]
    fn test_assume_val_not_orphan() {
        // assume val declarations never need .fst implementations
        let fsti_content = r#"
module Test

assume val external_fn: int -> int

val foo: int -> int
"#;
        let fst_content = r#"
module Test

let foo x = x + 1
"#;

        let result = analyze_interface_consistency(fsti_content, fst_content);

        // assume val should not be flagged (it's BlockType::Assume, not Val)
        assert!(
            !result
                .orphan_declarations
                .iter()
                .any(|(name, _, _)| name == "external_fn"),
            "assume val should NOT be flagged as orphan"
        );
    }

    // ==================== SAFETY FEATURE TESTS ====================

    #[test]
    fn test_content_hash_identical() {
        let content = "module Test\n\nval foo: int -> int\n";
        let hash1 = compute_content_hash(content);
        let hash2 = compute_content_hash(content);
        assert_eq!(hash1, hash2, "Same content should produce same hash");
    }

    #[test]
    fn test_content_hash_whitespace_insensitive() {
        let content1 = "module Test\n\nval foo: int -> int\n";
        let content2 = "module Test\n\n\n  val   foo:   int  ->  int\n";
        // Both have the SAME non-whitespace content, so hashes should match
        let hash1 = compute_content_hash(content1);
        let hash2 = compute_content_hash(content2);
        // Hash is computed over non-whitespace chars only, so these should match
        assert_eq!(hash1, hash2, "Same non-ws content should produce same hash");
    }

    #[test]
    fn test_content_hash_detects_missing_content() {
        let content1 = "module Test\n\nval foo: int -> int\nval bar: int -> int\n";
        let content2 = "module Test\n\nval foo: int -> int\n";
        let hash1 = compute_content_hash(content1);
        let hash2 = compute_content_hash(content2);
        assert_ne!(hash1, hash2, "Missing content should produce different hash");
    }

    #[test]
    fn test_content_hash_detects_duplicated_content() {
        let content1 = "module Test\n\nval foo: int -> int\n";
        let content2 = "module Test\n\nval foo: int -> int\nval foo: int -> int\n";
        let hash1 = compute_content_hash(content1);
        let hash2 = compute_content_hash(content2);
        assert_ne!(hash1, hash2, "Duplicated content should produce different hash");
    }

    #[test]
    fn test_extract_declaration_names() {
        let content = r#"
module Test

val foo: int -> int
type mytype = int
let bar x = x + 1
"#;
        let names = extract_all_declaration_names(content);
        assert!(names.contains(&"foo".to_string()));
        assert!(names.contains(&"mytype".to_string()));
        assert!(names.contains(&"bar".to_string()));
    }

    #[test]
    fn test_count_declaration_names() {
        let names = vec!["foo".to_string(), "bar".to_string(), "foo".to_string()];
        let counts = count_declaration_names(&names);
        assert_eq!(counts.get("foo"), Some(&2));
        assert_eq!(counts.get("bar"), Some(&1));
    }

    #[test]
    fn test_validate_reorder_identical_content() {
        let content = r#"module Test

val foo: int -> int
val bar: int -> int
"#;
        let warnings = validate_reorder(content, content, "Test.fsti");
        assert!(warnings.is_empty(), "Identical content should produce no warnings");
    }

    #[test]
    fn test_validate_reorder_detects_lost_content() {
        let original = r#"module Test

val foo: int -> int
val bar: int -> int
"#;
        let reordered = r#"module Test

val foo: int -> int
"#;
        let warnings = validate_reorder(original, reordered, "Test.fsti");
        assert!(!warnings.is_empty(), "Lost content should produce warnings");
        assert!(
            warnings.iter().any(|w| w.severity == ReorderWarningSeverity::Critical),
            "Lost content should produce CRITICAL warning. Got: {:?}",
            warnings
        );
    }

    #[test]
    fn test_validate_reorder_detects_lost_module() {
        let original = r#"module Test

val foo: int -> int
"#;
        let reordered = r#"
val foo: int -> int
"#;
        let warnings = validate_reorder(original, reordered, "Test.fsti");
        // Should detect the missing module via character count or declaration check
        assert!(
            warnings.iter().any(|w| w.severity == ReorderWarningSeverity::Critical),
            "Lost module should produce CRITICAL warning. Got: {:?}",
            warnings
        );
    }

    #[test]
    fn test_validate_reorder_allows_declaration_reordering() {
        // Reordering declarations (changing order but not content) should be OK
        let original = r#"module Test

val foo: int -> int

val bar: int -> int
"#;
        let reordered = r#"module Test

val bar: int -> int

val foo: int -> int
"#;
        let warnings = validate_reorder(original, reordered, "Test.fsti");
        // Should NOT have critical warnings for reordering
        let critical_count = warnings
            .iter()
            .filter(|w| w.severity == ReorderWarningSeverity::Critical)
            .count();
        assert_eq!(
            critical_count, 0,
            "Reordering should not cause critical warnings. Got: {:?}",
            warnings
        );
    }

    #[test]
    fn test_preflight_check_basic() {
        let content = r#"module Test

val foo: int -> int
type mytype = int
"#;
        let result = preflight_reorder_check(content);
        assert!(result.is_ok(), "Valid content should pass preflight");
        let report = result.unwrap();
        assert!(report.has_module_declaration);
        assert_eq!(report.total_declarations, 2);
        assert!(report.declaration_names.contains(&"foo".to_string()));
        assert!(report.declaration_names.contains(&"mytype".to_string()));
    }

    #[test]
    fn test_preflight_check_no_module() {
        let content = r#"
val foo: int -> int
"#;
        let result = preflight_reorder_check(content);
        assert!(result.is_err(), "Missing module should fail preflight");
    }

    #[test]
    fn test_dry_run_no_changes() {
        let fst_content = r#"
module Test

let foo x = x + 1
let bar x = foo x
"#;
        let fsti_content = r#"
module Test

val foo: int -> int
val bar: int -> int
"#;
        let result = dry_run_reorder(fsti_content, fst_content);
        assert!(result.is_ok());
        let dry_run = result.unwrap();
        assert!(!dry_run.has_changes, "No forward refs means no changes needed");
        assert_eq!(dry_run.warning_level, DryRunWarningLevel::None);
    }

    #[test]
    fn test_dry_run_with_changes() {
        let fst_content = r#"module Test

type mytype = int
let foo (x: mytype) = x
"#;
        // foo uses mytype, but mytype comes AFTER foo - forward reference
        let fsti_content = r#"module Test

val foo: mytype -> mytype
type mytype = int
"#;
        let result = dry_run_reorder(fsti_content, fst_content);
        // Dry run may fail if there are parsing issues, but if it succeeds...
        if let Ok(dry_run) = result {
            // Note: the reordering algorithm may or may not make changes depending
            // on whether it detects the forward reference
            // The important thing is that it doesn't crash
            if dry_run.has_changes {
                assert!(!dry_run.movements.is_empty(), "If changes, should have movements");
            }
        }
        // Test passes as long as it doesn't panic
    }

    #[test]
    fn test_dry_run_warning_levels() {
        // Test that warning levels are assigned correctly
        // Low: 1-3 movements
        // Medium: 4-10 movements
        // High: >10 movements
        let dry_run_low = DryRunResult {
            movements: vec![
                MovementInfo {
                    name: "a".to_string(),
                    old_position: 0,
                    new_position: 1,
                    direction: MovementDirection::Down,
                    distance: 1,
                },
            ],
            total_declarations: 5,
            has_changes: true,
            warning_level: DryRunWarningLevel::Low,
            validation_warnings: vec![],
        };
        assert_eq!(dry_run_low.warning_level, DryRunWarningLevel::Low);
    }

    #[test]
    fn test_movement_direction() {
        let up = MovementInfo {
            name: "test".to_string(),
            old_position: 5,
            new_position: 2,
            direction: MovementDirection::Up,
            distance: 3,
        };
        assert_eq!(up.direction, MovementDirection::Up);

        let down = MovementInfo {
            name: "test".to_string(),
            old_position: 2,
            new_position: 5,
            direction: MovementDirection::Down,
            distance: 3,
        };
        assert_eq!(down.direction, MovementDirection::Down);
    }

    #[test]
    fn test_validation_blocks_dangerous_fix() {
        // If validation fails with critical warnings, the check_pair should NOT offer a fix
        // This is tested indirectly through validate_reorder
        let original = r#"module Test

val foo: int -> int
val bar: int -> int
"#;
        // Simulate corrupted reordering that loses content
        let corrupted = r#"module Test

val foo: int -> int
"#;
        let warnings = validate_reorder(original, corrupted, "Test.fsti");
        let has_critical = warnings
            .iter()
            .any(|w| w.severity == ReorderWarningSeverity::Critical);
        assert!(has_critical, "Corrupted content should produce critical warnings");
    }

    #[test]
    fn test_reorder_preserves_content_basic() {
        // Test a basic reordering scenario
        let fst_content = r#"module Test

type mytype = int
let foo (x: mytype) = x
"#;
        let fsti_content = r#"module Test

val foo: mytype -> mytype
type mytype = int
"#;
        let result = reorder_fsti_content(fsti_content, fst_content);
        // The reordering might fail or succeed depending on parsing
        // What's important is that if it succeeds, we validate it
        if let Ok((reordered, _, changed)) = result {
            if changed {
                // Validate that content is preserved using character comparison
                let warnings = validate_reorder(fsti_content, &reordered, "Test.fsti");

                // Print for debugging
                println!("Original:\n{}", fsti_content);
                println!("Reordered:\n{}", reordered);
                println!("Warnings: {:?}", warnings);

                // The key check is that declaration names are preserved
                let orig_names = extract_all_declaration_names(fsti_content);
                let new_names = extract_all_declaration_names(&reordered);
                assert_eq!(
                    orig_names.len(),
                    new_names.len(),
                    "Declaration count should be preserved"
                );
            }
        }
    }

    #[test]
    fn test_mutual_recursion_preservation() {
        // Mutual recursion blocks should stay together
        let fst_content = r#"
module Test

type a = A of b
and b = B of a

let foo x = x
"#;
        let fsti_content = r#"
module Test

type a = A of b
and b = B of a

val foo: int -> int
"#;
        let result = reorder_fsti_content(fsti_content, fst_content);
        assert!(result.is_ok());
        let (reordered, _, _) = result.unwrap();

        // Both types should be present
        assert!(reordered.contains("type a"), "Type a should be preserved");
        assert!(reordered.contains("and b"), "Mutual recursion 'and b' should be preserved");

        // Validate no critical issues
        let warnings = validate_reorder(fsti_content, &reordered, "Test.fsti");
        let critical_count = warnings
            .iter()
            .filter(|w| w.severity == ReorderWarningSeverity::Critical)
            .count();
        assert_eq!(critical_count, 0, "Mutual recursion should be handled correctly");
    }
}