// Code generated by Fiat Cryptography. DO NOT EDIT.
//
// Autogenerated: 'fiat-crypto/src/ExtractionOCaml/unsaturated_solinas' --lang Go --no-wide-int --cmovznz-by-mul --internal-static --public-function-case camelCase --public-type-case camelCase --private-function-case camelCase --private-type-case camelCase --no-prefix-fiat --package-name fiat --doc-text-before-function-name '' --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --doc-newline-before-package-declaration p521 64 9 '2^521 - 1' carry_mul carry_square carry add sub to_bytes from_bytes selectznz
//
// curve description: p521
//
// machine_wordsize = 64 (from "64")
//
// requested operations: carry_mul, carry_square, carry, add, sub, to_bytes, from_bytes, selectznz
//
// n = 9 (from "9")
//
// s-c = 2^521 - [(1, 1)] (from "2^521 - 1")
//
// tight_bounds_multiplier = 1 (from "")
//
//
//
// Computed values:
//
//   carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]
//
//   eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0)
//
//   bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)
//
//   balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe]

package fiat

import "math/bits"

type p521Uint1 uint8
type p521Int1 int8

// p521AddcarryxU64 is a thin wrapper around bits.Add64 that uses p521Uint1 rather than uint64
func p521AddcarryxU64(x uint64, y uint64, carry p521Uint1) (uint64, p521Uint1) {
	sum, carryOut := bits.Add64(x, y, uint64(carry))
	return sum, p521Uint1(carryOut)
}

// p521SubborrowxU64 is a thin wrapper around bits.Sub64 that uses p521Uint1 rather than uint64
func p521SubborrowxU64(x uint64, y uint64, carry p521Uint1) (uint64, p521Uint1) {
	sum, carryOut := bits.Sub64(x, y, uint64(carry))
	return sum, p521Uint1(carryOut)
}

// p521AddcarryxU58 is an addition with carry.
//
// Postconditions:
//   out1 = (arg1 + arg2 + arg3) mod 2^58
//   out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋
//
// Input Bounds:
//   arg1: [0x0 ~> 0x1]
//   arg2: [0x0 ~> 0x3ffffffffffffff]
//   arg3: [0x0 ~> 0x3ffffffffffffff]
// Output Bounds:
//   out1: [0x0 ~> 0x3ffffffffffffff]
//   out2: [0x0 ~> 0x1]
func p521AddcarryxU58(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
	x1 := ((uint64(arg1) + arg2) + arg3)
	x2 := (x1 & 0x3ffffffffffffff)
	x3 := p521Uint1((x1 >> 58))
	*out1 = x2
	*out2 = x3
}

// p521SubborrowxU58 is a subtraction with borrow.
//
// Postconditions:
//   out1 = (-arg1 + arg2 + -arg3) mod 2^58
//   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋
//
// Input Bounds:
//   arg1: [0x0 ~> 0x1]
//   arg2: [0x0 ~> 0x3ffffffffffffff]
//   arg3: [0x0 ~> 0x3ffffffffffffff]
// Output Bounds:
//   out1: [0x0 ~> 0x3ffffffffffffff]
//   out2: [0x0 ~> 0x1]
func p521SubborrowxU58(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
	x1 := ((int64(arg2) - int64(arg1)) - int64(arg3))
	x2 := p521Int1((x1 >> 58))
	x3 := (uint64(x1) & 0x3ffffffffffffff)
	*out1 = x3
	*out2 = (0x0 - p521Uint1(x2))
}

// p521AddcarryxU57 is an addition with carry.
//
// Postconditions:
//   out1 = (arg1 + arg2 + arg3) mod 2^57
//   out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋
//
// Input Bounds:
//   arg1: [0x0 ~> 0x1]
//   arg2: [0x0 ~> 0x1ffffffffffffff]
//   arg3: [0x0 ~> 0x1ffffffffffffff]
// Output Bounds:
//   out1: [0x0 ~> 0x1ffffffffffffff]
//   out2: [0x0 ~> 0x1]
func p521AddcarryxU57(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
	x1 := ((uint64(arg1) + arg2) + arg3)
	x2 := (x1 & 0x1ffffffffffffff)
	x3 := p521Uint1((x1 >> 57))
	*out1 = x2
	*out2 = x3
}

// p521SubborrowxU57 is a subtraction with borrow.
//
// Postconditions:
//   out1 = (-arg1 + arg2 + -arg3) mod 2^57
//   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋
//
// Input Bounds:
//   arg1: [0x0 ~> 0x1]
//   arg2: [0x0 ~> 0x1ffffffffffffff]
//   arg3: [0x0 ~> 0x1ffffffffffffff]
// Output Bounds:
//   out1: [0x0 ~> 0x1ffffffffffffff]
//   out2: [0x0 ~> 0x1]
func p521SubborrowxU57(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
	x1 := ((int64(arg2) - int64(arg1)) - int64(arg3))
	x2 := p521Int1((x1 >> 57))
	x3 := (uint64(x1) & 0x1ffffffffffffff)
	*out1 = x3
	*out2 = (0x0 - p521Uint1(x2))
}

// p521CmovznzU64 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]
func p521CmovznzU64(out1 *uint64, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
	x1 := (uint64(arg1) * 0xffffffffffffffff)
	x2 := ((x1 & arg3) | ((^x1) & arg2))
	*out1 = x2
}

