SAFETY-13: the output freeze gets an exit, and only where it needs one
checks / unit (pull_request) Successful in 5m30s

While the loop is frozen the command's magnitude may fall but never rise. At
prev_w == 0 there is no magnitude left to fall, so a charge cannot START. That
refusal is deliberate and it is kept: the inverter reporting power we did not
command means another writer is on the actuator, which is the §1.5 non-goal.
What it did not have was an END - nothing cleared it but the other writer
leaving.

Reproduced on release/1.0 @ c8dcb38, at the live install's shape (max_w 5000,
slew_w 400, target_grid_w -10), with another writer holding the pack at +700 W.
The route is not the obvious one: entering from an export, the slew limit moves
the command off zero before the counter reaches 3. It is entered from the
DEADBAND - a site resting at its target counts saturated cycles while nothing is
wrong - and 0 W is then a fixed point: a 2 kW export arriving afterwards leaves
the command at exactly 0.0 W on every subsequent cycle.

And prev_w == 0 is not where it stops. The same tuning pins at -800 W against
its own integrator standing at -2388 W, with the same absence of an exit. So the
change is written against the output freeze, not against a special case of it.

THE DECISION IS WHICH FREEZES GET AN EXIT, NOT HOW LONG THE BLOCK LASTS.

  - A divergence a LIMIT could have produced - the inverter doing less than the
    command, in the command's own direction - clears itself, because the command
    is pinned at something the inverter can reach. No exit. release/1.0
    unchanged, and asserted so: a curtailed inverter is never released over 30
    cycles.
  - A divergence a limit could NOT have produced - overshooting the command, or
    the opposite sign - cannot clear itself, because clearing it needs the
    inverter to track OUR command. That one releases.

unasked_power() is that predicate and it is physical, not statistical: a limit
can only make the inverter do less, in the command's own direction, so
everything a limit can produce lies in the interval spanned by 0 and prev_w
widened by saturation_w. At prev_w == 0 it IS the saturation test, which is
exactly why the zero case is the one that strands.

The bound is not a new number. SETTLE_CYCLES = ceil(PLANT_SETTLE_S /
LOOP_TICK_S) = 9, SAFETY-39's two measured constants and the reciprocal of
SLEW_RAIL_FRAC: a divergence still standing after the plant's own settling time
is not this plant catching up. _SAT_COUNT_CAP is written as SETTLE_CYCLES + 1;
its value is unchanged at 10.

RELEASING THE OUTPUT FREEZE DOES NOT UNFREEZE THE LOOP, which is what makes this
bounded. The integrator freeze is untouched, so a released cycle can only move
the command toward an accumulator that stopped accumulating, by at most one slew
step, and never past it - swept over 107 625 released states. On the run above
the command starts on the ninth saturated cycle and settles at -1190 W against a
frozen integrator of -1194 W, not at the 5000 W rail.

Graded against a transcription of release/1.0 over the 3024-case sweep, which
was NOT taught the new rule: 2592 cases bit-identical, 432 releases, and 27 of
those change the command - every one a charge from prev_w == 0 that release/1.0
refused to start.

SAFETY-04's deliberate assertion is kept rather than inverted: its fixture sits
below the bound, so it still asserts the block, and the release is asserted
beside it on the other side of the bound.

Coverage audit re-measured, same mutation form, __pycache__ purged: output
freeze 2 -> 11 (2 reproduced on a pristine c8dcb38 first), the exit 4,
unasked_power 6.

saturation_cycles at 9 or 10 removes the block entirely, because the freeze
cannot engage before its own exit is due. Not refused at startup; asserted in
the tests and written in DOCS.md.

Nothing was measured on two inverters: inverter B does not physically exist
(NOTES.md §1.1b) and sim/plantsim.py:216 INVERTER_B is INVERTER_A copied with
measured=False. The N=2 escalation is stated from the code (actual_w is
site_batt_w, the SUM) and is labelled as such.

