SAFETY-56: the gate cannot tell a dead register from a pack that cannot comply, so stop saying it can (#112)
Text only, no behaviour change. Three operator-facing sentences stop asserting a dead register where the gate cannot distinguish a dead register from a pack the BMS is refusing. Reviewed on the PR: behaviour byte-identical (trace tool sha256 6030175ed2ab reproduced on both trees, plus AST identity with string constants normalised); five mutations re-applied on purged trees, all matching claimed named-red counts; SoC of the live episode independently measured at 11 percent; CI green traced to PRNUM 112 / BASEREF release/1.0.
This commit was merged in pull request #112.
This commit is contained in:
@@ -0,0 +1,181 @@
|
||||
# SAFETY-56 — what the gate cannot tell apart, said in the sentence
|
||||
|
||||
**Text only. No behaviour changes in this card**, and §5 is the measurement that
|
||||
says so: the same stimuli through the tree before and after produce a
|
||||
**byte-identical** trace of every verdict, every `reading()`, every `inputs_ok`
|
||||
and every readiness row's `(ok, warn)`.
|
||||
|
||||
---
|
||||
|
||||
## 1. The defect
|
||||
|
||||
0.10.1 is regulating a real GW5000S-BP. Two messages tell the operator that
|
||||
healthy hardware has failed.
|
||||
|
||||
**The log line**, as emitted on the reference site on 2026-09-21:
|
||||
|
||||
> SAFETY-37: inverter-a battery-power register **is not following its own
|
||||
> command** - STALE_READING: -3 unchanged for 36 s while the standing command
|
||||
> moved 800 W to +1600 W - **the reading is not following**, so it is reported
|
||||
> as MISSING rather than as a measurement … Treating it as MISSING, which
|
||||
> commands 0 W.
|
||||
|
||||
**The readiness row**, at the same moment:
|
||||
|
||||
> NOT READY — battery power: `sensor.kelder_goodwe_master_stage1_goodwe_inverter_ac_power`
|
||||
> **is missing or not numeric**
|
||||
|
||||
That entity was present, numeric and updating.
|
||||
|
||||
**SAFETY-37's conjunction is correct and is not touched by this card** —
|
||||
`unchanged > 35 s AND |command| > 250 W AND |travel| > 250 W`. A register
|
||||
genuinely stuck against a real command is exactly what it should catch, and a
|
||||
pack that cannot comply is a state the site must stop in too. What was wrong is
|
||||
what the sentences **concluded** from it.
|
||||
|
||||
## 2. Two worlds satisfy the conjunction
|
||||
|
||||
| | the register | the pack |
|
||||
|---|---|---|
|
||||
| **DEAD** | has stopped reporting reality | is doing what it was told |
|
||||
| **REFUSED** | is reporting reality correctly | cannot comply — the BMS is refusing at its floor |
|
||||
|
||||
A refused pack holds still under any setpoint, so an honest register publishes
|
||||
the same unchanged number a dead one does. **Nothing `freshness.py` is handed
|
||||
separates them.** All three sentences asserted DEAD.
|
||||
|
||||
## 3. The live episode was REFUSED, and it is measured, not argued
|
||||
|
||||
Off the committed capture `scenarios/safety57-2026-09-21/bus-a-2026-09-21-1030-1110.log.gz`,
|
||||
whose bytes and decoder are already graded by `test_freshness.py` part 10a:
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| the register | answered **-3 W for 850 s**, 10:51:24 → 11:05:34 |
|
||||
| the commands during that hold | **+260, +660, +1060 W** — discharge only, never a charge |
|
||||
| pack SoC throughout | **11 %** |
|
||||
| first **charge** command after the restart | 11:05:31 at **-400 W** |
|
||||
| the register moves | **11:05:34** — **3 s**, inside one 17.0 s obligation window |
|
||||
|
||||
**A register that answers a reversed command inside one obligation window had
|
||||
not stopped reporting.** What would not move was the pack. The sentence the
|
||||
operator read named the one thing in the loop that was telling the truth.
|
||||
|
||||
⚠️ What this does **not** establish: that no register is ever intermittently
|
||||
wrong. It excludes a register that had simply stopped; it cannot exclude one
|
||||
that was wrong and then right. That is the point — the new sentence claims
|
||||
neither.
|
||||
|
||||
## 4. The fix, and why it is three sentences and not one helper
|
||||
|
||||
Each message states **what was observed** and names **both** explanations.
|
||||
|
||||
| where | before | after |
|
||||
|---|---|---|
|
||||
| `app/freshness.py` `_grade()` | *"…+1600 W - the reading is not following, so it is reported as MISSING…"* | *"…+1600 W. **TWO THINGS LOOK LIKE THIS AND THIS GATE CANNOT TELL THEM APART**: the register may have stopped reporting reality, or the source may be unable to comply with the command - a pack the BMS is refusing holds still under any setpoint, and an honest register then reads exactly like a frozen one. Either way the number cannot be read as this command's effect, so it is reported as MISSING…"* |
|
||||
| `app/main.py` `_read_unit()` | *"SAFETY-37: %s battery-power **register is not following its own command** - %s."* | *"SAFETY-37: %s battery-power reading **did not move under a command that did, WHICH IS NOT BY ITSELF A VERDICT ON THE REGISTER** - %s."* |
|
||||
| `app/main.py` `checks()` | *"{label}: {entity} **is missing or not numeric**"* | *"{label}: **no usable value this cycle from** {entity} - **and this row cannot tell which of two things that is**: the entity is missing or not numeric, or it is publishing a number that this controller is withholding (a freshness gate does exactly that, and names itself in a row of its own). Confirm the entity in Developer Tools before replacing it"* |
|
||||
|
||||
**Three sentences, three wordings, no shared helper.** The first two are a log
|
||||
line about a **behaviour**; the third is a banner about a named **entity**, and
|
||||
the two answer different questions ("what did the register do" against "can I
|
||||
trust this entity"). A helper serving both would have to drop whichever half
|
||||
the other caller does not need, and the half it dropped would be the
|
||||
operator's next step. The log line names the pair **once**, inside the `%s` it
|
||||
already interpolates, rather than in both of its own halves.
|
||||
|
||||
**No new input, and SoC is not wired.** `BOUNDS["soc"]` stays *STATED, NOT
|
||||
WIRED*; telling the two worlds apart needs the pack floor (SAFETY-32's number)
|
||||
and SoC (TEL-08's wiring), and a message honest about its own ambiguity needs
|
||||
neither. Part 11b drives the two worlds at **50 %** and **11 %** SoC and
|
||||
asserts the sentence does not move one byte.
|
||||
|
||||
**The readiness row does not branch.** `inv.batt_fresh.stale` is on the same
|
||||
object at the same moment, and the row deliberately does not ask it: the same
|
||||
loop renders the grid and SoC rows, which have no gate, and a branch per row
|
||||
would be a second place where "why is this None" is decided. The gate already
|
||||
has a surface — `stale_note()` rides `liveness_notes()` a few rows below with
|
||||
the whole STALE_READING sentence in it — so the operator's discriminator is
|
||||
*"is that row there?"*, and part 11d asserts that row is **present in REFUSED
|
||||
and absent in ABSENT**.
|
||||
|
||||
## 5. Behaviour is byte-identical, measured
|
||||
|
||||
`tools/safety56_behaviour_trace.py` prints two documents from one stimulus set.
|
||||
The `behaviour` half contains **no sentence**: only `stale`, `reading()`,
|
||||
`releases`, `held`, the window bookkeeping, `inputs_ok`, and every readiness
|
||||
row's `(ok, warn)`. Run in the CI image, purged, `:ro`, against
|
||||
`origin/release/1.0` **archived out of git** and against this branch:
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| the committed live capture | **2390 reads**, 7 verdict edges |
|
||||
| a swept grid of command × register schedules | **66 cells × 120 reads** — 1060 stale reads, 1309 `MISSING` readings, 6 releases |
|
||||
| six driven controller worlds through the shipped read path | DEAD, REFUSED, ABSENT, HEALTHY, RELEASE, RETRIP — every read's `(batt, inputs_ok, stale)` and every `checks()` row's `(ok, warn)` |
|
||||
| **result** | `6030175ed2ab9a4143e86e89a71d45c8ab041ac1c00121a3e3e023cd2b08996c` **on both trees** |
|
||||
|
||||
⚠️ **AND THE CONTROL IS INSIDE THE TOOL, BECAUSE AN IDENTITY BETWEEN TWO TREES
|
||||
THAT ARE THE SAME TREE IS HABIT 4.** `--compare` refuses to report "behaviour
|
||||
unchanged" unless the `sentences` halves **differ**. This card's first
|
||||
invariance run was exactly that mistake — it archived a branch whose edits were
|
||||
not committed yet, so `before` and `after` were the same code and the identity
|
||||
was perfect and worthless.
|
||||
|
||||
Both of the tool's refusals are **driven**, not asserted:
|
||||
|
||||
| | |
|
||||
|---|---|
|
||||
| the same file compared with itself | `REFUSED: the sentences halves are IDENTICAL…`, exit **2** |
|
||||
| `MOVE_W` 250.0 → 240.0 in the after tree | `BEHAVIOUR MOVED at 'sweep_stale_reads' / 'sweep_missing_reads' / 'sweep_trace'`, exit **1** |
|
||||
| this card | `OK: sentences differ, behaviour is byte-identical.`, exit **0** |
|
||||
|
||||
## 6. The mutation battery
|
||||
|
||||
Each in its own `mktemp`'d copy (habit 18), purged on the host, mounted `:ro`,
|
||||
graded by `tools/mutation_run.sh` in the CI image.
|
||||
|
||||
| | mutation | Δ bytes | named reds |
|
||||
|---|---|---|---|
|
||||
| M1 | `_grade()` reverted to *"the reading is not following"* | -402 | **3** |
|
||||
| M2 | the log line reverted to *"register is not following its own command"* | -80 | **2** |
|
||||
| M3 | the row reverted to *"{entity} is missing or not numeric"* | -619 | **2** |
|
||||
| M4 | *register* and *source* transposed between the two explanations | **0** | **1** |
|
||||
| M5 | the second explanation deleted, the first kept | -216 | **1** |
|
||||
| M6 | *"CANNOT TELL THEM APART"* replaced by *"IN ORDER OF LIKELIHOOD"* | -13 | **1** |
|
||||
| M7 | the REFUSED world's ground truth set to the DEAD world's | 0 | **2** |
|
||||
| M8 | the row's second cause deleted | -309 | **1** |
|
||||
| M9 | `label` and `entity` transposed in the row | **0** | **3** |
|
||||
| M10 | M1 + M2 + M3 together, i.e. exactly what 0.10.1 ships | -1101 | **5** |
|
||||
| M11 | the accusation literals replaced by one that matches nothing | 0 | **1** |
|
||||
|
||||
⚠️ **M9's first run was a defect in this card's own check, and it is the one
|
||||
worth reading.** The row was fetched with `[...][0]`. Transposing `label` and
|
||||
`entity` makes the row unfindable, so the run died on an `IndexError` — a red
|
||||
with **no name attached**, with every check after that line **ungraded**. That
|
||||
is FCST-06's shape exactly. `_s56_row()` now returns a named absence instead of
|
||||
raising, and a precondition grades it: **0 named reds before, 3 after.**
|
||||
|
||||
⚠️ **M11 is the other one aimed inward.** `not any(...)` over an empty list is
|
||||
True, and so is one over three mistyped literals. The positive control runs the
|
||||
same predicate against the three sentences **as 0.10.1 shipped them** and
|
||||
requires it to find an accusation in every one, and every literal to match at
|
||||
least one of them (habit 7: vary one thing from an accepted baseline).
|
||||
|
||||
## 7. What part 11 does not grade
|
||||
|
||||
* It does not show the live episode was a BMS refusal beyond doubt — see §3.
|
||||
* It does not grade English. A sentence that named both explanations and then
|
||||
said something useless about them would pass.
|
||||
* The `no entity configured` branch beside the rewritten row is untouched and
|
||||
ungraded: a blank entity really is the only thing it can be.
|
||||
* The **grid-power and battery-SoC rows** go through the same rewritten line and
|
||||
have no freshness gate today, so for them the second cause is a hypothesis
|
||||
about this controller rather than a live possibility. That is weaker than the
|
||||
battery-power case and is the price of not branching per row. A gate on either
|
||||
signal — TEL-08 would be one — makes it exact.
|
||||
* **SAFETY-58 is not touched** (the first read after a long rest trips before a
|
||||
healthy register could answer), and neither is the 710/790 disagreement
|
||||
between `test_freshness.py` and the changelog. Both are separate cards; the
|
||||
second has a **fourth site** at
|
||||
`DECISIONS/SAFETY-57-the-exit-from-a-stale-verdict.md:274` that a fix written
|
||||
off the PR table alone would miss.
|
||||
@@ -360,6 +360,14 @@ two cards editing one sentence is how one of them silently loses. Only the
|
||||
false, and part 10h has a named check asserting the diagnosis half is still
|
||||
there so that rewrite has to be a deliberate act.
|
||||
|
||||
> ⚠️ **SINCE SUPERSEDED, WHICH IS WHAT THAT CHECK WAS FOR.** [[SAFETY-56]] is
|
||||
> the deliberate act: all three sentences now name **both** explanations and
|
||||
> accuse neither, and part 10h's check is inverted — it requires the accusation
|
||||
> to be **gone**. Nothing else in this section moved; the escape clause above is
|
||||
> still this card's and is untouched by it. See
|
||||
> `DECISIONS/SAFETY-56-what-the-gate-cannot-tell-apart.md`, and
|
||||
> `test_freshness.py` part 11 for the graded pair of worlds.
|
||||
|
||||
**Survivor 5 is older than this card and is not closed by it.** After a long
|
||||
rest the unchanged clock is already past 35 s, so the **first** read carrying a
|
||||
travelled command trips the gate — before the 17.0 s in which a healthy register
|
||||
|
||||
@@ -565,10 +565,44 @@ class Freshness:
|
||||
# and different afterwards, and an operator comparing this line against
|
||||
# a history graph is reading the register.
|
||||
shown_s = self.unchanged_s(now_mono)
|
||||
# ⚠️ SAFETY-56. THE OBSERVATION IS A FACT, THE DIAGNOSIS WAS NOT, AND
|
||||
# THE SENTENCE NOW STOPS WHERE THE EVIDENCE DOES. The conjunction above
|
||||
# is satisfied by TWO disjoint worlds, and nothing this object is handed
|
||||
# separates them:
|
||||
# (1) the register has stopped reporting reality - what the gate was
|
||||
# built for - or
|
||||
# (2) reality is not moving, because the SOURCE cannot comply with
|
||||
# the command. A pack the BMS is refusing at its floor holds
|
||||
# still under any setpoint, and a register reporting that
|
||||
# truthfully publishes the same unchanged number a dead one does.
|
||||
# The live 2026-09-21 episode was (2) - the pack read 11 % for the
|
||||
# whole 850 s hold, the commands were discharge-only, and the register
|
||||
# answered the first CHARGE command within one obligation window
|
||||
# (test_freshness.py 11a measures all three off the committed capture)
|
||||
# - and this sentence asserted (1), which sent the operator to look at
|
||||
# healthy hardware.
|
||||
# Naming both is what the module can honestly say. Naming WHICH would
|
||||
# need SoC and the pack floor - deliberately not this module's inputs
|
||||
# (see the `soc` row in BOUNDS and the docstring's last section), and
|
||||
# TEL-08's and SAFETY-32's numbers rather than this sentence's.
|
||||
#
|
||||
# ⚠️ AND IT IS NOT SHARED WITH `main.py`'s NOT READY ROW, WHICH SAYS
|
||||
# THE SAME AMBIGUITY IN DIFFERENT WORDS ON PURPOSE. This sentence is a
|
||||
# LOG LINE about a behaviour, quoted verbatim by `note()` onto the
|
||||
# status page and by `_read_unit()` into the action log; that one is a
|
||||
# BANNER about a named ENTITY, and the two answer different questions
|
||||
# ("what did the register do" against "can I trust this entity"). One
|
||||
# helper serving both would have to drop whichever half the other does
|
||||
# not need, and the half it dropped would be the operator's next step.
|
||||
self.reason = (
|
||||
f"STALE_READING: {self.held:+.0f} unchanged for {shown_s:.0f} s "
|
||||
f"while the standing command moved {moved_w:.0f} W to "
|
||||
f"{standing_w:+.0f} W - the reading is not following, so it is "
|
||||
f"{standing_w:+.0f} W. TWO THINGS LOOK LIKE THIS AND THIS GATE "
|
||||
f"CANNOT TELL THEM APART: the register may have stopped reporting "
|
||||
f"reality, or the source may be unable to comply with the command "
|
||||
f"- a pack the BMS is refusing holds still under any setpoint, and "
|
||||
f"an honest register then reads exactly like a frozen one. Either "
|
||||
f"way the number cannot be read as this command's effect, so it is "
|
||||
f"reported as MISSING rather than as a measurement (limits: "
|
||||
f"unchanged over {self.bound.unchanged_s:.0f} s, command over "
|
||||
f"{self.bound.move_w:.0f} W and moved by over "
|
||||
|
||||
@@ -1785,13 +1785,28 @@ class Controller:
|
||||
# 0 W it announces in the sentence before is exactly what stops the
|
||||
# register ever being asked to report anything different. The live
|
||||
# site sat in it for 790 s on 2026-09-21 and was freed by a human.
|
||||
# ⚠️ THE DIAGNOSIS HALF IS SAFETY-56'S AND IS DELIBERATELY UNTOUCHED
|
||||
# HERE - "is not following its own command" is wrong in a different
|
||||
# way (a pack the BMS is refusing is not a faulty register) and that
|
||||
# card is rewriting it. Two cards editing one sentence is how one of
|
||||
# them silently loses.
|
||||
_LOG.error("SAFETY-37: %s battery-power register is not following "
|
||||
"its own command - %s. Treating it as MISSING, which "
|
||||
# ⚠️ SAFETY-56 REWROTE THE DIAGNOSIS HALF, WHICH SAFETY-57 LEFT
|
||||
# STANDING ON PURPOSE. It used to open "battery-power register is
|
||||
# not following its own command" - an accusation against a named
|
||||
# piece of hardware, and FALSE on the very episode above. The
|
||||
# pack read 11 % for the whole hold, every command in it was a
|
||||
# DISCHARGE, and the register answered the first CHARGE command
|
||||
# three seconds later - so the BMS was refusing, the register was
|
||||
# publishing that refusal correctly, and the operator was sent to
|
||||
# look at a working sensor. All three numbers are measured off the
|
||||
# committed capture by test_freshness.py part 11a. The gate's
|
||||
# conjunction is right and is NOT touched; only its conclusion was.
|
||||
#
|
||||
# ⚠️ AND THE TWO EXPLANATIONS ARE NAMED ONCE, IN `%s`, NOT TWICE.
|
||||
# This line's own words are the OBSERVATION plus the one thing a
|
||||
# log reader has to be told before acting - that the observation is
|
||||
# not yet a verdict - and `freshness._grade()`'s sentence, which
|
||||
# this line already interpolates, is where the pair is spelled out.
|
||||
# Saying it in both halves of one sentence is how an operator
|
||||
# learns to skim it.
|
||||
_LOG.error("SAFETY-37: %s battery-power reading did not move under "
|
||||
"a command that did, WHICH IS NOT BY ITSELF A VERDICT "
|
||||
"ON THE REGISTER - %s. Treating it as MISSING, which "
|
||||
"commands 0 W. It clears itself the moment the register "
|
||||
"reports a different value, and failing that %.0f s "
|
||||
"after the standing command falls below %.0f W "
|
||||
@@ -4663,8 +4678,38 @@ class Controller:
|
||||
if not entity:
|
||||
out.append({"ok": False, "warn": False, "text": f"{label}: no entity configured"})
|
||||
elif value is None:
|
||||
# ⚠️ SAFETY-56. THIS ROW ASSERTED A FALSE FACT ABOUT A NAMED
|
||||
# ENTITY, WHICH IS THE WORST THING A DIAGNOSTIC CAN DO. It read
|
||||
# "<entity> is missing or not numeric" for ANY None, and one of
|
||||
# the ways this value becomes None is SAFETY-37's freshness gate
|
||||
# withholding a reading that is present, numeric and updating -
|
||||
# `Freshness.reading()` returns None BY DESIGN there. On the
|
||||
# live site on 2026-09-21 the operator opened Developer Tools on
|
||||
# the entity this row named, found it working, and had every
|
||||
# reason to conclude the diagnostics were broken.
|
||||
#
|
||||
# ⚠️ AND IT IS FIXED BY SAYING LESS, NOT BY LOOKING HARDER. The
|
||||
# row could ask `inv.batt_fresh.stale` - it is on the same
|
||||
# object at the same moment - but this loop also renders the
|
||||
# grid and SoC rows, which have no gate, and a branch per row
|
||||
# would be a second place where "why is this None" is decided.
|
||||
# The gate already has a surface of its own: `stale_note()`
|
||||
# rides `liveness_notes()` a few rows below with the whole
|
||||
# STALE_READING sentence in it, so the operator's discriminator
|
||||
# is "is that row there?" and this row's job is only to stop
|
||||
# pre-empting the answer. Same reason the wording is not shared
|
||||
# with `freshness._grade()`: that one is a log line about a
|
||||
# BEHAVIOUR, this one is a banner about an ENTITY.
|
||||
out.append({"ok": False, "warn": False,
|
||||
"text": f"{label}: {entity} is missing or not numeric"})
|
||||
"text": f"{label}: no usable value this cycle from "
|
||||
f"{entity} - and this row cannot tell which "
|
||||
f"of two things that is: the entity is "
|
||||
f"missing or not numeric, or it is "
|
||||
f"publishing a number that this controller "
|
||||
f"is withholding (a freshness gate does "
|
||||
f"exactly that, and names itself in a row "
|
||||
f"of its own). Confirm the entity in "
|
||||
f"Developer Tools before replacing it"})
|
||||
else:
|
||||
out.append({"ok": True, "warn": False, "text": f"{label}: {entity} = {value:g}"})
|
||||
|
||||
|
||||
@@ -35,6 +35,12 @@ module does honour.
|
||||
7. THE POLICY TABLE tells the truth about what is wired.
|
||||
8. THE MEASUREMENT the bound rests on, replayed from the committed capture.
|
||||
9. KNOWN SURVIVORS, graded so they are residuals rather than surprises.
|
||||
10. SAFETY-57's EXIT from the verdict, against the committed live capture.
|
||||
11. SAFETY-56: THE SENTENCE THIS GATE CAN HONESTLY SAY. The conjunction is
|
||||
satisfied by two disjoint worlds - a register that has stopped reporting,
|
||||
and a source that cannot comply - and nothing here separates them. Part
|
||||
11 builds both, shows the verdict is byte-identical across them, and
|
||||
grades the three operator-facing sentences against that ambiguity.
|
||||
|
||||
⚠️ INVERTER B DOES NOT PHYSICALLY EXIST (~2026-09-12; goodwe/NOTES.md §1.1b).
|
||||
Every two-unit case below is two copies of inverter A's behaviour with
|
||||
@@ -1608,12 +1614,17 @@ check("...and the 35.0 s the register is re-graded over is named in the note "
|
||||
"too, because it is what the operator is being told to wait out",
|
||||
f"re-graded over a fresh {BOUNDS['batt'].unchanged_s:.0f} s window"
|
||||
in _rel57[0])
|
||||
check("⚠️ AND THE DIAGNOSIS HALF OF THE STALE LINE IS UNTOUCHED, WHICH IS "
|
||||
"SAFETY-56'S. That card is rewriting 'is not following its own command' "
|
||||
"- the live episode's register was following perfectly and the pack was "
|
||||
"simply empty - and two cards editing one sentence is how one of them "
|
||||
"silently loses. This check is here so that rewrite is a deliberate act",
|
||||
"battery-power register is not following its own command" in _stale57[0])
|
||||
check("⚠️ AND THE DIAGNOSIS HALF IS SAFETY-56'S AND HAS NOW BEEN REWRITTEN, "
|
||||
"WHICH IS WHAT THIS CHECK WAS FOR. It used to require 'battery-power "
|
||||
"register is not following its own command' to still be present, so "
|
||||
"that removing it had to be a deliberate act rather than a side effect "
|
||||
"of editing the escape clause beside it. SAFETY-56 is that act, and the "
|
||||
"requirement is now the inverse: the accusation is GONE from this line "
|
||||
"and part 11 grades what replaced it. The escape clause above is "
|
||||
"SAFETY-57's and is untouched by it",
|
||||
"battery-power register is not following its own command"
|
||||
not in _stale57[0]
|
||||
and "did not move under a command that did" in _stale57[0])
|
||||
check("...and a re-trip's reason names the TWO durations separately, each "
|
||||
"beside its own value, because after a release the verdict's window and "
|
||||
"the register's own unchanged time are different facts",
|
||||
@@ -1630,6 +1641,335 @@ check("...and a re-trip's reason names the TWO durations separately, each "
|
||||
Freshness(BOUNDS["batt"])))
|
||||
|
||||
|
||||
# ==============================================================================
|
||||
print()
|
||||
print("11. SAFETY-56: the sentence this gate can honestly say")
|
||||
# ⚠️ THE SUBJECT OF THIS PART IS A CLAIM, NOT A STRING, AND NOTHING IN IT
|
||||
# CHANGES A DECISION. SAFETY-37's conjunction is correct and is untouched;
|
||||
# what was wrong is what two sentences CONCLUDED from it. The conjunction is
|
||||
# satisfied by two disjoint worlds -
|
||||
#
|
||||
# DEAD the register has stopped reporting reality. The pack really is
|
||||
# doing what it was told; the published number does not say so.
|
||||
# REFUSED the register is honest and the SOURCE cannot comply. The BMS is
|
||||
# refusing at the pack floor, so the pack does nothing whatever the
|
||||
# command asks, and an unchanged reading is the TRUTH.
|
||||
#
|
||||
# - and nothing this module is handed separates them. Three sentences named
|
||||
# DEAD as fact: `freshness._grade()`'s "the reading is not following",
|
||||
# `main.py`'s log line "battery-power register is not following its own
|
||||
# command", and the NOT READY row's "<entity> is missing or not numeric". On
|
||||
# the live 2026-09-21 episode all three were the wrong one of the two, and the
|
||||
# third was the worst because it asserts a false fact about a NAMED entity: the
|
||||
# operator opens Developer Tools, finds it working, and concludes the
|
||||
# diagnostics are broken.
|
||||
#
|
||||
# So the property graded below is not "the new words are present". It is that
|
||||
# the two worlds are REAL AND DIFFERENT (11a on the committed capture, 11b in a
|
||||
# driven pair), that the gate CANNOT separate them (11b), and therefore that a
|
||||
# clause asserting either one is false half the time - which is what makes 11c
|
||||
# and 11d a claim rather than decoration. Habit 4: without 11a and 11b those
|
||||
# two would be substring tests over a sentence this file also wrote.
|
||||
|
||||
# --- 11a. the old diagnosis was FALSE on the site it was printed on ----------
|
||||
# ⚠️ OFF THE COMMITTED CAPTURE, NOT OFF A FIXTURE. Part 10a has already graded
|
||||
# this file's bytes against the manifest and its decoder's sign convention
|
||||
# against the frames, so the three series below are evidence rather than a
|
||||
# story. Every boundary is derived in part 10b from the register's own longest
|
||||
# hold; nothing here is typed.
|
||||
_S56_CMDS_HELD = sorted({_D.held_at(_sp, t)
|
||||
for t in range(int(_HOLD_FROM), int(_PARK))})
|
||||
_S56_SOC_HELD = sorted({_D.held_at(_soc, t)
|
||||
for t in range(int(_HOLD_FROM), int(_HUMAN))})
|
||||
_S56_CHARGE_T, _S56_CHARGE_W = next((t, v) for t, v in _sp
|
||||
if t > _PARK and v < 0.0)
|
||||
_S56_AFTER = _D.held_at(_bt, _REG_MOVES + 5.0)
|
||||
print(f" during the 850 s hold: commands {_S56_CMDS_HELD} W, "
|
||||
f"SoC {_S56_SOC_HELD} %, register {_HOLD_W:+.0f} W")
|
||||
print(f" first CHARGE command {hms(_S56_CHARGE_T)} at "
|
||||
f"{_S56_CHARGE_W:+.0f} W -> register moves {hms(_REG_MOVES)} "
|
||||
f"({_REG_MOVES - _S56_CHARGE_T:.0f} s) to {_S56_AFTER:+.0f} W")
|
||||
check("11a. ⚠️ THE OLD DIAGNOSIS WAS FALSE ON THE ONE SITE IT WAS EVER "
|
||||
"PRINTED ON. Through the whole hold the site asked for DISCHARGE only "
|
||||
"(+260 to +1060 W) out of a pack reading 11 %, and the register answered "
|
||||
"-3 W. Then the first CHARGE command arrives and it moves within ONE "
|
||||
"17.0 s obligation window. A register that answers a reversed command in "
|
||||
"one window had not stopped reporting; what would not move was the PACK",
|
||||
all(v > 0.0 for v in _S56_CMDS_HELD)
|
||||
and min(_S56_CMDS_HELD) == 260.0 and max(_S56_CMDS_HELD) == 1060.0
|
||||
and _S56_SOC_HELD == [11.0] and _HOLD_W == -3.0
|
||||
and _S56_CHARGE_W < 0.0
|
||||
and 0.0 < _REG_MOVES - _S56_CHARGE_T <= F.BATT_OBLIGED_S
|
||||
and _S56_AFTER != _HOLD_W)
|
||||
check("...and the gate was RIGHT to fire anyway, which is why this card touches "
|
||||
"no term of the conjunction. The three limits are still the derived ones "
|
||||
"and the same capture still arms at 10:52:00 with the verdict standing: "
|
||||
"a register genuinely stuck against a real command is exactly what "
|
||||
"SAFETY-37 should catch, and a pack that cannot comply is a state the "
|
||||
"site must stop in too. What was wrong was never the firing",
|
||||
BOUNDS["batt"].unchanged_s == BATT_UNCHANGED_S
|
||||
and BOUNDS["batt"].move_w == MOVE_W
|
||||
and BOUNDS["batt"].release_s == F.BATT_OBLIGED_S
|
||||
and hms(_TRIP) == "10:52:00" and _f_after.releases == 1
|
||||
and next(r for r in _rows_after if r[0] == _TRIP)[1] is True)
|
||||
|
||||
# --- 11b. two worlds, one published stream, one verdict ----------------------
|
||||
# ⚠️ GROUND TRUTH IS WRITTEN DOWN, NOT DERIVED FROM THE PUBLISHED STREAM
|
||||
# (habit 2). A check that computes "what the pack was really doing" out of the
|
||||
# number the register published is comparing a thing with itself, which is the
|
||||
# defect MUTATION.md has recorded fifteen times.
|
||||
_BATT_ENT = "sensor.batt_a"
|
||||
_S56_N = 40
|
||||
_S56_CMD = [800.0 if t < 1 else 1600.0 for t in range(_S56_N)]
|
||||
_S56_PUB = [-3.0] * _S56_N # what the ENTITY publishes, both
|
||||
_S56_TRUE_DEAD = list(_S56_CMD) # the pack obeyed; the register lied
|
||||
_S56_TRUE_REFUSED = [-3.0] * _S56_N # the pack refused; the register told
|
||||
|
||||
|
||||
async def _s56_world(soc_pct):
|
||||
"""The shipped read path at N=1. The ground-truth stream above is never
|
||||
handed to the controller - it is what the WORLD is, not an input."""
|
||||
c, hass = one_site()
|
||||
hass.numbers["sensor.soc_a"] = soc_pct
|
||||
for t in range(_S56_N):
|
||||
hass.numbers[_BATT_ENT] = _S56_PUB[t]
|
||||
c.inverters[0].last_write = _S56_CMD[t]
|
||||
await c.read_inputs(now_mono=float(t))
|
||||
return c, hass
|
||||
|
||||
|
||||
_S56_LOG0 = len(_LOGREC)
|
||||
# ⚠️ THE TWO WORLDS ARE DRIVEN AT DIFFERENT SoC ON PURPOSE - 50 % against the
|
||||
# 11 % the live pack sat at - so that "the sentence did not move" below is a
|
||||
# measurement of this module's `soc` bound being STATED, NOT WIRED, and not an
|
||||
# artefact of both runs being handed the same percentage. Wiring it is TEL-08's.
|
||||
_c56_dead, _h56_dead = run(_s56_world(50.0))
|
||||
_c56_ref, _h56_ref = run(_s56_world(11.0))
|
||||
_pub_dead = [v for e, v in _h56_dead.served if e == _BATT_ENT]
|
||||
_pub_ref = [v for e, v in _h56_ref.served if e == _BATT_ENT]
|
||||
_S56_DIFFER = sum(1 for a, b in zip(_S56_TRUE_DEAD, _S56_TRUE_REFUSED) if a != b)
|
||||
print(f" DEAD truth {_S56_TRUE_DEAD[:2]}... published {_pub_dead[:2]}...")
|
||||
print(f" REFUSED truth {_S56_TRUE_REFUSED[:2]}... published {_pub_ref[:2]}...")
|
||||
check(f"11b. PRECONDITION: the two worlds are REALLY TWO - their ground truth "
|
||||
f"differs on {_S56_DIFFER} of {_S56_N} reads - and the PUBLISHED stream "
|
||||
f"is bit-identical in both, so nothing downstream of {_BATT_ENT} can "
|
||||
f"tell them apart. Without this the rest of part 11 is one world twice",
|
||||
_S56_DIFFER == _S56_N and _pub_dead == _pub_ref == _S56_PUB
|
||||
and len(_pub_dead) == _S56_N)
|
||||
check("...and in REFUSED the register is RIGHT on every one of the 40 reads "
|
||||
"(published == truth) while in DEAD it is wrong on all 40. That is the "
|
||||
"fact the old sentence got backwards: it named the register in a world "
|
||||
"where the register is the only thing telling the truth",
|
||||
_S56_PUB == _S56_TRUE_REFUSED
|
||||
and not any(p == t for p, t in zip(_S56_PUB, _S56_TRUE_DEAD)))
|
||||
_r56_dead = _c56_dead.inverters[0].batt_fresh.reason
|
||||
_r56_ref = _c56_ref.inverters[0].batt_fresh.reason
|
||||
check("⚠️ AND THE GATE FIRES IDENTICALLY IN BOTH, WHICH IS THE WHOLE REASON "
|
||||
"ITS SENTENCE MAY NOT NAME ONE OF THEM: same verdict, same MISSING "
|
||||
"reading, same site stop - and the sentence is BYTE-IDENTICAL across two "
|
||||
"worlds that share no ground truth at all",
|
||||
_c56_dead.inverters[0].batt_fresh.stale is True
|
||||
and _c56_ref.inverters[0].batt_fresh.stale is True
|
||||
and _c56_dead.inverters[0].batt is None
|
||||
and _c56_ref.inverters[0].batt is None
|
||||
and _c56_dead.inputs_ok is False and _c56_ref.inputs_ok is False
|
||||
and _r56_dead == _r56_ref and _r56_dead != "")
|
||||
check("...and the two runs were driven at 50 % and 11 % SoC and the sentence "
|
||||
"did not move one byte, because `BOUNDS['soc']` is STATED, NOT WIRED. A "
|
||||
"message honest about its own ambiguity needs no new input, and adding "
|
||||
"one here would make this sentence depend on a second measurement being "
|
||||
"right - TEL-08's card, not this one",
|
||||
_c56_dead.inverters[0].soc == 50.0 and _c56_ref.inverters[0].soc == 11.0
|
||||
and _r56_dead == _r56_ref)
|
||||
|
||||
# --- 11c. both explanations, and no accusation, on every surface -------------
|
||||
# The two explanations, each tagged with the world it is true OF. The emitted
|
||||
# sentence is the same in both worlds (11b), so a sentence naming only one is
|
||||
# false half the time - which is why BOTH are required, as an ORDERED PAIR
|
||||
# (habit 14): two clauses in one sentence can always be transposed at zero
|
||||
# bytes, and "the register may be unable to comply / the source may have
|
||||
# stopped reporting reality" is a different and wrong claim.
|
||||
_S56_EXPLANATIONS = [
|
||||
("DEAD", "the register may have stopped reporting reality"),
|
||||
("REFUSED", "the source may be unable to comply with the command"),
|
||||
]
|
||||
# ⚠️ WHAT THE THREE SENTENCES USED TO ASSERT. Each is a claim about the
|
||||
# REGISTER or about the ENTITY, and 11a measured the register to be alive on
|
||||
# the live episode while 11d measures the entity to be serving a float. They
|
||||
# are listed with the file they came from so a reviewer can see the set is the
|
||||
# whole set rather than the ones that were easy to find.
|
||||
_S56_ACCUSATIONS = [
|
||||
("app/freshness.py _grade()", "the reading is not following"),
|
||||
("app/main.py _read_unit()", "register is not following its own command"),
|
||||
("app/main.py checks()", f"{_BATT_ENT} is missing or not numeric"),
|
||||
]
|
||||
_log56 = [r.getMessage() for r in _LOGREC[_S56_LOG0:] if "SAFETY-37" in r.getMessage()]
|
||||
|
||||
|
||||
def _s56_row(c):
|
||||
"""The battery-power readiness row, or a NAMED absence - never a raise.
|
||||
|
||||
⚠️ IT MUST NOT RAISE, AND THAT IS FCST-06'S RULE RATHER THAN TIDINESS. The
|
||||
first draft of this part was `[... ][0]`, and the mutation that transposes
|
||||
`label` and `entity` in the row - zero bytes - makes the row unfindable. The
|
||||
run then died on an IndexError with every check after this line UNGRADED:
|
||||
a red with no name attached, which reads like broken infrastructure and gets
|
||||
retried rather than read. Measured: 0 named reds before, 2 after.
|
||||
"""
|
||||
hits = [r for r in c.checks() if r["text"].startswith("battery power")]
|
||||
if len(hits) != 1:
|
||||
return {"ok": None, "warn": None,
|
||||
"text": f"<NO SINGLE `battery power` ROW: {len(hits)} found>"}
|
||||
return hits[0]
|
||||
|
||||
|
||||
_row56_ref = _s56_row(_c56_ref)
|
||||
_S56_SURFACES = {
|
||||
"reason (status page + action log)": _r56_ref,
|
||||
"log line (SAFETY-37 ERROR)": _log56[-1] if _log56 else "",
|
||||
"stale_note() (NOT READY row)": _c56_ref.inverters[0].stale_note(),
|
||||
"checks() battery-power row": _row56_ref["text"],
|
||||
}
|
||||
for _n, _s in _S56_SURFACES.items():
|
||||
print(f" {_n}: {_s[:96]}...")
|
||||
check("PRECONDITION: the readiness row is FINDABLE BY ITS LABEL in both worlds "
|
||||
"- exactly one `battery power` row each - so every row graded below is "
|
||||
"that row, and a mutation that moves `label` out of the first slot is a "
|
||||
"NAMED red here rather than an IndexError three checks later (FCST-06). "
|
||||
f"REFUSED: {_row56_ref['text'][:44]!r}",
|
||||
_row56_ref["ok"] is not None)
|
||||
check("PRECONDITION: all four operator-facing surfaces were really produced by "
|
||||
"this run and are non-empty, so the two quantifiers below are not over "
|
||||
"an empty set - and the log line is the one the SHIPPED read path "
|
||||
"emitted, not one this file formatted. Both worlds emitted one and the "
|
||||
"two are the same string, which is 11b again on the log surface",
|
||||
len(_log56) == 2 and _log56[0] == _log56[1]
|
||||
and all(len(s) > 30 for s in _S56_SURFACES.values())
|
||||
and _r56_ref in _log56[-1])
|
||||
_idx56 = [_r56_ref.find(t) for _w, t in _S56_EXPLANATIONS]
|
||||
check(f"11c. BOTH EXPLANATIONS ARE NAMED, AND IN THAT ORDER: "
|
||||
f"{_S56_EXPLANATIONS[0][1]!r} at {_idx56[0]} then "
|
||||
f"{_S56_EXPLANATIONS[1][1]!r} at {_idx56[1]}. Pinned as an ordered pair "
|
||||
f"because transposing 'register' and 'source' between the two clauses is "
|
||||
f"a zero-byte edit that leaves both words in the sentence (habit 14)",
|
||||
all(i >= 0 for i in _idx56) and _idx56 == sorted(_idx56)
|
||||
and len(set(_idx56)) == len(_idx56))
|
||||
check("...and the sentence says in its own words that it CANNOT choose, rather "
|
||||
"than leaving two explanations side by side for a reader to rank - an "
|
||||
"operator who reads a list picks the first item",
|
||||
"CANNOT TELL THEM APART" in _r56_ref)
|
||||
# ⚠️ THE POSITIVE CONTROL FOR THE `not any(...)` BELOW, AND IT IS NOT OPTIONAL:
|
||||
# a quantifier over an empty list is True, and so is one over three literals
|
||||
# with a typo in each. These are the three sentences as 0.10.1 SHIPPED them,
|
||||
# quoted from the release rather than rebuilt, and the same predicate is
|
||||
# required to FIND an accusation in every one of them (habit 7: vary one thing
|
||||
# from an ACCEPTED baseline).
|
||||
_S56_SHIPPED_010_1 = {
|
||||
"reason": "STALE_READING: -3 unchanged for 35 s while the standing command "
|
||||
"moved 800 W to +1600 W - the reading is not following, so it is "
|
||||
"reported as MISSING rather than as a measurement (limits: "
|
||||
"unchanged over 35 s, command over 250 W and moved by over 250 W)",
|
||||
"log": "SAFETY-37: inverter-a battery-power register is not following its "
|
||||
"own command - STALE_READING: ... Treating it as MISSING, which "
|
||||
"commands 0 W.",
|
||||
"row": f"battery power: {_BATT_ENT} is missing or not numeric",
|
||||
}
|
||||
check(f"POSITIVE CONTROL: the very same predicate, run against the three "
|
||||
f"sentences as 0.10.1 SHIPPED them, finds an accusation in EVERY one - "
|
||||
f"and every one of the {len(_S56_ACCUSATIONS)} literals matches at least "
|
||||
f"one of them, so neither an empty list nor a mistyped literal can make "
|
||||
f"the check below pass by vacuity",
|
||||
len(_S56_ACCUSATIONS) == 3 and len(_S56_EXPLANATIONS) == 2
|
||||
and all(any(t in old for _w, t in _S56_ACCUSATIONS)
|
||||
for old in _S56_SHIPPED_010_1.values())
|
||||
and all(any(t in old for old in _S56_SHIPPED_010_1.values())
|
||||
for _w, t in _S56_ACCUSATIONS))
|
||||
check("⚠️ AND NOT ONE OF THE THREE ACCUSATIONS SURVIVES, ON ANY OF THE FOUR "
|
||||
"SURFACES: " + "; ".join(f"{w} -> {t!r}" for w, t in _S56_ACCUSATIONS)
|
||||
+ ". This is the check that goes red if any of the three sentences is "
|
||||
"reverted, and it is stated over the SURFACES rather than over the "
|
||||
"source files because two of the three are assembled from two modules",
|
||||
not any(t in s for _w, t in _S56_ACCUSATIONS
|
||||
for s in _S56_SURFACES.values()))
|
||||
|
||||
# --- 11d. the NOT READY row that named a working entity ----------------------
|
||||
async def _s56_absent():
|
||||
"""The other half of the row's ambiguity: the entity really is gone."""
|
||||
c, hass = one_site()
|
||||
for t in range(3):
|
||||
hass.numbers[_BATT_ENT] = None # Home Assistant has no state
|
||||
c.inverters[0].last_write = 0.0
|
||||
await c.read_inputs(now_mono=float(t))
|
||||
return c, hass
|
||||
|
||||
|
||||
_c56_abs, _h56_abs = run(_s56_absent())
|
||||
_last_ref = [v for e, v in _h56_ref.served if e == _BATT_ENT][-1]
|
||||
_last_abs = [v for e, v in _h56_abs.served if e == _BATT_ENT][-1]
|
||||
_row56_abs = _s56_row(_c56_abs)
|
||||
print(f" WITHHELD: {_BATT_ENT} served {_last_ref!r}, stale="
|
||||
f"{_c56_ref.inverters[0].batt_fresh.stale} ABSENT: served "
|
||||
f"{_last_abs!r}, stale={_c56_abs.inverters[0].batt_fresh.stale}")
|
||||
check("11d. PRECONDITION: the row's two causes are both REACHED. In REFUSED "
|
||||
f"{_BATT_ENT} served a real float on the last read and the gate is "
|
||||
f"holding the value back; in ABSENT Home Assistant served None and the "
|
||||
f"gate is not armed at all. Two different causes, one `inv.batt is None`",
|
||||
_last_ref == -3.0 and _last_abs is None
|
||||
and _c56_ref.inverters[0].batt_fresh.stale is True
|
||||
and _c56_abs.inverters[0].batt_fresh.stale is False
|
||||
and _c56_ref.inverters[0].batt is None
|
||||
and _c56_abs.inverters[0].batt is None)
|
||||
check("⚠️ AND THE VERDICT IS UNCHANGED BY THIS CARD - both rows are still "
|
||||
"ok=False, warn=False, i.e. still NOT READY. The defect was never the "
|
||||
"pass/fail, it was the row asserting a fact about a named entity that "
|
||||
"was at that moment present, numeric and updating",
|
||||
_row56_ref["ok"] is False and _row56_ref["warn"] is False
|
||||
and _row56_abs["ok"] is False and _row56_abs["warn"] is False
|
||||
and _row56_ref["text"] == _row56_abs["text"])
|
||||
check("...and what it says instead is the observation plus BOTH causes, with "
|
||||
f"{_BATT_ENT} in its own slot - `label` and `entity` are two "
|
||||
f"interpolations in one sentence and swapping them costs zero bytes, so "
|
||||
f"the literal around each is pinned (habit 14)",
|
||||
f"battery power: no usable value this cycle from {_BATT_ENT} - and this "
|
||||
f"row cannot tell which of two things that is" in _row56_ref["text"]
|
||||
and "the entity is missing or not numeric" in _row56_ref["text"]
|
||||
and "a number that this controller is withholding" in _row56_ref["text"])
|
||||
check("⚠️ AND THE DISCRIMINATOR IT POINTS AT EXISTS AND IS SELECTIVE, which is "
|
||||
"why the row does not need to ask `batt_fresh.stale` itself: `checks()` "
|
||||
"carries a STALE_READING row in REFUSED and NONE in ABSENT, so 'is that "
|
||||
"row below?' answers the question this one declines to answer. A row "
|
||||
"that pointed at a surface present in both states would be worse than "
|
||||
"the accusation it replaced",
|
||||
any("STALE_READING" in r["text"] for r in _c56_ref.checks())
|
||||
and not any("STALE_READING" in r["text"] for r in _c56_abs.checks()))
|
||||
check("...and the row's wording is NOT shared with the log line's, which is a "
|
||||
"design choice rather than an omission: the two sentences have no clause "
|
||||
"in common longer than the word 'entity', because one explains a "
|
||||
"BEHAVIOUR to a log reader and the other tells a page reader whether to "
|
||||
"trust a NAME. A shared helper would have to drop whichever half the "
|
||||
"other caller does not need",
|
||||
_S56_EXPLANATIONS[0][1] not in _row56_ref["text"]
|
||||
and _S56_EXPLANATIONS[1][1] not in _row56_ref["text"]
|
||||
and "no usable value this cycle" not in _r56_ref)
|
||||
|
||||
# --- 11e. what part 11 does NOT grade, with its shape (habit 13) -------------
|
||||
# * It does not show the live episode was a BMS refusal beyond doubt. 11a
|
||||
# measures that the register answered a reversed command inside one
|
||||
# obligation window, which excludes a register that had simply stopped; it
|
||||
# does not exclude one that was intermittently wrong. That is the point: the
|
||||
# sentence no longer claims to know either.
|
||||
# * It does not grade ENGLISH. A wording that named both explanations and then
|
||||
# said something useless about them would pass 11c.
|
||||
# * The `no entity configured` branch beside the rewritten row is untouched and
|
||||
# ungraded here - it has no second explanation, because a blank entity really
|
||||
# is the only thing it can be.
|
||||
# * The grid-power and battery-SoC rows go through the same rewritten line and
|
||||
# have no freshness gate today, so for them the second cause is a hypothesis
|
||||
# about this controller rather than a live possibility. That is weaker than
|
||||
# the battery-power case and is the price of not branching per row; a gate on
|
||||
# either of those signals (TEL-08 would be one) makes it exact.
|
||||
|
||||
|
||||
print()
|
||||
if fails:
|
||||
print(f"{len(fails)} FAILED: {', '.join(fails)}")
|
||||
|
||||
@@ -0,0 +1,300 @@
|
||||
"""SAFETY-56's behaviour-invariance instrument. `tools/safety56_behaviour_trace.py`
|
||||
|
||||
SAFETY-56 rewrote three operator-facing sentences and nothing else. This is what
|
||||
says so: it drives a fixed stimulus set through the SHIPPED modules and prints
|
||||
two documents -
|
||||
|
||||
`behaviour` every verdict, every `reading()`, every `releases`, every
|
||||
`inputs_ok` and every readiness row's (ok, warn). NO SENTENCE
|
||||
REACHES IT, so a tree whose only change is wording must produce
|
||||
this document byte for byte.
|
||||
`sentences` the four operator-facing surfaces, from the same stimulus.
|
||||
|
||||
Run it in two trees and compare:
|
||||
|
||||
python3 tools/safety56_behaviour_trace.py > /tmp/after.json
|
||||
python3 tools/safety56_behaviour_trace.py --compare /tmp/before.json /tmp/after.json
|
||||
|
||||
⚠️ THE CONTROL IS PART OF THE TOOL AND NOT A SEPARATE STEP, WHICH IS MUTATION.md
|
||||
HABIT 4 IN AN INSTRUMENT. `--compare` REFUSES to report "behaviour unchanged"
|
||||
unless the `sentences` halves DIFFER. Without that, comparing a tree with itself
|
||||
- which this card's first run did, by archiving a branch whose edits were not
|
||||
committed yet - gives a perfect result that means nothing. An identity is
|
||||
evidence only when the two sides could have differed, and ARCH-02's rehearsal
|
||||
harness is the worked example of what happens when nobody checks.
|
||||
|
||||
⚠️ IT GRADES BEHAVIOUR, NEVER WORDING. Two trees that agree here can still print
|
||||
different sentences - that is the point. `test_freshness.py` part 11 grades the
|
||||
sentences themselves.
|
||||
|
||||
⚠️ WHAT IT CANNOT SEE, with shapes (habit 13): anything outside `freshness.py`'s
|
||||
verdict, `_read_unit()`'s gating and `checks()`'s rows; a roster of more than
|
||||
one; the MQTT and ingress surfaces; and wall-clock behaviour, since every clock
|
||||
here is the caller's monotonic argument. It is a pin on the three things this
|
||||
card is forbidden to move, not a full behavioural equivalence.
|
||||
|
||||
⚠️ PURGE BEFORE USE on a tree you have just edited. `tools/mutation_run.sh`
|
||||
does, and MUTATION.md says why `python3 -B` alone does not.
|
||||
"""
|
||||
import asyncio
|
||||
import hashlib
|
||||
import importlib.util
|
||||
import json
|
||||
import logging
|
||||
import sys
|
||||
from pathlib import Path
|
||||
|
||||
HERE = Path(__file__).resolve().parent.parent # the add-on directory
|
||||
sys.path.insert(0, str(HERE))
|
||||
|
||||
BOUNDS = Freshness = Controller = DEFAULTS = None
|
||||
|
||||
|
||||
def _load():
|
||||
"""The add-on's modules, imported LAZILY so that `--compare` runs anywhere.
|
||||
|
||||
⚠️ NOT A STYLE CHOICE. `--compare` is the half a reviewer runs on a laptop,
|
||||
against two JSON files, in a directory that has no `app/` in it - and a
|
||||
top-level import would make the comparison impossible exactly where it is
|
||||
most useful.
|
||||
"""
|
||||
global BOUNDS, Freshness, Controller, DEFAULTS
|
||||
from app.freshness import BOUNDS, Freshness # noqa: E402,F401
|
||||
from app.main import Controller # noqa: E402,F401
|
||||
from app.store import DEFAULTS # noqa: E402,F401
|
||||
|
||||
A = 5000.0
|
||||
ONE = dict(meter_source="off", meter_entity="sensor.grid",
|
||||
setpoint_entity="number.sp_a", soc_entity="sensor.soc_a",
|
||||
batt_entity="sensor.batt_a", max_w=A, gain=0.6, slew_w=0,
|
||||
deadband_w=15, target_grid_w=0, step_w=10, heartbeat_s=10,
|
||||
stale_input_s=15, inverters=[], bms_soc_floor=10)
|
||||
|
||||
|
||||
class MemStore:
|
||||
def __init__(self, d=None):
|
||||
self.data = dict(DEFAULTS, **(d or {}))
|
||||
|
||||
def set(self, k, v):
|
||||
self.data[k] = v
|
||||
|
||||
def get_time(self, *a):
|
||||
return None
|
||||
|
||||
def set_time(self, *a):
|
||||
pass
|
||||
|
||||
|
||||
class Pub:
|
||||
enabled = False
|
||||
|
||||
def publish(self, *a, **k):
|
||||
pass
|
||||
|
||||
def close(self):
|
||||
pass
|
||||
|
||||
|
||||
class Hass:
|
||||
def __init__(self, numbers=None, limits=None):
|
||||
self.numbers = dict(numbers or {})
|
||||
self.limits_by = dict(limits or {})
|
||||
self.served = []
|
||||
self.writes = []
|
||||
|
||||
async def number(self, entity, invert=False):
|
||||
v = self.numbers.get(entity)
|
||||
self.served.append((entity, v))
|
||||
return None if v is None else (-v if invert else v)
|
||||
|
||||
async def limits(self, entity):
|
||||
return self.limits_by.get(entity, (None, None, None))
|
||||
|
||||
async def set_number(self, entity, value):
|
||||
self.writes.append((entity, value))
|
||||
return True
|
||||
|
||||
async def call(self, domain, service, data):
|
||||
return True
|
||||
|
||||
|
||||
def one_site(soc=50.0):
|
||||
hass = Hass({"sensor.grid": 0.0, "sensor.soc_a": soc,
|
||||
"sensor.batt_a": -1200.0},
|
||||
{"number.sp_a": (-A, A, 1.0)})
|
||||
c = Controller(dict(ONE), hass, MemStore(), Pub(), stop=asyncio.Event())
|
||||
c.inverters[0].dev_min, c.inverters[0].dev_max = -A, A
|
||||
return c, hass
|
||||
|
||||
|
||||
async def _world(name, soc, reg_of, cmd_of, n):
|
||||
c, hass = one_site(soc)
|
||||
seen = []
|
||||
for t in range(n):
|
||||
hass.numbers["sensor.batt_a"] = reg_of(t)
|
||||
c.inverters[0].last_write = cmd_of(t)
|
||||
await c.read_inputs(now_mono=float(t))
|
||||
seen.append([c.inverters[0].batt, c.inputs_ok,
|
||||
c.inverters[0].batt_fresh.stale])
|
||||
return {"name": name, "reads": seen,
|
||||
"rows": [[r["ok"], r["warn"]] for r in c.checks()],
|
||||
"n_rows": len(c.checks()), "events": len(c.events),
|
||||
"inputs_bad": c.inputs_bad_since is not None,
|
||||
"releases": [i.batt_fresh.releases for i in c.inverters]}
|
||||
|
||||
|
||||
# The command and register schedules. Each of the conjunction's three terms is
|
||||
# exercised alone and with the others, and the last two schedules take a verdict
|
||||
# all the way through SAFETY-57's release and back into a re-trip.
|
||||
CMDS = [lambda t: 0.0, lambda t: 1300.0, lambda t: -1200.0,
|
||||
lambda t: 1300.0 if t >= 1 else -1200.0,
|
||||
lambda t: 249.0 if t >= 1 else 0.0,
|
||||
lambda t: 251.0 if t >= 1 else 0.0,
|
||||
lambda t: 1300.0 if t < 40 else 0.0,
|
||||
lambda t: 5.0 if t >= 1 else 1300.0,
|
||||
lambda t: (t % 7) * 200.0 - 600.0,
|
||||
lambda t: (-1200.0 if t < 1 else 1300.0) if t < 45 else (
|
||||
0.0 if t < 90 else 1300.0),
|
||||
lambda t: (-1200.0 if t < 1 else 1300.0) if t < 45 else 100.0]
|
||||
REGS = [lambda t: -3.0, lambda t: -1200.0, lambda t: -1200.0 + (t % 3),
|
||||
lambda t: None if t % 5 == 0 else -1200.0,
|
||||
lambda t: 0.0, lambda t: float((t * 37) % 11) - 5.0]
|
||||
|
||||
WORLDS = [
|
||||
("DEAD", 50.0, lambda t: -3.0, lambda t: 800.0 if t < 1 else 1600.0, 40),
|
||||
("REFUSED", 11.0, lambda t: -3.0, lambda t: 800.0 if t < 1 else 1600.0, 40),
|
||||
("ABSENT", 50.0, lambda t: None, lambda t: 0.0, 3),
|
||||
("HEALTHY", 50.0, lambda t: -1200.0 + (t % 3),
|
||||
lambda t: 1300.0 if t % 2 else -1200.0, 60),
|
||||
("RELEASE", 50.0, lambda t: -1200.0,
|
||||
lambda t: (-1200.0 if t < 1 else 1300.0) if t < 40 else 0.0, 60),
|
||||
("RETRIP", 50.0, lambda t: -1200.0,
|
||||
lambda t: (-1200.0 if t < 1 else 1300.0) if t < 40 else
|
||||
(0.0 if t < 80 else 1300.0), 130),
|
||||
]
|
||||
|
||||
|
||||
def behaviour():
|
||||
"""Everything this card is forbidden to move. No sentence may enter it."""
|
||||
_load()
|
||||
logging.disable(logging.CRITICAL)
|
||||
out = {}
|
||||
|
||||
# 1. the committed live capture, read by read.
|
||||
spec = importlib.util.spec_from_file_location(
|
||||
"_s56decode", HERE / "tools" / "decode_bus_capture.py")
|
||||
dec = importlib.util.module_from_spec(spec)
|
||||
spec.loader.exec_module(dec)
|
||||
cap_file = (HERE / "scenarios" / "safety57-2026-09-21"
|
||||
/ "bus-a-2026-09-21-1030-1110.log.gz")
|
||||
events, _census = dec.decode(cap_file)
|
||||
sp, bt = dec.series(events, "setpoint_w"), dec.series(events, "batt_w")
|
||||
f = Freshness(BOUNDS["batt"])
|
||||
t = float(int(max(sp[0][0], bt[0][0])) + 1)
|
||||
t1 = int(min(sp[-1][0], bt[-1][0]))
|
||||
cap = []
|
||||
while t <= t1:
|
||||
f.submit(dec.held_at(bt, t), dec.held_at(sp, t), t)
|
||||
cap.append([t, f.stale, f.reading(), f.releases, f.held,
|
||||
f.rested_since, f.graded_from, f.standing_at_grade,
|
||||
f.released_at])
|
||||
t += 1.0
|
||||
out["capture_reads"] = len(cap)
|
||||
out["capture_trace"] = hashlib.sha256(
|
||||
json.dumps(cap, sort_keys=True).encode()).hexdigest()
|
||||
out["capture_edges"] = [r[:4] for i, r in enumerate(cap)
|
||||
if i == 0 or r[1] != cap[i - 1][1]]
|
||||
|
||||
# 2. the swept grid over the policy object.
|
||||
sweep = []
|
||||
for ci, cf in enumerate(CMDS):
|
||||
for ri, rf in enumerate(REGS):
|
||||
g = Freshness(BOUNDS["batt"])
|
||||
row = []
|
||||
for n in range(120):
|
||||
g.submit(rf(n), cf(n), float(n))
|
||||
row.append([g.stale, g.reading(), g.releases])
|
||||
sweep.append([ci, ri, row])
|
||||
out["sweep_cells"] = len(sweep)
|
||||
out["sweep_trace"] = hashlib.sha256(
|
||||
json.dumps(sweep, sort_keys=True).encode()).hexdigest()
|
||||
out["sweep_stale_reads"] = sum(1 for _c, _r, row in sweep
|
||||
for s, _v, _n in row if s)
|
||||
out["sweep_missing_reads"] = sum(1 for _c, _r, row in sweep
|
||||
for _s, v, _n in row if v is None)
|
||||
out["sweep_releases"] = sum(row[-1][2] for _c, _r, row in sweep)
|
||||
|
||||
# 3. the shipped read path and every readiness row's verdict.
|
||||
loop = asyncio.new_event_loop()
|
||||
out["worlds"] = [loop.run_until_complete(_world(*w)) for w in WORLDS]
|
||||
loop.close()
|
||||
return out
|
||||
|
||||
|
||||
def sentences():
|
||||
"""The four operator-facing surfaces, from the REFUSED world."""
|
||||
_load()
|
||||
recs = []
|
||||
|
||||
class _H(logging.Handler):
|
||||
def emit(self, record):
|
||||
recs.append(record.getMessage())
|
||||
|
||||
logging.disable(logging.NOTSET)
|
||||
log = logging.getLogger("goodwe")
|
||||
log.addHandler(_H())
|
||||
log.setLevel(logging.DEBUG)
|
||||
|
||||
async def go():
|
||||
c, hass = one_site(11.0)
|
||||
for t in range(40):
|
||||
hass.numbers["sensor.batt_a"] = -3.0
|
||||
c.inverters[0].last_write = 800.0 if t < 1 else 1600.0
|
||||
await c.read_inputs(now_mono=float(t))
|
||||
return c
|
||||
|
||||
loop = asyncio.new_event_loop()
|
||||
c = loop.run_until_complete(go())
|
||||
loop.close()
|
||||
return {
|
||||
"reason": c.inverters[0].batt_fresh.reason,
|
||||
"log": [m for m in recs if "SAFETY-37" in m],
|
||||
"stale_note": c.inverters[0].stale_note(),
|
||||
"not_ready_row": [r["text"] for r in c.checks()
|
||||
if r["text"].startswith("battery power")],
|
||||
}
|
||||
|
||||
|
||||
def compare(a_path, b_path):
|
||||
a = json.loads(Path(a_path).read_text(encoding="utf-8"))
|
||||
b = json.loads(Path(b_path).read_text(encoding="utf-8"))
|
||||
beh_same = a["behaviour"] == b["behaviour"]
|
||||
sent_same = a["sentences"] == b["sentences"]
|
||||
ha = hashlib.sha256(json.dumps(a["behaviour"], sort_keys=True).encode())
|
||||
hb = hashlib.sha256(json.dumps(b["behaviour"], sort_keys=True).encode())
|
||||
print(f"behaviour A {ha.hexdigest()}")
|
||||
print(f"behaviour B {hb.hexdigest()}")
|
||||
if sent_same:
|
||||
# ⚠️ THE REFUSAL, AND IT IS THE POINT OF THE TOOL. Two runs whose
|
||||
# sentences agree are either the same tree twice or a card that changed
|
||||
# nothing an operator reads. Either way "behaviour unchanged" is not a
|
||||
# result, and reporting it would be an identity measured against itself.
|
||||
print("REFUSED: the `sentences` halves are IDENTICAL, so these two runs "
|
||||
"cannot be evidence that behaviour survived a WORDING change - "
|
||||
"they may be the same tree twice. Compare a tree against one "
|
||||
"whose sentences differ.")
|
||||
return 2
|
||||
if not beh_same:
|
||||
for k in sorted(set(a["behaviour"]) | set(b["behaviour"])):
|
||||
if a["behaviour"].get(k) != b["behaviour"].get(k):
|
||||
print(f"BEHAVIOUR MOVED at {k!r}")
|
||||
return 1
|
||||
print("OK: sentences differ, behaviour is byte-identical.")
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
if len(sys.argv) == 4 and sys.argv[1] == "--compare":
|
||||
sys.exit(compare(sys.argv[2], sys.argv[3]))
|
||||
print(json.dumps({"behaviour": behaviour(), "sentences": sentences()},
|
||||
sort_keys=True, indent=1))
|
||||
Reference in New Issue
Block a user