Speed up proof encoding using egglog's :merge and unboxing pairs#933
Draft
oflatt wants to merge 23 commits into
Draft
Speed up proof encoding using egglog's :merge and unboxing pairs#933oflatt wants to merge 23 commits into
:merge and unboxing pairs#933oflatt wants to merge 23 commits into
Conversation
… foundation Constructor congruence as a functional-dependency view `:merge` instead of a separate congruence rule. - New primitives: begin, uf-set, select-eq (src/lib.rs). - Backend MergeFn::TableInsert (declares its table as a write-dep) and MergeFn::Seq, so a merge can write a table on the side safely during batched merges (egglog-bridge). - Block-form `:merge ((set ...) ... value)`: parser + `merge_action` AST field + typecheck (reuse typecheck_standalone_actions) + lowering to Seq/TableInsert. - Term-encoding mode: constructor view is now FD `(children) -> output`, with congruence handled by the view merge (no separate congruence rule). At baseline parity; normal mode unaffected. - Multi-value bridge foundation: FunctionConfig/FunctionInfo/SchemaMath carry `num_values`; column math generalized (behavior-preserving at num_values=1). Known WIP: proof-mode const-fold proofs (e.g. commute-collapse) still panic on the interim term_proof routing; to be replaced by the multi-value (output,proof) view once the bridge merge/lookup are generalized. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
ResolvedMergeFn::run now takes the old/new value-column slices instead of a single value; MergeFn gains OldCol(i)/NewCol(i) (Old/New == col 0) and a top-level Tuple(Vec<MergeFn>) that produces one value per column (each may read any column, so cross-column merges like the proof view's are expressible). to_callback writes each value column. Behavior-preserving at num_values==1 (18 egglog-bridge tests pass; test/example FunctionConfig literals updated). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Detect a Pair container output sort in declare_function and store the function with two value columns (its component sorts). At the rule lowering boundary (BackendRule), transparently box the two value columns back into a (pair ..) value on reads/lookups and unbox a pair value into the two columns on writes. Adds RuleBuilder::lookup_value_col for selecting a value column of a multi-value function. Behavior-preserving: no existing test uses Pair outputs, files suite unchanged (43 baseline proof-mode fails, no new regressions). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Re-encode proof-mode constructor views as functional dependencies (children) -> (output, proof), stored via the multi-value front-end as two value columns. The FD :merge now reads both colliding rows' proofs directly (oriented with select-eq) and builds Trans(p_large, Sym(p_small)) for the congruence union, replacing the stale term_proof-based proof routing that produced wrong proofs when an eclass held multiple distinct constructor terms (the const-fold/commute-collapse "expected Num, got Add" panic). Changes: - proof_encoding: view value = (Pair out proof) in proof mode; constructor_view_merge, update_view, query_view_and_get_proof, and the constructor case of instrument_fact_expr source the proof from the pair (pair-second) instead of term_proof. term_proof is kept only as an arbitrary per-eclass existence proof for bare eq-sort fact variables. - lib.rs: pair-aware merge lowering (Tuple of per-column MergeFns; old/new and pair-first/second map to OldCol/NewCol; (pair a b) -> Tuple). Fuse pair-first/pair-second of a pair-valued view result to a direct value column read (pre-scan records projections so fusion is order-independent), keeping the output an indexed column for fast rebuild canonicalization (rebuild_rule6: 14.5s -> 0.9s; rectangle --proofs 11s). - egglog-bridge: multi-value subsume (subsume_multi_value + lookup_value_col[_with_subsumed]); RuleBuilder::assert_eq_entries. - extract.rs / serialize.rs: a pair-valued view's extracted/serialized output is the first value column with the pair's first component sort. Results: files suite 733 passed / 0 failed (was 690/43); whole test suite green (one proof snapshot updated via INSTA_UPDATE after confirming program-run correctness); commute-collapse --proofs rc 0; rectangle --proofs ~11s. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds a term-free merge proof constructor `MergeFree (name p_old p_new)` and the corresponding RawProof::MergeFnFree, whose conclusion term is reconstructed during proof conversion from the two premise proofs plus running the merge function (mirroring the proof checker's MergeFn reconstruction). This is the enabler for the FD custom-function view merge, which runs without access to the children and so cannot embed the conclusion term. Not yet emitted by the encoding; the existing term-carrying Merge constructor is unchanged so all current proofs are unaffected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
MergeFnIdx(name, p_old, p_new, idx) carries a deterministic pre-order index identifying WHICH subexpression of f's merge body the proof is for, so nested merge-body subexpressions (which share the same premises p_old/p_new) become distinguishable. Reconstruction navigates to subexpression[idx] of the merge body and evaluates it on the premise outputs via the new run_merge_subexpr helper. Encoder does not emit MergeFnIdx yet, so behavior is unchanged (files 733/0). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Move custom (non-constructor) functions whose `:merge` body is a pure primitive call (min/max/or/set-union/vec-union/...) onto the SAME FD pair-valued view that constructors use: `(children) -> (pair output proof)`, keyed on children only. The user's primitive merge runs on the output column; the proof column carries a single-value `MergeIdx(name, p_old, p_new, 0)` justification (proof-datatype constructors are single-value, so no backend mint primitive is needed). No union: a custom function's output is a merged value, not an eclass collision. A single predicate `is_fd_pair_view(fdecl)` routes every site (view decl, delete/subsume, merge-or-congruence, rebuild, instrument_fact, update_view, query_view_and_get_proof, add_term_and_view, PrintSize, extract is_legacy_view). Custom is FD iff its merge body is all-primitive AND output is non-eq-sort AND inputs are non-eq-sort. Function/constructor-bodied merges, eq-sort outputs, eq-sort children, and no-merge customs stay on the legacy handle_merge_fn path (a hybrid end state). Saturation: the proof column uses `select-eq` to keep a premise's existing proof when the merged output equals that premise (the common min/max/or case), so the surviving pair is byte-identical and the merge does not re-fire forever; a fresh MergeIdx is minted only for a value distinct from both premises. Eq-sort children are excluded because rebuild canonicalization rewrites the per-row pair proof to a non-reflexive congruence proof, which the MergeFn checker (requiring reflexive premises) rejects. Also fixes a pre-existing query-lowering bug: `(= n (pair-first (f ...)))` followed by `(= n <literal>)` silently dropped the constraint for non-eq-sort pair projections (the fusion aliased the literal to the column). Now a literal projection result is constrained via assert_eq instead of aliased. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The single-parent union-find invariant (each source term has at most one parent) was maintained by a separate `single_parent` ruleset that joined two UF rows sharing a source. The UF function index `(UF_<sort>f source)` is already source-keyed and is the sole writer of its rows, so a key collision on the index is exactly the single-parent situation. Fold the union into the index's `:merge`: - The merge unions the two colliding parents by writing the edge `(UF (ordering-max b c) (ordering-min b c))` back into the UF table (via the existing block-merge `TableInsert` machinery) and keeps the smaller leader as the surviving index value. - Path compression (kept as a rule, since it chases a 2-row join) then removes the now-redundant `(UF a larger)` row, so the UF table converges to one parent per source. - In proof mode the index value is a `(Pair leader proof)`; the union proof is composed via `Trans`/`Sym` and oriented with `select-eq`. The surviving row keeps an existing premise proof verbatim, keeping the value stable so the merge saturates (no fresh proof minted each iteration). Removes the `single_parent` ruleset (rule, ruleset declaration, schedule saturate step, and the `single_parent_ruleset_name` field). Path compression and the (larger, smaller) UF table are unchanged. No backend mint primitive needed — uses only existing Trans/Sym (single-value proof constructors), TableInsert, and the pair-merge lowering. files suite 733/0; lib/extraction_proof_mode/terms green; clippy/fmt clean. Regenerated the two doc_example proof_tests snapshots (single_parent removed from schedule + the UF index merge now block-form; function2 also picks up the already-pending Phase A FD-view shape for `add`). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…hem) The `begin` and `uf-set` primitives were scaffolding for an earlier merge-side-effect design. The block-form `:merge` (Seq + TableInsert) replaced both: a `set` action names its table statically (exact write-dep) and the block sequences effects before the value. Neither primitive is emitted anywhere in the encoding. `select-eq` stays (load-bearing for FD-merge proof orientation + saturation). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Phase B foundation: a :merge can now mint a pair-valued constructor e-class and use it as a child of the merged value. TableAction:: lookup_or_insert_multi mints the first value column (FreshId) and writes the remaining value columns (e.g. the proof) from provided values, returning the minted output; idempotent on an existing key. MergeFn:: Construct(func, key_args, value_args) wires it through fill_deps (read+write the func table), resolve, and run. predict_val already supports arbitrary-length rows, so no core-relations change. Unused until the proof encoder emits it for function-bodied custom merges. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Phase B step 2. Adds MergeRow(name,p_old,p_new) proving the FD view row f(children)=eval(whole body); switches Phase A primitive-bodied FD emission to it. MergeIdx now indexes ALL body nodes (pre-order, incl the top node as a bare term) and always reconstructs the bare node term, dropping the idx==0==row special case. No behavior change (lib 38/0, files 733/0). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…roof linkage Recovers the function-bodied custom-merge FD encoder (fd-mint surface form, fd_mint_to_mergefn lowering, constructor-bodied FD view emitter) on top of the MergeRow/MergeIdx proof-format split. Root-cause fix for complex_merge_func_desugar_proof_testing: fd_mint_to_mergefn sourced the per-sort term-proof table from proof_state.proof_names.term_proof_name, which is only populated during on-the-fly proof instrumentation and is EMPTY when the resolved-to-string program is re-parsed in a fresh (non-instrumented) egraph. That made the fd-mint merge skip the (term_proof minted_output = proof) insert in the desugar-rerun, so the merged constructor terms (C1/C2/top-C2) had no @treeproof row, and the @prove_exists rule's `(= p (@treeproof out))` premise never matched -> prove-exists could not find the witness. Fix: source the term-proof table from proof_state.proof_func_parent, which is re-populated from each sort's `:internal-proof-func` annotation on every parse, so it survives the round-trip. Both maps name the identical table for any eq-sort (proof encoding sets `:internal-proof-func` = term_proof_name). Also drops the leftover no-op `dump_ctor_view_proof` debug test (it only eprintln'd, tripping clippy::disallowed-macros and adding a non-asserting lib test). complex-merge-func now passes in normal/term/proofs/proof_testing/desugar_proof_testing. lib 38/0, files 733/0, bridge 19/0, clippy + fmt clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…bodied) Manufacture the reflexive premise MergeFn needs from the rebuild-rewritten congruence proof via Trans(Sym(p), p) at resugaring time. This lets primitive-bodied custom functions with eq-sort INPUTS move onto the FD pair-view (e.g. merge-during-rebuild's distance: min over N N). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…GELOG Keep eq-sort-input constructor-bodied customs (e.g. rw-analysis const-prop) on the legacy handle_merge_fn path: the reflexivity wall is lifted by reflexivize_premise, but their merge mints constructor intermediates into FD views that persist as rows, diverging from normal-mode (print-size) and breaking the across-treatments snapshot. Primitive-bodied eq-sort-input customs (merge-during-rebuild) are on FD. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…column merge short-circuit A constructor-bodied custom :merge (e.g. rw-analysis const-prop's (merge-val old new)) mints constructor enodes. In a fixpoint analysis almost all collisions are no-ops (merged output == existing output), which normal egglog short-circuits via its cur == new check so it mints nothing. The FD view's value carries an extra proof column (proof mode) or runs a minting body (term mode), so an equal-output collision would still run the body and mint a spurious merge-val(out, out), diverging (print-size) from normal mode (0 vs 4 merge-val rows) and breaking the across-treatments snapshot. Fix: add FunctionConfig::identity_values: Option<usize> to egglog-bridge. When Some(k), a key collision whose leading k value columns are unchanged is a no-op merge: the existing row is kept verbatim and the merge body is NOT evaluated, so no side effects (mints/inserts) run. None (the default) preserves the classic behavior for ordinary functions. egglog declares every function with Some(1) so the output column alone determines merge identity (proof/term columns are passengers) — matching normal egglog's cur == new short-circuit. Then remove the eq-sort-input bail in is_constructor_bodied_fd_custom so const-prop routes to FD. rw-analysis now produces merge-val 0 in all modes (normal/term/proofs/proof-testing), matching the shared snapshot with NO snapshot change. The FD MergeRow/MergeIdx proof path is exercised end-to-end on const-prop's eq-sort inputs and verifies (rc 0). lib 38/0, files 733/0, bridge 20/0 (added a bridge test for the short-circuit). make nits clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…alues annotation
The Phase C-2 backend identity-column merge short-circuit
(FunctionConfig::identity_values) was wired in too broadly: declare_function
set identity_values: Some(1) for EVERY function, changing merge semantics for
user functions and making a user :merge <literal> (MergeFn::Const) latently
unsound (an equal-value collision would keep the old value instead of applying
the merge body).
Scope it via a new internal function annotation :identity-values <n>:
- New Option<usize> field on Command::Function / GenericFunctionDecl, parsed
in parse.rs and emitted by the function decl's Display so it round-trips
through the desugar resolve->string->re-parse harness.
- proof_encoding stamps :identity-values 1 onto every generated FD view
declaration (constructors AND FD custom views, term + proof modes).
- declare_function now reads decl.identity_values (None when absent) instead
of the universal Some(1) -- user functions keep classic merge semantics.
Added lib test test_user_merge_not_identity_short_circuited: a user
(function counter () i64 :merge (+ old 1)) re-set with an equal value still
increments (would fail under the old universal Some(1)). Kept the backend
identity_column_short_circuit bridge test.
Snapshots doc_example_add_function{1,2} updated: the FD view decls now carry
:identity-values 1 (the annotation is explicit in the generated encoding; no
behavior change). lib 39/0, files 733/0 (rw_analysis + merge_during_rebuild +
complex_merge_func pass in all 7 modes incl _desugar_proof_testing), bridge
20/0, make nits clean.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Trivial value-replacement custom merges with an eq-sort OUTPUT (`:merge old` / `:merge new` / `:merge <literal>` for a datatype output) now route onto the FD pair-valued view like every other proof-supported merge. `is_primitive_bodied_fd_custom` no longer bars an eq-sort output for a bare-var/literal body (a new `merge_body_is_trivial` predicate); such a merge just keeps one of the two colliding eq-sort outputs (no new term, no union), so it works through the existing FD machinery (custom_fd_view_merge / rebuild congruence / pair extraction). With this, every proof-supported custom merge is FD, so: - the non-FD branch in `handle_merge_or_congruence` is now `unreachable!` (function-reading merges -> FunctionLookupInAction; non-global :no-merge -> NoMergeOnNonGlobalFunction are rejected at file level); - `handle_merge_fn` is deleted entirely, along with the now-dead `Justification::Merge` variant and its match arms, and the unreachable legacy view-decl branch in `term_and_view`. Synthetic coverage: tests/merge-eq-sort-trivial.egg (`:merge old` and `:merge new` over an eq-sort datatype) runs in all treatments including proofs/proof_testing/desugar_proof_testing; verified that reverting the predicate makes it hit the new `unreachable!`. Added lib test `trivial_eq_sort_output_merge_is_fd`. lib 40/0, files 740/0, egglog-bridge 20/0, make nits clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
# Conflicts: # src/proofs/proof_tests.rs
…unreachable! gap) A custom function whose :merge READS a non-constructor function (e.g. `:merge (foo)`) is a live-DB read — merges are pure writes — so it is not FD-encodable and would reach the handle_merge_or_congruence unreachable!. command_supports_proof_encoding's action-lookup check uses visit_actions, which does not descend into a Function decl's merge body, so a proof- eligible function-reading merge slipped past it and PANICKED at the unreachable! instead of being cleanly rejected. Add an explicit check of the merge body (and block-merge actions) via expr_has_function_lookup (which flags only Custom, non-global calls, so constructor-/primitive-/ trivial-bodied merges are unaffected). Such programs now return a graceful UnsupportedProofCommand error. Surfaced by the origin/main merge audit; the bug predates the merge (handle_merge_fn-deletion commit). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #933 +/- ##
==========================================
- Coverage 86.54% 86.25% -0.29%
==========================================
Files 89 89
Lines 26804 28059 +1255
==========================================
+ Hits 23197 24202 +1005
- Misses 3607 3857 +250 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Merging this PR will improve performance by 12.59%
|
| Mode | Benchmark | BASE |
HEAD |
Efficiency | |
|---|---|---|---|---|---|
| ❌ | Simulation | tests[proof_testing_unify] |
14.9 ms | 18.5 ms | -19.3% |
| ❌ | Simulation | tests[proof_testing_typecheck] |
123.7 ms | 145.3 ms | -14.85% |
| ❌ | Simulation | tests[proof_testing_eqsat-basic-proof] |
23.4 ms | 26.4 ms | -11.4% |
| ❌ | Simulation | tests[proof_testing_eqsat-basic] |
23.4 ms | 26.4 ms | -11.24% |
| ❌ | Simulation | tests[taylor51] |
5.3 s | 5.6 s | -6.26% |
| ⚡ | Simulation | tests[proof_testing_math] |
59.3 s | 14.7 s | ×4 |
Tip
Investigate this regression by commenting @codspeedbot fix this regression on this PR, or directly use the CodSpeed MCP with your agent.
Comparing fd-proof-encoding (7f713c7) with main (7d102db)
Footnotes
-
219 benchmarks were skipped, so the baseline results were used instead. If they were deleted from the codebase, click here and archive them to remove them from the performance reports. ↩
A `:merge` must be a PURE WRITE: it may use old/new, call primitives, or mint constructor terms, but it must NOT read the live value of another (non-constructor) function -- such a read is untracked by seminaive rule execution. egglog previously let a merge READ a non-constructor function (e.g. `(function bar () i64 :merge (foo))` for a non-constructor `foo`): it silently TOOK EFFECT in normal mode and PANICKED at the proof encoder's `handle_merge_or_congruence` unreachable!. There was an analogous check for rule bodies (LookupInRuleDisallowed) but it never ran on merges. Add a dedicated `TypeError::LookupInMergeDisallowed(String, Span)` and check the merge value expression + every block-merge action in `resolve_function_decl` via the same predicate as the rule check (`expr_function_lookup`, which flags ONLY `ResolvedCall::Func` with subtype==Custom && !is_global). So constructor-bodied (`:merge (Ctor old new)`), primitive-bodied (`:merge (min old new)`), and trivial (`:merge old`) merges are NOT affected. This fires in ALL modes (normal/term/proofs) since plain typechecking runs before proof encoding. Revert the now-dead proof-only band-aid added to `command_supports_proof_encoding` (the typecheck error fires first, so a merge-read never reaches proof encoding) and update the `handle_merge_or_congruence` unreachable! comment to cite the new typecheck error as the guard. Relocate the now-correctly-rejected `tests/merge_read.egg` (foo a non-constructor `:no-merge` function, `bar :merge (foo)`) to `tests/fail-typecheck/merge_reads_function.egg`, asserting the error message; drop its obsolete shared snapshot (which documented the silent-accept bug) and remove it from the proof-unsupported file list. Rename the lib test `function_reading_merge_is_proof_unsupported` -> `function_reading_merge_is_rejected`, now asserting normal-mode `resolve_program` returns `LookupInMergeDisallowed`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…rites) A merge typechecks in Context::Write, so a Read/Full-context primitive has no Write entrypoint and is rejected by the context-id filtering. Locks in that behavior with the FullOnly (full-only) test primitive: using it in a :merge yields UnboundFunction. Complements LookupInMergeDisallowed (which rejects function LOOKUPS in merges) — together they enforce that merges cannot read the database. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Trim long, blow-by-blow comments to 1-2 line intent/invariant statements and remove ALL-CAPS emphasis words. Comments only; no behavior change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
oflatt
added a commit
to oflatt/egglog-duckdb
that referenced
this pull request
Jun 30, 2026
Port the non-proof half of egglog PR egraphs-good#933 to the FlowLog backend: replace the rule-encoded @congruence_rule* with an FD view keyed on children + a UnionId-style side-effecting merge that unions colliding outputs at FD-conflict time (drained at the iteration boundary). Behind a --native-merge flag (FlowLog-only, term mode, implies --native-uf); off by default with byte-identical rule encoding. Bit-exact to flowlog's rule encoding; agent-measured ~1.16x (1.28x with --fast-rebuild) faster than --native-uf on math-microbenchmark. Also fixes a pre-existing clone_boxed panic on --native-uf --flowlog/feldera. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
oflatt
added a commit
to oflatt/egglog-duckdb
that referenced
this pull request
Jun 30, 2026
…rt/Construct (bridge, term) Follow PR egraphs-good#933 to extend :merge with multiple actions, eliminating merge_rule for term-building custom :merge on the bridge (term mode). Port MergeFn::{Seq, TableInsert, Construct} to the shared egglog-backend-trait + bridge resolve/run/fill_deps (+ TableAction::lookup_or_insert_multi). Lower the desugared merge body to a Seq: nested constructors -> Construct, view writes -> TableInsert (respects the target view's own merge, so nested-view congruence resolves by construction), canon-at-creation -> Function(@UF_Sf) find-or-self. New native_term_build_views gate (mutually exclusive with value-fold); drops handle_merge_fn's 2 rules for these views. complex-merge-func bit-exact to the merge_rule oracle (merge_rule gone); nested-view congruence bit-exact; no regression (value-fold native, congruence unchanged, tuple_outputs 12/12). Proof mode deferred (needs MergeJustification through Construct value_args). Other backends keep merge_rule (inert arms). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
2 participants
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.
This PR: