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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
|
default Order dec
$include <exception_basic.sail>
$include <flow.sail>
$include <vector_dec.sail>
$include <arith.sail>
function main (() : unit) -> unit = {
assert(sub_int(0, 0) == 0);
assert(sub_int(0, 14) == -14);
assert(sub_int(0, 17) == -17);
assert(sub_int(0, 29) == -29);
assert(sub_int(0, 30) == -30);
assert(sub_int(0, 33) == -33);
assert(sub_int(0, 38) == -38);
assert(sub_int(0, 52) == -52);
assert(sub_int(0, 56) == -56);
assert(sub_int(1, 0) == 1);
assert(sub_int(1, 1) == 0);
assert(sub_int(1, 14) == -13);
assert(sub_int(1, 30) == -29);
assert(sub_int(1, 5) == -4);
assert(sub_int(1, 50) == -49);
assert(sub_int(10, 10) == 0);
assert(sub_int(10, 13) == -3);
assert(sub_int(10, 17) == -7);
assert(sub_int(10, 9) == 1);
assert(sub_int(100, 64) == 36);
assert(sub_int(1024, 1) == 1023);
assert(sub_int(11, 1) == 10);
assert(sub_int(11, 10) == 1);
assert(sub_int(11, 11) == 0);
assert(sub_int(11, 14) == -3);
assert(sub_int(11, 21) == -10);
assert(sub_int(11, 30) == -19);
assert(sub_int(111, 64) == 47);
assert(sub_int(12, 1) == 11);
assert(sub_int(12, 10) == 2);
assert(sub_int(12, 14) == -2);
assert(sub_int(128, 128) == 0);
assert(sub_int(13, 10) == 3);
assert(sub_int(13, 3) == 10);
assert(sub_int(13, 59) == -46);
assert(sub_int(14, 0) == 14);
assert(sub_int(14, 1) == 13);
assert(sub_int(14, 10) == 4);
assert(sub_int(14, 26) == -12);
assert(sub_int(14, 3) == 11);
assert(sub_int(14, 59) == -45);
assert(sub_int(14, 8) == 6);
assert(sub_int(15, 0) == 15);
assert(sub_int(15, 10) == 5);
assert(sub_int(15, 16) == -1);
assert(sub_int(16, 1) == 15);
assert(sub_int(16, 10) == 6);
assert(sub_int(16, 22) == -6);
assert(sub_int(16, 36) == -20);
assert(sub_int(17, 10) == 7);
assert(sub_int(17, 22) == -5);
assert(sub_int(17, 40) == -23);
assert(sub_int(17, 62) == -45);
assert(sub_int(18, 10) == 8);
assert(sub_int(18, 11) == 7);
assert(sub_int(18, 19) == -1);
assert(sub_int(18, 24) == -6);
assert(sub_int(19, 10) == 9);
assert(sub_int(2, 0) == 2);
assert(sub_int(2, 2) == 0);
assert(sub_int(2, 5) == -3);
assert(sub_int(20, 20) == 0);
assert(sub_int(21, 1) == 20);
assert(sub_int(21, 18) == 3);
assert(sub_int(21, 2) == 19);
assert(sub_int(21, 20) == 1);
assert(sub_int(22, 10) == 12);
assert(sub_int(22, 20) == 2);
assert(sub_int(23, 11) == 12);
assert(sub_int(23, 20) == 3);
assert(sub_int(23, 39) == -16);
assert(sub_int(24, 1) == 23);
assert(sub_int(24, 14) == 10);
assert(sub_int(24, 20) == 4);
assert(sub_int(24, 25) == -1);
assert(sub_int(24, 62) == -38);
assert(sub_int(25, 1) == 24);
assert(sub_int(25, 10) == 15);
assert(sub_int(25, 20) == 5);
assert(sub_int(25, 45) == -20);
assert(sub_int(256, 1) == 255);
assert(sub_int(26, 1) == 25);
assert(sub_int(26, 20) == 6);
assert(sub_int(26, 27) == -1);
assert(sub_int(27, 20) == 7);
assert(sub_int(27, 22) == 5);
assert(sub_int(27, 3) == 24);
assert(sub_int(27, 56) == -29);
assert(sub_int(27, 59) == -32);
assert(sub_int(28, 1) == 27);
assert(sub_int(28, 15) == 13);
assert(sub_int(28, 16) == 12);
assert(sub_int(28, 20) == 8);
assert(sub_int(28, 8) == 20);
assert(sub_int(29, 20) == 9);
assert(sub_int(29, 6) == 23);
assert(sub_int(3, 0) == 3);
assert(sub_int(3, 1) == 2);
assert(sub_int(3, 2) == 1);
assert(sub_int(3, 3) == 0);
assert(sub_int(3, 44) == -41);
assert(sub_int(3, 62) == -59);
assert(sub_int(30, 30) == 0);
assert(sub_int(31, 0) == 31);
assert(sub_int(31, 16) == 15);
assert(sub_int(31, 24) == 7);
assert(sub_int(31, 26) == 5);
assert(sub_int(31, 30) == 1);
assert(sub_int(31, 8) == 23);
assert(sub_int(32, 1) == 31);
assert(sub_int(32, 11) == 21);
assert(sub_int(32, 12) == 20);
assert(sub_int(32, 16) == 16);
assert(sub_int(32, 24) == 8);
assert(sub_int(32, 26) == 6);
assert(sub_int(32, 32) == 0);
assert(sub_int(32, 53) == -21);
assert(sub_int(32, 7) == 25);
assert(sub_int(32, 8) == 24);
assert(sub_int(33, 1) == 32);
assert(sub_int(33, 39) == -6);
assert(sub_int(34, 1) == 33);
assert(sub_int(35, 0) == 35);
assert(sub_int(35, 1) == 34);
assert(sub_int(35, 25) == 10);
assert(sub_int(35, 36) == -1);
assert(sub_int(35, 48) == -13);
assert(sub_int(36, 1) == 35);
assert(sub_int(36, 10) == 26);
assert(sub_int(36, 59) == -23);
assert(sub_int(39, 32) == 7);
assert(sub_int(4, 0) == 4);
assert(sub_int(4, 1) == 3);
assert(sub_int(4, 2) == 2);
assert(sub_int(4, 4) == 0);
assert(sub_int(4, 5) == -1);
assert(sub_int(4, 54) == -50);
assert(sub_int(4, 7) == -3);
assert(sub_int(4, 9) == -5);
assert(sub_int(40, 28) == 12);
assert(sub_int(40, 32) == 8);
assert(sub_int(42, 22) == 20);
assert(sub_int(42, 39) == 3);
assert(sub_int(42, 54) == -12);
assert(sub_int(43, 29) == 14);
assert(sub_int(43, 32) == 11);
assert(sub_int(44, 34) == 10);
assert(sub_int(45, 19) == 26);
assert(sub_int(46, 36) == 10);
assert(sub_int(46, 61) == -15);
assert(sub_int(47, 0) == 47);
assert(sub_int(47, 1) == 46);
assert(sub_int(47, 15) == 32);
assert(sub_int(47, 47) == 0);
assert(sub_int(48, 1) == 47);
assert(sub_int(48, 14) == 34);
assert(sub_int(48, 32) == 16);
assert(sub_int(48, 47) == 1);
assert(sub_int(49, 6) == 43);
assert(sub_int(5, 0) == 5);
assert(sub_int(5, 11) == -6);
assert(sub_int(5, 14) == -9);
assert(sub_int(5, 2) == 3);
assert(sub_int(5, 7) == -2);
assert(sub_int(51, 47) == 4);
assert(sub_int(51, 5) == 46);
assert(sub_int(51, 63) == -12);
assert(sub_int(52, 14) == 38);
assert(sub_int(52, 4) == 48);
assert(sub_int(52, 48) == 4);
assert(sub_int(52, 59) == -7);
assert(sub_int(54, 34) == 20);
assert(sub_int(54, 47) == 7);
assert(sub_int(55, 60) == -5);
assert(sub_int(55, 7) == 48);
assert(sub_int(56, 12) == 44);
assert(sub_int(56, 32) == 24);
assert(sub_int(56, 52) == 4);
assert(sub_int(57, 12) == 45);
assert(sub_int(58, 32) == 26);
assert(sub_int(58, 34) == 24);
assert(sub_int(58, 62) == -4);
assert(sub_int(59, 60) == -1);
assert(sub_int(6, 0) == 6);
assert(sub_int(6, 1) == 5);
assert(sub_int(6, 10) == -4);
assert(sub_int(6, 2) == 4);
assert(sub_int(6, 3) == 3);
assert(sub_int(6, 33) == -27);
assert(sub_int(6, 4) == 2);
assert(sub_int(6, 5) == 1);
assert(sub_int(6, 6) == 0);
assert(sub_int(6, 7) == -1);
assert(sub_int(61, 13) == 48);
assert(sub_int(62, 31) == 31);
assert(sub_int(62, 56) == 6);
assert(sub_int(62, 63) == -1);
assert(sub_int(63, 14) == 49);
assert(sub_int(63, 48) == 15);
assert(sub_int(64, 0) == 64);
assert(sub_int(64, 1) == 63);
assert(sub_int(64, 12) == 52);
assert(sub_int(64, 14) == 50);
assert(sub_int(64, 16) == 48);
assert(sub_int(64, 2) == 62);
assert(sub_int(64, 21) == 43);
assert(sub_int(64, 24) == 40);
assert(sub_int(64, 28) == 36);
assert(sub_int(64, 3) == 61);
assert(sub_int(64, 32) == 32);
assert(sub_int(64, 33) == 31);
assert(sub_int(64, 34) == 30);
assert(sub_int(64, 35) == 29);
assert(sub_int(64, 36) == 28);
assert(sub_int(64, 39) == 25);
assert(sub_int(64, 52) == 12);
assert(sub_int(64, 64) == 0);
assert(sub_int(64, 7) == 57);
assert(sub_int(64, 8) == 56);
assert(sub_int(64, 9) == 55);
assert(sub_int(68, 64) == 4);
assert(sub_int(7, 0) == 7);
assert(sub_int(7, 1) == 6);
assert(sub_int(7, 19) == -12);
assert(sub_int(7, 34) == -27);
assert(sub_int(7, 41) == -34);
assert(sub_int(72, 64) == 8);
assert(sub_int(76, 64) == 12);
assert(sub_int(78, 64) == 14);
assert(sub_int(8, 0) == 8);
assert(sub_int(8, 1) == 7);
assert(sub_int(8, 16) == -8);
assert(sub_int(8, 19) == -11);
assert(sub_int(8, 26) == -18);
assert(sub_int(89, 64) == 25);
assert(sub_int(9, 0) == 9);
assert(sub_int(9, 1) == 8);
assert(sub_int(9, 13) == -4);
assert(sub_int(9, 6) == 3);
assert(sub_int(9, 8) == 1);
}
|
