Aeneas-compat: index-based LE word load in non_adjacent_form

Pure refactor, semantics identical: the read_le_u64_into call (whose
chunks/zip iterators are opaque to the extraction) becomes an explicit
nested index loop, the same shape as the proven from_bytes_wide unpack.
With this the entire vartime_double_base::mul extraction closure is
self-contained: zero external axioms, zero sorries.
This commit is contained in:
mrwulf 2026-07-04 11:39:11 +02:00
parent 58894a049a
commit 1c8497d682

View file

@ -1034,7 +1034,20 @@ impl Scalar {
let mut naf = [0i8; 256];
let mut x_u64 = [0u64; 5];
read_le_u64_into(&self.bytes, &mut x_u64[0..4]);
// AENEAS-COMPAT: index-based little-endian load instead of
// read_le_u64_into (its chunks/zip iterators are opaque to the
// extraction). Pure refactor, semantics identical.
let mut k: usize = 0;
while k < 4 {
let mut t: u64 = 0;
let mut bi: usize = 0;
while bi < 8 {
t |= (self.bytes[8 * k + bi] as u64) << (8 * bi);
bi += 1;
}
x_u64[k] = t;
k += 1;
}
let width = 1 << w;
let window_mask = width - 1;