From 0705315b76070497d410ed8667832db11225d00a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 4 Jul 2026 17:08:50 +0200 Subject: [PATCH] Aeneas-compat: monomorphic SHA-512 verify path + extraction-safe idioms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four pure refactors in ed25519-dalek (semantics identical, extraction only): - verifying.rs: verify_sha512/recompute_r_sha512 — the exact unrolling of raw_verify:: (None context, single message slice) with every digest-trait call behind monomorphic sha512_* wrappers, and from_hash unrolled to from_bytes_mod_order_wide(finalize(h)). The generic Digest machinery (typenum/hybrid-array) defeats the extractor's type translation. - verifying.rs: the R comparison as an explicit byte loop (derived PartialEq on CompressedEdwardsY is uninterpretable). - signature.rs from_bytes: index loops instead of range-slicing + copy_from_slice (SliceIndex const-generics wall). - signature.rs: compressed_from_bytes — an opaque constructor wrapper (aggregate construction of an extraction-opaque type crashes the translator). With these, the full verify path extracts cleanly: charon --start-from crate::verifying::{verify_sha512,recompute_r_sha512} with curve25519_dalek/sha2/digest/ed25519/signature/subtle/zeroize opaque and hybrid_array/typenum excluded. Co-Authored-By: Claude Fable 5 --- ed25519-dalek/src/signature.rs | 21 ++++++++-- ed25519-dalek/src/verifying.rs | 74 ++++++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+), 3 deletions(-) diff --git a/ed25519-dalek/src/signature.rs b/ed25519-dalek/src/signature.rs index af82768..0c39239 100644 --- a/ed25519-dalek/src/signature.rs +++ b/ed25519-dalek/src/signature.rs @@ -62,6 +62,14 @@ impl Debug for InternalSignature { } } + +/// AENEAS-COMPAT (formal verification): opaque constructor — building the +/// (extraction-opaque) `CompressedEdwardsY` aggregate directly cannot be +/// interpreted by the extractor. Semantics: the tuple constructor. +pub(crate) fn compressed_from_bytes(bytes: [u8; 32]) -> CompressedEdwardsY { + CompressedEdwardsY(bytes) +} + /// Ensures that the scalar `s` of a signature is within the bounds [0, 2^253). /// /// **Unsafe**: This version of `check_scalar` permits signature malleability. See README. @@ -150,13 +158,20 @@ impl InternalSignature { #[allow(non_snake_case)] pub fn from_bytes(bytes: &[u8; SIGNATURE_LENGTH]) -> Result { // TODO: Use bytes.split_array_ref once it’s in MSRV. + // AENEAS-COMPAT (formal verification): plain index loops instead of + // range-slicing + copy_from_slice — the SliceIndex const-generics + // machinery defeats the extractor. Semantics identical. let mut R_bytes: [u8; 32] = [0u8; 32]; let mut s_bytes: [u8; 32] = [0u8; 32]; - R_bytes.copy_from_slice(&bytes[00..32]); - s_bytes.copy_from_slice(&bytes[32..64]); + let mut i = 0; + while i < 32 { + R_bytes[i] = bytes[i]; + s_bytes[i] = bytes[i + 32]; + i += 1; + } Ok(InternalSignature { - R: CompressedEdwardsY(R_bytes), + R: compressed_from_bytes(R_bytes), s: check_scalar(s_bytes)?, }) } diff --git a/ed25519-dalek/src/verifying.rs b/ed25519-dalek/src/verifying.rs index 246951b..f42b989 100644 --- a/ed25519-dalek/src/verifying.rs +++ b/ed25519-dalek/src/verifying.rs @@ -682,3 +682,77 @@ impl<'d> Deserialize<'d> for VerifyingKey { deserializer.deserialize_bytes(VerifyingKeyVisitor) } } + +// ───────────────────────────────────────────────────────────────────────────── +// AENEAS-COMPAT (formal verification): monomorphic SHA-512 verification path. +// +// `raw_verify::`'s generic `Digest` bound drags +// the typenum/hybrid-array type-level machinery through the extractor, which +// cannot translate it (mixed type/function recursion groups). The functions +// below are the EXACT unrolling of `raw_verify::` with +// `prehash_ctx = None` and a single message slice — the path the `Verifier` +// impl takes — with the digest fixed to the concrete `Sha512` type and every +// digest-trait call isolated behind a monomorphic wrapper (extracted opaque, +// so no generic signature ever reaches the translator): +// sha512_new/sha512_update/sha512_finalize_bytes = Digest::new/update/ +// finalize∘into at D = Sha512 +// Scalar::from_hash(h) = Scalar::from_bytes_mod_order_wide(&finalize(h)) +// (from_hash's definition, unrolled) +// Semantics identical; pure refactor for extraction only. +// ───────────────────────────────────────────────────────────────────────────── + +pub(crate) fn sha512_new() -> Sha512 { + Digest::new() +} + +pub(crate) fn sha512_update(h: &mut Sha512, m: &[u8]) { + Digest::update(h, m) +} + +pub(crate) fn sha512_finalize_bytes(h: Sha512) -> [u8; 64] { + Digest::finalize(h).into() +} + +#[allow(non_snake_case)] +pub(crate) fn recompute_r_sha512( + key: &VerifyingKey, + signature: &InternalSignature, + message: &[u8], +) -> CompressedEdwardsY { + let mut h = sha512_new(); + sha512_update(&mut h, signature.R.as_bytes()); + sha512_update(&mut h, key.compressed.as_bytes()); + sha512_update(&mut h, message); + let k = Scalar::from_bytes_mod_order_wide(&sha512_finalize_bytes(h)); + + let minus_A: EdwardsPoint = -key.point; + EdwardsPoint::vartime_double_scalar_mul_basepoint(&k, &minus_A, &signature.s).compress() +} + +#[allow(non_snake_case)] +pub(crate) fn verify_sha512( + key: &VerifyingKey, + message: &[u8], + signature: &ed25519::Signature, +) -> Result<(), SignatureError> { + let signature = InternalSignature::try_from(signature)?; + let expected_R = recompute_r_sha512(key, &signature, message); + // AENEAS-COMPAT: explicit byte comparison (the derived PartialEq routes + // through machinery the extractor cannot interpret). Semantics identical + // to `expected_R == signature.R`. + let e = expected_R.as_bytes(); + let r = signature.R.as_bytes(); + let mut equal = true; + let mut i = 0; + while i < 32 { + if e[i] != r[i] { + equal = false; + } + i += 1; + } + if equal { + Ok(()) + } else { + Err(InternalError::Verify.into()) + } +}