feat(opt): ægraph pipeline integration (v1.0.5 Track 1) + #48 prep survey (Track 4)#130
Merged
Merged
Conversation
…rvey (Track 4) ## Track 1: ægraph pipeline integration New `pub fn egraph_optimize(module: &mut Module) -> Result<()>` in the optimize module. Feeds each function's straight-line maximal (0→1)-net-stack-effect expression trees through the v1.0.4 Track C ægraph engine, saturates with the 3 identity rules, and extracts the smaller form when one exists. ### Tree builder `try_build_egraph_tree(instructions, start)` greedily walks consecutive instructions, building the e-graph by stack simulation: each egraph-supported op pops its operands and pushes its result. Bails on control flow / unsupported ops / stack underflow. Returns a tree iff the final symbolic stack has exactly 1 entry (a (0→1)-net-effect expression). ### Extraction workaround The v1.0.4 substrate's `extract()` always emits the node originally stored at the requested class id, ignoring union-find merges. To get the smaller representative after a rule fire, the pipeline pass scans all class ids in the same union-find root and picks the shortest extraction. A v1.0.6 follow-up should move this into `egraph::extract()` as proper cost-driven extraction. ### CLI wiring New CLI pass `egraph`. Opt-in via `--passes egraph,…` (NOT included in the default pipeline yet — the candidate set is tiny and v1.0.6 will widen op coverage before flipping the default). ### Tests (4 new) - test_egraph_optimize_folds_x_plus_zero: positive (x+0 → x). - test_egraph_optimize_no_op_on_plain_function: non-identity function is byte-for-byte unchanged. - test_egraph_optimize_skips_across_call: a Call breaks the tree, but the post-call identity tree still folds. - test_egraph_optimize_recurses_into_blocks: block-nested identity must fold. All 4 pass. ## Track 4: #48 prep survey New doc docs/research/v1.0.5/rocq-roundtrip-prep.md (~700 words). Surveys the proofs/ tree's Admitted state (4 remaining: 3 in placeholder files Roundtrip.v / TermBijection.v / StackSignature.v, 1 in the real partial-composition lemma). Recommends Path A for v1.1.0 (close #48 properly, ~1400 LOC Rocq + 150 LOC Rust subset extraction) or Path B for v1.0.5 cleanup (signal-noise reduction). Trace: REQ-1, REQ-3, REQ-7, REQ-14
Merged
avrabe
added a commit
that referenced
this pull request
May 19, 2026
…#68 fused + Rocq prep) (#133) Four v1.0.4 infrastructure pieces grew real consumers: #130 Track 1+4 ægraph pipeline integration + Rocq Roundtrip prep doc #131 Track 2 #70 six-pass chain composition + task.return shim peephole #132 Track 3 #68 Tier-1.1 scalar adapter inlining + Tier-2.2 body dedup +18 tests, 400+ total. Code-section bytes unchanged on the current corpus — Track 3 agent flagged 4 pre-existing observations worth tracking for v1.0.6+.
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.
Combined: egraph_optimize pass (opt-in) + 4 tests + rocq-roundtrip-prep.md.
🤖 Generated with Claude Code