Add proof support for Pair and Either containers#923
Closed
saulshanabrook wants to merge 6 commits into
Closed
Conversation
Member
Author
|
@coderabbitai full review |
Contributor
✅ Action performedFull review finished. |
Merging this PR will not alter performance
Comparing 
Footnotes
|
Contributor
📝 WalkthroughWalkthroughAdds proof-mode support for fixed-shape container sorts (Pair and Either): container proof metadata and hooks, Either implementation and Pair updates, generalized proof-view congruence/rebuild encoding, instrumentation for container constructors/projections, and integration with typechecking and presort registration. ChangesContainer Proof Support
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Suggested labels
Suggested reviewers
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
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. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
src/proofs/proof_encoding_helpers.rs (1)
551-565:⚠️ Potential issue | 🟠 Major | ⚡ Quick winDon't let proof-capable presorts bypass reserved sort-annotation checks.
Line 554 returns
Ok(())for supported presorts before Lines 559-565 reject user-specifieduf/proof_funcannotations. That means aPair/Eithersort can now slip through with internal annotations that the encoder assumes it owns, which breaks the sort-command contract for proof mode.Suggested fix
- GenericCommand::Sort { - presort_and_args: Some((presort, _)), - .. - } if type_info.presort_supports_proof_encoding(presort) => Ok(()), - GenericCommand::Sort { - presort_and_args: Some(_), - .. - } => Err(ProofEncodingUnsupportedReason::SortWithPresort), GenericCommand::Sort { uf: Some(_), .. } => { Err(ProofEncodingUnsupportedReason::SortWithUfAnnotation) } GenericCommand::Sort { proof_func: Some(_), .. } => Err(ProofEncodingUnsupportedReason::SortWithProofFuncAnnotation), + GenericCommand::Sort { + presort_and_args: Some((presort, _)), + .. + } if type_info.presort_supports_proof_encoding(presort) => Ok(()), + GenericCommand::Sort { + presort_and_args: Some(_), + .. + } => Err(ProofEncodingUnsupportedReason::SortWithPresort),🤖 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/proofs/proof_encoding_helpers.rs` around lines 551 - 565, The match arm for GenericCommand::Sort currently returns Ok(()) when presort_and_args: Some((presort, _)) and type_info.presort_supports_proof_encoding(presort) is true, which short-circuits later checks that reject user-provided uf or proof_func annotations; update the logic so that even when a presort is proof-capable you still verify that uf and proof_func are None before accepting the sort. Concretely, in the GenericCommand::Sort handling (presort_and_args, presort, type_info.presort_supports_proof_encoding, uf, proof_func, and the ProofEncodingUnsupportedReason variants SortWithUfAnnotation and SortWithProofFuncAnnotation), ensure you check uf and proof_func first (or add an additional guard) and return the appropriate Err if they are present, only returning Ok(()) if no user annotations exist.
🤖 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/proofs/proof_encoding.rs`:
- Around line 865-899: The projection branch currently drops the container/view
justification and arg_proofs[0] and returns only proof_for_value(selected);
instead, preserve and include the view/query proof and the original container
argument proof when building the returned proof: after calling
self.query_view_and_get_proof(&view_key, &field_vars) append the returned
view/query proof variable (and also ensure arg_proofs[0] is pushed into res)
before calling self.proof_for_value so that the resulting proof chain includes
the container/view justification for the projection; locate this logic around
the projection closure handling (symbols: projection, specialized_primitive,
container_view_key, query_view_and_get_proof, proof_for_value, res, arg_proofs)
and modify the res population and proof creation accordingly.
In `@src/sort/either.rs`:
- Around line 79-101: Replace the panic in make_sort with a Result::Err
returning a TypeError variant so callers can handle the error: instead of
panic!("Either sort requires exactly two arguments"), return
Err(TypeError::InvalidSortArity(name.clone(), args.len())) (or add a new
TypeError variant such as InvalidSortArguments/InvalidSortArity) and construct
the error with the sort name and actual arg count (optionally include spans from
args if your TypeError carries span info); update the TypeError enum to include
that new variant if necessary and use it in make_sort where the arg pattern
fails.
In `@src/sort/mod.rs`:
- Around line 30-47: The projection method on ContainerProofSpec assumes
projection primitive names are unique across all constructors but doesn't
document this; add a doc comment on the ContainerProofSpec::projection method
(or on the ContainerProofSpec type) stating that projection primitive names must
be globally unique within a ContainerProofSpec and that the method returns the
first matching (constructor, projection) pair when duplicates exist, so callers
or implementers must ensure uniqueness or handle ambiguity accordingly
(reference symbols: ContainerProofSpec, projection, constructors, projections,
primitive).
---
Outside diff comments:
In `@src/proofs/proof_encoding_helpers.rs`:
- Around line 551-565: The match arm for GenericCommand::Sort currently returns
Ok(()) when presort_and_args: Some((presort, _)) and
type_info.presort_supports_proof_encoding(presort) is true, which short-circuits
later checks that reject user-provided uf or proof_func annotations; update the
logic so that even when a presort is proof-capable you still verify that uf and
proof_func are None before accepting the sort. Concretely, in the
GenericCommand::Sort handling (presort_and_args, presort,
type_info.presort_supports_proof_encoding, uf, proof_func, and the
ProofEncodingUnsupportedReason variants SortWithUfAnnotation and
SortWithProofFuncAnnotation), ensure you check uf and proof_func first (or add
an additional guard) and return the appropriate Err if they are present, only
returning Ok(()) if no user annotations exist.
🪄 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: 20f07def-05ca-40d3-93c4-a039e88527cf
⛔ Files ignored due to path filters (8)
tests/proofs/either-proof.eggis excluded by!**/*.eggtests/proofs/either-userland-proof.eggis excluded by!**/*.eggtests/proofs/pair-proof.eggis excluded by!**/*.eggtests/proofs/pair-userland-proof.eggis excluded by!**/*.eggtests/snapshots/files__shared_snapshot_either_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_either_userland_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_pair_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_pair_userland_proof.snapis excluded by!**/*.snap
📒 Files selected for processing (11)
rfcs/001-proof-containers.mdsrc/lib.rssrc/prelude.rssrc/proofs/proof_encoding.rssrc/proofs/proof_encoding_helpers.rssrc/proofs/proof_normal_form.rssrc/sort/either.rssrc/sort/fn.rssrc/sort/mod.rssrc/sort/pair.rssrc/typechecking.rs
📜 Review details
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (16)
- GitHub Check: benchmark (ubuntu-latest, rectangle)
- GitHub Check: benchmark (ubuntu-latest, stresstest_large_expr)
- GitHub Check: benchmark (ubuntu-latest, conv1d_32)
- GitHub Check: benchmark (ubuntu-latest, luminal-llama)
- GitHub Check: benchmark (ubuntu-latest, conv1d_128)
- GitHub Check: benchmark (ubuntu-latest, rust_rule_insert_loop)
- GitHub Check: benchmark (ubuntu-latest, eggcc-2mm)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_typecheck)
- GitHub Check: benchmark (ubuntu-latest, repro-665-set-union)
- GitHub Check: benchmark (ubuntu-latest, herbie)
- GitHub Check: benchmark (ubuntu-latest, taylor51)
- GitHub Check: benchmark (ubuntu-latest, rust_rule_fib)
- GitHub Check: benchmark (ubuntu-latest, factoring-multisets)
- GitHub Check: benchmark (ubuntu-latest, eggcc-extraction)
- GitHub Check: coverage
- 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:
src/lib.rssrc/sort/fn.rssrc/typechecking.rssrc/proofs/proof_encoding_helpers.rssrc/sort/mod.rssrc/prelude.rssrc/proofs/proof_normal_form.rssrc/sort/pair.rsrfcs/001-proof-containers.mdsrc/sort/either.rssrc/proofs/proof_encoding.rs
🧠 Learnings (1)
📚 Learning: 2026-05-31T20:06:45.343Z
Learnt from: saulshanabrook
Repo: egraphs-good/egglog PR: 881
File: src/exec_state.rs:114-129
Timestamp: 2026-05-31T20:06:45.343Z
Learning: In `src/exec_state.rs` (egglog crate, Rust), `Internal::apply_table_function` and related helpers deliberately gate authorization via `self.ctx()` (the stamped call-site context) rather than a per-wrapper capability type check. The potential capability escalation (a less-capable wrapper running under a wider Context invoking wider operations) is intentionally prevented by the experimental call site that prepares and registers primitives, not by a Rust type-level capability guard. The design decision is documented in the `Core::apply_primitive` and `Core::eval_resolved_expr` doc comments rather than enforced structurally. This is an accepted trade-off to keep the PR minimal.
Applied to files:
src/proofs/proof_normal_form.rs
🔇 Additional comments (11)
rfcs/001-proof-containers.md (1)
1-208: LGTM!src/sort/mod.rs (1)
22-68: LGTM!Also applies to: 137-141, 208-212, 94-95
src/prelude.rs (1)
860-862: LGTM!Also applies to: 927-929
src/typechecking.rs (1)
201-201: LGTM!Also applies to: 606-608, 615-617
src/sort/either.rs (5)
1-15: LGTM!
17-58: LGTM!
104-273: LGTM!
317-365: LGTM!
290-315: Verify name-based sort comparison intry_registering_either_matchis safe.
left_fn.inputs()[0].name()/right_fn.inputs()[0].name()/left_fn.output().name()comparisons are sufficient because anEGraphinterns sorts inTypeInfo.sorts: HashMap<String, Arc<dyn Sort>>keyed bysort.name(), andEGraph::add_arcsortrejects duplicates withTypeError::SortAlreadyBound. So two incompatible sorts can’t share the same name in the same graph, making name-equality effectively equivalent to sort identity here.src/lib.rs (1)
420-420: LGTM!src/sort/fn.rs (1)
220-220: LGTM!
Member
Author
|
@coderabbitai full review |
Contributor
✅ Action performedFull review finished. |
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
♻️ Duplicate comments (1)
src/proofs/proof_encoding.rs (1)
865-899:⚠️ Potential issue | 🟠 Major | ⚡ Quick winPreserve the projection/view proof instead of returning only the field proof.
This branch still drops the proof returned by
query_view_and_get_proof(...)and returns onlyproof_for_value(selected). That proves the extracted field value in isolation, but it no longer proves that the matched expression was the projection term being queried, so facts like=(pair-first (pair a b)) xlose the justification that connectspair-first(...)back to the container view and its input proof.🤖 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/proofs/proof_encoding.rs` around lines 865 - 899, The code drops the view proof from query_view_and_get_proof(...) and only returns the field's proof; capture the view proof variable returned by query_view_and_get_proof (instead of _view_proof_var), ensure that that view proof (or its proof variable) is appended to res (or otherwise combined) before calling self.proof_for_value(...) so the resulting proof chain includes both the container/view proof and the extracted field proof; update the tuple binding from let (query, _view_proof_var) = self.query_view_and_get_proof(...) to capture the view proof and include it in res so facts like the projection are justified.
🤖 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/proofs/proof_encoding_helpers.rs`:
- Around line 558-565: The rejection branch for GenericCommand::Sort with
presort_and_args should report that the specific presort does not advertise
proof-encoding support instead of the generic
ProofEncodingUnsupportedReason::SortWithPresort; update the Err returned in the
arm that matches presort_and_args: Some(_) (the arm guarded by
!type_info.presort_supports_proof_encoding) to return a more specific diagnostic
(either a new enum variant like
ProofEncodingUnsupportedReason::PresortNotSupported or include the presort
identifier/name from presort_and_args in the error message) and use
type_info.presort_supports_proof_encoding(presort) and the presort value to
populate the new message so users see which presort lacks support.
In `@src/proofs/proof_normal_form.rs`:
- Around line 121-129: Update the module's documented normal-form invariant to
mention the new exception: when a ResolvedCall::Primitive is recognized by
proof_container_constructor(...) as a container constructor, its call arguments
are intentionally preserved (handled by proof_form_expr and returned as
ResolvedExpr::Call). Find the comment that currently states "primitives cannot
keep constructor/function-call arguments" and revise it to explicitly allow this
container-constructor exception and briefly note proof_container_constructor,
ResolvedCall::Primitive, proof_form_expr, and ResolvedExpr::Call as the relevant
implementation points.
In `@src/sort/either.rs`:
- Around line 36-39: The code is matching self.data (and either.data) by value
which moves the non-Copy EitherData out of a borrowed context; change the
matches in the iter method (impl for Either::iter) and in
ContainerValues::get_val to match on &self.data / &either.data and then copy or
clone the inner Value when returning it (e.g. match &self.data {
EitherData::Left(v) => Some(v.clone()).into_iter(), ... }), ensuring you only
borrow the enum and duplicate the contained Value rather than moving the enum
itself.
In `@src/sort/pair.rs`:
- Around line 61-63: The supports_proof_encoding() implementation in PairSort
currently returns true unconditionally which lets
command_supports_proof_encoding() accept (Pair ...) in proof mode even when
inner sorts are non-eq; update the admission check so proof support is
instance-aware: change supports_proof_encoding() (and the analogous EitherSort
method) to inspect the instantiated inner sorts and return true only when both
inner sorts satisfy is_eq_container_sort() (or otherwise meet the per-sort proof
criteria), or alternatively perform the check inside
command_supports_proof_encoding() by querying the instantiated Pair/Either sort
parameters and rejecting non-eq instantiations during typechecking/proof-mode
admission.
---
Duplicate comments:
In `@src/proofs/proof_encoding.rs`:
- Around line 865-899: The code drops the view proof from
query_view_and_get_proof(...) and only returns the field's proof; capture the
view proof variable returned by query_view_and_get_proof (instead of
_view_proof_var), ensure that that view proof (or its proof variable) is
appended to res (or otherwise combined) before calling self.proof_for_value(...)
so the resulting proof chain includes both the container/view proof and the
extracted field proof; update the tuple binding from let (query,
_view_proof_var) = self.query_view_and_get_proof(...) to capture the view proof
and include it in res so facts like the projection are justified.
🪄 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: a6eca469-f7cf-4a2a-bfdd-538fb204e6fb
⛔ Files ignored due to path filters (10)
tests/fail-typecheck/either-invalid-arity.eggis excluded by!**/*.eggtests/proofs/either-proof.eggis excluded by!**/*.eggtests/proofs/either-userland-proof.eggis excluded by!**/*.eggtests/proofs/pair-proof.eggis excluded by!**/*.eggtests/proofs/pair-userland-proof.eggis excluded by!**/*.eggtests/snapshots/files__fail-typecheck__either_invalid_arity.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_either_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_either_userland_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_pair_proof.snapis excluded by!**/*.snaptests/snapshots/files__shared_snapshot_pair_userland_proof.snapis excluded by!**/*.snap
📒 Files selected for processing (11)
rfcs/001-proof-containers.mdsrc/lib.rssrc/prelude.rssrc/proofs/proof_encoding.rssrc/proofs/proof_encoding_helpers.rssrc/proofs/proof_normal_form.rssrc/sort/either.rssrc/sort/fn.rssrc/sort/mod.rssrc/sort/pair.rssrc/typechecking.rs
📜 Review details
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (20)
- GitHub Check: benchmark (ubuntu-latest, eggcc-2mm)
- GitHub Check: benchmark (ubuntu-latest, rust_rule_match_overhead)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_eqsat-basic)
- GitHub Check: benchmark (ubuntu-latest, typeinfer)
- GitHub Check: benchmark (ubuntu-latest, taylor51)
- GitHub Check: benchmark (ubuntu-latest, rust_rule_insert_loop)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_typecheck)
- GitHub Check: benchmark (ubuntu-latest, conv1d_128)
- GitHub Check: benchmark (ubuntu-latest, stresstest_large_expr)
- GitHub Check: benchmark (ubuntu-latest, proof_testing_unify)
- GitHub Check: benchmark (ubuntu-latest, cykjson)
- GitHub Check: benchmark (ubuntu-latest, repro-665-set-union)
- GitHub Check: benchmark (ubuntu-latest, luminal-llama)
- GitHub Check: benchmark (ubuntu-latest, python_array_optimize)
- GitHub Check: benchmark (ubuntu-latest, eggcc-extraction)
- GitHub Check: benchmark (ubuntu-latest, herbie)
- GitHub Check: benchmark (ubuntu-latest, math-microbenchmark)
- GitHub Check: benchmark (ubuntu-latest, extract-vec-bench)
- GitHub Check: test
- GitHub Check: coverage
🧰 Additional context used
📓 Path-based instructions (1)
**/*.{md,txt,rs}
📄 CodeRabbit inference engine (CLAUDE.md)
Keep documentation concise and avoid duplicate information
Files:
src/lib.rssrc/proofs/proof_normal_form.rssrc/prelude.rssrc/proofs/proof_encoding_helpers.rssrc/sort/fn.rssrc/sort/pair.rssrc/typechecking.rsrfcs/001-proof-containers.mdsrc/sort/mod.rssrc/sort/either.rssrc/proofs/proof_encoding.rs
🧠 Learnings (1)
📚 Learning: 2026-05-31T20:06:45.343Z
Learnt from: saulshanabrook
Repo: egraphs-good/egglog PR: 881
File: src/exec_state.rs:114-129
Timestamp: 2026-05-31T20:06:45.343Z
Learning: In `src/exec_state.rs` (egglog crate, Rust), `Internal::apply_table_function` and related helpers deliberately gate authorization via `self.ctx()` (the stamped call-site context) rather than a per-wrapper capability type check. The potential capability escalation (a less-capable wrapper running under a wider Context invoking wider operations) is intentionally prevented by the experimental call site that prepares and registers primitives, not by a Rust type-level capability guard. The design decision is documented in the `Core::apply_primitive` and `Core::eval_resolved_expr` doc comments rather than enforced structurally. This is an accepted trade-off to keep the PR minimal.
Applied to files:
src/proofs/proof_normal_form.rs
🪛 LanguageTool
rfcs/001-proof-containers.md
[grammar] ~170-~170: Use a hyphen to join words.
Context: ...s. That would make projection and unwrap proof objects more explicit and would re...
(QB_NEW_EN_HYPHEN)
🔇 Additional comments (4)
rfcs/001-proof-containers.md (1)
1-220: LGTM!src/sort/mod.rs (1)
22-73: LGTM!Also applies to: 98-99, 141-145, 212-216
src/prelude.rs (1)
860-862: LGTM!Also applies to: 927-929
src/typechecking.rs (1)
201-201: LGTM!Also applies to: 606-608, 615-617, 1132-1137
Member
Author
|
Closing for now. @oflatt suggested we dont want a partial solution that doesn't work for other containers, I aggree |
github-project-automation
Bot
moved this from Waiting for Review
to Done
in Saul Shanabrook
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Context
This is an initial proof-support slice for container-backed values. The motivating path is getting eggcc merge functions working without relying on datatype constructors by adding proof support for the Rust-level containers that those merge functions use.
Related PRs:
Design
This treats a first set of fixed-shape containers as constructor-like at the proof boundary. Pair and the constructor/projection pieces of Either expose metadata describing their proof-level constructor heads and field projections. The proof encoder consumes that metadata generically, rather than hard-coding Pair or Either in proof_encoding.rs.
For supported container constructors, proof instrumentation creates proof-carrying views and rebuild rules in the same spirit as constructor views. Rebuilds preserve enough constructor structure that extracted equality proofs lower to ordinary Congr/Trans/Sym proof terms over pair, either-left, or either-right, matching the shape reviewers would expect from equivalent user-land datatypes.
The branch also adds proof-normal-form handling so supported container constructors can remain constructor-shaped instead of being treated like arbitrary primitives, while projections such as pair-first and either-unwrap-left stay projection operations.
proof_encoding.rsShapeThe largest-looking core diff is in
src/proofs/proof_encoding.rs, because that file is where proof mode lowers user commands into term/view/proof instrumentation. The conceptual change there is intentionally narrow:query_fact_viewfactors the existing view-query/proof-composition path so constructors, custom functions, and container constructor views use the same machinery.proof_container_encodingemits term/view, congruence, and rebuild rules from a genericContainerProofSpecsupplied by the sort.instrument_fact_exprrecognizes container constructor primitives and projection primitives through that metadata, rather than matching on Pair/Either names.So while the file diff is visible, the new behavior is mostly a small set of generic hooks into the existing term/view/rebuild pipeline. The Pair/Either-specific details live in the sort implementations and the RFC/tests, not in proof encoding.
Scope And TBD
This PR covers Pair and the constructor/projection pieces of Either through eq-sort wrapper use cases. Direct non-eq container globals remain out of scope.
The remaining proof-mode work for the eggcc direction is still support for the
(primitive)macro and unstable functions in proofs.