Repository navigation
Design document: individually addressable rewrite rules (#746 item 50) #825
Description
Activity
- added a commit that references this issue
on Aug 8, 2026 Two findings from building
rulecheck, a harness for #746 tier 2's "confluence and termination checked by tooling rather than asserted by authors". Both are input to the design this issue is about rather than defects, so they are here rather than in issues of their own.1. The declared metadata distinguishes nothing
All 30 rule sets in
RewriteRulesdeclareTransformationRelation.EquivalenceandSoundness.SoundUnderAssumptions. Every one, identically.So no tool can hold a set to a stronger claim than its neighbour, and the
Soundnessfield carries no information at the moment it is read. Tier 2 asks for a "justification tier" as part of rules-as-data; for that to be worth having, it has to be data that varies — a set whose rules are unconditionally true over ℂ is a different thing from one whose rules need a domain assumption, and today they are spelled the same.The one thing that is checkable as written is
Equivalence, and checking it found #936 —RewriteRules.NumericNeatanswering2for-1 + -1, a wrong answer through public API that noSimplify-based harness could see, because the rule only fires on numerals and evaluation had already covered for it.2. A rule set is not a terminating rewrite system on its own
Measured over 1365 applications on generated input, iterating each set to a fixed point two ways — alone, and with
InnerSimplifiedbetween passes, which is howsimplifyChildrenactually composes them:0 never settle 8 cycle when iterated alone, settle once the normalisation runs between passes 0 settle alone but not composed The eight are in
NumericNeat(3),Power(3) andCommon(2).--xunderNumericNeatgrows-1 * 1 * 1 * 1 * ...for ever, because the rule keeps producing a unit factor that only the normalisation folds.(-x)^2underPoweralternates between(-1)^2 * x^2and its regrouping.None of this is a defect in the simplifier — the pipeline composes them exactly the way that terminates, and I checked that before writing it down, having first recorded them as eight non-termination bugs and been wrong. But it matters here, because the premise of individually addressable rules is that a caller reaches for one on its own. Today:
- nothing in
RewriteRuleSetsays whether iterating it terminates; - nothing says it is only half of a rewrite system whose other half is
InnerSimplified; - and
ApplyOnceis public, so a caller can already write the loop that does not end.
Whatever shape the design takes, termination wants to be a property the type records and a tool checks, in the same way this issue wants provenance and cost recorded. The harness is in the analysis workspace (
work/rulecheck) and its report names the eight, so the check exists and can be pointed at whatever the rules become.- nothing in
Third measurement, and the one most directly about priorities: 161 of the 435 rule-set pairs do not commute.
rulechecknow applies A-then-B against B-then-A, normalising after each so the comparison is between settled trees rather than half-finished ones. Every one of the 435 pairs does something in at least one order; 161 of them land somewhere different depending on which order they ran in.first second example A then B B then A CanonicalOrderCommon(1/2)^(1/2)sqrt(2) / 21/2 * sqrt(2)CommonPowerln(1/2)ln(1/2)-ln(2)CanonicalOrderCollapseMultipleFractions2 / x2 / x2 * 1 / xCanonicalOrderFactorization0 ^ x0 provided x / 2 * (...) > 00 provided 1/2 * (...) * x > 0Almost all of these are presentation rather than soundness —
sqrt(2)/2and1/2 * sqrt(2)are the same number,ln(1/2)and-ln(2)the same value. That is what makes it a priorities question rather than a bug list: the order is not deciding whether the answer is right, it is deciding which of several right answers a user sees, andSimplifythen breaks ties by generation order (seeSimplifiedRate— differently-shaped forms rate equal far more often than one would hope).So the hardcoded sequence in
Simplificator.simplifyChildrenis load-bearing for output in a way nothing records. Two consequences for the design here:- A pair that commutes may be reordered freely and a pair that does not may not. 274 of 435 commute; those are free. The other 161 are where "rule priorities" has to mean something, and they are now enumerated rather than guessed at.
- Priority cannot be a single number per rule if the goal is a predictable form, because the conflicts are pairwise and not obviously transitive. Whatever the design chooses, this matrix is the thing to check it against, and re-running it after a change says whether the change moved the conflict set.
The harness and its report are in the analysis workspace (
work/rulecheck,work/rulecheck.md); the matrix is regenerated by running it, so it can be diffed across a change rather than trusted from this comment.I tried to act on my own suggestion — audit the 30 sets and give the
Soundnesstier something to vary over — and the audit's result is that it cannot vary at set granularity, which is a sharper argument for this issue than the observation that it currently doesn't.Soundness.cssays the conservatism is deliberate: "the registry starts conservative on purpose: tightening a label needs an argument, loosening one does not." So the exercise is to produce the argument per set. I could not produce one for any of them, and the reason is the same every time.A set's tier is the minimum over its arms, and every set is a heterogeneous bag. Two worked examples:
NumericNeatis the best candidate there is — every arm is a sign rearrangement among real numerals,(-a) + (-b) = -(a + b)and so on, unconditional. Except the four that regroup a quotient:(-n·a)/c→-(n·(a/c))holds only wherec ≠ 0. The enum lists "wherever both sides are defined" as an assumption, so those four arms areSoundUnderAssumptionsand they set the tier for all eighteen.SetOperatoris the next best —A ∩ A = A,A ∪ A = A,A \ A = ∅, distributivity over a union, all unconditional for sets. Exceptx ∈ [a, b]paraphrased into inequalities, which differs at complexx:i ∈ [0, 1]is false and0 <= i and i <= 1isNaN, the same branch that madep or not punsound.
Every other set touches division, a branch cut or a domain-sensitive rewrite somewhere in its
switch.So the tier belongs on the rule, not on the set — which is exactly what this issue is for. And the reason it cannot be put there today is not that nobody has got round to it: a rule set is a
switchexpression, so its arms are not values, cannot be enumerated, cannot be counted, and cannot carry a tier each. Individually addressable rules are the prerequisite for the metadata being informative, rather than a nice-to-have alongside it.Two things done rather than proposed:
rulechecknow enforces the declaration instead of merely reporting against it. A set declaringSoundthat changes a value at a point where both sides are defined is an error; the same observation underSoundUnderAssumptionsstays information, because that tier permits it and no tool can tell an assumption from a mistake. Today that reads0 of 30 declare Soundand0 violations, which is honest and uninteresting — the point is that the moment a label is tightened, something checks it, so tightening can be incremental and safe.- The report records the tier distribution, so "the metadata still distinguishes nothing" is a number that moves rather than a remark someone has to notice.
Implemented and merged in #951.
What landed against this document:
- A source generator over the existing
switchbodies, as the "What follows" section argued for — 347 rules across 16 rule sets, each with its pattern, guard, replacement, source line, node types and direction. RewriteStepnow names which rewrite fired rather than which set, which is the grain Add a way to collect intermediate pattern replacements when simplifying #28 asked for.- The transcription objection — the one this document said the measurement did not dispose of — is answered by construction rather than by care: each arm is copied verbatim as syntax into the generated code, so a divergence is a compile error rather than a silent change.
Two things worth recording here, since this document is the place they will be looked for.
The generator found four unreachable arms. Three in
Patterns.Common.cs, one inPatterns.Power.cs, each an exact duplicate — same pattern, same guard, same result — of an arm above it, and so unable to ever fire. The compiler cannot warn about them, because a guarded arm never marks a later arm unreachable. They are removed, no answer changes, and a test now fails the build if another appears. That is the "order is semantics" concern in this document turning up something real on the first run.The measurement that made item 51 depend on this one has now been re-run, and it holds.
work/egraphwas re-run with rules carrying their direction: withholding the 60 rules that expand ends the saturation blow-up inside the addressable half — every expression saturates, none above 19 e-nodes, where the same configuration with all rules reaches thousands — while still findingsin(x)^2 + cos(x)^2 = 1. Direction was the binding constraint.What is left, and what this document did not anticipate: the 14 sets that are not a
switch— the sorts, polynomial division, the factorial rules — have no arms to generate from, so they can state nothing. They are now the binding constraint for item 51 rather than the rule grain is.Leaving this open rather than closing it: the design is implemented, but it was never marked
Accepted, so whether it is the shape you want is still yours to say.- A source generator over the existing
- added 7 commits that reference this issue
on Aug 16, 2026 31 remaining items
- added 12 commits that reference this issue
on Sep 4, 2026 Closing as delivered. Since the comment above (27 of 30 sets), #1192 repointed the last three — the
CanonicalOrderfamily — so every one of the 30 registered rule sets runs as data and describes the rules it runs; theswitchspellings remain only because the agreement test holds the two to each other. A step names the arm that fired and carries the rule itself (pattern, guard, replacement, growth, source line),RewriteStep.Soundnessis the rule's own tier rather than its set's, and every rule carries a name, an identity and a growth declaration or a reason beside it for not having one (#1195–#1197). What this document asked for under #746 item 50 is on master; what remains around the graph is tracked on #746 itself and on #1200.
Design document for item 50 of #746 — "the rule registry: turn the pattern set into enumerable, attributable data without regressing
Simplifyperformance".The registry half landed in #818: all thirty rule sets the simplifier applies are named, attributed and enumerable, and
Simplifygot faster (allocation 157.6 → 125.8 KB). What remains is the finer grain — making the individual rewrites addressable, which is what #28 actually asks for and what #819 could only approximate at rule-set level.The reason given for not doing it was a performance claim, and I made it repeatedly — in the code, in the docs, on #28 and on #746:
I measured it. It is not true. This document is mostly that measurement, because the whole decision turned on it.
What was measured
Fifteen rules transcribed from
Patterns.CommonRules, in four shapes, applied throughEntity.Replaceover a 259-node expression (the oneDotnetBenchmarkuses forSimplifyHard). All four produce identical output, verified by structural equality, and identical allocation.switch, as the library writes it todayDictionary<Type, …>switchinstead of a dictionaryMethod: 3000 warmup iterations, then the minimum of seven rounds of 3000 — the minimum rather than the mean because every source of error here adds time, so the fastest round is the least interfered with. net10.0, Release, x64.
Results
Reproduced across three separate process runs, within ±0.0004 ms.
The mechanism is unsurprising once seen: most of the 259 nodes cannot match any rule in the set, and a type-indexed dispatch rejects those in one test, while a source-ordered switch works through the arms.
Does it hold as the set grows?
Fifteen rules is the small end;
Patterns.CommonRuleshas about forty arms. Twenty further rules were added to both shapes, on node types this expression does not contain — so the answer is unchanged and only the dispatch grows:The switch gets faster when it gets bigger — from 0.0054 to 0.0025 — and lands exactly on the bucketed registry. That is Roslyn: given enough arms over enough distinct types, it stops emitting sequential type tests and emits a real type dispatch.
Which is the most useful thing in this document. The compiler is already doing the bucketing. A registry that dispatches on node type is not a tax we would be paying for addressability — it is the same strategy, written down as data instead of inferred from the source order of a
switch.What follows
The performance argument against per-rule granularity does not survive measurement, at either size, in either direction. Nothing here is a reason not to proceed.
The real costs are elsewhere, and they are about people rather than machines:
All three point at the same answer: a source generator over the existing
switchbodies, rather than a hand transcription. The pattern already states the node type in its outermost position, and the arm order is already the priority order — so the generator has everything it needs, theswitchstays the thing a human edits, and the registry becomes a build artefact that cannot drift from it. That also keeps #746's constraint that extensibility must not be bought with runtime reflection.What I am not proposing
Not equality saturation, not an e-graph, not a rewrite of the rule sets. Only that the rewrites the library already has become individually named, so that #28 can be answered at the grain it asks for and a derivation can say which rule fired rather than which set.
Corrections owed
The claim this document refutes is currently written into the repository in four places —
RewriteRuleSet.cs's remarks,Docs/Contributing/Transformations.md, and my comments on #28 and #746. I will correct all four regardless of what is decided here; an unmeasured performance claim sitting in the source as justification is worse than the design question being open.Limits of the measurement
One rule set, one expression, one machine, one runtime. The filler rules in the scaling test never match, so it stresses dispatch and not within-bucket ordering; a set where many rules match the same node type would exercise that instead. The harness is small and I am happy to hand it over or extend it — in particular, running it against the real
Patterns.CommonRulesrather than a fifteen-rule transcription would settle the remaining doubt.