From 5f8e70e6360ee51ae9f8e74a58b69aec25961828 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 6 Jul 2026 01:41:56 +0200 Subject: [PATCH] Aeneas-compat: decompress step_2 negate-then-conditional-assign 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 --- curve25519/solana-ed25519/src/edwards.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/curve25519/solana-ed25519/src/edwards.rs b/curve25519/solana-ed25519/src/edwards.rs index f989c2f..fb6ef4a 100644 --- a/curve25519/solana-ed25519/src/edwards.rs +++ b/curve25519/solana-ed25519/src/edwards.rs @@ -121,7 +121,6 @@ use { use rand_core::{CryptoRng, RngCore}; use subtle::Choice; -use subtle::ConditionallyNegatable; use subtle::ConditionallySelectable; use subtle::ConstantTimeEq; @@ -246,7 +245,13 @@ mod decompress { // FieldElement::sqrt_ratio_i always returns the nonnegative square root, // so we negate according to the supplied sign bit. 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 { X,