Skip to content

fix(security): truncated modules verified — pin the terminal hash (BLOCKS v0.12.0) - #305

Merged
avrabe merged 2 commits into
mainfrom
fix/terminal-hash-pinning
Oct 16, 2026
Merged

avrabe merged 2 commits into
mainfrom
fix/terminal-hash-pinning

Conversation

@avrabe

@avrabe avrabe commented Oct 6, 2026

Copy link
Copy Markdown
Contributor

Wrong-accept in the DEFAULT verification path. Found by the v0.12.0 pre-release Mythos pass, on files that stale rank.md scoping had hidden from every previous pass. Stacks on #301.

Root cause

sign_multi never resets its hasher: at each signature delimiter it pushes hasher.finalize(), so a signed hashes list is a sequence of cumulative prefix hashes [H(P₁), H(P₂), … H(Pₙ)] — only the last is the hash of the complete stream. The header signs their concatenation with no count, index or scope tag, and valid_hashes_for_pk inserts every element into an unordered accept-set. No verifier required the terminal hash.

So a split-signed module truncated at any delimiter still verifies — the truncated stream's whole-module hash is a signed prefix hash.

PublicKey::verify — what plain wsc verify calls for every module, the most-executed verification entry point in the tool — returned Ok for a module whose Function and Code sections were deleted after signing. The attacker needs no key material and no collision, only the published artifact: strip trailing custom sections carrying SBOM/attestation/policy metadata, or strip code/data to force a fail-open downstream, and the signature keeps validating.

Fixed

Path Change
PublicKey::verify, PublicKeySet::verify whole-module verifiers accept only the terminal hash
verify_multi, verify_matrix keep the prefix set (they legitimately check delimiter-bounded ranges) but now pin the end of the stream — the last hash compared must be terminal
verify_multi, verify_matrix finalize the predicate contract: sections appended after the last delimiter were never hash-compared yet returned Ok even when the caller's own predicate said they must be signed

This is one step past #301, which closed "no delimiter at all" but left "truncate at a delimiter" open — same loop, same missing finalization.

valid_hashes_for_pk gains a terminal_only flag rather than being changed outright, because the partial verifiers genuinely need the prefix set. The bug was whole-module verifiers borrowing it.

Oracles

8 regression tests (5 in split.rs, 3 in simple.rs), each with a positive control (untampered module verifies) and a negative control (cutting at a NON-delimiter is rejected) so none can pass for the wrong reason. Fixtures built only through shipped APIs, with truncation at the section level then re-serialized — no malformed framing can create a false positive.

Mutation-verified, each guard independently: reverting simple.rs's pinning fails all 3 truncation tests; reverting multi.rs's fails 2 more; matrix.rs's is separately load-bearing.

Deferred — oracles kept as #[ignore]d tests naming the issue, not deleted

Tests

wsc-verify-core 177 pass/3 ignored (+8) · wsc 657 pass/3 ignored · airgapped_e2e 5 · keyless_integration 5 · sigstore_bundle 10. End-to-end: a full split-signed module still verifies (exit 0).

Merge order: #301 → this → #300 (the v0.12.0 bump), then tag. #300's CHANGELOG needs an entry for this.

🤖 Generated with Claude Code

https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH

avrabe and others added 2 commits October 6, 2026 21:10
… delimiter

WRONG-ACCEPT, reachable from `wsc verify --split`. Found by the v0.12.0
pre-release Mythos delta pass; blocks the release.

In both `PublicKey::verify_multi` (multi.rs) and `PublicKeySet::verify_matrix`
(matrix.rs) the running hash is compared against the signed hashes ONLY inside
the `if section.is_signature_delimiter()` branch, and neither finalizes after
the section loop. A module that carries a signature header but NO delimiter
section — i.e. one signed without `wsc split` — therefore ran the loop doing
predicate bookkeeping only, never compared its content against any signed hash,
and still succeeded:

  - verify_multi fell through to `Ok(())`, so `wsc verify -k K -i M --split <rx>`
    printed "Signature is valid." for content that was never checked.
  - verify_matrix left `valid_hashes_for_pks` unpruned, so every key merely
    present in the signature header came back "valid" — an affirmative accept,
    not just a missing rejection.

