brrr-lint 0.1.0

//! FST016: Verification performance profiler.
//!
//! Detects patterns that cause slow verification:
//! - High fuel/ifuel requirements
//! - Large contexts
//! - Timeout-prone patterns
//!
//! This rule performs static analysis to identify code patterns that commonly
//! lead to slow F* verification times, providing actionable hints for optimization.

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

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

lazy_static! {
    /// Matches --fuel N settings in push-options or other directives.
    static ref FUEL_SETTING: Regex = Regex::new(r#"--fuel\s+(\d+)"#).unwrap();

    /// Matches --ifuel N settings.
    static ref IFUEL_SETTING: Regex = Regex::new(r#"--ifuel\s+(\d+)"#).unwrap();

    /// Matches --z3rlimit N settings.
    static ref RLIMIT_SETTING: Regex = Regex::new(r#"--z3rlimit\s+(\d+)"#).unwrap();

    /// Matches --quake option indicating proof instability testing.
    static ref QUAKE_OPTION: Regex = Regex::new(r"--quake").unwrap();

    /// Matches --retry option indicating proof flakiness workaround.
    static ref RETRY_OPTION: Regex = Regex::new(r"--retry").unwrap();

    /// Matches calc (==) blocks which can be expensive for large chains.
    static ref LONG_CALC: Regex = Regex::new(r"calc\s*\(\s*==\s*\)").unwrap();

    /// Matches assert statements for counting assertion density.
    static ref MANY_ASSERTS: Regex = Regex::new(r"assert\s*\(").unwrap();

    /// Matches SMTPat annotations (many patterns can slow verification).
    static ref SMTPAT_MANY: Regex = Regex::new(r"SMTPat").unwrap();

    /// Matches #push-options directives.
    static ref PUSH_OPTIONS: Regex = Regex::new(r"#push-options").unwrap();

    /// Matches split_queries option.
    static ref SPLIT_QUERIES: Regex = Regex::new(r"--split_queries").unwrap();
}

/// FST016: Performance profiler rule.
///
/// Detects patterns that commonly cause slow verification in F* code:
/// - High fuel settings (> threshold) indicating complex recursion unfolding
/// - High ifuel settings (> threshold) indicating deep inductive reasoning
/// - High z3rlimit values (> threshold) suggesting SMT solver stress
/// - Usage of --quake indicating proof instability
/// - High assertion density suggesting overly complex proof obligations
pub struct PerfProfilerRule {
    /// Threshold above which fuel settings trigger a warning.
    pub fuel_threshold: u32,
    /// Threshold above which ifuel settings trigger a warning.
    pub ifuel_threshold: u32,
    /// Threshold above which z3rlimit settings trigger a warning.
    pub rlimit_threshold: u32,
    /// Threshold for assertion count to trigger module complexity warning.
    pub assert_count_threshold: usize,
}

impl PerfProfilerRule {
    /// Create a new performance profiler rule with default thresholds.
    ///
    /// Default thresholds calibrated against real-world F* projects (e.g. hacl-star):
    /// - fuel_threshold: 5 (fuel 0-4 is standard practice)
    /// - ifuel_threshold: 3 (ifuel 0-2 is standard, 3 is borderline)
    /// - rlimit_threshold: 300 (z3rlimit 50-200 is common for crypto proofs)
    /// - assert_count_threshold: 50
    ///
    /// Severity is proportional to the value:
    /// - fuel 6-7 / ifuel 4: Info, fuel 8+ / ifuel 5+: Warning
    /// - z3rlimit 301-600: Info, 601-1000: Warning, 1001+: Error
    pub fn new() -> Self {
        Self {
            fuel_threshold: 5,
            ifuel_threshold: 3,
            rlimit_threshold: 300,
            assert_count_threshold: 50,
        }
    }

    /// Create a rule with custom thresholds.
    pub fn with_thresholds(
        fuel_threshold: u32,
        ifuel_threshold: u32,
        rlimit_threshold: u32,
        assert_count_threshold: usize,
    ) -> Self {
        Self {
            fuel_threshold,
            ifuel_threshold,
            rlimit_threshold,
            assert_count_threshold,
        }
    }

    /// Check for high fuel setting on a single line.
    ///
    /// Severity scales with the value:
    /// - threshold+1 to threshold+2: Info (mildly elevated)
    /// - threshold+3 and above: Warning (significantly elevated)
    fn check_fuel(&self, file: &PathBuf, line_num: usize, line: &str) -> Option<Diagnostic> {
        if let Some(caps) = FUEL_SETTING.captures(line) {
            if let Ok(fuel) = caps.get(1).unwrap().as_str().parse::<u32>() {
                if fuel > self.fuel_threshold {
                    let severity = if fuel > self.fuel_threshold + 2 {
                        DiagnosticSeverity::Warning
                    } else {
                        DiagnosticSeverity::Info
                    };
                    return Some(Diagnostic {
                        rule: RuleCode::FST016,
                        severity,
                        file: file.clone(),
                        range: Range::point(line_num + 1, 1),
                        message: format!(
                            "High fuel setting ({}) may indicate proof complexity. \
                             Consider splitting into smaller lemmas or adding explicit hints.",
                            fuel
                        ),
                        fix: None,
                    });
                }
            }
        }
        None
    }

    /// Check for high ifuel setting on a single line.
    ///
    /// Severity scales with the value:
    /// - threshold+1: Info (mildly elevated)
    /// - threshold+2 and above: Warning (significantly elevated)
    fn check_ifuel(&self, file: &PathBuf, line_num: usize, line: &str) -> Option<Diagnostic> {
        if let Some(caps) = IFUEL_SETTING.captures(line) {
            if let Ok(ifuel) = caps.get(1).unwrap().as_str().parse::<u32>() {
                if ifuel > self.ifuel_threshold {
                    let severity = if ifuel > self.ifuel_threshold + 1 {
                        DiagnosticSeverity::Warning
                    } else {
                        DiagnosticSeverity::Info
                    };
                    return Some(Diagnostic {
                        rule: RuleCode::FST016,
                        severity,
                        file: file.clone(),
                        range: Range::point(line_num + 1, 1),
                        message: format!(
                            "High ifuel setting ({}) suggests deep inductive reasoning. \
                             Consider adding explicit inversion lemmas.",
                            ifuel
                        ),
                        fix: None,
                    });
                }
            }
        }
        None
    }

    /// Check for high z3rlimit setting on a single line.
    ///
    /// Severity scales with the value:
    /// - threshold+1 to 2*threshold: Info (elevated but manageable)
    /// - 2*threshold+1 to 3*threshold: Warning (high, likely needs refactoring)
    /// - above 3*threshold: Error (extremely high, proof architecture issue)
    fn check_rlimit(&self, file: &PathBuf, line_num: usize, line: &str) -> Option<Diagnostic> {
        if let Some(caps) = RLIMIT_SETTING.captures(line) {
            if let Ok(rlimit) = caps.get(1).unwrap().as_str().parse::<u32>() {
                if rlimit > self.rlimit_threshold {
                    let severity = if rlimit > self.rlimit_threshold * 3 {
                        DiagnosticSeverity::Error
                    } else if rlimit > self.rlimit_threshold * 2 {
                        DiagnosticSeverity::Warning
                    } else {
                        DiagnosticSeverity::Info
                    };
                    return Some(Diagnostic {
                        rule: RuleCode::FST016,
                        severity,
                        file: file.clone(),
                        range: Range::point(line_num + 1, 1),
                        message: format!(
                            "High z3rlimit ({}) detected. Consider using --split_queries always \
                             or extracting helper lemmas to reduce SMT solver load.",
                            rlimit
                        ),
                        fix: None,
                    });
                }
            }
        }
        None
    }

    /// Check for --quake option indicating proof instability.
    ///
    /// Quake is a legitimate tool for testing proof stability in CI environments.
    /// Only emit a Hint (lowest severity) as an informational note, not a warning.
    fn check_quake(&self, file: &PathBuf, line_num: usize, line: &str) -> Option<Diagnostic> {
        if QUAKE_OPTION.is_match(line) {
            return Some(Diagnostic {
                rule: RuleCode::FST016,
                severity: DiagnosticSeverity::Hint,
                file: file.clone(),
                range: Range::point(line_num + 1, 1),
                message: "Using --quake for proof stability testing. \
                         This is fine for CI; consider removing if proof is now stable."
                    .to_string(),
                fix: None,
            });
        }
        None
    }

    /// Check for --retry option indicating flaky proof workaround.
    ///
    /// Retry is acceptable during development and incremental proving.
    /// Emit as Info rather than Warning to reduce noise.
    fn check_retry(&self, file: &PathBuf, line_num: usize, line: &str) -> Option<Diagnostic> {
        if RETRY_OPTION.is_match(line) {
            return Some(Diagnostic {
                rule: RuleCode::FST016,
                severity: DiagnosticSeverity::Info,
                file: file.clone(),
                range: Range::point(line_num + 1, 1),
                message: "Using --retry for flaky verification. \
                         Acceptable during development; consider stabilizing for production."
                    .to_string(),
                fix: None,
            });
        }
        None
    }
}

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

impl Rule for PerfProfilerRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST016
    }

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

        for (line_num, line) in content.lines().enumerate() {
            // Skip comment lines
            let trimmed = line.trim();
            if trimmed.starts_with("//") || trimmed.starts_with("(*") {
                continue;
            }

            // Check fuel settings
            if let Some(diag) = self.check_fuel(file, line_num, line) {
                diagnostics.push(diag);
            }

            // Check ifuel settings
            if let Some(diag) = self.check_ifuel(file, line_num, line) {
                diagnostics.push(diag);
            }

            // Check z3rlimit settings
            if let Some(diag) = self.check_rlimit(file, line_num, line) {
                diagnostics.push(diag);
            }

            // Check for quake option
            if let Some(diag) = self.check_quake(file, line_num, line) {
                diagnostics.push(diag);
            }

            // Check for retry option
            if let Some(diag) = self.check_retry(file, line_num, line) {
                diagnostics.push(diag);
            }
        }

        // Check for high assertion density (file-level metric)
        let assert_count = MANY_ASSERTS.find_iter(content).count();
        if assert_count > self.assert_count_threshold {
            diagnostics.push(Diagnostic {
                rule: RuleCode::FST016,
                severity: DiagnosticSeverity::Info,
                file: file.clone(),
                range: Range::point(1, 1),
                message: format!(
                    "File has {} assertions. High assertion density ({} > {}) may slow \
                     verification. Consider splitting into smaller modules.",
                    assert_count, assert_count, self.assert_count_threshold
                ),
                fix: None,
            });
        }

        // Check for many SMTPat annotations (can cause pattern explosion)
        let smtpat_count = SMTPAT_MANY.find_iter(content).count();
        if smtpat_count > 20 {
            diagnostics.push(Diagnostic {
                rule: RuleCode::FST016,
                severity: DiagnosticSeverity::Info,
                file: file.clone(),
                range: Range::point(1, 1),
                message: format!(
                    "File has {} SMTPat annotations. Many patterns can cause quantifier \
                     instantiation explosion. Review pattern selectivity.",
                    smtpat_count
                ),
                fix: None,
            });
        }

        diagnostics
    }
}

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

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

    // ---------------------------------------------------------------
    // Fuel threshold tests
    // ---------------------------------------------------------------

    #[test]
    fn test_fuel_below_threshold_no_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 5
        // fuel 0-5 should produce no warnings (common in real F* code)
        for fuel in [0, 1, 2, 3, 4, 5] {
            let content = format!("#push-options \"--fuel {}\"", fuel);
            let diagnostics = rule.check(&test_file(), &content);
            assert!(
                diagnostics.is_empty(),
                "fuel {} should not trigger a warning",
                fuel
            );
        }
    }

    #[test]
    fn test_fuel_mildly_elevated_is_info() {
        let rule = PerfProfilerRule::new(); // threshold = 5, info for 6-7
        let content = "#push-options \"--fuel 6\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Info);
        assert!(diagnostics[0].message.contains("6"));
    }

    #[test]
    fn test_fuel_high_is_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 5, warning for 8+
        let content = "#push-options \"--fuel 10\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Warning);
        assert!(diagnostics[0].message.contains("10"));
    }

    // ---------------------------------------------------------------
    // Ifuel threshold tests
    // ---------------------------------------------------------------

    #[test]
    fn test_ifuel_below_threshold_no_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 3
        // ifuel 0-3 should produce no warnings (standard in F*)
        for ifuel in [0, 1, 2, 3] {
            let content = format!("#push-options \"--ifuel {}\"", ifuel);
            let diagnostics = rule.check(&test_file(), &content);
            assert!(
                diagnostics.is_empty(),
                "ifuel {} should not trigger a warning",
                ifuel
            );
        }
    }

    #[test]
    fn test_ifuel_mildly_elevated_is_info() {
        let rule = PerfProfilerRule::new(); // threshold = 3, info for 4
        let content = "#push-options \"--ifuel 4\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Info);
        assert!(diagnostics[0].message.contains("4"));
    }

    #[test]
    fn test_ifuel_high_is_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 3, warning for 5+
        let content = "#push-options \"--ifuel 5\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Warning);
        assert!(diagnostics[0].message.contains("5"));
    }

    // ---------------------------------------------------------------
    // z3rlimit threshold tests (the main source of false positives)
    // ---------------------------------------------------------------

    #[test]
    fn test_rlimit_common_values_no_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 300
        // These are all common in crypto proofs and should NOT warn
        for rlimit in [10, 20, 30, 40, 50, 60, 75, 80, 100, 150, 200, 250, 300] {
            let content = format!("#push-options \"--z3rlimit {}\"", rlimit);
            let diagnostics = rule.check(&test_file(), &content);
            assert!(
                diagnostics.is_empty(),
                "z3rlimit {} should not trigger a warning (common in crypto proofs)",
                rlimit
            );
        }
    }

    #[test]
    fn test_rlimit_elevated_is_info() {
        let rule = PerfProfilerRule::new(); // threshold = 300, info for 301-600
        let content = "#push-options \"--z3rlimit 400\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Info);
        assert!(diagnostics[0].message.contains("400"));
    }

    #[test]
    fn test_rlimit_high_is_warning() {
        let rule = PerfProfilerRule::new(); // threshold = 300, warning for 601-900
        let content = "#push-options \"--z3rlimit 700\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Warning);
        assert!(diagnostics[0].message.contains("700"));
    }

    #[test]
    fn test_rlimit_extreme_is_error() {
        let rule = PerfProfilerRule::new(); // threshold = 300, error for 901+
        let content = "#push-options \"--z3rlimit 2000\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Error);
        assert!(diagnostics[0].message.contains("2000"));
    }

    #[test]
    fn test_rlimit_boundary_600_is_info() {
        let rule = PerfProfilerRule::new(); // 600 <= 2*300, so Info
        let content = "#push-options \"--z3rlimit 600\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Info);
    }

    #[test]
    fn test_rlimit_boundary_601_is_warning() {
        let rule = PerfProfilerRule::new(); // 601 > 2*300, so Warning
        let content = "#push-options \"--z3rlimit 601\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Warning);
    }

    #[test]
    fn test_rlimit_boundary_900_is_warning() {
        let rule = PerfProfilerRule::new(); // 900 <= 3*300, so Warning
        let content = "#push-options \"--z3rlimit 900\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Warning);
    }

    #[test]
    fn test_rlimit_boundary_901_is_error() {
        let rule = PerfProfilerRule::new(); // 901 > 3*300, so Error
        let content = "#push-options \"--z3rlimit 901\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Error);
    }

    // ---------------------------------------------------------------
    // Quake and retry tests
    // ---------------------------------------------------------------

    #[test]
    fn test_quake_is_hint() {
        let rule = PerfProfilerRule::new();
        let content = "#push-options \"--quake 3/5\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Hint);
        assert!(diagnostics[0].message.contains("stability"));
    }

    #[test]
    fn test_retry_is_info() {
        let rule = PerfProfilerRule::new();
        let content = "#push-options \"--retry 3\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert_eq!(diagnostics[0].severity, DiagnosticSeverity::Info);
        assert!(diagnostics[0].message.contains("retry"));
    }

    // ---------------------------------------------------------------
    // File-level metrics tests
    // ---------------------------------------------------------------

    #[test]
    fn test_many_asserts_detection() {
        let rule = PerfProfilerRule::with_thresholds(5, 3, 300, 5);
        let content = r#"
let test () =
    assert (1 = 1);
    assert (2 = 2);
    assert (3 = 3);
    assert (4 = 4);
    assert (5 = 5);
    assert (6 = 6);
    ()
"#;
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("assertions"));
        assert!(diagnostics[0].message.contains("6"));
    }

    #[test]
    fn test_smtpat_count() {
        let rule = PerfProfilerRule::new();
        let mut content = String::new();
        for i in 0..25 {
            content.push_str(&format!(
                "val lemma_{} : x:int -> Lemma (requires True) (ensures True) [SMTPat (x + {})]\n",
                i, i
            ));
        }
        let diagnostics = rule.check(&test_file(), &content);
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("SMTPat"));
        assert!(diagnostics[0].message.contains("25"));
    }

    // ---------------------------------------------------------------
    // Combined and edge case tests
    // ---------------------------------------------------------------

    #[test]
    fn test_multiple_issues_on_one_line() {
        let rule = PerfProfilerRule::new();
        let content = "#push-options \"--fuel 10 --ifuel 5 --z3rlimit 400 --quake 3/5\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 4); // fuel, ifuel, rlimit, quake
    }

    #[test]
    fn test_comments_skipped() {
        let rule = PerfProfilerRule::new();
        let content = r#"
// #push-options "--fuel 10"
(* --fuel 10 *)
let normal () = ()
"#;
        let diagnostics = rule.check(&test_file(), content);
        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_custom_thresholds() {
        let rule = PerfProfilerRule::with_thresholds(2, 1, 50, 10);
        let content = "#push-options \"--fuel 3 --ifuel 2 --z3rlimit 60\"";
        let diagnostics = rule.check(&test_file(), content);
        assert_eq!(diagnostics.len(), 3); // All three exceed lower thresholds
    }

    #[test]
    fn test_hacl_star_common_pattern_no_warning() {
        // This is the most common pattern in hacl-star: should produce zero warnings
        let rule = PerfProfilerRule::new();
        let content = r#"
#push-options "--fuel 0 --ifuel 0 --z3rlimit 50"
let poly1305_update (ctx: poly_ctx) (block: lbytes 16) : poly_ctx =
    let acc = ctx.acc in
    let r = ctx.r in
    (acc +. encode block) *. r
#pop-options
"#;
        let diagnostics = rule.check(&test_file(), content);
        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_hacl_star_elevated_rlimit_no_warning() {
        // z3rlimit 200 is used 77 times in hacl-star -- must not warn
        let rule = PerfProfilerRule::new();
        let content = r#"
#push-options "--fuel 1 --ifuel 0 --z3rlimit 200"
let lemma_chacha20_quarter_round a b c d s =
    ()
#pop-options
"#;
        let diagnostics = rule.check(&test_file(), content);
        assert!(diagnostics.is_empty());
    }

    #[test]
    fn test_severity_proportional_to_value() {
        let rule = PerfProfilerRule::new(); // fuel=5, ifuel=3, rlimit=300

        // Just over threshold: Info
        let d = rule.check_fuel(&test_file(), 0, "--fuel 6").unwrap();
        assert_eq!(d.severity, DiagnosticSeverity::Info);

        // Well over threshold: Warning
        let d = rule.check_fuel(&test_file(), 0, "--fuel 9").unwrap();
        assert_eq!(d.severity, DiagnosticSeverity::Warning);

        // rlimit tiers
        let d = rule.check_rlimit(&test_file(), 0, "--z3rlimit 400").unwrap();
        assert_eq!(d.severity, DiagnosticSeverity::Info);

        let d = rule.check_rlimit(&test_file(), 0, "--z3rlimit 700").unwrap();
        assert_eq!(d.severity, DiagnosticSeverity::Warning);

        let d = rule.check_rlimit(&test_file(), 0, "--z3rlimit 1000").unwrap();
        assert_eq!(d.severity, DiagnosticSeverity::Error);
    }
}