fix(proofs): restore the proof gate (dedupe allTake, read idris2 pin, run on every PR)

.github/workflows/proofs.yml

@@ -11,29 +11,23 @@
 # ever ran `idris2 --typecheck` on cartridges/**/abi in CI (the Justfile's old
 # `typecheck` recipe covered only 5 of ~50 cartridge ABIs and was never wired
 # into a workflow). This gate type-checks the core ABI package AND every
-# cartridge ABI under the pinned toolchain (.tool-versions → idris2 0.8.0), and
+# cartridge ABI under the pinned toolchain (.mise.toml → idris2), and
 # runs the trusted-base audit so no new believe_me / axiom slips in.
 name: Proofs Gate
 
-# Was workflow-level path-filtered: a required check that never ran on PRs
-# touching none of its paths, leaving the check "Expected" and the PR blocked.
-# Now always runs; the `changes` job gates the heavy jobs, which when skipped
-# report SUCCESS to required checks.
+# Runs on every PR and push to main, with no path filter and no `changes`
+# gate. A path-skipped proof job reports success without checking anything,
+# which is how a duplicate `allTake` in SafetyLemmas.idr sat in main behind a
+# green gate (#343, DEBT P-1). This workflow is not a required check, so always
+# running it blocks nothing.
 on:
   push:
     branches: [main]
   pull_request:
     branches: [main]
   workflow_dispatch:
-  # Weekly baseline re-verification of main. The `changes` path-filter below
-  # skips the heavy type-check on PRs/pushes that don't touch src/abi/** (so an
-  # off-path PR isn't blocked and doesn't pay for a 45-min Idris2 build). The
-  # side effect is that a proof break ALREADY living in main — merged before
-  # this gate existed, or via a path the filter ignores — is otherwise never
-  # re-detected. On a `schedule` event the detect step leaves run=true (its
-  # default), so the full core + every-cartridge type-check runs unconditionally
-  # and catches such drift. (This is exactly how a duplicate `allTake` in
-  # SafetyLemmas.idr sat in main with a green gate — see PR fixing it.)
+  # Weekly re-verification of main, so toolchain or runner drift is caught
+  # even when nothing is merged.
   schedule:
     - cron: '17 6 * * 1'   # Mondays 06:17 UTC
 
@@ -46,40 +40,9 @@ concurrency:
   cancel-in-progress: ${{ github.event_name == 'pull_request' }}
 
 jobs:
-  changes:
-    name: Detect relevant changes
-    runs-on: ubuntu-latest
-    timeout-minutes: 5
-    outputs:
-      run: ${{ steps.detect.outputs.run }}
-    steps:
-      - uses: actions/checkout@v6.0.2
-        with:
-          fetch-depth: 0
-      - id: detect
-        env:
-          EVENT: ${{ github.event_name }}
-          BASE: ${{ github.base_ref }}
-          BEFORE: ${{ github.event.before }}
-        run: |
-          set -uo pipefail
-          run=true
-          if [ "$EVENT" = pull_request ]; then
-            git fetch --no-tags --depth=200 origin "$BASE" 2>/dev/null \
-              && changed=$(git diff --name-only "origin/${BASE}...HEAD" 2>/dev/null) \
-              && { printf '%s\n' "$changed" | grep -qE '^src/abi/|^verification/|^scripts/check-trusted-base\.sh$|^scripts/typecheck-proofs\.sh$|^\.tool-versions$' && run=true || run=false; }
-          elif [ "$EVENT" = push ] && [ -n "$BEFORE" ] && [ "$BEFORE" != 0000000000000000000000000000000000000000 ]; then
-            changed=$(git diff --name-only "${BEFORE}...${GITHUB_SHA}" 2>/dev/null) \
-              && { printf '%s\n' "$changed" | grep -qE '^src/abi/|^verification/|^scripts/check-trusted-base\.sh$|^scripts/typecheck-proofs\.sh$|^\.tool-versions$' && run=true || run=false; }
-          fi
-          printf 'run=%s\n' "$run" >> "$GITHUB_OUTPUT"
-          echo "relevant=$run; changed files:"; printf '%s\n' "${changed:-<none computed>}"
-
   # Cheap, dependency-free gate: scan for unsound constructs + axiom-count drift.
   trusted-base:
     name: Trusted-base audit (no new axioms)
-    needs: changes
-    if: needs.changes.outputs.run == 'true'
     runs-on: ubuntu-latest
     timeout-minutes: 10
     steps:
