Proof support for containers

[oflatt]

No description provided.

[codecov-commenter]

Codecov Report

❌ Patch coverage is 81.93956% with 257 lines in your changes missing coverage. Please review.
✅ Project coverage is 86.71%. Comparing base (7e926c6) to head (85ba262).
⚠️ Report is 24 commits behind head on main.

Files with missing lines	Patch %	Lines
src/sort/map.rs	53.28%	64 Missing ⚠️
src/sort/set.rs	39.60%	61 Missing ⚠️
src/proofs/proof_checker.rs	67.82%	37 Missing ⚠️
src/sort/vec.rs	73.68%	15 Missing ⚠️
src/proofs/proof_format.rs	79.10%	14 Missing ⚠️
src/sort/multiset.rs	68.18%	14 Missing ⚠️
src/ast/parse.rs	82.35%	9 Missing ⚠️
src/proofs/proof_encoding.rs	95.58%	9 Missing ⚠️
src/proofs/proof_simplification.rs	66.66%	8 Missing ⚠️
src/sort/pair.rs	73.33%	8 Missing ⚠️
... and 6 more

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #927      +/-   ##
==========================================
- Coverage   86.86%   86.71%   -0.16%     
==========================================
  Files          91       92       +1     
  Lines       27305    28609    +1304     
==========================================
+ Hits        23718    24807    +1089     
- Misses       3587     3802     +215     

☔ 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

✅ 36 untouched benchmarks
🆕 1 new benchmark
⏩ 226 skipped benchmarks¹

Performance Changes

	Mode	Benchmark	BASE	HEAD	Efficiency
🆕	Simulation	tests[proof_testing_repro-665-set-union]	N/A	17.4 s	N/A

---

_{Comparing oflatt:oflatt-container-proofs (85ba262) with main (3960015)²}

Footnotes

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

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

[Copilot]

Pull request overview

Adds end-to-end proof/term-encoding support for built-in container sorts (Vec/Set/Map/MultiSet/Pair) by introducing deterministic container term normalization and container-aware rebuild/proof generation, enabling previously-unsupported programs to participate in proof production and checking.

Changes:

• Add deterministic AST-structural ordering (TermDag::ast_cmp) and shared container canonicalization (normalize_container_term) used by reconstruction, validators, and proof checking.
• Extend proof encoding to rebuild container columns (including nested containers) and introduce a ContainerNormalize proof justification to bridge reorder/merge canonicalization steps.
• Add new container rebuild tests and proof snapshots; update unsupported-proof-file snapshot list and document the feature in the changelog/docs.

Reviewed changes

Copilot reviewed 25 out of 25 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/snapshots/files__shared_snapshot_container_set_collapse.snap	New snapshot covering a proof involving collapsing set normalization.
tests/snapshots/files__proof_unsupported_files.snap	Updates list of files considered unsupported in proof mode (now fewer).
tests/proofs/container-set-collapse.egg	New proof-focused .egg program exercising collapsing set rebuild/normalization.
tests/container_rebuild.rs	New end-to-end Rust tests for container rebuild behavior in term-only and proof modes.
src/typechecking.rs	Registers container rebuild primitives from serialized sort annotations during typechecking.
src/termdag.rs	Adds ast_cmp and normalize_container_term (set/multiset/map canonicalization) plus tests.
src/sort/vec.rs	Adds proof validators for vec term forms (vec-of/vec-empty).
src/sort/set.rs	Adds proof validators and canonical reconstruction for sets via shared normalization.
src/sort/pair.rs	Adds proof validators for pair/pair-first/pair-second.
src/sort/multiset.rs	Adds proof validators and canonical reconstruction for multisets via shared normalization.
src/sort/mod.rs	Adds Sort::rebuild_container_with_leaders hook for value-level container rebuilds.
src/sort/map.rs	Introduces canonical flat (map-of ...) form, validator support, and custom typing for map-of.
src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap	Snapshot update reflecting new UF variable naming in encoded rules.
src/proofs/proof_simplification.rs	Adds simplification to drop redundant ContainerNormalize and updates term mapping logic.
src/proofs/proof_format.rs	Adds ContainerNormalize to proof format parsing/printing and conversion pipeline.
src/proofs/proof_encoding.rs	Implements container rebuild primitives/spec serialization and container-aware rebuild rules in encoding.
src/proofs/proof_encoding.md	Documents container participation in term/proof encoding and normalization mechanism.
src/proofs/proof_encoding_helpers.rs	Extends proof header and proof-encoding support checks to include built-in container presorts.
src/proofs/proof_checker.rs	Adds checker support and a dedicated error for ContainerNormalize proof verification.
src/prelude.rs	Implements generic container rebuild via ContainerValues::rebuild_val_with for container sorts.
src/ast/parse.rs	Parses :internal-container-rebuild option on container sort declarations.
src/ast/mod.rs	Threads container_rebuild through AST commands and ensures it round-trips in formatting.
src/ast/desugar.rs	Propagates container_rebuild field through desugaring paths.
core-relations/src/containers/mod.rs	Adds ContainerValues::rebuild_val_with and a closure-based rebuilder helper.
CHANGELOG.md	Documents new container support in term/proof encoding and associated user-visible extraction changes.

