From bea105195b8ec874026224005a63b920557b7e63 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 24 Jul 2026 08:47:15 +0200 Subject: [PATCH] =?UTF-8?q?helpers:=20de-plumb=20round=202=20=E2=80=94=20t?= =?UTF-8?q?o=5Fint=20&=20base=5F2b=20iterators=20to=20index=20loops?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/helpers.rs | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/helpers.rs b/src/helpers.rs index 6987f6e..6f85746 100644 --- a/src/helpers.rs +++ b/src/helpers.rs @@ -14,10 +14,13 @@ pub(crate) fn to_int(x: &[u8], n: u32) -> u64 { let mut total = 0; // 2: for i from 0 to n − 1 do - for item in x.iter().take(n as usize) { + // Aeneas-compat: index loop instead of iter().take() (the Take iterator + // adapter is untranslatable-clean; x.len() == n by the assert above, so + // 0..n indexes exactly the same elements in the same order — identical). + for i in 0..(n as usize) { // // 3: total ← 256 · total + X[i] - total = (total << 8) + u64::from(*item); + total = (total << 8) + u64::from(x[i]); // 4: end for } @@ -77,7 +80,11 @@ pub(crate) fn base_2b(x: &[u8], b: u32, out_len: u32, baseb: &mut [u32]) { let mut total = 0; // 4: for out from 0 to out_len − 1 do - for item in baseb.iter_mut() { + // Aeneas-compat: index loop instead of iter_mut() (the IterMut adapter with + // its next_back write-back closure is untranslatable-clean; out_len == + // baseb.len() by the assert above, so 0..out_len writes exactly the same + // slots in the same order with the same values — identical). + for out in 0..(out_len as usize) { // // 5: while bits < b do while bits < b { @@ -98,7 +105,7 @@ pub(crate) fn base_2b(x: &[u8], b: u32, out_len: u32, baseb: &mut [u32]) { bits -= b; // 11: baseb[out] ← (total ≫ bits) mod 2^b - *item = (total >> bits) & (u32::MAX >> (32 - b)); + baseb[out] = (total >> bits) & (u32::MAX >> (32 - b)); // 12: end for }