From 71a9bce14256709227a1823f04bf21dbf866e346 Mon Sep 17 00:00:00 2001 From: Arvind Mukund Date: Wed, 10 Jan 2024 02:33:24 +0530 Subject: [PATCH] p521: fiat-constify update (#1003) Implementation for the fiat-constify update @ RustCrypto/utils#992 --- .github/workflows/p521.yml | 12 + Cargo.lock | 29 +- bign256/Cargo.toml | 2 +- bp256/Cargo.toml | 2 +- bp384/Cargo.toml | 2 +- p192/Cargo.toml | 4 +- p224/Cargo.toml | 4 +- p256/Cargo.toml | 4 +- p384/Cargo.toml | 4 +- p521/Cargo.toml | 11 + p521/benches/field.rs | 54 ++ p521/benches/scalar.rs | 73 ++ p521/src/arithmetic/field.rs | 10 +- p521/src/arithmetic/field/p521_64.rs | 694 +++++++------- p521/src/arithmetic/scalar.rs | 47 +- p521/src/arithmetic/scalar/p521_scalar_64.rs | 921 +++++++++---------- p521/src/lib.rs | 3 + primeorder/src/field.rs | 19 +- sm2/Cargo.toml | 2 +- 19 files changed, 978 insertions(+), 919 deletions(-) create mode 100644 p521/benches/field.rs create mode 100644 p521/benches/scalar.rs diff --git a/.github/workflows/p521.yml b/.github/workflows/p521.yml index fc9d5359..90246eb3 100644 --- a/.github/workflows/p521.yml +++ b/.github/workflows/p521.yml @@ -38,6 +38,18 @@ jobs: - run: cargo build --target ${{ matrix.target }} --release --no-default-features - run: cargo build --target ${{ matrix.target }} --release --no-default-features --features alloc + benches: + runs-on: ubuntu-latest + strategy: + matrix: + rust: stable + steps: + - uses: actions/checkout@v4 + - uses: dtolnay/rust-toolchain@master + with: + toolchain: ${{ matrix.rust }} + - run: cargo build --all-features --benches + test: runs-on: ubuntu-latest strategy: diff --git a/Cargo.lock b/Cargo.lock index db2e6498..3fd15af9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -58,7 +58,7 @@ dependencies = [ "elliptic-curve", "hex", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "rfc6979", @@ -125,7 +125,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "sha2", ] @@ -135,7 +135,7 @@ version = "0.6.1" dependencies = [ "ecdsa", "elliptic-curve", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "sha2", ] @@ -742,7 +742,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "sec1", "serdect", ] @@ -755,7 +755,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "rand_core", "serdect", "sha2", @@ -770,7 +770,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "serdect", @@ -786,7 +786,7 @@ dependencies = [ "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "serdect", @@ -799,10 +799,11 @@ version = "0.13.3" dependencies = [ "base16ct", "blobby", + "criterion", "ecdsa", "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6", "proptest", "rand_core", "serdect", @@ -876,6 +877,16 @@ 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" @@ -1181,7 +1192,7 @@ version = "0.13.3" dependencies = [ "elliptic-curve", "hex-literal", - "primeorder", + "primeorder 0.13.6 (registry+https://github.com/rust-lang/crates.io-index)", "proptest", "rand_core", "rfc6979", diff --git a/bign256/Cargo.toml b/bign256/Cargo.toml index 5d5b3a14..5ce5ad90 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, path = "../primeorder" } +primeorder = { version = "0.13.5", optional = true } 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 8bfb5032..ee909ba4 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, path = "../primeorder" } +primeorder = { version = "0.13.5", optional = true } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/bp384/Cargo.toml b/bp384/Cargo.toml index 9e94519b..94b8e96e 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, path = "../primeorder" } +primeorder = { version = "0.13.5", optional = true } sha2 = { version = "0.10", optional = true, default-features = false } [features] diff --git a/p192/Cargo.toml b/p192/Cargo.toml index 1060f6b6..2cf75144 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, path = "../primeorder" } +primeorder = { version = "0.13.5", optional = true } serdect = { version = "0.2", optional = true, default-features = false } [dev-dependencies] ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13", features = ["dev"] } [features] default = ["arithmetic", "ecdsa", "pem", "std"] diff --git a/p224/Cargo.toml b/p224/Cargo.toml index 9762e5b0..8f7bca94 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, path = "../primeorder" } +primeorder = { version = "0.13.5", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -29,7 +29,7 @@ sha2 = { version = "0.10", optional = true, default-features = false } blobby = "0.3" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13", features = ["dev"] } rand_core = { version = "0.6", features = ["getrandom"] } [features] diff --git a/p256/Cargo.toml b/p256/Cargo.toml index 59b98444..65c04f12 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, path = "../primeorder" } +primeorder = { version = "0.13", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13.5", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.5", features = ["dev"] } proptest = "1" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p384/Cargo.toml b/p384/Cargo.toml index a39ae32c..ed445926 100644 --- a/p384/Cargo.toml +++ b/p384/Cargo.toml @@ -22,7 +22,7 @@ elliptic-curve = { version = "0.13", default-features = false, features = ["hazm # optional dependencies ecdsa-core = { version = "0.16", package = "ecdsa", optional = true, default-features = false, features = ["der"] } hex-literal = { version = "0.4", optional = true } -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.1", optional = true } serdect = { version = "0.2", optional = true, default-features = false } sha2 = { version = "0.10", optional = true, default-features = false } @@ -31,7 +31,7 @@ blobby = "0.3" criterion = "0.5" ecdsa-core = { version = "0.16", package = "ecdsa", default-features = false, features = ["dev"] } hex-literal = "0.4" -primeorder = { version = "0.13.5", features = ["dev"], path = "../primeorder" } +primeorder = { version = "0.13.5", features = ["dev"] } proptest = "1.4" rand_core = { version = "0.6", features = ["getrandom"] } diff --git a/p521/Cargo.toml b/p521/Cargo.toml index 8aee7bf3..b6f19d98 100644 --- a/p521/Cargo.toml +++ b/p521/Cargo.toml @@ -34,6 +34,7 @@ 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"] @@ -44,6 +45,7 @@ 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"] @@ -57,3 +59,12 @@ voprf = ["elliptic-curve/voprf", "dep:sha2"] [package.metadata.docs.rs] all-features = true rustdoc-args = ["--cfg", "docsrs"] + +[[bench]] +name = "field" +harness = false +required-features = ["expose-field"] + +[[bench]] +name = "scalar" +harness = false diff --git a/p521/benches/field.rs b/p521/benches/field.rs new file mode 100644 index 00000000..19907e74 --- /dev/null +++ b/p521/benches/field.rs @@ -0,0 +1,54 @@ +//! secp521r1 field element benchmarks + +use criterion::{ + black_box, criterion_group, criterion_main, measurement::Measurement, BenchmarkGroup, Criterion, +}; +use hex_literal::hex; +use p521::{FieldBytes, FieldElement}; + +fn test_field_element_x() -> FieldElement { + black_box(FieldElement::from_bytes( + &FieldBytes::clone_from_slice(&hex!("01a7596d38aac7868327ddc1ef5e8178cf052b7ebc512828e8a45955d85bef49494d15278198bbcc5454358c12a2af9a3874e7002e1a2f02fcb36ff3e3b4bc0c69e7")) + ) + .unwrap()) +} + +fn test_field_element_y() -> FieldElement { + black_box(FieldElement::from_bytes( + &FieldBytes::clone_from_slice(&hex!("0184902e515982bb225b8c84f245e61b327c08e94d41c07d0b4101a963e02fe52f6a9f33e8b1de2394e0cb74c40790b4e489b5500e6804cabed0fe8c192443d4027b")) + ) + .unwrap()) +} + +fn bench_field_element_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + let y = test_field_element_y(); + group.bench_function("mul", |b| b.iter(|| &x * &y)); +} + +fn bench_field_element_square<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("square", |b| b.iter(|| x.square())); +} + +fn bench_field_element_sqrt<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("sqrt", |b| b.iter(|| x.sqrt())); +} + +fn bench_field_element_invert<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_field_element_x(); + group.bench_function("invert", |b| b.iter(|| x.invert())); +} + +fn bench_field_element(c: &mut Criterion) { + let mut group = c.benchmark_group("field element operations"); + bench_field_element_mul(&mut group); + bench_field_element_square(&mut group); + bench_field_element_invert(&mut group); + bench_field_element_sqrt(&mut group); + group.finish(); +} + +criterion_group!(benches, bench_field_element); +criterion_main!(benches); diff --git a/p521/benches/scalar.rs b/p521/benches/scalar.rs new file mode 100644 index 00000000..9979c6ec --- /dev/null +++ b/p521/benches/scalar.rs @@ -0,0 +1,73 @@ +//! secp521r1 scalar arithmetic benchmarks + +use criterion::{ + black_box, criterion_group, criterion_main, measurement::Measurement, BenchmarkGroup, Criterion, +}; +use hex_literal::hex; +use p521::{elliptic_curve::group::ff::PrimeField, FieldBytes, ProjectivePoint, Scalar}; + +fn test_scalar_x() -> Scalar { + black_box(Scalar::from_repr( + FieldBytes::clone_from_slice(&hex!("01d7bb864c5b5ecae019296cf9b5c63a166f5f1113942819b1933d889a96d12245777a99428f93de4fc9a18d709bf91889d7f8dddd522b4c364aeae13c983e9fae46")) + ).unwrap()) +} + +fn test_scalar_y() -> Scalar { + black_box(Scalar::from_repr( + FieldBytes::clone_from_slice(&hex!("017e49b8ea8f9d1b7c0378e378a7a42e68e12cf78779ed41dcd29a090ae7e0f883b0d0f2cbc8f0473c0ad6732bea40d371a7f363bc6537d075bd1a4c23e558b0bc73")) + ).unwrap()) +} + +fn bench_point_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let p = ProjectivePoint::GENERATOR; + let m = test_scalar_x(); + let s = Scalar::from_repr(m.into()).unwrap(); + group.bench_function("point-scalar mul", |b| b.iter(|| &p * &s)); +} + +fn bench_scalar_sub<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("sub", |b| b.iter(|| &x - &y)); +} + +fn bench_scalar_add<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("add", |b| b.iter(|| &x + &y)); +} + +fn bench_scalar_mul<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + let y = test_scalar_y(); + group.bench_function("mul", |b| b.iter(|| &x * &y)); +} + +fn bench_scalar_negate<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + group.bench_function("negate", |b| b.iter(|| -x)); +} + +fn bench_scalar_invert<'a, M: Measurement>(group: &mut BenchmarkGroup<'a, M>) { + let x = test_scalar_x(); + group.bench_function("invert", |b| b.iter(|| x.invert())); +} + +fn bench_point(c: &mut Criterion) { + let mut group = c.benchmark_group("point operations"); + bench_point_mul(&mut group); + group.finish(); +} + +fn bench_scalar(c: &mut Criterion) { + let mut group = c.benchmark_group("scalar operations"); + bench_scalar_sub(&mut group); + bench_scalar_add(&mut group); + bench_scalar_mul(&mut group); + bench_scalar_negate(&mut group); + bench_scalar_invert(&mut group); + group.finish(); +} + +criterion_group!(benches, bench_point, bench_scalar); +criterion_main!(benches); diff --git a/p521/src/arithmetic/field.rs b/p521/src/arithmetic/field.rs index 70382335..31176c64 100644 --- a/p521/src/arithmetic/field.rs +++ b/p521/src/arithmetic/field.rs @@ -397,13 +397,15 @@ impl From for FieldElement { impl ConditionallySelectable for FieldElement { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO; + let mut ret = Self::ZERO.0.into_inner(); + let a = a.0.as_inner(); + let b = b.0.as_inner(); - for i in 0..ret.0.len() { - ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); + for i in 0..ret.len() { + ret[i] = u64::conditional_select(&a[i], &b[i], choice); } - ret + Self(fiat_p521_tight_field_element(ret)) } } diff --git a/p521/src/arithmetic/field/p521_64.rs b/p521/src/arithmetic/field/p521_64.rs index 46e08f4c..b72668d8 100644 --- a/p521/src/arithmetic/field/p521_64.rs +++ b/p521/src/arithmetic/field/p521_64.rs @@ -1,17 +1,17 @@ -#![doc = " fiat-crypto output postprocessed by fiat-constify: "] -#![doc = " Autogenerated: './unsaturated_solinas' --lang Rust --inline p521 64 9 '2^521 - 1'"] -#![doc = " curve description: p521"] -#![doc = " machine_wordsize = 64 (from \"64\")"] -#![doc = " requested operations: (all)"] -#![doc = " n = 9 (from \"9\")"] -#![doc = " s-c = 2^521 - [(1, 1)] (from \"2^521 - 1\")"] -#![doc = " tight_bounds_multiplier = 1 (from \"\")"] -#![doc = ""] -#![doc = " Computed values:"] -#![doc = " carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]"] -#![doc = " eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0)"] -#![doc = " bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)"] -#![doc = " balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe]"] +//! fiat-crypto output postprocessed by fiat-constify: +//! Autogenerated: './fiat-crypto' unsaturated-solinas --lang Rust --inline p521 64 9 '2^521 - 1' +//! curve description: p521 +//! machine_wordsize = 64 (from "64") +//! requested operations: (all) +//! n = 9 (from "9") +//! s-c = 2^521 - [(1, 1)] (from "2^521 - 1") +//! tight_bounds_multiplier = 1 (from "") +//! +//! Computed values: +//! carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] +//! eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0) +//! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) +//! balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe] #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -23,156 +23,181 @@ unused_mut, unused_variables )] +/// fiat_p521_u1 represents values of 1 bits, stored in one byte. pub type fiat_p521_u1 = u8; +/// fiat_p521_i1 represents values of 1 bits, stored in one byte. pub type fiat_p521_i1 = i8; +/// fiat_p521_u2 represents values of 2 bits, stored in one byte. pub type fiat_p521_u2 = u8; +/// fiat_p521_i2 represents values of 2 bits, stored in one byte. pub type fiat_p521_i2 = i8; -pub type fiat_p521_loose_field_element = [u64; 9]; -pub type fiat_p521_tight_field_element = [u64; 9]; -#[doc = " The function fiat_p521_addcarryx_u58 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^58"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The type fiat_p521_loose_field_element is a field element with loose bounds. +/// Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub struct fiat_p521_loose_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_loose_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_loose_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The type fiat_p521_tight_field_element is a field element with tight bounds. +/// Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub struct fiat_p521_tight_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_tight_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_tight_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The function fiat_p521_addcarryx_u58 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^58 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x3ffffffffffffff] +/// arg3: [0x0 ~> 0x3ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x3ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_addcarryx_u58( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: u64 = (((arg1 as u64) + arg2) + arg3); let x2: u64 = (x1 & 0x3ffffffffffffff); let x3: fiat_p521_u1 = ((x1 >> 58) as fiat_p521_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_subborrowx_u58 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^58"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_subborrowx_u58 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^58 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x3ffffffffffffff] +/// arg3: [0x0 ~> 0x3ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x3ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_subborrowx_u58( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 58) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x3ffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), + ) } -#[doc = " The function fiat_p521_addcarryx_u57 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^57"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_addcarryx_u57 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^57 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x1ffffffffffffff] +/// arg3: [0x0 ~> 0x1ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x1ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_addcarryx_u57( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: u64 = (((arg1 as u64) + arg2) + arg3); let x2: u64 = (x1 & 0x1ffffffffffffff); let x3: fiat_p521_u1 = ((x1 >> 57) as fiat_p521_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_subborrowx_u57 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^57"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_subborrowx_u57 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^57 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0x1ffffffffffffff] +/// arg3: [0x0 ~> 0x1ffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0x1ffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_subborrowx_u57( arg1: fiat_p521_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_u1 = 0; let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64); let x2: fiat_p521_i1 = ((x1 >> 57) as fiat_p521_i1); let x3: u64 = (((x1 as i128) & (0x1ffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1), + ) } -#[doc = " The function fiat_p521_cmovznz_u64 is a single-word conditional move."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_cmovznz_u64 is a single-word conditional move. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_cmovznz_u64(arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> u64 { - let mut out1: u64 = 0; let x1: fiat_p521_u1 = (!(!arg1)); let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) as i128) & (0xffffffffffffffff as i128)) as u64); let x3: u64 = ((x2 & arg3) | ((!x2) & arg2)); - out1 = x3; - out1 + (x3) } -#[doc = " The function fiat_p521_carry_mul multiplies two field elements and reduces the result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_mul multiplies two field elements and reduces the result. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 * eval arg2) mod m +/// #[inline] pub const fn fiat_p521_carry_mul( arg1: &fiat_p521_loose_field_element, arg2: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u128 = (((arg1[8]) as u128) * (((arg2[8]) * 0x2) as u128)); let x2: u128 = (((arg1[8]) as u128) * (((arg2[7]) * 0x2) as u128)); let x3: u128 = (((arg1[8]) as u128) * (((arg2[6]) * 0x2) as u128)); @@ -296,27 +321,18 @@ pub const fn fiat_p521_carry_mul( let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1); let x122: u64 = (x120 & 0x3ffffffffffffff); let x123: u64 = ((x121 as u64) + x98); - out1[0] = x119; - out1[1] = x122; - out1[2] = x123; - out1[3] = x101; - out1[4] = x104; - out1[5] = x107; - out1[6] = x110; - out1[7] = x113; - out1[8] = x116; - out1 + (fiat_p521_tight_field_element([x119, x122, x123, x101, x104, x107, x110, x113, x116])) } -#[doc = " The function fiat_p521_carry_square squares a field element and reduces the result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * eval arg1) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_square squares a field element and reduces the result. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 * eval arg1) mod m +/// #[inline] pub const fn fiat_p521_carry_square( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[8]); let x2: u64 = (x1 * 0x2); let x3: u64 = ((arg1[8]) * 0x2); @@ -420,27 +436,18 @@ pub const fn fiat_p521_carry_square( let x101: fiat_p521_u1 = ((x100 >> 58) as fiat_p521_u1); let x102: u64 = (x100 & 0x3ffffffffffffff); let x103: u64 = ((x101 as u64) + x78); - out1[0] = x99; - out1[1] = x102; - out1[2] = x103; - out1[3] = x81; - out1[4] = x84; - out1[5] = x87; - out1[6] = x90; - out1[7] = x93; - out1[8] = x96; - out1 + (fiat_p521_tight_field_element([x99, x102, x103, x81, x84, x87, x90, x93, x96])) } -#[doc = " The function fiat_p521_carry reduces a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = eval arg1 mod m"] -#[doc = ""] +/// The function fiat_p521_carry reduces a field element. +/// +/// Postconditions: +/// eval out1 mod m = eval arg1 mod m +/// #[inline] pub const fn fiat_p521_carry( arg1: &fiat_p521_loose_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[0]); let x2: u64 = ((x1 >> 58) + (arg1[1])); let x3: u64 = ((x2 >> 58) + (arg1[2])); @@ -461,28 +468,20 @@ pub const fn fiat_p521_carry( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) } -#[doc = " The function fiat_p521_add adds two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_add adds two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 + eval arg2) mod m +/// #[inline] pub const fn fiat_p521_add( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((arg1[1]) + (arg2[1])); let x3: u64 = ((arg1[2]) + (arg2[2])); @@ -492,28 +491,20 @@ pub const fn fiat_p521_add( let x7: u64 = ((arg1[6]) + (arg2[6])); let x8: u64 = ((arg1[7]) + (arg2[7])); let x9: u64 = ((arg1[8]) + (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_sub subtracts two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_sub subtracts two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 - eval arg2) mod m +/// #[inline] pub const fn fiat_p521_sub( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); let x2: u64 = ((0x7fffffffffffffe + (arg1[1])) - (arg2[1])); let x3: u64 = ((0x7fffffffffffffe + (arg1[2])) - (arg2[2])); @@ -523,25 +514,16 @@ pub const fn fiat_p521_sub( let x7: u64 = ((0x7fffffffffffffe + (arg1[6])) - (arg2[6])); let x8: u64 = ((0x7fffffffffffffe + (arg1[7])) - (arg2[7])); let x9: u64 = ((0x3fffffffffffffe + (arg1[8])) - (arg2[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_opp negates a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = -eval arg1 mod m"] -#[doc = ""] +/// The function fiat_p521_opp negates a field element. +/// +/// Postconditions: +/// eval out1 mod m = -eval arg1 mod m +/// #[inline] pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = (0x7fffffffffffffe - (arg1[1])); let x3: u64 = (0x7fffffffffffffe - (arg1[2])); @@ -551,28 +533,20 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo let x7: u64 = (0x7fffffffffffffe - (arg1[6])); let x8: u64 = (0x7fffffffffffffe - (arg1[7])); let x9: u64 = (0x3fffffffffffffe - (arg1[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_carry_add adds two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_add adds two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 + eval arg2) mod m +/// #[inline] pub const fn fiat_p521_carry_add( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = ((arg1[0]) + (arg2[0])); let x2: u64 = ((x1 >> 58) + ((arg1[1]) + (arg2[1]))); let x3: u64 = ((x2 >> 58) + ((arg1[2]) + (arg2[2]))); @@ -593,28 +567,20 @@ pub const fn fiat_p521_carry_add( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) } -#[doc = " The function fiat_p521_carry_sub subtracts two field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"] -#[doc = ""] +/// The function fiat_p521_carry_sub subtracts two field elements. +/// +/// Postconditions: +/// eval out1 mod m = (eval arg1 - eval arg2) mod m +/// #[inline] pub const fn fiat_p521_carry_sub( arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0])); let x2: u64 = ((x1 >> 58) + ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]))); let x3: u64 = ((x2 >> 58) + ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]))); @@ -635,27 +601,18 @@ pub const fn fiat_p521_carry_sub( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) } -#[doc = " The function fiat_p521_carry_opp negates a field element."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = -eval arg1 mod m"] -#[doc = ""] +/// The function fiat_p521_carry_opp negates a field element. +/// +/// Postconditions: +/// eval out1 mod m = -eval arg1 mod m +/// #[inline] pub const fn fiat_p521_carry_opp( arg1: &fiat_p521_tight_field_element, ) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (0x7fffffffffffffe - (arg1[0])); let x2: u64 = ((((x1 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[1]))); let x3: u64 = ((((x2 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[2]))); @@ -676,27 +633,18 @@ pub const fn fiat_p521_carry_opp( let x18: u64 = (x7 & 0x3ffffffffffffff); let x19: u64 = (x8 & 0x3ffffffffffffff); let x20: u64 = (x9 & 0x1ffffffffffffff); - out1[0] = x12; - out1[1] = x13; - out1[2] = x14; - out1[3] = x15; - out1[4] = x16; - out1[5] = x17; - out1[6] = x18; - out1[7] = x19; - out1[8] = x20; - out1 + (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20])) } -#[doc = " The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = arg1"] -#[doc = ""] +/// The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements. +/// +/// Postconditions: +/// out1 = arg1 +/// #[inline] pub const fn fiat_p521_relax( arg1: &fiat_p521_tight_field_element, ) -> fiat_p521_loose_field_element { - let mut out1: fiat_p521_loose_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[0]); let x2: u64 = (arg1[1]); let x3: u64 = (arg1[2]); @@ -706,31 +654,21 @@ pub const fn fiat_p521_relax( let x7: u64 = (arg1[6]); let x8: u64 = (arg1[7]); let x9: u64 = (arg1[8]); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9])) } -#[doc = " The function fiat_p521_selectznz is a multi-limb conditional select."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_selectznz is a multi-limb conditional select. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let (x1) = fiat_p521_cmovznz_u64(arg1, (arg2[0]), (arg3[0])); let mut x2: u64 = 0; @@ -749,27 +687,18 @@ pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u6 let (x8) = fiat_p521_cmovznz_u64(arg1, (arg2[7]), (arg3[7])); let mut x9: u64 = 0; let (x9) = fiat_p521_cmovznz_u64(arg1, (arg2[8]), (arg3[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) } -#[doc = " The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order. +/// +/// Postconditions: +/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66] { - let mut out1: [u8; 66] = [0; 66]; + let arg1 = arg1.as_inner(); let mut x1: u64 = 0; let mut x2: fiat_p521_u1 = 0; let (x1, x2) = fiat_p521_subborrowx_u58(0x0, (arg1[0]), 0x3ffffffffffffff); @@ -964,84 +893,84 @@ pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66 let x173: u64 = (x171 >> 8); let x174: u8 = ((x173 & (0xff as u64)) as u8); let x175: fiat_p521_u1 = ((x173 >> 8) as fiat_p521_u1); - out1[0] = x44; - out1[1] = x46; - out1[2] = x48; - out1[3] = x50; - out1[4] = x52; - out1[5] = x54; - out1[6] = x56; - out1[7] = x59; - out1[8] = x61; - out1[9] = x63; - out1[10] = x65; - out1[11] = x67; - out1[12] = x69; - out1[13] = x71; - out1[14] = x74; - out1[15] = x76; - out1[16] = x78; - out1[17] = x80; - out1[18] = x82; - out1[19] = x84; - out1[20] = x86; - out1[21] = x89; - out1[22] = x91; - out1[23] = x93; - out1[24] = x95; - out1[25] = x97; - out1[26] = x99; - out1[27] = x101; - out1[28] = x102; - out1[29] = x103; - out1[30] = x105; - out1[31] = x107; - out1[32] = x109; - out1[33] = x111; - out1[34] = x113; - out1[35] = x115; - out1[36] = x118; - out1[37] = x120; - out1[38] = x122; - out1[39] = x124; - out1[40] = x126; - out1[41] = x128; - out1[42] = x130; - out1[43] = x133; - out1[44] = x135; - out1[45] = x137; - out1[46] = x139; - out1[47] = x141; - out1[48] = x143; - out1[49] = x145; - out1[50] = x148; - out1[51] = x150; - out1[52] = x152; - out1[53] = x154; - out1[54] = x156; - out1[55] = x158; - out1[56] = x160; - out1[57] = x161; - out1[58] = x162; - out1[59] = x164; - out1[60] = x166; - out1[61] = x168; - out1[62] = x170; - out1[63] = x172; - out1[64] = x174; - out1[65] = (x175 as u8); - out1 + ([ + x44, + x46, + x48, + x50, + x52, + x54, + x56, + x59, + x61, + x63, + x65, + x67, + x69, + x71, + x74, + x76, + x78, + x80, + x82, + x84, + x86, + x89, + x91, + x93, + x95, + x97, + x99, + x101, + x102, + x103, + x105, + x107, + x109, + x111, + x113, + x115, + x118, + x120, + x122, + x124, + x126, + x128, + x130, + x133, + x135, + x137, + x139, + x141, + x143, + x145, + x148, + x150, + x152, + x154, + x156, + x158, + x160, + x161, + x162, + x164, + x166, + x168, + x170, + x172, + x174, + (x175 as u8), + ]) } -#[doc = " The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = bytes_eval arg1 mod m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order. +/// +/// Postconditions: +/// eval out1 mod m = bytes_eval arg1 mod m +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_element { - let mut out1: fiat_p521_tight_field_element = [0; 9]; let x1: u64 = ((((arg1[65]) as fiat_p521_u1) as u64) << 56); let x2: u64 = (((arg1[64]) as u64) << 48); let x3: u64 = (((arg1[63]) as u64) << 40); @@ -1183,14 +1112,25 @@ pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_elem let x139: u64 = (x3 + x138); let x140: u64 = (x2 + x139); let x141: u64 = (x1 + x140); - out1[0] = x74; - out1[1] = x83; - out1[2] = x92; - out1[3] = x100; - out1[4] = x108; - out1[5] = x117; - out1[6] = x126; - out1[7] = x134; - out1[8] = x141; - out1 + (fiat_p521_tight_field_element([x74, x83, x92, x100, x108, x117, x126, x134, x141])) +} +impl fiat_p521_loose_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } +} +impl fiat_p521_tight_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } } diff --git a/p521/src/arithmetic/scalar.rs b/p521/src/arithmetic/scalar.rs index 66de4997..c161364b 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(&u32x18_to_u64x9( - w.as_words(), - ))) + Self(fiat_p521_scalar_to_montgomery( + &fiat_p521_scalar_non_montgomery_domain_field_element(u32x18_to_u64x9(w.as_words())), + )) } /// Decode [`Scalar`] from [`U576`] converting it into Montgomery form. @@ -142,7 +142,9 @@ impl Scalar { /// Used incorrectly this can lead to invalid results! #[cfg(target_pointer_width = "64")] pub(crate) const fn from_uint_unchecked(w: U576) -> Self { - Self(fiat_p521_scalar_to_montgomery(w.as_words())) + Self(fiat_p521_scalar_to_montgomery( + &fiat_p521_scalar_non_montgomery_domain_field_element(*w.as_words()), + )) } /// Returns the big-endian encoding of this [`Scalar`]. @@ -155,7 +157,9 @@ impl Scalar { #[inline] #[cfg(target_pointer_width = "32")] pub const fn to_canonical(self) -> U576 { - U576::from_words(u64x9_to_u32x18(&fiat_p521_scalar_from_montgomery(&self.0))) + U576::from_words(u64x9_to_u32x18( + fiat_p521_scalar_from_montgomery(&self.0).as_inner(), + )) } /// Translate [`Scalar`] out of the Montgomery domain, returning a [`U576`] @@ -163,7 +167,7 @@ impl Scalar { #[inline] #[cfg(target_pointer_width = "64")] pub const fn to_canonical(self) -> U576 { - U576::from_words(fiat_p521_scalar_from_montgomery(&self.0)) + U576::from_words(fiat_p521_scalar_from_montgomery(&self.0).into_inner()) } /// Determine if this [`Scalar`] is odd in the SEC1 sense: `self mod 2 == 1`. @@ -234,6 +238,7 @@ impl Scalar { 521, 9, u64, + fiat_p521_scalar_montgomery_domain_field_element, fiat_p521_scalar_from_montgomery, fiat_p521_scalar_mul, fiat_p521_scalar_opp, @@ -288,10 +293,12 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "32")] pub const fn shr_vartime(&self, shift: usize) -> Scalar { - Self(u32x18_to_u64x9( - &U576::from_words(u64x9_to_u32x18(&self.0)) - .shr_vartime(shift) - .to_words(), + Self(fiat_p521_scalar_montgomery_domain_field_element( + u32x18_to_u64x9( + &U576::from_words(u64x9_to_u32x18(self.0.as_inner())) + .shr_vartime(shift) + .to_words(), + ), )) } @@ -300,7 +307,11 @@ impl Scalar { /// Note: not constant-time with respect to the `shift` parameter. #[cfg(target_pointer_width = "64")] pub const fn shr_vartime(&self, shift: usize) -> Scalar { - Self(U576::from_words(self.0).shr_vartime(shift).to_words()) + Self(fiat_p521_scalar_montgomery_domain_field_element( + U576::from_words(self.0.into_inner()) + .shr_vartime(shift) + .to_words(), + )) } } @@ -319,7 +330,7 @@ impl Default for Scalar { impl Eq for Scalar {} impl PartialEq for Scalar { fn eq(&self, rhs: &Self) -> bool { - self.0.ct_eq(&(rhs.0)).into() + self.0.as_inner().ct_eq(rhs.0.as_inner()).into() } } @@ -343,19 +354,21 @@ impl From for Scalar { impl ConditionallySelectable for Scalar { fn conditional_select(a: &Self, b: &Self, choice: Choice) -> Self { - let mut ret = Self::ZERO; + let mut ret = Self::ZERO.0.into_inner(); + let a = a.0.as_inner(); + let b = b.0.as_inner(); - for i in 0..ret.0.len() { - ret.0[i] = u64::conditional_select(&a.0[i], &b.0[i], choice); + for i in 0..ret.len() { + ret[i] = u64::conditional_select(&a[i], &b[i], choice); } - ret + Self(fiat_p521_scalar_montgomery_domain_field_element(ret)) } } impl ConstantTimeEq for Scalar { fn ct_eq(&self, other: &Self) -> Choice { - self.0.ct_eq(&other.0) + self.0.as_inner().ct_eq(other.0.as_inner()) } } diff --git a/p521/src/arithmetic/scalar/p521_scalar_64.rs b/p521/src/arithmetic/scalar/p521_scalar_64.rs index 60c8646f..6b47cc92 100644 --- a/p521/src/arithmetic/scalar/p521_scalar_64.rs +++ b/p521/src/arithmetic/scalar/p521_scalar_64.rs @@ -1,22 +1,22 @@ -#![doc = " fiat-crypto output postprocessed by fiat-constify: "] -#![doc = " Autogenerated: './word_by_word_montgomery' --lang Rust --inline p521_scalar 64 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409"] -#![doc = " curve description: p521_scalar"] -#![doc = " machine_wordsize = 64 (from \"64\")"] -#![doc = " requested operations: (all)"] -#![doc = " m = 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 (from \"0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409\")"] -#![doc = ""] -#![doc = " NOTE: In addition to the bounds specified above each function, all"] -#![doc = " functions synthesized for this Montgomery arithmetic require the"] -#![doc = " input to be strictly less than the prime modulus (m), and also"] -#![doc = " require the input to be in the unique saturated representation."] -#![doc = " All functions also ensure that these two properties are true of"] -#![doc = " return values."] -#![doc = ""] -#![doc = " Computed values:"] -#![doc = " eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9)"] -#![doc = " bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)"] -#![doc = " twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) in"] -#![doc = " if x1 & (2^576-1) < 2^575 then x1 & (2^576-1) else (x1 & (2^576-1)) - 2^576"] +//! fiat-crypto output postprocessed by fiat-constify: +//! Autogenerated: './fiat-crypto' word-by-word-montgomery --lang Rust --inline p521_scalar 64 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 +//! curve description: p521_scalar +//! machine_wordsize = 64 (from "64") +//! requested operations: (all) +//! m = 0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409 (from "0x1fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffa51868783bf2f966b7fcc0148f709a5d03bb5c9b8899c47aebb6fb71e91386409") +//! +//! NOTE: In addition to the bounds specified above each function, all +//! functions synthesized for this Montgomery arithmetic require the +//! input to be strictly less than the prime modulus (m), and also +//! require the input to be in the unique saturated representation. +//! All functions also ensure that these two properties are true of +//! return values. +//! +//! Computed values: +//! eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) +//! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208) +//! twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) + (z[6] << 0x180) + (z[7] << 0x1c0) + (z[8] << 2^9) in +//! if x1 & (2^576-1) < 2^575 then x1 & (2^576-1) else (x1 & (2^576-1)) - 2^576 #![allow(unused_parens)] #![allow(non_camel_case_types)] #![allow( @@ -28,128 +28,154 @@ unused_mut, unused_variables )] +/// fiat_p521_scalar_u1 represents values of 1 bits, stored in one byte. pub type fiat_p521_scalar_u1 = u8; +/// fiat_p521_scalar_i1 represents values of 1 bits, stored in one byte. pub type fiat_p521_scalar_i1 = i8; +/// fiat_p521_scalar_u2 represents values of 2 bits, stored in one byte. pub type fiat_p521_scalar_u2 = u8; +/// fiat_p521_scalar_i2 represents values of 2 bits, stored in one byte. pub type fiat_p521_scalar_i2 = i8; -pub type fiat_p521_scalar_montgomery_domain_field_element = [u64; 9]; -pub type fiat_p521_scalar_non_montgomery_domain_field_element = [u64; 9]; -#[doc = " The function fiat_p521_scalar_addcarryx_u64 is an addition with carry."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^64"] -#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The type fiat_p521_scalar_montgomery_domain_field_element is a field element in the Montgomery domain. +/// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub struct fiat_p521_scalar_montgomery_domain_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_scalar_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_scalar_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The type fiat_p521_scalar_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. +/// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)] +pub struct fiat_p521_scalar_non_montgomery_domain_field_element(pub [u64; 9]); +impl core::ops::Index for fiat_p521_scalar_non_montgomery_domain_field_element { + type Output = u64; + #[inline] + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} +impl core::ops::IndexMut for fiat_p521_scalar_non_montgomery_domain_field_element { + #[inline] + fn index_mut(&mut self, index: usize) -> &mut Self::Output { + &mut self.0[index] + } +} +/// The function fiat_p521_scalar_addcarryx_u64 is an addition with carry. +/// +/// Postconditions: +/// out1 = (arg1 + arg2 + arg3) mod 2^64 +/// out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_scalar_addcarryx_u64( arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_scalar_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_scalar_u1 = 0; let x1: u128 = (((arg1 as u128) + (arg2 as u128)) + (arg3 as u128)); let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64); let x3: fiat_p521_scalar_u1 = ((x1 >> 64) as fiat_p521_scalar_u1); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_scalar_subborrowx_u64 is a subtraction with borrow."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^64"] -#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0x1]"] +/// The function fiat_p521_scalar_subborrowx_u64 is a subtraction with borrow. +/// +/// Postconditions: +/// out1 = (-arg1 + arg2 + -arg3) mod 2^64 +/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0x1] #[inline] pub const fn fiat_p521_scalar_subborrowx_u64( arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64, ) -> (u64, fiat_p521_scalar_u1) { - let mut out1: u64 = 0; - let mut out2: fiat_p521_scalar_u1 = 0; let x1: i128 = (((arg2 as i128) - (arg1 as i128)) - (arg3 as i128)); let x2: fiat_p521_scalar_i1 = ((x1 >> 64) as fiat_p521_scalar_i1); let x3: u64 = ((x1 & (0xffffffffffffffff as i128)) as u64); - out1 = x3; - out2 = (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1); - (out1, out2) + ( + x3, + (((0x0 as fiat_p521_scalar_i2) - (x2 as fiat_p521_scalar_i2)) as fiat_p521_scalar_u1), + ) } -#[doc = " The function fiat_p521_scalar_mulx_u64 is a multiplication, returning the full double-width result."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (arg1 * arg2) mod 2^64"] -#[doc = " out2 = ⌊arg1 * arg2 / 2^64⌋"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_mulx_u64 is a multiplication, returning the full double-width result. +/// +/// Postconditions: +/// out1 = (arg1 * arg2) mod 2^64 +/// out2 = ⌊arg1 * arg2 / 2^64⌋ +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0xffffffffffffffff] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_mulx_u64(arg1: u64, arg2: u64) -> (u64, u64) { - let mut out1: u64 = 0; - let mut out2: u64 = 0; let x1: u128 = ((arg1 as u128) * (arg2 as u128)); let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64); let x3: u64 = ((x1 >> 64) as u64); - out1 = x2; - out2 = x3; - (out1, out2) + (x2, x3) } -#[doc = " The function fiat_p521_scalar_cmovznz_u64 is a single-word conditional move."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_cmovznz_u64 is a single-word conditional move. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [0x0 ~> 0xffffffffffffffff] +/// arg3: [0x0 ~> 0xffffffffffffffff] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_cmovznz_u64(arg1: fiat_p521_scalar_u1, arg2: u64, arg3: u64) -> u64 { - let mut out1: u64 = 0; let x1: fiat_p521_scalar_u1 = (!(!arg1)); let x2: u64 = ((((((0x0 as fiat_p521_scalar_i2) - (x1 as fiat_p521_scalar_i2)) as fiat_p521_scalar_i1) as i128) & (0xffffffffffffffff as i128)) as u64); let x3: u64 = ((x2 & arg3) | ((!x2) & arg2)); - out1 = x3; - out1 + (x3) } -#[doc = " The function fiat_p521_scalar_mul multiplies two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_mul multiplies two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_mul( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -1688,30 +1714,23 @@ pub const fn fiat_p521_scalar_mul( let (x1033) = fiat_p521_scalar_cmovznz_u64(x1025, x1020, x1001); let mut x1034: u64 = 0; let (x1034) = fiat_p521_scalar_cmovznz_u64(x1025, x1022, x1003); - out1[0] = x1026; - out1[1] = x1027; - out1[2] = x1028; - out1[3] = x1029; - out1[4] = x1030; - out1[5] = x1031; - out1[6] = x1032; - out1[7] = x1033; - out1[8] = x1034; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, + ])) } -#[doc = " The function fiat_p521_scalar_square squares a field element in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_square squares a field element in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_square( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -3250,32 +3269,26 @@ pub const fn fiat_p521_scalar_square( let (x1033) = fiat_p521_scalar_cmovznz_u64(x1025, x1020, x1001); let mut x1034: u64 = 0; let (x1034) = fiat_p521_scalar_cmovznz_u64(x1025, x1022, x1003); - out1[0] = x1026; - out1[1] = x1027; - out1[2] = x1028; - out1[3] = x1029; - out1[4] = x1030; - out1[5] = x1031; - out1[6] = x1032; - out1[7] = x1033; - out1[8] = x1034; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x1026, x1027, x1028, x1029, x1030, x1031, x1032, x1033, x1034, + ])) } -#[doc = " The function fiat_p521_scalar_add adds two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_add adds two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_add( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_addcarryx_u64(0x0, (arg1[0]), (arg2[0])); @@ -3351,32 +3364,26 @@ pub const fn fiat_p521_scalar_add( let (x46) = fiat_p521_scalar_cmovznz_u64(x38, x33, x15); let mut x47: u64 = 0; let (x47) = fiat_p521_scalar_cmovznz_u64(x38, x35, x17); - out1[0] = x39; - out1[1] = x40; - out1[2] = x41; - out1[3] = x42; - out1[4] = x43; - out1[5] = x44; - out1[6] = x45; - out1[7] = x46; - out1[8] = x47; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x39, x40, x41, x42, x43, x44, x45, x46, x47, + ])) } -#[doc = " The function fiat_p521_scalar_sub subtracts two field elements in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " 0 ≤ eval arg2 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_sub subtracts two field elements in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// 0 ≤ eval arg2 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_sub( arg1: &fiat_p521_scalar_montgomery_domain_field_element, arg2: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); + let arg2 = arg2.as_inner(); let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_subborrowx_u64(0x0, (arg1[0]), (arg2[0])); @@ -3433,30 +3440,23 @@ pub const fn fiat_p521_scalar_sub( let mut x36: u64 = 0; let mut x37: fiat_p521_scalar_u1 = 0; let (x36, x37) = fiat_p521_scalar_addcarryx_u64(x35, x17, (x19 & 0x1ff)); - out1[0] = x20; - out1[1] = x22; - out1[2] = x24; - out1[3] = x26; - out1[4] = x28; - out1[5] = x30; - out1[6] = x32; - out1[7] = x34; - out1[8] = x36; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x20, x22, x24, x26, x28, x30, x32, x34, x36, + ])) } -#[doc = " The function fiat_p521_scalar_opp negates a field element in the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_opp negates a field element in the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_opp( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_subborrowx_u64(0x0, (0x0 as u64), (arg1[0])); @@ -3513,30 +3513,23 @@ pub const fn fiat_p521_scalar_opp( let mut x36: u64 = 0; let mut x37: fiat_p521_scalar_u1 = 0; let (x36, x37) = fiat_p521_scalar_addcarryx_u64(x35, x17, (x19 & 0x1ff)); - out1[0] = x20; - out1[1] = x22; - out1[2] = x24; - out1[3] = x26; - out1[4] = x28; - out1[5] = x30; - out1[6] = x32; - out1[7] = x34; - out1[8] = x36; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x20, x22, x24, x26, x28, x30, x32, x34, x36, + ])) } -#[doc = " The function fiat_p521_scalar_from_montgomery translates a field element out of the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^9) mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_from_montgomery translates a field element out of the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^9) mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_from_montgomery( arg1: &fiat_p521_scalar_montgomery_domain_field_element, ) -> fiat_p521_scalar_non_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_non_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[0]); let mut x2: u64 = 0; let mut x3: u64 = 0; @@ -4540,30 +4533,23 @@ pub const fn fiat_p521_scalar_from_montgomery( let (x644) = fiat_p521_scalar_cmovznz_u64(x636, x631, x614); let mut x645: u64 = 0; let (x645) = fiat_p521_scalar_cmovznz_u64(x636, x633, x616); - out1[0] = x637; - out1[1] = x638; - out1[2] = x639; - out1[3] = x640; - out1[4] = x641; - out1[5] = x642; - out1[6] = x643; - out1[7] = x644; - out1[8] = x645; - out1 + (fiat_p521_scalar_non_montgomery_domain_field_element([ + x637, x638, x639, x640, x641, x642, x643, x644, x645, + ])) } -#[doc = " The function fiat_p521_scalar_to_montgomery translates a field element into the Montgomery domain."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = eval arg1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_to_montgomery translates a field element into the Montgomery domain. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// eval (from_montgomery out1) mod m = eval arg1 mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_to_montgomery( arg1: &fiat_p521_scalar_non_montgomery_domain_field_element, ) -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; + let arg1 = arg1.as_inner(); let x1: u64 = (arg1[1]); let x2: u64 = (arg1[2]); let x3: u64 = (arg1[3]); @@ -6059,57 +6045,47 @@ pub const fn fiat_p521_scalar_to_montgomery( let (x974) = fiat_p521_scalar_cmovznz_u64(x966, x961, x944); let mut x975: u64 = 0; let (x975) = fiat_p521_scalar_cmovznz_u64(x966, x963, x946); - out1[0] = x967; - out1[1] = x968; - out1[2] = x969; - out1[3] = x970; - out1[4] = x971; - out1[5] = x972; - out1[6] = x973; - out1[7] = x974; - out1[8] = x975; - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + x967, x968, x969, x970, x971, x972, x973, x974, x975, + ])) } -#[doc = " The function fiat_p521_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] +/// The function fiat_p521_scalar_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] #[inline] pub const fn fiat_p521_scalar_nonzero(arg1: &[u64; 9]) -> u64 { - let mut out1: u64 = 0; let x1: u64 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | ((arg1[7]) | (arg1[8]))))))))); - out1 = x1; - out1 + (x1) } -#[doc = " The function fiat_p521_scalar_selectznz is a multi-limb conditional select."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0x1]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_selectznz is a multi-limb conditional select. +/// +/// Postconditions: +/// out1 = (if arg1 = 0 then arg2 else arg3) +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0x1] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_selectznz( arg1: fiat_p521_scalar_u1, arg2: &[u64; 9], arg3: &[u64; 9], ) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let (x1) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[0]), (arg3[0])); let mut x2: u64 = 0; @@ -6128,31 +6104,21 @@ pub const fn fiat_p521_scalar_selectznz( let (x8) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[7]), (arg3[7])); let mut x9: u64 = 0; let (x9) = fiat_p521_scalar_cmovznz_u64(arg1, (arg2[8]), (arg3[8])); - out1[0] = x1; - out1[1] = x2; - out1[2] = x3; - out1[3] = x4; - out1[4] = x5; - out1[5] = x6; - out1[6] = x7; - out1[7] = x8; - out1[8] = x9; - out1 + ([x1, x2, x3, x4, x5, x6, x7, x8, x9]) } -#[doc = " The function fiat_p521_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] +/// The function fiat_p521_scalar_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order. +/// +/// Preconditions: +/// 0 ≤ eval arg1 < m +/// Postconditions: +/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65] +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] #[inline] pub const fn fiat_p521_scalar_to_bytes(arg1: &[u64; 9]) -> [u8; 66] { - let mut out1: [u8; 66] = [0; 66]; let x1: u64 = (arg1[8]); let x2: u64 = (arg1[7]); let x3: u64 = (arg1[6]); @@ -6276,89 +6242,89 @@ pub const fn fiat_p521_scalar_to_bytes(arg1: &[u64; 9]) -> [u8; 66] { let x121: u8 = ((x119 >> 8) as u8); let x122: u8 = ((x1 & (0xff as u64)) as u8); let x123: fiat_p521_scalar_u1 = ((x1 >> 8) as fiat_p521_scalar_u1); - out1[0] = x10; - out1[1] = x12; - out1[2] = x14; - out1[3] = x16; - out1[4] = x18; - out1[5] = x20; - out1[6] = x22; - out1[7] = x23; - out1[8] = x24; - out1[9] = x26; - out1[10] = x28; - out1[11] = x30; - out1[12] = x32; - out1[13] = x34; - out1[14] = x36; - out1[15] = x37; - out1[16] = x38; - out1[17] = x40; - out1[18] = x42; - out1[19] = x44; - out1[20] = x46; - out1[21] = x48; - out1[22] = x50; - out1[23] = x51; - out1[24] = x52; - out1[25] = x54; - out1[26] = x56; - out1[27] = x58; - out1[28] = x60; - out1[29] = x62; - out1[30] = x64; - out1[31] = x65; - out1[32] = x66; - out1[33] = x68; - out1[34] = x70; - out1[35] = x72; - out1[36] = x74; - out1[37] = x76; - out1[38] = x78; - out1[39] = x79; - out1[40] = x80; - out1[41] = x82; - out1[42] = x84; - out1[43] = x86; - out1[44] = x88; - out1[45] = x90; - out1[46] = x92; - out1[47] = x93; - out1[48] = x94; - out1[49] = x96; - out1[50] = x98; - out1[51] = x100; - out1[52] = x102; - out1[53] = x104; - out1[54] = x106; - out1[55] = x107; - out1[56] = x108; - out1[57] = x110; - out1[58] = x112; - out1[59] = x114; - out1[60] = x116; - out1[61] = x118; - out1[62] = x120; - out1[63] = x121; - out1[64] = x122; - out1[65] = (x123 as u8); - out1 + ([ + x10, + x12, + x14, + x16, + x18, + x20, + x22, + x23, + x24, + x26, + x28, + x30, + x32, + x34, + x36, + x37, + x38, + x40, + x42, + x44, + x46, + x48, + x50, + x51, + x52, + x54, + x56, + x58, + x60, + x62, + x64, + x65, + x66, + x68, + x70, + x72, + x74, + x76, + x78, + x79, + x80, + x82, + x84, + x86, + x88, + x90, + x92, + x93, + x94, + x96, + x98, + x100, + x102, + x104, + x106, + x107, + x108, + x110, + x112, + x114, + x116, + x118, + x120, + x121, + x122, + (x123 as u8), + ]) } -#[doc = " The function fiat_p521_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ bytes_eval arg1 < m"] -#[doc = " Postconditions:"] -#[doc = " eval out1 mod m = bytes_eval arg1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]]"] +/// The function fiat_p521_scalar_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order. +/// +/// Preconditions: +/// 0 ≤ bytes_eval arg1 < m +/// Postconditions: +/// eval out1 mod m = bytes_eval arg1 mod m +/// 0 ≤ eval out1 < m +/// +/// Input Bounds: +/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]] +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1ff]] #[inline] pub const fn fiat_p521_scalar_from_bytes(arg1: &[u8; 66]) -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; let x1: u64 = ((((arg1[65]) as fiat_p521_scalar_u1) as u64) << 8); let x2: u8 = (arg1[64]); let x3: u64 = (((arg1[63]) as u64) << 56); @@ -6482,110 +6448,101 @@ pub const fn fiat_p521_scalar_from_bytes(arg1: &[u8; 66]) -> [u64; 9] { let x121: u64 = (x4 + x120); let x122: u64 = (x3 + x121); let x123: u64 = (x1 + (x2 as u64)); - out1[0] = x73; - out1[1] = x80; - out1[2] = x87; - out1[3] = x94; - out1[4] = x101; - out1[5] = x108; - out1[6] = x115; - out1[7] = x122; - out1[8] = x123; - out1 + ([x73, x80, x87, x94, x101, x108, x115, x122, x123]) } -#[doc = " The function fiat_p521_scalar_set_one returns the field element one in the Montgomery domain."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) mod m = 1 mod m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] +/// The function fiat_p521_scalar_set_one returns the field element one in the Montgomery domain. +/// +/// Postconditions: +/// eval (from_montgomery out1) mod m = 1 mod m +/// 0 ≤ eval out1 < m +/// #[inline] pub const fn fiat_p521_scalar_set_one() -> fiat_p521_scalar_montgomery_domain_field_element { - let mut out1: fiat_p521_scalar_montgomery_domain_field_element = [0; 9]; - out1[0] = 0xfb80000000000000; - out1[1] = 0x28a2482470b763cd; - out1[2] = 0x17e2251b23bb31dc; - out1[3] = 0xca4019ff5b847b2d; - out1[4] = 0x2d73cbc3e206834; - out1[5] = (0x0 as u64); - out1[6] = (0x0 as u64); - out1[7] = (0x0 as u64); - out1[8] = (0x0 as u64); - out1 + (fiat_p521_scalar_montgomery_domain_field_element([ + 0xfb80000000000000, + 0x28a2482470b763cd, + 0x17e2251b23bb31dc, + 0xca4019ff5b847b2d, + 0x2d73cbc3e206834, + (0x0 as u64), + (0x0 as u64), + (0x0 as u64), + (0x0 as u64), + ])) } -#[doc = " The function fiat_p521_scalar_msat returns the saturated representation of the prime modulus."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " twos_complement_eval out1 = m"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_msat returns the saturated representation of the prime modulus. +/// +/// Postconditions: +/// twos_complement_eval out1 = m +/// 0 ≤ eval out1 < m +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_msat() -> [u64; 10] { - let mut out1: [u64; 10] = [0; 10]; - out1[0] = 0xbb6fb71e91386409; - out1[1] = 0x3bb5c9b8899c47ae; - out1[2] = 0x7fcc0148f709a5d0; - out1[3] = 0x51868783bf2f966b; - out1[4] = 0xfffffffffffffffa; - out1[5] = 0xffffffffffffffff; - out1[6] = 0xffffffffffffffff; - out1[7] = 0xffffffffffffffff; - out1[8] = 0x1ff; - out1[9] = (0x0 as u64); - out1 + ([ + 0xbb6fb71e91386409, + 0x3bb5c9b8899c47ae, + 0x7fcc0148f709a5d0, + 0x51868783bf2f966b, + 0xfffffffffffffffa, + 0xffffffffffffffff, + 0xffffffffffffffff, + 0xffffffffffffffff, + 0x1ff, + (0x0 as u64), + ]) } -#[doc = " The function fiat_p521_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form)."] -#[doc = ""] -#[doc = " Postconditions:"] -#[doc = " eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)"] -#[doc = " 0 ≤ eval out1 < m"] -#[doc = ""] -#[doc = " Output Bounds:"] -#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form). +/// +/// Postconditions: +/// eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋) +/// 0 ≤ eval out1 < m +/// +/// Output Bounds: +/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_divstep_precomp() -> [u64; 9] { - let mut out1: [u64; 9] = [0; 9]; - out1[0] = 0x7b27a0cb33d1884b; - out1[1] = 0x9ef6cb011f2467d8; - out1[2] = 0x5fbc88e1d6e7fce; - out1[3] = 0xb08222d0fe97e1dc; - out1[4] = 0x1624870c44df3fce; - out1[5] = 0xb7f07b8eedbce602; - out1[6] = 0x62da93cf721f63bc; - out1[7] = 0xafd209c16c4f0d20; - out1[8] = 0x1c7; - out1 + ([ + 0x7b27a0cb33d1884b, + 0x9ef6cb011f2467d8, + 0x5fbc88e1d6e7fce, + 0xb08222d0fe97e1dc, + 0x1624870c44df3fce, + 0xb7f07b8eedbce602, + 0x62da93cf721f63bc, + 0xafd209c16c4f0d20, + 0x1c7, + ]) } -#[doc = " The function fiat_p521_scalar_divstep computes a divstep."] -#[doc = ""] -#[doc = " Preconditions:"] -#[doc = " 0 ≤ eval arg4 < m"] -#[doc = " 0 ≤ eval arg5 < m"] -#[doc = " Postconditions:"] -#[doc = " out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)"] -#[doc = " twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)"] -#[doc = " twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)"] -#[doc = " eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)"] -#[doc = " eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)"] -#[doc = " 0 ≤ eval out5 < m"] -#[doc = " 0 ≤ eval out5 < m"] -#[doc = " 0 ≤ eval out2 < m"] -#[doc = " 0 ≤ eval out3 < m"] -#[doc = ""] -#[doc = " Input Bounds:"] -#[doc = " arg1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " Output Bounds:"] -#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"] -#[doc = " out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] -#[doc = " out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"] +/// The function fiat_p521_scalar_divstep computes a divstep. +/// +/// Preconditions: +/// 0 ≤ eval arg4 < m +/// 0 ≤ eval arg5 < m +/// Postconditions: +/// out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1) +/// twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2) +/// twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋) +/// eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m) +/// eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m) +/// 0 ≤ eval out5 < m +/// 0 ≤ eval out5 < m +/// 0 ≤ eval out2 < m +/// 0 ≤ eval out3 < m +/// +/// Input Bounds: +/// arg1: [0x0 ~> 0xffffffffffffffff] +/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// Output Bounds: +/// out1: [0x0 ~> 0xffffffffffffffff] +/// out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] +/// out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] #[inline] pub const fn fiat_p521_scalar_divstep( arg1: u64, @@ -6594,11 +6551,6 @@ pub const fn fiat_p521_scalar_divstep( arg4: &[u64; 9], arg5: &[u64; 9], ) -> (u64, [u64; 10], [u64; 10], [u64; 9], [u64; 9]) { - let mut out1: u64 = 0; - let mut out2: [u64; 10] = [0; 10]; - let mut out3: [u64; 10] = [0; 10]; - let mut out4: [u64; 9] = [0; 9]; - let mut out5: [u64; 9] = [0; 9]; let mut x1: u64 = 0; let mut x2: fiat_p521_scalar_u1 = 0; let (x1, x2) = fiat_p521_scalar_addcarryx_u64(0x0, (!arg1), (0x1 as u64)); @@ -7012,44 +6964,31 @@ pub const fn fiat_p521_scalar_divstep( let (x255) = fiat_p521_scalar_cmovznz_u64(x226, x221, x203); let mut x256: u64 = 0; let (x256) = fiat_p521_scalar_cmovznz_u64(x226, x223, x205); - out1 = x227; - out2[0] = x7; - out2[1] = x8; - out2[2] = x9; - out2[3] = x10; - out2[4] = x11; - out2[5] = x12; - out2[6] = x13; - out2[7] = x14; - out2[8] = x15; - out2[9] = x16; - out3[0] = x229; - out3[1] = x230; - out3[2] = x231; - out3[3] = x232; - out3[4] = x233; - out3[5] = x234; - out3[6] = x235; - out3[7] = x236; - out3[8] = x237; - out3[9] = x238; - out4[0] = x239; - out4[1] = x240; - out4[2] = x241; - out4[3] = x242; - out4[4] = x243; - out4[5] = x244; - out4[6] = x245; - out4[7] = x246; - out4[8] = x247; - out5[0] = x248; - out5[1] = x249; - out5[2] = x250; - out5[3] = x251; - out5[4] = x252; - out5[5] = x253; - out5[6] = x254; - out5[7] = x255; - out5[8] = x256; - (out1, out2, out3, out4, out5) + ( + x227, + [x7, x8, x9, x10, x11, x12, x13, x14, x15, x16], + [x229, x230, x231, x232, x233, x234, x235, x236, x237, x238], + [x239, x240, x241, x242, x243, x244, x245, x246, x247], + [x248, x249, x250, x251, x252, x253, x254, x255, x256], + ) +} +impl fiat_p521_scalar_montgomery_domain_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } +} +impl fiat_p521_scalar_non_montgomery_domain_field_element { + #[inline] + pub const fn as_inner(&self) -> &[u64; 9] { + &self.0 + } + #[inline] + pub const fn into_inner(self) -> [u64; 9] { + self.0 + } } diff --git a/p521/src/lib.rs b/p521/src/lib.rs index e0056a01..ecacd617 100644 --- a/p521/src/lib.rs +++ b/p521/src/lib.rs @@ -40,6 +40,9 @@ pub mod test_vectors; #[cfg(feature = "arithmetic")] pub use arithmetic::{scalar::Scalar, AffinePoint, ProjectivePoint}; +#[cfg(feature = "expose-field")] +pub use arithmetic::field::FieldElement; + pub use elliptic_curve::{self, bigint::U576}; #[cfg(feature = "pkcs8")] diff --git a/primeorder/src/field.rs b/primeorder/src/field.rs index 9a3b6ead..8ef8880b 100644 --- a/primeorder/src/field.rs +++ b/primeorder/src/field.rs @@ -510,6 +510,7 @@ macro_rules! impl_bernstein_yang_invert { $d:expr, $nlimbs:expr, $word:ty, + $mont_type: expr, $from_mont:ident, $mul:ident, $neg:ident, @@ -525,36 +526,36 @@ macro_rules! impl_bernstein_yang_invert { let mut d = 1; let mut f = $msat(); let mut g = [0; $nlimbs + 1]; - let mut v = [0; $nlimbs]; - let mut r = $one; + let mut v = $mont_type([0; $nlimbs]); + let mut r = $one.into_inner(); let mut i = 0; let mut j = 0; while j < $nlimbs { - g[j] = a[j]; + g[j] = a.as_inner()[j]; j += 1; } while i < ITERATIONS - ITERATIONS % 2 { - let (out1, out2, out3, out4, out5) = $divstep(d, &f, &g, &v, &r); + let (out1, out2, out3, out4, out5) = $divstep(d, &f, &g, &v.0, &r); let (out1, out2, out3, out4, out5) = $divstep(out1, &out2, &out3, &out4, &out5); d = out1; f = out2; g = out3; - v = out4; + v = $mont_type(out4); r = out5; i += 2; } if ITERATIONS % 2 != 0 { - let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, &v, &r); - v = out4; + let (_out1, out2, _out3, out4, _out5) = $divstep(d, &f, &g, v.as_inner(), &r); + v = $mont_type(out4); f = out2; } let s = ((f[f.len() - 1] >> <$word>::BITS - 1) & 1) as u8; - let v = $selectznz(s, &v, &$neg(&v)); - $mul(&v, &$divstep_precomp()) + let v = $mont_type($selectznz(s, v.as_inner(), $neg(&v).as_inner())); + $mul(&v, &$mont_type($divstep_precomp())) }}; } diff --git a/sm2/Cargo.toml b/sm2/Cargo.toml index 2847f36c..8e58be1f 100644 --- a/sm2/Cargo.toml +++ b/sm2/Cargo.toml @@ -20,7 +20,7 @@ rust-version = "1.65" elliptic-curve = { version = "0.13", default-features = false, features = ["hazmat", "sec1"] } # optional dependencies -primeorder = { version = "0.13.1", optional = true, path = "../primeorder" } +primeorder = { version = "0.13.1", optional = true } rfc6979 = { version = "0.4", optional = true } serdect = { version = "0.2", optional = true, default-features = false } signature = { version = "2.2", optional = true, features = ["rand_core"] }