ci: concurrency cancel-in-progress + timeout-minutes on 4 long-running workflows (#115)

## Summary

Resolves queue saturation. With proven on GitHub Pro (40 concurrent-job
ceiling), every push to a feature branch was spawning a fresh Idris2
build (~20 min) and Architecture Enforcement run **without superseding
the predecessor**. A 6-PR proof-debt session in ~90 min accumulated 32
in-progress + 36 queued jobs — blocking every other workflow.

## Change

Adds to 4 long-running workflows:

| Workflow | Concurrency | Per-job timeouts |
|---|---|---|
| architecture-enforcement.yml | + | enforce-idris-only: 5m,
verify-idris-build: 20m |
| idris2-ci.yml | + | build: 45m (cold-cache bootstrap), docs: 30m |
| zig-ffi.yml | + | build-cross: 15m, build-macos: 20m, wasm-browser:
15m, release: 10m |
| trustfile.yml | + | validate-trustfile: 5m, enforce-policies: 5m |

Each subsequent push to the same ref now cancels its predecessor. Stuck
jobs self-terminate at the declared budget instead of holding a slot for
the 6-hour default.

## Bonus

Closes the underlying `workflow_audit/missing_timeout_minutes` findings
(currently mislabeled as `workflow_audit/unknown` in the Security tab;
the label fix is hyperpolymath/hypatia#395) for these 4 workflows.

## Scope-out (deliberate)

Remaining workflows tracked as follow-up:
- `boj-build.yml`, `dogfood-gate.yml` — documented persistent-red
non-blocking jobs (commit 7260383)
- `casket-pages.yml`, `mirror.yml`, `instant-sync.yml`, `scorecard.yml`,
`spark-theatre-gate.yml` — reusable wrappers (short)
- `publish-*.yml`, `release.yml`, `cflite_*.yml` — rarely run

## Test plan

- [ ] CI green
- [ ] Push a fresh commit to this branch — verify the predecessor run on
this branch gets cancelled (concurrency working)

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/architecture-enforcement.yml

@@ -10,9 +10,18 @@ on:
 permissions:
   contents: read
 
+# Cancel superseded runs on the same ref so a rapid sequence of pushes
+# to a feature branch does not pile up jobs against the Pro-plan 40-job
+# concurrent ceiling. Each new push to a ref supersedes its predecessor.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   enforce-idris-only:
     runs-on: ubuntu-latest
+    # Fast grep checks; if this exceeds 5 minutes something is wrong.
+    timeout-minutes: 5
     steps:
       - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
 
@@ -98,6 +107,10 @@ jobs:
 
   verify-idris-build:
     runs-on: ubuntu-latest
+    # Docker pull (snazzybucket/idris2) + Idris2 totality check across all
+    # Proven.Safe.* modules. Local oracle runs in ~8 minutes; 20-minute
+    # budget covers cold cache and the occasional Docker Hub slowdown.
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
 

.github/workflows/idris2-ci.yml

@@ -23,9 +23,20 @@ on:
       - '.github/workflows/idris2-ci.yml'
   workflow_dispatch:
 
+# Cancel superseded runs on the same ref. Idris2 bootstrap + build is
+# ~20 minutes per run; without cancel-in-progress, a rapid PR-push
+# sequence saturates the Pro-plan 40-job concurrent ceiling within
+# minutes and blocks every other workflow estate-wide.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   build:
     runs-on: ubuntu-latest
+    # Idris2 bootstrap (cold cache) is ~10 min, build+typecheck ~12 min.
+    # 45-minute budget gives cold-cache + slow apt mirror headroom.
+    timeout-minutes: 45
     strategy:
       matrix:
         idris2-version: ['0.8.0']
@@ -87,7 +98,8 @@ jobs:
     runs-on: ubuntu-latest
     needs: build
     if: github.ref == 'refs/heads/main'
-
+    # Reuses Idris2 cache from build job; docs generation is fast (~5 min).
+    timeout-minutes: 30
     steps:
       - name: Checkout
         uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4

.github/workflows/trustfile.yml

@@ -18,10 +18,15 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   validate-trustfile:
     name: Validate Trustfile Integrity
     runs-on: ubuntu-latest
+    timeout-minutes: 5
 
     steps:
       - name: Checkout repository
@@ -84,6 +89,7 @@ jobs:
     name: Enforce Trustfile Policies
     runs-on: ubuntu-latest
     needs: validate-trustfile
+    timeout-minutes: 5
 
     steps:
       - name: Checkout repository

.github/workflows/zig-ffi.yml

@@ -17,10 +17,15 @@ on:
       - '.github/workflows/zig-ffi.yml'
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   # Cross-compile from Ubuntu (most targets)
   build-cross:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     strategy:
       fail-fast: false
       matrix:
@@ -81,6 +86,7 @@ jobs:
             target: aarch64-macos
 
     runs-on: ${{ matrix.os }}
+    timeout-minutes: 20
 
     steps:
       - name: Checkout proven
@@ -115,6 +121,7 @@ jobs:
 
   wasm-browser:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
 
     steps:
       - name: Checkout proven
@@ -147,6 +154,7 @@ jobs:
     runs-on: ubuntu-latest
     needs: [build-cross, build-macos, wasm-browser]
     if: github.ref == 'refs/heads/main' && github.event_name == 'push'
+    timeout-minutes: 10
 
     steps:
       - name: Download all artifacts

src/Proven/SafeBitset/Proofs.idr

@@ -83,12 +83,18 @@ fromIntegerCapacity cap n = Refl
 -- `singleton` bounds-rejection
 --------------------------------------------------------------------------------
 
-||| OWED: `singleton 0 bit` always rejects (no bit fits in zero
-||| capacity). Blocked because `bit < 0` for variable `bit : Nat`
-||| does not Refl-reduce (standards#128 Nat-comparison opacity).
-public export
-0 singletonZeroCapRejects :
+||| DISCHARGED via 2-arm case-split on `bit`. The `bit < 0` check
+||| inside `singleton 0 bit` reduces on each constructor:
+|||   * `Z < 0` → `compareNat 0 0 == LT` → `EQ == LT` → `False`
+|||   * `S _ < 0` → `compareNat (S _) 0 == LT` → `GT == LT` → `False`
+||| Both make the `if` take the `else` branch, returning `Nothing`.
+||| The OWED's "abstract bit doesn't Refl-reduce" was correct for the
+||| zero-arg version; the case-split unblocks it.
+public export
+singletonZeroCapRejects :
   (bit : Nat) -> singleton 0 bit = Nothing
+singletonZeroCapRejects Z = Refl
+singletonZeroCapRejects (S _) = Refl
 
 --------------------------------------------------------------------------------
 -- Capacity preservation on `Right`-branch (structural case split on `if`)