Proof optimization- consolidate proof and view/UF tables#850
Proof optimization- consolidate proof and view/UF tables#850
Conversation
There was a problem hiding this comment.
Pull request overview
This PR speeds up proof execution by consolidating proof-related tables (UF + view proof) into fewer function-backed tables, and introduces a built-in Pair container sort to bundle related values (e.g., UF leader + proof) for more efficient lookups.
Changes:
- Consolidate UF + view proof storage by making UF and view tables function-backed and storing proofs in the function output column (or
Unitwhen proofs are disabled). - Add a
Paircontainer sort plus primitives (pair,pair-first,pair-second) and use it for proof-mode UF indexing. - Extend parsing/AST/desugaring/extraction to support
:term-constructorand:unextractableonfunction, update subsumption/extraction logic accordingly, and add seminaive “skip focus atom” support inegglog-bridge.
Reviewed changes
Copilot reviewed 20 out of 20 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
src/proofs/proof_encoding.rs |
Main consolidation of UF/view tables into functions; UF index now returns Pair(leader, proof) in proof mode. |
src/proofs/proof_encoding_helpers.rs |
Removes separate UF/view proof-name maps; adds UF pair sort naming + proof_type_str(). |
src/proofs/proof_encoding.md |
Updates documentation to reflect function-backed UF/view tables and proof storage semantics. |
src/sort/pair.rs |
New Pair container sort implementation and primitives. |
src/sort/mod.rs, src/lib.rs |
Wires PairSort into the default EGraph and enables subsumption for view functions (term_constructor). |
src/ast/parse.rs, src/ast/mod.rs, src/ast/desugar.rs |
Adds :term-constructor/:unextractable to function syntax and propagates metadata. |
src/extract.rs |
Allows extracting from functions with term_constructor (view tables), with options to skip them for proof extraction. |
egglog-bridge/src/rule.rs |
Adds skip_seminaive support and public APIs to control seminaive variant generation. |
tests/integration_test.rs, tests/pair.egg, snapshots |
Adds coverage for constructor option rejection and new Pair behavior; updates snapshots for new printed forms. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| } | ||
| // View is always a function (returning Proof or Unit), with :merge old | ||
| let proof_type = self.proof_type_str().to_string(); | ||
| let mut view_flags = String::new(); |
There was a problem hiding this comment.
fdecl.cost is only propagated to the hidden/unextractable term constructor (line 472), but the extractable view table is now a function (lines 453–467) and cannot carry :cost. Since extraction now uses view tables (functions with term_constructor) for user-facing extraction, this makes any user-specified constructor costs effectively ignored (all view rows fall back to the default cost). Consider adding :cost support for function, or teaching extraction to use the referenced term_constructor's cost when term_constructor.is_some().
| let mut view_flags = String::new(); | |
| let mut view_flags = String::new(); | |
| if let Some(cost) = fdecl.cost { | |
| view_flags.push_str(&format!(" :cost {cost}")); | |
| } |
There was a problem hiding this comment.
ah this is a real problem
| 'outer: for focus_atom in 0..self.atoms.len() { | ||
| if self.skip_seminaive.contains(&focus_atom) { | ||
| continue; | ||
| } | ||
| for (i, (_, _, schema_info)) in self.atoms.iter().enumerate() { |
There was a problem hiding this comment.
skip_seminaive is a Vec<usize> and this loop calls contains() inside the seminaive variant generation (including in the nested atom loop). This turns seminaive rule construction into extra O(atoms * skipped) scans and can become noticeable for large rulesets. Consider representing skip_seminaive as a FixedBitSet/Vec<bool> (indexed by atom) or dedup/sort once and use binary search.
There was a problem hiding this comment.
hmm this shouldn't be here anymore
There was a problem hiding this comment.
we should rip out the changes in this file
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #850 +/- ##
==========================================
- Coverage 86.26% 86.19% -0.08%
==========================================
Files 85 86 +1
Lines 23262 23348 +86
==========================================
+ Hits 20067 20124 +57
- Misses 3195 3224 +29 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Merging this PR will improve performance by 43.49%
|
| Mode | Benchmark | BASE |
HEAD |
Efficiency | |
|---|---|---|---|---|---|
| ⚡ | WallTime | tests[proof_testing_unify] |
22.1 ms | 18 ms | +23.01% |
| ⚡ | WallTime | tests[proof_testing_eqsat-basic] |
35.7 ms | 26.2 ms | +36.08% |
| ⚡ | WallTime | tests[proof_testing_typecheck] |
238.1 ms | 165.9 ms | +43.49% |
| ⚡ | Simulation | tests[proof_testing_unify] |
20.4 ms | 15.7 ms | +29.62% |
| ⚡ | Simulation | tests[proof_testing_eqsat-basic] |
34 ms | 24.6 ms | +38.18% |
| ⚡ | Simulation | tests[proof_testing_typecheck] |
218.4 ms | 153.6 ms | +42.22% |
Comparing oflatt-proof-optimization (ef00588) with main (b27cd22)
Footnotes
-
190 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. ↩
| (sort __view) | ||
| (constructor Add (i64 i64) Math :unextractable :internal-hidden) | ||
| (constructor __AddView (i64 i64 Math) __view :term-constructor Add) | ||
| (function __AddView (i64 i64 Math) Unit :merge old :term-constructor Add) |
There was a problem hiding this comment.
Just curious, why do we need merge old here? Shouldn't any two units be the same value so the default merge function of assert equality should be fine?
This PR makes proofs twice as fast by consolidating tables, also resulting in a negative diff in the core proof instrumentation