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

patch: remove ConditionallyNegatable for Aeneas/Charon transpilation

Browse source 
Upstream: risc0/curve25519-dalek v4.1.3
Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c
This commit is contained in:
mrwulf 2026-06-30 17:30:36 +02:00
parent 385adda1fa
commit 54ef3c9293
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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