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>
