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>
External review round 2 (GPT B1.5) flagged that no Cargo.lock was committed
and the extraction toolchain was undocumented. Fixes:
- Un-ignore and commit Cargo.lock (this is a verification-pinned snapshot, not
a library — a locked dependency graph is part of the reproducible artifact).
- Add rust-toolchain.toml pinning nightly-2026-06-01, the exact channel the
Charon/Aeneas transpiler uses, so `charon cargo` extraction and the `cargo
test` differential harness agree on one compiler.
Verified: re-running verification/extract.sh against this tree reproduces
gen/SlhVerify/{Types,Funs}.lean BYTE-IDENTICALLY (sha256 unchanged) — these
additions do not perturb the extracted Lean model.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Removes the last two untranslatable iterator adapters on the verify path so
their loops extract to real definitions (no Take/IterMut axioms in any cone):
- to_int: `for item in x.iter().take(n)` -> `for i in 0..n { ... x[i] }`. The
Take adapter was the LAST non-oracle, non-zeroize axiom in the model.
- base_2b: `for item in baseb.iter_mut()` -> `for out in 0..out_len { ...;
baseb[out] = ... }`. The IterMut adapter carried a next_back write-back
closure as loop state (a function-typed fixpoint), painful to reason about.
Both are semantics-identical for every FIPS 205 parameter set: the asserts
already pin x.len()==n and out_len==baseb.len(), so the index ranges visit
exactly the same elements/slots in the same order with the same values. The
inner `while bits < b` loop of base_2b was already clean and is untouched.
Validation: cargo test --features slh_dsa_sha2_128s --lib green — all 12
parameter-set round trips AND mono_matches_deployed_verify (mono == deployed
generic verify on valid / corrupted / wrong-message inputs).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Aeneas translates the affected core-library instances only as axioms
(TryFrom/unwrap Result plumbing, iterator adapters, the &u32 Sub instance),
which would put transpiler axioms into certificate cones. Each site is
replaced by a construct that extracts to a real definition, with identical
semantics for every FIPS 205 parameter set:
- wots/xmss/ht/fors/slh const-generic preps: u32::try_from(X).unwrap() ->
X as u32 (every parameter <= 63; cast lossless).
- wots checksum loop: msg.iter().take(2*N) with &u32 subtraction -> index
loop over 0..2*N with value reads (same iteration space, same values).
- ht per-layer idx_leaf and slh idx_leaf: u32::try_from + is_err/unwrap ->
plain cast. Both values are pre-masked to hp' resp. h/d bits, and hp',
h/d <= 9 for every FIPS 205 parameter set, so the conversion cannot
fail: the removed error branch is dead code.
Validation: cargo test --features slh_dsa_sha2_128s --lib green — all 12
parameter-set round trips AND the differential test
mono_matches_deployed_verify (mono verify == deployed generic verify on
valid / corrupted / wrong-message inputs).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Two further transpiler-compat refinements found while extracting (Aeneas
reported one Unimplemented in slh_verify_internal_free):
- h_msg / slh_verify take the message-digest input M' as a SINGLE
contiguous &[u8] instead of &[&[u8]] (nested slices are untranslatable;
the dalek verify_sha512 single-message-slice lesson). H_msg hashes the
byte concatenation, so a pre-concatenated M' is bit-identical — the
differential test builds M' = toByte(0,1)||toByte(0,1)||<>||msg and
still agrees with the deployed verifier.
- the one let-else (u32::try_from(idx_leaf) else return false) rewritten
to the translatable is_err/unwrap idiom already used in ht_verify.
Result: charon + aeneas both exit 0 on the verify cone; the extracted
Lean model type-checks. Differential test still passes; default-feature
build still clean (additive).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The generic verify path threads the six hash primitives through
crate::hashers::Hashers, a struct of fn() POINTERS, which the Aeneas
Rust->Lean transpiler cannot translate (the sole gate-0 obstruction).
This adds src/verify_mono.rs: the verify cone (chain, wots_pk_from_sig,
xmss_pk_from_sig, ht_verify, fors_pk_from_sig, slh_verify_internal)
reproduced with the hash suite reached through NAMED free functions in a
verify_mono::oracle module (the deliberate SHA-2 opaque boundary of the
proof) instead of fn-pointer dereferences, plus a monomorphic entry
slh_verify_128s fixing the SLH-DSA-SHA2-128s constants. Function bodies
are copied verbatim from wots/xmss/hypertree/fors/slh so the extracted
Lean model stays faithful to the deployed algorithm.
Additive and inert: gated behind feature slh_dsa_sha2_128s; the only
change to existing code is two lines declaring the module. All twelve
parameter sets build unchanged (cargo build default features: clean).
Fidelity is pinned by an in-crate differential unit test that pits
slh_verify_128s against the deployed Verifier::verify on freshly
generated signatures — valid (both accept), corrupted (both reject),
and wrong-message (both reject), across three keypairs. Passes.
Same pattern as the curve25519-dalek-source verify_sha512 shim. This is
a frozen snapshot for the formal-verification campaign; no affiliation
with, and no changes proposed to, the upstream project.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This is a frozen snapshot for the SLH-DSA verification campaign, pinned
at upstream 30bac08. Upstream's CI does not belong in this namespace
(and must not run here); removing .github is the only deviation from
verbatim. Upstream history is fully preserved beneath this commit.
No affiliation with, and no changes proposed to, the upstream project.
