fiat_crypto/
poly1305_32.rs

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 "")
8//!
9//! Computed values:
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]
14
15#![allow(unused_parens)]
16#![allow(non_camel_case_types)]
17
18/// Since `Index` and `IndexMut` aren't callable in `const` contexts yet, this helper type helps unify
19/// arrays and user-defined array-wrapper types into a single type which can be indexed in `const`
20/// contexts. Once `const trait`s are stabilized this type can go away
21struct IndexConst<T: ?Sized>(T);
22
23impl<'a, T, const N: usize> IndexConst<&'a [T; N]> {
24    #[inline(always)]
25    #[allow(unused)]
26    const fn index(self, i: usize) -> &'a T {
27        &self.0[i]
28    }
29}
30impl<'a, 'b, T, const N: usize> IndexConst<&'a mut &'b mut [T; N]> {
31    #[inline(always)]
32    #[allow(unused)]
33    const fn index_mut(self, i: usize) -> &'a mut T {
34        &mut self.0[i]
35    }
36}
37
38/** fiat_poly1305_u1 represents values of 1 bits, stored in one byte. */
39pub type fiat_poly1305_u1 = u8;
40/** fiat_poly1305_i1 represents values of 1 bits, stored in one byte. */
41pub type fiat_poly1305_i1 = i8;
42/** fiat_poly1305_u2 represents values of 2 bits, stored in one byte. */
43pub type fiat_poly1305_u2 = u8;
44/** fiat_poly1305_i2 represents values of 2 bits, stored in one byte. */
45pub type fiat_poly1305_i2 = i8;
46
47/** The type fiat_poly1305_loose_field_element is a field element with loose bounds. */
48/** Bounds: [[0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000], [0x0 ~> 0xc000000]] */
49#[derive(Clone, Copy)]
50pub struct fiat_poly1305_loose_field_element(pub [u32; 5]);
51
52impl core::ops::Index<usize> for fiat_poly1305_loose_field_element {
53    type Output = u32;
54    #[inline]
55    fn index(&self, index: usize) -> &Self::Output {
56        &self.0[index]
57    }
58}
59
60impl core::ops::IndexMut<usize> for fiat_poly1305_loose_field_element {
61    #[inline]
62    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
63        &mut self.0[index]
64    }
65}
66
67impl<'a> IndexConst<&'a fiat_poly1305_loose_field_element> {
68    #[allow(unused)]
69    #[inline(always)]
70    const fn index(self, i: usize) -> &'a u32 {
71        &self.0.0[i]
72    }
73}
74
75impl<'a, 'b> IndexConst<&'a mut &'b mut fiat_poly1305_loose_field_element> {
76    #[allow(unused)]
77    #[inline(always)]
78    const fn index_mut(self, i: usize) -> &'a mut u32 {
79        &mut self.0.0[i]
80    }
81}
82
83/** The type fiat_poly1305_tight_field_element is a field element with tight bounds. */
84/** Bounds: [[0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000], [0x0 ~> 0x4000000]] */
85#[derive(Clone, Copy)]
86pub struct fiat_poly1305_tight_field_element(pub [u32; 5]);
87
88impl core::ops::Index<usize> for fiat_poly1305_tight_field_element {
89    type Output = u32;
90    #[inline]
91    fn index(&self, index: usize) -> &Self::Output {
92        &self.0[index]
93    }
94}
95
96impl core::ops::IndexMut<usize> for fiat_poly1305_tight_field_element {
97    #[inline]
98    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
99        &mut self.0[index]
100    }
101}
102
103impl<'a> IndexConst<&'a fiat_poly1305_tight_field_element> {
104    #[allow(unused)]
105    #[inline(always)]
106    const fn index(self, i: usize) -> &'a u32 {
107        &self.0.0[i]
108    }
109}
110
111impl<'a, 'b> IndexConst<&'a mut &'b mut fiat_poly1305_tight_field_element> {
112    #[allow(unused)]
113    #[inline(always)]
114    const fn index_mut(self, i: usize) -> &'a mut u32 {
115        &mut self.0.0[i]
116    }
117}
118
119
120/// The function fiat_poly1305_addcarryx_u26 is an addition with carry.
121///
122/// Postconditions:
123///   out1 = (arg1 + arg2 + arg3) mod 2^26
124///   out2 = ⌊(arg1 + arg2 + arg3) / 2^26⌋
125///
126/// Input Bounds:
127///   arg1: [0x0 ~> 0x1]
128///   arg2: [0x0 ~> 0x3ffffff]
129///   arg3: [0x0 ~> 0x3ffffff]
130/// Output Bounds:
131///   out1: [0x0 ~> 0x3ffffff]
132///   out2: [0x0 ~> 0x1]
133#[inline]
134pub const fn fiat_poly1305_addcarryx_u26(out1: &mut u32, out2: &mut fiat_poly1305_u1, arg1: fiat_poly1305_u1, arg2: u32, arg3: u32) {
135  let x1: u32 = (((arg1 as u32) + arg2) + arg3);
136  let x2: u32 = (x1 & 0x3ffffff);
137  let x3: fiat_poly1305_u1 = ((x1 >> 26) as fiat_poly1305_u1);
138  *out1 = x2;
139  *out2 = x3;
140}
141
142/// The function fiat_poly1305_subborrowx_u26 is a subtraction with borrow.
143///
144/// Postconditions:
145///   out1 = (-arg1 + arg2 + -arg3) mod 2^26
146///   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^26⌋
147///
148/// Input Bounds:
149///   arg1: [0x0 ~> 0x1]
150///   arg2: [0x0 ~> 0x3ffffff]
151///   arg3: [0x0 ~> 0x3ffffff]
152/// Output Bounds:
153///   out1: [0x0 ~> 0x3ffffff]
154///   out2: [0x0 ~> 0x1]
155#[inline]
156pub const fn fiat_poly1305_subborrowx_u26(out1: &mut u32, out2: &mut fiat_poly1305_u1, arg1: fiat_poly1305_u1, arg2: u32, arg3: u32) {
157  let x1: i32 = ((((((arg2 as i64) - (arg1 as i64)) as i32) as i64) - (arg3 as i64)) as i32);
158  let x2: fiat_poly1305_i1 = ((x1 >> 26) as fiat_poly1305_i1);
159  let x3: u32 = (((x1 as i64) & (0x3ffffff as i64)) as u32);
160  *out1 = x3;
161  *out2 = (((0x0 as fiat_poly1305_i2) - (x2 as fiat_poly1305_i2)) as fiat_poly1305_u1);
162}
163
164/// The function fiat_poly1305_cmovznz_u32 is a single-word conditional move.
165///
166/// Postconditions:
167///   out1 = (if arg1 = 0 then arg2 else arg3)
168///
169/// Input Bounds:
170///   arg1: [0x0 ~> 0x1]
171///   arg2: [0x0 ~> 0xffffffff]
172///   arg3: [0x0 ~> 0xffffffff]
173/// Output Bounds:
174///   out1: [0x0 ~> 0xffffffff]
175#[inline]
176pub const fn fiat_poly1305_cmovznz_u32(out1: &mut u32, arg1: fiat_poly1305_u1, arg2: u32, arg3: u32) {
177  let x1: fiat_poly1305_u1 = (!(!arg1));
178  let x2: u32 = ((((((0x0 as fiat_poly1305_i2) - (x1 as fiat_poly1305_i2)) as fiat_poly1305_i1) as i64) & (0xffffffff as i64)) as u32);
179  let x3: u32 = ((x2 & arg3) | ((!x2) & arg2));
180  *out1 = x3;
181}
182
183/// The function fiat_poly1305_carry_mul multiplies two field elements and reduces the result.
184///
185/// Postconditions:
186///   eval out1 mod m = (eval arg1 * eval arg2) mod m
187///
188#[inline]
189pub const fn fiat_poly1305_carry_mul(mut out1: &mut fiat_poly1305_tight_field_element, arg1: &fiat_poly1305_loose_field_element, arg2: &fiat_poly1305_loose_field_element) {
190  let x1: u64 = (((*IndexConst(arg1).index(4)) as u64) * (((*IndexConst(arg2).index(4)) * 0x5) as u64));
191  let x2: u64 = (((*IndexConst(arg1).index(4)) as u64) * (((*IndexConst(arg2).index(3)) * 0x5) as u64));
192  let x3: u64 = (((*IndexConst(arg1).index(4)) as u64) * (((*IndexConst(arg2).index(2)) * 0x5) as u64));
193  let x4: u64 = (((*IndexConst(arg1).index(4)) as u64) * (((*IndexConst(arg2).index(1)) * 0x5) as u64));
194  let x5: u64 = (((*IndexConst(arg1).index(3)) as u64) * (((*IndexConst(arg2).index(4)) * 0x5) as u64));
195  let x6: u64 = (((*IndexConst(arg1).index(3)) as u64) * (((*IndexConst(arg2).index(3)) * 0x5) as u64));
196  let x7: u64 = (((*IndexConst(arg1).index(3)) as u64) * (((*IndexConst(arg2).index(2)) * 0x5) as u64));
197  let x8: u64 = (((*IndexConst(arg1).index(2)) as u64) * (((*IndexConst(arg2).index(4)) * 0x5) as u64));
198  let x9: u64 = (((*IndexConst(arg1).index(2)) as u64) * (((*IndexConst(arg2).index(3)) * 0x5) as u64));
199  let x10: u64 = (((*IndexConst(arg1).index(1)) as u64) * (((*IndexConst(arg2).index(4)) * 0x5) as u64));
200  let x11: u64 = (((*IndexConst(arg1).index(4)) as u64) * ((*IndexConst(arg2).index(0)) as u64));
201  let x12: u64 = (((*IndexConst(arg1).index(3)) as u64) * ((*IndexConst(arg2).index(1)) as u64));
202  let x13: u64 = (((*IndexConst(arg1).index(3)) as u64) * ((*IndexConst(arg2).index(0)) as u64));
203  let x14: u64 = (((*IndexConst(arg1).index(2)) as u64) * ((*IndexConst(arg2).index(2)) as u64));
204  let x15: u64 = (((*IndexConst(arg1).index(2)) as u64) * ((*IndexConst(arg2).index(1)) as u64));
205  let x16: u64 = (((*IndexConst(arg1).index(2)) as u64) * ((*IndexConst(arg2).index(0)) as u64));
206  let x17: u64 = (((*IndexConst(arg1).index(1)) as u64) * ((*IndexConst(arg2).index(3)) as u64));
207  let x18: u64 = (((*IndexConst(arg1).index(1)) as u64) * ((*IndexConst(arg2).index(2)) as u64));
208  let x19: u64 = (((*IndexConst(arg1).index(1)) as u64) * ((*IndexConst(arg2).index(1)) as u64));
209  let x20: u64 = (((*IndexConst(arg1).index(1)) as u64) * ((*IndexConst(arg2).index(0)) as u64));
210  let x21: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg2).index(4)) as u64));
211  let x22: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg2).index(3)) as u64));
212  let x23: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg2).index(2)) as u64));
213  let x24: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg2).index(1)) as u64));
214  let x25: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg2).index(0)) as u64));
215  let x26: u64 = (x25 + (x10 + (x9 + (x7 + x4))));
216  let x27: u64 = (x26 >> 26);
217  let x28: u32 = ((x26 & (0x3ffffff as u64)) as u32);
218  let x29: u64 = (x21 + (x17 + (x14 + (x12 + x11))));
219  let x30: u64 = (x22 + (x18 + (x15 + (x13 + x1))));
220  let x31: u64 = (x23 + (x19 + (x16 + (x5 + x2))));
221  let x32: u64 = (x24 + (x20 + (x8 + (x6 + x3))));
222  let x33: u64 = (x27 + x32);
223  let x34: u64 = (x33 >> 26);
224  let x35: u32 = ((x33 & (0x3ffffff as u64)) as u32);
225  let x36: u64 = (x34 + x31);
226  let x37: u64 = (x36 >> 26);
227  let x38: u32 = ((x36 & (0x3ffffff as u64)) as u32);
228  let x39: u64 = (x37 + x30);
229  let x40: u64 = (x39 >> 26);
230  let x41: u32 = ((x39 & (0x3ffffff as u64)) as u32);
231  let x42: u64 = (x40 + x29);
232  let x43: u32 = ((x42 >> 26) as u32);
233  let x44: u32 = ((x42 & (0x3ffffff as u64)) as u32);
234  let x45: u64 = ((x43 as u64) * (0x5 as u64));
235  let x46: u64 = ((x28 as u64) + x45);
236  let x47: u32 = ((x46 >> 26) as u32);
237  let x48: u32 = ((x46 & (0x3ffffff as u64)) as u32);
238  let x49: u32 = (x47 + x35);
239  let x50: fiat_poly1305_u1 = ((x49 >> 26) as fiat_poly1305_u1);
240  let x51: u32 = (x49 & 0x3ffffff);
241  let x52: u32 = ((x50 as u32) + x38);
242  *IndexConst(&mut out1).index_mut(0) = x48;
243  *IndexConst(&mut out1).index_mut(1) = x51;
244  *IndexConst(&mut out1).index_mut(2) = x52;
245  *IndexConst(&mut out1).index_mut(3) = x41;
246  *IndexConst(&mut out1).index_mut(4) = x44;
247}
248
249/// The function fiat_poly1305_carry_square squares a field element and reduces the result.
250///
251/// Postconditions:
252///   eval out1 mod m = (eval arg1 * eval arg1) mod m
253///
254#[inline]
255pub const fn fiat_poly1305_carry_square(mut out1: &mut fiat_poly1305_tight_field_element, arg1: &fiat_poly1305_loose_field_element) {
256  let x1: u32 = ((*IndexConst(arg1).index(4)) * 0x5);
257  let x2: u32 = (x1 * 0x2);
258  let x3: u32 = ((*IndexConst(arg1).index(4)) * 0x2);
259  let x4: u32 = ((*IndexConst(arg1).index(3)) * 0x5);
260  let x5: u32 = (x4 * 0x2);
261  let x6: u32 = ((*IndexConst(arg1).index(3)) * 0x2);
262  let x7: u32 = ((*IndexConst(arg1).index(2)) * 0x2);
263  let x8: u32 = ((*IndexConst(arg1).index(1)) * 0x2);
264  let x9: u64 = (((*IndexConst(arg1).index(4)) as u64) * (x1 as u64));
265  let x10: u64 = (((*IndexConst(arg1).index(3)) as u64) * (x2 as u64));
266  let x11: u64 = (((*IndexConst(arg1).index(3)) as u64) * (x4 as u64));
267  let x12: u64 = (((*IndexConst(arg1).index(2)) as u64) * (x2 as u64));
268  let x13: u64 = (((*IndexConst(arg1).index(2)) as u64) * (x5 as u64));
269  let x14: u64 = (((*IndexConst(arg1).index(2)) as u64) * ((*IndexConst(arg1).index(2)) as u64));
270  let x15: u64 = (((*IndexConst(arg1).index(1)) as u64) * (x2 as u64));
271  let x16: u64 = (((*IndexConst(arg1).index(1)) as u64) * (x6 as u64));
272  let x17: u64 = (((*IndexConst(arg1).index(1)) as u64) * (x7 as u64));
273  let x18: u64 = (((*IndexConst(arg1).index(1)) as u64) * ((*IndexConst(arg1).index(1)) as u64));
274  let x19: u64 = (((*IndexConst(arg1).index(0)) as u64) * (x3 as u64));
275  let x20: u64 = (((*IndexConst(arg1).index(0)) as u64) * (x6 as u64));
276  let x21: u64 = (((*IndexConst(arg1).index(0)) as u64) * (x7 as u64));
277  let x22: u64 = (((*IndexConst(arg1).index(0)) as u64) * (x8 as u64));
278  let x23: u64 = (((*IndexConst(arg1).index(0)) as u64) * ((*IndexConst(arg1).index(0)) as u64));
279  let x24: u64 = (x23 + (x15 + x13));
280  let x25: u64 = (x24 >> 26);
281  let x26: u32 = ((x24 & (0x3ffffff as u64)) as u32);
282  let x27: u64 = (x19 + (x16 + x14));
283  let x28: u64 = (x20 + (x17 + x9));
284  let x29: u64 = (x21 + (x18 + x10));
285  let x30: u64 = (x22 + (x12 + x11));
286  let x31: u64 = (x25 + x30);
287  let x32: u64 = (x31 >> 26);
288  let x33: u32 = ((x31 & (0x3ffffff as u64)) as u32);
289  let x34: u64 = (x32 + x29);
290  let x35: u64 = (x34 >> 26);
291  let x36: u32 = ((x34 & (0x3ffffff as u64)) as u32);
292  let x37: u64 = (x35 + x28);
293  let x38: u64 = (x37 >> 26);
294  let x39: u32 = ((x37 & (0x3ffffff as u64)) as u32);
295  let x40: u64 = (x38 + x27);
296  let x41: u32 = ((x40 >> 26) as u32);
297  let x42: u32 = ((x40 & (0x3ffffff as u64)) as u32);
298  let x43: u64 = ((x41 as u64) * (0x5 as u64));
299  let x44: u64 = ((x26 as u64) + x43);
300  let x45: u32 = ((x44 >> 26) as u32);
301  let x46: u32 = ((x44 & (0x3ffffff as u64)) as u32);
302  let x47: u32 = (x45 + x33);
303  let x48: fiat_poly1305_u1 = ((x47 >> 26) as fiat_poly1305_u1);
304  let x49: u32 = (x47 & 0x3ffffff);
305  let x50: u32 = ((x48 as u32) + x36);
306  *IndexConst(&mut out1).index_mut(0) = x46;
307  *IndexConst(&mut out1).index_mut(1) = x49;
308  *IndexConst(&mut out1).index_mut(2) = x50;
309  *IndexConst(&mut out1).index_mut(3) = x39;
310  *IndexConst(&mut out1).index_mut(4) = x42;
311}
312
313/// The function fiat_poly1305_carry reduces a field element.
314///
315/// Postconditions:
316///   eval out1 mod m = eval arg1 mod m
317///
318#[inline]
319pub const fn fiat_poly1305_carry(mut out1: &mut fiat_poly1305_tight_field_element, arg1: &fiat_poly1305_loose_field_element) {
320  let x1: u32 = (*IndexConst(arg1).index(0));
321  let x2: u32 = ((x1 >> 26) + (*IndexConst(arg1).index(1)));
322  let x3: u32 = ((x2 >> 26) + (*IndexConst(arg1).index(2)));
323  let x4: u32 = ((x3 >> 26) + (*IndexConst(arg1).index(3)));
324  let x5: u32 = ((x4 >> 26) + (*IndexConst(arg1).index(4)));
325  let x6: u32 = ((x1 & 0x3ffffff) + ((x5 >> 26) * 0x5));
326  let x7: u32 = ((((x6 >> 26) as fiat_poly1305_u1) as u32) + (x2 & 0x3ffffff));
327  let x8: u32 = (x6 & 0x3ffffff);
328  let x9: u32 = (x7 & 0x3ffffff);
329  let x10: u32 = ((((x7 >> 26) as fiat_poly1305_u1) as u32) + (x3 & 0x3ffffff));
330  let x11: u32 = (x4 & 0x3ffffff);
331  let x12: u32 = (x5 & 0x3ffffff);
332  *IndexConst(&mut out1).index_mut(0) = x8;
333  *IndexConst(&mut out1).index_mut(1) = x9;
334  *IndexConst(&mut out1).index_mut(2) = x10;
335  *IndexConst(&mut out1).index_mut(3) = x11;
336  *IndexConst(&mut out1).index_mut(4) = x12;
337}
338
339/// The function fiat_poly1305_add adds two field elements.
340///
341/// Postconditions:
342///   eval out1 mod m = (eval arg1 + eval arg2) mod m
343///
344#[inline]
345pub const fn fiat_poly1305_add(mut out1: &mut fiat_poly1305_loose_field_element, arg1: &fiat_poly1305_tight_field_element, arg2: &fiat_poly1305_tight_field_element) {
346  let x1: u32 = ((*IndexConst(arg1).index(0)) + (*IndexConst(arg2).index(0)));
347  let x2: u32 = ((*IndexConst(arg1).index(1)) + (*IndexConst(arg2).index(1)));
348  let x3: u32 = ((*IndexConst(arg1).index(2)) + (*IndexConst(arg2).index(2)));
349  let x4: u32 = ((*IndexConst(arg1).index(3)) + (*IndexConst(arg2).index(3)));
350  let x5: u32 = ((*IndexConst(arg1).index(4)) + (*IndexConst(arg2).index(4)));
351  *IndexConst(&mut out1).index_mut(0) = x1;
352  *IndexConst(&mut out1).index_mut(1) = x2;
353  *IndexConst(&mut out1).index_mut(2) = x3;
354  *IndexConst(&mut out1).index_mut(3) = x4;
355  *IndexConst(&mut out1).index_mut(4) = x5;
356}
357
358/// The function fiat_poly1305_sub subtracts two field elements.
359///
360/// Postconditions:
361///   eval out1 mod m = (eval arg1 - eval arg2) mod m
362///
363#[inline]
364pub const fn fiat_poly1305_sub(mut out1: &mut fiat_poly1305_loose_field_element, arg1: &fiat_poly1305_tight_field_element, arg2: &fiat_poly1305_tight_field_element) {
365  let x1: u32 = ((0x7fffff6 + (*IndexConst(arg1).index(0))) - (*IndexConst(arg2).index(0)));
366  let x2: u32 = ((0x7fffffe + (*IndexConst(arg1).index(1))) - (*IndexConst(arg2).index(1)));
367  let x3: u32 = ((0x7fffffe + (*IndexConst(arg1).index(2))) - (*IndexConst(arg2).index(2)));
368  let x4: u32 = ((0x7fffffe + (*IndexConst(arg1).index(3))) - (*IndexConst(arg2).index(3)));
369  let x5: u32 = ((0x7fffffe + (*IndexConst(arg1).index(4))) - (*IndexConst(arg2).index(4)));
370  *IndexConst(&mut out1).index_mut(0) = x1;
371  *IndexConst(&mut out1).index_mut(1) = x2;
372  *IndexConst(&mut out1).index_mut(2) = x3;
373  *IndexConst(&mut out1).index_mut(3) = x4;
374  *IndexConst(&mut out1).index_mut(4) = x5;
375}
376
377/// The function fiat_poly1305_opp negates a field element.
378///
379/// Postconditions:
380///   eval out1 mod m = -eval arg1 mod m
381///
382#[inline]
383pub const fn fiat_poly1305_opp(mut out1: &mut fiat_poly1305_loose_field_element, arg1: &fiat_poly1305_tight_field_element) {
384  let x1: u32 = (0x7fffff6 - (*IndexConst(arg1).index(0)));
385  let x2: u32 = (0x7fffffe - (*IndexConst(arg1).index(1)));
386  let x3: u32 = (0x7fffffe - (*IndexConst(arg1).index(2)));
387  let x4: u32 = (0x7fffffe - (*IndexConst(arg1).index(3)));
388  let x5: u32 = (0x7fffffe - (*IndexConst(arg1).index(4)));
389  *IndexConst(&mut out1).index_mut(0) = x1;
390  *IndexConst(&mut out1).index_mut(1) = x2;
391  *IndexConst(&mut out1).index_mut(2) = x3;
392  *IndexConst(&mut out1).index_mut(3) = x4;
393  *IndexConst(&mut out1).index_mut(4) = x5;
394}
395
396/// The function fiat_poly1305_selectznz is a multi-limb conditional select.
397///
398/// Postconditions:
399///   out1 = (if arg1 = 0 then arg2 else arg3)
400///
401/// Input Bounds:
402///   arg1: [0x0 ~> 0x1]
403///   arg2: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
404///   arg3: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
405/// Output Bounds:
406///   out1: [[0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff], [0x0 ~> 0xffffffff]]
407#[inline]
408pub const fn fiat_poly1305_selectznz(mut out1: &mut [u32; 5], arg1: fiat_poly1305_u1, arg2: &[u32; 5], arg3: &[u32; 5]) {
409  let mut x1: u32 = 0;
410  fiat_poly1305_cmovznz_u32(&mut x1, arg1, (*IndexConst(arg2).index(0)), (*IndexConst(arg3).index(0)));
411  let mut x2: u32 = 0;
412  fiat_poly1305_cmovznz_u32(&mut x2, arg1, (*IndexConst(arg2).index(1)), (*IndexConst(arg3).index(1)));
413  let mut x3: u32 = 0;
414  fiat_poly1305_cmovznz_u32(&mut x3, arg1, (*IndexConst(arg2).index(2)), (*IndexConst(arg3).index(2)));
415  let mut x4: u32 = 0;
416  fiat_poly1305_cmovznz_u32(&mut x4, arg1, (*IndexConst(arg2).index(3)), (*IndexConst(arg3).index(3)));
417  let mut x5: u32 = 0;
418  fiat_poly1305_cmovznz_u32(&mut x5, arg1, (*IndexConst(arg2).index(4)), (*IndexConst(arg3).index(4)));
419  *IndexConst(&mut out1).index_mut(0) = x1;
420  *IndexConst(&mut out1).index_mut(1) = x2;
421  *IndexConst(&mut out1).index_mut(2) = x3;
422  *IndexConst(&mut out1).index_mut(3) = x4;
423  *IndexConst(&mut out1).index_mut(4) = x5;
424}
425
426/// The function fiat_poly1305_to_bytes serializes a field element to bytes in little-endian order.
427///
428/// Postconditions:
429///   out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..16]
430///
431/// Output Bounds:
432///   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]]
433#[inline]
434pub const fn fiat_poly1305_to_bytes(mut out1: &mut [u8; 17], arg1: &fiat_poly1305_tight_field_element) {
435  let mut x1: u32 = 0;
436  let mut x2: fiat_poly1305_u1 = 0;
437  fiat_poly1305_subborrowx_u26(&mut x1, &mut x2, 0x0, (*IndexConst(arg1).index(0)), 0x3fffffb);
438  let mut x3: u32 = 0;
439  let mut x4: fiat_poly1305_u1 = 0;
440  fiat_poly1305_subborrowx_u26(&mut x3, &mut x4, x2, (*IndexConst(arg1).index(1)), 0x3ffffff);
441  let mut x5: u32 = 0;
442  let mut x6: fiat_poly1305_u1 = 0;
443  fiat_poly1305_subborrowx_u26(&mut x5, &mut x6, x4, (*IndexConst(arg1).index(2)), 0x3ffffff);
444  let mut x7: u32 = 0;
445  let mut x8: fiat_poly1305_u1 = 0;
446  fiat_poly1305_subborrowx_u26(&mut x7, &mut x8, x6, (*IndexConst(arg1).index(3)), 0x3ffffff);
447  let mut x9: u32 = 0;
448  let mut x10: fiat_poly1305_u1 = 0;
449  fiat_poly1305_subborrowx_u26(&mut x9, &mut x10, x8, (*IndexConst(arg1).index(4)), 0x3ffffff);
450  let mut x11: u32 = 0;
451  fiat_poly1305_cmovznz_u32(&mut x11, x10, (0x0 as u32), 0xffffffff);
452  let mut x12: u32 = 0;
453  let mut x13: fiat_poly1305_u1 = 0;
454  fiat_poly1305_addcarryx_u26(&mut x12, &mut x13, 0x0, x1, (x11 & 0x3fffffb));
455  let mut x14: u32 = 0;
456  let mut x15: fiat_poly1305_u1 = 0;
457  fiat_poly1305_addcarryx_u26(&mut x14, &mut x15, x13, x3, (x11 & 0x3ffffff));
458  let mut x16: u32 = 0;
459  let mut x17: fiat_poly1305_u1 = 0;
460  fiat_poly1305_addcarryx_u26(&mut x16, &mut x17, x15, x5, (x11 & 0x3ffffff));
461  let mut x18: u32 = 0;
462  let mut x19: fiat_poly1305_u1 = 0;
463  fiat_poly1305_addcarryx_u26(&mut x18, &mut x19, x17, x7, (x11 & 0x3ffffff));
464  let mut x20: u32 = 0;
465  let mut x21: fiat_poly1305_u1 = 0;
466  fiat_poly1305_addcarryx_u26(&mut x20, &mut x21, x19, x9, (x11 & 0x3ffffff));
467  let x22: u32 = (x18 << 6);
468  let x23: u32 = (x16 << 4);
469  let x24: u32 = (x14 << 2);
470  let x25: u8 = ((x12 & (0xff as u32)) as u8);
471  let x26: u32 = (x12 >> 8);
472  let x27: u8 = ((x26 & (0xff as u32)) as u8);
473  let x28: u32 = (x26 >> 8);
474  let x29: u8 = ((x28 & (0xff as u32)) as u8);
475  let x30: u8 = ((x28 >> 8) as u8);
476  let x31: u32 = (x24 + (x30 as u32));
477  let x32: u8 = ((x31 & (0xff as u32)) as u8);
478  let x33: u32 = (x31 >> 8);
479  let x34: u8 = ((x33 & (0xff as u32)) as u8);
480  let x35: u32 = (x33 >> 8);
481  let x36: u8 = ((x35 & (0xff as u32)) as u8);
482  let x37: u8 = ((x35 >> 8) as u8);
483  let x38: u32 = (x23 + (x37 as u32));
484  let x39: u8 = ((x38 & (0xff as u32)) as u8);
485  let x40: u32 = (x38 >> 8);
486  let x41: u8 = ((x40 & (0xff as u32)) as u8);
487  let x42: u32 = (x40 >> 8);
488  let x43: u8 = ((x42 & (0xff as u32)) as u8);
489  let x44: u8 = ((x42 >> 8) as u8);
490  let x45: u32 = (x22 + (x44 as u32));
491  let x46: u8 = ((x45 & (0xff as u32)) as u8);
492  let x47: u32 = (x45 >> 8);
493  let x48: u8 = ((x47 & (0xff as u32)) as u8);
494  let x49: u32 = (x47 >> 8);
495  let x50: u8 = ((x49 & (0xff as u32)) as u8);
496  let x51: u8 = ((x49 >> 8) as u8);
497  let x52: u8 = ((x20 & (0xff as u32)) as u8);
498  let x53: u32 = (x20 >> 8);
499  let x54: u8 = ((x53 & (0xff as u32)) as u8);
500  let x55: u32 = (x53 >> 8);
501  let x56: u8 = ((x55 & (0xff as u32)) as u8);
502  let x57: u8 = ((x55 >> 8) as u8);
503  *IndexConst(&mut out1).index_mut(0) = x25;
504  *IndexConst(&mut out1).index_mut(1) = x27;
505  *IndexConst(&mut out1).index_mut(2) = x29;
506  *IndexConst(&mut out1).index_mut(3) = x32;
507  *IndexConst(&mut out1).index_mut(4) = x34;
508  *IndexConst(&mut out1).index_mut(5) = x36;
509  *IndexConst(&mut out1).index_mut(6) = x39;
510  *IndexConst(&mut out1).index_mut(7) = x41;
511  *IndexConst(&mut out1).index_mut(8) = x43;
512  *IndexConst(&mut out1).index_mut(9) = x46;
513  *IndexConst(&mut out1).index_mut(10) = x48;
514  *IndexConst(&mut out1).index_mut(11) = x50;
515  *IndexConst(&mut out1).index_mut(12) = x51;
516  *IndexConst(&mut out1).index_mut(13) = x52;
517  *IndexConst(&mut out1).index_mut(14) = x54;
518  *IndexConst(&mut out1).index_mut(15) = x56;
519  *IndexConst(&mut out1).index_mut(16) = x57;
520}
521
522/// The function fiat_poly1305_from_bytes deserializes a field element from bytes in little-endian order.
523///
524/// Postconditions:
525///   eval out1 mod m = bytes_eval arg1 mod m
526///
527/// Input Bounds:
528///   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]]
529#[inline]
530pub const fn fiat_poly1305_from_bytes(mut out1: &mut fiat_poly1305_tight_field_element, arg1: &[u8; 17]) {
531  let x1: u32 = (((*IndexConst(arg1).index(16)) as u32) << 24);
532  let x2: u32 = (((*IndexConst(arg1).index(15)) as u32) << 16);
533  let x3: u32 = (((*IndexConst(arg1).index(14)) as u32) << 8);
534  let x4: u8 = (*IndexConst(arg1).index(13));
535  let x5: u32 = (((*IndexConst(arg1).index(12)) as u32) << 18);
536  let x6: u32 = (((*IndexConst(arg1).index(11)) as u32) << 10);
537  let x7: u32 = (((*IndexConst(arg1).index(10)) as u32) << 2);
538  let x8: u32 = (((*IndexConst(arg1).index(9)) as u32) << 20);
539  let x9: u32 = (((*IndexConst(arg1).index(8)) as u32) << 12);
540  let x10: u32 = (((*IndexConst(arg1).index(7)) as u32) << 4);
541  let x11: u32 = (((*IndexConst(arg1).index(6)) as u32) << 22);
542  let x12: u32 = (((*IndexConst(arg1).index(5)) as u32) << 14);
543  let x13: u32 = (((*IndexConst(arg1).index(4)) as u32) << 6);
544  let x14: u32 = (((*IndexConst(arg1).index(3)) as u32) << 24);
545  let x15: u32 = (((*IndexConst(arg1).index(2)) as u32) << 16);
546  let x16: u32 = (((*IndexConst(arg1).index(1)) as u32) << 8);
547  let x17: u8 = (*IndexConst(arg1).index(0));
548  let x18: u32 = (x16 + (x17 as u32));
549  let x19: u32 = (x15 + x18);
550  let x20: u32 = (x14 + x19);
551  let x21: u32 = (x20 & 0x3ffffff);
552  let x22: u8 = ((x20 >> 26) as u8);
553  let x23: u32 = (x13 + (x22 as u32));
554  let x24: u32 = (x12 + x23);
555  let x25: u32 = (x11 + x24);
556  let x26: u32 = (x25 & 0x3ffffff);
557  let x27: u8 = ((x25 >> 26) as u8);
558  let x28: u32 = (x10 + (x27 as u32));
559  let x29: u32 = (x9 + x28);
560  let x30: u32 = (x8 + x29);
561  let x31: u32 = (x30 & 0x3ffffff);
562  let x32: u8 = ((x30 >> 26) as u8);
563  let x33: u32 = (x7 + (x32 as u32));
564  let x34: u32 = (x6 + x33);
565  let x35: u32 = (x5 + x34);
566  let x36: u32 = (x3 + (x4 as u32));
567  let x37: u32 = (x2 + x36);
568  let x38: u32 = (x1 + x37);
569  *IndexConst(&mut out1).index_mut(0) = x21;
570  *IndexConst(&mut out1).index_mut(1) = x26;
571  *IndexConst(&mut out1).index_mut(2) = x31;
572  *IndexConst(&mut out1).index_mut(3) = x35;
573  *IndexConst(&mut out1).index_mut(4) = x38;
574}
575
576/// The function fiat_poly1305_relax is the identity function converting from tight field elements to loose field elements.
577///
578/// Postconditions:
579///   out1 = arg1
580///
581#[inline]
582pub const fn fiat_poly1305_relax(mut out1: &mut fiat_poly1305_loose_field_element, arg1: &fiat_poly1305_tight_field_element) {
583  let x1: u32 = (*IndexConst(arg1).index(0));
584  let x2: u32 = (*IndexConst(arg1).index(1));
585  let x3: u32 = (*IndexConst(arg1).index(2));
586  let x4: u32 = (*IndexConst(arg1).index(3));
587  let x5: u32 = (*IndexConst(arg1).index(4));
588  *IndexConst(&mut out1).index_mut(0) = x1;
589  *IndexConst(&mut out1).index_mut(1) = x2;
590  *IndexConst(&mut out1).index_mut(2) = x3;
591  *IndexConst(&mut out1).index_mut(3) = x4;
592  *IndexConst(&mut out1).index_mut(4) = x5;
593}
fiat_crypto/poly1305_32.rs

fiat_crypto/
poly1305_32.rs
