vendor/fiat-crypto/src/curve25519_64.rs

   1 //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline 25519 64 '(auto)' '2^255 - 19' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax carry_scmul121666
   2 //! curve description: 25519
   3 //! machine_wordsize = 64 (from "64")
   4 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax, carry_scmul121666
   5 //! n = 5 (from "(auto)")
   6 //! s-c = 2^255 - [(1, 19)] (from "2^255 - 19")
   7 //! tight_bounds_multiplier = 1 (from "")
   8 //!
   9 //! Computed values:
  10 //!   carry_chain = [0, 1, 2, 3, 4, 0, 1]
  11 //!   eval z = z[0] + (z[1] << 51) + (z[2] << 102) + (z[3] << 153) + (z[4] << 204)
  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)
  13 //!   balance = [0xfffffffffffda, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe, 0xffffffffffffe]
  14
  15 #![allow(unused_parens)]
  16 #![allow(non_camel_case_types)]
  17
  18 pub type fiat_25519_u1 = u8;
  19 pub type fiat_25519_i1 = i8;
  20 pub type fiat_25519_u2 = u8;
  21 pub type fiat_25519_i2 = i8;
  22
  23 /* The type fiat_25519_loose_field_element is a field element with loose bounds. */
  24 /* Bounds: [[0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000], [0x0 ~> 0x18000000000000]] */
  25 pub type fiat_25519_loose_field_element = [u64; 5];
  26
  27 /* The type fiat_25519_tight_field_element is a field element with tight bounds. */
  28 /* Bounds: [[0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000], [0x0 ~> 0x8000000000000]] */
  29 pub type fiat_25519_tight_field_element = [u64; 5];
  30
  31
  32 /// The function fiat_25519_addcarryx_u51 is an addition with carry.
  33 ///
  34 /// Postconditions:
  35 ///   out1 = (arg1 + arg2 + arg3) mod 2^51
  36 ///   out2 = ⌊(arg1 + arg2 + arg3) / 2^51⌋
  37 ///
  38 /// Input Bounds:
  39 ///   arg1: [0x0 ~> 0x1]
  40 ///   arg2: [0x0 ~> 0x7ffffffffffff]
  41 ///   arg3: [0x0 ~> 0x7ffffffffffff]
  42 /// Output Bounds:
  43 ///   out1: [0x0 ~> 0x7ffffffffffff]
  44 ///   out2: [0x0 ~> 0x1]
  45 #[inline]
  46 pub fn fiat_25519_addcarryx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1: fiat_25519_u1, arg2: u64, arg3: u64) -> () {
  47   let x1: u64 = (((arg1 as u64) + arg2) + arg3);
  48   let x2: u64 = (x1 & 0x7ffffffffffff);
  49   let x3: fiat_25519_u1 = ((x1 >> 51) as fiat_25519_u1);
  50   *out1 = x2;
  51   *out2 = x3;
  52 }
  53
  54 /// The function fiat_25519_subborrowx_u51 is a subtraction with borrow.
  55 ///
  56 /// Postconditions:
  57 ///   out1 = (-arg1 + arg2 + -arg3) mod 2^51
  58 ///   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^51⌋
  59 ///
  60 /// Input Bounds:
  61 ///   arg1: [0x0 ~> 0x1]
  62 ///   arg2: [0x0 ~> 0x7ffffffffffff]
  63 ///   arg3: [0x0 ~> 0x7ffffffffffff]
  64 /// Output Bounds:
  65 ///   out1: [0x0 ~> 0x7ffffffffffff]
  66 ///   out2: [0x0 ~> 0x1]
  67 #[inline]
  68 pub fn fiat_25519_subborrowx_u51(out1: &mut u64, out2: &mut fiat_25519_u1, arg1: fiat_25519_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_25519_i1 = ((x1 >> 51) as fiat_25519_i1);
  71   let x3: u64 = (((x1 as i128) & (0x7ffffffffffff as i128)) as u64);
  72   *out1 = x3;
  73   *out2 = (((0x0 as fiat_25519_i2) - (x2 as fiat_25519_i2)) as fiat_25519_u1);
  74 }
  75
  76 /// The function fiat_25519_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_25519_cmovznz_u64(out1: &mut u64, arg1: fiat_25519_u1, arg2: u64, arg3: u64) -> () {
  89   let x1: fiat_25519_u1 = (!(!arg1));
  90   let x2: u64 = ((((((0x0 as fiat_25519_i2) - (x1 as fiat_25519_i2)) as fiat_25519_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_25519_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_25519_carry_mul(out1: &mut fiat_25519_tight_field_element, arg1: &fiat_25519_loose_field_element, arg2: &fiat_25519_loose_field_element) -> () {
 102   let x1: u128 = (((arg1[4]) as u128) * (((arg2[4]) * 0x13) as u128));
 103   let x2: u128 = (((arg1[4]) as u128) * (((arg2[3]) * 0x13) as u128));
 104   let x3: u128 = (((arg1[4]) as u128) * (((arg2[2]) * 0x13) as u128));
 105   let x4: u128 = (((arg1[4]) as u128) * (((arg2[1]) * 0x13) as u128));
 106   let x5: u128 = (((arg1[3]) as u128) * (((arg2[4]) * 0x13) as u128));
 107   let x6: u128 = (((arg1[3]) as u128) * (((arg2[3]) * 0x13) as u128));
 108   let x7: u128 = (((arg1[3]) as u128) * (((arg2[2]) * 0x13) as u128));
 109   let x8: u128 = (((arg1[2]) as u128) * (((arg2[4]) * 0x13) as u128));
 110   let x9: u128 = (((arg1[2]) as u128) * (((arg2[3]) * 0x13) as u128));
 111   let x10: u128 = (((arg1[1]) as u128) * (((arg2[4]) * 0x13) as u128));
 112   let x11: u128 = (((arg1[4]) as u128) * ((arg2[0]) as u128));
 113   let x12: u128 = (((arg1[3]) as u128) * ((arg2[1]) as u128));
 114   let x13: u128 = (((arg1[3]) as u128) * ((arg2[0]) as u128));
 115   let x14: u128 = (((arg1[2]) as u128) * ((arg2[2]) as u128));
 116   let x15: u128 = (((arg1[2]) as u128) * ((arg2[1]) as u128));
 117   let x16: u128 = (((arg1[2]) as u128) * ((arg2[0]) as u128));
 118   let x17: u128 = (((arg1[1]) as u128) * ((arg2[3]) as u128));
 119   let x18: u128 = (((arg1[1]) as u128) * ((arg2[2]) as u128));
 120   let x19: u128 = (((arg1[1]) as u128) * ((arg2[1]) as u128));
 121   let x20: u128 = (((arg1[1]) as u128) * ((arg2[0]) as u128));
 122   let x21: u128 = (((arg1[0]) as u128) * ((arg2[4]) as u128));
 123   let x22: u128 = (((arg1[0]) as u128) * ((arg2[3]) as u128));
 124   let x23: u128 = (((arg1[0]) as u128) * ((arg2[2]) as u128));
 125   let x24: u128 = (((arg1[0]) as u128) * ((arg2[1]) as u128));
 126   let x25: u128 = (((arg1[0]) as u128) * ((arg2[0]) as u128));
 127   let x26: u128 = (x25 + (x10 + (x9 + (x7 + x4))));
 128   let x27: u64 = ((x26 >> 51) as u64);
 129   let x28: u64 = ((x26 & (0x7ffffffffffff as u128)) as u64);
 130   let x29: u128 = (x21 + (x17 + (x14 + (x12 + x11))));
 131   let x30: u128 = (x22 + (x18 + (x15 + (x13 + x1))));
 132   let x31: u128 = (x23 + (x19 + (x16 + (x5 + x2))));
 133   let x32: u128 = (x24 + (x20 + (x8 + (x6 + x3))));
 134   let x33: u128 = ((x27 as u128) + x32);
 135   let x34: u64 = ((x33 >> 51) as u64);
 136   let x35: u64 = ((x33 & (0x7ffffffffffff as u128)) as u64);
 137   let x36: u128 = ((x34 as u128) + x31);
 138   let x37: u64 = ((x36 >> 51) as u64);
 139   let x38: u64 = ((x36 & (0x7ffffffffffff as u128)) as u64);
 140   let x39: u128 = ((x37 as u128) + x30);
 141   let x40: u64 = ((x39 >> 51) as u64);
 142   let x41: u64 = ((x39 & (0x7ffffffffffff as u128)) as u64);
 143   let x42: u128 = ((x40 as u128) + x29);
 144   let x43: u64 = ((x42 >> 51) as u64);
 145   let x44: u64 = ((x42 & (0x7ffffffffffff as u128)) as u64);
 146   let x45: u64 = (x43 * 0x13);
 147   let x46: u64 = (x28 + x45);
 148   let x47: u64 = (x46 >> 51);
 149   let x48: u64 = (x46 & 0x7ffffffffffff);
 150   let x49: u64 = (x47 + x35);
 151   let x50: fiat_25519_u1 = ((x49 >> 51) as fiat_25519_u1);
 152   let x51: u64 = (x49 & 0x7ffffffffffff);
 153   let x52: u64 = ((x50 as u64) + x38);
 154   out1[0] = x48;
 155   out1[1] = x51;
 156   out1[2] = x52;
 157   out1[3] = x41;
 158   out1[4] = x44;
 159 }
 160
 161 /// The function fiat_25519_carry_square squares a field element and reduces the result.
 162 ///
 163 /// Postconditions:
 164 ///   eval out1 mod m = (eval arg1 * eval arg1) mod m
 165 ///
 166 #[inline]
 167 pub fn fiat_25519_carry_square(out1: &mut fiat_25519_tight_field_element, arg1: &fiat_25519_loose_field_element) -> () {
 168   let x1: u64 = ((arg1[4]) * 0x13);
 169   let x2: u64 = (x1 * 0x2);
 170   let x3: u64 = ((arg1[4]) * 0x2);
 171   let x4: u64 = ((arg1[3]) * 0x13);
 172   let x5: u64 = (x4 * 0x2);
 173   let x6: u64 = ((arg1[3]) * 0x2);
 174   let x7: u64 = ((arg1[2]) * 0x2);
 175   let x8: u64 = ((arg1[1]) * 0x2);
 176   let x9: u128 = (((arg1[4]) as u128) * (x1 as u128));
 177   let x10: u128 = (((arg1[3]) as u128) * (x2 as u128));
 178   let x11: u128 = (((arg1[3]) as u128) * (x4 as u128));
 179   let x12: u128 = (((arg1[2]) as u128) * (x2 as u128));
 180   let x13: u128 = (((arg1[2]) as u128) * (x5 as u128));
 181   let x14: u128 = (((arg1[2]) as u128) * ((arg1[2]) as u128));
 182   let x15: u128 = (((arg1[1]) as u128) * (x2 as u128));
 183   let x16: u128 = (((arg1[1]) as u128) * (x6 as u128));
 184   let x17: u128 = (((arg1[1]) as u128) * (x7 as u128));
 185   let x18: u128 = (((arg1[1]) as u128) * ((arg1[1]) as u128));
 186   let x19: u128 = (((arg1[0]) as u128) * (x3 as u128));
 187   let x20: u128 = (((arg1[0]) as u128) * (x6 as u128));
 188   let x21: u128 = (((arg1[0]) as u128) * (x7 as u128));
 189   let x22: u128 = (((arg1[0]) as u128) * (x8 as u128));
 190   let x23: u128 = (((arg1[0]) as u128) * ((arg1[0]) as u128));
 191   let x24: u128 = (x23 + (x15 + x13));
 192   let x25: u64 = ((x24 >> 51) as u64);
 193   let x26: u64 = ((x24 & (0x7ffffffffffff as u128)) as u64);
 194   let x27: u128 = (x19 + (x16 + x14));
 195   let x28: u128 = (x20 + (x17 + x9));
 196   let x29: u128 = (x21 + (x18 + x10));
 197   let x30: u128 = (x22 + (x12 + x11));
 198   let x31: u128 = ((x25 as u128) + x30);
 199   let x32: u64 = ((x31 >> 51) as u64);
 200   let x33: u64 = ((x31 & (0x7ffffffffffff as u128)) as u64);
 201   let x34: u128 = ((x32 as u128) + x29);
 202   let x35: u64 = ((x34 >> 51) as u64);
 203   let x36: u64 = ((x34 & (0x7ffffffffffff as u128)) as u64);
 204   let x37: u128 = ((x35 as u128) + x28);
 205   let x38: u64 = ((x37 >> 51) as u64);
 206   let x39: u64 = ((x37 & (0x7ffffffffffff as u128)) as u64);
 207   let x40: u128 = ((x38 as u128) + x27);
 208   let x41: u64 = ((x40 >> 51) as u64);
 209   let x42: u64 = ((x40 & (0x7ffffffffffff as u128)) as u64);
 210   let x43: u64 = (x41 * 0x13);
 211   let x44: u64 = (x26 + x43);
 212   let x45: u64 = (x44 >> 51);
 213   let x46: u64 = (x44 & 0x7ffffffffffff);
 214   let x47: u64 = (x45 + x33);
 215   let x48: fiat_25519_u1 = ((x47 >> 51) as fiat_25519_u1);
 216   let x49: u64 = (x47 & 0x7ffffffffffff);
 217   let x50: u64 = ((x48 as u64) + x36);
 218   out1[0] = x46;
 219   out1[1] = x49;
 220   out1[2] = x50;
 221   out1[3] = x39;
 222   out1[4] = x42;
 223 }
 224
 225 /// The function fiat_25519_carry reduces a field element.
 226 ///
 227 /// Postconditions:
 228 ///   eval out1 mod m = eval arg1 mod m
 229 ///
 230 #[inline]
 231 pub fn fiat_25519_carry(out1: &mut fiat_25519_tight_field_element, arg1: &fiat_25519_loose_field_element) -> () {
 232   let x1: u64 = (arg1[0]);
 233   let x2: u64 = ((x1 >> 51) + (arg1[1]));
 234   let x3: u64 = ((x2 >> 51) + (arg1[2]));
 235   let x4: u64 = ((x3 >> 51) + (arg1[3]));
 236   let x5: u64 = ((x4 >> 51) + (arg1[4]));
 237   let x6: u64 = ((x1 & 0x7ffffffffffff) + ((x5 >> 51) * 0x13));
 238   let x7: u64 = ((((x6 >> 51) as fiat_25519_u1) as u64) + (x2 & 0x7ffffffffffff));
 239   let x8: u64 = (x6 & 0x7ffffffffffff);
 240   let x9: u64 = (x7 & 0x7ffffffffffff);
 241   let x10: u64 = ((((x7 >> 51) as fiat_25519_u1) as u64) + (x3 & 0x7ffffffffffff));
 242   let x11: u64 = (x4 & 0x7ffffffffffff);
 243   let x12: u64 = (x5 & 0x7ffffffffffff);
 244   out1[0] = x8;
 245   out1[1] = x9;
 246   out1[2] = x10;
 247   out1[3] = x11;
 248   out1[4] = x12;
 249 }
 250
 251 /// The function fiat_25519_add adds two field elements.
 252 ///
 253 /// Postconditions:
 254 ///   eval out1 mod m = (eval arg1 + eval arg2) mod m
 255 ///
 256 #[inline]
 257 pub fn fiat_25519_add(out1: &mut fiat_25519_loose_field_element, arg1: &fiat_25519_tight_field_element, arg2: &fiat_25519_tight_field_element) -> () {
 258   let x1: u64 = ((arg1[0]) + (arg2[0]));
 259   let x2: u64 = ((arg1[1]) + (arg2[1]));
 260   let x3: u64 = ((arg1[2]) + (arg2[2]));
 261   let x4: u64 = ((arg1[3]) + (arg2[3]));
 262   let x5: u64 = ((arg1[4]) + (arg2[4]));
 263   out1[0] = x1;
 264   out1[1] = x2;
 265   out1[2] = x3;
 266   out1[3] = x4;
 267   out1[4] = x5;
 268 }
 269
 270 /// The function fiat_25519_sub subtracts two field elements.
 271 ///
 272 /// Postconditions:
 273 ///   eval out1 mod m = (eval arg1 - eval arg2) mod m
 274 ///
 275 #[inline]
 276 pub fn fiat_25519_sub(out1: &mut fiat_25519_loose_field_element, arg1: &fiat_25519_tight_field_element, arg2: &fiat_25519_tight_field_element) -> () {
 277   let x1: u64 = ((0xfffffffffffda + (arg1[0])) - (arg2[0]));
 278   let x2: u64 = ((0xffffffffffffe + (arg1[1])) - (arg2[1]));
 279   let x3: u64 = ((0xffffffffffffe + (arg1[2])) - (arg2[2]));
 280   let x4: u64 = ((0xffffffffffffe + (arg1[3])) - (arg2[3]));
 281   let x5: u64 = ((0xffffffffffffe + (arg1[4])) - (arg2[4]));
 282   out1[0] = x1;
 283   out1[1] = x2;
 284   out1[2] = x3;
 285   out1[3] = x4;
 286   out1[4] = x5;
 287 }
 288
 289 /// The function fiat_25519_opp negates a field element.
 290 ///
 291 /// Postconditions:
 292 ///   eval out1 mod m = -eval arg1 mod m
 293 ///
 294 #[inline]
 295 pub fn fiat_25519_opp(out1: &mut fiat_25519_loose_field_element, arg1: &fiat_25519_tight_field_element) -> () {
 296   let x1: u64 = (0xfffffffffffda - (arg1[0]));
 297   let x2: u64 = (0xffffffffffffe - (arg1[1]));
 298   let x3: u64 = (0xffffffffffffe - (arg1[2]));
 299   let x4: u64 = (0xffffffffffffe - (arg1[3]));
 300   let x5: u64 = (0xffffffffffffe - (arg1[4]));
 301   out1[0] = x1;
 302   out1[1] = x2;
 303   out1[2] = x3;
 304   out1[3] = x4;
 305   out1[4] = x5;
 306 }
 307
 308 /// The function fiat_25519_selectznz is a multi-limb conditional select.
 309 ///
 310 /// Postconditions:
 311 ///   out1 = (if arg1 = 0 then arg2 else arg3)
 312 ///
 313 /// Input Bounds:
 314 ///   arg1: [0x0 ~> 0x1]
 315 ///   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 316 ///   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 317 /// Output Bounds:
 318 ///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
 319 #[inline]
 320 pub fn fiat_25519_selectznz(out1: &mut [u64; 5], arg1: fiat_25519_u1, arg2: &[u64; 5], arg3: &[u64; 5]) -> () {
 321   let mut x1: u64 = 0;
 322   fiat_25519_cmovznz_u64(&mut x1, arg1, (arg2[0]), (arg3[0]));
 323   let mut x2: u64 = 0;
 324   fiat_25519_cmovznz_u64(&mut x2, arg1, (arg2[1]), (arg3[1]));
 325   let mut x3: u64 = 0;
 326   fiat_25519_cmovznz_u64(&mut x3, arg1, (arg2[2]), (arg3[2]));
 327   let mut x4: u64 = 0;
 328   fiat_25519_cmovznz_u64(&mut x4, arg1, (arg2[3]), (arg3[3]));
 329   let mut x5: u64 = 0;
 330   fiat_25519_cmovznz_u64(&mut x5, arg1, (arg2[4]), (arg3[4]));
 331   out1[0] = x1;
 332   out1[1] = x2;
 333   out1[2] = x3;
 334   out1[3] = x4;
 335   out1[4] = x5;
 336 }
 337
 338 /// The function fiat_25519_to_bytes serializes a field element to bytes in little-endian order.
 339 ///
 340 /// Postconditions:
 341 ///   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
 342 ///
 343 /// Output Bounds:
 344 ///   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 ~> 0x7f]]
 345 #[inline]
 346 pub fn fiat_25519_to_bytes(out1: &mut [u8; 32], arg1: &fiat_25519_tight_field_element) -> () {
 347   let mut x1: u64 = 0;
 348   let mut x2: fiat_25519_u1 = 0;
 349   fiat_25519_subborrowx_u51(&mut x1, &mut x2, 0x0, (arg1[0]), 0x7ffffffffffed);
 350   let mut x3: u64 = 0;
 351   let mut x4: fiat_25519_u1 = 0;
 352   fiat_25519_subborrowx_u51(&mut x3, &mut x4, x2, (arg1[1]), 0x7ffffffffffff);
 353   let mut x5: u64 = 0;
 354   let mut x6: fiat_25519_u1 = 0;
 355   fiat_25519_subborrowx_u51(&mut x5, &mut x6, x4, (arg1[2]), 0x7ffffffffffff);
 356   let mut x7: u64 = 0;
 357   let mut x8: fiat_25519_u1 = 0;
 358   fiat_25519_subborrowx_u51(&mut x7, &mut x8, x6, (arg1[3]), 0x7ffffffffffff);
 359   let mut x9: u64 = 0;
 360   let mut x10: fiat_25519_u1 = 0;
 361   fiat_25519_subborrowx_u51(&mut x9, &mut x10, x8, (arg1[4]), 0x7ffffffffffff);
 362   let mut x11: u64 = 0;
 363   fiat_25519_cmovznz_u64(&mut x11, x10, (0x0 as u64), 0xffffffffffffffff);
 364   let mut x12: u64 = 0;
 365   let mut x13: fiat_25519_u1 = 0;
 366   fiat_25519_addcarryx_u51(&mut x12, &mut x13, 0x0, x1, (x11 & 0x7ffffffffffed));
 367   let mut x14: u64 = 0;
 368   let mut x15: fiat_25519_u1 = 0;
 369   fiat_25519_addcarryx_u51(&mut x14, &mut x15, x13, x3, (x11 & 0x7ffffffffffff));
 370   let mut x16: u64 = 0;
 371   let mut x17: fiat_25519_u1 = 0;
 372   fiat_25519_addcarryx_u51(&mut x16, &mut x17, x15, x5, (x11 & 0x7ffffffffffff));
 373   let mut x18: u64 = 0;
 374   let mut x19: fiat_25519_u1 = 0;
 375   fiat_25519_addcarryx_u51(&mut x18, &mut x19, x17, x7, (x11 & 0x7ffffffffffff));
 376   let mut x20: u64 = 0;
 377   let mut x21: fiat_25519_u1 = 0;
 378   fiat_25519_addcarryx_u51(&mut x20, &mut x21, x19, x9, (x11 & 0x7ffffffffffff));
 379   let x22: u64 = (x20 << 4);
 380   let x23: u64 = (x18 * (0x2 as u64));
 381   let x24: u64 = (x16 << 6);
 382   let x25: u64 = (x14 << 3);
 383   let x26: u8 = ((x12 & (0xff as u64)) as u8);
 384   let x27: u64 = (x12 >> 8);
 385   let x28: u8 = ((x27 & (0xff as u64)) as u8);
 386   let x29: u64 = (x27 >> 8);
 387   let x30: u8 = ((x29 & (0xff as u64)) as u8);
 388   let x31: u64 = (x29 >> 8);
 389   let x32: u8 = ((x31 & (0xff as u64)) as u8);
 390   let x33: u64 = (x31 >> 8);
 391   let x34: u8 = ((x33 & (0xff as u64)) as u8);
 392   let x35: u64 = (x33 >> 8);
 393   let x36: u8 = ((x35 & (0xff as u64)) as u8);
 394   let x37: u8 = ((x35 >> 8) as u8);
 395   let x38: u64 = (x25 + (x37 as u64));
 396   let x39: u8 = ((x38 & (0xff as u64)) as u8);
 397   let x40: u64 = (x38 >> 8);
 398   let x41: u8 = ((x40 & (0xff as u64)) as u8);
 399   let x42: u64 = (x40 >> 8);
 400   let x43: u8 = ((x42 & (0xff as u64)) as u8);
 401   let x44: u64 = (x42 >> 8);
 402   let x45: u8 = ((x44 & (0xff as u64)) as u8);
 403   let x46: u64 = (x44 >> 8);
 404   let x47: u8 = ((x46 & (0xff as u64)) as u8);
 405   let x48: u64 = (x46 >> 8);
 406   let x49: u8 = ((x48 & (0xff as u64)) as u8);
 407   let x50: u8 = ((x48 >> 8) as u8);
 408   let x51: u64 = (x24 + (x50 as u64));
 409   let x52: u8 = ((x51 & (0xff as u64)) as u8);
 410   let x53: u64 = (x51 >> 8);
 411   let x54: u8 = ((x53 & (0xff as u64)) as u8);
 412   let x55: u64 = (x53 >> 8);
 413   let x56: u8 = ((x55 & (0xff as u64)) as u8);
 414   let x57: u64 = (x55 >> 8);
 415   let x58: u8 = ((x57 & (0xff as u64)) as u8);
 416   let x59: u64 = (x57 >> 8);
 417   let x60: u8 = ((x59 & (0xff as u64)) as u8);
 418   let x61: u64 = (x59 >> 8);
 419   let x62: u8 = ((x61 & (0xff as u64)) as u8);
 420   let x63: u64 = (x61 >> 8);
 421   let x64: u8 = ((x63 & (0xff as u64)) as u8);
 422   let x65: fiat_25519_u1 = ((x63 >> 8) as fiat_25519_u1);
 423   let x66: u64 = (x23 + (x65 as u64));
 424   let x67: u8 = ((x66 & (0xff as u64)) as u8);
 425   let x68: u64 = (x66 >> 8);
 426   let x69: u8 = ((x68 & (0xff as u64)) as u8);
 427   let x70: u64 = (x68 >> 8);
 428   let x71: u8 = ((x70 & (0xff as u64)) as u8);
 429   let x72: u64 = (x70 >> 8);
 430   let x73: u8 = ((x72 & (0xff as u64)) as u8);
 431   let x74: u64 = (x72 >> 8);
 432   let x75: u8 = ((x74 & (0xff as u64)) as u8);
 433   let x76: u64 = (x74 >> 8);
 434   let x77: u8 = ((x76 & (0xff as u64)) as u8);
 435   let x78: u8 = ((x76 >> 8) as u8);
 436   let x79: u64 = (x22 + (x78 as u64));
 437   let x80: u8 = ((x79 & (0xff as u64)) as u8);
 438   let x81: u64 = (x79 >> 8);
 439   let x82: u8 = ((x81 & (0xff as u64)) as u8);
 440   let x83: u64 = (x81 >> 8);
 441   let x84: u8 = ((x83 & (0xff as u64)) as u8);
 442   let x85: u64 = (x83 >> 8);
 443   let x86: u8 = ((x85 & (0xff as u64)) as u8);
 444   let x87: u64 = (x85 >> 8);
 445   let x88: u8 = ((x87 & (0xff as u64)) as u8);
 446   let x89: u64 = (x87 >> 8);
 447   let x90: u8 = ((x89 & (0xff as u64)) as u8);
 448   let x91: u8 = ((x89 >> 8) as u8);
 449   out1[0] = x26;
 450   out1[1] = x28;
 451   out1[2] = x30;
 452   out1[3] = x32;
 453   out1[4] = x34;
 454   out1[5] = x36;
 455   out1[6] = x39;
 456   out1[7] = x41;
 457   out1[8] = x43;
 458   out1[9] = x45;
 459   out1[10] = x47;
 460   out1[11] = x49;
 461   out1[12] = x52;
 462   out1[13] = x54;
 463   out1[14] = x56;
 464   out1[15] = x58;
 465   out1[16] = x60;
 466   out1[17] = x62;
 467   out1[18] = x64;
 468   out1[19] = x67;
 469   out1[20] = x69;
 470   out1[21] = x71;
 471   out1[22] = x73;
 472   out1[23] = x75;
 473   out1[24] = x77;
 474   out1[25] = x80;
 475   out1[26] = x82;
 476   out1[27] = x84;
 477   out1[28] = x86;
 478   out1[29] = x88;
 479   out1[30] = x90;
 480   out1[31] = x91;
 481 }
 482
 483 /// The function fiat_25519_from_bytes deserializes a field element from bytes in little-endian order.
 484 ///
 485 /// Postconditions:
 486 ///   eval out1 mod m = bytes_eval arg1 mod m
 487 ///
 488 /// Input Bounds:
 489 ///   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 ~> 0x7f]]
 490 #[inline]
 491 pub fn fiat_25519_from_bytes(out1: &mut fiat_25519_tight_field_element, arg1: &[u8; 32]) -> () {
 492   let x1: u64 = (((arg1[31]) as u64) << 44);
 493   let x2: u64 = (((arg1[30]) as u64) << 36);
 494   let x3: u64 = (((arg1[29]) as u64) << 28);
 495   let x4: u64 = (((arg1[28]) as u64) << 20);
 496   let x5: u64 = (((arg1[27]) as u64) << 12);
 497   let x6: u64 = (((arg1[26]) as u64) << 4);
 498   let x7: u64 = (((arg1[25]) as u64) << 47);
 499   let x8: u64 = (((arg1[24]) as u64) << 39);
 500   let x9: u64 = (((arg1[23]) as u64) << 31);
 501   let x10: u64 = (((arg1[22]) as u64) << 23);
 502   let x11: u64 = (((arg1[21]) as u64) << 15);
 503   let x12: u64 = (((arg1[20]) as u64) << 7);
 504   let x13: u64 = (((arg1[19]) as u64) << 50);
 505   let x14: u64 = (((arg1[18]) as u64) << 42);
 506   let x15: u64 = (((arg1[17]) as u64) << 34);
 507   let x16: u64 = (((arg1[16]) as u64) << 26);
 508   let x17: u64 = (((arg1[15]) as u64) << 18);
 509   let x18: u64 = (((arg1[14]) as u64) << 10);
 510   let x19: u64 = (((arg1[13]) as u64) << 2);
 511   let x20: u64 = (((arg1[12]) as u64) << 45);
 512   let x21: u64 = (((arg1[11]) as u64) << 37);
 513   let x22: u64 = (((arg1[10]) as u64) << 29);
 514   let x23: u64 = (((arg1[9]) as u64) << 21);
 515   let x24: u64 = (((arg1[8]) as u64) << 13);
 516   let x25: u64 = (((arg1[7]) as u64) << 5);
 517   let x26: u64 = (((arg1[6]) as u64) << 48);
 518   let x27: u64 = (((arg1[5]) as u64) << 40);
 519   let x28: u64 = (((arg1[4]) as u64) << 32);
 520   let x29: u64 = (((arg1[3]) as u64) << 24);
 521   let x30: u64 = (((arg1[2]) as u64) << 16);
 522   let x31: u64 = (((arg1[1]) as u64) << 8);
 523   let x32: u8 = (arg1[0]);
 524   let x33: u64 = (x31 + (x32 as u64));
 525   let x34: u64 = (x30 + x33);
 526   let x35: u64 = (x29 + x34);
 527   let x36: u64 = (x28 + x35);
 528   let x37: u64 = (x27 + x36);
 529   let x38: u64 = (x26 + x37);
 530   let x39: u64 = (x38 & 0x7ffffffffffff);
 531   let x40: u8 = ((x38 >> 51) as u8);
 532   let x41: u64 = (x25 + (x40 as u64));
 533   let x42: u64 = (x24 + x41);
 534   let x43: u64 = (x23 + x42);
 535   let x44: u64 = (x22 + x43);
 536   let x45: u64 = (x21 + x44);
 537   let x46: u64 = (x20 + x45);
 538   let x47: u64 = (x46 & 0x7ffffffffffff);
 539   let x48: u8 = ((x46 >> 51) as u8);
 540   let x49: u64 = (x19 + (x48 as u64));
 541   let x50: u64 = (x18 + x49);
 542   let x51: u64 = (x17 + x50);
 543   let x52: u64 = (x16 + x51);
 544   let x53: u64 = (x15 + x52);
 545   let x54: u64 = (x14 + x53);
 546   let x55: u64 = (x13 + x54);
 547   let x56: u64 = (x55 & 0x7ffffffffffff);
 548   let x57: u8 = ((x55 >> 51) as u8);
 549   let x58: u64 = (x12 + (x57 as u64));
 550   let x59: u64 = (x11 + x58);
 551   let x60: u64 = (x10 + x59);
 552   let x61: u64 = (x9 + x60);
 553   let x62: u64 = (x8 + x61);
 554   let x63: u64 = (x7 + x62);
 555   let x64: u64 = (x63 & 0x7ffffffffffff);
 556   let x65: u8 = ((x63 >> 51) as u8);
 557   let x66: u64 = (x6 + (x65 as u64));
 558   let x67: u64 = (x5 + x66);
 559   let x68: u64 = (x4 + x67);
 560   let x69: u64 = (x3 + x68);
 561   let x70: u64 = (x2 + x69);
 562   let x71: u64 = (x1 + x70);
 563   out1[0] = x39;
 564   out1[1] = x47;
 565   out1[2] = x56;
 566   out1[3] = x64;
 567   out1[4] = x71;
 568 }
 569
 570 /// The function fiat_25519_relax is the identity function converting from tight field elements to loose field elements.
 571 ///
 572 /// Postconditions:
 573 ///   out1 = arg1
 574 ///
 575 #[inline]
 576 pub fn fiat_25519_relax(out1: &mut fiat_25519_loose_field_element, arg1: &fiat_25519_tight_field_element) -> () {
 577   let x1: u64 = (arg1[0]);
 578   let x2: u64 = (arg1[1]);
 579   let x3: u64 = (arg1[2]);
 580   let x4: u64 = (arg1[3]);
 581   let x5: u64 = (arg1[4]);
 582   out1[0] = x1;
 583   out1[1] = x2;
 584   out1[2] = x3;
 585   out1[3] = x4;
 586   out1[4] = x5;
 587 }
 588
 589 /// The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
 590 ///
 591 /// Postconditions:
 592 ///   eval out1 mod m = (121666 * eval arg1) mod m
 593 ///
 594 #[inline]
 595 pub fn fiat_25519_carry_scmul_121666(out1: &mut fiat_25519_tight_field_element, arg1: &fiat_25519_loose_field_element) -> () {
 596   let x1: u128 = ((0x1db42 as u128) * ((arg1[4]) as u128));
 597   let x2: u128 = ((0x1db42 as u128) * ((arg1[3]) as u128));
 598   let x3: u128 = ((0x1db42 as u128) * ((arg1[2]) as u128));
 599   let x4: u128 = ((0x1db42 as u128) * ((arg1[1]) as u128));
 600   let x5: u128 = ((0x1db42 as u128) * ((arg1[0]) as u128));
 601   let x6: u64 = ((x5 >> 51) as u64);
 602   let x7: u64 = ((x5 & (0x7ffffffffffff as u128)) as u64);
 603   let x8: u128 = ((x6 as u128) + x4);
 604   let x9: u64 = ((x8 >> 51) as u64);
 605   let x10: u64 = ((x8 & (0x7ffffffffffff as u128)) as u64);
 606   let x11: u128 = ((x9 as u128) + x3);
 607   let x12: u64 = ((x11 >> 51) as u64);
 608   let x13: u64 = ((x11 & (0x7ffffffffffff as u128)) as u64);
 609   let x14: u128 = ((x12 as u128) + x2);
 610   let x15: u64 = ((x14 >> 51) as u64);
 611   let x16: u64 = ((x14 & (0x7ffffffffffff as u128)) as u64);
 612   let x17: u128 = ((x15 as u128) + x1);
 613   let x18: u64 = ((x17 >> 51) as u64);
 614   let x19: u64 = ((x17 & (0x7ffffffffffff as u128)) as u64);
 615   let x20: u64 = (x18 * 0x13);
 616   let x21: u64 = (x7 + x20);
 617   let x22: fiat_25519_u1 = ((x21 >> 51) as fiat_25519_u1);
 618   let x23: u64 = (x21 & 0x7ffffffffffff);
 619   let x24: u64 = ((x22 as u64) + x10);
 620   let x25: fiat_25519_u1 = ((x24 >> 51) as fiat_25519_u1);
 621   let x26: u64 = (x24 & 0x7ffffffffffff);
 622   let x27: u64 = ((x25 as u64) + x13);
 623   out1[0] = x23;
 624   out1[1] = x26;
 625   out1[2] = x27;
 626   out1[3] = x16;
 627   out1[4] = x19;
 628 }