test(aggregate): ideal Idris2 proof fixture + end-to-end fold test

tests/aggregate_proof_fixture.rs

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//! End-to-end fixture test for `aggregate`'s prover-output folding.
+//!
+//! `aggregate` has unit tests for annotation/spec parsing, but no test that
+//! folds a *real* prover artifact end to end. This exercises that path against
+//! `tests/fixtures/proofs/UnsafeCodeSoundness.idr` — a genuine, `idris2
+//! --check`-clean, `%default total` Idris2 proof (no escape hatches) of the
+//! UnsafeCode (PA001) detector's soundness, carrying the `@name` / `@covers`
+//! annotations the folder reads. It asserts the artifact is recognised as
+//! Idris2, classified `Closed` (no holes), hashed, named, and that the
+//! `sound:category:UnsafeCode` coverage is parsed.
+
+use panic_attack::aggregate::{
+    run, AggregateConfig, CoverageKind, ProofClaim, ProofInput, ProofVerdict, Prover,
+};
+use std::path::PathBuf;
+
+fn fixture() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("tests/fixtures/proofs/UnsafeCodeSoundness.idr")
+}
+
+#[test]
+fn aggregate_folds_idris2_unsafecode_soundness_proof() {
+    let path = fixture();
+    assert!(path.exists(), "fixture missing: {}", path.display());
+
+    let report = run(AggregateConfig {
+        proofs: vec![ProofInput {
+            path,
+            label: None,
+            covers: Vec::new(),
+        }],
+        base_report: None,
+    })
+    .expect("aggregate should fold the Idris2 fixture");
+
+    assert_eq!(report.aggregated_proofs.len(), 1);
+    let p = &report.aggregated_proofs[0];
+
+    // Recognised as an Idris2 artifact (by `.idr` extension).
+    assert!(matches!(p.prover, Prover::Idris2), "prover: {:?}", p.prover);
+
+    // No escape hatches + a closure signal => Closed (not Holes / Indeterminate).
+    assert!(
+        matches!(p.verdict, ProofVerdict::Closed),
+        "verdict: {:?}, holes: {:?}",
+        p.verdict,
+        p.holes
+    );
+    assert!(p.holes.is_empty(), "unexpected holes: {:?}", p.holes);
+
+    // Non-repudiation: the whole file was hashed (byte length recorded).
+    assert!(p.bytes > 0, "no bytes hashed");
+
+    // Friendly name lifted from the in-file `@name "..."` annotation.
+    assert!(
+        p.friendly_name.contains("UnsafeCode"),
+        "friendly name: {}",
+        p.friendly_name
+    );
+
+    // Coverage parsed from `@covers sound:category:UnsafeCode`.
+    assert!(
+        p.covers.iter().any(|c| matches!(c.claim, ProofClaim::Sound)
+            && matches!(c.kind, CoverageKind::Category)
+            && c.value == "UnsafeCode"),
+        "covers: {:?}",
+        p.covers
+    );
+}

tests/fixtures/proofs/UnsafeCodeSoundness.idr

@@ -0,0 +1,55 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-- @name "UnsafeCode detector soundness (Idris2)"
+-- @covers sound:category:UnsafeCode
+|||
+||| A closed Idris2 soundness witness for panic-attack's UnsafeCode (PA001)
+||| detector, in the exact shape `panic-attack aggregate` folds: no escape
+||| hatches, a total proof that a positive detection is backed by a genuine
+||| occurrence -- the detector raises no UnsafeCode finding on a token stream
+||| that contains no unsafe construct (no false positives).
+|||
+||| `aggregate` records this artifact by BLAKE3 hash and does NOT re-check it;
+||| the recorded verdict is conditioned on the Idris2 checker, whose input this
+||| file is. The `@covers sound:category:UnsafeCode` annotation marks any
+||| overlapping UnsafeCode finding in a base report as proof-Backed.
+module UnsafeCodeSoundness
+
+%default total
+
+||| A scanned token: ordinary code, or an unsafe construct (e.g. a Rust
+||| `unsafe` block) -- the minimal model the UnsafeCode detector reasons over.
+public export
+data Tok = Ordinary | Unsafe
+
+||| The detector under study: positive on the first unsafe construct seen.
+||| Structurally the per-file first-hit scan the real analyzer performs.
+public export
+detect : List Tok -> Bool
+detect []               = False
+detect (Unsafe   :: _)  = True
+detect (Ordinary :: ts) = detect ts
+
+||| A structural witness that an `Unsafe` token genuinely occurs in the stream.
+public export
+data Occurs : List Tok -> Type where
+  Here  : Occurs (Unsafe :: ts)
+  There : Occurs ts -> Occurs (x :: ts)
+
+||| SOUNDNESS (no false positives): every positive detection is backed by a
+||| real `Unsafe` occurrence -- exactly the `sound` claim that `aggregate`
+||| reconciles as `Backed` against an overlapping UnsafeCode finding.
+export
+detectSound : (ts : List Tok) -> detect ts = True -> Occurs ts
+detectSound (Unsafe   :: _)  _   = Here
+detectSound (Ordinary :: ts) prf = There (detectSound ts prf)
+detectSound []               prf = absurd prf
+
+||| COMPLETENESS (no false negatives): a real occurrence forces a positive
+||| detection. Together with `detectSound` this pins detection as exactly
+||| "an unsafe construct occurs", with no hidden gap in either direction.
+export
+detectComplete : (ts : List Tok) -> Occurs ts -> detect ts = True
+detectComplete (Unsafe   :: _)  Here      = Refl
+detectComplete (Unsafe   :: _)  (There _) = Refl
+detectComplete (Ordinary :: ts) (There o) = detectComplete ts o