INSTR-01: restore M12 on the leg I generalised past, and measure the clause that had no row

Review found two things this PR asserted about itself that were false. Both are
mine and both are worse than the defect the card was filed for.

⚠️ "NO FIXTURE CAN RESTORE IT, MEASURED BOTH WAYS" WAS NOT TRUE, AND TWO
MEASUREMENTS ARE NOT AN IMPOSSIBILITY PROOF. I deleted M12 - SAFETY-44's
working end-to-end control for the off-roster narrowing - on the argument that
the provenance clause made it unrestorable. The structural claim behind it,
that `run()` builds both snapshots from one state file so "already latched" and
"made by this transition" are incompatible, IS TRUE OF SAME-STEP AND FALSE OF
STAGED: `snapshot_over()` starts the after-leg over the file the BEFORE-leg
wrote, so a transition-made destination is available there. Both arrangements I
measured were same-step shaped. Review found the third.

RESTORED, and it discriminates with all six clauses in:

    staged leg, legacy+shed, shipped     _m12_new = VANISHED unit/shed/sign_tripped
    ...C5 narrowing removed              _m12_new = []          ⚠️ suppressed

⚠️ AND MY FIRST RESTORATION DIDN'T DISCRIMINATE EITHER, for a reason worth
recording: `data.pop(k, False)` RETURNS the value, so shed lost the KEY and
kept the LATCH - `_grade_store_migration()` saw `on_roster_latched`, never
re-armed garage, and there was no transition-made destination. The finding was
reported whether or not C5 existed and the control looked restored. `and False`
is the difference between "the key is gone" and "the LATCH is gone", and only
the second reaches the re-arm this arrangement needs.

⚠️ WHAT ACTUALLY BROKE WAS M12's exit-0 PRECONDITION, NOT M12. A legacy-shaped
fixture is never clean. That precondition is the one SAFETY-44's own commit
called "belt-and-braces, load-bearing only if the exit-0 requirement is ever
relaxed", saying what closed the gap is `_m12_new` BEING A SET DIFFERENCE - and
a stable dirty baseline is fine for a set difference. So I deleted a control on
the strength of a precondition the same commit had already called not
load-bearing. That is removing coverage rather than failing to add it, which is
the worse of the two directions.

⭐ AND THE BARE-KEY CLAUSE HAD NO ROW AT ALL. Review deleted
`k.rsplit("/", 1)[-1] == bare` and the whole 28-file suite stayed GREEN. 5e
mutated five clauses; the comprehension carries more, and this one is
load-bearing: a vanished SAFETY-02 `sign_tripped` was suppressed by a SAFETY-42
`delivery_tripped` on a roster unit - a DIFFERENT FAILSAFE's key. The rule's own
comment says "THE TEST IS NOT 'the name appears somewhere'. It is: the SAME bare
key", and nothing measured that sentence. `unit/*/delivery_tripped` is
machine-read, so it is reachable on any real two-latch store. R7 added; C2 now
flips exactly R7.

All six clause-removals now flip exactly their own row:

    C1 machine_read   -> ['R6-machine-read']    C5 off-roster  -> ['R2-narrowing']
    C2 same bare key  -> ['R7-bare-key']        C6 injectivity -> ['R5-injectivity']
    C3 same value     -> ['R4-value']           C7 provenance  -> ['R3-provenance']

