feat(language): math can be layered onto a model built elsewhere

docs/about/limits.md

@@ -199,8 +199,15 @@ A template reads the coupling surface it is written against, and declares that
 column under `given_variables:`. So a template loads on its own, and prints as
 math on its own, which is what it could not do while a fragment was a file the
 loader had to refuse. `merge` folds each given declaration into the one that
-introduces it, and a program carries none of them: a build makes every column it
-holds.
+introduces it, so a composed library carries none.
+
+A layer over a model this language never sees — one built through linopy, say —
+has nothing to fold into. There the declaration stays, and the program carries
+the name and the frame for a consumer to bind, under
+[what a program does not build](../reference/language/reading.md#what-a-program-does-not-build).
+`given_constraints:` is the same fact about a row family: `dual(balance)` prices
+what the base model settles, and the file says how many duals there are and what
+indexes them.
 
 The verb is built to collide, so every collision the caller did not ask for is
 refused. An entry naming some fields of a declaration the base does not have is

docs/howto/compose.md

@@ -62,9 +62,9 @@ compose: `override(merge({…}), {…})`.
      expression: sum(gen_p * gen_cost)
    ```
 
-   The template loads on its own, and it prints as math on its own. What it
-   cannot do is lower: a program builds every column it carries, and this file
-   says the opposite about `flow`.
+   The template loads on its own, and it prints as math on its own. Lowering
+   it gives a program that names `flow` as a column to bind rather than build,
+   which is what a layer over another model wants; a library merges instead.
 
 3. **Merge the templates you need.** Each fragment is given a name, and that
    name is what a refusal calls it.

docs/reference/language/declarations.md

@@ -152,18 +152,43 @@ An expression reads a given variable as it reads any other, so
 `at(flow, by=gen_port)` lands on the generator frame and the dim algebra
 checks it at load.
 
-**A file with a `given_variables` block does not lower.** A program builds
-every column it carries, and this file says the opposite about one of its own:
-
-```text
-this file reads a variable it does not introduce: 'flow'. A program builds every column it carries, so compose the file with the ones that declare them first — to_program(merge({...})). The file loads and prints on its own either way.
-```
-
 [`merge`](../../howto/compose.md) folds each given declaration into the
-declaration that introduces it, so a composed model carries none of them. The
+declaration that introduces it, so a composed library carries none of them. The
 folded declaration is the introducer's, and what the reader stated has to agree
 with it.
 
+Where nothing in this language introduces the column — a layer over a model
+built in Python — the declaration stays, and the program carries it for a
+consumer to bind. See
+[what a program does not build](reading.md#what-a-program-does-not-build).
+
+## `given_constraints`
+
+A given constraint is a row family this file reads the dual of and another
+model builds. It is what lets a layer price something the base model settles.
+
+```yaml
+given_constraints:
+  balance:
+    dims: [snapshot, bus]
+    description: the host model clears each bus
+expressions:
+  price:
+    expression: dual(balance)
+```
+
+| Field         |                                                   |                |
+| ------------- | ------------------------------------------------- | -------------- |
+| `dims`        | required. The dimensions the row family runs over |                |
+| `description` | free text                                         | default `null` |
+
+There is no `expression`, because nothing here builds the row, and no `sense`.
+The dual comes back from whoever solved the model, under that model's own
+convention, and a sense written here would be a claim no file could check.
+
+`dual(name)` is the only place a given row family may be named, and the frame
+is what gives the reported expression its dimensions.
+
 ## `constraints`
 
 One block is one rule. The name of the block is the name of the constraint, and

docs/reference/language/file.md

@@ -5,8 +5,8 @@ SPDX-License-Identifier: CC-BY-4.0
 
 # File shape
 
-A model file is a YAML mapping with **eleven declaration keys**, plus
-`version` and `description`. Any subset of the eleven is accepted.
+A model file is a YAML mapping with **twelve declaration keys**, plus
+`version` and `description`. Any subset of the twelve is accepted.
 
 | Key               |                                                                                                                     |
 | ----------------- | ------------------------------------------------------------------------------------------------------------------- |

docs/reference/language/index.md

@@ -46,7 +46,7 @@ message that names the fix. These ten rules are what it checks.
 
 | #   | Rule                                                                                                                                                                                                                                     |                                                                 |
 | --- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------- |
-| 1   | A file has eleven declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`.                                                                  | [File shape](file.md)                                           |
+| 1   | A file has twelve declaration keys, plus `version` and `description`. A key the schema does not know is refused, with the nearest valid key named: `boundz` → `bounds`.                                                                  | [File shape](file.md)                                           |
 | 2   | Everything that can be checked without data is checked when the file loads.                                                                                                                                                              | [Errors](errors.md)                                             |
 | 3   | Every name is declared once. A parameter and a dimension both called `snapshot` is refused, and the message names both lines.                                                                                                            | [Names](expressions.md#name-resolution)                         |
 | 4   | Where a name may stand depends on what it is. A dimension may follow `over=` or `along=`, and may not be multiplied: `dispatch * snapshot` is refused, because `snapshot` is an axis and not a column of numbers.                        | [Names](expressions.md#name-resolution)                         |

docs/reference/language/reading.md

@@ -116,6 +116,44 @@ tree, so a boolean literal stands at a mask's root or nowhere. A tree with an
 unresolved leaf is refused. A `Region`'s `when` arrives as a `Mask` too. The node
 classes live in `math_spec.program`.
 
+## What a program does not build
+
+`program.given_variables` and `program.given_constraints` name what the model
+reads and does not build. Every other group is a build instruction — a column
+for each entry of `variables`, a row family for each entry of `constraints`.
+These two are the opposite: a name to look up in the model this one is layered
+onto.
+
+```python
+layer = to_program(
+    {
+        'dimensions': {'snapshot': {'dtype': 'int'}, 'bus': {'dtype': 'str'}},
+        'given_variables': {'p': {'dims': ['snapshot', 'bus']}},
+        'given_constraints': {'balance': {'dims': ['snapshot', 'bus']}},
+        'parameters': {'rate': {'dims': ['bus']}},
+        'constraints': {'cap': {'dims': [], 'expression': 'sum(p * rate) <= 100'}},
+        'expressions': {'price': {'expression': 'dual(balance)'}},
+    }
+)
+
+sorted(layer.variables)  # []
+sorted(layer.given_variables)  # ['p']
+layer.given_constraints['balance'].dims  # ('snapshot', 'bus')
+```
+
+A consumer that builds a program does three things with them:
+
+1. **Bind each name** to a column or a row family the host model already holds.
+2. **Check the frame.** `dims` is what the file claims about the shape, and it
+   is the one claim a binder can settle.
+3. **Refuse what it cannot bind, and name it.** Building a column of its own
+   instead would be a second column nothing else refers to, and the model would
+   solve and be wrong.
+
+A consumer with no host to bind against refuses a program whose two groups are
+not both empty. [`merge`](../../howto/compose.md) is what empties them wherever
+a file in this language introduces the declaration.
+
 ## Asking what a program uses
 
 `program.footprint` says which of the language's constructs one model uses. It

schema/math-spec.schema.json

@@ -216,6 +216,36 @@
       "title": "ExpressionCase",
       "type": "object"
     },
+    "GivenConstraintBlock": {
+      "additionalProperties": false,
+      "description": "A row family this file reads the dual of and does not build.\n\nThe frame says how many duals there are and what indexes them, which is\nwhat ``dual()`` needs and all this file can answer. There is no\n``expression:``: the body is the owner's, and nothing here builds a row.",
+      "properties": {
+        "description": {
+          "anyOf": [
+            {
+              "type": "string"
+            },
+            {
+              "type": "null"
+            }
+          ],
+          "default": null,
+          "title": "Description"
+        },
+        "dims": {
+          "items": {
+            "type": "string"
+          },
+          "title": "Dims",
+          "type": "array"
+        }
+      },
+      "required": [
+        "dims"
+      ],
+      "title": "GivenConstraintBlock",
+      "type": "object"
+    },
     "GivenVariableBlock": {
       "additionalProperties": false,
       "description": "A variable this file reads and does not introduce.\n\nThe frame is what every load-time pass asks of a variable, and it is all\nthis file can answer: whoever introduces the column owns its bounds and its\nmask, and a second spelling of either here would be a second home for one\nfact. :func:`~math_spec.composition.merge` folds the declaration into the\none that introduces it, so a composed model carries none of these.",
@@ -676,7 +706,7 @@
   },
   "$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\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\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. Everything else on\nthis class is pydantic's, not a contract this package keeps.",
+  "description": "The declared math \u2014 one YAML file, or one dict, validated. Nothing here has seen data.\n\nA ``Spec`` that exists has passed the whole language: constructing one by\nany route \u2014 ``to_spec``, :meth:`model_validate`, the constructor \u2014 runs\nevery load-time check, expansion and expression pass included, and raises\n:class:`~math_spec.errors.LanguageError` on a model the language refuses.\nHolding one is the proof, so nothing downstream checks it again.\n\nThe API is the twelve 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. Everything else on\nthis class is pydantic's, not a contract this package keeps.",
   "properties": {
     "constraints": {
       "additionalProperties": {
@@ -714,6 +744,14 @@
       "title": "Expressions",
       "type": "object"
     },
+    "given_constraints": {
+      "additionalProperties": {
+        "$ref": "#/$defs/GivenConstraintBlock"
+      },
+      "default": {},
+      "title": "Given Constraints",
+      "type": "object"
+    },
     "given_variables": {
       "additionalProperties": {
         "$ref": "#/$defs/GivenVariableBlock"

src/math_spec/advice.py

@@ -33,11 +33,34 @@ def advice(model: str | Path | dict[str, Any] | Spec | Program) -> tuple[Advice,
             answer alike.
 
     Returns:
-        The never-an-axis advice in declaration order, then the unboundedness
-        advice; ``str()`` of each is its sentence.
+        The never-an-axis advice in declaration order, then what the model
+        reads and does not build, then the unboundedness advice; ``str()`` of
+        each is its sentence.
     """
     program = to_program(model)
-    return tuple(_never_an_axis(program) + unbounded_notes(program))
+    return tuple(_never_an_axis(program) + _given(program) + unbounded_notes(program))
+
+
+def _given(program: Program) -> list[Advice]:
+    """One note per declaration the program reads and does not build.
+
+    A note rather than a refusal, because both readings are a model somebody
+    meant: a template is composed with the file that introduces the column, and
+    a layer is bound to the model it is laid onto. What neither is, is a model
+    a consumer can build alone, and the consumer is the one that can tell which
+    it is holding.
+    """
+    return [
+        Advice(
+            'given',
+            name,
+            f"{kind} '{name}' is read here and built elsewhere: a consumer binds it to the model this "
+            f'one is layered onto, and refuses where it cannot. A template is composed instead, and '
+            f'merge() folds it into the file that introduces it.',
+        )
+        for kind, group in (('variable', program.given_variables), ('row family', program.given_constraints))
+        for name in group
+    ]
 
 
 def _never_an_axis(program: Program) -> list[Advice]:
@@ -50,6 +73,8 @@ def _never_an_axis(program: Program) -> list[Advice]:
     reached: set[str] = set()
     for declaration in (*program.parameters.values(), *program.variables.values(), *program.constraints.values()):
         reached.update(declaration.dims)
+    reached.update(dim for given in program.given_variables.values() for dim in given.dims)
+    reached.update(dim for given in program.given_constraints.values() for dim in given.dims)
     reached |= _produced_axes(program)
     reached |= {dim for lk in program.relations.values() for dim in lk.dims}
 

src/math_spec/composition.py

@@ -73,7 +73,7 @@
 #: The declarations a file reads and does not introduce. Peers must agree
 #: about one, and :func:`merge` folds it into the declaration that introduces
 #: it, so a composed library carries none.
-GIVEN_SECTIONS = ('given_variables',)
+GIVEN_SECTIONS = ('given_variables', 'given_constraints')
 
 #: Every section keyed by declaration name. ``objective`` is one declaration
 #: rather than a mapping of them, and is laid over field by field beside these.

src/math_spec/dimensions.py

@@ -97,7 +97,7 @@ def _dims(
         raise AssertionError(msg)
 
     if isinstance(node, DualNode):
-        return frozenset(schema.constraints[node.constraint].dims)
+        return frozenset({**schema.constraints, **schema.given_constraints}[node.constraint].dims)
 
     if isinstance(node, FunctionCallNode):
         return _dims_call(node, schema, context)

src/math_spec/errors.py

@@ -18,7 +18,7 @@
 
 #: Which pass an :class:`Advice` comes from. Closed, like the operator set: a
 #: consumer filtering on it can enumerate every value.
-AdviceKind = Literal['never-an-axis', 'unbounded']
+AdviceKind = Literal['never-an-axis', 'unbounded', 'given']
 ADVICE_KINDS = frozenset(get_args(AdviceKind))
 
 

src/math_spec/lowering.py

@@ -34,12 +34,11 @@
     VariableNode,
 )
 from math_spec.dimensions import dims_of
-from math_spec.errors import LanguageError
 from math_spec.piecewise import declaration_of, derivations_of, expand_piecewise
 from math_spec.validation import to_spec
 
 if TYPE_CHECKING:
-    from collections.abc import Callable, Mapping
+    from collections.abc import Callable
     from pathlib import Path
     from typing import Any
 
@@ -78,32 +77,11 @@ def to_program(spec: str | Path | dict[str, Any] | Spec | program.Program) -> pr
     Raises:
         SchemaError: The file is not a valid model.
         LanguageError: A construct outside the language, named with its
-            rewrite, or a file that reads variables it does not introduce.
+            rewrite.
     """
     if isinstance(spec, program.Program):
         return spec
-    schema = to_spec(spec)
-    if schema.given_variables:
-        raise LanguageError(_unintroduced_message(schema.given_variables))
-    return lower_program(expand_piecewise(schema))
-
-
-def _unintroduced_message(given: Mapping[str, Any]) -> str:
-    """The refusal for lowering a fragment, which is a model no build can finish.
-
-    A program is what a consumer builds and solves, so every column in one is a
-    column something introduces. A fragment states the opposite about some of
-    its own, which is why it is composed before it is lowered — and why it
-    still loads and still prints, both of which read the model rather than
-    build it.
-    """
-    named = ', '.join(f"'{name}'" for name in sorted(given))
-    noun = 'a variable' if len(given) == 1 else 'variables'
-    return (
-        f'this file reads {noun} it does not introduce: {named}. A program builds every column it '
-        f'carries, so compose the file with the ones that declare them first — '
-        f'to_program(merge({{...}})). The file loads and prints on its own either way.'
-    )
+    return lower_program(expand_piecewise(to_spec(spec)))
 
 
 def lower_program(expanded: _ExpandedSpec) -> program.Program:
@@ -187,6 +165,10 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program:
         expressions[name] = program.ExpressionDeclaration(
             _Lowering(expanded, f"named expression '{name}'").expr(ast), in_math=name in resolved.read_by_the_math
         )
+    given_variables = {name: program.GivenDeclaration(tuple(g.dims)) for name, g in expanded.given_variables.items()}
+    given_constraints = {
+        name: program.GivenDeclaration(tuple(g.dims)) for name, g in expanded.given_constraints.items()
+    }
     return program.Program(
         parameters=parameters,
         variables=variables,
@@ -196,6 +178,8 @@ def lower_program(expanded: _ExpandedSpec) -> program.Program:
         sos=sos,
         piecewise={name: declaration_of(ex) for name, ex in expanded.expanded_piecewise.items()},
         named_expressions=expressions,
+        given_variables=given_variables,
+        given_constraints=given_constraints,
     )