1 //! Autogenerated: 'src/ExtractionOCaml/unsaturated_solinas' --lang Rust --inline poly1305 32 '(auto)' '2^130 - 5' carry_mul carry_square carry add sub opp selectznz to_bytes from_bytes relax
2 //! curve description: poly1305
3 //! machine_wordsize = 32 (from "32")
4 //! requested operations: carry_mul, carry_square, carry, add, sub, opp, selectznz, to_bytes, from_bytes, relax
5 //! n = 5 (from "(auto)")
6 //! s-c = 2^130 - [(1, 5)] (from "2^130 - 5")
7 //! tight_bounds_multiplier = 1 (from "")
10 //! carry_chain = [0, 1, 2, 3, 4, 0, 1]
11 //! eval z = z[0] + (z[1] << 26) + (z[2] << 52) + (z[3] << 78) + (z[4] << 104)
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 = [0x7fffff6, 0x7fffffe, 0x7fffffe, 0x7fffffe, 0x7fffffe]
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 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000]] */
25 pub type fiat_poly1305_loose_field_element
= [u32; 5];
27 /* The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
28 /* Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000]] */
29 pub type fiat_poly1305_tight_field_element
= [u32; 5];
32 /// The function fiat_poly1305_addcarryx_u26 is an addition with carry.
35 /// out1 = (arg1 + arg2 + arg3) mod 2^26
36 /// out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋
39 /// arg1: [0x0 ~> 0x1]
40 /// arg2: [0x0 ~> 0x3ffffff]
41 /// arg3: [0x0 ~> 0x3ffffff]
43 /// out1: [0x0 ~> 0x3ffffff]
44 /// out2: [0x0 ~> 0x1]
46 pub fn fiat_poly1305_addcarryx_u26(out1
: &mut u32, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_u1
, arg2
: u32, arg3
: u32) -> () {
47 let x1
: u32 = (((arg1
as u32) + arg2
) + arg3
);
48 let x2
: u32 = (x1
& 0x3ffffff);
49 let x3
: fiat_poly1305_u1
= ((x1
>> 26) as fiat_poly1305_u1
);
54 /// The function fiat_poly1305_subborrowx_u26 is a subtraction with borrow.
57 /// out1 = (-arg1 + arg2 + -arg3) mod 2^26
58 /// out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋
61 /// arg1: [0x0 ~> 0x1]
62 /// arg2: [0x0 ~> 0x3ffffff]
63 /// arg3: [0x0 ~> 0x3ffffff]
65 /// out1: [0x0 ~> 0x3ffffff]
66 /// out2: [0x0 ~> 0x1]
68 pub fn fiat_poly1305_subborrowx_u26(out1
: &mut u32, out2
: &mut fiat_poly1305_u1
, arg1
: fiat_poly1305_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_poly1305_i1
= ((x1
>> 26) as fiat_poly1305_i1
);
71 let x3
: u32 = (((x1
as i64) & (0x3ffffff as i64)) as u32);
73 *out2
= (((0x0 as fiat_poly1305_i2
) - (x2
as fiat_poly1305_i2
)) as fiat_poly1305_u1
);
76 /// The function fiat_poly1305_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_poly1305_cmovznz_u32(out1
: &mut u32, arg1
: fiat_poly1305_u1
, arg2
: u32, arg3
: u32) -> () {
89 let x1
: fiat_poly1305_u1
= (!(!arg1
));
90 let x2
: u32 = ((((((0x0 as fiat_poly1305_i2
) - (x1
as fiat_poly1305_i2
)) as fiat_poly1305_i1
) as i64) & (0xffffffff as i64)) as u32);
91 let x3
: u32 = ((x2
& arg3
) | ((!x2
) & arg2
));
95 /// The function fiat_poly1305_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_poly1305_carry_mul(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
, arg2
: &fiat_poly1305_loose_field_element
) -> () {
102 let x1
: u64 = (((arg1
[4]) as u64) * (((arg2
[4]) * 0x5) as u64));
103 let x2
: u64 = (((arg1
[4]) as u64) * (((arg2
[3]) * 0x5) as u64));
104 let x3
: u64 = (((arg1
[4]) as u64) * (((arg2
[2]) * 0x5) as u64));
105 let x4
: u64 = (((arg1
[4]) as u64) * (((arg2
[1]) * 0x5) as u64));
106 let x5
: u64 = (((arg1
[3]) as u64) * (((arg2
[4]) * 0x5) as u64));
107 let x6
: u64 = (((arg1
[3]) as u64) * (((arg2
[3]) * 0x5) as u64));
108 let x7
: u64 = (((arg1
[3]) as u64) * (((arg2
[2]) * 0x5) as u64));
109 let x8
: u64 = (((arg1
[2]) as u64) * (((arg2
[4]) * 0x5) as u64));
110 let x9
: u64 = (((arg1
[2]) as u64) * (((arg2
[3]) * 0x5) as u64));
111 let x10
: u64 = (((arg1
[1]) as u64) * (((arg2
[4]) * 0x5) as u64));
112 let x11
: u64 = (((arg1
[4]) as u64) * ((arg2
[0]) as u64));
113 let x12
: u64 = (((arg1
[3]) as u64) * ((arg2
[1]) as u64));
114 let x13
: u64 = (((arg1
[3]) as u64) * ((arg2
[0]) as u64));
115 let x14
: u64 = (((arg1
[2]) as u64) * ((arg2
[2]) as u64));
116 let x15
: u64 = (((arg1
[2]) as u64) * ((arg2
[1]) as u64));
117 let x16
: u64 = (((arg1
[2]) as u64) * ((arg2
[0]) as u64));
118 let x17
: u64 = (((arg1
[1]) as u64) * ((arg2
[3]) as u64));
119 let x18
: u64 = (((arg1
[1]) as u64) * ((arg2
[2]) as u64));
120 let x19
: u64 = (((arg1
[1]) as u64) * ((arg2
[1]) as u64));
121 let x20
: u64 = (((arg1
[1]) as u64) * ((arg2
[0]) as u64));
122 let x21
: u64 = (((arg1
[0]) as u64) * ((arg2
[4]) as u64));
123 let x22
: u64 = (((arg1
[0]) as u64) * ((arg2
[3]) as u64));
124 let x23
: u64 = (((arg1
[0]) as u64) * ((arg2
[2]) as u64));
125 let x24
: u64 = (((arg1
[0]) as u64) * ((arg2
[1]) as u64));
126 let x25
: u64 = (((arg1
[0]) as u64) * ((arg2
[0]) as u64));
127 let x26
: u64 = (x25
+ (x10
+ (x9
+ (x7
+ x4
))));
128 let x27
: u64 = (x26
>> 26);
129 let x28
: u32 = ((x26
& (0x3ffffff as u64)) as u32);
130 let x29
: u64 = (x21
+ (x17
+ (x14
+ (x12
+ x11
))));
131 let x30
: u64 = (x22
+ (x18
+ (x15
+ (x13
+ x1
))));
132 let x31
: u64 = (x23
+ (x19
+ (x16
+ (x5
+ x2
))));
133 let x32
: u64 = (x24
+ (x20
+ (x8
+ (x6
+ x3
))));
134 let x33
: u64 = (x27
+ x32
);
135 let x34
: u64 = (x33
>> 26);
136 let x35
: u32 = ((x33
& (0x3ffffff as u64)) as u32);
137 let x36
: u64 = (x34
+ x31
);
138 let x37
: u64 = (x36
>> 26);
139 let x38
: u32 = ((x36
& (0x3ffffff as u64)) as u32);
140 let x39
: u64 = (x37
+ x30
);
141 let x40
: u64 = (x39
>> 26);
142 let x41
: u32 = ((x39
& (0x3ffffff as u64)) as u32);
143 let x42
: u64 = (x40
+ x29
);
144 let x43
: u32 = ((x42
>> 26) as u32);
145 let x44
: u32 = ((x42
& (0x3ffffff as u64)) as u32);
146 let x45
: u64 = ((x43
as u64) * (0x5 as u64));
147 let x46
: u64 = ((x28
as u64) + x45
);
148 let x47
: u32 = ((x46
>> 26) as u32);
149 let x48
: u32 = ((x46
& (0x3ffffff as u64)) as u32);
150 let x49
: u32 = (x47
+ x35
);
151 let x50
: fiat_poly1305_u1
= ((x49
>> 26) as fiat_poly1305_u1
);
152 let x51
: u32 = (x49
& 0x3ffffff);
153 let x52
: u32 = ((x50
as u32) + x38
);
161 /// The function fiat_poly1305_carry_square squares a field element and reduces the result.
164 /// eval out1 mod m = (eval arg1 * eval arg1) mod m
167 pub fn fiat_poly1305_carry_square(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
) -> () {
168 let x1
: u32 = ((arg1
[4]) * 0x5);
169 let x2
: u32 = (x1
* 0x2);
170 let x3
: u32 = ((arg1
[4]) * 0x2);
171 let x4
: u32 = ((arg1
[3]) * 0x5);
172 let x5
: u32 = (x4
* 0x2);
173 let x6
: u32 = ((arg1
[3]) * 0x2);
174 let x7
: u32 = ((arg1
[2]) * 0x2);
175 let x8
: u32 = ((arg1
[1]) * 0x2);
176 let x9
: u64 = (((arg1
[4]) as u64) * (x1
as u64));
177 let x10
: u64 = (((arg1
[3]) as u64) * (x2
as u64));
178 let x11
: u64 = (((arg1
[3]) as u64) * (x4
as u64));
179 let x12
: u64 = (((arg1
[2]) as u64) * (x2
as u64));
180 let x13
: u64 = (((arg1
[2]) as u64) * (x5
as u64));
181 let x14
: u64 = (((arg1
[2]) as u64) * ((arg1
[2]) as u64));
182 let x15
: u64 = (((arg1
[1]) as u64) * (x2
as u64));
183 let x16
: u64 = (((arg1
[1]) as u64) * (x6
as u64));
184 let x17
: u64 = (((arg1
[1]) as u64) * (x7
as u64));
185 let x18
: u64 = (((arg1
[1]) as u64) * ((arg1
[1]) as u64));
186 let x19
: u64 = (((arg1
[0]) as u64) * (x3
as u64));
187 let x20
: u64 = (((arg1
[0]) as u64) * (x6
as u64));
188 let x21
: u64 = (((arg1
[0]) as u64) * (x7
as u64));
189 let x22
: u64 = (((arg1
[0]) as u64) * (x8
as u64));
190 let x23
: u64 = (((arg1
[0]) as u64) * ((arg1
[0]) as u64));
191 let x24
: u64 = (x23
+ (x15
+ x13
));
192 let x25
: u64 = (x24
>> 26);
193 let x26
: u32 = ((x24
& (0x3ffffff as u64)) as u32);
194 let x27
: u64 = (x19
+ (x16
+ x14
));
195 let x28
: u64 = (x20
+ (x17
+ x9
));
196 let x29
: u64 = (x21
+ (x18
+ x10
));
197 let x30
: u64 = (x22
+ (x12
+ x11
));
198 let x31
: u64 = (x25
+ x30
);
199 let x32
: u64 = (x31
>> 26);
200 let x33
: u32 = ((x31
& (0x3ffffff as u64)) as u32);
201 let x34
: u64 = (x32
+ x29
);
202 let x35
: u64 = (x34
>> 26);
203 let x36
: u32 = ((x34
& (0x3ffffff as u64)) as u32);
204 let x37
: u64 = (x35
+ x28
);
205 let x38
: u64 = (x37
>> 26);
206 let x39
: u32 = ((x37
& (0x3ffffff as u64)) as u32);
207 let x40
: u64 = (x38
+ x27
);
208 let x41
: u32 = ((x40
>> 26) as u32);
209 let x42
: u32 = ((x40
& (0x3ffffff as u64)) as u32);
210 let x43
: u64 = ((x41
as u64) * (0x5 as u64));
211 let x44
: u64 = ((x26
as u64) + x43
);
212 let x45
: u32 = ((x44
>> 26) as u32);
213 let x46
: u32 = ((x44
& (0x3ffffff as u64)) as u32);
214 let x47
: u32 = (x45
+ x33
);
215 let x48
: fiat_poly1305_u1
= ((x47
>> 26) as fiat_poly1305_u1
);
216 let x49
: u32 = (x47
& 0x3ffffff);
217 let x50
: u32 = ((x48
as u32) + x36
);
225 /// The function fiat_poly1305_carry reduces a field element.
228 /// eval out1 mod m = eval arg1 mod m
231 pub fn fiat_poly1305_carry(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &fiat_poly1305_loose_field_element
) -> () {
232 let x1
: u32 = (arg1
[0]);
233 let x2
: u32 = ((x1
>> 26) + (arg1
[1]));
234 let x3
: u32 = ((x2
>> 26) + (arg1
[2]));
235 let x4
: u32 = ((x3
>> 26) + (arg1
[3]));
236 let x5
: u32 = ((x4
>> 26) + (arg1
[4]));
237 let x6
: u32 = ((x1
& 0x3ffffff) + ((x5
>> 26) * 0x5));
238 let x7
: u32 = ((((x6
>> 26) as fiat_poly1305_u1
) as u32) + (x2
& 0x3ffffff));
239 let x8
: u32 = (x6
& 0x3ffffff);
240 let x9
: u32 = (x7
& 0x3ffffff);
241 let x10
: u32 = ((((x7
>> 26) as fiat_poly1305_u1
) as u32) + (x3
& 0x3ffffff));
242 let x11
: u32 = (x4
& 0x3ffffff);
243 let x12
: u32 = (x5
& 0x3ffffff);
251 /// The function fiat_poly1305_add adds two field elements.
254 /// eval out1 mod m = (eval arg1 + eval arg2) mod m
257 pub fn fiat_poly1305_add(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
, arg2
: &fiat_poly1305_tight_field_element
) -> () {
258 let x1
: u32 = ((arg1
[0]) + (arg2
[0]));
259 let x2
: u32 = ((arg1
[1]) + (arg2
[1]));
260 let x3
: u32 = ((arg1
[2]) + (arg2
[2]));
261 let x4
: u32 = ((arg1
[3]) + (arg2
[3]));
262 let x5
: u32 = ((arg1
[4]) + (arg2
[4]));
270 /// The function fiat_poly1305_sub subtracts two field elements.
273 /// eval out1 mod m = (eval arg1 - eval arg2) mod m
276 pub fn fiat_poly1305_sub(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
, arg2
: &fiat_poly1305_tight_field_element
) -> () {
277 let x1
: u32 = ((0x7fffff6 + (arg1
[0])) - (arg2
[0]));
278 let x2
: u32 = ((0x7fffffe + (arg1
[1])) - (arg2
[1]));
279 let x3
: u32 = ((0x7fffffe + (arg1
[2])) - (arg2
[2]));
280 let x4
: u32 = ((0x7fffffe + (arg1
[3])) - (arg2
[3]));
281 let x5
: u32 = ((0x7fffffe + (arg1
[4])) - (arg2
[4]));
289 /// The function fiat_poly1305_opp negates a field element.
292 /// eval out1 mod m = -eval arg1 mod m
295 pub fn fiat_poly1305_opp(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
) -> () {
296 let x1
: u32 = (0x7fffff6 - (arg1
[0]));
297 let x2
: u32 = (0x7fffffe - (arg1
[1]));
298 let x3
: u32 = (0x7fffffe - (arg1
[2]));
299 let x4
: u32 = (0x7fffffe - (arg1
[3]));
300 let x5
: u32 = (0x7fffffe - (arg1
[4]));
308 /// The function fiat_poly1305_selectznz is a multi-limb conditional select.
311 /// out1 = (if arg1 = 0 then arg2 else arg3)
314 /// arg1: [0x0 ~> 0x1]
315 /// arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
316 /// arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
318 /// out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
320 pub fn fiat_poly1305_selectznz(out1
: &mut [u32; 5], arg1
: fiat_poly1305_u1
, arg2
: &[u32; 5], arg3
: &[u32; 5]) -> () {
322 fiat_poly1305_cmovznz_u32(&mut x1
, arg1
, (arg2
[0]), (arg3
[0]));
324 fiat_poly1305_cmovznz_u32(&mut x2
, arg1
, (arg2
[1]), (arg3
[1]));
326 fiat_poly1305_cmovznz_u32(&mut x3
, arg1
, (arg2
[2]), (arg3
[2]));
328 fiat_poly1305_cmovznz_u32(&mut x4
, arg1
, (arg2
[3]), (arg3
[3]));
330 fiat_poly1305_cmovznz_u32(&mut x5
, arg1
, (arg2
[4]), (arg3
[4]));
338 /// The function fiat_poly1305_to_bytes serializes a field element to bytes in little-endian order.
341 /// out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..16]
344 /// 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]]
346 pub fn fiat_poly1305_to_bytes(out1
: &mut [u8; 17], arg1
: &fiat_poly1305_tight_field_element
) -> () {
348 let mut x2
: fiat_poly1305_u1
= 0;
349 fiat_poly1305_subborrowx_u26(&mut x1
, &mut x2
, 0x0, (arg1
[0]), 0x3fffffb);
351 let mut x4
: fiat_poly1305_u1
= 0;
352 fiat_poly1305_subborrowx_u26(&mut x3
, &mut x4
, x2
, (arg1
[1]), 0x3ffffff);
354 let mut x6
: fiat_poly1305_u1
= 0;
355 fiat_poly1305_subborrowx_u26(&mut x5
, &mut x6
, x4
, (arg1
[2]), 0x3ffffff);
357 let mut x8
: fiat_poly1305_u1
= 0;
358 fiat_poly1305_subborrowx_u26(&mut x7
, &mut x8
, x6
, (arg1
[3]), 0x3ffffff);
360 let mut x10
: fiat_poly1305_u1
= 0;
361 fiat_poly1305_subborrowx_u26(&mut x9
, &mut x10
, x8
, (arg1
[4]), 0x3ffffff);
362 let mut x11
: u32 = 0;
363 fiat_poly1305_cmovznz_u32(&mut x11
, x10
, (0x0 as u32), 0xffffffff);
364 let mut x12
: u32 = 0;
365 let mut x13
: fiat_poly1305_u1
= 0;
366 fiat_poly1305_addcarryx_u26(&mut x12
, &mut x13
, 0x0, x1
, (x11
& 0x3fffffb));
367 let mut x14
: u32 = 0;
368 let mut x15
: fiat_poly1305_u1
= 0;
369 fiat_poly1305_addcarryx_u26(&mut x14
, &mut x15
, x13
, x3
, (x11
& 0x3ffffff));
370 let mut x16
: u32 = 0;
371 let mut x17
: fiat_poly1305_u1
= 0;
372 fiat_poly1305_addcarryx_u26(&mut x16
, &mut x17
, x15
, x5
, (x11
& 0x3ffffff));
373 let mut x18
: u32 = 0;
374 let mut x19
: fiat_poly1305_u1
= 0;
375 fiat_poly1305_addcarryx_u26(&mut x18
, &mut x19
, x17
, x7
, (x11
& 0x3ffffff));
376 let mut x20
: u32 = 0;
377 let mut x21
: fiat_poly1305_u1
= 0;
378 fiat_poly1305_addcarryx_u26(&mut x20
, &mut x21
, x19
, x9
, (x11
& 0x3ffffff));
379 let x22
: u32 = (x18
<< 6);
380 let x23
: u32 = (x16
<< 4);
381 let x24
: u32 = (x14
<< 2);
382 let x25
: u8 = ((x12
& (0xff as u32)) as u8);
383 let x26
: u32 = (x12
>> 8);
384 let x27
: u8 = ((x26
& (0xff as u32)) as u8);
385 let x28
: u32 = (x26
>> 8);
386 let x29
: u8 = ((x28
& (0xff as u32)) as u8);
387 let x30
: u8 = ((x28
>> 8) as u8);
388 let x31
: u32 = (x24
+ (x30
as u32));
389 let x32
: u8 = ((x31
& (0xff as u32)) as u8);
390 let x33
: u32 = (x31
>> 8);
391 let x34
: u8 = ((x33
& (0xff as u32)) as u8);
392 let x35
: u32 = (x33
>> 8);
393 let x36
: u8 = ((x35
& (0xff as u32)) as u8);
394 let x37
: u8 = ((x35
>> 8) as u8);
395 let x38
: u32 = (x23
+ (x37
as u32));
396 let x39
: u8 = ((x38
& (0xff as u32)) as u8);
397 let x40
: u32 = (x38
>> 8);
398 let x41
: u8 = ((x40
& (0xff as u32)) as u8);
399 let x42
: u32 = (x40
>> 8);
400 let x43
: u8 = ((x42
& (0xff as u32)) as u8);
401 let x44
: u8 = ((x42
>> 8) as u8);
402 let x45
: u32 = (x22
+ (x44
as u32));
403 let x46
: u8 = ((x45
& (0xff as u32)) as u8);
404 let x47
: u32 = (x45
>> 8);
405 let x48
: u8 = ((x47
& (0xff as u32)) as u8);
406 let x49
: u32 = (x47
>> 8);
407 let x50
: u8 = ((x49
& (0xff as u32)) as u8);
408 let x51
: u8 = ((x49
>> 8) as u8);
409 let x52
: u8 = ((x20
& (0xff as u32)) as u8);
410 let x53
: u32 = (x20
>> 8);
411 let x54
: u8 = ((x53
& (0xff as u32)) as u8);
412 let x55
: u32 = (x53
>> 8);
413 let x56
: u8 = ((x55
& (0xff as u32)) as u8);
414 let x57
: u8 = ((x55
>> 8) as u8);
434 /// The function fiat_poly1305_from_bytes deserializes a field element from bytes in little-endian order.
437 /// eval out1 mod m = bytes_eval arg1 mod m
440 /// 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]]
442 pub fn fiat_poly1305_from_bytes(out1
: &mut fiat_poly1305_tight_field_element
, arg1
: &[u8; 17]) -> () {
443 let x1
: u32 = (((arg1
[16]) as u32) << 24);
444 let x2
: u32 = (((arg1
[15]) as u32) << 16);
445 let x3
: u32 = (((arg1
[14]) as u32) << 8);
446 let x4
: u8 = (arg1
[13]);
447 let x5
: u32 = (((arg1
[12]) as u32) << 18);
448 let x6
: u32 = (((arg1
[11]) as u32) << 10);
449 let x7
: u32 = (((arg1
[10]) as u32) << 2);
450 let x8
: u32 = (((arg1
[9]) as u32) << 20);
451 let x9
: u32 = (((arg1
[8]) as u32) << 12);
452 let x10
: u32 = (((arg1
[7]) as u32) << 4);
453 let x11
: u32 = (((arg1
[6]) as u32) << 22);
454 let x12
: u32 = (((arg1
[5]) as u32) << 14);
455 let x13
: u32 = (((arg1
[4]) as u32) << 6);
456 let x14
: u32 = (((arg1
[3]) as u32) << 24);
457 let x15
: u32 = (((arg1
[2]) as u32) << 16);
458 let x16
: u32 = (((arg1
[1]) as u32) << 8);
459 let x17
: u8 = (arg1
[0]);
460 let x18
: u32 = (x16
+ (x17
as u32));
461 let x19
: u32 = (x15
+ x18
);
462 let x20
: u32 = (x14
+ x19
);
463 let x21
: u32 = (x20
& 0x3ffffff);
464 let x22
: u8 = ((x20
>> 26) as u8);
465 let x23
: u32 = (x13
+ (x22
as u32));
466 let x24
: u32 = (x12
+ x23
);
467 let x25
: u32 = (x11
+ x24
);
468 let x26
: u32 = (x25
& 0x3ffffff);
469 let x27
: u8 = ((x25
>> 26) as u8);
470 let x28
: u32 = (x10
+ (x27
as u32));
471 let x29
: u32 = (x9
+ x28
);
472 let x30
: u32 = (x8
+ x29
);
473 let x31
: u32 = (x30
& 0x3ffffff);
474 let x32
: u8 = ((x30
>> 26) as u8);
475 let x33
: u32 = (x7
+ (x32
as u32));
476 let x34
: u32 = (x6
+ x33
);
477 let x35
: u32 = (x5
+ x34
);
478 let x36
: u32 = (x3
+ (x4
as u32));
479 let x37
: u32 = (x2
+ x36
);
480 let x38
: u32 = (x1
+ x37
);
488 /// The function fiat_poly1305_relax is the identity function converting from tight field elements to loose field elements.
494 pub fn fiat_poly1305_relax(out1
: &mut fiat_poly1305_loose_field_element
, arg1
: &fiat_poly1305_tight_field_element
) -> () {
495 let x1
: u32 = (arg1
[0]);
496 let x2
: u32 = (arg1
[1]);
497 let x3
: u32 = (arg1
[2]);
498 let x4
: u32 = (arg1
[3]);
499 let x5
: u32 = (arg1
[4]);