Hash-cons term and proof tables instead of minting with get-fresh! by oflatt-claude · Pull Request #36 · saulshanabrook/egglog-encoding

oflatt-claude · 2026-07-27T14:53:24Z

Replaces the term/proof encoding's get-fresh! minting with hash-consing, so building the
same term twice reuses one node instead of piling up duplicate copies.

The problem

Every term/proof/AST/ProofList node was built by minting a fresh id and unconditionally
asserting a row into a Unit-valued relation keyed on (children, id):

(let v (get-fresh! "Math"))
(set (Add a b v) ())

Because the id was minted fresh each time, every rebuild of the same term produced another
copy, and the proof encoding accumulated large numbers of structurally identical nodes.

The change

Each node table becomes a children-keyed function whose output is the interned id, built
with the existing set-if-empty primitive:

(function Add (Math Math) Math
  :merge ((set (@AuxUF_Math (ordering-max old new)) (ordering-min old new))
          (ordering-min old new))
  :internal-hidden :internal-term-node :internal-identity-vals 1)

(let cand (get-fresh! "Math"))
(let v (set-if-empty-Add! a b cand))

set-if-empty returns the already-interned id on a hit, so identical terms share one node and
the candidate is discarded.

Because set-if-empty only sees the previous iteration's committed rows, two rules that build
the same term within one iteration each insert a distinct candidate. The key then collides at
merge time and the table's :merge records loser -> winner in a new per-sort auxiliary
union-find @AuxUF_<Sort>, kept separate from the encoding's real @UF_<Sort> so it never
mixes with genuine unions. Proof extraction consults AuxUF to resolve an aliased id back to the
surviving, structurally identical node.

This applies uniformly to term tables and to the proof-format node tables (@Fiat, @Rule,
@Trans, @Sym, @Congr, @PCons, the Ast* constructors, …). Interning works uniformly inside :merge bodies too. That needs care, because merges run a whole
stratum at once with every table in it taken out of the database, so set-if-empty's read would
fail if its target shared the stratum. External functions were invisible to the dependency graph,
so set-if-empty now declares a read dependency on its target
(declare_external_func_table_deps), and MergeFn::Primitive's fill_deps contributes it. The
graph places a reader strictly above what it reads, so the target merges in an earlier stratum and
is back in the database when the reader's merge runs.

Read dependencies must stay acyclic. For this encoding they are: a :merge body can only build
constructor applications and call primitives, and a custom-function lookup in an action is
rejected up front, which rules out two custom functions interning into each other's merges. The
resulting strata are node tables and AuxUF at level 0, @UF_<Sort> and congruence views at
level 1, and custom-function views at level 2.

Commits

Hash-cons term tables via set-if-empty + AuxUF (term mode)
Hash-cons proof/AST/ProofList tables; AuxUF for the proof sorts
Restore AuxUF on re-parse via a :internal-aux-uf sort annotation
Untrack and gitignore insta .snap.new reject artifacts
Seed a hash-consed view with the natural node, fixing proof-mode drift

On commit 5

Worth calling out, since it was the subtle one. add_constructor_with_proof used to intern two
nodes per constructor — fv_nat (as-built children) and fv_can (deduped children). Once
children are hash-consed those two children-lists usually coincide, so both set-if-empty calls
hit the same key; within one iteration neither sees the other's uncommitted row, so both mint
candidates, the :merge keeps ordering-min (fv_nat), and the other is aliased into AuxUF
— but the view had been seeded with fv_can, the loser. That id has no term row, so extraction
fell through to the real union-find, whose leader is a differently-shaped term, and the pinned
natural form silently changed (e.g. (Mul (Num 2) (Num 3)) became (Num 6)), producing
congruence failures downstream.

The fix interns only fv_nat, seeds the view with it, and stores the Congr-chain proof
fv_nat = f(deduped children) as the row proof; fv_can/can_prf are gone. Proof extraction
now resolves a missing row through AuxUF (a structural alias) before the real union-find,
whose leader may be a differently-shaped term.

Testing

Whole workspace green. cargo test --release --test files: 783 passed / 0 failed;
cargo test --release --lib: 68 passed / 0 failed; cargo fmt --all --check clean.

Proof-mode tests run with verify_proofs enabled, so every passing proof test is checked by the
proof checker rather than only snapshot-compared. Snapshots updated where the change is fresh-var
renumbering or the expected structural difference from dropping the reflexive can_prf step.

Native rebuild is now provably dead under the encoding

The encoding removes every union and declares no constructor, so nothing it lowers can stage a
union in the backend's own union-find — all equality reasoning runs as ordinary encoded rules
over @UF_<Sort> tables. That was previously implicit; it is now measured and enforced.

Measured with temporary counters (since removed), single-threaded:

