1// Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --lang Zig --internal-static --public-function-case camelCase --private-function-case camelCase --public-type-case UpperCamelCase --private-type-case UpperCamelCase --no-prefix-fiat --package-name secp256k1_scalar '' 64 '2^256 - 432420386565659656852420866394968145599' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
   2// curve description (via package name): secp256k1_scalar
   3// machine_wordsize = 64 (from "64")
   4// requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp
   5// m = 0xfffffffffffffffffffffffffffffffebaaedce6af48a03bbfd25e8cd0364141 (from "2^256 - 432420386565659656852420866394968145599")
   6//
   7// NOTE: In addition to the bounds specified above each function, all
   8//   functions synthesized for this Montgomery arithmetic require the
   9//   input to be strictly less than the prime modulus (m), and also
  10//   require the input to be in the unique saturated representation.
  11//   All functions also ensure that these two properties are true of
  12//   return values.
  13//
  14// Computed values:
  15//   eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192)
  16//   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)
  17//   twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) in
  18//                            if x1 & (2^256-1) < 2^255 then x1 & (2^256-1) else (x1 & (2^256-1)) - 2^256
  19
  20const std = @import("std");
  21const mode = @import("builtin").mode; // Checked arithmetic is disabled in non-debug modes to avoid side channels
  22
  23// The type MontgomeryDomainFieldElement is a field element in the Montgomery domain.
  24// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  25pub const MontgomeryDomainFieldElement = [4]u64;
  26
  27// The type NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain.
  28// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  29pub const NonMontgomeryDomainFieldElement = [4]u64;
  30
  31/// The function addcarryxU64 is an addition with carry.
  32///
  33/// Postconditions:
  34///   out1 = (arg1 + arg2 + arg3) mod 2^64
  35///   out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
  36///
  37/// Input Bounds:
  38///   arg1: [0x0 ~> 0x1]
  39///   arg2: [0x0 ~> 0xffffffffffffffff]
  40///   arg3: [0x0 ~> 0xffffffffffffffff]
  41/// Output Bounds:
  42///   out1: [0x0 ~> 0xffffffffffffffff]
  43///   out2: [0x0 ~> 0x1]
  44fn addcarryxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
  45    const x = @as(u128, arg2) +% arg3 +% arg1;
  46    out1.* = @truncate(x);
  47    out2.* = @truncate(x >> 64);
  48}
  49
  50/// The function subborrowxU64 is a subtraction with borrow.
  51///
  52/// Postconditions:
  53///   out1 = (-arg1 + arg2 + -arg3) mod 2^64
  54///   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
  55///
  56/// Input Bounds:
  57///   arg1: [0x0 ~> 0x1]
  58///   arg2: [0x0 ~> 0xffffffffffffffff]
  59///   arg3: [0x0 ~> 0xffffffffffffffff]
  60/// Output Bounds:
  61///   out1: [0x0 ~> 0xffffffffffffffff]
  62///   out2: [0x0 ~> 0x1]
  63fn subborrowxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
  64    const x = @as(u128, arg2) -% arg3 -% arg1;
  65    out1.* = @truncate(x);
  66    out2.* = @truncate(x >> 64);
  67}
  68
  69/// The function mulxU64 is a multiplication, returning the full double-width result.
  70///
  71/// Postconditions:
  72///   out1 = (arg1 * arg2) mod 2^64
  73///   out2 = ⌊arg1 * arg2 / 2^64⌋
  74///
  75/// Input Bounds:
  76///   arg1: [0x0 ~> 0xffffffffffffffff]
  77///   arg2: [0x0 ~> 0xffffffffffffffff]
  78/// Output Bounds:
  79///   out1: [0x0 ~> 0xffffffffffffffff]
  80///   out2: [0x0 ~> 0xffffffffffffffff]
  81fn mulxU64(out1: *u64, out2: *u64, arg1: u64, arg2: u64) void {
  82    @setRuntimeSafety(mode == .Debug);
  83
  84    const x = @as(u128, arg1) * @as(u128, arg2);
  85    out1.* = @as(u64, @truncate(x));
  86    out2.* = @as(u64, @truncate(x >> 64));
  87}
  88
  89/// The function cmovznzU64 is a single-word conditional move.
  90///
  91/// Postconditions:
  92///   out1 = (if arg1 = 0 then arg2 else arg3)
  93///
  94/// Input Bounds:
  95///   arg1: [0x0 ~> 0x1]
  96///   arg2: [0x0 ~> 0xffffffffffffffff]
  97///   arg3: [0x0 ~> 0xffffffffffffffff]
  98/// Output Bounds:
  99///   out1: [0x0 ~> 0xffffffffffffffff]
 100fn cmovznzU64(out1: *u64, arg1: u1, arg2: u64, arg3: u64) void {
 101    @setRuntimeSafety(mode == .Debug);
 102
 103    const mask = 0 -% @as(u64, arg1);
 104    out1.* = (mask & arg3) | ((~mask) & arg2);
 105}
 106
 107/// The function mul multiplies two field elements in the Montgomery domain.
 108///
 109/// Preconditions:
 110///   0 ≤ eval arg1 < m
 111///   0 ≤ eval arg2 < m
 112/// Postconditions:
 113///   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
 114///   0 ≤ eval out1 < m
 115///
 116pub fn mul(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
 117    @setRuntimeSafety(mode == .Debug);
 118
 119    const x1 = (arg1[1]);
 120    const x2 = (arg1[2]);
 121    const x3 = (arg1[3]);
 122    const x4 = (arg1[0]);
 123    var x5: u64 = undefined;
 124    var x6: u64 = undefined;
 125    mulxU64(&x5, &x6, x4, (arg2[3]));
 126    var x7: u64 = undefined;
 127    var x8: u64 = undefined;
 128    mulxU64(&x7, &x8, x4, (arg2[2]));
 129    var x9: u64 = undefined;
 130    var x10: u64 = undefined;
 131    mulxU64(&x9, &x10, x4, (arg2[1]));
 132    var x11: u64 = undefined;
 133    var x12: u64 = undefined;
 134    mulxU64(&x11, &x12, x4, (arg2[0]));
 135    var x13: u64 = undefined;
 136    var x14: u1 = undefined;
 137    addcarryxU64(&x13, &x14, 0x0, x12, x9);
 138    var x15: u64 = undefined;
 139    var x16: u1 = undefined;
 140    addcarryxU64(&x15, &x16, x14, x10, x7);
 141    var x17: u64 = undefined;
 142    var x18: u1 = undefined;
 143    addcarryxU64(&x17, &x18, x16, x8, x5);
 144    const x19 = (@as(u64, x18) + x6);
 145    var x20: u64 = undefined;
 146    var x21: u64 = undefined;
 147    mulxU64(&x20, &x21, x11, 0x4b0dff665588b13f);
 148    var x22: u64 = undefined;
 149    var x23: u64 = undefined;
 150    mulxU64(&x22, &x23, x20, 0xffffffffffffffff);
 151    var x24: u64 = undefined;
 152    var x25: u64 = undefined;
 153    mulxU64(&x24, &x25, x20, 0xfffffffffffffffe);
 154    var x26: u64 = undefined;
 155    var x27: u64 = undefined;
 156    mulxU64(&x26, &x27, x20, 0xbaaedce6af48a03b);
 157    var x28: u64 = undefined;
 158    var x29: u64 = undefined;
 159    mulxU64(&x28, &x29, x20, 0xbfd25e8cd0364141);
 160    var x30: u64 = undefined;
 161    var x31: u1 = undefined;
 162    addcarryxU64(&x30, &x31, 0x0, x29, x26);
 163    var x32: u64 = undefined;
 164    var x33: u1 = undefined;
 165    addcarryxU64(&x32, &x33, x31, x27, x24);
 166    var x34: u64 = undefined;
 167    var x35: u1 = undefined;
 168    addcarryxU64(&x34, &x35, x33, x25, x22);
 169    const x36 = (@as(u64, x35) + x23);
 170    var x37: u64 = undefined;
 171    var x38: u1 = undefined;
 172    addcarryxU64(&x37, &x38, 0x0, x11, x28);
 173    var x39: u64 = undefined;
 174    var x40: u1 = undefined;
 175    addcarryxU64(&x39, &x40, x38, x13, x30);
 176    var x41: u64 = undefined;
 177    var x42: u1 = undefined;
 178    addcarryxU64(&x41, &x42, x40, x15, x32);
 179    var x43: u64 = undefined;
 180    var x44: u1 = undefined;
 181    addcarryxU64(&x43, &x44, x42, x17, x34);
 182    var x45: u64 = undefined;
 183    var x46: u1 = undefined;
 184    addcarryxU64(&x45, &x46, x44, x19, x36);
 185    var x47: u64 = undefined;
 186    var x48: u64 = undefined;
 187    mulxU64(&x47, &x48, x1, (arg2[3]));
 188    var x49: u64 = undefined;
 189    var x50: u64 = undefined;
 190    mulxU64(&x49, &x50, x1, (arg2[2]));
 191    var x51: u64 = undefined;
 192    var x52: u64 = undefined;
 193    mulxU64(&x51, &x52, x1, (arg2[1]));
 194    var x53: u64 = undefined;
 195    var x54: u64 = undefined;
 196    mulxU64(&x53, &x54, x1, (arg2[0]));
 197    var x55: u64 = undefined;
 198    var x56: u1 = undefined;
 199    addcarryxU64(&x55, &x56, 0x0, x54, x51);
 200    var x57: u64 = undefined;
 201    var x58: u1 = undefined;
 202    addcarryxU64(&x57, &x58, x56, x52, x49);
 203    var x59: u64 = undefined;
 204    var x60: u1 = undefined;
 205    addcarryxU64(&x59, &x60, x58, x50, x47);
 206    const x61 = (@as(u64, x60) + x48);
 207    var x62: u64 = undefined;
 208    var x63: u1 = undefined;
 209    addcarryxU64(&x62, &x63, 0x0, x39, x53);
 210    var x64: u64 = undefined;
 211    var x65: u1 = undefined;
 212    addcarryxU64(&x64, &x65, x63, x41, x55);
 213    var x66: u64 = undefined;
 214    var x67: u1 = undefined;
 215    addcarryxU64(&x66, &x67, x65, x43, x57);
 216    var x68: u64 = undefined;
 217    var x69: u1 = undefined;
 218    addcarryxU64(&x68, &x69, x67, x45, x59);
 219    var x70: u64 = undefined;
 220    var x71: u1 = undefined;
 221    addcarryxU64(&x70, &x71, x69, @as(u64, x46), x61);
 222    var x72: u64 = undefined;
 223    var x73: u64 = undefined;
 224    mulxU64(&x72, &x73, x62, 0x4b0dff665588b13f);
 225    var x74: u64 = undefined;
 226    var x75: u64 = undefined;
 227    mulxU64(&x74, &x75, x72, 0xffffffffffffffff);
 228    var x76: u64 = undefined;
 229    var x77: u64 = undefined;
 230    mulxU64(&x76, &x77, x72, 0xfffffffffffffffe);
 231    var x78: u64 = undefined;
 232    var x79: u64 = undefined;
 233    mulxU64(&x78, &x79, x72, 0xbaaedce6af48a03b);
 234    var x80: u64 = undefined;
 235    var x81: u64 = undefined;
 236    mulxU64(&x80, &x81, x72, 0xbfd25e8cd0364141);
 237    var x82: u64 = undefined;
 238    var x83: u1 = undefined;
 239    addcarryxU64(&x82, &x83, 0x0, x81, x78);
 240    var x84: u64 = undefined;
 241    var x85: u1 = undefined;
 242    addcarryxU64(&x84, &x85, x83, x79, x76);
 243    var x86: u64 = undefined;
 244    var x87: u1 = undefined;
 245    addcarryxU64(&x86, &x87, x85, x77, x74);
 246    const x88 = (@as(u64, x87) + x75);
 247    var x89: u64 = undefined;
 248    var x90: u1 = undefined;
 249    addcarryxU64(&x89, &x90, 0x0, x62, x80);
 250    var x91: u64 = undefined;
 251    var x92: u1 = undefined;
 252    addcarryxU64(&x91, &x92, x90, x64, x82);
 253    var x93: u64 = undefined;
 254    var x94: u1 = undefined;
 255    addcarryxU64(&x93, &x94, x92, x66, x84);
 256    var x95: u64 = undefined;
 257    var x96: u1 = undefined;
 258    addcarryxU64(&x95, &x96, x94, x68, x86);
 259    var x97: u64 = undefined;
 260    var x98: u1 = undefined;
 261    addcarryxU64(&x97, &x98, x96, x70, x88);
 262    const x99 = (@as(u64, x98) + @as(u64, x71));
 263    var x100: u64 = undefined;
 264    var x101: u64 = undefined;
 265    mulxU64(&x100, &x101, x2, (arg2[3]));
 266    var x102: u64 = undefined;
 267    var x103: u64 = undefined;
 268    mulxU64(&x102, &x103, x2, (arg2[2]));
 269    var x104: u64 = undefined;
 270    var x105: u64 = undefined;
 271    mulxU64(&x104, &x105, x2, (arg2[1]));
 272    var x106: u64 = undefined;
 273    var x107: u64 = undefined;
 274    mulxU64(&x106, &x107, x2, (arg2[0]));
 275    var x108: u64 = undefined;
 276    var x109: u1 = undefined;
 277    addcarryxU64(&x108, &x109, 0x0, x107, x104);
 278    var x110: u64 = undefined;
 279    var x111: u1 = undefined;
 280    addcarryxU64(&x110, &x111, x109, x105, x102);
 281    var x112: u64 = undefined;
 282    var x113: u1 = undefined;
 283    addcarryxU64(&x112, &x113, x111, x103, x100);
 284    const x114 = (@as(u64, x113) + x101);
 285    var x115: u64 = undefined;
 286    var x116: u1 = undefined;
 287    addcarryxU64(&x115, &x116, 0x0, x91, x106);
 288    var x117: u64 = undefined;
 289    var x118: u1 = undefined;
 290    addcarryxU64(&x117, &x118, x116, x93, x108);
 291    var x119: u64 = undefined;
 292    var x120: u1 = undefined;
 293    addcarryxU64(&x119, &x120, x118, x95, x110);
 294    var x121: u64 = undefined;
 295    var x122: u1 = undefined;
 296    addcarryxU64(&x121, &x122, x120, x97, x112);
 297    var x123: u64 = undefined;
 298    var x124: u1 = undefined;
 299    addcarryxU64(&x123, &x124, x122, x99, x114);
 300    var x125: u64 = undefined;
 301    var x126: u64 = undefined;
 302    mulxU64(&x125, &x126, x115, 0x4b0dff665588b13f);
 303    var x127: u64 = undefined;
 304    var x128: u64 = undefined;
 305    mulxU64(&x127, &x128, x125, 0xffffffffffffffff);
 306    var x129: u64 = undefined;
 307    var x130: u64 = undefined;
 308    mulxU64(&x129, &x130, x125, 0xfffffffffffffffe);
 309    var x131: u64 = undefined;
 310    var x132: u64 = undefined;
 311    mulxU64(&x131, &x132, x125, 0xbaaedce6af48a03b);
 312    var x133: u64 = undefined;
 313    var x134: u64 = undefined;
 314    mulxU64(&x133, &x134, x125, 0xbfd25e8cd0364141);
 315    var x135: u64 = undefined;
 316    var x136: u1 = undefined;
 317    addcarryxU64(&x135, &x136, 0x0, x134, x131);
 318    var x137: u64 = undefined;
 319    var x138: u1 = undefined;
 320    addcarryxU64(&x137, &x138, x136, x132, x129);
 321    var x139: u64 = undefined;
 322    var x140: u1 = undefined;
 323    addcarryxU64(&x139, &x140, x138, x130, x127);
 324    const x141 = (@as(u64, x140) + x128);
 325    var x142: u64 = undefined;
 326    var x143: u1 = undefined;
 327    addcarryxU64(&x142, &x143, 0x0, x115, x133);
 328    var x144: u64 = undefined;
 329    var x145: u1 = undefined;
 330    addcarryxU64(&x144, &x145, x143, x117, x135);
 331    var x146: u64 = undefined;
 332    var x147: u1 = undefined;
 333    addcarryxU64(&x146, &x147, x145, x119, x137);
 334    var x148: u64 = undefined;
 335    var x149: u1 = undefined;
 336    addcarryxU64(&x148, &x149, x147, x121, x139);
 337    var x150: u64 = undefined;
 338    var x151: u1 = undefined;
 339    addcarryxU64(&x150, &x151, x149, x123, x141);
 340    const x152 = (@as(u64, x151) + @as(u64, x124));
 341    var x153: u64 = undefined;
 342    var x154: u64 = undefined;
 343    mulxU64(&x153, &x154, x3, (arg2[3]));
 344    var x155: u64 = undefined;
 345    var x156: u64 = undefined;
 346    mulxU64(&x155, &x156, x3, (arg2[2]));
 347    var x157: u64 = undefined;
 348    var x158: u64 = undefined;
 349    mulxU64(&x157, &x158, x3, (arg2[1]));
 350    var x159: u64 = undefined;
 351    var x160: u64 = undefined;
 352    mulxU64(&x159, &x160, x3, (arg2[0]));
 353    var x161: u64 = undefined;
 354    var x162: u1 = undefined;
 355    addcarryxU64(&x161, &x162, 0x0, x160, x157);
 356    var x163: u64 = undefined;
 357    var x164: u1 = undefined;
 358    addcarryxU64(&x163, &x164, x162, x158, x155);
 359    var x165: u64 = undefined;
 360    var x166: u1 = undefined;
 361    addcarryxU64(&x165, &x166, x164, x156, x153);
 362    const x167 = (@as(u64, x166) + x154);
 363    var x168: u64 = undefined;
 364    var x169: u1 = undefined;
 365    addcarryxU64(&x168, &x169, 0x0, x144, x159);
 366    var x170: u64 = undefined;
 367    var x171: u1 = undefined;
 368    addcarryxU64(&x170, &x171, x169, x146, x161);
 369    var x172: u64 = undefined;
 370    var x173: u1 = undefined;
 371    addcarryxU64(&x172, &x173, x171, x148, x163);
 372    var x174: u64 = undefined;
 373    var x175: u1 = undefined;
 374    addcarryxU64(&x174, &x175, x173, x150, x165);
 375    var x176: u64 = undefined;
 376    var x177: u1 = undefined;
 377    addcarryxU64(&x176, &x177, x175, x152, x167);
 378    var x178: u64 = undefined;
 379    var x179: u64 = undefined;
 380    mulxU64(&x178, &x179, x168, 0x4b0dff665588b13f);
 381    var x180: u64 = undefined;
 382    var x181: u64 = undefined;
 383    mulxU64(&x180, &x181, x178, 0xffffffffffffffff);
 384    var x182: u64 = undefined;
 385    var x183: u64 = undefined;
 386    mulxU64(&x182, &x183, x178, 0xfffffffffffffffe);
 387    var x184: u64 = undefined;
 388    var x185: u64 = undefined;
 389    mulxU64(&x184, &x185, x178, 0xbaaedce6af48a03b);
 390    var x186: u64 = undefined;
 391    var x187: u64 = undefined;
 392    mulxU64(&x186, &x187, x178, 0xbfd25e8cd0364141);
 393    var x188: u64 = undefined;
 394    var x189: u1 = undefined;
 395    addcarryxU64(&x188, &x189, 0x0, x187, x184);
 396    var x190: u64 = undefined;
 397    var x191: u1 = undefined;
 398    addcarryxU64(&x190, &x191, x189, x185, x182);
 399    var x192: u64 = undefined;
 400    var x193: u1 = undefined;
 401    addcarryxU64(&x192, &x193, x191, x183, x180);
 402    const x194 = (@as(u64, x193) + x181);
 403    var x195: u64 = undefined;
 404    var x196: u1 = undefined;
 405    addcarryxU64(&x195, &x196, 0x0, x168, x186);
 406    var x197: u64 = undefined;
 407    var x198: u1 = undefined;
 408    addcarryxU64(&x197, &x198, x196, x170, x188);
 409    var x199: u64 = undefined;
 410    var x200: u1 = undefined;
 411    addcarryxU64(&x199, &x200, x198, x172, x190);
 412    var x201: u64 = undefined;
 413    var x202: u1 = undefined;
 414    addcarryxU64(&x201, &x202, x200, x174, x192);
 415    var x203: u64 = undefined;
 416    var x204: u1 = undefined;
 417    addcarryxU64(&x203, &x204, x202, x176, x194);
 418    const x205 = (@as(u64, x204) + @as(u64, x177));
 419    var x206: u64 = undefined;
 420    var x207: u1 = undefined;
 421    subborrowxU64(&x206, &x207, 0x0, x197, 0xbfd25e8cd0364141);
 422    var x208: u64 = undefined;
 423    var x209: u1 = undefined;
 424    subborrowxU64(&x208, &x209, x207, x199, 0xbaaedce6af48a03b);
 425    var x210: u64 = undefined;
 426    var x211: u1 = undefined;
 427    subborrowxU64(&x210, &x211, x209, x201, 0xfffffffffffffffe);
 428    var x212: u64 = undefined;
 429    var x213: u1 = undefined;
 430    subborrowxU64(&x212, &x213, x211, x203, 0xffffffffffffffff);
 431    var x214: u64 = undefined;
 432    var x215: u1 = undefined;
 433    subborrowxU64(&x214, &x215, x213, x205, 0x0);
 434    var x216: u64 = undefined;
 435    cmovznzU64(&x216, x215, x206, x197);
 436    var x217: u64 = undefined;
 437    cmovznzU64(&x217, x215, x208, x199);
 438    var x218: u64 = undefined;
 439    cmovznzU64(&x218, x215, x210, x201);
 440    var x219: u64 = undefined;
 441    cmovznzU64(&x219, x215, x212, x203);
 442    out1[0] = x216;
 443    out1[1] = x217;
 444    out1[2] = x218;
 445    out1[3] = x219;
 446}
 447
 448/// The function square squares a field element in the Montgomery domain.
 449///
 450/// Preconditions:
 451///   0 ≤ eval arg1 < m
 452/// Postconditions:
 453///   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
 454///   0 ≤ eval out1 < m
 455///
 456pub fn square(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
 457    @setRuntimeSafety(mode == .Debug);
 458
 459    const x1 = (arg1[1]);
 460    const x2 = (arg1[2]);
 461    const x3 = (arg1[3]);
 462    const x4 = (arg1[0]);
 463    var x5: u64 = undefined;
 464    var x6: u64 = undefined;
 465    mulxU64(&x5, &x6, x4, (arg1[3]));
 466    var x7: u64 = undefined;
 467    var x8: u64 = undefined;
 468    mulxU64(&x7, &x8, x4, (arg1[2]));
 469    var x9: u64 = undefined;
 470    var x10: u64 = undefined;
 471    mulxU64(&x9, &x10, x4, (arg1[1]));
 472    var x11: u64 = undefined;
 473    var x12: u64 = undefined;
 474    mulxU64(&x11, &x12, x4, (arg1[0]));
 475    var x13: u64 = undefined;
 476    var x14: u1 = undefined;
 477    addcarryxU64(&x13, &x14, 0x0, x12, x9);
 478    var x15: u64 = undefined;
 479    var x16: u1 = undefined;
 480    addcarryxU64(&x15, &x16, x14, x10, x7);
 481    var x17: u64 = undefined;
 482    var x18: u1 = undefined;
 483    addcarryxU64(&x17, &x18, x16, x8, x5);
 484    const x19 = (@as(u64, x18) + x6);
 485    var x20: u64 = undefined;
 486    var x21: u64 = undefined;
 487    mulxU64(&x20, &x21, x11, 0x4b0dff665588b13f);
 488    var x22: u64 = undefined;
 489    var x23: u64 = undefined;
 490    mulxU64(&x22, &x23, x20, 0xffffffffffffffff);
 491    var x24: u64 = undefined;
 492    var x25: u64 = undefined;
 493    mulxU64(&x24, &x25, x20, 0xfffffffffffffffe);
 494    var x26: u64 = undefined;
 495    var x27: u64 = undefined;
 496    mulxU64(&x26, &x27, x20, 0xbaaedce6af48a03b);
 497    var x28: u64 = undefined;
 498    var x29: u64 = undefined;
 499    mulxU64(&x28, &x29, x20, 0xbfd25e8cd0364141);
 500    var x30: u64 = undefined;
 501    var x31: u1 = undefined;
 502    addcarryxU64(&x30, &x31, 0x0, x29, x26);
 503    var x32: u64 = undefined;
 504    var x33: u1 = undefined;
 505    addcarryxU64(&x32, &x33, x31, x27, x24);
 506    var x34: u64 = undefined;
 507    var x35: u1 = undefined;
 508    addcarryxU64(&x34, &x35, x33, x25, x22);
 509    const x36 = (@as(u64, x35) + x23);
 510    var x37: u64 = undefined;
 511    var x38: u1 = undefined;
 512    addcarryxU64(&x37, &x38, 0x0, x11, x28);
 513    var x39: u64 = undefined;
 514    var x40: u1 = undefined;
 515    addcarryxU64(&x39, &x40, x38, x13, x30);
 516    var x41: u64 = undefined;
 517    var x42: u1 = undefined;
 518    addcarryxU64(&x41, &x42, x40, x15, x32);
 519    var x43: u64 = undefined;
 520    var x44: u1 = undefined;
 521    addcarryxU64(&x43, &x44, x42, x17, x34);
 522    var x45: u64 = undefined;
 523    var x46: u1 = undefined;
 524    addcarryxU64(&x45, &x46, x44, x19, x36);
 525    var x47: u64 = undefined;
 526    var x48: u64 = undefined;
 527    mulxU64(&x47, &x48, x1, (arg1[3]));
 528    var x49: u64 = undefined;
 529    var x50: u64 = undefined;
 530    mulxU64(&x49, &x50, x1, (arg1[2]));
 531    var x51: u64 = undefined;
 532    var x52: u64 = undefined;
 533    mulxU64(&x51, &x52, x1, (arg1[1]));
 534    var x53: u64 = undefined;
 535    var x54: u64 = undefined;
 536    mulxU64(&x53, &x54, x1, (arg1[0]));
 537    var x55: u64 = undefined;
 538    var x56: u1 = undefined;
 539    addcarryxU64(&x55, &x56, 0x0, x54, x51);
 540    var x57: u64 = undefined;
 541    var x58: u1 = undefined;
 542    addcarryxU64(&x57, &x58, x56, x52, x49);
 543    var x59: u64 = undefined;
 544    var x60: u1 = undefined;
 545    addcarryxU64(&x59, &x60, x58, x50, x47);
 546    const x61 = (@as(u64, x60) + x48);
 547    var x62: u64 = undefined;
 548    var x63: u1 = undefined;
 549    addcarryxU64(&x62, &x63, 0x0, x39, x53);
 550    var x64: u64 = undefined;
 551    var x65: u1 = undefined;
 552    addcarryxU64(&x64, &x65, x63, x41, x55);
 553    var x66: u64 = undefined;
 554    var x67: u1 = undefined;
 555    addcarryxU64(&x66, &x67, x65, x43, x57);
 556    var x68: u64 = undefined;
 557    var x69: u1 = undefined;
 558    addcarryxU64(&x68, &x69, x67, x45, x59);
 559    var x70: u64 = undefined;
 560    var x71: u1 = undefined;
 561    addcarryxU64(&x70, &x71, x69, @as(u64, x46), x61);
 562    var x72: u64 = undefined;
 563    var x73: u64 = undefined;
 564    mulxU64(&x72, &x73, x62, 0x4b0dff665588b13f);
 565    var x74: u64 = undefined;
 566    var x75: u64 = undefined;
 567    mulxU64(&x74, &x75, x72, 0xffffffffffffffff);
 568    var x76: u64 = undefined;
 569    var x77: u64 = undefined;
 570    mulxU64(&x76, &x77, x72, 0xfffffffffffffffe);
 571    var x78: u64 = undefined;
 572    var x79: u64 = undefined;
 573    mulxU64(&x78, &x79, x72, 0xbaaedce6af48a03b);
 574    var x80: u64 = undefined;
 575    var x81: u64 = undefined;
 576    mulxU64(&x80, &x81, x72, 0xbfd25e8cd0364141);
 577    var x82: u64 = undefined;
 578    var x83: u1 = undefined;
 579    addcarryxU64(&x82, &x83, 0x0, x81, x78);
 580    var x84: u64 = undefined;
 581    var x85: u1 = undefined;
 582    addcarryxU64(&x84, &x85, x83, x79, x76);
 583    var x86: u64 = undefined;
 584    var x87: u1 = undefined;
 585    addcarryxU64(&x86, &x87, x85, x77, x74);
 586    const x88 = (@as(u64, x87) + x75);
 587    var x89: u64 = undefined;
 588    var x90: u1 = undefined;
 589    addcarryxU64(&x89, &x90, 0x0, x62, x80);
 590    var x91: u64 = undefined;
 591    var x92: u1 = undefined;
 592    addcarryxU64(&x91, &x92, x90, x64, x82);
 593    var x93: u64 = undefined;
 594    var x94: u1 = undefined;
 595    addcarryxU64(&x93, &x94, x92, x66, x84);
 596    var x95: u64 = undefined;
 597    var x96: u1 = undefined;
 598    addcarryxU64(&x95, &x96, x94, x68, x86);
 599    var x97: u64 = undefined;
 600    var x98: u1 = undefined;
 601    addcarryxU64(&x97, &x98, x96, x70, x88);
 602    const x99 = (@as(u64, x98) + @as(u64, x71));
 603    var x100: u64 = undefined;
 604    var x101: u64 = undefined;
 605    mulxU64(&x100, &x101, x2, (arg1[3]));
 606    var x102: u64 = undefined;
 607    var x103: u64 = undefined;
 608    mulxU64(&x102, &x103, x2, (arg1[2]));
 609    var x104: u64 = undefined;
 610    var x105: u64 = undefined;
 611    mulxU64(&x104, &x105, x2, (arg1[1]));
 612    var x106: u64 = undefined;
 613    var x107: u64 = undefined;
 614    mulxU64(&x106, &x107, x2, (arg1[0]));
 615    var x108: u64 = undefined;
 616    var x109: u1 = undefined;
 617    addcarryxU64(&x108, &x109, 0x0, x107, x104);
 618    var x110: u64 = undefined;
 619    var x111: u1 = undefined;
 620    addcarryxU64(&x110, &x111, x109, x105, x102);
 621    var x112: u64 = undefined;
 622    var x113: u1 = undefined;
 623    addcarryxU64(&x112, &x113, x111, x103, x100);
 624    const x114 = (@as(u64, x113) + x101);
 625    var x115: u64 = undefined;
 626    var x116: u1 = undefined;
 627    addcarryxU64(&x115, &x116, 0x0, x91, x106);
 628    var x117: u64 = undefined;
 629    var x118: u1 = undefined;
 630    addcarryxU64(&x117, &x118, x116, x93, x108);
 631    var x119: u64 = undefined;
 632    var x120: u1 = undefined;
 633    addcarryxU64(&x119, &x120, x118, x95, x110);
 634    var x121: u64 = undefined;
 635    var x122: u1 = undefined;
 636    addcarryxU64(&x121, &x122, x120, x97, x112);
 637    var x123: u64 = undefined;
 638    var x124: u1 = undefined;
 639    addcarryxU64(&x123, &x124, x122, x99, x114);
 640    var x125: u64 = undefined;
 641    var x126: u64 = undefined;
 642    mulxU64(&x125, &x126, x115, 0x4b0dff665588b13f);
 643    var x127: u64 = undefined;
 644    var x128: u64 = undefined;
 645    mulxU64(&x127, &x128, x125, 0xffffffffffffffff);
 646    var x129: u64 = undefined;
 647    var x130: u64 = undefined;
 648    mulxU64(&x129, &x130, x125, 0xfffffffffffffffe);
 649    var x131: u64 = undefined;
 650    var x132: u64 = undefined;
 651    mulxU64(&x131, &x132, x125, 0xbaaedce6af48a03b);
 652    var x133: u64 = undefined;
 653    var x134: u64 = undefined;
 654    mulxU64(&x133, &x134, x125, 0xbfd25e8cd0364141);
 655    var x135: u64 = undefined;
 656    var x136: u1 = undefined;
 657    addcarryxU64(&x135, &x136, 0x0, x134, x131);
 658    var x137: u64 = undefined;
 659    var x138: u1 = undefined;
 660    addcarryxU64(&x137, &x138, x136, x132, x129);
 661    var x139: u64 = undefined;
 662    var x140: u1 = undefined;
 663    addcarryxU64(&x139, &x140, x138, x130, x127);
 664    const x141 = (@as(u64, x140) + x128);
 665    var x142: u64 = undefined;
 666    var x143: u1 = undefined;
 667    addcarryxU64(&x142, &x143, 0x0, x115, x133);
 668    var x144: u64 = undefined;
 669    var x145: u1 = undefined;
 670    addcarryxU64(&x144, &x145, x143, x117, x135);
 671    var x146: u64 = undefined;
 672    var x147: u1 = undefined;
 673    addcarryxU64(&x146, &x147, x145, x119, x137);
 674    var x148: u64 = undefined;
 675    var x149: u1 = undefined;
 676    addcarryxU64(&x148, &x149, x147, x121, x139);
 677    var x150: u64 = undefined;
 678    var x151: u1 = undefined;
 679    addcarryxU64(&x150, &x151, x149, x123, x141);
 680    const x152 = (@as(u64, x151) + @as(u64, x124));
 681    var x153: u64 = undefined;
 682    var x154: u64 = undefined;
 683    mulxU64(&x153, &x154, x3, (arg1[3]));
 684    var x155: u64 = undefined;
 685    var x156: u64 = undefined;
 686    mulxU64(&x155, &x156, x3, (arg1[2]));
 687    var x157: u64 = undefined;
 688    var x158: u64 = undefined;
 689    mulxU64(&x157, &x158, x3, (arg1[1]));
 690    var x159: u64 = undefined;
 691    var x160: u64 = undefined;
 692    mulxU64(&x159, &x160, x3, (arg1[0]));
 693    var x161: u64 = undefined;
 694    var x162: u1 = undefined;
 695    addcarryxU64(&x161, &x162, 0x0, x160, x157);
 696    var x163: u64 = undefined;
 697    var x164: u1 = undefined;
 698    addcarryxU64(&x163, &x164, x162, x158, x155);
 699    var x165: u64 = undefined;
 700    var x166: u1 = undefined;
 701    addcarryxU64(&x165, &x166, x164, x156, x153);
 702    const x167 = (@as(u64, x166) + x154);
 703    var x168: u64 = undefined;
 704    var x169: u1 = undefined;
 705    addcarryxU64(&x168, &x169, 0x0, x144, x159);
 706    var x170: u64 = undefined;
 707    var x171: u1 = undefined;
 708    addcarryxU64(&x170, &x171, x169, x146, x161);
 709    var x172: u64 = undefined;
 710    var x173: u1 = undefined;
 711    addcarryxU64(&x172, &x173, x171, x148, x163);
 712    var x174: u64 = undefined;
 713    var x175: u1 = undefined;
 714    addcarryxU64(&x174, &x175, x173, x150, x165);
 715    var x176: u64 = undefined;
 716    var x177: u1 = undefined;
 717    addcarryxU64(&x176, &x177, x175, x152, x167);
 718    var x178: u64 = undefined;
 719    var x179: u64 = undefined;
 720    mulxU64(&x178, &x179, x168, 0x4b0dff665588b13f);
 721    var x180: u64 = undefined;
 722    var x181: u64 = undefined;
 723    mulxU64(&x180, &x181, x178, 0xffffffffffffffff);
 724    var x182: u64 = undefined;
 725    var x183: u64 = undefined;
 726    mulxU64(&x182, &x183, x178, 0xfffffffffffffffe);
 727    var x184: u64 = undefined;
 728    var x185: u64 = undefined;
 729    mulxU64(&x184, &x185, x178, 0xbaaedce6af48a03b);
 730    var x186: u64 = undefined;
 731    var x187: u64 = undefined;
 732    mulxU64(&x186, &x187, x178, 0xbfd25e8cd0364141);
 733    var x188: u64 = undefined;
 734    var x189: u1 = undefined;
 735    addcarryxU64(&x188, &x189, 0x0, x187, x184);
 736    var x190: u64 = undefined;
 737    var x191: u1 = undefined;
 738    addcarryxU64(&x190, &x191, x189, x185, x182);
 739    var x192: u64 = undefined;
 740    var x193: u1 = undefined;
 741    addcarryxU64(&x192, &x193, x191, x183, x180);
 742    const x194 = (@as(u64, x193) + x181);
 743    var x195: u64 = undefined;
 744    var x196: u1 = undefined;
 745    addcarryxU64(&x195, &x196, 0x0, x168, x186);
 746    var x197: u64 = undefined;
 747    var x198: u1 = undefined;
 748    addcarryxU64(&x197, &x198, x196, x170, x188);
 749    var x199: u64 = undefined;
 750    var x200: u1 = undefined;
 751    addcarryxU64(&x199, &x200, x198, x172, x190);
 752    var x201: u64 = undefined;
 753    var x202: u1 = undefined;
 754    addcarryxU64(&x201, &x202, x200, x174, x192);
 755    var x203: u64 = undefined;
 756    var x204: u1 = undefined;
 757    addcarryxU64(&x203, &x204, x202, x176, x194);
 758    const x205 = (@as(u64, x204) + @as(u64, x177));
 759    var x206: u64 = undefined;
 760    var x207: u1 = undefined;
 761    subborrowxU64(&x206, &x207, 0x0, x197, 0xbfd25e8cd0364141);
 762    var x208: u64 = undefined;
 763    var x209: u1 = undefined;
 764    subborrowxU64(&x208, &x209, x207, x199, 0xbaaedce6af48a03b);
 765    var x210: u64 = undefined;
 766    var x211: u1 = undefined;
 767    subborrowxU64(&x210, &x211, x209, x201, 0xfffffffffffffffe);
 768    var x212: u64 = undefined;
 769    var x213: u1 = undefined;
 770    subborrowxU64(&x212, &x213, x211, x203, 0xffffffffffffffff);
 771    var x214: u64 = undefined;
 772    var x215: u1 = undefined;
 773    subborrowxU64(&x214, &x215, x213, x205, 0x0);
 774    var x216: u64 = undefined;
 775    cmovznzU64(&x216, x215, x206, x197);
 776    var x217: u64 = undefined;
 777    cmovznzU64(&x217, x215, x208, x199);
 778    var x218: u64 = undefined;
 779    cmovznzU64(&x218, x215, x210, x201);
 780    var x219: u64 = undefined;
 781    cmovznzU64(&x219, x215, x212, x203);
 782    out1[0] = x216;
 783    out1[1] = x217;
 784    out1[2] = x218;
 785    out1[3] = x219;
 786}
 787
 788/// The function add adds two field elements in the Montgomery domain.
 789///
 790/// Preconditions:
 791///   0 ≤ eval arg1 < m
 792///   0 ≤ eval arg2 < m
 793/// Postconditions:
 794///   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
 795///   0 ≤ eval out1 < m
 796///
 797pub fn add(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
 798    @setRuntimeSafety(mode == .Debug);
 799
 800    var x1: u64 = undefined;
 801    var x2: u1 = undefined;
 802    addcarryxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
 803    var x3: u64 = undefined;
 804    var x4: u1 = undefined;
 805    addcarryxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
 806    var x5: u64 = undefined;
 807    var x6: u1 = undefined;
 808    addcarryxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
 809    var x7: u64 = undefined;
 810    var x8: u1 = undefined;
 811    addcarryxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
 812    var x9: u64 = undefined;
 813    var x10: u1 = undefined;
 814    subborrowxU64(&x9, &x10, 0x0, x1, 0xbfd25e8cd0364141);
 815    var x11: u64 = undefined;
 816    var x12: u1 = undefined;
 817    subborrowxU64(&x11, &x12, x10, x3, 0xbaaedce6af48a03b);
 818    var x13: u64 = undefined;
 819    var x14: u1 = undefined;
 820    subborrowxU64(&x13, &x14, x12, x5, 0xfffffffffffffffe);
 821    var x15: u64 = undefined;
 822    var x16: u1 = undefined;
 823    subborrowxU64(&x15, &x16, x14, x7, 0xffffffffffffffff);
 824    var x17: u64 = undefined;
 825    var x18: u1 = undefined;
 826    subborrowxU64(&x17, &x18, x16, @as(u64, x8), 0x0);
 827    var x19: u64 = undefined;
 828    cmovznzU64(&x19, x18, x9, x1);
 829    var x20: u64 = undefined;
 830    cmovznzU64(&x20, x18, x11, x3);
 831    var x21: u64 = undefined;
 832    cmovznzU64(&x21, x18, x13, x5);
 833    var x22: u64 = undefined;
 834    cmovznzU64(&x22, x18, x15, x7);
 835    out1[0] = x19;
 836    out1[1] = x20;
 837    out1[2] = x21;
 838    out1[3] = x22;
 839}
 840
 841/// The function sub subtracts two field elements in the Montgomery domain.
 842///
 843/// Preconditions:
 844///   0 ≤ eval arg1 < m
 845///   0 ≤ eval arg2 < m
 846/// Postconditions:
 847///   eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
 848///   0 ≤ eval out1 < m
 849///
 850pub fn sub(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
 851    @setRuntimeSafety(mode == .Debug);
 852
 853    var x1: u64 = undefined;
 854    var x2: u1 = undefined;
 855    subborrowxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
 856    var x3: u64 = undefined;
 857    var x4: u1 = undefined;
 858    subborrowxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
 859    var x5: u64 = undefined;
 860    var x6: u1 = undefined;
 861    subborrowxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
 862    var x7: u64 = undefined;
 863    var x8: u1 = undefined;
 864    subborrowxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
 865    var x9: u64 = undefined;
 866    cmovznzU64(&x9, x8, 0x0, 0xffffffffffffffff);
 867    var x10: u64 = undefined;
 868    var x11: u1 = undefined;
 869    addcarryxU64(&x10, &x11, 0x0, x1, (x9 & 0xbfd25e8cd0364141));
 870    var x12: u64 = undefined;
 871    var x13: u1 = undefined;
 872    addcarryxU64(&x12, &x13, x11, x3, (x9 & 0xbaaedce6af48a03b));
 873    var x14: u64 = undefined;
 874    var x15: u1 = undefined;
 875    addcarryxU64(&x14, &x15, x13, x5, (x9 & 0xfffffffffffffffe));
 876    var x16: u64 = undefined;
 877    var x17: u1 = undefined;
 878    addcarryxU64(&x16, &x17, x15, x7, x9);
 879    out1[0] = x10;
 880    out1[1] = x12;
 881    out1[2] = x14;
 882    out1[3] = x16;
 883}
 884
 885/// The function opp negates a field element in the Montgomery domain.
 886///
 887/// Preconditions:
 888///   0 ≤ eval arg1 < m
 889/// Postconditions:
 890///   eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
 891///   0 ≤ eval out1 < m
 892///
 893pub fn opp(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
 894    @setRuntimeSafety(mode == .Debug);
 895
 896    var x1: u64 = undefined;
 897    var x2: u1 = undefined;
 898    subborrowxU64(&x1, &x2, 0x0, 0x0, (arg1[0]));
 899    var x3: u64 = undefined;
 900    var x4: u1 = undefined;
 901    subborrowxU64(&x3, &x4, x2, 0x0, (arg1[1]));
 902    var x5: u64 = undefined;
 903    var x6: u1 = undefined;
 904    subborrowxU64(&x5, &x6, x4, 0x0, (arg1[2]));
 905    var x7: u64 = undefined;
 906    var x8: u1 = undefined;
 907    subborrowxU64(&x7, &x8, x6, 0x0, (arg1[3]));
 908    var x9: u64 = undefined;
 909    cmovznzU64(&x9, x8, 0x0, 0xffffffffffffffff);
 910    var x10: u64 = undefined;
 911    var x11: u1 = undefined;
 912    addcarryxU64(&x10, &x11, 0x0, x1, (x9 & 0xbfd25e8cd0364141));
 913    var x12: u64 = undefined;
 914    var x13: u1 = undefined;
 915    addcarryxU64(&x12, &x13, x11, x3, (x9 & 0xbaaedce6af48a03b));
 916    var x14: u64 = undefined;
 917    var x15: u1 = undefined;
 918    addcarryxU64(&x14, &x15, x13, x5, (x9 & 0xfffffffffffffffe));
 919    var x16: u64 = undefined;
 920    var x17: u1 = undefined;
 921    addcarryxU64(&x16, &x17, x15, x7, x9);
 922    out1[0] = x10;
 923    out1[1] = x12;
 924    out1[2] = x14;
 925    out1[3] = x16;
 926}
 927
 928/// The function fromMontgomery translates a field element out of the Montgomery domain.
 929///
 930/// Preconditions:
 931///   0 ≤ eval arg1 < m
 932/// Postconditions:
 933///   eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m
 934///   0 ≤ eval out1 < m
 935///
 936pub fn fromMontgomery(out1: *NonMontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
 937    @setRuntimeSafety(mode == .Debug);
 938
 939    const x1 = (arg1[0]);
 940    var x2: u64 = undefined;
 941    var x3: u64 = undefined;
 942    mulxU64(&x2, &x3, x1, 0x4b0dff665588b13f);
 943    var x4: u64 = undefined;
 944    var x5: u64 = undefined;
 945    mulxU64(&x4, &x5, x2, 0xffffffffffffffff);
 946    var x6: u64 = undefined;
 947    var x7: u64 = undefined;
 948    mulxU64(&x6, &x7, x2, 0xfffffffffffffffe);
 949    var x8: u64 = undefined;
 950    var x9: u64 = undefined;
 951    mulxU64(&x8, &x9, x2, 0xbaaedce6af48a03b);
 952    var x10: u64 = undefined;
 953    var x11: u64 = undefined;
 954    mulxU64(&x10, &x11, x2, 0xbfd25e8cd0364141);
 955    var x12: u64 = undefined;
 956    var x13: u1 = undefined;
 957    addcarryxU64(&x12, &x13, 0x0, x11, x8);
 958    var x14: u64 = undefined;
 959    var x15: u1 = undefined;
 960    addcarryxU64(&x14, &x15, x13, x9, x6);
 961    var x16: u64 = undefined;
 962    var x17: u1 = undefined;
 963    addcarryxU64(&x16, &x17, x15, x7, x4);
 964    var x18: u64 = undefined;
 965    var x19: u1 = undefined;
 966    addcarryxU64(&x18, &x19, 0x0, x1, x10);
 967    var x20: u64 = undefined;
 968    var x21: u1 = undefined;
 969    addcarryxU64(&x20, &x21, x19, 0x0, x12);
 970    var x22: u64 = undefined;
 971    var x23: u1 = undefined;
 972    addcarryxU64(&x22, &x23, x21, 0x0, x14);
 973    var x24: u64 = undefined;
 974    var x25: u1 = undefined;
 975    addcarryxU64(&x24, &x25, x23, 0x0, x16);
 976    var x26: u64 = undefined;
 977    var x27: u1 = undefined;
 978    addcarryxU64(&x26, &x27, x25, 0x0, (@as(u64, x17) + x5));
 979    var x28: u64 = undefined;
 980    var x29: u1 = undefined;
 981    addcarryxU64(&x28, &x29, 0x0, x20, (arg1[1]));
 982    var x30: u64 = undefined;
 983    var x31: u1 = undefined;
 984    addcarryxU64(&x30, &x31, x29, x22, 0x0);
 985    var x32: u64 = undefined;
 986    var x33: u1 = undefined;
 987    addcarryxU64(&x32, &x33, x31, x24, 0x0);
 988    var x34: u64 = undefined;
 989    var x35: u1 = undefined;
 990    addcarryxU64(&x34, &x35, x33, x26, 0x0);
 991    var x36: u64 = undefined;
 992    var x37: u64 = undefined;
 993    mulxU64(&x36, &x37, x28, 0x4b0dff665588b13f);
 994    var x38: u64 = undefined;
 995    var x39: u64 = undefined;
 996    mulxU64(&x38, &x39, x36, 0xffffffffffffffff);
 997    var x40: u64 = undefined;
 998    var x41: u64 = undefined;
 999    mulxU64(&x40, &x41, x36, 0xfffffffffffffffe);
1000    var x42: u64 = undefined;
1001    var x43: u64 = undefined;
1002    mulxU64(&x42, &x43, x36, 0xbaaedce6af48a03b);
1003    var x44: u64 = undefined;
1004    var x45: u64 = undefined;
1005    mulxU64(&x44, &x45, x36, 0xbfd25e8cd0364141);
1006    var x46: u64 = undefined;
1007    var x47: u1 = undefined;
1008    addcarryxU64(&x46, &x47, 0x0, x45, x42);
1009    var x48: u64 = undefined;
1010    var x49: u1 = undefined;
1011    addcarryxU64(&x48, &x49, x47, x43, x40);
1012    var x50: u64 = undefined;
1013    var x51: u1 = undefined;
1014    addcarryxU64(&x50, &x51, x49, x41, x38);
1015    var x52: u64 = undefined;
1016    var x53: u1 = undefined;
1017    addcarryxU64(&x52, &x53, 0x0, x28, x44);
1018    var x54: u64 = undefined;
1019    var x55: u1 = undefined;
1020    addcarryxU64(&x54, &x55, x53, x30, x46);
1021    var x56: u64 = undefined;
1022    var x57: u1 = undefined;
1023    addcarryxU64(&x56, &x57, x55, x32, x48);
1024    var x58: u64 = undefined;
1025    var x59: u1 = undefined;
1026    addcarryxU64(&x58, &x59, x57, x34, x50);
1027    var x60: u64 = undefined;
1028    var x61: u1 = undefined;
1029    addcarryxU64(&x60, &x61, x59, (@as(u64, x35) + @as(u64, x27)), (@as(u64, x51) + x39));
1030    var x62: u64 = undefined;
1031    var x63: u1 = undefined;
1032    addcarryxU64(&x62, &x63, 0x0, x54, (arg1[2]));
1033    var x64: u64 = undefined;
1034    var x65: u1 = undefined;
1035    addcarryxU64(&x64, &x65, x63, x56, 0x0);
1036    var x66: u64 = undefined;
1037    var x67: u1 = undefined;
1038    addcarryxU64(&x66, &x67, x65, x58, 0x0);
1039    var x68: u64 = undefined;
1040    var x69: u1 = undefined;
1041    addcarryxU64(&x68, &x69, x67, x60, 0x0);
1042    var x70: u64 = undefined;
1043    var x71: u64 = undefined;
1044    mulxU64(&x70, &x71, x62, 0x4b0dff665588b13f);
1045    var x72: u64 = undefined;
1046    var x73: u64 = undefined;
1047    mulxU64(&x72, &x73, x70, 0xffffffffffffffff);
1048    var x74: u64 = undefined;
1049    var x75: u64 = undefined;
1050    mulxU64(&x74, &x75, x70, 0xfffffffffffffffe);
1051    var x76: u64 = undefined;
1052    var x77: u64 = undefined;
1053    mulxU64(&x76, &x77, x70, 0xbaaedce6af48a03b);
1054    var x78: u64 = undefined;
1055    var x79: u64 = undefined;
1056    mulxU64(&x78, &x79, x70, 0xbfd25e8cd0364141);
1057    var x80: u64 = undefined;
1058    var x81: u1 = undefined;
1059    addcarryxU64(&x80, &x81, 0x0, x79, x76);
1060    var x82: u64 = undefined;
1061    var x83: u1 = undefined;
1062    addcarryxU64(&x82, &x83, x81, x77, x74);
1063    var x84: u64 = undefined;
1064    var x85: u1 = undefined;
1065    addcarryxU64(&x84, &x85, x83, x75, x72);
1066    var x86: u64 = undefined;
1067    var x87: u1 = undefined;
1068    addcarryxU64(&x86, &x87, 0x0, x62, x78);
1069    var x88: u64 = undefined;
1070    var x89: u1 = undefined;
1071    addcarryxU64(&x88, &x89, x87, x64, x80);
1072    var x90: u64 = undefined;
1073    var x91: u1 = undefined;
1074    addcarryxU64(&x90, &x91, x89, x66, x82);
1075    var x92: u64 = undefined;
1076    var x93: u1 = undefined;
1077    addcarryxU64(&x92, &x93, x91, x68, x84);
1078    var x94: u64 = undefined;
1079    var x95: u1 = undefined;
1080    addcarryxU64(&x94, &x95, x93, (@as(u64, x69) + @as(u64, x61)), (@as(u64, x85) + x73));
1081    var x96: u64 = undefined;
1082    var x97: u1 = undefined;
1083    addcarryxU64(&x96, &x97, 0x0, x88, (arg1[3]));
1084    var x98: u64 = undefined;
1085    var x99: u1 = undefined;
1086    addcarryxU64(&x98, &x99, x97, x90, 0x0);
1087    var x100: u64 = undefined;
1088    var x101: u1 = undefined;
1089    addcarryxU64(&x100, &x101, x99, x92, 0x0);
1090    var x102: u64 = undefined;
1091    var x103: u1 = undefined;
1092    addcarryxU64(&x102, &x103, x101, x94, 0x0);
1093    var x104: u64 = undefined;
1094    var x105: u64 = undefined;
1095    mulxU64(&x104, &x105, x96, 0x4b0dff665588b13f);
1096    var x106: u64 = undefined;
1097    var x107: u64 = undefined;
1098    mulxU64(&x106, &x107, x104, 0xffffffffffffffff);
1099    var x108: u64 = undefined;
1100    var x109: u64 = undefined;
1101    mulxU64(&x108, &x109, x104, 0xfffffffffffffffe);
1102    var x110: u64 = undefined;
1103    var x111: u64 = undefined;
1104    mulxU64(&x110, &x111, x104, 0xbaaedce6af48a03b);
1105    var x112: u64 = undefined;
1106    var x113: u64 = undefined;
1107    mulxU64(&x112, &x113, x104, 0xbfd25e8cd0364141);
1108    var x114: u64 = undefined;
1109    var x115: u1 = undefined;
1110    addcarryxU64(&x114, &x115, 0x0, x113, x110);
1111    var x116: u64 = undefined;
1112    var x117: u1 = undefined;
1113    addcarryxU64(&x116, &x117, x115, x111, x108);
1114    var x118: u64 = undefined;
1115    var x119: u1 = undefined;
1116    addcarryxU64(&x118, &x119, x117, x109, x106);
1117    var x120: u64 = undefined;
1118    var x121: u1 = undefined;
1119    addcarryxU64(&x120, &x121, 0x0, x96, x112);
1120    var x122: u64 = undefined;
1121    var x123: u1 = undefined;
1122    addcarryxU64(&x122, &x123, x121, x98, x114);
1123    var x124: u64 = undefined;
1124    var x125: u1 = undefined;
1125    addcarryxU64(&x124, &x125, x123, x100, x116);
1126    var x126: u64 = undefined;
1127    var x127: u1 = undefined;
1128    addcarryxU64(&x126, &x127, x125, x102, x118);
1129    var x128: u64 = undefined;
1130    var x129: u1 = undefined;
1131    addcarryxU64(&x128, &x129, x127, (@as(u64, x103) + @as(u64, x95)), (@as(u64, x119) + x107));
1132    var x130: u64 = undefined;
1133    var x131: u1 = undefined;
1134    subborrowxU64(&x130, &x131, 0x0, x122, 0xbfd25e8cd0364141);
1135    var x132: u64 = undefined;
1136    var x133: u1 = undefined;
1137    subborrowxU64(&x132, &x133, x131, x124, 0xbaaedce6af48a03b);
1138    var x134: u64 = undefined;
1139    var x135: u1 = undefined;
1140    subborrowxU64(&x134, &x135, x133, x126, 0xfffffffffffffffe);
1141    var x136: u64 = undefined;
1142    var x137: u1 = undefined;
1143    subborrowxU64(&x136, &x137, x135, x128, 0xffffffffffffffff);
1144    var x138: u64 = undefined;
1145    var x139: u1 = undefined;
1146    subborrowxU64(&x138, &x139, x137, @as(u64, x129), 0x0);
1147    var x140: u64 = undefined;
1148    cmovznzU64(&x140, x139, x130, x122);
1149    var x141: u64 = undefined;
1150    cmovznzU64(&x141, x139, x132, x124);
1151    var x142: u64 = undefined;
1152    cmovznzU64(&x142, x139, x134, x126);
1153    var x143: u64 = undefined;
1154    cmovznzU64(&x143, x139, x136, x128);
1155    out1[0] = x140;
1156    out1[1] = x141;
1157    out1[2] = x142;
1158    out1[3] = x143;
1159}
1160
1161/// The function toMontgomery translates a field element into the Montgomery domain.
1162///
1163/// Preconditions:
1164///   0 ≤ eval arg1 < m
1165/// Postconditions:
1166///   eval (from_montgomery out1) mod m = eval arg1 mod m
1167///   0 ≤ eval out1 < m
1168///
1169pub fn toMontgomery(out1: *MontgomeryDomainFieldElement, arg1: NonMontgomeryDomainFieldElement) void {
1170    @setRuntimeSafety(mode == .Debug);
1171
1172    const x1 = (arg1[1]);
1173    const x2 = (arg1[2]);
1174    const x3 = (arg1[3]);
1175    const x4 = (arg1[0]);
1176    var x5: u64 = undefined;
1177    var x6: u64 = undefined;
1178    mulxU64(&x5, &x6, x4, 0x9d671cd581c69bc5);
1179    var x7: u64 = undefined;
1180    var x8: u64 = undefined;
1181    mulxU64(&x7, &x8, x4, 0xe697f5e45bcd07c6);
1182    var x9: u64 = undefined;
1183    var x10: u64 = undefined;
1184    mulxU64(&x9, &x10, x4, 0x741496c20e7cf878);
1185    var x11: u64 = undefined;
1186    var x12: u64 = undefined;
1187    mulxU64(&x11, &x12, x4, 0x896cf21467d7d140);
1188    var x13: u64 = undefined;
1189    var x14: u1 = undefined;
1190    addcarryxU64(&x13, &x14, 0x0, x12, x9);
1191    var x15: u64 = undefined;
1192    var x16: u1 = undefined;
1193    addcarryxU64(&x15, &x16, x14, x10, x7);
1194    var x17: u64 = undefined;
1195    var x18: u1 = undefined;
1196    addcarryxU64(&x17, &x18, x16, x8, x5);
1197    var x19: u64 = undefined;
1198    var x20: u64 = undefined;
1199    mulxU64(&x19, &x20, x11, 0x4b0dff665588b13f);
1200    var x21: u64 = undefined;
1201    var x22: u64 = undefined;
1202    mulxU64(&x21, &x22, x19, 0xffffffffffffffff);
1203    var x23: u64 = undefined;
1204    var x24: u64 = undefined;
1205    mulxU64(&x23, &x24, x19, 0xfffffffffffffffe);
1206    var x25: u64 = undefined;
1207    var x26: u64 = undefined;
1208    mulxU64(&x25, &x26, x19, 0xbaaedce6af48a03b);
1209    var x27: u64 = undefined;
1210    var x28: u64 = undefined;
1211    mulxU64(&x27, &x28, x19, 0xbfd25e8cd0364141);
1212    var x29: u64 = undefined;
1213    var x30: u1 = undefined;
1214    addcarryxU64(&x29, &x30, 0x0, x28, x25);
1215    var x31: u64 = undefined;
1216    var x32: u1 = undefined;
1217    addcarryxU64(&x31, &x32, x30, x26, x23);
1218    var x33: u64 = undefined;
1219    var x34: u1 = undefined;
1220    addcarryxU64(&x33, &x34, x32, x24, x21);
1221    var x35: u64 = undefined;
1222    var x36: u1 = undefined;
1223    addcarryxU64(&x35, &x36, 0x0, x11, x27);
1224    var x37: u64 = undefined;
1225    var x38: u1 = undefined;
1226    addcarryxU64(&x37, &x38, x36, x13, x29);
1227    var x39: u64 = undefined;
1228    var x40: u1 = undefined;
1229    addcarryxU64(&x39, &x40, x38, x15, x31);
1230    var x41: u64 = undefined;
1231    var x42: u1 = undefined;
1232    addcarryxU64(&x41, &x42, x40, x17, x33);
1233    var x43: u64 = undefined;
1234    var x44: u1 = undefined;
1235    addcarryxU64(&x43, &x44, x42, (@as(u64, x18) + x6), (@as(u64, x34) + x22));
1236    var x45: u64 = undefined;
1237    var x46: u64 = undefined;
1238    mulxU64(&x45, &x46, x1, 0x9d671cd581c69bc5);
1239    var x47: u64 = undefined;
1240    var x48: u64 = undefined;
1241    mulxU64(&x47, &x48, x1, 0xe697f5e45bcd07c6);
1242    var x49: u64 = undefined;
1243    var x50: u64 = undefined;
1244    mulxU64(&x49, &x50, x1, 0x741496c20e7cf878);
1245    var x51: u64 = undefined;
1246    var x52: u64 = undefined;
1247    mulxU64(&x51, &x52, x1, 0x896cf21467d7d140);
1248    var x53: u64 = undefined;
1249    var x54: u1 = undefined;
1250    addcarryxU64(&x53, &x54, 0x0, x52, x49);
1251    var x55: u64 = undefined;
1252    var x56: u1 = undefined;
1253    addcarryxU64(&x55, &x56, x54, x50, x47);
1254    var x57: u64 = undefined;
1255    var x58: u1 = undefined;
1256    addcarryxU64(&x57, &x58, x56, x48, x45);
1257    var x59: u64 = undefined;
1258    var x60: u1 = undefined;
1259    addcarryxU64(&x59, &x60, 0x0, x37, x51);
1260    var x61: u64 = undefined;
1261    var x62: u1 = undefined;
1262    addcarryxU64(&x61, &x62, x60, x39, x53);
1263    var x63: u64 = undefined;
1264    var x64: u1 = undefined;
1265    addcarryxU64(&x63, &x64, x62, x41, x55);
1266    var x65: u64 = undefined;
1267    var x66: u1 = undefined;
1268    addcarryxU64(&x65, &x66, x64, x43, x57);
1269    var x67: u64 = undefined;
1270    var x68: u64 = undefined;
1271    mulxU64(&x67, &x68, x59, 0x4b0dff665588b13f);
1272    var x69: u64 = undefined;
1273    var x70: u64 = undefined;
1274    mulxU64(&x69, &x70, x67, 0xffffffffffffffff);
1275    var x71: u64 = undefined;
1276    var x72: u64 = undefined;
1277    mulxU64(&x71, &x72, x67, 0xfffffffffffffffe);
1278    var x73: u64 = undefined;
1279    var x74: u64 = undefined;
1280    mulxU64(&x73, &x74, x67, 0xbaaedce6af48a03b);
1281    var x75: u64 = undefined;
1282    var x76: u64 = undefined;
1283    mulxU64(&x75, &x76, x67, 0xbfd25e8cd0364141);
1284    var x77: u64 = undefined;
1285    var x78: u1 = undefined;
1286    addcarryxU64(&x77, &x78, 0x0, x76, x73);
1287    var x79: u64 = undefined;
1288    var x80: u1 = undefined;
1289    addcarryxU64(&x79, &x80, x78, x74, x71);
1290    var x81: u64 = undefined;
1291    var x82: u1 = undefined;
1292    addcarryxU64(&x81, &x82, x80, x72, x69);
1293    var x83: u64 = undefined;
1294    var x84: u1 = undefined;
1295    addcarryxU64(&x83, &x84, 0x0, x59, x75);
1296    var x85: u64 = undefined;
1297    var x86: u1 = undefined;
1298    addcarryxU64(&x85, &x86, x84, x61, x77);
1299    var x87: u64 = undefined;
1300    var x88: u1 = undefined;
1301    addcarryxU64(&x87, &x88, x86, x63, x79);
1302    var x89: u64 = undefined;
1303    var x90: u1 = undefined;
1304    addcarryxU64(&x89, &x90, x88, x65, x81);
1305    var x91: u64 = undefined;
1306    var x92: u1 = undefined;
1307    addcarryxU64(&x91, &x92, x90, ((@as(u64, x66) + @as(u64, x44)) + (@as(u64, x58) + x46)), (@as(u64, x82) + x70));
1308    var x93: u64 = undefined;
1309    var x94: u64 = undefined;
1310    mulxU64(&x93, &x94, x2, 0x9d671cd581c69bc5);
1311    var x95: u64 = undefined;
1312    var x96: u64 = undefined;
1313    mulxU64(&x95, &x96, x2, 0xe697f5e45bcd07c6);
1314    var x97: u64 = undefined;
1315    var x98: u64 = undefined;
1316    mulxU64(&x97, &x98, x2, 0x741496c20e7cf878);
1317    var x99: u64 = undefined;
1318    var x100: u64 = undefined;
1319    mulxU64(&x99, &x100, x2, 0x896cf21467d7d140);
1320    var x101: u64 = undefined;
1321    var x102: u1 = undefined;
1322    addcarryxU64(&x101, &x102, 0x0, x100, x97);
1323    var x103: u64 = undefined;
1324    var x104: u1 = undefined;
1325    addcarryxU64(&x103, &x104, x102, x98, x95);
1326    var x105: u64 = undefined;
1327    var x106: u1 = undefined;
1328    addcarryxU64(&x105, &x106, x104, x96, x93);
1329    var x107: u64 = undefined;
1330    var x108: u1 = undefined;
1331    addcarryxU64(&x107, &x108, 0x0, x85, x99);
1332    var x109: u64 = undefined;
1333    var x110: u1 = undefined;
1334    addcarryxU64(&x109, &x110, x108, x87, x101);
1335    var x111: u64 = undefined;
1336    var x112: u1 = undefined;
1337    addcarryxU64(&x111, &x112, x110, x89, x103);
1338    var x113: u64 = undefined;
1339    var x114: u1 = undefined;
1340    addcarryxU64(&x113, &x114, x112, x91, x105);
1341    var x115: u64 = undefined;
1342    var x116: u64 = undefined;
1343    mulxU64(&x115, &x116, x107, 0x4b0dff665588b13f);
1344    var x117: u64 = undefined;
1345    var x118: u64 = undefined;
1346    mulxU64(&x117, &x118, x115, 0xffffffffffffffff);
1347    var x119: u64 = undefined;
1348    var x120: u64 = undefined;
1349    mulxU64(&x119, &x120, x115, 0xfffffffffffffffe);
1350    var x121: u64 = undefined;
1351    var x122: u64 = undefined;
1352    mulxU64(&x121, &x122, x115, 0xbaaedce6af48a03b);
1353    var x123: u64 = undefined;
1354    var x124: u64 = undefined;
1355    mulxU64(&x123, &x124, x115, 0xbfd25e8cd0364141);
1356    var x125: u64 = undefined;
1357    var x126: u1 = undefined;
1358    addcarryxU64(&x125, &x126, 0x0, x124, x121);
1359    var x127: u64 = undefined;
1360    var x128: u1 = undefined;
1361    addcarryxU64(&x127, &x128, x126, x122, x119);
1362    var x129: u64 = undefined;
1363    var x130: u1 = undefined;
1364    addcarryxU64(&x129, &x130, x128, x120, x117);
1365    var x131: u64 = undefined;
1366    var x132: u1 = undefined;
1367    addcarryxU64(&x131, &x132, 0x0, x107, x123);
1368    var x133: u64 = undefined;
1369    var x134: u1 = undefined;
1370    addcarryxU64(&x133, &x134, x132, x109, x125);
1371    var x135: u64 = undefined;
1372    var x136: u1 = undefined;
1373    addcarryxU64(&x135, &x136, x134, x111, x127);
1374    var x137: u64 = undefined;
1375    var x138: u1 = undefined;
1376    addcarryxU64(&x137, &x138, x136, x113, x129);
1377    var x139: u64 = undefined;
1378    var x140: u1 = undefined;
1379    addcarryxU64(&x139, &x140, x138, ((@as(u64, x114) + @as(u64, x92)) + (@as(u64, x106) + x94)), (@as(u64, x130) + x118));
1380    var x141: u64 = undefined;
1381    var x142: u64 = undefined;
1382    mulxU64(&x141, &x142, x3, 0x9d671cd581c69bc5);
1383    var x143: u64 = undefined;
1384    var x144: u64 = undefined;
1385    mulxU64(&x143, &x144, x3, 0xe697f5e45bcd07c6);
1386    var x145: u64 = undefined;
1387    var x146: u64 = undefined;
1388    mulxU64(&x145, &x146, x3, 0x741496c20e7cf878);
1389    var x147: u64 = undefined;
1390    var x148: u64 = undefined;
1391    mulxU64(&x147, &x148, x3, 0x896cf21467d7d140);
1392    var x149: u64 = undefined;
1393    var x150: u1 = undefined;
1394    addcarryxU64(&x149, &x150, 0x0, x148, x145);
1395    var x151: u64 = undefined;
1396    var x152: u1 = undefined;
1397    addcarryxU64(&x151, &x152, x150, x146, x143);
1398    var x153: u64 = undefined;
1399    var x154: u1 = undefined;
1400    addcarryxU64(&x153, &x154, x152, x144, x141);
1401    var x155: u64 = undefined;
1402    var x156: u1 = undefined;
1403    addcarryxU64(&x155, &x156, 0x0, x133, x147);
1404    var x157: u64 = undefined;
1405    var x158: u1 = undefined;
1406    addcarryxU64(&x157, &x158, x156, x135, x149);
1407    var x159: u64 = undefined;
1408    var x160: u1 = undefined;
1409    addcarryxU64(&x159, &x160, x158, x137, x151);
1410    var x161: u64 = undefined;
1411    var x162: u1 = undefined;
1412    addcarryxU64(&x161, &x162, x160, x139, x153);
1413    var x163: u64 = undefined;
1414    var x164: u64 = undefined;
1415    mulxU64(&x163, &x164, x155, 0x4b0dff665588b13f);
1416    var x165: u64 = undefined;
1417    var x166: u64 = undefined;
1418    mulxU64(&x165, &x166, x163, 0xffffffffffffffff);
1419    var x167: u64 = undefined;
1420    var x168: u64 = undefined;
1421    mulxU64(&x167, &x168, x163, 0xfffffffffffffffe);
1422    var x169: u64 = undefined;
1423    var x170: u64 = undefined;
1424    mulxU64(&x169, &x170, x163, 0xbaaedce6af48a03b);
1425    var x171: u64 = undefined;
1426    var x172: u64 = undefined;
1427    mulxU64(&x171, &x172, x163, 0xbfd25e8cd0364141);
1428    var x173: u64 = undefined;
1429    var x174: u1 = undefined;
1430    addcarryxU64(&x173, &x174, 0x0, x172, x169);
1431    var x175: u64 = undefined;
1432    var x176: u1 = undefined;
1433    addcarryxU64(&x175, &x176, x174, x170, x167);
1434    var x177: u64 = undefined;
1435    var x178: u1 = undefined;
1436    addcarryxU64(&x177, &x178, x176, x168, x165);
1437    var x179: u64 = undefined;
1438    var x180: u1 = undefined;
1439    addcarryxU64(&x179, &x180, 0x0, x155, x171);
1440    var x181: u64 = undefined;
1441    var x182: u1 = undefined;
1442    addcarryxU64(&x181, &x182, x180, x157, x173);
1443    var x183: u64 = undefined;
1444    var x184: u1 = undefined;
1445    addcarryxU64(&x183, &x184, x182, x159, x175);
1446    var x185: u64 = undefined;
1447    var x186: u1 = undefined;
1448    addcarryxU64(&x185, &x186, x184, x161, x177);
1449    var x187: u64 = undefined;
1450    var x188: u1 = undefined;
1451    addcarryxU64(&x187, &x188, x186, ((@as(u64, x162) + @as(u64, x140)) + (@as(u64, x154) + x142)), (@as(u64, x178) + x166));
1452    var x189: u64 = undefined;
1453    var x190: u1 = undefined;
1454    subborrowxU64(&x189, &x190, 0x0, x181, 0xbfd25e8cd0364141);
1455    var x191: u64 = undefined;
1456    var x192: u1 = undefined;
1457    subborrowxU64(&x191, &x192, x190, x183, 0xbaaedce6af48a03b);
1458    var x193: u64 = undefined;
1459    var x194: u1 = undefined;
1460    subborrowxU64(&x193, &x194, x192, x185, 0xfffffffffffffffe);
1461    var x195: u64 = undefined;
1462    var x196: u1 = undefined;
1463    subborrowxU64(&x195, &x196, x194, x187, 0xffffffffffffffff);
1464    var x197: u64 = undefined;
1465    var x198: u1 = undefined;
1466    subborrowxU64(&x197, &x198, x196, @as(u64, x188), 0x0);
1467    var x199: u64 = undefined;
1468    cmovznzU64(&x199, x198, x189, x181);
1469    var x200: u64 = undefined;
1470    cmovznzU64(&x200, x198, x191, x183);
1471    var x201: u64 = undefined;
1472    cmovznzU64(&x201, x198, x193, x185);
1473    var x202: u64 = undefined;
1474    cmovznzU64(&x202, x198, x195, x187);
1475    out1[0] = x199;
1476    out1[1] = x200;
1477    out1[2] = x201;
1478    out1[3] = x202;
1479}
1480
1481/// The function nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
1482///
1483/// Preconditions:
1484///   0 ≤ eval arg1 < m
1485/// Postconditions:
1486///   out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
1487///
1488/// Input Bounds:
1489///   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1490/// Output Bounds:
1491///   out1: [0x0 ~> 0xffffffffffffffff]
1492pub fn nonzero(out1: *u64, arg1: [4]u64) void {
1493    @setRuntimeSafety(mode == .Debug);
1494
1495    const x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | (arg1[3]))));
1496    out1.* = x1;
1497}
1498
1499/// The function selectznz is a multi-limb conditional select.
1500///
1501/// Postconditions:
1502///   out1 = (if arg1 = 0 then arg2 else arg3)
1503///
1504/// Input Bounds:
1505///   arg1: [0x0 ~> 0x1]
1506///   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1507///   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1508/// Output Bounds:
1509///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1510pub fn selectznz(out1: *[4]u64, arg1: u1, arg2: [4]u64, arg3: [4]u64) void {
1511    @setRuntimeSafety(mode == .Debug);
1512
1513    var x1: u64 = undefined;
1514    cmovznzU64(&x1, arg1, (arg2[0]), (arg3[0]));
1515    var x2: u64 = undefined;
1516    cmovznzU64(&x2, arg1, (arg2[1]), (arg3[1]));
1517    var x3: u64 = undefined;
1518    cmovznzU64(&x3, arg1, (arg2[2]), (arg3[2]));
1519    var x4: u64 = undefined;
1520    cmovznzU64(&x4, arg1, (arg2[3]), (arg3[3]));
1521    out1[0] = x1;
1522    out1[1] = x2;
1523    out1[2] = x3;
1524    out1[3] = x4;
1525}
1526
1527/// The function toBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
1528///
1529/// Preconditions:
1530///   0 ≤ eval arg1 < m
1531/// Postconditions:
1532///   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31]
1533///
1534/// Input Bounds:
1535///   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1536/// Output Bounds:
1537///   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]]
1538pub fn toBytes(out1: *[32]u8, arg1: [4]u64) void {
1539    @setRuntimeSafety(mode == .Debug);
1540
1541    const x1 = (arg1[3]);
1542    const x2 = (arg1[2]);
1543    const x3 = (arg1[1]);
1544    const x4 = (arg1[0]);
1545    const x5 = @as(u8, @truncate((x4 & 0xff)));
1546    const x6 = (x4 >> 8);
1547    const x7 = @as(u8, @truncate((x6 & 0xff)));
1548    const x8 = (x6 >> 8);
1549    const x9 = @as(u8, @truncate((x8 & 0xff)));
1550    const x10 = (x8 >> 8);
1551    const x11 = @as(u8, @truncate((x10 & 0xff)));
1552    const x12 = (x10 >> 8);
1553    const x13 = @as(u8, @truncate((x12 & 0xff)));
1554    const x14 = (x12 >> 8);
1555    const x15 = @as(u8, @truncate((x14 & 0xff)));
1556    const x16 = (x14 >> 8);
1557    const x17 = @as(u8, @truncate((x16 & 0xff)));
1558    const x18 = @as(u8, @truncate((x16 >> 8)));
1559    const x19 = @as(u8, @truncate((x3 & 0xff)));
1560    const x20 = (x3 >> 8);
1561    const x21 = @as(u8, @truncate((x20 & 0xff)));
1562    const x22 = (x20 >> 8);
1563    const x23 = @as(u8, @truncate((x22 & 0xff)));
1564    const x24 = (x22 >> 8);
1565    const x25 = @as(u8, @truncate((x24 & 0xff)));
1566    const x26 = (x24 >> 8);
1567    const x27 = @as(u8, @truncate((x26 & 0xff)));
1568    const x28 = (x26 >> 8);
1569    const x29 = @as(u8, @truncate((x28 & 0xff)));
1570    const x30 = (x28 >> 8);
1571    const x31 = @as(u8, @truncate((x30 & 0xff)));
1572    const x32 = @as(u8, @truncate((x30 >> 8)));
1573    const x33 = @as(u8, @truncate((x2 & 0xff)));
1574    const x34 = (x2 >> 8);
1575    const x35 = @as(u8, @truncate((x34 & 0xff)));
1576    const x36 = (x34 >> 8);
1577    const x37 = @as(u8, @truncate((x36 & 0xff)));
1578    const x38 = (x36 >> 8);
1579    const x39 = @as(u8, @truncate((x38 & 0xff)));
1580    const x40 = (x38 >> 8);
1581    const x41 = @as(u8, @truncate((x40 & 0xff)));
1582    const x42 = (x40 >> 8);
1583    const x43 = @as(u8, @truncate((x42 & 0xff)));
1584    const x44 = (x42 >> 8);
1585    const x45 = @as(u8, @truncate((x44 & 0xff)));
1586    const x46 = @as(u8, @truncate((x44 >> 8)));
1587    const x47 = @as(u8, @truncate((x1 & 0xff)));
1588    const x48 = (x1 >> 8);
1589    const x49 = @as(u8, @truncate((x48 & 0xff)));
1590    const x50 = (x48 >> 8);
1591    const x51 = @as(u8, @truncate((x50 & 0xff)));
1592    const x52 = (x50 >> 8);
1593    const x53 = @as(u8, @truncate((x52 & 0xff)));
1594    const x54 = (x52 >> 8);
1595    const x55 = @as(u8, @truncate((x54 & 0xff)));
1596    const x56 = (x54 >> 8);
1597    const x57 = @as(u8, @truncate((x56 & 0xff)));
1598    const x58 = (x56 >> 8);
1599    const x59 = @as(u8, @truncate((x58 & 0xff)));
1600    const x60 = @as(u8, @truncate((x58 >> 8)));
1601    out1[0] = x5;
1602    out1[1] = x7;
1603    out1[2] = x9;
1604    out1[3] = x11;
1605    out1[4] = x13;
1606    out1[5] = x15;
1607    out1[6] = x17;
1608    out1[7] = x18;
1609    out1[8] = x19;
1610    out1[9] = x21;
1611    out1[10] = x23;
1612    out1[11] = x25;
1613    out1[12] = x27;
1614    out1[13] = x29;
1615    out1[14] = x31;
1616    out1[15] = x32;
1617    out1[16] = x33;
1618    out1[17] = x35;
1619    out1[18] = x37;
1620    out1[19] = x39;
1621    out1[20] = x41;
1622    out1[21] = x43;
1623    out1[22] = x45;
1624    out1[23] = x46;
1625    out1[24] = x47;
1626    out1[25] = x49;
1627    out1[26] = x51;
1628    out1[27] = x53;
1629    out1[28] = x55;
1630    out1[29] = x57;
1631    out1[30] = x59;
1632    out1[31] = x60;
1633}
1634
1635/// The function fromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
1636///
1637/// Preconditions:
1638///   0 ≤ bytes_eval arg1 < m
1639/// Postconditions:
1640///   eval out1 mod m = bytes_eval arg1 mod m
1641///   0 ≤ eval out1 < m
1642///
1643/// Input Bounds:
1644///   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]]
1645/// Output Bounds:
1646///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1647pub fn fromBytes(out1: *[4]u64, arg1: [32]u8) void {
1648    @setRuntimeSafety(mode == .Debug);
1649
1650    const x1 = (@as(u64, (arg1[31])) << 56);
1651    const x2 = (@as(u64, (arg1[30])) << 48);
1652    const x3 = (@as(u64, (arg1[29])) << 40);
1653    const x4 = (@as(u64, (arg1[28])) << 32);
1654    const x5 = (@as(u64, (arg1[27])) << 24);
1655    const x6 = (@as(u64, (arg1[26])) << 16);
1656    const x7 = (@as(u64, (arg1[25])) << 8);
1657    const x8 = (arg1[24]);
1658    const x9 = (@as(u64, (arg1[23])) << 56);
1659    const x10 = (@as(u64, (arg1[22])) << 48);
1660    const x11 = (@as(u64, (arg1[21])) << 40);
1661    const x12 = (@as(u64, (arg1[20])) << 32);
1662    const x13 = (@as(u64, (arg1[19])) << 24);
1663    const x14 = (@as(u64, (arg1[18])) << 16);
1664    const x15 = (@as(u64, (arg1[17])) << 8);
1665    const x16 = (arg1[16]);
1666    const x17 = (@as(u64, (arg1[15])) << 56);
1667    const x18 = (@as(u64, (arg1[14])) << 48);
1668    const x19 = (@as(u64, (arg1[13])) << 40);
1669    const x20 = (@as(u64, (arg1[12])) << 32);
1670    const x21 = (@as(u64, (arg1[11])) << 24);
1671    const x22 = (@as(u64, (arg1[10])) << 16);
1672    const x23 = (@as(u64, (arg1[9])) << 8);
1673    const x24 = (arg1[8]);
1674    const x25 = (@as(u64, (arg1[7])) << 56);
1675    const x26 = (@as(u64, (arg1[6])) << 48);
1676    const x27 = (@as(u64, (arg1[5])) << 40);
1677    const x28 = (@as(u64, (arg1[4])) << 32);
1678    const x29 = (@as(u64, (arg1[3])) << 24);
1679    const x30 = (@as(u64, (arg1[2])) << 16);
1680    const x31 = (@as(u64, (arg1[1])) << 8);
1681    const x32 = (arg1[0]);
1682    const x33 = (x31 + @as(u64, x32));
1683    const x34 = (x30 + x33);
1684    const x35 = (x29 + x34);
1685    const x36 = (x28 + x35);
1686    const x37 = (x27 + x36);
1687    const x38 = (x26 + x37);
1688    const x39 = (x25 + x38);
1689    const x40 = (x23 + @as(u64, x24));
1690    const x41 = (x22 + x40);
1691    const x42 = (x21 + x41);
1692    const x43 = (x20 + x42);
1693    const x44 = (x19 + x43);
1694    const x45 = (x18 + x44);
1695    const x46 = (x17 + x45);
1696    const x47 = (x15 + @as(u64, x16));
1697    const x48 = (x14 + x47);
1698    const x49 = (x13 + x48);
1699    const x50 = (x12 + x49);
1700    const x51 = (x11 + x50);
1701    const x52 = (x10 + x51);
1702    const x53 = (x9 + x52);
1703    const x54 = (x7 + @as(u64, x8));
1704    const x55 = (x6 + x54);
1705    const x56 = (x5 + x55);
1706    const x57 = (x4 + x56);
1707    const x58 = (x3 + x57);
1708    const x59 = (x2 + x58);
1709    const x60 = (x1 + x59);
1710    out1[0] = x39;
1711    out1[1] = x46;
1712    out1[2] = x53;
1713    out1[3] = x60;
1714}
1715
1716/// The function setOne returns the field element one in the Montgomery domain.
1717///
1718/// Postconditions:
1719///   eval (from_montgomery out1) mod m = 1 mod m
1720///   0 ≤ eval out1 < m
1721///
1722pub fn setOne(out1: *MontgomeryDomainFieldElement) void {
1723    @setRuntimeSafety(mode == .Debug);
1724
1725    out1[0] = 0x402da1732fc9bebf;
1726    out1[1] = 0x4551231950b75fc4;
1727    out1[2] = 0x1;
1728    out1[3] = 0x0;
1729}
1730
1731/// The function msat returns the saturated representation of the prime modulus.
1732///
1733/// Postconditions:
1734///   twos_complement_eval out1 = m
1735///   0 ≤ eval out1 < m
1736///
1737/// Output Bounds:
1738///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1739pub fn msat(out1: *[5]u64) void {
1740    @setRuntimeSafety(mode == .Debug);
1741
1742    out1[0] = 0xbfd25e8cd0364141;
1743    out1[1] = 0xbaaedce6af48a03b;
1744    out1[2] = 0xfffffffffffffffe;
1745    out1[3] = 0xffffffffffffffff;
1746    out1[4] = 0x0;
1747}
1748
1749/// The function divstep computes a divstep.
1750///
1751/// Preconditions:
1752///   0 ≤ eval arg4 < m
1753///   0 ≤ eval arg5 < m
1754/// Postconditions:
1755///   out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
1756///   twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
1757///   twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)
1758///   eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)
1759///   eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)
1760///   0 ≤ eval out5 < m
1761///   0 ≤ eval out5 < m
1762///   0 ≤ eval out2 < m
1763///   0 ≤ eval out3 < m
1764///
1765/// Input Bounds:
1766///   arg1: [0x0 ~> 0xffffffffffffffff]
1767///   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1768///   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1769///   arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1770///   arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1771/// Output Bounds:
1772///   out1: [0x0 ~> 0xffffffffffffffff]
1773///   out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1774///   out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1775///   out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1776///   out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
1777pub fn divstep(out1: *u64, out2: *[5]u64, out3: *[5]u64, out4: *[4]u64, out5: *[4]u64, arg1: u64, arg2: [5]u64, arg3: [5]u64, arg4: [4]u64, arg5: [4]u64) void {
1778    @setRuntimeSafety(mode == .Debug);
1779
1780    var x1: u64 = undefined;
1781    var x2: u1 = undefined;
1782    addcarryxU64(&x1, &x2, 0x0, (~arg1), 0x1);
1783    const x3 = (@as(u1, @truncate((x1 >> 63))) & @as(u1, @truncate(((arg3[0]) & 0x1))));
1784    var x4: u64 = undefined;
1785    var x5: u1 = undefined;
1786    addcarryxU64(&x4, &x5, 0x0, (~arg1), 0x1);
1787    var x6: u64 = undefined;
1788    cmovznzU64(&x6, x3, arg1, x4);
1789    var x7: u64 = undefined;
1790    cmovznzU64(&x7, x3, (arg2[0]), (arg3[0]));
1791    var x8: u64 = undefined;
1792    cmovznzU64(&x8, x3, (arg2[1]), (arg3[1]));
1793    var x9: u64 = undefined;
1794    cmovznzU64(&x9, x3, (arg2[2]), (arg3[2]));
1795    var x10: u64 = undefined;
1796    cmovznzU64(&x10, x3, (arg2[3]), (arg3[3]));
1797    var x11: u64 = undefined;
1798    cmovznzU64(&x11, x3, (arg2[4]), (arg3[4]));
1799    var x12: u64 = undefined;
1800    var x13: u1 = undefined;
1801    addcarryxU64(&x12, &x13, 0x0, 0x1, (~(arg2[0])));
1802    var x14: u64 = undefined;
1803    var x15: u1 = undefined;
1804    addcarryxU64(&x14, &x15, x13, 0x0, (~(arg2[1])));
1805    var x16: u64 = undefined;
1806    var x17: u1 = undefined;
1807    addcarryxU64(&x16, &x17, x15, 0x0, (~(arg2[2])));
1808    var x18: u64 = undefined;
1809    var x19: u1 = undefined;
1810    addcarryxU64(&x18, &x19, x17, 0x0, (~(arg2[3])));
1811    var x20: u64 = undefined;
1812    var x21: u1 = undefined;
1813    addcarryxU64(&x20, &x21, x19, 0x0, (~(arg2[4])));
1814    var x22: u64 = undefined;
1815    cmovznzU64(&x22, x3, (arg3[0]), x12);
1816    var x23: u64 = undefined;
1817    cmovznzU64(&x23, x3, (arg3[1]), x14);
1818    var x24: u64 = undefined;
1819    cmovznzU64(&x24, x3, (arg3[2]), x16);
1820    var x25: u64 = undefined;
1821    cmovznzU64(&x25, x3, (arg3[3]), x18);
1822    var x26: u64 = undefined;
1823    cmovznzU64(&x26, x3, (arg3[4]), x20);
1824    var x27: u64 = undefined;
1825    cmovznzU64(&x27, x3, (arg4[0]), (arg5[0]));
1826    var x28: u64 = undefined;
1827    cmovznzU64(&x28, x3, (arg4[1]), (arg5[1]));
1828    var x29: u64 = undefined;
1829    cmovznzU64(&x29, x3, (arg4[2]), (arg5[2]));
1830    var x30: u64 = undefined;
1831    cmovznzU64(&x30, x3, (arg4[3]), (arg5[3]));
1832    var x31: u64 = undefined;
1833    var x32: u1 = undefined;
1834    addcarryxU64(&x31, &x32, 0x0, x27, x27);
1835    var x33: u64 = undefined;
1836    var x34: u1 = undefined;
1837    addcarryxU64(&x33, &x34, x32, x28, x28);
1838    var x35: u64 = undefined;
1839    var x36: u1 = undefined;
1840    addcarryxU64(&x35, &x36, x34, x29, x29);
1841    var x37: u64 = undefined;
1842    var x38: u1 = undefined;
1843    addcarryxU64(&x37, &x38, x36, x30, x30);
1844    var x39: u64 = undefined;
1845    var x40: u1 = undefined;
1846    subborrowxU64(&x39, &x40, 0x0, x31, 0xbfd25e8cd0364141);
1847    var x41: u64 = undefined;
1848    var x42: u1 = undefined;
1849    subborrowxU64(&x41, &x42, x40, x33, 0xbaaedce6af48a03b);
1850    var x43: u64 = undefined;
1851    var x44: u1 = undefined;
1852    subborrowxU64(&x43, &x44, x42, x35, 0xfffffffffffffffe);
1853    var x45: u64 = undefined;
1854    var x46: u1 = undefined;
1855    subborrowxU64(&x45, &x46, x44, x37, 0xffffffffffffffff);
1856    var x47: u64 = undefined;
1857    var x48: u1 = undefined;
1858    subborrowxU64(&x47, &x48, x46, @as(u64, x38), 0x0);
1859    const x49 = (arg4[3]);
1860    const x50 = (arg4[2]);
1861    const x51 = (arg4[1]);
1862    const x52 = (arg4[0]);
1863    var x53: u64 = undefined;
1864    var x54: u1 = undefined;
1865    subborrowxU64(&x53, &x54, 0x0, 0x0, x52);
1866    var x55: u64 = undefined;
1867    var x56: u1 = undefined;
1868    subborrowxU64(&x55, &x56, x54, 0x0, x51);
1869    var x57: u64 = undefined;
1870    var x58: u1 = undefined;
1871    subborrowxU64(&x57, &x58, x56, 0x0, x50);
1872    var x59: u64 = undefined;
1873    var x60: u1 = undefined;
1874    subborrowxU64(&x59, &x60, x58, 0x0, x49);
1875    var x61: u64 = undefined;
1876    cmovznzU64(&x61, x60, 0x0, 0xffffffffffffffff);
1877    var x62: u64 = undefined;
1878    var x63: u1 = undefined;
1879    addcarryxU64(&x62, &x63, 0x0, x53, (x61 & 0xbfd25e8cd0364141));
1880    var x64: u64 = undefined;
1881    var x65: u1 = undefined;
1882    addcarryxU64(&x64, &x65, x63, x55, (x61 & 0xbaaedce6af48a03b));
1883    var x66: u64 = undefined;
1884    var x67: u1 = undefined;
1885    addcarryxU64(&x66, &x67, x65, x57, (x61 & 0xfffffffffffffffe));
1886    var x68: u64 = undefined;
1887    var x69: u1 = undefined;
1888    addcarryxU64(&x68, &x69, x67, x59, x61);
1889    var x70: u64 = undefined;
1890    cmovznzU64(&x70, x3, (arg5[0]), x62);
1891    var x71: u64 = undefined;
1892    cmovznzU64(&x71, x3, (arg5[1]), x64);
1893    var x72: u64 = undefined;
1894    cmovznzU64(&x72, x3, (arg5[2]), x66);
1895    var x73: u64 = undefined;
1896    cmovznzU64(&x73, x3, (arg5[3]), x68);
1897    const x74 = @as(u1, @truncate((x22 & 0x1)));
1898    var x75: u64 = undefined;
1899    cmovznzU64(&x75, x74, 0x0, x7);
1900    var x76: u64 = undefined;
1901    cmovznzU64(&x76, x74, 0x0, x8);
1902    var x77: u64 = undefined;
1903    cmovznzU64(&x77, x74, 0x0, x9);
1904    var x78: u64 = undefined;
1905    cmovznzU64(&x78, x74, 0x0, x10);
1906    var x79: u64 = undefined;
1907    cmovznzU64(&x79, x74, 0x0, x11);
1908    var x80: u64 = undefined;
1909    var x81: u1 = undefined;
1910    addcarryxU64(&x80, &x81, 0x0, x22, x75);
1911    var x82: u64 = undefined;
1912    var x83: u1 = undefined;
1913    addcarryxU64(&x82, &x83, x81, x23, x76);
1914    var x84: u64 = undefined;
1915    var x85: u1 = undefined;
1916    addcarryxU64(&x84, &x85, x83, x24, x77);
1917    var x86: u64 = undefined;
1918    var x87: u1 = undefined;
1919    addcarryxU64(&x86, &x87, x85, x25, x78);
1920    var x88: u64 = undefined;
1921    var x89: u1 = undefined;
1922    addcarryxU64(&x88, &x89, x87, x26, x79);
1923    var x90: u64 = undefined;
1924    cmovznzU64(&x90, x74, 0x0, x27);
1925    var x91: u64 = undefined;
1926    cmovznzU64(&x91, x74, 0x0, x28);
1927    var x92: u64 = undefined;
1928    cmovznzU64(&x92, x74, 0x0, x29);
1929    var x93: u64 = undefined;
1930    cmovznzU64(&x93, x74, 0x0, x30);
1931    var x94: u64 = undefined;
1932    var x95: u1 = undefined;
1933    addcarryxU64(&x94, &x95, 0x0, x70, x90);
1934    var x96: u64 = undefined;
1935    var x97: u1 = undefined;
1936    addcarryxU64(&x96, &x97, x95, x71, x91);
1937    var x98: u64 = undefined;
1938    var x99: u1 = undefined;
1939    addcarryxU64(&x98, &x99, x97, x72, x92);
1940    var x100: u64 = undefined;
1941    var x101: u1 = undefined;
1942    addcarryxU64(&x100, &x101, x99, x73, x93);
1943    var x102: u64 = undefined;
1944    var x103: u1 = undefined;
1945    subborrowxU64(&x102, &x103, 0x0, x94, 0xbfd25e8cd0364141);
1946    var x104: u64 = undefined;
1947    var x105: u1 = undefined;
1948    subborrowxU64(&x104, &x105, x103, x96, 0xbaaedce6af48a03b);
1949    var x106: u64 = undefined;
1950    var x107: u1 = undefined;
1951    subborrowxU64(&x106, &x107, x105, x98, 0xfffffffffffffffe);
1952    var x108: u64 = undefined;
1953    var x109: u1 = undefined;
1954    subborrowxU64(&x108, &x109, x107, x100, 0xffffffffffffffff);
1955    var x110: u64 = undefined;
1956    var x111: u1 = undefined;
1957    subborrowxU64(&x110, &x111, x109, @as(u64, x101), 0x0);
1958    var x112: u64 = undefined;
1959    var x113: u1 = undefined;
1960    addcarryxU64(&x112, &x113, 0x0, x6, 0x1);
1961    const x114 = ((x80 >> 1) | ((x82 << 63) & 0xffffffffffffffff));
1962    const x115 = ((x82 >> 1) | ((x84 << 63) & 0xffffffffffffffff));
1963    const x116 = ((x84 >> 1) | ((x86 << 63) & 0xffffffffffffffff));
1964    const x117 = ((x86 >> 1) | ((x88 << 63) & 0xffffffffffffffff));
1965    const x118 = ((x88 & 0x8000000000000000) | (x88 >> 1));
1966    var x119: u64 = undefined;
1967    cmovznzU64(&x119, x48, x39, x31);
1968    var x120: u64 = undefined;
1969    cmovznzU64(&x120, x48, x41, x33);
1970    var x121: u64 = undefined;
1971    cmovznzU64(&x121, x48, x43, x35);
1972    var x122: u64 = undefined;
1973    cmovznzU64(&x122, x48, x45, x37);
1974    var x123: u64 = undefined;
1975    cmovznzU64(&x123, x111, x102, x94);
1976    var x124: u64 = undefined;
1977    cmovznzU64(&x124, x111, x104, x96);
1978    var x125: u64 = undefined;
1979    cmovznzU64(&x125, x111, x106, x98);
1980    var x126: u64 = undefined;
1981    cmovznzU64(&x126, x111, x108, x100);
1982    out1.* = x112;
1983    out2[0] = x7;
1984    out2[1] = x8;
1985    out2[2] = x9;
1986    out2[3] = x10;
1987    out2[4] = x11;
1988    out3[0] = x114;
1989    out3[1] = x115;
1990    out3[2] = x116;
1991    out3[3] = x117;
1992    out3[4] = x118;
1993    out4[0] = x119;
1994    out4[1] = x120;
1995    out4[2] = x121;
1996    out4[3] = x122;
1997    out5[0] = x123;
1998    out5[1] = x124;
1999    out5[2] = x125;
2000    out5[3] = x126;
2001}
2002
2003/// The function divstepPrecomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
2004///
2005/// Postconditions:
2006///   eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)
2007///   0 ≤ eval out1 < m
2008///
2009/// Output Bounds:
2010///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2011pub fn divstepPrecomp(out1: *[4]u64) void {
2012    @setRuntimeSafety(mode == .Debug);
2013
2014    out1[0] = 0xd7431a4d2b9cb4e9;
2015    out1[1] = 0xab67d35a32d9c503;
2016    out1[2] = 0xadf6c7e5859ce35f;
2017    out1[3] = 0x615441451df6c379;
2018}