What happens
RewriteRules.NumericNeat inverts the sign when both operands of a sum or a difference are negative numerals. Measured on a clean build of master at 1596bf1, .NET 10, default settings:
RewriteRules.NumericNeat.ApplyOnce("-1 + -1") -> 2 the value is -2
RewriteRules.NumericNeat.ApplyOnce("-2 + -3") -> 5 the value is -5
RewriteRules.NumericNeat.ApplyOnce("-1 - (-1)") -> 2 the value is 0
This is a wrong answer, not a coverage gap, and it is reachable through public API: RewriteRules and RewriteRuleSet.ApplyOnce are both public, and Transformation.Rewriting(RewriteRules.NumericNeat) is the documented way to run a single rule set.
Why nothing caught it
Simplify and Evaled are both correct — "-1 + -1".Simplify() is -2 — because evaluation folds a pair of numerals before this rule is ever consulted. The rule only ever fires on numerals, and on numerals something else has already produced the right answer, so the defect has no way to reach the corpora. casbench, propcheck, simpsweep and boundcheck all exercise Simplify, so none of them can see it.
That is the general shape of it: a rule that only fires where evaluation already covers for it can be arbitrarily wrong and stay invisible, until something applies the rule on its own. The transformation layer made that possible, and this is the first thing to look through it.
Where
Patterns.NumericNeatRules, the two branches where both operands are negative:
Sumf(Real { IsNegative: true } left, Real { IsNegative: true } right) => -(left + right),
Minusf(Real { IsNegative: true } left, Real { IsNegative: true } right) => -left + -right,The first negates a sum that is already negative: with left = -a and right = -b, left + right is -(a+b) and negating it gives a + b. It should be -((-left) + (-right)).
The second computes a + b where (-a) - (-b) is b - a. It should be (-right) - (-left).
Every neighbouring branch is right — the four mixed-sign sum and difference cases, and the both-negative product and quotient — so this is two lines rather than a design problem.
How it was found
rulecheck, a new harness for #746 tier 2, which asks for "confluence and termination checked by tooling rather than asserted by authors". Every RewriteRuleSet declares a TransformationRelation and a Soundness and nothing has ever checked either. The harness applies each set to generated expressions and, for a set declaring Equivalence, compares the value at sample points on and off the real line.
It also reports 8 non-termination findings across NumericNeat, Power and Common — NumericNeat on --x produces -1 * 1 * 1 * 1 * ... without ever settling — which want their own issue once these two lines are fixed, since one of them is the same rule set.
And a remark for #825: all 30 rule sets declare the same relation and the same soundness, so the metadata distinguishes nothing and no tool can hold one set to a stronger claim than its neighbour. Tier 2's "justification tier" wants to be data that varies.
What happens
RewriteRules.NumericNeatinverts the sign when both operands of a sum or a difference are negative numerals. Measured on a clean build ofmasterat1596bf1, .NET 10, default settings:This is a wrong answer, not a coverage gap, and it is reachable through public API:
RewriteRulesandRewriteRuleSet.ApplyOnceare both public, andTransformation.Rewriting(RewriteRules.NumericNeat)is the documented way to run a single rule set.Why nothing caught it
SimplifyandEvaledare both correct —"-1 + -1".Simplify()is-2— because evaluation folds a pair of numerals before this rule is ever consulted. The rule only ever fires on numerals, and on numerals something else has already produced the right answer, so the defect has no way to reach the corpora.casbench,propcheck,simpsweepandboundcheckall exerciseSimplify, so none of them can see it.That is the general shape of it: a rule that only fires where evaluation already covers for it can be arbitrarily wrong and stay invisible, until something applies the rule on its own. The transformation layer made that possible, and this is the first thing to look through it.
Where
Patterns.NumericNeatRules, the two branches where both operands are negative:The first negates a sum that is already negative: with
left = -aandright = -b,left + rightis-(a+b)and negating it givesa + b. It should be-((-left) + (-right)).The second computes
a + bwhere(-a) - (-b)isb - a. It should be(-right) - (-left).Every neighbouring branch is right — the four mixed-sign sum and difference cases, and the both-negative product and quotient — so this is two lines rather than a design problem.
How it was found
rulecheck, a new harness for #746 tier 2, which asks for "confluence and termination checked by tooling rather than asserted by authors". EveryRewriteRuleSetdeclares aTransformationRelationand aSoundnessand nothing has ever checked either. The harness applies each set to generated expressions and, for a set declaringEquivalence, compares the value at sample points on and off the real line.It also reports 8 non-termination findings across
NumericNeat,PowerandCommon—NumericNeaton--xproduces-1 * 1 * 1 * 1 * ...without ever settling — which want their own issue once these two lines are fixed, since one of them is the same rule set.And a remark for #825: all 30 rule sets declare the same relation and the same soundness, so the metadata distinguishes nothing and no tool can hold one set to a stronger claim than its neighbour. Tier 2's "justification tier" wants to be data that varies.