From 9ec6f252a624abcf4fe4058f9e3fc061c91c7372 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:15:14 +0000 Subject: [PATCH 1/2] test(corpus): mark the two deliberate sorry fixtures as accepted detector inputs isabelle/Smoke.thy and minif2f/algebra.lean each keep one `sorry` on purpose: corpus_hazard_fixtures asserts the adapters flag it. panic-attack reports both as Critical ProofDrift, which is the last thing failing the static analysis gate once the scanner can complete coverage (#478). An inline `panic-attack: accepted` marker on the line above each sorry records the audit beside the evidence and suppresses only that occurrence; any other sorry in either file still fails the gate. The markers take effect with the line-anchored findings in hyperpolymath/panic-attack#278; with the current scanner they are inert comments. Checked with a build of that branch, scanned from another directory: both findings are suppressed at Smoke.thy:21 and algebra.lean:11, and static-analysis-evidence.sh scan + gate pass (critical 0, total 109). Both corpus_hazard_fixtures tests and the five corpus_estate_adapters tests still pass with the annotated files. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- tests/corpus_fixtures/isabelle/Smoke.thy | 1 + tests/corpus_fixtures/minif2f/algebra.lean | 1 + 2 files changed, 2 insertions(+) diff --git a/tests/corpus_fixtures/isabelle/Smoke.thy b/tests/corpus_fixtures/isabelle/Smoke.thy index 5537af2d..c3fb88e7 100644 --- a/tests/corpus_fixtures/isabelle/Smoke.thy +++ b/tests/corpus_fixtures/isabelle/Smoke.thy @@ -17,6 +17,7 @@ theorem double_zero: "double 0 = 0" (* A lemma left open with `sorry` — the corpus adapter must flag this as a sorry hazard. *) lemma double_mono: "n \ m \ double n \ double m" + (* panic-attack: accepted (detector fixture: the corpus adapter must flag this sorry) *) sorry (* An axiomatization block — the adapter must flag the postulate hazard. *) diff --git a/tests/corpus_fixtures/minif2f/algebra.lean b/tests/corpus_fixtures/minif2f/algebra.lean index be3b1918..a7d0f9fc 100644 --- a/tests/corpus_fixtures/minif2f/algebra.lean +++ b/tests/corpus_fixtures/minif2f/algebra.lean @@ -7,4 +7,5 @@ theorem mathd_algebra_171 (a b : ℝ) (h₀ : a + b = 10) (h₁ : a - b = 4) : a linarith theorem imo_1959_p1 (n : ℕ) (h : 0 < n) : Nat.gcd (21 * n + 4) (14 * n + 3) = 1 := by + -- panic-attack: accepted (detector fixture: the corpus adapter must flag this sorry) sorry From 11f8c3178a25a3068ed1d478a7ee95e18ac7189a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:35:50 +0000 Subject: [PATCH 2/2] test(corpus): keep the detector token out of the fixture markers' rationale Codex review (P2): both corpus adapters flag a hazard with a plain `text.contains("sorry")` over the declaration, comments included. The marker rationale said "...must flag this sorry", so the marker alone set axiom_usage.sorry: with the real `sorry` replaced by a finished proof, corpus_hazard_fixtures still passed, i.e. the fixture stopped testing anything. The rationale now reads "...must flag the unfinished proof below", which contains none of the adapters' hazard tokens (sorry, oops, admit, Admitted, axiom, axiomatization, consts, nitpick, quickcheck). Checked: with the real sorry present, corpus_hazard_fixtures passes (2/2); with it replaced by a finished proof, both tests fail on "hazard classification" (previously both still passed). panic-attack built from hyperpolymath/panic-attack#278 still suppresses both findings at Smoke.thy:21 and algebra.lean:11. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- tests/corpus_fixtures/isabelle/Smoke.thy | 2 +- tests/corpus_fixtures/minif2f/algebra.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/corpus_fixtures/isabelle/Smoke.thy b/tests/corpus_fixtures/isabelle/Smoke.thy index c3fb88e7..72b95075 100644 --- a/tests/corpus_fixtures/isabelle/Smoke.thy +++ b/tests/corpus_fixtures/isabelle/Smoke.thy @@ -17,7 +17,7 @@ theorem double_zero: "double 0 = 0" (* A lemma left open with `sorry` — the corpus adapter must flag this as a sorry hazard. *) lemma double_mono: "n \ m \ double n \ double m" - (* panic-attack: accepted (detector fixture: the corpus adapter must flag this sorry) *) + (* panic-attack: accepted (detector fixture: the corpus adapter must flag the unfinished proof below) *) sorry (* An axiomatization block — the adapter must flag the postulate hazard. *) diff --git a/tests/corpus_fixtures/minif2f/algebra.lean b/tests/corpus_fixtures/minif2f/algebra.lean index a7d0f9fc..bf6a8a55 100644 --- a/tests/corpus_fixtures/minif2f/algebra.lean +++ b/tests/corpus_fixtures/minif2f/algebra.lean @@ -7,5 +7,5 @@ theorem mathd_algebra_171 (a b : ℝ) (h₀ : a + b = 10) (h₁ : a - b = 4) : a linarith theorem imo_1959_p1 (n : ℕ) (h : 0 < n) : Nat.gcd (21 * n + 4) (14 * n + 3) = 1 := by - -- panic-attack: accepted (detector fixture: the corpus adapter must flag this sorry) + -- panic-attack: accepted (detector fixture: the corpus adapter must flag the unfinished proof below) sorry