Merge branch 'main' into fix/toolchain-version-asserts

Author: hyperpolymath

.github/workflows/ci.yml

@@ -27,17 +27,24 @@ jobs:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
-      # The pinned idris2-pack image ships no xz binary, so setup-zig's
-      # .tar.xz download fails with "tar (child): xz: Cannot exec".
-      - name: Install xz (needed to unpack the Zig tarball)
+      # The pinned idris2-pack image is minimal. Two things are missing:
+      #   xz — setup-zig's .tar.xz download dies with "tar: xz: Cannot exec"
+      #   jq — tests/check-examples.sh exits 2 with "jq is required", so the
+      #        Trope IR conformance test never actually ran in CI
+      - name: Install container prerequisites (xz, jq)
         shell: bash
         run: |
           set -euo pipefail
-          if ! command -v xz >/dev/null 2>&1; then
+          missing=()
+          command -v xz >/dev/null 2>&1 || missing+=(xz-utils)
+          command -v jq >/dev/null 2>&1 || missing+=(jq)
+          if [ "${#missing[@]}" -gt 0 ]; then
+            echo "installing: ${missing[*]}"
             apt-get update -qq
-            apt-get install -y -qq --no-install-recommends xz-utils
+            apt-get install -y -qq --no-install-recommends "${missing[@]}"
           fi
           xz --version | head -1
+          jq --version
 
       - name: Set up Zig
         uses: goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406 # v2.2.1

.github/workflows/npm-bun-blocker.yml

@@ -0,0 +1,71 @@
+# SPDX-License-Identifier: MPL-2.0
+# Runtime and package-manager policy check.
+#
+# Authority: hyperpolymath/standards LANGUAGE-POLICY.adoc §1.
+# Ordering:  Bun (1st) > Deno (2nd) > pnpm (3rd) > npm (last resort).
+#
+# REPLACES npm-bun-blocker.yml, which failed any build carrying `bun.lockb` with
+# the message "npm/bun artifacts detected. Use Deno instead." That gate blocked
+# what is now the FIRST-choice runtime and mandated the second. It was present in
+# 55 repositories.
+#
+# What this fails on, deliberately:
+#   MIXED TOOLCHAINS -- two different package managers' lockfiles in one repo.
+#   That is real, actionable drift: two dependency graphs that can disagree.
+# What it does NOT fail on:
+#   Using bun, deno, pnpm or npm. npm is LAST but PERMITTED; the check reports
+#   the tier in use so drift is visible without blocking legitimate work.
+name: Runtime Policy
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  runtime-policy:
+    name: Runtime Policy
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Report runtime tier and reject mixed toolchains
+        run: |
+          set -euo pipefail
+
+          bun=0; deno=0; pnpm=0; npm=0
+          [ -f bun.lockb ] || [ -f bun.lock ]                 && bun=1  || true
+          [ -f deno.lock ] || [ -f deno.json ] || [ -f deno.jsonc ] && deno=1 || true
+          [ -f pnpm-lock.yaml ]                               && pnpm=1 || true
+          [ -f package-lock.json ]                            && npm=1  || true
+
+          total=$((bun + deno + pnpm + npm))
+
+          if [ "$total" -eq 0 ]; then
+            echo "::notice::No JS/TS package manager in use — nothing to check."
+            exit 0
+          fi
+
+          # Report the tier actually in use (LANGUAGE-POLICY.adoc §1).
+          [ "$bun"  -eq 1 ] && echo "Bun   — tier 1 (preferred)"
+          [ "$deno" -eq 1 ] && echo "Deno  — tier 2 (accepted; existing projects are grandfathered)"
+          [ "$pnpm" -eq 1 ] && echo "pnpm  — tier 3"
+          [ "$npm"  -eq 1 ] && echo "::warning::npm lockfile present. npm is tier 4, the last resort — permitted, never preferred. See LANGUAGE-POLICY.adoc §1."
+
+          if [ "$total" -gt 1 ]; then
+            echo "::error::Mixed toolchains: $total package managers have lockfiles in this repository."
+            echo "Two dependency graphs that can disagree is real drift. Pick one — preferring the"
+            echo "highest tier present — and delete the others' lockfiles."
+            exit 1
+          fi
+
+          echo "✅ Single package manager in use."

.github/workflows/runtime-policy.yml

@@ -1,7 +1,12 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# Haec: every example lowers to a well-formed Trope IR document (bash + jq, no Python).
+# Haec: every example lowers to a well-formed Trope IR document AND round-trips
+# through the reference tropechecker to its expected verdict and witness.
+#
+# The round-trip is the one seam joining the three repos — Haec emits IR, the
+# checker returns a verdict — so it is built and asserted here rather than
+# skipped. TROPECHECK_REQUIRED=1 makes a missing binary a hard failure.
 name: "🔴 Gate: Trope conformance"
 on:
   push:
@@ -16,7 +21,56 @@ concurrency:
 jobs:
   examples-lower-to-valid-ir:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
+    # The reference checker is an Idris2 program whose verified core requires
+    # Idris 2 *0.8.0*: under 0.7.0, Trope/Fidelity.idr fails to parse at the
+    # lambda-impossible clause `No (\Refl impossible)`. Pinned by image digest.
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:de9781906050dc44704ec6de0108c86f899ef17b2642932b79e00245d613b8ad
     steps:
