zig/lib/std/crypto/pcurves/p384/p384_scalar_64.zig
Andrew Kelley e7b18a7ce6 std.crypto: remove inline from most functions
To quote the language reference,

It is generally better to let the compiler decide when to inline a
function, except for these scenarios:

* To change how many stack frames are in the call stack, for debugging
  purposes.
* To force comptime-ness of the arguments to propagate to the return
  value of the function, as in the above example.
* Real world performance measurements demand it. Don't guess!

Note that inline actually restricts what the compiler is allowed to do.
This can harm binary size, compilation speed, and even runtime
performance.

`zig run lib/std/crypto/benchmark.zig -OReleaseFast`
[-before-] vs {+after+}

              md5:        [-990-]        {+998+} MiB/s
             sha1:       [-1144-]       {+1140+} MiB/s
           sha256:       [-2267-]       {+2275+} MiB/s
           sha512:        [-762-]        {+767+} MiB/s
         sha3-256:        [-680-]        {+683+} MiB/s
         sha3-512:        [-362-]        {+363+} MiB/s
        shake-128:        [-835-]        {+839+} MiB/s
        shake-256:        [-680-]        {+681+} MiB/s
   turboshake-128:       [-1567-]       {+1570+} MiB/s
   turboshake-256:       [-1276-]       {+1282+} MiB/s
          blake2s:        [-778-]        {+789+} MiB/s
          blake2b:       [-1071-]       {+1086+} MiB/s
           blake3:       [-1148-]       {+1137+} MiB/s
            ghash:      [-10044-]      {+10033+} MiB/s
          polyval:       [-9726-]      {+10033+} MiB/s
         poly1305:       [-2486-]       {+2703+} MiB/s
         hmac-md5:        [-991-]        {+998+} MiB/s
        hmac-sha1:       [-1134-]       {+1137+} MiB/s
      hmac-sha256:       [-2265-]       {+2288+} MiB/s
      hmac-sha512:        [-765-]        {+764+} MiB/s
      siphash-2-4:       [-4410-]       {+4438+} MiB/s
      siphash-1-3:       [-7144-]       {+7225+} MiB/s
   siphash128-2-4:       [-4397-]       {+4449+} MiB/s
   siphash128-1-3:       [-7281-]       {+7374+} MiB/s
  aegis-128x4 mac:      [-73385-]      {+74523+} MiB/s
  aegis-256x4 mac:      [-30160-]      {+30539+} MiB/s
  aegis-128x2 mac:      [-66662-]      {+67267+} MiB/s
  aegis-256x2 mac:      [-16812-]      {+16806+} MiB/s
   aegis-128l mac:      [-33876-]      {+34055+} MiB/s
    aegis-256 mac:       [-8993-]       {+9087+} MiB/s
         aes-cmac:       2036 MiB/s
           x25519:      [-20670-]      {+16844+} exchanges/s
          ed25519:      [-29763-]      {+29576+} signatures/s
       ecdsa-p256:       [-4762-]       {+4900+} signatures/s
       ecdsa-p384:       [-1465-]       {+1500+} signatures/s
  ecdsa-secp256k1:       [-5643-]       {+5769+} signatures/s
          ed25519:      [-21926-]      {+21721+} verifications/s
          ed25519:      [-51200-]      {+50880+} verifications/s (batch)
 chacha20Poly1305:       [-1189-]       {+1109+} MiB/s
xchacha20Poly1305:       [-1196-]       {+1107+} MiB/s
 xchacha8Poly1305:       [-1466-]       {+1555+} MiB/s
 xsalsa20Poly1305:        [-660-]        {+620+} MiB/s
      aegis-128x4:      [-76389-]      {+78181+} MiB/s
      aegis-128x2:      [-53946-]      {+53495+} MiB/s
       aegis-128l:      [-27219-]      {+25621+} MiB/s
      aegis-256x4:      [-49351-]      {+49542+} MiB/s
      aegis-256x2:      [-32390-]      {+32366+} MiB/s
        aegis-256:       [-8881-]       {+8944+} MiB/s
       aes128-gcm:       [-6095-]       {+6205+} MiB/s
       aes256-gcm:       [-5306-]       {+5427+} MiB/s
       aes128-ocb:       [-8529-]      {+13974+} MiB/s
       aes256-ocb:       [-7241-]       {+9442+} MiB/s
        isapa128a:        [-204-]        {+214+} MiB/s
    aes128-single:  [-133857882-]  {+134170944+} ops/s
    aes256-single:   [-96306962-]   {+96408639+} ops/s
         aes128-8: [-1083210101-] {+1073727253+} ops/s
         aes256-8:  [-762042466-]  {+767091778+} ops/s
           bcrypt:      0.009 s/ops
           scrypt:      [-0.018-]      {+0.017+} s/ops
           argon2:      [-0.037-]      {+0.060+} s/ops
      kyber512d00:     [-206057-]     {+205779+} encaps/s
      kyber768d00:     [-156074-]     {+150711+} encaps/s
     kyber1024d00:     [-116626-]     {+115469+} encaps/s
      kyber512d00:     [-181149-]     {+182046+} decaps/s
      kyber768d00:     [-136965-]     {+135676+} decaps/s
     kyber1024d00:     [-101307-]     {+100643+} decaps/s
      kyber512d00:     [-123624-]     {+123375+} keygen/s
      kyber768d00:      [-69465-]      {+70828+} keygen/s
     kyber1024d00:      [-43117-]      {+43208+} keygen/s
2025-07-13 18:26:13 +02:00

3627 lines
134 KiB
Zig

// 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 p384_scalar '' 64 '2^384 - 1388124618062372383947042015309946732620727252194336364173' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
// curve description (via package name): p384_scalar
// machine_wordsize = 64 (from "64")
// requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp
// m = 0xffffffffffffffffffffffffffffffffffffffffffffffffc7634d81f4372ddf581a0db248b0a77aecec196accc52973 (from "2^384 - 1388124618062372383947042015309946732620727252194336364173")
//
// NOTE: In addition to the bounds specified above each function, all
// functions synthesized for this Montgomery arithmetic require the
// input to be strictly less than the prime modulus (m), and also
// require the input to be in the unique saturated representation.
// All functions also ensure that these two properties are true of
// return values.
//
// Computed values:
// eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140)
// bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178)
// twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) in
// if x1 & (2^384-1) < 2^383 then x1 & (2^384-1) else (x1 & (2^384-1)) - 2^384
const std = @import("std");
const mode = @import("builtin").mode; // Checked arithmetic is disabled in non-debug modes to avoid side channels
// The type MontgomeryDomainFieldElement is a field element in the Montgomery domain.
// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub const MontgomeryDomainFieldElement = [6]u64;
// The type NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain.
// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub const NonMontgomeryDomainFieldElement = [6]u64;
/// The function addcarryxU64 is an addition with carry.
///
/// Postconditions:
/// out1 = (arg1 + arg2 + arg3) mod 2^64
/// out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
///
/// Input Bounds:
/// arg1: [0x0 ~> 0x1]
/// arg2: [0x0 ~> 0xffffffffffffffff]
/// arg3: [0x0 ~> 0xffffffffffffffff]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
/// out2: [0x0 ~> 0x1]
fn addcarryxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
const x = @as(u128, arg2) +% arg3 +% arg1;
out1.* = @truncate(x);
out2.* = @truncate(x >> 64);
}
/// The function subborrowxU64 is a subtraction with borrow.
///
/// Postconditions:
/// out1 = (-arg1 + arg2 + -arg3) mod 2^64
/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
///
/// Input Bounds:
/// arg1: [0x0 ~> 0x1]
/// arg2: [0x0 ~> 0xffffffffffffffff]
/// arg3: [0x0 ~> 0xffffffffffffffff]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
/// out2: [0x0 ~> 0x1]
fn subborrowxU64(out1: *u64, out2: *u1, arg1: u1, arg2: u64, arg3: u64) void {
const x = @as(u128, arg2) -% arg3 -% arg1;
out1.* = @truncate(x);
out2.* = @truncate(x >> 64);
}
/// The function mulxU64 is a multiplication, returning the full double-width result.
///
/// Postconditions:
/// out1 = (arg1 * arg2) mod 2^64
/// out2 = ⌊arg1 * arg2 / 2^64⌋
///
/// Input Bounds:
/// arg1: [0x0 ~> 0xffffffffffffffff]
/// arg2: [0x0 ~> 0xffffffffffffffff]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
/// out2: [0x0 ~> 0xffffffffffffffff]
fn mulxU64(out1: *u64, out2: *u64, arg1: u64, arg2: u64) void {
@setRuntimeSafety(mode == .Debug);
const x = @as(u128, arg1) * @as(u128, arg2);
out1.* = @as(u64, @truncate(x));
out2.* = @as(u64, @truncate(x >> 64));
}
/// The function cmovznzU64 is a single-word conditional move.
///
/// Postconditions:
/// out1 = (if arg1 = 0 then arg2 else arg3)
///
/// Input Bounds:
/// arg1: [0x0 ~> 0x1]
/// arg2: [0x0 ~> 0xffffffffffffffff]
/// arg3: [0x0 ~> 0xffffffffffffffff]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
fn cmovznzU64(out1: *u64, arg1: u1, arg2: u64, arg3: u64) void {
@setRuntimeSafety(mode == .Debug);
const mask = 0 -% @as(u64, arg1);
out1.* = (mask & arg3) | ((~mask) & arg2);
}
/// The function mul multiplies two field elements in the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// 0 ≤ eval arg2 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
/// 0 ≤ eval out1 < m
///
pub fn mul(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (arg1[1]);
const x2 = (arg1[2]);
const x3 = (arg1[3]);
const x4 = (arg1[4]);
const x5 = (arg1[5]);
const x6 = (arg1[0]);
var x7: u64 = undefined;
var x8: u64 = undefined;
mulxU64(&x7, &x8, x6, (arg2[5]));
var x9: u64 = undefined;
var x10: u64 = undefined;
mulxU64(&x9, &x10, x6, (arg2[4]));
var x11: u64 = undefined;
var x12: u64 = undefined;
mulxU64(&x11, &x12, x6, (arg2[3]));
var x13: u64 = undefined;
var x14: u64 = undefined;
mulxU64(&x13, &x14, x6, (arg2[2]));
var x15: u64 = undefined;
var x16: u64 = undefined;
mulxU64(&x15, &x16, x6, (arg2[1]));
var x17: u64 = undefined;
var x18: u64 = undefined;
mulxU64(&x17, &x18, x6, (arg2[0]));
var x19: u64 = undefined;
var x20: u1 = undefined;
addcarryxU64(&x19, &x20, 0x0, x18, x15);
var x21: u64 = undefined;
var x22: u1 = undefined;
addcarryxU64(&x21, &x22, x20, x16, x13);
var x23: u64 = undefined;
var x24: u1 = undefined;
addcarryxU64(&x23, &x24, x22, x14, x11);
var x25: u64 = undefined;
var x26: u1 = undefined;
addcarryxU64(&x25, &x26, x24, x12, x9);
var x27: u64 = undefined;
var x28: u1 = undefined;
addcarryxU64(&x27, &x28, x26, x10, x7);
const x29 = (@as(u64, x28) + x8);
var x30: u64 = undefined;
var x31: u64 = undefined;
mulxU64(&x30, &x31, x17, 0x6ed46089e88fdc45);
var x32: u64 = undefined;
var x33: u64 = undefined;
mulxU64(&x32, &x33, x30, 0xffffffffffffffff);
var x34: u64 = undefined;
var x35: u64 = undefined;
mulxU64(&x34, &x35, x30, 0xffffffffffffffff);
var x36: u64 = undefined;
var x37: u64 = undefined;
mulxU64(&x36, &x37, x30, 0xffffffffffffffff);
var x38: u64 = undefined;
var x39: u64 = undefined;
mulxU64(&x38, &x39, x30, 0xc7634d81f4372ddf);
var x40: u64 = undefined;
var x41: u64 = undefined;
mulxU64(&x40, &x41, x30, 0x581a0db248b0a77a);
var x42: u64 = undefined;
var x43: u64 = undefined;
mulxU64(&x42, &x43, x30, 0xecec196accc52973);
var x44: u64 = undefined;
var x45: u1 = undefined;
addcarryxU64(&x44, &x45, 0x0, x43, x40);
var x46: u64 = undefined;
var x47: u1 = undefined;
addcarryxU64(&x46, &x47, x45, x41, x38);
var x48: u64 = undefined;
var x49: u1 = undefined;
addcarryxU64(&x48, &x49, x47, x39, x36);
var x50: u64 = undefined;
var x51: u1 = undefined;
addcarryxU64(&x50, &x51, x49, x37, x34);
var x52: u64 = undefined;
var x53: u1 = undefined;
addcarryxU64(&x52, &x53, x51, x35, x32);
const x54 = (@as(u64, x53) + x33);
var x55: u64 = undefined;
var x56: u1 = undefined;
addcarryxU64(&x55, &x56, 0x0, x17, x42);
var x57: u64 = undefined;
var x58: u1 = undefined;
addcarryxU64(&x57, &x58, x56, x19, x44);
var x59: u64 = undefined;
var x60: u1 = undefined;
addcarryxU64(&x59, &x60, x58, x21, x46);
var x61: u64 = undefined;
var x62: u1 = undefined;
addcarryxU64(&x61, &x62, x60, x23, x48);
var x63: u64 = undefined;
var x64: u1 = undefined;
addcarryxU64(&x63, &x64, x62, x25, x50);
var x65: u64 = undefined;
var x66: u1 = undefined;
addcarryxU64(&x65, &x66, x64, x27, x52);
var x67: u64 = undefined;
var x68: u1 = undefined;
addcarryxU64(&x67, &x68, x66, x29, x54);
var x69: u64 = undefined;
var x70: u64 = undefined;
mulxU64(&x69, &x70, x1, (arg2[5]));
var x71: u64 = undefined;
var x72: u64 = undefined;
mulxU64(&x71, &x72, x1, (arg2[4]));
var x73: u64 = undefined;
var x74: u64 = undefined;
mulxU64(&x73, &x74, x1, (arg2[3]));
var x75: u64 = undefined;
var x76: u64 = undefined;
mulxU64(&x75, &x76, x1, (arg2[2]));
var x77: u64 = undefined;
var x78: u64 = undefined;
mulxU64(&x77, &x78, x1, (arg2[1]));
var x79: u64 = undefined;
var x80: u64 = undefined;
mulxU64(&x79, &x80, x1, (arg2[0]));
var x81: u64 = undefined;
var x82: u1 = undefined;
addcarryxU64(&x81, &x82, 0x0, x80, x77);
var x83: u64 = undefined;
var x84: u1 = undefined;
addcarryxU64(&x83, &x84, x82, x78, x75);
var x85: u64 = undefined;
var x86: u1 = undefined;
addcarryxU64(&x85, &x86, x84, x76, x73);
var x87: u64 = undefined;
var x88: u1 = undefined;
addcarryxU64(&x87, &x88, x86, x74, x71);
var x89: u64 = undefined;
var x90: u1 = undefined;
addcarryxU64(&x89, &x90, x88, x72, x69);
const x91 = (@as(u64, x90) + x70);
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, 0x0, x57, x79);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x59, x81);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x61, x83);
var x98: u64 = undefined;
var x99: u1 = undefined;
addcarryxU64(&x98, &x99, x97, x63, x85);
var x100: u64 = undefined;
var x101: u1 = undefined;
addcarryxU64(&x100, &x101, x99, x65, x87);
var x102: u64 = undefined;
var x103: u1 = undefined;
addcarryxU64(&x102, &x103, x101, x67, x89);
var x104: u64 = undefined;
var x105: u1 = undefined;
addcarryxU64(&x104, &x105, x103, @as(u64, x68), x91);
var x106: u64 = undefined;
var x107: u64 = undefined;
mulxU64(&x106, &x107, x92, 0x6ed46089e88fdc45);
var x108: u64 = undefined;
var x109: u64 = undefined;
mulxU64(&x108, &x109, x106, 0xffffffffffffffff);
var x110: u64 = undefined;
var x111: u64 = undefined;
mulxU64(&x110, &x111, x106, 0xffffffffffffffff);
var x112: u64 = undefined;
var x113: u64 = undefined;
mulxU64(&x112, &x113, x106, 0xffffffffffffffff);
var x114: u64 = undefined;
var x115: u64 = undefined;
mulxU64(&x114, &x115, x106, 0xc7634d81f4372ddf);
var x116: u64 = undefined;
var x117: u64 = undefined;
mulxU64(&x116, &x117, x106, 0x581a0db248b0a77a);
var x118: u64 = undefined;
var x119: u64 = undefined;
mulxU64(&x118, &x119, x106, 0xecec196accc52973);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, 0x0, x119, x116);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x117, x114);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x115, x112);
var x126: u64 = undefined;
var x127: u1 = undefined;
addcarryxU64(&x126, &x127, x125, x113, x110);
var x128: u64 = undefined;
var x129: u1 = undefined;
addcarryxU64(&x128, &x129, x127, x111, x108);
const x130 = (@as(u64, x129) + x109);
var x131: u64 = undefined;
var x132: u1 = undefined;
addcarryxU64(&x131, &x132, 0x0, x92, x118);
var x133: u64 = undefined;
var x134: u1 = undefined;
addcarryxU64(&x133, &x134, x132, x94, x120);
var x135: u64 = undefined;
var x136: u1 = undefined;
addcarryxU64(&x135, &x136, x134, x96, x122);
var x137: u64 = undefined;
var x138: u1 = undefined;
addcarryxU64(&x137, &x138, x136, x98, x124);
var x139: u64 = undefined;
var x140: u1 = undefined;
addcarryxU64(&x139, &x140, x138, x100, x126);
var x141: u64 = undefined;
var x142: u1 = undefined;
addcarryxU64(&x141, &x142, x140, x102, x128);
var x143: u64 = undefined;
var x144: u1 = undefined;
addcarryxU64(&x143, &x144, x142, x104, x130);
const x145 = (@as(u64, x144) + @as(u64, x105));
var x146: u64 = undefined;
var x147: u64 = undefined;
mulxU64(&x146, &x147, x2, (arg2[5]));
var x148: u64 = undefined;
var x149: u64 = undefined;
mulxU64(&x148, &x149, x2, (arg2[4]));
var x150: u64 = undefined;
var x151: u64 = undefined;
mulxU64(&x150, &x151, x2, (arg2[3]));
var x152: u64 = undefined;
var x153: u64 = undefined;
mulxU64(&x152, &x153, x2, (arg2[2]));
var x154: u64 = undefined;
var x155: u64 = undefined;
mulxU64(&x154, &x155, x2, (arg2[1]));
var x156: u64 = undefined;
var x157: u64 = undefined;
mulxU64(&x156, &x157, x2, (arg2[0]));
var x158: u64 = undefined;
var x159: u1 = undefined;
addcarryxU64(&x158, &x159, 0x0, x157, x154);
var x160: u64 = undefined;
var x161: u1 = undefined;
addcarryxU64(&x160, &x161, x159, x155, x152);
var x162: u64 = undefined;
var x163: u1 = undefined;
addcarryxU64(&x162, &x163, x161, x153, x150);
var x164: u64 = undefined;
var x165: u1 = undefined;
addcarryxU64(&x164, &x165, x163, x151, x148);
var x166: u64 = undefined;
var x167: u1 = undefined;
addcarryxU64(&x166, &x167, x165, x149, x146);
const x168 = (@as(u64, x167) + x147);
var x169: u64 = undefined;
var x170: u1 = undefined;
addcarryxU64(&x169, &x170, 0x0, x133, x156);
var x171: u64 = undefined;
var x172: u1 = undefined;
addcarryxU64(&x171, &x172, x170, x135, x158);
var x173: u64 = undefined;
var x174: u1 = undefined;
addcarryxU64(&x173, &x174, x172, x137, x160);
var x175: u64 = undefined;
var x176: u1 = undefined;
addcarryxU64(&x175, &x176, x174, x139, x162);
var x177: u64 = undefined;
var x178: u1 = undefined;
addcarryxU64(&x177, &x178, x176, x141, x164);
var x179: u64 = undefined;
var x180: u1 = undefined;
addcarryxU64(&x179, &x180, x178, x143, x166);
var x181: u64 = undefined;
var x182: u1 = undefined;
addcarryxU64(&x181, &x182, x180, x145, x168);
var x183: u64 = undefined;
var x184: u64 = undefined;
mulxU64(&x183, &x184, x169, 0x6ed46089e88fdc45);
var x185: u64 = undefined;
var x186: u64 = undefined;
mulxU64(&x185, &x186, x183, 0xffffffffffffffff);
var x187: u64 = undefined;
var x188: u64 = undefined;
mulxU64(&x187, &x188, x183, 0xffffffffffffffff);
var x189: u64 = undefined;
var x190: u64 = undefined;
mulxU64(&x189, &x190, x183, 0xffffffffffffffff);
var x191: u64 = undefined;
var x192: u64 = undefined;
mulxU64(&x191, &x192, x183, 0xc7634d81f4372ddf);
var x193: u64 = undefined;
var x194: u64 = undefined;
mulxU64(&x193, &x194, x183, 0x581a0db248b0a77a);
var x195: u64 = undefined;
var x196: u64 = undefined;
mulxU64(&x195, &x196, x183, 0xecec196accc52973);
var x197: u64 = undefined;
var x198: u1 = undefined;
addcarryxU64(&x197, &x198, 0x0, x196, x193);
var x199: u64 = undefined;
var x200: u1 = undefined;
addcarryxU64(&x199, &x200, x198, x194, x191);
var x201: u64 = undefined;
var x202: u1 = undefined;
addcarryxU64(&x201, &x202, x200, x192, x189);
var x203: u64 = undefined;
var x204: u1 = undefined;
addcarryxU64(&x203, &x204, x202, x190, x187);
var x205: u64 = undefined;
var x206: u1 = undefined;
addcarryxU64(&x205, &x206, x204, x188, x185);
const x207 = (@as(u64, x206) + x186);
var x208: u64 = undefined;
var x209: u1 = undefined;
addcarryxU64(&x208, &x209, 0x0, x169, x195);
var x210: u64 = undefined;
var x211: u1 = undefined;
addcarryxU64(&x210, &x211, x209, x171, x197);
var x212: u64 = undefined;
var x213: u1 = undefined;
addcarryxU64(&x212, &x213, x211, x173, x199);
var x214: u64 = undefined;
var x215: u1 = undefined;
addcarryxU64(&x214, &x215, x213, x175, x201);
var x216: u64 = undefined;
var x217: u1 = undefined;
addcarryxU64(&x216, &x217, x215, x177, x203);
var x218: u64 = undefined;
var x219: u1 = undefined;
addcarryxU64(&x218, &x219, x217, x179, x205);
var x220: u64 = undefined;
var x221: u1 = undefined;
addcarryxU64(&x220, &x221, x219, x181, x207);
const x222 = (@as(u64, x221) + @as(u64, x182));
var x223: u64 = undefined;
var x224: u64 = undefined;
mulxU64(&x223, &x224, x3, (arg2[5]));
var x225: u64 = undefined;
var x226: u64 = undefined;
mulxU64(&x225, &x226, x3, (arg2[4]));
var x227: u64 = undefined;
var x228: u64 = undefined;
mulxU64(&x227, &x228, x3, (arg2[3]));
var x229: u64 = undefined;
var x230: u64 = undefined;
mulxU64(&x229, &x230, x3, (arg2[2]));
var x231: u64 = undefined;
var x232: u64 = undefined;
mulxU64(&x231, &x232, x3, (arg2[1]));
var x233: u64 = undefined;
var x234: u64 = undefined;
mulxU64(&x233, &x234, x3, (arg2[0]));
var x235: u64 = undefined;
var x236: u1 = undefined;
addcarryxU64(&x235, &x236, 0x0, x234, x231);
var x237: u64 = undefined;
var x238: u1 = undefined;
addcarryxU64(&x237, &x238, x236, x232, x229);
var x239: u64 = undefined;
var x240: u1 = undefined;
addcarryxU64(&x239, &x240, x238, x230, x227);
var x241: u64 = undefined;
var x242: u1 = undefined;
addcarryxU64(&x241, &x242, x240, x228, x225);
var x243: u64 = undefined;
var x244: u1 = undefined;
addcarryxU64(&x243, &x244, x242, x226, x223);
const x245 = (@as(u64, x244) + x224);
var x246: u64 = undefined;
var x247: u1 = undefined;
addcarryxU64(&x246, &x247, 0x0, x210, x233);
var x248: u64 = undefined;
var x249: u1 = undefined;
addcarryxU64(&x248, &x249, x247, x212, x235);
var x250: u64 = undefined;
var x251: u1 = undefined;
addcarryxU64(&x250, &x251, x249, x214, x237);
var x252: u64 = undefined;
var x253: u1 = undefined;
addcarryxU64(&x252, &x253, x251, x216, x239);
var x254: u64 = undefined;
var x255: u1 = undefined;
addcarryxU64(&x254, &x255, x253, x218, x241);
var x256: u64 = undefined;
var x257: u1 = undefined;
addcarryxU64(&x256, &x257, x255, x220, x243);
var x258: u64 = undefined;
var x259: u1 = undefined;
addcarryxU64(&x258, &x259, x257, x222, x245);
var x260: u64 = undefined;
var x261: u64 = undefined;
mulxU64(&x260, &x261, x246, 0x6ed46089e88fdc45);
var x262: u64 = undefined;
var x263: u64 = undefined;
mulxU64(&x262, &x263, x260, 0xffffffffffffffff);
var x264: u64 = undefined;
var x265: u64 = undefined;
mulxU64(&x264, &x265, x260, 0xffffffffffffffff);
var x266: u64 = undefined;
var x267: u64 = undefined;
mulxU64(&x266, &x267, x260, 0xffffffffffffffff);
var x268: u64 = undefined;
var x269: u64 = undefined;
mulxU64(&x268, &x269, x260, 0xc7634d81f4372ddf);
var x270: u64 = undefined;
var x271: u64 = undefined;
mulxU64(&x270, &x271, x260, 0x581a0db248b0a77a);
var x272: u64 = undefined;
var x273: u64 = undefined;
mulxU64(&x272, &x273, x260, 0xecec196accc52973);
var x274: u64 = undefined;
var x275: u1 = undefined;
addcarryxU64(&x274, &x275, 0x0, x273, x270);
var x276: u64 = undefined;
var x277: u1 = undefined;
addcarryxU64(&x276, &x277, x275, x271, x268);
var x278: u64 = undefined;
var x279: u1 = undefined;
addcarryxU64(&x278, &x279, x277, x269, x266);
var x280: u64 = undefined;
var x281: u1 = undefined;
addcarryxU64(&x280, &x281, x279, x267, x264);
var x282: u64 = undefined;
var x283: u1 = undefined;
addcarryxU64(&x282, &x283, x281, x265, x262);
const x284 = (@as(u64, x283) + x263);
var x285: u64 = undefined;
var x286: u1 = undefined;
addcarryxU64(&x285, &x286, 0x0, x246, x272);
var x287: u64 = undefined;
var x288: u1 = undefined;
addcarryxU64(&x287, &x288, x286, x248, x274);
var x289: u64 = undefined;
var x290: u1 = undefined;
addcarryxU64(&x289, &x290, x288, x250, x276);
var x291: u64 = undefined;
var x292: u1 = undefined;
addcarryxU64(&x291, &x292, x290, x252, x278);
var x293: u64 = undefined;
var x294: u1 = undefined;
addcarryxU64(&x293, &x294, x292, x254, x280);
var x295: u64 = undefined;
var x296: u1 = undefined;
addcarryxU64(&x295, &x296, x294, x256, x282);
var x297: u64 = undefined;
var x298: u1 = undefined;
addcarryxU64(&x297, &x298, x296, x258, x284);
const x299 = (@as(u64, x298) + @as(u64, x259));
var x300: u64 = undefined;
var x301: u64 = undefined;
mulxU64(&x300, &x301, x4, (arg2[5]));
var x302: u64 = undefined;
var x303: u64 = undefined;
mulxU64(&x302, &x303, x4, (arg2[4]));
var x304: u64 = undefined;
var x305: u64 = undefined;
mulxU64(&x304, &x305, x4, (arg2[3]));
var x306: u64 = undefined;
var x307: u64 = undefined;
mulxU64(&x306, &x307, x4, (arg2[2]));
var x308: u64 = undefined;
var x309: u64 = undefined;
mulxU64(&x308, &x309, x4, (arg2[1]));
var x310: u64 = undefined;
var x311: u64 = undefined;
mulxU64(&x310, &x311, x4, (arg2[0]));
var x312: u64 = undefined;
var x313: u1 = undefined;
addcarryxU64(&x312, &x313, 0x0, x311, x308);
var x314: u64 = undefined;
var x315: u1 = undefined;
addcarryxU64(&x314, &x315, x313, x309, x306);
var x316: u64 = undefined;
var x317: u1 = undefined;
addcarryxU64(&x316, &x317, x315, x307, x304);
var x318: u64 = undefined;
var x319: u1 = undefined;
addcarryxU64(&x318, &x319, x317, x305, x302);
var x320: u64 = undefined;
var x321: u1 = undefined;
addcarryxU64(&x320, &x321, x319, x303, x300);
const x322 = (@as(u64, x321) + x301);
var x323: u64 = undefined;
var x324: u1 = undefined;
addcarryxU64(&x323, &x324, 0x0, x287, x310);
var x325: u64 = undefined;
var x326: u1 = undefined;
addcarryxU64(&x325, &x326, x324, x289, x312);
var x327: u64 = undefined;
var x328: u1 = undefined;
addcarryxU64(&x327, &x328, x326, x291, x314);
var x329: u64 = undefined;
var x330: u1 = undefined;
addcarryxU64(&x329, &x330, x328, x293, x316);
var x331: u64 = undefined;
var x332: u1 = undefined;
addcarryxU64(&x331, &x332, x330, x295, x318);
var x333: u64 = undefined;
var x334: u1 = undefined;
addcarryxU64(&x333, &x334, x332, x297, x320);
var x335: u64 = undefined;
var x336: u1 = undefined;
addcarryxU64(&x335, &x336, x334, x299, x322);
var x337: u64 = undefined;
var x338: u64 = undefined;
mulxU64(&x337, &x338, x323, 0x6ed46089e88fdc45);
var x339: u64 = undefined;
var x340: u64 = undefined;
mulxU64(&x339, &x340, x337, 0xffffffffffffffff);
var x341: u64 = undefined;
var x342: u64 = undefined;
mulxU64(&x341, &x342, x337, 0xffffffffffffffff);
var x343: u64 = undefined;
var x344: u64 = undefined;
mulxU64(&x343, &x344, x337, 0xffffffffffffffff);
var x345: u64 = undefined;
var x346: u64 = undefined;
mulxU64(&x345, &x346, x337, 0xc7634d81f4372ddf);
var x347: u64 = undefined;
var x348: u64 = undefined;
mulxU64(&x347, &x348, x337, 0x581a0db248b0a77a);
var x349: u64 = undefined;
var x350: u64 = undefined;
mulxU64(&x349, &x350, x337, 0xecec196accc52973);
var x351: u64 = undefined;
var x352: u1 = undefined;
addcarryxU64(&x351, &x352, 0x0, x350, x347);
var x353: u64 = undefined;
var x354: u1 = undefined;
addcarryxU64(&x353, &x354, x352, x348, x345);
var x355: u64 = undefined;
var x356: u1 = undefined;
addcarryxU64(&x355, &x356, x354, x346, x343);
var x357: u64 = undefined;
var x358: u1 = undefined;
addcarryxU64(&x357, &x358, x356, x344, x341);
var x359: u64 = undefined;
var x360: u1 = undefined;
addcarryxU64(&x359, &x360, x358, x342, x339);
const x361 = (@as(u64, x360) + x340);
var x362: u64 = undefined;
var x363: u1 = undefined;
addcarryxU64(&x362, &x363, 0x0, x323, x349);
var x364: u64 = undefined;
var x365: u1 = undefined;
addcarryxU64(&x364, &x365, x363, x325, x351);
var x366: u64 = undefined;
var x367: u1 = undefined;
addcarryxU64(&x366, &x367, x365, x327, x353);
var x368: u64 = undefined;
var x369: u1 = undefined;
addcarryxU64(&x368, &x369, x367, x329, x355);
var x370: u64 = undefined;
var x371: u1 = undefined;
addcarryxU64(&x370, &x371, x369, x331, x357);
var x372: u64 = undefined;
var x373: u1 = undefined;
addcarryxU64(&x372, &x373, x371, x333, x359);
var x374: u64 = undefined;
var x375: u1 = undefined;
addcarryxU64(&x374, &x375, x373, x335, x361);
const x376 = (@as(u64, x375) + @as(u64, x336));
var x377: u64 = undefined;
var x378: u64 = undefined;
mulxU64(&x377, &x378, x5, (arg2[5]));
var x379: u64 = undefined;
var x380: u64 = undefined;
mulxU64(&x379, &x380, x5, (arg2[4]));
var x381: u64 = undefined;
var x382: u64 = undefined;
mulxU64(&x381, &x382, x5, (arg2[3]));
var x383: u64 = undefined;
var x384: u64 = undefined;
mulxU64(&x383, &x384, x5, (arg2[2]));
var x385: u64 = undefined;
var x386: u64 = undefined;
mulxU64(&x385, &x386, x5, (arg2[1]));
var x387: u64 = undefined;
var x388: u64 = undefined;
mulxU64(&x387, &x388, x5, (arg2[0]));
var x389: u64 = undefined;
var x390: u1 = undefined;
addcarryxU64(&x389, &x390, 0x0, x388, x385);
var x391: u64 = undefined;
var x392: u1 = undefined;
addcarryxU64(&x391, &x392, x390, x386, x383);
var x393: u64 = undefined;
var x394: u1 = undefined;
addcarryxU64(&x393, &x394, x392, x384, x381);
var x395: u64 = undefined;
var x396: u1 = undefined;
addcarryxU64(&x395, &x396, x394, x382, x379);
var x397: u64 = undefined;
var x398: u1 = undefined;
addcarryxU64(&x397, &x398, x396, x380, x377);
const x399 = (@as(u64, x398) + x378);
var x400: u64 = undefined;
var x401: u1 = undefined;
addcarryxU64(&x400, &x401, 0x0, x364, x387);
var x402: u64 = undefined;
var x403: u1 = undefined;
addcarryxU64(&x402, &x403, x401, x366, x389);
var x404: u64 = undefined;
var x405: u1 = undefined;
addcarryxU64(&x404, &x405, x403, x368, x391);
var x406: u64 = undefined;
var x407: u1 = undefined;
addcarryxU64(&x406, &x407, x405, x370, x393);
var x408: u64 = undefined;
var x409: u1 = undefined;
addcarryxU64(&x408, &x409, x407, x372, x395);
var x410: u64 = undefined;
var x411: u1 = undefined;
addcarryxU64(&x410, &x411, x409, x374, x397);
var x412: u64 = undefined;
var x413: u1 = undefined;
addcarryxU64(&x412, &x413, x411, x376, x399);
var x414: u64 = undefined;
var x415: u64 = undefined;
mulxU64(&x414, &x415, x400, 0x6ed46089e88fdc45);
var x416: u64 = undefined;
var x417: u64 = undefined;
mulxU64(&x416, &x417, x414, 0xffffffffffffffff);
var x418: u64 = undefined;
var x419: u64 = undefined;
mulxU64(&x418, &x419, x414, 0xffffffffffffffff);
var x420: u64 = undefined;
var x421: u64 = undefined;
mulxU64(&x420, &x421, x414, 0xffffffffffffffff);
var x422: u64 = undefined;
var x423: u64 = undefined;
mulxU64(&x422, &x423, x414, 0xc7634d81f4372ddf);
var x424: u64 = undefined;
var x425: u64 = undefined;
mulxU64(&x424, &x425, x414, 0x581a0db248b0a77a);
var x426: u64 = undefined;
var x427: u64 = undefined;
mulxU64(&x426, &x427, x414, 0xecec196accc52973);
var x428: u64 = undefined;
var x429: u1 = undefined;
addcarryxU64(&x428, &x429, 0x0, x427, x424);
var x430: u64 = undefined;
var x431: u1 = undefined;
addcarryxU64(&x430, &x431, x429, x425, x422);
var x432: u64 = undefined;
var x433: u1 = undefined;
addcarryxU64(&x432, &x433, x431, x423, x420);
var x434: u64 = undefined;
var x435: u1 = undefined;
addcarryxU64(&x434, &x435, x433, x421, x418);
var x436: u64 = undefined;
var x437: u1 = undefined;
addcarryxU64(&x436, &x437, x435, x419, x416);
const x438 = (@as(u64, x437) + x417);
var x439: u64 = undefined;
var x440: u1 = undefined;
addcarryxU64(&x439, &x440, 0x0, x400, x426);
var x441: u64 = undefined;
var x442: u1 = undefined;
addcarryxU64(&x441, &x442, x440, x402, x428);
var x443: u64 = undefined;
var x444: u1 = undefined;
addcarryxU64(&x443, &x444, x442, x404, x430);
var x445: u64 = undefined;
var x446: u1 = undefined;
addcarryxU64(&x445, &x446, x444, x406, x432);
var x447: u64 = undefined;
var x448: u1 = undefined;
addcarryxU64(&x447, &x448, x446, x408, x434);
var x449: u64 = undefined;
var x450: u1 = undefined;
addcarryxU64(&x449, &x450, x448, x410, x436);
var x451: u64 = undefined;
var x452: u1 = undefined;
addcarryxU64(&x451, &x452, x450, x412, x438);
const x453 = (@as(u64, x452) + @as(u64, x413));
var x454: u64 = undefined;
var x455: u1 = undefined;
subborrowxU64(&x454, &x455, 0x0, x441, 0xecec196accc52973);
var x456: u64 = undefined;
var x457: u1 = undefined;
subborrowxU64(&x456, &x457, x455, x443, 0x581a0db248b0a77a);
var x458: u64 = undefined;
var x459: u1 = undefined;
subborrowxU64(&x458, &x459, x457, x445, 0xc7634d81f4372ddf);
var x460: u64 = undefined;
var x461: u1 = undefined;
subborrowxU64(&x460, &x461, x459, x447, 0xffffffffffffffff);
var x462: u64 = undefined;
var x463: u1 = undefined;
subborrowxU64(&x462, &x463, x461, x449, 0xffffffffffffffff);
var x464: u64 = undefined;
var x465: u1 = undefined;
subborrowxU64(&x464, &x465, x463, x451, 0xffffffffffffffff);
var x466: u64 = undefined;
var x467: u1 = undefined;
subborrowxU64(&x466, &x467, x465, x453, 0x0);
var x468: u64 = undefined;
cmovznzU64(&x468, x467, x454, x441);
var x469: u64 = undefined;
cmovznzU64(&x469, x467, x456, x443);
var x470: u64 = undefined;
cmovznzU64(&x470, x467, x458, x445);
var x471: u64 = undefined;
cmovznzU64(&x471, x467, x460, x447);
var x472: u64 = undefined;
cmovznzU64(&x472, x467, x462, x449);
var x473: u64 = undefined;
cmovznzU64(&x473, x467, x464, x451);
out1[0] = x468;
out1[1] = x469;
out1[2] = x470;
out1[3] = x471;
out1[4] = x472;
out1[5] = x473;
}
/// The function square squares a field element in the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
/// 0 ≤ eval out1 < m
///
pub fn square(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (arg1[1]);
const x2 = (arg1[2]);
const x3 = (arg1[3]);
const x4 = (arg1[4]);
const x5 = (arg1[5]);
const x6 = (arg1[0]);
var x7: u64 = undefined;
var x8: u64 = undefined;
mulxU64(&x7, &x8, x6, (arg1[5]));
var x9: u64 = undefined;
var x10: u64 = undefined;
mulxU64(&x9, &x10, x6, (arg1[4]));
var x11: u64 = undefined;
var x12: u64 = undefined;
mulxU64(&x11, &x12, x6, (arg1[3]));
var x13: u64 = undefined;
var x14: u64 = undefined;
mulxU64(&x13, &x14, x6, (arg1[2]));
var x15: u64 = undefined;
var x16: u64 = undefined;
mulxU64(&x15, &x16, x6, (arg1[1]));
var x17: u64 = undefined;
var x18: u64 = undefined;
mulxU64(&x17, &x18, x6, (arg1[0]));
var x19: u64 = undefined;
var x20: u1 = undefined;
addcarryxU64(&x19, &x20, 0x0, x18, x15);
var x21: u64 = undefined;
var x22: u1 = undefined;
addcarryxU64(&x21, &x22, x20, x16, x13);
var x23: u64 = undefined;
var x24: u1 = undefined;
addcarryxU64(&x23, &x24, x22, x14, x11);
var x25: u64 = undefined;
var x26: u1 = undefined;
addcarryxU64(&x25, &x26, x24, x12, x9);
var x27: u64 = undefined;
var x28: u1 = undefined;
addcarryxU64(&x27, &x28, x26, x10, x7);
const x29 = (@as(u64, x28) + x8);
var x30: u64 = undefined;
var x31: u64 = undefined;
mulxU64(&x30, &x31, x17, 0x6ed46089e88fdc45);
var x32: u64 = undefined;
var x33: u64 = undefined;
mulxU64(&x32, &x33, x30, 0xffffffffffffffff);
var x34: u64 = undefined;
var x35: u64 = undefined;
mulxU64(&x34, &x35, x30, 0xffffffffffffffff);
var x36: u64 = undefined;
var x37: u64 = undefined;
mulxU64(&x36, &x37, x30, 0xffffffffffffffff);
var x38: u64 = undefined;
var x39: u64 = undefined;
mulxU64(&x38, &x39, x30, 0xc7634d81f4372ddf);
var x40: u64 = undefined;
var x41: u64 = undefined;
mulxU64(&x40, &x41, x30, 0x581a0db248b0a77a);
var x42: u64 = undefined;
var x43: u64 = undefined;
mulxU64(&x42, &x43, x30, 0xecec196accc52973);
var x44: u64 = undefined;
var x45: u1 = undefined;
addcarryxU64(&x44, &x45, 0x0, x43, x40);
var x46: u64 = undefined;
var x47: u1 = undefined;
addcarryxU64(&x46, &x47, x45, x41, x38);
var x48: u64 = undefined;
var x49: u1 = undefined;
addcarryxU64(&x48, &x49, x47, x39, x36);
var x50: u64 = undefined;
var x51: u1 = undefined;
addcarryxU64(&x50, &x51, x49, x37, x34);
var x52: u64 = undefined;
var x53: u1 = undefined;
addcarryxU64(&x52, &x53, x51, x35, x32);
const x54 = (@as(u64, x53) + x33);
var x55: u64 = undefined;
var x56: u1 = undefined;
addcarryxU64(&x55, &x56, 0x0, x17, x42);
var x57: u64 = undefined;
var x58: u1 = undefined;
addcarryxU64(&x57, &x58, x56, x19, x44);
var x59: u64 = undefined;
var x60: u1 = undefined;
addcarryxU64(&x59, &x60, x58, x21, x46);
var x61: u64 = undefined;
var x62: u1 = undefined;
addcarryxU64(&x61, &x62, x60, x23, x48);
var x63: u64 = undefined;
var x64: u1 = undefined;
addcarryxU64(&x63, &x64, x62, x25, x50);
var x65: u64 = undefined;
var x66: u1 = undefined;
addcarryxU64(&x65, &x66, x64, x27, x52);
var x67: u64 = undefined;
var x68: u1 = undefined;
addcarryxU64(&x67, &x68, x66, x29, x54);
var x69: u64 = undefined;
var x70: u64 = undefined;
mulxU64(&x69, &x70, x1, (arg1[5]));
var x71: u64 = undefined;
var x72: u64 = undefined;
mulxU64(&x71, &x72, x1, (arg1[4]));
var x73: u64 = undefined;
var x74: u64 = undefined;
mulxU64(&x73, &x74, x1, (arg1[3]));
var x75: u64 = undefined;
var x76: u64 = undefined;
mulxU64(&x75, &x76, x1, (arg1[2]));
var x77: u64 = undefined;
var x78: u64 = undefined;
mulxU64(&x77, &x78, x1, (arg1[1]));
var x79: u64 = undefined;
var x80: u64 = undefined;
mulxU64(&x79, &x80, x1, (arg1[0]));
var x81: u64 = undefined;
var x82: u1 = undefined;
addcarryxU64(&x81, &x82, 0x0, x80, x77);
var x83: u64 = undefined;
var x84: u1 = undefined;
addcarryxU64(&x83, &x84, x82, x78, x75);
var x85: u64 = undefined;
var x86: u1 = undefined;
addcarryxU64(&x85, &x86, x84, x76, x73);
var x87: u64 = undefined;
var x88: u1 = undefined;
addcarryxU64(&x87, &x88, x86, x74, x71);
var x89: u64 = undefined;
var x90: u1 = undefined;
addcarryxU64(&x89, &x90, x88, x72, x69);
const x91 = (@as(u64, x90) + x70);
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, 0x0, x57, x79);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x59, x81);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x61, x83);
var x98: u64 = undefined;
var x99: u1 = undefined;
addcarryxU64(&x98, &x99, x97, x63, x85);
var x100: u64 = undefined;
var x101: u1 = undefined;
addcarryxU64(&x100, &x101, x99, x65, x87);
var x102: u64 = undefined;
var x103: u1 = undefined;
addcarryxU64(&x102, &x103, x101, x67, x89);
var x104: u64 = undefined;
var x105: u1 = undefined;
addcarryxU64(&x104, &x105, x103, @as(u64, x68), x91);
var x106: u64 = undefined;
var x107: u64 = undefined;
mulxU64(&x106, &x107, x92, 0x6ed46089e88fdc45);
var x108: u64 = undefined;
var x109: u64 = undefined;
mulxU64(&x108, &x109, x106, 0xffffffffffffffff);
var x110: u64 = undefined;
var x111: u64 = undefined;
mulxU64(&x110, &x111, x106, 0xffffffffffffffff);
var x112: u64 = undefined;
var x113: u64 = undefined;
mulxU64(&x112, &x113, x106, 0xffffffffffffffff);
var x114: u64 = undefined;
var x115: u64 = undefined;
mulxU64(&x114, &x115, x106, 0xc7634d81f4372ddf);
var x116: u64 = undefined;
var x117: u64 = undefined;
mulxU64(&x116, &x117, x106, 0x581a0db248b0a77a);
var x118: u64 = undefined;
var x119: u64 = undefined;
mulxU64(&x118, &x119, x106, 0xecec196accc52973);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, 0x0, x119, x116);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x117, x114);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x115, x112);
var x126: u64 = undefined;
var x127: u1 = undefined;
addcarryxU64(&x126, &x127, x125, x113, x110);
var x128: u64 = undefined;
var x129: u1 = undefined;
addcarryxU64(&x128, &x129, x127, x111, x108);
const x130 = (@as(u64, x129) + x109);
var x131: u64 = undefined;
var x132: u1 = undefined;
addcarryxU64(&x131, &x132, 0x0, x92, x118);
var x133: u64 = undefined;
var x134: u1 = undefined;
addcarryxU64(&x133, &x134, x132, x94, x120);
var x135: u64 = undefined;
var x136: u1 = undefined;
addcarryxU64(&x135, &x136, x134, x96, x122);
var x137: u64 = undefined;
var x138: u1 = undefined;
addcarryxU64(&x137, &x138, x136, x98, x124);
var x139: u64 = undefined;
var x140: u1 = undefined;
addcarryxU64(&x139, &x140, x138, x100, x126);
var x141: u64 = undefined;
var x142: u1 = undefined;
addcarryxU64(&x141, &x142, x140, x102, x128);
var x143: u64 = undefined;
var x144: u1 = undefined;
addcarryxU64(&x143, &x144, x142, x104, x130);
const x145 = (@as(u64, x144) + @as(u64, x105));
var x146: u64 = undefined;
var x147: u64 = undefined;
mulxU64(&x146, &x147, x2, (arg1[5]));
var x148: u64 = undefined;
var x149: u64 = undefined;
mulxU64(&x148, &x149, x2, (arg1[4]));
var x150: u64 = undefined;
var x151: u64 = undefined;
mulxU64(&x150, &x151, x2, (arg1[3]));
var x152: u64 = undefined;
var x153: u64 = undefined;
mulxU64(&x152, &x153, x2, (arg1[2]));
var x154: u64 = undefined;
var x155: u64 = undefined;
mulxU64(&x154, &x155, x2, (arg1[1]));
var x156: u64 = undefined;
var x157: u64 = undefined;
mulxU64(&x156, &x157, x2, (arg1[0]));
var x158: u64 = undefined;
var x159: u1 = undefined;
addcarryxU64(&x158, &x159, 0x0, x157, x154);
var x160: u64 = undefined;
var x161: u1 = undefined;
addcarryxU64(&x160, &x161, x159, x155, x152);
var x162: u64 = undefined;
var x163: u1 = undefined;
addcarryxU64(&x162, &x163, x161, x153, x150);
var x164: u64 = undefined;
var x165: u1 = undefined;
addcarryxU64(&x164, &x165, x163, x151, x148);
var x166: u64 = undefined;
var x167: u1 = undefined;
addcarryxU64(&x166, &x167, x165, x149, x146);
const x168 = (@as(u64, x167) + x147);
var x169: u64 = undefined;
var x170: u1 = undefined;
addcarryxU64(&x169, &x170, 0x0, x133, x156);
var x171: u64 = undefined;
var x172: u1 = undefined;
addcarryxU64(&x171, &x172, x170, x135, x158);
var x173: u64 = undefined;
var x174: u1 = undefined;
addcarryxU64(&x173, &x174, x172, x137, x160);
var x175: u64 = undefined;
var x176: u1 = undefined;
addcarryxU64(&x175, &x176, x174, x139, x162);
var x177: u64 = undefined;
var x178: u1 = undefined;
addcarryxU64(&x177, &x178, x176, x141, x164);
var x179: u64 = undefined;
var x180: u1 = undefined;
addcarryxU64(&x179, &x180, x178, x143, x166);
var x181: u64 = undefined;
var x182: u1 = undefined;
addcarryxU64(&x181, &x182, x180, x145, x168);
var x183: u64 = undefined;
var x184: u64 = undefined;
mulxU64(&x183, &x184, x169, 0x6ed46089e88fdc45);
var x185: u64 = undefined;
var x186: u64 = undefined;
mulxU64(&x185, &x186, x183, 0xffffffffffffffff);
var x187: u64 = undefined;
var x188: u64 = undefined;
mulxU64(&x187, &x188, x183, 0xffffffffffffffff);
var x189: u64 = undefined;
var x190: u64 = undefined;
mulxU64(&x189, &x190, x183, 0xffffffffffffffff);
var x191: u64 = undefined;
var x192: u64 = undefined;
mulxU64(&x191, &x192, x183, 0xc7634d81f4372ddf);
var x193: u64 = undefined;
var x194: u64 = undefined;
mulxU64(&x193, &x194, x183, 0x581a0db248b0a77a);
var x195: u64 = undefined;
var x196: u64 = undefined;
mulxU64(&x195, &x196, x183, 0xecec196accc52973);
var x197: u64 = undefined;
var x198: u1 = undefined;
addcarryxU64(&x197, &x198, 0x0, x196, x193);
var x199: u64 = undefined;
var x200: u1 = undefined;
addcarryxU64(&x199, &x200, x198, x194, x191);
var x201: u64 = undefined;
var x202: u1 = undefined;
addcarryxU64(&x201, &x202, x200, x192, x189);
var x203: u64 = undefined;
var x204: u1 = undefined;
addcarryxU64(&x203, &x204, x202, x190, x187);
var x205: u64 = undefined;
var x206: u1 = undefined;
addcarryxU64(&x205, &x206, x204, x188, x185);
const x207 = (@as(u64, x206) + x186);
var x208: u64 = undefined;
var x209: u1 = undefined;
addcarryxU64(&x208, &x209, 0x0, x169, x195);
var x210: u64 = undefined;
var x211: u1 = undefined;
addcarryxU64(&x210, &x211, x209, x171, x197);
var x212: u64 = undefined;
var x213: u1 = undefined;
addcarryxU64(&x212, &x213, x211, x173, x199);
var x214: u64 = undefined;
var x215: u1 = undefined;
addcarryxU64(&x214, &x215, x213, x175, x201);
var x216: u64 = undefined;
var x217: u1 = undefined;
addcarryxU64(&x216, &x217, x215, x177, x203);
var x218: u64 = undefined;
var x219: u1 = undefined;
addcarryxU64(&x218, &x219, x217, x179, x205);
var x220: u64 = undefined;
var x221: u1 = undefined;
addcarryxU64(&x220, &x221, x219, x181, x207);
const x222 = (@as(u64, x221) + @as(u64, x182));
var x223: u64 = undefined;
var x224: u64 = undefined;
mulxU64(&x223, &x224, x3, (arg1[5]));
var x225: u64 = undefined;
var x226: u64 = undefined;
mulxU64(&x225, &x226, x3, (arg1[4]));
var x227: u64 = undefined;
var x228: u64 = undefined;
mulxU64(&x227, &x228, x3, (arg1[3]));
var x229: u64 = undefined;
var x230: u64 = undefined;
mulxU64(&x229, &x230, x3, (arg1[2]));
var x231: u64 = undefined;
var x232: u64 = undefined;
mulxU64(&x231, &x232, x3, (arg1[1]));
var x233: u64 = undefined;
var x234: u64 = undefined;
mulxU64(&x233, &x234, x3, (arg1[0]));
var x235: u64 = undefined;
var x236: u1 = undefined;
addcarryxU64(&x235, &x236, 0x0, x234, x231);
var x237: u64 = undefined;
var x238: u1 = undefined;
addcarryxU64(&x237, &x238, x236, x232, x229);
var x239: u64 = undefined;
var x240: u1 = undefined;
addcarryxU64(&x239, &x240, x238, x230, x227);
var x241: u64 = undefined;
var x242: u1 = undefined;
addcarryxU64(&x241, &x242, x240, x228, x225);
var x243: u64 = undefined;
var x244: u1 = undefined;
addcarryxU64(&x243, &x244, x242, x226, x223);
const x245 = (@as(u64, x244) + x224);
var x246: u64 = undefined;
var x247: u1 = undefined;
addcarryxU64(&x246, &x247, 0x0, x210, x233);
var x248: u64 = undefined;
var x249: u1 = undefined;
addcarryxU64(&x248, &x249, x247, x212, x235);
var x250: u64 = undefined;
var x251: u1 = undefined;
addcarryxU64(&x250, &x251, x249, x214, x237);
var x252: u64 = undefined;
var x253: u1 = undefined;
addcarryxU64(&x252, &x253, x251, x216, x239);
var x254: u64 = undefined;
var x255: u1 = undefined;
addcarryxU64(&x254, &x255, x253, x218, x241);
var x256: u64 = undefined;
var x257: u1 = undefined;
addcarryxU64(&x256, &x257, x255, x220, x243);
var x258: u64 = undefined;
var x259: u1 = undefined;
addcarryxU64(&x258, &x259, x257, x222, x245);
var x260: u64 = undefined;
var x261: u64 = undefined;
mulxU64(&x260, &x261, x246, 0x6ed46089e88fdc45);
var x262: u64 = undefined;
var x263: u64 = undefined;
mulxU64(&x262, &x263, x260, 0xffffffffffffffff);
var x264: u64 = undefined;
var x265: u64 = undefined;
mulxU64(&x264, &x265, x260, 0xffffffffffffffff);
var x266: u64 = undefined;
var x267: u64 = undefined;
mulxU64(&x266, &x267, x260, 0xffffffffffffffff);
var x268: u64 = undefined;
var x269: u64 = undefined;
mulxU64(&x268, &x269, x260, 0xc7634d81f4372ddf);
var x270: u64 = undefined;
var x271: u64 = undefined;
mulxU64(&x270, &x271, x260, 0x581a0db248b0a77a);
var x272: u64 = undefined;
var x273: u64 = undefined;
mulxU64(&x272, &x273, x260, 0xecec196accc52973);
var x274: u64 = undefined;
var x275: u1 = undefined;
addcarryxU64(&x274, &x275, 0x0, x273, x270);
var x276: u64 = undefined;
var x277: u1 = undefined;
addcarryxU64(&x276, &x277, x275, x271, x268);
var x278: u64 = undefined;
var x279: u1 = undefined;
addcarryxU64(&x278, &x279, x277, x269, x266);
var x280: u64 = undefined;
var x281: u1 = undefined;
addcarryxU64(&x280, &x281, x279, x267, x264);
var x282: u64 = undefined;
var x283: u1 = undefined;
addcarryxU64(&x282, &x283, x281, x265, x262);
const x284 = (@as(u64, x283) + x263);
var x285: u64 = undefined;
var x286: u1 = undefined;
addcarryxU64(&x285, &x286, 0x0, x246, x272);
var x287: u64 = undefined;
var x288: u1 = undefined;
addcarryxU64(&x287, &x288, x286, x248, x274);
var x289: u64 = undefined;
var x290: u1 = undefined;
addcarryxU64(&x289, &x290, x288, x250, x276);
var x291: u64 = undefined;
var x292: u1 = undefined;
addcarryxU64(&x291, &x292, x290, x252, x278);
var x293: u64 = undefined;
var x294: u1 = undefined;
addcarryxU64(&x293, &x294, x292, x254, x280);
var x295: u64 = undefined;
var x296: u1 = undefined;
addcarryxU64(&x295, &x296, x294, x256, x282);
var x297: u64 = undefined;
var x298: u1 = undefined;
addcarryxU64(&x297, &x298, x296, x258, x284);
const x299 = (@as(u64, x298) + @as(u64, x259));
var x300: u64 = undefined;
var x301: u64 = undefined;
mulxU64(&x300, &x301, x4, (arg1[5]));
var x302: u64 = undefined;
var x303: u64 = undefined;
mulxU64(&x302, &x303, x4, (arg1[4]));
var x304: u64 = undefined;
var x305: u64 = undefined;
mulxU64(&x304, &x305, x4, (arg1[3]));
var x306: u64 = undefined;
var x307: u64 = undefined;
mulxU64(&x306, &x307, x4, (arg1[2]));
var x308: u64 = undefined;
var x309: u64 = undefined;
mulxU64(&x308, &x309, x4, (arg1[1]));
var x310: u64 = undefined;
var x311: u64 = undefined;
mulxU64(&x310, &x311, x4, (arg1[0]));
var x312: u64 = undefined;
var x313: u1 = undefined;
addcarryxU64(&x312, &x313, 0x0, x311, x308);
var x314: u64 = undefined;
var x315: u1 = undefined;
addcarryxU64(&x314, &x315, x313, x309, x306);
var x316: u64 = undefined;
var x317: u1 = undefined;
addcarryxU64(&x316, &x317, x315, x307, x304);
var x318: u64 = undefined;
var x319: u1 = undefined;
addcarryxU64(&x318, &x319, x317, x305, x302);
var x320: u64 = undefined;
var x321: u1 = undefined;
addcarryxU64(&x320, &x321, x319, x303, x300);
const x322 = (@as(u64, x321) + x301);
var x323: u64 = undefined;
var x324: u1 = undefined;
addcarryxU64(&x323, &x324, 0x0, x287, x310);
var x325: u64 = undefined;
var x326: u1 = undefined;
addcarryxU64(&x325, &x326, x324, x289, x312);
var x327: u64 = undefined;
var x328: u1 = undefined;
addcarryxU64(&x327, &x328, x326, x291, x314);
var x329: u64 = undefined;
var x330: u1 = undefined;
addcarryxU64(&x329, &x330, x328, x293, x316);
var x331: u64 = undefined;
var x332: u1 = undefined;
addcarryxU64(&x331, &x332, x330, x295, x318);
var x333: u64 = undefined;
var x334: u1 = undefined;
addcarryxU64(&x333, &x334, x332, x297, x320);
var x335: u64 = undefined;
var x336: u1 = undefined;
addcarryxU64(&x335, &x336, x334, x299, x322);
var x337: u64 = undefined;
var x338: u64 = undefined;
mulxU64(&x337, &x338, x323, 0x6ed46089e88fdc45);
var x339: u64 = undefined;
var x340: u64 = undefined;
mulxU64(&x339, &x340, x337, 0xffffffffffffffff);
var x341: u64 = undefined;
var x342: u64 = undefined;
mulxU64(&x341, &x342, x337, 0xffffffffffffffff);
var x343: u64 = undefined;
var x344: u64 = undefined;
mulxU64(&x343, &x344, x337, 0xffffffffffffffff);
var x345: u64 = undefined;
var x346: u64 = undefined;
mulxU64(&x345, &x346, x337, 0xc7634d81f4372ddf);
var x347: u64 = undefined;
var x348: u64 = undefined;
mulxU64(&x347, &x348, x337, 0x581a0db248b0a77a);
var x349: u64 = undefined;
var x350: u64 = undefined;
mulxU64(&x349, &x350, x337, 0xecec196accc52973);
var x351: u64 = undefined;
var x352: u1 = undefined;
addcarryxU64(&x351, &x352, 0x0, x350, x347);
var x353: u64 = undefined;
var x354: u1 = undefined;
addcarryxU64(&x353, &x354, x352, x348, x345);
var x355: u64 = undefined;
var x356: u1 = undefined;
addcarryxU64(&x355, &x356, x354, x346, x343);
var x357: u64 = undefined;
var x358: u1 = undefined;
addcarryxU64(&x357, &x358, x356, x344, x341);
var x359: u64 = undefined;
var x360: u1 = undefined;
addcarryxU64(&x359, &x360, x358, x342, x339);
const x361 = (@as(u64, x360) + x340);
var x362: u64 = undefined;
var x363: u1 = undefined;
addcarryxU64(&x362, &x363, 0x0, x323, x349);
var x364: u64 = undefined;
var x365: u1 = undefined;
addcarryxU64(&x364, &x365, x363, x325, x351);
var x366: u64 = undefined;
var x367: u1 = undefined;
addcarryxU64(&x366, &x367, x365, x327, x353);
var x368: u64 = undefined;
var x369: u1 = undefined;
addcarryxU64(&x368, &x369, x367, x329, x355);
var x370: u64 = undefined;
var x371: u1 = undefined;
addcarryxU64(&x370, &x371, x369, x331, x357);
var x372: u64 = undefined;
var x373: u1 = undefined;
addcarryxU64(&x372, &x373, x371, x333, x359);
var x374: u64 = undefined;
var x375: u1 = undefined;
addcarryxU64(&x374, &x375, x373, x335, x361);
const x376 = (@as(u64, x375) + @as(u64, x336));
var x377: u64 = undefined;
var x378: u64 = undefined;
mulxU64(&x377, &x378, x5, (arg1[5]));
var x379: u64 = undefined;
var x380: u64 = undefined;
mulxU64(&x379, &x380, x5, (arg1[4]));
var x381: u64 = undefined;
var x382: u64 = undefined;
mulxU64(&x381, &x382, x5, (arg1[3]));
var x383: u64 = undefined;
var x384: u64 = undefined;
mulxU64(&x383, &x384, x5, (arg1[2]));
var x385: u64 = undefined;
var x386: u64 = undefined;
mulxU64(&x385, &x386, x5, (arg1[1]));
var x387: u64 = undefined;
var x388: u64 = undefined;
mulxU64(&x387, &x388, x5, (arg1[0]));
var x389: u64 = undefined;
var x390: u1 = undefined;
addcarryxU64(&x389, &x390, 0x0, x388, x385);
var x391: u64 = undefined;
var x392: u1 = undefined;
addcarryxU64(&x391, &x392, x390, x386, x383);
var x393: u64 = undefined;
var x394: u1 = undefined;
addcarryxU64(&x393, &x394, x392, x384, x381);
var x395: u64 = undefined;
var x396: u1 = undefined;
addcarryxU64(&x395, &x396, x394, x382, x379);
var x397: u64 = undefined;
var x398: u1 = undefined;
addcarryxU64(&x397, &x398, x396, x380, x377);
const x399 = (@as(u64, x398) + x378);
var x400: u64 = undefined;
var x401: u1 = undefined;
addcarryxU64(&x400, &x401, 0x0, x364, x387);
var x402: u64 = undefined;
var x403: u1 = undefined;
addcarryxU64(&x402, &x403, x401, x366, x389);
var x404: u64 = undefined;
var x405: u1 = undefined;
addcarryxU64(&x404, &x405, x403, x368, x391);
var x406: u64 = undefined;
var x407: u1 = undefined;
addcarryxU64(&x406, &x407, x405, x370, x393);
var x408: u64 = undefined;
var x409: u1 = undefined;
addcarryxU64(&x408, &x409, x407, x372, x395);
var x410: u64 = undefined;
var x411: u1 = undefined;
addcarryxU64(&x410, &x411, x409, x374, x397);
var x412: u64 = undefined;
var x413: u1 = undefined;
addcarryxU64(&x412, &x413, x411, x376, x399);
var x414: u64 = undefined;
var x415: u64 = undefined;
mulxU64(&x414, &x415, x400, 0x6ed46089e88fdc45);
var x416: u64 = undefined;
var x417: u64 = undefined;
mulxU64(&x416, &x417, x414, 0xffffffffffffffff);
var x418: u64 = undefined;
var x419: u64 = undefined;
mulxU64(&x418, &x419, x414, 0xffffffffffffffff);
var x420: u64 = undefined;
var x421: u64 = undefined;
mulxU64(&x420, &x421, x414, 0xffffffffffffffff);
var x422: u64 = undefined;
var x423: u64 = undefined;
mulxU64(&x422, &x423, x414, 0xc7634d81f4372ddf);
var x424: u64 = undefined;
var x425: u64 = undefined;
mulxU64(&x424, &x425, x414, 0x581a0db248b0a77a);
var x426: u64 = undefined;
var x427: u64 = undefined;
mulxU64(&x426, &x427, x414, 0xecec196accc52973);
var x428: u64 = undefined;
var x429: u1 = undefined;
addcarryxU64(&x428, &x429, 0x0, x427, x424);
var x430: u64 = undefined;
var x431: u1 = undefined;
addcarryxU64(&x430, &x431, x429, x425, x422);
var x432: u64 = undefined;
var x433: u1 = undefined;
addcarryxU64(&x432, &x433, x431, x423, x420);
var x434: u64 = undefined;
var x435: u1 = undefined;
addcarryxU64(&x434, &x435, x433, x421, x418);
var x436: u64 = undefined;
var x437: u1 = undefined;
addcarryxU64(&x436, &x437, x435, x419, x416);
const x438 = (@as(u64, x437) + x417);
var x439: u64 = undefined;
var x440: u1 = undefined;
addcarryxU64(&x439, &x440, 0x0, x400, x426);
var x441: u64 = undefined;
var x442: u1 = undefined;
addcarryxU64(&x441, &x442, x440, x402, x428);
var x443: u64 = undefined;
var x444: u1 = undefined;
addcarryxU64(&x443, &x444, x442, x404, x430);
var x445: u64 = undefined;
var x446: u1 = undefined;
addcarryxU64(&x445, &x446, x444, x406, x432);
var x447: u64 = undefined;
var x448: u1 = undefined;
addcarryxU64(&x447, &x448, x446, x408, x434);
var x449: u64 = undefined;
var x450: u1 = undefined;
addcarryxU64(&x449, &x450, x448, x410, x436);
var x451: u64 = undefined;
var x452: u1 = undefined;
addcarryxU64(&x451, &x452, x450, x412, x438);
const x453 = (@as(u64, x452) + @as(u64, x413));
var x454: u64 = undefined;
var x455: u1 = undefined;
subborrowxU64(&x454, &x455, 0x0, x441, 0xecec196accc52973);
var x456: u64 = undefined;
var x457: u1 = undefined;
subborrowxU64(&x456, &x457, x455, x443, 0x581a0db248b0a77a);
var x458: u64 = undefined;
var x459: u1 = undefined;
subborrowxU64(&x458, &x459, x457, x445, 0xc7634d81f4372ddf);
var x460: u64 = undefined;
var x461: u1 = undefined;
subborrowxU64(&x460, &x461, x459, x447, 0xffffffffffffffff);
var x462: u64 = undefined;
var x463: u1 = undefined;
subborrowxU64(&x462, &x463, x461, x449, 0xffffffffffffffff);
var x464: u64 = undefined;
var x465: u1 = undefined;
subborrowxU64(&x464, &x465, x463, x451, 0xffffffffffffffff);
var x466: u64 = undefined;
var x467: u1 = undefined;
subborrowxU64(&x466, &x467, x465, x453, 0x0);
var x468: u64 = undefined;
cmovznzU64(&x468, x467, x454, x441);
var x469: u64 = undefined;
cmovznzU64(&x469, x467, x456, x443);
var x470: u64 = undefined;
cmovznzU64(&x470, x467, x458, x445);
var x471: u64 = undefined;
cmovznzU64(&x471, x467, x460, x447);
var x472: u64 = undefined;
cmovznzU64(&x472, x467, x462, x449);
var x473: u64 = undefined;
cmovznzU64(&x473, x467, x464, x451);
out1[0] = x468;
out1[1] = x469;
out1[2] = x470;
out1[3] = x471;
out1[4] = x472;
out1[5] = x473;
}
/// The function add adds two field elements in the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// 0 ≤ eval arg2 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
/// 0 ≤ eval out1 < m
///
pub fn add(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
addcarryxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
var x3: u64 = undefined;
var x4: u1 = undefined;
addcarryxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
var x5: u64 = undefined;
var x6: u1 = undefined;
addcarryxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
var x7: u64 = undefined;
var x8: u1 = undefined;
addcarryxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
var x9: u64 = undefined;
var x10: u1 = undefined;
addcarryxU64(&x9, &x10, x8, (arg1[4]), (arg2[4]));
var x11: u64 = undefined;
var x12: u1 = undefined;
addcarryxU64(&x11, &x12, x10, (arg1[5]), (arg2[5]));
var x13: u64 = undefined;
var x14: u1 = undefined;
subborrowxU64(&x13, &x14, 0x0, x1, 0xecec196accc52973);
var x15: u64 = undefined;
var x16: u1 = undefined;
subborrowxU64(&x15, &x16, x14, x3, 0x581a0db248b0a77a);
var x17: u64 = undefined;
var x18: u1 = undefined;
subborrowxU64(&x17, &x18, x16, x5, 0xc7634d81f4372ddf);
var x19: u64 = undefined;
var x20: u1 = undefined;
subborrowxU64(&x19, &x20, x18, x7, 0xffffffffffffffff);
var x21: u64 = undefined;
var x22: u1 = undefined;
subborrowxU64(&x21, &x22, x20, x9, 0xffffffffffffffff);
var x23: u64 = undefined;
var x24: u1 = undefined;
subborrowxU64(&x23, &x24, x22, x11, 0xffffffffffffffff);
var x25: u64 = undefined;
var x26: u1 = undefined;
subborrowxU64(&x25, &x26, x24, @as(u64, x12), 0x0);
var x27: u64 = undefined;
cmovznzU64(&x27, x26, x13, x1);
var x28: u64 = undefined;
cmovznzU64(&x28, x26, x15, x3);
var x29: u64 = undefined;
cmovznzU64(&x29, x26, x17, x5);
var x30: u64 = undefined;
cmovznzU64(&x30, x26, x19, x7);
var x31: u64 = undefined;
cmovznzU64(&x31, x26, x21, x9);
var x32: u64 = undefined;
cmovznzU64(&x32, x26, x23, x11);
out1[0] = x27;
out1[1] = x28;
out1[2] = x29;
out1[3] = x30;
out1[4] = x31;
out1[5] = x32;
}
/// The function sub subtracts two field elements in the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// 0 ≤ eval arg2 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
/// 0 ≤ eval out1 < m
///
pub fn sub(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement, arg2: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
subborrowxU64(&x1, &x2, 0x0, (arg1[0]), (arg2[0]));
var x3: u64 = undefined;
var x4: u1 = undefined;
subborrowxU64(&x3, &x4, x2, (arg1[1]), (arg2[1]));
var x5: u64 = undefined;
var x6: u1 = undefined;
subborrowxU64(&x5, &x6, x4, (arg1[2]), (arg2[2]));
var x7: u64 = undefined;
var x8: u1 = undefined;
subborrowxU64(&x7, &x8, x6, (arg1[3]), (arg2[3]));
var x9: u64 = undefined;
var x10: u1 = undefined;
subborrowxU64(&x9, &x10, x8, (arg1[4]), (arg2[4]));
var x11: u64 = undefined;
var x12: u1 = undefined;
subborrowxU64(&x11, &x12, x10, (arg1[5]), (arg2[5]));
var x13: u64 = undefined;
cmovznzU64(&x13, x12, 0x0, 0xffffffffffffffff);
var x14: u64 = undefined;
var x15: u1 = undefined;
addcarryxU64(&x14, &x15, 0x0, x1, (x13 & 0xecec196accc52973));
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, x15, x3, (x13 & 0x581a0db248b0a77a));
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, x5, (x13 & 0xc7634d81f4372ddf));
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, x7, x13);
var x22: u64 = undefined;
var x23: u1 = undefined;
addcarryxU64(&x22, &x23, x21, x9, x13);
var x24: u64 = undefined;
var x25: u1 = undefined;
addcarryxU64(&x24, &x25, x23, x11, x13);
out1[0] = x14;
out1[1] = x16;
out1[2] = x18;
out1[3] = x20;
out1[4] = x22;
out1[5] = x24;
}
/// The function opp negates a field element in the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
/// 0 ≤ eval out1 < m
///
pub fn opp(out1: *MontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
subborrowxU64(&x1, &x2, 0x0, 0x0, (arg1[0]));
var x3: u64 = undefined;
var x4: u1 = undefined;
subborrowxU64(&x3, &x4, x2, 0x0, (arg1[1]));
var x5: u64 = undefined;
var x6: u1 = undefined;
subborrowxU64(&x5, &x6, x4, 0x0, (arg1[2]));
var x7: u64 = undefined;
var x8: u1 = undefined;
subborrowxU64(&x7, &x8, x6, 0x0, (arg1[3]));
var x9: u64 = undefined;
var x10: u1 = undefined;
subborrowxU64(&x9, &x10, x8, 0x0, (arg1[4]));
var x11: u64 = undefined;
var x12: u1 = undefined;
subborrowxU64(&x11, &x12, x10, 0x0, (arg1[5]));
var x13: u64 = undefined;
cmovznzU64(&x13, x12, 0x0, 0xffffffffffffffff);
var x14: u64 = undefined;
var x15: u1 = undefined;
addcarryxU64(&x14, &x15, 0x0, x1, (x13 & 0xecec196accc52973));
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, x15, x3, (x13 & 0x581a0db248b0a77a));
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, x5, (x13 & 0xc7634d81f4372ddf));
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, x7, x13);
var x22: u64 = undefined;
var x23: u1 = undefined;
addcarryxU64(&x22, &x23, x21, x9, x13);
var x24: u64 = undefined;
var x25: u1 = undefined;
addcarryxU64(&x24, &x25, x23, x11, x13);
out1[0] = x14;
out1[1] = x16;
out1[2] = x18;
out1[3] = x20;
out1[4] = x22;
out1[5] = x24;
}
/// The function fromMontgomery translates a field element out of the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m
/// 0 ≤ eval out1 < m
///
pub fn fromMontgomery(out1: *NonMontgomeryDomainFieldElement, arg1: MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (arg1[0]);
var x2: u64 = undefined;
var x3: u64 = undefined;
mulxU64(&x2, &x3, x1, 0x6ed46089e88fdc45);
var x4: u64 = undefined;
var x5: u64 = undefined;
mulxU64(&x4, &x5, x2, 0xffffffffffffffff);
var x6: u64 = undefined;
var x7: u64 = undefined;
mulxU64(&x6, &x7, x2, 0xffffffffffffffff);
var x8: u64 = undefined;
var x9: u64 = undefined;
mulxU64(&x8, &x9, x2, 0xffffffffffffffff);
var x10: u64 = undefined;
var x11: u64 = undefined;
mulxU64(&x10, &x11, x2, 0xc7634d81f4372ddf);
var x12: u64 = undefined;
var x13: u64 = undefined;
mulxU64(&x12, &x13, x2, 0x581a0db248b0a77a);
var x14: u64 = undefined;
var x15: u64 = undefined;
mulxU64(&x14, &x15, x2, 0xecec196accc52973);
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, 0x0, x15, x12);
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, x13, x10);
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, x11, x8);
var x22: u64 = undefined;
var x23: u1 = undefined;
addcarryxU64(&x22, &x23, x21, x9, x6);
var x24: u64 = undefined;
var x25: u1 = undefined;
addcarryxU64(&x24, &x25, x23, x7, x4);
var x26: u64 = undefined;
var x27: u1 = undefined;
addcarryxU64(&x26, &x27, 0x0, x1, x14);
var x28: u64 = undefined;
var x29: u1 = undefined;
addcarryxU64(&x28, &x29, x27, 0x0, x16);
var x30: u64 = undefined;
var x31: u1 = undefined;
addcarryxU64(&x30, &x31, x29, 0x0, x18);
var x32: u64 = undefined;
var x33: u1 = undefined;
addcarryxU64(&x32, &x33, x31, 0x0, x20);
var x34: u64 = undefined;
var x35: u1 = undefined;
addcarryxU64(&x34, &x35, x33, 0x0, x22);
var x36: u64 = undefined;
var x37: u1 = undefined;
addcarryxU64(&x36, &x37, x35, 0x0, x24);
var x38: u64 = undefined;
var x39: u1 = undefined;
addcarryxU64(&x38, &x39, x37, 0x0, (@as(u64, x25) + x5));
var x40: u64 = undefined;
var x41: u1 = undefined;
addcarryxU64(&x40, &x41, 0x0, x28, (arg1[1]));
var x42: u64 = undefined;
var x43: u1 = undefined;
addcarryxU64(&x42, &x43, x41, x30, 0x0);
var x44: u64 = undefined;
var x45: u1 = undefined;
addcarryxU64(&x44, &x45, x43, x32, 0x0);
var x46: u64 = undefined;
var x47: u1 = undefined;
addcarryxU64(&x46, &x47, x45, x34, 0x0);
var x48: u64 = undefined;
var x49: u1 = undefined;
addcarryxU64(&x48, &x49, x47, x36, 0x0);
var x50: u64 = undefined;
var x51: u1 = undefined;
addcarryxU64(&x50, &x51, x49, x38, 0x0);
var x52: u64 = undefined;
var x53: u64 = undefined;
mulxU64(&x52, &x53, x40, 0x6ed46089e88fdc45);
var x54: u64 = undefined;
var x55: u64 = undefined;
mulxU64(&x54, &x55, x52, 0xffffffffffffffff);
var x56: u64 = undefined;
var x57: u64 = undefined;
mulxU64(&x56, &x57, x52, 0xffffffffffffffff);
var x58: u64 = undefined;
var x59: u64 = undefined;
mulxU64(&x58, &x59, x52, 0xffffffffffffffff);
var x60: u64 = undefined;
var x61: u64 = undefined;
mulxU64(&x60, &x61, x52, 0xc7634d81f4372ddf);
var x62: u64 = undefined;
var x63: u64 = undefined;
mulxU64(&x62, &x63, x52, 0x581a0db248b0a77a);
var x64: u64 = undefined;
var x65: u64 = undefined;
mulxU64(&x64, &x65, x52, 0xecec196accc52973);
var x66: u64 = undefined;
var x67: u1 = undefined;
addcarryxU64(&x66, &x67, 0x0, x65, x62);
var x68: u64 = undefined;
var x69: u1 = undefined;
addcarryxU64(&x68, &x69, x67, x63, x60);
var x70: u64 = undefined;
var x71: u1 = undefined;
addcarryxU64(&x70, &x71, x69, x61, x58);
var x72: u64 = undefined;
var x73: u1 = undefined;
addcarryxU64(&x72, &x73, x71, x59, x56);
var x74: u64 = undefined;
var x75: u1 = undefined;
addcarryxU64(&x74, &x75, x73, x57, x54);
var x76: u64 = undefined;
var x77: u1 = undefined;
addcarryxU64(&x76, &x77, 0x0, x40, x64);
var x78: u64 = undefined;
var x79: u1 = undefined;
addcarryxU64(&x78, &x79, x77, x42, x66);
var x80: u64 = undefined;
var x81: u1 = undefined;
addcarryxU64(&x80, &x81, x79, x44, x68);
var x82: u64 = undefined;
var x83: u1 = undefined;
addcarryxU64(&x82, &x83, x81, x46, x70);
var x84: u64 = undefined;
var x85: u1 = undefined;
addcarryxU64(&x84, &x85, x83, x48, x72);
var x86: u64 = undefined;
var x87: u1 = undefined;
addcarryxU64(&x86, &x87, x85, x50, x74);
var x88: u64 = undefined;
var x89: u1 = undefined;
addcarryxU64(&x88, &x89, x87, (@as(u64, x51) + @as(u64, x39)), (@as(u64, x75) + x55));
var x90: u64 = undefined;
var x91: u1 = undefined;
addcarryxU64(&x90, &x91, 0x0, x78, (arg1[2]));
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, x91, x80, 0x0);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x82, 0x0);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x84, 0x0);
var x98: u64 = undefined;
var x99: u1 = undefined;
addcarryxU64(&x98, &x99, x97, x86, 0x0);
var x100: u64 = undefined;
var x101: u1 = undefined;
addcarryxU64(&x100, &x101, x99, x88, 0x0);
var x102: u64 = undefined;
var x103: u64 = undefined;
mulxU64(&x102, &x103, x90, 0x6ed46089e88fdc45);
var x104: u64 = undefined;
var x105: u64 = undefined;
mulxU64(&x104, &x105, x102, 0xffffffffffffffff);
var x106: u64 = undefined;
var x107: u64 = undefined;
mulxU64(&x106, &x107, x102, 0xffffffffffffffff);
var x108: u64 = undefined;
var x109: u64 = undefined;
mulxU64(&x108, &x109, x102, 0xffffffffffffffff);
var x110: u64 = undefined;
var x111: u64 = undefined;
mulxU64(&x110, &x111, x102, 0xc7634d81f4372ddf);
var x112: u64 = undefined;
var x113: u64 = undefined;
mulxU64(&x112, &x113, x102, 0x581a0db248b0a77a);
var x114: u64 = undefined;
var x115: u64 = undefined;
mulxU64(&x114, &x115, x102, 0xecec196accc52973);
var x116: u64 = undefined;
var x117: u1 = undefined;
addcarryxU64(&x116, &x117, 0x0, x115, x112);
var x118: u64 = undefined;
var x119: u1 = undefined;
addcarryxU64(&x118, &x119, x117, x113, x110);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, x119, x111, x108);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x109, x106);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x107, x104);
var x126: u64 = undefined;
var x127: u1 = undefined;
addcarryxU64(&x126, &x127, 0x0, x90, x114);
var x128: u64 = undefined;
var x129: u1 = undefined;
addcarryxU64(&x128, &x129, x127, x92, x116);
var x130: u64 = undefined;
var x131: u1 = undefined;
addcarryxU64(&x130, &x131, x129, x94, x118);
var x132: u64 = undefined;
var x133: u1 = undefined;
addcarryxU64(&x132, &x133, x131, x96, x120);
var x134: u64 = undefined;
var x135: u1 = undefined;
addcarryxU64(&x134, &x135, x133, x98, x122);
var x136: u64 = undefined;
var x137: u1 = undefined;
addcarryxU64(&x136, &x137, x135, x100, x124);
var x138: u64 = undefined;
var x139: u1 = undefined;
addcarryxU64(&x138, &x139, x137, (@as(u64, x101) + @as(u64, x89)), (@as(u64, x125) + x105));
var x140: u64 = undefined;
var x141: u1 = undefined;
addcarryxU64(&x140, &x141, 0x0, x128, (arg1[3]));
var x142: u64 = undefined;
var x143: u1 = undefined;
addcarryxU64(&x142, &x143, x141, x130, 0x0);
var x144: u64 = undefined;
var x145: u1 = undefined;
addcarryxU64(&x144, &x145, x143, x132, 0x0);
var x146: u64 = undefined;
var x147: u1 = undefined;
addcarryxU64(&x146, &x147, x145, x134, 0x0);
var x148: u64 = undefined;
var x149: u1 = undefined;
addcarryxU64(&x148, &x149, x147, x136, 0x0);
var x150: u64 = undefined;
var x151: u1 = undefined;
addcarryxU64(&x150, &x151, x149, x138, 0x0);
var x152: u64 = undefined;
var x153: u64 = undefined;
mulxU64(&x152, &x153, x140, 0x6ed46089e88fdc45);
var x154: u64 = undefined;
var x155: u64 = undefined;
mulxU64(&x154, &x155, x152, 0xffffffffffffffff);
var x156: u64 = undefined;
var x157: u64 = undefined;
mulxU64(&x156, &x157, x152, 0xffffffffffffffff);
var x158: u64 = undefined;
var x159: u64 = undefined;
mulxU64(&x158, &x159, x152, 0xffffffffffffffff);
var x160: u64 = undefined;
var x161: u64 = undefined;
mulxU64(&x160, &x161, x152, 0xc7634d81f4372ddf);
var x162: u64 = undefined;
var x163: u64 = undefined;
mulxU64(&x162, &x163, x152, 0x581a0db248b0a77a);
var x164: u64 = undefined;
var x165: u64 = undefined;
mulxU64(&x164, &x165, x152, 0xecec196accc52973);
var x166: u64 = undefined;
var x167: u1 = undefined;
addcarryxU64(&x166, &x167, 0x0, x165, x162);
var x168: u64 = undefined;
var x169: u1 = undefined;
addcarryxU64(&x168, &x169, x167, x163, x160);
var x170: u64 = undefined;
var x171: u1 = undefined;
addcarryxU64(&x170, &x171, x169, x161, x158);
var x172: u64 = undefined;
var x173: u1 = undefined;
addcarryxU64(&x172, &x173, x171, x159, x156);
var x174: u64 = undefined;
var x175: u1 = undefined;
addcarryxU64(&x174, &x175, x173, x157, x154);
var x176: u64 = undefined;
var x177: u1 = undefined;
addcarryxU64(&x176, &x177, 0x0, x140, x164);
var x178: u64 = undefined;
var x179: u1 = undefined;
addcarryxU64(&x178, &x179, x177, x142, x166);
var x180: u64 = undefined;
var x181: u1 = undefined;
addcarryxU64(&x180, &x181, x179, x144, x168);
var x182: u64 = undefined;
var x183: u1 = undefined;
addcarryxU64(&x182, &x183, x181, x146, x170);
var x184: u64 = undefined;
var x185: u1 = undefined;
addcarryxU64(&x184, &x185, x183, x148, x172);
var x186: u64 = undefined;
var x187: u1 = undefined;
addcarryxU64(&x186, &x187, x185, x150, x174);
var x188: u64 = undefined;
var x189: u1 = undefined;
addcarryxU64(&x188, &x189, x187, (@as(u64, x151) + @as(u64, x139)), (@as(u64, x175) + x155));
var x190: u64 = undefined;
var x191: u1 = undefined;
addcarryxU64(&x190, &x191, 0x0, x178, (arg1[4]));
var x192: u64 = undefined;
var x193: u1 = undefined;
addcarryxU64(&x192, &x193, x191, x180, 0x0);
var x194: u64 = undefined;
var x195: u1 = undefined;
addcarryxU64(&x194, &x195, x193, x182, 0x0);
var x196: u64 = undefined;
var x197: u1 = undefined;
addcarryxU64(&x196, &x197, x195, x184, 0x0);
var x198: u64 = undefined;
var x199: u1 = undefined;
addcarryxU64(&x198, &x199, x197, x186, 0x0);
var x200: u64 = undefined;
var x201: u1 = undefined;
addcarryxU64(&x200, &x201, x199, x188, 0x0);
var x202: u64 = undefined;
var x203: u64 = undefined;
mulxU64(&x202, &x203, x190, 0x6ed46089e88fdc45);
var x204: u64 = undefined;
var x205: u64 = undefined;
mulxU64(&x204, &x205, x202, 0xffffffffffffffff);
var x206: u64 = undefined;
var x207: u64 = undefined;
mulxU64(&x206, &x207, x202, 0xffffffffffffffff);
var x208: u64 = undefined;
var x209: u64 = undefined;
mulxU64(&x208, &x209, x202, 0xffffffffffffffff);
var x210: u64 = undefined;
var x211: u64 = undefined;
mulxU64(&x210, &x211, x202, 0xc7634d81f4372ddf);
var x212: u64 = undefined;
var x213: u64 = undefined;
mulxU64(&x212, &x213, x202, 0x581a0db248b0a77a);
var x214: u64 = undefined;
var x215: u64 = undefined;
mulxU64(&x214, &x215, x202, 0xecec196accc52973);
var x216: u64 = undefined;
var x217: u1 = undefined;
addcarryxU64(&x216, &x217, 0x0, x215, x212);
var x218: u64 = undefined;
var x219: u1 = undefined;
addcarryxU64(&x218, &x219, x217, x213, x210);
var x220: u64 = undefined;
var x221: u1 = undefined;
addcarryxU64(&x220, &x221, x219, x211, x208);
var x222: u64 = undefined;
var x223: u1 = undefined;
addcarryxU64(&x222, &x223, x221, x209, x206);
var x224: u64 = undefined;
var x225: u1 = undefined;
addcarryxU64(&x224, &x225, x223, x207, x204);
var x226: u64 = undefined;
var x227: u1 = undefined;
addcarryxU64(&x226, &x227, 0x0, x190, x214);
var x228: u64 = undefined;
var x229: u1 = undefined;
addcarryxU64(&x228, &x229, x227, x192, x216);
var x230: u64 = undefined;
var x231: u1 = undefined;
addcarryxU64(&x230, &x231, x229, x194, x218);
var x232: u64 = undefined;
var x233: u1 = undefined;
addcarryxU64(&x232, &x233, x231, x196, x220);
var x234: u64 = undefined;
var x235: u1 = undefined;
addcarryxU64(&x234, &x235, x233, x198, x222);
var x236: u64 = undefined;
var x237: u1 = undefined;
addcarryxU64(&x236, &x237, x235, x200, x224);
var x238: u64 = undefined;
var x239: u1 = undefined;
addcarryxU64(&x238, &x239, x237, (@as(u64, x201) + @as(u64, x189)), (@as(u64, x225) + x205));
var x240: u64 = undefined;
var x241: u1 = undefined;
addcarryxU64(&x240, &x241, 0x0, x228, (arg1[5]));
var x242: u64 = undefined;
var x243: u1 = undefined;
addcarryxU64(&x242, &x243, x241, x230, 0x0);
var x244: u64 = undefined;
var x245: u1 = undefined;
addcarryxU64(&x244, &x245, x243, x232, 0x0);
var x246: u64 = undefined;
var x247: u1 = undefined;
addcarryxU64(&x246, &x247, x245, x234, 0x0);
var x248: u64 = undefined;
var x249: u1 = undefined;
addcarryxU64(&x248, &x249, x247, x236, 0x0);
var x250: u64 = undefined;
var x251: u1 = undefined;
addcarryxU64(&x250, &x251, x249, x238, 0x0);
var x252: u64 = undefined;
var x253: u64 = undefined;
mulxU64(&x252, &x253, x240, 0x6ed46089e88fdc45);
var x254: u64 = undefined;
var x255: u64 = undefined;
mulxU64(&x254, &x255, x252, 0xffffffffffffffff);
var x256: u64 = undefined;
var x257: u64 = undefined;
mulxU64(&x256, &x257, x252, 0xffffffffffffffff);
var x258: u64 = undefined;
var x259: u64 = undefined;
mulxU64(&x258, &x259, x252, 0xffffffffffffffff);
var x260: u64 = undefined;
var x261: u64 = undefined;
mulxU64(&x260, &x261, x252, 0xc7634d81f4372ddf);
var x262: u64 = undefined;
var x263: u64 = undefined;
mulxU64(&x262, &x263, x252, 0x581a0db248b0a77a);
var x264: u64 = undefined;
var x265: u64 = undefined;
mulxU64(&x264, &x265, x252, 0xecec196accc52973);
var x266: u64 = undefined;
var x267: u1 = undefined;
addcarryxU64(&x266, &x267, 0x0, x265, x262);
var x268: u64 = undefined;
var x269: u1 = undefined;
addcarryxU64(&x268, &x269, x267, x263, x260);
var x270: u64 = undefined;
var x271: u1 = undefined;
addcarryxU64(&x270, &x271, x269, x261, x258);
var x272: u64 = undefined;
var x273: u1 = undefined;
addcarryxU64(&x272, &x273, x271, x259, x256);
var x274: u64 = undefined;
var x275: u1 = undefined;
addcarryxU64(&x274, &x275, x273, x257, x254);
var x276: u64 = undefined;
var x277: u1 = undefined;
addcarryxU64(&x276, &x277, 0x0, x240, x264);
var x278: u64 = undefined;
var x279: u1 = undefined;
addcarryxU64(&x278, &x279, x277, x242, x266);
var x280: u64 = undefined;
var x281: u1 = undefined;
addcarryxU64(&x280, &x281, x279, x244, x268);
var x282: u64 = undefined;
var x283: u1 = undefined;
addcarryxU64(&x282, &x283, x281, x246, x270);
var x284: u64 = undefined;
var x285: u1 = undefined;
addcarryxU64(&x284, &x285, x283, x248, x272);
var x286: u64 = undefined;
var x287: u1 = undefined;
addcarryxU64(&x286, &x287, x285, x250, x274);
var x288: u64 = undefined;
var x289: u1 = undefined;
addcarryxU64(&x288, &x289, x287, (@as(u64, x251) + @as(u64, x239)), (@as(u64, x275) + x255));
var x290: u64 = undefined;
var x291: u1 = undefined;
subborrowxU64(&x290, &x291, 0x0, x278, 0xecec196accc52973);
var x292: u64 = undefined;
var x293: u1 = undefined;
subborrowxU64(&x292, &x293, x291, x280, 0x581a0db248b0a77a);
var x294: u64 = undefined;
var x295: u1 = undefined;
subborrowxU64(&x294, &x295, x293, x282, 0xc7634d81f4372ddf);
var x296: u64 = undefined;
var x297: u1 = undefined;
subborrowxU64(&x296, &x297, x295, x284, 0xffffffffffffffff);
var x298: u64 = undefined;
var x299: u1 = undefined;
subborrowxU64(&x298, &x299, x297, x286, 0xffffffffffffffff);
var x300: u64 = undefined;
var x301: u1 = undefined;
subborrowxU64(&x300, &x301, x299, x288, 0xffffffffffffffff);
var x302: u64 = undefined;
var x303: u1 = undefined;
subborrowxU64(&x302, &x303, x301, @as(u64, x289), 0x0);
var x304: u64 = undefined;
cmovznzU64(&x304, x303, x290, x278);
var x305: u64 = undefined;
cmovznzU64(&x305, x303, x292, x280);
var x306: u64 = undefined;
cmovznzU64(&x306, x303, x294, x282);
var x307: u64 = undefined;
cmovznzU64(&x307, x303, x296, x284);
var x308: u64 = undefined;
cmovznzU64(&x308, x303, x298, x286);
var x309: u64 = undefined;
cmovznzU64(&x309, x303, x300, x288);
out1[0] = x304;
out1[1] = x305;
out1[2] = x306;
out1[3] = x307;
out1[4] = x308;
out1[5] = x309;
}
/// The function toMontgomery translates a field element into the Montgomery domain.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// eval (from_montgomery out1) mod m = eval arg1 mod m
/// 0 ≤ eval out1 < m
///
pub fn toMontgomery(out1: *MontgomeryDomainFieldElement, arg1: NonMontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (arg1[1]);
const x2 = (arg1[2]);
const x3 = (arg1[3]);
const x4 = (arg1[4]);
const x5 = (arg1[5]);
const x6 = (arg1[0]);
var x7: u64 = undefined;
var x8: u64 = undefined;
mulxU64(&x7, &x8, x6, 0xc84ee012b39bf21);
var x9: u64 = undefined;
var x10: u64 = undefined;
mulxU64(&x9, &x10, x6, 0x3fb05b7a28266895);
var x11: u64 = undefined;
var x12: u64 = undefined;
mulxU64(&x11, &x12, x6, 0xd40d49174aab1cc5);
var x13: u64 = undefined;
var x14: u64 = undefined;
mulxU64(&x13, &x14, x6, 0xbc3e483afcb82947);
var x15: u64 = undefined;
var x16: u64 = undefined;
mulxU64(&x15, &x16, x6, 0xff3d81e5df1aa419);
var x17: u64 = undefined;
var x18: u64 = undefined;
mulxU64(&x17, &x18, x6, 0x2d319b2419b409a9);
var x19: u64 = undefined;
var x20: u1 = undefined;
addcarryxU64(&x19, &x20, 0x0, x18, x15);
var x21: u64 = undefined;
var x22: u1 = undefined;
addcarryxU64(&x21, &x22, x20, x16, x13);
var x23: u64 = undefined;
var x24: u1 = undefined;
addcarryxU64(&x23, &x24, x22, x14, x11);
var x25: u64 = undefined;
var x26: u1 = undefined;
addcarryxU64(&x25, &x26, x24, x12, x9);
var x27: u64 = undefined;
var x28: u1 = undefined;
addcarryxU64(&x27, &x28, x26, x10, x7);
var x29: u64 = undefined;
var x30: u64 = undefined;
mulxU64(&x29, &x30, x17, 0x6ed46089e88fdc45);
var x31: u64 = undefined;
var x32: u64 = undefined;
mulxU64(&x31, &x32, x29, 0xffffffffffffffff);
var x33: u64 = undefined;
var x34: u64 = undefined;
mulxU64(&x33, &x34, x29, 0xffffffffffffffff);
var x35: u64 = undefined;
var x36: u64 = undefined;
mulxU64(&x35, &x36, x29, 0xffffffffffffffff);
var x37: u64 = undefined;
var x38: u64 = undefined;
mulxU64(&x37, &x38, x29, 0xc7634d81f4372ddf);
var x39: u64 = undefined;
var x40: u64 = undefined;
mulxU64(&x39, &x40, x29, 0x581a0db248b0a77a);
var x41: u64 = undefined;
var x42: u64 = undefined;
mulxU64(&x41, &x42, x29, 0xecec196accc52973);
var x43: u64 = undefined;
var x44: u1 = undefined;
addcarryxU64(&x43, &x44, 0x0, x42, x39);
var x45: u64 = undefined;
var x46: u1 = undefined;
addcarryxU64(&x45, &x46, x44, x40, x37);
var x47: u64 = undefined;
var x48: u1 = undefined;
addcarryxU64(&x47, &x48, x46, x38, x35);
var x49: u64 = undefined;
var x50: u1 = undefined;
addcarryxU64(&x49, &x50, x48, x36, x33);
var x51: u64 = undefined;
var x52: u1 = undefined;
addcarryxU64(&x51, &x52, x50, x34, x31);
var x53: u64 = undefined;
var x54: u1 = undefined;
addcarryxU64(&x53, &x54, 0x0, x17, x41);
var x55: u64 = undefined;
var x56: u1 = undefined;
addcarryxU64(&x55, &x56, x54, x19, x43);
var x57: u64 = undefined;
var x58: u1 = undefined;
addcarryxU64(&x57, &x58, x56, x21, x45);
var x59: u64 = undefined;
var x60: u1 = undefined;
addcarryxU64(&x59, &x60, x58, x23, x47);
var x61: u64 = undefined;
var x62: u1 = undefined;
addcarryxU64(&x61, &x62, x60, x25, x49);
var x63: u64 = undefined;
var x64: u1 = undefined;
addcarryxU64(&x63, &x64, x62, x27, x51);
var x65: u64 = undefined;
var x66: u1 = undefined;
addcarryxU64(&x65, &x66, x64, (@as(u64, x28) + x8), (@as(u64, x52) + x32));
var x67: u64 = undefined;
var x68: u64 = undefined;
mulxU64(&x67, &x68, x1, 0xc84ee012b39bf21);
var x69: u64 = undefined;
var x70: u64 = undefined;
mulxU64(&x69, &x70, x1, 0x3fb05b7a28266895);
var x71: u64 = undefined;
var x72: u64 = undefined;
mulxU64(&x71, &x72, x1, 0xd40d49174aab1cc5);
var x73: u64 = undefined;
var x74: u64 = undefined;
mulxU64(&x73, &x74, x1, 0xbc3e483afcb82947);
var x75: u64 = undefined;
var x76: u64 = undefined;
mulxU64(&x75, &x76, x1, 0xff3d81e5df1aa419);
var x77: u64 = undefined;
var x78: u64 = undefined;
mulxU64(&x77, &x78, x1, 0x2d319b2419b409a9);
var x79: u64 = undefined;
var x80: u1 = undefined;
addcarryxU64(&x79, &x80, 0x0, x78, x75);
var x81: u64 = undefined;
var x82: u1 = undefined;
addcarryxU64(&x81, &x82, x80, x76, x73);
var x83: u64 = undefined;
var x84: u1 = undefined;
addcarryxU64(&x83, &x84, x82, x74, x71);
var x85: u64 = undefined;
var x86: u1 = undefined;
addcarryxU64(&x85, &x86, x84, x72, x69);
var x87: u64 = undefined;
var x88: u1 = undefined;
addcarryxU64(&x87, &x88, x86, x70, x67);
var x89: u64 = undefined;
var x90: u1 = undefined;
addcarryxU64(&x89, &x90, 0x0, x55, x77);
var x91: u64 = undefined;
var x92: u1 = undefined;
addcarryxU64(&x91, &x92, x90, x57, x79);
var x93: u64 = undefined;
var x94: u1 = undefined;
addcarryxU64(&x93, &x94, x92, x59, x81);
var x95: u64 = undefined;
var x96: u1 = undefined;
addcarryxU64(&x95, &x96, x94, x61, x83);
var x97: u64 = undefined;
var x98: u1 = undefined;
addcarryxU64(&x97, &x98, x96, x63, x85);
var x99: u64 = undefined;
var x100: u1 = undefined;
addcarryxU64(&x99, &x100, x98, x65, x87);
var x101: u64 = undefined;
var x102: u64 = undefined;
mulxU64(&x101, &x102, x89, 0x6ed46089e88fdc45);
var x103: u64 = undefined;
var x104: u64 = undefined;
mulxU64(&x103, &x104, x101, 0xffffffffffffffff);
var x105: u64 = undefined;
var x106: u64 = undefined;
mulxU64(&x105, &x106, x101, 0xffffffffffffffff);
var x107: u64 = undefined;
var x108: u64 = undefined;
mulxU64(&x107, &x108, x101, 0xffffffffffffffff);
var x109: u64 = undefined;
var x110: u64 = undefined;
mulxU64(&x109, &x110, x101, 0xc7634d81f4372ddf);
var x111: u64 = undefined;
var x112: u64 = undefined;
mulxU64(&x111, &x112, x101, 0x581a0db248b0a77a);
var x113: u64 = undefined;
var x114: u64 = undefined;
mulxU64(&x113, &x114, x101, 0xecec196accc52973);
var x115: u64 = undefined;
var x116: u1 = undefined;
addcarryxU64(&x115, &x116, 0x0, x114, x111);
var x117: u64 = undefined;
var x118: u1 = undefined;
addcarryxU64(&x117, &x118, x116, x112, x109);
var x119: u64 = undefined;
var x120: u1 = undefined;
addcarryxU64(&x119, &x120, x118, x110, x107);
var x121: u64 = undefined;
var x122: u1 = undefined;
addcarryxU64(&x121, &x122, x120, x108, x105);
var x123: u64 = undefined;
var x124: u1 = undefined;
addcarryxU64(&x123, &x124, x122, x106, x103);
var x125: u64 = undefined;
var x126: u1 = undefined;
addcarryxU64(&x125, &x126, 0x0, x89, x113);
var x127: u64 = undefined;
var x128: u1 = undefined;
addcarryxU64(&x127, &x128, x126, x91, x115);
var x129: u64 = undefined;
var x130: u1 = undefined;
addcarryxU64(&x129, &x130, x128, x93, x117);
var x131: u64 = undefined;
var x132: u1 = undefined;
addcarryxU64(&x131, &x132, x130, x95, x119);
var x133: u64 = undefined;
var x134: u1 = undefined;
addcarryxU64(&x133, &x134, x132, x97, x121);
var x135: u64 = undefined;
var x136: u1 = undefined;
addcarryxU64(&x135, &x136, x134, x99, x123);
var x137: u64 = undefined;
var x138: u1 = undefined;
addcarryxU64(&x137, &x138, x136, ((@as(u64, x100) + @as(u64, x66)) + (@as(u64, x88) + x68)), (@as(u64, x124) + x104));
var x139: u64 = undefined;
var x140: u64 = undefined;
mulxU64(&x139, &x140, x2, 0xc84ee012b39bf21);
var x141: u64 = undefined;
var x142: u64 = undefined;
mulxU64(&x141, &x142, x2, 0x3fb05b7a28266895);
var x143: u64 = undefined;
var x144: u64 = undefined;
mulxU64(&x143, &x144, x2, 0xd40d49174aab1cc5);
var x145: u64 = undefined;
var x146: u64 = undefined;
mulxU64(&x145, &x146, x2, 0xbc3e483afcb82947);
var x147: u64 = undefined;
var x148: u64 = undefined;
mulxU64(&x147, &x148, x2, 0xff3d81e5df1aa419);
var x149: u64 = undefined;
var x150: u64 = undefined;
mulxU64(&x149, &x150, x2, 0x2d319b2419b409a9);
var x151: u64 = undefined;
var x152: u1 = undefined;
addcarryxU64(&x151, &x152, 0x0, x150, x147);
var x153: u64 = undefined;
var x154: u1 = undefined;
addcarryxU64(&x153, &x154, x152, x148, x145);
var x155: u64 = undefined;
var x156: u1 = undefined;
addcarryxU64(&x155, &x156, x154, x146, x143);
var x157: u64 = undefined;
var x158: u1 = undefined;
addcarryxU64(&x157, &x158, x156, x144, x141);
var x159: u64 = undefined;
var x160: u1 = undefined;
addcarryxU64(&x159, &x160, x158, x142, x139);
var x161: u64 = undefined;
var x162: u1 = undefined;
addcarryxU64(&x161, &x162, 0x0, x127, x149);
var x163: u64 = undefined;
var x164: u1 = undefined;
addcarryxU64(&x163, &x164, x162, x129, x151);
var x165: u64 = undefined;
var x166: u1 = undefined;
addcarryxU64(&x165, &x166, x164, x131, x153);
var x167: u64 = undefined;
var x168: u1 = undefined;
addcarryxU64(&x167, &x168, x166, x133, x155);
var x169: u64 = undefined;
var x170: u1 = undefined;
addcarryxU64(&x169, &x170, x168, x135, x157);
var x171: u64 = undefined;
var x172: u1 = undefined;
addcarryxU64(&x171, &x172, x170, x137, x159);
var x173: u64 = undefined;
var x174: u64 = undefined;
mulxU64(&x173, &x174, x161, 0x6ed46089e88fdc45);
var x175: u64 = undefined;
var x176: u64 = undefined;
mulxU64(&x175, &x176, x173, 0xffffffffffffffff);
var x177: u64 = undefined;
var x178: u64 = undefined;
mulxU64(&x177, &x178, x173, 0xffffffffffffffff);
var x179: u64 = undefined;
var x180: u64 = undefined;
mulxU64(&x179, &x180, x173, 0xffffffffffffffff);
var x181: u64 = undefined;
var x182: u64 = undefined;
mulxU64(&x181, &x182, x173, 0xc7634d81f4372ddf);
var x183: u64 = undefined;
var x184: u64 = undefined;
mulxU64(&x183, &x184, x173, 0x581a0db248b0a77a);
var x185: u64 = undefined;
var x186: u64 = undefined;
mulxU64(&x185, &x186, x173, 0xecec196accc52973);
var x187: u64 = undefined;
var x188: u1 = undefined;
addcarryxU64(&x187, &x188, 0x0, x186, x183);
var x189: u64 = undefined;
var x190: u1 = undefined;
addcarryxU64(&x189, &x190, x188, x184, x181);
var x191: u64 = undefined;
var x192: u1 = undefined;
addcarryxU64(&x191, &x192, x190, x182, x179);
var x193: u64 = undefined;
var x194: u1 = undefined;
addcarryxU64(&x193, &x194, x192, x180, x177);
var x195: u64 = undefined;
var x196: u1 = undefined;
addcarryxU64(&x195, &x196, x194, x178, x175);
var x197: u64 = undefined;
var x198: u1 = undefined;
addcarryxU64(&x197, &x198, 0x0, x161, x185);
var x199: u64 = undefined;
var x200: u1 = undefined;
addcarryxU64(&x199, &x200, x198, x163, x187);
var x201: u64 = undefined;
var x202: u1 = undefined;
addcarryxU64(&x201, &x202, x200, x165, x189);
var x203: u64 = undefined;
var x204: u1 = undefined;
addcarryxU64(&x203, &x204, x202, x167, x191);
var x205: u64 = undefined;
var x206: u1 = undefined;
addcarryxU64(&x205, &x206, x204, x169, x193);
var x207: u64 = undefined;
var x208: u1 = undefined;
addcarryxU64(&x207, &x208, x206, x171, x195);
var x209: u64 = undefined;
var x210: u1 = undefined;
addcarryxU64(&x209, &x210, x208, ((@as(u64, x172) + @as(u64, x138)) + (@as(u64, x160) + x140)), (@as(u64, x196) + x176));
var x211: u64 = undefined;
var x212: u64 = undefined;
mulxU64(&x211, &x212, x3, 0xc84ee012b39bf21);
var x213: u64 = undefined;
var x214: u64 = undefined;
mulxU64(&x213, &x214, x3, 0x3fb05b7a28266895);
var x215: u64 = undefined;
var x216: u64 = undefined;
mulxU64(&x215, &x216, x3, 0xd40d49174aab1cc5);
var x217: u64 = undefined;
var x218: u64 = undefined;
mulxU64(&x217, &x218, x3, 0xbc3e483afcb82947);
var x219: u64 = undefined;
var x220: u64 = undefined;
mulxU64(&x219, &x220, x3, 0xff3d81e5df1aa419);
var x221: u64 = undefined;
var x222: u64 = undefined;
mulxU64(&x221, &x222, x3, 0x2d319b2419b409a9);
var x223: u64 = undefined;
var x224: u1 = undefined;
addcarryxU64(&x223, &x224, 0x0, x222, x219);
var x225: u64 = undefined;
var x226: u1 = undefined;
addcarryxU64(&x225, &x226, x224, x220, x217);
var x227: u64 = undefined;
var x228: u1 = undefined;
addcarryxU64(&x227, &x228, x226, x218, x215);
var x229: u64 = undefined;
var x230: u1 = undefined;
addcarryxU64(&x229, &x230, x228, x216, x213);
var x231: u64 = undefined;
var x232: u1 = undefined;
addcarryxU64(&x231, &x232, x230, x214, x211);
var x233: u64 = undefined;
var x234: u1 = undefined;
addcarryxU64(&x233, &x234, 0x0, x199, x221);
var x235: u64 = undefined;
var x236: u1 = undefined;
addcarryxU64(&x235, &x236, x234, x201, x223);
var x237: u64 = undefined;
var x238: u1 = undefined;
addcarryxU64(&x237, &x238, x236, x203, x225);
var x239: u64 = undefined;
var x240: u1 = undefined;
addcarryxU64(&x239, &x240, x238, x205, x227);
var x241: u64 = undefined;
var x242: u1 = undefined;
addcarryxU64(&x241, &x242, x240, x207, x229);
var x243: u64 = undefined;
var x244: u1 = undefined;
addcarryxU64(&x243, &x244, x242, x209, x231);
var x245: u64 = undefined;
var x246: u64 = undefined;
mulxU64(&x245, &x246, x233, 0x6ed46089e88fdc45);
var x247: u64 = undefined;
var x248: u64 = undefined;
mulxU64(&x247, &x248, x245, 0xffffffffffffffff);
var x249: u64 = undefined;
var x250: u64 = undefined;
mulxU64(&x249, &x250, x245, 0xffffffffffffffff);
var x251: u64 = undefined;
var x252: u64 = undefined;
mulxU64(&x251, &x252, x245, 0xffffffffffffffff);
var x253: u64 = undefined;
var x254: u64 = undefined;
mulxU64(&x253, &x254, x245, 0xc7634d81f4372ddf);
var x255: u64 = undefined;
var x256: u64 = undefined;
mulxU64(&x255, &x256, x245, 0x581a0db248b0a77a);
var x257: u64 = undefined;
var x258: u64 = undefined;
mulxU64(&x257, &x258, x245, 0xecec196accc52973);
var x259: u64 = undefined;
var x260: u1 = undefined;
addcarryxU64(&x259, &x260, 0x0, x258, x255);
var x261: u64 = undefined;
var x262: u1 = undefined;
addcarryxU64(&x261, &x262, x260, x256, x253);
var x263: u64 = undefined;
var x264: u1 = undefined;
addcarryxU64(&x263, &x264, x262, x254, x251);
var x265: u64 = undefined;
var x266: u1 = undefined;
addcarryxU64(&x265, &x266, x264, x252, x249);
var x267: u64 = undefined;
var x268: u1 = undefined;
addcarryxU64(&x267, &x268, x266, x250, x247);
var x269: u64 = undefined;
var x270: u1 = undefined;
addcarryxU64(&x269, &x270, 0x0, x233, x257);
var x271: u64 = undefined;
var x272: u1 = undefined;
addcarryxU64(&x271, &x272, x270, x235, x259);
var x273: u64 = undefined;
var x274: u1 = undefined;
addcarryxU64(&x273, &x274, x272, x237, x261);
var x275: u64 = undefined;
var x276: u1 = undefined;
addcarryxU64(&x275, &x276, x274, x239, x263);
var x277: u64 = undefined;
var x278: u1 = undefined;
addcarryxU64(&x277, &x278, x276, x241, x265);
var x279: u64 = undefined;
var x280: u1 = undefined;
addcarryxU64(&x279, &x280, x278, x243, x267);
var x281: u64 = undefined;
var x282: u1 = undefined;
addcarryxU64(&x281, &x282, x280, ((@as(u64, x244) + @as(u64, x210)) + (@as(u64, x232) + x212)), (@as(u64, x268) + x248));
var x283: u64 = undefined;
var x284: u64 = undefined;
mulxU64(&x283, &x284, x4, 0xc84ee012b39bf21);
var x285: u64 = undefined;
var x286: u64 = undefined;
mulxU64(&x285, &x286, x4, 0x3fb05b7a28266895);
var x287: u64 = undefined;
var x288: u64 = undefined;
mulxU64(&x287, &x288, x4, 0xd40d49174aab1cc5);
var x289: u64 = undefined;
var x290: u64 = undefined;
mulxU64(&x289, &x290, x4, 0xbc3e483afcb82947);
var x291: u64 = undefined;
var x292: u64 = undefined;
mulxU64(&x291, &x292, x4, 0xff3d81e5df1aa419);
var x293: u64 = undefined;
var x294: u64 = undefined;
mulxU64(&x293, &x294, x4, 0x2d319b2419b409a9);
var x295: u64 = undefined;
var x296: u1 = undefined;
addcarryxU64(&x295, &x296, 0x0, x294, x291);
var x297: u64 = undefined;
var x298: u1 = undefined;
addcarryxU64(&x297, &x298, x296, x292, x289);
var x299: u64 = undefined;
var x300: u1 = undefined;
addcarryxU64(&x299, &x300, x298, x290, x287);
var x301: u64 = undefined;
var x302: u1 = undefined;
addcarryxU64(&x301, &x302, x300, x288, x285);
var x303: u64 = undefined;
var x304: u1 = undefined;
addcarryxU64(&x303, &x304, x302, x286, x283);
var x305: u64 = undefined;
var x306: u1 = undefined;
addcarryxU64(&x305, &x306, 0x0, x271, x293);
var x307: u64 = undefined;
var x308: u1 = undefined;
addcarryxU64(&x307, &x308, x306, x273, x295);
var x309: u64 = undefined;
var x310: u1 = undefined;
addcarryxU64(&x309, &x310, x308, x275, x297);
var x311: u64 = undefined;
var x312: u1 = undefined;
addcarryxU64(&x311, &x312, x310, x277, x299);
var x313: u64 = undefined;
var x314: u1 = undefined;
addcarryxU64(&x313, &x314, x312, x279, x301);
var x315: u64 = undefined;
var x316: u1 = undefined;
addcarryxU64(&x315, &x316, x314, x281, x303);
var x317: u64 = undefined;
var x318: u64 = undefined;
mulxU64(&x317, &x318, x305, 0x6ed46089e88fdc45);
var x319: u64 = undefined;
var x320: u64 = undefined;
mulxU64(&x319, &x320, x317, 0xffffffffffffffff);
var x321: u64 = undefined;
var x322: u64 = undefined;
mulxU64(&x321, &x322, x317, 0xffffffffffffffff);
var x323: u64 = undefined;
var x324: u64 = undefined;
mulxU64(&x323, &x324, x317, 0xffffffffffffffff);
var x325: u64 = undefined;
var x326: u64 = undefined;
mulxU64(&x325, &x326, x317, 0xc7634d81f4372ddf);
var x327: u64 = undefined;
var x328: u64 = undefined;
mulxU64(&x327, &x328, x317, 0x581a0db248b0a77a);
var x329: u64 = undefined;
var x330: u64 = undefined;
mulxU64(&x329, &x330, x317, 0xecec196accc52973);
var x331: u64 = undefined;
var x332: u1 = undefined;
addcarryxU64(&x331, &x332, 0x0, x330, x327);
var x333: u64 = undefined;
var x334: u1 = undefined;
addcarryxU64(&x333, &x334, x332, x328, x325);
var x335: u64 = undefined;
var x336: u1 = undefined;
addcarryxU64(&x335, &x336, x334, x326, x323);
var x337: u64 = undefined;
var x338: u1 = undefined;
addcarryxU64(&x337, &x338, x336, x324, x321);
var x339: u64 = undefined;
var x340: u1 = undefined;
addcarryxU64(&x339, &x340, x338, x322, x319);
var x341: u64 = undefined;
var x342: u1 = undefined;
addcarryxU64(&x341, &x342, 0x0, x305, x329);
var x343: u64 = undefined;
var x344: u1 = undefined;
addcarryxU64(&x343, &x344, x342, x307, x331);
var x345: u64 = undefined;
var x346: u1 = undefined;
addcarryxU64(&x345, &x346, x344, x309, x333);
var x347: u64 = undefined;
var x348: u1 = undefined;
addcarryxU64(&x347, &x348, x346, x311, x335);
var x349: u64 = undefined;
var x350: u1 = undefined;
addcarryxU64(&x349, &x350, x348, x313, x337);
var x351: u64 = undefined;
var x352: u1 = undefined;
addcarryxU64(&x351, &x352, x350, x315, x339);
var x353: u64 = undefined;
var x354: u1 = undefined;
addcarryxU64(&x353, &x354, x352, ((@as(u64, x316) + @as(u64, x282)) + (@as(u64, x304) + x284)), (@as(u64, x340) + x320));
var x355: u64 = undefined;
var x356: u64 = undefined;
mulxU64(&x355, &x356, x5, 0xc84ee012b39bf21);
var x357: u64 = undefined;
var x358: u64 = undefined;
mulxU64(&x357, &x358, x5, 0x3fb05b7a28266895);
var x359: u64 = undefined;
var x360: u64 = undefined;
mulxU64(&x359, &x360, x5, 0xd40d49174aab1cc5);
var x361: u64 = undefined;
var x362: u64 = undefined;
mulxU64(&x361, &x362, x5, 0xbc3e483afcb82947);
var x363: u64 = undefined;
var x364: u64 = undefined;
mulxU64(&x363, &x364, x5, 0xff3d81e5df1aa419);
var x365: u64 = undefined;
var x366: u64 = undefined;
mulxU64(&x365, &x366, x5, 0x2d319b2419b409a9);
var x367: u64 = undefined;
var x368: u1 = undefined;
addcarryxU64(&x367, &x368, 0x0, x366, x363);
var x369: u64 = undefined;
var x370: u1 = undefined;
addcarryxU64(&x369, &x370, x368, x364, x361);
var x371: u64 = undefined;
var x372: u1 = undefined;
addcarryxU64(&x371, &x372, x370, x362, x359);
var x373: u64 = undefined;
var x374: u1 = undefined;
addcarryxU64(&x373, &x374, x372, x360, x357);
var x375: u64 = undefined;
var x376: u1 = undefined;
addcarryxU64(&x375, &x376, x374, x358, x355);
var x377: u64 = undefined;
var x378: u1 = undefined;
addcarryxU64(&x377, &x378, 0x0, x343, x365);
var x379: u64 = undefined;
var x380: u1 = undefined;
addcarryxU64(&x379, &x380, x378, x345, x367);
var x381: u64 = undefined;
var x382: u1 = undefined;
addcarryxU64(&x381, &x382, x380, x347, x369);
var x383: u64 = undefined;
var x384: u1 = undefined;
addcarryxU64(&x383, &x384, x382, x349, x371);
var x385: u64 = undefined;
var x386: u1 = undefined;
addcarryxU64(&x385, &x386, x384, x351, x373);
var x387: u64 = undefined;
var x388: u1 = undefined;
addcarryxU64(&x387, &x388, x386, x353, x375);
var x389: u64 = undefined;
var x390: u64 = undefined;
mulxU64(&x389, &x390, x377, 0x6ed46089e88fdc45);
var x391: u64 = undefined;
var x392: u64 = undefined;
mulxU64(&x391, &x392, x389, 0xffffffffffffffff);
var x393: u64 = undefined;
var x394: u64 = undefined;
mulxU64(&x393, &x394, x389, 0xffffffffffffffff);
var x395: u64 = undefined;
var x396: u64 = undefined;
mulxU64(&x395, &x396, x389, 0xffffffffffffffff);
var x397: u64 = undefined;
var x398: u64 = undefined;
mulxU64(&x397, &x398, x389, 0xc7634d81f4372ddf);
var x399: u64 = undefined;
var x400: u64 = undefined;
mulxU64(&x399, &x400, x389, 0x581a0db248b0a77a);
var x401: u64 = undefined;
var x402: u64 = undefined;
mulxU64(&x401, &x402, x389, 0xecec196accc52973);
var x403: u64 = undefined;
var x404: u1 = undefined;
addcarryxU64(&x403, &x404, 0x0, x402, x399);
var x405: u64 = undefined;
var x406: u1 = undefined;
addcarryxU64(&x405, &x406, x404, x400, x397);
var x407: u64 = undefined;
var x408: u1 = undefined;
addcarryxU64(&x407, &x408, x406, x398, x395);
var x409: u64 = undefined;
var x410: u1 = undefined;
addcarryxU64(&x409, &x410, x408, x396, x393);
var x411: u64 = undefined;
var x412: u1 = undefined;
addcarryxU64(&x411, &x412, x410, x394, x391);
var x413: u64 = undefined;
var x414: u1 = undefined;
addcarryxU64(&x413, &x414, 0x0, x377, x401);
var x415: u64 = undefined;
var x416: u1 = undefined;
addcarryxU64(&x415, &x416, x414, x379, x403);
var x417: u64 = undefined;
var x418: u1 = undefined;
addcarryxU64(&x417, &x418, x416, x381, x405);
var x419: u64 = undefined;
var x420: u1 = undefined;
addcarryxU64(&x419, &x420, x418, x383, x407);
var x421: u64 = undefined;
var x422: u1 = undefined;
addcarryxU64(&x421, &x422, x420, x385, x409);
var x423: u64 = undefined;
var x424: u1 = undefined;
addcarryxU64(&x423, &x424, x422, x387, x411);
var x425: u64 = undefined;
var x426: u1 = undefined;
addcarryxU64(&x425, &x426, x424, ((@as(u64, x388) + @as(u64, x354)) + (@as(u64, x376) + x356)), (@as(u64, x412) + x392));
var x427: u64 = undefined;
var x428: u1 = undefined;
subborrowxU64(&x427, &x428, 0x0, x415, 0xecec196accc52973);
var x429: u64 = undefined;
var x430: u1 = undefined;
subborrowxU64(&x429, &x430, x428, x417, 0x581a0db248b0a77a);
var x431: u64 = undefined;
var x432: u1 = undefined;
subborrowxU64(&x431, &x432, x430, x419, 0xc7634d81f4372ddf);
var x433: u64 = undefined;
var x434: u1 = undefined;
subborrowxU64(&x433, &x434, x432, x421, 0xffffffffffffffff);
var x435: u64 = undefined;
var x436: u1 = undefined;
subborrowxU64(&x435, &x436, x434, x423, 0xffffffffffffffff);
var x437: u64 = undefined;
var x438: u1 = undefined;
subborrowxU64(&x437, &x438, x436, x425, 0xffffffffffffffff);
var x439: u64 = undefined;
var x440: u1 = undefined;
subborrowxU64(&x439, &x440, x438, @as(u64, x426), 0x0);
var x441: u64 = undefined;
cmovznzU64(&x441, x440, x427, x415);
var x442: u64 = undefined;
cmovznzU64(&x442, x440, x429, x417);
var x443: u64 = undefined;
cmovznzU64(&x443, x440, x431, x419);
var x444: u64 = undefined;
cmovznzU64(&x444, x440, x433, x421);
var x445: u64 = undefined;
cmovznzU64(&x445, x440, x435, x423);
var x446: u64 = undefined;
cmovznzU64(&x446, x440, x437, x425);
out1[0] = x441;
out1[1] = x442;
out1[2] = x443;
out1[3] = x444;
out1[4] = x445;
out1[5] = x446;
}
/// The function nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
///
/// Input Bounds:
/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
pub fn nonzero(out1: *u64, arg1: [6]u64) void {
@setRuntimeSafety(mode == .Debug);
const x1 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | (arg1[5]))))));
out1.* = x1;
}
/// The function selectznz is a multi-limb conditional select.
///
/// Postconditions:
/// out1 = (if arg1 = 0 then arg2 else arg3)
///
/// Input Bounds:
/// arg1: [0x0 ~> 0x1]
/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn selectznz(out1: *[6]u64, arg1: u1, arg2: [6]u64, arg3: [6]u64) void {
@setRuntimeSafety(mode == .Debug);
var x1: u64 = undefined;
cmovznzU64(&x1, arg1, (arg2[0]), (arg3[0]));
var x2: u64 = undefined;
cmovznzU64(&x2, arg1, (arg2[1]), (arg3[1]));
var x3: u64 = undefined;
cmovznzU64(&x3, arg1, (arg2[2]), (arg3[2]));
var x4: u64 = undefined;
cmovznzU64(&x4, arg1, (arg2[3]), (arg3[3]));
var x5: u64 = undefined;
cmovznzU64(&x5, arg1, (arg2[4]), (arg3[4]));
var x6: u64 = undefined;
cmovznzU64(&x6, arg1, (arg2[5]), (arg3[5]));
out1[0] = x1;
out1[1] = x2;
out1[2] = x3;
out1[3] = x4;
out1[4] = x5;
out1[5] = x6;
}
/// The function toBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
///
/// Preconditions:
/// 0 ≤ eval arg1 < m
/// Postconditions:
/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47]
///
/// Input Bounds:
/// arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// Output Bounds:
/// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
pub fn toBytes(out1: *[48]u8, arg1: [6]u64) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (arg1[5]);
const x2 = (arg1[4]);
const x3 = (arg1[3]);
const x4 = (arg1[2]);
const x5 = (arg1[1]);
const x6 = (arg1[0]);
const x7 = @as(u8, @truncate((x6 & 0xff)));
const x8 = (x6 >> 8);
const x9 = @as(u8, @truncate((x8 & 0xff)));
const x10 = (x8 >> 8);
const x11 = @as(u8, @truncate((x10 & 0xff)));
const x12 = (x10 >> 8);
const x13 = @as(u8, @truncate((x12 & 0xff)));
const x14 = (x12 >> 8);
const x15 = @as(u8, @truncate((x14 & 0xff)));
const x16 = (x14 >> 8);
const x17 = @as(u8, @truncate((x16 & 0xff)));
const x18 = (x16 >> 8);
const x19 = @as(u8, @truncate((x18 & 0xff)));
const x20 = @as(u8, @truncate((x18 >> 8)));
const x21 = @as(u8, @truncate((x5 & 0xff)));
const x22 = (x5 >> 8);
const x23 = @as(u8, @truncate((x22 & 0xff)));
const x24 = (x22 >> 8);
const x25 = @as(u8, @truncate((x24 & 0xff)));
const x26 = (x24 >> 8);
const x27 = @as(u8, @truncate((x26 & 0xff)));
const x28 = (x26 >> 8);
const x29 = @as(u8, @truncate((x28 & 0xff)));
const x30 = (x28 >> 8);
const x31 = @as(u8, @truncate((x30 & 0xff)));
const x32 = (x30 >> 8);
const x33 = @as(u8, @truncate((x32 & 0xff)));
const x34 = @as(u8, @truncate((x32 >> 8)));
const x35 = @as(u8, @truncate((x4 & 0xff)));
const x36 = (x4 >> 8);
const x37 = @as(u8, @truncate((x36 & 0xff)));
const x38 = (x36 >> 8);
const x39 = @as(u8, @truncate((x38 & 0xff)));
const x40 = (x38 >> 8);
const x41 = @as(u8, @truncate((x40 & 0xff)));
const x42 = (x40 >> 8);
const x43 = @as(u8, @truncate((x42 & 0xff)));
const x44 = (x42 >> 8);
const x45 = @as(u8, @truncate((x44 & 0xff)));
const x46 = (x44 >> 8);
const x47 = @as(u8, @truncate((x46 & 0xff)));
const x48 = @as(u8, @truncate((x46 >> 8)));
const x49 = @as(u8, @truncate((x3 & 0xff)));
const x50 = (x3 >> 8);
const x51 = @as(u8, @truncate((x50 & 0xff)));
const x52 = (x50 >> 8);
const x53 = @as(u8, @truncate((x52 & 0xff)));
const x54 = (x52 >> 8);
const x55 = @as(u8, @truncate((x54 & 0xff)));
const x56 = (x54 >> 8);
const x57 = @as(u8, @truncate((x56 & 0xff)));
const x58 = (x56 >> 8);
const x59 = @as(u8, @truncate((x58 & 0xff)));
const x60 = (x58 >> 8);
const x61 = @as(u8, @truncate((x60 & 0xff)));
const x62 = @as(u8, @truncate((x60 >> 8)));
const x63 = @as(u8, @truncate((x2 & 0xff)));
const x64 = (x2 >> 8);
const x65 = @as(u8, @truncate((x64 & 0xff)));
const x66 = (x64 >> 8);
const x67 = @as(u8, @truncate((x66 & 0xff)));
const x68 = (x66 >> 8);
const x69 = @as(u8, @truncate((x68 & 0xff)));
const x70 = (x68 >> 8);
const x71 = @as(u8, @truncate((x70 & 0xff)));
const x72 = (x70 >> 8);
const x73 = @as(u8, @truncate((x72 & 0xff)));
const x74 = (x72 >> 8);
const x75 = @as(u8, @truncate((x74 & 0xff)));
const x76 = @as(u8, @truncate((x74 >> 8)));
const x77 = @as(u8, @truncate((x1 & 0xff)));
const x78 = (x1 >> 8);
const x79 = @as(u8, @truncate((x78 & 0xff)));
const x80 = (x78 >> 8);
const x81 = @as(u8, @truncate((x80 & 0xff)));
const x82 = (x80 >> 8);
const x83 = @as(u8, @truncate((x82 & 0xff)));
const x84 = (x82 >> 8);
const x85 = @as(u8, @truncate((x84 & 0xff)));
const x86 = (x84 >> 8);
const x87 = @as(u8, @truncate((x86 & 0xff)));
const x88 = (x86 >> 8);
const x89 = @as(u8, @truncate((x88 & 0xff)));
const x90 = @as(u8, @truncate((x88 >> 8)));
out1[0] = x7;
out1[1] = x9;
out1[2] = x11;
out1[3] = x13;
out1[4] = x15;
out1[5] = x17;
out1[6] = x19;
out1[7] = x20;
out1[8] = x21;
out1[9] = x23;
out1[10] = x25;
out1[11] = x27;
out1[12] = x29;
out1[13] = x31;
out1[14] = x33;
out1[15] = x34;
out1[16] = x35;
out1[17] = x37;
out1[18] = x39;
out1[19] = x41;
out1[20] = x43;
out1[21] = x45;
out1[22] = x47;
out1[23] = x48;
out1[24] = x49;
out1[25] = x51;
out1[26] = x53;
out1[27] = x55;
out1[28] = x57;
out1[29] = x59;
out1[30] = x61;
out1[31] = x62;
out1[32] = x63;
out1[33] = x65;
out1[34] = x67;
out1[35] = x69;
out1[36] = x71;
out1[37] = x73;
out1[38] = x75;
out1[39] = x76;
out1[40] = x77;
out1[41] = x79;
out1[42] = x81;
out1[43] = x83;
out1[44] = x85;
out1[45] = x87;
out1[46] = x89;
out1[47] = x90;
}
/// The function fromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
///
/// Preconditions:
/// 0 ≤ bytes_eval arg1 < m
/// Postconditions:
/// eval out1 mod m = bytes_eval arg1 mod m
/// 0 ≤ eval out1 < m
///
/// Input Bounds:
/// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn fromBytes(out1: *[6]u64, arg1: [48]u8) void {
@setRuntimeSafety(mode == .Debug);
const x1 = (@as(u64, (arg1[47])) << 56);
const x2 = (@as(u64, (arg1[46])) << 48);
const x3 = (@as(u64, (arg1[45])) << 40);
const x4 = (@as(u64, (arg1[44])) << 32);
const x5 = (@as(u64, (arg1[43])) << 24);
const x6 = (@as(u64, (arg1[42])) << 16);
const x7 = (@as(u64, (arg1[41])) << 8);
const x8 = (arg1[40]);
const x9 = (@as(u64, (arg1[39])) << 56);
const x10 = (@as(u64, (arg1[38])) << 48);
const x11 = (@as(u64, (arg1[37])) << 40);
const x12 = (@as(u64, (arg1[36])) << 32);
const x13 = (@as(u64, (arg1[35])) << 24);
const x14 = (@as(u64, (arg1[34])) << 16);
const x15 = (@as(u64, (arg1[33])) << 8);
const x16 = (arg1[32]);
const x17 = (@as(u64, (arg1[31])) << 56);
const x18 = (@as(u64, (arg1[30])) << 48);
const x19 = (@as(u64, (arg1[29])) << 40);
const x20 = (@as(u64, (arg1[28])) << 32);
const x21 = (@as(u64, (arg1[27])) << 24);
const x22 = (@as(u64, (arg1[26])) << 16);
const x23 = (@as(u64, (arg1[25])) << 8);
const x24 = (arg1[24]);
const x25 = (@as(u64, (arg1[23])) << 56);
const x26 = (@as(u64, (arg1[22])) << 48);
const x27 = (@as(u64, (arg1[21])) << 40);
const x28 = (@as(u64, (arg1[20])) << 32);
const x29 = (@as(u64, (arg1[19])) << 24);
const x30 = (@as(u64, (arg1[18])) << 16);
const x31 = (@as(u64, (arg1[17])) << 8);
const x32 = (arg1[16]);
const x33 = (@as(u64, (arg1[15])) << 56);
const x34 = (@as(u64, (arg1[14])) << 48);
const x35 = (@as(u64, (arg1[13])) << 40);
const x36 = (@as(u64, (arg1[12])) << 32);
const x37 = (@as(u64, (arg1[11])) << 24);
const x38 = (@as(u64, (arg1[10])) << 16);
const x39 = (@as(u64, (arg1[9])) << 8);
const x40 = (arg1[8]);
const x41 = (@as(u64, (arg1[7])) << 56);
const x42 = (@as(u64, (arg1[6])) << 48);
const x43 = (@as(u64, (arg1[5])) << 40);
const x44 = (@as(u64, (arg1[4])) << 32);
const x45 = (@as(u64, (arg1[3])) << 24);
const x46 = (@as(u64, (arg1[2])) << 16);
const x47 = (@as(u64, (arg1[1])) << 8);
const x48 = (arg1[0]);
const x49 = (x47 + @as(u64, x48));
const x50 = (x46 + x49);
const x51 = (x45 + x50);
const x52 = (x44 + x51);
const x53 = (x43 + x52);
const x54 = (x42 + x53);
const x55 = (x41 + x54);
const x56 = (x39 + @as(u64, x40));
const x57 = (x38 + x56);
const x58 = (x37 + x57);
const x59 = (x36 + x58);
const x60 = (x35 + x59);
const x61 = (x34 + x60);
const x62 = (x33 + x61);
const x63 = (x31 + @as(u64, x32));
const x64 = (x30 + x63);
const x65 = (x29 + x64);
const x66 = (x28 + x65);
const x67 = (x27 + x66);
const x68 = (x26 + x67);
const x69 = (x25 + x68);
const x70 = (x23 + @as(u64, x24));
const x71 = (x22 + x70);
const x72 = (x21 + x71);
const x73 = (x20 + x72);
const x74 = (x19 + x73);
const x75 = (x18 + x74);
const x76 = (x17 + x75);
const x77 = (x15 + @as(u64, x16));
const x78 = (x14 + x77);
const x79 = (x13 + x78);
const x80 = (x12 + x79);
const x81 = (x11 + x80);
const x82 = (x10 + x81);
const x83 = (x9 + x82);
const x84 = (x7 + @as(u64, x8));
const x85 = (x6 + x84);
const x86 = (x5 + x85);
const x87 = (x4 + x86);
const x88 = (x3 + x87);
const x89 = (x2 + x88);
const x90 = (x1 + x89);
out1[0] = x55;
out1[1] = x62;
out1[2] = x69;
out1[3] = x76;
out1[4] = x83;
out1[5] = x90;
}
/// The function setOne returns the field element one in the Montgomery domain.
///
/// Postconditions:
/// eval (from_montgomery out1) mod m = 1 mod m
/// 0 ≤ eval out1 < m
///
pub fn setOne(out1: *MontgomeryDomainFieldElement) void {
@setRuntimeSafety(mode == .Debug);
out1[0] = 0x1313e695333ad68d;
out1[1] = 0xa7e5f24db74f5885;
out1[2] = 0x389cb27e0bc8d220;
out1[3] = 0x0;
out1[4] = 0x0;
out1[5] = 0x0;
}
/// The function msat returns the saturated representation of the prime modulus.
///
/// Postconditions:
/// twos_complement_eval out1 = m
/// 0 ≤ eval out1 < m
///
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn msat(out1: *[7]u64) void {
@setRuntimeSafety(mode == .Debug);
out1[0] = 0xecec196accc52973;
out1[1] = 0x581a0db248b0a77a;
out1[2] = 0xc7634d81f4372ddf;
out1[3] = 0xffffffffffffffff;
out1[4] = 0xffffffffffffffff;
out1[5] = 0xffffffffffffffff;
out1[6] = 0x0;
}
/// The function divstep computes a divstep.
///
/// Preconditions:
/// 0 ≤ eval arg4 < m
/// 0 ≤ eval arg5 < m
/// Postconditions:
/// out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
/// twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
/// 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⌋)
/// 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)
/// 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)
/// 0 ≤ eval out5 < m
/// 0 ≤ eval out5 < m
/// 0 ≤ eval out2 < m
/// 0 ≤ eval out3 < m
///
/// Input Bounds:
/// arg1: [0x0 ~> 0xffffffffffffffff]
/// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// arg4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// arg5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// Output Bounds:
/// out1: [0x0 ~> 0xffffffffffffffff]
/// out2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// out3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// out4: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
/// out5: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn divstep(out1: *u64, out2: *[7]u64, out3: *[7]u64, out4: *[6]u64, out5: *[6]u64, arg1: u64, arg2: [7]u64, arg3: [7]u64, arg4: [6]u64, arg5: [6]u64) void {
@setRuntimeSafety(mode == .Debug);
var x1: u64 = undefined;
var x2: u1 = undefined;
addcarryxU64(&x1, &x2, 0x0, (~arg1), 0x1);
const x3 = (@as(u1, @truncate((x1 >> 63))) & @as(u1, @truncate(((arg3[0]) & 0x1))));
var x4: u64 = undefined;
var x5: u1 = undefined;
addcarryxU64(&x4, &x5, 0x0, (~arg1), 0x1);
var x6: u64 = undefined;
cmovznzU64(&x6, x3, arg1, x4);
var x7: u64 = undefined;
cmovznzU64(&x7, x3, (arg2[0]), (arg3[0]));
var x8: u64 = undefined;
cmovznzU64(&x8, x3, (arg2[1]), (arg3[1]));
var x9: u64 = undefined;
cmovznzU64(&x9, x3, (arg2[2]), (arg3[2]));
var x10: u64 = undefined;
cmovznzU64(&x10, x3, (arg2[3]), (arg3[3]));
var x11: u64 = undefined;
cmovznzU64(&x11, x3, (arg2[4]), (arg3[4]));
var x12: u64 = undefined;
cmovznzU64(&x12, x3, (arg2[5]), (arg3[5]));
var x13: u64 = undefined;
cmovznzU64(&x13, x3, (arg2[6]), (arg3[6]));
var x14: u64 = undefined;
var x15: u1 = undefined;
addcarryxU64(&x14, &x15, 0x0, 0x1, (~(arg2[0])));
var x16: u64 = undefined;
var x17: u1 = undefined;
addcarryxU64(&x16, &x17, x15, 0x0, (~(arg2[1])));
var x18: u64 = undefined;
var x19: u1 = undefined;
addcarryxU64(&x18, &x19, x17, 0x0, (~(arg2[2])));
var x20: u64 = undefined;
var x21: u1 = undefined;
addcarryxU64(&x20, &x21, x19, 0x0, (~(arg2[3])));
var x22: u64 = undefined;
var x23: u1 = undefined;
addcarryxU64(&x22, &x23, x21, 0x0, (~(arg2[4])));
var x24: u64 = undefined;
var x25: u1 = undefined;
addcarryxU64(&x24, &x25, x23, 0x0, (~(arg2[5])));
var x26: u64 = undefined;
var x27: u1 = undefined;
addcarryxU64(&x26, &x27, x25, 0x0, (~(arg2[6])));
var x28: u64 = undefined;
cmovznzU64(&x28, x3, (arg3[0]), x14);
var x29: u64 = undefined;
cmovznzU64(&x29, x3, (arg3[1]), x16);
var x30: u64 = undefined;
cmovznzU64(&x30, x3, (arg3[2]), x18);
var x31: u64 = undefined;
cmovznzU64(&x31, x3, (arg3[3]), x20);
var x32: u64 = undefined;
cmovznzU64(&x32, x3, (arg3[4]), x22);
var x33: u64 = undefined;
cmovznzU64(&x33, x3, (arg3[5]), x24);
var x34: u64 = undefined;
cmovznzU64(&x34, x3, (arg3[6]), x26);
var x35: u64 = undefined;
cmovznzU64(&x35, x3, (arg4[0]), (arg5[0]));
var x36: u64 = undefined;
cmovznzU64(&x36, x3, (arg4[1]), (arg5[1]));
var x37: u64 = undefined;
cmovznzU64(&x37, x3, (arg4[2]), (arg5[2]));
var x38: u64 = undefined;
cmovznzU64(&x38, x3, (arg4[3]), (arg5[3]));
var x39: u64 = undefined;
cmovznzU64(&x39, x3, (arg4[4]), (arg5[4]));
var x40: u64 = undefined;
cmovznzU64(&x40, x3, (arg4[5]), (arg5[5]));
var x41: u64 = undefined;
var x42: u1 = undefined;
addcarryxU64(&x41, &x42, 0x0, x35, x35);
var x43: u64 = undefined;
var x44: u1 = undefined;
addcarryxU64(&x43, &x44, x42, x36, x36);
var x45: u64 = undefined;
var x46: u1 = undefined;
addcarryxU64(&x45, &x46, x44, x37, x37);
var x47: u64 = undefined;
var x48: u1 = undefined;
addcarryxU64(&x47, &x48, x46, x38, x38);
var x49: u64 = undefined;
var x50: u1 = undefined;
addcarryxU64(&x49, &x50, x48, x39, x39);
var x51: u64 = undefined;
var x52: u1 = undefined;
addcarryxU64(&x51, &x52, x50, x40, x40);
var x53: u64 = undefined;
var x54: u1 = undefined;
subborrowxU64(&x53, &x54, 0x0, x41, 0xecec196accc52973);
var x55: u64 = undefined;
var x56: u1 = undefined;
subborrowxU64(&x55, &x56, x54, x43, 0x581a0db248b0a77a);
var x57: u64 = undefined;
var x58: u1 = undefined;
subborrowxU64(&x57, &x58, x56, x45, 0xc7634d81f4372ddf);
var x59: u64 = undefined;
var x60: u1 = undefined;
subborrowxU64(&x59, &x60, x58, x47, 0xffffffffffffffff);
var x61: u64 = undefined;
var x62: u1 = undefined;
subborrowxU64(&x61, &x62, x60, x49, 0xffffffffffffffff);
var x63: u64 = undefined;
var x64: u1 = undefined;
subborrowxU64(&x63, &x64, x62, x51, 0xffffffffffffffff);
var x65: u64 = undefined;
var x66: u1 = undefined;
subborrowxU64(&x65, &x66, x64, @as(u64, x52), 0x0);
const x67 = (arg4[5]);
const x68 = (arg4[4]);
const x69 = (arg4[3]);
const x70 = (arg4[2]);
const x71 = (arg4[1]);
const x72 = (arg4[0]);
var x73: u64 = undefined;
var x74: u1 = undefined;
subborrowxU64(&x73, &x74, 0x0, 0x0, x72);
var x75: u64 = undefined;
var x76: u1 = undefined;
subborrowxU64(&x75, &x76, x74, 0x0, x71);
var x77: u64 = undefined;
var x78: u1 = undefined;
subborrowxU64(&x77, &x78, x76, 0x0, x70);
var x79: u64 = undefined;
var x80: u1 = undefined;
subborrowxU64(&x79, &x80, x78, 0x0, x69);
var x81: u64 = undefined;
var x82: u1 = undefined;
subborrowxU64(&x81, &x82, x80, 0x0, x68);
var x83: u64 = undefined;
var x84: u1 = undefined;
subborrowxU64(&x83, &x84, x82, 0x0, x67);
var x85: u64 = undefined;
cmovznzU64(&x85, x84, 0x0, 0xffffffffffffffff);
var x86: u64 = undefined;
var x87: u1 = undefined;
addcarryxU64(&x86, &x87, 0x0, x73, (x85 & 0xecec196accc52973));
var x88: u64 = undefined;
var x89: u1 = undefined;
addcarryxU64(&x88, &x89, x87, x75, (x85 & 0x581a0db248b0a77a));
var x90: u64 = undefined;
var x91: u1 = undefined;
addcarryxU64(&x90, &x91, x89, x77, (x85 & 0xc7634d81f4372ddf));
var x92: u64 = undefined;
var x93: u1 = undefined;
addcarryxU64(&x92, &x93, x91, x79, x85);
var x94: u64 = undefined;
var x95: u1 = undefined;
addcarryxU64(&x94, &x95, x93, x81, x85);
var x96: u64 = undefined;
var x97: u1 = undefined;
addcarryxU64(&x96, &x97, x95, x83, x85);
var x98: u64 = undefined;
cmovznzU64(&x98, x3, (arg5[0]), x86);
var x99: u64 = undefined;
cmovznzU64(&x99, x3, (arg5[1]), x88);
var x100: u64 = undefined;
cmovznzU64(&x100, x3, (arg5[2]), x90);
var x101: u64 = undefined;
cmovznzU64(&x101, x3, (arg5[3]), x92);
var x102: u64 = undefined;
cmovznzU64(&x102, x3, (arg5[4]), x94);
var x103: u64 = undefined;
cmovznzU64(&x103, x3, (arg5[5]), x96);
const x104 = @as(u1, @truncate((x28 & 0x1)));
var x105: u64 = undefined;
cmovznzU64(&x105, x104, 0x0, x7);
var x106: u64 = undefined;
cmovznzU64(&x106, x104, 0x0, x8);
var x107: u64 = undefined;
cmovznzU64(&x107, x104, 0x0, x9);
var x108: u64 = undefined;
cmovznzU64(&x108, x104, 0x0, x10);
var x109: u64 = undefined;
cmovznzU64(&x109, x104, 0x0, x11);
var x110: u64 = undefined;
cmovznzU64(&x110, x104, 0x0, x12);
var x111: u64 = undefined;
cmovznzU64(&x111, x104, 0x0, x13);
var x112: u64 = undefined;
var x113: u1 = undefined;
addcarryxU64(&x112, &x113, 0x0, x28, x105);
var x114: u64 = undefined;
var x115: u1 = undefined;
addcarryxU64(&x114, &x115, x113, x29, x106);
var x116: u64 = undefined;
var x117: u1 = undefined;
addcarryxU64(&x116, &x117, x115, x30, x107);
var x118: u64 = undefined;
var x119: u1 = undefined;
addcarryxU64(&x118, &x119, x117, x31, x108);
var x120: u64 = undefined;
var x121: u1 = undefined;
addcarryxU64(&x120, &x121, x119, x32, x109);
var x122: u64 = undefined;
var x123: u1 = undefined;
addcarryxU64(&x122, &x123, x121, x33, x110);
var x124: u64 = undefined;
var x125: u1 = undefined;
addcarryxU64(&x124, &x125, x123, x34, x111);
var x126: u64 = undefined;
cmovznzU64(&x126, x104, 0x0, x35);
var x127: u64 = undefined;
cmovznzU64(&x127, x104, 0x0, x36);
var x128: u64 = undefined;
cmovznzU64(&x128, x104, 0x0, x37);
var x129: u64 = undefined;
cmovznzU64(&x129, x104, 0x0, x38);
var x130: u64 = undefined;
cmovznzU64(&x130, x104, 0x0, x39);
var x131: u64 = undefined;
cmovznzU64(&x131, x104, 0x0, x40);
var x132: u64 = undefined;
var x133: u1 = undefined;
addcarryxU64(&x132, &x133, 0x0, x98, x126);
var x134: u64 = undefined;
var x135: u1 = undefined;
addcarryxU64(&x134, &x135, x133, x99, x127);
var x136: u64 = undefined;
var x137: u1 = undefined;
addcarryxU64(&x136, &x137, x135, x100, x128);
var x138: u64 = undefined;
var x139: u1 = undefined;
addcarryxU64(&x138, &x139, x137, x101, x129);
var x140: u64 = undefined;
var x141: u1 = undefined;
addcarryxU64(&x140, &x141, x139, x102, x130);
var x142: u64 = undefined;
var x143: u1 = undefined;
addcarryxU64(&x142, &x143, x141, x103, x131);
var x144: u64 = undefined;
var x145: u1 = undefined;
subborrowxU64(&x144, &x145, 0x0, x132, 0xecec196accc52973);
var x146: u64 = undefined;
var x147: u1 = undefined;
subborrowxU64(&x146, &x147, x145, x134, 0x581a0db248b0a77a);
var x148: u64 = undefined;
var x149: u1 = undefined;
subborrowxU64(&x148, &x149, x147, x136, 0xc7634d81f4372ddf);
var x150: u64 = undefined;
var x151: u1 = undefined;
subborrowxU64(&x150, &x151, x149, x138, 0xffffffffffffffff);
var x152: u64 = undefined;
var x153: u1 = undefined;
subborrowxU64(&x152, &x153, x151, x140, 0xffffffffffffffff);
var x154: u64 = undefined;
var x155: u1 = undefined;
subborrowxU64(&x154, &x155, x153, x142, 0xffffffffffffffff);
var x156: u64 = undefined;
var x157: u1 = undefined;
subborrowxU64(&x156, &x157, x155, @as(u64, x143), 0x0);
var x158: u64 = undefined;
var x159: u1 = undefined;
addcarryxU64(&x158, &x159, 0x0, x6, 0x1);
const x160 = ((x112 >> 1) | ((x114 << 63) & 0xffffffffffffffff));
const x161 = ((x114 >> 1) | ((x116 << 63) & 0xffffffffffffffff));
const x162 = ((x116 >> 1) | ((x118 << 63) & 0xffffffffffffffff));
const x163 = ((x118 >> 1) | ((x120 << 63) & 0xffffffffffffffff));
const x164 = ((x120 >> 1) | ((x122 << 63) & 0xffffffffffffffff));
const x165 = ((x122 >> 1) | ((x124 << 63) & 0xffffffffffffffff));
const x166 = ((x124 & 0x8000000000000000) | (x124 >> 1));
var x167: u64 = undefined;
cmovznzU64(&x167, x66, x53, x41);
var x168: u64 = undefined;
cmovznzU64(&x168, x66, x55, x43);
var x169: u64 = undefined;
cmovznzU64(&x169, x66, x57, x45);
var x170: u64 = undefined;
cmovznzU64(&x170, x66, x59, x47);
var x171: u64 = undefined;
cmovznzU64(&x171, x66, x61, x49);
var x172: u64 = undefined;
cmovznzU64(&x172, x66, x63, x51);
var x173: u64 = undefined;
cmovznzU64(&x173, x157, x144, x132);
var x174: u64 = undefined;
cmovznzU64(&x174, x157, x146, x134);
var x175: u64 = undefined;
cmovznzU64(&x175, x157, x148, x136);
var x176: u64 = undefined;
cmovznzU64(&x176, x157, x150, x138);
var x177: u64 = undefined;
cmovznzU64(&x177, x157, x152, x140);
var x178: u64 = undefined;
cmovznzU64(&x178, x157, x154, x142);
out1.* = x158;
out2[0] = x7;
out2[1] = x8;
out2[2] = x9;
out2[3] = x10;
out2[4] = x11;
out2[5] = x12;
out2[6] = x13;
out3[0] = x160;
out3[1] = x161;
out3[2] = x162;
out3[3] = x163;
out3[4] = x164;
out3[5] = x165;
out3[6] = x166;
out4[0] = x167;
out4[1] = x168;
out4[2] = x169;
out4[3] = x170;
out4[4] = x171;
out4[5] = x172;
out5[0] = x173;
out5[1] = x174;
out5[2] = x175;
out5[3] = x176;
out5[4] = x177;
out5[5] = x178;
}
/// The function divstepPrecomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
///
/// Postconditions:
/// 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⌋)
/// 0 ≤ eval out1 < m
///
/// Output Bounds:
/// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
pub fn divstepPrecomp(out1: *[6]u64) void {
@setRuntimeSafety(mode == .Debug);
out1[0] = 0x49589ae0e6045b6a;
out1[1] = 0x3c9a5352870040ed;
out1[2] = 0xdacb097e977dc242;
out1[3] = 0xb5ab30a6d1ecbe36;
out1[4] = 0x97d7a1081f959973;
out1[5] = 0x2ba012f8d27192bc;
}