Skip to content

Sync egglog subtrees for eggcc container benchmark#9

Merged
saulshanabrook merged 9 commits into
mainfrom
codex/eggcc-container-subtree-sync
Jul 9, 2026
Merged

Sync egglog subtrees for eggcc container benchmark#9
saulshanabrook merged 9 commits into
mainfrom
codex/eggcc-container-subtree-sync

Conversation

@saulshanabrook

@saulshanabrook saulshanabrook commented Jul 8, 2026

Copy link
Copy Markdown
Owner

Summary

This PR is the subtree-sync base for the eggcc container benchmark work.

It contains:

The local benchmark, proof snapshot, CI, and review-fix changes are intentionally kept out of this PR and stacked in #10.

Review Notes

Review this as imported upstream/subtree work. The follow-up PR should be reviewed against this branch so the local changes are isolated from the subtree and PR 914 diffs.

Summary by CodeRabbit

  • New Features

    • Added experimental support for container types and rebuild behavior in the CLI and proof mode.
    • Introduced a nightly benchmark command that produces an HTML results dashboard.
    • Added deterministic ordering helpers for term handling, improving canonical output.
  • Bug Fixes

    • Improved proof handling for container-related expressions, including normalization and validation.
    • Fixed scheduler behavior so subsumed matches are no longer treated as fresh results.
  • Tests

    • Added end-to-end coverage for container rebuilds and proof-mode container behavior.

