docs(campaigns): add 2026-05-26 estate sweep report (human + machine)

.hypatia-ignore

@@ -0,0 +1,2 @@
+hypatia/cicd_rules/banned_language_file:docs/campaigns/2026-05-26/01-triage.ts
+hypatia/security_errors/secret_detected:docs/campaigns/2026-05-26/01-triage.ts

docs/campaigns/2026-05-26.md

@@ -0,0 +1,178 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
+# Estate sweep campaign — 2026-05-26
+
+**Owner**: @hyperpolymath
+**Tracker**: [hyperpolymath/panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32)
+**Tool**: `panic-attack` v2.5.0 built 2026-05-26
+**Scope**: 369-repo estate at `~/developer/repos/`
+**Outcome**: 16 narrow PRs + 1 real-bug fix PR + 35+ tracking issues + 3 upstream bug reports
+
+## Method
+
+Two-session campaign across 5 work tracks:
+
+1. **Track A — FFI / fixture classification PRs**: per-repo `audits/assail-classifications.a2ml` + `audits/audit-*.md` writing a narrow allow-list for legitimate `unsafe` / fixture-context findings. Each PR documents both the rationale and the anti-gameability mechanism (registry is a separate file from the source under scan; new unsafe inside a classified root requires a companion entry + doc edit, both visible in the diff).
+2. **Track B — real-bug remainder**: after Track A's classifications drained ~500 FFI-shaped findings, the genuine code-bug remainder was small. One critical fix landed (`svalinn` JWT signature verification).
+3. **Track C — per-repo tracking issues**: 35+ GitHub issues, one per repo, listing the Critical/High findings by category for human triage. Excludes Track A and Track D-coverage categories.
+4. **Track D / Phase 5 — proof-aware**: ProofDrift findings in 3 proof repos (`echidna`, `tropical-resource-typing`, `standards`) classified as legitimate axioms or detector false positives. **Zero findings required actual proof discharge.**
+5. **Track E — bridge CVE triage**: 24 per-repo CVE tracking issues from `panic-attack bridge triage` (RustSec advisory DB + reachability analysis) across 29 of 58 Rust repos with non-zero advisories.
+
+### Scan pipeline
+
+Initial attempt used `panic-attack assemblyline` (batch-scan a directory of repos) but stalled on a single 7-min repo with `--parallel` enabled. Pivoted to **per-repo `panic-attack assail --headless` with a 90s timeout** so no single repo can block the campaign. 349 of 368 repos scanned cleanly; 19 skipped (content-only, no source). Plus a nested-repo pass for 6 container directories (`a2ml`, `awesome-projects`, `idaptik`, `isers`, `julia-libraries`, `k9`) covering ~90 sub-repos.
+
+### Findings shape (post-scan, before any classification PRs)
+
+| Severity bucket | Count |
+|---|---|
+| Critical/High `UnsafeCode` / `UnsafeFFI` | 497 |
+| Critical/High `SupplyChain` | 398 |
+| Critical/High `UnboundedAllocation` | 516 |
+| Critical/High `DynamicCodeExecution` | 472 |
+| Critical/High `HardcodedSecret` | 122 |
+| Critical/High `CommandInjection` | 113 |
+| Critical/High `UnsafeDeserialization` | 73 |
+| Critical/High `UnsafeTypeCoercion` | 32 |
+| Critical/High `CryptoMisuse` | 28 |
+| Critical/High `ProofDrift` | 219 |
+| Other (Low/Medium) | 2,591 |
+| Already-suppressed | 961 |
+| Worktree-path artefacts (skipped) | 40 |
+| **Actionable this campaign** | **~2,477** |
+
+## Outputs
+
+### Pull requests (17 narrow PRs)
+
+Track A — FFI / fixture classifications:
+
+| Repo | PR | Findings | Pattern |
+|---|---|---|---|
+| `svalinn` | [#11](https://github.com/hyperpolymath/svalinn/pull/11) | 4 | test-context-fixture (JWT decode in bench/tests) |
+| `proven` | [#67](https://github.com/hyperpolymath/proven/pull/67) | 150 | legitimate-FFI (bindings/, ffi/) + protocol-type-identifier + binding-wrapper-naming |
+| `gossamer` | [#54](https://github.com/hyperpolymath/gossamer/pull/54) | 24 | Zig FFI (GTK WebKit) |
+| `docudactyl` | [#20](https://github.com/hyperpolymath/docudactyl/pull/20) | 15 | Zig FFI |
+| `proven-servers` | [#11](https://github.com/hyperpolymath/proven-servers/pull/11) | 10 | bindings/rust FFI |
+| `aerie` | [#35](https://github.com/hyperpolymath/aerie/pull/35) | 10 | Zig FFI |
+| `stapeln` | [#62](https://github.com/hyperpolymath/stapeln/pull/62) | 10 | eBPF + Zig FFI + Ada↔liboqs |
+| `ambientops` | [#102](https://github.com/hyperpolymath/ambientops/pull/102) | 10 | syscall + cross-subproject FFI |
+| `valence-shell` | [#32](https://github.com/hyperpolymath/valence-shell/pull/32) | 8 | POSIX shell job-control libc + Zig FFI |
+| `panll` | [#47](https://github.com/hyperpolymath/panll/pull/47) | 6 | Idris2 Zig FFI + src-gossamer OS-FFI |
+| `linguist` | [#3](https://github.com/hyperpolymath/linguist/pull/3) | 13 | sample-reference-fixture (PA001+PA022) + vendored PCRE |
+| `boj-server` | [#154](https://github.com/hyperpolymath/boj-server/pull/154) | 119 | 117 MCP cartridge_shim + 2 backend FFI (supersedes #153) |
+| `idaptik` | [#98](https://github.com/hyperpolymath/idaptik/pull/98) | 12 | in-game password fixtures (game-content) |
+
+Track D / Phase 5 — proof-aware:
+
+| Repo | PR | Findings | Status |
+|---|---|---|---|
+| `tropical-resource-typing` | [#4](https://github.com/hyperpolymath/tropical-resource-typing/pull/4) | 4 | merged — all PA021 detector false positives (comment-text matches in Isabelle `\<open>...\</close>`) |
+| `echidna` | [#107](https://github.com/hyperpolymath/echidna/pull/107) | 2 | merged — `funext` (HoTT standard axiom) + `Conflicts` (intentional design parameter) |
+| `standards` | [#184](https://github.com/hyperpolymath/standards/pull/184) | 1 file (4 postulates) | open — justified real-analysis postulates per file's own comment |
+
+Track B — real-bug fix:
+
+| Repo | PR / Issue | Type |
+|---|---|---|
+| `svalinn` | [#12](https://github.com/hyperpolymath/svalinn/issues/12), fix [#14](https://github.com/hyperpolymath/svalinn/pull/14) | `Jwt.verifyJwt` now actually verifies signatures via Web Crypto (was failing closed by accident on every call due to a chain of `%raw`-opacity bugs) |
+
+### GitHub issues (62+)
+
+Per-repo Track C tracking issues filed across 35+ repos aggregating ~1,300 Critical/High findings (excluding PA001/PA007 covered by Track A and ProofDrift covered by Track D). Full list in [panic-attack#32](https://github.com/hyperpolymath/panic-attack/issues/32) comment thread.
+
+Track E bridge-triage CVE tracking issues filed across 24 of 29 non-zero-CVE Rust repos. Full list in same tracker.
+
+Track D proof-aware tracking issues filed (then closed as superseded by Track D classification PRs): echidna#105, tropical-resource-typing#3, standards#181.
+
+### Upstream bugs filed against panic-attack itself
+
+- [#33](https://github.com/hyperpolymath/panic-attack/issues/33) — **design**: VeriSimDB hexad persistence (JSON output schema doesn't handle multi-axis well; would enable real `temporal diff` coverage)
+- [#43](https://github.com/hyperpolymath/panic-attack/issues/43) — **bug**: PA021 ProofDrift detector matches `sorry` / `oops` inside Isabelle `\<open>...\</close>` and `@{text ...}` comment antiquotations; Agda/Coq/Idris detectors likely have the same blind spot
+- [#47](https://github.com/hyperpolymath/panic-attack/issues/47) — **bug**: `bridge triage`'s `"Remove unused dependency from Cargo.toml"` action assumes direct dependency but fires on transitive deps (28/28 phantoms in a 6-repo sample were transitive)
+
+### Skipped / blocked
+
+| Repo / scope | Reason |
+|---|---|
+| `polystack` | Archived on GitHub (read-only) — 7 findings unclassified |
+| `hypatia` | Active working tree with 280+ untracked files at session start; deferred to avoid disturbing in-progress work |
+| `linguist` / `rescript` / `HOL` | Forks with issues disabled on GitHub — Track A PRs landed where possible, no Track C tracking issue |
+| `hyperpolymath-archive`, `standards-as-port` | Deleted on GitHub; local copies are orphans |
+| `julia-libraries/*.jl` | Julia chapter closed per project memory; covered only via container-level `julia-ecosystem#6` tracking issue |
+| `ephapax` preservation (`Semantics.v:3327`) | Parked debt per `ephapax-preservation-closure-plan` — not refiled |
+| `boj-server` `SafetyLemmas.idr` (5 `believe_me`) | Parked class-J primitive axioms (3-month dedicated harness) — not refiled |
+| `betlang` `substTop_preserves_typing` | Parked axiom with discharge recipe in betlang PR#27 — not refiled |
+| `agda-stdlib` | Upstream agda/agda-stdlib clone; no `hyperpolymath/` fork — out of scope |
+
+## Discoveries
+
+### `%raw` opacity in ReScript (svalinn)
+
+The most surprising find of the campaign: `svalinn`'s `Jwt.verifyJwt` was reported as a JWT-verify *bypass* on reading the ReScript source, but the compiled JS was actually compile-broken. ReScript's `%raw("decoded.payload")` block referenced a variable `decoded` that the compiler optimised away (it can't see references inside `%raw` strings), so every call threw `ReferenceError`. The catch-block in `AuthMiddleware.authenticateBearerToken` swallowed the error and returned `authenticated: false` — so JWT auth was **fail-closed by accident**, not by signature-skip.
+
+The same `%raw`-opacity pitfall was present in:
+- `base64UrlDecode` (bound `_i`, `%raw` referenced `i` — different variable name in compiled output)
+- `OAuth2.generateState` (`array` var elided across `%raw` boundaries)
+- `OAuth2` module named `URLSearchParams` (compiled to `let URLSearchParams = {}` which shadowed the global constructor → `getAuthorizationUrl` non-functional)
+
+All four bugs were in code that *looked* obviously correct on visual inspection. Lesson: never trust a `%raw` block whose only "use" of a binding is through the `%raw` string — ReScript will silently drop the binding.
+
+PR [`svalinn#14`](https://github.com/hyperpolymath/svalinn/pull/14) fixes all four with proper Web Crypto wiring (`importKey` + `verify` via JWK, signing input built from raw b64 segments via TextEncoder, algorithm allow-list rejecting `none`). 29/29 auth tests now pass (was 17/12 split).
+
+### Transitive-dep misclassification in `bridge triage`
+
+`bridge triage` reports `"Remove unused dependency from Cargo.toml"` as the recommended action for every phantom-classified CVE. Audit across 6 repos found **28/28 phantom packages were transitive** (pulled in by upstream crates, never declared in any local `Cargo.toml`). `cargo update` doesn't drop them because they're already at the latest crates.io version matching the upstream parent's constraint.
+
+Net: Lane 1 of the planned remediation (small no-behaviour-change PRs deleting unused deps) doesn't apply estate-wide. The underlying classification (`informational` + `phantom` = code unreachable) is correct; only the action string is misleading. Filed as panic-attack#47.
+
+### PA021 detector reads docstring text (tropical-resource-typing)
+
+Three of four PA021 ProofDrift findings on `tropical-resource-typing` were the detector counting the literal word `sorry` inside Isabelle `\<open>All proofs are complete — zero @{text sorry}.\</close>` header docstrings. The fourth (`Tropical_Ordinal.thy`) matched `oops` inside a docstring explaining echidna's evaluation handoff (`with \<open>oops\</close> are the ones we want ECHIDNA to evaluate`).
+
+Filed as panic-attack#43. Same blind spot probably affects PA021's Agda/Coq/Idris equivalents (counting `postulate` / `Admitted` / `believe_me` inside Haddock-style docstrings) and warrants a re-audit.
+
+### Mid-campaign correction: file-overwrite mistake
+
+The first `echidna` PR (#107) initially overwrote 14 pre-existing FFI-boundary classification entries on `audits/assail-classifications.a2ml`. The driver script (`file-ffi-pr-v2.sh`) did `cat > audits/assail-classifications.a2ml` without checking for an existing file. Fixed in a follow-up commit on the same branch (`fix: restore pre-existing FFI-boundary classifications`); the PR now sits at 16 entries (14 original + 2 new PA021). Future per-repo classification PRs should `git show origin/main:audits/assail-classifications.a2ml` before truncating.
+
+## Guardrails honoured throughout
+
+- All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`).
+- Base = `main` for every PR — no stacked bases.
+- Auto-merge disabled on every PR (estate-wide auto-merge is banned per project memory).
+- Never `--no-verify` / `--no-gpg-sign`.
+- `features/panic-attacker/` stub dirs in other repos untouched (they reference the canonical tool, not divergent copies).
+- `vcl-ut/_wt-vclut*`, `hypatia/.claude/worktrees/agent-*`, ephapax `_wt-eph-*` worktrees — all untouched (parallel sessions).
+- Parked proof debts (`ephapax`, `betlang`, `boj-server` class-J) — not refiled.
+- Julia chapter closed — no per-`.jl` issues filed; container-level only.
+- `valence-shell`'s stray local `main` commit (workflow hardening, unpushed) preserved by branching from `origin/main` not local `main`.
+- Same defence applied to standards (foreign parallel session on `claude/governance-allowlist-foundation` branch left alone) and panic-attack itself (foreign session on `fix/idris-lang-chapel-not-c` left alone — this campaign-report branch was created from `origin/main`).
+
+## What remains
+
+Owner-side throughput now bounds the campaign:
+
+1. **Review/merge the 15 open PRs** — all narrow, signed, small surface area.
+2. **Triage the Track C tracking issues** (~1,300 findings) — separate real bugs from false-positive patterns per repo.
+3. **Decide on the 3 upstream panic-attack bugs** filed (#33 design, #43 detector, #47 bridge action).
+
+Deferred to follow-up sessions:
+
+- **hypatia** classification PR — re-attempt once the active session's untracked files have committed or cleared.
+- **polystack** — owner action to unarchive on GitHub before any work can land.
+- **Track E `assault`** — heavyweight per-target work (each binary needs build + manually-chosen long-running input). Not estate-wide automatable. Smoke-tested on `panic-attack` self-binary (light intensity, 5s/axis, cpu+memory): 0 crashes, 0 signatures, 100% robustness — as expected for a fast-exit CLI.
+
+## Campaign workspace
+
+Preserved at `/tmp/panic-attack-campaign-2026-05-26/`:
+
+- `per-repo/*.json` (349 assail reports, one per repo)
+- `bridge/*.json` (58 Rust-repo bridge reports)
+- `02-plan.json` (triage classification plan)
+- `assault/self-test.json` (Track E smoke test)
+- `00-per-repo.sh`, `00b-nested.sh`, `01-triage.ts`, `file-ffi-pr-v2.sh`, `file-track-c-issue.sh` (driver scripts)
+- `TRACKER-UPDATE.md` ... `TRACKER-UPDATE-V5.md` (intermediate session summaries posted on #32)

docs/campaigns/2026-05-26/00-per-repo.sh

@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+# Per-repo assail loop with timeout. No single repo can stall the campaign.
+set -uo pipefail
+
+ESTATE="${ESTATE:-/home/hyperpolymath/developer/repos}"
+CAMP="${CAMP:-/tmp/panic-attack-campaign-2026-05-26}"
+BIN="${BIN:-$ESTATE/panic-attack/target/release/panic-attack}"
+TIMEOUT="${TIMEOUT:-90}"
+PER_REPO="$CAMP/per-repo"
+LOG="$CAMP/00-per-repo.log"
+DONE_FILE="$CAMP/00-per-repo-done.txt"
+SKIPPED_FILE="$CAMP/00-per-repo-skipped.txt"
+
+mkdir -p "$PER_REPO"
+: > "$LOG"
+: > "$DONE_FILE"
+: > "$SKIPPED_FILE"
+
+echo "=== per-repo assail $(date -u --iso=seconds) timeout=${TIMEOUT}s ===" | tee -a "$LOG"
+
+# Build repo list: top-level dirs with .git/ as a directory
+REPOS=()
+for d in "$ESTATE"/*; do
+  [ -d "$d/.git" ] || continue
+  REPOS+=("$d")
+done
+TOTAL=${#REPOS[@]}
+echo "estate: $TOTAL repos" | tee -a "$LOG"
+
+I=0
+for repo in "${REPOS[@]}"; do
+  I=$((I + 1))
+  name=$(basename "$repo")
+  # Skip the canonical tool repo (we don't audit ourselves here)
+  if [ "$name" = "panic-attack" ]; then
+    echo "[$I/$TOTAL] $name — SKIP (canonical tool)" | tee -a "$LOG"
+    continue
+  fi
+  out="$PER_REPO/${name}.json"
+  start=$SECONDS
+  if timeout "${TIMEOUT}s" "$BIN" assail "$repo" --headless --output "$out" >/dev/null 2>&1; then
+    dur=$((SECONDS - start))
+    findings=$(jq '.weak_points | length' "$out" 2>/dev/null || echo "?")
+    crit=$(jq '[.weak_points[] | select(.severity == "Critical")] | length' "$out" 2>/dev/null || echo "?")
+    high=$(jq '[.weak_points[] | select(.severity == "High")] | length' "$out" 2>/dev/null || echo "?")
+    echo "[$I/$TOTAL] $name ✓ ${dur}s findings=$findings crit=$crit high=$high" | tee -a "$LOG"
+    echo "$name" >> "$DONE_FILE"
+  else
+    dur=$((SECONDS - start))
+    echo "[$I/$TOTAL] $name ✗ TIMEOUT(${dur}s)" | tee -a "$LOG"
+    echo "$name" >> "$SKIPPED_FILE"
+    rm -f "$out"
+  fi
+done
+
+echo "=== pass complete $(date -u --iso=seconds) ===" | tee -a "$LOG"
+echo "done: $(wc -l < "$DONE_FILE")" | tee -a "$LOG"
+echo "skipped: $(wc -l < "$SKIPPED_FILE")" | tee -a "$LOG"

docs/campaigns/2026-05-26/00b-nested.sh

@@ -0,0 +1,80 @@
+#!/usr/bin/env bash
+# Pass 1b: per-repo assail loop for NESTED sub-repos and peer locations
+# Picks up everything the top-level walker missed.
+set -uo pipefail
+
+CAMP="${CAMP:-/tmp/panic-attack-campaign-2026-05-26}"
+BIN="${BIN:-/home/hyperpolymath/developer/repos/panic-attack/target/release/panic-attack}"
+TIMEOUT="${TIMEOUT:-90}"
+PER_REPO="$CAMP/per-repo"
+LOG="$CAMP/00b-nested.log"
+DONE_FILE="$CAMP/00b-nested-done.txt"
+SKIPPED_FILE="$CAMP/00b-nested-skipped.txt"
+
+mkdir -p "$PER_REPO"
+: > "$LOG"
+: > "$DONE_FILE"
+: > "$SKIPPED_FILE"
+
+echo "=== nested-repo assail $(date -u --iso=seconds) timeout=${TIMEOUT}s ===" | tee -a "$LOG"
+
+# Container dirs: scan their direct children that have .git/
+CONTAINERS=(
+  /home/hyperpolymath/developer/repos/a2ml
+  /home/hyperpolymath/developer/repos/awesome-projects
+  /home/hyperpolymath/developer/repos/idaptik
+  /home/hyperpolymath/developer/repos/isers
+  /home/hyperpolymath/developer/repos/julia-libraries
+  /home/hyperpolymath/developer/repos/k9
+)
+# Peer locations: scan top-level + 1 level deep
+PEERS=(
+  /home/hyperpolymath/typed-wasm-final
+  /home/hyperpolymath/ephapax-fix
+)
+
+REPOS=()
+for parent in "${CONTAINERS[@]}"; do
+  for d in "$parent"/*; do
+    [ -d "$d/.git" ] && REPOS+=("$d")
+  done
+done
+for peer in "${PEERS[@]}"; do
+  [ -d "$peer/.git" ] && REPOS+=("$peer")
+  if [ -d "$peer" ]; then
+    for d in "$peer"/*; do
+      [ -d "$d/.git" ] && REPOS+=("$d")
+    done
+  fi
+done
+
+TOTAL=${#REPOS[@]}
+echo "nested + peers: $TOTAL repos" | tee -a "$LOG"
+
+I=0
+for repo in "${REPOS[@]}"; do
+  I=$((I + 1))
+  # Use parent/child slug to avoid name collisions
+  parent=$(basename "$(dirname "$repo")")
+  child=$(basename "$repo")
+  name="${parent}__${child}"
+  out="$PER_REPO/${name}.json"
+  start=$SECONDS
+  if timeout "${TIMEOUT}s" "$BIN" assail "$repo" --headless --output "$out" >/dev/null 2>&1; then
+    dur=$((SECONDS - start))
+    findings=$(jq '.weak_points | length' "$out" 2>/dev/null || echo "?")
+    crit=$(jq '[.weak_points[] | select(.severity == "Critical")] | length' "$out" 2>/dev/null || echo "?")
+    high=$(jq '[.weak_points[] | select(.severity == "High")] | length' "$out" 2>/dev/null || echo "?")
+    echo "[$I/$TOTAL] $name ✓ ${dur}s findings=$findings crit=$crit high=$high" | tee -a "$LOG"
+    echo "$name" >> "$DONE_FILE"
+  else
+    dur=$((SECONDS - start))
+    echo "[$I/$TOTAL] $name ✗ TIMEOUT/EARLY-EXIT(${dur}s)" | tee -a "$LOG"
+    echo "$name" >> "$SKIPPED_FILE"
+    rm -f "$out"
+  fi
+done
+
+echo "=== nested pass complete $(date -u --iso=seconds) ===" | tee -a "$LOG"
+echo "done: $(wc -l < "$DONE_FILE")" | tee -a "$LOG"
+echo "skipped: $(wc -l < "$SKIPPED_FILE")" | tee -a "$LOG"