fix(ci): actually run the verdict round-trip against the reference checker (#34)

Phase 0 of `dev-notes/trope-family-completeness-plan-2026-07-28.md`, and
the
highest-leverage item in it.

## The gate was green while its central assertion never ran

`tests/check-examples.sh` skipped the verdict round-trip whenever the
sibling
`tropecheck` binary was absent — and `trope-check.yml` checked out only
haec and
built no checker, so that binary **could not exist in CI**. The skip was
therefore
unconditional. The schema drift guard was skipping for the same reason.

The round-trip is *the* seam joining the three repos: Haec emits Trope
IR, the
checker returns a verdict. Unexercised, the repository's core claim was
asserted
but never measured.

## A finding I have to correct

My own gap analysis reported that the Idris2 reference checker "cannot
build". **That
was wrong**, and the correction matters.

It builds fine under the right compiler. `verification/proofs/idris2`
requires
Idris 2 **0.8.0** — under 0.7.0, `Trope/Fidelity.idr:72` fails to parse
at the
lambda-impossible clause `No (\Refl impossible)`. **Nothing in either
repo declares
that requirement**, so reading local state (0.7.0 installed) suggests
the reference is
unbuildable and invites swapping in the Rust fast-core as the new
reference.

That would have been the wrong trade. ADR 0002/0003 chose Idris2
precisely so that
*"the thing that runs is the thing that is proved"* — the executable
reuses the proved
verified core. Ratifying the conformance-validated-only Rust checker
would have traded
away the family's central epistemic claim **to fix a toolchain pin.**

## Measured under the digest-pinned `idris2-pack` image (Idris 2 0.8.0)

```
verified core ......... typechecks 8/8 modules, exit 0
tropecheck ............ builds, exit 0
conformance suite ..... all pass (13 verdict cases + 9 schema-invalid rejections)
haec round-trip ....... 3/3 correct, witness e_collapse/fate.quality exact
```

The Rust fast-core agrees with the Idris2 reference on all of the above
— the
cross-validation the calculus §9.3 asks for, now actually performed.

## Changes

- **`trope-check.yml`** runs in the pinned 0.8.0 container; checks out
`trope-checker`
as a **sibling** of `haec/` so `$ROOT/../trope-checker` resolves (which
also
re-activates the schema drift guard); installs `jq` (the image ships
none); builds
  the reference checker; runs the gate with `TROPECHECK_REQUIRED=1`.
- **`check-examples.sh`** honours `TROPECHECK_BIN` — the same variable
trope-checker's
own conformance runner already uses — and treats a missing binary as
**fatal** under
  `TROPECHECK_REQUIRED=1` rather than skipping.
- **The round-trip now asserts the WITNESS.** `EXAMPLES.json` has always
declared
  `["e_collapse","fate.quality"]`; nothing ever checked it.
- The checker exits non-zero on `p-insufficient` — a *verdict*, not an
error — so the
  loop no longer aborts on it.

## Canary-tested — a gate that cannot fail is not a gate

| Falsifier | Result |
|---|---|
| `TROPECHECK_BIN=/nonexistent` + `REQUIRED=1` | **fails**, naming the
missing path |
| expected witness corrupted to `e_WRONG` | **fails**, printing got vs
expected |

## Follow-ups (not in this PR)

- `trope-checker` should declare Idris 2 0.8.0 in
`.tool-versions`/README so the next
reader does not repeat my mistake, and run its own conformance suite in
CI.
- `trope-checker/build/guix.scm` still reads `(name "squisher-corpus")`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/trope-check.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

tests/check-examples.sh

@@ -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