SAFETY-44: ship only what this suite can measure, and split the two clauses it cannot
checks / unit (pull_request) Successful in 6m58s
checks / unit (pull_request) Successful in 6m58s
⚠️ REVIEW FOUND THE INJECTIVITY CHECK INERT IN THE SAME WAY M12's FIRST DRAFT
WAS, three paragraphs below the comment diagnosing it. Removing the whole
mechanism left 28/28 GREEN: part 5's two destinations are `sign_reason` and
`sign_tripped`, DIFFERENT bare keys, which can never contend. The
`len(_dests) >= 2` precondition was true and established nothing - "not
asserting over an empty list" was correct, "this run can exercise injectivity"
was not.
Review also measured a second, narrower silent loss: `moved_to` accepts a
destination regardless of whether the TRANSITION put the value there, so a
roster unit already latched in its own right is a free suppression slot. A build
deleting `old-a` while renaming `old-b` -> `shed` reported exit 0, NO FINDINGS,
with `old-a` "migrated" into a key that already held True.
⚠️ I WROTE BOTH ONE-LINE FIXES AND HAVE REVERTED BOTH, because THIS SUITE
CANNOT MEASURE EITHER. Three attempts, three different ways of proving nothing:
1. assert injectivity over part 5's real destinations
-> passes with the entire mechanism deleted (non-contending bare keys)
2. build a dedicated fixture for the two-claimant case
-> discriminates NOTHING: both snapshots read one state file, so nothing
vanishes and there are no migrated lines with the clause or without it
3. rebuild M12's fixture so the destination is transition-made, to reach the
provenance case
-> ⚠️ DISARMED M12 FOR THE NARROWING. All three clause-removals came back
GREEN at once, and the control I had measured RED last round was gone.
⭐ (3) IS WHY 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 saw it only
because I re-drove the removal rather than trusting the suite's exit code.
Shipping two more unmeasured clauses into the rehearsal instrument, on a card
whose entire subject is checks that cannot reach what they name, would be the
fourth inert artifact in one PR. They go on their own card, with review's
measurements as the starting evidence and the fixture built BEFORE the fix -
which is the ordering that worked for M12 and failed every time I inverted it.
⚠️ AND THE SPLIT IS SAFE, WHICH IS WHY IT IS AVAILABLE. Both remaining holes are
in the REHEARSAL TOOL, not the controller. The round-2 narrowing guarantees a
suppressed key is always OFF the roster, so no roster unit loses protection;
what is left is rollback-view/history mis-reporting on a tool an operator runs
before commissioning. Nothing here can disarm a latch on a live site, and
inverter B goes in on ~2026-09-12. Review offered this split explicitly.
M12's PRECONDITION IS STRENGTHENED, because the exit code could not carry it.
It now requires the shipped tree to be clean AND to not already report the
finding the mutation exists to produce. The first draft passed on exactly that
gap: the fixture's own litter made the run red and nothing separated the two.
Re-driven after the revert, on the round-3 fixture:
shipped exit 0
`vanished_unit not in after.units` gone ⚠️ exit 1
28/28 files pass. The controller half is unchanged since d1b7e3f and review has
no further concerns about it.
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
f6d7bfcb04
commit
f109153216
@@ -452,10 +452,13 @@ _m12_new = (set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_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("⚠️ PRECONDITION: the fixture is clean on the shipped tree AND does not "
|
||||
"already report the finding this mutation exists to produce. The exit "
|
||||
"code alone cannot say the second thing, and the previous draft passed "
|
||||
"on exactly that gap",
|
||||
_m12_clean_code == RR.EXIT_OK
|
||||
and not any(k == "unit/shed/sign_tripped"
|
||||
for _, k in re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_clean_out)))
|
||||
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), "
|
||||
@@ -706,37 +709,40 @@ 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.
|
||||
# ⚠️ 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.
|
||||
#
|
||||
# ⚠️ 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)))
|
||||
|
||||
# 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.
|
||||
#
|
||||
# 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.
|
||||
#
|
||||
# ⚠️ 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.
|
||||
#
|
||||
# What IS measured here is the narrowing, by M12 above, both ways.
|
||||
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 "
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
{
|
||||
"_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.",
|
||||
"_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,
|
||||
@@ -7,4 +7,4 @@
|
||||
"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,19 +545,6 @@ 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]
|
||||
@@ -611,10 +598,8 @@ 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