1% MICROCODED COMPUTER PROOF : HOL % 2% % 3% 'proof3.ml' % 4% % 5% Description % 6% % 7% This theory identifies the term "((t1 + 1) ... + 1)" with t2 % 8% for each of the fifteen possible execution cycles from results in % 9% 'proof1', lemmas about the 'NEXT' relation, and the assumption % 10% "NEXT (t1,t2) ready". The theorems about each of the the execution % 11% cycles derived in 'proof1' can be simplified with this identity. % 12% The assumptions "STABLE (t1,t2) knob" and "STABLE (t1,t2) switches" % 13% also allow "knob (t1 + 1)" and "switches ((t1 + 1) + 1)" to be % 14% replaced by "knob t1" and "switches t1". These identities result % 15% in theorems which only have "t1" and "t2" as terms of time. That % 16% is, references to times in between 't1' and 't2' are eliminated. % 17% The resulting theorems are further simplifed to an assertion about % 18% the memory, program counter, accumulator, and idle status. Other % 19% results from 'proof1' (eg. the status of 'ready' and the other % 20% registers) are not required beyond this step in the proof. % 21% % 22% Author: Jeff Joyce % 23% Date: August 4, 1985 % 24 25new_theory `proof3`;; 26 27new_parent `next`;; 28new_parent `proof2`;; 29 30let NEXT_INC_LEMMA = theorem `next` `NEXT_INC_LEMMA`;; 31let NEXT_IDENTITY_LEMMA = theorem `next` `NEXT_IDENTITY_LEMMA`;; 32let NEXT_INC_INTERVAL_LEMMA = theorem `next` `NEXT_INC_INTERVAL_LEMMA`;; 33 34let STABLE = definition `values` `STABLE`;; 35let VAL_word2_CASES = theorem `values` `VAL_word2_CASES`;; 36 37let COMPUTER_IMP_mpc_0_button_T_knob_0 = 38 theorem `proof2` `COMPUTER_IMP_mpc_0_button_T_knob_0`;; 39let COMPUTER_IMP_mpc_0_button_T_knob_1 = 40 theorem `proof2` `COMPUTER_IMP_mpc_0_button_T_knob_1`;; 41let COMPUTER_IMP_mpc_0_button_T_knob_2 = 42 theorem `proof2` `COMPUTER_IMP_mpc_0_button_T_knob_2`;; 43let COMPUTER_IMP_mpc_0_button_T_knob_3 = 44 theorem `proof2` `COMPUTER_IMP_mpc_0_button_T_knob_3`;; 45let COMPUTER_IMP_mpc_0_button_F = 46 theorem `proof2` `COMPUTER_IMP_mpc_0_button_F`;; 47let COMPUTER_IMP_mpc_5_button_T = 48 theorem `proof2` `COMPUTER_IMP_mpc_5_button_T`;; 49let COMPUTER_IMP_mpc_5_button_F_opcode_0 = 50 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_0`;; 51let COMPUTER_IMP_mpc_5_button_F_opcode_1 = 52 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_1`;; 53let COMPUTER_IMP_mpc_5_button_F_zero_opcode_2 = 54 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_zero_opcode_2`;; 55let COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2 = 56 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2`;; 57let COMPUTER_IMP_mpc_5_button_F_opcode_3 = 58 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_3`;; 59let COMPUTER_IMP_mpc_5_button_F_opcode_4 = 60 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_4`;; 61let COMPUTER_IMP_mpc_5_button_F_opcode_5 = 62 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_5`;; 63let COMPUTER_IMP_mpc_5_button_F_opcode_6 = 64 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_6`;;d 65let COMPUTER_IMP_mpc_5_button_F_opcode_7 = 66 theorem `proof2` `COMPUTER_IMP_mpc_5_button_F_opcode_7`;; 67 68letrec tm n = if n = 0 then "t1:num" else "(^(tm (n - 1))) + 1";; 69 70letrec reduce_interval i n ready next = 71 if i < 0 then next 72 else reduce_interval (i - 1) n (CONJUNCT2 ready) 73 (MP 74 (SPECL [(tm i);(tm n)] (SPEC "ready:num->bool" NEXT_INC_INTERVAL_LEMMA)) 75 (LIST_CONJ [(CONJUNCT1 (CONJUNCT2 ready));next]));; 76 77let identify_interval n thm = 78 MP 79 (SPECL [(tm 0);(tm n);"t2:num"] (SPEC "ready:num->bool" NEXT_IDENTITY_LEMMA)) 80 (LIST_CONJ 81 [ 82 (reduce_interval (n - 2) n 83 (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 thm)))) 84 (MP 85 (SPEC (tm (n - 1))(SPEC "ready:num->bool" NEXT_INC_LEMMA)) 86 (CONJUNCT1 (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 thm)))))) 87 ); 88 (ASSUME "NEXT (t1,t2) ready") 89 ]);; 90 91let between_0_1_2 = 92 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in 93 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in 94 LIST_CONJ [th1;th2];; 95 96let between_0_1_3 = 97 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in 98 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in 99 let th3 = (MP (SPECL [(tm 1);(tm 2)] LESS_SUC) th2) in 100 let th4 = (SUBS [SPEC (tm 2) ADD1] th3) in 101 LIST_CONJ [th1;th4];; 102 103let between_0_1_4 = 104 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in 105 let th2 = (SUBS [SPEC (tm 1) ADD1] (SPEC (tm 1) LESS_SUC_REFL)) in 106 let th3 = (MP (SPECL [(tm 1);(tm 2)] LESS_SUC) th2) in 107 let th4 = (SUBS [SPEC (tm 2) ADD1] th3) in 108 let th5 = (MP (SPECL [(tm 1);(tm 3)] LESS_SUC) th4) in 109 let th6 = (SUBS [SPEC (tm 3) ADD1] th5) in 110 LIST_CONJ [th1;th6];; 111 112let between_mpc_0_button_T_knob_0 = 113 SUBS [identify_interval 3 COMPUTER_IMP_mpc_0_button_T_knob_0] between_0_1_3;; 114let between_mpc_0_button_T_knob_1 = 115 SUBS [identify_interval 3 COMPUTER_IMP_mpc_0_button_T_knob_1] between_0_1_3;; 116let between_mpc_0_button_T_knob_2 = 117 SUBS [identify_interval 4 COMPUTER_IMP_mpc_0_button_T_knob_2] between_0_1_4;; 118let between_mpc_0_button_T_knob_3 = 119 SUBS [identify_interval 2 COMPUTER_IMP_mpc_0_button_T_knob_3] between_0_1_2;; 120 121let th1 = 122 DISJ_CASES 123 (ASSUME "(VAL2(knob(t1 + 1)) = 2) \/ (VAL2(knob(t1 + 1)) = 3)") 124 between_mpc_0_button_T_knob_2 between_mpc_0_button_T_knob_3;; 125 126let th2 = 127 DISJ_CASES 128 (ASSUME 129 "(VAL2(knob(t1 + 1)) = 1) \/ 130 (VAL2(knob(t1 + 1)) = 2) \/ (VAL2(knob(t1 + 1)) = 3)") 131 between_mpc_0_button_T_knob_1 th1;; 132 133let knob_interval = 134 DISJ_CASES (SPEC "(knob ((t1:num) + 1)):word2" VAL_word2_CASES) 135 between_mpc_0_button_T_knob_0 th2;; 136 137let knob_constant_mpc_0_button_T = 138 let th1 = (ASSUME "STABLE (t1,t2) (knob:num->word2)") in 139 let th2 = (PURE_REWRITE_RULE [STABLE] th1) in 140 let th3 = (SPEC (tm 1) th2) in 141 MP th3 knob_interval;; 142 143let between_0_2_3 = 144 let th1 = (SUBS [SPEC (tm 0) ADD1] (SPEC (tm 0) LESS_SUC_REFL)) in 145 let th2 = (MP (SPECL [(tm 0);(tm 1)] LESS_SUC) th1) in 146 let th3 = (SUBS [SPEC (tm 1) ADD1] th2) in 147 let th4 = (SUBS [SPEC (tm 2) ADD1] (SPEC (tm 2) LESS_SUC_REFL)) in 148 LIST_CONJ [th3;th4];; 149 150let switches_constant_rule identity = 151 let th1 = (SUBS [identity] between_0_2_3) in 152 let th2 = (ASSUME "STABLE (t1,t2) (switches:num->word16)") in 153 let th3 = (PURE_REWRITE_RULE [STABLE] th2) in 154 let th4 = (SPEC (tm 2) th3) in 155 let th5 = (MP th4 th1) in 156 UNDISCH_ALL (SUBS [knob_constant_mpc_0_button_T] (DISCH_ALL th5));; 157 158let switches_constant_mpc_0_button_T_knob_0 = 159 switches_constant_rule (identify_interval 3 COMPUTER_IMP_mpc_0_button_T_knob_0);; 160 161let switches_constant_mpc_0_button_T_knob_1 = 162 switches_constant_rule (identify_interval 3 COMPUTER_IMP_mpc_0_button_T_knob_1);; 163 164let simplify n constant_signal_lemmas thm = 165 UNDISCH_ALL 166 (SUBS constant_signal_lemmas 167 (DISCH_ALL 168 (SUBS [identify_interval n thm] 169 (LIST_CONJ 170 [ 171 CONJUNCT1 thm; 172 CONJUNCT1 (CONJUNCT2 thm); 173 CONJUNCT1 (CONJUNCT2 (CONJUNCT2 thm)); 174 CONJUNCT1 (CONJUNCT2 (CONJUNCT2 (CONJUNCT2 thm))) 175 ]))));; 176 177% ===================================================================== % 178% Case: mpc = 0, button = T, knob = 0 ================================= % 179 180let constant_signal_lemmas = 181 [knob_constant_mpc_0_button_T;switches_constant_mpc_0_button_T_knob_0];; 182 183let SIMP_mpc_0_button_T_knob_0 = 184 save_thm 185 ( 186 `SIMP_mpc_0_button_T_knob_0`, 187 (simplify 3 constant_signal_lemmas COMPUTER_IMP_mpc_0_button_T_knob_0) 188 );; 189 190% ===================================================================== % 191% Case: mpc = 0, button = T, knob = 1 ================================= % 192 193let constant_signal_lemmas = 194 [knob_constant_mpc_0_button_T;switches_constant_mpc_0_button_T_knob_1];; 195 196let SIMP_mpc_0_button_T_knob_1 = 197 save_thm 198 ( 199 `SIMP_mpc_0_button_T_knob_1`, 200 (simplify 3 constant_signal_lemmas COMPUTER_IMP_mpc_0_button_T_knob_1) 201 );; 202 203% ===================================================================== % 204% Case: mpc = 0, button = T, knob = 2 ================================= % 205 206let constant_signal_lemmas = [knob_constant_mpc_0_button_T];; 207 208let SIMP_mpc_0_button_T_knob_2 = 209 save_thm 210 ( 211 `SIMP_mpc_0_button_T_knob_2`, 212 (simplify 4 constant_signal_lemmas COMPUTER_IMP_mpc_0_button_T_knob_2) 213 );; 214 215% ===================================================================== % 216% Case: mpc = 0, button = T, knob = 3 ================================= % 217 218let constant_signal_lemmas = [knob_constant_mpc_0_button_T];; 219 220let SIMP_mpc_0_button_T_knob_3 = 221 save_thm 222 ( 223 `SIMP_mpc_0_button_T_knob_3`, 224 (simplify 2 constant_signal_lemmas COMPUTER_IMP_mpc_0_button_T_knob_3) 225 );; 226 227% ===================================================================== % 228% Case: mpc = 0, button = F =========================================== % 229 230let SIMP_mpc_0_button_F = 231 save_thm 232 ( 233 `SIMP_mpc_0_button_F`, 234 (simplify 1 [] COMPUTER_IMP_mpc_0_button_F) 235 );; 236 237% ===================================================================== % 238% Case: mpc = 5, button = T =========================================== % 239 240let SIMP_mpc_5_button_T = 241 save_thm 242 ( 243 `SIMP_mpc_5_button_T`, 244 (simplify 1 [] COMPUTER_IMP_mpc_5_button_T) 245 );; 246 247% ===================================================================== % 248% Case: mpc = 5, button = F, opcode is 0 (HALT) ======================= % 249 250let SIMP_mpc_5_button_F_opcode_0 = 251 save_thm 252 ( 253 `SIMP_mpc_5_button_F_opcode_0`, 254 (simplify 5 [] COMPUTER_IMP_mpc_5_button_F_opcode_0) 255 );; 256 257% ===================================================================== % 258% Case: mpc = 5, button = F, opcode is 1 (JMP) ======================== % 259 260let SIMP_mpc_5_button_F_opcode_1 = 261 save_thm 262 ( 263 `SIMP_mpc_5_button_F_opcode_1`, 264 (simplify 5 [] COMPUTER_IMP_mpc_5_button_F_opcode_1) 265 );; 266 267% ===================================================================== % 268% Case: mpc = 5, button = F, zero, opcode is 2 (JZR) ================== % 269 270let SIMP_mpc_5_button_F_zero_opcode_2 = 271 save_thm 272 ( 273 `SIMP_mpc_5_button_F_zero_opcode_2`, 274 (simplify 6 [] COMPUTER_IMP_mpc_5_button_F_zero_opcode_2) 275 );; 276 277% ===================================================================== % 278% Case: mpc = 5, button = F, nonzero, opcode is 2 (JZR) =============== % 279 280let SIMP_mpc_5_button_F_nonzero_opcode_2 = 281 save_thm 282 ( 283 `SIMP_mpc_5_button_F_nonzero_opcode_2`, 284 (simplify 7 [] COMPUTER_IMP_mpc_5_button_F_nonzero_opcode_2) 285 );; 286 287% ===================================================================== % 288% Case: mpc = 5, button = F, opcode is 3 (ADD) ======================== % 289 290let SIMP_mpc_5_button_F_opcode_3 = 291 save_thm 292 ( 293 `SIMP_mpc_5_button_F_opcode_3`, 294 (simplify 10 [] COMPUTER_IMP_mpc_5_button_F_opcode_3) 295 );; 296 297% ===================================================================== % 298% Case: mpc = 5, button = F, opcode is 4 (SUB) ======================== % 299 300let SIMP_mpc_5_button_F_opcode_4 = 301 save_thm 302 ( 303 `SIMP_mpc_5_button_F_opcode_4`, 304 (simplify 10 [] COMPUTER_IMP_mpc_5_button_F_opcode_4) 305 );; 306 307% ===================================================================== % 308% Case: mpc = 5, button = F, opcode is 5 (LD) ========================= % 309 310let SIMP_mpc_5_button_F_opcode_5 = 311 save_thm 312 ( 313 `SIMP_mpc_5_button_F_opcode_5`, 314 (simplify 8 [] COMPUTER_IMP_mpc_5_button_F_opcode_5) 315 );; 316 317% ===================================================================== % 318% Case: mpc = 5, button = F, opcode is 6 (ST) ========================= % 319 320let SIMP_mpc_5_button_F_opcode_6 = 321 save_thm 322 ( 323 `SIMP_mpc_5_button_F_opcode_6`, 324 (simplify 8 [] COMPUTER_IMP_mpc_5_button_F_opcode_6) 325 );; 326 327% ===================================================================== % 328% Case: mpc = 5, button = F, opcode is 7 (SKIP) ======================= % 329 330let SIMP_mpc_5_button_F_opcode_7 = 331 save_thm 332 ( 333 `SIMP_mpc_5_button_F_opcode_7`, 334 (simplify 6 [] COMPUTER_IMP_mpc_5_button_F_opcode_7) 335 );; 336 337close_theory ();; 338