SAFETY-32: bms_soc_floor per pack, rule 8 per unit #48

Merged
admin merged 5 commits from SAFETY-32 into release/1.0 2026-09-05 08:10:51 +02:00
5 changed files with 1106 additions and 1 deletions
Showing only changes of commit 8beba0a3e7 - Show all commits
+65
View File
@@ -302,6 +302,71 @@ thing that stops. Rule 8's own failure mode, reached through rule 8.
cannot permit anything either way because `pack_floor_soc` is `None` at an
empty roster.
* ⚠️ **THIRD FIX ROUND — the same family was alive at the SIBLING ARGUMENT of
the same call.** Rounds 2 and 3 hardened the FLOOR axis; `decide()` is handed
a second reduction over the same roster beside it, `soc=self.pack_floor_soc`,
and `peakguard.py`'s own docstring names the two as a pair. Three rewrites of
`Controller.pack_floor_soc` were green across all 19 files on `52380c0` and
again after the rebase onto `3934ad7`: `min(float(v) for v in vals)` →
`vals[:2]` (+4), `vals[-2:]` (+5) and `vals[:3]` (+4), while `[:1]`, `[-1:]`,
`[1:]`, `[:-1]`, `max()` and the mean were all red. **The suite's separating
power on the SoC axis stopped at exactly N=2** — the state the floor axis was
in before round 3. It changes a real answer: a three-pack roster at
50 / 60 / 11 % with the emptiest pack THIRD answers 11 % shipped and 50 %
mutated, so the site is graded for discharge PERMISSION against a pack 39
points fuller than the emptiest and spends a pack its own BMS stops. Round 3's
machinery transfers directly — new **part 12i**: six real `cycle()`s with the
emptiest pack at every position of a three-pack roster and both positions of a
two-pack one (the observable read off `PeakDecision.soc`, cut-outs held flat
so the floor axis cannot be what moved the answers); computed slice and
non-slice tables that go red naming any member nothing kills; a **length
sweep** of 78 real rosters, lengths 1–12, closing head and tail windows of
width 1–11 and recording width 12 as honestly unreached; a **none-guard
sweep** over the same 78; and **three exact structural pins** — the `vals`
comprehension must iterate the bare `self.inverters`, and both `any()` and
`min()` must reduce the whole `vals` — which close every slice width at every
roster length. No shipped behaviour changed; only what observes it.
* ⚠️ **SPIKE-04: production is DEGENERATE on the floor axis, so the
differing-floor fixtures are the entire exposure.** Pack B is 4 × Dyness
DL5.0C, DoD 90 → floor 10 % — **FROM THE DATASHEET AND THE SERIAL; inverter B
does not exist and nothing about it is measured.** Pack A is DoD 90 → 10 % as
well, and that one *is* measured. Both packs therefore floor at the same value
in the field, `max(10, 10)` is 10 whatever it reduces, and a differing floor
exists **only in the fixtures**. That is the argument for keeping them, not for
simplifying them: anyone who collapses `A_PACK_FLOOR != B_PACK_FLOOR_SIM` to
one number deletes the only data this repository has that can see the
reduction at all, and part 12c2's precondition check goes red if they do. The
**SoC** axis has no such degeneracy — two batteries at the same state of
charge is a coincidence, not a configuration — which is what makes
`pack_floor_soc` the half of the pair that will be live from the day inverter
B is wired up.
* ⚠️ **The FAMILY enumerated rather than the member closed, and it found four
more survivors in code this card never touched.** Every reduction over
`self.inverters` / `self.packs` in `Controller` was found from the AST and
mutated to a slice against the full suite. Eighteen were already graded
(`site_batt_w`, `site_rating_w`, `site_max_w`, `site_dev_bound`,
`site_circulating_w`, `inputs_ok`, `units`, `Controller.packs`, `maint_unit`,
the maintenance-due minimum, the store-migration roster, `validate_unit_ranges`
and the round-2/3 sites). **Four were not, and three of them are SAFETY-30's,
all `any(i.sign_wd.tripped for i in self.inverters)`** — `cycle()`'s
stale-input hold, `publish()`'s status vocabulary and `status_payload()`'s
banner — each +4 bytes and green across all 19 files, for the reason every
blocker on this card was invisible: **the only fixture that reached them was a
roster of ONE, where `self.inverters[:1]` IS `self.inverters`.** The first has
teeth: a latched unit must take the roster past that hold or its `failsafe`
SET stops being re-filed the moment a poll is missed, which is main.py's own
sentence for it. New **test_watchdog.py part 8** grades all three with the
latch at EACH position plus a no-latch counterfactual, and new **part 12j**
pins all 26 roster comprehensions in `Controller` to iterating the roster
whole — so a reduction added over a slice anywhere in the class is red on the
line it is written, with no fixture required. Two rows are reported open
rather than closed: `_grade_store_migration()`'s second disjunct (now red on
12j, and argued to be an equivalent mutant because a unit tripped at startup
implies its namespaced key is set) and `cycle()`'s undeliverable-unit **log
line**, where `sorted(...)[:1]` (+4 bytes) is still green — it truncates names
in one event message; the refusal itself is a different expression and is
graded, so the site still stops.
⚠️ **No measurement of inverter B appears anywhere in this change.** It does not
exist yet. Every second-pack figure — in fixtures, in the probe, in
config.yaml's commented example — is **simulated and labelled**; only inverter
@@ -311,6 +311,173 @@ refuses the two-model config that used to start; the permission is answered per
pack, so the alarm names the pack that stopped the site rather than "the
battery"; and an entry with no stated cut-out is withheld instead of defaulted.
## 4b. ⚠️ ROUND 4 — the sibling argument, and SPIKE-04 making this the live axis
Rounds 2 and 3 hardened the **floor** axis: the `max` inside
`binding_soc_floor()`, the roster handed to it, `Controller.packs`, and
`pack_floor_pct()`'s conjunction. Round 4's blocker is the same family at the
**sibling argument of the same call**:
```python
self.peak_guard = peakguard.decide(
...,
soc=self.pack_floor_soc, # MINIMUM <- round 4
soc_floor=peakguard.binding_soc_floor(self.packs, ...), # MAXIMUM <- rounds 2-3
```
`peakguard.py`'s own docstring names them as a pair — *"MAXIMUM here pairs with
the MINIMUM in `pack_floor_soc`"* — and a conjunction is exactly as strong as
its weaker half. On `52380c0`, with all 19 files green and verified again after
the rebase onto `3934ad7`:
| mutation in `Controller.pack_floor_soc` | bytes | before round 4 | now |
|---|---|---|---|
| `min(float(v) for v in vals[:2])` | +4 | **GREEN** | RED |
| `min(float(v) for v in vals[-2:])` | +5 | **GREEN** | RED |
| `min(float(v) for v in vals[:3])` | +4 | **GREEN** | RED |
| `vals[:1]`, `vals[-1:]`, `vals[1:]`, `vals[:-1]`, `max(vals)`, the mean | | RED | RED |
The suite's separating power on the SoC axis stopped at exactly **N = 2** —
precisely the state the floor axis was in before round 3, and which round 3
itself named as its blocker 2. A fixture of N packs cannot separate reductions
that agree on N packs.
**It changes a real answer.** A three-pack roster at 50 / 60 / 11 %, emptiest
pack **third**: the shipped property answers 11 %, `vals[:2]` answers 50 %. The
site is then graded for discharge *permission* against a pack 39 points fuller
than the emptiest, and spends a pack its own BMS stops — through
`sim/inject.py`, which runs no validator rule at all. The verdict flips with it:
11 % is below the 20 % EMS floor, so the shipped site is floor-limited and sizes
no forced discharge, where the mutant is permitted and sizes a positive one.
### ⚠️ SPIKE-04 makes the differing-floor discipline the entire exposure
SPIKE-04 reads pack B as **4 × Dyness DL5.0C, DoD 90 → floor 10 %** — **FROM THE
DATASHEET AND THE SERIAL. Inverter B does not physically exist (~8 days out) and
nothing about it has been measured.** Pack A is DoD 90 → 10 % as well, and *that
one is measured*, off register `0x0560` on the reference GW5000S-BP.
So **production is degenerate on the floor axis**: both packs floor at the same
value, `max(10, 10) == 10`, and a differing floor exists **only in the
fixtures**. That is not an argument for simplifying the fixtures to matching
values — it is the argument for keeping them. `binding_soc_floor()`'s reduction
is observable *nowhere else*, and the moment a third pack, a replacement pack or
a different chemistry arrives it is observable in the field. **Anyone who
"simplifies" `A_PACK_FLOOR != B_PACK_FLOOR_SIM` to one number deletes the only
data this repository has that can see the reduction at all**; part 12c2's
precondition check goes red if they do, and this paragraph is why.
The **SoC axis has no such degeneracy**. Two batteries at the same state of
charge is a coincidence, not a configuration, so `pack_floor_soc` is the half of
the pair that will be non-degenerate in the field from the day inverter B is
wired up.
### The treatment, transferred from round 3
* **the roster SET** — six real `Controller.cycle()` runs, the emptiest pack at
every position of a three-pack roster and both positions of a two-pack one,
the observable read off `PeakDecision.soc` (the argument, echoed) rather than
off a spy or a grep. Cut-outs held flat across all of them, so the floor axis
cannot be what moved the answers.
* **the positional-slice table and the non-slice table** — computed against the
real `Controller.inverters` each cycle carried and the real decision it
produced, printed, with a member that nothing kills taking the check red.
* **the length sweep** — the real property on real rosters of 1 to 12 inverters,
the empty pack at every position. Closes head and tail windows of width 1-11
at once. Width 12 and wider is **honestly not reached**, and asserted to be
unreached so a later sweep that lengthens the rosters must rewrite the
sentence.
* **the exact structural pin** — three of them, because there are three
reductions over roster length in this one property: `vals` is built by one
comprehension over the bare `self.inverters`; `any(... for v in vals)` reduces
the whole list; `min(... for v in vals)` reduces the whole list. Every slice
of either is red at **every** roster length, including the `[:3]` and `[:12]`
the runs and the sweep cannot see.
Unlike the floor axis, **there is no uncaught row here**: the claim at
`pack_floor_soc` is an *identity* ("this list"), so a shape pin is the right
instrument, where `binding_soc_floor()`'s claim is *semantic* ("the maximum")
and a shape pin there would refuse honest refactors. That asymmetry is why one
carries an open row and the other does not.
## 4c. ⚠️ THE ENUMERATION — what OTHER reductions over roster length are graded
This card has now been rejected three times for the same shape one step over, so
round 4 stopped closing members and enumerated the **family**. Every reduction
over `self.inverters` / `self.packs` in `Controller` was found from the AST and
mutated to a slice, one at a time, against the full 19-file suite.
| # | site | reduction | consumer | mutation | result |
|---|---|---|---|---|---|
| 1 | `pack_floor_soc` | `min` over SoC | `decide(soc=)`, `arbitrage.decide(soc=)` | `vals[:2]` +4 | **was GREEN → now RED** (12i) |
| 2 | `pack_floor_soc` | `any(v is None)` | same | `vals[:1]` +4 | RED (raises in 12d; pinned in 12i) |
| 3 | `pack_floor_soc` | the `vals` comprehension | same | `self.inverters[:2]` +4 | RED (12i sweep + pin) |
| 4 | `binding_soc_floor` | `max` over floors | `decide(soc_floor=)` | `min`, windows | RED (12c2, round 2-3) |
| 5 | call site | the roster argument | same | `self.packs[:1..3]` | RED (12g, round 3) |
| 6 | `Controller.packs` | the comprehension | `binding_soc_floor`, `pack_permissions` | `self.inverters[:2]` +4 | RED (12g three-pack runs) |
| 7 | `site_batt_w` | `sum` + `any(None)` | `decide(batt_w=)` — sizes the floor | `self.inverters[:1]` +4 | RED (test_inverter.py) |
| 8 | `site_rating_w` | `sum` of per-unit conjunction | `decide(achievable_w=)`, freeze rail | `[:1]` +4 | RED (test_inverter.py) |
| 9 | `site_max_w` | `sum` of `max_w` | the site loop's supervised bound | `[:1]` +4 | RED (test_inverter.py) |
| 10 | `site_dev_bound` | `sum` + `any(None)` | `looks_frozen`, `rail_unreachable` | `[:1]` +4 | RED (test_inverter.py) |
| 11 | `site_circulating_w` | `circulating_w` over measured power | SAFETY-31 trip | `[:1]` +4 | RED (test_watchdog.py) |
| 12 | `inputs_ok` | `all` over both readings | gates the whole cycle (§11.1 rule 1) | `[:1]` +4 | RED (test_inverter.py) |
| 13 | `units` | `tuple` of names | the arbiter's scope table | `[:1]` +4 | RED (5 files) |
| 14 | `status_payload` | `min(_dues)` over `self.maints` | the operator's "maintenance due" row | `_dues[:1]` +4 | RED (test_maintenance.py) |
| 15 | `maint_unit` | `self.inverters[self.maint_index]` | which pack the FSM drives | `[0]` −15 | RED (test_maintenance.py) |
| 16 | store migration | the roster name list | MAINT-05's key migration | `[:1]` +4 | RED (test_maintenance.py) |
| 17 | `validate_unit_ranges` | the roster argument | startup refusal | `[:1]` +4 | RED (test_inverter.py) |
| 18 | `cycle()` stale-input hold | `any(sign_wd.tripped)` | **a latched unit's failsafe SET** | `[:1]` +4 | **was GREEN → now RED** (test_watchdog.py part 8) |
| 19 | `publish()` status | `any(sign_wd.tripped)` | the MQTT status vocabulary | `[:1]` +4 | **was GREEN → now RED** (part 8) |
| 20 | `status_payload()` banner | `any(sign_wd.tripped)` | the one headline on the page | `[:1]` +4 | **was GREEN → now RED** (part 8) |
| 21 | `_grade_store_migration` | `any(sign_wd.tripped)` | SAFETY-02's re-arm guard | `[:1]` +4 | was GREEN → now RED (12j), see below |
| 22 | `cycle()` undeliverable list | `sorted(...)` over shares | the *text* of one event line | `[:1]` +4 | **STILL GREEN — honest gap, below** |
**Rows 18-20 are the finding, and they are not this card's code.** All three are
`any(i.sign_wd.tripped for i in self.inverters)`, all three are SAFETY-30's, and
all three survived a green 19-file suite for exactly the reason every blocker on
this card survived: *the only fixture that reached them was a roster of ONE,
where `self.inverters[:1]` IS `self.inverters`.* Part 3 of test_watchdog.py has
built a two-inverter roster with only inverter B latched since SAFETY-30
shipped — the precise data all three needed — and none of them read it.
Row 18 is the one with teeth. A latched unit must take the whole roster past the
stale-input hold, because that unit's `failsafe` SET is the thing parking it;
main.py's own comment says *"the trip would stop acting the moment a poll was
missed"*. With `[:1]`, a latched inverter B plus a one-cycle gap in inverter A's
SoC returns early, and B's last share stands for the heartbeat to re-emit.
test_watchdog.py part 8 now drives that with the latch at **each** position, plus
the no-latch counterfactual that proves the hold really fires.
**Row 21 — graded structurally, and argued to be redundant.** The `[:1]` there
is now red on 12j's enumeration, but I could not construct a *reachable* state in
which it changes an answer: `_grade_store_migration()` runs at startup, before
any cycle, so a unit is tripped in memory only if its own `unit/<name>/sign_tripped`
key was truthy — which makes `namespaced_latched` True and short-circuits the
disjunct. I believe it is an equivalent mutant at that call site rather than a
live hole, and I am recording the argument instead of asserting the conclusion.
**Row 22 — STILL GREEN, and reported with its size.** `", ".join(sorted(u for u
in resolution.shares if not self._can_write(u)))[:1]` truncates the **names in
one event-log line**. It is +4 bytes and no check bites. The refusal itself —
`elif {u for u in resolution.shares if not self._can_write(u)}` — is a different
expression and *is* graded (test_peakguard.py part 10h-1b), so the site still
stops; what a `[:1]` costs is an operator being told one name when two units have
no writer. It is not a roster comprehension (it iterates `resolution.shares`), so
12j does not cover it and does not pretend to. Closing it needs a three-inverter
fixture with two writer-less entries, which is ALLOC-01's fixture and not this
card's. **Filed as open, with its size and its consequence, rather than closed
quietly or left unmentioned.**
### And the family closed rather than the member
`test_peakguard.py` part 12j enumerates **every** comprehension in `Controller`
that iterates the roster — 26 of them across 23 methods, computed from main.py's
AST, printed, and required to iterate the roster **whole**. A new reduction added
over `self.inverters[:1]` anywhere in the class is red **on the line it is
written**, at every roster length, with no fixture required. That check is what
would have caught rounds 2, 3 and 4's blockers on the round they were written
instead of one review round each; it is also what found rows 18-21.
## 5. ⚠️ THE RESIDUAL — a per-pack EMS floor is NOT this card
`peak_soc_floor` is still **one number for the site**, so the card's own
+32
View File
@@ -300,6 +300,38 @@ Cheap habits fall out of it, and all of them are now used in this repository:
assert the **shape** of that second report, not only its verdict, so the
check cannot silently revert to grading the first path.
10. **A fixture of N members cannot separate two reductions that agree on N
members — so grade the FAMILY, and grade it from the SOURCE.** This is the
only lesson SAFETY-32 cost four review rounds to learn, and it generalises
past packs to every roster, list and window in this repository. Two packs
cannot tell `max` from `min` from first from last. Three cannot tell `max`
from `max(x[-2:])`. **The regress does not terminate in a fixture**: `[:1]`
needs two members, `[:2]` three, `[:3]` four, and adding one more member
moves the hole rather than closing it. Three things follow, and all three
are now in `test_peakguard.py` parts 12c2, 12g, 12i and 12j:
* the fixture is a **SET** — the extreme at every position of the roster,
not one roster with the extreme somewhere;
* the family table is **COMPUTED and PRINTED**, so a member no fixture kills
shows up as a named survivor and takes the check red, instead of being
absent from a list nobody re-derived;
* where the claim is an **IDENTITY** ("this roster", "this list"), pin it
**exactly on the AST** — `ast.unparse(arg) == "self.packs"` is false of
every slice, where `"self.packs" in src` is true of all of them. Where the
claim is **SEMANTIC** ("the maximum"), a shape pin would refuse honest
refactors, so report the unreached width **with its size** instead.
11. **When a check of this shape is found, mutate its SIBLINGS before shipping
the fix.** SAFETY-32 was rejected three times for the same defect one step
over: the reduction, then the roster handed to it, then the reduction handed
to the *other argument of the same call*. Enumerating the family from the
AST and mutating each member took one afternoon and found **four more
survivors in code the card never touched** — three of SAFETY-30's
`any(i.sign_wd.tripped for i in self.inverters)` reductions, invisible
because the only fixture that reached them was a roster of ONE, where
`self.inverters[:1]` **is** `self.inverters`. Ask of every fix: *what is the
sibling of the thing I just hardened, and does any fixture separate it from
a slice of itself?*
And the mutation-table consequence: **a variant is not covered because a
near-miss of it is.** DEV-02's table listed the *actuator* variant of the
per-unit claim defect (`device`/`supervised` filed without `inv`), which the
+667 -1
View File
@@ -4159,6 +4159,590 @@ check("⚠️ AC 5. At a roster of ONE the same notification carries NO per-pack
and "peak_soc_floor bounds THE PEAK GUARD ONLY" in _body32one)
# --- 12i. THE SIBLING ARGUMENT: `pack_floor_soc`, THE OTHER HALF OF THE PAIR --
# ⚠️ THIS IS ROUND 4's BLOCKER, AND IT IS THE SAME FAMILY ONE ARGUMENT OVER.
# Everything from 12c2 to 12h grades reductions on the FLOOR axis: the max
# inside `binding_soc_floor()`, the roster handed to it, `Controller.packs`, and
# `pack_floor_pct()`'s conjunction. `Controller.pack_floor_soc` is the MINIMUM
# over the same roster, handed to the SAME `peakguard.decide()` call as `soc=`,
# and until this block nothing graded its reduction past N=2.
#
# ⚠️ THE PAIRING IS DOCUMENTED, WHICH IS WHY HARDENING ONE HALF IS NOT ENOUGH.
# main.py's call site says "MAXIMUM here pairs with the MINIMUM in
# `pack_floor_soc`: both reductions move the verdict towards refusing a shave
# and away from spending a pack". A conjunction whose two halves have different
# amounts of evidence behind them is exactly as strong as its weaker half.
#
# THE SURVIVORS THIS BLOCK EXISTS FOR, all confirmed GREEN across all 19 files
# at 52380c0 and again on the rebase onto 3934ad7:
#
# min(float(v) for v in vals) -> ... for v in vals[:2] +4 bytes
# -> ... for v in vals[-2:] +5 bytes
# -> ... for v in vals[:3] +4 bytes
#
# while `vals[:1]`, `vals[-1:]`, `vals[1:]`, `vals[:-1]`, `max(vals)` and the
# mean were all killed. The suite's separating power on the SoC axis stopped at
# exactly N=2 - which is the state the FLOOR axis was in before round 3, and
# which round 3 named as its own blocker 2. The evidence is a fixture of two
# packs, and A FIXTURE OF N PACKS CANNOT SEPARATE REDUCTIONS THAT AGREE ON N.
#
# IT CHANGES A REAL ANSWER, which is why it is a defect and not a tidiness
# point: a three-pack roster at 50 / 60 / 11 % with the emptiest pack THIRD.
# The shipped property answers 11 %; `vals[:2]` answers 50 %. The site is then
# graded for discharge PERMISSION against a pack 39 points fuller than the
# emptiest one, and spends a pack its own BMS stops - through `sim/inject.py`,
# which runs no validator rule at all.
#
# ⚠️ AND PRODUCTION IS DEGENERATE ON THE FLOOR AXIS, WHICH MAKES THIS AXIS THE
# LIVE ONE. SPIKE-04 reads pack B as 4 x Dyness DL5.0C at DoD 90 [FROM THE
# DATASHEET AND THE SERIAL - inverter B does not exist and nothing about it has
# been measured], so its cut-out is 10 %, the same as pack A's MEASURED 10 %.
# Two packs that floor at the same value make `binding_soc_floor()` answer the
# option whatever it reduces. The SoC axis has no such degeneracy: two batteries
# at the same state of charge is a coincidence, not a configuration.
#
# THE TREATMENT IS ROUND 3's, TRANSFERRED: a roster SET with the extreme at
# every position, a LENGTH SWEEP, and an EXACT STRUCTURAL PIN on the reduction's
# argument. Nothing below is a measurement of a second or third pack.
_S_EMPTY_SIM, _S_MID_SIM, _S_FULL_SIM = 11.0, 50.0, 60.0
_S_TRIO_SIM = (_S_FULL_SIM, _S_MID_SIM, _S_EMPTY_SIM)
def _soc_reaching_decide(tag, *socs):
"""Drive ONE REAL `Controller.cycle()` on an N-pack roster and report the
SoC `peakguard.decide()` was actually handed, read back off the decision
main.py itself filed (`PeakDecision.soc` is the argument, echoed).
⚠️ THE EXACT MIRROR OF `_floor_reaching_decide` ABOVE, on the other axis.
Not a spy and not a grep: the shipped `cycle()` runs, the shipped
`pack_floor_soc` 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. Every pack carries the SAME cut-out
(inverter A's measured 10 %, which is below `peak_soc_floor`, so
`binding_soc_floor()` answers the option for every roster here); the only
thing that varies between calls is the packs' states of charge. That is
habit 1: with the FLOOR axis held flat, nothing but the SoC reduction can
move these answers.
"""
def _prep(ctl):
for _i in range(len(socs) - 1):
_sfx = chr(ord("b") + _i)
second_inverter(ctl, name=f"inverter-{_sfx}",
setpoint=f"number.sp_{_sfx}")
for inv, so in zip(ctl.inverters, socs):
inv.soc, inv.batt, inv.bms_soc_floor = so, 0.0, A_PACK_FLOOR
ctl, _hs, _net, _rem = wired_over_limit(
TMP / f"s32s_{tag}.db", LIVE_MAX_W * 0.3, prepare=_prep)
return ctl, ctl.peak_guard
# BASELINE: three packs, all of them ABOVE `peak_soc_floor`, so the guard is
# permitted and sizes a real forced discharge. Every run below varies one thing
# from this baseline (habit 7) - which pack is the empty one, and nothing else.
_s_ctl_ok, _s_ok = _soc_reaching_decide("ok3", _S_FULL_SIM, _S_MID_SIM,
SOC_BETWEEN)
# THE SET: the SAME THREE readings, the emptiest at EACH position in turn. A
# reduction that reads a proper subset of the positions misses the empty pack on
# the run where it sits at the position that subset drops, and answers a fuller
# pack instead.
_s3_runs = []
for _pos in range(3):
_sc3 = [_S_FULL_SIM, _S_MID_SIM, _S_EMPTY_SIM]
_sc3.remove(_S_EMPTY_SIM)
_sc3.insert(_pos, _S_EMPTY_SIM)
_c3s, _d3s = _soc_reaching_decide(f"s3p{_pos}", *_sc3)
_s3_runs.append((f"3-pack, emptiest at index {_pos}", _sc3, _c3s, _d3s))
# ...and the two-pack mirror, which is the shape production reaches first.
_s2_runs = []
for _pos in range(2):
_sc2 = [_S_FULL_SIM, _S_EMPTY_SIM] if _pos else [_S_EMPTY_SIM, _S_FULL_SIM]
_c2s, _d2s = _soc_reaching_decide(f"s2p{_pos}", *_sc2)
_s2_runs.append((f"2-pack, emptiest at index {_pos}", _sc2, _c2s, _d2s))
print(f" REAL cycles, every cut-out held at inverter-a's measured "
f"{A_PACK_FLOOR:.0f} %, peak_soc_floor {SOC_FLOOR:.0f} % (every pack past "
f"the first is SIMULATED):")
print(f" 3-pack baseline, none empty: SoCs "
f"{[f'{s:g}' for s in (_S_FULL_SIM, _S_MID_SIM, SOC_BETWEEN)]} % -> "
f"decide() got soc={_s_ok.soc:g} %, floor_limited={_s_ok.floor_limited}")
for _rn, _sc, _ctl_s, _dec_s in _s3_runs + _s2_runs:
print(f" {_rn}: SoCs {[f'{s:g}' for s in _sc]} % -> decide() got "
f"soc={_dec_s.soc:g} %, floor_limited={_dec_s.floor_limited}")
check("⚠️ THE POSITIONAL PIN ON THE SoC AXIS, AND IT NEEDS THREE PACKS TO "
"EXIST. On a roster of THREE the SoC that reaches `decide()` is the "
"EMPTIEST pack wherever on the roster that pack sits - index 0, index 1 "
"and index 2 all answer 11 %, and all three rosters carry the SAME "
"multiset of readings. A property that reduced any PROPER SUBSET of the "
"positions would answer a fuller pack on the run whose empty one sits at "
"the position it dropped. `vals[:2]` and `vals[-2:]` - the +4- and "
"+5-byte mutations that walked through every fixture in this file up to "
"round 3, because at N=2 they ARE the roster - go red here",
[r[3].soc for r in _s3_runs] == [_S_EMPTY_SIM] * 3
and all(len(r[2].inverters) == 3 for r in _s3_runs)
and all(sorted(inv.soc for inv in r[2].inverters)
== sorted(_S_TRIO_SIM) for r in _s3_runs)
and [[inv.soc for inv in r[2].inverters] for r in _s3_runs]
== [r[1] for r in _s3_runs])
check("...and the TWO-pack mirror, which is what production reaches the moment "
"inverter B is installed: swap the same two readings between the packs "
"and the answer is the emptier one both times. `vals[:1]` and `vals[-1:]` "
"- grade the site against pack A alone, or against the last pack alone - "
"each agree with the roster on one of these two runs and disagree on the "
"other, so neither survives the pair",
[r[3].soc for r in _s2_runs] == [_S_EMPTY_SIM] * 2
and [[inv.soc for inv in r[2].inverters] for r in _s2_runs]
== [[_S_EMPTY_SIM, _S_FULL_SIM], [_S_FULL_SIM, _S_EMPTY_SIM]])
check("⚠️ ...AND THE SITE'S VERDICT FLIPS WITH IT, which is what makes this a "
"defect rather than a reporting difference. With the emptiest pack at "
"11 % - below the 20 % EMS floor - every one of those five sites is "
"FLOOR-LIMITED and sizes NO forced discharge at all, where the baseline "
"with its emptiest pack at 25 % is permitted and sizes a positive one. A "
"reduction that dropped the empty pack's position would grade this site "
"for PERMISSION against a pack 39 points fuller and spend, through "
"`sim/inject.py`, a pack its own BMS stops",
all(r[3].floor_limited is True and r[3].floor_w == 0.0
for r in _s3_runs + _s2_runs)
and _s_ok.floor_limited is False and _s_ok.floor_w > 0.0
and _s_ok.soc == SOC_BETWEEN)
check("...and the precondition that makes the six runs comparable (habit 1): "
"every pack in every roster carries the SAME cut-out, so "
"`binding_soc_floor()` answers the SAME site floor on all of them and the "
"FLOOR axis cannot be what separated the answers; the three readings "
"really are three different numbers; and the empty one is really below "
"the EMS floor while the other two are really above it - two readings on "
"the same side of it would make every line here vacuous",
len({r[3].soc_floor for r in _s3_runs + _s2_runs}) == 1
and _s_ok.soc_floor == _s3_runs[0][3].soc_floor == float(SOC_FLOOR)
and all(inv.bms_soc_floor == A_PACK_FLOOR
for r in _s3_runs + _s2_runs for inv in r[2].inverters)
and len({_S_EMPTY_SIM, _S_MID_SIM, _S_FULL_SIM}) == 3
and _S_EMPTY_SIM < SOC_FLOOR < SOC_BETWEEN < _S_MID_SIM < _S_FULL_SIM)
# ⚠️ AND THE ENUMERATION ITSELF, COMPUTED RATHER THAN CLAIMED - 12g's table on
# the other axis. Every positional slice of `vals`, applied to the REAL
# `Controller.inverters` each cycle above actually carried, compared against the
# SoC that REALLY reached `decide()` on that run. A slice with an empty kill
# list is a live 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. `max` and the mean
# are graded on the same runs immediately below. The table is PRINTED so a
# reader can see exactly how far the claim reaches.
_S_RUNS = ([("3-pack baseline, none empty", _s_ctl_ok, _s_ok)]
+ [(rn, ctl, dec) for rn, _sc, ctl, dec in _s3_runs + _s2_runs])
def _soc_reduced(vals, fn):
"""`pack_floor_soc`'s body with ONE thing changed: what `min()` iterates.
The None guard still runs over the WHOLE list, because these mutations are
inside the `min()` generator and not in the guard - the guard is graded
separately below. An empty slice makes the real `min()` raise, which is a
crashing cycle and therefore a kill; it is reported as a distinct answer
rather than swallowed.
"""
if not vals or any(v is None for v in vals):
return None
sl = fn(vals)
return float(min(float(v) for v in sl)) if sl else "min() of an empty slice"
_SOC_SLICE_FAMILY = {
"vals[:1]": lambda vs: vs[:1],
"vals[-1:]": lambda vs: vs[-1:],
"vals[:2]": lambda vs: vs[:2],
"vals[-2:]": lambda vs: vs[-2:],
"vals[1:]": lambda vs: vs[1:],
"vals[:-1]": lambda vs: vs[:-1],
"vals[1:-1]": lambda vs: vs[1:-1],
"vals[::2]": lambda vs: vs[::2],
}
_SOC_REDUCTION_FAMILY = {
"max(vals)": lambda vs: max(vs),
"mean(vals)": lambda vs: sum(vs) / len(vs),
"median(vals), upper": lambda vs: sorted(vs)[len(vs) // 2],
"sorted(vals)[1] (second emptiest)": lambda vs: sorted(vs)[min(1, len(vs) - 1)],
}
_soc_slice_kills = {
_nm: [rn for rn, ctl, dec in _S_RUNS
if _soc_reduced([inv.soc for inv in ctl.inverters], _fn) != dec.soc]
for _nm, _fn in _SOC_SLICE_FAMILY.items()}
_soc_red_kills = {
_nm: [rn for rn, ctl, dec in _S_RUNS
if _fn([inv.soc for inv in ctl.inverters]) != dec.soc]
for _nm, _fn in _SOC_REDUCTION_FAMILY.items()}
print(" THE POSITIONAL-SLICE FAMILY inside `pack_floor_soc`, and which run "
"separates each from the whole roster:")
for _nm, _k in _soc_slice_kills.items():
print(f" {_nm:<12} killed by: "
+ ("; ".join(_k) if _k else "*** NOTHING HERE - SURVIVOR ***"))
print(" ...and the NON-slice rewrites of the reduction itself:")
for _nm, _k in _soc_red_kills.items():
print(f" {_nm:<34} killed by: "
+ ("; ".join(_k) if _k else "*** NOTHING HERE - SURVIVOR ***"))
check("⚠️ EVERY positional slice in the enumerated family answers something "
"OTHER than the SoC that really reached `decide()` on at least one of "
"the six runs above - and it is the THREE-pack runs that kill `[:2]` and "
"`[-2:]`, which the two-pack runs structurally could not, by exactly the "
"argument 12c2 makes about N packs and reductions that agree on N. The "
"kill list is computed against the REAL `Controller.inverters` each cycle "
"carried and the REAL `PeakDecision.soc` 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(_soc_slice_kills.values()))
check("...and the same for the rewrites that are not slices at all: `max` - "
"the FULLEST pack, which is `binding_soc_floor()`'s reduction pasted onto "
"the wrong axis and the single most likely wrong edit here - the mean, "
"the median and the second-emptiest each disagree with the shipped answer "
"on at least one run. `max(vals)` on the index-2 run answers 60 % where "
"the site is graded at 11 %",
all(_soc_red_kills.values()))
check("...and the baseline the tables are measured against is the shipped "
"property's OWN answer, not a re-derivation: on every run, the SoC that "
"reached `decide()` equals `Controller.pack_floor_soc` on the roster that "
"cycle carried. If it did not, every kill list above would be measuring "
"the wrong thing",
all(dec.soc == ctl.pack_floor_soc for _rn, ctl, dec in _S_RUNS)
and len(_S_RUNS) == 6
and sorted(len(ctl.inverters) for _rn, ctl, dec in _S_RUNS)
== [2, 2, 3, 3, 3, 3])
# ⚠️ AND THE HONEST LIMIT OF EVERY RUN ABOVE, FOUND BY THIS ROUND'S OWN BATTERY
# AND NOT ARGUED FROM: `vals[:3]` and `vals[-3:]` SURVIVE all six behavioural
# runs, for the same reason `[:2]` survived the two-pack ones - THE LONGEST
# ROSTER HERE IS THREE, and a slice that keeps three consecutive positions IS
# the roster at N=3. Adding a four-pack cycle would close those two and hand
# `[:4]` and `[-4:]` the same free pass. THE REGRESS DOES NOT TERMINATE IN A
# FIXTURE - round 3's lesson, arriving unchanged on this axis.
#
# So the same two halves, each saying what it reaches. First the SWEEP, which is
# cheap here because `pack_floor_soc` is a PROPERTY and needs no cycle to
# evaluate: rosters of 1 to 12 real `Inverter`s, the empty pack at EVERY
# position of each, and the property must answer the emptiest 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.
_S_SWEEP_N = 12
def _roster_of(socs):
"""A real Controller carrying one real `Inverter` per reading given."""
ctl, _hs = built(TMP / f"s32sw{len(socs)}.db")
for _i in range(len(socs) - 1):
second_inverter(ctl, name=f"sweep-{_i}", setpoint=f"number.sw_{_i}")
for inv, so in zip(ctl.inverters, socs):
inv.soc, inv.batt, inv.bms_soc_floor = so, 0.0, A_PACK_FLOOR
return ctl
_s_sweep_rows = []
for _n in range(1, _S_SWEEP_N + 1):
for _pos in range(_n):
_sc = [_S_FULL_SIM] * _n
_sc[_pos] = _S_EMPTY_SIM
_s_sweep_rows.append((_n, _pos, tuple(_sc),
_roster_of(_sc).pack_floor_soc))
_s_sweep_bad = [(n, p, sc, got) for n, p, sc, got in _s_sweep_rows
if got != min(sc)]
_s_head_kill = {w: any(min(sc[:w]) != min(sc) for _n, _p, sc, _g in _s_sweep_rows)
for w in range(1, _S_SWEEP_N + 1)}
_s_tail_kill = {w: any(min(sc[-w:]) != min(sc) for _n, _p, sc, _g in _s_sweep_rows)
for w in range(1, _S_SWEEP_N + 1)}
print(f" LENGTH SWEEP on the real property (all SIMULATED past pack A): "
f"{len(_s_sweep_rows)} rosters, lengths 1..{_S_SWEEP_N}, the "
f"{_S_EMPTY_SIM:g} % pack at EVERY position of each among "
f"{_S_FULL_SIM:g} % siblings -> "
f"{len(_s_sweep_rows) - len(_s_sweep_bad)} answer the emptiest, "
f"{len(_s_sweep_bad)} do not")
print(" fixed-width windows killed by the sweep: head widths "
+ ",".join(str(w) for w in sorted(_s_head_kill) if _s_head_kill[w])
+ "; tail widths "
+ ",".join(str(w) for w in sorted(_s_tail_kill) if _s_tail_kill[w])
+ f"; NOT reached: head/tail width {_S_SWEEP_N} and wider")
check("⚠️ THE LENGTH SWEEP, on real `Controller.pack_floor_soc`. Over rosters "
"of 1 to 12 real inverters with the empty pack at every position of each, "
"the property answers the EMPTIEST every time - so every head window "
"`min(vals[:w])` and every tail window `min(vals[-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. ⚠️ THIS IS THE REAL PROPERTY ON A REAL ROSTER, not a "
"re-implementation: `_roster_of()` appends real `Inverter` objects and "
"reads `ctl.pack_floor_soc`, so it also sees a rewrite of the "
"comprehension that builds `vals`",
not _s_sweep_bad
and len(_s_sweep_rows) == _S_SWEEP_N * (_S_SWEEP_N + 1) // 2
and all(_s_head_kill[w] and _s_tail_kill[w]
for w in range(1, _S_SWEEP_N)))
check("⚠️ ...AND WIDTH 12 AND WIDER IS HONESTLY NOT REACHED, recorded rather "
"than papered over - the same ceiling 12c2's sweep records on the floor "
"axis. No roster in this file is longer than 12, so `min(vals[:12])` IS "
"`min(vals)` 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. That is why the STRUCTURAL PIN below exists alongside these runs, "
"and this line asserts the unreachedness itself so a later sweep that "
"lengthens the rosters takes it red and forces the sentence rewritten",
not _s_head_kill[_S_SWEEP_N] and not _s_tail_kill[_S_SWEEP_N]
and max(len(sc) for _n, _p, sc, _g in _s_sweep_rows) == _S_SWEEP_N)
# ...and the NONE GUARD is a reduction over roster length TOO, and it had
# exactly the same fixture problem: 12d sets the SECOND of two packs to None, so
# `any(v is None for v in vals[:1])` - grade only pack A for silence - answers
# "all present" there and hands a list containing None to `min()`. The sweep
# below moves the silent pack along the roster at every length, which is the
# data that reaches it. THE DIRECTION MATTERS: None must WIN, because a silent
# pack is a pack nothing can grade and `decide()` treats None as floor-limited.
def _pfs_answer(ctl):
"""`pack_floor_soc`, with a raise reported as an ANSWER rather than
ending the file. A guard narrowed to a slice does not return a wrong
number - it lets a None reach `min(float(v) ...)` and raises TypeError -
and a check that dies is a check that names nothing."""
try:
return ctl.pack_floor_soc
except Exception as exc: # noqa: BLE001 - reported
return f"raised {type(exc).__name__}"
_s_none_rows = []
for _n in range(1, _S_SWEEP_N + 1):
for _pos in range(_n):
_ctl_n = _roster_of([_S_FULL_SIM] * _n)
_ctl_n.inverters[_pos].soc = None
_s_none_rows.append((_n, _pos, _pfs_answer(_ctl_n)))
print(f" NONE-GUARD SWEEP: {len(_s_none_rows)} rosters, ONE silent pack at "
f"every position of every length 1..{_S_SWEEP_N} -> "
f"{sum(1 for _n, _p, g in _s_none_rows if g is None)} answer None")
check("⚠️ THE NONE GUARD IS THE SAME FAMILY. One silent pack at ANY position of "
"ANY roster length makes `pack_floor_soc` None - never a number, and "
"never the minimum of the packs that did answer. A guard narrowed to a "
"positional slice would let the site spend the packs that answered while "
"one sat unmeasured; 12d's two-pack fixture, with the SECOND pack silent, "
"cannot see a guard narrowed to the first",
all(g is None for _n, _p, g in _s_none_rows)
and len(_s_none_rows) == _S_SWEEP_N * (_S_SWEEP_N + 1) // 2)
# ⚠️ THE STRUCTURAL HALF: the reduction's ARGUMENT, pinned EXACTLY, at any N.
# This is 12g's treatment applied inside a property rather than at a call site,
# and it is NOT a substring test - `"vals" in src` is true of every slice of
# `vals`, whereas `ast.unparse(iter) == "vals"` is false of all of them.
# `vals[:3]` unparses to `vals[:3]`.
#
# THREE expressions are pinned, because there are three reductions over roster
# length in this one property and the runs above reach them unevenly:
# the LIST `[inv.soc for inv in self.inverters]` - the roster itself
# the GUARD `any(v is None for v in vals)`
# the REDUCTION `min(float(v) for v in vals)`
#
# ⚠️ AND THE PIN IS BLIND TO WHAT THE RUNS SEE, which is why both halves are
# here. It cannot see `min` become `max` (identical shape, different name -
# killed by the roster set), it cannot see `inv.soc` become `inv.bms_soc_floor`
# (killed by the runs' held-flat cut-outs), and it cannot see a change inside
# `Inverter.soc` at all.
_pfs_fn = next(n for n in ast.walk(ast.parse(_mainsrc))
if isinstance(n, (ast.FunctionDef, ast.AsyncFunctionDef))
and n.name == "pack_floor_soc")
_pfs_vals = next(n.value for n in _pfs_fn.body
if isinstance(n, ast.Assign)
and [ast.unparse(t) for t in n.targets] == ["vals"])
def _gen_iter_of(fn_node, name):
"""The iterable of the comprehension inside the single `name(...)` call."""
call = next(n for n in ast.walk(fn_node)
if isinstance(n, ast.Call) and isinstance(n.func, ast.Name)
and n.func.id == name)
comp = call.args[0]
return comp.generators[0].iter if len(comp.generators) == 1 else None
_pfs_min_iter = _gen_iter_of(_pfs_fn, "min")
_pfs_any_iter = _gen_iter_of(_pfs_fn, "any")
print(f" pack_floor_soc reduces: list over `{ast.unparse(_pfs_vals.generators[0].iter)}`"
f", any() over `{ast.unparse(_pfs_any_iter)}`, min() over "
f"`{ast.unparse(_pfs_min_iter)}`")
check("⚠️ THE STRUCTURAL HALF, EXACT RATHER THAN A SUBSTRING. `min()` reduces "
"the WHOLE list `vals` - a bare Name, not a Subscript, not a call, not a "
"second comprehension - and `vals` is built by ONE comprehension over the "
"WHOLE property `self.inverters`, an attribute of self and not a slice of "
"one. So EVERY slice of either is red here at EVERY roster length, "
"including `vals[:3]` and `vals[-3:]`, which survive all six runs above "
"because the longest roster they drive is three packs long, and including "
"`self.inverters[:2]` in the comprehension, which the sweep sees only up "
"to length 12. This grades the code's SHAPE and nothing about the values; "
"what the expression MEANS is graded by the runs",
isinstance(_pfs_min_iter, ast.Name) and _pfs_min_iter.id == "vals"
and ast.unparse(_pfs_min_iter) == "vals"
and isinstance(_pfs_vals, ast.ListComp)
and len(_pfs_vals.generators) == 1
and not _pfs_vals.generators[0].ifs
and isinstance(_pfs_vals.generators[0].iter, ast.Attribute)
and isinstance(_pfs_vals.generators[0].iter.value, ast.Name)
and _pfs_vals.generators[0].iter.value.id == "self"
and _pfs_vals.generators[0].iter.attr == "inverters"
and ast.unparse(_pfs_vals.generators[0].iter) == "self.inverters")
check("...and the NONE GUARD reduces that same whole list, pinned the same way. "
"`any(v is None for v in vals[:1])` is +4 bytes and leaves every other "
"line in this file identical; the sweep above reaches it up to length 12 "
"and this reaches it at every length",
isinstance(_pfs_any_iter, ast.Name) and _pfs_any_iter.id == "vals"
and ast.unparse(_pfs_any_iter) == "vals")
check("...and the counterfactual that shows these pins are not vacuous (habit "
"7): the very slices they exist for really do unparse to something else, "
"so the equalities above are doing work rather than being trivially true "
"of anything shaped like an argument",
all(ast.unparse(ast.parse(f"vals{sl}", mode="eval").body) != "vals"
and ast.unparse(ast.parse(f"self.inverters{sl}",
mode="eval").body) != "self.inverters"
for sl in ("[:1]", "[-1:]", "[:2]", "[-2:]", "[:3]", "[-3:]",
"[:12]", "[-12:]", "[1:]", "[:-1]", "[1:-1]", "[::2]"))
and ast.unparse(ast.parse("list(reversed(vals))",
mode="eval").body) != "vals")
# ...and BOTH consumers of this property are pinned to it by name, so a reduction
# hardened here cannot be bypassed by a call site that stops using it. The peak
# guard's `soc=` is already pinned in part 4; the OTHER one is arbitrage's, and
# it is a safety consumer too - `soc_floor_pct` is what stops a sell.
_arb_calls = [n for n in ast.walk(ast.parse(_mainsrc))
if isinstance(n, ast.Call) and isinstance(n.func, ast.Attribute)
and n.func.attr == "decide"
and isinstance(n.func.value, ast.Name)
and n.func.value.id == "arbitrage"]
_arb_soc = ast.unparse(next(k.value for k in _arb_calls[0].keywords
if k.arg == "soc"))
print(f" main.py's arbitrage.decide(soc=...) is `{_arb_soc}` "
f"({len(_arb_calls)} call site)")
check("⚠️ AND THE SECOND CONSUMER OF THE SAME REDUCTION. `arbitrage.decide()` "
"is handed the SAME `self.pack_floor_soc` and grades it against "
"`soc_floor_pct` to decide whether to SELL - so the mutation this block "
"exists for spends a pack on the arbitrage path as well as the peak-guard "
"path, and hardening the property covers both. A call site that reverted "
"to a per-unit reading, or defaulted it, would take this line red",
len(_arb_calls) == 1 and _arb_soc == "self.pack_floor_soc")
# --- 12j. THE ENUMERATION ITSELF, AS A RUNNING CHECK -------------------------
# ⚠️ THIS CARD HAS NOW BEEN REJECTED THREE TIMES FOR THE SAME SHAPE ONE STEP
# OVER: a reduction over roster length whose fixture could not separate it from
# a slice of the roster. Round 2 hardened `binding_soc_floor()`; round 3 found
# the call site's argument; round 4's blocker was `pack_floor_soc`, the SIBLING
# ARGUMENT of the same `decide()` call. Closing them one at a time has cost four
# rounds, so this block stops enumerating them by hand.
#
# EVERY comprehension in `Controller` that iterates the roster is listed here,
# COMPUTED from main.py's AST, PRINTED, and required to iterate the roster
# WHOLE. That is the family: `min`, `max`, `sum`, `any`, `all`, `sorted` and the
# list builders all take their roster through one of these, so a `[:1]`, a
# `[-1:]` or a `[:2]` anywhere in the class takes this line red on the line it
# was written - at every roster length, in every configuration, whether or not
# any fixture in this repository reaches it.
#
# ⚠️ WHAT IT DOES NOT COVER, said plainly. It grades the ITERABLE and nothing
# else: not which attribute is read off each unit, not which reduction is
# applied, and not the direct index sites (`self.inverters[0]` in `_only()`,
# `actuator_of()` and the store migration, `self.inverters[self.maint_index]` in
# `maint_unit`), which are not comprehensions and are graded where they live.
# The behavioural halves above are what say what these reductions MEAN.
_ctrl_cls = next(n for n in ast.walk(ast.parse(_mainsrc))
if isinstance(n, ast.ClassDef) and n.name == "Controller")
_ROSTER_ATTRS = ("inverters", "packs")
def _is_roster(node):
return (isinstance(node, ast.Attribute) and node.attr in _ROSTER_ATTRS
and isinstance(node.value, ast.Name) and node.value.id == "self")
def _mentions_roster(node):
return any(_is_roster(n) for n in ast.walk(node))
_roster_comps = []
for _fn in ast.walk(_ctrl_cls):
if not isinstance(_fn, (ast.FunctionDef, ast.AsyncFunctionDef)):
continue
for _n in ast.walk(_fn):
if isinstance(_n, (ast.ListComp, ast.SetComp, ast.DictComp,
ast.GeneratorExp)):
for _g in _n.generators:
if _mentions_roster(_g.iter):
_roster_comps.append((_fn.name, _g.iter.lineno,
ast.unparse(_g.iter)))
_roster_comps.sort(key=lambda r: (r[1], r[2]))
def _slices_roster(node):
"""Is the roster SUBSCRIPTED anywhere inside this expression?
⚠️ THE TEST IS ON THE SUBSCRIPT, NOT ON THE SPELLING. `enumerate(...)`,
`zip(...)` and `pack_permissions(roster, floor)` all hand the WHOLE roster
on and are legitimate; `self.inverters[:1]` is the family this card has been
rejected over three times. Requiring the iterable to unparse to exactly
`self.inverters` would refuse the first three and grade the spelling instead
of the thing.
"""
return any(isinstance(n, ast.Subscript) and _is_roster(n.value)
for n in ast.walk(node))
_sliced = [r for r in _roster_comps
if _slices_roster(ast.parse(r[2], mode="eval").body)]
print(f" EVERY comprehension in Controller that iterates the roster "
f"({len(_roster_comps)} of them, in "
f"{len({m for m, _l, _s in _roster_comps})} methods), and what each "
f"iterates:")
for _mname, _ln, _src in _roster_comps:
print(f" main.py:{_ln:<5} {_mname:<26} for ... in {_src}"
+ ("" if _src in ("self.inverters", "self.packs")
else " [whole roster, wrapped]"))
check("⚠️ THE FAMILY, ENUMERATED FROM THE SOURCE RATHER THAN FROM MEMORY. Every "
"comprehension in `Controller` that iterates the roster iterates it "
"WHOLE - `self.inverters` or `self.packs`, bare. This is the check that "
"would have caught rounds 2, 3 and 4's blockers on the round they were "
"written instead of one review each: `min(... for v in vals[:2])` is not "
"here (it reduces a derived list, which 12i pins directly), but every "
"`for inv in self.inverters[:1]` in the class is. A new reduction added "
"over a slice of the roster is red on the line it is written, at every "
"roster length and with no fixture required. ⚠️ THE ITERABLE ONLY - what "
"is read off each unit and what reduction is applied are graded by the "
"runs, and the direct index sites are not comprehensions and not here",
len(_roster_comps) > 0 and not _sliced)
check("...and the enumeration is not vacuously empty and its predicate is not "
"trivially true (habit 7): it found more than twenty roster "
"comprehensions across more than fifteen methods, it REJECTS the same "
"expressions with a slice on them - bare and wrapped in `enumerate()` "
"alike - and it ACCEPTS the three legitimate wrapped forms this class "
"actually uses. A predicate that answered the same thing for both would "
"make the line above a description rather than a check",
len(_roster_comps) >= 20
and len({m for m, _l, _s in _roster_comps}) >= 15
and all(_slices_roster(ast.parse(f"self.{a}{sl}", mode="eval").body)
and _slices_roster(ast.parse(f"enumerate(self.{a}{sl})",
mode="eval").body)
for a in _ROSTER_ATTRS
for sl in ("[:1]", "[-1:]", "[:2]", "[1:]", "[:-1]", "[::2]"))
and not any(_slices_roster(ast.parse(e, mode="eval").body)
for e in ("self.inverters", "self.packs",
"enumerate(self.inverters)",
"peakguard.pack_permissions(self.packs, f)")))
# ⚠️ AND THE TWO THIS ENUMERATION ACTUALLY FOUND, recorded here because the
# lesson is the finding and not the fix. Mutating every roster reduction in
# `Controller` to `[:1]` one at a time turned up TWO that survived a green
# 19-file suite, both `any(i.sign_wd.tripped for i in self.inverters)` and both
# SAFETY-30's rather than this card's:
#
# `cycle()`'s stale-input hold +4 bytes, 19/19 green - a LATCHED unit must
# take the roster past the hold, or its failsafe SET stops being re-filed
# the moment a poll is missed. Graded now in test_watchdog.py part 8, on
# a two-inverter roster with the latch at EACH position in turn.
# `publish()`'s status vocabulary +4 bytes, 19/19 green - a site with one
# inverter parked by its own failsafe claim published `running`. Same
# part, same two positions.
#
# Both were invisible for the same reason every blocker on this card was
# invisible: the only fixture that reached them was a roster of ONE, where
# `self.inverters[:1]` IS `self.inverters`.
# ==============================================================================
print()
print("11. mutation: what defeats these guards, and which check bites")
@@ -4512,6 +5096,74 @@ MUT.append(("`binding_soc_floor()` reduced over a window 12 packs wide or "
"max is order- and duplicate-invariant; the second is nonetheless "
"red on 12g's structural pin"))
# --- ROUND 4: THE SIBLING ARGUMENT, AND THE ENUMERATION THAT FOUND THE REST --
# 28. `pack_floor_soc` reduced over a WINDOW of roster positions. THIS ROUND'S
# BLOCKER, and the same family as rows 25-26 one ARGUMENT over: the MINIMUM
# handed to the same `decide()` call as `soc=`. Green across all 19 files at
# 52380c0 and again on the rebase onto 3934ad7.
MUT.append(("`pack_floor_soc` reduced over a WINDOW - `vals[:2]` (+4 bytes) or "
"`vals[-2:]` (+5) - ROUND 4's BLOCKER, the SoC axis of the pair",
all(_soc_slice_kills[k] for k in ("vals[:2]", "vals[-2:]",
"vals[:1]", "vals[-1:]")),
"part 12i's THREE-pack runs and their POSITIONAL-SLICE TABLE: the "
"same three readings with the emptiest at index 0, 1 and 2, so "
"every proper subset of the positions drops the empty pack on some "
"run. ⚠️ At N=2 `[:2]` IS the roster - the two-pack mirror cannot "
"see it, which is why the suite's separating power on this axis "
"stopped at exactly N=2 for four rounds"))
# 29. ...and the three-wide window, invisible to every behavioural run here.
MUT.append(("`pack_floor_soc` reduced over a THREE-wide window - `vals[:3]` / "
"`vals[-3:]` - invisible to every cycle in this file",
_s_head_kill[3] and _s_tail_kill[3]
and ast.unparse(_pfs_min_iter) == "vals",
"part 12i's LENGTH SWEEP (widths 1-11, on the REAL property over "
"rosters of 1 to 12 real inverters) and its STRUCTURAL PIN. The "
"six real cycles cannot see it - three packs is the longest roster "
"they drive - and the sweep and the pin are what do"))
# 30. the reduction itself, on the wrong axis. Zero byte delta.
MUT.append(("`pack_floor_soc` reduced with `max()` - the FULLEST pack, which is "
"`binding_soc_floor()`'s own reduction pasted onto the SoC axis - "
"or with the mean, the median or the second-emptiest",
all(_soc_red_kills.values()),
"part 12i's NON-SLICE table, on the same six real cycles: the "
"emptiest pack is 11 % where the fullest is 60 %, so every one of "
"the four disagrees on every run. ⚠️ Zero byte delta, and the most "
"likely wrong edit here precisely because the sibling reduction one "
"argument over IS a max"))
# 31. the None guard, which is a reduction over roster length too.
MUT.append(("`pack_floor_soc`'s NONE GUARD narrowed to a slice - "
"`any(v is None for v in vals[:1])`, +4 bytes",
all(g is None for _n, _p, g in _s_none_rows)
and ast.unparse(_pfs_any_iter) == "vals",
"part 12i's NONE-GUARD SWEEP - one silent pack at every position of "
"every length 1..12 - and the same structural pin. ⚠️ 12d's "
"two-pack fixture silences the SECOND pack only, so a guard "
"narrowed to the FIRST answers 'all present' there and hands a None "
"to `min()`"))
# 32. and the roster the list itself is built from.
MUT.append(("`pack_floor_soc` building `vals` from a SLICE of the roster - "
"`[inv.soc for inv in self.inverters[:2]]`, +4 bytes",
ast.unparse(_pfs_vals.generators[0].iter) == "self.inverters"
and _s_head_kill[2] and not _sliced,
"part 12i's sweep reads the REAL property on real rosters so it "
"sees this too, its pin is on the comprehension's own iterable, "
"and 12j's ENUMERATION covers every other comprehension in the "
"class at once"))
# 33. THE ENUMERATION'S OWN FINDING, and the reason this row is worth more than
# the four above: it is not this card's code.
MUT.append(("a reduction over the roster added ANYWHERE ELSE in `Controller` "
"over a slice - which is how rounds 2, 3 and 4 each began",
bool(_roster_comps) and not _sliced,
"part 12j: every roster comprehension in the class, enumerated "
"from main.py's AST and required to iterate the roster whole. ⚠️ "
"Mutating each of them to `[:1]` found FOUR that survived a green "
"19-file suite, none of them this card's: three `sign_wd.tripped` "
"reductions (SAFETY-30's stale-input hold, `publish()`'s status "
"vocabulary and `status_payload()`'s banner - now graded in "
"test_watchdog.py part 8) and the store-migration guard's redundant "
"second disjunct. THIS row is the one that closes the family "
"rather than the member"))
for label, caught, where in MUT:
print(f" {'caught' if caught else 'NOT CAUGHT':>10} {label}")
print(f" {where}")
@@ -4546,7 +5198,7 @@ check("...⚠️ AND SO ARE THE SEVEN DEFEATS THAT SURVIVED A GREEN 19-FILE SUIT
"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)
all(m[1] for m in MUT[21:27]) and len(MUT) == 34)
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 "
@@ -4559,6 +5211,20 @@ check("...⚠️ AND ONE IS RECORDED AS NOT CAUGHT, which is the only honest row
"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 ROUND 4's SIX, WHICH ARE THE SAME FAMILY AT THE SIBLING "
"ARGUMENT OF THE SAME CALL. `pack_floor_soc` is the MINIMUM over the "
"roster handed to `decide(soc=...)`; `binding_soc_floor()` is the MAXIMUM "
"handed to `decide(soc_floor=...)` beside it, and peakguard.py's own "
"docstring names them as a pair. Rounds 2 and 3 hardened one half; "
"`vals[:2]`, `vals[-2:]` and `vals[:3]` were still green on 52380c0 with "
"the other, and a three-pack roster at 50 / 60 / 11 % answers 11 % clean "
"and 50 % mutated - a discharge PERMISSION graded against a pack 39 "
"points fuller than the emptiest. The last row is the one that matters "
"most: closing the MEMBER four times has cost four review rounds, so the "
"FAMILY is now enumerated from the source, and that enumeration found "
"four more survivors in code this card never touched",
all(m[1] for m in MUT[28:34]) and len(MUT) == 34
and _S_EMPTY_SIM < SOC_FLOOR)
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 "
+175
View File
@@ -1818,6 +1818,181 @@ check("...and no `sign_site` claim can be filed at a roster of one, so the "
"arbitration is byte-identical to what shipped",
"sign_site" not in _c1s.reason)
print()
print("8. SAFETY-32 ROUND 4's ENUMERATION: the two `any(...)` reductions over")
print(" the roster whose only evidence is a latched NON-FIRST unit")
# ⚠️ THIS SECTION IS NOT SAFETY-32's SUBJECT, AND IT IS HERE BECAUSE OF IT.
# SAFETY-32 was rejected three times for the same shape one step over: a
# reduction over roster length whose fixture could not separate it from a slice
# of the roster. Round 4 therefore ENUMERATED every such reduction in
# `Controller` - min, max, sum, any, all, sorted, [0], [-1] over
# `self.inverters` / `self.packs` - and mutated each to `[:1]` to find out which
# were GRADED. Two survived a green 19-file suite, both `any(i.sign_wd.tripped
# for i in self.inverters)`, both SAFETY-30's, and this block is what closes
# them. No shipped behaviour changes; the reductions were already right.
#
# main.py `cycle()`, the stale-input hold - +4 bytes, 19/19 GREEN
# main.py `publish()`, the status vocabulary - +4 bytes, 19/19 GREEN
#
# ⚠️ WHY THE SUITE COULD NOT SEE THEM, and it is the same sentence every time:
# the only fixture that reached either was a roster of ONE, where
# `self.inverters[:1]` IS `self.inverters`. Part 3 above builds a two-inverter
# roster in which ONLY inverter B is latched - the exact data both reductions
# needed - and neither of them was read on it. A fixture of N units cannot
# separate reductions that agree on N units, one card over.
#
# ⚠️ AND BOTH ORDERS ARE RUN, for 12g's reason: a single "only B is latched"
# fixture kills `[:1]` and leaves `[-1:]` - grade the roster by its LAST unit -
# answering identically. The pair is what leaves no single-position slice.
async def _latched_then_input_gap(reversed_idx):
"""Latch ONE unit's sign watchdog, then take a SIBLING's reading away.
⚠️ A REAL LATCH FROM A REAL EPISODE, not `sign_wd.tripped = True`: the same
`_SignHass` plant and the same `_drive()` part 3 uses, so the detector
reaches its verdict through the shipped path. Then one pack's SoC goes
missing for LESS than `stale_input_s`, which is the state the hold exists
for - a single missed poll must not become a fault.
THE FAULT THIS GRADES: a LATCHED unit must take the whole roster past that
hold, because the unit's `failsafe` SET is the thing parking it. Return
early and the unit's last share stays standing for the heartbeat to
re-emit - main.py's own comment: "the trip would stop acting the moment a
poll was missed". A reduction that looked at one roster POSITION would do
exactly that whenever the latched unit was not the position it looked at.
"""
hass = _SignHass(load_w=2000.0, reversed_units={reversed_idx})
c = _sign_site(hass)
await _drive(c)
sibling = c.inverters[1 - reversed_idx]
sibling.soc = None
c.inputs_bad_since = datetime.now(timezone.utc)
await c.cycle()
return c
_gap_b = asyncio.run(_latched_then_input_gap(1))
_gap_a = asyncio.run(_latched_then_input_gap(0))
for _tag, _c, _i in (("B latched", _gap_b, 1), ("A latched", _gap_a, 0)):
_pl = [p for p in (_c.allocation.plans if _c.allocation else ())
if p.unit == _c.inverters[_i].name]
print(f" {_tag}, sibling's SoC missing 0 s: inputs_ok="
f"{_c.inputs_ok}, reason={_c.reason!r}, latched unit target="
f"{_c.inverters[_i].target}, why={_pl[0].why if _pl else '(no plan)'}")
check("PRECONDITION (habit 1): on BOTH runs the site really is in the state "
"the hold is for - one pack's reading is missing, `inputs_ok` is False, "
"the gap is younger than `stale_input_s`, and the SITE latch is NOT "
"tripped, so the only thing that can carry the roster past the hold is "
"the per-unit `any()`. And exactly ONE unit is latched on each run, at "
"the OTHER position",
_gap_b.inputs_ok is False and _gap_a.inputs_ok is False
and _gap_b.site_sign_wd.tripped is False
and _gap_a.site_sign_wd.tripped is False
and [i.sign_wd.tripped for i in _gap_b.inverters] == [False, True]
and [i.sign_wd.tripped for i in _gap_a.inverters] == [True, False])
check("⚠️ A LATCHED UNIT TAKES THE ROSTER PAST THE STALE-INPUT HOLD FROM EITHER "
"POSITION. Neither cycle parks on `inputs missing`; both go on to file "
"claims, and the latched unit is commanded 0 W by its OWN `failsafe` "
"claim, named in the allocation record. Grade this with "
"`self.inverters[:1]` and the B-latched run returns early - the +4-byte "
"mutation that was GREEN across all 19 files - and with "
"`self.inverters[-1:]` the A-latched run does. The remedy stops acting "
"the moment a poll is missed, which is main.py's own sentence for it",
not (_gap_b.reason or "").startswith("inputs missing")
and not (_gap_a.reason or "").startswith("inputs missing")
and _gap_b.inverters[1].target == 0.0
and _gap_a.inverters[0].target == 0.0
and all(any(p.unit == c.inverters[i].name and "failsafe" in p.why
for p in (c.allocation.plans if c.allocation else ()))
for c, i in ((_gap_b, 1), (_gap_a, 0))))
# ...and the counterfactual, which is what makes the two lines above a
# DIFFERENCE rather than a description: with NOTHING latched, the very same
# input gap DOES park the site on the hold. Without this the checks above would
# be satisfied by a `cycle()` that never had a hold at all.
async def _gap_no_latch():
c = _sign_site(_SignHass(load_w=2000.0))
await _drive(c, n=2)
c.inverters[0].soc = None
c.inputs_bad_since = datetime.now(timezone.utc)
await c.cycle()
return c
_gap_none = asyncio.run(_gap_no_latch())
print(f" nothing latched, same gap: reason={_gap_none.reason!r}")
check("...and the counterfactual (habit 7): with NO unit latched the SAME gap "
"DOES hold the site - `inputs missing 0s` - so the two runs above show "
"the latch carrying the roster past a hold that is really there, rather "
"than a hold that never fires",
(_gap_none.reason or "").startswith("inputs missing")
and not any(i.sign_wd.tripped for i in _gap_none.inverters))
# --- and the SECOND survivor: the status vocabulary publish() hands the broker
# ⚠️ THE EXISTING CHECK IS AT A ROSTER OF ONE, which is why this one exists.
# "MQTT's controller-status sensor reports 'failsafe'" above drives a
# single-inverter Controller, where `self.inverters[:1]` is the whole roster.
# A site at 0 W reporting `running` is the failure main.py's comment names, and
# at two inverters it is reachable whenever the latched unit is not the one a
# narrowed reduction happens to read.
_pub = {}
def _published(ctl):
_pub.clear()
ctl.mqtt = type("P", (), {"enabled": True,
"publish": lambda _s, v: _pub.update(v),
"close": lambda _s: None})()
ctl.publish()
return dict(_pub)
_pb, _pa = _published(_gap_b), _published(_gap_a)
_pn = _published(_gap_none)
print(f" published status: B latched -> {_pb.get('status')!r}, "
f"A latched -> {_pa.get('status')!r}, none latched -> "
f"{_pn.get('status')!r}")
check("⚠️ AND `publish()` SAYS `failsafe` WHICHEVER UNIT IS LATCHED. The status "
"sensor is the vocabulary every dashboard already reads, and a site with "
"one inverter parked by its own failsafe claim reporting `running` is "
"the exact failure main.py's comment names. `self.inverters[:1]` "
"publishes `running` on the B-latched site - +4 bytes, GREEN across all "
"19 files - and `self.inverters[-1:]` does it on the A-latched one",
_pb.get("status") == "failsafe" and _pa.get("status") == "failsafe")
check("...and the counterfactual: the same two-inverter site with NOTHING "
"latched publishes `running`, so the two above are a difference the "
"reduction produced and not a constant",
_pn.get("status") == "running" and _gap_none.auto is True)
# --- and the THIRD one the same enumeration found: the OPERATOR'S BANNER -----
# ⚠️ `status_payload()`'s failsafe branch is a fourth `any(... for i in
# self.inverters)`, and `self.inverters[:1]` there was +4 bytes and GREEN across
# all 19 files too - for the third time, because the only fixture that reached
# it was a roster of ONE. The banner is the ONE sentence at the top of the page;
# a site holding an inverter at 0 W under a "Stopped" or "NOT READY" headline
# sends the operator to the wrong question.
_bn_b = _gap_b.status_payload()
_bn_a = _gap_a.status_payload()
_bn_n = _gap_none.status_payload()
print(f" banner: B latched -> {_bn_b['banner']!r}")
print(f" A latched -> {_bn_a['banner']!r}")
print(f" none -> {_bn_n['banner']!r}")
check("⚠️ AND THE BANNER LEADS WITH THE FAILSAFE WHICHEVER UNIT IS LATCHED, at "
"level `bad`, with the N>=2 sentence that names the unit's OWN measured "
"power rather than the meter. `self.inverters[:1]` drops the headline on "
"the B-latched site and `self.inverters[-1:]` on the A-latched one, and "
"the page then leads with whatever the next branch says",
_bn_b["level"] == _bn_a["level"] == "bad"
and _bn_b["banner"] == _bn_a["banner"]
and _bn_b["banner"].startswith("FAILSAFE")
and "its own measured power" in _bn_b["banner"])
check("...and the counterfactual again: the same site with nothing latched "
"carries neither that level nor that sentence, so the banner really is "
"being produced by the reduction under test",
not _bn_n["banner"].startswith("FAILSAFE")
and _bn_n["banner"] != _bn_b["banner"])
print()
if fails:
print(f"{len(fails)} FAILED: {', '.join(fails)}")