saymrwulf/risc0-curve25519-dalek-source
1
0
Fork 0
mirror of https://github.com/saymrwulf/risc0-curve25519-dalek-source.git synced 2026-09-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Aeneas-compat: decompress step_2 negate-then-conditional-assign

Browse source 
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>
This commit is contained in:
mrwulf 2026-07-06 01:41:54 +02:00
parent f17cbd1a19
commit d58065f735
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
curve25519-dalek/src/edwards.rs
View file

@ -116,7 +116,6 @@ use {
use rand_core::RngCore; use rand_core::RngCore;
use subtle::Choice; use subtle::Choice;
use subtle::ConditionallyNegatable;
use subtle::ConditionallySelectable; use subtle::ConditionallySelectable;
use subtle::ConstantTimeEq; use subtle::ConstantTimeEq;
@ -229,7 +228,13 @@ mod decompress {
// FieldElement::sqrt_ratio_i always returns the nonnegative square root, // FieldElement::sqrt_ratio_i always returns the nonnegative square root,
// so we negate according to the supplied sign bit. // so we negate according to the supplied sign bit.
let compressed_sign_bit = Choice::from(repr.as_bytes()[31] >> 7); let compressed_sign_bit = Choice::from(repr.as_bytes()[31] >> 7);
X.conditional_negate(compressed_sign_bit); // AENEAS-COMPAT: negate-then-conditional-assign instead of
// `X.conditional_negate(...)` — semantically identical and still
// constant-time, but avoids subtle's `ConditionallyNegatable`
// blanket impl which breaks the verification toolchain (the same
// documented rewrite as in `FieldElement::sqrt_ratio_i`).
let X_neg = -&X;
X.conditional_assign(&X_neg, compressed_sign_bit);
EdwardsPoint { EdwardsPoint {
X, X,