pmat 3.30.1

// Formatting functions: JSON output, table output, summary output, annotator setup, and annotation collection.

/// Format proof annotations as JSON
///
/// DETERMINISM (round-3 sweep): this document is a pure function of the
/// analysed tree. Two wall-clock fields used to make that false, so five runs
/// over an unchanged tree produced five different md5 sums even after the entry
/// order and the `annotationId`s were made stable:
///
/// * per-annotation `dateVerified` — 1298 copies of one `Utc::now()`. That is
///   one measurement of the RUN, not 1298 measurements of the code, and it is
///   now reported once on stderr by the handler instead of 1298 times in the
///   document.
/// * `summary.analysis_time_ms` — how long this machine took, under whatever
///   load it happened to be under. Also reported on stderr.
///
/// Both are still shown to the operator; neither is a property of the input, so
/// neither belongs in the artifact a baseline is diffed against.
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn format_as_json(
    annotations: &[(Location, ProofAnnotation)],
    _elapsed: std::time::Duration,
    annotator: &ProofAnnotator,
) -> Result<String> {
    let cache_stats = annotator.cache_stats();
    let annotations_json: Vec<serde_json::Value> = annotations
        .iter()
        .map(|(location, annotation)| {
            let mut rendered = serde_json::to_value(annotation).unwrap_or_else(
                |_| serde_json::json!({ "error": "annotation could not be serialized" }),
            );
            if let Some(obj) = rendered.as_object_mut() {
                obj.remove("dateVerified");
            }
            serde_json::json!({
                "location": {
                    "file_path": location.file_path.to_string_lossy(),
                    "start_pos": location.span.start.0,
                    "end_pos": location.span.end.0
                },
                "annotation": rendered
            })
        })
        .collect();

    // COMPLETENESS: files the collector could not read or parse contribute no
    // annotations, and their failure used to stop at one `warn!` line on
    // stderr. The document then reported a total with nothing to say it was
    // computed over a subset — 31 unparsed files on this repo, invisible to
    // anything consuming the JSON. Reported here so a consumer can tell a
    // complete analysis from a partial one.
    let files_not_analyzed = annotator.collection_errors();

    let json_data = serde_json::json!({
        "proof_annotations": annotations_json,
        "summary": {
            "total_annotations": annotations.len(),
            "files_not_analyzed": files_not_analyzed,
            "cache_stats": {
                "size": cache_stats.size,
                "files_tracked": cache_stats.files_tracked
            }
        }
    });

    serde_json::to_string_pretty(&json_data).map_err(Into::into)
}

/// Setup the proof annotator with the real proof source.
///
/// This used to register three `MockProofSource`s -- a TEST DOUBLE -- in the
/// production path. Its own doc comment said "with mock sources". The mock
/// ignores the project path entirely and synthesises `count` annotations
/// against invented filenames, so `analyze proof-annotations` emitted exactly
/// 5 + 3 + 2 = 10 annotations naming borrow_checker_0.rs, static_analyzer_1.rs
/// and friends -- files that exist nowhere on disk -- for ANY path, including
/// a nonexistent one, each stamped with a fresh UUID and a current-time
/// `dateVerified`. That is machine-readable fabricated evidence of formal
/// verification, which is the most damaging thing this tool could emit.
///
/// `RustBorrowChecker` is a real, default-feature-enabled `ProofSource` that
/// walks the project and derives annotations from parsed source. It existed
/// the whole time with zero callers.
///
/// See contracts/pmat-no-fabrication-v1.yaml, `output_derived_from_input`.
///
/// # `--clear-cache`
///
/// `ProofAnnotator`'s cache is a `HashMap` inside `ProofAnnotator` with no load
/// and no save path (`src/services/proof_annotator_cache.rs` touches the
/// filesystem only for `metadata()`), so it starts empty in every process. The
/// old body called `annotator.clear_cache()` on an annotator constructed one
/// line earlier — clearing an always-empty map before any work — which is why
/// `--clear-cache` produced byte-identical output under every format including
/// the JSON one that prints `cache_stats`.
///
/// There is nothing persistent to delete, so the flag says so instead of
/// pantomiming a clear: a no-op that looks like an action is the defect.
#[must_use]
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn setup_proof_annotator(clear_cache: bool) -> ProofAnnotator {
    use crate::services::{rust_borrow_checker::RustBorrowChecker, symbol_table::SymbolTable};

    let symbol_table = std::sync::Arc::new(SymbolTable::new());
    let mut annotator = ProofAnnotator::new(symbol_table);

    if clear_cache {
        eprintln!(
            "🧹 --clear-cache: pmat keeps no proof-annotation cache between runs — the cache \
             lives in this process only and starts empty, so every annotation below was \
             re-derived from source regardless of this flag"
        );
    }

    annotator.add_source(RustBorrowChecker::default());

    annotator
}

/// Filter and collect proof annotations
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "path_exists")]
pub async fn collect_and_filter_annotations(
    annotator: &ProofAnnotator,
    project_path: &Path,
    filter: &ProofAnnotationFilter,
) -> Vec<(Location, ProofAnnotation)> {
    let proof_map = annotator.collect_proofs(project_path).await;

    let mut collected: Vec<(Location, ProofAnnotation)> = proof_map
        .into_iter()
        .flat_map(|(location, annotations)| {
            annotations
                .into_iter()
                .filter(|annotation| filter_annotation(annotation, filter))
                .map(|annotation| (location.clone(), annotation))
                .collect::<Vec<_>>()
        })
        .collect();

    // DETERMINISM (round-3 sweep): `ProofMap` is a `HashMap<Location, ...>`, so
    // this vector came out in a per-process random order and every renderer
    // inherited it — 5 runs of `analyze proof-annotations --format json` over
    // an unchanged tree produced 5 different orderings of the same 1298
    // annotations (run 1 started at `name_similarity_help…`, run 2 at
    // `satd_formatting.rs`, run 3 at `tdg_handler_analysis…`). The content was
    // identical as a SET every time, which is precisely why the ordering was
    // the only thing making the output undiffable.
    //
    // Sorted by source position first, then by what is asserted there, so the
    // key is total: no two annotations at one site assert the same property by
    // the same method (that is also what `annotation_id` is derived from).
    collected.sort_by(|(la, aa), (lb, ab)| {
        la.file_path
            .cmp(&lb.file_path)
            .then_with(|| la.span.start.0.cmp(&lb.span.start.0))
            .then_with(|| la.span.end.0.cmp(&lb.span.end.0))
            .then_with(|| {
                format!("{:?}", aa.property_proven).cmp(&format!("{:?}", ab.property_proven))
            })
            .then_with(|| format!("{:?}", aa.method).cmp(&format!("{:?}", ab.method)))
            .then_with(|| aa.specification_id.cmp(&ab.specification_id))
            .then_with(|| aa.annotation_id.cmp(&ab.annotation_id))
    });

    collected
}

/// The disclosure appended to every human-readable report when the collector
/// skipped files.
///
/// `None` when nothing was skipped, so a complete run reads exactly as before.
/// The JSON document carries the same fact as `summary.files_not_analyzed`.
#[must_use]
pub fn incomplete_analysis_note(files_not_analyzed: usize) -> Option<String> {
    if files_not_analyzed == 0 {
        return None;
    }
    Some(format!(
        "\nINCOMPLETE: {files_not_analyzed} file(s) could not be read or parsed and \
         contributed no annotations. The totals above are computed over the rest.\n"
    ))
}

/// Format annotations as table output
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn format_as_table(
    annotations: &[(Location, ProofAnnotation)],
    _elapsed: std::time::Duration,
) -> Result<String> {
    use std::fmt::Write;
    let mut output = String::new();

    writeln!(
        &mut output,
        "| File | Position | Property | Method | Confidence |"
    )?;
    writeln!(
        &mut output,
        "|------|----------|----------|---------|------------|"
    )?;

    for (location, annotation) in annotations {
        writeln!(
            &mut output,
            "| {} | {}-{} | {:?} | {:?} | {:?} |",
            location
                .file_path
                .file_name()
                .unwrap_or_default()
                .to_string_lossy(),
            location.span.start.0,
            location.span.end.0,
            annotation.property_proven,
            annotation.method,
            annotation.confidence_level
        )?;
    }

    Ok(output)
}

/// Format annotations as summary output
#[provable_contracts_macros::contract("pmat-core.yaml", equation = "check_compliance")]
pub fn format_as_summary(
    annotations: &[(Location, ProofAnnotation)],
    elapsed: std::time::Duration,
    top_files: usize,
) -> Result<String> {
    let mut output = String::new();

    format_summary_header(&mut output, annotations, elapsed)?;
    format_summary_property_counts(&mut output, annotations)?;
    format_summary_top_files(&mut output, annotations, top_files)?;

    Ok(output)
}

fn format_summary_header(
    output: &mut String,
    annotations: &[(Location, ProofAnnotation)],
    elapsed: std::time::Duration,
) -> Result<()> {
    use std::fmt::Write;

    let total_proofs = annotations.len();
    let high_confidence = annotations
        .iter()
        .filter(|(_, ann)| matches!(ann.confidence_level, ConfidenceLevel::High))
        .count();

    writeln!(output, "Proof Annotations Summary:")?;
    writeln!(output, "Total proofs: {total_proofs}\n")?;
    writeln!(
        output,
        "High confidence: {} ({:.1}%)",
        high_confidence,
        if total_proofs > 0 {
            (high_confidence as f64 / total_proofs as f64) * 100.0
        } else {
            0.0
        }
    )?;
    writeln!(output, "Analysis time: {:.2}s\n", elapsed.as_secs_f64())?;

    Ok(())
}

fn format_summary_property_counts(
    output: &mut String,
    annotations: &[(Location, ProofAnnotation)],
) -> Result<()> {
    use std::fmt::Write;

    // DETERMINISM: a `BTreeMap`, not a `HashMap`. `--format summary` listed the
    // same property counts in a different order on every run, for the same
    // reason the JSON entry order moved: nothing sorted them.
    let mut property_counts = std::collections::BTreeMap::new();
    for (_, ann) in annotations {
        let key = format!("{:?}", ann.property_proven);
        *property_counts.entry(key).or_insert(0) += 1;
    }

    if !property_counts.is_empty() {
        writeln!(output, "\nProofs by property type:")?;
        for (prop_type, count) in property_counts {
            writeln!(output, "  {prop_type}: {count}")?;
        }
    }

    Ok(())
}

