1%  MICROCODED COMPUTER PROOF : HOL                                      %
2%                                                                       %
3%  'proof2.ml'                                                          %
4%                                                                       %
5%  Description                                                          % 
6%                                                                       %
7%     This theory results in a theorem about each of the fifteen        %
8%  possible execution cycles.  There are five possible cycles for       %
9%  the idling case, four when the button is pressed depending on the    %
10%  value of knob, and one possible cycle when the button is not         %
11%  pressed.  The remaining ten possible execution cycles are cases      %
12%  of when the computer is running.  There is one possible execution    %
13%  cycle for each of the eight opcode except for the conditional jump   %
14%  for which there are two possible execution cycles depending on       %
15%  whether the accumulator is zero or non-zero.  Finally, there is      %
16%  is the execution cycle which results when the machine is running     %
17%  and the button is pressed.  The idling case is mpc t1 = #00000"      %
18%  and the running case is "mpc t1 = #00101".                           %
19%     The theorems are derived for each case by simulating the exec-    %
20%  ution cycle.  Instead of data, the 'values' are assertions about     %
21%  data in terms of the state at the start of the execution cycle.      %
22%     This is the major step in the proof.  The rest of the proof is    %
23%  mostly 'stitching' together results of this step.                    %
24%                                                                       %
25%  Author:  Jeff Joyce                                                  %
26%  Date:    August 4, 1985                                              %
27
28new_theory `proof2`;;
29
30new_parent `proof1`;;
31
32let CUT_PAD = axiom `values` `CUT_PAD`;;
33let CUT_INC_PAD = axiom `values` `CUT_INC_PAD`;;
34
35let arith_lemmas =
36 [
37  (theorem `arith` `plus_0_2`);
38  (theorem `arith` `plus_1_2`);
39  (theorem `arith` `plus_2_2`);
40  (theorem `arith` `plus_3_2`);
41  (theorem `arith` `plus_0_10`);
42  (theorem `arith` `plus_1_10`);
43  (theorem `arith` `plus_2_10`);
44  (theorem `arith` `plus_3_10`);
45  (theorem `arith` `plus_4_10`);
46  (theorem `arith` `plus_5_10`);
47  (theorem `arith` `plus_6_10`);
48  (theorem `arith` `plus_7_10`)
49 ];;
50
51let microcode =
52[
53 WORD_RULE (axiom `microcode` `MICROCODE0`);
54 WORD_RULE (axiom `microcode` `MICROCODE1`);
55 WORD_RULE (axiom `microcode` `MICROCODE2`);
56 WORD_RULE (axiom `microcode` `MICROCODE3`);
57 WORD_RULE (axiom `microcode` `MICROCODE4`);
58 WORD_RULE (axiom `microcode` `MICROCODE5`);
59 WORD_RULE (axiom `microcode` `MICROCODE6`);
60 WORD_RULE (axiom `microcode` `MICROCODE7`);
61 WORD_RULE (axiom `microcode` `MICROCODE8`);
62 WORD_RULE (axiom `microcode` `MICROCODE9`);
63 WORD_RULE (axiom `microcode` `MICROCODE10`);
64 WORD_RULE (axiom `microcode` `MICROCODE11`);
65 WORD_RULE (axiom `microcode` `MICROCODE12`);
66 WORD_RULE (axiom `microcode` `MICROCODE13`);
67 WORD_RULE (axiom `microcode` `MICROCODE14`);
68 WORD_RULE (axiom `microcode` `MICROCODE15`);
69 WORD_RULE (axiom `microcode` `MICROCODE16`);
70 WORD_RULE (axiom `microcode` `MICROCODE17`);
71 WORD_RULE (axiom `microcode` `MICROCODE18`);
72 WORD_RULE (axiom `microcode` `MICROCODE19`);
73 WORD_RULE (axiom `microcode` `MICROCODE20`);
74 WORD_RULE (axiom `microcode` `MICROCODE21`);
75 WORD_RULE (axiom `microcode` `MICROCODE22`);
76 WORD_RULE (axiom `microcode` `MICROCODE23`);
77 WORD_RULE (axiom `microcode` `MICROCODE24`);
78 WORD_RULE (axiom `microcode` `MICROCODE25`)
79];;
80
81let COMPUTER_IMP_EXP_ASM = theorem `computer_imp` `COMPUTER_IMP_EXP_ASM`;;
82
83letrec nth_CONJUNCT n thm =
84 if n = 0 then thm else (nth_CONJUNCT (n - 1) (CONJUNCT2 thm));;
85
86let COMPUTER_IMP_buf   = CONJUNCT1 (nth_CONJUNCT 0 COMPUTER_IMP_EXP_ASM);;
87let COMPUTER_IMP_m     = CONJUNCT1 (nth_CONJUNCT 1 COMPUTER_IMP_EXP_ASM);;
88let COMPUTER_IMP_mar   = CONJUNCT1 (nth_CONJUNCT 2 COMPUTER_IMP_EXP_ASM);;
89let COMPUTER_IMP_pc    = CONJUNCT1 (nth_CONJUNCT 3 COMPUTER_IMP_EXP_ASM);;
90let COMPUTER_IMP_acc   = CONJUNCT1 (nth_CONJUNCT 4 COMPUTER_IMP_EXP_ASM);;
91let COMPUTER_IMP_ir    = CONJUNCT1 (nth_CONJUNCT 5 COMPUTER_IMP_EXP_ASM);;
92let COMPUTER_IMP_arg   = CONJUNCT1 (nth_CONJUNCT 6 COMPUTER_IMP_EXP_ASM);;
93let COMPUTER_IMP_mpc   = CONJUNCT1 (nth_CONJUNCT 7 COMPUTER_IMP_EXP_ASM);;
94let COMPUTER_IMP_ready = CONJUNCT1 (nth_CONJUNCT 8 COMPUTER_IMP_EXP_ASM);;
95let COMPUTER_IMP_idle  = CONJUNCT2 (nth_CONJUNCT 8 COMPUTER_IMP_EXP_ASM);;
96
97letrec tm n = if n = 0 then "t1:num" else "(^(tm (n - 1))) + 1";;
98
99let arith_rule thm = WORD_RULE (SUBS arith_lemmas thm);;
100
101let evaluate_rule =
102	BITS_RULE thenf
103	EL_RULE   thenf
104	COND_RULE thenf
105	SEG_RULE  thenf
106	V_RULE    thenf
107	WORD_RULE thenf
108	VAL_RULE  thenf
109	EQ_RULE   thenf
110	COND_RULE thenf
111	U_RULE    thenf
112	TRI_RULE  thenf
113	bool_RULE thenf
114	COND_RULE;;
115
116let reduce_rule assumptions thm =
117 REWRITE_RULE [CUT_PAD;CUT_INC_PAD]
118  (arith_rule
119   (SUBS assumptions
120    (evaluate_rule
121     (SUBS microcode
122      (SUBS assumptions thm)))));;
123
124let first_state assumptions =
125 (
126  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_buf)),
127  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_m)),
128  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_mar)),
129  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_pc)),
130  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_acc)),
131  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_ir)),
132  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_arg)),
133  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_mpc)),
134  (reduce_rule assumptions (SPEC "t1:num" COMPUTER_IMP_ready))
135 );;
136
137% The state at time t1 + i is obtained by specifying COMPUTER_IMP_buf,  %
138% COMPUTER_IMP_m, ..., COMPUTER_IMP_ready for the term (tm (i - 1)) and %
139% 'reducing' these assertions.  Reduction involves substitution with    %
140% assertions about the state at time t1 + (i - 1) as well as substi-    %
141% tution with the microcode and assumptions for the the particular      %
142% case followed by an evaluation.  The evalution uses BITS_RULE,        %
143% EL_RULE, WORD_RULE, etc. (see 'evaluate_rule').                       %
144
145letrec iterate_state
146 i n assumptions (buf,m,mar,pc,acc,ir,arg,mpc,ready) =
147 if i > n
148  then (buf,m,mar,pc,acc,ir,arg,mpc,ready)
149  else
150   let update_rule thm =
151    (reduce_rule
152     ([buf;m;mar;pc;acc;ir;arg;mpc] @ assumptions)
153     (SPEC (tm (i - 1)) thm)
154    ) in
155    iterate_state
156     (i + 1)
157     n
158     assumptions
159     (
160      (update_rule COMPUTER_IMP_buf),
161      (update_rule COMPUTER_IMP_m),
162      (update_rule COMPUTER_IMP_mar),
163      (update_rule COMPUTER_IMP_pc),
164      (update_rule COMPUTER_IMP_acc),
165      (update_rule COMPUTER_IMP_ir),
166      (update_rule COMPUTER_IMP_arg),
167      (update_rule COMPUTER_IMP_mpc),
168      (LIST_CONJ [(update_rule COMPUTER_IMP_ready);ready])
169     );;
170
171let simulate ncycles assumptions =
172 let (buf,m,mar,pc,acc,ir,arg,mpc,readylist) =
173  iterate_state 2 ncycles assumptions (first_state assumptions) in
174 let idle = reduce_rule [mpc] (SPEC (tm ncycles) COMPUTER_IMP_idle) in
175 let ready = reduce_rule [mpc] (SPEC (tm ncycles) COMPUTER_IMP_ready) in
176 LIST_CONJ [m;pc;acc;idle;ready;readylist];;
177
178% ===================================================================== %
179% Case: mpc = 0, button = T, knob = 0 ================================= %
180
181let assumptions = 
182[
183 ASSUME "(mpc (t1:num)) = #00000";
184 ASSUME "(button (t1:num)) = T";
185 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 0"
186];;
187
188let COMPUTER_IMP_mpc_0_button_T_knob_0 =
189 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_0`,(simulate 3 assumptions));;
190
191% ===================================================================== %
192% Case: mpc = 0, button = T, knob = 1 ================================= %
193
194let assumptions = 
195[
196 ASSUME "(mpc (t1:num)) = #00000";
197 ASSUME "(button (t1:num)) = T";
198 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 1"
199];;
200
201let COMPUTER_IMP_mpc_0_button_T_knob_1 =
202 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_1`,(simulate 3 assumptions));;
203
204% ===================================================================== %
205% Case: mpc = 0, button = T, knob = 2 ================================= %
206
207let assumptions = 
208[
209 ASSUME "(mpc (t1:num)) = #00000";
210 ASSUME "(button (t1:num)) = T";
211 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 2"
212];;
213
214let COMPUTER_IMP_mpc_0_button_T_knob_2 =
215 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_2`,(simulate 4 assumptions));;
216
217% ===================================================================== %
218% Case: mpc = 0, button = T, knob = 3 ================================= %
219
220let assumptions = 
221[
222 ASSUME "(mpc (t1:num)) = #00000";
223 ASSUME "(button (t1:num)) = T";
224 ASSUME "(VAL2 (knob ((t1:num) + 1))) = 3"
225];;
226
227let COMPUTER_IMP_mpc_0_button_T_knob_3 =
228 save_thm (`COMPUTER_IMP_mpc_0_button_T_knob_3`,(simulate 2 assumptions));;
229
230% ===================================================================== %
231% Case: mpc = 0, button = F =========================================== %
232
233let assumptions = 
234[
235 ASSUME "(mpc (t1:num)) = #00000";
236 ASSUME "(button (t1:num)) = F";
237];;
238
239let COMPUTER_IMP_mpc_0_button_F =
240 save_thm (`COMPUTER_IMP_mpc_0_button_F`,(simulate 1 assumptions));;
241
242% ===================================================================== %
243% Case: mpc = 5, button = T =========================================== %
244
245let assumptions = 
246[
247 ASSUME "(mpc (t1:num)) = #00101";
248 ASSUME "(button (t1:num)) = T";
249];;
250
251let COMPUTER_IMP_mpc_5_button_T =
252 save_thm (`COMPUTER_IMP_mpc_5_button_T`,(simulate 1 assumptions));;
253
254% ===================================================================== %
255% Case: mpc = 5, button = F, opcode is 0 (HALT) ======================= %
256
257let assumptions = 
258[
259 ASSUME "(mpc (t1:num)) = #00101";
260 ASSUME "(button (t1:num)) = F";
261 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 0"
262];;
263
264let COMPUTER_IMP_mpc_5_button_F_opcode_0 =
265 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_0`,(simulate 5 assumptions));;
266
267% ===================================================================== %
268% Case: mpc = 5, button = F, opcode is 1 (JMP) ======================== %
269
270let assumptions = 
271[
272 ASSUME "(mpc (t1:num)) = #00101";
273 ASSUME "(button (t1:num)) = F";
274 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 1"
275];;
276
277let COMPUTER_IMP_mpc_5_button_F_opcode_1 =
278 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_1`,(simulate 5 assumptions));;
279
280% ===================================================================== %
281% Case: mpc = 5, button = F, zero, opcode is 2 (JZR) ================== %
282
283let assumptions = 
284[
285 ASSUME "(mpc (t1:num)) = #00101";
286 ASSUME "(button (t1:num)) = F";
287 ASSUME "((VAL16(acc (t1:num))) = 0) = T";
288 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 2"
289];;
290
291let COMPUTER_IMP_mpc_5_button_F_zero_opcode_2 =
292 save_thm (`COMPUTER_IMP_mpc_5_button_F_zero_opcode_2`,(simulate 6 assumptions));;
293
294% ===================================================================== %
295% Case: mpc = 5, button = F, nonzero, opcode is 2 (JZR) =============== %
296
297let assumptions = 
298[
299 ASSUME "(mpc (t1:num)) = #00101";
300 ASSUME "(button (t1:num)) = F";
301 ASSUME "((VAL16(acc (t1:num))) = 0) = F";
302 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 2"
303];;
304
305let COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2 =
306 save_thm (`COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2`,(simulate 7 assumptions));;
307
308% ===================================================================== %
309% Case: mpc = 5, button = F, opcode is 3 (ADD) ======================== %
310
311let assumptions = 
312[
313 ASSUME "(mpc (t1:num)) = #00101";
314 ASSUME "(button (t1:num)) = F";
315 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 3"
316];;
317
318let COMPUTER_IMP_mpc_5_button_F_opcode_3 =
319 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_3`,(simulate 10 assumptions));;
320
321% ===================================================================== %
322% Case: mpc = 5, button = F, opcode is 4 (SUB) ======================== %
323
324let assumptions = 
325[
326 ASSUME "(mpc (t1:num)) = #00101";
327 ASSUME "(button (t1:num)) = F";
328 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 4"
329];;
330
331let COMPUTER_IMP_mpc_5_button_F_opcode_4 =
332 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_4`,(simulate 10 assumptions));;
333
334% ===================================================================== %
335% Case: mpc = 5, button = F, opcode is 5 (LD) ========================= %
336
337let assumptions = 
338[
339 ASSUME "(mpc (t1:num)) = #00101";
340 ASSUME "(button (t1:num)) = F";
341 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 5"
342];;
343
344let COMPUTER_IMP_mpc_5_button_F_opcode_5 =
345 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_5`,(simulate 8 assumptions));;
346
347% ===================================================================== %
348% Case: mpc = 5, button = F, opcode is 6 (ST) ========================= %
349
350let assumptions = 
351[
352 ASSUME "(mpc (t1:num)) = #00101";
353 ASSUME "(button (t1:num)) = F";
354 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 6"
355];;
356
357let COMPUTER_IMP_mpc_5_button_F_opcode_6 =
358 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_6`,(simulate 8 assumptions));;
359
360% ===================================================================== %
361% Case: mpc = 5, button = F, opcode is 7 (SKIP) ======================= %
362
363let assumptions = 
364[
365 ASSUME "(mpc (t1:num)) = #00101";
366 ASSUME "(button (t1:num)) = F";
367 ASSUME "(VAL3(OPCODE(FETCH13(memory (t1:num))(pc (t1:num))))) = 7"
368];;
369
370let COMPUTER_IMP_mpc_5_button_F_opcode_7 =
371 save_thm (`COMPUTER_IMP_mpc_5_button_F_opcode_7`,(simulate 6 assumptions));;
372
373close_theory ();;
374