fix(corpus): run conformance programs, and correct a second false assertion - #97
Merged
Merged
Conversation
…ertion The trefoil assertion corrected in #95 was not an isolated slip. Auditing whether the conformance corpus actually RUNS — the gate only ever checked that it PARSED — turned up a second mathematically false claim of exactly the same kind, plus one genuine unimplemented feature. ## The second false assertion conformance/valid/v16_close_mirror_reverse.tangle asserted assert reverse(braid[s1, s2]) == braid[s2, s1] `reverse` reverses the word AND negates every exponent — it yields the INVERSE braid, so reverse(s1 s2) = s2^-1 s1^-1. Disproved by invariant: writhe(reverse(braid[s1,s2])) = -2 while writhe(braid[s2,s1]) = +2, and writhe is invariant under the braid relations. Corrected. Two independent authors made the identical mistake, which is a documentation failure, not carelessness: FORMAL-SEMANTICS.md described the operation as "reverse word", which reads as order-only. Now stated as an identity — reverse(w) = w^-1, i.e. reverse(g1 … gn) = gn^-1 … g1^-1 — with the contrast against `mirror` (which negates IN PLACE) spelled out, and with the writhe argument recorded so the next reader can check it themselves. ## The systemic fix `scripts/check-corpus.sh` now EVALUATES conformance/valid, not just parses it. Parsing was never enough: a program can parse perfectly and assert something false. Both bad assertions survived precisely because nothing ran them. Verified by reintroducing the exact false assertion — the gate catches it (exit 1, "parses but does not evaluate") — and by restoring it (exit 0). ## The genuine gap conformance/valid/v09_twist.tangle uses `(~a)` to twist a named strand inside a weave. spec/grammar.ebnf says "In weave context: (~a) twists named strand a", but infer_expr rejects any strand name used as an expression, so the construct is specified and unimplemented. Recorded in the new CONFORMANCE_KNOWN_UNRUNNABLE manifest list rather than papered over, and raised as its own issue. ## Regression tests Four pinning `reverse`'s semantics, chosen so they cannot pass vacuously: that it is NOT order-reversal, that applying it twice is the identity (only true if it really inverts), that it negates writhe, and the contrast with `mirror`. Suites 112 -> 116; all green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedUpdates the corpus check script to evaluate conformance programs rather than just parsing them, and corrects a false reverse-braid assertion alongside documentation and regression tests. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
|
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The false assertion corrected in #95 was not an isolated slip. Auditing whether the conformance corpus actually runs — the gate only ever checked that it parsed — turned up a second mathematically false claim of exactly the same kind, plus one genuine unimplemented feature.
The second false assertion
conformance/valid/v16_close_mirror_reverse.tangle:reversereverses the word and negates every exponent — it yields the inverse braid, soreverse(s1 s2) = s2⁻¹ s1⁻¹.Disproved by invariant:
writhe(reverse(braid[s1,s2])) = -2whilewrithe(braid[s2,s1]) = +2, and writhe is invariant under the braid relations, so they cannot be the same element.Two authors, same mistake → a documentation failure
examples/trefoil.tangleand this file made the identical wrong assumption. That is not carelessness.FORMAL-SEMANTICS.mddescribed the operation as:which reads as order-only. Now stated as an identity:
with the contrast against
mirror(which negates in place) spelled out, and the writhe argument recorded so the next reader can check it rather than trust it.The systemic fix
scripts/check-corpus.shnow evaluatesconformance/valid, not just parses it. Parsing was never enough — a program can parse perfectly and assert something false. Both bad assertions survived precisely because nothing ran them.Verified in both directions: reintroducing the exact false assertion makes the gate fail (
exit 1, "parses but does not evaluate"); restoring it returnsexit 0.The genuine gap
v09_twist.tangleuses(~a)to twist a named strand inside a weave.spec/grammar.ebnfsays "In weave context: (~a) twists named strand a", butinfer_exprrejects any strand name used as an expression — specified and unimplemented. Recorded in the newCONFORMANCE_KNOWN_UNRUNNABLElist rather than papered over, and raised as #96.Worth noting why it was invisible: until #93 a weave block could not be bound to anything, so its body was never evaluated. The construct has literally never run.
Regression tests
Four pinning
reverse, chosen so they cannot pass vacuously:reverse(reverse(w)) = wmirrornegates in placeSuites 112 → 116, all green; TG-3 still 1008/0.
🤖 Generated with Claude Code