SAFETY-44: give the moved-not-lost branch a control that reaches it, and make the move injective
checks / unit (pull_request) Successful in 7m38s
checks / unit (pull_request) Successful in 7m38s
⚠️ THE CONTROL I WROTE LAST ROUND WAS INERT, AND REVIEW MEASURED IT. M12 ran its
mutant over `state-legacy.json` and the findings diff against the UNMUTATED tree
was EMPTY. It "passed" because that fixture's STAGED leg is already exit 1 on
pre-existing litter, and `"migrated unit/shed/" not in out` was trivially true
because a pre-DEV-02 FLAT store has no shed latch to lose - after migration only
the FIRST roster entry is ever latched.
The decisive measurement is the one it could not make: reverting the
`vanished_unit not in after.units` narrowing - restoring exactly the rule that
hides a real latch loss - left 28/28 GREEN.
⚠️ SO IT WAS HABIT 4 WEARING THE CLOTHES OF ITS OWN FIX, AND WORSE THAN THE
"NO CONTROL" IT REPLACED, because it reads as checked. That is this commit's
own argument about the M3 mis-citation, turned on the thing I wrote to answer it.
⭐ THE FIXTURE CAME FIRST THIS TIME. `state-both-latched.json` is a store at
SCHEMA_VERSION with `unit/garage/*` AND `unit/shed/*` both latched by ONE site
event, so the reasons match too - the arrangement in which same-value
suppression is most dangerous, and the one no existing fixture could produce.
M12's mutant then makes ONE roster unit's latch key VANISH while its sibling's
survives at the same value:
shipped tree, both-latched fixture exit 0, no findings
one unit's latch key deleted exit 1, ADDS
VANISHED STORE KEY unit/shed/sign_tripped
narrowing reverted ⚠️ RED (was 28/28 green)
And it asserts the PRECONDITION - the fixture is clean on the shipped tree -
plus that the mutation ADDS findings rather than coinciding with ones the
fixture already had. An empty diff there is exactly what made the last draft
inert, and nothing said so.
⭐ AND THE MOVE IS NOW INJECTIVE, which is the narrower hole review found still
open. `moved_to` is "any machine-read key with the same bare name and the same
value", and `DEFAULTS["sign_tripped"] is False` means `True` is the ONLY
non-default value a latch can hold - so N vanished keys could all claim the SAME
destination, by construction rather than by coincidence. Measured on a rename
carrying `inverter-a` -> `garage` correctly while DROPPING `inverter-b` -> `shed`:
migrated unit/inverter-a/sign_tripped = True -> unit/garage/sign_tripped
migrated unit/inverter-b/sign_tripped = True -> unit/garage/sign_tripped
Zero store-key findings, on a run where `shed` came up UNLATCHED. Two keys
cannot both have become one key. `diff()` claims each destination once.
⚠️ AND THE CHECK FOR IT IS ANCHORED TO A RUN THAT ACTUALLY PRODUCES MIGRATED
LINES. A dedicated mutant was written first and asserted over an EMPTY list -
vacuous, passing, indistinguishable from working, the same defect twice in one
sitting. These fixtures cannot produce two claimants (`migrate_unit_keys()`
moves FLAT keys only, so one flat latch yields one migration), so rather than
build a fiction to grade, injectivity is asserted over part 5's real migrations,
with a PRECONDITION that there are at least two of them. THE TWO-CLAIMANT
ARRANGEMENT IS A STATED RESIDUAL: bounded in `diff()` by construction, not
measured end-to-end.
Finding 4, and my correction to it was also wrong. The comment cited "line 315"
and "two hundred lines below"; the fix I wrote said "~54 lines down", which was
review's distance to the WRONG line, carried to a new referent without
re-measuring - inside the sentence apologising for a wrong number. Recomputed at
5e382f5: 327-261 = 66, 327-252 = 75, and 54 was neither. There is no distance
now, because a distance is a coordinate and the sentence already names the thing.
And the residual gains its second half, which review noticed and I had not: the
reason re-armed from is the FLAT mirror, carrying whatever tripped LAST, so this
path can print one inverter's evidence under another's name. The latch is right
and the explanation may not be. `test_maintenance.py`'s check that the reason is
not the removed unit's is guaranteed by that fixture's flat string, NOT by the
code, and now says so.
28/28 files pass.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
This commit is contained in:
co-authored by
Claude Opus 5
parent
d1b7e3f113
commit
f6d7bfcb04
@@ -251,11 +251,14 @@ class Controller:
|
||||
# WRITES FOR THEM. This line used to read `migrate_unit_keys(store,
|
||||
# UNIT_A)`, and the constant was wrong in exactly the way the
|
||||
# `maint_migration` call below says the SAME constant would be wrong -
|
||||
# ⚠️ this comment used to cite "line 315" and "two hundred lines below",
|
||||
# and BOTH numbers were wrong (315 is the CFG-03 defaults note; the
|
||||
# comment meant is ~54 lines down, and line numbers move). Cite the
|
||||
# thing, not its coordinates. On a declared roster the flat latch
|
||||
# landed under
|
||||
# ⚠️ this comment used to cite "line 315" and "two hundred lines
|
||||
# below", and both were wrong. The correction I wrote for them was
|
||||
# wrong too: it said "~54 lines down", which was review's distance to
|
||||
# the WRONG line, carried to a new referent without re-measuring -
|
||||
# inside the sentence apologising for a wrong number. There is no
|
||||
# distance here now, because a distance is a coordinate and the
|
||||
# sentence above already names the thing. On a declared roster the flat
|
||||
# latch landed under
|
||||
# `unit/inverter-a/`, which is on no roster, was read back under the
|
||||
# name it was handed, and stamped the marker. `roster_names()` is the
|
||||
# naming rule itself and returns `[UNIT_A]` on the flat shape, so the
|
||||
@@ -830,6 +833,15 @@ class Controller:
|
||||
# held at 0 W until an operator clears it, which is the conservative
|
||||
# direction; SAFETY-44's is a site DRIVING on a state file that says it
|
||||
# is latched.
|
||||
#
|
||||
# ⚠️ AND THE SECOND HALF OF THAT RESIDUAL IS THE **SENTENCE**, NOT THE
|
||||
# BOOLEAN. The reason re-armed from is the FLAT mirror, which carries
|
||||
# whatever tripped LAST - so on a multi-unit site this path can print
|
||||
# one inverter's evidence under another inverter's name. The latch is
|
||||
# right and the explanation may not be. It is disclosed here because the
|
||||
# banner is what an operator acts on, and `test_maintenance.py`'s check
|
||||
# that the reason is not the removed unit's is guaranteed by that
|
||||
# fixture's choice of flat string, NOT by this code.
|
||||
# ⚠️ AND THE THREE CASES ARE THREE VARIABLES, NOT ONE SHARED FLAG.
|
||||
# THIS IS WHERE THE FIRST VERSION OF THIS FIX WAS DEFEATED, BY ONE KEY.
|
||||
# It wrote `namespaced_latched = True` for BOTH "on the roster" and "off
|
||||
|
||||
@@ -411,37 +411,64 @@ 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)
|
||||
|
||||
# ⚠️ AND `M12` BOUNDS THE **MOVED-NOT-LOST** RULE, WHICH NOTHING DID. The
|
||||
# suppression added with SAFETY-44 cites its own bound in a comment, and the
|
||||
# first version of that comment cited M3 - which drops `sign_reason` from
|
||||
# `LEGACY_UNIT_KEYS` and expects `LATCH KEY NOT UNDER A ROSTER NAME` - and the
|
||||
# commit message cited it too. It is the wrong mutant, and so is M9: every key
|
||||
# M9 vanishes is FLAT, so neither can satisfy the `unit/` gate the rule sits
|
||||
# behind. THE BRANCH HAD NO NEGATIVE CONTROL AT ALL, in a card whose whole
|
||||
# subject is checks that cannot reach the failure they name.
|
||||
# ⚠️ AND `M12` BOUNDS THE **MOVED-NOT-LOST** RULE, WHICH NOTHING DID - AND ITS
|
||||
# FIRST DRAFT DID NOT EITHER, WHICH IS THE WORSE FAILURE OF THE TWO.
|
||||
#
|
||||
# ⚠️ AND THE HOLE IT LEFT WAS REAL. `DEFAULTS["sign_tripped"] is False`, so the
|
||||
# ONLY non-default value a latch can hold is `True` - which means, before the
|
||||
# `vanished_unit not in after.units` clause, ANY surviving latched roster unit
|
||||
# suppressed ANY other unit's vanished latch. Measured on a build that drops a
|
||||
# roster unit's `sign_*` while a sibling's survives at the same value: exit 0,
|
||||
# "nothing vanished, nothing stranded", on a deleted SAFETY-02 latch.
|
||||
# The rule cited M3 as its bound, and the commit message cited it too. M3 drops
|
||||
# `sign_reason` from `LEGACY_UNIT_KEYS`; M9, the one actually meant, vanishes
|
||||
# only FLAT keys, so neither can satisfy the `unit/` gate the rule sits behind.
|
||||
# THE BRANCH HAD NO CONTROL AT ALL.
|
||||
#
|
||||
# ⚠️ THE FIRST FIX FOR THAT WAS INERT, AND REVIEW MEASURED IT: run M12's mutant
|
||||
# over `state-legacy.json` and the findings diff against the UNMUTATED tree is
|
||||
# EMPTY. It "passed" because that fixture's STAGED leg is already exit 1 on
|
||||
# pre-existing litter, and `"migrated unit/shed/" not in out` was trivially
|
||||
# true because a pre-DEV-02 FLAT store has no shed latch to lose - after
|
||||
# migration only the FIRST roster entry is ever latched. A control written
|
||||
# against a fixture that cannot hold the failure is habit 4 wearing the clothes
|
||||
# of its own fix, and it is WORSE than the honest "no control" it replaced,
|
||||
# because it reads as checked.
|
||||
#
|
||||
# ⭐ SO THE FIXTURE CAME FIRST. `state-both-latched.json` is a store at
|
||||
# SCHEMA_VERSION with `unit/garage/*` AND `unit/shed/*` both latched, by ONE
|
||||
# site event so the reasons match too - the arrangement in which the
|
||||
# suppression is most dangerous, and the one no existing fixture could produce.
|
||||
# The mutant then makes ONE roster unit's latch key VANISH while its sibling's
|
||||
# survives at the same value.
|
||||
#
|
||||
# THE DECISIVE MEASUREMENT, which is what the previous draft could not make:
|
||||
# reverting the `vanished_unit not in after.units` narrowing - restoring exactly
|
||||
# the rule review proved hides a real loss - turns this RED. Before, it was
|
||||
# 28/28 green.
|
||||
_M12_OLD = 'tripped=bool(data.get(self.key("sign_tripped"), False)),'
|
||||
_M12_NEW = ('tripped=bool(data.get(self.key("sign_tripped"), False))' + chr(10)
|
||||
+ ' if self.name != "shed" else False,')
|
||||
_M12_NEW = ('tripped=bool(data.pop(self.key("sign_tripped"), False)'
|
||||
+ chr(10) + ' if self.name == "shed"'
|
||||
+ chr(10) + ' else data.get(self.key("sign_tripped"), False)),')
|
||||
_m12 = mutant_tree([("app/inverter.py", _M12_OLD, _M12_NEW)])
|
||||
_m12_code, _m12_out = run(Path(_m12), "state-legacy.json", "roster.yaml")
|
||||
print(f" a roster unit that stops restoring its latch -> exit {_m12_code}")
|
||||
check("⭐ M12: a ROSTER unit's latch that stops being read is still a finding - "
|
||||
"the moved-not-lost rule suppresses a RENAME (the key left a name this "
|
||||
"roster does not carry and arrived under one it does), never a LOSS",
|
||||
_m12_code == RR.EXIT_FINDING)
|
||||
check("...and the suppression is not what swallowed it: a key whose own unit is "
|
||||
"ON the roster is never reported as migrated, whatever else carries the "
|
||||
"same value",
|
||||
"migrated unit/shed/" not in _m12_out)
|
||||
_m12_code, _m12_out = run(Path(_m12), "state-both-latched.json", "roster.yaml")
|
||||
_m12_clean_code, _m12_clean_out = run(HERE, "state-both-latched.json", "roster.yaml")
|
||||
_m12_new = (set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_out))
|
||||
- set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_clean_out)))
|
||||
print(f" both-latched store, shipped -> exit {_m12_clean_code}; "
|
||||
f"one unit's latch key deleted -> exit {_m12_code}")
|
||||
print(f" findings the mutation ADDS: {sorted(_m12_new)}")
|
||||
check("⚠️ PRECONDITION: the fixture is clean on the shipped tree, so anything "
|
||||
"below is the MUTATION's doing and not the fixture's - the previous "
|
||||
"draft of this control failed exactly here and nothing said so",
|
||||
_m12_clean_code == RR.EXIT_OK)
|
||||
check("⭐ M12: a ROSTER unit's latch key that VANISHES is a finding even though "
|
||||
"a sibling on the same roster still holds True - the moved-not-lost rule "
|
||||
"suppresses a RENAME (a key leaving a name this roster does not carry), "
|
||||
"never a LOSS",
|
||||
_m12_code == RR.EXIT_FINDING
|
||||
and any(k == "unit/shed/sign_tripped" for _, k in _m12_new))
|
||||
check("...and the mutation ADDS findings rather than merely coinciding with "
|
||||
"ones the fixture already had - an empty diff here is what made the "
|
||||
"previous draft inert",
|
||||
bool(_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
|
||||
# a live state file; a tool that edited it would be a tool that had to be
|
||||
# trusted rather than one that cannot do harm.
|
||||
@@ -679,6 +706,37 @@ 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()))
|
||||
# ⚠️ INJECTIVITY, ASSERTED WHERE MIGRATED LINES ACTUALLY EXIST. `moved_to` is
|
||||
# "any machine-read key with the same bare name and the same value", so N
|
||||
# vanished keys could all claim the SAME destination - and
|
||||
# `DEFAULTS["sign_tripped"] is False` means `True` is the ONLY non-default value
|
||||
# a latch can hold, so same-value matching collides by CONSTRUCTION here, not by
|
||||
# coincidence. 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. Two
|
||||
# keys cannot both have become one key. `diff()` now claims each destination
|
||||
# once.
|
||||
#
|
||||
# ⚠️ AND THIS CHECK IS DELIBERATELY ANCHORED TO A RUN THAT PRODUCES MIGRATED
|
||||
# LINES, WHICH IS THE WHOLE LESSON OF M12's FIRST DRAFT. A dedicated mutant for
|
||||
# the two-claimant arrangement was written first and asserted over an EMPTY
|
||||
# list - vacuous, passing, and indistinguishable from working. These fixtures
|
||||
# cannot produce two claimants (`migrate_unit_keys()` moves FLAT keys only, so
|
||||
# one flat latch yields one migration), and rather than build a fiction to
|
||||
# grade, the property is asserted over the migrations part 5 really makes. THE
|
||||
# TWO-CLAIMANT ARRANGEMENT IS A STATED RESIDUAL, bounded in `diff()` by
|
||||
# construction and unmeasured end-to-end.
|
||||
_dests = re.findall(r"migrated \S+ = .*? -> (\S+)", out44)
|
||||
print(f" migrated-to destinations: {_dests}")
|
||||
check("⚠️ PRECONDITION: this run really does produce migrated lines, so the "
|
||||
"injectivity check below is not asserting over an empty list - which is "
|
||||
"exactly how M12's first draft passed while testing nothing",
|
||||
len(_dests) >= 2)
|
||||
check("⭐ no destination is claimed by TWO vanished keys: a second claimant has "
|
||||
"not moved anywhere, and calling it migrated is how a DELETED latch reads "
|
||||
"as a rename",
|
||||
len(_dests) == len(set(_dests)))
|
||||
|
||||
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 "
|
||||
|
||||
@@ -0,0 +1,10 @@
|
||||
{
|
||||
"_comment": "SAFETY-44 SYNTHETIC FIXTURE - not a copy of any live state file; this session cannot read that one and did not try. It exists for ONE control: a store in which TWO ROSTER UNITS ARE LATCHED AT THE SAME VALUE. `state-legacy.json` cannot serve it - it is pre-DEV-02 and flat, so after migration only the FIRST roster entry is ever latched, and a rule that suppresses a vanished key when another key holds the same value can never be exercised against it. That is exactly how M12's first draft came to pass on the UNMUTATED tree. Both units are latched by ONE site event, so the reasons match too, which is the arrangement in which the suppression is most dangerous.",
|
||||
"schema_version": 1,
|
||||
"maint_schema_version": 1,
|
||||
"auto": true,
|
||||
"unit/garage/sign_tripped": true,
|
||||
"unit/garage/sign_reason": "SIGN_DISAGREEMENT: grid meter reversed, both units",
|
||||
"unit/shed/sign_tripped": true,
|
||||
"unit/shed/sign_reason": "SIGN_DISAGREEMENT: grid meter reversed, both units"
|
||||
}
|
||||
@@ -545,6 +545,19 @@ def diff(before: Snapshot, after: Snapshot) -> list:
|
||||
# name and whose roster start writes them under another reported two
|
||||
# VANISHED findings about a pair of defaults, and CONTROL-C went red on a
|
||||
# build that was CORRECT.
|
||||
# ⚠️ `claimed` MAKES THE MOVE **INJECTIVE**, WHICH IT WAS NOT. `moved_to` is
|
||||
# "any machine-read key with the same bare name and the same value", so N
|
||||
# vanished keys could all claim the SAME destination. Review measured it: a
|
||||
# rename that carries `inverter-a` -> `garage` correctly and DROPS
|
||||
# `inverter-b` -> `shed`, both latched by one event, reported
|
||||
#
|
||||
# migrated unit/inverter-a/sign_tripped = True -> unit/garage/sign_tripped
|
||||
# migrated unit/inverter-b/sign_tripped = True -> unit/garage/sign_tripped
|
||||
#
|
||||
# with ZERO store-key findings, on a run where `shed` came up unlatched. Two
|
||||
# keys cannot both have become one key. A destination is claimable once; the
|
||||
# second claimant has not moved anywhere and is reported as what it is.
|
||||
claimed = set()
|
||||
for key in sorted(set(before.data) - set(after.data)):
|
||||
value = before.data[key]
|
||||
bare = key.rsplit("/", 1)[-1]
|
||||
@@ -598,8 +611,10 @@ def diff(before: Snapshot, after: Snapshot) -> list:
|
||||
# own unit is still on the roster has not been renamed - it has been
|
||||
# LOST - and no amount of the same value elsewhere makes that untrue.
|
||||
vanished_unit = key.split("/")[1] if key.startswith("unit/") else None
|
||||
moved_to = [k for k in moved_to if k not in claimed]
|
||||
if vanished_unit is not None and vanished_unit not in after.units \
|
||||
and moved_to:
|
||||
claimed.add(moved_to[0])
|
||||
after.vanished_but_migrated.append(
|
||||
f"{key} = {value!r} -> {moved_to[0]}")
|
||||
continue
|
||||
|
||||
Reference in New Issue
Block a user