Faster proof encoding: congruence via :merge + single self-referential UF (~1.8x)

[oflatt-claude]

Stacked on #3 (tuple-output functions) — review/merge that first. Until #3 merges the diff includes its commits; the encoding work here is the last 8 commits.

Brings the term/proof encoding much closer to egglog-duckdb's converged design, making proofs substantially faster. Two coordinated changes:

1. Congruence via native :merge instead of a generated self-join rule.
2. A single self-referential union-find per sort, replacing the two-table UF.

Result

Proofs on tests/math-microbenchmark.egg ((run 11), release):

version	wall clock	@rebuilding search
baseline (rule congruence, 2-table UF)	~43.3 s	13.7 s
+ congruence via :merge (2-table UF)	~36.7 s	9.6 s
+ single self-referential UF (this PR)	~23.7 s	3.8 s

≈1.83× faster than baseline. Output equivalent; full tests/files.rs suite 747/747 across all treatments (the proofs/proof_testing treatments run the proof checker, so proof validity is verified), proof unit tests pass, make nits clean.

How it works

• View congruence is a :merge. A constructor's view is the FD tuple (children) -> (eclass, proof); on an FD conflict its :merge orients max→min and stages the congruence edge (with a composed Trans/Sym proof) into the sort's UF. The @congruence_rule self-join is gone.
• One self-referential UF @UF : (S) -> (S, Proof) (native (values …), one table per sort). Union writes a single-key edge; the UF's own :merge keeps min and TableInserts the displaced edge back into itself, composing the transitivity proof. Single-parent is automatic (keyed by the node), so single_parent, uf_function_index, the @UF_Sf index, and the per-term self-loops are all dropped — only a proof-composing path_compress remains.
• Rebuild is fanned out to one rule per eq-sort column ((= (values leader proof) (@UF ci))). A canonical (root) column has no @UF row, so its rule doesn't fire — which is exactly what lets us drop the self-loops, the Pair index, and any default-on-miss lookup (nothing needs find(root) to hit).
• The encoding is self-contained: :internal-proof-names (ported from egglog #927) and :internal-uf re-register the proof constructors and the self-merge on a desugar re-parse.

Engine additions (small, general — reused everywhere)

• egglog-bridge: general merge-action MergeFn::{Seq, TableInsert, Construct, IfEq} + lookup_or_insert_multi (following egglog #933); peek_next_function_id + an add_table reorder so a :merge can name its own table.
• core-relations: pre-seed a merging table's own write-buffer (~16 lines) so a :merge can stage into its own table.

No DefaultVal::Identity, no backend-trait layer, no --native-uf, no dataflow backends.

🤖 Generated with Claude Code

Summary by CodeRabbit

• New Features

  • Added support for functions that return multiple values as tuples.
  • Added support for proof-related sort metadata and reserved keyword handling.

• Bug Fixes

  • Improved handling of values expressions across parsing, type checking, execution, and proof flows.
  • Fixed self-referential merge behavior and tuple-output merging.
  • Tightened validation for reserved names and tuple-output definitions.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: 96232a53-b8a4-46f7-8872-02e09b51e36b

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

📝 Walkthrough

Walkthrough

This PR adds tuple-output function support to egglog (multi-value columns, a values tuple constructor, per-column merges) spanning parsing, typechecking, core IR, and the egglog-bridge merge engine, and reworks proof-mode union-find/congruence encoding around a single self-referential native-merge table.

Changes

Tuple outputs and proof encoding rework

Layer / File(s)	Summary
AST/type contracts egglog/src/ast/mod.rs	Schema gains extra_outputs with tuple helpers; GenericNCommand/GenericCommand::Sort gain a proof_ctors field propagated through display/mapping.
Parser support egglog/src/ast/parse.rs	Reserved/command-only keyword enforcement, input/output call-head restriction, :internal-proof-names parsing, and tuple-output schema parsing via Schema::new_tuple.
Core IR values constructor egglog/src/core.rs, egglog/src/exec_state.rs, egglog/src/util.rs, egglog/src/proofs/proof_checker.rs, egglog/src/proofs/proof_extraction.rs, egglog-experimental/src/primitive.rs	Adds ResolvedCall::Values, HeadOps trait, multi-value Set, and rejects values in single-value/proof contexts.
Typechecking egglog/src/typechecking.rs, egglog/src/constraint.rs	FuncType.extra_outputs, typecheck_tuple_merge, new TypeError variants, and constraint generation for multi-output arity/groundedness.
Function declaration wiring egglog/src/lib.rs	ResolvedSchema.extra_outputs, per-column merge placeholders, native congruence/UF self-merge construction, and merge selection in declare_function.
egglog-bridge merge engine egglog/egglog-bridge/src/lib.rs, egglog/egglog-bridge/src/rule.rs, egglog/core-relations/src/free_join/mod.rs	SchemaMath reworked around n_keys; MergeFn/ResolvedMergeFn gain column and merge-action variants; lookup_or_insert_multi, subsume rewrite, and self-referential merge buffer seeding.
Proof encoding rework egglog/src/proofs/proof_encoding.rs, egglog/src/proofs/proof_encoding_helpers.rs, egglog/src/proofs/proof_encoding.md	Replaces two-table UF/rulesets with a native self-merge UF and FD tuple views, plus updated headers/rulesets and documentation.
Extraction and serialization egglog/src/extract.rs, egglog/src/serialize.rs	find_canonical supports two UF shapes; function_to_dag extracts all output columns; serialize splits rows by input arity.
Desugar/prelude/globals wiring egglog/src/ast/desugar.rs, egglog/src/prelude.rs, egglog/src/ast/remove_globals.rs, egglog/src/ast/proof_global_remover.rs, egglog-experimental/src/fresh_macro.rs	Generated Schema/Command literals set extra_outputs/proof_ctors.
Tests and changelog egglog/tests/tuple_outputs.rs, egglog/CHANGELOG.md	New integration tests and changelog entries for tuple outputs and reserved identifiers.

Estimated code review effort: 5 (Critical) | ~120 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Rule as EgglogRule
  participant TableAction as TableAction
  participant MergeFn as ResolvedMergeFn
  participant Table as UF Table

  Rule->>TableAction: insert/merge row for key
  TableAction->>MergeFn: run(cur, new, n_keys, self_col, ts)
  MergeFn->>Table: TableInsert/Construct staged write
  MergeFn-->>TableAction: merged value column
  TableAction->>Table: write_table_row

Loading

Suggested reviewers: oflatt

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main change: faster proof encoding via native congruence merge and a single self-referential UF.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[oflatt]

Got this run :

th: /Users/oflatt/egglog
╭──────────────────────────────────────────────── Outcome: 321393178b22 ────────────────────────────────────────────────╮
│ <2x proof gate        [19.387x, 20.951x]  <2x not established                                                         │
│ equal-file geom mean              4.982x  descriptive                                                                 │
╰──────────────────── Within-target proof overhead. This is separate from target-vs-baseline speed. ────────────────────╯
                                     321393178b22: per-file wall time                                     
                                                                                                          
  File                                    off                  term                 proofs                
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 
  egglog/tests/math-microbenchmark.egg    [0.4930s, 0.5161s]   [4.8234s, 4.9543s]   [10.2916s, 10.9804s]  
  egglog/tests/web-demo/rw-analysis.egg   [0.0115s, 0.0126s]   [0.0290s, 0.0296s]   [0.0372s, 0.0389s]    
  egglog/tests/integer_math.egg           [0.0081s, 0.0087s]   [0.0252s, 0.0258s]   [0.0312s, 0.0318s]    
  egglog/tests/web-demo/resolution.egg    [0.0067s, 0.0070s]   [0.0133s, 0.0147s]   [0.0164s, 0.0175s]    
                                                                                                          
Within-target wall-time estimates. These are not target-vs-baseline ratios.                               
                                   321393178b22: overhead ratios                                    
                                                                                                    
  File                                    term/off           proofs/off           proofs/term       
 ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ 
  egglog/tests/math-microbenchmark.egg    [9.438x, 9.951x]   [20.255x, 21.926x]   [2.100x, 2.252x]  
  egglog/tests/web-demo/rw-analysis.egg   [2.329x, 2.547x]   [3.009x, 3.319x]     [1.265x, 1.331x]  
  egglog/tests/integer_math.egg           [2.934x, 3.139x]   [3.631x, 3.876x]     [1.217x, 1.255x]  
  egglog/tests/web-demo/resolution.egg    [1.921x, 2.145x]   [2.367x, 2.570x]     [1.143x, 1.291x]  

[codspeed-hq]

Merging this PR will improve performance by 39.1%

⚡ 3 improved benchmarks

Performance Changes

	Benchmark	BASE	HEAD	Efficiency
⚡	files[resolution_proofs]	77 ms	52.6 ms	+46.42%
⚡	files[integer_math_proofs]	188.4 ms	131.2 ms	+43.62%
⚡	files[rw_analysis_proofs]	194.3 ms	151.8 ms	+28%

Tip

Curious why this is faster? Comment @codspeedbot explain why this is faster on this PR, or directly use the CodSpeed MCP with your agent.

---

_{Comparing oflatt-claude:port-native-merge (ab88652) with main (d9b4001)}

[oflatt]

@coderabbitai full review

[coderabbitai]

✅ Action performed

Full review finished.

[coderabbitai]

Actionable comments posted: 1

🧹 Nitpick comments (2)

egglog/tests/tuple_outputs.rs (1)

111-119: 🚀 Performance & Scalability | 🔵 Trivial

Consider adding relation/view-table tuple-output rejection tests.

CHANGELOG documents that tuple outputs are disallowed for constructors, relations, and view tables, but only the constructor case (constructor_tuple_output_rejected) is tested here. Adding parallel tests for relation and view-table declarations would close the coverage gap for the documented restriction.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog/tests/tuple_outputs.rs` around lines 111 - 119, Add test coverage for
the tuple-output restriction beyond constructor_tuple_output_rejected by adding
parallel rejection tests for relation and view-table declarations in
tuple_outputs.rs. Reuse the existing
EGraph::default().parse_and_run_program(None, ...) pattern and assert the same
TypeError::TupleOutputNotAllowed result for the relation and view-table symbols
so the documented restriction is covered consistently.

egglog/egglog-bridge/src/lib.rs (1)

548-559: 🗄️ Data Integrity & Integration | 🔵 Trivial | ⚡ Quick win

Consider a hard assert! for the reserved-table-id invariant.

The knot-tying relies on add_table_named assigning exactly the id returned by next_table_id(), and the merge callback is built against that reserved id. If this ever diverges (e.g. a future refactor adds a table between the reserve and the create), the self-referential merge would be wired to the wrong backing table and silently corrupt writes. Since debug_assert_eq! compiles out in release, the invariant is unchecked in production builds. A plain assert_eq! here is cheap insurance for a correctness-critical wiring step.

♻️ Proposed change

-        debug_assert_eq!(assigned_table_id, table_id);
+        assert_eq!(
+            assigned_table_id, table_id,
+            "reserved table id for self-referential merge diverged from assigned id"
+        );

Also applies to: 572-578

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@egglog/egglog-bridge/src/lib.rs` around lines 548 - 559, The
reserved-table-id check in the knot-tying flow is only a debug assertion, so the
invariant is unchecked in release builds. Update the
`add_table_named`/`FunctionInfo` wiring in `egglog-bridge/src/lib.rs` to use a
hard assertion (`assert_eq!`) for the `next_table_id()` versus created
function/table id match, including the same guarantee in the later
`add_table_named` merge setup referenced by the comment. This keeps the
self-referential merge callback bound to the reserved table id and prevents
silent miswiring if the ids ever diverge.

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@egglog/src/lib.rs`:
- Around line 1084-1090: The TSV input parsing for custom functions is still
using only func.schema.output, so tuple-output functions can be rejected or
built with the wrong row shape. Update the input type check and the row_schema
construction in input_file to use func.schema.outputs() instead of the single
output field, and make sure the row width matches the full backend schema
registered by the function config.

---

Nitpick comments:
In `@egglog/egglog-bridge/src/lib.rs`:
- Around line 548-559: The reserved-table-id check in the knot-tying flow is
only a debug assertion, so the invariant is unchecked in release builds. Update
the `add_table_named`/`FunctionInfo` wiring in `egglog-bridge/src/lib.rs` to use
a hard assertion (`assert_eq!`) for the `next_table_id()` versus created
function/table id match, including the same guarantee in the later
`add_table_named` merge setup referenced by the comment. This keeps the
self-referential merge callback bound to the reserved table id and prevents
silent miswiring if the ids ever diverge.

In `@egglog/tests/tuple_outputs.rs`:
- Around line 111-119: Add test coverage for the tuple-output restriction beyond
constructor_tuple_output_rejected by adding parallel rejection tests for
relation and view-table declarations in tuple_outputs.rs. Reuse the existing
EGraph::default().parse_and_run_program(None, ...) pattern and assert the same
TypeError::TupleOutputNotAllowed result for the relation and view-table symbols
so the documented restriction is covered consistently.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 929ef4c8-0ed1-46e4-b295-814acdee9c14

📥 Commits

Reviewing files that changed from the base of the PR and between d9b4001 and 61905dd.

⛔ Files ignored due to path filters (3)

• egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap is excluded by !**/*.snap
• egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap is excluded by !**/*.snap
• egglog/tests/snapshots/files__shared_snapshot_eqsat_basic_proof.snap is excluded by !**/*.snap

📒 Files selected for processing (26)

• egglog-experimental/src/fresh_macro.rs
• egglog-experimental/src/primitive.rs
• egglog/CHANGELOG.md
• egglog/core-relations/src/free_join/mod.rs
• egglog/egglog-bridge/src/lib.rs
• egglog/egglog-bridge/src/rule.rs
• egglog/src/ast/desugar.rs
• egglog/src/ast/mod.rs
• egglog/src/ast/parse.rs
• egglog/src/ast/proof_global_remover.rs
• egglog/src/ast/remove_globals.rs
• egglog/src/constraint.rs
• egglog/src/core.rs
• egglog/src/exec_state.rs
• egglog/src/extract.rs
• egglog/src/lib.rs
• egglog/src/prelude.rs
• egglog/src/proofs/proof_checker.rs
• egglog/src/proofs/proof_encoding.md
• egglog/src/proofs/proof_encoding.rs
• egglog/src/proofs/proof_encoding_helpers.rs
• egglog/src/proofs/proof_extraction.rs
• egglog/src/serialize.rs
• egglog/src/typechecking.rs
• egglog/src/util.rs
• egglog/tests/tuple_outputs.rs

[oflatt]

Pulled into #13