From cda876d78ae5cc3c9a87055b407ccca587d22708 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Thu, 5 Nov 2026 07:36:30 +0000
Subject: [PATCH 1/7] ci: dispose of the 14 allow-fail units and retire the T1
 Guix job

Owner ruling 2026-11-05 (CI-4): each allow-fail unit is made blocking or
deleted, never re-dated. A unit was made blocking only where recent runs
show it passing; the rest were deleted or fixed in place.

Blocking: static-analysis-gate hypatia-scan "Setup Elixir" and "Clone and
build Hypatia"; chapel-ci rust-chapel-feature; live-provers tier3 job;
live-provers tier2 and tier3 provisioning steps, where the two backends
whose provisioning failed (isabelle download reset, proverif missing from
apt) now degrade with a ::warning:: and SKIP as they already did.

Deleted: boj-build.yml (posts to boj-server.local, unreachable from a
hosted runner, exit 2 on every run); container-ci tier3-container (all 8
cells fail on the 2026-11-01 run with E0391 from the unpinned nightly in
Containerfile.wave3); chapel-ci rust-chapel-real (undefined chapel_*
symbols on main, #408); live-provers tier4 (echo only) and tier4-gpu
(job and both steps; neither binary was ever provisioned).

CI-3: the T1 Guix manifest job is retired by owner ruling; the Containerfile
is the reproducibility path.

check-allow-fail-expiry.sh now reads FAKE_DATE when --today is absent, so
`FAKE_DATE=2026-12-01 scripts/ci/check-allow-fail-expiry.sh` is the W0 gate
form. It exits 0 with 0 units after this change, and 1 on origin/main (14
expired) and on a planted expired unit.

Refs #416

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 .github/workflows/boj-build.yml            |  31 -----
 .github/workflows/chapel-ci.yml            |  82 +++---------
 .github/workflows/container-ci.yml         | 144 ++------------------
 .github/workflows/live-provers.yml         | 147 ++++++---------------
 .github/workflows/static-analysis-gate.yml |   6 +-
 scripts/ci/check-allow-fail-expiry.sh      |   8 +-
 6 files changed, 78 insertions(+), 340 deletions(-)
 delete mode 100644 .github/workflows/boj-build.yml

diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
deleted file mode 100644
index 9251f3a0..00000000
--- a/.github/workflows/boj-build.yml
+++ /dev/null
@@ -1,31 +0,0 @@
-# This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-name: BoJ Server Build Trigger
-on:
-  push:
-    branches: [main, master]
-  workflow_dispatch:
-
-# Cause-B mitigation (#77): de-duplicate stacked BoJ build triggers.
-# cancel-in-progress is false so an in-flight dispatch always completes.
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: false
-
-jobs:
-  trigger-boj:
-    runs-on: ubuntu-latest
-    timeout-minutes: 10
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Trigger BoJ Server (Casket/ssg-mcp)
-        run: |
-          # Send a secure trigger to boj-server to build this repository
-          curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke"             -H "Content-Type: application/json"             -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\\"}"}
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-permissions:
-  contents: read
diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index 8c9316f0..5c242c7d 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -135,16 +135,15 @@ jobs:
           path: src/zig_ffi/zig-out/lib/
 
   # Job 3: Build Rust with chapel feature (links against Zig FFI stubs).
-  # Marked continue-on-error: true alongside its needed dependency zig-ffi
-  # (#133) — when the upstream Zig FFI build is allowed to fail, this job's
-  # "Download FFI library" step has no artifact to consume and red-fires.
-  # Re-enable strict gating once #133's Chapel + FFI rehabilitation lands.
+  # Strict gating since 2026-11-05 (CI-4, #416). It was allow-fail while its
+  # dependency zig-ffi was; zig-ffi has been strict since #133 closed, and
+  # this job passed on every recent run checked, main run 41913186222 among
+  # them.
   rust-chapel-feature:
     name: Rust Build with Chapel Feature
     runs-on: ubuntu-22.04
     timeout-minutes: 30
     needs: zig-ffi
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     steps:
       - uses: actions/checkout@v7.0.1
 
@@ -168,65 +167,14 @@ jobs:
       - name: Test with chapel feature
         run: cargo test --features chapel -- proof_search
 
-  # Job 4: Build Rust linking against the real Chapel library (no Zig stubs).
-  #
-  # Still allow-fail in Wave 1: the full static link of Chapel runtime
-  # (`libchpl.a` + dependency archives) into the Zig FFI shared library
-  # is non-trivial and is tracked as the next milestone after #133
-  # (Wave 2). The chapel-build artifact is now `libechidna_chapel.a`
-  # (static) rather than the previous `.so`, because the apt-shipped
-  # Chapel only carries the `CHPL_LIB_PIC=none` runtime. Once a PIC
-  # runtime is available in the CI image we can revert to `--dynamic`
-  # and flip this job to strict.
-  rust-chapel-real:
-    name: Rust Build — Real Chapel Library (allow-fail, L2.3+ gate)
-    runs-on: ubuntu-22.04
-    timeout-minutes: 30
-    needs: [chapel-build, zig-ffi]
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    steps:
-      - uses: actions/checkout@v7.0.1
-
-      - name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
-        run: |
-          set -euo pipefail
-          sudo apt-get update -qq
-          sudo apt-get install -y libunwind-dev
-          curl -fsSL --max-time 300 --retry 3 -o /tmp/chapel.deb "$CHAPEL_DEB_URL"
-          echo "$CHAPEL_DEB_SHA256  /tmp/chapel.deb" | sha256sum --check
-          sudo apt-get install -y /tmp/chapel.deb
-          chpl --version
-
-      - name: Install Zig
-        uses: mlugg/setup-zig@v2.2.1
-        with:
-          version: 0.14.0
-
-      - name: Install Rust
-        uses: dtolnay/rust-toolchain@v1
-        with:
-          toolchain: stable
-
-      - name: Rust cache
-        uses: Swatinem/rust-cache@v2.9.3
-
-      - name: Download real Chapel library
-        uses: actions/download-artifact@v8.0.2
-        with:
-          name: chapel-lib
-          path: src/chapel/
-
-      - name: Build Zig FFI without stubs (links against real Chapel)
-        run: |
-          cd src/zig_ffi
-          zig build -Doptimize=ReleaseSafe -Dcpu=baseline -Dstubs=false
-
-      - name: Build Rust with real Chapel library
-        run: |
-          export LD_LIBRARY_PATH="$PWD/src/chapel:$PWD/src/zig_ffi/zig-out/lib:${LD_LIBRARY_PATH:-}"
-          cargo build --features chapel
-
-      - name: Test Rust with real Chapel library
-        run: |
-          export LD_LIBRARY_PATH="$PWD/src/chapel:$PWD/src/zig_ffi/zig-out/lib:${LD_LIBRARY_PATH:-}"
-          cargo test --features chapel -- proof_search
+  # Job 4 (`rust-chapel-real`, Rust linked against the real Chapel library
+  # with no Zig stubs) was removed on 2026-11-05 under the CI-4 ruling: every
+  # allow-fail unit is made blocking or deleted, never re-dated (#416). It
+  # could not be made blocking because it fails on main: run 41913186222
+  # (2026-11-04) and the main runs before it stop at "Build Rust with real
+  # Chapel library" (#408) with
+  # `rust-lld: undefined symbol: chapel_is_available`
+  # (and chapel_parallel_search, chapel_free_result, chapel_get_version,
+  # chapel_available_prover_count). The static link of the Chapel runtime
+  # into the Zig FFI library is the next milestone after #133. Add the job
+  # back, blocking, in the change that makes that link work.
diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 3e435a41..1563fb49 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -6,12 +6,12 @@
 #
 # container-ci.yml — Container build verification.
 #
-# Two jobs:
+# One job:
 #   container-build   — builds the minimal ECHIDNA image on every PR/push;
 #                       hard gate.
-#   tier3-container   — builds each Wave-3 prover image weekly (Sunday 06:00 UTC)
-#                       and on any change to the .containerization/** tree;
-#                       allow-fail per image (proprietary builds excluded).
+#
+# The weekly Tier-3 prover-image matrix was removed 2026-11-05 (CI-4, #416);
+# see the note at the end of this file for why and how to restore it.
 
 name: Container Build Verification
 
@@ -36,11 +36,6 @@ on:
       - 'Cargo.lock'
       - 'src/rust/**'
       - '.github/workflows/container-ci.yml'
-  schedule:
-    # Weekly build of Tier-3 prover images (Sunday 06:00 UTC).
-    # Distinct from live-provers.yml Tier-3 run (Sunday 05:00 UTC)
-    # so the container build does not race the live-prover tests.
-    - cron: '0 6 * * 0'
 
 # Cause-B mitigation (#77): de-duplicate superseded builds on the same
 # ref. cancel-in-progress is false so an in-flight image build/publish
@@ -104,124 +99,13 @@ jobs:
         if: always()
         run: podman rmi echidna:ci-test 2>/dev/null || true
 