Run	encoded `run_rules`	UF growth	`rebuild()` entries	unions staged	tables w/ `UnionId`/`FreshId`
`--test files -- term_encoding` (107)	37,318	0	0	0	0
`--test files -- proofs/` (100)	75,110	0	0	0	0
`--test files` (all 783)	112,292	0	0	0	0
`--lib` (68)	3,494	0	0	0	0

The counters were not vacuous: in the same full-suite process, unencoded e-graphs performed
3,692 rebuilds, 1,632,172 MergeFn::UnionId merges, 1,414 container-merge unions and 2,318
rule-level unions. Notably containers are included — the backend's container rebuild is reached
only from rebuild(), so container canonicalization is done exclusively by the encoding's own
primitives.

Enforced by Backend::forbid_native_rebuild() (default no-op), called from
enable_term_encoding, with a release-checked assert in the bridge's rebuild() and tests in
tests/no_native_rebuild.rs. The guard was verified non-vacuous by deliberately tripping it.

Performance

bench.py --target . --compare-target @853fbfd --treatment proofs --compare-treatment proofs,
6 rounds per endpoint/file, baseline = the main this branch merges (853fbfd). Ratios are
candidate / baseline.

Wall time — roughly neutral overall.

File	Baseline	Candidate	Ratio	Result
math-microbenchmark.egg	9.69–9.78 s	10.3–10.4 s	1.06–1.07x	slower
eggcc-2mm-pass1.egg	13.0 s	13.0–13.1 s	0.998–1.01x	CI includes 1
pointer-analysis-small.egg	66.5–81.2 ms	66.5–82.0 ms	0.870–1.16x	CI includes 1
hardboiled_conv1d_32.egg	1.43–1.45 s	1.39–1.41 s	0.961–0.981x	faster
luminal-llama.egg	8.60–8.64 s	8.24–8.33 s	0.955–0.967x	faster
herbie.egg	969–993 ms	1.02–1.05 s	1.04–1.07x	slower

Suite total: 1.01x — within noise of neutral. Two benchmarks get slightly slower
(math-microbenchmark, herbie ~5%), two get slightly faster (luminal-llama, conv1d ~3-4%), two are
indistinguishable.

Peak RSS — lower on 5 of 6, higher on none.

File	Baseline	Candidate	Ratio	Result
math-microbenchmark.egg	2.2 GiB	1.6 GiB	0.725–0.727x	lower
eggcc-2mm-pass1.egg	988.5 MiB	722.3 MiB	0.730–0.736x	lower
hardboiled_conv1d_32.egg	200.6 MiB	160.1 MiB	0.795–0.799x	lower
herbie.egg	125.4 MiB	107.5 MiB	0.853–0.859x	lower
luminal-llama.egg	745.7 MiB	674.5 MiB	0.904–0.906x	lower
pointer-analysis-small.egg	106.0 MiB	106.0 MiB	1.00x	CI includes 1

So the duplicate-term elimination shows up as a consistent memory win — up to a 27% cut in peak
RSS — at roughly break-even wall time.

Rebuild is 0 ns in both baseline and candidate on every benchmark, independently corroborating
the section above.

Measuring against this branch's original base (e6feb75) instead would report a misleading
1.19–1.21x slowdown. That is an artifact of the stale baseline: main itself improved these
workloads substantially in the interim (luminal-llama 36.9 s -> 8.6 s, math-microbenchmark
16.1 s -> 9.7 s), and the CSE prepass added there already removes many of the duplicate terms
this change also targets. Against current main, the two compose without the regression.

Cost of uniform interning