// p521CarryMul multiplies two field elements and reduces the result.
//
// Postconditions:
//   eval out1 mod m = (eval arg1 * eval arg2) mod m
//
// Input Bounds:
//   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
//   arg2: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
// Output Bounds:
//   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
func p521CarryMul(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
	var x1 uint64
	var x2 uint64
	x2, x1 = bits.Mul64(arg1[8], (arg2[8] * 0x2))
	var x3 uint64
	var x4 uint64
	x4, x3 = bits.Mul64(arg1[8], (arg2[7] * 0x2))
	var x5 uint64
	var x6 uint64
	x6, x5 = bits.Mul64(arg1[8], (arg2[6] * 0x2))
	var x7 uint64
	var x8 uint64
	x8, x7 = bits.Mul64(arg1[8], (arg2[5] * 0x2))
	var x9 uint64
	var x10 uint64
	x10, x9 = bits.Mul64(arg1[8], (arg2[4] * 0x2))
	var x11 uint64
	var x12 uint64
	x12, x11 = bits.Mul64(arg1[8], (arg2[3] * 0x2))
	var x13 uint64
	var x14 uint64
	x14, x13 = bits.Mul64(arg1[8], (arg2[2] * 0x2))
	var x15 uint64
	var x16 uint64
	x16, x15 = bits.Mul64(arg1[8], (arg2[1] * 0x2))
	var x17 uint64
	var x18 uint64
	x18, x17 = bits.Mul64(arg1[7], (arg2[8] * 0x2))
	var x19 uint64
	var x20 uint64
	x20, x19 = bits.Mul64(arg1[7], (arg2[7] * 0x2))
	var x21 uint64
	var x22 uint64
	x22, x21 = bits.Mul64(arg1[7], (arg2[6] * 0x2))
	var x23 uint64
	var x24 uint64
	x24, x23 = bits.Mul64(arg1[7], (arg2[5] * 0x2))
	var x25 uint64
	var x26 uint64
	x26, x25 = bits.Mul64(arg1[7], (arg2[4] * 0x2))
	var x27 uint64
	var x28 uint64
	x28, x27 = bits.Mul64(arg1[7], (arg2[3] * 0x2))
	var x29 uint64
	var x30 uint64
	x30, x29 = bits.Mul64(arg1[7], (arg2[2] * 0x2))
	var x31 uint64
	var x32 uint64
	x32, x31 = bits.Mul64(arg1[6], (arg2[8] * 0x2))
	var x33 uint64
	var x34 uint64
	x34, x33 = bits.Mul64(arg1[6], (arg2[7] * 0x2))
	var x35 uint64
	var x36 uint64
	x36, x35 = bits.Mul64(arg1[6], (arg2[6] * 0x2))
	var x37 uint64
	var x38 uint64
	x38, x37 = bits.Mul64(arg1[6], (arg2[5] * 0x2))
	var x39 uint64
	var x40 uint64
	x40, x39 = bits.Mul64(arg1[6], (arg2[4] * 0x2))
	var x41 uint64
	var x42 uint64
	x42, x41 = bits.Mul64(arg1[6], (arg2[3] * 0x2))
	var x43 uint64
	var x44 uint64
	x44, x43 = bits.Mul64(arg1[5], (arg2[8] * 0x2))
	var x45 uint64
	var x46 uint64
	x46, x45 = bits.Mul64(arg1[5], (arg2[7] * 0x2))
	var x47 uint64
	var x48 uint64
	x48, x47 = bits.Mul64(arg1[5], (arg2[6] * 0x2))
	var x49 uint64
	var x50 uint64
	x50, x49 = bits.Mul64(arg1[5], (arg2[5] * 0x2))
	var x51 uint64
	var x52 uint64
	x52, x51 = bits.Mul64(arg1[5], (arg2[4] * 0x2))
	var x53 uint64
	var x54 uint64
	x54, x53 = bits.Mul64(arg1[4], (arg2[8] * 0x2))
	var x55 uint64
	var x56 uint64
	x56, x55 = bits.Mul64(arg1[4], (arg2[7] * 0x2))
	var x57 uint64
	var x58 uint64
	x58, x57 = bits.Mul64(arg1[4], (arg2[6] * 0x2))
	var x59 uint64
	var x60 uint64
	x60, x59 = bits.Mul64(arg1[4], (arg2[5] * 0x2))
	var x61 uint64
	var x62 uint64
	x62, x61 = bits.Mul64(arg1[3], (arg2[8] * 0x2))
	var x63 uint64
	var x64 uint64
	x64, x63 = bits.Mul64(arg1[3], (arg2[7] * 0x2))
	var x65 uint64
	var x66 uint64
	x66, x65 = bits.Mul64(arg1[3], (arg2[6] * 0x2))
	var x67 uint64
	var x68 uint64
	x68, x67 = bits.Mul64(arg1[2], (arg2[8] * 0x2))
	var x69 uint64
	var x70 uint64
	x70, x69 = bits.Mul64(arg1[2], (arg2[7] * 0x2))
	var x71 uint64
	var x72 uint64
	x72, x71 = bits.Mul64(arg1[1], (arg2[8] * 0x2))
	var x73 uint64
	var x74 uint64
	x74, x73 = bits.Mul64(arg1[8], arg2[0])
	var x75 uint64
	var x76 uint64
	x76, x75 = bits.Mul64(arg1[7], arg2[1])
	var x77 uint64
	var x78 uint64
	x78, x77 = bits.Mul64(arg1[7], arg2[0])
	var x79 uint64
	var x80 uint64
	x80, x79 = bits.Mul64(arg1[6], arg2[2])
	var x81 uint64
	var x82 uint64
	x82, x81 = bits.Mul64(arg1[6], arg2[1])
	var x83 uint64
	var x84 uint64
	x84, x83 = bits.Mul64(arg1[6], arg2[0])
	var x85 uint64
	var x86 uint64
	x86, x85 = bits.Mul64(arg1[5], arg2[3])
	var x87 uint64
	var x88 uint64
	x88, x87 = bits.Mul64(arg1[5], arg2[2])
	var x89 uint64
	var x90 uint64
	x90, x89 = bits.Mul64(arg1[5], arg2[1])
	var x91 uint64
	var x92 uint64
	x92, x91 = bits.Mul64(arg1[5], arg2[0])
	var x93 uint64
	var x94 uint64
	x94, x93 = bits.Mul64(arg1[4], arg2[4])
	var x95 uint64
	var x96 uint64
	x96, x95 = bits.Mul64(arg1[4], arg2[3])
	var x97 uint64
	var x98 uint64
	x98, x97 = bits.Mul64(arg1[4], arg2[2])
	var x99 uint64
	var x100 uint64
	x100, x99 = bits.Mul64(arg1[4], arg2[1])
	var x101 uint64
	var x102 uint64
	x102, x101 = bits.Mul64(arg1[4], arg2[0])
	var x103 uint64
	var x104 uint64
	x104, x103 = bits.Mul64(arg1[3], arg2[5])
	var x105 uint64
	var x106 uint64
	x106, x105 = bits.Mul64(arg1[3], arg2[4])
	var x107 uint64
	var x108 uint64
	x108, x107 = bits.Mul64(arg1[3], arg2[3])
	var x109 uint64
	var x110 uint64
	x110, x109 = bits.Mul64(arg1[3], arg2[2])
	var x111 uint64
	var x112 uint64
	x112, x111 = bits.Mul64(arg1[3], arg2[1])
	var x113 uint64
	var x114 uint64
	x114, x113 = bits.Mul64(arg1[3], arg2[0])
	var x115 uint64
	var x116 uint64
	x116, x115 = bits.Mul64(arg1[2], arg2[6])
	var x117 uint64
	var x118 uint64
	x118, x117 = bits.Mul64(arg1[2], arg2[5])
	var x119 uint64
	var x120 uint64
	x120, x119 = bits.Mul64(arg1[2], arg2[4])
	var x121 uint64
	var x122 uint64
	x122, x121 = bits.Mul64(arg1[2], arg2[3])
	var x123 uint64
	var x124 uint64
	x124, x123 = bits.Mul64(arg1[2], arg2[2])
	var x125 uint64
	var x126 uint64
	x126, x125 = bits.Mul64(arg1[2], arg2[1])
	var x127 uint64
	var x128 uint64
	x128, x127 = bits.Mul64(arg1[2], arg2[0])
	var x129 uint64
	var x130 uint64
	x130, x129 = bits.Mul64(arg1[1], arg2[7])
	var x131 uint64
	var x132 uint64
	x132, x131 = bits.Mul64(arg1[1], arg2[6])
	var x133 uint64
	var x134 uint64
	x134, x133 = bits.Mul64(arg1[1], arg2[5])
	var x135 uint64
	var x136 uint64
	x136, x135 = bits.Mul64(arg1[1], arg2[4])
	var x137 uint64
	var x138 uint64
	x138, x137 = bits.Mul64(arg1[1], arg2[3])
	var x139 uint64
	var x140 uint64
	x140, x139 = bits.Mul64(arg1[1], arg2[2])
	var x141 uint64
	var x142 uint64
	x142, x141 = bits.Mul64(arg1[1], arg2[1])
	var x143 uint64
	var x144 uint64
	x144, x143 = bits.Mul64(arg1[1], arg2[0])
	var x145 uint64
	var x146 uint64
	x146, x145 = bits.Mul64(arg1[0], arg2[8])
	var x147 uint64
	var x148 uint64
	x148, x147 = bits.Mul64(arg1[0], arg2[7])
	var x149 uint64
	var x150 uint64
	x150, x149 = bits.Mul64(arg1[0], arg2[6])
	var x151 uint64
	var x152 uint64
	x152, x151 = bits.Mul64(arg1[0], arg2[5])
	var x153 uint64
	var x154 uint64
	x154, x153 = bits.Mul64(arg1[0], arg2[4])
	var x155 uint64
	var x156 uint64
	x156, x155 = bits.Mul64(arg1[0], arg2[3])
	var x157 uint64
	var x158 uint64
	x158, x157 = bits.Mul64(arg1[0], arg2[2])
	var x159 uint64
	var x160 uint64
	x160, x159 = bits.Mul64(arg1[0], arg2[1])
	var x161 uint64
	var x162 uint64
	x162, x161 = bits.Mul64(arg1[0], arg2[0])
	var x163 uint64
	var x164 p521Uint1
	x163, x164 = p521AddcarryxU64(x29, x15, 0x0)
	var x165 uint64
	x165, _ = p521AddcarryxU64(x30, x16, x164)
	var x167 uint64
	var x168 p521Uint1
	x167, x168 = p521AddcarryxU64(x41, x163, 0x0)
	var x169 uint64
	x169, _ = p521AddcarryxU64(x42, x165, x168)
	var x171 uint64
	var x172 p521Uint1
	x171, x172 = p521AddcarryxU64(x51, x167, 0x0)
	var x173 uint64
	x173, _ = p521AddcarryxU64(x52, x169, x172)
	var x175 uint64
	var x176 p521Uint1
	x175, x176 = p521AddcarryxU64(x59, x171, 0x0)
	var x177 uint64
	x177, _ = p521AddcarryxU64(x60, x173, x176)
	var x179 uint64
	var x180 p521Uint1
	x179, x180 = p521AddcarryxU64(x65, x175, 0x0)
	var x181 uint64
	x181, _ = p521AddcarryxU64(x66, x177, x180)
	var x183 uint64
	var x184 p521Uint1
	x183, x184 = p521AddcarryxU64(x69, x179, 0x0)
	var x185 uint64
	x185, _ = p521AddcarryxU64(x70, x181, x184)
	var x187 uint64
	var x188 p521Uint1
	x187, x188 = p521AddcarryxU64(x71, x183, 0x0)
	var x189 uint64
	x189, _ = p521AddcarryxU64(x72, x185, x188)
	var x191 uint64
	var x192 p521Uint1
	x191, x192 = p521AddcarryxU64(x161, x187, 0x0)
	var x193 uint64
	x193, _ = p521AddcarryxU64(x162, x189, x192)
	x195 := ((x191 >> 58) | ((x193 << 6) & 0xffffffffffffffff))
	x196 := (x193 >> 58)
	x197 := (x191 & 0x3ffffffffffffff)
	var x198 uint64
	var x199 p521Uint1
	x198, x199 = p521AddcarryxU64(x75, x73, 0x0)
	var x200 uint64
	x200, _ = p521AddcarryxU64(x76, x74, x199)
	var x202 uint64
	var x203 p521Uint1
	x202, x203 = p521AddcarryxU64(x79, x198, 0x0)
	var x204 uint64
	x204, _ = p521AddcarryxU64(x80, x200, x203)
	var x206 uint64
	var x207 p521Uint1
	x206, x207 = p521AddcarryxU64(x85, x202, 0x0)
	var x208 uint64
	x208, _ = p521AddcarryxU64(x86, x204, x207)
	var x210 uint64
	var x211 p521Uint1
	x210, x211 = p521AddcarryxU64(x93, x206, 0x0)
	var x212 uint64
	x212, _ = p521AddcarryxU64(x94, x208, x211)
	var x214 uint64
	var x215 p521Uint1
	x214, x215 = p521AddcarryxU64(x103, x210, 0x0)
	var x216 uint64
	x216, _ = p521AddcarryxU64(x104, x212, x215)
	var x218 uint64
	var x219 p521Uint1
	x218, x219 = p521AddcarryxU64(x115, x214, 0x0)
	var x220 uint64
	x220, _ = p521AddcarryxU64(x116, x216, x219)
	var x222 uint64
	var x223 p521Uint1
	x222, x223 = p521AddcarryxU64(x129, x218, 0x0)
	var x224 uint64
	x224, _ = p521AddcarryxU64(x130, x220, x223)
	var x226 uint64
	var x227 p521Uint1
	x226, x227 = p521AddcarryxU64(x145, x222, 0x0)
	var x228 uint64
	x228, _ = p521AddcarryxU64(x146, x224, x227)
	var x230 uint64
	var x231 p521Uint1
	x230, x231 = p521AddcarryxU64(x77, x1, 0x0)
	var x232 uint64
	x232, _ = p521AddcarryxU64(x78, x2, x231)
	var x234 uint64
	var x235 p521Uint1
	x234, x235 = p521AddcarryxU64(x81, x230, 0x0)
	var x236 uint64
	x236, _ = p521AddcarryxU64(x82, x232, x235)
	var x238 uint64
	var x239 p521Uint1
	x238, x239 = p521AddcarryxU64(x87, x234, 0x0)
	var x240 uint64
	x240, _ = p521AddcarryxU64(x88, x236, x239)
	var x242 uint64
	var x243 p521Uint1
	x242, x243 = p521AddcarryxU64(x95, x238, 0x0)
	var x244 uint64
	x244, _ = p521AddcarryxU64(x96, x240, x243)
	var x246 uint64
	var x247 p521Uint1
	x246, x247 = p521AddcarryxU64(x105, x242, 0x0)
	var x248 uint64
	x248, _ = p521AddcarryxU64(x106, x244, x247)
	var x250 uint64
	var x251 p521Uint1
	x250, x251 = p521AddcarryxU64(x117, x246, 0x0)
	var x252 uint64
	x252, _ = p521AddcarryxU64(x118, x248, x251)
	var x254 uint64
	var x255 p521Uint1
	x254, x255 = p521AddcarryxU64(x131, x250, 0x0)
	var x256 uint64
	x256, _ = p521AddcarryxU64(x132, x252, x255)
	var x258 uint64
	var x259 p521Uint1
	x258, x259 = p521AddcarryxU64(x147, x254, 0x0)
	var x260 uint64
	x260, _ = p521AddcarryxU64(x148, x256, x259)
	var x262 uint64
	var x263 p521Uint1
	x262, x263 = p521AddcarryxU64(x17, x3, 0x0)
	var x264 uint64
	x264, _ = p521AddcarryxU64(x18, x4, x263)
	var x266 uint64
	var x267 p521Uint1
	x266, x267 = p521AddcarryxU64(x83, x262, 0x0)
	var x268 uint64
	x268, _ = p521AddcarryxU64(x84, x264, x267)
	var x270 uint64
	var x271 p521Uint1
	x270, x271 = p521AddcarryxU64(x89, x266, 0x0)
	var x272 uint64
	x272, _ = p521AddcarryxU64(x90, x268, x271)
	var x274 uint64
	var x275 p521Uint1
	x274, x275 = p521AddcarryxU64(x97, x270, 0x0)
	var x276 uint64
	x276, _ = p521AddcarryxU64(x98, x272, x275)
	var x278 uint64
	var x279 p521Uint1
	x278, x279 = p521AddcarryxU64(x107, x274, 0x0)
	var x280 uint64
	x280, _ = p521AddcarryxU64(x108, x276, x279)
	var x282 uint64
	var x283 p521Uint1
	x282, x283 = p521AddcarryxU64(x119, x278, 0x0)
	var x284 uint64
	x284, _ = p521AddcarryxU64(x120, x280, x283)
	var x286 uint64
	var x287 p521Uint1
	x286, x287 = p521AddcarryxU64(x133, x282, 0x0)
	var x288 uint64
	x288, _ = p521AddcarryxU64(x134, x284, x287)
	var x290 uint64
	var x291 p521Uint1
	x290, x291 = p521AddcarryxU64(x149, x286, 0x0)
	var x292 uint64
	x292, _ = p521AddcarryxU64(x150, x288, x291)
	var x294 uint64
	var x295 p521Uint1
	x294, x295 = p521AddcarryxU64(x19, x5, 0x0)
	var x296 uint64
	x296, _ = p521AddcarryxU64(x20, x6, x295)
	var x298 uint64
	var x299 p521Uint1
	x298, x299 = p521AddcarryxU64(x31, x294, 0x0)
	var x300 uint64
	x300, _ = p521AddcarryxU64(x32, x296, x299)
	var x302 uint64
	var x303 p521Uint1
	x302, x303 = p521AddcarryxU64(x91, x298, 0x0)
	var x304 uint64
	x304, _ = p521AddcarryxU64(x92, x300, x303)
	var x306 uint64
	var x307 p521Uint1
	x306, x307 = p521AddcarryxU64(x99, x302, 0x0)
	var x308 uint64
	x308, _ = p521AddcarryxU64(x100, x304, x307)
	var x310 uint64
	var x311 p521Uint1
	x310, x311 = p521AddcarryxU64(x109, x306, 0x0)
	var x312 uint64
	x312, _ = p521AddcarryxU64(x110, x308, x311)
	var x314 uint64
	var x315 p521Uint1
	x314, x315 = p521AddcarryxU64(x121, x310, 0x0)
	var x316 uint64
	x316, _ = p521AddcarryxU64(x122, x312, x315)
	var x318 uint64
	var x319 p521Uint1
	x318, x319 = p521AddcarryxU64(x135, x314, 0x0)
	var x320 uint64
	x320, _ = p521AddcarryxU64(x136, x316, x319)
	var x322 uint64
	var x323 p521Uint1
	x322, x323 = p521AddcarryxU64(x151, x318, 0x0)
	var x324 uint64
	x324, _ = p521AddcarryxU64(x152, x320, x323)
	var x326 uint64
	var x327 p521Uint1
	x326, x327 = p521AddcarryxU64(x21, x7, 0x0)
	var x328 uint64
	x328, _ = p521AddcarryxU64(x22, x8, x327)
	var x330 uint64
	var x331 p521Uint1
	x330, x331 = p521AddcarryxU64(x33, x326, 0x0)
	var x332 uint64
	x332, _ = p521AddcarryxU64(x34, x328, x331)
	var x334 uint64
	var x335 p521Uint1
	x334, x335 = p521AddcarryxU64(x43, x330, 0x0)
	var x336 uint64
	x336, _ = p521AddcarryxU64(x44, x332, x335)
	var x338 uint64
	var x339 p521Uint1
	x338, x339 = p521AddcarryxU64(x101, x334, 0x0)
	var x340 uint64
	x340, _ = p521AddcarryxU64(x102, x336, x339)
	var x342 uint64
	var x343 p521Uint1
	x342, x343 = p521AddcarryxU64(x111, x338, 0x0)
	var x344 uint64
	x344, _ = p521AddcarryxU64(x112, x340, x343)
	var x346 uint64
	var x347 p521Uint1
	x346, x347 = p521AddcarryxU64(x123, x342, 0x0)
	var x348 uint64
	x348, _ = p521AddcarryxU64(x124, x344, x347)
	var x350 uint64
	var x351 p521Uint1
	x350, x351 = p521AddcarryxU64(x137, x346, 0x0)
	var x352 uint64
	x352, _ = p521AddcarryxU64(x138, x348, x351)
	var x354 uint64
	var x355 p521Uint1
	x354, x355 = p521AddcarryxU64(x153, x350, 0x0)
	var x356 uint64
	x356, _ = p521AddcarryxU64(x154, x352, x355)
	var x358 uint64
	var x359 p521Uint1
	x358, x359 = p521AddcarryxU64(x23, x9, 0x0)
	var x360 uint64
	x360, _ = p521AddcarryxU64(x24, x10, x359)
	var x362 uint64
	var x363 p521Uint1
	x362, x363 = p521AddcarryxU64(x35, x358, 0x0)
	var x364 uint64
	x364, _ = p521AddcarryxU64(x36, x360, x363)
	var x366 uint64
	var x367 p521Uint1
	x366, x367 = p521AddcarryxU64(x45, x362, 0x0)
	var x368 uint64
	x368, _ = p521AddcarryxU64(x46, x364, x367)
	var x370 uint64
	var x371 p521Uint1
	x370, x371 = p521AddcarryxU64(x53, x366, 0x0)
	var x372 uint64
	x372, _ = p521AddcarryxU64(x54, x368, x371)
	var x374 uint64
	var x375 p521Uint1
	x374, x375 = p521AddcarryxU64(x113, x370, 0x0)
	var x376 uint64
	x376, _ = p521AddcarryxU64(x114, x372, x375)
	var x378 uint64
	var x379 p521Uint1
	x378, x379 = p521AddcarryxU64(x125, x374, 0x0)
	var x380 uint64
	x380, _ = p521AddcarryxU64(x126, x376, x379)
	var x382 uint64
	var x383 p521Uint1
	x382, x383 = p521AddcarryxU64(x139, x378, 0x0)
	var x384 uint64
	x384, _ = p521AddcarryxU64(x140, x380, x383)
	var x386 uint64
	var x387 p521Uint1
	x386, x387 = p521AddcarryxU64(x155, x382, 0x0)
	var x388 uint64
	x388, _ = p521AddcarryxU64(x156, x384, x387)
	var x390 uint64
	var x391 p521Uint1
	x390, x391 = p521AddcarryxU64(x25, x11, 0x0)
	var x392 uint64
	x392, _ = p521AddcarryxU64(x26, x12, x391)
	var x394 uint64
	var x395 p521Uint1
	x394, x395 = p521AddcarryxU64(x37, x390, 0x0)
	var x396 uint64
	x396, _ = p521AddcarryxU64(x38, x392, x395)
	var x398 uint64
	var x399 p521Uint1
	x398, x399 = p521AddcarryxU64(x47, x394, 0x0)
	var x400 uint64
	x400, _ = p521AddcarryxU64(x48, x396, x399)
	var x402 uint64
	var x403 p521Uint1
	x402, x403 = p521AddcarryxU64(x55, x398, 0x0)
	var x404 uint64
	x404, _ = p521AddcarryxU64(x56, x400, x403)
	var x406 uint64
	var x407 p521Uint1
	x406, x407 = p521AddcarryxU64(x61, x402, 0x0)
	var x408 uint64
	x408, _ = p521AddcarryxU64(x62, x404, x407)
	var x410 uint64
	var x411 p521Uint1
	x410, x411 = p521AddcarryxU64(x127, x406, 0x0)
	var x412 uint64
	x412, _ = p521AddcarryxU64(x128, x408, x411)
	var x414 uint64
	var x415 p521Uint1
	x414, x415 = p521AddcarryxU64(x141, x410, 0x0)
	var x416 uint64
	x416, _ = p521AddcarryxU64(x142, x412, x415)
	var x418 uint64
	var x419 p521Uint1
	x418, x419 = p521AddcarryxU64(x157, x414, 0x0)
	var x420 uint64
	x420, _ = p521AddcarryxU64(x158, x416, x419)
	var x422 uint64
	var x423 p521Uint1
	x422, x423 = p521AddcarryxU64(x27, x13, 0x0)
	var x424 uint64
	x424, _ = p521AddcarryxU64(x28, x14, x423)
	var x426 uint64
	var x427 p521Uint1
	x426, x427 = p521AddcarryxU64(x39, x422, 0x0)
	var x428 uint64
	x428, _ = p521AddcarryxU64(x40, x424, x427)
	var x430 uint64
	var x431 p521Uint1
	x430, x431 = p521AddcarryxU64(x49, x426, 0x0)
	var x432 uint64
	x432, _ = p521AddcarryxU64(x50, x428, x431)
	var x434 uint64
	var x435 p521Uint1
	x434, x435 = p521AddcarryxU64(x57, x430, 0x0)
	var x436 uint64
	x436, _ = p521AddcarryxU64(x58, x432, x435)
	var x438 uint64
	var x439 p521Uint1
	x438, x439 = p521AddcarryxU64(x63, x434, 0x0)
	var x440 uint64
	x440, _ = p521AddcarryxU64(x64, x436, x439)
	var x442 uint64
	var x443 p521Uint1
	x442, x443 = p521AddcarryxU64(x67, x438, 0x0)
	var x444 uint64
	x444, _ = p521AddcarryxU64(x68, x440, x443)
	var x446 uint64
	var x447 p521Uint1
	x446, x447 = p521AddcarryxU64(x143, x442, 0x0)
	var x448 uint64
	x448, _ = p521AddcarryxU64(x144, x444, x447)
	var x450 uint64
	var x451 p521Uint1
	x450, x451 = p521AddcarryxU64(x159, x446, 0x0)
	var x452 uint64
	x452, _ = p521AddcarryxU64(x160, x448, x451)
	var x454 uint64
	var x455 p521Uint1
	x454, x455 = p521AddcarryxU64(x195, x450, 0x0)
	var x456 uint64
	x456, _ = p521AddcarryxU64(x196, x452, x455)
	x458 := ((x454 >> 58) | ((x456 << 6) & 0xffffffffffffffff))
	x459 := (x456 >> 58)
	x460 := (x454 & 0x3ffffffffffffff)
	var x461 uint64
	var x462 p521Uint1
	x461, x462 = p521AddcarryxU64(x458, x418, 0x0)
	var x463 uint64
	x463, _ = p521AddcarryxU64(x459, x420, x462)
	x465 := ((x461 >> 58) | ((x463 << 6) & 0xffffffffffffffff))
	x466 := (x463 >> 58)
	x467 := (x461 & 0x3ffffffffffffff)
	var x468 uint64
	var x469 p521Uint1
	x468, x469 = p521AddcarryxU64(x465, x386, 0x0)
	var x470 uint64
	x470, _ = p521AddcarryxU64(x466, x388, x469)
	x472 := ((x468 >> 58) | ((x470 << 6) & 0xffffffffffffffff))
	x473 := (x470 >> 58)
	x474 := (x468 & 0x3ffffffffffffff)
	var x475 uint64
	var x476 p521Uint1
	x475, x476 = p521AddcarryxU64(x472, x354, 0x0)
	var x477 uint64
	x477, _ = p521AddcarryxU64(x473, x356, x476)
	x479 := ((x475 >> 58) | ((x477 << 6) & 0xffffffffffffffff))
	x480 := (x477 >> 58)
	x481 := (x475 & 0x3ffffffffffffff)
	var x482 uint64
	var x483 p521Uint1
	x482, x483 = p521AddcarryxU64(x479, x322, 0x0)
	var x484 uint64
	x484, _ = p521AddcarryxU64(x480, x324, x483)
	x486 := ((x482 >> 58) | ((x484 << 6) & 0xffffffffffffffff))
	x487 := (x484 >> 58)
	x488 := (x482 & 0x3ffffffffffffff)
	var x489 uint64
	var x490 p521Uint1
	x489, x490 = p521AddcarryxU64(x486, x290, 0x0)
	var x491 uint64
	x491, _ = p521AddcarryxU64(x487, x292, x490)
	x493 := ((x489 >> 58) | ((x491 << 6) & 0xffffffffffffffff))
	x494 := (x491 >> 58)
	x495 := (x489 & 0x3ffffffffffffff)
	var x496 uint64
	var x497 p521Uint1
	x496, x497 = p521AddcarryxU64(x493, x258, 0x0)
	var x498 uint64
	x498, _ = p521AddcarryxU64(x494, x260, x497)
	x500 := ((x496 >> 58) | ((x498 << 6) & 0xffffffffffffffff))
	x501 := (x498 >> 58)
	x502 := (x496 & 0x3ffffffffffffff)
	var x503 uint64
	var x504 p521Uint1
	x503, x504 = p521AddcarryxU64(x500, x226, 0x0)
	var x505 uint64
	x505, _ = p521AddcarryxU64(x501, x228, x504)
	x507 := ((x503 >> 57) | ((x505 << 7) & 0xffffffffffffffff))
	x508 := (x505 >> 57)
	x509 := (x503 & 0x1ffffffffffffff)
	var x510 uint64
	var x511 p521Uint1
	x510, x511 = p521AddcarryxU64(x197, x507, 0x0)
	x512 := (uint64(x511) + x508)
	x513 := ((x510 >> 58) | ((x512 << 6) & 0xffffffffffffffff))
	x514 := (x510 & 0x3ffffffffffffff)
	x515 := (x513 + x460)
	x516 := p521Uint1((x515 >> 58))
	x517 := (x515 & 0x3ffffffffffffff)
	x518 := (uint64(x516) + x467)
	out1[0] = x514
	out1[1] = x517
	out1[2] = x518
	out1[3] = x474
	out1[4] = x481
	out1[5] = x488
	out1[6] = x495
	out1[7] = x502
	out1[8] = x509
}

