Skip to content

The e-graph moves from a harness into the kernel, behind an explicit opt-in - #1101

Merged
Rafael-SOWNet merged 3 commits into
masterfrom
tier2-inverse-pair-table
Aug 29, 2026
Merged

The e-graph moves from a harness into the kernel, behind an explicit opt-in#1101
Rafael-SOWNet merged 3 commits into
masterfrom
tier2-inverse-pair-table

Conversation

@Rafael-SOWNet

@Rafael-SOWNet Rafael-SOWNet commented Aug 28, 2026

Copy link
Copy Markdown
Member

Summary

#746 tier 2's row names two things remaining "in dependency order": no production caller for the reversible-rule mechanism, and folding on insertion. This closes the second (already proven in the work/egraph measurement harness — 7/16 → 15/16 corpus expressions saturating under the full rule set, neutral-element churn 13–34% → 0%) and gives the first a real, narrowly-scoped answer.

  • EGraph — the harness's e-graph design (union-find, hash-consed e-nodes, congruence rebuild, neutral-element folding on insertion) moved into the kernel unchanged, as an internal type.
  • MatchPattern.Construct → ConstructNode — widened from private to internal (as ConstructNode) so extraction rebuilds a node's type from the same registry the pattern-matching layer already trusts, instead of a second, independently-drifting operator list.
  • Transformation.EqualitySaturation(WorkBudget, CostModel) — the production caller. Builds an e-graph from the input, fires only rules whose RewriteRuleGrowth is Collects or Rearranges (withholding Expands and Unknown — unproven isn't the same as safe), bounded by AngouriMath.Core.Budgets.BudgetLedger (the same budget type Gröbner elimination already answers to), and extracts the cheapest candidate under the given CostModel.

Nothing runs this by default — same standing as RationalCanonicalization/Canonicalization. Simplify applies a rule set once and moves on; equality saturation deletes exactly that ordering, which is why it needs a budget rather than a pass count.

What this is not, stated in the doc comment rather than left implicit: the harness this is built from enumerates a class's terms and rewrites each — it finds what e-matching would, but by materialising terms a real e-matcher never builds. That instrument moved here unchanged; a production e-matcher over MatchPattern is not this, and tier 2 still names it as the production caller's other missing half. Nor does a 16-expression textbook corpus settle whether this generalises to what Simplify is actually asked to handle — the budget parameter is the honest acknowledgment of that, not a solved problem's formality.

A flake chased down, not papered over

a / b / c rewritten to a / (b * c) occasionally failed a numeric equality check under dotnet test, and never once across 2,300+ raw concurrent calls to the same code in an isolated process. Both chains are the same value reached by differently-ordered complex divisions; comparing them with the exact equality ExpressionNumerical.AreEqual uses is comparing two floating-point rounding paths, not the value each settles on. Fixed by verifying against Entity.EqualsImprecisely — the tolerance this library already has for exactly that comparison — rather than loosening what the transformation itself promises.

Test plan

  • TDD throughout: EGraph's union-find, hash-consing, congruence rebuild, and neutral folding (all 5 operator cases, including the 2 — 0 - x, 1 / x — that must not fold) each have a test that failed for the right reason before the fix.
  • Transformation.EqualitySaturation tested for its stated relation/soundness, that it declines to change an already-cheapest expression, that it never throws under a starved budget, and — across the existing TransformationTest.Corpus — that it never changes the value it claims to preserve (numerically, at several real check points).
  • Full suite: 8838 tests, 8824 passed, 14 skipped (pre-existing), 0 failed.
  • PublicApi.txt regenerated for the one new public member (Transformation.EqualitySaturation) — diff is exactly that one line.

🤖 Generated with Claude Code

@Rafael-SOWNet
The e-graph moves from a harness into the kernel, behind an explicit …
76def51 
…opt-in

#746 tier 2's own row names two things as remaining "in dependency order":
no production caller for the reversible-rule mechanism, and folding on
insertion. The second is done (this workspace's `work/egraph` harness,
proven against a 16-expression corpus: 7 of 16 saturating under the full
rule set became 15 of 16, neutral-element churn from 13-34% to 0%). This
gives the first a real, if narrowly-scoped, answer.

EGraph is that harness's design moved here unchanged: e-classes over a
union-find, e-nodes hash-consed by operator and child class, congruence
restored by Rebuild, neutral elements folded on insertion rather than
discovered later by a rule. `MatchPattern.Construct` -- until now `private`,
used to build a rule's right-hand side from bindings -- is exposed as
`ConstructNode` so extraction rebuilds a node's type from the same registry
the rest of the pattern-matching layer already trusts, rather than a second,
independently-drifting list of the same operators.

`Transformation.EqualitySaturation(WorkBudget, CostModel)` is the caller:
builds an e-graph from the input, fires every rule whose `RewriteRuleGrowth`
is `Collects` or `Rearranges` -- withholding `Expands` and `Unknown` for the
same reason, unproven is not the same as safe -- against
`AngouriMath.Core.Budgets.BudgetLedger`, the same budget type Gröbner
elimination already answers to, and extracts the cheapest candidate under
the given `CostModel`. Nothing runs this by default, the same standing as
`RationalCanonicalization` and `Canonicalization`: `Simplify` applies a rule
set once and moves on, so an expanding rule and a collecting one never meet,
and equality saturation deletes exactly that ordering.

What this is not, stated in its own doc comment rather than left implicit:
the harness this is built from enumerates a class's terms and rewrites each,
which finds what e-matching would but by materialising terms a real
e-matcher never builds. That instrument moved here unchanged. A production
e-matcher over `MatchPattern` is not this, and tier 2 still names it as the
production caller's other missing half. Nor does a 16-expression textbook
corpus settle whether this generalises to what `Simplify` is actually asked
to handle -- the budget is the honest acknowledgment of that, not a solved
problem's formality.

One test flake chased down rather than papered over: `a / b / c` rewritten
to `a / (b * c)` occasionally failed a numeric equality check under
`dotnet test` and never once under 2,300+ raw concurrent calls to the same
code in an isolated process. The two chains are the same value reached by
differently-ordered complex divisions, and comparing them by the exact
equality `ExpressionNumerical.AreEqual` uses is comparing two floating-point
rounding paths, not the value each settles on. Fixed by verifying against
`Entity.EqualsImprecisely` -- the tolerance this library already has for
exactly that comparison -- not by loosening what the transformation itself
promises.

TDD throughout: EGraph's union-find, hash-consing, congruence rebuild and
neutral folding (all five operator cases, including the two -- `0 - x`,
`1 / x` -- that must not fold) each have a test that failed for the right
reason before the line that makes it pass. `PublicApi.txt` regenerated for
the one new public member.
This was referenced Aug 28, 2026
Open
Merged
@Rafael-SOWNet
The inverse-pair table is not Growth's small extension, and here is why
476dc3d 
Tried the obvious move: give RewriteRule a Reversed the same way AsAddressable()
already gives it a Growth. Measured against the live registry rather than
assumed to work -- grep says AsAddressable() is called exactly once, for
RationalizeDenominator, and every other set's addressable Rules still comes
from RuleRegistryGenerator reading a switch's arms, kept around after the
exchange purely for that. Wiring Reversed into AsAddressable() alone therefore
changes nothing for 29 of 30 sets, and the one it does reach has two
code-built, non-reversible rules -- so the change measured zero reversible
rules registry-wide and was reverted rather than shipped speculative.

Recorded here rather than in a commit message that stops being read: what a
real fix costs (extending the generator to compute reversibility from syntax,
or re-deriving Rules from AsAddressable() for every converted set and
reconciling two independent renderings that have never been compared), and
why RationalizeDenominator specifically is the wrong set to prototype against.
Not fixed here -- estimating which option is worth its cost is a separate
question from measuring that the cheap option does not exist.
@Rafael-SOWNet

Rafael-SOWNet commented Aug 28, 2026

Copy link
Copy Markdown
Member Author

Added a follow-up commit: while working on this, tried extending Reversed/IsReversible onto the public RewriteRule the same way Growth is exposed there (tier 2's own text names the inverse-pair table as needing exactly that). Measured against the live registry before shipping it, found it changes nothing for 29 of 30 sets (only RationalizeDenominator flows through AsAddressable(), and its rules are non-reversible anyway), and reverted the code rather than ship something inert. Docs/Contributing/InversePairTable.md records what a real fix would need, so the next attempt starts from there instead of re-discovering it.

@Rafael-SOWNet @claude
A review caught the e-graph silently changing what it claimed to pres…
41f8121 
…erve

EGraph.Extract rebuilt every node through a bare constructor, which
restores neither Entity.Codomain nor the reference identity that keeps
EulerIntrinsic out of a binder over the name e -- both confirmed
wrong-answer bugs, both fixed with a regression test at the EGraph level
and at the public Transformation.EqualitySaturation level.

The other thirteen findings from the same review are recorded in
EqualitySaturationReviewFindings.md rather than fixed here: several
point at the same underlying gap (the e-graph's node model has nowhere
to carry metadata beyond raw tree shape), which is a design question
worth its own pass rather than a patch alongside these two.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@Rafael-SOWNet

Rafael-SOWNet commented Aug 29, 2026

Copy link
Copy Markdown
Member Author

A code review of this PR and #1102 found fifteen issues before either had a human reviewer. Two were confirmed wrong-answer bugs and are fixed in the latest commit, each with a regression test at the EGraph level and at this PR's own Transformation.EqualitySaturation level:

  • Codomain loss on every reconstructed node. EGraph.Extract rebuilt through a bare constructor (MatchPattern.ConstructNode), which restores nothing — the rest of the codebase copies Codomain forward on every Replace via a New(...) helper. A Codomain-narrowed subexpression (sqrt(-1) restricted to the reals evaluates to NaN, unrestricted to i) silently reverted to its type's default codomain, unconditionally, whether or not any rule fired.
  • EulerIntrinsic identity loss. The e-graph keys a leaf by its printed form, and Entity.Constant.EulerIntrinsic prints identically to the ordinary named constant e — the two are Equals-equal by design but only EulerIntrinsic is meant to stay outside what a binder over the name e can capture. Re-parsing the printed form silently substituted the named constant, invisible to every equality check and only wrong at a binder (sum(ln(x), e, 1, 2) after a round trip through the graph).

The other thirteen findings are recorded in EqualitySaturationReviewFindings.md rather than fixed here — several (a Providedf-wrapped result unioned onto a dead end, Extract's 14-type reconstruction whitelist, a NaN CostModel corrupting comparison) point at the same underlying gap: the e-graph's node model has nowhere to carry anything beyond raw tree shape. That's a design question worth its own pass rather than a patch alongside these two. The rest (budget-charge timing, an unused NodeTypes pre-filter, a duplicated operator-type list, RewriteRecording blindness, SimplifiedRate cache staleness on #1102) are each small and independent, and are listed there for whoever picks one up next.

Full suite green: 8828 passed, 14 skipped (pre-existing), 0 failed.

Rafael-SOWNet added a commit that referenced this pull request Aug 29, 2026
@Rafael-SOWNet @claude
Implementation plan for the real e-matcher
a1b4c1a 
11 TDD tasks covering EBindings, NodeCount/Growth on MatchPattern and
MatchedRule, the EGraph helpers e-matching needs, CanEMatch/EMatch/
ETryBuild on all four pattern kinds, MatchedRule.TryEMatchApply, and
rewiring EqualitySaturationTransformation to source from
Matching.MatchedRules. Also rebases this branch onto
tier2-inverse-pair-table (#1101), which EGraph.cs and
EqualitySaturationTransformation only exist on.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@Rafael-SOWNet Rafael-SOWNet mentioned this pull request Aug 29, 2026
Merged
5 tasks done
@Rafael-SOWNet
Rafael-SOWNet merged commit 3a9930b into master Aug 29, 2026
31 checks passed
Rafael-SOWNet added a commit that referenced this pull request Aug 29, 2026
@Rafael-SOWNet
Merge master after #1101 squash-merged: this branch already carries i…
2b43dd6 
…ts content
Rafael-SOWNet added a commit that referenced this pull request Aug 29, 2026
@Rafael-SOWNet @claude
A real e-matcher: matching a pattern against an e-class, not a term (#…
77d1c70 
…1103)

* The e-graph moves from a harness into the kernel, behind an explicit opt-in

#746 tier 2's own row names two things as remaining "in dependency order":
no production caller for the reversible-rule mechanism, and folding on
insertion. The second is done (this workspace's `work/egraph` harness,
proven against a 16-expression corpus: 7 of 16 saturating under the full
rule set became 15 of 16, neutral-element churn from 13-34% to 0%). This
gives the first a real, if narrowly-scoped, answer.

EGraph is that harness's design moved here unchanged: e-classes over a
union-find, e-nodes hash-consed by operator and child class, congruence
restored by Rebuild, neutral elements folded on insertion rather than
discovered later by a rule. `MatchPattern.Construct` -- until now `private`,
used to build a rule's right-hand side from bindings -- is exposed as
`ConstructNode` so extraction rebuilds a node's type from the same registry
the rest of the pattern-matching layer already trusts, rather than a second,
independently-drifting list of the same operators.

`Transformation.EqualitySaturation(WorkBudget, CostModel)` is the caller:
builds an e-graph from the input, fires every rule whose `RewriteRuleGrowth`
is `Collects` or `Rearranges` -- withholding `Expands` and `Unknown` for the
same reason, unproven is not the same as safe -- against
`AngouriMath.Core.Budgets.BudgetLedger`, the same budget type Gröbner
elimination already answers to, and extracts the cheapest candidate under
the given `CostModel`. Nothing runs this by default, the same standing as
`RationalCanonicalization` and `Canonicalization`: `Simplify` applies a rule
set once and moves on, so an expanding rule and a collecting one never meet,
and equality saturation deletes exactly that ordering.

What this is not, stated in its own doc comment rather than left implicit:
the harness this is built from enumerates a class's terms and rewrites each,
which finds what e-matching would but by materialising terms a real
e-matcher never builds. That instrument moved here unchanged. A production
e-matcher over `MatchPattern` is not this, and tier 2 still names it as the
production caller's other missing half. Nor does a 16-expression textbook
corpus settle whether this generalises to what `Simplify` is actually asked
to handle -- the budget is the honest acknowledgment of that, not a solved
problem's formality.

One test flake chased down rather than papered over: `a / b / c` rewritten
to `a / (b * c)` occasionally failed a numeric equality check under
`dotnet test` and never once under 2,300+ raw concurrent calls to the same
code in an isolated process. The two chains are the same value reached by
differently-ordered complex divisions, and comparing them by the exact
equality `ExpressionNumerical.AreEqual` uses is comparing two floating-point
rounding paths, not the value each settles on. Fixed by verifying against
`Entity.EqualsImprecisely` -- the tolerance this library already has for
exactly that comparison -- not by loosening what the transformation itself
promises.

TDD throughout: EGraph's union-find, hash-consing, congruence rebuild and
neutral folding (all five operator cases, including the two -- `0 - x`,
`1 / x` -- that must not fold) each have a test that failed for the right
reason before the line that makes it pass. `PublicApi.txt` regenerated for
the one new public member.

* The inverse-pair table is not Growth's small extension, and here is why

Tried the obvious move: give RewriteRule a Reversed the same way AsAddressable()
already gives it a Growth. Measured against the live registry rather than
assumed to work -- grep says AsAddressable() is called exactly once, for
RationalizeDenominator, and every other set's addressable Rules still comes
from RuleRegistryGenerator reading a switch's arms, kept around after the
exchange purely for that. Wiring Reversed into AsAddressable() alone therefore
changes nothing for 29 of 30 sets, and the one it does reach has two
code-built, non-reversible rules -- so the change measured zero reversible
rules registry-wide and was reverted rather than shipped speculative.

Recorded here rather than in a commit message that stops being read: what a
real fix costs (extending the generator to compute reversibility from syntax,
or re-deriving Rules from AsAddressable() for every converted set and
reconciling two independent renderings that have never been compared), and
why RationalizeDenominator specifically is the wrong set to prototype against.
Not fixed here -- estimating which option is worth its cost is a separate
question from measuring that the cheap option does not exist.

* A review caught the e-graph silently changing what it claimed to preserve

EGraph.Extract rebuilt every node through a bare constructor, which
restores neither Entity.Codomain nor the reference identity that keeps
EulerIntrinsic out of a binder over the name e -- both confirmed
wrong-answer bugs, both fixed with a regression test at the EGraph level
and at the public Transformation.EqualitySaturation level.

The other thirteen findings from the same review are recorded in
EqualitySaturationReviewFindings.md rather than fixed here: several
point at the same underlying gap (the e-graph's node model has nowhere
to carry metadata beyond raw tree shape), which is a design question
worth its own pass rather than a patch alongside these two.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* Spec: a real e-matcher for EqualitySaturation

Design document for the other half PR #1101's own doc comment names as
missing -- matching MatchPattern against an e-class directly, rather than
enumerating a class's terms and rewriting each. Scoped by two findings made
before committing to it rather than assumed:

Checked against the measurement rather than assumed to help: the original
motivation (letting Growth.Expands rules join SafeRules safely) does not
follow from switching matchers. The harness's measured blowup happened with
hash-consing and congruence closure already in place, found through term
enumeration -- an expand rule mostly produces genuinely new shapes each time,
so congruence closure (which catches exact repeats) does not bound it either
way. This document is scoped to what e-matching actually buys -- not
materialising a term to find a rule's shape -- and says so rather than
quietly keeping the original framing.

Checked which rules even have a MatchPattern to e-match against: most of
RewriteRules.All is still RuleRegistryGenerator output -- text rendered from
a switch arm's Roslyn syntax, not a MatchPattern object -- per
InversePairTable.md's measurement. The real patterns live in the internal
Matching.MatchedRules catalogue, so EqualitySaturationTransformation's rule
source moves there, which is a same-assembly reference needing no visibility
widening.

Not implemented here. GatheredPattern (n-ary chain matching) is out of scope
-- already "the one shape that has to be enumerated" against a single
concrete Entity per its own documentation, and matching it against a class
that can bundle many equivalent tree shapes has no obvious bound the way
NodePattern's does. A pattern containing one anywhere falls back to today's
extract-then-TryApply path.

* Implementation plan for the real e-matcher

11 TDD tasks covering EBindings, NodeCount/Growth on MatchPattern and
MatchedRule, the EGraph helpers e-matching needs, CanEMatch/EMatch/
ETryBuild on all four pattern kinds, MatchedRule.TryEMatchApply, and
rewiring EqualitySaturationTransformation to source from
Matching.MatchedRules. Also rebases this branch onto
tier2-inverse-pair-table (#1101), which EGraph.cs and
EqualitySaturationTransformation only exist on.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* Matching.MatchedRules gains a real All, and a test stops reflecting on its own

* EBindings: Bindings' cons-list, over e-class ids instead of entities

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* MatchPattern.NodeCount: an exact structural count, for Growth to use

* MatchedRule.Growth: an exact node-count classification, not a string-length proxy

* EGraph.ContainsLeaf and .RuntimeType: what e-matching needs from the graph

* WIP: CanEMatch/EMatch/ETryBuild on MatchPattern, ExactPattern and GatheredPattern

* WIP: AnyPattern e-matches and e-builds

* NodePattern e-matches recursively, trying both orders when commutative

* AnyPattern.EMatch: decline rather than crash on a wrong-typed extracted witness

EMatch's eligibility check only asks whether *some* e-node in the class
satisfies the required type; the cost-cheapest witness it extracts for a
'where' predicate can be a different e-node of the same class entirely, and
Any<T>(name, where) compiles 'where' as an unguarded cast to T. ETryBuild
already guarded this with required.IsInstanceOfType(witness) before calling
where; EMatch now applies the same guard, declining the candidate instead of
throwing InvalidCastException. Not reachable from today's registry rules --
covered here with a hand-built adversarial cost model, since it needs a class
holding two congruent representations of different types, which real
EqualitySaturation unions (Tasks 10-11) will produce.

* MatchedRule.TryEMatchApply: what TryApply does, against an e-class directly

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* EqualitySaturation draws rules from Matching.MatchedRules and e-matches where it can

* Cache a failed extraction too, so TryTerm re-extracts at most once per class per round

* Verification: e-matching agrees with matching, crosses a union, and builds the same

Adapted two of the brief's three tests against what the registry and the
e-graph actually contain, probed directly rather than assumed:

- EMatchingAgreesWithMatching needed a guard the brief's text did not
  anticipate. EGraph.Add folds a neutral-element application into its other
  operand on insertion (`x * 1`, `x + 0` never get a Mulf/Sumf e-node at
  all -- deliberate, pre-existing behaviour, not part of this plan), and
  EGraph.Extract can only rebuild the 14 node types MatchPattern.Construct
  knows how to build, so any node type outside that list anywhere in the
  tree (Factorial, the boolean connectives, a comparison, a set operator)
  makes the class unreconstructible -- a gap EqualitySaturationReviewFindings.md
  already records. Both are properties of the EGraph and MatchPattern.Construct
  that Tasks 1-2 built, not defects in the e-matching added by Tasks 5-9.
  Skipping a corpus row where the graph does not faithfully represent what
  was inserted leaves 11 of 18 rows and 69 (rule, row) pairs genuinely
  checked, and it is exactly those seven rows that failed before the guard
  existed, and no others.

- EMatchingFindsAMatchThatCrossesAUnion's `.First(RequiredRootType == Mulf)`
  picked whichever Mulf-rooted rule came first in registry order, which does
  not mean it matches `2 * x` on any graph -- filtered instead for a rule
  that actually fires on this one.

- ETryBuildAgreesWithTryBuildOnTheSameBindings's `.First(Right.CanEMatch)`
  followed by a corpus lookup hit the same failure mode
  MatchedRuleTryEMatchApplyTest already found and fixed (its own comment:
  "the first few such rules ... fire on none of the eighteen corpus rows"):
  picked a rule with no corpus row to apply to and returned early, never
  calling TryEMatchApply. Fixed the same way: search (rule, source) pairs
  together for one that fires.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* EMatchingAgreesWithMatching asserts its own skip list instead of trusting it

Review finding: the guard that skips a corpus row because the e-graph
cannot faithfully represent it (neutral-element folding, or a node type
outside the 14-type reconstruction whitelist) produced a plain "Passed"
indistinguishable from a row that ran the full 69-pair check. A future
regression widening what EGraph.Add/Extract cannot represent would make
this test keep reporting "18 passed" with no signal that coverage shrank.

Added an explicit, named list of the seven rows expected to hit the guard,
each with its own diagnosed cause, and assert row membership when the
guard fires -- so an eighth, unlisted row hitting it fails loudly instead
of silently joining the pass count. Verified the assertion is load-bearing
by removing one entry (`phi(12)`) and confirming the test fails with a
specific message naming that row, then restoring it.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* Plan addendum: close the final review's Critical rule-collapse finding

The final whole-branch review found SafeRules collapsed to 23 rules
because 266 of 298 registry rules are code-built and can't be
classified by node-count Growth. Decided with Rafael: extend rather
than ship as-is. Tasks 12-13 add a declared-Growth mechanism for
code-built rules (mirroring how Soundness is already declared, not
derived) and apply it to a first, conservatively-scoped batch. Task 14
closes the remaining findings (dropped exception guard, vacuous test,
false doc comment) against the real final count.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* A code-built rule can declare its own Growth, the same way Soundness is declared

* A first batch of code-built rules declare a Growth they can justify by inspection

* Close the final review: restore the exception guard, measure SafeRules, correct the doc comment

- ApplyCore's e-match branch now wraps TryEMatchApply in try/catch, mirroring the
  fallback branch's existing guards around TryApply/AddEntity (final review finding I2).
  Traced TryEMatchApply and EGraph.Extract by hand: Extract already swallows a failing
  cost model internally, and Evaled is documented and implemented to be total, so the
  named rule's own when clause cannot be forced to throw with real data today -- the
  live hazard is the unguarded `when(forWhen)` call itself, reproduced directly against
  a throwaway rule built the way MatchedRuleGrowthTest already builds one.
- Replaced the vacuous EqualitySaturationNowDrawsFromMatchingMatchedRules test (which
  passed on Parse("x + 0") even with SafeRules empty, since EGraph.Add's neutral-fold
  removes it before any rule runs) with a real sin(arcsin(x)) -> x case that e-matches
  and is not folded away on insertion (final review finding C1, test half).
- Added SafeRulesHasAtLeastAFloor, a kept regression test against SafeRules.Count,
  exposed to the Tests assembly via a small internal accessor since the field itself is
  private on a private nested class. Measured (and force-failed once to confirm): 43
  rules pass the filter today; floor set to 38 (final review finding C1, measurement
  half).
- Corrected EqualitySaturation's doc comment, which still said a production e-matcher
  "is not this" and cited a 16-expression measurement made under a since-superseded
  rule population (final review finding I7). States the real filter (Growth, derived or
  declared since Task 12, and Soundness), the real count (43, of which ~27-28 can
  currently build a replacement -- the remaining ~15 build a boolean connective or a
  turned-around equality and are correctly classified but blocked by EGraph's 14-type
  reconstruction whitelist, a separate known limitation), and that the old harness
  measurement should not be read as describing this population without being re-run.

Full suite: 8874 passed, 14 skipped (pre-existing), 0 failed.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* Correct an inverted fact and drop unresolvable review-label citations

The doc comment said the original work/egraph measurement was made
under "a much smaller rule set" than today's 43 -- it was actually
made under a much larger one (313 rules, off the public registry's
string-length Growth proxy, before the Soundness filter or e-matching
existed). Fixed the direction and named what actually differs.

A few comments cited "final review finding C1/I2" as if a reader could
look that up -- those labels only ever existed in this session's local
review ledger, never shipped. Reworded to describe the issue plainly
instead of pointing at an unresolvable reference, and corrected a
stale "23" (the count before it grew to 24) quoted forward rather than
re-measured, in a comment whose whole point is that numbers must be
measured. EMatching.md's present-tense claim about which registry
EqualitySaturation draws from is now past tense with a pointer to
where that changed.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
Rafael-SOWNet added a commit that referenced this pull request Aug 29, 2026
@Rafael-SOWNet
Close four of the recorded e-graph review findings, one of them misdi…
1b7cb6b 
…agnosed

The review pass on #1101/#1102 recorded thirteen findings it did not fix. Four of them
were independent of the open design question about e-node metadata, so they go first.

`Extract` declines a candidate its cost model cannot rank. `here >= bestCost` is false
whenever either side is NaN, so a NaN cost became the incumbent cheapest and every
candidate after it then won unconditionally -- the answer stopped being the cheapest and
became whichever member the enumeration reached last. A cost model that throws is already
declined by the surrounding catch; one that answers NaN is saying the same thing.

`Extract` settles a cost tie on a defined order. HashSet enumeration order is unspecified
and string hashing is randomised per process, so one run's tie-break was not the next
run's. ENode gains a total order -- ordinal on the operator, then children.

`Extract` declines to build past a depth of 256. Its cycle guard bounds the chain only by
the number of distinct classes, which unions grow past the input's own syntactic depth,
and a StackOverflowException cannot be caught. Same shape as Gruntz.MaxDepth.

`WorkBudget.Steps` now bounds something. This is the one the review got wrong: it was
recorded as a timing defect -- the growth charge landing after a sweep rather than before
the next one. Measuring it found the timing is not the problem. Steps charged the e-graph's
node-count growth, and SafeRules is by construction the rules whose Growth does not expand,
so on ordinary input the ledger was charged nothing whatever: under Steps = 0, three of
five varied expressions ran the entire sweep to saturation and reported that they had
completed, never having reached a ceiling. Time was the only bound really holding. A step
is now one unit of work attempted, charged before the attempt, as Buchberger, FGLM and
MatchPattern all charge; the growth charge stays alongside it and moves after the sweep;
and Rebuild's full-graph rescan is charged for the first time.

The findings document is updated to match, including the correction to its own account of
the budget finding -- the wrong diagnosis was the more flattering one, since a bound that
is slightly late reads as a rounding error where a bound that never fires is the feature
missing.

Full suite: 8885 passed, 14 skipped (pre-existing), 0 failed.
@Rafael-SOWNet Rafael-SOWNet mentioned this pull request Aug 29, 2026
Merged
Rafael-SOWNet added a commit that referenced this pull request Aug 30, 2026
@Rafael-SOWNet
Close twelve of the thirteen recorded e-graph review findings (#1104)
841c3f1 
* Close four of the recorded e-graph review findings, one of them misdiagnosed

The review pass on #1101/#1102 recorded thirteen findings it did not fix. Four of them
were independent of the open design question about e-node metadata, so they go first.

`Extract` declines a candidate its cost model cannot rank. `here >= bestCost` is false
whenever either side is NaN, so a NaN cost became the incumbent cheapest and every
candidate after it then won unconditionally -- the answer stopped being the cheapest and
became whichever member the enumeration reached last. A cost model that throws is already
declined by the surrounding catch; one that answers NaN is saying the same thing.

`Extract` settles a cost tie on a defined order. HashSet enumeration order is unspecified
and string hashing is randomised per process, so one run's tie-break was not the next
run's. ENode gains a total order -- ordinal on the operator, then children.

`Extract` declines to build past a depth of 256. Its cycle guard bounds the chain only by
the number of distinct classes, which unions grow past the input's own syntactic depth,
and a StackOverflowException cannot be caught. Same shape as Gruntz.MaxDepth.

`WorkBudget.Steps` now bounds something. This is the one the review got wrong: it was
recorded as a timing defect -- the growth charge landing after a sweep rather than before
the next one. Measuring it found the timing is not the problem. Steps charged the e-graph's
node-count growth, and SafeRules is by construction the rules whose Growth does not expand,
so on ordinary input the ledger was charged nothing whatever: under Steps = 0, three of
five varied expressions ran the entire sweep to saturation and reported that they had
completed, never having reached a ceiling. Time was the only bound really holding. A step
is now one unit of work attempted, charged before the attempt, as Buchberger, FGLM and
MatchPattern all charge; the growth charge stays alongside it and moves after the sweep;
and Rebuild's full-graph rescan is charged for the first time.

The findings document is updated to match, including the correction to its own account of
the budget finding -- the wrong diagnosis was the more flattering one, since a bound that
is slightly late reads as a rounding error where a bound that never fires is the feature
missing.

Full suite: 8885 passed, 14 skipped (pre-existing), 0 failed.

* One table of buildable node types, and it is three times longer

Three more of the recorded findings, all with one cause: the fourteen node types
`MatchPattern.Construct` built were what it had accumulated, not a boundary anyone chose.

`EGraph` kept a second copy of that list to resolve an e-node's operator back to a type,
next to a doc comment on `Construct` warning that a list written twice is a list that
drifts. Now one table holds the type, its arity and the constructor call together, and
`BuildableNodeTypes`, the name lookup and `CanConstruct` are all derived from its keys --
there is no second list left to drift from. A table rather than a chain of
`nodeType == typeof(T)` tests also makes it O(1) rather than linear in the list, which
matters more now.

`Extract` silently no-opped on any root outside the list, and a rule wrapping a conditional
result in `Providedf` -- the registry's own convention -- had that result unioned onto a
class nothing could build. Both were the same gap. The table now holds 44 types: every node
type whose constructor takes one or two Entity children, less two binders. Comparisons,
connectives, the inverse trigonometric functions, floor/ceil/round, mod, gcd, min/max, the
set operations and Providedf all rebuild now, where before an expression rooted at any of
them came back unchanged reporting `Changed = false` -- indistinguishable from being
already at its cheapest.

What stays out is now a statement rather than an accident. Binders, because the e-graph has
no notion of a bound variable's scope and DirectChildren hands out a capture-avoidingly
renamed body, so rebuilding one would produce a term meaning something else. Variable-arity
nodes, because the table keys on an arity of one or two.

Six rules gain a reverse direction as a consequence -- the four inverse-trigonometric
round trips and the two set idempotences, whose left-hand pattern named a type that could
not be built. Each reversed rule is Expands, so none joins SafeRules and saturation is
unchanged. Two tests that used Modf as their example of an unbuildable node now use
Integralf, which is unbuildable for a reason that will not change: it carries an optional
range beside its two children.

Full suite: 8906 passed, 14 skipped (pre-existing), 0 failed.

* The last four recorded findings, and none of them needed the open design question

`RewriteRecording` could not see `EqualitySaturation` at all: it is populated inside
`RewriteRuleSet.ApplyOnce`, and saturation asks rules directly, so a caller who opened a
recording got a real rewrite with an empty derivation and nothing to distinguish
"introspection cannot see this" from "there was nothing to see". Now the pass is noted --
one edge, input to output, under the transformation's own name.

Deliberately not finer than the pass. A rule set records each firing because a firing there
is the rewrite: the node it matched leaves and the replacement takes its place. A firing in
saturation adds another member to an e-class whose members are all already believed equal,
and the answer is then chosen by Extract from all of them at once. Most firings contribute
nothing to what extraction picked, and none is a step on a route from input to output,
because there is no route. Reporting them as RewriteSteps would name rewrites that are not
in the answer.

`MatchPattern.RequiredRootType` was already there and never consulted, so every rule ran a
full pattern match against every class of every pass. A pattern requiring a root type cannot
match a class holding no node of it, and being a necessary condition is what makes it a
filter: it licenses skipping a rule, never firing one. Gathering each class's types once per
sweep and consulting them cuts match attempts about thirteenfold -- 1076 steps to 78 on the
largest of four expressions, 87 to 3 on `x + 0` -- with the same answer in every case.

`NeutralClass` hand-rolled an identity table that InnerSimplify already implements and
tests, with nothing keeping the two in step; the divergence would have been silent in the
worst direction, the e-graph merging two classes the rest of the library no longer believes
equal. It is derived now, by asking InnerSimplified whether `op(x, leaf)` really is `x`.
That settles the asymmetries without anyone having to remember them -- `0 - x` is a
negation, `1 / x` a reciprocal, `1 ^ x` the constant 1 -- and handles what a written table
cannot: an arm answering with a condition attached does not answer with the bare operand, so
no fold is claimed.

`Entity.SimplifiedRate` answered one cost model's question with another's cached number: the
cache is one slot per instance and the criteria is ambient, so the two do not agree about
what the cached number is a rate of. Not merely stale -- `Simplificator.PickSimplest`
compares candidates by this property, so it weighed one model's cached rate against
another's fresh one and chose on the strength of it. Cached now only while nobody has scoped
the setting, which is the `IsOverriden` test `BudgetLedger.For` already applies to the
budget, and one ambient read rather than a read plus a delegate comparison on a hot path.

Fourteen of the fifteen findings are now closed. What remains is a design question rather
than a defect -- how much should ride along on an e-node beyond its bare shape -- and the
notable thing is how little of the cluster actually depended on it: one finding, Codomain.
The Providedf case this document had offered as evidence for it was the buildable-type table
and nothing deeper.

Full suite: 8919 passed, 14 skipped (pre-existing), 0 failed.

* Drop a documented workaround for the rate cache, now that the cache is fixed

MathS.Settings.ComplexityCriteria's own example read its rate through
FromString(expr, useCache: false), to keep the parser from handing back an instance
whose SimplifiedRate had already been computed under the default criteria. That was
a workaround for the bug the previous commit fixed, and a doc teaching a workaround
for a bug that is gone is worse than no doc.

Measured both ways before changing it: with the cache left on, the example prints
the same 24 / 24 / 2 / 1 it prints with it defeated.

* Pay no allocation for the pre-filter, and say what it can miss

Two corrections to the root-type filter added a commit ago.

`held.Any(type => required.IsAssignableFrom(type))` captures `required`, so it
allocated a closure every time the exact-type test missed -- which is most rules of
most classes, since the filter's whole job is to miss. Paying an allocation to avoid
a pattern match is not a pre-filter. Written as a loop instead.

And the set is gathered before the class's sweep, so a union later in that same sweep
can add a type it does not have, and a rule can be skipped in the pass where it had
just become applicable. That costs nothing and is worth saying rather than leaving a
reader to work out: a union is exactly what sets `merged`, so there is another pass,
and the set is gathered again there.

Full suite: 8919 passed, 14 skipped (pre-existing), 0 failed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Rafael-SOWNet