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 on 8501e05.

  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
to 8501e05.

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:
glenn schrooyen
2026-09-05 03:01:57 +02:00
co-authored by Claude Opus 5
parent ffbabea8ce
commit a4c95f83ce
3 changed files with 621 additions and 26 deletions
@@ -191,6 +191,95 @@ command a forced discharge to 20 % on a pack whose BMS cuts out at 35 %.
later edit that re-degenerates any of these fixtures goes red on a row rather
than on nothing.
### 3b. ⚠️ SECOND FIX ROUND — the fix carried the defect it was written to close
Round 2 closed both named survivors, and both of round 3's blockers are the
**same defect sitting inside that fix**: a check whose TEXT claims more than its
FIXTURE can observe. Applied to `app/` on `8501e05`, **all 19 files stayed
green** for both:
| mutation | Δ | the sentence that was too broad | why the fixture could not see it |
|---|---|---|---|
| `binding_soc_floor()`: `max(floors)` → `max(floors[-2:])` | **+5 bytes** | *"So the reduction reads **every entry**"* | 12c2's only counterfactual raised the **last** pack (`_deeper[-1]`), and **every window that ends at the roster's end follows the last pack**. On `(30,25,40,35)` both answer 40; on `_deeper` both answer 45. |
| the `decide()` call site: `self.packs` → `self.packs[:2]` | **+4 bytes** | *"what is reduced is the **ROSTER** and not a POSITION in it"* | all three `_floor_reaching_decide` runs drove a **two-pack** roster, where `self.packs[:2]` **is** `self.packs` — by exactly the argument 12c2 itself makes about two packs being unable to separate max/min/first/last. |
Round 2's *report* stated the narrow, true claim ("no **single-position** slice
passes all three runs"). The *check in the file* stated the broad one. That gap
is the whole of round 3.
**THE GENERAL LAW, stated once so the next card can use it:**
> **A fixture of N packs cannot separate two reductions that agree on N packs.**
> Two cannot separate max from min from first from last. Three cannot separate
> max from max-of-the-last-two. A single counterfactual that varies one position
> cannot separate the reduction from any window containing that position.
Its corollary is the reason this section is long: **the regress does not
terminate in a fixture.** Closing `[:1]` took two packs; `[:2]` took three;
`[:3]` takes four — and a four-pack run hands `[:4]` the same free pass. Round 3
therefore does two different things rather than adding one more pack.
**What was added — no shipped behaviour changed, only what observes it:**
* **Part 12c2 gained a ROSTER SET and a computed FAMILY TABLE.** The same four
simulated cut-outs with the **deepest moved to each of the four positions**,
and fourteen enumerated rewrites of `max(floors)` each checked against every
roster. The table is **computed and printed**, and a member with an empty kill
list takes the check **red naming it** — so a family member can no longer be
added without a fixture that reaches it. `max(floors[-2:])` is killed only by
the rosters whose deepest sits at index 0 or 1, which is precisely the data the
single last-pack counterfactual could not supply.
* **Part 12c2 gained a LENGTH SWEEP.** `binding_soc_floor()` is a pure function
over a list, which is the one place a sweep is cheap: **78 simulated rosters,
lengths 1 through 12, the deepest cut-out at every position of each.** That
closes *every* head window `max(floors[:w])` and *every* tail window
`max(floors[-w:])` of width **1 to 11** in one property rather than one
mutation at a time — and the check asserts that width **12 is NOT reached**, so
the limit is a red line rather than a silence.
* **Part 12g drives THREE-pack rosters**, with the deep cut-out at index 0, 1
**and** 2. Every positional slice of a three-pack roster is a proper subset of
`{0,1,2}` and so drops a position; the run whose deep pack sits there answers
the option, 20 %, where the roster answers 35 %. `self.packs[:2]` goes red on
the index-2 run. `_floor_reaching_decide()` now takes `*floors`, and the extra
units join through the same `second_inverter()` hook the two-pack runs use.
* **Part 12g gained a POSITIONAL-SLICE TABLE**, computed against the **real**
`Controller.packs` each of the six cycles actually ran and the **real**
`PeakDecision.soc_floor` it produced — so it measures the shipped call site's
own answer, not a re-derivation, and a survivor takes the check red.
* ⚠️ **AND A FIFTH AND SIXTH SURVIVOR, FOUND BY ROUND 3'S OWN BATTERY AND
CLOSED STRUCTURALLY RATHER THAN BY ONE MORE PACK.** `self.packs[:3]` (+4) and
`self.packs[-3:]` (+5) survive **all six** behavioural runs, because the
longest roster those runs drive is three packs long. Part 12g therefore also
pins the roster **argument's identity** on the AST: it must unparse to exactly
`self.packs`, which is false of every slice at every length. ⚠️ This is **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 two
halves are separated and each says what it reaches: the **runs** grade the
VALUE and reach every slice up to N=3; the **pin** grades the ARGUMENT'S
IDENTITY at any N and is blind to two things the runs are not — a rewrite of
what `Controller.packs` *returns* (the runs' `len(ctl.packs) == 3` catches
that) and the reduction *inside* `binding_soc_floor()` (12c2's).
* ⚠️ **AND ONE ROW IS RECORDED AS NOT CAUGHT.** A reduction over a window
**twelve packs wide** is indistinguishable from `max(floors)` on every roster
in the file, because the sweep stops at twelve. Unlike the call site there is
no identity claim to pin — the claim is semantic, "the maximum", and a shape
pin would refuse honest refactors of the expression. It is reported **with its
size** (it needs a 13-pack roster, on a site whose roster is ONE and whose
second unit is ~8 days out) rather than hidden.
* **Two rewrites are EQUIVALENT, not uncaught.** `max(set(floors))` and
`list(reversed(self.packs))` cannot change any answer — `max` is order- and
duplicate-invariant. The second is nonetheless red on the structural pin.
* **In-process mutation rows 24 – 27** record all four of round 3's findings,
including the not-caught one, so a later edit that re-degenerates any of these
fixtures goes red on a row rather than on nothing.
## 4. ⚠️ THE HONEST LIMITATION, and it is the reason this record exists
**Under any configuration rule 8 accepts, `binding_soc_floor()` answers
@@ -270,10 +359,23 @@ per-pack bound. Nothing here touched it.
MUTATION.md's masking section in three lines of option reading. It has one
defaulting line now, and M12 takes six checks red.
* **Round 3 changed no `app/` file at all.** `test_peakguard.py` only:
parts 12c2 and 12g. Its battery was **46 mutations across
`binding_soc_floor()`'s reduction, the `decide()` call site, `Controller.packs`
and `pack_floor_pct()`'s conjunction** — bytecode purged and counted before and
after each (23 → 0). **43 red, 3 survivors, all three recorded above and in the
in-process rows**: `max(floors[:12])` and `max(floors[-12:])`, which need a
13-pack roster to observe and are reported with that size rather than hidden;
and `max(set(floors))`, which is **equivalent** — `max` is duplicate-invariant,
so it cannot change an answer. `list(reversed(self.packs))` is equivalent too
(`max` is order-invariant) and is nonetheless red on the structural pin.
⚠️ **No measurement of inverter B appears anywhere in this change.** It does not
physically exist. Every second-pack number in a fixture, in the probe and in
config.yaml's commented example is **simulated and labelled as such**; only the
10 % on inverter A is read off hardware.
10 % on inverter A is read off hardware. The three-pack runs added in round 3 are simulated
twice over: there is no inverter C at all, and the shallow slots carry inverter
A's measured 10 % while the 35 % cut-out that moves along the roster is invented.
---