22/22 test files pass in goodwe-addon-ci, mounted :ro, bytecode purged first.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
This commit is contained in:
2026-09-06 13:56:26 +02:00
co-authored by Claude Opus 5
parent c8dcb38a95
commit 6c4565659b
5 changed files with 761 additions and 13 deletions
+251 -9
View File
@@ -17,8 +17,9 @@ Read MUTATION.md before you report a survivor.
import sys
from app.control import (LOOP_TICK_S, PLANT_SETTLE_S, SLEW_RAIL_FRAC,
Tuning, compute, slew_limit_w,
from app.control import (LOOP_TICK_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.
@@ -59,6 +60,17 @@ 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 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.
# The new row is the RAIL DEFAULT specifically - `slew_limit_w()` reduced to
@@ -75,7 +87,9 @@ def check(name, cond):
# output clamp 3
# slew limit 5
# slew follows the rail (SAFETY-39), `slew_w` read raw 3
# output freeze 2
# output freeze 11
# the output freeze's EXIT (SAFETY-13), freeze made unconditional again 4
# `unasked_power()` discriminates, replaced by `return True` 6
# deadband 5
# quantisation 2
# saturation detector, `saturated_now = False` 11
@@ -282,8 +296,15 @@ check("frozen at i_w=0.0: an export push moves the integrator",
# hundreds of watts means something else is driving the bus. Asserted so that
# nobody "fixes" it by accident - the integrator moving is what this ticket
# owns, the command rule belongs to the output freeze.
#
# ⚠️ SAFETY-13 KEPT THIS ASSERTION RATHER THAN INVERTING IT, and the fixture is
# why it survived unchanged: `sat_count=3` becomes 4, which is below
# SETTLE_CYCLES, so this is still inside the window in which the block holds.
# SAFETY-13 gave the block an EXIT, not a different opinion about its first
# cycles - see the SAFETY-13 section below, where the same state is driven past
# the bound and the release is asserted on the other side of it.
check("frozen at i_w=0.0: the output freeze still blocks a charge from 0 W",
ze.target_w == 0.0)
ze.target_w == 0.0 and ze.sat_count < SETTLE_CYCLES)
# Where prev_w is already charging the output freeze does NOT block, and there
# the difference reaches the wire: held at 0.0 the integrator abandons the
# charge mid-export.
@@ -358,6 +379,192 @@ check(f"after saturation ends the command is {tight:.0f} W (<= 1000)", tight <=
check(f"headroom above max_w makes that worse ({loose:.0f} W) - hence the default",
loose > tight)
print("SAFETY-13: the output freeze has an exit, and only where it needs one")
# THE SHAPE OF THIS SECTION. release/1.0's output freeze holds the command's
# magnitude down while the inverter is not following, and nothing ends it. At
# `prev_w == 0` the held magnitude is ZERO, so it reads as "refuses to start a
# charge"; that is the case the card was written about, but it is one instance
# of a rule that is unbounded at every prev_w. SAFETY-13 bounds it exactly where
# it CANNOT end on its own - see `unasked_power()` - and nowhere else.
# --- 1. the predicate, which is the whole of the decision -------------------
# A limit can only make the inverter do LESS than the command, in the command's
# own direction, so everything a limit can produce lies in the interval spanned
# by 0 and prev_w widened by saturation_w. These are the four cases in the
# docstring, run rather than described.
check("limit: 700 W under a +2000 W command is explainable",
not unasked_power(2000.0, 700.0, 500.0))
check("limit: -700 W under a -5000 W command is explainable",
not unasked_power(-5000.0, -700.0, 500.0))
check("unasked: +700 W under a 0 W command is not",
unasked_power(0.0, 700.0, 500.0))
check("unasked: +700 W under a -800 W command is not",
unasked_power(-800.0, 700.0, 500.0))
# The band edges belong to the limit side, because saturation_w is the same
# tolerance the detector uses - a reading the detector calls "following" must
# never be called "another writer".
check("the saturation band is inclusive on both edges",
not unasked_power(0.0, 500.0, 500.0)
and not unasked_power(0.0, -500.0, 500.0)
and unasked_power(0.0, 500.01, 500.0))
# ⚠️ AT prev_w == 0 THE PREDICATE AND THE DETECTOR ARE THE SAME TEST, which is
# why the zero case is the one that strands: with nothing commanded there is no
# interval for a limit to live in.
same = all(unasked_power(0.0, a, 500.0) == (abs(a) > 500.0)
for a in [x * 5.0 for x in range(-400, 401)])
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)
# 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.
c, sc = 0, 0
while c < 50:
sc = compute(0.0, -2000.0, 900.0, T, sc).sat_count
c += 1
check(f"the saturation counter reaches {sc}, which is above the bound",
sc >= SETTLE_CYCLES)
# --- 3. prev_w == 0: blocked below the bound, released above it -------------
# The same state either side of the bound. This is the pair the card asks for.
blk = compute(prev_w=0, grid_w=-2000, actual_w=-600, tuning=T,
sat_count=SETTLE_CYCLES - 2, i_w=0.0)
check("prev_w=0: below the bound the charge is still refused",
blk.target_w == 0.0 and blk.reason == "saturated-freeze"
and blk.sat_count == SETTLE_CYCLES - 1)
rel = compute(prev_w=0, grid_w=-2000, actual_w=-600, tuning=T,
sat_count=SETTLE_CYCLES - 1, i_w=0.0)
check(f"prev_w=0: at the bound it is released to {rel.target_w:.0f} W",
rel.target_w < 0.0 and rel.reason == "freeze-released"
and rel.sat_count == SETTLE_CYCLES)
# ...and the released command is the SLEW step from 0, not the rail. A release
# that jumped to the integrator in one cycle would be the windup this ticket
# was told to avoid.
check(f"the released command is exactly one slew step"
f" ({slew_limit_w(T):.0f} W)",
abs(rel.target_w) == slew_limit_w(T))
# The mirror. Nothing here is sign-specific, so the discharge side must behave
# identically - every freeze rule in this file has a mirror, because the one
# that did not is the defect that got through review.
mblk = compute(prev_w=0, grid_w=2000, actual_w=600, tuning=T,
sat_count=SETTLE_CYCLES - 2, i_w=0.0)
mrel = compute(prev_w=0, grid_w=2000, actual_w=600, tuning=T,
sat_count=SETTLE_CYCLES - 1, i_w=0.0)
check("prev_w=0, discharging: same block, same release, mirrored",
mblk.reason == "saturated-freeze" and mrel.reason == "freeze-released"
and mrel.target_w == slew_limit_w(T))
# --- 4. non-zero prev_w, and the two halves are NOT the same --------------
# (a) A divergence a LIMIT could have produced is never released, however long
# it stands. This is release/1.0's behaviour and it is kept deliberately: the
# freeze clears itself here, because the command is pinned at something the
# inverter can do.
TL = Tuning(max_w=5000.0, slew_w=400.0, target_grid_w=-10.0)
prev, i_w, sat, reasons = 0.0, 0.0, 0, set()
for _ in range(30):
d = compute(prev, 4000.0, max(-1000.0, min(1000.0, prev)), TL, sat, i_w)
prev, i_w, sat, _r = d.target_w, d.i_w, d.sat_count, reasons.add(d.reason)
check("non-zero prev_w, a curtailed inverter: never released over 30 cycles",
"freeze-released" not in reasons and prev == 2400.0)
# (b) A divergence a limit could NOT have produced is released at the bound,
# at a non-zero prev_w exactly as at zero. release/1.0 pinned this run at
# -800 W, against its own integrator standing at -2388 W, for as long as it ran.
prev, i_w, sat, rows = 0.0, 0.0, 0, []
for _ in range(20):
d = compute(prev, -2000.0, 700.0, TL, sat, i_w)
rows.append((prev, d.target_w, d.i_w, d.reason))
prev, i_w, sat = d.target_w, d.i_w, d.sat_count
pinned = [r for r in rows if r[3] == "saturated-freeze"]
check(f"non-zero prev_w, another writer: pinned at {pinned[0][1]:.0f} W...",
pinned and all(r[1] == -800.0 for r in pinned))
check(f"...then released, settling at {prev:.0f} W", prev == -2390.0)
# --- 5. THE CARD'S OWN CASE, DRIVEN END TO END -----------------------------
# The live install's shape (max_w 5000, slew_w 400, target_grid_w -10). The site
# rests in the deadband with another writer holding the pack at +700 W - so the
# saturation counter climbs while the command is 0 and nothing is wrong - and
# then 2 kW of export arrives. On release/1.0 @ c8dcb38 the command is 0.0 W on
# every cycle from there on: 0 W is a FIXED POINT, and the export is given away
# for as long as the other writer stays.
prev, i_w, sat, cmds = 0.0, 0.0, 0, []
for c in range(24):
d = compute(prev, -10.0 if c < 6 else -2000.0, 700.0, TL, sat, i_w)
cmds.append(d.target_w)
prev, i_w, sat = d.target_w, d.i_w, d.sat_count
check("the card's case: the block does hold at first, at 0 W",
cmds[6] == 0.0 and cmds[7] == 0.0)
started = [i for i, c in enumerate(cmds) if c != 0.0]
check(f"the card's case: the charge starts at cycle {started[0]}"
f" instead of never", bool(started))
# ⚠️ AND IT STOPS AT THE FROZEN INTEGRATOR, NOT AT THE RAIL. This is AC 4: the
# integrator moved while the output was blocked, and the release must not turn
# that divergence into windup. It cannot, because releasing the OUTPUT freeze
# does not release the INTEGRATOR freeze - so the command can only walk, one
# slew step per cycle, to a value the integrator stopped accumulating at.
check(f"the card's case: it settles at {prev:.0f} W, at the frozen integrator "
f"({i_w:.0f} W) and not the {TL.max_w:.0f} W rail",
prev == -1190.0 and abs(prev) <= abs(i_w) and abs(prev) < TL.max_w)
steps = [abs(cmds[i] - cmds[i - 1]) for i in range(1, len(cmds))]
check(f"the card's case: no cycle moves more than the slew limit "
f"(worst {max(steps):.0f} W of {slew_limit_w(TL):.0f})",
max(steps) <= slew_limit_w(TL))
# --- 6. AC 4, AS A PROPERTY RATHER THAN A TRAJECTORY -----------------------
# ⚠️ THE FIRST FORM OF THIS CHECK WAS WRONG AND THE SWEEP SAID SO, which is
# worth leaving in the file. It asserted `|target| <= |i_w|` on a released
# cycle, and the sweep produced prev_w -5000, i_w -3000, target -4600: the
# command was walking BACK from -5000 toward the integrator and had not
# arrived. It was moving the right way and the assertion still failed, because
# "never exceeds the integrator" is not what no-windup means here.
#
# What it means: a released cycle can only move the command TOWARD the
# integrator, by at most one slew step, and never past it. So the divergence
# 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.
step = float(T.step_w)
past, jumped = [], []
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):
d = compute(prev, grid, actual, TL, SETTLE_CYCLES, i0)
if d.reason != "freeze-released":
continue
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("...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)
prev, i_w, sat, reasons = 0.0, 0.0, 0, set()
for _ in range(20):
d = compute(prev, -2000.0, 700.0, TN, sat, i_w)
reasons.add(d.reason)
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)
print("SAFETY-04: the i_w=None path is still release/1.0, exactly")
@@ -394,8 +601,19 @@ def legacy(prev, grid, actual, t, sat_count):
# "i-clamped", because the truncation happens on the integrator before the
# command is derived from it. Aliased here rather than papered over - if any
# OTHER reason ever diverges, this check goes red.
# ⚠️ SAFETY-13 IS A DELIBERATE DIVERGENCE FROM `legacy()`, AND THE SWEEP NOW
# GRADES THE DIVERGENCE INSTEAD OF FORBIDDING IT. `legacy()` above stays a
# transcription of release/1.0 - it is not edited to agree, for the reason the
# note on `slew_w` gives: an oracle taught the new rule compares the new law
# against itself. What changed is the assertion. Every case must either be
# IDENTICAL to release/1.0, or be a case where release/1.0 said
# "saturated-freeze" and this law says "freeze-released" with the two conditions
# 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"}
diffs = []
released = []
value_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
@@ -414,11 +632,35 @@ for tune in (Tuning(slew_w=1000.0), Tuning(slew_w=1000.0, target_grid_w=-10.0),
seen.add(d.reason)
got = (d.target_w, d.sat_count, d.frozen,
ALIAS.get(d.reason, d.reason))
if got != legacy(prev, grid, actual, tune, sc):
diffs.append((prev, grid, actual, sc, got,
legacy(prev, grid, actual, tune, sc)))
check(f"i_w=None reproduces release/1.0 over {3*7*9*4*4} cases, reason included"
+ (f" (first diff {diffs[0]})" if diffs else ""), not diffs)
was = legacy(prev, grid, actual, tune, sc)
if got == was:
continue
explained = (
d.reason == "freeze-released"
and was[3] == "saturated-freeze"
and d.sat_count >= SETTLE_CYCLES
and unasked_power(prev, actual, tune.saturation_w))
if not explained:
diffs.append((prev, grid, actual, sc, got, was))
continue
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
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)
# ⚠️ 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
# start from exactly 0 W, which is the ticket, stated as a count.
check(f"{len(value_diffs)} of those {len(released)} change the command,"
f" and every one is a charge start from prev_w == 0 that was refused",
len(value_diffs) == 27
and all(p == 0.0 and new_ < 0.0 and old_ == 0.0
for p, new_, old_ in value_diffs))
# ...and the rename is not a quiet deletion: the signal SAFETY-03 alarms on has
# to actually occur in that sweep, or its hook is dead.