ci(kernel-proofs): Agda 2.6.4.3 and the PROOF-POLICY §2.1 invocation

.github/workflows/contract-gate.yml

@@ -48,30 +48,34 @@
 
   # The mechanical falsifiers behind the kernel: Idris2 0.8.0 builds the ABI,
   # refuses tests/reject/*.idr for the intended reasons, and agrees with the
-  # PINNED Agda kernel (resource-algebra at the fetch-siblings.sh pin, Agda --safe --without-K)
+  # PINNED Agda kernel (resource-algebra at the fetch-siblings.sh pin, Agda
+  # --safe --without-K --cubical-compatible, PROOF-POLICY §2.1)
   # on tests/transcription/ops.tsv; both provers refuse the wrong rows.
   # Idris2 publishes no binaries and its release-tarball URL 404s (see
   # e2e.yml build-e2e), so 0.8.0 is built from source with Chez Scheme,
   # fetched by the commit its v0.8.0 tag names (a tag can move; the SHA
   # cannot).
   kernel-proofs:
     name: Grade kernel proofs (Idris2 0.8.0 + Agda)
-    # Pinned: the job installs Agda from apt, so the image decides the Agda
-    # version, and the reject checks need 2.6.3 (tools/check-kernel-proofs.sh
-    # refuses any other). ubuntu-latest moved to 26.04 (Agda 2.8.0) on
-    # 2026-10-19.
-    runs-on: ubuntu-24.04
+    # Agda 2.6.4.3, the Debian agda-bin package the sibling repositories pin
+    # (resource-algebra, occupancy-types and choreographic-types proofs.yml),
+    # so this gate re-checks their proofs on the prover their own CI uses.
+    # tools/check-kernel-proofs.sh refuses any other Agda. Until 2026-11-09
+    # this job ran Ubuntu 24.04's Agda 2.6.3.
+    runs-on: ubuntu-latest
+    container: debian:trixie-slim
     timeout-minutes: 40
     env:
       IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df  # v0.8.0
     steps:
+      - name: Install Chez Scheme, GMP, build tools and the pinned Agda
+        run: |
+          apt-get update -qq
+          apt-get install --no-install-recommends -y -qq ca-certificates git make gcc libc6-dev \
+            libgmp-dev chezscheme agda-bin=2.6.4.3-1+b2
+          test "$(agda --version)" = 'Agda version 2.6.4.3'
       - name: Checkout
         uses: actions/checkout@v7.0.1
-      - name: Install Chez Scheme, GMP and Agda
-        run: |
-          sudo apt-get update -qq
-          sudo apt-get install -y -qq chezscheme libgmp-dev agda-bin
-          agda --version
       - name: Build Idris2 0.8.0 from source
         run: |
           git init --quiet "$RUNNER_TEMP/idris2-src"
@@ -81,7 +85,9 @@
           # Local tag on the verified commit, so the Makefile reports the
           # release version (0.8.0) rather than 0.8.0-<sha>.
           git -C "$RUNNER_TEMP/idris2-src" tag v0.8.0
-          make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \
+          # Debian names the Chez binary chezscheme; Ubuntu also ships scheme.
+          SCHEME="$(command -v chezscheme || command -v scheme)"
+          make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME="$SCHEME" -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \
             || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; }
           make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \
             || { tail -60 "$RUNNER_TEMP/idris2-install.log"; exit 1; }

CHANGELOG.adoc

