diff --git a/.github/workflows/trope-check.yml b/.github/workflows/trope-check.yml index 7ea78f5..3c9a1ae 100644 --- a/.github/workflows/trope-check.yml +++ b/.github/workflows/trope-check.yml @@ -1,31 +1,19 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# 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 diff --git a/AUDIT.adoc b/AUDIT.adoc index 127708f..b2bfc54 100644 --- a/AUDIT.adoc +++ b/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 |=== diff --git a/README.adoc b/README.adoc index 546a3c8..9b22ac2 100644 --- a/README.adoc +++ b/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 diff --git a/build/just/trope.just b/build/just/trope.just index ba454e4..37c9eb0 100644 --- a/build/just/trope.just +++ b/build/just/trope.just @@ -1,15 +1,12 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# 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 diff --git a/design/trope-ir.schema.json b/design/trope-ir.schema.json index 9771d60..854da88 100644 --- a/design/trope-ir.schema.json +++ b/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) . 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) . 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", diff --git a/tests/check-examples.py b/tests/check-examples.py deleted file mode 100644 index b1059f7..0000000 --- a/tests/check-examples.py +++ /dev/null @@ -1,52 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) -# SPDX-License-Identifier: MPL-2.0 -"""Validate that every Haec example lowers to a well-formed Trope IR document. - -Self-contained: validates examples/*.ir.json against the vendored IR contract -(design/trope-ir.schema.json — canonical in trope-checker). The full round-trip -(verdicts via the checker) is a cross-repo integration; run it with a checkout of -the sibling trope-checker (see README). This keeps `just check` green standalone. -""" -from __future__ import annotations -import json, pathlib, sys - -try: - from jsonschema import Draft202012Validator -except ImportError: - sys.exit("error: python 'jsonschema' package is required") - -ROOT = pathlib.Path(__file__).resolve().parent.parent -SCHEMA = ROOT / "design" / "trope-ir.schema.json" -EX = ROOT / "examples" -GREEN, RED, OFF = "\033[32m", "\033[31m", "\033[0m" - - -def main() -> int: - v = Draft202012Validator(json.loads(SCHEMA.read_text(encoding="utf-8"))) - manifest = json.loads((EX / "EXAMPLES.json").read_text(encoding="utf-8")) - by_ir = {e["ir"]: e for e in manifest["examples"]} - failures = 0 - for path in sorted(EX.glob("*.ir.json")): - doc = json.loads(path.read_text(encoding="utf-8")) - errs = sorted(v.iter_errors(doc), key=lambda e: list(e.absolute_path)) - if errs: - failures += 1 - print(f"{RED}FAIL{OFF} {path.name}: {errs[0].message} at " - f"{'/'.join(str(p) for p in errs[0].absolute_path)}") - elif path.name not in by_ir: - failures += 1 - print(f"{RED}FAIL{OFF} {path.name}: not listed in EXAMPLES.json") - else: - prog = by_ir[path.name]["program"] - if not (EX / prog).exists(): - failures += 1 - print(f"{RED}FAIL{OFF} {path.name}: program {prog} missing") - else: - print(f"{GREEN}ok{OFF} {prog} → {path.name} (valid IR, expects {by_ir[path.name]['expect']})") - print(f"\n{(GREEN+'examples: all lower to valid Trope IR') if not failures else (RED+f'examples: {failures} failure(s)')}{OFF}") - return 1 if failures else 0 - - -if __name__ == "__main__": - raise SystemExit(main()) diff --git a/tests/check-examples.sh b/tests/check-examples.sh new file mode 100644 index 0000000..f840ff2 --- /dev/null +++ b/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) +# +# 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"