fn format_summary_top_files(
    output: &mut String,
    annotations: &[(Location, ProofAnnotation)],
    top_files: usize,
) -> Result<()> {
    use std::fmt::Write;

    if annotations.is_empty() {
        return Ok(());
    }

    writeln!(output, "\n## Top Files with Proof Annotations\n")?;

    let mut file_counts: std::collections::HashMap<&std::path::Path, usize> =
        std::collections::HashMap::new();
    for (location, _) in annotations {
        *file_counts.entry(&location.file_path).or_insert(0) += 1;
    }

    // DETERMINISM: the count alone is not a total order — most files tie — and
    // the input is a `HashMap`, so `.take(10)` picked whichever tied files the
    // hash seed visited first. Path breaks the tie.
    let mut sorted_files: Vec<_> = file_counts.into_iter().collect();
    sorted_files.sort_by(|a, b| b.1.cmp(&a.1).then_with(|| a.0.cmp(b.0)));

    // Print the whole path, not `file_name()`: a repo has many `build.rs` and
    // `mod.rs` files, so a basename-only list rendered ten *distinct* files as
    // two basenames repeated five times each, with no way to tell them apart.
    //
    // The row count is `--top-files`, not a hardcoded 10: over an 84-file
    // corpus `--top-files 1` and `--top-files 50` both printed exactly ten
    // rows, because the flag never reached this loop.
    for (i, (file_path, count)) in crate::cli::top_files_slice(&sorted_files, top_files)
        .iter()
        .enumerate()
    {
        writeln!(
            output,
            "{}. `{}` - {} annotations",
            i + 1,
            file_path.display(),
            count
        )?;
    }

    Ok(())
}

#[cfg_attr(coverage_nightly, coverage(off))]
#[cfg(test)]
mod top_files_path_tests {
    use super::*;
    use crate::models::unified_ast::{BytePos, EvidenceType, Span};
    use chrono::Utc;
    use std::path::PathBuf;
    use uuid::Uuid;

    fn entry(path: &str) -> (Location, ProofAnnotation) {
        (
            Location {
                file_path: PathBuf::from(path),
                span: Span {
                    start: BytePos(0),
                    end: BytePos(1),
                },
            },
            ProofAnnotation {
                annotation_id: Uuid::nil(),
                property_proven: PropertyType::MemorySafety,
                specification_id: None,
                method: VerificationMethod::BorrowChecker,
                tool_name: "test".to_string(),
                tool_version: "1.0".to_string(),
                confidence_level: ConfidenceLevel::High,
                assumptions: vec![],
                evidence_type: EvidenceType::ImplicitTypeSystemGuarantee,
                evidence_location: None,
                date_verified: Utc::now(),
            },
        )
    }

    /// Distinct files that share a basename must render as distinct lines. The
    /// list used to print `file_name()` only, so a repo's many `build.rs` files
    /// collapsed into the same label repeated over and over.
    #[test]
    fn top_files_distinguishes_same_basename_in_different_directories() {
        let annotations = vec![
            entry("/repo/a/build.rs"),
            entry("/repo/a/build.rs"),
            entry("/repo/b/build.rs"),
        ];

        let mut out = String::new();
        format_summary_top_files(&mut out, &annotations, 10).unwrap();

        assert!(
            out.contains("/repo/a/build.rs"),
            "expected full path in top-files list, got:\n{out}"
        );
        assert!(
            out.contains("/repo/b/build.rs"),
            "expected full path in top-files list, got:\n{out}"
        );
        let lines: Vec<&str> = out.lines().filter(|l| l.contains("build.rs")).collect();
        assert_eq!(lines.len(), 2, "two distinct files, two distinct lines");
        assert_ne!(lines[0], lines[1], "lines must not be identical labels");
    }

    /// The row count is `--top-files`, not the literal 10 this loop used to
    /// carry. Over an 84-file corpus `analyze proof-annotations --top-files 1`
    /// and `--top-files 50` both printed exactly ten rows, because the route
    /// bound the flag to `_top_files` and dropped it.
    #[test]
    fn top_files_sets_the_row_count() {
        let annotations: Vec<_> = (0..24)
            .map(|i| entry(&format!("/repo/f{i:02}.rs")))
            .collect();

        let rows = |top_files: usize| {
            let mut out = String::new();
            format_summary_top_files(&mut out, &annotations, top_files).expect("render");
            out.lines().filter(|l| l.contains("annotations")).count()
        };

        assert_eq!(rows(1), 1, "--top-files 1 must list one file");
        assert_eq!(rows(10), 10, "--top-files 10 must list ten files");
        assert_eq!(rows(50), 24, "a limit above the total lists every file");
        assert_eq!(rows(0), 24, "--top-files 0 means all");
    }
}