THREE DANGLING CITATIONS TO A CONTROL THIS PR HAD DELETED, one of them in the
shipped tool eight lines below the paragraph condemning exactly that ("a
citation is the worst possible carrier, because it reads as having been
checked"). The tool no longer names a check; it states the property - every
clause has a row, and each removal flips its own.

A STALE SAFETY-44 BLOCK saying both fixes were "REVERTED OUT OF THIS CARD,
because THIS SUITE CANNOT MEASURE EITHER ONE" - describing a tree this PR
replaced. Rewritten as a map of where each clause is now measured. A comment
that outlives its subject is the same defect as a citation that outlives its
check.

AND A SELF-CONTRADICTION about the driver, in the file and in the last commit
message: "THE DRIVER IS WRITTEN INTO THE TREE UNDER TEST" eight lines above
"THE DRIVER GOES IN A TEMPDIR, NOT IN THE TREE". The code does the tempdir; the
first sentence stated the read-only-CI bug the same commit says it fixed, as if
it were the design. It now says the driver IMPORTS the tree and is WRITTEN to a
tempdir.

ONE HOLE REMAINS OPEN AND IS STATED AS UNMEASURED: attribution. `sorted()`
decides which vanished key claims a destination, so a deleted key can sort
first and be named as the one that migrated while the key that really moved is
reported VANISHED. Review measured that `sorted(` -> `list(` leaves the suite
green - every 5e case has at most one candidate, so no row can see ordering.
Still exit 1, so a wrong sentence rather than a hidden loss. Recorded rather
than left looking guarded.

28/28 files pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU

goodwe_controller/test_rehearse.py

@@ -411,41 +411,82 @@ check("...and `phase` is NOT among them, because its value 'idle' IS the "
       "phase" not in _m9_vanished)
 shutil.rmtree(Path(_m9).parent, ignore_errors=True)
 
-# ⚠️ `M12` IS GONE, AND ITS REMOVAL IS THE MOST USEFUL THING THIS CARD FOUND.
+# ⭐ `M12` IS BACK, AND THE CLAIM THAT KILLED IT WAS WRONG.
 #
-# M12 was SAFETY-44's end-to-end control for the off-roster narrowing: a mutant
-# deleted one roster unit's latch key while a sibling held the same value, and
-# it went red when the narrowing was removed. It was a real control. Adding the
-# PROVENANCE clause (C7) disarmed it, and no fixture can restore it:
+# M12 is SAFETY-44's end-to-end control for the off-roster narrowing: a mutant
+# makes one ROSTER unit's latch key vanish while a sibling holds the same
+# value, and it must go red when the narrowing is removed. INSTR-01's first
+# draft DELETED it, on the claim that the provenance clause made it
+# unrestorable and that "NO FIXTURE CAN RESTORE IT, measured both ways".
 #
-#   `state-both-latched.json` has the sibling latched IN ITS OWN RIGHT, so C7
-#   rejects the destination before C5 is ever consulted - the mutation is
-#   reported whether or not C5 exists.
+# ⚠️ TWO MEASUREMENTS ARE NOT AN IMPOSSIBILITY PROOF, AND THIS ONE WAS FALSE.
+# Both arrangements I measured were SAME-STEP shaped, and the structural
+# argument - `run()` builds both snapshots from one state file, so "already
+# latched" and "made by this transition" are incompatible - is TRUE OF
+# SAME-STEP AND FALSE OF STAGED. `snapshot_over()` starts the after-leg over
+# the file the BEFORE-leg wrote, so on the staged leg a transition-made
+# destination is available and the two questions stop being incompatible.
+# Review found the third arrangement I had generalised past.
 #
-#   Making the destination TRANSITION-MADE instead means a flat latch, which
-#   the roster start migrates - and that makes the shipped run dirty, which
-#   breaks M12's own precondition (that the fixture is clean before the
-#   mutation). Measured, both ways.
+# HOW IT WORKS. The fixture is `state-legacy.json` plus a second roster unit
+# already latched. The mutant makes `shed` POP its own latch key and come up
+# untripped - a truer SAFETY-02 loss than the original, which left `tripped`
+# True in memory. On the staged leg, losing shed's latch makes
+# `_grade_store_migration()` fall through `on_roster_latched` and RE-ARM
+# `unit/garage/sign_tripped`, which is absent from `before.data` - so the
+# destination is transition-made and C7 lets it through. The off-roster
+# `inverter-a` litter is present in BOTH snapshots on this leg, so it never
+# vanishes and never claims the destination, and C6 stays out of the way.
 #
-# ⭐ SO THE TWO CLAUSES CANNOT BOTH BE MEASURED END-TO-END BY ONE STORE, AND
-# THAT IS NOT A FIXTURE PROBLEM. `run()` builds both snapshots from ONE state
-# file, so "the destination was already latched" and "the destination was made
-# by this transition" are the same file answering two incompatible questions.
-# It is the structural finding SAFETY-44 hit three times and could only
-# describe; part 5e is the answer to it - `diff()` graded at the level it is
-# written at, one case per clause, where the two questions are two rows.
-#
-# What is NOT lost: the rule is still exercised END-TO-END by part 5, which
-# rehearses a real flat-to-roster switch and asserts the legitimate rename is
-# suppressed and named. That is integration coverage; discrimination lives in
-# 5e.
-#
-# ⚠️ `state-both-latched.json` IS DELETED WITH IT. Nothing referenced it once
-# M12 was gone, and the first draft of this paragraph said it was "kept,
-# because 5e's R2/R3 are derived from the arrangements it represents" - which
-# is a nice sentence and not a reference. 5e's rows are dicts in this file.
-# An unused fixture that a comment claims is load-bearing is the same defect as
-# an inert check, one directory over.
+# ⚠️ AND WHAT ACTUALLY BROKE WAS THE PRECONDITION, NOT THE CONTROL. M12's
+# `exit == EXIT_OK` baseline does not survive a legacy-shaped fixture. That
+# precondition is the one SAFETY-44's own commit called "belt-and-braces,
+# load-bearing only if the exit-0 requirement is ever relaxed", saying that
+# what closed the first draft's gap is `_m12_new` BEING A SET DIFFERENCE. A
+# stable dirty baseline is fine for a set difference. So the control was
+# deleted on the strength of a precondition the same commit had already
+# characterised as not load-bearing - which is a worse mistake than the
+# original inert check, because it removed coverage rather than failing to add
+# it.
+_M12_OLD = 'tripped=bool(data.get(self.key("sign_tripped"), False)),'
+# ⚠️ THE MUTANT POPS **AND COMES UP UNTRIPPED**, which is the whole point and
+# which the first draft got wrong: `data.pop(k, False)` RETURNS the value, so
+# shed stayed latched in memory, `_grade_store_migration()` saw
+# `on_roster_latched` and never re-armed garage - no transition-made
+# destination, and the finding was reported whether or not C5 existed. The
+# control looked restored and discriminated nothing. `and False` is the
+# difference between "the key is gone" and "the LATCH is gone", and only the
+# second reaches the re-arm this arrangement needs.
+_M12_NEW = ('tripped=bool(data.pop(self.key("sign_tripped"), False) and False'
+            + chr(10) + '                     if self.name == "shed" else'
+            + chr(10) + '                     data.get(self.key("sign_tripped"), False)),')
+
+
+def m12_findings(tree):
+    """The finding SET of a staged-leg run over the legacy+shed fixture."""
+    code, out = run(Path(tree), "state-legacy-plus-shed.json", "roster.yaml",
+                    "--paths", "staged")
+    return code, set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", out)), out
+
+
+_m12 = mutant_tree([("app/inverter.py", _M12_OLD, _M12_NEW)])
+_m12_clean_code, _m12_clean, _ = m12_findings(HERE)
+_m12_code, _m12_mut, _m12_out = m12_findings(Path(_m12))
+_m12_new = _m12_mut - _m12_clean
+print(f"      staged leg, legacy+shed: shipped exit {_m12_clean_code}, "
+      f"one roster unit's latch popped -> exit {_m12_code}")
+print(f"      findings the mutation ADDS: {sorted(_m12_new)}")
+check("⚠️ PRECONDITION: the baseline is STABLE and does not already carry the "
+      "finding this mutation exists to produce. It is NOT clean - a legacy "
+      "fixture never is - and the SET DIFFERENCE is what makes that fine, "
+      "which is the sentence the deletion should have read before acting on it",
+      not any(k == "unit/shed/sign_tripped" for _, k in _m12_clean))
+check("⭐ M12 RESTORED: a ROSTER unit's latch key that vanishes is a finding "
+      "even though a sibling holds True - and this is the STAGED leg, where "
+      "`snapshot_over()` supplies a transition-made destination, so the "
+      "provenance clause does not foreclose the narrowing",
+      any(k == "unit/shed/sign_tripped" for _, k in _m12_new))
+shutil.rmtree(Path(_m12).parent, ignore_errors=True)
 
 
 # ⚠️ AND THE INPUT FILE IS NEVER WRITTEN. The owner runs this against a copy of
@@ -685,60 +726,34 @@ check("...and no leg's text has swallowed the CLOSING SUMMARY, which repeats "
       "red whenever any leg was",
       not any("FINDING(S) - this transition is not clean" in v
               for v in _L.values()))
-# ⚠️ TWO FURTHER HOLES IN THIS RULE ARE **KNOWN, MEASURED BY REVIEW, AND NOT
-# FIXED HERE** - deliberately, and this paragraph is the whole of the entry.
+# ⚠️ THIS BLOCK USED TO SAY THOSE HOLES WERE KNOWN AND NOT FIXED, AND IT IS
+# NOW STALE IN THE OTHER DIRECTION - INSTR-01 fixed them, and left the
+# paragraph saying "BOTH ARE REVERTED OUT OF THIS CARD, because THIS SUITE
+# CANNOT MEASURE EITHER ONE" describing a tree that no longer exists. Review
+# found it. A comment that outlives its subject is the same defect as a
+# citation that outlives its check.
 #
-#   INJECTIVITY. `moved_to` is "any machine-read key with the same bare name
-#   and the same value", so N vanished keys can all claim the SAME destination.
-#   Review measured a rename carrying `inverter-a` -> `garage` correctly while
-#   DROPPING `inverter-b` -> `shed`: both reported as migrated to
-#   `unit/garage/sign_tripped`, zero store-key findings, `shed` unlatched.
+# WHERE EACH ONE NOW LIVES, and every clause of `moved_to` has a row in 5e:
 #
-#   PROVENANCE. A destination is accepted regardless of whether the transition
-#   put the value there, so a roster unit already latched in its own right is a
-#   free suppression slot. Review measured a build deleting `old-a` while
-#   renaming `old-b` -> `shed`: exit 0, NO FINDINGS, `old-a` reported as having
-#   moved into a key that already held True.
+#   INJECTIVITY  (C6)  R5, and removing the clause flips exactly R5
+#   PROVENANCE   (C7)  R3, likewise
+#   SAME VALUE   (C3)  R4
+#   SAME BARE KEY(C2)  R7 - which had NO row until review deleted the clause
+#                      and the whole 28-file suite stayed green
+#   MACHINE-READ (C1)  R6
+#   OFF-ROSTER   (C5)  R2, and M12 end-to-end on the staged leg
 #
-#   ATTRIBUTION. Which vanished key gets a destination is decided by
-#   `sorted()`, so on a build renaming `inverter-b` -> `garage` while DELETING
-#   `inverter-a`, the deleted key sorts first and takes it: the report names the
-#   DELETED key as migrated and the one that really moved as VANISHED. The run
-#   is still exit 1, so this is a wrong sentence rather than a hidden loss - but
-#   an operator chasing the named key looks at the wrong inverter.
-#
-#   VALUE MATCHING. `and after.data.get(k) == value` survives the suite and is
-#   load-bearing: without it the rule degenerates to BARE-NAME matching, and
-#   review measured a deleted `unit/old-x/sign_reason` reported as having
-#   migrated into a `sign_reason` holding a COMPLETELY DIFFERENT SENTENCE.
-#   Essentially every off-roster vanished `unit/*` key would be suppressed.
-#
-# ⚠️ BOTH FIXES ARE ONE LINE AND BOTH WERE WRITTEN, AND BOTH ARE REVERTED OUT
-# OF THIS CARD, because THIS SUITE CANNOT MEASURE EITHER ONE. Three attempts:
-# a check over part 5's destinations passed with the whole injectivity
-# mechanism deleted (its two destinations are `sign_reason` and `sign_tripped`
-# - different bare keys, which can never contend); a dedicated fixture
-# discriminated nothing (both snapshots read one state file, so nothing
-# vanishes and there are no migrated lines either way); and rebuilding M12's
-# fixture to reach the provenance case disarmed M12 for the NARROWING, so all
-# three clause-removals came back green at once.
-#
-# ⚠️ THAT LAST ONE IS THE REASON THIS IS A SPLIT AND NOT A JUDGEMENT CALL: a
-# later fix to the same function silently disarmed the control for an earlier
-# one, and I only saw it because the removal was re-driven. Shipping two more
-# unmeasured clauses into the instrument, on a card whose subject is checks
-# that cannot reach what they name, would be the fourth instance in one PR.
-# They go on their own card, with review's measurements as the starting
-# evidence and a fixture built BEFORE the fix.
-#
-# ⚠️ ALL FOUR ARE CLAUSES OF **ONE COMPREHENSION**, WHICH IS THE STRUCTURAL
-# POINT AND NOT A LIST OF CHORES. `diff()`'s `moved_to` now carries four
-# conditions with four different reasons to exist, against one fixture set that
-# can reach only some of them at a time - so rebuilding a fixture to reach
-# clause N moves the others. That is exactly how (3) happened, and it is what
-# INSTR-01 has to design against rather than patch around.
-#
-# What IS measured here is the narrowing, by M12 above, both ways.
+# ⚠️ ONE HOLE IS STILL OPEN AND IS **UNMEASURED**, stated so nobody reads
+# `sorted()` as guarded: ATTRIBUTION. Which vanished key gets a destination is
+# decided by `sorted()` order, so on a build renaming `inverter-b` -> `garage`
+# while DELETING `inverter-a`, the deleted key sorts first and takes it - the
+# report names the DELETED key as migrated and the one that really moved as
+# VANISHED. Review measured that replacing `sorted(` with `list(` leaves the
+# suite green: every 5e case has at most one candidate destination, so no row
+# can see ordering. The run is still exit 1, so this is a WRONG SENTENCE rather
+# than a hidden loss - an operator chasing the named key looks at the wrong
+# inverter. Fixing it needs the destination's provenance rather than
+# first-come, which is more than a rename diff currently knows.
 check("⚠️ and the key that MOVED is not reported as lost: the before-snapshot "
       "holds `unit/inverter-a/sign_tripped = True` and the after-snapshot "
       "holds it under `garage`, three lines apart in the same report. A "
@@ -868,8 +883,9 @@ print("5e. INSTR-01: `diff()`'s suppression rule, ONE FIXTURE PER CLAUSE")
 # So the rule is graded at the level it is written at - `diff()` on constructed
 # Snapshots - with ONE CASE PER CLAUSE. Nothing here is a fiction: the inputs
 # are the same three fields `diff()` reads (`data`, `machine_read`, `units`),
-# and the end-to-end controls above (M12, part 5) still grade the same rule
-# through a real start. This is the separability those cannot have.
+# and the end-to-end controls above - M12 on the STAGED leg, and part 5 -
+# still grade the same rule through a real start. This is the separability
+# those cannot have, not a replacement for them.
 CLAUSE_CASES = {
     # name: (units, machine_read, before, after)
     "R1-rename-legit": (
@@ -893,6 +909,18 @@ CLAUSE_CASES = {
     "R6-machine-read": (
         ["garage"], [],
         {"unit/old/sign_tripped": True}, {"unit/garage/sign_tripped": True}),
+    # ⚠️ R7 EXISTS BECAUSE THE BARE-KEY MATCH HAD NO ROW AT ALL, and review
+    # deleted it and left the whole 28-file suite GREEN. The rule's own comment
+    # says "THE TEST IS NOT 'the name appears somewhere'. It is: the SAME bare
+    # key" - and nothing measured that sentence. It is load-bearing: a vanished
+    # SAFETY-02 `sign_tripped` was suppressed by a SAFETY-42
+    # `delivery_tripped` on a roster unit, i.e. by a DIFFERENT FAILSAFE's key.
+    # `unit/*/delivery_tripped` is machine-read, so this is reachable on any
+    # real two-latch store rather than a contrivance.
+    "R7-bare-key": (
+        ["garage"], ["unit/garage/delivery_tripped"],
+        {"unit/old/sign_tripped": True},
+        {"unit/garage/delivery_tripped": True}),
 }
 # What the SHIPPED rule must answer. `migrated` is the suppression firing.
 CLAUSE_EXPECT = {
@@ -902,10 +930,14 @@ CLAUSE_EXPECT = {
     "R4-value":        (["unit/old/sign_reason"], []),
     "R5-injectivity":  (["unit/old-b/sign_tripped"], ["unit/old-a/sign_tripped"]),
     "R6-machine-read": (["unit/old/sign_tripped"], []),
+    "R7-bare-key":     (["unit/old/sign_tripped"], []),
 }
-# ⚠️ THE DRIVER IS WRITTEN INTO THE TREE UNDER TEST, and the TABLE stays HERE.
-# Expectation and implementation on opposite sides of the subprocess, so a
-# mutation to the tool cannot also move the answer it is graded against.
+# ⚠️ THE DRIVER **IMPORTS** THE TREE UNDER TEST AND THE TABLE STAYS HERE, so
+# expectation and implementation sit on opposite sides of the subprocess and
+# a mutation to the tool cannot also move the answer it is graded against.
+# (It is WRITTEN to a tempdir - see `clause_table()`. The first draft of this
+# sentence said "written into the tree", which is the read-only-CI bug the
+# same commit says it fixed, stated as if it were the design.)
 CLAUSE_DRIVER = """
 import json, sys
 import rehearse_roster as RR
@@ -976,6 +1008,9 @@ check("⚠️ ...and the LEGITIMATE case is still suppressed - a rule that repor
 # nothing is an unmeasured clause, and a removal that flips someone else's row
 # means the cases are not separable after all - which is (3) above, caught.
 CLAUSE_MUTATIONS = [
+    ("C2 same bare key", "R7-bare-key",
+     '            if k.rsplit("/", 1)[-1] == bare and after.data.get(k) == value',
+     "            if True and after.data.get(k) == value"),
     ("C1 machine_read", "R6-machine-read",
      "            k for k in after.machine_read",
      "            k for k in after.data"),

goodwe_controller/tools/rehearsal/state-legacy-plus-shed.json

@@ -0,0 +1,12 @@
+{
+ "_comment": "INSTR-01 SYNTHETIC FIXTURE - `state-legacy.json` with a SECOND roster unit already latched. Not a copy of any live state file. It exists to restore M12 END-TO-END on the STAGED leg, which is the arrangement SAFETY-44 and INSTR-01's first draft both missed: `snapshot_over()` starts the after-leg over the file the BEFORE-leg wrote, so a transition-made destination is available there and the two questions the provenance clause and the narrowing ask are NOT incompatible. Every same-step arrangement makes them incompatible; that is what was measured and over-generalised to 'no fixture can'.",
+ "phase": "idle",
+ "phase_started": "2026-08-07T10:00:00+00:00",
+ "last_completed": "2026-08-07T18:42:00+00:00",
+ "last_start_attempt": "2026-08-07T10:00:00+00:00",
+ "sign_tripped": true,
+ "sign_reason": "SIGN_DISAGREEMENT: commanded -1800 W against a meter reading -1450 W for 190 s",
+ "auto": true,
+ "unit/shed/sign_tripped": true,
+ "unit/shed/sign_reason": "SIGN_DISAGREEMENT: shed, latched before the switch"
+}

goodwe_controller/tools/rehearse_roster.py

@@ -579,8 +579,15 @@ def diff(before: Snapshot, after: Snapshot) -> list:
         # here. Neither mutation exercises this branch. The sentence "what keeps
         # this from being a softening of the check" was not supported by the
         # thing it named - and a citation is the worst possible carrier for that,
-        # because it reads as having been checked. The branch is now bounded by
-        # M12, written for it, in test_rehearse.py.
+        # because it reads as having been checked.
+        #
+        # ⚠️ AND THE REPLACEMENT CITATION WENT STALE THE SAME WAY. It read "the
+        # branch is now bounded by M12" through a card that DELETED M12 and a
+        # card that restored it on a different leg - eight lines below the
+        # paragraph condemning exactly this. Every clause of this comprehension
+        # is now graded by a row in test_rehearse.py part 5e, one case per
+        # clause, and each clause-removal must flip exactly its own row. That
+        # is a property of the section, not a pointer at a named check.
         # ⚠️ AND THE DESTINATION MUST BE ONE **THIS TRANSITION MADE**
         # (`before.data.get(k) != value`) AND NOT ALREADY SPOKEN FOR
         # (`k not in claimed`). Without the first, a roster unit that was