[FBumann]

Prompt: Lets do it — And we need to document the now more less ambigouos behaviour and cotract!

Prompt: Can mathspec provide sth in the Program so specsolve can refuse right at attach?

Prompt: Should we combine them into one PR? With one description?

Prompt: Yes, go ahead. The decisions are right. I have one correction to the review and four additions.

Note

The following content was generated by AI.

missing: refused now refuses a row only where the model reads it, and Program.reads gives that set as a mask a tool evaluates at attach. neutral is gone: a file writes the value. A masked variable may stand as any number. Imports break: TranslatedPredicate is WindowPredicate.

This PR carries what were #881 and #885. Departure from AGENTS.md: the two halves can be separated, but the contract has no code in mathspec except Program.reads, and its oracle is the only check of the contract, so they are reviewed together.

Contract: where a parameter is read

absence.md has a new section, Where a parameter is read. The model reads a parameter at these coordinates: a row it builds, a summand that exists, a bound of a variable that exists, an offset=/window= amount, the objective, a reported expression, the breakpoints of a curve, and a term with adds_to: a given expression wherever the term is present. A row that an absent term removes reads nothing, and a row with no variable term left is not built.

Inside a where, only a bare bool name reads. A flag such as where: committable is read wherever the model evaluates that where: every coordinate of a variable's or constraint's dims, the when of a case wherever the expression that holds it is evaluated, and the positions that count, shift or at look at. A flag in an assumptions: entry is read at every coordinate of the frame of the assumption. So a missing flag is still refused, as in 0.3.0. Without this rule, 45 bool flags in the PyPSA spec would never be refused.

A comparison and a bare number or label read nothing. A bare number tests whether the row is there, and a comparison at a missing row is false unless missing: names a value. Both sides of AND are evaluated, so if a comparison counted as a read, the guard where: cost AND cost > 0 would refuse the rows it is there to skip. Two str labels in PyPSA are used only in comparisons, so they are not protected.

Two load refusals relied on "a row at every coordinate", so they are removed. This moves a limit: a file may now write both forms.

• a bare int/str name in a where under refused;
• a values table of a curve under points: declared refused. The curve reads no row past its mask.

limits.md never listed either refusal, so it has no line to change.

Readings: refused, absent, or a value

neutral read a missing row as 0 or false. It was named for "contributes nothing", which holds only for an additive term. As a factor it dropped the whole term. As an exponent it gave 1. As an offset= it read the coordinate itself. Its three refusals (divisor, bound, constant side) are now what refused does.

• A parameter takes refused, absent or a value. 'neutral' gets the closed-vocabulary error, which names the valid readings.
• absence.md has a table with one row per position (coefficient or constant, summand, divisor, bound, offset=/window= amount, where comparison, bare flag, bare number or label) and one column per reading. Under absent, a missing amount makes the shift/sum_back absent there.
• A divisor that a missing row of a missing: 0 parameter can make 0 is refused at load. The check walks the whole divisor: a factor, the numerator of a quotient, the base of a power, the operand of a sum, a window, a shift or a lookup, a named expression, any region of a case, and a sum only where every addend can be 0, so c + 1 loads. where: c > 0 beside x / c is still refused: the refusal is strict but sound, and its rewrite (missing: absent) works without a guard.
• A variable takes absent or any finite number. It needs a where:, and the number must fit the variable: 0/1 for binary, an integer for integer, and inside any literal bound. A parameter bound is data, so it is not checked. A curve gate is binary, so it takes 0 (no curve) or 1 (ungated, which is also what absent gives).

One reading changes: a where comparison. Under neutral, a comparison at a missing row was false. A value compares as itself, so cost < 1 becomes true at a missing row under missing: 0. Every comparison on a migrated parameter in examples/ is > 0, which is false both ways. To keep the old reading, write where: cost AND cost < 1.

Migration. examples/, tests/expand/ and the golden fixture use 0 for float/int and false for bool. The divisor refusal caught the PyPSA module sizes: Generator_p_nom_mod divides in *_maint_modstatus_*. Every arithmetic read of the seven *_nom_mod parameters sits inside a *_nom_mod > 0 mask, so they keep the default refused. Regenerated: the schema, the golden output, the gallery and notation pages.

Program.reads, model_trees and WindowPredicate

Program.reads maps each refused parameter to a Mask over its dims that holds where the model reads it. A tool evaluates the mask at attach, as it evaluates a where, and refuses a missing row where it holds. No row needs building first. reading.md documents it with an example the suite runs. On a program that still holds a piecewise: curve, reads raises a LanguageError that names spec.expand('piecewise'), because the rows of the curve do not exist yet.

One list of what goes into the model. model_trees yields every tree whose value goes into the model, with what holds it: both sides of each constraint, the objective, each bound, each curve link and each term. Lowering marks in_math from it, and reads starts its walk from it, matching on the kind with assert_never, so a kind added to the list reaches both. A reported expression and an assumption are not model trees; reads walks them separately.

mathspec/_reads.py builds the masks with three walks.

• Two run bottom-up, each over a node's own frame. present is where absence has not removed the value. live is where a variable term is left.
• One runs top-down. read starts at each model tree. Each operator hands it to its operand in the opposite direction: a shift back by k becomes a window ahead by k, sum_back a window ahead of the same width, a lookup at() the sum(by=) that inverts it, and sum(by=) the lookup, both as a Join with the columns swapped. A summand also needs its own presence.
• Flags: the top-down walk carries a second mask, evaluated, down to each case's when, and a walk over each where and each assumption passes it to the flags under count, shift and at.

WindowPredicate replaces TranslatedPredicate: the operand holds at some position of a window along a dimension, looking back or ahead, with wrap and a partition. A file's predicate shift is a window of one position, and offset=-1 loads as "ahead by 1". Only program.reads writes a wider window, or one that looks ahead by a named offset. Its contract states the normal form:

• a literal offset is 0 or more, and ahead carries the direction;
• a named offset carries its sign in the data, as on Translate;
• a width of 0 or less is an empty window, which holds nothing;
• where a named amount has no row, the window holds nothing; an amount declared with a value reads that value.

A missing named amount therefore makes its operator absent in the masks too: a shift with edge= and a sum_back are present only where the amount has a row. A read through a relation is a Join of an indicator (Cases of 1 and 0) compared > 0, so a missing map row reads as false.

Alternative rejected: reverse and ahead flags on Translate and WindowSum. A default-off flag gives one node two meanings and gets around the assert_never exhaustiveness every walker relies on.

Review fixes

A review of 34cc571 found three wrong masks, a contract gap on named amounts, a zero-divisor refusal that missed most spellings, and cost. Each bug was reproduced before it was fixed: commit c9a44ef7 adds the tests, and on it these fail:

• the oracle models a-term-added-to-a-given-sum (12 of 12 draws), a-flag-in-an-assumption (12 of 12), and a-missing-named-offset-that-wraps (11 of 12), a case the review did not name: a wrapped shift by a named offset folded "present" to true, so a missing offset counted as present;
• test_a_program_that_still_holds_a_curve_says_its_reads_are_not_known;
• test_a_divisor_that_reads_a_missing_row_as_zero_is_refused for -c, 2 * c, c / 2, c ** 2, c + c, sum(c), shift(c) and a named expression standing for c.

The review's finding that a named offset was not recorded as read was wrong: amount() already records it.

Cost, on examples/pypsa.yaml, median of 5 runs, not on an idle machine, before and after the fixes on the same tree: computing reads takes 0.37 s and then 0.26 s. snapshot_weightings_objective had 31 parts with 22 distinct, and now has 22. The masks total 3,588,253 characters of repr and then 3,105,647; the largest is 434,407 characters, because repr writes each shared subtree out again. Connectives are flattened before repeated parts are dropped, and the dims of a predicate are cached by identity.