---

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

[saulshanabrook]

Added one last comment and seeing if the AI has anything else useful, since a lot of the term encoding code I didn't look through super carefully: @coderabbitai full review

[coderabbitai]

@saulshanabrook Got it — I'll do a full review of all the changes in this PR, paying extra attention to the term encoding code in src/proofs/proof_encoding.rs, src/proofs/proof_checker.rs, and src/proofs/proof_format.rs since you mentioned those weren't reviewed as carefully.

✅ Action performed

Full review finished.

[coderabbitai]

📝 Walkthrough

Summary by CodeRabbit

• New Features

  • Added container support in proof and term encoding, including canonical handling for vectors, sets, maps, multisets, and pairs.
  • Introduced richer proof support for container normalization and evaluation side conditions.
  • Added canonical map-of handling and improved container rebuild behavior.

• Bug Fixes

  • Improved proof checking for container-related rules and side conditions.
  • Fixed ordering and normalization of extracted container terms.

• Documentation

  • Updated the changelog and proof encoding docs to describe the new container behavior.

Walkthrough

This PR adds container-value support to egglog's term/proof encoding: a new ValueRebuilder trait separates value-level rebuild logic from table-level rebuild logic, container sorts gain rebuild/proof primitives, AST/typechecking track container-rebuild specs and proof constructor names, container terms (map/set/multiset/pair/vec) get canonical normalization forms, and proof checking/simplification handle new ContainerNormalize/Eval justifications.

Changes

Container rebuild and proof encoding

Layer / File(s)	Summary
ValueRebuilder trait split core-relations/src/table_spec.rs, core-relations/src/containers/mod.rs, core-relations/src/uf/mod.rs, core-relations/src/lib.rs, core-relations/src/containers/tests.rs, egglog-bridge/src/tests.rs, src/sort/mod.rs, src/sort/{fn,map,set,multiset,pair,vec}.rs	A new ValueRebuilder trait provides rebuild_val/rebuild_slice; Rebuilder now extends it. ContainerValue::rebuild_contents and all container sort implementations switch to &dyn ValueRebuilder. Adds ContainerValues::rebuild_val_with, DynamicContainerEnv::rebuild_val_with, and a private ClosureRebuilder.
AST/parse schema and desugar wiring src/ast/mod.rs, src/ast/parse.rs, src/ast/desugar.rs, src/prelude.rs	Adds ContainerRebuildSpec and ProofConstructorNames; Sort command variants gain container_rebuild/proof_constructors fields and a richer uf shape. Parsing, display, and symbol-mapping utilities are updated; desugar paths populate the new fields with None.
Typechecking wiring and rebuild primitives src/typechecking.rs, src/proofs/mod.rs, src/proofs/proof_container_rebuild.rs, src/proofs/proof_encoding.md, src/lib.rs, src/prelude.rs	Typechecking records UF/proof-constructor state and registers container rebuild primitives; a new module implements per-container rebuild and rebuild-proof primitives; run_command restores this state; ContainerSort gains a rebuild_container_normalizer hook.
Encoding rebuild rules and instrumentation src/proofs/proof_encoding.rs, src/proofs/proof_encoding_helpers.rs, src/proofs/proof_extraction.rs	declare_sort/rebuilding_rules handle container columns and congruence proof chaining; EncodingNames gains container-normalize/eval constructors; encoding-support checks reject containers created in query but used in actions; existence proofs pass container normalizers.
Proof checking/format/simplification/normal form src/proofs/proof_checker.rs, src/proofs/proof_format.rs, src/proofs/proof_simplification.rs, src/proofs/proof_normal_form.rs, src/proofs/proof_tests.rs	Adds ContainerNormalize/Eval justification handling, side-condition checking, exact-head proof parsing, redundant-normalization elimination, and lifting of container-producing primitives into side conditions.
Container sort normalization src/sort/map.rs, src/sort/set.rs, src/sort/multiset.rs, src/sort/pair.rs, src/sort/vec.rs	Adds canonical term conversion helpers (map-of, set-of, multiset-of, pair, vec-of) and switches primitives to validator-backed registration with normalization.
Deterministic term ordering src/termdag.rs, src/lib.rs	Adds OrdTerm and TermDag::ast_cmp/sort_terms_by_ast/ord_term for deterministic structural term comparison.
End-to-end tests and changelog tests/container_rebuild.rs, CHANGELOG.md	Adds integration tests for container rebuild/collapse/normalization across container types in term-encoding and proof modes.

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

