From 7f89a3ee10b5a1164d94fb855469c1de51583b74 Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Sat, 4 Jul 2026 18:00:28 +0200
Subject: [PATCH] Aeneas-compat: rename verify params signature->sig (namespace
 shadowing)

The extractor's generated Lean would otherwise shadow the signature:: crate
namespace with the parameter binder, turning module paths into invalid field
projections. Pure rename.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 ed25519-dalek/src/verifying.rs | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/ed25519-dalek/src/verifying.rs b/ed25519-dalek/src/verifying.rs
index 8600241..cd49a3f 100644
--- a/ed25519-dalek/src/verifying.rs
+++ b/ed25519-dalek/src/verifying.rs
@@ -783,32 +783,34 @@ pub(crate) fn sha512_finalize_bytes(h: Sha512) -> [u8; 64] {
 #[allow(non_snake_case)]
 pub(crate) fn recompute_r_sha512(
     key: &VerifyingKey,
-    signature: &InternalSignature,
+    sig: &InternalSignature,
     message: &[u8],
 ) -> CompressedEdwardsY {
     let mut h = sha512_new();
-    sha512_update(&mut h, signature.R.as_bytes());
+    sha512_update(&mut h, sig.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()
+    EdwardsPoint::vartime_double_scalar_mul_basepoint(&k, &minus_A, &sig.s).compress()
 }
 
 #[allow(non_snake_case)]
 pub(crate) fn verify_sha512(
     key: &VerifyingKey,
     message: &[u8],
-    signature: &ed25519::Signature,
+    sig: &ed25519::Signature,
 ) -> Result<(), SignatureError> {
-    let signature = InternalSignature::try_from(signature)?;
-    let expected_R = recompute_r_sha512(key, &signature, message);
+    // (parameter named `sig`, not `signature`: the extractor's generated
+    // code would otherwise shadow the `signature::` crate namespace)
+    let sig = InternalSignature::try_from(sig)?;
+    let expected_R = recompute_r_sha512(key, &sig, 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 r = sig.R.as_bytes();
     let mut equal = true;
     let mut i = 0;
     while i < 32 {