From f667c67b7f190a04e4ab387376b00be412ad0b64 Mon Sep 17 00:00:00 2001 From: Arvind Mukund Date: Sun, 29 Oct 2023 19:47:51 -0700 Subject: [PATCH 1/4] p521: Update `fiat-crypto` + `fiat-constify` The fiat-crypto version is v0.0.24 and the fiat-constify from https://github.com/RustCrypto/utils/pull/978 was used Signed-off-by: Arvind Mukund --- p521/src/arithmetic/field/p521_64.rs | 752 ++++++---------- p521/src/arithmetic/scalar/p521_scalar_64.rs | 897 +++++++++---------- 2 files changed, 690 insertions(+), 959 deletions(-) diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index 46e08f4c..e2be648b 100644 --- a/p521/src/arithmetic/field/p521_64.rs +++ b/p521/src/arithmetic/field/p521_64.rs @@ -1,17 +1,17 @@ -#![doc = " fiat-crypto output postprocessed by fiat-constify: "] -#![doc = " Autogenerated: './unsaturated_solinas' --lang Rust --inline p521 64 9 '2^521 - 1'"] -#![doc = " curve description: p521"] -#![doc = " machine_wordsize = 64 (from \"64\")"] -#![doc = " requested operations: (all)"] -#![doc = " n = 9 (from \"9\")"] -#![doc = " s-c = 2^521 - [(1, 1)] (from \"2^521 - 1\")"] -#![doc = " tight_bounds_multiplier = 1 (from \"\")"] -#![doc = ""] -#![doc = " Computed values:"] -#![doc = " carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]"] -#![doc = " eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0)"] -#![doc = " bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)"] -#![doc = " balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe]"] +//! fiat-crypto output postprocessed by fiat-constify: +//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p521 64 '(auto)' '2^521 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax +//! curve description: p521 +//! machine_wordsize = 64 (from "64") +//! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax +//! n = 9 (from "(auto)") +//! s-c = 2^521 - [(1, 1)] (from "2^521 - 1") +//! tight_bounds_multiplier = 1 (from "") +//! +//! Computed values: +//! carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] +//! eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0) +//! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) +//! balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe] #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -27,152 +27,173 @@ pub type fiat_p521_u1 = u8; pub type fiat_p521_i1 = i8; pub type fiat_p521_u2 = u8; pub type fiat_p521_i2 = i8; -pub type fiat_p521_loose_field_element = [u64; 9]; -pub type fiat_p521_tight_field_element = [u64; 9]; -#[doc = " The function fiat_p521_addcarryx_u58 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^58"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The type fiat_p521_loose_field_element is a field element with loose bounds. +/// Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] +#[derive(Clone, Copy)] +pub struct fiat_p521_loose_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The type fiat_p521_tight_field_element is a field element with tight bounds. +/// Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] +#[derive(Clone, Copy)] +pub struct fiat_p521_tight_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The function fiat_p521_addcarryx_u58 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^58 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x3ffffffffffffff] +/// arg3: [0x0 ~> 0x3ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x3ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_addcarryx_u58( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: u64 = (((arg1 as u64) + arg2) + arg3); let x2: u64 = (x1 & 0x3ffffffffffffff); let x3: fiat_p521_u1 = ((x1 >> 58) as fiat_p521_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_subborrowx_u58 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^58"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_subborrowx_u58 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^58 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x3ffffffffffffff] +/// arg3: [0x0 ~> 0x3ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x3ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_subborrowx_u58( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 58) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x3ffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), + ) } -#[doc = " The function fiat_p521_addcarryx_u57 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^57"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_addcarryx_u57 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^57 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x1ffffffffffffff] +/// arg3: [0x0 ~> 0x1ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x1ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_addcarryx_u57( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: u64 = (((arg1 as u64) + arg2) + arg3); let x2: u64 = (x1 & 0x1ffffffffffffff); let x3: fiat_p521_u1 = ((x1 >> 57) as fiat_p521_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_subborrowx_u57 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^57"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_subborrowx_u57 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^57 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x1ffffffffffffff] +/// arg3: [0x0 ~> 0x1ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x1ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_subborrowx_u57( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 57) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x1ffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), + ) } -#[doc = " The function fiat_p521_cmovznz_u64 is a single-word conditional move."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_cmovznz_u64 is a single-word conditional move. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_cmovznz_u64(arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> u64 { - let mut out1: u64 = 0; let x1: fiat_p521_u1 = (!(!arg1)); let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) as i128) & (0xffffffffffffffff as i128)) as u64); let x3: u64 = ((x2 & arg3) | ((!x2) & arg2)); - out1 = x3; - out1 + (x3) } -#[doc = " The function fiat_p521_carry_mul multiplies two field elements and reduces the result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_mul multiplies two field elements and reduces the result. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 * eval arg2) mod m +/// #[inline] pub const fn fiat_p521_carry_mul( arg1: &fiat_p521_loose_field_element, arg2: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let x1: u128 = (((arg1[8]) as u128) * (((arg2[8]) * 0x2) as u128)); let x2: u128 = (((arg1[8]) as u128) * (((arg2[7]) * 0x2) as u128)); let x3: u128 = (((arg1[8]) as u128) * (((arg2[6]) * 0x2) as u128)); @@ -296,27 +317,18 @@ pub const fn fiat_p521_carry_mul( let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1); let x122: u64 = (x120 & 0x3ffffffffffffff); let x123: u64 = ((x121 as u64) + x98); - out1[0] = x119; - out1[1] = x122; - out1[2] = x123; - out1[3] = x101; - out1[4] = x104; - out1[5] = x107; - out1[6] = x110; - out1[7] = x113; - out1[8] = x116; - out1 + (fiat_p521_tight_field_element([x119, x122, x123, x101, x104, x107, x110, x113, x116])) } -#[doc = " The function fiat_p521_carry_square squares a field element and reduces the result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * eval arg1) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_square squares a field element and reduces the result. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 * eval arg1) mod m +/// #[inline] pub const fn fiat_p521_carry_square( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (arg1[8]); let x2: u64 = (x1 * 0x2); let x3: u64 = ((arg1[8]) * 0x2); @@ -420,27 +432,18 @@ pub const fn fiat_p521_carry_square( let x101: fiat_p521_u1 = ((x100 >> 58) as fiat_p521_u1); let x102: u64 = (x100 & 0x3ffffffffffffff); let x103: u64 = ((x101 as u64) + x78); - out1[0] = x99; - out1[1] = x102; - out1[2] = x103; - out1[3] = x81; - out1[4] = x84; - out1[5] = x87; - out1[6] = x90; - out1[7] = x93; - out1[8] = x96; - out1 + (fiat_p521_tight_field_element([x99, x102, x103, x81, x84, x87, x90, x93, x96])) } -#[doc = " The function fiat_p521_carry reduces a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = eval arg1 mod m"] -#[doc = ""] +/// The function fiat_p521_carry reduces a field element. +/// +/// Postconditions: +/// eval out1 mod m = eval arg1 mod m +/// #[inline] pub const fn fiat_p521_carry( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (arg1[0]); let x2: u64 = ((x1 >> 58) + (arg1[1])); let x3: u64 = ((x2 >> 58) + (arg1[2])); @@ -461,28 +464,20 @@ pub const fn fiat_p521_carry( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) } -#[doc = " The function fiat_p521_add adds two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_add adds two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 + eval arg2) mod m +/// #[inline] pub const fn fiat_p521_add( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((arg1[1]) + (arg2[1])); let x3: u64 = ((arg1[2]) + (arg2[2])); @@ -492,28 +487,20 @@ pub const fn fiat_p521_add( let x7: u64 = ((arg1[6]) + (arg2[6])); let x8: u64 = ((arg1[7]) + (arg2[7])); let x9: u64 = ((arg1[8]) + (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_sub subtracts two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_sub subtracts two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 - eval arg2) mod m +/// #[inline] pub const fn fiat_p521_sub( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); let x2: u64 = ((0x7fffffffffffffe + (arg1[1])) - (arg2[1])); let x3: u64 = ((0x7fffffffffffffe + (arg1[2])) - (arg2[2])); @@ -523,25 +510,16 @@ pub const fn fiat_p521_sub( let x7: u64 = ((0x7fffffffffffffe + (arg1[6])) - (arg2[6])); let x8: u64 = ((0x7fffffffffffffe + (arg1[7])) - (arg2[7])); let x9: u64 = ((0x3fffffffffffffe + (arg1[8])) - (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_opp negates a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = -eval arg1 mod m"] -#[doc = ""] +/// The function fiat_p521_opp negates a field element. +/// +/// Postconditions: +/// eval out1 mod m = -eval arg1 mod m +/// #[inline] pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = (0x7fffffffffffffe - (arg1[1])); let x3: u64 = (0x7fffffffffffffe - (arg1[2])); @@ -551,186 +529,21 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo let x7: u64 = (0x7fffffffffffffe - (arg1[6])); let x8: u64 = (0x7fffffffffffffe - (arg1[7])); let x9: u64 = (0x3fffffffffffffe - (arg1[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 -} -#[doc = " The function fiat_p521_carry_add adds two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"] -#[doc = ""] -#[inline] -pub const fn fiat_p521_carry_add( - arg1: &fiat_p521_tight_field_element, - arg2: &fiat_p521_tight_field_element, -) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; - let x1: u64 = ((arg1[0]) + (arg2[0])); - let x2: u64 = ((x1 >> 58) + ((arg1[1]) + (arg2[1]))); - let x3: u64 = ((x2 >> 58) + ((arg1[2]) + (arg2[2]))); - let x4: u64 = ((x3 >> 58) + ((arg1[3]) + (arg2[3]))); - let x5: u64 = ((x4 >> 58) + ((arg1[4]) + (arg2[4]))); - let x6: u64 = ((x5 >> 58) + ((arg1[5]) + (arg2[5]))); - let x7: u64 = ((x6 >> 58) + ((arg1[6]) + (arg2[6]))); - let x8: u64 = ((x7 >> 58) + ((arg1[7]) + (arg2[7]))); - let x9: u64 = ((x8 >> 58) + ((arg1[8]) + (arg2[8]))); - let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57)); - let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); - let x12: u64 = (x10 & 0x3ffffffffffffff); - let x13: u64 = (x11 & 0x3ffffffffffffff); - let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); - let x15: u64 = (x4 & 0x3ffffffffffffff); - let x16: u64 = (x5 & 0x3ffffffffffffff); - let x17: u64 = (x6 & 0x3ffffffffffffff); - let x18: u64 = (x7 & 0x3ffffffffffffff); - let x19: u64 = (x8 & 0x3ffffffffffffff); - let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_carry_sub subtracts two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] -#[doc = ""] -#[inline] -pub const fn fiat_p521_carry_sub( - arg1: &fiat_p521_tight_field_element, - arg2: &fiat_p521_tight_field_element, -) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; - let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); - let x2: u64 = ((x1 >> 58) + ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]))); - let x3: u64 = ((x2 >> 58) + ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]))); - let x4: u64 = ((x3 >> 58) + ((0x7fffffffffffffe + (arg1[3])) - (arg2[3]))); - let x5: u64 = ((x4 >> 58) + ((0x7fffffffffffffe + (arg1[4])) - (arg2[4]))); - let x6: u64 = ((x5 >> 58) + ((0x7fffffffffffffe + (arg1[5])) - (arg2[5]))); - let x7: u64 = ((x6 >> 58) + ((0x7fffffffffffffe + (arg1[6])) - (arg2[6]))); - let x8: u64 = ((x7 >> 58) + ((0x7fffffffffffffe + (arg1[7])) - (arg2[7]))); - let x9: u64 = ((x8 >> 58) + ((0x3fffffffffffffe + (arg1[8])) - (arg2[8]))); - let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57)); - let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); - let x12: u64 = (x10 & 0x3ffffffffffffff); - let x13: u64 = (x11 & 0x3ffffffffffffff); - let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); - let x15: u64 = (x4 & 0x3ffffffffffffff); - let x16: u64 = (x5 & 0x3ffffffffffffff); - let x17: u64 = (x6 & 0x3ffffffffffffff); - let x18: u64 = (x7 & 0x3ffffffffffffff); - let x19: u64 = (x8 & 0x3ffffffffffffff); - let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 -} -#[doc = " The function fiat_p521_carry_opp negates a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = -eval arg1 mod m"] -#[doc = ""] -#[inline] -pub const fn fiat_p521_carry_opp( - arg1: &fiat_p521_tight_field_element, -) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; - let x1: u64 = (0x7fffffffffffffe - (arg1[0])); - let x2: u64 = ((((x1 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[1]))); - let x3: u64 = ((((x2 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[2]))); - let x4: u64 = ((((x3 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[3]))); - let x5: u64 = ((((x4 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[4]))); - let x6: u64 = ((((x5 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[5]))); - let x7: u64 = ((((x6 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[6]))); - let x8: u64 = ((((x7 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[7]))); - let x9: u64 = ((((x8 >> 58) as fiat_p521_u1) as u64) + (0x3fffffffffffffe - (arg1[8]))); - let x10: u64 = ((x1 & 0x3ffffffffffffff) + (((x9 >> 57) as fiat_p521_u1) as u64)); - let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); - let x12: u64 = (x10 & 0x3ffffffffffffff); - let x13: u64 = (x11 & 0x3ffffffffffffff); - let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); - let x15: u64 = (x4 & 0x3ffffffffffffff); - let x16: u64 = (x5 & 0x3ffffffffffffff); - let x17: u64 = (x6 & 0x3ffffffffffffff); - let x18: u64 = (x7 & 0x3ffffffffffffff); - let x19: u64 = (x8 & 0x3ffffffffffffff); - let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 -} -#[doc = " The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = arg1"] -#[doc = ""] -#[inline] -pub const fn fiat_p521_relax( - arg1: &fiat_p521_tight_field_element, -) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; - let x1: u64 = (arg1[0]); - let x2: u64 = (arg1[1]); - let x3: u64 = (arg1[2]); - let x4: u64 = (arg1[3]); - let x5: u64 = (arg1[4]); - let x6: u64 = (arg1[5]); - let x7: u64 = (arg1[6]); - let x8: u64 = (arg1[7]); - let x9: u64 = (arg1[8]); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 -} -#[doc = " The function fiat_p521_selectznz is a multi-limb conditional select."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_selectznz is a multi-limb conditional select. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let (x1) = fiat_p521_cmovznz_u64(arg1, (arg2[0]), (arg3[0])); let mut x2: u64 = 0; @@ -749,27 +562,18 @@ pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u6 let (x8) = fiat_p521_cmovznz_u64(arg1, (arg2[7]), (arg3[7])); let mut x9: u64 = 0; let (x9) = fiat_p521_cmovznz_u64(arg1, (arg2[8]), (arg3[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) } -#[doc = " The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order. +/// +/// Postconditions: +/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66] { - let mut out1: [u8; 66] = [0; 66]; + let arg1 = &arg1.0; let mut x1: u64 = 0; let mut x2: fiat_p521_u1 = 0; let (x1, x2) = fiat_p521_subborrowx_u58(0x0, (arg1[0]), 0x3ffffffffffffff); @@ -964,84 +768,84 @@ pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66 let x173: u64 = (x171 >> 8); let x174: u8 = ((x173 & (0xff as u64)) as u8); let x175: fiat_p521_u1 = ((x173 >> 8) as fiat_p521_u1); - out1[0] = x44; - out1[1] = x46; - out1[2] = x48; - out1[3] = x50; - out1[4] = x52; - out1[5] = x54; - out1[6] = x56; - out1[7] = x59; - out1[8] = x61; - out1[9] = x63; - out1[10] = x65; - out1[11] = x67; - out1[12] = x69; - out1[13] = x71; - out1[14] = x74; - out1[15] = x76; - out1[16] = x78; - out1[17] = x80; - out1[18] = x82; - out1[19] = x84; - out1[20] = x86; - out1[21] = x89; - out1[22] = x91; - out1[23] = x93; - out1[24] = x95; - out1[25] = x97; - out1[26] = x99; - out1[27] = x101; - out1[28] = x102; - out1[29] = x103; - out1[30] = x105; - out1[31] = x107; - out1[32] = x109; - out1[33] = x111; - out1[34] = x113; - out1[35] = x115; - out1[36] = x118; - out1[37] = x120; - out1[38] = x122; - out1[39] = x124; - out1[40] = x126; - out1[41] = x128; - out1[42] = x130; - out1[43] = x133; - out1[44] = x135; - out1[45] = x137; - out1[46] = x139; - out1[47] = x141; - out1[48] = x143; - out1[49] = x145; - out1[50] = x148; - out1[51] = x150; - out1[52] = x152; - out1[53] = x154; - out1[54] = x156; - out1[55] = x158; - out1[56] = x160; - out1[57] = x161; - out1[58] = x162; - out1[59] = x164; - out1[60] = x166; - out1[61] = x168; - out1[62] = x170; - out1[63] = x172; - out1[64] = x174; - out1[65] = (x175 as u8); - out1 + ([ + x44, + x46, + x48, + x50, + x52, + x54, + x56, + x59, + x61, + x63, + x65, + x67, + x69, + x71, + x74, + x76, + x78, + x80, + x82, + x84, + x86, + x89, + x91, + x93, + x95, + x97, + x99, + x101, + x102, + x103, + x105, + x107, + x109, + x111, + x113, + x115, + x118, + x120, + x122, + x124, + x126, + x128, + x130, + x133, + x135, + x137, + x139, + x141, + x143, + x145, + x148, + x150, + x152, + x154, + x156, + x158, + x160, + x161, + x162, + x164, + x166, + x168, + x170, + x172, + x174, + (x175 as u8), + ]) } -#[doc = " The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = bytes_eval arg1 mod m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order. +/// +/// Postconditions: +/// eval out1 mod m = bytes_eval arg1 mod m +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = ((((arg1[65]) as fiat_p521_u1) as u64) << 56); let x2: u64 = (((arg1[64]) as u64) << 48); let x3: u64 = (((arg1[63]) as u64) << 40); @@ -1183,14 +987,26 @@ pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_elem let x139: u64 = (x3 + x138); let x140: u64 = (x2 + x139); let x141: u64 = (x1 + x140); - out1[0] = x74; - out1[1] = x83; - out1[2] = x92; - out1[3] = x100; - out1[4] = x108; - out1[5] = x117; - out1[6] = x126; - out1[7] = x134; - out1[8] = x141; - out1 + (fiat_p521_tight_field_element([x74, x83, x92, x100, x108, x117, x126, x134, x141])) +} +/// The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements. +/// +/// Postconditions: +/// out1 = arg1 +/// +#[inline] +pub const fn fiat_p521_relax( + arg1: &fiat_p521_tight_field_element, +) -> fiat_p521_loose_field_element { + let arg1 = &arg1.0; + let x1: u64 = (arg1[0]); + let x2: u64 = (arg1[1]); + let x3: u64 = (arg1[2]); + let x4: u64 = (arg1[3]); + let x5: u64 = (arg1[4]); + let x6: u64 = (arg1[5]); + let x7: u64 = (arg1[6]); + let x8: u64 = (arg1[7]); + let x9: u64 = (arg1[8]); + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } diff --git a/p521/src/arithmetic/scalar/p521_scalar_64.rs b/p521/src/arithmetic/scalar/p521_scalar_64.rs index 60c8646f..8b349f2e 100644 --- a/p521/src/arithmetic/scalar/p521_scalar_64.rs +++ b/p521/src/arithmetic/scalar/p521_scalar_64.rs @@ -1,22 +1,22 @@ -#![doc = " fiat-crypto output postprocessed by fiat-constify: "] -#![doc = " Autogenerated: './word_by_word_montgomery' --lang Rust --inline p521_scalar 64 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409"] -#![doc = " curve description: p521_scalar"] -#![doc = " machine_wordsize = 64 (from \"64\")"] -#![doc = " requested operations: (all)"] -#![doc = " m = 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 (from \"0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409\")"] -#![doc = ""] -#![doc = " NOTE: In addition to the bounds specified above each function, all"] -#![doc = " functions synthesized for this Montgomery arithmetic require the"] -#![doc = " input to be strictly less than the prime modulus (m), and also"] -#![doc = " require the input to be in the unique saturated representation."] -#![doc = " All functions also ensure that these two properties are true of"] -#![doc = " return values."] -#![doc = ""] -#![doc = " Computed values:"] -#![doc = " eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9)"] -#![doc = " bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)"] -#![doc = " twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) in"] -#![doc = " if x1 & (2^576-1) < 2^575 then x1 & (2^576-1) else (x1 & (2^576-1)) - 2^576"] +//! fiat-crypto output postprocessed by fiat-constify: +//! Autogenerated: './word_by_word_montgomery' --lang Rust --inline p521_scalar 64 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 +//! curve description: p521_scalar +//! machine_wordsize = 64 (from "64") +//! requested operations: (all) +//! m = 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 (from "0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409") +//! +//! NOTE: In addition to the bounds specified above each function, all +//! functions synthesized for this Montgomery arithmetic require the +//! input to be strictly less than the prime modulus (m), and also +//! require the input to be in the unique saturated representation. +//! All functions also ensure that these two properties are true of +//! return values. +//! +//! Computed values: +//! eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) +//! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) +//! twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) in +//! if x1 & (2^576-1) < 2^575 then x1 & (2^576-1) else (x1 & (2^576-1)) - 2^576 #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -32,124 +32,146 @@ pub type fiat_p521_scalar_u1 = u8; pub type fiat_p521_scalar_i1 = i8; pub type fiat_p521_scalar_u2 = u8; pub type fiat_p521_scalar_i2 = i8; -pub type fiat_p521_scalar_montgomery_domain_field_element = [u64; 9]; -pub type fiat_p521_scalar_non_montgomery_domain_field_element = [u64; 9]; -#[doc = " The function fiat_p521_scalar_addcarryx_u64 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^64"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The type fiat_p521_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. +/// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +#[derive(Debug, Clone, Copy, PartialEq, PartialOrd)] +pub struct fiat_p521_scalar_montgomery_domain_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The type fiat_p521_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. +/// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +#[derive(Debug, Clone, Copy, PartialEq, PartialOrd)] +pub struct fiat_p521_scalar_non_montgomery_domain_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The function fiat_p521_scalar_addcarryx_u64 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^64 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_scalar_addcarryx_u64( arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_scalar_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_scalar_u1 = 0; let x1: u128 = (((arg1 as u128) + (arg2 as u128)) + (arg3 as u128)); let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64); let x3: fiat_p521_scalar_u1 = ((x1 >> 64) as fiat_p521_scalar_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_scalar_subborrowx_u64 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^64"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_scalar_subborrowx_u64 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^64 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_scalar_subborrowx_u64( arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_scalar_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_scalar_u1 = 0; let x1: i128 = (((arg2 as i128) - (arg1 as i128)) - (arg3 as i128)); let x2: fiat_p521_scalar_i1 = ((x1 >> 64) as fiat_p521_scalar_i1); let x3: u64 = ((x1 & (0xffffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1), + ) } -#[doc = " The function fiat_p521_scalar_mulx_u64 is a multiplication, returning the full double-width result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 * arg2) mod 2^64"] -#[doc = " out2 = ⌊arg1 * arg2 / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_mulx_u64 is a multiplication, returning the full double-width result. +/// +/// Postconditions: +/// out1 = (arg1 * arg2) mod 2^64 +/// out2 = ⌊arg1 * arg2 / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0xffffffffffffffff] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_mulx_u64(arg1: u64, arg2: u64) -> (u64, u64) { - let mut out1: u64 = 0; - let mut out2: u64 = 0; let x1: u128 = ((arg1 as u128) * (arg2 as u128)); let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64); let x3: u64 = ((x1 >> 64) as u64); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_scalar_cmovznz_u64 is a single-word conditional move."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_cmovznz_u64 is a single-word conditional move. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_cmovznz_u64(arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64) -> u64 { - let mut out1: u64 = 0; let x1: fiat_p521_scalar_u1 = (!(!arg1)); let x2: u64 = ((((((0x0 as fiat_p521_scalar_i2) - (x1 as fiat_p521_scalar_i2)) as fiat_p521_scalar_i1) as i128) & (0xffffffffffffffff as i128)) as u64); let x3: u64 = ((x2 & arg3) | ((!x2) & arg2)); - out1 = x3; - out1 + (x3) } -#[doc = " The function fiat_p521_scalar_mul multiplies two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_mul multiplies two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_mul( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -1688,30 +1710,23 @@ pub const fn fiat_p521_scalar_mul( let (x1033) = fiat_p521_scalar_cmovznz_u64(x1025, x1020, x1001); let mut x1034: u64 = 0; let (x1034) = fiat_p521_scalar_cmovznz_u64(x1025, x1022, x1003); - out1[0] = x1026; - out1[1] = x1027; - out1[2] = x1028; - out1[3] = x1029; - out1[4] = x1030; - out1[5] = x1031; - out1[6] = x1032; - out1[7] = x1033; - out1[8] = x1034; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, + ])) } -#[doc = " The function fiat_p521_scalar_square squares a field element in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_square squares a field element in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_square( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -3250,32 +3265,26 @@ pub const fn fiat_p521_scalar_square( let (x1033) = fiat_p521_scalar_cmovznz_u64(x1025, x1020, x1001); let mut x1034: u64 = 0; let (x1034) = fiat_p521_scalar_cmovznz_u64(x1025, x1022, x1003); - out1[0] = x1026; - out1[1] = x1027; - out1[2] = x1028; - out1[3] = x1029; - out1[4] = x1030; - out1[5] = x1031; - out1[6] = x1032; - out1[7] = x1033; - out1[8] = x1034; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, + ])) } -#[doc = " The function fiat_p521_scalar_add adds two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_add adds two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_add( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_addcarryx_u64(0x0, (arg1[0]), (arg2[0])); @@ -3351,32 +3360,26 @@ pub const fn fiat_p521_scalar_add( let (x46) = fiat_p521_scalar_cmovznz_u64(x38, x33, x15); let mut x47: u64 = 0; let (x47) = fiat_p521_scalar_cmovznz_u64(x38, x35, x17); - out1[0] = x39; - out1[1] = x40; - out1[2] = x41; - out1[3] = x42; - out1[4] = x43; - out1[5] = x44; - out1[6] = x45; - out1[7] = x46; - out1[8] = x47; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x39, x40, x41, x42, x43, x44, x45, x46, x47, + ])) } -#[doc = " The function fiat_p521_scalar_sub subtracts two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_sub subtracts two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_sub( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; + let arg2 = &arg2.0; let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_subborrowx_u64(0x0, (arg1[0]), (arg2[0])); @@ -3433,30 +3436,23 @@ pub const fn fiat_p521_scalar_sub( let mut x36: u64 = 0; let mut x37: fiat_p521_scalar_u1 = 0; let (x36, x37) = fiat_p521_scalar_addcarryx_u64(x35, x17, (x19 & 0x1ff)); - out1[0] = x20; - out1[1] = x22; - out1[2] = x24; - out1[3] = x26; - out1[4] = x28; - out1[5] = x30; - out1[6] = x32; - out1[7] = x34; - out1[8] = x36; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x20, x22, x24, x26, x28, x30, x32, x34, x36, + ])) } -#[doc = " The function fiat_p521_scalar_opp negates a field element in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_opp negates a field element in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_opp( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_subborrowx_u64(0x0, (0x0 as u64), (arg1[0])); @@ -3513,30 +3509,23 @@ pub const fn fiat_p521_scalar_opp( let mut x36: u64 = 0; let mut x37: fiat_p521_scalar_u1 = 0; let (x36, x37) = fiat_p521_scalar_addcarryx_u64(x35, x17, (x19 & 0x1ff)); - out1[0] = x20; - out1[1] = x22; - out1[2] = x24; - out1[3] = x26; - out1[4] = x28; - out1[5] = x30; - out1[6] = x32; - out1[7] = x34; - out1[8] = x36; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x20, x22, x24, x26, x28, x30, x32, x34, x36, + ])) } -#[doc = " The function fiat_p521_scalar_from_montgomery translates a field element out of the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^9) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_from_montgomery translates a field element out of the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^9) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_from_montgomery( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_non_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_non_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (arg1[0]); let mut x2: u64 = 0; let mut x3: u64 = 0; @@ -4540,30 +4529,23 @@ pub const fn fiat_p521_scalar_from_montgomery( let (x644) = fiat_p521_scalar_cmovznz_u64(x636, x631, x614); let mut x645: u64 = 0; let (x645) = fiat_p521_scalar_cmovznz_u64(x636, x633, x616); - out1[0] = x637; - out1[1] = x638; - out1[2] = x639; - out1[3] = x640; - out1[4] = x641; - out1[5] = x642; - out1[6] = x643; - out1[7] = x644; - out1[8] = x645; - out1 + (fiat_p521_scalar_non_montgomery_domain_field_element([ + x637, x638, x639, x640, x641, x642, x643, x644, x645, + ])) } -#[doc = " The function fiat_p521_scalar_to_montgomery translates a field element into the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = eval arg1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_to_montgomery translates a field element into the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = eval arg1 mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_to_montgomery( arg1: &fiat_p521_scalar_non_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = &arg1.0; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -6059,57 +6041,47 @@ pub const fn fiat_p521_scalar_to_montgomery( let (x974) = fiat_p521_scalar_cmovznz_u64(x966, x961, x944); let mut x975: u64 = 0; let (x975) = fiat_p521_scalar_cmovznz_u64(x966, x963, x946); - out1[0] = x967; - out1[1] = x968; - out1[2] = x969; - out1[3] = x970; - out1[4] = x971; - out1[5] = x972; - out1[6] = x973; - out1[7] = x974; - out1[8] = x975; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x967, x968, x969, x970, x971, x972, x973, x974, x975, + ])) } -#[doc = " The function fiat_p521_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_nonzero(arg1: &[u64; 9]) -> u64 { - let mut out1: u64 = 0; let x1: u64 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | ((arg1[7]) | (arg1[8]))))))))); - out1 = x1; - out1 + (x1) } -#[doc = " The function fiat_p521_scalar_selectznz is a multi-limb conditional select."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_selectznz is a multi-limb conditional select. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_selectznz( arg1: fiat_p521_scalar_u1, arg2: &[u64; 9], arg3: &[u64; 9], ) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let (x1) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[0]), (arg3[0])); let mut x2: u64 = 0; @@ -6128,31 +6100,21 @@ pub const fn fiat_p521_scalar_selectznz( let (x8) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[7]), (arg3[7])); let mut x9: u64 = 0; let (x9) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[8]), (arg3[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) } -#[doc = " The function fiat_p521_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_scalar_to_bytes(arg1: &[u64; 9]) -> [u8; 66] { - let mut out1: [u8; 66] = [0; 66]; let x1: u64 = (arg1[8]); let x2: u64 = (arg1[7]); let x3: u64 = (arg1[6]); @@ -6276,89 +6238,89 @@ pub const fn fiat_p521_scalar_to_bytes(arg1: &[u64; 9]) -> [u8; 66] { let x121: u8 = ((x119 >> 8) as u8); let x122: u8 = ((x1 & (0xff as u64)) as u8); let x123: fiat_p521_scalar_u1 = ((x1 >> 8) as fiat_p521_scalar_u1); - out1[0] = x10; - out1[1] = x12; - out1[2] = x14; - out1[3] = x16; - out1[4] = x18; - out1[5] = x20; - out1[6] = x22; - out1[7] = x23; - out1[8] = x24; - out1[9] = x26; - out1[10] = x28; - out1[11] = x30; - out1[12] = x32; - out1[13] = x34; - out1[14] = x36; - out1[15] = x37; - out1[16] = x38; - out1[17] = x40; - out1[18] = x42; - out1[19] = x44; - out1[20] = x46; - out1[21] = x48; - out1[22] = x50; - out1[23] = x51; - out1[24] = x52; - out1[25] = x54; - out1[26] = x56; - out1[27] = x58; - out1[28] = x60; - out1[29] = x62; - out1[30] = x64; - out1[31] = x65; - out1[32] = x66; - out1[33] = x68; - out1[34] = x70; - out1[35] = x72; - out1[36] = x74; - out1[37] = x76; - out1[38] = x78; - out1[39] = x79; - out1[40] = x80; - out1[41] = x82; - out1[42] = x84; - out1[43] = x86; - out1[44] = x88; - out1[45] = x90; - out1[46] = x92; - out1[47] = x93; - out1[48] = x94; - out1[49] = x96; - out1[50] = x98; - out1[51] = x100; - out1[52] = x102; - out1[53] = x104; - out1[54] = x106; - out1[55] = x107; - out1[56] = x108; - out1[57] = x110; - out1[58] = x112; - out1[59] = x114; - out1[60] = x116; - out1[61] = x118; - out1[62] = x120; - out1[63] = x121; - out1[64] = x122; - out1[65] = (x123 as u8); - out1 + ([ + x10, + x12, + x14, + x16, + x18, + x20, + x22, + x23, + x24, + x26, + x28, + x30, + x32, + x34, + x36, + x37, + x38, + x40, + x42, + x44, + x46, + x48, + x50, + x51, + x52, + x54, + x56, + x58, + x60, + x62, + x64, + x65, + x66, + x68, + x70, + x72, + x74, + x76, + x78, + x79, + x80, + x82, + x84, + x86, + x88, + x90, + x92, + x93, + x94, + x96, + x98, + x100, + x102, + x104, + x106, + x107, + x108, + x110, + x112, + x114, + x116, + x118, + x120, + x121, + x122, + (x123 as u8), + ]) } -#[doc = " The function fiat_p521_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ bytes_eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = bytes_eval arg1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]]"] +/// The function fiat_p521_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order. +/// +/// Preconditions: +/// 0 ≤ bytes_eval arg1 < m +/// Postconditions: +/// eval out1 mod m = bytes_eval arg1 mod m +/// 0 ≤ eval out1 < m +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]] #[inline] pub const fn fiat_p521_scalar_from_bytes(arg1: &[u8; 66]) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let x1: u64 = ((((arg1[65]) as fiat_p521_scalar_u1) as u64) << 8); let x2: u8 = (arg1[64]); let x3: u64 = (((arg1[63]) as u64) << 56); @@ -6482,110 +6444,101 @@ pub const fn fiat_p521_scalar_from_bytes(arg1: &[u8; 66]) -> [u64; 9] { let x121: u64 = (x4 + x120); let x122: u64 = (x3 + x121); let x123: u64 = (x1 + (x2 as u64)); - out1[0] = x73; - out1[1] = x80; - out1[2] = x87; - out1[3] = x94; - out1[4] = x101; - out1[5] = x108; - out1[6] = x115; - out1[7] = x122; - out1[8] = x123; - out1 + ([x73, x80, x87, x94, x101, x108, x115, x122, x123]) } -#[doc = " The function fiat_p521_scalar_set_one returns the field element one in the Montgomery domain."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = 1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_set_one returns the field element one in the Montgomery domain. +/// +/// Postconditions: +/// eval (from_montgomery out1) mod m = 1 mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_set_one() -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; - out1[0] = 0xfb80000000000000; - out1[1] = 0x28a2482470b763cd; - out1[2] = 0x17e2251b23bb31dc; - out1[3] = 0xca4019ff5b847b2d; - out1[4] = 0x2d73cbc3e206834; - out1[5] = (0x0 as u64); - out1[6] = (0x0 as u64); - out1[7] = (0x0 as u64); - out1[8] = (0x0 as u64); - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + 0xfb80000000000000, + 0x28a2482470b763cd, + 0x17e2251b23bb31dc, + 0xca4019ff5b847b2d, + 0x2d73cbc3e206834, + (0x0 as u64), + (0x0 as u64), + (0x0 as u64), + (0x0 as u64), + ])) } -#[doc = " The function fiat_p521_scalar_msat returns the saturated representation of the prime modulus."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " twos_complement_eval out1 = m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_msat returns the saturated representation of the prime modulus. +/// +/// Postconditions: +/// twos_complement_eval out1 = m +/// 0 ≤ eval out1 < m +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_msat() -> [u64; 10] { - let mut out1: [u64; 10] = [0; 10]; - out1[0] = 0xbb6fb71e91386409; - out1[1] = 0x3bb5c9b8899c47ae; - out1[2] = 0x7fcc0148f709a5d0; - out1[3] = 0x51868783bf2f966b; - out1[4] = 0xfffffffffffffffa; - out1[5] = 0xffffffffffffffff; - out1[6] = 0xffffffffffffffff; - out1[7] = 0xffffffffffffffff; - out1[8] = 0x1ff; - out1[9] = (0x0 as u64); - out1 + ([ + 0xbb6fb71e91386409, + 0x3bb5c9b8899c47ae, + 0x7fcc0148f709a5d0, + 0x51868783bf2f966b, + 0xfffffffffffffffa, + 0xffffffffffffffff, + 0xffffffffffffffff, + 0xffffffffffffffff, + 0x1ff, + (0x0 as u64), + ]) } -#[doc = " The function fiat_p521_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form)."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form). +/// +/// Postconditions: +/// eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋) +/// 0 ≤ eval out1 < m +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_divstep_precomp() -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; - out1[0] = 0x7b27a0cb33d1884b; - out1[1] = 0x9ef6cb011f2467d8; - out1[2] = 0x5fbc88e1d6e7fce; - out1[3] = 0xb08222d0fe97e1dc; - out1[4] = 0x1624870c44df3fce; - out1[5] = 0xb7f07b8eedbce602; - out1[6] = 0x62da93cf721f63bc; - out1[7] = 0xafd209c16c4f0d20; - out1[8] = 0x1c7; - out1 + ([ + 0x7b27a0cb33d1884b, + 0x9ef6cb011f2467d8, + 0x5fbc88e1d6e7fce, + 0xb08222d0fe97e1dc, + 0x1624870c44df3fce, + 0xb7f07b8eedbce602, + 0x62da93cf721f63bc, + 0xafd209c16c4f0d20, + 0x1c7, + ]) } -#[doc = " The function fiat_p521_scalar_divstep computes a divstep."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg4 < m"] -#[doc = " 0 ≤ eval arg5 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)"] -#[doc = " twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)"] -#[doc = " twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)"] -#[doc = " eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)"] -#[doc = " eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)"] -#[doc = " 0 ≤ eval out5 < m"] -#[doc = " 0 ≤ eval out5 < m"] -#[doc = " 0 ≤ eval out2 < m"] -#[doc = " 0 ≤ eval out3 < m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_divstep computes a divstep. +/// +/// Preconditions: +/// 0 ≤ eval arg4 < m +/// 0 ≤ eval arg5 < m +/// Postconditions: +/// out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1) +/// twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2) +/// twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋) +/// eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m) +/// eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m) +/// 0 ≤ eval out5 < m +/// 0 ≤ eval out5 < m +/// 0 ≤ eval out2 < m +/// 0 ≤ eval out3 < m +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0xffffffffffffffff] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_divstep( arg1: u64, @@ -6594,11 +6547,6 @@ pub const fn fiat_p521_scalar_divstep( arg4: &[u64; 9], arg5: &[u64; 9], ) -> (u64, [u64; 10], [u64; 10], [u64; 9], [u64; 9]) { - let mut out1: u64 = 0; - let mut out2: [u64; 10] = [0; 10]; - let mut out3: [u64; 10] = [0; 10]; - let mut out4: [u64; 9] = [0; 9]; - let mut out5: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_addcarryx_u64(0x0, (!arg1), (0x1 as u64)); @@ -7012,44 +6960,11 @@ pub const fn fiat_p521_scalar_divstep( let (x255) = fiat_p521_scalar_cmovznz_u64(x226, x221, x203); let mut x256: u64 = 0; let (x256) = fiat_p521_scalar_cmovznz_u64(x226, x223, x205); - out1 = x227; - out2[0] = x7; - out2[1] = x8; - out2[2] = x9; - out2[3] = x10; - out2[4] = x11; - out2[5] = x12; - out2[6] = x13; - out2[7] = x14; - out2[8] = x15; - out2[9] = x16; - out3[0] = x229; - out3[1] = x230; - out3[2] = x231; - out3[3] = x232; - out3[4] = x233; - out3[5] = x234; - out3[6] = x235; - out3[7] = x236; - out3[8] = x237; - out3[9] = x238; - out4[0] = x239; - out4[1] = x240; - out4[2] = x241; - out4[3] = x242; - out4[4] = x243; - out4[5] = x244; - out4[6] = x245; - out4[7] = x246; - out4[8] = x247; - out5[0] = x248; - out5[1] = x249; - out5[2] = x250; - out5[3] = x251; - out5[4] = x252; - out5[5] = x253; - out5[6] = x254; - out5[7] = x255; - out5[8] = x256; - (out1, out2, out3, out4, out5) + ( + x227, + [x7, x8, x9, x10, x11, x12, x13, x14, x15, x16], + [x229, x230, x231, x232, x233, x234, x235, x236, x237, x238], + [x239, x240, x241, x242, x243, x244, x245, x246, x247], + [x248, x249, x250, x251, x252, x253, x254, x255, x256], + ) } From ac145e3e57763fdf63fae159aa5f911fc003f1f3 Mon Sep 17 00:00:00 2001 From: Arvind Mukund Date: Sun, 29 Oct 2023 22:25:54 -0700 Subject: [PATCH 2/4] Derive extra-impls Signed-off-by: Arvind Mukund --- p521/src/arithmetic/field/p521_64.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index e2be648b..61e1b2a7 100644 --- a/p521/src/arithmetic/field/p521_64.rs +++ b/p521/src/arithmetic/field/p521_64.rs @@ -29,7 +29,7 @@ pub type fiat_p521_u2 = u8; pub type fiat_p521_i2 = i8; /// The type fiat_p521_loose_field_element is a field element with loose bounds. /// Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] -#[derive(Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq, PartialOrd)] pub struct fiat_p521_loose_field_element(pub [u64; 9]); impl core::ops::Index for fiat_p521_loose_field_element { type Output = u64; @@ -46,7 +46,7 @@ impl core::ops::IndexMut for fiat_p521_loose_field_element { } /// The type fiat_p521_tight_field_element is a field element with tight bounds. /// Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] -#[derive(Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq, PartialOrd)] pub struct fiat_p521_tight_field_element(pub [u64; 9]); impl core::ops::Index for fiat_p521_tight_field_element { type Output = u64; From 9ba5e57d0ffe619c169861a0c96eefdf4b7a899e Mon Sep 17 00:00:00 2001 From: Arvind Mukund Date: Sun, 29 Oct 2023 22:50:04 -0700 Subject: [PATCH 3/4] Regenerate field arithmetic Signed-off-by: Arvind Mukund --- p521/src/arithmetic/field/p521_64.rs | 197 +++++++++++++++++++++------ 1 file changed, 159 insertions(+), 38 deletions(-) diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index 61e1b2a7..b6c30403 100644 --- a/p521/src/arithmetic/field/p521_64.rs +++ b/p521/src/arithmetic/field/p521_64.rs @@ -1,8 +1,8 @@ //! fiat-crypto output postprocessed by fiat-constify: -//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p521 64 '(auto)' '2^521 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax +//! Autogenerated: './unsaturated_solinas' --lang Rust --inline p521 64 '(auto)' '2^521 - 1' carry_mul carry_square carry add sub opp carry_add carry_sub carry_opp relax selectznz to_bytes from_bytes //! curve description: p521 //! machine_wordsize = 64 (from "64") -//! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax +//! requested operations: carry_mul, carry_square, carry, add, sub, opp, carry_add, carry_sub, carry_opp, relax, selectznz, to_bytes, from_bytes //! n = 9 (from "(auto)") //! s-c = 2^521 - [(1, 1)] (from "2^521 - 1") //! tight_bounds_multiplier = 1 (from "") @@ -104,13 +104,11 @@ pub const fn fiat_p521_subborrowx_u58( arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); + let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) + - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 58) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x3ffffffffffffff as i128)) as u64); - ( - x3, - (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), - ) + (x3, (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1)) } /// The function fiat_p521_addcarryx_u57 is an addition with carry. /// @@ -155,13 +153,11 @@ pub const fn fiat_p521_subborrowx_u57( arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); + let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) + - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 57) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x1ffffffffffffff as i128)) as u64); - ( - x3, - (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), - ) + (x3, (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1)) } /// The function fiat_p521_cmovznz_u64 is a single-word conditional move. /// @@ -177,8 +173,8 @@ pub const fn fiat_p521_subborrowx_u57( #[inline] pub const fn fiat_p521_cmovznz_u64(arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> u64 { let x1: fiat_p521_u1 = (!(!arg1)); - let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) as i128) - & (0xffffffffffffffff as i128)) as u64); + let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) + as i128) & (0xffffffffffffffff as i128)) as u64); let x3: u64 = ((x2 & arg3) | ((!x2) & arg2)); (x3) } @@ -317,7 +313,17 @@ pub const fn fiat_p521_carry_mul( let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1); let x122: u64 = (x120 & 0x3ffffffffffffff); let x123: u64 = ((x121 as u64) + x98); - (fiat_p521_tight_field_element([x119, x122, x123, x101, x104, x107, x110, x113, x116])) + (fiat_p521_tight_field_element([ + x119, + x122, + x123, + x101, + x104, + x107, + x110, + x113, + x116, + ])) } /// The function fiat_p521_carry_square squares a field element and reduces the result. /// @@ -518,7 +524,9 @@ pub const fn fiat_p521_sub( /// eval out1 mod m = -eval arg1 mod m /// #[inline] -pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_loose_field_element { +pub const fn fiat_p521_opp( + arg1: &fiat_p521_tight_field_element, +) -> fiat_p521_loose_field_element { let arg1 = &arg1.0; let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = (0x7fffffffffffffe - (arg1[1])); @@ -531,6 +539,135 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo let x9: u64 = (0x3fffffffffffffe - (arg1[8])); (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } +/// The function fiat_p521_carry_add adds two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 + eval arg2) mod m +/// +#[inline] +pub const fn fiat_p521_carry_add( + arg1: &fiat_p521_tight_field_element, + arg2: &fiat_p521_tight_field_element, +) -> fiat_p521_tight_field_element { + let arg1 = &arg1.0; + let arg2 = &arg2.0; + let x1: u64 = ((arg1[0]) + (arg2[0])); + let x2: u64 = ((x1 >> 58) + ((arg1[1]) + (arg2[1]))); + let x3: u64 = ((x2 >> 58) + ((arg1[2]) + (arg2[2]))); + let x4: u64 = ((x3 >> 58) + ((arg1[3]) + (arg2[3]))); + let x5: u64 = ((x4 >> 58) + ((arg1[4]) + (arg2[4]))); + let x6: u64 = ((x5 >> 58) + ((arg1[5]) + (arg2[5]))); + let x7: u64 = ((x6 >> 58) + ((arg1[6]) + (arg2[6]))); + let x8: u64 = ((x7 >> 58) + ((arg1[7]) + (arg2[7]))); + let x9: u64 = ((x8 >> 58) + ((arg1[8]) + (arg2[8]))); + let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57)); + let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); + let x12: u64 = (x10 & 0x3ffffffffffffff); + let x13: u64 = (x11 & 0x3ffffffffffffff); + let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); + let x15: u64 = (x4 & 0x3ffffffffffffff); + let x16: u64 = (x5 & 0x3ffffffffffffff); + let x17: u64 = (x6 & 0x3ffffffffffffff); + let x18: u64 = (x7 & 0x3ffffffffffffff); + let x19: u64 = (x8 & 0x3ffffffffffffff); + let x20: u64 = (x9 & 0x1ffffffffffffff); + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) +} +/// The function fiat_p521_carry_sub subtracts two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 - eval arg2) mod m +/// +#[inline] +pub const fn fiat_p521_carry_sub( + arg1: &fiat_p521_tight_field_element, + arg2: &fiat_p521_tight_field_element, +) -> fiat_p521_tight_field_element { + let arg1 = &arg1.0; + let arg2 = &arg2.0; + let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); + let x2: u64 = ((x1 >> 58) + ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]))); + let x3: u64 = ((x2 >> 58) + ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]))); + let x4: u64 = ((x3 >> 58) + ((0x7fffffffffffffe + (arg1[3])) - (arg2[3]))); + let x5: u64 = ((x4 >> 58) + ((0x7fffffffffffffe + (arg1[4])) - (arg2[4]))); + let x6: u64 = ((x5 >> 58) + ((0x7fffffffffffffe + (arg1[5])) - (arg2[5]))); + let x7: u64 = ((x6 >> 58) + ((0x7fffffffffffffe + (arg1[6])) - (arg2[6]))); + let x8: u64 = ((x7 >> 58) + ((0x7fffffffffffffe + (arg1[7])) - (arg2[7]))); + let x9: u64 = ((x8 >> 58) + ((0x3fffffffffffffe + (arg1[8])) - (arg2[8]))); + let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57)); + let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); + let x12: u64 = (x10 & 0x3ffffffffffffff); + let x13: u64 = (x11 & 0x3ffffffffffffff); + let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); + let x15: u64 = (x4 & 0x3ffffffffffffff); + let x16: u64 = (x5 & 0x3ffffffffffffff); + let x17: u64 = (x6 & 0x3ffffffffffffff); + let x18: u64 = (x7 & 0x3ffffffffffffff); + let x19: u64 = (x8 & 0x3ffffffffffffff); + let x20: u64 = (x9 & 0x1ffffffffffffff); + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) +} +/// The function fiat_p521_carry_opp negates a field element. +/// +/// Postconditions: +/// eval out1 mod m = -eval arg1 mod m +/// +#[inline] +pub const fn fiat_p521_carry_opp( + arg1: &fiat_p521_tight_field_element, +) -> fiat_p521_tight_field_element { + let arg1 = &arg1.0; + let x1: u64 = (0x7fffffffffffffe - (arg1[0])); + let x2: u64 = ((((x1 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[1]))); + let x3: u64 = ((((x2 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[2]))); + let x4: u64 = ((((x3 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[3]))); + let x5: u64 = ((((x4 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[4]))); + let x6: u64 = ((((x5 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[5]))); + let x7: u64 = ((((x6 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[6]))); + let x8: u64 = ((((x7 >> 58) as fiat_p521_u1) as u64) + + (0x7fffffffffffffe - (arg1[7]))); + let x9: u64 = ((((x8 >> 58) as fiat_p521_u1) as u64) + + (0x3fffffffffffffe - (arg1[8]))); + let x10: u64 = ((x1 & 0x3ffffffffffffff) + (((x9 >> 57) as fiat_p521_u1) as u64)); + let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff)); + let x12: u64 = (x10 & 0x3ffffffffffffff); + let x13: u64 = (x11 & 0x3ffffffffffffff); + let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff)); + let x15: u64 = (x4 & 0x3ffffffffffffff); + let x16: u64 = (x5 & 0x3ffffffffffffff); + let x17: u64 = (x6 & 0x3ffffffffffffff); + let x18: u64 = (x7 & 0x3ffffffffffffff); + let x19: u64 = (x8 & 0x3ffffffffffffff); + let x20: u64 = (x9 & 0x1ffffffffffffff); + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) +} +/// The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements. +/// +/// Postconditions: +/// out1 = arg1 +/// +#[inline] +pub const fn fiat_p521_relax( + arg1: &fiat_p521_tight_field_element, +) -> fiat_p521_loose_field_element { + let arg1 = &arg1.0; + let x1: u64 = (arg1[0]); + let x2: u64 = (arg1[1]); + let x3: u64 = (arg1[2]); + let x4: u64 = (arg1[3]); + let x5: u64 = (arg1[4]); + let x6: u64 = (arg1[5]); + let x7: u64 = (arg1[6]); + let x8: u64 = (arg1[7]); + let x9: u64 = (arg1[8]); + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) +} /// The function fiat_p521_selectznz is a multi-limb conditional select. /// /// Postconditions: @@ -543,7 +680,11 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo /// Output Bounds: /// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] -pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) -> [u64; 9] { +pub const fn fiat_p521_selectznz( + arg1: fiat_p521_u1, + arg2: &[u64; 9], + arg3: &[u64; 9], +) -> [u64; 9] { let mut x1: u64 = 0; let (x1) = fiat_p521_cmovznz_u64(arg1, (arg2[0]), (arg3[0])); let mut x2: u64 = 0; @@ -989,24 +1130,4 @@ pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_elem let x141: u64 = (x1 + x140); (fiat_p521_tight_field_element([x74, x83, x92, x100, x108, x117, x126, x134, x141])) } -/// The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements. -/// -/// Postconditions: -/// out1 = arg1 -/// -#[inline] -pub const fn fiat_p521_relax( - arg1: &fiat_p521_tight_field_element, -) -> fiat_p521_loose_field_element { - let arg1 = &arg1.0; - let x1: u64 = (arg1[0]); - let x2: u64 = (arg1[1]); - let x3: u64 = (arg1[2]); - let x4: u64 = (arg1[3]); - let x5: u64 = (arg1[4]); - let x6: u64 = (arg1[5]); - let x7: u64 = (arg1[6]); - let x8: u64 = (arg1[7]); - let x9: u64 = (arg1[8]); - (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) -} + From 981108810ee9fb632810d07dac39d73ccb55ec5d Mon Sep 17 00:00:00 2001 From: Arvind Mukund Date: Mon, 30 Oct 2023 23:18:02 -0700 Subject: [PATCH 4/4] Remove all path dependents of `primeorder` P521 alone uses path based primeorder Signed-off-by: Arvind Mukund --- Cargo.lock | 28 +++++++++++++++++++--------- bign256/Cargo.toml | 2 +- bp256/Cargo.toml | 2 +- bp384/Cargo.toml | 2 +- p192/Cargo.toml | 4 ++-- p224/Cargo.toml | 4 ++-- p256/Cargo.toml | 4 ++-- p384/Cargo.toml | 4 ++-- p521/Cargo.toml | 2 +- sm2/Cargo.toml | 2 +- 10 files changed, 32 insertions(+), 22 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ab0300e2..9f28b934 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -48,7 +48,7 @@ dependencies = [ "criterion", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", ] @@ -112,7 +112,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "sha2", ] @@ -122,7 +122,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "sha2", ] @@ -723,7 +723,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "sec1", "serdect", ] @@ -736,7 +736,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "rand_core", "serdect", "sha2", @@ -751,7 +751,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "serdect", @@ -767,7 +767,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "serdect", @@ -779,7 +779,7 @@ name = "p521" version = "0.13.0" dependencies = [ "elliptic-curve", - "primeorder", + "primeorder 0.13.2", "sha2", ] @@ -844,6 +844,16 @@ dependencies = [ "serdect", ] +[[package]] +name = "primeorder" +version = "0.13.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3c2fcef82c0ec6eefcc179b978446c399b3cdf73c392c35604e399eee6df1ee3" +dependencies = [ + "elliptic-curve", + "serdect", +] + [[package]] name = "proc-macro2" version = "1.0.51" @@ -1149,7 +1159,7 @@ version = "0.13.2" dependencies = [ "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.2 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "rfc6979", diff --git a/bign256/Cargo.toml b/bign256/Cargo.toml index 0347e3a4..fb6a3ae3 100644 --- a/bign256/Cargo.toml +++ b/bign256/Cargo.toml @@ -20,7 +20,7 @@ rust-version = "1.65" elliptic-curve = { version = "0.13.6", features = ["hazmat", "sec1"] } # optional dependencies -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } [dev-dependencies] criterion = "0.5" diff --git a/bp256/Cargo.toml b/bp256/Cargo.toml index 659505a1..b9af4174 100644 --- a/bp256/Cargo.toml +++ b/bp256/Cargo.toml @@ -17,7 +17,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa = { version = "0.16", optional = true, default-features = false, features = ["der"] } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/bp384/Cargo.toml b/bp384/Cargo.toml index 8c806f36..d9b418f4 100644 --- a/bp384/Cargo.toml +++ b/bp384/Cargo.toml @@ -17,7 +17,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa = { version = "0.16", optional = true, default-features = false, features = ["der"] } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/p192/Cargo.toml b/p192/Cargo.toml index 892db7fd..bbeb8af4 100644 --- a/p192/Cargo.toml +++ b/p192/Cargo.toml @@ -22,13 +22,13 @@ sec1 = { version = "0.7.3", default-features = false } # optional dependencies ecdsa-core = { version = "0.16.6", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } serdect = { version = "0.2", optional = true, default-features = false } [dev-dependencies] ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.2", features = ["dev"] } [features] default = ["arithmetic", "ecdsa", "pem", "std"] diff --git a/p224/Cargo.toml b/p224/Cargo.toml index 78d7e794..a181acf9 100644 --- a/p224/Cargo.toml +++ b/p224/Cargo.toml @@ -21,7 +21,7 @@ elliptic-curve = { version = "0.13.6", default-features = false, features = ["ha # optional dependencies ecdsa-core = { version = "0.16.6", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -29,7 +29,7 @@ sha2 = { version = "0.10", optional = true, default-features = false } blobby = "0.3" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.2", features = ["dev"] } rand_core = { version = "0.6", features = ["getrandom"] } [features] diff --git a/p256/Cargo.toml b/p256/Cargo.toml index 96ebd10c..f97d8506 100644 --- a/p256/Cargo.toml +++ b/p256/Cargo.toml @@ -22,7 +22,7 @@ elliptic-curve = { version = "0.13.6", default-features = false, features = ["ha # optional dependencies ecdsa-core = { version = "0.16", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.2", features = ["dev"] } proptest = "1" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p384/Cargo.toml b/p384/Cargo.toml index 9f5f5418..58906c84 100644 --- a/p384/Cargo.toml +++ b/p384/Cargo.toml @@ -22,7 +22,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa-core = { version = "0.16", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.2", features = ["dev"] } proptest = "1.3" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p521/Cargo.toml b/p521/Cargo.toml index 5b2a2dea..4a4c452d 100644 --- a/p521/Cargo.toml +++ b/p521/Cargo.toml @@ -20,7 +20,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm sha2 = { version = "0.10", optional = true, default-features = false } # optional dependencies -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { path = "../primeorder", optional = true } [features] default = ["pem", "std"] diff --git a/sm2/Cargo.toml b/sm2/Cargo.toml index 3f37ac73..e0545b62 100644 --- a/sm2/Cargo.toml +++ b/sm2/Cargo.toml @@ -20,7 +20,7 @@ rust-version = "1.65" elliptic-curve = { version = "0.13", default-features = false, features = ["hazmat", "sec1"] } # optional dependencies -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.2", optional = true } rfc6979 = { version = "0.4", optional = true } serdect = { version = "0.2", optional = true, default-features = false } signature = { version = "2", optional = true }