`PublicKey::verify` (simple.rs) is unaffected: it hashes the whole remaining
stream, which is why plain `wsc verify` rejects the same bytes with exit 1.

Fix: fail closed when no delimiter was ever processed. multi.rs already tracked
this in `matching_section_ranges`; matrix.rs gains an explicit
`compared_against_a_signed_hash` flag.

Also fixes the two CLI defects the same pass found in the `verify-matrix` arm:

  - It read the argument id `signature_file`, which the subcommand never
    declared; clap v4 panics on an unknown id (v3's `value_of` returned None),
    so the verb aborted with exit 101 on EVERY invocation — shipped through the
    clap v3->v4 upgrade because `verify-matrix` had zero test coverage. The arg
    is now declared, which both removes the panic and makes detached signatures
    work as the handler intended.
  - An empty valid-key set printed "No valid public keys found" and fell through
    to `Ok(())`, exiting 0 — a verification failure reported to CI as success, on
    the only machine-readable signal. It now returns
    VerificationFailedForPredicates, so `main()` exits 1 like `wsc verify`.

Plus a diagnostic: `verify-matrix` only speaks about delimiter-bounded ranges, so
a non-split module now fails with a note pointing at `wsc verify`, rather than a
bare "No valid signatures" that reads as "my signed module is broken".

And completes #286: rank.md's tier-4/3/2 paths also drifted in the v0.11.0 split
(`signature/{matrix,multi,simple,hash}.rs`, `signature/info.rs`, `split.rs` all
moved to verify-core). That stale scoping is exactly why matrix.rs and multi.rs
were never in the delta scope and this wrong-accept went unhunted.

Oracles, both mutation-verified:
  - matrix: test_verify_matrix_rejects_tampered_module_without_delimiter —
    removing the guard yields `Ok([0])`, failing the test.
  - multi: test_verify_multi_rejects_tampered_module_without_delimiter, plus a
    control asserting a properly split-and-signed module still verifies.
    NOTE: the first version of this test was itself vacuous — a varying
    predicate ("Type only") tripped verify_multi's predicate bookkeeping, so it
    passed with the guard removed. It now uses a CONSTANT predicate so the guard
    is the only thing that can reject. multi.rs previously had no test module
    at all.

End-to-end (debug CLI): split+signed -> "Valid public keys", exit 0; the same
module with one byte flipped -> rejected, exit 1 (was exit 0); non-split signed
-> wrong-verb note, exit 1; no invocation panics (was exit 101 always).

Tests: wsc-verify-core 169 pass/1 ignored (+3); wsc 657 pass/3 ignored;
airgapped_e2e 5; keyless_integration 5; sigstore_bundle 10; gate exit 0.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
…(WRONG-ACCEPT)

Release-blocking wrong-accept in the DEFAULT verification path. Found by the
v0.12.0 pre-release Mythos delta pass, on files that stale rank.md scoping had
hidden from every previous pass.

ROOT CAUSE. `sign_multi` never resets its hasher: at each signature delimiter it
pushes `hasher.finalize()`, so a signed `hashes` list is a sequence of CUMULATIVE
PREFIX hashes [H(P1), H(P2), ... H(Pn)] and only the LAST element is the hash of
the complete section stream. The header signs their concatenation with no count,
index or scope tag, and `valid_hashes_for_pk` then inserts EVERY element into an
unordered accept-set. No verifier required the terminal hash.

Consequence: a split-signed module truncated at ANY delimiter still verifies,
because the truncated stream's whole-module hash IS a signed prefix hash.
`PublicKey::verify` — what plain `wsc verify` calls for every module, the
most-executed verification entry point in the tool — returned Ok for a module
whose Function and Code sections had been DELETED after signing. Attacker needs
no key material and no collision, only the published artifact: strip trailing
custom sections carrying SBOM/attestation/policy metadata, or strip code/data to
force a fail-open downstream, and the signature keeps validating.

Affected and fixed:
  - PublicKey::verify, PublicKeySet::verify (simple.rs) — whole-module verifiers
    now accept ONLY the terminal hash (`valid_hashes_for_pk(.., true)`).
  - verify_multi (multi.rs), verify_matrix (matrix.rs) — these legitimately need
    every prefix hash to check delimiter-bounded ranges, so they keep the full
    set but now additionally pin the END of the stream: the last hash compared
    must be a terminal hash. This is one step past commit a63ff86, which closed
    "no delimiter at all" but left "truncate AT a delimiter" open in the same
    loop, from the same missing finalization.
  - verify_multi/verify_matrix also finalize the predicate contract: sections
    appended AFTER the last delimiter are never hash-compared, yet both returned
    Ok even when the caller's own predicate said those sections must be signed.
    The in-loop bookkeeping rejects the inverse case, so the intent was
    unambiguous; it simply was never finalized.

`valid_hashes_for_pk` gains a `terminal_only` flag rather than being changed
outright, because the partial verifiers genuinely need the prefix set — the bug
was whole-module verifiers borrowing it.

Oracles: 8 regression tests (5 in split.rs, 3 in simple.rs), each carrying a
positive control (the untampered module verifies) AND a negative control
(cutting at a NON-delimiter is rejected), so none can pass for the wrong reason.
Mutation-verified: reverting the simple.rs pinning fails all three truncation
tests, reverting multi.rs's fails two more, and matrix.rs's is independently
load-bearing. Fixtures are built only through shipped APIs (`Module::split` +
`sign_multi` + `serialize`) with truncation done at the SECTION level and
re-serialized, so no malformed framing can produce a false positive.

Two findings from the same pass are DEFERRED with their oracles kept as
`#[ignore]`d tests naming the issue, rather than deleted:
  - #303 the 8-byte WASM preamble is not hashed at all, so a signed core module
    relabels to a component and still verifies. Fixing it changes what is signed
    and invalidates every existing signature — needs a SIGNATURE_VERSION bump
    and migration, not a patch.
  - #304 re-signing retains stale signed_hashes_set entries, so v1 content
    verifies under a v2 header. NOT fixed by terminal pinning (v1's hash is
    terminal within its own entry); the remedy is sign-side.

Tests: wsc-verify-core 177 pass/3 ignored (+8); wsc 657 pass/3 ignored;
airgapped_e2e 5; keyless_integration 5; sigstore_bundle 10. End-to-end: a full
split-signed module still verifies (exit 0).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
@codecov

codecov Bot commented Oct 6, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 86.09524% with 73 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
src/verify-core/src/signature/simple.rs 61.01% 69 Missing ⚠️
src/verify-core/src/signature/matrix.rs 97.01% 2 Missing ⚠️
src/verify-core/src/signature/multi.rs 98.66% 1 Missing ⚠️
src/verify-core/src/split.rs 99.51% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe
avrabe merged commit 74665d9 into main Oct 16, 2026
20 checks passed
@avrabe
avrabe deleted the fix/terminal-hash-pinning branch October 16, 2026 21:44
avrabe added a commit that referenced this pull request Oct 21, 2026
Four additions and three corrections to the v0.12.0 entry.

Added:
  * #305, placed FIRST under Fixed because it is the cycle's most severe
    finding: a split-signed module truncated at any delimiter verified, through
    plain `wsc verify`, with Function+Code deleted and no key involved.
  * REQ-31 / #302 under a new Changed section — toolchain 1.96.1, wasmtime
    49.0.4, the 9.3 CRITICAL retired rather than excepted, and the MSRV
    consequence stated for consumers (`runtime` now needs rustc >= 1.96).
  * the two webpki advisories published within 48 hours of the release, with
    why they are not housekeeping: both land on step 1 of
    PinnedCertVerifier::verify_server_cert.
  * #284 — the real cause (rivet 0.3.0 byte-slicing an em-dashed title during
    Export), the 22 validate errors, the unresolvable `../synth` external, and
    the duplicate CV-25 id that had kept one verification artifact out of the
    trace entirely.