Verification

Differential oracle. tests/test_reads.py holds an oracle that shares no code with _reads.py. It builds the rows of 32 small models on random data by the absence rules, and records each parameter coordinate that a built row, an existing variable's bound, the objective, a term, a reported expression, an evaluated where or an assumption reads. Each mask is evaluated on the same data and must hold at exactly those coordinates. 32 models × 12 draws = 384 cases. Named offsets and widths are drawn from −1 to 3, so they can be negative, zero, or missing. The data is sparse, so most masks hold on a strict subset. The oracle caught a real bug during the first build: a read through at() dropped the dimensions of the row beyond the node's frame.

Mutation table. Each guard was deleted by hand. The relevant tests were run, the file was restored through git checkout -- with __pycache__ dropped on both sides, and the tree came back clean each time. Rows before the review fixes were taken before the merge of main, which renamed the module and the node classes but changed no logic.

Guard deleted	Caught by
zero divisor: a bare missing: 0 parameter	12 divisor cases
zero divisor: through -, sum, sum_back, shift / a named expression / a factor / a numerator / a base / every addend / a case / a lookup	3 / 1 / 1 / 1 / 1 / 1 / 1 / 1
zero divisor: isinstance(declared.missing, bool)	still green. No file can reach it: false on a numeric parameter is refused. Kept on review request, so that False == 0 can never read as a zero divisor
binary / integer domain check on a variable number	…_outside_what_the_variable_takes_is_refused[binary], [integer]
lower / upper bound check on a variable number	…[below-lower], [above-upper]
finite, not-a-flag check on a variable	test_a_variable_missing_that_reads_data_is_refused[a-flag], [an-infinity]
a row needs a variable term / both sides present / its where	22 / 34 / 12 oracle cases
a summand needs to be present	30
a shift is read from the other side / a window is read ahead	44 / 15
a join keeps the dims of the read / is read back with its columns swapped	12 / 8
a filled shift is present where it vacates	6
an absent parameter can be missing / a variable read as a number is present	11 / 12
a case is read only in its region / a bound where its variable exists	12 / 13
a named offset / width is read	12 / 12
a flag is recorded / only a bool name reads	59 / 12
a when is read where the case is evaluated / a case below is found	11 / 11
a flag shifted in a where / through a map / counted	12 / 5 / 12
a constraint's / variable's where is evaluated	24 / 24
a term is read where it is present / a flag in an assumption is read	12 / 12
a program that holds a curve is refused	1
a missing amount makes a filled shift absent (two branches)	11 / 11
a missing width makes a window absent	11
a named window never folds to true	11

Six deletions first survived and each got a model or a test that catches it: a row needs its where, a variable read as a number is present, only a bool name reads, a when is read where the case is evaluated, a missing amount makes a filled shift absent, and the zero divisor through a case or a lookup.

On the examples. program.reads computes for every spec in examples/; the ones with a curve are expanded first. The full pypsa.yaml has 188 masks. Only its two str labels are never read.

Coverage moved. neutral cases became 0/false cases. an-int-under-neutral, neutral-on-a-label and the neutral exclusivity reading are removed, and their value counterparts stay. The bare-name refusal cases became loading cases. …_under_points_is_not_refused became …_may_be_refused. The reading page no longer shows a mask for an unexpanded curve, because reads raises there.

Gates on 01c80e4: pixi run lint and pixi run test pass (3325 passed, 1 skipped). docs-build stops only on the strict warning for pathlib.Path, because the container's proxy blocks docs.python.org. compile-tex was not run.

Not verified. The oracle does not cover a partition (within=), a Dual in a reported expression, or given parameters. The masks pass a partition through unchanged, so their correctness there depends on WindowPredicate and Join meaning in an engine what they mean on a Translate.

