Same documented rewrite as FieldElement::sqrt_ratio_i: semantically
identical and still constant-time, but avoids subtle's
ConditionallyNegatable blanket impl, which the verification toolchain
cannot translate. Unblocks extracting decompress for the phase-2 full
point-level lift.
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>
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>
Pure refactor, semantics identical: the read_le_u64_into call (whose
chunks/zip iterators are opaque to the extraction) becomes an explicit
nested index loop, the same shape as the proven from_bytes_wide unpack.
With this the entire vartime_double_base::mul extraction closure is
self-contained: zero external axioms, zero sorries.
Pure refactors (cargo check green under both feature sets), semantics of
mul unchanged:
- dsm_top_index / dsm_loop / dsm_step_p / dsm_step_b helpers: the main
double-and-add loop becomes a strictly-decreasing while with a
single-assignment body and parameter-rooted borrows (the original
loop/break shape with match-updates fails Aeneas' loop fixed point);
- the starting-index scan always returns 255: leading zero NAF digits
double the identity (a no-op), so the result is unchanged - only the
variable-time skip is dropped (constant-time behavior improves);
- the downward break-scan (which failed Aeneas' symbolic join) is gone.
With these, Charon+Aeneas extract the complete path - non_adjacent_form,
NafLookupTable5::from/select, the affine basepoint table, the 256-step
dsm_loop, and mul - with zero errors and zero sorries. This opens the
double-scalar-multiplication verification campaign (the EdDSA verify
equation's core).
Pure refactor, semantics identical (cargo check green):
- from_bytes_wide_parts(bytes) -> (Scalar52, Scalar52): the byte-unpack
loops + the 52-bit lo/hi split, as a named prefix
- split_words_lo / split_words_hi: the two split halves, built with
Scalar52([...]) struct literals instead of per-index mutation
- from_bytes_wide: parts -> montgomery_mul(lo, R) ->
montgomery_mul(hi, RR) -> add
Why: the verification side measured that (a) a WP walk whose motives
contain a montgomery_mul call replays its whole body at every kernel
step, and (b) straight-line chains of IndexMut closure back-functions
make kernel defeq exponential in chain depth. Named prefix functions fix
(a); struct-literal construction eliminates the closures and fixes (b).
With this shape the full from_bytes_wide certificate kernel-checks in
77 seconds (was: aborted after 30+ minutes).
hi[4] = words[7] >> 20 is the only shift in the function whose result is
stored without a trailing mask/or; at the pinned Aeneas (bf13c42e) a bare
`x >> c` as a full RHS extracts ill-typed (wrapping_shr applied to an i32
with an emitted-but-unsubstituted U32 cast). Masking is a semantic no-op:
words[7] >> 20 < 2^44 < 2^52. Semantics unchanged; needed to bring
from_bytes_wide (the hash-to-scalar reduction) into verification scope.
* Revert "curve: Remove ff/group features for now (#907)"
This reverts commit 13ac5e66a7.
* Fix build
* Remove group-bits features for soundness concerns
* Update changelog
* [WIP] ed25519-dalek: bump `ed25519` crate dependency to v3.0.0
This has two test failures:
serialisation::serialize_deserialize_signature_json
serialisation::serialize_signature_size
These are due to a last minute change to use `serdect` for implementing
`serde` support: RustCrypto/signatures#1324.
The signature size regression from `64` to `72` is a deliberate tradeoff
we've accepted in `serdect`. First note that this test is for now the
unmaintained `bincode` crate.
The core problem is that `serde` does not actually provide fixed-size
arrays as a type within its data model (serde-rs/serde#1937) and you're
instead left faking it using `SerializeTuple` and serializing it a
byte-at-a-time as a tuple. While this gives optimal-sized results on
`bincode`, it gives less-than-optimal results on e.g. `rmp-serde` where
the bytes each end up tagged with a type prefix.
`serde` does provide portable APIs for using optimal format-specific
byte encodings, but they carry an additional length prefix, which is
unnecessary and suboptimal for something fixed-width like an Ed25519
signature, but alas as noted earlier `serde` does not actually have
fixed-width arrays in its data model.
The second test failure occurs specifically because `serdect`
introspects the format and uses `base16ct` to perform hex serialization
for human readable formats. While this is a readability improvement for
these formats (and also makes them easier to implement in constant-time,
though it's not relevant here), the drawback is it currently requires
the `alloc` feature for such formats, which is a regression:
Error("serializer is human readable, which requires the `alloc` crate feature", line: 0, column: 0)
Note that regardless these are both breaking changes to how `serde`
serialization is handled.
See also:
- RustCrypto/formats#1111
- RustCrypto/formats#1112
- dalek-cryptography/ed25519-dalek#140
* Migrate bincode -> postcard
* Bump `serdect` to v0.4.3
Includes `no_alloc` hex serialization support
---------
Co-authored-by: Michael Rosenberg <mrosenberg@cloudflare.com>
This bumps `pkcs8`, `signature`, `spki`, `sha3`, and `der` to newly released versions.
This also bumps the version of `blake2`, `rustcrypto-ff`,
`rustcrypto-group`, and `ed25519` to their latest pre-released versions.
Adds a table of low order points, adapted from
https://cr.yp.to/ecdh.html, which suggests that non-Diffie-Hellman
protocols that depend on "contributory" behavior should reject them.
They're also useful for testing, e.g. how a protocol implementation
handles them during a key exchange (noting that a well-implemented AKE
shouldn't need to explicitly reject them, as someone attempting to use
them for MitM should be spotted as a transcript mismatch).
rust-random/rand#1697 which updates `rand_core` to v0.10.0-rc-3 for the
`rand` crate has been merged.
This removes `patch.crates-io` for `getrandom` and pins to the merged
commit revision for `rand`, as well as bumping the `getrandom`
dependency of `x25519-dalek` to v0.4.0-rc.0.
Most of the changes in this PR are actually from the associated `rand`
crate updates which are happening in rust-random/rand#1697, notably
`OsRng` has been renamed to `SysRng` (and is now provided by the
`getrandom` crate).
We do use some `rand_core` APIs in a few places though, like the STROBE
implementation, where this migrates from `rand_core::le` to
`rand_core::utils`.
* Clarify features in x25519 README
* Remove alloc feature from x25519 bc it was doing nothing
* Add pubkey constructor benchmark
* Correct code size claim on README
* Update changelog
Prior to a final stable release of the @RustCrypto dependencies used by
the dalek crates, we are going to target `rand_core` v0.10.
This updates the `rand` and `rand_core` dependencies as well as the
aforementioned @RustCrypto dependencies to be compatible with
`rand_core` v0.10, which incurred a few API changes:
- `rand_core` no longer includes `OsRng`, so this replaces the `os_rng`
features with `getrandom` features (same thing we did for @RustCrypto)
which uses the `getrandom` crate directly
- For `dev-dependencies` it just migrates straight to `rand`, replacing
`rand_chacha` with the `chacha` feature of `rand` (which pulls in
`chacha20`), and sourcing `OsRng` from `rand`, its new home (for now)
This PR also switches to using the `rustcrypto-ff`/`rustcrypto-group` crates
(hopefully temporary) which are forks of `ff` and `group` which have crate
releases that have been updated to use `rand_core` v0.10.0 prereleases.
Enforced via the newly added `clippy::mod_module_files` lint.
Previously a mixture of 2015 (`mod.rs`) module files along with
the 2018 `foo.rs` and `foo/` approach.
All of the toplevel modules (`edwards`, `field`, `montgomery`, and
`scalar`) were using the 2018 convention, except for `backend`,
`ristretto`, and the recently added `lizard` were using the 2015
convention.
This renames the files so everything follows the 2018 convention, and
applies the afforementioned clippy lint which will error if anyone tries
to add new files using the 2015 convention.
* Vendor lizard hash to curve from Signal
* Add invalid Lizard encoding test
* Added lizard details to readme and changelog
* Upgrade ristretto.sage to Python3
* Add lizard test vector generation to ristretto.sage
* Added map_to_curve and its inverse
* Use CtOption instead of bitmasks; other cleanup
* Add README to lizard folder
* Split map_to_curve into map_to_curve and map_to_curve_restricted; make its inverse return 16 elements
* Consolidate Ristretto Elligator functions into its own file