@@ -90,16 +53,24 @@ jobs:
   # Full type-check of the core ABI + every cartridge ABI under the pinned Idris2.
   typecheck:
     name: Idris2 type-check (core + all cartridge ABIs)
-    needs: changes
-    if: needs.changes.outputs.run == 'true'
     runs-on: ubuntu-latest
     timeout-minutes: 45
     steps:
       - uses: actions/checkout@v6.0.2
 
+      # The pin lives in .mise.toml (.tool-versions was converted, 4d1fe0c9).
+      # Fail here on an empty or malformed value rather than asking asdf to
+      # install version "".
       - name: Read pinned Idris2 version
         id: ver
-        run: echo "idris2=$(awk '/^idris2 /{print $2}' .tool-versions)" >> "$GITHUB_OUTPUT"
+        run: |
+          set -euo pipefail
+          v=$(awk -F'"' '/^idris2[[:space:]]*=/{print $2}' .mise.toml)
+          if ! printf '%s' "$v" | grep -qE '^[0-9]+\.[0-9]+\.[0-9]+$'; then
+            echo "::error file=.mise.toml::no idris2 = \"X.Y.Z\" pin found (got '$v')"
+            exit 1
+          fi
+          echo "idris2=$v" >> "$GITHUB_OUTPUT"
 
       - name: Install build deps (Chez Scheme + GMP)
         run: sudo apt-get update && sudo apt-get install -y chezscheme libgmp-dev build-essential

README.adoc

@@ -283,9 +283,8 @@ Every safety claim BoJ makes sits in one of three bins. "Proven" always means _p
 |Proven — the compiler checks it |Witnessed — an artefact backs it |Trusted — relied on from outside
 
 a|
-* *Status (2026-10-06): the core does not currently typecheck.* `SafetyLemmas.idr` defines `allTake` twice, and the CI typecheck job has not completed since at least 2026-09-21 (it fails while installing Idris2, and is path-skipped on most PRs). Tracked in link:https://github.com/hyperpolymath/boj-server/issues/343[#343]. Until that is fixed, read this column as "proven when last green", not "proven now".
 * The Idris2 ABI in `src/abi/Boj/` (17 modules, all `%default total`) covers catalogue and dispatch, HTTP/CORS/API-key/WebSocket/prompt-injection safety predicates, and the credential-isolation model.
-* `believe++_++me` appears only in *four* documented axioms over opaque `Char`/`String` primitives (`SafetyLemmas.idr`); CI (`scripts/check-trusted-base.sh`) pins that count and greps the rest of the Idris tree for `believe++_++me`, `assert++_++total`, `assert++_++smaller` and `idris++_++crash`. The grep has known gaps (a use followed by a `--` comment is skipped; `partial`, `covering` and holes are not scanned) and the job is path-filtered, so it does not run on every PR.
+* `believe++_++me` appears only in *four* documented axioms over opaque `Char`/`String` primitives (`SafetyLemmas.idr`); CI (`scripts/check-trusted-base.sh`) pins that count and greps the rest of the Idris tree for `believe++_++me`, `assert++_++total`, `assert++_++smaller` and `idris++_++crash`. The grep has known gaps (a use followed by a `--` comment is skipped; `partial`, `covering` and holes are not scanned). CI runs it, and the full typecheck, on every PR and push to `main`.
 * *Limit:* these proofs are about the Idris model. The model is only ever typechecked, never compiled or linked into the running server, and 13 of the 17 C safety checks it binds (`libbozsafety`) are not yet implemented.
 a|
 * Property tests (Elixir StreamData, `elixir/test/backend_assurance/`) of the behaviour each of the four axioms assumes, run against Elixir analogues of the Chez primitives (not the compiled Idris code); last executed and green 2026-10-06.

README.md

@@ -279,9 +279,8 @@ Every safety claim BoJ makes sits in one of three bins. "Proven" always means *p
 <tbody>
 <tr>
 <td style="text-align: left;"><ul>
-<li><p><strong>Status (2026-10-06): the core does not currently typecheck.</strong> <code>SafetyLemmas.idr</code> defines <code>allTake</code> twice, and the CI typecheck job has not completed since at least 2026-09-21 (it fails while installing Idris2, and is path-skipped on most PRs). Tracked in <a href="https://github.com/hyperpolymath/boj-server/issues/343">#343</a>. Until that is fixed, read this column as "proven when last green", not "proven now".</p></li>
 <li><p>The Idris2 ABI in <code>src/abi/Boj/</code> (17 modules, all <code>%default total</code>) covers catalogue and dispatch, HTTP/CORS/API-key/WebSocket/prompt-injection safety predicates, and the credential-isolation model.</p></li>
