Docs: the width guard reads the representation the law compared (improvise-btyw)

This commit is contained in:
Edward Langley
2026-09-22 23:34:45 -07:00
parent e2b132f594
commit 83c3c7d392
2 changed files with 32 additions and 7 deletions
+16 -6
View File
@@ -3307,10 +3307,19 @@ the whole slice of records under that item, not one record picked by name. In
the demo that is four records and eight cells for each of the eight drills. With
the store's sort removed, the law fails 400 of 400 runs.
**The width guard measures what the comparison compared (improvise-b9f2).** The
test asserts that some `drill-into-cell` the comparison actually built and
compared froze at least four records. For each one it applies those very effects
to one scratch `App` and counts the records in its `drill_state`. A first
**The width guard measures what the comparison compared (improvise-b9f2,
improvise-btyw).** The test asserts that some `drill-into-cell` the comparison
actually built and compared froze at least four records. For each one it applies
those very effects to one scratch `App` and counts the records in its
`drill_state`. It counts them only when their `Debug` text, which carries their
order, appears in the text the comparison compared. The comparison reads `Debug`
while the scratch `App` reads the applied state, and those are two
representations. The review showed they can disagree: give `StartDrill` a
`Debug` that prints only a row count, and the frozen records are still four
while the compared text no longer holds their order. With the store's sort
removed the law then passed 300 of 300 runs, with the guard green. Requiring
the ordered records in the compared text ties the guard to what the comparison
could actually see. A first
version measured what the *argument lists* match in the store instead. That was
a parallel derivation, and the review beat it with a `drill-into-cell` parser
that refuses fewer than two arguments. Every one-coordinate drill then went to
@@ -3323,8 +3332,9 @@ Counting frozen records is not enough by itself. A drill over no coordinates
never through the narrowing index where gotcha 18 lives. Under the parser rival
that whole-store drill still froze 16 records, and a guard counting it stayed
silent. So only a drill that **narrowed** the store counts: one that froze fewer
records than the store holds. With the rival in place, the guard now fires on
every run ("froze 1 records").
records than the store holds. With the parser rival in place, the guard fires on
every run ("froze 1 records"), and it fires on every run under the `Debug` rival
too ("froze 0 records").
What the guard still cannot see is a narrowing drill whose records are frozen in
an order that does not come from the store. It checks that the law had a wide
+16 -1
View File
@@ -5388,13 +5388,28 @@ rivals it catches:
and it reads them in insertion order through `iter_cells`, which the
injection cannot reach. So the guard counts only drills that froze fewer
records than the store holds.
- Measured on the final form, test binary in a loop:
- Measured at `7dfa90f1`, test binary in a loop:
| Faults | Law passes | Guard fired |
|---|---|---|
| gotcha 18 + parser rival | **0 of 300** | all 300 |
| gotcha 18 alone | **0 of 300** | 0 (every failure a real divergence) |
| neither | 300 of 300 | 0 |
- **`StartDrill`'s `Debug` changed to print only its row count**
(`StartDrill(4 rows)`, improvise-btyw): the law compares effects by their
`Debug` text, and this rival takes the record order out of that text, while
the frozen `drill_state` still holds four records. At `7dfa90f1`, with gotcha
18 re-injected, the law **passed 200 of 200** runs and the guard stayed green.
The guard now counts a drill only when its frozen records, as `Debug` prints
them, appear in the text the comparison compared. The same measurements after
the repair, 200 runs each:
| Faults | Law passes | Guard fired |
|---|---|---|
| gotcha 18 + `Debug` rival | **0 of 200** | all 200 ("froze 0 records") |
| gotcha 18 + parser rival | **0 of 200** | all 200 |
| gotcha 18 alone | **0 of 200** | 0 (every failure a real divergence) |
| neither | 200 of 200 | 0 |
- **A stale exemption**: `("quit", "stale")` listed in `OUTSIDE_THE_CONTEXT`.
It fails as "listed … but did not".