SAFETY-32 round 3: a fixture of N packs cannot separate reductions that agree on N
Both blockers were the recurring defect sitting inside the fix written to close it: a check whose TEXT claims more than its FIXTURE can observe. Both survived a green 19-file suite on8501e05. max(floors) -> max(floors[-2:]) +5 bytes. 12c2's only counterfactual raised the LAST pack, and every window ending at the roster's end follows the last pack. The check said "the reduction reads every entry"; the data reached "it reads the last entry". self.packs -> self.packs[:2] +4 bytes. All three 12g runs drove a TWO-pack roster, where [:2] IS the roster. The check said "what is reduced is the ROSTER and not a POSITION in it"; the true claim was the narrower "no SINGLE-POSITION slice passes all three runs". The prose is cut back to what the old data reaches, and new data added for the rest. No app/ file is touched - app/peakguard.py and app/main.py are byte-identical to8501e05. 12c2 - the pure function: * a ROSTER SET: the same four simulated cut-outs with the deepest moved to each of the four positions. * a computed FAMILY TABLE of fourteen rewrites, printed, with the roster that kills each. A member with an empty kill list takes the check RED naming it. * a LENGTH SWEEP: 78 rosters, lengths 1-12, deepest at every position of each. Closes every head window max(floors[:w]) and tail window max(floors[-w:]) of width 1-11 in one property. 12g - the call site: * _floor_reaching_decide() takes *floors; extra units join through the same second_inverter() hook. * THREE-pack runs with the deep cut-out at index 0, 1 and 2. Every positional slice of a three-pack roster drops a position, and the run whose deep pack sits there answers the option where the roster answers the cut-out. * a POSITIONAL-SLICE TABLE computed against the REAL Controller.packs each of the six cycles ran and the REAL PeakDecision.soc_floor it produced. * an EXACT STRUCTURAL PIN on the roster argument's identity. Not the substring test round 2 removed: "self.packs" in expr is TRUE of every slice; ast.unparse(arg) == "self.packs" is FALSE of all of them. THE GENERAL LAW, and why the pin is there: a fixture of N packs cannot separate two reductions that agree on N packs, and the regress does not terminate in a fixture. [:1] needed two packs, [:2] three, [:3] four. This round's own battery found self.packs[:3] (+4) and self.packs[-3:] (+5) surviving all six behavioural runs; the structural pin is what closes them, and one more pack would only have moved the hole. Battery: 46 mutations over the reduction, the call site, Controller.packs and pack_floor_pct()'s conjunction. Bytecode purged and counted 23 -> 0 for each. 43 red, 3 survivors, all three recorded: max(floors[:12]) / max(floors[-12:]) NOT CAUGHT - needs a 13-pack roster, reported with its size, row 27. max(set(floors)) EQUIVALENT - max is duplicate-invariant. (list(reversed(self.packs)) is equivalent too and is red on the structural pin.) In-process mutation rows 24-27 record all of it, including the not-caught one. 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
619b218110
commit
59ab73559e
@@ -169,6 +169,27 @@ thing that stops. Rule 8's own failure mode, reached through rule 8.
|
||||
isolated counterfactual over an accepted, merged baseline, one key varied per
|
||||
case, asserting the key **name** in the refusal — `all cases passed` on
|
||||
`amd64-hassio-supervisor:2026.08.0`.
|
||||
* ⚠️ **SECOND FIX ROUND — the round-2 fix carried the defect it was written to
|
||||
close, in its prose.** Two more rewrites survived a green 19-file suite on
|
||||
`8501e05`: `binding_soc_floor()`'s `max(floors)` → `max(floors[-2:])` (+5
|
||||
bytes) and the call site's `self.packs` → `self.packs[:2]` (+4 bytes). Both are
|
||||
checks whose TEXT claimed more than their FIXTURE could reach — 12c2's only
|
||||
counterfactual varied the **last** pack, which every window ending at the
|
||||
roster's end follows, and all three 12g runs drove a **two**-pack roster, where
|
||||
`[:2]` *is* the roster. **The general law, now stated in the file: a fixture of
|
||||
N packs cannot separate two reductions that agree on N packs**, and the regress
|
||||
does not terminate in a fixture — `[:1]` needed two packs, `[:2]` three, `[:3]`
|
||||
four. So the reduction is now graded by a **length sweep** (78 simulated
|
||||
rosters, lengths 1–12, deepest cut-out at every position, closing head and tail
|
||||
windows of width 1–11 at once) plus a **computed family table** of fourteen
|
||||
rewrites that goes red naming any member no roster kills; the call site is
|
||||
graded by **three-pack runs** with the deep cut-out at index 0, 1 and 2, plus
|
||||
an **exact structural pin** (the roster argument must unparse to `self.packs`)
|
||||
for the slice widths no bounded roster can reach. Round 3's own battery found
|
||||
`self.packs[:3]` / `[-3:]` surviving all six behavioural runs — the structural
|
||||
pin is what closes them — and one row is recorded **NOT CAUGHT**: a reduction
|
||||
over a window twelve packs wide, which needs a 13-pack roster to observe.
|
||||
No shipped behaviour changed in this round; only what observes it.
|
||||
* **Twelve source mutations, eleven red, one argued survivor**, through
|
||||
`tools/mutation_run.sh` (bytecode purged). The battery also found a real
|
||||
weakness of its own: `_flat_bms_floor()` had the default in two places and each
|
||||
|
||||
Reference in New Issue
Block a user