Regenerate field arithmetic

Signed-off-by: Arvind Mukund <[email protected]>

p521/src/arithmetic/field/p521_64.rs

@@ -1,8 +1,8 @@
 //! fiat-crypto output postprocessed by fiat-constify: <https://github.com/rustcrypto/utils>
-//! 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
+//! Autogenerated: './unsaturated_solinas' --lang Rust --inline p521 64 '(auto)' '2^521 - 1' carry_mul carry_square carry add sub opp carry_add carry_sub carry_opp relax selectznz to_bytes from_bytes
 //! curve description: p521
 //! machine_wordsize = 64 (from "64")
-//! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
+//! requested operations: carry_mul, carry_square, carry, add, sub, opp, carry_add, carry_sub, carry_opp, relax, selectznz, to_bytes, from_bytes
 //! n = 9 (from "(auto)")
 //! s-c = 2^521 - [(1, 1)] (from "2^521 - 1")
 //! tight_bounds_multiplier = 1 (from "")
@@ -104,13 +104,11 @@ pub const fn fiat_p521_subborrowx_u58(
     arg2: u64,
     arg3: u64,
 ) -> (u64, fiat_p521_u1) {
-    let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
+    let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128)
+        - (arg3 as i128)) as i64);
     let x2: fiat_p521_i1 = ((x1 >> 58) as fiat_p521_i1);
     let x3: u64 = (((x1 as i128) & (0x3ffffffffffffff as i128)) as u64);
-    (
-        x3,
-        (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1),
-    )
+    (x3, (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1))
 }
 /// The function fiat_p521_addcarryx_u57 is an addition with carry.
 ///
@@ -155,13 +153,11 @@ pub const fn fiat_p521_subborrowx_u57(
     arg2: u64,
     arg3: u64,
 ) -> (u64, fiat_p521_u1) {
-    let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
+    let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128)
+        - (arg3 as i128)) as i64);
     let x2: fiat_p521_i1 = ((x1 >> 57) as fiat_p521_i1);
     let x3: u64 = (((x1 as i128) & (0x1ffffffffffffff as i128)) as u64);
-    (
-        x3,
-        (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1),
-    )
+    (x3, (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1))
 }
 /// The function fiat_p521_cmovznz_u64 is a single-word conditional move.
 ///
@@ -177,8 +173,8 @@ pub const fn fiat_p521_subborrowx_u57(
 #[inline]
 pub const fn fiat_p521_cmovznz_u64(arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> 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 x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1)
+        as i128) & (0xffffffffffffffff as i128)) as u64);
     let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
     (x3)
 }
@@ -317,7 +313,17 @@ pub const fn fiat_p521_carry_mul(
     let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1);
     let x122: u64 = (x120 & 0x3ffffffffffffff);
     let x123: u64 = ((x121 as u64) + x98);
-    (fiat_p521_tight_field_element([x119, x122, x123, x101, x104, x107, x110, x113, x116]))
+    (fiat_p521_tight_field_element([
+        x119,
+        x122,
+        x123,
+        x101,
+        x104,
+        x107,
+        x110,
+        x113,
+        x116,
+    ]))
 }
 /// The function fiat_p521_carry_square squares a field element and reduces the result.
 ///
@@ -518,7 +524,9 @@ pub const fn fiat_p521_sub(
 ///   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 {
+pub const fn fiat_p521_opp(
+    arg1: &fiat_p521_tight_field_element,
+) -> fiat_p521_loose_field_element {
     let arg1 = &arg1.0;
     let x1: u64 = (0x7fffffffffffffe - (arg1[0]));
     let x2: u64 = (0x7fffffffffffffe - (arg1[1]));
@@ -531,6 +539,135 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo
     let x9: u64 = (0x3fffffffffffffe - (arg1[8]));
     (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9]))
 }
