1 //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline p448 32 16 '2^448 - 2^224 - 1' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
2 //! curve description: p448
3 //! machine_wordsize = 32 (from "32")
4 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
6 //! s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1")
7 //! tight_bounds_multiplier = 1 (from "")
10 //! carry_chain = [7, 15, 8, 0, 9, 1, 10, 2, 11, 3, 12, 4, 13, 5, 14, 6, 15, 7, 8, 0]
11 //! eval z = z[0] + (z[1] << 28) + (z[2] << 56) + (z[3] << 84) + (z[4] << 112) + (z[5] << 140) + (z[6] << 168) + (z[7] << 196) + (z[8] << 224) + (z[9] << 252) + (z[10] << 0x118) + (z[11] << 0x134) + (z[12] << 0x150) + (z[13] << 0x16c) + (z[14] << 0x188) + (z[15] << 0x1a4)
12 //! bytes_eval z = z[0] + (z[1] << 8) + (z[2] << 16) + (z[3] << 24) + (z[4] << 32) + (z[5] << 40) + (z[6] << 48) + (z[7] << 56) + (z[8] << 64) + (z[9] << 72) + (z[10] << 80) + (z[11] << 88) + (z[12] << 96) + (z[13] << 104) + (z[14] << 112) + (z[15] << 120) + (z[16] << 128) + (z[17] << 136) + (z[18] << 144) + (z[19] << 152) + (z[20] << 160) + (z[21] << 168) + (z[22] << 176) + (z[23] << 184) + (z[24] << 192) + (z[25] << 200) + (z[26] << 208) + (z[27] << 216) + (z[28] << 224) + (z[29] << 232) + (z[30] << 240) + (z[31] << 248) + (z[32] << 256) + (z[33] << 0x108) + (z[34] << 0x110) + (z[35] << 0x118) + (z[36] << 0x120) + (z[37] << 0x128) + (z[38] << 0x130) + (z[39] << 0x138) + (z[40] << 0x140) + (z[41] << 0x148) + (z[42] << 0x150) + (z[43] << 0x158) + (z[44] << 0x160) + (z[45] << 0x168) + (z[46] << 0x170) + (z[47] << 0x178) + (z[48] << 0x180) + (z[49] << 0x188) + (z[50] << 0x190) + (z[51] << 0x198) + (z[52] << 0x1a0) + (z[53] << 0x1a8) + (z[54] << 0x1b0) + (z[55] << 0x1b8)
13 //! balance = [0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffc, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe, 0x1ffffffe]
15 #![allow(unused_parens)]
16 #![allow(non_camel_case_types)]
18 pub type fiat_p448_u1
= u8;
19 pub type fiat_p448_i1
= i8;
20 pub type fiat_p448_u2
= u8;
21 pub type fiat_p448_i2
= i8;
23 /* The type fiat_p448_loose_field_element is a field element with loose bounds. */
24 /* Bounds: [[0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000], [0x0 ~> 0x30000000]] */
25 pub type fiat_p448_loose_field_element
= [u32; 16];
27 /* The type fiat_p448_tight_field_element is a field element with tight bounds. */
28 /* Bounds: [[0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000], [0x0 ~> 0x10000000]] */
29 pub type fiat_p448_tight_field_element
= [u32; 16];
32 /// The function fiat_p448_addcarryx_u28 is an addition with carry.
35 /// out1 = (arg1 + arg2 + arg3) mod 2^28
36 /// out2 = ⌊(arg1 + arg2 + arg3) / 2^28⌋
39 /// arg1: [0x0 ~> 0x1]
40 /// arg2: [0x0 ~> 0xfffffff]
41 /// arg3: [0x0 ~> 0xfffffff]
43 /// out1: [0x0 ~> 0xfffffff]
44 /// out2: [0x0 ~> 0x1]
46 pub fn fiat_p448_addcarryx_u28(out1
: &mut u32, out2
: &mut fiat_p448_u1
, arg1
: fiat_p448_u1
, arg2
: u32, arg3
: u32) -> () {
47 let x1
: u32 = (((arg1
as u32) + arg2
) + arg3
);
48 let x2
: u32 = (x1
& 0xfffffff);
49 let x3
: fiat_p448_u1
= ((x1
>> 28) as fiat_p448_u1
);
54 /// The function fiat_p448_subborrowx_u28 is a subtraction with borrow.
57 /// out1 = (-arg1 + arg2 + -arg3) mod 2^28
58 /// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^28⌋
61 /// arg1: [0x0 ~> 0x1]
62 /// arg2: [0x0 ~> 0xfffffff]
63 /// arg3: [0x0 ~> 0xfffffff]
65 /// out1: [0x0 ~> 0xfffffff]
66 /// out2: [0x0 ~> 0x1]
68 pub fn fiat_p448_subborrowx_u28(out1
: &mut u32, out2
: &mut fiat_p448_u1
, arg1
: fiat_p448_u1
, arg2
: u32, arg3
: u32) -> () {
69 let x1
: i32 = ((((((arg2
as i64) - (arg1
as i64)) as i32) as i64) - (arg3
as i64)) as i32);
70 let x2
: fiat_p448_i1
= ((x1
>> 28) as fiat_p448_i1
);
71 let x3
: u32 = (((x1
as i64) & (0xfffffff as i64)) as u32);
73 *out2
= (((0x0 as fiat_p448_i2
) - (x2
as fiat_p448_i2
)) as fiat_p448_u1
);
76 /// The function fiat_p448_cmovznz_u32 is a single-word conditional move.
79 /// out1 = (if arg1 = 0 then arg2 else arg3)
82 /// arg1: [0x0 ~> 0x1]
83 /// arg2: [0x0 ~> 0xffffffff]
84 /// arg3: [0x0 ~> 0xffffffff]
86 /// out1: [0x0 ~> 0xffffffff]
88 pub fn fiat_p448_cmovznz_u32(out1
: &mut u32, arg1
: fiat_p448_u1
, arg2
: u32, arg3
: u32) -> () {
89 let x1
: fiat_p448_u1
= (!(!arg1
));
90 let x2
: u32 = ((((((0x0 as fiat_p448_i2
) - (x1
as fiat_p448_i2
)) as fiat_p448_i1
) as i64) & (0xffffffff as i64)) as u32);
91 let x3
: u32 = ((x2
& arg3
) | ((!x2
) & arg2
));
95 /// The function fiat_p448_carry_mul multiplies two field elements and reduces the result.
98 /// eval out1 mod m = (eval arg1 * eval arg2) mod m
101 pub fn fiat_p448_carry_mul(out1
: &mut fiat_p448_tight_field_element
, arg1
: &fiat_p448_loose_field_element
, arg2
: &fiat_p448_loose_field_element
) -> () {
102 let x1
: u64 = (((arg1
[15]) as u64) * ((arg2
[15]) as u64));
103 let x2
: u64 = (((arg1
[15]) as u64) * ((arg2
[14]) as u64));
104 let x3
: u64 = (((arg1
[15]) as u64) * ((arg2
[13]) as u64));
105 let x4
: u64 = (((arg1
[15]) as u64) * ((arg2
[12]) as u64));
106 let x5
: u64 = (((arg1
[15]) as u64) * ((arg2
[11]) as u64));
107 let x6
: u64 = (((arg1
[15]) as u64) * ((arg2
[10]) as u64));
108 let x7
: u64 = (((arg1
[15]) as u64) * ((arg2
[9]) as u64));
109 let x8
: u64 = (((arg1
[14]) as u64) * ((arg2
[15]) as u64));
110 let x9
: u64 = (((arg1
[14]) as u64) * ((arg2
[14]) as u64));
111 let x10
: u64 = (((arg1
[14]) as u64) * ((arg2
[13]) as u64));
112 let x11
: u64 = (((arg1
[14]) as u64) * ((arg2
[12]) as u64));
113 let x12
: u64 = (((arg1
[14]) as u64) * ((arg2
[11]) as u64));
114 let x13
: u64 = (((arg1
[14]) as u64) * ((arg2
[10]) as u64));
115 let x14
: u64 = (((arg1
[13]) as u64) * ((arg2
[15]) as u64));
116 let x15
: u64 = (((arg1
[13]) as u64) * ((arg2
[14]) as u64));
117 let x16
: u64 = (((arg1
[13]) as u64) * ((arg2
[13]) as u64));
118 let x17
: u64 = (((arg1
[13]) as u64) * ((arg2
[12]) as u64));
119 let x18
: u64 = (((arg1
[13]) as u64) * ((arg2
[11]) as u64));
120 let x19
: u64 = (((arg1
[12]) as u64) * ((arg2
[15]) as u64));
121 let x20
: u64 = (((arg1
[12]) as u64) * ((arg2
[14]) as u64));
122 let x21
: u64 = (((arg1
[12]) as u64) * ((arg2
[13]) as u64));
123 let x22
: u64 = (((arg1
[12]) as u64) * ((arg2
[12]) as u64));
124 let x23
: u64 = (((arg1
[11]) as u64) * ((arg2
[15]) as u64));
125 let x24
: u64 = (((arg1
[11]) as u64) * ((arg2
[14]) as u64));
126 let x25
: u64 = (((arg1
[11]) as u64) * ((arg2
[13]) as u64));
127 let x26
: u64 = (((arg1
[10]) as u64) * ((arg2
[15]) as u64));
128 let x27
: u64 = (((arg1
[10]) as u64) * ((arg2
[14]) as u64));
129 let x28
: u64 = (((arg1
[9]) as u64) * ((arg2
[15]) as u64));
130 let x29
: u64 = (((arg1
[15]) as u64) * ((arg2
[15]) as u64));
131 let x30
: u64 = (((arg1
[15]) as u64) * ((arg2
[14]) as u64));
132 let x31
: u64 = (((arg1
[15]) as u64) * ((arg2
[13]) as u64));
133 let x32
: u64 = (((arg1
[15]) as u64) * ((arg2
[12]) as u64));
134 let x33
: u64 = (((arg1
[15]) as u64) * ((arg2
[11]) as u64));
135 let x34
: u64 = (((arg1
[15]) as u64) * ((arg2
[10]) as u64));
136 let x35
: u64 = (((arg1
[15]) as u64) * ((arg2
[9]) as u64));
137 let x36
: u64 = (((arg1
[14]) as u64) * ((arg2
[15]) as u64));
138 let x37
: u64 = (((arg1
[14]) as u64) * ((arg2
[14]) as u64));
139 let x38
: u64 = (((arg1
[14]) as u64) * ((arg2
[13]) as u64));
140 let x39
: u64 = (((arg1
[14]) as u64) * ((arg2
[12]) as u64));
141 let x40
: u64 = (((arg1
[14]) as u64) * ((arg2
[11]) as u64));
142 let x41
: u64 = (((arg1
[14]) as u64) * ((arg2
[10]) as u64));
143 let x42
: u64 = (((arg1
[13]) as u64) * ((arg2
[15]) as u64));
144 let x43
: u64 = (((arg1
[13]) as u64) * ((arg2
[14]) as u64));
145 let x44
: u64 = (((arg1
[13]) as u64) * ((arg2
[13]) as u64));
146 let x45
: u64 = (((arg1
[13]) as u64) * ((arg2
[12]) as u64));
147 let x46
: u64 = (((arg1
[13]) as u64) * ((arg2
[11]) as u64));
148 let x47
: u64 = (((arg1
[12]) as u64) * ((arg2
[15]) as u64));
149 let x48
: u64 = (((arg1
[12]) as u64) * ((arg2
[14]) as u64));
150 let x49
: u64 = (((arg1
[12]) as u64) * ((arg2
[13]) as u64));
151 let x50
: u64 = (((arg1
[12]) as u64) * ((arg2
[12]) as u64));
152 let x51
: u64 = (((arg1
[11]) as u64) * ((arg2
[15]) as u64));
153 let x52
: u64 = (((arg1
[11]) as u64) * ((arg2
[14]) as u64));
154 let x53
: u64 = (((arg1
[11]) as u64) * ((arg2
[13]) as u64));
155 let x54
: u64 = (((arg1
[10]) as u64) * ((arg2
[15]) as u64));
156 let x55
: u64 = (((arg1
[10]) as u64) * ((arg2
[14]) as u64));
157 let x56
: u64 = (((arg1
[9]) as u64) * ((arg2
[15]) as u64));
158 let x57
: u64 = (((arg1
[15]) as u64) * ((arg2
[15]) as u64));
159 let x58
: u64 = (((arg1
[15]) as u64) * ((arg2
[14]) as u64));
160 let x59
: u64 = (((arg1
[15]) as u64) * ((arg2
[13]) as u64));
161 let x60
: u64 = (((arg1
[15]) as u64) * ((arg2
[12]) as u64));
162 let x61
: u64 = (((arg1
[15]) as u64) * ((arg2
[11]) as u64));
163 let x62
: u64 = (((arg1
[15]) as u64) * ((arg2
[10]) as u64));
164 let x63
: u64 = (((arg1
[15]) as u64) * ((arg2
[9]) as u64));
165 let x64
: u64 = (((arg1
[15]) as u64) * ((arg2
[8]) as u64));
166 let x65
: u64 = (((arg1
[15]) as u64) * ((arg2
[7]) as u64));
167 let x66
: u64 = (((arg1
[15]) as u64) * ((arg2
[6]) as u64));
168 let x67
: u64 = (((arg1
[15]) as u64) * ((arg2
[5]) as u64));
169 let x68
: u64 = (((arg1
[15]) as u64) * ((arg2
[4]) as u64));
170 let x69
: u64 = (((arg1
[15]) as u64) * ((arg2
[3]) as u64));
171 let x70
: u64 = (((arg1
[15]) as u64) * ((arg2
[2]) as u64));
172 let x71
: u64 = (((arg1
[15]) as u64) * ((arg2
[1]) as u64));
173 let x72
: u64 = (((arg1
[14]) as u64) * ((arg2
[15]) as u64));
174 let x73
: u64 = (((arg1
[14]) as u64) * ((arg2
[14]) as u64));
175 let x74
: u64 = (((arg1
[14]) as u64) * ((arg2
[13]) as u64));
176 let x75
: u64 = (((arg1
[14]) as u64) * ((arg2
[12]) as u64));
177 let x76
: u64 = (((arg1
[14]) as u64) * ((arg2
[11]) as u64));
178 let x77
: u64 = (((arg1
[14]) as u64) * ((arg2
[10]) as u64));
179 let x78
: u64 = (((arg1
[14]) as u64) * ((arg2
[9]) as u64));
180 let x79
: u64 = (((arg1
[14]) as u64) * ((arg2
[8]) as u64));
181 let x80
: u64 = (((arg1
[14]) as u64) * ((arg2
[7]) as u64));
182 let x81
: u64 = (((arg1
[14]) as u64) * ((arg2
[6]) as u64));
183 let x82
: u64 = (((arg1
[14]) as u64) * ((arg2
[5]) as u64));
184 let x83
: u64 = (((arg1
[14]) as u64) * ((arg2
[4]) as u64));
185 let x84
: u64 = (((arg1
[14]) as u64) * ((arg2
[3]) as u64));
186 let x85
: u64 = (((arg1
[14]) as u64) * ((arg2
[2]) as u64));
187 let x86
: u64 = (((arg1
[13]) as u64) * ((arg2
[15]) as u64));
188 let x87
: u64 = (((arg1
[13]) as u64) * ((arg2
[14]) as u64));
189 let x88
: u64 = (((arg1
[13]) as u64) * ((arg2
[13]) as u64));
190 let x89
: u64 = (((arg1
[13]) as u64) * ((arg2
[12]) as u64));
191 let x90
: u64 = (((arg1
[13]) as u64) * ((arg2
[11]) as u64));
192 let x91
: u64 = (((arg1
[13]) as u64) * ((arg2
[10]) as u64));
193 let x92
: u64 = (((arg1
[13]) as u64) * ((arg2
[9]) as u64));
194 let x93
: u64 = (((arg1
[13]) as u64) * ((arg2
[8]) as u64));
195 let x94
: u64 = (((arg1
[13]) as u64) * ((arg2
[7]) as u64));
196 let x95
: u64 = (((arg1
[13]) as u64) * ((arg2
[6]) as u64));
197 let x96
: u64 = (((arg1
[13]) as u64) * ((arg2
[5]) as u64));
198 let x97
: u64 = (((arg1
[13]) as u64) * ((arg2
[4]) as u64));
199 let x98
: u64 = (((arg1
[13]) as u64) * ((arg2
[3]) as u64));
200 let x99
: u64 = (((arg1
[12]) as u64) * ((arg2
[15]) as u64));
201 let x100
: u64 = (((arg1
[12]) as u64) * ((arg2
[14]) as u64));
202 let x101
: u64 = (((arg1
[12]) as u64) * ((arg2
[13]) as u64));
203 let x102
: u64 = (((arg1
[12]) as u64) * ((arg2
[12]) as u64));
204 let x103
: u64 = (((arg1
[12]) as u64) * ((arg2
[11]) as u64));
205 let x104
: u64 = (((arg1
[12]) as u64) * ((arg2
[10]) as u64));
206 let x105
: u64 = (((arg1
[12]) as u64) * ((arg2
[9]) as u64));
207 let x106
: u64 = (((arg1
[12]) as u64) * ((arg2
[8]) as u64));
208 let x107
: u64 = (((arg1
[12]) as u64) * ((arg2
[7]) as u64));
209 let x108
: u64 = (((arg1
[12]) as u64) * ((arg2
[6]) as u64));
210 let x109
: u64 = (((arg1
[12]) as u64) * ((arg2
[5]) as u64));
211 let x110
: u64 = (((arg1
[12]) as u64) * ((arg2
[4]) as u64));
212 let x111
: u64 = (((arg1
[11]) as u64) * ((arg2
[15]) as u64));
213 let x112
: u64 = (((arg1
[11]) as u64) * ((arg2
[14]) as u64));
214 let x113
: u64 = (((arg1
[11]) as u64) * ((arg2
[13]) as u64));
215 let x114
: u64 = (((arg1
[11]) as u64) * ((arg2
[12]) as u64));
216 let x115
: u64 = (((arg1
[11]) as u64) * ((arg2
[11]) as u64));
217 let x116
: u64 = (((arg1
[11]) as u64) * ((arg2
[10]) as u64));
218 let x117
: u64 = (((arg1
[11]) as u64) * ((arg2
[9]) as u64));
219 let x118
: u64 = (((arg1
[11]) as u64) * ((arg2
[8]) as u64));
220 let x119
: u64 = (((arg1
[11]) as u64) * ((arg2
[7]) as u64));
221 let x120
: u64 = (((arg1
[11]) as u64) * ((arg2
[6]) as u64));
222 let x121
: u64 = (((arg1
[11]) as u64) * ((arg2
[5]) as u64));
223 let x122
: u64 = (((arg1
[10]) as u64) * ((arg2
[15]) as u64));
224 let x123
: u64 = (((arg1
[10]) as u64) * ((arg2
[14]) as u64));
225 let x124
: u64 = (((arg1
[10]) as u64) * ((arg2
[13]) as u64));
226 let x125
: u64 = (((arg1
[10]) as u64) * ((arg2
[12]) as u64));
227 let x126
: u64 = (((arg1
[10]) as u64) * ((arg2
[11]) as u64));
228 let x127
: u64 = (((arg1
[10]) as u64) * ((arg2
[10]) as u64));
229 let x128
: u64 = (((arg1
[10]) as u64) * ((arg2
[9]) as u64));
230 let x129
: u64 = (((arg1
[10]) as u64) * ((arg2
[8]) as u64));
231 let x130
: u64 = (((arg1
[10]) as u64) * ((arg2
[7]) as u64));
232 let x131
: u64 = (((arg1
[10]) as u64) * ((arg2
[6]) as u64));
233 let x132
: u64 = (((arg1
[9]) as u64) * ((arg2
[15]) as u64));
234 let x133
: u64 = (((arg1
[9]) as u64) * ((arg2
[14]) as u64));
235 let x134
: u64 = (((arg1
[9]) as u64) * ((arg2
[13]) as u64));
236 let x135
: u64 = (((arg1
[9]) as u64) * ((arg2
[12]) as u64));
237 let x136
: u64 = (((arg1
[9]) as u64) * ((arg2
[11]) as u64));
238 let x137
: u64 = (((arg1
[9]) as u64) * ((arg2
[10]) as u64));
239 let x138
: u64 = (((arg1
[9]) as u64) * ((arg2
[9]) as u64));
240 let x139
: u64 = (((arg1
[9]) as u64) * ((arg2
[8]) as u64));
241 let x140
: u64 = (((arg1
[9]) as u64) * ((arg2
[7]) as u64));
242 let x141
: u64 = (((arg1
[8]) as u64) * ((arg2
[15]) as u64));
243 let x142
: u64 = (((arg1
[8]) as u64) * ((arg2
[14]) as u64));
244 let x143
: u64 = (((arg1
[8]) as u64) * ((arg2
[13]) as u64));
245 let x144
: u64 = (((arg1
[8]) as u64) * ((arg2
[12]) as u64));
246 let x145
: u64 = (((arg1
[8]) as u64) * ((arg2
[11]) as u64));
247 let x146
: u64 = (((arg1
[8]) as u64) * ((arg2
[10]) as u64));
248 let x147
: u64 = (((arg1
[8]) as u64) * ((arg2
[9]) as u64));
249 let x148
: u64 = (((arg1
[8]) as u64) * ((arg2
[8]) as u64));
250 let x149
: u64 = (((arg1
[7]) as u64) * ((arg2
[15]) as u64));
251 let x150
: u64 = (((arg1
[7]) as u64) * ((arg2
[14]) as u64));
252 let x151
: u64 = (((arg1
[7]) as u64) * ((arg2
[13]) as u64));
253 let x152
: u64 = (((arg1
[7]) as u64) * ((arg2
[12]) as u64));
254 let x153
: u64 = (((arg1
[7]) as u64) * ((arg2
[11]) as u64));
255 let x154
: u64 = (((arg1
[7]) as u64) * ((arg2
[10]) as u64));
256 let x155
: u64 = (((arg1
[7]) as u64) * ((arg2
[9]) as u64));
257 let x156
: u64 = (((arg1
[6]) as u64) * ((arg2
[15]) as u64));
258 let x157
: u64 = (((arg1
[6]) as u64) * ((arg2
[14]) as u64));
259 let x158
: u64 = (((arg1
[6]) as u64) * ((arg2
[13]) as u64));
260 let x159
: u64 = (((arg1
[6]) as u64) * ((arg2
[12]) as u64));
261 let x160
: u64 = (((arg1
[6]) as u64) * ((arg2
[11]) as u64));
262 let x161
: u64 = (((arg1
[6]) as u64) * ((arg2
[10]) as u64));
263 let x162
: u64 = (((arg1
[5]) as u64) * ((arg2
[15]) as u64));
264 let x163
: u64 = (((arg1
[5]) as u64) * ((arg2
[14]) as u64));
265 let x164
: u64 = (((arg1
[5]) as u64) * ((arg2
[13]) as u64));
266 let x165
: u64 = (((arg1
[5]) as u64) * ((arg2
[12]) as u64));
267 let x166
: u64 = (((arg1
[5]) as u64) * ((arg2
[11]) as u64));
268 let x167
: u64 = (((arg1
[4]) as u64) * ((arg2
[15]) as u64));
269 let x168
: u64 = (((arg1
[4]) as u64) * ((arg2
[14]) as u64));
270 let x169
: u64 = (((arg1
[4]) as u64) * ((arg2
[13]) as u64));
271 let x170
: u64 = (((arg1
[4]) as u64) * ((arg2
[12]) as u64));
272 let x171
: u64 = (((arg1
[3]) as u64) * ((arg2
[15]) as u64));
273 let x172
: u64 = (((arg1
[3]) as u64) * ((arg2
[14]) as u64));
274 let x173
: u64 = (((arg1
[3]) as u64) * ((arg2
[13]) as u64));
275 let x174
: u64 = (((arg1
[2]) as u64) * ((arg2
[15]) as u64));
276 let x175
: u64 = (((arg1
[2]) as u64) * ((arg2
[14]) as u64));
277 let x176
: u64 = (((arg1
[1]) as u64) * ((arg2
[15]) as u64));
278 let x177
: u64 = (((arg1
[15]) as u64) * ((arg2
[8]) as u64));
279 let x178
: u64 = (((arg1
[15]) as u64) * ((arg2
[7]) as u64));
280 let x179
: u64 = (((arg1
[15]) as u64) * ((arg2
[6]) as u64));
281 let x180
: u64 = (((arg1
[15]) as u64) * ((arg2
[5]) as u64));
282 let x181
: u64 = (((arg1
[15]) as u64) * ((arg2
[4]) as u64));
283 let x182
: u64 = (((arg1
[15]) as u64) * ((arg2
[3]) as u64));
284 let x183
: u64 = (((arg1
[15]) as u64) * ((arg2
[2]) as u64));
285 let x184
: u64 = (((arg1
[15]) as u64) * ((arg2
[1]) as u64));
286 let x185
: u64 = (((arg1
[14]) as u64) * ((arg2
[9]) as u64));
287 let x186
: u64 = (((arg1
[14]) as u64) * ((arg2
[8]) as u64));
288 let x187
: u64 = (((arg1
[14]) as u64) * ((arg2
[7]) as u64));
289 let x188
: u64 = (((arg1
[14]) as u64) * ((arg2
[6]) as u64));
290 let x189
: u64 = (((arg1
[14]) as u64) * ((arg2
[5]) as u64));
291 let x190
: u64 = (((arg1
[14]) as u64) * ((arg2
[4]) as u64));
292 let x191
: u64 = (((arg1
[14]) as u64) * ((arg2
[3]) as u64));
293 let x192
: u64 = (((arg1
[14]) as u64) * ((arg2
[2]) as u64));
294 let x193
: u64 = (((arg1
[13]) as u64) * ((arg2
[10]) as u64));
295 let x194
: u64 = (((arg1
[13]) as u64) * ((arg2
[9]) as u64));
296 let x195
: u64 = (((arg1
[13]) as u64) * ((arg2
[8]) as u64));
297 let x196
: u64 = (((arg1
[13]) as u64) * ((arg2
[7]) as u64));
298 let x197
: u64 = (((arg1
[13]) as u64) * ((arg2
[6]) as u64));
299 let x198
: u64 = (((arg1
[13]) as u64) * ((arg2
[5]) as u64));
300 let x199
: u64 = (((arg1
[13]) as u64) * ((arg2
[4]) as u64));
301 let x200
: u64 = (((arg1
[13]) as u64) * ((arg2
[3]) as u64));
302 let x201
: u64 = (((arg1
[12]) as u64) * ((arg2
[11]) as u64));
303 let x202
: u64 = (((arg1
[12]) as u64) * ((arg2
[10]) as u64));
304 let x203
: u64 = (((arg1
[12]) as u64) * ((arg2
[9]) as u64));
305 let x204
: u64 = (((arg1
[12]) as u64) * ((arg2
[8]) as u64));
306 let x205
: u64 = (((arg1
[12]) as u64) * ((arg2
[7]) as u64));
307 let x206
: u64 = (((arg1
[12]) as u64) * ((arg2
[6]) as u64));
308 let x207
: u64 = (((arg1
[12]) as u64) * ((arg2
[5]) as u64));
309 let x208
: u64 = (((arg1
[12]) as u64) * ((arg2
[4]) as u64));
310 let x209
: u64 = (((arg1
[11]) as u64) * ((arg2
[12]) as u64));
311 let x210
: u64 = (((arg1
[11]) as u64) * ((arg2
[11]) as u64));
312 let x211
: u64 = (((arg1
[11]) as u64) * ((arg2
[10]) as u64));
313 let x212
: u64 = (((arg1
[11]) as u64) * ((arg2
[9]) as u64));
314 let x213
: u64 = (((arg1
[11]) as u64) * ((arg2
[8]) as u64));
315 let x214
: u64 = (((arg1
[11]) as u64) * ((arg2
[7]) as u64));
316 let x215
: u64 = (((arg1
[11]) as u64) * ((arg2
[6]) as u64));
317 let x216
: u64 = (((arg1
[11]) as u64) * ((arg2
[5]) as u64));
318 let x217
: u64 = (((arg1
[10]) as u64) * ((arg2
[13]) as u64));
319 let x218
: u64 = (((arg1
[10]) as u64) * ((arg2
[12]) as u64));
320 let x219
: u64 = (((arg1
[10]) as u64) * ((arg2
[11]) as u64));
321 let x220
: u64 = (((arg1
[10]) as u64) * ((arg2
[10]) as u64));
322 let x221
: u64 = (((arg1
[10]) as u64) * ((arg2
[9]) as u64));
323 let x222
: u64 = (((arg1
[10]) as u64) * ((arg2
[8]) as u64));
324 let x223
: u64 = (((arg1
[10]) as u64) * ((arg2
[7]) as u64));
325 let x224
: u64 = (((arg1
[10]) as u64) * ((arg2
[6]) as u64));
326 let x225
: u64 = (((arg1
[9]) as u64) * ((arg2
[14]) as u64));
327 let x226
: u64 = (((arg1
[9]) as u64) * ((arg2
[13]) as u64));
328 let x227
: u64 = (((arg1
[9]) as u64) * ((arg2
[12]) as u64));
329 let x228
: u64 = (((arg1
[9]) as u64) * ((arg2
[11]) as u64));
330 let x229
: u64 = (((arg1
[9]) as u64) * ((arg2
[10]) as u64));
331 let x230
: u64 = (((arg1
[9]) as u64) * ((arg2
[9]) as u64));
332 let x231
: u64 = (((arg1
[9]) as u64) * ((arg2
[8]) as u64));
333 let x232
: u64 = (((arg1
[9]) as u64) * ((arg2
[7]) as u64));
334 let x233
: u64 = (((arg1
[8]) as u64) * ((arg2
[15]) as u64));
335 let x234
: u64 = (((arg1
[8]) as u64) * ((arg2
[14]) as u64));
336 let x235
: u64 = (((arg1
[8]) as u64) * ((arg2
[13]) as u64));
337 let x236
: u64 = (((arg1
[8]) as u64) * ((arg2
[12]) as u64));
338 let x237
: u64 = (((arg1
[8]) as u64) * ((arg2
[11]) as u64));
339 let x238
: u64 = (((arg1
[8]) as u64) * ((arg2
[10]) as u64));
340 let x239
: u64 = (((arg1
[8]) as u64) * ((arg2
[9]) as u64));
341 let x240
: u64 = (((arg1
[8]) as u64) * ((arg2
[8]) as u64));
342 let x241
: u64 = (((arg1
[7]) as u64) * ((arg2
[15]) as u64));
343 let x242
: u64 = (((arg1
[7]) as u64) * ((arg2
[14]) as u64));
344 let x243
: u64 = (((arg1
[7]) as u64) * ((arg2
[13]) as u64));
345 let x244
: u64 = (((arg1
[7]) as u64) * ((arg2
[12]) as u64));
346 let x245
: u64 = (((arg1
[7]) as u64) * ((arg2
[11]) as u64));
347 let x246
: u64 = (((arg1
[7]) as u64) * ((arg2
[10]) as u64));
348 let x247
: u64 = (((arg1
[7]) as u64) * ((arg2
[9]) as u64));
349 let x248
: u64 = (((arg1
[6]) as u64) * ((arg2
[15]) as u64));
350 let x249
: u64 = (((arg1
[6]) as u64) * ((arg2
[14]) as u64));
351 let x250
: u64 = (((arg1
[6]) as u64) * ((arg2
[13]) as u64));
352 let x251
: u64 = (((arg1
[6]) as u64) * ((arg2
[12]) as u64));
353 let x252
: u64 = (((arg1
[6]) as u64) * ((arg2
[11]) as u64));
354 let x253
: u64 = (((arg1
[6]) as u64) * ((arg2
[10]) as u64));
355 let x254
: u64 = (((arg1
[5]) as u64) * ((arg2
[15]) as u64));
356 let x255
: u64 = (((arg1
[5]) as u64) * ((arg2
[14]) as u64));
357 let x256
: u64 = (((arg1
[5]) as u64) * ((arg2
[13]) as u64));
358 let x257
: u64 = (((arg1
[5]) as u64) * ((arg2
[12]) as u64));
359 let x258
: u64 = (((arg1
[5]) as u64) * ((arg2
[11]) as u64));
360 let x259
: u64 = (((arg1
[4]) as u64) * ((arg2
[15]) as u64));
361 let x260
: u64 = (((arg1
[4]) as u64) * ((arg2
[14]) as u64));
362 let x261
: u64 = (((arg1
[4]) as u64) * ((arg2
[13]) as u64));
363 let x262
: u64 = (((arg1
[4]) as u64) * ((arg2
[12]) as u64));
364 let x263
: u64 = (((arg1
[3]) as u64) * ((arg2
[15]) as u64));
365 let x264
: u64 = (((arg1
[3]) as u64) * ((arg2
[14]) as u64));
366 let x265
: u64 = (((arg1
[3]) as u64) * ((arg2
[13]) as u64));
367 let x266
: u64 = (((arg1
[2]) as u64) * ((arg2
[15]) as u64));
368 let x267
: u64 = (((arg1
[2]) as u64) * ((arg2
[14]) as u64));
369 let x268
: u64 = (((arg1
[1]) as u64) * ((arg2
[15]) as u64));
370 let x269
: u64 = (((arg1
[15]) as u64) * ((arg2
[0]) as u64));
371 let x270
: u64 = (((arg1
[14]) as u64) * ((arg2
[1]) as u64));
372 let x271
: u64 = (((arg1
[14]) as u64) * ((arg2
[0]) as u64));
373 let x272
: u64 = (((arg1
[13]) as u64) * ((arg2
[2]) as u64));
374 let x273
: u64 = (((arg1
[13]) as u64) * ((arg2
[1]) as u64));
375 let x274
: u64 = (((arg1
[13]) as u64) * ((arg2
[0]) as u64));
376 let x275
: u64 = (((arg1
[12]) as u64) * ((arg2
[3]) as u64));
377 let x276
: u64 = (((arg1
[12]) as u64) * ((arg2
[2]) as u64));
378 let x277
: u64 = (((arg1
[12]) as u64) * ((arg2
[1]) as u64));
379 let x278
: u64 = (((arg1
[12]) as u64) * ((arg2
[0]) as u64));
380 let x279
: u64 = (((arg1
[11]) as u64) * ((arg2
[4]) as u64));
381 let x280
: u64 = (((arg1
[11]) as u64) * ((arg2
[3]) as u64));
382 let x281
: u64 = (((arg1
[11]) as u64) * ((arg2
[2]) as u64));
383 let x282
: u64 = (((arg1
[11]) as u64) * ((arg2
[1]) as u64));
384 let x283
: u64 = (((arg1
[11]) as u64) * ((arg2
[0]) as u64));
385 let x284
: u64 = (((arg1
[10]) as u64) * ((arg2
[5]) as u64));
386 let x285
: u64 = (((arg1
[10]) as u64) * ((arg2
[4]) as u64));
387 let x286
: u64 = (((arg1
[10]) as u64) * ((arg2
[3]) as u64));
388 let x287
: u64 = (((arg1
[10]) as u64) * ((arg2
[2]) as u64));
389 let x288
: u64 = (((arg1
[10]) as u64) * ((arg2
[1]) as u64));
390 let x289
: u64 = (((arg1
[10]) as u64) * ((arg2
[0]) as u64));
391 let x290
: u64 = (((arg1
[9]) as u64) * ((arg2
[6]) as u64));
392 let x291
: u64 = (((arg1
[9]) as u64) * ((arg2
[5]) as u64));
393 let x292
: u64 = (((arg1
[9]) as u64) * ((arg2
[4]) as u64));
394 let x293
: u64 = (((arg1
[9]) as u64) * ((arg2
[3]) as u64));
395 let x294
: u64 = (((arg1
[9]) as u64) * ((arg2
[2]) as u64));
396 let x295
: u64 = (((arg1
[9]) as u64) * ((arg2
[1]) as u64));
397 let x296
: u64 = (((arg1
[9]) as u64) * ((arg2
[0]) as u64));
398 let x297
: u64 = (((arg1
[8]) as u64) * ((arg2
[7]) as u64));
399 let x298
: u64 = (((arg1
[8]) as u64) * ((arg2
[6]) as u64));
400 let x299
: u64 = (((arg1
[8]) as u64) * ((arg2
[5]) as u64));
401 let x300
: u64 = (((arg1
[8]) as u64) * ((arg2
[4]) as u64));
402 let x301
: u64 = (((arg1
[8]) as u64) * ((arg2
[3]) as u64));
403 let x302
: u64 = (((arg1
[8]) as u64) * ((arg2
[2]) as u64));
404 let x303
: u64 = (((arg1
[8]) as u64) * ((arg2
[1]) as u64));
405 let x304
: u64 = (((arg1
[8]) as u64) * ((arg2
[0]) as u64));
406 let x305
: u64 = (((arg1
[7]) as u64) * ((arg2
[8]) as u64));
407 let x306
: u64 = (((arg1
[7]) as u64) * ((arg2
[7]) as u64));
408 let x307
: u64 = (((arg1
[7]) as u64) * ((arg2
[6]) as u64));
409 let x308
: u64 = (((arg1
[7]) as u64) * ((arg2
[5]) as u64));
410 let x309
: u64 = (((arg1
[7]) as u64) * ((arg2
[4]) as u64));
411 let x310
: u64 = (((arg1
[7]) as u64) * ((arg2
[3]) as u64));
412 let x311
: u64 = (((arg1
[7]) as u64) * ((arg2
[2]) as u64));
413 let x312
: u64 = (((arg1
[7]) as u64) * ((arg2
[1]) as u64));
414 let x313
: u64 = (((arg1
[7]) as u64) * ((arg2
[0]) as u64));
415 let x314
: u64 = (((arg1
[6]) as u64) * ((arg2
[9]) as u64));
416 let x315
: u64 = (((arg1
[6]) as u64) * ((arg2
[8]) as u64));
417 let x316
: u64 = (((arg1
[6]) as u64) * ((arg2
[7]) as u64));
418 let x317
: u64 = (((arg1
[6]) as u64) * ((arg2
[6]) as u64));
419 let x318
: u64 = (((arg1
[6]) as u64) * ((arg2
[5]) as u64));
420 let x319
: u64 = (((arg1
[6]) as u64) * ((arg2
[4]) as u64));
421 let x320
: u64 = (((arg1
[6]) as u64) * ((arg2
[3]) as u64));
422 let x321
: u64 = (((arg1
[6]) as u64) * ((arg2
[2]) as u64));
423 let x322
: u64 = (((arg1
[6]) as u64) * ((arg2
[1]) as u64));
424 let x323
: u64 = (((arg1
[6]) as u64) * ((arg2
[0]) as u64));
425 let x324
: u64 = (((arg1
[5]) as u64) * ((arg2
[10]) as u64));
426 let x325
: u64 = (((arg1
[5]) as u64) * ((arg2
[9]) as u64));
427 let x326
: u64 = (((arg1
[5]) as u64) * ((arg2
[8]) as u64));
428 let x327
: u64 = (((arg1
[5]) as u64) * ((arg2
[7]) as u64));
429 let x328
: u64 = (((arg1
[5]) as u64) * ((arg2
[6]) as u64));
430 let x329
: u64 = (((arg1
[5]) as u64) * ((arg2
[5]) as u64));
431 let x330
: u64 = (((arg1
[5]) as u64) * ((arg2
[4]) as u64));
432 let x331
: u64 = (((arg1
[5]) as u64) * ((arg2
[3]) as u64));
433 let x332
: u64 = (((arg1
[5]) as u64) * ((arg2
[2]) as u64));
434 let x333
: u64 = (((arg1
[5]) as u64) * ((arg2
[1]) as u64));
435 let x334
: u64 = (((arg1
[5]) as u64) * ((arg2
[0]) as u64));
436 let x335
: u64 = (((arg1
[4]) as u64) * ((arg2
[11]) as u64));
437 let x336
: u64 = (((arg1
[4]) as u64) * ((arg2
[10]) as u64));
438 let x337
: u64 = (((arg1
[4]) as u64) * ((arg2
[9]) as u64));
439 let x338
: u64 = (((arg1
[4]) as u64) * ((arg2
[8]) as u64));
440 let x339
: u64 = (((arg1
[4]) as u64) * ((arg2
[7]) as u64));
441 let x340
: u64 = (((arg1
[4]) as u64) * ((arg2
[6]) as u64));
442 let x341
: u64 = (((arg1
[4]) as u64) * ((arg2
[5]) as u64));
443 let x342
: u64 = (((arg1
[4]) as u64) * ((arg2
[4]) as u64));
444 let x343
: u64 = (((arg1
[4]) as u64) * ((arg2
[3]) as u64));
445 let x344
: u64 = (((arg1
[4]) as u64) * ((arg2
[2]) as u64));
446 let x345
: u64 = (((arg1
[4]) as u64) * ((arg2
[1]) as u64));
447 let x346
: u64 = (((arg1
[4]) as u64) * ((arg2
[0]) as u64));
448 let x347
: u64 = (((arg1
[3]) as u64) * ((arg2
[12]) as u64));
449 let x348
: u64 = (((arg1
[3]) as u64) * ((arg2
[11]) as u64));
450 let x349
: u64 = (((arg1
[3]) as u64) * ((arg2
[10]) as u64));
451 let x350
: u64 = (((arg1
[3]) as u64) * ((arg2
[9]) as u64));
452 let x351
: u64 = (((arg1
[3]) as u64) * ((arg2
[8]) as u64));
453 let x352
: u64 = (((arg1
[3]) as u64) * ((arg2
[7]) as u64));
454 let x353
: u64 = (((arg1
[3]) as u64) * ((arg2
[6]) as u64));
455 let x354
: u64 = (((arg1
[3]) as u64) * ((arg2
[5]) as u64));
456 let x355
: u64 = (((arg1
[3]) as u64) * ((arg2
[4]) as u64));
457 let x356
: u64 = (((arg1
[3]) as u64) * ((arg2
[3]) as u64));
458 let x357
: u64 = (((arg1
[3]) as u64) * ((arg2
[2]) as u64));
459 let x358
: u64 = (((arg1
[3]) as u64) * ((arg2
[1]) as u64));
460 let x359
: u64 = (((arg1
[3]) as u64) * ((arg2
[0]) as u64));
461 let x360
: u64 = (((arg1
[2]) as u64) * ((arg2
[13]) as u64));
462 let x361
: u64 = (((arg1
[2]) as u64) * ((arg2
[12]) as u64));
463 let x362
: u64 = (((arg1
[2]) as u64) * ((arg2
[11]) as u64));
464 let x363
: u64 = (((arg1
[2]) as u64) * ((arg2
[10]) as u64));
465 let x364
: u64 = (((arg1
[2]) as u64) * ((arg2
[9]) as u64));
466 let x365
: u64 = (((arg1
[2]) as u64) * ((arg2
[8]) as u64));
467 let x366
: u64 = (((arg1
[2]) as u64) * ((arg2
[7]) as u64));
468 let x367
: u64 = (((arg1
[2]) as u64) * ((arg2
[6]) as u64));
469 let x368
: u64 = (((arg1
[2]) as u64) * ((arg2
[5]) as u64));
470 let x369
: u64 = (((arg1
[2]) as u64) * ((arg2
[4]) as u64));
471 let x370
: u64 = (((arg1
[2]) as u64) * ((arg2
[3]) as u64));
472 let x371
: u64 = (((arg1
[2]) as u64) * ((arg2
[2]) as u64));
473 let x372
: u64 = (((arg1
[2]) as u64) * ((arg2
[1]) as u64));
474 let x373
: u64 = (((arg1
[2]) as u64) * ((arg2
[0]) as u64));
475 let x374
: u64 = (((arg1
[1]) as u64) * ((arg2
[14]) as u64));
476 let x375
: u64 = (((arg1
[1]) as u64) * ((arg2
[13]) as u64));
477 let x376
: u64 = (((arg1
[1]) as u64) * ((arg2
[12]) as u64));
478 let x377
: u64 = (((arg1
[1]) as u64) * ((arg2
[11]) as u64));
479 let x378
: u64 = (((arg1
[1]) as u64) * ((arg2
[10]) as u64));
480 let x379
: u64 = (((arg1
[1]) as u64) * ((arg2
[9]) as u64));
481 let x380
: u64 = (((arg1
[1]) as u64) * ((arg2
[8]) as u64));
482 let x381
: u64 = (((arg1
[1]) as u64) * ((arg2
[7]) as u64));
483 let x382
: u64 = (((arg1
[1]) as u64) * ((arg2
[6]) as u64));
484 let x383
: u64 = (((arg1
[1]) as u64) * ((arg2
[5]) as u64));
485 let x384
: u64 = (((arg1
[1]) as u64) * ((arg2
[4]) as u64));
486 let x385
: u64 = (((arg1
[1]) as u64) * ((arg2
[3]) as u64));
487 let x386
: u64 = (((arg1
[1]) as u64) * ((arg2
[2]) as u64));
488 let x387
: u64 = (((arg1
[1]) as u64) * ((arg2
[1]) as u64));
489 let x388
: u64 = (((arg1
[1]) as u64) * ((arg2
[0]) as u64));
490 let x389
: u64 = (((arg1
[0]) as u64) * ((arg2
[15]) as u64));
491 let x390
: u64 = (((arg1
[0]) as u64) * ((arg2
[14]) as u64));
492 let x391
: u64 = (((arg1
[0]) as u64) * ((arg2
[13]) as u64));
493 let x392
: u64 = (((arg1
[0]) as u64) * ((arg2
[12]) as u64));
494 let x393
: u64 = (((arg1
[0]) as u64) * ((arg2
[11]) as u64));
495 let x394
: u64 = (((arg1
[0]) as u64) * ((arg2
[10]) as u64));
496 let x395
: u64 = (((arg1
[0]) as u64) * ((arg2
[9]) as u64));
497 let x396
: u64 = (((arg1
[0]) as u64) * ((arg2
[8]) as u64));
498 let x397
: u64 = (((arg1
[0]) as u64) * ((arg2
[7]) as u64));
499 let x398
: u64 = (((arg1
[0]) as u64) * ((arg2
[6]) as u64));
500 let x399
: u64 = (((arg1
[0]) as u64) * ((arg2
[5]) as u64));
501 let x400
: u64 = (((arg1
[0]) as u64) * ((arg2
[4]) as u64));
502 let x401
: u64 = (((arg1
[0]) as u64) * ((arg2
[3]) as u64));
503 let x402
: u64 = (((arg1
[0]) as u64) * ((arg2
[2]) as u64));
504 let x403
: u64 = (((arg1
[0]) as u64) * ((arg2
[1]) as u64));
505 let x404
: u64 = (((arg1
[0]) as u64) * ((arg2
[0]) as u64));
506 let x405
: u64 = (x397
+ (x382
+ (x368
+ (x355
+ (x343
+ (x332
+ (x322
+ (x313
+ (x141
+ (x133
+ (x124
+ (x114
+ (x103
+ (x91
+ (x78
+ x64
)))))))))))))));
507 let x406
: u64 = (x405
>> 28);
508 let x407
: u32 = ((x405
& (0xfffffff as u64)) as u32);
509 let x408
: u64 = (x389
+ (x374
+ (x360
+ (x347
+ (x335
+ (x324
+ (x314
+ (x305
+ (x297
+ (x290
+ (x284
+ (x279
+ (x275
+ (x272
+ (x270
+ (x269
+ (x233
+ (x225
+ (x217
+ (x209
+ (x201
+ (x193
+ (x185
+ x177
)))))))))))))))))))))));
510 let x409
: u64 = (x390
+ (x375
+ (x361
+ (x348
+ (x336
+ (x325
+ (x315
+ (x306
+ (x298
+ (x291
+ (x285
+ (x280
+ (x276
+ (x273
+ (x271
+ (x241
+ (x234
+ (x226
+ (x218
+ (x210
+ (x202
+ (x194
+ (x186
+ (x178
+ (x57
+ x29
)))))))))))))))))))))))));
511 let x410
: u64 = (x391
+ (x376
+ (x362
+ (x349
+ (x337
+ (x326
+ (x316
+ (x307
+ (x299
+ (x292
+ (x286
+ (x281
+ (x277
+ (x274
+ (x248
+ (x242
+ (x235
+ (x227
+ (x219
+ (x211
+ (x203
+ (x195
+ (x187
+ (x179
+ (x72
+ (x58
+ (x36
+ x30
)))))))))))))))))))))))))));
512 let x411
: u128
= ((x392
as u128
) + ((x377
as u128
) + ((x363
+ (x350
+ (x338
+ (x327
+ (x317
+ (x308
+ (x300
+ (x293
+ (x287
+ (x282
+ (x278
+ (x254
+ (x249
+ (x243
+ (x236
+ (x228
+ (x220
+ (x212
+ (x204
+ (x196
+ (x188
+ (x180
+ (x86
+ (x73
+ (x59
+ (x42
+ (x37
+ x31
))))))))))))))))))))))))))) as u128
)));
513 let x412
: u128
= ((x393
as u128
) + ((x378
as u128
) + ((x364
as u128
) + ((x351
as u128
) + ((x339
+ (x328
+ (x318
+ (x309
+ (x301
+ (x294
+ (x288
+ (x283
+ (x259
+ (x255
+ (x250
+ (x244
+ (x237
+ (x229
+ (x221
+ (x213
+ (x205
+ (x197
+ (x189
+ (x181
+ (x99
+ (x87
+ (x74
+ (x60
+ (x47
+ (x43
+ (x38
+ x32
))))))))))))))))))))))))))) as u128
)))));
514 let x413
: u128
= ((x394
as u128
) + ((x379
as u128
) + ((x365
as u128
) + ((x352
as u128
) + ((x340
as u128
) + ((x329
as u128
) + ((x319
+ (x310
+ (x302
+ (x295
+ (x289
+ (x263
+ (x260
+ (x256
+ (x251
+ (x245
+ (x238
+ (x230
+ (x222
+ (x214
+ (x206
+ (x198
+ (x190
+ (x182
+ (x111
+ (x100
+ (x88
+ (x75
+ (x61
+ (x51
+ (x48
+ (x44
+ (x39
+ x33
))))))))))))))))))))))))))) as u128
)))))));
515 let x414
: u128
= ((x395
as u128
) + ((x380
as u128
) + ((x366
as u128
) + ((x353
as u128
) + ((x341
as u128
) + ((x330
as u128
) + ((x320
as u128
) + ((x311
as u128
) + ((x303
+ (x296
+ (x266
+ (x264
+ (x261
+ (x257
+ (x252
+ (x246
+ (x239
+ (x231
+ (x223
+ (x215
+ (x207
+ (x199
+ (x191
+ (x183
+ (x122
+ (x112
+ (x101
+ (x89
+ (x76
+ (x62
+ (x54
+ (x52
+ (x49
+ (x45
+ (x40
+ x34
))))))))))))))))))))))))))) as u128
)))))))));
516 let x415
: u128
= ((x396
as u128
) + ((x381
as u128
) + ((x367
as u128
) + ((x354
as u128
) + ((x342
as u128
) + ((x331
as u128
) + ((x321
as u128
) + ((x312
as u128
) + ((x304
as u128
) + ((x268
as u128
) + ((x267
+ (x265
+ (x262
+ (x258
+ (x253
+ (x247
+ (x240
+ (x232
+ (x224
+ (x216
+ (x208
+ (x200
+ (x192
+ (x184
+ (x132
+ (x123
+ (x113
+ (x102
+ (x90
+ (x77
+ (x63
+ (x56
+ (x55
+ (x53
+ (x50
+ (x46
+ (x41
+ x35
))))))))))))))))))))))))))) as u128
)))))))))));
517 let x416
: u64 = (x398
+ (x383
+ (x369
+ (x356
+ (x344
+ (x333
+ (x323
+ (x149
+ (x142
+ (x134
+ (x125
+ (x115
+ (x104
+ (x92
+ (x79
+ (x65
+ x1
))))))))))))))));
518 let x417
: u64 = (x399
+ (x384
+ (x370
+ (x357
+ (x345
+ (x334
+ (x156
+ (x150
+ (x143
+ (x135
+ (x126
+ (x116
+ (x105
+ (x93
+ (x80
+ (x66
+ (x8
+ x2
)))))))))))))))));
519 let x418
: u64 = (x400
+ (x385
+ (x371
+ (x358
+ (x346
+ (x162
+ (x157
+ (x151
+ (x144
+ (x136
+ (x127
+ (x117
+ (x106
+ (x94
+ (x81
+ (x67
+ (x14
+ (x9
+ x3
))))))))))))))))));
520 let x419
: u64 = (x401
+ (x386
+ (x372
+ (x359
+ (x167
+ (x163
+ (x158
+ (x152
+ (x145
+ (x137
+ (x128
+ (x118
+ (x107
+ (x95
+ (x82
+ (x68
+ (x19
+ (x15
+ (x10
+ x4
)))))))))))))))))));
521 let x420
: u64 = (x402
+ (x387
+ (x373
+ (x171
+ (x168
+ (x164
+ (x159
+ (x153
+ (x146
+ (x138
+ (x129
+ (x119
+ (x108
+ (x96
+ (x83
+ (x69
+ (x23
+ (x20
+ (x16
+ (x11
+ x5
))))))))))))))))))));
522 let x421
: u64 = (x403
+ (x388
+ (x174
+ (x172
+ (x169
+ (x165
+ (x160
+ (x154
+ (x147
+ (x139
+ (x130
+ (x120
+ (x109
+ (x97
+ (x84
+ (x70
+ (x26
+ (x24
+ (x21
+ (x17
+ (x12
+ x6
)))))))))))))))))))));
523 let x422
: u64 = (x404
+ (x176
+ (x175
+ (x173
+ (x170
+ (x166
+ (x161
+ (x155
+ (x148
+ (x140
+ (x131
+ (x121
+ (x110
+ (x98
+ (x85
+ (x71
+ (x28
+ (x27
+ (x25
+ (x22
+ (x18
+ (x13
+ x7
))))))))))))))))))))));
524 let x423
: u128
= ((x406
as u128
) + x415
);
525 let x424
: u64 = (x408
>> 28);
526 let x425
: u32 = ((x408
& (0xfffffff as u64)) as u32);
527 let x426
: u128
= (x423
+ (x424
as u128
));
528 let x427
: u64 = ((x426
>> 28) as u64);
529 let x428
: u32 = ((x426
& (0xfffffff as u128
)) as u32);
530 let x429
: u64 = (x422
+ x424
);
531 let x430
: u128
= ((x427
as u128
) + x414
);
532 let x431
: u64 = (x429
>> 28);
533 let x432
: u32 = ((x429
& (0xfffffff as u64)) as u32);
534 let x433
: u64 = (x431
+ x421
);
535 let x434
: u64 = ((x430
>> 28) as u64);
536 let x435
: u32 = ((x430
& (0xfffffff as u128
)) as u32);
537 let x436
: u128
= ((x434
as u128
) + x413
);
538 let x437
: u64 = (x433
>> 28);
539 let x438
: u32 = ((x433
& (0xfffffff as u64)) as u32);
540 let x439
: u64 = (x437
+ x420
);
541 let x440
: u64 = ((x436
>> 28) as u64);
542 let x441
: u32 = ((x436
& (0xfffffff as u128
)) as u32);
543 let x442
: u128
= ((x440
as u128
) + x412
);
544 let x443
: u64 = (x439
>> 28);
545 let x444
: u32 = ((x439
& (0xfffffff as u64)) as u32);
546 let x445
: u64 = (x443
+ x419
);
547 let x446
: u64 = ((x442
>> 28) as u64);
548 let x447
: u32 = ((x442
& (0xfffffff as u128
)) as u32);
549 let x448
: u128
= ((x446
as u128
) + x411
);
550 let x449
: u64 = (x445
>> 28);
551 let x450
: u32 = ((x445
& (0xfffffff as u64)) as u32);
552 let x451
: u64 = (x449
+ x418
);
553 let x452
: u64 = ((x448
>> 28) as u64);
554 let x453
: u32 = ((x448
& (0xfffffff as u128
)) as u32);
555 let x454
: u64 = (x452
+ x410
);
556 let x455
: u64 = (x451
>> 28);
557 let x456
: u32 = ((x451
& (0xfffffff as u64)) as u32);
558 let x457
: u64 = (x455
+ x417
);
559 let x458
: u64 = (x454
>> 28);
560 let x459
: u32 = ((x454
& (0xfffffff as u64)) as u32);
561 let x460
: u64 = (x458
+ x409
);
562 let x461
: u64 = (x457
>> 28);
563 let x462
: u32 = ((x457
& (0xfffffff as u64)) as u32);
564 let x463
: u64 = (x461
+ x416
);
565 let x464
: u64 = (x460
>> 28);
566 let x465
: u32 = ((x460
& (0xfffffff as u64)) as u32);
567 let x466
: u64 = (x464
+ (x425
as u64));
568 let x467
: u64 = (x463
>> 28);
569 let x468
: u32 = ((x463
& (0xfffffff as u64)) as u32);
570 let x469
: u64 = (x467
+ (x407
as u64));
571 let x470
: u32 = ((x466
>> 28) as u32);
572 let x471
: u32 = ((x466
& (0xfffffff as u64)) as u32);
573 let x472
: u32 = ((x469
>> 28) as u32);
574 let x473
: u32 = ((x469
& (0xfffffff as u64)) as u32);
575 let x474
: u32 = (x428
+ x470
);
576 let x475
: u32 = (x432
+ x470
);
577 let x476
: u32 = (x472
+ x474
);
578 let x477
: fiat_p448_u1
= ((x476
>> 28) as fiat_p448_u1
);
579 let x478
: u32 = (x476
& 0xfffffff);
580 let x479
: u32 = ((x477
as u32) + x435
);
581 let x480
: fiat_p448_u1
= ((x475
>> 28) as fiat_p448_u1
);
582 let x481
: u32 = (x475
& 0xfffffff);
583 let x482
: u32 = ((x480
as u32) + x438
);
602 /// The function fiat_p448_carry_square squares a field element and reduces the result.
605 /// eval out1 mod m = (eval arg1 * eval arg1) mod m
608 pub fn fiat_p448_carry_square(out1
: &mut fiat_p448_tight_field_element
, arg1
: &fiat_p448_loose_field_element
) -> () {
609 let x1
: u32 = (arg1
[15]);
610 let x2
: u32 = (arg1
[15]);
611 let x3
: u32 = (x1
* 0x2);
612 let x4
: u32 = (x2
* 0x2);
613 let x5
: u32 = ((arg1
[15]) * 0x2);
614 let x6
: u32 = (arg1
[14]);
615 let x7
: u32 = (arg1
[14]);
616 let x8
: u32 = (x6
* 0x2);
617 let x9
: u32 = (x7
* 0x2);
618 let x10
: u32 = ((arg1
[14]) * 0x2);
619 let x11
: u32 = (arg1
[13]);
620 let x12
: u32 = (arg1
[13]);
621 let x13
: u32 = (x11
* 0x2);
622 let x14
: u32 = (x12
* 0x2);
623 let x15
: u32 = ((arg1
[13]) * 0x2);
624 let x16
: u32 = (arg1
[12]);
625 let x17
: u32 = (arg1
[12]);
626 let x18
: u32 = (x16
* 0x2);
627 let x19
: u32 = (x17
* 0x2);
628 let x20
: u32 = ((arg1
[12]) * 0x2);
629 let x21
: u32 = (arg1
[11]);
630 let x22
: u32 = (arg1
[11]);
631 let x23
: u32 = (x21
* 0x2);
632 let x24
: u32 = (x22
* 0x2);
633 let x25
: u32 = ((arg1
[11]) * 0x2);
634 let x26
: u32 = (arg1
[10]);
635 let x27
: u32 = (arg1
[10]);
636 let x28
: u32 = (x26
* 0x2);
637 let x29
: u32 = (x27
* 0x2);
638 let x30
: u32 = ((arg1
[10]) * 0x2);
639 let x31
: u32 = (arg1
[9]);
640 let x32
: u32 = (arg1
[9]);
641 let x33
: u32 = (x31
* 0x2);
642 let x34
: u32 = (x32
* 0x2);
643 let x35
: u32 = ((arg1
[9]) * 0x2);
644 let x36
: u32 = (arg1
[8]);
645 let x37
: u32 = (arg1
[8]);
646 let x38
: u32 = ((arg1
[8]) * 0x2);
647 let x39
: u32 = ((arg1
[7]) * 0x2);
648 let x40
: u32 = ((arg1
[6]) * 0x2);
649 let x41
: u32 = ((arg1
[5]) * 0x2);
650 let x42
: u32 = ((arg1
[4]) * 0x2);
651 let x43
: u32 = ((arg1
[3]) * 0x2);
652 let x44
: u32 = ((arg1
[2]) * 0x2);
653 let x45
: u32 = ((arg1
[1]) * 0x2);
654 let x46
: u64 = (((arg1
[15]) as u64) * (x1
as u64));
655 let x47
: u64 = (((arg1
[14]) as u64) * (x3
as u64));
656 let x48
: u64 = (((arg1
[14]) as u64) * (x6
as u64));
657 let x49
: u64 = (((arg1
[13]) as u64) * (x3
as u64));
658 let x50
: u64 = (((arg1
[13]) as u64) * (x8
as u64));
659 let x51
: u64 = (((arg1
[13]) as u64) * (x11
as u64));
660 let x52
: u64 = (((arg1
[12]) as u64) * (x3
as u64));
661 let x53
: u64 = (((arg1
[12]) as u64) * (x8
as u64));
662 let x54
: u64 = (((arg1
[12]) as u64) * (x13
as u64));
663 let x55
: u64 = (((arg1
[12]) as u64) * (x16
as u64));
664 let x56
: u64 = (((arg1
[11]) as u64) * (x3
as u64));
665 let x57
: u64 = (((arg1
[11]) as u64) * (x8
as u64));
666 let x58
: u64 = (((arg1
[11]) as u64) * (x13
as u64));
667 let x59
: u64 = (((arg1
[10]) as u64) * (x3
as u64));
668 let x60
: u64 = (((arg1
[10]) as u64) * (x8
as u64));
669 let x61
: u64 = (((arg1
[9]) as u64) * (x3
as u64));
670 let x62
: u64 = (((arg1
[15]) as u64) * (x1
as u64));
671 let x63
: u64 = (((arg1
[14]) as u64) * (x3
as u64));
672 let x64
: u64 = (((arg1
[14]) as u64) * (x6
as u64));
673 let x65
: u64 = (((arg1
[13]) as u64) * (x3
as u64));
674 let x66
: u64 = (((arg1
[13]) as u64) * (x8
as u64));
675 let x67
: u64 = (((arg1
[13]) as u64) * (x11
as u64));
676 let x68
: u64 = (((arg1
[12]) as u64) * (x3
as u64));
677 let x69
: u64 = (((arg1
[12]) as u64) * (x8
as u64));
678 let x70
: u64 = (((arg1
[12]) as u64) * (x13
as u64));
679 let x71
: u64 = (((arg1
[12]) as u64) * (x16
as u64));
680 let x72
: u64 = (((arg1
[11]) as u64) * (x3
as u64));
681 let x73
: u64 = (((arg1
[11]) as u64) * (x8
as u64));
682 let x74
: u64 = (((arg1
[11]) as u64) * (x13
as u64));
683 let x75
: u64 = (((arg1
[10]) as u64) * (x3
as u64));
684 let x76
: u64 = (((arg1
[10]) as u64) * (x8
as u64));
685 let x77
: u64 = (((arg1
[9]) as u64) * (x3
as u64));
686 let x78
: u64 = (((arg1
[15]) as u64) * (x2
as u64));
687 let x79
: u64 = (((arg1
[14]) as u64) * (x4
as u64));
688 let x80
: u64 = (((arg1
[14]) as u64) * (x7
as u64));
689 let x81
: u64 = (((arg1
[13]) as u64) * (x4
as u64));
690 let x82
: u64 = (((arg1
[13]) as u64) * (x9
as u64));
691 let x83
: u64 = (((arg1
[13]) as u64) * (x12
as u64));
692 let x84
: u64 = (((arg1
[12]) as u64) * (x4
as u64));
693 let x85
: u64 = (((arg1
[12]) as u64) * (x9
as u64));
694 let x86
: u64 = (((arg1
[12]) as u64) * (x14
as u64));
695 let x87
: u64 = (((arg1
[12]) as u64) * (x17
as u64));
696 let x88
: u64 = (((arg1
[11]) as u64) * (x4
as u64));
697 let x89
: u64 = (((arg1
[11]) as u64) * (x9
as u64));
698 let x90
: u64 = (((arg1
[11]) as u64) * (x14
as u64));
699 let x91
: u64 = (((arg1
[11]) as u64) * (x19
as u64));
700 let x92
: u64 = (((arg1
[11]) as u64) * (x18
as u64));
701 let x93
: u64 = (((arg1
[11]) as u64) * (x22
as u64));
702 let x94
: u64 = (((arg1
[11]) as u64) * (x21
as u64));
703 let x95
: u64 = (((arg1
[10]) as u64) * (x4
as u64));
704 let x96
: u64 = (((arg1
[10]) as u64) * (x9
as u64));
705 let x97
: u64 = (((arg1
[10]) as u64) * (x14
as u64));
706 let x98
: u64 = (((arg1
[10]) as u64) * (x13
as u64));
707 let x99
: u64 = (((arg1
[10]) as u64) * (x19
as u64));
708 let x100
: u64 = (((arg1
[10]) as u64) * (x18
as u64));
709 let x101
: u64 = (((arg1
[10]) as u64) * (x24
as u64));
710 let x102
: u64 = (((arg1
[10]) as u64) * (x23
as u64));
711 let x103
: u64 = (((arg1
[10]) as u64) * (x27
as u64));
712 let x104
: u64 = (((arg1
[10]) as u64) * (x26
as u64));
713 let x105
: u64 = (((arg1
[9]) as u64) * (x4
as u64));
714 let x106
: u64 = (((arg1
[9]) as u64) * (x9
as u64));
715 let x107
: u64 = (((arg1
[9]) as u64) * (x8
as u64));
716 let x108
: u64 = (((arg1
[9]) as u64) * (x14
as u64));
717 let x109
: u64 = (((arg1
[9]) as u64) * (x13
as u64));
718 let x110
: u64 = (((arg1
[9]) as u64) * (x19
as u64));
719 let x111
: u64 = (((arg1
[9]) as u64) * (x18
as u64));
720 let x112
: u64 = (((arg1
[9]) as u64) * (x24
as u64));
721 let x113
: u64 = (((arg1
[9]) as u64) * (x23
as u64));
722 let x114
: u64 = (((arg1
[9]) as u64) * (x29
as u64));
723 let x115
: u64 = (((arg1
[9]) as u64) * (x28
as u64));
724 let x116
: u64 = (((arg1
[9]) as u64) * (x32
as u64));
725 let x117
: u64 = (((arg1
[9]) as u64) * (x31
as u64));
726 let x118
: u64 = (((arg1
[8]) as u64) * (x4
as u64));
727 let x119
: u64 = (((arg1
[8]) as u64) * (x3
as u64));
728 let x120
: u64 = (((arg1
[8]) as u64) * (x9
as u64));
729 let x121
: u64 = (((arg1
[8]) as u64) * (x8
as u64));
730 let x122
: u64 = (((arg1
[8]) as u64) * (x14
as u64));
731 let x123
: u64 = (((arg1
[8]) as u64) * (x13
as u64));
732 let x124
: u64 = (((arg1
[8]) as u64) * (x19
as u64));
733 let x125
: u64 = (((arg1
[8]) as u64) * (x18
as u64));
734 let x126
: u64 = (((arg1
[8]) as u64) * (x24
as u64));
735 let x127
: u64 = (((arg1
[8]) as u64) * (x23
as u64));
736 let x128
: u64 = (((arg1
[8]) as u64) * (x29
as u64));
737 let x129
: u64 = (((arg1
[8]) as u64) * (x28
as u64));
738 let x130
: u64 = (((arg1
[8]) as u64) * (x34
as u64));
739 let x131
: u64 = (((arg1
[8]) as u64) * (x33
as u64));
740 let x132
: u64 = (((arg1
[8]) as u64) * (x37
as u64));
741 let x133
: u64 = (((arg1
[8]) as u64) * (x36
as u64));
742 let x134
: u64 = (((arg1
[7]) as u64) * (x4
as u64));
743 let x135
: u64 = (((arg1
[7]) as u64) * (x3
as u64));
744 let x136
: u64 = (((arg1
[7]) as u64) * (x9
as u64));
745 let x137
: u64 = (((arg1
[7]) as u64) * (x8
as u64));
746 let x138
: u64 = (((arg1
[7]) as u64) * (x14
as u64));
747 let x139
: u64 = (((arg1
[7]) as u64) * (x13
as u64));
748 let x140
: u64 = (((arg1
[7]) as u64) * (x19
as u64));
749 let x141
: u64 = (((arg1
[7]) as u64) * (x18
as u64));
750 let x142
: u64 = (((arg1
[7]) as u64) * (x24
as u64));
751 let x143
: u64 = (((arg1
[7]) as u64) * (x23
as u64));
752 let x144
: u64 = (((arg1
[7]) as u64) * (x29
as u64));
753 let x145
: u64 = (((arg1
[7]) as u64) * (x28
as u64));
754 let x146
: u64 = (((arg1
[7]) as u64) * (x34
as u64));
755 let x147
: u64 = (((arg1
[7]) as u64) * (x33
as u64));
756 let x148
: u64 = (((arg1
[7]) as u64) * (x38
as u64));
757 let x149
: u64 = (((arg1
[7]) as u64) * ((arg1
[7]) as u64));
758 let x150
: u64 = (((arg1
[6]) as u64) * (x4
as u64));
759 let x151
: u64 = (((arg1
[6]) as u64) * (x3
as u64));
760 let x152
: u64 = (((arg1
[6]) as u64) * (x9
as u64));
761 let x153
: u64 = (((arg1
[6]) as u64) * (x8
as u64));
762 let x154
: u64 = (((arg1
[6]) as u64) * (x14
as u64));
763 let x155
: u64 = (((arg1
[6]) as u64) * (x13
as u64));
764 let x156
: u64 = (((arg1
[6]) as u64) * (x19
as u64));
765 let x157
: u64 = (((arg1
[6]) as u64) * (x18
as u64));
766 let x158
: u64 = (((arg1
[6]) as u64) * (x24
as u64));
767 let x159
: u64 = (((arg1
[6]) as u64) * (x23
as u64));
768 let x160
: u64 = (((arg1
[6]) as u64) * (x29
as u64));
769 let x161
: u64 = (((arg1
[6]) as u64) * (x28
as u64));
770 let x162
: u64 = (((arg1
[6]) as u64) * (x35
as u64));
771 let x163
: u64 = (((arg1
[6]) as u64) * (x38
as u64));
772 let x164
: u64 = (((arg1
[6]) as u64) * (x39
as u64));
773 let x165
: u64 = (((arg1
[6]) as u64) * ((arg1
[6]) as u64));
774 let x166
: u64 = (((arg1
[5]) as u64) * (x4
as u64));
775 let x167
: u64 = (((arg1
[5]) as u64) * (x3
as u64));
776 let x168
: u64 = (((arg1
[5]) as u64) * (x9
as u64));
777 let x169
: u64 = (((arg1
[5]) as u64) * (x8
as u64));
778 let x170
: u64 = (((arg1
[5]) as u64) * (x14
as u64));
779 let x171
: u64 = (((arg1
[5]) as u64) * (x13
as u64));
780 let x172
: u64 = (((arg1
[5]) as u64) * (x19
as u64));
781 let x173
: u64 = (((arg1
[5]) as u64) * (x18
as u64));
782 let x174
: u64 = (((arg1
[5]) as u64) * (x24
as u64));
783 let x175
: u64 = (((arg1
[5]) as u64) * (x23
as u64));
784 let x176
: u64 = (((arg1
[5]) as u64) * (x30
as u64));
785 let x177
: u64 = (((arg1
[5]) as u64) * (x35
as u64));
786 let x178
: u64 = (((arg1
[5]) as u64) * (x38
as u64));
787 let x179
: u64 = (((arg1
[5]) as u64) * (x39
as u64));
788 let x180
: u64 = (((arg1
[5]) as u64) * (x40
as u64));
789 let x181
: u64 = (((arg1
[5]) as u64) * ((arg1
[5]) as u64));
790 let x182
: u64 = (((arg1
[4]) as u64) * (x4
as u64));
791 let x183
: u64 = (((arg1
[4]) as u64) * (x3
as u64));
792 let x184
: u64 = (((arg1
[4]) as u64) * (x9
as u64));
793 let x185
: u64 = (((arg1
[4]) as u64) * (x8
as u64));
794 let x186
: u64 = (((arg1
[4]) as u64) * (x14
as u64));
795 let x187
: u64 = (((arg1
[4]) as u64) * (x13
as u64));
796 let x188
: u64 = (((arg1
[4]) as u64) * (x19
as u64));
797 let x189
: u64 = (((arg1
[4]) as u64) * (x18
as u64));
798 let x190
: u64 = (((arg1
[4]) as u64) * (x25
as u64));
799 let x191
: u64 = (((arg1
[4]) as u64) * (x30
as u64));
800 let x192
: u64 = (((arg1
[4]) as u64) * (x35
as u64));
801 let x193
: u64 = (((arg1
[4]) as u64) * (x38
as u64));
802 let x194
: u64 = (((arg1
[4]) as u64) * (x39
as u64));
803 let x195
: u64 = (((arg1
[4]) as u64) * (x40
as u64));
804 let x196
: u64 = (((arg1
[4]) as u64) * (x41
as u64));
805 let x197
: u64 = (((arg1
[4]) as u64) * ((arg1
[4]) as u64));
806 let x198
: u64 = (((arg1
[3]) as u64) * (x4
as u64));
807 let x199
: u64 = (((arg1
[3]) as u64) * (x3
as u64));
808 let x200
: u64 = (((arg1
[3]) as u64) * (x9
as u64));
809 let x201
: u64 = (((arg1
[3]) as u64) * (x8
as u64));
810 let x202
: u64 = (((arg1
[3]) as u64) * (x14
as u64));
811 let x203
: u64 = (((arg1
[3]) as u64) * (x13
as u64));
812 let x204
: u64 = (((arg1
[3]) as u64) * (x20
as u64));
813 let x205
: u64 = (((arg1
[3]) as u64) * (x25
as u64));
814 let x206
: u64 = (((arg1
[3]) as u64) * (x30
as u64));
815 let x207
: u64 = (((arg1
[3]) as u64) * (x35
as u64));
816 let x208
: u64 = (((arg1
[3]) as u64) * (x38
as u64));
817 let x209
: u64 = (((arg1
[3]) as u64) * (x39
as u64));
818 let x210
: u64 = (((arg1
[3]) as u64) * (x40
as u64));
819 let x211
: u64 = (((arg1
[3]) as u64) * (x41
as u64));
820 let x212
: u64 = (((arg1
[3]) as u64) * (x42
as u64));
821 let x213
: u64 = (((arg1
[3]) as u64) * ((arg1
[3]) as u64));
822 let x214
: u64 = (((arg1
[2]) as u64) * (x4
as u64));
823 let x215
: u64 = (((arg1
[2]) as u64) * (x3
as u64));
824 let x216
: u64 = (((arg1
[2]) as u64) * (x9
as u64));
825 let x217
: u64 = (((arg1
[2]) as u64) * (x8
as u64));
826 let x218
: u64 = (((arg1
[2]) as u64) * (x15
as u64));
827 let x219
: u64 = (((arg1
[2]) as u64) * (x20
as u64));
828 let x220
: u64 = (((arg1
[2]) as u64) * (x25
as u64));
829 let x221
: u64 = (((arg1
[2]) as u64) * (x30
as u64));
830 let x222
: u64 = (((arg1
[2]) as u64) * (x35
as u64));
831 let x223
: u64 = (((arg1
[2]) as u64) * (x38
as u64));
832 let x224
: u64 = (((arg1
[2]) as u64) * (x39
as u64));
833 let x225
: u64 = (((arg1
[2]) as u64) * (x40
as u64));
834 let x226
: u64 = (((arg1
[2]) as u64) * (x41
as u64));
835 let x227
: u64 = (((arg1
[2]) as u64) * (x42
as u64));
836 let x228
: u64 = (((arg1
[2]) as u64) * (x43
as u64));
837 let x229
: u64 = (((arg1
[2]) as u64) * ((arg1
[2]) as u64));
838 let x230
: u64 = (((arg1
[1]) as u64) * (x4
as u64));
839 let x231
: u64 = (((arg1
[1]) as u64) * (x3
as u64));
840 let x232
: u64 = (((arg1
[1]) as u64) * (x10
as u64));
841 let x233
: u64 = (((arg1
[1]) as u64) * (x15
as u64));
842 let x234
: u64 = (((arg1
[1]) as u64) * (x20
as u64));
843 let x235
: u64 = (((arg1
[1]) as u64) * (x25
as u64));
844 let x236
: u64 = (((arg1
[1]) as u64) * (x30
as u64));
845 let x237
: u64 = (((arg1
[1]) as u64) * (x35
as u64));
846 let x238
: u64 = (((arg1
[1]) as u64) * (x38
as u64));
847 let x239
: u64 = (((arg1
[1]) as u64) * (x39
as u64));
848 let x240
: u64 = (((arg1
[1]) as u64) * (x40
as u64));
849 let x241
: u64 = (((arg1
[1]) as u64) * (x41
as u64));
850 let x242
: u64 = (((arg1
[1]) as u64) * (x42
as u64));
851 let x243
: u64 = (((arg1
[1]) as u64) * (x43
as u64));
852 let x244
: u64 = (((arg1
[1]) as u64) * (x44
as u64));
853 let x245
: u64 = (((arg1
[1]) as u64) * ((arg1
[1]) as u64));
854 let x246
: u64 = (((arg1
[0]) as u64) * (x5
as u64));
855 let x247
: u64 = (((arg1
[0]) as u64) * (x10
as u64));
856 let x248
: u64 = (((arg1
[0]) as u64) * (x15
as u64));
857 let x249
: u64 = (((arg1
[0]) as u64) * (x20
as u64));
858 let x250
: u64 = (((arg1
[0]) as u64) * (x25
as u64));
859 let x251
: u64 = (((arg1
[0]) as u64) * (x30
as u64));
860 let x252
: u64 = (((arg1
[0]) as u64) * (x35
as u64));
861 let x253
: u64 = (((arg1
[0]) as u64) * (x38
as u64));
862 let x254
: u64 = (((arg1
[0]) as u64) * (x39
as u64));
863 let x255
: u64 = (((arg1
[0]) as u64) * (x40
as u64));
864 let x256
: u64 = (((arg1
[0]) as u64) * (x41
as u64));
865 let x257
: u64 = (((arg1
[0]) as u64) * (x42
as u64));
866 let x258
: u64 = (((arg1
[0]) as u64) * (x43
as u64));
867 let x259
: u64 = (((arg1
[0]) as u64) * (x44
as u64));
868 let x260
: u64 = (((arg1
[0]) as u64) * (x45
as u64));
869 let x261
: u64 = (((arg1
[0]) as u64) * ((arg1
[0]) as u64));
870 let x262
: u64 = (x254
+ (x240
+ (x226
+ (x212
+ (x118
+ (x106
+ (x97
+ x91
)))))));
871 let x263
: u64 = (x262
>> 28);
872 let x264
: u32 = ((x262
& (0xfffffff as u64)) as u32);
873 let x265
: u64 = (x246
+ (x232
+ (x218
+ (x204
+ (x190
+ (x176
+ (x162
+ (x148
+ (x119
+ (x107
+ (x98
+ x92
)))))))))));
874 let x266
: u64 = (x247
+ (x233
+ (x219
+ (x205
+ (x191
+ (x177
+ (x163
+ (x149
+ (x135
+ (x121
+ (x109
+ (x100
+ (x94
+ (x78
+ x62
))))))))))))));
875 let x267
: u64 = (x248
+ (x234
+ (x220
+ (x206
+ (x192
+ (x178
+ (x164
+ (x151
+ (x137
+ (x123
+ (x111
+ (x102
+ (x79
+ x63
)))))))))))));
876 let x268
: u128
= ((x249
as u128
) + ((x235
+ (x221
+ (x207
+ (x193
+ (x179
+ (x167
+ (x165
+ (x153
+ (x139
+ (x125
+ (x113
+ (x104
+ (x81
+ (x80
+ (x65
+ x64
))))))))))))))) as u128
));
877 let x269
: u128
= ((x250
as u128
) + ((x236
as u128
) + ((x222
+ (x208
+ (x194
+ (x183
+ (x180
+ (x169
+ (x155
+ (x141
+ (x127
+ (x115
+ (x84
+ (x82
+ (x68
+ x66
))))))))))))) as u128
)));
878 let x270
: u128
= ((x251
as u128
) + ((x237
as u128
) + ((x223
as u128
) + ((x209
+ (x199
+ (x195
+ (x185
+ (x181
+ (x171
+ (x157
+ (x143
+ (x129
+ (x117
+ (x88
+ (x85
+ (x83
+ (x72
+ (x69
+ x67
))))))))))))))) as u128
))));
879 let x271
: u128
= ((x252
as u128
) + ((x238
as u128
) + ((x224
as u128
) + ((x215
as u128
) + ((x210
+ (x201
+ (x196
+ (x187
+ (x173
+ (x159
+ (x145
+ (x131
+ (x95
+ (x89
+ (x86
+ (x75
+ (x73
+ x70
))))))))))))) as u128
)))));
880 let x272
: u128
= ((x253
as u128
) + ((x239
as u128
) + ((x231
as u128
) + ((x225
as u128
) + ((x217
as u128
) + ((x211
+ (x203
+ (x197
+ (x189
+ (x175
+ (x161
+ (x147
+ (x133
+ (x105
+ (x96
+ (x90
+ (x87
+ (x77
+ (x76
+ (x74
+ x71
))))))))))))))) as u128
))))));
881 let x273
: u64 = (x255
+ (x241
+ (x227
+ (x213
+ (x134
+ (x120
+ (x108
+ (x99
+ (x93
+ x46
)))))))));
882 let x274
: u64 = (x256
+ (x242
+ (x228
+ (x150
+ (x136
+ (x122
+ (x110
+ (x101
+ x47
))))))));
883 let x275
: u64 = (x257
+ (x243
+ (x229
+ (x166
+ (x152
+ (x138
+ (x124
+ (x112
+ (x103
+ (x49
+ x48
))))))))));
884 let x276
: u64 = (x258
+ (x244
+ (x182
+ (x168
+ (x154
+ (x140
+ (x126
+ (x114
+ (x52
+ x50
)))))))));
885 let x277
: u64 = (x259
+ (x245
+ (x198
+ (x184
+ (x170
+ (x156
+ (x142
+ (x128
+ (x116
+ (x56
+ (x53
+ x51
)))))))))));
886 let x278
: u64 = (x260
+ (x214
+ (x200
+ (x186
+ (x172
+ (x158
+ (x144
+ (x130
+ (x59
+ (x57
+ x54
))))))))));
887 let x279
: u64 = (x261
+ (x230
+ (x216
+ (x202
+ (x188
+ (x174
+ (x160
+ (x146
+ (x132
+ (x61
+ (x60
+ (x58
+ x55
))))))))))));
888 let x280
: u128
= ((x263
as u128
) + x272
);
889 let x281
: u64 = (x265
>> 28);
890 let x282
: u32 = ((x265
& (0xfffffff as u64)) as u32);
891 let x283
: u128
= (x280
+ (x281
as u128
));
892 let x284
: u64 = ((x283
>> 28) as u64);
893 let x285
: u32 = ((x283
& (0xfffffff as u128
)) as u32);
894 let x286
: u64 = (x279
+ x281
);
895 let x287
: u128
= ((x284
as u128
) + x271
);
896 let x288
: u64 = (x286
>> 28);
897 let x289
: u32 = ((x286
& (0xfffffff as u64)) as u32);
898 let x290
: u64 = (x288
+ x278
);
899 let x291
: u64 = ((x287
>> 28) as u64);
900 let x292
: u32 = ((x287
& (0xfffffff as u128
)) as u32);
901 let x293
: u128
= ((x291
as u128
) + x270
);
902 let x294
: u64 = (x290
>> 28);
903 let x295
: u32 = ((x290
& (0xfffffff as u64)) as u32);
904 let x296
: u64 = (x294
+ x277
);
905 let x297
: u64 = ((x293
>> 28) as u64);
906 let x298
: u32 = ((x293
& (0xfffffff as u128
)) as u32);
907 let x299
: u128
= ((x297
as u128
) + x269
);
908 let x300
: u64 = (x296
>> 28);
909 let x301
: u32 = ((x296
& (0xfffffff as u64)) as u32);
910 let x302
: u64 = (x300
+ x276
);
911 let x303
: u64 = ((x299
>> 28) as u64);
912 let x304
: u32 = ((x299
& (0xfffffff as u128
)) as u32);
913 let x305
: u128
= ((x303
as u128
) + x268
);
914 let x306
: u64 = (x302
>> 28);
915 let x307
: u32 = ((x302
& (0xfffffff as u64)) as u32);
916 let x308
: u64 = (x306
+ x275
);
917 let x309
: u64 = ((x305
>> 28) as u64);
918 let x310
: u32 = ((x305
& (0xfffffff as u128
)) as u32);
919 let x311
: u64 = (x309
+ x267
);
920 let x312
: u64 = (x308
>> 28);
921 let x313
: u32 = ((x308
& (0xfffffff as u64)) as u32);
922 let x314
: u64 = (x312
+ x274
);
923 let x315
: u64 = (x311
>> 28);
924 let x316
: u32 = ((x311
& (0xfffffff as u64)) as u32);
925 let x317
: u64 = (x315
+ x266
);
926 let x318
: u64 = (x314
>> 28);
927 let x319
: u32 = ((x314
& (0xfffffff as u64)) as u32);
928 let x320
: u64 = (x318
+ x273
);
929 let x321
: u64 = (x317
>> 28);
930 let x322
: u32 = ((x317
& (0xfffffff as u64)) as u32);
931 let x323
: u64 = (x321
+ (x282
as u64));
932 let x324
: u64 = (x320
>> 28);
933 let x325
: u32 = ((x320
& (0xfffffff as u64)) as u32);
934 let x326
: u64 = (x324
+ (x264
as u64));
935 let x327
: u32 = ((x323
>> 28) as u32);
936 let x328
: u32 = ((x323
& (0xfffffff as u64)) as u32);
937 let x329
: u32 = ((x326
>> 28) as u32);
938 let x330
: u32 = ((x326
& (0xfffffff as u64)) as u32);
939 let x331
: u32 = (x285
+ x327
);
940 let x332
: u32 = (x289
+ x327
);
941 let x333
: u32 = (x329
+ x331
);
942 let x334
: fiat_p448_u1
= ((x333
>> 28) as fiat_p448_u1
);
943 let x335
: u32 = (x333
& 0xfffffff);
944 let x336
: u32 = ((x334
as u32) + x292
);
945 let x337
: fiat_p448_u1
= ((x332
>> 28) as fiat_p448_u1
);
946 let x338
: u32 = (x332
& 0xfffffff);
947 let x339
: u32 = ((x337
as u32) + x295
);
966 /// The function fiat_p448_carry reduces a field element.
969 /// eval out1 mod m = eval arg1 mod m
972 pub fn fiat_p448_carry(out1
: &mut fiat_p448_tight_field_element
, arg1
: &fiat_p448_loose_field_element
) -> () {
973 let x1
: u32 = (arg1
[7]);
974 let x2
: u32 = (arg1
[15]);
975 let x3
: u32 = (x2
>> 28);
976 let x4
: u32 = (((x1
>> 28) + (arg1
[8])) + x3
);
977 let x5
: u32 = ((arg1
[0]) + x3
);
978 let x6
: u32 = ((x4
>> 28) + (arg1
[9]));
979 let x7
: u32 = ((x5
>> 28) + (arg1
[1]));
980 let x8
: u32 = ((x6
>> 28) + (arg1
[10]));
981 let x9
: u32 = ((x7
>> 28) + (arg1
[2]));
982 let x10
: u32 = ((x8
>> 28) + (arg1
[11]));
983 let x11
: u32 = ((x9
>> 28) + (arg1
[3]));
984 let x12
: u32 = ((x10
>> 28) + (arg1
[12]));
985 let x13
: u32 = ((x11
>> 28) + (arg1
[4]));
986 let x14
: u32 = ((x12
>> 28) + (arg1
[13]));
987 let x15
: u32 = ((x13
>> 28) + (arg1
[5]));
988 let x16
: u32 = ((x14
>> 28) + (arg1
[14]));
989 let x17
: u32 = ((x15
>> 28) + (arg1
[6]));
990 let x18
: u32 = ((x16
>> 28) + (x2
& 0xfffffff));
991 let x19
: u32 = ((x17
>> 28) + (x1
& 0xfffffff));
992 let x20
: fiat_p448_u1
= ((x18
>> 28) as fiat_p448_u1
);
993 let x21
: u32 = ((x5
& 0xfffffff) + (x20
as u32));
994 let x22
: u32 = ((((x19
>> 28) as fiat_p448_u1
) as u32) + ((x4
& 0xfffffff) + (x20
as u32)));
995 let x23
: u32 = (x21
& 0xfffffff);
996 let x24
: u32 = ((((x21
>> 28) as fiat_p448_u1
) as u32) + (x7
& 0xfffffff));
997 let x25
: u32 = (x9
& 0xfffffff);
998 let x26
: u32 = (x11
& 0xfffffff);
999 let x27
: u32 = (x13
& 0xfffffff);
1000 let x28
: u32 = (x15
& 0xfffffff);
1001 let x29
: u32 = (x17
& 0xfffffff);
1002 let x30
: u32 = (x19
& 0xfffffff);
1003 let x31
: u32 = (x22
& 0xfffffff);
1004 let x32
: u32 = ((((x22
>> 28) as fiat_p448_u1
) as u32) + (x6
& 0xfffffff));
1005 let x33
: u32 = (x8
& 0xfffffff);
1006 let x34
: u32 = (x10
& 0xfffffff);
1007 let x35
: u32 = (x12
& 0xfffffff);
1008 let x36
: u32 = (x14
& 0xfffffff);
1009 let x37
: u32 = (x16
& 0xfffffff);
1010 let x38
: u32 = (x18
& 0xfffffff);
1029 /// The function fiat_p448_add adds two field elements.
1032 /// eval out1 mod m = (eval arg1 + eval arg2) mod m
1035 pub fn fiat_p448_add(out1
: &mut fiat_p448_loose_field_element
, arg1
: &fiat_p448_tight_field_element
, arg2
: &fiat_p448_tight_field_element
) -> () {
1036 let x1
: u32 = ((arg1
[0]) + (arg2
[0]));
1037 let x2
: u32 = ((arg1
[1]) + (arg2
[1]));
1038 let x3
: u32 = ((arg1
[2]) + (arg2
[2]));
1039 let x4
: u32 = ((arg1
[3]) + (arg2
[3]));
1040 let x5
: u32 = ((arg1
[4]) + (arg2
[4]));
1041 let x6
: u32 = ((arg1
[5]) + (arg2
[5]));
1042 let x7
: u32 = ((arg1
[6]) + (arg2
[6]));
1043 let x8
: u32 = ((arg1
[7]) + (arg2
[7]));
1044 let x9
: u32 = ((arg1
[8]) + (arg2
[8]));
1045 let x10
: u32 = ((arg1
[9]) + (arg2
[9]));
1046 let x11
: u32 = ((arg1
[10]) + (arg2
[10]));
1047 let x12
: u32 = ((arg1
[11]) + (arg2
[11]));
1048 let x13
: u32 = ((arg1
[12]) + (arg2
[12]));
1049 let x14
: u32 = ((arg1
[13]) + (arg2
[13]));
1050 let x15
: u32 = ((arg1
[14]) + (arg2
[14]));
1051 let x16
: u32 = ((arg1
[15]) + (arg2
[15]));
1070 /// The function fiat_p448_sub subtracts two field elements.
1073 /// eval out1 mod m = (eval arg1 - eval arg2) mod m
1076 pub fn fiat_p448_sub(out1
: &mut fiat_p448_loose_field_element
, arg1
: &fiat_p448_tight_field_element
, arg2
: &fiat_p448_tight_field_element
) -> () {
1077 let x1
: u32 = ((0x1ffffffe + (arg1
[0])) - (arg2
[0]));
1078 let x2
: u32 = ((0x1ffffffe + (arg1
[1])) - (arg2
[1]));
1079 let x3
: u32 = ((0x1ffffffe + (arg1
[2])) - (arg2
[2]));
1080 let x4
: u32 = ((0x1ffffffe + (arg1
[3])) - (arg2
[3]));
1081 let x5
: u32 = ((0x1ffffffe + (arg1
[4])) - (arg2
[4]));
1082 let x6
: u32 = ((0x1ffffffe + (arg1
[5])) - (arg2
[5]));
1083 let x7
: u32 = ((0x1ffffffe + (arg1
[6])) - (arg2
[6]));
1084 let x8
: u32 = ((0x1ffffffe + (arg1
[7])) - (arg2
[7]));
1085 let x9
: u32 = ((0x1ffffffc + (arg1
[8])) - (arg2
[8]));
1086 let x10
: u32 = ((0x1ffffffe + (arg1
[9])) - (arg2
[9]));
1087 let x11
: u32 = ((0x1ffffffe + (arg1
[10])) - (arg2
[10]));
1088 let x12
: u32 = ((0x1ffffffe + (arg1
[11])) - (arg2
[11]));
1089 let x13
: u32 = ((0x1ffffffe + (arg1
[12])) - (arg2
[12]));
1090 let x14
: u32 = ((0x1ffffffe + (arg1
[13])) - (arg2
[13]));
1091 let x15
: u32 = ((0x1ffffffe + (arg1
[14])) - (arg2
[14]));
1092 let x16
: u32 = ((0x1ffffffe + (arg1
[15])) - (arg2
[15]));
1111 /// The function fiat_p448_opp negates a field element.
1114 /// eval out1 mod m = -eval arg1 mod m
1117 pub fn fiat_p448_opp(out1
: &mut fiat_p448_loose_field_element
, arg1
: &fiat_p448_tight_field_element
) -> () {
1118 let x1
: u32 = (0x1ffffffe - (arg1
[0]));
1119 let x2
: u32 = (0x1ffffffe - (arg1
[1]));
1120 let x3
: u32 = (0x1ffffffe - (arg1
[2]));
1121 let x4
: u32 = (0x1ffffffe - (arg1
[3]));
1122 let x5
: u32 = (0x1ffffffe - (arg1
[4]));
1123 let x6
: u32 = (0x1ffffffe - (arg1
[5]));
1124 let x7
: u32 = (0x1ffffffe - (arg1
[6]));
1125 let x8
: u32 = (0x1ffffffe - (arg1
[7]));
1126 let x9
: u32 = (0x1ffffffc - (arg1
[8]));
1127 let x10
: u32 = (0x1ffffffe - (arg1
[9]));
1128 let x11
: u32 = (0x1ffffffe - (arg1
[10]));
1129 let x12
: u32 = (0x1ffffffe - (arg1
[11]));
1130 let x13
: u32 = (0x1ffffffe - (arg1
[12]));
1131 let x14
: u32 = (0x1ffffffe - (arg1
[13]));
1132 let x15
: u32 = (0x1ffffffe - (arg1
[14]));
1133 let x16
: u32 = (0x1ffffffe - (arg1
[15]));
1152 /// The function fiat_p448_selectznz is a multi-limb conditional select.
1155 /// out1 = (if arg1 = 0 then arg2 else arg3)
1158 /// arg1: [0x0 ~> 0x1]
1159 /// arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
1160 /// arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
1162 /// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
1164 pub fn fiat_p448_selectznz(out1
: &mut [u32; 16], arg1
: fiat_p448_u1
, arg2
: &[u32; 16], arg3
: &[u32; 16]) -> () {
1165 let mut x1
: u32 = 0;
1166 fiat_p448_cmovznz_u32(&mut x1
, arg1
, (arg2
[0]), (arg3
[0]));
1167 let mut x2
: u32 = 0;
1168 fiat_p448_cmovznz_u32(&mut x2
, arg1
, (arg2
[1]), (arg3
[1]));
1169 let mut x3
: u32 = 0;
1170 fiat_p448_cmovznz_u32(&mut x3
, arg1
, (arg2
[2]), (arg3
[2]));
1171 let mut x4
: u32 = 0;
1172 fiat_p448_cmovznz_u32(&mut x4
, arg1
, (arg2
[3]), (arg3
[3]));
1173 let mut x5
: u32 = 0;
1174 fiat_p448_cmovznz_u32(&mut x5
, arg1
, (arg2
[4]), (arg3
[4]));
1175 let mut x6
: u32 = 0;
1176 fiat_p448_cmovznz_u32(&mut x6
, arg1
, (arg2
[5]), (arg3
[5]));
1177 let mut x7
: u32 = 0;
1178 fiat_p448_cmovznz_u32(&mut x7
, arg1
, (arg2
[6]), (arg3
[6]));
1179 let mut x8
: u32 = 0;
1180 fiat_p448_cmovznz_u32(&mut x8
, arg1
, (arg2
[7]), (arg3
[7]));
1181 let mut x9
: u32 = 0;
1182 fiat_p448_cmovznz_u32(&mut x9
, arg1
, (arg2
[8]), (arg3
[8]));
1183 let mut x10
: u32 = 0;
1184 fiat_p448_cmovznz_u32(&mut x10
, arg1
, (arg2
[9]), (arg3
[9]));
1185 let mut x11
: u32 = 0;
1186 fiat_p448_cmovznz_u32(&mut x11
, arg1
, (arg2
[10]), (arg3
[10]));
1187 let mut x12
: u32 = 0;
1188 fiat_p448_cmovznz_u32(&mut x12
, arg1
, (arg2
[11]), (arg3
[11]));
1189 let mut x13
: u32 = 0;
1190 fiat_p448_cmovznz_u32(&mut x13
, arg1
, (arg2
[12]), (arg3
[12]));
1191 let mut x14
: u32 = 0;
1192 fiat_p448_cmovznz_u32(&mut x14
, arg1
, (arg2
[13]), (arg3
[13]));
1193 let mut x15
: u32 = 0;
1194 fiat_p448_cmovznz_u32(&mut x15
, arg1
, (arg2
[14]), (arg3
[14]));
1195 let mut x16
: u32 = 0;
1196 fiat_p448_cmovznz_u32(&mut x16
, arg1
, (arg2
[15]), (arg3
[15]));
1215 /// The function fiat_p448_to_bytes serializes a field element to bytes in little-endian order.
1218 /// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..55]
1221 /// out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
1223 pub fn fiat_p448_to_bytes(out1
: &mut [u8; 56], arg1
: &fiat_p448_tight_field_element
) -> () {
1224 let mut x1
: u32 = 0;
1225 let mut x2
: fiat_p448_u1
= 0;
1226 fiat_p448_subborrowx_u28(&mut x1
, &mut x2
, 0x0, (arg1
[0]), 0xfffffff);
1227 let mut x3
: u32 = 0;
1228 let mut x4
: fiat_p448_u1
= 0;
1229 fiat_p448_subborrowx_u28(&mut x3
, &mut x4
, x2
, (arg1
[1]), 0xfffffff);
1230 let mut x5
: u32 = 0;
1231 let mut x6
: fiat_p448_u1
= 0;
1232 fiat_p448_subborrowx_u28(&mut x5
, &mut x6
, x4
, (arg1
[2]), 0xfffffff);
1233 let mut x7
: u32 = 0;
1234 let mut x8
: fiat_p448_u1
= 0;
1235 fiat_p448_subborrowx_u28(&mut x7
, &mut x8
, x6
, (arg1
[3]), 0xfffffff);
1236 let mut x9
: u32 = 0;
1237 let mut x10
: fiat_p448_u1
= 0;
1238 fiat_p448_subborrowx_u28(&mut x9
, &mut x10
, x8
, (arg1
[4]), 0xfffffff);
1239 let mut x11
: u32 = 0;
1240 let mut x12
: fiat_p448_u1
= 0;
1241 fiat_p448_subborrowx_u28(&mut x11
, &mut x12
, x10
, (arg1
[5]), 0xfffffff);
1242 let mut x13
: u32 = 0;
1243 let mut x14
: fiat_p448_u1
= 0;
1244 fiat_p448_subborrowx_u28(&mut x13
, &mut x14
, x12
, (arg1
[6]), 0xfffffff);
1245 let mut x15
: u32 = 0;
1246 let mut x16
: fiat_p448_u1
= 0;
1247 fiat_p448_subborrowx_u28(&mut x15
, &mut x16
, x14
, (arg1
[7]), 0xfffffff);
1248 let mut x17
: u32 = 0;
1249 let mut x18
: fiat_p448_u1
= 0;
1250 fiat_p448_subborrowx_u28(&mut x17
, &mut x18
, x16
, (arg1
[8]), 0xffffffe);
1251 let mut x19
: u32 = 0;
1252 let mut x20
: fiat_p448_u1
= 0;
1253 fiat_p448_subborrowx_u28(&mut x19
, &mut x20
, x18
, (arg1
[9]), 0xfffffff);
1254 let mut x21
: u32 = 0;
1255 let mut x22
: fiat_p448_u1
= 0;
1256 fiat_p448_subborrowx_u28(&mut x21
, &mut x22
, x20
, (arg1
[10]), 0xfffffff);
1257 let mut x23
: u32 = 0;
1258 let mut x24
: fiat_p448_u1
= 0;
1259 fiat_p448_subborrowx_u28(&mut x23
, &mut x24
, x22
, (arg1
[11]), 0xfffffff);
1260 let mut x25
: u32 = 0;
1261 let mut x26
: fiat_p448_u1
= 0;
1262 fiat_p448_subborrowx_u28(&mut x25
, &mut x26
, x24
, (arg1
[12]), 0xfffffff);
1263 let mut x27
: u32 = 0;
1264 let mut x28
: fiat_p448_u1
= 0;
1265 fiat_p448_subborrowx_u28(&mut x27
, &mut x28
, x26
, (arg1
[13]), 0xfffffff);
1266 let mut x29
: u32 = 0;
1267 let mut x30
: fiat_p448_u1
= 0;
1268 fiat_p448_subborrowx_u28(&mut x29
, &mut x30
, x28
, (arg1
[14]), 0xfffffff);
1269 let mut x31
: u32 = 0;
1270 let mut x32
: fiat_p448_u1
= 0;
1271 fiat_p448_subborrowx_u28(&mut x31
, &mut x32
, x30
, (arg1
[15]), 0xfffffff);
1272 let mut x33
: u32 = 0;
1273 fiat_p448_cmovznz_u32(&mut x33
, x32
, (0x0 as u32), 0xffffffff);
1274 let mut x34
: u32 = 0;
1275 let mut x35
: fiat_p448_u1
= 0;
1276 fiat_p448_addcarryx_u28(&mut x34
, &mut x35
, 0x0, x1
, (x33
& 0xfffffff));
1277 let mut x36
: u32 = 0;
1278 let mut x37
: fiat_p448_u1
= 0;
1279 fiat_p448_addcarryx_u28(&mut x36
, &mut x37
, x35
, x3
, (x33
& 0xfffffff));
1280 let mut x38
: u32 = 0;
1281 let mut x39
: fiat_p448_u1
= 0;
1282 fiat_p448_addcarryx_u28(&mut x38
, &mut x39
, x37
, x5
, (x33
& 0xfffffff));
1283 let mut x40
: u32 = 0;
1284 let mut x41
: fiat_p448_u1
= 0;
1285 fiat_p448_addcarryx_u28(&mut x40
, &mut x41
, x39
, x7
, (x33
& 0xfffffff));
1286 let mut x42
: u32 = 0;
1287 let mut x43
: fiat_p448_u1
= 0;
1288 fiat_p448_addcarryx_u28(&mut x42
, &mut x43
, x41
, x9
, (x33
& 0xfffffff));
1289 let mut x44
: u32 = 0;
1290 let mut x45
: fiat_p448_u1
= 0;
1291 fiat_p448_addcarryx_u28(&mut x44
, &mut x45
, x43
, x11
, (x33
& 0xfffffff));
1292 let mut x46
: u32 = 0;
1293 let mut x47
: fiat_p448_u1
= 0;
1294 fiat_p448_addcarryx_u28(&mut x46
, &mut x47
, x45
, x13
, (x33
& 0xfffffff));
1295 let mut x48
: u32 = 0;
1296 let mut x49
: fiat_p448_u1
= 0;
1297 fiat_p448_addcarryx_u28(&mut x48
, &mut x49
, x47
, x15
, (x33
& 0xfffffff));
1298 let mut x50
: u32 = 0;
1299 let mut x51
: fiat_p448_u1
= 0;
1300 fiat_p448_addcarryx_u28(&mut x50
, &mut x51
, x49
, x17
, (x33
& 0xffffffe));
1301 let mut x52
: u32 = 0;
1302 let mut x53
: fiat_p448_u1
= 0;
1303 fiat_p448_addcarryx_u28(&mut x52
, &mut x53
, x51
, x19
, (x33
& 0xfffffff));
1304 let mut x54
: u32 = 0;
1305 let mut x55
: fiat_p448_u1
= 0;
1306 fiat_p448_addcarryx_u28(&mut x54
, &mut x55
, x53
, x21
, (x33
& 0xfffffff));
1307 let mut x56
: u32 = 0;
1308 let mut x57
: fiat_p448_u1
= 0;
1309 fiat_p448_addcarryx_u28(&mut x56
, &mut x57
, x55
, x23
, (x33
& 0xfffffff));
1310 let mut x58
: u32 = 0;
1311 let mut x59
: fiat_p448_u1
= 0;
1312 fiat_p448_addcarryx_u28(&mut x58
, &mut x59
, x57
, x25
, (x33
& 0xfffffff));
1313 let mut x60
: u32 = 0;
1314 let mut x61
: fiat_p448_u1
= 0;
1315 fiat_p448_addcarryx_u28(&mut x60
, &mut x61
, x59
, x27
, (x33
& 0xfffffff));
1316 let mut x62
: u32 = 0;
1317 let mut x63
: fiat_p448_u1
= 0;
1318 fiat_p448_addcarryx_u28(&mut x62
, &mut x63
, x61
, x29
, (x33
& 0xfffffff));
1319 let mut x64
: u32 = 0;
1320 let mut x65
: fiat_p448_u1
= 0;
1321 fiat_p448_addcarryx_u28(&mut x64
, &mut x65
, x63
, x31
, (x33
& 0xfffffff));
1322 let x66
: u32 = (x64
<< 4);
1323 let x67
: u32 = (x60
<< 4);
1324 let x68
: u32 = (x56
<< 4);
1325 let x69
: u32 = (x52
<< 4);
1326 let x70
: u32 = (x48
<< 4);
1327 let x71
: u32 = (x44
<< 4);
1328 let x72
: u32 = (x40
<< 4);
1329 let x73
: u32 = (x36
<< 4);
1330 let x74
: u8 = ((x34
& (0xff as u32)) as u8);
1331 let x75
: u32 = (x34
>> 8);
1332 let x76
: u8 = ((x75
& (0xff as u32)) as u8);
1333 let x77
: u32 = (x75
>> 8);
1334 let x78
: u8 = ((x77
& (0xff as u32)) as u8);
1335 let x79
: u8 = ((x77
>> 8) as u8);
1336 let x80
: u32 = (x73
+ (x79
as u32));
1337 let x81
: u8 = ((x80
& (0xff as u32)) as u8);
1338 let x82
: u32 = (x80
>> 8);
1339 let x83
: u8 = ((x82
& (0xff as u32)) as u8);
1340 let x84
: u32 = (x82
>> 8);
1341 let x85
: u8 = ((x84
& (0xff as u32)) as u8);
1342 let x86
: u8 = ((x84
>> 8) as u8);
1343 let x87
: u8 = ((x38
& (0xff as u32)) as u8);
1344 let x88
: u32 = (x38
>> 8);
1345 let x89
: u8 = ((x88
& (0xff as u32)) as u8);
1346 let x90
: u32 = (x88
>> 8);
1347 let x91
: u8 = ((x90
& (0xff as u32)) as u8);
1348 let x92
: u8 = ((x90
>> 8) as u8);
1349 let x93
: u32 = (x72
+ (x92
as u32));
1350 let x94
: u8 = ((x93
& (0xff as u32)) as u8);
1351 let x95
: u32 = (x93
>> 8);
1352 let x96
: u8 = ((x95
& (0xff as u32)) as u8);
1353 let x97
: u32 = (x95
>> 8);
1354 let x98
: u8 = ((x97
& (0xff as u32)) as u8);
1355 let x99
: u8 = ((x97
>> 8) as u8);
1356 let x100
: u8 = ((x42
& (0xff as u32)) as u8);
1357 let x101
: u32 = (x42
>> 8);
1358 let x102
: u8 = ((x101
& (0xff as u32)) as u8);
1359 let x103
: u32 = (x101
>> 8);
1360 let x104
: u8 = ((x103
& (0xff as u32)) as u8);
1361 let x105
: u8 = ((x103
>> 8) as u8);
1362 let x106
: u32 = (x71
+ (x105
as u32));
1363 let x107
: u8 = ((x106
& (0xff as u32)) as u8);
1364 let x108
: u32 = (x106
>> 8);
1365 let x109
: u8 = ((x108
& (0xff as u32)) as u8);
1366 let x110
: u32 = (x108
>> 8);
1367 let x111
: u8 = ((x110
& (0xff as u32)) as u8);
1368 let x112
: u8 = ((x110
>> 8) as u8);
1369 let x113
: u8 = ((x46
& (0xff as u32)) as u8);
1370 let x114
: u32 = (x46
>> 8);
1371 let x115
: u8 = ((x114
& (0xff as u32)) as u8);
1372 let x116
: u32 = (x114
>> 8);
1373 let x117
: u8 = ((x116
& (0xff as u32)) as u8);
1374 let x118
: u8 = ((x116
>> 8) as u8);
1375 let x119
: u32 = (x70
+ (x118
as u32));
1376 let x120
: u8 = ((x119
& (0xff as u32)) as u8);
1377 let x121
: u32 = (x119
>> 8);
1378 let x122
: u8 = ((x121
& (0xff as u32)) as u8);
1379 let x123
: u32 = (x121
>> 8);
1380 let x124
: u8 = ((x123
& (0xff as u32)) as u8);
1381 let x125
: u8 = ((x123
>> 8) as u8);
1382 let x126
: u8 = ((x50
& (0xff as u32)) as u8);
1383 let x127
: u32 = (x50
>> 8);
1384 let x128
: u8 = ((x127
& (0xff as u32)) as u8);
1385 let x129
: u32 = (x127
>> 8);
1386 let x130
: u8 = ((x129
& (0xff as u32)) as u8);
1387 let x131
: u8 = ((x129
>> 8) as u8);
1388 let x132
: u32 = (x69
+ (x131
as u32));
1389 let x133
: u8 = ((x132
& (0xff as u32)) as u8);
1390 let x134
: u32 = (x132
>> 8);
1391 let x135
: u8 = ((x134
& (0xff as u32)) as u8);
1392 let x136
: u32 = (x134
>> 8);
1393 let x137
: u8 = ((x136
& (0xff as u32)) as u8);
1394 let x138
: u8 = ((x136
>> 8) as u8);
1395 let x139
: u8 = ((x54
& (0xff as u32)) as u8);
1396 let x140
: u32 = (x54
>> 8);
1397 let x141
: u8 = ((x140
& (0xff as u32)) as u8);
1398 let x142
: u32 = (x140
>> 8);
1399 let x143
: u8 = ((x142
& (0xff as u32)) as u8);
1400 let x144
: u8 = ((x142
>> 8) as u8);
1401 let x145
: u32 = (x68
+ (x144
as u32));
1402 let x146
: u8 = ((x145
& (0xff as u32)) as u8);
1403 let x147
: u32 = (x145
>> 8);
1404 let x148
: u8 = ((x147
& (0xff as u32)) as u8);
1405 let x149
: u32 = (x147
>> 8);
1406 let x150
: u8 = ((x149
& (0xff as u32)) as u8);
1407 let x151
: u8 = ((x149
>> 8) as u8);
1408 let x152
: u8 = ((x58
& (0xff as u32)) as u8);
1409 let x153
: u32 = (x58
>> 8);
1410 let x154
: u8 = ((x153
& (0xff as u32)) as u8);
1411 let x155
: u32 = (x153
>> 8);
1412 let x156
: u8 = ((x155
& (0xff as u32)) as u8);
1413 let x157
: u8 = ((x155
>> 8) as u8);
1414 let x158
: u32 = (x67
+ (x157
as u32));
1415 let x159
: u8 = ((x158
& (0xff as u32)) as u8);
1416 let x160
: u32 = (x158
>> 8);
1417 let x161
: u8 = ((x160
& (0xff as u32)) as u8);
1418 let x162
: u32 = (x160
>> 8);
1419 let x163
: u8 = ((x162
& (0xff as u32)) as u8);
1420 let x164
: u8 = ((x162
>> 8) as u8);
1421 let x165
: u8 = ((x62
& (0xff as u32)) as u8);
1422 let x166
: u32 = (x62
>> 8);
1423 let x167
: u8 = ((x166
& (0xff as u32)) as u8);
1424 let x168
: u32 = (x166
>> 8);
1425 let x169
: u8 = ((x168
& (0xff as u32)) as u8);
1426 let x170
: u8 = ((x168
>> 8) as u8);
1427 let x171
: u32 = (x66
+ (x170
as u32));
1428 let x172
: u8 = ((x171
& (0xff as u32)) as u8);
1429 let x173
: u32 = (x171
>> 8);
1430 let x174
: u8 = ((x173
& (0xff as u32)) as u8);
1431 let x175
: u32 = (x173
>> 8);
1432 let x176
: u8 = ((x175
& (0xff as u32)) as u8);
1433 let x177
: u8 = ((x175
>> 8) as u8);
1492 /// The function fiat_p448_from_bytes deserializes a field element from bytes in little-endian order.
1495 /// eval out1 mod m = bytes_eval arg1 mod m
1498 /// arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff]]
1500 pub fn fiat_p448_from_bytes(out1
: &mut fiat_p448_tight_field_element
, arg1
: &[u8; 56]) -> () {
1501 let x1
: u32 = (((arg1
[55]) as u32) << 20);
1502 let x2
: u32 = (((arg1
[54]) as u32) << 12);
1503 let x3
: u32 = (((arg1
[53]) as u32) << 4);
1504 let x4
: u32 = (((arg1
[52]) as u32) << 24);
1505 let x5
: u32 = (((arg1
[51]) as u32) << 16);
1506 let x6
: u32 = (((arg1
[50]) as u32) << 8);
1507 let x7
: u8 = (arg1
[49]);
1508 let x8
: u32 = (((arg1
[48]) as u32) << 20);
1509 let x9
: u32 = (((arg1
[47]) as u32) << 12);
1510 let x10
: u32 = (((arg1
[46]) as u32) << 4);
1511 let x11
: u32 = (((arg1
[45]) as u32) << 24);
1512 let x12
: u32 = (((arg1
[44]) as u32) << 16);
1513 let x13
: u32 = (((arg1
[43]) as u32) << 8);
1514 let x14
: u8 = (arg1
[42]);
1515 let x15
: u32 = (((arg1
[41]) as u32) << 20);
1516 let x16
: u32 = (((arg1
[40]) as u32) << 12);
1517 let x17
: u32 = (((arg1
[39]) as u32) << 4);
1518 let x18
: u32 = (((arg1
[38]) as u32) << 24);
1519 let x19
: u32 = (((arg1
[37]) as u32) << 16);
1520 let x20
: u32 = (((arg1
[36]) as u32) << 8);
1521 let x21
: u8 = (arg1
[35]);
1522 let x22
: u32 = (((arg1
[34]) as u32) << 20);
1523 let x23
: u32 = (((arg1
[33]) as u32) << 12);
1524 let x24
: u32 = (((arg1
[32]) as u32) << 4);
1525 let x25
: u32 = (((arg1
[31]) as u32) << 24);
1526 let x26
: u32 = (((arg1
[30]) as u32) << 16);
1527 let x27
: u32 = (((arg1
[29]) as u32) << 8);
1528 let x28
: u8 = (arg1
[28]);
1529 let x29
: u32 = (((arg1
[27]) as u32) << 20);
1530 let x30
: u32 = (((arg1
[26]) as u32) << 12);
1531 let x31
: u32 = (((arg1
[25]) as u32) << 4);
1532 let x32
: u32 = (((arg1
[24]) as u32) << 24);
1533 let x33
: u32 = (((arg1
[23]) as u32) << 16);
1534 let x34
: u32 = (((arg1
[22]) as u32) << 8);
1535 let x35
: u8 = (arg1
[21]);
1536 let x36
: u32 = (((arg1
[20]) as u32) << 20);
1537 let x37
: u32 = (((arg1
[19]) as u32) << 12);
1538 let x38
: u32 = (((arg1
[18]) as u32) << 4);
1539 let x39
: u32 = (((arg1
[17]) as u32) << 24);
1540 let x40
: u32 = (((arg1
[16]) as u32) << 16);
1541 let x41
: u32 = (((arg1
[15]) as u32) << 8);
1542 let x42
: u8 = (arg1
[14]);
1543 let x43
: u32 = (((arg1
[13]) as u32) << 20);
1544 let x44
: u32 = (((arg1
[12]) as u32) << 12);
1545 let x45
: u32 = (((arg1
[11]) as u32) << 4);
1546 let x46
: u32 = (((arg1
[10]) as u32) << 24);
1547 let x47
: u32 = (((arg1
[9]) as u32) << 16);
1548 let x48
: u32 = (((arg1
[8]) as u32) << 8);
1549 let x49
: u8 = (arg1
[7]);
1550 let x50
: u32 = (((arg1
[6]) as u32) << 20);
1551 let x51
: u32 = (((arg1
[5]) as u32) << 12);
1552 let x52
: u32 = (((arg1
[4]) as u32) << 4);
1553 let x53
: u32 = (((arg1
[3]) as u32) << 24);
1554 let x54
: u32 = (((arg1
[2]) as u32) << 16);
1555 let x55
: u32 = (((arg1
[1]) as u32) << 8);
1556 let x56
: u8 = (arg1
[0]);
1557 let x57
: u32 = (x55
+ (x56
as u32));
1558 let x58
: u32 = (x54
+ x57
);
1559 let x59
: u32 = (x53
+ x58
);
1560 let x60
: u32 = (x59
& 0xfffffff);
1561 let x61
: u8 = ((x59
>> 28) as u8);
1562 let x62
: u32 = (x52
+ (x61
as u32));
1563 let x63
: u32 = (x51
+ x62
);
1564 let x64
: u32 = (x50
+ x63
);
1565 let x65
: u32 = (x48
+ (x49
as u32));
1566 let x66
: u32 = (x47
+ x65
);
1567 let x67
: u32 = (x46
+ x66
);
1568 let x68
: u32 = (x67
& 0xfffffff);
1569 let x69
: u8 = ((x67
>> 28) as u8);
1570 let x70
: u32 = (x45
+ (x69
as u32));
1571 let x71
: u32 = (x44
+ x70
);
1572 let x72
: u32 = (x43
+ x71
);
1573 let x73
: u32 = (x41
+ (x42
as u32));
1574 let x74
: u32 = (x40
+ x73
);
1575 let x75
: u32 = (x39
+ x74
);
1576 let x76
: u32 = (x75
& 0xfffffff);
1577 let x77
: u8 = ((x75
>> 28) as u8);
1578 let x78
: u32 = (x38
+ (x77
as u32));
1579 let x79
: u32 = (x37
+ x78
);
1580 let x80
: u32 = (x36
+ x79
);
1581 let x81
: u32 = (x34
+ (x35
as u32));
1582 let x82
: u32 = (x33
+ x81
);
1583 let x83
: u32 = (x32
+ x82
);
1584 let x84
: u32 = (x83
& 0xfffffff);
1585 let x85
: u8 = ((x83
>> 28) as u8);
1586 let x86
: u32 = (x31
+ (x85
as u32));
1587 let x87
: u32 = (x30
+ x86
);
1588 let x88
: u32 = (x29
+ x87
);
1589 let x89
: u32 = (x27
+ (x28
as u32));
1590 let x90
: u32 = (x26
+ x89
);
1591 let x91
: u32 = (x25
+ x90
);
1592 let x92
: u32 = (x91
& 0xfffffff);
1593 let x93
: u8 = ((x91
>> 28) as u8);
1594 let x94
: u32 = (x24
+ (x93
as u32));
1595 let x95
: u32 = (x23
+ x94
);
1596 let x96
: u32 = (x22
+ x95
);
1597 let x97
: u32 = (x20
+ (x21
as u32));
1598 let x98
: u32 = (x19
+ x97
);
1599 let x99
: u32 = (x18
+ x98
);
1600 let x100
: u32 = (x99
& 0xfffffff);
1601 let x101
: u8 = ((x99
>> 28) as u8);
1602 let x102
: u32 = (x17
+ (x101
as u32));
1603 let x103
: u32 = (x16
+ x102
);
1604 let x104
: u32 = (x15
+ x103
);
1605 let x105
: u32 = (x13
+ (x14
as u32));
1606 let x106
: u32 = (x12
+ x105
);
1607 let x107
: u32 = (x11
+ x106
);
1608 let x108
: u32 = (x107
& 0xfffffff);
1609 let x109
: u8 = ((x107
>> 28) as u8);
1610 let x110
: u32 = (x10
+ (x109
as u32));
1611 let x111
: u32 = (x9
+ x110
);
1612 let x112
: u32 = (x8
+ x111
);
1613 let x113
: u32 = (x6
+ (x7
as u32));
1614 let x114
: u32 = (x5
+ x113
);
1615 let x115
: u32 = (x4
+ x114
);
1616 let x116
: u32 = (x115
& 0xfffffff);
1617 let x117
: u8 = ((x115
>> 28) as u8);
1618 let x118
: u32 = (x3
+ (x117
as u32));
1619 let x119
: u32 = (x2
+ x118
);
1620 let x120
: u32 = (x1
+ x119
);
1639 /// The function fiat_p448_relax is the identity function converting from tight field elements to loose field elements.
1645 pub fn fiat_p448_relax(out1
: &mut fiat_p448_loose_field_element
, arg1
: &fiat_p448_tight_field_element
) -> () {
1646 let x1
: u32 = (arg1
[0]);
1647 let x2
: u32 = (arg1
[1]);
1648 let x3
: u32 = (arg1
[2]);
1649 let x4
: u32 = (arg1
[3]);
1650 let x5
: u32 = (arg1
[4]);
1651 let x6
: u32 = (arg1
[5]);
1652 let x7
: u32 = (arg1
[6]);
1653 let x8
: u32 = (arg1
[7]);
1654 let x9
: u32 = (arg1
[8]);
1655 let x10
: u32 = (arg1
[9]);
1656 let x11
: u32 = (arg1
[10]);
1657 let x12
: u32 = (arg1
[11]);
1658 let x13
: u32 = (arg1
[12]);
1659 let x14
: u32 = (arg1
[13]);
1660 let x15
: u32 = (arg1
[14]);
1661 let x16
: u32 = (arg1
[15]);