@@ -9,18 +9,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
-==== CI: standards re-pinned to metadatastician @ `e064539` (2026-11-09)
-
-* The five standards reusables (governance, hypatia-scan, mirror, scorecard,
-  secret-scanner) move from `hyperpolymath/standards@da2c748` to
-  `metadatastician/standards@e064539`, the commit panll runs green
-  (hyperpolymath/panll#171). At `da2c748` all five failed at startup on
-  every push, so the required `scan / gitleaks` check never reported.
-* `governance.yml` and `mirror.yml` grant `actions: read`, which both
-  reusables declare at workflow level at `e064539`.
-* `mirror.yml` passes the seven forge keys the reusable declares by name,
-  and `secret-scanner.yml` passes none (its reusable declares none), instead
-  of `secrets: inherit`, which handed every repository secret to the callee.
+==== Kernel-proofs gate on Agda 2.6.4.3, PROOF-POLICY §2.1 flags (2026-11-09)
+
+* The `kernel-proofs` job (Contract Gate) runs in `debian:trixie-slim` with
+  `agda-bin=2.6.4.3-1+b2`, the prover resource-algebra, occupancy-types and
+  choreographic-types pin in their own CI, so this gate re-checks their
+  proofs on the same Agda. It ran Ubuntu 24.04's 2.6.3 before.
+  `tools/check-kernel-proofs.sh` refuses any Agda but 2.6.4.3.
+* The gate's own Agda checks (choreographic-types' KCut slice and rejects,
+  the transcription table, the negative controls) run under
+  `--safe --without-K --cubical-compatible`, PROOF-POLICY §2.1's canonical
+  invocation, and with `LC_ALL=C.UTF-8`: Agda stops with exit 42 on
+  Unicode warnings without a UTF-8 locale.
 
 ==== L15-C at the front-end: a caller's caps contain its callee's (2026-10-27)
 

tools/check-kernel-proofs.sh

@@ -4,9 +4,11 @@
 #
 # check-kernel-proofs.sh — the mechanical falsifiers behind the grade kernel.
 #
-#   1. upstream   resource-algebra's and occupancy-types' own checks, and
-#                 choreographic-types' KCut slice, at the pins (Agda --safe
-#                 --without-K --no-libraries --double-check + their rejects)
+#   1. upstream   resource-algebra's and occupancy-types' own checks at the
+#                 pins (each repository's own scripts and flags), and
+#                 choreographic-types' KCut slice and rejects under
+#                 AGDA_FLAGS (--safe --without-K --cubical-compatible
+#                 --no-libraries --double-check)
 #   2. build      idris2 --build src/abi/typed-wasm.ipkg: exit 0 AND no
 #                 `Error:` line (idris2 can exit 0 while printing an error)
 #   3. rejects    every tests/reject/*.idr must FAIL, at its `invalid`
@@ -32,7 +34,12 @@ REGEN=0; [ "${1:-}" = "--regen" ] && REGEN=1
 RA="_build/dependencies/resource-algebra"
 OUT="_build/kernel-proofs"
 TTC="$ROOT/src/abi/build/ttc"
-AGDA_FLAGS=(--safe --without-K --no-libraries --double-check --ignore-interfaces)
+# PROOF-POLICY §2.1: the canonical theory invocation is
+# --safe --without-K --cubical-compatible.
+AGDA_FLAGS=(--safe --without-K --cubical-compatible --no-libraries --double-check --ignore-interfaces)
+# Agda prints its (Unicode) warnings through the locale; without UTF-8 it
+# stops with exit 42 instead, as the sibling scripts also guard against.
+export LC_ALL="${LC_ALL:-C.UTF-8}"
 WRONG_REASON='Undefined name|Couldn.t parse|Parse error|not in the source directory|Can.t find import|Module .* not found|INTERNAL ERROR|Not in scope|Failed to find'
 
 fail=0
@@ -49,11 +56,12 @@ case "$iv" in
   *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (src/abi targets 0.8.0; EXPECT messages are 0.8.0's). Set ALLOW_ANY_IDRIS2=1 to try another." ;;
 esac
 # The rejection checks match prover messages and locations, and both change
-# between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed
+# between Agda releases: 2.8.0 prints `file:11.38` where 2.6.x printed
 # `file:11,38`, which occupancy-types' own reject check does not accept.
+# 2.6.4.3 is the Debian agda-bin the siblings' own CI pins.
 case "$av" in
-  "Agda version 2.6.3") ;;  # the whole line: 2.6.3.1 is another release
-  *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;;
+  "Agda version 2.6.4.3") ;;  # the whole line: another point release is another prover
+  *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.4.3 required (the siblings' CI and their reject checks use it). Set ALLOW_ANY_AGDA=1 to try another." ;;
 esac
 [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh"
 echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)"