Aeneas-compat: monomorphic SHA-512 verify path + extraction-safe idioms

Four pure refactors in ed25519-dalek (semantics identical, extraction only):
- verifying.rs: verify_sha512/recompute_r_sha512 — the exact unrolling of
  raw_verify::<Sha512> (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<OutputSize = U64> 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 <noreply@anthropic.com>

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<InternalSignature, SignatureError> {
         // 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)?,
         })
     }

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::<CtxDigest>`'s generic `Digest<OutputSize = U64>` 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::<Sha512>` 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())
+    }
+}