You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Mechanical sweep to catch up active docs and config after the
2026-02-08 binary rename (`panic-attacker` → `panic-attack`,
`xray` → `assail`, `XRayReport` → `AssailReport`) and the v2.5.0
release. Active prose, install commands, and config still referenced
the old names; some counts had not been refreshed since v2.1/v2.3.
### Mass rename `panic-attacker` → `panic-attack`
20 files: DESIGN.md, VISION.md, CONTRIBUTING.md, SECURITY.md,
QUICKSTART-{USER,DEV,MAINTAINER}.adoc, llm-warmup-{dev,user}.md,
PROOF-NEEDS.md, TEST-NEEDS.md, FUTURE-IMPROVEMENTS.md,
docs/json-schema.md, docs/007-FALSE-POSITIVE-GUIDANCE.md,
docs/mass-panic-fnirs-paper.adoc, docs/HYPATIA-RULE-UPDATES.md,
.github/workflows/{mirror,scan-and-report}.yml, stapeln.toml,
k9iser.toml.
Intentional exclusions (historical record):
* `CHANGELOG.md` — rename entry is the historical record itself
* `.claude/CLAUDE.md` — rename block is intentionally preserved
* `docs/reports/audit/*` — dated audit snapshots, frozen-in-time
### File rename
* `panic-attacker.toml.example` → `panic-attack.toml.example`
(config template's own header already instructed "copy to
panic-attack.toml")
### Critical CI fixes
* `.github/workflows/mirror.yml:15` — `if: github.repository ==
'hyperpolymath/panic-attacker'` was a dead guard (repo renamed);
workflow had silently been a no-op since 2026-02-08.
* `.github/workflows/scan-and-report.yml:35` — `cargo install --git
https://github.com/hyperpolymath/panic-attacker --branch main` would
404 against the renamed repo on the next install attempt.
### Stale-fact refresh
* `TOPOLOGY.md:93,97` — 282 tests → 400+ tests; v2.3.0 → v2.5.0
* `k9iser.toml:22` — LICENSE comment PMPL → MPL-2.0 (Cargo.toml
contract on line 19 already encodes `package.name == 'panic-attack'`)
* `PROOF-NEEDS.md:14` — 47 `Lang` constructors → 49 (matches
PatternCompleteness.idr's own line 24 and the README)
* `src/abi/PatternCompleteness.idr:21` — inline comment "47 variants"
→ "49 variants" (file's docstring on line 24 already said 49)
* `READINESS.md:16` — add Isabelle to dogfood-tested language list
* `ROADMAP.adoc:29` — drop stale "(Next)" qualifier on v2.1.0
section (all checkboxes ticked; v2.5.0 is current)
### Verified
* `cargo check` — clean
* `cargo fmt --check` — clean
* Diff is symmetric (+86/-86) — no semantic drift, just renames
### Not in this PR (separate concerns)
* README.adoc — open PR #35 already fixes the OpenSSF link, license
badge, version, and counts; deliberately not touched here to avoid
conflict.
* ROADMAP.adoc structural refresh — sections v2.1-v2.5 use checkbox
history correctly; only the "(Next)" label was stale. Deeper
re-organisation would be a separate doc PR.
* Proof-drift between `src/types.rs` (has `Chapel`, no `C`) and
`src/abi/PatternCompleteness.idr` (has `C`, no `Chapel`) — both
enumerate 49 constructors but disagree on which 49. Out of scope
for docs hygiene; filing as a separate proof-drift issue.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Copy file name to clipboardExpand all lines: PROOF-NEEDS.md
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,4 +1,4 @@
1
-
# PROOF-NEEDS.md — panic-attacker
1
+
# PROOF-NEEDS.md — panic-attack
2
2
3
3
## Current State
4
4
@@ -11,7 +11,7 @@
11
11
12
12
| Proof | File | What it proves |
13
13
|-------|------|---------------|
14
-
| PA1 Pattern detection completeness |`src/abi/PatternCompleteness.idr`| All 47`Lang` constructors have an analyzer; all 20 `WPCategory` constructors have at least one detector; cross-language checks applied unconditionally to all languages. `completeScanForAll` is the top-level theorem. |
14
+
| PA1 Pattern detection completeness |`src/abi/PatternCompleteness.idr`| All 49`Lang` constructors have an analyzer; all 20 `WPCategory` constructors have at least one detector; cross-language checks applied unconditionally to all languages. `completeScanForAll` is the top-level theorem. |
15
15
| PA2 Classification soundness |`src/abi/ClassificationSoundness.idr`| Severity (Low/Medium/High/Critical) is totally ordered (`LTE`); `maxSeverity` is commutative and idempotent; numeric ABI encoding preserves the ordering. |
0 commit comments