From 5ec2ce0bbd048c2733842e1bfc1190c584b645b3 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 18:32:22 +0200 Subject: [PATCH] S16: ratification round 1 -- pin 5 gains a permanent regression test MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First independent round against the draft as a whole rather than against the previous revision's edits. One blocking finding, and it is one that ten revisions of amendment review did not surface. Pin 5's staff-undo repair was signed by M5 alone. No named test performed CreateStaffGroup(g, []) -> CreateStaff(s, group: Some(g)) -> undo the staff -> assert the still-live g.members no longer holds s. Verified that nothing existing supplies it: - Pin 8's four tests are group-undo guards. u2tomb_a (reduce.rs:17125) does undo a staff, but its assertions are that the undo tombstones the referencer, that T1's undo then proceeds, and that "the group leaves Score.staff_groups" (:17187) -- it undoes the group too, so no live group's members is ever inspected. - Gate 6's m41/m41b build materialized fixtures and never run the reducer's undo path. Pin 5a adds u5_undoing_a_staff_strips_it_from_the_live_groups_members with three assertions: the group is still live (without which the test can pass vacuously on a score where the group was undone too -- exactly how u2tomb_a misses this path), g.members lacks s by id, and check_invariants reports no StaffGroupMembershipAgreement violation. Gate 13 runs it. §6 item 2f reports it. M5 now breaks it by name and reports the changed state -- the post-undo g.members still containing s, with the invariant-21 witness -- rather than stating a condition. The finding is revision C's, on the sibling pin. Revision C established pin 3a's rule that a mutation demonstrates the hazard once and only a test keeps it demonstrated, and applied it to pin 6 and M6. Pin 5 and M5 have the identical shape and were left alone, two paragraphs from the sentence "pin 6 is coupled to pin 5 and they split only together." So the lesson is not "check mutations for permanent tests" -- that was already learned. It is that a coupling stated in prose does not propagate a fix. Every fix-propagation failure in revisions A-J was a correction reaching a CONSUMER one hop late; this one failed to reach a declared PEER. Why ten revisions missed it: each reviewed the previous revision's edits, so the question asked was always "is this change right?", never "is anything else the same shape?" A first whole-artifact round asks the second question. Swept the other mutations for the same shape: M1/M2 break t8b, M3/M4 break t8c/t8d via pins 3a/4a and gate 9, M6 breaks m41/m41b, M7a/M7b break the two grep guards, M9 uses t7, and M8's structural gate 8 is explicitly the only signature available for a deletion no behaviour observes. M5 was the only gap. Also fixed before commit: gate 13 was first inserted before gate 12. Still DRAFT, still unratified. No implementation work has begun. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x --- spec/CONTRACT_P13S16_PROJECTION.md | 90 +++++++++++++++++++++++++++++- 1 file changed, 88 insertions(+), 2 deletions(-) diff --git a/spec/CONTRACT_P13S16_PROJECTION.md b/spec/CONTRACT_P13S16_PROJECTION.md index 2286d80..39dc8bd 100644 --- a/spec/CONTRACT_P13S16_PROJECTION.md +++ b/spec/CONTRACT_P13S16_PROJECTION.md @@ -277,6 +277,34 @@ three revised tests, pin 8's four G3a tests — is read off, not restated, and a the set edits the table and the adjacent word together. **The defect is a count living away from the set it counts.** +### RATIFICATION ROUND 1 — independent, against `253249e`. One blocking finding. + +**This is the first round against the draft as a whole rather than against the previous +revision's edits**, and it found a gap ten revisions of amendment review had not: **pin +5's repair had no permanent regression test.** + +| # | Finding | Disposition | +|---|---|---| +| **1** | **Pin 5 was signed by M5 alone.** No named test performed `CreateStaffGroup(g, [])` → `CreateStaff(s, group: Some(g))` → **undo the staff** → assert the still-live `g.members` no longer holds `s`. **Pin 8's four are group-undo guards** — `u2tomb_a` undoes a staff but asserts *"the group leaves `Score.staff_groups`"*, so **no live group's members is ever inspected**; and gate 6's `m41`/`m41b` build **materialized fixtures**, never running the reducer's undo path | **Pin 5a** adds `u5_undoing_a_staff_strips_it_from_the_live_groups_members` with three assertions — group still live, `members` lacks `s`, no invariant-21 violation. **Gate 13** runs it; **§6 item 2f** reports it; **M5 now breaks it by name and reports the changed `g.members` state** rather than a condition | + +**The finding is revision C's, on the sibling pin.** Revision C established that *a +mutation demonstrates the hazard once; only a test keeps it demonstrated* — pin 3a's own +words — and applied it to **pin 6 and M6**. Pin 5 and M5 have the identical shape and were +left alone, **two paragraphs from the sentence "pin 6 is coupled to pin 5 and they split +only together."** + +**So the lesson is not "check mutations for permanent tests" — that was already learned. +It is that a coupling stated in prose does not propagate a fix.** When two pins are +declared to stand or fall together, a correction to one is a correction owed to the +other, and nothing in this document made that automatic. **Every fix-propagation failure +recorded in revisions A–J was a correction reaching a *consumer* one hop late; this one +failed to reach a declared *peer*.** + +**Why ten revisions missed it:** each reviewed the previous revision's edits, so the +question asked was always *"is this change right?"* — never *"is anything else the same +shape?"* A first whole-artifact round asks the second question, which is the argument for +running one before ratification rather than after. + **The pattern across revisions A–J is sharper than any individual finding: a correction propagates one hop and stops.** Rev A fixed pin 10a and left touch row 11; the sweep caught row 11 and stopped before §6's consumer; rev D found pin 10a's *decision* still @@ -683,6 +711,41 @@ held — wherever else the projection lives. The `StaffGroup` arm (`:2977`) need no change: `:6736`'s reference guard already blocks undoing a group a live staff names. +**Pin 5a — a permanent named regression test for the staff-undo strip. ADDED IN +RATIFICATION ROUND 1.** + +Pin 5's repair was signed by **M5 alone**, and a mutation is reverted. Add to +`crates/epiphany-ops/src/reduce.rs`, named **exactly**: + +``` +u5_undoing_a_staff_strips_it_from_the_live_groups_members +``` + +**Sequence — the one the pin repairs, end to end:** `CreateStaffGroup(g, [])` → +`CreateStaff(s, group: Some(g))` → **undo the `CreateStaff`** → then assert, on the +materialized graph: + +1. **`g` is still live** in `Score.staff_groups` — if the group is gone there is no + projection left to be wrong, and the test asserts nothing; +2. **`g.members` does not contain `s`**, quoted by id; +3. **`check_invariants` reports no `StaffGroupMembershipAgreement` violation** — the + exactness form pin 6a uses, so the test fails on a residue whichever direction it + leaves. + +> **Why the existing tests do not supply this, checked rather than assumed.** Pin 8's +> four are **group-undo guards**: `u2tomb_a` (`:17125`) undoes a staff, but its +> assertions are that the undo tombstones the referencer, that T1's undo then proceeds, +> and that *"the group leaves `Score.staff_groups`"* (`:17187`) — **it undoes the group +> too, so no live group's `members` is ever inspected.** Gate 6's `m41`/`m41b` build +> **materialized fixtures** and never run the reducer's undo path. **So nothing +> permanent exercised the sequence pin 5 exists for.** +> +> **This is pin 3a's rule — *a mutation demonstrates the hazard once; only a test keeps +> it demonstrated* — and revision C applied it to pin 6/M6 and not to pin 5/M5.** The +> contract states two paragraphs below that **"pin 6 is coupled to pin 5 and they split +> only together"**; their evidence models were nonetheless fixed one at a time. **A +> coupling stated in prose is not a coupling applied.** + **Pin 6 — graph invariant 21, `StaffGroupMembershipAgreement`.** Flags both directions: a staff whose `group` names a group whose `members` omit it, and a group listing a staff whose own `group` is not that group. Witnesses @@ -1193,8 +1256,19 @@ pin 1's refusal behind `self.graph.is_some()` and confirm that arm reverts to applying. Signs that the empty-container precondition is deliberately universe-independent. -**M5 — the undo hole is closed.** Remove pin 5's strip; undoing a `CreateStaff` -must leave a disagreeing pair that invariant 21 flags. +**M5 — the undo hole is closed. BOUND TO A NAMED TEST IN RATIFICATION ROUND 1.** +Remove pin 5's strip. **Required:** + +- **`u5_undoing_a_staff_strips_it_from_the_live_groups_members` (pin 5a) must fail**, and +- **the changed state must be reported, not the failure**: quote `g.members` after the + undo — showing it still contains `s` — and quote the + `StaffGroupMembershipAgreement` violation `check_invariants` then returns, with its + witness ids. + +*(M5 previously required only that undoing a `CreateStaff` "leave a disagreeing pair that +invariant 21 flags" — an observation with **no permanent test to break**, and phrased as +a condition rather than a named artifact. Both halves are fixed: pin 5a supplies the +test, and the observation now names the state.)* **M6 — invariant 21 sees both directions. FIXTURES MUST ISOLATE, tightened on review.** Delete each arm in turn; each deletion must leave a distinct disagreeing fixture @@ -1440,6 +1514,13 @@ weakening is invisible. > and this gate and M6 both use them. If the implementation chose other names, **that > is the finding** — the gate has not "passed with zero matches", it has failed. +13. **Pin 5a's undo regression test runs and passes — ADDED IN RATIFICATION ROUND 1.** + `u5_undoing_a_staff_strips_it_from_the_live_groups_members`, by name, with its three + assertions **quoted from source** and its pass verdict — gate 6's evidence model. + **Confirm assertion 1 is present**: without the still-live check the test can pass + vacuously on a score where the group was undone too, which is exactly how the + existing `u2tomb_a` fails to cover this path. + --- ## §4a. Landing obligation — files that must NOT be staged, and must be fixed after @@ -1534,6 +1615,11 @@ its evidence at `invariants.rs:69`–`:71` must stay intact. *(Earlier still, this item asked whether `shrink` matches `GraphInvariant` exhaustively — a **static fact the draft could read**: it does not, it calls `check_invariant(score, inv)`.)* +2f. **Pin 5a's `u5_undoing_a_staff_strips_it_from_the_live_groups_members`** — its three + assertions quoted from source and its pass verdict, **and M5's observed state**: the + post-undo `g.members` still containing `s`, with the invariant-21 witness. **ADDED IN + RATIFICATION ROUND 1**, which found pin 5 signed by a mutation and by no permanent + test. 2e. **The three invariant-21 tests' verdicts** — `m41`, `m41b`, and `invariant_21_negative_generator_breaks_staff_to_group_only` — **each with its exact-set and direction assertions quoted from source**, per gate 6's evidence model,