DEV-02: merge release/1.0, and close the two review blockers
checks / unit (pull_request) Successful in 4m15s
checks / unit (pull_request) Successful in 4m15s
PR #43 was rejected on two findings and had gone unmergeable behind SAFETY-28 and the ALLOC-01 fix. This is the merge commit; the conflict resolution and both fixes are below, because a merge that also changes behaviour has to say so. THE MERGE, AND WHAT IT COST =========================== Two conflicts in main.py, both where SAFETY-28 and this card touched the same method: * `write_setpoint()` split into a site entry point plus a per-unit `_write_unit()` here, while SAFETY-28 put its record gate in the old single-unit body. `write_refusal()` now takes the INVERTER it is about. Asking it with `self.unit` - as release/1.0 does - would authorise A's share on B's wire, and would also trip test_inverter.py part 1's AST scan, which goes red on any read of a Controller N=1 view inside Controller. * the SAFETY-28 gate sits above the clamp and below the non-finite coercion, exactly where release/1.0 put it, and is now asked about `inv`. Fallout the merge produced in the checks, re-aimed rather than relaxed: * every fixture that calls `write_setpoint()` DIRECTLY - the clamp probe, the hung-heartbeat experiment and its serialised counterfactual, the split deadline probe - now arms a real allocation record first. test_inverter.py grows an `arm()` built through the shipped `resolve()`, the same shape test_clamp.py's is: the per-unit envelopes are filed as real `supervised` claims and the site target is their sum, so the water-fill has exactly one answer and the fixture cannot quietly become its own allocator. * test_clamp.py's two-unit failsafe fixture assigned `c.units`, which DEV-02 made a derived property with no setter. It appends a real `Inverter`. BLOCKER 1 - AC 4's ARBITER-BOUND EVIDENCE WAS VACUOUS ===================================================== test_peakguard.py claimed "each unit's `supervised` bound is ITS OWN `max_w` - give inverter B a different rating and the claim filed on inverter B moves with it", and compared B's bound against `_b2.max_w`. `second_inverter()` DEFAULTED B's rating to `LIVE_MAX_W`, which is A's. IT COMPARED (-5000, 5000) AGAINST (-5000, 5000): a number against itself, unable to observe the failure it named. Reproduced: filing the per-unit `device`/`supervised` claims from `self.inverters[0]`'s numbers while leaving `actuator=self.actuator_of(..., inv)` alone left ALL 19 FILES GREEN. At a roster of two with A=5000/B=3000 that makes inverter B's planned envelope (-5000, 5000) instead of (-3000, 3000) - a 2000 W over-command the arbiter believes is supervised. It is a DIFFERENT defect from the actuator variant the static routing pin catches, and only the actuator variant was in the mutation table. * `second_inverter()` gives B 3000 W - a hypothesis, marked as one - for every fixture in the file, so no check there can compare B against A by accident. * the claim is asserted against LITERAL numbers rather than against an expression that can read the same object twice, for `supervised` AND for `device` (whose `dev` had the same defect), plus the envelope the ARBITER RESOLVED for B - a claim filed right and resolved wrong is the same defect one layer down. * a PRECONDITION check fails if the two ratings are ever made equal again. * the BOUND mutation is in the table, beside the actuator one, and was observed RED (3 checks in test_peakguard.py) via tools/mutation_run.sh. ⚠️ THIRD INSTANCE THIS SESSION of a check whose DATA cannot reach the failure it names - ARB-03's call-site scan saw 3 of 8 appends, ALLOC-01's replay generator saw 0 escapes where a widened one saw 39,991. MUTATION.md gains a section for it beside the stale-bytecode and masking ones, and the rule is written at the line: ANY CHECK ASSERTING "X DIFFERS FROM Y" MUST BE RUN ONCE WITH X AND Y ACTUALLY MADE DIFFERENT. BLOCKER 2 - THE LATCH WAS SILENTLY DISARMED BY THE ROLLBACK ROUND TRIP ====================================================================== store.py's rule 2 keeps the flat keys "so a rollback still finds its latch". The operator path that rule contemplates is a ROUND TRIP, and this card lost the latch on it: 1. install migrates -> schema_version=1, unit/inverter-a/... = False 2. operator DOWNGRADES; SAFETY-02 trips inside the downgrade window and the old add-on writes only the flat `sign_tripped: true` 3. operator upgrades again -> `rep.ran` is False, so `_grade_store_migration()` returned early, and `Inverter.__init__` read the namespaced key: False Observed: the controller came up with `sign_wd.tripped = False` while /data/state.json said `sign_tripped: true`. That is store.py's own header sentence - "the file still says sign_tripped: true, the banner is green, and the controller resumes driving the wrong way" - rebuilt by the version marker. A firmware version change with a rollback path was performed on this site on 2026-09-02, so this is not hypothetical. Three changes, each graded by a mutation observed RED: * THE OPERATOR'S CLEAR CLEARS BOTH SPELLINGS. That is what removes the "re-arm forever" objection the `rep.ran` gate existed to answer: with the fossil cleared, `flat True + namespaced False` is unambiguously a downgrade-window latch. * A TRIP MIRRORS THE FLAT PAIR. Rule 2 only ever covered the latch present AT MIGRATION TIME - nothing flat was written for a trip taken afterwards, so an operator who downgraded found `sign_tripped: false` and came up DRIVING. store.py claimed the staleness could only fail toward a SPURIOUS latch. It could not; that sentence is corrected rather than left standing. * THE GUARD RUNS ON EVERY START, and asks the STORE - not the roster - whether anything namespaced is latched. A mirrored trip on B must not re-arm a healthy A, and the store is the right place to ask because it holds every `unit/*/sign_tripped` this install has written, including one belonging to a unit that is not in today's roster. Graded by the three-step scenario itself, run end to end in test_inverter.py part 2, with all three preconditions asserted - including that the catching start did NOT migrate anything, which is what used to skip the guard. Part 2's idempotence check now PRESSES the button instead of hand-writing the store, because the state it used to construct is not one the shipped clear path can produce. Part 3 grades the mirror and the clear on a real roster of two. test_watchdog.py's "the flat key is NOT written" assertion is re-aimed rather than deleted: its argument was right about the READ and wrong about the WRITE. Nothing at runtime reads that key, and the one thing that does ignores it whenever any namespaced latch is set - which a sibling's trip always leaves. What its absence actually cost was the rollback. HANDOVER.md and DOCS.md said the flat key "is never read again", which was the instruction an operator clearing a trip by hand would follow. Both corrected: it is a maintained rollback view, it IS read on every start, and clearing a trip by hand means clearing both spellings. MUTATIONS THIS ROUND, each applied on a purged tree via tools/mutation_run.sh and observed RED: * per-unit `device`/`supervised` BOUNDS from `self.inverters[0]`, actuator left correct -> test_peakguard.py 10g * `_grade_store_migration()` gated on `rep.ran` -> test_inverter.py part 2 * the operator's clear leaving the flat keys set -> test_inverter.py part 2/3 * a trip not mirroring the flat pair -> test_inverter.py part 3 * the guard asking only `self.inverters[0]` -> test_inverter.py part 3 19/19 files green on the merged tree. No hardware was touched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BwRLw7eKYj2byVdwB6kbjU
This commit is contained in:
@@ -64,6 +64,70 @@ the P1 reading, the site integrator, and the tariff quarter.
|
||||
two-unit figure above is architecture, not a measurement of a second device;
|
||||
the second rating in the checks is marked as a hypothesis.
|
||||
|
||||
**The write path is gated on the allocation record, not on how many config keys
|
||||
exist (SAFETY-28).** specs §1.5 makes *"any configuration in which two writers
|
||||
can reach one actuator"* a non-goal. Until now that non-goal was enforced by
|
||||
`len(validate.ACTUATOR_WRITE_KEYS) == 1` - there is exactly one option key, so a
|
||||
second writer is not expressible in the schema. True, and a statement about **the
|
||||
shape of the options schema rather than about the writes**: add a per-inverter
|
||||
config (CFG-04) and there are two real writers with that length still 1, so the
|
||||
check stays green while the property it protects is gone. `sim/inject.py`'s
|
||||
`two_writers` scenario asserted on the same tuple and went green with it.
|
||||
|
||||
* **The enforcement moved onto the writes.** `write_setpoint()` now refuses any
|
||||
value that is not in **this tick's** allocation record from ALLOC-01:
|
||||
`Controller.write_refusal()` asks `Allocation.authorises()` whether the single
|
||||
allocator placed exactly this number, for this unit, on this tick. A second
|
||||
writer with arithmetic of its own cannot satisfy that - its number appears in
|
||||
no record - so it has to file a `Claim` and go through `resolve()`, which is
|
||||
the one allocator. "Exactly one allocator per shared resource" stops being a
|
||||
convention and becomes something the write path checks.
|
||||
* **A refusal is a refusal, not a log line.** The unauthorised value is replaced
|
||||
with **0 W and written**. Returning instead would leave the inverter latched
|
||||
on its last command with the ESP32 heartbeat still being fed - holding an
|
||||
unauthorised setpoint quietly, which is the outcome the gate exists to prevent.
|
||||
* **A stale record cannot be replayed.** Every record now carries the `tick` it
|
||||
was made for, handed *in* by the caller so `allocator.plan()` stays the pure
|
||||
function `test_alloc.py` part 10 grades. The counter advances **once per
|
||||
resolution, not once per loop iteration**: a new allocation makes the previous
|
||||
record stale immediately, while the "inputs missing, not yet stale" hold -
|
||||
which returns before the allocator runs, so one dropped meter reading does not
|
||||
zero the inverter - leaves the standing authorisation intact for the heartbeat.
|
||||
An **unstamped** record authorises nothing; "I cannot say when I was made"
|
||||
fails closed.
|
||||
* **⚠️ 0 W IS AUTHORISED UNCONDITIONALLY, SO THE FAILSAFE CANNOT DEADLOCK BEHIND
|
||||
THE GATE.** `write_setpoint()` is also how layer 2 commands zero, and every
|
||||
path that does so - `cycle()`'s two refusal branches, `shutdown()`, the
|
||||
operator's stop button - runs while the allocator has *refused*. A gate that
|
||||
asked the allocator's permission to command zero would block the safety write
|
||||
behind the very component whose failure the safety write answers. The
|
||||
exemption is on the **value**, not on a `failsafe=True` flag a caller asserts,
|
||||
and the argument is that the hazard §1.5 names is N-times loop gain from
|
||||
*broadcast*: at `S = 0` the broadcast and the correct allocation coincide -
|
||||
`a_i = 1` for every unit gives every unit 0 W, which is exactly its share - so
|
||||
there is no over-command to make at zero. Driven end to end through the real
|
||||
refusal branch in `test_clamp.py` part 7c.
|
||||
* **`unmet_w` is still not `ok`.** The gate reads `ok` and the unit's share and
|
||||
never `unmet_w`, because an allocation that could not place every watt is
|
||||
still safe to write; fusing them would let one saturated inverter park the
|
||||
whole site. Graded on a record with 3800 W unmet.
|
||||
* **`ACTUATOR_WRITE_KEYS` is replaced by `actuator_writers()`**, which counts
|
||||
**writers per actuator** rather than option keys, and finds them by walking
|
||||
the options tree rather than by looking for a container name CFG-04 has not
|
||||
chosen yet. Two inverters with two entities are accepted - that is what the
|
||||
per-inverter roster is *for*; two declarations aimed at one entity are refused,
|
||||
naming the actuator and every writer pointed at it. The tuple survives only as
|
||||
the enumeration a census needs, and nothing asserts on its length any more.
|
||||
* **What neither check observes, said out loud.** The census sees *configured*
|
||||
writers, so a second write path added in **code** is invisible to it - exactly
|
||||
as it was invisible to the tuple. That half is closed at runtime by the record
|
||||
gate, which does not care what the options look like or who called the method.
|
||||
* Verified by breaking it: seven mutations on a purged tree via
|
||||
`tools/mutation_run.sh` - removing the gate, making the zero exit an amnesty,
|
||||
dropping the tick comparison, deleting the census refusal, fusing `unmet_w`
|
||||
into `ok`, freezing the tick on the live path, and moving the gate below the
|
||||
clamp - each turn `test_clamp.py` or `test_validate.py` red.
|
||||
|
||||
**The site grid target is now ALLOCATED across N inverters, sum-invariant, and
|
||||
never broadcast (ALLOC-01).** `ARB-03` left `allocate()` as a documented seam
|
||||
that passed through at N<=1 and DECLINED at N>=2; this fills it. The new
|
||||
|
||||
Reference in New Issue
Block a user