vendor/fiat-crypto/src/p448_solinas_64.rs

   1 //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p448 64 8 '2^448 - 2^224 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
   2 //! curve description: p448
   3 //! machine_wordsize = 64 (from "64")
   4 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
   5 //! n = 8 (from "8")
   6 //! s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1")
   7 //! tight_bounds_multiplier = 1 (from "")
   8 //!
   9 //! Computed values:
  10 //!   carry_chain = [3, 7, 4, 0, 5, 1, 6, 2, 7, 3, 4, 0]
  11 //!   eval z = z[0] + (z[1] << 56) + (z[2] << 112) + (z[3] << 168) + (z[4] << 224) + (z[5] << 0x118) + (z[6] << 0x150) + (z[7] << 0x188)
  12 //!   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)
  13 //!   balance = [0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffc, 0x1fffffffffffffe, 0x1fffffffffffffe, 0x1fffffffffffffe]
  14
  15 #![allow(unused_parens)]
  16 #![allow(non_camel_case_types)]
  17
  18 pub type fiat_p448_u1 = u8;
  19 pub type fiat_p448_i1 = i8;
  20 pub type fiat_p448_u2 = u8;
  21 pub type fiat_p448_i2 = i8;
  22
  23 /* The type fiat_p448_loose_field_element is a field element with loose bounds. */
  24 /* Bounds: [[0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000], [0x0 ~> 0x300000000000000]] */
  25 pub type fiat_p448_loose_field_element = [u64; 8];
  26
  27 /* The type fiat_p448_tight_field_element is a field element with tight bounds. */
  28 /* Bounds: [[0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000], [0x0 ~> 0x100000000000000]] */
  29 pub type fiat_p448_tight_field_element = [u64; 8];
  30
  31
  32 /// The function fiat_p448_addcarryx_u56 is an addition with carry.
  33 ///
  34 /// Postconditions:
  35 ///   out1 = (arg1 + arg2 + arg3) mod 2^56
  36 ///   out2 = ⌊(arg1 + arg2 + arg3) / 2^56⌋
  37 ///
  38 /// Input Bounds:
  39 ///   arg1: [0x0 ~> 0x1]
  40 ///   arg2: [0x0 ~> 0xffffffffffffff]
  41 ///   arg3: [0x0 ~> 0xffffffffffffff]
  42 /// Output Bounds:
  43 ///   out1: [0x0 ~> 0xffffffffffffff]
  44 ///   out2: [0x0 ~> 0x1]
  45 #[inline]
  46 pub fn fiat_p448_addcarryx_u56(out1: &mut u64, out2: &mut fiat_p448_u1, arg1: fiat_p448_u1, arg2: u64, arg3: u64) -> () {
  47   let x1: u64 = (((arg1 as u64) + arg2) + arg3);
  48   let x2: u64 = (x1 & 0xffffffffffffff);
  49   let x3: fiat_p448_u1 = ((x1 >> 56) as fiat_p448_u1);
  50   *out1 = x2;
  51   *out2 = x3;
  52 }
  53
  54 /// The function fiat_p448_subborrowx_u56 is a subtraction with borrow.
  55 ///
  56 /// Postconditions:
  57 ///   out1 = (-arg1 + arg2 + -arg3) mod 2^56
  58 ///   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^56⌋
  59 ///
  60 /// Input Bounds:
  61 ///   arg1: [0x0 ~> 0x1]
  62 ///   arg2: [0x0 ~> 0xffffffffffffff]
  63 ///   arg3: [0x0 ~> 0xffffffffffffff]
  64 /// Output Bounds:
  65 ///   out1: [0x0 ~> 0xffffffffffffff]
  66 ///   out2: [0x0 ~> 0x1]
  67 #[inline]
  68 pub fn fiat_p448_subborrowx_u56(out1: &mut u64, out2: &mut fiat_p448_u1, arg1: fiat_p448_u1, arg2: u64, arg3: u64) -> () {
  69   let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
  70   let x2: fiat_p448_i1 = ((x1 >> 56) as fiat_p448_i1);
  71   let x3: u64 = (((x1 as i128) & (0xffffffffffffff as i128)) as u64);
  72   *out1 = x3;
  73   *out2 = (((0x0 as fiat_p448_i2) - (x2 as fiat_p448_i2)) as fiat_p448_u1);
  74 }
  75
  76 /// The function fiat_p448_cmovznz_u64 is a single-word conditional move.
  77 ///
  78 /// Postconditions:
  79 ///   out1 = (if arg1 = 0 then arg2 else arg3)
  80 ///
  81 /// Input Bounds:
  82 ///   arg1: [0x0 ~> 0x1]
  83 ///   arg2: [0x0 ~> 0xffffffffffffffff]
  84 ///   arg3: [0x0 ~> 0xffffffffffffffff]
  85 /// Output Bounds:
  86 ///   out1: [0x0 ~> 0xffffffffffffffff]
  87 #[inline]
  88 pub fn fiat_p448_cmovznz_u64(out1: &mut u64, arg1: fiat_p448_u1, arg2: u64, arg3: u64) -> () {
  89   let x1: fiat_p448_u1 = (!(!arg1));
  90   let x2: u64 = ((((((0x0 as fiat_p448_i2) - (x1 as fiat_p448_i2)) as fiat_p448_i1) as i128) & (0xffffffffffffffff as i128)) as u64);
  91   let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
  92   *out1 = x3;
  93 }
  94
  95 /// The function fiat_p448_carry_mul multiplies two field elements and reduces the result.
  96 ///
  97 /// Postconditions:
  98 ///   eval out1 mod m = (eval arg1 * eval arg2) mod m
  99 ///
 100 #[inline]
 101 pub fn fiat_p448_carry_mul(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element, arg2: &fiat_p448_loose_field_element) -> () {
 102   let x1: u128 = (((arg1[7]) as u128) * ((arg2[7]) as u128));
 103   let x2: u128 = (((arg1[7]) as u128) * ((arg2[6]) as u128));
 104   let x3: u128 = (((arg1[7]) as u128) * ((arg2[5]) as u128));
 105   let x4: u128 = (((arg1[6]) as u128) * ((arg2[7]) as u128));
 106   let x5: u128 = (((arg1[6]) as u128) * ((arg2[6]) as u128));
 107   let x6: u128 = (((arg1[5]) as u128) * ((arg2[7]) as u128));
 108   let x7: u128 = (((arg1[7]) as u128) * ((arg2[7]) as u128));
 109   let x8: u128 = (((arg1[7]) as u128) * ((arg2[6]) as u128));
 110   let x9: u128 = (((arg1[7]) as u128) * ((arg2[5]) as u128));
 111   let x10: u128 = (((arg1[6]) as u128) * ((arg2[7]) as u128));
 112   let x11: u128 = (((arg1[6]) as u128) * ((arg2[6]) as u128));
 113   let x12: u128 = (((arg1[5]) as u128) * ((arg2[7]) as u128));
 114   let x13: u128 = (((arg1[7]) as u128) * ((arg2[7]) as u128));
 115   let x14: u128 = (((arg1[7]) as u128) * ((arg2[6]) as u128));
 116   let x15: u128 = (((arg1[7]) as u128) * ((arg2[5]) as u128));
 117   let x16: u128 = (((arg1[7]) as u128) * ((arg2[4]) as u128));
 118   let x17: u128 = (((arg1[7]) as u128) * ((arg2[3]) as u128));
 119   let x18: u128 = (((arg1[7]) as u128) * ((arg2[2]) as u128));
 120   let x19: u128 = (((arg1[7]) as u128) * ((arg2[1]) as u128));
 121   let x20: u128 = (((arg1[6]) as u128) * ((arg2[7]) as u128));
 122   let x21: u128 = (((arg1[6]) as u128) * ((arg2[6]) as u128));
 123   let x22: u128 = (((arg1[6]) as u128) * ((arg2[5]) as u128));
 124   let x23: u128 = (((arg1[6]) as u128) * ((arg2[4]) as u128));
 125   let x24: u128 = (((arg1[6]) as u128) * ((arg2[3]) as u128));
 126   let x25: u128 = (((arg1[6]) as u128) * ((arg2[2]) as u128));
 127   let x26: u128 = (((arg1[5]) as u128) * ((arg2[7]) as u128));
 128   let x27: u128 = (((arg1[5]) as u128) * ((arg2[6]) as u128));
 129   let x28: u128 = (((arg1[5]) as u128) * ((arg2[5]) as u128));
 130   let x29: u128 = (((arg1[5]) as u128) * ((arg2[4]) as u128));
 131   let x30: u128 = (((arg1[5]) as u128) * ((arg2[3]) as u128));
 132   let x31: u128 = (((arg1[4]) as u128) * ((arg2[7]) as u128));
 133   let x32: u128 = (((arg1[4]) as u128) * ((arg2[6]) as u128));
 134   let x33: u128 = (((arg1[4]) as u128) * ((arg2[5]) as u128));
 135   let x34: u128 = (((arg1[4]) as u128) * ((arg2[4]) as u128));
 136   let x35: u128 = (((arg1[3]) as u128) * ((arg2[7]) as u128));
 137   let x36: u128 = (((arg1[3]) as u128) * ((arg2[6]) as u128));
 138   let x37: u128 = (((arg1[3]) as u128) * ((arg2[5]) as u128));
 139   let x38: u128 = (((arg1[2]) as u128) * ((arg2[7]) as u128));
 140   let x39: u128 = (((arg1[2]) as u128) * ((arg2[6]) as u128));
 141   let x40: u128 = (((arg1[1]) as u128) * ((arg2[7]) as u128));
 142   let x41: u128 = (((arg1[7]) as u128) * ((arg2[4]) as u128));
 143   let x42: u128 = (((arg1[7]) as u128) * ((arg2[3]) as u128));
 144   let x43: u128 = (((arg1[7]) as u128) * ((arg2[2]) as u128));
 145   let x44: u128 = (((arg1[7]) as u128) * ((arg2[1]) as u128));
 146   let x45: u128 = (((arg1[6]) as u128) * ((arg2[5]) as u128));
 147   let x46: u128 = (((arg1[6]) as u128) * ((arg2[4]) as u128));
 148   let x47: u128 = (((arg1[6]) as u128) * ((arg2[3]) as u128));
 149   let x48: u128 = (((arg1[6]) as u128) * ((arg2[2]) as u128));
 150   let x49: u128 = (((arg1[5]) as u128) * ((arg2[6]) as u128));
 151   let x50: u128 = (((arg1[5]) as u128) * ((arg2[5]) as u128));
 152   let x51: u128 = (((arg1[5]) as u128) * ((arg2[4]) as u128));
 153   let x52: u128 = (((arg1[5]) as u128) * ((arg2[3]) as u128));
 154   let x53: u128 = (((arg1[4]) as u128) * ((arg2[7]) as u128));
 155   let x54: u128 = (((arg1[4]) as u128) * ((arg2[6]) as u128));
 156   let x55: u128 = (((arg1[4]) as u128) * ((arg2[5]) as u128));
 157   let x56: u128 = (((arg1[4]) as u128) * ((arg2[4]) as u128));
 158   let x57: u128 = (((arg1[3]) as u128) * ((arg2[7]) as u128));
 159   let x58: u128 = (((arg1[3]) as u128) * ((arg2[6]) as u128));
 160   let x59: u128 = (((arg1[3]) as u128) * ((arg2[5]) as u128));
 161   let x60: u128 = (((arg1[2]) as u128) * ((arg2[7]) as u128));
 162   let x61: u128 = (((arg1[2]) as u128) * ((arg2[6]) as u128));
 163   let x62: u128 = (((arg1[1]) as u128) * ((arg2[7]) as u128));
 164   let x63: u128 = (((arg1[7]) as u128) * ((arg2[0]) as u128));
 165   let x64: u128 = (((arg1[6]) as u128) * ((arg2[1]) as u128));
 166   let x65: u128 = (((arg1[6]) as u128) * ((arg2[0]) as u128));
 167   let x66: u128 = (((arg1[5]) as u128) * ((arg2[2]) as u128));
 168   let x67: u128 = (((arg1[5]) as u128) * ((arg2[1]) as u128));
 169   let x68: u128 = (((arg1[5]) as u128) * ((arg2[0]) as u128));
 170   let x69: u128 = (((arg1[4]) as u128) * ((arg2[3]) as u128));
 171   let x70: u128 = (((arg1[4]) as u128) * ((arg2[2]) as u128));
 172   let x71: u128 = (((arg1[4]) as u128) * ((arg2[1]) as u128));
 173   let x72: u128 = (((arg1[4]) as u128) * ((arg2[0]) as u128));
 174   let x73: u128 = (((arg1[3]) as u128) * ((arg2[4]) as u128));
 175   let x74: u128 = (((arg1[3]) as u128) * ((arg2[3]) as u128));
 176   let x75: u128 = (((arg1[3]) as u128) * ((arg2[2]) as u128));
 177   let x76: u128 = (((arg1[3]) as u128) * ((arg2[1]) as u128));
 178   let x77: u128 = (((arg1[3]) as u128) * ((arg2[0]) as u128));
 179   let x78: u128 = (((arg1[2]) as u128) * ((arg2[5]) as u128));
 180   let x79: u128 = (((arg1[2]) as u128) * ((arg2[4]) as u128));
 181   let x80: u128 = (((arg1[2]) as u128) * ((arg2[3]) as u128));
 182   let x81: u128 = (((arg1[2]) as u128) * ((arg2[2]) as u128));
 183   let x82: u128 = (((arg1[2]) as u128) * ((arg2[1]) as u128));
 184   let x83: u128 = (((arg1[2]) as u128) * ((arg2[0]) as u128));
 185   let x84: u128 = (((arg1[1]) as u128) * ((arg2[6]) as u128));
 186   let x85: u128 = (((arg1[1]) as u128) * ((arg2[5]) as u128));
 187   let x86: u128 = (((arg1[1]) as u128) * ((arg2[4]) as u128));
 188   let x87: u128 = (((arg1[1]) as u128) * ((arg2[3]) as u128));
 189   let x88: u128 = (((arg1[1]) as u128) * ((arg2[2]) as u128));
 190   let x89: u128 = (((arg1[1]) as u128) * ((arg2[1]) as u128));
 191   let x90: u128 = (((arg1[1]) as u128) * ((arg2[0]) as u128));
 192   let x91: u128 = (((arg1[0]) as u128) * ((arg2[7]) as u128));
 193   let x92: u128 = (((arg1[0]) as u128) * ((arg2[6]) as u128));
 194   let x93: u128 = (((arg1[0]) as u128) * ((arg2[5]) as u128));
 195   let x94: u128 = (((arg1[0]) as u128) * ((arg2[4]) as u128));
 196   let x95: u128 = (((arg1[0]) as u128) * ((arg2[3]) as u128));
 197   let x96: u128 = (((arg1[0]) as u128) * ((arg2[2]) as u128));
 198   let x97: u128 = (((arg1[0]) as u128) * ((arg2[1]) as u128));
 199   let x98: u128 = (((arg1[0]) as u128) * ((arg2[0]) as u128));
 200   let x99: u128 = (x95 + (x88 + (x82 + (x77 + (x31 + (x27 + (x22 + x16)))))));
 201   let x100: u64 = ((x99 >> 56) as u64);
 202   let x101: u64 = ((x99 & (0xffffffffffffff as u128)) as u64);
 203   let x102: u128 = (x91 + (x84 + (x78 + (x73 + (x69 + (x66 + (x64 + (x63 + (x53 + (x49 + (x45 + x41)))))))))));
 204   let x103: u128 = (x92 + (x85 + (x79 + (x74 + (x70 + (x67 + (x65 + (x57 + (x54 + (x50 + (x46 + (x42 + (x13 + x7)))))))))))));
 205   let x104: u128 = (x93 + (x86 + (x80 + (x75 + (x71 + (x68 + (x60 + (x58 + (x55 + (x51 + (x47 + (x43 + (x20 + (x14 + (x10 + x8)))))))))))))));
 206   let x105: u128 = (x94 + (x87 + (x81 + (x76 + (x72 + (x62 + (x61 + (x59 + (x56 + (x52 + (x48 + (x44 + (x26 + (x21 + (x15 + (x12 + (x11 + x9)))))))))))))))));
 207   let x106: u128 = (x96 + (x89 + (x83 + (x35 + (x32 + (x28 + (x23 + (x17 + x1))))))));
 208   let x107: u128 = (x97 + (x90 + (x38 + (x36 + (x33 + (x29 + (x24 + (x18 + (x4 + x2)))))))));
 209   let x108: u128 = (x98 + (x40 + (x39 + (x37 + (x34 + (x30 + (x25 + (x19 + (x6 + (x5 + x3))))))))));
 210   let x109: u128 = ((x100 as u128) + x105);
 211   let x110: u64 = ((x102 >> 56) as u64);
 212   let x111: u64 = ((x102 & (0xffffffffffffff as u128)) as u64);
 213   let x112: u128 = (x109 + (x110 as u128));
 214   let x113: u64 = ((x112 >> 56) as u64);
 215   let x114: u64 = ((x112 & (0xffffffffffffff as u128)) as u64);
 216   let x115: u128 = (x108 + (x110 as u128));
 217   let x116: u128 = ((x113 as u128) + x104);
 218   let x117: u64 = ((x115 >> 56) as u64);
 219   let x118: u64 = ((x115 & (0xffffffffffffff as u128)) as u64);
 220   let x119: u128 = ((x117 as u128) + x107);
 221   let x120: u64 = ((x116 >> 56) as u64);
 222   let x121: u64 = ((x116 & (0xffffffffffffff as u128)) as u64);
 223   let x122: u128 = ((x120 as u128) + x103);
 224   let x123: u64 = ((x119 >> 56) as u64);
 225   let x124: u64 = ((x119 & (0xffffffffffffff as u128)) as u64);
 226   let x125: u128 = ((x123 as u128) + x106);
 227   let x126: u64 = ((x122 >> 56) as u64);
 228   let x127: u64 = ((x122 & (0xffffffffffffff as u128)) as u64);
 229   let x128: u64 = (x126 + x111);
 230   let x129: u64 = ((x125 >> 56) as u64);
 231   let x130: u64 = ((x125 & (0xffffffffffffff as u128)) as u64);
 232   let x131: u64 = (x129 + x101);
 233   let x132: u64 = (x128 >> 56);
 234   let x133: u64 = (x128 & 0xffffffffffffff);
 235   let x134: u64 = (x131 >> 56);
 236   let x135: u64 = (x131 & 0xffffffffffffff);
 237   let x136: u64 = (x114 + x132);
 238   let x137: u64 = (x118 + x132);
 239   let x138: u64 = (x134 + x136);
 240   let x139: fiat_p448_u1 = ((x138 >> 56) as fiat_p448_u1);
 241   let x140: u64 = (x138 & 0xffffffffffffff);
 242   let x141: u64 = ((x139 as u64) + x121);
 243   let x142: fiat_p448_u1 = ((x137 >> 56) as fiat_p448_u1);
 244   let x143: u64 = (x137 & 0xffffffffffffff);
 245   let x144: u64 = ((x142 as u64) + x124);
 246   out1[0] = x143;
 247   out1[1] = x144;
 248   out1[2] = x130;
 249   out1[3] = x135;
 250   out1[4] = x140;
 251   out1[5] = x141;
 252   out1[6] = x127;
 253   out1[7] = x133;
 254 }
 255
 256 /// The function fiat_p448_carry_square squares a field element and reduces the result.
 257 ///
 258 /// Postconditions:
 259 ///   eval out1 mod m = (eval arg1 * eval arg1) mod m
 260 ///
 261 #[inline]
 262 pub fn fiat_p448_carry_square(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element) -> () {
 263   let x1: u64 = (arg1[7]);
 264   let x2: u64 = (arg1[7]);
 265   let x3: u64 = (x1 * 0x2);
 266   let x4: u64 = (x2 * 0x2);
 267   let x5: u64 = ((arg1[7]) * 0x2);
 268   let x6: u64 = (arg1[6]);
 269   let x7: u64 = (arg1[6]);
 270   let x8: u64 = (x6 * 0x2);
 271   let x9: u64 = (x7 * 0x2);
 272   let x10: u64 = ((arg1[6]) * 0x2);
 273   let x11: u64 = (arg1[5]);
 274   let x12: u64 = (arg1[5]);
 275   let x13: u64 = (x11 * 0x2);
 276   let x14: u64 = (x12 * 0x2);
 277   let x15: u64 = ((arg1[5]) * 0x2);
 278   let x16: u64 = (arg1[4]);
 279   let x17: u64 = (arg1[4]);
 280   let x18: u64 = ((arg1[4]) * 0x2);
 281   let x19: u64 = ((arg1[3]) * 0x2);
 282   let x20: u64 = ((arg1[2]) * 0x2);
 283   let x21: u64 = ((arg1[1]) * 0x2);
 284   let x22: u128 = (((arg1[7]) as u128) * (x1 as u128));
 285   let x23: u128 = (((arg1[6]) as u128) * (x3 as u128));
 286   let x24: u128 = (((arg1[6]) as u128) * (x6 as u128));
 287   let x25: u128 = (((arg1[5]) as u128) * (x3 as u128));
 288   let x26: u128 = (((arg1[7]) as u128) * (x1 as u128));
 289   let x27: u128 = (((arg1[6]) as u128) * (x3 as u128));
 290   let x28: u128 = (((arg1[6]) as u128) * (x6 as u128));
 291   let x29: u128 = (((arg1[5]) as u128) * (x3 as u128));
 292   let x30: u128 = (((arg1[7]) as u128) * (x2 as u128));
 293   let x31: u128 = (((arg1[6]) as u128) * (x4 as u128));
 294   let x32: u128 = (((arg1[6]) as u128) * (x7 as u128));
 295   let x33: u128 = (((arg1[5]) as u128) * (x4 as u128));
 296   let x34: u128 = (((arg1[5]) as u128) * (x9 as u128));
 297   let x35: u128 = (((arg1[5]) as u128) * (x8 as u128));
 298   let x36: u128 = (((arg1[5]) as u128) * (x12 as u128));
 299   let x37: u128 = (((arg1[5]) as u128) * (x11 as u128));
 300   let x38: u128 = (((arg1[4]) as u128) * (x4 as u128));
 301   let x39: u128 = (((arg1[4]) as u128) * (x3 as u128));
 302   let x40: u128 = (((arg1[4]) as u128) * (x9 as u128));
 303   let x41: u128 = (((arg1[4]) as u128) * (x8 as u128));
 304   let x42: u128 = (((arg1[4]) as u128) * (x14 as u128));
 305   let x43: u128 = (((arg1[4]) as u128) * (x13 as u128));
 306   let x44: u128 = (((arg1[4]) as u128) * (x17 as u128));
 307   let x45: u128 = (((arg1[4]) as u128) * (x16 as u128));
 308   let x46: u128 = (((arg1[3]) as u128) * (x4 as u128));
 309   let x47: u128 = (((arg1[3]) as u128) * (x3 as u128));
 310   let x48: u128 = (((arg1[3]) as u128) * (x9 as u128));
 311   let x49: u128 = (((arg1[3]) as u128) * (x8 as u128));
 312   let x50: u128 = (((arg1[3]) as u128) * (x14 as u128));
 313   let x51: u128 = (((arg1[3]) as u128) * (x13 as u128));
 314   let x52: u128 = (((arg1[3]) as u128) * (x18 as u128));
 315   let x53: u128 = (((arg1[3]) as u128) * ((arg1[3]) as u128));
 316   let x54: u128 = (((arg1[2]) as u128) * (x4 as u128));
 317   let x55: u128 = (((arg1[2]) as u128) * (x3 as u128));
 318   let x56: u128 = (((arg1[2]) as u128) * (x9 as u128));
 319   let x57: u128 = (((arg1[2]) as u128) * (x8 as u128));
 320   let x58: u128 = (((arg1[2]) as u128) * (x15 as u128));
 321   let x59: u128 = (((arg1[2]) as u128) * (x18 as u128));
 322   let x60: u128 = (((arg1[2]) as u128) * (x19 as u128));
 323   let x61: u128 = (((arg1[2]) as u128) * ((arg1[2]) as u128));
 324   let x62: u128 = (((arg1[1]) as u128) * (x4 as u128));
 325   let x63: u128 = (((arg1[1]) as u128) * (x3 as u128));
 326   let x64: u128 = (((arg1[1]) as u128) * (x10 as u128));
 327   let x65: u128 = (((arg1[1]) as u128) * (x15 as u128));
 328   let x66: u128 = (((arg1[1]) as u128) * (x18 as u128));
 329   let x67: u128 = (((arg1[1]) as u128) * (x19 as u128));
 330   let x68: u128 = (((arg1[1]) as u128) * (x20 as u128));
 331   let x69: u128 = (((arg1[1]) as u128) * ((arg1[1]) as u128));
 332   let x70: u128 = (((arg1[0]) as u128) * (x5 as u128));
 333   let x71: u128 = (((arg1[0]) as u128) * (x10 as u128));
 334   let x72: u128 = (((arg1[0]) as u128) * (x15 as u128));
 335   let x73: u128 = (((arg1[0]) as u128) * (x18 as u128));
 336   let x74: u128 = (((arg1[0]) as u128) * (x19 as u128));
 337   let x75: u128 = (((arg1[0]) as u128) * (x20 as u128));
 338   let x76: u128 = (((arg1[0]) as u128) * (x21 as u128));
 339   let x77: u128 = (((arg1[0]) as u128) * ((arg1[0]) as u128));
 340   let x78: u128 = (x74 + (x68 + (x38 + x34)));
 341   let x79: u64 = ((x78 >> 56) as u64);
 342   let x80: u64 = ((x78 & (0xffffffffffffff as u128)) as u64);
 343   let x81: u128 = (x70 + (x64 + (x58 + (x52 + (x39 + x35)))));
 344   let x82: u128 = (x71 + (x65 + (x59 + (x53 + (x47 + (x41 + (x37 + (x30 + x26))))))));
 345   let x83: u128 = (x72 + (x66 + (x60 + (x55 + (x49 + (x43 + (x31 + x27)))))));
 346   let x84: u128 = (x73 + (x67 + (x63 + (x61 + (x57 + (x51 + (x45 + (x33 + (x32 + (x29 + x28))))))))));
 347   let x85: u128 = (x75 + (x69 + (x46 + (x40 + (x36 + x22)))));
 348   let x86: u128 = (x76 + (x54 + (x48 + (x42 + x23))));
 349   let x87: u128 = (x77 + (x62 + (x56 + (x50 + (x44 + (x25 + x24))))));
 350   let x88: u128 = ((x79 as u128) + x84);
 351   let x89: u64 = ((x81 >> 56) as u64);
 352   let x90: u64 = ((x81 & (0xffffffffffffff as u128)) as u64);
 353   let x91: u128 = (x88 + (x89 as u128));
 354   let x92: u64 = ((x91 >> 56) as u64);
 355   let x93: u64 = ((x91 & (0xffffffffffffff as u128)) as u64);
 356   let x94: u128 = (x87 + (x89 as u128));
 357   let x95: u128 = ((x92 as u128) + x83);
 358   let x96: u64 = ((x94 >> 56) as u64);
 359   let x97: u64 = ((x94 & (0xffffffffffffff as u128)) as u64);
 360   let x98: u128 = ((x96 as u128) + x86);
 361   let x99: u64 = ((x95 >> 56) as u64);
 362   let x100: u64 = ((x95 & (0xffffffffffffff as u128)) as u64);
 363   let x101: u128 = ((x99 as u128) + x82);
 364   let x102: u64 = ((x98 >> 56) as u64);
 365   let x103: u64 = ((x98 & (0xffffffffffffff as u128)) as u64);
 366   let x104: u128 = ((x102 as u128) + x85);
 367   let x105: u64 = ((x101 >> 56) as u64);
 368   let x106: u64 = ((x101 & (0xffffffffffffff as u128)) as u64);
 369   let x107: u64 = (x105 + x90);
 370   let x108: u64 = ((x104 >> 56) as u64);
 371   let x109: u64 = ((x104 & (0xffffffffffffff as u128)) as u64);
 372   let x110: u64 = (x108 + x80);
 373   let x111: u64 = (x107 >> 56);
 374   let x112: u64 = (x107 & 0xffffffffffffff);
 375   let x113: u64 = (x110 >> 56);
 376   let x114: u64 = (x110 & 0xffffffffffffff);
 377   let x115: u64 = (x93 + x111);
 378   let x116: u64 = (x97 + x111);
 379   let x117: u64 = (x113 + x115);
 380   let x118: fiat_p448_u1 = ((x117 >> 56) as fiat_p448_u1);
 381   let x119: u64 = (x117 & 0xffffffffffffff);
 382   let x120: u64 = ((x118 as u64) + x100);
 383   let x121: fiat_p448_u1 = ((x116 >> 56) as fiat_p448_u1);
 384   let x122: u64 = (x116 & 0xffffffffffffff);
 385   let x123: u64 = ((x121 as u64) + x103);
 386   out1[0] = x122;
 387   out1[1] = x123;
 388   out1[2] = x109;
 389   out1[3] = x114;
 390   out1[4] = x119;
 391   out1[5] = x120;
 392   out1[6] = x106;
 393   out1[7] = x112;
 394 }
 395
 396 /// The function fiat_p448_carry reduces a field element.
 397 ///
 398 /// Postconditions:
 399 ///   eval out1 mod m = eval arg1 mod m
 400 ///
 401 #[inline]
 402 pub fn fiat_p448_carry(out1: &mut fiat_p448_tight_field_element, arg1: &fiat_p448_loose_field_element) -> () {
 403   let x1: u64 = (arg1[3]);
 404   let x2: u64 = (arg1[7]);
 405   let x3: u64 = (x2 >> 56);
 406   let x4: u64 = (((x1 >> 56) + (arg1[4])) + x3);
 407   let x5: u64 = ((arg1[0]) + x3);
 408   let x6: u64 = ((x4 >> 56) + (arg1[5]));
 409   let x7: u64 = ((x5 >> 56) + (arg1[1]));
 410   let x8: u64 = ((x6 >> 56) + (arg1[6]));
 411   let x9: u64 = ((x7 >> 56) + (arg1[2]));
 412   let x10: u64 = ((x8 >> 56) + (x2 & 0xffffffffffffff));
 413   let x11: u64 = ((x9 >> 56) + (x1 & 0xffffffffffffff));
 414   let x12: fiat_p448_u1 = ((x10 >> 56) as fiat_p448_u1);
 415   let x13: u64 = ((x5 & 0xffffffffffffff) + (x12 as u64));
 416   let x14: u64 = ((((x11 >> 56) as fiat_p448_u1) as u64) + ((x4 & 0xffffffffffffff) + (x12 as u64)));
 417   let x15: u64 = (x13 & 0xffffffffffffff);
 418   let x16: u64 = ((((x13 >> 56) as fiat_p448_u1) as u64) + (x7 & 0xffffffffffffff));
 419   let x17: u64 = (x9 & 0xffffffffffffff);
 420   let x18: u64 = (x11 & 0xffffffffffffff);
 421   let x19: u64 = (x14 & 0xffffffffffffff);
 422   let x20: u64 = ((((x14 >> 56) as fiat_p448_u1) as u64) + (x6 & 0xffffffffffffff));
 423   let x21: u64 = (x8 & 0xffffffffffffff);
 424   let x22: u64 = (x10 & 0xffffffffffffff);
 425   out1[0] = x15;
 426   out1[1] = x16;
 427   out1[2] = x17;
 428   out1[3] = x18;
 429   out1[4] = x19;
 430   out1[5] = x20;
 431   out1[6] = x21;
 432   out1[7] = x22;
 433 }
 434
 435 /// The function fiat_p448_add adds two field elements.
 436 ///
 437 /// Postconditions:
 438 ///   eval out1 mod m = (eval arg1 + eval arg2) mod m
 439 ///
 440 #[inline]
 441 pub fn fiat_p448_add(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element, arg2: &fiat_p448_tight_field_element) -> () {
 442   let x1: u64 = ((arg1[0]) + (arg2[0]));
 443   let x2: u64 = ((arg1[1]) + (arg2[1]));
 444   let x3: u64 = ((arg1[2]) + (arg2[2]));
 445   let x4: u64 = ((arg1[3]) + (arg2[3]));
 446   let x5: u64 = ((arg1[4]) + (arg2[4]));
 447   let x6: u64 = ((arg1[5]) + (arg2[5]));
 448   let x7: u64 = ((arg1[6]) + (arg2[6]));
 449   let x8: u64 = ((arg1[7]) + (arg2[7]));
 450   out1[0] = x1;
 451   out1[1] = x2;
 452   out1[2] = x3;
 453   out1[3] = x4;
 454   out1[4] = x5;
 455   out1[5] = x6;
 456   out1[6] = x7;
 457   out1[7] = x8;
 458 }
 459
 460 /// The function fiat_p448_sub subtracts two field elements.
 461 ///
 462 /// Postconditions:
 463 ///   eval out1 mod m = (eval arg1 - eval arg2) mod m
 464 ///
 465 #[inline]
 466 pub fn fiat_p448_sub(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element, arg2: &fiat_p448_tight_field_element) -> () {
 467   let x1: u64 = ((0x1fffffffffffffe + (arg1[0])) - (arg2[0]));
 468   let x2: u64 = ((0x1fffffffffffffe + (arg1[1])) - (arg2[1]));
 469   let x3: u64 = ((0x1fffffffffffffe + (arg1[2])) - (arg2[2]));
 470   let x4: u64 = ((0x1fffffffffffffe + (arg1[3])) - (arg2[3]));
 471   let x5: u64 = ((0x1fffffffffffffc + (arg1[4])) - (arg2[4]));
 472   let x6: u64 = ((0x1fffffffffffffe + (arg1[5])) - (arg2[5]));
 473   let x7: u64 = ((0x1fffffffffffffe + (arg1[6])) - (arg2[6]));
 474   let x8: u64 = ((0x1fffffffffffffe + (arg1[7])) - (arg2[7]));
 475   out1[0] = x1;
 476   out1[1] = x2;
 477   out1[2] = x3;
 478   out1[3] = x4;
 479   out1[4] = x5;
 480   out1[5] = x6;
 481   out1[6] = x7;
 482   out1[7] = x8;
 483 }
 484
 485 /// The function fiat_p448_opp negates a field element.
 486 ///
 487 /// Postconditions:
 488 ///   eval out1 mod m = -eval arg1 mod m
 489 ///
 490 #[inline]
 491 pub fn fiat_p448_opp(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element) -> () {
 492   let x1: u64 = (0x1fffffffffffffe - (arg1[0]));
 493   let x2: u64 = (0x1fffffffffffffe - (arg1[1]));
 494   let x3: u64 = (0x1fffffffffffffe - (arg1[2]));
 495   let x4: u64 = (0x1fffffffffffffe - (arg1[3]));
 496   let x5: u64 = (0x1fffffffffffffc - (arg1[4]));
 497   let x6: u64 = (0x1fffffffffffffe - (arg1[5]));
 498   let x7: u64 = (0x1fffffffffffffe - (arg1[6]));
 499   let x8: u64 = (0x1fffffffffffffe - (arg1[7]));
 500   out1[0] = x1;
 501   out1[1] = x2;
 502   out1[2] = x3;
 503   out1[3] = x4;
 504   out1[4] = x5;
 505   out1[5] = x6;
 506   out1[6] = x7;
 507   out1[7] = x8;
 508 }
 509
 510 /// The function fiat_p448_selectznz is a multi-limb conditional select.
 511 ///
 512 /// Postconditions:
 513 ///   out1 = (if arg1 = 0 then arg2 else arg3)
 514 ///
 515 /// Input Bounds:
 516 ///   arg1: [0x0 ~> 0x1]
 517 ///   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 518 ///   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 519 /// Output Bounds:
 520 ///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 521 #[inline]
 522 pub fn fiat_p448_selectznz(out1: &mut [u64; 8], arg1: fiat_p448_u1, arg2: &[u64; 8], arg3: &[u64; 8]) -> () {
 523   let mut x1: u64 = 0;
 524   fiat_p448_cmovznz_u64(&mut x1, arg1, (arg2[0]), (arg3[0]));
 525   let mut x2: u64 = 0;
 526   fiat_p448_cmovznz_u64(&mut x2, arg1, (arg2[1]), (arg3[1]));
 527   let mut x3: u64 = 0;
 528   fiat_p448_cmovznz_u64(&mut x3, arg1, (arg2[2]), (arg3[2]));
 529   let mut x4: u64 = 0;
 530   fiat_p448_cmovznz_u64(&mut x4, arg1, (arg2[3]), (arg3[3]));
 531   let mut x5: u64 = 0;
 532   fiat_p448_cmovznz_u64(&mut x5, arg1, (arg2[4]), (arg3[4]));
 533   let mut x6: u64 = 0;
 534   fiat_p448_cmovznz_u64(&mut x6, arg1, (arg2[5]), (arg3[5]));
 535   let mut x7: u64 = 0;
 536   fiat_p448_cmovznz_u64(&mut x7, arg1, (arg2[6]), (arg3[6]));
 537   let mut x8: u64 = 0;
 538   fiat_p448_cmovznz_u64(&mut x8, arg1, (arg2[7]), (arg3[7]));
 539   out1[0] = x1;
 540   out1[1] = x2;
 541   out1[2] = x3;
 542   out1[3] = x4;
 543   out1[4] = x5;
 544   out1[5] = x6;
 545   out1[6] = x7;
 546   out1[7] = x8;
 547 }
 548
 549 /// The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order.
 550 ///
 551 /// Postconditions:
 552 ///   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55]
 553 ///
 554 /// Output Bounds:
 555 ///   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]]
 556 #[inline]
 557 pub fn fiat_p448_to_bytes(out1: &mut [u8; 56], arg1: &fiat_p448_tight_field_element) -> () {
 558   let mut x1: u64 = 0;
 559   let mut x2: fiat_p448_u1 = 0;
 560   fiat_p448_subborrowx_u56(&mut x1, &mut x2, 0x0, (arg1[0]), 0xffffffffffffff);
 561   let mut x3: u64 = 0;
 562   let mut x4: fiat_p448_u1 = 0;
 563   fiat_p448_subborrowx_u56(&mut x3, &mut x4, x2, (arg1[1]), 0xffffffffffffff);
 564   let mut x5: u64 = 0;
 565   let mut x6: fiat_p448_u1 = 0;
 566   fiat_p448_subborrowx_u56(&mut x5, &mut x6, x4, (arg1[2]), 0xffffffffffffff);
 567   let mut x7: u64 = 0;
 568   let mut x8: fiat_p448_u1 = 0;
 569   fiat_p448_subborrowx_u56(&mut x7, &mut x8, x6, (arg1[3]), 0xffffffffffffff);
 570   let mut x9: u64 = 0;
 571   let mut x10: fiat_p448_u1 = 0;
 572   fiat_p448_subborrowx_u56(&mut x9, &mut x10, x8, (arg1[4]), 0xfffffffffffffe);
 573   let mut x11: u64 = 0;
 574   let mut x12: fiat_p448_u1 = 0;
 575   fiat_p448_subborrowx_u56(&mut x11, &mut x12, x10, (arg1[5]), 0xffffffffffffff);
 576   let mut x13: u64 = 0;
 577   let mut x14: fiat_p448_u1 = 0;
 578   fiat_p448_subborrowx_u56(&mut x13, &mut x14, x12, (arg1[6]), 0xffffffffffffff);
 579   let mut x15: u64 = 0;
 580   let mut x16: fiat_p448_u1 = 0;
 581   fiat_p448_subborrowx_u56(&mut x15, &mut x16, x14, (arg1[7]), 0xffffffffffffff);
 582   let mut x17: u64 = 0;
 583   fiat_p448_cmovznz_u64(&mut x17, x16, (0x0 as u64), 0xffffffffffffffff);
 584   let mut x18: u64 = 0;
 585   let mut x19: fiat_p448_u1 = 0;
 586   fiat_p448_addcarryx_u56(&mut x18, &mut x19, 0x0, x1, (x17 & 0xffffffffffffff));
 587   let mut x20: u64 = 0;
 588   let mut x21: fiat_p448_u1 = 0;
 589   fiat_p448_addcarryx_u56(&mut x20, &mut x21, x19, x3, (x17 & 0xffffffffffffff));
 590   let mut x22: u64 = 0;
 591   let mut x23: fiat_p448_u1 = 0;
 592   fiat_p448_addcarryx_u56(&mut x22, &mut x23, x21, x5, (x17 & 0xffffffffffffff));
 593   let mut x24: u64 = 0;
 594   let mut x25: fiat_p448_u1 = 0;
 595   fiat_p448_addcarryx_u56(&mut x24, &mut x25, x23, x7, (x17 & 0xffffffffffffff));
 596   let mut x26: u64 = 0;
 597   let mut x27: fiat_p448_u1 = 0;
 598   fiat_p448_addcarryx_u56(&mut x26, &mut x27, x25, x9, (x17 & 0xfffffffffffffe));
 599   let mut x28: u64 = 0;
 600   let mut x29: fiat_p448_u1 = 0;
 601   fiat_p448_addcarryx_u56(&mut x28, &mut x29, x27, x11, (x17 & 0xffffffffffffff));
 602   let mut x30: u64 = 0;
 603   let mut x31: fiat_p448_u1 = 0;
 604   fiat_p448_addcarryx_u56(&mut x30, &mut x31, x29, x13, (x17 & 0xffffffffffffff));
 605   let mut x32: u64 = 0;
 606   let mut x33: fiat_p448_u1 = 0;
 607   fiat_p448_addcarryx_u56(&mut x32, &mut x33, x31, x15, (x17 & 0xffffffffffffff));
 608   let x34: u8 = ((x18 & (0xff as u64)) as u8);
 609   let x35: u64 = (x18 >> 8);
 610   let x36: u8 = ((x35 & (0xff as u64)) as u8);
 611   let x37: u64 = (x35 >> 8);
 612   let x38: u8 = ((x37 & (0xff as u64)) as u8);
 613   let x39: u64 = (x37 >> 8);
 614   let x40: u8 = ((x39 & (0xff as u64)) as u8);
 615   let x41: u64 = (x39 >> 8);
 616   let x42: u8 = ((x41 & (0xff as u64)) as u8);
 617   let x43: u64 = (x41 >> 8);
 618   let x44: u8 = ((x43 & (0xff as u64)) as u8);
 619   let x45: u8 = ((x43 >> 8) as u8);
 620   let x46: u8 = ((x20 & (0xff as u64)) as u8);
 621   let x47: u64 = (x20 >> 8);
 622   let x48: u8 = ((x47 & (0xff as u64)) as u8);
 623   let x49: u64 = (x47 >> 8);
 624   let x50: u8 = ((x49 & (0xff as u64)) as u8);
 625   let x51: u64 = (x49 >> 8);
 626   let x52: u8 = ((x51 & (0xff as u64)) as u8);
 627   let x53: u64 = (x51 >> 8);
 628   let x54: u8 = ((x53 & (0xff as u64)) as u8);
 629   let x55: u64 = (x53 >> 8);
 630   let x56: u8 = ((x55 & (0xff as u64)) as u8);
 631   let x57: u8 = ((x55 >> 8) as u8);
 632   let x58: u8 = ((x22 & (0xff as u64)) as u8);
 633   let x59: u64 = (x22 >> 8);
 634   let x60: u8 = ((x59 & (0xff as u64)) as u8);
 635   let x61: u64 = (x59 >> 8);
 636   let x62: u8 = ((x61 & (0xff as u64)) as u8);
 637   let x63: u64 = (x61 >> 8);
 638   let x64: u8 = ((x63 & (0xff as u64)) as u8);
 639   let x65: u64 = (x63 >> 8);
 640   let x66: u8 = ((x65 & (0xff as u64)) as u8);
 641   let x67: u64 = (x65 >> 8);
 642   let x68: u8 = ((x67 & (0xff as u64)) as u8);
 643   let x69: u8 = ((x67 >> 8) as u8);
 644   let x70: u8 = ((x24 & (0xff as u64)) as u8);
 645   let x71: u64 = (x24 >> 8);
 646   let x72: u8 = ((x71 & (0xff as u64)) as u8);
 647   let x73: u64 = (x71 >> 8);
 648   let x74: u8 = ((x73 & (0xff as u64)) as u8);
 649   let x75: u64 = (x73 >> 8);
 650   let x76: u8 = ((x75 & (0xff as u64)) as u8);
 651   let x77: u64 = (x75 >> 8);
 652   let x78: u8 = ((x77 & (0xff as u64)) as u8);
 653   let x79: u64 = (x77 >> 8);
 654   let x80: u8 = ((x79 & (0xff as u64)) as u8);
 655   let x81: u8 = ((x79 >> 8) as u8);
 656   let x82: u8 = ((x26 & (0xff as u64)) as u8);
 657   let x83: u64 = (x26 >> 8);
 658   let x84: u8 = ((x83 & (0xff as u64)) as u8);
 659   let x85: u64 = (x83 >> 8);
 660   let x86: u8 = ((x85 & (0xff as u64)) as u8);
 661   let x87: u64 = (x85 >> 8);
 662   let x88: u8 = ((x87 & (0xff as u64)) as u8);
 663   let x89: u64 = (x87 >> 8);
 664   let x90: u8 = ((x89 & (0xff as u64)) as u8);
 665   let x91: u64 = (x89 >> 8);
 666   let x92: u8 = ((x91 & (0xff as u64)) as u8);
 667   let x93: u8 = ((x91 >> 8) as u8);
 668   let x94: u8 = ((x28 & (0xff as u64)) as u8);
 669   let x95: u64 = (x28 >> 8);
 670   let x96: u8 = ((x95 & (0xff as u64)) as u8);
 671   let x97: u64 = (x95 >> 8);
 672   let x98: u8 = ((x97 & (0xff as u64)) as u8);
 673   let x99: u64 = (x97 >> 8);
 674   let x100: u8 = ((x99 & (0xff as u64)) as u8);
 675   let x101: u64 = (x99 >> 8);
 676   let x102: u8 = ((x101 & (0xff as u64)) as u8);
 677   let x103: u64 = (x101 >> 8);
 678   let x104: u8 = ((x103 & (0xff as u64)) as u8);
 679   let x105: u8 = ((x103 >> 8) as u8);
 680   let x106: u8 = ((x30 & (0xff as u64)) as u8);
 681   let x107: u64 = (x30 >> 8);
 682   let x108: u8 = ((x107 & (0xff as u64)) as u8);
 683   let x109: u64 = (x107 >> 8);
 684   let x110: u8 = ((x109 & (0xff as u64)) as u8);
 685   let x111: u64 = (x109 >> 8);
 686   let x112: u8 = ((x111 & (0xff as u64)) as u8);
 687   let x113: u64 = (x111 >> 8);
 688   let x114: u8 = ((x113 & (0xff as u64)) as u8);
 689   let x115: u64 = (x113 >> 8);
 690   let x116: u8 = ((x115 & (0xff as u64)) as u8);
 691   let x117: u8 = ((x115 >> 8) as u8);
 692   let x118: u8 = ((x32 & (0xff as u64)) as u8);
 693   let x119: u64 = (x32 >> 8);
 694   let x120: u8 = ((x119 & (0xff as u64)) as u8);
 695   let x121: u64 = (x119 >> 8);
 696   let x122: u8 = ((x121 & (0xff as u64)) as u8);
 697   let x123: u64 = (x121 >> 8);
 698   let x124: u8 = ((x123 & (0xff as u64)) as u8);
 699   let x125: u64 = (x123 >> 8);
 700   let x126: u8 = ((x125 & (0xff as u64)) as u8);
 701   let x127: u64 = (x125 >> 8);
 702   let x128: u8 = ((x127 & (0xff as u64)) as u8);
 703   let x129: u8 = ((x127 >> 8) as u8);
 704   out1[0] = x34;
 705   out1[1] = x36;
 706   out1[2] = x38;
 707   out1[3] = x40;
 708   out1[4] = x42;
 709   out1[5] = x44;
 710   out1[6] = x45;
 711   out1[7] = x46;
 712   out1[8] = x48;
 713   out1[9] = x50;
 714   out1[10] = x52;
 715   out1[11] = x54;
 716   out1[12] = x56;
 717   out1[13] = x57;
 718   out1[14] = x58;
 719   out1[15] = x60;
 720   out1[16] = x62;
 721   out1[17] = x64;
 722   out1[18] = x66;
 723   out1[19] = x68;
 724   out1[20] = x69;
 725   out1[21] = x70;
 726   out1[22] = x72;
 727   out1[23] = x74;
 728   out1[24] = x76;
 729   out1[25] = x78;
 730   out1[26] = x80;
 731   out1[27] = x81;
 732   out1[28] = x82;
 733   out1[29] = x84;
 734   out1[30] = x86;
 735   out1[31] = x88;
 736   out1[32] = x90;
 737   out1[33] = x92;
 738   out1[34] = x93;
 739   out1[35] = x94;
 740   out1[36] = x96;
 741   out1[37] = x98;
 742   out1[38] = x100;
 743   out1[39] = x102;
 744   out1[40] = x104;
 745   out1[41] = x105;
 746   out1[42] = x106;
 747   out1[43] = x108;
 748   out1[44] = x110;
 749   out1[45] = x112;
 750   out1[46] = x114;
 751   out1[47] = x116;
 752   out1[48] = x117;
 753   out1[49] = x118;
 754   out1[50] = x120;
 755   out1[51] = x122;
 756   out1[52] = x124;
 757   out1[53] = x126;
 758   out1[54] = x128;
 759   out1[55] = x129;
 760 }
 761
 762 /// The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order.
 763 ///
 764 /// Postconditions:
 765 ///   eval out1 mod m = bytes_eval arg1 mod m
 766 ///
 767 /// Input Bounds:
 768 ///   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]]
 769 #[inline]
 770 pub fn fiat_p448_from_bytes(out1: &mut fiat_p448_tight_field_element, arg1: &[u8; 56]) -> () {
 771   let x1: u64 = (((arg1[55]) as u64) << 48);
 772   let x2: u64 = (((arg1[54]) as u64) << 40);
 773   let x3: u64 = (((arg1[53]) as u64) << 32);
 774   let x4: u64 = (((arg1[52]) as u64) << 24);
 775   let x5: u64 = (((arg1[51]) as u64) << 16);
 776   let x6: u64 = (((arg1[50]) as u64) << 8);
 777   let x7: u8 = (arg1[49]);
 778   let x8: u64 = (((arg1[48]) as u64) << 48);
 779   let x9: u64 = (((arg1[47]) as u64) << 40);
 780   let x10: u64 = (((arg1[46]) as u64) << 32);
 781   let x11: u64 = (((arg1[45]) as u64) << 24);
 782   let x12: u64 = (((arg1[44]) as u64) << 16);
 783   let x13: u64 = (((arg1[43]) as u64) << 8);
 784   let x14: u8 = (arg1[42]);
 785   let x15: u64 = (((arg1[41]) as u64) << 48);
 786   let x16: u64 = (((arg1[40]) as u64) << 40);
 787   let x17: u64 = (((arg1[39]) as u64) << 32);
 788   let x18: u64 = (((arg1[38]) as u64) << 24);
 789   let x19: u64 = (((arg1[37]) as u64) << 16);
 790   let x20: u64 = (((arg1[36]) as u64) << 8);
 791   let x21: u8 = (arg1[35]);
 792   let x22: u64 = (((arg1[34]) as u64) << 48);
 793   let x23: u64 = (((arg1[33]) as u64) << 40);
 794   let x24: u64 = (((arg1[32]) as u64) << 32);
 795   let x25: u64 = (((arg1[31]) as u64) << 24);
 796   let x26: u64 = (((arg1[30]) as u64) << 16);
 797   let x27: u64 = (((arg1[29]) as u64) << 8);
 798   let x28: u8 = (arg1[28]);
 799   let x29: u64 = (((arg1[27]) as u64) << 48);
 800   let x30: u64 = (((arg1[26]) as u64) << 40);
 801   let x31: u64 = (((arg1[25]) as u64) << 32);
 802   let x32: u64 = (((arg1[24]) as u64) << 24);
 803   let x33: u64 = (((arg1[23]) as u64) << 16);
 804   let x34: u64 = (((arg1[22]) as u64) << 8);
 805   let x35: u8 = (arg1[21]);
 806   let x36: u64 = (((arg1[20]) as u64) << 48);
 807   let x37: u64 = (((arg1[19]) as u64) << 40);
 808   let x38: u64 = (((arg1[18]) as u64) << 32);
 809   let x39: u64 = (((arg1[17]) as u64) << 24);
 810   let x40: u64 = (((arg1[16]) as u64) << 16);
 811   let x41: u64 = (((arg1[15]) as u64) << 8);
 812   let x42: u8 = (arg1[14]);
 813   let x43: u64 = (((arg1[13]) as u64) << 48);
 814   let x44: u64 = (((arg1[12]) as u64) << 40);
 815   let x45: u64 = (((arg1[11]) as u64) << 32);
 816   let x46: u64 = (((arg1[10]) as u64) << 24);
 817   let x47: u64 = (((arg1[9]) as u64) << 16);
 818   let x48: u64 = (((arg1[8]) as u64) << 8);
 819   let x49: u8 = (arg1[7]);
 820   let x50: u64 = (((arg1[6]) as u64) << 48);
 821   let x51: u64 = (((arg1[5]) as u64) << 40);
 822   let x52: u64 = (((arg1[4]) as u64) << 32);
 823   let x53: u64 = (((arg1[3]) as u64) << 24);
 824   let x54: u64 = (((arg1[2]) as u64) << 16);
 825   let x55: u64 = (((arg1[1]) as u64) << 8);
 826   let x56: u8 = (arg1[0]);
 827   let x57: u64 = (x55 + (x56 as u64));
 828   let x58: u64 = (x54 + x57);
 829   let x59: u64 = (x53 + x58);
 830   let x60: u64 = (x52 + x59);
 831   let x61: u64 = (x51 + x60);
 832   let x62: u64 = (x50 + x61);
 833   let x63: u64 = (x48 + (x49 as u64));
 834   let x64: u64 = (x47 + x63);
 835   let x65: u64 = (x46 + x64);
 836   let x66: u64 = (x45 + x65);
 837   let x67: u64 = (x44 + x66);
 838   let x68: u64 = (x43 + x67);
 839   let x69: u64 = (x41 + (x42 as u64));
 840   let x70: u64 = (x40 + x69);
 841   let x71: u64 = (x39 + x70);
 842   let x72: u64 = (x38 + x71);
 843   let x73: u64 = (x37 + x72);
 844   let x74: u64 = (x36 + x73);
 845   let x75: u64 = (x34 + (x35 as u64));
 846   let x76: u64 = (x33 + x75);
 847   let x77: u64 = (x32 + x76);
 848   let x78: u64 = (x31 + x77);
 849   let x79: u64 = (x30 + x78);
 850   let x80: u64 = (x29 + x79);
 851   let x81: u64 = (x27 + (x28 as u64));
 852   let x82: u64 = (x26 + x81);
 853   let x83: u64 = (x25 + x82);
 854   let x84: u64 = (x24 + x83);
 855   let x85: u64 = (x23 + x84);
 856   let x86: u64 = (x22 + x85);
 857   let x87: u64 = (x20 + (x21 as u64));
 858   let x88: u64 = (x19 + x87);
 859   let x89: u64 = (x18 + x88);
 860   let x90: u64 = (x17 + x89);
 861   let x91: u64 = (x16 + x90);
 862   let x92: u64 = (x15 + x91);
 863   let x93: u64 = (x13 + (x14 as u64));
 864   let x94: u64 = (x12 + x93);
 865   let x95: u64 = (x11 + x94);
 866   let x96: u64 = (x10 + x95);
 867   let x97: u64 = (x9 + x96);
 868   let x98: u64 = (x8 + x97);
 869   let x99: u64 = (x6 + (x7 as u64));
 870   let x100: u64 = (x5 + x99);
 871   let x101: u64 = (x4 + x100);
 872   let x102: u64 = (x3 + x101);
 873   let x103: u64 = (x2 + x102);
 874   let x104: u64 = (x1 + x103);
 875   out1[0] = x62;
 876   out1[1] = x68;
 877   out1[2] = x74;
 878   out1[3] = x80;
 879   out1[4] = x86;
 880   out1[5] = x92;
 881   out1[6] = x98;
 882   out1[7] = x104;
 883 }
 884
 885 /// The function fiat_p448_relax is the identity function converting from tight field elements to loose field elements.
 886 ///
 887 /// Postconditions:
 888 ///   out1 = arg1
 889 ///
 890 #[inline]
 891 pub fn fiat_p448_relax(out1: &mut fiat_p448_loose_field_element, arg1: &fiat_p448_tight_field_element) -> () {
 892   let x1: u64 = (arg1[0]);
 893   let x2: u64 = (arg1[1]);
 894   let x3: u64 = (arg1[2]);
 895   let x4: u64 = (arg1[3]);
 896   let x5: u64 = (arg1[4]);
 897   let x6: u64 = (arg1[5]);
 898   let x7: u64 = (arg1[6]);
 899   let x8: u64 = (arg1[7]);
 900   out1[0] = x1;
 901   out1[1] = x2;
 902   out1[2] = x3;
 903   out1[3] = x4;
 904   out1[4] = x5;
 905   out1[5] = x6;
 906   out1[6] = x7;
 907   out1[7] = x8;
 908 }