From 07cdf5ae4252c3aee09e31792481ecf51acd6d0a Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 09:54:01 +0000 Subject: [PATCH 1/3] fix(language): a divisor that a where, a case or a masked variable guards loads under missing: 0, and so does a variable number outside its bounds The divisor refusal looked at the divisor alone, so `where: c > 0` over `y <= d / c` was refused although no row divides where `c` is missing. A pass after lowering now reads the guards in force: the conjuncts of the constraint's where, of a case's when, and of the mask of a variable that multiplies the quotient. A sum, a window, a shift or a lookup drops the guards from outside it. A quotient in a condition keeps the unguarded check. A variable's missing: number no longer has to lie inside its literal bounds, which hold only inside the mask. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01YZ68heVBrHxKUKsXxqJrXX --- docs/reference/language/absence.md | 58 +++++++-- src/mathspec/_condition_resolver.py | 2 + src/mathspec/_divisors.py | 170 +++++++++++++++++++++++++++ src/mathspec/_expression_resolver.py | 49 -------- src/mathspec/_lowering.py | 30 +++++ src/mathspec/spec.py | 8 +- tests/test_validation.py | 155 +++++++++++++++++++++++- 7 files changed, 400 insertions(+), 72 deletions(-) create mode 100644 src/mathspec/_divisors.py diff --git a/docs/reference/language/absence.md b/docs/reference/language/absence.md index b4da77d8..9a78a5e6 100644 --- a/docs/reference/language/absence.md +++ b/docs/reference/language/absence.md @@ -54,16 +54,16 @@ for a cost that is zero, `missing: 1` for an efficiency that is one, and row of an `absent` parameter, or of a parameter with a value, does at each position: -| Position | `absent` | a value | -| ----------------------------------------------------------- | ------------------------------------- | --------------------------------------- | -| a coefficient, or a constant on either side of a comparison | removes the row | reads the value | -| a factor of a summand in a `sum` | removes the summand, not the row | reads the value | -| a divisor | removes the row | reads the value. `0` is refused at load | -| a `bounds:` entry | leaves that side of the variable open | reads the value | -| the amount of an `offset=` or a `window=` | makes the operator absent there | reads the value | -| a comparison in a `where` | is false | compares the value | -| a bare `bool` name in a `where` | is false | reads the value | -| a bare number or label in a `where` | is false | is false | +| Position | `absent` | a value | +| ----------------------------------------------------------- | ------------------------------------- | -------------------------------------------------------------------------- | +| a coefficient, or a constant on either side of a comparison | removes the row | reads the value | +| a factor of a summand in a `sum` | removes the summand, not the row | reads the value | +| a divisor | removes the row | reads the value. `0` is refused at load, unless a guard leaves the row out | +| a `bounds:` entry | leaves that side of the variable open | reads the value | +| the amount of an `offset=` or a `window=` | makes the operator absent there | reads the value | +| a comparison in a `where` | is false | compares the value | +| a bare `bool` name in a `where` | is false | reads the value | +| a bare number or label in a `where` | is false | is false | A value of `0` as an amount reads `shift(x, along=t, offset=0)` as `x` itself, and sums nothing under `sum_back(x, along=t, window=0)`. A curve needs a row at @@ -73,6 +73,35 @@ of a table that a curve reads means. For a bound only where the data has one, mask the variable, or declare the parameter `missing: absent` or `missing: .inf`. +### A guarded divisor + +A divisor that a missing row of a `missing: 0` parameter can make `0` is +refused at load, unless a guard leaves every missing row out where the quotient +is read. A guard is a condition that is false at a missing row, such as `c > 0`, +`c != 0` or the bare name `c`. It guards the quotient when it is one of the +conditions joined by `AND` in one of these places: + +- the `where:` of the constraint, +- the `when:` of the case that holds the quotient, +- the `where:` of a variable that multiplies the quotient, because the product + is absent where that variable is absent. + +```yaml +parameters: + c: { dims: [g], missing: 0 } + d: { dims: [g] } +constraints: + per_unit: + dims: [g] + where: "c > 0" + expression: y <= d / c +``` + +A guard holds only at the coordinate where it is read. A `sum`, a window, a +`shift` or an `at` reads other coordinates, so a guard outside one of them does +not guard a divisor inside it. A named expression is read over its own +dimensions, so a guard for its divisor goes in its own `cases:`. + ## How absence travels An absent term in arithmetic removes the whole row. An absent term inside a @@ -174,8 +203,10 @@ a storage with inflow and no store, there is no row. A variable takes `missing: absent` or a finite number, because a variable has no data to refuse. A number needs a `where:`. It must lie in the `domain:` of -the variable, so a `binary` variable takes `0` or `1`, and inside its literal -`bounds:`. `to_spec` refuses the file otherwise. Inside a summing operator, +the variable, so a `binary` variable takes `0` or `1`, and `to_spec` refuses +the file otherwise. The `bounds:` hold only inside the mask, so the number may +lie outside them: a unit with `lower: 1` where it is built can have +`missing: 0` where it is not. Inside a summing operator, `missing: 0` changes nothing, and another number adds itself once for each coordinate that the mask leaves out. The typeset legend prints the number where the mask leaves it out beside the variable. @@ -194,5 +225,6 @@ divisor is absent, and where its divisor is exactly zero, whether a solve or the data gave that zero. A solved value is read as the engine reads it back, so an engine may read a value within its solver's tolerance of zero as zero. A missing row of an `absent` divisor parameter makes the quotient absent, and -`to_spec` refuses a divisor that a `missing: 0` parameter can make zero. A +`to_spec` refuses a divisor that a `missing: 0` parameter can make zero, +unless a [guard](#a-guarded-divisor) leaves the missing row out. A deleted row has [no dual](named.md#reading-a-constraints-dual). diff --git a/src/mathspec/_condition_resolver.py b/src/mathspec/_condition_resolver.py index 0cb3763e..4d97f389 100644 --- a/src/mathspec/_condition_resolver.py +++ b/src/mathspec/_condition_resolver.py @@ -26,6 +26,7 @@ UnresolvedCountNode, ) from mathspec._dimensions import join_dims +from mathspec._divisors import zero_divisor_refusals from mathspec._expansion import expand from mathspec._expression_parser import ( ArithmeticNode, @@ -411,6 +412,7 @@ def _expression_comparison(self, node: UnresolvedComparisonNode) -> ExpressionCo dims |= set(side.dims) except LanguageError as e: self.errors.append(str(e)) + self.errors.extend(zero_divisor_refusals(side, context, ns.spec.parameters, {})) if len(self.errors) > found: return node left, right = sides diff --git a/src/mathspec/_divisors.py b/src/mathspec/_divisors.py new file mode 100644 index 00000000..d0995049 --- /dev/null +++ b/src/mathspec/_divisors.py @@ -0,0 +1,170 @@ +# SPDX-FileCopyrightText: mathspec Contributors +# +# SPDX-License-Identifier: MIT + +"""The load-time refusal of a divisor that a missing row of a ``missing: 0`` parameter makes 0. + +The language puts that 0 in, so no data can repair it. A guard spares the +divisor where it is false at every missing row: a conjunct of the ``where`` +of the declaration, of the ``when`` of a case, or of the mask of a variable +that is a factor of the quotient, since an absent factor makes the whole +product absent. A guard holds only at the coordinate it is read at, so a +sum, a window, a shift or a lookup drops every guard from outside it. +""" + +from __future__ import annotations + +from typing import TYPE_CHECKING + +from mathspec.program import ( + Add, + Cases, + ConditionReference, + Divide, + ExpressionReference, + Join, + Mask, + Multiply, + Negate, + ParameterComparison, + ParameterDefined, + ParameterReference, + Power, + Sum, + Translate, + VariableReference, + WindowSum, + children, +) + +if TYPE_CHECKING: + from collections.abc import Iterator, Mapping + + from mathspec.program import ComparisonOperator, Condition, Expression + from mathspec.spec import ParameterSpec + + +def zero_divisor_refusals( + expression: Expression, + context: str, + parameters: Mapping[str, ParameterSpec], + masks: Mapping[str, Mask | None], + where: Mask | None = None, +) -> list[str]: + """A refusal for each ``missing: 0`` parameter that can make a divisor under *expression* 0. + + *masks* are the variables' ``where`` masks, and *where* is the mask of the + declaration that holds *expression*. A named expression is not entered: + it is read over its own frame, so it is checked as its own entry. + """ + names = dict.fromkeys(_zero_divisors(expression, parameters, masks, _spared(where))) + return [ + f"{context}: the divisor reads '{name}', which is declared missing: 0, so a missing row of '{name}' " + f'makes the divisor 0, which no number divides by. Declare missing: refused, absent, or a value other ' + f'than 0, or guard the quotient with a where such as "{name} > 0".' + for name in names + ] + + +def _zero_divisors( + e: Expression, parameters: Mapping[str, ParameterSpec], masks: Mapping[str, Mask | None], spared: frozenset[str] +) -> Iterator[str]: + """Each parameter not in *spared* whose missing row zeroes a divisor under *e*.""" + match e: + case Multiply() | Divide(): + for factor in _factors(e): + if isinstance(factor, VariableReference): + spared |= _spared(masks.get(factor.name)) + if isinstance(e, Divide) and (name := _zero_where_missing(e.divisor, parameters, spared)) is not None: + yield name + case Cases(regions=regions): + for region in regions: + yield from _zero_divisors(region.value, parameters, masks, spared | _spared(region.when)) + return + case Sum() | WindowSum() | Translate() | Join(): + spared = frozenset() + case ExpressionReference(): + return + for child in children(e): + yield from _zero_divisors(child, parameters, masks, spared) + + +def _factors(e: Expression) -> tuple[Expression, ...]: + """The factors of the product *e* heads, through a negation; a divisor is no factor, since it never is absent alone.""" + match e: + case Multiply(left=left, right=right): + return _factors(left) + _factors(right) + case Divide(numerator=numerator): + return _factors(numerator) + case Negate(operand=operand): + return _factors(operand) + return (e,) + + +def _zero_where_missing(e: Expression, parameters: Mapping[str, ParameterSpec], spared: frozenset[str]) -> str | None: + """The ``missing: 0`` parameter not in *spared* whose missing row makes *e* 0, or ``None`` where no missing row can. + + A factor, the numerator of a quotient, the base of a power, and the + operand of a sum, a shift, a lookup or a named expression make *e* 0 where + they are 0; a sum of terms only where every term is, so ``p + 1`` never + is; a case where any region is. + """ + match e: + case ParameterReference(name=name): + declared = parameters.get(name) + return name if declared is not None and declared.missing == 0 and name not in spared else None + case Sum(operand=operand) | WindowSum(operand=operand) | Translate(operand=operand) | Join(operand=operand): + return _zero_where_missing(operand, parameters, frozenset()) + case Negate(operand=operand) | ExpressionReference(body=operand): + return _zero_where_missing(operand, parameters, spared) + case Multiply(left=left, right=right): + return _zero_where_missing(left, parameters, spared) or _zero_where_missing(right, parameters, spared) + case Divide(numerator=numerator): + return _zero_where_missing(numerator, parameters, spared) + case Power(base=base): + return _zero_where_missing(base, parameters, spared) + case Add(left=left, right=right): + name = _zero_where_missing(left, parameters, spared) + return name if name is not None and _zero_where_missing(right, parameters, spared) is not None else None + case Cases(regions=regions): + return next( + (n for r in regions if (n := _zero_where_missing(r.value, parameters, spared | _spared(r.when)))), + None, + ) + return None + + +def _spared(mask: Mask | None) -> frozenset[str]: + """The parameters whose every missing row *mask* leaves out, read off its ``AND`` spine.""" + if mask is None: + return frozenset() + return frozenset(name for conjunct in mask.conjuncts for name in _left_out(conjunct)) + + +def _left_out(conjunct: Condition) -> frozenset[str]: + """The parameter a conjunct is false at wherever its row is missing and it reads as 0.""" + match conjunct: + case ParameterDefined(name=name): + return frozenset({name}) + case ParameterComparison(name=name, op=op, value=float() | int() as value) if not _holds(0.0, op, value): + return frozenset({name}) + case ConditionReference(body=body): + return _spared(Mask(body)) + return frozenset() + + +def _holds(left: float, op: ComparisonOperator, right: float) -> bool: + """Whether ``left right`` holds.""" + match op: + case '<': + return left < right + case '<=': + return left <= right + case '>': + return left > right + case '>=': + return left >= right + case '==': + return left == right + case '!=': + return left != right diff --git a/src/mathspec/_expression_resolver.py b/src/mathspec/_expression_resolver.py index 1ee9db23..6d2edb27 100644 --- a/src/mathspec/_expression_resolver.py +++ b/src/mathspec/_expression_resolver.py @@ -44,12 +44,10 @@ from mathspec.program import ( Add, Axis, - Cases, Constant, Divide, Dual, Expression, - ExpressionReference, Join, JoinColumns, Multiply, @@ -71,7 +69,6 @@ from collections.abc import Mapping from mathspec._resolution import Namespace - from mathspec.spec import ParameterSpec #: An ``edge=`` as a translation carries it: whether it wraps, and the number @@ -86,38 +83,6 @@ MAX_RESOLVED_DEPTH = 3 * MAX_DEPTH -def _zero_where_missing(e: Expression, parameters: Mapping[str, ParameterSpec]) -> str | None: - """The ``missing: 0`` parameter whose missing row makes *e* 0, or ``None`` where no missing row can. - - The language puts that 0 in, so a divisor it can zero is refused at load. - A factor, the numerator of a quotient, the base of a power, and the - operand of a sum, a shift, a lookup or a named expression make *e* 0 where - they are 0; a sum of terms only where every term is, so ``p + 1`` never - is; a case where any region is. - """ - match e: - case ParameterReference(name=name): - declared = parameters.get(name) - zero = declared is not None and declared.missing == 0 - return name if zero else None - case Negate(operand=operand) | Sum(operand=operand) | WindowSum(operand=operand) | Translate(operand=operand): - return _zero_where_missing(operand, parameters) - case Join(operand=operand) | ExpressionReference(body=operand): - return _zero_where_missing(operand, parameters) - case Multiply(left=left, right=right): - return _zero_where_missing(left, parameters) or _zero_where_missing(right, parameters) - case Divide(numerator=numerator): - return _zero_where_missing(numerator, parameters) - case Power(base=base): - return _zero_where_missing(base, parameters) - case Add(left=left, right=right): - name = _zero_where_missing(left, parameters) - return name if name is not None and _zero_where_missing(right, parameters) is not None else None - case Cases(regions=regions): - return next((n for r in regions if (n := _zero_where_missing(r.value, parameters)) is not None), None) - return None - - @dataclass(frozen=True) class ExpressionResolver: """One resolution walk over an expression, and the three things every step of it reads. @@ -208,26 +173,12 @@ def _binary(self, node: BinaryOperatorNode) -> Expression | None: case '*': return Multiply(left, right, dims=dims) case '/': - if self._zero_divisor(right): - return None return Divide(left, right, dims=dims) case '**': return Power(left, right, dims=dims) case _: assert_never(node.op) - def _zero_divisor(self, divisor: Expression) -> bool: - """Whether a missing row of a ``missing: 0`` parameter can make *divisor* 0, recorded as an error.""" - name = _zero_where_missing(divisor, self.ns.spec.parameters) - if name is None: - return False - self.errors.append( - f"{self.context}: the divisor reads '{name}', which is declared missing: 0, so a missing row of '{name}' " - f'makes the divisor 0, which no number divides by. Declare missing: refused, absent, or a value other ' - f'than 0.' - ) - return True - def _name(self, node: NameNode) -> Expression | None: """A bare name as the variable, parameter or named expression it declares; a dimension or relation is not a value. diff --git a/src/mathspec/_lowering.py b/src/mathspec/_lowering.py index da43b0d7..0155eace 100644 --- a/src/mathspec/_lowering.py +++ b/src/mathspec/_lowering.py @@ -18,6 +18,7 @@ from typing import TYPE_CHECKING from mathspec._dimensions import check_spec, sorted_dims +from mathspec._divisors import zero_divisor_refusals from mathspec._expansion import expand, parse_template from mathspec._piecewise import assumptions_of, curve_frame, lp_domain_refusal, refused_under_points, resolve_links from mathspec._resolution import ( @@ -187,6 +188,7 @@ def lower(spec: Spec) -> Program: errors.append(refusal) curves[pname] = links + errors.extend(_zero_divisor_refusals(spec, variables, entries, constraints, objective, curves)) if errors: raise ns.error(errors) @@ -338,6 +340,34 @@ def _loop(target: str, entry: ExpressionReference, sums: Mapping[str, list[Expre return None +def _zero_divisor_refusals( + spec: Spec, + variables: Mapping[str, Variable], + entries: Mapping[str, ExpressionReference], + constraints: Mapping[str, Constraint], + objective: Objective | None, + curves: Mapping[str, tuple[Expression, ...]], +) -> list[str]: + """[`zero_divisor_refusals`][mathspec._divisors.zero_divisor_refusals] over every expression the file declares. + + Read once every variable mask is resolved, because a masked factor spares + a divisor wherever its mask leaves a missing row out. + """ + masks = {name: v.where for name, v in variables.items()} + found: list[str] = [] + for name, entry in entries.items(): + found += zero_divisor_refusals(entry.body, f"Named expression '{name}'", spec.parameters, masks) + for name, c in constraints.items(): + for side in (c.lhs, c.rhs): + found += zero_divisor_refusals(side, f"Constraint '{name}'", spec.parameters, masks, c.where) + if objective is not None: + found += zero_divisor_refusals(objective.expression, 'The objective', spec.parameters, masks) + for name, links in curves.items(): + for link in links: + found += zero_divisor_refusals(link, f"piecewise '{name}'", spec.parameters, masks) + return list(dict.fromkeys(found)) + + def _frame_of(name: str, entry: ExpressionReference, spec: Spec) -> tuple[str, ...]: """The dims an entry is read over: the ``dims:`` it declares, as written, else the body's, sorted by name.""" declared = spec.expressions[name].dims diff --git a/src/mathspec/spec.py b/src/mathspec/spec.py index d2a9f2f8..c14b2367 100644 --- a/src/mathspec/spec.py +++ b/src/mathspec/spec.py @@ -440,12 +440,12 @@ def _absent_or_a_number(cls, v: object) -> object: def _a_number_fits_the_variable(self) -> VariableSpec: """The number stands for the variable where its mask leaves it out, so a mask must leave something out. - The number lies in the variable's domain and inside its literal bounds. + The number lies in the variable's domain. The bounds hold only inside + the mask, so the number may lie outside them. """ v = self.missing if isinstance(v, str): return self - lower, upper = self.bounds.lower, self.bounds.upper if self.where is None: msg = ( f'missing: {_as_yaml(v)} needs a `where:`. A variable with no mask exists at every ' @@ -455,10 +455,6 @@ def _a_number_fits_the_variable(self) -> VariableSpec: msg = f'missing: {_as_yaml(v)} on a binary variable, which takes 0 or 1.' elif self.domain == 'integer' and not float(v).is_integer(): msg = f'missing: {_as_yaml(v)} on an integer variable, which takes an integer.' - elif isinstance(lower, int | float) and v < lower: - msg = f'missing: {_as_yaml(v)} is below bounds.lower {_as_yaml(lower)}. Write a number inside the bounds.' - elif isinstance(upper, int | float) and v > upper: - msg = f'missing: {_as_yaml(v)} is above bounds.upper {_as_yaml(upper)}. Write a number inside the bounds.' else: return self raise ValueError(msg) diff --git a/tests/test_validation.py b/tests/test_validation.py index 5d4e028c..fba559e2 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -2544,10 +2544,6 @@ def test_a_variable_missing_that_reads_data_is_refused(written, fragment): 'missing: 1.5 on an integer variable, which takes an integer', id='integer', ), - pytest.param({'bounds': {'lower': 0}, 'missing': -1}, 'missing: -1 is below bounds.lower 0', id='below-lower'), - pytest.param( - {'bounds': {'upper': 10}, 'missing': 11}, 'missing: 11 is above bounds.upper 10', id='above-upper' - ), ], ) def test_a_variable_missing_outside_what_the_variable_takes_is_refused(declared, fragment): @@ -2555,6 +2551,24 @@ def test_a_variable_missing_outside_what_the_variable_takes_is_refused(declared, assert fragment in _refusal(**{'variables.p': {'dims': ['g'], 'where': 'c', **declared}}) +@pytest.mark.parametrize( + 'declared', + [ + pytest.param({'bounds': {'lower': 1, 'upper': 4}, 'missing': 0}, id='below-a-literal-lower-bound'), + pytest.param({'bounds': {'lower': -10, 'upper': -1}, 'missing': 0}, id='above-a-literal-upper-bound'), + pytest.param({'domain': 'integer', 'bounds': {'lower': 1}, 'missing': 0}, id='an-integer-with-a-minimum'), + ], +) +def test_a_variable_number_outside_its_bounds_loads(declared): + """`missing: 0` on a variable with `lower: 1` was refused, though the bounds hold only inside the mask. + + A unit of one to four modules where it is a candidate has no modules elsewhere, so the number outside the mask + lies outside the bounds by design. A parameter bound already loaded the same file. + """ + spec = to_spec(varied(SMALL_MODEL, **{'variables.p': {'dims': ['g'], 'where': 'c', **declared}})) + assert spec.program.variables['p'].missing == 0 + + @pytest.mark.parametrize( 'declared', [ @@ -2642,6 +2656,139 @@ def test_a_parameter_read_as_zero_loads_where_it_divides_nothing(patch): assert to_spec(varied(SMALL_MODEL, **patch)).program.constraints['cap'] is not None +@pytest.mark.parametrize( + 'section', + [ + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'c > 0', 'expression': 'p / c <= 1'}}, id='above-zero' + ), + pytest.param({'constraints.cap': {'dims': ['g'], 'where': 'c', 'expression': 'p / c <= 1'}}, id='has-a-row'), + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'c != 0', 'expression': 'p / c <= 1'}}, id='not-zero' + ), + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'flag AND c < -1', 'expression': 'p / c <= 1'}}, + id='in-a-conjunction', + ), + pytest.param( + { + 'conditions.priced': 'c > 0', + 'constraints.cap': {'dims': ['g'], 'where': 'priced', 'expression': 'p / c <= 1'}, + }, + id='a-named-condition', + ), + pytest.param( + { + 'expressions.e': { + 'dims': ['g'], + 'cases': {'on': {'when': 'c > 0', 'expression': '1 / c'}}, + 'otherwise': '0', + } + }, + id='a-case', + ), + pytest.param( + { + 'expressions.e': { + 'dims': ['g'], + 'cases': {'on': {'when': 'c > 0', 'expression': 'c'}}, + 'otherwise': '1', + }, + 'constraints.cap': {'dims': ['g'], 'expression': 'p / e <= 1'}, + }, + id='a-case-in-the-divisor', + ), + pytest.param( + { + 'variables.y': {'dims': ['g'], 'where': 'c > 0'}, + 'constraints.cap': {'dims': [], 'expression': 'sum(y / c, over=g) <= 1'}, + }, + id='a-masked-numerator', + ), + pytest.param( + { + 'variables.y': {'dims': ['g'], 'where': 'c > 0'}, + 'constraints.cap': {'dims': [], 'expression': 'sum(k / c * y, over=g) <= 1'}, + }, + id='a-masked-factor', + ), + ], +) +def test_a_divisor_guarded_against_a_missing_row_loads(section): + """A missing row of a `missing: 0` divisor was refused even where a `where:`, a case or a mask left it out. + + A `where: c > 0` is false at a missing row, so no row divides there, yet the file was refused. + """ + assert to_spec(varied(SMALL_MODEL, **{'parameters.c.missing': 0, **section})) is not None + + +@pytest.mark.parametrize( + 'section', + [ + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'c >= 0', 'expression': 'p / c <= 1'}}, + id='a-guard-that-admits-zero', + ), + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'flag OR c > 0', 'expression': 'p / c <= 1'}}, + id='a-guard-under-an-or', + ), + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'NOT (c > 0)', 'expression': 'p / c <= 1'}}, + id='a-negated-guard', + ), + pytest.param( + { + 'constraints.cap': { + 'dims': ['g'], + 'where': 'c > 0', + 'expression': "p / shift(c, along=g, offset=1, edge='wrap') <= 1", + } + }, + id='a-guard-at-another-coordinate', + ), + pytest.param( + { + 'constraints.cap': { + 'dims': ['g'], + 'where': 'c > 0', + 'expression': "shift(p / c, along=g, offset=1, edge='wrap') <= 1", + } + }, + id='a-guard-outside-a-shift', + ), + pytest.param( + {'constraints.cap': {'dims': ['g'], 'where': 'k / c > 1', 'expression': 'p <= 1'}}, + id='a-quotient-in-a-where', + ), + pytest.param( + {'constraints.cap': {'dims': [], 'where': 'k > 0', 'expression': 'sum(p / c, over=g) <= 1'}}, + id='a-guard-on-another-parameter', + ), + pytest.param( + { + 'variables.y': {'dims': ['g'], 'where': 'c > 0'}, + 'constraints.cap': { + 'dims': [], + 'expression': "sum(shift(y, along=g, offset=1, edge='wrap') / c, over=g) <= 1", + }, + }, + id='a-mask-at-another-coordinate', + ), + pytest.param( + { + 'variables.y': {'dims': ['g'], 'where': 'c > 0'}, + 'constraints.cap': {'dims': [], 'expression': 'sum(y + p / c, over=g) <= 1'}, + }, + id='a-mask-on-another-term', + ), + ], +) +def test_a_guard_that_leaves_a_missing_row_in_does_not_spare_the_divisor(section): + message = _refusal(**{'parameters.c.missing': 0, **section}) + assert "reads 'c', which is declared missing: 0, so a missing row of 'c' makes the divisor 0" in message + + #: One dimension every construct below reads the order of, and a breakpoint #: dimension for the two formulations; neither declares its order. UNORDERED: dict[str, Any] = { From 41bed1dca714dcf1654ef82cfdf9f6b7eecf54a7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 10:07:16 +0000 Subject: [PATCH 2/3] docs(changelog): add the line for #942 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01YZ68heVBrHxKUKsXxqJrXX --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5c42de4b..bf37f053 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ it releases that version ([RELEASING.md](https://github.com/energy-models/mathsp ## Upcoming version +- fix(language): a divisor that a where, a case or a masked variable guards loads under missing: 0, and so does a variable number outside its bounds ([#942](https://github.com/energy-models/mathspec/pull/942)) - 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](https://github.com/energy-models/mathspec/pull/912)) - feat(language)!: a missing row reads as the value the file names, and `missing: neutral` is gone ([#894](https://github.com/energy-models/mathspec/pull/894)) - feat(program): each expression node states the dimensions it is read over ([#899](https://github.com/energy-models/mathspec/pull/899)) From 0aa8a62486a39799e116e681ab29c542ebdaf490 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 10:21:50 +0000 Subject: [PATCH 3/3] fix(language): a variable with a missing: number guards no divisor A masked variable spared a divisor because the product is absent where the variable is absent. A variable with a missing: number is not absent outside its mask: it reads that number, so `sum(y / c, over=g)` with `y: {where: c > 0, missing: 1}` divided 1 by 0 at every missing row of c, and loaded. Only a missing: absent variable spares a divisor now. Found by a differential fuzzer that evaluates random specs on random data. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01YZ68heVBrHxKUKsXxqJrXX --- docs/reference/language/absence.md | 6 ++++-- src/mathspec/_divisors.py | 9 +++++---- src/mathspec/_lowering.py | 6 ++++-- tests/test_validation.py | 7 +++++++ 4 files changed, 20 insertions(+), 8 deletions(-) diff --git a/docs/reference/language/absence.md b/docs/reference/language/absence.md index 9a78a5e6..ed4ee83d 100644 --- a/docs/reference/language/absence.md +++ b/docs/reference/language/absence.md @@ -83,8 +83,10 @@ conditions joined by `AND` in one of these places: - the `where:` of the constraint, - the `when:` of the case that holds the quotient, -- the `where:` of a variable that multiplies the quotient, because the product - is absent where that variable is absent. +- the `where:` of a variable that multiplies the quotient and is + `missing: absent`, because the product is absent where that variable is + absent. A variable with a `missing:` number reads that number outside its + mask, so its mask guards nothing. ```yaml parameters: diff --git a/src/mathspec/_divisors.py b/src/mathspec/_divisors.py index d0995049..80be33bf 100644 --- a/src/mathspec/_divisors.py +++ b/src/mathspec/_divisors.py @@ -6,9 +6,9 @@ The language puts that 0 in, so no data can repair it. A guard spares the divisor where it is false at every missing row: a conjunct of the ``where`` -of the declaration, of the ``when`` of a case, or of the mask of a variable -that is a factor of the quotient, since an absent factor makes the whole -product absent. A guard holds only at the coordinate it is read at, so a +of the declaration, of the ``when`` of a case, or of the mask of a +``missing: absent`` variable that is a factor of the quotient, since an absent +factor makes the whole product absent. A guard holds only at the coordinate it is read at, so a sum, a window, a shift or a lookup drops every guard from outside it. """ @@ -53,7 +53,8 @@ def zero_divisor_refusals( ) -> list[str]: """A refusal for each ``missing: 0`` parameter that can make a divisor under *expression* 0. - *masks* are the variables' ``where`` masks, and *where* is the mask of the + *masks* are the ``where`` masks of the variables that are absent outside + them, and *where* is the mask of the declaration that holds *expression*. A named expression is not entered: it is read over its own frame, so it is checked as its own entry. """ diff --git a/src/mathspec/_lowering.py b/src/mathspec/_lowering.py index 0155eace..3cbfd7fe 100644 --- a/src/mathspec/_lowering.py +++ b/src/mathspec/_lowering.py @@ -351,9 +351,11 @@ def _zero_divisor_refusals( """[`zero_divisor_refusals`][mathspec._divisors.zero_divisor_refusals] over every expression the file declares. Read once every variable mask is resolved, because a masked factor spares - a divisor wherever its mask leaves a missing row out. + a divisor wherever its mask leaves a missing row out. Only a variable that + is absent outside its mask spares one: a ``missing:`` number stands for it + there, and the quotient is read. """ - masks = {name: v.where for name, v in variables.items()} + masks = {name: v.where for name, v in variables.items() if v.missing == 'absent'} found: list[str] = [] for name, entry in entries.items(): found += zero_divisor_refusals(entry.body, f"Named expression '{name}'", spec.parameters, masks) diff --git a/tests/test_validation.py b/tests/test_validation.py index fba559e2..499f69b6 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -2782,6 +2782,13 @@ def test_a_divisor_guarded_against_a_missing_row_loads(section): }, id='a-mask-on-another-term', ), + pytest.param( + { + 'variables.y': {'dims': ['g'], 'where': 'c > 0', 'missing': 1}, + 'constraints.cap': {'dims': [], 'expression': 'sum(y / c, over=g) <= 1'}, + }, + id='a-mask-of-a-variable-that-reads-a-number-outside-it', + ), ], ) def test_a_guard_that_leaves_a_missing_row_in_does_not_spare_the_divisor(section):