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.
