diff --git a/.github/workflows/trope-check.yml b/.github/workflows/trope-check.yml index 360f1ec..ca56393 100644 --- a/.github/workflows/trope-check.yml +++ b/.github/workflows/trope-check.yml @@ -1,7 +1,12 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# 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 diff --git a/tests/check-examples.sh b/tests/check-examples.sh index f840ff2..d090700 100644 --- a/tests/check-examples.sh +++ b/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