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
|
λ 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, 0x8f5c28f5c28f5c29L);
uint64_t x34, uint64_t x35 = mulx_u64(x31, 0xffffffffffffffe7L);
uint64_t x37, uint64_t x38 = mulx_u64(x31, 0xffffffffffffffffL);
uint64_t x40, uint8_t x41 = addcarryx_u64(0x0, x35, x37);
uint64_t x43, uint8_t x44 = addcarryx_u64(x41, x38, x31);
uint64_t _, uint8_t x47 = addcarryx_u64(0x0, x13, x34);
uint64_t x49, uint8_t x50 = addcarryx_u64(x47, x22, x40);
uint64_t x52, uint8_t x53 = addcarryx_u64(x50, x25, x43);
uint64_t x55, uint8_t x56 = addcarryx_u64(x53, x28, x44);
uint64_t x58, uint64_t x59 = mulx_u64(x7, x9);
uint64_t x61, uint64_t x62 = mulx_u64(x7, x11);
uint64_t x64, uint64_t x65 = mulx_u64(x7, x10);
uint64_t x67, uint8_t x68 = addcarryx_u64(0x0, x59, x61);
uint64_t x70, uint8_t x71 = addcarryx_u64(x68, x62, x64);
uint64_t x73, uint8_t _ = addcarryx_u64(0x0, x71, x65);
uint64_t x76, uint8_t x77 = addcarryx_u64(0x0, x49, x58);
uint64_t x79, uint8_t x80 = addcarryx_u64(x77, x52, x67);
uint64_t x82, uint8_t x83 = addcarryx_u64(x80, x55, x70);
uint64_t x85, uint8_t x86 = addcarryx_u64(x83, x56, x73);
uint64_t x88, uint64_t _ = mulx_u64(x76, 0x8f5c28f5c28f5c29L);
uint64_t x91, uint64_t x92 = mulx_u64(x88, 0xffffffffffffffe7L);
uint64_t x94, uint64_t x95 = mulx_u64(x88, 0xffffffffffffffffL);
uint64_t x97, uint8_t x98 = addcarryx_u64(0x0, x92, x94);
uint64_t x100, uint8_t x101 = addcarryx_u64(x98, x95, x88);
uint64_t _, uint8_t x104 = addcarryx_u64(0x0, x76, x91);
uint64_t x106, uint8_t x107 = addcarryx_u64(x104, x79, x97);
uint64_t x109, uint8_t x110 = addcarryx_u64(x107, x82, x100);
uint64_t x112, uint8_t x113 = addcarryx_u64(x110, x85, x101);
uint8_t x114 = (x113 + x86);
uint64_t x116, uint64_t x117 = mulx_u64(x6, x9);
uint64_t x119, uint64_t x120 = mulx_u64(x6, x11);
uint64_t x122, uint64_t x123 = mulx_u64(x6, x10);
uint64_t x125, uint8_t x126 = addcarryx_u64(0x0, x117, x119);
uint64_t x128, uint8_t x129 = addcarryx_u64(x126, x120, x122);
uint64_t x131, uint8_t _ = addcarryx_u64(0x0, x129, x123);
uint64_t x134, uint8_t x135 = addcarryx_u64(0x0, x106, x116);
uint64_t x137, uint8_t x138 = addcarryx_u64(x135, x109, x125);
uint64_t x140, uint8_t x141 = addcarryx_u64(x138, x112, x128);
uint64_t x143, uint8_t x144 = addcarryx_u64(x141, x114, x131);
uint64_t x146, uint64_t _ = mulx_u64(x134, 0x8f5c28f5c28f5c29L);
uint64_t x149, uint64_t x150 = mulx_u64(x146, 0xffffffffffffffe7L);
uint64_t x152, uint64_t x153 = mulx_u64(x146, 0xffffffffffffffffL);
uint64_t x155, uint8_t x156 = addcarryx_u64(0x0, x150, x152);
uint64_t x158, uint8_t x159 = addcarryx_u64(x156, x153, x146);
uint64_t _, uint8_t x162 = addcarryx_u64(0x0, x134, x149);
uint64_t x164, uint8_t x165 = addcarryx_u64(x162, x137, x155);
uint64_t x167, uint8_t x168 = addcarryx_u64(x165, x140, x158);
uint64_t x170, uint8_t x171 = addcarryx_u64(x168, x143, x159);
uint8_t x172 = (x171 + x144);
uint64_t x174, uint8_t x175 = subborrow_u64(0x0, x164, 0xffffffffffffffe7L);
uint64_t x177, uint8_t x178 = subborrow_u64(x175, x167, 0xffffffffffffffffL);
uint64_t x180, uint8_t x181 = subborrow_u64(x178, x170, 0x1);
uint64_t _, uint8_t x184 = subborrow_u64(x181, x172, 0x0);
uint64_t x185 = cmovznz64(x184, x180, x170);
uint64_t x186 = cmovznz64(x184, x177, x167);
uint64_t x187 = cmovznz64(x184, x174, x164);
return (x185, x186, x187))
(x, x0)%core
: word64 * word64 * word64 → word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t)
|
