fiat_crypto/
secp256k1_dettman_32.rs

1//! Autogenerated: 'src/ExtractionOCaml/dettman_multiplication' --lang Rust --inline secp256k1_dettman 32 10 22 6 '2^256 - 4294968273' mul square
2//! curve description: secp256k1_dettman
3//! machine_wordsize = 32 (from "32")
4//! requested operations: mul, square
5//! n = 10 (from "10")
6//! last_limb_width = 22 (from "22")
7//! last_reduction = 6 (from "6")
8//! s-c = 2^256 - [(1, 4294968273)] (from "2^256 - 4294968273")
9//! inbounds_multiplier: None (from "")
10//!
11//! Computed values:
12//!
13//!
14
15#![allow(unused_parens)]
16#![allow(non_camel_case_types)]
17
18
19
20/// The function fiat_secp256k1_dettman_mul multiplies two field elements.
21///
22/// Postconditions:
23///   eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg2) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663
24///
25/// Input Bounds:
26///   arg1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
27///   arg2: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
28/// Output Bounds:
29///   out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x5fffff]]
30#[inline]
31pub fn fiat_secp256k1_dettman_mul(out1: &mut [u32; 10], arg1: &[u32; 10], arg2: &[u32; 10]) {
32  let x1: u64 = ((((arg1[8]) as u64) * ((arg2[9]) as u64)) + (((arg1[9]) as u64) * ((arg2[8]) as u64)));
33  let x2: u32 = ((x1 >> 26) as u32);
34  let x3: u32 = ((x1 & (0x3ffffff as u64)) as u32);
35  let x4: u64 = (((((arg1[0]) as u64) * ((arg2[7]) as u64)) + ((((arg1[1]) as u64) * ((arg2[6]) as u64)) + ((((arg1[2]) as u64) * ((arg2[5]) as u64)) + ((((arg1[3]) as u64) * ((arg2[4]) as u64)) + ((((arg1[4]) as u64) * ((arg2[3]) as u64)) + ((((arg1[5]) as u64) * ((arg2[2]) as u64)) + ((((arg1[6]) as u64) * ((arg2[1]) as u64)) + (((arg1[7]) as u64) * ((arg2[0]) as u64))))))))) + ((x3 as u64) * (0x3d10 as u64)));
36  let x5: u32 = ((x4 >> 26) as u32);
37  let x6: u32 = ((x4 & (0x3ffffff as u64)) as u32);
38  let x7: u64 = ((x2 as u64) + (((arg1[9]) as u64) * ((arg2[9]) as u64)));
39  let x8: u32 = ((x7 >> 32) as u32);
40  let x9: u32 = ((x7 & (0xffffffff as u64)) as u32);
41  let x10: u64 = (((x5 as u64) + (((((arg1[0]) as u64) * ((arg2[8]) as u64)) + ((((arg1[1]) as u64) * ((arg2[7]) as u64)) + ((((arg1[2]) as u64) * ((arg2[6]) as u64)) + ((((arg1[3]) as u64) * ((arg2[5]) as u64)) + ((((arg1[4]) as u64) * ((arg2[4]) as u64)) + ((((arg1[5]) as u64) * ((arg2[3]) as u64)) + ((((arg1[6]) as u64) * ((arg2[2]) as u64)) + ((((arg1[7]) as u64) * ((arg2[1]) as u64)) + (((arg1[8]) as u64) * ((arg2[0]) as u64)))))))))) + ((x3 as u64) << 10))) + ((x9 as u64) * (0x3d10 as u64)));
42  let x11: u32 = ((x10 >> 26) as u32);
43  let x12: u32 = ((x10 & (0x3ffffff as u64)) as u32);
44  let x13: u64 = (((x11 as u64) + (((((arg1[0]) as u64) * ((arg2[9]) as u64)) + ((((arg1[1]) as u64) * ((arg2[8]) as u64)) + ((((arg1[2]) as u64) * ((arg2[7]) as u64)) + ((((arg1[3]) as u64) * ((arg2[6]) as u64)) + ((((arg1[4]) as u64) * ((arg2[5]) as u64)) + ((((arg1[5]) as u64) * ((arg2[4]) as u64)) + ((((arg1[6]) as u64) * ((arg2[3]) as u64)) + ((((arg1[7]) as u64) * ((arg2[2]) as u64)) + ((((arg1[8]) as u64) * ((arg2[1]) as u64)) + (((arg1[9]) as u64) * ((arg2[0]) as u64))))))))))) + ((x9 as u64) << 10))) + ((x8 as u64) * (0xf4400 as u64)));
45  let x14: u32 = ((x13 >> 26) as u32);
46  let x15: u32 = ((x13 & (0x3ffffff as u64)) as u32);
47  let x16: u64 = ((x14 as u64) + (((((arg1[1]) as u64) * ((arg2[9]) as u64)) + ((((arg1[2]) as u64) * ((arg2[8]) as u64)) + ((((arg1[3]) as u64) * ((arg2[7]) as u64)) + ((((arg1[4]) as u64) * ((arg2[6]) as u64)) + ((((arg1[5]) as u64) * ((arg2[5]) as u64)) + ((((arg1[6]) as u64) * ((arg2[4]) as u64)) + ((((arg1[7]) as u64) * ((arg2[3]) as u64)) + ((((arg1[8]) as u64) * ((arg2[2]) as u64)) + (((arg1[9]) as u64) * ((arg2[1]) as u64)))))))))) + ((x8 << 16) as u64)));
48  let x17: u32 = ((x16 >> 26) as u32);
49  let x18: u32 = ((x16 & (0x3ffffff as u64)) as u32);
50  let x19: u32 = (x15 >> 22);
51  let x20: u32 = (x15 & 0x3fffff);
52  let x21: u64 = ((((arg1[0]) as u64) * ((arg2[0]) as u64)) + (((x19 + (x18 << 4)) as u64) * (0x3d1 as u64)));
53  let x22: u32 = ((x21 >> 26) as u32);
54  let x23: u32 = ((x21 & (0x3ffffff as u64)) as u32);
55  let x24: u64 = ((x17 as u64) + ((((arg1[2]) as u64) * ((arg2[9]) as u64)) + ((((arg1[3]) as u64) * ((arg2[8]) as u64)) + ((((arg1[4]) as u64) * ((arg2[7]) as u64)) + ((((arg1[5]) as u64) * ((arg2[6]) as u64)) + ((((arg1[6]) as u64) * ((arg2[5]) as u64)) + ((((arg1[7]) as u64) * ((arg2[4]) as u64)) + ((((arg1[8]) as u64) * ((arg2[3]) as u64)) + (((arg1[9]) as u64) * ((arg2[2]) as u64))))))))));
56  let x25: u32 = ((x24 >> 26) as u32);
57  let x26: u32 = ((x24 & (0x3ffffff as u64)) as u32);
58  let x27: u64 = (((x22 as u64) + (((((arg1[0]) as u64) * ((arg2[1]) as u64)) + (((arg1[1]) as u64) * ((arg2[0]) as u64))) + (((x19 + (x18 << 4)) as u64) << 6))) + ((x26 as u64) * (0x3d10 as u64)));
59  let x28: u32 = ((x27 >> 26) as u32);
60  let x29: u32 = ((x27 & (0x3ffffff as u64)) as u32);
61  let x30: u64 = ((x25 as u64) + ((((arg1[3]) as u64) * ((arg2[9]) as u64)) + ((((arg1[4]) as u64) * ((arg2[8]) as u64)) + ((((arg1[5]) as u64) * ((arg2[7]) as u64)) + ((((arg1[6]) as u64) * ((arg2[6]) as u64)) + ((((arg1[7]) as u64) * ((arg2[5]) as u64)) + ((((arg1[8]) as u64) * ((arg2[4]) as u64)) + (((arg1[9]) as u64) * ((arg2[3]) as u64)))))))));
62  let x31: u32 = ((x30 >> 26) as u32);
63  let x32: u32 = ((x30 & (0x3ffffff as u64)) as u32);
64  let x33: u64 = (((x28 as u64) + (((((arg1[0]) as u64) * ((arg2[2]) as u64)) + ((((arg1[1]) as u64) * ((arg2[1]) as u64)) + (((arg1[2]) as u64) * ((arg2[0]) as u64)))) + ((x26 as u64) << 10))) + ((x32 as u64) * (0x3d10 as u64)));
65  let x34: u32 = ((x33 >> 26) as u32);
66  let x35: u32 = ((x33 & (0x3ffffff as u64)) as u32);
67  let x36: u64 = ((x31 as u64) + ((((arg1[4]) as u64) * ((arg2[9]) as u64)) + ((((arg1[5]) as u64) * ((arg2[8]) as u64)) + ((((arg1[6]) as u64) * ((arg2[7]) as u64)) + ((((arg1[7]) as u64) * ((arg2[6]) as u64)) + ((((arg1[8]) as u64) * ((arg2[5]) as u64)) + (((arg1[9]) as u64) * ((arg2[4]) as u64))))))));
68  let x37: u32 = ((x36 >> 26) as u32);
69  let x38: u32 = ((x36 & (0x3ffffff as u64)) as u32);
70  let x39: u64 = (((x34 as u64) + (((((arg1[0]) as u64) * ((arg2[3]) as u64)) + ((((arg1[1]) as u64) * ((arg2[2]) as u64)) + ((((arg1[2]) as u64) * ((arg2[1]) as u64)) + (((arg1[3]) as u64) * ((arg2[0]) as u64))))) + ((x32 as u64) << 10))) + ((x38 as u64) * (0x3d10 as u64)));
71  let x40: u32 = ((x39 >> 26) as u32);
72  let x41: u32 = ((x39 & (0x3ffffff as u64)) as u32);
73  let x42: u64 = ((x37 as u64) + ((((arg1[5]) as u64) * ((arg2[9]) as u64)) + ((((arg1[6]) as u64) * ((arg2[8]) as u64)) + ((((arg1[7]) as u64) * ((arg2[7]) as u64)) + ((((arg1[8]) as u64) * ((arg2[6]) as u64)) + (((arg1[9]) as u64) * ((arg2[5]) as u64)))))));
74  let x43: u32 = ((x42 >> 26) as u32);
75  let x44: u32 = ((x42 & (0x3ffffff as u64)) as u32);
76  let x45: u64 = (((x40 as u64) + (((((arg1[0]) as u64) * ((arg2[4]) as u64)) + ((((arg1[1]) as u64) * ((arg2[3]) as u64)) + ((((arg1[2]) as u64) * ((arg2[2]) as u64)) + ((((arg1[3]) as u64) * ((arg2[1]) as u64)) + (((arg1[4]) as u64) * ((arg2[0]) as u64)))))) + ((x38 as u64) << 10))) + ((x44 as u64) * (0x3d10 as u64)));
77  let x46: u32 = ((x45 >> 26) as u32);
78  let x47: u32 = ((x45 & (0x3ffffff as u64)) as u32);
79  let x48: u64 = ((x43 as u64) + ((((arg1[6]) as u64) * ((arg2[9]) as u64)) + ((((arg1[7]) as u64) * ((arg2[8]) as u64)) + ((((arg1[8]) as u64) * ((arg2[7]) as u64)) + (((arg1[9]) as u64) * ((arg2[6]) as u64))))));
80  let x49: u32 = ((x48 >> 26) as u32);
81  let x50: u32 = ((x48 & (0x3ffffff as u64)) as u32);
82  let x51: u64 = (((x46 as u64) + (((((arg1[0]) as u64) * ((arg2[5]) as u64)) + ((((arg1[1]) as u64) * ((arg2[4]) as u64)) + ((((arg1[2]) as u64) * ((arg2[3]) as u64)) + ((((arg1[3]) as u64) * ((arg2[2]) as u64)) + ((((arg1[4]) as u64) * ((arg2[1]) as u64)) + (((arg1[5]) as u64) * ((arg2[0]) as u64))))))) + ((x44 as u64) << 10))) + ((x50 as u64) * (0x3d10 as u64)));
83  let x52: u32 = ((x51 >> 26) as u32);
84  let x53: u32 = ((x51 & (0x3ffffff as u64)) as u32);
85  let x54: u64 = ((x49 as u64) + ((((arg1[7]) as u64) * ((arg2[9]) as u64)) + ((((arg1[8]) as u64) * ((arg2[8]) as u64)) + (((arg1[9]) as u64) * ((arg2[7]) as u64)))));
86  let x55: u32 = ((x54 >> 32) as u32);
87  let x56: u32 = ((x54 & (0xffffffff as u64)) as u32);
88  let x57: u64 = (((x52 as u64) + (((((arg1[0]) as u64) * ((arg2[6]) as u64)) + ((((arg1[1]) as u64) * ((arg2[5]) as u64)) + ((((arg1[2]) as u64) * ((arg2[4]) as u64)) + ((((arg1[3]) as u64) * ((arg2[3]) as u64)) + ((((arg1[4]) as u64) * ((arg2[2]) as u64)) + ((((arg1[5]) as u64) * ((arg2[1]) as u64)) + (((arg1[6]) as u64) * ((arg2[0]) as u64)))))))) + ((x50 as u64) << 10))) + ((x56 as u64) * (0x3d10 as u64)));
89  let x58: u32 = ((x57 >> 26) as u32);
90  let x59: u32 = ((x57 & (0x3ffffff as u64)) as u32);
91  let x60: u64 = (((x58 as u64) + ((x6 as u64) + ((x56 as u64) << 10))) + ((x55 as u64) * (0xf4400 as u64)));
92  let x61: u32 = ((x60 >> 26) as u32);
93  let x62: u32 = ((x60 & (0x3ffffff as u64)) as u32);
94  let x63: u64 = ((x61 as u64) + ((x12 as u64) + ((x55 as u64) << 16)));
95  let x64: u32 = ((x63 >> 26) as u32);
96  let x65: u32 = ((x63 & (0x3ffffff as u64)) as u32);
97  let x66: u32 = (x64 + x20);
98  out1[0] = x23;
99  out1[1] = x29;
100  out1[2] = x35;
101  out1[3] = x41;
102  out1[4] = x47;
103  out1[5] = x53;
104  out1[6] = x59;
105  out1[7] = x62;
106  out1[8] = x65;
107  out1[9] = x66;
108}
109
110/// The function fiat_secp256k1_dettman_square squares a field element.
111///
112/// Postconditions:
113///   eval out1 mod 115792089237316195423570985008687907853269984665640564039457584007908834671663 = (eval arg1 * eval arg1) mod 115792089237316195423570985008687907853269984665640564039457584007908834671663
114///
115/// Input Bounds:
116///   arg1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7ffffe]]
117/// Output Bounds:
118///   out1: [[0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x7fffffe], [0x0 ~> 0x5fffff]]
119#[inline]
120pub fn fiat_secp256k1_dettman_square(out1: &mut [u32; 10], arg1: &[u32; 10]) {
121  let x1: u32 = ((arg1[8]) * 0x2);
122  let x2: u32 = ((arg1[7]) * 0x2);
123  let x3: u32 = ((arg1[6]) * 0x2);
124  let x4: u32 = ((arg1[5]) * 0x2);
125  let x5: u32 = ((arg1[4]) * 0x2);
126  let x6: u32 = ((arg1[3]) * 0x2);
127  let x7: u32 = ((arg1[2]) * 0x2);
128  let x8: u32 = ((arg1[1]) * 0x2);
129  let x9: u32 = ((arg1[0]) * 0x2);
130  let x10: u64 = ((x1 as u64) * ((arg1[9]) as u64));
131  let x11: u32 = ((x10 >> 26) as u32);
132  let x12: u32 = ((x10 & (0x3ffffff as u64)) as u32);
133  let x13: u64 = ((((x9 as u64) * ((arg1[7]) as u64)) + (((x8 as u64) * ((arg1[6]) as u64)) + (((x7 as u64) * ((arg1[5]) as u64)) + ((x6 as u64) * ((arg1[4]) as u64))))) + ((x12 as u64) * (0x3d10 as u64)));
134  let x14: u32 = ((x13 >> 26) as u32);
135  let x15: u32 = ((x13 & (0x3ffffff as u64)) as u32);
136  let x16: u64 = ((x11 as u64) + (((arg1[9]) as u64) * ((arg1[9]) as u64)));
137  let x17: u32 = ((x16 >> 32) as u32);
138  let x18: u32 = ((x16 & (0xffffffff as u64)) as u32);
139  let x19: u64 = (((x14 as u64) + ((((x9 as u64) * ((arg1[8]) as u64)) + (((x8 as u64) * ((arg1[7]) as u64)) + (((x7 as u64) * ((arg1[6]) as u64)) + (((x6 as u64) * ((arg1[5]) as u64)) + (((arg1[4]) as u64) * ((arg1[4]) as u64)))))) + ((x12 as u64) << 10))) + ((x18 as u64) * (0x3d10 as u64)));
140  let x20: u32 = ((x19 >> 26) as u32);
141  let x21: u32 = ((x19 & (0x3ffffff as u64)) as u32);
142  let x22: u64 = (((x20 as u64) + ((((x9 as u64) * ((arg1[9]) as u64)) + (((x8 as u64) * ((arg1[8]) as u64)) + (((x7 as u64) * ((arg1[7]) as u64)) + (((x6 as u64) * ((arg1[6]) as u64)) + ((x5 as u64) * ((arg1[5]) as u64)))))) + ((x18 as u64) << 10))) + ((x17 as u64) * (0xf4400 as u64)));
143  let x23: u32 = ((x22 >> 26) as u32);
144  let x24: u32 = ((x22 & (0x3ffffff as u64)) as u32);
145  let x25: u64 = ((x23 as u64) + ((((x8 as u64) * ((arg1[9]) as u64)) + (((x7 as u64) * ((arg1[8]) as u64)) + (((x6 as u64) * ((arg1[7]) as u64)) + (((x5 as u64) * ((arg1[6]) as u64)) + (((arg1[5]) as u64) * ((arg1[5]) as u64)))))) + ((x17 << 16) as u64)));
146  let x26: u32 = ((x25 >> 26) as u32);
147  let x27: u32 = ((x25 & (0x3ffffff as u64)) as u32);
148  let x28: u32 = (x24 >> 22);
149  let x29: u32 = (x24 & 0x3fffff);
150  let x30: u64 = ((((arg1[0]) as u64) * ((arg1[0]) as u64)) + (((x28 + (x27 << 4)) as u64) * (0x3d1 as u64)));
151  let x31: u32 = ((x30 >> 26) as u32);
152  let x32: u32 = ((x30 & (0x3ffffff as u64)) as u32);
153  let x33: u64 = ((x26 as u64) + (((x7 as u64) * ((arg1[9]) as u64)) + (((x6 as u64) * ((arg1[8]) as u64)) + (((x5 as u64) * ((arg1[7]) as u64)) + ((x4 as u64) * ((arg1[6]) as u64))))));
154  let x34: u32 = ((x33 >> 26) as u32);
155  let x35: u32 = ((x33 & (0x3ffffff as u64)) as u32);
156  let x36: u64 = (((x31 as u64) + (((x9 as u64) * ((arg1[1]) as u64)) + (((x28 + (x27 << 4)) as u64) << 6))) + ((x35 as u64) * (0x3d10 as u64)));
157  let x37: u32 = ((x36 >> 26) as u32);
158  let x38: u32 = ((x36 & (0x3ffffff as u64)) as u32);
159  let x39: u64 = ((x34 as u64) + (((x6 as u64) * ((arg1[9]) as u64)) + (((x5 as u64) * ((arg1[8]) as u64)) + (((x4 as u64) * ((arg1[7]) as u64)) + (((arg1[6]) as u64) * ((arg1[6]) as u64))))));
160  let x40: u32 = ((x39 >> 26) as u32);
161  let x41: u32 = ((x39 & (0x3ffffff as u64)) as u32);
162  let x42: u64 = (((x37 as u64) + ((((x9 as u64) * ((arg1[2]) as u64)) + (((arg1[1]) as u64) * ((arg1[1]) as u64))) + ((x35 as u64) << 10))) + ((x41 as u64) * (0x3d10 as u64)));
163  let x43: u32 = ((x42 >> 26) as u32);
164  let x44: u32 = ((x42 & (0x3ffffff as u64)) as u32);
165  let x45: u64 = ((x40 as u64) + (((x5 as u64) * ((arg1[9]) as u64)) + (((x4 as u64) * ((arg1[8]) as u64)) + ((x3 as u64) * ((arg1[7]) as u64)))));
166  let x46: u32 = ((x45 >> 26) as u32);
167  let x47: u32 = ((x45 & (0x3ffffff as u64)) as u32);
168  let x48: u64 = (((x43 as u64) + ((((x9 as u64) * ((arg1[3]) as u64)) + ((x8 as u64) * ((arg1[2]) as u64))) + ((x41 as u64) << 10))) + ((x47 as u64) * (0x3d10 as u64)));
169  let x49: u32 = ((x48 >> 26) as u32);
170  let x50: u32 = ((x48 & (0x3ffffff as u64)) as u32);
171  let x51: u64 = ((x46 as u64) + (((x4 as u64) * ((arg1[9]) as u64)) + (((x3 as u64) * ((arg1[8]) as u64)) + (((arg1[7]) as u64) * ((arg1[7]) as u64)))));
172  let x52: u32 = ((x51 >> 26) as u32);
173  let x53: u32 = ((x51 & (0x3ffffff as u64)) as u32);
174  let x54: u64 = (((x49 as u64) + ((((x9 as u64) * ((arg1[4]) as u64)) + (((x8 as u64) * ((arg1[3]) as u64)) + (((arg1[2]) as u64) * ((arg1[2]) as u64)))) + ((x47 as u64) << 10))) + ((x53 as u64) * (0x3d10 as u64)));
175  let x55: u32 = ((x54 >> 26) as u32);
176  let x56: u32 = ((x54 & (0x3ffffff as u64)) as u32);
177  let x57: u64 = ((x52 as u64) + (((x3 as u64) * ((arg1[9]) as u64)) + ((x2 as u64) * ((arg1[8]) as u64))));
178  let x58: u32 = ((x57 >> 26) as u32);
179  let x59: u32 = ((x57 & (0x3ffffff as u64)) as u32);
180  let x60: u64 = (((x55 as u64) + ((((x9 as u64) * ((arg1[5]) as u64)) + (((x8 as u64) * ((arg1[4]) as u64)) + ((x7 as u64) * ((arg1[3]) as u64)))) + ((x53 as u64) << 10))) + ((x59 as u64) * (0x3d10 as u64)));
181  let x61: u32 = ((x60 >> 26) as u32);
182  let x62: u32 = ((x60 & (0x3ffffff as u64)) as u32);
183  let x63: u64 = ((x58 as u64) + (((x2 as u64) * ((arg1[9]) as u64)) + (((arg1[8]) as u64) * ((arg1[8]) as u64))));
184  let x64: u32 = ((x63 >> 32) as u32);
185  let x65: u32 = ((x63 & (0xffffffff as u64)) as u32);
186  let x66: u64 = (((x61 as u64) + ((((x9 as u64) * ((arg1[6]) as u64)) + (((x8 as u64) * ((arg1[5]) as u64)) + (((x7 as u64) * ((arg1[4]) as u64)) + (((arg1[3]) as u64) * ((arg1[3]) as u64))))) + ((x59 as u64) << 10))) + ((x65 as u64) * (0x3d10 as u64)));
187  let x67: u32 = ((x66 >> 26) as u32);
188  let x68: u32 = ((x66 & (0x3ffffff as u64)) as u32);
189  let x69: u64 = (((x67 as u64) + ((x15 as u64) + ((x65 as u64) << 10))) + ((x64 as u64) * (0xf4400 as u64)));
190  let x70: u32 = ((x69 >> 26) as u32);
191  let x71: u32 = ((x69 & (0x3ffffff as u64)) as u32);
192  let x72: u64 = ((x70 as u64) + ((x21 as u64) + ((x64 as u64) << 16)));
193  let x73: u32 = ((x72 >> 26) as u32);
194  let x74: u32 = ((x72 & (0x3ffffff as u64)) as u32);
195  let x75: u32 = (x73 + x29);
196  out1[0] = x32;
197  out1[1] = x38;
198  out1[2] = x44;
199  out1[3] = x50;
200  out1[4] = x56;
201  out1[5] = x62;
202  out1[6] = x68;
203  out1[7] = x71;
204  out1[8] = x74;
205  out1[9] = x75;
206}
fiat_crypto/secp256k1_dettman_32.rs

fiat_crypto/
secp256k1_dettman_32.rs
