diff --git a/goodwe_controller/test_rehearse.py b/goodwe_controller/test_rehearse.py index 4db7185..bf98399 100644 --- a/goodwe_controller/test_rehearse.py +++ b/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"), diff --git a/goodwe_controller/tools/rehearsal/state-legacy-plus-shed.json b/goodwe_controller/tools/rehearsal/state-legacy-plus-shed.json new file mode 100644 index 0000000..9c6151e --- /dev/null +++ b/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" +} diff --git a/goodwe_controller/tools/rehearse_roster.py b/goodwe_controller/tools/rehearse_roster.py index 36a7384..418f44e 100644 --- a/goodwe_controller/tools/rehearse_roster.py +++ b/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