Not done

• No engine evaluates WindowPredicate or program.reads yet. specsolve and its linopy backend need their own PRs: the rename, the wider window, evaluating the masks at attach, and the value forms of missing:.
• x / shift(p, along=t, offset=1, edge=0) divides by the edge= value 0 at the edge whatever missing: says. A check at load could catch it; it is a separate bug.
• A relation's refused still checks every key combination when the data is attached.
• missing: <parameter> on a variable. A named expression with cases: already says "the variable where the mask holds, the data elsewhere".
• The masks share subtrees but are not simplified beyond folding literals and dropping repeated parts, so some carry a redundant ∃.
• The 0.3.0 release notes still name neutral. They are history.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AvtZGymCbY9swLnR8JwHng

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35172353 | 📁 Comparing 01c80e4 against latest (df10096)

  🔍 Preview build  

61 files changed · + 1 added · ± 59 modified · - 1 deleted

+ Added

• reference/language/parameters-variables-constraints/index.html

± Modified

• index.html
• changelog/index.html
• contributing/index.html
• examples/index.html
• first-spec/index.html
• several-files/index.html
• about/limits/index.html
• about/relations-as-linear-maps/index.html
• about/what-counts-as-language/index.html
• about/what-counts-as-public-api/index.html
• and 49 more...

- Deleted

• reference/language/declarations/index.html

[FBumann]

Prompt: And merge 880 and 881 into one PR

Note

The following content was generated by AI.

Closed in favour of #881, which carries every commit of this PR and has one changelog line for both changes.

---

Generated by Claude Code

[FBumann]

Prompt: Could mathspec also statically collect that info about a table from its spec? SO we can check upfront?

Note

The following content was generated by AI.

Two points for the contract, from porting specsolve to 0.3.0 (fluxopt/specsolve#2047):

1. Leave the timing to the tool. "Not done" says tools must move the check from attach to build. The contract only needs the coordinates where a row is required. A table with a row at every coordinate meets any such set, so a tool can accept it at attach and look closer only at a short table.
2. mathspec can publish where each parameter is read, so a tool checks before it builds. Which coordinates are read depends on the data, because masks read data. But the rule that decides it is fixed by the spec. If the program carries that rule per parameter, every tool evaluates the same object at attach, with the machinery it already has for masks. No tool then needs its own read tracking, and the contract can be tested in mathspec.

What the read set is made of, and what it cannot be

For a parameter p, the coordinates read are the union over every place p is read (a read site). Each site contributes: the coordinates where the site exists, mapped onto p's dims.

• Where a site exists is a data-only predicate:
  • A constraint row exists where its where: holds and every term that propagates absence is present. That means each variable's where:, each absent parameter's rows, a shift's edge, and a partial relation's rows.
  • A summand exists where its own factors are present.
  • A bound exists where its variable exists.
  • A curve's breakpoints exist where its points: mask admits them.
  • The objective and a reported expression follow the same rules.
• The map onto p's dims is one of these:
  • identity;
  • a projection, which is ∃ over the dims p lacks, like count(..., over=d) >= 1;
  • a shift by a literal or a named amount;
  • a join through a relation. A lookup at(price, by=zone_of[zone]) reads price at the image of the rows under zone_of.

The image through a relation is a push-forward. As far as I can see, the where grammar has no node for it: a pullback is at(pred, by=...), but the image is not. So the read set should be a program-level object, not a Mask. For example, program.reads[name] could hold a tuple of sites, each with its declaration, its frame, the predicate under which it exists, and its map onto the parameter. Authors never write it; tools only evaluate it.

This also answers the guard idiom without exempting masks: where: cost AND cost > 0 reads cost only where the first conjunct holds, if the site predicate keeps the AND spine in order. A plain capacity > 0 on a lost row could then be refused rather than silently dropping the generator.

---

Generated by Claude Code

[FBumann]

Superseeded by #894