WIP: Materialized rebuild index + single-rule UF rebuild, rebuilt on #36

[oflatt-claude]

Draft — this is saulshanabrook#19 rebuilt on top of saulshanabrook#36, and the result is a measured regression. Not for merge as-is.

Rebuilds #19 (materialized rebuild index + single-rule UF rebuild) on top of #36 (hash-consed term/proof tables). saulshanabrook#19's original diff no longer applies — rebuilding_rules moved to proof_encoding_rebuild.rs, views are now always FD (keyed on children) for constructors and custom functions, and saulshanabrook#36 added the Stmts/mint hash-consing layer — so this is a reimplementation rather than a rebase.

Base is saulshanabrook#36's head (f5fb271), so the diff here is only the saulshanabrook#19 rebuild.

Why this was worth retrying

saulshanabrook#19 measured ~+18% on math-microbenchmark and diagnosed the cause as the native rebuild scanning the extra index tables' :internal-uf columns. saulshanabrook#36 makes native rebuild provably dead under the encoding (forbid_native_rebuild), which should have removed exactly that cost. It did not — the approach is still slower — so that diagnosis was wrong. The measurements below locate the real cost instead.

What it does

• Rebuild index. One hidden (function <F>Index_<S> (S key...) Unit :merge old) per view, per distinct child eq-sort, holding for each view row one entry per S-typed child: that child first, then the row's whole key. Leading with the child makes "which rows mention this term" a key-prefix lookup. Maintained wherever the view is written or deleted. Container children are not indexed — they have no @UF row to drive a lookup.
• One rule per indexed child position, driven by an @UF_<S> edge joined against the index rather than by matching the view. The moved term is bound at a known position, so its leader is a plain substitution and proof mode composes one Congr there from the edge proof the body already bound.
• The row's value tuple is read on the RHS (WIP: Materialized rebuild index + single-rule UF rebuild saulshanabrook/egglog-encoding#19's third commit), not joined as a third body atom — the index entry already binds the key. This turned out to be the single most important part; see the numbers below.
• New SPI Backend::register_view_column_lookup, a fallback-free (keys) -> column view read. ExternalFunction::invoke returning None halts the calling rule, which is exactly the semantics a body join has when the row is absent — so unlike the existing fallback-taking register_view_column_read, there is no need to invent an e-class for a row that is not there. The DD interpreter cannot abandon an action mid-flight, so it reports an absent key instead; the index witnesses the row, so it never fires.

Two dead ends worth recording, both verified against the code:

