diff --git a/Cargo.lock b/Cargo.lock index dff90077..4c783557 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -797,9 +797,11 @@ version = "0.14.0-pre" dependencies = [ "base16ct", "blobby", + "criterion", "ecdsa", "elliptic-curve", "hex-literal", + "primefield", "primeorder", "proptest", "rand_core", diff --git a/p521/Cargo.toml b/p521/Cargo.toml index eca1e10d..76f0df99 100644 --- a/p521/Cargo.toml +++ b/p521/Cargo.toml @@ -22,6 +22,7 @@ elliptic-curve = { version = "=0.14.0-pre.2", default-features = false, features # optional dependencies ecdsa-core = { version = "=0.17.0-pre.2", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } +primefield = { version = "=0.14.0-pre", optional = true, path = "../primefield" } primeorder = { version = "=0.14.0-pre", optional = true, path = "../primeorder" } rand_core = { version = "0.6", optional = true, default-features = false } serdect = { version = "0.2", optional = true, default-features = false } @@ -34,16 +35,18 @@ hex-literal = "0.4" primeorder = { version = "=0.14.0-pre", features = ["dev"], path = "../primeorder" } proptest = "1.4" rand_core = { version = "0.6", features = ["getrandom"] } +criterion = "0.5.1" [features] default = ["arithmetic", "ecdsa", "getrandom", "pem", "std"] alloc = ["ecdsa-core?/alloc", "elliptic-curve/alloc", "primeorder?/alloc"] std = ["alloc", "ecdsa-core?/std", "elliptic-curve/std"] -arithmetic = ["dep:primeorder"] +arithmetic = ["dep:primefield", "dep:primeorder"] digest = ["ecdsa-core/digest", "ecdsa-core/hazmat"] ecdh = ["arithmetic", "elliptic-curve/ecdh"] ecdsa = ["arithmetic", "ecdsa-core/signing", "ecdsa-core/verifying", "sha512"] +expose-field = ["arithmetic"] getrandom = ["rand_core/getrandom"] hash2curve = ["arithmetic", "elliptic-curve/hash2curve"] jwk = ["elliptic-curve/jwk"] @@ -57,3 +60,12 @@ voprf = ["elliptic-curve/voprf", "dep:sha2"] [package.metadata.docs.rs] all-features = true rustdoc-args = ["--cfg", "docsrs"] + +[[bench]] +name = "field" +harness = false +required-features = ["expose-field"] + +[[bench]] +name = "scalar" +harness = false diff --git a/p521/benches/field.rs b/p521/benches/field.rs new file mode 100644 index 00000000..19907e74 --- /dev/null +++ b/p521/benches/field.rs @@ -0,0 +1,54 @@ +//! secp521r1 field element benchmarks + +use criterion::{ + black_box, criterion_group, criterion_main, measurement::Measurement, BenchmarkGroup, Criterion, +}; +use hex_literal::hex; +use p521::{FieldBytes, FieldElement}; + +fn test_field_element_x() -> FieldElement { + black_box(FieldElement::from_bytes( + &FieldBytes::clone_from_slice(&hex!("01a7596d38aac7868327ddc1ef5e8178cf052b7ebc512828e8a45955d85bef49494d15278198bbcc5454358c12a2af9a3874e7002e1a2f02fcb36ff3e3b4bc0c69e7")) + ) + .unwrap()) +} + +fn test_field_element_y() -> FieldElement { + black_box(FieldElement::from_bytes( + &FieldBytes::clone_from_slice(&hex!("0184902e515982bb225b8c84f245e61b327c08e94d41c07d0b4101a963e02fe52f6a9f33e8b1de2394e0cb74c40790b4e489b5500e6804cabed0fe8c192443d4027b")) + ) + .unwrap()) +} + +fn bench_field_element_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + let y = test_field_element_y(); + group.bench_function("mul", |b| b.iter(|| &x * &y)); +} + +fn bench_field_element_square<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("square", |b| b.iter(|| x.square())); +} + +fn bench_field_element_sqrt<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("sqrt", |b| b.iter(|| x.sqrt())); +} + +fn bench_field_element_invert<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("invert", |b| b.iter(|| x.invert())); +} + +fn bench_field_element(c: &mut Criterion) { + let mut group = c.benchmark_group("field element operations"); + bench_field_element_mul(&mut group); + bench_field_element_square(&mut group); + bench_field_element_invert(&mut group); + bench_field_element_sqrt(&mut group); + group.finish(); +} + +criterion_group!(benches, bench_field_element); +criterion_main!(benches); diff --git a/p521/benches/scalar.rs b/p521/benches/scalar.rs new file mode 100644 index 00000000..9979c6ec --- /dev/null +++ b/p521/benches/scalar.rs @@ -0,0 +1,73 @@ +//! secp521r1 scalar arithmetic benchmarks + +use criterion::{ + black_box, criterion_group, criterion_main, measurement::Measurement, BenchmarkGroup, Criterion, +}; +use hex_literal::hex; +use p521::{elliptic_curve::group::ff::PrimeField, FieldBytes, ProjectivePoint, Scalar}; + +fn test_scalar_x() -> Scalar { + black_box(Scalar::from_repr( + FieldBytes::clone_from_slice(&hex!("01d7bb864c5b5ecae019296cf9b5c63a166f5f1113942819b1933d889a96d12245777a99428f93de4fc9a18d709bf91889d7f8dddd522b4c364aeae13c983e9fae46")) + ).unwrap()) +} + +fn test_scalar_y() -> Scalar { + black_box(Scalar::from_repr( + FieldBytes::clone_from_slice(&hex!("017e49b8ea8f9d1b7c0378e378a7a42e68e12cf78779ed41dcd29a090ae7e0f883b0d0f2cbc8f0473c0ad6732bea40d371a7f363bc6537d075bd1a4c23e558b0bc73")) + ).unwrap()) +} + +fn bench_point_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let p = ProjectivePoint::GENERATOR; + let m = test_scalar_x(); + let s = Scalar::from_repr(m.into()).unwrap(); + group.bench_function("point-scalar mul", |b| b.iter(|| &p * &s)); +} + +fn bench_scalar_sub<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("sub", |b| b.iter(|| &x - &y)); +} + +fn bench_scalar_add<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("add", |b| b.iter(|| &x + &y)); +} + +fn bench_scalar_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("mul", |b| b.iter(|| &x * &y)); +} + +fn bench_scalar_negate<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + group.bench_function("negate", |b| b.iter(|| -x)); +} + +fn bench_scalar_invert<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + group.bench_function("invert", |b| b.iter(|| x.invert())); +} + +fn bench_point(c: &mut Criterion) { + let mut group = c.benchmark_group("point operations"); + bench_point_mul(&mut group); + group.finish(); +} + +fn bench_scalar(c: &mut Criterion) { + let mut group = c.benchmark_group("scalar operations"); + bench_scalar_sub(&mut group); + bench_scalar_add(&mut group); + bench_scalar_mul(&mut group); + bench_scalar_negate(&mut group); + bench_scalar_invert(&mut group); + group.finish(); +} + +criterion_group!(benches, bench_point, bench_scalar); +criterion_main!(benches); diff --git a/p521/src/arithmetic/field.rs b/p521/src/arithmetic/field.rs index a3ef84cd..ba658514 100644 --- a/p521/src/arithmetic/field.rs +++ b/p521/src/arithmetic/field.rs @@ -397,13 +397,15 @@ impl From for FieldElement { impl ConditionallySelectable for FieldElement { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO; + let mut ret = Self::ZERO.0.into_inner(); + let a = a.0.as_inner(); + let b = b.0.as_inner(); - for i in 0..ret.0.len() { - ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); + for i in 0..ret.len() { + ret[i] = u64::conditional_select(&a[i], &b[i], choice); } - ret + Self(fiat_p521_tight_field_element(ret)) } } @@ -666,7 +668,7 @@ mod tests { use super::FieldElement; use elliptic_curve::ff::PrimeField; use hex_literal::hex; - use primeorder::{ + use primefield::{ impl_field_identity_tests, impl_field_invert_tests, impl_field_sqrt_tests, impl_primefield_tests, }; diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index 46e08f4c..b72668d8 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: './fiat-crypto' unsaturated-solinas --lang Rust --inline p521 64 9 '2^521 - 1' +//! curve description: p521 +//! machine_wordsize = 64 (from "64") +//! requested operations: (all) +//! n = 9 (from "9") +//! 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( @@ -23,156 +23,181 @@ unused_mut, unused_variables )] +/// fiat_p521_u1 represents values of 1 bits, stored in one byte. pub type fiat_p521_u1 = u8; +/// fiat_p521_i1 represents values of 1 bits, stored in one byte. pub type fiat_p521_i1 = i8; +/// fiat_p521_u2 represents values of 2 bits, stored in one byte. pub type fiat_p521_u2 = u8; +/// fiat_p521_i2 represents values of 2 bits, stored in one byte. 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, Debug, PartialEq, Eq, PartialOrd, Ord)] +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, Debug, PartialEq, Eq, PartialOrd, Ord)] +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.as_inner(); + let arg2 = arg2.as_inner(); 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 +321,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.as_inner(); let x1: u64 = (arg1[8]); let x2: u64 = (x1 * 0x2); let x3: u64 = ((arg1[8]) * 0x2); @@ -420,27 +436,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.as_inner(); let x1: u64 = (arg1[0]); let x2: u64 = ((x1 >> 58) + (arg1[1])); let x3: u64 = ((x2 >> 58) + (arg1[2])); @@ -461,28 +468,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.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((arg1[1]) + (arg2[1])); let x3: u64 = ((arg1[2]) + (arg2[2])); @@ -492,28 +491,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.as_inner(); + let arg2 = arg2.as_inner(); 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 +514,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.as_inner(); let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = (0x7fffffffffffffe - (arg1[1])); let x3: u64 = (0x7fffffffffffffe - (arg1[2])); @@ -551,28 +533,20 @@ 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 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[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 = ""] +/// 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 mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); 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]))); @@ -593,28 +567,20 @@ pub const fn fiat_p521_carry_add( 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_carry_sub subtracts two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] -#[doc = ""] +/// 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 mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); 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]))); @@ -635,27 +601,18 @@ pub const fn fiat_p521_carry_sub( 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_carry_opp negates a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = -eval arg1 mod m"] -#[doc = ""] +/// 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 mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); 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]))); @@ -676,27 +633,18 @@ pub const fn fiat_p521_carry_opp( 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_relax is the identity function converting from tight field elements to loose field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = arg1"] -#[doc = ""] +/// 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 mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[0]); let x2: u64 = (arg1[1]); let x3: u64 = (arg1[2]); @@ -706,31 +654,21 @@ pub const fn fiat_p521_relax( 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 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[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 +687,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.as_inner(); 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 +893,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 +1112,25 @@ 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])) +} +impl fiat_p521_loose_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } +} +impl fiat_p521_tight_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } } diff --git a/p521/src/arithmetic/scalar.rs b/p521/src/arithmetic/scalar.rs index 13c6726b..159152be 100644 --- a/p521/src/arithmetic/scalar.rs +++ b/p521/src/arithmetic/scalar.rs @@ -34,7 +34,7 @@ use elliptic_curve::{ zeroize::DefaultIsZeroes, Curve as _, Error, FieldBytesEncoding, Result, ScalarPrimitive, }; -use primeorder::{impl_bernstein_yang_invert, impl_field_op}; +use primefield::{impl_bernstein_yang_invert, impl_field_op}; #[cfg(feature = "bits")] use {crate::ScalarBits, elliptic_curve::group::ff::PrimeFieldBits}; @@ -130,9 +130,9 @@ impl Scalar { /// Used incorrectly this can lead to invalid results! #[cfg(target_pointer_width = "32")] pub(crate) const fn from_uint_unchecked(w: U576) -> Self { - Self(fiat_p521_scalar_to_montgomery(&u32x18_to_u64x9( - w.as_words(), - ))) + Self(fiat_p521_scalar_to_montgomery( + &fiat_p521_scalar_non_montgomery_domain_field_element(u32x18_to_u64x9(w.as_words())), + )) } /// Decode [`Scalar`] from [`U576`] converting it into Montgomery form. @@ -142,7 +142,9 @@ impl Scalar { /// Used incorrectly this can lead to invalid results! #[cfg(target_pointer_width = "64")] pub(crate) const fn from_uint_unchecked(w: U576) -> Self { - Self(fiat_p521_scalar_to_montgomery(w.as_words())) + Self(fiat_p521_scalar_to_montgomery( + &fiat_p521_scalar_non_montgomery_domain_field_element(*w.as_words()), + )) } /// Returns the big-endian encoding of this [`Scalar`]. @@ -155,7 +157,9 @@ impl Scalar { #[inline] #[cfg(target_pointer_width = "32")] pub const fn to_canonical(self) -> U576 { - U576::from_words(u64x9_to_u32x18(&fiat_p521_scalar_from_montgomery(&self.0))) + U576::from_words(u64x9_to_u32x18( + fiat_p521_scalar_from_montgomery(&self.0).as_inner(), + )) } /// Translate [`Scalar`] out of the Montgomery domain, returning a [`U576`] @@ -163,7 +167,7 @@ impl Scalar { #[inline] #[cfg(target_pointer_width = "64")] pub const fn to_canonical(self) -> U576 { - U576::from_words(fiat_p521_scalar_from_montgomery(&self.0)) + U576::from_words(fiat_p521_scalar_from_montgomery(&self.0).into_inner()) } /// Determine if this [`Scalar`] is odd in the SEC1 sense: `self mod 2 == 1`. @@ -234,6 +238,7 @@ impl Scalar { 521, 9, u64, + fiat_p521_scalar_montgomery_domain_field_element, fiat_p521_scalar_from_montgomery, fiat_p521_scalar_mul, fiat_p521_scalar_opp, @@ -288,10 +293,12 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "32")] pub const fn shr_vartime(&self, shift: u32) -> Scalar { - Self(u32x18_to_u64x9( - &U576::from_words(u64x9_to_u32x18(&self.0)) - .wrapping_shr_vartime(shift) - .to_words(), + Self(fiat_p521_scalar_montgomery_domain_field_element( + u32x18_to_u64x9( + &U576::from_words(u64x9_to_u32x18(self.0.as_inner())) + .wrapping_shr_vartime(shift) + .to_words(), + ), )) } @@ -300,11 +307,11 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "64")] pub const fn shr_vartime(&self, shift: u32) -> Scalar { - Self( - U576::from_words(self.0) + Self(fiat_p521_scalar_montgomery_domain_field_element( + U576::from_words(self.0.into_inner()) .wrapping_shr_vartime(shift) .to_words(), - ) + )) } } @@ -323,7 +330,7 @@ impl Default for Scalar { impl Eq for Scalar {} impl PartialEq for Scalar { fn eq(&self, rhs: &Self) -> bool { - self.0.ct_eq(&(rhs.0)).into() + self.0.as_inner().ct_eq(rhs.0.as_inner()).into() } } @@ -347,19 +354,21 @@ impl From for Scalar { impl ConditionallySelectable for Scalar { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO; + let mut ret = Self::ZERO.0.into_inner(); + let a = a.0.as_inner(); + let b = b.0.as_inner(); - for i in 0..ret.0.len() { - ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); + for i in 0..ret.len() { + ret[i] = u64::conditional_select(&a[i], &b[i], choice); } - ret + Self(fiat_p521_scalar_montgomery_domain_field_element(ret)) } } impl ConstantTimeEq for Scalar { fn ct_eq(&self, other: &Self) -> Choice { - self.0.ct_eq(&other.0) + self.0.as_inner().ct_eq(other.0.as_inner()) } } @@ -682,7 +691,7 @@ impl<'de> Deserialize<'de> for Scalar { mod tests { use super::Scalar; use elliptic_curve::PrimeField; - use primeorder::{impl_field_identity_tests, impl_field_invert_tests, impl_primefield_tests}; + use primefield::{impl_field_identity_tests, impl_field_invert_tests, impl_primefield_tests}; /// t = (modulus - 1) >> S const T: [u64; 9] = [ diff --git a/p521/src/arithmetic/scalar/p521_scalar_64.rs b/p521/src/arithmetic/scalar/p521_scalar_64.rs index 60c8646f..6b47cc92 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: './fiat-crypto' 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( @@ -28,128 +28,154 @@ unused_mut, unused_variables )] +/// fiat_p521_scalar_u1 represents values of 1 bits, stored in one byte. pub type fiat_p521_scalar_u1 = u8; +/// fiat_p521_scalar_i1 represents values of 1 bits, stored in one byte. pub type fiat_p521_scalar_i1 = i8; +/// fiat_p521_scalar_u2 represents values of 2 bits, stored in one byte. pub type fiat_p521_scalar_u2 = u8; +/// fiat_p521_scalar_i2 represents values of 2 bits, stored in one byte. 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(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +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(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +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.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -1688,30 +1714,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.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -3250,32 +3269,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.as_inner(); + let arg2 = arg2.as_inner(); 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 +3364,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.as_inner(); + let arg2 = arg2.as_inner(); 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 +3440,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.as_inner(); 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 +3513,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.as_inner(); let x1: u64 = (arg1[0]); let mut x2: u64 = 0; let mut x3: u64 = 0; @@ -4540,30 +4533,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.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -6059,57 +6045,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 +6104,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 +6242,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 +6448,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 +6551,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 +6964,31 @@ 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], + ) +} +impl fiat_p521_scalar_montgomery_domain_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } +} +impl fiat_p521_scalar_non_montgomery_domain_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } } diff --git a/p521/src/lib.rs b/p521/src/lib.rs index 4a42a808..c6e1c8af 100644 --- a/p521/src/lib.rs +++ b/p521/src/lib.rs @@ -40,6 +40,9 @@ pub mod test_vectors; #[cfg(feature = "arithmetic")] pub use arithmetic::{scalar::Scalar, AffinePoint, ProjectivePoint}; +#[cfg(feature = "expose-field")] +pub use arithmetic::field::FieldElement; + pub use elliptic_curve::{self, bigint::U576}; #[cfg(feature = "pkcs8")] diff --git a/primefield/src/lib.rs b/primefield/src/lib.rs index b7685221..d63fdebc 100644 --- a/primefield/src/lib.rs +++ b/primefield/src/lib.rs @@ -7,3 +7,665 @@ #![forbid(unsafe_code)] #![warn(missing_docs, rust_2018_idioms, unused_qualifications)] #![doc = include_str!("../README.md")] + +/// Implements a field element type whose internal representation is in +/// Montgomery form, providing a combination of trait impls and inherent impls +/// which are `const fn` where possible. +/// +/// Accepts a set of `const fn` arithmetic operation functions as arguments. +/// +/// # Inherent impls +/// - `const ZERO: Self` +/// - `const ONE: Self` (multiplicative identity) +/// - `pub fn from_bytes` +/// - `pub fn from_slice` +/// - `pub fn from_uint` +/// - `fn from_uint_unchecked` +/// - `pub fn to_bytes` +/// - `pub fn to_canonical` +/// - `pub fn is_odd` +/// - `pub fn is_zero` +/// - `pub fn double` +/// +/// NOTE: field implementations must provide their own inherent impls of +/// the following methods in order for the code generated by this macro to +/// compile: +/// +/// - `pub fn invert` +/// - `pub fn sqrt` +/// +/// # Trait impls +/// - `AsRef<$arr>` +/// - `ConditionallySelectable` +/// - `ConstantTimeEq` +/// - `ConstantTimeGreater` +/// - `ConstantTimeLess` +/// - `Default` +/// - `DefaultIsZeroes` +/// - `Eq` +/// - `Field` +/// - `PartialEq` +/// +/// ## Ops +/// - `Add` +/// - `AddAssign` +/// - `Sub` +/// - `SubAssign` +/// - `Mul` +/// - `MulAssign` +/// - `Neg` +#[macro_export] +macro_rules! impl_mont_field_element { + ( + $curve:tt, + $fe:tt, + $bytes:ty, + $uint:ty, + $modulus:expr, + $arr:ty, + $from_mont:ident, + $to_mont:ident, + $add:ident, + $sub:ident, + $mul:ident, + $neg:ident, + $square:ident + ) => { + impl $fe { + /// Zero element. + pub const ZERO: Self = Self(<$uint>::ZERO); + + /// Multiplicative identity. + pub const ONE: Self = Self::from_uint_unchecked(<$uint>::ONE); + + /// Create a [` + #[doc = stringify!($fe)] + /// `] from a canonical big-endian representation. + pub fn from_bytes(repr: &$bytes) -> $crate::elliptic_curve::subtle::CtOption { + use $crate::elliptic_curve::FieldBytesEncoding; + Self::from_uint(FieldBytesEncoding::<$curve>::decode_field_bytes(repr)) + } + + /// Decode [` + #[doc = stringify!($fe)] + /// `] from a big endian byte slice. + pub fn from_slice(slice: &[u8]) -> $crate::elliptic_curve::Result { + use $crate::elliptic_curve::array::{typenum::Unsigned, Array}; + + if slice.len() != <$curve as $crate::elliptic_curve::Curve>::FieldBytesSize::USIZE { + return Err($crate::elliptic_curve::Error); + } + + Option::from(Self::from_bytes(Array::from_slice(slice))) + .ok_or($crate::elliptic_curve::Error) + } + + /// Decode [` + #[doc = stringify!($fe)] + /// `] + /// from [` + #[doc = stringify!($uint)] + /// `] converting it into Montgomery form: + /// + /// ```text + /// w * R^2 * R^-1 mod p = wR mod p + /// ``` + pub fn from_uint(uint: $uint) -> $crate::elliptic_curve::subtle::CtOption { + use $crate::elliptic_curve::subtle::ConstantTimeLess as _; + let is_some = uint.ct_lt(&$modulus); + $crate::elliptic_curve::subtle::CtOption::new( + Self::from_uint_unchecked(uint), + is_some, + ) + } + + /// Parse a [` + #[doc = stringify!($fe)] + /// `] from big endian hex-encoded bytes. + /// + /// Does *not* perform a check that the field element does not overflow the order. + /// + /// This method is primarily intended for defining internal constants. + #[allow(dead_code)] + pub(crate) const fn from_hex(hex: &str) -> Self { + Self::from_uint_unchecked(<$uint>::from_be_hex(hex)) + } + + /// Convert a `u64` into a [` + #[doc = stringify!($fe)] + /// `]. + pub const fn from_u64(w: u64) -> Self { + Self::from_uint_unchecked(<$uint>::from_u64(w)) + } + + /// Decode [` + #[doc = stringify!($fe)] + /// `] from [` + #[doc = stringify!($uint)] + /// `] converting it into Montgomery form. + /// + /// Does *not* perform a check that the field element does not overflow the order. + /// + /// Used incorrectly this can lead to invalid results! + pub(crate) const fn from_uint_unchecked(w: $uint) -> Self { + Self(<$uint>::from_words($to_mont(w.as_words()))) + } + + /// Returns the big-endian encoding of this [` + #[doc = stringify!($fe)] + /// `]. + pub fn to_bytes(self) -> $bytes { + use $crate::elliptic_curve::FieldBytesEncoding; + FieldBytesEncoding::<$curve>::encode_field_bytes(&self.to_canonical()) + } + + /// Translate [` + #[doc = stringify!($fe)] + /// `] out of the Montgomery domain, returning a [` + #[doc = stringify!($uint)] + /// `] in canonical form. + #[inline] + pub const fn to_canonical(self) -> $uint { + <$uint>::from_words($from_mont(self.0.as_words())) + } + + /// Determine if this [` + #[doc = stringify!($fe)] + /// `] is odd in the SEC1 sense: `self mod 2 == 1`. + /// + /// # Returns + /// + /// If odd, return `Choice(1)`. Otherwise, return `Choice(0)`. + pub fn is_odd(&self) -> Choice { + use $crate::elliptic_curve::bigint::Integer; + self.to_canonical().is_odd() + } + + /// Determine if this [` + #[doc = stringify!($fe)] + /// `] is even in the SEC1 sense: `self mod 2 == 0`. + /// + /// # Returns + /// + /// If even, return `Choice(1)`. Otherwise, return `Choice(0)`. + pub fn is_even(&self) -> Choice { + !self.is_odd() + } + + /// Determine if this [` + #[doc = stringify!($fe)] + /// `] is zero. + /// + /// # Returns + /// + /// If zero, return `Choice(1)`. Otherwise, return `Choice(0)`. + pub fn is_zero(&self) -> Choice { + self.ct_eq(&Self::ZERO) + } + + /// Add elements. + pub const fn add(&self, rhs: &Self) -> Self { + Self(<$uint>::from_words($add( + self.0.as_words(), + rhs.0.as_words(), + ))) + } + + /// Double element (add it to itself). + #[must_use] + pub const fn double(&self) -> Self { + self.add(self) + } + + /// Subtract elements. + pub const fn sub(&self, rhs: &Self) -> Self { + Self(<$uint>::from_words($sub( + self.0.as_words(), + rhs.0.as_words(), + ))) + } + + /// Multiply elements. + pub const fn multiply(&self, rhs: &Self) -> Self { + Self(<$uint>::from_words($mul( + self.0.as_words(), + rhs.0.as_words(), + ))) + } + + /// Negate element. + pub const fn neg(&self) -> Self { + Self(<$uint>::from_words($neg(self.0.as_words()))) + } + + /// Compute modular square. + #[must_use] + pub const fn square(&self) -> Self { + Self(<$uint>::from_words($square(self.0.as_words()))) + } + + /// Returns `self^exp`, where `exp` is a little-endian integer exponent. + /// + /// **This operation is variable time with respect to the exponent.** + /// + /// If the exponent is fixed, this operation is effectively constant time. + pub const fn pow_vartime(&self, exp: &[u64]) -> Self { + let mut res = Self::ONE; + let mut i = exp.len(); + + while i > 0 { + i -= 1; + + let mut j = 64; + while j > 0 { + j -= 1; + res = res.square(); + + if ((exp[i] >> j) & 1) == 1 { + res = res.multiply(self); + } + } + } + + res + } + } + + $crate::impl_mont_field_element_arithmetic!( + $fe, $bytes, $uint, $arr, $add, $sub, $mul, $neg + ); + }; +} + +/// Add arithmetic impls to the given field element. +#[macro_export] +macro_rules! impl_mont_field_element_arithmetic { + ( + $fe:tt, + $bytes:ty, + $uint:ty, + $arr:ty, + $add:ident, + $sub:ident, + $mul:ident, + $neg:ident + ) => { + impl AsRef<$arr> for $fe { + fn as_ref(&self) -> &$arr { + self.0.as_ref() + } + } + + impl Default for $fe { + fn default() -> Self { + Self::ZERO + } + } + + impl Eq for $fe {} + impl PartialEq for $fe { + fn eq(&self, rhs: &Self) -> bool { + self.0.ct_eq(&(rhs.0)).into() + } + } + + impl From for $fe { + fn from(n: u32) -> $fe { + Self::from_uint_unchecked(<$uint>::from(n)) + } + } + + impl From for $fe { + fn from(n: u64) -> $fe { + Self::from_uint_unchecked(<$uint>::from(n)) + } + } + + impl From for $fe { + fn from(n: u128) -> $fe { + Self::from_uint_unchecked(<$uint>::from(n)) + } + } + + impl $crate::elliptic_curve::subtle::ConditionallySelectable for $fe { + fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { + Self(<$uint>::conditional_select(&a.0, &b.0, choice)) + } + } + + impl $crate::elliptic_curve::subtle::ConstantTimeEq for $fe { + fn ct_eq(&self, other: &Self) -> $crate::elliptic_curve::subtle::Choice { + self.0.ct_eq(&other.0) + } + } + + impl $crate::elliptic_curve::subtle::ConstantTimeGreater for $fe { + fn ct_gt(&self, other: &Self) -> $crate::elliptic_curve::subtle::Choice { + self.0.ct_gt(&other.0) + } + } + + impl $crate::elliptic_curve::subtle::ConstantTimeLess for $fe { + fn ct_lt(&self, other: &Self) -> $crate::elliptic_curve::subtle::Choice { + self.0.ct_lt(&other.0) + } + } + + impl $crate::elliptic_curve::zeroize::DefaultIsZeroes for $fe {} + + impl $crate::elliptic_curve::ff::Field for $fe { + const ZERO: Self = Self::ZERO; + const ONE: Self = Self::ONE; + + fn random(mut rng: impl $crate::elliptic_curve::rand_core::RngCore) -> Self { + // NOTE: can't use ScalarPrimitive::random due to CryptoRng bound + let mut bytes = <$bytes>::default(); + + loop { + rng.fill_bytes(&mut bytes); + if let Some(fe) = Self::from_bytes(&bytes).into() { + return fe; + } + } + } + + fn is_zero(&self) -> Choice { + Self::ZERO.ct_eq(self) + } + + #[must_use] + fn square(&self) -> Self { + self.square() + } + + #[must_use] + fn double(&self) -> Self { + self.double() + } + + fn invert(&self) -> CtOption { + self.invert() + } + + fn sqrt(&self) -> CtOption { + self.sqrt() + } + + fn sqrt_ratio(num: &Self, div: &Self) -> (Choice, Self) { + $crate::elliptic_curve::ff::helpers::sqrt_ratio_generic(num, div) + } + } + + $crate::impl_field_op!($fe, Add, add, $add); + $crate::impl_field_op!($fe, Sub, sub, $sub); + $crate::impl_field_op!($fe, Mul, mul, $mul); + + impl AddAssign<$fe> for $fe { + #[inline] + fn add_assign(&mut self, other: $fe) { + *self = *self + other; + } + } + + impl AddAssign<&$fe> for $fe { + #[inline] + fn add_assign(&mut self, other: &$fe) { + *self = *self + other; + } + } + + impl SubAssign<$fe> for $fe { + #[inline] + fn sub_assign(&mut self, other: $fe) { + *self = *self - other; + } + } + + impl SubAssign<&$fe> for $fe { + #[inline] + fn sub_assign(&mut self, other: &$fe) { + *self = *self - other; + } + } + + impl MulAssign<&$fe> for $fe { + #[inline] + fn mul_assign(&mut self, other: &$fe) { + *self = *self * other; + } + } + + impl MulAssign for $fe { + #[inline] + fn mul_assign(&mut self, other: $fe) { + *self = *self * other; + } + } + + impl Neg for $fe { + type Output = $fe; + + #[inline] + fn neg(self) -> $fe { + Self($neg(self.as_ref()).into()) + } + } + + impl Sum for $fe { + fn sum>(iter: I) -> Self { + iter.reduce(core::ops::Add::add).unwrap_or(Self::ZERO) + } + } + + impl<'a> Sum<&'a $fe> for $fe { + fn sum>(iter: I) -> Self { + iter.copied().sum() + } + } + + impl Product for $fe { + fn product>(iter: I) -> Self { + iter.reduce(core::ops::Mul::mul).unwrap_or(Self::ONE) + } + } + + impl<'a> Product<&'a $fe> for $fe { + fn product>(iter: I) -> Self { + iter.copied().product() + } + } + }; +} + +/// Emit impls for a `core::ops` trait for all combinations of reference types, +/// which thunk to the given function. +#[macro_export] +macro_rules! impl_field_op { + ($fe:tt, $op:tt, $op_fn:ident, $func:ident) => { + impl ::core::ops::$op for $fe { + type Output = $fe; + + #[inline] + fn $op_fn(self, rhs: $fe) -> $fe { + $fe($func(self.as_ref(), rhs.as_ref()).into()) + } + } + + impl ::core::ops::$op<&$fe> for $fe { + type Output = $fe; + + #[inline] + fn $op_fn(self, rhs: &$fe) -> $fe { + $fe($func(self.as_ref(), rhs.as_ref()).into()) + } + } + + impl ::core::ops::$op<&$fe> for &$fe { + type Output = $fe; + + #[inline] + fn $op_fn(self, rhs: &$fe) -> $fe { + $fe($func(self.as_ref(), rhs.as_ref()).into()) + } + } + }; +} + +/// Implement Bernstein-Yang field element inversion. +#[macro_export] +macro_rules! impl_bernstein_yang_invert { + ( + $a:expr, + $one:expr, + $d:expr, + $nlimbs:expr, + $word:ty, + $mont_type: expr, + $from_mont:ident, + $mul:ident, + $neg:ident, + $divstep_precomp:ident, + $divstep:ident, + $msat:ident, + $selectznz:ident, + ) => {{ + // See Bernstein-Yang 2019 p.366 + const ITERATIONS: usize = (49 * $d + 57) / 17; + + let a = $from_mont($a); + let mut d = 1; + let mut f = $msat(); + let mut g = [0; $nlimbs + 1]; + let mut v = $mont_type([0; $nlimbs]); + let mut r = $one.into_inner(); + let mut i = 0; + let mut j = 0; + + while j < $nlimbs { + g[j] = a.as_inner()[j]; + j += 1; + } + + while i < ITERATIONS - ITERATIONS % 2 { + let (out1, out2, out3, out4, out5) = $divstep(d, &f, &g, &v.0, &r); + let (out1, out2, out3, out4, out5) = $divstep(out1, &out2, &out3, &out4, &out5); + d = out1; + f = out2; + g = out3; + v = $mont_type(out4); + r = out5; + i += 2; + } + + if ITERATIONS % 2 != 0 { + let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, v.as_inner(), &r); + v = $mont_type(out4); + f = out2; + } + + let s = ((f[f.len() - 1] >> <$word>::BITS - 1) & 1) as u8; + let v = $mont_type($selectznz(s, v.as_inner(), $neg(&v).as_inner())); + $mul(&v, &$mont_type($divstep_precomp())) + }}; +} + +/// Implement field element identity tests. +#[macro_export] +macro_rules! impl_field_identity_tests { + ($fe:tt) => { + #[test] + fn zero_is_additive_identity() { + let zero = $fe::ZERO; + let one = $fe::ONE; + assert_eq!(zero.add(&zero), zero); + assert_eq!(one.add(&zero), one); + } + + #[test] + fn one_is_multiplicative_identity() { + let one = $fe::ONE; + assert_eq!(one.multiply(&one), one); + } + }; +} + +/// Implement field element inversion tests. +#[macro_export] +macro_rules! impl_field_invert_tests { + ($fe:tt) => { + #[test] + fn invert() { + let one = $fe::ONE; + assert_eq!(one.invert().unwrap(), one); + + let three = one + &one + &one; + let inv_three = three.invert().unwrap(); + assert_eq!(three * &inv_three, one); + + let minus_three = -three; + let inv_minus_three = minus_three.invert().unwrap(); + assert_eq!(inv_minus_three, -inv_three); + assert_eq!(three * &inv_minus_three, -one); + } + }; +} + +/// Implement field element square root tests. +#[macro_export] +macro_rules! impl_field_sqrt_tests { + ($fe:tt) => { + #[test] + fn sqrt() { + for &n in &[1u64, 4, 9, 16, 25, 36, 49, 64] { + let fe = $fe::from(n); + let sqrt = fe.sqrt().unwrap(); + assert_eq!(sqrt.square(), fe); + } + } + }; +} + +/// Implement tests for the `PrimeField` trait. +#[macro_export] +macro_rules! impl_primefield_tests { + ($fe:tt, $t:expr) => { + #[test] + fn two_inv_constant() { + assert_eq!($fe::from(2u32) * $fe::TWO_INV, $fe::ONE); + } + + #[test] + fn root_of_unity_constant() { + assert!($fe::S < 128); + let two_to_s = 1u128 << $fe::S; + + // ROOT_OF_UNITY^{2^s} mod m == 1 + assert_eq!( + $fe::ROOT_OF_UNITY.pow_vartime(&[ + (two_to_s & 0xFFFFFFFFFFFFFFFF) as u64, + (two_to_s >> 64) as u64, + 0, + 0 + ]), + $fe::ONE + ); + + // MULTIPLICATIVE_GENERATOR^{t} mod m == ROOT_OF_UNITY + assert_eq!( + $fe::MULTIPLICATIVE_GENERATOR.pow_vartime(&$t), + $fe::ROOT_OF_UNITY + ) + } + + #[test] + fn root_of_unity_inv_constant() { + assert_eq!($fe::ROOT_OF_UNITY * $fe::ROOT_OF_UNITY_INV, $fe::ONE); + } + + #[test] + fn delta_constant() { + // DELTA^{t} mod m == 1 + assert_eq!($fe::DELTA.pow_vartime(&$t), $fe::ONE); + } + }; +} diff --git a/primeorder/src/field.rs b/primeorder/src/field.rs index 44070228..732a17b6 100644 --- a/primeorder/src/field.rs +++ b/primeorder/src/field.rs @@ -510,6 +510,7 @@ macro_rules! impl_bernstein_yang_invert { $d:expr, $nlimbs:expr, $word:ty, + $mont_type: expr, $from_mont:ident, $mul:ident, $neg:ident, @@ -525,36 +526,36 @@ macro_rules! impl_bernstein_yang_invert { let mut d = 1; let mut f = $msat(); let mut g = [0; $nlimbs + 1]; - let mut v = [0; $nlimbs]; - let mut r = $one; + let mut v = $mont_type([0; $nlimbs]); + let mut r = $one.into_inner(); let mut i = 0; let mut j = 0; while j < $nlimbs { - g[j] = a[j]; + g[j] = a.as_inner()[j]; j += 1; } while i < ITERATIONS - ITERATIONS % 2 { - let (out1, out2, out3, out4, out5) = $divstep(d, &f, &g, &v, &r); + let (out1, out2, out3, out4, out5) = $divstep(d, &f, &g, &v.0, &r); let (out1, out2, out3, out4, out5) = $divstep(out1, &out2, &out3, &out4, &out5); d = out1; f = out2; g = out3; - v = out4; + v = $mont_type(out4); r = out5; i += 2; } if ITERATIONS % 2 != 0 { - let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, &v, &r); - v = out4; + let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, v.as_inner(), &r); + v = $mont_type(out4); f = out2; } let s = ((f[f.len() - 1] >> <$word>::BITS - 1) & 1) as u8; - let v = $selectznz(s, &v, &$neg(&v)); - $mul(&v, &$divstep_precomp()) + let v = $mont_type($selectznz(s, v.as_inner(), $neg(&v).as_inner())); + $mul(&v, &$mont_type($divstep_precomp())) }}; }