Corrected:
  * **"Unmasked and therefore potent: kani varint, kani dsse, kani
    wasm_module" was FALSE** — and false because it copied
    formal-verification.yml's own summary comment, which contradicted the
    matrix three lines below it. One module is unmasked. Replaced with the
    measured table: pre-mask exit codes read out of the run logs (the API
    reports a masked step as success), showing SEVEN failing Kani harnesses
    behind a green board, `format.rs` — this release's largest piece of new
    attacker-facing code — among them. Publishing the original sentence would
    have shipped a false verification claim in the release notes.
  * the same paragraph now records that EVERY gate here is advisory in a
    second sense: main's required_status_checks.contexts is empty, so nothing
    blocks a merge. This release's merges were verified green by hand, and the
    notes say so rather than implying CI enforced them.
  * #301's falsification note: #305's terminal check subsumed its guard, so
    its mutation verification was true when written and stopped being true
    afterwards. The variant-pinning fix and the matrix.rs case that CANNOT be
    separated are both stated.
  * #285's wasmtime claim is marked superseded within this same release, and
    credited with #274's committed example lockfile, which is the half that
    makes it stay fixed.

Release date moved to 2026-10-21.

Refs #284, #302, #305, #274, #145

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Oct 21, 2026
…d way

Each of these cost real time this cycle and none of them was written anywhere.