-<li><p><code>believe_me</code> appears only in <strong>four</strong> documented axioms over opaque <code>Char</code>/<code>String</code> primitives (<code>SafetyLemmas.idr</code>); CI (<code>scripts/check-trusted-base.sh</code>) pins that count and greps the rest of the Idris tree for <code>believe_me</code>, <code>assert_total</code>, <code>assert_smaller</code> and <code>idris_crash</code>. The grep has known gaps (a use followed by a <code>--</code> comment is skipped; <code>partial</code>, <code>covering</code> and holes are not scanned) and the job is path-filtered, so it does not run on every PR.</p></li>
+<li><p><code>believe_me</code> appears only in <strong>four</strong> documented axioms over opaque <code>Char</code>/<code>String</code> primitives (<code>SafetyLemmas.idr</code>); CI (<code>scripts/check-trusted-base.sh</code>) pins that count and greps the rest of the Idris tree for <code>believe_me</code>, <code>assert_total</code>, <code>assert_smaller</code> and <code>idris_crash</code>. The grep has known gaps (a use followed by a <code>--</code> comment is skipped; <code>partial</code>, <code>covering</code> and holes are not scanned). CI runs it, and the full typecheck, on every PR and push to <code>main</code>.</p></li>
 <li><p><strong>Limit:</strong> these proofs are about the Idris model. The model is only ever typechecked, never compiled or linked into the running server, and 13 of the 17 C safety checks it binds (<code>libbozsafety</code>) are not yet implemented.</p></li>
 </ul></td>
 <td style="text-align: left;"><ul>

site/index.html

@@ -169,7 +169,7 @@ <h2 id="about-h">What BoJ does</h2>
     <h2 id="proven-h">What is proven, witnessed, and trusted</h2>
     <p>"Proven" here means proven about a model. Each claim sits in one of three bins.</p>
     <div class="grid">
-      <div class="card-flat"><strong>Proven</strong><p>An Idris2 model of the safety predicates, catalogue, dispatch and credential isolation, total, with four documented axioms. It does not typecheck at the moment (a duplicate lemma, and a broken CI job); the fix is tracked in <a href="https://github.com/hyperpolymath/boj-server/issues/343">#343</a>. The model is not yet linked to the running server, and 13 of the runtime checks it binds are not yet implemented.</p></div>
+      <div class="card-flat"><strong>Proven</strong><p>An Idris2 model of the safety predicates, catalogue, dispatch and credential isolation, total, with four documented axioms. CI typechecks it on every pull request. The model is not yet linked to the running server, and 13 of the runtime checks it binds are not yet implemented.</p></div>
       <div class="card-flat"><strong>Witnessed</strong><p>Property tests on the four axioms, coherence tests between advertised and dispatched tools, npm provenance, SLSA level 3 release tarballs, container attestation.</p></div>
       <div class="card-flat"><strong>Trusted</strong><p>The JavaScript bridge and Zig FFI themselves, hand-written tool annotations, cloud and forge APIs, compilers, runtimes, the OS, and the AI choosing the right tool.</p></div>
     </div>

src/abi/Boj/SafetyLemmas.idr

@@ -232,16 +232,6 @@ allNotImpliesAnyFalse {p} {xs = x :: xs'} prf with (p x) proof pEq
   allNotImpliesAnyFalse {p} {xs = x :: xs'} prf | False =
     allNotImpliesAnyFalse {xs = xs'} prf
 
-||| If `allRec p xs = True`, then `allRec p (take n xs) = True`.
-export
-allTake : {p : a -> Bool} -> {xs : List a} -> {n : Nat} ->
-          allRec p xs = True -> allRec p (take n xs) = True
-allTake {n = Z} _ = Refl
-allTake {xs = []} {n = S _} _ = Refl
-allTake {p} {xs = x :: xs'} {n = S n'} prf with (p x) proof eq
-  allTake {p} {xs = x :: xs'} {n = S n'} prf | True  = allTake {xs = xs'} {n = n'} prf
-  allTake {p} {xs = x :: xs'} {n = S n'} prf | False = absurd prf
-
 ||| Convert a Bool lte witness to LTE.
 export
 fromLteTrue : (a, b : Nat) -> (a <= b) = True -> LTE a b