-      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
-      - name: Examples lower to valid Trope IR
+      - name: Checkout Haec
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          path: haec
+
+      # Checked out as a SIBLING of haec/ so tests/check-examples.sh finds it at
+      # $ROOT/../trope-checker — which also activates the schema drift guard.
+      - name: Checkout trope-checker (reference checker + canonical IR schema)
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          repository: hyperpolymath/trope-checker
+          ref: 69221ad6bec0c9286cb5c917edfad281e7e0089e # main @ 2026-07-28
+          path: trope-checker
+
+      # The pinned idris2-pack image is minimal and ships no jq, which both the
+      # test script and the conformance runner require.
+      - name: Install container prerequisites (jq)
+        shell: bash
+        run: |
+          set -euo pipefail
+          if ! command -v jq >/dev/null 2>&1; then
+            apt-get update -qq
+            apt-get install -y -qq --no-install-recommends jq
+          fi
+          jq --version
+          idris2 --version
+
+      # ADR 0002/0003: the Idris2 executable is the reference checker and reuses
+      # the *proved* verified core, so the thing that runs is the thing that is
+      # proved. Installing that core is therefore part of building the oracle.
+      - name: Build the Idris2 reference checker
+        shell: bash
+        working-directory: trope-checker
+        run: |
+          set -euo pipefail
+          idris2 --install verification/proofs/idris2/trope.ipkg
+          ( cd src/idris2 && idris2 --build tropecheck.ipkg )
+          test -x src/idris2/build/exec/tropecheck
+          echo "reference checker built"
+
+      - name: Examples lower to valid Trope IR, and round-trip to their verdicts
+        shell: bash
+        working-directory: haec
+        env:
+          TROPECHECK_REQUIRED: '1'
         run: bash tests/check-examples.sh

.github/workflows/trope-check.yml

@@ -40,17 +40,38 @@ else
   echo -e "${Y}note${O} sibling trope-checker not checked out; skipping schema-drift guard"
 fi
 
-# 4. full round-trip: verdicts via the sibling Idris2 checker, if built.
-BIN="$SIB/src/idris2/build/exec/tropecheck"
-if [ -x "$BIN" ]; then
+# 4. full round-trip: verdicts via the reference checker.
+#
+# TROPECHECK_BIN names the binary (same variable trope-checker's own conformance
+# runner honours); it defaults to the sibling Idris2 reference build. Set
+# TROPECHECK_REQUIRED=1 — as CI does — to make a missing binary a hard failure
+# rather than a skip: a round-trip that silently does not run is a fake gate.
+BIN="${TROPECHECK_BIN:-$SIB/src/idris2/build/exec/tropecheck}"
+if [ ! -x "$BIN" ] && [ "${TROPECHECK_REQUIRED:-0}" = "1" ]; then
+  echo -e "${R}FAIL${O} TROPECHECK_REQUIRED=1 but no checker binary at $BIN"
+  echo "      build it with: idris2 --install verification/proofs/idris2/trope.ipkg"
+  echo "                     idris2 --build   src/idris2/tropecheck.ipkg   (Idris2 0.8.0)"
+  fail=1
+elif [ -x "$BIN" ]; then
   while read -r e; do
     ir=$(jq -r '.ir' <<<"$e"); exp=$(jq -r '.expect' <<<"$e")
-    got=$("$BIN" "$EX/$ir" | awk '{print $1}')
-    if [ "$got" = "$exp" ]; then echo -e "${G}ok${O}   round-trip $ir → $got"
-    else echo -e "${R}FAIL${O} round-trip $ir: got $got, expected $exp"; fail=1; fi
+    # the checker exits non-zero on p-insufficient — that is a verdict, not an
+    # error, so do not let it abort the loop.
+    out=$("$BIN" "$EX/$ir" || true)
+    got=$(awk '{print $1}' <<<"$out")
+    wexp=$(jq -r '.witness // [] | join("/")' <<<"$e")
+    ok=1
+    [ "$got" = "$exp" ] || ok=0
+    if [ -n "$wexp" ]; then
+      gw=$(grep -o 'witness=[^[:space:]]*' <<<"$out" | cut -d= -f2)
+      gc=$(grep -o 'coord=[^[:space:]]*'   <<<"$out" | cut -d= -f2)
+      [ "$gw/$gc" = "$wexp" ] || ok=0
+    fi
+    if [ "$ok" = 1 ]; then echo -e "${G}ok${O}   round-trip $ir → $got${wexp:+ (witness $wexp)}"
+    else echo -e "${R}FAIL${O} round-trip $ir: got '$out', expected $exp${wexp:+ witness $wexp}"; fail=1; fi
   done < <(jq -c '.examples[]' "$EX/EXAMPLES.json")
 else
-  echo -e "${Y}note${O} sibling tropecheck binary not built; skipping verdict round-trip (run 'just trope-build' in ../trope-checker)"
+  echo -e "${Y}note${O} no checker binary; skipping verdict round-trip (set TROPECHECK_BIN, or TROPECHECK_REQUIRED=1 to make this fatal)"
 fi
 
 if [ "$fail" = 0 ]; then echo -e "\n${G}examples: all lower to valid Trope IR${O}"; else echo -e "\n${R}examples: failures${O}"; fi