saymrwulf/curve25519-dalek-source
1
0
Fork 0
mirror of https://github.com/saymrwulf/curve25519-dalek-source.git synced 2026-09-04 20:24:10 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Aeneas-compat: factor from_bytes_wide through named, closure-free helpers

Browse source 
Pure refactor, semantics identical (cargo check green):
- from_bytes_wide_parts(bytes) -> (Scalar52, Scalar52): the byte-unpack
  loops + the 52-bit lo/hi split, as a named prefix
- split_words_lo / split_words_hi: the two split halves, built with
  Scalar52([...]) struct literals instead of per-index mutation
- from_bytes_wide: parts -> montgomery_mul(lo, R) ->
  montgomery_mul(hi, RR) -> add

Why: the verification side measured that (a) a WP walk whose motives
contain a montgomery_mul call replays its whole body at every kernel
step, and (b) straight-line chains of IndexMut closure back-functions
make kernel defeq exponential in chain depth. Named prefix functions fix
(a); struct-literal construction eliminates the closures and fixes (b).
With this shape the full from_bytes_wide certificate kernel-checks in
77 seconds (was: aborted after 30+ minutes).
This commit is contained in:
mrwulf 2026-07-04 10:23:22 +02:00
parent b73a5480b6
commit 26284959e4
1 changed files with 45 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

67
curve25519-dalek/src/backend/serial/u64/scalar.rs
View file

@ -86,35 +86,58 @@ impl Scalar52 {
/// Reduce a 64 byte / 512 bit scalar mod l
#[rustfmt::skip] // keep alignment of lo[*] and hi[*] calculations
pub fn from_bytes_wide(bytes: &[u8; 64]) -> Scalar52 {
/// AENEAS-COMPAT: the bit-splitting prefix of `from_bytes_wide`,
/// extracted as its own function (pure refactor, semantics identical).
/// A verification-side split keeps Montgomery calls out of the
/// prefix walk's proof obligations.
/// AENEAS-COMPAT: lo-half of the 52-bit split (pure refactor; struct
/// literal instead of field mutation keeps higher-order IndexMut
/// closures out of the extraction).
fn split_words_lo(words: &[u64; 8]) -> Scalar52 {
let mask = (1u64 << 52) - 1;
Scalar52([
words[0] & mask,
((words[0] >> 52) | (words[1] << 12)) & mask,
((words[1] >> 40) | (words[2] << 24)) & mask,
((words[2] >> 28) | (words[3] << 36)) & mask,
((words[3] >> 16) | (words[4] << 48)) & mask,
])
}
/// AENEAS-COMPAT: hi-half of the 52-bit split (pure refactor, as above).
fn split_words_hi(words: &[u64; 8]) -> Scalar52 {
let mask = (1u64 << 52) - 1;
Scalar52([
(words[4] >> 4) & mask,
((words[4] >> 56) | (words[5] << 8)) & mask,
((words[5] >> 44) | (words[6] << 20)) & mask,
((words[6] >> 32) | (words[7] << 32)) & mask,
(words[7] >> 20) & mask,
])
}
/// AENEAS-COMPAT: the bit-splitting prefix of `from_bytes_wide`,
/// extracted as its own function (pure refactor, semantics identical).
/// A verification-side split keeps Montgomery calls out of the
/// prefix walk's proof obligations.
/// AENEAS-COMPAT: the bit-splitting prefix of `from_bytes_wide`,
/// factored into named halves (pure refactor, semantics identical);
/// keeps each verification walk at the proven-cheap ~25-step scale.
fn from_bytes_wide_parts(bytes: &[u8; 64]) -> (Scalar52, Scalar52) {
let mut words = [0u64; 8];
for i in 0..8 {
for j in 0..8 {
words[i] |= (bytes[(i * 8) + j] as u64) << (j * 8);
}
}
(Scalar52::split_words_lo(&words), Scalar52::split_words_hi(&words))
}
let mask = (1u64 << 52) - 1;
let mut lo = Scalar52::ZERO;
let mut hi = Scalar52::ZERO;
lo[0] = words[0] & mask;
lo[1] = ((words[0] >> 52) | (words[ 1] << 12)) & mask;
lo[2] = ((words[1] >> 40) | (words[ 2] << 24)) & mask;
lo[3] = ((words[2] >> 28) | (words[ 3] << 36)) & mask;
lo[4] = ((words[3] >> 16) | (words[ 4] << 48)) & mask;
hi[0] = (words[4] >> 4) & mask;
hi[1] = ((words[4] >> 56) | (words[ 5] << 8)) & mask;
hi[2] = ((words[5] >> 44) | (words[ 6] << 20)) & mask;
hi[3] = ((words[6] >> 32) | (words[ 7] << 32)) & mask;
// AENEAS-COMPAT: a bare `x >> c` as the full RHS extracts ill-typed
// at the pinned Aeneas (wrapping_shr with an unsubstituted i32 cast);
// masking is a semantic no-op here (words[7] >> 20 < 2^44 < 2^52).
hi[4] = (words[7] >> 20) & mask;
lo = Scalar52::montgomery_mul(&lo, &constants::R); // (lo * R) / R = lo
hi = Scalar52::montgomery_mul(&hi, &constants::RR); // (hi * R^2) / R = hi * R
pub fn from_bytes_wide(bytes: &[u8; 64]) -> Scalar52 {
let (lo, hi) = Scalar52::from_bytes_wide_parts(bytes);
let lo = Scalar52::montgomery_mul(&lo, &constants::R); // (lo * R) / R = lo
let hi = Scalar52::montgomery_mul(&hi, &constants::RR); // (hi * R^2) / R = hi * R
Scalar52::add(&hi, &lo)
}