From 889a21ad7637cfed6ee2bc436907b4a3bbe92513 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:01:33 +0000 Subject: [PATCH 1/5] fix(ci): pin panic-attack f2a6a70 so the static analysis scan can complete The pinned scanner 410a8f8 classified 190 config and markup inputs (toml, yml, json, html, css, Containerfiles, Justfile, one F# file) as "unsupported", so coverage was "partial" (718/908) and --fail-on-incomplete exited 2 before any finding was counted. The gate therefore failed on every commit for a reason unrelated to the code. f2a6a70 includes the configuration/build input coverage repair (panic-attack#258): 913/913 inputs analysed here, exit 0, and the report qualifies under the existing panic-attack contract. The same range moved the Patch Bridge report to schema 0.3.0, which adds vulnerability_data (queried | offline-unavailable | no-dependencies). The qualifier now requires 0.3.0 with vulnerability_data == "queried": a zero-CVE report that never reached the feed is not a clean result. Receipt controls: the bridge mock moves to 0.3.0; new controls reject an offline report (paired with an otherwise identical queried report that qualifies) and a stale 0.2.0 report. 34 controls pass; the mutants drop-feed-check, back-to-0.2.0 and accept-any-feed are each killed. Known after this change: the gate still fails, now on its real finding. It reports 2 Critical ProofDrift findings, the deliberate `sorry` detector fixtures in tests/corpus_fixtures/{isabelle/Smoke.thy,minif2f/algebra.lean}. Clearing those is a separate change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- .github/workflows/static-analysis-gate.yml | 9 +++++++-- scripts/ci/static-analysis-evidence.sh | 2 +- scripts/ci/test-static-analysis-evidence.sh | 11 ++++++++++- 3 files changed, 18 insertions(+), 4 deletions(-) diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index a33b0240..8414a119 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -15,9 +15,14 @@ permissions: contents: read env: # Exact Hypatia repair canary: Agda keyword boundaries and patched dependencies. - # The panic-attack pin remains the standards-vetted source pending coverage repair. + # panic-attack runs ahead of the standards-vetted 410a8f8 (hypatia-scan-reusable + # default) because that commit cannot report complete coverage for this tree: + # 190 config/markup inputs were "unsupported", so --fail-on-incomplete exited 2 + # before any finding was counted. f2a6a70 includes the coverage repair + # (panic-attack#258: 913/913 inputs here) and Patch Bridge schema 0.3.0 + # (vulnerability_data), which the qualifier below checks. HYPATIA_REF: 82396d81677b11d17c7a0dede5bf0efcf768d5a1 - PANIC_ATTACK_REF: 410a8f821ea8297833162565b50a298f787815da + PANIC_ATTACK_REF: f2a6a70eaec0cb02331e3264e05f185b5faab0f7 SCAN_EXPECTED_SHA: ${{ github.event.pull_request.head.sha || github.sha }} jobs: panic-attack-assail: diff --git a/scripts/ci/static-analysis-evidence.sh b/scripts/ci/static-analysis-evidence.sh index 41041c5c..49f43fff 100755 --- a/scripts/ci/static-analysis-evidence.sh +++ b/scripts/ci/static-analysis-evidence.sh @@ -34,7 +34,7 @@ valid_report() { and (.weak_points | type == "array") and all(.weak_points[]; type == "object" and (.severity as $s | ["Critical","High","Medium","Low"] | index($s) != null)))' "$report" >/dev/null 2>&1 ;; patch-bridge) - jq -e -s 'length == 1 and (.[0] | type == "object" and .schema_version == "0.2.0" + jq -e -s 'length == 1 and (.[0] | type == "object" and .schema_version == "0.3.0" and .vulnerability_data == "queried" and (.total_dependencies | type == "number" and . > 0 and floor == .) and (.cves | type == "array") and all(.cves[]; type == "object" and (.classification as $c | diff --git a/scripts/ci/test-static-analysis-evidence.sh b/scripts/ci/test-static-analysis-evidence.sh index e2accf98..309a020c 100755 --- a/scripts/ci/test-static-analysis-evidence.sh +++ b/scripts/ci/test-static-analysis-evidence.sh @@ -135,7 +135,7 @@ expect_exit 2 panic # Bridge needs its real subcommand and output-file contract. CLI/parser errors # cannot turn into a fabricated zero-CVE report; no offline zero is requested. -printf '%s\n' '{"schema_version":"0.2.0","total_dependencies":2,"vulnerable_dependencies":1,"cves":[{"classification":"unmitigable"}],"mitigated":0,"unmitigable":1,"concatenative":0,"informational":0}' > "$MOCK_REPORT" +printf '%s\n' '{"schema_version":"0.3.0","vulnerability_data":"queried","total_dependencies":2,"vulnerable_dependencies":1,"cves":[{"classification":"unmitigable"}],"mitigated":0,"unmitigable":1,"concatenative":0,"informational":0}' > "$MOCK_REPORT" expect_exit 0 bridge grep -Fxq bridge "$MOCK_ARGS" grep -Fxq triage "$MOCK_ARGS" @@ -148,6 +148,15 @@ export MOCK_EXIT=0 jq '.unmitigable = 0' "$MOCK_REPORT" > "$tmp/inconsistent.json" cp "$tmp/inconsistent.json" "$MOCK_REPORT" expect_exit 2 bridge +# A report that never reached the vulnerability feed is not a zero-CVE result. +# Paired: the same zero-CVE report qualifies only when the feed was queried. +printf '%s\n' '{"schema_version":"0.3.0","vulnerability_data":"queried","total_dependencies":2,"vulnerable_dependencies":0,"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$MOCK_REPORT" +expect_exit 0 bridge +printf '%s\n' '{"schema_version":"0.3.0","vulnerability_data":"offline-unavailable","total_dependencies":2,"vulnerable_dependencies":0,"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$MOCK_REPORT" +expect_exit 2 bridge +# The pre-0.3.0 contract has no feed status, so it cannot qualify either. +printf '%s\n' '{"schema_version":"0.2.0","total_dependencies":2,"vulnerable_dependencies":1,"cves":[{"classification":"unmitigable"}],"mitigated":0,"unmitigable":1,"concatenative":0,"informational":0}' > "$MOCK_REPORT" +expect_exit 2 bridge # Deposit preserves actual critical findings even though their gate failed. # Only mutually matching completed scan receipts may create the legacy artifact. From bec79696b1d903a764997d2da9feebf069030abc Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:14:15 +0000 Subject: [PATCH 2/5] test(ci): reject a feed-less 0.3.0 bridge report and gate the clean receipt The controls added in the previous commit let a qualifier that rejects only `offline-unavailable` through: a 0.3.0 report with no vulnerability_data at all still qualified (mutant reject-only-offline survived). Add that negative control, and pass the queried zero-CVE receipt through the gate so a gate that rejects clean receipts is caught too. 36 receipt controls pass. Mutants reject-only-offline, drop-feed-check, accept-any-feed and back-to-0.2.0 are each killed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- scripts/ci/test-static-analysis-evidence.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/ci/test-static-analysis-evidence.sh b/scripts/ci/test-static-analysis-evidence.sh index 309a020c..07b5f20b 100755 --- a/scripts/ci/test-static-analysis-evidence.sh +++ b/scripts/ci/test-static-analysis-evidence.sh @@ -152,8 +152,12 @@ expect_exit 2 bridge # Paired: the same zero-CVE report qualifies only when the feed was queried. printf '%s\n' '{"schema_version":"0.3.0","vulnerability_data":"queried","total_dependencies":2,"vulnerable_dependencies":0,"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$MOCK_REPORT" expect_exit 0 bridge +expect_exit 0 bash "$adapter" gate "$tmp/bridge/receipt.json" printf '%s\n' '{"schema_version":"0.3.0","vulnerability_data":"offline-unavailable","total_dependencies":2,"vulnerable_dependencies":0,"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$MOCK_REPORT" expect_exit 2 bridge +# A 0.3.0 report with no feed status at all must not qualify either. +printf '%s\n' '{"schema_version":"0.3.0","total_dependencies":2,"vulnerable_dependencies":0,"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$MOCK_REPORT" +expect_exit 2 bridge # The pre-0.3.0 contract has no feed status, so it cannot qualify either. printf '%s\n' '{"schema_version":"0.2.0","total_dependencies":2,"vulnerable_dependencies":1,"cves":[{"classification":"unmitigable"}],"mitigated":0,"unmitigable":1,"concatenative":0,"informational":0}' > "$MOCK_REPORT" expect_exit 2 bridge From a792534efeb5d8b8d057760f287aaa5c3f758020 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:42:18 +0000 Subject: [PATCH 3/5] fix(deps): rmcp 3.5.0 -> 3.9.0 for RUSTSEC-2026-0457/-0461/-0462 Dependency audit fails on main and every PR: rmcp 3.5.0 (crates/echidna-mcp) has three advisories, the newest published 2026-11-05. Ported from hyperpolymath/echidna#465 (also carried by #473); Cargo.lock is byte-identical to both, so whichever merges first leaves the others a no-op. scripts/ci/audit-dependencies.sh (cargo-audit 0.22.2): both lockfiles PASSED. cargo check -p echidna-mcp --locked: passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- Cargo.lock | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0bf91e23..0592b0e7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -133,7 +133,7 @@ version = "1.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -144,7 +144,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d" dependencies = [ "anstyle", "once_cell_polyfill", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -640,7 +640,7 @@ version = "3.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "faf9468729b8cbcea668e36183cb69d317348c2e08e994829fb56ebfdfbaac34" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -1246,7 +1246,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb" dependencies = [ "libc", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -2093,7 +2093,7 @@ version = "0.50.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5" dependencies = [ - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -2837,20 +2837,22 @@ dependencies = [ [[package]] name = "rmcp" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fae7019994ae0fe4ada40b732f798f3ff26f0f04facb1477f1bf37eb4f18a2d3" +checksum = "d24a7e92f4bcaa36b97fa93c4fa7ca8f3e669eced949345b3462dba333c7f909" dependencies = [ "base64 0.23.1", "chrono", "futures", "indexmap", + "libc", "pastey", "pin-project-lite", "rmcp-macros", "schemars", "serde", "serde_json", + "sha2 0.11.0", "thiserror", "tokio", "tokio-util", @@ -2860,9 +2862,9 @@ dependencies = [ [[package]] name = "rmcp-macros" -version = "3.5.0" +version = "3.9.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7e66877136e969d5a2d561ee5841b17717a0619aebd64abb47a2a2f46e34683" +checksum = "b3140f24a766f80f9ec1607bde85680959a69b83d46fa9ce87dadab7e67ab029" dependencies = [ "darling 0.24.0", "proc-macro2", @@ -2910,7 +2912,7 @@ dependencies = [ "errno", "libc", "linux-raw-sys", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -3251,7 +3253,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "52d1cfed4120b4d927bf7c0f86d2087a4a7d6027c906d9f9d525a80573b9be51" dependencies = [ "libc", - "windows-sys 0.60.2", + "windows-sys 0.61.2", ] [[package]] @@ -3391,10 +3393,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd" dependencies = [ "fastrand", - "getrandom 0.4.2", + "getrandom 0.3.4", "once_cell", "rustix", - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] @@ -4198,7 +4200,7 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.61.2", ] [[package]] From 42f3c884c6ca7d42c8d3c7fb09fc79861b1bf5d1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:24:18 +0000 Subject: [PATCH 4/5] fix(ci): reasoned inline hypatia allows on the nine Zig callback casts (port of #465) governance / Validate Hypatia Baseline fails on main and so here: Hypatia reports code_safety/zig_ptr_cast and zig_align_cast (high) on the nine `@ptrCast(@alignCast(raw))` lines in src/zig_ffi/. Each cast recovers a callback's own *@This() from the type-erased *anyopaque it was registered with, so type and alignment are the original ones. Ported from hyperpolymath/echidna#465 (f48fe0a), comments only, no baseline entry; both files are byte-identical to #465's and #473's. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb --- src/zig_ffi/chapel_bridge.zig | 15 ++++++++++----- src/zig_ffi/runtime_owner.zig | 12 ++++++++---- 2 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/zig_ffi/chapel_bridge.zig b/src/zig_ffi/chapel_bridge.zig index 807c23fe..f8d12591 100644 --- a/src/zig_ffi/chapel_bridge.zig +++ b/src/zig_ffi/chapel_bridge.zig @@ -70,7 +70,8 @@ fn callOnOwner(owner: anytype, comptime function: anytype, args: anytype, result result: @TypeOf(result), fn run(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.result.* = @call(.auto, function, self.arguments); } }; @@ -650,7 +651,8 @@ const CallerAllocator = struct { } fn alloc(raw: *anyopaque, len: usize, alignment: std.mem.Alignment, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds if (!self.record() or self.allocations >= self.fail_after) return null; const pointer = std.heap.c_allocator.rawAlloc(len, alignment, ret_addr) orelse return null; self.allocations += 1; @@ -659,7 +661,8 @@ const CallerAllocator = struct { } fn resize(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) bool { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -669,7 +672,8 @@ const CallerAllocator = struct { } fn remap(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, new_len: usize, ret_addr: usize) ?[*]u8 { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); _ = memory; _ = alignment; @@ -679,7 +683,8 @@ const CallerAllocator = struct { } fn free(raw: *anyopaque, memory: []u8, alignment: std.mem.Alignment, ret_addr: usize) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds _ = self.record(); // The backing allocator is cross-thread safe so a failed assertion // never requires corrupting memory or leaking the test allocation. diff --git a/src/zig_ffi/runtime_owner.zig b/src/zig_ffi/runtime_owner.zig index 79d9d543..da2f1b8a 100644 --- a/src/zig_ffi/runtime_owner.zig +++ b/src/zig_ffi/runtime_owner.zig @@ -169,7 +169,8 @@ const Probe = struct { } fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.wrong_thread = self.wrong_thread or self.init_id != std.Thread.getCurrentId(); self.calls += 1; } @@ -239,7 +240,8 @@ test "shutdown drains accepted work and refuses new work before joining" { shutdown_failed: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast(); @@ -311,7 +313,8 @@ test "owner callbacks cannot re-enter or finalize themselves" { stop_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds var nested = Work{ .context = self.probe, .run = Probe.work }; self.call_refused = if (self.owner.call(&nested)) |_| false else |err| err == error.ReentrantCall; self.stop_refused = if (self.owner.shutdown()) |_| false else |err| err == error.ReentrantCall; @@ -358,7 +361,8 @@ test "a nonowner process-exit request refuses active work without a join cycle" exit_refused: bool = false, fn work(raw: *anyopaque) void { - const self: *@This() = @ptrCast(@alignCast(raw)); + // hypatia: allow code_safety/zig_ptr_cast -- raw is the type-erased *@This() this callback was registered with + const self: *@This() = @ptrCast(@alignCast(raw)); // hypatia: allow code_safety/zig_align_cast -- same pointer, so @This() alignment holds self.mutex.lock(); self.entered = true; self.changed.broadcast(); From c63cff9f9295b0ae23a585a81e00dd2c623af14a Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 9 Nov 2026 23:03:35 +0000 Subject: [PATCH 5/5] test(corpus): mark the two deliberate sorry fixtures as accepted detector inputs (#480) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Stacked on #478. With #478 the static analysis scan completes. Its only remaining Critical findings are the two deliberate `sorry` fixtures that `tests/corpus_hazard_fixtures.rs` uses to check that the adapters flag unfinished proofs. This PR records that audit as an inline `panic-attack: accepted` marker beside each one. The owner chose this over a gate exemption list. A marker suppresses only the occurrence it sits above, so a real `sorry` added later to either file still fails the gate. **Waits on hyperpolymath/panic-attack#278**, which line-anchors these findings so a marker can apply. Under the current scanner the markers are inert comments. Once #278 merges I will move `PANIC_ATTACK_REF` to the merged commit in this PR. ## Changes - `tests/corpus_fixtures/isabelle/Smoke.thy`: `(* panic-attack: accepted (detector fixture: …) *)` above the `sorry` in `double_mono`. - `tests/corpus_fixtures/minif2f/algebra.lean`: `-- panic-attack: accepted (detector fixture: …)` above the `sorry` in `imo_1959_p1`. - *(pending #278)*: `PANIC_ATTACK_REF` in `.github/workflows/static-analysis-gate.yml`. ## RSR Quality Checklist ### Required - [x] Tests pass: `cargo test --test corpus_hazard_fixtures --test corpus_estate_adapters` gives 2 + 5 passed with the annotated files - [x] Code is formatted (comment lines only) - [x] Linter is clean - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments (none touched) - [x] No banned functions introduced. The two `sorry` lines pre-exist and are deliberate detector inputs, now marked as such. - [x] SPDX license headers present (unchanged) - [x] No secrets, credentials, or `.env` files included ### As Applicable - n/a. ## Testing Run locally with a release build of panic-attack#278 (`--features http`), against echidna `main` with these exact two edits (byte-identical): | Check | Result | |---|---| | `assail --fail-on-incomplete`, run from `/tmp` | exit 0; `Smoke.thy:21` and `algebra.lean:11` both `suppressed: true`; 0 unsuppressed Critical | | `static-analysis-evidence.sh scan panic-attack` + `gate` | `status: ran`, exit 0, `critical: 0`, total 109 (111 minus the two fixtures); gate exit 0 | | `corpus_hazard_fixtures` | 2 passed: both adapters still flag their `sorry` | | `corpus_estate_adapters` | 5 passed | --- _Generated by [Claude Code](https://claude.ai/code/session_01JHfuPCv1pEiqkQGG5DQASb)_ --------- Co-authored-by: Claude --- 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..72b95075 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 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 be3b1918..bf6a8a55 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 the unfinished proof below) sorry