trace (L005, BOLT-LAW-5) checks one direction: every Law-cell entry must be a real law carrying the row's tag. It doesn't check the other direction: a law tagged # <ID> whose row's Law cell doesn't name it. That goes unreported, for proved and pending rows alike.
Reproduction
On shake main (1b39897), using bolt at ada294e:
- drop
src/LAWS.bend pos_binds from SHAKE-PARSE-2's Law cell (a pending row), and
- drop
src/LAWS.bend raw_refused from SHAKE-TOK-4's Law cell (a proved row).
Both laws keep their tags. bolt still reports 0 errors.
This came up for real during shake's rollout. A cell-editing script missed two pending rows' new laws, and I only caught it with a separate cross-check script.
Why it matters
The Law cell is how a reader of SPEC.md learns what backs a row, pending or proved. A tagged law missing from it means:
- a pending row's "proved so far" is understated;
- a proved row's evidence list is incomplete;
- the tag, which is supposed to be the checked link, points at a row that doesn't point back.
Proposal
Add to BOLT-LAW-5's list of defects:
for each law with a tag naming a Proved row, proved or pending, one finding when that row's Law cell has no entry for the law.
Report it at the law's tag line, as for a tag naming an unknown ID. This is a behavior change to BOLT-LAW-5: the "and nothing else" clause grows by one item.
trace(L005, BOLT-LAW-5) checks one direction: every Law-cell entry must be a real law carrying the row's tag. It doesn't check the other direction: a law tagged# <ID>whose row's Law cell doesn't name it. That goes unreported, for proved and pending rows alike.Reproduction
On shake
main(1b39897), using bolt atada294e:src/LAWS.bend pos_bindsfrom SHAKE-PARSE-2's Law cell (a pending row), andsrc/LAWS.bend raw_refusedfrom SHAKE-TOK-4's Law cell (a proved row).Both laws keep their tags. bolt still reports
0 errors.This came up for real during shake's rollout. A cell-editing script missed two pending rows' new laws, and I only caught it with a separate cross-check script.
Why it matters
The Law cell is how a reader of SPEC.md learns what backs a row, pending or proved. A tagged law missing from it means:
Proposal
Add to BOLT-LAW-5's list of defects:
Report it at the law's tag line, as for a tag naming an unknown ID. This is a behavior change to BOLT-LAW-5: the "and nothing else" clause grows by one item.