Sequence Diagram(s)

sequenceDiagram
  participant Rule
  participant RebuildingRules
  participant ContainerRebuildPrim
  participant UFTable
  participant CSortProofTable
  Rule->>RebuildingRules: eq_container column update
  RebuildingRules->>ContainerRebuildPrim: rebuild_val_with(remap closure)
  ContainerRebuildPrim->>UFTable: resolve element leaders
  ContainerRebuildPrim-->>RebuildingRules: rebuilt canonical container value
  RebuildingRules->>CSortProofTable: mint Congr/ContainerNormalize proof
  CSortProofTable-->>Rule: reflexive anchor on rebuilt container

Loading

sequenceDiagram
  participant ProofStore
  participant ProofChecker
  participant SideCondition
  participant Term
  ProofStore->>ProofChecker: check_proof_with_context(rule)
  ProofChecker->>SideCondition: is_container_side_condition(fact)
  SideCondition->>Term: eval_side(lhs), eval_side(rhs)
  Term-->>SideCondition: evaluated container values
  SideCondition-->>ProofChecker: extended substitution
  ProofChecker->>ProofChecker: assert_body_proof_normal_form

Loading

Possibly related PRs

• egraphs-good/egglog#941: Both PRs modify the proof-mode prove_exists workflow in src/proofs/proof_extraction.rs.

Suggested labels: status:needs decision

Suggested reviewers: ezrosent

🚥 Pre-merge checks | ✅ 4 | ❌ 1

❌ Failed checks (1 inconclusive)

Check name	Status	Explanation	Resolution
Description check	❓ Inconclusive	No description was provided, so there is no meaningful PR summary to assess.	Add a short description of the container-proof changes and their scope.

✅ Passed checks (4 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly matches the main change: container proof support.
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.

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

[coderabbitai]

Actionable comments posted: 4

Caution

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

⚠️ Outside diff range comments (1)

src/ast/mod.rs (1)

1671-1690: 🗄️ Data Integrity & Integration | 🟠 Major | ⚡ Quick win

container_rebuild/proof_constructors names skipped by map_string_symbols.

uf and proof_func are run through fun (the sanitizer) here, but container_rebuild and proof_constructors are passed straight through unchanged, even though they carry the same kind of internally-generated symbol names (internal_rebuild_prim, internal_rebuild_proof_prim, congr, trans, sym, normalize). Since this function is documented as being used by sanitize_internal_symbols, these fields will retain un-sanitized internal names in output where uf/proof_func would not, which looks like an oversight rather than intentional.

🐛 Suggested fix

             } => GenericCommand::Sort {
                 span,
                 name: fun(name),
                 presort_and_args,
                 uf: uf.map(|(ctor, index)| (fun(ctor), index.map(&mut *fun))),
                 proof_func: proof_func.map(&mut *fun),
-                container_rebuild,
-                proof_constructors,
+                container_rebuild: container_rebuild.map(|spec| ContainerRebuildSpec {
+                    internal_rebuild_prim: fun(spec.internal_rebuild_prim),
+                    internal_rebuild_proof_prim: spec.internal_rebuild_proof_prim.map(&mut *fun),
+                }),
+                proof_constructors: proof_constructors.map(|pc| ProofConstructorNames {
+                    congr: fun(pc.congr),
+                    trans: fun(pc.trans),
+                    sym: fun(pc.sym),
+                    normalize: fun(pc.normalize),
+                }),
                 unionable,
             },

