Factorized aggregate sinks: COUNT/SUM/MIN/MAX/AND without enumerating the join - #130
Open
MesTTo wants to merge 35 commits into
Open
Factorized aggregate sinks: COUNT/SUM/MIN/MAX/AND without enumerating the join#130MesTTo wants to merge 35 commits into
MesTTo wants to merge 35 commits into
Conversation
Contributor
Author
|
Current numbers on this tip (fe662ff, RUSTFLAGS="-C target-cpu=native", nightly, release): The bench runs both routes and asserts the results byte-identical before reporting. The full default suite ( |
zipper_join.rs answers a conjunctive (exec .. (, ..) ..) by seeking the PathMap byte-trie one variable at a time and intersecting factors on each shared variable, instead of materializing the product the ProductZipper builds. The term encoding, unification, and answer emit are expr's own (Tag/byte_item, unify, apply); the module contributes the seek order. Behind a self-contained router it returns exactly the ProductZipper's answers on the conjunctive fragment it covers (ground and free-variable answers, and data-side capture of a query compound), and runs in O(s) on the AGM triangle where the ProductZipper is O(s^2). It declines the one compound shape a per-column union-find is provably unsound on (proofs/ZipperUnifySafe.thy, nonflat_uf_unsound), keeping it on the ProductZipper, and an assignment whose bindings close a cycle yields no row, mirroring Expr::_unify's occurs rejection. Depends only on PathMap and expr, and adds one pub mod line. cargo run --example wco_leapfrog reproduces the differential and the scaling table.
The relation head was baked into the seek prefix, so it was exempt from unification in both directions: a variable query head returned nothing where the ProductZipper unifies it with every stored head, and a wildcard stored head was invisible under a ground query head. The prefix is now the arity byte alone and the head is column 0 like any argument, so both directions flow through the ordinary column machinery (a ground head seeks exact plus wildcards, a variable head enumerates). With the head a column, the per-fact gate scan lost its meaning and its need: the per-column step is full unification with cycle rejection at emit, so no query or fact shape requires a decline. The router now takes every nonempty relation-prefixed conjunction, the once-declined join-propagated capture included, and the routability check is parse-level, reading nothing from the map (it was a full fact scan per query). Verified: the corpus grows head-position and cycle cases (11 shapes, all matching the ProductZipper), the random distribution gains variable heads, wildcard-headed facts, and compound columns (4000 trials, 0 fallback, 0 mismatches; variable-headed patterns keep total arity 3 so they cannot match the harness's own exec and ans atoms, which is full-evaluation semantics rather than the compared query), and an in-module adversarial differential runs the raw join against a nested-loop reference over the same unify on eleven templates around the old boundary (20000 seeds, 0 mismatches). The triangle is unchanged within noise: the O(1) gate pays for the head column.
TotalRouterSafe.thy: a solution of an equation system solves every subsystem (solvable_mono, the per-level pruning), pairwise unifiability does not give a simultaneous solution (threading_necessary, why one bindings store threads the whole descent), and a variable equated with a term properly containing it has no finite solution (occurs_unsolvable, the emit-time cycle rejection). nonflat_uf_unsound stands as the boundary of the retired byte-level union-find, the mechanism whose decline this router no longer needs. Checked with isabelle build -D proofs.
A fully-wildcard fact captures a compound and propagates it through a four-factor cycle: (h $s1 $u1) binds $u1 to (k v3), which (e (k $s0) v2) then absorbs. The total router finds the answer row, byte-identical to the ProductZipper; the shape is the one a route co-tuned to the old decline structurally misses, so the corpus pins it.
The space-to-space transform, the ,/, exec path, now routes its body through query_multi_dispatch: a nonempty relation-prefixed conjunction with a variable occurring as a whole column in two or more factors runs on the worst-case-optimal join, and everything else, with interpreted sources, sinks, and the pattern dumps, keeps the ProductZipper path. The join streams one callback per product tuple: an accepted leaf reconstructs its per-factor stored facts (a re-indexed factor's columns go back to original order and numbering), pairs them with the pattern exactly as query_multi_raw does, and re-derives the bindings with mork_expr::unify, so the template emit downstream is stock and byte-identity is inherited rather than re-proven. MORK_LEAPFROG=0 pins the stock path per thread; =all dispatches every routable body. The policy is measured, not assumed. The triangle runs 240x end to end through metta_calculus at s=4096. The counter machine, whose bodies never intersect, would run 3.4x slower dispatched everywhere (callgrind: 3.3x the instructions) and stays stock at parity; a 10^6-tuple pure product would run 1.8x slower and stays stock. Nil's bfc chainer is at parity too, its hot single-factor sol lookups correctly left stock (forced dispatch costs it 21%), and byte-identical off/on at every proof size with the bench's own assertions passing. Every resource program is byte-identical both ways to 2000 steps, as are 20000 random whole programs with chained exec atoms and machinery collisions, the corpus, and 4000 random single-flip trials, each also run through the wired engine; the transform's match count and changed flag agree case by case.
The shipped policy dispatched any body with a variable column shared by two factors, which routed finite_domain, a functional pipeline whose factors share columns, onto the join for a 3.7x loss (bench: 70ms stock, 261ms dispatched). The gate is now the actual boundary of the worst-case-optimal advantage, three conjuncts, cheapest first: the body must be cyclic over its whole-column variables (a cycle carried only inside compounds gives the seek nothing; the counter machine measured 1.6x slower without this), cyclic over its full variable sets (alpha-acyclic queries are where a relation-at-a-time plan already meets the optimal bound), and not functionally degenerate (a diamond of function tables is FD-acyclic, its AGM bound linear, per Gottlob-Lee-Valiant-Valiant and Abo Khamis-Ngo-Suciu). The first two conjuncts read no data; the third probes each simple factor's trailing functional dependency over the facts, one shared scan per prefix, dead at the first determinant collision, capped at 200k rows, so a genuine graph pattern stops paying within its first facts and dispatches. Measured: finite_domain 70.3ms stock / 79.4ms dispatched (the residual is the one-time confirm scan of the genuinely functional tables); counter machine 12/13ms parity; the s=4096 triangle keeps 2602ms -> 10ms. Resources, bfc, the corpus, 4000 trials, and 20000 random whole programs stay byte-identical; a policy test pins the four routing classes.
The full bench suite measured the boundary inside the cyclic non-functional class. bench transitive's triangle detect over a million uniform random edges ran 15% slower dispatched (the product never blows up there, so the join's per-candidate machinery loses on constants), while bench clique's 6- and 10-factor queries ran 50x faster dispatched, and the hub triangle keeps its 250x. The gate now reads a bounded region of the instance before dispatching: every relation tiny declines, since the ProductZipper's straight-line constants win outright; four or more join factors dispatch, since the product deepens multiplicatively while the join stays output-bounded; a three-factor body dispatches only when a bounded sample of first-argument values finds a heavy hitter, the hub a product blows up through. A hub outside the sample window is missed and the body merely stays on the stock path; the exact version of this decision is the cost-based dispatch these capped cursor walks approximate. Measured after: transitive 1.01 (from 1.15), clique 0.02 (kept), tile_puzzle 1.01, finite_domain 1.00, the s=4096 triangle 2506ms -> 10ms (kept), every other bench at parity. Resources, bfc, the corpus, 4000 trials, and 20000 random whole programs stay byte-identical, and the policy test pins all seven clauses.
…und_join ground_join opened a fresh read-zipper at prefix+bound for every column of every factor at every recursion node, re-walking the byte-trie from the root each time (the dominant cost; the join is compute-bound). Hold one SubtermCursor per factor instead, opened once at the relation prefix and walked column by column with a floor stack (SubtermCursor::descend_floor/ascend_floor): the zipper descends and ascends in place, never re-opened from root. Byte-identical to the prior join (ground_join_matches_brute_force) and, measured on a 3000-node/150k-edge graph (7,369,139 two-hop answers), 2731ms -> 1139ms (2.4x). ground_join_parallel partitions the leading variable's domain across worker threads by hash (hash(value) % nworkers), each running the join on the SHARED READ-ONLY map into its own buffer, concatenated at the end. Safe by construction: concurrent reads of an immutable PathMap, no shared writes; the workers' answer sets partition the whole, so the result equals sequential ground_join (ground_join_parallel_matches_sequential). Same graph: 1139ms -> 121ms at 32 workers (byte-identical). ground_join_for_each streams answers without materializing the domain. See examples/ground_join_parallel.rs.
…a only ground_join does not unify. It is complete only when every joined relation is fully ground; on schematic data it is a strict subset of the ProductZipper and silently drops answers (a stored (sol $n ..) is not matched against a query (sol Z ..); a nonground compound query column stays unconsumed). A caller that may join over schematic facts must detect that and route to a unifying join. Making the contract explicit at the API so callers gate correctly.
The routing block in query_multi_dispatch now compiles only under a new default-off leapfrog feature, so the default build takes the stock ProductZipper path unconditionally; with the feature on, the MORK_LEAPFROG runtime toggle keeps working within it, and the wco_leapfrog example requires the feature. This is the review shape requested on the PR: the join under an experimental flag, main.rs untouched. The gate contract is modeled in Alloy (fac26 in MesTTo/alloy-mork): routing requires feature AND toggle AND flat shape, every other state is the stock engine, and answers are gate-independent.
The query hypergraph (factors as hyperedges over the body's variables), GYO
alpha-acyclicity with a join tree, and a minimum-width partition search. An
acyclic body is width 1 (each factor its own bag along the GYO tree); a cyclic
body searches partitions into blocks of size <= k for the smallest whose
bag-query is acyclic, so Yannakakis applies over the bags. The 4-cycle is the
target: rho* = 2 (one global WCO join is O(N^2)) but a width-2 decomposition
evaluates in O(N^{3/2}).
Soundness is the cover condition, machine-checked in Alloy (fac14_ghd, Model
14): every factor sits in some bag, so the join of the bags equals the join of
all factors. Unit-tested on the hypergraph in isolation: a path is acyclic
(width 1), the triangle and 4-cycle are cyclic (width 2, every factor covered,
bag-query acyclic). Evaluation over the bags follows in a later commit.
…them
materialize_bag runs the WCO join over a bag's factors and records each match's
facts plus its variable values (read from top-level columns). join_bags natural-
joins the materialized bags on shared variables into one full tuple of matched
facts per original factor. query_multi_ghd is the drop-in: for a cyclic body
(width >= 2) whose columns are all top-level variables it decomposes, materializes,
joins, and streams the SAME unify+effect per full tuple as the global WCO join;
acyclic or nonground-compound bodies fall back to it.
Differential oracle ghd_full_tuples_match_global_join_on_cycles: for the triangle
and the 4-cycle over a real space, the GHD's full tuples equal the global WCO
join's as a set -- Model 14 in the running engine. join_bags is unit-tested in
isolation; all 22 zipper_join tests still pass.
join_bags is a correct nested loop here; Yannakakis semijoin reduction over the
join tree (the O(N^fhtw) bound, e.g. 4-cycle O(N^{3/2}) vs the global O(N^2))
replaces it next.
Sum-product variable elimination over the factor relations: materialize each factor as a count table over its variables, then for each variable multiply the tables that mention it and sum it out, leaving a scalar whose product is the count. O(sum of intermediate sizes) = O(N^fhtw); enumerate-and-count is O(output). This is the asymptotic win the WCO join cannot match. WCO is output-optimal for ENUMERATION (that is the clique 1000x), but a COUNT does not need the tuples, only the aggregate, which factorizes into a sum-of-products. Alloy: fac16 shows projection pushdown is sound only for a variable local to one relation (so a join variable cannot be pushed out -- why enumeration cannot be beaten); fac17 shows the factorized count equals enumerate-and-count and touches fewer rows. Differential oracle ghd_count_matches_enumerate_count: factorized == enumerate on the 2-path and a single relation. Scaling demo ghd_count_win_scales on a hub 2-path (k inputs, k^2 output): enumerate O(k^2), factorized O(k), speedup 10x to 167x for k = 50 to 800 -- growing without bound, a dropped exponent. All 8 ghd/count tests pass; the 22 zipper_join tests are unaffected.
One sum-product engine, ghd_aggregate<S: Semiring>, now serves COUNT (the natural numbers), EXISTS (the booleans), and weighted SUM (a per-fact weight), by parameterizing the factor tables, multiply, and sum-out over the semiring's zero/one/add/mul. ghd_count is a thin wrapper (u64, weight one). This is the FAQ generalization: weighted joins, existence, and shortest-path (tropical) share the same factorization. Test ghd_aggregate_over_semirings: COUNT, EXISTS, and a weight-2 SUM (= 2^m * count) over a 2-path agree; the existing count oracle and scaling demo still pass. 9 ghd/aggregate tests green.
ghd_aggregate_auto decomposes the body, derives a post-order (leaf-first) elimination order via elimination_order, and aggregates, so the caller need not choose one. Each variable is eliminated at the bag that does not share it with its parent, confining it to that bag's subtree; the induced width is the hypertree width, so an acyclic body aggregates in O(N^fhtw) = O(N). Test ghd_aggregate_auto_derives_order_on_a_chain: a 3-chain r-s-t decomposes to a width-1 GHD, the derived order aggregates, and the factorized count equals enumerate. 10 ghd tests green.
The flybase P1 query (main.rs bench_flybase) is a star join whose COUNT the CountSink computes today by enumerating the O(k^2) product into a PathMap. Since $y and $z are independent given $x, ghd_aggregate_auto counts it in O(k) via the auto-derived elimination order, Sum_x deg_y(x) * deg_z(x). ghd_count_flybase_star_shape: the factorized count equals the enumerated count and the speedup grows 11.6x -> 216.9x from k=50 to 800 -- a dropped exponent on the realistic query shape. The existing CountSink is a grouped distinct-count over a materialized PathMap; routing a projection-free multi-factor-join COUNT through the factorized path is the next wiring step.
Durable pick-up doc: how to accelerate the existing enumerate-based CountSink/ SumSink with ghd_aggregate_auto (O(N^fhtw) not O(output)), byte-identical. Records the branch/commits/email, the reusable ghd.rs + zipper_join.rs entry points, the sink/transform_multi_multi_o wiring target, the soundness condition (distinct proj == match count), five build slices each with a differential oracle, and the never-wrong fallbacks.
gyo_join_tree is connected-only: an isolated edge is a component root, not an ear, so it rejected a disconnected hypergraph (alive count > 1) and ghd_aggregate_auto returned None for a Cartesian body like the sink_count_literal shape (foo $x)(bar $y)(baz $z). But a disconnected conjunctive query is a Cartesian product, and its aggregate is the semiring product of the per-component aggregates (Yan-Larson double-eager, VLDB'95): COUNT = |foo|*|bar|*|baz| in O(sum) not O(product). Split the body into connected components, decompose each on its own (the connected case gyo/decompose are tested on), concatenate the elimination orders, and let ghd_aggregate's final scalar-mul combine them. ghd_aggregate already multiplied disjoint leftover tables, so the engine needed no change -- only the planner wrapper. ghd_count_cartesian_product_factorizes checks 3*2*3=18 == enumerate; the 6 existing ghd tests are unchanged.
…default) MORK's CountSink counts distinct outputs by materializing them into a PathMap and reading val_count -- O(output). For an ungrouped, projection-free count over a decomposable multi-factor body the answer is the join's match count, which the factorized aggregate computes in O(N^fhtw) without enumerating (FAQ InsideOut over the join tree; Yan-Larson double-eager COUNT). transform_multi_multi_o gains a gate (factorized_count_gate): single count sink, the template mentions no pattern variable (a single group) and the projection mentions every pattern variable (distinct-output == match count, Alloy fac18), body decomposes with >=2 factors. When it fires, the query stops after one representative match -- enough to seed the single group and its template context -- and CountSink::set_precomputed supplies the factorized count, so finalize emits byte-identically to the enumerate path. The gate is a pure VarRef-set check (pattern variables are VarRef(i<P) in the sink) so grouped and projected counts, where match-count != distinct-output, always fall back. Gated behind MORK_FACTORIZED_COUNT (env) or a per-thread override for tests, default OFF; the default exec path is untouched. Three differential oracles run the same count exec both ways and assert a byte-identical whole-space dump: sound routes (Cartesian + connected star, count values checked), and grouped/projected decline and stay identical by falling back. Full lib suite 35/0.
factorized_count_sink_win_scales drives the same count exec at growing scale both ways. The star has k*k output but O(k) inputs, so the routed factorized count grows its lead 16.3x -> 399.9x from k=50 to 800 -- a dropped exponent, and byte-identical at every k. The growing (not flat ~1x) speedup is the proof the fast path is actually taken through the exec and not silently falling back to enumerate.
Mark slices 1-3 landed with the measured result (wired 16.3x->399.9x, byte-identical), and cite the prior art the routing combines: FAQ InsideOut, Yan-Larson eager aggregation, GYO forest handling, the commutative-semiring contract.
SumSink dedups then sums the distinct values of a numeric projection column (the FAQ SumSum case), so it needs a Yannakakis semi-join reduction to the surviving domain plus a sum, not ghd_aggregate with a per-fact weight (which sums with multiplicity). Document the correct mechanism so the next session does not ship the naive version.
… by default)
MORK's SumSink is SUM(DISTINCT numeric column): it dedups then sums the distinct
values of one projected column -- the FAQ SumSum case, which does NOT factorize as
a COUNT sum-product with a per-fact weight. The sound factorization is Yannakakis:
the distinct summed values are exactly the column's semi-join-reduced surviving
domain (the values in >= 1 full join answer), which is FAQ's free-variable form --
eliminate every OTHER variable over the EXISTS (boolean) semiring, keeping the
column free. ghd_surviving_domain computes it; ghd_sum_distinct parses and sums.
The elimination order must be rooted at the free variable: GYO can build the join
tree as a chain, and eliminating a shared join variable before a leaf materializes a
quadratic {g,x,y} intermediate. elimination_order_free re-roots the order at the
summed column's bag so leaves eliminate first -- O(N^fhtw). Measured: ghd_sum_distinct
went from O(k^2) (324918us at k=800) to O(k) (971us), and end to end through the exec
the SUM sink grows 13.3x -> 340.5x (k=50..800), byte-identical each k.
The transform_multi_multi_o gate generalizes to a FactorizedAgg enum: COUNT needs a
full projection (fac18), SUM a single-column projection; both need no grouping. Both
sinks get set_precomputed and the same one-representative seeding. SumSink::finalize
uses precomputed in both the literal-assert and $c-var emit guards. Two differential
oracles (value + literal guards; dangling tuple correctly excluded) and a scaling
proof. eliminate_var and collect_bag_elims factor the shared elimination code (jscpd
0). Full lib suite 37/0, default OFF (MORK_FACTORIZED_COUNT).
Record the semi-join routing, the elimination_order_free O(N^2)->O(N) fix, the 340.5x measured win, and fac19. Slice 5 (fusion) remains.
600 random programs over random data and six join shapes -- chain, star, cyclic triangle, 4-cycle, self-join, and 3-chain, with COUNT and SUM sinks -- plus grouped and partial-projection sinks the gate must decline. Each runs both ways (factorized on/off) and the whole space must be byte-identical. Random data exercises empty joins, single matches, dangling tuples, and high fan-out. Deterministic LCG per seed. All 600 pass, so the gate is sound and the factorization exact across the surface.
FloatReductionSink<Min>/<Max> reduce the distinct values of one column, exactly like SumSink. MIN/MAX(DISTINCT x) == MIN/MAX over x's semi-join-reduced surviving domain (idempotent, so distinct vs multiplicity is irrelevant; exact, so the f64 to_string is byte-identical). ghd_float_reduce_distinct reduces the domain with the sink's own Reduction::ACC/op; the gate routes FMinSink/FMaxSink on a single-column projection with no grouping; both FloatReductionSink emit guards take set_precomputed. Deliberately NOT float SUM/PROD: their reduction is order-sensitive (float rounding is non-associative), so summing the domain in a different order than the enumerate sink could differ in the last bit -- not byte-identical. MIN/MAX are safe. The differential checks MIN/MAX exclude dangling values (MIN=10 not 5, MAX=30 not 40); the fuzz adds fmin/fmax over 600 random programs. Full lib suite 39/0, jscpd 0.
…N/MAX) factorized_aggregate_enabled / set_factorized_aggregate_override / MORK_FACTORIZED_AGGREGATE. The knob is default-off and unshipped, so no compat shim needed. Pure rename, tests unchanged.
The aggregate family is COUNT/SUM/MIN/MAX; float SUM/PROD excluded (order-sensitive). 600-program fuzz, fac16-fac21 Alloy, gate renamed. Slice 5 fusion removes an observable relation from the space and can't prove res0 dead in the open model, so it is sound only as a user-directed rewrite, not an automatic pass.
A flybase-shaped star (one gene, k numeric rel1 partners, k rel2 partners) with no external data: the join has k*k matches but O(k) inputs. Runs COUNT (full projection) and SUM(DISTINCT x) each both ways, asserts byte-identical, reports the speedup. At k=800: COUNT 440.5x, SUM 398.4x through metta_calculus. Wired into 'all'. The default suite uses no aggregate sinks, so this is the benchmark that exercises the routing.
The gate is Alloy-sound (fac16-fac21) and byte-identical across the differential corpus (600-program fuzz over every join shape and all four aggregates, plus mork bench aggregate), and it only engages on cases it proves equal to the enumerate sink. MORK_FACTORIZED_AGGREGATE=0 is the kill switch; a thread-local override still wins for tests. Full lib suite 39/0 default-on. The default bench suite uses no aggregate sinks, so it is unchanged (counter_machine 1.28s, process_calculus 32s, tile 7.6s -- all within noise of the default-off baseline); the aggregate bench routes at 451.6x COUNT / 413.6x SUM.
AndSink bitwise-ANDs the first byte of the distinct column values; AND is associative, commutative, and idempotent, so it reduces the semi-join surviving domain order- and multiplicity-independently -- byte-identical. ghd_and_distinct + FactorizedAgg::And + AndSink::set_precomputed in both guards. connected_free_domain factors the shared connected/decompose/free-order/domain front half of the SUM/MIN/MAX/AND reducers (jscpd 0). Also fixed a stray debug println! in AndSink::finalize (-> trace!). The routable aggregate family is now COUNT, SUM, MIN, MAX, AND. Float SUM/PROD stay declined (order-sensitive rounding). AndSink differential (dangling value excluded) + fuzz coverage; full lib suite 40/0.
The Alloy models live in their own repo (github.com/MesTTo/alloy-mork); the wiring plan and GHD build notes were session-internal scratch. The design and soundness argument belong in the PR description, not committed dev notes.
The routing gate returns None unless the new default-off factorized_aggregate feature is on, so the default build runs the stock enumerate path unconditionally; within the feature the MORK_FACTORIZED_AGGREGATE runtime kill switch keeps working. The aggregate bench arm, its place in 'bench all', and the routing-dependent differential and win-scales tests move under the same feature (the ghd engine tests stay always-on). Same review shape as the leapfrog dispatch on the PR this stacks on: experimental flag, stock default. With the feature: 40/40 lib tests incl. the 600-program fuzz; bench aggregate COUNT 473.4x / SUM 389.1x, results asserted byte-identical both routes.
PathMap already exposes this as BitMask::test_bit (src/utils/mod.rs:609), implemented for ByteMask. The local copy duplicated it byte-for-byte and indexed the mask words directly instead of going through the bounds-checked accessor. least_ge keeps its next_bit call: ByteMask::next_bit is strictly greater-than, so testing k first is a real gap it fills.
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
1 participant
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.
Factorized aggregate sinks — COUNT / SUM / MIN / MAX / AND computed by variable elimination over a hypertree decomposition instead of enumerating the join: O(N^fhtw) rather than O(output), an exponent drop. COUNT runs FAQ InsideOut over the full projection; SUM/MIN/MAX/AND run over the Yannakakis semi-join-reduced single-column domain. The routing gate declines everything outside the proven fragment (grouping, partial projection for COUNT, nonground compounds, disconnected or single-factor bodies), and every routed shape is asserted byte-identical to the enumerate path.
Review shape: the routing is behind an experimental
factorized_aggregatefeature flag (default off), same as the leapfrog dispatch in #124 this stacks on. The default build runs the stock enumerate path unconditionally; within the feature theMORK_FACTORIZED_AGGREGATEruntime kill switch keeps working.cargo test -p mork --features factorized_aggregateruns the differential suite including a 600-program fuzz across six body shapes;mork bench aggregate(feature build) reports COUNT 473.4x / SUM 389.1x at k=800 with results asserted byte-identical both routes.mork bench allandmork teston the default build are unchanged.The gate soundness is modeled in Alloy (github.com/MesTTo/alloy-mork): fac17–fac21 pin the aggregation fragment (full projection for COUNT, the semi-join domain for SUM, grouping declined, SUM≠weight-swap), and fac26 pins the feature-gate contract itself.