pmat 3.30.1

/// Analyzes function provability using lightweight formal methods analysis.
///
/// This handler performs provability analysis on functions to determine their
/// formal verification potential using static analysis techniques.
///
/// # Toyota Way: Single Responsibility
/// - Dedicated handler for provability analysis only
/// - Clear separation from complexity analysis  
/// - Focused on formal methods and verification
///
/// # Parameters
///
/// * `project_path` - Root directory of the project to analyze
/// * `functions` - Specific functions to analyze (empty = all functions)
/// * `_analysis_depth` - Depth of analysis (currently unused)
/// * `format` - Output format for results
/// * `high_confidence_only` - Filter to high-confidence results only
/// * `include_evidence` - Include supporting evidence in output
/// * `output` - Optional output file path
/// * `top_files` - Number of top files to include in summary
///
/// # Returns
///
/// Configuration for provability analysis (SPRINT-22)
#[derive(Debug, Clone)]
pub struct ProvabilityConfig {
    pub project_path: PathBuf,
    pub functions: Vec<String>,
    pub analysis_depth: usize,
    pub format: ProvabilityOutputFormat,
    pub high_confidence_only: bool,
    pub include_evidence: bool,
    pub output: Option<PathBuf>,
    pub top_files: usize,
}

/// * `Ok(())` - Analysis completed successfully
/// * `Err(anyhow::Error)` - Analysis failed with detailed error context (cognitive complexity ≤8)
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub async fn handle_analyze_provability(config: ProvabilityConfig) -> Result<()> {
    use crate::services::lightweight_provability_analyzer::LightweightProvabilityAnalyzer;

    // GH-666: a nonexistent path discovered zero functions and this reported
    // "📊 Found 0 source files / ✓ Analyzed 0 functions" with exit 0 — a
    // successful empty analysis of a tree that was never there.
    crate::cli::ensure_analysis_path_exists(&config.project_path)?;

    use crate::cli::colors as c;
    crate::status_eprintln!("{}", c::dim("🔬 Analyzing function provability..."));

    // The discovered FunctionIds carry paths relative to `project_path` (that is
    // what the report prints), so the analyzer has to be told what they are
    // relative TO. Without it the source was read relative to the process cwd
    // and every function fell back to the 20% no-evidence baseline whenever the
    // shell was not already inside the analyzed project.
    let analyzer = LightweightProvabilityAnalyzer::new().with_project_root(&config.project_path);
    let function_ids = resolve_function_targets(&config).await?;
    let summaries = run_provability_analysis(&analyzer, &function_ids).await?;
    let filtered_summaries = prepare_filtered_summaries(&summaries, config.high_confidence_only);
    let content = format_provability_output(&function_ids, &filtered_summaries, &config)?;

    write_provability_output(&content, &config.output).await?;

    Ok(())
}

/// Resolve function targets for analysis (cognitive complexity ≤6)
async fn resolve_function_targets(
    config: &ProvabilityConfig,
) -> Result<Vec<crate::services::lightweight_provability_analyzer::FunctionId>> {
    use crate::cli::provability_helpers::{discover_project_functions, match_function_spec};

    let discovered = discover_project_functions(&config.project_path).await?;

    if config.functions.is_empty() {
        return Ok(discovered);
    }

    // Every --functions spec used to be handed to parse_function_spec, which
    // built a FunctionId out of the argument string with no lookup at all — so
    // `--functions ghost` against an EMPTY directory still printed "✓ Analyzed
    // 1 functions" and scored it 20.0%. A name that is not in the tree has to
    // come back as an error, not as a result row.
    let mut ids = Vec::new();
    for spec in &config.functions {
        let matches = match_function_spec(spec, &discovered);
        if matches.is_empty() {
            anyhow::bail!(
                "no function named `{spec}` found under {}",
                config.project_path.display()
            );
        }
        ids.extend(matches);
    }
    Ok(ids)
}

/// Run provability analysis on function targets (cognitive complexity ≤3)
async fn run_provability_analysis(
    analyzer: &crate::services::lightweight_provability_analyzer::LightweightProvabilityAnalyzer,
    function_ids: &[crate::services::lightweight_provability_analyzer::FunctionId],
) -> Result<Vec<ProofSummary>> {
    let summaries = analyzer.analyze_incrementally(function_ids).await;
    use crate::cli::colors as c;
    crate::status_eprintln!(
        "{} Analyzed {} functions",
        c::pass(""),
        c::number(&summaries.len().to_string())
    );
    Ok(summaries)
}

/// Prepare filtered summaries for output (cognitive complexity ≤3)
fn prepare_filtered_summaries(
    summaries: &[ProofSummary],
    high_confidence_only: bool,
) -> Vec<ProofSummary> {
    use crate::cli::provability_helpers::filter_summaries;
    let filtered = filter_summaries(summaries, high_confidence_only);
    filtered.into_iter().cloned().collect()
}

/// Format provability output based on config (cognitive complexity ≤8)
fn format_provability_output(
    function_ids: &[crate::services::lightweight_provability_analyzer::FunctionId],
    summaries: &[ProofSummary],
    config: &ProvabilityConfig,
) -> Result<String> {
    use crate::cli::provability_helpers::{
        format_provability_detailed, format_provability_json, format_provability_markdown,
        format_provability_sarif, format_provability_summary,
    };

    match config.format {
        ProvabilityOutputFormat::Json => {
            format_provability_json(function_ids, summaries, config.include_evidence)
        }
        ProvabilityOutputFormat::Summary => {
            format_provability_summary(function_ids, summaries, config.top_files)
        }
        ProvabilityOutputFormat::Full => {
            format_provability_detailed(function_ids, summaries, config.include_evidence)
        }
        ProvabilityOutputFormat::Sarif => format_provability_sarif(function_ids, summaries),
        // `markdown` used to call `format_provability_detailed` — the terminal
        // renderer — so `-f markdown` and `-f full` produced byte-identical,
        // ANSI-decorated output containing no markdown at all.
        ProvabilityOutputFormat::Markdown => {
            format_provability_markdown(function_ids, summaries, config.include_evidence)
        }
    }
}

