From c0a104ac5b6517196b20378ef87fa42a939783e9 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 24 Jun 2026 10:33:40 +0100 Subject: [PATCH] test(aggregate): add ideal Idris2 proof fixture + end-to-end fold test aggregate folds external prover output (incl. Idris2) but had NO proof fixture and no end-to-end fold test (only annotation/spec unit tests). proven has Idris2 files, but they are library property-tests, not detector-soundness proofs in aggregate's shape. Adds tests/fixtures/proofs/UnsafeCodeSoundness.idr: a genuine idris2 --check clean, %default total proof (no escape hatches) of the UnsafeCode (PA001) detector's soundness AND completeness, carrying the @name and @covers sound:category:UnsafeCode annotations aggregate reads. And tests/aggregate_proof_fixture.rs: folds it via aggregate::run and asserts it is recognised as Idris2, classified Closed (no holes), hashed, named, and that the coverage parses to Sound/Category/UnsafeCode. Co-Authored-By: Claude Opus 4.8 --- tests/aggregate_proof_fixture.rs | 71 +++++++++++++++++++ tests/fixtures/proofs/UnsafeCodeSoundness.idr | 55 ++++++++++++++ 2 files changed, 126 insertions(+) create mode 100644 tests/aggregate_proof_fixture.rs create mode 100644 tests/fixtures/proofs/UnsafeCodeSoundness.idr diff --git a/tests/aggregate_proof_fixture.rs b/tests/aggregate_proof_fixture.rs new file mode 100644 index 0000000..e06638f --- /dev/null +++ b/tests/aggregate_proof_fixture.rs @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +//! 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 + ); +} diff --git a/tests/fixtures/proofs/UnsafeCodeSoundness.idr b/tests/fixtures/proofs/UnsafeCodeSoundness.idr new file mode 100644 index 0000000..409ad10 --- /dev/null +++ b/tests/fixtures/proofs/UnsafeCodeSoundness.idr @@ -0,0 +1,55 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- @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