Round-8 review found a tautological assert in this script — it compared a dict
against the comprehension that had just built it, so it could never fire, in the
very script written to fix a provenance-honesty defect. The first repair
(comparing kept[k] to t[k]) was tautological for the same reason; a negative test
confirmed it did not catch a tampered input.
No check inside a transformer can detect a corrupted input, because the
transformer is what defines the output from that input. Both vacuous checks are
removed and the lesson is recorded in the code. The header and the embedded
_provenance now say that fields are carried through BY CONSTRUCTION — a property
a reviewer reads — and name the guarantees that can actually fail: the pinned
upstream SOURCE_SHA256, the requirement that sk be present to be dropped, the
expected group and per-group test counts, and verify mode's byte-comparison of
the committed file. The last two were negative-tested: removing sk aborts with
'has no field sk to drop', deleting a test aborts with 'group 19 has 13 tests'.
The script is also now described as re-runnable EVIDENCE rather than a gate: it
needs network access, so nothing invokes it automatically.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Round-7 review (both reviewers, independently) found that the ACVP provenance
note said "the per-test private key `sk` dropped ... Nothing else altered" while
the extraction had in fact also dropped `additionalRandomness` and `deferred`
from all 42 tests, plus the top-level `isSample`. No field the tests consume was
affected and no verdict changed — but the provenance block is the audit trail a
third party diffs against, and as written it would have produced a false alarm
or taught the next reviewer to wave differences through.
Rather than reword the note, the transformation is now executable and pinned:
tests/nist_acvp_vectors/extract_sha2_128s.py re-derives the file, verifies the
upstream sha256 before doing anything, requires exactly 3 groups x 14 tests,
removes exactly ONE field (`sk`) and asserts that invariant, carries every other
per-test, group and top-level key through untouched, and writes canonical
output. Run with no arguments it VERIFIES the committed file against a fresh
extraction; --write regenerates. The file was regenerated with it, so
"only `sk` removed" is now literally true and machine-checkable.
Also from round 7, precision in the tests themselves:
- exact assertions replace floors: `points == 108` (was >= 100),
`with_ctx == 9` (was > 0), and prehash `3/4/7` (was `checked > 0`). With 7 of
14 prehash vectors skipped for unimplemented hash functions, a floor would
have let real coverage fall from 3 to 1 while the total still summed to 14.
- the randomized bridge's doc comment claimed corruption "across the WHOLE
signature"; measured, the schedule hits 72 distinct positions in 11..=7779,
never bytes 0-10 or 7780-7855. Corrected to the measured statement.
Verified on stable Rust (rustc 1.95) as well as the pinned nightly: the bridge
needs no nightly feature, so a third party can run all of it with cargo alone.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
External review flagged across rounds 4-6 that the empirical evidence tying the
proved model to the deployed code had not moved by a single data point in six
rounds: the sole bridge was nine assertion points (3 rounds, one fixed seed,
corruption always at byte 100), and the ACVP vectors vendored here contain NO
SLH-DSA-SHA2-128s sigVer group at all — the one parameter set this verification
campaign is about had zero NIST known-answer verification coverage.
VECTORS. tests/nist_acvp_vectors/SLH-DSA-sigVer-FIPS205/sha2_128s_extracted.json
carries the three SHA2-128s sigVer groups extracted verbatim from the official
NIST ACVP-Server vector set (source URL, upstream file sha256 and extraction
method recorded in the file's own _provenance block; per-test private keys
dropped as unnecessary to verify). 42 tests: 2 valid and 12 negative per group,
the negatives spread over structurally distinct corruption sites — modified R,
modified SIGFORS, modified SIGHT, modified message, too-small and too-large
signatures.
TESTS (all in src/verify_mono.rs, so they exercise the monomorphic path the Lean
certificates are about):
- mono_matches_nist_acvp_128s_internal — NIST's `internal` group carries M'
directly, which is exactly what slh_verify_128s consumes, so these are true
known-answer tests OF THE PROVED PATH: 10 executed, 4 attributed to
deserialization (wrong-length signatures, rejected above the extraction root).
Accounting is exact — all 14 are accounted for, nothing silently skipped.
- mono_matches_nist_acvp_128s_external_pure — builds M' the way lib.rs does and
requires mono, the deployed verifier and NIST to agree: 10 executed, 9 of them
with a NON-EMPTY context. This is the first empirical check of the
domain-separator byte and context-length prefix that TRUSTED-BASE item 10
declares outside every proof.
- deployed_matches_nist_acvp_128s_prehash — validates the deployed prehash path
for 128s: 3 executed, 4 wrong-length, and 7 skipped because NIST exercises
prehash functions (SHA3-*, truncated SHA2) this crate's `Ph` enum does not
implement. Counted and reported rather than hidden.
- mono_matches_deployed_randomized — replaces the fixed-seed/fixed-byte bridge:
12 rounds, varying message lengths including empty, corruption spread across
the WHOLE 7856-byte signature, plus wrong-public-key and wrong-context cases
that were never exercised before. 108 assertion points, each requiring mono
and deployed to agree.
Bridge coverage: 9 assertion points -> 131, of which 20 are NIST known-answer
tests on the proved path where there were previously none.
No change to any verify-path function: this commit touches test code and test
data only, so the Charon/Aeneas extraction is unaffected (verified separately by
re-running extract.sh and diffing the generated model).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