-  # ── Job 2: Wave-3 Tier-3 prover images — weekly, allow-fail per image ─────
-  #
-  # Runs on the weekly schedule and whenever any .containerization/** file
-  # changes.  Each prover builds in its own matrix cell; allow-fail is set
-  # at cell level so one broken prover does not mask the others.
-  #
-  # Imandra is excluded: it is proprietary and requires a licence token not
-  # available in public CI.
-  tier3-container:
-    name: Tier-3 / ${{ matrix.prover }}
-    runs-on: ubuntu-latest
-    timeout-minutes: 90
-    # Run on schedule or when the .containerization tree changes on main.
-    # Not a merge gate — these are informational weekly builds.
-    if: >-
-      github.event_name == 'schedule' ||
-      (github.event_name == 'push' && contains(github.event.head_commit.modified, '.containerization/'))
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    strategy:
-      fail-fast: false
-      matrix:
-        # All targets live in the consolidated .containerization/Containerfile.wave3
-        # (shared rust-builder stage, one --target per prover). Each matrix cell
-        # is an isolated runner so the shared stage still rebuilds per cell with
-        # --no-cache; cross-cell base caching would need a registry and is a
-        # deliberate future optimisation, not required for correctness.
-        include:
-          - prover: tamarin
-            image: echidna:tamarin
-            version_check: "tamarin-prover --version"
-          - prover: proverif
-            image: echidna:proverif
-            version_check: "proverif -help 2>&1 | head -1"
-          - prover: metamath
-            image: echidna:metamath
-            version_check: "echo exit | metamath 2>&1 | head -1 || true"
-          - prover: twelf
-            image: "echidna:twelf"
-            version_check: "twelf-server --help 2>&1 | head -1 || true"
-          - prover: or-tools
-            image: echidna:or-tools
-            version_check: "ls /usr/local/lib/libortools* 2>/dev/null | head -1 || true"
-          - prover: scip
-            image: echidna:scip
-            version_check: "scip --version 2>&1 | head -1 || true"
-          - prover: hol4
-            image: echidna:hol4
-            version_check: "echo '(* quit *);' | hol 2>&1 | head -1 || true"
-          - prover: acl2
-            image: echidna:acl2
-            version_check: "echo '(acl2::quit)' | acl2 2>&1 | head -3 || true"
-
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-
-      - name: Install Podman
-        run: |
-          sudo apt-get update -q
-          sudo apt-get install -y -q podman
-
-      - name: Build ${{ matrix.prover }} image
-        # HOL4 and ACL2 have long build times; give them extra headroom.
-        timeout-minutes: 90
-        run: |
-          podman build \
-            -f .containerization/Containerfile.wave3 \
-            --target "${{ matrix.prover }}" \
-            -t "${{ matrix.image }}" \
-            --no-cache \
-            .
-
-      - name: Verify ECHIDNA binary inside ${{ matrix.prover }} image
-        run: |
-          podman run --rm "${{ matrix.image }}" --version
-
-      # version_check is passed via env to avoid the YAML→outer-shell→inner-sh
-      # single-quote nesting trap: for acl2 (`echo '(acl2::quit)' | acl2 …`) and
-      # hol4 (`echo '(* quit *);' | hol …`), the inline `-c '${{ matrix.version_check }}'`
-      # form lets the embedded `'` close the outer string and the bash parser
-      # fails with "syntax error near unexpected token `('". Confirmed root-cause
-      # of the persistent acl2/hol4 cron red since 2026-04-27 (a87fae12).
-      - name: Smoke-check ${{ matrix.prover }} binary
-        env:
-          VERSION_CHECK: ${{ matrix.version_check }}
-        run: |
-          podman run --rm --entrypoint /bin/sh "${{ matrix.image }}" \
-            -c "$VERSION_CHECK"
-
-      # #75: the per-prover version_check above uses `|| true` for several
-      # backends because tools like metamath / hol4 / acl2 exit non-zero on
-      # quit. Side effect: a stub fallback (graceful-degrade on a dead
-      # upstream pin, see Containerfile.wave3 :: tamarin/proverif/scip/metamath)
-      # prints "<prover> not available (... failed at image build time)" and
-      # `|| true` swallows it. This step re-runs the check, captures the
-      # output verbatim, and fails LOUDLY on any stub sentinel — turning the
-      # silent degradation into a visible weekly red.
-      - name: Stub-sentinel detection (#75)
-        env:
-          VERSION_CHECK: ${{ matrix.version_check }}
-        run: |
-          set +e
-          OUTPUT=$(podman run --rm --entrypoint /bin/sh "${{ matrix.image }}" \
-            -c "$VERSION_CHECK" 2>&1)
-          echo "--- version_check output ---"
-          echo "$OUTPUT"
-          echo "--- end ---"
-          if echo "$OUTPUT" | grep -qiE 'not available \(bundle install failed|not available \(build failed|not available \(source build failed|bundle install failed at image build time|build failed at image build time|source build failed at image build'; then
-            echo "::error file=.containerization/Containerfile.wave3::Stub sentinel detected in ${{ matrix.prover }} image. The upstream pin is broken and was masked by graceful fallback — bump the pin (#75)."
-            exit 1
-          fi
-          echo "OK: no stub sentinel for ${{ matrix.prover }}"
-
-      - name: Verify image metadata
-        run: |
-          podman inspect "${{ matrix.image }}" \
-            --format '{{index .Config.Labels "org.opencontainers.image.description"}}'
-
-      - name: Clean up
-        if: always()
-        run: podman rmi "${{ matrix.image }}" 2>/dev/null || true
+  # The weekly `tier3-container` matrix (one Containerfile.wave3 target per
+  # Tier-3 prover, with stub-sentinel detection, #75) was removed on
+  # 2026-11-05 under the CI-4 ruling: every allow-fail unit is made blocking
+  # or deleted, never re-dated (#416). It could not be made blocking because
+  # it failed on its latest scheduled run (41279400647, 2026-11-01): all 8
+  # cells stopped at `cargo build` in the rust-builder stage with E0391
+  # ("cycle detected when computing when `provers::pvs::PVSBinding` needs
+  # async drop"), because Containerfile.wave3 installs an unpinned nightly.
+  # Restore it as a blocking job, without continue-on-error, once the
+  # rust-builder stage pins its toolchain and a manual run is green.
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index 5672ce63..0c19ef35 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -6,18 +6,19 @@
 # Exercises real prover binaries against canonical micro-goals. Complements
 # rust-ci.yml (which runs mock tests on every PR) with live-subprocess coverage.
 #
-# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md + manifests/live-provers.scm):
+# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md):
 #   T1 — trivial    — every PR + push to main
 #   T2 — build      — nightly
 #   T3 — container  — weekly
-#   T4 — niche      — quarterly, allow-fail
 #
-# Reproducibility paths (both tried; at least one must succeed):
-#   1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
-#   2. apt-get (expedient bootstrap for T1 only):       jobs below
+# The quarterly T4 jobs (a TODO announcement and a GPUVerify/Faial version
+# check that never provisioned either binary) were removed 2026-11-05 under
+# the CI-4 ruling (#416): every allow-fail unit is made blocking or deleted.
 #
-# (Guix flake removed 2026-06-01 per estate-wide guix-deprecation directive;
-# Guix is the sole reproducible-build primary.)
+# Reproducibility: the Containerfile (and .containerization/Containerfile.wave3
+# for the Tier-3 images) is the reproducibility path. The T1 Guix manifest
+# check was retired 2026-11-05 by owner ruling (ultraplan item CI-3); the
+# jobs below provision provers with apt and upstream releases.
 
 name: Live Provers
 
@@ -29,11 +30,10 @@ on:
   schedule:
     - cron: '0 3 * * *'    # Tier-2 nightly at 03:00 UTC
     - cron: '0 5 * * 0'    # Tier-3 weekly  Sunday 05:00 UTC
-    - cron: '0 6 1 */3 *'  # Tier-4 quarterly 1st of Jan/Apr/Jul/Oct 06:00 UTC
   workflow_dispatch:
     inputs:
       tier:
-        description: 'Which tier to run (1|2|3|4|all)'
+        description: 'Which tier to run (1|2|3|all)'
         required: false
         default: '1'
 
@@ -124,30 +124,6 @@ jobs:
       - name: Run live test for ${{ matrix.backend }}
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
-  # ============================================================================
-  # Tier 1 reproducibility check — ensure Guix manifest actually resolves.
-  # Allow-fail: this is additional proof, not a gate (Guix-on-Ubuntu is flaky
-  # without dedicated setup).
-  # ============================================================================
-  tier1-guix-reproducibility:
-    name: T1 Guix manifest check
-    if: github.event_name != 'schedule'
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Guix
-        run: |
-          sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
-          sudo apt-get install -y --fix-missing guix
-      - name: Resolve manifest (doesn't run tests — just proves the .scm parses)
-        run: |
-          guix describe || true
-          guix package -m manifests/live-provers.scm --dry-run || \
-            echo "NOTE: Guix manifest resolution failed — non-blocking reproducibility signal."
-
   # ============================================================================
   # Tier 2 — nightly.  Larger build-from-source provers.
   # ============================================================================
@@ -179,8 +155,10 @@ jobs:
           toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
+      # Blocking since 2026-11-05 (CI-4, #416). On the three latest nightly
+      # runs only the isabelle download failed; it now degrades to a warning
+      # (see the isabelle case). Any other provisioning failure fails the job.
       - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
         run: |
           set -euo pipefail
           sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
@@ -222,13 +200,22 @@ jobs:
               # --retry 3 + --max-time 600 guard the large download.
               # find locates the binary regardless of extracted dir name,
               # so the symlink survives a future Isabelle2025 release.
-              curl -fsSL --max-time 600 --retry 3 --retry-delay 15 \
-                -o /tmp/isabelle.tar.gz \
-                https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
-              sudo mkdir -p /opt/isabelle
-              sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-              ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
-              [ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
+              # The upstream host reset the connection from hosted runners
+              # (curl exit 35) on every nightly run checked up to 2026-11-05.
+              # Since this step became blocking (CI-4, #416) that failure is
+              # reported as a warning, Isabelle is left uninstalled and the
+              # live test reports SKIP. Every other provisioning failure in
+              # this step fails the job.
+              if curl -fsSL --max-time 600 --retry 3 --retry-delay 15 --retry-all-errors \
+                  -o /tmp/isabelle.tar.gz \
+                  https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz; then
+                sudo mkdir -p /opt/isabelle
+                sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
+                ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
+                [ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
+              else
+                echo "::warning::isabelle: download from isabelle.in.tum.de failed (curl exit $?); Isabelle is not installed and its live test will SKIP."
+              fi
               ;;
             why3)
               sudo apt-get install -y --fix-missing why3
@@ -297,16 +284,19 @@ jobs:
   #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
   #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
   #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
-  #       Provisioning step emits a skip note; test step runs the suite with
-  #       continue-on-error so the matrix stays green and the binary's absence
-  #       is logged as SKIP by the suite's `which` probe.
+  #       Provisioning step emits a skip note, and the binary's absence is
+  #       logged as SKIP by the suite's `which` probe.
+  #
+  # The job and its provisioning step are blocking since 2026-11-05 (CI-4,
+  # #416). On the two latest weekly runs every cell passed; inside the
+  # provisioning step only proverif failed (no apt package on the runner
+  # image), and it now degrades to a warning like twelf.
   # ============================================================================
   tier3:
     name: T3 / ${{ matrix.backend }}
     if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
     runs-on: ubuntu-latest
     timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     strategy:
       fail-fast: false
       matrix:
@@ -330,7 +320,6 @@ jobs:
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
       - name: Provision ${{ matrix.backend }} (best-effort)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
         run: |
           set -euo pipefail
           sudo apt-get update -qq || sudo apt-get update -qq --fix-missing
@@ -348,8 +337,10 @@ jobs:
               [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
               ;;
             proverif)
-              # ProVerif is in the Ubuntu/Debian main repos.
-              sudo apt-get install -y proverif
+              # ProVerif had no apt package on ubuntu-latest in the weekly runs
+              # of 2026-10-25 and 2026-11-01 ("Unable to locate package").
+              sudo apt-get install -y proverif || \
+                echo "::warning::proverif: no apt package on this runner image; ProVerif is not installed and its live test will SKIP."
               ;;
             metamath)
               # metamath-exe is small; apt-installable on Ubuntu with build fallback.
@@ -415,63 +406,3 @@ jobs:
       - name: Run live test for ${{ matrix.backend }}
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
 
-  # ============================================================================
-  # Tier 4 — quarterly, best-effort / allow-fail.
-  # ============================================================================
-  tier4:
-    name: T4 niche provers
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Announce Wave-4 TODO
-        run: |
-          echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
-          echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
-          echo "retained as mock-only unless a maintainer volunteers a Containerfile."
-
-  # ============================================================================
-  # Tier 4 GPU — quarterly, best-effort / allow-fail.
-  # GPUVerify and Faial require CUDA SDK or OpenCL runtime; provisioning is
-  # deferred to a developer workstation or GPU-capable CI runner.
-  # ============================================================================
-  tier4-gpu:
-    name: T4 / ${{ matrix.backend }}
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    strategy:
-      fail-fast: false
-      matrix:
-        backend:
-          - gpuverify
-          - faial
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Rust
-        uses: dtolnay/rust-toolchain@v1
-        with:
-          toolchain: stable
-      - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-        run: |
-          case "${{ matrix.backend }}" in
-            gpuverify)
-              echo "GPUVerify requires CUDA SDK + .NET; deferred to developer workstation."
-              echo "See: https://github.com/mc-imperial/gpuverify"
-              ;;
-            faial)
-              echo "Faial requires CUDA/OpenCL headers; install via: cargo install faial"
-              echo "See: https://github.com/elliotttate/faial"
-              ;;
-          esac
-      - name: Run live version check (SKIP if binary absent)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-        run: cargo test --test live_prover_suite --features live-provers -- --nocapture live_${{ matrix.backend }}_version
diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml
index 1f34ab8e..e95eda10 100644
--- a/.github/workflows/static-analysis-gate.yml
+++ b/.github/workflows/static-analysis-gate.yml
@@ -156,16 +156,18 @@ jobs:
         uses: actions/checkout@v7.0.1
         with:
           fetch-depth: 0
+      # CI-4 (#416, 2026-11-05): these two steps were allow-fail. Both passed,
+      # and the scan they feed ran, in the 15 latest non-cancelled runs
+      # (main run 41943675300 among them), so they are now blocking: a
+      # toolchain or build failure fails this job.
       - name: Setup Elixir for Hypatia scanner
         id: beam
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
         uses: erlef/setup-beam@v1.24.1
         with:
           elixir-version: '1.19.4'
           otp-version: '28.3'
       - name: Clone and build Hypatia
         id: build
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
         env:
           # Pinned to the hypatia commit standards@5751b97e vets as its default.
           # When the standards callers move to that ref, the governance baseline
diff --git a/scripts/ci/check-allow-fail-expiry.sh b/scripts/ci/check-allow-fail-expiry.sh
index 9d96b8ee..2fcc9e08 100755
--- a/scripts/ci/check-allow-fail-expiry.sh
+++ b/scripts/ci/check-allow-fail-expiry.sh
@@ -19,6 +19,10 @@
 #
 # Usage: check-allow-fail-expiry.sh [--today YYYY-MM-DD] [--warn-days N] [DIR ...]
 #
+# The date defaults to FAKE_DATE when that is set (for example
+# `FAKE_DATE=2026-12-01 scripts/ci/check-allow-fail-expiry.sh`, the W0 exit
+# gate), otherwise to today in UTC. `--today` overrides both.
+#
 # Exit codes: 0 all units owned and in date, 1 a unit is unowned, undated,
 # or expired, 2 bad arguments.
 
@@ -33,7 +37,7 @@ while [ $# -gt 0 ]; do
   case "$1" in
     --today) [ $# -ge 2 ] || { echo "--today needs a value" >&2; exit 2; }; today="$2"; shift 2 ;;
     --warn-days) [ $# -ge 2 ] || { echo "--warn-days needs a value" >&2; exit 2; }; warn_days="$2"; shift 2 ;;
-    -h|--help) sed -n '3,20p' "$0"; exit 0 ;;
+    -h|--help) sed -n '3,25p' "$0"; exit 0 ;;
     --) shift; dirs+=("$@"); break ;;
     -*) echo "unknown option: $1" >&2; exit 2 ;;
     *) dirs+=("$1"); shift ;;
