From fc137c086493a47b33f592fcc579a5930bf286e5 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 17:30:41 +0000 Subject: [PATCH] fix(audits): classify the two deliberate corpus-fixture sorrys The Static Analysis Gate on main fails with "Critical scanner findings block merge". Coverage is complete with the pinned panic-attack; the only criticals are two PA021 ProofDrift findings, one open `sorry` each in tests/corpus_fixtures/isabelle/Smoke.thy and tests/corpus_fixtures/minif2f/algebra.lean. Both are deliberate test inputs: tests/corpus_hazard_fixtures.rs asserts that the corpus adapters flag them as sorry hazards, so removing them would break those tests. Record them in the panic-attack classification registry, which suppresses exactly these file and category pairs. No existing entry changes. Checked with panic-attack main (4f51cca, --features http): assail exits 0 with coverage complete 913/913 and 0 unsuppressed critical findings. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0136P7ZnmBahbhfkFEP6ark4 --- audits/assail-classifications.a2ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index d3dc7030..92b5f806 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -172,4 +172,20 @@ schema_version = "1.0.0" (audit "audits/audit-ffi-boundary.adoc §11") (rationale "Single @ptrCast at line 333 in echidna_typell_last_error(): identical pattern to boj.zig and overlay.zig — module-static error_buf [N]u8 → [*:0]const u8 with null-fast-path guard")) + ; ─── PA021 ProofDrift, deliberate corpus-adapter test fixtures ────────── + ; Each fixture holds one open `sorry` on purpose: the corpus adapters must + ; flag it as a hazard, and the tests below fail if it is removed. These + ; files are test inputs, not proofs ECHIDNA relies on. + (classification + (file "tests/corpus_fixtures/isabelle/Smoke.thy") + (category "ProofDrift") + (audit "tests/corpus_hazard_fixtures.rs isabelle_fixture_keeps_incomplete_proofs_unqualified") + (rationale "Deliberate open `sorry` in lemma double_mono; the test asserts the Isabelle adapter marks it as a sorry hazard")) + + (classification + (file "tests/corpus_fixtures/minif2f/algebra.lean") + (category "ProofDrift") + (audit "tests/corpus_hazard_fixtures.rs minif2f_fixture_keeps_incomplete_proofs_unqualified") + (rationale "Deliberate open `sorry` in imo_1959_p1; the test asserts the MiniF2F adapter marks it as a sorry hazard")) + )