Avoid redundant proof merge rows for eager current values

[saulshanabrook]

Summary

• Add a hidden current-value function for proof-encoded custom functions that have a merge function.
• Keep that current-value function updated from ordinary proof-view writes, using the original eager backend merge.
• Add a cleanup rule that deletes stale proof-view candidates when the eager current value already has a proof witness, while leaving the existing merge-proof path as the fallback.
• Add a focused regression test for a selector-style :merge old function.

Why

This is needed for eggcc proof export to finish in reasonable time. The old proof encoding could keep every candidate proof-view row for a merged function and then run @merge_rule over every pair. For selector/eager merges, the backend already knows the current value, so those pairwise proof merges are redundant when the selected row already has a proof witness.

Slow Example

A generated file with this shape was slow before this change and is faster now:

(sort Key)
(constructor K () Key)
(function Best (Key) i64 :merge old)
(relation Candidate (Key i64))
(rule ((Candidate k v))
      ((set (Best k) v)))

;; Repeat many same-key candidates, e.g. 3000 rows:
(Candidate (K) 0)
(Candidate (K) 1)
;; ...
(Candidate (K) 2999)

(run 1)
(check (= (Best (K)) 0))

Run with proof mode, for example:

egglog --proofs --save-report selector-old-3000-report.json selector-old-3000.egg

On the same 3000-candidate file:

• before: @merge_rule = 4,498,500, @merge_cleanup = 4,498,500, wall time about 7.04s
• after: @merge_rule = 0, @merge_current_cleanup = 2,999, wall time about 4.61s

The wall-time improvement is partially hidden by parsing and report overhead, but the quadratic proof-merge work is eliminated for this selector case.

Validation

• cargo test --release --test proof_selector_merge
• git diff --check

[saulshanabrook]

@coderabbitai full review

[coderabbitai]

✅ Action performed

Full review finished.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro

Run ID: e08edefb-f8f3-4c11-825a-945e0e49ad60

📥 Commits

Reviewing files that changed from the base of the PR and between 7d102db and 1f4f128.

📒 Files selected for processing (2)

• src/proofs/proof_encoding.rs
• tests/proof_selector_merge.rs

📜 Recent review details

⏰ Context from checks skipped due to timeout. (16)

• GitHub Check: benchmark (ubuntu-latest, proof_testing_math)
• GitHub Check: benchmark (ubuntu-latest, math_normal)
• GitHub Check: benchmark (ubuntu-latest, proof_testing_typecheck)
• GitHub Check: benchmark (ubuntu-latest, rust_rule_match_with_serialize)
• GitHub Check: benchmark (ubuntu-latest, rust_rule_match_overhead)
• GitHub Check: benchmark (ubuntu-latest, proof_testing_eqsat-basic)
• GitHub Check: benchmark (ubuntu-latest, proof_testing_unify)
• GitHub Check: benchmark (ubuntu-latest, rust_rule_insert_loop)
• GitHub Check: benchmark (ubuntu-latest, eggcc-2mm)
• GitHub Check: benchmark (ubuntu-latest, stresstest_large_expr)
• GitHub Check: benchmark (ubuntu-latest, rectangle)
• GitHub Check: benchmark (ubuntu-latest, conv1d_128)
• GitHub Check: benchmark (ubuntu-latest, math-microbenchmark)
• GitHub Check: benchmark (ubuntu-latest, taylor51)
• GitHub Check: benchmark (ubuntu-latest, herbie)
• GitHub Check: test

🧰 Additional context used

📓 Path-based instructions (1)

**/*.{md,txt,rs}

📄 CodeRabbit inference engine (CLAUDE.md)

Keep documentation concise and avoid duplicate information

Files:

• tests/proof_selector_merge.rs
• src/proofs/proof_encoding.rs

🔇 Additional comments (5)

src/proofs/proof_encoding.rs (3)

13-17: LGTM!

Also applies to: 38-38

---

264-282: LGTM!

Also applies to: 331-335, 358-364

---

1031-1040: 🩺 Stability & Availability

Edition 2024 and Rust 1.88+ requirement already satisfied.

The let-chain syntax at lines 1032–1034 requires Rust 1.88.0+ with edition 2024. The workspace Cargo.toml is configured with edition = "2024", and the code is already present in the codebase, confirming the toolchain meets this requirement. No action needed.

tests/proof_selector_merge.rs (2)

19-20: 🎯 Functional Correctness | 💤 Low value

Verify the (Best (K)) = 0 check is deterministic.

With :merge old, all 200 (set (Best k) v) for v in 0..200 are applied within a single iteration ((run 1)). The surviving value depends on the merge resolution order for batched inserts; if that order isn't guaranteed to keep the first-inserted value, this check could be flaky across runs/backends. The core assertion (merge_rule matches == 0) is unaffected. Please confirm the value selection is deterministic, or relax the check to not assume a specific winner.

---

27-34: LGTM!

---

📝 Walkthrough

Summary by CodeRabbit

Bug Fixes

• Enhanced merge-rule cleanup logic to reduce unnecessary rule executions during proof generation, improving system efficiency
• Improved tracking of merged function operations to prevent stale data accumulation

Tests

• Added comprehensive test coverage for merge selector cleanup behavior, validating correct proof operation handling

Walkthrough

EncodingState gains a merge_current map tracking a "current-value" function symbol and input arity per merge function. handle_merge_fn allocates this symbol, records it in the map, and emits a function declaration plus a stale-row cleanup rule. update_view is extended to conditionally emit a set for the current-name table. A regression test asserts zero merge-rule matches.

Changes

merge_current proof cleanup

Layer / File(s)	Summary
merge_current field and initialization src/proofs/proof_encoding.rs	Adds merge_current: HashMap<String, (String, usize)> to EncodingState with a doc comment and initializes it to HashMap::default() in EncodingState::new.
current_name allocation, declaration, and cleanup rule in handle_merge_fn src/proofs/proof_encoding.rs	Allocates a fresh current_name symbol per merge function, records it in merge_current, emits a (function {current_name} ...) declaration with merge/unextractable/internal-hidden attributes, and generates a rebuild cleanup rule that deletes stale {view_name} rows when selected differs from old.
update_view current-name set and regression test src/proofs/proof_encoding.rs, tests/proof_selector_merge.rs	update_view conditionally emits an extra set targeting {current_name} when the argument arity matches. The new test builds a :merge old program with 200 facts, runs it with proofs, and asserts zero "merge_rule" matches.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title directly addresses the main optimization: avoiding redundant proof merge rows for eager current values, which matches the primary change.
Description check	✅ Passed	The description is comprehensive and directly related to the changeset, explaining the motivation, implementation approach, and performance improvements.
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.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests

---

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

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 86.56%. Comparing base (7d102db) to head (0a868b6).

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #928      +/-   ##
==========================================
+ Coverage   86.54%   86.56%   +0.02%     
==========================================
  Files          89       89              
  Lines       26804    26835      +31     
==========================================
+ Hits        23197    23231      +34     
+ Misses       3607     3604       -3     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[codspeed-hq]

Merging this PR will not alter performance

✅ 29 untouched benchmarks
⏩ 219 skipped benchmarks¹

---

_{Comparing saulshanabrook:codex/proof-selector-merge-main (0a868b6) with main (7d102db)}

Footnotes

1. 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. ↩

[oflatt]

I'm working on #933, which hopefully will replace this. We'll keep this open as an option for now

[oflatt]

makes sense to me! nice fix