From b0586d17063b571195571342887b0c2011bb760f Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 13:56:54 +0100
Subject: [PATCH 1/4] chore(ci): grant `actions: read` across all workflows
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Recovers the un-upstreamed half of local commit c655117 (2026-07-26), which
never reached origin/main.

`actions: read` lets a job read workflow/run metadata via the API. Several
gates need it — the staleness check reads run history, and CodeQL reads
workflow definitions when scanning the `actions` language. Widening a *caller*
grant is always safe: the startup_failure trap is a REUSABLE requesting more
than its caller grants, never the reverse.

Deliberately NOT carried over from c655117:

  - `.github/funding.yml` — a sweeper artefact. Lowercase (GitHub reads
    `FUNDING.yml`), no SPDX header, and it names `metadatastician` while the
    real `.github/FUNDING.yml` already present names `hyperpolymath` across
    github/ko_fi/liberapay. Adding it would have put a second, wrong funding
    file in the repo.

Also dropped from that local branch entirely: commit 5a5301d, which pinned
github/codeql-action to 29b1f65c1f735799893313399435a59f54045865 — a SHA that
DOES NOT EXIST (HTTP 404 from both the commits and git/commits endpoints).
origin/main already carries a real, newer pin. Landing 5a5301d would have made
CodeQL unable to resolve the action.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/TagBot.yml               | 1 +
 .github/workflows/agda.yml                 | 1 +
 .github/workflows/boj-build.yml            | 1 +
 .github/workflows/codeql.yml               | 1 +
 .github/workflows/container-build.yml      | 1 +
 .github/workflows/dependabot-automerge.yml | 1 +
 .github/workflows/dogfood-gate.yml         | 1 +
 .github/workflows/e2e.yml                  | 1 +
 .github/workflows/governance.yml           | 1 +
 .github/workflows/hypatia-scan.yml         | 1 +
 .github/workflows/install-smoke.yml        | 1 +
 .github/workflows/instant-sync.yml         | 1 +
 .github/workflows/mirror.yml               | 1 +
 .github/workflows/pages.yml                | 1 +
 .github/workflows/push-email-notify.yml    | 1 +
 .github/workflows/release.yml              | 1 +
 .github/workflows/scorecard.yml            | 1 +
 .github/workflows/secret-scanner.yml       | 1 +
 .github/workflows/zig.yml                  | 1 +
 19 files changed, 19 insertions(+)

diff --git a/.github/workflows/TagBot.yml b/.github/workflows/TagBot.yml
index dfde769..36fa2f2 100644
--- a/.github/workflows/TagBot.yml
+++ b/.github/workflows/TagBot.yml
@@ -26,6 +26,7 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
index 4531d8b..ad4dbfc 100644
--- a/.github/workflows/agda.yml
+++ b/.github/workflows/agda.yml
@@ -22,6 +22,7 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 concurrency:
diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
index e796d25..428759a 100644
--- a/.github/workflows/boj-build.yml
+++ b/.github/workflows/boj-build.yml
@@ -6,6 +6,7 @@ on:
     branches: [main, master]
   workflow_dispatch:
 permissions:
+  actions: read
   contents: read
 jobs:
   trigger-boj:
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
index ec97ec0..19a6f2a 100644
--- a/.github/workflows/codeql.yml
+++ b/.github/workflows/codeql.yml
@@ -16,6 +16,7 @@ concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 permissions:
+  actions: read
   contents: read
 jobs:
   analyze:
diff --git a/.github/workflows/container-build.yml b/.github/workflows/container-build.yml
index ef425c0..f568eee 100644
--- a/.github/workflows/container-build.yml
+++ b/.github/workflows/container-build.yml
@@ -30,6 +30,7 @@ on:
   workflow_dispatch:
 
 permissions: read-all
+  actions: read
 
 concurrency:
   group: container-build-${{ github.ref }}
diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml
index 4464081..ef4efeb 100644
--- a/.github/workflows/dependabot-automerge.yml
+++ b/.github/workflows/dependabot-automerge.yml
@@ -40,6 +40,7 @@ on:
   pull_request:
     types: [opened, reopened, synchronize]
 permissions:
+  actions: read
   contents: write # needed to enable auto-merge
   pull-requests: write # needed to approve
   # NB: keep narrow — do NOT add secrets: read or id-token: write here.
diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml
index 8e3a6bb..04f6171 100644
--- a/.github/workflows/dogfood-gate.yml
+++ b/.github/workflows/dogfood-gate.yml
@@ -13,6 +13,7 @@ on:
     branches: [main, master]
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 8c657aa..0698994 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -20,6 +20,7 @@ on:
   workflow_dispatch:
 
 permissions: read-all
