fix(ci): actually run the verdict round-trip against the reference checker - #34
Conversation
…ecker The Trope conformance 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 never built any checker — so that binary could not exist in CI, and the skip was unconditional. The schema drift guard was skipping for the same reason. The round-trip is the one seam that joins the three repos: Haec emits Trope IR, the checker returns a verdict. Leaving it unexercised meant the repository's core claim was asserted, never measured. Why the checker "could not build" --------------------------------- 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 declared that requirement, so reading local state (0.7.0 installed) suggests the reference checker is unbuildable, and invites replacing it with the Rust fast-core. That would have been the wrong trade: ADR 0002/0003 chose Idris2 precisely so the thing that runs is the thing that is proved. The fix is a toolchain pin, not a new reference implementation. 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) haec round-trip 3/3 correct, witness e_collapse/fate.quality exact The Rust fast-core agrees with it on all of the above (cross-validation). 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, and runs the gate with TROPECHECK_REQUIRED=1. * check-examples.sh honours TROPECHECK_BIN — the same variable trope-checker's own conformance runner uses — and treats a missing binary as fatal when TROPECHECK_REQUIRED=1, instead of silently skipping. * The round-trip now also asserts the WITNESS. EXAMPLES.json has always declared witness ["e_collapse","fate.quality"] and 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: with TROPECHECK_BIN=/nonexistent and TROPECHECK_REQUIRED=1 the gate fails; with a deliberately corrupted expected witness it fails, naming both got and expected. A gate that cannot fail is not a gate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
Code Review ✅ Approved 1 resolved / 1 findingsUpdates CI and the check script to properly build the Idris 2 0.8.0 reference checker and enforce the verdict round-trip and witness assertions. Consider making the witness assertion shape robust against variable-length coordinates.
✅ 1 resolved✅ Edge Case: Witness check hardcodes a 2-part witness=/coord= shape
OptionsAuto-apply is off → Gitar will not commit updates to this branch. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
1 participant
Phase 0 of
dev-notes/trope-family-completeness-plan-2026-07-28.md, and thehighest-leverage item in it.
The gate was green while its central assertion never ran
tests/check-examples.shskipped the verdict round-trip whenever the siblingtropecheckbinary was absent — andtrope-check.ymlchecked out only haec andbuilt 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/idris2requiresIdris 2 0.8.0 — under 0.7.0,
Trope/Fidelity.idr:72fails to parse at thelambda-impossible clause
No (\Refl impossible). Nothing in either repo declaresthat 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-packimage (Idris 2 0.8.0)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.ymlruns in the pinned 0.8.0 container; checks outtrope-checkeras a sibling of
haec/so$ROOT/../trope-checkerresolves (which alsore-activates the schema drift guard); installs
jq(the image ships none); buildsthe reference checker; runs the gate with
TROPECHECK_REQUIRED=1.check-examples.shhonoursTROPECHECK_BIN— the same variable trope-checker'sown conformance runner already uses — and treats a missing binary as fatal under
TROPECHECK_REQUIRED=1rather than skipping.EXAMPLES.jsonhas always declared["e_collapse","fate.quality"]; nothing ever checked it.p-insufficient— a verdict, not an error — so theloop no longer aborts on it.
Canary-tested — a gate that cannot fail is not a gate
TROPECHECK_BIN=/nonexistent+REQUIRED=1e_WRONGFollow-ups (not in this PR)
trope-checkershould declare Idris 2 0.8.0 in.tool-versions/README so the nextreader does not repeat my mistake, and run its own conformance suite in CI.
trope-checker/build/guix.scmstill reads(name "squisher-corpus").🤖 Generated with Claude Code