Aeneas-compat: mask the bare shift in Scalar52::from_bytes_wide

hi[4] = words[7] >> 20  is the only shift in the function whose result is
stored without a trailing mask/or; at the pinned Aeneas (bf13c42e) a bare
`x >> c` as a full RHS extracts ill-typed (wrapping_shr applied to an i32
with an emitted-but-unsubstituted U32 cast). Masking is a semantic no-op:
words[7] >> 20 < 2^44 < 2^52.  Semantics unchanged; needed to bring
from_bytes_wide (the hash-to-scalar reduction) into verification scope.
This commit is contained in:
mrwulf 2026-07-03 22:40:03 +02:00
parent 64ee8f0ef3
commit 87928d7896

View file

@ -106,7 +106,10 @@ impl Scalar52 {
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;
hi[4] = words[7] >> 20 ;
// 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