From 28990d42a9873e7af833051f6a9f2ce84e4901bb Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 19:32:06 +0000 Subject: [PATCH] fix(audits): drop the 2 fixture entries that inline markers now cover #489 added registry entries for the deliberate `sorry` in tests/corpus_fixtures/isabelle/Smoke.thy and tests/corpus_fixtures/minif2f/algebra.lean, because the gate's scanner (panic-attack f2a6a70) could not apply the inline `panic-attack: accepted` markers those files already carry. #497 moved the gate to panic-attack 55ffcc9, which line-anchors Lean and Isabelle `sorry` findings (panic-attack#278), so the markers suppress them. The entries are now a second suppression for the same 2 lines, and they cover every ProofDrift finding in the 2 files, not only the marked line. This removes them; the file returns to its state before #489. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude --- audits/assail-classifications.a2ml | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index 92b5f806..d3dc7030 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -172,20 +172,4 @@ 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")) - )