]> git.proxmox.com Git - rustc.git/blame - vendor/fiat-crypto/src/p224_32.rs
New upstream version 1.71.1+dfsg1
[rustc.git] / vendor / fiat-crypto / src / p224_32.rs
CommitLineData
0a29b90c
FG
1//! Autogenerated: 'src/ExtractionOCaml/word_by_word_montgomery' --lang Rust --inline p224 32 '2^224 - 2^96 + 1' mul square add sub opp from_montgomery to_montgomery nonzero selectznz to_bytes from_bytes one msat divstep divstep_precomp
2//! curve description: p224
3//! machine_wordsize = 32 (from "32")
4//! requested operations: mul, square, add, sub, opp, from_montgomery, to_montgomery, nonzero, selectznz, to_bytes, from_bytes, one, msat, divstep, divstep_precomp
5//! m = 0xffffffffffffffffffffffffffffffff000000000000000000000001 (from "2^224 - 2^96 + 1")
6//!
7//! NOTE: In addition to the bounds specified above each function, all
8//! functions synthesized for this Montgomery arithmetic require the
9//! input to be strictly less than the prime modulus (m), and also
10//! require the input to be in the unique saturated representation.
11//! All functions also ensure that these two properties are true of
12//! return values.
13//!
14//! Computed values:
15//! eval z = z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192)
16//! 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)
17//! twos_complement_eval z = let x1 := z[0] + (z[1] << 32) + (z[2] << 64) + (z[3] << 96) + (z[4] << 128) + (z[5] << 160) + (z[6] << 192) in
18//! if x1 & (2^224-1) < 2^223 then x1 & (2^224-1) else (x1 & (2^224-1)) - 2^224
19
20#![allow(unused_parens)]
21#![allow(non_camel_case_types)]
22
23pub type fiat_p224_u1 = u8;
24pub type fiat_p224_i1 = i8;
25pub type fiat_p224_u2 = u8;
26pub type fiat_p224_i2 = i8;
27
28/* The type fiat_p224_montgomery_domain_field_element is a field element in the Montgomery domain. */
29/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
30pub type fiat_p224_montgomery_domain_field_element = [u32; 7];
31
32/* The type fiat_p224_non_montgomery_domain_field_element is a field element NOT in the Montgomery domain. */
33/* Bounds: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]] */
34pub type fiat_p224_non_montgomery_domain_field_element = [u32; 7];
35
36
37/// The function fiat_p224_addcarryx_u32 is an addition with carry.
38///
39/// Postconditions:
40/// out1 = (arg1 + arg2 + arg3) mod 2^32
41/// out2 = ⌊(arg1 + arg2 + arg3) / 2^32⌋
42///
43/// Input Bounds:
44/// arg1: [0x0 ~> 0x1]
45/// arg2: [0x0 ~> 0xffffffff]
46/// arg3: [0x0 ~> 0xffffffff]
47/// Output Bounds:
48/// out1: [0x0 ~> 0xffffffff]
49/// out2: [0x0 ~> 0x1]
50#[inline]
51pub fn fiat_p224_addcarryx_u32(out1: &mut u32, out2: &mut fiat_p224_u1, arg1: fiat_p224_u1, arg2: u32, arg3: u32) -> () {
52 let x1: u64 = (((arg1 as u64) + (arg2 as u64)) + (arg3 as u64));
53 let x2: u32 = ((x1 & (0xffffffff as u64)) as u32);
54 let x3: fiat_p224_u1 = ((x1 >> 32) as fiat_p224_u1);
55 *out1 = x2;
56 *out2 = x3;
57}
58
59/// The function fiat_p224_subborrowx_u32 is a subtraction with borrow.
60///
61/// Postconditions:
62/// out1 = (-arg1 + arg2 + -arg3) mod 2^32
63/// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^32⌋
64///
65/// Input Bounds:
66/// arg1: [0x0 ~> 0x1]
67/// arg2: [0x0 ~> 0xffffffff]
68/// arg3: [0x0 ~> 0xffffffff]
69/// Output Bounds:
70/// out1: [0x0 ~> 0xffffffff]
71/// out2: [0x0 ~> 0x1]
72#[inline]
73pub fn fiat_p224_subborrowx_u32(out1: &mut u32, out2: &mut fiat_p224_u1, arg1: fiat_p224_u1, arg2: u32, arg3: u32) -> () {
74 let x1: i64 = (((arg2 as i64) - (arg1 as i64)) - (arg3 as i64));
75 let x2: fiat_p224_i1 = ((x1 >> 32) as fiat_p224_i1);
76 let x3: u32 = ((x1 & (0xffffffff as i64)) as u32);
77 *out1 = x3;
78 *out2 = (((0x0 as fiat_p224_i2) - (x2 as fiat_p224_i2)) as fiat_p224_u1);
79}
80
81/// The function fiat_p224_mulx_u32 is a multiplication, returning the full double-width result.
82///
83/// Postconditions:
84/// out1 = (arg1 * arg2) mod 2^32
85/// out2 = ⌊arg1 * arg2 / 2^32⌋
86///
87/// Input Bounds:
88/// arg1: [0x0 ~> 0xffffffff]
89/// arg2: [0x0 ~> 0xffffffff]
90/// Output Bounds:
91/// out1: [0x0 ~> 0xffffffff]
92/// out2: [0x0 ~> 0xffffffff]
93#[inline]
94pub fn fiat_p224_mulx_u32(out1: &mut u32, out2: &mut u32, arg1: u32, arg2: u32) -> () {
95 let x1: u64 = ((arg1 as u64) * (arg2 as u64));
96 let x2: u32 = ((x1 & (0xffffffff as u64)) as u32);
97 let x3: u32 = ((x1 >> 32) as u32);
98 *out1 = x2;
99 *out2 = x3;
100}
101
102/// The function fiat_p224_cmovznz_u32 is a single-word conditional move.
103///
104/// Postconditions:
105/// out1 = (if arg1 = 0 then arg2 else arg3)
106///
107/// Input Bounds:
108/// arg1: [0x0 ~> 0x1]
109/// arg2: [0x0 ~> 0xffffffff]
110/// arg3: [0x0 ~> 0xffffffff]
111/// Output Bounds:
112/// out1: [0x0 ~> 0xffffffff]
113#[inline]
114pub fn fiat_p224_cmovznz_u32(out1: &mut u32, arg1: fiat_p224_u1, arg2: u32, arg3: u32) -> () {
115 let x1: fiat_p224_u1 = (!(!arg1));
116 let x2: u32 = ((((((0x0 as fiat_p224_i2) - (x1 as fiat_p224_i2)) as fiat_p224_i1) as i64) & (0xffffffff as i64)) as u32);
117 let x3: u32 = ((x2 & arg3) | ((!x2) & arg2));
118 *out1 = x3;
119}
120
121/// The function fiat_p224_mul multiplies two field elements in the Montgomery domain.
122///
123/// Preconditions:
124/// 0 ≤ eval arg1 < m
125/// 0 ≤ eval arg2 < m
126/// Postconditions:
127/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m
128/// 0 ≤ eval out1 < m
129///
130#[inline]
131pub fn fiat_p224_mul(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element, arg2: &fiat_p224_montgomery_domain_field_element) -> () {
132 let x1: u32 = (arg1[1]);
133 let x2: u32 = (arg1[2]);
134 let x3: u32 = (arg1[3]);
135 let x4: u32 = (arg1[4]);
136 let x5: u32 = (arg1[5]);
137 let x6: u32 = (arg1[6]);
138 let x7: u32 = (arg1[0]);
139 let mut x8: u32 = 0;
140 let mut x9: u32 = 0;
141 fiat_p224_mulx_u32(&mut x8, &mut x9, x7, (arg2[6]));
142 let mut x10: u32 = 0;
143 let mut x11: u32 = 0;
144 fiat_p224_mulx_u32(&mut x10, &mut x11, x7, (arg2[5]));
145 let mut x12: u32 = 0;
146 let mut x13: u32 = 0;
147 fiat_p224_mulx_u32(&mut x12, &mut x13, x7, (arg2[4]));
148 let mut x14: u32 = 0;
149 let mut x15: u32 = 0;
150 fiat_p224_mulx_u32(&mut x14, &mut x15, x7, (arg2[3]));
151 let mut x16: u32 = 0;
152 let mut x17: u32 = 0;
153 fiat_p224_mulx_u32(&mut x16, &mut x17, x7, (arg2[2]));
154 let mut x18: u32 = 0;
155 let mut x19: u32 = 0;
156 fiat_p224_mulx_u32(&mut x18, &mut x19, x7, (arg2[1]));
157 let mut x20: u32 = 0;
158 let mut x21: u32 = 0;
159 fiat_p224_mulx_u32(&mut x20, &mut x21, x7, (arg2[0]));
160 let mut x22: u32 = 0;
161 let mut x23: fiat_p224_u1 = 0;
162 fiat_p224_addcarryx_u32(&mut x22, &mut x23, 0x0, x21, x18);
163 let mut x24: u32 = 0;
164 let mut x25: fiat_p224_u1 = 0;
165 fiat_p224_addcarryx_u32(&mut x24, &mut x25, x23, x19, x16);
166 let mut x26: u32 = 0;
167 let mut x27: fiat_p224_u1 = 0;
168 fiat_p224_addcarryx_u32(&mut x26, &mut x27, x25, x17, x14);
169 let mut x28: u32 = 0;
170 let mut x29: fiat_p224_u1 = 0;
171 fiat_p224_addcarryx_u32(&mut x28, &mut x29, x27, x15, x12);
172 let mut x30: u32 = 0;
173 let mut x31: fiat_p224_u1 = 0;
174 fiat_p224_addcarryx_u32(&mut x30, &mut x31, x29, x13, x10);
175 let mut x32: u32 = 0;
176 let mut x33: fiat_p224_u1 = 0;
177 fiat_p224_addcarryx_u32(&mut x32, &mut x33, x31, x11, x8);
178 let x34: u32 = ((x33 as u32) + x9);
179 let mut x35: u32 = 0;
180 let mut x36: u32 = 0;
181 fiat_p224_mulx_u32(&mut x35, &mut x36, x20, 0xffffffff);
182 let mut x37: u32 = 0;
183 let mut x38: u32 = 0;
184 fiat_p224_mulx_u32(&mut x37, &mut x38, x35, 0xffffffff);
185 let mut x39: u32 = 0;
186 let mut x40: u32 = 0;
187 fiat_p224_mulx_u32(&mut x39, &mut x40, x35, 0xffffffff);
188 let mut x41: u32 = 0;
189 let mut x42: u32 = 0;
190 fiat_p224_mulx_u32(&mut x41, &mut x42, x35, 0xffffffff);
191 let mut x43: u32 = 0;
192 let mut x44: u32 = 0;
193 fiat_p224_mulx_u32(&mut x43, &mut x44, x35, 0xffffffff);
194 let mut x45: u32 = 0;
195 let mut x46: fiat_p224_u1 = 0;
196 fiat_p224_addcarryx_u32(&mut x45, &mut x46, 0x0, x44, x41);
197 let mut x47: u32 = 0;
198 let mut x48: fiat_p224_u1 = 0;
199 fiat_p224_addcarryx_u32(&mut x47, &mut x48, x46, x42, x39);
200 let mut x49: u32 = 0;
201 let mut x50: fiat_p224_u1 = 0;
202 fiat_p224_addcarryx_u32(&mut x49, &mut x50, x48, x40, x37);
203 let x51: u32 = ((x50 as u32) + x38);
204 let mut x52: u32 = 0;
205 let mut x53: fiat_p224_u1 = 0;
206 fiat_p224_addcarryx_u32(&mut x52, &mut x53, 0x0, x20, x35);
207 let mut x54: u32 = 0;
208 let mut x55: fiat_p224_u1 = 0;
209 fiat_p224_addcarryx_u32(&mut x54, &mut x55, x53, x22, (0x0 as u32));
210 let mut x56: u32 = 0;
211 let mut x57: fiat_p224_u1 = 0;
212 fiat_p224_addcarryx_u32(&mut x56, &mut x57, x55, x24, (0x0 as u32));
213 let mut x58: u32 = 0;
214 let mut x59: fiat_p224_u1 = 0;
215 fiat_p224_addcarryx_u32(&mut x58, &mut x59, x57, x26, x43);
216 let mut x60: u32 = 0;
217 let mut x61: fiat_p224_u1 = 0;
218 fiat_p224_addcarryx_u32(&mut x60, &mut x61, x59, x28, x45);
219 let mut x62: u32 = 0;
220 let mut x63: fiat_p224_u1 = 0;
221 fiat_p224_addcarryx_u32(&mut x62, &mut x63, x61, x30, x47);
222 let mut x64: u32 = 0;
223 let mut x65: fiat_p224_u1 = 0;
224 fiat_p224_addcarryx_u32(&mut x64, &mut x65, x63, x32, x49);
225 let mut x66: u32 = 0;
226 let mut x67: fiat_p224_u1 = 0;
227 fiat_p224_addcarryx_u32(&mut x66, &mut x67, x65, x34, x51);
228 let mut x68: u32 = 0;
229 let mut x69: u32 = 0;
230 fiat_p224_mulx_u32(&mut x68, &mut x69, x1, (arg2[6]));
231 let mut x70: u32 = 0;
232 let mut x71: u32 = 0;
233 fiat_p224_mulx_u32(&mut x70, &mut x71, x1, (arg2[5]));
234 let mut x72: u32 = 0;
235 let mut x73: u32 = 0;
236 fiat_p224_mulx_u32(&mut x72, &mut x73, x1, (arg2[4]));
237 let mut x74: u32 = 0;
238 let mut x75: u32 = 0;
239 fiat_p224_mulx_u32(&mut x74, &mut x75, x1, (arg2[3]));
240 let mut x76: u32 = 0;
241 let mut x77: u32 = 0;
242 fiat_p224_mulx_u32(&mut x76, &mut x77, x1, (arg2[2]));
243 let mut x78: u32 = 0;
244 let mut x79: u32 = 0;
245 fiat_p224_mulx_u32(&mut x78, &mut x79, x1, (arg2[1]));
246 let mut x80: u32 = 0;
247 let mut x81: u32 = 0;
248 fiat_p224_mulx_u32(&mut x80, &mut x81, x1, (arg2[0]));
249 let mut x82: u32 = 0;
250 let mut x83: fiat_p224_u1 = 0;
251 fiat_p224_addcarryx_u32(&mut x82, &mut x83, 0x0, x81, x78);
252 let mut x84: u32 = 0;
253 let mut x85: fiat_p224_u1 = 0;
254 fiat_p224_addcarryx_u32(&mut x84, &mut x85, x83, x79, x76);
255 let mut x86: u32 = 0;
256 let mut x87: fiat_p224_u1 = 0;
257 fiat_p224_addcarryx_u32(&mut x86, &mut x87, x85, x77, x74);
258 let mut x88: u32 = 0;
259 let mut x89: fiat_p224_u1 = 0;
260 fiat_p224_addcarryx_u32(&mut x88, &mut x89, x87, x75, x72);
261 let mut x90: u32 = 0;
262 let mut x91: fiat_p224_u1 = 0;
263 fiat_p224_addcarryx_u32(&mut x90, &mut x91, x89, x73, x70);
264 let mut x92: u32 = 0;
265 let mut x93: fiat_p224_u1 = 0;
266 fiat_p224_addcarryx_u32(&mut x92, &mut x93, x91, x71, x68);
267 let x94: u32 = ((x93 as u32) + x69);
268 let mut x95: u32 = 0;
269 let mut x96: fiat_p224_u1 = 0;
270 fiat_p224_addcarryx_u32(&mut x95, &mut x96, 0x0, x54, x80);
271 let mut x97: u32 = 0;
272 let mut x98: fiat_p224_u1 = 0;
273 fiat_p224_addcarryx_u32(&mut x97, &mut x98, x96, x56, x82);
274 let mut x99: u32 = 0;
275 let mut x100: fiat_p224_u1 = 0;
276 fiat_p224_addcarryx_u32(&mut x99, &mut x100, x98, x58, x84);
277 let mut x101: u32 = 0;
278 let mut x102: fiat_p224_u1 = 0;
279 fiat_p224_addcarryx_u32(&mut x101, &mut x102, x100, x60, x86);
280 let mut x103: u32 = 0;
281 let mut x104: fiat_p224_u1 = 0;
282 fiat_p224_addcarryx_u32(&mut x103, &mut x104, x102, x62, x88);
283 let mut x105: u32 = 0;
284 let mut x106: fiat_p224_u1 = 0;
285 fiat_p224_addcarryx_u32(&mut x105, &mut x106, x104, x64, x90);
286 let mut x107: u32 = 0;
287 let mut x108: fiat_p224_u1 = 0;
288 fiat_p224_addcarryx_u32(&mut x107, &mut x108, x106, x66, x92);
289 let mut x109: u32 = 0;
290 let mut x110: fiat_p224_u1 = 0;
291 fiat_p224_addcarryx_u32(&mut x109, &mut x110, x108, (x67 as u32), x94);
292 let mut x111: u32 = 0;
293 let mut x112: u32 = 0;
294 fiat_p224_mulx_u32(&mut x111, &mut x112, x95, 0xffffffff);
295 let mut x113: u32 = 0;
296 let mut x114: u32 = 0;
297 fiat_p224_mulx_u32(&mut x113, &mut x114, x111, 0xffffffff);
298 let mut x115: u32 = 0;
299 let mut x116: u32 = 0;
300 fiat_p224_mulx_u32(&mut x115, &mut x116, x111, 0xffffffff);
301 let mut x117: u32 = 0;
302 let mut x118: u32 = 0;
303 fiat_p224_mulx_u32(&mut x117, &mut x118, x111, 0xffffffff);
304 let mut x119: u32 = 0;
305 let mut x120: u32 = 0;
306 fiat_p224_mulx_u32(&mut x119, &mut x120, x111, 0xffffffff);
307 let mut x121: u32 = 0;
308 let mut x122: fiat_p224_u1 = 0;
309 fiat_p224_addcarryx_u32(&mut x121, &mut x122, 0x0, x120, x117);
310 let mut x123: u32 = 0;
311 let mut x124: fiat_p224_u1 = 0;
312 fiat_p224_addcarryx_u32(&mut x123, &mut x124, x122, x118, x115);
313 let mut x125: u32 = 0;
314 let mut x126: fiat_p224_u1 = 0;
315 fiat_p224_addcarryx_u32(&mut x125, &mut x126, x124, x116, x113);
316 let x127: u32 = ((x126 as u32) + x114);
317 let mut x128: u32 = 0;
318 let mut x129: fiat_p224_u1 = 0;
319 fiat_p224_addcarryx_u32(&mut x128, &mut x129, 0x0, x95, x111);
320 let mut x130: u32 = 0;
321 let mut x131: fiat_p224_u1 = 0;
322 fiat_p224_addcarryx_u32(&mut x130, &mut x131, x129, x97, (0x0 as u32));
323 let mut x132: u32 = 0;
324 let mut x133: fiat_p224_u1 = 0;
325 fiat_p224_addcarryx_u32(&mut x132, &mut x133, x131, x99, (0x0 as u32));
326 let mut x134: u32 = 0;
327 let mut x135: fiat_p224_u1 = 0;
328 fiat_p224_addcarryx_u32(&mut x134, &mut x135, x133, x101, x119);
329 let mut x136: u32 = 0;
330 let mut x137: fiat_p224_u1 = 0;
331 fiat_p224_addcarryx_u32(&mut x136, &mut x137, x135, x103, x121);
332 let mut x138: u32 = 0;
333 let mut x139: fiat_p224_u1 = 0;
334 fiat_p224_addcarryx_u32(&mut x138, &mut x139, x137, x105, x123);
335 let mut x140: u32 = 0;
336 let mut x141: fiat_p224_u1 = 0;
337 fiat_p224_addcarryx_u32(&mut x140, &mut x141, x139, x107, x125);
338 let mut x142: u32 = 0;
339 let mut x143: fiat_p224_u1 = 0;
340 fiat_p224_addcarryx_u32(&mut x142, &mut x143, x141, x109, x127);
341 let x144: u32 = ((x143 as u32) + (x110 as u32));
342 let mut x145: u32 = 0;
343 let mut x146: u32 = 0;
344 fiat_p224_mulx_u32(&mut x145, &mut x146, x2, (arg2[6]));
345 let mut x147: u32 = 0;
346 let mut x148: u32 = 0;
347 fiat_p224_mulx_u32(&mut x147, &mut x148, x2, (arg2[5]));
348 let mut x149: u32 = 0;
349 let mut x150: u32 = 0;
350 fiat_p224_mulx_u32(&mut x149, &mut x150, x2, (arg2[4]));
351 let mut x151: u32 = 0;
352 let mut x152: u32 = 0;
353 fiat_p224_mulx_u32(&mut x151, &mut x152, x2, (arg2[3]));
354 let mut x153: u32 = 0;
355 let mut x154: u32 = 0;
356 fiat_p224_mulx_u32(&mut x153, &mut x154, x2, (arg2[2]));
357 let mut x155: u32 = 0;
358 let mut x156: u32 = 0;
359 fiat_p224_mulx_u32(&mut x155, &mut x156, x2, (arg2[1]));
360 let mut x157: u32 = 0;
361 let mut x158: u32 = 0;
362 fiat_p224_mulx_u32(&mut x157, &mut x158, x2, (arg2[0]));
363 let mut x159: u32 = 0;
364 let mut x160: fiat_p224_u1 = 0;
365 fiat_p224_addcarryx_u32(&mut x159, &mut x160, 0x0, x158, x155);
366 let mut x161: u32 = 0;
367 let mut x162: fiat_p224_u1 = 0;
368 fiat_p224_addcarryx_u32(&mut x161, &mut x162, x160, x156, x153);
369 let mut x163: u32 = 0;
370 let mut x164: fiat_p224_u1 = 0;
371 fiat_p224_addcarryx_u32(&mut x163, &mut x164, x162, x154, x151);
372 let mut x165: u32 = 0;
373 let mut x166: fiat_p224_u1 = 0;
374 fiat_p224_addcarryx_u32(&mut x165, &mut x166, x164, x152, x149);
375 let mut x167: u32 = 0;
376 let mut x168: fiat_p224_u1 = 0;
377 fiat_p224_addcarryx_u32(&mut x167, &mut x168, x166, x150, x147);
378 let mut x169: u32 = 0;
379 let mut x170: fiat_p224_u1 = 0;
380 fiat_p224_addcarryx_u32(&mut x169, &mut x170, x168, x148, x145);
381 let x171: u32 = ((x170 as u32) + x146);
382 let mut x172: u32 = 0;
383 let mut x173: fiat_p224_u1 = 0;
384 fiat_p224_addcarryx_u32(&mut x172, &mut x173, 0x0, x130, x157);
385 let mut x174: u32 = 0;
386 let mut x175: fiat_p224_u1 = 0;
387 fiat_p224_addcarryx_u32(&mut x174, &mut x175, x173, x132, x159);
388 let mut x176: u32 = 0;
389 let mut x177: fiat_p224_u1 = 0;
390 fiat_p224_addcarryx_u32(&mut x176, &mut x177, x175, x134, x161);
391 let mut x178: u32 = 0;
392 let mut x179: fiat_p224_u1 = 0;
393 fiat_p224_addcarryx_u32(&mut x178, &mut x179, x177, x136, x163);
394 let mut x180: u32 = 0;
395 let mut x181: fiat_p224_u1 = 0;
396 fiat_p224_addcarryx_u32(&mut x180, &mut x181, x179, x138, x165);
397 let mut x182: u32 = 0;
398 let mut x183: fiat_p224_u1 = 0;
399 fiat_p224_addcarryx_u32(&mut x182, &mut x183, x181, x140, x167);
400 let mut x184: u32 = 0;
401 let mut x185: fiat_p224_u1 = 0;
402 fiat_p224_addcarryx_u32(&mut x184, &mut x185, x183, x142, x169);
403 let mut x186: u32 = 0;
404 let mut x187: fiat_p224_u1 = 0;
405 fiat_p224_addcarryx_u32(&mut x186, &mut x187, x185, x144, x171);
406 let mut x188: u32 = 0;
407 let mut x189: u32 = 0;
408 fiat_p224_mulx_u32(&mut x188, &mut x189, x172, 0xffffffff);
409 let mut x190: u32 = 0;
410 let mut x191: u32 = 0;
411 fiat_p224_mulx_u32(&mut x190, &mut x191, x188, 0xffffffff);
412 let mut x192: u32 = 0;
413 let mut x193: u32 = 0;
414 fiat_p224_mulx_u32(&mut x192, &mut x193, x188, 0xffffffff);
415 let mut x194: u32 = 0;
416 let mut x195: u32 = 0;
417 fiat_p224_mulx_u32(&mut x194, &mut x195, x188, 0xffffffff);
418 let mut x196: u32 = 0;
419 let mut x197: u32 = 0;
420 fiat_p224_mulx_u32(&mut x196, &mut x197, x188, 0xffffffff);
421 let mut x198: u32 = 0;
422 let mut x199: fiat_p224_u1 = 0;
423 fiat_p224_addcarryx_u32(&mut x198, &mut x199, 0x0, x197, x194);
424 let mut x200: u32 = 0;
425 let mut x201: fiat_p224_u1 = 0;
426 fiat_p224_addcarryx_u32(&mut x200, &mut x201, x199, x195, x192);
427 let mut x202: u32 = 0;
428 let mut x203: fiat_p224_u1 = 0;
429 fiat_p224_addcarryx_u32(&mut x202, &mut x203, x201, x193, x190);
430 let x204: u32 = ((x203 as u32) + x191);
431 let mut x205: u32 = 0;
432 let mut x206: fiat_p224_u1 = 0;
433 fiat_p224_addcarryx_u32(&mut x205, &mut x206, 0x0, x172, x188);
434 let mut x207: u32 = 0;
435 let mut x208: fiat_p224_u1 = 0;
436 fiat_p224_addcarryx_u32(&mut x207, &mut x208, x206, x174, (0x0 as u32));
437 let mut x209: u32 = 0;
438 let mut x210: fiat_p224_u1 = 0;
439 fiat_p224_addcarryx_u32(&mut x209, &mut x210, x208, x176, (0x0 as u32));
440 let mut x211: u32 = 0;
441 let mut x212: fiat_p224_u1 = 0;
442 fiat_p224_addcarryx_u32(&mut x211, &mut x212, x210, x178, x196);
443 let mut x213: u32 = 0;
444 let mut x214: fiat_p224_u1 = 0;
445 fiat_p224_addcarryx_u32(&mut x213, &mut x214, x212, x180, x198);
446 let mut x215: u32 = 0;
447 let mut x216: fiat_p224_u1 = 0;
448 fiat_p224_addcarryx_u32(&mut x215, &mut x216, x214, x182, x200);
449 let mut x217: u32 = 0;
450 let mut x218: fiat_p224_u1 = 0;
451 fiat_p224_addcarryx_u32(&mut x217, &mut x218, x216, x184, x202);
452 let mut x219: u32 = 0;
453 let mut x220: fiat_p224_u1 = 0;
454 fiat_p224_addcarryx_u32(&mut x219, &mut x220, x218, x186, x204);
455 let x221: u32 = ((x220 as u32) + (x187 as u32));
456 let mut x222: u32 = 0;
457 let mut x223: u32 = 0;
458 fiat_p224_mulx_u32(&mut x222, &mut x223, x3, (arg2[6]));
459 let mut x224: u32 = 0;
460 let mut x225: u32 = 0;
461 fiat_p224_mulx_u32(&mut x224, &mut x225, x3, (arg2[5]));
462 let mut x226: u32 = 0;
463 let mut x227: u32 = 0;
464 fiat_p224_mulx_u32(&mut x226, &mut x227, x3, (arg2[4]));
465 let mut x228: u32 = 0;
466 let mut x229: u32 = 0;
467 fiat_p224_mulx_u32(&mut x228, &mut x229, x3, (arg2[3]));
468 let mut x230: u32 = 0;
469 let mut x231: u32 = 0;
470 fiat_p224_mulx_u32(&mut x230, &mut x231, x3, (arg2[2]));
471 let mut x232: u32 = 0;
472 let mut x233: u32 = 0;
473 fiat_p224_mulx_u32(&mut x232, &mut x233, x3, (arg2[1]));
474 let mut x234: u32 = 0;
475 let mut x235: u32 = 0;
476 fiat_p224_mulx_u32(&mut x234, &mut x235, x3, (arg2[0]));
477 let mut x236: u32 = 0;
478 let mut x237: fiat_p224_u1 = 0;
479 fiat_p224_addcarryx_u32(&mut x236, &mut x237, 0x0, x235, x232);
480 let mut x238: u32 = 0;
481 let mut x239: fiat_p224_u1 = 0;
482 fiat_p224_addcarryx_u32(&mut x238, &mut x239, x237, x233, x230);
483 let mut x240: u32 = 0;
484 let mut x241: fiat_p224_u1 = 0;
485 fiat_p224_addcarryx_u32(&mut x240, &mut x241, x239, x231, x228);
486 let mut x242: u32 = 0;
487 let mut x243: fiat_p224_u1 = 0;
488 fiat_p224_addcarryx_u32(&mut x242, &mut x243, x241, x229, x226);
489 let mut x244: u32 = 0;
490 let mut x245: fiat_p224_u1 = 0;
491 fiat_p224_addcarryx_u32(&mut x244, &mut x245, x243, x227, x224);
492 let mut x246: u32 = 0;
493 let mut x247: fiat_p224_u1 = 0;
494 fiat_p224_addcarryx_u32(&mut x246, &mut x247, x245, x225, x222);
495 let x248: u32 = ((x247 as u32) + x223);
496 let mut x249: u32 = 0;
497 let mut x250: fiat_p224_u1 = 0;
498 fiat_p224_addcarryx_u32(&mut x249, &mut x250, 0x0, x207, x234);
499 let mut x251: u32 = 0;
500 let mut x252: fiat_p224_u1 = 0;
501 fiat_p224_addcarryx_u32(&mut x251, &mut x252, x250, x209, x236);
502 let mut x253: u32 = 0;
503 let mut x254: fiat_p224_u1 = 0;
504 fiat_p224_addcarryx_u32(&mut x253, &mut x254, x252, x211, x238);
505 let mut x255: u32 = 0;
506 let mut x256: fiat_p224_u1 = 0;
507 fiat_p224_addcarryx_u32(&mut x255, &mut x256, x254, x213, x240);
508 let mut x257: u32 = 0;
509 let mut x258: fiat_p224_u1 = 0;
510 fiat_p224_addcarryx_u32(&mut x257, &mut x258, x256, x215, x242);
511 let mut x259: u32 = 0;
512 let mut x260: fiat_p224_u1 = 0;
513 fiat_p224_addcarryx_u32(&mut x259, &mut x260, x258, x217, x244);
514 let mut x261: u32 = 0;
515 let mut x262: fiat_p224_u1 = 0;
516 fiat_p224_addcarryx_u32(&mut x261, &mut x262, x260, x219, x246);
517 let mut x263: u32 = 0;
518 let mut x264: fiat_p224_u1 = 0;
519 fiat_p224_addcarryx_u32(&mut x263, &mut x264, x262, x221, x248);
520 let mut x265: u32 = 0;
521 let mut x266: u32 = 0;
522 fiat_p224_mulx_u32(&mut x265, &mut x266, x249, 0xffffffff);
523 let mut x267: u32 = 0;
524 let mut x268: u32 = 0;
525 fiat_p224_mulx_u32(&mut x267, &mut x268, x265, 0xffffffff);
526 let mut x269: u32 = 0;
527 let mut x270: u32 = 0;
528 fiat_p224_mulx_u32(&mut x269, &mut x270, x265, 0xffffffff);
529 let mut x271: u32 = 0;
530 let mut x272: u32 = 0;
531 fiat_p224_mulx_u32(&mut x271, &mut x272, x265, 0xffffffff);
532 let mut x273: u32 = 0;
533 let mut x274: u32 = 0;
534 fiat_p224_mulx_u32(&mut x273, &mut x274, x265, 0xffffffff);
535 let mut x275: u32 = 0;
536 let mut x276: fiat_p224_u1 = 0;
537 fiat_p224_addcarryx_u32(&mut x275, &mut x276, 0x0, x274, x271);
538 let mut x277: u32 = 0;
539 let mut x278: fiat_p224_u1 = 0;
540 fiat_p224_addcarryx_u32(&mut x277, &mut x278, x276, x272, x269);
541 let mut x279: u32 = 0;
542 let mut x280: fiat_p224_u1 = 0;
543 fiat_p224_addcarryx_u32(&mut x279, &mut x280, x278, x270, x267);
544 let x281: u32 = ((x280 as u32) + x268);
545 let mut x282: u32 = 0;
546 let mut x283: fiat_p224_u1 = 0;
547 fiat_p224_addcarryx_u32(&mut x282, &mut x283, 0x0, x249, x265);
548 let mut x284: u32 = 0;
549 let mut x285: fiat_p224_u1 = 0;
550 fiat_p224_addcarryx_u32(&mut x284, &mut x285, x283, x251, (0x0 as u32));
551 let mut x286: u32 = 0;
552 let mut x287: fiat_p224_u1 = 0;
553 fiat_p224_addcarryx_u32(&mut x286, &mut x287, x285, x253, (0x0 as u32));
554 let mut x288: u32 = 0;
555 let mut x289: fiat_p224_u1 = 0;
556 fiat_p224_addcarryx_u32(&mut x288, &mut x289, x287, x255, x273);
557 let mut x290: u32 = 0;
558 let mut x291: fiat_p224_u1 = 0;
559 fiat_p224_addcarryx_u32(&mut x290, &mut x291, x289, x257, x275);
560 let mut x292: u32 = 0;
561 let mut x293: fiat_p224_u1 = 0;
562 fiat_p224_addcarryx_u32(&mut x292, &mut x293, x291, x259, x277);
563 let mut x294: u32 = 0;
564 let mut x295: fiat_p224_u1 = 0;
565 fiat_p224_addcarryx_u32(&mut x294, &mut x295, x293, x261, x279);
566 let mut x296: u32 = 0;
567 let mut x297: fiat_p224_u1 = 0;
568 fiat_p224_addcarryx_u32(&mut x296, &mut x297, x295, x263, x281);
569 let x298: u32 = ((x297 as u32) + (x264 as u32));
570 let mut x299: u32 = 0;
571 let mut x300: u32 = 0;
572 fiat_p224_mulx_u32(&mut x299, &mut x300, x4, (arg2[6]));
573 let mut x301: u32 = 0;
574 let mut x302: u32 = 0;
575 fiat_p224_mulx_u32(&mut x301, &mut x302, x4, (arg2[5]));
576 let mut x303: u32 = 0;
577 let mut x304: u32 = 0;
578 fiat_p224_mulx_u32(&mut x303, &mut x304, x4, (arg2[4]));
579 let mut x305: u32 = 0;
580 let mut x306: u32 = 0;
581 fiat_p224_mulx_u32(&mut x305, &mut x306, x4, (arg2[3]));
582 let mut x307: u32 = 0;
583 let mut x308: u32 = 0;
584 fiat_p224_mulx_u32(&mut x307, &mut x308, x4, (arg2[2]));
585 let mut x309: u32 = 0;
586 let mut x310: u32 = 0;
587 fiat_p224_mulx_u32(&mut x309, &mut x310, x4, (arg2[1]));
588 let mut x311: u32 = 0;
589 let mut x312: u32 = 0;
590 fiat_p224_mulx_u32(&mut x311, &mut x312, x4, (arg2[0]));
591 let mut x313: u32 = 0;
592 let mut x314: fiat_p224_u1 = 0;
593 fiat_p224_addcarryx_u32(&mut x313, &mut x314, 0x0, x312, x309);
594 let mut x315: u32 = 0;
595 let mut x316: fiat_p224_u1 = 0;
596 fiat_p224_addcarryx_u32(&mut x315, &mut x316, x314, x310, x307);
597 let mut x317: u32 = 0;
598 let mut x318: fiat_p224_u1 = 0;
599 fiat_p224_addcarryx_u32(&mut x317, &mut x318, x316, x308, x305);
600 let mut x319: u32 = 0;
601 let mut x320: fiat_p224_u1 = 0;
602 fiat_p224_addcarryx_u32(&mut x319, &mut x320, x318, x306, x303);
603 let mut x321: u32 = 0;
604 let mut x322: fiat_p224_u1 = 0;
605 fiat_p224_addcarryx_u32(&mut x321, &mut x322, x320, x304, x301);
606 let mut x323: u32 = 0;
607 let mut x324: fiat_p224_u1 = 0;
608 fiat_p224_addcarryx_u32(&mut x323, &mut x324, x322, x302, x299);
609 let x325: u32 = ((x324 as u32) + x300);
610 let mut x326: u32 = 0;
611 let mut x327: fiat_p224_u1 = 0;
612 fiat_p224_addcarryx_u32(&mut x326, &mut x327, 0x0, x284, x311);
613 let mut x328: u32 = 0;
614 let mut x329: fiat_p224_u1 = 0;
615 fiat_p224_addcarryx_u32(&mut x328, &mut x329, x327, x286, x313);
616 let mut x330: u32 = 0;
617 let mut x331: fiat_p224_u1 = 0;
618 fiat_p224_addcarryx_u32(&mut x330, &mut x331, x329, x288, x315);
619 let mut x332: u32 = 0;
620 let mut x333: fiat_p224_u1 = 0;
621 fiat_p224_addcarryx_u32(&mut x332, &mut x333, x331, x290, x317);
622 let mut x334: u32 = 0;
623 let mut x335: fiat_p224_u1 = 0;
624 fiat_p224_addcarryx_u32(&mut x334, &mut x335, x333, x292, x319);
625 let mut x336: u32 = 0;
626 let mut x337: fiat_p224_u1 = 0;
627 fiat_p224_addcarryx_u32(&mut x336, &mut x337, x335, x294, x321);
628 let mut x338: u32 = 0;
629 let mut x339: fiat_p224_u1 = 0;
630 fiat_p224_addcarryx_u32(&mut x338, &mut x339, x337, x296, x323);
631 let mut x340: u32 = 0;
632 let mut x341: fiat_p224_u1 = 0;
633 fiat_p224_addcarryx_u32(&mut x340, &mut x341, x339, x298, x325);
634 let mut x342: u32 = 0;
635 let mut x343: u32 = 0;
636 fiat_p224_mulx_u32(&mut x342, &mut x343, x326, 0xffffffff);
637 let mut x344: u32 = 0;
638 let mut x345: u32 = 0;
639 fiat_p224_mulx_u32(&mut x344, &mut x345, x342, 0xffffffff);
640 let mut x346: u32 = 0;
641 let mut x347: u32 = 0;
642 fiat_p224_mulx_u32(&mut x346, &mut x347, x342, 0xffffffff);
643 let mut x348: u32 = 0;
644 let mut x349: u32 = 0;
645 fiat_p224_mulx_u32(&mut x348, &mut x349, x342, 0xffffffff);
646 let mut x350: u32 = 0;
647 let mut x351: u32 = 0;
648 fiat_p224_mulx_u32(&mut x350, &mut x351, x342, 0xffffffff);
649 let mut x352: u32 = 0;
650 let mut x353: fiat_p224_u1 = 0;
651 fiat_p224_addcarryx_u32(&mut x352, &mut x353, 0x0, x351, x348);
652 let mut x354: u32 = 0;
653 let mut x355: fiat_p224_u1 = 0;
654 fiat_p224_addcarryx_u32(&mut x354, &mut x355, x353, x349, x346);
655 let mut x356: u32 = 0;
656 let mut x357: fiat_p224_u1 = 0;
657 fiat_p224_addcarryx_u32(&mut x356, &mut x357, x355, x347, x344);
658 let x358: u32 = ((x357 as u32) + x345);
659 let mut x359: u32 = 0;
660 let mut x360: fiat_p224_u1 = 0;
661 fiat_p224_addcarryx_u32(&mut x359, &mut x360, 0x0, x326, x342);
662 let mut x361: u32 = 0;
663 let mut x362: fiat_p224_u1 = 0;
664 fiat_p224_addcarryx_u32(&mut x361, &mut x362, x360, x328, (0x0 as u32));
665 let mut x363: u32 = 0;
666 let mut x364: fiat_p224_u1 = 0;
667 fiat_p224_addcarryx_u32(&mut x363, &mut x364, x362, x330, (0x0 as u32));
668 let mut x365: u32 = 0;
669 let mut x366: fiat_p224_u1 = 0;
670 fiat_p224_addcarryx_u32(&mut x365, &mut x366, x364, x332, x350);
671 let mut x367: u32 = 0;
672 let mut x368: fiat_p224_u1 = 0;
673 fiat_p224_addcarryx_u32(&mut x367, &mut x368, x366, x334, x352);
674 let mut x369: u32 = 0;
675 let mut x370: fiat_p224_u1 = 0;
676 fiat_p224_addcarryx_u32(&mut x369, &mut x370, x368, x336, x354);
677 let mut x371: u32 = 0;
678 let mut x372: fiat_p224_u1 = 0;
679 fiat_p224_addcarryx_u32(&mut x371, &mut x372, x370, x338, x356);
680 let mut x373: u32 = 0;
681 let mut x374: fiat_p224_u1 = 0;
682 fiat_p224_addcarryx_u32(&mut x373, &mut x374, x372, x340, x358);
683 let x375: u32 = ((x374 as u32) + (x341 as u32));
684 let mut x376: u32 = 0;
685 let mut x377: u32 = 0;
686 fiat_p224_mulx_u32(&mut x376, &mut x377, x5, (arg2[6]));
687 let mut x378: u32 = 0;
688 let mut x379: u32 = 0;
689 fiat_p224_mulx_u32(&mut x378, &mut x379, x5, (arg2[5]));
690 let mut x380: u32 = 0;
691 let mut x381: u32 = 0;
692 fiat_p224_mulx_u32(&mut x380, &mut x381, x5, (arg2[4]));
693 let mut x382: u32 = 0;
694 let mut x383: u32 = 0;
695 fiat_p224_mulx_u32(&mut x382, &mut x383, x5, (arg2[3]));
696 let mut x384: u32 = 0;
697 let mut x385: u32 = 0;
698 fiat_p224_mulx_u32(&mut x384, &mut x385, x5, (arg2[2]));
699 let mut x386: u32 = 0;
700 let mut x387: u32 = 0;
701 fiat_p224_mulx_u32(&mut x386, &mut x387, x5, (arg2[1]));
702 let mut x388: u32 = 0;
703 let mut x389: u32 = 0;
704 fiat_p224_mulx_u32(&mut x388, &mut x389, x5, (arg2[0]));
705 let mut x390: u32 = 0;
706 let mut x391: fiat_p224_u1 = 0;
707 fiat_p224_addcarryx_u32(&mut x390, &mut x391, 0x0, x389, x386);
708 let mut x392: u32 = 0;
709 let mut x393: fiat_p224_u1 = 0;
710 fiat_p224_addcarryx_u32(&mut x392, &mut x393, x391, x387, x384);
711 let mut x394: u32 = 0;
712 let mut x395: fiat_p224_u1 = 0;
713 fiat_p224_addcarryx_u32(&mut x394, &mut x395, x393, x385, x382);
714 let mut x396: u32 = 0;
715 let mut x397: fiat_p224_u1 = 0;
716 fiat_p224_addcarryx_u32(&mut x396, &mut x397, x395, x383, x380);
717 let mut x398: u32 = 0;
718 let mut x399: fiat_p224_u1 = 0;
719 fiat_p224_addcarryx_u32(&mut x398, &mut x399, x397, x381, x378);
720 let mut x400: u32 = 0;
721 let mut x401: fiat_p224_u1 = 0;
722 fiat_p224_addcarryx_u32(&mut x400, &mut x401, x399, x379, x376);
723 let x402: u32 = ((x401 as u32) + x377);
724 let mut x403: u32 = 0;
725 let mut x404: fiat_p224_u1 = 0;
726 fiat_p224_addcarryx_u32(&mut x403, &mut x404, 0x0, x361, x388);
727 let mut x405: u32 = 0;
728 let mut x406: fiat_p224_u1 = 0;
729 fiat_p224_addcarryx_u32(&mut x405, &mut x406, x404, x363, x390);
730 let mut x407: u32 = 0;
731 let mut x408: fiat_p224_u1 = 0;
732 fiat_p224_addcarryx_u32(&mut x407, &mut x408, x406, x365, x392);
733 let mut x409: u32 = 0;
734 let mut x410: fiat_p224_u1 = 0;
735 fiat_p224_addcarryx_u32(&mut x409, &mut x410, x408, x367, x394);
736 let mut x411: u32 = 0;
737 let mut x412: fiat_p224_u1 = 0;
738 fiat_p224_addcarryx_u32(&mut x411, &mut x412, x410, x369, x396);
739 let mut x413: u32 = 0;
740 let mut x414: fiat_p224_u1 = 0;
741 fiat_p224_addcarryx_u32(&mut x413, &mut x414, x412, x371, x398);
742 let mut x415: u32 = 0;
743 let mut x416: fiat_p224_u1 = 0;
744 fiat_p224_addcarryx_u32(&mut x415, &mut x416, x414, x373, x400);
745 let mut x417: u32 = 0;
746 let mut x418: fiat_p224_u1 = 0;
747 fiat_p224_addcarryx_u32(&mut x417, &mut x418, x416, x375, x402);
748 let mut x419: u32 = 0;
749 let mut x420: u32 = 0;
750 fiat_p224_mulx_u32(&mut x419, &mut x420, x403, 0xffffffff);
751 let mut x421: u32 = 0;
752 let mut x422: u32 = 0;
753 fiat_p224_mulx_u32(&mut x421, &mut x422, x419, 0xffffffff);
754 let mut x423: u32 = 0;
755 let mut x424: u32 = 0;
756 fiat_p224_mulx_u32(&mut x423, &mut x424, x419, 0xffffffff);
757 let mut x425: u32 = 0;
758 let mut x426: u32 = 0;
759 fiat_p224_mulx_u32(&mut x425, &mut x426, x419, 0xffffffff);
760 let mut x427: u32 = 0;
761 let mut x428: u32 = 0;
762 fiat_p224_mulx_u32(&mut x427, &mut x428, x419, 0xffffffff);
763 let mut x429: u32 = 0;
764 let mut x430: fiat_p224_u1 = 0;
765 fiat_p224_addcarryx_u32(&mut x429, &mut x430, 0x0, x428, x425);
766 let mut x431: u32 = 0;
767 let mut x432: fiat_p224_u1 = 0;
768 fiat_p224_addcarryx_u32(&mut x431, &mut x432, x430, x426, x423);
769 let mut x433: u32 = 0;
770 let mut x434: fiat_p224_u1 = 0;
771 fiat_p224_addcarryx_u32(&mut x433, &mut x434, x432, x424, x421);
772 let x435: u32 = ((x434 as u32) + x422);
773 let mut x436: u32 = 0;
774 let mut x437: fiat_p224_u1 = 0;
775 fiat_p224_addcarryx_u32(&mut x436, &mut x437, 0x0, x403, x419);
776 let mut x438: u32 = 0;
777 let mut x439: fiat_p224_u1 = 0;
778 fiat_p224_addcarryx_u32(&mut x438, &mut x439, x437, x405, (0x0 as u32));
779 let mut x440: u32 = 0;
780 let mut x441: fiat_p224_u1 = 0;
781 fiat_p224_addcarryx_u32(&mut x440, &mut x441, x439, x407, (0x0 as u32));
782 let mut x442: u32 = 0;
783 let mut x443: fiat_p224_u1 = 0;
784 fiat_p224_addcarryx_u32(&mut x442, &mut x443, x441, x409, x427);
785 let mut x444: u32 = 0;
786 let mut x445: fiat_p224_u1 = 0;
787 fiat_p224_addcarryx_u32(&mut x444, &mut x445, x443, x411, x429);
788 let mut x446: u32 = 0;
789 let mut x447: fiat_p224_u1 = 0;
790 fiat_p224_addcarryx_u32(&mut x446, &mut x447, x445, x413, x431);
791 let mut x448: u32 = 0;
792 let mut x449: fiat_p224_u1 = 0;
793 fiat_p224_addcarryx_u32(&mut x448, &mut x449, x447, x415, x433);
794 let mut x450: u32 = 0;
795 let mut x451: fiat_p224_u1 = 0;
796 fiat_p224_addcarryx_u32(&mut x450, &mut x451, x449, x417, x435);
797 let x452: u32 = ((x451 as u32) + (x418 as u32));
798 let mut x453: u32 = 0;
799 let mut x454: u32 = 0;
800 fiat_p224_mulx_u32(&mut x453, &mut x454, x6, (arg2[6]));
801 let mut x455: u32 = 0;
802 let mut x456: u32 = 0;
803 fiat_p224_mulx_u32(&mut x455, &mut x456, x6, (arg2[5]));
804 let mut x457: u32 = 0;
805 let mut x458: u32 = 0;
806 fiat_p224_mulx_u32(&mut x457, &mut x458, x6, (arg2[4]));
807 let mut x459: u32 = 0;
808 let mut x460: u32 = 0;
809 fiat_p224_mulx_u32(&mut x459, &mut x460, x6, (arg2[3]));
810 let mut x461: u32 = 0;
811 let mut x462: u32 = 0;
812 fiat_p224_mulx_u32(&mut x461, &mut x462, x6, (arg2[2]));
813 let mut x463: u32 = 0;
814 let mut x464: u32 = 0;
815 fiat_p224_mulx_u32(&mut x463, &mut x464, x6, (arg2[1]));
816 let mut x465: u32 = 0;
817 let mut x466: u32 = 0;
818 fiat_p224_mulx_u32(&mut x465, &mut x466, x6, (arg2[0]));
819 let mut x467: u32 = 0;
820 let mut x468: fiat_p224_u1 = 0;
821 fiat_p224_addcarryx_u32(&mut x467, &mut x468, 0x0, x466, x463);
822 let mut x469: u32 = 0;
823 let mut x470: fiat_p224_u1 = 0;
824 fiat_p224_addcarryx_u32(&mut x469, &mut x470, x468, x464, x461);
825 let mut x471: u32 = 0;
826 let mut x472: fiat_p224_u1 = 0;
827 fiat_p224_addcarryx_u32(&mut x471, &mut x472, x470, x462, x459);
828 let mut x473: u32 = 0;
829 let mut x474: fiat_p224_u1 = 0;
830 fiat_p224_addcarryx_u32(&mut x473, &mut x474, x472, x460, x457);
831 let mut x475: u32 = 0;
832 let mut x476: fiat_p224_u1 = 0;
833 fiat_p224_addcarryx_u32(&mut x475, &mut x476, x474, x458, x455);
834 let mut x477: u32 = 0;
835 let mut x478: fiat_p224_u1 = 0;
836 fiat_p224_addcarryx_u32(&mut x477, &mut x478, x476, x456, x453);
837 let x479: u32 = ((x478 as u32) + x454);
838 let mut x480: u32 = 0;
839 let mut x481: fiat_p224_u1 = 0;
840 fiat_p224_addcarryx_u32(&mut x480, &mut x481, 0x0, x438, x465);
841 let mut x482: u32 = 0;
842 let mut x483: fiat_p224_u1 = 0;
843 fiat_p224_addcarryx_u32(&mut x482, &mut x483, x481, x440, x467);
844 let mut x484: u32 = 0;
845 let mut x485: fiat_p224_u1 = 0;
846 fiat_p224_addcarryx_u32(&mut x484, &mut x485, x483, x442, x469);
847 let mut x486: u32 = 0;
848 let mut x487: fiat_p224_u1 = 0;
849 fiat_p224_addcarryx_u32(&mut x486, &mut x487, x485, x444, x471);
850 let mut x488: u32 = 0;
851 let mut x489: fiat_p224_u1 = 0;
852 fiat_p224_addcarryx_u32(&mut x488, &mut x489, x487, x446, x473);
853 let mut x490: u32 = 0;
854 let mut x491: fiat_p224_u1 = 0;
855 fiat_p224_addcarryx_u32(&mut x490, &mut x491, x489, x448, x475);
856 let mut x492: u32 = 0;
857 let mut x493: fiat_p224_u1 = 0;
858 fiat_p224_addcarryx_u32(&mut x492, &mut x493, x491, x450, x477);
859 let mut x494: u32 = 0;
860 let mut x495: fiat_p224_u1 = 0;
861 fiat_p224_addcarryx_u32(&mut x494, &mut x495, x493, x452, x479);
862 let mut x496: u32 = 0;
863 let mut x497: u32 = 0;
864 fiat_p224_mulx_u32(&mut x496, &mut x497, x480, 0xffffffff);
865 let mut x498: u32 = 0;
866 let mut x499: u32 = 0;
867 fiat_p224_mulx_u32(&mut x498, &mut x499, x496, 0xffffffff);
868 let mut x500: u32 = 0;
869 let mut x501: u32 = 0;
870 fiat_p224_mulx_u32(&mut x500, &mut x501, x496, 0xffffffff);
871 let mut x502: u32 = 0;
872 let mut x503: u32 = 0;
873 fiat_p224_mulx_u32(&mut x502, &mut x503, x496, 0xffffffff);
874 let mut x504: u32 = 0;
875 let mut x505: u32 = 0;
876 fiat_p224_mulx_u32(&mut x504, &mut x505, x496, 0xffffffff);
877 let mut x506: u32 = 0;
878 let mut x507: fiat_p224_u1 = 0;
879 fiat_p224_addcarryx_u32(&mut x506, &mut x507, 0x0, x505, x502);
880 let mut x508: u32 = 0;
881 let mut x509: fiat_p224_u1 = 0;
882 fiat_p224_addcarryx_u32(&mut x508, &mut x509, x507, x503, x500);
883 let mut x510: u32 = 0;
884 let mut x511: fiat_p224_u1 = 0;
885 fiat_p224_addcarryx_u32(&mut x510, &mut x511, x509, x501, x498);
886 let x512: u32 = ((x511 as u32) + x499);
887 let mut x513: u32 = 0;
888 let mut x514: fiat_p224_u1 = 0;
889 fiat_p224_addcarryx_u32(&mut x513, &mut x514, 0x0, x480, x496);
890 let mut x515: u32 = 0;
891 let mut x516: fiat_p224_u1 = 0;
892 fiat_p224_addcarryx_u32(&mut x515, &mut x516, x514, x482, (0x0 as u32));
893 let mut x517: u32 = 0;
894 let mut x518: fiat_p224_u1 = 0;
895 fiat_p224_addcarryx_u32(&mut x517, &mut x518, x516, x484, (0x0 as u32));
896 let mut x519: u32 = 0;
897 let mut x520: fiat_p224_u1 = 0;
898 fiat_p224_addcarryx_u32(&mut x519, &mut x520, x518, x486, x504);
899 let mut x521: u32 = 0;
900 let mut x522: fiat_p224_u1 = 0;
901 fiat_p224_addcarryx_u32(&mut x521, &mut x522, x520, x488, x506);
902 let mut x523: u32 = 0;
903 let mut x524: fiat_p224_u1 = 0;
904 fiat_p224_addcarryx_u32(&mut x523, &mut x524, x522, x490, x508);
905 let mut x525: u32 = 0;
906 let mut x526: fiat_p224_u1 = 0;
907 fiat_p224_addcarryx_u32(&mut x525, &mut x526, x524, x492, x510);
908 let mut x527: u32 = 0;
909 let mut x528: fiat_p224_u1 = 0;
910 fiat_p224_addcarryx_u32(&mut x527, &mut x528, x526, x494, x512);
911 let x529: u32 = ((x528 as u32) + (x495 as u32));
912 let mut x530: u32 = 0;
913 let mut x531: fiat_p224_u1 = 0;
914 fiat_p224_subborrowx_u32(&mut x530, &mut x531, 0x0, x515, (0x1 as u32));
915 let mut x532: u32 = 0;
916 let mut x533: fiat_p224_u1 = 0;
917 fiat_p224_subborrowx_u32(&mut x532, &mut x533, x531, x517, (0x0 as u32));
918 let mut x534: u32 = 0;
919 let mut x535: fiat_p224_u1 = 0;
920 fiat_p224_subborrowx_u32(&mut x534, &mut x535, x533, x519, (0x0 as u32));
921 let mut x536: u32 = 0;
922 let mut x537: fiat_p224_u1 = 0;
923 fiat_p224_subborrowx_u32(&mut x536, &mut x537, x535, x521, 0xffffffff);
924 let mut x538: u32 = 0;
925 let mut x539: fiat_p224_u1 = 0;
926 fiat_p224_subborrowx_u32(&mut x538, &mut x539, x537, x523, 0xffffffff);
927 let mut x540: u32 = 0;
928 let mut x541: fiat_p224_u1 = 0;
929 fiat_p224_subborrowx_u32(&mut x540, &mut x541, x539, x525, 0xffffffff);
930 let mut x542: u32 = 0;
931 let mut x543: fiat_p224_u1 = 0;
932 fiat_p224_subborrowx_u32(&mut x542, &mut x543, x541, x527, 0xffffffff);
933 let mut x544: u32 = 0;
934 let mut x545: fiat_p224_u1 = 0;
935 fiat_p224_subborrowx_u32(&mut x544, &mut x545, x543, x529, (0x0 as u32));
936 let mut x546: u32 = 0;
937 fiat_p224_cmovznz_u32(&mut x546, x545, x530, x515);
938 let mut x547: u32 = 0;
939 fiat_p224_cmovznz_u32(&mut x547, x545, x532, x517);
940 let mut x548: u32 = 0;
941 fiat_p224_cmovznz_u32(&mut x548, x545, x534, x519);
942 let mut x549: u32 = 0;
943 fiat_p224_cmovznz_u32(&mut x549, x545, x536, x521);
944 let mut x550: u32 = 0;
945 fiat_p224_cmovznz_u32(&mut x550, x545, x538, x523);
946 let mut x551: u32 = 0;
947 fiat_p224_cmovznz_u32(&mut x551, x545, x540, x525);
948 let mut x552: u32 = 0;
949 fiat_p224_cmovznz_u32(&mut x552, x545, x542, x527);
950 out1[0] = x546;
951 out1[1] = x547;
952 out1[2] = x548;
953 out1[3] = x549;
954 out1[4] = x550;
955 out1[5] = x551;
956 out1[6] = x552;
957}
958
959/// The function fiat_p224_square squares a field element in the Montgomery domain.
960///
961/// Preconditions:
962/// 0 ≤ eval arg1 < m
963/// Postconditions:
964/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg1)) mod m
965/// 0 ≤ eval out1 < m
966///
967#[inline]
968pub fn fiat_p224_square(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element) -> () {
969 let x1: u32 = (arg1[1]);
970 let x2: u32 = (arg1[2]);
971 let x3: u32 = (arg1[3]);
972 let x4: u32 = (arg1[4]);
973 let x5: u32 = (arg1[5]);
974 let x6: u32 = (arg1[6]);
975 let x7: u32 = (arg1[0]);
976 let mut x8: u32 = 0;
977 let mut x9: u32 = 0;
978 fiat_p224_mulx_u32(&mut x8, &mut x9, x7, (arg1[6]));
979 let mut x10: u32 = 0;
980 let mut x11: u32 = 0;
981 fiat_p224_mulx_u32(&mut x10, &mut x11, x7, (arg1[5]));
982 let mut x12: u32 = 0;
983 let mut x13: u32 = 0;
984 fiat_p224_mulx_u32(&mut x12, &mut x13, x7, (arg1[4]));
985 let mut x14: u32 = 0;
986 let mut x15: u32 = 0;
987 fiat_p224_mulx_u32(&mut x14, &mut x15, x7, (arg1[3]));
988 let mut x16: u32 = 0;
989 let mut x17: u32 = 0;
990 fiat_p224_mulx_u32(&mut x16, &mut x17, x7, (arg1[2]));
991 let mut x18: u32 = 0;
992 let mut x19: u32 = 0;
993 fiat_p224_mulx_u32(&mut x18, &mut x19, x7, (arg1[1]));
994 let mut x20: u32 = 0;
995 let mut x21: u32 = 0;
996 fiat_p224_mulx_u32(&mut x20, &mut x21, x7, (arg1[0]));
997 let mut x22: u32 = 0;
998 let mut x23: fiat_p224_u1 = 0;
999 fiat_p224_addcarryx_u32(&mut x22, &mut x23, 0x0, x21, x18);
1000 let mut x24: u32 = 0;
1001 let mut x25: fiat_p224_u1 = 0;
1002 fiat_p224_addcarryx_u32(&mut x24, &mut x25, x23, x19, x16);
1003 let mut x26: u32 = 0;
1004 let mut x27: fiat_p224_u1 = 0;
1005 fiat_p224_addcarryx_u32(&mut x26, &mut x27, x25, x17, x14);
1006 let mut x28: u32 = 0;
1007 let mut x29: fiat_p224_u1 = 0;
1008 fiat_p224_addcarryx_u32(&mut x28, &mut x29, x27, x15, x12);
1009 let mut x30: u32 = 0;
1010 let mut x31: fiat_p224_u1 = 0;
1011 fiat_p224_addcarryx_u32(&mut x30, &mut x31, x29, x13, x10);
1012 let mut x32: u32 = 0;
1013 let mut x33: fiat_p224_u1 = 0;
1014 fiat_p224_addcarryx_u32(&mut x32, &mut x33, x31, x11, x8);
1015 let x34: u32 = ((x33 as u32) + x9);
1016 let mut x35: u32 = 0;
1017 let mut x36: u32 = 0;
1018 fiat_p224_mulx_u32(&mut x35, &mut x36, x20, 0xffffffff);
1019 let mut x37: u32 = 0;
1020 let mut x38: u32 = 0;
1021 fiat_p224_mulx_u32(&mut x37, &mut x38, x35, 0xffffffff);
1022 let mut x39: u32 = 0;
1023 let mut x40: u32 = 0;
1024 fiat_p224_mulx_u32(&mut x39, &mut x40, x35, 0xffffffff);
1025 let mut x41: u32 = 0;
1026 let mut x42: u32 = 0;
1027 fiat_p224_mulx_u32(&mut x41, &mut x42, x35, 0xffffffff);
1028 let mut x43: u32 = 0;
1029 let mut x44: u32 = 0;
1030 fiat_p224_mulx_u32(&mut x43, &mut x44, x35, 0xffffffff);
1031 let mut x45: u32 = 0;
1032 let mut x46: fiat_p224_u1 = 0;
1033 fiat_p224_addcarryx_u32(&mut x45, &mut x46, 0x0, x44, x41);
1034 let mut x47: u32 = 0;
1035 let mut x48: fiat_p224_u1 = 0;
1036 fiat_p224_addcarryx_u32(&mut x47, &mut x48, x46, x42, x39);
1037 let mut x49: u32 = 0;
1038 let mut x50: fiat_p224_u1 = 0;
1039 fiat_p224_addcarryx_u32(&mut x49, &mut x50, x48, x40, x37);
1040 let x51: u32 = ((x50 as u32) + x38);
1041 let mut x52: u32 = 0;
1042 let mut x53: fiat_p224_u1 = 0;
1043 fiat_p224_addcarryx_u32(&mut x52, &mut x53, 0x0, x20, x35);
1044 let mut x54: u32 = 0;
1045 let mut x55: fiat_p224_u1 = 0;
1046 fiat_p224_addcarryx_u32(&mut x54, &mut x55, x53, x22, (0x0 as u32));
1047 let mut x56: u32 = 0;
1048 let mut x57: fiat_p224_u1 = 0;
1049 fiat_p224_addcarryx_u32(&mut x56, &mut x57, x55, x24, (0x0 as u32));
1050 let mut x58: u32 = 0;
1051 let mut x59: fiat_p224_u1 = 0;
1052 fiat_p224_addcarryx_u32(&mut x58, &mut x59, x57, x26, x43);
1053 let mut x60: u32 = 0;
1054 let mut x61: fiat_p224_u1 = 0;
1055 fiat_p224_addcarryx_u32(&mut x60, &mut x61, x59, x28, x45);
1056 let mut x62: u32 = 0;
1057 let mut x63: fiat_p224_u1 = 0;
1058 fiat_p224_addcarryx_u32(&mut x62, &mut x63, x61, x30, x47);
1059 let mut x64: u32 = 0;
1060 let mut x65: fiat_p224_u1 = 0;
1061 fiat_p224_addcarryx_u32(&mut x64, &mut x65, x63, x32, x49);
1062 let mut x66: u32 = 0;
1063 let mut x67: fiat_p224_u1 = 0;
1064 fiat_p224_addcarryx_u32(&mut x66, &mut x67, x65, x34, x51);
1065 let mut x68: u32 = 0;
1066 let mut x69: u32 = 0;
1067 fiat_p224_mulx_u32(&mut x68, &mut x69, x1, (arg1[6]));
1068 let mut x70: u32 = 0;
1069 let mut x71: u32 = 0;
1070 fiat_p224_mulx_u32(&mut x70, &mut x71, x1, (arg1[5]));
1071 let mut x72: u32 = 0;
1072 let mut x73: u32 = 0;
1073 fiat_p224_mulx_u32(&mut x72, &mut x73, x1, (arg1[4]));
1074 let mut x74: u32 = 0;
1075 let mut x75: u32 = 0;
1076 fiat_p224_mulx_u32(&mut x74, &mut x75, x1, (arg1[3]));
1077 let mut x76: u32 = 0;
1078 let mut x77: u32 = 0;
1079 fiat_p224_mulx_u32(&mut x76, &mut x77, x1, (arg1[2]));
1080 let mut x78: u32 = 0;
1081 let mut x79: u32 = 0;
1082 fiat_p224_mulx_u32(&mut x78, &mut x79, x1, (arg1[1]));
1083 let mut x80: u32 = 0;
1084 let mut x81: u32 = 0;
1085 fiat_p224_mulx_u32(&mut x80, &mut x81, x1, (arg1[0]));
1086 let mut x82: u32 = 0;
1087 let mut x83: fiat_p224_u1 = 0;
1088 fiat_p224_addcarryx_u32(&mut x82, &mut x83, 0x0, x81, x78);
1089 let mut x84: u32 = 0;
1090 let mut x85: fiat_p224_u1 = 0;
1091 fiat_p224_addcarryx_u32(&mut x84, &mut x85, x83, x79, x76);
1092 let mut x86: u32 = 0;
1093 let mut x87: fiat_p224_u1 = 0;
1094 fiat_p224_addcarryx_u32(&mut x86, &mut x87, x85, x77, x74);
1095 let mut x88: u32 = 0;
1096 let mut x89: fiat_p224_u1 = 0;
1097 fiat_p224_addcarryx_u32(&mut x88, &mut x89, x87, x75, x72);
1098 let mut x90: u32 = 0;
1099 let mut x91: fiat_p224_u1 = 0;
1100 fiat_p224_addcarryx_u32(&mut x90, &mut x91, x89, x73, x70);
1101 let mut x92: u32 = 0;
1102 let mut x93: fiat_p224_u1 = 0;
1103 fiat_p224_addcarryx_u32(&mut x92, &mut x93, x91, x71, x68);
1104 let x94: u32 = ((x93 as u32) + x69);
1105 let mut x95: u32 = 0;
1106 let mut x96: fiat_p224_u1 = 0;
1107 fiat_p224_addcarryx_u32(&mut x95, &mut x96, 0x0, x54, x80);
1108 let mut x97: u32 = 0;
1109 let mut x98: fiat_p224_u1 = 0;
1110 fiat_p224_addcarryx_u32(&mut x97, &mut x98, x96, x56, x82);
1111 let mut x99: u32 = 0;
1112 let mut x100: fiat_p224_u1 = 0;
1113 fiat_p224_addcarryx_u32(&mut x99, &mut x100, x98, x58, x84);
1114 let mut x101: u32 = 0;
1115 let mut x102: fiat_p224_u1 = 0;
1116 fiat_p224_addcarryx_u32(&mut x101, &mut x102, x100, x60, x86);
1117 let mut x103: u32 = 0;
1118 let mut x104: fiat_p224_u1 = 0;
1119 fiat_p224_addcarryx_u32(&mut x103, &mut x104, x102, x62, x88);
1120 let mut x105: u32 = 0;
1121 let mut x106: fiat_p224_u1 = 0;
1122 fiat_p224_addcarryx_u32(&mut x105, &mut x106, x104, x64, x90);
1123 let mut x107: u32 = 0;
1124 let mut x108: fiat_p224_u1 = 0;
1125 fiat_p224_addcarryx_u32(&mut x107, &mut x108, x106, x66, x92);
1126 let mut x109: u32 = 0;
1127 let mut x110: fiat_p224_u1 = 0;
1128 fiat_p224_addcarryx_u32(&mut x109, &mut x110, x108, (x67 as u32), x94);
1129 let mut x111: u32 = 0;
1130 let mut x112: u32 = 0;
1131 fiat_p224_mulx_u32(&mut x111, &mut x112, x95, 0xffffffff);
1132 let mut x113: u32 = 0;
1133 let mut x114: u32 = 0;
1134 fiat_p224_mulx_u32(&mut x113, &mut x114, x111, 0xffffffff);
1135 let mut x115: u32 = 0;
1136 let mut x116: u32 = 0;
1137 fiat_p224_mulx_u32(&mut x115, &mut x116, x111, 0xffffffff);
1138 let mut x117: u32 = 0;
1139 let mut x118: u32 = 0;
1140 fiat_p224_mulx_u32(&mut x117, &mut x118, x111, 0xffffffff);
1141 let mut x119: u32 = 0;
1142 let mut x120: u32 = 0;
1143 fiat_p224_mulx_u32(&mut x119, &mut x120, x111, 0xffffffff);
1144 let mut x121: u32 = 0;
1145 let mut x122: fiat_p224_u1 = 0;
1146 fiat_p224_addcarryx_u32(&mut x121, &mut x122, 0x0, x120, x117);
1147 let mut x123: u32 = 0;
1148 let mut x124: fiat_p224_u1 = 0;
1149 fiat_p224_addcarryx_u32(&mut x123, &mut x124, x122, x118, x115);
1150 let mut x125: u32 = 0;
1151 let mut x126: fiat_p224_u1 = 0;
1152 fiat_p224_addcarryx_u32(&mut x125, &mut x126, x124, x116, x113);
1153 let x127: u32 = ((x126 as u32) + x114);
1154 let mut x128: u32 = 0;
1155 let mut x129: fiat_p224_u1 = 0;
1156 fiat_p224_addcarryx_u32(&mut x128, &mut x129, 0x0, x95, x111);
1157 let mut x130: u32 = 0;
1158 let mut x131: fiat_p224_u1 = 0;
1159 fiat_p224_addcarryx_u32(&mut x130, &mut x131, x129, x97, (0x0 as u32));
1160 let mut x132: u32 = 0;
1161 let mut x133: fiat_p224_u1 = 0;
1162 fiat_p224_addcarryx_u32(&mut x132, &mut x133, x131, x99, (0x0 as u32));
1163 let mut x134: u32 = 0;
1164 let mut x135: fiat_p224_u1 = 0;
1165 fiat_p224_addcarryx_u32(&mut x134, &mut x135, x133, x101, x119);
1166 let mut x136: u32 = 0;
1167 let mut x137: fiat_p224_u1 = 0;
1168 fiat_p224_addcarryx_u32(&mut x136, &mut x137, x135, x103, x121);
1169 let mut x138: u32 = 0;
1170 let mut x139: fiat_p224_u1 = 0;
1171 fiat_p224_addcarryx_u32(&mut x138, &mut x139, x137, x105, x123);
1172 let mut x140: u32 = 0;
1173 let mut x141: fiat_p224_u1 = 0;
1174 fiat_p224_addcarryx_u32(&mut x140, &mut x141, x139, x107, x125);
1175 let mut x142: u32 = 0;
1176 let mut x143: fiat_p224_u1 = 0;
1177 fiat_p224_addcarryx_u32(&mut x142, &mut x143, x141, x109, x127);
1178 let x144: u32 = ((x143 as u32) + (x110 as u32));
1179 let mut x145: u32 = 0;
1180 let mut x146: u32 = 0;
1181 fiat_p224_mulx_u32(&mut x145, &mut x146, x2, (arg1[6]));
1182 let mut x147: u32 = 0;
1183 let mut x148: u32 = 0;
1184 fiat_p224_mulx_u32(&mut x147, &mut x148, x2, (arg1[5]));
1185 let mut x149: u32 = 0;
1186 let mut x150: u32 = 0;
1187 fiat_p224_mulx_u32(&mut x149, &mut x150, x2, (arg1[4]));
1188 let mut x151: u32 = 0;
1189 let mut x152: u32 = 0;
1190 fiat_p224_mulx_u32(&mut x151, &mut x152, x2, (arg1[3]));
1191 let mut x153: u32 = 0;
1192 let mut x154: u32 = 0;
1193 fiat_p224_mulx_u32(&mut x153, &mut x154, x2, (arg1[2]));
1194 let mut x155: u32 = 0;
1195 let mut x156: u32 = 0;
1196 fiat_p224_mulx_u32(&mut x155, &mut x156, x2, (arg1[1]));
1197 let mut x157: u32 = 0;
1198 let mut x158: u32 = 0;
1199 fiat_p224_mulx_u32(&mut x157, &mut x158, x2, (arg1[0]));
1200 let mut x159: u32 = 0;
1201 let mut x160: fiat_p224_u1 = 0;
1202 fiat_p224_addcarryx_u32(&mut x159, &mut x160, 0x0, x158, x155);
1203 let mut x161: u32 = 0;
1204 let mut x162: fiat_p224_u1 = 0;
1205 fiat_p224_addcarryx_u32(&mut x161, &mut x162, x160, x156, x153);
1206 let mut x163: u32 = 0;
1207 let mut x164: fiat_p224_u1 = 0;
1208 fiat_p224_addcarryx_u32(&mut x163, &mut x164, x162, x154, x151);
1209 let mut x165: u32 = 0;
1210 let mut x166: fiat_p224_u1 = 0;
1211 fiat_p224_addcarryx_u32(&mut x165, &mut x166, x164, x152, x149);
1212 let mut x167: u32 = 0;
1213 let mut x168: fiat_p224_u1 = 0;
1214 fiat_p224_addcarryx_u32(&mut x167, &mut x168, x166, x150, x147);
1215 let mut x169: u32 = 0;
1216 let mut x170: fiat_p224_u1 = 0;
1217 fiat_p224_addcarryx_u32(&mut x169, &mut x170, x168, x148, x145);
1218 let x171: u32 = ((x170 as u32) + x146);
1219 let mut x172: u32 = 0;
1220 let mut x173: fiat_p224_u1 = 0;
1221 fiat_p224_addcarryx_u32(&mut x172, &mut x173, 0x0, x130, x157);
1222 let mut x174: u32 = 0;
1223 let mut x175: fiat_p224_u1 = 0;
1224 fiat_p224_addcarryx_u32(&mut x174, &mut x175, x173, x132, x159);
1225 let mut x176: u32 = 0;
1226 let mut x177: fiat_p224_u1 = 0;
1227 fiat_p224_addcarryx_u32(&mut x176, &mut x177, x175, x134, x161);
1228 let mut x178: u32 = 0;
1229 let mut x179: fiat_p224_u1 = 0;
1230 fiat_p224_addcarryx_u32(&mut x178, &mut x179, x177, x136, x163);
1231 let mut x180: u32 = 0;
1232 let mut x181: fiat_p224_u1 = 0;
1233 fiat_p224_addcarryx_u32(&mut x180, &mut x181, x179, x138, x165);
1234 let mut x182: u32 = 0;
1235 let mut x183: fiat_p224_u1 = 0;
1236 fiat_p224_addcarryx_u32(&mut x182, &mut x183, x181, x140, x167);
1237 let mut x184: u32 = 0;
1238 let mut x185: fiat_p224_u1 = 0;
1239 fiat_p224_addcarryx_u32(&mut x184, &mut x185, x183, x142, x169);
1240 let mut x186: u32 = 0;
1241 let mut x187: fiat_p224_u1 = 0;
1242 fiat_p224_addcarryx_u32(&mut x186, &mut x187, x185, x144, x171);
1243 let mut x188: u32 = 0;
1244 let mut x189: u32 = 0;
1245 fiat_p224_mulx_u32(&mut x188, &mut x189, x172, 0xffffffff);
1246 let mut x190: u32 = 0;
1247 let mut x191: u32 = 0;
1248 fiat_p224_mulx_u32(&mut x190, &mut x191, x188, 0xffffffff);
1249 let mut x192: u32 = 0;
1250 let mut x193: u32 = 0;
1251 fiat_p224_mulx_u32(&mut x192, &mut x193, x188, 0xffffffff);
1252 let mut x194: u32 = 0;
1253 let mut x195: u32 = 0;
1254 fiat_p224_mulx_u32(&mut x194, &mut x195, x188, 0xffffffff);
1255 let mut x196: u32 = 0;
1256 let mut x197: u32 = 0;
1257 fiat_p224_mulx_u32(&mut x196, &mut x197, x188, 0xffffffff);
1258 let mut x198: u32 = 0;
1259 let mut x199: fiat_p224_u1 = 0;
1260 fiat_p224_addcarryx_u32(&mut x198, &mut x199, 0x0, x197, x194);
1261 let mut x200: u32 = 0;
1262 let mut x201: fiat_p224_u1 = 0;
1263 fiat_p224_addcarryx_u32(&mut x200, &mut x201, x199, x195, x192);
1264 let mut x202: u32 = 0;
1265 let mut x203: fiat_p224_u1 = 0;
1266 fiat_p224_addcarryx_u32(&mut x202, &mut x203, x201, x193, x190);
1267 let x204: u32 = ((x203 as u32) + x191);
1268 let mut x205: u32 = 0;
1269 let mut x206: fiat_p224_u1 = 0;
1270 fiat_p224_addcarryx_u32(&mut x205, &mut x206, 0x0, x172, x188);
1271 let mut x207: u32 = 0;
1272 let mut x208: fiat_p224_u1 = 0;
1273 fiat_p224_addcarryx_u32(&mut x207, &mut x208, x206, x174, (0x0 as u32));
1274 let mut x209: u32 = 0;
1275 let mut x210: fiat_p224_u1 = 0;
1276 fiat_p224_addcarryx_u32(&mut x209, &mut x210, x208, x176, (0x0 as u32));
1277 let mut x211: u32 = 0;
1278 let mut x212: fiat_p224_u1 = 0;
1279 fiat_p224_addcarryx_u32(&mut x211, &mut x212, x210, x178, x196);
1280 let mut x213: u32 = 0;
1281 let mut x214: fiat_p224_u1 = 0;
1282 fiat_p224_addcarryx_u32(&mut x213, &mut x214, x212, x180, x198);
1283 let mut x215: u32 = 0;
1284 let mut x216: fiat_p224_u1 = 0;
1285 fiat_p224_addcarryx_u32(&mut x215, &mut x216, x214, x182, x200);
1286 let mut x217: u32 = 0;
1287 let mut x218: fiat_p224_u1 = 0;
1288 fiat_p224_addcarryx_u32(&mut x217, &mut x218, x216, x184, x202);
1289 let mut x219: u32 = 0;
1290 let mut x220: fiat_p224_u1 = 0;
1291 fiat_p224_addcarryx_u32(&mut x219, &mut x220, x218, x186, x204);
1292 let x221: u32 = ((x220 as u32) + (x187 as u32));
1293 let mut x222: u32 = 0;
1294 let mut x223: u32 = 0;
1295 fiat_p224_mulx_u32(&mut x222, &mut x223, x3, (arg1[6]));
1296 let mut x224: u32 = 0;
1297 let mut x225: u32 = 0;
1298 fiat_p224_mulx_u32(&mut x224, &mut x225, x3, (arg1[5]));
1299 let mut x226: u32 = 0;
1300 let mut x227: u32 = 0;
1301 fiat_p224_mulx_u32(&mut x226, &mut x227, x3, (arg1[4]));
1302 let mut x228: u32 = 0;
1303 let mut x229: u32 = 0;
1304 fiat_p224_mulx_u32(&mut x228, &mut x229, x3, (arg1[3]));
1305 let mut x230: u32 = 0;
1306 let mut x231: u32 = 0;
1307 fiat_p224_mulx_u32(&mut x230, &mut x231, x3, (arg1[2]));
1308 let mut x232: u32 = 0;
1309 let mut x233: u32 = 0;
1310 fiat_p224_mulx_u32(&mut x232, &mut x233, x3, (arg1[1]));
1311 let mut x234: u32 = 0;
1312 let mut x235: u32 = 0;
1313 fiat_p224_mulx_u32(&mut x234, &mut x235, x3, (arg1[0]));
1314 let mut x236: u32 = 0;
1315 let mut x237: fiat_p224_u1 = 0;
1316 fiat_p224_addcarryx_u32(&mut x236, &mut x237, 0x0, x235, x232);
1317 let mut x238: u32 = 0;
1318 let mut x239: fiat_p224_u1 = 0;
1319 fiat_p224_addcarryx_u32(&mut x238, &mut x239, x237, x233, x230);
1320 let mut x240: u32 = 0;
1321 let mut x241: fiat_p224_u1 = 0;
1322 fiat_p224_addcarryx_u32(&mut x240, &mut x241, x239, x231, x228);
1323 let mut x242: u32 = 0;
1324 let mut x243: fiat_p224_u1 = 0;
1325 fiat_p224_addcarryx_u32(&mut x242, &mut x243, x241, x229, x226);
1326 let mut x244: u32 = 0;
1327 let mut x245: fiat_p224_u1 = 0;
1328 fiat_p224_addcarryx_u32(&mut x244, &mut x245, x243, x227, x224);
1329 let mut x246: u32 = 0;
1330 let mut x247: fiat_p224_u1 = 0;
1331 fiat_p224_addcarryx_u32(&mut x246, &mut x247, x245, x225, x222);
1332 let x248: u32 = ((x247 as u32) + x223);
1333 let mut x249: u32 = 0;
1334 let mut x250: fiat_p224_u1 = 0;
1335 fiat_p224_addcarryx_u32(&mut x249, &mut x250, 0x0, x207, x234);
1336 let mut x251: u32 = 0;
1337 let mut x252: fiat_p224_u1 = 0;
1338 fiat_p224_addcarryx_u32(&mut x251, &mut x252, x250, x209, x236);
1339 let mut x253: u32 = 0;
1340 let mut x254: fiat_p224_u1 = 0;
1341 fiat_p224_addcarryx_u32(&mut x253, &mut x254, x252, x211, x238);
1342 let mut x255: u32 = 0;
1343 let mut x256: fiat_p224_u1 = 0;
1344 fiat_p224_addcarryx_u32(&mut x255, &mut x256, x254, x213, x240);
1345 let mut x257: u32 = 0;
1346 let mut x258: fiat_p224_u1 = 0;
1347 fiat_p224_addcarryx_u32(&mut x257, &mut x258, x256, x215, x242);
1348 let mut x259: u32 = 0;
1349 let mut x260: fiat_p224_u1 = 0;
1350 fiat_p224_addcarryx_u32(&mut x259, &mut x260, x258, x217, x244);
1351 let mut x261: u32 = 0;
1352 let mut x262: fiat_p224_u1 = 0;
1353 fiat_p224_addcarryx_u32(&mut x261, &mut x262, x260, x219, x246);
1354 let mut x263: u32 = 0;
1355 let mut x264: fiat_p224_u1 = 0;
1356 fiat_p224_addcarryx_u32(&mut x263, &mut x264, x262, x221, x248);
1357 let mut x265: u32 = 0;
1358 let mut x266: u32 = 0;
1359 fiat_p224_mulx_u32(&mut x265, &mut x266, x249, 0xffffffff);
1360 let mut x267: u32 = 0;
1361 let mut x268: u32 = 0;
1362 fiat_p224_mulx_u32(&mut x267, &mut x268, x265, 0xffffffff);
1363 let mut x269: u32 = 0;
1364 let mut x270: u32 = 0;
1365 fiat_p224_mulx_u32(&mut x269, &mut x270, x265, 0xffffffff);
1366 let mut x271: u32 = 0;
1367 let mut x272: u32 = 0;
1368 fiat_p224_mulx_u32(&mut x271, &mut x272, x265, 0xffffffff);
1369 let mut x273: u32 = 0;
1370 let mut x274: u32 = 0;
1371 fiat_p224_mulx_u32(&mut x273, &mut x274, x265, 0xffffffff);
1372 let mut x275: u32 = 0;
1373 let mut x276: fiat_p224_u1 = 0;
1374 fiat_p224_addcarryx_u32(&mut x275, &mut x276, 0x0, x274, x271);
1375 let mut x277: u32 = 0;
1376 let mut x278: fiat_p224_u1 = 0;
1377 fiat_p224_addcarryx_u32(&mut x277, &mut x278, x276, x272, x269);
1378 let mut x279: u32 = 0;
1379 let mut x280: fiat_p224_u1 = 0;
1380 fiat_p224_addcarryx_u32(&mut x279, &mut x280, x278, x270, x267);
1381 let x281: u32 = ((x280 as u32) + x268);
1382 let mut x282: u32 = 0;
1383 let mut x283: fiat_p224_u1 = 0;
1384 fiat_p224_addcarryx_u32(&mut x282, &mut x283, 0x0, x249, x265);
1385 let mut x284: u32 = 0;
1386 let mut x285: fiat_p224_u1 = 0;
1387 fiat_p224_addcarryx_u32(&mut x284, &mut x285, x283, x251, (0x0 as u32));
1388 let mut x286: u32 = 0;
1389 let mut x287: fiat_p224_u1 = 0;
1390 fiat_p224_addcarryx_u32(&mut x286, &mut x287, x285, x253, (0x0 as u32));
1391 let mut x288: u32 = 0;
1392 let mut x289: fiat_p224_u1 = 0;
1393 fiat_p224_addcarryx_u32(&mut x288, &mut x289, x287, x255, x273);
1394 let mut x290: u32 = 0;
1395 let mut x291: fiat_p224_u1 = 0;
1396 fiat_p224_addcarryx_u32(&mut x290, &mut x291, x289, x257, x275);
1397 let mut x292: u32 = 0;
1398 let mut x293: fiat_p224_u1 = 0;
1399 fiat_p224_addcarryx_u32(&mut x292, &mut x293, x291, x259, x277);
1400 let mut x294: u32 = 0;
1401 let mut x295: fiat_p224_u1 = 0;
1402 fiat_p224_addcarryx_u32(&mut x294, &mut x295, x293, x261, x279);
1403 let mut x296: u32 = 0;
1404 let mut x297: fiat_p224_u1 = 0;
1405 fiat_p224_addcarryx_u32(&mut x296, &mut x297, x295, x263, x281);
1406 let x298: u32 = ((x297 as u32) + (x264 as u32));
1407 let mut x299: u32 = 0;
1408 let mut x300: u32 = 0;
1409 fiat_p224_mulx_u32(&mut x299, &mut x300, x4, (arg1[6]));
1410 let mut x301: u32 = 0;
1411 let mut x302: u32 = 0;
1412 fiat_p224_mulx_u32(&mut x301, &mut x302, x4, (arg1[5]));
1413 let mut x303: u32 = 0;
1414 let mut x304: u32 = 0;
1415 fiat_p224_mulx_u32(&mut x303, &mut x304, x4, (arg1[4]));
1416 let mut x305: u32 = 0;
1417 let mut x306: u32 = 0;
1418 fiat_p224_mulx_u32(&mut x305, &mut x306, x4, (arg1[3]));
1419 let mut x307: u32 = 0;
1420 let mut x308: u32 = 0;
1421 fiat_p224_mulx_u32(&mut x307, &mut x308, x4, (arg1[2]));
1422 let mut x309: u32 = 0;
1423 let mut x310: u32 = 0;
1424 fiat_p224_mulx_u32(&mut x309, &mut x310, x4, (arg1[1]));
1425 let mut x311: u32 = 0;
1426 let mut x312: u32 = 0;
1427 fiat_p224_mulx_u32(&mut x311, &mut x312, x4, (arg1[0]));
1428 let mut x313: u32 = 0;
1429 let mut x314: fiat_p224_u1 = 0;
1430 fiat_p224_addcarryx_u32(&mut x313, &mut x314, 0x0, x312, x309);
1431 let mut x315: u32 = 0;
1432 let mut x316: fiat_p224_u1 = 0;
1433 fiat_p224_addcarryx_u32(&mut x315, &mut x316, x314, x310, x307);
1434 let mut x317: u32 = 0;
1435 let mut x318: fiat_p224_u1 = 0;
1436 fiat_p224_addcarryx_u32(&mut x317, &mut x318, x316, x308, x305);
1437 let mut x319: u32 = 0;
1438 let mut x320: fiat_p224_u1 = 0;
1439 fiat_p224_addcarryx_u32(&mut x319, &mut x320, x318, x306, x303);
1440 let mut x321: u32 = 0;
1441 let mut x322: fiat_p224_u1 = 0;
1442 fiat_p224_addcarryx_u32(&mut x321, &mut x322, x320, x304, x301);
1443 let mut x323: u32 = 0;
1444 let mut x324: fiat_p224_u1 = 0;
1445 fiat_p224_addcarryx_u32(&mut x323, &mut x324, x322, x302, x299);
1446 let x325: u32 = ((x324 as u32) + x300);
1447 let mut x326: u32 = 0;
1448 let mut x327: fiat_p224_u1 = 0;
1449 fiat_p224_addcarryx_u32(&mut x326, &mut x327, 0x0, x284, x311);
1450 let mut x328: u32 = 0;
1451 let mut x329: fiat_p224_u1 = 0;
1452 fiat_p224_addcarryx_u32(&mut x328, &mut x329, x327, x286, x313);
1453 let mut x330: u32 = 0;
1454 let mut x331: fiat_p224_u1 = 0;
1455 fiat_p224_addcarryx_u32(&mut x330, &mut x331, x329, x288, x315);
1456 let mut x332: u32 = 0;
1457 let mut x333: fiat_p224_u1 = 0;
1458 fiat_p224_addcarryx_u32(&mut x332, &mut x333, x331, x290, x317);
1459 let mut x334: u32 = 0;
1460 let mut x335: fiat_p224_u1 = 0;
1461 fiat_p224_addcarryx_u32(&mut x334, &mut x335, x333, x292, x319);
1462 let mut x336: u32 = 0;
1463 let mut x337: fiat_p224_u1 = 0;
1464 fiat_p224_addcarryx_u32(&mut x336, &mut x337, x335, x294, x321);
1465 let mut x338: u32 = 0;
1466 let mut x339: fiat_p224_u1 = 0;
1467 fiat_p224_addcarryx_u32(&mut x338, &mut x339, x337, x296, x323);
1468 let mut x340: u32 = 0;
1469 let mut x341: fiat_p224_u1 = 0;
1470 fiat_p224_addcarryx_u32(&mut x340, &mut x341, x339, x298, x325);
1471 let mut x342: u32 = 0;
1472 let mut x343: u32 = 0;
1473 fiat_p224_mulx_u32(&mut x342, &mut x343, x326, 0xffffffff);
1474 let mut x344: u32 = 0;
1475 let mut x345: u32 = 0;
1476 fiat_p224_mulx_u32(&mut x344, &mut x345, x342, 0xffffffff);
1477 let mut x346: u32 = 0;
1478 let mut x347: u32 = 0;
1479 fiat_p224_mulx_u32(&mut x346, &mut x347, x342, 0xffffffff);
1480 let mut x348: u32 = 0;
1481 let mut x349: u32 = 0;
1482 fiat_p224_mulx_u32(&mut x348, &mut x349, x342, 0xffffffff);
1483 let mut x350: u32 = 0;
1484 let mut x351: u32 = 0;
1485 fiat_p224_mulx_u32(&mut x350, &mut x351, x342, 0xffffffff);
1486 let mut x352: u32 = 0;
1487 let mut x353: fiat_p224_u1 = 0;
1488 fiat_p224_addcarryx_u32(&mut x352, &mut x353, 0x0, x351, x348);
1489 let mut x354: u32 = 0;
1490 let mut x355: fiat_p224_u1 = 0;
1491 fiat_p224_addcarryx_u32(&mut x354, &mut x355, x353, x349, x346);
1492 let mut x356: u32 = 0;
1493 let mut x357: fiat_p224_u1 = 0;
1494 fiat_p224_addcarryx_u32(&mut x356, &mut x357, x355, x347, x344);
1495 let x358: u32 = ((x357 as u32) + x345);
1496 let mut x359: u32 = 0;
1497 let mut x360: fiat_p224_u1 = 0;
1498 fiat_p224_addcarryx_u32(&mut x359, &mut x360, 0x0, x326, x342);
1499 let mut x361: u32 = 0;
1500 let mut x362: fiat_p224_u1 = 0;
1501 fiat_p224_addcarryx_u32(&mut x361, &mut x362, x360, x328, (0x0 as u32));
1502 let mut x363: u32 = 0;
1503 let mut x364: fiat_p224_u1 = 0;
1504 fiat_p224_addcarryx_u32(&mut x363, &mut x364, x362, x330, (0x0 as u32));
1505 let mut x365: u32 = 0;
1506 let mut x366: fiat_p224_u1 = 0;
1507 fiat_p224_addcarryx_u32(&mut x365, &mut x366, x364, x332, x350);
1508 let mut x367: u32 = 0;
1509 let mut x368: fiat_p224_u1 = 0;
1510 fiat_p224_addcarryx_u32(&mut x367, &mut x368, x366, x334, x352);
1511 let mut x369: u32 = 0;
1512 let mut x370: fiat_p224_u1 = 0;
1513 fiat_p224_addcarryx_u32(&mut x369, &mut x370, x368, x336, x354);
1514 let mut x371: u32 = 0;
1515 let mut x372: fiat_p224_u1 = 0;
1516 fiat_p224_addcarryx_u32(&mut x371, &mut x372, x370, x338, x356);
1517 let mut x373: u32 = 0;
1518 let mut x374: fiat_p224_u1 = 0;
1519 fiat_p224_addcarryx_u32(&mut x373, &mut x374, x372, x340, x358);
1520 let x375: u32 = ((x374 as u32) + (x341 as u32));
1521 let mut x376: u32 = 0;
1522 let mut x377: u32 = 0;
1523 fiat_p224_mulx_u32(&mut x376, &mut x377, x5, (arg1[6]));
1524 let mut x378: u32 = 0;
1525 let mut x379: u32 = 0;
1526 fiat_p224_mulx_u32(&mut x378, &mut x379, x5, (arg1[5]));
1527 let mut x380: u32 = 0;
1528 let mut x381: u32 = 0;
1529 fiat_p224_mulx_u32(&mut x380, &mut x381, x5, (arg1[4]));
1530 let mut x382: u32 = 0;
1531 let mut x383: u32 = 0;
1532 fiat_p224_mulx_u32(&mut x382, &mut x383, x5, (arg1[3]));
1533 let mut x384: u32 = 0;
1534 let mut x385: u32 = 0;
1535 fiat_p224_mulx_u32(&mut x384, &mut x385, x5, (arg1[2]));
1536 let mut x386: u32 = 0;
1537 let mut x387: u32 = 0;
1538 fiat_p224_mulx_u32(&mut x386, &mut x387, x5, (arg1[1]));
1539 let mut x388: u32 = 0;
1540 let mut x389: u32 = 0;
1541 fiat_p224_mulx_u32(&mut x388, &mut x389, x5, (arg1[0]));
1542 let mut x390: u32 = 0;
1543 let mut x391: fiat_p224_u1 = 0;
1544 fiat_p224_addcarryx_u32(&mut x390, &mut x391, 0x0, x389, x386);
1545 let mut x392: u32 = 0;
1546 let mut x393: fiat_p224_u1 = 0;
1547 fiat_p224_addcarryx_u32(&mut x392, &mut x393, x391, x387, x384);
1548 let mut x394: u32 = 0;
1549 let mut x395: fiat_p224_u1 = 0;
1550 fiat_p224_addcarryx_u32(&mut x394, &mut x395, x393, x385, x382);
1551 let mut x396: u32 = 0;
1552 let mut x397: fiat_p224_u1 = 0;
1553 fiat_p224_addcarryx_u32(&mut x396, &mut x397, x395, x383, x380);
1554 let mut x398: u32 = 0;
1555 let mut x399: fiat_p224_u1 = 0;
1556 fiat_p224_addcarryx_u32(&mut x398, &mut x399, x397, x381, x378);
1557 let mut x400: u32 = 0;
1558 let mut x401: fiat_p224_u1 = 0;
1559 fiat_p224_addcarryx_u32(&mut x400, &mut x401, x399, x379, x376);
1560 let x402: u32 = ((x401 as u32) + x377);
1561 let mut x403: u32 = 0;
1562 let mut x404: fiat_p224_u1 = 0;
1563 fiat_p224_addcarryx_u32(&mut x403, &mut x404, 0x0, x361, x388);
1564 let mut x405: u32 = 0;
1565 let mut x406: fiat_p224_u1 = 0;
1566 fiat_p224_addcarryx_u32(&mut x405, &mut x406, x404, x363, x390);
1567 let mut x407: u32 = 0;
1568 let mut x408: fiat_p224_u1 = 0;
1569 fiat_p224_addcarryx_u32(&mut x407, &mut x408, x406, x365, x392);
1570 let mut x409: u32 = 0;
1571 let mut x410: fiat_p224_u1 = 0;
1572 fiat_p224_addcarryx_u32(&mut x409, &mut x410, x408, x367, x394);
1573 let mut x411: u32 = 0;
1574 let mut x412: fiat_p224_u1 = 0;
1575 fiat_p224_addcarryx_u32(&mut x411, &mut x412, x410, x369, x396);
1576 let mut x413: u32 = 0;
1577 let mut x414: fiat_p224_u1 = 0;
1578 fiat_p224_addcarryx_u32(&mut x413, &mut x414, x412, x371, x398);
1579 let mut x415: u32 = 0;
1580 let mut x416: fiat_p224_u1 = 0;
1581 fiat_p224_addcarryx_u32(&mut x415, &mut x416, x414, x373, x400);
1582 let mut x417: u32 = 0;
1583 let mut x418: fiat_p224_u1 = 0;
1584 fiat_p224_addcarryx_u32(&mut x417, &mut x418, x416, x375, x402);
1585 let mut x419: u32 = 0;
1586 let mut x420: u32 = 0;
1587 fiat_p224_mulx_u32(&mut x419, &mut x420, x403, 0xffffffff);
1588 let mut x421: u32 = 0;
1589 let mut x422: u32 = 0;
1590 fiat_p224_mulx_u32(&mut x421, &mut x422, x419, 0xffffffff);
1591 let mut x423: u32 = 0;
1592 let mut x424: u32 = 0;
1593 fiat_p224_mulx_u32(&mut x423, &mut x424, x419, 0xffffffff);
1594 let mut x425: u32 = 0;
1595 let mut x426: u32 = 0;
1596 fiat_p224_mulx_u32(&mut x425, &mut x426, x419, 0xffffffff);
1597 let mut x427: u32 = 0;
1598 let mut x428: u32 = 0;
1599 fiat_p224_mulx_u32(&mut x427, &mut x428, x419, 0xffffffff);
1600 let mut x429: u32 = 0;
1601 let mut x430: fiat_p224_u1 = 0;
1602 fiat_p224_addcarryx_u32(&mut x429, &mut x430, 0x0, x428, x425);
1603 let mut x431: u32 = 0;
1604 let mut x432: fiat_p224_u1 = 0;
1605 fiat_p224_addcarryx_u32(&mut x431, &mut x432, x430, x426, x423);
1606 let mut x433: u32 = 0;
1607 let mut x434: fiat_p224_u1 = 0;
1608 fiat_p224_addcarryx_u32(&mut x433, &mut x434, x432, x424, x421);
1609 let x435: u32 = ((x434 as u32) + x422);
1610 let mut x436: u32 = 0;
1611 let mut x437: fiat_p224_u1 = 0;
1612 fiat_p224_addcarryx_u32(&mut x436, &mut x437, 0x0, x403, x419);
1613 let mut x438: u32 = 0;
1614 let mut x439: fiat_p224_u1 = 0;
1615 fiat_p224_addcarryx_u32(&mut x438, &mut x439, x437, x405, (0x0 as u32));
1616 let mut x440: u32 = 0;
1617 let mut x441: fiat_p224_u1 = 0;
1618 fiat_p224_addcarryx_u32(&mut x440, &mut x441, x439, x407, (0x0 as u32));
1619 let mut x442: u32 = 0;
1620 let mut x443: fiat_p224_u1 = 0;
1621 fiat_p224_addcarryx_u32(&mut x442, &mut x443, x441, x409, x427);
1622 let mut x444: u32 = 0;
1623 let mut x445: fiat_p224_u1 = 0;
1624 fiat_p224_addcarryx_u32(&mut x444, &mut x445, x443, x411, x429);
1625 let mut x446: u32 = 0;
1626 let mut x447: fiat_p224_u1 = 0;
1627 fiat_p224_addcarryx_u32(&mut x446, &mut x447, x445, x413, x431);
1628 let mut x448: u32 = 0;
1629 let mut x449: fiat_p224_u1 = 0;
1630 fiat_p224_addcarryx_u32(&mut x448, &mut x449, x447, x415, x433);
1631 let mut x450: u32 = 0;
1632 let mut x451: fiat_p224_u1 = 0;
1633 fiat_p224_addcarryx_u32(&mut x450, &mut x451, x449, x417, x435);
1634 let x452: u32 = ((x451 as u32) + (x418 as u32));
1635 let mut x453: u32 = 0;
1636 let mut x454: u32 = 0;
1637 fiat_p224_mulx_u32(&mut x453, &mut x454, x6, (arg1[6]));
1638 let mut x455: u32 = 0;
1639 let mut x456: u32 = 0;
1640 fiat_p224_mulx_u32(&mut x455, &mut x456, x6, (arg1[5]));
1641 let mut x457: u32 = 0;
1642 let mut x458: u32 = 0;
1643 fiat_p224_mulx_u32(&mut x457, &mut x458, x6, (arg1[4]));
1644 let mut x459: u32 = 0;
1645 let mut x460: u32 = 0;
1646 fiat_p224_mulx_u32(&mut x459, &mut x460, x6, (arg1[3]));
1647 let mut x461: u32 = 0;
1648 let mut x462: u32 = 0;
1649 fiat_p224_mulx_u32(&mut x461, &mut x462, x6, (arg1[2]));
1650 let mut x463: u32 = 0;
1651 let mut x464: u32 = 0;
1652 fiat_p224_mulx_u32(&mut x463, &mut x464, x6, (arg1[1]));
1653 let mut x465: u32 = 0;
1654 let mut x466: u32 = 0;
1655 fiat_p224_mulx_u32(&mut x465, &mut x466, x6, (arg1[0]));
1656 let mut x467: u32 = 0;
1657 let mut x468: fiat_p224_u1 = 0;
1658 fiat_p224_addcarryx_u32(&mut x467, &mut x468, 0x0, x466, x463);
1659 let mut x469: u32 = 0;
1660 let mut x470: fiat_p224_u1 = 0;
1661 fiat_p224_addcarryx_u32(&mut x469, &mut x470, x468, x464, x461);
1662 let mut x471: u32 = 0;
1663 let mut x472: fiat_p224_u1 = 0;
1664 fiat_p224_addcarryx_u32(&mut x471, &mut x472, x470, x462, x459);
1665 let mut x473: u32 = 0;
1666 let mut x474: fiat_p224_u1 = 0;
1667 fiat_p224_addcarryx_u32(&mut x473, &mut x474, x472, x460, x457);
1668 let mut x475: u32 = 0;
1669 let mut x476: fiat_p224_u1 = 0;
1670 fiat_p224_addcarryx_u32(&mut x475, &mut x476, x474, x458, x455);
1671 let mut x477: u32 = 0;
1672 let mut x478: fiat_p224_u1 = 0;
1673 fiat_p224_addcarryx_u32(&mut x477, &mut x478, x476, x456, x453);
1674 let x479: u32 = ((x478 as u32) + x454);
1675 let mut x480: u32 = 0;
1676 let mut x481: fiat_p224_u1 = 0;
1677 fiat_p224_addcarryx_u32(&mut x480, &mut x481, 0x0, x438, x465);
1678 let mut x482: u32 = 0;
1679 let mut x483: fiat_p224_u1 = 0;
1680 fiat_p224_addcarryx_u32(&mut x482, &mut x483, x481, x440, x467);
1681 let mut x484: u32 = 0;
1682 let mut x485: fiat_p224_u1 = 0;
1683 fiat_p224_addcarryx_u32(&mut x484, &mut x485, x483, x442, x469);
1684 let mut x486: u32 = 0;
1685 let mut x487: fiat_p224_u1 = 0;
1686 fiat_p224_addcarryx_u32(&mut x486, &mut x487, x485, x444, x471);
1687 let mut x488: u32 = 0;
1688 let mut x489: fiat_p224_u1 = 0;
1689 fiat_p224_addcarryx_u32(&mut x488, &mut x489, x487, x446, x473);
1690 let mut x490: u32 = 0;
1691 let mut x491: fiat_p224_u1 = 0;
1692 fiat_p224_addcarryx_u32(&mut x490, &mut x491, x489, x448, x475);
1693 let mut x492: u32 = 0;
1694 let mut x493: fiat_p224_u1 = 0;
1695 fiat_p224_addcarryx_u32(&mut x492, &mut x493, x491, x450, x477);
1696 let mut x494: u32 = 0;
1697 let mut x495: fiat_p224_u1 = 0;
1698 fiat_p224_addcarryx_u32(&mut x494, &mut x495, x493, x452, x479);
1699 let mut x496: u32 = 0;
1700 let mut x497: u32 = 0;
1701 fiat_p224_mulx_u32(&mut x496, &mut x497, x480, 0xffffffff);
1702 let mut x498: u32 = 0;
1703 let mut x499: u32 = 0;
1704 fiat_p224_mulx_u32(&mut x498, &mut x499, x496, 0xffffffff);
1705 let mut x500: u32 = 0;
1706 let mut x501: u32 = 0;
1707 fiat_p224_mulx_u32(&mut x500, &mut x501, x496, 0xffffffff);
1708 let mut x502: u32 = 0;
1709 let mut x503: u32 = 0;
1710 fiat_p224_mulx_u32(&mut x502, &mut x503, x496, 0xffffffff);
1711 let mut x504: u32 = 0;
1712 let mut x505: u32 = 0;
1713 fiat_p224_mulx_u32(&mut x504, &mut x505, x496, 0xffffffff);
1714 let mut x506: u32 = 0;
1715 let mut x507: fiat_p224_u1 = 0;
1716 fiat_p224_addcarryx_u32(&mut x506, &mut x507, 0x0, x505, x502);
1717 let mut x508: u32 = 0;
1718 let mut x509: fiat_p224_u1 = 0;
1719 fiat_p224_addcarryx_u32(&mut x508, &mut x509, x507, x503, x500);
1720 let mut x510: u32 = 0;
1721 let mut x511: fiat_p224_u1 = 0;
1722 fiat_p224_addcarryx_u32(&mut x510, &mut x511, x509, x501, x498);
1723 let x512: u32 = ((x511 as u32) + x499);
1724 let mut x513: u32 = 0;
1725 let mut x514: fiat_p224_u1 = 0;
1726 fiat_p224_addcarryx_u32(&mut x513, &mut x514, 0x0, x480, x496);
1727 let mut x515: u32 = 0;
1728 let mut x516: fiat_p224_u1 = 0;
1729 fiat_p224_addcarryx_u32(&mut x515, &mut x516, x514, x482, (0x0 as u32));
1730 let mut x517: u32 = 0;
1731 let mut x518: fiat_p224_u1 = 0;
1732 fiat_p224_addcarryx_u32(&mut x517, &mut x518, x516, x484, (0x0 as u32));
1733 let mut x519: u32 = 0;
1734 let mut x520: fiat_p224_u1 = 0;
1735 fiat_p224_addcarryx_u32(&mut x519, &mut x520, x518, x486, x504);
1736 let mut x521: u32 = 0;
1737 let mut x522: fiat_p224_u1 = 0;
1738 fiat_p224_addcarryx_u32(&mut x521, &mut x522, x520, x488, x506);
1739 let mut x523: u32 = 0;
1740 let mut x524: fiat_p224_u1 = 0;
1741 fiat_p224_addcarryx_u32(&mut x523, &mut x524, x522, x490, x508);
1742 let mut x525: u32 = 0;
1743 let mut x526: fiat_p224_u1 = 0;
1744 fiat_p224_addcarryx_u32(&mut x525, &mut x526, x524, x492, x510);
1745 let mut x527: u32 = 0;
1746 let mut x528: fiat_p224_u1 = 0;
1747 fiat_p224_addcarryx_u32(&mut x527, &mut x528, x526, x494, x512);
1748 let x529: u32 = ((x528 as u32) + (x495 as u32));
1749 let mut x530: u32 = 0;
1750 let mut x531: fiat_p224_u1 = 0;
1751 fiat_p224_subborrowx_u32(&mut x530, &mut x531, 0x0, x515, (0x1 as u32));
1752 let mut x532: u32 = 0;
1753 let mut x533: fiat_p224_u1 = 0;
1754 fiat_p224_subborrowx_u32(&mut x532, &mut x533, x531, x517, (0x0 as u32));
1755 let mut x534: u32 = 0;
1756 let mut x535: fiat_p224_u1 = 0;
1757 fiat_p224_subborrowx_u32(&mut x534, &mut x535, x533, x519, (0x0 as u32));
1758 let mut x536: u32 = 0;
1759 let mut x537: fiat_p224_u1 = 0;
1760 fiat_p224_subborrowx_u32(&mut x536, &mut x537, x535, x521, 0xffffffff);
1761 let mut x538: u32 = 0;
1762 let mut x539: fiat_p224_u1 = 0;
1763 fiat_p224_subborrowx_u32(&mut x538, &mut x539, x537, x523, 0xffffffff);
1764 let mut x540: u32 = 0;
1765 let mut x541: fiat_p224_u1 = 0;
1766 fiat_p224_subborrowx_u32(&mut x540, &mut x541, x539, x525, 0xffffffff);
1767 let mut x542: u32 = 0;
1768 let mut x543: fiat_p224_u1 = 0;
1769 fiat_p224_subborrowx_u32(&mut x542, &mut x543, x541, x527, 0xffffffff);
1770 let mut x544: u32 = 0;
1771 let mut x545: fiat_p224_u1 = 0;
1772 fiat_p224_subborrowx_u32(&mut x544, &mut x545, x543, x529, (0x0 as u32));
1773 let mut x546: u32 = 0;
1774 fiat_p224_cmovznz_u32(&mut x546, x545, x530, x515);
1775 let mut x547: u32 = 0;
1776 fiat_p224_cmovznz_u32(&mut x547, x545, x532, x517);
1777 let mut x548: u32 = 0;
1778 fiat_p224_cmovznz_u32(&mut x548, x545, x534, x519);
1779 let mut x549: u32 = 0;
1780 fiat_p224_cmovznz_u32(&mut x549, x545, x536, x521);
1781 let mut x550: u32 = 0;
1782 fiat_p224_cmovznz_u32(&mut x550, x545, x538, x523);
1783 let mut x551: u32 = 0;
1784 fiat_p224_cmovznz_u32(&mut x551, x545, x540, x525);
1785 let mut x552: u32 = 0;
1786 fiat_p224_cmovznz_u32(&mut x552, x545, x542, x527);
1787 out1[0] = x546;
1788 out1[1] = x547;
1789 out1[2] = x548;
1790 out1[3] = x549;
1791 out1[4] = x550;
1792 out1[5] = x551;
1793 out1[6] = x552;
1794}
1795
1796/// The function fiat_p224_add adds two field elements in the Montgomery domain.
1797///
1798/// Preconditions:
1799/// 0 ≤ eval arg1 < m
1800/// 0 ≤ eval arg2 < m
1801/// Postconditions:
1802/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m
1803/// 0 ≤ eval out1 < m
1804///
1805#[inline]
1806pub fn fiat_p224_add(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element, arg2: &fiat_p224_montgomery_domain_field_element) -> () {
1807 let mut x1: u32 = 0;
1808 let mut x2: fiat_p224_u1 = 0;
1809 fiat_p224_addcarryx_u32(&mut x1, &mut x2, 0x0, (arg1[0]), (arg2[0]));
1810 let mut x3: u32 = 0;
1811 let mut x4: fiat_p224_u1 = 0;
1812 fiat_p224_addcarryx_u32(&mut x3, &mut x4, x2, (arg1[1]), (arg2[1]));
1813 let mut x5: u32 = 0;
1814 let mut x6: fiat_p224_u1 = 0;
1815 fiat_p224_addcarryx_u32(&mut x5, &mut x6, x4, (arg1[2]), (arg2[2]));
1816 let mut x7: u32 = 0;
1817 let mut x8: fiat_p224_u1 = 0;
1818 fiat_p224_addcarryx_u32(&mut x7, &mut x8, x6, (arg1[3]), (arg2[3]));
1819 let mut x9: u32 = 0;
1820 let mut x10: fiat_p224_u1 = 0;
1821 fiat_p224_addcarryx_u32(&mut x9, &mut x10, x8, (arg1[4]), (arg2[4]));
1822 let mut x11: u32 = 0;
1823 let mut x12: fiat_p224_u1 = 0;
1824 fiat_p224_addcarryx_u32(&mut x11, &mut x12, x10, (arg1[5]), (arg2[5]));
1825 let mut x13: u32 = 0;
1826 let mut x14: fiat_p224_u1 = 0;
1827 fiat_p224_addcarryx_u32(&mut x13, &mut x14, x12, (arg1[6]), (arg2[6]));
1828 let mut x15: u32 = 0;
1829 let mut x16: fiat_p224_u1 = 0;
1830 fiat_p224_subborrowx_u32(&mut x15, &mut x16, 0x0, x1, (0x1 as u32));
1831 let mut x17: u32 = 0;
1832 let mut x18: fiat_p224_u1 = 0;
1833 fiat_p224_subborrowx_u32(&mut x17, &mut x18, x16, x3, (0x0 as u32));
1834 let mut x19: u32 = 0;
1835 let mut x20: fiat_p224_u1 = 0;
1836 fiat_p224_subborrowx_u32(&mut x19, &mut x20, x18, x5, (0x0 as u32));
1837 let mut x21: u32 = 0;
1838 let mut x22: fiat_p224_u1 = 0;
1839 fiat_p224_subborrowx_u32(&mut x21, &mut x22, x20, x7, 0xffffffff);
1840 let mut x23: u32 = 0;
1841 let mut x24: fiat_p224_u1 = 0;
1842 fiat_p224_subborrowx_u32(&mut x23, &mut x24, x22, x9, 0xffffffff);
1843 let mut x25: u32 = 0;
1844 let mut x26: fiat_p224_u1 = 0;
1845 fiat_p224_subborrowx_u32(&mut x25, &mut x26, x24, x11, 0xffffffff);
1846 let mut x27: u32 = 0;
1847 let mut x28: fiat_p224_u1 = 0;
1848 fiat_p224_subborrowx_u32(&mut x27, &mut x28, x26, x13, 0xffffffff);
1849 let mut x29: u32 = 0;
1850 let mut x30: fiat_p224_u1 = 0;
1851 fiat_p224_subborrowx_u32(&mut x29, &mut x30, x28, (x14 as u32), (0x0 as u32));
1852 let mut x31: u32 = 0;
1853 fiat_p224_cmovznz_u32(&mut x31, x30, x15, x1);
1854 let mut x32: u32 = 0;
1855 fiat_p224_cmovznz_u32(&mut x32, x30, x17, x3);
1856 let mut x33: u32 = 0;
1857 fiat_p224_cmovznz_u32(&mut x33, x30, x19, x5);
1858 let mut x34: u32 = 0;
1859 fiat_p224_cmovznz_u32(&mut x34, x30, x21, x7);
1860 let mut x35: u32 = 0;
1861 fiat_p224_cmovznz_u32(&mut x35, x30, x23, x9);
1862 let mut x36: u32 = 0;
1863 fiat_p224_cmovznz_u32(&mut x36, x30, x25, x11);
1864 let mut x37: u32 = 0;
1865 fiat_p224_cmovznz_u32(&mut x37, x30, x27, x13);
1866 out1[0] = x31;
1867 out1[1] = x32;
1868 out1[2] = x33;
1869 out1[3] = x34;
1870 out1[4] = x35;
1871 out1[5] = x36;
1872 out1[6] = x37;
1873}
1874
1875/// The function fiat_p224_sub subtracts two field elements in the Montgomery domain.
1876///
1877/// Preconditions:
1878/// 0 ≤ eval arg1 < m
1879/// 0 ≤ eval arg2 < m
1880/// Postconditions:
1881/// eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m
1882/// 0 ≤ eval out1 < m
1883///
1884#[inline]
1885pub fn fiat_p224_sub(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element, arg2: &fiat_p224_montgomery_domain_field_element) -> () {
1886 let mut x1: u32 = 0;
1887 let mut x2: fiat_p224_u1 = 0;
1888 fiat_p224_subborrowx_u32(&mut x1, &mut x2, 0x0, (arg1[0]), (arg2[0]));
1889 let mut x3: u32 = 0;
1890 let mut x4: fiat_p224_u1 = 0;
1891 fiat_p224_subborrowx_u32(&mut x3, &mut x4, x2, (arg1[1]), (arg2[1]));
1892 let mut x5: u32 = 0;
1893 let mut x6: fiat_p224_u1 = 0;
1894 fiat_p224_subborrowx_u32(&mut x5, &mut x6, x4, (arg1[2]), (arg2[2]));
1895 let mut x7: u32 = 0;
1896 let mut x8: fiat_p224_u1 = 0;
1897 fiat_p224_subborrowx_u32(&mut x7, &mut x8, x6, (arg1[3]), (arg2[3]));
1898 let mut x9: u32 = 0;
1899 let mut x10: fiat_p224_u1 = 0;
1900 fiat_p224_subborrowx_u32(&mut x9, &mut x10, x8, (arg1[4]), (arg2[4]));
1901 let mut x11: u32 = 0;
1902 let mut x12: fiat_p224_u1 = 0;
1903 fiat_p224_subborrowx_u32(&mut x11, &mut x12, x10, (arg1[5]), (arg2[5]));
1904 let mut x13: u32 = 0;
1905 let mut x14: fiat_p224_u1 = 0;
1906 fiat_p224_subborrowx_u32(&mut x13, &mut x14, x12, (arg1[6]), (arg2[6]));
1907 let mut x15: u32 = 0;
1908 fiat_p224_cmovznz_u32(&mut x15, x14, (0x0 as u32), 0xffffffff);
1909 let mut x16: u32 = 0;
1910 let mut x17: fiat_p224_u1 = 0;
1911 fiat_p224_addcarryx_u32(&mut x16, &mut x17, 0x0, x1, (((x15 & (0x1 as u32)) as fiat_p224_u1) as u32));
1912 let mut x18: u32 = 0;
1913 let mut x19: fiat_p224_u1 = 0;
1914 fiat_p224_addcarryx_u32(&mut x18, &mut x19, x17, x3, (0x0 as u32));
1915 let mut x20: u32 = 0;
1916 let mut x21: fiat_p224_u1 = 0;
1917 fiat_p224_addcarryx_u32(&mut x20, &mut x21, x19, x5, (0x0 as u32));
1918 let mut x22: u32 = 0;
1919 let mut x23: fiat_p224_u1 = 0;
1920 fiat_p224_addcarryx_u32(&mut x22, &mut x23, x21, x7, x15);
1921 let mut x24: u32 = 0;
1922 let mut x25: fiat_p224_u1 = 0;
1923 fiat_p224_addcarryx_u32(&mut x24, &mut x25, x23, x9, x15);
1924 let mut x26: u32 = 0;
1925 let mut x27: fiat_p224_u1 = 0;
1926 fiat_p224_addcarryx_u32(&mut x26, &mut x27, x25, x11, x15);
1927 let mut x28: u32 = 0;
1928 let mut x29: fiat_p224_u1 = 0;
1929 fiat_p224_addcarryx_u32(&mut x28, &mut x29, x27, x13, x15);
1930 out1[0] = x16;
1931 out1[1] = x18;
1932 out1[2] = x20;
1933 out1[3] = x22;
1934 out1[4] = x24;
1935 out1[5] = x26;
1936 out1[6] = x28;
1937}
1938
1939/// The function fiat_p224_opp negates a field element in the Montgomery domain.
1940///
1941/// Preconditions:
1942/// 0 ≤ eval arg1 < m
1943/// Postconditions:
1944/// eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m
1945/// 0 ≤ eval out1 < m
1946///
1947#[inline]
1948pub fn fiat_p224_opp(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element) -> () {
1949 let mut x1: u32 = 0;
1950 let mut x2: fiat_p224_u1 = 0;
1951 fiat_p224_subborrowx_u32(&mut x1, &mut x2, 0x0, (0x0 as u32), (arg1[0]));
1952 let mut x3: u32 = 0;
1953 let mut x4: fiat_p224_u1 = 0;
1954 fiat_p224_subborrowx_u32(&mut x3, &mut x4, x2, (0x0 as u32), (arg1[1]));
1955 let mut x5: u32 = 0;
1956 let mut x6: fiat_p224_u1 = 0;
1957 fiat_p224_subborrowx_u32(&mut x5, &mut x6, x4, (0x0 as u32), (arg1[2]));
1958 let mut x7: u32 = 0;
1959 let mut x8: fiat_p224_u1 = 0;
1960 fiat_p224_subborrowx_u32(&mut x7, &mut x8, x6, (0x0 as u32), (arg1[3]));
1961 let mut x9: u32 = 0;
1962 let mut x10: fiat_p224_u1 = 0;
1963 fiat_p224_subborrowx_u32(&mut x9, &mut x10, x8, (0x0 as u32), (arg1[4]));
1964 let mut x11: u32 = 0;
1965 let mut x12: fiat_p224_u1 = 0;
1966 fiat_p224_subborrowx_u32(&mut x11, &mut x12, x10, (0x0 as u32), (arg1[5]));
1967 let mut x13: u32 = 0;
1968 let mut x14: fiat_p224_u1 = 0;
1969 fiat_p224_subborrowx_u32(&mut x13, &mut x14, x12, (0x0 as u32), (arg1[6]));
1970 let mut x15: u32 = 0;
1971 fiat_p224_cmovznz_u32(&mut x15, x14, (0x0 as u32), 0xffffffff);
1972 let mut x16: u32 = 0;
1973 let mut x17: fiat_p224_u1 = 0;
1974 fiat_p224_addcarryx_u32(&mut x16, &mut x17, 0x0, x1, (((x15 & (0x1 as u32)) as fiat_p224_u1) as u32));
1975 let mut x18: u32 = 0;
1976 let mut x19: fiat_p224_u1 = 0;
1977 fiat_p224_addcarryx_u32(&mut x18, &mut x19, x17, x3, (0x0 as u32));
1978 let mut x20: u32 = 0;
1979 let mut x21: fiat_p224_u1 = 0;
1980 fiat_p224_addcarryx_u32(&mut x20, &mut x21, x19, x5, (0x0 as u32));
1981 let mut x22: u32 = 0;
1982 let mut x23: fiat_p224_u1 = 0;
1983 fiat_p224_addcarryx_u32(&mut x22, &mut x23, x21, x7, x15);
1984 let mut x24: u32 = 0;
1985 let mut x25: fiat_p224_u1 = 0;
1986 fiat_p224_addcarryx_u32(&mut x24, &mut x25, x23, x9, x15);
1987 let mut x26: u32 = 0;
1988 let mut x27: fiat_p224_u1 = 0;
1989 fiat_p224_addcarryx_u32(&mut x26, &mut x27, x25, x11, x15);
1990 let mut x28: u32 = 0;
1991 let mut x29: fiat_p224_u1 = 0;
1992 fiat_p224_addcarryx_u32(&mut x28, &mut x29, x27, x13, x15);
1993 out1[0] = x16;
1994 out1[1] = x18;
1995 out1[2] = x20;
1996 out1[3] = x22;
1997 out1[4] = x24;
1998 out1[5] = x26;
1999 out1[6] = x28;
2000}
2001
2002/// The function fiat_p224_from_montgomery translates a field element out of the Montgomery domain.
2003///
2004/// Preconditions:
2005/// 0 ≤ eval arg1 < m
2006/// Postconditions:
2007/// eval out1 mod m = (eval arg1 * ((2^32)⁻¹ mod m)^7) mod m
2008/// 0 ≤ eval out1 < m
2009///
2010#[inline]
2011pub fn fiat_p224_from_montgomery(out1: &mut fiat_p224_non_montgomery_domain_field_element, arg1: &fiat_p224_montgomery_domain_field_element) -> () {
2012 let x1: u32 = (arg1[0]);
2013 let mut x2: u32 = 0;
2014 let mut x3: u32 = 0;
2015 fiat_p224_mulx_u32(&mut x2, &mut x3, x1, 0xffffffff);
2016 let mut x4: u32 = 0;
2017 let mut x5: u32 = 0;
2018 fiat_p224_mulx_u32(&mut x4, &mut x5, x2, 0xffffffff);
2019 let mut x6: u32 = 0;
2020 let mut x7: u32 = 0;
2021 fiat_p224_mulx_u32(&mut x6, &mut x7, x2, 0xffffffff);
2022 let mut x8: u32 = 0;
2023 let mut x9: u32 = 0;
2024 fiat_p224_mulx_u32(&mut x8, &mut x9, x2, 0xffffffff);
2025 let mut x10: u32 = 0;
2026 let mut x11: u32 = 0;
2027 fiat_p224_mulx_u32(&mut x10, &mut x11, x2, 0xffffffff);
2028 let mut x12: u32 = 0;
2029 let mut x13: fiat_p224_u1 = 0;
2030 fiat_p224_addcarryx_u32(&mut x12, &mut x13, 0x0, x11, x8);
2031 let mut x14: u32 = 0;
2032 let mut x15: fiat_p224_u1 = 0;
2033 fiat_p224_addcarryx_u32(&mut x14, &mut x15, x13, x9, x6);
2034 let mut x16: u32 = 0;
2035 let mut x17: fiat_p224_u1 = 0;
2036 fiat_p224_addcarryx_u32(&mut x16, &mut x17, x15, x7, x4);
2037 let mut x18: u32 = 0;
2038 let mut x19: fiat_p224_u1 = 0;
2039 fiat_p224_addcarryx_u32(&mut x18, &mut x19, 0x0, x1, x2);
2040 let mut x20: u32 = 0;
2041 let mut x21: fiat_p224_u1 = 0;
2042 fiat_p224_addcarryx_u32(&mut x20, &mut x21, 0x0, (x19 as u32), (arg1[1]));
2043 let mut x22: u32 = 0;
2044 let mut x23: u32 = 0;
2045 fiat_p224_mulx_u32(&mut x22, &mut x23, x20, 0xffffffff);
2046 let mut x24: u32 = 0;
2047 let mut x25: u32 = 0;
2048 fiat_p224_mulx_u32(&mut x24, &mut x25, x22, 0xffffffff);
2049 let mut x26: u32 = 0;
2050 let mut x27: u32 = 0;
2051 fiat_p224_mulx_u32(&mut x26, &mut x27, x22, 0xffffffff);
2052 let mut x28: u32 = 0;
2053 let mut x29: u32 = 0;
2054 fiat_p224_mulx_u32(&mut x28, &mut x29, x22, 0xffffffff);
2055 let mut x30: u32 = 0;
2056 let mut x31: u32 = 0;
2057 fiat_p224_mulx_u32(&mut x30, &mut x31, x22, 0xffffffff);
2058 let mut x32: u32 = 0;
2059 let mut x33: fiat_p224_u1 = 0;
2060 fiat_p224_addcarryx_u32(&mut x32, &mut x33, 0x0, x31, x28);
2061 let mut x34: u32 = 0;
2062 let mut x35: fiat_p224_u1 = 0;
2063 fiat_p224_addcarryx_u32(&mut x34, &mut x35, x33, x29, x26);
2064 let mut x36: u32 = 0;
2065 let mut x37: fiat_p224_u1 = 0;
2066 fiat_p224_addcarryx_u32(&mut x36, &mut x37, x35, x27, x24);
2067 let mut x38: u32 = 0;
2068 let mut x39: fiat_p224_u1 = 0;
2069 fiat_p224_addcarryx_u32(&mut x38, &mut x39, 0x0, x12, x30);
2070 let mut x40: u32 = 0;
2071 let mut x41: fiat_p224_u1 = 0;
2072 fiat_p224_addcarryx_u32(&mut x40, &mut x41, x39, x14, x32);
2073 let mut x42: u32 = 0;
2074 let mut x43: fiat_p224_u1 = 0;
2075 fiat_p224_addcarryx_u32(&mut x42, &mut x43, x41, x16, x34);
2076 let mut x44: u32 = 0;
2077 let mut x45: fiat_p224_u1 = 0;
2078 fiat_p224_addcarryx_u32(&mut x44, &mut x45, x43, ((x17 as u32) + x5), x36);
2079 let mut x46: u32 = 0;
2080 let mut x47: fiat_p224_u1 = 0;
2081 fiat_p224_addcarryx_u32(&mut x46, &mut x47, x45, (0x0 as u32), ((x37 as u32) + x25));
2082 let mut x48: u32 = 0;
2083 let mut x49: fiat_p224_u1 = 0;
2084 fiat_p224_addcarryx_u32(&mut x48, &mut x49, 0x0, x20, x22);
2085 let mut x50: u32 = 0;
2086 let mut x51: fiat_p224_u1 = 0;
2087 fiat_p224_addcarryx_u32(&mut x50, &mut x51, 0x0, ((x49 as u32) + (x21 as u32)), (arg1[2]));
2088 let mut x52: u32 = 0;
2089 let mut x53: fiat_p224_u1 = 0;
2090 fiat_p224_addcarryx_u32(&mut x52, &mut x53, x51, x10, (0x0 as u32));
2091 let mut x54: u32 = 0;
2092 let mut x55: fiat_p224_u1 = 0;
2093 fiat_p224_addcarryx_u32(&mut x54, &mut x55, x53, x38, (0x0 as u32));
2094 let mut x56: u32 = 0;
2095 let mut x57: fiat_p224_u1 = 0;
2096 fiat_p224_addcarryx_u32(&mut x56, &mut x57, x55, x40, (0x0 as u32));
2097 let mut x58: u32 = 0;
2098 let mut x59: fiat_p224_u1 = 0;
2099 fiat_p224_addcarryx_u32(&mut x58, &mut x59, x57, x42, (0x0 as u32));
2100 let mut x60: u32 = 0;
2101 let mut x61: fiat_p224_u1 = 0;
2102 fiat_p224_addcarryx_u32(&mut x60, &mut x61, x59, x44, (0x0 as u32));
2103 let mut x62: u32 = 0;
2104 let mut x63: fiat_p224_u1 = 0;
2105 fiat_p224_addcarryx_u32(&mut x62, &mut x63, x61, x46, (0x0 as u32));
2106 let mut x64: u32 = 0;
2107 let mut x65: u32 = 0;
2108 fiat_p224_mulx_u32(&mut x64, &mut x65, x50, 0xffffffff);
2109 let mut x66: u32 = 0;
2110 let mut x67: u32 = 0;
2111 fiat_p224_mulx_u32(&mut x66, &mut x67, x64, 0xffffffff);
2112 let mut x68: u32 = 0;
2113 let mut x69: u32 = 0;
2114 fiat_p224_mulx_u32(&mut x68, &mut x69, x64, 0xffffffff);
2115 let mut x70: u32 = 0;
2116 let mut x71: u32 = 0;
2117 fiat_p224_mulx_u32(&mut x70, &mut x71, x64, 0xffffffff);
2118 let mut x72: u32 = 0;
2119 let mut x73: u32 = 0;
2120 fiat_p224_mulx_u32(&mut x72, &mut x73, x64, 0xffffffff);
2121 let mut x74: u32 = 0;
2122 let mut x75: fiat_p224_u1 = 0;
2123 fiat_p224_addcarryx_u32(&mut x74, &mut x75, 0x0, x73, x70);
2124 let mut x76: u32 = 0;
2125 let mut x77: fiat_p224_u1 = 0;
2126 fiat_p224_addcarryx_u32(&mut x76, &mut x77, x75, x71, x68);
2127 let mut x78: u32 = 0;
2128 let mut x79: fiat_p224_u1 = 0;
2129 fiat_p224_addcarryx_u32(&mut x78, &mut x79, x77, x69, x66);
2130 let mut x80: u32 = 0;
2131 let mut x81: fiat_p224_u1 = 0;
2132 fiat_p224_addcarryx_u32(&mut x80, &mut x81, 0x0, x50, x64);
2133 let mut x82: u32 = 0;
2134 let mut x83: fiat_p224_u1 = 0;
2135 fiat_p224_addcarryx_u32(&mut x82, &mut x83, x81, x52, (0x0 as u32));
2136 let mut x84: u32 = 0;
2137 let mut x85: fiat_p224_u1 = 0;
2138 fiat_p224_addcarryx_u32(&mut x84, &mut x85, x83, x54, (0x0 as u32));
2139 let mut x86: u32 = 0;
2140 let mut x87: fiat_p224_u1 = 0;
2141 fiat_p224_addcarryx_u32(&mut x86, &mut x87, x85, x56, x72);
2142 let mut x88: u32 = 0;
2143 let mut x89: fiat_p224_u1 = 0;
2144 fiat_p224_addcarryx_u32(&mut x88, &mut x89, x87, x58, x74);
2145 let mut x90: u32 = 0;
2146 let mut x91: fiat_p224_u1 = 0;
2147 fiat_p224_addcarryx_u32(&mut x90, &mut x91, x89, x60, x76);
2148 let mut x92: u32 = 0;
2149 let mut x93: fiat_p224_u1 = 0;
2150 fiat_p224_addcarryx_u32(&mut x92, &mut x93, x91, x62, x78);
2151 let mut x94: u32 = 0;
2152 let mut x95: fiat_p224_u1 = 0;
2153 fiat_p224_addcarryx_u32(&mut x94, &mut x95, x93, ((x63 as u32) + (x47 as u32)), ((x79 as u32) + x67));
2154 let mut x96: u32 = 0;
2155 let mut x97: fiat_p224_u1 = 0;
2156 fiat_p224_addcarryx_u32(&mut x96, &mut x97, 0x0, x82, (arg1[3]));
2157 let mut x98: u32 = 0;
2158 let mut x99: fiat_p224_u1 = 0;
2159 fiat_p224_addcarryx_u32(&mut x98, &mut x99, x97, x84, (0x0 as u32));
2160 let mut x100: u32 = 0;
2161 let mut x101: fiat_p224_u1 = 0;
2162 fiat_p224_addcarryx_u32(&mut x100, &mut x101, x99, x86, (0x0 as u32));
2163 let mut x102: u32 = 0;
2164 let mut x103: fiat_p224_u1 = 0;
2165 fiat_p224_addcarryx_u32(&mut x102, &mut x103, x101, x88, (0x0 as u32));
2166 let mut x104: u32 = 0;
2167 let mut x105: fiat_p224_u1 = 0;
2168 fiat_p224_addcarryx_u32(&mut x104, &mut x105, x103, x90, (0x0 as u32));
2169 let mut x106: u32 = 0;
2170 let mut x107: fiat_p224_u1 = 0;
2171 fiat_p224_addcarryx_u32(&mut x106, &mut x107, x105, x92, (0x0 as u32));
2172 let mut x108: u32 = 0;
2173 let mut x109: fiat_p224_u1 = 0;
2174 fiat_p224_addcarryx_u32(&mut x108, &mut x109, x107, x94, (0x0 as u32));
2175 let mut x110: u32 = 0;
2176 let mut x111: u32 = 0;
2177 fiat_p224_mulx_u32(&mut x110, &mut x111, x96, 0xffffffff);
2178 let mut x112: u32 = 0;
2179 let mut x113: u32 = 0;
2180 fiat_p224_mulx_u32(&mut x112, &mut x113, x110, 0xffffffff);
2181 let mut x114: u32 = 0;
2182 let mut x115: u32 = 0;
2183 fiat_p224_mulx_u32(&mut x114, &mut x115, x110, 0xffffffff);
2184 let mut x116: u32 = 0;
2185 let mut x117: u32 = 0;
2186 fiat_p224_mulx_u32(&mut x116, &mut x117, x110, 0xffffffff);
2187 let mut x118: u32 = 0;
2188 let mut x119: u32 = 0;
2189 fiat_p224_mulx_u32(&mut x118, &mut x119, x110, 0xffffffff);
2190 let mut x120: u32 = 0;
2191 let mut x121: fiat_p224_u1 = 0;
2192 fiat_p224_addcarryx_u32(&mut x120, &mut x121, 0x0, x119, x116);
2193 let mut x122: u32 = 0;
2194 let mut x123: fiat_p224_u1 = 0;
2195 fiat_p224_addcarryx_u32(&mut x122, &mut x123, x121, x117, x114);
2196 let mut x124: u32 = 0;
2197 let mut x125: fiat_p224_u1 = 0;
2198 fiat_p224_addcarryx_u32(&mut x124, &mut x125, x123, x115, x112);
2199 let mut x126: u32 = 0;
2200 let mut x127: fiat_p224_u1 = 0;
2201 fiat_p224_addcarryx_u32(&mut x126, &mut x127, 0x0, x96, x110);
2202 let mut x128: u32 = 0;
2203 let mut x129: fiat_p224_u1 = 0;
2204 fiat_p224_addcarryx_u32(&mut x128, &mut x129, x127, x98, (0x0 as u32));
2205 let mut x130: u32 = 0;
2206 let mut x131: fiat_p224_u1 = 0;
2207 fiat_p224_addcarryx_u32(&mut x130, &mut x131, x129, x100, (0x0 as u32));
2208 let mut x132: u32 = 0;
2209 let mut x133: fiat_p224_u1 = 0;
2210 fiat_p224_addcarryx_u32(&mut x132, &mut x133, x131, x102, x118);
2211 let mut x134: u32 = 0;
2212 let mut x135: fiat_p224_u1 = 0;
2213 fiat_p224_addcarryx_u32(&mut x134, &mut x135, x133, x104, x120);
2214 let mut x136: u32 = 0;
2215 let mut x137: fiat_p224_u1 = 0;
2216 fiat_p224_addcarryx_u32(&mut x136, &mut x137, x135, x106, x122);
2217 let mut x138: u32 = 0;
2218 let mut x139: fiat_p224_u1 = 0;
2219 fiat_p224_addcarryx_u32(&mut x138, &mut x139, x137, x108, x124);
2220 let mut x140: u32 = 0;
2221 let mut x141: fiat_p224_u1 = 0;
2222 fiat_p224_addcarryx_u32(&mut x140, &mut x141, x139, ((x109 as u32) + (x95 as u32)), ((x125 as u32) + x113));
2223 let mut x142: u32 = 0;
2224 let mut x143: fiat_p224_u1 = 0;
2225 fiat_p224_addcarryx_u32(&mut x142, &mut x143, 0x0, x128, (arg1[4]));
2226 let mut x144: u32 = 0;
2227 let mut x145: fiat_p224_u1 = 0;
2228 fiat_p224_addcarryx_u32(&mut x144, &mut x145, x143, x130, (0x0 as u32));
2229 let mut x146: u32 = 0;
2230 let mut x147: fiat_p224_u1 = 0;
2231 fiat_p224_addcarryx_u32(&mut x146, &mut x147, x145, x132, (0x0 as u32));
2232 let mut x148: u32 = 0;
2233 let mut x149: fiat_p224_u1 = 0;
2234 fiat_p224_addcarryx_u32(&mut x148, &mut x149, x147, x134, (0x0 as u32));
2235 let mut x150: u32 = 0;
2236 let mut x151: fiat_p224_u1 = 0;
2237 fiat_p224_addcarryx_u32(&mut x150, &mut x151, x149, x136, (0x0 as u32));
2238 let mut x152: u32 = 0;
2239 let mut x153: fiat_p224_u1 = 0;
2240 fiat_p224_addcarryx_u32(&mut x152, &mut x153, x151, x138, (0x0 as u32));
2241 let mut x154: u32 = 0;
2242 let mut x155: fiat_p224_u1 = 0;
2243 fiat_p224_addcarryx_u32(&mut x154, &mut x155, x153, x140, (0x0 as u32));
2244 let mut x156: u32 = 0;
2245 let mut x157: u32 = 0;
2246 fiat_p224_mulx_u32(&mut x156, &mut x157, x142, 0xffffffff);
2247 let mut x158: u32 = 0;
2248 let mut x159: u32 = 0;
2249 fiat_p224_mulx_u32(&mut x158, &mut x159, x156, 0xffffffff);
2250 let mut x160: u32 = 0;
2251 let mut x161: u32 = 0;
2252 fiat_p224_mulx_u32(&mut x160, &mut x161, x156, 0xffffffff);
2253 let mut x162: u32 = 0;
2254 let mut x163: u32 = 0;
2255 fiat_p224_mulx_u32(&mut x162, &mut x163, x156, 0xffffffff);
2256 let mut x164: u32 = 0;
2257 let mut x165: u32 = 0;
2258 fiat_p224_mulx_u32(&mut x164, &mut x165, x156, 0xffffffff);
2259 let mut x166: u32 = 0;
2260 let mut x167: fiat_p224_u1 = 0;
2261 fiat_p224_addcarryx_u32(&mut x166, &mut x167, 0x0, x165, x162);
2262 let mut x168: u32 = 0;
2263 let mut x169: fiat_p224_u1 = 0;
2264 fiat_p224_addcarryx_u32(&mut x168, &mut x169, x167, x163, x160);
2265 let mut x170: u32 = 0;
2266 let mut x171: fiat_p224_u1 = 0;
2267 fiat_p224_addcarryx_u32(&mut x170, &mut x171, x169, x161, x158);
2268 let mut x172: u32 = 0;
2269 let mut x173: fiat_p224_u1 = 0;
2270 fiat_p224_addcarryx_u32(&mut x172, &mut x173, 0x0, x142, x156);
2271 let mut x174: u32 = 0;
2272 let mut x175: fiat_p224_u1 = 0;
2273 fiat_p224_addcarryx_u32(&mut x174, &mut x175, x173, x144, (0x0 as u32));
2274 let mut x176: u32 = 0;
2275 let mut x177: fiat_p224_u1 = 0;
2276 fiat_p224_addcarryx_u32(&mut x176, &mut x177, x175, x146, (0x0 as u32));
2277 let mut x178: u32 = 0;
2278 let mut x179: fiat_p224_u1 = 0;
2279 fiat_p224_addcarryx_u32(&mut x178, &mut x179, x177, x148, x164);
2280 let mut x180: u32 = 0;
2281 let mut x181: fiat_p224_u1 = 0;
2282 fiat_p224_addcarryx_u32(&mut x180, &mut x181, x179, x150, x166);
2283 let mut x182: u32 = 0;
2284 let mut x183: fiat_p224_u1 = 0;
2285 fiat_p224_addcarryx_u32(&mut x182, &mut x183, x181, x152, x168);
2286 let mut x184: u32 = 0;
2287 let mut x185: fiat_p224_u1 = 0;
2288 fiat_p224_addcarryx_u32(&mut x184, &mut x185, x183, x154, x170);
2289 let mut x186: u32 = 0;
2290 let mut x187: fiat_p224_u1 = 0;
2291 fiat_p224_addcarryx_u32(&mut x186, &mut x187, x185, ((x155 as u32) + (x141 as u32)), ((x171 as u32) + x159));
2292 let mut x188: u32 = 0;
2293 let mut x189: fiat_p224_u1 = 0;
2294 fiat_p224_addcarryx_u32(&mut x188, &mut x189, 0x0, x174, (arg1[5]));
2295 let mut x190: u32 = 0;
2296 let mut x191: fiat_p224_u1 = 0;
2297 fiat_p224_addcarryx_u32(&mut x190, &mut x191, x189, x176, (0x0 as u32));
2298 let mut x192: u32 = 0;
2299 let mut x193: fiat_p224_u1 = 0;
2300 fiat_p224_addcarryx_u32(&mut x192, &mut x193, x191, x178, (0x0 as u32));
2301 let mut x194: u32 = 0;
2302 let mut x195: fiat_p224_u1 = 0;
2303 fiat_p224_addcarryx_u32(&mut x194, &mut x195, x193, x180, (0x0 as u32));
2304 let mut x196: u32 = 0;
2305 let mut x197: fiat_p224_u1 = 0;
2306 fiat_p224_addcarryx_u32(&mut x196, &mut x197, x195, x182, (0x0 as u32));
2307 let mut x198: u32 = 0;
2308 let mut x199: fiat_p224_u1 = 0;
2309 fiat_p224_addcarryx_u32(&mut x198, &mut x199, x197, x184, (0x0 as u32));
2310 let mut x200: u32 = 0;
2311 let mut x201: fiat_p224_u1 = 0;
2312 fiat_p224_addcarryx_u32(&mut x200, &mut x201, x199, x186, (0x0 as u32));
2313 let mut x202: u32 = 0;
2314 let mut x203: u32 = 0;
2315 fiat_p224_mulx_u32(&mut x202, &mut x203, x188, 0xffffffff);
2316 let mut x204: u32 = 0;
2317 let mut x205: u32 = 0;
2318 fiat_p224_mulx_u32(&mut x204, &mut x205, x202, 0xffffffff);
2319 let mut x206: u32 = 0;
2320 let mut x207: u32 = 0;
2321 fiat_p224_mulx_u32(&mut x206, &mut x207, x202, 0xffffffff);
2322 let mut x208: u32 = 0;
2323 let mut x209: u32 = 0;
2324 fiat_p224_mulx_u32(&mut x208, &mut x209, x202, 0xffffffff);
2325 let mut x210: u32 = 0;
2326 let mut x211: u32 = 0;
2327 fiat_p224_mulx_u32(&mut x210, &mut x211, x202, 0xffffffff);
2328 let mut x212: u32 = 0;
2329 let mut x213: fiat_p224_u1 = 0;
2330 fiat_p224_addcarryx_u32(&mut x212, &mut x213, 0x0, x211, x208);
2331 let mut x214: u32 = 0;
2332 let mut x215: fiat_p224_u1 = 0;
2333 fiat_p224_addcarryx_u32(&mut x214, &mut x215, x213, x209, x206);
2334 let mut x216: u32 = 0;
2335 let mut x217: fiat_p224_u1 = 0;
2336 fiat_p224_addcarryx_u32(&mut x216, &mut x217, x215, x207, x204);
2337 let mut x218: u32 = 0;
2338 let mut x219: fiat_p224_u1 = 0;
2339 fiat_p224_addcarryx_u32(&mut x218, &mut x219, 0x0, x188, x202);
2340 let mut x220: u32 = 0;
2341 let mut x221: fiat_p224_u1 = 0;
2342 fiat_p224_addcarryx_u32(&mut x220, &mut x221, x219, x190, (0x0 as u32));
2343 let mut x222: u32 = 0;
2344 let mut x223: fiat_p224_u1 = 0;
2345 fiat_p224_addcarryx_u32(&mut x222, &mut x223, x221, x192, (0x0 as u32));
2346 let mut x224: u32 = 0;
2347 let mut x225: fiat_p224_u1 = 0;
2348 fiat_p224_addcarryx_u32(&mut x224, &mut x225, x223, x194, x210);
2349 let mut x226: u32 = 0;
2350 let mut x227: fiat_p224_u1 = 0;
2351 fiat_p224_addcarryx_u32(&mut x226, &mut x227, x225, x196, x212);
2352 let mut x228: u32 = 0;
2353 let mut x229: fiat_p224_u1 = 0;
2354 fiat_p224_addcarryx_u32(&mut x228, &mut x229, x227, x198, x214);
2355 let mut x230: u32 = 0;
2356 let mut x231: fiat_p224_u1 = 0;
2357 fiat_p224_addcarryx_u32(&mut x230, &mut x231, x229, x200, x216);
2358 let mut x232: u32 = 0;
2359 let mut x233: fiat_p224_u1 = 0;
2360 fiat_p224_addcarryx_u32(&mut x232, &mut x233, x231, ((x201 as u32) + (x187 as u32)), ((x217 as u32) + x205));
2361 let mut x234: u32 = 0;
2362 let mut x235: fiat_p224_u1 = 0;
2363 fiat_p224_addcarryx_u32(&mut x234, &mut x235, 0x0, x220, (arg1[6]));
2364 let mut x236: u32 = 0;
2365 let mut x237: fiat_p224_u1 = 0;
2366 fiat_p224_addcarryx_u32(&mut x236, &mut x237, x235, x222, (0x0 as u32));
2367 let mut x238: u32 = 0;
2368 let mut x239: fiat_p224_u1 = 0;
2369 fiat_p224_addcarryx_u32(&mut x238, &mut x239, x237, x224, (0x0 as u32));
2370 let mut x240: u32 = 0;
2371 let mut x241: fiat_p224_u1 = 0;
2372 fiat_p224_addcarryx_u32(&mut x240, &mut x241, x239, x226, (0x0 as u32));
2373 let mut x242: u32 = 0;
2374 let mut x243: fiat_p224_u1 = 0;
2375 fiat_p224_addcarryx_u32(&mut x242, &mut x243, x241, x228, (0x0 as u32));
2376 let mut x244: u32 = 0;
2377 let mut x245: fiat_p224_u1 = 0;
2378 fiat_p224_addcarryx_u32(&mut x244, &mut x245, x243, x230, (0x0 as u32));
2379 let mut x246: u32 = 0;
2380 let mut x247: fiat_p224_u1 = 0;
2381 fiat_p224_addcarryx_u32(&mut x246, &mut x247, x245, x232, (0x0 as u32));
2382 let mut x248: u32 = 0;
2383 let mut x249: u32 = 0;
2384 fiat_p224_mulx_u32(&mut x248, &mut x249, x234, 0xffffffff);
2385 let mut x250: u32 = 0;
2386 let mut x251: u32 = 0;
2387 fiat_p224_mulx_u32(&mut x250, &mut x251, x248, 0xffffffff);
2388 let mut x252: u32 = 0;
2389 let mut x253: u32 = 0;
2390 fiat_p224_mulx_u32(&mut x252, &mut x253, x248, 0xffffffff);
2391 let mut x254: u32 = 0;
2392 let mut x255: u32 = 0;
2393 fiat_p224_mulx_u32(&mut x254, &mut x255, x248, 0xffffffff);
2394 let mut x256: u32 = 0;
2395 let mut x257: u32 = 0;
2396 fiat_p224_mulx_u32(&mut x256, &mut x257, x248, 0xffffffff);
2397 let mut x258: u32 = 0;
2398 let mut x259: fiat_p224_u1 = 0;
2399 fiat_p224_addcarryx_u32(&mut x258, &mut x259, 0x0, x257, x254);
2400 let mut x260: u32 = 0;
2401 let mut x261: fiat_p224_u1 = 0;
2402 fiat_p224_addcarryx_u32(&mut x260, &mut x261, x259, x255, x252);
2403 let mut x262: u32 = 0;
2404 let mut x263: fiat_p224_u1 = 0;
2405 fiat_p224_addcarryx_u32(&mut x262, &mut x263, x261, x253, x250);
2406 let mut x264: u32 = 0;
2407 let mut x265: fiat_p224_u1 = 0;
2408 fiat_p224_addcarryx_u32(&mut x264, &mut x265, 0x0, x234, x248);
2409 let mut x266: u32 = 0;
2410 let mut x267: fiat_p224_u1 = 0;
2411 fiat_p224_addcarryx_u32(&mut x266, &mut x267, x265, x236, (0x0 as u32));
2412 let mut x268: u32 = 0;
2413 let mut x269: fiat_p224_u1 = 0;
2414 fiat_p224_addcarryx_u32(&mut x268, &mut x269, x267, x238, (0x0 as u32));
2415 let mut x270: u32 = 0;
2416 let mut x271: fiat_p224_u1 = 0;
2417 fiat_p224_addcarryx_u32(&mut x270, &mut x271, x269, x240, x256);
2418 let mut x272: u32 = 0;
2419 let mut x273: fiat_p224_u1 = 0;
2420 fiat_p224_addcarryx_u32(&mut x272, &mut x273, x271, x242, x258);
2421 let mut x274: u32 = 0;
2422 let mut x275: fiat_p224_u1 = 0;
2423 fiat_p224_addcarryx_u32(&mut x274, &mut x275, x273, x244, x260);
2424 let mut x276: u32 = 0;
2425 let mut x277: fiat_p224_u1 = 0;
2426 fiat_p224_addcarryx_u32(&mut x276, &mut x277, x275, x246, x262);
2427 let mut x278: u32 = 0;
2428 let mut x279: fiat_p224_u1 = 0;
2429 fiat_p224_addcarryx_u32(&mut x278, &mut x279, x277, ((x247 as u32) + (x233 as u32)), ((x263 as u32) + x251));
2430 let mut x280: u32 = 0;
2431 let mut x281: fiat_p224_u1 = 0;
2432 fiat_p224_subborrowx_u32(&mut x280, &mut x281, 0x0, x266, (0x1 as u32));
2433 let mut x282: u32 = 0;
2434 let mut x283: fiat_p224_u1 = 0;
2435 fiat_p224_subborrowx_u32(&mut x282, &mut x283, x281, x268, (0x0 as u32));
2436 let mut x284: u32 = 0;
2437 let mut x285: fiat_p224_u1 = 0;
2438 fiat_p224_subborrowx_u32(&mut x284, &mut x285, x283, x270, (0x0 as u32));
2439 let mut x286: u32 = 0;
2440 let mut x287: fiat_p224_u1 = 0;
2441 fiat_p224_subborrowx_u32(&mut x286, &mut x287, x285, x272, 0xffffffff);
2442 let mut x288: u32 = 0;
2443 let mut x289: fiat_p224_u1 = 0;
2444 fiat_p224_subborrowx_u32(&mut x288, &mut x289, x287, x274, 0xffffffff);
2445 let mut x290: u32 = 0;
2446 let mut x291: fiat_p224_u1 = 0;
2447 fiat_p224_subborrowx_u32(&mut x290, &mut x291, x289, x276, 0xffffffff);
2448 let mut x292: u32 = 0;
2449 let mut x293: fiat_p224_u1 = 0;
2450 fiat_p224_subborrowx_u32(&mut x292, &mut x293, x291, x278, 0xffffffff);
2451 let mut x294: u32 = 0;
2452 let mut x295: fiat_p224_u1 = 0;
2453 fiat_p224_subborrowx_u32(&mut x294, &mut x295, x293, (x279 as u32), (0x0 as u32));
2454 let mut x296: u32 = 0;
2455 fiat_p224_cmovznz_u32(&mut x296, x295, x280, x266);
2456 let mut x297: u32 = 0;
2457 fiat_p224_cmovznz_u32(&mut x297, x295, x282, x268);
2458 let mut x298: u32 = 0;
2459 fiat_p224_cmovznz_u32(&mut x298, x295, x284, x270);
2460 let mut x299: u32 = 0;
2461 fiat_p224_cmovznz_u32(&mut x299, x295, x286, x272);
2462 let mut x300: u32 = 0;
2463 fiat_p224_cmovznz_u32(&mut x300, x295, x288, x274);
2464 let mut x301: u32 = 0;
2465 fiat_p224_cmovznz_u32(&mut x301, x295, x290, x276);
2466 let mut x302: u32 = 0;
2467 fiat_p224_cmovznz_u32(&mut x302, x295, x292, x278);
2468 out1[0] = x296;
2469 out1[1] = x297;
2470 out1[2] = x298;
2471 out1[3] = x299;
2472 out1[4] = x300;
2473 out1[5] = x301;
2474 out1[6] = x302;
2475}
2476
2477/// The function fiat_p224_to_montgomery translates a field element into the Montgomery domain.
2478///
2479/// Preconditions:
2480/// 0 ≤ eval arg1 < m
2481/// Postconditions:
2482/// eval (from_montgomery out1) mod m = eval arg1 mod m
2483/// 0 ≤ eval out1 < m
2484///
2485#[inline]
2486pub fn fiat_p224_to_montgomery(out1: &mut fiat_p224_montgomery_domain_field_element, arg1: &fiat_p224_non_montgomery_domain_field_element) -> () {
2487 let x1: u32 = (arg1[1]);
2488 let x2: u32 = (arg1[2]);
2489 let x3: u32 = (arg1[3]);
2490 let x4: u32 = (arg1[4]);
2491 let x5: u32 = (arg1[5]);
2492 let x6: u32 = (arg1[6]);
2493 let x7: u32 = (arg1[0]);
2494 let mut x8: u32 = 0;
2495 let mut x9: u32 = 0;
2496 fiat_p224_mulx_u32(&mut x8, &mut x9, x7, 0xffffffff);
2497 let mut x10: u32 = 0;
2498 let mut x11: u32 = 0;
2499 fiat_p224_mulx_u32(&mut x10, &mut x11, x7, 0xffffffff);
2500 let mut x12: u32 = 0;
2501 let mut x13: u32 = 0;
2502 fiat_p224_mulx_u32(&mut x12, &mut x13, x7, 0xfffffffe);
2503 let mut x14: u32 = 0;
2504 let mut x15: fiat_p224_u1 = 0;
2505 fiat_p224_addcarryx_u32(&mut x14, &mut x15, 0x0, x13, x10);
2506 let mut x16: u32 = 0;
2507 let mut x17: fiat_p224_u1 = 0;
2508 fiat_p224_addcarryx_u32(&mut x16, &mut x17, x15, x11, x8);
2509 let mut x18: u32 = 0;
2510 let mut x19: u32 = 0;
2511 fiat_p224_mulx_u32(&mut x18, &mut x19, x7, 0xffffffff);
2512 let mut x20: u32 = 0;
2513 let mut x21: u32 = 0;
2514 fiat_p224_mulx_u32(&mut x20, &mut x21, x18, 0xffffffff);
2515 let mut x22: u32 = 0;
2516 let mut x23: u32 = 0;
2517 fiat_p224_mulx_u32(&mut x22, &mut x23, x18, 0xffffffff);
2518 let mut x24: u32 = 0;
2519 let mut x25: u32 = 0;
2520 fiat_p224_mulx_u32(&mut x24, &mut x25, x18, 0xffffffff);
2521 let mut x26: u32 = 0;
2522 let mut x27: u32 = 0;
2523 fiat_p224_mulx_u32(&mut x26, &mut x27, x18, 0xffffffff);
2524 let mut x28: u32 = 0;
2525 let mut x29: fiat_p224_u1 = 0;
2526 fiat_p224_addcarryx_u32(&mut x28, &mut x29, 0x0, x27, x24);
2527 let mut x30: u32 = 0;
2528 let mut x31: fiat_p224_u1 = 0;
2529 fiat_p224_addcarryx_u32(&mut x30, &mut x31, x29, x25, x22);
2530 let mut x32: u32 = 0;
2531 let mut x33: fiat_p224_u1 = 0;
2532 fiat_p224_addcarryx_u32(&mut x32, &mut x33, x31, x23, x20);
2533 let mut x34: u32 = 0;
2534 let mut x35: fiat_p224_u1 = 0;
2535 fiat_p224_addcarryx_u32(&mut x34, &mut x35, 0x0, x12, x26);
2536 let mut x36: u32 = 0;
2537 let mut x37: fiat_p224_u1 = 0;
2538 fiat_p224_addcarryx_u32(&mut x36, &mut x37, x35, x14, x28);
2539 let mut x38: u32 = 0;
2540 let mut x39: fiat_p224_u1 = 0;
2541 fiat_p224_addcarryx_u32(&mut x38, &mut x39, x37, x16, x30);
2542 let mut x40: u32 = 0;
2543 let mut x41: fiat_p224_u1 = 0;
2544 fiat_p224_addcarryx_u32(&mut x40, &mut x41, x39, ((x17 as u32) + x9), x32);
2545 let mut x42: u32 = 0;
2546 let mut x43: fiat_p224_u1 = 0;
2547 fiat_p224_addcarryx_u32(&mut x42, &mut x43, x41, (0x0 as u32), ((x33 as u32) + x21));
2548 let mut x44: u32 = 0;
2549 let mut x45: u32 = 0;
2550 fiat_p224_mulx_u32(&mut x44, &mut x45, x1, 0xffffffff);
2551 let mut x46: u32 = 0;
2552 let mut x47: u32 = 0;
2553 fiat_p224_mulx_u32(&mut x46, &mut x47, x1, 0xffffffff);
2554 let mut x48: u32 = 0;
2555 let mut x49: u32 = 0;
2556 fiat_p224_mulx_u32(&mut x48, &mut x49, x1, 0xfffffffe);
2557 let mut x50: u32 = 0;
2558 let mut x51: fiat_p224_u1 = 0;
2559 fiat_p224_addcarryx_u32(&mut x50, &mut x51, 0x0, x49, x46);
2560 let mut x52: u32 = 0;
2561 let mut x53: fiat_p224_u1 = 0;
2562 fiat_p224_addcarryx_u32(&mut x52, &mut x53, x51, x47, x44);
2563 let mut x54: u32 = 0;
2564 let mut x55: fiat_p224_u1 = 0;
2565 fiat_p224_addcarryx_u32(&mut x54, &mut x55, 0x0, x7, x18);
2566 let mut x56: u32 = 0;
2567 let mut x57: fiat_p224_u1 = 0;
2568 fiat_p224_addcarryx_u32(&mut x56, &mut x57, 0x0, (x55 as u32), x1);
2569 let mut x58: u32 = 0;
2570 let mut x59: fiat_p224_u1 = 0;
2571 fiat_p224_addcarryx_u32(&mut x58, &mut x59, 0x0, x36, x48);
2572 let mut x60: u32 = 0;
2573 let mut x61: fiat_p224_u1 = 0;
2574 fiat_p224_addcarryx_u32(&mut x60, &mut x61, x59, x38, x50);
2575 let mut x62: u32 = 0;
2576 let mut x63: fiat_p224_u1 = 0;
2577 fiat_p224_addcarryx_u32(&mut x62, &mut x63, x61, x40, x52);
2578 let mut x64: u32 = 0;
2579 let mut x65: fiat_p224_u1 = 0;
2580 fiat_p224_addcarryx_u32(&mut x64, &mut x65, x63, x42, ((x53 as u32) + x45));
2581 let mut x66: u32 = 0;
2582 let mut x67: u32 = 0;
2583 fiat_p224_mulx_u32(&mut x66, &mut x67, x56, 0xffffffff);
2584 let mut x68: u32 = 0;
2585 let mut x69: u32 = 0;
2586 fiat_p224_mulx_u32(&mut x68, &mut x69, x66, 0xffffffff);
2587 let mut x70: u32 = 0;
2588 let mut x71: u32 = 0;
2589 fiat_p224_mulx_u32(&mut x70, &mut x71, x66, 0xffffffff);
2590 let mut x72: u32 = 0;
2591 let mut x73: u32 = 0;
2592 fiat_p224_mulx_u32(&mut x72, &mut x73, x66, 0xffffffff);
2593 let mut x74: u32 = 0;
2594 let mut x75: u32 = 0;
2595 fiat_p224_mulx_u32(&mut x74, &mut x75, x66, 0xffffffff);
2596 let mut x76: u32 = 0;
2597 let mut x77: fiat_p224_u1 = 0;
2598 fiat_p224_addcarryx_u32(&mut x76, &mut x77, 0x0, x75, x72);
2599 let mut x78: u32 = 0;
2600 let mut x79: fiat_p224_u1 = 0;
2601 fiat_p224_addcarryx_u32(&mut x78, &mut x79, x77, x73, x70);
2602 let mut x80: u32 = 0;
2603 let mut x81: fiat_p224_u1 = 0;
2604 fiat_p224_addcarryx_u32(&mut x80, &mut x81, x79, x71, x68);
2605 let mut x82: u32 = 0;
2606 let mut x83: fiat_p224_u1 = 0;
2607 fiat_p224_addcarryx_u32(&mut x82, &mut x83, 0x0, x58, x74);
2608 let mut x84: u32 = 0;
2609 let mut x85: fiat_p224_u1 = 0;
2610 fiat_p224_addcarryx_u32(&mut x84, &mut x85, x83, x60, x76);
2611 let mut x86: u32 = 0;
2612 let mut x87: fiat_p224_u1 = 0;
2613 fiat_p224_addcarryx_u32(&mut x86, &mut x87, x85, x62, x78);
2614 let mut x88: u32 = 0;
2615 let mut x89: fiat_p224_u1 = 0;
2616 fiat_p224_addcarryx_u32(&mut x88, &mut x89, x87, x64, x80);
2617 let mut x90: u32 = 0;
2618 let mut x91: fiat_p224_u1 = 0;
2619 fiat_p224_addcarryx_u32(&mut x90, &mut x91, x89, ((x65 as u32) + (x43 as u32)), ((x81 as u32) + x69));
2620 let mut x92: u32 = 0;
2621 let mut x93: u32 = 0;
2622 fiat_p224_mulx_u32(&mut x92, &mut x93, x2, 0xffffffff);
2623 let mut x94: u32 = 0;
2624 let mut x95: u32 = 0;
2625 fiat_p224_mulx_u32(&mut x94, &mut x95, x2, 0xffffffff);
2626 let mut x96: u32 = 0;
2627 let mut x97: u32 = 0;
2628 fiat_p224_mulx_u32(&mut x96, &mut x97, x2, 0xfffffffe);
2629 let mut x98: u32 = 0;
2630 let mut x99: fiat_p224_u1 = 0;
2631 fiat_p224_addcarryx_u32(&mut x98, &mut x99, 0x0, x97, x94);
2632 let mut x100: u32 = 0;
2633 let mut x101: fiat_p224_u1 = 0;
2634 fiat_p224_addcarryx_u32(&mut x100, &mut x101, x99, x95, x92);
2635 let mut x102: u32 = 0;
2636 let mut x103: fiat_p224_u1 = 0;
2637 fiat_p224_addcarryx_u32(&mut x102, &mut x103, 0x0, x56, x66);
2638 let mut x104: u32 = 0;
2639 let mut x105: fiat_p224_u1 = 0;
2640 fiat_p224_addcarryx_u32(&mut x104, &mut x105, 0x0, ((x103 as u32) + (x57 as u32)), x2);
2641 let mut x106: u32 = 0;
2642 let mut x107: fiat_p224_u1 = 0;
2643 fiat_p224_addcarryx_u32(&mut x106, &mut x107, x105, x34, (0x0 as u32));
2644 let mut x108: u32 = 0;
2645 let mut x109: fiat_p224_u1 = 0;
2646 fiat_p224_addcarryx_u32(&mut x108, &mut x109, x107, x82, (0x0 as u32));
2647 let mut x110: u32 = 0;
2648 let mut x111: fiat_p224_u1 = 0;
2649 fiat_p224_addcarryx_u32(&mut x110, &mut x111, x109, x84, x96);
2650 let mut x112: u32 = 0;
2651 let mut x113: fiat_p224_u1 = 0;
2652 fiat_p224_addcarryx_u32(&mut x112, &mut x113, x111, x86, x98);
2653 let mut x114: u32 = 0;
2654 let mut x115: fiat_p224_u1 = 0;
2655 fiat_p224_addcarryx_u32(&mut x114, &mut x115, x113, x88, x100);
2656 let mut x116: u32 = 0;
2657 let mut x117: fiat_p224_u1 = 0;
2658 fiat_p224_addcarryx_u32(&mut x116, &mut x117, x115, x90, ((x101 as u32) + x93));
2659 let mut x118: u32 = 0;
2660 let mut x119: u32 = 0;
2661 fiat_p224_mulx_u32(&mut x118, &mut x119, x104, 0xffffffff);
2662 let mut x120: u32 = 0;
2663 let mut x121: u32 = 0;
2664 fiat_p224_mulx_u32(&mut x120, &mut x121, x118, 0xffffffff);
2665 let mut x122: u32 = 0;
2666 let mut x123: u32 = 0;
2667 fiat_p224_mulx_u32(&mut x122, &mut x123, x118, 0xffffffff);
2668 let mut x124: u32 = 0;
2669 let mut x125: u32 = 0;
2670 fiat_p224_mulx_u32(&mut x124, &mut x125, x118, 0xffffffff);
2671 let mut x126: u32 = 0;
2672 let mut x127: u32 = 0;
2673 fiat_p224_mulx_u32(&mut x126, &mut x127, x118, 0xffffffff);
2674 let mut x128: u32 = 0;
2675 let mut x129: fiat_p224_u1 = 0;
2676 fiat_p224_addcarryx_u32(&mut x128, &mut x129, 0x0, x127, x124);
2677 let mut x130: u32 = 0;
2678 let mut x131: fiat_p224_u1 = 0;
2679 fiat_p224_addcarryx_u32(&mut x130, &mut x131, x129, x125, x122);
2680 let mut x132: u32 = 0;
2681 let mut x133: fiat_p224_u1 = 0;
2682 fiat_p224_addcarryx_u32(&mut x132, &mut x133, x131, x123, x120);
2683 let mut x134: u32 = 0;
2684 let mut x135: fiat_p224_u1 = 0;
2685 fiat_p224_addcarryx_u32(&mut x134, &mut x135, 0x0, x104, x118);
2686 let mut x136: u32 = 0;
2687 let mut x137: fiat_p224_u1 = 0;
2688 fiat_p224_addcarryx_u32(&mut x136, &mut x137, x135, x106, (0x0 as u32));
2689 let mut x138: u32 = 0;
2690 let mut x139: fiat_p224_u1 = 0;
2691 fiat_p224_addcarryx_u32(&mut x138, &mut x139, x137, x108, (0x0 as u32));
2692 let mut x140: u32 = 0;
2693 let mut x141: fiat_p224_u1 = 0;
2694 fiat_p224_addcarryx_u32(&mut x140, &mut x141, x139, x110, x126);
2695 let mut x142: u32 = 0;
2696 let mut x143: fiat_p224_u1 = 0;
2697 fiat_p224_addcarryx_u32(&mut x142, &mut x143, x141, x112, x128);
2698 let mut x144: u32 = 0;
2699 let mut x145: fiat_p224_u1 = 0;
2700 fiat_p224_addcarryx_u32(&mut x144, &mut x145, x143, x114, x130);
2701 let mut x146: u32 = 0;
2702 let mut x147: fiat_p224_u1 = 0;
2703 fiat_p224_addcarryx_u32(&mut x146, &mut x147, x145, x116, x132);
2704 let mut x148: u32 = 0;
2705 let mut x149: fiat_p224_u1 = 0;
2706 fiat_p224_addcarryx_u32(&mut x148, &mut x149, x147, ((x117 as u32) + (x91 as u32)), ((x133 as u32) + x121));
2707 let mut x150: u32 = 0;
2708 let mut x151: u32 = 0;
2709 fiat_p224_mulx_u32(&mut x150, &mut x151, x3, 0xffffffff);
2710 let mut x152: u32 = 0;
2711 let mut x153: u32 = 0;
2712 fiat_p224_mulx_u32(&mut x152, &mut x153, x3, 0xffffffff);
2713 let mut x154: u32 = 0;
2714 let mut x155: u32 = 0;
2715 fiat_p224_mulx_u32(&mut x154, &mut x155, x3, 0xfffffffe);
2716 let mut x156: u32 = 0;
2717 let mut x157: fiat_p224_u1 = 0;
2718 fiat_p224_addcarryx_u32(&mut x156, &mut x157, 0x0, x155, x152);
2719 let mut x158: u32 = 0;
2720 let mut x159: fiat_p224_u1 = 0;
2721 fiat_p224_addcarryx_u32(&mut x158, &mut x159, x157, x153, x150);
2722 let mut x160: u32 = 0;
2723 let mut x161: fiat_p224_u1 = 0;
2724 fiat_p224_addcarryx_u32(&mut x160, &mut x161, 0x0, x136, x3);
2725 let mut x162: u32 = 0;
2726 let mut x163: fiat_p224_u1 = 0;
2727 fiat_p224_addcarryx_u32(&mut x162, &mut x163, x161, x138, (0x0 as u32));
2728 let mut x164: u32 = 0;
2729 let mut x165: fiat_p224_u1 = 0;
2730 fiat_p224_addcarryx_u32(&mut x164, &mut x165, x163, x140, (0x0 as u32));
2731 let mut x166: u32 = 0;
2732 let mut x167: fiat_p224_u1 = 0;
2733 fiat_p224_addcarryx_u32(&mut x166, &mut x167, x165, x142, x154);
2734 let mut x168: u32 = 0;
2735 let mut x169: fiat_p224_u1 = 0;
2736 fiat_p224_addcarryx_u32(&mut x168, &mut x169, x167, x144, x156);
2737 let mut x170: u32 = 0;
2738 let mut x171: fiat_p224_u1 = 0;
2739 fiat_p224_addcarryx_u32(&mut x170, &mut x171, x169, x146, x158);
2740 let mut x172: u32 = 0;
2741 let mut x173: fiat_p224_u1 = 0;
2742 fiat_p224_addcarryx_u32(&mut x172, &mut x173, x171, x148, ((x159 as u32) + x151));
2743 let mut x174: u32 = 0;
2744 let mut x175: u32 = 0;
2745 fiat_p224_mulx_u32(&mut x174, &mut x175, x160, 0xffffffff);
2746 let mut x176: u32 = 0;
2747 let mut x177: u32 = 0;
2748 fiat_p224_mulx_u32(&mut x176, &mut x177, x174, 0xffffffff);
2749 let mut x178: u32 = 0;
2750 let mut x179: u32 = 0;
2751 fiat_p224_mulx_u32(&mut x178, &mut x179, x174, 0xffffffff);
2752 let mut x180: u32 = 0;
2753 let mut x181: u32 = 0;
2754 fiat_p224_mulx_u32(&mut x180, &mut x181, x174, 0xffffffff);
2755 let mut x182: u32 = 0;
2756 let mut x183: u32 = 0;
2757 fiat_p224_mulx_u32(&mut x182, &mut x183, x174, 0xffffffff);
2758 let mut x184: u32 = 0;
2759 let mut x185: fiat_p224_u1 = 0;
2760 fiat_p224_addcarryx_u32(&mut x184, &mut x185, 0x0, x183, x180);
2761 let mut x186: u32 = 0;
2762 let mut x187: fiat_p224_u1 = 0;
2763 fiat_p224_addcarryx_u32(&mut x186, &mut x187, x185, x181, x178);
2764 let mut x188: u32 = 0;
2765 let mut x189: fiat_p224_u1 = 0;
2766 fiat_p224_addcarryx_u32(&mut x188, &mut x189, x187, x179, x176);
2767 let mut x190: u32 = 0;
2768 let mut x191: fiat_p224_u1 = 0;
2769 fiat_p224_addcarryx_u32(&mut x190, &mut x191, 0x0, x160, x174);
2770 let mut x192: u32 = 0;
2771 let mut x193: fiat_p224_u1 = 0;
2772 fiat_p224_addcarryx_u32(&mut x192, &mut x193, x191, x162, (0x0 as u32));
2773 let mut x194: u32 = 0;
2774 let mut x195: fiat_p224_u1 = 0;
2775 fiat_p224_addcarryx_u32(&mut x194, &mut x195, x193, x164, (0x0 as u32));
2776 let mut x196: u32 = 0;
2777 let mut x197: fiat_p224_u1 = 0;
2778 fiat_p224_addcarryx_u32(&mut x196, &mut x197, x195, x166, x182);
2779 let mut x198: u32 = 0;
2780 let mut x199: fiat_p224_u1 = 0;
2781 fiat_p224_addcarryx_u32(&mut x198, &mut x199, x197, x168, x184);
2782 let mut x200: u32 = 0;
2783 let mut x201: fiat_p224_u1 = 0;
2784 fiat_p224_addcarryx_u32(&mut x200, &mut x201, x199, x170, x186);
2785 let mut x202: u32 = 0;
2786 let mut x203: fiat_p224_u1 = 0;
2787 fiat_p224_addcarryx_u32(&mut x202, &mut x203, x201, x172, x188);
2788 let mut x204: u32 = 0;
2789 let mut x205: fiat_p224_u1 = 0;
2790 fiat_p224_addcarryx_u32(&mut x204, &mut x205, x203, ((x173 as u32) + (x149 as u32)), ((x189 as u32) + x177));
2791 let mut x206: u32 = 0;
2792 let mut x207: u32 = 0;
2793 fiat_p224_mulx_u32(&mut x206, &mut x207, x4, 0xffffffff);
2794 let mut x208: u32 = 0;
2795 let mut x209: u32 = 0;
2796 fiat_p224_mulx_u32(&mut x208, &mut x209, x4, 0xffffffff);
2797 let mut x210: u32 = 0;
2798 let mut x211: u32 = 0;
2799 fiat_p224_mulx_u32(&mut x210, &mut x211, x4, 0xfffffffe);
2800 let mut x212: u32 = 0;
2801 let mut x213: fiat_p224_u1 = 0;
2802 fiat_p224_addcarryx_u32(&mut x212, &mut x213, 0x0, x211, x208);
2803 let mut x214: u32 = 0;
2804 let mut x215: fiat_p224_u1 = 0;
2805 fiat_p224_addcarryx_u32(&mut x214, &mut x215, x213, x209, x206);
2806 let mut x216: u32 = 0;
2807 let mut x217: fiat_p224_u1 = 0;
2808 fiat_p224_addcarryx_u32(&mut x216, &mut x217, 0x0, x192, x4);
2809 let mut x218: u32 = 0;
2810 let mut x219: fiat_p224_u1 = 0;
2811 fiat_p224_addcarryx_u32(&mut x218, &mut x219, x217, x194, (0x0 as u32));
2812 let mut x220: u32 = 0;
2813 let mut x221: fiat_p224_u1 = 0;
2814 fiat_p224_addcarryx_u32(&mut x220, &mut x221, x219, x196, (0x0 as u32));
2815 let mut x222: u32 = 0;
2816 let mut x223: fiat_p224_u1 = 0;
2817 fiat_p224_addcarryx_u32(&mut x222, &mut x223, x221, x198, x210);
2818 let mut x224: u32 = 0;
2819 let mut x225: fiat_p224_u1 = 0;
2820 fiat_p224_addcarryx_u32(&mut x224, &mut x225, x223, x200, x212);
2821 let mut x226: u32 = 0;
2822 let mut x227: fiat_p224_u1 = 0;
2823 fiat_p224_addcarryx_u32(&mut x226, &mut x227, x225, x202, x214);
2824 let mut x228: u32 = 0;
2825 let mut x229: fiat_p224_u1 = 0;
2826 fiat_p224_addcarryx_u32(&mut x228, &mut x229, x227, x204, ((x215 as u32) + x207));
2827 let mut x230: u32 = 0;
2828 let mut x231: u32 = 0;
2829 fiat_p224_mulx_u32(&mut x230, &mut x231, x216, 0xffffffff);
2830 let mut x232: u32 = 0;
2831 let mut x233: u32 = 0;
2832 fiat_p224_mulx_u32(&mut x232, &mut x233, x230, 0xffffffff);
2833 let mut x234: u32 = 0;
2834 let mut x235: u32 = 0;
2835 fiat_p224_mulx_u32(&mut x234, &mut x235, x230, 0xffffffff);
2836 let mut x236: u32 = 0;
2837 let mut x237: u32 = 0;
2838 fiat_p224_mulx_u32(&mut x236, &mut x237, x230, 0xffffffff);
2839 let mut x238: u32 = 0;
2840 let mut x239: u32 = 0;
2841 fiat_p224_mulx_u32(&mut x238, &mut x239, x230, 0xffffffff);
2842 let mut x240: u32 = 0;
2843 let mut x241: fiat_p224_u1 = 0;
2844 fiat_p224_addcarryx_u32(&mut x240, &mut x241, 0x0, x239, x236);
2845 let mut x242: u32 = 0;
2846 let mut x243: fiat_p224_u1 = 0;
2847 fiat_p224_addcarryx_u32(&mut x242, &mut x243, x241, x237, x234);
2848 let mut x244: u32 = 0;
2849 let mut x245: fiat_p224_u1 = 0;
2850 fiat_p224_addcarryx_u32(&mut x244, &mut x245, x243, x235, x232);
2851 let mut x246: u32 = 0;
2852 let mut x247: fiat_p224_u1 = 0;
2853 fiat_p224_addcarryx_u32(&mut x246, &mut x247, 0x0, x216, x230);
2854 let mut x248: u32 = 0;
2855 let mut x249: fiat_p224_u1 = 0;
2856 fiat_p224_addcarryx_u32(&mut x248, &mut x249, x247, x218, (0x0 as u32));
2857 let mut x250: u32 = 0;
2858 let mut x251: fiat_p224_u1 = 0;
2859 fiat_p224_addcarryx_u32(&mut x250, &mut x251, x249, x220, (0x0 as u32));
2860 let mut x252: u32 = 0;
2861 let mut x253: fiat_p224_u1 = 0;
2862 fiat_p224_addcarryx_u32(&mut x252, &mut x253, x251, x222, x238);
2863 let mut x254: u32 = 0;
2864 let mut x255: fiat_p224_u1 = 0;
2865 fiat_p224_addcarryx_u32(&mut x254, &mut x255, x253, x224, x240);
2866 let mut x256: u32 = 0;
2867 let mut x257: fiat_p224_u1 = 0;
2868 fiat_p224_addcarryx_u32(&mut x256, &mut x257, x255, x226, x242);
2869 let mut x258: u32 = 0;
2870 let mut x259: fiat_p224_u1 = 0;
2871 fiat_p224_addcarryx_u32(&mut x258, &mut x259, x257, x228, x244);
2872 let mut x260: u32 = 0;
2873 let mut x261: fiat_p224_u1 = 0;
2874 fiat_p224_addcarryx_u32(&mut x260, &mut x261, x259, ((x229 as u32) + (x205 as u32)), ((x245 as u32) + x233));
2875 let mut x262: u32 = 0;
2876 let mut x263: u32 = 0;
2877 fiat_p224_mulx_u32(&mut x262, &mut x263, x5, 0xffffffff);
2878 let mut x264: u32 = 0;
2879 let mut x265: u32 = 0;
2880 fiat_p224_mulx_u32(&mut x264, &mut x265, x5, 0xffffffff);
2881 let mut x266: u32 = 0;
2882 let mut x267: u32 = 0;
2883 fiat_p224_mulx_u32(&mut x266, &mut x267, x5, 0xfffffffe);
2884 let mut x268: u32 = 0;
2885 let mut x269: fiat_p224_u1 = 0;
2886 fiat_p224_addcarryx_u32(&mut x268, &mut x269, 0x0, x267, x264);
2887 let mut x270: u32 = 0;
2888 let mut x271: fiat_p224_u1 = 0;
2889 fiat_p224_addcarryx_u32(&mut x270, &mut x271, x269, x265, x262);
2890 let mut x272: u32 = 0;
2891 let mut x273: fiat_p224_u1 = 0;
2892 fiat_p224_addcarryx_u32(&mut x272, &mut x273, 0x0, x248, x5);
2893 let mut x274: u32 = 0;
2894 let mut x275: fiat_p224_u1 = 0;
2895 fiat_p224_addcarryx_u32(&mut x274, &mut x275, x273, x250, (0x0 as u32));
2896 let mut x276: u32 = 0;
2897 let mut x277: fiat_p224_u1 = 0;
2898 fiat_p224_addcarryx_u32(&mut x276, &mut x277, x275, x252, (0x0 as u32));
2899 let mut x278: u32 = 0;
2900 let mut x279: fiat_p224_u1 = 0;
2901 fiat_p224_addcarryx_u32(&mut x278, &mut x279, x277, x254, x266);
2902 let mut x280: u32 = 0;
2903 let mut x281: fiat_p224_u1 = 0;
2904 fiat_p224_addcarryx_u32(&mut x280, &mut x281, x279, x256, x268);
2905 let mut x282: u32 = 0;
2906 let mut x283: fiat_p224_u1 = 0;
2907 fiat_p224_addcarryx_u32(&mut x282, &mut x283, x281, x258, x270);
2908 let mut x284: u32 = 0;
2909 let mut x285: fiat_p224_u1 = 0;
2910 fiat_p224_addcarryx_u32(&mut x284, &mut x285, x283, x260, ((x271 as u32) + x263));
2911 let mut x286: u32 = 0;
2912 let mut x287: u32 = 0;
2913 fiat_p224_mulx_u32(&mut x286, &mut x287, x272, 0xffffffff);
2914 let mut x288: u32 = 0;
2915 let mut x289: u32 = 0;
2916 fiat_p224_mulx_u32(&mut x288, &mut x289, x286, 0xffffffff);
2917 let mut x290: u32 = 0;
2918 let mut x291: u32 = 0;
2919 fiat_p224_mulx_u32(&mut x290, &mut x291, x286, 0xffffffff);
2920 let mut x292: u32 = 0;
2921 let mut x293: u32 = 0;
2922 fiat_p224_mulx_u32(&mut x292, &mut x293, x286, 0xffffffff);
2923 let mut x294: u32 = 0;
2924 let mut x295: u32 = 0;
2925 fiat_p224_mulx_u32(&mut x294, &mut x295, x286, 0xffffffff);
2926 let mut x296: u32 = 0;
2927 let mut x297: fiat_p224_u1 = 0;
2928 fiat_p224_addcarryx_u32(&mut x296, &mut x297, 0x0, x295, x292);
2929 let mut x298: u32 = 0;
2930 let mut x299: fiat_p224_u1 = 0;
2931 fiat_p224_addcarryx_u32(&mut x298, &mut x299, x297, x293, x290);
2932 let mut x300: u32 = 0;
2933 let mut x301: fiat_p224_u1 = 0;
2934 fiat_p224_addcarryx_u32(&mut x300, &mut x301, x299, x291, x288);
2935 let mut x302: u32 = 0;
2936 let mut x303: fiat_p224_u1 = 0;
2937 fiat_p224_addcarryx_u32(&mut x302, &mut x303, 0x0, x272, x286);
2938 let mut x304: u32 = 0;
2939 let mut x305: fiat_p224_u1 = 0;
2940 fiat_p224_addcarryx_u32(&mut x304, &mut x305, x303, x274, (0x0 as u32));
2941 let mut x306: u32 = 0;
2942 let mut x307: fiat_p224_u1 = 0;
2943 fiat_p224_addcarryx_u32(&mut x306, &mut x307, x305, x276, (0x0 as u32));
2944 let mut x308: u32 = 0;
2945 let mut x309: fiat_p224_u1 = 0;
2946 fiat_p224_addcarryx_u32(&mut x308, &mut x309, x307, x278, x294);
2947 let mut x310: u32 = 0;
2948 let mut x311: fiat_p224_u1 = 0;
2949 fiat_p224_addcarryx_u32(&mut x310, &mut x311, x309, x280, x296);
2950 let mut x312: u32 = 0;
2951 let mut x313: fiat_p224_u1 = 0;
2952 fiat_p224_addcarryx_u32(&mut x312, &mut x313, x311, x282, x298);
2953 let mut x314: u32 = 0;
2954 let mut x315: fiat_p224_u1 = 0;
2955 fiat_p224_addcarryx_u32(&mut x314, &mut x315, x313, x284, x300);
2956 let mut x316: u32 = 0;
2957 let mut x317: fiat_p224_u1 = 0;
2958 fiat_p224_addcarryx_u32(&mut x316, &mut x317, x315, ((x285 as u32) + (x261 as u32)), ((x301 as u32) + x289));
2959 let mut x318: u32 = 0;
2960 let mut x319: u32 = 0;
2961 fiat_p224_mulx_u32(&mut x318, &mut x319, x6, 0xffffffff);
2962 let mut x320: u32 = 0;
2963 let mut x321: u32 = 0;
2964 fiat_p224_mulx_u32(&mut x320, &mut x321, x6, 0xffffffff);
2965 let mut x322: u32 = 0;
2966 let mut x323: u32 = 0;
2967 fiat_p224_mulx_u32(&mut x322, &mut x323, x6, 0xfffffffe);
2968 let mut x324: u32 = 0;
2969 let mut x325: fiat_p224_u1 = 0;
2970 fiat_p224_addcarryx_u32(&mut x324, &mut x325, 0x0, x323, x320);
2971 let mut x326: u32 = 0;
2972 let mut x327: fiat_p224_u1 = 0;
2973 fiat_p224_addcarryx_u32(&mut x326, &mut x327, x325, x321, x318);
2974 let mut x328: u32 = 0;
2975 let mut x329: fiat_p224_u1 = 0;
2976 fiat_p224_addcarryx_u32(&mut x328, &mut x329, 0x0, x304, x6);
2977 let mut x330: u32 = 0;
2978 let mut x331: fiat_p224_u1 = 0;
2979 fiat_p224_addcarryx_u32(&mut x330, &mut x331, x329, x306, (0x0 as u32));
2980 let mut x332: u32 = 0;
2981 let mut x333: fiat_p224_u1 = 0;
2982 fiat_p224_addcarryx_u32(&mut x332, &mut x333, x331, x308, (0x0 as u32));
2983 let mut x334: u32 = 0;
2984 let mut x335: fiat_p224_u1 = 0;
2985 fiat_p224_addcarryx_u32(&mut x334, &mut x335, x333, x310, x322);
2986 let mut x336: u32 = 0;
2987 let mut x337: fiat_p224_u1 = 0;
2988 fiat_p224_addcarryx_u32(&mut x336, &mut x337, x335, x312, x324);
2989 let mut x338: u32 = 0;
2990 let mut x339: fiat_p224_u1 = 0;
2991 fiat_p224_addcarryx_u32(&mut x338, &mut x339, x337, x314, x326);
2992 let mut x340: u32 = 0;
2993 let mut x341: fiat_p224_u1 = 0;
2994 fiat_p224_addcarryx_u32(&mut x340, &mut x341, x339, x316, ((x327 as u32) + x319));
2995 let mut x342: u32 = 0;
2996 let mut x343: u32 = 0;
2997 fiat_p224_mulx_u32(&mut x342, &mut x343, x328, 0xffffffff);
2998 let mut x344: u32 = 0;
2999 let mut x345: u32 = 0;
3000 fiat_p224_mulx_u32(&mut x344, &mut x345, x342, 0xffffffff);
3001 let mut x346: u32 = 0;
3002 let mut x347: u32 = 0;
3003 fiat_p224_mulx_u32(&mut x346, &mut x347, x342, 0xffffffff);
3004 let mut x348: u32 = 0;
3005 let mut x349: u32 = 0;
3006 fiat_p224_mulx_u32(&mut x348, &mut x349, x342, 0xffffffff);
3007 let mut x350: u32 = 0;
3008 let mut x351: u32 = 0;
3009 fiat_p224_mulx_u32(&mut x350, &mut x351, x342, 0xffffffff);
3010 let mut x352: u32 = 0;
3011 let mut x353: fiat_p224_u1 = 0;
3012 fiat_p224_addcarryx_u32(&mut x352, &mut x353, 0x0, x351, x348);
3013 let mut x354: u32 = 0;
3014 let mut x355: fiat_p224_u1 = 0;
3015 fiat_p224_addcarryx_u32(&mut x354, &mut x355, x353, x349, x346);
3016 let mut x356: u32 = 0;
3017 let mut x357: fiat_p224_u1 = 0;
3018 fiat_p224_addcarryx_u32(&mut x356, &mut x357, x355, x347, x344);
3019 let mut x358: u32 = 0;
3020 let mut x359: fiat_p224_u1 = 0;
3021 fiat_p224_addcarryx_u32(&mut x358, &mut x359, 0x0, x328, x342);
3022 let mut x360: u32 = 0;
3023 let mut x361: fiat_p224_u1 = 0;
3024 fiat_p224_addcarryx_u32(&mut x360, &mut x361, x359, x330, (0x0 as u32));
3025 let mut x362: u32 = 0;
3026 let mut x363: fiat_p224_u1 = 0;
3027 fiat_p224_addcarryx_u32(&mut x362, &mut x363, x361, x332, (0x0 as u32));
3028 let mut x364: u32 = 0;
3029 let mut x365: fiat_p224_u1 = 0;
3030 fiat_p224_addcarryx_u32(&mut x364, &mut x365, x363, x334, x350);
3031 let mut x366: u32 = 0;
3032 let mut x367: fiat_p224_u1 = 0;
3033 fiat_p224_addcarryx_u32(&mut x366, &mut x367, x365, x336, x352);
3034 let mut x368: u32 = 0;
3035 let mut x369: fiat_p224_u1 = 0;
3036 fiat_p224_addcarryx_u32(&mut x368, &mut x369, x367, x338, x354);
3037 let mut x370: u32 = 0;
3038 let mut x371: fiat_p224_u1 = 0;
3039 fiat_p224_addcarryx_u32(&mut x370, &mut x371, x369, x340, x356);
3040 let mut x372: u32 = 0;
3041 let mut x373: fiat_p224_u1 = 0;
3042 fiat_p224_addcarryx_u32(&mut x372, &mut x373, x371, ((x341 as u32) + (x317 as u32)), ((x357 as u32) + x345));
3043 let mut x374: u32 = 0;
3044 let mut x375: fiat_p224_u1 = 0;
3045 fiat_p224_subborrowx_u32(&mut x374, &mut x375, 0x0, x360, (0x1 as u32));
3046 let mut x376: u32 = 0;
3047 let mut x377: fiat_p224_u1 = 0;
3048 fiat_p224_subborrowx_u32(&mut x376, &mut x377, x375, x362, (0x0 as u32));
3049 let mut x378: u32 = 0;
3050 let mut x379: fiat_p224_u1 = 0;
3051 fiat_p224_subborrowx_u32(&mut x378, &mut x379, x377, x364, (0x0 as u32));
3052 let mut x380: u32 = 0;
3053 let mut x381: fiat_p224_u1 = 0;
3054 fiat_p224_subborrowx_u32(&mut x380, &mut x381, x379, x366, 0xffffffff);
3055 let mut x382: u32 = 0;
3056 let mut x383: fiat_p224_u1 = 0;
3057 fiat_p224_subborrowx_u32(&mut x382, &mut x383, x381, x368, 0xffffffff);
3058 let mut x384: u32 = 0;
3059 let mut x385: fiat_p224_u1 = 0;
3060 fiat_p224_subborrowx_u32(&mut x384, &mut x385, x383, x370, 0xffffffff);
3061 let mut x386: u32 = 0;
3062 let mut x387: fiat_p224_u1 = 0;
3063 fiat_p224_subborrowx_u32(&mut x386, &mut x387, x385, x372, 0xffffffff);
3064 let mut x388: u32 = 0;
3065 let mut x389: fiat_p224_u1 = 0;
3066 fiat_p224_subborrowx_u32(&mut x388, &mut x389, x387, (x373 as u32), (0x0 as u32));
3067 let mut x390: u32 = 0;
3068 fiat_p224_cmovznz_u32(&mut x390, x389, x374, x360);
3069 let mut x391: u32 = 0;
3070 fiat_p224_cmovznz_u32(&mut x391, x389, x376, x362);
3071 let mut x392: u32 = 0;
3072 fiat_p224_cmovznz_u32(&mut x392, x389, x378, x364);
3073 let mut x393: u32 = 0;
3074 fiat_p224_cmovznz_u32(&mut x393, x389, x380, x366);
3075 let mut x394: u32 = 0;
3076 fiat_p224_cmovznz_u32(&mut x394, x389, x382, x368);
3077 let mut x395: u32 = 0;
3078 fiat_p224_cmovznz_u32(&mut x395, x389, x384, x370);
3079 let mut x396: u32 = 0;
3080 fiat_p224_cmovznz_u32(&mut x396, x389, x386, x372);
3081 out1[0] = x390;
3082 out1[1] = x391;
3083 out1[2] = x392;
3084 out1[3] = x393;
3085 out1[4] = x394;
3086 out1[5] = x395;
3087 out1[6] = x396;
3088}
3089
3090/// The function fiat_p224_nonzero outputs a single non-zero word if the input is non-zero and zero otherwise.
3091///
3092/// Preconditions:
3093/// 0 ≤ eval arg1 < m
3094/// Postconditions:
3095/// out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0
3096///
3097/// Input Bounds:
3098/// arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3099/// Output Bounds:
3100/// out1: [0x0 ~> 0xffffffff]
3101#[inline]
3102pub fn fiat_p224_nonzero(out1: &mut u32, arg1: &[u32; 7]) -> () {
3103 let x1: u32 = ((arg1[0]) | ((arg1[1]) | ((arg1[2]) | ((arg1[3]) | ((arg1[4]) | ((arg1[5]) | (arg1[6])))))));
3104 *out1 = x1;
3105}
3106
3107/// The function fiat_p224_selectznz is a multi-limb conditional select.
3108///
3109/// Postconditions:
3110/// out1 = (if arg1 = 0 then arg2 else arg3)
3111///
3112/// Input Bounds:
3113/// arg1: [0x0 ~> 0x1]
3114/// arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3115/// arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3116/// Output Bounds:
3117/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3118#[inline]
3119pub fn fiat_p224_selectznz(out1: &mut [u32; 7], arg1: fiat_p224_u1, arg2: &[u32; 7], arg3: &[u32; 7]) -> () {
3120 let mut x1: u32 = 0;
3121 fiat_p224_cmovznz_u32(&mut x1, arg1, (arg2[0]), (arg3[0]));
3122 let mut x2: u32 = 0;
3123 fiat_p224_cmovznz_u32(&mut x2, arg1, (arg2[1]), (arg3[1]));
3124 let mut x3: u32 = 0;
3125 fiat_p224_cmovznz_u32(&mut x3, arg1, (arg2[2]), (arg3[2]));
3126 let mut x4: u32 = 0;
3127 fiat_p224_cmovznz_u32(&mut x4, arg1, (arg2[3]), (arg3[3]));
3128 let mut x5: u32 = 0;
3129 fiat_p224_cmovznz_u32(&mut x5, arg1, (arg2[4]), (arg3[4]));
3130 let mut x6: u32 = 0;
3131 fiat_p224_cmovznz_u32(&mut x6, arg1, (arg2[5]), (arg3[5]));
3132 let mut x7: u32 = 0;
3133 fiat_p224_cmovznz_u32(&mut x7, arg1, (arg2[6]), (arg3[6]));
3134 out1[0] = x1;
3135 out1[1] = x2;
3136 out1[2] = x3;
3137 out1[3] = x4;
3138 out1[4] = x5;
3139 out1[5] = x6;
3140 out1[6] = x7;
3141}
3142
3143/// The function fiat_p224_to_bytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order.
3144///
3145/// Preconditions:
3146/// 0 ≤ eval arg1 < m
3147/// Postconditions:
3148/// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..27]
3149///
3150/// Input Bounds:
3151/// arg1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3152/// Output Bounds:
3153/// 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]]
3154#[inline]
3155pub fn fiat_p224_to_bytes(out1: &mut [u8; 28], arg1: &[u32; 7]) -> () {
3156 let x1: u32 = (arg1[6]);
3157 let x2: u32 = (arg1[5]);
3158 let x3: u32 = (arg1[4]);
3159 let x4: u32 = (arg1[3]);
3160 let x5: u32 = (arg1[2]);
3161 let x6: u32 = (arg1[1]);
3162 let x7: u32 = (arg1[0]);
3163 let x8: u8 = ((x7 & (0xff as u32)) as u8);
3164 let x9: u32 = (x7 >> 8);
3165 let x10: u8 = ((x9 & (0xff as u32)) as u8);
3166 let x11: u32 = (x9 >> 8);
3167 let x12: u8 = ((x11 & (0xff as u32)) as u8);
3168 let x13: u8 = ((x11 >> 8) as u8);
3169 let x14: u8 = ((x6 & (0xff as u32)) as u8);
3170 let x15: u32 = (x6 >> 8);
3171 let x16: u8 = ((x15 & (0xff as u32)) as u8);
3172 let x17: u32 = (x15 >> 8);
3173 let x18: u8 = ((x17 & (0xff as u32)) as u8);
3174 let x19: u8 = ((x17 >> 8) as u8);
3175 let x20: u8 = ((x5 & (0xff as u32)) as u8);
3176 let x21: u32 = (x5 >> 8);
3177 let x22: u8 = ((x21 & (0xff as u32)) as u8);
3178 let x23: u32 = (x21 >> 8);
3179 let x24: u8 = ((x23 & (0xff as u32)) as u8);
3180 let x25: u8 = ((x23 >> 8) as u8);
3181 let x26: u8 = ((x4 & (0xff as u32)) as u8);
3182 let x27: u32 = (x4 >> 8);
3183 let x28: u8 = ((x27 & (0xff as u32)) as u8);
3184 let x29: u32 = (x27 >> 8);
3185 let x30: u8 = ((x29 & (0xff as u32)) as u8);
3186 let x31: u8 = ((x29 >> 8) as u8);
3187 let x32: u8 = ((x3 & (0xff as u32)) as u8);
3188 let x33: u32 = (x3 >> 8);
3189 let x34: u8 = ((x33 & (0xff as u32)) as u8);
3190 let x35: u32 = (x33 >> 8);
3191 let x36: u8 = ((x35 & (0xff as u32)) as u8);
3192 let x37: u8 = ((x35 >> 8) as u8);
3193 let x38: u8 = ((x2 & (0xff as u32)) as u8);
3194 let x39: u32 = (x2 >> 8);
3195 let x40: u8 = ((x39 & (0xff as u32)) as u8);
3196 let x41: u32 = (x39 >> 8);
3197 let x42: u8 = ((x41 & (0xff as u32)) as u8);
3198 let x43: u8 = ((x41 >> 8) as u8);
3199 let x44: u8 = ((x1 & (0xff as u32)) as u8);
3200 let x45: u32 = (x1 >> 8);
3201 let x46: u8 = ((x45 & (0xff as u32)) as u8);
3202 let x47: u32 = (x45 >> 8);
3203 let x48: u8 = ((x47 & (0xff as u32)) as u8);
3204 let x49: u8 = ((x47 >> 8) as u8);
3205 out1[0] = x8;
3206 out1[1] = x10;
3207 out1[2] = x12;
3208 out1[3] = x13;
3209 out1[4] = x14;
3210 out1[5] = x16;
3211 out1[6] = x18;
3212 out1[7] = x19;
3213 out1[8] = x20;
3214 out1[9] = x22;
3215 out1[10] = x24;
3216 out1[11] = x25;
3217 out1[12] = x26;
3218 out1[13] = x28;
3219 out1[14] = x30;
3220 out1[15] = x31;
3221 out1[16] = x32;
3222 out1[17] = x34;
3223 out1[18] = x36;
3224 out1[19] = x37;
3225 out1[20] = x38;
3226 out1[21] = x40;
3227 out1[22] = x42;
3228 out1[23] = x43;
3229 out1[24] = x44;
3230 out1[25] = x46;
3231 out1[26] = x48;
3232 out1[27] = x49;
3233}
3234
3235/// The function fiat_p224_from_bytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order.
3236///
3237/// Preconditions:
3238/// 0 ≤ bytes_eval arg1 < m
3239/// Postconditions:
3240/// eval out1 mod m = bytes_eval arg1 mod m
3241/// 0 ≤ eval out1 < m
3242///
3243/// Input Bounds:
3244/// 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]]
3245/// Output Bounds:
3246/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3247#[inline]
3248pub fn fiat_p224_from_bytes(out1: &mut [u32; 7], arg1: &[u8; 28]) -> () {
3249 let x1: u32 = (((arg1[27]) as u32) << 24);
3250 let x2: u32 = (((arg1[26]) as u32) << 16);
3251 let x3: u32 = (((arg1[25]) as u32) << 8);
3252 let x4: u8 = (arg1[24]);
3253 let x5: u32 = (((arg1[23]) as u32) << 24);
3254 let x6: u32 = (((arg1[22]) as u32) << 16);
3255 let x7: u32 = (((arg1[21]) as u32) << 8);
3256 let x8: u8 = (arg1[20]);
3257 let x9: u32 = (((arg1[19]) as u32) << 24);
3258 let x10: u32 = (((arg1[18]) as u32) << 16);
3259 let x11: u32 = (((arg1[17]) as u32) << 8);
3260 let x12: u8 = (arg1[16]);
3261 let x13: u32 = (((arg1[15]) as u32) << 24);
3262 let x14: u32 = (((arg1[14]) as u32) << 16);
3263 let x15: u32 = (((arg1[13]) as u32) << 8);
3264 let x16: u8 = (arg1[12]);
3265 let x17: u32 = (((arg1[11]) as u32) << 24);
3266 let x18: u32 = (((arg1[10]) as u32) << 16);
3267 let x19: u32 = (((arg1[9]) as u32) << 8);
3268 let x20: u8 = (arg1[8]);
3269 let x21: u32 = (((arg1[7]) as u32) << 24);
3270 let x22: u32 = (((arg1[6]) as u32) << 16);
3271 let x23: u32 = (((arg1[5]) as u32) << 8);
3272 let x24: u8 = (arg1[4]);
3273 let x25: u32 = (((arg1[3]) as u32) << 24);
3274 let x26: u32 = (((arg1[2]) as u32) << 16);
3275 let x27: u32 = (((arg1[1]) as u32) << 8);
3276 let x28: u8 = (arg1[0]);
3277 let x29: u32 = (x27 + (x28 as u32));
3278 let x30: u32 = (x26 + x29);
3279 let x31: u32 = (x25 + x30);
3280 let x32: u32 = (x23 + (x24 as u32));
3281 let x33: u32 = (x22 + x32);
3282 let x34: u32 = (x21 + x33);
3283 let x35: u32 = (x19 + (x20 as u32));
3284 let x36: u32 = (x18 + x35);
3285 let x37: u32 = (x17 + x36);
3286 let x38: u32 = (x15 + (x16 as u32));
3287 let x39: u32 = (x14 + x38);
3288 let x40: u32 = (x13 + x39);
3289 let x41: u32 = (x11 + (x12 as u32));
3290 let x42: u32 = (x10 + x41);
3291 let x43: u32 = (x9 + x42);
3292 let x44: u32 = (x7 + (x8 as u32));
3293 let x45: u32 = (x6 + x44);
3294 let x46: u32 = (x5 + x45);
3295 let x47: u32 = (x3 + (x4 as u32));
3296 let x48: u32 = (x2 + x47);
3297 let x49: u32 = (x1 + x48);
3298 out1[0] = x31;
3299 out1[1] = x34;
3300 out1[2] = x37;
3301 out1[3] = x40;
3302 out1[4] = x43;
3303 out1[5] = x46;
3304 out1[6] = x49;
3305}
3306
3307/// The function fiat_p224_set_one returns the field element one in the Montgomery domain.
3308///
3309/// Postconditions:
3310/// eval (from_montgomery out1) mod m = 1 mod m
3311/// 0 ≤ eval out1 < m
3312///
3313#[inline]
3314pub fn fiat_p224_set_one(out1: &mut fiat_p224_montgomery_domain_field_element) -> () {
3315 out1[0] = 0xffffffff;
3316 out1[1] = 0xffffffff;
3317 out1[2] = 0xffffffff;
3318 out1[3] = (0x0 as u32);
3319 out1[4] = (0x0 as u32);
3320 out1[5] = (0x0 as u32);
3321 out1[6] = (0x0 as u32);
3322}
3323
3324/// The function fiat_p224_msat returns the saturated representation of the prime modulus.
3325///
3326/// Postconditions:
3327/// twos_complement_eval out1 = m
3328/// 0 ≤ eval out1 < m
3329///
3330/// Output Bounds:
3331/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3332#[inline]
3333pub fn fiat_p224_msat(out1: &mut [u32; 8]) -> () {
3334 out1[0] = (0x1 as u32);
3335 out1[1] = (0x0 as u32);
3336 out1[2] = (0x0 as u32);
3337 out1[3] = 0xffffffff;
3338 out1[4] = 0xffffffff;
3339 out1[5] = 0xffffffff;
3340 out1[6] = 0xffffffff;
3341 out1[7] = (0x0 as u32);
3342}
3343
3344/// The function fiat_p224_divstep computes a divstep.
3345///
3346/// Preconditions:
3347/// 0 ≤ eval arg4 < m
3348/// 0 ≤ eval arg5 < m
3349/// Postconditions:
3350/// out1 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then 1 - arg1 else 1 + arg1)
3351/// twos_complement_eval out2 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then twos_complement_eval arg3 else twos_complement_eval arg2)
3352/// twos_complement_eval out3 = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then ⌊(twos_complement_eval arg3 - twos_complement_eval arg2) / 2⌋ else ⌊(twos_complement_eval arg3 + (twos_complement_eval arg3 mod 2) * twos_complement_eval arg2) / 2⌋)
3353/// eval (from_montgomery out4) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (2 * eval (from_montgomery arg5)) mod m else (2 * eval (from_montgomery arg4)) mod m)
3354/// eval (from_montgomery out5) mod m = (if 0 < arg1 ∧ (twos_complement_eval arg3) is odd then (eval (from_montgomery arg4) - eval (from_montgomery arg4)) mod m else (eval (from_montgomery arg5) + (twos_complement_eval arg3 mod 2) * eval (from_montgomery arg4)) mod m)
3355/// 0 ≤ eval out5 < m
3356/// 0 ≤ eval out5 < m
3357/// 0 ≤ eval out2 < m
3358/// 0 ≤ eval out3 < m
3359///
3360/// Input Bounds:
3361/// arg1: [0x0 ~> 0xffffffff]
3362/// arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3363/// arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3364/// arg4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3365/// arg5: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3366/// Output Bounds:
3367/// out1: [0x0 ~> 0xffffffff]
3368/// out2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3369/// out3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3370/// out4: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3371/// out5: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3372#[inline]
3373pub fn fiat_p224_divstep(out1: &mut u32, out2: &mut [u32; 8], out3: &mut [u32; 8], out4: &mut [u32; 7], out5: &mut [u32; 7], arg1: u32, arg2: &[u32; 8], arg3: &[u32; 8], arg4: &[u32; 7], arg5: &[u32; 7]) -> () {
3374 let mut x1: u32 = 0;
3375 let mut x2: fiat_p224_u1 = 0;
3376 fiat_p224_addcarryx_u32(&mut x1, &mut x2, 0x0, (!arg1), (0x1 as u32));
3377 let x3: fiat_p224_u1 = (((x1 >> 31) as fiat_p224_u1) & (((arg3[0]) & (0x1 as u32)) as fiat_p224_u1));
3378 let mut x4: u32 = 0;
3379 let mut x5: fiat_p224_u1 = 0;
3380 fiat_p224_addcarryx_u32(&mut x4, &mut x5, 0x0, (!arg1), (0x1 as u32));
3381 let mut x6: u32 = 0;
3382 fiat_p224_cmovznz_u32(&mut x6, x3, arg1, x4);
3383 let mut x7: u32 = 0;
3384 fiat_p224_cmovznz_u32(&mut x7, x3, (arg2[0]), (arg3[0]));
3385 let mut x8: u32 = 0;
3386 fiat_p224_cmovznz_u32(&mut x8, x3, (arg2[1]), (arg3[1]));
3387 let mut x9: u32 = 0;
3388 fiat_p224_cmovznz_u32(&mut x9, x3, (arg2[2]), (arg3[2]));
3389 let mut x10: u32 = 0;
3390 fiat_p224_cmovznz_u32(&mut x10, x3, (arg2[3]), (arg3[3]));
3391 let mut x11: u32 = 0;
3392 fiat_p224_cmovznz_u32(&mut x11, x3, (arg2[4]), (arg3[4]));
3393 let mut x12: u32 = 0;
3394 fiat_p224_cmovznz_u32(&mut x12, x3, (arg2[5]), (arg3[5]));
3395 let mut x13: u32 = 0;
3396 fiat_p224_cmovznz_u32(&mut x13, x3, (arg2[6]), (arg3[6]));
3397 let mut x14: u32 = 0;
3398 fiat_p224_cmovznz_u32(&mut x14, x3, (arg2[7]), (arg3[7]));
3399 let mut x15: u32 = 0;
3400 let mut x16: fiat_p224_u1 = 0;
3401 fiat_p224_addcarryx_u32(&mut x15, &mut x16, 0x0, (0x1 as u32), (!(arg2[0])));
3402 let mut x17: u32 = 0;
3403 let mut x18: fiat_p224_u1 = 0;
3404 fiat_p224_addcarryx_u32(&mut x17, &mut x18, x16, (0x0 as u32), (!(arg2[1])));
3405 let mut x19: u32 = 0;
3406 let mut x20: fiat_p224_u1 = 0;
3407 fiat_p224_addcarryx_u32(&mut x19, &mut x20, x18, (0x0 as u32), (!(arg2[2])));
3408 let mut x21: u32 = 0;
3409 let mut x22: fiat_p224_u1 = 0;
3410 fiat_p224_addcarryx_u32(&mut x21, &mut x22, x20, (0x0 as u32), (!(arg2[3])));
3411 let mut x23: u32 = 0;
3412 let mut x24: fiat_p224_u1 = 0;
3413 fiat_p224_addcarryx_u32(&mut x23, &mut x24, x22, (0x0 as u32), (!(arg2[4])));
3414 let mut x25: u32 = 0;
3415 let mut x26: fiat_p224_u1 = 0;
3416 fiat_p224_addcarryx_u32(&mut x25, &mut x26, x24, (0x0 as u32), (!(arg2[5])));
3417 let mut x27: u32 = 0;
3418 let mut x28: fiat_p224_u1 = 0;
3419 fiat_p224_addcarryx_u32(&mut x27, &mut x28, x26, (0x0 as u32), (!(arg2[6])));
3420 let mut x29: u32 = 0;
3421 let mut x30: fiat_p224_u1 = 0;
3422 fiat_p224_addcarryx_u32(&mut x29, &mut x30, x28, (0x0 as u32), (!(arg2[7])));
3423 let mut x31: u32 = 0;
3424 fiat_p224_cmovznz_u32(&mut x31, x3, (arg3[0]), x15);
3425 let mut x32: u32 = 0;
3426 fiat_p224_cmovznz_u32(&mut x32, x3, (arg3[1]), x17);
3427 let mut x33: u32 = 0;
3428 fiat_p224_cmovznz_u32(&mut x33, x3, (arg3[2]), x19);
3429 let mut x34: u32 = 0;
3430 fiat_p224_cmovznz_u32(&mut x34, x3, (arg3[3]), x21);
3431 let mut x35: u32 = 0;
3432 fiat_p224_cmovznz_u32(&mut x35, x3, (arg3[4]), x23);
3433 let mut x36: u32 = 0;
3434 fiat_p224_cmovznz_u32(&mut x36, x3, (arg3[5]), x25);
3435 let mut x37: u32 = 0;
3436 fiat_p224_cmovznz_u32(&mut x37, x3, (arg3[6]), x27);
3437 let mut x38: u32 = 0;
3438 fiat_p224_cmovznz_u32(&mut x38, x3, (arg3[7]), x29);
3439 let mut x39: u32 = 0;
3440 fiat_p224_cmovznz_u32(&mut x39, x3, (arg4[0]), (arg5[0]));
3441 let mut x40: u32 = 0;
3442 fiat_p224_cmovznz_u32(&mut x40, x3, (arg4[1]), (arg5[1]));
3443 let mut x41: u32 = 0;
3444 fiat_p224_cmovznz_u32(&mut x41, x3, (arg4[2]), (arg5[2]));
3445 let mut x42: u32 = 0;
3446 fiat_p224_cmovznz_u32(&mut x42, x3, (arg4[3]), (arg5[3]));
3447 let mut x43: u32 = 0;
3448 fiat_p224_cmovznz_u32(&mut x43, x3, (arg4[4]), (arg5[4]));
3449 let mut x44: u32 = 0;
3450 fiat_p224_cmovznz_u32(&mut x44, x3, (arg4[5]), (arg5[5]));
3451 let mut x45: u32 = 0;
3452 fiat_p224_cmovznz_u32(&mut x45, x3, (arg4[6]), (arg5[6]));
3453 let mut x46: u32 = 0;
3454 let mut x47: fiat_p224_u1 = 0;
3455 fiat_p224_addcarryx_u32(&mut x46, &mut x47, 0x0, x39, x39);
3456 let mut x48: u32 = 0;
3457 let mut x49: fiat_p224_u1 = 0;
3458 fiat_p224_addcarryx_u32(&mut x48, &mut x49, x47, x40, x40);
3459 let mut x50: u32 = 0;
3460 let mut x51: fiat_p224_u1 = 0;
3461 fiat_p224_addcarryx_u32(&mut x50, &mut x51, x49, x41, x41);
3462 let mut x52: u32 = 0;
3463 let mut x53: fiat_p224_u1 = 0;
3464 fiat_p224_addcarryx_u32(&mut x52, &mut x53, x51, x42, x42);
3465 let mut x54: u32 = 0;
3466 let mut x55: fiat_p224_u1 = 0;
3467 fiat_p224_addcarryx_u32(&mut x54, &mut x55, x53, x43, x43);
3468 let mut x56: u32 = 0;
3469 let mut x57: fiat_p224_u1 = 0;
3470 fiat_p224_addcarryx_u32(&mut x56, &mut x57, x55, x44, x44);
3471 let mut x58: u32 = 0;
3472 let mut x59: fiat_p224_u1 = 0;
3473 fiat_p224_addcarryx_u32(&mut x58, &mut x59, x57, x45, x45);
3474 let mut x60: u32 = 0;
3475 let mut x61: fiat_p224_u1 = 0;
3476 fiat_p224_subborrowx_u32(&mut x60, &mut x61, 0x0, x46, (0x1 as u32));
3477 let mut x62: u32 = 0;
3478 let mut x63: fiat_p224_u1 = 0;
3479 fiat_p224_subborrowx_u32(&mut x62, &mut x63, x61, x48, (0x0 as u32));
3480 let mut x64: u32 = 0;
3481 let mut x65: fiat_p224_u1 = 0;
3482 fiat_p224_subborrowx_u32(&mut x64, &mut x65, x63, x50, (0x0 as u32));
3483 let mut x66: u32 = 0;
3484 let mut x67: fiat_p224_u1 = 0;
3485 fiat_p224_subborrowx_u32(&mut x66, &mut x67, x65, x52, 0xffffffff);
3486 let mut x68: u32 = 0;
3487 let mut x69: fiat_p224_u1 = 0;
3488 fiat_p224_subborrowx_u32(&mut x68, &mut x69, x67, x54, 0xffffffff);
3489 let mut x70: u32 = 0;
3490 let mut x71: fiat_p224_u1 = 0;
3491 fiat_p224_subborrowx_u32(&mut x70, &mut x71, x69, x56, 0xffffffff);
3492 let mut x72: u32 = 0;
3493 let mut x73: fiat_p224_u1 = 0;
3494 fiat_p224_subborrowx_u32(&mut x72, &mut x73, x71, x58, 0xffffffff);
3495 let mut x74: u32 = 0;
3496 let mut x75: fiat_p224_u1 = 0;
3497 fiat_p224_subborrowx_u32(&mut x74, &mut x75, x73, (x59 as u32), (0x0 as u32));
3498 let x76: u32 = (arg4[6]);
3499 let x77: u32 = (arg4[5]);
3500 let x78: u32 = (arg4[4]);
3501 let x79: u32 = (arg4[3]);
3502 let x80: u32 = (arg4[2]);
3503 let x81: u32 = (arg4[1]);
3504 let x82: u32 = (arg4[0]);
3505 let mut x83: u32 = 0;
3506 let mut x84: fiat_p224_u1 = 0;
3507 fiat_p224_subborrowx_u32(&mut x83, &mut x84, 0x0, (0x0 as u32), x82);
3508 let mut x85: u32 = 0;
3509 let mut x86: fiat_p224_u1 = 0;
3510 fiat_p224_subborrowx_u32(&mut x85, &mut x86, x84, (0x0 as u32), x81);
3511 let mut x87: u32 = 0;
3512 let mut x88: fiat_p224_u1 = 0;
3513 fiat_p224_subborrowx_u32(&mut x87, &mut x88, x86, (0x0 as u32), x80);
3514 let mut x89: u32 = 0;
3515 let mut x90: fiat_p224_u1 = 0;
3516 fiat_p224_subborrowx_u32(&mut x89, &mut x90, x88, (0x0 as u32), x79);
3517 let mut x91: u32 = 0;
3518 let mut x92: fiat_p224_u1 = 0;
3519 fiat_p224_subborrowx_u32(&mut x91, &mut x92, x90, (0x0 as u32), x78);
3520 let mut x93: u32 = 0;
3521 let mut x94: fiat_p224_u1 = 0;
3522 fiat_p224_subborrowx_u32(&mut x93, &mut x94, x92, (0x0 as u32), x77);
3523 let mut x95: u32 = 0;
3524 let mut x96: fiat_p224_u1 = 0;
3525 fiat_p224_subborrowx_u32(&mut x95, &mut x96, x94, (0x0 as u32), x76);
3526 let mut x97: u32 = 0;
3527 fiat_p224_cmovznz_u32(&mut x97, x96, (0x0 as u32), 0xffffffff);
3528 let mut x98: u32 = 0;
3529 let mut x99: fiat_p224_u1 = 0;
3530 fiat_p224_addcarryx_u32(&mut x98, &mut x99, 0x0, x83, (((x97 & (0x1 as u32)) as fiat_p224_u1) as u32));
3531 let mut x100: u32 = 0;
3532 let mut x101: fiat_p224_u1 = 0;
3533 fiat_p224_addcarryx_u32(&mut x100, &mut x101, x99, x85, (0x0 as u32));
3534 let mut x102: u32 = 0;
3535 let mut x103: fiat_p224_u1 = 0;
3536 fiat_p224_addcarryx_u32(&mut x102, &mut x103, x101, x87, (0x0 as u32));
3537 let mut x104: u32 = 0;
3538 let mut x105: fiat_p224_u1 = 0;
3539 fiat_p224_addcarryx_u32(&mut x104, &mut x105, x103, x89, x97);
3540 let mut x106: u32 = 0;
3541 let mut x107: fiat_p224_u1 = 0;
3542 fiat_p224_addcarryx_u32(&mut x106, &mut x107, x105, x91, x97);
3543 let mut x108: u32 = 0;
3544 let mut x109: fiat_p224_u1 = 0;
3545 fiat_p224_addcarryx_u32(&mut x108, &mut x109, x107, x93, x97);
3546 let mut x110: u32 = 0;
3547 let mut x111: fiat_p224_u1 = 0;
3548 fiat_p224_addcarryx_u32(&mut x110, &mut x111, x109, x95, x97);
3549 let mut x112: u32 = 0;
3550 fiat_p224_cmovznz_u32(&mut x112, x3, (arg5[0]), x98);
3551 let mut x113: u32 = 0;
3552 fiat_p224_cmovznz_u32(&mut x113, x3, (arg5[1]), x100);
3553 let mut x114: u32 = 0;
3554 fiat_p224_cmovznz_u32(&mut x114, x3, (arg5[2]), x102);
3555 let mut x115: u32 = 0;
3556 fiat_p224_cmovznz_u32(&mut x115, x3, (arg5[3]), x104);
3557 let mut x116: u32 = 0;
3558 fiat_p224_cmovznz_u32(&mut x116, x3, (arg5[4]), x106);
3559 let mut x117: u32 = 0;
3560 fiat_p224_cmovznz_u32(&mut x117, x3, (arg5[5]), x108);
3561 let mut x118: u32 = 0;
3562 fiat_p224_cmovznz_u32(&mut x118, x3, (arg5[6]), x110);
3563 let x119: fiat_p224_u1 = ((x31 & (0x1 as u32)) as fiat_p224_u1);
3564 let mut x120: u32 = 0;
3565 fiat_p224_cmovznz_u32(&mut x120, x119, (0x0 as u32), x7);
3566 let mut x121: u32 = 0;
3567 fiat_p224_cmovznz_u32(&mut x121, x119, (0x0 as u32), x8);
3568 let mut x122: u32 = 0;
3569 fiat_p224_cmovznz_u32(&mut x122, x119, (0x0 as u32), x9);
3570 let mut x123: u32 = 0;
3571 fiat_p224_cmovznz_u32(&mut x123, x119, (0x0 as u32), x10);
3572 let mut x124: u32 = 0;
3573 fiat_p224_cmovznz_u32(&mut x124, x119, (0x0 as u32), x11);
3574 let mut x125: u32 = 0;
3575 fiat_p224_cmovznz_u32(&mut x125, x119, (0x0 as u32), x12);
3576 let mut x126: u32 = 0;
3577 fiat_p224_cmovznz_u32(&mut x126, x119, (0x0 as u32), x13);
3578 let mut x127: u32 = 0;
3579 fiat_p224_cmovznz_u32(&mut x127, x119, (0x0 as u32), x14);
3580 let mut x128: u32 = 0;
3581 let mut x129: fiat_p224_u1 = 0;
3582 fiat_p224_addcarryx_u32(&mut x128, &mut x129, 0x0, x31, x120);
3583 let mut x130: u32 = 0;
3584 let mut x131: fiat_p224_u1 = 0;
3585 fiat_p224_addcarryx_u32(&mut x130, &mut x131, x129, x32, x121);
3586 let mut x132: u32 = 0;
3587 let mut x133: fiat_p224_u1 = 0;
3588 fiat_p224_addcarryx_u32(&mut x132, &mut x133, x131, x33, x122);
3589 let mut x134: u32 = 0;
3590 let mut x135: fiat_p224_u1 = 0;
3591 fiat_p224_addcarryx_u32(&mut x134, &mut x135, x133, x34, x123);
3592 let mut x136: u32 = 0;
3593 let mut x137: fiat_p224_u1 = 0;
3594 fiat_p224_addcarryx_u32(&mut x136, &mut x137, x135, x35, x124);
3595 let mut x138: u32 = 0;
3596 let mut x139: fiat_p224_u1 = 0;
3597 fiat_p224_addcarryx_u32(&mut x138, &mut x139, x137, x36, x125);
3598 let mut x140: u32 = 0;
3599 let mut x141: fiat_p224_u1 = 0;
3600 fiat_p224_addcarryx_u32(&mut x140, &mut x141, x139, x37, x126);
3601 let mut x142: u32 = 0;
3602 let mut x143: fiat_p224_u1 = 0;
3603 fiat_p224_addcarryx_u32(&mut x142, &mut x143, x141, x38, x127);
3604 let mut x144: u32 = 0;
3605 fiat_p224_cmovznz_u32(&mut x144, x119, (0x0 as u32), x39);
3606 let mut x145: u32 = 0;
3607 fiat_p224_cmovznz_u32(&mut x145, x119, (0x0 as u32), x40);
3608 let mut x146: u32 = 0;
3609 fiat_p224_cmovznz_u32(&mut x146, x119, (0x0 as u32), x41);
3610 let mut x147: u32 = 0;
3611 fiat_p224_cmovznz_u32(&mut x147, x119, (0x0 as u32), x42);
3612 let mut x148: u32 = 0;
3613 fiat_p224_cmovznz_u32(&mut x148, x119, (0x0 as u32), x43);
3614 let mut x149: u32 = 0;
3615 fiat_p224_cmovznz_u32(&mut x149, x119, (0x0 as u32), x44);
3616 let mut x150: u32 = 0;
3617 fiat_p224_cmovznz_u32(&mut x150, x119, (0x0 as u32), x45);
3618 let mut x151: u32 = 0;
3619 let mut x152: fiat_p224_u1 = 0;
3620 fiat_p224_addcarryx_u32(&mut x151, &mut x152, 0x0, x112, x144);
3621 let mut x153: u32 = 0;
3622 let mut x154: fiat_p224_u1 = 0;
3623 fiat_p224_addcarryx_u32(&mut x153, &mut x154, x152, x113, x145);
3624 let mut x155: u32 = 0;
3625 let mut x156: fiat_p224_u1 = 0;
3626 fiat_p224_addcarryx_u32(&mut x155, &mut x156, x154, x114, x146);
3627 let mut x157: u32 = 0;
3628 let mut x158: fiat_p224_u1 = 0;
3629 fiat_p224_addcarryx_u32(&mut x157, &mut x158, x156, x115, x147);
3630 let mut x159: u32 = 0;
3631 let mut x160: fiat_p224_u1 = 0;
3632 fiat_p224_addcarryx_u32(&mut x159, &mut x160, x158, x116, x148);
3633 let mut x161: u32 = 0;
3634 let mut x162: fiat_p224_u1 = 0;
3635 fiat_p224_addcarryx_u32(&mut x161, &mut x162, x160, x117, x149);
3636 let mut x163: u32 = 0;
3637 let mut x164: fiat_p224_u1 = 0;
3638 fiat_p224_addcarryx_u32(&mut x163, &mut x164, x162, x118, x150);
3639 let mut x165: u32 = 0;
3640 let mut x166: fiat_p224_u1 = 0;
3641 fiat_p224_subborrowx_u32(&mut x165, &mut x166, 0x0, x151, (0x1 as u32));
3642 let mut x167: u32 = 0;
3643 let mut x168: fiat_p224_u1 = 0;
3644 fiat_p224_subborrowx_u32(&mut x167, &mut x168, x166, x153, (0x0 as u32));
3645 let mut x169: u32 = 0;
3646 let mut x170: fiat_p224_u1 = 0;
3647 fiat_p224_subborrowx_u32(&mut x169, &mut x170, x168, x155, (0x0 as u32));
3648 let mut x171: u32 = 0;
3649 let mut x172: fiat_p224_u1 = 0;
3650 fiat_p224_subborrowx_u32(&mut x171, &mut x172, x170, x157, 0xffffffff);
3651 let mut x173: u32 = 0;
3652 let mut x174: fiat_p224_u1 = 0;
3653 fiat_p224_subborrowx_u32(&mut x173, &mut x174, x172, x159, 0xffffffff);
3654 let mut x175: u32 = 0;
3655 let mut x176: fiat_p224_u1 = 0;
3656 fiat_p224_subborrowx_u32(&mut x175, &mut x176, x174, x161, 0xffffffff);
3657 let mut x177: u32 = 0;
3658 let mut x178: fiat_p224_u1 = 0;
3659 fiat_p224_subborrowx_u32(&mut x177, &mut x178, x176, x163, 0xffffffff);
3660 let mut x179: u32 = 0;
3661 let mut x180: fiat_p224_u1 = 0;
3662 fiat_p224_subborrowx_u32(&mut x179, &mut x180, x178, (x164 as u32), (0x0 as u32));
3663 let mut x181: u32 = 0;
3664 let mut x182: fiat_p224_u1 = 0;
3665 fiat_p224_addcarryx_u32(&mut x181, &mut x182, 0x0, x6, (0x1 as u32));
3666 let x183: u32 = ((x128 >> 1) | ((x130 << 31) & 0xffffffff));
3667 let x184: u32 = ((x130 >> 1) | ((x132 << 31) & 0xffffffff));
3668 let x185: u32 = ((x132 >> 1) | ((x134 << 31) & 0xffffffff));
3669 let x186: u32 = ((x134 >> 1) | ((x136 << 31) & 0xffffffff));
3670 let x187: u32 = ((x136 >> 1) | ((x138 << 31) & 0xffffffff));
3671 let x188: u32 = ((x138 >> 1) | ((x140 << 31) & 0xffffffff));
3672 let x189: u32 = ((x140 >> 1) | ((x142 << 31) & 0xffffffff));
3673 let x190: u32 = ((x142 & 0x80000000) | (x142 >> 1));
3674 let mut x191: u32 = 0;
3675 fiat_p224_cmovznz_u32(&mut x191, x75, x60, x46);
3676 let mut x192: u32 = 0;
3677 fiat_p224_cmovznz_u32(&mut x192, x75, x62, x48);
3678 let mut x193: u32 = 0;
3679 fiat_p224_cmovznz_u32(&mut x193, x75, x64, x50);
3680 let mut x194: u32 = 0;
3681 fiat_p224_cmovznz_u32(&mut x194, x75, x66, x52);
3682 let mut x195: u32 = 0;
3683 fiat_p224_cmovznz_u32(&mut x195, x75, x68, x54);
3684 let mut x196: u32 = 0;
3685 fiat_p224_cmovznz_u32(&mut x196, x75, x70, x56);
3686 let mut x197: u32 = 0;
3687 fiat_p224_cmovznz_u32(&mut x197, x75, x72, x58);
3688 let mut x198: u32 = 0;
3689 fiat_p224_cmovznz_u32(&mut x198, x180, x165, x151);
3690 let mut x199: u32 = 0;
3691 fiat_p224_cmovznz_u32(&mut x199, x180, x167, x153);
3692 let mut x200: u32 = 0;
3693 fiat_p224_cmovznz_u32(&mut x200, x180, x169, x155);
3694 let mut x201: u32 = 0;
3695 fiat_p224_cmovznz_u32(&mut x201, x180, x171, x157);
3696 let mut x202: u32 = 0;
3697 fiat_p224_cmovznz_u32(&mut x202, x180, x173, x159);
3698 let mut x203: u32 = 0;
3699 fiat_p224_cmovznz_u32(&mut x203, x180, x175, x161);
3700 let mut x204: u32 = 0;
3701 fiat_p224_cmovznz_u32(&mut x204, x180, x177, x163);
3702 *out1 = x181;
3703 out2[0] = x7;
3704 out2[1] = x8;
3705 out2[2] = x9;
3706 out2[3] = x10;
3707 out2[4] = x11;
3708 out2[5] = x12;
3709 out2[6] = x13;
3710 out2[7] = x14;
3711 out3[0] = x183;
3712 out3[1] = x184;
3713 out3[2] = x185;
3714 out3[3] = x186;
3715 out3[4] = x187;
3716 out3[5] = x188;
3717 out3[6] = x189;
3718 out3[7] = x190;
3719 out4[0] = x191;
3720 out4[1] = x192;
3721 out4[2] = x193;
3722 out4[3] = x194;
3723 out4[4] = x195;
3724 out4[5] = x196;
3725 out4[6] = x197;
3726 out5[0] = x198;
3727 out5[1] = x199;
3728 out5[2] = x200;
3729 out5[3] = x201;
3730 out5[4] = x202;
3731 out5[5] = x203;
3732 out5[6] = x204;
3733}
3734
3735/// The function fiat_p224_divstep_precomp returns the precomputed value for Bernstein-Yang-inversion (in montgomery form).
3736///
3737/// Postconditions:
3738/// eval (from_montgomery out1) = ⌊(m - 1) / 2⌋^(if ⌊log2 m⌋ + 1 < 46 then ⌊(49 * (⌊log2 m⌋ + 1) + 80) / 17⌋ else ⌊(49 * (⌊log2 m⌋ + 1) + 57) / 17⌋)
3739/// 0 ≤ eval out1 < m
3740///
3741/// Output Bounds:
3742/// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
3743#[inline]
3744pub fn fiat_p224_divstep_precomp(out1: &mut [u32; 7]) -> () {
3745 out1[0] = 0x800000;
3746 out1[1] = 0x800000;
3747 out1[2] = 0xfe000000;
3748 out1[3] = 0xffffff;
3749 out1[4] = (0x0 as u32);
3750 out1[5] = 0xff800000;
3751 out1[6] = 0x17fffff;
3752}