refactor: Haec example checker to bash+jq (no Python)

.github/workflows/trope-check.yml

@@ -1,31 +1,19 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# Haec: validate that every example lowers to a well-formed Trope IR document.
+# Haec: every example lowers to a well-formed Trope IR document (bash + jq, no Python).
 name: trope-check
-
 on:
   push:
-    paths:
-      - 'design/**'
-      - 'examples/**'
-      - 'tests/**'
-      - '.github/workflows/trope-check.yml'
+    paths: ['design/**', 'examples/**', 'tests/**', '.github/workflows/trope-check.yml']
   pull_request:
   workflow_dispatch:
-
 permissions:
   contents: read
-
 jobs:
   examples-lower-to-valid-ir:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - uses: actions/setup-python@v5
-        with:
-          python-version: '3.12'
-      - name: Install jsonschema
-        run: python -m pip install --upgrade jsonschema
       - name: Examples lower to valid Trope IR
-        run: python3 tests/check-examples.py
+        run: bash tests/check-examples.sh

AUDIT.adoc

@@ -9,7 +9,7 @@ The release-audit gate. Ground-truth by running the tools.
 [cols="1,2,1",options="header"]
 |===
 | Check | Command | State 2026-06-22
-| Examples lower to valid IR | `just check` (`python3 tests/check-examples.py`) | PASS (3/3)
+| Examples lower to valid IR | `just check` (`bash tests/check-examples.sh`) | PASS (3/3)
 | Round-trip through the checker | `just haec-roundtrip` (needs sibling trope-checker) | PASS (verdicts + witness match)
 | Design artefacts present | grammar.ebnf, elaboration.adoc | PASS
 |===

README.adoc

@@ -129,7 +129,7 @@ compiler yet — `compiler/` and `lsp/` are named future work (`STATUS.adoc`).
 ----
 just check     # validate examples/*.ir.json against the vendored IR schema
 # full round-trip (verdicts) needs a checkout of the sibling trope-checker:
-python3 ../trope-checker/src/checker/tropecheck.py examples/survey-collapse.ir.json
+../trope-checker/src/idris2/build/exec/tropecheck examples/survey-collapse.ir.json
 ----
 
 == Licence

build/just/trope.just

@@ -1,15 +1,12 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# Haec (trope-particularity front-end) recipes. Imported by the root Justfile via
+# Haec (trope front-end) recipes. No Python. Imported by the root Justfile via
 #   import? "build/just/trope.just"
 
-# Validate that every example lowers to a well-formed Trope IR document.
+# Every example lowers to a well-formed Trope IR document (+ round-trip if the
+# sibling trope-checker is checked out/built).
 check: haec-examples
 
 haec-examples:
