Measure rebuild/search cost; make the @UF clear opt-in - #44
Closed
oflatt-claude wants to merge 118 commits into
Closed
Measure rebuild/search cost; make the @UF clear opt-in#44oflatt-claude wants to merge 118 commits into
oflatt-claude wants to merge 118 commits into
Conversation
Groundwork for a declarable "any-of" index. A ColumnIndex keyed on a set of columns already maps each value appearing in any of them to the rows holding it -- the disjunctive counterpart to the tuple indexes in `indexes`, and the structure SortedWritesTable::rebuild_index uses. Only the catalog assumed a single column, so add `occurrence_indexes` keyed on a column set alongside it. ColumnIndex::add_row posted a row once per column, so a value sitting in two indexed columns of one row appeared twice in its posting list. The native rebuild hides this by collecting candidates into a HashSet; a consumer that treats the index as a relation cannot. Post each distinct value once instead. The scan is over the indexed columns only, so the single-column case does no extra work. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
An occurrence atom binds a variable to a value appearing in *some* one of a set of columns, and is serviced by the occurrence index. This is the query form of "which rows mention this term", which a rebuild needs and which an ordinary atom cannot express: a variable repeated across columns constrains them to be equal, where this reads them disjunctively. - Atom::occurrence records the variable and its column set. The variable is not a column of the table, so it stays out of the var/column bijection. - QueryBuilder::add_occurrence_atom registers the column set as the variable's foothold in the atom, so the planner probes once the variable is bound. - get_index routes such an atom to the occurrence index. No new plumbing: the probe key comes from the *cover's* columns while the index is built from the probed atom's, so "several indexed columns, one-value key" was already representable. - The atom can only be probed. Scanning it would have to yield one binding per distinct occurring value, so the occurrence variable must be bound by another atom; building a query that does not is an assertion failure rather than silently wrong results. - compile_stage's generic-join path collapses a subatom to vars[0], which is sound for a repeated variable but drops all but the first occurrence column. Such stages take the fused path, which keeps the whole set. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
query_table_by_occurrence adds a table atom that also binds a variable to a value occurring in some one of the given columns. No index declaration is needed: the planner builds the occurrence index on demand, so the column set on the atom is the whole input. A rule's staged atoms were a (table, entries, schema) tuple, destructured in several places that only wanted the schema. They are now a QueryAtom struct, so the occurrence spec is a named field rather than a fourth tuple slot. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Declares a read-only relation over a function's rows: each value appearing in any of the listed columns, followed by the whole row. Querying it is an ordinary body atom, so no new fact syntax; the backend builds the occurrence index the first time a rule probes it, so the declaration binds a name and registers no runtime state. The columns cover the function's inputs *and* its output, so a value is found wherever it sits in the row. `(any ...)` is an extractor over the row rather than a fixed keyword, leaving room for others -- indexing the elements inside a container column would give container rebuild the delta it currently lacks. The term/proof encoding rewrites a function into a view whose columns differ, so a declaration written against the user function would silently point at the wrong ones. It is reported unsupported there rather than passed through. The DD backend has no occurrence index over its mirror, so it rejects index atoms rather than answering them wrongly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The encoder emits one index per view per child eq-sort, covering the children and the e-class, and one rule per sort: an @uf edge joined against that index reaches every row mentioning the moved term, and the action canonicalizes the whole row. This replaces the per-column fan-out and folds the separate e-class rule into it. Two children moving in one iteration therefore fire twice with the same result rather than each leaving a differently half-rewritten row behind. Canonicalizing a term in an action needs its @uf row read there, so eq-sorts register uf_canon / uf_canon_proof: the generic view-column read over the two-output @UF_<S> table, with the term and its reflexive proof as fallbacks. The rule is :unsafe-seminaive, and the driving @uf delta in its body is what makes that read sound. Three fixes in the occurrence-atom plumbing, all found by measuring this: - compile_stage pushed any stage touching an occurrence subatom off the generic-join path, which cost 20-160x on math-microbenchmark for an identical database. SingleScanSpec now carries the occurrence columns instead, so the scan reads them disjunctively; a bare column cannot say whether it means the variable at that column or a value occurring in the set. Occurrence scans also bypass the per-column trie-node cache, whose key has the same ambiguity. - get_index ignored the atom's subset for occurrence probes, so a probe answered from the whole table and discarded the seminaive timestamp bound. - It also ignored the heuristic choosing between the cached whole-table index and one built over the subset -- the latter being exactly the delta case. The Differential Dataflow backend serves index atoms by deriving the occurrence view where it already feeds row deltas: one (value, row...) per distinct value a row holds in the indexed columns. A read key carries those columns as a bitmask so it stays Copy. Proof snapshots are regenerated: the different rebuild order yields different derivations, which the proof checker validates in proof-testing mode. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
proof_encoding.md still described the per-column fan-out this replaced. Its rebuild section now shows the declared index and the single index-driven rule, checked against the generated program. Trim the comments the change added to the caller-facing contract: drop the rationale for the read key being a bitmask, the cost argument for the trie-node cache, why a bare column cannot express an occurrence set, and a note justifying an assert over an error. Drop QueryError::UnboundOccurrenceVar, which was never constructed -- the check is an assert at query-build time -- and stop linking a public method's docs at the private Atom::occurrence. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Wrong results, in order of severity: - A reused TrieNode cleared its column and child caches but not the new occurrence one, so an occurrence atom refined by an outer stage kept the index built over the previous frame's subset. This produced tuples matching no row. - ColumnIndex::merge_parallel still posted a row once per column, so above the parallel-refresh threshold a value in two indexed columns returned its row twice. The serial path was already fixed; this is the same bug in the other half, and it predates the occurrence work -- rebuild_index has it too. - The index-driven rebuild composed a *custom* function's output with the e-class shape `Trans(Sym …)` rather than `Congr` at its position, and indexed that column as well, so the column got two rules and an unprovable row proof. Only an e-class takes that shape; a custom output keeps its own rule. - Index atoms dropped ReadMode, so they matched subsumed rows where a plain atom would not -- and the DD backend, which honours it, disagreed with the reference backend on the same program. Panics on ordinary input: - Tree decomposition and the MinCover/PureSize planners reason about an atom's variables through its columns, and an occurrence variable has none, so they could not see the edge to the atom binding the value: any rule with an index atom and three or more atoms panicked. Such a query is now planned whole with generic join, forced at build so a later set_plan_strategy cannot undo it. - Repeating the indexed value at a row column gave the variable two footholds in one atom and a stage probed that atom twice. When the repeated column is one of the indexed ones the occurrence is implied, so the atom is an ordinary one; otherwise it is rejected, as no single probe serves it. - An index value bound by no other atom aborted inside core-relations. It is now a spanned type error naming the index and the variable. - set/delete/subsume on an index aborted with "no entry found for key" instead of the error its docs promise. Tests: index_any.egg only had two-atom rules, which is why none of the planner defects showed up. It now covers a three-atom rule, a cover binding two variables of the index atom, and the value repeated at an indexed column. custom-eqsort-output-rebuild.egg covers the proof regression, which no corpus file exercised. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The two wrong-result bugs had no test, and one of the tests written for them did not actually discriminate: - The stale-occurrence-cache case needs several bindings that cross-combine the cover's two variables, so a trie node is reused with a different subset. The simpler two-row version passes either way. The new case reports a row that does not exist and loses two that do when the cache is not cleared. - The parallel index build has its own dedup path and its own threshold, so it needs a table over 20k rows and more than one thread to reach. Verified both tests fail with their fix reverted. - An index must read the same rows the function itself would, subsumption included; a rule going through the index and one going direct now have to agree. Two plan shapes remain that an occurrence index cannot answer, both unreachable from egglog source: a probe spanning the indexed columns *and others* (no single index answers it, and a tuple index over the union would read them conjunctively and drop rows), and a cover that would bind the occurrence variable by scanning, which has no column to bind from. Both were silent -- the first a wrong answer, the second a bare unwrap -- and now say what is unsupported. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A probe can ask two things of the same table: whether a value sits at given columns, or whether it occurs among them. get_index was deciding which by comparing the requested column set against the atom's indexed one, so an ordinary variable repeated across exactly those columns was served disjunctively -- right only because the atom's Eq constraints filtered the extra rows back out. ScanSpec now carries the occurrence columns, as SingleScanSpec already did, and get_index is told. Both are populated by one predicate over the subatom, so the two paths cannot drift. This is well-defined because the generic-join path builds one ScanSpec per subatom, and a subatom belongs to a single variable. The decomposition prologue does merge subatoms across an atom's variables, which an occurrence read cannot share -- but a query containing one is planned without decomposition, so that path is not reached. Also fixes a false rejection introduced with the unbound-value check: the value may sit at a column of the index atom itself, which binds it and makes the occurrence redundant. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The MinCover and PureSize planners map a subatom's columns back to its variables, which an occurrence variable has none of, so a query containing one is planned with generic join whatever was asked for. That was asserted but not covered; requesting either strategy explicitly now has to still answer correctly rather than panic. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The occurrence concept was explained in four places; it now lives on Atom::occurrence and the rest refer to it. Drop the rationale for where a check is placed and for why a parameter exists, keeping the guarantee callers rely on (the plan strategy cannot be overridden). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A printed rule proof's `(substitution …)` list came out in hash order over the variable names. Those names are generated symbols, so any change to how many proof nodes are minted reshuffled the whole list and churned the snapshots. `compute_rule_substitution` already walks the body front to back, so the insertion order was first-appearance order all along — it was just discarded by `HashMap`. Keep it with `IndexMap`, and unify a custom function's arguments before its output so `(= (f a b) v)` reads a, b, v. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The proof checker replays a rule head into a set of propositions, which throws away which position in the head produced which proposition. A proof that names its conclusion by position needs that mapping, and the position has to mean the same thing to the encoder as it does to the checker. `proofs::proof_sites::conclusion_sites` is now the single numbering of a head's conclusion sites: actions in order, and within an action the pre-order of its expressions, with a `union` also contributing the equality it writes. `process_actions` is driven by that enumeration instead of its own match over action kinds, and reports the proposition each site resolved to alongside the unchanged set of propositions. No consumer of the set changes and no proof output changes. `conclusion_sites_index_every_rule_head_proposition` makes the indexing contract a test rather than a comment: the sites are the pre-order of each action's expressions, they are numbered densely from zero, and processing a head resolves each of them, in that order and orientation, to a proposition the head implies. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Proof encoding is meant to run early, so later passes need not know proofs exist. `ast::cse` runs before it and reshapes rule heads, which leaves the encoder looking at a different head from the one the proof checker replays — so a conclusion-site index assigned by one side does not resolve to the same site on the other. Aligning the two heads would entrench the inversion, so the pass is off until it can run on the encoded program instead. Everything switched off for the rework hangs off `PROOF_REWORK_IN_PROGRESS`, so the set is greppable from one place. Without the prepass the term encoding makes less progress per bounded run, so `integer_math.egg` (`(run 4)`) no longer ends on the same e-graph under the native and term-encoding treatments. That cross-treatment check is suspended for it by name rather than by accepting a snapshot that records the divergence. Four proof snapshots move; no proof fails to check. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…fact `(run N)` is N iterations under either treatment, so the tuple counts must match exactly. The term encoding reaching `(Add 121)` where native reaches `(Add 331)` means it is not executing the schedule faithfully — CSE was masking a real defect rather than merely making the encoding faster. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Records the design, the phase gates, the open questions, and the two detours found so far: the begin-block defect CSE was masking, and the measurement caveats that hold while CSE is off. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Phase 1 of the proof-encoding rework: prove that a rule proof needs only (rule name, premise proofs, position in the head), not a stored conclusion term. Nothing is deleted and no emitted proof changes. `proof_reconstruct_check` replays every checked `Rule` node's head under the recorded substitution and reports which of the head's `conclusion_sites` reproduce the conclusion the proof records. It replays a second time under a substitution rebuilt without reading any premise proof that exists only to carry a value, recomputing those variables from the rule body with `prim.validator()` — what a term-free justification would have to do. Over the `proofs/` corpus, 13438 nodes: 12530 reproduce the conclusion at exactly one site, 646 at several (always a reflexive `t = t` concluded at repeated head positions), 262 at one site reversed (always a `union` recorded the other way round, so the reverse must come out as `Sym` of a site). None failed to reconstruct, and the payload-free substitution agreed on every node. `bind-prim-result.egg`'s `res` recomputes to `"hello world"`; the same holds for a `(Vec i64)` and a `(Map String i64)` read in a rule body. The check is off unless `EGGLOG_PROOF_RECONSTRUCT_CHECK=1`, which logs one line per node at `info`; a test drives it directly and asserts agreement. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`register_set_if_empty` looked its key up in the committed table and, on a
miss, staged an insert. Two calls with the same key inside one action batch
therefore both missed and both inserted, minting two e-classes for one term.
Native `lookup_or_insert` reads through the batch's predicted rows instead, so
the treatments disagreed and the term encoding ran exactly one iteration
behind:
(datatype Math (Sub Math Math) (Const i64))
(rewrite (Sub a a) (Const 0))
(let $e (Sub (Const 2) (Const 2)))
(run 1)
(print-size Const) ; native 2, term-encoded 1
Route it through a new `TableAction::lookup_or_insert_vals`, which uses
`predict_val` with caller-supplied value columns rather than a minted default.
This is the defect the CSE prepass had been masking since PR saulshanabrook#35, so the
cross-treatment check suspended for `integer_math.egg` is restored — it now
agrees with CSE still off. The fix is strictly stronger than that prepass,
which only caught textually identical duplicates within one scope.
Two proof snapshots record a different, still-verified derivation now that a
duplicated subterm shares one node.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Measured on this branch the rollback-log fix is ~1% slower, not the ~12% faster it is on main — CSE being off means the hoisted global tables that make the O(rules x tables) term large are not there. Revisit in phase 5. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Adding the conclusion-site index and removing the skeleton fail differently, so gate them separately: 2a proves encoder and reconstructor agree on which site a proof came from while the old conclusion is still there to disagree with. Records the three hazards for assigning the index. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Phase 2a of the proof-encoding rework: the encoder records *where* in a rule head a proof's equality comes from, and proof conversion derives the equality by replaying the head at that site instead of reading the node's stored `Ast` columns. Nothing is deleted — the `Ast` columns and the RHS skeleton stay, so the old conclusion is still there to disagree with. `Rule` gains a fifth column, an `i64` holding `SiteRef::encode()`: the site index and a direction bit packed as `2 * index + reversed`. One packed column rather than a `Sym` wrapper or a second column because a `union`'s direction is not known when the rule is encoded — the `@UF` edge runs `ordering-max = ordering-min`, so which operand lands on the left depends on the ids the firing sees. The encoder emits `(proof-of-max lhs <forward> rhs <reversed>)`; that primitive is typed `(T, P, T, P) -> P` for any `P`, so it selects between two `i64`s by the same value ordering `ordering-max` uses. A `Sym` wrapper would have changed the emitted proof, which this phase must not do. `proof_sites` gains `action_sites`, the same numbering as `conclusion_sites` shaped like the head — per action, its own conclusion's site plus an `ExprSites` tree per operand — from the same walk, so there is still one numbering. The instrumenter carries a node's `ExprSites` down as it recurses rather than counting, since it emits post-order. Sites are assigned to the head as written, before `normalize_union_operands` and `plan_construct_into` run: each normalized action keeps the `ActionSites` of the action it came from, and the construct-into plan captures the site of the `union` it drops, oriented `target = guest` the way the guest's view row states it. `proof_reconstruct_check` now also reports whether the stamped site reproduces the recorded conclusion. Over the `proofs/` corpus, 13392 nodes: 12632 where the stamped site is the only site that reproduces the conclusion, 760 where it is one of several (all the reflexive repeated-subexpression case), 0 where it does not. 558 stamps are reversed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Proof node counts move as the hash-consing key changes, but a view row count moving means the e-graph diverged. Zero shared snapshots have changed across phases 0-2a; state it as a rule rather than leaving it implicit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Phase 2b of the proof-encoding rework — stop emitting the RHS
`Congr`/`Trans`/`Sym` skeleton and have proof conversion synthesize it from
`(rule name, premise proofs, conclusion-site index)` — cannot be done as
planned. Part of that skeleton states equalities the head never concludes, so no
site index can name them and no replay can rebuild them.
The step that does it is the canonicalization bridge. A head that builds a term
interns each subterm into its view; when `set-if-empty` returns an *existing*
e-class, that e-class's term row may hold a differently shaped term. The two
shapes are equal in the e-graph but they are different terms, and the proof
saying so came from whichever *other* rule firing made them equal — it is
neither a site of the head under construction nor one of its premises. It
reaches the head only as the `Congr` child `build_natural_with_congr` folds on.
`proof_reconstruct_check` now counts these bridges, so the amount of the
skeleton that is runtime data is measured rather than argued: over the `proofs/`
corpus, 2082 bridges are the identity on terms and 240 move the term. Deleting
the chain (`nat_to_dedup := nat_prf`) fails 28 of the 206 `proofs/` tests, every
one at conversion time with `transitivity requires matching middle terms` — the
view row's proof stops ending at the term the row's children spell, so nothing
composes with it. `head_canonicalization_bridge_is_load_bearing` pins the
smallest program that needs one.
A second, independent blocker: the "zero changed proof snapshots" gate cannot
hold for *any* phase that changes how many proof nodes a firing mints. Seven
`proofs/` snapshots print rule-body variables that `proof_normal_form` names
from `symbol_gen.fresh("v")` — the same counter `fresh_var` mints proof-node
variables from — so one node fewer renumbers every later `@vNNN`. Measured with
an output-equivalent reduction of the statically-trivial composites, written up
under "Available now": 7 snapshots changed, all 7 diffs nothing but the
renumbering. Both blockers, the reproducer, and what a working 2b has to carry
are in `proof_encoding_rework.md`.
No encoder change: a rule firing still writes the same nine proof rows plus four
`@Ast` rows, and the `proofs/` corpus, the shared snapshots and the harness
counters (13392 nodes, no stamped site disagreeing, no substitution needing a
carried value) are unchanged.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`fresh_var` shared the `"v"` hint with the rule-body variables that `proof_normal_form` names, and `SymbolGen` counts per hint — so minting one fewer proof node renumbered every later body variable. Those names are printed in a proof's `substitution`, which made "this phase changes no proof output" an impossible claim for any change to how many nodes a firing mints. Separate hints, so the two no longer interact. Verified by doubling every temporary: zero snapshots change, where nine did before. Eleven snapshots are re-blessed once for the renumbering this introduces; every diff is a name change with no structural difference, and no proof failed to check. View row counts are untouched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The interned subterms' view-row proofs become trailing premises of RuleN. They are already read at no row cost, and cannot be hoisted to the front because an outer view's key comes from its children's deduped ids. A sentinel fallback distinguishes a newly interned subterm, whose row proof would otherwise be the node being built. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A rule head used to write out its whole `Congr`/`Trans`/`Sym` composition as proof rows: the chain moving each built term onto its children's representatives, the reflexive proof of the canonical form, and the connector between them. All of it is determined by the rule text, the substitution, and which e-class each interned subterm landed in, so a firing now writes only the proofs it *stores* — a term proof, a view row, a union-find edge — and proof conversion rebuilds the composition around them. Three pieces: * `SiteRef` gains a `SiteRole`, packed into the same `i64` column, naming which of a site's propositions a `Rule` row states. A build site needs three the head does not conclude (as written, over canonical children, and the edge between them); a `union` and a construct-into guest need their own. * `proof_head_skeleton.rs` owns `HeadPlan` — union-operand normalization plus the construct-into plan, moved out of the encoder — and derives from it, per build site, its children's build sites and the order the head builds them. The encoder and conversion both read it, so neither mirrors the other. * `Rule` gains a second `ProofList` column: the body premises extended with the view-row proof of each interned subterm. The two lists share cells, so recording both costs no rows and their length difference is the bridge count. A row the head's own `set-if-empty` seeded is absent when `view-proof` reads it, so the read returns a proof about the term as written; only a proof whose rhs is the canonical term names an e-class, which is the discriminator. Only roled rows record bridges, and conversion converts only the ones the requested role is composed from, so a term-proof anchor still reaches nothing but its own premises. A `(rewrite (Add a b) (Add b a))` firing writes 6 proof rows instead of 9 and 2 `@Ast` rows instead of 4; a nested `(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))` firing writes 13 instead of 22. The `proofs/` corpus passes with no snapshot changes. Known regression, written up in the rework plan: `egglog-experimental`'s `eggcc-2mm-pass1` proof fixture overflows the stack in `ProofExtractor::extract`, whose depth is one frame per premise-list cell — 15 frames on that fixture before, over 2000 now. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Phase 2b's bridge premises are a cons list, so on `eggcc-2mm-pass1` the extracted proof term's depth went from a measured 15 to over 2000 and the fixture died of a stack overflow. A test runs on a spawned thread, so the whole read has 2 MiB to work in. Both readers of the extracted term recursed once per level. `RootExtractor` now drives its search from an explicit stack of frames. A frame records which reconstruction its node is trying -- a container's elements, a table row's children, or the canonical representative -- and the driver resolves one child at a time. It visits the same functions and rows in the same order, so it produces the same term. `RawProofStore::from_extracted` now parses a term's nested proofs deepest first on an explicit stack, in the order `parse_proof` would, so `parse_proof` finds each one already parsed. `parse_proof_list` also walks the cons spine with a loop. Measured with a per-routine stack probe, parsing peaked at 2.3 MiB before and stays under 256 KiB after -- as do `convert_raw_proof`, `simplify` and `check_proof`. Nothing about what a rule firing emits changes: the commute rule still writes 6 proof rows and 2 `@Ast` rows, and no snapshot moves. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Merge bodies already mint no @ast, and top-level actions are not sited yet rather than unsiteable — the design already gives them a program-site index. Also records the row budget, the order to take the remaining work in, and the untraced 2000-cell bridge depth. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`RootExtractor`'s `Stage::Eq` search ran a full `for_each` over every
candidate function's rows for every extracted node, then sorted the
matches, so extraction cost O(nodes x rows). The quadratic is
pre-existing; phase 2b of the proof-encoding rework raised the node
count enough to make it the dominant cost.
Each candidate function is now read once per extraction run into
`ScannedRows`, keyed by its index in `EGraph::functions`: the
non-subsumed rows concatenated into one `Vec<Value>`, a permutation
ordering them by extraction output value and then by whole row, and a
map from output value to that group's range in the permutation. The
search takes rows from the group instead of rescanning.
The chosen term is unchanged. A group is still ordered lexicographically
by whole row, so the search still reconstructs from the
lexicographically-smallest matching row and stays independent of the
backend's row iteration order (see `prove_exists`). The candidate filter
is untouched. Only functions the search actually consults are read, and
the index dies with the `RootExtractor`.
Measured --release on a 128-core box at load ~23; test-phase wall time
and peak child RSS:
egglog-experimental --test files (46) 200.4 s / 5.36 GB
-> 28.8-29.3 s / 4.3-5.2 GB
proofs/eggcc_2mm_pass1_proof_testing 202.8 s / 3.26 GB
-> 31.6 s / 3.29 GB
egglog --test files 'proofs/' (206) 9.16 s / 6.06 GB
-> 8.96-9.22 s / 5.90-6.07 GB
Whole-suite RSS is the peak of whichever tests overlap, so read the
single-fixture row: it moves under 1%. The small corpus is unchanged
because its tables are too small for the rescan to have dominated.
206 proofs tests pass with zero snapshot changes and no shared-snapshot
diff.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The runtime simplifier rewrites Sym(refl) -> refl, Trans(refl, p) -> p, Trans(p, refl) -> p and Congr(p, i, refl) -> p, so a step composed onto a reflexive proof is minted as a row and then discarded when the proof is read. The encoder knows statically which proofs are reflexive, so it can apply those identities itself and never write the row. ProofInstrumentor carries a `reflexive` set of emitted proof-variable names -- fresh_var names are globally fresh, so entries never collide across generated programs -- and mint_sym / mint_trans / mint_congr consult it. Two things enter the set: a body variable's <S>Proof read, and term_proof_with_asts's Rule / Fiat result, whose two AST endpoints both wrap the same value. edge_proof_with_asts mints its endpoints over two different values, so its rows stay out. What this deletes from a rule head is the body-premise composition. In proof normal form a matched call appears as (= var (call ...)), whose fact proof was Trans(Sym(var_proof), call_proof) with var_proof the variable's reflexive term proof; both nodes go. Every other rule-head site was already deleted by phase 2b, which records a roled row instead of the composition. The remaining collapses are on the paths phase 2b leaves alone: top-level actions and merge bodies. Rows written per rule firing, from --proofs --mode desugar: (rewrite (Add a b) (Add b a)) 6 -> 4 (rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c))) 13 -> 11 @ast rows are unchanged at 2 and 6. Zero snapshot movement, which is the point: the deleted nodes are exactly the ones simplify was already removing, so the printed proof is byte-identical. 206 proofs/ tests pass with no changed snapshots and no changed shared snapshots. proof_reconstruct_check is unmoved as well -- 13392 nodes, 0 stamped_wrong, 0 payload-free failures, 3540 canonicalization bridges of which 288 move the term, all identical to the phase 2b baseline. This is the first half of step 3 of the sequenced plan, ported from the abandoned reduce-proof-writes branch (0b79259, 6dd5366, fc1aada). The second half, fused Rule0..Rule4 carrying premises inline, is untouched: its arity has to cover the phase 2b bridge list, which needs a design decision first. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Where there is no rule head to replay, the encoder runs the proof algebra itself and wrote a `@Sym`, `@Trans` or `@Congr` row for every step of the walk: a top-level action, a merge body, a rule body's premises. The shape of that walk is fixed while lowering, which is the same property that lets a view rebuild and a merge collision each ship their composition as one packed row. So those sites ship theirs too. `mint_sym`/`mint_trans`/`mint_congr` no longer emit; they build a `Composition` over the proof names in scope, and the row is written where a statement reads the name — one `@Packed_<spelling>` for the whole tree, or the plain constructor when the tree is a single step. `Composition::pack` lays the tree out as a skeleton over the row's columns, sharing a column between equal subtrees, so `reflexive` carries its one operand once rather than twice. That is what relaxes `Skeleton`'s column check from "named exactly once" to "columns are 0..n": `trans_sym_p0_p0` is a one-column row. Two things bound what a row spells, since a name that grew with the term would be a table per term shape. A composition nothing reads is never written — the connector of a top-level term nobody builds on. And a term whose children moved seals the connector it hands its parent, so the level above holds a column here instead of spelling this level out again; a row is then a function of the term's arity, not of its size. `(Add (Num 1) (Num 2))` at top level: 9 `@Proof` rows to 4. `(Neg (Add (Num 1) (Add (Num 2) (Num 3))))`: 24 to 11. A custom `:merge` body: 4 to 3. Per firing, unchanged: a flat rewrite 2, the nested head 6, a view rebuild 1, a merge collision 1. Across `egglog/tests/**/*.egg` the rows a top-level block writes go 9879 to 5028, and every line that changed is composition rows becoming one packed row. The `@Fiat` conclusions stay. A fiat is composed from nothing, so it cannot be a hole of a skeleton, and each is stored under its own term; the six `@Ast` rows in the example are its endpoints and stay with it. The cost is constructors: distinct `@Packed_*` across the corpus goes from 15 to 78, 44 in the largest single program, because a step reached through a moved child spells `sym p<n>` where one reached through a sealed connector spells `p<n>`. The longest name is unchanged at 239 characters — still the 16-column view rebuild's — with the widest new one at 151. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A packed row's constructor spelled the composition it stands for, so a name was a table and the corpus had 78 of them: a step through a leaf child spells `sym p<n>` where one through a sealed connector spells `p<n>`, which is a shape per arity per moved-child pattern. The widest name ran to 238 characters. The skeleton is data, so the row carries it: a leading `String` column spelling it, and `@Packed_<k>` for a row of `k` proofs. That is 13 constructors, and it makes a packed row the same shape as the rule proof beside it — `@Rule_<k>` already leads with the rule's name, and `packed_proof`/`packed_proof_columns` are now `fused_rule`/`fused_rule_arity` over a different payload. A column count alone cannot name the constructor while a congruence's child position is an `i64` column, since then two rows of the same width can have different column types — 26 distinct type patterns across the corpus, or 23 if the layout is reordered to put the proofs first. The position is a constant at every site that writes one, so it goes into the spelling instead. Every column is then a proof, which is also one less thing `Skeleton` has to be: a hole is a proof column and nothing else, so `width`, the column collection and `from_spelling`'s check lose their second case, `Composition::lay_out` stops allocating a column per congruence, `leaves` is what `pack` already returns, `nested_proofs` reads a packed row without parsing its skeleton, and `instantiate` reads the position off the term rather than out of a column. Dumping every `egglog/tests/**/*.egg` in proof mode before and after: with each packed row rewritten to the composition it states, the 109 that encode are identical. Per firing the rows are unchanged — a top-level `(Add (Num 1) (Num 2))` still writes 3 `@Fiat` and 1 packed, the nested example 11 — and the rows are narrower, the 16-column view rebuild's going from 34 columns to a string plus 18. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`defer_lookup` also took the variables its group reads, so the flush could emit those groups first. Both callers passed none: a group binds every proof it reads before reading it — the `Fiat` group mints its own `@Ast` rows — so the recursion never fired. Drop the parameter and the recursion. `Pending` is then just the statements, so the map holds them directly. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Statements and compositions were held back in maps of their own, flushed at the same point and discarded together, differing only in what a flush does with them: statements go out as they stand, a composition can still become one row. Say that with one map keyed by proof variable, whose value is either. The flush is then one lookup and an exhaustive match, so which of the two a variable is is a fact of the type rather than of the order the maps are consulted in. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Naming a head's proofs by position made conversion total where it had been partial: `Firing::column` walked the whole head, and a `Firing` was built per converted rule proof, so a head with n positions was walked n times over. Worse, a full walk reads a bridge premise at every built position, so each walk pulled in the conversion of every rule proof the firing passed over — and each of those walked the whole head again. `proofs/eggcc_2mm_pass1_proof_testing`, whose generated `initialization` rule has a 3154-`let` head, walked it 3149 times for 21,094,950 positions, and took 837 s against 25 s before. Two things bound it. A walk now stops at the action that fills the column it was asked for: columns are claimed in walk order, so one already filled is final. And the walk it stopped is kept, so the next rule proof of the same firing — same rule, same body premises — carries on from there instead of starting over. Between them the head is walked once, not once per proof: the same test now walks 3154 positions. What a walk may keep is bounded by the bridges the rule proof it is answering carries, which are only those recorded before that proof was minted. An action that asks for a bridge past them composes a connector the next proof would compose differently, so the walk is rewound to the action boundary before it and that action is redone. Nothing about the proofs changes: the encoding is byte-identical over all 109 `egglog/tests` programs that encode, the proof checker is untouched, and every snapshot stands. `cargo test --release -p egglog-experimental --test files`: 831 s -> 24 s. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A rule proof row carries exactly the bridges the head had interned when it minted the row, so replaying it takes them in the order the head built and needs no more than the row has. Hand the walk a supply it draws the next bridge from instead of a function of a bridge's position, which is what a replay of the head's own lowering does. The `wanted` column stops being state as well: it is an argument to the one walk that reads it, so `fill`, `filled` and `walk` collapse into one function. Measured over the 206 `proofs/` files and the 46 experimental ones: of 9695 columns read back, every composed one was filled before its row's supply ran dry, and in 6147 of them the supply ran dry on the very next bridge. The 42 columns read past a dry supply all hold an own conclusion, which composes nothing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
A row stating the head's own conclusion composes nothing, so it used to carry no bridge premise even when it sat thousands of columns into the head. The replay therefore could not treat the bridges running out as "this row has nothing more to say": it had to keep walking to the column it was asked for, past the point where the bridges stopped agreeing with the head. Now every row after the head interns a subterm is a RuleLink over the row before that interning, own conclusions included. A row's bridges then run out exactly once past the column it names, so running out is the whole of the stopping condition. The walk still finishes the action it runs out in — it discovers this mid-action, and the column it was asked for is in there — and hands the next row the state from before that action, which that row rebuilds with the bridge this one lacked. Same rows per firing, RuleLink swapped in for Rule_k: the 2mm fixture emits 9235 rule proof rows either way, 5155/4080 Rule_k/RuleLink before and 1063/8172 after, and every snapshot is unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`HeadLayout::new` walks the whole head, and `Firing::new` called it — so conversion laid the head out again for every rule proof row it read, including the rows that immediately throw the fresh walk away by carrying on from an earlier one. The plan is already cached per rule and the layout is a function of the plan, so the layout goes on the plan and both walks read it there. `HeadRun` is `Copy`, so sharing costs nothing, and the layout keeps its job of refereeing the encoder's walk against the replay's. Two more per-row costs in the same arm: the bindings a carried walk discards are no longer built, and the rule a proof names is found through a name index rather than by scanning a program that also holds a command per loaded input row. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`lookup_or_insert_vals` reaches `RowBuffer::add_row`, which only debug-asserts arity; the route it replaced normalized the row first. A short row would shift every later row of the fixed-stride buffer in release, so assert the arity against the table's own value-column count, as `lookup_or_insert_multi` already does. `RawProofStore::add_proof` hash-conses, so the four packed-row tests were handing `assert_agree` two equal `RawProofId`s and `same_proof` compared a proof to itself. That equality *is* the structural comparison: assert it, and drop `same_proof`. Premises pair with body facts by position only because `remove_globals` appends its lookups after the written facts. The test compared counts; compare positions. Also: say what `RuleColumns::premises` holds, and stop shadowing `proof_head::Firing` with an unrelated test type. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`reflexivize_premise` built `Trans(Sym(p), p)` with bare `id_to_proof` pushes while `proof_head` builds the same thing through `push_shared_proof`, so the two rows of one firing could reflexivize a premise to different ids — and the premise vector is both the head-walk memo's key and a rule proof's sharing key. `ProofAlgebra::reflexive` is that composition, over the shared builders. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`HeadProof::GlobalValue` was the one proof a head's walk filled with `None` and the one no encoder site named, so every head containing a `set` carried a padding column. A `set` claims its row and nothing else. `HeadPosition::Set` stays distinct from `Call`: the layout assertion is what catches a `set` lowered where the walk expects a call. Encoding change: a numbered column after a `set` shifts down by one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The rebuild skeleton was written twice — once where the encoder builds the row, once in the test that unpacks it — so the test round-tripped its own copy of the shape rather than the one the encoder writes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`Skeleton` and `Composition` were variant-for-variant identical; the only difference was what a leaf holds, and `Composition::pack` is the map between them. One `ProofTree<L>` says that, and gives `Composition` the `sym`/`trans`/`congr` builders it lacked. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Every constructor's arity and child positions were written twice, in `parse_proof_inner` and again in `nested_proofs` with a different scrutinee. A constructor added to one and not the other left only a `debug_assert`: in release, a deep chain through it overflows the stack instead of reporting anything. One table says how a constructor is read, and both derive from it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
- `RawProofStore::proof_to_term` was written on every parse and read nowhere; its doc called the pair a bidirectional map, which it is not. - `compute_rule_substitution`'s length check is unreachable: its one caller asserts the premises cover the body and then zips, which truncates to exactly that length. - `unify_fact` has one caller, in the same `impl`. - `is_custom_func_fact`'s reversed `Eq(Var, Call)` arm cannot match: proof normal form always writes the call on the left. - `stage_batch`'s row count is always positive — `run_instrs` returns on an empty mask and neither `Insert` nor `Remove` clears it — so the count, the return, and the branch on it do nothing. - `source_at` and `row_sources` re-matched `ValueSource` and `QueryEntry`, which `mask.rs` already does; both now live there. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The changelog entry described the encoding's internals -- which premises ride in which row, what a rebuild packs. None of that is visible to someone using egglog: the proofs are identical. What changed for them is that proof mode is faster and smaller. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The union-find's only readers are the maintenance rules: path compression, the rebuild rules driven by a @uf delta, and the container rebuild primitive. Once the rebuild loop saturates, every row a query, delete, or subsume can reach is canonical, so the edges that got it there are dead. Drop them, so the next iteration's rebuild reads only its own unions. A @uf_clear ruleset holds one :naive delete-everything rule per eq-sort and runs last in the maintenance schedule. Set EGGLOG_UF_CLEAR=0 to keep every edge, which restores the previous encoding byte for byte. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…t-in Clearing @uf each iteration is sound — 801 file tests pass with proof snapshots byte-identical — but it is not faster. The rebuild rule is :unsafe-seminaive, so its driving @uf atom already reads only the delta and the rows a clear drops are ones its join never visits. At 6 rounds it is 1.006x on math-microbenchmark and 1.027x with +43 MiB on eggcc-2mm-pass1: the clear costs +134 ms while @parent saves 27 ms. Time in @parent is 0.2-3% of wall, so a free clear could not win more. It also loses stale-value canonicalization, which find_canonical needs, and lets a rule re-deriving one union per iteration keep saturate from terminating. Now off unless EGGLOG_UF_CLEAR=1; the default encoding is unchanged byte for byte. rebuild_cost.md records that and what the search time is actually made of: the encoded rebuild is ~4.5x native's, native chooses its full-table-scan branch on 93-99.8% of rebuilds where the encoding can never scan, and the larger share of the gap on most files is in user rules rather than maintenance -- for reasons that are not join width, contrary to what the two desugared programs suggest. EGGLOG_REBUILD_TRACE=1 logs native's per-table rebuild branch and its inputs. Co-Authored-By: Claude Opus 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 |
Merging this PR will improve performance by 37.27%
Performance Changes
Tip Curious why this is faster? Comment Comparing 
|
Plan reporting hit `todo!()` for any tree-decomposed plan and for the materialization stage, so `--report-level with-plan` panicked on every program that decomposes -- which is most of them. Render a DecomposedPlan as each bag's stages followed by the block that joins their materialized results, and a materialization cover as the pseudo-atom it reads. A key spec indexes the cover rather than the probed atom, so a column that names no variable there now falls back to its index instead of unwrapping None. With proofs off, a view read's second output is `Unit` and nothing reads it, so match the literal instead of binding a variable no other atom shares. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This reverts commit d8a6086.
…e lever The user-rule search gap is not the encoding's queries: the e-graph is identical, every rule fires the same 12550 times, and with --no-decomp the plans and the time both match native (166 ms vs 158 ms over the shared rules, against 523 ms vs 1225 ms with it). Tree decomposition covers a 1301-row view in the outer loop where native covers a 12-row one. `remove_dup_vars` also has a real bug -- it splits the last argument as the output, so a tuple-output view keeps its e-class in the key and two reads of one row never group. Keying on the inputs fixes it and makes the encoded plan structurally native's, but it costs proofs ~9% and herbie 8.7% at 8 rounds, so it stays reverted until the planner costs these queries stably. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Author
|
CodeRabbit raised this against #45, which is stacked on this branch, so the finding is really about this PR's It was the review's only Major finding. The claim:
Sites it lists:
Line numbers are as of #45's diff, so they may have drifted here. Worth noting the shape of the objection rather than the specific edits it proposes: it is not disputing that clearing helps, it is arguing that an env var should not be able to switch normal proof-mode runs into incorrect extraction or non-termination. Gating it behind something that cannot be flipped in a normal run — a benchmark-only path, or a build feature — would answer it without giving up the measurement. For context on the other side: #45 now merges |
oflatt-claude
pushed a commit
to oflatt-claude/egglog-encoding
that referenced
this pull request
Aug 7, 2026
This branch was cut on top of saulshanabrook#44, so its diff carried that PR's `uf_clear` knob and rebuild-cost measurement. None of it is needed to merge upstream, and reviewing the two together conflates them. Removes the `EGGLOG_UF_CLEAR` switch and its generated ruleset, rule, and schedule step; the `EGGLOG_REBUILD_TRACE` logging in `table/rebuild.rs`; and `rebuild_cost.md` with the paragraph citing it. `proof_encoding.rs`, `proof_encoding.md`, and `rebuild_cost.md` now match `main` exactly. Re-apply on top once saulshanabrook#44 lands.
Collaborator
|
outdated I think |
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.
Draft. Stacked on #39 (
proof-encoding-minimal), which is not yet merged, so the diff below includes #39's commits. This branch's own work is the two commits after5cc4dc1.The question
Can we delete old
@UFrows every iteration, keeping only the ones the next rebuild reads?Sound, but not faster. The knob is therefore off by default; with it off the encoding is unchanged byte for byte.
Why it is sound
The union-find's only readers are the maintenance rules, so once the rebuild loop saturates, every row a query,
delete, orsubsumecan reach is canonical and the edges that got it there are dead. A@uf_clearruleset (one:naivedelete-everything rule per eq-sort, run last in the maintenance schedule) passes 801/801--test fileswith every proof snapshot byte-identical, and the full workspace at 1494+3 = the same 1497 the base branch passes.Why it does not pay
math-microbenchmarkwalleggcc-2mm-pass1walleggcc-2mm-pass1peak RSS6 rounds per endpoint via
bench.py, serial, proofs vs proofs against5cc4dc1.The clear costs +134 ms;
@parentsaves 27 ms;@rebuildingdoes not move outside noise. The rebuild rule is:unsafe-seminaive, so its driving@UFatom is already restricted to the delta — the rows a clear removes are ones the join never visits. Only@parent(which joins@UFagainst itself) sees its full side shrink, and time in@parentis 3.0% of wall onmath-microbenchmarkand 0.2% oneggcc-2mm-pass1. A clear that cost nothing could not win more than that.A whole-table
clear_tablefast path (already present fromDatabase::clear_tablethroughEGraph::clear_function) would remove the +134 ms but not the reason there is nothing to win.Two things it breaks
find_canonicaland proof extraction's fall-back read@UFoutside rebuilding. Surface syntax never needs it; a Rust-API caller holding aValueacross a union does, and native resolves those.saturatetermination.(rule ((Same x y)) ((union x y)) :naive)undersaturateterminates normally and hangs with the clear on: oncexandyare canonically equal the re-firing rule writes the self-edgev -> v, normally an idempotent no-op via:internal-identity-vals 1. After a clear it is a fresh insert, so the loop always reports a change. Suppressing self-edges at the source would fix the class — a@UFrow whose key is its own parent carries no information.What the search time is actually made of
rebuild_cost.mdrecords the rest, since the interesting result is the negative one.Encoded proofs against native, fastest of 3:
@rebuilding+@parentmath-microbenchmarkeggcc-2mm-pass1luminal-llamamath-microbenchmark) is 2.3x native's entire rebuild.diff > table_size/8; tracing that choice gives fullscan on 93.2% ofmath-microbenchmark's rebuilds and 99.8% ofeggcc-2mm-pass1's, with mediandiff/table_sizeof 1.0 and 0.8. The encoding can never scan: its rebuild joins the@UFdelta against a declared occurrence index, and an index atom is probed rather than scanned by construction. So on these workloads it pays twice — maintaining an index native would not consult, then probing it per delta row instead of making one pass. Scanning the index is not the fix either, since(any 0 1 2)holds an entry per row per column; the scan has to be over the view, which makes it a different rule body rather than a different plan.math-microbenchmarkand 55% onherbie, but 21% oneggcc-2mm-pass1and 0.5% onluminal-llama— whose 7.35x is the worst in the set. That gap is in user rules, and it is not join width: comparing the desugared programs suggests bodies grow 13 to 38 atoms, butto_queryflattens nestedCalls into one atom per subterm, so native's nested text compiles to the same atoms the encoding writes longhand. Both come to eleven real atoms on the rule checked. The leading untested explanation is rebuild churn feeding seminaive: the rebuilddeletes and re-sets a row per delta-times-occurrence match rather than per row that moved, and each re-inserted row is a fresh delta for every user rule reading that view.State
--test files801 passed,--lib83 passed,--workspace1497 passed / 0 failed,cargo fmt --checkandclippy --all-targetsclean.🤖 Generated with Claude Code