summaryrefslogtreecommitdiffstats
path: root/vendor/fiat-crypto/src/p521_64.rs
diff options
context:
space:
mode:
authorDaniel Baumann <daniel.baumann@progress-linux.org>2024-06-19 09:26:03 +0000
committerDaniel Baumann <daniel.baumann@progress-linux.org>2024-06-19 09:26:03 +0000
commit9918693037dce8aa4bb6f08741b6812923486c18 (patch)
tree21d2b40bec7e6a7ea664acee056eb3d08e15a1cf /vendor/fiat-crypto/src/p521_64.rs
parentReleasing progress-linux version 1.75.0+dfsg1-5~progress7.99u1. (diff)
downloadrustc-9918693037dce8aa4bb6f08741b6812923486c18.tar.xz
rustc-9918693037dce8aa4bb6f08741b6812923486c18.zip
Merging upstream version 1.76.0+dfsg1.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'vendor/fiat-crypto/src/p521_64.rs')
-rw-r--r--vendor/fiat-crypto/src/p521_64.rs82
1 files changed, 59 insertions, 23 deletions
diff --git a/vendor/fiat-crypto/src/p521_64.rs b/vendor/fiat-crypto/src/p521_64.rs
index c9e82ff70..5dc862935 100644
--- a/vendor/fiat-crypto/src/p521_64.rs
+++ b/vendor/fiat-crypto/src/p521_64.rs
@@ -1,8 +1,8 @@
-//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p521 64 9 '2^521 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
+//! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p521 64 '(auto)' '2^521 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
//! curve description: p521
//! machine_wordsize = 64 (from "64")
//! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
-//! n = 9 (from "9")
+//! n = 9 (from "(auto)")
//! s-c = 2^521 - [(1, 1)] (from "2^521 - 1")
//! tight_bounds_multiplier = 1 (from "")
//!
@@ -15,18 +15,54 @@
#![allow(unused_parens)]
#![allow(non_camel_case_types)]
+/** fiat_p521_u1 represents values of 1 bits, stored in one byte. */
pub type fiat_p521_u1 = u8;
+/** fiat_p521_i1 represents values of 1 bits, stored in one byte. */
pub type fiat_p521_i1 = i8;
+/** fiat_p521_u2 represents values of 2 bits, stored in one byte. */
pub type fiat_p521_u2 = u8;
+/** fiat_p521_i2 represents values of 2 bits, stored in one byte. */
pub type fiat_p521_i2 = i8;
-/* The type fiat_p521_loose_field_element is a field element with loose bounds. */
-/* Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */
-pub type fiat_p521_loose_field_element = [u64; 9];
+/** The type fiat_p521_loose_field_element is a field element with loose bounds. */
+/** Bounds: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]] */
+#[derive(Clone, Copy)]
+pub struct fiat_p521_loose_field_element(pub [u64; 9]);
-/* 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]] */
-pub type fiat_p521_tight_field_element = [u64; 9];
+impl core::ops::Index<usize> for fiat_p521_loose_field_element {
+ type Output = u64;
+ #[inline]
+ fn index(&self, index: usize) -> &Self::Output {
+ &self.0[index]
+ }
+}
+
+impl core::ops::IndexMut<usize> for fiat_p521_loose_field_element {
+ #[inline]
+ fn index_mut(&mut self, index: usize) -> &mut Self::Output {
+ &mut self.0[index]
+ }
+}
+
+/** The type fiat_p521_tight_field_element is a field element with tight bounds. */
+/** Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]] */
+#[derive(Clone, Copy)]
+pub struct fiat_p521_tight_field_element(pub [u64; 9]);
+
+impl core::ops::Index<usize> for fiat_p521_tight_field_element {
+ type Output = u64;
+ #[inline]
+ fn index(&self, index: usize) -> &Self::Output {
+ &self.0[index]
+ }
+}
+
+impl core::ops::IndexMut<usize> 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.
@@ -43,7 +79,7 @@ pub type fiat_p521_tight_field_element = [u64; 9];
/// out1: [0x0 ~> 0x3ffffffffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p521_addcarryx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> () {
+pub fn fiat_p521_addcarryx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) {
let x1: u64 = (((arg1 as u64) + arg2) + arg3);
let x2: u64 = (x1 & 0x3ffffffffffffff);
let x3: fiat_p521_u1 = ((x1 >> 58) as fiat_p521_u1);
@@ -65,7 +101,7 @@ pub fn fiat_p521_addcarryx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fi
/// out1: [0x0 ~> 0x3ffffffffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p521_subborrowx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> () {
+pub fn fiat_p521_subborrowx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) {
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);
@@ -87,7 +123,7 @@ pub fn fiat_p521_subborrowx_u58(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: f
/// out1: [0x0 ~> 0x1ffffffffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p521_addcarryx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> () {
+pub fn fiat_p521_addcarryx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) {
let x1: u64 = (((arg1 as u64) + arg2) + arg3);
let x2: u64 = (x1 & 0x1ffffffffffffff);
let x3: fiat_p521_u1 = ((x1 >> 57) as fiat_p521_u1);
@@ -109,7 +145,7 @@ pub fn fiat_p521_addcarryx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fi
/// out1: [0x0 ~> 0x1ffffffffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p521_subborrowx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> () {
+pub fn fiat_p521_subborrowx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: fiat_p521_u1, arg2: u64, arg3: u64) {
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);
@@ -129,7 +165,7 @@ pub fn fiat_p521_subborrowx_u57(out1: &mut u64, out2: &mut fiat_p521_u1, arg1: f
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
#[inline]
-pub fn fiat_p521_cmovznz_u64(out1: &mut u64, arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> () {
+pub fn fiat_p521_cmovznz_u64(out1: &mut u64, arg1: fiat_p521_u1, arg2: u64, arg3: u64) {
let x1: fiat_p521_u1 = (!(!arg1));
let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) as i128) & (0xffffffffffffffff as i128)) as u64);
let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
@@ -142,7 +178,7 @@ pub fn fiat_p521_cmovznz_u64(out1: &mut u64, arg1: fiat_p521_u1, arg2: u64, arg3
/// eval out1 mod m = (eval arg1 * eval arg2) mod m
///
#[inline]
-pub fn fiat_p521_carry_mul(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element, arg2: &fiat_p521_loose_field_element) -> () {
+pub fn fiat_p521_carry_mul(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element, arg2: &fiat_p521_loose_field_element) {
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));
@@ -283,7 +319,7 @@ pub fn fiat_p521_carry_mul(out1: &mut fiat_p521_tight_field_element, arg1: &fiat
/// eval out1 mod m = (eval arg1 * eval arg1) mod m
///
#[inline]
-pub fn fiat_p521_carry_square(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element) -> () {
+pub fn fiat_p521_carry_square(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element) {
let x1: u64 = (arg1[8]);
let x2: u64 = (x1 * 0x2);
let x3: u64 = ((arg1[8]) * 0x2);
@@ -404,7 +440,7 @@ pub fn fiat_p521_carry_square(out1: &mut fiat_p521_tight_field_element, arg1: &f
/// eval out1 mod m = eval arg1 mod m
///
#[inline]
-pub fn fiat_p521_carry(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element) -> () {
+pub fn fiat_p521_carry(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p521_loose_field_element) {
let x1: u64 = (arg1[0]);
let x2: u64 = ((x1 >> 58) + (arg1[1]));
let x3: u64 = ((x2 >> 58) + (arg1[2]));
@@ -442,7 +478,7 @@ pub fn fiat_p521_carry(out1: &mut fiat_p521_tight_field_element, arg1: &fiat_p52
/// eval out1 mod m = (eval arg1 + eval arg2) mod m
///
#[inline]
-pub fn fiat_p521_add(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element) -> () {
+pub fn fiat_p521_add(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element) {
let x1: u64 = ((arg1[0]) + (arg2[0]));
let x2: u64 = ((arg1[1]) + (arg2[1]));
let x3: u64 = ((arg1[2]) + (arg2[2]));
@@ -469,7 +505,7 @@ pub fn fiat_p521_add(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_
/// eval out1 mod m = (eval arg1 - eval arg2) mod m
///
#[inline]
-pub fn fiat_p521_sub(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element) -> () {
+pub fn fiat_p521_sub(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element, arg2: &fiat_p521_tight_field_element) {
let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0]));
let x2: u64 = ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]));
let x3: u64 = ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]));
@@ -496,7 +532,7 @@ pub fn fiat_p521_sub(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_
/// eval out1 mod m = -eval arg1 mod m
///
#[inline]
-pub fn fiat_p521_opp(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element) -> () {
+pub fn fiat_p521_opp(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element) {
let x1: u64 = (0x7fffffffffffffe - (arg1[0]));
let x2: u64 = (0x7fffffffffffffe - (arg1[1]));
let x3: u64 = (0x7fffffffffffffe - (arg1[2]));
@@ -529,7 +565,7 @@ pub fn fiat_p521_opp(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
#[inline]
-pub fn fiat_p521_selectznz(out1: &mut [u64; 9], arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) -> () {
+pub fn fiat_p521_selectznz(out1: &mut [u64; 9], arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) {
let mut x1: u64 = 0;
fiat_p521_cmovznz_u64(&mut x1, arg1, (arg2[0]), (arg3[0]));
let mut x2: u64 = 0;
@@ -567,7 +603,7 @@ pub fn fiat_p521_selectznz(out1: &mut [u64; 9], arg1: fiat_p521_u1, arg2: &[u64;
/// 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 fn fiat_p521_to_bytes(out1: &mut [u8; 66], arg1: &fiat_p521_tight_field_element) -> () {
+pub fn fiat_p521_to_bytes(out1: &mut [u8; 66], arg1: &fiat_p521_tight_field_element) {
let mut x1: u64 = 0;
let mut x2: fiat_p521_u1 = 0;
fiat_p521_subborrowx_u58(&mut x1, &mut x2, 0x0, (arg1[0]), 0x3ffffffffffffff);
@@ -838,7 +874,7 @@ pub fn fiat_p521_to_bytes(out1: &mut [u8; 66], arg1: &fiat_p521_tight_field_elem
/// 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 fn fiat_p521_from_bytes(out1: &mut fiat_p521_tight_field_element, arg1: &[u8; 66]) -> () {
+pub fn fiat_p521_from_bytes(out1: &mut fiat_p521_tight_field_element, arg1: &[u8; 66]) {
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);
@@ -997,7 +1033,7 @@ pub fn fiat_p521_from_bytes(out1: &mut fiat_p521_tight_field_element, arg1: &[u8
/// out1 = arg1
///
#[inline]
-pub fn fiat_p521_relax(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element) -> () {
+pub fn fiat_p521_relax(out1: &mut fiat_p521_loose_field_element, arg1: &fiat_p521_tight_field_element) {
let x1: u64 = (arg1[0]);
let x2: u64 = (arg1[1]);
let x3: u64 = (arg1[2]);