feat(opt): ægraph MVP — acyclic e-graph data structure (v1.0.3 Track 2)#122
Merged
Conversation
INFRASTRUCTURE ONLY. Lands the minimal Cranelift-style acyclic
equality-graph substrate so future PRs can grow a per-rewrite-verifiable
optimizer pipeline on top.
What ships:
- `loom-core/src/egraph.rs` (~430 non-test LOC, 180 LOC of tests)
- `Op` discriminator covering 14 i32 arithmetic / bitwise / comparison /
load-class opcodes (Const, Const64, LocalGet, I32{Add,Sub,Mul,And,Or,
Xor,Shl,ShrS,ShrU,Eq,Eqz}).
- `ENode { op, children: Vec<EClassId> }` with arity validation.
- `EGraph::add` performs hash-consing (structural sharing via
`HashMap<ENode, EClassId>`) and enforces the acyclic invariant —
every child id must be strictly less than the about-to-be-created
class id, which makes self-reference and forward edges syntactically
impossible.
- `ENode::from_instruction` / `EGraph::extract` round-trip helpers so
upstream callers can opt-in incrementally; unsupported ops return
`None` so callers cleanly fall back to existing pipeline.
- 30-LOC inline `UnionFind` (no external `union-find` crate) wired so a
future rewrite engine can add `union()` without API churn.
Out of scope (deferred to v1.0.4+):
- Rewrite engine / `union()` API.
- Wider op coverage (i64, conversions, memory ops).
- Real cost model.
- Integration with the canonicalize / `simplify_with_env` pipeline.
Tests: 7 unit tests, all pass under `cargo test --release egraph`:
- hash-cons const, hash-cons arith tree, distinct nodes get distinct ids
(commutativity NOT normalized — that's rewrite-engine work)
- extract round-trips through `encode::encode_wasm` and produces a valid
wasm module header
- acyclic invariant: forging a self-referential child id is rejected
- `from_instruction` returns None for unsupported ops and wrong arity
- supported ops convert correctly when given the right children
Soundness gotchas surfaced while building this:
- Commutativity is NOT normalized in the MVP. `add(1,2)` and `add(2,1)`
hash-cons to different e-classes. Any future rewrite rule that wants
to unify them must do so through `union()` (not yet implemented) and
carry its proof obligation.
- Identity-element rewrites (x+0 == x, x*1 == x, x&-1 == x, etc.) are
also rewrite-engine work, not substrate work. The MVP intentionally
ships zero rewrites so the substrate can be reviewed in isolation.
- The acyclic guard is "child id < new id" — this is the structural
reason ægraphs are easier to verify than full e-graphs: there is no
congruence-closure fixpoint that can re-introduce cycles.
Implements: track2/egraph-mvp
Refs: docs/research/v0.7.0/optimization-methods-survey.md
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 17, 2026
…ap) (#124) Five-track sprint. Three landed via agents in worktrees, one direct-work, one deferred when its agent died. Merged: #120 Track 4: close SG-3..6 lifecycle gaps #121 Track 1 (PR-Q): real corpus fixtures (3rd attempt — success) #122 Track 2: ægraph MVP (acyclic e-graph substrate) #123 Track 5: issue triage + roadmap doc Issues closed via the roadmap: #45 Rocq foundation (already shipped) #47 StackSignature::compose associativity (proven) #50 Crocus-style ISLE verification (already in verify_rules.rs) #75 P3 async callback trampolines (duplicate of #70) Deferred to v1.0.4: Track 3: verifier table-resolver teaching (agent died) ægraph rewrite engine + per-rule proofs KEEP issues #48 #68 #70 #71 Lifecycle gaps: 4 → 0 (track 4 closed all remaining).
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.
Cranelift-style acyclic ægraph substrate per docs/research/v0.7.0/optimization-methods-survey.md. STRICTLY MVP — data structure + hash-consing + acyclic invariant + extraction + 7 tests. No pipeline integration; no rewrite engine; no union() yet. Future PRs add the rewrite layer with per-rule proofs.
432 LOC (excluding tests), 7 tests pass.
🤖 Generated with Claude Code