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