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
|
λ x x0 : word64 * word64 * word64,
Interp-η
(λ var : Syntax.base_type → Type,
λ '(x6, x7, x5, (x10, x11, x9))%core,
uint64_t x13, uint64_t x14 = mulx_u64(x5, x9);
uint64_t x16, uint64_t x17 = mulx_u64(x5, x11);
uint64_t x19, uint64_t x20 = mulx_u64(x5, x10);
uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x14, x16);
uint64_t x25, uint8_t x26 = addcarryx_u64(x23, x17, x19);
uint64_t x28, uint8_t _ = addcarryx_u64(0x0, x26, x20);
uint64_t x31, uint64_t _ = mulx_u64(x13, 0xcccccccccccccccdL);
uint64_t x34, uint64_t x35 = mulx_u64(x31, 0xfffffffffffffffbL);
uint64_t x37, uint64_t x38 = mulx_u64(x31, 0xffffffffffffffffL);
uint64_t x40, uint8_t x41 = mulx_u64_out_u8(x31, 0x3);
uint64_t x43, uint8_t x44 = addcarryx_u64(0x0, x35, x37);
uint64_t x46, uint8_t x47 = addcarryx_u64(x44, x38, x40);
uint8_t x48 = (x47 + x41);
uint64_t _, uint8_t x51 = addcarryx_u64(0x0, x13, x34);
uint64_t x53, uint8_t x54 = addcarryx_u64(x51, x22, x43);
uint64_t x56, uint8_t x57 = addcarryx_u64(x54, x25, x46);
uint64_t x59, uint8_t x60 = addcarryx_u64(x57, x28, x48);
uint64_t x62, uint64_t x63 = mulx_u64(x7, x9);
uint64_t x65, uint64_t x66 = mulx_u64(x7, x11);
uint64_t x68, uint64_t x69 = mulx_u64(x7, x10);
uint64_t x71, uint8_t x72 = addcarryx_u64(0x0, x63, x65);
uint64_t x74, uint8_t x75 = addcarryx_u64(x72, x66, x68);
uint64_t x77, uint8_t _ = addcarryx_u64(0x0, x75, x69);
uint64_t x80, uint8_t x81 = addcarryx_u64(0x0, x53, x62);
uint64_t x83, uint8_t x84 = addcarryx_u64(x81, x56, x71);
uint64_t x86, uint8_t x87 = addcarryx_u64(x84, x59, x74);
uint64_t x89, uint8_t x90 = addcarryx_u64(x87, x60, x77);
uint64_t x92, uint64_t _ = mulx_u64(x80, 0xcccccccccccccccdL);
uint64_t x95, uint64_t x96 = mulx_u64(x92, 0xfffffffffffffffbL);
uint64_t x98, uint64_t x99 = mulx_u64(x92, 0xffffffffffffffffL);
uint64_t x101, uint8_t x102 = mulx_u64_out_u8(x92, 0x3);
uint64_t x104, uint8_t x105 = addcarryx_u64(0x0, x96, x98);
uint64_t x107, uint8_t x108 = addcarryx_u64(x105, x99, x101);
uint8_t x109 = (x108 + x102);
uint64_t _, uint8_t x112 = addcarryx_u64(0x0, x80, x95);
uint64_t x114, uint8_t x115 = addcarryx_u64(x112, x83, x104);
uint64_t x117, uint8_t x118 = addcarryx_u64(x115, x86, x107);
uint64_t x120, uint8_t x121 = addcarryx_u64(x118, x89, x109);
uint8_t x122 = (x121 + x90);
uint64_t x124, uint64_t x125 = mulx_u64(x6, x9);
uint64_t x127, uint64_t x128 = mulx_u64(x6, x11);
uint64_t x130, uint64_t x131 = mulx_u64(x6, x10);
uint64_t x133, uint8_t x134 = addcarryx_u64(0x0, x125, x127);
uint64_t x136, uint8_t x137 = addcarryx_u64(x134, x128, x130);
uint64_t x139, uint8_t _ = addcarryx_u64(0x0, x137, x131);
uint64_t x142, uint8_t x143 = addcarryx_u64(0x0, x114, x124);
uint64_t x145, uint8_t x146 = addcarryx_u64(x143, x117, x133);
uint64_t x148, uint8_t x149 = addcarryx_u64(x146, x120, x136);
uint64_t x151, uint8_t x152 = addcarryx_u64(x149, x122, x139);
uint64_t x154, uint64_t _ = mulx_u64(x142, 0xcccccccccccccccdL);
uint64_t x157, uint64_t x158 = mulx_u64(x154, 0xfffffffffffffffbL);
uint64_t x160, uint64_t x161 = mulx_u64(x154, 0xffffffffffffffffL);
uint64_t x163, uint8_t x164 = mulx_u64_out_u8(x154, 0x3);
uint64_t x166, uint8_t x167 = addcarryx_u64(0x0, x158, x160);
uint64_t x169, uint8_t x170 = addcarryx_u64(x167, x161, x163);
uint8_t x171 = (x170 + x164);
uint64_t _, uint8_t x174 = addcarryx_u64(0x0, x142, x157);
uint64_t x176, uint8_t x177 = addcarryx_u64(x174, x145, x166);
uint64_t x179, uint8_t x180 = addcarryx_u64(x177, x148, x169);
uint64_t x182, uint8_t x183 = addcarryx_u64(x180, x151, x171);
uint8_t x184 = (x183 + x152);
uint64_t x186, uint8_t x187 = subborrow_u64(0x0, x176, 0xfffffffffffffffbL);
uint64_t x189, uint8_t x190 = subborrow_u64(x187, x179, 0xffffffffffffffffL);
uint64_t x192, uint8_t x193 = subborrow_u64(x190, x182, 0x3);
uint64_t _, uint8_t x196 = subborrow_u64(x193, x184, 0x0);
uint64_t x197 = cmovznz64(x196, x192, x182);
uint64_t x198 = cmovznz64(x196, x189, x179);
uint64_t x199 = cmovznz64(x196, x186, x176);
return (x197, x198, x199))
(x, x0)%core
: word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)
|