+  actions: read
 
 concurrency:
   group: e2e-${{ github.ref }}
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
index 8776de0..966a16e 100644
--- a/.github/workflows/governance.yml
+++ b/.github/workflows/governance.yml
@@ -9,6 +9,7 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
index 5eeee3c..ae59369 100644
--- a/.github/workflows/hypatia-scan.yml
+++ b/.github/workflows/hypatia-scan.yml
@@ -14,6 +14,7 @@ on:
 # `security-events: write` to upload its SARIF, so the job below raises it
 # explicitly (same pattern as scorecard.yml).
 permissions:
+  actions: read
   contents: read
   security-events: write
 
diff --git a/.github/workflows/install-smoke.yml b/.github/workflows/install-smoke.yml
index 148e62e..14221e8 100644
--- a/.github/workflows/install-smoke.yml
+++ b/.github/workflows/install-smoke.yml
@@ -23,6 +23,7 @@ on:
   workflow_dispatch:
 
 permissions: read-all
+  actions: read
 
 concurrency:
   group: install-smoke-${{ github.ref }}
diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml
index a718d56..a98e2b1 100644
--- a/.github/workflows/instant-sync.yml
+++ b/.github/workflows/instant-sync.yml
@@ -10,6 +10,7 @@ on:
     types: [published]
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index 13ca1bd..9357e25 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -8,6 +8,7 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
index b14bddd..e1f3dde 100644
--- a/.github/workflows/pages.yml
+++ b/.github/workflows/pages.yml
@@ -6,6 +6,7 @@ on:
     branches: [main, master]
   workflow_dispatch:
 permissions:
+  actions: read
   contents: read
   pages: write
   id-token: write
diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml
index 2a95f5d..c08ea16 100644
--- a/.github/workflows/push-email-notify.yml
+++ b/.github/workflows/push-email-notify.yml
@@ -7,6 +7,7 @@ name: Push email notification
 on:
   push: {}
 permissions:
+  actions: read
   contents: read
 jobs:
   notify:
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index a97320e..3fa13d5 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -33,6 +33,7 @@ on:
         type: string
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
index b97e2cb..cede40a 100644
--- a/.github/workflows/scorecard.yml
+++ b/.github/workflows/scorecard.yml
@@ -9,6 +9,7 @@ on:
   workflow_dispatch:
 
 permissions:
+  actions: read
   contents: read
 
 jobs:
diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml
index 8262804..6d1906c 100644
--- a/.github/workflows/secret-scanner.yml
+++ b/.github/workflows/secret-scanner.yml
@@ -14,6 +14,7 @@ concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
 permissions:
+  actions: read
   contents: read
 jobs:
   trufflehog:
diff --git a/.github/workflows/zig.yml b/.github/workflows/zig.yml
index 0a65d9f..9ae2c47 100644
--- a/.github/workflows/zig.yml
+++ b/.github/workflows/zig.yml
@@ -24,6 +24,7 @@ on:
   workflow_dispatch:
 
 permissions: read-all
+  actions: read
 
 concurrency:
   group: zig-${{ github.ref }}

From be2f8b890264404833267acb8cefcdf3e0b03a90 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 13:57:37 +0100
Subject: [PATCH 2/4] docs(ci): stop asserting stale test counts in the e2e
 header
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The header claimed "693 @test assertions, 10 Agda proofs, 8 integrations".
Measured on this tree: 1129 `@test` occurrences under test/ and 3 Agda modules
(Inequalities, RankIdentities, TropicalSemiring). Wrong in both directions —
it undercounted the tests by 63% and overcounted the proofs 3x.

Replacing it with a corrected count would be wrong again on the next commit
that adds a test, so the header now describes what the job does and points at
the job's own output as the authoritative source. A comment that has to be
manually resynced to stay true is a comment that will drift.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/e2e.yml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 0698994..2fd946b 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -3,7 +3,13 @@
 #
 # Statistikles — E2E + Aspect Tests
 #
-# Runs the Julia test suite (693 @test assertions, 10 Agda proofs, 8 integrations).
+# Runs the Julia test suite, then the Agda proof gate.
+#
+# Counts are deliberately NOT stated here. The previous header claimed
+# "693 @test assertions, 10 Agda proofs, 8 integrations"; measured on this tree
+# it is 1129 `@test` occurrences under test/ and 3 Agda modules under proofs/ —
+# wrong in both directions, and wrong again on the next commit that adds a test.
+# The authoritative counts are whatever this job prints when it runs.
 
 name: E2E + Aspect
 

