diff --git a/Cargo.lock b/Cargo.lock index 3fd15af9..db2e6498 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -58,7 +58,7 @@ dependencies = [ "elliptic-curve", "hex", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "proptest", "rand_core", "rfc6979", @@ -125,7 +125,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "sha2", ] @@ -135,7 +135,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "sha2", ] @@ -742,7 +742,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "sec1", "serdect", ] @@ -755,7 +755,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "rand_core", "serdect", "sha2", @@ -770,7 +770,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "proptest", "rand_core", "serdect", @@ -786,7 +786,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "proptest", "rand_core", "serdect", @@ -799,11 +799,10 @@ version = "0.13.3" dependencies = [ "base16ct", "blobby", - "criterion", "ecdsa", "elliptic-curve", "hex-literal", - "primeorder 0.13.6", + "primeorder", "proptest", "rand_core", "serdect", @@ -877,16 +876,6 @@ dependencies = [ "serdect", ] -[[package]] -name = "primeorder" -version = "0.13.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "353e1ca18966c16d9deb1c69278edbc5f194139612772bd9537af60ac231e1e6" -dependencies = [ - "elliptic-curve", - "serdect", -] - [[package]] name = "proc-macro2" version = "1.0.51" @@ -1192,7 +1181,7 @@ version = "0.13.3" dependencies = [ "elliptic-curve", "hex-literal", - "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", + "primeorder", "proptest", "rand_core", "rfc6979", diff --git a/bign256/Cargo.toml b/bign256/Cargo.toml index 5ce5ad90..5d5b3a14 100644 --- a/bign256/Cargo.toml +++ b/bign256/Cargo.toml @@ -20,7 +20,7 @@ rust-version = "1.65" elliptic-curve = { version = "0.13.8", features = ["hazmat", "sec1"] } # optional dependencies -primeorder = { version = "0.13.5", optional = true } +primeorder = { version = "0.13.5", optional = true, path = "../primeorder" } signature = { version = "2", optional = true } belt-hash = { version = "0.1.0", optional = true, default-features = false } crypto-bigint = { version = "0.5.5", optional = true } diff --git a/bp256/Cargo.toml b/bp256/Cargo.toml index ee909ba4..8bfb5032 100644 --- a/bp256/Cargo.toml +++ b/bp256/Cargo.toml @@ -17,7 +17,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa = { version = "0.16", optional = true, default-features = false, features = ["der"] } -primeorder = { version = "0.13.5", optional = true } +primeorder = { version = "0.13.5", optional = true, path = "../primeorder" } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/bp384/Cargo.toml b/bp384/Cargo.toml index 94b8e96e..9e94519b 100644 --- a/bp384/Cargo.toml +++ b/bp384/Cargo.toml @@ -17,7 +17,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa = { version = "0.16", optional = true, default-features = false, features = ["der"] } -primeorder = { version = "0.13.5", optional = true } +primeorder = { version = "0.13.5", optional = true, path = "../primeorder" } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/p192/Cargo.toml b/p192/Cargo.toml index 2cf75144..1060f6b6 100644 --- a/p192/Cargo.toml +++ b/p192/Cargo.toml @@ -22,13 +22,13 @@ sec1 = { version = "0.7.3", default-features = false } # optional dependencies ecdsa-core = { version = "0.16.6", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.5", optional = true } +primeorder = { version = "0.13.5", optional = true, path = "../primeorder" } serdect = { version = "0.2", optional = true, default-features = false } [dev-dependencies] ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"] } +primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } [features] default = ["arithmetic", "ecdsa", "pem", "std"] diff --git a/p224/Cargo.toml b/p224/Cargo.toml index 8f7bca94..9762e5b0 100644 --- a/p224/Cargo.toml +++ b/p224/Cargo.toml @@ -21,7 +21,7 @@ elliptic-curve = { version = "0.13.8", default-features = false, features = ["ha # optional dependencies ecdsa-core = { version = "0.16.6", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.5", optional = true } +primeorder = { version = "0.13.5", optional = true, path = "../primeorder" } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -29,7 +29,7 @@ sha2 = { version = "0.10", optional = true, default-features = false } blobby = "0.3" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"] } +primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } rand_core = { version = "0.6", features = ["getrandom"] } [features] diff --git a/p256/Cargo.toml b/p256/Cargo.toml index 65c04f12..59b98444 100644 --- a/p256/Cargo.toml +++ b/p256/Cargo.toml @@ -22,7 +22,7 @@ elliptic-curve = { version = "0.13.8", default-features = false, features = ["ha # optional dependencies ecdsa-core = { version = "0.16", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13", optional = true } +primeorder = { version = "0.13", optional = true, path = "../primeorder" } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13.5", features = ["dev"] } +primeorder = { version = "0.13.5", features = ["dev"], path = "../primeorder" } proptest = "1" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p384/Cargo.toml b/p384/Cargo.toml index ed445926..a39ae32c 100644 --- a/p384/Cargo.toml +++ b/p384/Cargo.toml @@ -22,7 +22,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa-core = { version = "0.16", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.1", optional = true } +primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13.5", features = ["dev"] } +primeorder = { version = "0.13.5", features = ["dev"], path = "../primeorder" } proptest = "1.4" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p521/Cargo.toml b/p521/Cargo.toml index b6f19d98..8aee7bf3 100644 --- a/p521/Cargo.toml +++ b/p521/Cargo.toml @@ -34,7 +34,6 @@ hex-literal = "0.4" primeorder = { version = "0.13.3", 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"] @@ -45,7 +44,6 @@ arithmetic = ["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"] @@ -59,12 +57,3 @@ 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 deleted file mode 100644 index 19907e74..00000000 --- a/p521/benches/field.rs +++ /dev/null @@ -1,54 +0,0 @@ -//! 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 deleted file mode 100644 index 9979c6ec..00000000 --- a/p521/benches/scalar.rs +++ /dev/null @@ -1,73 +0,0 @@ -//! 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 31176c64..70382335 100644 --- a/p521/src/arithmetic/field.rs +++ b/p521/src/arithmetic/field.rs @@ -397,15 +397,13 @@ impl From for FieldElement { impl ConditionallySelectable for FieldElement { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO.0.into_inner(); - let a = a.0.as_inner(); - let b = b.0.as_inner(); + let mut ret = Self::ZERO; - for i in 0..ret.len() { - ret[i] = u64::conditional_select(&a[i], &b[i], choice); + for i in 0..ret.0.len() { + ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); } - Self(fiat_p521_tight_field_element(ret)) + ret } } diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index b72668d8..46e08f4c 100644 --- a/p521/src/arithmetic/field/p521_64.rs +++ b/p521/src/arithmetic/field/p521_64.rs @@ -1,17 +1,17 @@ -//! 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] +#![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]"] #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -23,181 +23,156 @@ 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; -/// 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] +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]"] #[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); - (x2, x3) + out1 = x2; + out2 = x3; + (out1, out2) } -/// 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] +#[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]"] #[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); - ( - x3, - (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), - ) + out1 = x3; + out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); + (out1, out2) } -/// 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] +#[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]"] #[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); - (x2, x3) + out1 = x2; + out2 = x3; + (out1, out2) } -/// 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] +#[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]"] #[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); - ( - x3, - (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), - ) + out1 = x3; + out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); + (out1, out2) } -/// 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] +#[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]"] #[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)); - (x3) + out1 = x3; + out1 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; 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)); @@ -321,18 +296,27 @@ pub const fn fiat_p521_carry_mul( let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1); let x122: u64 = (x120 & 0x3ffffffffffffff); let x123: u64 = ((x121 as u64) + x98); - (fiat_p521_tight_field_element([x119, x122, x123, x101, x104, x107, x110, x113, x116])) + 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 } -/// 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 -/// +#[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 = ""] #[inline] pub const fn fiat_p521_carry_square( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = (arg1[8]); let x2: u64 = (x1 * 0x2); let x3: u64 = ((arg1[8]) * 0x2); @@ -436,18 +420,27 @@ 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); - (fiat_p521_tight_field_element([x99, x102, x103, x81, x84, x87, x90, x93, x96])) + 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 } -/// The function fiat_p521_carry reduces a field element. -/// -/// Postconditions: -/// eval out1 mod m = eval arg1 mod m -/// +#[doc = " The function fiat_p521_carry reduces a field element."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " eval out1 mod m = eval arg1 mod m"] +#[doc = ""] #[inline] pub const fn fiat_p521_carry( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = (arg1[0]); let x2: u64 = ((x1 >> 58) + (arg1[1])); let x3: u64 = ((x2 >> 58) + (arg1[2])); @@ -468,20 +461,28 @@ pub const fn fiat_p521_carry( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) + 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 } -/// The function fiat_p521_add adds two field elements. -/// -/// Postconditions: -/// eval out1 mod m = (eval arg1 + eval arg2) mod m -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_loose_field_element = [0; 9]; let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((arg1[1]) + (arg2[1])); let x3: u64 = ((arg1[2]) + (arg2[2])); @@ -491,20 +492,28 @@ 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])); - (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) + 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 } -/// The function fiat_p521_sub subtracts two field elements. -/// -/// Postconditions: -/// eval out1 mod m = (eval arg1 - eval arg2) mod m -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_loose_field_element = [0; 9]; let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); let x2: u64 = ((0x7fffffffffffffe + (arg1[1])) - (arg2[1])); let x3: u64 = ((0x7fffffffffffffe + (arg1[2])) - (arg2[2])); @@ -514,16 +523,25 @@ 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])); - (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) + 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 } -/// The function fiat_p521_opp negates a field element. -/// -/// Postconditions: -/// eval out1 mod m = -eval arg1 mod m -/// +#[doc = " The function fiat_p521_opp negates a field element."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " eval out1 mod m = -eval arg1 mod m"] +#[doc = ""] #[inline] pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_loose_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_loose_field_element = [0; 9]; let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = (0x7fffffffffffffe - (arg1[1])); let x3: u64 = (0x7fffffffffffffe - (arg1[2])); @@ -533,20 +551,28 @@ 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])); - (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) + 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 } -/// The function fiat_p521_carry_add adds two field elements. -/// -/// Postconditions: -/// eval out1 mod m = (eval arg1 + eval arg2) mod m -/// +#[doc = " The function fiat_p521_carry_add adds two field elements."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"] +#[doc = ""] #[inline] pub const fn fiat_p521_carry_add( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((x1 >> 58) + ((arg1[1]) + (arg2[1]))); let x3: u64 = ((x2 >> 58) + ((arg1[2]) + (arg2[2]))); @@ -567,20 +593,28 @@ pub const fn fiat_p521_carry_add( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) + 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 } -/// The function fiat_p521_carry_sub subtracts two field elements. -/// -/// Postconditions: -/// eval out1 mod m = (eval arg1 - eval arg2) mod m -/// +#[doc = " The function fiat_p521_carry_sub subtracts two field elements."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] +#[doc = ""] #[inline] pub const fn fiat_p521_carry_sub( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); let x2: u64 = ((x1 >> 58) + ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]))); let x3: u64 = ((x2 >> 58) + ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]))); @@ -601,18 +635,27 @@ pub const fn fiat_p521_carry_sub( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) + 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 } -/// The function fiat_p521_carry_opp negates a field element. -/// -/// Postconditions: -/// eval out1 mod m = -eval arg1 mod m -/// +#[doc = " The function fiat_p521_carry_opp negates a field element."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " eval out1 mod m = -eval arg1 mod m"] +#[doc = ""] #[inline] pub const fn fiat_p521_carry_opp( arg1: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = ((((x1 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[1]))); let x3: u64 = ((((x2 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[2]))); @@ -633,18 +676,27 @@ pub const fn fiat_p521_carry_opp( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) + 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 } -/// The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements. -/// -/// Postconditions: -/// out1 = arg1 -/// +#[doc = " The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements."] +#[doc = ""] +#[doc = " Postconditions:"] +#[doc = " out1 = arg1"] +#[doc = ""] #[inline] pub const fn fiat_p521_relax( arg1: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_loose_field_element = [0; 9]; let x1: u64 = (arg1[0]); let x2: u64 = (arg1[1]); let x3: u64 = (arg1[2]); @@ -654,21 +706,31 @@ pub const fn fiat_p521_relax( let x7: u64 = (arg1[6]); let x8: u64 = (arg1[7]); let x9: u64 = (arg1[8]); - (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) + 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 } -/// 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]] +#[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]]"] #[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; @@ -687,18 +749,27 @@ 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])); - ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) + 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 } -/// 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]] +#[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]]"] #[inline] pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66] { - let arg1 = arg1.as_inner(); + let mut out1: [u8; 66] = [0; 66]; let mut x1: u64 = 0; let mut x2: fiat_p521_u1 = 0; let (x1, x2) = fiat_p521_subborrowx_u58(0x0, (arg1[0]), 0x3ffffffffffffff); @@ -893,84 +964,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); - ([ - 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), - ]) + 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 } -/// 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]] +#[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]]"] #[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); @@ -1112,25 +1183,14 @@ 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); - (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 - } + 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 } diff --git a/p521/src/arithmetic/scalar.rs b/p521/src/arithmetic/scalar.rs index c161364b..66de4997 100644 --- a/p521/src/arithmetic/scalar.rs +++ b/p521/src/arithmetic/scalar.rs @@ -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( - &fiat_p521_scalar_non_montgomery_domain_field_element(u32x18_to_u64x9(w.as_words())), - )) + Self(fiat_p521_scalar_to_montgomery(&u32x18_to_u64x9( + w.as_words(), + ))) } /// Decode [`Scalar`] from [`U576`] converting it into Montgomery form. @@ -142,9 +142,7 @@ 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( - &fiat_p521_scalar_non_montgomery_domain_field_element(*w.as_words()), - )) + Self(fiat_p521_scalar_to_montgomery(w.as_words())) } /// Returns the big-endian encoding of this [`Scalar`]. @@ -157,9 +155,7 @@ 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).as_inner(), - )) + U576::from_words(u64x9_to_u32x18(&fiat_p521_scalar_from_montgomery(&self.0))) } /// Translate [`Scalar`] out of the Montgomery domain, returning a [`U576`] @@ -167,7 +163,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).into_inner()) + U576::from_words(fiat_p521_scalar_from_montgomery(&self.0)) } /// Determine if this [`Scalar`] is odd in the SEC1 sense: `self mod 2 == 1`. @@ -238,7 +234,6 @@ 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, @@ -293,12 +288,10 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "32")] pub const fn shr_vartime(&self, shift: usize) -> Scalar { - Self(fiat_p521_scalar_montgomery_domain_field_element( - u32x18_to_u64x9( - &U576::from_words(u64x9_to_u32x18(self.0.as_inner())) - .shr_vartime(shift) - .to_words(), - ), + Self(u32x18_to_u64x9( + &U576::from_words(u64x9_to_u32x18(&self.0)) + .shr_vartime(shift) + .to_words(), )) } @@ -307,11 +300,7 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "64")] pub const fn shr_vartime(&self, shift: usize) -> Scalar { - Self(fiat_p521_scalar_montgomery_domain_field_element( - U576::from_words(self.0.into_inner()) - .shr_vartime(shift) - .to_words(), - )) + Self(U576::from_words(self.0).shr_vartime(shift).to_words()) } } @@ -330,7 +319,7 @@ impl Default for Scalar { impl Eq for Scalar {} impl PartialEq for Scalar { fn eq(&self, rhs: &Self) -> bool { - self.0.as_inner().ct_eq(rhs.0.as_inner()).into() + self.0.ct_eq(&(rhs.0)).into() } } @@ -354,21 +343,19 @@ impl From for Scalar { impl ConditionallySelectable for Scalar { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO.0.into_inner(); - let a = a.0.as_inner(); - let b = b.0.as_inner(); + let mut ret = Self::ZERO; - for i in 0..ret.len() { - ret[i] = u64::conditional_select(&a[i], &b[i], choice); + for i in 0..ret.0.len() { + ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); } - Self(fiat_p521_scalar_montgomery_domain_field_element(ret)) + ret } } impl ConstantTimeEq for Scalar { fn ct_eq(&self, other: &Self) -> Choice { - self.0.as_inner().ct_eq(other.0.as_inner()) + self.0.ct_eq(&other.0) } } diff --git a/p521/src/arithmetic/scalar/p521_scalar_64.rs b/p521/src/arithmetic/scalar/p521_scalar_64.rs index 6b47cc92..60c8646f 100644 --- a/p521/src/arithmetic/scalar/p521_scalar_64.rs +++ b/p521/src/arithmetic/scalar/p521_scalar_64.rs @@ -1,22 +1,22 @@ -//! 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 +#![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"] #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -28,154 +28,128 @@ 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; -/// 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] +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]"] #[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); - (x2, x3) + out1 = x2; + out2 = x3; + (out1, out2) } -/// 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] +#[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]"] #[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); - ( - x3, - (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1), - ) + out1 = x3; + out2 = (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1); + (out1, out2) } -/// 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] +#[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]"] #[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); - (x2, x3) + out1 = x2; + out2 = x3; + (out1, out2) } -/// 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] +#[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]"] #[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)); - (x3) + out1 = x3; + out1 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -1714,23 +1688,30 @@ 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); - (fiat_p521_scalar_montgomery_domain_field_element([ - x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[inline] pub const fn fiat_p521_scalar_square( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -3269,26 +3250,32 @@ 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); - (fiat_p521_scalar_montgomery_domain_field_element([ - x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [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[0]), (arg2[0])); @@ -3364,26 +3351,32 @@ 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); - (fiat_p521_scalar_montgomery_domain_field_element([ - x39, x40, x41, x42, x43, x44, x45, x46, x47, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); - let arg2 = arg2.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; 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])); @@ -3440,23 +3433,30 @@ 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)); - (fiat_p521_scalar_montgomery_domain_field_element([ - x20, x22, x24, x26, x28, x30, x32, x34, x36, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[inline] pub const fn fiat_p521_scalar_opp( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let arg1 = arg1.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; 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,23 +3513,30 @@ 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)); - (fiat_p521_scalar_montgomery_domain_field_element([ - x20, x22, x24, x26, x28, x30, x32, x34, x36, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); + let mut out1: fiat_p521_scalar_non_montgomery_domain_field_element = [0; 9]; let x1: u64 = (arg1[0]); let mut x2: u64 = 0; let mut x3: u64 = 0; @@ -4533,23 +4540,30 @@ 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); - (fiat_p521_scalar_non_montgomery_domain_field_element([ - x637, x638, x639, x640, x641, x642, x643, x644, x645, - ])) + 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 } -/// 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 -/// +#[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 = ""] #[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 arg1 = arg1.as_inner(); + let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -6045,47 +6059,57 @@ 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); - (fiat_p521_scalar_montgomery_domain_field_element([ - x967, x968, x969, x970, x971, x972, x973, x974, x975, - ])) + 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 } -/// 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] +#[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]"] #[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]))))))))); - (x1) + out1 = x1; + out1 } -/// 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]] +#[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]]"] #[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; @@ -6104,21 +6128,31 @@ 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])); - ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) + 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 } -/// 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]] +#[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]]"] #[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]); @@ -6242,89 +6276,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); - ([ - 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), - ]) + 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 } -/// 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]] +#[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]]"] #[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); @@ -6448,101 +6482,110 @@ 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)); - ([x73, x80, x87, x94, x101, x108, x115, x122, x123]) + 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 } -/// 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 -/// +#[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 = ""] #[inline] pub const fn fiat_p521_scalar_set_one() -> fiat_p521_scalar_montgomery_domain_field_element { - (fiat_p521_scalar_montgomery_domain_field_element([ - 0xfb80000000000000, - 0x28a2482470b763cd, - 0x17e2251b23bb31dc, - 0xca4019ff5b847b2d, - 0x2d73cbc3e206834, - (0x0 as u64), - (0x0 as u64), - (0x0 as u64), - (0x0 as u64), - ])) + 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 } -/// 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]] +#[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]]"] #[inline] pub const fn fiat_p521_scalar_msat() -> [u64; 10] { - ([ - 0xbb6fb71e91386409, - 0x3bb5c9b8899c47ae, - 0x7fcc0148f709a5d0, - 0x51868783bf2f966b, - 0xfffffffffffffffa, - 0xffffffffffffffff, - 0xffffffffffffffff, - 0xffffffffffffffff, - 0x1ff, - (0x0 as u64), - ]) + 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 } -/// 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]] +#[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]]"] #[inline] pub const fn fiat_p521_scalar_divstep_precomp() -> [u64; 9] { - ([ - 0x7b27a0cb33d1884b, - 0x9ef6cb011f2467d8, - 0x5fbc88e1d6e7fce, - 0xb08222d0fe97e1dc, - 0x1624870c44df3fce, - 0xb7f07b8eedbce602, - 0x62da93cf721f63bc, - 0xafd209c16c4f0d20, - 0x1c7, - ]) + 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 } -/// 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]] +#[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]]"] #[inline] pub const fn fiat_p521_scalar_divstep( arg1: u64, @@ -6551,6 +6594,11 @@ 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)); @@ -6964,31 +7012,44 @@ 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); - ( - 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 - } + 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) } diff --git a/p521/src/lib.rs b/p521/src/lib.rs index ecacd617..e0056a01 100644 --- a/p521/src/lib.rs +++ b/p521/src/lib.rs @@ -40,9 +40,6 @@ 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/primeorder/src/field.rs b/primeorder/src/field.rs index 8ef8880b..9a3b6ead 100644 --- a/primeorder/src/field.rs +++ b/primeorder/src/field.rs @@ -510,7 +510,6 @@ macro_rules! impl_bernstein_yang_invert { $d:expr, $nlimbs:expr, $word:ty, - $mont_type: expr, $from_mont:ident, $mul:ident, $neg:ident, @@ -526,36 +525,36 @@ macro_rules! impl_bernstein_yang_invert { 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 v = [0; $nlimbs]; + let mut r = $one; let mut i = 0; let mut j = 0; while j < $nlimbs { - g[j] = a.as_inner()[j]; + g[j] = a[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(d, &f, &g, &v, &r); let (out1, out2, out3, out4, out5) = $divstep(out1, &out2, &out3, &out4, &out5); d = out1; f = out2; g = out3; - v = $mont_type(out4); + v = 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); + let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, &v, &r); + v = 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())) + let v = $selectznz(s, &v, &$neg(&v)); + $mul(&v, &$divstep_precomp()) }}; } diff --git a/sm2/Cargo.toml b/sm2/Cargo.toml index 8e58be1f..2847f36c 100644 --- a/sm2/Cargo.toml +++ b/sm2/Cargo.toml @@ -20,7 +20,7 @@ rust-version = "1.65" elliptic-curve = { version = "0.13", default-features = false, features = ["hazmat", "sec1"] } # optional dependencies -primeorder = { version = "0.13.1", optional = true } +primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } rfc6979 = { version = "0.4", optional = true } serdect = { version = "0.2", optional = true, default-features = false } signature = { version = "2.2", optional = true, features = ["rand_core"] }