1 //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 64 3 '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
2 //! curve description: poly1305
3 //! machine_wordsize = 64 (from "64")
4 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
6 //! s-c = 2^130 - [(1, 5)] (from "2^130 - 5")
7 //! tight_bounds_multiplier = 1 (from "")
10 //! carry_chain = [0, 1, 2, 0, 1]
11 //! eval z = z[0] + (z[1] << 44) + (z[2] << 87)
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)
13 //! balance = [0x1ffffffffff6, 0xffffffffffe, 0xffffffffffe]
15 #![allow(unused_parens)]
16 #![allow(non_camel_case_types)]
18 pub type fiat_poly1305_u1
= u8;
19 pub type fiat_poly1305_i1
= i8;
20 pub type fiat_poly1305_u2
= u8;
21 pub type fiat_poly1305_i2
= i8;
23 /* The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
24 /* Bounds: [[0x0 ~> 0x300000000000], [0x0 ~> 0x180000000000], [0x0 ~> 0x180000000000]] */
25 pub type fiat_poly1305_loose_field_element
= [u64; 3];
27 /* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
28 /* Bounds: [[0x0 ~> 0x100000000000], [0x0 ~> 0x80000000000], [0x0 ~> 0x80000000000]] */
29 pub type fiat_poly1305_tight_field_element
= [u64; 3];
32 /// The function fiat_poly1305_addcarryx_u44 is an addition with carry.
35 /// out1 = (arg1 + arg2 + arg3) mod 2^44
36 /// out2 = ⌊(arg1 + arg2 + arg3) / 2^44⌋
39 /// arg1: [0x0 ~> 0x1]
40 /// arg2: [0x0 ~> 0xfffffffffff]
41 /// arg3: [0x0 ~> 0xfffffffffff]
43 /// out1: [0x0 ~> 0xfffffffffff]
44 /// out2: [0x0 ~> 0x1]
46 pub fn fiat_poly1305_addcarryx_u44(out1
: &mut u64, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_u1
, arg2
: u64, arg3
: u64) -> () {
47 let x1
: u64 = (((arg1
as u64) + arg2
) + arg3
);
48 let x2
: u64 = (x1
& 0xfffffffffff);
49 let x3
: fiat_poly1305_u1
= ((x1
>> 44) as fiat_poly1305_u1
);
54 /// The function fiat_poly1305_subborrowx_u44 is a subtraction with borrow.
57 /// out1 = (-arg1 + arg2 + -arg3) mod 2^44
58 /// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^44⌋
61 /// arg1: [0x0 ~> 0x1]
62 /// arg2: [0x0 ~> 0xfffffffffff]
63 /// arg3: [0x0 ~> 0xfffffffffff]
65 /// out1: [0x0 ~> 0xfffffffffff]
66 /// out2: [0x0 ~> 0x1]
68 pub fn fiat_poly1305_subborrowx_u44(out1
: &mut u64, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_u1
, arg2
: u64, arg3
: u64) -> () {
69 let x1
: i64 = ((((((arg2
as i128
) - (arg1
as i128
)) as i64) as i128
) - (arg3
as i128
)) as i64);
70 let x2
: fiat_poly1305_i1
= ((x1
>> 44) as fiat_poly1305_i1
);
71 let x3
: u64 = (((x1
as i128
) & (0xfffffffffff as i128
)) as u64);
73 *out2
= (((0x0 as fiat_poly1305_i2
) - (x2
as fiat_poly1305_i2
)) as fiat_poly1305_u1
);
76 /// The function fiat_poly1305_addcarryx_u43 is an addition with carry.
79 /// out1 = (arg1 + arg2 + arg3) mod 2^43
80 /// out2 = ⌊(arg1 + arg2 + arg3) / 2^43⌋
83 /// arg1: [0x0 ~> 0x1]
84 /// arg2: [0x0 ~> 0x7ffffffffff]
85 /// arg3: [0x0 ~> 0x7ffffffffff]
87 /// out1: [0x0 ~> 0x7ffffffffff]
88 /// out2: [0x0 ~> 0x1]
90 pub fn fiat_poly1305_addcarryx_u43(out1
: &mut u64, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_u1
, arg2
: u64, arg3
: u64) -> () {
91 let x1
: u64 = (((arg1
as u64) + arg2
) + arg3
);
92 let x2
: u64 = (x1
& 0x7ffffffffff);
93 let x3
: fiat_poly1305_u1
= ((x1
>> 43) as fiat_poly1305_u1
);
98 /// The function fiat_poly1305_subborrowx_u43 is a subtraction with borrow.
101 /// out1 = (-arg1 + arg2 + -arg3) mod 2^43
102 /// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^43⌋
105 /// arg1: [0x0 ~> 0x1]
106 /// arg2: [0x0 ~> 0x7ffffffffff]
107 /// arg3: [0x0 ~> 0x7ffffffffff]
109 /// out1: [0x0 ~> 0x7ffffffffff]
110 /// out2: [0x0 ~> 0x1]
112 pub fn fiat_poly1305_subborrowx_u43(out1
: &mut u64, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_u1
, arg2
: u64, arg3
: u64) -> () {
113 let x1
: i64 = ((((((arg2
as i128
) - (arg1
as i128
)) as i64) as i128
) - (arg3
as i128
)) as i64);
114 let x2
: fiat_poly1305_i1
= ((x1
>> 43) as fiat_poly1305_i1
);
115 let x3
: u64 = (((x1
as i128
) & (0x7ffffffffff as i128
)) as u64);
117 *out2
= (((0x0 as fiat_poly1305_i2
) - (x2
as fiat_poly1305_i2
)) as fiat_poly1305_u1
);
120 /// The function fiat_poly1305_cmovznz_u64 is a single-word conditional move.
123 /// out1 = (if arg1 = 0 then arg2 else arg3)
126 /// arg1: [0x0 ~> 0x1]
127 /// arg2: [0x0 ~> 0xffffffffffffffff]
128 /// arg3: [0x0 ~> 0xffffffffffffffff]
130 /// out1: [0x0 ~> 0xffffffffffffffff]
132 pub fn fiat_poly1305_cmovznz_u64(out1
: &mut u64, arg1
: fiat_poly1305_u1
, arg2
: u64, arg3
: u64) -> () {
133 let x1
: fiat_poly1305_u1
= (!(!arg1
));
134 let x2
: u64 = ((((((0x0 as fiat_poly1305_i2
) - (x1
as fiat_poly1305_i2
)) as fiat_poly1305_i1
) as i128
) & (0xffffffffffffffff as i128
)) as u64);
135 let x3
: u64 = ((x2
& arg3
) | ((!x2
) & arg2
));
139 /// The function fiat_poly1305_carry_mul multiplies two field elements and reduces the result.
142 /// eval out1 mod m = (eval arg1 * eval arg2) mod m
145 pub fn fiat_poly1305_carry_mul(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
, arg2
: &fiat_poly1305_loose_field_element
) -> () {
146 let x1
: u128
= (((arg1
[2]) as u128
) * (((arg2
[2]) * 0x5) as u128
));
147 let x2
: u128
= (((arg1
[2]) as u128
) * (((arg2
[1]) * 0xa) as u128
));
148 let x3
: u128
= (((arg1
[1]) as u128
) * (((arg2
[2]) * 0xa) as u128
));
149 let x4
: u128
= (((arg1
[2]) as u128
) * ((arg2
[0]) as u128
));
150 let x5
: u128
= (((arg1
[1]) as u128
) * (((arg2
[1]) * 0x2) as u128
));
151 let x6
: u128
= (((arg1
[1]) as u128
) * ((arg2
[0]) as u128
));
152 let x7
: u128
= (((arg1
[0]) as u128
) * ((arg2
[2]) as u128
));
153 let x8
: u128
= (((arg1
[0]) as u128
) * ((arg2
[1]) as u128
));
154 let x9
: u128
= (((arg1
[0]) as u128
) * ((arg2
[0]) as u128
));
155 let x10
: u128
= (x9
+ (x3
+ x2
));
156 let x11
: u64 = ((x10
>> 44) as u64);
157 let x12
: u64 = ((x10
& (0xfffffffffff as u128
)) as u64);
158 let x13
: u128
= (x7
+ (x5
+ x4
));
159 let x14
: u128
= (x8
+ (x6
+ x1
));
160 let x15
: u128
= ((x11
as u128
) + x14
);
161 let x16
: u64 = ((x15
>> 43) as u64);
162 let x17
: u64 = ((x15
& (0x7ffffffffff as u128
)) as u64);
163 let x18
: u128
= ((x16
as u128
) + x13
);
164 let x19
: u64 = ((x18
>> 43) as u64);
165 let x20
: u64 = ((x18
& (0x7ffffffffff as u128
)) as u64);
166 let x21
: u64 = (x19
* 0x5);
167 let x22
: u64 = (x12
+ x21
);
168 let x23
: u64 = (x22
>> 44);
169 let x24
: u64 = (x22
& 0xfffffffffff);
170 let x25
: u64 = (x23
+ x17
);
171 let x26
: fiat_poly1305_u1
= ((x25
>> 43) as fiat_poly1305_u1
);
172 let x27
: u64 = (x25
& 0x7ffffffffff);
173 let x28
: u64 = ((x26
as u64) + x20
);
179 /// The function fiat_poly1305_carry_square squares a field element and reduces the result.
182 /// eval out1 mod m = (eval arg1 * eval arg1) mod m
185 pub fn fiat_poly1305_carry_square(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
) -> () {
186 let x1
: u64 = ((arg1
[2]) * 0x5);
187 let x2
: u64 = (x1
* 0x2);
188 let x3
: u64 = ((arg1
[2]) * 0x2);
189 let x4
: u64 = ((arg1
[1]) * 0x2);
190 let x5
: u128
= (((arg1
[2]) as u128
) * (x1
as u128
));
191 let x6
: u128
= (((arg1
[1]) as u128
) * ((x2
* 0x2) as u128
));
192 let x7
: u128
= (((arg1
[1]) as u128
) * (((arg1
[1]) * 0x2) as u128
));
193 let x8
: u128
= (((arg1
[0]) as u128
) * (x3
as u128
));
194 let x9
: u128
= (((arg1
[0]) as u128
) * (x4
as u128
));
195 let x10
: u128
= (((arg1
[0]) as u128
) * ((arg1
[0]) as u128
));
196 let x11
: u128
= (x10
+ x6
);
197 let x12
: u64 = ((x11
>> 44) as u64);
198 let x13
: u64 = ((x11
& (0xfffffffffff as u128
)) as u64);
199 let x14
: u128
= (x8
+ x7
);
200 let x15
: u128
= (x9
+ x5
);
201 let x16
: u128
= ((x12
as u128
) + x15
);
202 let x17
: u64 = ((x16
>> 43) as u64);
203 let x18
: u64 = ((x16
& (0x7ffffffffff as u128
)) as u64);
204 let x19
: u128
= ((x17
as u128
) + x14
);
205 let x20
: u64 = ((x19
>> 43) as u64);
206 let x21
: u64 = ((x19
& (0x7ffffffffff as u128
)) as u64);
207 let x22
: u64 = (x20
* 0x5);
208 let x23
: u64 = (x13
+ x22
);
209 let x24
: u64 = (x23
>> 44);
210 let x25
: u64 = (x23
& 0xfffffffffff);
211 let x26
: u64 = (x24
+ x18
);
212 let x27
: fiat_poly1305_u1
= ((x26
>> 43) as fiat_poly1305_u1
);
213 let x28
: u64 = (x26
& 0x7ffffffffff);
214 let x29
: u64 = ((x27
as u64) + x21
);
220 /// The function fiat_poly1305_carry reduces a field element.
223 /// eval out1 mod m = eval arg1 mod m
226 pub fn fiat_poly1305_carry(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
) -> () {
227 let x1
: u64 = (arg1
[0]);
228 let x2
: u64 = ((x1
>> 44) + (arg1
[1]));
229 let x3
: u64 = ((x2
>> 43) + (arg1
[2]));
230 let x4
: u64 = ((x1
& 0xfffffffffff) + ((x3
>> 43) * 0x5));
231 let x5
: u64 = ((((x4
>> 44) as fiat_poly1305_u1
) as u64) + (x2
& 0x7ffffffffff));
232 let x6
: u64 = (x4
& 0xfffffffffff);
233 let x7
: u64 = (x5
& 0x7ffffffffff);
234 let x8
: u64 = ((((x5
>> 43) as fiat_poly1305_u1
) as u64) + (x3
& 0x7ffffffffff));
240 /// The function fiat_poly1305_add adds two field elements.
243 /// eval out1 mod m = (eval arg1 + eval arg2) mod m
246 pub fn fiat_poly1305_add(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
, arg2
: &fiat_poly1305_tight_field_element
) -> () {
247 let x1
: u64 = ((arg1
[0]) + (arg2
[0]));
248 let x2
: u64 = ((arg1
[1]) + (arg2
[1]));
249 let x3
: u64 = ((arg1
[2]) + (arg2
[2]));
255 /// The function fiat_poly1305_sub subtracts two field elements.
258 /// eval out1 mod m = (eval arg1 - eval arg2) mod m
261 pub fn fiat_poly1305_sub(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
, arg2
: &fiat_poly1305_tight_field_element
) -> () {
262 let x1
: u64 = ((0x1ffffffffff6 + (arg1
[0])) - (arg2
[0]));
263 let x2
: u64 = ((0xffffffffffe + (arg1
[1])) - (arg2
[1]));
264 let x3
: u64 = ((0xffffffffffe + (arg1
[2])) - (arg2
[2]));
270 /// The function fiat_poly1305_opp negates a field element.
273 /// eval out1 mod m = -eval arg1 mod m
276 pub fn fiat_poly1305_opp(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
) -> () {
277 let x1
: u64 = (0x1ffffffffff6 - (arg1
[0]));
278 let x2
: u64 = (0xffffffffffe - (arg1
[1]));
279 let x3
: u64 = (0xffffffffffe - (arg1
[2]));
285 /// The function fiat_poly1305_selectznz is a multi-limb conditional select.
288 /// out1 = (if arg1 = 0 then arg2 else arg3)
291 /// arg1: [0x0 ~> 0x1]
292 /// arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
293 /// arg3: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
295 /// out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
297 pub fn fiat_poly1305_selectznz(out1
: &mut [u64; 3], arg1
: fiat_poly1305_u1
, arg2
: &[u64; 3], arg3
: &[u64; 3]) -> () {
299 fiat_poly1305_cmovznz_u64(&mut x1
, arg1
, (arg2
[0]), (arg3
[0]));
301 fiat_poly1305_cmovznz_u64(&mut x2
, arg1
, (arg2
[1]), (arg3
[1]));
303 fiat_poly1305_cmovznz_u64(&mut x3
, arg1
, (arg2
[2]), (arg3
[2]));
309 /// The function fiat_poly1305_to_bytes serializes a field element to bytes in little-endian order.
312 /// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..16]
315 /// 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 ~> 0x3]]
317 pub fn fiat_poly1305_to_bytes(out1
: &mut [u8; 17], arg1
: &fiat_poly1305_tight_field_element
) -> () {
319 let mut x2
: fiat_poly1305_u1
= 0;
320 fiat_poly1305_subborrowx_u44(&mut x1
, &mut x2
, 0x0, (arg1
[0]), 0xffffffffffb);
322 let mut x4
: fiat_poly1305_u1
= 0;
323 fiat_poly1305_subborrowx_u43(&mut x3
, &mut x4
, x2
, (arg1
[1]), 0x7ffffffffff);
325 let mut x6
: fiat_poly1305_u1
= 0;
326 fiat_poly1305_subborrowx_u43(&mut x5
, &mut x6
, x4
, (arg1
[2]), 0x7ffffffffff);
328 fiat_poly1305_cmovznz_u64(&mut x7
, x6
, (0x0 as u64), 0xffffffffffffffff);
330 let mut x9
: fiat_poly1305_u1
= 0;
331 fiat_poly1305_addcarryx_u44(&mut x8
, &mut x9
, 0x0, x1
, (x7
& 0xffffffffffb));
332 let mut x10
: u64 = 0;
333 let mut x11
: fiat_poly1305_u1
= 0;
334 fiat_poly1305_addcarryx_u43(&mut x10
, &mut x11
, x9
, x3
, (x7
& 0x7ffffffffff));
335 let mut x12
: u64 = 0;
336 let mut x13
: fiat_poly1305_u1
= 0;
337 fiat_poly1305_addcarryx_u43(&mut x12
, &mut x13
, x11
, x5
, (x7
& 0x7ffffffffff));
338 let x14
: u64 = (x12
<< 7);
339 let x15
: u64 = (x10
<< 4);
340 let x16
: u8 = ((x8
& (0xff as u64)) as u8);
341 let x17
: u64 = (x8
>> 8);
342 let x18
: u8 = ((x17
& (0xff as u64)) as u8);
343 let x19
: u64 = (x17
>> 8);
344 let x20
: u8 = ((x19
& (0xff as u64)) as u8);
345 let x21
: u64 = (x19
>> 8);
346 let x22
: u8 = ((x21
& (0xff as u64)) as u8);
347 let x23
: u64 = (x21
>> 8);
348 let x24
: u8 = ((x23
& (0xff as u64)) as u8);
349 let x25
: u8 = ((x23
>> 8) as u8);
350 let x26
: u64 = (x15
+ (x25
as u64));
351 let x27
: u8 = ((x26
& (0xff as u64)) as u8);
352 let x28
: u64 = (x26
>> 8);
353 let x29
: u8 = ((x28
& (0xff as u64)) as u8);
354 let x30
: u64 = (x28
>> 8);
355 let x31
: u8 = ((x30
& (0xff as u64)) as u8);
356 let x32
: u64 = (x30
>> 8);
357 let x33
: u8 = ((x32
& (0xff as u64)) as u8);
358 let x34
: u64 = (x32
>> 8);
359 let x35
: u8 = ((x34
& (0xff as u64)) as u8);
360 let x36
: u8 = ((x34
>> 8) as u8);
361 let x37
: u64 = (x14
+ (x36
as u64));
362 let x38
: u8 = ((x37
& (0xff as u64)) as u8);
363 let x39
: u64 = (x37
>> 8);
364 let x40
: u8 = ((x39
& (0xff as u64)) as u8);
365 let x41
: u64 = (x39
>> 8);
366 let x42
: u8 = ((x41
& (0xff as u64)) as u8);
367 let x43
: u64 = (x41
>> 8);
368 let x44
: u8 = ((x43
& (0xff as u64)) as u8);
369 let x45
: u64 = (x43
>> 8);
370 let x46
: u8 = ((x45
& (0xff as u64)) as u8);
371 let x47
: u64 = (x45
>> 8);
372 let x48
: u8 = ((x47
& (0xff as u64)) as u8);
373 let x49
: u8 = ((x47
>> 8) as u8);
393 /// The function fiat_poly1305_from_bytes deserializes a field element from bytes in little-endian order.
396 /// eval out1 mod m = bytes_eval arg1 mod m
399 /// 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 ~> 0x3]]
401 pub fn fiat_poly1305_from_bytes(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &[u8; 17]) -> () {
402 let x1
: u64 = (((arg1
[16]) as u64) << 41);
403 let x2
: u64 = (((arg1
[15]) as u64) << 33);
404 let x3
: u64 = (((arg1
[14]) as u64) << 25);
405 let x4
: u64 = (((arg1
[13]) as u64) << 17);
406 let x5
: u64 = (((arg1
[12]) as u64) << 9);
407 let x6
: u64 = (((arg1
[11]) as u64) * (0x2 as u64));
408 let x7
: u64 = (((arg1
[10]) as u64) << 36);
409 let x8
: u64 = (((arg1
[9]) as u64) << 28);
410 let x9
: u64 = (((arg1
[8]) as u64) << 20);
411 let x10
: u64 = (((arg1
[7]) as u64) << 12);
412 let x11
: u64 = (((arg1
[6]) as u64) << 4);
413 let x12
: u64 = (((arg1
[5]) as u64) << 40);
414 let x13
: u64 = (((arg1
[4]) as u64) << 32);
415 let x14
: u64 = (((arg1
[3]) as u64) << 24);
416 let x15
: u64 = (((arg1
[2]) as u64) << 16);
417 let x16
: u64 = (((arg1
[1]) as u64) << 8);
418 let x17
: u8 = (arg1
[0]);
419 let x18
: u64 = (x16
+ (x17
as u64));
420 let x19
: u64 = (x15
+ x18
);
421 let x20
: u64 = (x14
+ x19
);
422 let x21
: u64 = (x13
+ x20
);
423 let x22
: u64 = (x12
+ x21
);
424 let x23
: u64 = (x22
& 0xfffffffffff);
425 let x24
: u8 = ((x22
>> 44) as u8);
426 let x25
: u64 = (x11
+ (x24
as u64));
427 let x26
: u64 = (x10
+ x25
);
428 let x27
: u64 = (x9
+ x26
);
429 let x28
: u64 = (x8
+ x27
);
430 let x29
: u64 = (x7
+ x28
);
431 let x30
: u64 = (x29
& 0x7ffffffffff);
432 let x31
: fiat_poly1305_u1
= ((x29
>> 43) as fiat_poly1305_u1
);
433 let x32
: u64 = (x6
+ (x31
as u64));
434 let x33
: u64 = (x5
+ x32
);
435 let x34
: u64 = (x4
+ x33
);
436 let x35
: u64 = (x3
+ x34
);
437 let x36
: u64 = (x2
+ x35
);
438 let x37
: u64 = (x1
+ x36
);
444 /// The function fiat_poly1305_relax is the identity function converting from tight field elements to loose field elements.
450 pub fn fiat_poly1305_relax(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
) -> () {
451 let x1
: u64 = (arg1
[0]);
452 let x2
: u64 = (arg1
[1]);
453 let x3
: u64 = (arg1
[2]);