-    python3 tests/check-examples.py
-
-# Full round-trip (verdicts) needs a checkout of the sibling trope-checker.
-haec-roundtrip:
-    @for f in examples/*.ir.json; do echo "== $f =="; python3 ../trope-checker/src/checker/tropecheck.py "$f" || true; done
+    bash tests/check-examples.sh

design/trope-ir.schema.json

@@ -2,7 +2,7 @@
   "$schema": "https://json-schema.org/draft/2020-12/schema",
   "$id": "https://github.com/hyperpolymath/trope-checker/schemas/trope-ir.schema.json",
   "title": "Trope IR",
-  "$comment": "SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>. SPDX-License-Identifier: MPL-2.0. The language-neutral interchange of the trope-particularity calculus (spec/calculus.adoc). This is the canonical PREVENT profile (DEPLOY_VARIANT=prevent, R-2026-06-22): the three deceptive grade values (fate=Falsified, bond=Misbound, merge=Conflated) and the untagged merge are MALFORMED here and are rejected at validation with the offending coordinate named. The grade shape is the dependent record Sigma(fate). Bond(fate.bearer) x Merge; the if/then/else on bond makes bearer-incoherent grades unrepresentable (HC-4). The semantics (Idris2 src/) carries the COMPLETE lattices including the deceptive bottoms; the detect-profile schema (trope-ir.detect.schema.json) permits them and defers the check to the verdict.",
+  "$comment": "SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>. SPDX-License-Identifier: MPL-2.0. The language-neutral interchange of the trope-particularity calculus (spec/calculus.adoc). This is the canonical PREVENT profile (DEPLOY_VARIANT=prevent, R-2026-06-22): the three deceptive grade values (fate=Falsified, bond=Misbound, merge=Conflated) and the untagged merge are MALFORMED here and are rejected at validation with the offending coordinate named. The grade shape is the dependent record Sigma(fate). Bond(fate.bearer) x Merge; the if/then/else on bond makes bearer-incoherent grades unrepresentable (HC-4). The semantics (Idris2 src/) carries the COMPLETE lattices including the deceptive bottoms; the detect profile (calculus §6.1) permits them and defers the check to the verdict; it is documented in the calculus, not shipped as a separate schema here.",
   "description": "A labelled DAG: nodes are property-instances (field-presence + type tag), edges are effect applications carrying a loss-shape grade, and a use-model node carries the floor. The checker is a pure function from this document to a verdict.",
   "type": "object",
   "required": ["version", "profile", "nodes", "edges", "use_model"],
@@ -14,7 +14,7 @@
     "profile": {
       "type": "string",
       "const": "prevent",
-      "$comment": "This schema is the prevent profile. A detect-profile document MUST use trope-ir.detect.schema.json and declare profile=detect."
+      "$comment": "This schema is the prevent profile. The detect profile (calculus §6.1) is documented there, not shipped as a separate schema; this repository serves prevent."
     },
     "nodes": {
       "type": "array",

tests/check-examples.sh

@@ -0,0 +1,57 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Every Haec example lowers to a well-formed Trope IR document. Pure bash + jq,
+# no Python. Self-contained: structural checks against the vendored IR contract.
+# The full round-trip (verdicts) runs when the sibling trope-checker is present.
+set -uo pipefail
+
+ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+EX="$ROOT/examples"
+SIB="$ROOT/../trope-checker"
+G="\033[32m"; R="\033[31m"; Y="\033[33m"; O="\033[0m"
+fail=0
+command -v jq >/dev/null || { echo "jq is required"; exit 2; }
+
+# 1. structural: each *.ir.json is well-formed and has the required IR shape.
+for f in "$EX"/*.ir.json; do
+  if ! jq -e '.version and .profile and .nodes and .edges and .use_model' "$f" >/dev/null 2>&1; then
+    echo -e "${R}FAIL${O} $(basename "$f"): not a well-formed Trope IR document"; fail=1
+  fi
+done
+
+# 2. every example in the manifest pairs a program with its IR.
+while read -r e; do
+  prog=$(jq -r '.program' <<<"$e"); ir=$(jq -r '.ir' <<<"$e")
+  [ -f "$EX/$prog" ] || { echo -e "${R}FAIL${O} missing program $prog"; fail=1; }
+  [ -f "$EX/$ir" ]   || { echo -e "${R}FAIL${O} missing IR $ir"; fail=1; }
+  [ "$fail" = 0 ] && echo -e "${G}ok${O}   $prog → $ir (well-formed IR, expects $(jq -r '.expect' <<<"$e"))"
+done < <(jq -c '.examples[]' "$EX/EXAMPLES.json")
+
+# 3. drift guard: the vendored IR schema must match the canonical one if present.
+if [ -f "$SIB/schemas/trope-ir.schema.json" ]; then
+  if diff -q "$ROOT/design/trope-ir.schema.json" "$SIB/schemas/trope-ir.schema.json" >/dev/null; then
+    echo -e "${G}ok${O}   vendored design/trope-ir.schema.json matches the canonical checker schema"
+  else
+    echo -e "${R}FAIL${O} vendored IR schema has drifted from trope-checker/schemas/trope-ir.schema.json"; fail=1
+  fi
+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
+  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
+  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)"
+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
+exit "$fail"