test(validator): the gate was pinned in its arithmetic, not in its decision [mutation-ok]

[mutation-ok] rationale: no mutation is pinned in code. `src/` is byte-identical
to HEAD (git diff HEAD -- src/ is empty; `if False` occurs 0 times under src/).
The three matches the guard found are PROSE in the docs note and the test file's
docstring, quoting the detach mutation that was run and restored. Every harness
run in this session verified its restore by sha256 from disk.

S2.7 is the D7 mirroring queue's topmost unmeasured candidate. The MAF sibling
tightened its validator in two halves -- (a) a structural block on
`claimed > nominal_feasible`, (b) an IR invariant `low <= unit_cost <= high`.
Both halves are GATED here on D-A pkt. 1 + a commons pull, and the defect they
answer is confirmed on our side as C-F2. So neither is built. The question this
answers is the one that is answerable offline: is today's boundary -- "the ONE
numeric gate is p90" -- load-bearing?

One rule, structurally: a claim is numerically bounded in exactly two places in
src, each with its own spec role (ir.py:50 §7.1, validator.py:68 §3 Step 4).
The sibling's drift shape does not exist here.

But the coverage splits cleanly across the rule. Measured with
scripts/mutation_harness.py, denominator tests/ (all 955), each run
sha256-restored: everything the gate COMPUTES is red, because the golden
fixture freezes it -- policy cap, band branch, band endpoint order, MC seed,
p90 cut point, nominal_feasible. Everything the gate DECIDES WITH is
green-but-dead -- bound to p10, bound to nominal_feasible, and loosening the
comparison each left all 955 green. The golden freezes what the validator
produces, so it cannot help with the one thing it does not observe: which bound
the gate reads. Swapping p90 for nominal_feasible IS the gated S2.7 half (a),
and it would have landed with the suite green, before D-A was decided.

Closed by tests/test_validator_gate_loadbearing.py (8 tests, 955 -> 963). Each
clause is green before and red after exactly its own mutation, with the golden
figures green in BOTH runs -- which shows mechanically that the mutation moved
the decision, not the arithmetic. The two IR tests are pinned with --red-at
against the invariant's own message, since they die in a helper. The AST
population control was proved against a BEHAVIOUR-PRESERVING mutation (the gate
widened to a logically equivalent conjunction) with all three behavioural
controls green: a new gate site is invisible to any behavioural test, which is
why it is there.

Two things the measurement gave in addition. Under the containment mutation the
golden test stayed green, confirming mechanically that half (b) is
golden-compatible when D-A lands. And the IR carries no ORDER on band endpoints
either -- strictly more than C-F2 names: (1.40, 0.70) is accepted, and while
random.uniform still draws from [0.70, 1.40], it walks the seeded stream
backwards, which is a different p90 (120456.91 against 121057.09).

Honest limit: pinning that a claim above nominal_feasible validates today is not
an endorsement of it. C-F2 calls that a MAJOR spec-level defect and the fix is
gated, not declined. These tests make the gated work arrive as a visible red
test and a decision, never as a silent swap. No src change, no spec text
touched, the fasit untouched.

Dated under the D7 frame: work AFTER 2026-08-09, not independent convergence.

Co-Authored-By: Claude <claude-opus-5>
This commit is contained in:
Kjell Tore Guttormsen 2026-09-07 00:07:19 +02:00
commit 544655b4c8
2 changed files with 287 additions and 2 deletions

View file

