Close twelve of the thirteen recorded e-graph review findings

[Rafael-SOWNet]

The code review on #1101/#1102 found fifteen issues and fixed two, recording the other thirteen in EqualitySaturationReviewFindings.md rather than fixing them. This closes twelve of the thirteen. What is left is a design question rather than a defect, and the interesting result is how little of the cluster depended on it.

Three commits, each independently reviewable.

Correctness in Extract

• A CostModel answering NaN corrupted every later comparison. here >= bestCost is false whenever either side is NaN, so a NaN 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 was already declined by the surrounding catch; one answering NaN is saying the same thing.
• Cost ties were settled by HashSet<ENode> enumeration order — 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.
• No depth cap. The 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. Capped at 256, declining to build — the answer the cycle case already gives, and the shape Gruntz.MaxDepth already uses.

And one the review diagnosed wrongly. WorkBudget.Steps was recorded as a timing defect: the growth charge landing after a sweep rather than before the next one. Measuring it found otherwise — 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.

One table of buildable node types

EGraph kept a second copy of the fourteen-type list MatchPattern.Construct hardcodes, next to a doc comment on Construct warning that a list written twice is a list that drifts. One table now holds the type, its arity and the constructor call together, with the list, the name lookup and CanConstruct all derived from its keys. Being a table rather than a chain of nodeType == typeof(T) tests also makes it O(1).

Fourteen types was what Construct had accumulated, not a boundary anyone chose — so Extract silently no-opped on any root outside it, and a rule wrapping a conditional result in Providedf (the registry's own convention) had that result unioned onto a class nothing could build. The table now holds 44: every node type whose constructor takes one or two Entity children, less two binders.

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. 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.

Introspection, a filter, a derived table, a cache

• RewriteRecording could not see EqualitySaturation at all, so a caller who opened a recording got a real rewrite with an empty derivation and no way to tell that introspection had missed it. The pass is noted now — and deliberately not finer, because a firing in saturation is not a rewrite: it adds a member to an e-class whose members are already believed equal, and most firings contribute nothing to what extraction chose. Reporting them as RewriteSteps would name rewrites that are not in the answer.
• MatchPattern.RequiredRootType was never consulted, so every rule ran a full pattern match against every class of every pass. Consulting it cuts match attempts about thirteenfold — 1076 steps to 78 on the largest of four expressions — with the same answer in every case.
• NeutralClass hand-rolled an identity table InnerSimplify already implements, with nothing keeping them in step; the divergence would have been silent in the worst direction. It is derived now, by asking InnerSimplified whether op(x, leaf) really is x — which settles 0 - x, 1 / x and 1 ^ x without anyone having to remember them, and declines a fold whose answer carries a condition.
• Entity.SimplifiedRate answered one cost model's question with another's cached number. Not merely stale: Simplificator.PickSimplest compares candidates by this property, so it weighed a cached rate against a fresh one and chose on the strength of it.

What is left

One entry, and it is a decision rather than a bug: how much should ride along on an e-node beyond its bare shape. Only Codomain turned out to depend on it. The Providedf case the findings document had offered as evidence that the e-graph could not represent a conditional equivalence was the buildable-type table and nothing deeper — a cluster of findings around one subsystem invites a single grand explanation, and thirteen of these fourteen did not have one.

Verification

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

Every fix has a regression test, named beside its entry in the findings document. 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.

Part of #746 tier 2.