DD backend perf: compact layouts, O(delta) host bookkeeping, shared arrangements (math-microbenchmark 211s -> 70s) - #29
Draft
oflatt-claude wants to merge 50 commits into
Draft
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>
…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 proof-tracking docs only showed flat, one-level term construction and still described it in the pre-relations constructor-call style. Add a section that traces `(union rewrite_var (Neg (Add a (Add b c))))` end to end in the actual relations encoding: flattening, `get-fresh!` term minting, `set-if-empty` view interning to canonical ids, the natural-vs-canonical node split, `Congr` over moved children via `natural = canonical` connectors, and the final oriented union edge. Also flag the earlier flat rule snippet as schematic and point to the new section. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Reorganize the encoding doc so the data structures come first, then actions (construction, union, delete), then queries, then the rebuilding machinery, then globals and containers — instead of interleaving term-mode and proof-mode passes over one example. Along the way, replace the stale pre-relations snippets (which still showed constructor-call term building) with the actual relations encoding: `get-fresh!` minting, `set-if-empty` / `view-proof` view interning, and the function-style term relation. The nested `(Neg (Add a (Add b c)))` walk-through from the previous commit becomes the "building nested terms with proofs" subsection under Actions. Snippets were generated from the real encoder output; the running Add example and the exercised Neg example both pass `--proof-testing`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- `(prove-exists f)` on a base-sort-output function (no proof table) now returns a clean `RequiresConstructor` error instead of panicking. Removing the old `subtype == Constructor` typecheck gate (needed because a constructor lowers to a `Custom` term relation) had left the runtime lookup to panic on a proof-func miss. - Remove dead code surfaced by review: the `proof_functions` `""` stub and its call, the caller-less `zz_report`, and the unused `TypeError::ProveExistsRequiresConstructor` variant. - Fix stale comments: the proof-extraction "first row" note (extraction is now deterministic) and the "allow primitive globals" note on the second `remove_globals` (both calls are identical; it removes encoding-introduced lets). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
No longer used after the merge_all touched-set change; nothing rolls a counter back to a previous value. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Reword the 'union in a rule' actions and rename the nested-term-building variables to e (natural), e' (canonical children), e'' (representative), with proofs named e_to_e'' etc., matching the running example. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- Global-value proofs: anchor a global let's proof on the *natural* term (the literal definition the checker establishes from '(let x e)') via the recorded natural->canonical connector, instead of fiat-ing the canonical e-class directly. A global whose value has a rewritten child (e.g. $six2 = (Plus 2 (Plus 2 2)) with (Plus 2 2) canonicalized to 4) otherwise produced a reflexive Fiat over a term the checker cannot establish, failing naturals proof-testing. - Skip the post-action maintenance rebuild only after a 'set' or top-level expr over non-container sorts; container-valued actions still rebuild so their ':naive' recanonicalization runs. - Remove the dead Merge justification (RawProof::MergeFn) parse/convert path; MergeFnIdx/MergeFnRow share merge_premise_view / merge_fn_proof helpers. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ckend) - Clarify why fd_custom_funcs is needed (FuncType lacks :merge info at action/query sites) — review comment. - Move the 'shared registration engine' doc back onto register_per_context (it had drifted onto add_backend_op_primitive) — review comment. - Document on the Backend trait that term encoding needs no dedicated union/constructor op (tables + rules + :merge suffice) — review comment. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Follow-up to the review thread: a union action lowers to a :merge write and a constructor application to a table insert, so the backend never sees union/constructor as primitives even during action evaluation. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
get-fresh! is a single generic mint primitive; register it in with_backend (a no-op without an eclass-id counter) rather than idempotently from every eq-sort's Sort command. Covers every e-graph that runs the encoded program, including replay of the already-desugared program in a plain e-graph (the desugar proof-testing path). Drops the get_fresh_registered guard/field. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The subexpression-conclusion helper is only used when converting a MergeFnIdx/MergeFnRow raw proof into its MergeFn conclusion, so it belongs with from_raw in proof_format, not the checker. Restore run_merge to its original body in proof_checker (used by check_proof to independently re-verify a MergeFn proof) — proof_checker now differs from base only by making eval_expr_with_subst pub(crate) so the moved helper can reuse it. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…end) Reverts the earlier removal: set_counter was not dead — egglog-experimental /dd/src/lib.rs uses it to roll a counter back. The egglog files test doesn't build the dd crate, so the breakage was missed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
native_input now derives everything from the encoded decls' annotations (like extraction) instead of proof_state.proof_names + original_typechecking: term relation by name, view via its term_constructor back-reference, CSV base-column sorts + the constructor/:merge/:no-merge shape from the schema (is_fd_view + arity), and proof tables from replay-safe annotations (Fiat added to the Proof sort's :internal-proof-names; the AST constructor by its (<sort> <Ast>)->Unit signature; <Sort>Proof via :internal-proof-func). The (input ...) dispatch keys on is_relation_term() rather than proof mode. This lets custom-function inputs load natively too, so the bodyless loader rule + input_loader_rulesets are gone, and — because the load is now self-contained on the encoded tables — a desugared proof-mode program replays correctly in a plain e-graph (the desugar+proof round-trip that previously had to be skipped for (input ...) files now runs). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
(fail c1 c2 ...) runs the wrapped commands in order and passes iff one of them errors. This lets fail wrap a block that fails somewhere within it, and in particular lets proof mode wrap (fail (set ...)) — a set encodes to many commands, so the old single-command fail (and its FailNonAtomicCommand gate) couldn't. Desugar/remove-globals now wrap the whole expanded block, not just the last command. set_sort_function.egg (an eq-sort :no-merge conflict wrapped in fail) is moved from the auto proof-unsupported list to an explicit, documented MANUAL_PROOF_DISABLED_FILES entry: making that conflict fire eagerly needs native :no-merge, which requires a conditional/UF-aware panic in the merge machinery (a separate follow-up) — panic doesn't lower inside a :merge today. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…values - nat_conn is now a local map threaded through the action/term builders instead of a shared field that was cleared per generated program (C6). - Add an output_is_eclass(fdecl) helper (constructor || encoded global) and use it in term_and_view + rebuilding_rules; is_fd_view delegates its internal-let check to is_encoded_global (C4). - DD backend: route add_values through the merge-aware apply_sets so same-key/different-value rows are collapsed by each function's :merge (FD-view congruence, :no-merge rejection) instead of coexisting raw; stash any error in the panic side channel to surface on the next run (C1). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
:no-merge functions were the last merge/conflict logic encoded as a *rule*
(the eq-sort conflict-panic rule in rebuilding_ruleset) plus a primitive-
output 'current' helper. Rather than build new merge machinery to detect
eq-sort conflicts eagerly, mark :no-merge functions unsupported by the
encoding (a new NoMergeFunction reason in command_supports_proof_encoding,
gated on Function{merge:None, let_binding:false} so encoded globals and
constructors are excluded). :no-merge files now run in plain mode only,
where the native backend handles them.
Deletes handle_no_merge_fn (both branches), handle_merge_or_congruence,
the merge_current field + its update_view/native_input uses, and the
:no-merge view-declaration branch — removing the merge-as-a-rule path
entirely; all merge/conflict logic now lives in the view's :merge.
The eggcc-2mm benchmark (egglog + the proof-tested fixture) is converted to
:merge old so it stays proof-supported. 12 genuinely-:no-merge files move to
the proof-unsupported list.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Only eq-sort-output :no-merge stays unsupported (needs union-find-aware conflict detection). A primitive/Unit :no-merge custom is now the FD pair-valued view (children) -> (output, proof) declared :no-merge with :internal-identity-vals 1: identity-vals skips on an unchanged raw output (ignoring the proof column) and the native :no-merge AssertEq panics on a genuine output conflict. No current helper, no rule. Since every encoded custom is now FD-viewed (:merge or primitive :no-merge; eq-sort :no-merge is never encoded), fd_custom_funcs is redundant: removed the field, its population, func_type_is_fd_view, and the query is_fd branch (add_term_and_view always uses the FD view). Resolves the fd_custom_funcs review comment by removal. 10 files regain term/proof coverage; lambda + set_sort_function stay unsupported (eq-sort :no-merge). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- Extract the duplicated rule-emission template into a rebuild_rule helper.
- Fold the two near-duplicate value-column rebuild blocks into one
fd_value_rebuild_rule over a ValueRebuild { Eclass, CustomOutput } enum,
written as if/else (they are mutually exclusive); only the proof and the
update action differ per arm.
- Reword the confusing 'original behaviour' comment; tighten the
rebuilding-rules and vec-of comments; clarify that the vec-of rebuild is
ordered-container-only because the threaded proof is a positional Congr
fold (the Rust rebuild itself is generic).
Behavior-preserving; no snapshot changes.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- @UF-Aux-<Sort> is now a fresh UF_Aux_<Sort> name recorded in an :internal-uf-aux annotation (carried on the sort's uf tuple) and rediscovered on re-parse via uf_aux_parent, instead of a hardcoded name the Rust container rebuild recomputed. The rebuild reads it from a collected aux_names map (lookup_aux_row). - add_term_and_view's proof branch now mints all proof terms first, then emits the anchor/dedup/view-proof statements, then the vprf-dependent connector mints — same behavior, less interleaving; comments tightened. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
EGGLOG_DD_TIMING=1 prints per-iteration phase times (diff/dd_step/envs/ head/writes) plus delta and binding counts. EGGLOG_DD_DUMP_PLANS=1 dumps each rule's naive join order, flagging cartesian stages, and arrangement counts per fused dataflow. EGGLOG_DD_W=<n> overrides the fixed row width at compile time for width experiments. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three changes to shrink what every arrangement stores and compares:
- RowN<const WIDTH>: the fused dataflow is monomorphized over a width
ladder {8, 16, 32, 48} and each ruleset runs at the smallest width that
fits its plans (JoinPlan::width), instead of a global [u32; 48]. W = 48
remains the planning cap.
- Join keys are a single u128 (up to 4 columns packed exactly; wider key
sets fold the tail into the top lane, with exactness restored by the
compiled shared-variable checks in the join closure) instead of a
full-width row.
- Per-tuple bind/remap closures run AtomOps slot programs compiled once
at dataflow-build time (const/dup/carry/check/write index lists),
replacing per-row HashMap lookups and Vec allocations.
math-microbenchmark (run 11) drops 211s -> 89s; the DD-internal share of
run 10 (dd_step) drops 11.1s -> 2.6s. Full corpus: 131/131 snapshots
match; math run 10/11 print-size output is bit-identical to main.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Every iteration previously paid O(database) three times over: feeding DD required a full version-map compare AND clone per read view, each merge transaction snapshotted whole functions into key->row maps, and the interpreter rebuilt a per-iteration lookup index per touched function (plus lookup_row scanned linearly). All three now run on incremental structures maintained at the existing row-event choke point: - by_key: a persistent per-function key->located-rows index updated by record_row_event. Merge transactions read it lazily through a staged overlay (no per-transaction snapshots), lookups and exact-key removals are O(1) per key, and the per-iteration LookupIndex is gone. - event_logs + dd_fused_cursors: per-view append-only signed row logs replace the three version maps and per-ruleset fed snapshots. Each fused worker folds only its unread window (net weight + last sign per row reproduces the remove/insert/refire batches exactly, without replaying transients); new workers seed from the full current state; fully-consumed prefixes are drained. math-microbenchmark run 11: 89s -> 72s; run-10 diff phase 1.09s -> 0.31s and events scanned drop from 5.6M (full state) to 1.3M (actual deltas). Full corpus: 131/131; run 9/10/11 outputs bit-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
One arrangement per (relation view, key-column projection) per ruleset, used by the right side of every stage AND both sides of each rule's first join: stage-1 joins run arranged-vs-arranged over the shared raw relations, with the bind/remap slot programs moved inside the join closure (bind is injective on surviving rows, so multiplicities are unchanged). Per-rule private stage-1 arrangements and their flat_map stages disappear; only intermediates of 3+-atom rules still arrange privately. Also net captured output deltas keyed by the Copy row type, allocating only for surviving rows. Honest measurement: on math-microbenchmark this is ~neutral (run 11 71.8s -> 70.1s) — the workload's join-key projections are genuinely distinct (the 49-rule rebuilding ruleset still needs 50 arrangements), so there was little to dedup. Where projections do coincide the counts drop (user ruleset: 33 -> 21). Corpus 131/131; outputs bit-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
📝 WalkthroughWalkthroughThis PR refactors the experimental Differential Dataflow backend around indexed event-driven state and const-generic joins, while extending term/proof encoding with auxiliary union-find data, fresh backend primitives, deterministic extraction, native encoded input, and ordered multi-command ChangesDifferential Dataflow backend
Term and proof encoding
Estimated code review effort: 5 (Critical) | ~120 minutes Sequence Diagram(s)sequenceDiagram
participant Parser
participant ProofInstrumentor
participant Backend
participant EGraph
participant ProofExtractor
Parser->>ProofInstrumentor: parse and encode commands
ProofInstrumentor->>Backend: register fresh and view primitives
Backend->>EGraph: mint ids and insert encoded rows
EGraph->>ProofExtractor: provide indexed proof rows
ProofExtractor->>Parser: reconstruct deterministic proof output
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 |
![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/src/proofs/proof_encoding.md`:
- Around line 370-378: Update the uf_path_compress rule’s proof-mode set
expression to preserve the composed equality evidence by storing Trans pb pc in
the UF_Math value for c, while leaving the non-proof-mode behavior unchanged.
In `@egglog/tests/proof_mode_regression.rs`:
- Around line 86-98: Update
term_and_proof_modes_reject_eq_sort_no_merge_functions to match the
UnsupportedProofCommand reason explicitly as
ProofEncodingUnsupportedReason::NoMergeEqSortFunction, while retaining the
existing `:no-merge` message assertion.
🪄 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: f1ac78b7-8f76-4660-8a90-c57c45d108a7
⛔ Files ignored due to path filters (35)
Cargo.lockis excluded by!**/*.lockegglog-experimental/tests/fixtures/eggcc-2mm-pass1.eggis excluded by!**/*.eggegglog-experimental/tests/snapshots/files__proofs__with_ruleset_proof_testing.snapis excluded by!**/*.snapegglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function1.snapis excluded by!**/*.snapegglog/src/proofs/snapshots/egglog__proofs__proof_tests__tests__doc_example_add_function2.snapis excluded by!**/*.snapegglog/tests/eggcc-2mm.eggis excluded by!**/*.eggegglog/tests/snapshots/files__proof_unsupported_files.snapis excluded by!**/*.snapegglog/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__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 (34)
egglog-experimental/dd/src/dd_native.rsegglog-experimental/dd/src/interpret.rsegglog-experimental/dd/src/lib.rsegglog-experimental/dd/tests/files.rsegglog-experimental/src/set_cost.rsegglog-experimental/tests/eggcc_2mm_proof.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/check_shadowing.rsegglog/src/ast/desugar.rsegglog/src/ast/mod.rsegglog/src/ast/parse.rsegglog/src/ast/proof_global_remover.rsegglog/src/ast/remove_globals.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.mdegglog/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/proofs/proof_tests.rsegglog/src/typechecking.rsegglog/tests/proof_mode_regression.rs
💤 Files with no reviewable changes (1)
- egglog/src/ast/proof_global_remover.rs
Comment on lines
+370
to
+378
| The only union-find rule flattens `a -> b -> c` chains to `a -> c` (composing the | ||
| two edge proofs with `Trans` in proof mode): | ||
|
|
||
| ```text | ||
| (function MathProof (Math) Proof :merge old :unextractable :internal-hidden) | ||
| (rule ((= (values b pb) (UF_Math a)) | ||
| (= (values c pc) (UF_Math b)) | ||
| (!= b c)) | ||
| ((set (UF_Math a) (values c ()))) | ||
| :ruleset parent :name "uf_path_compress") |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Preserve the composed proof during path compression.
In proof mode, UF_Math has a Proof column, so values c () is invalid and discards the equality evidence. The compressed edge must carry Trans pb pc, proving a = c from a = b and b = c.
Proposed fix
- ((set (UF_Math a) (values c ())))
+ ((set (UF_Math a) (values c (Trans pb pc))))📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| The only union-find rule flattens `a -> b -> c` chains to `a -> c` (composing the | |
| two edge proofs with `Trans` in proof mode): | |
| ```text | |
| (function MathProof (Math) Proof :merge old :unextractable :internal-hidden) | |
| (rule ((= (values b pb) (UF_Math a)) | |
| (= (values c pc) (UF_Math b)) | |
| (!= b c)) | |
| ((set (UF_Math a) (values c ()))) | |
| :ruleset parent :name "uf_path_compress") | |
| The only union-find rule flattens `a -> b -> c` chains to `a -> c` (composing the | |
| two edge proofs with `Trans` in proof mode): | |
🤖 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.md` around lines 370 - 378, Update the
uf_path_compress rule’s proof-mode set expression to preserve the composed
equality evidence by storing Trans pb pc in the UF_Math value for c, while
leaving the non-proof-mode behavior unchanged.
Comment on lines
+86
to
+98
| fn term_and_proof_modes_reject_eq_sort_no_merge_functions() { | ||
| // Eq-sort-output `:no-merge` is not modeled by the encoding (its conflict check | ||
| // needs union-find leaders); such a program is unsupported and runs plain only. | ||
| // Primitive/Unit-output `:no-merge` is supported (see the input test above). | ||
| for mut egraph in [ | ||
| EGraph::new_with_term_encoding(), | ||
| EGraph::new_with_proofs().with_proof_testing(), | ||
| ] { | ||
| let error = egraph | ||
| .parse_and_run_program( | ||
| None, | ||
| r#" | ||
| (function score () i64 :no-merge) | ||
| (set (score) 1) | ||
| (set (score) 2) | ||
| "#, | ||
| ) | ||
| .parse_and_run_program(None, "(sort Foo) (function bar () Foo :no-merge)") | ||
| .unwrap_err(); | ||
| assert!(error.to_string().contains("Illegal merge attempted")); | ||
| assert!(matches!(error, Error::UnsupportedProofCommand { .. })); | ||
| assert!(error.to_string().contains("`:no-merge`")); |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Assert the specific unsupported reason.
Line 97 accepts any UnsupportedProofCommand, so an unrelated encoder rejection would pass this regression. Match ProofEncodingUnsupportedReason::NoMergeEqSortFunction explicitly.
Proposed fix
- assert!(matches!(error, Error::UnsupportedProofCommand { .. }));
+ assert!(matches!(
+ error,
+ Error::UnsupportedProofCommand {
+ reason: ProofEncodingUnsupportedReason::NoMergeEqSortFunction,
+ ..
+ }
+ ));📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| fn term_and_proof_modes_reject_eq_sort_no_merge_functions() { | |
| // Eq-sort-output `:no-merge` is not modeled by the encoding (its conflict check | |
| // needs union-find leaders); such a program is unsupported and runs plain only. | |
| // Primitive/Unit-output `:no-merge` is supported (see the input test above). | |
| for mut egraph in [ | |
| EGraph::new_with_term_encoding(), | |
| EGraph::new_with_proofs().with_proof_testing(), | |
| ] { | |
| let error = egraph | |
| .parse_and_run_program( | |
| None, | |
| r#" | |
| (function score () i64 :no-merge) | |
| (set (score) 1) | |
| (set (score) 2) | |
| "#, | |
| ) | |
| .parse_and_run_program(None, "(sort Foo) (function bar () Foo :no-merge)") | |
| .unwrap_err(); | |
| assert!(error.to_string().contains("Illegal merge attempted")); | |
| assert!(matches!(error, Error::UnsupportedProofCommand { .. })); | |
| assert!(error.to_string().contains("`:no-merge`")); | |
| fn term_and_proof_modes_reject_eq_sort_no_merge_functions() { | |
| // Eq-sort-output `:no-merge` is not modeled by the encoding (its conflict check | |
| // needs union-find leaders); such a program is unsupported and runs plain only. | |
| // Primitive/Unit-output `:no-merge` is supported (see the input test above). | |
| for mut egraph in [ | |
| EGraph::new_with_term_encoding(), | |
| EGraph::new_with_proofs().with_proof_testing(), | |
| ] { | |
| let error = egraph | |
| .parse_and_run_program(None, "(sort Foo) (function bar () Foo :no-merge)") | |
| .unwrap_err(); | |
| assert!(matches!( | |
| error, | |
| Error::UnsupportedProofCommand { | |
| reason: ProofEncodingUnsupportedReason::NoMergeEqSortFunction, | |
| .. | |
| } | |
| )); | |
| assert!(error.to_string().contains("`:no-merge`")); |
🤖 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/tests/proof_mode_regression.rs` around lines 86 - 98, Update
term_and_proof_modes_reject_eq_sort_no_merge_functions to match the
UnsupportedProofCommand reason explicitly as
ProofEncodingUnsupportedReason::NoMergeEqSortFunction, while retaining the
existing `:no-merge` message assertion.
oflatt
marked this pull request as draft
July 21, 2026 20:40
This was referenced Jul 23, 2026
This was referenced Aug 4, 2026
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
2 participants
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.
Stacked on #22 (base is
main, so the first 46 commits here are #22's; review the last four:a809beae,a90bd49d,b08f6167,233c7cab). Goal: make the DD backend fast enough to run math-microbenchmark with full iterations.Why the DD backend was slow
Measured with the env-gated diagnostics added in the first commit (
EGGLOG_DD_TIMING=1per-iteration phase timing,EGGLOG_DD_DUMP_PLANS=1plan/arrangement dumps) on(run N)scaling ofmath-microbenchmark.egg:run 11) was not hanging — it completed in 211s vs 5.9s for the main backend under the term encoding (~36×), with bit-identical output.dd_step). Two constant factors dominated: every arrangement key and value was a fixed[u32; 48]row (192 B,Ord/Hashover all 48 lanes), and the per-tuple bind/remap closures did per-rowHashMaplookups and allocations.key → rowsnapshots per merge transaction, a per-iteration lookup index rebuilt from scratch, andlookup_rowdoing a linear scan.Changes
a809beae) — env-gated, zero-cost when off.a90bd49d) — the fused dataflow is monomorphized over a width ladder{8, 16, 32, 48}and each ruleset runs at the smallest width that fits its plans (W = 48stays as the planning cap; math runs entirely at width 8). Join keys become a singleu128(≤4 columns packed exactly; wider key sets fold the tail, with exactness restored by the compiled shared-variable checks in the join closure). Per-tuple closures execute slot programs (AtomOps) compiled once at dataflow-build time — no per-row hashing or allocation.dd_steponrun 10: 11.1s → 2.6s.b08f6167) — a persistent per-function key index (by_key), maintained at the existingrecord_row_eventchoke point, replaces merge-transaction snapshots, the per-iteration lookup index, andlookup_rowscans. Per-view signed event logs with per-worker cursors replace the three version maps and per-ruleset fed-version snapshots: folding a worker's unread window (net weight + last event sign per row) reproduces exactly the old remove/insert/refire batches without replaying transients; new workers seed from the full current state; fully-consumed prefixes are drained.233c7cab) — one shared arrangement per(relation view, key-column projection)per ruleset, consumed by the right side of every stage and by both sides of each rule's first join (arranged-vs-arrangedjoin_coreover the raw relations, with the bind/remap slot programs moved inside the join closure; bind is injective on surviving rows so multiplicities are unchanged). Honest result: ~neutral on math-microbenchmark (71.8s → 70.1s) — measurement showed this workload's join-key projections are genuinely distinct (the 49-rule rebuilding ruleset still needs 50 arrangements), so there was little to dedup; where projections coincide the counts do drop (user ruleset 33 → 21). Kept because it deletes the per-rule stage-1 flat_map/arrange operator chains and is the right base for delta-query plans.Results (math-microbenchmark
(run N), same machine)Where
run 11time goes now:dd_step~36s (54%; arrangement maintenance + join processing across ~110 genuinely-distinct arrangements × ~225 epochs),apply_writes~20s (linear per-write constants),diff~4s, env/head interpretation ~8s. Next levers, in rough order: per-operator timing inside the dataflow (timely logging) to splitdd_step; delta-query plans (dogsdogsdogs) to kill intermediate arrangements on 3+-atom chains; a cheaperEnvrepresentation than oneHashMapper binding; allocation constants in the write path.Validation
cargo test --release -p egglog-experimental-dd: 131/131 corpus snapshots, 36 lib tests,rewrite_joinpass. The one failingsmoketest (backend_generic_reads_work_without_an_action_registry,WrongSubtype) pre-exists on the Relations-based term/proof encoding #22 base.clippy --all-targetsclean.print-sizeoutput for runs 9/10/11 is bit-identical to the main backend under term encoding (e.g.Add 641743at run 11).🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
(fail ...)now supports multiple commands and succeeds when any wrapped command fails.Bug Fixes
Performance
Documentation