What happened?
where: "snapshot > index(snapshot, 0)" parses, resolves, validates, and typesets. It has two possible meanings, and nothing in the language or the package chooses between them — so the file loads and which model it means is undetermined.
As a value. index(snapshot, 0) names the coordinate that sits at position 0, and > compares the row's coordinate against it. The mask then depends on how coordinates sort, and snapshot == index(snapshot, 0) or snapshot > index(snapshot, 0) misses every coordinate sorting below the first one.
As a position. > compares ranks — "later in the dimension's order than the first" — the mask does not depend on sorting at all, and the same two masks cover every row.
The two agree on == and !=, which is why this has not bitten yet. All four ordering comparators (<, <=, >, >=) are affected.
This is rule 2's territory — "everything decidable without data is decided without data", and nothing is guessed. A construct whose meaning the file does not determine should be a load error at worst and a defined meaning at best; today it is neither.
Expected: either the docs define which comparison it is and both lanes implement that, or resolve_where refuses the four ordering comparators against index() and names the rewrite.
Where it is underspecified. dimensions.md says where the coordinates come from "and in what order, is settled when data is bound", so the file never declares the order to be the sorted order. The where-string table describes the surface as "the coordinate at position i of that dimension's own order" and does not say what an ordering against it compares.
It reaches the typeset math too. The rendered LaTeX is t > \mathrm{index}(\mathcal{T}, 0) — the same ambiguity, now in the paper, so a reader cannot recover the model either.
Proposed fix
The position reading. index() exists to name a coordinate by where it sits rather than by the label that happens to be there — that is its whole argument in declarations.md, where a boundary clause "survives the index being relabelled". An ordering that silently depends on labels sorting the same way as positions gives that back. It also needs no claim about the data.
The cost is that a value comparison against a positional coordinate becomes unsayable, which looks cheap: comparing coordinates against a literal (snapshot > '2030-01-01') already says a value boundary and does not need index().
Either answer closes the bug. What is not acceptable is that both are sayable and the file cannot tell you which it got.
How it surfaced
The partition check in #31 has to decide whether case masks cover a constraint's rows exactly once, and the two readings disagree for == index(0) / > index(0): a partition under the position reading, not one under the value reading. The first cut of that checker quietly took the position reading and proved a partition on the strength of it; it now refuses the shape as undecidable and names the rewrite. That is correct behaviour for the checker, but it works around this bug rather than fixing it.
Which operating systems have you used?
Version
v0.0.0 (main @ 526fdf8)
Relevant log output
>>> from math_spec.validation import load_model, validate_expressions
>>> from math_spec.resolution import Namespace, where_of
>>> model = load_model({
... 'dimensions': {'snapshot': {'dtype': 'int'}},
... 'variables': {'soc': {'foreach': ['snapshot']}},
... 'constraints': {
... 'first': {'foreach': ['snapshot'], 'where': 'snapshot == index(snapshot, 0)', 'expression': 'soc == 0'},
... 'rest': {'foreach': ['snapshot'], 'where': 'snapshot > index(snapshot, 0)', 'expression': 'soc == 1'},
... },
... })
>>> validate_expressions(model) # no error
>>> where_of('snapshot > index(snapshot, 0)', Namespace.of(model), 'the mask')
DimensionPositionNode(name='snapshot', op='>', position=0, by=None)
# and the typeset math carries the ambiguity through:
# \forall\, t \in \mathcal{T} \,:\, t > \mathrm{index}(\mathcal{T}, 0)
What happened?
where: "snapshot > index(snapshot, 0)"parses, resolves, validates, and typesets. It has two possible meanings, and nothing in the language or the package chooses between them — so the file loads and which model it means is undetermined.As a value.
index(snapshot, 0)names the coordinate that sits at position 0, and>compares the row's coordinate against it. The mask then depends on how coordinates sort, andsnapshot == index(snapshot, 0) or snapshot > index(snapshot, 0)misses every coordinate sorting below the first one.As a position.
>compares ranks — "later in the dimension's order than the first" — the mask does not depend on sorting at all, and the same two masks cover every row.The two agree on
==and!=, which is why this has not bitten yet. All four ordering comparators (<,<=,>,>=) are affected.This is rule 2's territory — "everything decidable without data is decided without data", and nothing is guessed. A construct whose meaning the file does not determine should be a load error at worst and a defined meaning at best; today it is neither.
Expected: either the docs define which comparison it is and both lanes implement that, or
resolve_whererefuses the four ordering comparators againstindex()and names the rewrite.Where it is underspecified.
dimensions.mdsays where the coordinates come from "and in what order, is settled when data is bound", so the file never declares the order to be the sorted order. The where-string table describes the surface as "the coordinate at positioniof that dimension's own order" and does not say what an ordering against it compares.It reaches the typeset math too. The rendered LaTeX is
t > \mathrm{index}(\mathcal{T}, 0)— the same ambiguity, now in the paper, so a reader cannot recover the model either.Proposed fix
The position reading.
index()exists to name a coordinate by where it sits rather than by the label that happens to be there — that is its whole argument indeclarations.md, where a boundary clause "survives the index being relabelled". An ordering that silently depends on labels sorting the same way as positions gives that back. It also needs no claim about the data.The cost is that a value comparison against a positional coordinate becomes unsayable, which looks cheap: comparing coordinates against a literal (
snapshot > '2030-01-01') already says a value boundary and does not needindex().Either answer closes the bug. What is not acceptable is that both are sayable and the file cannot tell you which it got.
How it surfaced
The partition check in #31 has to decide whether case masks cover a constraint's rows exactly once, and the two readings disagree for
== index(0)/> index(0): a partition under the position reading, not one under the value reading. The first cut of that checker quietly took the position reading and proved a partition on the strength of it; it now refuses the shape as undecidable and names the rewrite. That is correct behaviour for the checker, but it works around this bug rather than fixing it.Which operating systems have you used?
Version
v0.0.0 (
main@ 526fdf8)Relevant log output
>>> from math_spec.validation import load_model, validate_expressions >>> from math_spec.resolution import Namespace, where_of >>> model = load_model({ ... 'dimensions': {'snapshot': {'dtype': 'int'}}, ... 'variables': {'soc': {'foreach': ['snapshot']}}, ... 'constraints': { ... 'first': {'foreach': ['snapshot'], 'where': 'snapshot == index(snapshot, 0)', 'expression': 'soc == 0'}, ... 'rest': {'foreach': ['snapshot'], 'where': 'snapshot > index(snapshot, 0)', 'expression': 'soc == 1'}, ... }, ... }) >>> validate_expressions(model) # no error >>> where_of('snapshot > index(snapshot, 0)', Namespace.of(model), 'the mask') DimensionPositionNode(name='snapshot', op='>', position=0, by=None) # and the typeset math carries the ambiguity through: # \forall\, t \in \mathcal{T} \,:\, t > \mathrm{index}(\mathcal{T}, 0)