test: classes of undriven path in the persisted-field contract harness #379

Open
opened 2026-08-23 22:45:08 +02:00 by clawbot · 1 comment
Collaborator

Split out of #366 by the scope ruling at #366 (comment). Deliberately outside milestone 1.0.0.

tests/persistedFieldContract.test.js proves each persisted field's floor by driving hostile values through a real popup boot. Four review rounds established that it cannot, by iteration, support a universal claim of the form "any field a restorable view dereferences on render turns the suite red" — proving that is exhaustive verification of the popup. That PR therefore narrows its claim to what is actually driven; this issue collects what is not.

Known undriven classes, each established by execution

  1. A views:-restricted polarity. The both polarities of every swept field are driven guard counts hostileRestore values toward a row's polarity, but such an entry may carry views: [...] and be driven onto only those views, while hostile/falsy are driven onto all of them. A future row could satisfy the guard with a polarity that reaches a single renderer. No current row does — the only views-restricted entries are viewData's, and viewData is neverFalsy so the guard never consults them. Narrow fix: require the polarity to come from hostile/falsy only.

  2. A mix of polarities across two fields. One boot puts every corrupted field on the same slot, so a branch reached only when one swept field is truthy and another falsy is not entered. Documented as a limit in that PR.

  3. Anything no stored record reaches by itself — a view only forward navigation opens, and anything behind a click. Also documented.

Why this is not urgent

The floors themselves are verified, and the harness does catch what it claims after #366's assertion fix. This is about extending coverage, not repairing a false guarantee — the guarantee is now stated accurately.

Note for whoever takes it: the recurring lesson from those four rounds is that widening the harness to support a broader claim produced a new hole every time. Prefer extending coverage in bounded, provable increments over restating a universal.

Definition of done

  • Class 1 closed — the polarity guard cannot be satisfied by a single-view value.
  • Classes 2 and 3 each either driven, or restated in the harness's own documentation with what replaced them.
  • Every claim added or changed is verified against the harness as built before it is written.
  • Runtime stays inside the script/test cap; say what it costs.
  • make check green.
Split out of https://git.eeqj.de/sneak/AutistMask/pulls/366 by the scope ruling at https://git.eeqj.de/sneak/AutistMask/pulls/366#issuecomment-69432. Deliberately outside milestone 1.0.0. `tests/persistedFieldContract.test.js` proves each persisted field's floor by driving hostile values through a real popup boot. Four review rounds established that it cannot, by iteration, support a universal claim of the form "any field a restorable view dereferences on render turns the suite red" — proving that is exhaustive verification of the popup. That PR therefore narrows its claim to what is actually driven; this issue collects what is not. ## Known undriven classes, each established by execution 1. **A `views:`-restricted polarity.** The `both polarities of every swept field are driven` guard counts `hostileRestore` values toward a row's polarity, but such an entry may carry `views: [...]` and be driven onto only those views, while `hostile`/`falsy` are driven onto all of them. A future row could satisfy the guard with a polarity that reaches a single renderer. No current row does — the only views-restricted entries are `viewData`'s, and `viewData` is `neverFalsy` so the guard never consults them. Narrow fix: require the polarity to come from `hostile`/`falsy` only. 2. **A mix of polarities across two fields.** One boot puts every corrupted field on the same slot, so a branch reached only when one swept field is truthy and another falsy is not entered. Documented as a limit in that PR. 3. **Anything no stored record reaches by itself** — a view only forward navigation opens, and anything behind a click. Also documented. ## Why this is not urgent The floors themselves are verified, and the harness does catch what it claims after https://git.eeqj.de/sneak/AutistMask/pulls/366's assertion fix. This is about extending coverage, not repairing a false guarantee — the guarantee is now stated accurately. Note for whoever takes it: the recurring lesson from those four rounds is that widening the harness to support a broader claim produced a new hole every time. Prefer extending coverage in bounded, provable increments over restating a universal. ## Definition of done - [ ] Class 1 closed — the polarity guard cannot be satisfied by a single-view value. - [ ] Classes 2 and 3 each either driven, or restated in the harness's own documentation with what replaced them. - [ ] Every claim added or changed is verified against the harness as built before it is written. - [ ] Runtime stays inside the `script/test` cap; say what it costs. - [ ] `make check` green.
Author
Collaborator

Fourth class, found by the final review of #366 (#366 (comment)) and deliberately kept off that PR under the scope ruling.

4. Boots held only to HEALTHY rather than RESTORED can fall back off-view. a hostile routing value restoring onto and a restore-only hostile value onto assert health, not that the boot landed on the view it stored. Such a boot can fall back, so the target view's renderer never runs and the boot passes anyway.

Nothing hides today: the combined sweep drives every restorable renderer with WELL_FORMED_DATA and asserts RESTORED. But a hostileRestore entry aimed at a specific renderer can silently stop reaching it if a guard later widens — the value would still be driven, and the assertion would still pass, while the renderer it was written for was never entered.

Narrow fix: require such entries to declare whether the boot is expected to land on the view, and assert that.

Also worth carrying into this issue: the final review flagged two calibration notes on the narrowed claim in #366, neither a defect. README.md and the test-file header phrase the in-boundary verdict as "unhealthy or off the view it stored", which is exactly true of the combined sweep the sentence names but would be too broad if read across every boot in the file; and "everything a healthy profile reaches" is listed as undriven when the base profile the sweep corrupts does boot a healthy profile onto all eleven restorable views. The second understates coverage, which is the safe direction. Tighten both if that wording is ever edited again.

Fourth class, found by the final review of https://git.eeqj.de/sneak/AutistMask/pulls/366 (https://git.eeqj.de/sneak/AutistMask/pulls/366#issuecomment-69439) and deliberately kept off that PR under the scope ruling. **4. Boots held only to `HEALTHY` rather than `RESTORED` can fall back off-view.** `a hostile routing value restoring onto` and `a restore-only hostile value onto` assert health, not that the boot landed on the view it stored. Such a boot can fall back, so the target view's renderer never runs and the boot passes anyway. Nothing hides today: the combined sweep drives every restorable renderer with `WELL_FORMED_DATA` and asserts `RESTORED`. But a `hostileRestore` entry aimed at a specific renderer can silently stop reaching it if a guard later widens — the value would still be driven, and the assertion would still pass, while the renderer it was written for was never entered. Narrow fix: require such entries to declare whether the boot is expected to land on the view, and assert that. Also worth carrying into this issue: the final review flagged two calibration notes on the narrowed claim in https://git.eeqj.de/sneak/AutistMask/pulls/366, neither a defect. `README.md` and the test-file header phrase the in-boundary verdict as "unhealthy **or off the view it stored**", which is exactly true of the combined sweep the sentence names but would be too broad if read across every boot in the file; and "everything a healthy profile reaches" is listed as undriven when `the base profile the sweep corrupts` does boot a healthy profile onto all eleven restorable views. The second understates coverage, which is the safe direction. Tighten both if that wording is ever edited again.
Sign in to join this conversation.
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: sneak/AutistMask#379