feat(language): a file may read variables and constraints it does not declare

[FBumann]

Prompt: "I think we should spike this in mathspec with a draft PR."

Scope was set by two earlier asks in the same conversation: "Let's only care about the linopy add spec stuff", and "What about constraints etc? For dual()?" — the second is why given.constraints exists at all.

Note

The following content was generated by AI.

What this changes

A given: block names the variables and constraints a file reads and does not introduce, so a layer of math can be written against a model that already exists — PyPSA/linopy#954's case, and #302's given: true comment.

given:
  variables:
    p: { foreach: [snapshot, generator] }
  constraints:
    balance: { foreach: [snapshot], sense: "==" }
constraints:
  co2_cap:
    foreach: []
    expression: sum(sum(p * emission_rate, over=generator), over=snapshot) <= cap
expressions:
  price: dual(balance)

There is no PartialSpec. That was the worry on #302, and the block avoids it: a given declaration is complete, so every load-time pass treats it as it treats any other and to_program gains no branch. Two closed block types, each total in its own fields, rather than one type with holes.

A given variable carries foreach, where, domain and absence, and no bounds:. Nothing at load reads a bound, and the owner of the column owns them; a second spelling here would be a second home for one fact. A given constraint carries foreach and sense, and no expression:. sense is required because it fixes the sign of the dual, which is the one thing dual() can read off a row family this file does not build.

Where each fact goes, and why

The line is the one both repos already run on — decided at load stays in the file, decided by whoever holds the data stays with them.

Field	In the file	Because
foreach	required	resolution, dim algebra, sum(by=)
domain	required	degree, SOS, reformulation
where / absence	required if masked	the absence rules; absence: zero already needs a where
bounds	refused	nothing at load needs them, and the model owns the column
sense (constraints)	required	a dual read against the wrong sense is a wrong number, not an error
expression (constraints)	refused	nothing here builds the row

This departs from what #954's description says it checks (dimensions, bounds and domain). Dropping bounds deletes a whole class of bind-time comparison, and an array-valued bound usually cannot be restated in YAML anyway — that the column already exists is the premise. The cost is honest: boundedness.advice reads lower/upper, so a given variable is exempt from the runs-to-infinity note.

How it prints

A Given section, last, beside the variable domains: both say what a symbol is rather than what the model asks of it. A given variable prints its domain like any other; a given row family prints as the one thing the file may do with it.

\mathit{imported}_{t,z} \in \mathbb{R}
\lambda_{\mathrm{import\_limit},t,z} \text{the dual of a given }\le\text{ row}

Printing it first, as a preamble, was the first shape tried. It is the better read, and it breaks tools/notation.py, which reads the objective as the first equation of the document in two places. Making that scanner position-independent is more fragility than the reading is worth here.

What the language does not answer

Whether the bound column has the declared dimensions, coordinates and domain, and whether the bound row family has the declared sense, is a question about the model rather than about the file. That is a consumer's check, and this PR deliberately states none of it. The two traps worth naming for whoever writes the binder:

• Integrality. A MIP has no duals at all, and the base model may carry binaries the layer never saw, so "were duals left?" has to be asked of the whole model rather than of the layer.
• The dual is the layered model's. dual(balance) after a layer is added is balance's shadow price in the model including the layer, not in the base model that was solved earlier. Correct, and surprising; it is stated once on the reference page.

Why

#302 asks for a composition verb and has two incompatible drafts. This is not that. #244 and #250 both produce one mapping validated once, and neither can express a layer over a model that is not a spec at all.

The variable half arguably needs no language change — #954 binds a fully declared variable through its sources entry today. What forces this upstream is the constraint half: dual(balance) cannot name a row family the file does not declare, because resolution has nothing to type and fan_in has no frame to shape against. So the smallest thing that works is a block, and reading duals off a base model is what it buys.

given: true as a flag on variables:/constraints: was the other shape considered. It was rejected because it makes expression: conditionally optional, which is the first place the language would admit an incomplete declaration.

⚠ This asks for a decision on the limits

Please read this before the rest. given: is none of the three kinds limits.md admits — it is not a macro, a primitive or a formulation, and that page says a request that is none of the three is refused. sos: is in the same position and entered anyway, but the taxonomy was never widened to describe it.

This PR widens it, adding a declaration block as a fourth kind. That is a decision, not a paragraph edit, and it is the one thing here that should be settled before anything else in the diff is reviewed.

The adjacent row in the refusals table is "A Python API for building models — the model is the file you review and diff." The argument that given: is not that: a file with a given: block still says all of its own math, in YAML, and still prints; what it does not say is which model supplies the declarations it reads, which is the same category of fact as the numbers behind a parameter. limits.md now makes that argument in two sentences rather than leaving it implicit.

Verified

