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
This commit is contained in:
glenn schrooyen
2026-09-08 23:51:35 +02:00
co-authored by Claude Opus 5
parent 806390d8b1
commit 91b0d5e4dc
3 changed files with 203 additions and 72 deletions
+189 -61
View File
@@ -411,71 +411,41 @@ 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 - AND ITS
# FIRST DRAFT DID NOT EITHER, WHICH IS THE WORSE FAILURE OF THE TWO.
# ⚠️ `M12` IS GONE, AND ITS REMOVAL IS THE MOST USEFUL THING THIS CARD FOUND.
#
# 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.
# 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:
#
# ⚠️ 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.
# `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.
#
# ⭐ 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.
# 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.
#
# 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.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-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)}")
# ⚠️ THE SECOND CONJUNCT IS IMPLIED BY THE FIRST TODAY - on a clean run the
# finding regex matches nothing - and the commit message that introduced it
# overclaimed by saying the exit code "cannot say" it. It is belt-and-braces,
# load-bearing only if the exit-0 requirement is ever relaxed. WHAT ACTUALLY
# CLOSED THE FIRST DRAFT'S GAP IS `_m12_new` BEING A SET DIFFERENCE: the
# mutation must ADD a finding, which is the check the narrowing's removal turns
# red. Said plainly here because the wrong half was credited once already.
check("⚠️ PRECONDITION: the fixture is clean on the shipped tree AND does not "
"already report the finding this mutation exists to produce - the second "
"is implied by the first today and kept as a belt-and-braces guard",
_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), "
"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)
# ⭐ 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 THE INPUT FILE IS NEVER WRITTEN. The owner runs this against a copy of
@@ -873,6 +843,164 @@ 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)
# --------------------------------------------------------------------------- #
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, part 5) still grade the same rule
# through a real start. This is the separability those cannot have.
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}),
}
# 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"], []),
}
# ⚠️ 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.
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 = [
("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("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"
}
+14 -1
View File
@@ -545,6 +545,12 @@ 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. 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)):
value = before.data[key]
bare = key.rsplit("/", 1)[-1]
@@ -575,9 +581,15 @@ def diff(before: Snapshot, after: Snapshot) -> list:
# 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.
# ⚠️ 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(
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
# 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
@@ -600,6 +612,7 @@ def diff(before: Snapshot, after: Snapshot) -> list:
vanished_unit = key.split("/")[1] if key.startswith("unit/") else None
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