// p521CarrySquare squares a field element and reduces the result.
//
// Postconditions:
//   eval out1 mod m = (eval arg1 * eval arg1) mod m
//
// Input Bounds:
//   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
// Output Bounds:
//   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
func p521CarrySquare(out1 *[9]uint64, arg1 *[9]uint64) {
	x1 := arg1[8]
	x2 := (x1 * 0x2)
	x3 := (arg1[8] * 0x2)
	x4 := arg1[7]
	x5 := (x4 * 0x2)
	x6 := (arg1[7] * 0x2)
	x7 := arg1[6]
	x8 := (x7 * 0x2)
	x9 := (arg1[6] * 0x2)
	x10 := arg1[5]
	x11 := (x10 * 0x2)
	x12 := (arg1[5] * 0x2)
	x13 := (arg1[4] * 0x2)
	x14 := (arg1[3] * 0x2)
	x15 := (arg1[2] * 0x2)
	x16 := (arg1[1] * 0x2)
	var x17 uint64
	var x18 uint64
	x18, x17 = bits.Mul64(arg1[8], (x1 * 0x2))
	var x19 uint64
	var x20 uint64
	x20, x19 = bits.Mul64(arg1[7], (x2 * 0x2))
	var x21 uint64
	var x22 uint64
	x22, x21 = bits.Mul64(arg1[7], (x4 * 0x2))
	var x23 uint64
	var x24 uint64
	x24, x23 = bits.Mul64(arg1[6], (x2 * 0x2))
	var x25 uint64
	var x26 uint64
	x26, x25 = bits.Mul64(arg1[6], (x5 * 0x2))
	var x27 uint64
	var x28 uint64
	x28, x27 = bits.Mul64(arg1[6], (x7 * 0x2))
	var x29 uint64
	var x30 uint64
	x30, x29 = bits.Mul64(arg1[5], (x2 * 0x2))
	var x31 uint64
	var x32 uint64
	x32, x31 = bits.Mul64(arg1[5], (x5 * 0x2))
	var x33 uint64
	var x34 uint64
	x34, x33 = bits.Mul64(arg1[5], (x8 * 0x2))
	var x35 uint64
	var x36 uint64
	x36, x35 = bits.Mul64(arg1[5], (x10 * 0x2))
	var x37 uint64
	var x38 uint64
	x38, x37 = bits.Mul64(arg1[4], (x2 * 0x2))
	var x39 uint64
	var x40 uint64
	x40, x39 = bits.Mul64(arg1[4], (x5 * 0x2))
	var x41 uint64
	var x42 uint64
	x42, x41 = bits.Mul64(arg1[4], (x8 * 0x2))
	var x43 uint64
	var x44 uint64
	x44, x43 = bits.Mul64(arg1[4], (x11 * 0x2))
	var x45 uint64
	var x46 uint64
	x46, x45 = bits.Mul64(arg1[4], arg1[4])
	var x47 uint64
	var x48 uint64
	x48, x47 = bits.Mul64(arg1[3], (x2 * 0x2))
	var x49 uint64
	var x50 uint64
	x50, x49 = bits.Mul64(arg1[3], (x5 * 0x2))
	var x51 uint64
	var x52 uint64
	x52, x51 = bits.Mul64(arg1[3], (x8 * 0x2))
	var x53 uint64
	var x54 uint64
	x54, x53 = bits.Mul64(arg1[3], x12)
	var x55 uint64
	var x56 uint64
	x56, x55 = bits.Mul64(arg1[3], x13)
	var x57 uint64
	var x58 uint64
	x58, x57 = bits.Mul64(arg1[3], arg1[3])
	var x59 uint64
	var x60 uint64
	x60, x59 = bits.Mul64(arg1[2], (x2 * 0x2))
	var x61 uint64
	var x62 uint64
	x62, x61 = bits.Mul64(arg1[2], (x5 * 0x2))
	var x63 uint64
	var x64 uint64
	x64, x63 = bits.Mul64(arg1[2], x9)
	var x65 uint64
	var x66 uint64
	x66, x65 = bits.Mul64(arg1[2], x12)
	var x67 uint64
	var x68 uint64
	x68, x67 = bits.Mul64(arg1[2], x13)
	var x69 uint64
	var x70 uint64
	x70, x69 = bits.Mul64(arg1[2], x14)
	var x71 uint64
	var x72 uint64
	x72, x71 = bits.Mul64(arg1[2], arg1[2])
	var x73 uint64
	var x74 uint64
	x74, x73 = bits.Mul64(arg1[1], (x2 * 0x2))
	var x75 uint64
	var x76 uint64
	x76, x75 = bits.Mul64(arg1[1], x6)
	var x77 uint64
	var x78 uint64
	x78, x77 = bits.Mul64(arg1[1], x9)
	var x79 uint64
	var x80 uint64
	x80, x79 = bits.Mul64(arg1[1], x12)
	var x81 uint64
	var x82 uint64
	x82, x81 = bits.Mul64(arg1[1], x13)
	var x83 uint64
	var x84 uint64
	x84, x83 = bits.Mul64(arg1[1], x14)
	var x85 uint64
	var x86 uint64
	x86, x85 = bits.Mul64(arg1[1], x15)
	var x87 uint64
	var x88 uint64
	x88, x87 = bits.Mul64(arg1[1], arg1[1])
	var x89 uint64
	var x90 uint64
	x90, x89 = bits.Mul64(arg1[0], x3)
	var x91 uint64
	var x92 uint64
	x92, x91 = bits.Mul64(arg1[0], x6)
	var x93 uint64
	var x94 uint64
	x94, x93 = bits.Mul64(arg1[0], x9)
	var x95 uint64
	var x96 uint64
	x96, x95 = bits.Mul64(arg1[0], x12)
	var x97 uint64
	var x98 uint64
	x98, x97 = bits.Mul64(arg1[0], x13)
	var x99 uint64
	var x100 uint64
	x100, x99 = bits.Mul64(arg1[0], x14)
	var x101 uint64
	var x102 uint64
	x102, x101 = bits.Mul64(arg1[0], x15)
	var x103 uint64
	var x104 uint64
	x104, x103 = bits.Mul64(arg1[0], x16)
	var x105 uint64
	var x106 uint64
	x106, x105 = bits.Mul64(arg1[0], arg1[0])
	var x107 uint64
	var x108 p521Uint1
	x107, x108 = p521AddcarryxU64(x51, x43, 0x0)
	var x109 uint64
	x109, _ = p521AddcarryxU64(x52, x44, x108)
	var x111 uint64
	var x112 p521Uint1
	x111, x112 = p521AddcarryxU64(x61, x107, 0x0)
	var x113 uint64
	x113, _ = p521AddcarryxU64(x62, x109, x112)
	var x115 uint64
	var x116 p521Uint1
	x115, x116 = p521AddcarryxU64(x73, x111, 0x0)
	var x117 uint64
	x117, _ = p521AddcarryxU64(x74, x113, x116)
	var x119 uint64
	var x120 p521Uint1
	x119, x120 = p521AddcarryxU64(x105, x115, 0x0)
	var x121 uint64
	x121, _ = p521AddcarryxU64(x106, x117, x120)
	x123 := ((x119 >> 58) | ((x121 << 6) & 0xffffffffffffffff))
	x124 := (x121 >> 58)
	x125 := (x119 & 0x3ffffffffffffff)
	var x126 uint64
	var x127 p521Uint1
	x126, x127 = p521AddcarryxU64(x53, x45, 0x0)
	var x128 uint64
	x128, _ = p521AddcarryxU64(x54, x46, x127)
	var x130 uint64
	var x131 p521Uint1
	x130, x131 = p521AddcarryxU64(x63, x126, 0x0)
	var x132 uint64
	x132, _ = p521AddcarryxU64(x64, x128, x131)
	var x134 uint64
	var x135 p521Uint1
	x134, x135 = p521AddcarryxU64(x75, x130, 0x0)
	var x136 uint64
	x136, _ = p521AddcarryxU64(x76, x132, x135)
	var x138 uint64
	var x139 p521Uint1
	x138, x139 = p521AddcarryxU64(x89, x134, 0x0)
	var x140 uint64
	x140, _ = p521AddcarryxU64(x90, x136, x139)
	var x142 uint64
	var x143 p521Uint1
	x142, x143 = p521AddcarryxU64(x55, x17, 0x0)
	var x144 uint64
	x144, _ = p521AddcarryxU64(x56, x18, x143)
	var x146 uint64
	var x147 p521Uint1
	x146, x147 = p521AddcarryxU64(x65, x142, 0x0)
	var x148 uint64
	x148, _ = p521AddcarryxU64(x66, x144, x147)
	var x150 uint64
	var x151 p521Uint1
	x150, x151 = p521AddcarryxU64(x77, x146, 0x0)
	var x152 uint64
	x152, _ = p521AddcarryxU64(x78, x148, x151)
	var x154 uint64
	var x155 p521Uint1
	x154, x155 = p521AddcarryxU64(x91, x150, 0x0)
	var x156 uint64
	x156, _ = p521AddcarryxU64(x92, x152, x155)
	var x158 uint64
	var x159 p521Uint1
	x158, x159 = p521AddcarryxU64(x57, x19, 0x0)
	var x160 uint64
	x160, _ = p521AddcarryxU64(x58, x20, x159)
	var x162 uint64
	var x163 p521Uint1
	x162, x163 = p521AddcarryxU64(x67, x158, 0x0)
	var x164 uint64
	x164, _ = p521AddcarryxU64(x68, x160, x163)
	var x166 uint64
	var x167 p521Uint1
	x166, x167 = p521AddcarryxU64(x79, x162, 0x0)
	var x168 uint64
	x168, _ = p521AddcarryxU64(x80, x164, x167)
	var x170 uint64
	var x171 p521Uint1
	x170, x171 = p521AddcarryxU64(x93, x166, 0x0)
	var x172 uint64
	x172, _ = p521AddcarryxU64(x94, x168, x171)
	var x174 uint64
	var x175 p521Uint1
	x174, x175 = p521AddcarryxU64(x23, x21, 0x0)
	var x176 uint64
	x176, _ = p521AddcarryxU64(x24, x22, x175)
	var x178 uint64
	var x179 p521Uint1
	x178, x179 = p521AddcarryxU64(x69, x174, 0x0)
	var x180 uint64
	x180, _ = p521AddcarryxU64(x70, x176, x179)
	var x182 uint64
	var x183 p521Uint1
	x182, x183 = p521AddcarryxU64(x81, x178, 0x0)
	var x184 uint64
	x184, _ = p521AddcarryxU64(x82, x180, x183)
	var x186 uint64
	var x187 p521Uint1
	x186, x187 = p521AddcarryxU64(x95, x182, 0x0)
	var x188 uint64
	x188, _ = p521AddcarryxU64(x96, x184, x187)
	var x190 uint64
	var x191 p521Uint1
	x190, x191 = p521AddcarryxU64(x29, x25, 0x0)
	var x192 uint64
	x192, _ = p521AddcarryxU64(x30, x26, x191)
	var x194 uint64
	var x195 p521Uint1
	x194, x195 = p521AddcarryxU64(x71, x190, 0x0)
	var x196 uint64
	x196, _ = p521AddcarryxU64(x72, x192, x195)
	var x198 uint64
	var x199 p521Uint1
	x198, x199 = p521AddcarryxU64(x83, x194, 0x0)
	var x200 uint64
	x200, _ = p521AddcarryxU64(x84, x196, x199)
	var x202 uint64
	var x203 p521Uint1
	x202, x203 = p521AddcarryxU64(x97, x198, 0x0)
	var x204 uint64
	x204, _ = p521AddcarryxU64(x98, x200, x203)
	var x206 uint64
	var x207 p521Uint1
	x206, x207 = p521AddcarryxU64(x31, x27, 0x0)
	var x208 uint64
	x208, _ = p521AddcarryxU64(x32, x28, x207)
	var x210 uint64
	var x211 p521Uint1
	x210, x211 = p521AddcarryxU64(x37, x206, 0x0)
	var x212 uint64
	x212, _ = p521AddcarryxU64(x38, x208, x211)
	var x214 uint64
	var x215 p521Uint1
	x214, x215 = p521AddcarryxU64(x85, x210, 0x0)
	var x216 uint64
	x216, _ = p521AddcarryxU64(x86, x212, x215)
	var x218 uint64
	var x219 p521Uint1
	x218, x219 = p521AddcarryxU64(x99, x214, 0x0)
	var x220 uint64
	x220, _ = p521AddcarryxU64(x100, x216, x219)
	var x222 uint64
	var x223 p521Uint1
	x222, x223 = p521AddcarryxU64(x39, x33, 0x0)
	var x224 uint64
	x224, _ = p521AddcarryxU64(x40, x34, x223)
	var x226 uint64
	var x227 p521Uint1
	x226, x227 = p521AddcarryxU64(x47, x222, 0x0)
	var x228 uint64
	x228, _ = p521AddcarryxU64(x48, x224, x227)
	var x230 uint64
	var x231 p521Uint1
	x230, x231 = p521AddcarryxU64(x87, x226, 0x0)
	var x232 uint64
	x232, _ = p521AddcarryxU64(x88, x228, x231)
	var x234 uint64
	var x235 p521Uint1
	x234, x235 = p521AddcarryxU64(x101, x230, 0x0)
	var x236 uint64
	x236, _ = p521AddcarryxU64(x102, x232, x235)
	var x238 uint64
	var x239 p521Uint1
	x238, x239 = p521AddcarryxU64(x41, x35, 0x0)
	var x240 uint64
	x240, _ = p521AddcarryxU64(x42, x36, x239)
	var x242 uint64
	var x243 p521Uint1
	x242, x243 = p521AddcarryxU64(x49, x238, 0x0)
	var x244 uint64
	x244, _ = p521AddcarryxU64(x50, x240, x243)
	var x246 uint64
	var x247 p521Uint1
	x246, x247 = p521AddcarryxU64(x59, x242, 0x0)
	var x248 uint64
	x248, _ = p521AddcarryxU64(x60, x244, x247)
	var x250 uint64
	var x251 p521Uint1
	x250, x251 = p521AddcarryxU64(x103, x246, 0x0)
	var x252 uint64
	x252, _ = p521AddcarryxU64(x104, x248, x251)
	var x254 uint64
	var x255 p521Uint1
	x254, x255 = p521AddcarryxU64(x123, x250, 0x0)
	var x256 uint64
	x256, _ = p521AddcarryxU64(x124, x252, x255)
	x258 := ((x254 >> 58) | ((x256 << 6) & 0xffffffffffffffff))
	x259 := (x256 >> 58)
	x260 := (x254 & 0x3ffffffffffffff)
	var x261 uint64
	var x262 p521Uint1
	x261, x262 = p521AddcarryxU64(x258, x234, 0x0)
	var x263 uint64
	x263, _ = p521AddcarryxU64(x259, x236, x262)
	x265 := ((x261 >> 58) | ((x263 << 6) & 0xffffffffffffffff))
	x266 := (x263 >> 58)
	x267 := (x261 & 0x3ffffffffffffff)
	var x268 uint64
	var x269 p521Uint1
	x268, x269 = p521AddcarryxU64(x265, x218, 0x0)
	var x270 uint64
	x270, _ = p521AddcarryxU64(x266, x220, x269)
	x272 := ((x268 >> 58) | ((x270 << 6) & 0xffffffffffffffff))
	x273 := (x270 >> 58)
	x274 := (x268 & 0x3ffffffffffffff)
	var x275 uint64
	var x276 p521Uint1
	x275, x276 = p521AddcarryxU64(x272, x202, 0x0)
	var x277 uint64
	x277, _ = p521AddcarryxU64(x273, x204, x276)
	x279 := ((x275 >> 58) | ((x277 << 6) & 0xffffffffffffffff))
	x280 := (x277 >> 58)
	x281 := (x275 & 0x3ffffffffffffff)
	var x282 uint64
	var x283 p521Uint1
	x282, x283 = p521AddcarryxU64(x279, x186, 0x0)
	var x284 uint64
	x284, _ = p521AddcarryxU64(x280, x188, x283)
	x286 := ((x282 >> 58) | ((x284 << 6) & 0xffffffffffffffff))
	x287 := (x284 >> 58)
	x288 := (x282 & 0x3ffffffffffffff)
	var x289 uint64
	var x290 p521Uint1
	x289, x290 = p521AddcarryxU64(x286, x170, 0x0)
	var x291 uint64
	x291, _ = p521AddcarryxU64(x287, x172, x290)
	x293 := ((x289 >> 58) | ((x291 << 6) & 0xffffffffffffffff))
	x294 := (x291 >> 58)
	x295 := (x289 & 0x3ffffffffffffff)
	var x296 uint64
	var x297 p521Uint1
	x296, x297 = p521AddcarryxU64(x293, x154, 0x0)
	var x298 uint64
	x298, _ = p521AddcarryxU64(x294, x156, x297)
	x300 := ((x296 >> 58) | ((x298 << 6) & 0xffffffffffffffff))
	x301 := (x298 >> 58)
	x302 := (x296 & 0x3ffffffffffffff)
	var x303 uint64
	var x304 p521Uint1
	x303, x304 = p521AddcarryxU64(x300, x138, 0x0)
	var x305 uint64
	x305, _ = p521AddcarryxU64(x301, x140, x304)
	x307 := ((x303 >> 57) | ((x305 << 7) & 0xffffffffffffffff))
	x308 := (x305 >> 57)
	x309 := (x303 & 0x1ffffffffffffff)
	var x310 uint64
	var x311 p521Uint1
	x310, x311 = p521AddcarryxU64(x125, x307, 0x0)
	x312 := (uint64(x311) + x308)
	x313 := ((x310 >> 58) | ((x312 << 6) & 0xffffffffffffffff))
	x314 := (x310 & 0x3ffffffffffffff)
	x315 := (x313 + x260)
	x316 := p521Uint1((x315 >> 58))
	x317 := (x315 & 0x3ffffffffffffff)
	x318 := (uint64(x316) + x267)
	out1[0] = x314
	out1[1] = x317
	out1[2] = x318
	out1[3] = x274
	out1[4] = x281
	out1[5] = x288
	out1[6] = x295
	out1[7] = x302
	out1[8] = x309
}

// p521Carry reduces a field element.
//
// Postconditions:
//   eval out1 mod m = eval arg1 mod m
//
// Input Bounds:
//   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
// Output Bounds:
//   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
func p521Carry(out1 *[9]uint64, arg1 *[9]uint64) {
	x1 := arg1[0]
	x2 := ((x1 >> 58) + arg1[1])
	x3 := ((x2 >> 58) + arg1[2])
	x4 := ((x3 >> 58) + arg1[3])
	x5 := ((x4 >> 58) + arg1[4])
	x6 := ((x5 >> 58) + arg1[5])
	x7 := ((x6 >> 58) + arg1[6])
	x8 := ((x7 >> 58) + arg1[7])
	x9 := ((x8 >> 58) + arg1[8])
	x10 := ((x1 & 0x3ffffffffffffff) + (x9 >> 57))
	x11 := (uint64(p521Uint1((x10 >> 58))) + (x2 & 0x3ffffffffffffff))
	x12 := (x10 & 0x3ffffffffffffff)
	x13 := (x11 & 0x3ffffffffffffff)
	x14 := (uint64(p521Uint1((x11 >> 58))) + (x3 & 0x3ffffffffffffff))
	x15 := (x4 & 0x3ffffffffffffff)
	x16 := (x5 & 0x3ffffffffffffff)
	x17 := (x6 & 0x3ffffffffffffff)
	x18 := (x7 & 0x3ffffffffffffff)
	x19 := (x8 & 0x3ffffffffffffff)
	x20 := (x9 & 0x1ffffffffffffff)
	out1[0] = x12
	out1[1] = x13
	out1[2] = x14
	out1[3] = x15
	out1[4] = x16
	out1[5] = x17
	out1[6] = x18
	out1[7] = x19
	out1[8] = x20
}

// p521Add adds two field elements.
//
// Postconditions:
//   eval out1 mod m = (eval arg1 + eval arg2) mod m
//
// Input Bounds:
//   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
//   arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
// Output Bounds:
//   out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
func p521Add(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
	x1 := (arg1[0] + arg2[0])
	x2 := (arg1[1] + arg2[1])
	x3 := (arg1[2] + arg2[2])
	x4 := (arg1[3] + arg2[3])
	x5 := (arg1[4] + arg2[4])
	x6 := (arg1[5] + arg2[5])
	x7 := (arg1[6] + arg2[6])
	x8 := (arg1[7] + arg2[7])
	x9 := (arg1[8] + arg2[8])
	out1[0] = x1
	out1[1] = x2
	out1[2] = x3
	out1[3] = x4
	out1[4] = x5
	out1[5] = x6
	out1[6] = x7
	out1[7] = x8
	out1[8] = x9
}

// p521Sub subtracts two field elements.
//
// Postconditions:
//   eval out1 mod m = (eval arg1 - eval arg2) mod m
//
// Input Bounds:
//   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
//   arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
// Output Bounds:
//   out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
func p521Sub(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
	x1 := ((0x7fffffffffffffe + arg1[0]) - arg2[0])
	x2 := ((0x7fffffffffffffe + arg1[1]) - arg2[1])
	x3 := ((0x7fffffffffffffe + arg1[2]) - arg2[2])
	x4 := ((0x7fffffffffffffe + arg1[3]) - arg2[3])
	x5 := ((0x7fffffffffffffe + arg1[4]) - arg2[4])
	x6 := ((0x7fffffffffffffe + arg1[5]) - arg2[5])
	x7 := ((0x7fffffffffffffe + arg1[6]) - arg2[6])
	x8 := ((0x7fffffffffffffe + arg1[7]) - arg2[7])
	x9 := ((0x3fffffffffffffe + arg1[8]) - arg2[8])
	out1[0] = x1
	out1[1] = x2
	out1[2] = x3
	out1[3] = x4
	out1[4] = x5
	out1[5] = x6
	out1[6] = x7
	out1[7] = x8
	out1[8] = x9
}

// p521ToBytes serializes a field element to bytes in little-endian order.
//
// Postconditions:
//   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]
//
// Input Bounds:
//   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
// 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], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]
func p521ToBytes(out1 *[66]uint8, arg1 *[9]uint64) {
	var x1 uint64
	var x2 p521Uint1
	p521SubborrowxU58(&x1, &x2, 0x0, arg1[0], 0x3ffffffffffffff)
	var x3 uint64
	var x4 p521Uint1
	p521SubborrowxU58(&x3, &x4, x2, arg1[1], 0x3ffffffffffffff)
	var x5 uint64
	var x6 p521Uint1
	p521SubborrowxU58(&x5, &x6, x4, arg1[2], 0x3ffffffffffffff)
	var x7 uint64
	var x8 p521Uint1
	p521SubborrowxU58(&x7, &x8, x6, arg1[3], 0x3ffffffffffffff)
	var x9 uint64
	var x10 p521Uint1
	p521SubborrowxU58(&x9, &x10, x8, arg1[4], 0x3ffffffffffffff)
	var x11 uint64
	var x12 p521Uint1
	p521SubborrowxU58(&x11, &x12, x10, arg1[5], 0x3ffffffffffffff)
	var x13 uint64
	var x14 p521Uint1
	p521SubborrowxU58(&x13, &x14, x12, arg1[6], 0x3ffffffffffffff)
	var x15 uint64
	var x16 p521Uint1
	p521SubborrowxU58(&x15, &x16, x14, arg1[7], 0x3ffffffffffffff)
	var x17 uint64
	var x18 p521Uint1
	p521SubborrowxU57(&x17, &x18, x16, arg1[8], 0x1ffffffffffffff)
	var x19 uint64
	p521CmovznzU64(&x19, x18, uint64(0x0), 0xffffffffffffffff)
	var x20 uint64
	var x21 p521Uint1
	p521AddcarryxU58(&x20, &x21, 0x0, x1, (x19 & 0x3ffffffffffffff))
	var x22 uint64
	var x23 p521Uint1
	p521AddcarryxU58(&x22, &x23, x21, x3, (x19 & 0x3ffffffffffffff))
	var x24 uint64
	var x25 p521Uint1
	p521AddcarryxU58(&x24, &x25, x23, x5, (x19 & 0x3ffffffffffffff))
	var x26 uint64
	var x27 p521Uint1
	p521AddcarryxU58(&x26, &x27, x25, x7, (x19 & 0x3ffffffffffffff))
	var x28 uint64
	var x29 p521Uint1
	p521AddcarryxU58(&x28, &x29, x27, x9, (x19 & 0x3ffffffffffffff))
	var x30 uint64
	var x31 p521Uint1
	p521AddcarryxU58(&x30, &x31, x29, x11, (x19 & 0x3ffffffffffffff))
	var x32 uint64
	var x33 p521Uint1
	p521AddcarryxU58(&x32, &x33, x31, x13, (x19 & 0x3ffffffffffffff))
	var x34 uint64
	var x35 p521Uint1
	p521AddcarryxU58(&x34, &x35, x33, x15, (x19 & 0x3ffffffffffffff))
	var x36 uint64
	var x37 p521Uint1
	p521AddcarryxU57(&x36, &x37, x35, x17, (x19 & 0x1ffffffffffffff))
	x38 := (x34 << 6)
	x39 := (x32 << 4)
	x40 := (x30 << 2)
	x41 := (x26 << 6)
	x42 := (x24 << 4)
	x43 := (x22 << 2)
	x44 := (uint8(x20) & 0xff)
	x45 := (x20 >> 8)
	x46 := (uint8(x45) & 0xff)
	x47 := (x45 >> 8)
	x48 := (uint8(x47) & 0xff)
	x49 := (x47 >> 8)
	x50 := (uint8(x49) & 0xff)
	x51 := (x49 >> 8)
	x52 := (uint8(x51) & 0xff)
	x53 := (x51 >> 8)
	x54 := (uint8(x53) & 0xff)
	x55 := (x53 >> 8)
	x56 := (uint8(x55) & 0xff)
	x57 := uint8((x55 >> 8))
	x58 := (x43 + uint64(x57))
	x59 := (uint8(x58) & 0xff)
	x60 := (x58 >> 8)
	x61 := (uint8(x60) & 0xff)
	x62 := (x60 >> 8)
	x63 := (uint8(x62) & 0xff)
	x64 := (x62 >> 8)
	x65 := (uint8(x64) & 0xff)
	x66 := (x64 >> 8)
	x67 := (uint8(x66) & 0xff)
	x68 := (x66 >> 8)
	x69 := (uint8(x68) & 0xff)
	x70 := (x68 >> 8)
	x71 := (uint8(x70) & 0xff)
	x72 := uint8((x70 >> 8))
	x73 := (x42 + uint64(x72))
	x74 := (uint8(x73) & 0xff)
	x75 := (x73 >> 8)
	x76 := (uint8(x75) & 0xff)
	x77 := (x75 >> 8)
	x78 := (uint8(x77) & 0xff)
	x79 := (x77 >> 8)
	x80 := (uint8(x79) & 0xff)
	x81 := (x79 >> 8)
	x82 := (uint8(x81) & 0xff)
	x83 := (x81 >> 8)
	x84 := (uint8(x83) & 0xff)
	x85 := (x83 >> 8)
	x86 := (uint8(x85) & 0xff)
	x87 := uint8((x85 >> 8))
	x88 := (x41 + uint64(x87))
	x89 := (uint8(x88) & 0xff)
	x90 := (x88 >> 8)
	x91 := (uint8(x90) & 0xff)
	x92 := (x90 >> 8)
	x93 := (uint8(x92) & 0xff)
	x94 := (x92 >> 8)
	x95 := (uint8(x94) & 0xff)
	x96 := (x94 >> 8)
	x97 := (uint8(x96) & 0xff)
	x98 := (x96 >> 8)
	x99 := (uint8(x98) & 0xff)
	x100 := (x98 >> 8)
	x101 := (uint8(x100) & 0xff)
	x102 := uint8((x100 >> 8))
	x103 := (uint8(x28) & 0xff)
	x104 := (x28 >> 8)
	x105 := (uint8(x104) & 0xff)
	x106 := (x104 >> 8)
	x107 := (uint8(x106) & 0xff)
	x108 := (x106 >> 8)
	x109 := (uint8(x108) & 0xff)
	x110 := (x108 >> 8)
	x111 := (uint8(x110) & 0xff)
	x112 := (x110 >> 8)
	x113 := (uint8(x112) & 0xff)
	x114 := (x112 >> 8)
	x115 := (uint8(x114) & 0xff)
	x116 := uint8((x114 >> 8))
	x117 := (x40 + uint64(x116))
	x118 := (uint8(x117) & 0xff)
	x119 := (x117 >> 8)
	x120 := (uint8(x119) & 0xff)
	x121 := (x119 >> 8)
	x122 := (uint8(x121) & 0xff)
	x123 := (x121 >> 8)
	x124 := (uint8(x123) & 0xff)
	x125 := (x123 >> 8)
	x126 := (uint8(x125) & 0xff)
	x127 := (x125 >> 8)
	x128 := (uint8(x127) & 0xff)
	x129 := (x127 >> 8)
	x130 := (uint8(x129) & 0xff)
	x131 := uint8((x129 >> 8))
	x132 := (x39 + uint64(x131))
	x133 := (uint8(x132) & 0xff)
	x134 := (x132 >> 8)
	x135 := (uint8(x134) & 0xff)
	x136 := (x134 >> 8)
	x137 := (uint8(x136) & 0xff)
	x138 := (x136 >> 8)
	x139 := (uint8(x138) & 0xff)
	x140 := (x138 >> 8)
	x141 := (uint8(x140) & 0xff)
	x142 := (x140 >> 8)
	x143 := (uint8(x142) & 0xff)
	x144 := (x142 >> 8)
	x145 := (uint8(x144) & 0xff)
	x146 := uint8((x144 >> 8))
	x147 := (x38 + uint64(x146))
	x148 := (uint8(x147) & 0xff)
	x149 := (x147 >> 8)
	x150 := (uint8(x149) & 0xff)
	x151 := (x149 >> 8)
	x152 := (uint8(x151) & 0xff)
	x153 := (x151 >> 8)
	x154 := (uint8(x153) & 0xff)
	x155 := (x153 >> 8)
	x156 := (uint8(x155) & 0xff)
	x157 := (x155 >> 8)
	x158 := (uint8(x157) & 0xff)
	x159 := (x157 >> 8)
	x160 := (uint8(x159) & 0xff)
	x161 := uint8((x159 >> 8))
	x162 := (uint8(x36) & 0xff)
	x163 := (x36 >> 8)
	x164 := (uint8(x163) & 0xff)
	x165 := (x163 >> 8)
	x166 := (uint8(x165) & 0xff)
	x167 := (x165 >> 8)
	x168 := (uint8(x167) & 0xff)
	x169 := (x167 >> 8)
	x170 := (uint8(x169) & 0xff)
	x171 := (x169 >> 8)
	x172 := (uint8(x171) & 0xff)
	x173 := (x171 >> 8)
	x174 := (uint8(x173) & 0xff)
	x175 := p521Uint1((x173 >> 8))
	out1[0] = x44
	out1[1] = x46
	out1[2] = x48
	out1[3] = x50
	out1[4] = x52
	out1[5] = x54
	out1[6] = x56
	out1[7] = x59
	out1[8] = x61
	out1[9] = x63
	out1[10] = x65
	out1[11] = x67
	out1[12] = x69
	out1[13] = x71
	out1[14] = x74
	out1[15] = x76
	out1[16] = x78
	out1[17] = x80
	out1[18] = x82
	out1[19] = x84
	out1[20] = x86
	out1[21] = x89
	out1[22] = x91
	out1[23] = x93
	out1[24] = x95
	out1[25] = x97
	out1[26] = x99
	out1[27] = x101
	out1[28] = x102
	out1[29] = x103
	out1[30] = x105
	out1[31] = x107
	out1[32] = x109
	out1[33] = x111
	out1[34] = x113
	out1[35] = x115
	out1[36] = x118
	out1[37] = x120
	out1[38] = x122
	out1[39] = x124
	out1[40] = x126
	out1[41] = x128
	out1[42] = x130
	out1[43] = x133
	out1[44] = x135
	out1[45] = x137
	out1[46] = x139
	out1[47] = x141
	out1[48] = x143
	out1[49] = x145
	out1[50] = x148
	out1[51] = x150
	out1[52] = x152
	out1[53] = x154
	out1[54] = x156
	out1[55] = x158
	out1[56] = x160
	out1[57] = x161
	out1[58] = x162
	out1[59] = x164
	out1[60] = x166
	out1[61] = x168
	out1[62] = x170
	out1[63] = x172
	out1[64] = x174
	out1[65] = uint8(x175)
}

// p521FromBytes deserializes a field element from bytes in little-endian order.
//
// Postconditions:
//   eval out1 mod m = bytes_eval arg1 mod 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], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]
// Output Bounds:
//   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
func p521FromBytes(out1 *[9]uint64, arg1 *[66]uint8) {
	x1 := (uint64(p521Uint1(arg1[65])) << 56)
	x2 := (uint64(arg1[64]) << 48)
	x3 := (uint64(arg1[63]) << 40)
	x4 := (uint64(arg1[62]) << 32)
	x5 := (uint64(arg1[61]) << 24)
	x6 := (uint64(arg1[60]) << 16)
	x7 := (uint64(arg1[59]) << 8)
	x8 := arg1[58]
	x9 := (uint64(arg1[57]) << 50)
	x10 := (uint64(arg1[56]) << 42)
	x11 := (uint64(arg1[55]) << 34)
	x12 := (uint64(arg1[54]) << 26)
	x13 := (uint64(arg1[53]) << 18)
	x14 := (uint64(arg1[52]) << 10)
	x15 := (uint64(arg1[51]) << 2)
	x16 := (uint64(arg1[50]) << 52)
	x17 := (uint64(arg1[49]) << 44)
	x18 := (uint64(arg1[48]) << 36)
	x19 := (uint64(arg1[47]) << 28)
	x20 := (uint64(arg1[46]) << 20)
	x21 := (uint64(arg1[45]) << 12)
	x22 := (uint64(arg1[44]) << 4)
	x23 := (uint64(arg1[43]) << 54)
	x24 := (uint64(arg1[42]) << 46)
	x25 := (uint64(arg1[41]) << 38)
	x26 := (uint64(arg1[40]) << 30)
	x27 := (uint64(arg1[39]) << 22)
	x28 := (uint64(arg1[38]) << 14)
	x29 := (uint64(arg1[37]) << 6)
	x30 := (uint64(arg1[36]) << 56)
	x31 := (uint64(arg1[35]) << 48)
	x32 := (uint64(arg1[34]) << 40)
	x33 := (uint64(arg1[33]) << 32)
	x34 := (uint64(arg1[32]) << 24)
	x35 := (uint64(arg1[31]) << 16)
	x36 := (uint64(arg1[30]) << 8)
	x37 := arg1[29]
	x38 := (uint64(arg1[28]) << 50)
	x39 := (uint64(arg1[27]) << 42)
	x40 := (uint64(arg1[26]) << 34)
	x41 := (uint64(arg1[25]) << 26)
	x42 := (uint64(arg1[24]) << 18)
	x43 := (uint64(arg1[23]) << 10)
	x44 := (uint64(arg1[22]) << 2)
	x45 := (uint64(arg1[21]) << 52)
	x46 := (uint64(arg1[20]) << 44)
	x47 := (uint64(arg1[19]) << 36)
	x48 := (uint64(arg1[18]) << 28)
	x49 := (uint64(arg1[17]) << 20)
	x50 := (uint64(arg1[16]) << 12)
	x51 := (uint64(arg1[15]) << 4)
	x52 := (uint64(arg1[14]) << 54)
	x53 := (uint64(arg1[13]) << 46)
	x54 := (uint64(arg1[12]) << 38)
	x55 := (uint64(arg1[11]) << 30)
	x56 := (uint64(arg1[10]) << 22)
	x57 := (uint64(arg1[9]) << 14)
	x58 := (uint64(arg1[8]) << 6)
	x59 := (uint64(arg1[7]) << 56)
	x60 := (uint64(arg1[6]) << 48)
	x61 := (uint64(arg1[5]) << 40)
	x62 := (uint64(arg1[4]) << 32)
	x63 := (uint64(arg1[3]) << 24)
	x64 := (uint64(arg1[2]) << 16)
	x65 := (uint64(arg1[1]) << 8)
	x66 := arg1[0]
	x67 := (x65 + uint64(x66))
	x68 := (x64 + x67)
	x69 := (x63 + x68)
	x70 := (x62 + x69)
	x71 := (x61 + x70)
	x72 := (x60 + x71)
	x73 := (x59 + x72)
	x74 := (x73 & 0x3ffffffffffffff)
	x75 := uint8((x73 >> 58))
	x76 := (x58 + uint64(x75))
	x77 := (x57 + x76)
	x78 := (x56 + x77)
	x79 := (x55 + x78)
	x80 := (x54 + x79)
	x81 := (x53 + x80)
	x82 := (x52 + x81)
	x83 := (x82 & 0x3ffffffffffffff)
	x84 := uint8((x82 >> 58))
	x85 := (x51 + uint64(x84))
	x86 := (x50 + x85)
	x87 := (x49 + x86)
	x88 := (x48 + x87)
	x89 := (x47 + x88)
	x90 := (x46 + x89)
	x91 := (x45 + x90)
	x92 := (x91 & 0x3ffffffffffffff)
	x93 := uint8((x91 >> 58))
	x94 := (x44 + uint64(x93))
	x95 := (x43 + x94)
	x96 := (x42 + x95)
	x97 := (x41 + x96)
	x98 := (x40 + x97)
	x99 := (x39 + x98)
	x100 := (x38 + x99)
	x101 := (x36 + uint64(x37))
	x102 := (x35 + x101)
	x103 := (x34 + x102)
	x104 := (x33 + x103)
	x105 := (x32 + x104)
	x106 := (x31 + x105)
	x107 := (x30 + x106)
	x108 := (x107 & 0x3ffffffffffffff)
	x109 := uint8((x107 >> 58))
	x110 := (x29 + uint64(x109))
	x111 := (x28 + x110)
	x112 := (x27 + x111)
	x113 := (x26 + x112)
	x114 := (x25 + x113)
	x115 := (x24 + x114)
	x116 := (x23 + x115)
	x117 := (x116 & 0x3ffffffffffffff)
	x118 := uint8((x116 >> 58))
	x119 := (x22 + uint64(x118))
	x120 := (x21 + x119)
	x121 := (x20 + x120)
	x122 := (x19 + x121)
	x123 := (x18 + x122)
	x124 := (x17 + x123)
	x125 := (x16 + x124)
	x126 := (x125 & 0x3ffffffffffffff)
	x127 := uint8((x125 >> 58))
	x128 := (x15 + uint64(x127))
	x129 := (x14 + x128)
	x130 := (x13 + x129)
	x131 := (x12 + x130)
	x132 := (x11 + x131)
	x133 := (x10 + x132)
	x134 := (x9 + x133)
	x135 := (x7 + uint64(x8))
	x136 := (x6 + x135)
	x137 := (x5 + x136)
	x138 := (x4 + x137)
	x139 := (x3 + x138)
	x140 := (x2 + x139)
	x141 := (x1 + x140)
	out1[0] = x74
	out1[1] = x83
	out1[2] = x92
	out1[3] = x100
	out1[4] = x108
	out1[5] = x117
	out1[6] = x126
	out1[7] = x134
	out1[8] = x141
}

// p521Selectznz is a multi-limb conditional select.
//
// Postconditions:
//   eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
//
// Input Bounds:
//   arg1: [0x0 ~> 0x1]
//   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [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], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
// Output Bounds:
//   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
func p521Selectznz(out1 *[9]uint64, arg1 p521Uint1, arg2 *[9]uint64, arg3 *[9]uint64) {
	var x1 uint64
	p521CmovznzU64(&x1, arg1, arg2[0], arg3[0])
	var x2 uint64
	p521CmovznzU64(&x2, arg1, arg2[1], arg3[1])
	var x3 uint64
	p521CmovznzU64(&x3, arg1, arg2[2], arg3[2])
	var x4 uint64
	p521CmovznzU64(&x4, arg1, arg2[3], arg3[3])
	var x5 uint64
	p521CmovznzU64(&x5, arg1, arg2[4], arg3[4])
	var x6 uint64
	p521CmovznzU64(&x6, arg1, arg2[5], arg3[5])
	var x7 uint64
	p521CmovznzU64(&x7, arg1, arg2[6], arg3[6])
	var x8 uint64
	p521CmovznzU64(&x8, arg1, arg2[7], arg3[7])
	var x9 uint64
	p521CmovznzU64(&x9, arg1, arg2[8], arg3[8])
	out1[0] = x1
	out1[1] = x2
	out1[2] = x3
	out1[3] = x4
	out1[4] = x5
	out1[5] = x6
	out1[6] = x7
	out1[7] = x8
	out1[8] = x9
}