@ -35,9 +35,9 @@ spørringen som ble kjørt** — ikke fila den ble kjørt mot.
## D7-speilingskøen
Åtte kandidater for speiling mellom D7-søsknene. **Ingen er besluttet** — de står som
kandidater, ikke som planlagt arbeid:
kandidater, ikke som planlagt arbeid. **Tre er målt, 5 står igjen:**
- S2.7
- ~~S2.7~~ — **MÅLT 2026-09-07, se under**
- S3.2
- S4.0 (`126807a`)
- (p) `to_ore` — TO kallsteder
@ -126,6 +126,71 @@ siden.
**Datering (D7-rammen):** arbeid ETTER 2026-08-09 — skal **ikke** leses som uavhengig konvergens.
### S2.7 — gaten er ÉN regel, og den var pinnet i ARITMETIKKEN, ikke i BESLUTNINGEN (målt 2026-09-07)
Kandidaten står i køen fordi søskenet strammet validatoren i to halvdeler: (a) en strukturell
blokk på `claimed > nominal_feasible`, og (b) en IR-invariant `low ≤ unit_cost ≤ high`. **Begge
halvdeler er GATET her** på D-A pkt. 1 + commons-pull (paritetsplanens rad 12), og defekten de
svarer på er bekreftet på vår side som C-F2 (`docs/review-2026-07.md`). Speilings-spørsmålet som
KAN besvares offline i dag er derfor et annet: **er dagens grense — «den ENE numeriske gaten er
p90» — load-bearing?**
**Populasjonen først.** En claim er numerisk avgrenset i nøyaktig TO steder i `src/`, med hver
sin spec-rolle: skjema-invarianten (claim ≤ items-total, §7.1, `ir.py:50`) og validator-gaten
(claim ≤ p90, §3 Steg 4, `validator.py:68`). `_FEASIBLE_FRACTION` forekommer kun i `validator.py`,
og det finnes ingen annen Monte Carlo eller `quantiles`-beregning i pakken (positiv kontroll:
samme spørring finner `validate_proposal` i `loop.py:284`). Søskenets drift-form — to gater som
har glidd fra hverandre — finnes altså ikke her.
**Men dekningen deler seg rent på tvers av regelen.** Med `scripts/mutation_harness.py`, nevner
`tests/` (hele suiten, 955 tester), hver kjøring sha256-restaurert:
- Å detache gaten helt (`if … > p90:``if False:`) er **RØD**`test_validator.py` fanger den.
- Alt gaten **REGNER UT** er RØDT, og goldenen er grunnen: policy-taket (`0.30``0.31`),
band-grenen (ignorér bands), band-endepunktenes rekkefølge, MC-seeden, p90-kuttpunkt-indeksen
og `nominal_feasible`-formelen reddet alle suiten.
- Alt gaten **BESLUTTER MED** er **grønn-men-dødt**: å bytte grensen til `p10`, å bytte den til
`nominal_feasible`, og å løsne `>` til `>=` lot alle 955 testene stå grønne.
Det skillet ER funnet, og det er skarpere enn «sømmen er tynn»: goldenen fryser hvert tall
validatoren PRODUSERER, og kan derfor ikke hjelpe med det ene den ikke observerer — hvilken
grense gaten LESER. Konsekvensen er konkret: **å bytte `p90` mot `nominal_feasible` ER den gatede
S2.7-halvdel (a), og den ville landet med suiten grønn**, før D-A er besluttet.
**Pinnet av** `tests/test_validator_gate_loadbearing.py` (8 tester, 955 → 963). Value-beviset er
kjørt, ikke påstått: hver klausul-test er grønn før og rød etter nøyaktig sin egen mutasjon, med
golden-tallene grønne i BEGGE kjøringer — som mekanisk viser at mutasjonen flyttet BESLUTNINGEN,
ikke aritmetikken. De to IR-testene er pinnet med `--red-at` mot invariantens egen feilmelding,
fordi de dør i en hjelpefunksjon og ikke i testkroppen.
**Mutasjonene ble vist å endre oppførsel FØR deres grønne ble lest som hull** (fellen fra økt 39).
Alle tre grensetilfellene er nåbare og ble kjørt: en claim nøyaktig PÅ p90 finnes (degenerert
band, `0.30 × 1000 == 300.0`), og med goldenens eget band valideres en claim på 100 000 mens
`nominal_feasible` er 90 000 — C-F2s første moteksempel, reprodusert live på p90 = 121 057.09,
sammen med det andre (claim 55 000 mot nominal 30 000, p90 = 65 058.49). Begge tallene er
identiske med review-ens, som bekrefter at defekten er spec-båren.
**To ting målingen ga i tillegg.** (1) Populasjonskontrollen (AST) ble bevist mot en
**oppførselsbevarende** mutasjon — `> p90` utvidet til `> p10 and > p90`, som er logisk identisk
når `p10 ≤ p90` — og alle tre oppførselskontrollene forble grønne. En ny gate-plassering er
usynlig for enhver oppførselstest; det er nettopp derfor AST-kontrollen står der. (2) Under
containment-mutasjonen forble golden-testen **grønn**, hvilket mekanisk bekrefter review-ens
påstand om at S2.7 halvdel (b) er golden-kompatibel når D-A lander.
**Nytt utover C-F2:** IR-en har heller ingen ORDNING på band-endepunktene. `(1.40, 0.70)`
aksepteres; `random.uniform(1.40, 0.70)` trekker fortsatt fra [0.70, 1.40], så området korrumperes
ikke — men den seedede strømmen vandres baklengs, hvilket er en ANNEN p90 (målt: 120 456.91 mot
121 057.09). Et band hvis betydning avhenger av argument-rekkefølgen er ennå ikke et band.
**Ærlig grense — hva dette IKKE sier.** Å pinne at en claim over `nominal_feasible` validerer i
dag er ingen godkjenning av oppførselen; C-F2 kaller den en MAJOR spec-nivå-defekt, og fiksen er
GATET, ikke avvist. Testene pinner grensen slik at det gatede arbeidet MÅ ankomme som en synlig
rød test og en beslutning, aldri som et stille bytte. Ingen `src/`-endring er gjort, ingen
spec-tekst rørt, og fasiten er ikke berørt.
**Datering (D7-rammen):** arbeid ETTER 2026-08-09 — skal **ikke** leses som uavhengig konvergens.
Rammen rundt køen: å lese søskenets kode er tillatt (`3bdf7f0`), men kopiering skal kun skje
der det tjener løsningen, aldri som snarvei. **Uavhengighets-beviset er DATERT** t.o.m.
2026-08-09; arbeid etter den datoen kan ikke leses som uavhengig konvergens.