Compare commits

..
4 Commits
Author SHA1 Message Date
glenn schrooyenandClaude Opus 5 3de4453956 INSTR-01: match the finding KIND, because M12 was not holding this file to its own rule
checks / unit (pull_request) Successful in 7m7s
Review APPROVED f6f3f22 plainly. Three LOW notes, all applied - the first is a
real gap and the other two are one line each.

⚠️ M12's ASSERTION WAS KIND-BLIND. It matched on the key and ignored the
finding kind, so renaming `diff()`'s `"VANISHED STORE KEY"` to
`"GONE STORE KEY"` left M12 GREEN - review measured it. A vanished latch
quietly downgraded to a softer heading is exactly what part 3 of this same file
requires every mutation to be graded against ("the SPECIFIC finding it should
produce"), so the file was not holding itself to its own doctrine. Inherited
from SAFETY-44's original M12, not introduced here, and fixed now:

    ("VANISHED STORE KEY", "unit/shed/sign_tripped") in _m12_new

Driven: the kind rename is exit 1 and M12 is among the reds where it was green
before, and C5's removal still turns M12 red, so the strengthening did not cost
the discrimination it exists for.

C4 IS NAMED IN THE CLAUSE MAP. It has no 5e row deliberately - part 3's M9
reaches `vanished_unit is not None` end-to-end and a synthetic row would
duplicate that rather than add separability - but C5 lives in the same `if`,
and listing one guard while omitting the other reads as an oversight rather
than a boundary. Review's own recommendation was not to add the row.

AND THE PRINTED SET SAYS WHAT IT LOSES. The finding regex captures the first
TOKEN of each text, so two findings of one kind collapse into one tuple; the
line now says "first token only" so nobody reads it as an inventory. Harmless
for M12 - the difference is one-directional and the pair it asserts on is exact
- but the display was lossier than it looked. Unused `_m12_out` dropped.

28/28 files pass. `rehearse_roster.py` is untouched by this round; review
confirmed its AST is identical between 91b0d5e and f6f3f22, so every
measurement made against the shipped rule still stands.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
2026-09-09 00:58:03 +02:00
glenn schrooyenandClaude Opus 5 f6f3f227c1 INSTR-01: restore M12 on the leg I generalised past, and measure the clause that had no row
checks / unit (pull_request) Successful in 7m6s
Review found two things this PR asserted about itself that were false. Both are
mine and both are worse than the defect the card was filed for.

⚠️ "NO FIXTURE CAN RESTORE IT, MEASURED BOTH WAYS" WAS NOT TRUE, AND TWO
MEASUREMENTS ARE NOT AN IMPOSSIBILITY PROOF. I deleted M12 - SAFETY-44's
working end-to-end control for the off-roster narrowing - on the argument that
the provenance clause made it unrestorable. The structural claim behind it,
that `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 a transition-made destination is available there. Both arrangements I
measured were same-step shaped. Review found the third.

RESTORED, and it discriminates with all six clauses in:

    staged leg, legacy+shed, shipped     _m12_new = VANISHED unit/shed/sign_tripped
    ...C5 narrowing removed              _m12_new = []          ⚠️ suppressed

⚠️ AND MY FIRST RESTORATION DIDN'T DISCRIMINATE EITHER, for a reason worth
recording: `data.pop(k, False)` RETURNS the value, so shed lost the KEY and
kept the LATCH - `_grade_store_migration()` saw `on_roster_latched`, never
re-armed garage, and there was no transition-made destination. The finding was
reported whether or not C5 existed and the control looked restored. `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.

⚠️ WHAT ACTUALLY BROKE WAS M12's exit-0 PRECONDITION, NOT M12. A legacy-shaped
fixture is never clean. 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 what closed the gap is `_m12_new` BEING A SET DIFFERENCE - and
a stable dirty baseline is fine for a set difference. So I deleted a control on
the strength of a precondition the same commit had already called not
load-bearing. That is removing coverage rather than failing to add it, which is
the worse of the two directions.

⭐ AND THE BARE-KEY CLAUSE HAD NO ROW AT ALL. Review deleted
`k.rsplit("/", 1)[-1] == bare` and the whole 28-file suite stayed GREEN. 5e
mutated five clauses; the comprehension carries more, and this one is
load-bearing: a vanished SAFETY-02 `sign_tripped` was suppressed by a SAFETY-42
`delivery_tripped` on a roster unit - a DIFFERENT FAILSAFE's key. 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. `unit/*/delivery_tripped` is
machine-read, so it is reachable on any real two-latch store. R7 added; C2 now
flips exactly R7.

All six clause-removals now flip exactly their own row:

    C1 machine_read   -> ['R6-machine-read']    C5 off-roster  -> ['R2-narrowing']
    C2 same bare key  -> ['R7-bare-key']        C6 injectivity -> ['R5-injectivity']
    C3 same value     -> ['R4-value']           C7 provenance  -> ['R3-provenance']

THREE DANGLING CITATIONS TO A CONTROL THIS PR HAD DELETED, one of them in the
shipped tool eight lines below the paragraph condemning exactly that ("a
citation is the worst possible carrier, because it reads as having been
checked"). The tool no longer names a check; it states the property - every
clause has a row, and each removal flips its own.

A STALE SAFETY-44 BLOCK saying both fixes were "REVERTED OUT OF THIS CARD,
because THIS SUITE CANNOT MEASURE EITHER ONE" - describing a tree this PR
replaced. Rewritten as a map of where each clause is now measured. A comment
that outlives its subject is the same defect as a citation that outlives its
check.

AND A SELF-CONTRADICTION about the driver, in the file and in the last commit
message: "THE DRIVER IS WRITTEN INTO THE TREE UNDER TEST" eight lines above
"THE DRIVER GOES IN A TEMPDIR, NOT IN THE TREE". The code does the tempdir; the
first sentence stated the read-only-CI bug the same commit says it fixed, as if
it were the design. It now says the driver IMPORTS the tree and is WRITTEN to a
tempdir.

ONE HOLE REMAINS OPEN AND IS STATED AS UNMEASURED: attribution. `sorted()`
decides which vanished key claims a destination, so a deleted key can sort
first and be named as the one that migrated while the key that really moved is
reported VANISHED. Review measured that `sorted(` -> `list(` leaves the suite
green - every 5e case has at most one candidate, so no row can see ordering.
Still exit 1, so a wrong sentence rather than a hidden loss. Recorded rather
than left looking guarded.

28/28 files pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
2026-09-09 00:29:00 +02:00
glenn schrooyenandClaude Opus 5 91b0d5e4dc INSTR-01: grade the suppression rule at the level it is written at, one case per clause
checks / unit (pull_request) Successful in 7m4s
SAFETY-44 produced THREE inert controls for this one rule, each inert
differently, and split the two remaining fixes out rather than ship them
unmeasured. This is that card, and the first thing it did was explain why the
end-to-end route could never have worked.

⚠️ `moved_to` IS ONE COMPREHENSION CARRYING FIVE CONDITIONS WITH FIVE DIFFERENT
REASONS TO EXIST, AND `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: the
arrangement that reaches one forecloses the other. That is why rebuilding a
fixture to reach clause N kept moving the others, and it is not a fixture
problem.

⭐ SO THE RULE IS GRADED WHERE IT IS WRITTEN - `diff()` on constructed
Snapshots, ONE CASE PER CLAUSE. Six rows, and on the SHIPPED tree before any
fix they already separated the two known defects:

    R1 rename (legitimate)   migrated                      correct
    R2 narrowing             vanished                      correct
    R3 provenance            MIGRATED                      ⚠️ the defect
    R4 same value            vanished                      correct
    R5 injectivity           BOTH migrated                 ⚠️ the defect
    R6 machine_read          vanished                      correct

The two one-line fixes SAFETY-44 reverted are back, and R3/R5 flip while
R1/R2/R4/R6 do not - so the legitimate rename is still suppressed and this is
not an over-correction.

⭐ AND EACH CLAUSE REMOVAL FLIPS **EXACTLY ITS OWN ROW**, which is the
acceptance criterion this card was filed with:

    C1 machine_read  removed -> ['R6-machine-read']
    C3 same value    removed -> ['R4-value']
    C5 off-roster    removed -> ['R2-narrowing']
    C6 injectivity   removed -> ['R5-injectivity']
    C7 provenance    removed -> ['R3-provenance']

A removal that flips nothing is an unmeasured clause; a removal that flips
someone else's row means the cases are not separable after all. Neither
happened.

⚠️ AND M12 IS DELETED, WHICH IS THE MOST USEFUL THING THIS CARD FOUND. M12 was
SAFETY-44's end-to-end control for the narrowing and it was a REAL control -
red when the narrowing was removed. Adding the provenance clause disarmed it,
and NO FIXTURE CAN RESTORE IT, measured both ways: with the sibling latched in
its own right, C7 rejects the destination before C5 is consulted, so the
mutation is reported whether or not C5 exists; making the destination
transition-made means a flat latch, which makes the shipped run dirty and
breaks M12's own precondition. The second half of the card's acceptance
criterion - "M12 still turns red with the new clauses in" - is therefore
UNSATISFIABLE, and the honest answer is to remove the control rather than keep
one that has become inert. R2 measures C5 strictly better. Part 5 keeps the
end-to-end coverage; discrimination lives in 5e.

`state-both-latched.json` goes with it. Nothing referenced it once M12 was
gone, and the first draft of that paragraph said it was "kept, because 5e's
R2/R3 are derived from the arrangements it represents" - a nice sentence and
not a reference. An unused fixture a comment calls load-bearing is an inert
check one directory over.

TWO THINGS THE DRIVER GETS RIGHT ON PURPOSE:
  - it is written to a TEMPDIR, not beside the tool. `checks / unit` mounts the
    checkout READ-ONLY, so writing into the tree works on a dev box and is
    `OSError: Read-only file system` in CI - green for whoever wrote it and red
    on every PR. Caught by running it in the check image before committing.
  - the TABLE stays in the test file and the driver goes into the tree under
    test, so a mutation to the tool cannot also move the answer it is graded
    against.

28/28 files pass.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
2026-09-08 23:51:35 +02:00
admin 806390d8b1 Merge pull request 'SAFETY-44: the latch migration takes the roster, and the guard stops being defeated by the key the defect wrote' (#71) from SAFETY-44 into release/1.0 2026-09-08 19:16:32 +02:00
4 changed files with 322 additions and 122 deletions
+287 -109
View File
@@ -411,70 +411,91 @@ check("...and `phase` is NOT among them, because its value 'idle' IS the "
"phase" not in _m9_vanished) "phase" not in _m9_vanished)
shutil.rmtree(Path(_m9).parent, ignore_errors=True) shutil.rmtree(Path(_m9).parent, ignore_errors=True)
# ⚠️ AND `M12` BOUNDS THE **MOVED-NOT-LOST** RULE, WHICH NOTHING DID - AND ITS # ⭐ `M12` IS BACK, AND THE CLAIM THAT KILLED IT WAS WRONG.
# FIRST DRAFT DID NOT EITHER, WHICH IS THE WORSE FAILURE OF THE TWO.
# #
# The rule cited M3 as its bound, and the commit message cited it too. M3 drops # M12 is SAFETY-44's end-to-end control for the off-roster narrowing: a mutant
# `sign_reason` from `LEGACY_UNIT_KEYS`; M9, the one actually meant, vanishes # makes one ROSTER unit's latch key vanish while a sibling holds the same
# only FLAT keys, so neither can satisfy the `unit/` gate the rule sits behind. # value, and it must go red when the narrowing is removed. INSTR-01's first
# THE BRANCH HAD NO CONTROL AT ALL. # draft DELETED it, on the claim that the provenance clause made it
# unrestorable and that "NO FIXTURE CAN RESTORE IT, measured both ways".
# #
# ⚠️ THE FIRST FIX FOR THAT WAS INERT, AND REVIEW MEASURED IT: run M12's mutant # ⚠️ TWO MEASUREMENTS ARE NOT AN IMPOSSIBILITY PROOF, AND THIS ONE WAS FALSE.
# over `state-legacy.json` and the findings diff against the UNMUTATED tree is # Both arrangements I measured were SAME-STEP shaped, and the structural
# EMPTY. It "passed" because that fixture's STAGED leg is already exit 1 on # argument - `run()` builds both snapshots from one state file, so "already
# pre-existing litter, and `"migrated unit/shed/" not in out` was trivially # latched" and "made by this transition" are incompatible - is TRUE OF
# true because a pre-DEV-02 FLAT store has no shed latch to lose - after # SAME-STEP AND FALSE OF STAGED. `snapshot_over()` starts the after-leg over
# migration only the FIRST roster entry is ever latched. A control written # the file the BEFORE-leg wrote, so on the staged leg a transition-made
# against a fixture that cannot hold the failure is habit 4 wearing the clothes # destination is available and the two questions stop being incompatible.
# of its own fix, and it is WORSE than the honest "no control" it replaced, # Review found the third arrangement I had generalised past.
# because it reads as checked.
# #
# ⭐ SO THE FIXTURE CAME FIRST. `state-both-latched.json` is a store at # HOW IT WORKS. The fixture is `state-legacy.json` plus a second roster unit
# SCHEMA_VERSION with `unit/garage/*` AND `unit/shed/*` both latched, by ONE # already latched. The mutant makes `shed` POP its own latch key and come up
# site event so the reasons match too - the arrangement in which the # untripped - a truer SAFETY-02 loss than the original, which left `tripped`
# suppression is most dangerous, and the one no existing fixture could produce. # True in memory. On the staged leg, losing shed's latch makes
# The mutant then makes ONE roster unit's latch key VANISH while its sibling's # `_grade_store_migration()` fall through `on_roster_latched` and RE-ARM
# survives at the same value. # `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.
# #
# THE DECISIVE MEASUREMENT, which is what the previous draft could not make: # ⚠️ AND WHAT ACTUALLY BROKE WAS THE PRECONDITION, NOT THE CONTROL. M12's
# reverting the `vanished_unit not in after.units` narrowing - restoring exactly # `exit == EXIT_OK` baseline does not survive a legacy-shaped fixture. That
# the rule review proved hides a real loss - turns this RED. Before, it was # precondition is the one SAFETY-44's own commit called "belt-and-braces,
# 28/28 green. # 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)),' _M12_OLD = 'tripped=bool(data.get(self.key("sign_tripped"), False)),'
_M12_NEW = ('tripped=bool(data.pop(self.key("sign_tripped"), False)' # ⚠️ THE MUTANT POPS **AND COMES UP UNTRIPPED**, which is the whole point and
+ chr(10) + ' if self.name == "shed"' # which the first draft got wrong: `data.pop(k, False)` RETURNS the value, so
+ chr(10) + ' else data.get(self.key("sign_tripped"), False)),') # 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 = mutant_tree([("app/inverter.py", _M12_OLD, _M12_NEW)])
_m12_code, _m12_out = run(Path(_m12), "state-both-latched.json", "roster.yaml") _m12_clean_code, _m12_clean, _ = m12_findings(HERE)
_m12_clean_code, _m12_clean_out = run(HERE, "state-both-latched.json", "roster.yaml") _m12_code, _m12_mut, _ = m12_findings(Path(_m12))
_m12_new = (set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_out)) _m12_new = _m12_mut - _m12_clean
- set(re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_clean_out))) print(f" staged leg, legacy+shed: shipped exit {_m12_clean_code}, "
print(f" both-latched store, shipped -> exit {_m12_clean_code}; " f"one roster unit's latch popped -> exit {_m12_code}")
f"one unit's latch key deleted -> exit {_m12_code}") # ⚠️ THE PRINTED SET IS LOSSIER THAN IT LOOKS: the regex captures the first
print(f" findings the mutation ADDS: {sorted(_m12_new)}") # TOKEN of each finding's text, so two findings of one kind collapse into one
# ⚠️ THE SECOND CONJUNCT IS IMPLIED BY THE FIRST TODAY - on a clean run the # tuple. Harmless here - the difference is one-directional and the pair M12
# finding regex matches nothing - and the commit message that introduced it # asserts on is exact - but do not read this line as an inventory.
# overclaimed by saying the exit code "cannot say" it. It is belt-and-braces, print(f" findings the mutation ADDS (first token only): {sorted(_m12_new)}")
# load-bearing only if the exit-0 requirement is ever relaxed. WHAT ACTUALLY check("⚠️ PRECONDITION: the baseline is STABLE and does not already carry the "
# CLOSED THE FIRST DRAFT'S GAP IS `_m12_new` BEING A SET DIFFERENCE: the "finding this mutation exists to produce. It is NOT clean - a legacy "
# mutation must ADD a finding, which is the check the narrowing's removal turns "fixture never is - and the SET DIFFERENCE is what makes that fine, "
# red. Said plainly here because the wrong half was credited once already. "which is the sentence the deletion should have read before acting on it",
check("⚠️ PRECONDITION: the fixture is clean on the shipped tree AND does not " not any(k == "unit/shed/sign_tripped" for _, k in _m12_clean))
"already report the finding this mutation exists to produce - the second " # ⚠️ AND IT MATCHES THE **KIND** AS WELL AS THE KEY, which SAFETY-44's original
"is implied by the first today and kept as a belt-and-braces guard", # did not. Review measured it: renaming the finding kind in `diff()` from
_m12_clean_code == RR.EXIT_OK # "VANISHED STORE KEY" to "GONE STORE KEY" left M12 GREEN. A vanished latch
and not any(k == "unit/shed/sign_tripped" # quietly downgraded to a softer heading is exactly the shape part 3 requires
for _, k in re.findall(r"⚠️ ([A-Z ]+): (\S+)", _m12_clean_out))) # every mutation to be graded against - "the SPECIFIC finding it should produce"
check("⭐ M12: a ROSTER unit's latch key that VANISHES is a finding even though " # - and this file was not holding itself to its own rule.
"a sibling on the same roster still holds True - the moved-not-lost rule " check("⭐ M12 RESTORED: a ROSTER unit's latch key that vanishes is a "
"suppresses a RENAME (a key leaving a name this roster does not carry), " "VANISHED STORE KEY finding even though a sibling holds True - and this "
"never a LOSS", "is the STAGED leg, where `snapshot_over()` supplies a transition-made "
_m12_code == RR.EXIT_FINDING "destination, so the provenance clause does not foreclose the narrowing",
and any(k == "unit/shed/sign_tripped" for _, k in _m12_new)) ("VANISHED STORE KEY", "unit/shed/sign_tripped") 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) shutil.rmtree(Path(_m12).parent, ignore_errors=True)
@@ -715,60 +736,39 @@ check("...and no leg's text has swallowed the CLOSING SUMMARY, which repeats "
"red whenever any leg was", "red whenever any leg was",
not any("FINDING(S) - this transition is not clean" in v not any("FINDING(S) - this transition is not clean" in v
for v in _L.values())) for v in _L.values()))
# ⚠️ TWO FURTHER HOLES IN THIS RULE ARE **KNOWN, MEASURED BY REVIEW, AND NOT # ⚠️ THIS BLOCK USED TO SAY THOSE HOLES WERE KNOWN AND NOT FIXED, AND IT IS
# FIXED HERE** - deliberately, and this paragraph is the whole of the entry. # 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 # WHERE EACH ONE NOW LIVES, and every clause of `moved_to` has a row in 5e:
# 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 # INJECTIVITY (C6) R5, and removing the clause flips exactly R5
# put the value there, so a roster unit already latched in its own right is a # PROVENANCE (C7) R3, likewise
# free suppression slot. Review measured a build deleting `old-a` while # SAME VALUE (C3) R4
# renaming `old-b` -> `shed`: exit 0, NO FINDINGS, `old-a` reported as having # SAME BARE KEY(C2) R7 - which had NO row until review deleted the clause
# moved into a key that already held True. # 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
# PREFIX GATE (C4) NO 5e ROW, deliberately - `vanished_unit is not None`
# is reached end-to-end by part 3's M9, and a synthetic
# row would duplicate that rather than add separability.
# Listed because C5 lives in the same `if` and omitting
# one guard while naming the other reads as an oversight.
# #
# ATTRIBUTION. Which vanished key gets a destination is decided by # ⚠️ ONE HOLE IS STILL OPEN AND IS **UNMEASURED**, stated so nobody reads
# `sorted()`, so on a build renaming `inverter-b` -> `garage` while DELETING # `sorted()` as guarded: ATTRIBUTION. Which vanished key gets a destination is
# `inverter-a`, the deleted key sorts first and takes it: the report names the # decided by `sorted()` order, so on a build renaming `inverter-b` -> `garage`
# DELETED key as migrated and the one that really moved as VANISHED. The run # while DELETING `inverter-a`, the deleted key sorts first and takes it - the
# is still exit 1, so this is a wrong sentence rather than a hidden loss - but # report names the DELETED key as migrated and the one that really moved as
# an operator chasing the named key looks at the wrong inverter. # VANISHED. Review measured that replacing `sorted(` with `list(` leaves the
# # suite green: every 5e case has at most one candidate destination, so no row
# VALUE MATCHING. `and after.data.get(k) == value` survives the suite and is # can see ordering. The run is still exit 1, so this is a WRONG SENTENCE rather
# load-bearing: without it the rule degenerates to BARE-NAME matching, and # than a hidden loss - an operator chasing the named key looks at the wrong
# review measured a deleted `unit/old-x/sign_reason` reported as having # inverter. Fixing it needs the destination's provenance rather than
# migrated into a `sign_reason` holding a COMPLETELY DIFFERENT SENTENCE. # first-come, which is more than a rename diff currently knows.
# 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.
check("⚠️ and the key that MOVED is not reported as lost: the before-snapshot " 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 `unit/inverter-a/sign_tripped = True` and the after-snapshot "
"holds it under `garage`, three lines apart in the same report. A " "holds it under `garage`, three lines apart in the same report. A "
@@ -873,6 +873,184 @@ check("the SAME state file onto a roster whose first entry IS `inverter-a` "
code_ok == RR.EXIT_OK and "LATCH CAME UP DISARMED" not in out_ok) code_ok == RR.EXIT_OK and "LATCH CAME UP DISARMED" not in out_ok)
# --------------------------------------------------------------------------- #
print()
print("5e. INSTR-01: `diff()`'s suppression rule, ONE FIXTURE PER CLAUSE")
# --------------------------------------------------------------------------- #
# ⚠️ THIS SECTION EXISTS BECAUSE SAFETY-44 PRODUCED THREE INERT CONTROLS FOR
# THIS ONE RULE, EACH INERT DIFFERENTLY:
#
# 1. a check over part 5's real destinations passed with the whole mechanism
# deleted - its two destinations are `sign_reason` and `sign_tripped`,
# DIFFERENT bare keys, which can never contend;
# 2. a dedicated end-to-end fixture discriminated nothing - both snapshots
# read ONE state file, so nothing vanishes and there are no migrated lines
# with the clause or without it;
# 3. rebuilding M12's fixture to reach a new clause DISARMED M12 for an older
# one, and all three clause-removals went green at once.
#
# ⭐ (3) IS THE STRUCTURAL FINDING AND IT IS WHY THIS SECTION IS SHAPED THIS WAY.
# `moved_to` is ONE comprehension carrying FIVE conditions with five different
# reasons to exist, and an END-TO-END fixture cannot separate them: both
# snapshots come from one state file, so the arrangement that reaches clause N
# forecloses clause M. Rebuilding the fixture to reach one moves the others.
#
# 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 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": (
["garage"], ["unit/garage/sign_tripped"],
{"unit/old/sign_tripped": True}, {"unit/garage/sign_tripped": True}),
"R2-narrowing": (
["garage", "shed"], ["unit/garage/sign_tripped", "unit/shed/sign_tripped"],
{"unit/shed/sign_tripped": True}, {"unit/garage/sign_tripped": True}),
"R3-provenance": (
["garage"], ["unit/garage/sign_tripped"],
{"unit/old/sign_tripped": True, "unit/garage/sign_tripped": True},
{"unit/garage/sign_tripped": True}),
"R4-value": (
["garage"], ["unit/garage/sign_reason"],
{"unit/old/sign_reason": "X-unique"},
{"unit/garage/sign_reason": "Y-different"}),
"R5-injectivity": (
["garage"], ["unit/garage/sign_tripped"],
{"unit/old-a/sign_tripped": True, "unit/old-b/sign_tripped": True},
{"unit/garage/sign_tripped": True}),
"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 = {
"R1-rename-legit": ([], ["unit/old/sign_tripped"]),
"R2-narrowing": (["unit/shed/sign_tripped"], []),
"R3-provenance": (["unit/old/sign_tripped"], []),
"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 **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
spec = json.load(sys.stdin)
out = {}
for name, case in spec.items():
units, mread, before, after = case
b = object.__new__(RR.Snapshot); a = object.__new__(RR.Snapshot)
for snap, data in ((b, before), (a, after)):
snap.label = name
snap.data = dict(data)
snap.units = list(units)
snap.machine_read = set(mread)
snap.entities = {}
snap.latched = {u: False for u in units}
snap.latch_reason = {u: "" for u in units}
snap.flat_tripped = False
snap.history = {}
snap.read = set()
snap.stranded_at_default = []
snap.vanished_at_default = []
snap.vanished_but_migrated = []
f = RR.diff(b, a)
out[name] = [
sorted(x.text.split(" = ")[0] for x in f
if x.kind == "VANISHED STORE KEY"),
sorted(t.split(" = ")[0] for t in a.vanished_but_migrated),
]
print(json.dumps(out))
"""
def clause_table(tree) -> dict:
"""Run CLAUSE_CASES through `diff()` in `tree`, as the tool would see it."""
# ⚠️ THE DRIVER GOES IN A TEMPDIR, NOT IN THE TREE. `checks / unit` mounts
# the checkout READ-ONLY, so writing beside the tool works on a dev box and
# is `OSError: Read-only file system` in CI - a difference that would have
# turned this section red on every PR and green for whoever wrote it.
tools = Path(tree) / "tools"
tmp = tempfile.mkdtemp(prefix="clause-drv-")
drv = Path(tmp) / "_clause_driver.py"
drv.write_text(CLAUSE_DRIVER, encoding="utf-8")
proc = subprocess.run(
[sys.executable, str(drv)],
input=json.dumps(CLAUSE_CASES), capture_output=True, text=True,
cwd=tmp,
env={**os.environ, "PYTHONDONTWRITEBYTECODE": "1",
"PYTHONPATH": f"{tools}{os.pathsep}{Path(tree)}"})
shutil.rmtree(tmp, ignore_errors=True)
assert proc.returncode == 0, (
"the clause driver did not run, so every row below would be "
f"fabricated:\n{proc.stdout}\n{proc.stderr}")
return {k: (v[0], v[1]) for k, v in json.loads(proc.stdout).items()}
_ct = clause_table(HERE)
for _name in sorted(CLAUSE_CASES):
_got, _want = _ct[_name], CLAUSE_EXPECT[_name]
print(f" {_name:<18} vanished={_got[0]} migrated={_got[1]}")
check(f"{_name}: the shipped rule answers as specified", list(_got) == [list(_want[0]), list(_want[1])])
check("⚠️ ...and the LEGITIMATE case is still suppressed - a rule that reports "
"every rename is a rule an operator turns off, which is the failure "
"CONTROL-C exists to prevent",
_ct["R1-rename-legit"][1] == ["unit/old/sign_tripped"])
# ⭐ AND EACH CLAUSE REMOVAL MUST FLIP **EXACTLY ITS OWN ROW**. That second half
# is the acceptance criterion this card was filed with: a removal that flips
# 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"),
("C3 same value", "R4-value",
" and after.data.get(k) == value\n", "\n"),
("C5 off-roster", "R2-narrowing",
" if vanished_unit is not None and vanished_unit not in after.units \\\n"
" and moved_to:",
" if vanished_unit is not None and moved_to:"),
("C6 injectivity", "R5-injectivity",
" and k not in claimed)", ")"),
("C7 provenance", "R3-provenance",
" and before.data.get(k) != value", " and True"),
]
for _label, _owns, _old, _new in CLAUSE_MUTATIONS:
_t = mutant_tree([("tools/rehearse_roster.py", _old, _new)])
_mt = clause_table(_t)
_flipped = sorted(n for n in CLAUSE_CASES if _mt[n] != _ct[n])
print(f" {_label:<16} removed -> rows that changed: {_flipped}")
check(f"⭐ removing {_label} flips {_owns} - the clause is load-bearing and "
f"this row is what measures it",
_flipped == [_owns])
shutil.rmtree(Path(_t).parent, ignore_errors=True)
# --------------------------------------------------------------------------- # # --------------------------------------------------------------------------- #
print() print()
print("6. THE REVERSE DIRECTION: the retreat, and the return from it") print("6. THE REVERSE DIRECTION: the retreat, and the return from it")
@@ -1,10 +0,0 @@
{
"_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"
}
@@ -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"
}
+23 -3
View File
@@ -545,6 +545,12 @@ def diff(before: Snapshot, after: Snapshot) -> list:
# name and whose roster start writes them under another reported two # 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 # VANISHED findings about a pair of defaults, and CONTROL-C went red on a
# build that was CORRECT. # build that was CORRECT.
# ⚠️ `claimed` MAKES THE MOVE INJECTIVE. Without it N vanished keys can all
# claim the SAME destination - and `DEFAULTS["sign_tripped"] is False`, so
# `True` is the ONLY non-default value a latch can hold, which means they
# collide by CONSTRUCTION rather than by coincidence. Two keys cannot both
# have become one key; the second claimant has not moved anywhere.
claimed = set()
for key in sorted(set(before.data) - set(after.data)): for key in sorted(set(before.data) - set(after.data)):
value = before.data[key] value = before.data[key]
bare = key.rsplit("/", 1)[-1] bare = key.rsplit("/", 1)[-1]
@@ -573,11 +579,24 @@ def diff(before: Snapshot, after: Snapshot) -> list:
# here. Neither mutation exercises this branch. The sentence "what keeps # here. Neither mutation exercises this branch. The sentence "what keeps
# this from being a softening of the check" was not supported by the # 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, # 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 # because it reads as having been checked.
# M12, written for it, in test_rehearse.py. #
# ⚠️ 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
# already latched in its own right is a free suppression slot that
# nobody moved into.
moved_to = sorted( moved_to = sorted(
k for k in after.machine_read k for k in after.machine_read
if k.rsplit("/", 1)[-1] == bare and after.data.get(k) == value) if k.rsplit("/", 1)[-1] == bare and after.data.get(k) == value
and before.data.get(k) != value and k not in claimed)
# ⚠️ AND THE VANISHED KEY'S OWN UNIT MUST BE **OFF THE ROSTER**, WHICH # ⚠️ AND THE VANISHED KEY'S OWN UNIT MUST BE **OFF THE ROSTER**, WHICH
# THE FIRST VERSION OF THIS RULE DID NOT REQUIRE AND WHICH IS WHAT MADE # THE FIRST VERSION OF THIS RULE DID NOT REQUIRE AND WHICH IS WHAT MADE
# IT A SOFTENING. The match was bare-key-plus-value over the whole of # IT A SOFTENING. The match was bare-key-plus-value over the whole of
@@ -600,6 +619,7 @@ def diff(before: Snapshot, after: Snapshot) -> list:
vanished_unit = key.split("/")[1] if key.startswith("unit/") else None vanished_unit = key.split("/")[1] if key.startswith("unit/") else None
if vanished_unit is not None and vanished_unit not in after.units \ if vanished_unit is not None and vanished_unit not in after.units \
and moved_to: and moved_to:
claimed.add(moved_to[0])
after.vanished_but_migrated.append( after.vanished_but_migrated.append(
f"{key} = {value!r} -> {moved_to[0]}") f"{key} = {value!r} -> {moved_to[0]}")
continue continue