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.
