summaryrefslogtreecommitdiffstats
path: root/vendor/fiat-crypto/src/p256_32.rs
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/fiat-crypto/src/p256_32.rs')
-rw-r--r--vendor/fiat-crypto/src/p256_32.rs86
1 files changed, 61 insertions, 25 deletions
diff --git a/vendor/fiat-crypto/src/p256_32.rs b/vendor/fiat-crypto/src/p256_32.rs
index 5eb80994d..2910796bc 100644
--- a/vendor/fiat-crypto/src/p256_32.rs
+++ b/vendor/fiat-crypto/src/p256_32.rs
@@ -20,18 +20,54 @@
#![allow(unused_parens)]
#![allow(non_camel_case_types)]
+/** fiat_p256_u1 represents values of 1 bits, stored in one byte. */
pub type fiat_p256_u1 = u8;
+/** fiat_p256_i1 represents values of 1 bits, stored in one byte. */
pub type fiat_p256_i1 = i8;
+/** fiat_p256_u2 represents values of 2 bits, stored in one byte. */
pub type fiat_p256_u2 = u8;
+/** fiat_p256_i2 represents values of 2 bits, stored in one byte. */
pub type fiat_p256_i2 = i8;
-/* The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
-pub type fiat_p256_montgomery_domain_field_element = [u32; 8];
+/** The type fiat_p256_montgomery_domain_field_element is a field element in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+#[derive(Clone, Copy)]
+pub struct fiat_p256_montgomery_domain_field_element(pub [u32; 8]);
-/* The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
-/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
-pub type fiat_p256_non_montgomery_domain_field_element = [u32; 8];
+impl core::ops::Index<usize> for fiat_p256_montgomery_domain_field_element {
+ type Output = u32;
+ #[inline]
+ fn index(&self, index: usize) -> &Self::Output {
+ &self.0[index]
+ }
+}
+
+impl core::ops::IndexMut<usize> for fiat_p256_montgomery_domain_field_element {
+ #[inline]
+ fn index_mut(&mut self, index: usize) -> &mut Self::Output {
+ &mut self.0[index]
+ }
+}
+
+/** The type fiat_p256_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
+/** Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
+#[derive(Clone, Copy)]
+pub struct fiat_p256_non_montgomery_domain_field_element(pub [u32; 8]);
+
+impl core::ops::Index<usize> for fiat_p256_non_montgomery_domain_field_element {
+ type Output = u32;
+ #[inline]
+ fn index(&self, index: usize) -> &Self::Output {
+ &self.0[index]
+ }
+}
+
+impl core::ops::IndexMut<usize> for fiat_p256_non_montgomery_domain_field_element {
+ #[inline]
+ fn index_mut(&mut self, index: usize) -> &mut Self::Output {
+ &mut self.0[index]
+ }
+}
/// The function fiat_p256_addcarryx_u32 is an addition with carry.
@@ -48,7 +84,7 @@ pub type fiat_p256_non_montgomery_domain_field_element = [u32; 8];
/// out1: [0x0 ~> 0xffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p256_addcarryx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: fiat_p256_u1, arg2: u32, arg3: u32) -> () {
+pub fn fiat_p256_addcarryx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: fiat_p256_u1, arg2: u32, arg3: u32) {
let x1: u64 = (((arg1 as u64) + (arg2 as u64)) + (arg3 as u64));
let x2: u32 = ((x1 & (0xffffffff as u64)) as u32);
let x3: fiat_p256_u1 = ((x1 >> 32) as fiat_p256_u1);
@@ -70,7 +106,7 @@ pub fn fiat_p256_addcarryx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: fi
/// out1: [0x0 ~> 0xffffffff]
/// out2: [0x0 ~> 0x1]
#[inline]
-pub fn fiat_p256_subborrowx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: fiat_p256_u1, arg2: u32, arg3: u32) -> () {
+pub fn fiat_p256_subborrowx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: fiat_p256_u1, arg2: u32, arg3: u32) {
let x1: i64 = (((arg2 as i64) - (arg1 as i64)) - (arg3 as i64));
let x2: fiat_p256_i1 = ((x1 >> 32) as fiat_p256_i1);
let x3: u32 = ((x1 & (0xffffffff as i64)) as u32);
@@ -91,7 +127,7 @@ pub fn fiat_p256_subborrowx_u32(out1: &mut u32, out2: &mut fiat_p256_u1, arg1: f
/// out1: [0x0 ~> 0xffffffff]
/// out2: [0x0 ~> 0xffffffff]
#[inline]
-pub fn fiat_p256_mulx_u32(out1: &mut u32, out2: &mut u32, arg1: u32, arg2: u32) -> () {
+pub fn fiat_p256_mulx_u32(out1: &mut u32, out2: &mut u32, arg1: u32, arg2: u32) {
let x1: u64 = ((arg1 as u64) * (arg2 as u64));
let x2: u32 = ((x1 & (0xffffffff as u64)) as u32);
let x3: u32 = ((x1 >> 32) as u32);
@@ -111,7 +147,7 @@ pub fn fiat_p256_mulx_u32(out1: &mut u32, out2: &mut u32, arg1: u32, arg2: u32)
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffff]
#[inline]
-pub fn fiat_p256_cmovznz_u32(out1: &mut u32, arg1: fiat_p256_u1, arg2: u32, arg3: u32) -> () {
+pub fn fiat_p256_cmovznz_u32(out1: &mut u32, arg1: fiat_p256_u1, arg2: u32, arg3: u32) {
let x1: fiat_p256_u1 = (!(!arg1));
let x2: u32 = ((((((0x0 as fiat_p256_i2) - (x1 as fiat_p256_i2)) as fiat_p256_i1) as i64) & (0xffffffff as i64)) as u32);
let x3: u32 = ((x2 & arg3) | ((!x2) & arg2));
@@ -128,7 +164,7 @@ pub fn fiat_p256_cmovznz_u32(out1: &mut u32, arg1: fiat_p256_u1, arg2: u32, arg3
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_mul(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_mul(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) {
let x1: u32 = (arg1[1]);
let x2: u32 = (arg1[2]);
let x3: u32 = (arg1[3]);
@@ -1131,7 +1167,7 @@ pub fn fiat_p256_mul(out1: &mut fiat_p256_montgomery_domain_field_element, arg1:
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_square(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_square(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) {
let x1: u32 = (arg1[1]);
let x2: u32 = (arg1[2]);
let x3: u32 = (arg1[3]);
@@ -2135,7 +2171,7 @@ pub fn fiat_p256_square(out1: &mut fiat_p256_montgomery_domain_field_element, ar
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_add(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_add(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) {
let mut x1: u32 = 0;
let mut x2: fiat_p256_u1 = 0;
fiat_p256_addcarryx_u32(&mut x1, &mut x2, 0x0, (arg1[0]), (arg2[0]));
@@ -2223,7 +2259,7 @@ pub fn fiat_p256_add(out1: &mut fiat_p256_montgomery_domain_field_element, arg1:
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_sub(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_sub(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element, arg2: &fiat_p256_montgomery_domain_field_element) {
let mut x1: u32 = 0;
let mut x2: fiat_p256_u1 = 0;
fiat_p256_subborrowx_u32(&mut x1, &mut x2, 0x0, (arg1[0]), (arg2[0]));
@@ -2293,7 +2329,7 @@ pub fn fiat_p256_sub(out1: &mut fiat_p256_montgomery_domain_field_element, arg1:
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_opp(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_opp(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) {
let mut x1: u32 = 0;
let mut x2: fiat_p256_u1 = 0;
fiat_p256_subborrowx_u32(&mut x1, &mut x2, 0x0, (0x0 as u32), (arg1[0]));
@@ -2363,7 +2399,7 @@ pub fn fiat_p256_opp(out1: &mut fiat_p256_montgomery_domain_field_element, arg1:
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_from_montgomery(out1: &mut fiat_p256_non_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_from_montgomery(out1: &mut fiat_p256_non_montgomery_domain_field_element, arg1: &fiat_p256_montgomery_domain_field_element) {
let x1: u32 = (arg1[0]);
let mut x2: u32 = 0;
let mut x3: u32 = 0;
@@ -2898,7 +2934,7 @@ pub fn fiat_p256_from_montgomery(out1: &mut fiat_p256_non_montgomery_domain_fiel
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_to_montgomery(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_non_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_to_montgomery(out1: &mut fiat_p256_montgomery_domain_field_element, arg1: &fiat_p256_non_montgomery_domain_field_element) {
let x1: u32 = (arg1[1]);
let x2: u32 = (arg1[2]);
let x3: u32 = (arg1[3]);
@@ -3788,7 +3824,7 @@ pub fn fiat_p256_to_montgomery(out1: &mut fiat_p256_montgomery_domain_field_elem
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffff]
#[inline]
-pub fn fiat_p256_nonzero(out1: &mut u32, arg1: &[u32; 8]) -> () {
+pub fn fiat_p256_nonzero(out1: &mut u32, arg1: &[u32; 8]) {
let x1: u32 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | ((arg1[6]) | (arg1[7]))))))));
*out1 = x1;
}
@@ -3805,7 +3841,7 @@ pub fn fiat_p256_nonzero(out1: &mut u32, arg1: &[u32; 8]) -> () {
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
#[inline]
-pub fn fiat_p256_selectznz(out1: &mut [u32; 8], arg1: fiat_p256_u1, arg2: &[u32; 8], arg3: &[u32; 8]) -> () {
+pub fn fiat_p256_selectznz(out1: &mut [u32; 8], arg1: fiat_p256_u1, arg2: &[u32; 8], arg3: &[u32; 8]) {
let mut x1: u32 = 0;
fiat_p256_cmovznz_u32(&mut x1, arg1, (arg2[0]), (arg3[0]));
let mut x2: u32 = 0;
@@ -3844,7 +3880,7 @@ pub fn fiat_p256_selectznz(out1: &mut [u32; 8], arg1: fiat_p256_u1, arg2: &[u32;
/// 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]]
#[inline]
-pub fn fiat_p256_to_bytes(out1: &mut [u8; 32], arg1: &[u32; 8]) -> () {
+pub fn fiat_p256_to_bytes(out1: &mut [u8; 32], arg1: &[u32; 8]) {
let x1: u32 = (arg1[7]);
let x2: u32 = (arg1[6]);
let x3: u32 = (arg1[5]);
@@ -3948,7 +3984,7 @@ pub fn fiat_p256_to_bytes(out1: &mut [u8; 32], arg1: &[u32; 8]) -> () {
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
#[inline]
-pub fn fiat_p256_from_bytes(out1: &mut [u32; 8], arg1: &[u8; 32]) -> () {
+pub fn fiat_p256_from_bytes(out1: &mut [u32; 8], arg1: &[u8; 32]) {
let x1: u32 = (((arg1[31]) as u32) << 24);
let x2: u32 = (((arg1[30]) as u32) << 16);
let x3: u32 = (((arg1[29]) as u32) << 8);
@@ -4022,7 +4058,7 @@ pub fn fiat_p256_from_bytes(out1: &mut [u32; 8], arg1: &[u8; 32]) -> () {
/// 0 ≤ eval out1 < m
///
#[inline]
-pub fn fiat_p256_set_one(out1: &mut fiat_p256_montgomery_domain_field_element) -> () {
+pub fn fiat_p256_set_one(out1: &mut fiat_p256_montgomery_domain_field_element) {
out1[0] = (0x1 as u32);
out1[1] = (0x0 as u32);
out1[2] = (0x0 as u32);
@@ -4042,7 +4078,7 @@ pub fn fiat_p256_set_one(out1: &mut fiat_p256_montgomery_domain_field_element) -
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
#[inline]
-pub fn fiat_p256_msat(out1: &mut [u32; 9]) -> () {
+pub fn fiat_p256_msat(out1: &mut [u32; 9]) {
out1[0] = 0xffffffff;
out1[1] = 0xffffffff;
out1[2] = 0xffffffff;
@@ -4083,7 +4119,7 @@ pub fn fiat_p256_msat(out1: &mut [u32; 9]) -> () {
/// out4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
/// out5: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
#[inline]
-pub fn fiat_p256_divstep(out1: &mut u32, out2: &mut [u32; 9], out3: &mut [u32; 9], out4: &mut [u32; 8], out5: &mut [u32; 8], arg1: u32, arg2: &[u32; 9], arg3: &[u32; 9], arg4: &[u32; 8], arg5: &[u32; 8]) -> () {
+pub fn fiat_p256_divstep(out1: &mut u32, out2: &mut [u32; 9], out3: &mut [u32; 9], out4: &mut [u32; 8], out5: &mut [u32; 8], arg1: u32, arg2: &[u32; 9], arg3: &[u32; 9], arg4: &[u32; 8], arg5: &[u32; 8]) {
let mut x1: u32 = 0;
let mut x2: fiat_p256_u1 = 0;
fiat_p256_addcarryx_u32(&mut x1, &mut x2, 0x0, (!arg1), (0x1 as u32));
@@ -4500,7 +4536,7 @@ pub fn fiat_p256_divstep(out1: &mut u32, out2: &mut [u32; 9], out3: &mut [u32; 9
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
#[inline]
-pub fn fiat_p256_divstep_precomp(out1: &mut [u32; 8]) -> () {
+pub fn fiat_p256_divstep_precomp(out1: &mut [u32; 8]) {
out1[0] = 0xb8000000;
out1[1] = 0x67ffffff;
out1[2] = 0x38000000;
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-06 13:59:26 +0000