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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
|
λ x x0 x1 x2 x3 : word128 * word128 * word128,
let (a, b) := Interp-η
(λ var : Syntax.base_type → Type,
λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core,
uint128_t x33 = (x17 + x21);
uint128_t x34 = (x18 + x22);
uint128_t x35 = (x16 + x20);
uint128_t x36 = ((0x3ffffffffffffffffffffeL + x17) - x21);
uint128_t x37 = ((0x3ffffffffffffffffffffeL + x18) - x22);
uint128_t x38 = ((0x3ffffffffffffffffffff6L + x16) - x20);
uint256_t x39 = (((uint256_t)x35 * x33) + (((uint256_t)x34 * x34) + ((uint256_t)x33 * x35)));
uint256_t x40 = ((((uint256_t)x35 * x34) + ((uint256_t)x34 * x35)) + (0x5 * ((uint256_t)x33 * x33)));
uint256_t x41 = (((uint256_t)x35 * x35) + (0x5 * (((uint256_t)x34 * x33) + ((uint256_t)x33 * x34))));
uint128_t x42 = (uint128_t) (x41 >> 0x55);
uint128_t x43 = ((uint128_t)x41 & 0x1fffffffffffffffffffffL);
uint256_t x44 = (x42 + x40);
uint128_t x45 = (uint128_t) (x44 >> 0x55);
uint128_t x46 = ((uint128_t)x44 & 0x1fffffffffffffffffffffL);
uint256_t x47 = (x45 + x39);
uint128_t x48 = (uint128_t) (x47 >> 0x55);
uint128_t x49 = ((uint128_t)x47 & 0x1fffffffffffffffffffffL);
uint128_t x50 = (x43 + (0x5 * x48));
uint128_t x51 = (x50 >> 0x55);
uint128_t x52 = (x50 & 0x1fffffffffffffffffffffL);
uint128_t x53 = (x51 + x46);
uint128_t x54 = (x53 >> 0x55);
uint128_t x55 = (x53 & 0x1fffffffffffffffffffffL);
uint128_t x56 = (x54 + x49);
uint256_t x57 = (((uint256_t)x38 * x36) + (((uint256_t)x37 * x37) + ((uint256_t)x36 * x38)));
uint256_t x58 = ((((uint256_t)x38 * x37) + ((uint256_t)x37 * x38)) + (0x5 * ((uint256_t)x36 * x36)));
uint256_t x59 = (((uint256_t)x38 * x38) + (0x5 * (((uint256_t)x37 * x36) + ((uint256_t)x36 * x37))));
uint128_t x60 = (uint128_t) (x59 >> 0x55);
uint128_t x61 = ((uint128_t)x59 & 0x1fffffffffffffffffffffL);
uint256_t x62 = (x60 + x58);
uint128_t x63 = (uint128_t) (x62 >> 0x55);
uint128_t x64 = ((uint128_t)x62 & 0x1fffffffffffffffffffffL);
uint256_t x65 = (x63 + x57);
uint128_t x66 = (uint128_t) (x65 >> 0x55);
uint128_t x67 = ((uint128_t)x65 & 0x1fffffffffffffffffffffL);
uint128_t x68 = (x61 + (0x5 * x66));
uint128_t x69 = (x68 >> 0x55);
uint128_t x70 = (x68 & 0x1fffffffffffffffffffffL);
uint128_t x71 = (x69 + x64);
uint128_t x72 = (x71 >> 0x55);
uint128_t x73 = (x71 & 0x1fffffffffffffffffffffL);
uint128_t x74 = (x72 + x67);
uint256_t x75 = (((uint256_t)x52 * x74) + (((uint256_t)x55 * x73) + ((uint256_t)x56 * x70)));
uint256_t x76 = ((((uint256_t)x52 * x73) + ((uint256_t)x55 * x70)) + (0x5 * ((uint256_t)x56 * x74)));
uint256_t x77 = (((uint256_t)x52 * x70) + (0x5 * (((uint256_t)x55 * x74) + ((uint256_t)x56 * x73))));
uint128_t x78 = (uint128_t) (x77 >> 0x55);
uint128_t x79 = ((uint128_t)x77 & 0x1fffffffffffffffffffffL);
uint256_t x80 = (x78 + x76);
uint128_t x81 = (uint128_t) (x80 >> 0x55);
uint128_t x82 = ((uint128_t)x80 & 0x1fffffffffffffffffffffL);
uint256_t x83 = (x81 + x75);
uint128_t x84 = (uint128_t) (x83 >> 0x55);
uint128_t x85 = ((uint128_t)x83 & 0x1fffffffffffffffffffffL);
uint128_t x86 = (x79 + (0x5 * x84));
uint128_t x87 = (x86 >> 0x55);
uint128_t x88 = (x86 & 0x1fffffffffffffffffffffL);
uint128_t x89 = (x87 + x82);
uint128_t x90 = (x89 >> 0x55);
uint128_t x91 = (x89 & 0x1fffffffffffffffffffffL);
uint128_t x92 = (x90 + x85);
uint128_t x93 = ((0x3ffffffffffffffffffffeL + x56) - x74);
uint128_t x94 = ((0x3ffffffffffffffffffffeL + x55) - x73);
uint128_t x95 = ((0x3ffffffffffffffffffff6L + x52) - x70);
uint128_t x96 = (0x1db41 * x93);
uint128_t x97 = (0x1db41 * x94);
uint128_t x98 = (0x1db41 * x95);
uint128_t x99 = (x98 >> 0x55);
uint128_t x100 = (x98 & 0x1fffffffffffffffffffffL);
uint128_t x101 = (x99 + x97);
uint128_t x102 = (x101 >> 0x55);
uint128_t x103 = (x101 & 0x1fffffffffffffffffffffL);
uint128_t x104 = (x102 + x96);
uint128_t x105 = (x104 >> 0x55);
uint128_t x106 = (x104 & 0x1fffffffffffffffffffffL);
uint128_t x107 = (x100 + (0x5 * x105));
uint128_t x108 = (x107 >> 0x55);
uint128_t x109 = (x107 & 0x1fffffffffffffffffffffL);
uint128_t x110 = (x108 + x103);
uint128_t x111 = (x110 >> 0x55);
uint128_t x112 = (x110 & 0x1fffffffffffffffffffffL);
uint128_t x113 = (x111 + x106);
uint128_t x114 = (x56 + x113);
uint128_t x115 = (x55 + x112);
uint128_t x116 = (x52 + x109);
uint256_t x117 = (((uint256_t)x95 * x114) + (((uint256_t)x94 * x115) + ((uint256_t)x93 * x116)));
uint256_t x118 = ((((uint256_t)x95 * x115) + ((uint256_t)x94 * x116)) + (0x5 * ((uint256_t)x93 * x114)));
uint256_t x119 = (((uint256_t)x95 * x116) + (0x5 * (((uint256_t)x94 * x114) + ((uint256_t)x93 * x115))));
uint128_t x120 = (uint128_t) (x119 >> 0x55);
uint128_t x121 = ((uint128_t)x119 & 0x1fffffffffffffffffffffL);
uint256_t x122 = (x120 + x118);
uint128_t x123 = (uint128_t) (x122 >> 0x55);
uint128_t x124 = ((uint128_t)x122 & 0x1fffffffffffffffffffffL);
uint256_t x125 = (x123 + x117);
uint128_t x126 = (uint128_t) (x125 >> 0x55);
uint128_t x127 = ((uint128_t)x125 & 0x1fffffffffffffffffffffL);
uint128_t x128 = (x121 + (0x5 * x126));
uint128_t x129 = (x128 >> 0x55);
uint128_t x130 = (x128 & 0x1fffffffffffffffffffffL);
uint128_t x131 = (x129 + x124);
uint128_t x132 = (x131 >> 0x55);
uint128_t x133 = (x131 & 0x1fffffffffffffffffffffL);
uint128_t x134 = (x132 + x127);
uint128_t x135 = (x27 + x31);
uint128_t x136 = (x28 + x32);
uint128_t x137 = (x26 + x30);
uint128_t x138 = ((0x3ffffffffffffffffffffeL + x27) - x31);
uint128_t x139 = ((0x3ffffffffffffffffffffeL + x28) - x32);
uint128_t x140 = ((0x3ffffffffffffffffffff6L + x26) - x30);
uint256_t x141 = (((uint256_t)x137 * x36) + (((uint256_t)x136 * x37) + ((uint256_t)x135 * x38)));
uint256_t x142 = ((((uint256_t)x137 * x37) + ((uint256_t)x136 * x38)) + (0x5 * ((uint256_t)x135 * x36)));
uint256_t x143 = (((uint256_t)x137 * x38) + (0x5 * (((uint256_t)x136 * x36) + ((uint256_t)x135 * x37))));
uint128_t x144 = (uint128_t) (x143 >> 0x55);
uint128_t x145 = ((uint128_t)x143 & 0x1fffffffffffffffffffffL);
uint256_t x146 = (x144 + x142);
uint128_t x147 = (uint128_t) (x146 >> 0x55);
uint128_t x148 = ((uint128_t)x146 & 0x1fffffffffffffffffffffL);
uint256_t x149 = (x147 + x141);
uint128_t x150 = (uint128_t) (x149 >> 0x55);
uint128_t x151 = ((uint128_t)x149 & 0x1fffffffffffffffffffffL);
uint128_t x152 = (x145 + (0x5 * x150));
uint128_t x153 = (x152 >> 0x55);
uint128_t x154 = (x152 & 0x1fffffffffffffffffffffL);
uint128_t x155 = (x153 + x148);
uint128_t x156 = (x155 >> 0x55);
uint128_t x157 = (x155 & 0x1fffffffffffffffffffffL);
uint128_t x158 = (x156 + x151);
uint256_t x159 = (((uint256_t)x140 * x33) + (((uint256_t)x139 * x34) + ((uint256_t)x138 * x35)));
uint256_t x160 = ((((uint256_t)x140 * x34) + ((uint256_t)x139 * x35)) + (0x5 * ((uint256_t)x138 * x33)));
uint256_t x161 = (((uint256_t)x140 * x35) + (0x5 * (((uint256_t)x139 * x33) + ((uint256_t)x138 * x34))));
uint128_t x162 = (uint128_t) (x161 >> 0x55);
uint128_t x163 = ((uint128_t)x161 & 0x1fffffffffffffffffffffL);
uint256_t x164 = (x162 + x160);
uint128_t x165 = (uint128_t) (x164 >> 0x55);
uint128_t x166 = ((uint128_t)x164 & 0x1fffffffffffffffffffffL);
uint256_t x167 = (x165 + x159);
uint128_t x168 = (uint128_t) (x167 >> 0x55);
uint128_t x169 = ((uint128_t)x167 & 0x1fffffffffffffffffffffL);
uint128_t x170 = (x163 + (0x5 * x168));
uint128_t x171 = (x170 >> 0x55);
uint128_t x172 = (x170 & 0x1fffffffffffffffffffffL);
uint128_t x173 = (x171 + x166);
uint128_t x174 = (x173 >> 0x55);
uint128_t x175 = (x173 & 0x1fffffffffffffffffffffL);
uint128_t x176 = (x174 + x169);
uint128_t x177 = (x176 + x158);
uint128_t x178 = (x175 + x157);
uint128_t x179 = (x172 + x154);
uint128_t x180 = (x176 + x158);
uint128_t x181 = (x175 + x157);
uint128_t x182 = (x172 + x154);
uint256_t x183 = (((uint256_t)x179 * x180) + (((uint256_t)x178 * x181) + ((uint256_t)x177 * x182)));
uint256_t x184 = ((((uint256_t)x179 * x181) + ((uint256_t)x178 * x182)) + (0x5 * ((uint256_t)x177 * x180)));
uint256_t x185 = (((uint256_t)x179 * x182) + (0x5 * (((uint256_t)x178 * x180) + ((uint256_t)x177 * x181))));
uint128_t x186 = (uint128_t) (x185 >> 0x55);
uint128_t x187 = ((uint128_t)x185 & 0x1fffffffffffffffffffffL);
uint256_t x188 = (x186 + x184);
uint128_t x189 = (uint128_t) (x188 >> 0x55);
uint128_t x190 = ((uint128_t)x188 & 0x1fffffffffffffffffffffL);
uint256_t x191 = (x189 + x183);
uint128_t x192 = (uint128_t) (x191 >> 0x55);
uint128_t x193 = ((uint128_t)x191 & 0x1fffffffffffffffffffffL);
uint128_t x194 = (x187 + (0x5 * x192));
uint128_t x195 = (x194 >> 0x55);
uint128_t x196 = (x194 & 0x1fffffffffffffffffffffL);
uint128_t x197 = (x195 + x190);
uint128_t x198 = (x197 >> 0x55);
uint128_t x199 = (x197 & 0x1fffffffffffffffffffffL);
uint128_t x200 = (x198 + x193);
uint128_t x201 = ((0x3ffffffffffffffffffffeL + x176) - x158);
uint128_t x202 = ((0x3ffffffffffffffffffffeL + x175) - x157);
uint128_t x203 = ((0x3ffffffffffffffffffff6L + x172) - x154);
uint128_t x204 = ((0x3ffffffffffffffffffffeL + x176) - x158);
uint128_t x205 = ((0x3ffffffffffffffffffffeL + x175) - x157);
uint128_t x206 = ((0x3ffffffffffffffffffff6L + x172) - x154);
uint256_t x207 = (((uint256_t)x203 * x204) + (((uint256_t)x202 * x205) + ((uint256_t)x201 * x206)));
uint256_t x208 = ((((uint256_t)x203 * x205) + ((uint256_t)x202 * x206)) + (0x5 * ((uint256_t)x201 * x204)));
uint256_t x209 = (((uint256_t)x203 * x206) + (0x5 * (((uint256_t)x202 * x204) + ((uint256_t)x201 * x205))));
uint128_t x210 = (uint128_t) (x209 >> 0x55);
uint128_t x211 = ((uint128_t)x209 & 0x1fffffffffffffffffffffL);
uint256_t x212 = (x210 + x208);
uint128_t x213 = (uint128_t) (x212 >> 0x55);
uint128_t x214 = ((uint128_t)x212 & 0x1fffffffffffffffffffffL);
uint256_t x215 = (x213 + x207);
uint128_t x216 = (uint128_t) (x215 >> 0x55);
uint128_t x217 = ((uint128_t)x215 & 0x1fffffffffffffffffffffL);
uint128_t x218 = (x211 + (0x5 * x216));
uint128_t x219 = (x218 >> 0x55);
uint128_t x220 = (x218 & 0x1fffffffffffffffffffffL);
uint128_t x221 = (x219 + x214);
uint128_t x222 = (x221 >> 0x55);
uint128_t x223 = (x221 & 0x1fffffffffffffffffffffL);
uint128_t x224 = (x222 + x217);
uint256_t x225 = (((uint256_t)x10 * x224) + (((uint256_t)x12 * x223) + ((uint256_t)x11 * x220)));
uint256_t x226 = ((((uint256_t)x10 * x223) + ((uint256_t)x12 * x220)) + (0x5 * ((uint256_t)x11 * x224)));
uint256_t x227 = (((uint256_t)x10 * x220) + (0x5 * (((uint256_t)x12 * x224) + ((uint256_t)x11 * x223))));
uint128_t x228 = (uint128_t) (x227 >> 0x55);
uint128_t x229 = ((uint128_t)x227 & 0x1fffffffffffffffffffffL);
uint256_t x230 = (x228 + x226);
uint128_t x231 = (uint128_t) (x230 >> 0x55);
uint128_t x232 = ((uint128_t)x230 & 0x1fffffffffffffffffffffL);
uint256_t x233 = (x231 + x225);
uint128_t x234 = (uint128_t) (x233 >> 0x55);
uint128_t x235 = ((uint128_t)x233 & 0x1fffffffffffffffffffffL);
uint128_t x236 = (x229 + (0x5 * x234));
uint128_t x237 = (x236 >> 0x55);
uint128_t x238 = (x236 & 0x1fffffffffffffffffffffL);
uint128_t x239 = (x237 + x232);
uint128_t x240 = (x239 >> 0x55);
uint128_t x241 = (x239 & 0x1fffffffffffffffffffffL);
uint128_t x242 = (x240 + x235);
return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238))))
(x, (x0, x1), (x2, x3))%core in
(let (a0, b0) := a in
(a0, b0), let (a0, b0) := b in
(a0, b0))%core
: word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 * (word128 * word128 * word128) * (word128 * word128 * word128 * (word128 * word128 * word128))
|