From 12ba5843f780f6bbda91f28aa07a5a25f3495ed7 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 13:58:21 +0100
Subject: [PATCH 3/4] fix(ci): don't append `actions: read` under scalar
 `permissions: read-all`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The previous commit recovered a sweep that inserted `actions: read` after every
`permissions:` line. Four workflows declare permissions in the SCALAR form:

    permissions: read-all

Hanging a mapping key under a scalar is invalid YAML, so the sweep produced:

    permissions: read-all
      actions: read      # <-- "mapping values are not allowed here"

Actions rejects a malformed workflow at PARSE time, which means zero jobs and
NO CHECK RUN AT ALL — not a red X. `gh pr checks` shows nothing amiss while the
gate silently ceases to exist. Affected: zig.yml, e2e.yml, container-build.yml,
install-smoke.yml — i.e. the Zig FFI gate, the Julia test suite, the container
build and the install smoke test. Four of the repo's most load-bearing gates.

The insertion was redundant anyway: `read-all` already grants every read scope,
including `actions: read`. The sweep matched `permissions:` as text, not as a
YAML node, so it could not tell the two forms apart.

Verified: all 19 workflows now parse under yaml.safe_load.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/container-build.yml | 1 -
 .github/workflows/e2e.yml             | 1 -
 .github/workflows/install-smoke.yml   | 1 -
 .github/workflows/zig.yml             | 1 -
 4 files changed, 4 deletions(-)

diff --git a/.github/workflows/container-build.yml b/.github/workflows/container-build.yml
index f568eee..ef425c0 100644
--- a/.github/workflows/container-build.yml
+++ b/.github/workflows/container-build.yml
@@ -30,7 +30,6 @@ on:
   workflow_dispatch:
 
 permissions: read-all
-  actions: read
 
 concurrency:
   group: container-build-${{ github.ref }}
diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml
index 2fd946b..3b41276 100644
--- a/.github/workflows/e2e.yml
+++ b/.github/workflows/e2e.yml
@@ -26,7 +26,6 @@ on:
   workflow_dispatch:
 
 permissions: read-all
-  actions: read
 
 concurrency:
   group: e2e-${{ github.ref }}
diff --git a/.github/workflows/install-smoke.yml b/.github/workflows/install-smoke.yml
index 14221e8..148e62e 100644
--- a/.github/workflows/install-smoke.yml
+++ b/.github/workflows/install-smoke.yml
@@ -23,7 +23,6 @@ on:
   workflow_dispatch:
 
 permissions: read-all
-  actions: read
 
 concurrency:
   group: install-smoke-${{ github.ref }}
diff --git a/.github/workflows/zig.yml b/.github/workflows/zig.yml
index 9ae2c47..0a65d9f 100644
--- a/.github/workflows/zig.yml
+++ b/.github/workflows/zig.yml
@@ -24,7 +24,6 @@ on:
   workflow_dispatch:
 
 permissions: read-all
-  actions: read
 
 concurrency:
   group: zig-${{ github.ref }}

From fe01956705f982f546f9a3875450006394b6ba0d Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 27 Jul 2026 14:03:48 +0100
Subject: [PATCH 4/4] fix(ci): drop the unnecessary `actions: read` from
 pages.yml
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The blanket sweep added `actions: read` to every workflow. pages.yml has no job
that reads workflow or run metadata — it checks out, compiles Ddraig, uploads an
artifact and deploys. The grant was unearned, so it goes.

This also reverts pages.yml to exactly origin/main, which clears a SonarCloud
Quality Gate failure ("C Security Rating on New Code"). Sonar's finding is real
but PRE-EXISTING and not introduced here: pages.yml grants `pages: write` and
`id-token: write` at WORKFLOW level, so the build job — which runs a compiler
over checked-out sources — inherits deploy credentials it never uses. Those
belong on the deploy job only.

Deliberately NOT fixed in this PR. Pages deployed successfully for the first
time since 2026-07-19 minutes ago (site now HTTP 200 after a long 404), and
restructuring the permissions of a just-recovered deployment inside a PR whose
`deploy` job cannot run is precisely the untestable change declined in #61.
Filed as a follow-up instead.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .github/workflows/pages.yml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
index e1f3dde..b14bddd 100644
--- a/.github/workflows/pages.yml
+++ b/.github/workflows/pages.yml
@@ -6,7 +6,6 @@ on:
     branches: [main, master]
   workflow_dispatch:
 permissions:
-  actions: read
   contents: read
   pages: write
   id-token: write