From a0377abd27c1b6a37a2660995b75357688a2f52a Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 22 Aug 2026 09:03:19 +0000 Subject: [PATCH 1/3] feat: a static partition check for constraint cases MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A constraint with `cases:` is one rule whose expression varies by region, and it is *one* constraint — one name, one row per coordinate, one dual — only if the cases claim each row exactly once. This decides that claim before any data binds, which is rule 2 in a new position. Both obligations are conditioned on the constraint's own `where`, which keeps that key meaning exactly what it means today (which rows exist) while `cases` says only which expression each existing row gets: disjoint where AND case_i AND case_j unsatisfiable exhaustive where AND NOT (case_1 OR ... case_n) unsatisfiable no dead case where AND case_i satisfiable Conditioning cuts both ways: cases overlapping somewhere the `where` already excludes are not an ambiguity and an unconditional check would refuse them, while a `where` wider than the cases cover is a gap that a "the rows are whatever the cases claim" reading could not express. Atoms are grouped by the subject they talk about and each subject is cut into cells, so equality against distinct labels comes out exclusive — a purely propositional reading invents a region where a storage is both a battery and hydrogen, and refuses the category split that motivates the feature. Three outcomes, and the third is refused rather than assumed: two positions counted from opposite ends of a dimension whose extent only data knows are the same row on a one-member axis. Every case carries its own mask. An open "everything else" case would have made exhaustiveness true by construction, but `not (x)` says the same thing and a mask edited without its restated negation lands here as a gap or an overlap rather than a silent change of model. Not wired into the schema: `cases:` is not a key the model accepts, and the spelling is still open (#2). This is the decision procedure the argument turns on, so it can be judged on what it proves and refuses. Tests pin one atom's reading at a time, plus a seeded fuzz asserting that anything proved a partition survives a value grid finer than the cells. Two of them cover a split counted from the back, where the rank cells had to mirror: the open end is before the earliest position named, since nothing follows -1. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01ADtfZf4V6W9XcLRSwSgHzE --- src/math_spec/partition.py | 652 +++++++++++++++++++++++++++++++++++++ tests/test_partition.py | 307 +++++++++++++++++ 2 files changed, 959 insertions(+) create mode 100644 src/math_spec/partition.py create mode 100644 tests/test_partition.py diff --git a/src/math_spec/partition.py b/src/math_spec/partition.py new file mode 100644 index 00000000..a5e838e3 --- /dev/null +++ b/src/math_spec/partition.py @@ -0,0 +1,652 @@ +# SPDX-FileCopyrightText: math-spec Contributors +# +# SPDX-License-Identifier: MIT + +"""Does a set of case masks partition a constraint's rows? Decided without data. + +A constraint with ``cases:`` is one rule whose expression varies by region. It +is *one* constraint — one name, one row per coordinate, one dual — only if the +cases claim each row **exactly once**. That claim is decidable here, before any +data binds, which is rule 2 in a new position. + +Two obligations, both conditioned on the constraint's own ``where`` (the rows +that exist at all), and both the same unsatisfiability question: + +* **disjoint** — ``where AND case_i AND case_j`` is unsatisfiable, for every pair +* **exhaustive** — ``where AND NOT (case_1 OR ... OR case_n)`` is unsatisfiable + +and one that falls out of the same machinery for free: + +* **no dead case** — ``where AND case_i`` unsatisfiable means that block builds + no rows, which is a mistake rather than a no-op. + +Conditioning matters in both directions. Two cases that overlap somewhere the +``where`` already excludes are *not* an ambiguity, and an unconditional check +would refuse them; a ``where`` wider than the cases cover is a real gap that a +"the rows are whatever the cases claim" reading could not even express. + +## How it decides + +Every atom in the where-grammar talks about exactly one **subject** — a +parameter, a dimension's coordinates, a dimension's *rank*, a lookup, a pair of +lookups. Atoms with different subjects are independent; atoms sharing one are +not, and that is where a propositional reading goes wrong: on `kind == 'battery'` +and `kind == 'h2'` it invents a world where both hold and reports an overlap +that no data can produce. + +So each subject is split into **cells** — finitely many regions its value can +sit in, chosen so that every atom over that subject is constant on each cell. +The cells of all subjects are multiplied out, and each masks is evaluated on +each cell. A cell where two cases are true is a witness for overlap; a cell +inside ``where`` where none is, a witness for a gap. Because the cells cover +every value the subject can take, "no witness" is a proof and not a sample. + +## Three outcomes, and why the third is not optional + +:attr:`Status.PARTITION`, :attr:`Status.VIOLATED` and +:attr:`Status.UNDECIDED`. Undecided is *refused* by the caller, never assumed: +a checker that guesses in the cases it cannot decide buys nothing over no +checker at all. What lands there is named in :class:`Verdict.reason` along with +the rewrite — the common one being two ``position()`` splits counted from +opposite ends of a dimension whose extent only data knows, where ``0`` and +``-1`` are the same row on a one-member axis and the split is a partition +everywhere else. + +Independence between subjects is an **over**-approximation: the product of +cells contains worlds the data may never produce, so a spurious world can only +manufacture a witness, never hide one. Every outcome here is therefore +conservative — this refuses groups that would have been fine, and admits none +that would not. + +Not wired into the schema: ``cases:`` is not a key the model accepts yet +(energy-models/math-spec#2), and which spelling it lands on does not change +anything below. +""" + +from __future__ import annotations + +import datetime +import itertools +import math +from dataclasses import dataclass, field +from enum import Enum +from typing import TYPE_CHECKING, Any, Literal + +from math_spec.where_parser import ( + AndNode, + BooleanLiteralNode, + DimensionComparisonNode, + DimensionPositionNode, + LookupComparisonNode, + LookupDefinedNode, + LookupPairComparisonNode, + NotNode, + OrNode, + ParameterComparisonNode, + ParameterDefinedNode, + VariableDefinedNode, +) + +if TYPE_CHECKING: + from collections.abc import Iterable, Iterator + + from math_spec.model import Model + from math_spec.where_parser import PredicateOperator, WhereNode + +#: The product of every subject's cells is enumerated, so the bound is on the +#: product rather than on any one subject. Real masks carry two to four atoms; +#: a group that blows this is telling you it is several constraints. +CELL_BUDGET = 8192 + + +class Status(Enum): + """What the check established. :attr:`UNDECIDED` is a refusal, not a pass.""" + + PARTITION = 'partition' + VIOLATED = 'violated' + UNDECIDED = 'undecided' + + +# --------------------------------------------------------------------------- +# cells +# --------------------------------------------------------------------------- + + +class Special(Enum): + """Values a cell can hold that are not values of the subject's own type.""" + + #: No row in the table. A null compares false whatever the comparator, and + #: is not `defined`. + NULL = 'null' + #: A magnitude, and the one that is a *value* everywhere else but is not + #: `defined` — see the bare-name row of the where-string table. + POS_INF = '+inf' + NEG_INF = '-inf' + #: A label none of the masks names. Stands for every such label at once, + #: which they cannot tell apart. + OTHER = 'other' + + +#: What one subject's value is, in one cell. +Cell = float | str | bool | int | datetime.date | Special + + +@dataclass(frozen=True) +class Subject: + """What an atom talks about — the key its cells are built for. + + ``kind`` separates the namespaces that could otherwise collide: a + dimension's coordinates and its *rank* are two subjects over one name, and + a rank is further split by the ``by=`` lookup it is counted within. + """ + + kind: Literal['param', 'dim', 'rank', 'lookup', 'lookup_pair', 'variable'] + name: str + qualifier: str | None = None + + def __str__(self) -> str: + if self.kind == 'rank': + within = f' within {self.qualifier}' if self.qualifier else '' + return f'the position of {self.name}{within}' + if self.kind == 'lookup_pair': + return f'{self.name} vs {self.qualifier}' + return self.name + + +class Undecidable(Exception): # noqa: N818 + """An atom this procedure will not reason about. Carries the rewrite.""" + + +# --------------------------------------------------------------------------- +# the verdict +# --------------------------------------------------------------------------- + +#: One cell, as ``subject -> value``, rendered for a message. +Witness = dict[str, str] + + +@dataclass(frozen=True) +class Overlap: + """Two cases that can both claim one row.""" + + cases: tuple[str, str] + witness: Witness + + +@dataclass(frozen=True) +class Gap: + """A row the ``where`` builds that no case gives an expression to.""" + + witness: Witness + + +@dataclass(frozen=True) +class Verdict: + status: Status + overlaps: tuple[Overlap, ...] = () + gaps: tuple[Gap, ...] = () + dead: tuple[str, ...] = () + reason: str | None = None + + @property + def ok(self) -> bool: + return self.status is Status.PARTITION + + def message(self) -> str: + """What a load error would print. Empty for a proven partition.""" + if self.status is Status.PARTITION: + return '' + if self.status is Status.UNDECIDED: + return f'cannot decide statically: {self.reason}' + parts = [] + for overlap in self.overlaps: + first, second = overlap.cases + parts.append(f"cases '{first}' and '{second}' both claim a row where {_render(overlap.witness)}") + parts.extend(f'no case claims the row where {_render(gap.witness)}' for gap in self.gaps) + parts.extend(f"case '{name}' builds no rows" for name in self.dead) + return '; '.join(parts) + + +def _render(witness: Witness) -> str: + return ', '.join(f'{subject} is {value}' for subject, value in witness.items()) + + +@dataclass(frozen=True) +class Case: + """One case of a group: a mask, and the name the LaTeX prints beside it. + + Every case carries one. An open "everything the others left" case would + save restating a long mask, but nothing else — ``not (x)`` says the same + thing, and a mask edited without its restated negation is a gap or an + overlap here rather than a silent change of model. + """ + + name: str + when: WhereNode + + +# --------------------------------------------------------------------------- +# entry point +# --------------------------------------------------------------------------- + + +def check_partition(where: WhereNode | None, cases: Iterable[Case], schema: Model) -> Verdict: + """Decide whether *cases* partition the rows *where* builds. + + Args: + where: The constraint's own mask — the rows that exist. ``None`` is + everything the ``foreach`` spans. + cases: The cases, in declaration order, each with its own mask. + schema: Read for dtypes, and for the declared ``values:`` that give a + dimension a statically known extent. + + Returns: + The verdict. :attr:`Status.UNDECIDED` is a refusal — see the module + docstring. + """ + cases = list(cases) + masks = [node for node in [where, *(case.when for case in cases)] if node is not None] + try: + domains = _domains(masks, schema) + except Undecidable as exc: + return Verdict(Status.UNDECIDED, reason=str(exc)) + + # The cells of a rank subject are counted from the front wherever the + # extent is known, so the positions the atoms carry have to be read in that + # same frame — `position(dim) == -1` on a three-member axis is rank 2. + extents = { + subject: extent + for subject in domains + if subject.kind == 'rank' and (extent := _extent_of(subject, schema)) is not None + } + + size = math.prod(len(cells) for cells in domains.values()) if domains else 1 + if size > CELL_BUDGET: + return Verdict( + Status.UNDECIDED, + reason=f'{size} regions to check exceeds the budget of {CELL_BUDGET} — split this into named constraints', + ) + + overlaps: list[Overlap] = [] + gaps: list[Gap] = [] + live: set[str] = set() + try: + for cell in _cells(domains): + if not _evaluate(where, cell, extents): + continue + hits = [case.name for case in cases if _evaluate(case.when, cell, extents)] + if len(hits) > 1: + overlaps.append(Overlap((hits[0], hits[1]), _witness(cell))) + elif not hits: + gaps.append(Gap(_witness(cell))) + live.update(hits) + except Undecidable as exc: + return Verdict(Status.UNDECIDED, reason=str(exc)) + + dead = tuple(case.name for case in cases if case.name not in live) + if overlaps or gaps or dead: + return Verdict(Status.VIOLATED, tuple(overlaps[:4]), tuple(gaps[:4]), dead) + return Verdict(Status.PARTITION) + + +# --------------------------------------------------------------------------- +# building the cells +# --------------------------------------------------------------------------- + + +@dataclass +class _Observed: + """What the masks say about one subject, before it is cut into cells.""" + + literals: set[Any] = field(default_factory=set) + positions: set[int] = field(default_factory=set) + bare: bool = False + ordered: bool = False + + +def _domains(masks: Iterable[WhereNode], schema: Model) -> dict[Subject, list[Cell]]: + observed: dict[Subject, _Observed] = {} + for mask in masks: + for node in _walk(mask): + _observe(node, observed, schema) + return {subject: _cells_for(subject, seen, schema) for subject, seen in observed.items()} + + +def _walk(node: WhereNode | None) -> Iterator[WhereNode]: + """Every atom in *node*; the connectives are stepped through.""" + if node is None: + return + if isinstance(node, NotNode): + yield from _walk(node.operand) + elif isinstance(node, AndNode | OrNode): + yield from _walk(node.left) + yield from _walk(node.right) + else: + yield node + + +def _observe(node: WhereNode, observed: dict[Subject, _Observed], schema: Model) -> None: + subject = _subject_of(node) + if subject is None: + return + seen = observed.setdefault(subject, _Observed()) + if isinstance(node, ParameterDefinedNode | VariableDefinedNode | LookupDefinedNode): + seen.bare = True + elif isinstance(node, DimensionPositionNode): + # Every comparator reads here: `position()` converts the dimension to + # an integer, so an ordering is an ordering of integers (#32). + seen.positions.add(node.position) + elif isinstance(node, LookupPairComparisonNode): + if node.op not in ('==', '!='): + msg = f'{subject} compared with {node.op!r}; two lookups compare only with == or !=' + raise Undecidable(msg) + elif isinstance(node, ParameterComparisonNode | DimensionComparisonNode | LookupComparisonNode): + if node.op not in ('==', '!='): + seen.ordered = True + seen.literals.add(node.value) + if seen.ordered and isinstance(node, ParameterComparisonNode | DimensionComparisonNode | LookupComparisonNode): + dtype = _dtype_of(subject, schema) + if dtype not in ('float', 'int', 'datetime', 'date'): + msg = f'{subject} has dtype {dtype!r} and is ordered with {node.op!r}; only == and != are decided here' + raise Undecidable(msg) + + +def _subject_of(node: WhereNode) -> Subject | None: + match node: + case BooleanLiteralNode(): + return None + case ParameterDefinedNode(name=name) | ParameterComparisonNode(name=name): + return Subject('param', name) + case VariableDefinedNode(name=name): + return Subject('variable', name) + case DimensionComparisonNode(name=name): + return Subject('dim', name) + case DimensionPositionNode(name=name, by=by): + return Subject('rank', name, by) + case LookupDefinedNode(name=name) | LookupComparisonNode(name=name): + return Subject('lookup', name) + case LookupPairComparisonNode(name=name, other=other): + return Subject('lookup_pair', name, other) + case _: + msg = f'{type(node).__name__} is not an atom this procedure knows' + raise Undecidable(msg) + + +def _dtype_of(subject: Subject, schema: Model) -> str | None: + if subject.kind == 'param': + block = schema.parameters.get(subject.name) + return None if block is None else block.dtype + if subject.kind == 'dim': + block = schema.dimensions.get(subject.name) + return None if block is None else block.dtype + return None + + +def _cells_for(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: + if subject.kind == 'rank': + return _rank_cells(subject, seen, schema) + if subject.kind == 'lookup_pair': + return [True, False] + if subject.kind == 'variable': + return [True, False] + dtype = _dtype_of(subject, schema) + if dtype == 'bool': + if seen.literals: + msg = f'{subject} has dtype bool and is compared to a literal' + raise Undecidable(msg) + return [Special.NULL, True, False] + numeric = _numeric(dtype, seen.literals) + cells: list[Cell] = [] + # A dimension's coordinates are its own index, so there is no null among + # them; everything else may be absent, and absence is a region of its own + # because a null compares false and is not `defined`. + if subject.kind != 'dim': + cells.append(Special.NULL) + if numeric: + # `defined` excludes an infinity, so it needs a region where every + # comparison still reads normally but the bare name is false. + cells.extend([Special.NEG_INF, Special.POS_INF]) + cells.extend(_ordered_cells(seen.literals) if numeric or _dated(seen.literals) else _label_cells(seen.literals)) + return cells + + +def _numeric(dtype: str | None, literals: set[Any]) -> bool: + """Is this subject a magnitude? The declaration says so where it is known.""" + if dtype is not None: + return dtype in ('float', 'int') + return bool(literals) and all(isinstance(value, int | float) and not isinstance(value, bool) for value in literals) + + +def _dated(literals: set[Any]) -> bool: + return bool(literals) and all(isinstance(value, datetime.date) for value in literals) + + +def _ordered_cells(literals: set[Any]) -> list[Cell]: + """Each literal, and one representative of the gap on either side of it. + + The representatives stand for every value in their gap, which they may + because each atom over this subject compares against one of the literals — + so two values with no literal between them are indistinguishable to every + mask here. + """ + if not literals: + return [0.0] + values = sorted(literals) + step = _step(values[0]) + cells: list[Cell] = [values[0] - step] + for index, value in enumerate(values): + cells.append(value) + following = values[index + 1] if index + 1 < len(values) else None + if following is None: + continue + between = _between(value, following, step) + if between is not None: + cells.append(between) + cells.append(values[-1] + step) + return cells + + +def _step(value: Any) -> Any: + """How far outside the named literals a representative has to sit.""" + if isinstance(value, datetime.datetime): + return datetime.timedelta(seconds=1) + if isinstance(value, datetime.date): + return datetime.timedelta(days=1) + return 1.0 + + +def _between(value: Any, following: Any, step: Any) -> Any | None: + """A value strictly between two literals, where the type admits one. + + A magnitude always does — the midpoint. A date is discrete, so the gap has + to be wider than one unit before there is anything in it to stand for. + """ + if isinstance(value, datetime.date): + return value + step if following - value > step else None + return (value + following) / 2.0 + + +def _label_cells(literals: set[Any]) -> list[Cell]: + """Every named label, and one standing for all the labels not named.""" + return [*sorted(literals, key=str), Special.OTHER] + + +def _rank_cells(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: + """Representative ranks, in one frame — counted from the front or the back. + + ``position(dim) == 0`` and ``position(dim) == -1`` are the same row when + the dimension has one member, so mixing the two frames is only decidable + where the extent is. A dimension that declares ``values:`` has one; a + dimension whose coordinates arrive from data does not, and neither does any + group a ``by=`` lookup makes, whatever the parent dimension declares. + + Within one frame the cells are its own mirror image. Counting from the + front, ranks run away from 0 and the open end is *after* the last position + named; counting from the back they run away from -1 and the open end is + *before* the first. Getting that backwards costs nothing while only ``==`` + and ``!=`` read — a representative on the wrong side still tells the named + positions apart — and gives wrong answers the moment an ordering does. + """ + positions = sorted(seen.positions) + extent = _extent_of(subject, schema) + if extent is not None: + positions = sorted({position + extent if position < 0 else position for position in positions}) + positions = [position for position in positions if 0 <= position < extent] + elif positions and positions[0] < 0 <= positions[-1]: + within = f' within each {subject.qualifier} group' if subject.qualifier else '' + msg = ( + f'{subject.name} is split at positions counted from both ends{within} ' + f'({", ".join(str(position) for position in sorted(seen.positions))}), and its extent is not declared, ' + f'so they are the same row on a short axis — declare `values:` for {subject.name}, or split at one end' + ) + raise Undecidable(msg) + if not positions: + return [0] + from_back = positions[-1] < 0 + cells: list[Cell] = [] + if from_back: + # The open end is before the earliest position named; there is nothing + # after -1, which is the last row by definition. + cells.append(positions[0] - 1) + elif positions[0] > 0: + cells.append(positions[0] - 1) + for index, position in enumerate(positions): + cells.append(position) + following = positions[index + 1] if index + 1 < len(positions) else None + if following is not None and following - position > 1: + cells.append(position + 1) + if from_back: + if positions[-1] < -1: + cells.append(positions[-1] + 1) + else: + beyond = positions[-1] + 1 + if extent is None or beyond < extent: + cells.append(beyond) + return cells + + +def _extent_of(subject: Subject, schema: Model) -> int | None: + """How many members the axis has, where the file says. ``by=`` never does.""" + if subject.qualifier is not None: + return None + block = schema.dimensions.get(subject.name) + if block is None or block.values is None: + return None + return len(block.values) + + +def _cells(domains: dict[Subject, list[Cell]]) -> Iterator[dict[Subject, Cell]]: + subjects = list(domains) + for combination in itertools.product(*(domains[subject] for subject in subjects)): + yield dict(zip(subjects, combination, strict=True)) + + +def _witness(cell: dict[Subject, Cell]) -> Witness: + return {str(subject): _shown(subject, value) for subject, value in cell.items()} + + +def _shown(subject: Subject, value: Cell) -> str: + if subject.kind == 'rank': + return f'{value}' + if subject.kind == 'lookup_pair': + return 'equal' if value else 'different' + if isinstance(value, Special): + return {Special.NULL: 'absent', Special.OTHER: 'anything else'}.get(value, value.value) + if isinstance(value, bool): + return 'true' if value else 'false' + return f'{value!r}' + + +# --------------------------------------------------------------------------- +# evaluating a mask on one cell +# --------------------------------------------------------------------------- + + +def _evaluate(node: WhereNode | None, cell: dict[Subject, Cell], extents: dict[Subject, int]) -> bool: + """Is *node* true in this cell? An absent mask is true everywhere.""" + if node is None: + return True + match node: + case BooleanLiteralNode(value=value): + return value + case NotNode(operand=operand): + return not _evaluate(operand, cell, extents) + case AndNode(left=left, right=right): + return _evaluate(left, cell, extents) and _evaluate(right, cell, extents) + case OrNode(left=left, right=right): + return _evaluate(left, cell, extents) or _evaluate(right, cell, extents) + case _: + return _atom(node, cell, extents) + + +def _atom(node: WhereNode, cell: dict[Subject, Cell], extents: dict[Subject, int]) -> bool: + subject = _subject_of(node) + assert subject is not None + value = cell[subject] + match node: + case ParameterDefinedNode() | LookupDefinedNode(): + # What `defined` means is the declaration's to say: a bool is its + # own answer, and a number has to be finite as well. + if isinstance(value, bool): + return value + return value not in (Special.NULL, Special.POS_INF, Special.NEG_INF) + case VariableDefinedNode(): + return bool(value) + case LookupPairComparisonNode(op=op): + return bool(value) if op == '==' else not value + case DimensionPositionNode(op=op, position=position): + extent = extents.get(subject) + if extent is not None and position < 0: + position += extent + return _compare(value, op, position) + case ParameterComparisonNode(op=op, value=literal) | LookupComparisonNode(op=op, value=literal): + # A null compares false, whatever the comparator. + if value is Special.NULL: + return False + return _compare(value, op, literal) + case DimensionComparisonNode(op=op, value=literal): + return _compare(value, op, literal) + case _: + msg = f'{type(node).__name__} is not an atom this procedure knows' + raise Undecidable(msg) + + +def _compare(value: Cell, op: PredicateOperator, literal: Any) -> bool: + """One atom's truth in one cell. Both sides are already this cell's frame.""" + if isinstance(value, Special): + if value is Special.OTHER: + # A label none of the masks names, so it matches none of them and + # sorts nowhere — an ordering against it is not decided here. + if op in ('==', '!='): + return op == '!=' + msg = f'an unnamed label ordered with {op!r}' + raise Undecidable(msg) + magnitude = math.inf if value is Special.POS_INF else -math.inf + return _numeric_compare(magnitude, op, float(literal)) + if isinstance(value, int | float) and isinstance(literal, int | float) and not isinstance(value, bool): + return _numeric_compare(float(value), op, float(literal)) + if type(value) is not type(literal) and not isinstance(value, type(literal)): + # Different types cannot be equal, and are not ordered against each + # other — which resolution has already refused, so this is the + # date-against-date case reached with one side a representative. + if op in ('==', '!='): + return op == '!=' + msg = f'{value!r} ordered against {literal!r}' + raise Undecidable(msg) + return _numeric_compare(value, op, literal) + + +def _numeric_compare(left: Any, op: PredicateOperator, right: Any) -> bool: + match op: + case '==': + return bool(left == right) + case '!=': + return bool(left != right) + case '<': + return bool(left < right) + case '<=': + return bool(left <= right) + case '>': + return bool(left > right) + case '>=': + return bool(left >= right) diff --git a/tests/test_partition.py b/tests/test_partition.py new file mode 100644 index 00000000..8633407f --- /dev/null +++ b/tests/test_partition.py @@ -0,0 +1,307 @@ +# SPDX-FileCopyrightText: math-spec Contributors +# +# SPDX-License-Identifier: MIT + +"""What the partition check proves, what it refuses, and what it will not decide. + +The three outcomes are the point: a case that lands in ``UNDECIDED`` is refused +by a caller exactly as a violation is, so a test that asserts ``not ok`` has not +said which of the two happened. Every test here names the status. +""" + +from __future__ import annotations + +import itertools +import random +from typing import TYPE_CHECKING, Any, ClassVar + +import pytest + +from math_spec.partition import Case, Special, Status, Subject, _evaluate, check_partition +from math_spec.resolution import Namespace, where_of +from math_spec.validation import load_model +from math_spec.where_parser import AndNode, NotNode, OrNode + +if TYPE_CHECKING: + from math_spec.model import Model + +#: A storage model with the two axes the argument turns on: `snapshot` gets its +#: coordinates from data, `storage` declares its own, so only the second has an +#: extent known before the data arrives. +STORAGE: dict[str, Any] = { + 'dimensions': { + 'snapshot': {'dtype': 'int'}, + 'storage': {'values': ['battery', 'reservoir', 'h2']}, + 'period': {'dtype': 'int', 'values': [2030, 2040]}, + }, + 'lookups': {'period_of': {'over': 'snapshot', 'into': 'period'}}, + 'parameters': { + 'cyclic': {'dims': ['storage'], 'dtype': 'bool'}, + 'kind': {'dims': ['storage'], 'dtype': 'str'}, + 'soc_initial': {'dims': ['storage']}, + 'capacity': {'dims': ['storage']}, + }, + 'variables': {'soc': {'foreach': ['snapshot', 'storage']}}, + 'constraints': {'balance': {'foreach': ['snapshot', 'storage'], 'expression': 'soc == 1'}}, +} + + +@pytest.fixture(scope='module') +def schema() -> Model: + return load_model(STORAGE) + + +def check(schema: Model, where: str | None, cases: dict[str, str]): + """Resolve the masks against *schema*, then decide.""" + namespace = Namespace.of(schema) + return check_partition( + where_of(where, namespace, 'the group'), + [Case(name, _mask(when, namespace, name)) for name, when in cases.items()], + schema, + ) + + +def _mask(text: str, namespace: Namespace, name: str): + mask = where_of(text, namespace, f"case '{name}'") + assert mask is not None + return mask + + +class TestProves: + def test_the_storage_split_from_the_issue(self, schema: Model): + """Two atoms, four regions, and the masks are exact complements. + + Spelled as the issue spells it, less `cyclic_state_of_charge == True`, + which is a load error: a bool's bare name *is* its value. + """ + verdict = check( + schema, + None, + { + 'first_ts': 'not cyclic and position(snapshot) == 0', + 'all_other_ts': '(not cyclic and position(snapshot) != 0) or cyclic', + }, + ) + assert verdict.status is Status.PARTITION + + def test_a_written_complement(self, schema: Model): + """The shape an `otherwise:` case would have saved restating.""" + verdict = check( + schema, + None, + {'first': 'position(snapshot) == 0', 'rest': 'not (position(snapshot) == 0)'}, + ) + assert verdict.status is Status.PARTITION + + def test_a_category_split_closed_by_the_where(self, schema: Model): + """Equality against distinct labels is exclusive — the theory step. + + Read propositionally these two atoms are independent, which invents a + region where a storage is both a battery and hydrogen and reports an + overlap no data can produce. + """ + verdict = check( + schema, + "kind == 'battery' or kind == 'h2'", + {'battery': "kind == 'battery'", 'hydrogen': "kind == 'h2'"}, + ) + assert verdict.status is Status.PARTITION + + def test_overlap_outside_the_where_is_not_an_overlap(self, schema: Model): + """The conditioning, in the direction that admits rather than refuses.""" + cases = { + 'cyclic': 'cyclic', + 'from_initial': 'soc_initial', + 'neither': 'not cyclic and not soc_initial', + } + assert check(schema, 'not (cyclic and soc_initial)', cases).status is Status.PARTITION + assert check(schema, None, cases).status is Status.VIOLATED + + def test_three_ways_where_the_extent_is_declared(self, schema: Model): + """`storage` declares `values:`, so 0 and -1 are provably different rows.""" + verdict = check( + schema, + None, + { + 'first': 'position(storage) == 0', + 'last': 'position(storage) == -1', + 'middle': 'position(storage) != 0 and position(storage) != -1', + }, + ) + assert verdict.status is Status.PARTITION + + def test_an_ordering_on_a_position(self, schema: Model): + """`position()` makes the comparison one between integers (#32). + + Every rank is either 0 or greater than 0, whatever order the + coordinates arrive in — which is the whole point of putting the + conversion on the left rather than naming the coordinate at a position. + """ + verdict = check(schema, None, {'first': 'position(snapshot) == 0', 'rest': 'position(snapshot) > 0'}) + assert verdict.status is Status.PARTITION + + def test_an_ordering_counted_from_the_back(self, schema: Model): + """The mirrored frame: ranks run away from -1, and nothing follows it.""" + verdict = check(schema, None, {'last': 'position(snapshot) == -1', 'rest': 'position(snapshot) < -1'}) + assert verdict.status is Status.PARTITION + + def test_a_band_counted_from_the_back(self, schema: Model): + verdict = check( + schema, + None, + { + 'final_two': 'position(snapshot) >= -2', + 'earlier': 'position(snapshot) < -2', + }, + ) + assert verdict.status is Status.PARTITION + + def test_numeric_bands(self, schema: Model): + verdict = check( + schema, + 'capacity > 0', + {'small': 'capacity <= 10', 'large': 'capacity > 10'}, + ) + assert verdict.status is Status.PARTITION + + +class TestRefuses: + def test_an_overlap_names_both_cases_and_a_witness(self, schema: Model): + verdict = check(schema, None, {'cyclic': 'cyclic', 'battery': "kind == 'battery'"}) + assert verdict.status is Status.VIOLATED + assert verdict.overlaps[0].cases == ('cyclic', 'battery') + assert 'cyclic is true' in verdict.message() + + def test_a_gap_is_a_row_with_no_expression(self, schema: Model): + verdict = check(schema, None, {'first': 'position(snapshot) == 0'}) + assert verdict.status is Status.VIOLATED + assert verdict.gaps + assert 'no case claims the row' in verdict.message() + + def test_a_case_the_where_excludes_is_dead(self, schema: Model): + verdict = check(schema, 'not cyclic', {'cyclic': 'cyclic', 'rest': 'not cyclic'}) + assert verdict.status is Status.VIOLATED + assert verdict.dead == ('cyclic',) + + def test_defined_is_not_non_zero(self, schema: Model): + """A bare name and `!= 0` are different questions, so these leave a gap.""" + verdict = check(schema, None, {'has_initial': 'soc_initial', 'zero': 'soc_initial == 0'}) + assert verdict.status is Status.VIOLATED + + +class TestWillNotDecide: + def test_both_ends_of_a_data_bound_axis(self, schema: Model): + """The one that matters: first/last on `snapshot` is a partition unless + the horizon has a single member, and nothing in the file rules that out. + """ + verdict = check( + schema, + None, + { + 'first': 'position(snapshot) == 0', + 'last': 'position(snapshot) == -1', + 'middle': 'position(snapshot) != 0 and position(snapshot) != -1', + }, + ) + assert verdict.status is Status.UNDECIDED + assert 'declare `values:`' in verdict.message() + + def test_a_group_never_has_a_declared_extent(self, schema: Model): + """`by=` counts within each group, and no declaration sizes those.""" + verdict = check( + schema, + None, + { + 'first': 'position(snapshot, by=period_of) == 0', + 'last': 'position(snapshot, by=period_of) == -1', + }, + ) + assert verdict.status is Status.UNDECIDED + + +class TestSoundness: + """A proved partition must hold on a grid finer than the cells it reasoned on. + + The claim the check rests on is that its regions cover every value a + subject can take, so "no witness among the cells" means "no witness". This + walks a concrete grid — several points inside single cells, both + infinities, an absent value, labels the masks never name — and asserts that + anything :attr:`Status.PARTITION` claims survives it. + + What it does not test is the reading of an individual atom: ground truth + here evaluates through the same ``_evaluate`` the checker uses, so a + misread atom would agree with itself. That is what `TestProves` and + `TestRefuses` pin, one atom at a time. + """ + + ATOMS: ClassVar[tuple[str, ...]] = ( + 'capacity', + 'capacity > 0', + 'capacity <= 10', + 'capacity == 0', + 'cyclic', + 'kind', + "kind == 'battery'", + "kind != 'h2'", + 'position(storage) == 0', + 'position(storage) != 0', + 'position(storage) == -1', + 'position(storage) > 0', + ) + + #: Finer than the cells: two points inside bands the masks cannot tell + #: apart, both infinities, absence, and labels no mask names. + GRID: ClassVar[dict[str, list[Any]]] = { + 'capacity': [Special.NULL, Special.NEG_INF, Special.POS_INF, -5.0, -0.5, 0.0, 0.5, 9.5, 10.0, 10.5], + 'cyclic': [Special.NULL, True, False], + 'kind': [Special.NULL, 'battery', 'h2', 'coal', 'nuclear'], + 'storage': [0, 1, 2], + } + + def _mask(self, rng: random.Random, atoms: list[Any], depth: int = 0) -> Any: + if depth >= 2 or rng.random() < 0.45: + atom = rng.choice(atoms) + return NotNode(atom) if rng.random() < 0.25 else atom + left = self._mask(rng, atoms, depth + 1) + right = self._mask(rng, atoms, depth + 1) + node = AndNode(left, right) if rng.random() < 0.5 else OrNode(left, right) + return NotNode(node) if rng.random() < 0.15 else node + + @pytest.mark.parametrize('seed', [1, 7]) + def test_a_proved_partition_holds_on_a_finer_grid(self, schema: Model, seed: int): + namespace = Namespace.of(schema) + atoms = [where_of(text, namespace, 'a probe') for text in self.ATOMS] + subjects = { + 'capacity': Subject('param', 'capacity'), + 'cyclic': Subject('param', 'cyclic'), + 'kind': Subject('param', 'kind'), + 'storage': Subject('rank', 'storage'), + } + extents = {subjects['storage']: 3} + grid = [ + {subjects[name]: value for name, value in zip(self.GRID, combination, strict=True)} + for combination in itertools.product(*self.GRID.values()) + ] + + rng = random.Random(seed) + proved = 0 + for _ in range(300): + split = self._mask(rng, atoms) + cases = [Case('a', split), Case('b', NotNode(split))] + if rng.random() < 0.5: + inner = self._mask(rng, atoms) + cases = [ + Case('a', AndNode(split, inner)), + Case('b', AndNode(split, NotNode(inner))), + Case('c', NotNode(split)), + ] + where = self._mask(rng, atoms) if rng.random() < 0.4 else None + if check_partition(where, cases, schema).status is not Status.PARTITION: + continue + proved += 1 + for point in grid: + if where is not None and not _evaluate(where, point, extents): + continue + claims = sum(1 for case in cases if _evaluate(case.when, point, extents)) + assert claims == 1, f'{claims} cases claim {point} — the cells hid a witness' + assert proved > 50, f'only {proved} partitions proved; the fuzz is not exercising the check' From 68788715795988f4b0e33dec338c61c797fc01de Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 22 Aug 2026 14:48:00 +0000 Subject: [PATCH 2/3] refactor: read dtypes off the namespace, and cut what was derivable MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `_dtype_of` re-derived what `Namespace.dtypes` already builds, and got a worse answer: it handled parameters and dimensions and returned None for every lookup, so an ordering on one — `period_of < 2040`, with `period` declared `dtype: int` — was refused as "has dtype None". Namespace covers lookups, including the non-obvious part that a targeted lookup takes its target dimension's dtype, so a natural multi-period split is now decided rather than refused. The dtype tuple also listed 'date', which is not a declarable dtype. `_Observed` is gone. `bare` was never read, `ordered` never outlived the node that set it, and `literals`/`positions` were never both populated for one subject — the tag was already `Subject.kind`, so a set per subject says it. `_Frame` replaces threading `domains` and `extents` separately, and memoises each atom's subject. `_subject_of` is a pure function of the node that allocates a fresh `Subject`, and `_atom` was calling it once per atom per cell: 972k calls in the fuzz. The nodes are `@dataclass(eq=True)` and so unhashable, hence the `id(node)` key. Witnesses are now built only while there is room for them — the verdict carries four, and a wide `where` over narrow cases would otherwise render one per uncovered cell and discard all but those. An unresolved node reaching `_subject_of` is now an AssertionError, as in `dimensions.py` and the typesetter. It is a caller that skipped `resolve_where`, not a model to refuse, and routing it to UNDECIDED put a message with no rewrite in front of a model author. Smaller: the two `except Undecidable` arms are one, `Gap` carried nothing a witness did not, the rank-cell frames share their head, and the prose loses what it said twice. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01ADtfZf4V6W9XcLRSwSgHzE --- src/math_spec/partition.py | 278 ++++++++++++++++--------------------- tests/test_partition.py | 25 ++-- 2 files changed, 131 insertions(+), 172 deletions(-) diff --git a/src/math_spec/partition.py b/src/math_spec/partition.py index a5e838e3..847165eb 100644 --- a/src/math_spec/partition.py +++ b/src/math_spec/partition.py @@ -25,8 +25,6 @@ would refuse them; a ``where`` wider than the cases cover is a real gap that a "the rows are whatever the cases claim" reading could not even express. -## How it decides - Every atom in the where-grammar talks about exactly one **subject** — a parameter, a dimension's coordinates, a dimension's *rank*, a lookup, a pair of lookups. Atoms with different subjects are independent; atoms sharing one are @@ -36,21 +34,10 @@ So each subject is split into **cells** — finitely many regions its value can sit in, chosen so that every atom over that subject is constant on each cell. -The cells of all subjects are multiplied out, and each masks is evaluated on -each cell. A cell where two cases are true is a witness for overlap; a cell -inside ``where`` where none is, a witness for a gap. Because the cells cover -every value the subject can take, "no witness" is a proof and not a sample. - -## Three outcomes, and why the third is not optional - -:attr:`Status.PARTITION`, :attr:`Status.VIOLATED` and -:attr:`Status.UNDECIDED`. Undecided is *refused* by the caller, never assumed: -a checker that guesses in the cases it cannot decide buys nothing over no -checker at all. What lands there is named in :class:`Verdict.reason` along with -the rewrite — the common one being two ``position()`` splits counted from -opposite ends of a dimension whose extent only data knows, where ``0`` and -``-1`` are the same row on a one-member axis and the split is a partition -everywhere else. +The cells of all subjects are multiplied out and each mask is evaluated on each +cell. A cell where two cases are true is a witness for overlap; a cell inside +``where`` where none is, a witness for a gap. Because the cells cover every +value the subject can take, "no witness" is a proof and not a sample. Independence between subjects is an **over**-approximation: the product of cells contains worlds the data may never produce, so a spurious world can only @@ -68,10 +55,11 @@ import datetime import itertools import math -from dataclasses import dataclass, field +from dataclasses import dataclass from enum import Enum -from typing import TYPE_CHECKING, Any, Literal +from typing import TYPE_CHECKING, Any, Literal, cast +from math_spec.resolution import Namespace from math_spec.where_parser import ( AndNode, BooleanLiteralNode, @@ -88,7 +76,7 @@ ) if TYPE_CHECKING: - from collections.abc import Iterable, Iterator + from collections.abc import Iterable, Iterator, Mapping from math_spec.model import Model from math_spec.where_parser import PredicateOperator, WhereNode @@ -98,9 +86,17 @@ #: a group that blows this is telling you it is several constraints. CELL_BUDGET = 8192 +#: The dtypes an ordering is decided against. Everything else compares only +#: with == and !=, which need no order on the values. +_ORDERED_DTYPES = ('float', 'int', 'datetime') + class Status(Enum): - """What the check established. :attr:`UNDECIDED` is a refusal, not a pass.""" + """What the check established. + + :attr:`UNDECIDED` is *refused* by the caller exactly as :attr:`VIOLATED` is: + a checker that guesses where it cannot decide buys nothing over no checker. + """ PARTITION = 'partition' VIOLATED = 'violated' @@ -173,18 +169,11 @@ class Overlap: witness: Witness -@dataclass(frozen=True) -class Gap: - """A row the ``where`` builds that no case gives an expression to.""" - - witness: Witness - - @dataclass(frozen=True) class Verdict: status: Status overlaps: tuple[Overlap, ...] = () - gaps: tuple[Gap, ...] = () + gaps: tuple[Witness, ...] = () dead: tuple[str, ...] = () reason: str | None = None @@ -202,7 +191,7 @@ def message(self) -> str: for overlap in self.overlaps: first, second = overlap.cases parts.append(f"cases '{first}' and '{second}' both claim a row where {_render(overlap.witness)}") - parts.extend(f'no case claims the row where {_render(gap.witness)}' for gap in self.gaps) + parts.extend(f'no case claims the row where {_render(gap)}' for gap in self.gaps) parts.extend(f"case '{name}' builds no rows" for name in self.dead) return '; '.join(parts) @@ -215,10 +204,7 @@ def _render(witness: Witness) -> str: class Case: """One case of a group: a mask, and the name the LaTeX prints beside it. - Every case carries one. An open "everything the others left" case would - save restating a long mask, but nothing else — ``not (x)`` says the same - thing, and a mask edited without its restated negation is a gap or an - overlap here rather than a silent change of model. + Every case carries a mask; ``not (x)`` is how the complement is written. """ name: str @@ -244,48 +230,45 @@ def check_partition(where: WhereNode | None, cases: Iterable[Case], schema: Mode The verdict. :attr:`Status.UNDECIDED` is a refusal — see the module docstring. """ - cases = list(cases) - masks = [node for node in [where, *(case.when for case in cases)] if node is not None] try: - domains = _domains(masks, schema) + return _decide(where, list(cases), schema) except Undecidable as exc: return Verdict(Status.UNDECIDED, reason=str(exc)) - # The cells of a rank subject are counted from the front wherever the - # extent is known, so the positions the atoms carry have to be read in that - # same frame — `position(dim) == -1` on a three-member axis is rank 2. - extents = { - subject: extent - for subject in domains - if subject.kind == 'rank' and (extent := _extent_of(subject, schema)) is not None - } - - size = math.prod(len(cells) for cells in domains.values()) if domains else 1 - if size > CELL_BUDGET: + +#: How many witnesses a verdict carries. The loop runs to the end whatever +#: happens — the dead-case check needs every hit — so this bounds the *rendering* +#: rather than the search, and a mask with a wide `where` and narrow cases would +#: otherwise render one witness per uncovered cell and throw all but these away. +_WITNESSES = 4 + + +def _decide(where: WhereNode | None, cases: list[Case], schema: Model) -> Verdict: + frame = _Frame.of([where, *(case.when for case in cases)], schema) + if frame.size > CELL_BUDGET: return Verdict( Status.UNDECIDED, - reason=f'{size} regions to check exceeds the budget of {CELL_BUDGET} — split this into named constraints', + reason=f'{frame.size} regions to check exceeds the budget of {CELL_BUDGET} — ' + f'split this into named constraints', ) overlaps: list[Overlap] = [] - gaps: list[Gap] = [] + gaps: list[Witness] = [] live: set[str] = set() - try: - for cell in _cells(domains): - if not _evaluate(where, cell, extents): - continue - hits = [case.name for case in cases if _evaluate(case.when, cell, extents)] - if len(hits) > 1: - overlaps.append(Overlap((hits[0], hits[1]), _witness(cell))) - elif not hits: - gaps.append(Gap(_witness(cell))) - live.update(hits) - except Undecidable as exc: - return Verdict(Status.UNDECIDED, reason=str(exc)) + for cell in frame.cells(): + if not _evaluate(where, cell, frame): + continue + hits = [case.name for case in cases if _evaluate(case.when, cell, frame)] + if len(hits) > 1: + if len(overlaps) < _WITNESSES: + overlaps.append(Overlap((hits[0], hits[1]), frame.witness(cell))) + elif not hits and len(gaps) < _WITNESSES: + gaps.append(frame.witness(cell)) + live.update(hits) dead = tuple(case.name for case in cases if case.name not in live) if overlaps or gaps or dead: - return Verdict(Status.VIOLATED, tuple(overlaps[:4]), tuple(gaps[:4]), dead) + return Verdict(Status.VIOLATED, tuple(overlaps), tuple(gaps), dead) return Verdict(Status.PARTITION) @@ -294,22 +277,48 @@ def check_partition(where: WhereNode | None, cases: Iterable[Case], schema: Mode # --------------------------------------------------------------------------- -@dataclass -class _Observed: - """What the masks say about one subject, before it is cut into cells.""" +@dataclass(frozen=True) +class _Frame: + """The cells to check, and what reading an atom on one of them needs. - literals: set[Any] = field(default_factory=set) - positions: set[int] = field(default_factory=set) - bare: bool = False - ordered: bool = False + ``subjects`` is keyed by ``id(node)`` because the where-AST nodes are + ``@dataclass`` with ``eq=True`` and so unhashable. It is a memo of a pure + function: without it every atom re-derives and re-allocates its subject once + per cell, which is the hot path here. + """ + domains: dict[Subject, list[Cell]] + #: Rank cells are counted from the front wherever the extent is known, so + #: the positions the atoms carry have to be read in that same frame — + #: `position(dim) == -1` on a three-member axis is rank 2. + extents: dict[Subject, int] + subjects: dict[int, Subject] + + @classmethod + def of(cls, masks: Iterable[WhereNode | None], schema: Model) -> _Frame: + dtypes = Namespace.of(schema).dtypes + values: dict[Subject, set[Any]] = {} + subjects: dict[int, Subject] = {} + for mask in masks: + for node in _walk(mask): + if (subject := _subject_of(node)) is None: + continue + subjects[id(node)] = subject + _observe(node, subject, values.setdefault(subject, set()), dtypes) + extents = {s: e for s in values if s.kind == 'rank' and (e := _extent_of(s, schema)) is not None} + domains = {s: _cells_for(s, seen, dtypes, extents.get(s)) for s, seen in values.items()} + return cls(domains, extents, subjects) -def _domains(masks: Iterable[WhereNode], schema: Model) -> dict[Subject, list[Cell]]: - observed: dict[Subject, _Observed] = {} - for mask in masks: - for node in _walk(mask): - _observe(node, observed, schema) - return {subject: _cells_for(subject, seen, schema) for subject, seen in observed.items()} + @property + def size(self) -> int: + return math.prod(len(cells) for cells in self.domains.values()) + + def cells(self) -> Iterator[dict[Subject, Cell]]: + for combination in itertools.product(*self.domains.values()): + yield dict(zip(self.domains, combination, strict=True)) + + def witness(self, cell: dict[Subject, Cell]) -> Witness: + return {str(subject): _shown(subject, value) for subject, value in cell.items()} def _walk(node: WhereNode | None) -> Iterator[WhereNode]: @@ -325,30 +334,24 @@ def _walk(node: WhereNode | None) -> Iterator[WhereNode]: yield node -def _observe(node: WhereNode, observed: dict[Subject, _Observed], schema: Model) -> None: - subject = _subject_of(node) - if subject is None: - return - seen = observed.setdefault(subject, _Observed()) - if isinstance(node, ParameterDefinedNode | VariableDefinedNode | LookupDefinedNode): - seen.bare = True - elif isinstance(node, DimensionPositionNode): +def _observe(node: WhereNode, subject: Subject, values: set[Any], dtypes: Mapping[str, str]) -> None: + """Record what *node* says about its subject: a position, or a literal.""" + if isinstance(node, DimensionPositionNode): # Every comparator reads here: `position()` converts the dimension to # an integer, so an ordering is an ordering of integers (#32). - seen.positions.add(node.position) + values.add(node.position) elif isinstance(node, LookupPairComparisonNode): if node.op not in ('==', '!='): msg = f'{subject} compared with {node.op!r}; two lookups compare only with == or !=' raise Undecidable(msg) elif isinstance(node, ParameterComparisonNode | DimensionComparisonNode | LookupComparisonNode): - if node.op not in ('==', '!='): - seen.ordered = True - seen.literals.add(node.value) - if seen.ordered and isinstance(node, ParameterComparisonNode | DimensionComparisonNode | LookupComparisonNode): - dtype = _dtype_of(subject, schema) - if dtype not in ('float', 'int', 'datetime', 'date'): - msg = f'{subject} has dtype {dtype!r} and is ordered with {node.op!r}; only == and != are decided here' + if node.op not in ('==', '!=') and dtypes.get(subject.name) not in _ORDERED_DTYPES: + msg = ( + f'{subject} has dtype {dtypes.get(subject.name)!r} and is ordered with ' + f'{node.op!r}; only == and != are decided here' + ) raise Undecidable(msg) + values.add(node.value) def _subject_of(node: WhereNode) -> Subject | None: @@ -368,34 +371,24 @@ def _subject_of(node: WhereNode) -> Subject | None: case LookupPairComparisonNode(name=name, other=other): return Subject('lookup_pair', name, other) case _: - msg = f'{type(node).__name__} is not an atom this procedure knows' - raise Undecidable(msg) - + # As in `dimensions.py` and the typesetter: an unresolved node here + # is a caller that skipped `resolve_where`, not a model to refuse. + msg = f'{type(node).__name__} reached the partition check unresolved.' + raise AssertionError(msg) -def _dtype_of(subject: Subject, schema: Model) -> str | None: - if subject.kind == 'param': - block = schema.parameters.get(subject.name) - return None if block is None else block.dtype - if subject.kind == 'dim': - block = schema.dimensions.get(subject.name) - return None if block is None else block.dtype - return None - -def _cells_for(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: +def _cells_for(subject: Subject, values: set[Any], dtypes: Mapping[str, str], extent: int | None) -> list[Cell]: if subject.kind == 'rank': - return _rank_cells(subject, seen, schema) - if subject.kind == 'lookup_pair': + return _rank_cells(subject, cast('set[int]', values), extent) + if subject.kind in ('lookup_pair', 'variable'): return [True, False] - if subject.kind == 'variable': - return [True, False] - dtype = _dtype_of(subject, schema) + dtype = dtypes.get(subject.name) if dtype == 'bool': - if seen.literals: + if values: msg = f'{subject} has dtype bool and is compared to a literal' raise Undecidable(msg) return [Special.NULL, True, False] - numeric = _numeric(dtype, seen.literals) + numeric = _numeric(dtype, values) cells: list[Cell] = [] # A dimension's coordinates are its own index, so there is no null among # them; everything else may be absent, and absence is a region of its own @@ -406,7 +399,7 @@ def _cells_for(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: # `defined` excludes an infinity, so it needs a region where every # comparison still reads normally but the bare name is false. cells.extend([Special.NEG_INF, Special.POS_INF]) - cells.extend(_ordered_cells(seen.literals) if numeric or _dated(seen.literals) else _label_cells(seen.literals)) + cells.extend(_ordered_cells(values) if numeric or _dated(values) else _label_cells(values)) return cells @@ -422,13 +415,7 @@ def _dated(literals: set[Any]) -> bool: def _ordered_cells(literals: set[Any]) -> list[Cell]: - """Each literal, and one representative of the gap on either side of it. - - The representatives stand for every value in their gap, which they may - because each atom over this subject compares against one of the literals — - so two values with no literal between them are indistinguishable to every - mask here. - """ + """Each literal, and one representative of the gap on either side of it.""" if not literals: return [0.0] values = sorted(literals) @@ -471,7 +458,7 @@ def _label_cells(literals: set[Any]) -> list[Cell]: return [*sorted(literals, key=str), Special.OTHER] -def _rank_cells(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: +def _rank_cells(subject: Subject, positions_seen: set[int], extent: int | None) -> list[Cell]: """Representative ranks, in one frame — counted from the front or the back. ``position(dim) == 0`` and ``position(dim) == -1`` are the same row when @@ -480,15 +467,11 @@ def _rank_cells(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: dimension whose coordinates arrive from data does not, and neither does any group a ``by=`` lookup makes, whatever the parent dimension declares. - Within one frame the cells are its own mirror image. Counting from the - front, ranks run away from 0 and the open end is *after* the last position - named; counting from the back they run away from -1 and the open end is - *before* the first. Getting that backwards costs nothing while only ``==`` - and ``!=`` read — a representative on the wrong side still tells the named - positions apart — and gives wrong answers the moment an ordering does. + Within one frame the cells are its own mirror image: counting from the + front the open end is *after* the last position named, counting from the + back it is *before* the first, since nothing follows -1. """ - positions = sorted(seen.positions) - extent = _extent_of(subject, schema) + positions = sorted(positions_seen) if extent is not None: positions = sorted({position + extent if position < 0 else position for position in positions}) positions = [position for position in positions if 0 <= position < extent] @@ -496,7 +479,7 @@ def _rank_cells(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: within = f' within each {subject.qualifier} group' if subject.qualifier else '' msg = ( f'{subject.name} is split at positions counted from both ends{within} ' - f'({", ".join(str(position) for position in sorted(seen.positions))}), and its extent is not declared, ' + f'({", ".join(str(position) for position in positions)}), and its extent is not declared, ' f'so they are the same row on a short axis — declare `values:` for {subject.name}, or split at one end' ) raise Undecidable(msg) @@ -504,11 +487,7 @@ def _rank_cells(subject: Subject, seen: _Observed, schema: Model) -> list[Cell]: return [0] from_back = positions[-1] < 0 cells: list[Cell] = [] - if from_back: - # The open end is before the earliest position named; there is nothing - # after -1, which is the last row by definition. - cells.append(positions[0] - 1) - elif positions[0] > 0: + if positions[0] != 0: cells.append(positions[0] - 1) for index, position in enumerate(positions): cells.append(position) @@ -535,19 +514,9 @@ def _extent_of(subject: Subject, schema: Model) -> int | None: return len(block.values) -def _cells(domains: dict[Subject, list[Cell]]) -> Iterator[dict[Subject, Cell]]: - subjects = list(domains) - for combination in itertools.product(*(domains[subject] for subject in subjects)): - yield dict(zip(subjects, combination, strict=True)) - - -def _witness(cell: dict[Subject, Cell]) -> Witness: - return {str(subject): _shown(subject, value) for subject, value in cell.items()} - - def _shown(subject: Subject, value: Cell) -> str: if subject.kind == 'rank': - return f'{value}' + return str(value) if subject.kind == 'lookup_pair': return 'equal' if value else 'different' if isinstance(value, Special): @@ -562,7 +531,7 @@ def _shown(subject: Subject, value: Cell) -> str: # --------------------------------------------------------------------------- -def _evaluate(node: WhereNode | None, cell: dict[Subject, Cell], extents: dict[Subject, int]) -> bool: +def _evaluate(node: WhereNode | None, cell: dict[Subject, Cell], frame: _Frame) -> bool: """Is *node* true in this cell? An absent mask is true everywhere.""" if node is None: return True @@ -570,18 +539,17 @@ def _evaluate(node: WhereNode | None, cell: dict[Subject, Cell], extents: dict[S case BooleanLiteralNode(value=value): return value case NotNode(operand=operand): - return not _evaluate(operand, cell, extents) + return not _evaluate(operand, cell, frame) case AndNode(left=left, right=right): - return _evaluate(left, cell, extents) and _evaluate(right, cell, extents) + return _evaluate(left, cell, frame) and _evaluate(right, cell, frame) case OrNode(left=left, right=right): - return _evaluate(left, cell, extents) or _evaluate(right, cell, extents) + return _evaluate(left, cell, frame) or _evaluate(right, cell, frame) case _: - return _atom(node, cell, extents) + return _atom(node, cell, frame) -def _atom(node: WhereNode, cell: dict[Subject, Cell], extents: dict[Subject, int]) -> bool: - subject = _subject_of(node) - assert subject is not None +def _atom(node: WhereNode, cell: dict[Subject, Cell], frame: _Frame) -> bool: + subject = frame.subjects[id(node)] value = cell[subject] match node: case ParameterDefinedNode() | LookupDefinedNode(): @@ -595,7 +563,7 @@ def _atom(node: WhereNode, cell: dict[Subject, Cell], extents: dict[Subject, int case LookupPairComparisonNode(op=op): return bool(value) if op == '==' else not value case DimensionPositionNode(op=op, position=position): - extent = extents.get(subject) + extent = frame.extents.get(subject) if extent is not None and position < 0: position += extent return _compare(value, op, position) diff --git a/tests/test_partition.py b/tests/test_partition.py index 8633407f..e65ddf9d 100644 --- a/tests/test_partition.py +++ b/tests/test_partition.py @@ -17,7 +17,7 @@ import pytest -from math_spec.partition import Case, Special, Status, Subject, _evaluate, check_partition +from math_spec.partition import Case, Special, Status, Subject, _evaluate, _Frame, check_partition from math_spec.resolution import Namespace, where_of from math_spec.validation import load_model from math_spec.where_parser import AndNode, NotNode, OrNode @@ -85,7 +85,6 @@ def test_the_storage_split_from_the_issue(self, schema: Model): assert verdict.status is Status.PARTITION def test_a_written_complement(self, schema: Model): - """The shape an `otherwise:` case would have saved restating.""" verdict = check( schema, None, @@ -94,12 +93,7 @@ def test_a_written_complement(self, schema: Model): assert verdict.status is Status.PARTITION def test_a_category_split_closed_by_the_where(self, schema: Model): - """Equality against distinct labels is exclusive — the theory step. - - Read propositionally these two atoms are independent, which invents a - region where a storage is both a battery and hydrogen and reports an - overlap no data can produce. - """ + """Equality against distinct labels is exclusive — the theory step.""" verdict = check( schema, "kind == 'battery' or kind == 'h2'", @@ -131,12 +125,7 @@ def test_three_ways_where_the_extent_is_declared(self, schema: Model): assert verdict.status is Status.PARTITION def test_an_ordering_on_a_position(self, schema: Model): - """`position()` makes the comparison one between integers (#32). - - Every rank is either 0 or greater than 0, whatever order the - coordinates arrive in — which is the whole point of putting the - conversion on the left rather than naming the coordinate at a position. - """ + """Every rank is either 0 or greater, whatever order the coordinates arrive in (#32).""" verdict = check(schema, None, {'first': 'position(snapshot) == 0', 'rest': 'position(snapshot) > 0'}) assert verdict.status is Status.PARTITION @@ -277,7 +266,6 @@ def test_a_proved_partition_holds_on_a_finer_grid(self, schema: Model, seed: int 'kind': Subject('param', 'kind'), 'storage': Subject('rank', 'storage'), } - extents = {subjects['storage']: 3} grid = [ {subjects[name]: value for name, value in zip(self.GRID, combination, strict=True)} for combination in itertools.product(*self.GRID.values()) @@ -299,9 +287,12 @@ def test_a_proved_partition_holds_on_a_finer_grid(self, schema: Model, seed: int if check_partition(where, cases, schema).status is not Status.PARTITION: continue proved += 1 + # The same frame the check built, so ground truth reads each atom + # the way it did — what differs is the grid, which is finer. + frame = _Frame.of([where, *(case.when for case in cases)], schema) for point in grid: - if where is not None and not _evaluate(where, point, extents): + if where is not None and not _evaluate(where, point, frame): continue - claims = sum(1 for case in cases if _evaluate(case.when, point, extents)) + claims = sum(1 for case in cases if _evaluate(case.when, point, frame)) assert claims == 1, f'{claims} cases claim {point} — the cells hid a witness' assert proved > 50, f'only {proved} partitions proved; the fuzz is not exercising the check' From 0a622c5f1c94ca8d91b5e85534ae5bd46f75f749 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 22 Aug 2026 19:52:31 +0000 Subject: [PATCH 3/3] refactor: cases belong to expressions, not constraints MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #2 moved: the cases go on a named expression rather than on the constraint that uses it. Three independent axes multiply into eight constraint cases and add into seven expression cases, and the inequality is written once instead of eight times — a change to it is then one edit rather than eight that nothing checks agree. It also answers the objection that opened #2 better than a constraint `cases:` did. The constraint keeps one name and one expression, so its dual is unambiguous by construction rather than by proof. `where` goes with it. An expression carries no mask: it is **total** over its frame or it is refused. Two expressions each masked would intersect in the constraint that used them — absence spreads and takes the row — so a constraint's row set would stop being readable at the constraint, which is what `diagnostics().omissions` exists to catch ("rows lost to a mask the constraint never mentions"). Nothing is conditioned here now, and the price is visible in the tests: with no mask to narrow the frame, the cases have to say what an absent capacity or an unnamed label gets. The per-case key is `when`, not `where`. A case selects which value a coordinate takes; it creates no absence and deletes no row, which is what `where` means everywhere else (rule 6). Under this design an expression has no `where` at all, so a `where:` here would be the only one on the block and would read as extent — precisely the wrong reading. Adds the three quantities #2 factors a PyPSA ramp limit into as a test, since they are the case the design is for. Not wired into the schema — `expressions:` accepts neither `foreach` nor `cases` yet, and that is the next change rather than this one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01ADtfZf4V6W9XcLRSwSgHzE --- src/math_spec/partition.py | 86 ++++++++++++++------------- tests/test_partition.py | 115 +++++++++++++++++++++++-------------- 2 files changed, 114 insertions(+), 87 deletions(-) diff --git a/src/math_spec/partition.py b/src/math_spec/partition.py index 847165eb..9f53ecde 100644 --- a/src/math_spec/partition.py +++ b/src/math_spec/partition.py @@ -2,28 +2,28 @@ # # SPDX-License-Identifier: MIT -"""Does a set of case masks partition a constraint's rows? Decided without data. +"""Do a named expression's cases partition its frame? Decided without data. -A constraint with ``cases:`` is one rule whose expression varies by region. It -is *one* constraint — one name, one row per coordinate, one dual — only if the -cases claim each row **exactly once**. That claim is decidable here, before any -data binds, which is rule 2 in a new position. +A named expression with ``cases:`` is one quantity whose value varies by +region — the regime a unit is in, which end of the horizon a row sits at. It is +*one* quantity, with one value per coordinate, only if the cases claim each +coordinate **exactly once**. That claim is decidable here, before any data +binds, which is rule 2 in a new position. -Two obligations, both conditioned on the constraint's own ``where`` (the rows -that exist at all), and both the same unsatisfiability question: +Three obligations, all the same unsatisfiability question: -* **disjoint** — ``where AND case_i AND case_j`` is unsatisfiable, for every pair -* **exhaustive** — ``where AND NOT (case_1 OR ... OR case_n)`` is unsatisfiable +* **disjoint** — ``case_i AND case_j`` is unsatisfiable, for every pair. Two + values at one coordinate is not a quantity. +* **exhaustive** — ``NOT (case_1 OR ... OR case_n)`` is unsatisfiable. An + expression is **total** over its ``foreach``: a gap would leave it undefined, + and rule 7 would spread that to every constraint referencing it, silently + deleting rows the constraint never masked. +* **no dead case** — ``case_i`` alone is satisfiable. A case that claims + nothing is a mistake rather than a no-op. -and one that falls out of the same machinery for free: - -* **no dead case** — ``where AND case_i`` unsatisfiable means that block builds - no rows, which is a mistake rather than a no-op. - -Conditioning matters in both directions. Two cases that overlap somewhere the -``where`` already excludes are *not* an ambiguity, and an unconditional check -would refuse them; a ``where`` wider than the cases cover is a real gap that a -"the rows are whatever the cases claim" reading could not even express. +Nothing is conditioned on a mask, because an expression carries none: it is +total or it is refused. That is what keeps a constraint's row set readable at +the constraint, which is the whole reason the cases sit here rather than there. Every atom in the where-grammar talks about exactly one **subject** — a parameter, a dimension's coordinates, a dimension's *rank*, a lookup, a pair of @@ -35,19 +35,18 @@ So each subject is split into **cells** — finitely many regions its value can sit in, chosen so that every atom over that subject is constant on each cell. The cells of all subjects are multiplied out and each mask is evaluated on each -cell. A cell where two cases are true is a witness for overlap; a cell inside -``where`` where none is, a witness for a gap. Because the cells cover every -value the subject can take, "no witness" is a proof and not a sample. +cell. A cell where two cases are true is a witness for overlap; a cell where +none is, a witness for a gap. Because the cells cover every value the subject +can take, "no witness" is a proof and not a sample. Independence between subjects is an **over**-approximation: the product of cells contains worlds the data may never produce, so a spurious world can only manufacture a witness, never hide one. Every outcome here is therefore -conservative — this refuses groups that would have been fine, and admits none -that would not. +conservative — this refuses case sets that would have been fine, and admits +none that would not. -Not wired into the schema: ``cases:`` is not a key the model accepts yet -(energy-models/math-spec#2), and which spelling it lands on does not change -anything below. +Not wired into the schema: ``cases:`` is not a key ``expressions:`` accepts +yet (energy-models/math-spec#2). This is the decision procedure only. """ from __future__ import annotations @@ -83,7 +82,7 @@ #: The product of every subject's cells is enumerated, so the bound is on the #: product rather than on any one subject. Real masks carry two to four atoms; -#: a group that blows this is telling you it is several constraints. +#: an expression that blows this is telling you it is several expressions. CELL_BUDGET = 8192 #: The dtypes an ordering is decided against. Everything else compares only @@ -163,7 +162,7 @@ class Undecidable(Exception): # noqa: N818 @dataclass(frozen=True) class Overlap: - """Two cases that can both claim one row.""" + """Two cases that can both claim one coordinate.""" cases: tuple[str, str] witness: Witness @@ -190,9 +189,9 @@ def message(self) -> str: parts = [] for overlap in self.overlaps: first, second = overlap.cases - parts.append(f"cases '{first}' and '{second}' both claim a row where {_render(overlap.witness)}") - parts.extend(f'no case claims the row where {_render(gap)}' for gap in self.gaps) - parts.extend(f"case '{name}' builds no rows" for name in self.dead) + parts.append(f"cases '{first}' and '{second}' both claim the value where {_render(overlap.witness)}") + parts.extend(f'no case claims the value where {_render(gap)}' for gap in self.gaps) + parts.extend(f"case '{name}' claims nothing" for name in self.dead) return '; '.join(parts) @@ -202,9 +201,12 @@ def _render(witness: Witness) -> str: @dataclass(frozen=True) class Case: - """One case of a group: a mask, and the name the LaTeX prints beside it. + """One case of an expression: its ``when``, and the name the LaTeX prints. - Every case carries a mask; ``not (x)`` is how the complement is written. + Every case carries a ``when``; ``NOT (x)`` is how the complement is + written. The key is not ``where`` because a case selects which value a + coordinate takes — it creates no absence and deletes no row, which is what + ``where`` means everywhere else (rule 6). """ name: str @@ -216,13 +218,11 @@ class Case: # --------------------------------------------------------------------------- -def check_partition(where: WhereNode | None, cases: Iterable[Case], schema: Model) -> Verdict: - """Decide whether *cases* partition the rows *where* builds. +def check_partition(cases: Iterable[Case], schema: Model) -> Verdict: + """Decide whether *cases* partition the expression's frame. Args: - where: The constraint's own mask — the rows that exist. ``None`` is - everything the ``foreach`` spans. - cases: The cases, in declaration order, each with its own mask. + cases: The cases, in declaration order, each with its own ``when``. schema: Read for dtypes, and for the declared ``values:`` that give a dimension a statically known extent. @@ -231,20 +231,20 @@ def check_partition(where: WhereNode | None, cases: Iterable[Case], schema: Mode docstring. """ try: - return _decide(where, list(cases), schema) + return _decide(list(cases), schema) except Undecidable as exc: return Verdict(Status.UNDECIDED, reason=str(exc)) #: How many witnesses a verdict carries. The loop runs to the end whatever #: happens — the dead-case check needs every hit — so this bounds the *rendering* -#: rather than the search, and a mask with a wide `where` and narrow cases would +#: rather than the search, and cases covering a thin slice of a wide frame would #: otherwise render one witness per uncovered cell and throw all but these away. _WITNESSES = 4 -def _decide(where: WhereNode | None, cases: list[Case], schema: Model) -> Verdict: - frame = _Frame.of([where, *(case.when for case in cases)], schema) +def _decide(cases: list[Case], schema: Model) -> Verdict: + frame = _Frame.of([case.when for case in cases], schema) if frame.size > CELL_BUDGET: return Verdict( Status.UNDECIDED, @@ -256,8 +256,6 @@ def _decide(where: WhereNode | None, cases: list[Case], schema: Model) -> Verdic gaps: list[Witness] = [] live: set[str] = set() for cell in frame.cells(): - if not _evaluate(where, cell, frame): - continue hits = [case.name for case in cases if _evaluate(case.when, cell, frame)] if len(hits) > 1: if len(overlaps) < _WITNESSES: diff --git a/tests/test_partition.py b/tests/test_partition.py index e65ddf9d..2b3975d6 100644 --- a/tests/test_partition.py +++ b/tests/test_partition.py @@ -37,6 +37,7 @@ 'lookups': {'period_of': {'over': 'snapshot', 'into': 'period'}}, 'parameters': { 'cyclic': {'dims': ['storage'], 'dtype': 'bool'}, + 'committable': {'dims': ['storage'], 'dtype': 'bool'}, 'kind': {'dims': ['storage'], 'dtype': 'str'}, 'soc_initial': {'dims': ['storage']}, 'capacity': {'dims': ['storage']}, @@ -51,14 +52,10 @@ def schema() -> Model: return load_model(STORAGE) -def check(schema: Model, where: str | None, cases: dict[str, str]): - """Resolve the masks against *schema*, then decide.""" +def check(schema: Model, cases: dict[str, str]): + """Resolve each case's `when` against *schema*, then decide.""" namespace = Namespace.of(schema) - return check_partition( - where_of(where, namespace, 'the group'), - [Case(name, _mask(when, namespace, name)) for name, when in cases.items()], - schema, - ) + return check_partition([Case(name, _mask(when, namespace, name)) for name, when in cases.items()], schema) def _mask(text: str, namespace: Namespace, name: str): @@ -76,7 +73,6 @@ def test_the_storage_split_from_the_issue(self, schema: Model): """ verdict = check( schema, - None, { 'first_ts': 'not cyclic and position(snapshot) == 0', 'all_other_ts': '(not cyclic and position(snapshot) != 0) or cyclic', @@ -87,35 +83,51 @@ def test_the_storage_split_from_the_issue(self, schema: Model): def test_a_written_complement(self, schema: Model): verdict = check( schema, - None, {'first': 'position(snapshot) == 0', 'rest': 'not (position(snapshot) == 0)'}, ) assert verdict.status is Status.PARTITION - def test_a_category_split_closed_by_the_where(self, schema: Model): - """Equality against distinct labels is exclusive — the theory step.""" + def test_a_category_split(self, schema: Model): + """Equality against distinct labels is exclusive — the theory step. + + Totality is what forces the third case: with no mask to narrow the + frame, a storage that is neither has to be given a value here. + """ verdict = check( schema, - "kind == 'battery' or kind == 'h2'", - {'battery': "kind == 'battery'", 'hydrogen': "kind == 'h2'"}, + { + 'battery': "kind == 'battery'", + 'hydrogen': "kind == 'h2'", + 'other': "not (kind == 'battery' or kind == 'h2')", + }, ) assert verdict.status is Status.PARTITION - def test_overlap_outside_the_where_is_not_an_overlap(self, schema: Model): - """The conditioning, in the direction that admits rather than refuses.""" - cases = { - 'cyclic': 'cyclic', - 'from_initial': 'soc_initial', - 'neither': 'not cyclic and not soc_initial', - } - assert check(schema, 'not (cyclic and soc_initial)', cases).status is Status.PARTITION - assert check(schema, None, cases).status is Status.VIOLATED + def test_the_cases_are_written_disjoint(self, schema: Model): + """Nothing conditions these, so the `NOT`s are the author's to write. + + There is no mask to exclude the region where both hold, which is the + price of an expression being total: the regimes have to be spelled + apart rather than narrowed from outside. + """ + assert ( + check( + schema, + { + 'cyclic': 'cyclic', + 'from_initial': 'not cyclic and soc_initial', + 'neither': 'not cyclic and not soc_initial', + }, + ).status + is Status.PARTITION + ) + overlapping = {'cyclic': 'cyclic', 'from_initial': 'soc_initial', 'neither': 'not cyclic and not soc_initial'} + assert check(schema, overlapping).status is Status.VIOLATED def test_three_ways_where_the_extent_is_declared(self, schema: Model): """`storage` declares `values:`, so 0 and -1 are provably different rows.""" verdict = check( schema, - None, { 'first': 'position(storage) == 0', 'last': 'position(storage) == -1', @@ -124,20 +136,38 @@ def test_three_ways_where_the_extent_is_declared(self, schema: Model): ) assert verdict.status is Status.PARTITION + def test_the_ramp_expressions_from_the_issue(self, schema: Model): + """The three quantities #2 factors a PyPSA ramp limit into. + + The point of putting cases here rather than on the constraint: three + independent axes multiply into eight constraint cases and add into + seven expression cases, and the inequality is written once instead of + eight times. + """ + for cases in ( + {'boundary': 'position(snapshot) == 0', 'interior': 'position(snapshot) > 0'}, + {'modular': 'cyclic', 'whole': 'not cyclic'}, + { + 'always_on': 'not committable', + 'boundary': 'committable and position(snapshot) == 0', + 'interior': 'committable and position(snapshot) > 0', + }, + ): + assert check(schema, cases).status is Status.PARTITION + def test_an_ordering_on_a_position(self, schema: Model): """Every rank is either 0 or greater, whatever order the coordinates arrive in (#32).""" - verdict = check(schema, None, {'first': 'position(snapshot) == 0', 'rest': 'position(snapshot) > 0'}) + verdict = check(schema, {'first': 'position(snapshot) == 0', 'rest': 'position(snapshot) > 0'}) assert verdict.status is Status.PARTITION def test_an_ordering_counted_from_the_back(self, schema: Model): """The mirrored frame: ranks run away from -1, and nothing follows it.""" - verdict = check(schema, None, {'last': 'position(snapshot) == -1', 'rest': 'position(snapshot) < -1'}) + verdict = check(schema, {'last': 'position(snapshot) == -1', 'rest': 'position(snapshot) < -1'}) assert verdict.status is Status.PARTITION def test_a_band_counted_from_the_back(self, schema: Model): verdict = check( schema, - None, { 'final_two': 'position(snapshot) >= -2', 'earlier': 'position(snapshot) < -2', @@ -146,35 +176,39 @@ def test_a_band_counted_from_the_back(self, schema: Model): assert verdict.status is Status.PARTITION def test_numeric_bands(self, schema: Model): + """And the same for a magnitude: an absent capacity needs a value too.""" verdict = check( schema, - 'capacity > 0', - {'small': 'capacity <= 10', 'large': 'capacity > 10'}, + { + 'small': 'capacity and capacity <= 10', + 'large': 'capacity and capacity > 10', + 'unknown': 'not capacity', + }, ) assert verdict.status is Status.PARTITION class TestRefuses: def test_an_overlap_names_both_cases_and_a_witness(self, schema: Model): - verdict = check(schema, None, {'cyclic': 'cyclic', 'battery': "kind == 'battery'"}) + verdict = check(schema, {'cyclic': 'cyclic', 'battery': "kind == 'battery'"}) assert verdict.status is Status.VIOLATED assert verdict.overlaps[0].cases == ('cyclic', 'battery') assert 'cyclic is true' in verdict.message() - def test_a_gap_is_a_row_with_no_expression(self, schema: Model): - verdict = check(schema, None, {'first': 'position(snapshot) == 0'}) + def test_a_gap_is_a_coordinate_with_no_value(self, schema: Model): + verdict = check(schema, {'first': 'position(snapshot) == 0'}) assert verdict.status is Status.VIOLATED assert verdict.gaps - assert 'no case claims the row' in verdict.message() + assert 'no case claims the value' in verdict.message() - def test_a_case_the_where_excludes_is_dead(self, schema: Model): - verdict = check(schema, 'not cyclic', {'cyclic': 'cyclic', 'rest': 'not cyclic'}) + def test_a_case_that_can_never_hold_is_dead(self, schema: Model): + verdict = check(schema, {'never': 'cyclic and not cyclic', 'rest': 'True'}) assert verdict.status is Status.VIOLATED - assert verdict.dead == ('cyclic',) + assert verdict.dead == ('never',) def test_defined_is_not_non_zero(self, schema: Model): """A bare name and `!= 0` are different questions, so these leave a gap.""" - verdict = check(schema, None, {'has_initial': 'soc_initial', 'zero': 'soc_initial == 0'}) + verdict = check(schema, {'has_initial': 'soc_initial', 'zero': 'soc_initial == 0'}) assert verdict.status is Status.VIOLATED @@ -185,7 +219,6 @@ def test_both_ends_of_a_data_bound_axis(self, schema: Model): """ verdict = check( schema, - None, { 'first': 'position(snapshot) == 0', 'last': 'position(snapshot) == -1', @@ -199,7 +232,6 @@ def test_a_group_never_has_a_declared_extent(self, schema: Model): """`by=` counts within each group, and no declaration sizes those.""" verdict = check( schema, - None, { 'first': 'position(snapshot, by=period_of) == 0', 'last': 'position(snapshot, by=period_of) == -1', @@ -283,16 +315,13 @@ def test_a_proved_partition_holds_on_a_finer_grid(self, schema: Model, seed: int Case('b', AndNode(split, NotNode(inner))), Case('c', NotNode(split)), ] - where = self._mask(rng, atoms) if rng.random() < 0.4 else None - if check_partition(where, cases, schema).status is not Status.PARTITION: + if check_partition(cases, schema).status is not Status.PARTITION: continue proved += 1 # The same frame the check built, so ground truth reads each atom # the way it did — what differs is the grid, which is finer. - frame = _Frame.of([where, *(case.when for case in cases)], schema) + frame = _Frame.of([case.when for case in cases], schema) for point in grid: - if where is not None and not _evaluate(where, point, frame): - continue claims = sum(1 for case in cases if _evaluate(case.when, point, frame)) assert claims == 1, f'{claims} cases claim {point} — the cells hid a witness' assert proved > 50, f'only {proved} partitions proved; the fuzz is not exercising the check'