fix(relational): absence propagates into a reduction, and laws to hold it there - #314
Merged
Conversation
…d it there Closes #311. `sum(x + y, over=f)` with `y` masked to `f=a` built different models on the two lanes: 400 eager, 240 native — a 40% gap, no error. Addition is fragment concatenation in the relational compiler, so `x + y` is two independent streams and each was reduced over its own coordinates. At row level that is right, since the executor intersects the presences when it assembles the row; a reduction consumes the expression before any row exists, so nothing intersected them. The eager lane was right and I first argued it was not. SPEC §6's carve-out — "a reduction skips what is absent" — has `sum(x, over=d)` over a bare variable as its example, and says a reduction must not propagate absence *outward*. It does not license distributing a compound summand, and distributing is what the relational lane was doing: rewriting `sum(x + y)` into `sum(x) + sum(y)` reads the absent `y[b]` as a zero, which is the reading v1 exists to remove and that #239 and #291 removed from masks and shifts. So reductions are not linear over operands of differing presence. That is the honest consequence of absence being a state rather than a value, and the two spellings are different questions: the total of the net where the net is defined, against the total in minus the total out. SPEC now puts them in a table side by side, because the composition of the two rules was nowhere written down — which is how I came to misread it. `tests/test_arithmetic_laws.py` is the other half. An arithmetic convention is a set of equalities between spellings and nothing else in the suite was checking those: a model can build, solve and agree across both lanes while `a + b` and `b + a` mean different things. Eight laws (commutativity, associativity, subtraction as negated addition, distribution over a variable-free factor and over a divisor, reduction linearity while every operand is total, roll invertibility, and commutativity *under* absence) plus three deliberate non-laws, each asserted through `differential` so a law holding is six numbers agreeing rather than two. The non-laws are the point. This defect is invisible to law-shaped tests — both spellings were individually consistent — and only a test saying "these two are supposed to disagree, and by exactly this much" would have caught it. Writing them also caught one of my own: a "law" that summing over a dim the operand lacks scales by that dim's cardinality. The language refuses that outright at load time. The scaling in `_sum_fragment` applies to a fragment lacking a dim the expression carries, which is not user-visible.
|
Warning Review limit reached
Next review available in: 4 minutes Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (3)
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 |
FBumann
added a commit
that referenced
this pull request
Jul 29, 2026
…_sum Follow-up to #314, which routed `group_sum` through the same absence propagation as `sum` on the argument that a group *is* a sum — and shipped it with no test. Its behaviour was a claim rather than a result; it is now a result: the two spellings separate 640 against 480, and both lanes agree about where each lands. The cases in #314 all reduced over `f` with one mask on `f`, which is the smallest arrangement that shows the rule and small enough to pass for the wrong reason. Five more, each varying one thing: - **group_sum** rather than sum — the untested path above - **two masks that do not nest**, so the summand needs the intersection rather than any one of them. The implementation collects one restriction per fragment and applies every one to every fragment; a version that stopped at the first, or composed them pairwise down the addition tree, passes every single-mask case - **a broadcast coefficient**, which must not move presence at all — a sparse parameter is encoding, not absence (SPEC §6), so the separation has to come from the masked variable alone - **a mask on a dim the reduction does not touch** — mask on `t`, reduce over `f`. The restriction is keyed by the dims the presence names, so this works; keying it by the reduced dim would silently do nothing here - **absence created by `shift`** rather than by a mask, because two sources of "not here" that behaved differently inside a reduction would mean SPEC §6 describes only one of them All five agree across both lanes and the LP re-solve, so this adds coverage rather than fixing anything — which is the outcome worth recording, since the group_sum path had no evidence either way. One fixture note: `g` and the coordinate reaching it exist only for the grouped cases. A dimension no declaration uses has no coordinate set to check against and the executor refuses it, correctly.
FBumann
added a commit
that referenced
this pull request
Jul 29, 2026
…_sum (#316) * test(laws): the absence rules under wider shapes, starting with group_sum Follow-up to #314, which routed `group_sum` through the same absence propagation as `sum` on the argument that a group *is* a sum — and shipped it with no test. Its behaviour was a claim rather than a result; it is now a result: the two spellings separate 640 against 480, and both lanes agree about where each lands. The cases in #314 all reduced over `f` with one mask on `f`, which is the smallest arrangement that shows the rule and small enough to pass for the wrong reason. Five more, each varying one thing: - **group_sum** rather than sum — the untested path above - **two masks that do not nest**, so the summand needs the intersection rather than any one of them. The implementation collects one restriction per fragment and applies every one to every fragment; a version that stopped at the first, or composed them pairwise down the addition tree, passes every single-mask case - **a broadcast coefficient**, which must not move presence at all — a sparse parameter is encoding, not absence (SPEC §6), so the separation has to come from the masked variable alone - **a mask on a dim the reduction does not touch** — mask on `t`, reduce over `f`. The restriction is keyed by the dims the presence names, so this works; keying it by the reduced dim would silently do nothing here - **absence created by `shift`** rather than by a mask, because two sources of "not here" that behaved differently inside a reduction would mean SPEC §6 describes only one of them All five agree across both lanes and the LP re-solve, so this adds coverage rather than fixing anything — which is the outcome worth recording, since the group_sum path had no evidence either way. One fixture note: `g` and the coordinate reaching it exist only for the grouped cases. A dimension no declaration uses has no coordinate set to check against and the executor refuses it, correctly. * test(laws): make the shift-in-a-reduction case actually discriminate As written it could not fail. `sum(x + shift(x, t=1), over=f) <= 120` bounds x[.,0] through the t=1 row whether or not absence propagates at t=0, so the t=1 row dominates and the objective reads 120 either way. Measured rather than argued: neutering `_propagate_absence` fails six of the sixteen cases in this file, and this was not one of them — a test guarding a rule it cannot observe. The shifted operand is now a separate variable from the one the objective maximises, so t=0 is the only place the rule can show. Propagated, the summand is absent there and x[.,0] is free to its bounds; without it the row survives as `sum(x, over=f) <= 120` and caps them, giving 240 against 320. Under the same neutering it now fails, and fails on the differential assertion — the two lanes disagree — rather than on the numeric one, which is the stronger signal. Seven of sixteen now catch the regression.
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.
Closes #311.
The defect
sum(x + y, over=f)withymasked tof=a:sum(x + y, over=f) <= 120sum(x, over=f) + sum(y, over=f) <= 120A 40% gap on the first row, no error. Addition is fragment concatenation in the relational compiler, so
x + yis two independent streams and each was reduced over its own coordinates. That is correct at row level — the executor intersects the presences when it assembles the row — but a reduction consumes the expression before any row exists, so nothing intersected them there.Fixed by restricting every fragment to where the whole summand exists before the reduction runs (
_propagate_absence).I argued the wrong side of this first, and the correction is the interesting part
#311 originally recommended making the eager lane distribute, on the grounds that SPEC §6 legislated it. Re-reading §6, it does not:
Its example is a bare variable, and the rule it states is that a reduction must not propagate absence outward — so one masked component cannot delete a whole accounting row. It says nothing about a compound summand whose absence arises before the reduction sees it. Both lanes already agreed on the case §6 actually covers.
And distributing is zero-fill wearing a disguise: rewriting
sum(x + y)intosum(x) + sum(y)means the absenty[b]contributed nothing — a zero. That is the reading v1 exists to remove, that #239 removed from masks and #291 from shifts, and proposing it for reductions would have reintroduced it in the one place nobody had looked.So reductions are not linear over operands of differing presence, and that is the honest consequence of absence being a state rather than a value:
+is addition on a partial domain.SPEC
The composition of the two rules was nowhere written down, which is how I misread it. It is now a table, because the two spellings are genuinely different questions:
yabsent atf=bsum(x + y, over=f)x[a] + y[a]—x[b]goes with the absenty[b]sum(x, over=f) + sum(y, over=f)x[a] + x[b] + y[a]The total of the net where the net is defined, against the total in minus the total out.
tests/test_arithmetic_laws.pyAn arithmetic convention is a set of equalities between spellings, and nothing in the suite was checking those — a model can build, solve and agree across both lanes while
a + bandb + amean different things. linopy ships formal law tests for the same reason.Eight laws: commutativity, associativity, subtraction as negated addition, distribution over a variable-free factor and over a divisor, reduction linearity while every operand is total,
rollinvertibility, and commutativity under absence — that last one included so the non-laws below read as specific rather than "anything with a mask behaves oddly".Three non-laws, asserted to differ with the values written down. These are the ones worth having: this defect is invisible to law-shaped tests, because both spellings were individually self-consistent. Only a test that says these two are supposed to disagree, and by exactly this much catches it.
Every case runs through
differential, so a law holding is six numbers agreeing (eager, relational, LP re-solve × two spellings) rather than two.Writing them caught one of my own errors too: I asserted a "law" that summing over a dim the operand lacks scales by that dim's cardinality. The language refuses that at load time; the scaling in
_sum_fragmentapplies to a fragment lacking a dim the expression carries, which is not user-visible. Test dropped rather than shipped as a false claim.Found on the way, not fixed here
foreach: [](a scalar constraint) builds on the eager lane and is aLanguageErroron the native one. Loud rather than silent, same class as #313 — worth its own issue.Gates: 648 passed, 4 skipped, 1 xfailed · ruff clean · pyrefly 0 errors ·
mkdocs build --strictclean.