**`rivet verify`, never `--set-status verified`** (checklist item 6).
`--set-status verified` writes the field and checks nothing; `rivet verify` is
the gate. This release's three requirements were all `verified` with zero
evidence, and the tool refused all three the moment it was actually asked.
Readiness is `rivet verify --dry-run` over the release's scope, not a read of
the status field.

**A masked gate's exit code is in the LOG, not the API** (item 7). A step under
`continue-on-error` reports `conclusion: success` for the step AND the job over
REST. Four of five Kani modules masked, seven harnesses failing, every job
green — and a workflow comment asserting three ran unmasked, which had already
propagated into the rivet store and the CHANGELOG before anyone read the
matrix below it.

**Confirm the merge actually waited** (item 8). `required_status_checks.contexts`
was empty with no rulesets, so every check here was advisory. Records the one
required context and why a paths-filtered context must never be required
directly — it will not report on an unrelated PR, and a *skipped* required
context satisfies the merge button.

**Never `--squash` a stacked PR** (merge step). It collapses the lower PR's
commits under the upper one's message, misattributes the work, and leaves the
lower PR looking unmerged forever. Twice here: REQ-27 under #273, and #301
inside #305. Also notes the merge-commit alternative's second benefit — the
base commit stays a real ancestor, so the sibling branch needs no replay and no
conflict resolution that might quietly drop a guard.

Plus: the `rivet validate` line this PR added already needed replacing. It said
"22 errors ... not a release gate". #314 takes it to PASS, and it IS a gate —
the compliance action propagates validate's exit code (rivet #953) and the
bundle is this project's V-model evidence. Also distinguishes the ~182 warnings
(real coverage gaps, `requirement-verification` 0/38) from errors, with the
rule that a warning is never closed by demoting an artifact to `draft`.

Two additions to "what NOT to do": never re-pin a baseline to get green, and
never add a `cargo audit --ignore` line to clear a release.

Refs #284, #300, #301, #302, #305, #314, #316, #317

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Oct 21, 2026
…ICAL (REQ-31), lands #307

Lands #307 and REQ-31 together, as a merge commit so each of the six commits
keeps its own message. Squashing a stack is what buried #301's security fix
inside #305 and REQ-27's 1,721 insertions under #273's 13-line title.

## The 9.3 CRITICAL is retired, not excepted

