SAFETY-02: the P_PEAK assertion was pinning the test's copy of the gate
Review finding 2, and it is the same duplication `disagrees()` just removed, so
it gets the same fix rather than a follow-up card.
`following_from()` in test_watchdog.py was a TRANSCRIPTION of the gate in
main.py, carrying "keep the two in step" as an instruction - which is exactly the
arrangement that does not keep two things in step. Measured: editing the shipped
gate alone to `winner in ("loop", "peak")` left every suite green while the
watchdog went blind for the duration of every peak event. The row whose whole job
is to force whoever lands peak shaving to come and change an expectation did not
do that.
The expression is now `watchdog.loop_is_following()`, called by main.py and by
the test. One definition, two callers, same reasoning as `disagrees()`: the copy
that drifts is always the one in the harness doing the grading.
⚠️ AND EXTRACTING IT WAS NOT SUFFICIENT - the drift proof still came out green
after the extraction, which is why it was worth running rather than assuming. The
realistic P_PEAK row has peak shaving asking for MORE than the loop, so the
magnitude term rejects it whatever `winner` says and masks the term under test. A
second row with peak asking for LESS makes `winner` the only deciding term. With
that row, widening the shipped gate fails two checks; without it, none.
Also enforcing the write ordering that was documented and not asserted: swapping
the two `store.set` calls passed everything. A store that fails the second write
now proves the property the ordering exists for - a crash mid-trip leaves a
reason with no latch, never a latch with no explanation. Swapping them now turns
that check red.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Du77usMj8XNKNFZGmUiWDa
This commit is contained in:
co-authored by
Claude Opus 5
parent
cc4e88490b
commit
e40eb0768d
@@ -29,11 +29,23 @@ Also in this release, all of it review follow-up rather than new behaviour:
|
|||||||
- **The MQTT `status: "failsafe"` value is tested.** The check that claimed to
|
- **The MQTT `status: "failsafe"` value is tested.** The check that claimed to
|
||||||
cover it restated the assertion three lines above it and never touched the
|
cover it restated the assertion three lines above it and never touched the
|
||||||
payload.
|
payload.
|
||||||
- **A forward hazard written down where it will be read.** `winner == "loop"`
|
- **A forward hazard written down where it will be read, and made to bite.**
|
||||||
disarms the watchdog under any higher-priority SET claim. Today only
|
`winner == "loop"` disarms the watchdog under any higher-priority SET claim.
|
||||||
maintenance and the safety stops emit one and neither follows the meter; a
|
Today only maintenance and the safety stops emit one and neither follows the
|
||||||
peak-shaving strategy at `P_PEAK` **does**, and would blind the watchdog for
|
meter; a peak-shaving strategy at `P_PEAK` **does**, and would blind the
|
||||||
every peak event. Noted at the gate itself, with what has to change.
|
watchdog for every peak event.
|
||||||
|
|
||||||
|
The gate is now `watchdog.loop_is_following()`, called by both `main.py` and
|
||||||
|
the test, for the same reason `disagrees()` was extracted: the test held a
|
||||||
|
*transcription* of the shipped expression, so editing the shipped gate alone to
|
||||||
|
`winner in ("loop", "peak")` left every suite green while the watchdog went
|
||||||
|
blind. Two copies, and the one that drifts is the one doing the grading.
|
||||||
|
|
||||||
|
⚠️ Extracting it was not sufficient on its own. The realistic P_PEAK row —
|
||||||
|
peak shaving asking for *more* than the loop — still could not detect the
|
||||||
|
widened gate, because the magnitude term rejects it regardless and masks the
|
||||||
|
winner term. A second row with peak asking for *less* isolates `winner` as the
|
||||||
|
only deciding term, and that is the one that turns red.
|
||||||
- **The worked example described a configuration that does not ship.** At the
|
- **The worked example described a configuration that does not ship.** At the
|
||||||
defaults `maintenance_charge_w` (2500) exceeds `max_w` (2000), so that claim is
|
defaults `maintenance_charge_w` (2500) exceeds `max_w` (2000), so that claim is
|
||||||
an arbiter *contradiction* resolving to 0 W, not a −2500 W charge. The example
|
an arbiter *contradiction* resolving to 0 W, not a −2500 W charge. The example
|
||||||
@@ -44,6 +56,11 @@ Also in this release, all of it review follow-up rather than new behaviour:
|
|||||||
of the predicate it grades.
|
of the predicate it grades.
|
||||||
- `held_s` takes the clock instead of reading one, restoring the pure-function
|
- `held_s` takes the clock instead of reading one, restoring the pure-function
|
||||||
property the module advertises.
|
property the module advertises.
|
||||||
|
- **The `sign_reason`-before-`sign_tripped` write ordering is enforced, not just
|
||||||
|
documented.** Swapping the two lines used to pass every check. A store that
|
||||||
|
fails the second write now proves the property the ordering exists for: what
|
||||||
|
survives a crash mid-trip is a reason with no latch, never a latch with no
|
||||||
|
explanation.
|
||||||
- Measured figures corrected throughout: 93.4 % / 4212 of 17280 (was 92.9 % /
|
- Measured figures corrected throughout: 93.4 % / 4212 of 17280 (was 92.9 % /
|
||||||
4127 of 16349), per-cluster 0.3 / 0.9 / 10.5 / 0.0 %.
|
4127 of 16349), per-cluster 0.3 / 0.9 / 10.5 / 0.0 %.
|
||||||
|
|
||||||
|
|||||||
@@ -41,7 +41,7 @@ from .maintenance import IDLE, MaintConfig, Maintenance
|
|||||||
from .mqtt import MqttPublisher
|
from .mqtt import MqttPublisher
|
||||||
from .p1 import P1Ingest, build_source, is_enabled
|
from .p1 import P1Ingest, build_source, is_enabled
|
||||||
from .validate import ConfigRefused, refuse, validate_startup_config
|
from .validate import ConfigRefused, refuse, validate_startup_config
|
||||||
from .watchdog import SignWatchdog, SignWatchdogConfig
|
from .watchdog import SignWatchdog, SignWatchdogConfig, loop_is_following
|
||||||
from . import web
|
from . import web
|
||||||
|
|
||||||
OPTIONS_PATH = "/data/options.json"
|
OPTIONS_PATH = "/data/options.json"
|
||||||
@@ -378,43 +378,17 @@ class Controller:
|
|||||||
# --- SAFETY-02's arming gate ------------------------------------------
|
# --- SAFETY-02's arming gate ------------------------------------------
|
||||||
# Was the number about to go on the wire chosen by the grid-following
|
# Was the number about to go on the wire chosen by the grid-following
|
||||||
# loop, or by a strategy that commands against the meter on purpose?
|
# loop, or by a strategy that commands against the meter on purpose?
|
||||||
# Only the former is expected to agree in sign with P1. See gate 1 in
|
# Only the former is expected to agree in sign with P1 - without this,
|
||||||
# watchdog.py - without this, every maintenance grid charge trips the
|
# every maintenance grid charge trips the failsafe within three minutes.
|
||||||
# failsafe within three minutes of starting.
|
|
||||||
#
|
#
|
||||||
# ⚠️ "THE LOOP WON" IS NOT ENOUGH, and the difference is a whole class of
|
# ⚠️ THE EXPRESSION LIVES IN watchdog.py, NOT HERE, and that is not
|
||||||
# false trip. A LIMIT claim can survive the loop winning and still
|
# tidiness. It was inline, test_watchdog.py held a transcription of it,
|
||||||
# replace its number: maintenance's cheap-window shaping is
|
# and the P_PEAK case meant to force whoever lands peak shaving to come
|
||||||
# `hi = -maintenance_charge_w`, so with `maintenance_charge_w: 1500` the
|
# and change an expectation did not: editing this line alone to
|
||||||
# loop can ask for +500 W of discharge, win the arbitration, and have the
|
# `winner in ("loop", "peak")` left every suite green while the watchdog
|
||||||
# emitted value come out at -1500 W of grid charge. Winner says "loop";
|
# went blind for every peak event. Read loop_is_following() before
|
||||||
# the wire carries maintenance's intent. So the test is on the NUMBER,
|
# touching the gate - the forward hazard and the reasoning are there.
|
||||||
# not on the name: the loop is following only while the emitted value
|
self.following = loop_is_following(resolution, self.loop_w)
|
||||||
# points the way the loop asked and is no larger than it asked - i.e.
|
|
||||||
# limits reduced it, they did not redirect it. Zero on either side falls
|
|
||||||
# out as not-following, which costs nothing: a 0 W command cannot be a
|
|
||||||
# wrong-direction command. The `abs(...) <= abs(asked)` half is
|
|
||||||
# load-bearing on its own: a `lo` limit can raise the magnitude without
|
|
||||||
# flipping the sign, and that is not the loop following either.
|
|
||||||
#
|
|
||||||
# (1500 W because at the SHIPPED defaults - maintenance_charge_w 2500 vs
|
|
||||||
# max_w 2000 - that claim is `lo=-2000 > hi=-2500`, which the arbiter
|
|
||||||
# calls a contradiction and resolves to 0 W. Filed separately; the
|
|
||||||
# redirect hazard here is real at any charge rate inside max_w.)
|
|
||||||
#
|
|
||||||
# ⚠️ FORWARD HAZARD, AND IT IS NOT HYPOTHETICAL - the claim block above
|
|
||||||
# already anticipates it. `winner == "loop"` disarms this watchdog under
|
|
||||||
# ANY higher-priority SET claim. Today only maintenance and the safety
|
|
||||||
# stops emit one, and neither is grid-following, so the gate costs
|
|
||||||
# nothing. A peak-shaving strategy claiming SET at P_PEAK **is**
|
|
||||||
# grid-following in sign, and the moment it lands this watchdog goes
|
|
||||||
# blind for the duration of every peak event. Whoever adds it must widen
|
|
||||||
# the gate to "the winning strategy follows the meter" rather than
|
|
||||||
# "the winner is the loop", not just add another name to a comparison.
|
|
||||||
asked = self.loop_w
|
|
||||||
self.following = (resolution.winner == "loop" and asked is not None
|
|
||||||
and resolution.target_w * asked > 0
|
|
||||||
and abs(resolution.target_w) <= abs(asked))
|
|
||||||
self.target = resolution.target_w
|
self.target = resolution.target_w
|
||||||
self.reason = resolution.explain()
|
self.reason = resolution.explain()
|
||||||
await self.write_setpoint(self.target)
|
await self.write_setpoint(self.target)
|
||||||
|
|||||||
@@ -221,6 +221,54 @@ def disagrees(commanded_w, grid_w, following: bool,
|
|||||||
and abs(grid_w) > cfg.min_w)
|
and abs(grid_w) > cfg.min_w)
|
||||||
|
|
||||||
|
|
||||||
|
def loop_is_following(resolution, loop_asked) -> bool:
|
||||||
|
"""Did the grid-following loop actually choose the number going on the wire?
|
||||||
|
|
||||||
|
Gate 1 of the predicate above, and it lives here rather than inline in
|
||||||
|
`cycle()` for the reason `disagrees()` does: the test suite has to be able to
|
||||||
|
assert on THE SHIPPED EXPRESSION, not on a transcription of it that drifts
|
||||||
|
apart from it in silence.
|
||||||
|
|
||||||
|
⚠️ IT WAS A TRANSCRIPTION, AND THAT WAS MEASURED, NOT FEARED. The P_PEAK case
|
||||||
|
in test_watchdog.py exists to make whoever lands peak shaving come here and
|
||||||
|
change an expectation. With the expression copied into the test it did not do
|
||||||
|
that: editing the shipped gate alone to `winner in ("loop", "peak")` left every
|
||||||
|
suite green while the watchdog went blind for the whole of every peak event.
|
||||||
|
One definition, two callers, and that test now bites.
|
||||||
|
|
||||||
|
`resolution` the arbiter's Resolution. Duck-typed on `.winner` and
|
||||||
|
`.target_w` so this module still imports nothing from arbiter.
|
||||||
|
`loop_asked` what the grid-following loop claimed this cycle, or None if it
|
||||||
|
did not claim at all.
|
||||||
|
|
||||||
|
"The loop won" is NOT the question, and the difference is a whole class of
|
||||||
|
false trip. A LIMIT claim can survive the loop winning and still replace its
|
||||||
|
number: maintenance's cheap-window shaping is `hi = -maintenance_charge_w`, so
|
||||||
|
at 1500 W the loop can ask for +500 W of discharge, win the arbitration, and
|
||||||
|
have the emitted value come out at -1500 W of grid charge. Winner says "loop";
|
||||||
|
the wire carries maintenance's intent.
|
||||||
|
|
||||||
|
So the test is on the NUMBER: the loop is following only while the emitted
|
||||||
|
value points the way the loop asked AND is no larger than it asked - limits
|
||||||
|
reduced it, they did not redirect it. The magnitude half is load-bearing on
|
||||||
|
its own, because a `lo` limit can raise magnitude without flipping sign, and
|
||||||
|
that is not the loop following either. Zero on either side falls out as
|
||||||
|
not-following, which costs nothing: a 0 W command cannot be a
|
||||||
|
wrong-direction command.
|
||||||
|
|
||||||
|
⚠️ FORWARD HAZARD, and the claim block in cycle() already anticipates it.
|
||||||
|
`winner == "loop"` disarms the watchdog under ANY higher-priority SET claim.
|
||||||
|
Today only maintenance and the safety stops emit one and neither follows the
|
||||||
|
meter, so the gate costs nothing. A peak-shaving strategy claiming SET at
|
||||||
|
P_PEAK **is** grid-following in sign, and the moment it lands this goes blind
|
||||||
|
for the duration of every peak event. Widening it means asking "does the
|
||||||
|
winning strategy follow the meter", not adding another name to a comparison.
|
||||||
|
"""
|
||||||
|
return (resolution.winner == "loop" and loop_asked is not None
|
||||||
|
and resolution.target_w * loop_asked > 0
|
||||||
|
and abs(resolution.target_w) <= abs(loop_asked))
|
||||||
|
|
||||||
|
|
||||||
class SignWatchdog:
|
class SignWatchdog:
|
||||||
"""One instance per actuator, evaluated once per control cycle.
|
"""One instance per actuator, evaluated once per control cycle.
|
||||||
|
|
||||||
|
|||||||
@@ -13,7 +13,9 @@ table-driven half: boundaries, timers, the latch, and the arming gate.
|
|||||||
import sys
|
import sys
|
||||||
from datetime import datetime, timedelta, timezone
|
from datetime import datetime, timedelta, timezone
|
||||||
|
|
||||||
from app.watchdog import SignWatchdog, SignWatchdogConfig
|
from app.watchdog import (
|
||||||
|
SignWatchdog, SignWatchdogConfig, loop_is_following,
|
||||||
|
)
|
||||||
|
|
||||||
fails = []
|
fails = []
|
||||||
T0 = datetime(2026, 8, 20, 15, 0, 0, tzinfo=timezone.utc)
|
T0 = datetime(2026, 8, 20, 15, 0, 0, tzinfo=timezone.utc)
|
||||||
@@ -164,11 +166,18 @@ from app.arbiter import ( # noqa: E402
|
|||||||
|
|
||||||
|
|
||||||
def following_from(claims, asked):
|
def following_from(claims, asked):
|
||||||
"""Exactly main.py's expression. Keep the two in step."""
|
"""THE SHIPPED gate, not a copy of it.
|
||||||
|
|
||||||
|
⚠️ This used to transcribe main.py's expression with a comment saying
|
||||||
|
"keep the two in step", which is exactly the arrangement that does not keep
|
||||||
|
two things in step. Measured: editing the shipped gate alone to
|
||||||
|
`winner in ("loop", "peak")` left this suite - including the P_PEAK row below,
|
||||||
|
whose entire job is to catch that edit - completely green, while the watchdog
|
||||||
|
went blind for the duration of every peak event. Import it or the P_PEAK
|
||||||
|
assertion is decoration.
|
||||||
|
"""
|
||||||
r = resolve(claims)
|
r = resolve(claims)
|
||||||
return r, (r.winner == "loop" and asked is not None
|
return r, loop_is_following(r, asked)
|
||||||
and r.target_w * asked > 0
|
|
||||||
and abs(r.target_w) <= abs(asked))
|
|
||||||
|
|
||||||
|
|
||||||
MAXW = Claim.limit("supervised", P_SAFETY, -2000, 2000, "max_w")
|
MAXW = Claim.limit("supervised", P_SAFETY, -2000, 2000, "max_w")
|
||||||
@@ -211,10 +220,21 @@ TABLE = [
|
|||||||
("the loop asked for zero",
|
("the loop asked for zero",
|
||||||
[Claim.set("loop", P_LOOP, 0.0), MAXW], 0.0, False),
|
[Claim.set("loop", P_LOOP, 0.0), MAXW], 0.0, False),
|
||||||
# The forward hazard, asserted as it stands TODAY rather than as it should
|
# The forward hazard, asserted as it stands TODAY rather than as it should
|
||||||
# be. When peak shaving lands, this expectation is what has to change.
|
# be. When peak shaving lands, these expectations are what have to change.
|
||||||
("peak shaving at P_PEAK disarms the gate (see main.py's forward hazard)",
|
("peak shaving at P_PEAK disarms the gate (loop_is_following's forward hazard)",
|
||||||
[Claim.set("loop", P_LOOP, 900),
|
[Claim.set("loop", P_LOOP, 900),
|
||||||
Claim.set("peak", P_PEAK, 1800, "shaving"), MAXW], 900, False),
|
Claim.set("peak", P_PEAK, 1800, "shaving"), MAXW], 900, False),
|
||||||
|
# ⚠️ AND THE ROW ABOVE CANNOT DETECT A WIDENED GATE ON ITS OWN, which was
|
||||||
|
# found by trying it: with the shipped gate edited to
|
||||||
|
# `winner in ("loop", "peak")` that case STILL comes out False, because peak
|
||||||
|
# shaving asked for MORE than the loop and the magnitude term rejects it
|
||||||
|
# anyway. The winner term is masked. This row isolates it - a peak claim
|
||||||
|
# smaller than the loop's ask and pointing the same way, so `winner` is the
|
||||||
|
# only term that can decide - and it is what actually turns red if the gate
|
||||||
|
# is widened without anyone revisiting the hazard.
|
||||||
|
("...and with peak BELOW the loop's ask, only the winner term separates them",
|
||||||
|
[Claim.set("loop", P_LOOP, 1800),
|
||||||
|
Claim.set("peak", P_PEAK, 900, "shaving"), MAXW], 1800, False),
|
||||||
]
|
]
|
||||||
for name, claims, asked, expect in TABLE:
|
for name, claims, asked, expect in TABLE:
|
||||||
r, got = following_from(claims, asked)
|
r, got = following_from(claims, asked)
|
||||||
@@ -414,6 +434,55 @@ fresh = Controller({"setpoint_entity": "number.sp", "meter_source": "off"},
|
|||||||
check("...so the next restart comes back armed and untripped, as it should",
|
check("...so the next restart comes back armed and untripped, as it should",
|
||||||
not fresh.sign_wd.tripped)
|
not fresh.sign_wd.tripped)
|
||||||
|
|
||||||
|
# ⚠️ THE WRITE ORDERING IS AN INVARIANT, SO IT GETS AN ASSERTION. main.py writes
|
||||||
|
# `sign_reason` and THEN `sign_tripped`, each one its own `save()`, so that a
|
||||||
|
# process that dies between the two leaves a reason nothing reads - harmless -
|
||||||
|
# rather than a latch with no explanation for the operator who has to decide
|
||||||
|
# whether to clear it. Documented reasoning is not enforcement: swapping those two
|
||||||
|
# lines used to pass every check in this file.
|
||||||
|
#
|
||||||
|
# The death is modelled as the second write raising. In the field it is a power
|
||||||
|
# cut or a container kill (Store.save() swallows OSError rather than raising), so
|
||||||
|
# what is asserted here is the PROPERTY - what survives on disk - not the
|
||||||
|
# mechanism.
|
||||||
|
|
||||||
|
|
||||||
|
class _CrashOnFlag(_MemStore):
|
||||||
|
def set(self, k, v):
|
||||||
|
if k == "sign_tripped" and v:
|
||||||
|
raise RuntimeError("power cut, mid-trip")
|
||||||
|
super().set(k, v)
|
||||||
|
|
||||||
|
|
||||||
|
async def _crash_mid_write():
|
||||||
|
store = _CrashOnFlag()
|
||||||
|
hass = _Hass()
|
||||||
|
opts = {"setpoint_entity": "number.sp", "meter_entity": "sensor.grid",
|
||||||
|
"soc_entity": "sensor.soc", "batt_entity": "sensor.batt",
|
||||||
|
"meter_source": "off", "max_w": 2000, "gain": -0.6,
|
||||||
|
"sign_disagree_w": 300, "sign_disagree_s": 1, "auto_start": True}
|
||||||
|
c = Controller(opts, hass, store, _P(), stop=asyncio.Event())
|
||||||
|
c.auto = True
|
||||||
|
c.dev_min, c.dev_max = -5000.0, 5000.0
|
||||||
|
died = False
|
||||||
|
for _ in range(12):
|
||||||
|
try:
|
||||||
|
await c.read_inputs()
|
||||||
|
await c.cycle()
|
||||||
|
except RuntimeError:
|
||||||
|
died = True
|
||||||
|
break
|
||||||
|
await asyncio.sleep(0.25)
|
||||||
|
return store, died
|
||||||
|
|
||||||
|
|
||||||
|
crashed_store, died = asyncio.run(_crash_mid_write())
|
||||||
|
check("the second write is the one that sets the flag", died)
|
||||||
|
check("a crash between the two writes leaves the REASON on disk",
|
||||||
|
"SIGN_DISAGREEMENT" in crashed_store.data.get("sign_reason", ""))
|
||||||
|
check("...and never a latch with nothing to explain it",
|
||||||
|
not crashed_store.data.get("sign_tripped"))
|
||||||
|
|
||||||
print()
|
print()
|
||||||
if fails:
|
if fails:
|
||||||
print(f"{len(fails)} FAILED: {', '.join(fails)}")
|
print(f"{len(fails)} FAILED: {', '.join(fails)}")
|
||||||
|
|||||||
Reference in New Issue
Block a user