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>
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>
