ARB-03: restore Claim.actuator and make resolve() three-stage
checks / unit (pull_request) Successful in 3m45s

specs.md:467 declares `actuator: str` as the FIRST field of `Claim`.
app/arbiter.py:55 had no such field. The specification designed
per-actuator claims and the implementation dropped it, so every claim was
implicitly about "the one and only actuator", resolve() returned one scalar
Resolution.target_w, and main.py assigned it to one self.target. THERE WAS
NO SEAM AN ALLOCATOR COULD OCCUPY - and ARCH-01 (specs.md §6.2, 2026-09-02)
decided the site grid target is ALLOCATED across several inverters and never
broadcast. This is a regression fix against the written design; creating that
seam is the whole of the change.

WHY IT MATTERS, IN THE UNITS THE SYSTEM IS BILLED IN. The control primitive
is meter emulation: the master reports a fabricated grid reading and the
inverter regulates itself to it, so one number means "the battery moves X W"
to the add-on and "the grid is at X W" to the inverter - an identity that
holds only at N=1. Broadcast one target to two inverters and each supplies it
in full; the loop gain at the meter becomes N times the per-unit gain, which
at the gain config.yaml:374 accepts is a permanent limit cycle with every
watchdog in §11.2 reporting healthy. And a per-inverter reserve filed as a
site `hi` against the peak guard's site `lo` is `lo > hi`, arbiter clause 3,
0 W IN THE BILLED QUARTER - the parked battery SAFETY-25's memo calls fatal.

THE SPLIT, VERIFIED AT EACH CONSTRUCTION SITE RATHER THAN ACCEPTED FROM THE
SURVEY. Four sources are about the GRID CONNECTION and are SITE claims:
`loop` (compute() regulates grid_w, the P1 measurement, and §6.2's whole
architecture is one integrator on P1 whose output is then split), `peak` (the
15-minute average offtake AT the grid connection, which is what the capacity
tariff bills - one quarter-hour peak per site, not one per pack),
`arbitrage` (buys and sells at the grid against a day-ahead price; the price
is a property of the connection and the energy crosses the meter) and
`safety` (both construction sites read: "stopped" is the operator switching
control off for the site, "inputs missing" is the site's own meter gone -
neither is about a pack, and both must stop every inverter).

