admin/goodwe-addon
1
0
Fork 0
Code Issues Pull Requests 1 Actions Packages Projects Releases Wiki Activity

SAFETY-13: the bound came from the wrong half of a two-sided measurement
checks / unit (pull_request) Successful in 5m34s
Details

Browse Source 
NOTES.md 5.10 measured the 1.78 kW step BOTH ways - "Up: ~18 s from step to
deadband. Down: ~23 s" (NOTES.md:1550). SAFETY-39 takes 18 correctly: its
bound is a REFUSAL and the looser number refuses less. This branch reused
PLANT_SETTLE_S for the opposite job - how long the plant may still be the
EXPLANATION for a divergence - where the conservative half is the longer one.
ceil(23/2) = 12, not 9, and being short there does not refuse anything, it
accuses.

The false positive is real and is measured here. One inverter, one compute(),
one plant, no second writer anywhere in the harness: the command falls through
zero while the pack is still coasting the old way, unasked_power() calls our
own power "unasked", the counter reaches 9 while it is still coasting, and the
law emits "freeze-released". At the plant's own measured 18 s/23 s shape, over
272 load-step pairs, the 9-cycle bound fires in 62 and the 12-cycle bound in 2.

  PLANT_SETTLE_DOWN_S = 23.0 is added beside PLANT_SETTLE_S = 18.0, because
  the plant's settling time is a PAIR and each bound has to say which half it
  means and why.
  SETTLE_CYCLES = ceil(PLANT_SETTLE_DOWN_S / LOOP_TICK_S) = 12. It is no
  longer the reciprocal of SLEW_RAIL_FRAC; that was a coincidence of both
  reading the same half, and test_control.py now asserts the inequality.
  _SAT_COUNT_CAP moves with it, 10 -> 13. config.yaml accepts
  saturation_cycles as int(1,10), so the whole accepted range is now strictly
  BELOW the bound and the degenerate configuration this branch used to
  document no longer exists - pinned against config.yaml's own schema line.

Three shipped statements were falsified by that measurement and are rewritten,
not renumbered - at 12 the residual is smaller, not zero:

  unasked_power()'s docstring said anything outside the interval "was put
  there by something other than this loop". It was our own power: eight cycles
  after a +1990 W command the command is 0 and the pack still reads +522.3 W.
  control.py said "SO THE BOUND BELONGS TO (b) AND ONLY TO (b)". It fired in
  case (a).
  DOCS.md told an operator "if you see freeze-released, look for the second
  writer" - on a single-inverter install, hunting something that does not
  exist. Replaced by a section that gives the innocent causes first (a large
  load or PV swing; a plant slower than the one measured, 8/320 scenarios at
  23 s rising to 268/320 at 50 s) and the second writer only when the state
  STANDS.

Round 1's own results are kept and re-graded, not weakened. The release/1.0
sweep had to widen to reach the new bound (3780 cases): 3267 bit-identical,
432 releases, 27 command changes - all still charge starts from prev_w == 0 -
and 81 differing in the saturation counter alone, which nothing downstream can
read. The card's case releases on the twelfth saturated cycle instead of the
ninth and settles at the same -1190 W against the same frozen integrator.

Also corrected, because they were claims and did not reproduce: the coverage
table's "output freeze" row was 11, and the mutation form its own note
describes gives 6 on this tree, 6 on the first SAFETY-13 commit and 2 on
release/1.0; the detector row was left at 11 and is 15; the frozen = False
footnote was left at 10 and is 13. And section 6 reported 107 625 as "released
states" when it is the number of states SWEPT - 67 500 of them release, and
both are counted now.

