mirror of
https://github.com/saymrwulf/curve25519-dalek-source.git
synced 2026-09-03 20:13:48 +00:00
Patched source for Aeneas/Charon formal verification transpilation
mrwulf
35aae547a3
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>
|
||
|---|---|---|
| curve25519-dalek | ||
| curve25519-dalek-derive | ||
| docs/assets | ||
| ed25519-dalek | ||
| x25519-dalek | ||
| .gitignore | ||
| .typos.toml | ||
| Cargo.lock | ||
| Cargo.toml | ||
| CONTRIBUTING.md | ||
| README.md | ||
Dalek elliptic curve cryptography
This repo contains pure-Rust crates for elliptic curve cryptography:
| Crate | Description | Crates.io | Docs | CI |
|---|---|---|---|---|
curve25519‑dalek |
A library for arithmetic over the Curve25519 and Ristretto elliptic curves and their associated scalars. |  |
 |
 |
ed25519‑dalek |
An implementation of the EdDSA digital signature scheme over Curve25519. |  |
 |
 |
x25519‑dalek |
An implementation of elliptic curve Diffie-Hellman key exchange over Curve25519. |  |
 |
 |
There is also the curve25519-dalek-derive crate, which is just a helper crate with some macros that make curve25519-dalek easier to write.
Contributing
Please see CONTRIBUTING.md.
Code of Conduct
We follow the Rust Code of Conduct, with the following additional clauses:
- We respect the rights to privacy and anonymity for contributors and people in the community. If someone wishes to contribute under a pseudonym different to their primary identity, that wish is to be respected by all contributors.