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
|
λ 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 = 0xffffffffffffe + x10;
uint64_t x21 = x20 - x18;
uint64_t x22 = 0xffffffffffffe + x11;
uint64_t x23 = x22 - x19;
uint64_t x24 = 0xffffffffffffe + x9;
uint64_t x25 = x24 - x17;
uint64_t x26 = 0xffffffffffffe + x7;
uint64_t x27 = x26 - x15;
uint64_t x28 = 0xfffffffffffda + x5;
uint64_t x29 = x28 - x13;
uint64_t x30 = x29 >> 0x33;
uint64_t x31 = x29 & 0x7ffffffffffff;
uint64_t x32 = x30 + x27;
uint64_t x33 = x32 >> 0x33;
uint64_t x34 = x32 & 0x7ffffffffffff;
uint64_t x35 = x33 + x25;
uint64_t x36 = x35 >> 0x33;
uint64_t x37 = x35 & 0x7ffffffffffff;
uint64_t x38 = x36 + x23;
uint64_t x39 = x38 >> 0x33;
uint64_t x40 = x38 & 0x7ffffffffffff;
uint64_t x41 = x39 + x21;
uint64_t x42 = x41 >> 0x33;
uint64_t x43 = x41 & 0x7ffffffffffff;
uint64_t x44 = 0x13 * x42;
uint64_t x45 = x31 + x44;
uint64_t x46 = x45 >> 0x33;
uint64_t x47 = x45 & 0x7ffffffffffff;
uint64_t x48 = x46 + x34;
uint64_t x49 = x48 >> 0x33;
uint64_t x50 = x48 & 0x7ffffffffffff;
uint64_t x51 = x49 + x37;
(Return x43, Return x40, Return x51, Return x50, Return x47))
(x, x0)%core
: word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
|