🤖 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 `@src/ast/mod.rs` around lines 1671 - 1690, `map_string_symbols` is skipping
internal symbol sanitization for `GenericCommand::Sort`’s `container_rebuild`
and `proof_constructors` fields while already sanitizing `name`, `uf`, and
`proof_func`. Update the `GenericCommand::Sort` match arm in `src/ast/mod.rs` so
these fields are also passed through the same `fun` sanitizer, preserving
consistency with `sanitize_internal_symbols` and preventing raw internal names
from leaking through.

🤖 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 `@src/sort/set.rs`:
- Around line 148-160: The set-get validator is using a different ordering
source than the runtime path, so it can pick a different element than the actual
primitive. Update the set-get logic around set_get_validator to use the same
ordering as the runtime implementation (the same BTreeSet<Value> ordering used
by set-get at execution), or derive the validator’s result from that shared
order instead of iterating the AST-based BTreeSet<OrdTerm>.

In `@src/termdag.rs`:
- Around line 177-197: `ast_cmp` in `TermDag` still compares `App` nodes
recursively, so deeply nested terms can overflow the stack during `OrdTerm::cmp`
and canonicalization. Update the `ast_cmp` logic to avoid structural recursion
for `App` chains by using an iterative comparison strategy or another bounded
approach, while preserving the existing ordering behavior for `Lit`, `Var`, and
`App` and keeping the comparison entry point in `ast_cmp`/`OrdTerm::cmp`
unchanged.

In `@tests/container_rebuild.rs`:
- Around line 248-273: The comment in set_rebuild_noncollapse_proof_mode is
stale and contradicts the later proof-mode collapse test in the same file.
Update the documentation near set_rebuild_noncollapse_proof_mode and
set_rebuild_collapse_proof_mode to remove the “known limitation” claim or
replace it with the current behavior, so the comments accurately reflect what
EGraph::new_with_proofs().with_proof_testing() now supports.
- Around line 326-349: `set_rebuild_reorder_proof_mode` is duplicating
`set_rebuild_noncollapse_proof_mode` instead of exercising the intended reorder
path. Update the test body in `set_rebuild_reorder_proof_mode` so the program
actually forces a leader to move to a different slot after union/rebuild, using
a distinct `parse_and_run_program` scenario with different element ordering and
a post-union `check` that validates the re-sorted result; if no such scenario is
needed, remove the redundant test.

---

Outside diff comments:
In `@src/ast/mod.rs`:
- Around line 1671-1690: `map_string_symbols` is skipping internal symbol
sanitization for `GenericCommand::Sort`’s `container_rebuild` and
`proof_constructors` fields while already sanitizing `name`, `uf`, and
`proof_func`. Update the `GenericCommand::Sort` match arm in `src/ast/mod.rs` so
these fields are also passed through the same `fun` sanitizer, preserving
consistency with `sanitize_internal_symbols` and preventing raw internal names
from leaking through.

🪄 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

Run ID: ec028ae6-cf07-4e95-a4f5-b4547fc8b1bf

📥 Commits

Reviewing files that changed from the base of the PR and between 7e926c6 and e45cd54.

⛔ Files ignored due to path filters (6)

• src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap is excluded by !**/*.snap
• tests/container-proofs.egg is excluded by !**/*.egg
• tests/proofs/container-set-collapse.egg is excluded by !**/*.egg
• tests/snapshots/files__proof_unsupported_files.snap is excluded by !**/*.snap
• tests/snapshots/files__shared_snapshot_container_proofs.snap is excluded by !**/*.snap
• tests/snapshots/files__shared_snapshot_container_set_collapse.snap is excluded by !**/*.snap

📒 Files selected for processing (33)

