feat(opt): ægraph rewrite engine + 3 identity rules (v1.0.4 Track C)#127
Merged
Conversation
Builds on the v1.0.3 acyclic e-graph substrate. Wires the previously
dormant inline union-find through a public API and adds a
rule-driven rewrite engine plus congruence-closure rebuild.
What lands:
- EGraph::union(a, b) -> bool: substrate primitive. Drives the inline
UnionFind (path compression + union-by-rank, O(α(N)) amortized).
- EGraph::rebuild(): congruence-closure fixpoint. After a batch of
unions, propagates equality through equal-op equal-children parents
until no further merges are possible.
- Pattern enum (Wild / Node) for both LHS and RHS of rewrite rules.
Linear matching: repeated occurrences of the same wildcard must
bind to the same union-find root.
- Rule struct + EGraph::apply_rules / saturate_with_rules.
- identity_rules(): three hand-proven i32 identities, each with its
one-line algebraic proof at the construction site:
1. x + 0 == x (additive identity in Z/2^32)
2. x * 1 == x (multiplicative identity in Z/2^32)
3. x & -1 == x (bitwise-AND all-ones identity)
Each identity is the e-graph analog of the corresponding rewrite in
crate::peephole_synth (proven there). The proof obligation is
unchanged; this PR just adds a second carrier for the same rule.
Tests (all pass):
- test_egraph_union_propagates_via_congruence: classic f(a) ≟ f(b)
given a ≟ b scenario.
- test_rule_x_plus_zero_fires, test_rule_x_times_one_fires,
test_rule_x_and_negone_fires.
- test_rules_dont_overfire: Add(x, 1) must NOT match the x+0 rule.
- test_saturation_terminates: nested ((((x * 1) + 0) & -1) saturates
to x's class in a bounded number of iterations, second saturation
is a no-op (fixpoint witness).
- test_rule_no_match_is_noop: no spurious class allocation.
NOT in scope (deferred to v1.0.5+):
- Pipeline integration (the rewrite engine is still a library, not
a pass yet).
- A real rewrite-time cost model (extraction still walks the unique
stored representative per class).
- Commutativity normalization (rules must match exact arg order).
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 18, 2026
Four-track parallel sprint with FULL success (vs v1.0.3 where Track 3 died): #125 Track A async-callback adapter pass (#70 first piece) #126 Track B verifier table-resolver teaching (drops directize Z3 bypass) #127 Track C ægraph rewrite engine + 3 identity rules #128 Track D island-model parallel optimization (#71) Plus a subagent new-issues sweep that found zero issues since v1.0.3. +20 tests, 380+ total. Code-section bytes unchanged on the current corpus — all four tracks ship infrastructure that will produce measurable wins once their consumers land in v1.0.5+.
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
1 participant
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.
Builds on v1.0.3 substrate. Adds union() + congruence-closure rebuild(), Pattern/Rule API, apply_rules + saturate_with_rules, and 3 hand-proven identity rules: x+0=x, x*1=x, x&(-1)=x. 7 new tests (14 total egraph tests pass).
Still library-only — no pipeline integration. v1.0.5 next.
🤖 Generated with Claude Code