/// Write provability output to file or stdout (cognitive complexity ≤4)
async fn write_provability_output(content: &str, output_path: &Option<PathBuf>) -> Result<()> {
    if let Some(output_path) = output_path {
        tokio::fs::write(output_path, content).await?;
        use crate::cli::colors as c;
        crate::status_eprintln!(
            "{} Provability analysis written to: {}",
            c::pass(""),
            c::path(&output_path.display().to_string())
        );
    } else {
        println!("{content}");
    }
    Ok(())
}

/// `analyze provability -p <dir>` must score the same from any working directory.
///
/// Discovery hands the analyzer paths relative to `-p` (that is what the report
/// prints), and the analyzer used to read them back relative to the process
/// cwd. Same binary, same 58,233 functions of the 3.30.0 snapshot: run from
/// inside the project, mean 89.31% over 14 distinct scores; run from `/tmp`,
/// exactly one score — 0.2 — for all 58,233. A 4.5x difference decided by the
/// caller's shell.
///
/// This test runs the handler against a project that is NOT the process cwd,
/// which is the shape the first fix (#754) missed: every test it added ran from
/// inside the tree it analyzed.
#[cfg(test)]
mod provability_is_cwd_independent_tests {
    use super::ProvabilityConfig;
    use crate::cli::enums::ProvabilityOutputFormat;

    /// The probe directory name cannot exist relative to any plausible cwd, so
    /// pre-fix this scored the empty-source baseline deterministically rather
    /// than accidentally reading a same-named file of the *host* repo.
    fn write_probe_project(root: &std::path::Path) {
        let probe = root.join("provability_cwd_probe");
        std::fs::create_dir_all(&probe).unwrap();
        std::fs::write(
            probe.join("pure.rs"),
            "pub fn add(a: i32, b: i32) -> i32 {\n    a + b\n}\n",
        )
        .unwrap();
    }

    #[tokio::test]
    async fn scores_are_evidence_based_when_run_from_another_directory() {
        let dir = tempfile::tempdir().unwrap();
        write_probe_project(dir.path());
        let out = dir.path().join("report.json");

        assert_ne!(
            std::env::current_dir().unwrap().canonicalize().unwrap(),
            dir.path().canonicalize().unwrap(),
            "this test is only meaningful when the cwd is not the analyzed project"
        );

        super::handle_analyze_provability(ProvabilityConfig {
            project_path: dir.path().to_path_buf(),
            functions: vec![],
            analysis_depth: crate::services::lightweight_provability_analyzer::ANALYSIS_DEPTH,
            format: ProvabilityOutputFormat::Json,
            high_confidence_only: false,
            include_evidence: false,
            output: Some(out.clone()),
            top_files: 10,
        })
        .await
        .unwrap();

        let report: serde_json::Value =
            serde_json::from_str(&std::fs::read_to_string(&out).unwrap()).unwrap();
        let results = report["provability_analysis"]["results"]
            .as_array()
            .expect("json report must carry per-function results")
            .clone();
        assert_eq!(
            results.len(),
            1,
            "one function was written, one is expected"
        );

        let score = results[0]["provability_score"].as_f64().unwrap();
        let properties = results[0]["verified_properties"].as_u64().unwrap();
        assert!(
            score > 0.2 && properties > 0,
            "a pure two-line function read from disk scores on evidence; \
             {score} with {properties} properties is the no-evidence baseline, \
             i.e. the source was resolved against the cwd and never opened"
        );
    }
}

/// `analyze provability --quiet` was byte-identical to `analyze provability`.
///
/// On the flag-efficacy gate's ~120-file corpus it wrote 125 bytes of progress
/// to stderr — "🔬 Analyzing function provability…", "📂 Discovering functions
/// in project…", "📊 Found 124 source files", "✓ Analyzed 160 functions" —
/// through unguarded stderr macros here and in the discovery helper. Note that
/// `analysis_utilities/provability.rs`, a *second* copy of the same banners,
/// was already routed; only this path was left, which is why the flag looked
/// half-fixed. The report itself still goes to stdout unconditionally.
#[cfg(test)]
mod provability_quiet_chatter_tests {
    use crate::cli::handlers::bottleneck_handler::quiet_chatter_tests::unguarded_stderr_lines;

    #[test]
    fn provability_progress_obeys_quiet() {
        for (what, source) in [
            ("handler", include_str!("provability_handler_core.rs")),
            (
                "discovery helper",
                include_str!("../provability_helpers_discovery.rs"),
            ),
        ] {
            assert!(
                source.contains("Analyzing function provability")
                    || source.contains("Discovering functions in project"),
                "{what}: the banner this test pins must still exist"
            );
            let leaking = unguarded_stderr_lines(source);
            assert!(
                leaking.is_empty(),
                "{what}: provability's stderr is progress chatter only, so every \
                 line must be suppressible; unguarded: {leaking:?}"
            );
        }
    }
}