@@ -44,7 +48,7 @@ if [ ${#dirs[@]} -eq 0 ]; then
   dirs=(.github/workflows)
 fi
 if [ -z "$today" ]; then
-  today=$(date +%F)
+  today=${FAKE_DATE:-$(date +%F)}
 fi
 if ! today_s=$(date -d "$today" +%s 2>/dev/null); then
   echo "invalid --today: $today" >&2

From 20dc69186dcee3a3a8ceec672c01f2bf7eddd8f1 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 12:54:18 +0000
Subject: [PATCH 2/7] fix(deps): move rmcp to 3.9.0 off three RustSec
 advisories

cargo audit fails on rmcp 3.5.0 (crates/echidna-mcp) with
RUSTSEC-2026-0457 (fixed >=3.7.0), RUSTSEC-2026-0461 (>=3.6.0) and
RUSTSEC-2026-0462 (>=3.9.0), published after main last passed the
Dependency audit check. `cargo update -p rmcp` moves rmcp and
rmcp-macros to 3.9.0, inside the existing "3" requirement; no other
entry changes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 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 17ebbb1f64bb5985130c9a86749dd61f6f398ffe Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 12:56:24 +0000
Subject: [PATCH 3/7] style: rustfmt src/rust/proof_search.rs

`cargo fmt --check` fails on main (2ab7574) in five places in
src/rust/proof_search.rs, so rust-ci 'Cargo check + clippy + fmt' is
red on every PR. Formatting only; no code change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 src/rust/proof_search.rs | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/rust/proof_search.rs b/src/rust/proof_search.rs
index 3c90d3bf..949b63c9 100644
--- a/src/rust/proof_search.rs
+++ b/src/rust/proof_search.rs
@@ -384,7 +384,8 @@ mod chapel_ffi {
                         let start = start.clone();
                         std::thread::spawn(move || {
                             start.wait();
-                            let strategy = ChapelParallelSearch::new().expect("real Chapel runtime");
+                            let strategy =
+                                ChapelParallelSearch::new().expect("real Chapel runtime");
                             assert_eq!(ChapelParallelSearch::available_prover_count(), 0);
                             for _ in 0..2 {
                                 assert!(strategy.available());
@@ -414,10 +415,8 @@ mod chapel_ffi {
             // No global environment mutation races with other Rust tests, and
             // no external prover can be dispatched by this allocation/free probe.
             let empty_path = tempfile::tempdir().expect("empty prover search directory");
-            let mut command = real_probe_command(
-                "real_search_without_provers_fails_and_frees_result",
-                CHILD,
-            );
+            let mut command =
+                real_probe_command("real_search_without_provers_fails_and_frees_result", CHILD);
             command.env("PATH", empty_path.path());
             run_real_probe(
                 &mut command,
@@ -478,7 +477,10 @@ mod chapel_ffi {
                     matches!(stopped_before_cleanup, Ok(true)),
                     "deadline returned with a live or unobservable prover: {stopped_before_cleanup:?}"
                 );
-                assert!(elapsed < Duration::from_secs(3), "deadline took {elapsed:?}");
+                assert!(
+                    elapsed < Duration::from_secs(3),
+                    "deadline took {elapsed:?}"
+                );
                 let result = result.expect("native timeout returns a failed search result");
                 assert!(!result.success);
                 assert_eq!(
@@ -500,17 +502,12 @@ mod chapel_ffi {
             .expect("write finite prover");
             std::fs::set_permissions(&prover, std::fs::Permissions::from_mode(0o700))
                 .expect("make finite prover executable");
-            let mut command = real_probe_command(
-                "real_search_deadline_stops_the_owned_prover",
-                CHILD,
-            );
+            let mut command =
+                real_probe_command("real_search_deadline_stops_the_owned_prover", CHILD);
             command
                 .env("PATH", fixture.path())
                 .env(PID_FILE, fixture.path().join("prover.pid"));
-            run_real_probe(
-                &mut command,
-                "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED",
-            );
+            run_real_probe(&mut command, "ECHIDNA_REAL_CHAPEL_DEADLINE_PROBE_COMPLETED");
         }
     }
 }

From f48fe0aaf82f9fc560f3d0aebec5aeb018da33e3 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 12:58:57 +0000
Subject: [PATCH 4/7] fix(ffi): annotate the audited Zig context-pointer casts
 for Hypatia

Hypatia's code_safety/zig_ptr_cast and zig_align_cast now flag the nine
`@ptrCast(@alignCast(raw))` lines in src/zig_ffi/chapel_bridge.zig and
src/zig_ffi/runtime_owner.zig as high, and the governance Hypatia
baseline gate is red on main (2ab7574) as a result.

Each of those lines recovers a callback's own `*@This()` from the
type-erased `*anyopaque` it was registered with (runtime_owner.Work
.context, or a std.mem.Allocator vtable's ptr), so the cast restores the
original type and alignment. Fixed at source with a reasoned inline
`hypatia: allow` per rule on each line, as the scanner documents,
rather than a baseline entry. No code change: comments only.

Checked by simulating ScannerSuppression.inline_allowed?/4 and
directive_re at hypatia 82396d81 (the CI pin): 18 unsuppressed
findings on main, 0 with this change. The scanner itself could not be
built here (hex.pm is unreachable).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 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 4ddfe3fb828c1909e79195288a9852edaf4ea876 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 13:52:23 +0000
Subject: [PATCH 5/7] ci: make every allow-fail unit blocking or remove it;
 Containerfile reproducibility replaces the Guix job

CI-4 ruling (#416, owner 2026-11-05): every allow-fail unit is made
blocking or deleted, never re-dated. After main's #455 there were 9
units left, plus boj-build, which this lane already deleted.
check-allow-fail-expiry.sh as of 2026-12-01 now counts 0.

Made blocking (each was green on main at the time of this change):
- chapel-ci rust-chapel-feature and rust-chapel-real. #455 landed the
  real Chapel link; both passed on main (run 42100322359) and on the PR
  runs checked up to 2026-11-09. The earlier version of this lane deleted
  rust-chapel-real on 2026-11-04 evidence that #455 made stale.
- container-ci tier3-container. All 8 cells passed on main on 2026-11-08
  (42453284210), stub-sentinel detection included. It runs weekly and on
  dispatch; the head_commit.modified condition, which never matched, is
  gone.
- live-provers tier2 provisioning, and tier3 (job and step).

Removed:
- The live-provers tier4 and tier4-gpu jobs. One echoed a TODO; the other
  never provisioned GPUVerify or Faial, so neither checked anything.
- The T1 Guix manifest check, retired by the same ruling (the
  Containerfile is the reproducibility path).

The Guix check is replaced by a Containerfile reproducibility check in
container-ci, not just dropped:
- container-build and a new container-rebuild build the minimal image on
  two independent runners, both with --no-cache --timestamp 0.
- container-reproducible requires the same image ID and lists the layer
  digests of both builds when they differ.
- A local podman 4.9 check confirms the mechanism: with --timestamp 0
  two builds give one ID, and without it they differ. Whether the full
  Containerfile is reproducible is what this PR's container-ci run tests.
- workflow_dispatch is added so the check can be rerun by hand.

Isabelle runs again instead of being skipped:
- scripts/ci/install-isabelle.sh pins Isabelle2025-2 and its SHA-256. It
  tries https-only mirrors, release archives (website-<release>/dist/)
  first.
- The T2 nightly used the TUM dist/ URL, which redirects to http:// (now
  refused) and reset connections. The weekly Isabelle/HOL job used the
  Cambridge dist/ URL, which returns 404 since the release was superseded
  (job 128978199538, 2026-11-09). Both now call the script.
- verification-proofs-cron gains the script in its path filter, so this
  PR runs it.

ProVerif, twelf and the OR-Tools tarball have no package on the runner
image. Each now writes NOT RUN to the step summary rather than passing
silently. Their containerised builds stay covered by tier3-container.

Docs: dated notes in the Chapel rehabilitation decision record and in
docs/handover/{STATE,TODO}.adoc. manifests/live-provers.scm now says it
has no CI consumer.

actions.lock still lists the deleted boj-build.yml. The lock is
tool-owned, so it is refreshed through the official path
(ci:refresh-actions-lock), not edited here.

Refs #416

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 .github/workflows/chapel-ci.yml               |  20 +-
 .github/workflows/container-ci.yml            | 115 +++++++++--
 .github/workflows/live-provers.yml            | 183 ++++--------------
 .../workflows/verification-proofs-cron.yml    |  16 +-
 .../2026-05-30-chapel-rehabilitation.adoc     |   5 +
 docs/handover/STATE.adoc                      |   4 +-
 docs/handover/TODO.adoc                       |   6 +-
 manifests/live-provers.scm                    |   6 +-
 scripts/ci/install-isabelle.sh                |  56 ++++++
 9 files changed, 232 insertions(+), 179 deletions(-)
 create mode 100755 scripts/ci/install-isabelle.sh

diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index abfeff2c..74f2b8c4 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -141,10 +141,10 @@ jobs:
           path: src/zig_ffi/zig-out/lib/
 
   # Job 3: Build Rust with chapel feature (links against Zig FFI stubs).
-  # Marked continue-on-error: true alongside its needed dependency zig-ffi
-  # (#133) — when the upstream Zig FFI build is allowed to fail, this job's
-  # "Download FFI library" step has no artifact to consume and red-fires.
-  # Re-enable strict gating once #133's Chapel + FFI rehabilitation lands.
+  # Blocking since the CI-4 ruling (#416). It was allow-fail while its
+  # dependency zig-ffi was; zig-ffi has been strict since #133 closed, and
+  # this job passed on main after #455 (run 42100322359) and on every PR run
+  # checked up to 2026-11-09.
   rust-chapel-feature:
     name: Rust Build with Chapel Feature
     runs-on: ubuntu-22.04
@@ -152,7 +152,6 @@ jobs:
     needs: zig-ffi
     env:
       ECHIDNA_CHAPEL_EXPECT_MODE: stubs
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     steps:
       - uses: actions/checkout@v7.0.1
 
@@ -180,16 +179,19 @@ jobs:
   #
   # Cargo is the final static consumer: Zig's archive intentionally leaves
   # chapel_* references for libechidna_chapel.a + the compiler's runtime.
-  # No PIC rebuild is needed for this executable link. The existing #416
-  # waiver is unchanged; promotion requires the exact-source hosted result.
+  # No PIC rebuild is needed for this executable link.
+  #
+  # Blocking since the CI-4 ruling (#416). The real link landed with #455
+  # (build.rs, build_support/chapel.rs), and this job passed on main
+  # (run 42100322359, job 127501960139) and on every PR run checked up to
+  # 2026-11-09. It also consumes chapel-build's chapel-lib artifact.
   rust-chapel-real:
-    name: Rust Build — Real Chapel Library (allow-fail, L2.3+ gate)
+    name: Rust Build — Real Chapel Library
     runs-on: ubuntu-22.04
     timeout-minutes: 30
     needs: [chapel-build, zig-ffi]
     env:
       ECHIDNA_CHAPEL_EXPECT_MODE: real
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     steps:
       - uses: actions/checkout@v7.0.1
 
diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 8cc44c81..58042293 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -6,12 +6,22 @@
 #
 # container-ci.yml — Container build verification.
 #
-# Two jobs:
-#   container-build   — builds the minimal ECHIDNA image on every PR/push;
-#                       hard gate.
-#   tier3-container   — builds each Wave-3 prover image weekly (Sunday 06:00 UTC)
-#                       and on any change to the .containerization/** tree;
-#                       allow-fail per image (proprietary builds excluded).
+# Jobs, all blocking:
+#   container-build         — builds and verifies the minimal ECHIDNA image.
+#   container-rebuild       — builds the same image again on an independent
+#                             runner.
+#   container-reproducible  — requires both builds to have the same image ID.
+#                             This is the reproducibility check that replaced
+#                             the T1 Guix manifest job (owner ruling, CI-4):
+#                             the Containerfile is the reproducibility path.
+#   tier3-container         — builds each Wave-3 prover image weekly (Sunday
+#                             06:00 UTC); proprietary builds excluded.
+#
+# Both minimal builds use --no-cache and --timestamp 0, so creation times
+# and file mtimes cannot make two builds of the same inputs differ. A
+# mismatch means an input floats (an unpinned package, a download without
+# a digest, a non-deterministic build step). The compare job prints the
+# layer digests of both builds so the drifting layer can be found.
 
 name: Container Build Verification
 
@@ -43,6 +53,7 @@ on:
     # Distinct from live-provers.yml Tier-3 run (Sunday 05:00 UTC)
     # so the container build does not race the live-prover tests.
     - cron: '0 6 * * 0'
+  workflow_dispatch:
 
 # Cause-B mitigation (#77): de-duplicate superseded builds on the same
 # ref. cancel-in-progress is false so an in-flight image build/publish
@@ -60,6 +71,9 @@ jobs:
     name: Build & verify container image
     runs-on: ubuntu-latest
     timeout-minutes: 90
+    outputs:
+      image-id: ${{ steps.identity.outputs.image-id }}
+      layers: ${{ steps.identity.outputs.layers }}
 
     steps:
       - name: Checkout
@@ -76,8 +90,16 @@ jobs:
             -f Containerfile \
             -t echidna:ci-test \
             --no-cache \
+            --timestamp 0 \
             .
 
+      - name: Record image identity
+        id: identity
+        run: |
+          set -euo pipefail
+          echo "image-id=$(podman image inspect echidna:ci-test --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
+          echo "layers=$(podman image inspect echidna:ci-test --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
+
       - name: Verify image metadata
         run: |
           echo "=== Image labels ==="
@@ -105,11 +127,75 @@ jobs:
         if: always()
         run: podman rmi echidna:ci-test 2>/dev/null || true
 
-  # ── Job 2: Wave-3 Tier-3 prover images — weekly, allow-fail per image ─────
+  # ── Containerfile reproducibility: an independent rebuild ─────────────────
+  container-rebuild:
+    name: Rebuild container image (independent runner)
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    outputs:
+      image-id: ${{ steps.identity.outputs.image-id }}
+      layers: ${{ steps.identity.outputs.layers }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
+      - name: Install Podman
+        run: |
+          sudo apt-get update -q
+          sudo apt-get install -y -q podman
+
+      - name: Rebuild minimal container image
+        run: |
+          podman build \
+            -f Containerfile \
+            -t echidna:ci-rebuild \
+            --no-cache \
+            --timestamp 0 \
+            .
+
+      - name: Record image identity
+        id: identity
+        run: |
+          set -euo pipefail
+          echo "image-id=$(podman image inspect echidna:ci-rebuild --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
+          echo "layers=$(podman image inspect echidna:ci-rebuild --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
+
+  container-reproducible:
+    name: Containerfile reproducibility (same image ID twice)
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    needs: [container-build, container-rebuild]
+    steps:
+      - name: Compare the two builds
+        env:
+          ID_A: ${{ needs.container-build.outputs.image-id }}
+          ID_B: ${{ needs.container-rebuild.outputs.image-id }}
+          LAYERS_A: ${{ needs.container-build.outputs.layers }}
+          LAYERS_B: ${{ needs.container-rebuild.outputs.layers }}
+        run: |
+          set -euo pipefail
+          [ -n "$ID_A" ] && [ -n "$ID_B" ] || { echo "::error::a build reported no image ID"; exit 1; }
+          {
+            echo "## Containerfile reproducibility"
+            echo "build:   $ID_A"
+            echo "rebuild: $ID_B"
+          } >> "$GITHUB_STEP_SUMMARY"
+          if [ "$ID_A" = "$ID_B" ]; then
+            echo "OK: two independent --no-cache --timestamp 0 builds gave image $ID_A"
+            exit 0
+          fi
+          echo "::error::The Containerfile is not reproducible: two builds of the same commit gave $ID_A and $ID_B."
+          paste <(jq -r '.[]' <<<"$LAYERS_A") <(jq -r '.[]' <<<"$LAYERS_B") \
+            | awk -F '\t' '{ printf "layer %d: %s %s %s\n", NR, ($1 == $2 ? "same" : "DIFFERS"), $1, $2 }' \
+            | tee -a "$GITHUB_STEP_SUMMARY"
+          exit 1
+
+  # ── Wave-3 Tier-3 prover images — weekly, blocking per image ──────────────
   #
-  # Runs on the weekly schedule and whenever any .containerization/** file
-  # changes.  Each prover builds in its own matrix cell; allow-fail is set
-  # at cell level so one broken prover does not mask the others.
+  # Runs on the weekly schedule. Each prover builds in its own matrix cell
+  # (fail-fast off), so one broken prover does not mask the others. Blocking
+  # since the CI-4 ruling (#416): the scheduled run on main of 2026-11-08
+  # (42453284210) passed all eight cells, stub-sentinel detection included.
   #
   # Imandra is excluded: it is proprietary and requires a licence token not
   # available in public CI.
@@ -117,12 +203,9 @@ jobs:
     name: Tier-3 / ${{ matrix.prover }}
     runs-on: ubuntu-latest
     timeout-minutes: 90
-    # Run on schedule or when the .containerization tree changes on main.
-    # Not a merge gate — these are informational weekly builds.
-    if: >-
-      github.event_name == 'schedule' ||
-      (github.event_name == 'push' && contains(github.event.head_commit.modified, '.containerization/'))
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+    # Weekly and on manual dispatch. A red cell is a real failure, but these
+    # builds are too slow to gate every PR.
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     strategy:
       fail-fast: false
       matrix:
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index b5ed9ea2..0bd08a9c 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -6,18 +6,21 @@
 # Exercises real prover binaries against canonical micro-goals. Complements
 # rust-ci.yml (which runs mock tests on every PR) with live-subprocess coverage.
 #
-# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md + manifests/live-provers.scm):
+# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md):
 #   T1 — trivial    — every PR + push to main
 #   T2 — build      — nightly
 #   T3 — container  — weekly
-#   T4 — niche      — quarterly, allow-fail
 #
-# Reproducibility paths (both tried; at least one must succeed):
-#   1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
-#   2. apt-get (expedient bootstrap for T1 only):       jobs below
+# Every job here is blocking: the allow-fail units were made blocking or
+# removed under the CI-4 ruling (2026-11-05, #416). Removed: the quarterly T4
+# jobs (a TODO announcement, and a GPUVerify/Faial check that never
+# provisioned either binary) and the T1 Guix manifest check.
 #
-# (Guix flake removed 2026-06-01 per estate-wide guix-deprecation directive;
-# Guix is the sole reproducible-build primary.)
+# Reproducibility: the Containerfile is the reproducibility path (owner
+# ruling, CI-4). container-ci.yml rebuilds the minimal image on a second,
+# independent runner and requires the same image ID. The jobs below
+# provision provers with apt and with digest- or version-pinned upstream
+# releases.
 
 name: Live Provers
 
@@ -29,11 +32,10 @@ on:
   schedule:
     - cron: '0 3 * * *'    # Tier-2 nightly at 03:00 UTC
     - cron: '0 5 * * 0'    # Tier-3 weekly  Sunday 05:00 UTC
-    - cron: '0 6 1 */3 *'  # Tier-4 quarterly 1st of Jan/Apr/Jul/Oct 06:00 UTC
   workflow_dispatch:
     inputs:
       tier:
-        description: 'Which tier to run (1|2|3|4|all)'
+        description: 'Which tier to run (1|2|3|all)'
         required: false
         default: '1'
 
@@ -140,40 +142,6 @@ jobs:
           LIVE_PROVER: ${{ matrix.backend }}
         run: bash scripts/ci/run-live-prover.sh "$LIVE_PROVER"
 
-  # ============================================================================
-  # Resolve the explicitly packaged Guix subset. This is not live-prover
-  # execution evidence and does not cover the externally provisioned backends.
-  # ============================================================================
-  tier1-guix-reproducibility:
-    name: T1 Guix manifest check
-    if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
-    # Ubuntu 26.04 removed the guix APT package. Noble has this audited version.
-    runs-on: ubuntu-24.04
-    timeout-minutes: 20
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Guix
-        run: |
-          set -euo pipefail
-          trap 'echo "::error::Guix setup failed; manifest check NOT RUN"; exit 2' ERR
-          sudo apt-get update -qq
-          sudo apt-get install -y --no-install-recommends guix=1.4.0-6build1
-          sudo systemctl start guix-daemon
-          guix --version
-      - name: Resolve packaged manifest (not a live-prover test)
-        run: |
-          set -euo pipefail
-          {
-            echo '## Guix manifest scope'
-            echo
-            echo 'This job resolves the Guix-packaged subset; it does not build or run provers.'
-            echo 'Guix coverage for cvc5, alt-ergo, vampire, eprover, spass, chuffed, Idris2 and Isabelle is UNKNOWN.'
-            echo 'Their separate live-prover jobs must supply execution evidence; this job cannot satisfy it.'
-            echo 'See manifests/live-provers.scm for the package boundary.'
-          } >> "$GITHUB_STEP_SUMMARY"
-          guix package --manifest=manifests/live-provers.scm --dry-run --no-substitutes
-
   # ============================================================================
   # Tier 2 — nightly.  Larger build-from-source provers.
   # ============================================================================
@@ -205,8 +173,11 @@ jobs:
           toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+      # Blocking since the CI-4 ruling (#416). In the nightly runs up to
+      # 2026-11-09 only the Isabelle download failed in this step; Isabelle
+      # now installs through scripts/ci/install-isabelle.sh, so any
+      # provisioning failure here is a real one.
+      - name: Provision ${{ matrix.backend }} (apt / pinned upstream release)
         run: |
           set -euo pipefail
           readonly https_protocol='=https'
@@ -241,17 +212,11 @@ jobs:
               echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
               ;;
             isabelle)
-              # Isabelle2024 tarball (~500MB); nightly only.
-              # --retry 3 + --max-time 600 guard the large download.
-              # find locates the binary regardless of extracted dir name,
-              # so the symlink survives a future Isabelle2025 release.
-              curl --proto "$https_protocol" --proto-redir "$https_protocol" -fsSL --max-time 600 --retry 3 --retry-delay 15 \
-                -o /tmp/isabelle.tar.gz \
-                https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
-              sudo mkdir -p /opt/isabelle
-              sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-              ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
-              [ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
+              # Pinned release and SHA-256, https-only mirrors (the upstream
+              # dist/ path redirected to http:// and reset connections from
+              # hosted runners on the nightlies up to 2026-11-09). One
+              # installer serves this job and verification-proofs-cron.yml.
+              bash scripts/ci/install-isabelle.sh
               ;;
             why3)
               sudo apt-get install -y --fix-missing why3
@@ -320,16 +285,20 @@ jobs:
   #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
   #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
   #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
-  #       Provisioning step emits a skip note; test step runs the suite with
-  #       continue-on-error so the matrix stays green and the binary's absence
-  #       is logged as SKIP by the suite's `which` probe.
+  #       Provisioning step emits a skip note, and the binary's absence is
+  #       logged as SKIP by the suite's `which` probe. Their containerised
+  #       builds are checked by container-ci.yml's tier3-container job.
+  #
+  # The job and its provisioning step are blocking since the CI-4 ruling
+  # (#416). On the weekly runs up to 2026-11-09 only proverif failed inside
+  # the provisioning step (no apt package on the runner image); it records
+  # NOT RUN in the step summary instead of failing, like twelf.
   # ============================================================================
   tier3:
     name: T3 / ${{ matrix.backend }}
     if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
     runs-on: ubuntu-latest
     timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     strategy:
       fail-fast: false
       matrix:
@@ -352,8 +321,7 @@ jobs:
           toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+      - name: Provision ${{ matrix.backend }}
         run: |
           set -euo pipefail
           readonly https_protocol='=https'
@@ -372,8 +340,15 @@ jobs:
               [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
               ;;
             proverif)
-              # ProVerif is in the Ubuntu/Debian main repos.
-              sudo apt-get install -y proverif
+              # ProVerif had no apt package on ubuntu-latest in the weekly
+              # runs up to 2026-11-09 ("Unable to locate package"). Record
+              # that as NOT RUN rather than a pass; the containerised build
+              # in container-ci.yml (tier3-container) remains the check that
+              # ProVerif itself still builds.
+              sudo apt-get install -y proverif || {
+                echo "::warning::proverif: no apt package on this runner image; not installed, live test will SKIP."
+                echo "proverif: NOT RUN (no apt package on this runner image)" >> "$GITHUB_STEP_SUMMARY"
+              }
               ;;
             metamath)
               # metamath-exe is small; apt-installable on Ubuntu with build fallback.
@@ -387,8 +362,10 @@ jobs:
               ;;
             twelf)
               # Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
-              sudo apt-get install -y twelf || \
+              sudo apt-get install -y twelf || {
                 echo "twelf unavailable via apt on this runner; test will SKIP."
+                echo "twelf: NOT RUN (no apt package on this runner image)" >> "$GITHUB_STEP_SUMMARY"
+              }
               ;;
             ortools)
               # Google OR-Tools ships prebuilt Linux tarballs.  The binary we
@@ -396,6 +373,7 @@ jobs:
               OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
               curl --proto "$https_protocol" --proto-redir "$https_protocol" -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
                 echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
+                echo "ortools: NOT RUN (release tarball unavailable)" >> "$GITHUB_STEP_SUMMARY"
                 exit 0
               }
               sudo mkdir -p /opt/ortools
@@ -438,78 +416,3 @@ jobs:
           esac
       - name: Run live test for ${{ matrix.backend }}
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
-
-  # ============================================================================
-  # Tier 4 — quarterly, best-effort / allow-fail.
-  # ============================================================================
-  tier4:
-    name: T4 niche provers
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Announce Wave-4 TODO
-        run: |
-          echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
-          echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
-          echo "retained as mock-only unless a maintainer volunteers a Containerfile."
-
-  # ============================================================================
-  # Tier 4 GPU — quarterly, best-effort / allow-fail.
-  # GPUVerify and Faial require CUDA SDK or OpenCL runtime; provisioning is
-  # deferred to a developer workstation or GPU-capable CI runner.
-  # ============================================================================
-  tier4-gpu:
-    name: T4 / ${{ matrix.backend }}
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    strategy:
-      fail-fast: false
-      matrix:
-        backend:
-          - gpuverify
-          - faial
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Rust
-        uses: dtolnay/rust-toolchain@v1
-        with:
-          toolchain: stable
-      - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-        run: |
-          case "${{ matrix.backend }}" in
-            gpuverify)
-              echo "GPUVerify requires CUDA SDK + .NET; deferred to developer workstation."
-              echo "See: https://github.com/mc-imperial/gpuverify"
-              ;;
-            faial)
-              echo "Faial requires CUDA/OpenCL headers; install via: cargo install faial"
-              echo "See: https://github.com/elliotttate/faial"
-              ;;
-          esac
-      - name: Require selected live version check
-        env:
-          LIVE_PROVER: ${{ matrix.backend }}
-        run: bash scripts/ci/run-live-prover.sh "$LIVE_PROVER"
-      - name: Record selected GPU capability
-        if: always()
-        env:
-          LIVE_PROVER: ${{ matrix.backend }}
-          GPU_JOB_STATUS: ${{ job.status }}
-        run: |
-          {
-            echo "## Selected GPU backend: $LIVE_PROVER"
-            echo "Execution status: $GPU_JOB_STATUS"
-            echo 'Missing tools mean NOT RUN, never a passed version check.'
-            echo 'The temporary job-level allow-fail is issue #416, expires 2026-11-30.'
-            echo 'A passed version probe establishes executable identity, not proof correctness.'
-          } >> "$GITHUB_STEP_SUMMARY"
diff --git a/.github/workflows/verification-proofs-cron.yml b/.github/workflows/verification-proofs-cron.yml
index 226d254a..9a5e2a31 100644
--- a/.github/workflows/verification-proofs-cron.yml
+++ b/.github/workflows/verification-proofs-cron.yml
@@ -25,6 +25,7 @@ on:
   pull_request:
     paths:
       - 'proofs/isabelle/**'
+      - 'scripts/ci/install-isabelle.sh'
       - '.github/workflows/verification-proofs-cron.yml'
 
 concurrency:
@@ -43,17 +44,10 @@ jobs:
       - uses: actions/checkout@v7.0.1
 
       - name: Install Isabelle
-        run: |
-          set -euo pipefail
-          # Official Cambridge distribution mirror; immutable version and digest.
-          curl -fL --max-time 900 --retry 3 --retry-delay 15 \
-            -o /tmp/isabelle.tar.gz \
-            https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2025-2_linux.tar.gz
-          echo "a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c  /tmp/isabelle.tar.gz" | sha256sum --check
-          sudo mkdir -p /opt/isabelle
-          sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-          sudo ln -sf /opt/isabelle/Isabelle2025-2/bin/isabelle /usr/local/bin/isabelle
-          isabelle version
+        # Pinned release, digest and https-only mirrors live in the script.
+        # The old inline URL used the mirror's current-release dist/ path,
+        # which returned 404 once that release was superseded (2026-11-09).
+        run: bash scripts/ci/install-isabelle.sh
 
       - name: Install just
         run: |
diff --git a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
index ecaac65f..c57f18c3 100644
--- a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
+++ b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
@@ -145,6 +145,11 @@ composable with the existing `+SoundnessPreservation+` proof.
 * Static-library distribution means the Rust-side link path
 (`+rust-chapel-real+`) remains allow-fail until the PIC-runtime CI image
 lands. Wave-2 work is non-trivial.
++
+_Update 2026-11-09._ The real link landed with #455 as a static link
+with Cargo as the final consumer (`+build.rs+`, `+build_support/chapel.rs+`),
+with no PIC rebuild. `+rust-chapel-real+` passed on main from then on and is
+blocking under the CI-4 ruling (#416), as is `+rust-chapel-feature+`.
 * `+chapel-ci.yml+`’s install step downloads a ~150 MB Chapel deb per
 run; this is unchanged from the prior state but matters more now that
 the job is strict (any apt mirror flake red-checks the workflow).
diff --git a/docs/handover/STATE.adoc b/docs/handover/STATE.adoc
index ed39e012..ad35ee19 100644
--- a/docs/handover/STATE.adoc
+++ b/docs/handover/STATE.adoc
@@ -45,7 +45,9 @@ highest-leverage gap, surfaces real bugs mocks hide. Cap’n Proto next,
 since Chapel consumes those schemas.
 
 |D5 |*Live-prover CI cadence tiered* |T1 every PR, T2 nightly, T3
-weekly, T4 quarterly allow-fail.
+weekly. (The T4 quarterly allow-fail jobs and the T1 Guix manifest check
+were removed 2026-11-09 under the CI-4 ruling, #416; every remaining job
+is blocking.)
 
 |D6 |*No JSON emit on hot path* |Per `+feedback_no_json_emit_a2ml+`.
 Cap’n Proto replaces HTTP-JSON Rust↔Julia. Tool config stays
diff --git a/docs/handover/TODO.adoc b/docs/handover/TODO.adoc
index 08d768b5..251f5420 100644
--- a/docs/handover/TODO.adoc
+++ b/docs/handover/TODO.adoc
@@ -155,7 +155,11 @@ at-source. *#74 (proverif opam) resolved.* Imandra remains the only stub
 — genuinely proprietary, honestly fail-loud, kept by decision (real
 adapter + Idris2 ABI proofs retained). No stub-theatre.
 
-==== Wave-4 (Tier-4 quarterly, 19 backends, allow-fail placeholder)
+==== Wave-4 (Tier-4, 19 backends, mock-only)
+
+_The quarterly Tier-4 CI placeholder jobs were removed 2026-11-09 under the
+CI-4 ruling (#416): they announced a TODO and never provisioned a binary.
+A backend returns to CI in a blocking job once it has a Containerfile._
 
 Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL, ViPER,
 NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy. Retain as
diff --git a/manifests/live-provers.scm b/manifests/live-provers.scm
index 51d198cc..b73d503a 100644
--- a/manifests/live-provers.scm
+++ b/manifests/live-provers.scm
@@ -6,7 +6,11 @@
 ;; Purpose: resolve the subset packaged by GNU Guix 1.4.0 (the CI baseline).
 ;; This manifest is NOT a declaration that every live prover is packaged or
 ;; tested. Resolution does not prove that a prover ran or that a proof passed.
-;; Used by `.github/workflows/live-provers.yml` and local developers via:
+;; It has no CI consumer: the T1 Guix manifest check in live-provers.yml was
+;; retired 2026-11-09 under the CI-4 ruling (#416), and the Containerfile is
+;; the reproducibility path (container-ci.yml rebuilds the image on an
+;; independent runner and requires the same image ID). Local developers can
+;; still resolve it via:
 ;;
 ;;     guix package -m manifests/live-provers.scm --dry-run --no-substitutes
 ;;
diff --git a/scripts/ci/install-isabelle.sh b/scripts/ci/install-isabelle.sh
new file mode 100755
index 00000000..5683939f
--- /dev/null
+++ b/scripts/ci/install-isabelle.sh
@@ -0,0 +1,56 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# install-isabelle.sh — install the pinned Isabelle release into
+# /opt/isabelle and link /usr/local/bin/isabelle. Used by every workflow
+# that needs Isabelle (live-provers T2, verification-proofs-cron), so the
+# version, digest and mirrors live in one place.
+#
+# Why the mirror list: the upstream `dist/` path holds only the current
+# release, so a pinned release 404s once the next one ships (weekly
+# Isabelle/HOL, 2026-11-09). isabelle.in.tum.de has also redirected to an
+# http:// mirror, which `--proto-redir =https` refuses (T2 nightly). Each
+# release stays published under `website-<release>/dist/`. Every candidate
+# is fetched over https only, and the tarball must match the pinned
+# SHA-256 whichever host served it.
+#
+# Exit codes: 0 installed and `isabelle version` ran, 1 no mirror served the
+# pinned tarball, or the install failed.
+set -euo pipefail
+
+RELEASE=Isabelle2025-2
+SHA256=a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c
+TARBALL="${RELEASE}_linux.tar.gz"
+MIRRORS=(
+  "https://isabelle.in.tum.de/website-${RELEASE}/dist/${TARBALL}"
+  "https://www.cl.cam.ac.uk/research/hvg/Isabelle/website-${RELEASE}/dist/${TARBALL}"
+  "https://isabelle.sketis.net/website-${RELEASE}/dist/${TARBALL}"
+  "https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/${TARBALL}"
+  "https://isabelle.in.tum.de/dist/${TARBALL}"
+)
+
+dest="${RUNNER_TEMP:-/tmp}/${TARBALL}"
+fetched=""
+for url in "${MIRRORS[@]}"; do
+  echo "install-isabelle: trying $url"
+  rm -f "$dest"
+  if curl --proto '=https' --proto-redir '=https' -fL --max-time 900 \
+       --retry 3 --retry-delay 15 --retry-all-errors -o "$dest" "$url" \
+     && printf '%s  %s\n' "$SHA256" "$dest" | sha256sum --check --status; then
+    fetched="$url"
+    break
+  fi
+  echo "install-isabelle: $url did not serve the pinned tarball" >&2
+done
+if [ -z "$fetched" ]; then
+  echo "::error::install-isabelle: no mirror served ${TARBALL} with SHA-256 ${SHA256}" >&2
+  exit 1
+fi
+echo "install-isabelle: ${TARBALL} from $fetched (SHA-256 verified)"
+
+sudo mkdir -p /opt/isabelle
+sudo tar xzf "$dest" -C /opt/isabelle
+sudo ln -sf "/opt/isabelle/${RELEASE}/bin/isabelle" /usr/local/bin/isabelle
+rm -f "$dest"
+isabelle version

From e2945c56a8f3e1ecf3c7f9f07e5fa6e455e8d1ef Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 15:19:32 +0000
Subject: [PATCH 6/7] ci(container): name the paths that make two builds
 differ, not only the layer

The first container-reproducible run gave two image IDs. 15 of 16
layers matched, including the echidna binary and z3. Layer 12 differed,
which is the `COPY --from=prover-installer /opt/elan` (the Lean
toolchain). A layer digest does not say which file drifts. I could not
reproduce locally: elan fetches Lean from releases.lean-lang.org, which
this sandbox cannot reach.

Each build job now prints a per-path fingerprint of its image
(scripts/ci/fs-fingerprint.sh, depth 12). The script hashes files
straight from the `podman export` stream, so nothing is extracted. On a
mismatch, container-reproducible reads both build jobs' logs (job-level
`actions: read`) and lists the deepest differing paths
(scripts/ci/fs-fingerprint-drift.sh). No new actions are used, so
actions.lock is unchanged: checkout was already locked for this
workflow.

scripts/ci/test-fs-fingerprint.sh covers identical trees, and content,
mode and link-target changes, each reported at exactly the changed path
and its ancestors. It also covers names with spaces, "|" and "&". It
passes locally. A depth-4 run over /usr/share (19,909 files) took
1m45s. actionlint 1.7.7 and shellcheck are clean, and the SC2015 in the
comparator is fixed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 .github/workflows/container-ci.yml | 69 ++++++++++++++++++++++++--
 scripts/ci/fs-fingerprint-drift.sh | 19 ++++++++
 scripts/ci/fs-fingerprint.sh       | 78 ++++++++++++++++++++++++++++++
 scripts/ci/test-fs-fingerprint.sh  | 47 ++++++++++++++++++
 4 files changed, 210 insertions(+), 3 deletions(-)
 create mode 100755 scripts/ci/fs-fingerprint-drift.sh
 create mode 100755 scripts/ci/fs-fingerprint.sh
 create mode 100755 scripts/ci/test-fs-fingerprint.sh

diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 58042293..39c53d86 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -21,7 +21,8 @@
 # and file mtimes cannot make two builds of the same inputs differ. A
 # mismatch means an input floats (an unpinned package, a download without
 # a digest, a non-deterministic build step). The compare job prints the
-# layer digests of both builds so the drifting layer can be found.
+# layer digests of both builds, and the deepest paths whose digests differ
+# (each build prints a per-path fingerprint, scripts/ci/fs-fingerprint.sh).
 
 name: Container Build Verification
 
@@ -34,6 +35,7 @@ on:
     paths:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
+      - 'scripts/ci/fs-fingerprint.sh'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -43,6 +45,7 @@ on:
     paths:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
+      - 'scripts/ci/fs-fingerprint.sh'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -100,6 +103,21 @@ jobs:
           echo "image-id=$(podman image inspect echidna:ci-test --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
           echo "layers=$(podman image inspect echidna:ci-test --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
 
+      # Per-path digests of the image filesystem, printed between markers so
+      # container-reproducible can name the drifting paths, not only the layer.
+      - name: Fingerprint the image filesystem
+        run: |
+          set -euo pipefail
+          cid=$(podman create echidna:ci-test)
+          podman export "$cid" | bash scripts/ci/fs-fingerprint.sh 12 > "$RUNNER_TEMP/fs-fingerprint"
+          podman rm "$cid" >/dev/null
+          echo "fs-fingerprint: $(wc -l < "$RUNNER_TEMP/fs-fingerprint") paths"
+          echo "::group::fs-fingerprint (depth 12)"
+          echo "FS-FINGERPRINT-BEGIN"
+          cat "$RUNNER_TEMP/fs-fingerprint"
+          echo "FS-FINGERPRINT-END"
+          echo "::endgroup::"
+
       - name: Verify image metadata
         run: |
           echo "=== Image labels ==="
@@ -160,21 +178,43 @@ jobs:
           echo "image-id=$(podman image inspect echidna:ci-rebuild --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
           echo "layers=$(podman image inspect echidna:ci-rebuild --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
 
+      # Per-path digests of the image filesystem, printed between markers so
+      # container-reproducible can name the drifting paths, not only the layer.
+      - name: Fingerprint the image filesystem
+        run: |
+          set -euo pipefail
+          cid=$(podman create echidna:ci-rebuild)
+          podman export "$cid" | bash scripts/ci/fs-fingerprint.sh 12 > "$RUNNER_TEMP/fs-fingerprint"
+          podman rm "$cid" >/dev/null
+          echo "fs-fingerprint: $(wc -l < "$RUNNER_TEMP/fs-fingerprint") paths"
+          echo "::group::fs-fingerprint (depth 12)"
+          echo "FS-FINGERPRINT-BEGIN"
+          cat "$RUNNER_TEMP/fs-fingerprint"
+          echo "FS-FINGERPRINT-END"
+          echo "::endgroup::"
+
   container-reproducible:
     name: Containerfile reproducibility (same image ID twice)
     runs-on: ubuntu-latest
-    timeout-minutes: 5
+    timeout-minutes: 10
     needs: [container-build, container-rebuild]
+    permissions:
+      actions: read     # read the two build jobs' logs for their fs-fingerprints
+      contents: read
     steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
       - name: Compare the two builds
         env:
+          GH_TOKEN: ${{ github.token }}
           ID_A: ${{ needs.container-build.outputs.image-id }}
           ID_B: ${{ needs.container-rebuild.outputs.image-id }}
           LAYERS_A: ${{ needs.container-build.outputs.layers }}
           LAYERS_B: ${{ needs.container-rebuild.outputs.layers }}
         run: |
           set -euo pipefail
-          [ -n "$ID_A" ] && [ -n "$ID_B" ] || { echo "::error::a build reported no image ID"; exit 1; }
+          if [ -z "$ID_A" ] || [ -z "$ID_B" ]; then echo "::error::a build reported no image ID"; exit 1; fi
           {
             echo "## Containerfile reproducibility"
             echo "build:   $ID_A"
@@ -188,6 +228,29 @@ jobs:
           paste <(jq -r '.[]' <<<"$LAYERS_A") <(jq -r '.[]' <<<"$LAYERS_B") \
             | awk -F '\t' '{ printf "layer %d: %s %s %s\n", NR, ($1 == $2 ? "same" : "DIFFERS"), $1, $2 }' \
             | tee -a "$GITHUB_STEP_SUMMARY"
+          # Name the drift: each build job printed per-path digests of its
+          # image between markers (scripts/ci/fs-fingerprint.sh).
+          fingerprint() {
+            local id
+            id=$(gh api "repos/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID/attempts/$GITHUB_RUN_ATTEMPT/jobs" \
+                   --paginate --jq ".jobs[] | select(.name == \"$1\") | .id" | head -n 1)
+            [ -n "$id" ] || { echo "::warning::no job named '$1' in this run attempt"; return 1; }
+            gh api "repos/$GITHUB_REPOSITORY/actions/jobs/$id/logs" \
+              | sed -E 's/^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9:.]+Z //' \
+              | sed -n '/^FS-FINGERPRINT-BEGIN$/,/^FS-FINGERPRINT-END$/p' \
+              | grep -E '^[0-9a-f]{64}  '
+          }
+          if fingerprint "Build & verify container image" > "$RUNNER_TEMP/fp-a" \
+             && fingerprint "Rebuild container image (independent runner)" > "$RUNNER_TEMP/fp-b"; then
+            {
+              echo "### Paths that differ between the two builds (deepest only)"
+              echo '```'
+              bash scripts/ci/fs-fingerprint-drift.sh "$RUNNER_TEMP/fp-a" "$RUNNER_TEMP/fp-b" | head -n 200
+              echo '```'
+            } | tee -a "$GITHUB_STEP_SUMMARY"
+          else
+            echo "::warning::could not read both fs-fingerprints; only the layer comparison is available"
+          fi
           exit 1
 
   # ── Wave-3 Tier-3 prover images — weekly, blocking per image ──────────────
diff --git a/scripts/ci/fs-fingerprint-drift.sh b/scripts/ci/fs-fingerprint-drift.sh
new file mode 100755
index 00000000..62e33957
--- /dev/null
+++ b/scripts/ci/fs-fingerprint-drift.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# fs-fingerprint-drift.sh A B
+#
+# A and B are fs-fingerprint.sh outputs ("<sha256>  <path>" per line).
+# Prints the deepest paths whose digest differs or that exist on one side
+# only. An ancestor of a printed path is left out, since it differs only
+# because the path beneath it does.
+set -euo pipefail
+a=${1:?usage: fs-fingerprint-drift.sh A B}; b=${2:?usage: fs-fingerprint-drift.sh A B}
+t=$(mktemp -d); trap 'rm -rf -- "$t"' EXIT
+# "path<TAB>digest", keyed on path; awk keeps names with spaces whole.
+key() { awk '{ d = substr($0, 1, 64); p = substr($0, 67); print p "\t" d }' "$1" | LC_ALL=C sort -t "$(printf '\t')" -k1,1; }
+key "$a" > "$t/a"; key "$b" > "$t/b"
+LC_ALL=C join -t "$(printf '\t')" -a 1 -a 2 -e MISSING -o 0,1.2,2.2 "$t/a" "$t/b" \
+  | awk -F '\t' '$2 != $3 { print $1 }' > "$t/drift"
+# Keep a path only if no other drifting path lies beneath it.
+awk 'NR == FNR { all[$0] = 1; next }
+     { for (q in all) if (index(q, $0 "/") == 1) next; print }' "$t/drift" "$t/drift" | LC_ALL=C sort
diff --git a/scripts/ci/fs-fingerprint.sh b/scripts/ci/fs-fingerprint.sh
new file mode 100755
index 00000000..a986294a
--- /dev/null
+++ b/scripts/ci/fs-fingerprint.sh
@@ -0,0 +1,78 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# fs-fingerprint.sh DEPTH < image.tar
+#
+# Reads a filesystem tar stream (`podman export`) on stdin. It prints one
+# line, "<sha256>  <path>", for every path at most DEPTH components deep.
+# A regular file's digest covers its content and mode. A symlink's covers
+# its target. A directory's covers the entries beneath it (type, mode,
+# path, and content digest or link target).
+#
+# Two builds whose image IDs differ can then be compared path by path.
+# The paths whose digests differ name where the drift is, not just which
+# layer. Nothing is extracted to disk: file contents are hashed as they
+# stream past (GNU tar --to-command). Owners and timestamps are left out,
+# since `podman build --timestamp` already fixes the times.
+set -euo pipefail
+depth=${1:?usage: fs-fingerprint.sh DEPTH < image.tar}
+[[ $depth =~ ^[1-9][0-9]*$ ]] || { echo "fs-fingerprint: DEPTH must be a positive integer" >&2; exit 2; }
+for tool in tar sha256sum awk sort; do
+  command -v "$tool" >/dev/null || { echo "fs-fingerprint: $tool missing" >&2; exit 2; }
+done
+tar --version | head -n 1 | grep -q 'GNU tar' || { echo "fs-fingerprint: GNU tar required" >&2; exit 2; }
+
+work=$(mktemp -d)
+trap 'rm -rf -- "$work"' EXIT
+mkfifo "$work/stream"
+
+# One pass for listings (types, modes, link targets) and one for content
+# hashes: tee splits the single input stream so it is read only once.
+# The single quotes are deliberate: tar runs the command, which expands them.
+# shellcheck disable=SC2016
+tee "$work/stream" < /dev/stdin \
+  | tar -x --to-command='printf "%s %s %s\n" "$(sha256sum | cut -d" " -f1)" "$TAR_MODE" "$TAR_FILENAME"' \
+      -f - > "$work/files" &
+hasher=$!
+# --quoting-style=escape keeps one entry per line whatever the names hold.
+tar --quoting-style=escape -tv --numeric-owner -f - < "$work/stream" > "$work/listing"
+wait "$hasher"
+
+# Manifest: "<path>\t<type>\t<mode-or-perm>\t<digest-or-target>", path
+# normalised to no leading "./" or "/". Regular files come from the hash
+# pass; directories and symlinks from the listing.
+awk '{ p = $0; sub(/^[^ ]+ [^ ]+ /, "", p); sub(/^\.?\//, "", p); if (p != "") printf "%s\tf\t%s\t%s\n", p, $2, $1 }' "$work/files" > "$work/manifest"
+awk '
+  {
+    t = substr($1, 1, 1); perm = substr($1, 2)
+    # Fields: perms owner size date time name [-> target]
+    name = ""; for (i = 6; i <= NF; i++) { if ($i == "->") break; name = name (name == "" ? "" : " ") $i }
+    target = ""; for (j = i + 1; j <= NF; j++) target = target (target == "" ? "" : " ") $j
+    sub(/^\.?\//, "", name); sub(/\/$/, "", name)
+    if (name == "") next
+    if (t == "d") printf "%s\td\t%s\t-\n", name, perm
+    else if (t == "l") printf "%s\tl\t%s\t%s\n", name, perm, target
+    else if (t == "h") printf "%s\th\t%s\t%s\n", name, perm, target
+  }' "$work/listing" >> "$work/manifest"
+LC_ALL=C sort -t "$(printf '\t')" -k1,1 -o "$work/manifest" "$work/manifest"
+
+# For every path up to DEPTH: a file/link digests its own row; a directory
+# digests every row at or beneath it. One awk pass emits "prefix\trow"
+# pairs; grouping and hashing happen per prefix.
+awk -v depth="$depth" -F '\t' '
+  {
+    n = split($1, part, "/")
+    prefix = ""
+    for (k = 1; k <= n && k <= depth; k++) {
+      prefix = prefix (k == 1 ? "" : "/") part[k]
+      print prefix "\t" $0
+    }
+  }' "$work/manifest" | LC_ALL=C sort -t "$(printf '\t')" -k1,1 -s > "$work/pairs"
+
+awk -F '\t' '
+  function flush() { if (cur != "") { close(cmd); } }
+  {
+    if ($1 != cur) { flush(); cur = $1; esc = cur; gsub(/[\\|&]/, "\\\\&", esc); cmd = "sha256sum | cut -c1-64 | sed \"s|$|  " esc "|\"" }
+    line = $2; for (i = 3; i <= NF; i++) line = line "\t" $i
+    print line | cmd
+  }
+  END { flush() }' "$work/pairs" | LC_ALL=C sort -k2
diff --git a/scripts/ci/test-fs-fingerprint.sh b/scripts/ci/test-fs-fingerprint.sh
new file mode 100755
index 00000000..785594a8
--- /dev/null
+++ b/scripts/ci/test-fs-fingerprint.sh
@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Self-test for scripts/ci/fs-fingerprint.sh: identical trees agree, and a
+# content, mode or link-target change is reported at the changed path and
+# its ancestors only. Names with spaces, "|" and "&" survive intact.
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+t=$(mktemp -d); trap 'rm -rf -- "$t"' EXIT
+fp() { (cd "$1" && tar --sort=name -cf - .) | bash "$here/fs-fingerprint.sh" "$2"; }
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+mkdir -p "$t/a/opt/elan/toolchains/lean/lib" "$t/a/usr/bin"
+echo hi > "$t/a/usr/bin/x"
+echo lean > "$t/a/opt/elan/toolchains/lean/lib/a.olean"
+echo s > "$t/a/opt/elan/settings.toml"
+ln -s ../usr/bin/x "$t/a/opt/link"
+echo odd > "$t/a/opt/we|ird &name"
+chmod 0644 "$t/a/usr/bin/x"
+
+clone() { rm -rf "$t/b"; cp -a "$t/a" "$t/b"; }
+changed() { diff <(fp "$t/a" "$1") <(fp "$t/b" "$1") | sed -n 's/^> [0-9a-f]\{64\}  //p' | sort | tr '\n' ' '; }
+
+clone
+[[ -z $(changed 4) ]] || fail "identical trees differ"
+fp "$t/a" 2 | grep -qx '[0-9a-f]\{64\}  opt/we|ird &name' || fail "odd name lost"
+
+echo changed > "$t/b/opt/elan/toolchains/lean/lib/a.olean"
+[[ $(changed 3) == "opt opt/elan opt/elan/toolchains " ]] || fail "deep content change: $(changed 3)"
+[[ $(changed 6) == "opt opt/elan opt/elan/toolchains opt/elan/toolchains/lean opt/elan/toolchains/lean/lib opt/elan/toolchains/lean/lib/a.olean " ]] \
+  || fail "deep content change at depth 6: $(changed 6)"
+
+clone; chmod 0755 "$t/b/usr/bin/x"
+[[ $(changed 3) == "usr usr/bin usr/bin/x " ]] || fail "mode change: $(changed 3)"
+
+clone; ln -sfn ../usr/bin/y "$t/b/opt/link"
+[[ $(changed 2) == "opt opt/link " ]] || fail "link target change: $(changed 2)"
+
+# fs-fingerprint-drift.sh names the deepest differing paths, odd names whole.
+clone; echo changed > "$t/b/opt/elan/toolchains/lean/lib/a.olean"; echo x > "$t/b/opt/we|ird &name"
+rm "$t/b/usr/bin/x"
+fp "$t/a" 9 > "$t/fa"; fp "$t/b" 9 > "$t/fb"
+leaves=$(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fb" | tr "\n" "|")
+[[ $leaves == "opt/elan/toolchains/lean/lib/a.olean|opt/we|ird &name|usr/bin/x|" ]] || fail "drift leaves: $leaves"
+[[ -z $(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fa") ]] || fail "self-drift not empty"
+
+if echo | bash "$here/fs-fingerprint.sh" 0 2>/dev/null; then fail "depth 0 accepted"; fi
+echo "PASS: fs-fingerprint names exactly the changed paths (content, mode, link target)"

From 4d9dfcf56b12d68b13caa384bfe2ce97bead8214 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 16:00:55 +0000
Subject: [PATCH 7/7] fix(ci): fingerprint names are data, never shell; review
 fixes for CI-4

Security. scripts/ci/fs-fingerprint.sh put image paths into a shell
command, the sed in each directory group's hash pipeline. A file named
`a$(touch PWNED)` in an image therefore ran on the runner. The new
self-test shows the old script running it. The script now reads names
and link targets from tar's C-quoted listing, which keeps spaces, tabs,
quotes and newlines as escapes. Content digests are matched to entries
by archive order, and the --to-command never sees a name. Directory
digests are computed over numbered group files, so no path is ever
passed as code.

This also fixes, from the same review:
- hard links ("link to") are parsed apart, not merged into the name;
- whitespace in names and link targets is kept exactly;
- tab names no longer collide.
The self-test adds injection (`$(...)` and backticks), quote, hard-link,
link-target-whitespace and tab cases. It also checks that owners and
mtimes do not change the fingerprint. A run over /usr/share gives the
same 15,728 lines as before, in 60s instead of 105s.

container-ci:
- the path filters now cover every input the Containerfile copies
  (build.rs, build_support, crates, benches, src/interfaces) and the
  fingerprint drift and test scripts;
- container-build runs the fingerprint self-test on every run.

install-isabelle.sh: each mirror gets a bounded budget
(--connect-timeout 20, --max-time 420, --retry-max-time 420), so a
stalled first mirror cannot use up the job before the fallbacks run.

check-allow-fail-expiry.sh: an explicit empty --today is rejected and
no longer falls back to FAKE_DATE. There is a new regression case in
test-issue-regressions.sh.

Docs: the chapel decision record marks its pre-#455 allow-fail guidance
as superseded. STATE.adoc, TODO.adoc and manifests/live-provers.scm no
longer describe the retired T4 quarterly jobs as running.

Checked locally: test-fs-fingerprint.sh and test-issue-regressions.sh
(mikefarah yq v4.44.6) pass; actionlint 1.7.7 and shellcheck are clean.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw
---
 .github/workflows/container-ci.yml            |  21 +++
 .../2026-05-30-chapel-rehabilitation.adoc     |   6 +
 docs/handover/STATE.adoc                      |   9 +-
 docs/handover/TODO.adoc                       |   3 +-
 manifests/live-provers.scm                    |   3 +-
 scripts/ci/check-allow-fail-expiry.sh         |   2 +-
 scripts/ci/fs-fingerprint.sh                  | 121 ++++++++++--------
 scripts/ci/install-isabelle.sh                |   4 +-
 scripts/ci/test-fs-fingerprint.sh             |  29 ++++-
 scripts/ci/test-issue-regressions.sh          |   7 +
 10 files changed, 144 insertions(+), 61 deletions(-)

diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 39c53d86..007020c4 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -36,6 +36,14 @@ on:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
       - 'scripts/ci/fs-fingerprint.sh'
+      - 'scripts/ci/fs-fingerprint-drift.sh'
+      - 'scripts/ci/test-fs-fingerprint.sh'
+      # Everything the Containerfile copies into the image (lines 26-42).
+      - 'build.rs'
+      - 'build_support/**'
+      - 'crates/**'
+      - 'benches/**'
+      - 'src/interfaces/**'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -46,6 +54,14 @@ on:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
       - 'scripts/ci/fs-fingerprint.sh'
+      - 'scripts/ci/fs-fingerprint-drift.sh'
+      - 'scripts/ci/test-fs-fingerprint.sh'
+      # Everything the Containerfile copies into the image (lines 26-42).
+      - 'build.rs'
+      - 'build_support/**'
+      - 'crates/**'
+      - 'benches/**'
+      - 'src/interfaces/**'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -82,6 +98,11 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v7.0.1
 
+      # The fingerprint and drift scripts are exercised on every run, not only
+      # when two builds differ.
+      - name: Test filesystem fingerprints
+        run: bash scripts/ci/test-fs-fingerprint.sh
+
       - name: Install Podman
         run: |
           sudo apt-get update -q
diff --git a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
index c57f18c3..ad394b2f 100644
--- a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
+++ b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
@@ -88,6 +88,9 @@ indicate a genuine regression. `+rust-chapel-real+` stays allow-fail
 because the Rust-side link of the full Chapel runtime is a different
 scope (gated on the PIC-runtime work above and on the static-archive
 integration in `+build.zig+`).
+_Superseded 2026-11-09:_ `+rust-chapel-real+` is blocking. The real link
+landed with #455 as a static link (see the update under *Negative* below);
+the PIC rebuild now concerns shared-library output only.
 
 === Rollout
 
@@ -104,6 +107,9 @@ recipes: `+chapel-build+`, `+chapel-smoke+`, `+chapel-test+`.
 Wave 2 (separate PR, after Wave 1 green-on-main for ≥7 days): - Rebuild
 Chapel from source with `+CHPL_LIB_PIC=pic+` runtime; revert the
 metalayer build to `+--dynamic+`; flip `+rust-chapel-real+` to strict.
+_Superseded 2026-11-09:_ `+rust-chapel-real+` was made strict without the
+PIC rebuild (static link, #455); the PIC rebuild remains relevant only for
+shared-library output.
 Recipe + tradeoffs:
 link:./2026-05-30-chapel-pic-rebuild.md[2026-05-30-chapel-pic-rebuild.adoc].
 CI flip deferred — the ~30 min source build dominates the chapel-ci
diff --git a/docs/handover/STATE.adoc b/docs/handover/STATE.adoc
index ad35ee19..2cd0f96d 100644
--- a/docs/handover/STATE.adoc
+++ b/docs/handover/STATE.adoc
@@ -77,8 +77,9 @@ CI-unverified |`+9a4aeeb+`, `+6717b12+`
 OR-Tools, HOL4, ACL2, Twelf, Metamath). Needs per-backend Containerfiles
 (Podman). |*SCAFFOLD ONLY* — handover hints in STATE.a2ml |—
 
-|Wave-4 |Tier-4 quarterly, 19 backends. Retained as mock-only unless a
-maintainer volunteers. |*SCAFFOLD ONLY* |—
+|Wave-4 |Tier-4, 19 backends, mock-only. The quarterly CI placeholder jobs
+were removed 2026-11-09 (CI-4, #416); a backend returns to CI in a blocking
+job once it has a Containerfile. |*SCAFFOLD ONLY* |—
 |===
 
 Local verification of Wave-1 + Wave-2: *18/18 live tests pass* (13 real
@@ -135,8 +136,8 @@ Baseline smoke.
 FFI bridge. *Does not feed into dispatch* and *does not link real
 Chapel*; tests run against bundled stubs only.
 * `+.github/workflows/live-provers.yml+` — tiered workflow (T1 PR, T2
-nightly, T3 weekly, T4 quarterly). T1 + T2 matrices filled with real
-provisioning; T3 + T4 placeholder jobs.
+nightly, T3 weekly). T1 + T2 matrices filled with real provisioning. The
+T4 quarterly placeholder jobs were removed 2026-11-09 (CI-4, #416).
 * `+.github/workflows/agda-meta-checker.yml+` — formally-verified
 trust-pipeline properties.
 
diff --git a/docs/handover/TODO.adoc b/docs/handover/TODO.adoc
index 251f5420..181c9f73 100644
--- a/docs/handover/TODO.adoc
+++ b/docs/handover/TODO.adoc
@@ -384,7 +384,8 @@ acceptance run.
 
 *P1 L3 finishers:* Wave-3 ✅ DONE & consolidated to one
 `+Containerfile.wave3+` (2026-05-18; see Wave-3 section above), Wave-4
-✅ (19 placeholder + rationale docs in STATE.a2ml). L3 P1 finisher work
+✅ (19 backends documented as mock-only in STATE.a2ml; the CI placeholder
+jobs were removed 2026-11-09, CI-4 #416). L3 P1 finisher work
 is complete; the L3→L1 hand-off remains gated only on the calendar/infra
 gate (Tier-1 green ≥7 days on main — blocked by main CI stuck
 `+queued/+`, infra-owned, not collapsible here).
diff --git a/manifests/live-provers.scm b/manifests/live-provers.scm
index b73d503a..f63c548f 100644
--- a/manifests/live-provers.scm
+++ b/manifests/live-provers.scm
@@ -22,7 +22,8 @@
 ;;   T1 — trivial (apt/Guix single-package)       — run on every PR
 ;;   T2 — build-from-source                       — run nightly
 ;;   T3 — container / special env                 — run weekly
-;;   T4 — niche / best-effort                     — run quarterly, allow-fail
+;;   T4 — niche / best-effort                     — no CI job (quarterly
+;;        allow-fail jobs retired 2026-11-09, CI-4 #416; mock-only)
 ;;
 ;; Policy (estate ruling 2026-05-18 + estate-wide nix-deprecation 2026-06-01):
 ;;   Guix is the PRIMARY (and only) package-management path declared here.
diff --git a/scripts/ci/check-allow-fail-expiry.sh b/scripts/ci/check-allow-fail-expiry.sh
index 2fcc9e08..aae13c38 100755
--- a/scripts/ci/check-allow-fail-expiry.sh
+++ b/scripts/ci/check-allow-fail-expiry.sh
@@ -35,7 +35,7 @@ dirs=()
 
 while [ $# -gt 0 ]; do
   case "$1" in
-    --today) [ $# -ge 2 ] || { echo "--today needs a value" >&2; exit 2; }; today="$2"; shift 2 ;;
+    --today) { [ $# -ge 2 ] && [ -n "$2" ]; } || { echo "--today needs a non-empty value" >&2; exit 2; }; today="$2"; shift 2 ;;
     --warn-days) [ $# -ge 2 ] || { echo "--warn-days needs a value" >&2; exit 2; }; warn_days="$2"; shift 2 ;;
     -h|--help) sed -n '3,25p' "$0"; exit 0 ;;
     --) shift; dirs+=("$@"); break ;;
diff --git a/scripts/ci/fs-fingerprint.sh b/scripts/ci/fs-fingerprint.sh
index a986294a..331eb059 100755
--- a/scripts/ci/fs-fingerprint.sh
+++ b/scripts/ci/fs-fingerprint.sh
@@ -2,21 +2,26 @@
 # SPDX-License-Identifier: MPL-2.0
 # fs-fingerprint.sh DEPTH < image.tar
 #
-# Reads a filesystem tar stream (`podman export`) on stdin. It prints one
+# Reads a filesystem tar stream (`podman export`) on stdin and prints one
 # line, "<sha256>  <path>", for every path at most DEPTH components deep.
-# A regular file's digest covers its content and mode. A symlink's covers
-# its target. A directory's covers the entries beneath it (type, mode,
-# path, and content digest or link target).
+# A regular file's digest covers its content and permissions; a symlink's
+# or hard link's covers its target; a directory's covers every entry beneath
+# it (type, permissions, path, and content digest or link target).
 #
-# Two builds whose image IDs differ can then be compared path by path.
-# The paths whose digests differ name where the drift is, not just which
-# layer. Nothing is extracted to disk: file contents are hashed as they
-# stream past (GNU tar --to-command). Owners and timestamps are left out,
-# since `podman build --timestamp` already fixes the times.
+# Comparing two builds path by path then names where they drift, not only
+# which layer. Nothing is extracted: content is hashed as it streams past.
+# Owners and timestamps are deliberately left out (`podman build
+# --timestamp` fixes the times; owners are not what reproducibility means).
+#
+# Names are untrusted (they come from an image). They are never put into a
+# shell command: names and link targets are read from tar's C-quoted
+# listing, which is lossless (spaces, tabs, quotes and newlines survive as
+# escapes), content digests are matched to entries by archive order, and
+# directory digests are computed over numbered group files.
 set -euo pipefail
 depth=${1:?usage: fs-fingerprint.sh DEPTH < image.tar}
 [[ $depth =~ ^[1-9][0-9]*$ ]] || { echo "fs-fingerprint: DEPTH must be a positive integer" >&2; exit 2; }
-for tool in tar sha256sum awk sort; do
+for tool in tar sha256sum awk sort join xargs; do
   command -v "$tool" >/dev/null || { echo "fs-fingerprint: $tool missing" >&2; exit 2; }
 done
 tar --version | head -n 1 | grep -q 'GNU tar' || { echo "fs-fingerprint: GNU tar required" >&2; exit 2; }
@@ -24,55 +29,69 @@ tar --version | head -n 1 | grep -q 'GNU tar' || { echo "fs-fingerprint: GNU tar
 work=$(mktemp -d)
 trap 'rm -rf -- "$work"' EXIT
 mkfifo "$work/stream"
+export LC_ALL=C
 
-# One pass for listings (types, modes, link targets) and one for content
-# hashes: tee splits the single input stream so it is read only once.
-# The single quotes are deliberate: tar runs the command, which expands them.
-# shellcheck disable=SC2016
-tee "$work/stream" < /dev/stdin \
-  | tar -x --to-command='printf "%s %s %s\n" "$(sha256sum | cut -d" " -f1)" "$TAR_MODE" "$TAR_FILENAME"' \
-      -f - > "$work/files" &
+# Single read of stdin, split two ways. The --to-command runs once per
+# regular file in archive order and prints only that file's digest: the
+# file name is not used, so it cannot be interpreted.
+tee "$work/stream" \
+  | tar -x --to-command='sha256sum | cut -c1-64' -f - > "$work/digests" &
 hasher=$!
-# --quoting-style=escape keeps one entry per line whatever the names hold.
-tar --quoting-style=escape -tv --numeric-owner -f - < "$work/stream" > "$work/listing"
+tar --quoting-style=c -tv --numeric-owner -f - < "$work/stream" > "$work/listing"
 wait "$hasher"
 
-# Manifest: "<path>\t<type>\t<mode-or-perm>\t<digest-or-target>", path
-# normalised to no leading "./" or "/". Regular files come from the hash
-# pass; directories and symlinks from the listing.
-awk '{ p = $0; sub(/^[^ ]+ [^ ]+ /, "", p); sub(/^\.?\//, "", p); if (p != "") printf "%s\tf\t%s\t%s\n", p, $2, $1 }' "$work/files" > "$work/manifest"
-awk '
+# Manifest rows: "<path>\t<type>\t<perms>\t<digest-or-target>", where path
+# and target keep tar's C escapes (no raw tab or newline can occur), with a
+# leading "./" or "/" removed. Regular files take the next digest in order.
+awk -v digests="$work/digests" '
+  # The i-th C-quoted string ("...", with \" escapes) on the line.
+  function quoted(s, which,    i, c, n, start, out, inq) {
+    n = 0; inq = 0; out = ""
+    for (i = 1; i <= length(s); i++) {
+      c = substr(s, i, 1)
+      if (!inq) { if (c == "\"") { inq = 1; out = "" } continue }
+      if (c == "\\") { out = out c substr(s, i + 1, 1); i++; continue }
+      if (c == "\"") { inq = 0; if (++n == which) return out; continue }
+      out = out c
+    }
+    return ""
+  }
+  function clean(p) { sub(/^\.?\//, "", p); sub(/\/$/, "", p); return p }
   {
     t = substr($1, 1, 1); perm = substr($1, 2)
-    # Fields: perms owner size date time name [-> target]
-    name = ""; for (i = 6; i <= NF; i++) { if ($i == "->") break; name = name (name == "" ? "" : " ") $i }
-    target = ""; for (j = i + 1; j <= NF; j++) target = target (target == "" ? "" : " ") $j
-    sub(/^\.?\//, "", name); sub(/\/$/, "", name)
-    if (name == "") next
-    if (t == "d") printf "%s\td\t%s\t-\n", name, perm
-    else if (t == "l") printf "%s\tl\t%s\t%s\n", name, perm, target
-    else if (t == "h") printf "%s\th\t%s\t%s\n", name, perm, target
-  }' "$work/listing" >> "$work/manifest"
-LC_ALL=C sort -t "$(printf '\t')" -k1,1 -o "$work/manifest" "$work/manifest"
+    name = clean(quoted($0, 1))
+    if (t == "-" || t == "C") {
+      if ((getline d < digests) <= 0) { print "fs-fingerprint: fewer digests than files" > "/dev/stderr"; exit 3 }
+      if (name != "") printf "%s\tf\t%s\t%s\n", name, perm, d
+    }
+    else if (name == "") next
+    else if (t == "d") printf "%s\td\t%s\t-\n", name, perm
+    else if (t == "l") printf "%s\tl\t%s\t%s\n", name, perm, quoted($0, 2)
+    else if (t == "h") printf "%s\th\t%s\t%s\n", name, perm, clean(quoted($0, 2))
+    else printf "%s\t%s\t%s\t-\n", name, t, perm
+  }
+  END { if ((getline d < digests) > 0) { print "fs-fingerprint: more digests than files" > "/dev/stderr"; exit 3 } }
+' "$work/listing" | sort -t "$(printf '\t')" -k1,1 > "$work/manifest"
 
-# For every path up to DEPTH: a file/link digests its own row; a directory
-# digests every row at or beneath it. One awk pass emits "prefix\trow"
-# pairs; grouping and hashing happen per prefix.
-awk -v depth="$depth" -F '\t' '
+# Every row is credited to each ancestor prefix up to DEPTH. awk writes
+# each prefix's rows to a numbered file (the number, not the name, is the
+# file name) and an index "number<TAB>prefix"; sha256sum then hashes the
+# numbered files, and join maps digests back to prefixes.
+mkdir "$work/g"
+awk -v depth="$depth" -v dir="$work/g" -F '\t' '
   {
-    n = split($1, part, "/")
-    prefix = ""
+    n = split($1, part, "/"); prefix = ""
     for (k = 1; k <= n && k <= depth; k++) {
       prefix = prefix (k == 1 ? "" : "/") part[k]
-      print prefix "\t" $0
+      if (!(prefix in id)) { id[prefix] = ++count; printf "%d\t%s\n", count, prefix > (dir "/index") }
+      print $0 >> (dir "/" id[prefix])
+      # Keep the number of open files bounded on large images.
+      close(dir "/" id[prefix])
     }
-  }' "$work/manifest" | LC_ALL=C sort -t "$(printf '\t')" -k1,1 -s > "$work/pairs"
-
-awk -F '\t' '
-  function flush() { if (cur != "") { close(cmd); } }
-  {
-    if ($1 != cur) { flush(); cur = $1; esc = cur; gsub(/[\\|&]/, "\\\\&", esc); cmd = "sha256sum | cut -c1-64 | sed \"s|$|  " esc "|\"" }
-    line = $2; for (i = 3; i <= NF; i++) line = line "\t" $i
-    print line | cmd
-  }
-  END { flush() }' "$work/pairs" | LC_ALL=C sort -k2
+  }' "$work/manifest"
+[[ -s "$work/g/index" ]] || exit 0
+(cd "$work/g" && find . -maxdepth 1 -type f ! -name index -printf '%f\0' \
+   | xargs -0 sha256sum | awk '{ print $2 "\t" $1 }' | sort -t "$(printf '\t')" -k1,1) > "$work/sums"
+sort -t "$(printf '\t')" -k1,1 "$work/g/index" \
+  | join -t "$(printf '\t')" -o 2.2,1.2 - "$work/sums" \
+  | awk -F '\t' '{ print $1 "  " $2 }' | sort -k2
diff --git a/scripts/ci/install-isabelle.sh b/scripts/ci/install-isabelle.sh
index 5683939f..558a1c3e 100755
--- a/scripts/ci/install-isabelle.sh
+++ b/scripts/ci/install-isabelle.sh
@@ -35,8 +35,8 @@ fetched=""
 for url in "${MIRRORS[@]}"; do
   echo "install-isabelle: trying $url"
   rm -f "$dest"
-  if curl --proto '=https' --proto-redir '=https' -fL --max-time 900 \
-       --retry 3 --retry-delay 15 --retry-all-errors -o "$dest" "$url" \
+  if curl --proto '=https' --proto-redir '=https' -fL --connect-timeout 20 --max-time 420 \
+       --retry 2 --retry-delay 10 --retry-max-time 420 --retry-all-errors -o "$dest" "$url" \
      && printf '%s  %s\n' "$SHA256" "$dest" | sha256sum --check --status; then
     fetched="$url"
     break
diff --git a/scripts/ci/test-fs-fingerprint.sh b/scripts/ci/test-fs-fingerprint.sh
index 785594a8..6615833f 100755
--- a/scripts/ci/test-fs-fingerprint.sh
+++ b/scripts/ci/test-fs-fingerprint.sh
@@ -44,4 +44,31 @@ leaves=$(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fb" | tr "\n" "|")
 [[ -z $(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fa") ]] || fail "self-drift not empty"
 
 if echo | bash "$here/fs-fingerprint.sh" 0 2>/dev/null; then fail "depth 0 accepted"; fi
-echo "PASS: fs-fingerprint names exactly the changed paths (content, mode, link target)"
+# Untrusted names never reach a shell: a name that is a command substitution
+# stays data, and nothing runs.
+clone; touch "$t/b/opt/a\$(touch PWNED)" "$t/b/opt/a\`touch PWNED\`" "$t/b/opt/q\"uote's"
+# Run from a scratch directory, where an injected relative `touch` would land.
+mkdir -p "$t/cwd"
+(cd "$t/cwd" && fp "$t/b" 3) > "$t/fb" 2>/dev/null
+[[ ! -e "$t/cwd/PWNED" && ! -e "$t/b/PWNED" ]] || fail "a file name was executed"
+grep -qF "opt/q\\\"uote's" "$t/fb" || fail "quote in a name lost"
+grep -qF "opt/a\$(touch" "$t/fb" || fail "command-substitution name lost"
+
+# Hard links: the name and its target are parsed apart ("link to").
+clone; ln "$t/b/usr/bin/x" "$t/b/usr/bin/hard"
+fp "$t/b" 3 | grep -qx "[0-9a-f]\{64\}  usr/bin/hard" || fail "hard link name mis-parsed"
+
+# Whitespace inside a link target and a tab inside a name are lossless.
+clone; ln -sfn "target value" "$t/a/opt/sp"; ln -sfn "target  value" "$t/b/opt/sp"
+[[ $(changed 2) == *"opt/sp "* ]] || fail "double space in a link target not detected"
+clone; touch "$t/a/opt/tab$(printf '\t')a" "$t/b/opt/tab$(printf '\t')b"
+[[ $(fp "$t/a" 2 | grep -c 'opt/tab\\ta$') == 1 && $(changed 2) == *"opt/tab\\tb"* ]] \
+  || fail "tab names collided or were truncated: $(changed 2)"
+
+# Owners and timestamps are not part of the fingerprint.
+clone
+A=$( (cd "$t/a" && tar --sort=name --owner=0 --group=0 --mtime=@0 -cf - .) | bash "$here/fs-fingerprint.sh" 4)
+B=$( (cd "$t/b" && tar --sort=name --owner=4242 --group=4242 --mtime=@1700000000 -cf - .) | bash "$here/fs-fingerprint.sh" 4)
+[[ "$A" == "$B" ]] || fail "owner or mtime changed the fingerprint"
+
+echo "PASS: fs-fingerprint names exactly the changed paths (content, mode, link target, hard links); names stay data; owners and times are ignored"
diff --git a/scripts/ci/test-issue-regressions.sh b/scripts/ci/test-issue-regressions.sh
index b1433f7a..4c404e01 100644
--- a/scripts/ci/test-issue-regressions.sh
+++ b/scripts/ci/test-issue-regressions.sh
@@ -110,6 +110,13 @@ fi
 grep -q 'allow-fail units checked: 1$' "$tmp/allow-fail.log"
 grep -q 'units.yml:7: continue-on-error without' "$tmp/allow-fail.log"
 
+# An explicit empty --today is an error, not a fall-back to FAKE_DATE (an
+# earlier FAKE_DATE would otherwise accept an expired unit).
+rc=0
+FAKE_DATE=2020-01-01 bash scripts/ci/check-allow-fail-expiry.sh --today "" "$tmp/allow-fail" \
+  > /dev/null 2>&1 || rc=$?
+[ "$rc" -eq 2 ] || { echo "FAIL: empty --today gave exit $rc, expected 2" >&2; exit 1; }
+
 # Managed workflows start with an actions-lock comment, not the SPDX header.
 # Inspect the comment preamble rather than assuming the licence is line one.
 # Top-level `permissions` is read with yq (YAML-POLICY Y-1): in KYAML it is