Four are about a pack, a device or one write and are PER-INVERTER: `device`
(one inverter's own reported min/max - there is no site rating),
`supervised` (max_w caps what may be WRITTEN to one setpoint entity, §11.3,
so it is scoped like `device` for the same reason), `maintenance` (§12's
recalibration is a pack procedure - drain THIS pack, charge THIS pack,
recalibrate THIS pack's counter) and `failsafe`. `failsafe` is the entry that
needed the reading rather than the survey: SAFETY-02's EVIDENCE is site-wide
(it compares P1 against the standing command) but its CONCLUSION is
"the unit I am driving is pushing power the wrong way" and its remedy is to
park that unit. At N>=2 the same evidence cannot be attributed to a sibling
this controller never commanded, so a site-wide stop would park an inverter
this watchdog never graded. The reasoning for all eight is recorded AT THE
LINE, in arbiter.CLAIM_SCOPE and again at each claims.append in main.py.

WHAT WAS BUILT. resolve() is three stages, each a separate function so a test
can construct a case at any one of them:

  pre_resolve()  - one inverter's own claims -> that unit's interval. Clauses
                   1 and 2 transposed: the unit's own winning SET gates its
                   own limits. The SET's value travels BESIDE the interval,
                   not inside it - folding a -2500 W drain into
                   [-2500, -2500] would turn "clamped to max_w" into
                   "contradicts max_w", a different and wrong answer.
  site_resolve() - THE SHIPPED ARBITER, UNCHANGED. Same code, new name.
  allocate()     - THE SEAM, AND DELIBERATELY NOT AN ALLOCATOR. ALLOC-01
                   builds it. At N<=1 it passes the target through (§6.2's
                   identity). At N>=2 it DECLINES - no shares,
                   allocated=False - and main.py refuses to write rather than
                   broadcast, because the obvious placeholder (hand the target
                   to each) is the fault ARCH-01 was filed about and no guard
                   we have can tell it apart from the real thing.

THE CONTRADICTION IS NOT GUARDED AGAINST, IT CANNOT BE WRITTEN DOWN. The
partition is by `actuator` and it is a partition: a unit's `hi` and the site's
`lo` are never both terms of one `lo > hi` test. Constructed and swept - 40
filings (every per-inverter source x unit x bound, including a unit
contradicting ITSELF at lo 900 > hi 100) against a live site floor, and not
one moves the site target or raises a contradiction. A unit's own impossible
pair parks that unit and says so on its own bounds; it does not park the site.
That is SAFETY-25 §0c's table made mechanical.

AT N=1 THIS IS A PURE REFACTOR, AND THAT IS PROVEN RATHER THAN ASSERTED. With
one inverter the fabricated grid reading and the battery setpoint are the same
number, so the grid connection and the only unit ARE one actuator:
actuator_for() routes every source to the site, no claim is filed on a unit,
stage 2 sees the whole list and answers what the shipped arbiter answered.
All 17 suites replay UNEDITED above the ARB-03 sections and are green on the
same numbers; test_arbiter.py additionally runs 13 claim lists through both
resolve() and site_resolve() and compares target, winner, binder,
contradiction flag, the considered list and the operator line.

EVIDENCE, BY BREAKING EACH THING (tools/mutation_run.sh, purged tree):
  * Claim's dataclass default emptied            -> RED (test_arbiter)
    ...and it survived until the check was added: the two helpers pass their
    own default down, so the FIELD's default never ran. Now checked directly.
  * `peak` reclassified SCOPE_UNIT               -> RED (arbiter x4, peakguard x2)
  * `maintenance` reclassified SCOPE_SITE        -> RED (arbiter x4, peakguard)
  * the N=1 identity dropped in actuator_for()   -> RED (arbiter, peakguard
    incl. the maintenance/peak suppression checks, freeze) - which is the
    measurement that says splitting at N=1 would be a behaviour change
  * resolve() stops partitioning                 -> RED (arbiter x4)
  * allocate() broadcasts at N>=2                -> RED (arbiter x2)
  * stage 1 drops clause-2 gating                -> RED (arbiter)
  * a call site routes `device` through `loop`   -> RED (peakguard 10g)
  * SAFETY-25 Option B built as a ninth source   -> RED (peakguard 10f, both
    halves, plus 10g) - the tripwire still bites

SAFETY-24's asymmetry proof is re-run and holds: 0 negative floors over the
shipped sweep, `hi` still +inf on every claim the guard files, and it now also
asserts every one of them is on the SITE actuator - a floor bound to one
inverter's share would leave the site, the thing the capacity tariff meters,
with no floor at all.

test_peakguard.py part 10f is kept, not adapted around. `source` is still
Claim.set()'s first positional argument precisely so its AST scan keeps
reading it, which is why `actuator` is the LAST field of Claim and not the
first - moving `source` off position 0 would silently blind the tripwire that
guards SAFETY-25's deferred option. The one adaptation is `**kw` on its spy,
so main.py's roster passes through unread rather than being silently dropped.
New part 10g pins CLAIM_SCOPE to the same eight-source set and grades a REAL
two-inverter cycle, which is the only place a mis-typed actuator_of(...) at a
call site is observable - at N=1 every source legitimately routes to the site,
so a swap there is invisible by construction.

No config key, no option, no operator surface, no default moved. Inverter B
does not exist yet and nothing here measures it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
This commit is contained in:
2026-09-02 01:54:29 +02:00
co-authored by Claude Opus 5
parent 0c7e786ed5
commit 06f95e0a64
7 changed files with 955 additions and 24 deletions
+122 -3
View File
@@ -115,7 +115,8 @@ from pathlib import Path
from app import peakguard
from app.arbiter import (
P_LOOP, P_MAINT_SHAPE, P_MAINTENANCE, P_PEAK, P_SAFETY, Claim, resolve,
ACTUATOR_SITE, CLAIM_SCOPE, P_LOOP, P_MAINT_SHAPE, P_MAINTENANCE, P_PEAK,
P_SAFETY, SCOPE_SITE, SCOPE_UNIT, Claim, resolve, scope_violations,
)
from app.control import Tuning, compute, peak_at_risk
from app.freeze import FreezeWatchdogConfig, looks_frozen, rail_w
@@ -1519,6 +1520,14 @@ check("...and its arbiter reason names the SoC floor rather than reusing "
# forbidden to cap. Swept rather than argued.
SWEEP_NEG = SWEEP_BOTH = SWEEP_N = 0
SWEEP_HI = True
# ⚠️ ARB-03 ADDS ONE DIMENSION TO THIS PROOF RATHER THAN RE-RUNNING IT UNCHANGED.
# `Claim` gained an `actuator`, and the asymmetry that makes this guard safe is
# now TWO facts, not one: `hi` is +inf on every claim it files, AND every claim
# it files is on the SITE actuator. A `lo` that landed on one inverter's interval
# would still have `hi = +inf` and would still never cap a discharge - and would
# leave the SITE, the thing the capacity tariff actually bills, with no floor at
# all. So the same combinations are swept for both.
SWEEP_SITE = True
for load in (0.0, CEIL - 500.0, CEIL, CEIL + 300.0, CEIL + 3000.0,
LIVE_MAX_W * 3):
for elapsed in (30.0, 450.0, 870.0):
@@ -1538,6 +1547,8 @@ for load in (0.0, CEIL - 500.0, CEIL, CEIL + 300.0, CEIL + 3000.0,
_c = peakguard.claim(_d)
if _c is not None and not (isinf(_c.hi) and _c.hi > 0):
SWEEP_HI = False
if _c is not None and _c.actuator != ACTUATOR_SITE:
SWEEP_SITE = False
print(f" swept {SWEEP_N} (load x elapsed x battery x SoC x floor) "
f"combinations, SoC included: {SWEEP_NEG} negative floors, "
f"{SWEEP_BOTH} decisions both floor-limited and saturated")
@@ -1548,6 +1559,12 @@ check(f"NOT ONE of the {SWEEP_N} combinations produces a negative floor. That "
SWEEP_NEG == 0 and SWEEP_N > 600)
check("...and `hi` stays +inf on every claim any of them files",
SWEEP_HI)
check("...and every one of them is filed on the SITE actuator, which is the "
"other half of the same asymmetry now that a claim has an actuator: the "
"billed quantity is the quarter's offtake AT THE GRID CONNECTION, so a "
"floor that bound one inverter's share would leave the site - the thing "
"the capacity tariff meters - with no floor at all",
SWEEP_SITE)
check("...and no combination is both floor-limited and saturated, so the two "
"notifications are exclusive on measured inputs and not merely by reading "
"the code", SWEEP_BOTH == 0)
@@ -2376,9 +2393,17 @@ def cycle_claims(run):
seen = []
real = app_main.resolve
def _spy(claims):
def _spy(claims, **kw):
# ⚠️ `**kw` PASSES THE ROSTER THROUGH UNREAD, AND THAT IS THE WHOLE
# ADAPTATION ARB-03 MADE HERE. main.py now calls
# `resolve(claims, units=self.units)`; a spy with a fixed signature would
# raise a TypeError on every real cycle, which is loud, but a spy that
# DROPPED the roster would be silently grading a different arbitration
# from the one main.py performs. What is observed - `claims`, the list
# itself - is unchanged, so the two halves below still see exactly what
# they saw before, and a ninth source still goes red.
seen.append(list(claims))
return real(claims)
return real(claims, **kw)
app_main.resolve = _spy
try:
@@ -2467,6 +2492,100 @@ check("...and replay_loop() folding main.py's TWO P_SAFETY rating limits into "
and near(LOOP_MAX_W, read_option("max_w")))
# --- 10g. ARB-03: AND THE ACTUATOR EACH OF THEM IS FILED ON -----------------
# ⚠️ THE SAME PIN, ONE DIMENSION WIDER, AND FOR THE SAME REASON. 10f pins WHICH
# sources main.py can file. ARB-03 gave every claim an `actuator`, and a claim
# routed to the wrong stage is a defect 10f cannot see: the source set is
# unchanged when the peak floor is misfiled onto one inverter, and the site is
# then left with no floor at all in the quarter that sets the month's bill.
#
# It is also what keeps SAFETY-25 §0c honest from the other side. That table
# says the deferred loop reserve becomes a PER-INVERTER `hi` at stage A while
# the peak floor stays a SITE `lo` at stage B, and calls the crossing
# structurally impossible. The structure is `CLAIM_SCOPE`, so `CLAIM_SCOPE` is
# pinned to the AST-scanned set rather than trusted to agree with it.
check("every source main.py can file is CLASSIFIED site or per-inverter, and "
"nothing else is. A ninth source now goes red twice - once here for "
"having no classification, once above for being a ninth - and it takes an "
"argument about what the claim is ABOUT to make either line green",
set(CLAIM_SCOPE) == CLAIM_SOURCES)
print(" site: " + ", ".join(sorted(s for s, v in CLAIM_SCOPE.items()
if v == SCOPE_SITE))
+ " | per-inverter: "
+ ", ".join(sorted(s for s, v in CLAIM_SCOPE.items() if v == SCOPE_UNIT)))
check("...and the split is the one ARB-03 argued: the four about the GRID "
"CONNECTION are site claims and the four about a pack, a device or one "
"write are per-inverter",
{s for s, v in CLAIM_SCOPE.items() if v == SCOPE_SITE}
== {"loop", "peak", "arbitrage", "safety"}
and {s for s, v in CLAIM_SCOPE.items() if v == SCOPE_UNIT}
== {"device", "supervised", "failsafe", "maintenance"})
# The shipped roster is ONE inverter, so §6.2's identity holds and every claim a
# real cycle files is a site claim. Observed on the claims main.py's own resolve
# was handed, not assumed from the routing table.
_real_acts = {(c.source, c.actuator) for c in _cl}
print(f" the real FLOOR-LIMITED cycle files: "
+ ", ".join(f"{s}@{a}" for s, a in sorted(_real_acts)))
check("at the SHIPPED one-inverter roster every claim a real cycle files is on "
"the SITE actuator, per-inverter sources included. That is §6.2's "
"identity - one inverter means the fabricated grid reading and the "
"battery setpoint are the same number, so there is one actuator and it is "
"both - and it is why ARB-03 is a pure refactor here",
all(a == ACTUATOR_SITE for _, a in _real_acts))
check("...and the arbiter agrees the routing is legal, on the list main.py "
"actually handed it", scope_violations(_cl) == [])
# And the day the roster grows, the SAME cycle must partition. Graded through
# main.py's own `actuator_of()` on a real Controller - the method every
# `claims.append` above routes through - rather than through a copy of it.
c_src.units = ("inverter-a", "inverter-b")
_routed = {s: c_src.actuator_of(s) for s in CLAIM_SOURCES}
c_src.units = (app_main.UNIT_A,)
print(" with a second inverter on the roster, main.py routes: "
+ ", ".join(f"{s}->{a}" for s, a in sorted(_routed.items())))
check("⚠️ AND THIS IS THE BREAKING HALF. Give the same Controller a second "
"inverter and its OWN routing method splits the eight: `device`, "
"`supervised`, `failsafe` and `maintenance` bind the unit this controller "
"drives, `loop`, `peak`, `arbitrage` and `safety` stay on the grid "
"connection. Swap any one of them - route `peak` to the unit and the site "
"keeps no floor; route `maintenance` to the site and it can cross that "
"floor into `lo > hi` - and this line goes red",
_routed == {"device": "inverter-a", "supervised": "inverter-a",
"failsafe": "inverter-a", "maintenance": "inverter-a",
"loop": ACTUATOR_SITE, "peak": ACTUATOR_SITE,
"arbitrage": ACTUATOR_SITE, "safety": ACTUATOR_SITE})
check("...and the roster it was restored to is the shipped one, so nothing "
"below inherits a two-inverter Controller",
c_src.units == (app_main.UNIT_A,) and len(c_src.units) == 1)
# ⚠️ AND THE ROUTING TABLE BEING RIGHT IS NOT THE SAME AS THE CALL SITES USING
# IT RIGHT. `actuator_of("maintenance")` written at the `device` append routes a
# rating limit to whatever `maintenance` routes to, and at the shipped
# one-inverter roster BOTH answers are the site, so nothing above can see it.
# The only place it becomes observable is a cycle at a roster of two - so take
# one, on real claims, spied at main.py's own resolve.
c_src.units = ("inverter-a", "inverter-b")
try:
_, _cl2 = cycle_claims(lambda: run_cycle(c_src))
finally:
c_src.units = (app_main.UNIT_A,)
print(" a REAL two-inverter cycle files: "
+ ", ".join(f"{c.source}@{c.actuator}" for c in _cl2))
check("a real cycle at a roster of TWO partitions its own claims correctly - "
"every claim main.py filed is on an actuator its source's scope permits. "
"This is the line a mis-typed `actuator_of(...)` at a call site goes red "
"on, and it is the only place one can be seen: at N=1 every source "
"legitimately routes to the site, so a swap there is invisible by "
"construction", len(_cl2) >= 3 and scope_violations(_cl2) == [])
check("...and the partition is the expected one on the sources this state "
"reaches: the two rating limits bind the unit, the loop claim stays on "
"the grid connection",
{c.source: c.actuator for c in _cl2}
== {"device": "inverter-a", "supervised": "inverter-a",
"loop": ACTUATOR_SITE})
# ==============================================================================
print()
print("11. mutation: what defeats these guards, and which check bites")