Declaring the read dependencies costs some merge parallelism, since a read-dependent table can no
longer merge in the same stratum as what it reads. Measured against the same branch with the
merge-body fallback still in place: suite wall time 0.976–1.03x (CI includes 1) and peak RSS
within ±2%, with the effect confined to the Merge phase (largest +92 ms on eggcc-2mm-pass1,
about +10% of that phase, ~1-2% of the file's wall time). It does not surface in total wall time.

Summary by CodeRabbit

New Features
- Improved term/proof encoding with auxiliary union-find tracking for more reliable canonicalization and extraction.
- Added a mode to forbid backend native rebuilds in encoded equality modes.
- Externally-registered functions can declare table read/write dependencies that influence merge planning.
Bug Fixes
- Fixed canonicalization and extraction behavior, including same-iteration set-if-empty collisions and relation-term handling.
- Corrected encoded term/proof table wiring and reconstruction.
Documentation
- Updated proof-encoding docs to reflect the auxiliary UF and revised workflows.
Tests
- Added native-rebuild prevention tests for term-encoding and proof modes.

Replace the term encoding's get-fresh! term relations (which mint a fresh id per build, piling up duplicate term copies) with children-keyed functions built via set-if-empty, so identical terms dedup to one row. The term table's :merge records same-iteration collisions (new -> old) in a new per-sort auxiliary union-find AuxUF, separate from the normal UF, so proof extraction can recover that two ids denote the same term. The id moves from the last-input column to the output column; extraction and native_input are updated accordingly. Term/plain/desugar modes all pass; proof mode (proof-table hash-consing) is next. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…f sorts Extend the term-table hash-consing to the proof-format node tables (Fiat, Rule, Trans, Sym, Congr, PCons, AST constructors, ...): each becomes children-keyed with the id in its output column, built via set-if-empty, with a per-sort AuxUF merge. Node interning inside :merge bodies (UF/view congruence, custom-function view merge) falls back to get-fresh!+set since set-if-empty's table read is unavailable there; the AuxUF merge folds the resulting duplicates away. Extraction's find_canonical now also chases AuxUF so an aliased id resolves to its surviving structurally-identical node. Non-proof modes fully green (677 pass). Proof mode: 96/202 proof tests pass (from 0); remaining failures are proof-threading interactions with hash-consing the natural/canonical constructor nodes (WIP). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

find_canonical resolves a hash-consed id that lost a same-iteration set-if-empty collision through proof_state.aux_uf_parent, but that map was only populated during encoding, so a re-parsed/desugared encoded program couldn't resolve aliased ids and proof extraction failed. Add an :internal-aux-uf annotation on sort declarations (mirroring :internal-uf / :internal-proof-func) recording each sort's AuxUF table, and repopulate aux_uf_parent when the sort is (re-)declared. Proof tests: 152/202 pass (from 96). Non-proof modes remain fully green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

These pending-snapshot artifacts were swept into an earlier commit by git add -A. They are regenerated on every test run, so ignore them instead of tracking.

With hash-consed term tables, `add_constructor_with_proof` interned two nodes per constructor: `fv_nat` at the as-built children and `fv_can` at the deduped children. Whenever the two children lists coincide at runtime (the common case, since a child's natural id equals its deduped id as soon as the child term already exists), both `set-if-empty` calls hit the same key. In one iteration both miss the committed table and mint distinct candidate ids: the term table's `:merge` keeps the smaller while the view was seeded with `fv_can`, the other one. The view's e-class then had no term-table row, so extracting it fell through `find_canonical` to the real union-find and produced a differently-shaped term — the natural form was no longer pinned to what the rule head built. Proof checking then rejected `Congr` steps whose base child and child-proof LHS had drifted apart (`congruence error - child proof lhs ... doesn't match base term child`), and `extract` could fail outright when the view's e-class resolved to a term id with no view row of its own. Intern only the natural node and seed the view with it, storing the `Congr`-chain proof `fv_nat = f(deduped children)` as the row proof. This keeps the invariant that a view row's proof has RHS `f(<row key columns>)` while guaranteeing the row's e-class is a node the term table knows. Also: - Proof extraction now resolves a missing row through `AuxUF` (the structural alias recorded when two same-iteration inserts collide) before the real union-find, whose leader may be a differently-shaped term. - `native_input` builds the `<Sort>Ast`/`@Fiat` rows in the hash-consed shape (children key, id in the output column) instead of the old id-as-last-input relation shape, and interns `ast(fv)` once. - Update the rule-name hoisting test, which matched the old `(set (@rule ... id) ())` action rather than the interning `let`. - Accept the pending proof snapshots (the emitted proof shape and fresh-var numbering change; every proof is still verified by the checker) and drop the `.snap.new` files that were left tracked. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

coderabbitai · 2026-07-27T14:53:32Z

Warning

Review limit reached

@oflatt-claude, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 46 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 0b4374b4-2802-4e10-9853-8c4ca14d847a

📥 Commits

Reviewing files that changed from the base of the PR and between 1e391a3 and 93fb4cb.

📒 Files selected for processing (8)

egglog/egglog-bridge/src/lib.rs
egglog/src/ast/mod.rs
egglog/src/extract.rs
egglog/src/lib.rs
egglog/src/proofs/proof_encoding.md
egglog/src/proofs/proof_encoding.rs
egglog/src/proofs/proof_encoding_helpers.rs
egglog/src/typechecking.rs

📝 Walkthrough

Walkthrough

The PR adds auxiliary union-find metadata to sort commands, refactors proof instrumentation around merge-aware hash-consing, tracks external-function table dependencies, updates extraction and encoded input handling, and prevents native backend rebuilds when term or proof encoding resolves equality itself.

Changes

Term encoding and proof extraction

Layer / File(s)	Summary
Auxiliary UF sort metadata `egglog/src/ast/*`, `egglog/src/prelude.rs`, `egglog/src/typechecking.rs`, `egglog/src/lib.rs`	Adds optional `:internal-aux-uf` sort metadata and preserves it through parsing, desugaring, symbol mapping, typechecking, and command replay.
Merge-aware proof generation `egglog/src/proofs/proof_encoding*`, `egglog/src/proofs/proof_fresh.rs`, `egglog/src/proofs/proof_encoding_helpers.rs`	Introduces auxiliary UF declarations, hash-consed term/view rows, in-place statement generation, revised constructor proof wiring, and updated proof headers and rebuild rules.
External function dependency propagation `egglog/egglog-bridge/src/lib.rs`, `egglog/core-relations/src/dependency_graph.rs`, `egglog/CHANGELOG.md`	Adds declared table read/write dependencies for external functions and incorporates them into merge dependency stratification.
Extraction and encoded input integration `egglog/src/extract.rs`, `egglog/src/proofs/proof_extractor.rs`, `egglog/src/lib.rs`, `egglog/src/proofs/proof_tests.rs`	Adds auxiliary canonicalization during extraction, changes internal-term-node position handling, updates encoded table loading, and adjusts proof instrumentation tests.
Native rebuild prohibition `egglog/egglog-backend-trait/*`, `egglog/egglog-bridge/src/lib.rs`, `egglog/src/lib.rs`, `egglog/tests/no_native_rebuild.rs`	Adds a backend capability that sets a bridge-level prohibition and asserts if native rebuilding is attempted; term-encoding and proof-mode workloads exercise the guard.

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

Sequence Diagram(s)

sequenceDiagram
  participant TermEncoding
  participant EGraph
  participant Backend
  participant ProofExtractor
  TermEncoding->>EGraph: enable term or proof encoding
  EGraph->>Backend: forbid_native_rebuild()
  TermEncoding->>EGraph: declare auxiliary UF and hash-consed tables
  EGraph->>ProofExtractor: provide encoded term and UF state
  ProofExtractor->>EGraph: resolve auxiliary canonical representative

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 accurately captures the main change: replacing get-fresh! minting with hash-consing for term and proof tables.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.
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

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

The encoding removes every `union` and declares every table as a plain function, so nothing it lowers stages a union in the backend's own union-find and the backend's native rebuilding (tables and containers) never runs. Measured across the whole test suite: encoded e-graphs make 112k `run_rules` calls with zero union-find growth and zero `rebuild` entries, while unencoded ones rebuild 3692 times. Make that a checked invariant: `Backend::forbid_native_rebuild` lets the frontend declare that it resolves equality itself, and the bridge backend turns a violation into a panic in `rebuild` rather than a silent divergence between the encoded and native notions of equality. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Upstream added a CSE prepass (`ast::cse`), `begin` blocks / `CoreActions`, and the construct-into optimization for `union` operands in proof mode. The only real conflict was `proofs/proof_encoding.rs`. Resolution: - Kept upstream's `build_natural_with_congr` helper (which mints only the natural node, so it already hash-conses via `mint`/`hash_cons`) and re-applied this branch's semantics in `add_constructor_with_proof`: the second `fv_can` node at the deduped children is gone, and the view is seeded with `(fv_nat, nat_to_dedup_term)`. This preserves the invariant from 55e83bc — exactly one interned node per constructor, and the view row's proof has RHS `f(<row key columns>)`. - `instrument_construct_into` (new upstream path) already obeys that invariant in proof mode: it interns only `fv_nat` and writes the view value `target` with the proof `target = f(dedup_args)`. Its term-only branch needed the hash-consing shape change: the term table is now `(F children) -> id`, so it emits `(set (F child_vals) target)` instead of the old relation row `(set (F child_vals target) ())`. Regenerated the 7 conflicting insta snapshots. All differ from upstream's only in `@vNNN` numbering and substitution ordering, plus the encoded-program snapshot showing the hash-consed table shapes; proof-mode tests run with `verify_proofs`, so they are checker-verified rather than snapshot-compared. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

codspeed-hq · 2026-07-27T16:05:08Z

Merging this PR will not alter performance

✅ 6 untouched benchmarks

_{Comparing oflatt-claude:worktree-revert-getfresh-to-constructors (93fb4cb) with main (853fbfd)}

Term, proof, AST, and proof-list node tables are children-keyed functions whose output column is the interned id, built with `set-if-empty`, not `get-fresh!`-minted `Unit` relations. Document that, the per-sort auxiliary union-find that records same-iteration collisions, the `:merge`-body fallback to `get-fresh!` + `set`, and the natural-node-seeded view in proof mode. Also fixes the missing `Sym` in two connector compositions and the stale `MathProof` / term-table flag lists. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The module doc still described the pre-hash-consing form, where a node id was minted with get-fresh! and blind-inserted as a relation row. Nodes are now interned: get-fresh! mints a candidate and set-if-empty returns the existing id on a hit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Node interning inside a `:merge` body cannot use `set-if-empty` (its table read is unavailable in a merge's execution state), so it falls back to `get-fresh!` + `set`. That mode was signalled by `EncodingState::in_merge`, a mutable flag on shared state saved/restored around two call sites. Replace it with a `Stmts` newtype: a `Vec<String>` statement sink tagged with its interning mode, constructed via `Stmts::new()` or `Stmts::merge_body()`. `hash_cons` reads the mode off the sink it is handed, so the mode is passed explicitly and cannot be mismatched. The proof-encoding emitters now thread `&mut Stmts` instead of `&mut Vec<String>`; `add_term_and_view` and `instrument_action` take the caller's sink rather than returning their own buffer, so merge mode is inherited rather than re-decided. No change to the emitted egglog source. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

The comments said set-if-empty's table read is unavailable in a merge's execution state. The real constraint is narrower and load-bearing: merges run a whole stratum at once with every table in it taken out of the database, and a merge's write targets are dependency-linked into its own stratum — so exactly the tables it would intern into are unreadable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Copilot

Pull request overview

This PR replaces the term/proof encoding’s “always mint fresh ids” strategy with hash-consing, so structurally identical term/proof/AST nodes are interned and reused (plus an auxiliary union-find to reconcile same-iteration collisions) and extraction can recover the surviving canonical node reliably.

Changes:

Hash-cons term/proof/AST/proof-list node tables via set-if-empty-* and record same-iteration collisions into per-sort AuxUF_<Sort>.
Extend parsing/typechecking/state restoration and extraction to track and consult :internal-aux-uf / aux_uf_parent (including extraction fallback via find_aux_canonical).
Add a backend guard (forbid_native_rebuild) plus regression tests, and update docs/snapshots/gitignore accordingly.

Reviewed changes

Copilot reviewed 33 out of 33 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap	Snapshot updates reflecting new interning / id allocation behavior in proofs.
egglog/tests/snapshots/files__proofs__rw_analysis_proof_testing.snap	Snapshot updates for proof construction changes under hash-consing.
egglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snap	Snapshot updates for fresh-var renumbering under new encoding.
egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap	Snapshot updates due to changed proof/node interning behavior.
egglog/tests/snapshots/files__proofs__naturals_proof_testing.snap	Snapshot updates reflecting altered proof structure after removing duplicate-node minting.
egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap	Snapshot updates (including metadata line changes) under new proof encoding.
egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap	Snapshot updates reflecting updated substitution ordering/ids.
egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap	Snapshot updates for container rebuild proofs under hash-consed nodes.
egglog/tests/snapshots/files__proofs__container_set_collapse_proof_testing.snap	Snapshot updates reflecting changed proof-node interning.
egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap	Snapshot updates for reordered/interened proof nodes.
egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap	Snapshot updates covering proof/AST/proof-list interning changes.
egglog/tests/no_native_rebuild.rs	New regression tests asserting the term/proof encoding never triggers backend-native rebuild.
egglog/src/typechecking.rs	Registers `set-if-empty-*` primitives for hash-consed `:internal-term-node` tables and restores `aux_uf_parent` on typecheck.
egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap	Snapshot updates showing hash-consed node tables and AuxUF in proof-mode output.
egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap	Snapshot updates showing `:internal-aux-uf` and new `set-if-empty-*` usage for term nodes.
egglog/src/proofs/proof_tests.rs	Updates tests to match new lowering pattern (interning via `set-if-empty-*` calls).
egglog/src/proofs/proof_fresh.rs	Documentation and primitives framing updated for interning/hash-consing.
egglog/src/proofs/proof_extractor.rs	Extraction now resolves AuxUF aliases before consulting the real union-find when a node row is missing.
egglog/src/proofs/proof_encoding.rs	Core refactor: introduce `Stmts` to track merge-body context; hash-cons term/proof node creation; emit/store AuxUF mappings.
egglog/src/proofs/proof_encoding.md	Documentation updated to describe hash-consed node tables, AuxUF behavior, and updated action lowering.
egglog/src/proofs/proof_encoding_rebuild.rs	Adjusts proof-rebuild instrumentation to use `Stmts` and new mint/intern behavior.
egglog/src/proofs/proof_encoding_helpers.rs	Adds `aux_uf_name` helper and updates proof/AST/proof-list table declarations to hash-consed forms.
egglog/src/proofs/proof_encoding_facts.rs	Updates fact instrumentation to use `Stmts` and new node interning approach.
egglog/src/prelude.rs	Initializes the new `aux_uf` field in sort commands.
egglog/src/lib.rs	Enables backend native-rebuild guard for term encoding; restores aux-uf mapping from sort annotations; updates native input handling for new table shapes.
egglog/src/extract.rs	Adds `find_aux_canonical` and updates `find_canonical` to fall back through AuxUF.
egglog/src/ast/parse.rs	Parses the new `:internal-aux-uf` sort annotation into the AST.
egglog/src/ast/mod.rs	Stores/prints the new `aux_uf` sort annotation field across AST transforms and formatting.
egglog/src/ast/desugar.rs	Threads the new `aux_uf` field through desugaring outputs.
egglog/egglog-bridge/src/lib.rs	Implements the backend-side `forbid_native_rebuild` latch and asserts in rebuild when violated.
egglog/egglog-backend-trait/src/lib.rs	Adds `Backend::forbid_native_rebuild` hook (default no-op).
egglog/egglog-backend-trait/src/backend_impl.rs	Wires `forbid_native_rebuild` through the backend trait impl.
egglog/.gitignore	Ignores insta pending snapshot artifacts (`*.snap.new`).

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

        let fresh_sort_decl = if output_is_eclass {
            String::new()
        } else {
            format!("(sort {fresh_sort})")
        };


coderabbitai

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

egglog/src/proofs/proof_encoding.rs (1)
1266-1289: 🗄️ Data Integrity & Integration | 🟠 Major | 🏗️ Heavy lift

Handle :merge mode for FD-view constructor interning.

add_constructor_term_only and add_constructor_with_proof only branch on proof mode, so a constructor in a custom-function :merge body is still emitted as set-if-empty-<View>!. Those helpers are already gated to run via merge-body interning, but the FD-view interning still bypasses in_merge; make the view interning also fall back to get-fresh! + set when compiling merge-body code.
🤖 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/src/proofs/proof_encoding.rs` around lines 1266 - 1289, Update
add_constructor_term_only and add_constructor_with_proof so FD-view interning
checks in_merge in addition to proof mode. When compiling merge-body code, use
get-fresh! followed by set instead of set-if-empty-<View>!, while preserving the
existing set-if-empty behavior for non-merge construction paths.

🤖 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.

Outside diff comments:
In `@egglog/src/proofs/proof_encoding.rs`:
- Around line 1266-1289: Update add_constructor_term_only and
add_constructor_with_proof so FD-view interning checks in_merge in addition to
proof mode. When compiling merge-body code, use get-fresh! followed by set
instead of set-if-empty-<View>!, while preserving the existing set-if-empty
behavior for non-merge construction paths.

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 9ee2db7c-1293-4102-9f1f-9fd7f1af93b5

📥 Commits

Reviewing files that changed from the base of the PR and between 853fbfd and f5fb271.

⛔ Files ignored due to path filters (13)

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__proofs__container_proofs_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__container_set_collapse_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__naturals_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__rw_analysis_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap is excluded by !**/*.snap

📒 Files selected for processing (20)

egglog/.gitignore
egglog/egglog-backend-trait/src/backend_impl.rs
egglog/egglog-backend-trait/src/lib.rs
egglog/egglog-bridge/src/lib.rs
egglog/src/ast/desugar.rs
egglog/src/ast/mod.rs
egglog/src/ast/parse.rs
egglog/src/extract.rs
egglog/src/lib.rs
egglog/src/prelude.rs
egglog/src/proofs/proof_encoding.md
egglog/src/proofs/proof_encoding.rs
egglog/src/proofs/proof_encoding_facts.rs
egglog/src/proofs/proof_encoding_helpers.rs
egglog/src/proofs/proof_encoding_rebuild.rs
egglog/src/proofs/proof_extractor.rs
egglog/src/proofs/proof_fresh.rs
egglog/src/proofs/proof_tests.rs
egglog/src/typechecking.rs
egglog/tests/no_native_rebuild.rs

Node interning inside a `:merge` body previously fell back to `get-fresh!` plus a blind `set`: `set-if-empty` reads the table it interns into, and a merge runs a whole stratum at once with every table in it taken out of the database, so the read hit a vacated table and panicked. The dependency graph already has the tool to fix this — a table that declares a read dependency is placed strictly above what it reads, so the target merges in an earlier stratum and is back in the database when the reader runs. The bridge just had no idea a primitive touched tables at all. Let a registered external function declare the tables it reads and writes (`EGraph::declare_external_func_table_deps`, by name, since primitives are registered before their target tables exist), and have `MergeFn::Primitive::fill_deps` resolve and contribute them. `register_set_if_empty` declares its target as both a read (the get-or-insert lookup) and a write (the insert on a miss); `register_view_column_read` declares a read. Declared deps are dropped in `free_external_func`, since external function ids are reused. With that in place, `hash_cons` always hash-conses, so `Stmts` — a `Vec<String>` newtype introduced only to carry the merge-body interning mode — collapses back to plain `Vec<String>`. Merge bodies now emit `set-if-empty-<Table>!` instead of `get-fresh!` + `set`. Nine proof snapshots shift only in internal gensym numbering/order inside `substitution` bindings; the proofs are checker-verified in those tests. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Declaring external-function read deps makes the DAG property load-bearing for backend stratification, so record why it holds for the term/proof encoding (a merge body cannot look up a custom function) and what would break it. Replace the bare unwrap in DependencyGraph::add_table with a message naming the table, the missing dependency, and the two ways to get there: a dependency registered too late, or a cycle. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

coderabbitai

Actionable comments posted: 1

Caution

Some comments are outside the diff and can’t be posted inline due to platform limitations.

⚠️ Outside diff range comments (1)

egglog/src/proofs/proof_encoding.md (1)
408-411: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Correct the term-table query description.

The term table is not queried by deletion maintenance, but proof extraction explicitly reads its :internal-term-node rows (Lines 128-132). Reword this to avoid contradicting the extraction contract; it also repeats the retention rationale from Lines 102-107.

As per coding guidelines, keep documentation concise and avoid duplicate information.
🤖 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/src/proofs/proof_encoding.md` around lines 408 - 411, Revise the
deletion-maintenance paragraph to state only that maintenance does not query the
term table, while preserving that proof extraction reads its :internal-term-node
rows. Remove the duplicated rationale about retaining rows and avoid implying
the term table is never accessed; update the text near delete_subsume_ruleset
accordingly.
Source: Coding guidelines

🤖 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/CHANGELOG.md`:
- Line 5: Condense the changelog bullet to the public contract: external
functions can declare the tables they read and write, and those dependencies are
included when called from :merge bodies for correct stratification. Remove
hash-consing implementation details and prior fallback behavior, then run make
nits or make fixnits before completing the change.

---

Outside diff comments:
In `@egglog/src/proofs/proof_encoding.md`:
- Around line 408-411: Revise the deletion-maintenance paragraph to state only
that maintenance does not query the term table, while preserving that proof
extraction reads its :internal-term-node rows. Remove the duplicated rationale
about retaining rows and avoid implying the term table is never accessed; update
the text near delete_subsume_ruleset accordingly.

🪄 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: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 966fa937-6aaa-4e27-a21a-4b20457a0b2b

📥 Commits

Reviewing files that changed from the base of the PR and between f5fb271 and 08bfaa1.

⛔ Files ignored due to path filters (9)

egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__container_reorder_proofs_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__container_set_collapse_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snap is excluded by !**/*.snap
egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap is excluded by !**/*.snap

📒 Files selected for processing (8)

egglog/CHANGELOG.md
egglog/core-relations/src/dependency_graph.rs
egglog/egglog-bridge/src/lib.rs
egglog/src/proofs/proof_encoding.md
egglog/src/proofs/proof_encoding.rs
egglog/src/proofs/proof_encoding_facts.rs
egglog/src/proofs/proof_encoding_helpers.rs
egglog/src/proofs/proof_encoding_rebuild.rs

coderabbitai · 2026-07-27T19:03:45Z


 ## [Unreleased] - ReleaseDate

+- A registered external function can declare which tables it reads and writes (`egglog_bridge::EGraph::declare_external_func_table_deps`), and a `:merge` body that calls it contributes those tables to the calling table's dependency-graph entry — so a merge that reads through a primitive is stratified above its read targets instead of racing them out of the database. `set-if-empty` and the view-column reader declare their target, which lets the term/proof encoding hash-cons node tables inside `:merge` bodies too (previously those fell back to `get-fresh!` plus a blind `set`, leaving duplicate ids for the `AuxUF` merge to fold away).


📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Condense this changelog entry to the public contract.

Keep one concise bullet describing dependency declarations for external functions used in :merge; move hash-consing mechanics and prior fallback behavior out of the changelog. Also confirm make nits or make fixnits ran before merge.

Proposed rewrite

-- A registered external function can declare which tables it reads and writes ... +- External functions used by `:merge` can declare table read/write dependencies, allowing dependency-aware merge stratification.

As per coding guidelines, “Keep documentation concise and avoid duplicate information,” and run make fixnits or make nits before completing changes.

📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change

- A registered external function can declare which tables it reads and writes (`egglog_bridge::EGraph::declare_external_func_table_deps`), and a `:merge` body that calls it contributes those tables to the calling table's dependency-graph entry — so a merge that reads through a primitive is stratified above its read targets instead of racing them out of the database. `set-if-empty` and the view-column reader declare their target, which lets the term/proof encoding hash-cons node tables inside `:merge` bodies too (previously those fell back to `get-fresh!` plus a blind `set`, leaving duplicate ids for the `AuxUF` merge to fold away).

- External functions used by `:merge` can declare table read/write dependencies, allowing dependency-aware merge stratification.

🤖 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/CHANGELOG.md` at line 5, Condense the changelog bullet to the public contract: external functions can declare the tables they read and write, and those dependencies are included when called from :merge bodies for correct stratification. Remove hash-consing implementation details and prior fallback behavior, then run make nits or make fixnits before completing the change.

Source: Coding guidelines

An eq-sort records its auxiliary union-find on the sort declaration so a re-parsed encoded program restores aux_uf_parent, but a custom function's throwaway view sort declared its AuxUF table without the annotation. Extraction could then not resolve a same-iteration hash-cons collision on those ids after a re-parse. Also condense the external-function dependency changelog entry to its contract. Reported by CodeRabbit on saulshanabrook#36. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Apply the `tidy-diff-docs` skill to the comments this branch added or changed: drop hash-consing mechanism re-explained at each site (the module doc and proof_encoding.md already cover it), demote an internal design rationale to a plain comment next to the code, and cut restated text where a nearby doc or the linked item already says it. Keep the caller obligations: the read-dependency declaration order and acyclicity requirement, `forbid_native_rebuild`'s contract, the `AuxUF`-before-real-UF extraction order, and the dependency-graph panic message. Also fix the `DependencyGraph::add_table` intra-doc link (private in core-relations, so it never resolved) and the stale claim that a plain `UF` edge is the whole story for `union` in proof mode. Comments only: no snapshot changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

oflatt · 2026-07-28T03:32:41Z

Might actually want to wait on this one, a different PR will cause tons of conflicts.

oflatt · 2026-08-11T20:50:39Z

I think merged already

oflatt and others added 5 commits July 24, 2026 16:33

Untrack insta .snap.new reject files and gitignore them

6d63994

These pending-snapshot artifacts were swept into an earlier commit by git add -A. They are regenerated on every test run, so ignore them instead of tracking.

oflatt and others added 2 commits July 27, 2026 15:21

oflatt and others added 4 commits July 27, 2026 16:17

oflatt marked this pull request as ready for review July 27, 2026 17:03

Copilot AI review requested due to automatic review settings July 27, 2026 17:03

Copilot started reviewing on behalf of oflatt July 27, 2026 17:03 View session

Copilot AI reviewed Jul 27, 2026

View reviewed changes

Comment thread egglog/src/proofs/proof_encoding.rs

Comment on lines 844 to 848

let fresh_sort_decl = if output_is_eclass {

String::new()

} else {

format!("(sort {fresh_sort})")

};

coderabbitai Bot reviewed Jul 27, 2026

View reviewed changes

oflatt-claude mentioned this pull request Jul 27, 2026

WIP: Materialized rebuild index + single-rule UF rebuild, rebuilt on #36 oflatt-claude/egglog-encoding#3

Draft

oflatt and others added 2 commits July 27, 2026 18:49

coderabbitai Bot reviewed Jul 27, 2026

View reviewed changes

oflatt and others added 2 commits July 28, 2026 03:08

oflatt marked this pull request as draft July 28, 2026 03:32

This was referenced Jul 29, 2026

Follow-ups after the minimal proof encoding (#39) #41

Open

FlowLog --emit-flowlog backend: performance follow-ups #50

Open

coderabbitai Bot mentioned this pull request Aug 8, 2026

:merge action block writes a dangling e-class when colliding values are equal #59

Open

oflatt closed this Aug 11, 2026

Navigation Menu

Hash-cons term and proof tables instead of minting with get-fresh! - #36

Hash-cons term and proof tables instead of minting with get-fresh!#36
oflatt-claude wants to merge 15 commits into
saulshanabrook:mainfrom
oflatt-claude:worktree-revert-getfresh-to-constructors

oflatt-claude commented Jul 27, 2026 •

edited by coderabbitai Bot

Loading

Uh oh!

coderabbitai Bot commented Jul 27, 2026 •

edited

Loading

Review limit reached

Walkthrough

Changes

Sequence Diagram(s)

Uh oh!

codspeed-hq Bot commented Jul 27, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

coderabbitai Bot left a comment

Uh oh!

coderabbitai Bot left a comment

Uh oh!

coderabbitai Bot Jul 27, 2026

Uh oh!

oflatt commented Jul 28, 2026

Uh oh!

oflatt commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants


		## [Unreleased] - ReleaseDate

		- A registered external function can declare which tables it reads and writes (`egglog_bridge::EGraph::declare_external_func_table_deps`), and a `:merge` body that calls it contributes those tables to the calling table's dependency-graph entry — so a merge that reads through a primitive is stratified above its read targets instead of racing them out of the database. `set-if-empty` and the view-column reader declare their target, which lets the term/proof encoding hash-cons node tables inside `:merge` bodies too (previously those fell back to `get-fresh!` plus a blind `set`, leaving duplicate ids for the `AuxUF` merge to fold away).

Conversation

oflatt-claude commented Jul 27, 2026 • edited by coderabbitai Bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

The problem

The change

Commits

On commit 5

Testing

Native rebuild is now provably dead under the encoding

Performance

Cost of uniform interning

Summary by CodeRabbit

Uh oh!

coderabbitai Bot commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Walkthrough

Changes

Sequence Diagram(s)

Uh oh!

codspeed-hq Bot commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Merging this PR will not alter performance

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

coderabbitai Bot left a comment

Choose a reason for hiding this comment

Uh oh!

coderabbitai Bot Jul 27, 2026

Choose a reason for hiding this comment

Uh oh!

oflatt commented Jul 28, 2026

Uh oh!

oflatt commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

oflatt-claude commented Jul 27, 2026 •

edited by coderabbitai Bot

Loading

coderabbitai Bot commented Jul 27, 2026 •

edited

Loading

codspeed-hq Bot commented Jul 27, 2026 •

edited

Loading