pytest -q -n 4: 1237 passed, 5 skipped (1205 on the base — 32 new). ruff format --check . and ruff check . clean. prettier --check clean over docs/**/*.md. python -m tools.schema, python -m tools.notation and python -m tests.typesetting.golden regenerate to no diff. mkdocs build --strict builds.

Not run: pyrefly, reuse, typos, taplo, zizmor, and the tectonic half of compile-tex. This environment has no pixi, so the suite ran in a plain 3.12 venv against the same runtime dependencies rather than through pixi run ci.

Two caveats on gates that could not run at the pinned version. mkdocs build --strict needed docs.python.org/objects.inv dropped from mkdocs.yml, which this environment's proxy refuses with a 403; that affects cross-links into CPython's docs and nothing in this diff. And prettier --check fails on mkdocs.yml on a pristine tree with the version available here (3.8.1), so the one added nav line is all this PR changes in that file — it is not reformatted.

The CI failure this PR earned

The first push went red on test_the_golden_model_reaches_every_line_of_the_walk, which asks the golden fixture to render every line of the walk. Nothing in the fixture declared a given: block, so seven lines of the new section printed nowhere.

The claim was the problem, not the code. The first run reported "1234 passed, 6 skipped" and I did not read what the six were: that guard is pytest.importorskip('coverage'), and the venv had no coverage. It skipped silently and I reported a green suite. The fixture now reads a column and a row family it does not introduce, and the coverage script asks for each given declaration's own line as it already asks for a constraint's. The suite above runs with coverage installed; the five remaining skips are typst, a dev dependency absent here.

Mutation table

Each guard deleted in turn on a clean tree, __pycache__ dropped on both sides, restored through git checkout --, tree verified clean at the end. Re-run in full after the fix above.

Every guard, and what caught it

Mutation	Result
a given row family is also built here, not refused	1 failed
a given column keeps whichever bounds the folded block had	1 failed
the given flag is never set, so a consumer cannot tell a bound column from a built one	7 failed
a given variable is not in the namespace an expression resolves against	31 failed, 4 errors
a given row family is not in the namespace dual() resolves against	32 failed, 4 errors
a given variable's frame is not read by the dim checker	64 failed
a given row family's frame is not read for its dual	52 failed
a given variable's where is never resolved	36 failed, 4 errors
a given variable's where dims are not checked against its frame	3 failed
a given frame over an undeclared dimension is not checked	1 failed
a name both introduced and given is not a collision	1 failed
a given entry nothing reads is not advised	7 failed
a dimension only a given row family reaches counts as unreached	1 failed
a given declaration name is not held to being a name	1 failed
a given block does not print	8 failed
restored	all green

One guard survived the first pass — the one that keeps a dimension only a given constraint indexes out of the never-an-axis advice. The layer fixture reached those dimensions through its given variable too, so nothing tested the constraint path. test_a_dimension_only_a_given_row_family_indexes_is_in_use is the purpose-built probe, and the row above is with it in place.

Deliberately not done

• No binder, and no bind-time checking. This repository has no model to bind against. The five checks a consumer needs — the declaration exists, dims agree by name, coordinates agree per dim, domain or sense agrees, and the mask may only narrow — are #954's.
• No given objective. A second objective over a model that already has one stays refused until someone brings the case.
• A given variable cannot gate a piecewise: block. piecewise.py still reads schema.variables, so activity: must name a column this file introduces. The refusal is correct; the message will read oddly for a file that did declare the name under given:.
• No where: on a given constraint. Whether a layer should be able to narrow which rows of a given family it reads the dual of is open; foreach and sense are what dual() needs today.
• Nothing about merge/override. shared math has no composition verb, so a component library ships as generated YAML or a script #302's verb question is untouched, and neither draft is blocked by this.

Departures from Part 2

The advice pass gained a third kind (given-never-read), so ADVICE_KINDS grew and test_advice.py's two assertions on the closed set moved with it — that coverage did not go away, it now pins three kinds instead of two. test_nothing_the_model_is_given_prints_italic reads every_variable rather than variables, for the same reason Symbols does: a given column is one the solver chooses, so it prints italic.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PUHW3akHVBCsuSjCXxf4Sf

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34494684 | 📁 Comparing 4ab5508 against latest (d64e5da)

  🔍 Preview build  

16 files changed · + 1 added · ± 15 modified

+ Added

• reference/language/given/index.html

± Modified

• index.html
• about/limits/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/language/file/index.html
• reference/math_spec/advice/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/errors/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/model/index.html
• and 5 more...

[FBumann]

@FabianHofmann I tried to come up with a solution for the partial stuff that doesnt produce a ton of problems.

Maybe take a look of you like this.
Not finished. Not keeping it open, as i think its not a good idea for the spec in general...