SAFETY-32 round 3: a fixture of N packs cannot separate reductions that agree on N
checks / unit (pull_request) Successful in 4m41s
checks / unit (pull_request) Successful in 4m41s
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
8501e055f2
commit
52380c0952
@@ -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.
|
||||
|
||||
---
|
||||
|
||||
|
||||
Reference in New Issue
Block a user