1// Code generated by Fiat Cryptography. DO NOT EDIT.
2//
3// Autogenerated: word_by_word_montgomery --lang Go --no-wide-int --cmovznz-by-mul --relax-primitive-carry-to-bitwidth 32,64 --internal-static --public-function-case camelCase --public-type-case camelCase --private-function-case camelCase --private-type-case camelCase --doc-text-before-function-name '' --doc-newline-before-package-declaration --doc-prepend-header 'Code generated by Fiat Cryptography. DO NOT EDIT.' --package-name fiat --no-prefix-fiat p384 64 '2^384 - 2^128 - 2^96 + 2^32 - 1' mul square add sub one from_montgomery to_montgomery selectznz to_bytes from_bytes
4//
5// curve description: p384
6//
7// machine_wordsize = 64 (from "64")
8//
9// requested operations: mul, square, add, sub, one, from_montgomery, to_montgomery, selectznz, to_bytes, from_bytes
10//
11// m = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffeffffffff0000000000000000ffffffff (from "2^384 - 2^128 - 2^96 + 2^32 - 1")
12//
13//
14//
15// NOTE: In addition to the bounds specified above each function, all
16//
17//   functions synthesized for this Montgomery arithmetic require the
18//
19//   input to be strictly less than the prime modulus (m), and also
20//
21//   require the input to be in the unique saturated representation.
22//
23//   All functions also ensure that these two properties are true of
24//
25//   return values.
26//
27//
28//
29// Computed values:
30//
31//   eval z = z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140)
32//
33//   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)
34//
35//   twos_complement_eval z = let x1 := z[0] + (z[1] << 64) + (z[2] << 128) + (z[3] << 192) + (z[4] << 256) + (z[5] << 0x140) in
36//
37//                            if x1 & (2^384-1) < 2^383 then x1 & (2^384-1) else (x1 & (2^384-1)) - 2^384
38
39package fiat
40
41import "math/bits"
42
43type p384Uint1 uint64 // We use uint64 instead of a more narrow type for performance reasons; see https://github.com/mit-plv/fiat-crypto/pull/1006#issuecomment-892625927
44type p384Int1 int64   // We use uint64 instead of a more narrow type for performance reasons; see https://github.com/mit-plv/fiat-crypto/pull/1006#issuecomment-892625927
45
46// The type p384MontgomeryDomainFieldElement is a field element in the Montgomery domain.
47//
48// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
49type p384MontgomeryDomainFieldElement [6]uint64
50
51// The type p384NonMontgomeryDomainFieldElement is a field element NOT in the Montgomery domain.
52//
53// Bounds: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
54type p384NonMontgomeryDomainFieldElement [6]uint64
55
56// p384CmovznzU64 is a single-word conditional move.
57//
58// Postconditions:
59//
60//	out1 = (if arg1 = 0 then arg2 else arg3)
61//
62// Input Bounds:
63//
64//	arg1: [0x0 ~> 0x1]
65//	arg2: [0x0 ~> 0xffffffffffffffff]
66//	arg3: [0x0 ~> 0xffffffffffffffff]
67//
68// Output Bounds:
69//
70//	out1: [0x0 ~> 0xffffffffffffffff]
71func p384CmovznzU64(out1 *uint64, arg1 p384Uint1, arg2 uint64, arg3 uint64) {
72	x1 := (uint64(arg1) * 0xffffffffffffffff)
73	x2 := ((x1 & arg3) | ((^x1) & arg2))
74	*out1 = x2
75}
76
77// p384Mul multiplies two field elements in the Montgomery domain.
78//
79// Preconditions:
80//
81//	0 ≤ eval arg1 < m
82//	0 ≤ eval arg2 < m
83//
84// Postconditions:
85//
86//	eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
87//	0 ≤ eval out1 < m
88func p384Mul(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement) {
89	x1 := arg1[1]
90	x2 := arg1[2]
91	x3 := arg1[3]
92	x4 := arg1[4]
93	x5 := arg1[5]
94	x6 := arg1[0]
95	var x7 uint64
96	var x8 uint64
97	x8, x7 = bits.Mul64(x6, arg2[5])
98	var x9 uint64
99	var x10 uint64
100	x10, x9 = bits.Mul64(x6, arg2[4])
101	var x11 uint64
102	var x12 uint64
103	x12, x11 = bits.Mul64(x6, arg2[3])
104	var x13 uint64
105	var x14 uint64
106	x14, x13 = bits.Mul64(x6, arg2[2])
107	var x15 uint64
108	var x16 uint64
109	x16, x15 = bits.Mul64(x6, arg2[1])
110	var x17 uint64
111	var x18 uint64
112	x18, x17 = bits.Mul64(x6, arg2[0])
113	var x19 uint64
114	var x20 uint64
115	x19, x20 = bits.Add64(x18, x15, uint64(0x0))
116	var x21 uint64
117	var x22 uint64
118	x21, x22 = bits.Add64(x16, x13, uint64(p384Uint1(x20)))
119	var x23 uint64
120	var x24 uint64
121	x23, x24 = bits.Add64(x14, x11, uint64(p384Uint1(x22)))
122	var x25 uint64
123	var x26 uint64
124	x25, x26 = bits.Add64(x12, x9, uint64(p384Uint1(x24)))
125	var x27 uint64
126	var x28 uint64
127	x27, x28 = bits.Add64(x10, x7, uint64(p384Uint1(x26)))
128	x29 := (uint64(p384Uint1(x28)) + x8)
129	var x30 uint64
130	_, x30 = bits.Mul64(x17, 0x100000001)
131	var x32 uint64
132	var x33 uint64
133	x33, x32 = bits.Mul64(x30, 0xffffffffffffffff)
134	var x34 uint64
135	var x35 uint64
136	x35, x34 = bits.Mul64(x30, 0xffffffffffffffff)
137	var x36 uint64
138	var x37 uint64
139	x37, x36 = bits.Mul64(x30, 0xffffffffffffffff)
140	var x38 uint64
141	var x39 uint64
142	x39, x38 = bits.Mul64(x30, 0xfffffffffffffffe)
143	var x40 uint64
144	var x41 uint64
145	x41, x40 = bits.Mul64(x30, 0xffffffff00000000)
146	var x42 uint64
147	var x43 uint64
148	x43, x42 = bits.Mul64(x30, 0xffffffff)
149	var x44 uint64
150	var x45 uint64
151	x44, x45 = bits.Add64(x43, x40, uint64(0x0))
152	var x46 uint64
153	var x47 uint64
154	x46, x47 = bits.Add64(x41, x38, uint64(p384Uint1(x45)))
155	var x48 uint64
156	var x49 uint64
157	x48, x49 = bits.Add64(x39, x36, uint64(p384Uint1(x47)))
158	var x50 uint64
159	var x51 uint64
160	x50, x51 = bits.Add64(x37, x34, uint64(p384Uint1(x49)))
161	var x52 uint64
162	var x53 uint64
163	x52, x53 = bits.Add64(x35, x32, uint64(p384Uint1(x51)))
164	x54 := (uint64(p384Uint1(x53)) + x33)
165	var x56 uint64
166	_, x56 = bits.Add64(x17, x42, uint64(0x0))
167	var x57 uint64
168	var x58 uint64
169	x57, x58 = bits.Add64(x19, x44, uint64(p384Uint1(x56)))
170	var x59 uint64
171	var x60 uint64
172	x59, x60 = bits.Add64(x21, x46, uint64(p384Uint1(x58)))
173	var x61 uint64
174	var x62 uint64
175	x61, x62 = bits.Add64(x23, x48, uint64(p384Uint1(x60)))
176	var x63 uint64
177	var x64 uint64
178	x63, x64 = bits.Add64(x25, x50, uint64(p384Uint1(x62)))
179	var x65 uint64
180	var x66 uint64
181	x65, x66 = bits.Add64(x27, x52, uint64(p384Uint1(x64)))
182	var x67 uint64
183	var x68 uint64
184	x67, x68 = bits.Add64(x29, x54, uint64(p384Uint1(x66)))
185	var x69 uint64
186	var x70 uint64
187	x70, x69 = bits.Mul64(x1, arg2[5])
188	var x71 uint64
189	var x72 uint64
190	x72, x71 = bits.Mul64(x1, arg2[4])
191	var x73 uint64
192	var x74 uint64
193	x74, x73 = bits.Mul64(x1, arg2[3])
194	var x75 uint64
195	var x76 uint64
196	x76, x75 = bits.Mul64(x1, arg2[2])
197	var x77 uint64
198	var x78 uint64
199	x78, x77 = bits.Mul64(x1, arg2[1])
200	var x79 uint64
201	var x80 uint64
202	x80, x79 = bits.Mul64(x1, arg2[0])
203	var x81 uint64
204	var x82 uint64
205	x81, x82 = bits.Add64(x80, x77, uint64(0x0))
206	var x83 uint64
207	var x84 uint64
208	x83, x84 = bits.Add64(x78, x75, uint64(p384Uint1(x82)))
209	var x85 uint64
210	var x86 uint64
211	x85, x86 = bits.Add64(x76, x73, uint64(p384Uint1(x84)))
212	var x87 uint64
213	var x88 uint64
214	x87, x88 = bits.Add64(x74, x71, uint64(p384Uint1(x86)))
215	var x89 uint64
216	var x90 uint64
217	x89, x90 = bits.Add64(x72, x69, uint64(p384Uint1(x88)))
218	x91 := (uint64(p384Uint1(x90)) + x70)
219	var x92 uint64
220	var x93 uint64
221	x92, x93 = bits.Add64(x57, x79, uint64(0x0))
222	var x94 uint64
223	var x95 uint64
224	x94, x95 = bits.Add64(x59, x81, uint64(p384Uint1(x93)))
225	var x96 uint64
226	var x97 uint64
227	x96, x97 = bits.Add64(x61, x83, uint64(p384Uint1(x95)))
228	var x98 uint64
229	var x99 uint64
230	x98, x99 = bits.Add64(x63, x85, uint64(p384Uint1(x97)))
231	var x100 uint64
232	var x101 uint64
233	x100, x101 = bits.Add64(x65, x87, uint64(p384Uint1(x99)))
234	var x102 uint64
235	var x103 uint64
236	x102, x103 = bits.Add64(x67, x89, uint64(p384Uint1(x101)))
237	var x104 uint64
238	var x105 uint64
239	x104, x105 = bits.Add64(uint64(p384Uint1(x68)), x91, uint64(p384Uint1(x103)))
240	var x106 uint64
241	_, x106 = bits.Mul64(x92, 0x100000001)
242	var x108 uint64
243	var x109 uint64
244	x109, x108 = bits.Mul64(x106, 0xffffffffffffffff)
245	var x110 uint64
246	var x111 uint64
247	x111, x110 = bits.Mul64(x106, 0xffffffffffffffff)
248	var x112 uint64
249	var x113 uint64
250	x113, x112 = bits.Mul64(x106, 0xffffffffffffffff)
251	var x114 uint64
252	var x115 uint64
253	x115, x114 = bits.Mul64(x106, 0xfffffffffffffffe)
254	var x116 uint64
255	var x117 uint64
256	x117, x116 = bits.Mul64(x106, 0xffffffff00000000)
257	var x118 uint64
258	var x119 uint64
259	x119, x118 = bits.Mul64(x106, 0xffffffff)
260	var x120 uint64
261	var x121 uint64
262	x120, x121 = bits.Add64(x119, x116, uint64(0x0))
263	var x122 uint64
264	var x123 uint64
265	x122, x123 = bits.Add64(x117, x114, uint64(p384Uint1(x121)))
266	var x124 uint64
267	var x125 uint64
268	x124, x125 = bits.Add64(x115, x112, uint64(p384Uint1(x123)))
269	var x126 uint64
270	var x127 uint64
271	x126, x127 = bits.Add64(x113, x110, uint64(p384Uint1(x125)))
272	var x128 uint64
273	var x129 uint64
274	x128, x129 = bits.Add64(x111, x108, uint64(p384Uint1(x127)))
275	x130 := (uint64(p384Uint1(x129)) + x109)
276	var x132 uint64
277	_, x132 = bits.Add64(x92, x118, uint64(0x0))
278	var x133 uint64
279	var x134 uint64
280	x133, x134 = bits.Add64(x94, x120, uint64(p384Uint1(x132)))
281	var x135 uint64
282	var x136 uint64
283	x135, x136 = bits.Add64(x96, x122, uint64(p384Uint1(x134)))
284	var x137 uint64
285	var x138 uint64
286	x137, x138 = bits.Add64(x98, x124, uint64(p384Uint1(x136)))
287	var x139 uint64
288	var x140 uint64
289	x139, x140 = bits.Add64(x100, x126, uint64(p384Uint1(x138)))
290	var x141 uint64
291	var x142 uint64
292	x141, x142 = bits.Add64(x102, x128, uint64(p384Uint1(x140)))
293	var x143 uint64
294	var x144 uint64
295	x143, x144 = bits.Add64(x104, x130, uint64(p384Uint1(x142)))
296	x145 := (uint64(p384Uint1(x144)) + uint64(p384Uint1(x105)))
297	var x146 uint64
298	var x147 uint64
299	x147, x146 = bits.Mul64(x2, arg2[5])
300	var x148 uint64
301	var x149 uint64
302	x149, x148 = bits.Mul64(x2, arg2[4])
303	var x150 uint64
304	var x151 uint64
305	x151, x150 = bits.Mul64(x2, arg2[3])
306	var x152 uint64
307	var x153 uint64
308	x153, x152 = bits.Mul64(x2, arg2[2])
309	var x154 uint64
310	var x155 uint64
311	x155, x154 = bits.Mul64(x2, arg2[1])
312	var x156 uint64
313	var x157 uint64
314	x157, x156 = bits.Mul64(x2, arg2[0])
315	var x158 uint64
316	var x159 uint64
317	x158, x159 = bits.Add64(x157, x154, uint64(0x0))
318	var x160 uint64
319	var x161 uint64
320	x160, x161 = bits.Add64(x155, x152, uint64(p384Uint1(x159)))
321	var x162 uint64
322	var x163 uint64
323	x162, x163 = bits.Add64(x153, x150, uint64(p384Uint1(x161)))
324	var x164 uint64
325	var x165 uint64
326	x164, x165 = bits.Add64(x151, x148, uint64(p384Uint1(x163)))
327	var x166 uint64
328	var x167 uint64
329	x166, x167 = bits.Add64(x149, x146, uint64(p384Uint1(x165)))
330	x168 := (uint64(p384Uint1(x167)) + x147)
331	var x169 uint64
332	var x170 uint64
333	x169, x170 = bits.Add64(x133, x156, uint64(0x0))
334	var x171 uint64
335	var x172 uint64
336	x171, x172 = bits.Add64(x135, x158, uint64(p384Uint1(x170)))
337	var x173 uint64
338	var x174 uint64
339	x173, x174 = bits.Add64(x137, x160, uint64(p384Uint1(x172)))
340	var x175 uint64
341	var x176 uint64
342	x175, x176 = bits.Add64(x139, x162, uint64(p384Uint1(x174)))
343	var x177 uint64
344	var x178 uint64
345	x177, x178 = bits.Add64(x141, x164, uint64(p384Uint1(x176)))
346	var x179 uint64
347	var x180 uint64
348	x179, x180 = bits.Add64(x143, x166, uint64(p384Uint1(x178)))
349	var x181 uint64
350	var x182 uint64
351	x181, x182 = bits.Add64(x145, x168, uint64(p384Uint1(x180)))
352	var x183 uint64
353	_, x183 = bits.Mul64(x169, 0x100000001)
354	var x185 uint64
355	var x186 uint64
356	x186, x185 = bits.Mul64(x183, 0xffffffffffffffff)
357	var x187 uint64
358	var x188 uint64
359	x188, x187 = bits.Mul64(x183, 0xffffffffffffffff)
360	var x189 uint64
361	var x190 uint64
362	x190, x189 = bits.Mul64(x183, 0xffffffffffffffff)
363	var x191 uint64
364	var x192 uint64
365	x192, x191 = bits.Mul64(x183, 0xfffffffffffffffe)
366	var x193 uint64
367	var x194 uint64
368	x194, x193 = bits.Mul64(x183, 0xffffffff00000000)
369	var x195 uint64
370	var x196 uint64
371	x196, x195 = bits.Mul64(x183, 0xffffffff)
372	var x197 uint64
373	var x198 uint64
374	x197, x198 = bits.Add64(x196, x193, uint64(0x0))
375	var x199 uint64
376	var x200 uint64
377	x199, x200 = bits.Add64(x194, x191, uint64(p384Uint1(x198)))
378	var x201 uint64
379	var x202 uint64
380	x201, x202 = bits.Add64(x192, x189, uint64(p384Uint1(x200)))
381	var x203 uint64
382	var x204 uint64
383	x203, x204 = bits.Add64(x190, x187, uint64(p384Uint1(x202)))
384	var x205 uint64
385	var x206 uint64
386	x205, x206 = bits.Add64(x188, x185, uint64(p384Uint1(x204)))
387	x207 := (uint64(p384Uint1(x206)) + x186)
388	var x209 uint64
389	_, x209 = bits.Add64(x169, x195, uint64(0x0))
390	var x210 uint64
391	var x211 uint64
392	x210, x211 = bits.Add64(x171, x197, uint64(p384Uint1(x209)))
393	var x212 uint64
394	var x213 uint64
395	x212, x213 = bits.Add64(x173, x199, uint64(p384Uint1(x211)))
396	var x214 uint64
397	var x215 uint64
398	x214, x215 = bits.Add64(x175, x201, uint64(p384Uint1(x213)))
399	var x216 uint64
400	var x217 uint64
401	x216, x217 = bits.Add64(x177, x203, uint64(p384Uint1(x215)))
402	var x218 uint64
403	var x219 uint64
404	x218, x219 = bits.Add64(x179, x205, uint64(p384Uint1(x217)))
405	var x220 uint64
406	var x221 uint64
407	x220, x221 = bits.Add64(x181, x207, uint64(p384Uint1(x219)))
408	x222 := (uint64(p384Uint1(x221)) + uint64(p384Uint1(x182)))
409	var x223 uint64
410	var x224 uint64
411	x224, x223 = bits.Mul64(x3, arg2[5])
412	var x225 uint64
413	var x226 uint64
414	x226, x225 = bits.Mul64(x3, arg2[4])
415	var x227 uint64
416	var x228 uint64
417	x228, x227 = bits.Mul64(x3, arg2[3])
418	var x229 uint64
419	var x230 uint64
420	x230, x229 = bits.Mul64(x3, arg2[2])
421	var x231 uint64
422	var x232 uint64
423	x232, x231 = bits.Mul64(x3, arg2[1])
424	var x233 uint64
425	var x234 uint64
426	x234, x233 = bits.Mul64(x3, arg2[0])
427	var x235 uint64
428	var x236 uint64
429	x235, x236 = bits.Add64(x234, x231, uint64(0x0))
430	var x237 uint64
431	var x238 uint64
432	x237, x238 = bits.Add64(x232, x229, uint64(p384Uint1(x236)))
433	var x239 uint64
434	var x240 uint64
435	x239, x240 = bits.Add64(x230, x227, uint64(p384Uint1(x238)))
436	var x241 uint64
437	var x242 uint64
438	x241, x242 = bits.Add64(x228, x225, uint64(p384Uint1(x240)))
439	var x243 uint64
440	var x244 uint64
441	x243, x244 = bits.Add64(x226, x223, uint64(p384Uint1(x242)))
442	x245 := (uint64(p384Uint1(x244)) + x224)
443	var x246 uint64
444	var x247 uint64
445	x246, x247 = bits.Add64(x210, x233, uint64(0x0))
446	var x248 uint64
447	var x249 uint64
448	x248, x249 = bits.Add64(x212, x235, uint64(p384Uint1(x247)))
449	var x250 uint64
450	var x251 uint64
451	x250, x251 = bits.Add64(x214, x237, uint64(p384Uint1(x249)))
452	var x252 uint64
453	var x253 uint64
454	x252, x253 = bits.Add64(x216, x239, uint64(p384Uint1(x251)))
455	var x254 uint64
456	var x255 uint64
457	x254, x255 = bits.Add64(x218, x241, uint64(p384Uint1(x253)))
458	var x256 uint64
459	var x257 uint64
460	x256, x257 = bits.Add64(x220, x243, uint64(p384Uint1(x255)))
461	var x258 uint64
462	var x259 uint64
463	x258, x259 = bits.Add64(x222, x245, uint64(p384Uint1(x257)))
464	var x260 uint64
465	_, x260 = bits.Mul64(x246, 0x100000001)
466	var x262 uint64
467	var x263 uint64
468	x263, x262 = bits.Mul64(x260, 0xffffffffffffffff)
469	var x264 uint64
470	var x265 uint64
471	x265, x264 = bits.Mul64(x260, 0xffffffffffffffff)
472	var x266 uint64
473	var x267 uint64
474	x267, x266 = bits.Mul64(x260, 0xffffffffffffffff)
475	var x268 uint64
476	var x269 uint64
477	x269, x268 = bits.Mul64(x260, 0xfffffffffffffffe)
478	var x270 uint64
479	var x271 uint64
480	x271, x270 = bits.Mul64(x260, 0xffffffff00000000)
481	var x272 uint64
482	var x273 uint64
483	x273, x272 = bits.Mul64(x260, 0xffffffff)
484	var x274 uint64
485	var x275 uint64
486	x274, x275 = bits.Add64(x273, x270, uint64(0x0))
487	var x276 uint64
488	var x277 uint64
489	x276, x277 = bits.Add64(x271, x268, uint64(p384Uint1(x275)))
490	var x278 uint64
491	var x279 uint64
492	x278, x279 = bits.Add64(x269, x266, uint64(p384Uint1(x277)))
493	var x280 uint64
494	var x281 uint64
495	x280, x281 = bits.Add64(x267, x264, uint64(p384Uint1(x279)))
496	var x282 uint64
497	var x283 uint64
498	x282, x283 = bits.Add64(x265, x262, uint64(p384Uint1(x281)))
499	x284 := (uint64(p384Uint1(x283)) + x263)
500	var x286 uint64
501	_, x286 = bits.Add64(x246, x272, uint64(0x0))
502	var x287 uint64
503	var x288 uint64
504	x287, x288 = bits.Add64(x248, x274, uint64(p384Uint1(x286)))
505	var x289 uint64
506	var x290 uint64
507	x289, x290 = bits.Add64(x250, x276, uint64(p384Uint1(x288)))
508	var x291 uint64
509	var x292 uint64
510	x291, x292 = bits.Add64(x252, x278, uint64(p384Uint1(x290)))
511	var x293 uint64
512	var x294 uint64
513	x293, x294 = bits.Add64(x254, x280, uint64(p384Uint1(x292)))
514	var x295 uint64
515	var x296 uint64
516	x295, x296 = bits.Add64(x256, x282, uint64(p384Uint1(x294)))
517	var x297 uint64
518	var x298 uint64
519	x297, x298 = bits.Add64(x258, x284, uint64(p384Uint1(x296)))
520	x299 := (uint64(p384Uint1(x298)) + uint64(p384Uint1(x259)))
521	var x300 uint64
522	var x301 uint64
523	x301, x300 = bits.Mul64(x4, arg2[5])
524	var x302 uint64
525	var x303 uint64
526	x303, x302 = bits.Mul64(x4, arg2[4])
527	var x304 uint64
528	var x305 uint64
529	x305, x304 = bits.Mul64(x4, arg2[3])
530	var x306 uint64
531	var x307 uint64
532	x307, x306 = bits.Mul64(x4, arg2[2])
533	var x308 uint64
534	var x309 uint64
535	x309, x308 = bits.Mul64(x4, arg2[1])
536	var x310 uint64
537	var x311 uint64
538	x311, x310 = bits.Mul64(x4, arg2[0])
539	var x312 uint64
540	var x313 uint64
541	x312, x313 = bits.Add64(x311, x308, uint64(0x0))
542	var x314 uint64
543	var x315 uint64
544	x314, x315 = bits.Add64(x309, x306, uint64(p384Uint1(x313)))
545	var x316 uint64
546	var x317 uint64
547	x316, x317 = bits.Add64(x307, x304, uint64(p384Uint1(x315)))
548	var x318 uint64
549	var x319 uint64
550	x318, x319 = bits.Add64(x305, x302, uint64(p384Uint1(x317)))
551	var x320 uint64
552	var x321 uint64
553	x320, x321 = bits.Add64(x303, x300, uint64(p384Uint1(x319)))
554	x322 := (uint64(p384Uint1(x321)) + x301)
555	var x323 uint64
556	var x324 uint64
557	x323, x324 = bits.Add64(x287, x310, uint64(0x0))
558	var x325 uint64
559	var x326 uint64
560	x325, x326 = bits.Add64(x289, x312, uint64(p384Uint1(x324)))
561	var x327 uint64
562	var x328 uint64
563	x327, x328 = bits.Add64(x291, x314, uint64(p384Uint1(x326)))
564	var x329 uint64
565	var x330 uint64
566	x329, x330 = bits.Add64(x293, x316, uint64(p384Uint1(x328)))
567	var x331 uint64
568	var x332 uint64
569	x331, x332 = bits.Add64(x295, x318, uint64(p384Uint1(x330)))
570	var x333 uint64
571	var x334 uint64
572	x333, x334 = bits.Add64(x297, x320, uint64(p384Uint1(x332)))
573	var x335 uint64
574	var x336 uint64
575	x335, x336 = bits.Add64(x299, x322, uint64(p384Uint1(x334)))
576	var x337 uint64
577	_, x337 = bits.Mul64(x323, 0x100000001)
578	var x339 uint64
579	var x340 uint64
580	x340, x339 = bits.Mul64(x337, 0xffffffffffffffff)
581	var x341 uint64
582	var x342 uint64
583	x342, x341 = bits.Mul64(x337, 0xffffffffffffffff)
584	var x343 uint64
585	var x344 uint64
586	x344, x343 = bits.Mul64(x337, 0xffffffffffffffff)
587	var x345 uint64
588	var x346 uint64
589	x346, x345 = bits.Mul64(x337, 0xfffffffffffffffe)
590	var x347 uint64
591	var x348 uint64
592	x348, x347 = bits.Mul64(x337, 0xffffffff00000000)
593	var x349 uint64
594	var x350 uint64
595	x350, x349 = bits.Mul64(x337, 0xffffffff)
596	var x351 uint64
597	var x352 uint64
598	x351, x352 = bits.Add64(x350, x347, uint64(0x0))
599	var x353 uint64
600	var x354 uint64
601	x353, x354 = bits.Add64(x348, x345, uint64(p384Uint1(x352)))
602	var x355 uint64
603	var x356 uint64
604	x355, x356 = bits.Add64(x346, x343, uint64(p384Uint1(x354)))
605	var x357 uint64
606	var x358 uint64
607	x357, x358 = bits.Add64(x344, x341, uint64(p384Uint1(x356)))
608	var x359 uint64
609	var x360 uint64
610	x359, x360 = bits.Add64(x342, x339, uint64(p384Uint1(x358)))
611	x361 := (uint64(p384Uint1(x360)) + x340)
612	var x363 uint64
613	_, x363 = bits.Add64(x323, x349, uint64(0x0))
614	var x364 uint64
615	var x365 uint64
616	x364, x365 = bits.Add64(x325, x351, uint64(p384Uint1(x363)))
617	var x366 uint64
618	var x367 uint64
619	x366, x367 = bits.Add64(x327, x353, uint64(p384Uint1(x365)))
620	var x368 uint64
621	var x369 uint64
622	x368, x369 = bits.Add64(x329, x355, uint64(p384Uint1(x367)))
623	var x370 uint64
624	var x371 uint64
625	x370, x371 = bits.Add64(x331, x357, uint64(p384Uint1(x369)))
626	var x372 uint64
627	var x373 uint64
628	x372, x373 = bits.Add64(x333, x359, uint64(p384Uint1(x371)))
629	var x374 uint64
630	var x375 uint64
631	x374, x375 = bits.Add64(x335, x361, uint64(p384Uint1(x373)))
632	x376 := (uint64(p384Uint1(x375)) + uint64(p384Uint1(x336)))
633	var x377 uint64
634	var x378 uint64
635	x378, x377 = bits.Mul64(x5, arg2[5])
636	var x379 uint64
637	var x380 uint64
638	x380, x379 = bits.Mul64(x5, arg2[4])
639	var x381 uint64
640	var x382 uint64
641	x382, x381 = bits.Mul64(x5, arg2[3])
642	var x383 uint64
643	var x384 uint64
644	x384, x383 = bits.Mul64(x5, arg2[2])
645	var x385 uint64
646	var x386 uint64
647	x386, x385 = bits.Mul64(x5, arg2[1])
648	var x387 uint64
649	var x388 uint64
650	x388, x387 = bits.Mul64(x5, arg2[0])
651	var x389 uint64
652	var x390 uint64
653	x389, x390 = bits.Add64(x388, x385, uint64(0x0))
654	var x391 uint64
655	var x392 uint64
656	x391, x392 = bits.Add64(x386, x383, uint64(p384Uint1(x390)))
657	var x393 uint64
658	var x394 uint64
659	x393, x394 = bits.Add64(x384, x381, uint64(p384Uint1(x392)))
660	var x395 uint64
661	var x396 uint64
662	x395, x396 = bits.Add64(x382, x379, uint64(p384Uint1(x394)))
663	var x397 uint64
664	var x398 uint64
665	x397, x398 = bits.Add64(x380, x377, uint64(p384Uint1(x396)))
666	x399 := (uint64(p384Uint1(x398)) + x378)
667	var x400 uint64
668	var x401 uint64
669	x400, x401 = bits.Add64(x364, x387, uint64(0x0))
670	var x402 uint64
671	var x403 uint64
672	x402, x403 = bits.Add64(x366, x389, uint64(p384Uint1(x401)))
673	var x404 uint64
674	var x405 uint64
675	x404, x405 = bits.Add64(x368, x391, uint64(p384Uint1(x403)))
676	var x406 uint64
677	var x407 uint64
678	x406, x407 = bits.Add64(x370, x393, uint64(p384Uint1(x405)))
679	var x408 uint64
680	var x409 uint64
681	x408, x409 = bits.Add64(x372, x395, uint64(p384Uint1(x407)))
682	var x410 uint64
683	var x411 uint64
684	x410, x411 = bits.Add64(x374, x397, uint64(p384Uint1(x409)))
685	var x412 uint64
686	var x413 uint64
687	x412, x413 = bits.Add64(x376, x399, uint64(p384Uint1(x411)))
688	var x414 uint64
689	_, x414 = bits.Mul64(x400, 0x100000001)
690	var x416 uint64
691	var x417 uint64
692	x417, x416 = bits.Mul64(x414, 0xffffffffffffffff)
693	var x418 uint64
694	var x419 uint64
695	x419, x418 = bits.Mul64(x414, 0xffffffffffffffff)
696	var x420 uint64
697	var x421 uint64
698	x421, x420 = bits.Mul64(x414, 0xffffffffffffffff)
699	var x422 uint64
700	var x423 uint64
701	x423, x422 = bits.Mul64(x414, 0xfffffffffffffffe)
702	var x424 uint64
703	var x425 uint64
704	x425, x424 = bits.Mul64(x414, 0xffffffff00000000)
705	var x426 uint64
706	var x427 uint64
707	x427, x426 = bits.Mul64(x414, 0xffffffff)
708	var x428 uint64
709	var x429 uint64
710	x428, x429 = bits.Add64(x427, x424, uint64(0x0))
711	var x430 uint64
712	var x431 uint64
713	x430, x431 = bits.Add64(x425, x422, uint64(p384Uint1(x429)))
714	var x432 uint64
715	var x433 uint64
716	x432, x433 = bits.Add64(x423, x420, uint64(p384Uint1(x431)))
717	var x434 uint64
718	var x435 uint64
719	x434, x435 = bits.Add64(x421, x418, uint64(p384Uint1(x433)))
720	var x436 uint64
721	var x437 uint64
722	x436, x437 = bits.Add64(x419, x416, uint64(p384Uint1(x435)))
723	x438 := (uint64(p384Uint1(x437)) + x417)
724	var x440 uint64
725	_, x440 = bits.Add64(x400, x426, uint64(0x0))
726	var x441 uint64
727	var x442 uint64
728	x441, x442 = bits.Add64(x402, x428, uint64(p384Uint1(x440)))
729	var x443 uint64
730	var x444 uint64
731	x443, x444 = bits.Add64(x404, x430, uint64(p384Uint1(x442)))
732	var x445 uint64
733	var x446 uint64
734	x445, x446 = bits.Add64(x406, x432, uint64(p384Uint1(x444)))
735	var x447 uint64
736	var x448 uint64
737	x447, x448 = bits.Add64(x408, x434, uint64(p384Uint1(x446)))
738	var x449 uint64
739	var x450 uint64
740	x449, x450 = bits.Add64(x410, x436, uint64(p384Uint1(x448)))
741	var x451 uint64
742	var x452 uint64
743	x451, x452 = bits.Add64(x412, x438, uint64(p384Uint1(x450)))
744	x453 := (uint64(p384Uint1(x452)) + uint64(p384Uint1(x413)))
745	var x454 uint64
746	var x455 uint64
747	x454, x455 = bits.Sub64(x441, 0xffffffff, uint64(0x0))
748	var x456 uint64
749	var x457 uint64
750	x456, x457 = bits.Sub64(x443, 0xffffffff00000000, uint64(p384Uint1(x455)))
751	var x458 uint64
752	var x459 uint64
753	x458, x459 = bits.Sub64(x445, 0xfffffffffffffffe, uint64(p384Uint1(x457)))
754	var x460 uint64
755	var x461 uint64
756	x460, x461 = bits.Sub64(x447, 0xffffffffffffffff, uint64(p384Uint1(x459)))
757	var x462 uint64
758	var x463 uint64
759	x462, x463 = bits.Sub64(x449, 0xffffffffffffffff, uint64(p384Uint1(x461)))
760	var x464 uint64
761	var x465 uint64
762	x464, x465 = bits.Sub64(x451, 0xffffffffffffffff, uint64(p384Uint1(x463)))
763	var x467 uint64
764	_, x467 = bits.Sub64(x453, uint64(0x0), uint64(p384Uint1(x465)))
765	var x468 uint64
766	p384CmovznzU64(&x468, p384Uint1(x467), x454, x441)
767	var x469 uint64
768	p384CmovznzU64(&x469, p384Uint1(x467), x456, x443)
769	var x470 uint64
770	p384CmovznzU64(&x470, p384Uint1(x467), x458, x445)
771	var x471 uint64
772	p384CmovznzU64(&x471, p384Uint1(x467), x460, x447)
773	var x472 uint64
774	p384CmovznzU64(&x472, p384Uint1(x467), x462, x449)
775	var x473 uint64
776	p384CmovznzU64(&x473, p384Uint1(x467), x464, x451)
777	out1[0] = x468
778	out1[1] = x469
779	out1[2] = x470
780	out1[3] = x471
781	out1[4] = x472
782	out1[5] = x473
783}
784
785// p384Square squares a field element in the Montgomery domain.
786//
787// Preconditions:
788//
789//	0 ≤ eval arg1 < m
790//
791// Postconditions:
792//
793//	eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
794//	0 ≤ eval out1 < m
795func p384Square(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement) {
796	x1 := arg1[1]
797	x2 := arg1[2]
798	x3 := arg1[3]
799	x4 := arg1[4]
800	x5 := arg1[5]
801	x6 := arg1[0]
802	var x7 uint64
803	var x8 uint64
804	x8, x7 = bits.Mul64(x6, arg1[5])
805	var x9 uint64
806	var x10 uint64
807	x10, x9 = bits.Mul64(x6, arg1[4])
808	var x11 uint64
809	var x12 uint64
810	x12, x11 = bits.Mul64(x6, arg1[3])
811	var x13 uint64
812	var x14 uint64
813	x14, x13 = bits.Mul64(x6, arg1[2])
814	var x15 uint64
815	var x16 uint64
816	x16, x15 = bits.Mul64(x6, arg1[1])
817	var x17 uint64
818	var x18 uint64
819	x18, x17 = bits.Mul64(x6, arg1[0])
820	var x19 uint64
821	var x20 uint64
822	x19, x20 = bits.Add64(x18, x15, uint64(0x0))
823	var x21 uint64
824	var x22 uint64
825	x21, x22 = bits.Add64(x16, x13, uint64(p384Uint1(x20)))
826	var x23 uint64
827	var x24 uint64
828	x23, x24 = bits.Add64(x14, x11, uint64(p384Uint1(x22)))
829	var x25 uint64
830	var x26 uint64
831	x25, x26 = bits.Add64(x12, x9, uint64(p384Uint1(x24)))
832	var x27 uint64
833	var x28 uint64
834	x27, x28 = bits.Add64(x10, x7, uint64(p384Uint1(x26)))
835	x29 := (uint64(p384Uint1(x28)) + x8)
836	var x30 uint64
837	_, x30 = bits.Mul64(x17, 0x100000001)
838	var x32 uint64
839	var x33 uint64
840	x33, x32 = bits.Mul64(x30, 0xffffffffffffffff)
841	var x34 uint64
842	var x35 uint64
843	x35, x34 = bits.Mul64(x30, 0xffffffffffffffff)
844	var x36 uint64
845	var x37 uint64
846	x37, x36 = bits.Mul64(x30, 0xffffffffffffffff)
847	var x38 uint64
848	var x39 uint64
849	x39, x38 = bits.Mul64(x30, 0xfffffffffffffffe)
850	var x40 uint64
851	var x41 uint64
852	x41, x40 = bits.Mul64(x30, 0xffffffff00000000)
853	var x42 uint64
854	var x43 uint64
855	x43, x42 = bits.Mul64(x30, 0xffffffff)
856	var x44 uint64
857	var x45 uint64
858	x44, x45 = bits.Add64(x43, x40, uint64(0x0))
859	var x46 uint64
860	var x47 uint64
861	x46, x47 = bits.Add64(x41, x38, uint64(p384Uint1(x45)))
862	var x48 uint64
863	var x49 uint64
864	x48, x49 = bits.Add64(x39, x36, uint64(p384Uint1(x47)))
865	var x50 uint64
866	var x51 uint64
867	x50, x51 = bits.Add64(x37, x34, uint64(p384Uint1(x49)))
868	var x52 uint64
869	var x53 uint64
870	x52, x53 = bits.Add64(x35, x32, uint64(p384Uint1(x51)))
871	x54 := (uint64(p384Uint1(x53)) + x33)
872	var x56 uint64
873	_, x56 = bits.Add64(x17, x42, uint64(0x0))
874	var x57 uint64
875	var x58 uint64
876	x57, x58 = bits.Add64(x19, x44, uint64(p384Uint1(x56)))
877	var x59 uint64
878	var x60 uint64
879	x59, x60 = bits.Add64(x21, x46, uint64(p384Uint1(x58)))
880	var x61 uint64
881	var x62 uint64
882	x61, x62 = bits.Add64(x23, x48, uint64(p384Uint1(x60)))
883	var x63 uint64
884	var x64 uint64
885	x63, x64 = bits.Add64(x25, x50, uint64(p384Uint1(x62)))
886	var x65 uint64
887	var x66 uint64
888	x65, x66 = bits.Add64(x27, x52, uint64(p384Uint1(x64)))
889	var x67 uint64
890	var x68 uint64
891	x67, x68 = bits.Add64(x29, x54, uint64(p384Uint1(x66)))
892	var x69 uint64
893	var x70 uint64
894	x70, x69 = bits.Mul64(x1, arg1[5])
895	var x71 uint64
896	var x72 uint64
897	x72, x71 = bits.Mul64(x1, arg1[4])
898	var x73 uint64
899	var x74 uint64
900	x74, x73 = bits.Mul64(x1, arg1[3])
901	var x75 uint64
902	var x76 uint64
903	x76, x75 = bits.Mul64(x1, arg1[2])
904	var x77 uint64
905	var x78 uint64
906	x78, x77 = bits.Mul64(x1, arg1[1])
907	var x79 uint64
908	var x80 uint64
909	x80, x79 = bits.Mul64(x1, arg1[0])
910	var x81 uint64
911	var x82 uint64
912	x81, x82 = bits.Add64(x80, x77, uint64(0x0))
913	var x83 uint64
914	var x84 uint64
915	x83, x84 = bits.Add64(x78, x75, uint64(p384Uint1(x82)))
916	var x85 uint64
917	var x86 uint64
918	x85, x86 = bits.Add64(x76, x73, uint64(p384Uint1(x84)))
919	var x87 uint64
920	var x88 uint64
921	x87, x88 = bits.Add64(x74, x71, uint64(p384Uint1(x86)))
922	var x89 uint64
923	var x90 uint64
924	x89, x90 = bits.Add64(x72, x69, uint64(p384Uint1(x88)))
925	x91 := (uint64(p384Uint1(x90)) + x70)
926	var x92 uint64
927	var x93 uint64
928	x92, x93 = bits.Add64(x57, x79, uint64(0x0))
929	var x94 uint64
930	var x95 uint64
931	x94, x95 = bits.Add64(x59, x81, uint64(p384Uint1(x93)))
932	var x96 uint64
933	var x97 uint64
934	x96, x97 = bits.Add64(x61, x83, uint64(p384Uint1(x95)))
935	var x98 uint64
936	var x99 uint64
937	x98, x99 = bits.Add64(x63, x85, uint64(p384Uint1(x97)))
938	var x100 uint64
939	var x101 uint64
940	x100, x101 = bits.Add64(x65, x87, uint64(p384Uint1(x99)))
941	var x102 uint64
942	var x103 uint64
943	x102, x103 = bits.Add64(x67, x89, uint64(p384Uint1(x101)))
944	var x104 uint64
945	var x105 uint64
946	x104, x105 = bits.Add64(uint64(p384Uint1(x68)), x91, uint64(p384Uint1(x103)))
947	var x106 uint64
948	_, x106 = bits.Mul64(x92, 0x100000001)
949	var x108 uint64
950	var x109 uint64
951	x109, x108 = bits.Mul64(x106, 0xffffffffffffffff)
952	var x110 uint64
953	var x111 uint64
954	x111, x110 = bits.Mul64(x106, 0xffffffffffffffff)
955	var x112 uint64
956	var x113 uint64
957	x113, x112 = bits.Mul64(x106, 0xffffffffffffffff)
958	var x114 uint64
959	var x115 uint64
960	x115, x114 = bits.Mul64(x106, 0xfffffffffffffffe)
961	var x116 uint64
962	var x117 uint64
963	x117, x116 = bits.Mul64(x106, 0xffffffff00000000)
964	var x118 uint64
965	var x119 uint64
966	x119, x118 = bits.Mul64(x106, 0xffffffff)
967	var x120 uint64
968	var x121 uint64
969	x120, x121 = bits.Add64(x119, x116, uint64(0x0))
970	var x122 uint64
971	var x123 uint64
972	x122, x123 = bits.Add64(x117, x114, uint64(p384Uint1(x121)))
973	var x124 uint64
974	var x125 uint64
975	x124, x125 = bits.Add64(x115, x112, uint64(p384Uint1(x123)))
976	var x126 uint64
977	var x127 uint64
978	x126, x127 = bits.Add64(x113, x110, uint64(p384Uint1(x125)))
979	var x128 uint64
980	var x129 uint64
981	x128, x129 = bits.Add64(x111, x108, uint64(p384Uint1(x127)))
982	x130 := (uint64(p384Uint1(x129)) + x109)
983	var x132 uint64
984	_, x132 = bits.Add64(x92, x118, uint64(0x0))
985	var x133 uint64
986	var x134 uint64
987	x133, x134 = bits.Add64(x94, x120, uint64(p384Uint1(x132)))
988	var x135 uint64
989	var x136 uint64
990	x135, x136 = bits.Add64(x96, x122, uint64(p384Uint1(x134)))
991	var x137 uint64
992	var x138 uint64
993	x137, x138 = bits.Add64(x98, x124, uint64(p384Uint1(x136)))
994	var x139 uint64
995	var x140 uint64
996	x139, x140 = bits.Add64(x100, x126, uint64(p384Uint1(x138)))
997	var x141 uint64
998	var x142 uint64
999	x141, x142 = bits.Add64(x102, x128, uint64(p384Uint1(x140)))
1000	var x143 uint64
1001	var x144 uint64
1002	x143, x144 = bits.Add64(x104, x130, uint64(p384Uint1(x142)))
1003	x145 := (uint64(p384Uint1(x144)) + uint64(p384Uint1(x105)))
1004	var x146 uint64
1005	var x147 uint64
1006	x147, x146 = bits.Mul64(x2, arg1[5])
1007	var x148 uint64
1008	var x149 uint64
1009	x149, x148 = bits.Mul64(x2, arg1[4])
1010	var x150 uint64
1011	var x151 uint64
1012	x151, x150 = bits.Mul64(x2, arg1[3])
1013	var x152 uint64
1014	var x153 uint64
1015	x153, x152 = bits.Mul64(x2, arg1[2])
1016	var x154 uint64
1017	var x155 uint64
1018	x155, x154 = bits.Mul64(x2, arg1[1])
1019	var x156 uint64
1020	var x157 uint64
1021	x157, x156 = bits.Mul64(x2, arg1[0])
1022	var x158 uint64
1023	var x159 uint64
1024	x158, x159 = bits.Add64(x157, x154, uint64(0x0))
1025	var x160 uint64
1026	var x161 uint64
1027	x160, x161 = bits.Add64(x155, x152, uint64(p384Uint1(x159)))
1028	var x162 uint64
1029	var x163 uint64
1030	x162, x163 = bits.Add64(x153, x150, uint64(p384Uint1(x161)))
1031	var x164 uint64
1032	var x165 uint64
1033	x164, x165 = bits.Add64(x151, x148, uint64(p384Uint1(x163)))
1034	var x166 uint64
1035	var x167 uint64
1036	x166, x167 = bits.Add64(x149, x146, uint64(p384Uint1(x165)))
1037	x168 := (uint64(p384Uint1(x167)) + x147)
1038	var x169 uint64
1039	var x170 uint64
1040	x169, x170 = bits.Add64(x133, x156, uint64(0x0))
1041	var x171 uint64
1042	var x172 uint64
1043	x171, x172 = bits.Add64(x135, x158, uint64(p384Uint1(x170)))
1044	var x173 uint64
1045	var x174 uint64
1046	x173, x174 = bits.Add64(x137, x160, uint64(p384Uint1(x172)))
1047	var x175 uint64
1048	var x176 uint64
1049	x175, x176 = bits.Add64(x139, x162, uint64(p384Uint1(x174)))
1050	var x177 uint64
1051	var x178 uint64
1052	x177, x178 = bits.Add64(x141, x164, uint64(p384Uint1(x176)))
1053	var x179 uint64
1054	var x180 uint64
1055	x179, x180 = bits.Add64(x143, x166, uint64(p384Uint1(x178)))
1056	var x181 uint64
1057	var x182 uint64
1058	x181, x182 = bits.Add64(x145, x168, uint64(p384Uint1(x180)))
1059	var x183 uint64
1060	_, x183 = bits.Mul64(x169, 0x100000001)
1061	var x185 uint64
1062	var x186 uint64
1063	x186, x185 = bits.Mul64(x183, 0xffffffffffffffff)
1064	var x187 uint64
1065	var x188 uint64
1066	x188, x187 = bits.Mul64(x183, 0xffffffffffffffff)
1067	var x189 uint64
1068	var x190 uint64
1069	x190, x189 = bits.Mul64(x183, 0xffffffffffffffff)
1070	var x191 uint64
1071	var x192 uint64
1072	x192, x191 = bits.Mul64(x183, 0xfffffffffffffffe)
1073	var x193 uint64
1074	var x194 uint64
1075	x194, x193 = bits.Mul64(x183, 0xffffffff00000000)
1076	var x195 uint64
1077	var x196 uint64
1078	x196, x195 = bits.Mul64(x183, 0xffffffff)
1079	var x197 uint64
1080	var x198 uint64
1081	x197, x198 = bits.Add64(x196, x193, uint64(0x0))
1082	var x199 uint64
1083	var x200 uint64
1084	x199, x200 = bits.Add64(x194, x191, uint64(p384Uint1(x198)))
1085	var x201 uint64
1086	var x202 uint64
1087	x201, x202 = bits.Add64(x192, x189, uint64(p384Uint1(x200)))
1088	var x203 uint64
1089	var x204 uint64
1090	x203, x204 = bits.Add64(x190, x187, uint64(p384Uint1(x202)))
1091	var x205 uint64
1092	var x206 uint64
1093	x205, x206 = bits.Add64(x188, x185, uint64(p384Uint1(x204)))
1094	x207 := (uint64(p384Uint1(x206)) + x186)
1095	var x209 uint64
1096	_, x209 = bits.Add64(x169, x195, uint64(0x0))
1097	var x210 uint64
1098	var x211 uint64
1099	x210, x211 = bits.Add64(x171, x197, uint64(p384Uint1(x209)))
1100	var x212 uint64
1101	var x213 uint64
1102	x212, x213 = bits.Add64(x173, x199, uint64(p384Uint1(x211)))
1103	var x214 uint64
1104	var x215 uint64
1105	x214, x215 = bits.Add64(x175, x201, uint64(p384Uint1(x213)))
1106	var x216 uint64
1107	var x217 uint64
1108	x216, x217 = bits.Add64(x177, x203, uint64(p384Uint1(x215)))
1109	var x218 uint64
1110	var x219 uint64
1111	x218, x219 = bits.Add64(x179, x205, uint64(p384Uint1(x217)))
1112	var x220 uint64
1113	var x221 uint64
1114	x220, x221 = bits.Add64(x181, x207, uint64(p384Uint1(x219)))
1115	x222 := (uint64(p384Uint1(x221)) + uint64(p384Uint1(x182)))
1116	var x223 uint64
1117	var x224 uint64
1118	x224, x223 = bits.Mul64(x3, arg1[5])
1119	var x225 uint64
1120	var x226 uint64
1121	x226, x225 = bits.Mul64(x3, arg1[4])
1122	var x227 uint64
1123	var x228 uint64
1124	x228, x227 = bits.Mul64(x3, arg1[3])
1125	var x229 uint64
1126	var x230 uint64
1127	x230, x229 = bits.Mul64(x3, arg1[2])
1128	var x231 uint64
1129	var x232 uint64
1130	x232, x231 = bits.Mul64(x3, arg1[1])
1131	var x233 uint64
1132	var x234 uint64
1133	x234, x233 = bits.Mul64(x3, arg1[0])
1134	var x235 uint64
1135	var x236 uint64
1136	x235, x236 = bits.Add64(x234, x231, uint64(0x0))
1137	var x237 uint64
1138	var x238 uint64
1139	x237, x238 = bits.Add64(x232, x229, uint64(p384Uint1(x236)))
1140	var x239 uint64
1141	var x240 uint64
1142	x239, x240 = bits.Add64(x230, x227, uint64(p384Uint1(x238)))
1143	var x241 uint64
1144	var x242 uint64
1145	x241, x242 = bits.Add64(x228, x225, uint64(p384Uint1(x240)))
1146	var x243 uint64
1147	var x244 uint64
1148	x243, x244 = bits.Add64(x226, x223, uint64(p384Uint1(x242)))
1149	x245 := (uint64(p384Uint1(x244)) + x224)
1150	var x246 uint64
1151	var x247 uint64
1152	x246, x247 = bits.Add64(x210, x233, uint64(0x0))
1153	var x248 uint64
1154	var x249 uint64
1155	x248, x249 = bits.Add64(x212, x235, uint64(p384Uint1(x247)))
1156	var x250 uint64
1157	var x251 uint64
1158	x250, x251 = bits.Add64(x214, x237, uint64(p384Uint1(x249)))
1159	var x252 uint64
1160	var x253 uint64
1161	x252, x253 = bits.Add64(x216, x239, uint64(p384Uint1(x251)))
1162	var x254 uint64
1163	var x255 uint64
1164	x254, x255 = bits.Add64(x218, x241, uint64(p384Uint1(x253)))
1165	var x256 uint64
1166	var x257 uint64
1167	x256, x257 = bits.Add64(x220, x243, uint64(p384Uint1(x255)))
1168	var x258 uint64
1169	var x259 uint64
1170	x258, x259 = bits.Add64(x222, x245, uint64(p384Uint1(x257)))
1171	var x260 uint64
1172	_, x260 = bits.Mul64(x246, 0x100000001)
1173	var x262 uint64
1174	var x263 uint64
1175	x263, x262 = bits.Mul64(x260, 0xffffffffffffffff)
1176	var x264 uint64
1177	var x265 uint64
1178	x265, x264 = bits.Mul64(x260, 0xffffffffffffffff)
1179	var x266 uint64
1180	var x267 uint64
1181	x267, x266 = bits.Mul64(x260, 0xffffffffffffffff)
1182	var x268 uint64
1183	var x269 uint64
1184	x269, x268 = bits.Mul64(x260, 0xfffffffffffffffe)
1185	var x270 uint64
1186	var x271 uint64
1187	x271, x270 = bits.Mul64(x260, 0xffffffff00000000)
1188	var x272 uint64
1189	var x273 uint64
1190	x273, x272 = bits.Mul64(x260, 0xffffffff)
1191	var x274 uint64
1192	var x275 uint64
1193	x274, x275 = bits.Add64(x273, x270, uint64(0x0))
1194	var x276 uint64
1195	var x277 uint64
1196	x276, x277 = bits.Add64(x271, x268, uint64(p384Uint1(x275)))
1197	var x278 uint64
1198	var x279 uint64
1199	x278, x279 = bits.Add64(x269, x266, uint64(p384Uint1(x277)))
1200	var x280 uint64
1201	var x281 uint64
1202	x280, x281 = bits.Add64(x267, x264, uint64(p384Uint1(x279)))
1203	var x282 uint64
1204	var x283 uint64
1205	x282, x283 = bits.Add64(x265, x262, uint64(p384Uint1(x281)))
1206	x284 := (uint64(p384Uint1(x283)) + x263)
1207	var x286 uint64
1208	_, x286 = bits.Add64(x246, x272, uint64(0x0))
1209	var x287 uint64
1210	var x288 uint64
1211	x287, x288 = bits.Add64(x248, x274, uint64(p384Uint1(x286)))
1212	var x289 uint64
1213	var x290 uint64
1214	x289, x290 = bits.Add64(x250, x276, uint64(p384Uint1(x288)))
1215	var x291 uint64
1216	var x292 uint64
1217	x291, x292 = bits.Add64(x252, x278, uint64(p384Uint1(x290)))
1218	var x293 uint64
1219	var x294 uint64
1220	x293, x294 = bits.Add64(x254, x280, uint64(p384Uint1(x292)))
1221	var x295 uint64
1222	var x296 uint64
1223	x295, x296 = bits.Add64(x256, x282, uint64(p384Uint1(x294)))
1224	var x297 uint64
1225	var x298 uint64
1226	x297, x298 = bits.Add64(x258, x284, uint64(p384Uint1(x296)))
1227	x299 := (uint64(p384Uint1(x298)) + uint64(p384Uint1(x259)))
1228	var x300 uint64
1229	var x301 uint64
1230	x301, x300 = bits.Mul64(x4, arg1[5])
1231	var x302 uint64
1232	var x303 uint64
1233	x303, x302 = bits.Mul64(x4, arg1[4])
1234	var x304 uint64
1235	var x305 uint64
1236	x305, x304 = bits.Mul64(x4, arg1[3])
1237	var x306 uint64
1238	var x307 uint64
1239	x307, x306 = bits.Mul64(x4, arg1[2])
1240	var x308 uint64
1241	var x309 uint64
1242	x309, x308 = bits.Mul64(x4, arg1[1])
1243	var x310 uint64
1244	var x311 uint64
1245	x311, x310 = bits.Mul64(x4, arg1[0])
1246	var x312 uint64
1247	var x313 uint64
1248	x312, x313 = bits.Add64(x311, x308, uint64(0x0))
1249	var x314 uint64
1250	var x315 uint64
1251	x314, x315 = bits.Add64(x309, x306, uint64(p384Uint1(x313)))
1252	var x316 uint64
1253	var x317 uint64
1254	x316, x317 = bits.Add64(x307, x304, uint64(p384Uint1(x315)))
1255	var x318 uint64
1256	var x319 uint64
1257	x318, x319 = bits.Add64(x305, x302, uint64(p384Uint1(x317)))
1258	var x320 uint64
1259	var x321 uint64
1260	x320, x321 = bits.Add64(x303, x300, uint64(p384Uint1(x319)))
1261	x322 := (uint64(p384Uint1(x321)) + x301)
1262	var x323 uint64
1263	var x324 uint64
1264	x323, x324 = bits.Add64(x287, x310, uint64(0x0))
1265	var x325 uint64
1266	var x326 uint64
1267	x325, x326 = bits.Add64(x289, x312, uint64(p384Uint1(x324)))
1268	var x327 uint64
1269	var x328 uint64
1270	x327, x328 = bits.Add64(x291, x314, uint64(p384Uint1(x326)))
1271	var x329 uint64
1272	var x330 uint64
1273	x329, x330 = bits.Add64(x293, x316, uint64(p384Uint1(x328)))
1274	var x331 uint64
1275	var x332 uint64
1276	x331, x332 = bits.Add64(x295, x318, uint64(p384Uint1(x330)))
1277	var x333 uint64
1278	var x334 uint64
1279	x333, x334 = bits.Add64(x297, x320, uint64(p384Uint1(x332)))
1280	var x335 uint64
1281	var x336 uint64
1282	x335, x336 = bits.Add64(x299, x322, uint64(p384Uint1(x334)))
1283	var x337 uint64
1284	_, x337 = bits.Mul64(x323, 0x100000001)
1285	var x339 uint64
1286	var x340 uint64
1287	x340, x339 = bits.Mul64(x337, 0xffffffffffffffff)
1288	var x341 uint64
1289	var x342 uint64
1290	x342, x341 = bits.Mul64(x337, 0xffffffffffffffff)
1291	var x343 uint64
1292	var x344 uint64
1293	x344, x343 = bits.Mul64(x337, 0xffffffffffffffff)
1294	var x345 uint64
1295	var x346 uint64
1296	x346, x345 = bits.Mul64(x337, 0xfffffffffffffffe)
1297	var x347 uint64
1298	var x348 uint64
1299	x348, x347 = bits.Mul64(x337, 0xffffffff00000000)
1300	var x349 uint64
1301	var x350 uint64
1302	x350, x349 = bits.Mul64(x337, 0xffffffff)
1303	var x351 uint64
1304	var x352 uint64
1305	x351, x352 = bits.Add64(x350, x347, uint64(0x0))
1306	var x353 uint64
1307	var x354 uint64
1308	x353, x354 = bits.Add64(x348, x345, uint64(p384Uint1(x352)))
1309	var x355 uint64
1310	var x356 uint64
1311	x355, x356 = bits.Add64(x346, x343, uint64(p384Uint1(x354)))
1312	var x357 uint64
1313	var x358 uint64
1314	x357, x358 = bits.Add64(x344, x341, uint64(p384Uint1(x356)))
1315	var x359 uint64
1316	var x360 uint64
1317	x359, x360 = bits.Add64(x342, x339, uint64(p384Uint1(x358)))
1318	x361 := (uint64(p384Uint1(x360)) + x340)
1319	var x363 uint64
1320	_, x363 = bits.Add64(x323, x349, uint64(0x0))
1321	var x364 uint64
1322	var x365 uint64
1323	x364, x365 = bits.Add64(x325, x351, uint64(p384Uint1(x363)))
1324	var x366 uint64
1325	var x367 uint64
1326	x366, x367 = bits.Add64(x327, x353, uint64(p384Uint1(x365)))
1327	var x368 uint64
1328	var x369 uint64
1329	x368, x369 = bits.Add64(x329, x355, uint64(p384Uint1(x367)))
1330	var x370 uint64
1331	var x371 uint64
1332	x370, x371 = bits.Add64(x331, x357, uint64(p384Uint1(x369)))
1333	var x372 uint64
1334	var x373 uint64
1335	x372, x373 = bits.Add64(x333, x359, uint64(p384Uint1(x371)))
1336	var x374 uint64
1337	var x375 uint64
1338	x374, x375 = bits.Add64(x335, x361, uint64(p384Uint1(x373)))
1339	x376 := (uint64(p384Uint1(x375)) + uint64(p384Uint1(x336)))
1340	var x377 uint64
1341	var x378 uint64
1342	x378, x377 = bits.Mul64(x5, arg1[5])
1343	var x379 uint64
1344	var x380 uint64
1345	x380, x379 = bits.Mul64(x5, arg1[4])
1346	var x381 uint64
1347	var x382 uint64
1348	x382, x381 = bits.Mul64(x5, arg1[3])
1349	var x383 uint64
1350	var x384 uint64
1351	x384, x383 = bits.Mul64(x5, arg1[2])
1352	var x385 uint64
1353	var x386 uint64
1354	x386, x385 = bits.Mul64(x5, arg1[1])
1355	var x387 uint64
1356	var x388 uint64
1357	x388, x387 = bits.Mul64(x5, arg1[0])
1358	var x389 uint64
1359	var x390 uint64
1360	x389, x390 = bits.Add64(x388, x385, uint64(0x0))
1361	var x391 uint64
1362	var x392 uint64
1363	x391, x392 = bits.Add64(x386, x383, uint64(p384Uint1(x390)))
1364	var x393 uint64
1365	var x394 uint64
1366	x393, x394 = bits.Add64(x384, x381, uint64(p384Uint1(x392)))
1367	var x395 uint64
1368	var x396 uint64
1369	x395, x396 = bits.Add64(x382, x379, uint64(p384Uint1(x394)))
1370	var x397 uint64
1371	var x398 uint64
1372	x397, x398 = bits.Add64(x380, x377, uint64(p384Uint1(x396)))
1373	x399 := (uint64(p384Uint1(x398)) + x378)
1374	var x400 uint64
1375	var x401 uint64
1376	x400, x401 = bits.Add64(x364, x387, uint64(0x0))
1377	var x402 uint64
1378	var x403 uint64
1379	x402, x403 = bits.Add64(x366, x389, uint64(p384Uint1(x401)))
1380	var x404 uint64
1381	var x405 uint64
1382	x404, x405 = bits.Add64(x368, x391, uint64(p384Uint1(x403)))
1383	var x406 uint64
1384	var x407 uint64
1385	x406, x407 = bits.Add64(x370, x393, uint64(p384Uint1(x405)))
1386	var x408 uint64
1387	var x409 uint64
1388	x408, x409 = bits.Add64(x372, x395, uint64(p384Uint1(x407)))
1389	var x410 uint64
1390	var x411 uint64
1391	x410, x411 = bits.Add64(x374, x397, uint64(p384Uint1(x409)))
1392	var x412 uint64
1393	var x413 uint64
1394	x412, x413 = bits.Add64(x376, x399, uint64(p384Uint1(x411)))
1395	var x414 uint64
1396	_, x414 = bits.Mul64(x400, 0x100000001)
1397	var x416 uint64
1398	var x417 uint64
1399	x417, x416 = bits.Mul64(x414, 0xffffffffffffffff)
1400	var x418 uint64
1401	var x419 uint64
1402	x419, x418 = bits.Mul64(x414, 0xffffffffffffffff)
1403	var x420 uint64
1404	var x421 uint64
1405	x421, x420 = bits.Mul64(x414, 0xffffffffffffffff)
1406	var x422 uint64
1407	var x423 uint64
1408	x423, x422 = bits.Mul64(x414, 0xfffffffffffffffe)
1409	var x424 uint64
1410	var x425 uint64
1411	x425, x424 = bits.Mul64(x414, 0xffffffff00000000)
1412	var x426 uint64
1413	var x427 uint64
1414	x427, x426 = bits.Mul64(x414, 0xffffffff)
1415	var x428 uint64
1416	var x429 uint64
1417	x428, x429 = bits.Add64(x427, x424, uint64(0x0))
1418	var x430 uint64
1419	var x431 uint64
1420	x430, x431 = bits.Add64(x425, x422, uint64(p384Uint1(x429)))
1421	var x432 uint64
1422	var x433 uint64
1423	x432, x433 = bits.Add64(x423, x420, uint64(p384Uint1(x431)))
1424	var x434 uint64
1425	var x435 uint64
1426	x434, x435 = bits.Add64(x421, x418, uint64(p384Uint1(x433)))
1427	var x436 uint64
1428	var x437 uint64
1429	x436, x437 = bits.Add64(x419, x416, uint64(p384Uint1(x435)))
1430	x438 := (uint64(p384Uint1(x437)) + x417)
1431	var x440 uint64
1432	_, x440 = bits.Add64(x400, x426, uint64(0x0))
1433	var x441 uint64
1434	var x442 uint64
1435	x441, x442 = bits.Add64(x402, x428, uint64(p384Uint1(x440)))
1436	var x443 uint64
1437	var x444 uint64
1438	x443, x444 = bits.Add64(x404, x430, uint64(p384Uint1(x442)))
1439	var x445 uint64
1440	var x446 uint64
1441	x445, x446 = bits.Add64(x406, x432, uint64(p384Uint1(x444)))
1442	var x447 uint64
1443	var x448 uint64
1444	x447, x448 = bits.Add64(x408, x434, uint64(p384Uint1(x446)))
1445	var x449 uint64
1446	var x450 uint64
1447	x449, x450 = bits.Add64(x410, x436, uint64(p384Uint1(x448)))
1448	var x451 uint64
1449	var x452 uint64
1450	x451, x452 = bits.Add64(x412, x438, uint64(p384Uint1(x450)))
1451	x453 := (uint64(p384Uint1(x452)) + uint64(p384Uint1(x413)))
1452	var x454 uint64
1453	var x455 uint64
1454	x454, x455 = bits.Sub64(x441, 0xffffffff, uint64(0x0))
1455	var x456 uint64
1456	var x457 uint64
1457	x456, x457 = bits.Sub64(x443, 0xffffffff00000000, uint64(p384Uint1(x455)))
1458	var x458 uint64
1459	var x459 uint64
1460	x458, x459 = bits.Sub64(x445, 0xfffffffffffffffe, uint64(p384Uint1(x457)))
1461	var x460 uint64
1462	var x461 uint64
1463	x460, x461 = bits.Sub64(x447, 0xffffffffffffffff, uint64(p384Uint1(x459)))
1464	var x462 uint64
1465	var x463 uint64
1466	x462, x463 = bits.Sub64(x449, 0xffffffffffffffff, uint64(p384Uint1(x461)))
1467	var x464 uint64
1468	var x465 uint64
1469	x464, x465 = bits.Sub64(x451, 0xffffffffffffffff, uint64(p384Uint1(x463)))
1470	var x467 uint64
1471	_, x467 = bits.Sub64(x453, uint64(0x0), uint64(p384Uint1(x465)))
1472	var x468 uint64
1473	p384CmovznzU64(&x468, p384Uint1(x467), x454, x441)
1474	var x469 uint64
1475	p384CmovznzU64(&x469, p384Uint1(x467), x456, x443)
1476	var x470 uint64
1477	p384CmovznzU64(&x470, p384Uint1(x467), x458, x445)
1478	var x471 uint64
1479	p384CmovznzU64(&x471, p384Uint1(x467), x460, x447)
1480	var x472 uint64
1481	p384CmovznzU64(&x472, p384Uint1(x467), x462, x449)
1482	var x473 uint64
1483	p384CmovznzU64(&x473, p384Uint1(x467), x464, x451)
1484	out1[0] = x468
1485	out1[1] = x469
1486	out1[2] = x470
1487	out1[3] = x471
1488	out1[4] = x472
1489	out1[5] = x473
1490}
1491
1492// p384Add adds two field elements in the Montgomery domain.
1493//
1494// Preconditions:
1495//
1496//	0 ≤ eval arg1 < m
1497//	0 ≤ eval arg2 < m
1498//
1499// Postconditions:
1500//
1501//	eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
1502//	0 ≤ eval out1 < m
1503func p384Add(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement) {
1504	var x1 uint64
1505	var x2 uint64
1506	x1, x2 = bits.Add64(arg1[0], arg2[0], uint64(0x0))
1507	var x3 uint64
1508	var x4 uint64
1509	x3, x4 = bits.Add64(arg1[1], arg2[1], uint64(p384Uint1(x2)))
1510	var x5 uint64
1511	var x6 uint64
1512	x5, x6 = bits.Add64(arg1[2], arg2[2], uint64(p384Uint1(x4)))
1513	var x7 uint64
1514	var x8 uint64
1515	x7, x8 = bits.Add64(arg1[3], arg2[3], uint64(p384Uint1(x6)))
1516	var x9 uint64
1517	var x10 uint64
1518	x9, x10 = bits.Add64(arg1[4], arg2[4], uint64(p384Uint1(x8)))
1519	var x11 uint64
1520	var x12 uint64
1521	x11, x12 = bits.Add64(arg1[5], arg2[5], uint64(p384Uint1(x10)))
1522	var x13 uint64
1523	var x14 uint64
1524	x13, x14 = bits.Sub64(x1, 0xffffffff, uint64(0x0))
1525	var x15 uint64
1526	var x16 uint64
1527	x15, x16 = bits.Sub64(x3, 0xffffffff00000000, uint64(p384Uint1(x14)))
1528	var x17 uint64
1529	var x18 uint64
1530	x17, x18 = bits.Sub64(x5, 0xfffffffffffffffe, uint64(p384Uint1(x16)))
1531	var x19 uint64
1532	var x20 uint64
1533	x19, x20 = bits.Sub64(x7, 0xffffffffffffffff, uint64(p384Uint1(x18)))
1534	var x21 uint64
1535	var x22 uint64
1536	x21, x22 = bits.Sub64(x9, 0xffffffffffffffff, uint64(p384Uint1(x20)))
1537	var x23 uint64
1538	var x24 uint64
1539	x23, x24 = bits.Sub64(x11, 0xffffffffffffffff, uint64(p384Uint1(x22)))
1540	var x26 uint64
1541	_, x26 = bits.Sub64(uint64(p384Uint1(x12)), uint64(0x0), uint64(p384Uint1(x24)))
1542	var x27 uint64
1543	p384CmovznzU64(&x27, p384Uint1(x26), x13, x1)
1544	var x28 uint64
1545	p384CmovznzU64(&x28, p384Uint1(x26), x15, x3)
1546	var x29 uint64
1547	p384CmovznzU64(&x29, p384Uint1(x26), x17, x5)
1548	var x30 uint64
1549	p384CmovznzU64(&x30, p384Uint1(x26), x19, x7)
1550	var x31 uint64
1551	p384CmovznzU64(&x31, p384Uint1(x26), x21, x9)
1552	var x32 uint64
1553	p384CmovznzU64(&x32, p384Uint1(x26), x23, x11)
1554	out1[0] = x27
1555	out1[1] = x28
1556	out1[2] = x29
1557	out1[3] = x30
1558	out1[4] = x31
1559	out1[5] = x32
1560}
1561
1562// p384Sub subtracts two field elements in the Montgomery domain.
1563//
1564// Preconditions:
1565//
1566//	0 ≤ eval arg1 < m
1567//	0 ≤ eval arg2 < m
1568//
1569// Postconditions:
1570//
1571//	eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
1572//	0 ≤ eval out1 < m
1573func p384Sub(out1 *p384MontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement, arg2 *p384MontgomeryDomainFieldElement) {
1574	var x1 uint64
1575	var x2 uint64
1576	x1, x2 = bits.Sub64(arg1[0], arg2[0], uint64(0x0))
1577	var x3 uint64
1578	var x4 uint64
1579	x3, x4 = bits.Sub64(arg1[1], arg2[1], uint64(p384Uint1(x2)))
1580	var x5 uint64
1581	var x6 uint64
1582	x5, x6 = bits.Sub64(arg1[2], arg2[2], uint64(p384Uint1(x4)))
1583	var x7 uint64
1584	var x8 uint64
1585	x7, x8 = bits.Sub64(arg1[3], arg2[3], uint64(p384Uint1(x6)))
1586	var x9 uint64
1587	var x10 uint64
1588	x9, x10 = bits.Sub64(arg1[4], arg2[4], uint64(p384Uint1(x8)))
1589	var x11 uint64
1590	var x12 uint64
1591	x11, x12 = bits.Sub64(arg1[5], arg2[5], uint64(p384Uint1(x10)))
1592	var x13 uint64
1593	p384CmovznzU64(&x13, p384Uint1(x12), uint64(0x0), 0xffffffffffffffff)
1594	var x14 uint64
1595	var x15 uint64
1596	x14, x15 = bits.Add64(x1, (x13 & 0xffffffff), uint64(0x0))
1597	var x16 uint64
1598	var x17 uint64
1599	x16, x17 = bits.Add64(x3, (x13 & 0xffffffff00000000), uint64(p384Uint1(x15)))
1600	var x18 uint64
1601	var x19 uint64
1602	x18, x19 = bits.Add64(x5, (x13 & 0xfffffffffffffffe), uint64(p384Uint1(x17)))
1603	var x20 uint64
1604	var x21 uint64
1605	x20, x21 = bits.Add64(x7, x13, uint64(p384Uint1(x19)))
1606	var x22 uint64
1607	var x23 uint64
1608	x22, x23 = bits.Add64(x9, x13, uint64(p384Uint1(x21)))
1609	var x24 uint64
1610	x24, _ = bits.Add64(x11, x13, uint64(p384Uint1(x23)))
1611	out1[0] = x14
1612	out1[1] = x16
1613	out1[2] = x18
1614	out1[3] = x20
1615	out1[4] = x22
1616	out1[5] = x24
1617}
1618
1619// p384SetOne returns the field element one in the Montgomery domain.
1620//
1621// Postconditions:
1622//
1623//	eval (from_montgomery out1) mod m = 1 mod m
1624//	0 ≤ eval out1 < m
1625func p384SetOne(out1 *p384MontgomeryDomainFieldElement) {
1626	out1[0] = 0xffffffff00000001
1627	out1[1] = 0xffffffff
1628	out1[2] = uint64(0x1)
1629	out1[3] = uint64(0x0)
1630	out1[4] = uint64(0x0)
1631	out1[5] = uint64(0x0)
1632}
1633
1634// p384FromMontgomery translates a field element out of the Montgomery domain.
1635//
1636// Preconditions:
1637//
1638//	0 ≤ eval arg1 < m
1639//
1640// Postconditions:
1641//
1642//	eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^6) mod m
1643//	0 ≤ eval out1 < m
1644func p384FromMontgomery(out1 *p384NonMontgomeryDomainFieldElement, arg1 *p384MontgomeryDomainFieldElement) {
1645	x1 := arg1[0]
1646	var x2 uint64
1647	_, x2 = bits.Mul64(x1, 0x100000001)
1648	var x4 uint64
1649	var x5 uint64
1650	x5, x4 = bits.Mul64(x2, 0xffffffffffffffff)
1651	var x6 uint64
1652	var x7 uint64
1653	x7, x6 = bits.Mul64(x2, 0xffffffffffffffff)
1654	var x8 uint64
1655	var x9 uint64
1656	x9, x8 = bits.Mul64(x2, 0xffffffffffffffff)
1657	var x10 uint64
1658	var x11 uint64
1659	x11, x10 = bits.Mul64(x2, 0xfffffffffffffffe)
1660	var x12 uint64
1661	var x13 uint64
1662	x13, x12 = bits.Mul64(x2, 0xffffffff00000000)
1663	var x14 uint64
1664	var x15 uint64
1665	x15, x14 = bits.Mul64(x2, 0xffffffff)
1666	var x16 uint64
1667	var x17 uint64
1668	x16, x17 = bits.Add64(x15, x12, uint64(0x0))
1669	var x18 uint64
1670	var x19 uint64
1671	x18, x19 = bits.Add64(x13, x10, uint64(p384Uint1(x17)))
1672	var x20 uint64
1673	var x21 uint64
1674	x20, x21 = bits.Add64(x11, x8, uint64(p384Uint1(x19)))
1675	var x22 uint64
1676	var x23 uint64
1677	x22, x23 = bits.Add64(x9, x6, uint64(p384Uint1(x21)))
1678	var x24 uint64
1679	var x25 uint64
1680	x24, x25 = bits.Add64(x7, x4, uint64(p384Uint1(x23)))
1681	var x27 uint64
1682	_, x27 = bits.Add64(x1, x14, uint64(0x0))
1683	var x28 uint64
1684	var x29 uint64
1685	x28, x29 = bits.Add64(uint64(0x0), x16, uint64(p384Uint1(x27)))
1686	var x30 uint64
1687	var x31 uint64
1688	x30, x31 = bits.Add64(uint64(0x0), x18, uint64(p384Uint1(x29)))
1689	var x32 uint64
1690	var x33 uint64
1691	x32, x33 = bits.Add64(uint64(0x0), x20, uint64(p384Uint1(x31)))
1692	var x34 uint64
1693	var x35 uint64
1694	x34, x35 = bits.Add64(uint64(0x0), x22, uint64(p384Uint1(x33)))
1695	var x36 uint64
1696	var x37 uint64
1697	x36, x37 = bits.Add64(uint64(0x0), x24, uint64(p384Uint1(x35)))
1698	var x38 uint64
1699	var x39 uint64
1700	x38, x39 = bits.Add64(uint64(0x0), (uint64(p384Uint1(x25)) + x5), uint64(p384Uint1(x37)))
1701	var x40 uint64
1702	var x41 uint64
1703	x40, x41 = bits.Add64(x28, arg1[1], uint64(0x0))
1704	var x42 uint64
1705	var x43 uint64
1706	x42, x43 = bits.Add64(x30, uint64(0x0), uint64(p384Uint1(x41)))
1707	var x44 uint64
1708	var x45 uint64
1709	x44, x45 = bits.Add64(x32, uint64(0x0), uint64(p384Uint1(x43)))
1710	var x46 uint64
1711	var x47 uint64
1712	x46, x47 = bits.Add64(x34, uint64(0x0), uint64(p384Uint1(x45)))
1713	var x48 uint64
1714	var x49 uint64
1715	x48, x49 = bits.Add64(x36, uint64(0x0), uint64(p384Uint1(x47)))
1716	var x50 uint64
1717	var x51 uint64
1718	x50, x51 = bits.Add64(x38, uint64(0x0), uint64(p384Uint1(x49)))
1719	var x52 uint64
1720	_, x52 = bits.Mul64(x40, 0x100000001)
1721	var x54 uint64
1722	var x55 uint64
1723	x55, x54 = bits.Mul64(x52, 0xffffffffffffffff)
1724	var x56 uint64
1725	var x57 uint64
1726	x57, x56 = bits.Mul64(x52, 0xffffffffffffffff)
1727	var x58 uint64
1728	var x59 uint64
1729	x59, x58 = bits.Mul64(x52, 0xffffffffffffffff)
1730	var x60 uint64
1731	var x61 uint64
1732	x61, x60 = bits.Mul64(x52, 0xfffffffffffffffe)
1733	var x62 uint64
1734	var x63 uint64
1735	x63, x62 = bits.Mul64(x52, 0xffffffff00000000)
1736	var x64 uint64
1737	var x65 uint64
1738	x65, x64 = bits.Mul64(x52, 0xffffffff)
1739	var x66 uint64
1740	var x67 uint64
1741	x66, x67 = bits.Add64(x65, x62, uint64(0x0))
1742	var x68 uint64
1743	var x69 uint64
1744	x68, x69 = bits.Add64(x63, x60, uint64(p384Uint1(x67)))
1745	var x70 uint64
1746	var x71 uint64
1747	x70, x71 = bits.Add64(x61, x58, uint64(p384Uint1(x69)))
1748	var x72 uint64
1749	var x73 uint64
1750	x72, x73 = bits.Add64(x59, x56, uint64(p384Uint1(x71)))
1751	var x74 uint64
1752	var x75 uint64
1753	x74, x75 = bits.Add64(x57, x54, uint64(p384Uint1(x73)))
1754	var x77 uint64
1755	_, x77 = bits.Add64(x40, x64, uint64(0x0))
1756	var x78 uint64
1757	var x79 uint64
1758	x78, x79 = bits.Add64(x42, x66, uint64(p384Uint1(x77)))
1759	var x80 uint64
1760	var x81 uint64
1761	x80, x81 = bits.Add64(x44, x68, uint64(p384Uint1(x79)))
1762	var x82 uint64
1763	var x83 uint64
1764	x82, x83 = bits.Add64(x46, x70, uint64(p384Uint1(x81)))
1765	var x84 uint64
1766	var x85 uint64
1767	x84, x85 = bits.Add64(x48, x72, uint64(p384Uint1(x83)))
1768	var x86 uint64
1769	var x87 uint64
1770	x86, x87 = bits.Add64(x50, x74, uint64(p384Uint1(x85)))
1771	var x88 uint64
1772	var x89 uint64
1773	x88, x89 = bits.Add64((uint64(p384Uint1(x51)) + uint64(p384Uint1(x39))), (uint64(p384Uint1(x75)) + x55), uint64(p384Uint1(x87)))
1774	var x90 uint64
1775	var x91 uint64
1776	x90, x91 = bits.Add64(x78, arg1[2], uint64(0x0))
1777	var x92 uint64
1778	var x93 uint64
1779	x92, x93 = bits.Add64(x80, uint64(0x0), uint64(p384Uint1(x91)))
1780	var x94 uint64
1781	var x95 uint64
1782	x94, x95 = bits.Add64(x82, uint64(0x0), uint64(p384Uint1(x93)))
1783	var x96 uint64
1784	var x97 uint64
1785	x96, x97 = bits.Add64(x84, uint64(0x0), uint64(p384Uint1(x95)))
1786	var x98 uint64
1787	var x99 uint64
1788	x98, x99 = bits.Add64(x86, uint64(0x0), uint64(p384Uint1(x97)))
1789	var x100 uint64
1790	var x101 uint64
1791	x100, x101 = bits.Add64(x88, uint64(0x0), uint64(p384Uint1(x99)))
1792	var x102 uint64
1793	_, x102 = bits.Mul64(x90, 0x100000001)
1794	var x104 uint64
1795	var x105 uint64
1796	x105, x104 = bits.Mul64(x102, 0xffffffffffffffff)
1797	var x106 uint64
1798	var x107 uint64
1799	x107, x106 = bits.Mul64(x102, 0xffffffffffffffff)
1800	var x108 uint64
1801	var x109 uint64
1802	x109, x108 = bits.Mul64(x102, 0xffffffffffffffff)
1803	var x110 uint64
1804	var x111 uint64
1805	x111, x110 = bits.Mul64(x102, 0xfffffffffffffffe)
1806	var x112 uint64
1807	var x113 uint64
1808	x113, x112 = bits.Mul64(x102, 0xffffffff00000000)
1809	var x114 uint64
1810	var x115 uint64
1811	x115, x114 = bits.Mul64(x102, 0xffffffff)
1812	var x116 uint64
1813	var x117 uint64
1814	x116, x117 = bits.Add64(x115, x112, uint64(0x0))
1815	var x118 uint64
1816	var x119 uint64
1817	x118, x119 = bits.Add64(x113, x110, uint64(p384Uint1(x117)))
1818	var x120 uint64
1819	var x121 uint64
1820	x120, x121 = bits.Add64(x111, x108, uint64(p384Uint1(x119)))
1821	var x122 uint64
1822	var x123 uint64
1823	x122, x123 = bits.Add64(x109, x106, uint64(p384Uint1(x121)))
1824	var x124 uint64
1825	var x125 uint64
1826	x124, x125 = bits.Add64(x107, x104, uint64(p384Uint1(x123)))
1827	var x127 uint64
1828	_, x127 = bits.Add64(x90, x114, uint64(0x0))
1829	var x128 uint64
1830	var x129 uint64
1831	x128, x129 = bits.Add64(x92, x116, uint64(p384Uint1(x127)))
1832	var x130 uint64
1833	var x131 uint64
1834	x130, x131 = bits.Add64(x94, x118, uint64(p384Uint1(x129)))
1835	var x132 uint64
1836	var x133 uint64
1837	x132, x133 = bits.Add64(x96, x120, uint64(p384Uint1(x131)))
1838	var x134 uint64
1839	var x135 uint64
1840	x134, x135 = bits.Add64(x98, x122, uint64(p384Uint1(x133)))
1841	var x136 uint64
1842	var x137 uint64
1843	x136, x137 = bits.Add64(x100, x124, uint64(p384Uint1(x135)))
1844	var x138 uint64
1845	var x139 uint64
1846	x138, x139 = bits.Add64((uint64(p384Uint1(x101)) + uint64(p384Uint1(x89))), (uint64(p384Uint1(x125)) + x105), uint64(p384Uint1(x137)))
1847	var x140 uint64
1848	var x141 uint64
1849	x140, x141 = bits.Add64(x128, arg1[3], uint64(0x0))
1850	var x142 uint64
1851	var x143 uint64
1852	x142, x143 = bits.Add64(x130, uint64(0x0), uint64(p384Uint1(x141)))
1853	var x144 uint64
1854	var x145 uint64
1855	x144, x145 = bits.Add64(x132, uint64(0x0), uint64(p384Uint1(x143)))
1856	var x146 uint64
1857	var x147 uint64
1858	x146, x147 = bits.Add64(x134, uint64(0x0), uint64(p384Uint1(x145)))
1859	var x148 uint64
1860	var x149 uint64
1861	x148, x149 = bits.Add64(x136, uint64(0x0), uint64(p384Uint1(x147)))
1862	var x150 uint64
1863	var x151 uint64
1864	x150, x151 = bits.Add64(x138, uint64(0x0), uint64(p384Uint1(x149)))
1865	var x152 uint64
1866	_, x152 = bits.Mul64(x140, 0x100000001)
1867	var x154 uint64
1868	var x155 uint64
1869	x155, x154 = bits.Mul64(x152, 0xffffffffffffffff)
1870	var x156 uint64
1871	var x157 uint64
1872	x157, x156 = bits.Mul64(x152, 0xffffffffffffffff)
1873	var x158 uint64
1874	var x159 uint64
1875	x159, x158 = bits.Mul64(x152, 0xffffffffffffffff)
1876	var x160 uint64
1877	var x161 uint64
1878	x161, x160 = bits.Mul64(x152, 0xfffffffffffffffe)
1879	var x162 uint64
1880	var x163 uint64
1881	x163, x162 = bits.Mul64(x152, 0xffffffff00000000)
1882	var x164 uint64
1883	var x165 uint64
1884	x165, x164 = bits.Mul64(x152, 0xffffffff)
1885	var x166 uint64
1886	var x167 uint64
1887	x166, x167 = bits.Add64(x165, x162, uint64(0x0))
1888	var x168 uint64
1889	var x169 uint64
1890	x168, x169 = bits.Add64(x163, x160, uint64(p384Uint1(x167)))
1891	var x170 uint64
1892	var x171 uint64
1893	x170, x171 = bits.Add64(x161, x158, uint64(p384Uint1(x169)))
1894	var x172 uint64
1895	var x173 uint64
1896	x172, x173 = bits.Add64(x159, x156, uint64(p384Uint1(x171)))
1897	var x174 uint64
1898	var x175 uint64
1899	x174, x175 = bits.Add64(x157, x154, uint64(p384Uint1(x173)))
1900	var x177 uint64
1901	_, x177 = bits.Add64(x140, x164, uint64(0x0))
1902	var x178 uint64
1903	var x179 uint64
1904	x178, x179 = bits.Add64(x142, x166, uint64(p384Uint1(x177)))
1905	var x180 uint64
1906	var x181 uint64
1907	x180, x181 = bits.Add64(x144, x168, uint64(p384Uint1(x179)))
1908	var x182 uint64
1909	var x183 uint64
1910	x182, x183 = bits.Add64(x146, x170, uint64(p384Uint1(x181)))
1911	var x184 uint64
1912	var x185 uint64
1913	x184, x185 = bits.Add64(x148, x172, uint64(p384Uint1(x183)))
1914	var x186 uint64
1915	var x187 uint64
1916	x186, x187 = bits.Add64(x150, x174, uint64(p384Uint1(x185)))
1917	var x188 uint64
1918	var x189 uint64
1919	x188, x189 = bits.Add64((uint64(p384Uint1(x151)) + uint64(p384Uint1(x139))), (uint64(p384Uint1(x175)) + x155), uint64(p384Uint1(x187)))
1920	var x190 uint64
1921	var x191 uint64
1922	x190, x191 = bits.Add64(x178, arg1[4], uint64(0x0))
1923	var x192 uint64
1924	var x193 uint64
1925	x192, x193 = bits.Add64(x180, uint64(0x0), uint64(p384Uint1(x191)))
1926	var x194 uint64
1927	var x195 uint64
1928	x194, x195 = bits.Add64(x182, uint64(0x0), uint64(p384Uint1(x193)))
1929	var x196 uint64
1930	var x197 uint64
1931	x196, x197 = bits.Add64(x184, uint64(0x0), uint64(p384Uint1(x195)))
1932	var x198 uint64
1933	var x199 uint64
1934	x198, x199 = bits.Add64(x186, uint64(0x0), uint64(p384Uint1(x197)))
1935	var x200 uint64
1936	var x201 uint64
1937	x200, x201 = bits.Add64(x188, uint64(0x0), uint64(p384Uint1(x199)))
1938	var x202 uint64
1939	_, x202 = bits.Mul64(x190, 0x100000001)
1940	var x204 uint64
1941	var x205 uint64
1942	x205, x204 = bits.Mul64(x202, 0xffffffffffffffff)
1943	var x206 uint64
1944	var x207 uint64
1945	x207, x206 = bits.Mul64(x202, 0xffffffffffffffff)
1946	var x208 uint64
1947	var x209 uint64
1948	x209, x208 = bits.Mul64(x202, 0xffffffffffffffff)
1949	var x210 uint64
1950	var x211 uint64
1951	x211, x210 = bits.Mul64(x202, 0xfffffffffffffffe)
1952	var x212 uint64
1953	var x213 uint64
1954	x213, x212 = bits.Mul64(x202, 0xffffffff00000000)
1955	var x214 uint64
1956	var x215 uint64
1957	x215, x214 = bits.Mul64(x202, 0xffffffff)
1958	var x216 uint64
1959	var x217 uint64
1960	x216, x217 = bits.Add64(x215, x212, uint64(0x0))
1961	var x218 uint64
1962	var x219 uint64
1963	x218, x219 = bits.Add64(x213, x210, uint64(p384Uint1(x217)))
1964	var x220 uint64
1965	var x221 uint64
1966	x220, x221 = bits.Add64(x211, x208, uint64(p384Uint1(x219)))
1967	var x222 uint64
1968	var x223 uint64
1969	x222, x223 = bits.Add64(x209, x206, uint64(p384Uint1(x221)))
1970	var x224 uint64
1971	var x225 uint64
1972	x224, x225 = bits.Add64(x207, x204, uint64(p384Uint1(x223)))
1973	var x227 uint64
1974	_, x227 = bits.Add64(x190, x214, uint64(0x0))
1975	var x228 uint64
1976	var x229 uint64
1977	x228, x229 = bits.Add64(x192, x216, uint64(p384Uint1(x227)))
1978	var x230 uint64
1979	var x231 uint64
1980	x230, x231 = bits.Add64(x194, x218, uint64(p384Uint1(x229)))
1981	var x232 uint64
1982	var x233 uint64
1983	x232, x233 = bits.Add64(x196, x220, uint64(p384Uint1(x231)))
1984	var x234 uint64
1985	var x235 uint64
1986	x234, x235 = bits.Add64(x198, x222, uint64(p384Uint1(x233)))
1987	var x236 uint64
1988	var x237 uint64
1989	x236, x237 = bits.Add64(x200, x224, uint64(p384Uint1(x235)))
1990	var x238 uint64
1991	var x239 uint64
1992	x238, x239 = bits.Add64((uint64(p384Uint1(x201)) + uint64(p384Uint1(x189))), (uint64(p384Uint1(x225)) + x205), uint64(p384Uint1(x237)))
1993	var x240 uint64
1994	var x241 uint64
1995	x240, x241 = bits.Add64(x228, arg1[5], uint64(0x0))
1996	var x242 uint64
1997	var x243 uint64
1998	x242, x243 = bits.Add64(x230, uint64(0x0), uint64(p384Uint1(x241)))
1999	var x244 uint64
2000	var x245 uint64
2001	x244, x245 = bits.Add64(x232, uint64(0x0), uint64(p384Uint1(x243)))
2002	var x246 uint64
2003	var x247 uint64
2004	x246, x247 = bits.Add64(x234, uint64(0x0), uint64(p384Uint1(x245)))
2005	var x248 uint64
2006	var x249 uint64
2007	x248, x249 = bits.Add64(x236, uint64(0x0), uint64(p384Uint1(x247)))
2008	var x250 uint64
2009	var x251 uint64
2010	x250, x251 = bits.Add64(x238, uint64(0x0), uint64(p384Uint1(x249)))
2011	var x252 uint64
2012	_, x252 = bits.Mul64(x240, 0x100000001)
2013	var x254 uint64
2014	var x255 uint64
2015	x255, x254 = bits.Mul64(x252, 0xffffffffffffffff)
2016	var x256 uint64
2017	var x257 uint64
2018	x257, x256 = bits.Mul64(x252, 0xffffffffffffffff)
2019	var x258 uint64
2020	var x259 uint64
2021	x259, x258 = bits.Mul64(x252, 0xffffffffffffffff)
2022	var x260 uint64
2023	var x261 uint64
2024	x261, x260 = bits.Mul64(x252, 0xfffffffffffffffe)
2025	var x262 uint64
2026	var x263 uint64
2027	x263, x262 = bits.Mul64(x252, 0xffffffff00000000)
2028	var x264 uint64
2029	var x265 uint64
2030	x265, x264 = bits.Mul64(x252, 0xffffffff)
2031	var x266 uint64
2032	var x267 uint64
2033	x266, x267 = bits.Add64(x265, x262, uint64(0x0))
2034	var x268 uint64
2035	var x269 uint64
2036	x268, x269 = bits.Add64(x263, x260, uint64(p384Uint1(x267)))
2037	var x270 uint64
2038	var x271 uint64
2039	x270, x271 = bits.Add64(x261, x258, uint64(p384Uint1(x269)))
2040	var x272 uint64
2041	var x273 uint64
2042	x272, x273 = bits.Add64(x259, x256, uint64(p384Uint1(x271)))
2043	var x274 uint64
2044	var x275 uint64
2045	x274, x275 = bits.Add64(x257, x254, uint64(p384Uint1(x273)))
2046	var x277 uint64
2047	_, x277 = bits.Add64(x240, x264, uint64(0x0))
2048	var x278 uint64
2049	var x279 uint64
2050	x278, x279 = bits.Add64(x242, x266, uint64(p384Uint1(x277)))
2051	var x280 uint64
2052	var x281 uint64
2053	x280, x281 = bits.Add64(x244, x268, uint64(p384Uint1(x279)))
2054	var x282 uint64
2055	var x283 uint64
2056	x282, x283 = bits.Add64(x246, x270, uint64(p384Uint1(x281)))
2057	var x284 uint64
2058	var x285 uint64
2059	x284, x285 = bits.Add64(x248, x272, uint64(p384Uint1(x283)))
2060	var x286 uint64
2061	var x287 uint64
2062	x286, x287 = bits.Add64(x250, x274, uint64(p384Uint1(x285)))
2063	var x288 uint64
2064	var x289 uint64
2065	x288, x289 = bits.Add64((uint64(p384Uint1(x251)) + uint64(p384Uint1(x239))), (uint64(p384Uint1(x275)) + x255), uint64(p384Uint1(x287)))
2066	var x290 uint64
2067	var x291 uint64
2068	x290, x291 = bits.Sub64(x278, 0xffffffff, uint64(0x0))
2069	var x292 uint64
2070	var x293 uint64
2071	x292, x293 = bits.Sub64(x280, 0xffffffff00000000, uint64(p384Uint1(x291)))
2072	var x294 uint64
2073	var x295 uint64
2074	x294, x295 = bits.Sub64(x282, 0xfffffffffffffffe, uint64(p384Uint1(x293)))
2075	var x296 uint64
2076	var x297 uint64
2077	x296, x297 = bits.Sub64(x284, 0xffffffffffffffff, uint64(p384Uint1(x295)))
2078	var x298 uint64
2079	var x299 uint64
2080	x298, x299 = bits.Sub64(x286, 0xffffffffffffffff, uint64(p384Uint1(x297)))
2081	var x300 uint64
2082	var x301 uint64
2083	x300, x301 = bits.Sub64(x288, 0xffffffffffffffff, uint64(p384Uint1(x299)))
2084	var x303 uint64
2085	_, x303 = bits.Sub64(uint64(p384Uint1(x289)), uint64(0x0), uint64(p384Uint1(x301)))
2086	var x304 uint64
2087	p384CmovznzU64(&x304, p384Uint1(x303), x290, x278)
2088	var x305 uint64
2089	p384CmovznzU64(&x305, p384Uint1(x303), x292, x280)
2090	var x306 uint64
2091	p384CmovznzU64(&x306, p384Uint1(x303), x294, x282)
2092	var x307 uint64
2093	p384CmovznzU64(&x307, p384Uint1(x303), x296, x284)
2094	var x308 uint64
2095	p384CmovznzU64(&x308, p384Uint1(x303), x298, x286)
2096	var x309 uint64
2097	p384CmovznzU64(&x309, p384Uint1(x303), x300, x288)
2098	out1[0] = x304
2099	out1[1] = x305
2100	out1[2] = x306
2101	out1[3] = x307
2102	out1[4] = x308
2103	out1[5] = x309
2104}
2105
2106// p384ToMontgomery translates a field element into the Montgomery domain.
2107//
2108// Preconditions:
2109//
2110//	0 ≤ eval arg1 < m
2111//
2112// Postconditions:
2113//
2114//	eval (from_montgomery out1) mod m = eval arg1 mod m
2115//	0 ≤ eval out1 < m
2116func p384ToMontgomery(out1 *p384MontgomeryDomainFieldElement, arg1 *p384NonMontgomeryDomainFieldElement) {
2117	x1 := arg1[1]
2118	x2 := arg1[2]
2119	x3 := arg1[3]
2120	x4 := arg1[4]
2121	x5 := arg1[5]
2122	x6 := arg1[0]
2123	var x7 uint64
2124	var x8 uint64
2125	x8, x7 = bits.Mul64(x6, 0x200000000)
2126	var x9 uint64
2127	var x10 uint64
2128	x10, x9 = bits.Mul64(x6, 0xfffffffe00000000)
2129	var x11 uint64
2130	var x12 uint64
2131	x12, x11 = bits.Mul64(x6, 0x200000000)
2132	var x13 uint64
2133	var x14 uint64
2134	x14, x13 = bits.Mul64(x6, 0xfffffffe00000001)
2135	var x15 uint64
2136	var x16 uint64
2137	x15, x16 = bits.Add64(x14, x11, uint64(0x0))
2138	var x17 uint64
2139	var x18 uint64
2140	x17, x18 = bits.Add64(x12, x9, uint64(p384Uint1(x16)))
2141	var x19 uint64
2142	var x20 uint64
2143	x19, x20 = bits.Add64(x10, x7, uint64(p384Uint1(x18)))
2144	var x21 uint64
2145	var x22 uint64
2146	x21, x22 = bits.Add64(x8, x6, uint64(p384Uint1(x20)))
2147	var x23 uint64
2148	_, x23 = bits.Mul64(x13, 0x100000001)
2149	var x25 uint64
2150	var x26 uint64
2151	x26, x25 = bits.Mul64(x23, 0xffffffffffffffff)
2152	var x27 uint64
2153	var x28 uint64
2154	x28, x27 = bits.Mul64(x23, 0xffffffffffffffff)
2155	var x29 uint64
2156	var x30 uint64
2157	x30, x29 = bits.Mul64(x23, 0xffffffffffffffff)
2158	var x31 uint64
2159	var x32 uint64
2160	x32, x31 = bits.Mul64(x23, 0xfffffffffffffffe)
2161	var x33 uint64
2162	var x34 uint64
2163	x34, x33 = bits.Mul64(x23, 0xffffffff00000000)
2164	var x35 uint64
2165	var x36 uint64
2166	x36, x35 = bits.Mul64(x23, 0xffffffff)
2167	var x37 uint64
2168	var x38 uint64
2169	x37, x38 = bits.Add64(x36, x33, uint64(0x0))
2170	var x39 uint64
2171	var x40 uint64
2172	x39, x40 = bits.Add64(x34, x31, uint64(p384Uint1(x38)))
2173	var x41 uint64
2174	var x42 uint64
2175	x41, x42 = bits.Add64(x32, x29, uint64(p384Uint1(x40)))
2176	var x43 uint64
2177	var x44 uint64
2178	x43, x44 = bits.Add64(x30, x27, uint64(p384Uint1(x42)))
2179	var x45 uint64
2180	var x46 uint64
2181	x45, x46 = bits.Add64(x28, x25, uint64(p384Uint1(x44)))
2182	var x48 uint64
2183	_, x48 = bits.Add64(x13, x35, uint64(0x0))
2184	var x49 uint64
2185	var x50 uint64
2186	x49, x50 = bits.Add64(x15, x37, uint64(p384Uint1(x48)))
2187	var x51 uint64
2188	var x52 uint64
2189	x51, x52 = bits.Add64(x17, x39, uint64(p384Uint1(x50)))
2190	var x53 uint64
2191	var x54 uint64
2192	x53, x54 = bits.Add64(x19, x41, uint64(p384Uint1(x52)))
2193	var x55 uint64
2194	var x56 uint64
2195	x55, x56 = bits.Add64(x21, x43, uint64(p384Uint1(x54)))
2196	var x57 uint64
2197	var x58 uint64
2198	x57, x58 = bits.Add64(uint64(p384Uint1(x22)), x45, uint64(p384Uint1(x56)))
2199	var x59 uint64
2200	var x60 uint64
2201	x59, x60 = bits.Add64(uint64(0x0), (uint64(p384Uint1(x46)) + x26), uint64(p384Uint1(x58)))
2202	var x61 uint64
2203	var x62 uint64
2204	x62, x61 = bits.Mul64(x1, 0x200000000)
2205	var x63 uint64
2206	var x64 uint64
2207	x64, x63 = bits.Mul64(x1, 0xfffffffe00000000)
2208	var x65 uint64
2209	var x66 uint64
2210	x66, x65 = bits.Mul64(x1, 0x200000000)
2211	var x67 uint64
2212	var x68 uint64
2213	x68, x67 = bits.Mul64(x1, 0xfffffffe00000001)
2214	var x69 uint64
2215	var x70 uint64
2216	x69, x70 = bits.Add64(x68, x65, uint64(0x0))
2217	var x71 uint64
2218	var x72 uint64
2219	x71, x72 = bits.Add64(x66, x63, uint64(p384Uint1(x70)))
2220	var x73 uint64
2221	var x74 uint64
2222	x73, x74 = bits.Add64(x64, x61, uint64(p384Uint1(x72)))
2223	var x75 uint64
2224	var x76 uint64
2225	x75, x76 = bits.Add64(x62, x1, uint64(p384Uint1(x74)))
2226	var x77 uint64
2227	var x78 uint64
2228	x77, x78 = bits.Add64(x49, x67, uint64(0x0))
2229	var x79 uint64
2230	var x80 uint64
2231	x79, x80 = bits.Add64(x51, x69, uint64(p384Uint1(x78)))
2232	var x81 uint64
2233	var x82 uint64
2234	x81, x82 = bits.Add64(x53, x71, uint64(p384Uint1(x80)))
2235	var x83 uint64
2236	var x84 uint64
2237	x83, x84 = bits.Add64(x55, x73, uint64(p384Uint1(x82)))
2238	var x85 uint64
2239	var x86 uint64
2240	x85, x86 = bits.Add64(x57, x75, uint64(p384Uint1(x84)))
2241	var x87 uint64
2242	var x88 uint64
2243	x87, x88 = bits.Add64(x59, uint64(p384Uint1(x76)), uint64(p384Uint1(x86)))
2244	var x89 uint64
2245	_, x89 = bits.Mul64(x77, 0x100000001)
2246	var x91 uint64
2247	var x92 uint64
2248	x92, x91 = bits.Mul64(x89, 0xffffffffffffffff)
2249	var x93 uint64
2250	var x94 uint64
2251	x94, x93 = bits.Mul64(x89, 0xffffffffffffffff)
2252	var x95 uint64
2253	var x96 uint64
2254	x96, x95 = bits.Mul64(x89, 0xffffffffffffffff)
2255	var x97 uint64
2256	var x98 uint64
2257	x98, x97 = bits.Mul64(x89, 0xfffffffffffffffe)
2258	var x99 uint64
2259	var x100 uint64
2260	x100, x99 = bits.Mul64(x89, 0xffffffff00000000)
2261	var x101 uint64
2262	var x102 uint64
2263	x102, x101 = bits.Mul64(x89, 0xffffffff)
2264	var x103 uint64
2265	var x104 uint64
2266	x103, x104 = bits.Add64(x102, x99, uint64(0x0))
2267	var x105 uint64
2268	var x106 uint64
2269	x105, x106 = bits.Add64(x100, x97, uint64(p384Uint1(x104)))
2270	var x107 uint64
2271	var x108 uint64
2272	x107, x108 = bits.Add64(x98, x95, uint64(p384Uint1(x106)))
2273	var x109 uint64
2274	var x110 uint64
2275	x109, x110 = bits.Add64(x96, x93, uint64(p384Uint1(x108)))
2276	var x111 uint64
2277	var x112 uint64
2278	x111, x112 = bits.Add64(x94, x91, uint64(p384Uint1(x110)))
2279	var x114 uint64
2280	_, x114 = bits.Add64(x77, x101, uint64(0x0))
2281	var x115 uint64
2282	var x116 uint64
2283	x115, x116 = bits.Add64(x79, x103, uint64(p384Uint1(x114)))
2284	var x117 uint64
2285	var x118 uint64
2286	x117, x118 = bits.Add64(x81, x105, uint64(p384Uint1(x116)))
2287	var x119 uint64
2288	var x120 uint64
2289	x119, x120 = bits.Add64(x83, x107, uint64(p384Uint1(x118)))
2290	var x121 uint64
2291	var x122 uint64
2292	x121, x122 = bits.Add64(x85, x109, uint64(p384Uint1(x120)))
2293	var x123 uint64
2294	var x124 uint64
2295	x123, x124 = bits.Add64(x87, x111, uint64(p384Uint1(x122)))
2296	var x125 uint64
2297	var x126 uint64
2298	x125, x126 = bits.Add64((uint64(p384Uint1(x88)) + uint64(p384Uint1(x60))), (uint64(p384Uint1(x112)) + x92), uint64(p384Uint1(x124)))
2299	var x127 uint64
2300	var x128 uint64
2301	x128, x127 = bits.Mul64(x2, 0x200000000)
2302	var x129 uint64
2303	var x130 uint64
2304	x130, x129 = bits.Mul64(x2, 0xfffffffe00000000)
2305	var x131 uint64
2306	var x132 uint64
2307	x132, x131 = bits.Mul64(x2, 0x200000000)
2308	var x133 uint64
2309	var x134 uint64
2310	x134, x133 = bits.Mul64(x2, 0xfffffffe00000001)
2311	var x135 uint64
2312	var x136 uint64
2313	x135, x136 = bits.Add64(x134, x131, uint64(0x0))
2314	var x137 uint64
2315	var x138 uint64
2316	x137, x138 = bits.Add64(x132, x129, uint64(p384Uint1(x136)))
2317	var x139 uint64
2318	var x140 uint64
2319	x139, x140 = bits.Add64(x130, x127, uint64(p384Uint1(x138)))
2320	var x141 uint64
2321	var x142 uint64
2322	x141, x142 = bits.Add64(x128, x2, uint64(p384Uint1(x140)))
2323	var x143 uint64
2324	var x144 uint64
2325	x143, x144 = bits.Add64(x115, x133, uint64(0x0))
2326	var x145 uint64
2327	var x146 uint64
2328	x145, x146 = bits.Add64(x117, x135, uint64(p384Uint1(x144)))
2329	var x147 uint64
2330	var x148 uint64
2331	x147, x148 = bits.Add64(x119, x137, uint64(p384Uint1(x146)))
2332	var x149 uint64
2333	var x150 uint64
2334	x149, x150 = bits.Add64(x121, x139, uint64(p384Uint1(x148)))
2335	var x151 uint64
2336	var x152 uint64
2337	x151, x152 = bits.Add64(x123, x141, uint64(p384Uint1(x150)))
2338	var x153 uint64
2339	var x154 uint64
2340	x153, x154 = bits.Add64(x125, uint64(p384Uint1(x142)), uint64(p384Uint1(x152)))
2341	var x155 uint64
2342	_, x155 = bits.Mul64(x143, 0x100000001)
2343	var x157 uint64
2344	var x158 uint64
2345	x158, x157 = bits.Mul64(x155, 0xffffffffffffffff)
2346	var x159 uint64
2347	var x160 uint64
2348	x160, x159 = bits.Mul64(x155, 0xffffffffffffffff)
2349	var x161 uint64
2350	var x162 uint64
2351	x162, x161 = bits.Mul64(x155, 0xffffffffffffffff)
2352	var x163 uint64
2353	var x164 uint64
2354	x164, x163 = bits.Mul64(x155, 0xfffffffffffffffe)
2355	var x165 uint64
2356	var x166 uint64
2357	x166, x165 = bits.Mul64(x155, 0xffffffff00000000)
2358	var x167 uint64
2359	var x168 uint64
2360	x168, x167 = bits.Mul64(x155, 0xffffffff)
2361	var x169 uint64
2362	var x170 uint64
2363	x169, x170 = bits.Add64(x168, x165, uint64(0x0))
2364	var x171 uint64
2365	var x172 uint64
2366	x171, x172 = bits.Add64(x166, x163, uint64(p384Uint1(x170)))
2367	var x173 uint64
2368	var x174 uint64
2369	x173, x174 = bits.Add64(x164, x161, uint64(p384Uint1(x172)))
2370	var x175 uint64
2371	var x176 uint64
2372	x175, x176 = bits.Add64(x162, x159, uint64(p384Uint1(x174)))
2373	var x177 uint64
2374	var x178 uint64
2375	x177, x178 = bits.Add64(x160, x157, uint64(p384Uint1(x176)))
2376	var x180 uint64
2377	_, x180 = bits.Add64(x143, x167, uint64(0x0))
2378	var x181 uint64
2379	var x182 uint64
2380	x181, x182 = bits.Add64(x145, x169, uint64(p384Uint1(x180)))
2381	var x183 uint64
2382	var x184 uint64
2383	x183, x184 = bits.Add64(x147, x171, uint64(p384Uint1(x182)))
2384	var x185 uint64
2385	var x186 uint64
2386	x185, x186 = bits.Add64(x149, x173, uint64(p384Uint1(x184)))
2387	var x187 uint64
2388	var x188 uint64
2389	x187, x188 = bits.Add64(x151, x175, uint64(p384Uint1(x186)))
2390	var x189 uint64
2391	var x190 uint64
2392	x189, x190 = bits.Add64(x153, x177, uint64(p384Uint1(x188)))
2393	var x191 uint64
2394	var x192 uint64
2395	x191, x192 = bits.Add64((uint64(p384Uint1(x154)) + uint64(p384Uint1(x126))), (uint64(p384Uint1(x178)) + x158), uint64(p384Uint1(x190)))
2396	var x193 uint64
2397	var x194 uint64
2398	x194, x193 = bits.Mul64(x3, 0x200000000)
2399	var x195 uint64
2400	var x196 uint64
2401	x196, x195 = bits.Mul64(x3, 0xfffffffe00000000)
2402	var x197 uint64
2403	var x198 uint64
2404	x198, x197 = bits.Mul64(x3, 0x200000000)
2405	var x199 uint64
2406	var x200 uint64
2407	x200, x199 = bits.Mul64(x3, 0xfffffffe00000001)
2408	var x201 uint64
2409	var x202 uint64
2410	x201, x202 = bits.Add64(x200, x197, uint64(0x0))
2411	var x203 uint64
2412	var x204 uint64
2413	x203, x204 = bits.Add64(x198, x195, uint64(p384Uint1(x202)))
2414	var x205 uint64
2415	var x206 uint64
2416	x205, x206 = bits.Add64(x196, x193, uint64(p384Uint1(x204)))
2417	var x207 uint64
2418	var x208 uint64
2419	x207, x208 = bits.Add64(x194, x3, uint64(p384Uint1(x206)))
2420	var x209 uint64
2421	var x210 uint64
2422	x209, x210 = bits.Add64(x181, x199, uint64(0x0))
2423	var x211 uint64
2424	var x212 uint64
2425	x211, x212 = bits.Add64(x183, x201, uint64(p384Uint1(x210)))
2426	var x213 uint64
2427	var x214 uint64
2428	x213, x214 = bits.Add64(x185, x203, uint64(p384Uint1(x212)))
2429	var x215 uint64
2430	var x216 uint64
2431	x215, x216 = bits.Add64(x187, x205, uint64(p384Uint1(x214)))
2432	var x217 uint64
2433	var x218 uint64
2434	x217, x218 = bits.Add64(x189, x207, uint64(p384Uint1(x216)))
2435	var x219 uint64
2436	var x220 uint64
2437	x219, x220 = bits.Add64(x191, uint64(p384Uint1(x208)), uint64(p384Uint1(x218)))
2438	var x221 uint64
2439	_, x221 = bits.Mul64(x209, 0x100000001)
2440	var x223 uint64
2441	var x224 uint64
2442	x224, x223 = bits.Mul64(x221, 0xffffffffffffffff)
2443	var x225 uint64
2444	var x226 uint64
2445	x226, x225 = bits.Mul64(x221, 0xffffffffffffffff)
2446	var x227 uint64
2447	var x228 uint64
2448	x228, x227 = bits.Mul64(x221, 0xffffffffffffffff)
2449	var x229 uint64
2450	var x230 uint64
2451	x230, x229 = bits.Mul64(x221, 0xfffffffffffffffe)
2452	var x231 uint64
2453	var x232 uint64
2454	x232, x231 = bits.Mul64(x221, 0xffffffff00000000)
2455	var x233 uint64
2456	var x234 uint64
2457	x234, x233 = bits.Mul64(x221, 0xffffffff)
2458	var x235 uint64
2459	var x236 uint64
2460	x235, x236 = bits.Add64(x234, x231, uint64(0x0))
2461	var x237 uint64
2462	var x238 uint64
2463	x237, x238 = bits.Add64(x232, x229, uint64(p384Uint1(x236)))
2464	var x239 uint64
2465	var x240 uint64
2466	x239, x240 = bits.Add64(x230, x227, uint64(p384Uint1(x238)))
2467	var x241 uint64
2468	var x242 uint64
2469	x241, x242 = bits.Add64(x228, x225, uint64(p384Uint1(x240)))
2470	var x243 uint64
2471	var x244 uint64
2472	x243, x244 = bits.Add64(x226, x223, uint64(p384Uint1(x242)))
2473	var x246 uint64
2474	_, x246 = bits.Add64(x209, x233, uint64(0x0))
2475	var x247 uint64
2476	var x248 uint64
2477	x247, x248 = bits.Add64(x211, x235, uint64(p384Uint1(x246)))
2478	var x249 uint64
2479	var x250 uint64
2480	x249, x250 = bits.Add64(x213, x237, uint64(p384Uint1(x248)))
2481	var x251 uint64
2482	var x252 uint64
2483	x251, x252 = bits.Add64(x215, x239, uint64(p384Uint1(x250)))
2484	var x253 uint64
2485	var x254 uint64
2486	x253, x254 = bits.Add64(x217, x241, uint64(p384Uint1(x252)))
2487	var x255 uint64
2488	var x256 uint64
2489	x255, x256 = bits.Add64(x219, x243, uint64(p384Uint1(x254)))
2490	var x257 uint64
2491	var x258 uint64
2492	x257, x258 = bits.Add64((uint64(p384Uint1(x220)) + uint64(p384Uint1(x192))), (uint64(p384Uint1(x244)) + x224), uint64(p384Uint1(x256)))
2493	var x259 uint64
2494	var x260 uint64
2495	x260, x259 = bits.Mul64(x4, 0x200000000)
2496	var x261 uint64
2497	var x262 uint64
2498	x262, x261 = bits.Mul64(x4, 0xfffffffe00000000)
2499	var x263 uint64
2500	var x264 uint64
2501	x264, x263 = bits.Mul64(x4, 0x200000000)
2502	var x265 uint64
2503	var x266 uint64
2504	x266, x265 = bits.Mul64(x4, 0xfffffffe00000001)
2505	var x267 uint64
2506	var x268 uint64
2507	x267, x268 = bits.Add64(x266, x263, uint64(0x0))
2508	var x269 uint64
2509	var x270 uint64
2510	x269, x270 = bits.Add64(x264, x261, uint64(p384Uint1(x268)))
2511	var x271 uint64
2512	var x272 uint64
2513	x271, x272 = bits.Add64(x262, x259, uint64(p384Uint1(x270)))
2514	var x273 uint64
2515	var x274 uint64
2516	x273, x274 = bits.Add64(x260, x4, uint64(p384Uint1(x272)))
2517	var x275 uint64
2518	var x276 uint64
2519	x275, x276 = bits.Add64(x247, x265, uint64(0x0))
2520	var x277 uint64
2521	var x278 uint64
2522	x277, x278 = bits.Add64(x249, x267, uint64(p384Uint1(x276)))
2523	var x279 uint64
2524	var x280 uint64
2525	x279, x280 = bits.Add64(x251, x269, uint64(p384Uint1(x278)))
2526	var x281 uint64
2527	var x282 uint64
2528	x281, x282 = bits.Add64(x253, x271, uint64(p384Uint1(x280)))
2529	var x283 uint64
2530	var x284 uint64
2531	x283, x284 = bits.Add64(x255, x273, uint64(p384Uint1(x282)))
2532	var x285 uint64
2533	var x286 uint64
2534	x285, x286 = bits.Add64(x257, uint64(p384Uint1(x274)), uint64(p384Uint1(x284)))
2535	var x287 uint64
2536	_, x287 = bits.Mul64(x275, 0x100000001)
2537	var x289 uint64
2538	var x290 uint64
2539	x290, x289 = bits.Mul64(x287, 0xffffffffffffffff)
2540	var x291 uint64
2541	var x292 uint64
2542	x292, x291 = bits.Mul64(x287, 0xffffffffffffffff)
2543	var x293 uint64
2544	var x294 uint64
2545	x294, x293 = bits.Mul64(x287, 0xffffffffffffffff)
2546	var x295 uint64
2547	var x296 uint64
2548	x296, x295 = bits.Mul64(x287, 0xfffffffffffffffe)
2549	var x297 uint64
2550	var x298 uint64
2551	x298, x297 = bits.Mul64(x287, 0xffffffff00000000)
2552	var x299 uint64
2553	var x300 uint64
2554	x300, x299 = bits.Mul64(x287, 0xffffffff)
2555	var x301 uint64
2556	var x302 uint64
2557	x301, x302 = bits.Add64(x300, x297, uint64(0x0))
2558	var x303 uint64
2559	var x304 uint64
2560	x303, x304 = bits.Add64(x298, x295, uint64(p384Uint1(x302)))
2561	var x305 uint64
2562	var x306 uint64
2563	x305, x306 = bits.Add64(x296, x293, uint64(p384Uint1(x304)))
2564	var x307 uint64
2565	var x308 uint64
2566	x307, x308 = bits.Add64(x294, x291, uint64(p384Uint1(x306)))
2567	var x309 uint64
2568	var x310 uint64
2569	x309, x310 = bits.Add64(x292, x289, uint64(p384Uint1(x308)))
2570	var x312 uint64
2571	_, x312 = bits.Add64(x275, x299, uint64(0x0))
2572	var x313 uint64
2573	var x314 uint64
2574	x313, x314 = bits.Add64(x277, x301, uint64(p384Uint1(x312)))
2575	var x315 uint64
2576	var x316 uint64
2577	x315, x316 = bits.Add64(x279, x303, uint64(p384Uint1(x314)))
2578	var x317 uint64
2579	var x318 uint64
2580	x317, x318 = bits.Add64(x281, x305, uint64(p384Uint1(x316)))
2581	var x319 uint64
2582	var x320 uint64
2583	x319, x320 = bits.Add64(x283, x307, uint64(p384Uint1(x318)))
2584	var x321 uint64
2585	var x322 uint64
2586	x321, x322 = bits.Add64(x285, x309, uint64(p384Uint1(x320)))
2587	var x323 uint64
2588	var x324 uint64
2589	x323, x324 = bits.Add64((uint64(p384Uint1(x286)) + uint64(p384Uint1(x258))), (uint64(p384Uint1(x310)) + x290), uint64(p384Uint1(x322)))
2590	var x325 uint64
2591	var x326 uint64
2592	x326, x325 = bits.Mul64(x5, 0x200000000)
2593	var x327 uint64
2594	var x328 uint64
2595	x328, x327 = bits.Mul64(x5, 0xfffffffe00000000)
2596	var x329 uint64
2597	var x330 uint64
2598	x330, x329 = bits.Mul64(x5, 0x200000000)
2599	var x331 uint64
2600	var x332 uint64
2601	x332, x331 = bits.Mul64(x5, 0xfffffffe00000001)
2602	var x333 uint64
2603	var x334 uint64
2604	x333, x334 = bits.Add64(x332, x329, uint64(0x0))
2605	var x335 uint64
2606	var x336 uint64
2607	x335, x336 = bits.Add64(x330, x327, uint64(p384Uint1(x334)))
2608	var x337 uint64
2609	var x338 uint64
2610	x337, x338 = bits.Add64(x328, x325, uint64(p384Uint1(x336)))
2611	var x339 uint64
2612	var x340 uint64
2613	x339, x340 = bits.Add64(x326, x5, uint64(p384Uint1(x338)))
2614	var x341 uint64
2615	var x342 uint64
2616	x341, x342 = bits.Add64(x313, x331, uint64(0x0))
2617	var x343 uint64
2618	var x344 uint64
2619	x343, x344 = bits.Add64(x315, x333, uint64(p384Uint1(x342)))
2620	var x345 uint64
2621	var x346 uint64
2622	x345, x346 = bits.Add64(x317, x335, uint64(p384Uint1(x344)))
2623	var x347 uint64
2624	var x348 uint64
2625	x347, x348 = bits.Add64(x319, x337, uint64(p384Uint1(x346)))
2626	var x349 uint64
2627	var x350 uint64
2628	x349, x350 = bits.Add64(x321, x339, uint64(p384Uint1(x348)))
2629	var x351 uint64
2630	var x352 uint64
2631	x351, x352 = bits.Add64(x323, uint64(p384Uint1(x340)), uint64(p384Uint1(x350)))
2632	var x353 uint64
2633	_, x353 = bits.Mul64(x341, 0x100000001)
2634	var x355 uint64
2635	var x356 uint64
2636	x356, x355 = bits.Mul64(x353, 0xffffffffffffffff)
2637	var x357 uint64
2638	var x358 uint64
2639	x358, x357 = bits.Mul64(x353, 0xffffffffffffffff)
2640	var x359 uint64
2641	var x360 uint64
2642	x360, x359 = bits.Mul64(x353, 0xffffffffffffffff)
2643	var x361 uint64
2644	var x362 uint64
2645	x362, x361 = bits.Mul64(x353, 0xfffffffffffffffe)
2646	var x363 uint64
2647	var x364 uint64
2648	x364, x363 = bits.Mul64(x353, 0xffffffff00000000)
2649	var x365 uint64
2650	var x366 uint64
2651	x366, x365 = bits.Mul64(x353, 0xffffffff)
2652	var x367 uint64
2653	var x368 uint64
2654	x367, x368 = bits.Add64(x366, x363, uint64(0x0))
2655	var x369 uint64
2656	var x370 uint64
2657	x369, x370 = bits.Add64(x364, x361, uint64(p384Uint1(x368)))
2658	var x371 uint64
2659	var x372 uint64
2660	x371, x372 = bits.Add64(x362, x359, uint64(p384Uint1(x370)))
2661	var x373 uint64
2662	var x374 uint64
2663	x373, x374 = bits.Add64(x360, x357, uint64(p384Uint1(x372)))
2664	var x375 uint64
2665	var x376 uint64
2666	x375, x376 = bits.Add64(x358, x355, uint64(p384Uint1(x374)))
2667	var x378 uint64
2668	_, x378 = bits.Add64(x341, x365, uint64(0x0))
2669	var x379 uint64
2670	var x380 uint64
2671	x379, x380 = bits.Add64(x343, x367, uint64(p384Uint1(x378)))
2672	var x381 uint64
2673	var x382 uint64
2674	x381, x382 = bits.Add64(x345, x369, uint64(p384Uint1(x380)))
2675	var x383 uint64
2676	var x384 uint64
2677	x383, x384 = bits.Add64(x347, x371, uint64(p384Uint1(x382)))
2678	var x385 uint64
2679	var x386 uint64
2680	x385, x386 = bits.Add64(x349, x373, uint64(p384Uint1(x384)))
2681	var x387 uint64
2682	var x388 uint64
2683	x387, x388 = bits.Add64(x351, x375, uint64(p384Uint1(x386)))
2684	var x389 uint64
2685	var x390 uint64
2686	x389, x390 = bits.Add64((uint64(p384Uint1(x352)) + uint64(p384Uint1(x324))), (uint64(p384Uint1(x376)) + x356), uint64(p384Uint1(x388)))
2687	var x391 uint64
2688	var x392 uint64
2689	x391, x392 = bits.Sub64(x379, 0xffffffff, uint64(0x0))
2690	var x393 uint64
2691	var x394 uint64
2692	x393, x394 = bits.Sub64(x381, 0xffffffff00000000, uint64(p384Uint1(x392)))
2693	var x395 uint64
2694	var x396 uint64
2695	x395, x396 = bits.Sub64(x383, 0xfffffffffffffffe, uint64(p384Uint1(x394)))
2696	var x397 uint64
2697	var x398 uint64
2698	x397, x398 = bits.Sub64(x385, 0xffffffffffffffff, uint64(p384Uint1(x396)))
2699	var x399 uint64
2700	var x400 uint64
2701	x399, x400 = bits.Sub64(x387, 0xffffffffffffffff, uint64(p384Uint1(x398)))
2702	var x401 uint64
2703	var x402 uint64
2704	x401, x402 = bits.Sub64(x389, 0xffffffffffffffff, uint64(p384Uint1(x400)))
2705	var x404 uint64
2706	_, x404 = bits.Sub64(uint64(p384Uint1(x390)), uint64(0x0), uint64(p384Uint1(x402)))
2707	var x405 uint64
2708	p384CmovznzU64(&x405, p384Uint1(x404), x391, x379)
2709	var x406 uint64
2710	p384CmovznzU64(&x406, p384Uint1(x404), x393, x381)
2711	var x407 uint64
2712	p384CmovznzU64(&x407, p384Uint1(x404), x395, x383)
2713	var x408 uint64
2714	p384CmovznzU64(&x408, p384Uint1(x404), x397, x385)
2715	var x409 uint64
2716	p384CmovznzU64(&x409, p384Uint1(x404), x399, x387)
2717	var x410 uint64
2718	p384CmovznzU64(&x410, p384Uint1(x404), x401, x389)
2719	out1[0] = x405
2720	out1[1] = x406
2721	out1[2] = x407
2722	out1[3] = x408
2723	out1[4] = x409
2724	out1[5] = x410
2725}
2726
2727// p384Selectznz is a multi-limb conditional select.
2728//
2729// Postconditions:
2730//
2731//	eval out1 = (if arg1 = 0 then eval arg2 else eval arg3)
2732//
2733// Input Bounds:
2734//
2735//	arg1: [0x0 ~> 0x1]
2736//	arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2737//	arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2738//
2739// Output Bounds:
2740//
2741//	out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2742func p384Selectznz(out1 *[6]uint64, arg1 p384Uint1, arg2 *[6]uint64, arg3 *[6]uint64) {
2743	var x1 uint64
2744	p384CmovznzU64(&x1, arg1, arg2[0], arg3[0])
2745	var x2 uint64
2746	p384CmovznzU64(&x2, arg1, arg2[1], arg3[1])
2747	var x3 uint64
2748	p384CmovznzU64(&x3, arg1, arg2[2], arg3[2])
2749	var x4 uint64
2750	p384CmovznzU64(&x4, arg1, arg2[3], arg3[3])
2751	var x5 uint64
2752	p384CmovznzU64(&x5, arg1, arg2[4], arg3[4])
2753	var x6 uint64
2754	p384CmovznzU64(&x6, arg1, arg2[5], arg3[5])
2755	out1[0] = x1
2756	out1[1] = x2
2757	out1[2] = x3
2758	out1[3] = x4
2759	out1[4] = x5
2760	out1[5] = x6
2761}
2762
2763// p384ToBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
2764//
2765// Preconditions:
2766//
2767//	0 ≤ eval arg1 < m
2768//
2769// Postconditions:
2770//
2771//	out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..47]
2772//
2773// Input Bounds:
2774//
2775//	arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2776//
2777// Output Bounds:
2778//
2779//	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]]
2780func p384ToBytes(out1 *[48]uint8, arg1 *[6]uint64) {
2781	x1 := arg1[5]
2782	x2 := arg1[4]
2783	x3 := arg1[3]
2784	x4 := arg1[2]
2785	x5 := arg1[1]
2786	x6 := arg1[0]
2787	x7 := (uint8(x6) & 0xff)
2788	x8 := (x6 >> 8)
2789	x9 := (uint8(x8) & 0xff)
2790	x10 := (x8 >> 8)
2791	x11 := (uint8(x10) & 0xff)
2792	x12 := (x10 >> 8)
2793	x13 := (uint8(x12) & 0xff)
2794	x14 := (x12 >> 8)
2795	x15 := (uint8(x14) & 0xff)
2796	x16 := (x14 >> 8)
2797	x17 := (uint8(x16) & 0xff)
2798	x18 := (x16 >> 8)
2799	x19 := (uint8(x18) & 0xff)
2800	x20 := uint8((x18 >> 8))
2801	x21 := (uint8(x5) & 0xff)
2802	x22 := (x5 >> 8)
2803	x23 := (uint8(x22) & 0xff)
2804	x24 := (x22 >> 8)
2805	x25 := (uint8(x24) & 0xff)
2806	x26 := (x24 >> 8)
2807	x27 := (uint8(x26) & 0xff)
2808	x28 := (x26 >> 8)
2809	x29 := (uint8(x28) & 0xff)
2810	x30 := (x28 >> 8)
2811	x31 := (uint8(x30) & 0xff)
2812	x32 := (x30 >> 8)
2813	x33 := (uint8(x32) & 0xff)
2814	x34 := uint8((x32 >> 8))
2815	x35 := (uint8(x4) & 0xff)
2816	x36 := (x4 >> 8)
2817	x37 := (uint8(x36) & 0xff)
2818	x38 := (x36 >> 8)
2819	x39 := (uint8(x38) & 0xff)
2820	x40 := (x38 >> 8)
2821	x41 := (uint8(x40) & 0xff)
2822	x42 := (x40 >> 8)
2823	x43 := (uint8(x42) & 0xff)
2824	x44 := (x42 >> 8)
2825	x45 := (uint8(x44) & 0xff)
2826	x46 := (x44 >> 8)
2827	x47 := (uint8(x46) & 0xff)
2828	x48 := uint8((x46 >> 8))
2829	x49 := (uint8(x3) & 0xff)
2830	x50 := (x3 >> 8)
2831	x51 := (uint8(x50) & 0xff)
2832	x52 := (x50 >> 8)
2833	x53 := (uint8(x52) & 0xff)
2834	x54 := (x52 >> 8)
2835	x55 := (uint8(x54) & 0xff)
2836	x56 := (x54 >> 8)
2837	x57 := (uint8(x56) & 0xff)
2838	x58 := (x56 >> 8)
2839	x59 := (uint8(x58) & 0xff)
2840	x60 := (x58 >> 8)
2841	x61 := (uint8(x60) & 0xff)
2842	x62 := uint8((x60 >> 8))
2843	x63 := (uint8(x2) & 0xff)
2844	x64 := (x2 >> 8)
2845	x65 := (uint8(x64) & 0xff)
2846	x66 := (x64 >> 8)
2847	x67 := (uint8(x66) & 0xff)
2848	x68 := (x66 >> 8)
2849	x69 := (uint8(x68) & 0xff)
2850	x70 := (x68 >> 8)
2851	x71 := (uint8(x70) & 0xff)
2852	x72 := (x70 >> 8)
2853	x73 := (uint8(x72) & 0xff)
2854	x74 := (x72 >> 8)
2855	x75 := (uint8(x74) & 0xff)
2856	x76 := uint8((x74 >> 8))
2857	x77 := (uint8(x1) & 0xff)
2858	x78 := (x1 >> 8)
2859	x79 := (uint8(x78) & 0xff)
2860	x80 := (x78 >> 8)
2861	x81 := (uint8(x80) & 0xff)
2862	x82 := (x80 >> 8)
2863	x83 := (uint8(x82) & 0xff)
2864	x84 := (x82 >> 8)
2865	x85 := (uint8(x84) & 0xff)
2866	x86 := (x84 >> 8)
2867	x87 := (uint8(x86) & 0xff)
2868	x88 := (x86 >> 8)
2869	x89 := (uint8(x88) & 0xff)
2870	x90 := uint8((x88 >> 8))
2871	out1[0] = x7
2872	out1[1] = x9
2873	out1[2] = x11
2874	out1[3] = x13
2875	out1[4] = x15
2876	out1[5] = x17
2877	out1[6] = x19
2878	out1[7] = x20
2879	out1[8] = x21
2880	out1[9] = x23
2881	out1[10] = x25
2882	out1[11] = x27
2883	out1[12] = x29
2884	out1[13] = x31
2885	out1[14] = x33
2886	out1[15] = x34
2887	out1[16] = x35
2888	out1[17] = x37
2889	out1[18] = x39
2890	out1[19] = x41
2891	out1[20] = x43
2892	out1[21] = x45
2893	out1[22] = x47
2894	out1[23] = x48
2895	out1[24] = x49
2896	out1[25] = x51
2897	out1[26] = x53
2898	out1[27] = x55
2899	out1[28] = x57
2900	out1[29] = x59
2901	out1[30] = x61
2902	out1[31] = x62
2903	out1[32] = x63
2904	out1[33] = x65
2905	out1[34] = x67
2906	out1[35] = x69
2907	out1[36] = x71
2908	out1[37] = x73
2909	out1[38] = x75
2910	out1[39] = x76
2911	out1[40] = x77
2912	out1[41] = x79
2913	out1[42] = x81
2914	out1[43] = x83
2915	out1[44] = x85
2916	out1[45] = x87
2917	out1[46] = x89
2918	out1[47] = x90
2919}
2920
2921// p384FromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
2922//
2923// Preconditions:
2924//
2925//	0 ≤ bytes_eval arg1 < m
2926//
2927// Postconditions:
2928//
2929//	eval out1 mod m = bytes_eval arg1 mod m
2930//	0 ≤ eval out1 < m
2931//
2932// Input Bounds:
2933//
2934//	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]]
2935//
2936// Output Bounds:
2937//
2938//	out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
2939func p384FromBytes(out1 *[6]uint64, arg1 *[48]uint8) {
2940	x1 := (uint64(arg1[47]) << 56)
2941	x2 := (uint64(arg1[46]) << 48)
2942	x3 := (uint64(arg1[45]) << 40)
2943	x4 := (uint64(arg1[44]) << 32)
2944	x5 := (uint64(arg1[43]) << 24)
2945	x6 := (uint64(arg1[42]) << 16)
2946	x7 := (uint64(arg1[41]) << 8)
2947	x8 := arg1[40]
2948	x9 := (uint64(arg1[39]) << 56)
2949	x10 := (uint64(arg1[38]) << 48)
2950	x11 := (uint64(arg1[37]) << 40)
2951	x12 := (uint64(arg1[36]) << 32)
2952	x13 := (uint64(arg1[35]) << 24)
2953	x14 := (uint64(arg1[34]) << 16)
2954	x15 := (uint64(arg1[33]) << 8)
2955	x16 := arg1[32]
2956	x17 := (uint64(arg1[31]) << 56)
2957	x18 := (uint64(arg1[30]) << 48)
2958	x19 := (uint64(arg1[29]) << 40)
2959	x20 := (uint64(arg1[28]) << 32)
2960	x21 := (uint64(arg1[27]) << 24)
2961	x22 := (uint64(arg1[26]) << 16)
2962	x23 := (uint64(arg1[25]) << 8)
2963	x24 := arg1[24]
2964	x25 := (uint64(arg1[23]) << 56)
2965	x26 := (uint64(arg1[22]) << 48)
2966	x27 := (uint64(arg1[21]) << 40)
2967	x28 := (uint64(arg1[20]) << 32)
2968	x29 := (uint64(arg1[19]) << 24)
2969	x30 := (uint64(arg1[18]) << 16)
2970	x31 := (uint64(arg1[17]) << 8)
2971	x32 := arg1[16]
2972	x33 := (uint64(arg1[15]) << 56)
2973	x34 := (uint64(arg1[14]) << 48)
2974	x35 := (uint64(arg1[13]) << 40)
2975	x36 := (uint64(arg1[12]) << 32)
2976	x37 := (uint64(arg1[11]) << 24)
2977	x38 := (uint64(arg1[10]) << 16)
2978	x39 := (uint64(arg1[9]) << 8)
2979	x40 := arg1[8]
2980	x41 := (uint64(arg1[7]) << 56)
2981	x42 := (uint64(arg1[6]) << 48)
2982	x43 := (uint64(arg1[5]) << 40)
2983	x44 := (uint64(arg1[4]) << 32)
2984	x45 := (uint64(arg1[3]) << 24)
2985	x46 := (uint64(arg1[2]) << 16)
2986	x47 := (uint64(arg1[1]) << 8)
2987	x48 := arg1[0]
2988	x49 := (x47 + uint64(x48))
2989	x50 := (x46 + x49)
2990	x51 := (x45 + x50)
2991	x52 := (x44 + x51)
2992	x53 := (x43 + x52)
2993	x54 := (x42 + x53)
2994	x55 := (x41 + x54)
2995	x56 := (x39 + uint64(x40))
2996	x57 := (x38 + x56)
2997	x58 := (x37 + x57)
2998	x59 := (x36 + x58)
2999	x60 := (x35 + x59)
3000	x61 := (x34 + x60)
3001	x62 := (x33 + x61)
3002	x63 := (x31 + uint64(x32))
3003	x64 := (x30 + x63)
3004	x65 := (x29 + x64)
3005	x66 := (x28 + x65)
3006	x67 := (x27 + x66)
3007	x68 := (x26 + x67)
3008	x69 := (x25 + x68)
3009	x70 := (x23 + uint64(x24))
3010	x71 := (x22 + x70)
3011	x72 := (x21 + x71)
3012	x73 := (x20 + x72)
3013	x74 := (x19 + x73)
3014	x75 := (x18 + x74)
3015	x76 := (x17 + x75)
3016	x77 := (x15 + uint64(x16))
3017	x78 := (x14 + x77)
3018	x79 := (x13 + x78)
3019	x80 := (x12 + x79)
3020	x81 := (x11 + x80)
3021	x82 := (x10 + x81)
3022	x83 := (x9 + x82)
3023	x84 := (x7 + uint64(x8))
3024	x85 := (x6 + x84)
3025	x86 := (x5 + x85)
3026	x87 := (x4 + x86)
3027	x88 := (x3 + x87)
3028	x89 := (x2 + x88)
3029	x90 := (x1 + x89)
3030	out1[0] = x55
3031	out1[1] = x62
3032	out1[2] = x69
3033	out1[3] = x76
3034	out1[4] = x83
3035	out1[5] = x90
3036}
3037