1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
λ x x0 : word64 * word64 * word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x8, x9, x7, x5, (x14, x15, x13, x11))%core,
uint128_t x16 = (uint128_t) x5 * x11;
uint64_t x17 = (uint64_t) x16 & 0xffffffffffffffffL;
uint64_t x18 = (uint64_t) (x16 >> 0x40);
uint128_t x19 = (uint128_t) x5 * x13;
uint64_t x20 = (uint64_t) x19 & 0xffffffffffffffffL;
uint64_t x21 = (uint64_t) (x19 >> 0x40);
uint128_t x22 = (uint128_t) x5 * x15;
uint64_t x23 = (uint64_t) x22 & 0xffffffffffffffffL;
uint64_t x24 = (uint64_t) (x22 >> 0x40);
uint128_t x25 = (uint128_t) x5 * x14;
uint64_t x26 = (uint64_t) x25 & 0xffffffffffffffffL;
uint64_t x27 = (uint64_t) (x25 >> 0x40);
uint64_t x29, uint8_t x30 = addcarryx_u64(0x0, x18, x20);
uint64_t x32, uint8_t x33 = addcarryx_u64(x30, x21, x23);
uint64_t x35, uint8_t x36 = addcarryx_u64(x33, x24, x26);
uint64_t x38, uint8_t _ = addcarryx_u64(0x0, x36, x27);
uint64_t x40 = x17 & 0xffffffffffffffffL;
uint128_t x41 = (uint128_t) x40 * 0xffffffffffffffffL;
uint64_t x42 = (uint64_t) x41 & 0xffffffffffffffffL;
uint64_t x43 = (uint64_t) (x41 >> 0x40);
uint128_t x44 = (uint128_t) x40 * 0xffffffff;
uint64_t x45 = (uint64_t) x44 & 0xffffffffffffffffL;
uint64_t x46 = (uint64_t) (x44 >> 0x40);
uint128_t x47 = (uint128_t) x40 * 0xffffffff00000001L;
uint64_t x48 = (uint64_t) x47 & 0xffffffffffffffffL;
uint64_t x49 = (uint64_t) (x47 >> 0x40);
uint64_t x51, uint8_t x52 = addcarryx_u64(0x0, x43, x45);
uint64_t x54, uint8_t x55 = addcarryx_u64(x52, x46, 0x0);
uint64_t x57, uint8_t x58 = addcarryx_u64(x55, 0x0, x48);
uint64_t x60, uint8_t _ = addcarryx_u64(0x0, x58, x49);
uint64_t _, uint8_t x64 = addcarryx_u64(0x0, x17, x42);
uint64_t x66, uint8_t x67 = addcarryx_u64(x64, x29, x51);
uint64_t x69, uint8_t x70 = addcarryx_u64(x67, x32, x54);
uint64_t x72, uint8_t x73 = addcarryx_u64(x70, x35, x57);
uint64_t x75, uint8_t x76 = addcarryx_u64(x73, x38, x60);
uint128_t x77 = (uint128_t) x7 * x11;
uint64_t x78 = (uint64_t) x77 & 0xffffffffffffffffL;
uint64_t x79 = (uint64_t) (x77 >> 0x40);
uint128_t x80 = (uint128_t) x7 * x13;
uint64_t x81 = (uint64_t) x80 & 0xffffffffffffffffL;
uint64_t x82 = (uint64_t) (x80 >> 0x40);
uint128_t x83 = (uint128_t) x7 * x15;
uint64_t x84 = (uint64_t) x83 & 0xffffffffffffffffL;
uint64_t x85 = (uint64_t) (x83 >> 0x40);
uint128_t x86 = (uint128_t) x7 * x14;
uint64_t x87 = (uint64_t) x86 & 0xffffffffffffffffL;
uint64_t x88 = (uint64_t) (x86 >> 0x40);
uint64_t x90, uint8_t x91 = addcarryx_u64(0x0, x79, x81);
uint64_t x93, uint8_t x94 = addcarryx_u64(x91, x82, x84);
uint64_t x96, uint8_t x97 = addcarryx_u64(x94, x85, x87);
uint64_t x99, uint8_t _ = addcarryx_u64(0x0, x97, x88);
uint64_t x102, uint8_t x103 = addcarryx_u64(0x0, x66, x78);
uint64_t x105, uint8_t x106 = addcarryx_u64(x103, x69, x90);
uint64_t x108, uint8_t x109 = addcarryx_u64(x106, x72, x93);
uint64_t x111, uint8_t x112 = addcarryx_u64(x109, x75, x96);
uint64_t x114, uint8_t x115 = addcarryx_u64(x112, x76, x99);
uint64_t x116 = x102 & 0xffffffffffffffffL;
uint128_t x117 = (uint128_t) x116 * 0xffffffffffffffffL;
uint64_t x118 = (uint64_t) x117 & 0xffffffffffffffffL;
uint64_t x119 = (uint64_t) (x117 >> 0x40);
uint128_t x120 = (uint128_t) x116 * 0xffffffff;
uint64_t x121 = (uint64_t) x120 & 0xffffffffffffffffL;
uint64_t x122 = (uint64_t) (x120 >> 0x40);
uint128_t x123 = (uint128_t) x116 * 0xffffffff00000001L;
uint64_t x124 = (uint64_t) x123 & 0xffffffffffffffffL;
uint64_t x125 = (uint64_t) (x123 >> 0x40);
uint64_t x127, uint8_t x128 = addcarryx_u64(0x0, x119, x121);
uint64_t x130, uint8_t x131 = addcarryx_u64(x128, x122, 0x0);
uint64_t x133, uint8_t x134 = addcarryx_u64(x131, 0x0, x124);
uint64_t x136, uint8_t _ = addcarryx_u64(0x0, x134, x125);
uint64_t _, uint8_t x140 = addcarryx_u64(0x0, x102, x118);
uint64_t x142, uint8_t x143 = addcarryx_u64(x140, x105, x127);
uint64_t x145, uint8_t x146 = addcarryx_u64(x143, x108, x130);
uint64_t x148, uint8_t x149 = addcarryx_u64(x146, x111, x133);
uint64_t x151, uint8_t x152 = addcarryx_u64(x149, x114, x136);
uint8_t x153 = x152 + x115;
uint128_t x154 = (uint128_t) x9 * x11;
uint64_t x155 = (uint64_t) x154 & 0xffffffffffffffffL;
uint64_t x156 = (uint64_t) (x154 >> 0x40);
uint128_t x157 = (uint128_t) x9 * x13;
uint64_t x158 = (uint64_t) x157 & 0xffffffffffffffffL;
uint64_t x159 = (uint64_t) (x157 >> 0x40);
uint128_t x160 = (uint128_t) x9 * x15;
uint64_t x161 = (uint64_t) x160 & 0xffffffffffffffffL;
uint64_t x162 = (uint64_t) (x160 >> 0x40);
uint128_t x163 = (uint128_t) x9 * x14;
uint64_t x164 = (uint64_t) x163 & 0xffffffffffffffffL;
uint64_t x165 = (uint64_t) (x163 >> 0x40);
uint64_t x167, uint8_t x168 = addcarryx_u64(0x0, x156, x158);
uint64_t x170, uint8_t x171 = addcarryx_u64(x168, x159, x161);
uint64_t x173, uint8_t x174 = addcarryx_u64(x171, x162, x164);
uint64_t x176, uint8_t _ = addcarryx_u64(0x0, x174, x165);
uint64_t x179, uint8_t x180 = addcarryx_u64(0x0, x142, x155);
uint64_t x182, uint8_t x183 = addcarryx_u64(x180, x145, x167);
uint64_t x185, uint8_t x186 = addcarryx_u64(x183, x148, x170);
uint64_t x188, uint8_t x189 = addcarryx_u64(x186, x151, x173);
uint64_t x191, uint8_t x192 = addcarryx_u64(x189, x153, x176);
uint64_t x193 = x179 & 0xffffffffffffffffL;
uint128_t x194 = (uint128_t) x193 * 0xffffffffffffffffL;
uint64_t x195 = (uint64_t) x194 & 0xffffffffffffffffL;
uint64_t x196 = (uint64_t) (x194 >> 0x40);
uint128_t x197 = (uint128_t) x193 * 0xffffffff;
uint64_t x198 = (uint64_t) x197 & 0xffffffffffffffffL;
uint64_t x199 = (uint64_t) (x197 >> 0x40);
uint128_t x200 = (uint128_t) x193 * 0xffffffff00000001L;
uint64_t x201 = (uint64_t) x200 & 0xffffffffffffffffL;
uint64_t x202 = (uint64_t) (x200 >> 0x40);
uint64_t x204, uint8_t x205 = addcarryx_u64(0x0, x196, x198);
uint64_t x207, uint8_t x208 = addcarryx_u64(x205, x199, 0x0);
uint64_t x210, uint8_t x211 = addcarryx_u64(x208, 0x0, x201);
uint64_t x213, uint8_t _ = addcarryx_u64(0x0, x211, x202);
uint64_t _, uint8_t x217 = addcarryx_u64(0x0, x179, x195);
uint64_t x219, uint8_t x220 = addcarryx_u64(x217, x182, x204);
uint64_t x222, uint8_t x223 = addcarryx_u64(x220, x185, x207);
uint64_t x225, uint8_t x226 = addcarryx_u64(x223, x188, x210);
uint64_t x228, uint8_t x229 = addcarryx_u64(x226, x191, x213);
uint8_t x230 = x229 + x192;
uint128_t x231 = (uint128_t) x8 * x11;
uint64_t x232 = (uint64_t) x231 & 0xffffffffffffffffL;
uint64_t x233 = (uint64_t) (x231 >> 0x40);
uint128_t x234 = (uint128_t) x8 * x13;
uint64_t x235 = (uint64_t) x234 & 0xffffffffffffffffL;
uint64_t x236 = (uint64_t) (x234 >> 0x40);
uint128_t x237 = (uint128_t) x8 * x15;
uint64_t x238 = (uint64_t) x237 & 0xffffffffffffffffL;
uint64_t x239 = (uint64_t) (x237 >> 0x40);
uint128_t x240 = (uint128_t) x8 * x14;
uint64_t x241 = (uint64_t) x240 & 0xffffffffffffffffL;
uint64_t x242 = (uint64_t) (x240 >> 0x40);
uint64_t x244, uint8_t x245 = addcarryx_u64(0x0, x233, x235);
uint64_t x247, uint8_t x248 = addcarryx_u64(x245, x236, x238);
uint64_t x250, uint8_t x251 = addcarryx_u64(x248, x239, x241);
uint64_t x253, uint8_t _ = addcarryx_u64(0x0, x251, x242);
uint64_t x256, uint8_t x257 = addcarryx_u64(0x0, x219, x232);
uint64_t x259, uint8_t x260 = addcarryx_u64(x257, x222, x244);
uint64_t x262, uint8_t x263 = addcarryx_u64(x260, x225, x247);
uint64_t x265, uint8_t x266 = addcarryx_u64(x263, x228, x250);
uint64_t x268, uint8_t _ = addcarryx_u64(x266, x230, x253);
uint64_t x270 = x256 & 0xffffffffffffffffL;
uint128_t x271 = (uint128_t) x270 * 0xffffffffffffffffL;
uint64_t x272 = (uint64_t) x271 & 0xffffffffffffffffL;
uint64_t x273 = (uint64_t) (x271 >> 0x40);
uint128_t x274 = (uint128_t) x270 * 0xffffffff;
uint64_t x275 = (uint64_t) x274 & 0xffffffffffffffffL;
uint64_t x276 = (uint64_t) (x274 >> 0x40);
uint128_t x277 = (uint128_t) x270 * 0xffffffff00000001L;
uint64_t x278 = (uint64_t) x277 & 0xffffffffffffffffL;
uint64_t x279 = (uint64_t) (x277 >> 0x40);
uint64_t x281, uint8_t x282 = addcarryx_u64(0x0, x273, x275);
uint64_t x284, uint8_t x285 = addcarryx_u64(x282, x276, 0x0);
uint64_t x287, uint8_t x288 = addcarryx_u64(x285, 0x0, x278);
uint64_t x290, uint8_t _ = addcarryx_u64(0x0, x288, x279);
uint64_t _, uint8_t x294 = addcarryx_u64(0x0, x256, x272);
uint64_t x296, uint8_t x297 = addcarryx_u64(x294, x259, x281);
uint64_t x299, uint8_t x300 = addcarryx_u64(x297, x262, x284);
uint64_t x302, uint8_t x303 = addcarryx_u64(x300, x265, x287);
uint64_t x305, uint8_t _ = addcarryx_u64(x303, x268, x290);
(Return x305, Return x302, Return x299, Return x296))
(x, x0)%core
: word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t)
|
