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

fiat_crypto/
curve25519_solinas_64.rs