`cargo audit` measured today with a freshly fetched advisory database and the
workflow's own ignore list:

    main                                   31 vulnerabilities, exit 1
    wasmtime 47.0.4 (the MSRV-1.94 ceiling) 18 vulnerabilities, exit 1
    this merge                               0,                 exit 0

wasmtime alone was 20 of the 31, quinn-proto 5, rustls 4. Eight advisories
stood against 47.0.4 — RUSTSEC-2026-0327 (9.3 CRITICAL) plus -0353, -0354,
-0356, -0357, -0361, -0378 and -0316, most published mid-cycle — all fixed only
in 48.0.4+/49.0.x. Staying inside MSRV 1.94 could clear nine of 31 and no more,
which is why the toolchain bump stopped being deferrable cleanup.

NOTE: the first commit's message says "cargo audit goes 12 -> 3". That was a
week-old DB snapshot and is wrong in both directions; the table above is the
measurement. Corrected on #284 and in the v0.12.0 CHANGELOG.

Shipping under a documented exception was available — wasmtime is optional and
not in `default` — and was declined. The two `--ignore` lines are deleted
rather than re-justified, and `Cargo Audit` is green in CI for the first time
this cycle.

Also cleared: RUSTSEC-2026-0382 (rustls-webpki) and -0381 (webpki-roots), both
certificate-verification, both published within 48 hours of the release, both
landing on step 1 of `PinnedCertVerifier::verify_server_cert`.

## What re-qualifying the gates actually found

The scope said "record each masked gate's status before/after". The before was
the finding: measured from pre-mask exit codes in the run logs rather than API
conclusions, **four of five Kani modules were masked and seven harnesses were
failing behind a green board** — while `formal-verification.yml`'s own summary
comment claimed three ran unmasked, contradicting the matrix three lines below
it. That false claim had already propagated into the rivet store and the
v0.12.0 CHANGELOG. All three corrected; `claims.yaml` gains
`KANI-MASK-RATCHET` so the masked count can shrink but not grow.

