[FBumann]

Prompt: fix cases 2 and 3 in the PR

Prompt: I think you should do it as a stacked PR! With a clear title that its only bug fixes

Note

The following content was generated by AI.

Bug fixes only, stacked on #894. Two load checks that #894 adds refuse valid files. missing: 0 on a divisor now loads where a guard leaves the missing row out. A variable's missing: number may now lie outside its bounds.

A later ask to fuzz the check found one bug in this PR's own guard: a variable with a missing: number spared a divisor. 0aa8a62 fixes it.

Case 2: a guarded divisor

#894 refused a divisor by looking at the divisor alone. Each file below was refused, although no row divides where c is missing:

parameters: { c: { dims: [g], missing: 0 }, d: { dims: [g] } }
constraints:
  coef: { dims: [g], expression: x - c * y <= 0 }            # 0 is the intended reading here
  div:  { dims: [g], where: "c > 0", expression: y <= d / c }

• the same divisor in a cases: region with when: c > 0;
• sum(y / c, over=g) where y has where: c > 0;
• the capacity factor p / p_nom in a reported expression.

missing: absent is not a fix for these. It deletes the coef row where c is missing, so x is unbounded there: specsolve solved x[b] = 100 instead of 0.

The check now runs after lowering, in _divisors.py. A guard spares a divisor when the guard is false at every missing row: c > 0, c != 0, the bare name c, or a named condition that holds one of these. The guard counts when it is a conjunct of one of three:

• the constraint's where;
• the when of the case that holds the quotient;
• the where of a missing: absent variable that multiplies the quotient. A variable with a missing: number reads that number outside its mask, so its mask guards nothing.

A sum, a window, a shift or an at reads other coordinates. So a guard from outside one of them is dropped inside it, and a guard under an OR or a NOT spares nothing. A named expression is still checked on its own frame, so its guard goes in its own cases:. A quotient inside a condition keeps the unguarded check.

The refusal now also suggests the guard: …or guard the quotient with a where such as "c > 0". A refusal inside a case now names the entry, without the case.

Case 3: a variable number outside its bounds

modules: { dims: [site], domain: integer, where: candidate, missing: 0, bounds: { lower: 1, upper: 4 } }

#894 refused this with missing: 0 is below bounds.lower 1.0. The bounds hold only inside the mask, so a unit of one to four modules where it is a candidate has 0 modules elsewhere. A parameter bound already loaded the same file. The domain check stays: a binary variable still takes 0 or 1.

Verification

Reproduced first. Each new loading case was a strict xfail on da86544 (the head of #894) and failed with the refusal it reports. So was [a-mask-of-a-variable-that-reads-a-number-outside-it] on 41bed1d. Each marker came off with its fix, and its XPASS is the mutation row for that guard.

Gates on 0aa8a62:

• pixi run lint passes.
• pixi run test passes: 3097 passed, 1 skipped.
• pixi run docs-build passed on 07cdf5a. 0aa8a62 changes one bullet in absence.md, and prettier and the lint pass on it.
• compile-tex was not run, because the container cannot download the TeX bundle. CI runs it.

Mutation table on 07cdf5a. A script deleted each guard in turn and ran the full suite. It restored the file with git checkout -- and dropped __pycache__ before and after each run. The tree came back clean.

Guard deleted	Caught by
a masked factor spares the divisor	[a-masked-numerator], [a-masked-factor]
a case's when spares a quotient in its region	[a-case]
a sum, window, shift or lookup drops guards from outside it	[a-guard-outside-a-shift]
the same, inside a divisor	[a-guard-at-another-coordinate]
a case's when spares a divisor that is a case	[a-case-in-the-divisor]
a bare name spares	[has-a-row]
a comparison spares only where 0 fails it	[a-guard-that-admits-zero]
a comparison spares at all	8 cases of test_a_divisor_guarded_against_a_missing_row_loads
a named condition spares	[a-named-condition]
only the AND spine spares	[a-guard-under-an-or], [a-negated-guard]
the check runs on a quotient in a condition	[a-quotient-in-a-where]
the check runs on every declaration	20 cases of the two refusal tests
only a missing: absent variable spares (0aa8a62)	[a-mask-of-a-variable-that-reads-a-number-outside-it]

Coverage moved. The below-lower and above-upper refusal cases are gone. test_a_variable_number_outside_its_bounds_loads now asserts that the same shapes load.

Fuzzing

A differential fuzzer drew 12,000 random specs, together with a Python model of what each one means. A spec holds one dimension, missing: values, guards, cases, shifts, sums and masked variables. The model ran each spec on random data with missing rows.

• Soundness: the spec loads, and the data divides by a zero that the missing rows alone cause, in a row that is built.
• Precision: the spec is refused, and no draw divides by zero.

On 41bed1d, 225 seeds were soundness failures of one kind: a masked variable with missing: 1 spared a divisor. 0aa8a62 fixes that, and on it none of that kind remain.

The other soundness failures exist on #894's head too, so this PR leaves them:

• a missing: value other than 0 that cancels, such as missing: 1 with x / (1 - c) (about 250 seeds);
• constants that cancel around a missing: 0 parameter, such as x / ((c + 1) - 1);
• a literal zero in a case, such as when: d > 0, expression: 1 - 1.

The 70 precision seeds are mostly rows that are never built, because their masks contradict each other. Two kinds are real and conservative: a guard written NOT (c != 1), and a masked variable in another term of the same row.

#893's fuzzer ran 6,000 mutants of the examples on 0aa8a62, with neutral removed from its choices. It found only the known #890 canonical-form order.

Not done

• The PyPSA *_nom_mod parameters stay missing: absent. Their divisors are guarded by *_p_nom_mod > 0, so missing: 0 would load now. Whether to change them back is a call for docs(pypsa): a PyPSA schedule, weight or limit that the data leaves out is absent rather than zero, and a committable extendable unit is assumed to have its big-M #912's scope.
• The guard that neutral gave is not restored: a missing row on a right-hand side or in a bound reads as 0 without an error. That is a decision for feat(language)!: a missing row reads as the value the file names, and missing: neutral is gone #894, not a bug fix.
• The fuzzer is not committed, and the three kinds of failure from feat(language)!: a missing row reads as the value the file names, and missing: neutral is gone #894 are not fixed here.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YZ68heVBrHxKUKsXxqJrXX

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35322085 | 📁 Comparing 0aa8a62 against latest (6088835)

  🔍 Preview build  

32 files changed · ± 32 modified

± Modified

• reference/changelog/index.html
• reference/glossary/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/program/index.html
• reference/reading/index.html
• examples/pypsa/carrier/index.html
• examples/pypsa/cost/index.html
• examples/pypsa/generator/index.html
• examples/pypsa/generator_commitment/index.html
• and 22 more...