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
|
λ x x0 : word64 * word64 * word64 * word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x10, x11, x9, x7, x5, (x18, x19, x17, x15, x13))%core,
uint64_t x20[1] = {(0xffffffffffffe + x10[0] - x18[0])};
uint64_t x21[1] = {(0xffffffffffffe + x11[0] - x19[0])};
uint64_t x22[1] = {(0xffffffffffffe + x9[0] - x17[0])};
uint64_t x23[1] = {(0xffffffffffffe + x7[0] - x15[0])};
uint64_t x24[1] = {(0xfffffffffffda + x5[0] - x13[0])};
uint64_t x25[1] = {(x24[0] >> 0x33)};
uint64_t x26[1] = {(x24[0] & 0x7ffffffffffff)};
uint64_t x27[1] = {(x25[0] + x23[0])};
uint64_t x28[1] = {(x27[0] >> 0x33)};
uint64_t x29[1] = {(x27[0] & 0x7ffffffffffff)};
uint64_t x30[1] = {(x28[0] + x22[0])};
uint64_t x31[1] = {(x30[0] >> 0x33)};
uint64_t x32[1] = {(x30[0] & 0x7ffffffffffff)};
uint64_t x33[1] = {(x31[0] + x21[0])};
uint64_t x34[1] = {(x33[0] >> 0x33)};
uint64_t x35[1] = {(x33[0] & 0x7ffffffffffff)};
uint64_t x36[1] = {(x34[0] + x20[0])};
uint64_t x37[1] = {(x36[0] >> 0x33)};
uint64_t x38[1] = {(x36[0] & 0x7ffffffffffff)};
uint64_t x39[1] = {(x26[0] + 0x13 * x37[0])};
uint64_t x40[1] = {(x39[0] >> 0x33)};
uint64_t x41[1] = {(x39[0] & 0x7ffffffffffff)};
uint64_t x42[1] = {(x40[0] + x29[0])};
uint64_t x43[1] = {(x42[0] >> 0x33)};
uint64_t x44[1] = {(x42[0] & 0x7ffffffffffff)};
return (x38[0], x35[0], x43[0] + x32[0], x44[0], x41[0]))
(x, x0)%core
: word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
|