• CHANGELOG.md
• core-relations/src/containers/mod.rs
• core-relations/src/containers/tests.rs
• core-relations/src/lib.rs
• core-relations/src/table_spec.rs
• core-relations/src/uf/mod.rs
• egglog-bridge/src/tests.rs
• src/ast/desugar.rs
• src/ast/mod.rs
• src/ast/parse.rs
• src/lib.rs
• src/prelude.rs
• src/proofs/mod.rs
• src/proofs/proof_checker.rs
• src/proofs/proof_container_rebuild.rs
• src/proofs/proof_encoding.md
• src/proofs/proof_encoding.rs
• src/proofs/proof_encoding_helpers.rs
• src/proofs/proof_extraction.rs
• src/proofs/proof_format.rs
• src/proofs/proof_normal_form.rs
• src/proofs/proof_simplification.rs
• src/proofs/proof_tests.rs
• src/sort/fn.rs
• src/sort/map.rs
• src/sort/mod.rs
• src/sort/multiset.rs
• src/sort/pair.rs
• src/sort/set.rs
• src/sort/vec.rs
• src/termdag.rs
• src/typechecking.rs
• tests/container_rebuild.rs

📜 Review details

⚠️ CI failures not shown inline (29)

GitHub Actions: Build / 26_wasm.txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 0_benchmark (ubuntu-latest, math_normal).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 3_benchmark (ubuntu-latest, proof_testing_eqsat-basic).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 4_benchmark (ubuntu-latest, luminal-llama).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 2_benchmark (ubuntu-latest, rectangle).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 5_benchmark (ubuntu-latest, taylor51).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 6_benchmark (ubuntu-latest, conv1d_128).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 8_benchmark (ubuntu-latest, rust_rule_insert_loop).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 7_benchmark (ubuntu-latest, extract-vec-bench).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 9_benchmark (ubuntu-latest, conv1d_32).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 10_benchmark (ubuntu-latest, rust_rule_match_overhead).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 14_benchmark (ubuntu-latest, typeinfer).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 11_benchmark (ubuntu-latest, proof_testing_math).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 15_benchmark (ubuntu-latest, stresstest_large_expr).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 12_benchmark (ubuntu-latest, herbie).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 16_benchmark (ubuntu-latest, rust_rule_match_with_serialize).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 1_benchmark (ubuntu-latest, python_array_optimize).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 19_benchmark (ubuntu-latest, eggcc-extraction).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 17_benchmark (ubuntu-latest, factoring-multisets).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 18_benchmark (ubuntu-latest, cykjson).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 21_benchmark (ubuntu-latest, proof_testing_typecheck).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 20_benchmark (ubuntu-latest, repro-665-set-union).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 23_benchmark (ubuntu-latest, proof_testing_unify).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 24_benchmark (ubuntu-latest, rust_rule_tableaction_hot_path).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 22_benchmark (ubuntu-latest, rust_rule_fib).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 25_benchmark (ubuntu-latest, math-microbenchmark).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 13_benchmark (ubuntu-latest, eggcc-2mm).txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 27_test.txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

---

GitHub Actions: Build / 29_coverage.txt: Proof support for containers

Conclusion: failure

View job details

