Name a conditional set's binder rather than guessing it from a hash (#891) - #904
Merged
Conversation
…891) A conditional set renames its bound variable in DirectChildren so that the x inside { x : P(x) } is not read as an x that may be free outside it. The replacement name was four lowercase letters derived from the predicate's hash code, and it was produced through MathS.Var -- which parses. Four lowercase letters can spell `true`, the parser reads that as a boolean, and the conversion to Variable throws CannotParseInstanceException. That is the intermittent CI failure of #891: one name in 26^4 does it, and .NET randomises string hash codes per process, so the same expression picks a different name on every run and the failure would not reproduce. The same four letters can also spell a variable the predicate already uses, in which case the rename captures it and the set means something else, with no exception to say so. CreateTemp answers both. It reads the predicate's variables rather than its hash and returns %1 upward, skipping the indices already taken: fresh by construction, deterministic, and with no reading as anything but a variable -- `%` is not a token the parser accepts, which is why no parsed input can collide with it. The class already trusted that name for the same purpose two methods below, where GetHashCode alpha-normalises with CreateVariableUnchecked("%"). Printed output is unchanged, since Stringize reads the node's fields rather than its DirectChildren: { x : x > 0 } still prints with its own binder, and Solve answers carrying a conditional set are unaffected. Recorded in BREAKING-CHANGES.md anyway, because DirectChildren is public. CreateRandom had this one caller and is removed. The new tests fail 5 of 8 against master and pass 8 of 8 here, so they pin the fix rather than describe it. Suite 6341 passed; casbench 117/119 with 0 wrong; rootcheck 596/596; simpsweep 10463/10463; propcheck 1340 checks 0 failures; crashcheck 1652 cases 0 crashes and 0 unexpected throws; boundcheck unchanged at master's 4 disagreements. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
One conflict, in BREAKING-CHANGES.md, where #901 and #903 landed their glance rows and their sections around the place this branch adds its own. All three are additions rather than disagreements: master's rows and sections keep their positions and this branch's follow. Verified after resolving rather than assumed: abs(-sqrt(6)) is sqrt(6), ln(e^x) is left as written, and a solve answer carrying a conditional set still prints its own binder. Suite 6359 passed, F# wrapper 130 passed, both 0 failed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
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.
Closes #891 — the intermittent CI failure that arrived on a documentation-only PR and passed on a
re-run of the same commit. It has a cause, and it is not a race.
What it was
A conditional set renames its bound variable in
DirectChildren, so thexinside{ x : P(x) }isnot read as an
xthat may be free outside it. The name came fromVariable.CreateRandom:Two things collide there.
MathS.Varparses. It ispublic static Variable Var(string name) => name;— the implicitconversion, which runs the string through the parser and casts. So a generated name that the parser
reads as something other than a variable does not come back as one.
Four lowercase letters can spell
true. The parser reads that as a boolean, and the conversionthrows
CannotParseInstanceException: Cannot parse an instance of Variable from 'true'— the exactmessage in the issue. One name in
26^4, and .NET randomises string hash codes per process, so thesame expression picks a different name on every run. That is why it could not be reproduced: three
attempts are recorded in the issue, including the full suite at
maxParallelThreads=2three times.The same four letters can also spell a variable the predicate already uses, and then the rename
captures it and the set means something else. No exception for that one.
The fix
Variable.CreateTemp(Predicate.Vars), which the class already trusts for this exact purpose twomethods below —
GetHashCodealpha-normalises withCreateVariableUnchecked("%"). It reads thepredicate's variables rather than its hash and returns
%1upward, skipping indices already taken, soit is fresh by construction, deterministic across processes, and unreadable as anything but a variable:
%is not a token the parser accepts, so no parsed input can collide with it. Nesting works outbecause the inner set's renamed predicate is part of the outer's variables, so the outer binder takes
%2.CreateRandomhad this one caller and is removed.What a caller sees
Nothing, unless they read
DirectChildrendirectly:new ConditionalSet("x", "x > 0").DirectChildren[0]abcd > 0, a different name every process%1 > 026^4%1 > 0{ x : x > 0 }.Stringize()Solveanswers containing a conditional setStringizereads the node's own fields, not itsDirectChildren, so printed output is untouched —checked on
(x - a)(x + a) <= 0, whose answer carries a conditional set, and it still prints{ x : ... }with its own binder. It is inBREAKING-CHANGES.mdregardless, becauseDirectChildrenispublic. Nothing could have depended on the old name, which differed from run to run.
Measured
The new tests fail 5 of 8 against
masterand pass 8 of 8 here, so they pin the fix rather thandescribe it. They assert the two properties the name has to have — that it is a temporary, and that a
nested binder does not reuse the inner one's — plus that a free variable is untouched, that
alpha-equivalent sets still compare equal, and that
%1is not something the parser produces, which iswhat makes the name safe.
Suite 6341 passed / 0 failed. casbench 117/119 with 0 wrong, rootcheck 596/596, simpsweep
10463/10463, propcheck 1340 checks with 0 failures, crashcheck 1652 cases with 0 crashes and 0
unexpected throws, boundcheck unchanged at master's 4 disagreements.
Cut from
masterat5397c6f9. It shares no file with #901 or #903 exceptBREAKING-CHANGES.md,where the three sections sit in different places — #901 and #903 merged cleanly against each other for
that reason.