+/// 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 arg1 = &arg1.0;
+    let arg2 = &arg2.0;
+    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])));
+    let x4: u64 = ((x3 >> 58) + ((arg1[3]) + (arg2[3])));
+    let x5: u64 = ((x4 >> 58) + ((arg1[4]) + (arg2[4])));
+    let x6: u64 = ((x5 >> 58) + ((arg1[5]) + (arg2[5])));
+    let x7: u64 = ((x6 >> 58) + ((arg1[6]) + (arg2[6])));
+    let x8: u64 = ((x7 >> 58) + ((arg1[7]) + (arg2[7])));
+    let x9: u64 = ((x8 >> 58) + ((arg1[8]) + (arg2[8])));
+    let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57));
+    let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
+    let x12: u64 = (x10 & 0x3ffffffffffffff);
+    let x13: u64 = (x11 & 0x3ffffffffffffff);
+    let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
+    let x15: u64 = (x4 & 0x3ffffffffffffff);
+    let x16: u64 = (x5 & 0x3ffffffffffffff);
+    let x17: u64 = (x6 & 0x3ffffffffffffff);
+    let x18: u64 = (x7 & 0x3ffffffffffffff);
+    let x19: u64 = (x8 & 0x3ffffffffffffff);
+    let x20: u64 = (x9 & 0x1ffffffffffffff);
+    (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20]))
+}
+/// 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 arg1 = &arg1.0;
+    let arg2 = &arg2.0;
+    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])));
+    let x4: u64 = ((x3 >> 58) + ((0x7fffffffffffffe + (arg1[3])) - (arg2[3])));
+    let x5: u64 = ((x4 >> 58) + ((0x7fffffffffffffe + (arg1[4])) - (arg2[4])));
+    let x6: u64 = ((x5 >> 58) + ((0x7fffffffffffffe + (arg1[5])) - (arg2[5])));
+    let x7: u64 = ((x6 >> 58) + ((0x7fffffffffffffe + (arg1[6])) - (arg2[6])));
+    let x8: u64 = ((x7 >> 58) + ((0x7fffffffffffffe + (arg1[7])) - (arg2[7])));
+    let x9: u64 = ((x8 >> 58) + ((0x3fffffffffffffe + (arg1[8])) - (arg2[8])));
+    let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57));
+    let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
+    let x12: u64 = (x10 & 0x3ffffffffffffff);
+    let x13: u64 = (x11 & 0x3ffffffffffffff);
+    let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
+    let x15: u64 = (x4 & 0x3ffffffffffffff);
+    let x16: u64 = (x5 & 0x3ffffffffffffff);
+    let x17: u64 = (x6 & 0x3ffffffffffffff);
+    let x18: u64 = (x7 & 0x3ffffffffffffff);
+    let x19: u64 = (x8 & 0x3ffffffffffffff);
+    let x20: u64 = (x9 & 0x1ffffffffffffff);
+    (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20]))
+}
+/// 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 arg1 = &arg1.0;
+    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])));
+    let x4: u64 = ((((x3 >> 58) as fiat_p521_u1) as u64)
+        + (0x7fffffffffffffe - (arg1[3])));
+    let x5: u64 = ((((x4 >> 58) as fiat_p521_u1) as u64)
+        + (0x7fffffffffffffe - (arg1[4])));
+    let x6: u64 = ((((x5 >> 58) as fiat_p521_u1) as u64)
+        + (0x7fffffffffffffe - (arg1[5])));
+    let x7: u64 = ((((x6 >> 58) as fiat_p521_u1) as u64)
+        + (0x7fffffffffffffe - (arg1[6])));
+    let x8: u64 = ((((x7 >> 58) as fiat_p521_u1) as u64)
+        + (0x7fffffffffffffe - (arg1[7])));
+    let x9: u64 = ((((x8 >> 58) as fiat_p521_u1) as u64)
+        + (0x3fffffffffffffe - (arg1[8])));
+    let x10: u64 = ((x1 & 0x3ffffffffffffff) + (((x9 >> 57) as fiat_p521_u1) as u64));
+    let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
+    let x12: u64 = (x10 & 0x3ffffffffffffff);
+    let x13: u64 = (x11 & 0x3ffffffffffffff);
+    let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
+    let x15: u64 = (x4 & 0x3ffffffffffffff);
+    let x16: u64 = (x5 & 0x3ffffffffffffff);
+    let x17: u64 = (x6 & 0x3ffffffffffffff);
+    let x18: u64 = (x7 & 0x3ffffffffffffff);
+    let x19: u64 = (x8 & 0x3ffffffffffffff);
+    let x20: u64 = (x9 & 0x1ffffffffffffff);
+    (fiat_p521_tight_field_element([x12, x13, x14, x15, x16, x17, x18, x19, x20]))
+}
+/// 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 arg1 = &arg1.0;
+    let x1: u64 = (arg1[0]);
+    let x2: u64 = (arg1[1]);
+    let x3: u64 = (arg1[2]);
+    let x4: u64 = (arg1[3]);
+    let x5: u64 = (arg1[4]);
+    let x6: u64 = (arg1[5]);
+    let x7: u64 = (arg1[6]);
+    let x8: u64 = (arg1[7]);
+    let x9: u64 = (arg1[8]);
+    (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9]))
+}
 /// The function fiat_p521_selectznz is a multi-limb conditional select.
 ///
 /// Postconditions:
@@ -543,7 +680,11 @@ pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_lo
 /// 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] {
+pub const fn fiat_p521_selectznz(
+    arg1: fiat_p521_u1,
+    arg2: &[u64; 9],
+    arg3: &[u64; 9],
+) -> [u64; 9] {
     let mut x1: u64 = 0;
     let (x1) = fiat_p521_cmovznz_u64(arg1, (arg2[0]), (arg3[0]));
     let mut x2: u64 = 0;
@@ -989,24 +1130,4 @@ pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_elem
     let x141: u64 = (x1 + x140);
     (fiat_p521_tight_field_element([x74, x83, x92, x100, x108, x117, x126, x134, x141]))
 }
-/// 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 arg1 = &arg1.0;
-    let x1: u64 = (arg1[0]);
-    let x2: u64 = (arg1[1]);
-    let x3: u64 = (arg1[2]);
-    let x4: u64 = (arg1[3]);
-    let x5: u64 = (arg1[4]);
-    let x6: u64 = (arg1[5]);
-    let x7: u64 = (arg1[6]);
-    let x8: u64 = (arg1[7]);
-    let x9: u64 = (arg1[8]);
-    (fiat_p521_loose_field_element([x1, x2, x3, x4, x5, x6, x7, x8, x9]))
-}
+