[FBumann]

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

Note

The following content was generated by AI.

Program.reads maps each refused parameter to a mask over its dims that holds exactly where the model reads it. A tool evaluates it at attach, like a where, and refuses missing rows before building anything. TranslatedPredicate becomes WindowPredicate.

Stacked on #880, whose contract this states as data.

How the mask is built

mathspec/reads.py runs three walks over the program.

• Two walks run bottom-up, each over a node's own frame. present is where absence has not removed the value. live is where the value still carries a variable term, since a row with none is not built.
• One walk runs top-down. read is where a node's value goes into the model, starting at each built row, each bound of an existing variable, the objective and each reported expression. Each operator hands read to its operand in the opposite direction:
  • A shift back by k becomes a window ahead by k.
  • sum_back becomes a window ahead of the same width.
  • A lookup at() becomes the sum(by=) that inverts it, and sum(by=) becomes the lookup. Both use Join with the columns swapped.
  • A summand also needs its own presence.
• A bare bool flag in a where follows feat(language)!: a missing row is refused only where the model reads it, a file names its value instead of neutral, and the program says where each parameter is read #880. It is read wherever the model evaluates that where, which is wider than where it reads: a row's where is evaluated at every coordinate. So the top-down walk carries a second mask, evaluated, down to each case's when, and a walk over each mask passes it to the flags under count, shift and at.

Every node in a mask is one a tool already evaluates, except one: WindowPredicate replaces TranslatedPredicate. It holds where its 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 (offset=-1 loads as "ahead by 1"). Only program.reads writes a wider window, or one that looks ahead by a named offset. 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: first draft put 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. One window predicate in the closed predicate set makes each walker grow a branch.

Verification

Differential oracle. tests/test_reads.py holds an oracle that shares no code with reads.py. It builds the rows of 26 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 reported expression, or an evaluated where reads. Each mask is evaluated on the same data and must hold at exactly those coordinates. 26 models × 12 draws = 312 cases. The data is sparse, so most masks hold on a strict subset: for example 10 of 20 coordinates for a flag in a case, and 16 of 20 for a shifted flag.

The oracle caught one real bug during the work: a read through at() dropped the dimensions of the row beyond the node's frame, so the projection did not sum over t.

Mutation table. Each guard was deleted by hand. The oracle suite was run, the file was restored through git checkout -- with __pycache__ dropped on both sides, and the tree came back clean each time. Three deletions first survived; each got a model that catches it.

Guard deleted	Caught by
a row needs a variable term	22 cases
a row needs both sides present	34
a row needs its where	12, after adding a-masked-row
a summand needs to be present	30
a shift is read from the other side	44
a window is read ahead	15
a join keeps the dims of the read	12
a filled shift is present where it vacates	6
an absent parameter can be missing	11
a variable read as a number is present	12, after s <= p became s + y <= p
a case is read only in its region	12
a bound is read where its variable exists	13
a join is read back with its columns swapped	8
a named offset is read	12
a named width is read	12
a flag is recorded	59
only a bool name reads	12, by a-guard-reads-no-number
a when is read where the case is evaluated	11, after the case model read the masked x
a flag shifted in a where is read from the other side	12
a flag through a map is read back	5
a case below is found	11
a constraint's where is evaluated	24
a variable's where is evaluated	24
a counted flag is read at every position	12

On the examples. program.reads computes for every spec in examples/. The full pypsa.yaml gets 188 masks in 0.33 s, one run, not measured on an idle machine.

Gates. pixi run lint and pixi run test pass (3178 passed, 1 skipped). tests/test_reading_page.py runs the new example on reading.md. 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 yet. specsolve and its linopy backend need the rename, the wider window, and to evaluate program.reads at attach. That is their own PRs.
• A curve still under piecewise: is not counted, as for footprint. Ask the program of spec.expand('piecewise'). specsolve already requires the expansion.
• Assumptions are checks, not reads, so a flag only in assumptions: is not in a mask.
• The masks are not simplified beyond folding literals and dropping a repeated conjunct, so some carry a redundant ∃.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AvtZGymCbY9swLnR8JwHng

---

Generated by Claude Code

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35165347 | 📁 Comparing e58e989 against latest (b161e41)

  🔍 Preview build  

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

+ Added

• reference/language/declarations/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/parameters-variables-constraints/index.html

[FBumann]

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

Note

The following content was generated by AI.

Closed in favour of #880. #880's branch was fast-forwarded to carry every commit of this PR, and it now has one description and one changelog line for both changes.

---

Generated by Claude Code