Relations-based term/proof encoding - #22
Merged
Merged
Conversation
Foundation for the relation-based term/proof encoding: - get-fresh! per-sort mint primitive (from the backend id counter) - term tables: constructor -> relation (function ... Unit :no-merge), created via (let fresh (get-fresh!)) (name children fresh) - extraction cost moved off term tables onto views via :internal-cost Terms functionally working (term-mode file tests pass modulo snapshots). Proof constructors still to convert. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- proof-datatype + AST + prooflist constructors -> relations (function ... Unit) - shared mint() helper (get-fresh! + set), returns the fresh var - term_proof_for_justification emits mint sequences, returns proof var Scattered nested proof-construction sites still to flatten. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Every generated nested proof/AST/ProofList expression now builds bottom-up via mint() (get-fresh! + relation assert). format_prooflist emits mints. Term-mode parses/typechecks; proof-mode extraction still to update. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- extract_eq/prove_exists read the minted id from the last input column (is_relation_term / extraction_output_index) - prove-exists expects a function (constructors are lowered to term relations) - fix custom-function merge: bare-var merge result no longer wrapped into a call - container-rebuild proof primitive mints+asserts proof relation rows instead of constructor lookup-or-insert proof_mode_regression: 9/9 green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Introduces per-view set-if-empty + view-proof primitives (proof_fresh.rs) and threads freshly-built constructor terms through set-if-empty so parents build with canonical children, keeping the FD views canonical (nothing for the encoded rebuild to re-key). Term-only mode: validated win on math-microbenchmark — @Rebuilding search+apply 2.67s -> 2.08s (-22%), total 4.45s -> 3.73s (-16%), tuples -10%. No new regressions (term suite 98/2, both pre-existing relation-encoding snapshot regens). Proof mode: canonicalization enabled but WIP. Deduped terms leave orphan term-relation rows (acceptable); the remaining work is bridging the canonical e-class back to a consumer's expected enode form via the view proof (Sym/Trans) in prove-exists / remove_globals. Proof suite currently 151/37. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Implements the plan's natural-term + canonical-term + Congr + set-if-empty threading in add_term_and_view: builds the natural term (children at as-built ids) and canonical term (children at view-deduped ids), connects them with a Congr chain over changed children, dedups via set-if-empty, and records (natural, connector: natural = deduped) in nat_conn for the parent's Congr. Returns the deduped e-class so parents/views stay canonical. Fixes some proof tests (e.g. eqsat_basic). Remaining: the root union still builds its Rule-proof AST from the deduped e-class (whose AST floats to a unioned form), so it must consume the connector (Trans of rule[L=nat] with connector[nat=dedup]); the UF-edge orientation makes that intricate. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The root union now routes its proof through the operands' natural forms (whose ASTs are pinned to the enode the rule built) instead of the deduped e-classes (whose ASTs float once unioned), then orients to the larger=smaller UF edge with proof-of-max/min over a shared natural form. Fixes proof checking for the term-construction plan (the (Neg (Add a (Add b c))) example proves cleanly) and simple rewrites. Remaining: complex/saturating rewrites where the *matched* LHS (a body var, no natural form recorded) has itself been unioned and its AST floats. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…en term The canonical-children term (fv_can) was given a fresh @rule term proof, which the checker validates against the rule head via check_rule_produces_equality. But fv_can is built with *deduped* children, which can extract to a canonicalized shape (a subterm rewritten elsewhere, e.g. matrix's nrows(NamedMat B) -> NamedDim m) that no longer matches the syntactic rule head -> 'rule head doesn't produce claimed equality'. Per the plan, fv_can's proof should be the reflexive Trans(Sym(e-to-e'), e-to-e') derived from the Congr chain, not a @rule -- so it is exempt from the rule-head check and serves as the view's 'eclass = f(children)' proof. The natural term keeps its @rule (its children are the as-matched forms, which do match the head). Fixes matrix/naturals/fibonacci proof-testing; 'rule head' failures 14 -> 2 (remaining: luminal complex rule + pre-existing @p1 custom-merge). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…erms Root cause of the proof-mode canonicalization failures on deeply-nested rules (e.g. matrix, and the constructor parts of luminal/hardboiled_conv1d): instrument_action's Let case bound the let variable to the built term's deduped e-class var but did NOT carry the term's nat_conn entry onto the let name. So a rule like `(let new-e (Bop ...)) (union e new-e)` looked up nat_conn["new-e"], missed, and `union` fell into the no-connector branch: a bare @rule over ordering-max/min(e, new-e) whose endpoint extracts the *deduped* (canonicalized) shape, while process_actions builds the syntactic shape -> "rule head doesn't produce claimed equality". Fix: propagate nat_conn from the result var to the let-bound name. Also keep the natural node *unseeded*: always mint a separate canonical-children node to seed the view (never collapse to seeding fv_nat), so the natural is never pulled into the view's congruence :merge (native UnionId) and stays as-built. Otherwise a birewrite re-keying the view to a differently-shaped partner (IntImm32 x <-> IntImm 32 x) natively merges the natural into the partner and its @rule endpoint extracts the wrong shape. Result: matrix, naturals, fib and all other constructor-based proofs prove cleanly. Remaining: luminal still fails on its `vec-of` container (containers are built with deduped elements and their @rule extracts the canonical shape rather than threading the natural like constructors -- a separate follow-up), and the pre-existing @p1 custom-merge bug is unaffected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The connector-threading fix changed the instrumented proof structure, so all proof-testing snapshots for passing constructor-based proofs are regenerated. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
nat_conn maps an instrumentation unit's freshly-minted vars (and let-bound
names) to their natural id + connector; it is local to a single generated
program. The connector-threading fix keys it by the user's let-variable names,
which repeat across rules, so without resetting it, stale entries leak between
rules/merges and can reference out-of-scope vars ("Unbound symbol @vn"). Clear
nat_conn at the start of each rule, merge function, and global action.
No current test changes result; this prevents cross-unit leaks (which a later
container change would otherwise surface).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Closes luminal's vec-of container proof failure with the container rebuild itself, rather than an action-side connector. A container built over deduped element ids has a term-proof whose endpoint extracts the canonicalized (birewrite-partner) shape instead of the syntactic one -> "rule head doesn't produce claimed equality" for a parent term. Building over the *natural* (as-built) element ids fixes the proof, but naturals have no union-find entry, so the container rebuild can't canonicalize them and the computation breaks. Fix: add a per-eq-sort auxiliary union-find `@UF-Aux-<Sort>` mapping a natural id to its canonical dedup id plus the connector proof `natural = canonical`. The container is built over natural element ids (so the term-proof extracts the syntactic shape); at build time each element's `natural -> (canonical, connector)` edge is written to `UF-Aux`. The Rust container rebuild (`rebuild_container_value_rec` / `rebuild_container_proof_rec`) now consults `UF-Aux` in addition to the main `UF`, chaining `natural ->(UF-Aux)-> canonical ->(UF)-> leader` and composing the connector with the UF proof via `Trans`. So the rebuild canonicalizes the elements and proves it with the existing machinery. `UF-Aux` is written only for container elements. Deterministic table name (`@UF-Aux-<Sort>`) so the rebuild needs no extra plumbing. Natural-element building is applied to `vec-of` only: it makes elements change during rebuild, which triggers the rebuild's per-element `@Congr` fold, and that fold is positional (sound only for ordered containers). Sets/maps keep the deduped path; an order-independent rebuild proof for a birewrite-canonicalized unordered-container element is a follow-up (no current test needs it). Result: luminal (both variants) and all container tests prove cleanly, with no proof-snapshot changes; only the pre-existing @p1 custom-merge failures remain. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Fix the custom-merge (@p1) and lambda evals-to proof-encoding failures by adopting egglog PR #933's children-free merge-proof mechanism while keeping this branch's canonical-id (set-if-empty) encoding. - Proof format/checker: add term-free MergeFnIdx(fn, old, new, idx) and MergeFnRow(fn, old, new) proof variants. The conclusion is reconstructed by evaluating the merge sub-expression (idx = pre-order position) on the premise outputs (subexpr_at_index + run_merge_subexpr), so a :merge action needs neither the function key nor an AST. Adds reflexivize_premise. - Custom-merge encoding: the hidden `current` helper is now 2-column (Out, Proof) for eq-sort/eq-container outputs, carrying the view proof so its :merge builds MergeFnIdx per subterm + MergeFnRow for the row (via add_term_and_view / set-if-empty). No rule-scoped @p1/@p2 in the :merge. - Reflexivize custom-function-fact rule premises: rebuild can rewrite a matched (= (f args) v) premise into a non-reflexive natural->canonical Congr; the checker's function-fact normal form requires a reflexive premise. Proof suite: 180/8 -> 186/2. The 2 remaining (complex_merge_func, rw_analysis proof-testing) fail only on a shared extraction-count snapshot that also differs in term_encoding mode (no proofs) -- a separate pre-existing issue. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adopt egglog PR #933's approach for custom merge functions: the user merge runs once, in the function's FD pair-valued view's own :merge, instead of a separate rebuild rule + a `current` helper table. This eliminates a double-merge (the rule fired on the view-key conflict AND `current`'s :merge fired on the current-key conflict), which minted over-merged extra term rows -- encoded extraction now matches normal mode. Canonical ids (set-if-empty) and the children-free MergeFnIdx/MergeFnRow proofs are unchanged. - Custom-with-merge functions now use the FD pair-valued view (is_fd_view / fd_custom_funcs). `custom_view_merge` runs the merge body once via instrument_merge_body (MergeFnIdx subterm proofs) + a MergeFnRow row proof, with NO @uf union (unlike constructor congruence). - Deleted handle_merge_fn, the `current` helper, the rebuild rule, and the cleanup rules; removed the now-dead Justification::Merge variant. - Added the `select-eq` primitive to keep the FD-view merge's proof column stable (reuse a premise proof when the merge is idempotent) so merges saturate. - Routed the query (instrument_fact), write (add_term_and_view), and rebuild paths to the FD form for custom-with-merge functions. Full files suite green (751 passed); proof-testing 188/0. Regenerated the repro_equal_constant + rw_analysis proof snapshots. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Groundwork for running the relations/proofs encoding on the differential-dataflow backend (egglog-experimental/dd): - Fix the egglog-experimental build (set_cost.rs: add the new `cost` field to its Function commands). - Unify DD's fresh-id minting onto a shared core-relations counter and add an eclass_id_counter() override, so the encoding's `(@get-fresh-<Sort>!)` primitive registers and its ids cannot collide with native FreshId ids. - Add Database::set_counter for the DD merge-rollback path. DD unit tests 34/34, core-relations 54/54; the non-eq-sort DD corpus passes. Full eq-sort support still needs get-fresh!/set-if-empty exposed through the backend SPI (so DD can service them against its host-side mirror) -- follow-up. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The term/proof encoding mints eq-sort ids via `(@get-fresh-<Sort>!)` and canonicalizes constructor terms via `(@set-if-empty-<View>!)`. These were `WritePrim`s that reached into core-relations db tables and were gated on the backend having an `ActionRegistry`, so they only worked on the core-relations reference backend. Expose them as backend operations instead: - Add `Backend::register_get_fresh` / `register_set_if_empty` / `register_view_proof`. `register_get_fresh` has a uniform default minting from the backend's eq-class id counter; the other two default to a loud panic and are overridden per backend. - The reference backend (egglog-bridge) implements set-if-empty/view-proof over its tables (behavior-preserving). The differential-dataflow backend implements them over its host-side `mirror` (intercepted in both `apply_head` and inside a view's `:merge` transaction). - Route the encoder's primitives (proof_fresh.rs) through the SPI via a new `add_backend_op_primitive`, dropping the `action_registry()` gate for these three ops (retained for genuine registry reads, still unsupported on DD). Reference backend: full `files` suite 756/0 (no regressions). DD backend now runs eq-sort programs under term/proof encoding (full DD corpus 131/0; unit 34/34; core-relations 54/54). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Two fixes surfaced while validating the backend/merge work:
- prove_exists panicked ("expected rule justification for existence proof") when
a constructor's witness row had a non-rule existence proof. A valid existence
proof need not be rule-justified (it may be Fiat/Merge/Congr); the rule case is
only an optimization to strip a single-premise wrapping rule. Use the proof
as-is otherwise (check_proof still validates it). This was order-dependent: the
witness is a constructor's first row, so a backend iterating rows in a different
order (the differential-dataflow backend's HashSet mirror) surfaced a non-rule
row and panicked nondeterministically. It also fixed container_rebuild (4 tests
hit it deterministically on the reference backend: container witnesses have
ContainerNormalize/Congr existence proofs) -> container_rebuild 16/0.
- Custom-with-merge FD views with an eq-sort output now canonicalize the output
column when it is unioned to a smaller leader, via delete+set (re-setting the
same key would re-run the user merge). Without this, a custom eq-sort output
later unioned stayed non-canonical and `check` could miss it. (This block was
authored during the merge re-architecture but landed after that commit.)
files suite 756/0; container_rebuild 16/0.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Replace the per-sort `@get-fresh-<Sort>!` mint primitives with one generic `get-fresh!` that takes the target sort as a string literal: `(get-fresh! "Math")`. Its runtime ignores the arg (the shared eq-class id counter is sort-agnostic); the string only types the output. This gives the desugared program a stable, always-registered name instead of per-sort fresh names that a name-sanitizer mangles on re-parse (so a plain e-graph can re-parse encoded output). The type constraint has dual behavior: at type-check time it reads the string literal and assigns the output eq-sort; at resolution/`accept` time (which runs constraints over placeholder int literals, not the real string) it just requires the first arg to be a String, letting the output sort come from the resolved types. Registered once, idempotently, from the first eq-sort declaration. files suite 756/0. (set-if-empty/view-proof are still per-view — a follow-up; the eqsat_basic roundtrip needs those generic too.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
These per-view mint/canonicalize primitives were named `@set-if-empty-<view>!` and `@view-proof-<view>`. The `@` is an internal-symbol marker, so a name sanitizer (e.g. the term-encoding roundtrip test) rewrites it — but the primitive is re-registered by re-deriving the name with the `@` intact, so the sanitized reference (`___set-if-empty-...`) no longer resolves to the registered `@set-if-empty-...`, and re-parsing the desugared program fails with UnboundFunction. Drop the `@`: the stable `set-if-empty-`/`view-proof-` prefix now carries no marker (so the sanitizer leaves it alone), while the embedded view name — a fresh internal symbol — is rewritten identically at both the reference and the re-registration, so the primitive stays resolvable. This restores self-containedness of the desugared program (a plain e-graph can re-parse it). Fixes eqsat_basic_term_encoding_roundtrip. files 756/0, integration_test 48/0, container_rebuild 16/0, proof_mode_regression 9/0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…lobals) In proof/term mode, `(input …)` lowered to one top-level fiat action per CSV row, and term-encoding expanded each into ~40 top-level `(let @v …)` globals. `proof_global_remover` turns every global into its own Constructor function, so loading N input facts created ~O(N) functions and ran ~O(N) one-shot rules — super-linear in practice (pointer-analysis proofs: ~9.2s, 380 MiB peak). Now each `(input …)` lowers, for execution, to a single bodyless rule whose head holds all rows' fiat actions, run once. The mints become local rule-head lets, so no per-mint function is created and the input loads in one rule execution. The head is instrumented with `Fiat`, so proofs are unchanged and no loader rule ever appears in a proof; the proof checker keeps using the per-row top-level form (`desugared_before_proofs`). pointer-analysis-small: reference proofs 9.2s→0.90s, DD proofs 6.3s→1.25s; term and peak RSS also improved. files 756/0, proof_mode_regression 9/0, and the other proof suites stay green; `--proof-testing` passes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
In term/proof mode, `(input …)` now inserts the encoded term/view (and, in proof mode, AST/proof) rows straight into the backend, rather than compiling and running a rule. Adds a small backend SPI — `fresh_eclass_id()` + `add_values(rows)` — serviced by each backend against its own storage (reference-bridge db buffers; the DD host-side mirror, with no fallback). `EGraph::native_input` mints a term id per row and plain-inserts the term relation, FD view, and (proof mode) `@Ast`/`@Fiat`/`@…Proof` rows via `add_values`; duplicate view keys are resolved by the view `:merge`, so there is no get-or-insert. Only constructor-subtype functions take the native path — constructors and relations (which desugar to constructors). Plain custom functions (with or without `:merge`, including `:no-merge` Unit-output ones) still go through the loader rule; `lower_inputs_for_execution` routes by subtype. The proof checker keeps consuming the per-row top-level fiat actions (`desugared_before_proofs`), so proofs are unchanged. pointer-analysis-small proofs: 0.90s→0.098s (reference), 1.25s→0.47s (DD); term 0.17s→0.055s. files 756/0, proof_mode_regression (non-luminal) green, DD corpus unchanged, and `--proof-testing` passes on both backends. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
📝 WalkthroughWalkthroughThe PR adds backend SPI support for shared fresh-id counters, native encoded input loading, ChangesTerm/proof backend integration
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related PRs
Suggested reviewers: 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
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 |
Merging this PR will degrade performance by 47.61%
Warning Please fix the performance issues or acknowledge them on CodSpeed. Performance Changes
Tip Investigate this regression by commenting Comparing 
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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/dd/src/lib.rs`:
- Around line 2401-2413: Update add_values to submit each function/row through
the existing merge-aware transaction path, such as apply_sets, instead of
calling insert_live_row directly. Preserve conversion of each Value to its
representative Row and ensure duplicate keys are collapsed according to the
view’s :merge behavior when loaded.
In `@egglog/src/lib.rs`:
- Around line 2666-2668: Remove the duplicate public zz_report accessor and
reuse the existing get_overall_run_report method at its call sites; if an
accessor is still required, rename it to a meaningful documented API instead of
exposing the zz_ debug-style name.
🪄 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: 21d66595-b5ce-4b83-965d-899c8eeeddb7
⛔ Files ignored due to path filters (30)
Cargo.lockis excluded by!**/*.lockegglog/tests/snapshots/files__proofs__antiunify_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__birewrite_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__calc_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__combinators_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__commute_collapse_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__container_set_collapse_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__fibonacci_demand_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__integer_math_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__intersection_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__matrix_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__merge_during_rebuild_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__naturals_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__path_union_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_define_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_noteqbug_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_small_rebuild_fail_term_encoding_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_typecheck_term_encoding_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__rule_head_fast_path_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__rw_analysis_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__typecheck_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__unify_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__until_proof_testing.snapis excluded by!**/*.snap
📒 Files selected for processing (27)
egglog-experimental/dd/src/interpret.rsegglog-experimental/dd/src/lib.rsegglog-experimental/dd/tests/files.rsegglog-experimental/src/set_cost.rsegglog/CHANGELOG.mdegglog/core-relations/src/free_join/mod.rsegglog/egglog-backend-trait/Cargo.tomlegglog/egglog-backend-trait/src/backend_impl.rsegglog/egglog-backend-trait/src/lib.rsegglog/egglog-bridge/src/lib.rsegglog/src/ast/desugar.rsegglog/src/ast/mod.rsegglog/src/ast/parse.rsegglog/src/extract.rsegglog/src/lib.rsegglog/src/prelude.rsegglog/src/proofs/mod.rsegglog/src/proofs/proof_checker.rsegglog/src/proofs/proof_container_rebuild.rsegglog/src/proofs/proof_encoding.rsegglog/src/proofs/proof_encoding_helpers.rsegglog/src/proofs/proof_extraction.rsegglog/src/proofs/proof_extractor.rsegglog/src/proofs/proof_format.rsegglog/src/proofs/proof_fresh.rsegglog/src/typechecking.rsegglog/tests/proof_mode_regression.rs
…coding Switch the term/proof encoding to the function-style `remove_globals` pass: a global `(let x e)` becomes a nullary `:internal-let` function `set` to its value, instead of a constructor plus a top-level `union`. The global now gets a functional-dependency view and rebuild rules like any other function, and references become the lookup `(x)`. - Encoder: globals are `output_is_eclass` (their output value *is* their e-class, like a constructor), so the term relation has no separate output column and the view is the congruence FD `() -> (eclass, proof)`. Added a global-lookup code path for actions/facts (the one custom lookup proof normal form allows) and a global-`set` path that stores value+proof in the view. - Rebuild: route globals to the constructor-style e-class rebuild (which composes the union edge into the view proof) instead of the custom-output congruence rebuild, which emitted a nonsensical `Congr` on a nullary term and broke proof reconstruction (transitivity middle-term mismatch). - Skip the post-command rebuild after every non-`union` top-level action: a `let`/`set`/insert aliases or dedups under a fresh view key and can't merge e-classes, so N global definitions no longer trigger N rebuilds. Any non-canonical id is fixed by the next real rebuild, as native defers it. - Remove the now-unused `proof_global_remover` pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`Database::merge_all` reset the cached column/key indexes of *every* table and re-summed every table's length on each call, regardless of which tables actually changed. That is O(all tables) per call, and quadratic when many small tables each trigger a merge — e.g. a long run of global-`let` definitions under the term/proof encoding, where each global adds a one-row view table and runs a one-shot action (→ merge_all). A 1600-global proof chain did ~1.1 billion table-index resets. Track the tables modified during the call (the notification list, accumulated here and in `merge_simple`) and reset only those. Unmodified tables keep their valid cached indexes — their table version is unchanged, so `Index::refresh` would be a no-op anyway (same reasoning as `clear_table`). `total_size_estimate` is maintained incrementally at each merge (mirroring `merge_table`) instead of re-summed. Same 1600-global chain now does ~62k resets (~18,000x fewer); proof time roughly halves and the remaining growth is the per-one-shot-action overhead, not merge_all. Correctness: core-relations 51/51, egglog + egglog-experimental suites show no new failures (only pre-existing snapshot diffs), proof-mode file sweep identical to baseline. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ndex `free_external_func` scanned the entire `panic_funcs` map on every call (`retain` looking for the entry whose `id` matches), because the map is keyed by message but freed by id. That scan ran even for non-panic external functions (e.g. the term/proof encoding's `get-fresh!` / `set-if-empty`), and `panic_funcs` grows with the program, so freeing the many short-lived one-shot action rules — one set per encoded global definition, ~38 per global — was O(panic_funcs) each, i.e. quadratic overall. On a 4000-global proof chain this was the dominant cost. Add a reverse `id -> message` index so a free finds its cache entry (or determines the func is not a cached panic) in O(1). The index is a `BTreeMap` so it introduces no new randomly-seeded hasher and leaves the seed sequence — and thus other tables' iteration order, which order-dependent proof extraction reads — unchanged. Perf: 4000-global proof chain 37s -> 12s (on top of the merge_all fix); scaling is now near-linear. Correctness: proof-mode file sweep identical to baseline, `cargo test -p egglog` unchanged (only the 3 pre-existing snapshot diffs). The free/keep semantics are preserved exactly: a cached panic with >1 reference is decremented; its last reference, or any non-cached func, is freed from the db. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
`prove_exists` took whichever row the backend yielded first as the witness, and the root extractor reconstructed from the first matching row. On a backend with nondeterministic row order — the differential-dataflow backend mirrors each relation in a `hashbrown::HashSet`, whose iteration order varies per process — the extracted (always-valid) existence proof therefore varied run to run, so the `*_proof_testing` snapshot tests were flaky (~40% failure independent of any recent change). Select the lexicographically-smallest matching row in both places instead. The proof is unchanged in validity; it is just now the same one every run. This removes the flakiness: the full `egglog-experimental` proof suite is now 46/0 deterministically (was ~40-41 passing with 5-6 flaky). Regenerated the one snapshot (`with_ruleset`) whose stored proof reflected an old nondeterministic witness; its proof still checks (`--proof-testing` passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ncoding Three `proofs::proof_tests` tests were stale after the encoding moved terms and proof constructors from egglog constructors to relations (`get-fresh!` mint + `set-if-empty` view) and globals to function style: - doc_example_add_function1/2: regenerated the encoding snapshots (now show the `(function Add (..) Unit)` term relation, `get-fresh!`/`set-if-empty` minting, and the function-style global) — the intended output, verified by reading the diff. - proof_encoding_hoists_unnamed_rule_name_in_actions: `@Rule` proofs are now emitted as `(set (@rule ..) ())` actions rather than call expressions, so the `visit_exprs` count saw zero. Count the `@Rule` set actions instead; they still reuse the hoisted rule-name variable and there is more than one, so the test's intent is preserved. (The program's proof already checks under `--proof-testing`.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The new corpus file exercises eq-container rebuilds, which need the registry-backed rebuild primitives DD does not service. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The FD-view value-column rebuild only handled eq-sort outputs, so a custom function's container output kept stale elements after unions (native egglog rebuilds them). Add a ValueRebuild::ContainerOutput rule: canonicalize the output with the container rebuild primitive (:naive), delete-then-reinsert the row so the user merge does not rerun, compose the row proof with a Congr at the output position, and anchor the rebuilt container's reflexive <CSort>Proof. On DD this newly emits the registry-backed rebuild primitive for such programs, so repro-querybug3 returns to the known-unsupported list alongside the new corpus file. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Author
Benchmark ReportComparison
6 file(s): math-microbenchmark.egg, eggcc-2mm-pass1.egg, pointer-analysis-small.egg (facts: /home/oflatt/work/egglog1/benchmarks/data/pointer-analysis-small), hardboiled_conv1d_32.egg, luminal-llama.egg, herbie.egg · 6 round(s) per endpoint/file · 300 s timeout per run · Report: /tmp/claude-1004/-home-oflatt-work-egglog1/6e62aa7f-4d6f-433c-8acb-b316f61c744c/scratchpad/reports.jsonl Summary — a453635 main/off vs 1cc0e8a main/off
Ratios are candidate / baseline; below 1 is lower and above 1 is higher. Benchmark ReportComparison
6 file(s): math-microbenchmark.egg, eggcc-2mm-pass1.egg, pointer-analysis-small.egg (facts: /home/oflatt/work/egglog1/benchmarks/data/pointer-analysis-small), hardboiled_conv1d_32.egg, luminal-llama.egg, herbie.egg · 6 round(s) per endpoint/file · 300 s timeout per run · Report: /tmp/claude-1004/-home-oflatt-work-egglog1/6e62aa7f-4d6f-433c-8acb-b316f61c744c/scratchpad/reports.jsonl Summary — a453635 main/term vs 1cc0e8a main/term
Ratios are candidate / baseline; below 1 is lower and above 1 is higher. Benchmark ReportComparison
6 file(s): math-microbenchmark.egg, eggcc-2mm-pass1.egg, pointer-analysis-small.egg (facts: /home/oflatt/work/egglog1/benchmarks/data/pointer-analysis-small), hardboiled_conv1d_32.egg, luminal-llama.egg, herbie.egg · 6 round(s) per endpoint/file · 300 s timeout per run · Report: /tmp/claude-1004/-home-oflatt-work-egglog1/6e62aa7f-4d6f-433c-8acb-b316f61c744c/scratchpad/reports.jsonl Summary — a453635 main/proofs vs 1cc0e8a main/proofs
Ratios are candidate / baseline; below 1 is lower and above 1 is higher. |
The dd crate's output.*.log files are written by (output ...) commands during its corpus tests; untrack and ignore them so test runs stop churning the diff. Reformat egglog-bridge/core-relations to pass the root `cargo fmt --all --check` that CI runs (the egglog-scoped check missed these files). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
This PR overhauls egglog’s term/proof encoding to represent terms and proofs as relations (not constructors), adds backend SPI hooks to support the new mint/canonicalization operations across backends, and introduces native (input …) loading for major proof-mode performance gains.
Changes:
- Re-encode terms/proofs as relation rows with explicit id minting (
get-fresh!) and canonicalization via FD “view” tables (set-if-empty+ view-proof reads). - Load encoded
(input …)facts natively into backend storage (bypassing generated loader rules) and make proof extraction deterministic across nondeterministic row-order backends. - Update proof/container rebuild machinery (including new
CongrAll) and refresh/expand regression + snapshot coverage.
Reviewed changes
Copilot reviewed 75 out of 77 changed files in this pull request and generated 1 comment.
Show a summary per file
| File | Description |
|---|---|
| egglog/tests/snapshots/files__shared_snapshot_custom_container_output_rebuild.snap | New shared snapshot output for custom container rebuild scenario. |
| egglog/tests/snapshots/files__shared_snapshot_container_reorder_proofs.snap | New shared snapshot output for container reorder proof scenarios. |
| egglog/tests/snapshots/files__proofs__until_proof_testing.snap | Updated proof snapshot due to relation-based proof encoding changes. |
| egglog/tests/snapshots/files__proofs__unify_proof_testing.snap | Updated proof snapshot reflecting new proof term shapes. |
| egglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snap | Updated proof snapshot for points-to/unification example under new encoding. |
| egglog/tests/snapshots/files__proofs__rule_head_fast_path_proof_testing.snap | Updated proof snapshot for rule-head fast path under new proof term form. |
| egglog/tests/snapshots/files__proofs__repro_typecheck_term_encoding_proof_testing.snap | Updated proof snapshot for term-encoding typecheck repro. |
| egglog/tests/snapshots/files__proofs__repro_small_rebuild_fail_term_encoding_proof_testing.snap | Updated proof snapshot for small rebuild-failure repro. |
| egglog/tests/snapshots/files__proofs__repro_noteqbug_proof_testing.snap | Updated proof snapshot for noteq bug repro. |
| egglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snap | Updated proof snapshot for equal-constant repro. |
| egglog/tests/snapshots/files__proofs__repro_define_proof_testing.snap | Updated proof snapshot for define repro. |
| egglog/tests/snapshots/files__proofs__path_union_proof_testing.snap | Updated proof snapshot for path/union example (symmetry handling changes). |
| egglog/tests/snapshots/files__proofs__nested_container_dirty_propagation_proof_testing.snap | Updated proof snapshot for nested container dirty propagation. |
| egglog/tests/snapshots/files__proofs__matrix_proof_testing.snap | Updated proof snapshot for matrix example and determinism changes. |
| egglog/tests/snapshots/files__proofs__intersection_proof_testing.snap | Updated proof snapshot for intersection example under relation-based encoding. |
| egglog/tests/snapshots/files__proofs__integer_math_proof_testing.snap | Updated proof snapshot for integer math example. |
| egglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snap | Updated proof snapshot IDs/substitutions after encoding changes. |
| egglog/tests/snapshots/files__proofs__fibonacci_demand_proof_testing.snap | Updated proof snapshot for fib demand due to new proof construction layout. |
| egglog/tests/snapshots/files__proofs__eqsat_basic_proof_testing.snap | Updated proof snapshot for eqsat basic example. |
| egglog/tests/snapshots/files__proofs__eqsat_basic_proof_proof_testing.snap | Updated proof snapshot for eqsat basic “proof of proof” case. |
| egglog/tests/snapshots/files__proofs__custom_container_output_rebuild_proof_testing.snap | New/updated proof snapshot covering custom container output rebuild. |
| egglog/tests/snapshots/files__proofs__container_set_collapse_proof_testing.snap | Updated proof snapshot for set collapse under new proof primitives. |
| egglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snap | Updated container proofs snapshot for new relation-based proof terms. |
| egglog/tests/snapshots/files__proofs__commute_collapse_proof_testing.snap | Updated commute/collapse proof snapshot. |
| egglog/tests/snapshots/files__proofs__calc_proof_testing.snap | Updated calc proof snapshot reflecting new Rule term form. |
| egglog/tests/snapshots/files__proofs__birewrite_proof_testing.snap | Updated birewrite proof snapshot under relation-based encoding. |
| egglog/tests/snapshots/files__proofs__antiunify_proof_testing.snap | Updated antiunify proof snapshot. |
| egglog/tests/snapshots/files__proof_unsupported_files.snap | Marks lambda.egg as proof-unsupported in snapshots list. |
| egglog/tests/proof_mode_regression.rs | Adjusts regression tests for updated :no-merge/fail semantics and adds new container-proof regression. |
| egglog/tests/eggcc-2mm.egg | Rewrites several :no-merge functions to :merge old to match encoding support. |
| egglog/tests/custom-container-output-rebuild.egg | New test program for container-valued custom output rebuild behavior. |
| egglog/tests/container-reorder-proofs.egg | New test program covering container rebuild proofs when container iteration order differs from canonical term order. |
| egglog/src/typechecking.rs | Adds backend-op primitive registration helper; updates fail typing; loosens prove-exists target constraints. |
| egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snap | Updates proof tests snapshot to relation-based term/proof encoding form. |
| egglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snap | Updates proof tests snapshot to relation-based term/proof encoding form. |
| egglog/src/proofs/proof_tests.rs | Updates internal proof tests to count Rule proof relation insertions rather than constructor calls. |
| egglog/src/proofs/proof_fresh.rs | New module defining/typing get-fresh!, set-if-empty, and view-proof primitives routed via backend SPI. |
| egglog/src/proofs/proof_extractor.rs | Supports reconstruction from relation terms and makes selection deterministic by sorting matching rows. |
| egglog/src/proofs/proof_extraction.rs | Makes prove-exists deterministic by choosing lexicographically smallest witness row and handling relation-term output indexing. |
| egglog/src/proofs/proof_encoding_helpers.rs | Introduces CongrAll, split merge-proof constructors, proof-list minting changes, and new proof encoding constraints/ops. |
| egglog/src/proofs/proof_encoding_facts.rs | New query-side instrumentation module for proof encoding fact handling. |
| egglog/src/proofs/proof_container_rebuild.rs | Updates container rebuild proof minting for relation-based proof terms and adds CongrAll-based element matching. |
| egglog/src/proofs/proof_checker.rs | Exposes eval_expr_with_subst for reuse in encoding components. |
| egglog/src/proofs/mod.rs | Wires in new proof encoding modules (proof_fresh, proof_encoding_facts, etc.). |
| egglog/src/prelude.rs | Updates function declaration helper to include new cost field. |
| egglog/src/lib.rs | Adds native encoded (input …) loading path, multi-command fail, and supporting input parsing refactor. |
| egglog/src/extract.rs | Updates extraction helpers for FD views/encoding relations and cost propagation via :internal-cost. |
| egglog/src/ast/remove_globals.rs | Updates global removal to handle multi-command fail correctly. |
| egglog/src/ast/proof_global_remover.rs | Removes obsolete proof-specific global remover (now unified under remove_globals). |
| egglog/src/ast/parse.rs | Extends parsing for multi-command fail and :internal-cost; updates proof-name metadata parsing. |
| egglog/src/ast/mod.rs | Updates AST model for multi-command fail, extended proof constructor metadata, and function cost. |
| egglog/src/ast/desugar.rs | Desugars multi-command fail by wrapping the full flattened expansion. |
| egglog/src/ast/check_shadowing.rs | Extends shadowing checks to iterate over multi-command fail. |
| egglog/egglog-bridge/src/lib.rs | Adds O(1) reverse index for cached panic functions; adds backend support for set-if-empty and view-proof ops. |
| egglog/egglog-backend-trait/src/lib.rs | Extends backend trait with counter access, native input batch insertion, and term-encoding SPI registrations. |
| egglog/egglog-backend-trait/src/backend_impl.rs | Implements new backend-trait methods for the reference backend. |
| egglog/egglog-backend-trait/Cargo.toml | Adds egglog-numeric-id dependency required by updated backend trait. |
| egglog/core-relations/src/free_join/mod.rs | Optimizes merge_all by resetting indexes only for touched tables and adds counter overwrite support. |
| egglog/CHANGELOG.md | Documents encoding rewrite highlights, performance wins, and behavioral changes (fail, no-merge support, determinism). |
| egglog-experimental/tests/snapshots/files__proofs__with_ruleset_proof_testing.snap | Updates experimental snapshot to new proof term form. |
| egglog-experimental/tests/fixtures/eggcc-2mm-pass1.egg | Rewrites no-merge declarations to :merge old for encoding compatibility. |
| egglog-experimental/tests/eggcc_2mm_proof.rs | Updates assertions to match rewritten no-merge behavior. |
| egglog-experimental/src/set_cost.rs | Updates macro-generated declarations to include the new cost field. |
| egglog-experimental/dd/tests/files.rs | Updates known-unsupported list and comments for DD backend coverage changes. |
| egglog-experimental/dd/src/lib.rs | Shares id minting counter with get-fresh! and adds mirror-based support for set-if-empty/view-proof ops and native input. |
| egglog-experimental/dd/src/interpret.rs | Intercepts set-if-empty/view-proof primitives to service them against the DD mirror during interpretation. |
| egglog-experimental/dd/output.R3.log | New DD output fixture for relation output rendering. |
| egglog-experimental/dd/output.R3.csv.log | New DD CSV output fixture for relation output rendering. |
| egglog-experimental/dd/output.R.log | New DD output fixture for relation output rendering (variant). |
| egglog-experimental/dd/output.R.csv.log | New DD CSV output fixture for relation output rendering (variant). |
| egglog-experimental/dd/output.G3.log | New DD output fixture for G output rendering. |
| egglog-experimental/dd/output.G3.csv.log | New DD CSV output fixture for G output rendering. |
| egglog-experimental/dd/output.G.log | New DD output fixture for G output rendering (variant). |
| egglog-experimental/dd/output.G.csv.log | New DD CSV output fixture for G output rendering (variant). |
| Cargo.lock | Adds egglog-numeric-id to lockfile due to backend-trait dependency update. |
Comments suppressed due to low confidence (1)
egglog/src/lib.rs:2264
read_input_filepanics on unsupported column sorts. Since this is triggered by user-provided programs (e.g.,(input ...)targeting a schema with an unexpected sort), it should return a structuredErrorinstead of aborting the process.
for sort in &function_type.input {
match sort.name() {
"i64" | "f64" | "String" => {}
name => panic!("Unsupported type {name} for input"),
}
}
if function_type.subtype != FunctionSubtype::Constructor {
for sort in &function_type.outputs {
match sort.name() {
"i64" | "String" | "Unit" => {}
name => panic!("Unsupported type {name} for input"),
}
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
2304
to
2316
| let literal = match sort.name() { | ||
| "i64" => raw | ||
| .parse() | ||
| .map(Literal::Int) | ||
| .map_err(|_| Error::InputFileFormatError(file.to_owned()))?, | ||
| "f64" => raw | ||
| .parse::<f64>() | ||
| .map(ordered_float::OrderedFloat) | ||
| .map(Literal::Float) | ||
| .map_err(|_| Error::InputFileFormatError(file.to_owned()))?, | ||
| "String" => Literal::String(raw.to_owned()), | ||
| _ => unreachable!(), | ||
| name => panic!("Unsupported type {name} for input"), | ||
| }; |
file_supports_proofs checked every command against the final popped scope, so a global defined in a (push)/(pop) block and read in an action looked like an unsupported function lookup. Collect the program's let-bound names up front and treat them as globals. Six corpus files (herbie, array, bdd, cyk, math, typeinfer) join the term/proof-encoding trials. Herbie then exposed a checker gap: the encoder mints reflexive Fiat proofs for base-primitive results, but BigInt/BigRat results are term-shaped, not literals, so the checker rejected them unless a global happened to establish them. The checker now accepts a reflexive Fiat over any primitive-closed term by re-evaluating it with the primitive validators (threaded into ProofStore like the container normalizers), and from-string gains a validator. typeinfer uses containers, so it joins DD's known-unsupported list. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
egglog/src/proofs/proof_encoding_helpers.rs (1)
793-800: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick winPreserve scoped globals while validating nested
failcommands.Line 798 calls the public wrapper, which replaces
extra_globalswith an empty set. Consequently, a(fail ...)command that reads a(push)-scoped global is still rejected in proof mode. Recurse throughcommand_supports_proof_encoding_implwith the existing set.Proposed fix
- command_supports_proof_encoding(command, type_info)?; + command_supports_proof_encoding_impl(command, type_info, extra_globals)?;🤖 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_encoding_helpers.rs` around lines 793 - 800, Update the GenericCommand::Fail branch to recurse through command_supports_proof_encoding_impl using the existing extra_globals set instead of the public command_supports_proof_encoding wrapper. Preserve the FailInputCommand rejection and propagate validation errors for all nested commands.egglog/CHANGELOG.md (1)
5-26: 📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick winCondense the Unreleased changelog entries.
These bullets expose extensive implementation detail (FD views, helper tables, rebuild mechanics) rather than concise caller-facing changes. Keep the behavioral contract and breaking-change guidance, but move internals to dedicated documentation or PR notes.
🤖 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/CHANGELOG.md` around lines 5 - 26, Condense the Unreleased changelog bullets into concise, caller-facing summaries, especially those describing FD views, helper tables, rebuild mechanics, proof constructors, and backend internals. Preserve each user-visible behavior change, performance improvement, backend/API addition, and breaking or migration guidance; move detailed implementation mechanics to dedicated documentation or PR notes.Source: Coding guidelines
🤖 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.
Outside diff comments:
In `@egglog/CHANGELOG.md`:
- Around line 5-26: Condense the Unreleased changelog bullets into concise,
caller-facing summaries, especially those describing FD views, helper tables,
rebuild mechanics, proof constructors, and backend internals. Preserve each
user-visible behavior change, performance improvement, backend/API addition, and
breaking or migration guidance; move detailed implementation mechanics to
dedicated documentation or PR notes.
In `@egglog/src/proofs/proof_encoding_helpers.rs`:
- Around line 793-800: Update the GenericCommand::Fail branch to recurse through
command_supports_proof_encoding_impl using the existing extra_globals set
instead of the public command_supports_proof_encoding wrapper. Preserve the
FailInputCommand rejection and propagate validation errors for all nested
commands.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: bdcb22f4-a934-402c-83d7-da0bd97af79f
⛔ Files ignored due to path filters (6)
egglog/tests/snapshots/files__proof_unsupported_files.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__array_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__bdd_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__cyk_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__math_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__typeinfer_proof_testing.snapis excluded by!**/*.snap
📒 Files selected for processing (8)
egglog-experimental/dd/tests/files.rsegglog/CHANGELOG.mdegglog/src/proofs/proof_checker.rsegglog/src/proofs/proof_encoding_helpers.rsegglog/src/proofs/proof_extraction.rsegglog/src/proofs/proof_format.rsegglog/src/sort/bigint.rsegglog/src/typechecking.rs
A reflexive Fiat over a container-producing primitive applied to base args (e.g. (set-of) or (vec-of 1 2)) would re-evaluate to itself and fabricate the container term's existence. Exclude presort (container / unstable-fn) primitives from the checker's validator map; eq-sort inputs were already excluded structurally (constructor heads are not validators). Legitimately built containers keep flowing through the globals branch. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Replace the checker's name-harvested primitive-validator map with an explicit per-sort declaration: a base sort whose values termify as an application (BigInt's (from-string ...), BigRat's (bigrat ...)) provides its canonical head and recognizer, mirroring rebuild_container_normalizer for containers. The Fiat rule then accepts reflexive proofs over exactly these declared value term forms — no overload disjunction, and the presort exclusion filter becomes unnecessary since existence-carrying sorts simply do not declare a value form. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reflexive proofs of primitive results were minted as Fiat, whose checker rule only accepted literals or global-established equalities — wrong for BigInt/BigRat values, which termify as applications. Split the concept: Fiat is now top-level (global) equalities only, and the new Computed form proves t = t for a chain of primitive applications over literals/variables, checked structurally in the checker itself against the base-value primitive names (presort/container families excluded, so no term-existence claim can be smuggled in). This replaces the short-lived value_term_validator sort hook. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The Computed rule accepted terms by shape without running anything. Rework per review: - Base-value primitive facts generalize the container side-condition mechanism: the fact is emitted verbatim (when free of function calls) with an Eval marker, and the checker re-evaluates it against the rule body with the program's typed validators — the computation actually runs where the types live. Facts containing global reads keep the instrumented path; the checker ignores side-condition premise slots, so only counts must align. - Computed remains for termified base values at proposition leaves (literal facts, base-sort variables): canonical value spellings like BigInt's (from-string ...) that the program never wrote. It is now verified by executing the sort-declared value_term_validator recognizer and requiring the term to reproduce itself — a real computation, local to the node. - prove_exists keeps the wrapping rule when a single premise is a side-condition marker (a bare Eval is only checkable in rule context). - The structural computable-term rule and its primitive-name set are deleted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 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/CHANGELOG.md`:
- Line 6: The changelog entry is overly detailed and the proof facts
documentation repeats implementation mechanics. In egglog/CHANGELOG.md line 6,
condense the entry to concise caller-facing behavior, removing corpus status and
proof-internal details. In egglog/src/proofs/proof_encoding_facts.rs lines
21-32, retain the side-condition contract while removing repeated checker and
premise-slot mechanics.
In `@egglog/src/proofs/proof_checker.rs`:
- Around line 695-696: Update the primitive side-condition branch in the
proof-checking logic around check_side_condition to validate premise_id before
re-evaluating fact: require the referenced premise’s justification to be
Justification::Eval, and return a dedicated mismatch error when it is not.
Preserve the existing side-condition substitution and checking behavior after
this validation.
In `@egglog/src/proofs/proof_format.rs`:
- Around line 193-197: Preserve every validator for a canonical head rather than
allowing collection-order overwrites: update value_term_validators in
egglog/src/proofs/proof_format.rs:193-197 to hold grouped validators, and update
validator collection in egglog/src/proofs/proof_extraction.rs:113-118
accordingly so validation accepts only a validator reproducing the exact term.
In egglog/src/sort/mod.rs:96-104, no direct change is required unless
single-validator storage is retained; in that case, enforce and document global
head uniqueness.
🪄 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: f9523fef-200b-470d-8066-71e7b7e3b729
⛔ Files ignored due to path filters (34)
egglog/tests/snapshots/files__proofs__array_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__bdd_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__bind_prim_result_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__bitwise_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__commute_collapse_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__container_proofs_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__cyk_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__f64_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__fail_wrong_assertion_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__fibonacci_demand_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__filter_or_bool_neq_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__i64_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__intersection_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__math_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__merge_during_rebuild_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__primitive_args_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__primitives_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__push_pop_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_empty_query_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_equal_constant2_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_equal_constant_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_filter_bug_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_new_backend_prims_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_querybug2_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__repro_querybug4_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__resolution_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__rw_analysis_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__schedule_demo_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__string_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__test_combined_steps_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__typecheck_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__typeinfer_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__unification_points_to_proof_testing.snapis excluded by!**/*.snapegglog/tests/snapshots/files__proofs__until_proof_testing.snapis excluded by!**/*.snap
📒 Files selected for processing (12)
egglog/CHANGELOG.mdegglog/src/prelude.rsegglog/src/proofs/proof_checker.rsegglog/src/proofs/proof_encoding_facts.rsegglog/src/proofs/proof_encoding_helpers.rsegglog/src/proofs/proof_extraction.rsegglog/src/proofs/proof_format.rsegglog/src/proofs/proof_simplification.rsegglog/src/sort/bigint.rsegglog/src/sort/bigrat.rsegglog/src/sort/mod.rsegglog/src/typechecking.rs
💤 Files with no reviewable changes (1)
- egglog/src/typechecking.rs
Owner
|
Ran the benchmarks on the most recent version of this, seems like it makes some faster and some slower right now: Benchmark ReportComparison
6 file(s): math-microbenchmark.egg, eggcc-2mm-pass1.egg, pointer-analysis-small.egg (facts: /Users/saul/p/egglog-encoding/benchmarks/data/pointer-analysis-small), hardboiled_conv1d_32.egg, luminal-llama.egg, herbie.egg · 6 round(s) per endpoint/file · 120 s timeout per run · Report: /Users/saul/p/egglog-encoding/.reports.jsonl Summary — a1933da main/proofs vs 1cc0e8a main/proofs
Ratios are candidate / baseline; below 1 is lower and above 1 is higher. Per-file resultsWall time
Peak RSS
|
Collaborator
|
yep- though for hardboiled that may just be the container bug fix this is a stepping stone for other optimizations, so I'd say worth the slowdown to herbie.egg |
saulshanabrook
approved these changes
Jul 23, 2026
saulshanabrook
left a comment
saulshanabrook
left a comment
Owner
There was a problem hiding this comment.
I think it would be OK to merge as is. I like that we get rid of constructors, that makes a lot more sense to me (I am confused why we had them in the first place, if we didnt depend on a UF?)
Main concern is adding the set-if-doesnt-exist primitive... seems to require a bunch of special casing and curious if there is a way to write the encoding without it.
Owner
|
Oh also a little worried about the performance here... since it makes sense benchmarks quite a bit slower. but 🤷 I know this is setup to make things faster in the future |
- Rename the backend SPI's `fresh_eclass_id`/`eclass_id_counter` to `fresh_id`/`id_counter`: they mint generic term/proof/AST ids, not e-class-specific ones (the backend has no e-class concept). Clarify the docs that a fresh id is just the next counter value, not stored anywhere until the encoding asserts a relation row that references it. - Make the backend SPI proof-agnostic: `Backend::register_view_proof` becomes `register_view_column_read(view, n_keys, col_idx)`, a generic view-column read. The proof encoding (which owns the notion of "proof") reads column 1. - Remove the last constructors from the encoding: the deferred delete/subsume marker tables are now `Unit :no-merge` relations tagged with a new `:internal-marker` function flag, so extraction never mistakes them for term relations (they carry no minted id and may be nullary). - proof_encoding.md: clarify `:internal-identity-vals` (idempotent re-writes, not a key), describe the proof nodes as relations rather than constructors, and document the delete/subsume markers. - Skip the oversized bdd/math/typeinfer proof-testing snapshots (2.6k-6.5k lines) via PROOF_TESTING_SNAPSHOT_DISABLED_FILES. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The proof checker never used the validator returned by `Sort::prim_value_constructor` — it only needs to know that a term's head is a base sort's value constructor so it can treat the term as a self-evident value (the `reflexive_value_term` check). Return just the head name (`Option<String>`) and drop the per-sort recognizer closures; the checker now accepts such a term by head membership plus recursion into its arguments. Add a sanity check when collecting these heads: a value constructor must resolve to exactly one primitive (no overloads). The checker treats the head as an unambiguous value marker, so an overloaded head would be unsound to ignore. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Under term encoding a user `(relation R …)` / constructor becomes an internal term relation — a `(function R (children… id) Unit :no-merge)` whose eclass id is the last input column, with a trailing `Unit` output. `EGraph::constructor_enodes` rejected it (its subtype is `Custom`, not `Constructor`) and, had it not, split the row assuming the eclass was the output column. Accept term relations (`is_relation_term`) in `constructor_enodes`, and locate the children/eclass with `extraction_num_children` / `extraction_output_index`, which are correct for both real constructors (eclass = output) and term relations (eclass = last input, trailing `Unit` ignored) — and reduce to the old `split_last` for real constructors, so non-term reads are unchanged. Reject term relations from `function_entries`, since they read as enodes rather than function entries. Fixes `backend_generic_reads_work_without_an_action_registry`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
| /// literal (e.g. a BigInt's `(from-string "…")`): the head of that canonical | ||
| /// value term (see [`Sort::prim_value_constructor`]). `None` (the default) | ||
| /// for literal-backed sorts. | ||
| fn prim_value_constructor(&self) -> Option<String> { |
The term/proof encoding's term/proof/AST/proof-list node relations are structurally identical to the deferred delete/subsume bookkeeping markers (all hidden `Unit :no-merge` relations), so extraction needs an explicit signal to tell them apart. Instead of tagging the two markers negatively with `:internal-marker`, tag the node relations positively with `:internal-term-node` (their minted id is the last input) and leave the markers plain. `is_relation_term()` is now just `decl.internal_term_node`. The flag lives on the FunctionDecl, so it round-trips through desugaring and re-parsing (verified by the `*_desugar_proof_testing` fixtures, which a records-based positive scan could not satisfy); extraction reconstructs exactly the flagged relations and never reads the markers as terms. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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
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.
Rewrites the term/proof encoding from constructors to relations, makes container proofs sound, and extends proof checking to programs the old gate wrongly rejected.
The encoding
(function F (args id) Unit). E-class / proof-node ids are minted explicitly with a genericget-fresh!primitive and canonicalized into per-constructor FD "view" tables(children) -> (eclass, proof)viaset-if-empty(get-or-insert on the view). Views stay canonical, so nothing needs re-keying at rebuild.MergeFnIdx/MergeFnRow, index-based over the merge body) so a custom merge's proof doesn't need the merged term's children; custom merges run once in the FD view's own:merge.(input …)loading: constructor/relation/custom-function inputs are loaded as data through a small backend SPI (fresh_eclass_id()+add_values(rows)) instead of a compiled loader rule.@UFfunction tables).Container proofs
Set/MultiSet/Map): rebuilds identified changed elements by their position in value order, which need not match the term's canonical child order. Rebuild proofs now use an element-matchingCongrAllraw-proof form, desugared into positionalCongrsteps during proof conversion (user-facing proof format unchanged).natural -> dedupedequality recorded in the element's ordinary union-find — so a container's term-proof stays anchored on the shape the rule wrote (e.g. when the deduped e-class extracts as a birewrite partner), and the standard rebuild + path compression canonicalize it. This replaced an earlierUF-Auxside-table design.Proof checking coverage
file_supports_proofsno longer rejects programs whose(push)-scoped globals are read in actions; herbie, array, bdd, cyk, math, and typeinfer joined the term/proof-encoding test trials.Computedproof form for primitive computations in queries: provest = tfor a chain of primitive applications over literals/variables (no constructors/functions), checked structurally. Needed because BigInt/BigRat values termify as applications, not literals.Fiatis reserved for top-level equalities again.Performance
Benchmarks vs
main(bench.py, full reports below): suite wall time ~2× faster under the term encoding and ~1.5× faster under proofs (pointer-analysis ~10×, luminal--proofs63s → 39s — the earlier luminal regression is resolved). Honest regressions:hardboiled_conv1d_32is ~1.44× slower under proofs (many distinct small terms, little congruence to amortize the relation-row minting) and luminal peak RSS is ~2× under proofs.Testing
files783/0 (includes the new herbie/array/bdd/cyk/math/typeinfer proof trials and new container-soundness corpus files), lib 65/0,proof_mode_regression10/10 (luminal + pointer-analysis proof checking green).KNOWN_UNSUPPORTEDlist (DD lacks the registry-backed container-rebuild primitives; routing them through the backend SPI is a follow-up).🤖 Generated with Claude Code
Summary by CodeRabbit
get-fresh!,set-if-empty, and view-proof support.(input ...)tables for faster ingestion.failwrapping.