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
@@ -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