From 3df6a2b04112daddc3e0d0c3f2c057877b29f4d5 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: betrusted-io/curve25519-dalek v4.1.2 Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c --- curve25519-dalek/src/field.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/curve25519-dalek/src/field.rs b/curve25519-dalek/src/field.rs index 80f51ea..014e387 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; @@ -290,7 +289,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;