6f0d26e3 Merge pull request #927 from oflatt/oflatt-container-proofs
85ba2626 small feedback fixes
4141a970 Merge pull request #935 from egraphs-good/nightly
5009aaee simplify map.rs
e45cd547 address feedback from Saul
3960015c Merge pull request #885 from saulshanabrook/codex/split-scheduler-stale-match-cleanup
bd1697a3 Tighten the Containers section of proof_encoding.md (#10)
5fca83b7 Add container support to the term/proof encoding
7f111370 nightly: prefer the rustup cargo shim over the system cargo (#942)
15888b87 nightly: install deps into a venv to satisfy PEP 668 (#939)
f295052e scheduler: skip subsumed fresh matches
d1418d20 Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup
f99482a2 Merge pull request #936 from oflatt-claude/nightly-eval-live
fe240e6b Render nightly benchmark report with eval-live
5bb42afc nightly
6c6f01d5 scheduler: simplify changelog entry
c1420100 scheduler: reduce held validation churn
ce4ef0b5 scheduler: validate only held matches
f0d4822b scheduler: keep stale validation focused
1dedb505 scheduler: condense changelog entry
939339b1 scheduler: simplify stale match validation
ed6aa6e9 scheduler: preserve existing match handling
8602f56e scheduler: split action-key dedup cleanup
89779541 scheduler: validate only held matches
e24d1468 scheduler: clarify stale match validation
eaf4ab4f Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup
0804bee1 scheduler: deduplicate residual match keys
2c55caff Merge remote-tracking branch 'upstream/main' into codex/split-scheduler-stale-match-cleanup
09b8c002 scheduler: document stale match validation
2c749b89 scheduler: clean stale matches

git-subtree-dir: egglog
git-subtree-split: 6f0d26e37241055a1230bdcdb33f0c5d3f01e935
5d24c481 Refresh eggcc proof baseline onto PR 927 core
19ed8666 Remove redundant eggcc helper fixture
fcdaccba Add full eggcc proof fixture
6b37b6b3 Add eggcc proof baseline helpers

git-subtree-dir: egglog-experimental
git-subtree-split: 5d24c48197f796e130457fa2f0c10a60dfe258c7
…gcc-container-benchmark

# Conflicts:
#	egglog-experimental/Cargo.toml
#	egglog-experimental/src/keep_best.rs
#	egglog-experimental/src/lib.rs
#	egglog-experimental/src/set_cost.rs
#	egglog-experimental/src/sugar/for.rs
#	egglog-experimental/src/table_stats.rs
@coderabbitai

coderabbitai Bot commented Jul 8, 2026

Copy link
Copy Markdown

Review Change Stack

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 00d21040-02c0-49cd-961a-ce6886fdaf5f

📥 Commits

Reviewing files that changed from the base of the PR and between cf26722 and e71edaf.

⛔ Files ignored due to path filters (71)
  • Cargo.lock is excluded by !**/*.lock
  • egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg is excluded by !**/*.egg
  • egglog-experimental/tests/proofs/unstable-fresh-proof.egg is excluded by !**/*.egg
  • egglog-experimental/tests/snapshots/files__proofs__eggcc_2mm_pass1_merge_old_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__for_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__test_fresh_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__test_simple_fresh_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__test_working_fresh_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__unstable_fresh_proof_proof_testing.snap is excluded by !**/*.snap
  • egglog-experimental/tests/snapshots/files__proofs__with_ruleset_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/proofs/rule-head-fast-path.egg is excluded by !**/*.egg
  • egglog/tests/snapshots/files__proof_manual_disabled_files.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__antiunify_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__bind_prim_result_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__birewrite_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__bitwise_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__calc_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__combinators_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__combined_nested_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__commute_collapse_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__complex_merge_func_proof_testing.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_set_collapse_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__f64_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__fail_wrong_assertion_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__fibonacci_demand_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__global_prove_query_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__i64_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__include_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__integer_math_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__matrix_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__merge_during_rebuild_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__path_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__path_union_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__pathproof_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__points_to_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__primitive_args_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__primitives_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__push_pop_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__relation_query_allowed_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_define_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_empty_query_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_equal_constant2_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__repro_filter_bug_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_new_backend_prims_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_noteqbug_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_querybug2_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_querybug4_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_small_rebuild_fail_term_encoding_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__repro_typecheck_term_encoding_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__resolution_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__rule_head_fast_path_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__schedule_demo_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__simple_proof_check_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__stratified_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__string_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__test_combined_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__test_combined_steps_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__typecheck_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__unify_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__proofs__until_proof_testing.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_rule_head_fast_path.snap is excluded by !**/*.snap
📒 Files selected for processing (14)
  • .github/workflows/build.yml
  • AGENTS.md
  • README.md
  • bench.py
  • egglog-experimental/Cargo.toml
  • egglog-experimental/src/container_primitives.rs
  • egglog-experimental/src/lib.rs
  • egglog-experimental/src/maybe.rs
  • egglog-experimental/tests/eggcc_2mm_proof.rs
  • egglog-experimental/tests/files.rs
  • egglog/src/lib.rs
  • egglog/src/proofs/proof_encoding_helpers.rs
  • egglog/tests/files.rs
  • test_bench.py
 _______________________________________________________________________________
< Fancy algorithms are slow when n is small, and n is usually small. - Rob Pike >
 -------------------------------------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).
📝 Walkthrough

Walkthrough

This PR adds container sort proof/rebuild support to egglog core (ValueRebuilder trait split, canonical term forms, proof encoding/checking for containers), new Maybe/Either sorts and merge primitives in egglog-experimental, hash index rebuild performance rework, a scheduler fix, and a nightly benchmark harness.

Changes

Core container proofs and rebuild support

Layer / File(s) Summary
ValueRebuilder trait split
egglog/core-relations/src/table_spec.rs, .../uf/mod.rs, .../containers/mod.rs, .../containers/tests.rs, .../lib.rs, egglog/egglog-bridge/src/tests.rs, egglog/src/sort/fn.rs, egglog/src/sort/mod.rs
New ValueRebuilder trait separates value-level rebuild from Rebuilder; rebuild_val_with added on container envs; all rebuild_contents implementations updated.
Sort AST metadata
egglog/src/ast/mod.rs, .../ast/parse.rs, .../ast/desugar.rs, egglog/src/prelude.rs
Adds ContainerRebuildSpec/ProofConstructorNames, extends Sort command variants with uf tuple, container_rebuild, proof_constructors, and parser/display/mapping support.
Container/Sort trait hook
egglog/src/prelude.rs, egglog/src/sort/mod.rs
Adds rebuild_container_normalizer to ContainerSort/Sort traits.
Canonical term forms
egglog/src/termdag.rs, egglog/src/sort/vec.rs, set.rs, map.rs, multiset.rs, pair.rs
Adds ast_cmp/OrdTerm and canonical term normalization/validators for Vec, Set, Map (new map-of), MultiSet, Pair.
Container rebuild primitives
egglog/src/proofs/proof_container_rebuild.rs, mod.rs, egglog/src/typechecking.rs, egglog/src/lib.rs
Registers value/proof rebuild primitives per container sort and wires them through typechecking and command execution.
Proof/term encoding pipeline
egglog/src/proofs/proof_encoding.rs, proof_encoding_helpers.rs, proof_extraction.rs
Extends encoding state and rebuilding rules for containers; detects query-constructed containers misused in actions.
Proof checking/format
egglog/src/proofs/proof_checker.rs, proof_normal_form.rs, proof_format.rs, proof_simplification.rs, proof_encoding.md
Adds ContainerNormalize/Eval justifications, side-condition checking, exact-match parsing, and redundant normalize elimination.
Tests
egglog/tests/container_rebuild.rs, egglog/src/proofs/proof_tests.rs, egglog/src/lib.rs
Adds end-to-end container rebuild tests and updated proof-support tests.

Egglog-experimental container primitives

Layer / File(s) Summary
Maybe/Either sorts
egglog-experimental/src/maybe.rs, either.rs
New container sorts with construction/unwrap primitives and term reconstruction.
Bound-merge primitives and wiring
egglog-experimental/src/container_primitives.rs, lib.rs
Adds pair-min-by-second-i64 and maybe-either-i64-bool-min/max primitives; registers new modules and sorts.
CLI/cost/tests
egglog-experimental/src/main.rs, set_cost.rs, tests/eggcc_2mm_proof.rs, tests/files.rs
Proof-mode CLI detection, cost lookup refactor, new fixture tests.

Hash index performance and scheduler fix

Layer / File(s) Summary
Index rebuild rework
egglog/core-relations/src/hash_index/mod.rs, tests.rs
Replaces vector-wide radix sort with block-based slice sort and tournament merge-dedup.
Scheduler fix
egglog/src/scheduler.rs
Prevents subsumed rows from being treated as fresh matches; adds regression test.

Nightly benchmark harness

Layer / File(s) Summary
Benchmark script and tooling
egglog/scripts/nightly_bench.py, Makefile, scripts/requirements.txt, .gitignore, CHANGELOG.md
Adds benchmark discovery/measurement/HTML report script, make target, dependencies, ignore rules, changelog entries.

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

Sequence Diagram(s)

sequenceDiagram
  participant Typechecker
  participant ProofState
  participant EGraph
  participant ContainerRebuild
  Typechecker->>ProofState: record uf/proof_func/proof_constructors metadata
  Typechecker->>ContainerRebuild: register_container_rebuild_from_spec(sort, spec)
  EGraph->>ProofState: restore uf_parent/proof_names on Sort command
  EGraph->>ContainerRebuild: invoke rebuild primitive on container value
  ContainerRebuild-->>EGraph: rebuilt canonical container value / proof
Loading
🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
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.
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title accurately summarizes the subtree sync and the eggcc container benchmark focus.
✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch codex/eggcc-container-subtree-sync

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.

@codspeed-hq

codspeed-hq Bot commented Jul 8, 2026

Copy link
Copy Markdown

Merging this PR will not alter performance

✅ 3 untouched benchmarks
🆕 3 new benchmarks

Performance Changes

Mode Benchmark BASE HEAD Efficiency
🆕 Memory files[integer_math_proofs] N/A 10.4 MB N/A
🆕 Memory files[resolution_proofs] N/A 4.2 MB N/A
🆕 Memory files[rw_analysis_proofs] N/A 10.6 MB N/A

Comparing codex/eggcc-container-subtree-sync (e71edaf) with main (d9b4001)1

Open in CodSpeed

Footnotes

  1. No successful run was found on main (e71edaf) during the generation of this report, so d9b4001 was used instead as the comparison base. There might be some changes unrelated to this pull request in this report.

@oflatt oflatt left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice, I assume this just syncs so approved

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 4

🧹 Nitpick comments (3)
egglog/core-relations/src/hash_index/mod.rs (1)

584-613: 🩺 Stability & Availability | 🔵 Trivial | ⚡ Quick win

Consider a debug_assert to guard the sorted invariant relied on by unsafe in get_subset.

The Sparse subsets built here feed SparseColumnIndex::get_subset, whose unsafe block assumes RowIds within each per-key range are non-decreasing (rows sorted by (Value, RowId)). Correctness today depends entirely on every caller pre-sorting pairs; a future caller that forgets would silently break that safety assumption. A cheap debug-only check documents and enforces the contract at the boundary.

🛡️ Proposed defensive check
 fn build_subsets_from_sorted(&mut self, pairs: &[(Value, RowId)]) {
+    debug_assert!(
+        pairs.windows(2).all(|w| w[0] <= w[1]),
+        "build_subsets_from_sorted requires pairs sorted by (Value, RowId); \
+         get_subset relies on non-decreasing RowIds per key"
+    );
     let mut i = 0;
🤖 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/core-relations/src/hash_index/mod.rs` around lines 584 - 613, The
sorted-order contract for build_subsets_from_sorted is only implied today, but
SparseColumnIndex::get_subset’s unsafe path depends on it. Add a debug-only
assertion at the start of build_subsets_from_sorted that verifies pairs are
sorted by (Value, RowId) and contain no duplicate (Value, RowId) entries, so any
future caller violating the invariant fails fast before reaching get_subset.
Keep the check local to build_subsets_from_sorted and reference the existing
precondition in its documentation.
egglog/scripts/requirements.txt (1)

1-1: 🔒 Security & Privacy | 🔵 Trivial | ⚡ Quick win

Pin eval-live to a specific commit for reproducibility.

An unpinned git dependency means any breaking change in eval-live will silently break the nightly benchmark. Pin to a commit hash and update it deliberately.

🔒️ Proposed fix
-eval-live @ git+https://github.com/oflatt/eval-live.git
+eval-live @ git+https://github.com/oflatt/eval-live.git@<commit-sha>
🤖 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/scripts/requirements.txt` at line 1, The eval-live dependency is using
an unpinned git reference, so update the requirements entry to use a specific
commit hash instead of the floating branch head. Make this change in the
requirements entry for eval-live in the dependency list, and keep the package
name and git URL the same while adding the commit-specific pin for reproducible
nightly runs.
egglog/src/proofs/proof_container_rebuild.rs (1)

277-368: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Reflexive anchor at the outer level looks duplicated by the caller.

rebuild_container_proof_rec's trailing anchor block (Lines 353-365) sets <CSort>Proof(rebuilt) = Trans(Sym(current), current) for every recursion level, including the top-level (sort == container_sort). But proof_encoding.rs::rebuilding_rules already emits an equivalent action for the outer container column:

(let proof_var (proof_prim ci))
(set (cproof rebuilt_var) (trans (sym proof_var) proof_var))

rebuilt_var/proof_var there should equal this function's rebuilt/current for the outer call, so the same table row appears to get set twice per rebuild firing (once via raw insert inside the primitive, once via the rule's set). The primitive-side anchor is genuinely needed for nested containers (since rebuilding_rules only handles the top column), but seems redundant at the outer level.

:merge old and hash-consed sym/trans likely make this harmless, but it's wasted work on a per-rebuild hot path and adds a second source of truth for the same invariant.

♻️ Possible fix: only anchor at nested recursion levels
 fn rebuild_container_proof_rec(
     state: &mut FullState,
     prim: &ContainerRebuildProof,
     sort: &ArcSort,
     value: Value,
+    is_top_level: bool,
 ) -> Option<(Value, Value)> {
@@
-    // Anchor a reflexive proof on the rebuilt value for future rebuilds.
-    if rebuilt != value {
+    // Anchor a reflexive proof on the rebuilt value for future rebuilds.
+    // The top-level anchor is already set by the caller's rebuild rule action.
+    if !is_top_level && rebuilt != value {

Please confirm this is intentional (or a leftover from before the caller-side anchoring existed) before deciding whether to change it.

🤖 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_container_rebuild.rs` around lines 277 - 368, The
trailing reflexive anchor in rebuild_container_proof_rec duplicates the
outer-level proof row already emitted by proof_encoding.rs::rebuilding_rules, so
adjust the anchoring logic to skip inserting the cproof row for the top-level
container while keeping it for nested container recursion. Keep the existing
proof construction in rebuild_container_proof_rec, but gate the final
sym/trans/cproof insert path so only recursive inner container rebuilds mint the
anchor, using the existing symbols rebuild_container_proof_rec, cproof_action,
sym_action, and trans_action to locate the change.
🤖 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-experimental/src/either.rs`:
- Around line 4-7: The import list in either.rs is missing Term, which is needed
by the validator closures that reference Term::App. Update the top-level egglog
import used near add_primitive_with_validator to include Term so the
Either-related validator code compiles without unresolved symbol errors.

In `@egglog-experimental/src/maybe.rs`:
- Around line 63-81: `MaybeSort::make_sort` currently panics when the sort
arguments don’t match the expected shape, so malformed input can crash
typechecking instead of returning a `TypeError`. Update the arity handling in
`make_sort` to validate the incoming `args` and return an appropriate error for
invalid container arity rather than panicking, and apply the same fix to
`EitherSort::make_sort` so both sort constructors fail gracefully on bad user
input.

In `@egglog/scripts/nightly_bench.py`:
- Around line 69-75: The proof exclusion list in nightly_bench.py has drifted
from the exclusions in tests/files.rs because eqsolve.egg is missing, so update
the PROOF_UNSUPPORTED_FILES source used by the proof benchmark setup to stay
aligned with the test harness. Prefer sharing one central list or helper for the
exclusions instead of duplicating the filenames, and make sure the code that
drives the nightly proof benchmarks references that shared source so future
additions stay in sync.

In `@egglog/src/ast/mod.rs`:
- Around line 1678-1688: The `replace_internal_symbol_with` path in `ast::mod`
is not updating the `container_rebuild` and `proof_constructors` fields when
building `GenericCommand::Sort`, so internal symbols can survive serialization
and parsing. Update the same `map_string_symbols`/`fun` transformation used for
`name`, `uf`, and `proof_func` to also map the symbol data inside
`container_rebuild` and `proof_constructors`, keeping the desugared sort command
round-trippable.

---

Nitpick comments:
In `@egglog/core-relations/src/hash_index/mod.rs`:
- Around line 584-613: The sorted-order contract for build_subsets_from_sorted
is only implied today, but SparseColumnIndex::get_subset’s unsafe path depends
on it. Add a debug-only assertion at the start of build_subsets_from_sorted that
verifies pairs are sorted by (Value, RowId) and contain no duplicate (Value,
RowId) entries, so any future caller violating the invariant fails fast before
reaching get_subset. Keep the check local to build_subsets_from_sorted and
reference the existing precondition in its documentation.

In `@egglog/scripts/requirements.txt`:
- Line 1: The eval-live dependency is using an unpinned git reference, so update
the requirements entry to use a specific commit hash instead of the floating
branch head. Make this change in the requirements entry for eval-live in the
dependency list, and keep the package name and git URL the same while adding the
commit-specific pin for reproducible nightly runs.

In `@egglog/src/proofs/proof_container_rebuild.rs`:
- Around line 277-368: The trailing reflexive anchor in
rebuild_container_proof_rec duplicates the outer-level proof row already emitted
by proof_encoding.rs::rebuilding_rules, so adjust the anchoring logic to skip
inserting the cproof row for the top-level container while keeping it for nested
container recursion. Keep the existing proof construction in
rebuild_container_proof_rec, but gate the final sym/trans/cproof insert path so
only recursive inner container rebuilds mint the anchor, using the existing
symbols rebuild_container_proof_rec, cproof_action, sym_action, and trans_action
to locate the change.
🪄 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: 71e2198d-e07d-4f49-96d1-eb6136cbff73

📥 Commits

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

⛔ Files ignored due to path filters (7)
  • egglog-experimental/tests/fixtures/eggcc-2mm-pass1-merge-old.egg is excluded by !**/*.egg
  • egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap is excluded by !**/*.snap
  • egglog/tests/container-proofs.egg is excluded by !**/*.egg
  • egglog/tests/proofs/container-set-collapse.egg is excluded by !**/*.egg
  • egglog/tests/snapshots/files__proof_unsupported_files.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_container_proofs.snap is excluded by !**/*.snap
  • egglog/tests/snapshots/files__shared_snapshot_container_set_collapse.snap is excluded by !**/*.snap
📒 Files selected for processing (48)
  • egglog-experimental/src/container_primitives.rs
  • egglog-experimental/src/either.rs
  • egglog-experimental/src/lib.rs
  • egglog-experimental/src/main.rs
  • egglog-experimental/src/maybe.rs
  • egglog-experimental/src/set_cost.rs
  • egglog-experimental/tests/eggcc_2mm_proof.rs
  • egglog-experimental/tests/files.rs
  • egglog/.gitignore
  • egglog/CHANGELOG.md
  • egglog/Makefile
  • egglog/core-relations/src/containers/mod.rs
  • egglog/core-relations/src/containers/tests.rs
  • egglog/core-relations/src/hash_index/mod.rs
  • egglog/core-relations/src/hash_index/tests.rs
  • egglog/core-relations/src/lib.rs
  • egglog/core-relations/src/table_spec.rs
  • egglog/core-relations/src/uf/mod.rs
  • egglog/egglog-bridge/src/tests.rs
  • egglog/scripts/nightly_bench.py
  • egglog/scripts/requirements.txt
  • egglog/src/ast/desugar.rs
  • egglog/src/ast/mod.rs
  • egglog/src/ast/parse.rs
  • egglog/src/lib.rs
  • egglog/src/prelude.rs
  • egglog/src/proofs/mod.rs
  • egglog/src/proofs/proof_checker.rs
  • egglog/src/proofs/proof_container_rebuild.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/proofs/proof_format.rs
  • egglog/src/proofs/proof_normal_form.rs
  • egglog/src/proofs/proof_simplification.rs
  • egglog/src/proofs/proof_tests.rs
  • egglog/src/scheduler.rs
  • egglog/src/sort/fn.rs
  • egglog/src/sort/map.rs
  • egglog/src/sort/mod.rs
  • egglog/src/sort/multiset.rs
  • egglog/src/sort/pair.rs
  • egglog/src/sort/set.rs
  • egglog/src/sort/vec.rs
  • egglog/src/termdag.rs
  • egglog/src/typechecking.rs
  • egglog/tests/container_rebuild.rs

Comment on lines +4 to +7
use egglog::{
ArcSort, ContainerValue, EGraph, TermDag, TermId, TypeError, TypeInfo, Value,
add_primitive_with_validator,
};

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
# Confirm Term is used but not imported in either.rs
echo "--- imports ---"; rg -nP 'use egglog::\{' -A3 egglog-experimental/src/either.rs
echo "--- Term usages ---"; rg -n 'Term::' egglog-experimental/src/either.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 552


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Map the file structure and inspect the surrounding context for any local `Term` definition or wildcard import.
ast-grep outline egglog-experimental/src/either.rs --view expanded || true

echo "--- nearby source around Term usages ---"
sed -n '1,260p' egglog-experimental/src/either.rs | nl -ba | sed -n '1,240p'

Repository: saulshanabrook/egglog-encoding

Length of output: 1420


Add Term to the import list. Term::App is used in the validator closures below, but egglog::Term is not imported here, so this file won’t compile.

🤖 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-experimental/src/either.rs` around lines 4 - 7, The import list in
either.rs is missing Term, which is needed by the validator closures that
reference Term::App. Update the top-level egglog import used near
add_primitive_with_validator to include Term so the Either-related validator
code compiles without unresolved symbol errors.

Comment on lines +63 to +81
fn make_sort(
typeinfo: &mut TypeInfo,
name: String,
args: &[Expr],
) -> Result<ArcSort, TypeError> {
if let [Expr::Var(span, element)] = args {
let element = typeinfo
.get_sort_by_name(element)
.ok_or(TypeError::UndefinedSort(element.clone(), span.clone()))?;

Ok(Self {
name,
element: element.clone(),
}
.to_arcsort())
} else {
panic!("Maybe sort requires exactly one argument")
}
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🩺 Stability & Availability | 🟡 Minor | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
# Check whether presort arity is validated before make_sort is called, and how other presorts handle wrong arity.
rg -nP 'fn make_sort' -A15 egglog/src/sort/ egglog-experimental/src/
rg -nP 'add_presort|make_sort\s*\(' -n egglog/src/typechecking.rs egglog/src/sort/mod.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 9241


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Inspect the presort registration path and the relevant make_sort implementations.
sed -n '620,760p' egglog/src/typechecking.rs
echo '---'
sed -n '1,220p' egglog/src/sort/mod.rs
echo '---'
sed -n '1,180p' egglog-experimental/src/maybe.rs
echo '---'
sed -n '1,180p' egglog-experimental/src/either.rs
echo '---'
sed -n '1,180p' egglog/src/sort/vec.rs
echo '---'
sed -n '1,180p' egglog/src/sort/set.rs
echo '---'
sed -n '1,180p' egglog/src/sort/multiset.rs
echo '---'
sed -n '1,180p' egglog/src/sort/map.rs
echo '---'
sed -n '1,180p' egglog/src/sort/pair.rs
echo '---'
sed -n '1,180p' egglog/src/sort/fn.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 50386


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Find where presort constructors are invoked and whether arg arity is validated beforehand.
rg -n "mksorts|make_sort\(|Presort" egglog/src egglog-experimental/src
echo '---'
sed -n '1,260p' egglog/src/typechecking.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 10918


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Inspect the sort declaration parsing / resolution path to see whether arg arity is constrained upstream.
sed -n '220,280p' egglog/src/typechecking.rs
echo '---'
rg -n "declare_sort\(" egglog/src egglog-experimental/src
echo '---'
rg -n "presort_and_args|Sort.*args|sort .*\\(" egglog/src egglog-ast/src egglog-experimental/src

Repository: saulshanabrook/egglog-encoding

Length of output: 15139


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Inspect parser handling of sort/presort arguments and any arity checks.
sed -n '260,420p' egglog/src/ast/parse.rs
echo '---'
sed -n '1000,1060p' egglog/src/ast/mod.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 10765


Return TypeError instead of panicking on invalid sort arity.
MaybeSort::make_sort (and EitherSort::make_sort) panic on malformed (sort ...) input, and container args are forwarded straight through, so bad user input can crash typechecking instead of producing a TypeError. Handle the wrong-arity case here and return an error.

🤖 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-experimental/src/maybe.rs` around lines 63 - 81,
`MaybeSort::make_sort` currently panics when the sort arguments don’t match the
expected shape, so malformed input can crash typechecking instead of returning a
`TypeError`. Update the arity handling in `make_sort` to validate the incoming
`args` and return an appropriate error for invalid container arity rather than
panicking, and apply the same fix to `EitherSort::make_sort` so both sort
constructors fail gracefully on bad user input.

Comment thread egglog/scripts/nightly_bench.py
Comment thread egglog/src/ast/mod.rs
Comment on lines +1678 to +1688
container_rebuild,
proof_constructors,
unionable,
} => GenericCommand::Sort {
span,
name: fun(name),
presort_and_args,
uf: uf.map(&mut *fun),
uf: uf.map(|(ctor, index)| (fun(ctor), index.map(&mut *fun))),
proof_func: proof_func.map(&mut *fun),
container_rebuild,
proof_constructors,

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
# Inspect sanitize_internal_symbols and how it uses map_string_symbols,
# and whether rebuild-prim / proof-constructor names are reserved/renamed.
rg -nP -C4 'fn sanitize_internal_symbols' egglog/src
rg -nP -C3 'map_string_symbols' egglog/src
# Where are internal_rebuild_prim / proof constructor names generated?
rg -nP -C3 'internal_rebuild_prim|internal_rebuild_proof_prim' egglog/src
rg -nP -C3 'congr_constructor|container_normalize_constructor|eq_trans_constructor|eq_sym_constructor' egglog/src

Repository: saulshanabrook/egglog-encoding

Length of output: 26720


🏁 Script executed:

#!/bin/bash
sed -n '1660,1705p' egglog/src/ast/mod.rs
printf '\n---\n'
sed -n '2136,2170p' egglog/src/ast/mod.rs
printf '\n---\n'
sed -n '1,120p' egglog/src/proofs/proof_container_rebuild.rs
printf '\n---\n'
sed -n '1,120p' egglog/src/proofs/proof_format.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 13412


🏁 Script executed:

#!/bin/bash
rg -n -C3 'INTERNAL_SYMBOL_PREFIX|sanitize_internal_symbols|replace_internal_symbol_with|ContainerRebuildSpec|proof_constructors|container_rebuild' egglog/src
printf '\n---\n'
sed -n '1,120p' egglog/src/ast/mod.rs
printf '\n---\n'
sed -n '440,500p' egglog/src/typechecking.rs
printf '\n---\n'
sed -n '1600,1645p' egglog/src/lib.rs

Repository: saulshanabrook/egglog-encoding

Length of output: 50386


Map container_rebuild and proof_constructors here too
replace_internal_symbol_with runs through map_string_symbols, and these annotations are serialized on (sort ...) and read back during parse/typecheck. Leaving them untouched can preserve stale internal names and break round-tripping of the desugared program.

🤖 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/ast/mod.rs` around lines 1678 - 1688, The
`replace_internal_symbol_with` path in `ast::mod` is not updating the
`container_rebuild` and `proof_constructors` fields when building
`GenericCommand::Sort`, so internal symbols can survive serialization and
parsing. Update the same `map_string_symbols`/`fun` transformation used for
`name`, `uf`, and `proof_func` to also map the symbol data inside
`container_rebuild` and `proof_constructors`, keeping the desugared sort command
round-trippable.

Stacked on the subtree-sync branch. This preserves the final reviewed tree from codex/eggcc-container-benchmark while separating local benchmark, proof, CI, and review-fix changes from the subtree merge commits. The hash index ordering fix from egraphs-good/egglog#914 lives in the subtree-sync branch.
…hmark-updates

Add eggcc container benchmark and proof coverage
@saulshanabrook saulshanabrook enabled auto-merge July 9, 2026 17:38
@saulshanabrook saulshanabrook merged commit a2d88ce into main Jul 9, 2026
5 of 6 checks passed
@saulshanabrook saulshanabrook deleted the codex/eggcc-container-subtree-sync branch July 9, 2026 17:45
@coderabbitai

coderabbitai Bot commented Jul 9, 2026

Copy link
Copy Markdown

Caution

Failed to replace (edit) comment. This is likely due to insufficient permissions or the comment being deleted.

Error details
putComment timed out

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants