feat(language): a model states the conditions its data must satisfy, so a table that breaks one is refused rather than solved

docs/reference/language/declarations.md

@@ -207,3 +207,46 @@ different models, and the bracket is the difference.
 
 A second objective is unsayable rather than checked — the schema holds one
 block. Weight several goals into one expression.
+
+## `checks`
+
+A condition the **data** must satisfy for the model to mean what it says. It
+builds no row and changes no answer; it is the sentence a reader has to believe
+about the table before believing the constraints above it.
+
+```yaml
+parameters:
+  CVaR_omega: { dims: [] }
+  Link_efficiency: { dims: [link] }
+checks:
+  omega_is_a_share: "CVaR_omega >= 0 AND CVaR_omega <= 1"
+  efficiency_is_a_share:
+    holds: "Link_efficiency > 0 AND Link_efficiency <= 1"
+    description: a link delivers some of what it takes, and no more
+```
+
+| Field         |                                                                        |                |
+| ------------- | ---------------------------------------------------------------------- | -------------- |
+| `holds`       | required — a `where` predicate ([where](expressions.md#where-strings)) |                |
+| `description` | free text                                                              | default `null` |
+
+Written as a bare string wherever it carries no description, like a named
+expression.
+
+**There is no `foreach`.** A check is asked at every coordinate the names in it
+span — `Link_efficiency` over `link` is one question per link, and a scalar
+parameter is one question — so the frame is read off the predicate rather than
+declared beside it.
+
+**Nothing here checks it.** No file determines whether a table satisfies a
+condition, so the language states it and the consumer binding the data raises
+it, in the language's own words — `check_message` is the sentence, and the
+`description:` is its second half, which is why a check is the one declaration
+whose prose reaches the program
+([reading a loaded model](reading.md)). What _is_ decided at load is that the
+condition is one data could break: a predicate the connectives settle to
+`True` checks nothing and one that settles to `False` refuses every table, and
+both are load errors naming the rewrite. So is a predicate reading a variable,
+which has no value before the solve.
+
+A check prints, under **Data conditions**, as the predicate it is — last, and [droppable](../typeset.md#options) for a page about the math alone.

docs/reference/language/file.md

@@ -20,6 +20,7 @@ and `description`:
 | `macros`      | parameterised templates ([macros](expressions.md#macros))                                                    |
 | `piecewise`   | piecewise-linear curves ([piecewise](piecewise.md))                                                          |
 | `sos`         | special-ordered sets ([sos](piecewise.md#sos))                                                               |
+| `checks`      | conditions the bound data must satisfy ([checks](declarations.md#checks))                                    |
 
 Any subset is accepted, `objective` included: a file with none is a
 **feasibility problem**, and the answer is whether the constraints can be met

docs/reference/language/reading.md

@@ -89,12 +89,19 @@ with nothing to see. `Program` is a different type from `Spec`, so that
 mistake is one the signature refuses rather than one the numbers report.
 
 **A program cannot answer what the file wrote.** It has no `macros:`, no
-`description:`, and no link expression — those are the `Spec`'s, and
+link expression, and no `description:` — bar one, below — so those are the
+`Spec`'s, and
 rendering has to be handed what `to_spec` returned. The projection runs one
 way on purpose. What it keeps of a `piecewise:` block is `program.piecewise`:
 which parameters carry the curve, and what the block assumes of the numbers as
 a `checks` tuple — each check carrying the names it is about, so the consumer
 holding the numbers runs it, with `check_message` for the sentence to raise.
+`program.checks` is the same vocabulary where the _file_ wrote the condition
+rather than a curve implying it: one `Holds` per
+[`checks:`](declarations.md#checks) block, carrying the resolved predicate, the
+dims it is asked over, and — the one prose a program keeps — the block's own
+`description:`, because there it is not documentation but the second half of
+the sentence `check_message` returns.
 What the expansion emitted is answered where it is asked instead: a
 `ParameterDeclaration.derivation` says how that parameter is filled, and `None`
 means the caller binds it.

docs/reference/typeset.md

@@ -39,6 +39,7 @@ The three functions take the same keywords; the CLI spells each as a flag.
 | `symbols`    | `--symbols FILE` | how names should print — [below](#symbol-tables). Default: derived                  |
 | `standalone` | `--standalone`   | emit a document that compiles, rather than a fragment to include. Default: fragment |
 | `legend`     | `--no-legend`    | the sets / parameters / variables table above the math. Default: on                 |
+| `checks`     | `--no-checks`    | the data conditions the model declares, below the math. Default: on                 |
 | `numbered`   | `--no-numbers`   | number the equations. Default: on                                                   |
 
 `-o FILE` writes to a file instead of stdout.
@@ -51,6 +52,10 @@ that is the math the solver receives. Where the math translates an index —
 what the notation for it means, so a reader meets no symbol the page has not
 defined.
 
+A [`checks:`](language/declarations.md#checks) block prints last, under **Data
+conditions** — a condition on the _input_ rather than a row a solver holds, so
+`--no-checks` leaves a page about the math alone.
+
 A model that does not compile does not print: typesetting runs the same
 load-time checks everything else does.
 

examples/pypsa_stochastic.yaml

@@ -202,3 +202,16 @@ objective:
     sum(Generator_p_nom_ext * Generator_capital_cost)
     + (1 - CVaR_omega) * sum(scenario_weight * scenario_opex, over=scenario)
     + CVaR_omega * CVaR
+
+checks:
+  omega_is_a_share:
+    holds: "CVaR_omega >= 0 AND CVaR_omega <= 1"
+    description: >-
+      the objective blends the expectation and the tail at `omega` and
+      `1 - omega`, so outside [0, 1] it is an extrapolation of the two rather
+      than a mix of them
+  tail_probability_is_one_or_more:
+    holds: "CVaR_inv_tail >= 1"
+    description: >-
+      `1 / (1 - alpha)` for a probability `alpha`, so below one the CVaR row
+      prices the tail at less than its own expectation

schema/math-spec.schema.json

@@ -30,6 +30,40 @@
       "title": "BoundsBlock",
       "type": "object"
     },
+    "CheckBlock": {
+      "anyOf": [
+        {
+          "additionalProperties": false,
+          "description": "A condition the data must satisfy for the model to mean what it says.\n\nWritten in YAML as a bare string, or as a mapping once it carries a\n``description:`` \u2014 and serialised back to whichever form it was written in,\nso a round trip through :meth:`Spec.to_yaml` reproduces the file::\n\n    checks:\n      omega_is_a_share: \"CVaR_omega >= 0 AND CVaR_omega <= 1\"\n      efficiency_is_a_share:\n        holds: \"Link_efficiency > 0 AND Link_efficiency <= 1\"\n        description: a link delivers some of what it takes, and no more\n\n``holds:`` is a ``where`` predicate, read over the dims the names in it\ncarry. It builds no row: a consumer holding the data refuses a model whose\ntable breaks it, in the language's own words\n(:func:`~math_spec.program.check_message`).",
+          "properties": {
+            "description": {
+              "anyOf": [
+                {
+                  "type": "string"
+                },
+                {
+                  "type": "null"
+                }
+              ],
+              "default": null,
+              "title": "Description"
+            },
+            "holds": {
+              "title": "Holds",
+              "type": "string"
+            }
+          },
+          "required": [
+            "holds"
+          ],
+          "title": "CheckBlock",
+          "type": "object"
+        },
+        {
+          "type": "string"
+        }
+      ]
+    },
     "ConstraintBlock": {
       "additionalProperties": false,
       "description": "A declared constraint: one rule, over one frame.",
@@ -552,8 +586,16 @@
   },
   "$schema": "https://json-schema.org/draft/2020-12/schema",
   "additionalProperties": false,
-  "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nThe API is the ten declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. In goes through\n``to_spec``, which raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\n\nEverything else on this class is pydantic's, not a contract this package\nkeeps \u2014 ``model_json_schema()`` describes the shape pydantic validates\nrather than the language (checked in for editors as\n``schema/math_spec.schema.json``), and ``model_construct()`` skips validation\nentirely, so a ``Spec`` is valid when it was built the normal way.",
+  "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nThe API is the eleven declaration sections plus ``version`` and\n``description``, and two ways back out: :meth:`to_dict` for the model as\ndata, :meth:`to_yaml` for the file a reviewer reads. In goes through\n``to_spec``, which raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\n\nEverything else on this class is pydantic's, not a contract this package\nkeeps \u2014 ``model_json_schema()`` describes the shape pydantic validates\nrather than the language (checked in for editors as\n``schema/math_spec.schema.json``), and ``model_construct()`` skips validation\nentirely, so a ``Spec`` is valid when it was built the normal way.",
   "properties": {
+    "checks": {
+      "additionalProperties": {
+        "$ref": "#/$defs/CheckBlock"
+      },
+      "default": {},
+      "title": "Checks",
+      "type": "object"
+    },
     "constraints": {
       "additionalProperties": {
         "$ref": "#/$defs/ConstraintBlock"

src/math_spec/__main__.py

@@ -36,6 +36,7 @@ def parser() -> argparse.ArgumentParser:
         verb.add_argument('--symbols', help='sidecar YAML saying how names should print')
         verb.add_argument('--standalone', action='store_true', help='emit a compilable document')
         verb.add_argument('--no-legend', action='store_true', help='omit the sets/parameters/variables table')
+        verb.add_argument('--no-checks', action='store_true', help='omit the data conditions the model declares')
         verb.add_argument('--no-numbers', action='store_true', help='leave the equations unnumbered')
     return front
 
@@ -61,6 +62,7 @@ def main(argv: list[str] | None = None) -> int:
         symbols=args.symbols,
         standalone=args.standalone,
         legend=not args.no_legend,
+        checks=not args.no_checks,
         numbered=not args.no_numbers,
     )
     if args.out:

src/math_spec/dimensions.py

@@ -464,6 +464,31 @@ def check_schema(schema: Spec) -> None:
             )
 
 
+def where_dims(node: WhereNode | None, schema: Spec) -> frozenset[str]:
+    """The dims a resolved predicate reads.
+
+    A ``where:`` is checked *against* a declared frame; a ``checks:`` block has
+    no frame of its own, so its rows are exactly the coordinates its names
+    span, and this is what says which those are.
+    """
+    if node is None or isinstance(node, BooleanLiteralNode):
+        return frozenset()
+    if isinstance(node, (ParameterDefinedNode, ParameterComparisonNode)):
+        return frozenset(schema.parameters[node.name].dims)
+    if isinstance(node, VariableDefinedNode):
+        return frozenset(schema.variables[node.name].foreach)
+    if isinstance(node, (DimensionComparisonNode, DimensionPositionNode)):
+        return frozenset({node.name})
+    if isinstance(node, (LookupComparisonNode, LookupPairComparisonNode, LookupDefinedNode)):
+        return frozenset({node.over})
+    if isinstance(node, NotNode):
+        return where_dims(node.operand, schema)
+    if isinstance(node, (AndNode, OrNode)):
+        return where_dims(node.left, schema) | where_dims(node.right, schema)
+    msg = f'{type(node).__name__} reached the dim reader unresolved.'
+    raise AssertionError(msg)
+
+
 def _check_where_dims(
     node: WhereNode | None,
     schema: Spec,

src/math_spec/lowering.py

@@ -32,7 +32,7 @@
 from typing import TYPE_CHECKING, Literal, assert_never, cast
 
 import math_spec.program as program
-from math_spec.dimensions import dims_of
+from math_spec.dimensions import dims_of, where_dims
 from math_spec.errors import LanguageError
 from math_spec.expression_parser import (
     ArithmeticNode,
@@ -187,6 +187,7 @@ def lower_program(schema: _ExpandedSpec) -> program.Program:
         for sname, sdef in expanded.sos.items()
     }
     expressions = {name: _lower_expression(expanded, ns, name) for name in expanded.expressions}
+    checks = {name: _lower_check(expanded, ns, name) for name in expanded.checks}
     return program.Program(
         parameters=parameters,
         variables=variables,
@@ -196,9 +197,18 @@ def lower_program(schema: _ExpandedSpec) -> program.Program:
         sos=sos,
         piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()},
         named_expressions=expressions,
+        checks=checks,
     )
 
 
+def _lower_check(schema: _ExpandedSpec, ns: Namespace, name: str) -> program.Holds:
+    """Resolve the check *name* and read the coordinates it is asked at off its own names."""
+    block = schema.checks[name]
+    holds = where_of(block.holds, ns, f"check '{name}'")
+    assert holds is not None, 'load-time validation refuses a check that holds whatever the data says'
+    return program.Holds(holds, tuple(sorted(where_dims(holds, schema))), block.description)
+
+
 def _lower_expression(schema: _ExpandedSpec, ns: Namespace, name: str) -> program.ExpressionNode:
     """Compile the named expression *name* into a program expression.
 

src/math_spec/model.py

@@ -352,6 +352,48 @@ def _as_written(self) -> str | dict[str, str]:
         return {'expression': self.expression, 'description': self.description}
 
 
+class CheckBlock(_StrictBlock):
+    """A condition the data must satisfy for the model to mean what it says.
+
+    Written in YAML as a bare string, or as a mapping once it carries a
+    ``description:`` — and serialised back to whichever form it was written in,
+    so a round trip through :meth:`Spec.to_yaml` reproduces the file::
+
+        checks:
+          omega_is_a_share: "CVaR_omega >= 0 AND CVaR_omega <= 1"
+          efficiency_is_a_share:
+            holds: "Link_efficiency > 0 AND Link_efficiency <= 1"
+            description: a link delivers some of what it takes, and no more
+
+    ``holds:`` is a ``where`` predicate, read over the dims the names in it
+    carry. It builds no row: a consumer holding the data refuses a model whose
+    table breaks it, in the language's own words
+    (:func:`~math_spec.program.check_message`).
+    """
+
+    _label: ClassVar[str] = 'a check'
+
+    holds: str
+    description: str | None = None
+
+    @model_validator(mode='before')
+    @classmethod
+    def _from_string(cls, data: Any) -> Any:
+        return {'holds': data} if isinstance(data, str) else data
+
+    @classmethod
+    @override
+    def __get_pydantic_json_schema__(cls, core_schema: CoreSchema, handler: GetJsonSchemaHandler) -> JsonSchemaValue:
+        """The published schema admits the bare string the one-line form is written as."""
+        return _also_written_as(core_schema, handler, {'type': 'string'})
+
+    @model_serializer
+    def _as_written(self) -> str | dict[str, str]:
+        if self.description is None:
+            return self.holds
+        return {'holds': self.holds, 'description': self.description}
+
+
 class PiecewiseLink(_StrictBlock):
     """One link of a piecewise block: an expression pinned to a values curve.
 
@@ -582,7 +624,7 @@ def _is_absent(value: Any) -> bool:
 class Spec(_StrictBlock):
     """The declared math — one YAML file, or one dict, validated. Nothing here has seen data.
 
-    The API is the ten declaration sections plus ``version`` and
+    The API is the eleven declaration sections plus ``version`` and
     ``description``, and two ways back out: :meth:`to_dict` for the model as
     data, :meth:`to_yaml` for the file a reviewer reads. In goes through
     ``to_spec``, which raises
@@ -620,6 +662,7 @@ class Spec(_StrictBlock):
     macros: dict[str, MacroBlock] = {}
     piecewise: dict[str, PiecewiseBlock] = {}
     sos: dict[str, SosBlock] = {}
+    checks: dict[str, CheckBlock] = {}
 
     def targeted_of(self, dimension: str) -> dict[str, str]:
         """The groupable lookups over *dimension*: name -> the dim they map into."""

src/math_spec/piecewise.py

@@ -101,8 +101,8 @@ def declaration_of(expanded: ExpandedPiecewise) -> PiecewiseDeclaration:
     curvature = _curvature_required(pw)
     if curvature is not None:
         x, y = pw.curve
-        checks.append(Increasing(x.values, pw.over))
-        checks.append(Curved(x.values, y.values, pw.over, curvature))
+        checks.append(Increasing(x.values, pw.over, pw.method))
+        checks.append(Curved(x.values, y.values, pw.over, curvature, pw.method))
     if pw.method == 'lp':
         checks.append(AtLeastTwo(pw.over, expanded.points))
     if expanded.points is not None: