DD backend: compile whole schedules to persistent fused dataflows (engine) - #31
Draft
oflatt-claude wants to merge 67 commits into
Draft
DD backend: compile whole schedules to persistent fused dataflows (engine)#31oflatt-claude wants to merge 67 commits into
oflatt-claude wants to merge 67 commits into
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>
…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>
Feasibility spike for moving the term encoding's rebuild loop (union-find canonicalization + congruence closure) INSIDE the dataflow instead of driving it via host (saturate ...) rounds, following the flowlog architecture (fixpoints in iterate scopes; host only commits deltas and reads outputs). Formulation: one loop variable labels(x) seeded as identity; congruence collisions are DERIVED from labels inside the loop (canonicalize term rows through labels; same (op, canonical children) with distinct eclass labels emits an ordering-min union edge), and labels re-close by min propagation over user + congruence edges. Both directions of the mutual recursion live in one Collection::iterate. Tests show two-level congruence cascades converge inside a single epoch and extend incrementally across epochs. docs/rebuild-in-dataflow.md records the integration design, expected impact (epochs ~225 -> ~30 at run 11; rebuild's version-bump churn and ~5M host merge sets vanish), the proof-mode/ordering/delete walls, and next steps. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…model Records the agreed direction: compile (rules + schedule) into one dataflow via a run_schedule backend-API extension (seq = dependency chaining, saturate = iterate scopes, run-N = gated feedback), with user-rule saturation in-dataflow as the goal. Two history-sensitive operators carry egglog's semantics on top of DD's view maintenance: a memoizing mint (append-only key->id dictionary; replay returns the same id, so retraction deltas cancel exactly and counter-id parity is kept) and a rising-edge fire operator (one effect event per 0->positive binding transition, nothing on falling edges) — because egglog's (delete ...) is DATA, not view retraction: consequences of a match persist after the trigger row is deleted. Table state is the integral of an append-only event stream; genuine retraction stays confined to join bookkeeping and the rebuild view layer. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The two history-sensitive operators the schedule->DD compiler needs to carry egglog's monotone-fire semantics on top of DD's view maintenance (docs/rebuild-in-dataflow.md), as frontier-ordered unary operators: - rising_edge: one +1 effect event per 0->positive transition of a binding's count, silence on falling edges. Applies each timestamp's NET delta in ascending order before detecting transitions, so a same-epoch insert+delete is a no-op and a remove-then-reinsert refires (today's version-bump semantics). - memoizing_mint: an append-only key->id dictionary minting from a counter on first demand (in sorted key order per timestamp, for deterministic ids) and emitting a never-retracted (key, id) mapping; replays and re-demands mint nothing. The test drives 'A(x) => B(x, fresh!)' across four epochs: deleting A(1) leaves B's row intact (delete is data, not view retraction), and re-inserting A(1) refires the rule but reuses the ORIGINAL id. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The frontend's schedule interpreter (egglog/src/lib.rs run_schedule over
ResolvedSchedule::{Run, Repeat, Saturate, Sequence}) is already the tree
the backend hook needs. Plan: a ScheduleSpec tree + default-implemented
run_schedule trait method in egglog-backend-trait (main backend unchanged
by construction), frontend delegation, and a fallback rule for regions
with host-side per-iteration machinery (custom Schedulers, until
conditions) that cannot be compiled into the dataflow.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
egglog-backend-trait gains ScheduleSpec (Run/Repeat/Saturate/Sequence, rulesets pre-resolved to rule ids) and an optional Backend::run_schedule hook returning one report per executed Run leaf, defaulting to None — the reference backend is unchanged by construction. The frontend's run_schedule lowers ResolvedSchedule to ScheduleSpec and delegates when the backend accepts, folding the returned leaf reports exactly as its own interpreter would (RunReport::singleton per leaf, unioned), so all reports including (print-stats) are bit-identical either way. Lowering refuses trees containing an until clause (host-side fact check per leaf visit) or an unknown ruleset; the interpreter then retries delegation per subtree. collect_rule_ids moves to a shared helper. The DD backend accepts every offered tree and interprets it over run_rules with the frontend's exact control flow — the seam where schedule regions will next compile into native dataflow fixpoints (docs/rebuild-in-dataflow.md). Validation: full egglog crate suite passes; DD corpus 131/131 with delegation active on every file; math run 9/10 outputs bit-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Promotes rising_edge/memoizing_mint into src/monotone.rs (the compiler will consume them) and prototypes the two schedule-region mechanisms the general any-schedule compiler still needed: - (run N) as gated feedback: a Variable loop whose feedback stream is filtered to rounds < N runs at most N bounded hops inside ONE epoch, with early convergence for free — matching the frontend's Repeat loop exactly on a successor-chain workload. - Minting inside a saturation scope: memoizing_mint runs at Product timestamps (their derived lexicographic Ord refines the lattice order for frontier-complete times), assigning ids deterministically in round order as the fixpoint grows, and the run-N gate caps minting to what the bounded region actually reaches. Design decisions recorded: the compiler handles ANY schedule with a mint stage at every fresh-id site (no mint-free-region analysis), and get-fresh! will take the hash-cons key as arguments so minting is a keyed, declarative operation the compiler recognizes like the other term-encoder ops — making the memo dictionary coincide with the FD view's key->eclass map. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
DD's run_schedule now attempts full compilation before interpreting: schedule_compiler lowers a ScheduleSpec tree into a single dataflow — Sequence chains table states through leaves, Saturate opens a nested scope whose feedback Variables carry each written table to fixpoint, Repeat(n) gates that feedback to rounds < n (early convergence free, Repeat(0) provably a no-op: loops leave 'seed union gated feedback'), and a Run leaf joins rule bodies (reusing plan_join/AtomOps/u128 keys) against the incoming state with match-then-apply leaf semantics. Final states drain into the host tables through the event-recording inserts. v1 compiles the insert-only datalog subset (pure Live table-atom bodies; Set-only heads with agreed constant value columns; one loop level) and falls back to the interpreter otherwise, with env-gated reasons (EGGLOG_DD_DUMP_PLANS=1). Unit tests pin compiled == interpreted for saturation and bounded runs; corpus 131/131 with the compiler live. Fallback probing surfaced the key next wall: under the term encoding EVERY head mints — even a relation head runs (get-fresh! "@sort") for its hidden per-row epoch id — so the keyed get-fresh! redesign (mint as a declarative keyed op the compiler lowers to the mint stage) is the gating step for compiling real term-encoded schedules, ahead of merges and nested loops. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Extends the schedule compiler to the term encoding's head idiom, which probing showed EVERY head uses (even relations mint their per-row epoch id): a head-action interpreter lowers 'Let v = get-fresh!(sort)' to a memoizing-mint stage keyed by (rule, binding) — ids drawn from a range reserved on the host counter and consumed after the run — and 'set-if-empty-<view>!' to a new first_per_key latch per (leaf, view): candidates race per key, the earliest round's minimum wins once, and pre-existing view keys are primed as zero-priority sentinels. LetAtomTerm aliases resolve through both; reading a hash-cons RESULT (constructors) still falls back. DD's execute_schedule now retries compilation on every loop-bearing subtree before interpreting it (the whole-tree attempt may fail on a sibling, e.g. the rebuild sequence the encoding splices into each user iteration); loop-free leaves stay on the incremental fused path. Fixes a livelock the new unit tests caught: the monotone operators held a CapabilitySet parked at the input frontier, which on a feedback path keeps the loop's rounds advancing forever. They now retain capabilities only for pending queued data (upsert-style) and drop them when drained, so loops terminate. Unit tests pin: replay-stable per-binding ids in deterministic order with correct counter advancement, and set-if-empty respecting existing keys. Corpus 131/131; mini-path and math outputs unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds the general (any-merge) lowering ahead of the semilattice-optimized one: merge_hub is ONE stateful operator hosting every written table's authoritative fold state in a compiled region, mirroring the host MergeTransaction at each timestamp — set-if-empty first (head-time on the host), then batched deletes, then merge-aware sets in WAVES to a fixed point (sorted by merge-dependency level; merge-block set actions like the union-find loser edge join the next wave). Waves run inside one timestamp, so Repeat budgets are untouched, exactly the host's waves-within-iteration model. The compiler's write model becomes one cycle per writing loop: state = seeds ∪ hub deltas; bindings join over state; latched tagged write ops feed the hub through a round-incrementing Variable, so effects from round r apply at r+1 — matches always see the previous iteration's state. Rounds are host iterations; the Repeat gate filters fed effects. Per-table Variables and the first_per_key wiring collapse into this structure; deletes lower to hub ops. Merge primitives evaluate against a cloned Database, guarded dynamically: a result that is not an argument echo or the unit rep aborts the run BEFORE any host mutation, caches the primitive as uncompilable (eg.unsafe_prims), and falls back to the interpreter. Merge table lookups (MergeFn::Function/Lookup) are gated out; writes must live in one loop with one write-bearing leaf (per-leaf phasing comes later). Unit tests pin: UnionId folds colliding writes with existing rows, hash-cons respects existing keys through the hub, mint ordering and counter advancement, and AssertEq violations surface as the host's error with no host mutation. Corpus 131/131; mini-path and math outputs unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
run_schedule hook (done, needs review), primitive metadata, keyed get-fresh!, and the shared append-only interner — in payoff order, with nested loops and multi-leaf phasing on the critical path needing no shared-crate changes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The schedule engine compiles an entire ScheduleSpec tree (Run/Repeat/
Saturate/Sequence, spliced rebuild included) into ONE differential
dataflow: a stateful ScheduleEngine operator walks the schedule as a
stack machine, fires monotone-fire rule turns, evaluates merges/mints/
set-if-empties, and emits row deltas; DD does only the incremental
joins, fed back through a root-scope Variable so round r effects match
at r+1. Replaces the merge-hub prototype (deleted).
Performance work, verified bit-identical on math-microbenchmark at
every step (run9/run10/run11 = ~1.0s / 6.8s / ~103s vs the hybrid's
0.8s / 5.5s / 70s; the first working engine was 16.6s / 231s / n.a.):
- cost-based join ordering in plan_join_with: per-view row counts +
sampled per-column distincts, exhaustive permutation scoring (rules
have <=4 atoms). One bad body order (factorization rule joining
Mul x Mul on one shared var) was 90% of all arrangement traffic.
- width-ladder monomorphization of the engine dataflow ({8,16,32,48}),
as the fused path already did; the engine ran everything at RowN<48>.
- one partition demux by (func, loc) instead of ~85 per-view filters
(Tee clones every batch per subscriber), and one N-way concatenate
for match streams instead of ~200 chained binary concats.
- engine feedback in the flat root u32 scope (4-byte timestamps, no
subgraph layer); completion is probe.done() after dropping inputs.
- shared (view, key-cols) arrangements on both sides of first joins.
- per-timestamp buckets in the engine's pending queue (the BinaryHeap
did 73.5M pushes of 72-byte payloads on run 11).
- replay cache for quiescent schedules keyed on spec + a global
row-event watermark: print-size/print-stats each splice a rebuild
schedule that cost ~6s at run-11 scale to fire nothing. Only no-op
runs are cached (budget-limited runs must re-run).
Also: env-gated diagnostics (EGGLOG_DD_ENGINE_DEBUG phase laps, turn
gaps, per-rule match traffic; EGGLOG_DD_VOLUMES arrangement volumes;
EGGLOG_DD_NO_ORDER planner escape hatch) and an optional pprof feature
writing per-invocation flamegraphs. ScheduleLeafReport gains Clone.
Corpus 131/131, dd unit+integration suites green, egglog suite 996/0
(the one smoke failure predates this branch). Remaining gap vs the
hybrid is measured: 73.5M match deltas through the engine on run 11,
56% from the Add-associativity rule; next step is the persistent
cross-invocation dataflow per the design doc.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Compiled schedules now keep their dataflow alive across invocations: a thread-local cache (keyed by EGraph instance id + spec fingerprint) holds the timely worker, boot input, probe, and channels; the engine's arrangements, table state, and match sets persist, so re-running the same spec pays only for new deltas instead of rebuild + reseed + full join recompute. Eleven separate (run 1)s now cost the same as one (run 11) — 91.6s vs 95.4s at run-11 scale (103.1s with persistence disabled via EGGLOG_DD_NO_PERSIST=1). Mechanics: - The engine emits its own seeds on first boot (distinct LOC_SEED_* codes route into join views but are filtered from the host-apply sink), so there are no per-table input sessions; the only input is the boot session. - A BOOT marker delta resets the scheduler PC per invocation; the host steps with a chase loop, keeping the input frontier one round ahead until the engine signals done, then drains. Rounds continue monotonically across invocations (timely time cannot rewind). - Reuse is guarded by watermarks: global row-event counter (mutation_counter in record_row_event), fresh-id position, and a new rules_version bumped on rule add/free. Any foreign change drops the entry and rebuilds; error/unsafe outcomes also drop it (the engine stops mid-pass). LRU-capped at 4 entries per thread. - Fired-flag soundness across passes: delete/subsume-capable rules reset their fired flags each pass. A fired delete whose row was re-added in the SAME round never sees its match retract (the -/+ pair cancels in the dataflow, where the interpreter's physical row timestamps would re-trigger it). Pure writers keep their flags, matching interpreter seminaive. Caught by the integer_math corpus test (341 vs 331 Adds). - Per-pass mint accounting (was cumulative since construction). Also: EGGLOG_DD_DUMP_APPLIES diagnostic; invocation watermark trace under EGGLOG_DD_ENGINE_DEBUG. Validation: corpus 131/131, dd suites green, egglog suite 996/0, math run9/10/11 single-invocation outputs bit-identical to prior DD references; split-run files semantically identical to the mainline backend (modulo print-stats: DD reports lack per-rule num_matches — a pre-existing backend-wide gap — and the term encoding's rulesets don't exist on mainline). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
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 |
Sort each round's raw match deltas and net equal-binding runs by sequential scan instead of hash-map netting; per-(leaf,rule) state is fetched once per group. Also: raw-volume counter, per-table emitted-row classification and distinct-match totals under the debug env vars, and a turn-trace diagnostic (EGGLOG_DD_TURN_TRACE). Measured ground truth recorded in the design doc: 62.6M netted deltas vs 17.26M distinct matches (4.26x re-derivation), churn dominated by canonicalization rewrites (not epoch columns), and a negative result — in-dataflow presence-edge distinct is exact but ~2x slower single- threaded, and differential's distinct_total emits spurious edges inside this feedback cycle (use reduce-based distinct in cycles). Corpus 131/131, run9/10/11 and split-11 outputs verified; split-11 driver now 74.7s (was 91.6s). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
saulshanabrook#12) First validation for the FlowLog-style re-architecture. Propagates min-labels (= egglog's union-find leader) to a fixpoint in a nested `iterate` scope, feeds the result to a downstream join, and counts how many tuples that join receives. `consolidate()` after the loop cuts reception from 17 (every intermediate label 5->4->3->2->1 leaks) to 5 (the net) — the exact mechanism that turns the flat engine's herbie blow-up (67M match deltas for 172K real emits) into per-epoch net. Confirms: (1) the churn is a flat-timestamp artifact, not inherent; (2) `consolidate` after `leave` is necessary and sufficient to contain it (DD's iterate does not auto-consolidate); (3) the label-propagation rebuild formulation composes with a downstream stratum. Standalone, touches no production code. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Pick-up-later summary of the branch: hybrid-parity perf, the churn wall that reframed the design, the FlowLog-style nested-iterate-scope vision, the egglog<->FlowLog mapping, prototypes that de-risk it, the lessons from failed attempts (seminaive-under-merge, content-addressed minting key requirements, lossy hash-cons, scope flattening), and the concrete next steps. Co-Authored-By: Claude Fable 5 <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
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.
Competitor to #29 (the hybrid): instead of host-side scheduling calling DD per ruleset-iteration, this compiles an entire
ScheduleSpectree into one differential dataflow and keeps that dataflow alive across invocations.Stacked on #22 (relations encoding) and #29 (perf work) — review the last three commits (
e0e39533,f6ea25de,91bbd181) for the new material.Design
ScheduleEngineoperator walks the schedule (Run/Repeat/Saturate/Sequence, spliced rebuild included) as a stack machine: it fires monotone-fire rule turns, evaluates merges (UF min/max cascades run as waves within one timestamp, not consuming schedule budget), mints, hash-conses, deletes/subsumes. DD does only the incremental joins. Effects feed back through a root-scopeVariable, so round r writes are matchable at r+1. Onerun_schedulecall = boot, chase rounds to completion, apply net deltas to the host.(run 1)s now cost the same as one(run 11).plan_join_with(per-view row counts + sampled per-column distincts, exhaustive over ≤4-atom rules). One body-order join in the factorization rule was 90% of all arrangement traffic.Numbers (single thread, math-microbenchmark)
(run 1)(driver pattern)* mainline re-runs from its native rebuild; the DD gap is per-tuple economics, not invocation overhead (now ~ms). Remaining engine-path costs are measured: 73.5M match deltas of re-derivation churn (56% from Add associativity alone) and arrangement maintenance.
Semantics notes (found by testing, worth review)
integer_math(341 vs 331 Adds).(run n)would skip real work.num_matches, so(print-stats)differs from mainline.Validation
Corpus 131/131 (shared snapshots with mainline), dd unit/integration suites green, egglog suite 996/0, run9/10/11 outputs bit-identical to the pre-persistence engine, split-run programs semantically identical to the mainline backend. One smoke failure (
backend_generic_reads_work_without_an_action_registry) predates this branch.Design doc with the full perf history and the delta-feeding (v2) plan:
dd/docs/rebuild-in-dataflow.md.Diagnostics:
EGGLOG_DD_ENGINE_DEBUG(phase laps, per-turn gaps, per-rule traffic),EGGLOG_DD_VOLUMES,EGGLOG_DD_NO_ORDER,EGGLOG_DD_NO_PERSIST, and approffeature writing per-invocation flamegraphs.🤖 Generated with Claude Code