• uf_canon as a ReadPrim (as WIP: Materialized rebuild index + single-rule UF rebuild saulshanabrook/egglog-encoding#19 had it) is rejected by the Differential Dataflow backend in an action context — requires a backend action registry, 22 DD test failures. Re-expressing it as a generic view-column read over the two-output @UF_<S> table fixed that. It is gone from the head anyway: binding the child position removed every caller.
• Having the view's :merge maintain the index (so the index could carry the e-class and absorb the value-column rule) is not expressible. A :merge body sees only old/new(0/1) and let locals — MergeFn has Old, New, OldCol(i), NewCol(i), LetVar(slot) and no way to name a key column — so it cannot name the index row to update. It would need a KeyCol(i) variant in the bridge. WIP: Materialized rebuild index + single-rule UF rebuild saulshanabrook/egglog-encoding#19 hit the same wall.

A real bug this surfaced

instrument_construct_into wrote the view with a raw set, bypassing update_fd_view, so those rows got no index entries and were unreachable from the rebuild rule — they silently stayed stale. unsafe_seminaive_matches_naive caught it. Added rebuild_index_covers_every_view_row, which asserts the invariant directly; verified non-vacuous by reverting the fix, which the test then catches.

Testing

Whole workspace green: --test files 792 passed, --lib 69 passed, egglog-experimental-dd --test files 135 passed, 0 failures anywhere. cargo fmt --all --check and clippy clean. Proof-mode tests run with verify_proofs, so every passing proof test is checker-validated, not just snapshot-compared.

11 proof snapshots regenerated, differing only by fresh-var renumbering — the per-position rule reproduces the baseline's proof derivations.

Performance — still a regression, but the shape changed

bench.py --target . --compare-target @f5fb271 --treatment proofs --compare-treatment proofs,
6 rounds per endpoint/file, machine otherwise idle. Ratios are candidate / baseline.

Three variants were built and measured in turn:

Variant	Suite wall time
Index + whole-row uf_canon recanon, view joined in the body	1.15–1.16x
…with the row's value tuple read on the RHS instead	1.08–1.13x
…driven from a known child position, one Congr, no uf_canon (head)	1.10–1.11x

Head — wall time, suite total 1.10–1.11x slower.

File	Baseline	Candidate	Ratio	Result
math-microbenchmark.egg	10.4–10.6 s	12.7–12.9 s	1.20–1.23x	slower
herbie.egg	1.02–1.04 s	1.10–1.13 s	1.07–1.10x	slower
luminal-llama.egg	8.24–8.26 s	8.75–8.80 s	1.06–1.07x	slower
hardboiled_conv1d_32.egg	1.39–1.41 s	1.48–1.50 s	1.05–1.07x	slower
eggcc-2mm-pass1.egg	13.0 s	13.7 s	1.05–1.06x	slower
pointer-analysis-small.egg	68.8–83.9 ms	73.1–87.5 ms	0.920–1.20x	CI includes 1

Peak RSS — 6–16% higher on 5 of 6. The index costs one entry per eq-sort child per
view row, which gives back part of saulshanabrook#36's memory win.

File	Baseline	Candidate	Ratio
math-microbenchmark.egg	1.6 GiB	1.9 GiB	1.16x
luminal-llama.egg	674.9 MiB	746.4 MiB	1.11x
eggcc-2mm-pass1.egg	726.3 MiB	802.0 MiB	1.10x
hardboiled_conv1d_32.egg	160.0 MiB	172.4 MiB	1.08x
herbie.egg	106.9 MiB	114.3 MiB	1.06–1.07x
pointer-analysis-small.egg	105.5 MiB	105.5 MiB	1.00x

Where the time goes

Rebuild is 0 ns on both sides everywhere, so native rebuild is not involved. Per-ruleset
deltas on math-microbenchmark, tracked across the three variants:

Variant	@rebuilding Search Δ	Apply Δ	Merge Δ	user rulesets Δ
body join + whole-row	+1.33 s	+693 ms	+306 ms	+885 ms
RHS read + whole-row	−267 ms	+922 ms	+381 ms	+757 ms
RHS read + per-position (head)	+205 ms	+557 ms	+797 ms	+672 ms

The interesting result is the middle row: once the view join leaves the body, the
index-driven rebuild searches faster than the per-column fan-out it replaces. The premise
of saulshanabrook#19 — that a materialized term→row index beats matching the view — does hold. What sank
the first version was the third body atom, not the index.

What remains is write cost, not search cost, in two places no rebuild-rule tuning reaches:

1. Index maintenance in the user rulesets (+672 ms of a ~10.5 s baseline, as Apply +
   Merge). Every term construction writes k index rows on top of its view row. This is
   inherent to keeping a materialized index, and it is also where the extra RSS comes from.
2. @rebuilding Merge (+797 ms), the re-keying writes themselves.

Whole-row recanon and per-position are a wash overall (1.08–1.13x vs 1.10–1.11x, overlapping
CIs): whole-row fixes a row in one firing but pays k union-find reads and k mostly-reflexive
Congr mints per firing; per-position pays O(1) per firing but needs k firings, trading
Apply for Merge. Head keeps per-position because it is simpler — no uf_canon primitives at
all, and proof derivations match the baseline's.

Conclusion: the index's search win is real and reproducible, but it does not cover the
maintenance and re-keying writes it adds. Preserved for reference, as saulshanabrook#19 was.

🤖 Generated with Claude Code