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