SAFETY-32: bms_soc_floor per pack, rule 8 per unit #48
Merged
admin
merged 5 commits from 2026-09-05 08:10:51 +02:00
SAFETY-32 into release/1.0
5
Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
|
|
19decf433f |
SAFETY-32 round 5: stop closing sites, build an instrument that finds its own scope
checks / unit (pull_request) Successful in 4m59s
Rounds 2, 3 and 4 each closed exactly the survivor they were handed and each time
the reviewer found the same shape one step over: the reduction, the call site, the
sibling argument, and now the sibling MODULE. Round 4's enumeration stopped at the
`Controller` class boundary; round 5's four blockers were reductions in validate.py,
over a list DERIVED from the roster three calls away from it. Closing four more sites
by hand would have produced a fifth rejection, so this round widens the instrument
instead and lets it enumerate.
⚠️ THE BLOCKERS ARE NOT EQUIVALENT MUTANTS - a safety refusal disappears, verified by
calling the shipped validator both ways on the real tree:
roster max_w 5000 (inverter-a) beside 2000 (inverter-b), sign_disagree_w 3000
clean -> 1 problem, "...max_w (inverter-b) is 2000 W, so the
SAFETY-02 sign-disagreement watchdog can never fire"
min(caps[:1]) +4 B -> 0 problems. The site STARTS.
caps_ix[:1] +4 B -> 0 problems.
the SAME roster with the small cap FIRST (2000, 5000)
clean -> 1 problem, naming inverter-a
min(caps[-1:]) +5 B -> 0 problems.
⚠️ AND THE ONE-ROSTER FIXTURE COULD NOT HAVE SEEN THAT. On [5000, 2000] the `[-1:]`
mutant still refuses, because last IS min there. A fixture of N members cannot separate
two reductions that agree on N members - which is why the behavioural half below is a
SET and not a roster.
THE INSTRUMENT (test_peakguard.py part 12j, widened past `Controller`)
Every `.py` under app/ is read off disk and parsed - NO MODULE IS NAMED IN THE CHECK -
and the roster is found by transitive closure from ONE seed, the `inverters` option key:
through returns, through lists ACCUMULATED in a loop over a roster (which is exactly
what `caps`, `roster` and `problems` are, and what round 4's rule could not express),
through attributes and properties, and THROUGH CALL ARGUMENTS, which is how it walks
into peakguard, arbiter, allocator, circulation, maintenance and store without being
told they exist. A slice of a roster stays a roster so a mutation cannot cut the taint;
an index is one unit and does not.
183 roster reductions across 9 modules, out of 23 files parsed:
main 96, allocator 24, validate 19, arbiter 14, circulation 10, maintenance 10,
peakguard 4, inverter 3, store 3. 14 modules reduce over no roster at all.
⚠️ THE HAND-WRITTEN MODULE LIST WOULD HAVE BEEN WRONG IN BOTH DIRECTIONS. It named
watchdog.py, which reduces over no roster at all (SAFETY-30's sign watchdogs are
strictly per-unit), and omitted maintenance.py and store.py, which both do. A vacuous
claim about one module and no claim at all about two others - which is the argument for
computing the scope, made with data.
The pin rediscovers ALL FOUR blockers without being told where to look, and finds a
FIFTH beside them (validate.py:783, rule 5's own message) that no review round named.
Its counterfactual runs at two depths: every enumerated site's expression mutated with
each of the four cuts this card has been defeated by (183 x 4 = 732 spellings, all
reported), and `[:1]` written into app/validate.py at each blocker position with the
WHOLE analysis re-run over the mutated source.
THE SWEEP, AND THE NUMBER THAT MUST NOT BE QUOTED ALONE
All 183 sites mutated to `[:1]`, +4 B each, against the full 19-file suite in
goodwe-addon-ci (:ro, -B, fresh rsync per mutant, 0 .pyc before and after - a read-only
mount cannot write one): 183/183 RED. ⚠️ That is TAUTOLOGICAL on its own, because the
pin makes every slice red. So the 51 whose first red was test_peakguard.py were re-run
with the pin NEUTRALISED:
145 of 183 a behavioural fixture separates the site from a slice of itself
38 of 183 ONLY the structural claim. Behaviourally UNGRADED.
All 38 are listed by site with what a `[:1]` there would cost, in the DECISIONS record
and in part 12j itself: 15 are rows and counts on the operator's page, 3 are
`len(targets)` arithmetic beside a write path that IS graded, 6 are allocator internals
ALLOC-01 reaches but not with enough units to separate. NONE of the 38 is closed
behaviourally by this card and none is counted as covered.
THE BEHAVIOURAL HALF, because a shape pin grades an identity and never a meaning
test_validate.py grows a ROSTER SET for the three rules that reduce over
`unit_caps_indexed()`: widths 2, 3, 4, 5 with the one small cap at EVERY position,
14 rosters x 3 rules = 42 runs of the real validator, each asserting the refusal fires
AND names the unit the number came off. Beside it a COMPUTED family table of twelve
candidates - max, first, last, the mean, [:1], [-1:], [:2], [:3], [1:], [:-1], [::2] -
each compared against what the shipped validator actually answered on the same roster.
Only `min` agrees everywhere; a member no roster kills is printed as a NAMED SURVIVOR.
⚠️ A THIRD RULE WAS READING THE FLAT `max_w`, AND IT IS SAFETY-30's
Found by reading the three branches side by side, NOT by the pin - and said that way
because it is the shape of what the pin cannot see. `unit_sign_disagree_w` was graded
against `_number(opts, "max_w", 2000.0)`, three lines under a branch that had already
stopped doing that. Both directions were measured before the fix:
two 2000 W units + a leftover `max_w: 5000` + unit_sign_disagree_w 3000 -> 0 problems.
The site started, the status page said `armed`, and the per-inverter watchdog could
not trip on EITHER unit. Identical sentence to the blocker, one branch over.
two 5000 W units with NO flat key -> REFUSED against a 2000 W default the operator
never wrote, for a threshold both units can reach.
It takes the same `weakest` the branch above takes and names the same unit. At a roster
of one `unit_caps()` is `[max_w]`, so the shipped single-inverter refusal is the same
comparison, the same boundary and the same sentence.
MUTATION PROOF (each: bytecode purged and counted 0 before and 0 after, the edit
re-read FROM DISK with the new text present and the old absent, byte delta printed)
B1 validate min(caps) -> min(caps[:1]) +4 B RED test_validate.py
B2 validate min(caps) -> min(caps[-1:]) +5 B RED test_validate.py
B3 validate caps_ix -> caps_ix[:1] +4 B RED test_validate.py
B4 validate rule 6 min -> min(caps_ix[-1:]) +5 B RED test_validate.py
B5 validate rule 5 msg -> min(caps_ix[:1]) +4 B RED test_validate.py
B6 validate rule 5b msg -> min(caps_ix[-1:]) +5 B RED test_validate.py
B7 CONTROL: weakest -> max(0.0, weakest) +10 B GREEN, as intended
R3a peakguard max(floors) -> min(floors) 0 B RED test_peakguard.py
R3b peakguard max(floors) -> max(floors[-2:]) +5 B RED test_peakguard.py
R3c main call site packs -> self.packs[:2] +4 B RED test_peakguard.py
R4a main pack_floor_soc -> vals[:2] +4 B RED test_peakguard.py
R4b main pack_floor_soc -> vals[-2:] +5 B RED test_peakguard.py
R4c main pack_floor_soc -> vals[:3] +4 B RED test_peakguard.py
R4d main cycle() any(...) -> self.inverters[:1] +4 B RED test_watchdog.py
B1-B6 are caught by the BEHAVIOURAL set in test_validate.py, before the pin is reached.
B7 is a deliberate no-op control: `max(0.0, weakest)` is `weakest` for weakest > 0, and
it stays green, so the battery is not merely red for everything.
R3a is a ZERO-byte delta, so the shipped function was called both ways as well:
packs floors [15.0, 30.0, 20.0], peak_soc_floor 15
binding_soc_floor(...) = 30.0 the 0-byte mutant would answer 15.0 (+15.0 pp)
-> the site would discharge to 15 % while pack-b's own BMS cuts out at 30 %.
⚠️ PRODUCTION IS DEGENERATE ON THE FLOOR AXIS. SPIKE-04: pack A and pack B BOTH floor
at 10 %, so a differing floor exists ONLY in the fixtures. That is the argument for
keeping them, not for simplifying them - collapsing them deletes the only data in this
repository that can see the reduction at all. Restated in config.yaml's example, in the
probe and in the fixtures.
⚠️ INVERTER B DOES NOT PHYSICALLY EXIST (~2026-09-12). Every second-unit figure here -
4600 W FROM ITS DATASHEET, 15 % illustrative, the whole roster SET - is SIMULATED and
labelled. Only inverter A's 10 % is read off hardware.
REBASED onto
|
||
|
|
8beba0a3e7 |
SAFETY-32 round 4: the same family at the SIBLING ARGUMENT, and the family enumerated
Rounds 2 and 3 hardened the FLOOR axis - the max inside binding_soc_floor(), the roster handed to it, Controller.packs, pack_floor_pct()'s conjunction. peakguard.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 |
||
|
|
a4c95f83ce |
SAFETY-32 round 3: a fixture of N packs cannot separate reductions that agree on N
Both blockers were the recurring defect sitting inside the fix written to close it: a check whose TEXT claims more than its FIXTURE can observe. Both survived a green 19-file suite on |
||
|
|
ffbabea8ce |
SAFETY-32 fix round: grade the reduction on packs whose floors DIFFER
AC 6 was not met for the reduction main.py actually hands decide(). The
reviewer removed the per-pack grading twice and the 19-file suite stayed green
both times. No shipped behaviour changes here - app/ is untouched. What changes
is what observes it.
WHY BOTH SURVIVED, and it is this repository's recurring defect landing on this
card's own Decision 2: under any rule-8-valid config every pack's
pack_floor_pct() equals peak_soc_floor, so `floors` is a list of IDENTICAL
numbers and max/min/first/last are four spellings of one answer. The only check
using a cut-out ABOVE the EMS floor - 12c's `_n1_deep` - ran on a roster of ONE,
where every reduction agrees. So no check ever evaluated binding_soc_floor() on
two packs whose floors differ. And the degeneracy is not a defence: this PR's own
argument ("unreachable is a claim about today's rule ordering, and
validate_startup_config() is also sim/inject.py's entry point") justifies writing
the reduction and equally obliges grading it.
* test_peakguard.py part 12c2 - NEW. binding_soc_floor() on a roster whose
per-pack floors ALL DIFFER: four SIMULATED cut-outs 30/25/40/35 %, each
strictly above peak_soc_floor, so max (40), min (25), first (30), last (35)
and the mean (32.5) are five different numbers and the extremes sit at
INTERIOR roster positions. Two packs structurally cannot separate those -
there max==last and min==first - and neither can three; four is the smallest
roster that can. Precondition is its own check (habit 1); the counterfactual
raises ONE pack - the last, neither extreme - past the old maximum and the
answer follows (habit 7); peak_soc_floor is then lifted above every cut-out
to grade the other side of the conjunction.
* test_peakguard.py part 12g - REWRITTEN as behaviour (habit 4). The old
assertion was `"self.packs" in <the unparsed call site>`, which `self.packs[:1]`
still satisfies. It now drives REAL Controller.cycle()s on a two-pack roster,
both packs at the same SoC, and reads PeakDecision.soc_floor - the argument,
echoed back by the shipped decide(). The cut-outs are the only thing varied,
and the SAME PAIR is carried in BOTH ORDERS.
* ⚠️ TWO MORE SURVIVORS, found by this round's own battery and recorded rather
than quietly repaired. (a) The first cut of 12g varied only pack B's cut-out,
so `self.packs[-1:]` (+5 bytes) agreed with the roster on both runs and stayed
green across all 19 files; the swapped pair closes it, and between the two
directions no single-position slice passes all three runs. (b)
binding_soc_floor()'s EMPTY-roster branch rewritten to `return None`
(-43 bytes) was green too - a defensive branch nothing in the suite reached.
Both directions of it are pinned now.
* wired_over_limit() gained a prepare(ctl) hook, inside its retry loop so every
attempt grades the same site.
* In-process mutation rows 22, 22b and 23 record all four survivors.
Nine further source mutations went through the harness on the fixed tree
(binding_soc_floor -> floors[0] / floors[-1], pack_floor_pct conjoining with
min, pack_permissions grading against packs[0], `any` -> `all` on the unknown
floor, Controller.packs reversed, decide(soc=) taking inverters[0].soc, and the
two survivors above). Seven were red on first run; the two survivors are now red
as well. Three of the nine have a ZERO byte delta and still went red, which is
the direction stale bytecode cannot fabricate - and the harness purged anyway.
MANDATORY PROOF, all in the CI image over a tree rsynced to a plain path and
bind-mounted :ro, bytecode entry count printed before and after the purge:
each of the four mutations now takes test_peakguard.py RED, and the unmutated
tree is 19/19 green (twice, plus test_peakguard.py five times in isolation -
card CI-06's flake did not reappear). The zero-byte one was proved to have RUN rather than
assumed: dis.get_instructions LOAD_GLOBALs were [float, pack_floor_pct, any,
min] and binding_soc_floor() returned 25.0 on the 12c2 roster where the shipped
code returns 40.0.
No measurement of inverter B appears anywhere. It does not physically exist.
Every second-pack and fourth-pack figure added here is SIMULATED and labelled at
its definition; only inverter A's 10 % is read off hardware. No hardware was
touched.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
|
||
|
|
f9e7fbf86d |
SAFETY-32: bms_soc_floor per pack, rule 8 per unit
`bms_soc_floor` describes A BATTERY, not a site. At two packs of different models the cut-outs differ, and one number for both graded the shallower pack against the deeper one's BMS - so a site with cut-outs of 10 % and 30 % under `peak_soc_floor: 20` STARTED, and the guard would command a forced discharge that pack B's BMS, not the operator's floor, is the thing that stops. That is rule 8's own failure mode, reached through rule 8. Scoped to the card's third bullet, per its PM PROOFREAD: the aggregate anti-windup (DEV-02) and per-instance `achievable_w` (CFG-04) were verified as already shipped and are untouched. * config.yaml: `bms_soc_floor: int(0,50)` REQUIRED per `inverters:` entry. Nothing is inherited; the flat key stays the single-inverter shape's own cut-out. A per-entry DEFAULT was declined - a default is one number for every pack, which is this card's defect - and the decision is recorded. * inverter.py: `Inverter.bms_soc_floor`; an entry that states none gets None, not a borrowed number and not 0.0 (the most permissive value the key has). * peakguard.py: `Pack`, `pack_floor_pct()`, `pack_permissions()`, `binding_soc_floor()`. `discharge_permitted()` is unchanged and is still the one place the question is answered. * validate.py: `unit_bms_floors_indexed()` carries the ROSTER index; rule 8 grades EVERY unit and NAMES the one it refuses. Graded with the offender SECOND and with the same two numbers in the other order. * main.py: `Controller.packs`; `decide(soc_floor=...)` is the per-pack reduction of the same option; the floor-limited notification names the pack that stopped the site. `pack_floor_soc` - the emptiest pack, and its None-on-missing behaviour - is untouched. * tools/supervisor_shape_probe.py: RE-RUN and repaired. The required key broke §C and left §D printing PASS on a refusal about a different key. §D is now an isolated counterfactual over an accepted merged baseline, one key varied, asserting the key name. `all cases passed` on 2026.08.0. Stated rather than hidden: under any config rule 8 accepts the per-pack FLOOR reduces to `peak_soc_floor` for every pack. The reduction is written for `unit_caps_indexed()`'s reason and graded on both sides - 1775 rule-8-valid pairs answer the option, the pair rule 8 refuses answers the cut-out. `peak_soc_floor` is still one number for the site, so the "deeper pack needlessly withheld" half is filed as an open question, not closed. Full 19-file suite green. Twelve source mutations through tools/mutation_run.sh: eleven red, one argued survivor. The battery also found `_flat_bms_floor()` defaulting in two places, each covering for the other. No measurement of inverter B appears anywhere: it does not exist yet. Every second-pack figure is simulated and labelled. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU |