1#![doc = " fiat-crypto output postprocessed by fiat-constify: <https://github.com/rustcrypto/utils>"]
2#![doc = " Autogenerated: './unsaturated_solinas' --lang Rust --inline p521 64 9 '2^521 - 1'"]
3#![doc = " curve description: p521"]
4#![doc = " machine_wordsize = 64 (from \"64\")"]
5#![doc = " requested operations: (all)"]
6#![doc = " n = 9 (from \"9\")"]
7#![doc = " s-c = 2^521 - [(1, 1)] (from \"2^521 - 1\")"]
8#![doc = " tight_bounds_multiplier = 1 (from \"\")"]
9#![doc = ""]
10#![doc = " Computed values:"]
11#![doc = " carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1]"]
12#![doc = " eval z = z[0] + (z[1] << 58) + (z[2] << 116) + (z[3] << 174) + (z[4] << 232) + (z[5] << 0x122) + (z[6] << 0x15c) + (z[7] << 0x196) + (z[8] << 0x1d0)"]
13#![doc = " bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8) + (z[56] << 0x1c0) + (z[57] << 0x1c8) + (z[58] << 0x1d0) + (z[59] << 0x1d8) + (z[60] << 0x1e0) + (z[61] << 0x1e8) + (z[62] << 0x1f0) + (z[63] << 0x1f8) + (z[64] << 2^9) + (z[65] << 0x208)"]
14#![doc = " balance = [0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x7fffffffffffffe, 0x3fffffffffffffe]"]
15#![allow(unused_parens)]
16#![allow(non_camel_case_types)]
17#![allow(
18 clippy::identity_op,
19 clippy::unnecessary_cast,
20 dead_code,
21 rustdoc::broken_intra_doc_links,
22 unused_assignments,
23 unused_mut,
24 unused_variables
25)]
26pub type fiat_p521_u1 = u8;
27pub type fiat_p521_i1 = i8;
28pub type fiat_p521_u2 = u8;
29pub type fiat_p521_i2 = i8;
30pub type fiat_p521_loose_field_element = [u64; 9];
31pub type fiat_p521_tight_field_element = [u64; 9];
32#[doc = " The function fiat_p521_addcarryx_u58 is an addition with carry."]
33#[doc = ""]
34#[doc = " Postconditions:"]
35#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^58"]
36#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^58⌋"]
37#[doc = ""]
38#[doc = " Input Bounds:"]
39#[doc = " arg1: [0x0 ~> 0x1]"]
40#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"]
41#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"]
42#[doc = " Output Bounds:"]
43#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"]
44#[doc = " out2: [0x0 ~> 0x1]"]
45#[inline]
46pub const fn fiat_p521_addcarryx_u58(
47 arg1: fiat_p521_u1,
48 arg2: u64,
49 arg3: u64,
50) -> (u64, fiat_p521_u1) {
51 let mut out1: u64 = 0;
52 let mut out2: fiat_p521_u1 = 0;
53 let x1: u64 = (((arg1 as u64) + arg2) + arg3);
54 let x2: u64 = (x1 & 0x3ffffffffffffff);
55 let x3: fiat_p521_u1 = ((x1 >> 58) as fiat_p521_u1);
56 out1 = x2;
57 out2 = x3;
58 (out1, out2)
59}
60#[doc = " The function fiat_p521_subborrowx_u58 is a subtraction with borrow."]
61#[doc = ""]
62#[doc = " Postconditions:"]
63#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^58"]
64#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^58⌋"]
65#[doc = ""]
66#[doc = " Input Bounds:"]
67#[doc = " arg1: [0x0 ~> 0x1]"]
68#[doc = " arg2: [0x0 ~> 0x3ffffffffffffff]"]
69#[doc = " arg3: [0x0 ~> 0x3ffffffffffffff]"]
70#[doc = " Output Bounds:"]
71#[doc = " out1: [0x0 ~> 0x3ffffffffffffff]"]
72#[doc = " out2: [0x0 ~> 0x1]"]
73#[inline]
74pub const fn fiat_p521_subborrowx_u58(
75 arg1: fiat_p521_u1,
76 arg2: u64,
77 arg3: u64,
78) -> (u64, fiat_p521_u1) {
79 let mut out1: u64 = 0;
80 let mut out2: fiat_p521_u1 = 0;
81 let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
82 let x2: fiat_p521_i1 = ((x1 >> 58) as fiat_p521_i1);
83 let x3: u64 = (((x1 as i128) & (0x3ffffffffffffff as i128)) as u64);
84 out1 = x3;
85 out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1);
86 (out1, out2)
87}
88#[doc = " The function fiat_p521_addcarryx_u57 is an addition with carry."]
89#[doc = ""]
90#[doc = " Postconditions:"]
91#[doc = " out1 = (arg1 + arg2 + arg3) mod 2^57"]
92#[doc = " out2 = ⌊(arg1 + arg2 + arg3) / 2^57⌋"]
93#[doc = ""]
94#[doc = " Input Bounds:"]
95#[doc = " arg1: [0x0 ~> 0x1]"]
96#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"]
97#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"]
98#[doc = " Output Bounds:"]
99#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"]
100#[doc = " out2: [0x0 ~> 0x1]"]
101#[inline]
102pub const fn fiat_p521_addcarryx_u57(
103 arg1: fiat_p521_u1,
104 arg2: u64,
105 arg3: u64,
106) -> (u64, fiat_p521_u1) {
107 let mut out1: u64 = 0;
108 let mut out2: fiat_p521_u1 = 0;
109 let x1: u64 = (((arg1 as u64) + arg2) + arg3);
110 let x2: u64 = (x1 & 0x1ffffffffffffff);
111 let x3: fiat_p521_u1 = ((x1 >> 57) as fiat_p521_u1);
112 out1 = x2;
113 out2 = x3;
114 (out1, out2)
115}
116#[doc = " The function fiat_p521_subborrowx_u57 is a subtraction with borrow."]
117#[doc = ""]
118#[doc = " Postconditions:"]
119#[doc = " out1 = (-arg1 + arg2 + -arg3) mod 2^57"]
120#[doc = " out2 = -⌊(-arg1 + arg2 + -arg3) / 2^57⌋"]
121#[doc = ""]
122#[doc = " Input Bounds:"]
123#[doc = " arg1: [0x0 ~> 0x1]"]
124#[doc = " arg2: [0x0 ~> 0x1ffffffffffffff]"]
125#[doc = " arg3: [0x0 ~> 0x1ffffffffffffff]"]
126#[doc = " Output Bounds:"]
127#[doc = " out1: [0x0 ~> 0x1ffffffffffffff]"]
128#[doc = " out2: [0x0 ~> 0x1]"]
129#[inline]
130pub const fn fiat_p521_subborrowx_u57(
131 arg1: fiat_p521_u1,
132 arg2: u64,
133 arg3: u64,
134) -> (u64, fiat_p521_u1) {
135 let mut out1: u64 = 0;
136 let mut out2: fiat_p521_u1 = 0;
137 let x1: i64 = ((((((arg2 as i128) - (arg1 as i128)) as i64) as i128) - (arg3 as i128)) as i64);
138 let x2: fiat_p521_i1 = ((x1 >> 57) as fiat_p521_i1);
139 let x3: u64 = (((x1 as i128) & (0x1ffffffffffffff as i128)) as u64);
140 out1 = x3;
141 out2 = (((0x0 as fiat_p521_i2) - (x2 as fiat_p521_i2)) as fiat_p521_u1);
142 (out1, out2)
143}
144#[doc = " The function fiat_p521_cmovznz_u64 is a single-word conditional move."]
145#[doc = ""]
146#[doc = " Postconditions:"]
147#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"]
148#[doc = ""]
149#[doc = " Input Bounds:"]
150#[doc = " arg1: [0x0 ~> 0x1]"]
151#[doc = " arg2: [0x0 ~> 0xffffffffffffffff]"]
152#[doc = " arg3: [0x0 ~> 0xffffffffffffffff]"]
153#[doc = " Output Bounds:"]
154#[doc = " out1: [0x0 ~> 0xffffffffffffffff]"]
155#[inline]
156pub const fn fiat_p521_cmovznz_u64(arg1: fiat_p521_u1, arg2: u64, arg3: u64) -> u64 {
157 let mut out1: u64 = 0;
158 let x1: fiat_p521_u1 = (!(!arg1));
159 let x2: u64 = ((((((0x0 as fiat_p521_i2) - (x1 as fiat_p521_i2)) as fiat_p521_i1) as i128)
160 & (0xffffffffffffffff as i128)) as u64);
161 let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
162 out1 = x3;
163 out1
164}
165#[doc = " The function fiat_p521_carry_mul multiplies two field elements and reduces the result."]
166#[doc = ""]
167#[doc = " Postconditions:"]
168#[doc = " eval out1 mod m = (eval arg1 * eval arg2) mod m"]
169#[doc = ""]
170#[inline]
171pub const fn fiat_p521_carry_mul(
172 arg1: &fiat_p521_loose_field_element,
173 arg2: &fiat_p521_loose_field_element,
174) -> fiat_p521_tight_field_element {
175 let mut out1: fiat_p521_tight_field_element = [0; 9];
176 let x1: u128 = (((arg1[8]) as u128) * (((arg2[8]) * 0x2) as u128));
177 let x2: u128 = (((arg1[8]) as u128) * (((arg2[7]) * 0x2) as u128));
178 let x3: u128 = (((arg1[8]) as u128) * (((arg2[6]) * 0x2) as u128));
179 let x4: u128 = (((arg1[8]) as u128) * (((arg2[5]) * 0x2) as u128));
180 let x5: u128 = (((arg1[8]) as u128) * (((arg2[4]) * 0x2) as u128));
181 let x6: u128 = (((arg1[8]) as u128) * (((arg2[3]) * 0x2) as u128));
182 let x7: u128 = (((arg1[8]) as u128) * (((arg2[2]) * 0x2) as u128));
183 let x8: u128 = (((arg1[8]) as u128) * (((arg2[1]) * 0x2) as u128));
184 let x9: u128 = (((arg1[7]) as u128) * (((arg2[8]) * 0x2) as u128));
185 let x10: u128 = (((arg1[7]) as u128) * (((arg2[7]) * 0x2) as u128));
186 let x11: u128 = (((arg1[7]) as u128) * (((arg2[6]) * 0x2) as u128));
187 let x12: u128 = (((arg1[7]) as u128) * (((arg2[5]) * 0x2) as u128));
188 let x13: u128 = (((arg1[7]) as u128) * (((arg2[4]) * 0x2) as u128));
189 let x14: u128 = (((arg1[7]) as u128) * (((arg2[3]) * 0x2) as u128));
190 let x15: u128 = (((arg1[7]) as u128) * (((arg2[2]) * 0x2) as u128));
191 let x16: u128 = (((arg1[6]) as u128) * (((arg2[8]) * 0x2) as u128));
192 let x17: u128 = (((arg1[6]) as u128) * (((arg2[7]) * 0x2) as u128));
193 let x18: u128 = (((arg1[6]) as u128) * (((arg2[6]) * 0x2) as u128));
194 let x19: u128 = (((arg1[6]) as u128) * (((arg2[5]) * 0x2) as u128));
195 let x20: u128 = (((arg1[6]) as u128) * (((arg2[4]) * 0x2) as u128));
196 let x21: u128 = (((arg1[6]) as u128) * (((arg2[3]) * 0x2) as u128));
197 let x22: u128 = (((arg1[5]) as u128) * (((arg2[8]) * 0x2) as u128));
198 let x23: u128 = (((arg1[5]) as u128) * (((arg2[7]) * 0x2) as u128));
199 let x24: u128 = (((arg1[5]) as u128) * (((arg2[6]) * 0x2) as u128));
200 let x25: u128 = (((arg1[5]) as u128) * (((arg2[5]) * 0x2) as u128));
201 let x26: u128 = (((arg1[5]) as u128) * (((arg2[4]) * 0x2) as u128));
202 let x27: u128 = (((arg1[4]) as u128) * (((arg2[8]) * 0x2) as u128));
203 let x28: u128 = (((arg1[4]) as u128) * (((arg2[7]) * 0x2) as u128));
204 let x29: u128 = (((arg1[4]) as u128) * (((arg2[6]) * 0x2) as u128));
205 let x30: u128 = (((arg1[4]) as u128) * (((arg2[5]) * 0x2) as u128));
206 let x31: u128 = (((arg1[3]) as u128) * (((arg2[8]) * 0x2) as u128));
207 let x32: u128 = (((arg1[3]) as u128) * (((arg2[7]) * 0x2) as u128));
208 let x33: u128 = (((arg1[3]) as u128) * (((arg2[6]) * 0x2) as u128));
209 let x34: u128 = (((arg1[2]) as u128) * (((arg2[8]) * 0x2) as u128));
210 let x35: u128 = (((arg1[2]) as u128) * (((arg2[7]) * 0x2) as u128));
211 let x36: u128 = (((arg1[1]) as u128) * (((arg2[8]) * 0x2) as u128));
212 let x37: u128 = (((arg1[8]) as u128) * ((arg2[0]) as u128));
213 let x38: u128 = (((arg1[7]) as u128) * ((arg2[1]) as u128));
214 let x39: u128 = (((arg1[7]) as u128) * ((arg2[0]) as u128));
215 let x40: u128 = (((arg1[6]) as u128) * ((arg2[2]) as u128));
216 let x41: u128 = (((arg1[6]) as u128) * ((arg2[1]) as u128));
217 let x42: u128 = (((arg1[6]) as u128) * ((arg2[0]) as u128));
218 let x43: u128 = (((arg1[5]) as u128) * ((arg2[3]) as u128));
219 let x44: u128 = (((arg1[5]) as u128) * ((arg2[2]) as u128));
220 let x45: u128 = (((arg1[5]) as u128) * ((arg2[1]) as u128));
221 let x46: u128 = (((arg1[5]) as u128) * ((arg2[0]) as u128));
222 let x47: u128 = (((arg1[4]) as u128) * ((arg2[4]) as u128));
223 let x48: u128 = (((arg1[4]) as u128) * ((arg2[3]) as u128));
224 let x49: u128 = (((arg1[4]) as u128) * ((arg2[2]) as u128));
225 let x50: u128 = (((arg1[4]) as u128) * ((arg2[1]) as u128));
226 let x51: u128 = (((arg1[4]) as u128) * ((arg2[0]) as u128));
227 let x52: u128 = (((arg1[3]) as u128) * ((arg2[5]) as u128));
228 let x53: u128 = (((arg1[3]) as u128) * ((arg2[4]) as u128));
229 let x54: u128 = (((arg1[3]) as u128) * ((arg2[3]) as u128));
230 let x55: u128 = (((arg1[3]) as u128) * ((arg2[2]) as u128));
231 let x56: u128 = (((arg1[3]) as u128) * ((arg2[1]) as u128));
232 let x57: u128 = (((arg1[3]) as u128) * ((arg2[0]) as u128));
233 let x58: u128 = (((arg1[2]) as u128) * ((arg2[6]) as u128));
234 let x59: u128 = (((arg1[2]) as u128) * ((arg2[5]) as u128));
235 let x60: u128 = (((arg1[2]) as u128) * ((arg2[4]) as u128));
236 let x61: u128 = (((arg1[2]) as u128) * ((arg2[3]) as u128));
237 let x62: u128 = (((arg1[2]) as u128) * ((arg2[2]) as u128));
238 let x63: u128 = (((arg1[2]) as u128) * ((arg2[1]) as u128));
239 let x64: u128 = (((arg1[2]) as u128) * ((arg2[0]) as u128));
240 let x65: u128 = (((arg1[1]) as u128) * ((arg2[7]) as u128));
241 let x66: u128 = (((arg1[1]) as u128) * ((arg2[6]) as u128));
242 let x67: u128 = (((arg1[1]) as u128) * ((arg2[5]) as u128));
243 let x68: u128 = (((arg1[1]) as u128) * ((arg2[4]) as u128));
244 let x69: u128 = (((arg1[1]) as u128) * ((arg2[3]) as u128));
245 let x70: u128 = (((arg1[1]) as u128) * ((arg2[2]) as u128));
246 let x71: u128 = (((arg1[1]) as u128) * ((arg2[1]) as u128));
247 let x72: u128 = (((arg1[1]) as u128) * ((arg2[0]) as u128));
248 let x73: u128 = (((arg1[0]) as u128) * ((arg2[8]) as u128));
249 let x74: u128 = (((arg1[0]) as u128) * ((arg2[7]) as u128));
250 let x75: u128 = (((arg1[0]) as u128) * ((arg2[6]) as u128));
251 let x76: u128 = (((arg1[0]) as u128) * ((arg2[5]) as u128));
252 let x77: u128 = (((arg1[0]) as u128) * ((arg2[4]) as u128));
253 let x78: u128 = (((arg1[0]) as u128) * ((arg2[3]) as u128));
254 let x79: u128 = (((arg1[0]) as u128) * ((arg2[2]) as u128));
255 let x80: u128 = (((arg1[0]) as u128) * ((arg2[1]) as u128));
256 let x81: u128 = (((arg1[0]) as u128) * ((arg2[0]) as u128));
257 let x82: u128 = (x81 + (x36 + (x35 + (x33 + (x30 + (x26 + (x21 + (x15 + x8))))))));
258 let x83: u128 = (x82 >> 58);
259 let x84: u64 = ((x82 & (0x3ffffffffffffff as u128)) as u64);
260 let x85: u128 = (x73 + (x65 + (x58 + (x52 + (x47 + (x43 + (x40 + (x38 + x37))))))));
261 let x86: u128 = (x74 + (x66 + (x59 + (x53 + (x48 + (x44 + (x41 + (x39 + x1))))))));
262 let x87: u128 = (x75 + (x67 + (x60 + (x54 + (x49 + (x45 + (x42 + (x9 + x2))))))));
263 let x88: u128 = (x76 + (x68 + (x61 + (x55 + (x50 + (x46 + (x16 + (x10 + x3))))))));
264 let x89: u128 = (x77 + (x69 + (x62 + (x56 + (x51 + (x22 + (x17 + (x11 + x4))))))));
265 let x90: u128 = (x78 + (x70 + (x63 + (x57 + (x27 + (x23 + (x18 + (x12 + x5))))))));
266 let x91: u128 = (x79 + (x71 + (x64 + (x31 + (x28 + (x24 + (x19 + (x13 + x6))))))));
267 let x92: u128 = (x80 + (x72 + (x34 + (x32 + (x29 + (x25 + (x20 + (x14 + x7))))))));
268 let x93: u128 = (x83 + x92);
269 let x94: u128 = (x93 >> 58);
270 let x95: u64 = ((x93 & (0x3ffffffffffffff as u128)) as u64);
271 let x96: u128 = (x94 + x91);
272 let x97: u128 = (x96 >> 58);
273 let x98: u64 = ((x96 & (0x3ffffffffffffff as u128)) as u64);
274 let x99: u128 = (x97 + x90);
275 let x100: u128 = (x99 >> 58);
276 let x101: u64 = ((x99 & (0x3ffffffffffffff as u128)) as u64);
277 let x102: u128 = (x100 + x89);
278 let x103: u128 = (x102 >> 58);
279 let x104: u64 = ((x102 & (0x3ffffffffffffff as u128)) as u64);
280 let x105: u128 = (x103 + x88);
281 let x106: u128 = (x105 >> 58);
282 let x107: u64 = ((x105 & (0x3ffffffffffffff as u128)) as u64);
283 let x108: u128 = (x106 + x87);
284 let x109: u128 = (x108 >> 58);
285 let x110: u64 = ((x108 & (0x3ffffffffffffff as u128)) as u64);
286 let x111: u128 = (x109 + x86);
287 let x112: u128 = (x111 >> 58);
288 let x113: u64 = ((x111 & (0x3ffffffffffffff as u128)) as u64);
289 let x114: u128 = (x112 + x85);
290 let x115: u128 = (x114 >> 57);
291 let x116: u64 = ((x114 & (0x1ffffffffffffff as u128)) as u64);
292 let x117: u128 = ((x84 as u128) + x115);
293 let x118: u64 = ((x117 >> 58) as u64);
294 let x119: u64 = ((x117 & (0x3ffffffffffffff as u128)) as u64);
295 let x120: u64 = (x118 + x95);
296 let x121: fiat_p521_u1 = ((x120 >> 58) as fiat_p521_u1);
297 let x122: u64 = (x120 & 0x3ffffffffffffff);
298 let x123: u64 = ((x121 as u64) + x98);
299 out1[0] = x119;
300 out1[1] = x122;
301 out1[2] = x123;
302 out1[3] = x101;
303 out1[4] = x104;
304 out1[5] = x107;
305 out1[6] = x110;
306 out1[7] = x113;
307 out1[8] = x116;
308 out1
309}
310#[doc = " The function fiat_p521_carry_square squares a field element and reduces the result."]
311#[doc = ""]
312#[doc = " Postconditions:"]
313#[doc = " eval out1 mod m = (eval arg1 * eval arg1) mod m"]
314#[doc = ""]
315#[inline]
316pub const fn fiat_p521_carry_square(
317 arg1: &fiat_p521_loose_field_element,
318) -> fiat_p521_tight_field_element {
319 let mut out1: fiat_p521_tight_field_element = [0; 9];
320 let x1: u64 = (arg1[8]);
321 let x2: u64 = (x1 * 0x2);
322 let x3: u64 = ((arg1[8]) * 0x2);
323 let x4: u64 = (arg1[7]);
324 let x5: u64 = (x4 * 0x2);
325 let x6: u64 = ((arg1[7]) * 0x2);
326 let x7: u64 = (arg1[6]);
327 let x8: u64 = (x7 * 0x2);
328 let x9: u64 = ((arg1[6]) * 0x2);
329 let x10: u64 = (arg1[5]);
330 let x11: u64 = (x10 * 0x2);
331 let x12: u64 = ((arg1[5]) * 0x2);
332 let x13: u64 = ((arg1[4]) * 0x2);
333 let x14: u64 = ((arg1[3]) * 0x2);
334 let x15: u64 = ((arg1[2]) * 0x2);
335 let x16: u64 = ((arg1[1]) * 0x2);
336 let x17: u128 = (((arg1[8]) as u128) * ((x1 * 0x2) as u128));
337 let x18: u128 = (((arg1[7]) as u128) * ((x2 * 0x2) as u128));
338 let x19: u128 = (((arg1[7]) as u128) * ((x4 * 0x2) as u128));
339 let x20: u128 = (((arg1[6]) as u128) * ((x2 * 0x2) as u128));
340 let x21: u128 = (((arg1[6]) as u128) * ((x5 * 0x2) as u128));
341 let x22: u128 = (((arg1[6]) as u128) * ((x7 * 0x2) as u128));
342 let x23: u128 = (((arg1[5]) as u128) * ((x2 * 0x2) as u128));
343 let x24: u128 = (((arg1[5]) as u128) * ((x5 * 0x2) as u128));
344 let x25: u128 = (((arg1[5]) as u128) * ((x8 * 0x2) as u128));
345 let x26: u128 = (((arg1[5]) as u128) * ((x10 * 0x2) as u128));
346 let x27: u128 = (((arg1[4]) as u128) * ((x2 * 0x2) as u128));
347 let x28: u128 = (((arg1[4]) as u128) * ((x5 * 0x2) as u128));
348 let x29: u128 = (((arg1[4]) as u128) * ((x8 * 0x2) as u128));
349 let x30: u128 = (((arg1[4]) as u128) * ((x11 * 0x2) as u128));
350 let x31: u128 = (((arg1[4]) as u128) * ((arg1[4]) as u128));
351 let x32: u128 = (((arg1[3]) as u128) * ((x2 * 0x2) as u128));
352 let x33: u128 = (((arg1[3]) as u128) * ((x5 * 0x2) as u128));
353 let x34: u128 = (((arg1[3]) as u128) * ((x8 * 0x2) as u128));
354 let x35: u128 = (((arg1[3]) as u128) * (x12 as u128));
355 let x36: u128 = (((arg1[3]) as u128) * (x13 as u128));
356 let x37: u128 = (((arg1[3]) as u128) * ((arg1[3]) as u128));
357 let x38: u128 = (((arg1[2]) as u128) * ((x2 * 0x2) as u128));
358 let x39: u128 = (((arg1[2]) as u128) * ((x5 * 0x2) as u128));
359 let x40: u128 = (((arg1[2]) as u128) * (x9 as u128));
360 let x41: u128 = (((arg1[2]) as u128) * (x12 as u128));
361 let x42: u128 = (((arg1[2]) as u128) * (x13 as u128));
362 let x43: u128 = (((arg1[2]) as u128) * (x14 as u128));
363 let x44: u128 = (((arg1[2]) as u128) * ((arg1[2]) as u128));
364 let x45: u128 = (((arg1[1]) as u128) * ((x2 * 0x2) as u128));
365 let x46: u128 = (((arg1[1]) as u128) * (x6 as u128));
366 let x47: u128 = (((arg1[1]) as u128) * (x9 as u128));
367 let x48: u128 = (((arg1[1]) as u128) * (x12 as u128));
368 let x49: u128 = (((arg1[1]) as u128) * (x13 as u128));
369 let x50: u128 = (((arg1[1]) as u128) * (x14 as u128));
370 let x51: u128 = (((arg1[1]) as u128) * (x15 as u128));
371 let x52: u128 = (((arg1[1]) as u128) * ((arg1[1]) as u128));
372 let x53: u128 = (((arg1[0]) as u128) * (x3 as u128));
373 let x54: u128 = (((arg1[0]) as u128) * (x6 as u128));
374 let x55: u128 = (((arg1[0]) as u128) * (x9 as u128));
375 let x56: u128 = (((arg1[0]) as u128) * (x12 as u128));
376 let x57: u128 = (((arg1[0]) as u128) * (x13 as u128));
377 let x58: u128 = (((arg1[0]) as u128) * (x14 as u128));
378 let x59: u128 = (((arg1[0]) as u128) * (x15 as u128));
379 let x60: u128 = (((arg1[0]) as u128) * (x16 as u128));
380 let x61: u128 = (((arg1[0]) as u128) * ((arg1[0]) as u128));
381 let x62: u128 = (x61 + (x45 + (x39 + (x34 + x30))));
382 let x63: u128 = (x62 >> 58);
383 let x64: u64 = ((x62 & (0x3ffffffffffffff as u128)) as u64);
384 let x65: u128 = (x53 + (x46 + (x40 + (x35 + x31))));
385 let x66: u128 = (x54 + (x47 + (x41 + (x36 + x17))));
386 let x67: u128 = (x55 + (x48 + (x42 + (x37 + x18))));
387 let x68: u128 = (x56 + (x49 + (x43 + (x20 + x19))));
388 let x69: u128 = (x57 + (x50 + (x44 + (x23 + x21))));
389 let x70: u128 = (x58 + (x51 + (x27 + (x24 + x22))));
390 let x71: u128 = (x59 + (x52 + (x32 + (x28 + x25))));
391 let x72: u128 = (x60 + (x38 + (x33 + (x29 + x26))));
392 let x73: u128 = (x63 + x72);
393 let x74: u128 = (x73 >> 58);
394 let x75: u64 = ((x73 & (0x3ffffffffffffff as u128)) as u64);
395 let x76: u128 = (x74 + x71);
396 let x77: u128 = (x76 >> 58);
397 let x78: u64 = ((x76 & (0x3ffffffffffffff as u128)) as u64);
398 let x79: u128 = (x77 + x70);
399 let x80: u128 = (x79 >> 58);
400 let x81: u64 = ((x79 & (0x3ffffffffffffff as u128)) as u64);
401 let x82: u128 = (x80 + x69);
402 let x83: u128 = (x82 >> 58);
403 let x84: u64 = ((x82 & (0x3ffffffffffffff as u128)) as u64);
404 let x85: u128 = (x83 + x68);
405 let x86: u128 = (x85 >> 58);
406 let x87: u64 = ((x85 & (0x3ffffffffffffff as u128)) as u64);
407 let x88: u128 = (x86 + x67);
408 let x89: u128 = (x88 >> 58);
409 let x90: u64 = ((x88 & (0x3ffffffffffffff as u128)) as u64);
410 let x91: u128 = (x89 + x66);
411 let x92: u128 = (x91 >> 58);
412 let x93: u64 = ((x91 & (0x3ffffffffffffff as u128)) as u64);
413 let x94: u128 = (x92 + x65);
414 let x95: u128 = (x94 >> 57);
415 let x96: u64 = ((x94 & (0x1ffffffffffffff as u128)) as u64);
416 let x97: u128 = ((x64 as u128) + x95);
417 let x98: u64 = ((x97 >> 58) as u64);
418 let x99: u64 = ((x97 & (0x3ffffffffffffff as u128)) as u64);
419 let x100: u64 = (x98 + x75);
420 let x101: fiat_p521_u1 = ((x100 >> 58) as fiat_p521_u1);
421 let x102: u64 = (x100 & 0x3ffffffffffffff);
422 let x103: u64 = ((x101 as u64) + x78);
423 out1[0] = x99;
424 out1[1] = x102;
425 out1[2] = x103;
426 out1[3] = x81;
427 out1[4] = x84;
428 out1[5] = x87;
429 out1[6] = x90;
430 out1[7] = x93;
431 out1[8] = x96;
432 out1
433}
434#[doc = " The function fiat_p521_carry reduces a field element."]
435#[doc = ""]
436#[doc = " Postconditions:"]
437#[doc = " eval out1 mod m = eval arg1 mod m"]
438#[doc = ""]
439#[inline]
440pub const fn fiat_p521_carry(
441 arg1: &fiat_p521_loose_field_element,
442) -> fiat_p521_tight_field_element {
443 let mut out1: fiat_p521_tight_field_element = [0; 9];
444 let x1: u64 = (arg1[0]);
445 let x2: u64 = ((x1 >> 58) + (arg1[1]));
446 let x3: u64 = ((x2 >> 58) + (arg1[2]));
447 let x4: u64 = ((x3 >> 58) + (arg1[3]));
448 let x5: u64 = ((x4 >> 58) + (arg1[4]));
449 let x6: u64 = ((x5 >> 58) + (arg1[5]));
450 let x7: u64 = ((x6 >> 58) + (arg1[6]));
451 let x8: u64 = ((x7 >> 58) + (arg1[7]));
452 let x9: u64 = ((x8 >> 58) + (arg1[8]));
453 let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57));
454 let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
455 let x12: u64 = (x10 & 0x3ffffffffffffff);
456 let x13: u64 = (x11 & 0x3ffffffffffffff);
457 let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
458 let x15: u64 = (x4 & 0x3ffffffffffffff);
459 let x16: u64 = (x5 & 0x3ffffffffffffff);
460 let x17: u64 = (x6 & 0x3ffffffffffffff);
461 let x18: u64 = (x7 & 0x3ffffffffffffff);
462 let x19: u64 = (x8 & 0x3ffffffffffffff);
463 let x20: u64 = (x9 & 0x1ffffffffffffff);
464 out1[0] = x12;
465 out1[1] = x13;
466 out1[2] = x14;
467 out1[3] = x15;
468 out1[4] = x16;
469 out1[5] = x17;
470 out1[6] = x18;
471 out1[7] = x19;
472 out1[8] = x20;
473 out1
474}
475#[doc = " The function fiat_p521_add adds two field elements."]
476#[doc = ""]
477#[doc = " Postconditions:"]
478#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"]
479#[doc = ""]
480#[inline]
481pub const fn fiat_p521_add(
482 arg1: &fiat_p521_tight_field_element,
483 arg2: &fiat_p521_tight_field_element,
484) -> fiat_p521_loose_field_element {
485 let mut out1: fiat_p521_loose_field_element = [0; 9];
486 let x1: u64 = ((arg1[0]) + (arg2[0]));
487 let x2: u64 = ((arg1[1]) + (arg2[1]));
488 let x3: u64 = ((arg1[2]) + (arg2[2]));
489 let x4: u64 = ((arg1[3]) + (arg2[3]));
490 let x5: u64 = ((arg1[4]) + (arg2[4]));
491 let x6: u64 = ((arg1[5]) + (arg2[5]));
492 let x7: u64 = ((arg1[6]) + (arg2[6]));
493 let x8: u64 = ((arg1[7]) + (arg2[7]));
494 let x9: u64 = ((arg1[8]) + (arg2[8]));
495 out1[0] = x1;
496 out1[1] = x2;
497 out1[2] = x3;
498 out1[3] = x4;
499 out1[4] = x5;
500 out1[5] = x6;
501 out1[6] = x7;
502 out1[7] = x8;
503 out1[8] = x9;
504 out1
505}
506#[doc = " The function fiat_p521_sub subtracts two field elements."]
507#[doc = ""]
508#[doc = " Postconditions:"]
509#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"]
510#[doc = ""]
511#[inline]
512pub const fn fiat_p521_sub(
513 arg1: &fiat_p521_tight_field_element,
514 arg2: &fiat_p521_tight_field_element,
515) -> fiat_p521_loose_field_element {
516 let mut out1: fiat_p521_loose_field_element = [0; 9];
517 let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0]));
518 let x2: u64 = ((0x7fffffffffffffe + (arg1[1])) - (arg2[1]));
519 let x3: u64 = ((0x7fffffffffffffe + (arg1[2])) - (arg2[2]));
520 let x4: u64 = ((0x7fffffffffffffe + (arg1[3])) - (arg2[3]));
521 let x5: u64 = ((0x7fffffffffffffe + (arg1[4])) - (arg2[4]));
522 let x6: u64 = ((0x7fffffffffffffe + (arg1[5])) - (arg2[5]));
523 let x7: u64 = ((0x7fffffffffffffe + (arg1[6])) - (arg2[6]));
524 let x8: u64 = ((0x7fffffffffffffe + (arg1[7])) - (arg2[7]));
525 let x9: u64 = ((0x3fffffffffffffe + (arg1[8])) - (arg2[8]));
526 out1[0] = x1;
527 out1[1] = x2;
528 out1[2] = x3;
529 out1[3] = x4;
530 out1[4] = x5;
531 out1[5] = x6;
532 out1[6] = x7;
533 out1[7] = x8;
534 out1[8] = x9;
535 out1
536}
537#[doc = " The function fiat_p521_opp negates a field element."]
538#[doc = ""]
539#[doc = " Postconditions:"]
540#[doc = " eval out1 mod m = -eval arg1 mod m"]
541#[doc = ""]
542#[inline]
543pub const fn fiat_p521_opp(arg1: &fiat_p521_tight_field_element) -> fiat_p521_loose_field_element {
544 let mut out1: fiat_p521_loose_field_element = [0; 9];
545 let x1: u64 = (0x7fffffffffffffe - (arg1[0]));
546 let x2: u64 = (0x7fffffffffffffe - (arg1[1]));
547 let x3: u64 = (0x7fffffffffffffe - (arg1[2]));
548 let x4: u64 = (0x7fffffffffffffe - (arg1[3]));
549 let x5: u64 = (0x7fffffffffffffe - (arg1[4]));
550 let x6: u64 = (0x7fffffffffffffe - (arg1[5]));
551 let x7: u64 = (0x7fffffffffffffe - (arg1[6]));
552 let x8: u64 = (0x7fffffffffffffe - (arg1[7]));
553 let x9: u64 = (0x3fffffffffffffe - (arg1[8]));
554 out1[0] = x1;
555 out1[1] = x2;
556 out1[2] = x3;
557 out1[3] = x4;
558 out1[4] = x5;
559 out1[5] = x6;
560 out1[6] = x7;
561 out1[7] = x8;
562 out1[8] = x9;
563 out1
564}
565#[doc = " The function fiat_p521_carry_add adds two field elements."]
566#[doc = ""]
567#[doc = " Postconditions:"]
568#[doc = " eval out1 mod m = (eval arg1 + eval arg2) mod m"]
569#[doc = ""]
570#[inline]
571pub const fn fiat_p521_carry_add(
572 arg1: &fiat_p521_tight_field_element,
573 arg2: &fiat_p521_tight_field_element,
574) -> fiat_p521_tight_field_element {
575 let mut out1: fiat_p521_tight_field_element = [0; 9];
576 let x1: u64 = ((arg1[0]) + (arg2[0]));
577 let x2: u64 = ((x1 >> 58) + ((arg1[1]) + (arg2[1])));
578 let x3: u64 = ((x2 >> 58) + ((arg1[2]) + (arg2[2])));
579 let x4: u64 = ((x3 >> 58) + ((arg1[3]) + (arg2[3])));
580 let x5: u64 = ((x4 >> 58) + ((arg1[4]) + (arg2[4])));
581 let x6: u64 = ((x5 >> 58) + ((arg1[5]) + (arg2[5])));
582 let x7: u64 = ((x6 >> 58) + ((arg1[6]) + (arg2[6])));
583 let x8: u64 = ((x7 >> 58) + ((arg1[7]) + (arg2[7])));
584 let x9: u64 = ((x8 >> 58) + ((arg1[8]) + (arg2[8])));
585 let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57));
586 let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
587 let x12: u64 = (x10 & 0x3ffffffffffffff);
588 let x13: u64 = (x11 & 0x3ffffffffffffff);
589 let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
590 let x15: u64 = (x4 & 0x3ffffffffffffff);
591 let x16: u64 = (x5 & 0x3ffffffffffffff);
592 let x17: u64 = (x6 & 0x3ffffffffffffff);
593 let x18: u64 = (x7 & 0x3ffffffffffffff);
594 let x19: u64 = (x8 & 0x3ffffffffffffff);
595 let x20: u64 = (x9 & 0x1ffffffffffffff);
596 out1[0] = x12;
597 out1[1] = x13;
598 out1[2] = x14;
599 out1[3] = x15;
600 out1[4] = x16;
601 out1[5] = x17;
602 out1[6] = x18;
603 out1[7] = x19;
604 out1[8] = x20;
605 out1
606}
607#[doc = " The function fiat_p521_carry_sub subtracts two field elements."]
608#[doc = ""]
609#[doc = " Postconditions:"]
610#[doc = " eval out1 mod m = (eval arg1 - eval arg2) mod m"]
611#[doc = ""]
612#[inline]
613pub const fn fiat_p521_carry_sub(
614 arg1: &fiat_p521_tight_field_element,
615 arg2: &fiat_p521_tight_field_element,
616) -> fiat_p521_tight_field_element {
617 let mut out1: fiat_p521_tight_field_element = [0; 9];
618 let x1: u64 = ((0x7fffffffffffffe + (arg1[0])) - (arg2[0]));
619 let x2: u64 = ((x1 >> 58) + ((0x7fffffffffffffe + (arg1[1])) - (arg2[1])));
620 let x3: u64 = ((x2 >> 58) + ((0x7fffffffffffffe + (arg1[2])) - (arg2[2])));
621 let x4: u64 = ((x3 >> 58) + ((0x7fffffffffffffe + (arg1[3])) - (arg2[3])));
622 let x5: u64 = ((x4 >> 58) + ((0x7fffffffffffffe + (arg1[4])) - (arg2[4])));
623 let x6: u64 = ((x5 >> 58) + ((0x7fffffffffffffe + (arg1[5])) - (arg2[5])));
624 let x7: u64 = ((x6 >> 58) + ((0x7fffffffffffffe + (arg1[6])) - (arg2[6])));
625 let x8: u64 = ((x7 >> 58) + ((0x7fffffffffffffe + (arg1[7])) - (arg2[7])));
626 let x9: u64 = ((x8 >> 58) + ((0x3fffffffffffffe + (arg1[8])) - (arg2[8])));
627 let x10: u64 = ((x1 & 0x3ffffffffffffff) + (x9 >> 57));
628 let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
629 let x12: u64 = (x10 & 0x3ffffffffffffff);
630 let x13: u64 = (x11 & 0x3ffffffffffffff);
631 let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
632 let x15: u64 = (x4 & 0x3ffffffffffffff);
633 let x16: u64 = (x5 & 0x3ffffffffffffff);
634 let x17: u64 = (x6 & 0x3ffffffffffffff);
635 let x18: u64 = (x7 & 0x3ffffffffffffff);
636 let x19: u64 = (x8 & 0x3ffffffffffffff);
637 let x20: u64 = (x9 & 0x1ffffffffffffff);
638 out1[0] = x12;
639 out1[1] = x13;
640 out1[2] = x14;
641 out1[3] = x15;
642 out1[4] = x16;
643 out1[5] = x17;
644 out1[6] = x18;
645 out1[7] = x19;
646 out1[8] = x20;
647 out1
648}
649#[doc = " The function fiat_p521_carry_opp negates a field element."]
650#[doc = ""]
651#[doc = " Postconditions:"]
652#[doc = " eval out1 mod m = -eval arg1 mod m"]
653#[doc = ""]
654#[inline]
655pub const fn fiat_p521_carry_opp(
656 arg1: &fiat_p521_tight_field_element,
657) -> fiat_p521_tight_field_element {
658 let mut out1: fiat_p521_tight_field_element = [0; 9];
659 let x1: u64 = (0x7fffffffffffffe - (arg1[0]));
660 let x2: u64 = ((((x1 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[1])));
661 let x3: u64 = ((((x2 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[2])));
662 let x4: u64 = ((((x3 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[3])));
663 let x5: u64 = ((((x4 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[4])));
664 let x6: u64 = ((((x5 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[5])));
665 let x7: u64 = ((((x6 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[6])));
666 let x8: u64 = ((((x7 >> 58) as fiat_p521_u1) as u64) + (0x7fffffffffffffe - (arg1[7])));
667 let x9: u64 = ((((x8 >> 58) as fiat_p521_u1) as u64) + (0x3fffffffffffffe - (arg1[8])));
668 let x10: u64 = ((x1 & 0x3ffffffffffffff) + (((x9 >> 57) as fiat_p521_u1) as u64));
669 let x11: u64 = ((((x10 >> 58) as fiat_p521_u1) as u64) + (x2 & 0x3ffffffffffffff));
670 let x12: u64 = (x10 & 0x3ffffffffffffff);
671 let x13: u64 = (x11 & 0x3ffffffffffffff);
672 let x14: u64 = ((((x11 >> 58) as fiat_p521_u1) as u64) + (x3 & 0x3ffffffffffffff));
673 let x15: u64 = (x4 & 0x3ffffffffffffff);
674 let x16: u64 = (x5 & 0x3ffffffffffffff);
675 let x17: u64 = (x6 & 0x3ffffffffffffff);
676 let x18: u64 = (x7 & 0x3ffffffffffffff);
677 let x19: u64 = (x8 & 0x3ffffffffffffff);
678 let x20: u64 = (x9 & 0x1ffffffffffffff);
679 out1[0] = x12;
680 out1[1] = x13;
681 out1[2] = x14;
682 out1[3] = x15;
683 out1[4] = x16;
684 out1[5] = x17;
685 out1[6] = x18;
686 out1[7] = x19;
687 out1[8] = x20;
688 out1
689}
690#[doc = " The function fiat_p521_relax is the identity function converting from tight field elements to loose field elements."]
691#[doc = ""]
692#[doc = " Postconditions:"]
693#[doc = " out1 = arg1"]
694#[doc = ""]
695#[inline]
696pub const fn fiat_p521_relax(
697 arg1: &fiat_p521_tight_field_element,
698) -> fiat_p521_loose_field_element {
699 let mut out1: fiat_p521_loose_field_element = [0; 9];
700 let x1: u64 = (arg1[0]);
701 let x2: u64 = (arg1[1]);
702 let x3: u64 = (arg1[2]);
703 let x4: u64 = (arg1[3]);
704 let x5: u64 = (arg1[4]);
705 let x6: u64 = (arg1[5]);
706 let x7: u64 = (arg1[6]);
707 let x8: u64 = (arg1[7]);
708 let x9: u64 = (arg1[8]);
709 out1[0] = x1;
710 out1[1] = x2;
711 out1[2] = x3;
712 out1[3] = x4;
713 out1[4] = x5;
714 out1[5] = x6;
715 out1[6] = x7;
716 out1[7] = x8;
717 out1[8] = x9;
718 out1
719}
720#[doc = " The function fiat_p521_selectznz is a multi-limb conditional select."]
721#[doc = ""]
722#[doc = " Postconditions:"]
723#[doc = " out1 = (if arg1 = 0 then arg2 else arg3)"]
724#[doc = ""]
725#[doc = " Input Bounds:"]
726#[doc = " arg1: [0x0 ~> 0x1]"]
727#[doc = " arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"]
728#[doc = " arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"]
729#[doc = " Output Bounds:"]
730#[doc = " out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]"]
731#[inline]
732pub const fn fiat_p521_selectznz(arg1: fiat_p521_u1, arg2: &[u64; 9], arg3: &[u64; 9]) -> [u64; 9] {
733 let mut out1: [u64; 9] = [0; 9];
734 let mut x1: u64 = 0;
735 let (x1) = fiat_p521_cmovznz_u64(arg1, (arg2[0]), (arg3[0]));
736 let mut x2: u64 = 0;
737 let (x2) = fiat_p521_cmovznz_u64(arg1, (arg2[1]), (arg3[1]));
738 let mut x3: u64 = 0;
739 let (x3) = fiat_p521_cmovznz_u64(arg1, (arg2[2]), (arg3[2]));
740 let mut x4: u64 = 0;
741 let (x4) = fiat_p521_cmovznz_u64(arg1, (arg2[3]), (arg3[3]));
742 let mut x5: u64 = 0;
743 let (x5) = fiat_p521_cmovznz_u64(arg1, (arg2[4]), (arg3[4]));
744 let mut x6: u64 = 0;
745 let (x6) = fiat_p521_cmovznz_u64(arg1, (arg2[5]), (arg3[5]));
746 let mut x7: u64 = 0;
747 let (x7) = fiat_p521_cmovznz_u64(arg1, (arg2[6]), (arg3[6]));
748 let mut x8: u64 = 0;
749 let (x8) = fiat_p521_cmovznz_u64(arg1, (arg2[7]), (arg3[7]));
750 let mut x9: u64 = 0;
751 let (x9) = fiat_p521_cmovznz_u64(arg1, (arg2[8]), (arg3[8]));
752 out1[0] = x1;
753 out1[1] = x2;
754 out1[2] = x3;
755 out1[3] = x4;
756 out1[4] = x5;
757 out1[5] = x6;
758 out1[6] = x7;
759 out1[7] = x8;
760 out1[8] = x9;
761 out1
762}
763#[doc = " The function fiat_p521_to_bytes serializes a field element to bytes in little-endian order."]
764#[doc = ""]
765#[doc = " Postconditions:"]
766#[doc = " out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..65]"]
767#[doc = ""]
768#[doc = " Output Bounds:"]
769#[doc = " out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"]
770#[inline]
771pub const fn fiat_p521_to_bytes(arg1: &fiat_p521_tight_field_element) -> [u8; 66] {
772 let mut out1: [u8; 66] = [0; 66];
773 let mut x1: u64 = 0;
774 let mut x2: fiat_p521_u1 = 0;
775 let (x1, x2) = fiat_p521_subborrowx_u58(0x0, (arg1[0]), 0x3ffffffffffffff);
776 let mut x3: u64 = 0;
777 let mut x4: fiat_p521_u1 = 0;
778 let (x3, x4) = fiat_p521_subborrowx_u58(x2, (arg1[1]), 0x3ffffffffffffff);
779 let mut x5: u64 = 0;
780 let mut x6: fiat_p521_u1 = 0;
781 let (x5, x6) = fiat_p521_subborrowx_u58(x4, (arg1[2]), 0x3ffffffffffffff);
782 let mut x7: u64 = 0;
783 let mut x8: fiat_p521_u1 = 0;
784 let (x7, x8) = fiat_p521_subborrowx_u58(x6, (arg1[3]), 0x3ffffffffffffff);
785 let mut x9: u64 = 0;
786 let mut x10: fiat_p521_u1 = 0;
787 let (x9, x10) = fiat_p521_subborrowx_u58(x8, (arg1[4]), 0x3ffffffffffffff);
788 let mut x11: u64 = 0;
789 let mut x12: fiat_p521_u1 = 0;
790 let (x11, x12) = fiat_p521_subborrowx_u58(x10, (arg1[5]), 0x3ffffffffffffff);
791 let mut x13: u64 = 0;
792 let mut x14: fiat_p521_u1 = 0;
793 let (x13, x14) = fiat_p521_subborrowx_u58(x12, (arg1[6]), 0x3ffffffffffffff);
794 let mut x15: u64 = 0;
795 let mut x16: fiat_p521_u1 = 0;
796 let (x15, x16) = fiat_p521_subborrowx_u58(x14, (arg1[7]), 0x3ffffffffffffff);
797 let mut x17: u64 = 0;
798 let mut x18: fiat_p521_u1 = 0;
799 let (x17, x18) = fiat_p521_subborrowx_u57(x16, (arg1[8]), 0x1ffffffffffffff);
800 let mut x19: u64 = 0;
801 let (x19) = fiat_p521_cmovznz_u64(x18, (0x0 as u64), 0xffffffffffffffff);
802 let mut x20: u64 = 0;
803 let mut x21: fiat_p521_u1 = 0;
804 let (x20, x21) = fiat_p521_addcarryx_u58(0x0, x1, (x19 & 0x3ffffffffffffff));
805 let mut x22: u64 = 0;
806 let mut x23: fiat_p521_u1 = 0;
807 let (x22, x23) = fiat_p521_addcarryx_u58(x21, x3, (x19 & 0x3ffffffffffffff));
808 let mut x24: u64 = 0;
809 let mut x25: fiat_p521_u1 = 0;
810 let (x24, x25) = fiat_p521_addcarryx_u58(x23, x5, (x19 & 0x3ffffffffffffff));
811 let mut x26: u64 = 0;
812 let mut x27: fiat_p521_u1 = 0;
813 let (x26, x27) = fiat_p521_addcarryx_u58(x25, x7, (x19 & 0x3ffffffffffffff));
814 let mut x28: u64 = 0;
815 let mut x29: fiat_p521_u1 = 0;
816 let (x28, x29) = fiat_p521_addcarryx_u58(x27, x9, (x19 & 0x3ffffffffffffff));
817 let mut x30: u64 = 0;
818 let mut x31: fiat_p521_u1 = 0;
819 let (x30, x31) = fiat_p521_addcarryx_u58(x29, x11, (x19 & 0x3ffffffffffffff));
820 let mut x32: u64 = 0;
821 let mut x33: fiat_p521_u1 = 0;
822 let (x32, x33) = fiat_p521_addcarryx_u58(x31, x13, (x19 & 0x3ffffffffffffff));
823 let mut x34: u64 = 0;
824 let mut x35: fiat_p521_u1 = 0;
825 let (x34, x35) = fiat_p521_addcarryx_u58(x33, x15, (x19 & 0x3ffffffffffffff));
826 let mut x36: u64 = 0;
827 let mut x37: fiat_p521_u1 = 0;
828 let (x36, x37) = fiat_p521_addcarryx_u57(x35, x17, (x19 & 0x1ffffffffffffff));
829 let x38: u64 = (x34 << 6);
830 let x39: u64 = (x32 << 4);
831 let x40: u64 = (x30 << 2);
832 let x41: u64 = (x26 << 6);
833 let x42: u64 = (x24 << 4);
834 let x43: u64 = (x22 << 2);
835 let x44: u8 = ((x20 & (0xff as u64)) as u8);
836 let x45: u64 = (x20 >> 8);
837 let x46: u8 = ((x45 & (0xff as u64)) as u8);
838 let x47: u64 = (x45 >> 8);
839 let x48: u8 = ((x47 & (0xff as u64)) as u8);
840 let x49: u64 = (x47 >> 8);
841 let x50: u8 = ((x49 & (0xff as u64)) as u8);
842 let x51: u64 = (x49 >> 8);
843 let x52: u8 = ((x51 & (0xff as u64)) as u8);
844 let x53: u64 = (x51 >> 8);
845 let x54: u8 = ((x53 & (0xff as u64)) as u8);
846 let x55: u64 = (x53 >> 8);
847 let x56: u8 = ((x55 & (0xff as u64)) as u8);
848 let x57: u8 = ((x55 >> 8) as u8);
849 let x58: u64 = (x43 + (x57 as u64));
850 let x59: u8 = ((x58 & (0xff as u64)) as u8);
851 let x60: u64 = (x58 >> 8);
852 let x61: u8 = ((x60 & (0xff as u64)) as u8);
853 let x62: u64 = (x60 >> 8);
854 let x63: u8 = ((x62 & (0xff as u64)) as u8);
855 let x64: u64 = (x62 >> 8);
856 let x65: u8 = ((x64 & (0xff as u64)) as u8);
857 let x66: u64 = (x64 >> 8);
858 let x67: u8 = ((x66 & (0xff as u64)) as u8);
859 let x68: u64 = (x66 >> 8);
860 let x69: u8 = ((x68 & (0xff as u64)) as u8);
861 let x70: u64 = (x68 >> 8);
862 let x71: u8 = ((x70 & (0xff as u64)) as u8);
863 let x72: u8 = ((x70 >> 8) as u8);
864 let x73: u64 = (x42 + (x72 as u64));
865 let x74: u8 = ((x73 & (0xff as u64)) as u8);
866 let x75: u64 = (x73 >> 8);
867 let x76: u8 = ((x75 & (0xff as u64)) as u8);
868 let x77: u64 = (x75 >> 8);
869 let x78: u8 = ((x77 & (0xff as u64)) as u8);
870 let x79: u64 = (x77 >> 8);
871 let x80: u8 = ((x79 & (0xff as u64)) as u8);
872 let x81: u64 = (x79 >> 8);
873 let x82: u8 = ((x81 & (0xff as u64)) as u8);
874 let x83: u64 = (x81 >> 8);
875 let x84: u8 = ((x83 & (0xff as u64)) as u8);
876 let x85: u64 = (x83 >> 8);
877 let x86: u8 = ((x85 & (0xff as u64)) as u8);
878 let x87: u8 = ((x85 >> 8) as u8);
879 let x88: u64 = (x41 + (x87 as u64));
880 let x89: u8 = ((x88 & (0xff as u64)) as u8);
881 let x90: u64 = (x88 >> 8);
882 let x91: u8 = ((x90 & (0xff as u64)) as u8);
883 let x92: u64 = (x90 >> 8);
884 let x93: u8 = ((x92 & (0xff as u64)) as u8);
885 let x94: u64 = (x92 >> 8);
886 let x95: u8 = ((x94 & (0xff as u64)) as u8);
887 let x96: u64 = (x94 >> 8);
888 let x97: u8 = ((x96 & (0xff as u64)) as u8);
889 let x98: u64 = (x96 >> 8);
890 let x99: u8 = ((x98 & (0xff as u64)) as u8);
891 let x100: u64 = (x98 >> 8);
892 let x101: u8 = ((x100 & (0xff as u64)) as u8);
893 let x102: u8 = ((x100 >> 8) as u8);
894 let x103: u8 = ((x28 & (0xff as u64)) as u8);
895 let x104: u64 = (x28 >> 8);
896 let x105: u8 = ((x104 & (0xff as u64)) as u8);
897 let x106: u64 = (x104 >> 8);
898 let x107: u8 = ((x106 & (0xff as u64)) as u8);
899 let x108: u64 = (x106 >> 8);
900 let x109: u8 = ((x108 & (0xff as u64)) as u8);
901 let x110: u64 = (x108 >> 8);
902 let x111: u8 = ((x110 & (0xff as u64)) as u8);
903 let x112: u64 = (x110 >> 8);
904 let x113: u8 = ((x112 & (0xff as u64)) as u8);
905 let x114: u64 = (x112 >> 8);
906 let x115: u8 = ((x114 & (0xff as u64)) as u8);
907 let x116: u8 = ((x114 >> 8) as u8);
908 let x117: u64 = (x40 + (x116 as u64));
909 let x118: u8 = ((x117 & (0xff as u64)) as u8);
910 let x119: u64 = (x117 >> 8);
911 let x120: u8 = ((x119 & (0xff as u64)) as u8);
912 let x121: u64 = (x119 >> 8);
913 let x122: u8 = ((x121 & (0xff as u64)) as u8);
914 let x123: u64 = (x121 >> 8);
915 let x124: u8 = ((x123 & (0xff as u64)) as u8);
916 let x125: u64 = (x123 >> 8);
917 let x126: u8 = ((x125 & (0xff as u64)) as u8);
918 let x127: u64 = (x125 >> 8);
919 let x128: u8 = ((x127 & (0xff as u64)) as u8);
920 let x129: u64 = (x127 >> 8);
921 let x130: u8 = ((x129 & (0xff as u64)) as u8);
922 let x131: u8 = ((x129 >> 8) as u8);
923 let x132: u64 = (x39 + (x131 as u64));
924 let x133: u8 = ((x132 & (0xff as u64)) as u8);
925 let x134: u64 = (x132 >> 8);
926 let x135: u8 = ((x134 & (0xff as u64)) as u8);
927 let x136: u64 = (x134 >> 8);
928 let x137: u8 = ((x136 & (0xff as u64)) as u8);
929 let x138: u64 = (x136 >> 8);
930 let x139: u8 = ((x138 & (0xff as u64)) as u8);
931 let x140: u64 = (x138 >> 8);
932 let x141: u8 = ((x140 & (0xff as u64)) as u8);
933 let x142: u64 = (x140 >> 8);
934 let x143: u8 = ((x142 & (0xff as u64)) as u8);
935 let x144: u64 = (x142 >> 8);
936 let x145: u8 = ((x144 & (0xff as u64)) as u8);
937 let x146: u8 = ((x144 >> 8) as u8);
938 let x147: u64 = (x38 + (x146 as u64));
939 let x148: u8 = ((x147 & (0xff as u64)) as u8);
940 let x149: u64 = (x147 >> 8);
941 let x150: u8 = ((x149 & (0xff as u64)) as u8);
942 let x151: u64 = (x149 >> 8);
943 let x152: u8 = ((x151 & (0xff as u64)) as u8);
944 let x153: u64 = (x151 >> 8);
945 let x154: u8 = ((x153 & (0xff as u64)) as u8);
946 let x155: u64 = (x153 >> 8);
947 let x156: u8 = ((x155 & (0xff as u64)) as u8);
948 let x157: u64 = (x155 >> 8);
949 let x158: u8 = ((x157 & (0xff as u64)) as u8);
950 let x159: u64 = (x157 >> 8);
951 let x160: u8 = ((x159 & (0xff as u64)) as u8);
952 let x161: u8 = ((x159 >> 8) as u8);
953 let x162: u8 = ((x36 & (0xff as u64)) as u8);
954 let x163: u64 = (x36 >> 8);
955 let x164: u8 = ((x163 & (0xff as u64)) as u8);
956 let x165: u64 = (x163 >> 8);
957 let x166: u8 = ((x165 & (0xff as u64)) as u8);
958 let x167: u64 = (x165 >> 8);
959 let x168: u8 = ((x167 & (0xff as u64)) as u8);
960 let x169: u64 = (x167 >> 8);
961 let x170: u8 = ((x169 & (0xff as u64)) as u8);
962 let x171: u64 = (x169 >> 8);
963 let x172: u8 = ((x171 & (0xff as u64)) as u8);
964 let x173: u64 = (x171 >> 8);
965 let x174: u8 = ((x173 & (0xff as u64)) as u8);
966 let x175: fiat_p521_u1 = ((x173 >> 8) as fiat_p521_u1);
967 out1[0] = x44;
968 out1[1] = x46;
969 out1[2] = x48;
970 out1[3] = x50;
971 out1[4] = x52;
972 out1[5] = x54;
973 out1[6] = x56;
974 out1[7] = x59;
975 out1[8] = x61;
976 out1[9] = x63;
977 out1[10] = x65;
978 out1[11] = x67;
979 out1[12] = x69;
980 out1[13] = x71;
981 out1[14] = x74;
982 out1[15] = x76;
983 out1[16] = x78;
984 out1[17] = x80;
985 out1[18] = x82;
986 out1[19] = x84;
987 out1[20] = x86;
988 out1[21] = x89;
989 out1[22] = x91;
990 out1[23] = x93;
991 out1[24] = x95;
992 out1[25] = x97;
993 out1[26] = x99;
994 out1[27] = x101;
995 out1[28] = x102;
996 out1[29] = x103;
997 out1[30] = x105;
998 out1[31] = x107;
999 out1[32] = x109;
1000 out1[33] = x111;
1001 out1[34] = x113;
1002 out1[35] = x115;
1003 out1[36] = x118;
1004 out1[37] = x120;
1005 out1[38] = x122;
1006 out1[39] = x124;
1007 out1[40] = x126;
1008 out1[41] = x128;
1009 out1[42] = x130;
1010 out1[43] = x133;
1011 out1[44] = x135;
1012 out1[45] = x137;
1013 out1[46] = x139;
1014 out1[47] = x141;
1015 out1[48] = x143;
1016 out1[49] = x145;
1017 out1[50] = x148;
1018 out1[51] = x150;
1019 out1[52] = x152;
1020 out1[53] = x154;
1021 out1[54] = x156;
1022 out1[55] = x158;
1023 out1[56] = x160;
1024 out1[57] = x161;
1025 out1[58] = x162;
1026 out1[59] = x164;
1027 out1[60] = x166;
1028 out1[61] = x168;
1029 out1[62] = x170;
1030 out1[63] = x172;
1031 out1[64] = x174;
1032 out1[65] = (x175 as u8);
1033 out1
1034}
1035#[doc = " The function fiat_p521_from_bytes deserializes a field element from bytes in little-endian order."]
1036#[doc = ""]
1037#[doc = " Postconditions:"]
1038#[doc = " eval out1 mod m = bytes_eval arg1 mod m"]
1039#[doc = ""]
1040#[doc = " Input Bounds:"]
1041#[doc = " arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1]]"]
1042#[inline]
1043pub const fn fiat_p521_from_bytes(arg1: &[u8; 66]) -> fiat_p521_tight_field_element {
1044 let mut out1: fiat_p521_tight_field_element = [0; 9];
1045 let x1: u64 = ((((arg1[65]) as fiat_p521_u1) as u64) << 56);
1046 let x2: u64 = (((arg1[64]) as u64) << 48);
1047 let x3: u64 = (((arg1[63]) as u64) << 40);
1048 let x4: u64 = (((arg1[62]) as u64) << 32);
1049 let x5: u64 = (((arg1[61]) as u64) << 24);
1050 let x6: u64 = (((arg1[60]) as u64) << 16);
1051 let x7: u64 = (((arg1[59]) as u64) << 8);
1052 let x8: u8 = (arg1[58]);
1053 let x9: u64 = (((arg1[57]) as u64) << 50);
1054 let x10: u64 = (((arg1[56]) as u64) << 42);
1055 let x11: u64 = (((arg1[55]) as u64) << 34);
1056 let x12: u64 = (((arg1[54]) as u64) << 26);
1057 let x13: u64 = (((arg1[53]) as u64) << 18);
1058 let x14: u64 = (((arg1[52]) as u64) << 10);
1059 let x15: u64 = (((arg1[51]) as u64) << 2);
1060 let x16: u64 = (((arg1[50]) as u64) << 52);
1061 let x17: u64 = (((arg1[49]) as u64) << 44);
1062 let x18: u64 = (((arg1[48]) as u64) << 36);
1063 let x19: u64 = (((arg1[47]) as u64) << 28);
1064 let x20: u64 = (((arg1[46]) as u64) << 20);
1065 let x21: u64 = (((arg1[45]) as u64) << 12);
1066 let x22: u64 = (((arg1[44]) as u64) << 4);
1067 let x23: u64 = (((arg1[43]) as u64) << 54);
1068 let x24: u64 = (((arg1[42]) as u64) << 46);
1069 let x25: u64 = (((arg1[41]) as u64) << 38);
1070 let x26: u64 = (((arg1[40]) as u64) << 30);
1071 let x27: u64 = (((arg1[39]) as u64) << 22);
1072 let x28: u64 = (((arg1[38]) as u64) << 14);
1073 let x29: u64 = (((arg1[37]) as u64) << 6);
1074 let x30: u64 = (((arg1[36]) as u64) << 56);
1075 let x31: u64 = (((arg1[35]) as u64) << 48);
1076 let x32: u64 = (((arg1[34]) as u64) << 40);
1077 let x33: u64 = (((arg1[33]) as u64) << 32);
1078 let x34: u64 = (((arg1[32]) as u64) << 24);
1079 let x35: u64 = (((arg1[31]) as u64) << 16);
1080 let x36: u64 = (((arg1[30]) as u64) << 8);
1081 let x37: u8 = (arg1[29]);
1082 let x38: u64 = (((arg1[28]) as u64) << 50);
1083 let x39: u64 = (((arg1[27]) as u64) << 42);
1084 let x40: u64 = (((arg1[26]) as u64) << 34);
1085 let x41: u64 = (((arg1[25]) as u64) << 26);
1086 let x42: u64 = (((arg1[24]) as u64) << 18);
1087 let x43: u64 = (((arg1[23]) as u64) << 10);
1088 let x44: u64 = (((arg1[22]) as u64) << 2);
1089 let x45: u64 = (((arg1[21]) as u64) << 52);
1090 let x46: u64 = (((arg1[20]) as u64) << 44);
1091 let x47: u64 = (((arg1[19]) as u64) << 36);
1092 let x48: u64 = (((arg1[18]) as u64) << 28);
1093 let x49: u64 = (((arg1[17]) as u64) << 20);
1094 let x50: u64 = (((arg1[16]) as u64) << 12);
1095 let x51: u64 = (((arg1[15]) as u64) << 4);
1096 let x52: u64 = (((arg1[14]) as u64) << 54);
1097 let x53: u64 = (((arg1[13]) as u64) << 46);
1098 let x54: u64 = (((arg1[12]) as u64) << 38);
1099 let x55: u64 = (((arg1[11]) as u64) << 30);
1100 let x56: u64 = (((arg1[10]) as u64) << 22);
1101 let x57: u64 = (((arg1[9]) as u64) << 14);
1102 let x58: u64 = (((arg1[8]) as u64) << 6);
1103 let x59: u64 = (((arg1[7]) as u64) << 56);
1104 let x60: u64 = (((arg1[6]) as u64) << 48);
1105 let x61: u64 = (((arg1[5]) as u64) << 40);
1106 let x62: u64 = (((arg1[4]) as u64) << 32);
1107 let x63: u64 = (((arg1[3]) as u64) << 24);
1108 let x64: u64 = (((arg1[2]) as u64) << 16);
1109 let x65: u64 = (((arg1[1]) as u64) << 8);
1110 let x66: u8 = (arg1[0]);
1111 let x67: u64 = (x65 + (x66 as u64));
1112 let x68: u64 = (x64 + x67);
1113 let x69: u64 = (x63 + x68);
1114 let x70: u64 = (x62 + x69);
1115 let x71: u64 = (x61 + x70);
1116 let x72: u64 = (x60 + x71);
1117 let x73: u64 = (x59 + x72);
1118 let x74: u64 = (x73 & 0x3ffffffffffffff);
1119 let x75: u8 = ((x73 >> 58) as u8);
1120 let x76: u64 = (x58 + (x75 as u64));
1121 let x77: u64 = (x57 + x76);
1122 let x78: u64 = (x56 + x77);
1123 let x79: u64 = (x55 + x78);
1124 let x80: u64 = (x54 + x79);
1125 let x81: u64 = (x53 + x80);
1126 let x82: u64 = (x52 + x81);
1127 let x83: u64 = (x82 & 0x3ffffffffffffff);
1128 let x84: u8 = ((x82 >> 58) as u8);
1129 let x85: u64 = (x51 + (x84 as u64));
1130 let x86: u64 = (x50 + x85);
1131 let x87: u64 = (x49 + x86);
1132 let x88: u64 = (x48 + x87);
1133 let x89: u64 = (x47 + x88);
1134 let x90: u64 = (x46 + x89);
1135 let x91: u64 = (x45 + x90);
1136 let x92: u64 = (x91 & 0x3ffffffffffffff);
1137 let x93: u8 = ((x91 >> 58) as u8);
1138 let x94: u64 = (x44 + (x93 as u64));
1139 let x95: u64 = (x43 + x94);
1140 let x96: u64 = (x42 + x95);
1141 let x97: u64 = (x41 + x96);
1142 let x98: u64 = (x40 + x97);
1143 let x99: u64 = (x39 + x98);
1144 let x100: u64 = (x38 + x99);
1145 let x101: u64 = (x36 + (x37 as u64));
1146 let x102: u64 = (x35 + x101);
1147 let x103: u64 = (x34 + x102);
1148 let x104: u64 = (x33 + x103);
1149 let x105: u64 = (x32 + x104);
1150 let x106: u64 = (x31 + x105);
1151 let x107: u64 = (x30 + x106);
1152 let x108: u64 = (x107 & 0x3ffffffffffffff);
1153 let x109: u8 = ((x107 >> 58) as u8);
1154 let x110: u64 = (x29 + (x109 as u64));
1155 let x111: u64 = (x28 + x110);
1156 let x112: u64 = (x27 + x111);
1157 let x113: u64 = (x26 + x112);
1158 let x114: u64 = (x25 + x113);
1159 let x115: u64 = (x24 + x114);
1160 let x116: u64 = (x23 + x115);
1161 let x117: u64 = (x116 & 0x3ffffffffffffff);
1162 let x118: u8 = ((x116 >> 58) as u8);
1163 let x119: u64 = (x22 + (x118 as u64));
1164 let x120: u64 = (x21 + x119);
1165 let x121: u64 = (x20 + x120);
1166 let x122: u64 = (x19 + x121);
1167 let x123: u64 = (x18 + x122);
1168 let x124: u64 = (x17 + x123);
1169 let x125: u64 = (x16 + x124);
1170 let x126: u64 = (x125 & 0x3ffffffffffffff);
1171 let x127: u8 = ((x125 >> 58) as u8);
1172 let x128: u64 = (x15 + (x127 as u64));
1173 let x129: u64 = (x14 + x128);
1174 let x130: u64 = (x13 + x129);
1175 let x131: u64 = (x12 + x130);
1176 let x132: u64 = (x11 + x131);
1177 let x133: u64 = (x10 + x132);
1178 let x134: u64 = (x9 + x133);
1179 let x135: u64 = (x7 + (x8 as u64));
1180 let x136: u64 = (x6 + x135);
1181 let x137: u64 = (x5 + x136);
1182 let x138: u64 = (x4 + x137);
1183 let x139: u64 = (x3 + x138);
1184 let x140: u64 = (x2 + x139);
1185 let x141: u64 = (x1 + x140);
1186 out1[0] = x74;
1187 out1[1] = x83;
1188 out1[2] = x92;
1189 out1[3] = x100;
1190 out1[4] = x108;
1191 out1[5] = x117;
1192 out1[6] = x126;
1193 out1[7] = x134;
1194 out1[8] = x141;
1195 out1
1196}