Nothing here reached the inverter. 22/22 test files pass in goodwe-addon-ci,
tree rsynced to a plain path, mounted :ro, python3 -B, __pycache__ purged and
printed first (0 dirs / 0 .pyc; the worktree carries none).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
This commit is contained in:
glenn schrooyen
2026-09-06 18:32:03 +02:00
co-authored by Claude Opus 5
parent 6c4565659b
commit f156fadac0
5 changed files with 648 additions and 150 deletions
Download Patch File Download Diff File Expand all files Collapse all files
goodwe_controller/test_control.py
+265 -42
View File
@@ -17,9 +17,9 @@ Read MUTATION.md before you report a survivor.
import sys
from app.control import (LOOP_TICK_S, PLANT_SETTLE_S, SETTLE_CYCLES,
SLEW_RAIL_FRAC, Tuning, compute, slew_limit_w,
unasked_power,
from app.control import (LOOP_TICK_S, PLANT_SETTLE_DOWN_S, PLANT_SETTLE_S,
SETTLE_CYCLES, SLEW_RAIL_FRAC, Tuning, compute,
slew_limit_w, unasked_power,
maintenance_charge_floor, peak_at_risk)
# ⚠️ SAFETY-39: `slew_w` IS EXPLICIT HERE NOW, AND IT IS release/1.0's VALUE.
@@ -60,16 +60,33 @@ def check(name, cond):
# A comment cannot go stale-green, because it never claims to be running.
#
# Measured at 389d9ec. Numbers are the lead's independent reproduction.
# ⚠️ THE OUTPUT FREEZE ROW WAS RE-MEASURED AT SAFETY-13 AND IT MOVED FROM 2 TO
# 11, because the SAFETY-13 section grades that branch too. Both figures are
# from the SAME mutation form - the whole `target = min(...)/max(...)` line
# removed, `reason` left alone - and 2 was reproduced on a pristine c8dcb38
# tree before the new figure was taken, so the row moved because checks were
# added and not because the mutation changed shape. The two new rows below it
# are that section's own mechanisms: removing the EXIT restores release/1.0's
# unbounded freeze, and making `unasked_power()` return True gives an exit to
# the limit case as well, which is the half of the decision that has to stay
# unbounded.
# ⚠️ THE SAFETY-13 ROWS WERE RE-MEASURED IN ROUND 2 AND THREE OF THEM WERE
# WRONG AS FIRST WRITTEN. Every figure below marked (S13) was taken by deleting
# the mechanism, purging __pycache__, running this file in the CI image and
# counting `FAIL` lines, on THIS tree; the release/1.0 comparison figures were
# taken the same way on a pristine c8dcb38 worktree.
#
# - `output freeze` was written as 11. The mutation form its own note
# describes - the whole `target = min(...)/max(...)` line removed, `reason`
# left alone - gives 6 on this tree AND 6 on the first SAFETY-13 commit,
# against 2 on release/1.0. 11 is not reproducible by that form, or by
# removing the line and its `reason` (4), or by swapping min/max (12). The
# row is 6.
# - `saturation detector, saturated_now = False` was left at 11 while the
# SAFETY-13 section added checks that grade it. It is 15.
# - the footnote's `frozen = False` figure was left at 10 for the same
# reason. It is 13.
#
# The rows below `output freeze` are this ticket's own mechanisms: removing the
# EXIT restores release/1.0's unbounded freeze; making `unasked_power()` return
# True gives an exit to the limit case as well, which is the half of the
# decision that has to stay unbounded; deriving SETTLE_CYCLES from
# PLANT_SETTLE_S (18 s, the UP ramp) instead of PLANT_SETTLE_DOWN_S (23 s) is
# the round-1 defect itself; and pinning `_SAT_COUNT_CAP` back at release/1.0's
# literal 10 caps the counter below the bound and deletes the exit silently.
#
# ⚠️ ONLY THE ROWS THIS BRANCH MOVES WERE RE-MEASURED. Everything not marked
# (S13) still carries 389d9ec's figures and was not re-run here.
#
# ⚠️ THE SLEW ROWS WERE RE-MEASURED AT SAFETY-39 AND ONE OF THEM MOVED: the
# slew limit was 4 and is now 5, because the SAFETY-39 section grades it too.
@@ -87,12 +104,14 @@ def check(name, cond):
# output clamp 3
# slew limit 5
# slew follows the rail (SAFETY-39), `slew_w` read raw 3
# output freeze 11
# the output freeze's EXIT (SAFETY-13), freeze made unconditional again 4
# `unasked_power()` discriminates, replaced by `return True` 6
# output freeze (S13) 6
# the output freeze's EXIT (S13), freeze made unconditional again 4
# `unasked_power()` discriminates, replaced by `return True` (S13) 6
# SETTLE_CYCLES from PLANT_SETTLE_S, not _DOWN_S (S13) 9
# `_SAT_COUNT_CAP` pinned back at release/1.0's 10 (S13) 6
# deadband 5
# quantisation 2
# saturation detector, `saturated_now = False` 11
# saturation detector, `saturated_now = False` (S13) 15
# saturation duration (AC 2), fires instantly 2
# sat counter reset on a good cycle 6
# target_grid_w bias 3
@@ -100,7 +119,8 @@ def check(name, cond):
#
# The detector figure is for the `saturated_now = False` form specifically;
# disabling it further down as `frozen = False` is a weaker mutation and gives
# 10. Reproduce the same form or the number will not match.
# 13 on this tree (10 on release/1.0). Reproduce the same form or the number
# will not match.
#
# ⚠️ IT HAS FOUND A DEAD MECHANISM TWICE, BOTH THE SAME WAY: a clamp standing in
# for the mechanism under test. Deleting the integrator freeze once failed
@@ -416,12 +436,30 @@ same = all(unasked_power(0.0, a, 500.0) == (abs(a) > 500.0)
check("at prev_w == 0 unasked_power IS the saturation test, over 801 readings",
same)
# --- 2. the bound is derived, not chosen ------------------------------------
check(f"SETTLE_CYCLES is ceil(PLANT_SETTLE_S / LOOP_TICK_S) = {SETTLE_CYCLES}",
SETTLE_CYCLES == 9 and SETTLE_CYCLES * LOOP_TICK_S >= PLANT_SETTLE_S
and (SETTLE_CYCLES - 1) * LOOP_TICK_S < PLANT_SETTLE_S)
check("...which is the reciprocal of SAFETY-39's SLEW_RAIL_FRAC",
abs(SETTLE_CYCLES - 1.0 / SLEW_RAIL_FRAC) < 1e-9)
# --- 2. the bound is derived, and from WHICH HALF of the measurement --------
# ⚠️ THE DIRECTION IS THE ASSERTION. goodwe/NOTES.md 5.10 measured the same
# 1.78 kW step both ways: ~18 s up, ~23 s down. SAFETY-39 takes the SHORTER
# one because its bound is a REFUSAL and the looser number refuses less. This
# bound asks the opposite question - how long the plant may still be the
# explanation for a divergence - and for that the conservative half is the
# LONGER one. The first version of this file derived it from 18, got 9, and
# that is three cycles short of the plant's own measured down-ramp, in the
# direction that ACCUSES rather than refuses (section 8 below drives it).
check(f"SETTLE_CYCLES is ceil(PLANT_SETTLE_DOWN_S / LOOP_TICK_S) ="
f" {SETTLE_CYCLES}",
SETTLE_CYCLES == 12
and SETTLE_CYCLES * LOOP_TICK_S >= PLANT_SETTLE_DOWN_S
and (SETTLE_CYCLES - 1) * LOOP_TICK_S < PLANT_SETTLE_DOWN_S)
check("...from the LONGER of the two measured settle times, so it is strictly"
" above what the shorter one would have given",
PLANT_SETTLE_DOWN_S > PLANT_SETTLE_S
and SETTLE_CYCLES > -(-PLANT_SETTLE_S // LOOP_TICK_S))
# ...and it is NOT SLEW_RAIL_FRAC's reciprocal any more. It was, while both
# were being derived from the same half of the pair, and that coincidence read
# as a derivation. Asserted as an INEQUALITY so the two cannot silently be
# re-fused into one number again.
check("the slew's rail crossing and this bound are now different numbers",
SETTLE_CYCLES > 1.0 / SLEW_RAIL_FRAC)
# The counter has to be able to REACH the bound or the exit does not exist.
# Driven, not read off the constant: run a saturated state and see how high the
# counter actually goes.
@@ -529,41 +567,179 @@ check(f"the card's case: no cycle moves more than the slew limit "
# that built up while the output was blocked cannot arrive as a jump - it is
# spent one slew step at a time, against an integrator that stopped
# accumulating when the freeze engaged and is not released with the output.
# ⚠️ AND THE COUNT BELOW IS THE RELEASED STATES, NOT THE SWEPT ONES. The first
# version of this check named 41*25*21*5 - the size of the sweep - while
# grading only the subset that actually releases, so the number in the message
# was not the number the assertion was about. It is counted now.
step = float(T.step_w)
past, jumped = [], []
swept, past, jumped = 0, [], []
n_released = 0
for prev in [x * 250.0 for x in range(-20, 21)]:
for grid in [x * 500.0 for x in range(-12, 13)]:
for actual in [x * 500.0 for x in range(-10, 11)]:
for i0 in (-3000.0, -500.0, 0.0, 500.0, 3000.0):
swept += 1
d = compute(prev, grid, actual, TL, SETTLE_CYCLES, i0)
if d.reason != "freeze-released":
continue
n_released += 1
lo, hi = min(prev, d.i_w), max(prev, d.i_w)
if not (lo - step <= d.target_w <= hi + step):
past.append((prev, grid, actual, i0, d.target_w, d.i_w))
if abs(d.target_w - prev) > slew_limit_w(TL) + step:
jumped.append((prev, grid, actual, i0, d.target_w))
check(f"over {41*25*21*5} released states the command stays between the"
f" previous command and the frozen integrator"
+ (f" (e.g. {past[0]})" if past else ""), not past)
check(f"of {swept} states swept, the {n_released} that release keep the command"
f" between the previous command and the frozen integrator"
+ (f" (e.g. {past[0]})" if past else ""), not past and n_released > 0)
check("...and no released cycle moves further than one slew step"
+ (f" (e.g. {jumped[0]})" if jumped else ""), not jumped)
# --- 7. the one configuration in which the block does not exist ------------
# ⚠️ SAID OUT LOUD BECAUSE IT IS A SILENT NO-OP OTHERWISE. `saturation_cycles`
# is accepted up to 10 by config.yaml. Set it at or above SETTLE_CYCLES and the
# freeze does not engage until the bound has already passed, so the no-start
# block never happens at all. It is not refused at startup - a controller that
# will not boot over a tuning nuance is worse than the nuance - but it must be
# a known consequence rather than a surprise.
TN = Tuning(slew_w=1000.0, saturation_cycles=SETTLE_CYCLES)
# --- 7. NO ACCEPTED CONFIGURATION CAN DELETE THE BLOCK ---------------------
# ⚠️ THIS CHECK REPLACES ITS OWN OPPOSITE, AND THE REASON IS WORTH KEEPING.
# While the bound was 9, `saturation_cycles` - which config.yaml accepts up to
# 10 - could be set AT OR ABOVE it, and then the freeze did not engage until
# its own exit was already due: the no-start block silently stopped existing,
# and this file asserted that as a known consequence. Moving the bound to 12
# put the whole accepted range strictly below it, so the degenerate
# configuration is gone rather than documented.
#
# It is pinned against config.yaml ITSELF and not a transcription, because the
# property is "two files agree" and a transcription is what lets them drift.
# Regex, not PyYAML: the add-on image ships no PyYAML (test_validate.py says
# the same thing at more length).
import os # noqa: E402
import re # noqa: E402
_CFG = os.path.join(os.path.dirname(os.path.abspath(__file__)), "config.yaml")
with open(_CFG, encoding="utf-8") as _fh:
_m = re.search(r"^ saturation_cycles: int\((\d+),(\d+)\)\s*$",
_fh.read(), re.M)
check("config.yaml's saturation_cycles range really was read", _m is not None)
_sc_lo, _sc_hi = int(_m.group(1)), int(_m.group(2))
check(f"every accepted saturation_cycles ({_sc_lo}..{_sc_hi}) is strictly"
f" below the bound ({SETTLE_CYCLES}), so no accepted configuration can"
f" push the freeze's engagement past its own exit",
_sc_hi < SETTLE_CYCLES)
# Driven at the schema's edge rather than argued: the block still engages, and
# it engages before the exit is due.
TN = Tuning(slew_w=1000.0, saturation_cycles=_sc_hi)
prev, i_w, sat, reasons = 0.0, 0.0, 0, set()
first_freeze = None
for _ in range(20):
d = compute(prev, -2000.0, 700.0, TN, sat, i_w)
reasons.add(d.reason)
if d.reason == "saturated-freeze" and first_freeze is None:
first_freeze = d.sat_count
prev, i_w, sat = d.target_w, d.i_w, d.sat_count
check(f"saturation_cycles >= {SETTLE_CYCLES} means the block never engages",
"saturated-freeze" not in reasons)
check(f"at the largest accepted saturation_cycles ({_sc_hi}) the block still"
f" engages, at sat_count {first_freeze}, below the bound",
"saturated-freeze" in reasons and first_freeze is not None
and first_freeze < SETTLE_CYCLES)
# --- 8. THE BOUND'S DIRECTION, DRIVEN ON ONE INVERTER ----------------------
# ⚠️ WHY THIS SECTION EXISTS. The exit's two conditions are read as "another
# writer is on the actuator". They are not that, and the first shipped form of
# this file said they were. `unasked_power()` compares a reading against ONE
# cycle's command while the pack carries every command before it, so a command
# that has fallen THROUGH ZERO - or simply fallen faster than the pack coasts -
# leaves our own power outside our own interval. With the bound derived from
# the 18 s UP measurement that is not a corner case: it is what a normal load
# step does.
#
# The plant here is a MODEL and is labelled one. It is a first-order lag whose
# two time constants come from the two measured settling times (a first-order
# step is 95 % done at 3 tau, so tau = t / 3), with the ramp cap
# sim/plantsim.py measured on inverter A. It is not the rig and it is not the
# house; what it is for is that the two settling times ENTER the model in the
# same direction they enter the constant, so the check moves if either does.
#
# ⚠️ AND THERE IS NO SECOND WRITER IN THIS SECTION. One `compute()`, one
# plant, one command. Every `freeze-released` below is therefore false.
import math # noqa: E402
class _Plant:
"""One inverter, obeying our command and nothing else. A MODEL."""
RAMP_W_S = 800.0 # sim/plantsim.py INVERTER_A, measured=True
def __init__(self, up_s, down_s):
self.a_up = 1.0 - math.exp(-LOOP_TICK_S / (up_s / 3.0))
self.a_dn = 1.0 - math.exp(-LOOP_TICK_S / (down_s / 3.0))
self.w = 0.0
def tick(self, cmd):
a = self.a_up if abs(cmd) > abs(self.w) else self.a_dn
cap = self.RAMP_W_S * LOOP_TICK_S
self.w += max(-cap, min(cap, a * (cmd - self.w)))
from app import control as _control # noqa: E402
TS8 = Tuning(max_w=5000.0, slew_w=400.0, target_grid_w=-10.0,
saturation_w=500.0, saturation_cycles=3)
def _drive(bound, load1, load2, cycles=60, switch=25):
"""Run one closed loop at an arbitrary bound. -> (release cycles, rows)."""
was_b, was_c = _control.SETTLE_CYCLES, _control._SAT_COUNT_CAP
# ⚠️ BOTH, OR THE PROBE LIES: `_SAT_COUNT_CAP` is what `compute()` caps the
# counter with, so moving the bound without it caps the counter BELOW the
# bound and the exit quietly becomes unreachable - which reads as "no false
# positives". That is the hazard `_SAT_COUNT_CAP`'s own comment names.
_control.SETTLE_CYCLES, _control._SAT_COUNT_CAP = bound, bound + 1
try:
p = _Plant(PLANT_SETTLE_S, PLANT_SETTLE_DOWN_S)
prev, i_w, sat, rows = 0.0, 0.0, 0, []
for c in range(cycles):
load = load1 if c < switch else load2
d = compute(prev, load - p.w, p.w, TS8, sat, i_w)
rows.append((c, prev, p.w, d.target_w, d.sat_count, d.reason))
prev, i_w, sat = d.target_w, d.i_w, d.sat_count
p.tick(prev)
return [r for r in rows if r[5] == "freeze-released"], rows
finally:
_control.SETTLE_CYCLES, _control._SAT_COUNT_CAP = was_b, was_c
_SHORT = int(-(-PLANT_SETTLE_S // LOOP_TICK_S)) # what 18 s would give: 9
# A 4 kW export falling to 2.5 kW. Nothing exotic; no second writer.
_bad, _rows = _drive(_SHORT, -4000.0, -2500.0)
check(f"a bound derived from the SHORTER measurement ({_SHORT} cycles) fires"
f" the exit on ONE inverter with nothing else on the bus"
+ (f" - {len(_bad)} cycle(s), first at cycle {_bad[0][0]}" if _bad else ""),
bool(_bad))
if _bad:
_c, _prev, _act, _tgt, _sat, _ = _bad[0]
check(f"...and what it called unasked is our own coast-down: command"
f" {_prev:.0f} W, pack still at {_act:.1f} W, and the pack was"
f" commanded {min(r[1] for r in _rows[:_c]):.0f} W a few cycles"
f" earlier",
unasked_power(_prev, _act, TS8.saturation_w)
and abs(_act) > abs(_prev)
and min(r[1] for r in _rows[:_c]) < _act)
_good, _ = _drive(SETTLE_CYCLES, -4000.0, -2500.0)
check(f"the shipped bound ({SETTLE_CYCLES} cycles, the LONGER measurement)"
f" does not fire on the same run", not _good)
# ...and not on any of these, either. The whole grid of load steps the same
# plant can be given, at the tuning every headline figure in this ticket is
# quoted from.
_L = [x * 500.0 for x in range(-8, 9)]
_fired = {}
for _b in (_SHORT, SETTLE_CYCLES):
_fired[_b] = sum(1 for _a in _L for _z in _L
if _a != _z and _drive(_b, _a, _z)[0])
_pairs = len(_L) * (len(_L) - 1)
check(f"over {_pairs} load-step pairs on the measured plant, one inverter and"
f" no second writer: the short bound fires in {_fired[_SHORT]} of them,"
f" the shipped bound in {_fired[SETTLE_CYCLES]}",
_fired[SETTLE_CYCLES] < _fired[_SHORT])
# ⚠️ AND THE SHIPPED FIGURE IS NOT ZERO IN GENERAL. It is small here because
# the plant in this model is the one that was measured. A plant slower than
# that brings the false release back, and no constant derived from a
# measurement can fix that - it is why DOCS.md tells the operator what
# `freeze-released` is evidence OF, rather than what it proves.
print("SAFETY-04: the i_w=None path is still release/1.0, exactly")
@@ -611,9 +787,27 @@ def legacy(prev, grid, actual, t, sat_count):
# that permit it both true. Anything else is a regression, and the counts below
# say how much of the sweep each answer covers.
ALIAS = {"i-clamped": "clamped"}
# ⚠️ SAFETY-13 ROUND 2 MOVED THE COUNTER'S CEILING, SO THE SWEEP NOW HAS A
# THIRD ANSWER. `_SAT_COUNT_CAP` is `SETTLE_CYCLES + 1`, which was 10 - the
# same literal release/1.0 used - and is now 13. Above release/1.0's own
# ceiling the two counters therefore differ, and NOTHING ELSE MAY: `frozen` is
# `sat_count >= saturation_cycles` and config.yaml accepts that at most 10, so
# a counter reading 13 instead of 10 cannot change it, and no other line in
# `compute()` reads the counter's value. That is asserted rather than asserted-
# by-omission, in `cap_diffs` below.
#
# ⚠️ AND THE SWEEP HAS TO REACH THE BOUND OR IT GRADES NOTHING. `sc` runs to 12
# now; at 9 the counter tops out one short of the exit and every release
# silently disappears from this table, which is exactly what happened when the
# bound moved and is why the count is asserted and not merely printed. 12 is a
# state release/1.0 could never hold - its counter stopped at 10 - so
# `legacy()` is being fed one input outside its own reachable domain, on
# purpose, and `cap_diffs` is where that shows up.
LEGACY_SAT_CAP = 10 # release/1.0's literal, transcribed in legacy()
diffs = []
released = []
value_diffs = []
cap_diffs = []
seen = set()
# ⚠️ `slew_w` IS WRITTEN OUT IN ALL THREE (SAFETY-39). `legacy()` below is a
# TRANSCRIPTION of release/1.0 and reads `t.slew_w` directly, as release/1.0
@@ -627,7 +821,7 @@ for tune in (Tuning(slew_w=1000.0), Tuning(slew_w=1000.0, target_grid_w=-10.0),
for prev in (-2000.0, -500.0, -100.0, 0.0, 100.0, 500.0, 2000.0):
for grid in (-6000.0, -1000.0, -500.0, -14.0, 0.0, 14.0, 500.0, 1000.0, 6000.0):
for actual in (-2000.0, 0.0, 600.0, 2000.0):
for sc in (0, 2, 3, 9):
for sc in (0, 2, 3, 9, 12):
d = compute(prev, grid, actual, tune, sc) # i_w defaults to None
seen.add(d.reason)
got = (d.target_w, d.sat_count, d.frozen,
@@ -635,6 +829,19 @@ for tune in (Tuning(slew_w=1000.0), Tuning(slew_w=1000.0, target_grid_w=-10.0),
was = legacy(prev, grid, actual, tune, sc)
if got == was:
continue
# everything that reaches the wire, without the counter
wire_same = (got[0], got[2], got[3]) == (was[0], was[2], was[3])
if wire_same:
# the ceiling moved and nothing else did. Only legal
# above release/1.0's own cap, and only with both
# counters standing at their own ceilings.
if (sc >= LEGACY_SAT_CAP
and was[1] == LEGACY_SAT_CAP
and got[1] == _control._SAT_COUNT_CAP):
cap_diffs.append((prev, grid, actual, sc, got[1], was[1]))
continue
diffs.append((prev, grid, actual, sc, got, was))
continue
explained = (
d.reason == "freeze-released"
and was[3] == "saturated-freeze"
@@ -646,12 +853,28 @@ for tune in (Tuning(slew_w=1000.0), Tuning(slew_w=1000.0, target_grid_w=-10.0),
released.append((prev, grid, actual, sc))
if got[0] != was[0]:
value_diffs.append((prev, got[0], was[0]))
TOTAL = 3 * 7 * 9 * 4 * 4
TOTAL = 3 * 7 * 9 * 4 * 5
check(f"i_w=None reproduces release/1.0 over {TOTAL} cases except where"
f" SAFETY-13 releases the freeze, reason included"
+ (f" (first unexplained diff {diffs[0]})" if diffs else ""), not diffs)
check(f"{TOTAL - len(released)} of {TOTAL} cases are bit-identical to"
f" release/1.0; {len(released)} are releases", len(released) == 432)
# ⚠️ EXACT COUNTS, NOT INEQUALITIES. A weaker form of this line ("some
# releases happened") was written while the bound was moving, and the coverage
# audit caught it immediately: a `unasked_power()` that stops discriminating
# went from 6 checks to 5. The three numbers partition the sweep, so any one of
# them moving is a change somebody has to explain.
check(f"{TOTAL - len(released) - len(cap_diffs)} of {TOTAL} cases are"
f" bit-identical to release/1.0; {len(released)} are releases;"
f" {len(cap_diffs)} differ in the saturation counter alone",
len(released) == 432 and len(cap_diffs) == 81
and TOTAL - len(released) - len(cap_diffs) == 3267)
# ⚠️ THE COUNTER-ONLY DIFFERENCES ARE NOT A LOOPHOLE, so they are pinned twice:
# they may only occur at an `sc` above release/1.0's ceiling, and the largest
# `saturation_cycles` config.yaml accepts is below BOTH ceilings, so no
# accepted configuration can see the difference at all.
check(f"the {len(cap_diffs)} counter-only differences all sit above"
f" release/1.0's cap of {LEGACY_SAT_CAP}, where no accepted"
f" saturation_cycles can read them",
all(r[3] >= LEGACY_SAT_CAP for r in cap_diffs) and _sc_hi <= LEGACY_SAT_CAP)
# ⚠️ AND THE RELEASES ARE MOSTLY A LABEL. Only these change what reaches the
# wire; the rest report "freeze-released" on a command the freeze was not
# binding on anyway. Every one of them is a charge that release/1.0 refused to