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

patch: remove ConditionallyNegatable for Aeneas/Charon transpilation

Browse source 
Upstream: dalek-cryptography/curve25519-dalek v5.0.0-rc.1
Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c
This commit is contained in:
mrwulf 2026-06-30 17:30:35 +02:00
parent 4cf8db2369
commit 8fa9083e12
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
curve25519-dalek/src/field.rs
View file

@ -28,7 +28,6 @@
use cfg_if::cfg_if; use cfg_if::cfg_if;
use subtle::Choice; use subtle::Choice;
use subtle::ConditionallyNegatable;
use subtle::ConditionallySelectable; use subtle::ConditionallySelectable;
use subtle::ConstantTimeEq; use subtle::ConstantTimeEq;
@ -357,8 +356,14 @@ impl FieldElement {
r.conditional_assign(&r_prime, flipped_sign_sqrt | flipped_sign_sqrt_i); r.conditional_assign(&r_prime, flipped_sign_sqrt | flipped_sign_sqrt_i);
// Choose the nonnegative square root. // Choose the nonnegative square root.
//
// NOTE: written as negate-then-conditional-assign rather than
// `r.conditional_negate(r_is_negative)`: semantically identical and
// still constant-time, but it avoids subtle's `ConditionallyNegatable`
// blanket impl which breaks the Aeneas verification toolchain.
let r_is_negative = r.is_negative(); let r_is_negative = r.is_negative();
r.conditional_negate(r_is_negative); let r_neg = -&r;
r.conditional_assign(&r_neg, r_is_negative);
let was_nonzero_square = correct_sign_sqrt | flipped_sign_sqrt; let was_nonzero_square = correct_sign_sqrt | flipped_sign_sqrt;
@ -518,6 +523,7 @@ where
#[cfg(test)] #[cfg(test)]
mod test { mod test {
use crate::field::*; use crate::field::*;
use subtle::ConditionallyNegatable;
/// Random element a of GF(2^255-19), from Sage /// Random element a of GF(2^255-19), from Sage
/// a = 1070314506888354081329385823235218444233221\ /// a = 1070314506888354081329385823235218444233221\