##[group]Run bail() {
 �[36;1mbail() {�[0m
 �[36;1m  printf '::error::install-action: %s\n' "$*"�[0m

🧰 Additional context used

📓 Path-based instructions (1)

CHANGELOG.md

📄 CodeRabbit inference engine (CLAUDE.md)

Update CHANGELOG.md with a concise bullet when making major changes such as breaking changes or new features.

Files:

• CHANGELOG.md

🧠 Learnings (1)

📚 Learning: 2026-06-07T21:55:12.804Z

Learnt from: saulshanabrook
Repo: egraphs-good/egglog PR: 923
File: src/sort/pair.rs:65-67
Timestamp: 2026-06-07T21:55:12.804Z
Learning: In egglog’s Rust sort implementations, treat `Presort::supports_proof_encoding()` for `PairSort` and `EitherSort` as presort-wide: it must return `true` unconditionally to indicate constructor/projection proof metadata is available regardless of inner sort types. Do not change it to require that all inner fields are eq/container sorts. Instead, control rebuild/canonicalization behavior via the existing gates: use `is_eq_container_sort()` plus per-field rebuild flags (`do_rebuild_first`/`do_rebuild_second` in `PairContainer`, `do_rebuild_left`/`do_rebuild_right` in `EitherContainer`) so mixed-sort instantiations like `(Pair Math i64)` and `(Either Math i64)` are allowed, with rebuild work contributed only by the eq-sort fields.

Applied to files:

• src/sort/pair.rs

🔇 Additional comments (49)

CHANGELOG.md (1)

20-20: LGTM!

tests/container_rebuild.rs (1)

1-401: LGTM! Good coverage across term-only vs. proof-mode pairs for each container sort, exercising collapse/non-collapse and nested cases.

src/termdag.rs (3)

26-63: LGTM!

---

199-210: LGTM!

---

552-579: LGTM!

src/proofs/proof_encoding.rs (6)

13-19: LGTM!

Also applies to: 45-46

---

113-142: LGTM!

Also applies to: 161-207, 217-224

---

561-644: The container rebuild path looks correct: the reflexive anchor Trans(Sym p, p) on rebuilt_var and the per-child Congr(current_proof, i, proof_var) chain compose soundly, and container_proof_bindings are emitted before pf_code so proof_var is bound before use. The multi-column congruence chain also keeps child_index i valid because earlier columns rewrite different indices.

LGTM!

Also applies to: 655-732

---

869-896: 🎯 Functional Correctness | 💤 Low value

Confirm ResolvedFact::to_string() emits re-parseable surface syntax for the side condition.

Unlike the sibling branch (which rebuilds the fact from instrumented sub-expressions), the container side-condition path pushes the raw fact.to_string() back into the encoded program to be re-parsed. This relies on the resolved fact stringifying to valid egglog and on all its argument variables already being bound in the query. The path is exercised by proof_mode_query_constructed_container_not_used_in_action, but please confirm it holds for facts whose container primitive arguments are non-trivial (e.g. nested container primitives already lifted by proof_normal_form).

---

1025-1044: LGTM!

Also applies to: 1147-1173, 1325-1346

---

1496-1550: LGTM!

Also applies to: 1664-1726

src/proofs/proof_encoding_helpers.rs (2)

31-32: LGTM!

Also applies to: 74-75, 371-418

---

455-458: The container-in-query-used-in-action detection correctly scans both (lhs,rhs) orderings and walks action expressions, and the Sort { presort_and_args: Some(_) } arm now accepts genuine container sorts via type_info.get_sort_by_name(name).filter(is_container_sort) — addressing the earlier request to treat all containers as supported.

LGTM!

Also applies to: 591-641

src/proofs/proof_extraction.rs (1)

97-109: Collecting container_normalizers keyed by canonical head is consistent with normalize_container's head-based lookup. Note that two container sorts of the same kind (e.g. Vec over different element types) both yield the head vec-of, so one validator overwrites the other in the map — this is benign because container normalization is purely structural and element-type independent.

LGTM!

src/proofs/proof_checker.rs (3)

23-40: LGTM!

Also applies to: 477-511

---

644-673: The reworked premise loop is sound: working_subst is seeded from substitution (already computed over all non-side-condition facts by compute_rule_substitution), so any variable feeding a side condition's primitive is bound before check_side_condition re-evaluates it, regardless of body order.

LGTM!

---

914-941: ContainerNormalize validates lhs-identity plus rhs-equals-normalized-raw, and Eval correctly errors when reached directly (side conditions are dispatched to check_side_condition, never check_proof). check_side_condition/eval_side/assert_body_proof_normal_form are consistent with the encoder's Eval-marker contract.

LGTM!

Also applies to: 952-1064

src/proofs/proof_format.rs (3)

5-46: LGTM!

Also applies to: 72-108

---

202-306: Switching proof-head dispatch to exact equality against EncodingNames (instead of substring matching) is a meaningful robustness fix, since fresh-gensym'd constructor names could otherwise be substrings of one another.

LGTM!

---

372-384: LGTM!

Also applies to: 407-413, 522-541, 578-583, 754-759, 851-859

src/proofs/proof_normal_form.rs (1)

6-19: The constructor-argument lift correctly targets only container-producing primitives (custom functions and primitives are handled by the earlier arms), and the recursion normalizes inner arguments first, matching assert_body_proof_normal_form's expectations in the checker.

LGTM!

Also applies to: 177-213

src/proofs/proof_simplification.rs (1)

77-152: opt_redundant_container_normalize safely collapses a no-op normalization (outer rhs equals inner rhs, so the inner proof already proves the identical proposition), and map_child_proofs correctly recomputes the proposition via normalize_container after remapping the inner proof.

LGTM!

Also applies to: 330-344, 386-388

src/proofs/proof_tests.rs (1)

5-6: Good coverage: the refactor to a real presort-declared EqContainer sort (registering the primitive on both the egraph and original_typechecking) exercises the actual rebuild-primitive path, and the two new tests cover both the accepted (container not carried into action) and rejected (ContainerCreatedInQueryUsedInAction) cases.

LGTM!

Also applies to: 181-238, 240-301

core-relations/src/table_spec.rs (2)

137-157: LGTM!

---

106-136: 🩺 Stability & Availability

Trait upcasting is fine here &dyn Rebuilder can coerce to &dyn ValueRebuilder, and the workspace toolchain is Rust 1.91.0, so this path compiles as written.

			> Likely an incorrect or invalid review comment.

core-relations/src/lib.rs (1)

43-43: LGTM!

core-relations/src/containers/mod.rs (1)

31-31: LGTM!

Also applies to: 165-189, 290-294, 320-328, 387-399, 787-799

core-relations/src/containers/tests.rs (1)

12-13: LGTM!

Also applies to: 26-26, 44-93

core-relations/src/uf/mod.rs (1)

21-21: LGTM!

Also applies to: 67-77

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

14-14: LGTM!

Also applies to: 452-452

src/sort/fn.rs (1)

57-57: LGTM!

src/sort/multiset.rs (1)

12-45: LGTM!

Also applies to: 148-177, 192-194, 260-272

src/sort/mod.rs (2)

87-95: 📐 Maintainability & Code Quality

Past feedback on this method placement appears unaddressed.

A prior review comment ("inline or move out of sort") suggested reconsidering whether rebuild_container_normalizer belongs on the generic Sort trait. It's still defined here unchanged, duplicating the near-identical method on ContainerSort (see src/prelude.rs's ContainerSort::rebuild_container_normalizer, which ContainerSortImpl forwards into this one). If this was intentionally kept as-is, feel free to disregard.

---

11-11: LGTM!

src/sort/map.rs (2)

122-133: 🎯 Functional Correctness

map-remove still has no proof term-form/validator — prior concern likely still open.

map-remove is registered via plain add_primitive! (Line 260) with no validator, unlike map-empty/map-of/map-insert/map-get/etc. This means any query-body use of map-remove will fail command_supports_proof_encoding's "all primitives have validators" check. This is the same limitation flagged in a previous review ("what's the deal with accepting map-insert + map-of + map-empty but not other map functions?"), which appears to remain unresolved here.

Also applies to: 260-260

---

12-37: LGTM!

Also applies to: 39-91, 196-264, 267-379

src/ast/mod.rs (2)

1009-1051: 🗄️ Data Integrity & Integration

Unresolved: where is container_rebuild actually populated for a sort?

A prior review thread asked exactly this question ("where is :internal-container-rebuild actually written to a sort? ... where did we set this in the code? didn't see it in proof instrumentation") and it doesn't appear resolved within the files in this cohort. The Display arm for presort_and_args: None also silently drops container_rebuild via .., which is fine only if it's guaranteed None in that branch — worth confirming against the writer in typechecking.rs/proof_encoding.rs (not in this review batch).

---

23-54: LGTM!

Also applies to: 91-109, 151-171, 283-301, 603-620, 1943-1971

src/ast/parse.rs (1)

114-138: LGTM!

Also applies to: 289-394

src/ast/desugar.rs (1)

68-78: LGTM!

Also applies to: 90-100, 145-163, 233-248, 290-300, 410-428

src/proofs/mod.rs (1)

2-2: LGTM!

src/proofs/proof_encoding.md (1)

366-416: LGTM!

src/sort/pair.rs (1)

12-12: LGTM!

Also applies to: 31-51, 143-170, 184-187

src/sort/set.rs (1)

11-11: LGTM!

Also applies to: 26-49, 161-251, 261-272

src/sort/vec.rs (1)

14-14: LGTM!

Also applies to: 38-56, 136-191, 235-244

src/prelude.rs (1)

761-762: LGTM!

Also applies to: 918-925, 996-999

src/typechecking.rs (1)

4-4: LGTM!

Also applies to: 419-474

src/proofs/proof_container_rebuild.rs (1)

1-368: LGTM!

src/lib.rs (1)

73-73: LGTM!

Also applies to: 1592-1620, 1973-1976, 2963-3020