From 6f6a9d65e7e6e79d4220ffdfe216b15616e07620 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 23 Jul 2026 17:04:52 +0200 Subject: [PATCH] verify_mono: de-plumb Result/iterator idioms (8 sites, semantics identical) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/verify_mono.rs | 39 +++++++++++++++++++++------------------ 1 file changed, 21 insertions(+), 18 deletions(-) diff --git a/src/verify_mono.rs b/src/verify_mono.rs index a1ea17f..3364129 100644 --- a/src/verify_mono.rs +++ b/src/verify_mono.rs @@ -107,7 +107,9 @@ pub(crate) fn chain_free( pub(crate) fn wots_pk_from_sig_free( sig: &WotsSig, m: &[u8], pk_seed: &[u8], adrs: &Adrs, ) -> WotsPk { - let n32 = u32::try_from(N).unwrap(); + // Aeneas-compat: plain cast for const-generic params (Result plumbing is + // untranslatable-clean; every FIPS 205 parameter is <= 63, cast lossless). + let n32 = N as u32; let mut adrs = adrs.clone(); let mut tmp = [[0u8; N]; LEN]; @@ -115,8 +117,10 @@ pub(crate) fn wots_pk_from_sig_free( let mut msg = [0u32; LEN]; base_2b(m, crate::LGW, 2 * n32, &mut msg[0..(2 * N)]); - for item in msg.iter().take(2 * N) { - csum += crate::W - 1 - item; + // Aeneas-compat: index loop with value reads (iterator adapters and the + // &u32 Sub instance are untranslatable); same first-2N iteration space. + for i in 0..(2 * N) { + csum += crate::W - 1 - msg[i]; } csum <<= (8 - ((crate::LEN2 * crate::LGW) & 0x07)) & 0x07; @@ -152,7 +156,7 @@ pub(crate) fn wots_pk_from_sig_free( pub(crate) fn xmss_pk_from_sig_free( idx: u32, sig_xmss: &XmssSig, m: &[u8], pk_seed: &[u8], adrs: &Adrs, ) -> [u8; N] { - let hp32 = u32::try_from(HP).unwrap(); + let hp32 = HP as u32; // Aeneas-compat: lossless (HP <= 63 in all sets) let mut adrs = adrs.clone(); adrs.set_type_and_clear(WOTS_HASH); @@ -191,7 +195,7 @@ pub(crate) fn ht_verify_free bool { let mut idx_tree = idx_tree; - let (d32, hp32) = (u32::try_from(D).unwrap(), u32::try_from(HP).unwrap()); + let (d32, hp32) = (D as u32, HP as u32); // Aeneas-compat: lossless casts let mut adrs = Adrs::default(); adrs.set_tree_address(idx_tree); @@ -200,11 +204,11 @@ pub(crate) fn ht_verify_free(idx_leaf, &sig_tmp, m, pk_seed, &adrs); for j in 1..d32 { - let idx_leaf = u32::try_from(idx_tree & ((1 << hp32) - 1)); - if idx_leaf.is_err() { - return false; - }; - let idx_leaf = idx_leaf.unwrap(); + // Aeneas-compat: plain cast (Result plumbing untranslatable-clean). + // The value is masked to hp' bits and hp' <= 9 for every FIPS 205 + // parameter set, so the u32 conversion cannot fail: identical. + #[allow(clippy::cast_possible_truncation)] + let idx_leaf = (idx_tree & ((1 << hp32) - 1)) as u32; idx_tree >>= hp32; @@ -224,7 +228,7 @@ pub(crate) fn ht_verify_free( sig_fors: &ForsSig, md: &[u8], pk_seed: &[u8], adrs: &Adrs, ) -> ForsPk { - let (a32, k32) = (u32::try_from(A).unwrap(), u32::try_from(K).unwrap()); + let (a32, k32) = (A as u32, K as u32); // Aeneas-compat: lossless casts let mut adrs = adrs.clone(); let mut indices = [0u32; K]; @@ -281,7 +285,7 @@ pub(crate) fn slh_verify_internal_free< >( mprime: &[u8], sig: &SlhDsaSig, pk: &SlhPublicKey, ) -> bool { - let (d32, h32) = (u32::try_from(D).unwrap(), u32::try_from(H).unwrap()); + let (d32, h32) = (D as u32, H as u32); // Aeneas-compat: lossless casts let mut adrs = Adrs::default(); @@ -308,12 +312,11 @@ pub(crate) fn slh_verify_internal_free< adrs.set_tree_address(idx_tree); adrs.set_type_and_clear(FORS_TREE); - // Aeneas-compat: is_err/unwrap idiom (translatable) instead of let-else. - let idx_leaf_u32 = u32::try_from(idx_leaf); - if idx_leaf_u32.is_err() { - return false; - } - let idx_leaf_u32 = idx_leaf_u32.unwrap(); + // Aeneas-compat: plain cast (Result plumbing untranslatable-clean). The + // value is masked to h/d bits above and h/d <= 9 for every FIPS 205 + // parameter set, so the u32 conversion cannot fail: identical. + #[allow(clippy::cast_possible_truncation)] + let idx_leaf_u32 = idx_leaf as u32; adrs.set_key_pair_address(idx_leaf_u32); let pk_fors = fors_pk_from_sig_free::(sig_fors, md, &pk.pk_seed, &adrs);