Skip to content

Judge every rendered claim, over the whole set of states that render one - #5

Closed
systemslibrarian wants to merge 2 commits into
mainfrom
verdict-harness
Closed

systemslibrarian wants to merge 2 commits into
mainfrom
verdict-harness

Conversation

@systemslibrarian

Copy link
Copy Markdown
Owner

Five of the six lane fixes in audits/LANE-VERDICT-HARNESS-2026-09-21.md apply to this lab. Fix 5 is a constraint and was honoured: branch protection was not touched in either direction, confirmed read-only at the API (build + verdict-coverage required, enforce_admins: false, force-push and deletions disabled) — which is why this is a pull request.

Baselines

Every run below used CI=1, so Playwright started its own server on this lab's pinned port 4698 (tools/playwright-ports.json) and no reused listener could turn a mutation into a false survivor.

Result
Unmutated baseline BEFORE any edit (ab679b9) 21 passed (15.0s)
Unmutated baseline AFTER all edits 23 passed (31.7s) (+ Tests 24 passed (24) unit)

Two gaps confirmed by survival, not by argument

Both were run against the suite exactly as it stood at ab679b9, before any harness change.

S1 — the record verdict's plate, pinned green (Fix 1). src/ui/app.ts sets verdict.className and verdict.dataset.status in separate expressions. Replacing the class expression with the constant 'verdict verdict-pass' leaves a green pass plate reading "RETRIEVED — AND WRONG".

  21 passed (13.9s)

SURVIVED. Seven assertions covered that marker's text and its data-status; none covered what a reader actually sees.

S2 — the size formula's total, a literal (Fix 4/6). = ${parts.total} bytes replaced with = 290 bytes, correct only at the default 65,536-record domain.

  21 passed (13.9s)

SURVIVED, because nothing in the suite ever moved #size-domain.

Mutations run against the new harness

All twelve were actually run; none is recorded from reasoning. Baseline was green in the same session for each.

Fix 1 — record-match, the same S1 mutation

Error: record-match is painted as alarm while its text says "RETRIEVED — AND WRONG / 1 of 16 bytes differ"

expect(received).toBe(expected) // Object.is equality

Expected: "rgb(66, 29, 36)"
Received: "rgb(15, 53, 43)"

   at verdict-assertions.ts:45

KILLED — 1 failed / 22 passed, on that marker's own assertion.

Fix 4/6 — key-size-formula, the same S2 mutation

Error: the formula states this domain's own measured parts: 17 + (17 × log₂ 16) + 1 = 290 bytes

expect(received).toEqual(expected) // deep equality

  Array [
    17,
    17,
    16,
    1,
-   86,
+   290,
  ]

KILLED — 1 failed / 22 passed. Note the domain in the failure: log₂ 16. It is the walk over all four domain options that makes this visible at all.

Fix 2/3 — the denominator itself, data-claim="chor-query-bytes" deleted from index.html

Error: mutations registered for measurements this page never renders

- Array []
+ Array [
+   "chor-query-bytes",
+ ]

and, from the stray-measurement scan:

