Repository navigation
Rule set termination is checked by the build (#746 tier 2) - #1057
Merged
Merged
Conversation
#746 tier 2 asks for termination "checked by tooling rather than asserted by authors". The tooling existed -- work/rulecheck -- and lived in a workspace, so it answered for whoever ran it and for no one else. A rule set that reaches no fixed point is a hang rather than a wrong answer, and a hang is what a test suite reports worst. Two facts, because they have different answers. Iterated alone, every set in the registry settles except Power and NumericNeat, both of which want the normalisation to fold arithmetic their own right-hand sides leave behind. With the normalisation between passes -- how Simplify actually runs them -- every set settles except Common. Both lists are asserted in both directions, so a set that starts cycling fails and a set that stops cycling fails too: a list that outlives what it describes is how the workspace reports went stale. The sets are named rather than counted, because a count that goes from two to two says nothing when one set was fixed and another started. Common's failure is a genuine three-cycle on -x * 1/2 -- Mulf(-1/2, x), Mulf(-1, Divf(x, 2)), Divf(Mulf(-1, x), 2) -- three trees printing as two strings, which is why it is written down as shapes. Two rules disagree about whether c * x or (c * x) / d is the destination. Simplify bounds its own iteration and does not hang, so nothing a caller sees today is broken by it; it is filed as #1056 and recorded here rather than fixed, because choosing an orientation for a set that runs on nearly every simplification is a decision and not a patch. The corpus goes three levels deep, and the third level is load-bearing: the shapes that cycle are a unary applied to something already compound, and without it the second assertion fires on an empty list. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd
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
2 participants
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.
#746 tier 2 asks for termination "checked by tooling rather than asserted by authors". The tooling existed and lived in a workspace harness, so it answered for whoever ran it and for no one else. A rule set that reaches no fixed point is a hang rather than a wrong answer, and a hang is what a test suite reports worst — it aborts the run instead of failing a test.
What it checks
Two questions, because they have different answers.
Power,NumericNeatSimplifyruns themCommonPowersplits a power of a product —(2 * x) ^ 2to2 ^ 2 * x ^ 2— and something has to fold2 ^ 2before the result stops being a power of a product.NumericNeatrewrites--xthrough a product of ones that only collapses when the normalisation multiplies them out. Both are the same shape: a right-hand side that is a fixed point only after arithmetic the set itself does not do.Both lists are asserted in both directions
A set that starts cycling fails, and a set that stops cycling fails too. A list that outlives what it describes is exactly how the workspace reports went stale, and the sets are named rather than counted — a count going from two to two says nothing when one set was fixed and another started.
What it found
Commonhas a genuine three-cycle on-x * 1/2, filed as #1056:Three trees printing as two strings, which is why the test records shapes and not printed forms. Two rules disagree about whether
c * xor(c * x) / dis the destination.Simplifybounds its own iteration and does not hang —"-x * 1/2".Simplify()is-1/2 * x— so nothing a caller sees today is broken by it. It is recorded here rather than fixed: choosing an orientation for a set that runs on nearly every simplification is a decision, not a patch.The corpus
Leaves, then unary and binary shapes over them, then a third level that is load-bearing — the shapes that cycle are a unary applied to something already compound (
(2 * x) ^ 2,--x), and without it the second assertion fires on an empty list. That is what it did the first time it ran.Cost
2 s for both tests. The corpus is parsed once into a static; building it per rule set parsed the same few hundred strings sixty times over, which was 83 s of the run and none of its coverage.
Full suite green:
Failed: 0, Passed: 8576, Skipped: 14, Total: 8590.🤖 Generated with Claude Code
https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd