Source file src/crypto/elliptic/internal/fiat/p521_fiat64.go

Documentation: crypto/elliptic/internal/fiat

     1  // Code generated by Fiat Cryptography. DO NOT EDIT.
     2  //
     3  // 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
     4  //
     5  // curve description: p521
     6  //
     7  // machine_wordsize = 64 (from "64")
     8  //
     9  // requested operations: carry_mul, carry_square, carry, add, sub, to_bytes, from_bytes, selectznz
    10  //
    11  // n = 9 (from "9")
    12  //
    13  // s-c = 2^521 - [(1, 1)] (from "2^521 - 1")
    14  //
    15  // tight_bounds_multiplier = 1 (from "")
    16  //
    17  //
    18  //
    19  // Computed values:
    20  //
    21  //   carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]
    22  //
    23  //   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)
    24  //
    25  //   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)
    26  //
    27  //   balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe]
    28  
    29  package fiat
    30  
    31  import "math/bits"
    32  
    33  type p521Uint1 uint8
    34  type p521Int1 int8
    35  
    36  // p521AddcarryxU64 is a thin wrapper around bits.Add64 that uses p521Uint1 rather than uint64
    37  func p521AddcarryxU64(x uint64, y uint64, carry p521Uint1) (uint64, p521Uint1) {
    38  	sum, carryOut := bits.Add64(x, y, uint64(carry))
    39  	return sum, p521Uint1(carryOut)
    40  }
    41  
    42  // p521SubborrowxU64 is a thin wrapper around bits.Sub64 that uses p521Uint1 rather than uint64
    43  func p521SubborrowxU64(x uint64, y uint64, carry p521Uint1) (uint64, p521Uint1) {
    44  	sum, carryOut := bits.Sub64(x, y, uint64(carry))
    45  	return sum, p521Uint1(carryOut)
    46  }
    47  
    48  // p521AddcarryxU58 is an addition with carry.
    49  //
    50  // Postconditions:
    51  //   out1 = (arg1 + arg2 + arg3) mod 2^58
    52  //   out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋
    53  //
    54  // Input Bounds:
    55  //   arg1: [0x0 ~> 0x1]
    56  //   arg2: [0x0 ~> 0x3ffffffffffffff]
    57  //   arg3: [0x0 ~> 0x3ffffffffffffff]
    58  // Output Bounds:
    59  //   out1: [0x0 ~> 0x3ffffffffffffff]
    60  //   out2: [0x0 ~> 0x1]
    61  func p521AddcarryxU58(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
    62  	x1 := ((uint64(arg1) + arg2) + arg3)
    63  	x2 := (x1 & 0x3ffffffffffffff)
    64  	x3 := p521Uint1((x1 >> 58))
    65  	*out1 = x2
    66  	*out2 = x3
    67  }
    68  
    69  // p521SubborrowxU58 is a subtraction with borrow.
    70  //
    71  // Postconditions:
    72  //   out1 = (-arg1 + arg2 + -arg3) mod 2^58
    73  //   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋
    74  //
    75  // Input Bounds:
    76  //   arg1: [0x0 ~> 0x1]
    77  //   arg2: [0x0 ~> 0x3ffffffffffffff]
    78  //   arg3: [0x0 ~> 0x3ffffffffffffff]
    79  // Output Bounds:
    80  //   out1: [0x0 ~> 0x3ffffffffffffff]
    81  //   out2: [0x0 ~> 0x1]
    82  func p521SubborrowxU58(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
    83  	x1 := ((int64(arg2) - int64(arg1)) - int64(arg3))
    84  	x2 := p521Int1((x1 >> 58))
    85  	x3 := (uint64(x1) & 0x3ffffffffffffff)
    86  	*out1 = x3
    87  	*out2 = (0x0 - p521Uint1(x2))
    88  }
    89  
    90  // p521AddcarryxU57 is an addition with carry.
    91  //
    92  // Postconditions:
    93  //   out1 = (arg1 + arg2 + arg3) mod 2^57
    94  //   out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋
    95  //
    96  // Input Bounds:
    97  //   arg1: [0x0 ~> 0x1]
    98  //   arg2: [0x0 ~> 0x1ffffffffffffff]
    99  //   arg3: [0x0 ~> 0x1ffffffffffffff]
   100  // Output Bounds:
   101  //   out1: [0x0 ~> 0x1ffffffffffffff]
   102  //   out2: [0x0 ~> 0x1]
   103  func p521AddcarryxU57(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
   104  	x1 := ((uint64(arg1) + arg2) + arg3)
   105  	x2 := (x1 & 0x1ffffffffffffff)
   106  	x3 := p521Uint1((x1 >> 57))
   107  	*out1 = x2
   108  	*out2 = x3
   109  }
   110  
   111  // p521SubborrowxU57 is a subtraction with borrow.
   112  //
   113  // Postconditions:
   114  //   out1 = (-arg1 + arg2 + -arg3) mod 2^57
   115  //   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋
   116  //
   117  // Input Bounds:
   118  //   arg1: [0x0 ~> 0x1]
   119  //   arg2: [0x0 ~> 0x1ffffffffffffff]
   120  //   arg3: [0x0 ~> 0x1ffffffffffffff]
   121  // Output Bounds:
   122  //   out1: [0x0 ~> 0x1ffffffffffffff]
   123  //   out2: [0x0 ~> 0x1]
   124  func p521SubborrowxU57(out1 *uint64, out2 *p521Uint1, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
   125  	x1 := ((int64(arg2) - int64(arg1)) - int64(arg3))
   126  	x2 := p521Int1((x1 >> 57))
   127  	x3 := (uint64(x1) & 0x1ffffffffffffff)
   128  	*out1 = x3
   129  	*out2 = (0x0 - p521Uint1(x2))
   130  }
   131  
   132  // p521CmovznzU64 is a single-word conditional move.
   133  //
   134  // Postconditions:
   135  //   out1 = (if arg1 = 0 then arg2 else arg3)
   136  //
   137  // Input Bounds:
   138  //   arg1: [0x0 ~> 0x1]
   139  //   arg2: [0x0 ~> 0xffffffffffffffff]
   140  //   arg3: [0x0 ~> 0xffffffffffffffff]
   141  // Output Bounds:
   142  //   out1: [0x0 ~> 0xffffffffffffffff]
   143  func p521CmovznzU64(out1 *uint64, arg1 p521Uint1, arg2 uint64, arg3 uint64) {
   144  	x1 := (uint64(arg1) * 0xffffffffffffffff)
   145  	x2 := ((x1 & arg3) | ((^x1) & arg2))
   146  	*out1 = x2
   147  }
   148  
   149  // p521CarryMul multiplies two field elements and reduces the result.
   150  //
   151  // Postconditions:
   152  //   eval out1 mod m = (eval arg1 * eval arg2) mod m
   153  //
   154  // Input Bounds:
   155  //   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
   156  //   arg2: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
   157  // Output Bounds:
   158  //   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
   159  func p521CarryMul(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
   160  	var x1 uint64
   161  	var x2 uint64
   162  	x2, x1 = bits.Mul64(arg1[8], (arg2[8] * 0x2))
   163  	var x3 uint64
   164  	var x4 uint64
   165  	x4, x3 = bits.Mul64(arg1[8], (arg2[7] * 0x2))
   166  	var x5 uint64
   167  	var x6 uint64
   168  	x6, x5 = bits.Mul64(arg1[8], (arg2[6] * 0x2))
   169  	var x7 uint64
   170  	var x8 uint64
   171  	x8, x7 = bits.Mul64(arg1[8], (arg2[5] * 0x2))
   172  	var x9 uint64
   173  	var x10 uint64
   174  	x10, x9 = bits.Mul64(arg1[8], (arg2[4] * 0x2))
   175  	var x11 uint64
   176  	var x12 uint64
   177  	x12, x11 = bits.Mul64(arg1[8], (arg2[3] * 0x2))
   178  	var x13 uint64
   179  	var x14 uint64
   180  	x14, x13 = bits.Mul64(arg1[8], (arg2[2] * 0x2))
   181  	var x15 uint64
   182  	var x16 uint64
   183  	x16, x15 = bits.Mul64(arg1[8], (arg2[1] * 0x2))
   184  	var x17 uint64
   185  	var x18 uint64
   186  	x18, x17 = bits.Mul64(arg1[7], (arg2[8] * 0x2))
   187  	var x19 uint64
   188  	var x20 uint64
   189  	x20, x19 = bits.Mul64(arg1[7], (arg2[7] * 0x2))
   190  	var x21 uint64
   191  	var x22 uint64
   192  	x22, x21 = bits.Mul64(arg1[7], (arg2[6] * 0x2))
   193  	var x23 uint64
   194  	var x24 uint64
   195  	x24, x23 = bits.Mul64(arg1[7], (arg2[5] * 0x2))
   196  	var x25 uint64
   197  	var x26 uint64
   198  	x26, x25 = bits.Mul64(arg1[7], (arg2[4] * 0x2))
   199  	var x27 uint64
   200  	var x28 uint64
   201  	x28, x27 = bits.Mul64(arg1[7], (arg2[3] * 0x2))
   202  	var x29 uint64
   203  	var x30 uint64
   204  	x30, x29 = bits.Mul64(arg1[7], (arg2[2] * 0x2))
   205  	var x31 uint64
   206  	var x32 uint64
   207  	x32, x31 = bits.Mul64(arg1[6], (arg2[8] * 0x2))
   208  	var x33 uint64
   209  	var x34 uint64
   210  	x34, x33 = bits.Mul64(arg1[6], (arg2[7] * 0x2))
   211  	var x35 uint64
   212  	var x36 uint64
   213  	x36, x35 = bits.Mul64(arg1[6], (arg2[6] * 0x2))
   214  	var x37 uint64
   215  	var x38 uint64
   216  	x38, x37 = bits.Mul64(arg1[6], (arg2[5] * 0x2))
   217  	var x39 uint64
   218  	var x40 uint64
   219  	x40, x39 = bits.Mul64(arg1[6], (arg2[4] * 0x2))
   220  	var x41 uint64
   221  	var x42 uint64
   222  	x42, x41 = bits.Mul64(arg1[6], (arg2[3] * 0x2))
   223  	var x43 uint64
   224  	var x44 uint64
   225  	x44, x43 = bits.Mul64(arg1[5], (arg2[8] * 0x2))
   226  	var x45 uint64
   227  	var x46 uint64
   228  	x46, x45 = bits.Mul64(arg1[5], (arg2[7] * 0x2))
   229  	var x47 uint64
   230  	var x48 uint64
   231  	x48, x47 = bits.Mul64(arg1[5], (arg2[6] * 0x2))
   232  	var x49 uint64
   233  	var x50 uint64
   234  	x50, x49 = bits.Mul64(arg1[5], (arg2[5] * 0x2))
   235  	var x51 uint64
   236  	var x52 uint64
   237  	x52, x51 = bits.Mul64(arg1[5], (arg2[4] * 0x2))
   238  	var x53 uint64
   239  	var x54 uint64
   240  	x54, x53 = bits.Mul64(arg1[4], (arg2[8] * 0x2))
   241  	var x55 uint64
   242  	var x56 uint64
   243  	x56, x55 = bits.Mul64(arg1[4], (arg2[7] * 0x2))
   244  	var x57 uint64
   245  	var x58 uint64
   246  	x58, x57 = bits.Mul64(arg1[4], (arg2[6] * 0x2))
   247  	var x59 uint64
   248  	var x60 uint64
   249  	x60, x59 = bits.Mul64(arg1[4], (arg2[5] * 0x2))
   250  	var x61 uint64
   251  	var x62 uint64
   252  	x62, x61 = bits.Mul64(arg1[3], (arg2[8] * 0x2))
   253  	var x63 uint64
   254  	var x64 uint64
   255  	x64, x63 = bits.Mul64(arg1[3], (arg2[7] * 0x2))
   256  	var x65 uint64
   257  	var x66 uint64
   258  	x66, x65 = bits.Mul64(arg1[3], (arg2[6] * 0x2))
   259  	var x67 uint64
   260  	var x68 uint64
   261  	x68, x67 = bits.Mul64(arg1[2], (arg2[8] * 0x2))
   262  	var x69 uint64
   263  	var x70 uint64
   264  	x70, x69 = bits.Mul64(arg1[2], (arg2[7] * 0x2))
   265  	var x71 uint64
   266  	var x72 uint64
   267  	x72, x71 = bits.Mul64(arg1[1], (arg2[8] * 0x2))
   268  	var x73 uint64
   269  	var x74 uint64
   270  	x74, x73 = bits.Mul64(arg1[8], arg2[0])
   271  	var x75 uint64
   272  	var x76 uint64
   273  	x76, x75 = bits.Mul64(arg1[7], arg2[1])
   274  	var x77 uint64
   275  	var x78 uint64
   276  	x78, x77 = bits.Mul64(arg1[7], arg2[0])
   277  	var x79 uint64
   278  	var x80 uint64
   279  	x80, x79 = bits.Mul64(arg1[6], arg2[2])
   280  	var x81 uint64
   281  	var x82 uint64
   282  	x82, x81 = bits.Mul64(arg1[6], arg2[1])
   283  	var x83 uint64
   284  	var x84 uint64
   285  	x84, x83 = bits.Mul64(arg1[6], arg2[0])
   286  	var x85 uint64
   287  	var x86 uint64
   288  	x86, x85 = bits.Mul64(arg1[5], arg2[3])
   289  	var x87 uint64
   290  	var x88 uint64
   291  	x88, x87 = bits.Mul64(arg1[5], arg2[2])
   292  	var x89 uint64
   293  	var x90 uint64
   294  	x90, x89 = bits.Mul64(arg1[5], arg2[1])
   295  	var x91 uint64
   296  	var x92 uint64
   297  	x92, x91 = bits.Mul64(arg1[5], arg2[0])
   298  	var x93 uint64
   299  	var x94 uint64
   300  	x94, x93 = bits.Mul64(arg1[4], arg2[4])
   301  	var x95 uint64
   302  	var x96 uint64
   303  	x96, x95 = bits.Mul64(arg1[4], arg2[3])
   304  	var x97 uint64
   305  	var x98 uint64
   306  	x98, x97 = bits.Mul64(arg1[4], arg2[2])
   307  	var x99 uint64
   308  	var x100 uint64
   309  	x100, x99 = bits.Mul64(arg1[4], arg2[1])
   310  	var x101 uint64
   311  	var x102 uint64
   312  	x102, x101 = bits.Mul64(arg1[4], arg2[0])
   313  	var x103 uint64
   314  	var x104 uint64
   315  	x104, x103 = bits.Mul64(arg1[3], arg2[5])
   316  	var x105 uint64
   317  	var x106 uint64
   318  	x106, x105 = bits.Mul64(arg1[3], arg2[4])
   319  	var x107 uint64
   320  	var x108 uint64
   321  	x108, x107 = bits.Mul64(arg1[3], arg2[3])
   322  	var x109 uint64
   323  	var x110 uint64
   324  	x110, x109 = bits.Mul64(arg1[3], arg2[2])
   325  	var x111 uint64
   326  	var x112 uint64
   327  	x112, x111 = bits.Mul64(arg1[3], arg2[1])
   328  	var x113 uint64
   329  	var x114 uint64
   330  	x114, x113 = bits.Mul64(arg1[3], arg2[0])
   331  	var x115 uint64
   332  	var x116 uint64
   333  	x116, x115 = bits.Mul64(arg1[2], arg2[6])
   334  	var x117 uint64
   335  	var x118 uint64
   336  	x118, x117 = bits.Mul64(arg1[2], arg2[5])
   337  	var x119 uint64
   338  	var x120 uint64
   339  	x120, x119 = bits.Mul64(arg1[2], arg2[4])
   340  	var x121 uint64
   341  	var x122 uint64
   342  	x122, x121 = bits.Mul64(arg1[2], arg2[3])
   343  	var x123 uint64
   344  	var x124 uint64
   345  	x124, x123 = bits.Mul64(arg1[2], arg2[2])
   346  	var x125 uint64
   347  	var x126 uint64
   348  	x126, x125 = bits.Mul64(arg1[2], arg2[1])
   349  	var x127 uint64
   350  	var x128 uint64
   351  	x128, x127 = bits.Mul64(arg1[2], arg2[0])
   352  	var x129 uint64
   353  	var x130 uint64
   354  	x130, x129 = bits.Mul64(arg1[1], arg2[7])
   355  	var x131 uint64
   356  	var x132 uint64
   357  	x132, x131 = bits.Mul64(arg1[1], arg2[6])
   358  	var x133 uint64
   359  	var x134 uint64
   360  	x134, x133 = bits.Mul64(arg1[1], arg2[5])
   361  	var x135 uint64
   362  	var x136 uint64
   363  	x136, x135 = bits.Mul64(arg1[1], arg2[4])
   364  	var x137 uint64
   365  	var x138 uint64
   366  	x138, x137 = bits.Mul64(arg1[1], arg2[3])
   367  	var x139 uint64
   368  	var x140 uint64
   369  	x140, x139 = bits.Mul64(arg1[1], arg2[2])
   370  	var x141 uint64
   371  	var x142 uint64
   372  	x142, x141 = bits.Mul64(arg1[1], arg2[1])
   373  	var x143 uint64
   374  	var x144 uint64
   375  	x144, x143 = bits.Mul64(arg1[1], arg2[0])
   376  	var x145 uint64
   377  	var x146 uint64
   378  	x146, x145 = bits.Mul64(arg1[0], arg2[8])
   379  	var x147 uint64
   380  	var x148 uint64
   381  	x148, x147 = bits.Mul64(arg1[0], arg2[7])
   382  	var x149 uint64
   383  	var x150 uint64
   384  	x150, x149 = bits.Mul64(arg1[0], arg2[6])
   385  	var x151 uint64
   386  	var x152 uint64
   387  	x152, x151 = bits.Mul64(arg1[0], arg2[5])
   388  	var x153 uint64
   389  	var x154 uint64
   390  	x154, x153 = bits.Mul64(arg1[0], arg2[4])
   391  	var x155 uint64
   392  	var x156 uint64
   393  	x156, x155 = bits.Mul64(arg1[0], arg2[3])
   394  	var x157 uint64
   395  	var x158 uint64
   396  	x158, x157 = bits.Mul64(arg1[0], arg2[2])
   397  	var x159 uint64
   398  	var x160 uint64
   399  	x160, x159 = bits.Mul64(arg1[0], arg2[1])
   400  	var x161 uint64
   401  	var x162 uint64
   402  	x162, x161 = bits.Mul64(arg1[0], arg2[0])
   403  	var x163 uint64
   404  	var x164 p521Uint1
   405  	x163, x164 = p521AddcarryxU64(x29, x15, 0x0)
   406  	var x165 uint64
   407  	x165, _ = p521AddcarryxU64(x30, x16, x164)
   408  	var x167 uint64
   409  	var x168 p521Uint1
   410  	x167, x168 = p521AddcarryxU64(x41, x163, 0x0)
   411  	var x169 uint64
   412  	x169, _ = p521AddcarryxU64(x42, x165, x168)
   413  	var x171 uint64
   414  	var x172 p521Uint1
   415  	x171, x172 = p521AddcarryxU64(x51, x167, 0x0)
   416  	var x173 uint64
   417  	x173, _ = p521AddcarryxU64(x52, x169, x172)
   418  	var x175 uint64
   419  	var x176 p521Uint1
   420  	x175, x176 = p521AddcarryxU64(x59, x171, 0x0)
   421  	var x177 uint64
   422  	x177, _ = p521AddcarryxU64(x60, x173, x176)
   423  	var x179 uint64
   424  	var x180 p521Uint1
   425  	x179, x180 = p521AddcarryxU64(x65, x175, 0x0)
   426  	var x181 uint64
   427  	x181, _ = p521AddcarryxU64(x66, x177, x180)
   428  	var x183 uint64
   429  	var x184 p521Uint1
   430  	x183, x184 = p521AddcarryxU64(x69, x179, 0x0)
   431  	var x185 uint64
   432  	x185, _ = p521AddcarryxU64(x70, x181, x184)
   433  	var x187 uint64
   434  	var x188 p521Uint1
   435  	x187, x188 = p521AddcarryxU64(x71, x183, 0x0)
   436  	var x189 uint64
   437  	x189, _ = p521AddcarryxU64(x72, x185, x188)
   438  	var x191 uint64
   439  	var x192 p521Uint1
   440  	x191, x192 = p521AddcarryxU64(x161, x187, 0x0)
   441  	var x193 uint64
   442  	x193, _ = p521AddcarryxU64(x162, x189, x192)
   443  	x195 := ((x191 >> 58) | ((x193 << 6) & 0xffffffffffffffff))
   444  	x196 := (x193 >> 58)
   445  	x197 := (x191 & 0x3ffffffffffffff)
   446  	var x198 uint64
   447  	var x199 p521Uint1
   448  	x198, x199 = p521AddcarryxU64(x75, x73, 0x0)
   449  	var x200 uint64
   450  	x200, _ = p521AddcarryxU64(x76, x74, x199)
   451  	var x202 uint64
   452  	var x203 p521Uint1
   453  	x202, x203 = p521AddcarryxU64(x79, x198, 0x0)
   454  	var x204 uint64
   455  	x204, _ = p521AddcarryxU64(x80, x200, x203)
   456  	var x206 uint64
   457  	var x207 p521Uint1
   458  	x206, x207 = p521AddcarryxU64(x85, x202, 0x0)
   459  	var x208 uint64
   460  	x208, _ = p521AddcarryxU64(x86, x204, x207)
   461  	var x210 uint64
   462  	var x211 p521Uint1
   463  	x210, x211 = p521AddcarryxU64(x93, x206, 0x0)
   464  	var x212 uint64
   465  	x212, _ = p521AddcarryxU64(x94, x208, x211)
   466  	var x214 uint64
   467  	var x215 p521Uint1
   468  	x214, x215 = p521AddcarryxU64(x103, x210, 0x0)
   469  	var x216 uint64
   470  	x216, _ = p521AddcarryxU64(x104, x212, x215)
   471  	var x218 uint64
   472  	var x219 p521Uint1
   473  	x218, x219 = p521AddcarryxU64(x115, x214, 0x0)
   474  	var x220 uint64
   475  	x220, _ = p521AddcarryxU64(x116, x216, x219)
   476  	var x222 uint64
   477  	var x223 p521Uint1
   478  	x222, x223 = p521AddcarryxU64(x129, x218, 0x0)
   479  	var x224 uint64
   480  	x224, _ = p521AddcarryxU64(x130, x220, x223)
   481  	var x226 uint64
   482  	var x227 p521Uint1
   483  	x226, x227 = p521AddcarryxU64(x145, x222, 0x0)
   484  	var x228 uint64
   485  	x228, _ = p521AddcarryxU64(x146, x224, x227)
   486  	var x230 uint64
   487  	var x231 p521Uint1
   488  	x230, x231 = p521AddcarryxU64(x77, x1, 0x0)
   489  	var x232 uint64
   490  	x232, _ = p521AddcarryxU64(x78, x2, x231)
   491  	var x234 uint64
   492  	var x235 p521Uint1
   493  	x234, x235 = p521AddcarryxU64(x81, x230, 0x0)
   494  	var x236 uint64
   495  	x236, _ = p521AddcarryxU64(x82, x232, x235)
   496  	var x238 uint64
   497  	var x239 p521Uint1
   498  	x238, x239 = p521AddcarryxU64(x87, x234, 0x0)
   499  	var x240 uint64
   500  	x240, _ = p521AddcarryxU64(x88, x236, x239)
   501  	var x242 uint64
   502  	var x243 p521Uint1
   503  	x242, x243 = p521AddcarryxU64(x95, x238, 0x0)
   504  	var x244 uint64
   505  	x244, _ = p521AddcarryxU64(x96, x240, x243)
   506  	var x246 uint64
   507  	var x247 p521Uint1
   508  	x246, x247 = p521AddcarryxU64(x105, x242, 0x0)
   509  	var x248 uint64
   510  	x248, _ = p521AddcarryxU64(x106, x244, x247)
   511  	var x250 uint64
   512  	var x251 p521Uint1
   513  	x250, x251 = p521AddcarryxU64(x117, x246, 0x0)
   514  	var x252 uint64
   515  	x252, _ = p521AddcarryxU64(x118, x248, x251)
   516  	var x254 uint64
   517  	var x255 p521Uint1
   518  	x254, x255 = p521AddcarryxU64(x131, x250, 0x0)
   519  	var x256 uint64
   520  	x256, _ = p521AddcarryxU64(x132, x252, x255)
   521  	var x258 uint64
   522  	var x259 p521Uint1
   523  	x258, x259 = p521AddcarryxU64(x147, x254, 0x0)
   524  	var x260 uint64
   525  	x260, _ = p521AddcarryxU64(x148, x256, x259)
   526  	var x262 uint64
   527  	var x263 p521Uint1
   528  	x262, x263 = p521AddcarryxU64(x17, x3, 0x0)
   529  	var x264 uint64
   530  	x264, _ = p521AddcarryxU64(x18, x4, x263)
   531  	var x266 uint64
   532  	var x267 p521Uint1
   533  	x266, x267 = p521AddcarryxU64(x83, x262, 0x0)
   534  	var x268 uint64
   535  	x268, _ = p521AddcarryxU64(x84, x264, x267)
   536  	var x270 uint64
   537  	var x271 p521Uint1
   538  	x270, x271 = p521AddcarryxU64(x89, x266, 0x0)
   539  	var x272 uint64
   540  	x272, _ = p521AddcarryxU64(x90, x268, x271)
   541  	var x274 uint64
   542  	var x275 p521Uint1
   543  	x274, x275 = p521AddcarryxU64(x97, x270, 0x0)
   544  	var x276 uint64
   545  	x276, _ = p521AddcarryxU64(x98, x272, x275)
   546  	var x278 uint64
   547  	var x279 p521Uint1
   548  	x278, x279 = p521AddcarryxU64(x107, x274, 0x0)
   549  	var x280 uint64
   550  	x280, _ = p521AddcarryxU64(x108, x276, x279)
   551  	var x282 uint64
   552  	var x283 p521Uint1
   553  	x282, x283 = p521AddcarryxU64(x119, x278, 0x0)
   554  	var x284 uint64
   555  	x284, _ = p521AddcarryxU64(x120, x280, x283)
   556  	var x286 uint64
   557  	var x287 p521Uint1
   558  	x286, x287 = p521AddcarryxU64(x133, x282, 0x0)
   559  	var x288 uint64
   560  	x288, _ = p521AddcarryxU64(x134, x284, x287)
   561  	var x290 uint64
   562  	var x291 p521Uint1
   563  	x290, x291 = p521AddcarryxU64(x149, x286, 0x0)
   564  	var x292 uint64
   565  	x292, _ = p521AddcarryxU64(x150, x288, x291)
   566  	var x294 uint64
   567  	var x295 p521Uint1
   568  	x294, x295 = p521AddcarryxU64(x19, x5, 0x0)
   569  	var x296 uint64
   570  	x296, _ = p521AddcarryxU64(x20, x6, x295)
   571  	var x298 uint64
   572  	var x299 p521Uint1
   573  	x298, x299 = p521AddcarryxU64(x31, x294, 0x0)
   574  	var x300 uint64
   575  	x300, _ = p521AddcarryxU64(x32, x296, x299)
   576  	var x302 uint64
   577  	var x303 p521Uint1
   578  	x302, x303 = p521AddcarryxU64(x91, x298, 0x0)
   579  	var x304 uint64
   580  	x304, _ = p521AddcarryxU64(x92, x300, x303)
   581  	var x306 uint64
   582  	var x307 p521Uint1
   583  	x306, x307 = p521AddcarryxU64(x99, x302, 0x0)
   584  	var x308 uint64
   585  	x308, _ = p521AddcarryxU64(x100, x304, x307)
   586  	var x310 uint64
   587  	var x311 p521Uint1
   588  	x310, x311 = p521AddcarryxU64(x109, x306, 0x0)
   589  	var x312 uint64
   590  	x312, _ = p521AddcarryxU64(x110, x308, x311)
   591  	var x314 uint64
   592  	var x315 p521Uint1
   593  	x314, x315 = p521AddcarryxU64(x121, x310, 0x0)
   594  	var x316 uint64
   595  	x316, _ = p521AddcarryxU64(x122, x312, x315)
   596  	var x318 uint64
   597  	var x319 p521Uint1
   598  	x318, x319 = p521AddcarryxU64(x135, x314, 0x0)
   599  	var x320 uint64
   600  	x320, _ = p521AddcarryxU64(x136, x316, x319)
   601  	var x322 uint64
   602  	var x323 p521Uint1
   603  	x322, x323 = p521AddcarryxU64(x151, x318, 0x0)
   604  	var x324 uint64
   605  	x324, _ = p521AddcarryxU64(x152, x320, x323)
   606  	var x326 uint64
   607  	var x327 p521Uint1
   608  	x326, x327 = p521AddcarryxU64(x21, x7, 0x0)
   609  	var x328 uint64
   610  	x328, _ = p521AddcarryxU64(x22, x8, x327)
   611  	var x330 uint64
   612  	var x331 p521Uint1
   613  	x330, x331 = p521AddcarryxU64(x33, x326, 0x0)
   614  	var x332 uint64
   615  	x332, _ = p521AddcarryxU64(x34, x328, x331)
   616  	var x334 uint64
   617  	var x335 p521Uint1
   618  	x334, x335 = p521AddcarryxU64(x43, x330, 0x0)
   619  	var x336 uint64
   620  	x336, _ = p521AddcarryxU64(x44, x332, x335)
   621  	var x338 uint64
   622  	var x339 p521Uint1
   623  	x338, x339 = p521AddcarryxU64(x101, x334, 0x0)
   624  	var x340 uint64
   625  	x340, _ = p521AddcarryxU64(x102, x336, x339)
   626  	var x342 uint64
   627  	var x343 p521Uint1
   628  	x342, x343 = p521AddcarryxU64(x111, x338, 0x0)
   629  	var x344 uint64
   630  	x344, _ = p521AddcarryxU64(x112, x340, x343)
   631  	var x346 uint64
   632  	var x347 p521Uint1
   633  	x346, x347 = p521AddcarryxU64(x123, x342, 0x0)
   634  	var x348 uint64
   635  	x348, _ = p521AddcarryxU64(x124, x344, x347)
   636  	var x350 uint64
   637  	var x351 p521Uint1
   638  	x350, x351 = p521AddcarryxU64(x137, x346, 0x0)
   639  	var x352 uint64
   640  	x352, _ = p521AddcarryxU64(x138, x348, x351)
   641  	var x354 uint64
   642  	var x355 p521Uint1
   643  	x354, x355 = p521AddcarryxU64(x153, x350, 0x0)
   644  	var x356 uint64
   645  	x356, _ = p521AddcarryxU64(x154, x352, x355)
   646  	var x358 uint64
   647  	var x359 p521Uint1
   648  	x358, x359 = p521AddcarryxU64(x23, x9, 0x0)
   649  	var x360 uint64
   650  	x360, _ = p521AddcarryxU64(x24, x10, x359)
   651  	var x362 uint64
   652  	var x363 p521Uint1
   653  	x362, x363 = p521AddcarryxU64(x35, x358, 0x0)
   654  	var x364 uint64
   655  	x364, _ = p521AddcarryxU64(x36, x360, x363)
   656  	var x366 uint64
   657  	var x367 p521Uint1
   658  	x366, x367 = p521AddcarryxU64(x45, x362, 0x0)
   659  	var x368 uint64
   660  	x368, _ = p521AddcarryxU64(x46, x364, x367)
   661  	var x370 uint64
   662  	var x371 p521Uint1
   663  	x370, x371 = p521AddcarryxU64(x53, x366, 0x0)
   664  	var x372 uint64
   665  	x372, _ = p521AddcarryxU64(x54, x368, x371)
   666  	var x374 uint64
   667  	var x375 p521Uint1
   668  	x374, x375 = p521AddcarryxU64(x113, x370, 0x0)
   669  	var x376 uint64
   670  	x376, _ = p521AddcarryxU64(x114, x372, x375)
   671  	var x378 uint64
   672  	var x379 p521Uint1
   673  	x378, x379 = p521AddcarryxU64(x125, x374, 0x0)
   674  	var x380 uint64
   675  	x380, _ = p521AddcarryxU64(x126, x376, x379)
   676  	var x382 uint64
   677  	var x383 p521Uint1
   678  	x382, x383 = p521AddcarryxU64(x139, x378, 0x0)
   679  	var x384 uint64
   680  	x384, _ = p521AddcarryxU64(x140, x380, x383)
   681  	var x386 uint64
   682  	var x387 p521Uint1
   683  	x386, x387 = p521AddcarryxU64(x155, x382, 0x0)
   684  	var x388 uint64
   685  	x388, _ = p521AddcarryxU64(x156, x384, x387)
   686  	var x390 uint64
   687  	var x391 p521Uint1
   688  	x390, x391 = p521AddcarryxU64(x25, x11, 0x0)
   689  	var x392 uint64
   690  	x392, _ = p521AddcarryxU64(x26, x12, x391)
   691  	var x394 uint64
   692  	var x395 p521Uint1
   693  	x394, x395 = p521AddcarryxU64(x37, x390, 0x0)
   694  	var x396 uint64
   695  	x396, _ = p521AddcarryxU64(x38, x392, x395)
   696  	var x398 uint64
   697  	var x399 p521Uint1
   698  	x398, x399 = p521AddcarryxU64(x47, x394, 0x0)
   699  	var x400 uint64
   700  	x400, _ = p521AddcarryxU64(x48, x396, x399)
   701  	var x402 uint64
   702  	var x403 p521Uint1
   703  	x402, x403 = p521AddcarryxU64(x55, x398, 0x0)
   704  	var x404 uint64
   705  	x404, _ = p521AddcarryxU64(x56, x400, x403)
   706  	var x406 uint64
   707  	var x407 p521Uint1
   708  	x406, x407 = p521AddcarryxU64(x61, x402, 0x0)
   709  	var x408 uint64
   710  	x408, _ = p521AddcarryxU64(x62, x404, x407)
   711  	var x410 uint64
   712  	var x411 p521Uint1
   713  	x410, x411 = p521AddcarryxU64(x127, x406, 0x0)
   714  	var x412 uint64
   715  	x412, _ = p521AddcarryxU64(x128, x408, x411)
   716  	var x414 uint64
   717  	var x415 p521Uint1
   718  	x414, x415 = p521AddcarryxU64(x141, x410, 0x0)
   719  	var x416 uint64
   720  	x416, _ = p521AddcarryxU64(x142, x412, x415)
   721  	var x418 uint64
   722  	var x419 p521Uint1
   723  	x418, x419 = p521AddcarryxU64(x157, x414, 0x0)
   724  	var x420 uint64
   725  	x420, _ = p521AddcarryxU64(x158, x416, x419)
   726  	var x422 uint64
   727  	var x423 p521Uint1
   728  	x422, x423 = p521AddcarryxU64(x27, x13, 0x0)
   729  	var x424 uint64
   730  	x424, _ = p521AddcarryxU64(x28, x14, x423)
   731  	var x426 uint64
   732  	var x427 p521Uint1
   733  	x426, x427 = p521AddcarryxU64(x39, x422, 0x0)
   734  	var x428 uint64
   735  	x428, _ = p521AddcarryxU64(x40, x424, x427)
   736  	var x430 uint64
   737  	var x431 p521Uint1
   738  	x430, x431 = p521AddcarryxU64(x49, x426, 0x0)
   739  	var x432 uint64
   740  	x432, _ = p521AddcarryxU64(x50, x428, x431)
   741  	var x434 uint64
   742  	var x435 p521Uint1
   743  	x434, x435 = p521AddcarryxU64(x57, x430, 0x0)
   744  	var x436 uint64
   745  	x436, _ = p521AddcarryxU64(x58, x432, x435)
   746  	var x438 uint64
   747  	var x439 p521Uint1
   748  	x438, x439 = p521AddcarryxU64(x63, x434, 0x0)
   749  	var x440 uint64
   750  	x440, _ = p521AddcarryxU64(x64, x436, x439)
   751  	var x442 uint64
   752  	var x443 p521Uint1
   753  	x442, x443 = p521AddcarryxU64(x67, x438, 0x0)
   754  	var x444 uint64
   755  	x444, _ = p521AddcarryxU64(x68, x440, x443)
   756  	var x446 uint64
   757  	var x447 p521Uint1
   758  	x446, x447 = p521AddcarryxU64(x143, x442, 0x0)
   759  	var x448 uint64
   760  	x448, _ = p521AddcarryxU64(x144, x444, x447)
   761  	var x450 uint64
   762  	var x451 p521Uint1
   763  	x450, x451 = p521AddcarryxU64(x159, x446, 0x0)
   764  	var x452 uint64
   765  	x452, _ = p521AddcarryxU64(x160, x448, x451)
   766  	var x454 uint64
   767  	var x455 p521Uint1
   768  	x454, x455 = p521AddcarryxU64(x195, x450, 0x0)
   769  	var x456 uint64
   770  	x456, _ = p521AddcarryxU64(x196, x452, x455)
   771  	x458 := ((x454 >> 58) | ((x456 << 6) & 0xffffffffffffffff))
   772  	x459 := (x456 >> 58)
   773  	x460 := (x454 & 0x3ffffffffffffff)
   774  	var x461 uint64
   775  	var x462 p521Uint1
   776  	x461, x462 = p521AddcarryxU64(x458, x418, 0x0)
   777  	var x463 uint64
   778  	x463, _ = p521AddcarryxU64(x459, x420, x462)
   779  	x465 := ((x461 >> 58) | ((x463 << 6) & 0xffffffffffffffff))
   780  	x466 := (x463 >> 58)
   781  	x467 := (x461 & 0x3ffffffffffffff)
   782  	var x468 uint64
   783  	var x469 p521Uint1
   784  	x468, x469 = p521AddcarryxU64(x465, x386, 0x0)
   785  	var x470 uint64
   786  	x470, _ = p521AddcarryxU64(x466, x388, x469)
   787  	x472 := ((x468 >> 58) | ((x470 << 6) & 0xffffffffffffffff))
   788  	x473 := (x470 >> 58)
   789  	x474 := (x468 & 0x3ffffffffffffff)
   790  	var x475 uint64
   791  	var x476 p521Uint1
   792  	x475, x476 = p521AddcarryxU64(x472, x354, 0x0)
   793  	var x477 uint64
   794  	x477, _ = p521AddcarryxU64(x473, x356, x476)
   795  	x479 := ((x475 >> 58) | ((x477 << 6) & 0xffffffffffffffff))
   796  	x480 := (x477 >> 58)
   797  	x481 := (x475 & 0x3ffffffffffffff)
   798  	var x482 uint64
   799  	var x483 p521Uint1
   800  	x482, x483 = p521AddcarryxU64(x479, x322, 0x0)
   801  	var x484 uint64
   802  	x484, _ = p521AddcarryxU64(x480, x324, x483)
   803  	x486 := ((x482 >> 58) | ((x484 << 6) & 0xffffffffffffffff))
   804  	x487 := (x484 >> 58)
   805  	x488 := (x482 & 0x3ffffffffffffff)
   806  	var x489 uint64
   807  	var x490 p521Uint1
   808  	x489, x490 = p521AddcarryxU64(x486, x290, 0x0)
   809  	var x491 uint64
   810  	x491, _ = p521AddcarryxU64(x487, x292, x490)
   811  	x493 := ((x489 >> 58) | ((x491 << 6) & 0xffffffffffffffff))
   812  	x494 := (x491 >> 58)
   813  	x495 := (x489 & 0x3ffffffffffffff)
   814  	var x496 uint64
   815  	var x497 p521Uint1
   816  	x496, x497 = p521AddcarryxU64(x493, x258, 0x0)
   817  	var x498 uint64
   818  	x498, _ = p521AddcarryxU64(x494, x260, x497)
   819  	x500 := ((x496 >> 58) | ((x498 << 6) & 0xffffffffffffffff))
   820  	x501 := (x498 >> 58)
   821  	x502 := (x496 & 0x3ffffffffffffff)
   822  	var x503 uint64
   823  	var x504 p521Uint1
   824  	x503, x504 = p521AddcarryxU64(x500, x226, 0x0)
   825  	var x505 uint64
   826  	x505, _ = p521AddcarryxU64(x501, x228, x504)
   827  	x507 := ((x503 >> 57) | ((x505 << 7) & 0xffffffffffffffff))
   828  	x508 := (x505 >> 57)
   829  	x509 := (x503 & 0x1ffffffffffffff)
   830  	var x510 uint64
   831  	var x511 p521Uint1
   832  	x510, x511 = p521AddcarryxU64(x197, x507, 0x0)
   833  	x512 := (uint64(x511) + x508)
   834  	x513 := ((x510 >> 58) | ((x512 << 6) & 0xffffffffffffffff))
   835  	x514 := (x510 & 0x3ffffffffffffff)
   836  	x515 := (x513 + x460)
   837  	x516 := p521Uint1((x515 >> 58))
   838  	x517 := (x515 & 0x3ffffffffffffff)
   839  	x518 := (uint64(x516) + x467)
   840  	out1[0] = x514
   841  	out1[1] = x517
   842  	out1[2] = x518
   843  	out1[3] = x474
   844  	out1[4] = x481
   845  	out1[5] = x488
   846  	out1[6] = x495
   847  	out1[7] = x502
   848  	out1[8] = x509
   849  }
   850  
   851  // p521CarrySquare squares a field element and reduces the result.
   852  //
   853  // Postconditions:
   854  //   eval out1 mod m = (eval arg1 * eval arg1) mod m
   855  //
   856  // Input Bounds:
   857  //   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
   858  // Output Bounds:
   859  //   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
   860  func p521CarrySquare(out1 *[9]uint64, arg1 *[9]uint64) {
   861  	x1 := arg1[8]
   862  	x2 := (x1 * 0x2)
   863  	x3 := (arg1[8] * 0x2)
   864  	x4 := arg1[7]
   865  	x5 := (x4 * 0x2)
   866  	x6 := (arg1[7] * 0x2)
   867  	x7 := arg1[6]
   868  	x8 := (x7 * 0x2)
   869  	x9 := (arg1[6] * 0x2)
   870  	x10 := arg1[5]
   871  	x11 := (x10 * 0x2)
   872  	x12 := (arg1[5] * 0x2)
   873  	x13 := (arg1[4] * 0x2)
   874  	x14 := (arg1[3] * 0x2)
   875  	x15 := (arg1[2] * 0x2)
   876  	x16 := (arg1[1] * 0x2)
   877  	var x17 uint64
   878  	var x18 uint64
   879  	x18, x17 = bits.Mul64(arg1[8], (x1 * 0x2))
   880  	var x19 uint64
   881  	var x20 uint64
   882  	x20, x19 = bits.Mul64(arg1[7], (x2 * 0x2))
   883  	var x21 uint64
   884  	var x22 uint64
   885  	x22, x21 = bits.Mul64(arg1[7], (x4 * 0x2))
   886  	var x23 uint64
   887  	var x24 uint64
   888  	x24, x23 = bits.Mul64(arg1[6], (x2 * 0x2))
   889  	var x25 uint64
   890  	var x26 uint64
   891  	x26, x25 = bits.Mul64(arg1[6], (x5 * 0x2))
   892  	var x27 uint64
   893  	var x28 uint64
   894  	x28, x27 = bits.Mul64(arg1[6], (x7 * 0x2))
   895  	var x29 uint64
   896  	var x30 uint64
   897  	x30, x29 = bits.Mul64(arg1[5], (x2 * 0x2))
   898  	var x31 uint64
   899  	var x32 uint64
   900  	x32, x31 = bits.Mul64(arg1[5], (x5 * 0x2))
   901  	var x33 uint64
   902  	var x34 uint64
   903  	x34, x33 = bits.Mul64(arg1[5], (x8 * 0x2))
   904  	var x35 uint64
   905  	var x36 uint64
   906  	x36, x35 = bits.Mul64(arg1[5], (x10 * 0x2))
   907  	var x37 uint64
   908  	var x38 uint64
   909  	x38, x37 = bits.Mul64(arg1[4], (x2 * 0x2))
   910  	var x39 uint64
   911  	var x40 uint64
   912  	x40, x39 = bits.Mul64(arg1[4], (x5 * 0x2))
   913  	var x41 uint64
   914  	var x42 uint64
   915  	x42, x41 = bits.Mul64(arg1[4], (x8 * 0x2))
   916  	var x43 uint64
   917  	var x44 uint64
   918  	x44, x43 = bits.Mul64(arg1[4], (x11 * 0x2))
   919  	var x45 uint64
   920  	var x46 uint64
   921  	x46, x45 = bits.Mul64(arg1[4], arg1[4])
   922  	var x47 uint64
   923  	var x48 uint64
   924  	x48, x47 = bits.Mul64(arg1[3], (x2 * 0x2))
   925  	var x49 uint64
   926  	var x50 uint64
   927  	x50, x49 = bits.Mul64(arg1[3], (x5 * 0x2))
   928  	var x51 uint64
   929  	var x52 uint64
   930  	x52, x51 = bits.Mul64(arg1[3], (x8 * 0x2))
   931  	var x53 uint64
   932  	var x54 uint64
   933  	x54, x53 = bits.Mul64(arg1[3], x12)
   934  	var x55 uint64
   935  	var x56 uint64
   936  	x56, x55 = bits.Mul64(arg1[3], x13)
   937  	var x57 uint64
   938  	var x58 uint64
   939  	x58, x57 = bits.Mul64(arg1[3], arg1[3])
   940  	var x59 uint64
   941  	var x60 uint64
   942  	x60, x59 = bits.Mul64(arg1[2], (x2 * 0x2))
   943  	var x61 uint64
   944  	var x62 uint64
   945  	x62, x61 = bits.Mul64(arg1[2], (x5 * 0x2))
   946  	var x63 uint64
   947  	var x64 uint64
   948  	x64, x63 = bits.Mul64(arg1[2], x9)
   949  	var x65 uint64
   950  	var x66 uint64
   951  	x66, x65 = bits.Mul64(arg1[2], x12)
   952  	var x67 uint64
   953  	var x68 uint64
   954  	x68, x67 = bits.Mul64(arg1[2], x13)
   955  	var x69 uint64
   956  	var x70 uint64
   957  	x70, x69 = bits.Mul64(arg1[2], x14)
   958  	var x71 uint64
   959  	var x72 uint64
   960  	x72, x71 = bits.Mul64(arg1[2], arg1[2])
   961  	var x73 uint64
   962  	var x74 uint64
   963  	x74, x73 = bits.Mul64(arg1[1], (x2 * 0x2))
   964  	var x75 uint64
   965  	var x76 uint64
   966  	x76, x75 = bits.Mul64(arg1[1], x6)
   967  	var x77 uint64
   968  	var x78 uint64
   969  	x78, x77 = bits.Mul64(arg1[1], x9)
   970  	var x79 uint64
   971  	var x80 uint64
   972  	x80, x79 = bits.Mul64(arg1[1], x12)
   973  	var x81 uint64
   974  	var x82 uint64
   975  	x82, x81 = bits.Mul64(arg1[1], x13)
   976  	var x83 uint64
   977  	var x84 uint64
   978  	x84, x83 = bits.Mul64(arg1[1], x14)
   979  	var x85 uint64
   980  	var x86 uint64
   981  	x86, x85 = bits.Mul64(arg1[1], x15)
   982  	var x87 uint64
   983  	var x88 uint64
   984  	x88, x87 = bits.Mul64(arg1[1], arg1[1])
   985  	var x89 uint64
   986  	var x90 uint64
   987  	x90, x89 = bits.Mul64(arg1[0], x3)
   988  	var x91 uint64
   989  	var x92 uint64
   990  	x92, x91 = bits.Mul64(arg1[0], x6)
   991  	var x93 uint64
   992  	var x94 uint64
   993  	x94, x93 = bits.Mul64(arg1[0], x9)
   994  	var x95 uint64
   995  	var x96 uint64
   996  	x96, x95 = bits.Mul64(arg1[0], x12)
   997  	var x97 uint64
   998  	var x98 uint64
   999  	x98, x97 = bits.Mul64(arg1[0], x13)
  1000  	var x99 uint64
  1001  	var x100 uint64
  1002  	x100, x99 = bits.Mul64(arg1[0], x14)
  1003  	var x101 uint64
  1004  	var x102 uint64
  1005  	x102, x101 = bits.Mul64(arg1[0], x15)
  1006  	var x103 uint64
  1007  	var x104 uint64
  1008  	x104, x103 = bits.Mul64(arg1[0], x16)
  1009  	var x105 uint64
  1010  	var x106 uint64
  1011  	x106, x105 = bits.Mul64(arg1[0], arg1[0])
  1012  	var x107 uint64
  1013  	var x108 p521Uint1
  1014  	x107, x108 = p521AddcarryxU64(x51, x43, 0x0)
  1015  	var x109 uint64
  1016  	x109, _ = p521AddcarryxU64(x52, x44, x108)
  1017  	var x111 uint64
  1018  	var x112 p521Uint1
  1019  	x111, x112 = p521AddcarryxU64(x61, x107, 0x0)
  1020  	var x113 uint64
  1021  	x113, _ = p521AddcarryxU64(x62, x109, x112)
  1022  	var x115 uint64
  1023  	var x116 p521Uint1
  1024  	x115, x116 = p521AddcarryxU64(x73, x111, 0x0)
  1025  	var x117 uint64
  1026  	x117, _ = p521AddcarryxU64(x74, x113, x116)
  1027  	var x119 uint64
  1028  	var x120 p521Uint1
  1029  	x119, x120 = p521AddcarryxU64(x105, x115, 0x0)
  1030  	var x121 uint64
  1031  	x121, _ = p521AddcarryxU64(x106, x117, x120)
  1032  	x123 := ((x119 >> 58) | ((x121 << 6) & 0xffffffffffffffff))
  1033  	x124 := (x121 >> 58)
  1034  	x125 := (x119 & 0x3ffffffffffffff)
  1035  	var x126 uint64
  1036  	var x127 p521Uint1
  1037  	x126, x127 = p521AddcarryxU64(x53, x45, 0x0)
  1038  	var x128 uint64
  1039  	x128, _ = p521AddcarryxU64(x54, x46, x127)
  1040  	var x130 uint64
  1041  	var x131 p521Uint1
  1042  	x130, x131 = p521AddcarryxU64(x63, x126, 0x0)
  1043  	var x132 uint64
  1044  	x132, _ = p521AddcarryxU64(x64, x128, x131)
  1045  	var x134 uint64
  1046  	var x135 p521Uint1
  1047  	x134, x135 = p521AddcarryxU64(x75, x130, 0x0)
  1048  	var x136 uint64
  1049  	x136, _ = p521AddcarryxU64(x76, x132, x135)
  1050  	var x138 uint64
  1051  	var x139 p521Uint1
  1052  	x138, x139 = p521AddcarryxU64(x89, x134, 0x0)
  1053  	var x140 uint64
  1054  	x140, _ = p521AddcarryxU64(x90, x136, x139)
  1055  	var x142 uint64
  1056  	var x143 p521Uint1
  1057  	x142, x143 = p521AddcarryxU64(x55, x17, 0x0)
  1058  	var x144 uint64
  1059  	x144, _ = p521AddcarryxU64(x56, x18, x143)
  1060  	var x146 uint64
  1061  	var x147 p521Uint1
  1062  	x146, x147 = p521AddcarryxU64(x65, x142, 0x0)
  1063  	var x148 uint64
  1064  	x148, _ = p521AddcarryxU64(x66, x144, x147)
  1065  	var x150 uint64
  1066  	var x151 p521Uint1
  1067  	x150, x151 = p521AddcarryxU64(x77, x146, 0x0)
  1068  	var x152 uint64
  1069  	x152, _ = p521AddcarryxU64(x78, x148, x151)
  1070  	var x154 uint64
  1071  	var x155 p521Uint1
  1072  	x154, x155 = p521AddcarryxU64(x91, x150, 0x0)
  1073  	var x156 uint64
  1074  	x156, _ = p521AddcarryxU64(x92, x152, x155)
  1075  	var x158 uint64
  1076  	var x159 p521Uint1
  1077  	x158, x159 = p521AddcarryxU64(x57, x19, 0x0)
  1078  	var x160 uint64
  1079  	x160, _ = p521AddcarryxU64(x58, x20, x159)
  1080  	var x162 uint64
  1081  	var x163 p521Uint1
  1082  	x162, x163 = p521AddcarryxU64(x67, x158, 0x0)
  1083  	var x164 uint64
  1084  	x164, _ = p521AddcarryxU64(x68, x160, x163)
  1085  	var x166 uint64
  1086  	var x167 p521Uint1
  1087  	x166, x167 = p521AddcarryxU64(x79, x162, 0x0)
  1088  	var x168 uint64
  1089  	x168, _ = p521AddcarryxU64(x80, x164, x167)
  1090  	var x170 uint64
  1091  	var x171 p521Uint1
  1092  	x170, x171 = p521AddcarryxU64(x93, x166, 0x0)
  1093  	var x172 uint64
  1094  	x172, _ = p521AddcarryxU64(x94, x168, x171)
  1095  	var x174 uint64
  1096  	var x175 p521Uint1
  1097  	x174, x175 = p521AddcarryxU64(x23, x21, 0x0)
  1098  	var x176 uint64
  1099  	x176, _ = p521AddcarryxU64(x24, x22, x175)
  1100  	var x178 uint64
  1101  	var x179 p521Uint1
  1102  	x178, x179 = p521AddcarryxU64(x69, x174, 0x0)
  1103  	var x180 uint64
  1104  	x180, _ = p521AddcarryxU64(x70, x176, x179)
  1105  	var x182 uint64
  1106  	var x183 p521Uint1
  1107  	x182, x183 = p521AddcarryxU64(x81, x178, 0x0)
  1108  	var x184 uint64
  1109  	x184, _ = p521AddcarryxU64(x82, x180, x183)
  1110  	var x186 uint64
  1111  	var x187 p521Uint1
  1112  	x186, x187 = p521AddcarryxU64(x95, x182, 0x0)
  1113  	var x188 uint64
  1114  	x188, _ = p521AddcarryxU64(x96, x184, x187)
  1115  	var x190 uint64
  1116  	var x191 p521Uint1
  1117  	x190, x191 = p521AddcarryxU64(x29, x25, 0x0)
  1118  	var x192 uint64
  1119  	x192, _ = p521AddcarryxU64(x30, x26, x191)
  1120  	var x194 uint64
  1121  	var x195 p521Uint1
  1122  	x194, x195 = p521AddcarryxU64(x71, x190, 0x0)
  1123  	var x196 uint64
  1124  	x196, _ = p521AddcarryxU64(x72, x192, x195)
  1125  	var x198 uint64
  1126  	var x199 p521Uint1
  1127  	x198, x199 = p521AddcarryxU64(x83, x194, 0x0)
  1128  	var x200 uint64
  1129  	x200, _ = p521AddcarryxU64(x84, x196, x199)
  1130  	var x202 uint64
  1131  	var x203 p521Uint1
  1132  	x202, x203 = p521AddcarryxU64(x97, x198, 0x0)
  1133  	var x204 uint64
  1134  	x204, _ = p521AddcarryxU64(x98, x200, x203)
  1135  	var x206 uint64
  1136  	var x207 p521Uint1
  1137  	x206, x207 = p521AddcarryxU64(x31, x27, 0x0)
  1138  	var x208 uint64
  1139  	x208, _ = p521AddcarryxU64(x32, x28, x207)
  1140  	var x210 uint64
  1141  	var x211 p521Uint1
  1142  	x210, x211 = p521AddcarryxU64(x37, x206, 0x0)
  1143  	var x212 uint64
  1144  	x212, _ = p521AddcarryxU64(x38, x208, x211)
  1145  	var x214 uint64
  1146  	var x215 p521Uint1
  1147  	x214, x215 = p521AddcarryxU64(x85, x210, 0x0)
  1148  	var x216 uint64
  1149  	x216, _ = p521AddcarryxU64(x86, x212, x215)
  1150  	var x218 uint64
  1151  	var x219 p521Uint1
  1152  	x218, x219 = p521AddcarryxU64(x99, x214, 0x0)
  1153  	var x220 uint64
  1154  	x220, _ = p521AddcarryxU64(x100, x216, x219)
  1155  	var x222 uint64
  1156  	var x223 p521Uint1
  1157  	x222, x223 = p521AddcarryxU64(x39, x33, 0x0)
  1158  	var x224 uint64
  1159  	x224, _ = p521AddcarryxU64(x40, x34, x223)
  1160  	var x226 uint64
  1161  	var x227 p521Uint1
  1162  	x226, x227 = p521AddcarryxU64(x47, x222, 0x0)
  1163  	var x228 uint64
  1164  	x228, _ = p521AddcarryxU64(x48, x224, x227)
  1165  	var x230 uint64
  1166  	var x231 p521Uint1
  1167  	x230, x231 = p521AddcarryxU64(x87, x226, 0x0)
  1168  	var x232 uint64
  1169  	x232, _ = p521AddcarryxU64(x88, x228, x231)
  1170  	var x234 uint64
  1171  	var x235 p521Uint1
  1172  	x234, x235 = p521AddcarryxU64(x101, x230, 0x0)
  1173  	var x236 uint64
  1174  	x236, _ = p521AddcarryxU64(x102, x232, x235)
  1175  	var x238 uint64
  1176  	var x239 p521Uint1
  1177  	x238, x239 = p521AddcarryxU64(x41, x35, 0x0)
  1178  	var x240 uint64
  1179  	x240, _ = p521AddcarryxU64(x42, x36, x239)
  1180  	var x242 uint64
  1181  	var x243 p521Uint1
  1182  	x242, x243 = p521AddcarryxU64(x49, x238, 0x0)
  1183  	var x244 uint64
  1184  	x244, _ = p521AddcarryxU64(x50, x240, x243)
  1185  	var x246 uint64
  1186  	var x247 p521Uint1
  1187  	x246, x247 = p521AddcarryxU64(x59, x242, 0x0)
  1188  	var x248 uint64
  1189  	x248, _ = p521AddcarryxU64(x60, x244, x247)
  1190  	var x250 uint64
  1191  	var x251 p521Uint1
  1192  	x250, x251 = p521AddcarryxU64(x103, x246, 0x0)
  1193  	var x252 uint64
  1194  	x252, _ = p521AddcarryxU64(x104, x248, x251)
  1195  	var x254 uint64
  1196  	var x255 p521Uint1
  1197  	x254, x255 = p521AddcarryxU64(x123, x250, 0x0)
  1198  	var x256 uint64
  1199  	x256, _ = p521AddcarryxU64(x124, x252, x255)
  1200  	x258 := ((x254 >> 58) | ((x256 << 6) & 0xffffffffffffffff))
  1201  	x259 := (x256 >> 58)
  1202  	x260 := (x254 & 0x3ffffffffffffff)
  1203  	var x261 uint64
  1204  	var x262 p521Uint1
  1205  	x261, x262 = p521AddcarryxU64(x258, x234, 0x0)
  1206  	var x263 uint64
  1207  	x263, _ = p521AddcarryxU64(x259, x236, x262)
  1208  	x265 := ((x261 >> 58) | ((x263 << 6) & 0xffffffffffffffff))
  1209  	x266 := (x263 >> 58)
  1210  	x267 := (x261 & 0x3ffffffffffffff)
  1211  	var x268 uint64
  1212  	var x269 p521Uint1
  1213  	x268, x269 = p521AddcarryxU64(x265, x218, 0x0)
  1214  	var x270 uint64
  1215  	x270, _ = p521AddcarryxU64(x266, x220, x269)
  1216  	x272 := ((x268 >> 58) | ((x270 << 6) & 0xffffffffffffffff))
  1217  	x273 := (x270 >> 58)
  1218  	x274 := (x268 & 0x3ffffffffffffff)
  1219  	var x275 uint64
  1220  	var x276 p521Uint1
  1221  	x275, x276 = p521AddcarryxU64(x272, x202, 0x0)
  1222  	var x277 uint64
  1223  	x277, _ = p521AddcarryxU64(x273, x204, x276)
  1224  	x279 := ((x275 >> 58) | ((x277 << 6) & 0xffffffffffffffff))
  1225  	x280 := (x277 >> 58)
  1226  	x281 := (x275 & 0x3ffffffffffffff)
  1227  	var x282 uint64
  1228  	var x283 p521Uint1
  1229  	x282, x283 = p521AddcarryxU64(x279, x186, 0x0)
  1230  	var x284 uint64
  1231  	x284, _ = p521AddcarryxU64(x280, x188, x283)
  1232  	x286 := ((x282 >> 58) | ((x284 << 6) & 0xffffffffffffffff))
  1233  	x287 := (x284 >> 58)
  1234  	x288 := (x282 & 0x3ffffffffffffff)
  1235  	var x289 uint64
  1236  	var x290 p521Uint1
  1237  	x289, x290 = p521AddcarryxU64(x286, x170, 0x0)
  1238  	var x291 uint64
  1239  	x291, _ = p521AddcarryxU64(x287, x172, x290)
  1240  	x293 := ((x289 >> 58) | ((x291 << 6) & 0xffffffffffffffff))
  1241  	x294 := (x291 >> 58)
  1242  	x295 := (x289 & 0x3ffffffffffffff)
  1243  	var x296 uint64
  1244  	var x297 p521Uint1
  1245  	x296, x297 = p521AddcarryxU64(x293, x154, 0x0)
  1246  	var x298 uint64
  1247  	x298, _ = p521AddcarryxU64(x294, x156, x297)
  1248  	x300 := ((x296 >> 58) | ((x298 << 6) & 0xffffffffffffffff))
  1249  	x301 := (x298 >> 58)
  1250  	x302 := (x296 & 0x3ffffffffffffff)
  1251  	var x303 uint64
  1252  	var x304 p521Uint1
  1253  	x303, x304 = p521AddcarryxU64(x300, x138, 0x0)
  1254  	var x305 uint64
  1255  	x305, _ = p521AddcarryxU64(x301, x140, x304)
  1256  	x307 := ((x303 >> 57) | ((x305 << 7) & 0xffffffffffffffff))
  1257  	x308 := (x305 >> 57)
  1258  	x309 := (x303 & 0x1ffffffffffffff)
  1259  	var x310 uint64
  1260  	var x311 p521Uint1
  1261  	x310, x311 = p521AddcarryxU64(x125, x307, 0x0)
  1262  	x312 := (uint64(x311) + x308)
  1263  	x313 := ((x310 >> 58) | ((x312 << 6) & 0xffffffffffffffff))
  1264  	x314 := (x310 & 0x3ffffffffffffff)
  1265  	x315 := (x313 + x260)
  1266  	x316 := p521Uint1((x315 >> 58))
  1267  	x317 := (x315 & 0x3ffffffffffffff)
  1268  	x318 := (uint64(x316) + x267)
  1269  	out1[0] = x314
  1270  	out1[1] = x317
  1271  	out1[2] = x318
  1272  	out1[3] = x274
  1273  	out1[4] = x281
  1274  	out1[5] = x288
  1275  	out1[6] = x295
  1276  	out1[7] = x302
  1277  	out1[8] = x309
  1278  }
  1279  
  1280  // p521Carry reduces a field element.
  1281  //
  1282  // Postconditions:
  1283  //   eval out1 mod m = eval arg1 mod m
  1284  //
  1285  // Input Bounds:
  1286  //   arg1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
  1287  // Output Bounds:
  1288  //   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1289  func p521Carry(out1 *[9]uint64, arg1 *[9]uint64) {
  1290  	x1 := arg1[0]
  1291  	x2 := ((x1 >> 58) + arg1[1])
  1292  	x3 := ((x2 >> 58) + arg1[2])
  1293  	x4 := ((x3 >> 58) + arg1[3])
  1294  	x5 := ((x4 >> 58) + arg1[4])
  1295  	x6 := ((x5 >> 58) + arg1[5])
  1296  	x7 := ((x6 >> 58) + arg1[6])
  1297  	x8 := ((x7 >> 58) + arg1[7])
  1298  	x9 := ((x8 >> 58) + arg1[8])
  1299  	x10 := ((x1 & 0x3ffffffffffffff) + (x9 >> 57))
  1300  	x11 := (uint64(p521Uint1((x10 >> 58))) + (x2 & 0x3ffffffffffffff))
  1301  	x12 := (x10 & 0x3ffffffffffffff)
  1302  	x13 := (x11 & 0x3ffffffffffffff)
  1303  	x14 := (uint64(p521Uint1((x11 >> 58))) + (x3 & 0x3ffffffffffffff))
  1304  	x15 := (x4 & 0x3ffffffffffffff)
  1305  	x16 := (x5 & 0x3ffffffffffffff)
  1306  	x17 := (x6 & 0x3ffffffffffffff)
  1307  	x18 := (x7 & 0x3ffffffffffffff)
  1308  	x19 := (x8 & 0x3ffffffffffffff)
  1309  	x20 := (x9 & 0x1ffffffffffffff)
  1310  	out1[0] = x12
  1311  	out1[1] = x13
  1312  	out1[2] = x14
  1313  	out1[3] = x15
  1314  	out1[4] = x16
  1315  	out1[5] = x17
  1316  	out1[6] = x18
  1317  	out1[7] = x19
  1318  	out1[8] = x20
  1319  }
  1320  
  1321  // p521Add adds two field elements.
  1322  //
  1323  // Postconditions:
  1324  //   eval out1 mod m = (eval arg1 + eval arg2) mod m
  1325  //
  1326  // Input Bounds:
  1327  //   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1328  //   arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1329  // Output Bounds:
  1330  //   out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
  1331  func p521Add(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
  1332  	x1 := (arg1[0] + arg2[0])
  1333  	x2 := (arg1[1] + arg2[1])
  1334  	x3 := (arg1[2] + arg2[2])
  1335  	x4 := (arg1[3] + arg2[3])
  1336  	x5 := (arg1[4] + arg2[4])
  1337  	x6 := (arg1[5] + arg2[5])
  1338  	x7 := (arg1[6] + arg2[6])
  1339  	x8 := (arg1[7] + arg2[7])
  1340  	x9 := (arg1[8] + arg2[8])
  1341  	out1[0] = x1
  1342  	out1[1] = x2
  1343  	out1[2] = x3
  1344  	out1[3] = x4
  1345  	out1[4] = x5
  1346  	out1[5] = x6
  1347  	out1[6] = x7
  1348  	out1[7] = x8
  1349  	out1[8] = x9
  1350  }
  1351  
  1352  // p521Sub subtracts two field elements.
  1353  //
  1354  // Postconditions:
  1355  //   eval out1 mod m = (eval arg1 - eval arg2) mod m
  1356  //
  1357  // Input Bounds:
  1358  //   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1359  //   arg2: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1360  // Output Bounds:
  1361  //   out1: [[0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0xc00000000000000], [0x0 ~> 0x600000000000000]]
  1362  func p521Sub(out1 *[9]uint64, arg1 *[9]uint64, arg2 *[9]uint64) {
  1363  	x1 := ((0x7fffffffffffffe + arg1[0]) - arg2[0])
  1364  	x2 := ((0x7fffffffffffffe + arg1[1]) - arg2[1])
  1365  	x3 := ((0x7fffffffffffffe + arg1[2]) - arg2[2])
  1366  	x4 := ((0x7fffffffffffffe + arg1[3]) - arg2[3])
  1367  	x5 := ((0x7fffffffffffffe + arg1[4]) - arg2[4])
  1368  	x6 := ((0x7fffffffffffffe + arg1[5]) - arg2[5])
  1369  	x7 := ((0x7fffffffffffffe + arg1[6]) - arg2[6])
  1370  	x8 := ((0x7fffffffffffffe + arg1[7]) - arg2[7])
  1371  	x9 := ((0x3fffffffffffffe + arg1[8]) - arg2[8])
  1372  	out1[0] = x1
  1373  	out1[1] = x2
  1374  	out1[2] = x3
  1375  	out1[3] = x4
  1376  	out1[4] = x5
  1377  	out1[5] = x6
  1378  	out1[6] = x7
  1379  	out1[7] = x8
  1380  	out1[8] = x9
  1381  }
  1382  
  1383  // p521ToBytes serializes a field element to bytes in little-endian order.
  1384  //
  1385  // Postconditions:
  1386  //   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]
  1387  //
  1388  // Input Bounds:
  1389  //   arg1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1390  // Output Bounds:
  1391  //   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]]
  1392  func p521ToBytes(out1 *[66]uint8, arg1 *[9]uint64) {
  1393  	var x1 uint64
  1394  	var x2 p521Uint1
  1395  	p521SubborrowxU58(&x1, &x2, 0x0, arg1[0], 0x3ffffffffffffff)
  1396  	var x3 uint64
  1397  	var x4 p521Uint1
  1398  	p521SubborrowxU58(&x3, &x4, x2, arg1[1], 0x3ffffffffffffff)
  1399  	var x5 uint64
  1400  	var x6 p521Uint1
  1401  	p521SubborrowxU58(&x5, &x6, x4, arg1[2], 0x3ffffffffffffff)
  1402  	var x7 uint64
  1403  	var x8 p521Uint1
  1404  	p521SubborrowxU58(&x7, &x8, x6, arg1[3], 0x3ffffffffffffff)
  1405  	var x9 uint64
  1406  	var x10 p521Uint1
  1407  	p521SubborrowxU58(&x9, &x10, x8, arg1[4], 0x3ffffffffffffff)
  1408  	var x11 uint64
  1409  	var x12 p521Uint1
  1410  	p521SubborrowxU58(&x11, &x12, x10, arg1[5], 0x3ffffffffffffff)
  1411  	var x13 uint64
  1412  	var x14 p521Uint1
  1413  	p521SubborrowxU58(&x13, &x14, x12, arg1[6], 0x3ffffffffffffff)
  1414  	var x15 uint64
  1415  	var x16 p521Uint1
  1416  	p521SubborrowxU58(&x15, &x16, x14, arg1[7], 0x3ffffffffffffff)
  1417  	var x17 uint64
  1418  	var x18 p521Uint1
  1419  	p521SubborrowxU57(&x17, &x18, x16, arg1[8], 0x1ffffffffffffff)
  1420  	var x19 uint64
  1421  	p521CmovznzU64(&x19, x18, uint64(0x0), 0xffffffffffffffff)
  1422  	var x20 uint64
  1423  	var x21 p521Uint1
  1424  	p521AddcarryxU58(&x20, &x21, 0x0, x1, (x19 & 0x3ffffffffffffff))
  1425  	var x22 uint64
  1426  	var x23 p521Uint1
  1427  	p521AddcarryxU58(&x22, &x23, x21, x3, (x19 & 0x3ffffffffffffff))
  1428  	var x24 uint64
  1429  	var x25 p521Uint1
  1430  	p521AddcarryxU58(&x24, &x25, x23, x5, (x19 & 0x3ffffffffffffff))
  1431  	var x26 uint64
  1432  	var x27 p521Uint1
  1433  	p521AddcarryxU58(&x26, &x27, x25, x7, (x19 & 0x3ffffffffffffff))
  1434  	var x28 uint64
  1435  	var x29 p521Uint1
  1436  	p521AddcarryxU58(&x28, &x29, x27, x9, (x19 & 0x3ffffffffffffff))
  1437  	var x30 uint64
  1438  	var x31 p521Uint1
  1439  	p521AddcarryxU58(&x30, &x31, x29, x11, (x19 & 0x3ffffffffffffff))
  1440  	var x32 uint64
  1441  	var x33 p521Uint1
  1442  	p521AddcarryxU58(&x32, &x33, x31, x13, (x19 & 0x3ffffffffffffff))
  1443  	var x34 uint64
  1444  	var x35 p521Uint1
  1445  	p521AddcarryxU58(&x34, &x35, x33, x15, (x19 & 0x3ffffffffffffff))
  1446  	var x36 uint64
  1447  	var x37 p521Uint1
  1448  	p521AddcarryxU57(&x36, &x37, x35, x17, (x19 & 0x1ffffffffffffff))
  1449  	x38 := (x34 << 6)
  1450  	x39 := (x32 << 4)
  1451  	x40 := (x30 << 2)
  1452  	x41 := (x26 << 6)
  1453  	x42 := (x24 << 4)
  1454  	x43 := (x22 << 2)
  1455  	x44 := (uint8(x20) & 0xff)
  1456  	x45 := (x20 >> 8)
  1457  	x46 := (uint8(x45) & 0xff)
  1458  	x47 := (x45 >> 8)
  1459  	x48 := (uint8(x47) & 0xff)
  1460  	x49 := (x47 >> 8)
  1461  	x50 := (uint8(x49) & 0xff)
  1462  	x51 := (x49 >> 8)
  1463  	x52 := (uint8(x51) & 0xff)
  1464  	x53 := (x51 >> 8)
  1465  	x54 := (uint8(x53) & 0xff)
  1466  	x55 := (x53 >> 8)
  1467  	x56 := (uint8(x55) & 0xff)
  1468  	x57 := uint8((x55 >> 8))
  1469  	x58 := (x43 + uint64(x57))
  1470  	x59 := (uint8(x58) & 0xff)
  1471  	x60 := (x58 >> 8)
  1472  	x61 := (uint8(x60) & 0xff)
  1473  	x62 := (x60 >> 8)
  1474  	x63 := (uint8(x62) & 0xff)
  1475  	x64 := (x62 >> 8)
  1476  	x65 := (uint8(x64) & 0xff)
  1477  	x66 := (x64 >> 8)
  1478  	x67 := (uint8(x66) & 0xff)
  1479  	x68 := (x66 >> 8)
  1480  	x69 := (uint8(x68) & 0xff)
  1481  	x70 := (x68 >> 8)
  1482  	x71 := (uint8(x70) & 0xff)
  1483  	x72 := uint8((x70 >> 8))
  1484  	x73 := (x42 + uint64(x72))
  1485  	x74 := (uint8(x73) & 0xff)
  1486  	x75 := (x73 >> 8)
  1487  	x76 := (uint8(x75) & 0xff)
  1488  	x77 := (x75 >> 8)
  1489  	x78 := (uint8(x77) & 0xff)
  1490  	x79 := (x77 >> 8)
  1491  	x80 := (uint8(x79) & 0xff)
  1492  	x81 := (x79 >> 8)
  1493  	x82 := (uint8(x81) & 0xff)
  1494  	x83 := (x81 >> 8)
  1495  	x84 := (uint8(x83) & 0xff)
  1496  	x85 := (x83 >> 8)
  1497  	x86 := (uint8(x85) & 0xff)
  1498  	x87 := uint8((x85 >> 8))
  1499  	x88 := (x41 + uint64(x87))
  1500  	x89 := (uint8(x88) & 0xff)
  1501  	x90 := (x88 >> 8)
  1502  	x91 := (uint8(x90) & 0xff)
  1503  	x92 := (x90 >> 8)
  1504  	x93 := (uint8(x92) & 0xff)
  1505  	x94 := (x92 >> 8)
  1506  	x95 := (uint8(x94) & 0xff)
  1507  	x96 := (x94 >> 8)
  1508  	x97 := (uint8(x96) & 0xff)
  1509  	x98 := (x96 >> 8)
  1510  	x99 := (uint8(x98) & 0xff)
  1511  	x100 := (x98 >> 8)
  1512  	x101 := (uint8(x100) & 0xff)
  1513  	x102 := uint8((x100 >> 8))
  1514  	x103 := (uint8(x28) & 0xff)
  1515  	x104 := (x28 >> 8)
  1516  	x105 := (uint8(x104) & 0xff)
  1517  	x106 := (x104 >> 8)
  1518  	x107 := (uint8(x106) & 0xff)
  1519  	x108 := (x106 >> 8)
  1520  	x109 := (uint8(x108) & 0xff)
  1521  	x110 := (x108 >> 8)
  1522  	x111 := (uint8(x110) & 0xff)
  1523  	x112 := (x110 >> 8)
  1524  	x113 := (uint8(x112) & 0xff)
  1525  	x114 := (x112 >> 8)
  1526  	x115 := (uint8(x114) & 0xff)
  1527  	x116 := uint8((x114 >> 8))
  1528  	x117 := (x40 + uint64(x116))
  1529  	x118 := (uint8(x117) & 0xff)
  1530  	x119 := (x117 >> 8)
  1531  	x120 := (uint8(x119) & 0xff)
  1532  	x121 := (x119 >> 8)
  1533  	x122 := (uint8(x121) & 0xff)
  1534  	x123 := (x121 >> 8)
  1535  	x124 := (uint8(x123) & 0xff)
  1536  	x125 := (x123 >> 8)
  1537  	x126 := (uint8(x125) & 0xff)
  1538  	x127 := (x125 >> 8)
  1539  	x128 := (uint8(x127) & 0xff)
  1540  	x129 := (x127 >> 8)
  1541  	x130 := (uint8(x129) & 0xff)
  1542  	x131 := uint8((x129 >> 8))
  1543  	x132 := (x39 + uint64(x131))
  1544  	x133 := (uint8(x132) & 0xff)
  1545  	x134 := (x132 >> 8)
  1546  	x135 := (uint8(x134) & 0xff)
  1547  	x136 := (x134 >> 8)
  1548  	x137 := (uint8(x136) & 0xff)
  1549  	x138 := (x136 >> 8)
  1550  	x139 := (uint8(x138) & 0xff)
  1551  	x140 := (x138 >> 8)
  1552  	x141 := (uint8(x140) & 0xff)
  1553  	x142 := (x140 >> 8)
  1554  	x143 := (uint8(x142) & 0xff)
  1555  	x144 := (x142 >> 8)
  1556  	x145 := (uint8(x144) & 0xff)
  1557  	x146 := uint8((x144 >> 8))
  1558  	x147 := (x38 + uint64(x146))
  1559  	x148 := (uint8(x147) & 0xff)
  1560  	x149 := (x147 >> 8)
  1561  	x150 := (uint8(x149) & 0xff)
  1562  	x151 := (x149 >> 8)
  1563  	x152 := (uint8(x151) & 0xff)
  1564  	x153 := (x151 >> 8)
  1565  	x154 := (uint8(x153) & 0xff)
  1566  	x155 := (x153 >> 8)
  1567  	x156 := (uint8(x155) & 0xff)
  1568  	x157 := (x155 >> 8)
  1569  	x158 := (uint8(x157) & 0xff)
  1570  	x159 := (x157 >> 8)
  1571  	x160 := (uint8(x159) & 0xff)
  1572  	x161 := uint8((x159 >> 8))
  1573  	x162 := (uint8(x36) & 0xff)
  1574  	x163 := (x36 >> 8)
  1575  	x164 := (uint8(x163) & 0xff)
  1576  	x165 := (x163 >> 8)
  1577  	x166 := (uint8(x165) & 0xff)
  1578  	x167 := (x165 >> 8)
  1579  	x168 := (uint8(x167) & 0xff)
  1580  	x169 := (x167 >> 8)
  1581  	x170 := (uint8(x169) & 0xff)
  1582  	x171 := (x169 >> 8)
  1583  	x172 := (uint8(x171) & 0xff)
  1584  	x173 := (x171 >> 8)
  1585  	x174 := (uint8(x173) & 0xff)
  1586  	x175 := p521Uint1((x173 >> 8))
  1587  	out1[0] = x44
  1588  	out1[1] = x46
  1589  	out1[2] = x48
  1590  	out1[3] = x50
  1591  	out1[4] = x52
  1592  	out1[5] = x54
  1593  	out1[6] = x56
  1594  	out1[7] = x59
  1595  	out1[8] = x61
  1596  	out1[9] = x63
  1597  	out1[10] = x65
  1598  	out1[11] = x67
  1599  	out1[12] = x69
  1600  	out1[13] = x71
  1601  	out1[14] = x74
  1602  	out1[15] = x76
  1603  	out1[16] = x78
  1604  	out1[17] = x80
  1605  	out1[18] = x82
  1606  	out1[19] = x84
  1607  	out1[20] = x86
  1608  	out1[21] = x89
  1609  	out1[22] = x91
  1610  	out1[23] = x93
  1611  	out1[24] = x95
  1612  	out1[25] = x97
  1613  	out1[26] = x99
  1614  	out1[27] = x101
  1615  	out1[28] = x102
  1616  	out1[29] = x103
  1617  	out1[30] = x105
  1618  	out1[31] = x107
  1619  	out1[32] = x109
  1620  	out1[33] = x111
  1621  	out1[34] = x113
  1622  	out1[35] = x115
  1623  	out1[36] = x118
  1624  	out1[37] = x120
  1625  	out1[38] = x122
  1626  	out1[39] = x124
  1627  	out1[40] = x126
  1628  	out1[41] = x128
  1629  	out1[42] = x130
  1630  	out1[43] = x133
  1631  	out1[44] = x135
  1632  	out1[45] = x137
  1633  	out1[46] = x139
  1634  	out1[47] = x141
  1635  	out1[48] = x143
  1636  	out1[49] = x145
  1637  	out1[50] = x148
  1638  	out1[51] = x150
  1639  	out1[52] = x152
  1640  	out1[53] = x154
  1641  	out1[54] = x156
  1642  	out1[55] = x158
  1643  	out1[56] = x160
  1644  	out1[57] = x161
  1645  	out1[58] = x162
  1646  	out1[59] = x164
  1647  	out1[60] = x166
  1648  	out1[61] = x168
  1649  	out1[62] = x170
  1650  	out1[63] = x172
  1651  	out1[64] = x174
  1652  	out1[65] = uint8(x175)
  1653  }
  1654  
  1655  // p521FromBytes deserializes a field element from bytes in little-endian order.
  1656  //
  1657  // Postconditions:
  1658  //   eval out1 mod m = bytes_eval arg1 mod m
  1659  //
  1660  // Input Bounds:
  1661  //   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]]
  1662  // Output Bounds:
  1663  //   out1: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]
  1664  func p521FromBytes(out1 *[9]uint64, arg1 *[66]uint8) {
  1665  	x1 := (uint64(p521Uint1(arg1[65])) << 56)
  1666  	x2 := (uint64(arg1[64]) << 48)
  1667  	x3 := (uint64(arg1[63]) << 40)
  1668  	x4 := (uint64(arg1[62]) << 32)
  1669  	x5 := (uint64(arg1[61]) << 24)
  1670  	x6 := (uint64(arg1[60]) << 16)
  1671  	x7 := (uint64(arg1[59]) << 8)
  1672  	x8 := arg1[58]
  1673  	x9 := (uint64(arg1[57]) << 50)
  1674  	x10 := (uint64(arg1[56]) << 42)
  1675  	x11 := (uint64(arg1[55]) << 34)
  1676  	x12 := (uint64(arg1[54]) << 26)
  1677  	x13 := (uint64(arg1[53]) << 18)
  1678  	x14 := (uint64(arg1[52]) << 10)
  1679  	x15 := (uint64(arg1[51]) << 2)
  1680  	x16 := (uint64(arg1[50]) << 52)
  1681  	x17 := (uint64(arg1[49]) << 44)
  1682  	x18 := (uint64(arg1[48]) << 36)
  1683  	x19 := (uint64(arg1[47]) << 28)
  1684  	x20 := (uint64(arg1[46]) << 20)
  1685  	x21 := (uint64(arg1[45]) << 12)
  1686  	x22 := (uint64(arg1[44]) << 4)
  1687  	x23 := (uint64(arg1[43]) << 54)
  1688  	x24 := (uint64(arg1[42]) << 46)
  1689  	x25 := (uint64(arg1[41]) << 38)
  1690  	x26 := (uint64(arg1[40]) << 30)
  1691  	x27 := (uint64(arg1[39]) << 22)
  1692  	x28 := (uint64(arg1[38]) << 14)
  1693  	x29 := (uint64(arg1[37]) << 6)
  1694  	x30 := (uint64(arg1[36]) << 56)
  1695  	x31 := (uint64(arg1[35]) << 48)
  1696  	x32 := (uint64(arg1[34]) << 40)
  1697  	x33 := (uint64(arg1[33]) << 32)
  1698  	x34 := (uint64(arg1[32]) << 24)
  1699  	x35 := (uint64(arg1[31]) << 16)
  1700  	x36 := (uint64(arg1[30]) << 8)
  1701  	x37 := arg1[29]
  1702  	x38 := (uint64(arg1[28]) << 50)
  1703  	x39 := (uint64(arg1[27]) << 42)
  1704  	x40 := (uint64(arg1[26]) << 34)
  1705  	x41 := (uint64(arg1[25]) << 26)
  1706  	x42 := (uint64(arg1[24]) << 18)
  1707  	x43 := (uint64(arg1[23]) << 10)
  1708  	x44 := (uint64(arg1[22]) << 2)
  1709  	x45 := (uint64(arg1[21]) << 52)
  1710  	x46 := (uint64(arg1[20]) << 44)
  1711  	x47 := (uint64(arg1[19]) << 36)
  1712  	x48 := (uint64(arg1[18]) << 28)
  1713  	x49 := (uint64(arg1[17]) << 20)
  1714  	x50 := (uint64(arg1[16]) << 12)
  1715  	x51 := (uint64(arg1[15]) << 4)
  1716  	x52 := (uint64(arg1[14]) << 54)
  1717  	x53 := (uint64(arg1[13]) << 46)
  1718  	x54 := (uint64(arg1[12]) << 38)
  1719  	x55 := (uint64(arg1[11]) << 30)
  1720  	x56 := (uint64(arg1[10]) << 22)
  1721  	x57 := (uint64(arg1[9]) << 14)
  1722  	x58 := (uint64(arg1[8]) << 6)
  1723  	x59 := (uint64(arg1[7]) << 56)
  1724  	x60 := (uint64(arg1[6]) << 48)
  1725  	x61 := (uint64(arg1[5]) << 40)
  1726  	x62 := (uint64(arg1[4]) << 32)
  1727  	x63 := (uint64(arg1[3]) << 24)
  1728  	x64 := (uint64(arg1[2]) << 16)
  1729  	x65 := (uint64(arg1[1]) << 8)
  1730  	x66 := arg1[0]
  1731  	x67 := (x65 + uint64(x66))
  1732  	x68 := (x64 + x67)
  1733  	x69 := (x63 + x68)
  1734  	x70 := (x62 + x69)
  1735  	x71 := (x61 + x70)
  1736  	x72 := (x60 + x71)
  1737  	x73 := (x59 + x72)
  1738  	x74 := (x73 & 0x3ffffffffffffff)
  1739  	x75 := uint8((x73 >> 58))
  1740  	x76 := (x58 + uint64(x75))
  1741  	x77 := (x57 + x76)
  1742  	x78 := (x56 + x77)
  1743  	x79 := (x55 + x78)
  1744  	x80 := (x54 + x79)
  1745  	x81 := (x53 + x80)
  1746  	x82 := (x52 + x81)
  1747  	x83 := (x82 & 0x3ffffffffffffff)
  1748  	x84 := uint8((x82 >> 58))
  1749  	x85 := (x51 + uint64(x84))
  1750  	x86 := (x50 + x85)
  1751  	x87 := (x49 + x86)
  1752  	x88 := (x48 + x87)
  1753  	x89 := (x47 + x88)
  1754  	x90 := (x46 + x89)
  1755  	x91 := (x45 + x90)
  1756  	x92 := (x91 & 0x3ffffffffffffff)
  1757  	x93 := uint8((x91 >> 58))
  1758  	x94 := (x44 + uint64(x93))
  1759  	x95 := (x43 + x94)
  1760  	x96 := (x42 + x95)
  1761  	x97 := (x41 + x96)
  1762  	x98 := (x40 + x97)
  1763  	x99 := (x39 + x98)
  1764  	x100 := (x38 + x99)
  1765  	x101 := (x36 + uint64(x37))
  1766  	x102 := (x35 + x101)
  1767  	x103 := (x34 + x102)
  1768  	x104 := (x33 + x103)
  1769  	x105 := (x32 + x104)
  1770  	x106 := (x31 + x105)
  1771  	x107 := (x30 + x106)
  1772  	x108 := (x107 & 0x3ffffffffffffff)
  1773  	x109 := uint8((x107 >> 58))
  1774  	x110 := (x29 + uint64(x109))
  1775  	x111 := (x28 + x110)
  1776  	x112 := (x27 + x111)
  1777  	x113 := (x26 + x112)
  1778  	x114 := (x25 + x113)
  1779  	x115 := (x24 + x114)
  1780  	x116 := (x23 + x115)
  1781  	x117 := (x116 & 0x3ffffffffffffff)
  1782  	x118 := uint8((x116 >> 58))
  1783  	x119 := (x22 + uint64(x118))
  1784  	x120 := (x21 + x119)
  1785  	x121 := (x20 + x120)
  1786  	x122 := (x19 + x121)
  1787  	x123 := (x18 + x122)
  1788  	x124 := (x17 + x123)
  1789  	x125 := (x16 + x124)
  1790  	x126 := (x125 & 0x3ffffffffffffff)
  1791  	x127 := uint8((x125 >> 58))
  1792  	x128 := (x15 + uint64(x127))
  1793  	x129 := (x14 + x128)
  1794  	x130 := (x13 + x129)
  1795  	x131 := (x12 + x130)
  1796  	x132 := (x11 + x131)
  1797  	x133 := (x10 + x132)
  1798  	x134 := (x9 + x133)
  1799  	x135 := (x7 + uint64(x8))
  1800  	x136 := (x6 + x135)
  1801  	x137 := (x5 + x136)
  1802  	x138 := (x4 + x137)
  1803  	x139 := (x3 + x138)
  1804  	x140 := (x2 + x139)
  1805  	x141 := (x1 + x140)
  1806  	out1[0] = x74
  1807  	out1[1] = x83
  1808  	out1[2] = x92
  1809  	out1[3] = x100
  1810  	out1[4] = x108
  1811  	out1[5] = x117
  1812  	out1[6] = x126
  1813  	out1[7] = x134
  1814  	out1[8] = x141
  1815  }
  1816  
  1817  // p521Selectznz is a multi-limb conditional select.
  1818  //
  1819  // Postconditions:
  1820  //   eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
  1821  //
  1822  // Input Bounds:
  1823  //   arg1: [0x0 ~> 0x1]
  1824  //   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  1825  //   arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  1826  // Output Bounds:
  1827  //   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
  1828  func p521Selectznz(out1 *[9]uint64, arg1 p521Uint1, arg2 *[9]uint64, arg3 *[9]uint64) {
  1829  	var x1 uint64
  1830  	p521CmovznzU64(&x1, arg1, arg2[0], arg3[0])
  1831  	var x2 uint64
  1832  	p521CmovznzU64(&x2, arg1, arg2[1], arg3[1])
  1833  	var x3 uint64
  1834  	p521CmovznzU64(&x3, arg1, arg2[2], arg3[2])
  1835  	var x4 uint64
  1836  	p521CmovznzU64(&x4, arg1, arg2[3], arg3[3])
  1837  	var x5 uint64
  1838  	p521CmovznzU64(&x5, arg1, arg2[4], arg3[4])
  1839  	var x6 uint64
  1840  	p521CmovznzU64(&x6, arg1, arg2[5], arg3[5])
  1841  	var x7 uint64
  1842  	p521CmovznzU64(&x7, arg1, arg2[6], arg3[6])
  1843  	var x8 uint64
  1844  	p521CmovznzU64(&x8, arg1, arg2[7], arg3[7])
  1845  	var x9 uint64
  1846  	p521CmovznzU64(&x9, arg1, arg2[8], arg3[8])
  1847  	out1[0] = x1
  1848  	out1[1] = x2
  1849  	out1[2] = x3
  1850  	out1[3] = x4
  1851  	out1[4] = x5
  1852  	out1[5] = x6
  1853  	out1[6] = x7
  1854  	out1[7] = x8
  1855  	out1[8] = x9
  1856  }
  1857  

View as plain text