From 54ef3c9293d1335adc7f245a00efce64d2f8232b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 30 Jun 2026 17:30:36 +0200 Subject: [PATCH] patch: remove ConditionallyNegatable for Aeneas/Charon transpilation Upstream: risc0/curve25519-dalek v4.1.3 Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c --- curve25519-dalek/src/field.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/curve25519-dalek/src/field.rs b/curve25519-dalek/src/field.rs index 492b05c..78b43ec 100644 --- a/curve25519-dalek/src/field.rs +++ b/curve25519-dalek/src/field.rs @@ -28,7 +28,7 @@ use cfg_if::cfg_if; use subtle::Choice; -use subtle::ConditionallyNegatable; + use subtle::ConditionallySelectable; use subtle::ConstantTimeEq; @@ -288,7 +288,7 @@ impl FieldElement { // Choose the nonnegative square root. 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; @@ -314,6 +314,7 @@ impl FieldElement { #[cfg(test)] mod test { + use subtle::ConditionallyNegatable; use crate::field::*; /// Random element a of GF(2^255-19), from Sage