From 8fa9083e123736281c432b23932e23f7cb86b36b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 30 Jun 2026 17:30:35 +0200 Subject: [PATCH] patch: remove ConditionallyNegatable for Aeneas/Charon transpilation Upstream: dalek-cryptography/curve25519-dalek v5.0.0-rc.1 Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c --- curve25519-dalek/src/field.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/curve25519-dalek/src/field.rs b/curve25519-dalek/src/field.rs index 8924166..a1d1b6d 100644 --- a/curve25519-dalek/src/field.rs +++ b/curve25519-dalek/src/field.rs @@ -28,7 +28,6 @@ use cfg_if::cfg_if; use subtle::Choice; -use subtle::ConditionallyNegatable; use subtle::ConditionallySelectable; use subtle::ConstantTimeEq; @@ -357,8 +356,14 @@ impl FieldElement { r.conditional_assign(&r_prime, flipped_sign_sqrt | flipped_sign_sqrt_i); // 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(); - 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; @@ -518,6 +523,7 @@ where #[cfg(test)] mod test { use crate::field::*; + use subtle::ConditionallyNegatable; /// Random element a of GF(2^255-19), from Sage /// a = 1070314506888354081329385823235218444233221\