From 96511e4ca0f59a6092dbf3d0d0eaeafbd62e7729 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:32:52 +0000 Subject: [PATCH] =?UTF-8?q?ci(kernel-proofs):=20Agda=202.6.4.3=20and=20the?= =?UTF-8?q?=20PROOF-POLICY=20=C2=A72.1=20invocation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The kernel-proofs job 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 instead of Ubuntu 24.04's 2.6.3. Idris2 0.8.0 is still built from source at its pinned commit; Debian names the Chez binary chezscheme, so the build finds whichever is present. tools/check-kernel-proofs.sh requires Agda 2.6.4.3, runs its own Agda checks under --safe --without-K --cubical-compatible, and sets LC_ALL=C.UTF-8: without a UTF-8 locale Agda stops with exit 42 on the Unicode warnings --cubical-compatible prints. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/contract-gate.yml | 30 +++++++++++++++++------------ CHANGELOG.adoc | 13 +++++++++++++ tools/check-kernel-proofs.sh | 22 ++++++++++++++------- 3 files changed, 46 insertions(+), 19 deletions(-) diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml index 7d27b61..b5e696c 100644 --- a/.github/workflows/contract-gate.yml +++ b/.github/workflows/contract-gate.yml @@ -48,7 +48,8 @@ jobs: # 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, @@ -56,22 +57,25 @@ jobs: # 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 @@ jobs: # Local tag on the verified commit, so the Makefile reports the # release version (0.8.0) rather than 0.8.0-. 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; } diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d2c5d68..517d2f0 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,19 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== 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) * The canonical Rust front-end (`typed-wasm-codegen`, ADR-0006) now parses diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh index 043c403..2d8aea3 100755 --- a/tools/check-kernel-proofs.sh +++ b/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)"