Error: unmarked measurements on the page: [
  {
    "tag": "span",
    "id": "chor-byte-label",
    "reason": "measurement rendered outside a data-claim marker: \"8,192 bytes · 65,536 bits\"",
    "text": "8,192 bytes · 65,536 bits"
  },

KILLED — 5 failed / 18 passed, both coverage directions plus the scan, all on the mutation's own subject.

The remaining measurement claims

Marker Mutation Verbatim Result
chor-query-bytes domainSize / 8 → / 4 Error: chor-query-bytes measured value / Expected: 2 / Received: 4 KILLED (1 failed / 22 passed)
key-part-root rendered root parts.rootMaterial → - 1 Error: key-part-root measured value / Expected: 17 / Received: 16 KILLED (1 failed / 22 passed)
key-part-levels rendered levels + perLevel Error: key-part-levels measured value / Expected: 68 / Received: 85 KILLED (1 failed / 22 passed)
key-part-final rendered final → 2 B Error: key-part-final measured value / Expected: 1 / Received: 2 KILLED (1 failed / 22 passed)
key-bytes-total rendered total serialized.length - 1 Error: key-bytes-total measured value / Expected: 86 / Received: 85 KILLED (2 failed / 21 passed)
dpf-key-bytes label renders parts.correctionWords Error: dpf-key-bytes measured value / Expected: 86 / Received: 68 KILLED (1 failed / 22 passed)
prg-node-width * 8 + 2 → * 8 Error: prg-node-width measured value / Expected: 258 / Received: 256 KILLED (1 failed / 22 passed)

key-bytes-total failed two tests, and the second is worth reading: the server-tile test now derives the key size it expects from that claim rather than from a literal 290, so it went red too —

Error: server-view-0 text
Expected substring: "one party-0 key of 289 B"
Received string:    "1Server 0 · one party-0 key of 290 B · folded 33,077 of 65,536 records"

One mutation run and REJECTED as evidence

key-part-root was first attempted at the source: const ROOT_MATERIAL_BYTES = 1 + SECURITY_BYTES → SECURITY_BYTES in src/dpf/serialize.ts. The key stops round-tripping and the whole suite goes red — 6 passed, with the first failure being locator('#step-value') Expected: "3 / 4" Received: "4 / 4", nothing to do with the marker. Per the lane's rule that is not a readable kill, so it is not the recorded mutation. The recorded one flips only that claim. The rejection is written into the registry entry so the deeper mutation is not "helpfully" restored later.

Two previously recorded verdict mutations, re-run through the new helper

Marker Mutation Verbatim Result
single-share namesAPoint: lit === 1 → lit >= 1 Error: single-share text / Expected pattern: /ONE KEY ONLY · k0 alone lights \d+ of \d+ leaves, naming no point/ / Received string: "!ONE KEY ONLY · k0 alone lights exactly 1 of 16 leaves, so this share names a point by itself" KILLED (1 failed / 22 passed)
record-match (the previously recorded shape) reconstruct drops server 1: byte ^ (answer1[index] & 0) Expected: "0000a179b775501af95aeda6e57ca896" / Received: "0000cb3c7630d6e4d53e25f1bcda4ba4" KILLED (4 failed / 19 passed). Honest note: the first failing assertion is the shelf-oracle comparison inside the record-match test, not the expectVerdict line. It is that marker's own test, and the registry now records the stronger class-pin mutation instead, because that one is the only mutation in the set that distinguishes a plate from a sentence.

No mutation survived the new harness. No mutation timed out. The six verdict mutations already recorded at ab679b9 and not re-run here (tree-point, collusion-recovery, server-view-0, server-view-1, collusion-state, no-authentication) keep their original records; the harness change only strengthened their assertions.

Fix 6, enumerated for this lab

driveEveryState visits every option of every control that changes what renders, each control on its own, never the cross-product:

Control Options visited
#alpha-range all 16 secret indices
expansion stepper (#step-back / #step-next) all 5 levels, down and back up
#new-keys one option, exercised once
#size-domain all 4 domains (16 / 256 / 4,096 / 65,536 records)
#collusion-toggle both states, and again through a fetch for the tile it paints
#tamper-toggle both states, with its own fetch
#fetch-record exercised throughout
#shelf-alpha not an enumerable option set — a 65,536-value number input, so its two rendering classes stand in: the in-range fetch and the rejection that renders no result
.key-inspector disclosure opened, because both scans skip elements with no client rects, so a closed disclosure hid the serialized key dump from the denominator entirely

No control on this page was judged not to change what renders, so nothing was skipped on that ground.

Catalog-affecting findings

None. Nothing in crypto-lab was edited. The card's copy and chips remain accurate: the page still teaches two-server DPF PIR, and the one page string that was a standing constant rather than a measurement (AES-128-CTR → 2(λ + 1) bits) is now rendered from a real expandSeed() and reads AES-128-CTR → 2(λ + 1) = 258 bits per node.

🤖 Generated with Claude Code

https://claude.ai/code/session_01UH9YUUhdeWXJz141Zy8FxW

systemslibrarian and others added 2 commits September 21, 2026 18:41
Five of the six lane fixes apply here. Two gaps were confirmed by running the
mutation against the suite as it stood at ab679b9 and watching it pass.

Fix 1 — one helper asserts words, state and plate together.
e2e/verdict-assertions.ts adds expectVerdict(page, id, {text, status, tone}) and
expectClaim(page, id, {value, text}), and the coverage test now requires every
recorded mutation's assertedBy spec to call the helper on that marker, instead of
merely mentioning the id. This lab set className and dataset.status in separate
expressions, so pinning the class green while the words and the status still
followed the run was invisible: at ab679b9 that mutation passed 21/21. tone is
checked as the painted background, because .verdict switches class and
.mini-verdict switches on [data-status].

Fix 2 — measurements join the coverage loop on the same terms.
The page rendered eighteen-odd numbers and not one carried a marker, so the
coverage rule enforced itself over one family of a page that had two. Eight
data-claim markers now carry the measurement in data-value, are registered in
e2e/verdict-mutations.json under "claims", and fail the build both ways: a
rendered measurement with no record, and a record naming a measurement the page
no longer renders.

Fix 3 — the digit-plus-unit scan.
findStrayMeasurements walks the result regions for digit-plus-unit text and for
bare integers in stats cells that sit outside a marker, with its own injection
self-test so it cannot pass by being blind. Hex dumps are exempt as raw material
(claims.spec checks them byte for byte against the size markers), and labels and
explanatory prose are exempt the same way the verdict-word scan exempts them.
The one static number on the page that was really a claim — "AES-128-CTR → 2(λ +
1) bits" — is now measured from a real expandSeed() and marked.

Fix 4 — the oracle multiplied where the artifact iterates.
The old key-size test asserted root + 17 * domainBits + final === measured at the
one default domain: one per-level size multiplied by a level count, both
literals, where serializeKey WRITES one correction word per level. It could not
tell "sixteen words of seventeen bytes" from "one 272-byte block", which is
exactly what the parts list claims. The oracle now measures the per-level cost as
the slope between domains, derives λ and the root from it, counts the correction
words actually present in the dump by walking it in stride, and SUMS them.

Fix 5 — branch protection untouched. Confirmed read-only at the API
(build + verdict-coverage required, enforce_admins false, force-push disabled),
which is why this is a pull request.

Fix 6 — driveEveryState visits every option of every control.
Per control, not the cross-product. #alpha-range all 16 indices; the expansion
stepper all 5 levels down and back; #new-keys once; #size-domain all 4 domains;
#collusion-toggle both states, and again through a fetch for the tile it paints;
#tamper-toggle both states with its own fetch; #fetch-record throughout. Two
controls are not enumerable option sets and are recorded as such: #shelf-alpha is
a 65,536-value number input, so its two rendering classes stand in — the in-range
fetch and the rejection that renders no result — and the .key-inspector
disclosure is opened because both scans skip elements with no client rects, so a
closed disclosure hid its contents from the denominator entirely. No control on
this page was judged not to change what renders.

That widening is load-bearing, not tidiness: the formula's total was a hard
literal correct only at 65,536 records, and at ab679b9 that mutation also passed
21/21 because nothing ever moved #size-domain.

Baseline before any edit: 21 passed (15.0s). After: 23 passed (31.7s), plus
24 unit tests. Every mutation below was run with CI=1 so Playwright started its
own server on the pinned port 4698.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UH9YUUhdeWXJz141Zy8FxW
D6, in this lab. Fix 1 as it shipped at 521d03d did not satisfy Fix 1. The
rule was FILE-granular and read with a regex: a record naming
e2e/claims.spec.ts was satisfied by the string expectVerdict(page,
'record-match' appearing ANYWHERE in that file — inside a comment, inside a
call handed the page's own values, inside a call asserting a different state
in a different test. And the shipped tree already contained an instance:
tree-point's recorded mutation was killed by two raw assertions that never
reached the helper, so the expectedFlip its record describes was a flip no
run had ever demonstrated.

expectVerdict/expectClaim now append the (spec, test, marker) triple of every
call they EXECUTE to a run-scoped ledger under test-results/verdict-ledger/,
cleared once per run in e2e/global-setup.ts. e2e/verdict-ledger.spec.ts reads
it back and fails when a record's triple is not among them. Playwright runs
each spec in its own worker process, so a module-level Set cannot aggregate;
the sink is one append-only file per process, and the reader is its own
project with dependencies: ['claims'] rather than an ordinary test. That
project is what npm run test:verdicts runs now, so the required check reads
the ledger with the specs that write it — .github/ is untouched.

assertedBy stops being a filename. It is {spec, test, status, says}: the
triple, plus the part of the expectation the RECORD decides — the outcome the
killing assertion must require, and one fragment it must hand the helper
verbatim (a "re:" prefix is a RegExp source). That second half is the only
thing that can catch a call kept but made tautological, and it has to work
that way round: on an unmutated tree an expectation read off the page and one
decided in advance are the same values, so no amount of observing the run
separates them. Only something decided before the run can.

The plate is no longer an argument. tone: 'pass' | 'alarm' is gone and the
plate is derived from the asserted status through one table, because a reader
is never shown an alarm outcome on the success plate — so a test cannot
expect one either. That closes the residue: a tautologist who has read the
record and hands the declared fragment still cannot mask record-match's
mutation, because the plate follows the status it read rather than the paint
it read.

Two recorded mutations were killed by a precursor rather than by the helper,
and both are reordered so the helper is reached first:

- tree-point — reconstruction[alpha], the lit-bit count and the #tree-xor
  readback all failed on the direction-bit mutation before line 232's
  expectVerdict ran.
- key-size-formula — found by running the set: the formulaNumbers comparison
  caught the pinned-290 mutation at claims.spec.ts:209, before expectClaim.
  Through the helper it now fails on its own terms, "data-value 86 is not in
  17 + (17 × log₂ 16) + 1 = 290 bytes".

Escapes. Each run in an isolated tree archived from this commit, node_modules
symlinked, port moved to 4931, spec-only rewrites with the built bundle
IDENTICAL before and after (index-RVWjpVch.js 3a8b3a777965e297ba523fe90f68143b),
baseline 21 passed / exit 0 in the same tree:

- Commented out — verdict-ledger fails: "e2e/verdict-mutations.json says its
  mutation is killed by expectVerdict in e2e/claims.spec.ts › 'tampering
  violates integrity…', and that call did not execute this run. expectVerdict
  ran for record-match in: e2e/claims.spec.ts › honest PIR output equals the
  indexed shelf record (status 'pass')."
- Kept but tautological — expectVerdict fails in the test itself: "declares
  the words this assertion must require — 'RETRIEVED — AND WRONG' — and it
  was handed ['RETRIEVED — AND WRONG · 1 of 16 bytes differ from shelf[α]; no
  PIR authentication failure was raised']." With the declared fragment handed
  over and the mutation applied, it fails one layer down instead: "record-match
  is painted as pass while its outcome is 'alarm'", expected rgb(66, 29, 36),
  received rgb(15, 53, 43).
- Satisfied from an unrelated line in the same file — this lab's own failure
  mode, the killing assertion rewritten as text + data-status with the
  honest-fetch call left in place. Same ledger failure as the first, naming
  the test the surviving call actually ran in. At 521d03d this shipped 23/23.

All 16 recorded mutations re-run against this tree with CI=1: none survived,
and every failure is now inside e2e/verdict-assertions.ts — line 110 (text),
112 (data-status), 118 (plate), 154 (measured value), 161 (the sentence
states its own value).

README: the count is 47 (24 Vitest + 23 Playwright), the gate paragraph
describes the ledger, and README:17's "every number it renders carries a
data-claim marker" is corrected. #fetch-status renders "Both full-domain
folds completed in 1,019 ms" outside every marker; verdict-scan.ts scans
result regions and not status prose, so the rule is met as scoped and it was
the sentence that was false. The figure is left unmarked on purpose — it
measures the device, not the protocol.

Branch protection untouched, in either direction.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@systemslibrarian
systemslibrarian deleted the verdict-harness branch September 30, 2026 01:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant