diff --git a/goodwe_controller/CHANGELOG.md b/goodwe_controller/CHANGELOG.md index 628c811..dfba0ff 100644 --- a/goodwe_controller/CHANGELOG.md +++ b/goodwe_controller/CHANGELOG.md @@ -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 cover it restated the assertion three lines above it and never touched the payload. -- **A forward hazard written down where it will be read.** `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; a - peak-shaving strategy at `P_PEAK` **does**, and would blind the watchdog for - every peak event. Noted at the gate itself, with what has to change. +- **A forward hazard written down where it will be read, and made to bite.** + `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; a peak-shaving strategy at `P_PEAK` **does**, and would blind the + 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 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 @@ -44,6 +56,11 @@ Also in this release, all of it review follow-up rather than new behaviour: of the predicate it grades. - `held_s` takes the clock instead of reading one, restoring the pure-function 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 % / 4127 of 16349), per-cluster 0.3 / 0.9 / 10.5 / 0.0 %. diff --git a/goodwe_controller/app/main.py b/goodwe_controller/app/main.py index 825b527..a44eb43 100644 --- a/goodwe_controller/app/main.py +++ b/goodwe_controller/app/main.py @@ -41,7 +41,7 @@ from .maintenance import IDLE, MaintConfig, Maintenance from .mqtt import MqttPublisher from .p1 import P1Ingest, build_source, is_enabled from .validate import ConfigRefused, refuse, validate_startup_config -from .watchdog import SignWatchdog, SignWatchdogConfig +from .watchdog import SignWatchdog, SignWatchdogConfig, loop_is_following from . import web OPTIONS_PATH = "/data/options.json" @@ -378,43 +378,17 @@ class Controller: # --- SAFETY-02's arming gate ------------------------------------------ # 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? - # Only the former is expected to agree in sign with P1. See gate 1 in - # watchdog.py - without this, every maintenance grid charge trips the - # failsafe within three minutes of starting. + # Only the former is expected to agree in sign with P1 - without this, + # every maintenance grid charge trips the failsafe within three minutes. # - # ⚠️ "THE LOOP WON" IS NOT ENOUGH, 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 with `maintenance_charge_w: 1500` 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, - # not on the name: the loop is following only while the emitted value - # 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)) + # ⚠️ THE EXPRESSION LIVES IN watchdog.py, NOT HERE, and that is not + # tidiness. It was inline, test_watchdog.py held a transcription of it, + # and the P_PEAK case meant to force whoever lands peak shaving to come + # and change an expectation did not: editing this line alone to + # `winner in ("loop", "peak")` left every suite green while the watchdog + # went blind for every peak event. Read loop_is_following() before + # touching the gate - the forward hazard and the reasoning are there. + self.following = loop_is_following(resolution, self.loop_w) self.target = resolution.target_w self.reason = resolution.explain() await self.write_setpoint(self.target) diff --git a/goodwe_controller/app/watchdog.py b/goodwe_controller/app/watchdog.py index f0162f4..afaf2a4 100644 --- a/goodwe_controller/app/watchdog.py +++ b/goodwe_controller/app/watchdog.py @@ -221,6 +221,54 @@ def disagrees(commanded_w, grid_w, following: bool, 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: """One instance per actuator, evaluated once per control cycle. diff --git a/goodwe_controller/test_watchdog.py b/goodwe_controller/test_watchdog.py index 3f92c87..5cb701a 100644 --- a/goodwe_controller/test_watchdog.py +++ b/goodwe_controller/test_watchdog.py @@ -13,7 +13,9 @@ table-driven half: boundaries, timers, the latch, and the arming gate. import sys from datetime import datetime, timedelta, timezone -from app.watchdog import SignWatchdog, SignWatchdogConfig +from app.watchdog import ( + SignWatchdog, SignWatchdogConfig, loop_is_following, +) fails = [] 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): - """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) - return r, (r.winner == "loop" and asked is not None - and r.target_w * asked > 0 - and abs(r.target_w) <= abs(asked)) + return r, loop_is_following(r, asked) MAXW = Claim.limit("supervised", P_SAFETY, -2000, 2000, "max_w") @@ -211,10 +220,21 @@ TABLE = [ ("the loop asked for zero", [Claim.set("loop", P_LOOP, 0.0), MAXW], 0.0, False), # 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. - ("peak shaving at P_PEAK disarms the gate (see main.py's forward hazard)", + # be. When peak shaving lands, these expectations are what have to change. + ("peak shaving at P_PEAK disarms the gate (loop_is_following's forward hazard)", [Claim.set("loop", P_LOOP, 900), 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: 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", 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() if fails: print(f"{len(fails)} FAILED: {', '.join(fails)}")