fiat_crypto/
curve25519_solinas_64.rs

1//! Autogenerated: 'src/ExtractionOCaml/solinas_reduction' --lang Rust --inline curve25519_solinas 64 '2^255 - 19' mul square
2//! curve description: curve25519_solinas
3//! machine_wordsize = 64 (from "64")
4//! requested operations: mul, square
5//! s-c = 2^255 - [(1, 19)] (from "2^255 - 19")
6//!
7//! Computed values:
8//!
9
10#![allow(unused_parens)]
11#![allow(non_camel_case_types)]
12
13/// Since `Index` and `IndexMut` aren't callable in `const` contexts yet, this helper type helps unify
14/// arrays and user-defined array-wrapper types into a single type which can be indexed in `const`
15/// contexts. Once `const trait`s are stabilized this type can go away
16struct IndexConst<T: ?Sized>(T);
17
18impl<'a, T, const N: usize> IndexConst<&'a [T; N]> {
19    #[inline(always)]
20    #[allow(unused)]
21    const fn index(self, i: usize) -> &'a T {
22        &self.0[i]
23    }
24}
25impl<'a, 'b, T, const N: usize> IndexConst<&'a mut &'b mut [T; N]> {
26    #[inline(always)]
27    #[allow(unused)]
28    const fn index_mut(self, i: usize) -> &'a mut T {
29        &mut self.0[i]
30    }
31}
32
33/** fiat_curve25519_solinas_u1 represents values of 1 bits, stored in one byte. */
34pub type fiat_curve25519_solinas_u1 = u8;
35/** fiat_curve25519_solinas_i1 represents values of 1 bits, stored in one byte. */
36pub type fiat_curve25519_solinas_i1 = i8;
37/** fiat_curve25519_solinas_u2 represents values of 2 bits, stored in one byte. */
38pub type fiat_curve25519_solinas_u2 = u8;
39/** fiat_curve25519_solinas_i2 represents values of 2 bits, stored in one byte. */
40pub type fiat_curve25519_solinas_i2 = i8;
41
42
43/// The function fiat_curve25519_solinas_addcarryx_u64 is an addition with carry.
44///
45/// Postconditions:
46///   out1 = (arg1 + arg2 + arg3) mod 2^64
47///   out2 = ⌊(arg1 + arg2 + arg3) / 2^64⌋
48///
49/// Input Bounds:
50///   arg1: [0x0 ~> 0x1]
51///   arg2: [0x0 ~> 0xffffffffffffffff]
52///   arg3: [0x0 ~> 0xffffffffffffffff]
53/// Output Bounds:
54///   out1: [0x0 ~> 0xffffffffffffffff]
55///   out2: [0x0 ~> 0x1]
56#[inline]
57pub const fn fiat_curve25519_solinas_addcarryx_u64(out1: &mut u64, out2: &mut fiat_curve25519_solinas_u1, arg1: fiat_curve25519_solinas_u1, arg2: u64, arg3: u64) {
58  let x1: u128 = (((arg1 as u128) + (arg2 as u128)) + (arg3 as u128));
59  let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64);
60  let x3: fiat_curve25519_solinas_u1 = ((x1 >> 64) as fiat_curve25519_solinas_u1);
61  *out1 = x2;
62  *out2 = x3;
63}
64
65/// The function fiat_curve25519_solinas_subborrowx_u64 is a subtraction with borrow.
66///
67/// Postconditions:
68///   out1 = (-arg1 + arg2 + -arg3) mod 2^64
69///   out2 = -⌊(-arg1 + arg2 + -arg3) / 2^64⌋
70///
71/// Input Bounds:
72///   arg1: [0x0 ~> 0x1]
73///   arg2: [0x0 ~> 0xffffffffffffffff]
74///   arg3: [0x0 ~> 0xffffffffffffffff]
75/// Output Bounds:
76///   out1: [0x0 ~> 0xffffffffffffffff]
77///   out2: [0x0 ~> 0x1]
78#[inline]
79pub const fn fiat_curve25519_solinas_subborrowx_u64(out1: &mut u64, out2: &mut fiat_curve25519_solinas_u1, arg1: fiat_curve25519_solinas_u1, arg2: u64, arg3: u64) {
80  let x1: i128 = (((arg2 as i128) - (arg1 as i128)) - (arg3 as i128));
81  let x2: fiat_curve25519_solinas_i1 = ((x1 >> 64) as fiat_curve25519_solinas_i1);
82  let x3: u64 = ((x1 & (0xffffffffffffffff as i128)) as u64);
83  *out1 = x3;
84  *out2 = (((0x0 as fiat_curve25519_solinas_i2) - (x2 as fiat_curve25519_solinas_i2)) as fiat_curve25519_solinas_u1);
85}
86
87/// The function fiat_curve25519_solinas_mulx_u64 is a multiplication, returning the full double-width result.
88///
89/// Postconditions:
90///   out1 = (arg1 * arg2) mod 2^64
91///   out2 = ⌊arg1 * arg2 / 2^64⌋
92///
93/// Input Bounds:
94///   arg1: [0x0 ~> 0xffffffffffffffff]
95///   arg2: [0x0 ~> 0xffffffffffffffff]
96/// Output Bounds:
97///   out1: [0x0 ~> 0xffffffffffffffff]
98///   out2: [0x0 ~> 0xffffffffffffffff]
99#[inline]
100pub const fn fiat_curve25519_solinas_mulx_u64(out1: &mut u64, out2: &mut u64, arg1: u64, arg2: u64) {
101  let x1: u128 = ((arg1 as u128) * (arg2 as u128));
102  let x2: u64 = ((x1 & (0xffffffffffffffff as u128)) as u64);
103  let x3: u64 = ((x1 >> 64) as u64);
104  *out1 = x2;
105  *out2 = x3;
106}
107
108/// The function fiat_curve25519_solinas_cmovznz_u64 is a single-word conditional move.
109///
110/// Postconditions:
111///   out1 = (if arg1 = 0 then arg2 else arg3)
112///
113/// Input Bounds:
114///   arg1: [0x0 ~> 0x1]
115///   arg2: [0x0 ~> 0xffffffffffffffff]
116///   arg3: [0x0 ~> 0xffffffffffffffff]
117/// Output Bounds:
118///   out1: [0x0 ~> 0xffffffffffffffff]
119#[inline]
120pub const fn fiat_curve25519_solinas_cmovznz_u64(out1: &mut u64, arg1: fiat_curve25519_solinas_u1, arg2: u64, arg3: u64) {
121  let x1: fiat_curve25519_solinas_u1 = (!(!arg1));
122  let x2: u64 = ((((((0x0 as fiat_curve25519_solinas_i2) - (x1 as fiat_curve25519_solinas_i2)) as fiat_curve25519_solinas_i1) as i128) & (0xffffffffffffffff as i128)) as u64);
123  let x3: u64 = ((x2 & arg3) | ((!x2) & arg2));
124  *out1 = x3;
125}
126
127/// The function fiat_curve25519_solinas_mul multiplies two field elements.
128///
129/// Postconditions:
130///   eval out1 mod 57896044618658097711785492504343953926634992332820282019728792003956564819949 = (eval arg1 * eval arg2) mod 57896044618658097711785492504343953926634992332820282019728792003956564819949
131///
132/// Input Bounds:
133///   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
134///   arg2: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
135/// Output Bounds:
136///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
137#[inline]
138pub const fn fiat_curve25519_solinas_mul(mut out1: &mut [u64; 4], arg1: &[u64; 4], arg2: &[u64; 4]) {
139  let mut x1: u64 = 0;
140  let mut x2: u64 = 0;
141  fiat_curve25519_solinas_mulx_u64(&mut x1, &mut x2, (*IndexConst(arg1).index(3)), (*IndexConst(arg2).index(3)));
142  let mut x3: u64 = 0;
143  let mut x4: u64 = 0;
144  fiat_curve25519_solinas_mulx_u64(&mut x3, &mut x4, (*IndexConst(arg1).index(3)), (*IndexConst(arg2).index(2)));
145  let mut x5: u64 = 0;
146  let mut x6: u64 = 0;
147  fiat_curve25519_solinas_mulx_u64(&mut x5, &mut x6, (*IndexConst(arg1).index(3)), (*IndexConst(arg2).index(1)));
148  let mut x7: u64 = 0;
149  let mut x8: u64 = 0;
150  fiat_curve25519_solinas_mulx_u64(&mut x7, &mut x8, (*IndexConst(arg1).index(3)), (*IndexConst(arg2).index(0)));
151  let mut x9: u64 = 0;
152  let mut x10: u64 = 0;
153  fiat_curve25519_solinas_mulx_u64(&mut x9, &mut x10, (*IndexConst(arg1).index(2)), (*IndexConst(arg2).index(3)));
154  let mut x11: u64 = 0;
155  let mut x12: u64 = 0;
156  fiat_curve25519_solinas_mulx_u64(&mut x11, &mut x12, (*IndexConst(arg1).index(2)), (*IndexConst(arg2).index(2)));
157  let mut x13: u64 = 0;
158  let mut x14: u64 = 0;
159  fiat_curve25519_solinas_mulx_u64(&mut x13, &mut x14, (*IndexConst(arg1).index(2)), (*IndexConst(arg2).index(1)));
160  let mut x15: u64 = 0;
161  let mut x16: u64 = 0;
162  fiat_curve25519_solinas_mulx_u64(&mut x15, &mut x16, (*IndexConst(arg1).index(2)), (*IndexConst(arg2).index(0)));
163  let mut x17: u64 = 0;
164  let mut x18: u64 = 0;
165  fiat_curve25519_solinas_mulx_u64(&mut x17, &mut x18, (*IndexConst(arg1).index(1)), (*IndexConst(arg2).index(3)));
166  let mut x19: u64 = 0;
167  let mut x20: u64 = 0;
168  fiat_curve25519_solinas_mulx_u64(&mut x19, &mut x20, (*IndexConst(arg1).index(1)), (*IndexConst(arg2).index(2)));
169  let mut x21: u64 = 0;
170  let mut x22: u64 = 0;
171  fiat_curve25519_solinas_mulx_u64(&mut x21, &mut x22, (*IndexConst(arg1).index(1)), (*IndexConst(arg2).index(1)));
172  let mut x23: u64 = 0;
173  let mut x24: u64 = 0;
174  fiat_curve25519_solinas_mulx_u64(&mut x23, &mut x24, (*IndexConst(arg1).index(1)), (*IndexConst(arg2).index(0)));
175  let mut x25: u64 = 0;
176  let mut x26: u64 = 0;
177  fiat_curve25519_solinas_mulx_u64(&mut x25, &mut x26, (*IndexConst(arg1).index(0)), (*IndexConst(arg2).index(3)));
178  let mut x27: u64 = 0;
179  let mut x28: u64 = 0;
180  fiat_curve25519_solinas_mulx_u64(&mut x27, &mut x28, (*IndexConst(arg1).index(0)), (*IndexConst(arg2).index(2)));
181  let mut x29: u64 = 0;
182  let mut x30: u64 = 0;
183  fiat_curve25519_solinas_mulx_u64(&mut x29, &mut x30, (*IndexConst(arg1).index(0)), (*IndexConst(arg2).index(1)));
184  let mut x31: u64 = 0;
185  let mut x32: u64 = 0;
186  fiat_curve25519_solinas_mulx_u64(&mut x31, &mut x32, (*IndexConst(arg1).index(0)), (*IndexConst(arg2).index(0)));
187  let mut x33: u64 = 0;
188  let mut x34: fiat_curve25519_solinas_u1 = 0;
189  fiat_curve25519_solinas_addcarryx_u64(&mut x33, &mut x34, 0x0, x28, x7);
190  let mut x35: u64 = 0;
191  let mut x36: fiat_curve25519_solinas_u1 = 0;
192  fiat_curve25519_solinas_addcarryx_u64(&mut x35, &mut x36, x34, x26, x5);
193  let x37: u64 = ((x36 as u64) + x18);
194  let mut x38: u64 = 0;
195  let mut x39: fiat_curve25519_solinas_u1 = 0;
196  fiat_curve25519_solinas_addcarryx_u64(&mut x38, &mut x39, 0x0, x33, x13);
197  let mut x40: u64 = 0;
198  let mut x41: fiat_curve25519_solinas_u1 = 0;
199  fiat_curve25519_solinas_addcarryx_u64(&mut x40, &mut x41, x39, x35, x8);
200  let mut x42: u64 = 0;
201  let mut x43: fiat_curve25519_solinas_u1 = 0;
202  fiat_curve25519_solinas_addcarryx_u64(&mut x42, &mut x43, x41, x37, (0x0 as u64));
203  let x44: u64 = ((x43 as u64) + x10);
204  let mut x45: u64 = 0;
205  let mut x46: fiat_curve25519_solinas_u1 = 0;
206  fiat_curve25519_solinas_addcarryx_u64(&mut x45, &mut x46, 0x0, x30, x15);
207  let mut x47: u64 = 0;
208  let mut x48: fiat_curve25519_solinas_u1 = 0;
209  fiat_curve25519_solinas_addcarryx_u64(&mut x47, &mut x48, x46, x38, x16);
210  let mut x49: u64 = 0;
211  let mut x50: fiat_curve25519_solinas_u1 = 0;
212  fiat_curve25519_solinas_addcarryx_u64(&mut x49, &mut x50, x48, x40, x11);
213  let mut x51: u64 = 0;
214  let mut x52: fiat_curve25519_solinas_u1 = 0;
215  fiat_curve25519_solinas_addcarryx_u64(&mut x51, &mut x52, x50, x42, x3);
216  let mut x53: u64 = 0;
217  let mut x54: fiat_curve25519_solinas_u1 = 0;
218  fiat_curve25519_solinas_addcarryx_u64(&mut x53, &mut x54, x52, x44, (0x0 as u64));
219  let x55: u64 = ((x54 as u64) + x2);
220  let mut x56: u64 = 0;
221  let mut x57: fiat_curve25519_solinas_u1 = 0;
222  fiat_curve25519_solinas_addcarryx_u64(&mut x56, &mut x57, 0x0, x45, x21);
223  let mut x58: u64 = 0;
224  let mut x59: fiat_curve25519_solinas_u1 = 0;
225  fiat_curve25519_solinas_addcarryx_u64(&mut x58, &mut x59, x57, x47, x19);
226  let mut x60: u64 = 0;
227  let mut x61: fiat_curve25519_solinas_u1 = 0;
228  fiat_curve25519_solinas_addcarryx_u64(&mut x60, &mut x61, x59, x49, x14);
229  let mut x62: u64 = 0;
230  let mut x63: fiat_curve25519_solinas_u1 = 0;
231  fiat_curve25519_solinas_addcarryx_u64(&mut x62, &mut x63, x61, x51, x6);
232  let mut x64: u64 = 0;
233  let mut x65: fiat_curve25519_solinas_u1 = 0;
234  fiat_curve25519_solinas_addcarryx_u64(&mut x64, &mut x65, x63, x53, (0x0 as u64));
235  let mut x66: u64 = 0;
236  let mut x67: fiat_curve25519_solinas_u1 = 0;
237  fiat_curve25519_solinas_addcarryx_u64(&mut x66, &mut x67, x65, x55, (0x0 as u64));
238  let mut x68: u64 = 0;
239  let mut x69: fiat_curve25519_solinas_u1 = 0;
240  fiat_curve25519_solinas_addcarryx_u64(&mut x68, &mut x69, 0x0, x32, x23);
241  let mut x70: u64 = 0;
242  let mut x71: fiat_curve25519_solinas_u1 = 0;
243  fiat_curve25519_solinas_addcarryx_u64(&mut x70, &mut x71, x69, x56, x24);
244  let mut x72: u64 = 0;
245  let mut x73: fiat_curve25519_solinas_u1 = 0;
246  fiat_curve25519_solinas_addcarryx_u64(&mut x72, &mut x73, x71, x58, x22);
247  let mut x74: u64 = 0;
248  let mut x75: fiat_curve25519_solinas_u1 = 0;
249  fiat_curve25519_solinas_addcarryx_u64(&mut x74, &mut x75, x73, x60, x17);
250  let mut x76: u64 = 0;
251  let mut x77: fiat_curve25519_solinas_u1 = 0;
252  fiat_curve25519_solinas_addcarryx_u64(&mut x76, &mut x77, x75, x62, x9);
253  let mut x78: u64 = 0;
254  let mut x79: fiat_curve25519_solinas_u1 = 0;
255  fiat_curve25519_solinas_addcarryx_u64(&mut x78, &mut x79, x77, x64, x1);
256  let mut x80: u64 = 0;
257  let mut x81: fiat_curve25519_solinas_u1 = 0;
258  fiat_curve25519_solinas_addcarryx_u64(&mut x80, &mut x81, x79, x66, (0x0 as u64));
259  let mut x82: u64 = 0;
260  let mut x83: fiat_curve25519_solinas_u1 = 0;
261  fiat_curve25519_solinas_addcarryx_u64(&mut x82, &mut x83, 0x0, x68, x29);
262  let mut x84: u64 = 0;
263  let mut x85: fiat_curve25519_solinas_u1 = 0;
264  fiat_curve25519_solinas_addcarryx_u64(&mut x84, &mut x85, x83, x70, x27);
265  let mut x86: u64 = 0;
266  let mut x87: fiat_curve25519_solinas_u1 = 0;
267  fiat_curve25519_solinas_addcarryx_u64(&mut x86, &mut x87, x85, x72, x25);
268  let mut x88: u64 = 0;
269  let mut x89: fiat_curve25519_solinas_u1 = 0;
270  fiat_curve25519_solinas_addcarryx_u64(&mut x88, &mut x89, x87, x74, x20);
271  let mut x90: u64 = 0;
272  let mut x91: fiat_curve25519_solinas_u1 = 0;
273  fiat_curve25519_solinas_addcarryx_u64(&mut x90, &mut x91, x89, x76, x12);
274  let mut x92: u64 = 0;
275  let mut x93: fiat_curve25519_solinas_u1 = 0;
276  fiat_curve25519_solinas_addcarryx_u64(&mut x92, &mut x93, x91, x78, x4);
277  let mut x94: u64 = 0;
278  let mut x95: fiat_curve25519_solinas_u1 = 0;
279  fiat_curve25519_solinas_addcarryx_u64(&mut x94, &mut x95, x93, x80, (0x0 as u64));
280  let mut x96: u64 = 0;
281  let mut x97: u64 = 0;
282  fiat_curve25519_solinas_mulx_u64(&mut x96, &mut x97, 0x26, x94);
283  let mut x98: u64 = 0;
284  let mut x99: u64 = 0;
285  fiat_curve25519_solinas_mulx_u64(&mut x98, &mut x99, 0x26, x92);
286  let mut x100: u64 = 0;
287  let mut x101: u64 = 0;
288  fiat_curve25519_solinas_mulx_u64(&mut x100, &mut x101, 0x26, x90);
289  let mut x102: u64 = 0;
290  let mut x103: u64 = 0;
291  fiat_curve25519_solinas_mulx_u64(&mut x102, &mut x103, 0x26, x88);
292  let mut x104: u64 = 0;
293  let mut x105: fiat_curve25519_solinas_u1 = 0;
294  fiat_curve25519_solinas_addcarryx_u64(&mut x104, &mut x105, 0x0, x82, x100);
295  let mut x106: u64 = 0;
296  let mut x107: fiat_curve25519_solinas_u1 = 0;
297  fiat_curve25519_solinas_addcarryx_u64(&mut x106, &mut x107, x105, x84, x98);
298  let mut x108: u64 = 0;
299  let mut x109: fiat_curve25519_solinas_u1 = 0;
300  fiat_curve25519_solinas_addcarryx_u64(&mut x108, &mut x109, x107, x86, x96);
301  let x110: u64 = ((x109 as u64) + x97);
302  let mut x111: u64 = 0;
303  let mut x112: fiat_curve25519_solinas_u1 = 0;
304  fiat_curve25519_solinas_addcarryx_u64(&mut x111, &mut x112, 0x0, x31, x102);
305  let mut x113: u64 = 0;
306  let mut x114: fiat_curve25519_solinas_u1 = 0;
307  fiat_curve25519_solinas_addcarryx_u64(&mut x113, &mut x114, x112, x104, x103);
308  let mut x115: u64 = 0;
309  let mut x116: fiat_curve25519_solinas_u1 = 0;
310  fiat_curve25519_solinas_addcarryx_u64(&mut x115, &mut x116, x114, x106, x101);
311  let mut x117: u64 = 0;
312  let mut x118: fiat_curve25519_solinas_u1 = 0;
313  fiat_curve25519_solinas_addcarryx_u64(&mut x117, &mut x118, x116, x108, x99);
314  let x119: u64 = ((x118 as u64) + x110);
315  let mut x120: u64 = 0;
316  let mut x121: u64 = 0;
317  fiat_curve25519_solinas_mulx_u64(&mut x120, &mut x121, 0x26, x119);
318  let mut x122: u64 = 0;
319  let mut x123: fiat_curve25519_solinas_u1 = 0;
320  fiat_curve25519_solinas_addcarryx_u64(&mut x122, &mut x123, 0x0, x111, x120);
321  let mut x124: u64 = 0;
322  let mut x125: fiat_curve25519_solinas_u1 = 0;
323  fiat_curve25519_solinas_addcarryx_u64(&mut x124, &mut x125, x123, x113, (0x0 as u64));
324  let mut x126: u64 = 0;
325  let mut x127: fiat_curve25519_solinas_u1 = 0;
326  fiat_curve25519_solinas_addcarryx_u64(&mut x126, &mut x127, x125, x115, (0x0 as u64));
327  let mut x128: u64 = 0;
328  let mut x129: fiat_curve25519_solinas_u1 = 0;
329  fiat_curve25519_solinas_addcarryx_u64(&mut x128, &mut x129, x127, x117, (0x0 as u64));
330  let mut x130: u64 = 0;
331  fiat_curve25519_solinas_cmovznz_u64(&mut x130, x129, (0x0 as u64), 0x26);
332  let mut x131: u64 = 0;
333  let mut x132: fiat_curve25519_solinas_u1 = 0;
334  fiat_curve25519_solinas_addcarryx_u64(&mut x131, &mut x132, 0x0, x130, x122);
335  *IndexConst(&mut out1).index_mut(0) = x131;
336  *IndexConst(&mut out1).index_mut(1) = x124;
337  *IndexConst(&mut out1).index_mut(2) = x126;
338  *IndexConst(&mut out1).index_mut(3) = x128;
339}
340
341/// The function fiat_curve25519_solinas_square squares a field element.
342///
343/// Postconditions:
344///   eval out1 mod 57896044618658097711785492504343953926634992332820282019728792003956564819949 = (eval arg1 * eval arg1) mod 57896044618658097711785492504343953926634992332820282019728792003956564819949
345///
346/// Input Bounds:
347///   arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
348/// Output Bounds:
349///   out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]]
350#[inline]
351pub const fn fiat_curve25519_solinas_square(mut out1: &mut [u64; 4], arg1: &[u64; 4]) {
352  let mut x1: u64 = 0;
353  let mut x2: u64 = 0;
354  fiat_curve25519_solinas_mulx_u64(&mut x1, &mut x2, (*IndexConst(arg1).index(0)), (*IndexConst(arg1).index(3)));
355  let mut x3: u64 = 0;
356  let mut x4: u64 = 0;
357  fiat_curve25519_solinas_mulx_u64(&mut x3, &mut x4, (*IndexConst(arg1).index(0)), (*IndexConst(arg1).index(2)));
358  let mut x5: u64 = 0;
359  let mut x6: u64 = 0;
360  fiat_curve25519_solinas_mulx_u64(&mut x5, &mut x6, (*IndexConst(arg1).index(0)), (*IndexConst(arg1).index(1)));
361  let mut x7: u64 = 0;
362  let mut x8: u64 = 0;
363  fiat_curve25519_solinas_mulx_u64(&mut x7, &mut x8, (*IndexConst(arg1).index(3)), (*IndexConst(arg1).index(2)));
364  let mut x9: u64 = 0;
365  let mut x10: u64 = 0;
366  fiat_curve25519_solinas_mulx_u64(&mut x9, &mut x10, (*IndexConst(arg1).index(3)), (*IndexConst(arg1).index(1)));
367  let mut x11: u64 = 0;
368  let mut x12: fiat_curve25519_solinas_u1 = 0;
369  fiat_curve25519_solinas_addcarryx_u64(&mut x11, &mut x12, 0x0, x6, x3);
370  let mut x13: u64 = 0;
371  let mut x14: fiat_curve25519_solinas_u1 = 0;
372  fiat_curve25519_solinas_addcarryx_u64(&mut x13, &mut x14, x12, x4, x1);
373  let mut x15: u64 = 0;
374  let mut x16: fiat_curve25519_solinas_u1 = 0;
375  fiat_curve25519_solinas_addcarryx_u64(&mut x15, &mut x16, x14, x2, x9);
376  let mut x17: u64 = 0;
377  let mut x18: fiat_curve25519_solinas_u1 = 0;
378  fiat_curve25519_solinas_addcarryx_u64(&mut x17, &mut x18, x16, x10, x7);
379  let x19: u64 = ((x18 as u64) + x8);
380  let mut x20: u64 = 0;
381  let mut x21: u64 = 0;
382  fiat_curve25519_solinas_mulx_u64(&mut x20, &mut x21, (*IndexConst(arg1).index(1)), (*IndexConst(arg1).index(2)));
383  let mut x22: u64 = 0;
384  let mut x23: fiat_curve25519_solinas_u1 = 0;
385  fiat_curve25519_solinas_addcarryx_u64(&mut x22, &mut x23, 0x0, x13, x20);
386  let mut x24: u64 = 0;
387  let mut x25: fiat_curve25519_solinas_u1 = 0;
388  fiat_curve25519_solinas_addcarryx_u64(&mut x24, &mut x25, x23, x15, x21);
389  let mut x26: u64 = 0;
390  let mut x27: fiat_curve25519_solinas_u1 = 0;
391  fiat_curve25519_solinas_addcarryx_u64(&mut x26, &mut x27, x25, x17, (0x0 as u64));
392  let mut x28: u64 = 0;
393  let mut x29: fiat_curve25519_solinas_u1 = 0;
394  fiat_curve25519_solinas_addcarryx_u64(&mut x28, &mut x29, x27, x19, (0x0 as u64));
395  let mut x30: u64 = 0;
396  let mut x31: fiat_curve25519_solinas_u1 = 0;
397  fiat_curve25519_solinas_addcarryx_u64(&mut x30, &mut x31, 0x0, x5, x5);
398  let mut x32: u64 = 0;
399  let mut x33: fiat_curve25519_solinas_u1 = 0;
400  fiat_curve25519_solinas_addcarryx_u64(&mut x32, &mut x33, x31, x11, x11);
401  let mut x34: u64 = 0;
402  let mut x35: fiat_curve25519_solinas_u1 = 0;
403  fiat_curve25519_solinas_addcarryx_u64(&mut x34, &mut x35, x33, x22, x22);
404  let mut x36: u64 = 0;
405  let mut x37: fiat_curve25519_solinas_u1 = 0;
406  fiat_curve25519_solinas_addcarryx_u64(&mut x36, &mut x37, x35, x24, x24);
407  let mut x38: u64 = 0;
408  let mut x39: fiat_curve25519_solinas_u1 = 0;
409  fiat_curve25519_solinas_addcarryx_u64(&mut x38, &mut x39, x37, x26, x26);
410  let mut x40: u64 = 0;
411  let mut x41: fiat_curve25519_solinas_u1 = 0;
412  fiat_curve25519_solinas_addcarryx_u64(&mut x40, &mut x41, x39, x28, x28);
413  let x42: u64 = (((x41 as u64) + (x29 as u64)) + (x29 as u64));
414  let mut x43: u64 = 0;
415  let mut x44: u64 = 0;
416  fiat_curve25519_solinas_mulx_u64(&mut x43, &mut x44, (*IndexConst(arg1).index(3)), (*IndexConst(arg1).index(3)));
417  let mut x45: u64 = 0;
418  let mut x46: u64 = 0;
419  fiat_curve25519_solinas_mulx_u64(&mut x45, &mut x46, (*IndexConst(arg1).index(2)), (*IndexConst(arg1).index(2)));
420  let mut x47: u64 = 0;
421  let mut x48: u64 = 0;
422  fiat_curve25519_solinas_mulx_u64(&mut x47, &mut x48, (*IndexConst(arg1).index(1)), (*IndexConst(arg1).index(1)));
423  let mut x49: u64 = 0;
424  let mut x50: u64 = 0;
425  fiat_curve25519_solinas_mulx_u64(&mut x49, &mut x50, (*IndexConst(arg1).index(0)), (*IndexConst(arg1).index(0)));
426  let mut x51: u64 = 0;
427  let mut x52: fiat_curve25519_solinas_u1 = 0;
428  fiat_curve25519_solinas_addcarryx_u64(&mut x51, &mut x52, 0x0, x30, x50);
429  let mut x53: u64 = 0;
430  let mut x54: fiat_curve25519_solinas_u1 = 0;
431  fiat_curve25519_solinas_addcarryx_u64(&mut x53, &mut x54, x52, x32, x47);
432  let mut x55: u64 = 0;
433  let mut x56: fiat_curve25519_solinas_u1 = 0;
434  fiat_curve25519_solinas_addcarryx_u64(&mut x55, &mut x56, x54, x34, x48);
435  let mut x57: u64 = 0;
436  let mut x58: fiat_curve25519_solinas_u1 = 0;
437  fiat_curve25519_solinas_addcarryx_u64(&mut x57, &mut x58, x56, x36, x45);
438  let mut x59: u64 = 0;
439  let mut x60: fiat_curve25519_solinas_u1 = 0;
440  fiat_curve25519_solinas_addcarryx_u64(&mut x59, &mut x60, x58, x38, x46);
441  let mut x61: u64 = 0;
442  let mut x62: fiat_curve25519_solinas_u1 = 0;
443  fiat_curve25519_solinas_addcarryx_u64(&mut x61, &mut x62, x60, x40, x43);
444  let mut x63: u64 = 0;
445  let mut x64: fiat_curve25519_solinas_u1 = 0;
446  fiat_curve25519_solinas_addcarryx_u64(&mut x63, &mut x64, x62, x42, x44);
447  let mut x65: u64 = 0;
448  let mut x66: u64 = 0;
449  fiat_curve25519_solinas_mulx_u64(&mut x65, &mut x66, 0x26, x63);
450  let mut x67: u64 = 0;
451  let mut x68: u64 = 0;
452  fiat_curve25519_solinas_mulx_u64(&mut x67, &mut x68, 0x26, x61);
453  let mut x69: u64 = 0;
454  let mut x70: u64 = 0;
455  fiat_curve25519_solinas_mulx_u64(&mut x69, &mut x70, 0x26, x59);
456  let mut x71: u64 = 0;
457  let mut x72: u64 = 0;
458  fiat_curve25519_solinas_mulx_u64(&mut x71, &mut x72, 0x26, x57);
459  let mut x73: u64 = 0;
460  let mut x74: fiat_curve25519_solinas_u1 = 0;
461  fiat_curve25519_solinas_addcarryx_u64(&mut x73, &mut x74, 0x0, x51, x69);
462  let mut x75: u64 = 0;
463  let mut x76: fiat_curve25519_solinas_u1 = 0;
464  fiat_curve25519_solinas_addcarryx_u64(&mut x75, &mut x76, x74, x53, x67);
465  let mut x77: u64 = 0;
466  let mut x78: fiat_curve25519_solinas_u1 = 0;
467  fiat_curve25519_solinas_addcarryx_u64(&mut x77, &mut x78, x76, x55, x65);
468  let x79: u64 = ((x78 as u64) + x66);
469  let mut x80: u64 = 0;
470  let mut x81: fiat_curve25519_solinas_u1 = 0;
471  fiat_curve25519_solinas_addcarryx_u64(&mut x80, &mut x81, 0x0, x49, x71);
472  let mut x82: u64 = 0;
473  let mut x83: fiat_curve25519_solinas_u1 = 0;
474  fiat_curve25519_solinas_addcarryx_u64(&mut x82, &mut x83, x81, x73, x72);
475  let mut x84: u64 = 0;
476  let mut x85: fiat_curve25519_solinas_u1 = 0;
477  fiat_curve25519_solinas_addcarryx_u64(&mut x84, &mut x85, x83, x75, x70);
478  let mut x86: u64 = 0;
479  let mut x87: fiat_curve25519_solinas_u1 = 0;
480  fiat_curve25519_solinas_addcarryx_u64(&mut x86, &mut x87, x85, x77, x68);
481  let x88: u64 = ((x87 as u64) + x79);
482  let mut x89: u64 = 0;
483  let mut x90: u64 = 0;
484  fiat_curve25519_solinas_mulx_u64(&mut x89, &mut x90, 0x26, x88);
485  let mut x91: u64 = 0;
486  let mut x92: fiat_curve25519_solinas_u1 = 0;
487  fiat_curve25519_solinas_addcarryx_u64(&mut x91, &mut x92, 0x0, x80, x89);
488  let mut x93: u64 = 0;
489  let mut x94: fiat_curve25519_solinas_u1 = 0;
490  fiat_curve25519_solinas_addcarryx_u64(&mut x93, &mut x94, x92, x82, (0x0 as u64));
491  let mut x95: u64 = 0;
492  let mut x96: fiat_curve25519_solinas_u1 = 0;
493  fiat_curve25519_solinas_addcarryx_u64(&mut x95, &mut x96, x94, x84, (0x0 as u64));
494  let mut x97: u64 = 0;
495  let mut x98: fiat_curve25519_solinas_u1 = 0;
496  fiat_curve25519_solinas_addcarryx_u64(&mut x97, &mut x98, x96, x86, (0x0 as u64));
497  let mut x99: u64 = 0;
498  fiat_curve25519_solinas_cmovznz_u64(&mut x99, x98, (0x0 as u64), 0x26);
499  let mut x100: u64 = 0;
500  let mut x101: fiat_curve25519_solinas_u1 = 0;
501  fiat_curve25519_solinas_addcarryx_u64(&mut x100, &mut x101, 0x0, x99, x91);
502  *IndexConst(&mut out1).index_mut(0) = x100;
503  *IndexConst(&mut out1).index_mut(1) = x93;
504  *IndexConst(&mut out1).index_mut(2) = x95;
505  *IndexConst(&mut out1).index_mut(3) = x97;
506}
fiat_crypto/curve25519_solinas_64.rs

fiat_crypto/
curve25519_solinas_64.rs
