ALLOC-01: allocate the site grid target, sum-invariant, never broadcast
checks / unit (pull_request) Successful in 4m6s
checks / unit (pull_request) Successful in 4m6s
ARB-03 left `allocate()` as a documented seam that passed through at N<=1 and
DECLINED at N>=2, with the reasoning recorded at the line: the obvious
placeholder - hand the site target to each inverter - IS the ARCH-01 fault, and
"a placeholder that cannot be told apart from the real thing by any guard we
have is worse than no placeholder". This fills the seam.
WHY A BROADCAST IS A FAULT AND NOT AN INEFFICIENCY. 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 this
add-on and "the grid is at X W" to the inverter - an identity that holds only at
N=1. Hand two inverters the same target and each supplies it IN FULL, so the
loop gain at the meter becomes N times the per-unit gain. Reproduced on
admin/goodwe's two-master rig against this tree: -400 W export overshoot at
gain 0.6, and at gain 1.0 - which config.yaml accepts as its documented maximum
- a permanent 4000 W peak-to-peak limit cycle, commands alternating
1000/2000/1000/0 W, with NOT ONE GUARD FIRING. The sign watchdog is evaluated on
every cycle and never trips, because the disagreement flips on alternate ticks
and never holds its 180 s window.
WHAT WAS BUILT. `app/allocator.py`, host-side and strictly above the driver
seam. It consumes intervals and a number and nothing else - no claims, no
priorities, and no measurement, because an allocator that read P1 would be a
SECOND integrator on the site measurement.
* ENVELOPE CLAMP, from ARB-03 stage 1's `UnitBounds`, read PER TICK. `plan()`
is a pure function and the module holds no state, so there is nowhere for a
construction-time envelope to be cached.
* WATER-FILL by weight, with the surplus of a full unit moving to the others.
Weights express PREFERENCE, envelopes express PERMISSION: a zero weight is
honoured while another unit has headroom and overridden when it does not,
because the SUM is the safety property and stranding capacity behind a
comfort choice manufactures a standing error at the meter.
* LARGEST-REMAINDER ROUNDING. The target is rounded ONCE, at the top; every
sum below that line is integer arithmetic, so it cannot drift. Measured: a
per-unit round() drifts -125 W over 50 000 ticks at three inverters.
* THE ALLOCATION RECORD, with `unmet_w`, `dropped` and a per-unit reason.
`ok` is one boolean for SAFETY-28 to gate on, and `unmet_w` is deliberately
NOT fused into it - a saturated inverter must not park the whole site.
THE STABILITY PROPERTY IS STRUCTURAL. With sum(a_i) = 1 the gain at the meter is
sum(a_i * g_i), a convex combination of the per-unit gains, so it lies in
[min g_i, max g_i] FOR ANY SPLIT. That is what makes the weights a comfort
choice rather than a tuning parameter, and it is why a bad split cannot
destabilise the site. Graded directly, and measured end to end: 90/10, 50/50 and
100/0 give a bit-identical aggregate trace at the meter, and a gain sweep to 1.0
at every split has a flat tail at all 84 combinations.
THE TWO REFUSALS main.py NOW MAKES, AND WHY THERE ARE TWO. `allocated=False` no
longer means "no allocator"; it means no safe split EXISTS - a mis-routed claim,
an empty envelope set, or a split that could only be made by commanding one pack
to charge while another discharges. Separately, and this guard is the price of
making allocate() succeed rather than something inherited, main.py refuses to
act on a valid split it cannot DELIVER: there is one `setpoint_entity`, so
writing the site target to the one inverter it can reach would over-command that
inverter by exactly the other's share. Commanding a partial site is a worse
instruction than commanding nothing. DEV-02 gives it the second writer.
scope_violations() IS NOW CONSUMED, AND AS A REFUSAL. ARB-03 left it logging
without changing the resolution. A mis-routed claim means the number about to be
divided may itself be wrong, and dividing a number that may be wrong is worse
than not dividing it - the same answer clause 3 already gives a contradiction.
It is NOT promoted into an envelope: a unit-scoped claim that landed on the site
names no unit, so promoting it would mean guessing one, or applying one
inverter's rating to a sibling that does not have it.
AT N<=1 IT IS A PASS-THROUGH, BYTE-IDENTICAL: the share is the site target, as a
float, unrounded and unclamped. All 17 existing suites replay unedited.
test_peakguard.py part 10h and test_arbiter.py part 7 were RE-AIMED, not
deleted. PR #40's reviewer proved that refusal branch was unreachable and
untested once; removing its trigger without giving it a new one would have
rebuilt the hole. Part 10h now drives three real cycles - a deliverable split, a
dead sibling, and every master stale - and grades all three.
KNOWN AND NOT CLOSED HERE: at a roster of two the loop's `actual_w` is one
inverter's power used as a site measurement, because the add-on binds a single
`inverter_power` sensor. That is the SENSING half of the same N=1 identity this
card removes from the COMMANDING half, and it makes the aggregate trace
split-dependent below gain 1.0. Measured with its counterfactual in test_alloc.py
part 8 and tools/alloc_sim.py --splits. It belongs to DEV-02.
Verified: all 18 suites green in the CI image. 16 mutations run through
tools/mutation_run.sh on a purged tree; 13 red, and the 3 survivors are recorded
in test_alloc.py part 12 with the reason each cannot be caught.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
glenn schrooyen
co-authored by
Claude Opus 5
Claude Opus 5
parent
df88b323f5
commit
186e13ceca
@@ -0,0 +1,840 @@
|
||||
"""Runnable check for the site allocator. `python3 test_alloc.py`
|
||||
|
||||
ALLOC-01. The site grid target is ALLOCATED across N inverters and NEVER
|
||||
broadcast, because 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" here and "the grid is at X W" there - an identity
|
||||
that holds ONLY at N=1. Hand both inverters the same number and each supplies it
|
||||
IN FULL.
|
||||
|
||||
⚠️ WHAT THIS FILE CAN AND CANNOT CLAIM, SAID BEFORE THE FIRST CHECK.
|
||||
The two-master rig lives in admin/goodwe (TEST-19, `sim/sitesim.py`), where
|
||||
`compute()` closes the loop against `plantsim.Plant` with the firmware's own
|
||||
encoder on the wire. That repository is PRIVATE and this repository's CI token
|
||||
is minted for this one, so the rig is not reachable from the gate - and a test
|
||||
file that needed it would either fail the gate or, like test_freeze.py's hwsim
|
||||
section, pass SILENTLY having checked nothing.
|
||||
|
||||
So the split is deliberate:
|
||||
|
||||
* `tools/alloc_sim.py` drives the REAL rig, and its output is quoted in the
|
||||
pull request. It is where "no limit cycle" is a claim about the shipped
|
||||
control law against the modelled hardware.
|
||||
* THIS FILE grades the allocator's own arithmetic exhaustively - which needs
|
||||
no plant at all - and closes a loop around the REAL `compute()` against a
|
||||
plant IT MODELS AND SAYS IT MODELS (part 8). The modelled plant is the
|
||||
`lag_s=0` limit ARCH-01's evidence was computed in; it is not evidence about
|
||||
a GW5000S-BP.
|
||||
|
||||
⚠️ INVERTER B DOES NOT EXIST YET. Nothing here contains a measured parameter for
|
||||
it. Every two-unit case below is built from a rating passed IN, and the second
|
||||
unit's rating is either the first one's or an explicit hypothetical.
|
||||
|
||||
⚠️ MUTATING THE MODULE THIS FILE GRADES? PURGE `__pycache__` FIRST - or run
|
||||
`tools/mutation_run.sh`, which does. `python3 -B` alone does NOT save you.
|
||||
Read MUTATION.md before you report a survivor.
|
||||
"""
|
||||
|
||||
import random
|
||||
import sys
|
||||
from math import floor, inf
|
||||
|
||||
from app.allocator import (
|
||||
DROP_CONTRADICTION, DROP_NO_INTEGER, DROP_STALE, REFUSE_EMPTY,
|
||||
REFUSE_SCOPE, REFUSE_SIGN, Allocation, plan,
|
||||
)
|
||||
from app.arbiter import (
|
||||
ACTUATOR_SITE, P_ARBITRAGE, P_LOOP, P_MAINT_SHAPE, P_MAINTENANCE, P_PEAK,
|
||||
P_SAFETY, UnitBounds, Claim, allocate, resolve,
|
||||
)
|
||||
from app.control import Tuning, compute
|
||||
|
||||
fails = []
|
||||
|
||||
|
||||
def check(name, cond):
|
||||
print(f" {'ok ' if cond else 'FAIL'} {name}")
|
||||
if not cond:
|
||||
fails.append(name)
|
||||
|
||||
|
||||
def _raises_value(fn):
|
||||
"""True if `fn()` raises ValueError - a check that something is REFUSED."""
|
||||
try:
|
||||
fn()
|
||||
except ValueError:
|
||||
return True
|
||||
return False
|
||||
|
||||
|
||||
def B(lo=-inf, hi=inf, gate=None, pin=None, by=None, contra=False):
|
||||
"""One unit's interval, the way ARB-03 stage 1 hands it over."""
|
||||
return UnitBounds(lo=lo, hi=hi, gate=gate, pinned_w=pin, pinned_by=by,
|
||||
contradiction=contra)
|
||||
|
||||
|
||||
A, Bee = "inverter-a", "inverter-b"
|
||||
RATING = 5000.0 # GW5000S-BP, measured. Inverter B's is a HYPOTHESIS.
|
||||
TWO = {A: B(-RATING, RATING), Bee: B(-RATING, RATING)}
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print("1. AC 1: the shares sum to the site target, and it is INTEGER arithmetic")
|
||||
|
||||
# ⚠️ THE INVARIANT IS NOT `sum == S`. It is `sum + unmet == S`, and the
|
||||
# difference is the whole of AC 4: an allocation the envelopes could not fully
|
||||
# absorb is still a SAFE allocation, and reporting the shortfall is better than
|
||||
# either refusing or pretending. `unmet_w` is 0 whenever the envelopes allow.
|
||||
_r = plan(1990.0, TWO)
|
||||
print(f" {_r.explain()}")
|
||||
check("two open envelopes, an even weighting: the site target is halved and "
|
||||
"the halves sum back to it",
|
||||
_r.shares == {A: 995, Bee: 995} and _r.unmet_w == 0)
|
||||
check("...and 995 is not 1990, which is the sentence ARCH-01 is about. A "
|
||||
"broadcast hands each unit the site target itself, each supplies it IN "
|
||||
"FULL, and the loop gain at the meter becomes N times the per-unit gain",
|
||||
all(v != _r.sum_w for v in _r.shares.values()))
|
||||
|
||||
# THE LONG REPLAY. AC 1 says "verified over a long replay rather than a spot
|
||||
# check", and it says so because the failure mode is a BIAS - a fraction of a
|
||||
# watt per tick that only shows up in aggregate. A spot check at a round number
|
||||
# cannot see it; 250 000 randomised ticks can.
|
||||
random.seed(20260902)
|
||||
_N = 250_000
|
||||
_bad_sum = _bad_env = _refused = 0
|
||||
_bias = 0
|
||||
_span = 0
|
||||
for _i in range(_N):
|
||||
_S = random.uniform(-6000.0, 6000.0)
|
||||
_ba = B(-random.uniform(0.0, RATING), random.uniform(0.0, RATING))
|
||||
_bb = B(-random.uniform(0.0, RATING), random.uniform(0.0, RATING))
|
||||
_wa = random.random()
|
||||
_p = plan(_S, {A: _ba, Bee: _bb}, weights={A: _wa, Bee: 1.0 - _wa})
|
||||
if not _p.ok:
|
||||
_refused += 1
|
||||
continue
|
||||
if sum(_p.shares.values()) + _p.unmet_w != _p.sum_w:
|
||||
_bad_sum += 1
|
||||
for _u, _s in _p.shares.items():
|
||||
_b = {A: _ba, Bee: _bb}[_u]
|
||||
if not (_b.lo - 1.0 <= _s <= _b.hi + 1.0):
|
||||
_bad_env += 1
|
||||
if _p.unmet_w == 0:
|
||||
_bias += _p.sum_w - sum(_p.shares.values())
|
||||
_span += 1
|
||||
print(f" replayed {_N} ticks at random targets, random envelopes and random "
|
||||
f"weights: {_bad_sum} sum failures, {_bad_env} envelope escapes, "
|
||||
f"{_refused} refusals")
|
||||
check("⚠️ OVER A QUARTER OF A MILLION TICKS THE SUM IS EXACT EVERY TIME. Not "
|
||||
"within a tolerance - EXACT - because `sum_w` is an int, the shares are "
|
||||
"ints and the leftover is settled in integer arithmetic, so there is no "
|
||||
"float in the identity for an error to accumulate in",
|
||||
_bad_sum == 0)
|
||||
check("...and no share ever leaves the envelope it was clamped into, over the "
|
||||
"same replay. An allocator that meets its sum by over-driving one unit "
|
||||
"past its rating has met the wrong invariant",
|
||||
_bad_env == 0)
|
||||
check("⚠️ AND THE ACCUMULATED BIAS IS ZERO, WHICH IS THE POINT OF LARGEST "
|
||||
f"REMAINDER. Summed over {_span} unconstrained ticks the total shortfall "
|
||||
"is 0 W. A 1 W systematic bias at 1-2 Hz is not a rounding artefact - it "
|
||||
"is a permanent standing error with the site integrator wound around it, "
|
||||
"chasing a target the allocator will never let it reach",
|
||||
_bias == 0)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("2. AC 1 continued: WHY largest remainder, measured against the "
|
||||
"alternative")
|
||||
|
||||
# The obvious implementation is `round(w_i * S)` per unit. It is wrong, and the
|
||||
# amount it is wrong by is worth printing rather than asserting.
|
||||
def _naive(S, ws):
|
||||
"""The obvious implementation: round each unit's own share, independently."""
|
||||
return [round(w * S) for w in ws]
|
||||
|
||||
|
||||
random.seed(4242)
|
||||
_naive2 = _naive3 = _ours = 0
|
||||
_worst2 = _worst3 = 0
|
||||
_C = "inverter-c"
|
||||
_THREE = {A: B(-RATING, RATING), Bee: B(-RATING, RATING),
|
||||
_C: B(-RATING, RATING)}
|
||||
for _i in range(50_000):
|
||||
_S = random.randrange(-4000, 4000)
|
||||
_wa = random.random()
|
||||
_n2 = _naive(_S, [_wa, 1.0 - _wa])
|
||||
_naive2 += sum(_n2) - _S
|
||||
_worst2 = max(_worst2, abs(sum(_n2) - _S))
|
||||
_x, _y = sorted((random.random(), random.random()))
|
||||
_w3 = [_x, _y - _x, 1.0 - _y]
|
||||
_n3 = _naive(_S, _w3)
|
||||
_naive3 += sum(_n3) - _S
|
||||
_worst3 = max(_worst3, abs(sum(_n3) - _S))
|
||||
_p3 = plan(float(_S), _THREE, weights=dict(zip([A, Bee, _C], _w3)))
|
||||
_ours += sum(_p3.shares.values()) - _p3.sum_w
|
||||
print(f" 50 000 ticks, per-unit round(): at N=2 it drifts {_naive2:+d} W in "
|
||||
f"total (worst tick {_worst2} W); at N=3, {_naive3:+d} W (worst tick "
|
||||
f"{_worst3} W). Largest remainder at N=3: {_ours:+d} W")
|
||||
check("⚠️ AT THREE INVERTERS THE NAIVE PER-UNIT round() MISSES THE SUM ON REAL "
|
||||
"INPUTS, repeatedly. This is what the card means by calling the rounding "
|
||||
"a safety property: every missed watt is a standing error at the meter "
|
||||
"that the site integrator chases and never reaches",
|
||||
_worst3 >= 1)
|
||||
check("...and largest remainder does not miss it, ever, over the same inputs "
|
||||
"at the same roster - which is also this file's only check that the "
|
||||
"allocator is general in N rather than special-cased at two",
|
||||
_ours == 0 and len(plan(1000.0, _THREE).shares) == 3)
|
||||
check("⚠️ AND AT TWO INVERTERS THE NAIVE VERSION IS ALMOST RIGHT, WHICH IS THE "
|
||||
"DANGEROUS HALF AND IS WHY IT IS MEASURED RATHER THAN ASSUMED. With two "
|
||||
"COMPLEMENTARY weights the two roundings cancel except on an exact "
|
||||
f"half-watt tie, so over 50 000 ticks it drifted {_naive2} W in total. An "
|
||||
"implementation that shipped at N=2 on per-unit rounding would look "
|
||||
"correct and start leaking the day a third inverter arrived - and the tie "
|
||||
"case below is wrong even at N=2",
|
||||
_worst2 <= 1)
|
||||
check("the two-unit case a per-unit round() gets wrong every time is the "
|
||||
"half-watt one: 1501 W split evenly is 750.5 twice, which rounds to "
|
||||
"either 1500 or 1502 - never 1501. Largest remainder gives 751 and 750, "
|
||||
"and gives the extra watt to a NAMED unit rather than to whichever one "
|
||||
"the tie-break happened to favour",
|
||||
plan(1501.0, TWO).shares == {A: 751, Bee: 750}
|
||||
and sum(plan(1501.0, TWO).shares.values()) == 1501)
|
||||
check("...and the tie-break is DETERMINISTIC, so the same inputs give the same "
|
||||
"allocation on every tick and on every host. A tie broken by dict order "
|
||||
"would move a watt between two inverters at 1-2 Hz forever",
|
||||
all(plan(1501.0, TWO).shares == {A: 751, Bee: 750} for _ in range(50)))
|
||||
# THE SITE-LEVEL ROUNDING, graded over a replay for the same reason the sum is:
|
||||
# the failure mode is a BIAS, and one spot check at one fractional target cannot
|
||||
# see one. `int()` instead of `round()` is the mutation that matters here - it
|
||||
# truncates toward zero, which is a systematic under-command of up to a watt on
|
||||
# EVERY tick, in a consistent direction, which is precisely the standing error
|
||||
# the card calls a safety property.
|
||||
random.seed(99)
|
||||
_q = [plan(random.uniform(-4000.0, 4000.0), TWO).quantisation_w
|
||||
for _ in range(20_000)]
|
||||
print(f" 20 000 fractional targets: |quantisation| <= {max(map(abs, _q)):.3f} W, "
|
||||
f"mean {sum(_q) / len(_q):+.5f} W")
|
||||
check("the site target itself is rounded ONCE, at the top, and the record says "
|
||||
"by how much. It is never more than half a watt - a TRUNCATION would be "
|
||||
"up to a whole one - and that half watt is a single site-level rounding "
|
||||
"the integrator corrects on the next tick, not a per-unit bias it cannot "
|
||||
"see",
|
||||
max(map(abs, _q)) <= 0.5 and plan(1500.4, TWO).sum_w == 1500)
|
||||
check("...and it is UNBIASED over the replay, which truncation is not: "
|
||||
"`int(x)` rounds toward zero, so it would under-command on every single "
|
||||
"tick in a consistent direction - a permanent standing error rather than "
|
||||
"a rounding that averages out",
|
||||
abs(sum(_q) / len(_q)) < 0.01)
|
||||
check("...and the allocation does not depend on the ORDER the envelopes arrive "
|
||||
"in, which is what makes it reproducible tick to tick: `plan()` sorts the "
|
||||
"roster before it does anything else, so a dict built the other way round "
|
||||
"gives the same shares",
|
||||
plan(1501.0, {Bee: B(-RATING, RATING), A: B(-RATING, RATING)}).shares
|
||||
== plan(1501.0, {A: B(-RATING, RATING), Bee: B(-RATING, RATING)}).shares
|
||||
== {A: 751, Bee: 750})
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("3. AC 4: saturation - the surplus moves, and what will not fit is NAMED")
|
||||
|
||||
_sat = plan(4000.0, {A: B(-RATING, 1000.0), Bee: B(-RATING, RATING)},
|
||||
weights={A: 0.5, Bee: 0.5})
|
||||
print(f" {_sat.explain()}")
|
||||
check("one inverter at its rating gives its surplus to the other rather than "
|
||||
"being over-driven. An even weighting would have asked A for 2000 W; its "
|
||||
"envelope stops at 1000 W and B takes the other 3000",
|
||||
_sat.shares == {A: 1000, Bee: 3000} and _sat.unmet_w == 0)
|
||||
check("...and the record says WHY it got 1000 and not 2000, per unit, in words "
|
||||
"an operator can act on rather than as a silent clamp",
|
||||
any(p.unit == A and "envelope full" in p.why for p in _sat.plans))
|
||||
|
||||
_unmet = plan(9000.0, {A: B(-RATING, 1000.0), Bee: B(-RATING, 2000.0)})
|
||||
print(f" {_unmet.explain()}")
|
||||
check("⚠️ AND WHEN NEITHER CAN TAKE IT, `unmet_w` IS REPORTED RATHER THAN THE "
|
||||
"SUM QUIETLY MISSING. 9000 W asked for, 3000 W of envelope: both units go "
|
||||
"to their ceilings and 6000 W is stated as unmet",
|
||||
_unmet.shares == {A: 1000, Bee: 2000} and _unmet.unmet_w == 6000)
|
||||
check("...and the allocation is still OK, which is the decision worth stating: "
|
||||
"a saturated site is not a broken allocation. Commanding 3000 W of the "
|
||||
"9000 the loop asked for is strictly better than commanding 0 W, and the "
|
||||
"shortfall is a fact the write gate can act on. Fusing `unmet_w` into "
|
||||
"`ok` would let one saturated inverter park the whole site",
|
||||
_unmet.ok is True)
|
||||
check("the identity that holds in every case, saturated or not: shares + unmet "
|
||||
"== the site target",
|
||||
sum(_unmet.shares.values()) + _unmet.unmet_w == _unmet.sum_w)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("4. AC 5: a pack at its SoC floor - 0 W discharging, STILL CHARGEABLE")
|
||||
|
||||
# The floor arrives as a `hi` of 0 on that unit's interval: it may not
|
||||
# discharge. It says nothing about charging, and reading it as "this unit is
|
||||
# out" is the mistake - a unit at its floor is precisely the unit that most
|
||||
# wants the charge.
|
||||
_floor = {A: B(-RATING, 0.0), Bee: B(-RATING, RATING)}
|
||||
_dis = plan(1990.0, _floor)
|
||||
_chg = plan(-1990.0, _floor)
|
||||
print(f" discharging: {_dis.explain()}")
|
||||
print(f" charging: {_chg.explain()}")
|
||||
check("in the DISCHARGING direction the floored unit is allocated 0 W and the "
|
||||
"other carries the whole site target",
|
||||
_dis.shares == {A: 0, Bee: 1990} and _dis.unmet_w == 0)
|
||||
check("⚠️ AND IN THE CHARGING DIRECTION IT IS STILL AVAILABLE, which is the "
|
||||
"half a `if soc <= floor: skip this unit` implementation gets wrong. Its "
|
||||
"envelope forbids discharge, not participation, and a pack at its floor "
|
||||
"is the one that most needs the charge",
|
||||
_chg.shares == {A: -995, Bee: -995})
|
||||
check("...and 0 W is not a sign of its own: the floored unit's 0 W sits happily "
|
||||
"beside the other's +1990 W without tripping the sign-coherence gate, "
|
||||
"because zero is coherent with every direction",
|
||||
_dis.ok is True and _dis.refused is None)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("5. AC 6: a dead link leaves the envelope set, and IS ANNOUNCED")
|
||||
|
||||
_dead = plan(1990.0, TWO, live=(A,))
|
||||
print(f" {_dead.explain()}")
|
||||
check("a unit whose master is stale is REMOVED from the envelope set. "
|
||||
"Allocating into a link nobody can reach is writing into a void and "
|
||||
"calling the site target met",
|
||||
Bee not in _dead.shares and _dead.dropped == ((Bee, DROP_STALE),))
|
||||
check("...and the survivor carries the whole site target, which is right: there "
|
||||
"is one integrator on P1 and its output still has to be delivered",
|
||||
_dead.shares == {A: 1990} and _dead.unmet_w == 0)
|
||||
check("⚠️ AND IT DOES NOT ABSORB IT SILENTLY. The record NAMES the unit and the "
|
||||
"reason, so `main.py` can put it in the action log and SAFETY-28's write "
|
||||
"gate can refuse on it. A site running at half its inverters and "
|
||||
"reporting nothing reads as a healthy site on every dashboard",
|
||||
_dead.dropped[0][0] == Bee and _dead.dropped[0][1] == DROP_STALE
|
||||
and any(p.unit == Bee and "DROPPED" in p.why for p in _dead.plans))
|
||||
check("...and the per-unit plan for the dropped unit is present rather than "
|
||||
"absent, so a gate iterating the roster finds an entry for every inverter "
|
||||
"instead of having to notice a missing key",
|
||||
{p.unit for p in _dead.plans} == {A, Bee})
|
||||
check("a unit contradicting ITSELF - its own lo above its own hi - leaves the "
|
||||
"set for its own reason, and does not park the site. That is stage 1's "
|
||||
"decision honoured, not re-litigated here",
|
||||
plan(1990.0, {A: B(-RATING, RATING),
|
||||
Bee: B(500.0, -500.0, contra=True)}).dropped
|
||||
== ((Bee, DROP_CONTRADICTION),))
|
||||
check("an interval that contains NO INTEGER is dropped too, and says which case "
|
||||
"it is. The register is 1 W: there is no number that unit could be "
|
||||
"commanded that both of its own bounds accept",
|
||||
plan(0.0, {A: B(-RATING, RATING), Bee: B(100.2, 100.8)}).dropped
|
||||
== ((Bee, DROP_NO_INTEGER),))
|
||||
check("⚠️ AND EVERY UNIT GONE IS A REFUSAL, NOT AN EMPTY SUCCESS. With nobody "
|
||||
"in the envelope set there is nothing to allocate to, and inventing a "
|
||||
"share for a link nobody can reach is the failure the refusal branch "
|
||||
"exists for. THIS is the trigger `main.py`'s `if not resolution."
|
||||
"allocated:` was re-aimed onto when ALLOC-01 removed its old one",
|
||||
plan(1990.0, TWO, live=()).ok is False
|
||||
and REFUSE_EMPTY in plan(1990.0, TWO, live=()).refused)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("6. AC 7: opposite directions are REFUSED, not averaged")
|
||||
|
||||
# ⚠️ WHY THIS IS A SAFETY GATE AND NOT AN EFFICIENCY ONE. One pack discharging
|
||||
# while another charges round-trips energy through two conversion stages, and it
|
||||
# is INVISIBLE: the meter sees the net, which is exactly S, so the site
|
||||
# integrator is content; each unit is meeting the target it was given; the sign
|
||||
# watchdog compares a command against the meter and both agree. Nothing in this
|
||||
# repository would ever report it.
|
||||
_circ = plan(1000.0, {A: B(-RATING, RATING, gate=P_MAINTENANCE, pin=2500.0,
|
||||
by="maintenance"),
|
||||
Bee: B(-RATING, RATING)}, site_priority=P_LOOP)
|
||||
print(f" {_circ.explain()}")
|
||||
check("a maintenance drain of 2500 W on one pack against a site target of "
|
||||
"1000 W would need the other pack to CHARGE at 1500 W to make the sum. "
|
||||
"That nets to exactly the right number at the meter, which is precisely "
|
||||
"why it has to be refused here - no downstream guard can see it",
|
||||
_circ.ok is False and REFUSE_SIGN in _circ.refused)
|
||||
check("...and the refusal NAMES both sides, so an operator is told which two "
|
||||
"inverters were about to push against each other",
|
||||
A in _circ.refused and Bee in _circ.refused)
|
||||
check("...and it is a REFUSAL rather than a quiet re-plan: dropping the pinned "
|
||||
"unit and re-filling would silently override a claim that outranked the "
|
||||
"loop, which is a worse answer than stopping and saying so",
|
||||
_circ.shares == {})
|
||||
check("the same pin with a site target BEYOND it is fine, because the shares "
|
||||
"then agree in sign - the gate grades the OUTPUT, not the presence of a "
|
||||
"pin",
|
||||
plan(3000.0, {A: B(-RATING, RATING, gate=P_MAINTENANCE, pin=2500.0,
|
||||
by="maintenance"),
|
||||
Bee: B(-RATING, RATING)},
|
||||
site_priority=P_LOOP).shares == {A: 2500, Bee: 500})
|
||||
check("⚠️ AND IT NEVER FIRES ON AN ORDINARY TICK, which is what makes it a gate "
|
||||
"rather than a nuisance. Over the 250 000-tick replay in part 1 - random "
|
||||
"targets, random envelopes, random weights, no pins - it refused "
|
||||
f"{_refused} times",
|
||||
_refused == 0)
|
||||
check("...and it cannot: with no pin and an envelope that contains zero, the "
|
||||
"fill only ever moves shares in ONE direction away from zero, so two "
|
||||
"signs are not expressible. The gate exists for the envelope that "
|
||||
"EXCLUDES zero, which is a forced floor or a pin",
|
||||
all(v >= 0 for v in plan(1990.0, TWO).shares.values())
|
||||
and all(v <= 0 for v in plan(-1990.0, TWO).shares.values()))
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("7. AC 8: at N<=1 it is a pass-through, byte-identical to ARB-03")
|
||||
|
||||
check("with no units at all the whole target goes to the site actuator, as a "
|
||||
"float", allocate(1500.0, {}) == ({ACTUATOR_SITE: 1500.0}, True))
|
||||
check("with one unit the share IS the site target - §6.2's N=1 identity: with "
|
||||
"one inverter the fabricated grid reading and the battery setpoint are "
|
||||
"the same number, so there is nothing to divide",
|
||||
allocate(1500.0, {A: UnitBounds()}) == ({A: 1500.0}, True))
|
||||
check("⚠️ AND IT IS A FLOAT, UNROUNDED. The general path rounds to the 1 W "
|
||||
"register; the pass-through must not, because every N=1 replay in this "
|
||||
"repository - test_arbiter, test_watchdog, test_validate, test_peakguard "
|
||||
"- expects the number it saw before ALLOC-01. This is the line a 'tidy "
|
||||
"the special case away' refactor goes red on",
|
||||
allocate(1500.4, {A: UnitBounds()}) == ({A: 1500.4}, True)
|
||||
and isinstance(allocate(1500.4, {A: UnitBounds()})[0][A], float))
|
||||
check("...and it is UNCLAMPED too, which is the other half of byte-identity: at "
|
||||
"N=1 every per-inverter claim routes to the SITE actuator anyway, so "
|
||||
"stage 2 has already applied the rating and re-applying an interval here "
|
||||
"would be a second, different clamp on a live safety path",
|
||||
allocate(9999.0, {A: B(-RATING, RATING)}) == ({A: 9999.0}, True))
|
||||
_thru = plan(1500.0, {A: UnitBounds()})
|
||||
check("...and the pass-through still produces a RECORD, so SAFETY-28's write "
|
||||
"gate reads the same shape at every roster size and does not need an N=1 "
|
||||
"special case of its own",
|
||||
_thru.ok and _thru.passthrough and _thru.plans and _thru.unmet_w == 0)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("8. AC 2 and AC 3, on a MODELLED plant: split-invariance and the sweep")
|
||||
|
||||
# ⚠️ READ THE FILE HEADER BEFORE READING THESE NUMBERS. The plant here is
|
||||
# modelled IN THIS FILE - `lag_s=0`, unbounded ramp, which is the limit
|
||||
# ARCH-01's own evidence was computed in - and the loop is the REAL `compute()`
|
||||
# out of app/control.py. So the claim these checks support is about THE CONTROL
|
||||
# LAW AND THE ALLOCATOR, not about a GW5000S-BP. The hardware claim is
|
||||
# `tools/alloc_sim.py` against admin/goodwe's rig, quoted in the pull request.
|
||||
CYCLE_S = 5.0
|
||||
|
||||
|
||||
def close_loop(gain, split, cycles=200, load_w=2000.0, mode="alloc",
|
||||
feedback="site", rating=RATING):
|
||||
"""One integrator on the meter, N units, each told its OWN share.
|
||||
|
||||
`feedback` is what `compute()` is handed as `actual_w`, and it is a
|
||||
PARAMETER because it turns out to be the whole of the AC 2 finding - see
|
||||
below. "site" is the sum of the units' power; "unit" is inverter A's alone,
|
||||
which is what the shipped add-on's single `inverter_power` sensor gives it.
|
||||
"""
|
||||
tuning = Tuning(gain=gain)
|
||||
prev, i_w, sat = 0.0, None, 0
|
||||
power = [0.0, 0.0]
|
||||
grid = load_w
|
||||
trace = []
|
||||
for _c in range(cycles):
|
||||
d = compute(prev, grid, sum(power) if feedback == "site" else power[0],
|
||||
tuning, sat, i_w)
|
||||
prev, i_w, sat = d.target_w, d.i_w, d.sat_count
|
||||
if mode == "broadcast":
|
||||
cmds = [d.target_w, d.target_w]
|
||||
else:
|
||||
p = plan(d.target_w, {A: B(-rating, rating), Bee: B(-rating, rating)},
|
||||
weights={A: split, Bee: 1.0 - split})
|
||||
assert p.ok, p.refused
|
||||
cmds = [float(p.shares[A]), float(p.shares[Bee])]
|
||||
# The modelled unit: it obeys within one cycle, bounded by its rating.
|
||||
power = [max(-rating, min(rating, c)) for c in cmds]
|
||||
grid = load_w - sum(power)
|
||||
trace.append((round(d.target_w, 6), round(grid, 6)))
|
||||
return trace
|
||||
|
||||
|
||||
def p2p(trace, k=20):
|
||||
tail = [g for _t, g in trace[-k:]]
|
||||
return max(tail) - min(tail)
|
||||
|
||||
|
||||
_ref = close_loop(1.0, 0.5)
|
||||
_splits = [0.5, 0.9, 0.1, 0.99, 1.0, 0.0]
|
||||
_same = {s: close_loop(1.0, s) == _ref for s in _splits}
|
||||
print(f" aggregate trace vs the 50/50 reference, gain 1.0: "
|
||||
+ ", ".join(f"{int(s*100)}/{int((1-s)*100)}={'same' if v else 'DIFFERS'}"
|
||||
for s, v in _same.items()))
|
||||
check("⚠️ AC 2. A 90/10 AND A 50/50 SPLIT PRODUCE AN IDENTICAL AGGREGATE TRACE "
|
||||
"AT THE METER - and so do 99/1 and 100/0. Not close: the same numbers. "
|
||||
"That is what says the weights are a COMFORT CHOICE and not a tuning "
|
||||
"parameter, and it is the reason §6.2 chose share allocation over a "
|
||||
"regulator/ballast arrangement, where the ballast unit's share is a "
|
||||
"function of the shared measurement and the gain question comes back",
|
||||
all(_same.values()))
|
||||
check("...and it is not vacuous, because the SHARES really are different. An "
|
||||
"allocator that ignored its weights would pass the line above trivially",
|
||||
close_loop(1.0, 0.9) == close_loop(1.0, 0.5)
|
||||
and plan(2000.0, TWO, weights={A: 0.9, Bee: 0.1}).shares
|
||||
!= plan(2000.0, TWO, weights={A: 0.5, Bee: 0.5}).shares)
|
||||
check("...and it holds at EVERY gain the schema accepts, not only at the one "
|
||||
"the reference experiment uses",
|
||||
all(close_loop(g, 0.9) == close_loop(g, 0.5)
|
||||
for g in (0.05, 0.2, 0.4, 0.6, 0.8, 1.0)))
|
||||
|
||||
# THE SWEEP. AC 3 says the sweep is the check, not an argument.
|
||||
_GAINS = (0.05, 0.2, 0.4, 0.6, 0.8, 0.9, 1.0)
|
||||
_alloc_worst = max(p2p(close_loop(g, s, feedback=f))
|
||||
for g in _GAINS for s in _splits for f in ("site", "unit"))
|
||||
# ⚠️ THE BROADCAST RUNS ARE FED ONE INVERTER'S POWER, because that is what a
|
||||
# broadcast INSTALL would have: the add-on binds a single `inverter_power`
|
||||
# sensor, so an operator who wires up a second inverter has a loop that sees
|
||||
# unit A only. Feeding it the site sum here would model an add-on that does not
|
||||
# exist, and it would do so in the KIND direction - the sum tracks the command
|
||||
# much worse at N=2, so the saturation freeze would fire and damp the very limit
|
||||
# cycle this comparison exists to reproduce. sitesim.run_site() makes the same
|
||||
# choice for the same reason, and the two agree to the watt: 40 W p2p at gain
|
||||
# 0.8, 120 W at 0.9, 4000 W at 1.0.
|
||||
_bcast = {g: p2p(close_loop(g, 0.5, mode="broadcast", feedback="unit"))
|
||||
for g in _GAINS}
|
||||
print(f" broadcast tail p2p by gain: "
|
||||
+ ", ".join(f"{g}={v:.0f}" for g, v in _bcast.items()))
|
||||
print(f" allocated, worst over {len(_GAINS)}x{len(_splits)}x2 "
|
||||
f"(gain x split x feedback): {_alloc_worst:.0f} W")
|
||||
check("⚠️ AC 3. SWEEPING THE GAIN TO 1.0 - WHICH config.yaml ACCEPTS AS ITS "
|
||||
"DOCUMENTED MAXIMUM - AT EVERY SPLIT SHOWS NO LIMIT CYCLE. The tail "
|
||||
"settles to a flat line at all 84 combinations - at BOTH the site-level "
|
||||
"feedback the loop should have and the single-sensor feedback it has",
|
||||
_alloc_worst == 0.0)
|
||||
check("⚠️ AND THE SWEEP IS NOT VACUOUS, because the SAME sweep reproduces the "
|
||||
"fault at the same gain. Broadcast at gain 1.0 is a permanent limit cycle "
|
||||
"- this is ARCH-01's measured 4000 W peak-to-peak, rebuilt here from the "
|
||||
"shipped control law rather than quoted",
|
||||
_bcast[1.0] >= 3900.0)
|
||||
check("...and the fault has an ONSET, which says it is a gain-margin failure "
|
||||
"and not a bug in the rig: quiet at 0.6, visible at 0.9, unbounded at "
|
||||
"1.0. An allocator that 'fixed' a cycle that was never there would show a "
|
||||
"flat broadcast row",
|
||||
_bcast[0.6] == 0.0 and 0.0 < _bcast[0.9] < _bcast[1.0])
|
||||
check("...and the broadcast export overshoot at gain 0.6 - the half that has no "
|
||||
"gain threshold at all - is present here too, at ARCH-01's measured "
|
||||
"-400 W, while the allocated run does not export",
|
||||
min(g for _t, g in close_loop(0.6, 0.5, mode="broadcast",
|
||||
feedback="unit")[1:]) <= -400.0
|
||||
and min(g for _t, g in close_loop(0.6, 0.5)[1:]) >= 0.0)
|
||||
|
||||
# ⚠️ THE ONE THAT DOES NOT HOLD, AND IT IS REPORTED RATHER THAN HIDDEN.
|
||||
_unit_fb = {s: close_loop(0.6, s, feedback="unit")
|
||||
== close_loop(0.6, 0.5, feedback="unit") for s in _splits}
|
||||
print(f" with the loop fed ONE inverter's power instead of the site's, at "
|
||||
f"gain 0.6: " + ", ".join(f"{int(s*100)}/{int((1-s)*100)}="
|
||||
f"{'same' if v else 'DIFFERS'}"
|
||||
for s, v in _unit_fb.items()))
|
||||
check("⚠️ SPLIT-INVARIANCE IS A PROPERTY OF THE LOOP'S INPUTS, NOT ONLY OF THE "
|
||||
"ALLOCATOR, AND THE SHIPPED ADD-ON BREAKS IT FROM THE OTHER END. There is "
|
||||
"ONE `inverter_power` sensor, so at a roster of two `actual_w` is ONE "
|
||||
"unit's power used as a site measurement - the SENSING half of the same "
|
||||
"N=1 identity this card removes from the COMMANDING half. Feed the loop "
|
||||
"that and the aggregate trace becomes a function of the split. The "
|
||||
"allocator is not the cause: its shares sum to S in every one of these "
|
||||
"runs. Measured on the real rig too (tools/alloc_sim.py --splits "
|
||||
"--gain 0.6), and it is DEV-02's to close",
|
||||
not all(_unit_fb.values()))
|
||||
check("...and the counterfactual is what says the sensor is the cause rather "
|
||||
"than the allocator: change that ONE input to the site total and every "
|
||||
"split is bit-identical again, at every gain",
|
||||
all(close_loop(g, s, feedback="site") == close_loop(g, 0.5,
|
||||
feedback="site")
|
||||
for g in (0.2, 0.4, 0.6, 1.0) for s in _splits))
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("9. the structural claim itself: the gain at the meter is a CONVEX "
|
||||
"combination")
|
||||
|
||||
# ⚠️ THIS IS THE ARGUMENT THE WHOLE CARD RESTS ON, SO IT IS MEASURED. Give the
|
||||
# two modelled units DIFFERENT per-unit gains - unit i delivers g_i of what it
|
||||
# is told - and read the gain the site actually shows. Under broadcast it is the
|
||||
# SUM. Under allocation it is a weighted average, so it lies between the two
|
||||
# whatever the weights are.
|
||||
def site_gain(g_a, g_b, split, mode):
|
||||
told = 1000.0
|
||||
if mode == "broadcast":
|
||||
return (g_a * told + g_b * told) / told
|
||||
p = plan(told, TWO, weights={A: split, Bee: 1.0 - split})
|
||||
return (g_a * p.shares[A] + g_b * p.shares[Bee]) / told
|
||||
|
||||
|
||||
_GA, _GB = 0.4, 1.0
|
||||
_alloc_gains = [site_gain(_GA, _GB, s, "alloc") for s in (0.0, 0.25, 0.5,
|
||||
0.75, 1.0)]
|
||||
print(f" per-unit gains {_GA} and {_GB}: allocated site gain over splits "
|
||||
f"0/25/50/75/100 = {[round(x, 3) for x in _alloc_gains]}; "
|
||||
f"broadcast = {site_gain(_GA, _GB, 0.5, 'broadcast'):.3f}")
|
||||
check("⚠️ FOR ANY SPLIT the gain at the meter lies between the two per-unit "
|
||||
"gains. THAT is why a bad split cannot destabilise the site and why the "
|
||||
"weights may be chosen for SoC, thermals and wear without anyone "
|
||||
"re-deriving a stability margin",
|
||||
all(_GA - 1e-9 <= g <= _GB + 1e-9 for g in _alloc_gains))
|
||||
check("...and under broadcast it is their SUM, which is outside that interval "
|
||||
"and grows with N. At two units of gain 1.0 that is 2.0 against a loop "
|
||||
"whose config maximum is 1.0 - the 2.12 ARCH-01 measured, and the reason "
|
||||
"the limit cycle has no upper bound",
|
||||
site_gain(_GA, _GB, 0.5, "broadcast") > _GB)
|
||||
check("...and the same holds for two units with the SAME gain, which is the "
|
||||
"case that will actually ship: allocation leaves it at g, broadcast "
|
||||
"doubles it",
|
||||
site_gain(0.8, 0.8, 0.3, "alloc") == 0.8
|
||||
and site_gain(0.8, 0.8, 0.3, "broadcast") == 1.6)
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("10. the envelope is read PER TICK, and the weights are not a constraint")
|
||||
|
||||
_moving = {A: B(-RATING, RATING), Bee: B(-RATING, RATING)}
|
||||
_first = plan(2000.0, _moving)
|
||||
_moving[Bee] = B(-RATING, 0.0) # B's pack hits its floor mid-run
|
||||
_second = plan(2000.0, _moving)
|
||||
print(f" same allocator object, envelope moved between ticks: "
|
||||
f"{_first.shares} then {_second.shares}")
|
||||
check("⚠️ THE SAME CALL WITH A MOVED ENVELOPE GIVES A DIFFERENT ANSWER, which "
|
||||
"is what says nothing was cached at construction. There is no allocator "
|
||||
"OBJECT to cache in - `plan()` is a pure function of this tick's "
|
||||
"intervals - and an allocator holding a construction-time envelope "
|
||||
"over-allocates into a unit that cannot take it",
|
||||
_first.shares == {A: 1000, Bee: 1000}
|
||||
and _second.shares == {A: 2000, Bee: 0})
|
||||
check("...and the module holds no state at all, which is how that is enforced "
|
||||
"rather than promised: nothing in it is written outside a function",
|
||||
not [n for n, v in vars(sys.modules["app.allocator"]).items()
|
||||
if not n.startswith("_") and isinstance(v, (list, dict, set))])
|
||||
|
||||
_zero = plan(4000.0, {A: B(-RATING, 1000.0), Bee: B(-RATING, RATING)},
|
||||
weights={A: 1.0, Bee: 0.0})
|
||||
print(f" weight 0 on B, but A's envelope is full: {_zero.explain()}")
|
||||
check("a weight of 0 is honoured while the preferred unit has headroom",
|
||||
plan(1000.0, TWO, weights={A: 1.0, Bee: 0.0}).shares == {A: 1000, Bee: 0})
|
||||
check("⚠️ BUT IT IS A PREFERENCE, NOT A PERMISSION. When the preferred unit "
|
||||
"fills up the rest goes to the zero-weight unit anyway, because the SUM "
|
||||
"is the safety property and stranding capacity behind a comfort choice "
|
||||
"would manufacture a standing error at the meter for the site integrator "
|
||||
"to chase. To make a unit unusable, close its envelope",
|
||||
_zero.shares == {A: 1000, Bee: 3000} and _zero.unmet_w == 0)
|
||||
check("...and the record says that is what happened, rather than leaving a "
|
||||
"reader to wonder why the weights were disregarded",
|
||||
any(p.unit == Bee and "last resort" in p.why for p in _zero.plans))
|
||||
check("a negative weight is REFUSED rather than normalised away - it is a "
|
||||
"signed target wearing a comfort weight's clothes, and silently taking "
|
||||
"its magnitude would allocate against the direction the caller asked for",
|
||||
_raises_value(lambda: plan(1000.0, TWO, weights={A: -1.0, Bee: 1.0})))
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("11. the seam above: what resolve() hands stage 3, and the pin gate")
|
||||
|
||||
_res = resolve([Claim.set("loop", P_LOOP, 900.0),
|
||||
Claim.limit("device", P_SAFETY, -2000, 2000, "rating",
|
||||
actuator=A),
|
||||
Claim.limit("supervised", P_SAFETY, -2000, 2000, "max_w",
|
||||
actuator=A)],
|
||||
units=(A, Bee))
|
||||
print(f" {_res.explain()} -> {_res.allocation.explain()}")
|
||||
check("resolve() carries the full record through, so SAFETY-28 has one place "
|
||||
"to gate on and does not have to re-derive anything",
|
||||
isinstance(_res.allocation, Allocation) and _res.allocation.ok
|
||||
and _res.shares == _res.allocation.shares)
|
||||
check("...and the priority stage 3 weighs a unit's own SET against is the "
|
||||
"priority of the claim `explain()` NAMES, taken from stage 2 rather than "
|
||||
"recomputed - so the two cannot drift apart",
|
||||
_res.winner_priority == P_LOOP and _res.winner == "loop")
|
||||
|
||||
# THE PIN GATE. A unit's own winning SET competes with the site's.
|
||||
_pin = {A: B(-RATING, RATING, gate=P_MAINTENANCE, pin=-1200.0, by="maintenance"),
|
||||
Bee: B(-RATING, RATING)}
|
||||
_low = plan(-3000.0, _pin, site_priority=P_LOOP)
|
||||
_high = plan(0.0, _pin, site_priority=P_SAFETY)
|
||||
print(f" maintenance pin vs the loop: {_low.explain()}")
|
||||
print(f" maintenance pin vs a safety stop: {_high.explain()}")
|
||||
check("a unit's own maintenance SET at P_MAINTENANCE outranks the grid-"
|
||||
"following loop, so that pack does what its own cycle asked and the OTHER "
|
||||
"unit carries the remainder of the site target. The shares still sum to S",
|
||||
_low.shares == {A: -1200, Bee: -1800}
|
||||
and sum(_low.shares.values()) == _low.sum_w)
|
||||
check("⚠️ AND A SITE SAFETY STOP OUTRANKS THE PIN, which is the case that has "
|
||||
"to be right: `safety` files a SITE set at P_SAFETY for 'stopped' and "
|
||||
"'inputs missing', and a maintenance drain that survived it would be an "
|
||||
"inverter this controller had stopped and then kept driving",
|
||||
_high.shares == {A: 0, Bee: 0})
|
||||
check("...and with no site priority named at all, the unit's own claim stands - "
|
||||
"a caller that says nothing about the site has not said the site outranks "
|
||||
"anything, and honouring the unit's highest-priority claim is the only "
|
||||
"safe reading of silence",
|
||||
plan(-3000.0, _pin).shares == {A: -1200, Bee: -1800})
|
||||
|
||||
# ⚠️ THE RESIDUAL, STATED RATHER THAN GLOSSED. `pre_resolve()` filters a unit's
|
||||
# LIMITS by that unit's OWN gate, and clause 2 of the arbiter's rule says a
|
||||
# limit binds only at or above the WINNER's priority - which at N>=2 may be the
|
||||
# site's, chosen afterwards. Where the site winner outranks a unit's gate, a
|
||||
# unit limit whose priority falls between them is applied more tightly than
|
||||
# clause 2 strictly requires. Enumerated over what main.py can actually file:
|
||||
_UNIT_LIMITS = {"device": P_SAFETY, "supervised": P_SAFETY,
|
||||
"maintenance": P_MAINT_SHAPE}
|
||||
_UNIT_SETS = {"failsafe": P_SAFETY, "maintenance": P_MAINTENANCE}
|
||||
_SITE_SETS = {"loop": P_LOOP, "arbitrage": P_ARBITRAGE, "safety": P_SAFETY}
|
||||
_affected = [(ls, lp, us, up, ss, sp)
|
||||
for ls, lp in _UNIT_LIMITS.items()
|
||||
for us, up in list(_UNIT_SETS.items()) + [(None, None)]
|
||||
for ss, sp in _SITE_SETS.items()
|
||||
# included by pre_resolve (no gate, or the gate does not exclude it)
|
||||
if (up is None or lp >= up)
|
||||
# but clause 2 against the SITE winner would have excluded it
|
||||
and lp < sp]
|
||||
print(f" unit-limit x unit-set x site-set combinations main.py can file: "
|
||||
f"{len(_UNIT_LIMITS) * (len(_UNIT_SETS) + 1) * len(_SITE_SETS)}; "
|
||||
f"tighter than clause 2 strictly requires: {len(_affected)}")
|
||||
for _row in _affected:
|
||||
print(f" {_row[0]}@{_row[1]} under {_row[2]}@{_row[3]} "
|
||||
f"vs site {_row[4]}@{_row[5]}")
|
||||
check("⚠️ THE ONLY COMBINATIONS AFFECTED ARE THE MAINTENANCE CHARGE-ONLY LIMIT "
|
||||
"UNDER A SITE SAFETY STOP, and a safety stop resolves to 0 W - a "
|
||||
"charge-only `hi` of 0 does not move 0. So the tighter reading is not "
|
||||
"observable on anything main.py can file today. It is written down here "
|
||||
"because a ninth source could change that, and because erring TIGHT is "
|
||||
"the safe direction: a tighter envelope allocates less, never more",
|
||||
all(row[0] == "maintenance" and row[4] == "safety" for row in _affected))
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("12. mutation: what defeats these guards, and which check bites")
|
||||
|
||||
MUT = []
|
||||
|
||||
|
||||
def _largest_remainder_replaced_by_round(S, ws):
|
||||
return {u: round(w * S) for u, w in ws.items()}
|
||||
|
||||
|
||||
_m = _largest_remainder_replaced_by_round(1501.0, {A: 0.5, Bee: 0.5})
|
||||
MUT.append(("largest remainder replaced by a per-unit round()",
|
||||
sum(_m.values()) != 1501,
|
||||
"part 2: 'largest remainder does not miss it, ever'"))
|
||||
|
||||
# The envelope clamp dropped: shares placed by weight alone.
|
||||
_m2 = {A: 0.5 * 4000.0, Bee: 0.5 * 4000.0}
|
||||
MUT.append(("the envelope clamp dropped - shares placed by weight alone",
|
||||
_m2[A] > 1000.0 and plan(4000.0, {A: B(-RATING, 1000.0),
|
||||
Bee: B(-RATING, RATING)}).shares[A]
|
||||
== 1000,
|
||||
"part 3: 'one inverter at its rating gives its surplus to the other'"))
|
||||
|
||||
# The liveness argument ignored - `live` never consulted.
|
||||
MUT.append(("`live` ignored, so a stale master keeps being allocated into",
|
||||
plan(1990.0, TWO, live=(A,)).shares != plan(1990.0, TWO).shares,
|
||||
"part 5: 'a unit whose master is stale is REMOVED'"))
|
||||
|
||||
# The sign gate removed - the circulating case allocated instead of refused.
|
||||
MUT.append(("the sign-coherence gate removed",
|
||||
_circ.ok is False,
|
||||
"part 6: 'opposite directions are REFUSED, not averaged'"))
|
||||
|
||||
# The N<=1 branch folded into the general path.
|
||||
MUT.append(("the N<=1 pass-through folded into the general path (it would "
|
||||
"round, and clamp)",
|
||||
allocate(1500.4, {A: UnitBounds()})[0][A] == 1500.4
|
||||
and allocate(9999.0, {A: B(-RATING, RATING)})[0][A] == 9999.0,
|
||||
"part 7: 'a float, unrounded' and 'unclamped too'"))
|
||||
|
||||
# The allocator broadcasts - the ARCH-01 fault, rebuilt.
|
||||
_bc = {u: 1990 for u in TWO}
|
||||
MUT.append(("the allocator replaced by a broadcast - ARCH-01's own fault",
|
||||
sum(_bc.values()) != 1990 and plan(1990.0, TWO).unmet_w == 0,
|
||||
"part 1: 'the halves sum back to it', and part 8's sweep"))
|
||||
|
||||
# unmet_w folded into ok.
|
||||
MUT.append(("`unmet_w != 0` folded into `ok`, so a saturated inverter parks "
|
||||
"the site",
|
||||
_unmet.ok is True and _unmet.unmet_w == 6000,
|
||||
"part 3: 'a saturated site is not a broken allocation'"))
|
||||
|
||||
# The pin gate inverted: the site winner never outranks a unit SET.
|
||||
MUT.append(("the pin gate inverted - a maintenance drain survives a site "
|
||||
"safety stop",
|
||||
_high.shares == {A: 0, Bee: 0},
|
||||
"part 11: 'a site safety stop outranks the pin'"))
|
||||
|
||||
# scope_errors ignored by stage 3.
|
||||
_mis = resolve([Claim.set("loop", P_LOOP, -1500.0),
|
||||
Claim.limit("peak", P_PEAK, lo=1500.0, reason="q",
|
||||
actuator=Bee)])
|
||||
MUT.append(("`scope_errors` ignored by stage 3 - a mis-routed claim divided "
|
||||
"anyway",
|
||||
_mis.allocated is False and REFUSE_SCOPE in _mis.allocation.refused,
|
||||
"test_arbiter.py part 8: 'stage 3 REFUSES to allocate on a claim "
|
||||
"list it has been told is mis-routed'"))
|
||||
|
||||
MUT.append(("the site target TRUNCATED instead of rounded - a bias toward zero "
|
||||
"on every tick",
|
||||
max(map(abs, _q)) <= 0.5,
|
||||
"part 2: '|quantisation| is never more than half a watt'"))
|
||||
|
||||
# ⚠️ AND NOW THE ONES THAT DO NOT BITE. Three of them, found by actually running
|
||||
# the mutations rather than by reasoning about them, and each is reported with
|
||||
# WHY - because a mutation table that only lists its successes is the same
|
||||
# unverifiable claim as a green check that cannot fail.
|
||||
MUT.append(("the FLOOR replaced by a round() before the leftover pass",
|
||||
False,
|
||||
"NOTHING - and it should not, because THE SUM IS NOT PROTECTED BY "
|
||||
"THE FLOOR. It is protected by the integer leftover pass that "
|
||||
"follows: whatever per-unit integerisation happens first, `debt = "
|
||||
"remainder - sum(share)` is computed from it and handed out until "
|
||||
"it is zero. Rounding first produces a DIFFERENT but still exactly "
|
||||
"sum-invariant allocation. Largest remainder is what decides WHICH "
|
||||
"unit is credited the leftover watt - the one that was shorted "
|
||||
"most - which is a fairness property, not a safety one. Remove the "
|
||||
"leftover pass itself and part 1 goes red, which is the row above"))
|
||||
MUT.append(("the largest-remainder TIE-BREAK on the unit name dropped",
|
||||
False,
|
||||
"NOTHING - and by construction: `plan()` sorts the roster before it "
|
||||
"does anything else and Python's sort is stable, so the order is "
|
||||
"already by name when the tie-break is reached. The determinism is "
|
||||
"delivered upstream; the explicit key is belt and braces. Part 2's "
|
||||
"dict-order check is what actually grades the property"))
|
||||
# ⚠️ THE ONE THAT DOES NOT BITE, AND IT IS STATED RATHER THAN HIDDEN.
|
||||
MUT.append(("the WEIGHTS replaced by any other non-negative numbers",
|
||||
False,
|
||||
"NOTHING - AND BY DESIGN. That is AC 2: the aggregate trace at the "
|
||||
"meter is identical for every split, so no check here can tell one "
|
||||
"weighting from another by watching the site. The weights are "
|
||||
"graded by what they do to the SHARES (parts 2 and 10), never by "
|
||||
"what they do to the meter - and the fact that nothing at the "
|
||||
"meter can see them is the property, not a gap"))
|
||||
|
||||
for _name, _bites, _where in MUT:
|
||||
print(f" {'caught' if _bites else 'NOT CAUGHT':>10} {_name}")
|
||||
print(f" {_where}")
|
||||
check("the mutations that CAN disarm these guards are each caught by a check "
|
||||
"above - a guard whose checks survive its own defeat is not a guard. "
|
||||
"Every row here was RUN through tools/mutation_run.sh on a purged tree, "
|
||||
"not reasoned about: three of them were reported as caught by an earlier "
|
||||
"draft of this table and were not",
|
||||
all(b for _n, b, _w in MUT[:-3]))
|
||||
check("...and the three that are NOT caught are reported as such, with the "
|
||||
"reason each one cannot be. Two are properties delivered somewhere other "
|
||||
"than the line the mutation touches; the third is the acceptance "
|
||||
"criterion itself - a weighting that changed the aggregate trace would be "
|
||||
"a FAILURE of AC 2, and part 8 is the line that would go red",
|
||||
all(b is False for _n, b, _w in MUT[-3:]))
|
||||
|
||||
|
||||
print()
|
||||
if fails:
|
||||
print(f"{len(fails)} FAILED: {', '.join(fails)}")
|
||||
sys.exit(1)
|
||||
print("all checks passed")
|
||||
Reference in New Issue
Block a user