mirror of
https://github.com/saymrwulf/anza-cryptography-source.git
synced 2026-09-05 20:30:51 +00:00
patch: remove ConditionallyNegatable for Aeneas/Charon transpilation
Upstream: anza-xyz/cryptography Required for: formal verification via Aeneas bf13c42e + Charon 9dd7f23c
This commit is contained in:
parent
0a54ccaf04
commit
e5f4598766
1 changed files with 9 additions and 2 deletions
|
|
@ -26,7 +26,6 @@
|
||||||
#![allow(unused_qualifications)]
|
#![allow(unused_qualifications)]
|
||||||
|
|
||||||
use subtle::Choice;
|
use subtle::Choice;
|
||||||
use subtle::ConditionallyNegatable;
|
|
||||||
use subtle::ConditionallySelectable;
|
use subtle::ConditionallySelectable;
|
||||||
use subtle::ConstantTimeEq;
|
use subtle::ConstantTimeEq;
|
||||||
|
|
||||||
|
|
@ -355,8 +354,15 @@ impl FieldElement {
|
||||||
r.conditional_assign(&r_prime, flipped_sign_sqrt | flipped_sign_sqrt_i);
|
r.conditional_assign(&r_prime, flipped_sign_sqrt | flipped_sign_sqrt_i);
|
||||||
|
|
||||||
// Choose the nonnegative square root.
|
// 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 (whose `for<'a> &'a T: Neg` bound breaks the Aeneas
|
||||||
|
// verification toolchain; see verification/field/README.md).
|
||||||
let r_is_negative = r.is_negative();
|
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;
|
let was_nonzero_square = correct_sign_sqrt | flipped_sign_sqrt;
|
||||||
|
|
||||||
|
|
@ -516,6 +522,7 @@ where
|
||||||
#[cfg(test)]
|
#[cfg(test)]
|
||||||
mod test {
|
mod test {
|
||||||
use crate::field::*;
|
use crate::field::*;
|
||||||
|
use subtle::ConditionallyNegatable;
|
||||||
|
|
||||||
/// Random element a of GF(2^255-19), from Sage
|
/// Random element a of GF(2^255-19), from Sage
|
||||||
/// a = 1070314506888354081329385823235218444233221\
|
/// a = 1070314506888354081329385823235218444233221\
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue