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:
glenn schrooyen
co-authored by
Claude Opus 5
Claude Opus 5
parent
8501e055f2
commit
52380c0952
@@ -53,6 +53,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
|
||||
|
||||
@@ -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.
|
||||
|
||||
---
|
||||
|
||||
|
||||
@@ -3388,10 +3388,173 @@ print(f" ...raise ONLY the last pack 35 % -> 45 %: "
|
||||
f"{binding_soc_floor(_deeper, SOC_FLOOR):g}")
|
||||
check("...and the counterfactual: raise ONE pack - the LAST, which was neither "
|
||||
"the deepest nor the shallowest - past the old deepest, and the answer "
|
||||
"follows it to 45 %. So the reduction reads every entry, and the 40 % "
|
||||
"above was not a coincidence of position",
|
||||
"follows it to 45 %. So the reduction reads the LAST entry, and the 40 % "
|
||||
"above was not a coincidence of that one position. ⚠️ THE LAST ENTRY IS "
|
||||
"ALL THIS REACHES: every window ending at the roster's end contains it, "
|
||||
"so `max(floors[-2:])` follows this line exactly. It claimed 'every "
|
||||
"entry' and could not see that; the table below is the data that can",
|
||||
binding_soc_floor(_deeper, SOC_FLOOR) == 45.0
|
||||
and binding_soc_floor(_many_packs, SOC_FLOOR) == 40.0)
|
||||
# ⚠️ AND THAT COUNTERFACTUAL IS NOT ENOUGH EITHER, WHICH IS ROUND 3's BLOCKER 1.
|
||||
# It varies only the LAST pack, and EVERY window that contains the last two
|
||||
# entries follows it - `max(floors[-2:])` answers 40 on the baseline and 45 on
|
||||
# `_deeper`, exactly as the shipped reduction does. It SURVIVED all 19 files.
|
||||
# The sentence above used to claim "the reduction reads every entry"; the DATA
|
||||
# reaches only "it reads the last entry", and the claim has been cut back to
|
||||
# that. This repository's recurring defect is a check whose text is broader than
|
||||
# its fixture, and it had landed inside the check written to close it.
|
||||
#
|
||||
# ⚠️ THE GENERAL LAW, and the thing to carry to the next card: A FIXTURE OF N
|
||||
# PACKS CANNOT SEPARATE TWO REDUCTIONS THAT AGREE ON N PACKS. Two packs cannot
|
||||
# separate max from min from first from last. THREE cannot separate max from
|
||||
# max-of-the-last-two. A single roster cannot separate a reduction from any
|
||||
# window that happens to contain its answer. So the fixture is not one roster
|
||||
# but a SET, and the property is not "this number is right" but "each member of
|
||||
# an enumerated family of rewrites is separated from `max` somewhere in the set".
|
||||
#
|
||||
# THE SET: the same four cut-outs, with the deepest one moved to EACH position
|
||||
# in turn. A slice that omits position i answers below the deepest on the roster
|
||||
# whose deepest sits at i, so no proper subset of {0,1,2,3} survives all four;
|
||||
# min, mean and median are separated by the baseline. The table is COMPUTED and
|
||||
# PRINTED, so a member no roster kills shows up as a survivor and takes the
|
||||
# check red naming it, rather than being absent from a list nobody re-derived.
|
||||
#
|
||||
# ⚠️ WHAT IT DOES NOT CLAIM. It grades the LISTED members. A rewrite outside the
|
||||
# family - one that sorts first, filters on pack NAME, or rounds - is not
|
||||
# covered, and the printed table is the exact extent of the claim.
|
||||
_DEEPEST_SIM = 50.0
|
||||
_reduction_rosters = [("baseline ", tuple(_MANY_FLOORS_SIM))]
|
||||
for _i in range(len(_MANY_FLOORS_SIM)):
|
||||
_fl = list(_MANY_FLOORS_SIM)
|
||||
_fl[_i] = _DEEPEST_SIM
|
||||
_reduction_rosters.append((f"deepest at index {_i} ", tuple(_fl)))
|
||||
|
||||
|
||||
def _sim_packs(floors):
|
||||
"""The same simulated roster shape 12c2 uses, at whatever floors are given."""
|
||||
return [Pack(f"sim-{i}", 50.0, f) for i, f in enumerate(floors)]
|
||||
|
||||
|
||||
_REDUCTION_FAMILY = {
|
||||
"min(floors)": lambda fl: min(fl),
|
||||
"floors[0] (== max(floors[:1]))": lambda fl: fl[0],
|
||||
"floors[-1] (== max(floors[-1:]))": lambda fl: fl[-1],
|
||||
"mean(floors)": lambda fl: sum(fl) / len(fl),
|
||||
"median(floors), upper": lambda fl: sorted(fl)[len(fl) // 2],
|
||||
"max(floors[:2])": lambda fl: max(fl[:2]),
|
||||
"max(floors[-2:])": lambda fl: max(fl[-2:]),
|
||||
"max(floors[:3])": lambda fl: max(fl[:3]),
|
||||
"max(floors[-3:])": lambda fl: max(fl[-3:]),
|
||||
"max(floors[1:])": lambda fl: max(fl[1:]),
|
||||
"max(floors[:-1])": lambda fl: max(fl[:-1]),
|
||||
"max(floors[1:-1])": lambda fl: max(fl[1:-1]),
|
||||
"max(floors[::2])": lambda fl: max(fl[::2]),
|
||||
"min(floors[-2:])": lambda fl: min(fl[-2:]),
|
||||
}
|
||||
_reduction_kills = {
|
||||
_nm: [_rn.strip() for _rn, _fl in _reduction_rosters if _fn(_fl) != max(_fl)]
|
||||
for _nm, _fn in _REDUCTION_FAMILY.items()}
|
||||
print(" THE ROSTER SET (all SIMULATED), and binding_soc_floor() on each:")
|
||||
for _rn, _fl in _reduction_rosters:
|
||||
print(f" {_rn} floors {[f'{f:.0f}' for f in _fl]} -> "
|
||||
f"{binding_soc_floor(_sim_packs(_fl), SOC_FLOOR):g} "
|
||||
f"(max() {max(_fl):g})")
|
||||
print(" THE REDUCTION FAMILY, and which roster separates each from max():")
|
||||
for _nm, _k in _reduction_kills.items():
|
||||
print(f" {_nm:<34} killed by: "
|
||||
+ ("; ".join(_k) if _k else "*** NOTHING IN THIS SET - SURVIVOR ***"))
|
||||
check("⚠️ THE FAMILY TABLE. Every listed rewrite of `max(floors)` answers "
|
||||
"something OTHER than `max` on at least one roster in this set - "
|
||||
"`max(floors[-2:])`, round 3's blocker, only on the roster whose deepest "
|
||||
"cut-out sits at index 0 or 1, which is precisely the data the single "
|
||||
"last-pack counterfactual above could not supply. A member with an empty "
|
||||
"kill list is a live survivor and takes THIS line red naming it, so "
|
||||
"adding a family member without a fixture that reaches it is not "
|
||||
"possible quietly. ⚠️ THE LISTED MEMBERS ONLY - the printed table is the "
|
||||
"extent of the claim",
|
||||
all(_reduction_kills.values()))
|
||||
check("...and `binding_soc_floor()` answers `max()` on EVERY roster in the set, "
|
||||
"which is what turns each separation above into a real mutation kill: "
|
||||
"rewrite the reduction as any listed member and it disagrees with this "
|
||||
"line on the roster named beside it. In particular the deepest cut-out is "
|
||||
"the answer at index 0, 1, 2 AND 3, so no positional window of the roster "
|
||||
"is what is being read",
|
||||
all(binding_soc_floor(_sim_packs(_fl), SOC_FLOOR) == max(_fl)
|
||||
for _rn, _fl in _reduction_rosters)
|
||||
and [binding_soc_floor(_sim_packs(_fl), SOC_FLOOR)
|
||||
for _rn, _fl in _reduction_rosters[1:]] == [_DEEPEST_SIM] * 4)
|
||||
check("PRECONDITION (habit 1): the set is five FOUR-pack rosters; the four "
|
||||
"derived ones each carry the SAME multiset of cut-outs with the deepest "
|
||||
"at a different position; every cut-out in every roster is strictly above "
|
||||
"`peak_soc_floor`, so `pack_floor_pct()` selects the cut-out and `floors` "
|
||||
"IS the tuple; and the deepest is UNIQUE in each, without which a "
|
||||
"positional slice could agree with max by accident",
|
||||
len(_reduction_rosters) == 5
|
||||
and all(len(_fl) == 4 for _rn, _fl in _reduction_rosters)
|
||||
and all(f > SOC_FLOOR for _rn, _fl in _reduction_rosters for f in _fl)
|
||||
and all(sorted(_fl) == sorted((_DEEPEST_SIM,) + _MANY_FLOORS_SIM[1:])
|
||||
or sorted(_fl) == sorted(_MANY_FLOORS_SIM[:1] + (_DEEPEST_SIM,)
|
||||
+ _MANY_FLOORS_SIM[2:])
|
||||
or sorted(_fl) == sorted(_MANY_FLOORS_SIM[:2] + (_DEEPEST_SIM,)
|
||||
+ _MANY_FLOORS_SIM[3:])
|
||||
or sorted(_fl) == sorted(_MANY_FLOORS_SIM[:3] + (_DEEPEST_SIM,))
|
||||
for _rn, _fl in _reduction_rosters[1:])
|
||||
and all(_fl.count(max(_fl)) == 1 for _rn, _fl in _reduction_rosters))
|
||||
|
||||
# ⚠️ AND THE FOUR-PACK SET HAS THE SAME CEILING AS EVERY OTHER FIXTURE: it
|
||||
# cannot separate `max(floors)` from `max(floors[:4])`, because at N=4 that
|
||||
# slice IS the list. This round's battery confirmed the identical shape one pack
|
||||
# along at the call site (`self.packs[:3]` survives a three-pack run), so it is
|
||||
# graded here rather than assumed away. `binding_soc_floor()` is a PURE function
|
||||
# over a list, which is the one place the sweep is cheap: rosters of length 1
|
||||
# through 12, the deepest cut-out at EVERY position of each, and the answer must
|
||||
# be the deepest every time. That kills every fixed-width head or tail window
|
||||
# narrower than the longest roster, at once, rather than one mutation at a time.
|
||||
_SWEEP_N = 12
|
||||
_SWEEP_SHALLOW, _SWEEP_DEEP = SOC_FLOOR + 5.0, SOC_FLOOR + 25.0
|
||||
_sweep_rows = []
|
||||
for _n in range(1, _SWEEP_N + 1):
|
||||
for _pos in range(_n):
|
||||
_fl = [_SWEEP_SHALLOW] * _n
|
||||
_fl[_pos] = _SWEEP_DEEP
|
||||
_sweep_rows.append((_n, _pos, tuple(_fl)))
|
||||
_sweep_bad = [(n, pos, fl) for n, pos, fl in _sweep_rows
|
||||
if binding_soc_floor(_sim_packs(fl), SOC_FLOOR) != max(fl)]
|
||||
_head_kill = {w: any(max(fl[:w]) != max(fl) for _n, _p, fl in _sweep_rows)
|
||||
for w in range(1, _SWEEP_N + 1)}
|
||||
_tail_kill = {w: any(max(fl[-w:]) != max(fl) for _n, _p, fl in _sweep_rows)
|
||||
for w in range(1, _SWEEP_N + 1)}
|
||||
print(f" LENGTH SWEEP (all SIMULATED): {len(_sweep_rows)} rosters, lengths 1"
|
||||
f"..{_SWEEP_N}, the {_SWEEP_DEEP:.0f} % cut-out at EVERY position of each "
|
||||
f"among {_SWEEP_SHALLOW:.0f} % siblings -> "
|
||||
f"{len(_sweep_rows) - len(_sweep_bad)} answer the deepest, "
|
||||
f"{len(_sweep_bad)} do not")
|
||||
print(" fixed-width windows killed by the sweep: head widths "
|
||||
+ ",".join(str(w) for w in sorted(_head_kill) if _head_kill[w])
|
||||
+ "; tail widths "
|
||||
+ ",".join(str(w) for w in sorted(_tail_kill) if _tail_kill[w])
|
||||
+ f"; NOT reached: head/tail width {_SWEEP_N} and wider")
|
||||
check("⚠️ THE LENGTH SWEEP. Over rosters of 1 to 12 packs with the deepest "
|
||||
"cut-out at every position of each, `binding_soc_floor()` answers the "
|
||||
"DEEPEST every time - so every head window `max(floors[:w])` and every "
|
||||
"tail window `max(floors[-w:])` of width 1 to 11 disagrees with it on at "
|
||||
"least one roster here, and that is the whole positional family below "
|
||||
"width 12 closed in one property rather than one mutation at a time",
|
||||
not _sweep_bad
|
||||
and len(_sweep_rows) == _SWEEP_N * (_SWEEP_N + 1) // 2
|
||||
and all(_head_kill[w] and _tail_kill[w] for w in range(1, _SWEEP_N)))
|
||||
check("⚠️ ...AND WIDTH 12 AND WIDER IS HONESTLY NOT REACHED, recorded rather "
|
||||
"than papered over. No roster in this file is longer than 12, so "
|
||||
"`max(floors[:12])` IS `max(floors)` on every one of them and no check "
|
||||
"here can tell them apart. A 13-pack roster would close width 12 and hand "
|
||||
"width 13 the same free pass: THE REGRESS DOES NOT TERMINATE IN A "
|
||||
"FIXTURE, which is this round's lesson and is why 12g's call site carries "
|
||||
"an EXACT STRUCTURAL pin alongside its runs. This line asserts the "
|
||||
"unreachedness itself, so a later sweep that lengthens the rosters takes "
|
||||
"it red and forces the sentence to be rewritten",
|
||||
not _head_kill[_SWEEP_N] and not _tail_kill[_SWEEP_N]
|
||||
and max(len(fl) for _n, _p, fl in _sweep_rows) == _SWEEP_N)
|
||||
|
||||
# ...and the EMS floor is still the other half of the conjunction: lift it above
|
||||
# every cut-out on the roster and it wins for all of them.
|
||||
_over = SOC_FLOOR + 40.0
|
||||
@@ -3584,23 +3747,34 @@ _floor_call = ast.unparse(next(k.value for k in _call.keywords
|
||||
print(f" main.py's decide(soc_floor=...) is `{_floor_call}`")
|
||||
|
||||
|
||||
def _floor_reaching_decide(tag, a_floor, b_floor, peak_floor=None):
|
||||
"""Drive ONE REAL `Controller.cycle()` on a TWO-pack roster and report the
|
||||
def _floor_reaching_decide(tag, *floors, peak_floor=None):
|
||||
"""Drive ONE REAL `Controller.cycle()` on an N-pack roster and report the
|
||||
floor `peakguard.decide()` was actually handed, read back off the decision
|
||||
main.py itself filed (`PeakDecision.soc_floor` is the argument, echoed).
|
||||
|
||||
⚠️ NOT A SPY AND NOT A GREP. The shipped `cycle()` runs, the shipped
|
||||
`binding_soc_floor()` runs, and the observable is a field of the decision
|
||||
the controller stored - so the whole path from `Controller.inverters` to the
|
||||
guard's argument is under test. Both packs are held at the SAME SoC and the
|
||||
guard's argument is under test. Every pack is held at the SAME SoC and the
|
||||
same everything else; the only things that vary between calls are the packs'
|
||||
own cut-outs.
|
||||
|
||||
⚠️ N IS A PARAMETER, AND THAT IS THIS ROUND'S BLOCKER 2. It used to be fixed
|
||||
at TWO, and a roster of two cannot distinguish a call site that reduces the
|
||||
ROSTER from one that reduces a WINDOW of two positions in it - `self.packs`
|
||||
and `self.packs[:2]` are the same list there, by exactly the argument 12c2
|
||||
makes about two packs being unable to separate max from min from first from
|
||||
last. The extra units are appended through `second_inverter()`, the same
|
||||
hook the two-pack runs use, one per floor past the first.
|
||||
"""
|
||||
opts = {} if peak_floor is None else {"peak_soc_floor": peak_floor}
|
||||
|
||||
def _prep(ctl):
|
||||
second_inverter(ctl)
|
||||
for inv, fl in zip(ctl.inverters, (a_floor, b_floor)):
|
||||
for _i in range(len(floors) - 1):
|
||||
_sfx = chr(ord("b") + _i)
|
||||
second_inverter(ctl, name=f"inverter-{_sfx}",
|
||||
setpoint=f"number.sp_{_sfx}")
|
||||
for inv, fl in zip(ctl.inverters, floors):
|
||||
inv.soc, inv.batt, inv.bms_soc_floor = SOC_BETWEEN, 0.0, fl
|
||||
|
||||
ctl, hs, _net, _rem = wired_over_limit(
|
||||
@@ -3652,13 +3826,16 @@ check("⚠️ THE CALL-SITE PIN, AS BEHAVIOUR. Change the cut-out of a NON-FIRST
|
||||
_g_shallow.soc_floor == float(SOC_FLOOR)
|
||||
and _g_deep.soc_floor == float(B_PACK_FLOOR_DEEP_SIM)
|
||||
and _g_deep.soc_floor != _g_shallow.soc_floor)
|
||||
check("⚠️ ...AND THE SAME PAIR SWAPPED GIVES THE SAME SITE FLOOR, so what is "
|
||||
"reduced is the ROSTER and not a POSITION in it. `self.packs[-1:]` - the "
|
||||
"LAST pack alone - agrees with the roster on both runs above and answers "
|
||||
"20 % here, where the deeper cut-out sits on the FIRST pack. That "
|
||||
"mutation SURVIVED the first cut of this fix round; this is the line "
|
||||
"that closes it, and between them the two directions leave no "
|
||||
"single-position slice that can pass all three runs",
|
||||
check("⚠️ ...AND THE SAME PAIR SWAPPED GIVES THE SAME SITE FLOOR, so no "
|
||||
"SINGLE-POSITION slice of the roster can produce these three answers. "
|
||||
"`self.packs[-1:]` - the LAST pack alone - agrees with the roster on both "
|
||||
"runs above and answers 20 % here, where the deeper cut-out sits on the "
|
||||
"FIRST pack. That mutation SURVIVED the first cut of this fix round and "
|
||||
"this is the line that closes it. ⚠️ AND THAT IS ALL THIS LINE SHOWS - "
|
||||
"NOT that the whole roster is read. At N=2 a two-position WINDOW is the "
|
||||
"roster: `self.packs[:2]` answers identically on all three runs above and "
|
||||
"walks straight through this check, +4 bytes, 19 files green. It is "
|
||||
"round 3's blocker 2, and the THREE-pack runs below are what reach it",
|
||||
_g_deepa.soc_floor == float(B_PACK_FLOOR_DEEP_SIM)
|
||||
and _g_deepa.soc_floor == _g_deep.soc_floor
|
||||
and _g_deepa.soc_floor != _g_shallow.soc_floor
|
||||
@@ -3693,6 +3870,197 @@ check("...and the precondition that makes the three runs comparable (habit 1): "
|
||||
== [A_PACK_FLOOR, B_PACK_FLOOR_SIM]
|
||||
and _g_ctl_deep.pack_floor_soc == _g_ctl_shallow.pack_floor_soc
|
||||
== _g_ctl_deepa.pack_floor_soc)
|
||||
# ⚠️ AND THREE RUNS ON A TWO-PACK ROSTER ARE STILL NOT ENOUGH, WHICH IS THIS
|
||||
# ROUND'S BLOCKER 2. The paragraph above states the TRUE claim - no
|
||||
# SINGLE-POSITION slice passes all three - and the check below it stated a
|
||||
# BROADER one, "what is reduced is the ROSTER and not a POSITION in it". The
|
||||
# broader one is false on this fixture: `self.packs[:2]` IS `self.packs` at a
|
||||
# roster of two, so it answers identically on every run above and SURVIVED all
|
||||
# 19 files (+4 bytes). The prose has been narrowed to what those three runs
|
||||
# reach; what follows is the data that reaches the rest.
|
||||
#
|
||||
# THE FIXTURE, and why it is shaped this way. Three REAL cycles on a THREE-pack
|
||||
# roster, the deep cut-out sitting at a DIFFERENT position each time - index 0,
|
||||
# index 1 (the interior one a two-pack roster has no room for) and index 2. Any
|
||||
# positional slice of `self.packs` is a proper subset of {0, 1, 2}, so it omits
|
||||
# at least one position, and on the run whose deep pack sits at that position it
|
||||
# sees only shallow cut-outs and answers the OPTION where the roster answers the
|
||||
# cut-out. That is the whole argument, and it is enumerated rather than asserted
|
||||
# from memory in the table below.
|
||||
#
|
||||
# ⚠️ SIMULATED. Two of the three units do not exist; inverter B is ~8 days out
|
||||
# and there is no inverter C at all. The shallow slots carry inverter A's
|
||||
# MEASURED 10 % cut-out and the deep one is the same SIMULATED 35 % the runs
|
||||
# above use. Nothing here is a measurement of a second or third pack.
|
||||
_G3_DEEP_SIM = B_PACK_FLOOR_DEEP_SIM
|
||||
_g3_runs = []
|
||||
for _pos in range(3):
|
||||
_fl3 = [A_PACK_FLOOR] * 3
|
||||
_fl3[_pos] = _G3_DEEP_SIM
|
||||
_ctl3, _dec3 = _floor_reaching_decide(f"n3p{_pos}", *_fl3)
|
||||
_g3_runs.append((f"3-pack, deep at index {_pos}", _fl3, _ctl3, _dec3))
|
||||
print(f" REAL THREE-pack cycles, all packs at {SOC_BETWEEN:.0f} %, "
|
||||
f"peak_soc_floor {SOC_FLOOR:.0f} %, the {_G3_DEEP_SIM:.0f} % cut-out "
|
||||
f"moved along the roster (units b and c are SIMULATED):")
|
||||
for _rn, _fl3, _ctl3, _dec3 in _g3_runs:
|
||||
print(f" {_rn}: cut-outs {[f'{f:.0f}' for f in _fl3]} % -> decide() "
|
||||
f"got soc_floor={_dec3.soc_floor:g} %, "
|
||||
f"floor_limited={_dec3.floor_limited}")
|
||||
check("⚠️ THE POSITIONAL PIN, AND IT NEEDS THREE PACKS TO EXIST. On a roster of "
|
||||
"THREE the floor that reaches `decide()` is the deep cut-out wherever on "
|
||||
"the roster that cut-out sits - index 0, index 1 and index 2 all answer "
|
||||
"35 %, and all three rosters carry the SAME multiset of cut-outs. A call "
|
||||
"site that handed `binding_soc_floor()` any PROPER SUBSET of the "
|
||||
"positions would answer the option, 20 %, on the run whose deep pack sits "
|
||||
"at the position it dropped. `self.packs[:2]` - the +4-byte mutation that "
|
||||
"walked through the two-pack runs above, because at N=2 it is the whole "
|
||||
"roster - goes red on the index-2 run",
|
||||
[r[3].soc_floor for r in _g3_runs]
|
||||
== [float(_G3_DEEP_SIM)] * 3
|
||||
and all(len(r[2].packs) == 3 for r in _g3_runs)
|
||||
and all(sorted(pk.bms_floor for pk in r[2].packs)
|
||||
== sorted([A_PACK_FLOOR, A_PACK_FLOOR, _G3_DEEP_SIM])
|
||||
for r in _g3_runs)
|
||||
and [[pk.bms_floor for pk in r[2].packs] for r in _g3_runs]
|
||||
== [r[1] for r in _g3_runs])
|
||||
check("...and the VERDICT flips with it, on all three: 25 % is at or below the "
|
||||
"35 % cut-out wherever it sits, so every one of these sites is "
|
||||
"FLOOR-LIMITED and sizes no forced discharge at all - where the "
|
||||
"all-shallow two-pack baseline above was permitted and sized a positive "
|
||||
"one. A slice that dropped the deep position would spend, through "
|
||||
"`sim/inject.py`, a pack its BMS stops",
|
||||
all(r[3].floor_limited is True and r[3].floor_w == 0.0
|
||||
and r[3].soc_floor_reason == FLOOR_AT_SOC_FLOOR for r in _g3_runs)
|
||||
and _g_shallow.floor_limited is False and _g_shallow.floor_w > 0.0)
|
||||
check("...and the precondition that makes the three comparable (habit 1): every "
|
||||
"pack in all three rosters is at the SAME state of charge, so neither the "
|
||||
"`pack_floor_soc` MINIMUM nor a roster position can be what separated the "
|
||||
"answers, and the deep cut-out really is above the EMS floor while the "
|
||||
"shallow one really is below it - two cut-outs on the same side of it "
|
||||
"would make every line above vacuous",
|
||||
all([pk.soc for pk in r[2].packs] == [SOC_BETWEEN] * 3 for r in _g3_runs)
|
||||
and len({r[2].pack_floor_soc for r in _g3_runs}) == 1
|
||||
and A_PACK_FLOOR < SOC_FLOOR < _G3_DEEP_SIM)
|
||||
|
||||
# ⚠️ AND THE ENUMERATION ITSELF, COMPUTED RATHER THAN CLAIMED. The lesson this
|
||||
# round is here to learn is that a fixture of N packs cannot separate reductions
|
||||
# that agree on N packs, so "no slice survives" is a claim about a FAMILY and a
|
||||
# SET OF RUNS and has to be graded as one. Below: every positional slice of the
|
||||
# roster, applied to the REAL `Controller.packs` each cycle above actually ran,
|
||||
# compared against the floor that REALLY reached `decide()` on that run. A slice
|
||||
# with an empty kill list is a survivor and this line goes red naming it.
|
||||
#
|
||||
# ⚠️ WHAT THIS DOES NOT CLAIM. It grades the members listed and nothing wider -
|
||||
# a rewrite that is not a positional slice (a different reduction, a filter on
|
||||
# pack NAME, a sort before the slice) is not covered here, and `min`/`mean`/the
|
||||
# rest of the reduction family are graded on the pure function in 12c2 instead.
|
||||
# The table is PRINTED so a reader can see exactly how far the claim reaches.
|
||||
_G_RUNS = ([("2-pack, no cut-out over the floor", _g_ctl_shallow, _g_shallow),
|
||||
("2-pack, deep at index 1", _g_ctl_deep, _g_deep),
|
||||
("2-pack, deep at index 0", _g_ctl_deepa, _g_deepa)]
|
||||
+ [(rn, ctl, dec) for rn, _fl, ctl, dec in _g3_runs])
|
||||
_SLICE_FAMILY = {
|
||||
"self.packs[:1]": lambda ps: ps[:1],
|
||||
"self.packs[-1:]": lambda ps: ps[-1:],
|
||||
"self.packs[:2]": lambda ps: ps[:2],
|
||||
"self.packs[-2:]": lambda ps: ps[-2:],
|
||||
"self.packs[1:]": lambda ps: ps[1:],
|
||||
"self.packs[:-1]": lambda ps: ps[:-1],
|
||||
"self.packs[1:-1]": lambda ps: ps[1:-1],
|
||||
"self.packs[::2]": lambda ps: ps[::2],
|
||||
}
|
||||
_slice_kills = {
|
||||
_nm: [rn for rn, ctl, dec in _G_RUNS
|
||||
if binding_soc_floor(_fn(ctl.packs), SOC_FLOOR) != dec.soc_floor]
|
||||
for _nm, _fn in _SLICE_FAMILY.items()}
|
||||
print(" THE POSITIONAL-SLICE FAMILY at this call site, and which run "
|
||||
"separates each from the whole roster:")
|
||||
for _nm, _k in _slice_kills.items():
|
||||
print(f" {_nm:<18} killed by: "
|
||||
+ ("; ".join(_k) if _k else "*** NOTHING HERE - SURVIVOR ***"))
|
||||
check("⚠️ EVERY positional slice in the enumerated family answers something "
|
||||
"OTHER than the floor that really reached `decide()` on at least one of "
|
||||
"the six runs above - and the two three-pack runs at index 2 and index 0 "
|
||||
"are what kill `[:2]` and `[-2:]`, which the two-pack runs structurally "
|
||||
"could not. The kill list is computed against the REAL `Controller.packs` "
|
||||
"each cycle ran and the REAL `PeakDecision.soc_floor` it produced, so a "
|
||||
"member with an empty list is a live survivor and takes this line red "
|
||||
"naming it. This grades the LISTED members only; the printed table is its "
|
||||
"extent",
|
||||
all(_slice_kills.values()))
|
||||
check("...and the baseline the table is measured against is the shipped call "
|
||||
"site's OWN answer, not a re-derivation: on every run, the floor that "
|
||||
"reached `decide()` equals `binding_soc_floor()` over the WHOLE roster "
|
||||
"that cycle carried. If it did not, every kill list above would be "
|
||||
"measuring the wrong thing",
|
||||
all(dec.soc_floor == binding_soc_floor(ctl.packs, SOC_FLOOR)
|
||||
for _rn, ctl, dec in _G_RUNS)
|
||||
and len(_G_RUNS) == 6
|
||||
and sorted(len(ctl.packs) for _rn, ctl, dec in _G_RUNS) == [2, 2, 2, 3, 3, 3])
|
||||
|
||||
# ⚠️ AND HERE IS THE HONEST LIMIT OF EVERY FIXTURE ABOVE, FOUND BY THIS ROUND'S
|
||||
# OWN BATTERY AND NOT ARGUED FROM: `self.packs[:3]` and `self.packs[-3:]` SURVIVE
|
||||
# all six behavioural runs, +4 and +5 bytes, and they survive for the same reason
|
||||
# `[:2]` survived the two-pack runs - THE LONGEST ROSTER HERE IS THREE, and a
|
||||
# slice that keeps three consecutive positions IS the roster at N=3. Adding a
|
||||
# four-pack run would close those two and hand `[:4]` and `[-4:]` the same free
|
||||
# pass. THE REGRESS DOES NOT TERMINATE IN A FIXTURE. A bounded roster cannot
|
||||
# grade an unbounded family of slices, and pretending otherwise by adding one
|
||||
# more pack is precisely the move that has been rejected twice on this card.
|
||||
#
|
||||
# So the two halves are separated and each says what it reaches:
|
||||
#
|
||||
# the RUNS above grade the VALUE - that the floor reaching `decide()` really
|
||||
# is the roster's deepest cut-out, wherever on the roster it sits, and that
|
||||
# the site's verdict follows it. They reach every positional slice up to N=3
|
||||
# and, by construction, nothing beyond.
|
||||
#
|
||||
# the PIN below grades the ARGUMENT'S IDENTITY - a claim genuinely about the
|
||||
# code's shape, so it is graded on the code's shape, exactly, at ANY N. It is
|
||||
# NOT the substring test this part replaced: `"self.packs" in _floor_call` is
|
||||
# true of every slice, whereas `ast.unparse(arg) == "self.packs"` is false of
|
||||
# all of them. `self.packs[:3]` unparses to `self.packs[:3]`.
|
||||
#
|
||||
# ⚠️ AND THE PIN IS BLIND TO TWO THINGS THE RUNS ARE NOT, which is why both are
|
||||
# here. It cannot see a change to what `Controller.packs` RETURNS - a property
|
||||
# rewritten as `self.inverters[:2]` leaves this expression identical, and it is
|
||||
# the three-pack runs' `len(ctl.packs) == 3` that goes red on it. And it cannot
|
||||
# see the reduction INSIDE `binding_soc_floor()` at all; that is 12c2's.
|
||||
_floor_node = next(k.value for k in _call.keywords if k.arg == "soc_floor")
|
||||
_floor_roster_arg = (_floor_node.args[0]
|
||||
if isinstance(_floor_node, ast.Call) and _floor_node.args
|
||||
else None)
|
||||
print(f" the ROSTER argument main.py reduces is "
|
||||
f"`{ast.unparse(_floor_roster_arg)}`, an AST "
|
||||
f"{type(_floor_roster_arg).__name__}")
|
||||
check("⚠️ THE STRUCTURAL HALF, AND IT IS EXACT RATHER THAN A SUBSTRING. The "
|
||||
"roster handed to `binding_soc_floor()` is the WHOLE property "
|
||||
"`self.packs` - an attribute of self, not a Subscript, not a call, not a "
|
||||
"comprehension - so EVERY slice of it is red here at every roster length, "
|
||||
"including `self.packs[:3]` and `self.packs[-3:]`, which survive all six "
|
||||
"runs above because the longest roster they drive is three packs long. "
|
||||
"This grades the code's SHAPE and nothing about the values; what the "
|
||||
"expression MEANS is graded by the runs, and which option key it reads is "
|
||||
"pinned in part 4",
|
||||
isinstance(_floor_node, ast.Call)
|
||||
and ast.unparse(_floor_node.func) == "peakguard.binding_soc_floor"
|
||||
and len(_floor_node.args) == 2 and not _floor_node.keywords
|
||||
and isinstance(_floor_roster_arg, ast.Attribute)
|
||||
and isinstance(_floor_roster_arg.value, ast.Name)
|
||||
and _floor_roster_arg.value.id == "self"
|
||||
and _floor_roster_arg.attr == "packs"
|
||||
and ast.unparse(_floor_roster_arg) == "self.packs")
|
||||
check("...and the counterfactual that shows this pin is not vacuous (habit 7): "
|
||||
"the very slices it exists for really do unparse to something else, so "
|
||||
"the equality above is doing work rather than being trivially true of "
|
||||
"anything shaped like an argument",
|
||||
all(ast.unparse(ast.parse(f"self.packs{sl}", mode="eval").body)
|
||||
!= "self.packs"
|
||||
for sl in ("[:1]", "[-1:]", "[:2]", "[-2:]", "[:3]", "[-3:]",
|
||||
"[1:]", "[:-1]", "[1:-1]", "[::2]"))
|
||||
and ast.unparse(ast.parse("list(reversed(self.packs))",
|
||||
mode="eval").body) != "self.packs")
|
||||
|
||||
# ...and the OTHER half of the conjunction still reaches the same argument, so
|
||||
# the reduction did not replace the source: move `peak_soc_floor` itself, with
|
||||
# both cut-outs held under it, and the floor follows the OPTION.
|
||||
@@ -4046,6 +4414,94 @@ MUT.append(("main.py grading the site against ONE roster position - "
|
||||
"than a position. ⚠️ A substring test over main.py cannot see a "
|
||||
"slice; MUTATION.md habit 4"))
|
||||
|
||||
# ---- and the TWO ROUND-3 SURVIVORS, the same defect one pack along -----------
|
||||
# ⚠️ BOTH SURVIVED THE ROUND-2 FIX, and both are the family law above: a fixture
|
||||
# of N packs cannot separate reductions that agree on N packs. Round 2 closed
|
||||
# `min(floors)` and the single-position slices and then stated, in the check
|
||||
# text, a BROADER claim than its data could reach - "the reduction reads every
|
||||
# entry", "what is reduced is the ROSTER and not a POSITION". The two rewrites
|
||||
# below satisfy every fixture round 2 had while making both of those sentences
|
||||
# false. The prose has been cut back to what the old data reached and new data
|
||||
# added for the rest; that is the whole of round 3.
|
||||
|
||||
# 24. `max(floors)` -> `max(floors[-2:])`, +5 bytes, green across all 19 files
|
||||
# on 8501e05. Entries 0 and 1 are never read, so a roster of >= 3 can be
|
||||
# graded against a floor BELOW its deepest cut-out - the same safety
|
||||
# inversion as `min(floors)`, one pack along. It survived because 12c2's
|
||||
# only counterfactual varied the LAST pack, and every window ending at the
|
||||
# roster's end follows that. 12c2's roster SET reaches it.
|
||||
MUT.append(("`binding_soc_floor()` reduced over a WINDOW - `max(floors[-2:])` - "
|
||||
"ROUND 3 SURVIVOR 1, +5 bytes",
|
||||
binding_soc_floor(_sim_packs(_reduction_rosters[1][1]), SOC_FLOOR)
|
||||
== _DEEPEST_SIM
|
||||
and max(_reduction_rosters[1][1][-2:]) != _DEEPEST_SIM
|
||||
and bool(_reduction_kills["max(floors[-2:])"])
|
||||
and all(_reduction_kills.values()),
|
||||
"part 12c2's FAMILY TABLE: the same four cut-outs with the deepest "
|
||||
"moved to each of the four positions in turn, and every listed "
|
||||
"rewrite separated from max() by at least one of them. ⚠️ A SINGLE "
|
||||
"counterfactual cannot do this - it can only show that ONE position "
|
||||
"is read"))
|
||||
|
||||
# 25. `binding_soc_floor(self.packs, ...)` -> `self.packs[:2]`, +4 bytes, green
|
||||
# across all 19 files on 8501e05. Every `_floor_reaching_decide` run in 12g
|
||||
# drove a TWO-pack roster, where `[:2]` IS the roster, so no run could see
|
||||
# it - and 12g's own check said so about two packs and max/min/first/last
|
||||
# while claiming otherwise about itself. Three-pack runs with the deep
|
||||
# cut-out at index 0, 1 and 2 reach it.
|
||||
MUT.append(("main.py grading the site against a WINDOW of roster positions - "
|
||||
"`self.packs[:2]` - ROUND 3 SURVIVOR 2, +4 bytes",
|
||||
_g3_runs[2][3].soc_floor == float(_G3_DEEP_SIM)
|
||||
and binding_soc_floor(_g3_runs[2][2].packs[:2], SOC_FLOOR)
|
||||
== float(SOC_FLOOR)
|
||||
and all(r[3].soc_floor == float(_G3_DEEP_SIM) for r in _g3_runs)
|
||||
and all(_slice_kills.values()),
|
||||
"part 12g's THREE-pack runs and their POSITIONAL-SLICE TABLE: the "
|
||||
"deep cut-out at index 0, 1 and 2 of a three-pack roster, so every "
|
||||
"proper subset of the positions drops the deep one on some run. "
|
||||
"⚠️ TWO packs are structurally blind to this; `[:2]` is the whole "
|
||||
"roster there"))
|
||||
|
||||
# 26. ...AND THE TWO THE BATTERY FOUND WHILE CLOSING THOSE. `self.packs[:3]`
|
||||
# (+4) and `self.packs[-3:]` (+5) survive ALL SIX behavioural runs in 12g,
|
||||
# because the longest roster those runs drive is three packs long and a
|
||||
# three-wide window IS that roster. This is the fourth turn of the same
|
||||
# screw: `[:1]` needed two packs, `[:2]` needed three, `[:3]` needs four,
|
||||
# and adding a fourth pack would hand `[:4]` the free pass. They are closed
|
||||
# STRUCTURALLY instead - the roster argument must unparse to exactly
|
||||
# `self.packs` - and the row asserts BOTH the pin and the reason it was
|
||||
# needed, so a later edit that deletes the pin cannot leave this green.
|
||||
MUT.append(("main.py grading the site against a THREE-wide window - "
|
||||
"`self.packs[:3]` / `self.packs[-3:]`, found by THIS round's "
|
||||
"battery, invisible to every behavioural run in this file",
|
||||
ast.unparse(_floor_roster_arg) == "self.packs"
|
||||
and isinstance(_floor_roster_arg, ast.Attribute)
|
||||
and all(binding_soc_floor(ctl.packs[:3], SOC_FLOOR) == dec.soc_floor
|
||||
and binding_soc_floor(ctl.packs[-3:], SOC_FLOOR)
|
||||
== dec.soc_floor for _rn, ctl, dec in _G_RUNS),
|
||||
"part 12g's STRUCTURAL PIN, and ONLY that - the runs cannot see it "
|
||||
"and this row asserts that they cannot. ⚠️ A bounded roster cannot "
|
||||
"grade an unbounded family of slices; one more pack moves the hole "
|
||||
"rather than closing it"))
|
||||
|
||||
# 27. AND THE ONE THAT IS NOT CLOSED. `max(floors[:12])` and every wider window
|
||||
# inside `binding_soc_floor()` are INVISIBLE to this file: the length sweep
|
||||
# runs to twelve packs, so a twelve-wide window is the whole list on every
|
||||
# roster it drives. Unlike the call site there is no identity claim to pin
|
||||
# here - the claim is semantic, "the maximum", and a shape pin would refuse
|
||||
# honest refactors of the expression. Recorded as open, with its size: it
|
||||
# needs a roster of THIRTEEN packs to become observable, on a site whose
|
||||
# roster is currently ONE and whose second unit is ~8 days out.
|
||||
MUT.append(("`binding_soc_floor()` reduced over a window 12 packs wide or "
|
||||
"wider - NOT CAUGHT, and it takes a 13-pack roster to reach",
|
||||
_head_kill.get(_SWEEP_N, False) or _tail_kill.get(_SWEEP_N, False),
|
||||
"NOTHING CATCHES IT, on purpose. The sweep closes widths 1-11 and "
|
||||
"says so; width 12 is where this file's data stops. ⚠️ Two further "
|
||||
"rewrites are EQUIVALENT rather than uncaught - `max(set(floors))` "
|
||||
"and `list(reversed(self.packs))` cannot change any answer, because "
|
||||
"max is order- and duplicate-invariant; the second is nonetheless "
|
||||
"red on 12g's structural pin"))
|
||||
|
||||
for label, caught, where in MUT:
|
||||
print(f" {'caught' if caught else 'NOT CAUGHT':>10} {label}")
|
||||
print(f" {where}")
|
||||
@@ -4066,17 +4522,33 @@ check("...and SAFETY-32's own eight defeats are each caught too - the flat "
|
||||
"cut-out defaulted to 0 %, rule 8 grading one unit, rule 8 naming a "
|
||||
"hardwired one, and the alarm naming a position instead of a pack",
|
||||
all(m[1] for m in MUT[13:21]))
|
||||
check("...⚠️ AND SO ARE THE FOUR DEFEATS THAT SURVIVED A GREEN 19-FILE SUITE, "
|
||||
"which is why this fix round exists: `min(floors)` in place of "
|
||||
"`max(floors)` (zero byte delta) and `self.packs[:1]` at the call site "
|
||||
"(+4 bytes), both green on d9388c8; `self.packs[-1:]` (+5 bytes), green "
|
||||
"on the FIRST CUT OF THE FIX ITSELF; and the empty-roster branch "
|
||||
"rewritten (-43 bytes). None of the four is a new guard - no shipped "
|
||||
"behaviour changed - they are checks whose DATA could not reach the "
|
||||
"failure they named, which is the defect this repository has now shipped "
|
||||
"in six consecutive cards. The last two were found by this round's own "
|
||||
"battery and are recorded rather than quietly repaired",
|
||||
all(m[1] for m in MUT[21:24]) and len(MUT) == 24)
|
||||
check("...⚠️ AND SO ARE THE SEVEN DEFEATS THAT SURVIVED A GREEN 19-FILE SUITE, "
|
||||
"which is why this card is on its third fix round: `min(floors)` in place "
|
||||
"of `max(floors)` (zero byte delta) and `self.packs[:1]` at the call site "
|
||||
"(+4 bytes), both green on d9388c8; `self.packs[-1:]` (+5 bytes) and the "
|
||||
"empty-roster branch rewritten (-43 bytes), green on the FIRST CUT OF THE "
|
||||
"FIX; `max(floors[-2:])` (+5) and `self.packs[:2]` (+4), both green on "
|
||||
"8501e05 - THE ROUND-2 FIX ITSELF; and `self.packs[:3]` / "
|
||||
"`self.packs[-3:]`, green on the first cut of ROUND 3 and found by its "
|
||||
"own battery. None of the seven is a new guard; no shipped behaviour "
|
||||
"changed. Every one is a check whose DATA could not reach the failure its "
|
||||
"TEXT named - the defect this repository has now shipped in six "
|
||||
"consecutive cards and, twice running, inside the fix written to close "
|
||||
"it. The last five were found by a battery rather than by argument, "
|
||||
"which is the only thing that has ever found any of them",
|
||||
all(m[1] for m in MUT[21:27]) and len(MUT) == 28)
|
||||
check("...⚠️ AND ONE IS RECORDED AS NOT CAUGHT, which is the only honest row "
|
||||
"this round could write for it: a reduction over a window TWELVE packs "
|
||||
"wide is indistinguishable from `max(floors)` on every roster in this "
|
||||
"file, because the length sweep stops at twelve. Thirteen packs would "
|
||||
"close it and open thirteen. The call site's half of the same regress is "
|
||||
"closed by an exact structural pin because the claim there is an IDENTITY "
|
||||
"('this roster'); the claim here is SEMANTIC ('the maximum') and a shape "
|
||||
"pin would refuse honest refactors, so the hole is reported with its size "
|
||||
"instead of hidden. THIS is the row that a fifth review should argue "
|
||||
"with, and it exists to be argued with",
|
||||
not MUT[27][1]
|
||||
and all(_head_kill[w] and _tail_kill[w] for w in range(1, _SWEEP_N)))
|
||||
check("...and so is the last one, which is not a defeat at all but the EDGE OF "
|
||||
"THIS CARD: the grid-following loop can still take the pack past this "
|
||||
"floor, because the floor bounds the peak guard's own forced discharge "
|
||||
|
||||
Reference in New Issue
Block a user