blob: 47536ebbfa5de38e25e917204631b76a662fdd18 (
plain)
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
rmulW =
fun var : Syntax.base_type -> Type =>
λ x x0 x1 x2 x3 x4 x5 x6 x7 x8 : var Syntax.TZ,
Tbase Syntax.TZ x9 = x3 * x8;
Tbase Syntax.TZ x10 = x * x7;
Tbase Syntax.TZ x11 = x0 * x6;
Tbase Syntax.TZ x12 = x1 * x5;
Tbase Syntax.TZ x13 = x2 * x4;
Tbase Syntax.TZ x14 = x12 + x13;
Tbase Syntax.TZ x15 = x11 + x14;
Tbase Syntax.TZ x16 = x10 + x15;
Tbase Syntax.TZ x17 = 0x13 * x16;
Tbase Syntax.TZ x18 = x9 + x17;
Tbase Syntax.TZ x19 = x18 >> 0x33;
Tbase Syntax.TZ x20 = x2 * x8;
Tbase Syntax.TZ x21 = x3 * x7;
Tbase Syntax.TZ x22 = x20 + x21;
Tbase Syntax.TZ x23 = x * x6;
Tbase Syntax.TZ x24 = x0 * x5;
Tbase Syntax.TZ x25 = x1 * x4;
Tbase Syntax.TZ x26 = x24 + x25;
Tbase Syntax.TZ x27 = x23 + x26;
Tbase Syntax.TZ x28 = 0x13 * x27;
Tbase Syntax.TZ x29 = x22 + x28;
Tbase Syntax.TZ x30 = x19 + x29;
Tbase Syntax.TZ x31 = x30 >> 0x33;
Tbase Syntax.TZ x32 = x1 * x8;
Tbase Syntax.TZ x33 = x2 * x7;
Tbase Syntax.TZ x34 = x3 * x6;
Tbase Syntax.TZ x35 = x33 + x34;
Tbase Syntax.TZ x36 = x32 + x35;
Tbase Syntax.TZ x37 = x * x5;
Tbase Syntax.TZ x38 = x0 * x4;
Tbase Syntax.TZ x39 = x37 + x38;
Tbase Syntax.TZ x40 = 0x13 * x39;
Tbase Syntax.TZ x41 = x36 + x40;
Tbase Syntax.TZ x42 = x31 + x41;
Tbase Syntax.TZ x43 = x42 >> 0x33;
Tbase Syntax.TZ x44 = x0 * x8;
Tbase Syntax.TZ x45 = x1 * x7;
Tbase Syntax.TZ x46 = x2 * x6;
Tbase Syntax.TZ x47 = x3 * x5;
Tbase Syntax.TZ x48 = x46 + x47;
Tbase Syntax.TZ x49 = x45 + x48;
Tbase Syntax.TZ x50 = x44 + x49;
Tbase Syntax.TZ x51 = x * x4;
Tbase Syntax.TZ x52 = 0x13 * x51;
Tbase Syntax.TZ x53 = x50 + x52;
Tbase Syntax.TZ x54 = x43 + x53;
Tbase Syntax.TZ x55 = x54 >> 0x33;
Tbase Syntax.TZ x56 = x * x8;
Tbase Syntax.TZ x57 = x0 * x7;
Tbase Syntax.TZ x58 = x1 * x6;
Tbase Syntax.TZ x59 = x2 * x5;
Tbase Syntax.TZ x60 = x3 * x4;
Tbase Syntax.TZ x61 = x59 + x60;
Tbase Syntax.TZ x62 = x58 + x61;
Tbase Syntax.TZ x63 = x57 + x62;
Tbase Syntax.TZ x64 = x56 + x63;
Tbase Syntax.TZ x65 = x55 + x64;
Tbase Syntax.TZ x66 = x65 >> 0x33;
Tbase Syntax.TZ x67 = 0x13 * x66;
Tbase Syntax.TZ x68 = x18 & 0x7ffffffffffff;
Tbase Syntax.TZ x69 = x67 + x68;
Tbase Syntax.TZ x70 = x69 >> 0x33;
Tbase Syntax.TZ x71 = x30 & 0x7ffffffffffff;
Tbase Syntax.TZ x72 = x70 + x71;
Tbase Syntax.TZ x73 = x65 & 0x7ffffffffffff;
Tbase Syntax.TZ x74 = x54 & 0x7ffffffffffff;
Tbase Syntax.TZ x75 = x72 >> 0x33;
Tbase Syntax.TZ x76 = x42 & 0x7ffffffffffff;
Tbase Syntax.TZ x77 = x75 + x76;
Tbase Syntax.TZ x78 = x72 & 0x7ffffffffffff;
Tbase Syntax.TZ x79 = x69 & 0x7ffffffffffff;
(Return x73, Return x74, Return x77, Return x78, Return x79)
: forall var : Syntax.base_type -> Type,
expr Syntax.base_type Syntax.op
(Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Syntax.TZ ->
Tbase Syntax.TZ * Tbase Syntax.TZ * Tbase Syntax.TZ *
Tbase Syntax.TZ * Tbase Syntax.TZ)
Argument scope is [function_scope]
|
