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
|
λ x x0 : word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x4, x5, (x6, x7))%core,
uint64_t x9, uint64_t x10 = mulx_u64(x5, x7);
uint64_t x12, uint64_t x13 = mulx_u64(x5, x6);
uint64_t x15, uint8_t x16 = addcarryx_u64(0x0, x10, x12);
uint64_t x18, uint8_t _ = addcarryx_u64(0x0, x16, x13);
uint64_t x21, uint64_t x22 = mulx_u64(x9, 0xffffffffffffffffL);
uint64_t x24, uint64_t x25 = mulx_u64(x9, 0x7fffffffffffffffL);
uint64_t x27, uint8_t x28 = addcarryx_u64(0x0, x22, x24);
uint64_t x30, uint8_t _ = addcarryx_u64(0x0, x28, x25);
uint64_t _, uint8_t x34 = addcarryx_u64(0x0, x9, x21);
uint64_t x36, uint8_t x37 = addcarryx_u64(x34, x15, x27);
uint64_t x39, uint8_t x40 = addcarryx_u64(x37, x18, x30);
uint64_t x42, uint64_t x43 = mulx_u64(x4, x7);
uint64_t x45, uint64_t x46 = mulx_u64(x4, x6);
uint64_t x48, uint8_t x49 = addcarryx_u64(0x0, x43, x45);
uint64_t x51, uint8_t _ = addcarryx_u64(0x0, x49, x46);
uint64_t x54, uint8_t x55 = addcarryx_u64(0x0, x36, x42);
uint64_t x57, uint8_t x58 = addcarryx_u64(x55, x39, x48);
uint64_t x60, uint8_t x61 = addcarryx_u64(x58, x40, x51);
uint64_t x63, uint64_t x64 = mulx_u64(x54, 0xffffffffffffffffL);
uint64_t x66, uint64_t x67 = mulx_u64(x54, 0x7fffffffffffffffL);
uint64_t x69, uint8_t x70 = addcarryx_u64(0x0, x64, x66);
uint64_t x72, uint8_t _ = addcarryx_u64(0x0, x70, x67);
uint64_t _, uint8_t x76 = addcarryx_u64(0x0, x54, x63);
uint64_t x78, uint8_t x79 = addcarryx_u64(x76, x57, x69);
uint64_t x81, uint8_t x82 = addcarryx_u64(x79, x60, x72);
uint8_t x83 = (x82 + x61);
uint64_t x85, uint8_t x86 = subborrow_u64(0x0, x78, 0xffffffffffffffffL);
uint64_t x88, uint8_t x89 = subborrow_u64(x86, x81, 0x7fffffffffffffffL);
uint64_t _, uint8_t x92 = subborrow_u64(x89, x83, 0x0);
uint64_t x93 = cmovznz64(x92, x88, x81);
uint64_t x94 = cmovznz64(x92, x85, x78);
return (x93, x94))
(x, x0)%core
: word64 * word64 → word64 * word64 → ReturnType (uint64_t * uint64_t)
|
