Aeneas-compat: check_scalar via explicit ell-compare + from_bytes_mod_order

Replaces from_canonical_bytes (subtle CtOption / black_box machinery the
extractor cannot interpret) with an explicit little-endian comparison of
the scalar bytes against ell, then from_bytes_mod_order (the identity on
canonical input). Value-level semantics identical; the verification path is
variable-time throughout, so the constant-time construction is not required.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-04 17:41:50 +02:00
parent 35aae547a3
commit 1e860fe771

View file

@ -92,12 +92,41 @@ fn check_scalar(bytes: [u8; 32]) -> Result<Scalar, SignatureError> {
}
/// Ensures that the scalar `s` of a signature is within the bounds [0, )
///
/// AENEAS-COMPAT (formal verification): explicit little-endian comparison
/// against followed by `from_bytes_mod_order` (the identity on canonical
/// bytes) — value-level semantics identical to
/// `Scalar::from_canonical_bytes(bytes).into()`; the subtle machinery's
/// `black_box` internals defeat the extractor, and the verification path is
/// variable-time throughout.
#[cfg(not(feature = "legacy_compatibility"))]
#[inline(always)]
fn check_scalar(bytes: [u8; 32]) -> Result<Scalar, SignatureError> {
match Scalar::from_canonical_bytes(bytes).into() {
None => Err(InternalError::ScalarFormat.into()),
Some(x) => Ok(x),
/// = 2^252 + 27742317777372353535851937790883648493, little-endian.
const L_BYTES: [u8; 32] = [
237, 211, 245, 92, 26, 99, 18, 88, 214, 156, 247, 162, 222, 249, 222,
20, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 16,
];
// bytes < , most-significant byte first; the first differing byte decides.
let mut lt = false;
let mut decided = false;
let mut i = 32;
while i > 0 {
let j = i - 1;
if !decided {
if bytes[j] < L_BYTES[j] {
lt = true;
decided = true;
} else if bytes[j] > L_BYTES[j] {
decided = true;
}
}
i -= 1;
}
if lt {
Ok(Scalar::from_bytes_mod_order(bytes))
} else {
Err(InternalError::ScalarFormat.into())
}
}