Same refactor as the risc0 fork: the three stateful hasher wrappers
collapse into one monomorphic sha512_hash3(r, a, m) -> [u8; 64] whose
signature carries no foreign types; extraction builds with
--no-default-features (the no-std From<InternalError> branch avoids the
boxed dyn-Error source path). Semantically Sha512 over r || a || m.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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>
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: remove `ExpandedSecretKey::to_bytes`
The reason `ExpandedSecretKey` needs a private `scalar_bytes` field is
to retain the canonical scalar bytes as output by SHA-512 during key
expansion so they can be serialized by the `to_bytes` method.
However, `ExpandedSecretKey`s should not be serialized to the wire.
Removing this method allows the private field to be removed, which
allows `ExpandedSecretKey` to be constructed entirely from public
fields. This provides an alternative to #544 for use cases like
Ed25519-BIP32 where the private scalar is derived rather than clamped
from bytes.
One other change is needed: `to_scalar_bytes` was changed to `to_scalar`
as the canonical scalar bytes are no longer retained, however this has
no impact on its main use case, X25519 Diffie-Hellman exchanges, where
the `Scalar` should NOT be written to the wire anyway.
* Added scalar byte comparison back to ed25519-dalek x25519 test
---------
Co-authored-by: Michael Rosenberg <michael@mrosenberg.pub>