Then the bump turned `Witness MC/DC gate` red, and reading the gap rows instead
of re-pinning the number found that on macOS/1.96.1 **the gate measured nothing
and reported OK** — the `^src/` scope collapsed to zero decisions, so the
"below baseline" branch printed a notice and exited 0. Empty scope is now a
hard error. The +2 on linux is `wasm_module/mod.rs:455` becoming visible, not
lost coverage: witness's own suggested row is infeasible for a short-circuit
`&&`. Baseline recalibrated 3 -> 4 with all four host/toolchain measurements
recorded, and a 6-case verdict table proves a further regression still trips
it, so the recalibration did not buy green by disarming the gate (#318).

Fixing that gate then exposed `.gitignore`'s `*.sh`, which had silently
dropped the new gate script — `git add -A` skipped it without a word and CI
failed with exit 127. `bash foo.sh || true` would have been green. The
vacuous-oracle gate now asserts every `bash <path>.sh` a workflow runs is a
tracked file, and `rust.yml` finally lists `verification/**`, so the gate is no
longer scoped to everything except itself.

## Re-qualification: before and after, from the logs

Pre-mask exit codes and harness counts, read from the run logs because the API
reports a masked step as success. Before: main @74665d9b, run 38971394138, rustc
1.94.0. After: this branch @35b8316c, run 39607181505, rustc 1.96.1.

    gate                 before (1.94.0)          after (1.96.1)
    Kani varint          5/5, exit 0  UNMASKED    5/5, exit 0
    Kani merkle          2 ok / 3 fail of 5       2 / 3 of 5   identical
    Kani dsse            0 / 1                    0 / 1        identical
    Kani format          2 / 2 of 4               2 / 2 of 4   identical
    Kani wasm_module     0 / 1                    0 / 1        identical
    Verus (both steps)   exit 1                   exit 1       identical
    Rocq                 exit 1                   exit 1       identical
    Witness MC/DC        2 gaps, baseline 3       4 gaps, baseline 4
                         UNMASKED                 3 decisions in scope

**The bump changed nothing behind any mask.** Every masked module carries the
same pass/fail counts on both toolchains, so the seven failing harnesses
predate it and none is new. That is the result the masked-gate accounting
existed to produce — "green before, green after" could not have shown it.

The calibration comment in witness-gate.sh lists two in-scope decisions for
linux/1.96.1; the log counts three. The third is `varint.rs:29`, FullMcdc,
0 gaps — the count and the verdict are unaffected. Recorded here rather than
fixed by another push, which would have restarted the full board.

## Also

`RUST_VERSION: "1.90.0"` deleted from three workflows — nothing ever read it.
`examples/wasmtime-loader/Cargo.lock` is now committed (#274), without which
raising the example to wasmtime 49.0.4 would not stay fixed.

**MSRV for consumers: the `runtime` feature now requires rustc >= 1.96.**

Closes #274 · Implements REQ-31 · Refs #284, #302, #312, #316, #318

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Nov 1, 2026
Audited 2026-10-21: main's `required_status_checks.contexts` is `[]` and the
repository has no rulesets. Every check in this repo is advisory. #305, #308,
#292, #306, #310 and #297 all merged over a board nothing enforced, and the
release that is being cut right now was gated by discipline rather than by CI.

Requiring the individual contexts is the obvious fix and a trap in both
directions:

  * rust.yml, formal-verification.yml and supply-chain.yml carry
    `on: pull_request: paths:`, so a PR touching none of their paths never gets
    a report from them — and a required context that never reports blocks the
    PR forever;
  * a job skipped INSIDE a workflow reports `skipped`, and on GitHub a skipped
    required context SATISFIES the merge button.

So a paths filter is a gate-disabler either way. This adds one unfiltered
workflow whose single job is the only context to require, and which judges what
the other workflows actually concluded.

Rules, all four failing closed:

  1. every completed check-run must conclude in {success, skipped, neutral} —
     ONE predicate, an allowlist, so a conclusion GitHub invents tomorrow is
     rejected rather than inherited as green;
  2. `Documentation claims hold` must be PRESENT. claim-check.yml has no paths
     filter, so its absence means it stopped running — the canary that keeps
     rule 1 from reading "everything was skipped" as mergeable;
  3. everything must be finished; hitting the deadline FAILS, because a gate
     that gives up and passes is worse than no gate;
  4. an API error, bad JSON or missing token exits non-zero. The audit's own
     finding is that a classifier's error path is usually its permissive one.

What it deliberately does NOT do: re-derive from the path globs which workflows
*should* have run. That would copy three filter lists into a fourth place, and
a copy that drifts is how this class of bug starts. The honest cost is stated in
the source — a job skipped by an in-workflow filter is taken at its word, with
rule 2 as the floor.

## The decision table found a hole in itself

`--self-test` drives 14 cases through the pure `classify()` function. Running
mutations against the FIRST draft, two of six survived:

  BLOCKING = set()                 -> 14/14 still held
  "failure" added to OK            -> 14/14 still held

Both for the same reason: a failure was rejected twice, once by a blocklist and
once by falling outside an allowlist, so either alone sufficed and neither could
be isolated. That is the same redundant-guard pattern just reported in
matrix.rs — reproduced from scratch in a new file, which is a decent argument
for how easily it happens.

Collapsed to the single allowlist, with the blocklist demoted to wording the
error message. Re-running every mutation:

  allowlist gains "failure"            13/14   caught
  allowlist accepts everything         10/14   caught
  conclusion check removed              9/14   caught
  canary presence defeated             11/14   caught
  never waits for in-progress          11/14   caught
  waits on itself (deadlock)           12/14   caught

6 of 6. The workflow runs `--self-test` as its first step, so the gate proves
itself before it judges anything.

NOT wired into branch protection by this commit. A context that has never
reported cannot be required without blocking every open PR, including the four
in this release's stack. Protection gets set after this lands and reports once.

Refs #316

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Nov 1, 2026
…ubsumed

#301 and #305 each added a post-loop guard to `verify_multi`, and #305's
terminal-hash check subsumes #301's no-delimiter check. Measured on main
@7699b3c:

  delete `matching_section_ranges.is_empty()`  -> 177 pass, 0 fail  UNDETECTED
  delete the terminal-hash check               -> 2 FAIL (split PoCs)
  delete both                                  -> the same 2 fail

So nothing isolated the guard #301's test was written for. That test was
genuinely mutation-verified when it was written — on a base where the
terminal check did not exist yet — and the subsumption arrived afterwards.
This is the sibling of a vacuous oracle: the test still asserts a true and
important property, but it can no longer tell you whether the mechanism it
names is still there.

The two guards return DIFFERENT error variants, which is what makes
separation possible: the no-delimiter guard yields `VerificationFailed`,
the terminal check `VerificationFailedForPredicates`. The test now pins the
variant instead of calling `is_err()`, and re-running the same mutation makes
it FAIL. One oracle per guard.

Not changed, deliberately: matrix.rs carries the same redundancy
(`!compared_against_a_signed_hash` and the `None` arm of the
`last_compared_hash` match are the same condition) but both return
`VerificationFailed`, so no assertion can distinguish them — and the `None`
arm cannot even be mutated away, since dropping it makes the match
non-exhaustive. Measured: deleting the flag guard there leaves all 177 tests
green. Stating that is honest; adding a test that pretends to isolate it
would not be.

Tests: wsc-verify-core 177 pass / 3 ignored, unchanged.

Refs #301, #305

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Nov 1, 2026
…#317)

Audited 2026-10-21: main's `required_status_checks.contexts` is `[]` and the
repository has no rulesets. Every check in this repo is advisory. #305, #308,
#292, #306, #310 and #297 all merged over a board nothing enforced, and the
release that is being cut right now was gated by discipline rather than by CI.

Requiring the individual contexts is the obvious fix and a trap in both
directions:

  * rust.yml, formal-verification.yml and supply-chain.yml carry
    `on: pull_request: paths:`, so a PR touching none of their paths never gets
    a report from them — and a required context that never reports blocks the
    PR forever;
  * a job skipped INSIDE a workflow reports `skipped`, and on GitHub a skipped
    required context SATISFIES the merge button.

So a paths filter is a gate-disabler either way. This adds one unfiltered
workflow whose single job is the only context to require, and which judges what
the other workflows actually concluded.

Rules, all four failing closed:

  1. every completed check-run must conclude in {success, skipped, neutral} —
     ONE predicate, an allowlist, so a conclusion GitHub invents tomorrow is
     rejected rather than inherited as green;
  2. `Documentation claims hold` must be PRESENT. claim-check.yml has no paths
     filter, so its absence means it stopped running — the canary that keeps
     rule 1 from reading "everything was skipped" as mergeable;
  3. everything must be finished; hitting the deadline FAILS, because a gate
     that gives up and passes is worse than no gate;
  4. an API error, bad JSON or missing token exits non-zero. The audit's own
     finding is that a classifier's error path is usually its permissive one.

What it deliberately does NOT do: re-derive from the path globs which workflows
*should* have run. That would copy three filter lists into a fourth place, and
a copy that drifts is how this class of bug starts. The honest cost is stated in
the source — a job skipped by an in-workflow filter is taken at its word, with
rule 2 as the floor.

## The decision table found a hole in itself

`--self-test` drives 14 cases through the pure `classify()` function. Running
mutations against the FIRST draft, two of six survived:

  BLOCKING = set()                 -> 14/14 still held
  "failure" added to OK            -> 14/14 still held

Both for the same reason: a failure was rejected twice, once by a blocklist and
once by falling outside an allowlist, so either alone sufficed and neither could
be isolated. That is the same redundant-guard pattern just reported in
matrix.rs — reproduced from scratch in a new file, which is a decent argument
for how easily it happens.

Collapsed to the single allowlist, with the blocklist demoted to wording the
error message. Re-running every mutation:

  allowlist gains "failure"            13/14   caught
  allowlist accepts everything         10/14   caught
  conclusion check removed              9/14   caught
  canary presence defeated             11/14   caught
  never waits for in-progress          11/14   caught
  waits on itself (deadlock)           12/14   caught

6 of 6. The workflow runs `--self-test` as its first step, so the gate proves
itself before it judges anything.

NOT wired into branch protection by this commit. A context that has never
reported cannot be required without blocking every open PR, including the four
in this release's stack. Protection gets set after this lands and reports once.

Refs #316


Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe added a commit that referenced this pull request Nov 1, 2026
…ubsumed

#301 and #305 each added a post-loop guard to `verify_multi`, and #305's
terminal-hash check subsumes #301's no-delimiter check. Measured on main
@7699b3c:

  delete `matching_section_ranges.is_empty()`  -> 177 pass, 0 fail  UNDETECTED
  delete the terminal-hash check               -> 2 FAIL (split PoCs)
  delete both                                  -> the same 2 fail

So nothing isolated the guard #301's test was written for. That test was
genuinely mutation-verified when it was written — on a base where the
terminal check did not exist yet — and the subsumption arrived afterwards.
This is the sibling of a vacuous oracle: the test still asserts a true and
important property, but it can no longer tell you whether the mechanism it
names is still there.

The two guards return DIFFERENT error variants, which is what makes
separation possible: the no-delimiter guard yields `VerificationFailed`,
the terminal check `VerificationFailedForPredicates`. The test now pins the
variant instead of calling `is_err()`, and re-running the same mutation makes
it FAIL. One oracle per guard.

Not changed, deliberately: matrix.rs carries the same redundancy
(`!compared_against_a_signed_hash` and the `None` arm of the
`last_compared_hash` match are the same condition) but both return
`VerificationFailed`, so no assertion can distinguish them — and the `None`
arm cannot even be mutated away, since dropping it makes the match
non-exhaustive. Measured: deleting the flag guard there leaves all 177 tests
green. Stating that is honest; adding a test that pretends to isolate it
would not be.

Tests: wsc-verify-core 177 pass / 3 ignored, unchanged.

Refs #301, #305

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH
avrabe added a commit that referenced this pull request Nov 1, 2026
…ubsumed (#315)

#301 and #305 each added a post-loop guard to `verify_multi`, and #305's
terminal-hash check subsumes #301's no-delimiter check. Measured on main
@7699b3c:

  delete `matching_section_ranges.is_empty()`  -> 177 pass, 0 fail  UNDETECTED
  delete the terminal-hash check               -> 2 FAIL (split PoCs)
  delete both                                  -> the same 2 fail

So nothing isolated the guard #301's test was written for. That test was
genuinely mutation-verified when it was written — on a base where the
terminal check did not exist yet — and the subsumption arrived afterwards.
This is the sibling of a vacuous oracle: the test still asserts a true and
important property, but it can no longer tell you whether the mechanism it
names is still there.

The two guards return DIFFERENT error variants, which is what makes
separation possible: the no-delimiter guard yields `VerificationFailed`,
the terminal check `VerificationFailedForPredicates`. The test now pins the
variant instead of calling `is_err()`, and re-running the same mutation makes
it FAIL. One oracle per guard.

Not changed, deliberately: matrix.rs carries the same redundancy
(`!compared_against_a_signed_hash` and the `None` arm of the
`last_compared_hash` match are the same condition) but both return
`VerificationFailed`, so no assertion can distinguish them — and the `None`
arm cannot even be mutated away, since dropping it makes the match
non-exhaustive. Measured: deleting the flag guard there leaves all 177 tests
green. Stating that is honest; adding a test that pretends to isolate it
would not be.

Tests: wsc-verify-core 177 pass / 3 ignored, unchanged.

Refs #301, #305


Claude-Session: https://claude.ai/code/session_012aR3Md1h46K9wAUWMQiESH

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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