From ba0df52da5c52c82523c4b02f3cdfbf24dacb553 Mon Sep 17 00:00:00 2001 From: FBumann <117816358+FBumann@users.noreply.github.com> Date: Mon, 31 Aug 2026 09:50:59 +0200 Subject: [PATCH] feat(language): which dims a mask reads is the language's answer, so two consumers cannot restrict one model differently Co-authored-by: Claude Opus 5 --- src/math_spec/dimensions.py | 77 +++++++++++++++----------------- src/math_spec/where_parser.py | 82 ++++++++++++++++++++++++++++++++++- tests/test_dimensions.py | 65 ++++++++++++++++++++++++++- 3 files changed, 179 insertions(+), 45 deletions(-) diff --git a/src/math_spec/dimensions.py b/src/math_spec/dimensions.py index 327c9ab3..5a0640a4 100644 --- a/src/math_spec/dimensions.py +++ b/src/math_spec/dimensions.py @@ -47,20 +47,14 @@ from math_spec.operators import BUILTINS, edge_error from math_spec.resolution import Namespace, expression_of, where_of from math_spec.where_parser import ( - AndNode, - BooleanLiteralNode, DimensionComparisonNode, DimensionPositionNode, - LookupComparisonNode, - LookupDefinedNode, - LookupPairComparisonNode, - NotNode, - OrNode, ParameterComparisonNode, ParameterDefinedNode, - UnresolvedWhereNode, VariableDefinedNode, WhereNode, + _atom_dims, + atoms, ) if TYPE_CHECKING: @@ -473,49 +467,50 @@ def _check_where_dims( """A predicate may only test dims the frame carries. Reducing an outside dim to fit — with ``any()``, say — is a mask that fails - *open*, silently including everything. It is rejected here, at load - time. + *open*, silently including everything. It is rejected here, at load time. + + **Which dims a leaf reads is not decided here.** That is + :func:`~math_spec.where_parser.dims_read`'s rule, and this walks the same + leaves by the same reading, so a mask cannot be checked against one answer + and built against another. What is decided here is the wording, and the + wording is per leaf: a reader told only that the predicate leaves the frame + would still have to work out which half of it did. """ if node is None: return - if isinstance(node, (ParameterDefinedNode, ParameterComparisonNode)): - pdims = frozenset(schema.parameters[node.name].dims) - if not pdims <= frame: + name_dims = _name_dims(schema) + for atom in atoms(node): + if not (outside := sorted(_atom_dims(atom, name_dims) - frame)): + continue + if isinstance(atom, (ParameterDefinedNode, ParameterComparisonNode)): raise DimensionError( - f"{context}: where-parameter '{node.name}' has dims " - f'{sorted(pdims - frame)} outside the frame {sorted(frame)}. Reducing ' + f"{context}: where-parameter '{atom.name}' has dims " + f'{outside} outside the frame {sorted(frame)}. Reducing ' f'a mask over an unlisted dim would silently widen it.' ) - elif isinstance(node, VariableDefinedNode): - vdims = frozenset(schema.variables[node.name].foreach) - if not vdims <= frame: + if isinstance(atom, VariableDefinedNode): raise DimensionError( - f"{context}: where-variable '{node.name}' has dims " - f'{sorted(vdims - frame)} outside the frame {sorted(frame)}. A mask ' + f"{context}: where-variable '{atom.name}' has dims " + f'{outside} outside the frame {sorted(frame)}. A mask ' f'reducing over an unlisted dim would silently widen it — say which ' f'reduction you mean.' ) - elif isinstance(node, (DimensionComparisonNode, DimensionPositionNode)): - if node.name not in frame: + if isinstance(atom, (DimensionComparisonNode, DimensionPositionNode)): raise DimensionError( - f"{context}: where-comparison on dimension '{node.name}', which is not in the frame {sorted(frame)}." + f"{context}: where-comparison on dimension '{atom.name}', which is not in the frame {sorted(frame)}." ) - elif isinstance(node, (LookupComparisonNode, LookupPairComparisonNode, LookupDefinedNode)): - if node.over not in frame: - raise DimensionError( - f"{context}: where-comparison on lookup '{node.name}', which is over " - f"dimension '{node.over}' — not in the frame {sorted(frame)}. A lookup is " - f'read on the dim it maps out of, so that dim has to be one the ' - f'declaration ranges over.' - ) - elif isinstance(node, NotNode): - _check_where_dims(node.operand, schema, frame, context) - elif isinstance(node, (AndNode, OrNode)): - _check_where_dims(node.left, schema, frame, context) - _check_where_dims(node.right, schema, frame, context) - elif isinstance(node, UnresolvedWhereNode): - msg = f'{type(node).__name__} reached the dim checker unresolved.' - raise AssertionError(msg) - elif not isinstance(node, BooleanLiteralNode): - assert_never(node) + raise DimensionError( + f"{context}: where-comparison on lookup '{atom.name}', which is over " + f"dimension '{atom.over}' — not in the frame {sorted(frame)}. A lookup is " + f'read on the dim it maps out of, so that dim has to be one the ' + f'declaration ranges over.' + ) + + +def _name_dims(schema: Spec) -> dict[str, tuple[str, ...]]: + """Every declared name to the dims it is read through — what :func:`~math_spec.where_parser.dims_read` takes.""" + return { + **{name: tuple(pdef.dims) for name, pdef in schema.parameters.items()}, + **{name: tuple(vdef.foreach) for name, vdef in schema.variables.items()}, + } diff --git a/src/math_spec/where_parser.py b/src/math_spec/where_parser.py index 4ab5806a..66daa8eb 100644 --- a/src/math_spec/where_parser.py +++ b/src/math_spec/where_parser.py @@ -13,7 +13,7 @@ import re from dataclasses import dataclass -from typing import TYPE_CHECKING, Any, Literal, cast +from typing import TYPE_CHECKING, Any, Literal, assert_never, cast import pyparsing as pp @@ -22,7 +22,7 @@ if TYPE_CHECKING: import datetime - from collections.abc import Callable + from collections.abc import Callable, Iterator, Mapping, Sequence PredicateOperator = Literal['<=', '>=', '==', '!=', '<', '>'] @@ -230,6 +230,84 @@ class OrNode: ConnectiveWhereNode = NotNode | AndNode | OrNode +# --------------------------------------------------------------------------- +# What a predicate reads +# --------------------------------------------------------------------------- + + +def atoms(where: WhereNode) -> Iterator[TypedPredicateNode]: + """Every node in *where* that reads a declaration, connectives removed. + + A predicate is a tree of :data:`ConnectiveWhereNode` over leaves that each + name one declaration, so every question about what a mask *reads* is asked + of the leaves and answered by taking them together. A boolean literal reads + nothing and yields nothing. + + Raises: + AssertionError: An unresolved node, which is a pass running before + resolution rather than a predicate with a property to read. + """ + if isinstance(where, NotNode): + yield from atoms(where.operand) + elif isinstance(where, (AndNode, OrNode)): + yield from atoms(where.left) + yield from atoms(where.right) + elif isinstance(where, UnresolvedWhereNode): + msg = f'{type(where).__name__} reached a predicate walk unresolved.' + raise AssertionError(msg) + elif not isinstance(where, BooleanLiteralNode): + yield where + + +def dims_read(where: WhereNode, name_dims: Mapping[str, Sequence[str]]) -> frozenset[str]: + """Which dims *where* reads, given what each declared name is read through. + + The dim rule for the predicate side, stated once: **a mask is read at the + coordinates its leaves are read at**. A parameter is read through its own + dims, a variable through the frame it is declared over, a comparison on a + dimension through that dimension, and a lookup through the dimension it + maps out of — a lookup being read on the dim it leaves, not the one it + lands in. + + A consumer masking rows needs this to know which coordinates a mask can + restrict, and answering it separately is the mistake + ``what-counts-as-language.md`` forbids: two consumers deciding differently + would mask the same model differently, with no error anywhere. + + Args: + where: A resolved predicate. + name_dims: Every declared name to the dims it is read through — + parameters by their ``dims`` and variables by their ``foreach``, + one flat mapping because the language has one flat namespace. + + Returns: + The dims read, which is empty for a predicate over nothing but + literals. + """ + return frozenset(dim for atom in atoms(where) for dim in _atom_dims(atom, name_dims)) + + +def _atom_dims(atom: TypedPredicateNode, name_dims: Mapping[str, Sequence[str]]) -> frozenset[str]: + """One leaf's dims — the rule :func:`dims_read` is the union of. + + Private because a caller wanting one leaf's answer wants the whole + predicate's, and separate because the load-time frame check reports per + leaf and so cannot take the union. Closed by ``assert_never``: a predicate + node added without a reading is a type error here, at the one place that + has to grow a branch, rather than a wrong dim set at the first model to use + it. + """ + match atom: + case ParameterComparisonNode() | ParameterDefinedNode() | VariableDefinedNode(): + return frozenset(name_dims.get(atom.name, ())) + case DimensionComparisonNode() | DimensionPositionNode(): + return frozenset({atom.name}) + case LookupComparisonNode() | LookupPairComparisonNode() | LookupDefinedNode(): + return frozenset({atom.over}) + case _: + assert_never(atom) + + # --------------------------------------------------------------------------- # Grammar # --------------------------------------------------------------------------- diff --git a/tests/test_dimensions.py b/tests/test_dimensions.py index 8b0546ae..e7063d43 100644 --- a/tests/test_dimensions.py +++ b/tests/test_dimensions.py @@ -14,9 +14,10 @@ import pytest -from math_spec.dimensions import DimensionError, check_schema, dims_of -from math_spec.resolution import Namespace, expression_of +from math_spec.dimensions import DimensionError, _check_where_dims, _name_dims, check_schema, dims_of +from math_spec.resolution import Namespace, expression_of, where_of from math_spec.validation import to_spec +from math_spec.where_parser import dims_read from tests.fixtures import OPERATOR_PROBES, override, schema_of if TYPE_CHECKING: @@ -276,3 +277,63 @@ def test_a_zero_step_vacates_nothing_and_needs_no_edge(self): """ raw = override(self.BASE, **{'constraints.k.expression': 'p <= shift(cap, over=g, offset=0)'}) assert to_spec(raw) is not None, 'a zero step is none at all, so no edge policy is owed' + + +# --------------------------------------------------------------------------- +# what a predicate reads +# --------------------------------------------------------------------------- + + +@pytest.mark.parametrize( + ('predicate', 'expected'), + [ + pytest.param('p_max > 0', {'generator'}, id='a-parameter-through-its-own-dims'), + pytest.param('snapshot == 0', {'snapshot'}, id='a-dimension-through-itself'), + pytest.param('position(snapshot) == 0', {'snapshot'}, id='a-position-through-the-axis-it-counts'), + pytest.param('snap_bus == "b1"', {'snapshot'}, id='a-lookup-through-the-dim-it-maps-out-of'), + pytest.param('p_max > 0 AND snapshot == 0', {'generator', 'snapshot'}, id='a-conjunction-reads-both-sides'), + pytest.param('NOT p_max > 0', {'generator'}, id='a-negation-reads-what-it-negates'), + pytest.param('False', set(), id='a-literal-reads-nothing'), + ], +) +def test_a_predicate_is_read_at_the_coordinates_its_leaves_are_read_at(predicate, expected): + """The dim rule for the predicate side, which a consumer masking rows needs. + + Stated here rather than in whichever engine builds the mask: two consumers + answering it differently would restrict the same model differently, with no + error anywhere to say which was meant. + """ + schema = to_spec(BASE) + ns = Namespace.of(schema) + name_dims = _name_dims(schema) + + where = where_of(predicate, ns, 'test') + + assert where is not None, 'a predicate the connectives cannot settle survives the fold' + assert dims_read(where, name_dims) == expected, f'{predicate!r} reads {expected}' + + +def test_a_predicate_that_admits_every_row_has_no_leaves_left_to_read(): + """`where_of` folds an always-true mask to `None`, so there is no node to ask.""" + schema = to_spec(BASE) + + assert where_of('True', Namespace.of(schema), 'test') is None, 'folded away, not a predicate over nothing' + + +def test_the_frame_check_and_the_reading_walk_the_same_leaves(): + """One rule, two readers — the check reports per leaf and so cannot take the union. + + A predicate outside the frame is refused by the *name* of the leaf that + left it, and that leaf is one `dims_read` counted: a check passing a mask + the builder then reads wider would be the divergence this shares a walk to + prevent. + """ + schema = to_spec(BASE) + ns = Namespace.of(schema) + + where = where_of('p_max > 0', ns, 'test') + assert where is not None + + assert dims_read(where, _name_dims(schema)) == {'generator'}, 'read at the generator axis' + with pytest.raises(DimensionError, match=r"where-parameter 'p_max' has dims \['generator'\]"): + _check_where_dims(where, schema, frozenset({'snapshot'}), 'test')