1(* interactive use: 2 3quietdec := true; 4 5loadPath := 6 (concat Globals.HOLDIR "/examples/dev/sw") :: 7 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 8 (concat Globals.HOLDIR "/examples/elliptic/sep") :: 9 !loadPath; 10 11map load 12 ["preARMTheory", 13 "finite_mapTheory", "listLib", "arm_evalLib", "arm_rulesTheory", 14"armLib", "wordsLib", "wordsTheory", "arithmeticTheory", "pairTheory", 15"listTheory", "ILTheory", "containerTheory", "schneiderUtils", 16"arm_progTheory", "set_sepLib", "arm_instTheory", "pred_setSyntax", 17"rulesTheory", "bsubstTheory"]; 18 19 20 21*) 22open HolKernel boolLib bossLib; 23open Parse ILTheory listLib preARMTheory finite_mapTheory arm_evalLib arm_rulesTheory armLib wordsLib wordsTheory arithmeticTheory pairTheory listTheory pred_setTheory containerTheory rich_listTheory 24open arm_progTheory progTheory pred_setTheory set_sepLib set_sepTheory arm_instTheory ILTheory sortingTheory; 25 26(* 27show_assums := false; 28show_assums := true; 29show_types := true; 30show_types := false; 31show_types_verbosely := true; 32show_types_verbosely := false; 33quietdec := false; 34*) 35 36val _ = hide "reg"; 37val _ = hide "regs"; 38val _ = hide "mem"; 39val _ = hide "M"; 40val _ = hide "cond"; 41 42 43 44val _ = new_theory "swsep"; 45 46 47 48val UNDISCH_HD_TAC = schneiderUtils.UNDISCH_HD_TAC; 49val UNDISCH_ALL_TAC = schneiderUtils.UNDISCH_ALL_TAC; 50val UNDISCH_NO_TAC = schneiderUtils.UNDISCH_NO_TAC 51val POP_NO_ASSUM = schneiderUtils.POP_NO_ASSUM; 52val WEAKEN_HD_TAC = WEAKEN_TAC (fn f => true); 53 54 55val SUBGOAL_TAC = (fn t => (t by ALL_TAC)); 56val REMAINS_TAC = (fn t => (Tactical.REVERSE(t by ALL_TAC))); 57 58val FORALL_EQ_STRIP_TAC :tactic = fn (asl,t) => 59 60 let val (lhs,rhs) = dest_eq t 61 val (lvar,LBody) = dest_forall lhs 62 val (rvar,RBody) = dest_forall rhs 63 val newVar = variant (free_varsl (t::asl)) lvar 64 val newLBody = subst[lvar |-> newVar] LBody 65 val newRBody = subst[rvar |-> newVar] RBody 66 val result = mk_eq(newLBody, newRBody) 67 in ([(asl, result)], 68 fn thList => FORALL_EQ newVar (hd thList)) 69 end 70 handle HOL_ERR _ => raise ERR "FORALL_EQ_STRIP_TAC" ""; 71 72 73val SPEC_NO_ASSUM = (fn n => fn S => POP_NO_ASSUM n (fn x=> ASSUME_TAC (SPEC S x))); 74fun Q_SPEC_NO_ASSUM n = Q_TAC (SPEC_NO_ASSUM n); 75fun Q_SPECL_NO_ASSUM n [] = ALL_TAC 76 | Q_SPECL_NO_ASSUM n (h::l) = (Q_SPEC_NO_ASSUM n h THEN Q_SPECL_NO_ASSUM 0 l); 77 78fun GSYM_DEF_TAC t (asl, w) = 79 let 80 fun is_t_eq term = 81 let 82 val (l, r) = dest_eq term 83 in 84 (l = t) orelse (r = t) 85 end handle _ => false 86 val m = first is_t_eq asl; 87 val (ob, asl') = Lib.pluck (Lib.equal m) asl 88 in 89 ASSUME_TAC (GSYM (ASSUME ob)) (asl', w) 90 end; 91 92fun PROVE_CONDITION_TAC thm (asl, t) = 93 let 94 val (p, c) = dest_imp (concl thm); 95 fun mp_thm thms = 96 let 97 val thm_p = el 1 thms; 98 val thm_t = el 2 thms; 99 val thm = MP thm thm_p; 100 val result = DISCH (concl thm) thm_t; 101 val result = MP result thm 102 in 103 result 104 end 105 in 106 ([(asl, p), (c::asl, t)], mp_thm) 107 end; 108 109fun PROVE_CONDITION_NO_ASSUM i = POP_NO_ASSUM i PROVE_CONDITION_TAC 110 111 112val MREG2REG_def = Define 113 `(MREG2REG reg = (n2w (index_of_reg reg)):4 word)` 114 115val MEXP2addr_model_def = Define 116 `(MEXP2addr_model (MR reg) = (Dp_shift_immediate (LSL (MREG2REG reg)) 0x0w)) /\ 117 (MEXP2addr_model (MC s c) = (Dp_immediate s c))`; 118 119val IS_MEMORY_DOPER_def = Define ` 120 (IS_MEMORY_DOPER (MLDR dst src) = T) /\ 121 (IS_MEMORY_DOPER (MSTR src dst) = T) /\ 122 (IS_MEMORY_DOPER (MPUSH dst' srcL) = T) /\ 123 (IS_MEMORY_DOPER (MPOP dst' srcL) = T) /\ 124 (IS_MEMORY_DOPER y = F)` 125 126val IS_WELL_FORMED_DOPER_def = Define ` 127 (IS_WELL_FORMED_DOPER (MMUL dst src1 src2) = ~(dst = src1)) /\ 128 (IS_WELL_FORMED_DOPER y = T)` 129 130val OFFSET2addr2_def = Define ` 131 (OFFSET2addr2 (POS n) = Dt_immediate ((n2w (n MOD 2**11)))) /\ 132 (OFFSET2addr2 (NEG n) = Dt_immediate ($- (n2w (n MOD 2**11))))`; 133 134 135val IS_SORTED_REG_LIST_def = Define` 136 (IS_SORTED_REG_LIST [] = T) /\ 137 (IS_SORTED_REG_LIST [e] = (e <= 15)) /\ 138 (IS_SORTED_REG_LIST (e1::e2::l) = (e1 < e2) /\ IS_SORTED_REG_LIST (e2::l))`; 139 140val IS_SORTED_REG_LIST___EL_SIZE = store_thm ("IS_SORTED_REG_LIST___EL_SIZE", 141``!l. IS_SORTED_REG_LIST l ==> (EVERY (\n. n < 16) l)``, 142 143Induct_on `l` THENL [ 144 SIMP_TAC list_ss [], 145 146 Cases_on `l` THENL [ 147 SIMP_TAC list_ss [IS_SORTED_REG_LIST_def], 148 149 FULL_SIMP_TAC list_ss [IS_SORTED_REG_LIST_def] THEN 150 REPEAT STRIP_TAC THEN 151 `h < 16` by RES_TAC THEN 152 ASM_SIMP_TAC arith_ss [] 153 ] 154]) 155 156val IS_SORTED_REG_LIST___SORTED_WORDS = 157 store_thm ("IS_SORTED_REG_LIST___SORTED_WORDS", 158 ``!l. IS_SORTED_REG_LIST l = 159 (SORTED $<+ (MAP (n2w:num->word4) l) /\ 160 (EVERY (\n. n < 16) l))``, 161 162 Induct_on `l` THENL [ 163 SIMP_TAC list_ss [SORTED_DEF, IS_SORTED_REG_LIST_def], 164 165 Cases_on `l` THENL [ 166 SIMP_TAC list_ss [SORTED_DEF, IS_SORTED_REG_LIST_def], 167 168 GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 169 FULL_SIMP_TAC list_ss [SORTED_DEF, IS_SORTED_REG_LIST_def, 170 WORD_LO, w2n_n2w, dimword_4] THEN 171 REPEAT STRIP_TAC THEN 172 IMP_RES_TAC IS_SORTED_REG_LIST___EL_SIZE THEN 173 FULL_SIMP_TAC list_ss [], 174 175 PROVE_TAC[IS_SORTED_REG_LIST___EL_SIZE], 176 177 FULL_SIMP_TAC list_ss [SORTED_DEF, IS_SORTED_REG_LIST_def, 178 WORD_LO, w2n_n2w, dimword_4] 179 ] 180 ] 181 ]) 182 183val REGISTER_LIST___reg_bitmap = store_thm ("REGISTER_LIST___reg_bitmap", 184``!l. IS_SORTED_REG_LIST l ==> (REGISTER_LIST (reg_bitmap (MAP n2w l)) = 185 (MAP n2w l))``, 186 187REPEAT STRIP_TAC THEN 188MATCH_MP_TAC SORTED_LOWER_IMP_EQ THEN 189FULL_SIMP_TAC std_ss [MEM_REGISTER_LIST_reg_bitmap, SORTED_REGSITER_LIST, IS_SORTED_REG_LIST___SORTED_WORDS]) 190 191 192val STACK_SIZE_DOPER_def = Define 193 `(STACK_SIZE_DOPER (MPUSH r l) = (LENGTH l, 0, (r = 13) /\ (IS_SORTED_REG_LIST l))) /\ 194 (STACK_SIZE_DOPER (MPOP r l) = (0, LENGTH l, (r = 13) /\ (IS_SORTED_REG_LIST l))) /\ 195 (STACK_SIZE_DOPER (MMOV dst e) = (0, 0, ~(dst = R13))) /\ 196 (STACK_SIZE_DOPER (MADD dst reg1 e) = (0, 0, ~(dst = R13))) /\ 197 (STACK_SIZE_DOPER (MSUB dst reg1 e) = (0, 0, ~(dst = R13))) /\ 198 (STACK_SIZE_DOPER (MRSB dst reg1 e) = (0, 0, ~(dst = R13))) /\ 199 (STACK_SIZE_DOPER (MMUL dst reg1 reg2) = (0, 0, ~(dst = R13) /\ 200 ~(dst = reg1))) /\ 201 (STACK_SIZE_DOPER (MAND dst reg1 e) = (0, 0, ~(dst = R13))) /\ 202 (STACK_SIZE_DOPER (MORR dst reg1 e) = (0, 0, ~(dst = R13))) /\ 203 (STACK_SIZE_DOPER (MEOR dst reg1 e) = (0, 0, ~(dst = R13))) /\ 204 (STACK_SIZE_DOPER (MLSL dst reg1 s) = (0, 0, ~(dst = R13))) /\ 205 (STACK_SIZE_DOPER (MLSR dst reg1 s) = (0, 0, ~(dst = R13))) /\ 206 (STACK_SIZE_DOPER (MASR dst reg1 s) = (0, 0, ~(dst = R13))) /\ 207 (STACK_SIZE_DOPER (MROR dst reg1 s) = (0, 0, ~(dst = R13))) /\ 208 (STACK_SIZE_DOPER _ = (0, 0, F))`; 209 210val VALID_STACK_SIZE_DOPER___IMPLIES___WELL_FORMED = 211 store_thm ("VALID_STACK_SIZE_DOPER___IMPLIES___WELL_FORMED", 212``!doper p n. 213 (STACK_SIZE_DOPER doper = (p, n, T)) ==> IS_WELL_FORMED_DOPER doper``, 214 215Cases_on `doper` THEN 216SIMP_TAC std_ss [IS_WELL_FORMED_DOPER_def, 217 STACK_SIZE_DOPER_def]) 218 219 220val NOT_MEMORY_DOPER___STACK_SIZE_DOPER = 221 store_thm ("NOT_MEMORY_DOPER___STACK_SIZE_DOPER", 222``!doper p n. 223 ~(IS_MEMORY_DOPER doper) ==> 224 ?v. (STACK_SIZE_DOPER doper = (0, 0, v))``, 225 226Cases_on `doper` THEN 227SIMP_TAC std_ss [IS_MEMORY_DOPER_def, 228 STACK_SIZE_DOPER_def]) 229 230 231val STACK_SIZE_BLK_def = Define 232 `(STACK_SIZE_BLK (max, current, valid) [] = (max, current, valid)) /\ 233 (STACK_SIZE_BLK (max, current, valid) (h::l) = 234 let (p, n, v) = STACK_SIZE_DOPER h in 235 let current' = ((current + p) - n) in 236 let max' = MAX current' max in 237 let valid' = (valid /\ (v:bool) /\ ((current + p) >= n) /\ (max >= current)) in 238 STACK_SIZE_BLK (max', current', valid') l)`; 239 240 241val STACK_SIZE_CTL_STRUCTURE_def = Define 242 `(STACK_SIZE_CTL_STRUCTURE (max, current, valid) (BLK l) = 243 STACK_SIZE_BLK (max, current, valid) l) /\ 244 (STACK_SIZE_CTL_STRUCTURE (max, current, valid) (SC ir1 ir2) = 245 let (max', current', valid') = STACK_SIZE_CTL_STRUCTURE (max, current, valid) ir1 in 246 STACK_SIZE_CTL_STRUCTURE (max', current', valid') ir2) /\ 247 (STACK_SIZE_CTL_STRUCTURE (max, current, valid) (CJ c ir1 ir2) = 248 let (max1, current1, valid1) = STACK_SIZE_CTL_STRUCTURE (max, current, valid) ir1 in 249 let (max2, current2, valid2) = STACK_SIZE_CTL_STRUCTURE (max, current, valid) ir2 in 250 (MAX max1 max2, current1, valid1 /\ valid2 /\ (current1 = current2))) /\ 251 (STACK_SIZE_CTL_STRUCTURE (max, current, valid) (TR c ir) = 252 let (max', current', valid') = STACK_SIZE_CTL_STRUCTURE (max, current, valid) ir in 253 (max', current', valid' /\ (current=current')))` 254 255 256val STACK_SIZE_BLK___VALID = store_thm ("STACK_SIZE_BLK___VALID", 257``!max current valid l max' current'. (STACK_SIZE_BLK (max, current, valid) l = (max', current', T)) ==> valid``, 258 259Induct_on `l` THENL [ 260 SIMP_TAC std_ss [STACK_SIZE_BLK_def], 261 262 SIMP_TAC std_ss [STACK_SIZE_BLK_def, LET_THM] THEN 263 REPEAT GEN_TAC THEN 264 `?p n v. STACK_SIZE_DOPER h = (p, n, v)` by METIS_TAC[PAIR] THEN 265 POP_ASSUM MP_TAC THEN 266 SIMP_TAC std_ss [] THEN 267 REPEAT STRIP_TAC THEN 268 RES_TAC 269]) 270 271 272 273(* 274!ir max current valid max' current'. (STACK_SIZE_CTL_STRUCTURE (max, current, valid) ir = 275 (max', current', T)) ==> 276 277 (!st. (read st (REG 13) + n2w (4*(current - current')) - 278 n2w (4*(current' - current))) = 279 read (run_ir ir st) (REG 13)) 280 281restart() 282Induct_on `ir` THENL [ 283 Induct_on `l` THENL [ 284 SIMP_TAC std_ss [SEMANTICS_OF_IR, STACK_SIZE_CTL_STRUCTURE_def, 285 STACK_SIZE_BLK_def, WORD_ADD_0, WORD_SUB_RZERO], 286 287 SIMP_TAC std_ss [SEMANTICS_OF_IR, STACK_SIZE_CTL_STRUCTURE_def, 288 STACK_SIZE_BLK_def, LET_THM] THEN 289 REPEAT GEN_TAC THEN 290 `?p n v. STACK_SIZE_DOPER h = (p, n, v)` by METIS_TAC[PAIR] THEN 291 ASM_SIMP_TAC std_ss [] THEN 292 REPEAT STRIP_TAC THEN 293 FULL_SIMP_TAC std_ss [STACK_SIZE_CTL_STRUCTURE_def] THEN 294 IMP_RES_TAC STACK_SIZE_BLK___VALID THEN 295 RES_TAC THEN 296 `!st st'. (read (run_ir (BLK l) st) (REG 13) = read (run_ir (BLK l) st') (REG 13)) = (read st (REG 13) = read st' (REG 13))` by ALL_TAC THEN1 ( 297 POP_ASSUM (fn thm => MP_TAC (GSYM thm)) THEN 298 SIMP_TAC std_ss [WORD_EQ_ADD_RCANCEL, word_sub_def] 299 ) THEN 300 `!st M1 v. ~(M1 = R13) ==> (read (write st (toREG M1) v) (REG 13) = 301 read st (REG 13))` by ALL_TAC THEN1 ( 302 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 303 Cases_on `st` THEN 304 SIMP_TAC std_ss [read_thm, toREG_def, write_thm, 305 FAPPLY_FUPDATE_THM, COND_RATOR, COND_RAND, 306 n2w_11, dimword_4] THEN 307 Cases_on `M1` THEN 308 SIMP_TAC std_ss [index_of_reg_def] 309 ) THEN 310 Q.PAT_ASSUM `STACK_SIZE_DOPER h = X` (fn thm => MP_TAC (GSYM thm)) THEN 311 Cases_on `h` THEN ( 312 SIMP_TAC std_ss [STACK_SIZE_DOPER_def] THEN 313 REPEAT STRIP_TAC THEN 314 FULL_SIMP_TAC std_ss [mdecode_def] 315 ) THENL [ 316 Q.PAT_ASSUM `v = X` (fn thm => ALL_TAC) THEN 317 Q.PAT_ASSUM `p = LENGTH l1` (fn thm => ALL_TAC) THEN 318 Q.PAT_ASSUM `IS_SORTED_REG_LIST l1` (fn thm => ALL_TAC) THEN 319 Q.PAT_ASSUM `STACK_SIZE_BLK X l = X'` (fn thm => ALL_TAC) THEN 320 Induct_on `l1` THENL [ 321 ASM_SIMP_TAC list_ss [pushL_def, WORD_SUB_RZERO] THEN 322 REPEAT STRIP_TAC THEN 323 Cases_on `st` THEN 324 REWRITE_TAC[read_thm, write_thm, FAPPLY_FUPDATE_THM], 325 326 ASM_SIMP_TAC list_ss [pushL_def] 327 ] 328 329 330 331 FULL_SIMP_TAC std_ss [mdecode_def], 332 FULL_SIMP_TAC std_ss [mdecode_def], 333 FULL_SIMP_TAC std_ss [mdecode_def], 334 335 SIMP_TAC std_ss [STACK_SIZE_DOPER_def, mdecode_def, toREG_def], 336 match [] ``read )write`` 337 338 339 SIMP_TAC std_ss [STACK_SIZE_DOPER_def], 340 SIMP_TAC std_ss [STACK_SIZE_DOPER_def], 341 SIMP_TAC std_ss [STACK_SIZE_DOPER_def], 342 343 344 DB.find "mdecode" 345 346 347 348match [] ``(let a = c in b a) = d`` 349 350CTL_STRUCTURE_11 351 = (max, current, valid)) /\ 352 ( (h::l) = 353 let (p, n, v) = STACK_SIZE_DOPER h in 354 let current' = ((current + p) - n) in 355 let max' = MAX current' max in 356 let valid' = (valid /\ (v:bool) /\ ((current + p) >= n) /\ (max >= current)) in 357 STACK_SIZE_BLOCK (max', current', valid') l)` 358 359 360val blk1 = ``[MADD R0 R0 (MR R1); MADD R0 R0 (MR R1); 361 MADD R0 R0 (MR R2)]`` 362val blk2 = ``[MPUSH 13 [0; 1]; MMOV R3 (MR R2); MMOV R2 (MR R1); 363 MMOV R1 (MR R3)]`` 364val blk3 = ``[MPOP 13 [0; 1]; MMOV R3 (MR R2); MMOV R2 (MR R1); 365 MMOV R1 (MR R3)]`` 366 367EVAL ``STACK_SIZE_BLOCK (3,3,T) ^blk3`` 368 369 ``STACK_SIZE_BLOCK (0,0,T) ^blk3 = X`` 370 371ONCE_REWRITE_TAC [STACK_SIZE_BLOCK_def] THEN 372SIMP_TAC list_ss [STACK_SIZE_DOPER_def, IS_SORTED_REG_LIST_def, LET_THM] THEN 373ONCE_REWRITE_TAC [STACK_SIZE_BLOCK_def] THEN 374SIMP_TAC list_ss [STACK_SIZE_DOPER_def, IS_SORTED_REG_LIST_def, LET_THM] 375 376 377CTL_STRUCTURE_11 378BLK 379 380 381 382 383val IS_SORTED_REG_LIST___SNOC = store_thm ("IS_SORTED_REG_LIST___SNOC", 384 ``!l x. IS_SORTED_REG_LIST (SNOC x l) = 385 (IS_SORTED_REG_LIST l /\ ((l = []) \/ (LAST l < x)) /\ (x <= 15))``, 386 387 Induct_on `l` THENL [ 388 SIMP_TAC list_ss [SNOC, IS_SORTED_REG_LIST_def], 389 390 Cases_on `l` THENL [ 391 SIMP_TAC list_ss [SNOC, IS_SORTED_REG_LIST_def], 392 393 FULL_SIMP_TAC list_ss [SNOC, IS_SORTED_REG_LIST_def] THEN 394 PROVE_TAC[] 395 ] 396 ]) 397 398 399 400val IS_SORTED_REG_LIST___LAST = store_thm ("IS_SORTED_REG_LIST___LAST", 401``!l. IS_SORTED_REG_LIST l ==> 402 (EVERY (\n. n <= (LAST l)) l)``, 403 404 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 405 SIMP_TAC list_ss [], 406 407 SIMP_TAC list_ss [IS_SORTED_REG_LIST___SNOC, LAST] THEN 408 SIMP_TAC list_ss [SNOC_APPEND, EVERY_APPEND] THEN 409 REPEAT STRIP_TAC THENL [ 410 ASM_SIMP_TAC list_ss [], 411 412 RES_TAC THEN 413 FULL_SIMP_TAC arith_ss [EVERY_MEM] THEN 414 REPEAT STRIP_TAC THEN 415 RES_TAC THEN 416 DECIDE_TAC 417 ] 418 ]); 419 420 421 422 423val enc_REG_LIST_def = Define ` 424 enc_REG_LIST l = (FCP i. (MEM i l)):word16` 425 426EVAL ``enc_REGISTER_LIST [2; 3; 5; 14]`` 427 428 429 430 431GEN_TAC THEN 432DISJ_CASES_TAC (ISPEC ``l:num list`` SNOC_CASES) THENL [ 433 ASM_SIMP_TAC list_ss [GENLIST] THEN 434 REPEAT ( 435 CONV_TAC (DEPTH_CONV numLib.num_CONV) THEN 436 SIMP_TAC list_ss [GENLIST, fcpTheory.FCP_BETA, dimindex_16, FILTER_SNOC] 437 ), 438 439restart() 440!l. IS_SORTED_REG_LIST l ==> 441(REGISTER_LIST (enc_REG_LIST l) = (MAP n2w l)) 442 443SIMP_TAC std_ss [enc_REG_LIST_def, MEM, armTheory.REGISTER_LIST_def] THEN 444REPEAT STRIP_TAC THEN 445`(EVERY (\n. n < 16) l)` by PROVE_TAC[IS_SORTED_REG_LIST___EL_SIZE] THEN 446Q.ABBREV_TAC `max = 16` THEN 447`max <= 16` by FULL_SIMP_TAC arith_ss [] THEN 448Q.PAT_ASSUM `Abbrev X` (fn thm => ALL_TAC) THEN 449REPEAT (POP_ASSUM MP_TAC) THEN 450SPEC_TAC (``l:num list``,``l:num list``) THEN 451Induct_on `max` THENL [ 452 Cases_on `l` THEN SIMP_TAC list_ss [GENLIST], 453 454 GEN_TAC THEN 455 DISJ_CASES_TAC (ISPEC ``l:num list`` SNOC_CASES) THENL [ 456 ASM_SIMP_TAC list_ss [] THEN 457 `!x. (x <= 16) ==> (FILTER FST (GENLIST (\i. ((FCP i. F):word16 %% i,(n2w i):word4)) x) = [])` by ALL_TAC THEN1 ( 458 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 459 Induct_on `x` THENL [ 460 SIMP_TAC list_ss [GENLIST], 461 ASM_SIMP_TAC list_ss [GENLIST, FILTER_SNOC, fcpTheory.FCP_BETA, dimindex_16] 462 ] 463 ) THEN 464 ASM_SIMP_TAC std_ss [], 465 466 FULL_SIMP_TAC list_ss [IS_SORTED_REG_LIST___SNOC, EVERY_APPEND, SNOC_APPEND] THEN 467 REPEAT STRIP_TAC THENL [ 468 FULL_SIMP_TAC list_ss [] THEN 469 Q.PAT_ASSUM `SUC max <= 16` MP_TAC THEN 470 Q.PAT_ASSUM `x < SUC max` MP_TAC THEN 471 Q.ABBREV_TAC `max' = SUC max` THEN 472 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 473 SPEC_TAC (``x:num``,``x:num``) THEN 474 Induct_on `max'` THENL [ 475 SIMP_TAC std_ss [], 476 477 REPEAT STRIP_TAC THEN 478 ASM_SIMP_TAC list_ss [GENLIST, FILTER_SNOC, fcpTheory.FCP_BETA, dimindex_16] THEN 479 Cases_on `max' = x` THENL [ 480 ASM_SIMP_TAC list_ss [MAP_SNOC, SNOC_11, GSYM SNOC] THEN 481 `!x y. ((x <= 16) /\ (x <= y)) ==> (FILTER FST (GENLIST (\i. ((FCP i. i = y):word16 %% i,(n2w i):word4)) x) = [])` by ALL_TAC THEN1 ( 482 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 483 Induct_on `x` THENL [ 484 SIMP_TAC list_ss [GENLIST], 485 ASM_SIMP_TAC list_ss [GENLIST, FILTER_SNOC, fcpTheory.FCP_BETA, dimindex_16] 486 ] 487 ) THEN 488 489 `x <= 16` by DECIDE_TAC THEN 490 POP_ASSUM MP_TAC THEN 491 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 492 Induct_on `x` THENL [ 493 SIMP_TAC list_ss [GENLIST], 494 ASM_SIMP_TAC list_ss [GENLIST, FILTER_SNOC, fcpTheory.FCP_BETA, dimindex_16] THEN 495 REPEAT STRIP_TAC THEN 496 FULL_SIMP_TAC arith_ss [] 497 ] 498 499 500 REPEAT ( 501 CONV_TAC (DEPTH_CONV numLib.num_CONV) THEN 502 SIMP_TAC list_ss [GENLIST, fcpTheory.FCP_BETA, dimindex_16, FILTER_SNOC] 503 ), 504 505 506 507 Cases SNOC_CASES THENL SIMP_TAC list_ss [GENLIST] 508 REPEAT STRIP_TAC THEN 509 510 Cases_on `EVERY (\n. n < max) l` THEN1 ( 511 FULL_SIMP_TAC arith_ss [GENLIST, FILTER_SNOC, fcpTheory.FCP_BETA, dimindex_16] 512 513 514 515 516ONCE_REWRITE_TAC [REDEPTH_CONV numLib.num_CONV ``16``] THEN 517REWRITE_TAC[GENLIST] THEN 518SIMP_TAC list_ss [fcpTheory.FCP_BETA, dimindex_16] THEN 519REWRITE_TAC [SNOC] THEN 520 521Induct_on `l` THENL [ 522 SIMP_TAC list_ss [] 523 524 525DB.find "GENLIST" 526DB.find "FCP" 527REGISTER_LIST 528 529 530 531match [] ``LDM`` 532 533ARM_LDM*) 534 535val PRE_TRANS_OPT_def = Define `PRE_TRANS_OPT = transfer_options F F F` 536 537val DOPER2INSTRUCTION_def = Define ` 538 (DOPER2INSTRUCTION (MPOP base regL) = 539 LDM AL T PRE_TRANS_OPT (n2w base) (reg_bitmap (MAP n2w regL))) /\ 540 (DOPER2INSTRUCTION (MPUSH base regL) = 541 STM AL T PRE_TRANS_OPT (n2w base) (reg_bitmap (MAP n2w regL))) /\ 542 (DOPER2INSTRUCTION (MMOV dst src) = 543 MOV AL F (MREG2REG dst) (MEXP2addr_model src)) /\ 544 (DOPER2INSTRUCTION (MADD dst src1 src2) = 545 ADD AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 546 (DOPER2INSTRUCTION (MSUB dst src1 src2) = 547 SUB AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 548 (DOPER2INSTRUCTION (MRSB dst src1 src2) = 549 RSB AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 550 (DOPER2INSTRUCTION (MMUL dst src1 src2_reg) = 551 MUL AL F (MREG2REG dst) (MREG2REG src1) (MREG2REG src2_reg)) /\ 552 (DOPER2INSTRUCTION (MAND dst src1 src2) = 553 AND AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 554 (DOPER2INSTRUCTION (MORR dst src1 src2) = 555 ORR AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 556 (DOPER2INSTRUCTION (MEOR dst src1 src2) = 557 EOR AL F (MREG2REG dst) (MREG2REG src1) (MEXP2addr_model src2)) /\ 558 (DOPER2INSTRUCTION (MLSL dst src2_reg src2_num) = 559 MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num)) /\ 560 (DOPER2INSTRUCTION (MLSR dst src2_reg src2_num) = 561 if (src2_num = 0w) then 562 (*avoid special case rrx*) 563 MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num) 564 else 565 MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSR (MREG2REG src2_reg)) src2_num)) /\ 566 (DOPER2INSTRUCTION (MASR dst src2_reg src2_num) = 567 if (src2_num = 0w) then 568 (*avoid special case rrx*) 569 MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num) 570 else 571 MOV AL F (MREG2REG dst) (Dp_shift_immediate (ASR (MREG2REG src2_reg)) src2_num)) /\ 572 (DOPER2INSTRUCTION (MROR dst src2_reg src2_num) = 573 if (src2_num = 0w) then 574 (*avoid special case rrx*) 575 MOV AL F (MREG2REG dst) (Dp_shift_immediate (LSL (MREG2REG src2_reg)) src2_num) 576 else 577 MOV AL F (MREG2REG dst) (Dp_shift_immediate (ROR (MREG2REG src2_reg)) src2_num)) 578 `; 579 580 581 582val MREG2register_def = Define 583 `MREG2register m r = 584 num2register (mode_reg2num m (MREG2REG r))` 585 586 587val REGS_EQUIVALENT_def = Define 588 `REGS_EQUIVALENT m registers regs = 589 (!r. ((regs ' (MREG2REG r)) = (registers (num2register (mode_reg2num m (MREG2REG r))))))` 590 591val mode_reg2num_11 = store_thm ("mode_reg2num_11", 592``!m v w. 593(mode_reg2num m v = mode_reg2num m w) = (v = w)``, 594 595REPEAT GEN_TAC THEN EQ_TAC THENL [ 596 Cases_on `m` THEN 597 SIMP_TAC std_ss [armTheory.mode_reg2num_def, armTheory.USER_def, LET_THM, w2n_11, 598 armTheory.mode_case_def, armTheory.mode_distinct] THENL [ 599 600 Cases_on `(w2n v = 15) \/ (w2n v < 8)` THEN Cases_on `(w2n w = 15) \/ (w2n w < 8)` THEN 601 FULL_SIMP_TAC arith_ss [GSYM w2n_11], 602 603 ALL_TAC, 604 ALL_TAC, 605 ALL_TAC, 606 ALL_TAC 607 ] THEN ( 608 Cases_on `(w2n v = 15) \/ (w2n v < 13)` THEN Cases_on `(w2n w = 15) \/ (w2n w < 13)` THEN 609 FULL_SIMP_TAC arith_ss [GSYM w2n_11] 610 ), 611 612 SIMP_TAC std_ss [] 613]); 614 615val mode_reg2num___PC = store_thm ("mode_reg2num___PC", 616``!m r. (mode_reg2num m r = 15) = (r = 15w)``, 617 618REPEAT GEN_TAC THEN 619`mode_reg2num m 15w = 15` by EVAL_TAC THEN 620PROVE_TAC[mode_reg2num_11]); 621 622 623 624 625 626 627val MREG_NOT_PC = store_thm ("MREG_NOT_PC", 628 ``(!r. ~(MREG2REG r = 15w)) /\ (!r m. ~(MREG2register m r = r15))``, 629 630 SIMP_TAC std_ss [GSYM FORALL_AND_THM, MREG2REG_def, 631 MREG2register_def, GSYM armTheory.num2register_thm] THEN 632 Cases_on `r` THEN( 633 SIMP_TAC std_ss [index_of_reg_def, arm_evalTheory.mode_reg2num_lt, armTheory.num2register_11, mode_reg2num___PC] THEN 634 WORDS_TAC 635 )); 636 637 638val DECODE_MEXP_def = Define ` 639 (DECODE_MEXP m (MR r) regs = regs (MREG2register m r)) /\ 640 (DECODE_MEXP m (MC s c) regs = ((w2w c):word32 #>> (2 * w2n s)))` 641 642val index_of_reg_lt = store_thm ("index_of_reg_lt", 643 ``!r. index_of_reg r < 15``, 644 Cases_on `r` THEN EVAL_TAC) 645 646val index_of_reg_11 = store_thm ("index_or_reg_11", 647 ``!r r'. ((index_of_reg r = index_of_reg r') = (r = r'))``, 648 Cases_on `r` THEN Cases_on `r'` THEN EVAL_TAC); 649 650val MREG2REG_11 = store_thm ("MREG2REG_11", 651 ``!r r'. ((MREG2REG r = MREG2REG r') = (r = r'))``, 652 REPEAT GEN_TAC THEN EQ_TAC THENL [ 653 ALL_TAC, 654 SIMP_TAC std_ss [] 655 ] THEN 656 SIMP_TAC std_ss [MREG2REG_def, n2w_11, dimword_4] THEN 657 `(index_of_reg r < 15) /\ (index_of_reg r' < 15)` by REWRITE_TAC[index_of_reg_lt] THEN 658 ASM_SIMP_TAC arith_ss [index_of_reg_11]); 659 660 661val MREG2addr_model_thm = store_thm ("MREG2addr_model_thm", 662``!mexp regs mode C. 663 (SND (ADDR_MODE1 regs mode C 664 (IS_DP_IMMEDIATE (MEXP2addr_model mexp)) 665 ((11 >< 0) (addr_mode1_encode (MEXP2addr_model mexp)))) = DECODE_MEXP mode mexp regs)``, 666 667REPEAT GEN_TAC THEN 668Cases_on `mexp` THENL [ 669 SIMP_TAC std_ss [MEXP2addr_model_def, arm_evalTheory.IS_DP_IMMEDIATE_def, 670 armTheory.ADDR_MODE1_def, 671 arm_evalTheory.shift_immediate_enc, 672 instructionTheory.shift_case_def, 673 arm_evalTheory.shift_immediate_shift_register, 674 armTheory.REG_READ_def, 675 armTheory.LSL_def, MREG_NOT_PC, 676 LET_THM, 677 MREG2register_def, 678 DECODE_MEXP_def], 679 680 SIMP_TAC std_ss [MEXP2addr_model_def, arm_evalTheory.IS_DP_IMMEDIATE_def, 681 armTheory.ADDR_MODE1_def, 682 arm_evalTheory.immediate_enc, 683 armTheory.ROR_def, DECODE_MEXP_def] THEN 684 SUBGOAL_TAC `(2w:word8 * w2w c) = n2w (2*w2n c)` THEN1 ( 685 REWRITE_TAC [word_mul_def] THEN 686 WORDS_TAC THEN 687 `w2n c < 16` by METIS_TAC [w2n_lt, dimword_4] THEN 688 ASM_SIMP_TAC arith_ss[] 689 ) THEN 690 ASM_SIMP_TAC std_ss [w2w_def, n2w_w2n, w2n_n2w, dimword_8, dimword_5] THEN 691 Cases_on `n2w (2 * w2n c) = 0w:word8` THENL [ 692 SUBGOAL_TAC `2* w2n c = 0` THEN1 ( 693 `w2n (n2w:num->word8 (2 * w2n c)) = w2n (0w:word8)` by PROVE_TAC[] THEN 694 UNDISCH_HD_TAC THEN 695 WORDS_TAC THEN 696 `w2n c < 16` by METIS_TAC [w2n_lt, dimword_4] THEN 697 ASM_SIMP_TAC arith_ss[] 698 ) THEN 699 ASM_SIMP_TAC std_ss [armTheory.LSL_def] THEN 700 PROVE_TAC[ROR_CYCLE, MULT], 701 702 `w2n c < 16` by METIS_TAC [w2n_lt, dimword_4] THEN 703 ASM_SIMP_TAC arith_ss [] 704 ] 705]); 706 707 708val FETCH_PC___PC_WRITE = store_thm ("FETCH_PC___PC_WRITE", 709 ``!registers v. FETCH_PC (REG_WRITE registers usr 15w v) = v``, 710 711 EVAL_TAC THEN 712 REWRITE_TAC [armTheory.num2register_thm]); 713 714 715val DECODE_SHIFT_def = Define ` 716 (DECODE_SHIFT m (LSL:word4->shift r) (c:word5) (regs:register->word32) = ((regs (num2register (mode_reg2num m r))) << w2n c)) /\ 717 (DECODE_SHIFT m (LSR r) c regs = ((regs (num2register (mode_reg2num m r))) >>> w2n c)) /\ 718 (DECODE_SHIFT m (ASR r) c regs = ((regs (num2register (mode_reg2num m r))) >> w2n c)) /\ 719 (DECODE_SHIFT m (ROR r) c regs = ((regs (num2register (mode_reg2num m r))) #>> w2n c))`; 720 721 722 723val WELL_FORMED_SHIFT_def = Define ` 724 (WELL_FORMED_SHIFT (ROR:word4->shift r) c = ~(c = 0w) /\ ~(r = 15w)) /\ 725 (WELL_FORMED_SHIFT (ASR r) c = ~(c = 0w) /\ ~(r = 15w)) /\ 726 (WELL_FORMED_SHIFT (LSR r) c = ~(c = 0w) /\ ~(r = 15w)) /\ 727 (WELL_FORMED_SHIFT (LSL r) c = ~(r = 15w))`; 728 729 730val STATE_ARM_MEM_EVAL = save_thm ("STATE_ARM_MEM_EVAL", 731 let 732 val def1 = (Q.ISPEC `NO_CP:'a coproc` (SIMP_RULE std_ss [Once (GSYM FORALL_AND_THM)] systemTheory.STATE_ARM_MMU_def)); 733 val def2 = REWRITE_RULE [GSYM systemTheory.NEXT_ARM_MEM_def, GSYM systemTheory.STATE_ARM_MEM_def] def1 734 in 735 def2 736 end) 737 738val STATE_ARM_MEM_SPLIT = store_thm ("STATE_ARM_MEM_SPLIT", 739 ``(!t1 t2 s. STATE_ARM_MEM (t1 + t2) s = (STATE_ARM_MEM t1 (STATE_ARM_MEM t2 s)))``, 740 741 Induct_on `t1` THENL [ 742 SIMP_TAC std_ss [STATE_ARM_MEM_EVAL], 743 744 REPEAT GEN_TAC THEN 745 `SUC t1 + t2 = SUC (t1 + t2)` by DECIDE_TAC THEN 746 FULL_SIMP_TAC std_ss [STATE_ARM_MEM_EVAL] 747 ]); 748 749 750 751val STATE_ARM_MEM_SPLIT___SYM = store_thm ("STATE_ARM_MEM_SPLIT___SYM", 752 ``(!t1 t2 s. STATE_ARM_MEM (t1 + t2) s = (STATE_ARM_MEM t2 (STATE_ARM_MEM t1 s)))``, 753 754 SIMP_TAC arith_ss [GSYM STATE_ARM_MEM_SPLIT]); 755 756 757val DECODE_SHIFT_thm = store_thm ("DECODE_SHIFT_thm", 758``!s c regs mode C. 759 WELL_FORMED_SHIFT s c ==> 760 (SND (ADDR_MODE1 regs mode C 761 (IS_DP_IMMEDIATE (Dp_shift_immediate s c)) 762 ((11 >< 0) (addr_mode1_encode (Dp_shift_immediate s c)))) = DECODE_SHIFT mode s c regs)``, 763 764 REPEAT STRIP_TAC THEN 765 SIMP_TAC std_ss [arm_evalTheory.IS_DP_IMMEDIATE_def, 766 armTheory.ADDR_MODE1_def, 767 arm_evalTheory.shift_immediate_enc, 768 instructionTheory.shift_case_def, 769 arm_evalTheory.shift_immediate_shift_register] THEN 770 Cases_on `c = 0w` THEN ASM_REWRITE_TAC[] THENL [ 771 Cases_on `s` THENL [ 772 FULL_SIMP_TAC std_ss [instructionTheory.shift_case_def, 773 armTheory.LSL_def, DECODE_SHIFT_def, WELL_FORMED_SHIFT_def] THEN 774 WORDS_TAC THEN 775 ASM_SIMP_TAC std_ss [SHIFT_ZERO, armTheory.REG_READ_def, 776 WELL_FORMED_SHIFT_def, armTheory.mode_reg2num_def, LET_THM], 777 778 FULL_SIMP_TAC std_ss [WELL_FORMED_SHIFT_def], 779 FULL_SIMP_TAC std_ss [WELL_FORMED_SHIFT_def], 780 FULL_SIMP_TAC std_ss [WELL_FORMED_SHIFT_def] 781 ], 782 783 SUBGOAL_TAC `~(w2w c = 0w:word8) /\ (w2n ((w2w c):word8) = w2n c)` THEN1 ( 784 WORDS_TAC THEN 785 `w2n c < 32` by METIS_TAC [w2n_lt, dimword_5] THEN 786 ASM_SIMP_TAC arith_ss [w2n_eq_0] 787 ) THEN 788 SUBGOAL_TAC `!c. ~(c = 15w) ==> 789 (REG_READ regs mode c = 790 regs (num2register (mode_reg2num mode c)))` THEN1 ( 791 ASM_SIMP_TAC std_ss [armTheory.REG_READ_def, 792 LET_THM] 793 ) THEN 794 795 Cases_on `s` THEN ( 796 FULL_SIMP_TAC std_ss [instructionTheory.shift_case_def, 797 armTheory.LSL_def, armTheory.LSR_def, armTheory.ASR_def, 798 armTheory.ROR_def, 799 DECODE_SHIFT_def, WELL_FORMED_SHIFT_def] 800 ) 801 ]); 802 803 804val DECODE_MEXP_thm = store_thm ("DECODE_MEXP_thm", 805 ``!registers regs m mem M0. 806 REGS_EQUIVALENT m registers regs ==> 807 (read (regs,mem) (toEXP M0) = DECODE_MEXP m M0 registers)``, 808 809 Cases_on `M0` THENL [ 810 SIMP_TAC std_ss [read_thm, toEXP_def, toREG_def, DECODE_MEXP_def, 811 REGS_EQUIVALENT_def, MREG2register_def, MREG2REG_def] THEN 812 PROVE_TAC[index_of_reg_lt], 813 814 SIMP_TAC std_ss [read_thm, toEXP_def, toREG_def, DECODE_MEXP_def] 815 ]); 816 817 818val MREG2REG_thm = store_thm ("MREG2REG_thm", 819 ``!registers regs mem m M. 820 (REGS_EQUIVALENT m registers regs) ==> 821 (REG_READ registers m (MREG2REG M) = read (regs, mem) (toREG M))``, 822 823 SIMP_TAC std_ss [armTheory.REG_READ_def, MREG_NOT_PC, 824 LET_THM, toREG_def, read_thm, 825 REGS_EQUIVALENT_def, MREG2REG_def] THEN 826 PROVE_TAC[index_of_reg_lt]); 827 828val REGS_EQUIVALENT___WRITE_PC = store_thm ("REGS_EQUIVALENT___WRITE_PC", 829``!registers regs m m' v. 830 REGS_EQUIVALENT m (REG_WRITE registers m' 15w v) regs = 831 REGS_EQUIVALENT m registers regs``, 832 833SIMP_TAC std_ss [REGS_EQUIVALENT_def, armTheory.REG_WRITE_def] THEN 834REPEAT GEN_TAC THEN 835FORALL_EQ_STRIP_TAC THEN 836MATCH_MP_TAC (prove (``((b:word32) = (c:word32)) ==> ((a = b) = (a = c))``, PROVE_TAC[])) THEN 837SIMP_TAC std_ss [combinTheory.UPDATE_def] THEN 838`num2register (mode_reg2num m' 15w) = r15` by (EVAL_TAC THEN REWRITE_TAC[armTheory.num2register_thm]) THEN 839SUBGOAL_TAC `~(r15 = num2register (mode_reg2num m (MREG2REG r)))` THEN1 ( 840 SIMP_TAC arith_ss [GSYM armTheory.num2register_thm, armTheory.num2register_11, arm_evalTheory.mode_reg2num_lt] THEN 841 ONCE_REWRITE_TAC [prove (``15 = mode_reg2num m 15w``, EVAL_TAC)] THEN 842 SIMP_TAC arith_ss [mode_reg2num_11, MREG2REG_def, n2w_11, dimword_4] THEN 843 `index_of_reg r < 15` by REWRITE_TAC[index_of_reg_lt] THEN 844 ASM_SIMP_TAC arith_ss [] 845) THEN 846ASM_REWRITE_TAC[]); 847 848 849 850 851 852val REGS_EQUIVALENT___INC_PC = store_thm ("REGS_EQUIVALENT___INC_PC", 853``!registers regs m. 854 REGS_EQUIVALENT m (INC_PC registers) regs = 855 REGS_EQUIVALENT m registers regs``, 856 857SIMP_TAC std_ss [arm_evalTheory.INC_PC, REGS_EQUIVALENT___WRITE_PC]); 858 859 860val REGS_EQUIVALENT___UPDATE = store_thm ("REGS_EQUIVALENT___UPDATE", 861``!registers regs M x. 862 REGS_EQUIVALENT m registers regs ==> 863 REGS_EQUIVALENT m ((MREG2register m M =+ x) registers) 864 (regs |+ (MREG2REG M, x))``, 865 866SIMP_TAC arith_ss [REGS_EQUIVALENT_def, combinTheory.UPDATE_def, FAPPLY_FUPDATE_THM, 867 MREG2register_def, MREG2REG_def, armTheory.num2register_11, arm_evalTheory.mode_reg2num_lt, mode_reg2num_11, n2w_11, dimword_4] THEN 868REPEAT STRIP_TAC THEN 869`index_of_reg M < 15` by PROVE_TAC[index_of_reg_lt] THEN 870ASM_SIMP_TAC arith_ss [] THEN PROVE_TAC[]); 871 872 873(*a very specialised tactic for data operations which get a register and an addr_mode1*) 874 875fun doper_reg_reg_addr_mode1 thm = 876 REPEAT GEN_TAC THEN STRIP_TAC THEN 877 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] thm) THEN 878 Q_SPECL_NO_ASSUM 0 [`state_old`, `F`, `AL:condition`, `MREG2REG M0`, `MREG2REG M'`, `(MEXP2addr_model M1)`] THEN 879 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 880 FULL_SIMP_TAC std_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 881 armTheory.condition_case_def] 882 ) THEN 883 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, 884 REG_OWRT_ALL] THEN WEAKEN_HD_TAC THEN 885 886 Q.PAT_UNDISCH_TAC `(reg',mem') = mdecode (reg, mem) X` THEN 887 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, MREG2addr_model_thm, 888 LET_THM, GSYM MREG2register_def, 889 mdecode_def] THEN 890 `read (reg,mem) (toEXP M1) = DECODE_MEXP m M1 state_old.registers` by 891 PROVE_TAC[DECODE_MEXP_thm] THEN 892 `read (reg,mem) (toREG M0) = REG_READ state_old.registers m (MREG2REG M0)` by 893 PROVE_TAC[MREG2REG_thm] THEN 894 ASM_SIMP_TAC std_ss [write_thm, toREG_def] THEN 895 REPEAT STRIP_TAC THENL [ 896 ASM_SIMP_TAC std_ss [REGS_EQUIVALENT___INC_PC, REGS_EQUIVALENT___UPDATE, 897 GSYM MREG2REG_def], 898 SIMP_TAC std_ss [armTheory.INC_PC_def, 899 armTheory.FETCH_PC_def, 900 combinTheory.UPDATE_def, 901 MREG_NOT_PC] 902 ]; 903 904(*a very specialised tactic for shift operations*) 905fun doper_shift s_term = 906 REPEAT GEN_TAC THEN STRIP_TAC THEN 907 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_MOV) THEN 908 Q_SPECL_NO_ASSUM 0 [`state_old`, `F`, `AL:condition`, `MREG2REG M'`, `MREG2REG M'`] THEN 909 Cases_on `c = 0w` THENL [ 910 SPEC_NO_ASSUM 1 ``Dp_shift_immediate (LSL (MREG2REG M0)) c``, 911 912 SPEC_NO_ASSUM 1 (list_mk_comb (``Dp_shift_immediate``, 913 [mk_comb (s_term, ``MREG2REG M0``), 914 ``c:word5``])) 915 ] THEN ( 916 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 917 FULL_SIMP_TAC std_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 918 armTheory.condition_case_def] 919 ) THEN 920 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, REG_OWRT_ALL] THEN WEAKEN_HD_TAC THEN 921 922 `read (reg,mem) (toREG M0) = REG_READ state_old.registers m (MREG2REG M0)` by 923 PROVE_TAC[MREG2REG_thm] THEN 924 Q.PAT_UNDISCH_TAC `(reg',mem') = mdecode (reg, mem) X` THEN 925 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, DECODE_SHIFT_thm, 926 WELL_FORMED_SHIFT_def, MREG_NOT_PC, 927 DECODE_SHIFT_def, SHIFT_ZERO, word_0_n2w, 928 LET_THM, GSYM MREG2register_def, 929 mdecode_def, toREG_def, write_thm, 930 systemTheory.arm_sys_state_accfupds, 931 armTheory.REG_READ_def, 932 REGS_EQUIVALENT___INC_PC, 933 REGS_EQUIVALENT___UPDATE, 934 GSYM MREG2REG_def] THEN 935 SIMP_TAC std_ss [armTheory.INC_PC_def, 936 armTheory.FETCH_PC_def, 937 combinTheory.UPDATE_def, 938 MREG_NOT_PC] 939 ) 940 941 942 943val DOPER2INSTRUCTION_NO_MEM_thm = store_thm ("DOPER2INSTRUCTION_NO_MEM_thm", 944`` 945!oper reg mem reg' mem' m 946 state_old state_new. 947(~(IS_MEMORY_DOPER oper) /\ (IS_WELL_FORMED_DOPER oper) /\ 948 (state_old.memory ((31 >< 2) (state_old.registers r15)) = 949 enc (DOPER2INSTRUCTION oper)) /\ 950 (~state_old.undefined) /\ 951 (Abbrev (m = (DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs))))) /\ 952 ((reg', mem') = mdecode (reg,mem) oper) /\ 953 (state_new = NEXT_ARM_MEM state_old) /\ 954 (REGS_EQUIVALENT m state_old.registers reg)) ==> 955 956 ((REGS_EQUIVALENT m state_new.registers reg') /\ 957 (mem' = mem) /\ (state_new.memory = state_old.memory) /\ 958 (~state_new.undefined) /\ 959 (state_new.psrs = state_old.psrs) /\ 960 (state_new.cp_state = state_old.cp_state) /\ 961 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 962 (FETCH_PC state_new.registers = FETCH_PC state_old.registers + 4w) 963 )``, 964 965SIMP_TAC std_ss [] THEN 966Cases_on `oper` THEN 967REWRITE_TAC[IS_MEMORY_DOPER_def, IS_WELL_FORMED_DOPER_def, DOPER2INSTRUCTION_def, 968 owrt_visible_regs_def, state_mode_def] THENL [ 969 970 (*MOV*) 971 REPEAT GEN_TAC THEN STRIP_TAC THEN 972 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_MOV) THEN 973 Q_SPECL_NO_ASSUM 0 [`state_old`, `F`, `AL:condition`, `MREG2REG M'`, `MREG2REG M'`, `(MEXP2addr_model M0)`] THEN 974 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 975 FULL_SIMP_TAC std_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 976 armTheory.condition_case_def] 977 ) THEN 978 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds,systemTheory.arm_sys_state_accessors, 979 REG_OWRT_ALL] THEN 980 981 `read (reg,mem) (toEXP M0) = DECODE_MEXP m M0 state_old.registers` by 982 PROVE_TAC[DECODE_MEXP_thm] THEN 983 Q.PAT_UNDISCH_TAC `(reg',mem') = mdecode (reg, mem) X` THEN 984 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, MREG2addr_model_thm, 985 GSYM MREG2register_def, 986 mdecode_def, toREG_def, write_thm] THEN 987 REPEAT STRIP_TAC THENL [ 988 ASM_SIMP_TAC std_ss [REGS_EQUIVALENT___INC_PC, REGS_EQUIVALENT___UPDATE, GSYM MREG2REG_def], 989 SIMP_TAC std_ss [armTheory.INC_PC_def, 990 armTheory.FETCH_PC_def, 991 MREG_NOT_PC, 992 combinTheory.UPDATE_def] 993 ], 994 995 996 doper_reg_reg_addr_mode1 ARM_ADD, 997 doper_reg_reg_addr_mode1 ARM_SUB, 998 doper_reg_reg_addr_mode1 ARM_RSB, 999 1000 (*MUL*) 1001 REPEAT GEN_TAC THEN STRIP_TAC THEN 1002 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_MUL) THEN 1003 Q_SPECL_NO_ASSUM 0 [`state_old`, `F`, `AL:condition`, `MREG2REG M1`, `MREG2REG M0`, `MREG2REG M'`] THEN 1004 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1005 FULL_SIMP_TAC arith_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 1006 armTheory.condition_case_def, MREG2REG_11] 1007 ) THEN 1008 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, REG_OWRT_ALL] THEN WEAKEN_HD_TAC THEN 1009 1010 Q.PAT_UNDISCH_TAC `(reg',mem') = mdecode (reg, mem) X` THEN 1011 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, MREG2addr_model_thm, 1012 LET_THM, GSYM MREG2register_def, 1013 mdecode_def] THEN 1014 `read (reg,mem) (toREG M0) = REG_READ state_old.registers m (MREG2REG M0)` by 1015 PROVE_TAC[MREG2REG_thm] THEN 1016 `read (reg,mem) (toREG M1) = REG_READ state_old.registers m (MREG2REG M1)` by 1017 PROVE_TAC[MREG2REG_thm] THEN 1018 ASM_SIMP_TAC std_ss [write_thm, toREG_def] THEN 1019 REPEAT STRIP_TAC THENL [ 1020 ASM_SIMP_TAC std_ss [REGS_EQUIVALENT___INC_PC, REGS_EQUIVALENT___UPDATE, GSYM MREG2REG_def], 1021 SIMP_TAC std_ss [armTheory.INC_PC_def, 1022 armTheory.FETCH_PC_def, 1023 combinTheory.UPDATE_def, 1024 MREG_NOT_PC] 1025 ], 1026 1027 1028 doper_reg_reg_addr_mode1 ARM_AND, 1029 doper_reg_reg_addr_mode1 ARM_ORR, 1030 doper_reg_reg_addr_mode1 ARM_EOR, 1031 1032 doper_shift ``LSL:word4->shift``, 1033 doper_shift ``LSR:word4->shift``, 1034 doper_shift ``ASR:word4->shift``, 1035 doper_shift ``ROR:word4->shift`` 1036]); 1037 1038val DOPER2INSTRUCTION_thm = save_thm ("DOPER2INSTRUCTION_thm", DOPER2INSTRUCTION_NO_MEM_thm); 1039 1040val MEMORY_SLICE_def = Define ` 1041 MEMORY_SLICE (base, length) = 1042 (MAP (\off. base - n2w off) (LIST_COUNT length))` 1043 1044val MEM_EQUIV_EXCEPT_SLICE_def = Define ` 1045 MEM_EQUIV_EXCEPT_SLICE (base, length) (mem, mem') = 1046 !slice. (slice = (MEMORY_SLICE (base, length))) ==> 1047 (((FDOM mem) UNION (LIST_TO_SET slice) = 1048 (FDOM mem') UNION (LIST_TO_SET slice)) /\ 1049 (!l. ~(MEM l slice) ==> (mem ' l = mem' ' l)))`; 1050 1051 1052val REGS_EQUIVALENT_MEM_def = Define ` 1053 REGS_EQUIVALENT_MEM m (offset, length) (registers, memory) (regs, mem) = 1054 REGS_EQUIVALENT m registers regs /\ 1055 (!l. (MEM l (MEMORY_SLICE ((MEM_ADDR (regs ' 13w) + offset), length)) ==> 1056 (mem ' l = memory l)))` 1057 1058 1059val REGS_EQUIVALENT_MEM___NO_MEM = 1060 store_thm ("REGS_EQUIVALENT_MEM___NO_MEM", 1061``!m offset registers memory regs mem. 1062REGS_EQUIVALENT_MEM m (offset, 0) (registers, memory) (regs, mem) = 1063REGS_EQUIVALENT m registers regs``, 1064 1065SIMP_TAC list_ss [REGS_EQUIVALENT_MEM_def, LIST_COUNT_def, MEMORY_SLICE_def]); 1066 1067 1068val REGS_EQUIVALENT___SP = 1069 store_thm ("REGS_EQUIVALENT___SP", 1070 ``!m registers reg. REGS_EQUIVALENT m registers reg ==> 1071 (registers (num2register (mode_reg2num m 13w)) = reg ' 13w)``, 1072 1073 SIMP_TAC std_ss [REGS_EQUIVALENT_def] THEN 1074 REPEAT STRIP_TAC THEN 1075 POP_ASSUM (fn thm => MP_TAC (Q.SPEC `R13` thm)) THEN 1076 SIMP_TAC std_ss [MREG2REG_def, index_of_reg_def]); 1077 1078 1079val pushL_mem_def = Define `pushL_mem (reg, mem) r off l = 1080FST (FOLDL (\(mem',i) reg'. (mem' |+ 1081 (MEM_ADDR (reg ' (n2w r)) - n2w i,reg ' (n2w reg')), 1082 i + 1)) (mem,off) (REVERSE l))` 1083 1084 1085val pushL_thm = store_thm ("pushL_thm", 1086``!l reg mem r. 1087pushL (reg, mem) r l = (reg |+ (n2w r, reg ' (n2w r) - n2w (4*(LENGTH l))), 1088 pushL_mem (reg, mem) r 0 l)``, 1089 1090 1091`!l reg mem reg' mem' r init. 1092(FOLDL (\(st1,i) reg''. (write st1 (MEM (r,NEG i)) (read (reg',mem') reg''), 1093 i + 1)) ((reg,mem),init) (REVERSE (MAP REG l))) = 1094(FOLDL (\(st1,i) reg''. (write st1 (MEM (r,NEG i)) (reg' ' (n2w reg'')), 1095 i + 1)) ((reg,mem),init) (REVERSE l))` by ALL_TAC THEN1 1096( 1097 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 1098 SIMP_TAC list_ss [], 1099 ASM_SIMP_TAC list_ss [REVERSE_SNOC, MAP_SNOC, read_thm, write_thm] 1100 ] 1101) THEN 1102 1103 1104`!l reg mem r init. 1105(FOLDL (\(st1,i) reg'. (write st1 (MEM (r,NEG i)) (read (reg,mem) reg'), 1106 i + 1)) ((reg,mem),init) (REVERSE (MAP REG l))) = 1107 1108let (mem, i) = 1109 (FOLDL (\(mem',i) reg'. (mem' |+ ((MEM_ADDR (reg ' (n2w r)) - (n2w i)), reg ' (n2w reg')), i + 1)) (mem, init) (REVERSE l)) in 1110((reg, mem), i)` by ALL_TAC THEN1 ( 1111 ASM_SIMP_TAC std_ss [] THEN 1112 POP_ASSUM (fn thm => ALL_TAC) THEN 1113 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 1114 SIMP_TAC list_ss [LET_THM], 1115 ASM_SIMP_TAC list_ss [MAP_SNOC, REVERSE_SNOC, write_thm, read_thm, LET_THM] 1116 ] 1117) THEN 1118REWRITE_TAC[pushL_mem_def] THEN 1119INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 1120 SIMP_TAC list_ss [pushL_def, WORD_SUB_RZERO, read_thm, write_thm], 1121 1122 FULL_SIMP_TAC list_ss [pushL_def, LET_THM] THEN 1123 PairRules.PBETA_TAC THEN 1124 SIMP_TAC std_ss [write_thm, read_thm] 1125]) 1126 1127 1128 1129val pushL_mem_thm = store_thm ("pushL_mem_thm", `` 1130 (!reg mem r off. (pushL_mem (reg, mem) r off [] = mem)) /\ 1131 (!reg mem r off h l. (pushL_mem (reg, mem) r off (SNOC h l) = 1132 pushL_mem (reg, mem |+ ((MEM_ADDR (reg ' (n2w r)) - (n2w off)), reg ' (n2w h))) r (SUC off) l))``, 1133 1134 SIMP_TAC list_ss [pushL_mem_def, FOLDL_APPEND] THEN 1135 REPEAT GEN_TAC THEN 1136 AP_TERM_TAC THEN 1137 Q.SPEC_TAC (`mem`, `mem`) THEN 1138 Q.SPEC_TAC (`reg`, `reg`) THEN 1139 Q.SPEC_TAC (`off`, `off`) THEN 1140 Q.SPEC_TAC (`h`, `h`) THEN 1141 Q.SPEC_TAC (`l`, `l`) THEN 1142 INDUCT_THEN SNOC_INDUCT ASSUME_TAC THENL [ 1143 SIMP_TAC list_ss [SNOC], 1144 ASM_SIMP_TAC list_ss [FOLDL_APPEND, Once REVERSE_SNOC, SUC_ONE_ADD] 1145 ]) 1146 1147(* 1148val DOPER2INSTRUCTION_thm = store_thm ("DOPER2INSTRUCTION_thm", 1149`` 1150!oper reg mem reg' mem' m off stack_size 1151 state_old state_new sp. 1152(((p,n,T) = STACK_SIZE_DOPER oper) /\ 1153 (state_old.memory ((31 >< 2) (state_old.registers r15)) = 1154 enc (DOPER2INSTRUCTION oper)) /\ 1155 (~state_old.undefined) /\ 1156 (stack_size >= n) /\ 1157 (Abbrev (m = (DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs))))) /\ 1158 (sp = num2register (mode_reg2num m 13w)) /\ 1159 ((reg', mem') = mdecode (reg,mem) oper) /\ 1160 (state_new = NEXT_ARM_MEM state_old) /\ 1161 (REGS_EQUIVALENT_MEM m (off, stack_size) (state_old.registers, state_old.memory) (reg, mem))) ==> 1162 1163 ((REGS_EQUIVALENT_MEM m (off + n2w n - n2w p, stack_size + p) (state_new.registers, state_new.memory) (reg', mem')) /\ 1164 (MEM_EQUIV_EXCEPT_SLICE (MEM_ADDR (state_new.registers sp), p) (mem, mem')) /\ 1165 (~state_new.undefined) /\ 1166 (state_new.psrs = state_old.psrs) /\ 1167 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 1168 (FETCH_PC state_new.registers = FETCH_PC state_old.registers + 4w) 1169 )``, 1170restart() 1171 1172 1173GEN_TAC THEN 1174Cases_on `~IS_MEMORY_DOPER oper` THENL [ 1175 REPEAT GEN_TAC THEN STRIP_TAC THEN 1176 IMP_RES_TAC (GSYM VALID_STACK_SIZE_DOPER___IMPLIES___WELL_FORMED) THEN 1177 Q.PAT_ASSUM `Y = STACK_SIZE_DOPER X` MP_TAC THEN 1178 IMP_RES_TAC NOT_MEMORY_DOPER___STACK_SIZE_DOPER THEN 1179 Q.PAT_ASSUM `(reg', mem') = X` (fn thm=> ASSUME_TAC (GSYM thm)) THEN 1180 ASM_SIMP_TAC std_ss [WORD_ADD_0, WORD_SUB_RZERO] THEN 1181 STRIP_TAC THEN 1182 FULL_SIMP_TAC std_ss [REGS_EQUIVALENT_MEM_def] THEN 1183 MP_TAC (Q.SPECL [`oper`, `reg`, `mem`, `reg'`, `mem'`, `state_old`] (SIMP_RULE std_ss [markerTheory.Abbrev_def] DOPER2INSTRUCTION_NO_MEM_thm)) THEN 1184 ASM_SIMP_TAC std_ss [MEM_EQUIV_EXCEPT_SLICE_def] THEN 1185 REPEAT STRIP_TAC THEN 1186 REMAINS_TAC `(reg ' 13w) = (reg' ' 13w)` THEN1 PROVE_TAC[] THEN 1187 Q.PAT_ASSUM `mdecode X oper = Y` (fn thm => MP_TAC (GSYM thm)) THEN 1188 Q.PAT_ASSUM `~(IS_MEMORY_DOPER oper)` MP_TAC THEN 1189 Q.PAT_ASSUM `STACK_SIZE_DOPER X = Y` MP_TAC THEN 1190 REPEAT (POP_ASSUM (fn thm => ALL_TAC)) THEN 1191 1192 `!M. (M = R13) = (13w:word4 = n2w (index_of_reg M))` by ALL_TAC THEN1 ( 1193 Cases_on `M` THEN 1194 SIMP_TAC std_ss [index_of_reg_def, n2w_11, dimword_4, MREG_distinct] 1195 ) THEN 1196 1197 Cases_on `oper` THEN ( 1198 ASM_SIMP_TAC std_ss [IS_MEMORY_DOPER_def, mdecode_def, toREG_def, write_thm, 1199 STACK_SIZE_DOPER_def, FAPPLY_FUPDATE_THM] 1200 ), 1201 1202 1203 UNDISCH_HD_TAC THEN 1204 Cases_on `oper` THEN REWRITE_TAC[IS_MEMORY_DOPER_def] THENL [ 1205 SIMP_TAC std_ss [STACK_SIZE_DOPER_def], 1206 SIMP_TAC std_ss [STACK_SIZE_DOPER_def], 1207 1208 1209 SIMP_TAC std_ss [STACK_SIZE_DOPER_def, DOPER2INSTRUCTION_def, 1210 WORD_ADD_0] THEN 1211 REPEAT GEN_TAC THEN STRIP_TAC THEN 1212 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_STM) THEN 1213 Q_SPECL_NO_ASSUM 0 [`state_old`, `PRE_TRANS_OPT`, `(reg_bitmap (MAP n2w l))`, `AL:condition`, `13w:word4`] THEN 1214 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1215 FULL_SIMP_TAC arith_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 1216 armTheory.condition_case_def, MREG2REG_11] 1217 ) THEN 1218 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, REG_OWRT_ALL, 1219 instructionTheory.transfer_options_accessors, owrt_visible_regs_def, PRE_TRANS_OPT_def] THEN WEAKEN_HD_TAC THEN 1220 FULL_SIMP_TAC std_ss [armTheory.ADDR_MODE4_def, REGISTER_LIST___reg_bitmap, LET_THM, LENGTH_MAP, 1221 armTheory.FIRST_ADDRESS_def, armTheory.WB_ADDRESS_def, 1222 armTheory.UP_DOWN_def] THEN 1223 MATCH_MP_TAC (prove (``((c /\ d) /\ (a /\ b)) ==> ((a:bool) /\ b /\ c /\ d)``, PROVE_TAC[])) THEN 1224 CONJ_TAC THENL [ 1225 SIMP_TAC std_ss [armTheory.INC_PC_def, 1226 armTheory.FETCH_PC_def, 1227 combinTheory.UPDATE_def, 1228 state_mode_def, armTheory.CPSR_READ_def, 1229 systemTheory.arm_sys_state_accfupds], 1230 1231 FULL_SIMP_TAC std_ss [mdecode_def, pushL_thm, REGS_EQUIVALENT_MEM_def, 1232 MEM_EQUIV_EXCEPT_SLICE_def], 1233 1234 DB.find "pushL" 1235 1236 DB.find "UP_DOWN_def" 1237 Q.PAT_UNDISCH_TAC `(reg',mem') = mdecode (reg, mem) X` THEN 1238 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, MREG2addr_model_thm, 1239 LET_THM, GSYM MREG2register_def, 1240 mdecode_def] THEN 1241 `read (reg,mem) (toREG M0) = REG_READ state_old.registers m (MREG2REG M0)` by 1242 PROVE_TAC[MREG2REG_thm] THEN 1243 `read (reg,mem) (toREG M1) = REG_READ state_old.registers m (MREG2REG M1)` by 1244 PROVE_TAC[MREG2REG_thm] THEN 1245 ASM_SIMP_TAC std_ss [write_thm, toREG_def] THEN 1246 REPEAT STRIP_TAC THENL [ 1247 ASM_SIMP_TAC std_ss [REGS_EQUIVALENT___INC_PC, REGS_EQUIVALENT___UPDATE, GSYM MREG2REG_def], 1248 SIMP_TAC std_ss [armTheory.INC_PC_def, 1249 armTheory.FETCH_PC_def, 1250 combinTheory.UPDATE_def, 1251 MREG_NOT_PC] 1252 ], 1253 1254 1255 1256*) 1257 1258 1259 1260 1261val DOPER2INSTRUCTION_LIST_def = Define ` 1262 DOPER2INSTRUCTION_LIST doper = 1263 [DOPER2INSTRUCTION doper]` 1264 1265 1266val TRANSLATE_COND_def = Define ` 1267 (TRANSLATE_COND (EQ:COND) = (EQ:condition)) /\ 1268 (TRANSLATE_COND (CS:COND) = (CS:condition)) /\ 1269 (TRANSLATE_COND (MI:COND) = (MI:condition)) /\ 1270 (TRANSLATE_COND (VS:COND) = (VS:condition)) /\ 1271 (TRANSLATE_COND (HI:COND) = (HI:condition)) /\ 1272 (TRANSLATE_COND (GE:COND) = (GE:condition)) /\ 1273 (TRANSLATE_COND (GT:COND) = (GT:condition)) /\ 1274 (TRANSLATE_COND (AL:COND) = (AL:condition)) /\ 1275 (TRANSLATE_COND (NE:COND) = (NE:condition)) /\ 1276 (TRANSLATE_COND (CC:COND) = (CC:condition)) /\ 1277 (TRANSLATE_COND (PL:COND) = (PL:condition)) /\ 1278 (TRANSLATE_COND (VC:COND) = (VC:condition)) /\ 1279 (TRANSLATE_COND (LS:COND) = (LS:condition)) /\ 1280 (TRANSLATE_COND (LT:COND) = (LT:condition)) /\ 1281 (TRANSLATE_COND (LE:COND) = (LE:condition)) /\ 1282 (TRANSLATE_COND (NV:COND) = (NV:condition))` 1283 1284val CJ2INSTRUCTION_LIST_def = Define ` 1285 CJ2INSTRUCTION_LIST (r, c, e) j = 1286 [CMP AL (MREG2REG r) (MEXP2addr_model e); 1287 B (TRANSLATE_COND c) j]` 1288 1289 1290val CJ2INSTRUCTION_LIST_thm = store_thm ("CJ2INSTRUCTION_LIST_thm", 1291`` 1292!r c e j tprog 1293 state_old state_new m reg mem. 1294((tprog = CJ2INSTRUCTION_LIST (r, c, e) j) /\ 1295 (!e. (e < LENGTH tprog) ==> 1296 (state_old.memory (ADDR30 (FETCH_PC state_old.registers + n2w (e*4))) = 1297 (enc (EL e tprog)))) /\ 1298 (~state_old.undefined) /\ 1299 (REGS_EQUIVALENT m state_old.registers reg) /\ 1300 1301 (Abbrev (m = (DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs))))) /\ 1302 (state_new = STATE_ARM_MEM (LENGTH tprog) state_old)) ==> 1303 1304 ((state_new.memory = state_old.memory) /\ 1305 (~state_new.undefined) /\ 1306 (?N Z C V. state_new.psrs = CPSR_WRITE state_old.psrs (SET_NZCV (N,Z,C,V) (CPSR_READ state_old.psrs))) /\ 1307 (state_new.cp_state = state_old.cp_state) /\ 1308 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 1309 (REGS_EQUIVALENT m state_new.registers reg) /\ 1310 (state_new.registers = if (eval_il_cond (r, c, e) (reg, mem)) then 1311 (REG_WRITE state_old.registers usr 15w 1312 (state_old.registers r15 + (n2w (4*(LENGTH tprog))) + 4w + sw2sw j << 2)) 1313 else (REG_WRITE state_old.registers usr 15w (state_old.registers r15 + (n2w (4*(LENGTH tprog))))))) 1314``, 1315 1316ASM_SIMP_TAC list_ss [prove (``!e1. (e1 < 2) = ((e1 = 0) \/ (e1 = 1))``, DECIDE_TAC), CJ2INSTRUCTION_LIST_def, DISJ_IMP_THM, FORALL_AND_THM, WORD_ADD_0] THEN 1317REWRITE_TAC[prove (``2 = SUC (SUC 0)``,DECIDE_TAC), STATE_ARM_MEM_EVAL] THEN 1318REPEAT GEN_TAC THEN STRIP_TAC THEN 1319ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_CMP) THEN 1320Q_SPECL_NO_ASSUM 0 [`state_old`, `AL:condition`, `MREG2REG r`, `(MEXP2addr_model e)`] THEN 1321PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1322 FULL_SIMP_TAC std_ss [MREG_NOT_PC, armTheory.CONDITION_PASSED2_def, armTheory.NZCV_def, 1323 armTheory.condition_case_def, systemTheory.ADDR30_def, armTheory.FETCH_PC_def] 1324) THEN 1325 1326SUBGOAL_TAC `CONDITION_PASSED2 (NZCV (CPSR_READ (NEXT_ARM_MEM state_old).psrs)) (TRANSLATE_COND c) = eval_il_cond (r,c,e) (reg,mem)` THEN1 ( 1327 `REG_READ state_old.registers m (MREG2REG r) = read (reg,mem) (toREG r)` by 1328 PROVE_TAC[MREG2REG_thm] THEN 1329 `DECODE_MEXP m e state_old.registers = read (reg,mem) (toEXP e)` by 1330 PROVE_TAC[DECODE_MEXP_thm] THEN 1331 ASSUME_TAC ARMCompositionTheory.eval_cond_thm THEN 1332 Q_SPECL_NO_ASSUM 0 [`toREG r`, `c`, `toEXP e`, `(reg, mem)`, `(CPSR_READ state_old.psrs)`] THEN 1333 1334 FULL_SIMP_TAC std_ss [armTheory.CONDITION_PASSED2_def, eval_il_cond_def, translate_condition_def, TRANSLATE_COND_def, 1335 systemTheory.arm_sys_state_accfupds, arm_evalTheory.CPSR_WRITE_READ, 1336 MREG2addr_model_thm, arm_evalTheory.DECODE_NZCV_SET_NZCV, 1337 armTheory.NZCV_def] THEN 1338 Cases_on `c` THEN 1339 SIMP_TAC std_ss [decode_cond_cpsr_def, TRANSLATE_COND_def, 1340 armTheory.condition_case_def, setNZCV_thm] 1341) THEN 1342 1343Cases_on `eval_il_cond (r, c, e) (reg, mem)` THENL [ 1344 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] arm_rulesTheory.ARM_B) THEN 1345 Q_SPECL_NO_ASSUM 0 [`NEXT_ARM_MEM state_old`, `j`, `TRANSLATE_COND c`] THEN 1346 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1347 FULL_SIMP_TAC std_ss [MREG_NOT_PC, systemTheory.arm_sys_state_accfupds, 1348 armTheory.INC_PC_def, combinTheory.APPLY_UPDATE_THM, 1349 systemTheory.ADDR30_def, armTheory.FETCH_PC_def] 1350 ) THEN 1351 1352 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, 1353 arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1354 owrt_visible_regs_def, state_mode_def, arm_evalTheory.CPSR_WRITE_READ, 1355 REG_OWRT_ALL] THEN 1356 REPEAT STRIP_TAC THENL [ 1357 METIS_TAC[], 1358 1359 ASM_SIMP_TAC std_ss [REGS_EQUIVALENT___WRITE_PC, REGS_EQUIVALENT___INC_PC], 1360 1361 REPEAT WEAKEN_HD_TAC THEN 1362 SIMP_TAC std_ss [arm_evalTheory.INC_PC, arm_evalTheory.REG_WRITE_WRITE] THEN 1363 AP_TERM_TAC THEN 1364 AP_THM_TAC THEN AP_TERM_TAC THEN 1365 ASM_SIMP_TAC std_ss [armTheory.REG_WRITE_def, armTheory.mode_reg2num_def, arm_evalTheory.USER_usr, LET_THM] THEN 1366 WORDS_TAC THEN 1367 SIMP_TAC std_ss [armTheory.num2register_thm, combinTheory.APPLY_UPDATE_THM, GSYM WORD_ADD_ASSOC] THEN 1368 WORDS_TAC 1369 ], 1370 1371 1372 1373 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] ARM_B_NOP) THEN 1374 Q_SPECL_NO_ASSUM 0 [`NEXT_ARM_MEM state_old`, `j`, `TRANSLATE_COND c`] THEN 1375 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1376 FULL_SIMP_TAC std_ss [MREG_NOT_PC, systemTheory.arm_sys_state_accfupds, 1377 armTheory.INC_PC_def, combinTheory.APPLY_UPDATE_THM, 1378 systemTheory.ADDR30_def, armTheory.FETCH_PC_def] 1379 ) THEN 1380 1381 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, 1382 arm_evalTheory.CPSR_WRITE_READ, REGS_EQUIVALENT___WRITE_PC, 1383 arm_evalTheory.INC_PC, arm_evalTheory.REG_WRITE_WRITE, 1384 arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1385 owrt_visible_regs_def, state_mode_def, arm_evalTheory.CPSR_WRITE_READ, 1386 REG_OWRT_ALL] THEN 1387 REPEAT STRIP_TAC THENL [ 1388 METIS_TAC[], 1389 1390 AP_TERM_TAC THEN 1391 SIMP_TAC std_ss [armTheory.REG_WRITE_def, armTheory.mode_reg2num_def, arm_evalTheory.USER_usr, LET_THM] THEN 1392 WORDS_TAC THEN 1393 SIMP_TAC std_ss [armTheory.num2register_thm, combinTheory.APPLY_UPDATE_THM, GSYM WORD_ADD_ASSOC] THEN 1394 WORDS_TAC 1395 ] 1396]); 1397 1398 1399 1400 1401 1402val CONTAINS_MEMORY_DOPER_def = Define ` 1403 (CONTAINS_MEMORY_DOPER (BLK l) = EXISTS IS_MEMORY_DOPER l) /\ 1404 (CONTAINS_MEMORY_DOPER (SC prog1 prog2) = ((CONTAINS_MEMORY_DOPER prog1) \/ (CONTAINS_MEMORY_DOPER prog2))) /\ 1405 (CONTAINS_MEMORY_DOPER (CJ cond prog1 prog2) = ((CONTAINS_MEMORY_DOPER prog1) \/ (CONTAINS_MEMORY_DOPER prog2))) /\ 1406 (CONTAINS_MEMORY_DOPER (TR cond prog1) = (CONTAINS_MEMORY_DOPER prog1))`; 1407 1408val IS_WELL_FORMED_CTL_STRUCTURE_def = Define ` 1409 (IS_WELL_FORMED_CTL_STRUCTURE (BLK l) = EVERY IS_WELL_FORMED_DOPER l) /\ 1410 (IS_WELL_FORMED_CTL_STRUCTURE (SC prog1 prog2) = (IS_WELL_FORMED_CTL_STRUCTURE prog1 /\ IS_WELL_FORMED_CTL_STRUCTURE prog2)) /\ 1411 (IS_WELL_FORMED_CTL_STRUCTURE (CJ cond prog1 prog2) = (IS_WELL_FORMED_CTL_STRUCTURE prog1 /\ IS_WELL_FORMED_CTL_STRUCTURE prog2)) /\ 1412 (IS_WELL_FORMED_CTL_STRUCTURE (TR cond prog1) = (IS_WELL_FORMED_CTL_STRUCTURE prog1))`; 1413 1414 1415val CTL_STRUCTURE2INSTRUCTION_LIST_def = Define ` 1416 (CTL_STRUCTURE2INSTRUCTION_LIST (BLK l) = FLAT ((MAP DOPER2INSTRUCTION_LIST) l)) /\ 1417 (CTL_STRUCTURE2INSTRUCTION_LIST (SC prog1 prog2) = 1418 (CTL_STRUCTURE2INSTRUCTION_LIST prog1) ++ (CTL_STRUCTURE2INSTRUCTION_LIST prog2)) /\ 1419 1420 (CTL_STRUCTURE2INSTRUCTION_LIST (CJ cond prog1 prog2) = 1421 (CJ2INSTRUCTION_LIST cond (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog2)))) ++ 1422 (CTL_STRUCTURE2INSTRUCTION_LIST prog2) ++ 1423 [B AL (if (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog1) = 0) then 1424 ($- 1w) else 1425 (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog1) - 1)))] ++ 1426 (CTL_STRUCTURE2INSTRUCTION_LIST prog1)) /\ 1427 1428 1429 (CTL_STRUCTURE2INSTRUCTION_LIST (TR cond prog1) = 1430 (CJ2INSTRUCTION_LIST cond (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog1)))) ++ 1431 (CTL_STRUCTURE2INSTRUCTION_LIST prog1) ++ 1432 [B AL ($- (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog1) + 1433 LENGTH (CJ2INSTRUCTION_LIST cond (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog1)))) + 2)))])`; 1434 1435 1436 1437 1438val DOPER2INSTRUCTION_LIST_thm = store_thm ("DOPER2INSTRUCTION_LIST_thm", 1439`` 1440!oper tprog reg mem reg' mem' m 1441 state_old state_new. 1442(~(IS_MEMORY_DOPER oper) /\ (IS_WELL_FORMED_DOPER oper) /\ 1443 (tprog = DOPER2INSTRUCTION_LIST oper) /\ 1444 (!e. (e < LENGTH tprog) ==> 1445 (state_old.memory (ADDR30 (FETCH_PC state_old.registers + n2w (e*4))) = 1446 (enc (EL e tprog)))) /\ 1447 (~state_old.undefined) /\ 1448 (Abbrev (m = (DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs))))) /\ 1449 ((reg', mem') = mdecode (reg,mem) oper) /\ 1450 (state_new = STATE_ARM_MEM (LENGTH tprog) state_old) /\ 1451 (REGS_EQUIVALENT m state_old.registers reg)) ==> 1452 1453 ((REGS_EQUIVALENT m state_new.registers reg') /\ 1454 (mem' = mem) /\ (state_new.memory = state_old.memory) /\ 1455 (~state_new.undefined) /\ 1456 (state_new.psrs = state_old.psrs) /\ 1457 (state_new.cp_state = state_old.cp_state) /\ 1458 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 1459 (FETCH_PC state_new.registers = FETCH_PC state_old.registers + n2w (4 * LENGTH tprog)) 1460 )``, 1461 1462 `!e. (e < 1) = (e = 0)` by DECIDE_TAC THEN 1463 ASM_SIMP_TAC list_ss [DOPER2INSTRUCTION_LIST_def] THEN 1464 REWRITE_TAC [prove(``1 = SUC 0``, DECIDE_TAC), STATE_ARM_MEM_EVAL] THEN 1465 ASSUME_TAC (SIMP_RULE std_ss [] DOPER2INSTRUCTION_thm) THEN 1466 FULL_SIMP_TAC std_ss [WORD_ADD_0, systemTheory.ADDR30_def, 1467 armTheory.FETCH_PC_def] THEN 1468 METIS_TAC[]); 1469 1470 1471 1472val JUMP_ADDRESS_OK_thm = store_thm ("JUMP_ADDRESS_OK_thm", 1473``!n. ((n < 2**(dimindex (:'a) - 1)) /\ (dimindex (:'a) <= dimindex (:'b))) ==> 1474(((sw2sw ((n2w:num->bool ** 'a) n)) = ((n2w:num->bool ** 'b) n)) /\ 1475 ((sw2sw ($-((n2w:num->bool ** 'a) n))) = ($- ((n2w:num->bool ** 'b) n))))``, 1476 1477REWRITE_TAC[sw2sw_def, bitTheory.SIGN_EXTEND_def, 1478MOD_2EXP_DIMINDEX, GSYM dimword_def, n2w_11, 1479GSYM word_msb_n2w, n2w_w2n, word_msb_n2w_numeric, word_2comp_n2w, w2n_n2w] THEN 1480REWRITE_TAC[dimword_def, INT_MIN_def] THEN 1481Q.ABBREV_TAC `a = dimindex (:'a)` THEN 1482Q.ABBREV_TAC `b = dimindex (:'b)` THEN 1483`(0 < a) /\ (0 < b)` by PROVE_TAC[DIMINDEX_GT_0] THEN 1484 1485SIMP_TAC arith_ss [MOD_2EXP_def, LET_THM] THEN 1486`?pa. a = SUC pa` by ALL_TAC THEN1 ( 1487 Cases_on `a` THENL [ 1488 FULL_SIMP_TAC std_ss [], 1489 PROVE_TAC[] 1490 ] 1491) THEN 1492REPEAT STRIP_TAC THENL [ 1493 UNDISCH_NO_TAC 1 THEN 1494 FULL_SIMP_TAC arith_ss [EXP], 1495 1496 UNDISCH_NO_TAC 1 THEN 1497 FULL_SIMP_TAC arith_ss [EXP] THEN 1498 REPEAT STRIP_TAC THEN 1499 Cases_on `n = 0` THENL [ 1500 ASM_SIMP_TAC arith_ss [], 1501 1502 `~(2 ** pa = 0)` by SIMP_TAC std_ss [EXP_EQ_0] THEN 1503 `(2 ** pa <= (2 * 2 ** pa - n) MOD (2 * 2 ** pa))` by FULL_SIMP_TAC arith_ss [] THEN 1504 ONCE_ASM_REWRITE_TAC[] THEN 1505 WEAKEN_HD_TAC THEN 1506 REWRITE_TAC[] THEN 1507 REMAINS_TAC `2 * 2** pa <= 2 ** b` THEN1 ASM_SIMP_TAC arith_ss [] THEN 1508 SIMP_TAC std_ss [GSYM EXP, EXP_BASE_LE_MONO] THEN 1509 PROVE_TAC[] 1510 ] 1511]); 1512 1513 1514val CTL_STRUCTURE2INSTRUCTION_LIST_thm = store_thm ("CTL_STRUCTURE2INSTRUCTION_LIST_thm", 1515`` 1516!prog tprog reg mem reg' mem' m state_old. 1517 1518 (~(CONTAINS_MEMORY_DOPER prog) /\ (WELL_FORMED prog) /\ (IS_WELL_FORMED_CTL_STRUCTURE prog) /\ 1519 (tprog = CTL_STRUCTURE2INSTRUCTION_LIST prog) /\ 1520 (LENGTH tprog < 2**(dimindex (:24) - 1) -1) /\ 1521 1522 (!e. (e < LENGTH tprog) ==> 1523 (state_old.memory (ADDR30 (FETCH_PC state_old.registers + n2w (e*4))) = 1524 (enc (EL e tprog)))) /\ 1525 1526 (~state_old.undefined) /\ 1527 1528 (Abbrev (m = DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs)))) /\ 1529 1530 ((reg', mem') = run_ir prog (reg,mem)) /\ 1531 (REGS_EQUIVALENT m state_old.registers reg)) ==> 1532 (?step_num. !state_new. (state_new = STATE_ARM_MEM step_num state_old) ==> 1533 1534((REGS_EQUIVALENT m state_new.registers reg') /\ 1535 (mem' = mem) /\ (state_new.memory = state_old.memory) /\ 1536 (~state_new.undefined) /\ 1537 (?N Z C V. state_new.psrs = CPSR_WRITE state_old.psrs (SET_NZCV (N,Z,C,V) (CPSR_READ state_old.psrs))) /\ 1538 (state_new.cp_state = state_old.cp_state) /\ 1539 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 1540 (FETCH_PC state_new.registers = (FETCH_PC state_old.registers + 1541 n2w (4 * LENGTH tprog)))))``, 1542 1543 1544Induct_on `prog` THENL [ 1545 (*BLK*) 1546 Induct_on `l` THENL [ 1547 REPEAT STRIP_TAC THEN 1548 EXISTS_TAC ``0`` THEN 1549 FULL_SIMP_TAC list_ss [STATE_ARM_MEM_EVAL, WORD_ADD_0, CTL_STRUCTURE2INSTRUCTION_LIST_def, SEMANTICS_OF_IR] THEN 1550 PROVE_TAC[arm_evalTheory.SET_NZCV_ID, arm_evalTheory.CPSR_READ_WRITE], 1551 1552 1553 1554 1555 1556 FULL_SIMP_TAC list_ss [CTL_STRUCTURE2INSTRUCTION_LIST_def, 1557 CONTAINS_MEMORY_DOPER_def,IS_WELL_FORMED_CTL_STRUCTURE_def, 1558 IR_SEMANTICS_BLK, 1559 WELL_FORMED_thm] THEN 1560 REPEAT GEN_TAC THEN STRIP_TAC THEN 1561 `?reg'' mem''. mdecode (reg, mem) h = (reg'', mem'')` by METIS_TAC[PAIR] THEN 1562 1563 ASSUME_TAC (SIMP_RULE std_ss [] DOPER2INSTRUCTION_LIST_thm) THEN 1564 Q_SPECL_NO_ASSUM 0 [`h`, `reg`, `mem`, `reg''`, `mem''`, `m`, `state_old`] THEN 1565 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1566 FULL_SIMP_TAC list_ss [] THEN 1567 REWRITE_TAC[markerTheory.Abbrev_def] THEN 1568 REPEAT STRIP_TAC THEN 1569 Q_SPEC_NO_ASSUM 6 `e` THEN 1570 UNDISCH_HD_TAC THEN 1571 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1] 1572 ) THEN 1573 1574 1575 SUBGOAL_TAC `!a b. (n2w (4 * (a + b))):word32 = 1576 n2w (4 * a) + n2w (4 * b)` THEN1 ( 1577 WORDS_TAC THEN 1578 SIMP_TAC arith_ss [] 1579 ) THEN 1580 1581 Q_SPECL_NO_ASSUM 13 [`reg''`, `mem''`, `reg'`, `mem'`, `m`, `STATE_ARM_MEM (LENGTH (DOPER2INSTRUCTION_LIST h)) state_old`] THEN 1582 FULL_SIMP_TAC list_ss [] THEN 1583 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1584 REWRITE_TAC[markerTheory.Abbrev_def] THEN 1585 FULL_SIMP_TAC arith_ss [] THEN 1586 REPEAT STRIP_TAC THEN 1587 Q_SPEC_NO_ASSUM 15 `LENGTH (DOPER2INSTRUCTION_LIST h) + e` THEN 1588 UNDISCH_HD_TAC THEN 1589 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, WORD_ADD_ASSOC] 1590 ) THEN 1591 FULL_SIMP_TAC std_ss [] THEN 1592 EXISTS_TAC ``step_num + LENGTH (DOPER2INSTRUCTION_LIST h)`` THEN 1593 SIMP_TAC std_ss [STATE_ARM_MEM_SPLIT] THEN 1594 FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC] THEN 1595 PROVE_TAC[] 1596 ], 1597 1598 1599 FULL_SIMP_TAC list_ss [CTL_STRUCTURE2INSTRUCTION_LIST_def, 1600 CONTAINS_MEMORY_DOPER_def,IS_WELL_FORMED_CTL_STRUCTURE_def, 1601 IR_SEMANTICS_SC, WELL_FORMED_thm] THEN 1602 REPEAT GEN_TAC THEN STRIP_TAC THEN 1603 `?reg'' mem''. run_ir prog (reg, mem) = (reg'', mem'')` by METIS_TAC[PAIR] THEN 1604 Q_SPECL_NO_ASSUM 14 [`reg`, `mem`, `reg''`, `mem''`, `m`, `state_old`] THEN 1605 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1606 ASM_SIMP_TAC arith_ss [markerTheory.Abbrev_def] THEN 1607 REPEAT STRIP_TAC THEN 1608 Q_SPEC_NO_ASSUM 6 `e` THEN 1609 UNDISCH_HD_TAC THEN 1610 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1] 1611 ) THEN 1612 FULL_SIMP_TAC std_ss [] THEN 1613 Q.ABBREV_TAC `state = (STATE_ARM_MEM step_num state_old)` THEN 1614 1615 SUBGOAL_TAC `!a b. (n2w (4 * (a + b))):word32 = 1616 n2w (4 * a) + n2w (4 * b)` THEN1 ( 1617 WORDS_TAC THEN 1618 SIMP_TAC arith_ss [] 1619 ) THEN 1620 Q_SPECL_NO_ASSUM 23 [`reg''`, `mem''`, `reg'`, `mem'`, `m`, `state`] THEN 1621 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1622 REWRITE_TAC[markerTheory.Abbrev_def] THEN 1623 FULL_SIMP_TAC arith_ss [arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1624 arm_evalTheory.CPSR_WRITE_READ] THEN 1625 REPEAT STRIP_TAC THENL [ 1626 Q_SPEC_NO_ASSUM 16 `LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog) + e` THEN 1627 UNDISCH_HD_TAC THEN 1628 ASM_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2, WORD_ADD_ASSOC], 1629 1630 ASM_SIMP_TAC std_ss [SEMANTICS_OF_IR] 1631 ] 1632 ) THEN 1633 FULL_SIMP_TAC std_ss [] THEN 1634 EXISTS_TAC ``(step_num':num) + step_num`` THEN 1635 Q.UNABBREV_TAC `state` THEN 1636 FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC, STATE_ARM_MEM_SPLIT, 1637 arm_evalTheory.SET_NZCV_IDEM, arm_evalTheory.CPSR_WRITE_WRITE, 1638 arm_evalTheory.CPSR_WRITE_READ] THEN 1639 PROVE_TAC[], 1640 1641 1642 1643 1644 1645 FULL_SIMP_TAC list_ss [CTL_STRUCTURE2INSTRUCTION_LIST_def, 1646 CONTAINS_MEMORY_DOPER_def,IS_WELL_FORMED_CTL_STRUCTURE_def, 1647 WELL_FORMED_thm] THEN 1648 REPEAT STRIP_TAC THEN 1649 UNDISCH_NO_TAC 1 (*run_ir CJ ...*) THEN 1650 ASM_SIMP_TAC std_ss [SEMANTICS_OF_IR] THEN 1651 STRIP_TAC THEN 1652 1653 `?r c e. p = (r, c, e)` by METIS_TAC[PAIR] THEN 1654 ASSUME_TAC (SIMP_RULE std_ss [] CJ2INSTRUCTION_LIST_thm) THEN 1655 Q_SPECL_NO_ASSUM 0 [`r`, `c`, `e`, `(n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog'))):word24`, `state_old`, `m`, `reg`, `mem`] THEN 1656 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1657 ASM_SIMP_TAC std_ss [markerTheory.Abbrev_def] THEN 1658 REPEAT STRIP_TAC THEN 1659 Q_SPEC_NO_ASSUM 6 `e'` THEN 1660 UNDISCH_HD_TAC THEN 1661 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1, 1662 GSYM APPEND_ASSOC] 1663 ) THEN 1664 FULL_SIMP_TAC std_ss [] THEN 1665 Q.ABBREV_TAC `length_cond = (LENGTH 1666 (CJ2INSTRUCTION_LIST (r,c,e) 1667 (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog')))))` THEN 1668 Q.ABBREV_TAC `length_false = (LENGTH 1669 (CTL_STRUCTURE2INSTRUCTION_LIST prog'))` THEN 1670 Q.ABBREV_TAC `length_true = (LENGTH 1671 (CTL_STRUCTURE2INSTRUCTION_LIST prog))` THEN 1672 Cases_on `eval_il_cond (r,c,e) (reg,mem)` THENL [ 1673 FULL_SIMP_TAC std_ss [dimindex_24] THEN 1674 Q_SPECL_NO_ASSUM 25 [`reg`, `mem`, `reg'`, `mem'`, `m`, `STATE_ARM_MEM length_cond state_old`] THEN 1675 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1676 REWRITE_TAC[markerTheory.Abbrev_def] THEN 1677 FULL_SIMP_TAC arith_ss [arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1678 arm_evalTheory.CPSR_WRITE_READ] THEN 1679 REPEAT STRIP_TAC THEN 1680 Q_SPEC_NO_ASSUM 17 `length_cond + (length_false + (1 + e'))` THEN 1681 UNDISCH_HD_TAC THEN 1682 `w2n (15w:word4) = 15` by WORDS_TAC THEN 1683 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, FETCH_PC___PC_WRITE, combinTheory.APPLY_UPDATE_THM, armTheory.FETCH_PC_def] THEN 1684 MATCH_MP_TAC (prove (``(a = b) ==> ((a = c) ==> (b = c))``, SIMP_TAC std_ss [])) THEN 1685 1686 AP_TERM_TAC THEN 1687 AP_TERM_TAC THEN 1688 SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL, GSYM WORD_ADD_ASSOC] THEN 1689 1690 ASSUME_TAC (SIMP_RULE arith_ss [dimindex_32, dimindex_24] (INST_TYPE [alpha |-> ``:24``, beta |-> ``:32``] JUMP_ADDRESS_OK_thm)) THEN 1691 Q_SPEC_NO_ASSUM 0 `length_false` THEN 1692 UNDISCH_HD_TAC THEN 1693 ASM_SIMP_TAC arith_ss [] THEN 1694 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1695 1696 REWRITE_TAC [prove (``2 = 1 + 1``, DECIDE_TAC), GSYM LSL_ADD, LSL_ONE, 1697 word_add_n2w] THEN 1698 AP_TERM_TAC THEN 1699 DECIDE_TAC 1700 ) THEN 1701 FULL_SIMP_TAC std_ss [] THEN 1702 Q_TAC EXISTS_TAC `step_num+length_cond` THEN 1703 ASM_SIMP_TAC std_ss [STATE_ARM_MEM_SPLIT, FETCH_PC___PC_WRITE, arm_evalTheory.SET_NZCV_IDEM, arm_evalTheory.CPSR_WRITE_READ, 1704 arm_evalTheory.CPSR_WRITE_WRITE] THEN 1705 REPEAT STRIP_TAC THENL [ 1706 METIS_TAC[], 1707 1708 SIMP_TAC std_ss [armTheory.FETCH_PC_def, WORD_EQ_ADD_LCANCEL, GSYM WORD_ADD_ASSOC] THEN 1709 ASSUME_TAC (SIMP_RULE arith_ss [dimindex_32, dimindex_24] (INST_TYPE [alpha |-> ``:24``, beta |-> ``:32``] JUMP_ADDRESS_OK_thm)) THEN 1710 Q_SPEC_NO_ASSUM 0 `length_false` THEN 1711 UNDISCH_HD_TAC THEN 1712 ASM_SIMP_TAC arith_ss [] THEN 1713 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1714 1715 REWRITE_TAC [prove (``2 = 1 + 1``, DECIDE_TAC), GSYM LSL_ADD, LSL_ONE, 1716 word_add_n2w] THEN 1717 AP_TERM_TAC THEN 1718 DECIDE_TAC 1719 ], 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 FULL_SIMP_TAC std_ss [dimindex_24] THEN 1731 Q_SPECL_NO_ASSUM 24 [`reg`, `mem`, `reg'`, `mem'`, `m`, `STATE_ARM_MEM length_cond state_old`] THEN 1732 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1733 ASM_SIMP_TAC arith_ss [markerTheory.Abbrev_def, arm_evalTheory.DECODE_IFMODE_SET_NZCV, arm_evalTheory.CPSR_WRITE_READ] THEN 1734 REPEAT STRIP_TAC THEN 1735 Q_SPEC_NO_ASSUM 17 `length_cond + e'` THEN 1736 UNDISCH_HD_TAC THEN 1737 `w2n (15w:word4) = 15` by WORDS_TAC THEN 1738 REWRITE_TAC [GSYM APPEND_ASSOC] THEN 1739 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, FETCH_PC___PC_WRITE, combinTheory.APPLY_UPDATE_THM, armTheory.FETCH_PC_def, rich_listTheory.EL_APPEND1, word_add_n2w, GSYM WORD_ADD_ASSOC] THEN 1740 MATCH_MP_TAC (prove (``(a = b) ==> ((a = c) ==> (b = c))``, SIMP_TAC std_ss [])) THEN 1741 1742 AP_TERM_TAC THEN 1743 AP_TERM_TAC THEN 1744 REWRITE_TAC [WORD_EQ_ADD_LCANCEL] THEN 1745 AP_TERM_TAC THEN 1746 DECIDE_TAC 1747 ) THEN 1748 FULL_SIMP_TAC std_ss [] THEN 1749 1750 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] arm_rulesTheory.ARM_B) THEN 1751 Q_SPECL_NO_ASSUM 0 [`(STATE_ARM_MEM step_num (STATE_ARM_MEM length_cond state_old))`, `if (length_true = 0) then $-1w else (n2w (length_true - 1)):word24`, `AL`] THEN 1752 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1753 FULL_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, armTheory.FETCH_PC_def, 1754 armTheory.CONDITION_PASSED2_def, arm_evalTheory.DECODE_NZCV_SET_NZCV, 1755 armTheory.NZCV_def, armTheory.condition_case_def] THEN 1756 Q_SPEC_NO_ASSUM 24 `length_cond + length_false` THEN 1757 UNDISCH_HD_TAC THEN 1758 REWRITE_TAC [GSYM APPEND_ASSOC] THEN 1759 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, systemTheory.ADDR30_def] THEN 1760 1761 MATCH_MP_TAC (prove (``(a = b) ==> ((a = c) ==> (b = c))``, SIMP_TAC std_ss [])) THEN 1762 1763 AP_TERM_TAC THEN 1764 AP_TERM_TAC THEN 1765 REWRITE_TAC[GSYM armTheory.FETCH_PC_def, FETCH_PC___PC_WRITE, 1766 GSYM WORD_ADD_ASSOC, WORD_EQ_ADD_LCANCEL, word_add_n2w] THEN 1767 AP_TERM_TAC THEN 1768 DECIDE_TAC 1769 ) THEN 1770 1771 1772 FULL_SIMP_TAC std_ss [] THEN 1773 Q_TAC EXISTS_TAC `(SUC 0)+step_num+length_cond` THEN 1774 REWRITE_TAC[STATE_ARM_MEM_SPLIT, STATE_ARM_MEM_EVAL] THEN 1775 ASM_SIMP_TAC std_ss [systemTheory.arm_sys_state_accfupds, FETCH_PC___PC_WRITE, 1776 arm_evalTheory.SET_NZCV_IDEM,REGS_EQUIVALENT___WRITE_PC, 1777 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.CPSR_WRITE_WRITE] THEN 1778 REPEAT STRIP_TAC THENL [ 1779 METIS_TAC[], 1780 1781 REPEAT (Q.PAT_ASSUM `owrt_visible_regs x = owrt_visible_regs y` MP_TAC) THEN 1782 ASM_SIMP_TAC std_ss [owrt_visible_regs_def, state_mode_def, 1783 systemTheory.arm_sys_state_accfupds, REG_OWRT_ALL, 1784 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.DECODE_IFMODE_SET_NZCV], 1785 1786 1787 1788 ASM_REWRITE_TAC[GSYM armTheory.FETCH_PC_def, FETCH_PC___PC_WRITE] THEN 1789 SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL, GSYM WORD_ADD_ASSOC] THEN 1790 Cases_on `length_true` THENL[ 1791 WORDS_TAC THEN 1792 ASM_SIMP_TAC arith_ss [], 1793 1794 ASSUME_TAC (SIMP_RULE arith_ss [dimindex_32, dimindex_24] (INST_TYPE [alpha |-> ``:24``, beta |-> ``:32``] JUMP_ADDRESS_OK_thm)) THEN 1795 Q_SPEC_NO_ASSUM 0 `n:num` THEN 1796 UNDISCH_HD_TAC THEN 1797 ASM_SIMP_TAC arith_ss [] THEN 1798 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1799 1800 REWRITE_TAC [prove (``2 = 1 + 1``, DECIDE_TAC), GSYM LSL_ADD, LSL_ONE, 1801 word_add_n2w] THEN 1802 AP_TERM_TAC THEN 1803 DECIDE_TAC 1804 ] 1805 ] 1806 ], 1807 1808 1809 1810 FULL_SIMP_TAC list_ss [CTL_STRUCTURE2INSTRUCTION_LIST_def, 1811 CONTAINS_MEMORY_DOPER_def,IS_WELL_FORMED_CTL_STRUCTURE_def, 1812 WELL_FORMED_thm] THEN 1813 REPEAT STRIP_TAC THEN 1814 UNDISCH_NO_TAC 1 (*run_ir CJ ...*) THEN 1815 ASM_SIMP_TAC std_ss [IR_SEMANTICS_TR___FUNPOW] THEN 1816 SUBGOAL_TAC `stopAt (eval_il_cond p) (run_ir prog) (reg,mem)` THEN1 ( 1817 MATCH_MP_TAC ARMCompositionTheory.WF_LOOP_IMP_STOPAT THEN 1818 ASM_SIMP_TAC std_ss [GSYM WF_ir_TR_def, WF_ir_TR_thm] 1819 ) THEN 1820 UNDISCH_ALL_TAC THEN 1821 SPEC_TAC (``state_old:'a arm_sys_state``, ``state_old:'a arm_sys_state``) THEN 1822 Induct_on `(shortest (eval_il_cond p) (run_ir prog) (reg,mem))` THENL [ 1823 REPEAT STRIP_TAC THEN 1824 `?r c e. p = (r, c, e)` by METIS_TAC[PAIR] THEN 1825 ASSUME_TAC (SIMP_RULE std_ss [] CJ2INSTRUCTION_LIST_thm) THEN 1826 Q_SPECL_NO_ASSUM 0 [`r`, `c`, `e`, `(n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog))):word24`, `state_old`, `m`, `reg`, `mem`] THEN 1827 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1828 ASM_SIMP_TAC std_ss [markerTheory.Abbrev_def] THEN 1829 REPEAT STRIP_TAC THEN 1830 Q_SPEC_NO_ASSUM 7 `e'` THEN 1831 UNDISCH_HD_TAC THEN 1832 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1, 1833 GSYM APPEND_ASSOC] 1834 ) THEN 1835 FULL_SIMP_TAC std_ss [] THEN 1836 Q.ABBREV_TAC `length_cond = (LENGTH 1837 (CJ2INSTRUCTION_LIST (r,c,e) 1838 (n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog)))))` THEN 1839 1840 `eval_il_cond (r,c,e) (reg, mem)` by METIS_TAC[SHORTEST_LEM] THEN 1841 Q.PAT_ASSUM `0 = shortest P Q X` (fn thm => ASSUME_TAC (GSYM thm)) THEN 1842 Q_TAC EXISTS_TAC `length_cond` THEN 1843 FULL_SIMP_TAC std_ss [FUNPOW, FETCH_PC___PC_WRITE, dimindex_24] THEN 1844 REPEAT STRIP_TAC THENL [ 1845 METIS_TAC[], 1846 1847 ASM_REWRITE_TAC[GSYM armTheory.FETCH_PC_def] THEN 1848 SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL, GSYM WORD_ADD_ASSOC] THEN 1849 Q.ABBREV_TAC `n = LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog)` THEN 1850 ASSUME_TAC (SIMP_RULE arith_ss [dimindex_32, dimindex_24] (INST_TYPE [alpha |-> ``:24``, beta |-> ``:32``] JUMP_ADDRESS_OK_thm)) THEN 1851 Q_SPEC_NO_ASSUM 0 `n` THEN 1852 UNDISCH_HD_TAC THEN 1853 ASM_SIMP_TAC arith_ss [] THEN 1854 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1855 1856 REWRITE_TAC [prove (``2 = 1 + 1``, DECIDE_TAC), GSYM LSL_ADD, LSL_ONE, 1857 word_add_n2w] THEN 1858 AP_TERM_TAC THEN 1859 DECIDE_TAC 1860 ], 1861 1862 1863 1864 1865 REPEAT STRIP_TAC THEN 1866 Q.PAT_ASSUM `SUC v = shortest P Q X` (fn thm => ASSUME_TAC (GSYM thm)) THEN 1867 IMP_RES_TAC SHORTEST_INDUCTIVE THEN 1868 `?reg'' mem''. run_ir prog (reg,mem) = (reg'', mem'')` by METIS_TAC[PAIR] THEN 1869 Q_SPECL_NO_ASSUM 17 [`p`, `prog`, `reg''`, `mem''`] THEN 1870 PROVE_CONDITION_NO_ASSUM 0 THEN1 ASM_REWRITE_TAC[] THEN 1871 FULL_SIMP_TAC std_ss [RIGHT_FORALL_IMP_THM, dimindex_24] THEN 1872 PROVE_CONDITION_NO_ASSUM 0 THEN1 METIS_TAC[] THEN 1873 UNDISCH_HD_TAC THEN 1874 ASM_REWRITE_TAC[] THEN 1875 STRIP_TAC THEN 1876 1877 1878 `?r c e. p = (r, c, e)` by METIS_TAC[PAIR] THEN 1879 ASSUME_TAC (SIMP_RULE std_ss [] CJ2INSTRUCTION_LIST_thm) THEN 1880 Q_SPECL_NO_ASSUM 0 [`r`, `c`, `e`, `(n2w (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog))):word24`, `state_old`, `m`, `reg`, `mem`] THEN 1881 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1882 ASM_SIMP_TAC std_ss [markerTheory.Abbrev_def] THEN 1883 REPEAT STRIP_TAC THEN 1884 Q_SPEC_NO_ASSUM 13 `e'` THEN 1885 UNDISCH_HD_TAC THEN 1886 ASM_SIMP_TAC arith_ss [rich_listTheory.EL_APPEND1, 1887 GSYM APPEND_ASSOC] 1888 ) THEN 1889 FULL_SIMP_TAC std_ss [] THEN 1890 Q.ABBREV_TAC `length_prog = (LENGTH (CTL_STRUCTURE2INSTRUCTION_LIST prog))` THEN 1891 Q.ABBREV_TAC `length_cond = (LENGTH (CJ2INSTRUCTION_LIST (r,c,e) (n2w length_prog)))` THEN 1892 1893 Q_SPECL_NO_ASSUM 27 [`reg`, `mem`, `reg''`, `mem''`, `m`, `STATE_ARM_MEM length_cond state_old`] THEN 1894 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1895 ASM_SIMP_TAC arith_ss [FUNPOW, REGS_EQUIVALENT___WRITE_PC, FETCH_PC___PC_WRITE, markerTheory.Abbrev_def, 1896 arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1897 arm_evalTheory.CPSR_WRITE_READ] THEN 1898 REPEAT STRIP_TAC THEN 1899 Q_SPEC_NO_ASSUM 22 `length_cond + e'` THEN 1900 UNDISCH_HD_TAC THEN 1901 REWRITE_TAC [GSYM APPEND_ASSOC] THEN 1902 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, rich_listTheory.EL_APPEND1, 1903 word_add_n2w, GSYM WORD_ADD_ASSOC, LEFT_ADD_DISTRIB, 1904 armTheory.FETCH_PC_def] 1905 ) THEN 1906 FULL_SIMP_TAC arith_ss [] THEN 1907 1908 1909 ASSUME_TAC (SIMP_RULE std_ss [markerTheory.Abbrev_def] arm_rulesTheory.ARM_B) THEN 1910 Q_SPECL_NO_ASSUM 0 [`(STATE_ARM_MEM step_num (STATE_ARM_MEM length_cond state_old))`, `($- (n2w (length_cond + (length_prog + 2)))):word24`, `AL`] THEN 1911 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1912 ASM_SIMP_TAC std_ss [ 1913 armTheory.CONDITION_PASSED2_def, arm_evalTheory.DECODE_NZCV_SET_NZCV, 1914 armTheory.NZCV_def, armTheory.condition_case_def] THEN 1915 ASM_REWRITE_TAC[GSYM armTheory.FETCH_PC_def, FETCH_PC___PC_WRITE] THEN 1916 Q_SPEC_NO_ASSUM 29 `length_cond + length_prog` THEN 1917 UNDISCH_HD_TAC THEN 1918 REWRITE_TAC [GSYM APPEND_ASSOC] THEN 1919 ASM_SIMP_TAC list_ss [rich_listTheory.EL_APPEND2, systemTheory.ADDR30_def, 1920 word_add_n2w, GSYM WORD_ADD_ASSOC, LEFT_ADD_DISTRIB] 1921 ) THEN 1922 1923 1924 SUBGOAL_TAC `!e1. (FETCH_PC state_old.registers + n2w (4 * length_cond) + 1925 n2w (4 * length_prog) + 8w + 1926 sw2sw ($- (n2w (length_cond + (length_prog + 2))):word24) << 2 + 1927 n2w (4 * e1) = FETCH_PC state_old.registers + n2w (4 * e1))` THEN1 ( 1928 1929 GEN_TAC THEN 1930 ASSUME_TAC (SIMP_RULE arith_ss [dimindex_32, dimindex_24] (INST_TYPE [alpha |-> ``:24``, beta |-> ``:32``] JUMP_ADDRESS_OK_thm)) THEN 1931 Q_SPEC_NO_ASSUM 0 `(length_cond + (length_prog + 2))` THEN 1932 UNDISCH_HD_TAC THEN 1933 ASM_SIMP_TAC arith_ss [] THEN 1934 DISCH_TAC THEN WEAKEN_HD_TAC THEN 1935 1936 REWRITE_TAC[WORD_EQ_ADD_RCANCEL, GSYM WORD_ADD_ASSOC,WORD_ADD_INV_0_EQ] THEN 1937 REWRITE_TAC [prove (``2 = 1 + 1``, DECIDE_TAC), GSYM LSL_ADD, LSL_ONE, 1938 word_add_n2w, GSYM WORD_NEG_ADD] THEN 1939 1940 `(length_cond + (length_prog + 2) + 1941 (length_cond + (length_prog + 2)) + 1942 (length_cond + (length_prog + 2) + 1943 (length_cond + (length_prog + 2)))) = 1944 4*length_cond + 4 * length_prog + 8` by DECIDE_TAC THEN 1945 ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 1946 1947 SIMP_TAC std_ss [GSYM word_add_n2w, WORD_NEG_ADD] THEN 1948 REPEAT WEAKEN_HD_TAC THEN 1949 METIS_TAC[WORD_SUB_REFL, WORD_SUB, WORD_ADD_ASSOC, WORD_ADD_COMM, 1950 WORD_ADD_0] 1951 ) THEN 1952 1953 Q_SPEC_NO_ASSUM 20 `NEXT_ARM_MEM 1954 (STATE_ARM_MEM step_num (STATE_ARM_MEM length_cond state_old))` THEN 1955 FULL_SIMP_TAC std_ss [AND_IMP_INTRO] THEN 1956 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 1957 REWRITE_TAC[markerTheory.Abbrev_def] THEN 1958 FULL_SIMP_TAC std_ss [FUNPOW, systemTheory.arm_sys_state_accfupds, 1959 arm_evalTheory.DECODE_IFMODE_SET_NZCV, 1960 REGS_EQUIVALENT___WRITE_PC, FETCH_PC___PC_WRITE, 1961 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.CPSR_WRITE_WRITE] THEN 1962 ASM_REWRITE_TAC[GSYM armTheory.FETCH_PC_def, FETCH_PC___PC_WRITE] 1963 ) THEN 1964 FULL_SIMP_TAC std_ss [] THEN 1965 1966 EXISTS_TAC ``step_num' + (SUC 0) + step_num + length_cond:num`` THEN 1967 SIMP_TAC std_ss [STATE_ARM_MEM_SPLIT, STATE_ARM_MEM_EVAL] THEN 1968 ASM_SIMP_TAC std_ss [FUNPOW, systemTheory.arm_sys_state_accfupds, FETCH_PC___PC_WRITE, arm_evalTheory.SET_NZCV_IDEM, 1969 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.CPSR_WRITE_WRITE] THEN 1970 REPEAT STRIP_TAC THENL [ 1971 METIS_TAC[], 1972 1973 REPEAT (Q.PAT_ASSUM `owrt_visible_regs x = owrt_visible_regs y` MP_TAC) THEN 1974 ASM_SIMP_TAC std_ss [owrt_visible_regs_def, state_mode_def, 1975 systemTheory.arm_sys_state_accfupds, REG_OWRT_ALL, 1976 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.DECODE_IFMODE_SET_NZCV], 1977 1978 ASM_REWRITE_TAC[GSYM armTheory.FETCH_PC_def, FETCH_PC___PC_WRITE] 1979 ] 1980 ] 1981]); 1982 1983 1984 1985val WORD_UNIV_IMAGE_COUNT = 1986 store_thm ("WORD_UNIV_IMAGE_COUNT", 1987``(UNIV:'a word -> bool) = 1988(IMAGE n2w (count (dimword (:'a))))``, 1989 1990SIMP_TAC std_ss [EXTENSION, IN_UNIV, IN_IMAGE, IN_COUNT] THEN 1991GEN_TAC THEN 1992Q_TAC EXISTS_TAC `w2n x` THEN 1993SIMP_TAC std_ss [n2w_w2n, w2n_lt]); 1994 1995 1996val FINITE_WORD_UNIV = 1997 store_thm ("FINITE_WORD_UNIV", 1998 ``FINITE (UNIV:'a word -> bool)``, 1999SIMP_TAC std_ss [WORD_UNIV_IMAGE_COUNT] THEN 2000MATCH_MP_TAC IMAGE_FINITE THEN 2001SIMP_TAC std_ss [FINITE_COUNT]); 2002 2003 2004val arm_mem_state2reg_fun_def = Define (`arm_mem_state2reg_fun state = 2005 let mode = DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs)) in 2006 (\n:word4. if (n=15w) then 0w else state.registers (num2register (mode_reg2num mode n)))`) 2007 2008val state2reg_fun_def = Define (`state2reg_fun (regs, memory) = 2009 (\n:word4. if (n=15w) then 0w else (regs ' n))`) 2010 2011 2012val arm_mem_state2state_def = Define (`arm_mem_state2state state = 2013 (let mode = DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs)) in 2014 (FUN_FMAP (\n:word4. state.registers (num2register (mode_reg2num mode n))) UNIV), 2015 FUN_FMAP (\n:word30. state.memory n) UNIV)`) 2016 2017val arm_mem_state2state___REGS_EQUIVALENT = 2018 store_thm ("arm_mem_state2state___REGS_EQUIVALENT", 2019``!state reg mem. ((reg, mem) = arm_mem_state2state state) ==> 2020 (REGS_EQUIVALENT (DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs))) state.registers reg)``, 2021 2022SIMP_TAC std_ss [arm_mem_state2state_def, LET_THM, REGS_EQUIVALENT_def, 2023 FINITE_WORD_UNIV, pred_setTheory.IN_UNIV, FUN_FMAP_DEF]); 2024 2025 2026 2027val MREG2REG_EXISTS = 2028 store_thm ("MREG2REG_EXISTS", 2029``!w:word4. ~(w = 15w) ==> (?r. MREG2REG r = w)``, 2030 2031REPEAT STRIP_TAC THEN 2032SUBGOAL_TAC `!r. index_of_reg r MOD 16 = index_of_reg r` THEN1 ( 2033 GEN_TAC THEN 2034 `index_of_reg r < 15` by REWRITE_TAC[index_of_reg_lt] THEN 2035 ASM_SIMP_TAC arith_ss [] 2036) THEN 2037SUBGOAL_TAC `?n. (w = n2w n) /\ n < 15` THEN1 ( 2038 Q_TAC EXISTS_TAC `w2n w` THEN 2039 SIMP_TAC std_ss [n2w_w2n] THEN 2040 `w2n w < 16` by SIMP_TAC std_ss [w2n_lt, GSYM dimword_4] THEN 2041 Cases_on `w2n w = 15` THENL [ 2042 METIS_TAC[n2w_w2n], 2043 DECIDE_TAC 2044 ] 2045) THEN 2046ASM_SIMP_TAC arith_ss [MREG2REG_def,n2w_11,dimword_4] THEN 2047UNDISCH_HD_TAC THEN 2048ASSUME_TAC ((REDEPTH_CONV numLib.num_CONV) ``15``) THEN 2049ASM_REWRITE_TAC[prim_recTheory.LESS_THM] THEN 2050SIMP_TAC std_ss [DISJ_IMP_THM] THEN 2051REWRITE_TAC[GSYM index_of_reg_def, index_of_reg_11] THEN 2052SIMP_TAC std_ss []); 2053 2054 2055 2056val REGS_EQUIVALENT___2reg_fun = 2057 store_thm ("REGS_EQUIVALENT___2reg_fun", 2058``!state regs memory. (REGS_EQUIVALENT (DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs))) state.registers regs) ==> 2059 (arm_mem_state2reg_fun state = 2060 state2reg_fun (regs, memory)) 2061 ``, 2062 2063SIMP_TAC std_ss [REGS_EQUIVALENT_def, arm_mem_state2reg_fun_def, state2reg_fun_def, LET_THM, FUN_EQ_THM, COND_RAND] THEN 2064REPEAT STRIP_TAC THEN 2065Cases_on `x=15w` THEN ASM_REWRITE_TAC[] THEN 2066METIS_TAC[MREG2REG_EXISTS] 2067); 2068 2069 2070 2071val TRANSLATION_SPEC_thm = store_thm ("TRANSLATION_SPEC_thm", 2072`` 2073!prog tprog P m state_old:'a arm_sys_state. 2074 2075 (~(CONTAINS_MEMORY_DOPER prog) /\ (WELL_FORMED prog) /\ (IS_WELL_FORMED_CTL_STRUCTURE prog) /\ 2076 (tprog = CTL_STRUCTURE2INSTRUCTION_LIST prog) /\ 2077 (LENGTH tprog < 2**(dimindex (:24) - 1) -1) /\ 2078 (!st. P (state2reg_fun st) (state2reg_fun (run_ir prog st))) /\ 2079 2080 (!e. (e < LENGTH tprog) ==> 2081 (state_old.memory (ADDR30 (FETCH_PC state_old.registers + n2w (e*4))) = 2082 (enc (EL e tprog)))) /\ 2083 2084 (~state_old.undefined) ==> 2085 (?step_num. !state_new. (state_new = STATE_ARM_MEM step_num state_old) ==> 2086 2087((P (arm_mem_state2reg_fun state_old) (arm_mem_state2reg_fun state_new)) /\ 2088 (state_new.memory = state_old.memory) /\ 2089 (~state_new.undefined) /\ 2090 (?N Z C V. state_new.psrs = CPSR_WRITE (state_old.psrs) (SET_NZCV (N,Z,C,V) (CPSR_READ state_old.psrs))) /\ 2091 (state_new.cp_state = state_old.cp_state) /\ 2092 (owrt_visible_regs state_new = owrt_visible_regs state_old) /\ 2093 (FETCH_PC state_new.registers = (FETCH_PC state_old.registers + 2094 n2w (4 * LENGTH tprog))))))``, 2095 2096 2097REPEAT STRIP_TAC THEN 2098`?m. DECODE_MODE ((4 >< 0) (CPSR_READ state_old.psrs)) = m` by METIS_TAC[] THEN 2099 2100`?reg_old mem_old:(num |-> word32). REGS_EQUIVALENT m state_old.registers reg_old` by METIS_TAC[PAIR, arm_mem_state2state___REGS_EQUIVALENT] THEN 2101`?reg_new mem_new. (reg_new, mem_new) = run_ir prog (reg_old, mem_old)` by METIS_TAC[PAIR] THEN 2102 2103ASSUME_TAC CTL_STRUCTURE2INSTRUCTION_LIST_thm THEN 2104Q_SPECL_NO_ASSUM 0 [`prog`, `tprog` , `reg_old`,`mem_old`, `reg_new`, `mem_new`,`m`, `state_old:'a arm_sys_state`] THEN 2105PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 2106 FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def] 2107) THEN 2108FULL_SIMP_TAC std_ss [] THEN 2109EXISTS_TAC ``step_num:num`` THEN 2110ASM_SIMP_TAC std_ss [] THEN 2111REPEAT STRIP_TAC THENL [ 2112 SUBGOAL_TAC `m = DECODE_MODE ((4 >< 0) (CPSR_READ (STATE_ARM_MEM step_num state_old).psrs))` THEN1 ( 2113 ASM_SIMP_TAC std_ss [arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.DECODE_IFMODE_SET_NZCV] 2114 ) THEN 2115 METIS_TAC[REGS_EQUIVALENT___2reg_fun], 2116 METIS_TAC[] 2117]); 2118 2119 2120val index_of_reg___from_reg_index = 2121 store_thm ("index_of_reg___from_reg_index", 2122``!n. (n < 15) ==> 2123 (index_of_reg (from_reg_index n) = n)``, 2124 2125GEN_TAC THEN 2126`!n m. (n < SUC m) = ((n < m) \/ (n = m))` by DECIDE_TAC THEN 2127`15 = SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))))))))))` by DECIDE_TAC THEN 2128ASM_REWRITE_TAC[] THEN 2129REPEAT WEAKEN_HD_TAC THEN REPEAT STRIP_TAC THEN 2130ASM_SIMP_TAC arith_ss [from_reg_index_thm, index_of_reg_def]); 2131 2132 2133val MREG2REG_EVAL = 2134 store_thm ("MREG2REG_EVAL", `` 2135 (MREG2REG R0 = 0w) /\ 2136 (MREG2REG R1 = 1w) /\ 2137 (MREG2REG R2 = 2w) /\ 2138 (MREG2REG R3 = 3w) /\ 2139 (MREG2REG R4 = 4w) /\ 2140 (MREG2REG R5 = 5w) /\ 2141 (MREG2REG R6 = 6w) /\ 2142 (MREG2REG R7 = 7w) /\ 2143 (MREG2REG R8 = 8w) /\ 2144 (MREG2REG R9 = 9w) /\ 2145 (MREG2REG R10 = 10w) /\ 2146 (MREG2REG R11 = 11w) /\ 2147 (MREG2REG R12 = 12w) /\ 2148 (MREG2REG R13 = 13w) /\ 2149 (MREG2REG R14 = 14w)``, EVAL_TAC); 2150 2151val state2reg_fun2mread = 2152 store_thm ("state2reg_fun2mread", 2153 2154``!st r. (state2reg_fun st (MREG2REG r) = mread st (RR r))``, 2155 2156Cases_on `st` THEN 2157SIMP_TAC std_ss [state2reg_fun_def, rulesTheory.mread_def, read_thm, 2158 toREG_def, GSYM MREG2REG_def, MREG_NOT_PC]); 2159 2160 2161val state2reg_fun2mread2 = 2162 store_thm ("state2reg_fun2mread2", 2163 2164``!st r. (~(r = 15w)) ==> (state2reg_fun st r = mread st (RR (from_reg_index (w2n r))))``, 2165 2166Cases_on `st` THEN 2167SIMP_TAC std_ss [state2reg_fun_def, rulesTheory.mread_def, read_thm, 2168 toREG_def] THEN 2169REPEAT STRIP_TAC THEN 2170`w2n r' < 16` by METIS_TAC[dimword_4, w2n_lt] THEN 2171Cases_on `w2n r' = 15` THEN1 PROVE_TAC[n2w_w2n] THEN 2172`w2n r' < 15` by DECIDE_TAC THEN 2173ASM_SIMP_TAC std_ss [index_of_reg___from_reg_index, n2w_w2n]); 2174 2175 2176 2177val arm_mem_state2reg_fun2REG_READ = 2178 store_thm ("arm_mem_state2reg_fun2REG_READ", 2179 2180``!state r. (arm_mem_state2reg_fun state (MREG2REG r) = REG_READ state.registers (DECODE_MODE ((4 >< 0) (CPSR_READ state.psrs))) (MREG2REG r))``, 2181 2182SIMP_TAC std_ss [arm_mem_state2reg_fun_def, armTheory.REG_READ_def, LET_THM, 2183MREG_NOT_PC]); 2184 2185 2186 2187val MEM_FST_UNZIP = store_thm ("MEM_FST_UNZIP", 2188``!l x. MEM x1 (FST (UNZIP l)) = 2189 (?x2. MEM (x1, x2) l)``, 2190 2191Induct_on `l` THENL [ 2192 ASM_SIMP_TAC list_ss [], 2193 2194 ASM_SIMP_TAC list_ss [] THEN 2195 METIS_TAC[FST, PAIR] 2196]); 2197 2198 2199val ALL_DISTINCT_IMPLIES_FILTER = store_thm ("ALL_DISTINCT_IMPLIES_FILTER", `` 2200!l P. ALL_DISTINCT l ==> ALL_DISTINCT (FILTER P l)``, 2201 2202Induct_on `l` THENL [ 2203 SIMP_TAC list_ss [], 2204 ASM_SIMP_TAC list_ss [COND_RATOR, COND_RAND, MEM_FILTER] 2205]) 2206 2207val SUBSET_DIFF = store_thm ("SUBSET_DIFF", 2208``!s t u. (s SUBSET (t DIFF u)) = (s SUBSET t /\ DISJOINT s u)``, 2209SIMP_TAC std_ss [SUBSET_DEF, DISJOINT_DEF, IN_DIFF, EXTENSION, NOT_IN_EMPTY, IN_INTER] THEN METIS_TAC[]) 2210 2211 2212val PAIR_EQ_ELIM = 2213prove (``!x y z. ((x, y) = z) = ((x = FST z) /\ (y = SND z))``, 2214 METIS_TAC[PAIR, FST, SND]) 2215 2216 2217val LIST_TO_FUN_def = 2218 Define `((LIST_TO_FUN s [] e) = s) /\ 2219 ((LIST_TO_FUN s ((h1, h2)::l) e) = 2220 if (h1 = e) then h2 else 2221 (LIST_TO_FUN s l e))`; 2222 2223val WORD_ADD_INV_0_EQ_SYM = prove (``!v w. (v = v + w) = (w = 0w)``, PROVE_TAC[WORD_ADD_INV_0_EQ]); 2224 2225val ELIM_PFORALL_PEXISTS = prove ( 2226 ``((!p. P p (FST p) (SND p)) = !p1 p2. P (p1, p2) p1 p2) /\ 2227 ((?p. P p (FST p) (SND p)) = ?p1 p2. P (p1, p2) p1 p2)``, 2228 METIS_TAC[PAIR, FST, SND]) 2229 2230 2231(* 2232val TRANSLATION_SPEC_SEP_thm = store_thm ("TRANSLATION_SPEC_SEP_thm", 2233``!prog uregs oregs f tprog uregs_words unknown_changed_regs_list stat rv9 rv8 rv7 2234 rv6 rv5 rv4 rv3 rv2 rv14 rv13 rv12 rv11 rv10 rv1 rv0 regs_list 2235 output_regs_list oregs_words input_regs_list. 2236 2237 (~(CONTAINS_MEMORY_DOPER prog) /\ (WELL_FORMED prog) /\ (IS_WELL_FORMED_CTL_STRUCTURE prog) /\ (UNCHANGED uregs prog) /\ 2238 (CTL_STRUCTURE2INSTRUCTION_LIST prog = tprog) /\ 2239 (LENGTH tprog < 2**(dimindex (:24) - 1) -1) /\ 2240 (!st r. (MEM r oregs_words) ==> ((state2reg_fun (run_ir prog st) r) = ((f (state2reg_fun st)) r))) /\ 2241 (!f1 f2. (!q. MEM q input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==> 2242 (!r. MEM r oregs_words ==> (f f1 r = f f2 r))) /\ 2243 ([(0w:word4, rv0); (1w:word4, rv1); (2w:word4, rv2); (3w:word4, rv3); 2244 (4w:word4, rv4); (5w:word4, rv5); (6w:word4, rv6); (7w:word4, rv7); 2245 (8w:word4, rv8); (9w:word4, rv9); (10w:word4, rv10); (11w:word4, rv11); 2246 (12w:word4, rv12); (13w:word4, rv13); (14w:word4, rv14)] = regs_list) /\ 2247 (!x. MEM x oregs ==> ~MEM x uregs) /\ 2248 (MAP MREG2REG uregs = uregs_words) /\ 2249 (MAP MREG2REG oregs = oregs_words) /\ 2250 (FILTER (\x. ~ (MEM (FST x) uregs_words)) regs_list = input_regs_list) /\ 2251 ((FILTER (\x. (MEM (FST x) oregs_words)) (MAP (\(r, v). (r, f (LIST_TO_FUN 0w regs_list) r)) regs_list)) = output_regs_list) /\ 2252 (FILTER (\x. ~(MEM x oregs_words)) (MAP FST input_regs_list) = unknown_changed_regs_list) 2253 ) ==> 2254 2255 ARM_PROG ((reg_spec input_regs_list) * (S stat)) (MAP enc tprog) {} ((reg_spec output_regs_list)*(ereg_spec unknown_changed_regs_list) * (SEP_EXISTS stat. S stat)) {}``, 2256 2257REPEAT STRIP_TAC THEN 2258FULL_SIMP_TAC list_ss [GSYM ARM_PROG_INTRO1, dimindex_24, LENGTH_MAP] THEN 2259GEN_TAC THEN 2260MATCH_MP_TAC IMP_ARM_RUN THEN 2261SIMP_TAC std_ss [RIGHT_EXISTS_AND_THM, Once SWAP_EXISTS_THM] THEN 2262 2263Q_TAC EXISTS_TAC `((15w:word4) INSERT (LIST_TO_SET (MAP FST input_regs_list)), BIGUNION (IMAGE (\e. ({(addr32 (p + n2w e) + 0w); (addr32 (p + n2w e) + 1w); (addr32 (p + n2w e) + 2w); (addr32 (p + n2w e) + 3w)})) (count (LENGTH tprog))), T, T, F)` THEN 2264SUBGOAL_TAC `ALL_DISTINCT output_regs_list /\ ALL_DISTINCT input_regs_list /\ ALL_DISTINCT unknown_changed_regs_list` THEN1 ( 2265 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2266 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2267 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2268 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2269 ASM_SIMP_TAC std_ss [MAP] THEN 2270 REPEAT STRIP_TAC THENL [ 2271 MATCH_MP_TAC ALL_DISTINCT_IMPLIES_FILTER THEN 2272 REWRITE_TAC [ALL_DISTINCT, preARMTheory.word4_distinct, MEM, 2273 PAIR_EQ], 2274 2275 MATCH_MP_TAC ALL_DISTINCT_IMPLIES_FILTER THEN 2276 REWRITE_TAC [ALL_DISTINCT, preARMTheory.word4_distinct, MEM, 2277 PAIR_EQ], 2278 2279 MATCH_MP_TAC ALL_DISTINCT_IMPLIES_FILTER THEN 2280 `(\x:(word4 # word32). ~MEM (FST x) uregs_words) = 2281 (\x. ~MEM x uregs_words) o FST` by SIMP_TAC std_ss [combinTheory.o_DEF] THEN 2282 ASM_SIMP_TAC std_ss [GSYM FILTER_MAP, MAP] THEN 2283 MATCH_MP_TAC ALL_DISTINCT_IMPLIES_FILTER THEN 2284 REWRITE_TAC [ALL_DISTINCT, preARMTheory.word4_distinct, MEM] 2285 ] 2286) THEN 2287 2288STRIP_TAC THENL [ 2289 ASM_SIMP_TAC list_ss [GSYM STAR_ASSOC, reg_spec_thm] THEN 2290 2291 ASM_SIMP_TAC arith_ss [LENGTH_MAP, ARMpc_def, ms_STAR___ZERO, R30_def, R_def, S_def, one_STAR, GSYM STAR_ASSOC, IN_DIFF, IN_DELETE, ARMel_distinct, SUBSET_DIFF, SUBSET_DELETE, ELIM_PFORALL_PEXISTS] THEN 2292 REPEAT STRIP_TAC THEN 2293 UNDISCH_HD_TAC THEN 2294 2295 SUBGOAL_TAC `LIST_TO_SET (MAP (\(r,v). Reg r v) input_regs_list) SUBSET t` THEN1 ( 2296 FULL_SIMP_TAC list_ss [SUBSET_DEF, MEM_MAP, EVERY_MEM] THEN 2297 REPEAT STRIP_TAC THEN 2298 RES_TAC THEN 2299 Cases_on `y` THEN 2300 FULL_SIMP_TAC std_ss [] 2301 ) THEN 2302 ASM_SIMP_TAC list_ss [arm2set'_def, one_def, DELETE_EQ_ELIM, IN_DIFF, IN_SING, ARMel_distinct, DIFF_EQ_ELIM, SUBSET_DIFF, SUBSET_DELETE, SUBSET_UNION, IN_DELETE] THEN 2303 SIMP_TAC std_ss [Once (EQ_SYM_EQ)] THEN 2304 2305 FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, ELIM_PFORALL_PEXISTS] THEN 2306 REPEAT STRIP_TAC THEN 2307 Q.PAT_ASSUM `t SUBSET arm2set s` (fn thm => MP_TAC thm) THEN 2308 SIMP_TAC std_ss [Once EXTENSION] THEN 2309 ASM_SIMP_TAC list_ss [GSYM RIGHT_EXISTS_AND_THM, IN_UNION, GSPECIFICATION, IN_INSERT, LEFT_AND_OVER_OR, EXISTS_OR_THM, NOT_IN_EMPTY, SUBSET_DEF, DISJ_IMP_THM, FORALL_AND_THM, IN_arm2set, MEM_MAP, GSYM LEFT_FORALL_IMP_THM, MEM_ENUMERATE, IN_BIGUNION, IN_LIST_TO_SET, ELIM_PFORALL_PEXISTS, M_set_thm, 2310 GSYM RIGHT_EXISTS_AND_THM, IN_IMAGE, IN_COUNT, prove (``((a:bool \/ b) /\ c) = ((a /\ c) \/ (b /\ c))``, PROVE_TAC[]), 2311 mem_byte_addr32] THEN 2312 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [ARMel_distinct, ARMel_11] THENL [ 2313 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2314 Q.EXISTS_TAC `p1` THEN 2315 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2316 2317 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2318 Q.EXISTS_TAC `p1` THEN 2319 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2320 2321 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2322 Q.EXISTS_TAC `p1` THEN 2323 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2324 2325 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2326 Q.EXISTS_TAC `p1` THEN 2327 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2328 2329 METIS_TAC[], 2330 METIS_TAC[], 2331 2332 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2333 Q.EXISTS_TAC `e` THEN 2334 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2335 2336 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2337 Q.EXISTS_TAC `e` THEN 2338 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2339 2340 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2341 Q.EXISTS_TAC `e` THEN 2342 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set], 2343 2344 SIMP_TAC std_ss [GSYM EXISTS_OR_THM] THEN 2345 Q.EXISTS_TAC `e` THEN 2346 ASM_SIMP_TAC std_ss [addr32_11, addr32_NEQ_addr32, IN_arm2set] 2347 ], 2348 2349 2350 ASM_SIMP_TAC list_ss [GSYM STAR_ASSOC, reg_spec_thm, ereg_spec_thm, RIGHT_EXISTS_IMP_THM, WD_ARM_arm2set', WD_ARM_DIFF] THEN 2351 ASM_SIMP_TAC arith_ss [ms_STAR___ZERO, LENGTH_MAP, ARMpc_def, R30_def, R_def, S_def, one_STAR, GSYM STAR_ASSOC, IN_DIFF, IN_DELETE, ARMel_distinct, SUBSET_DIFF, SUBSET_DELETE, SEP_EXISTS_ABSORB_STAR, SEP_EXISTS_THM, GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM] THEN 2352 REPEAT STRIP_TAC THEN 2353 UNDISCH_HD_TAC THEN 2354 2355 SUBGOAL_TAC `LIST_TO_SET (MAP (\(r,v). Reg r v) input_regs_list) SUBSET 2356 (arm2set' 2357 (15w INSERT LIST_TO_SET (MAP FST input_regs_list), 2358 BIGUNION 2359 (IMAGE 2360 (\e. 2361 {addr32 (p + n2w e) + 0w; addr32 (p + n2w e) + 1w; 2362 addr32 (p + n2w e) + 2w; addr32 (p + n2w e) + 3w}) 2363 (count (LENGTH tprog))),T,T,F) s)` THEN1 ( 2364 FULL_SIMP_TAC list_ss [SUBSET_DEF, MEM_MAP, EVERY_MEM, 2365 GSYM LEFT_FORALL_IMP_THM, IN_arm2set'] THEN 2366 Cases_on `y` THEN 2367 ASM_SIMP_TAC std_ss [IN_arm2set', IN_INSERT, IN_LIST_TO_SET, MEM_MAP] THEN 2368 REPEAT STRIP_TAC THENL [ 2369 RES_TAC THEN 2370 FULL_SIMP_TAC std_ss [], 2371 2372 METIS_TAC[FST, SND, PAIR] 2373 ] 2374 ) THEN 2375 ASM_SIMP_TAC list_ss [one_def, DELETE_EQ_ELIM, IN_DIFF, IN_SING, ARMel_distinct, DIFF_EQ_ELIM, SUBSET_DIFF, SUBSET_DELETE, SUBSET_UNION, IN_DELETE] THEN 2376 REPEAT STRIP_TAC THEN 2377 Q.PAT_ASSUM `X = arm2set' Y s` (fn thm => ASSUME_TAC (GSYM thm)) THEN 2378 FULL_SIMP_TAC std_ss [] THEN 2379 ASSUME_TAC (SIMP_RULE std_ss [dimindex_24] TRANSLATION_SPEC_thm) THEN 2380 Q_SPECL_NO_ASSUM 0 [`prog`, `\st st'. (EVERY (\r. st' r = f st r) oregs_words /\ EVERY (\r. ~(r = 15w) ==> (st' r = st r)) uregs_words)`, `s`] THEN 2381 PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 2382 Q_TAC GSYM_DEF_TAC `uregs_words` THEN 2383 ASM_SIMP_TAC std_ss [EVERY_MEM] THEN 2384 FULL_SIMP_TAC std_ss [SET_EQ_SUBSET, UNCHANGED_THM, toREG_def, read_thm, EVERY_MEM, MEM_MAP, MREG2REG_def] THEN 2385 CONJ_TAC THENL [ 2386 REPEAT STRIP_TAC THEN 2387 `?st'. (run_ir prog st) = st'` by PROVE_TAC[] THEN 2388 Cases_on `st` THEN Cases_on `st'` THEN 2389 Q_TAC GSYM_DEF_TAC `r` THEN 2390 ASM_SIMP_TAC std_ss [state2reg_fun_def] THEN 2391 `q ' r = read (run_ir prog (q,r')) (REG (index_of_reg y))` by METIS_TAC[] THEN 2392 ASM_REWRITE_TAC[read_thm], 2393 2394 2395 Q.PAT_ASSUM `Y SUBSET arm2set' X s` MP_TAC THEN 2396 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_LIST_TO_SET, MEM_MAP, DISJ_IMP_THM, 2397 FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM, MEM_ENUMERATE, IN_INSERT, NOT_IN_EMPTY, IN_arm2set'] THEN 2398 FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, ELIM_PFORALL_PEXISTS, 2399 GSYM RIGHT_EXISTS_AND_THM, MEM_ENUMERATE, LENGTH_MAP, 2400 GSYM LEFT_FORALL_IMP_THM] THEN 2401 REPEAT STRIP_TAC THEN 2402 POP_NO_ASSUM 2 (fn thm => MP_TAC (Q.GEN `x` (Q.SPECL [`x`, `e`] thm))) THEN 2403 `!e'. ((e = e' MOD 1073741824) /\ e' < LENGTH tprog) = (e' = e)` by ALL_TAC THEN1 ( 2404 GEN_TAC THEN EQ_TAC THEN ASM_SIMP_TAC arith_ss [] 2405 ) THEN 2406 ASM_SIMP_TAC arith_ss [M_set_thm, IN_INSERT, NOT_IN_EMPTY, DISJ_IMP_THM, FORALL_AND_THM, 2407 IN_arm2set', IN_BIGUNION, IN_IMAGE, IN_COUNT, GSYM RIGHT_EXISTS_AND_THM, 2408 addr32_NEQ_addr32, addr32_11, WORD_EQ_ADD_LCANCEL, n2w_11, dimword_30, 2409 GSYM mem_byte_EQ_mem, GSYM mem_def, EL_MAP] THEN 2410 `addr32 (p + n2w e) = addr32 (ADDR30 (FETCH_PC s.registers + n2w (4 * e)))` by ALL_TAC THENL [ 2411 ALL_TAC, 2412 ASM_SIMP_TAC std_ss [] 2413 ] THEN 2414 SIMP_TAC std_ss [addr32_11, armTheory.FETCH_PC_def, systemTheory.ADDR30_def, MEM_ADDR_ADD_CONST_MULT, 2415 GSYM MEM_ADDR_def, MULT_COMM, WORD_EQ_ADD_RCANCEL] THEN 2416 Q.PAT_ASSUM `addr32 p = X` (fn thm => MP_TAC (GSYM thm)) THEN 2417 SIMP_TAC std_ss [reg_def, MEM_ADDR_def, GSYM addr30_def, addr30_addr32] 2418 ] 2419 ) THEN 2420 FULL_SIMP_TAC std_ss [] THEN 2421 EXISTS_TAC ``step_num:num`` THEN 2422 EXISTS_TAC ``status (STATE_ARM_MEM step_num s)`` THEN 2423 SIMP_TAC std_ss [CONJ_ASSOC] THEN 2424 MATCH_MP_TAC (prove (``(a /\ (a ==> b)) ==> (a /\ b)``, PROVE_TAC[])) THEN 2425 REPEAT STRIP_TAC THENL [ 2426 ASM_SIMP_TAC std_ss [arm2set''_EQ, mem_def] THEN 2427 CONJ_TAC THENL [ 2428 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2429 ASM_SIMP_TAC std_ss [IN_INSERT, IN_LIST_TO_SET, MEM_MAP, MEM_FILTER, 2430 GSYM FORALL_AND_THM] THEN 2431 REPEAT STRIP_TAC THEN 2432 SUBGOAL_TAC `MEM r uregs_words` THEN1 ( 2433 REMAINS_TAC `?x. MEM (r, x) regs_list` THEN1 METIS_TAC[FST, SND, PAIR] THEN 2434 `r IN UNIV` by REWRITE_TAC[IN_UNIV] THEN 2435 UNDISCH_HD_TAC THEN 2436 SIMP_TAC std_ss [WORD_UNIV_IMAGE_COUNT, dimword_4] THEN 2437 CONV_TAC (REDEPTH_CONV numLib.num_CONV) THEN 2438 REWRITE_TAC[COUNT_SUC, COUNT_ZERO] THEN 2439 SIMP_TAC std_ss [IN_IMAGE, IN_INSERT, NOT_IN_EMPTY, LEFT_AND_OVER_OR, 2440 EXISTS_OR_THM, DISJ_IMP_THM] THEN 2441 2442 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2443 ASM_SIMP_TAC list_ss [preARMTheory.word4_distinct] 2444 ) THEN 2445 FULL_SIMP_TAC std_ss [EVERY_MEM] THEN 2446 Q_SPEC_NO_ASSUM 10 `r` THEN 2447 UNDISCH_HD_TAC THEN 2448 ASM_SIMP_TAC std_ss [arm_mem_state2reg_fun_def, reg_def, LET_THM, 2449 armTheory.REG_READ_def, state_mode_def], 2450 2451 2452 RW_TAC std_ss [owrt_visible_def] THEN 2453 ASM_SIMP_TAC std_ss [set_status_def, arm_evalTheory.SET_NZCV_IDEM, 2454 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.CPSR_WRITE_WRITE, 2455 mem_byte_def, arm_progTheory.mem_def] 2456 ], 2457 2458 2459 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2460 ASM_SIMP_TAC std_ss [EVERY_MEM, MAP, MEM_FILTER, MEM_MAP] THEN 2461 Cases_on `e` THEN 2462 SIMP_TAC std_ss [IN_arm2set', IN_INSERT, IN_LIST_TO_SET, MEM_MAP] THEN 2463 STRIP_TAC THEN 2464 SUBGOAL_TAC `(~(q = 15w)) /\ (r = f (LIST_TO_FUN 0w regs_list) q)` THEN1 ( 2465 NTAC 2 UNDISCH_HD_TAC THEN 2466 Cases_on `y` THEN 2467 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2468 ASM_SIMP_TAC list_ss [DISJ_IMP_THM, preARMTheory.word4_distinct] 2469 ) THEN 2470 REPEAT STRIP_TAC THENL [ 2471 FULL_SIMP_TAC std_ss [EVERY_MEM] THEN 2472 Q.PAT_ASSUM `!r. (MEM r oregs_words) ==> P r` (fn thm => MP_TAC (ISPEC ``q:word4`` thm)) THEN 2473 ASM_SIMP_TAC std_ss [arm_mem_state2reg_fun_def,LET_THM, reg_def, armTheory.REG_READ_def, arm_evalTheory.CPSR_WRITE_READ, 2474 arm_evalTheory.DECODE_IFMODE_SET_NZCV, state_mode_def] THEN 2475 REPEAT STRIP_TAC THEN 2476 Q.PAT_ASSUM `!f1 f2. P f1 f2` (fn thm => MATCH_MP_TAC 2477 (SIMP_RULE std_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] thm)) THEN 2478 FULL_SIMP_TAC std_ss [SET_EQ_SUBSET] THEN 2479 Q.PAT_ASSUM `Y SUBSET arm2set' X s` MP_TAC THEN 2480 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_LIST_TO_SET, DISJ_IMP_THM, 2481 FORALL_AND_THM, MEM_MAP, GSYM LEFT_FORALL_IMP_THM] THEN 2482 REPEAT STRIP_TAC THEN 2483 Q_SPEC_NO_ASSUM 1 `q'` THEN 2484 UNDISCH_HD_TAC THEN 2485 pairLib.GEN_BETA_TAC THEN 2486 UNDISCH_HD_TAC THEN 2487 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2488 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2489 ASM_SIMP_TAC std_ss [IN_arm2set', MEM_FILTER, reg_def, armTheory.REG_READ_def, state_mode_def] THEN 2490 REPEAT STRIP_TAC THEN 2491 SUBGOAL_TAC `~(FST q' = 15w)` THEN1 ( 2492 UNDISCH_NO_TAC 2 THEN 2493 SIMP_TAC list_ss [DISJ_IMP_THM, word4_distinct] 2494 ) THEN 2495 FULL_SIMP_TAC std_ss [] THEN 2496 POP_NO_ASSUM 2 (fn thm => ASSUME_TAC (GSYM thm)) THEN 2497 ASM_REWRITE_TAC[] THEN 2498 UNDISCH_NO_TAC 3 THEN 2499 SIMP_TAC list_ss [DISJ_IMP_THM, word4_distinct,LIST_TO_FUN_def], 2500 2501 2502 ASM_REWRITE_TAC[] THEN 2503 SUBGOAL_TAC `~(MEM q uregs_words)` THEN1 ( 2504 Q.PAT_ASSUM `MEM q oregs_words` MP_TAC THEN 2505 Q_TAC GSYM_DEF_TAC `oregs_words` THEN 2506 Q_TAC GSYM_DEF_TAC `uregs_words` THEN 2507 ASM_SIMP_TAC std_ss [MEM_MAP] THEN 2508 METIS_TAC[MREG2REG_11] 2509 ) THEN 2510 Q_TAC EXISTS_TAC `y` THEN 2511 Cases_on `y` THEN 2512 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2513 FULL_SIMP_TAC std_ss [MEM_FILTER] THEN 2514 PROVE_TAC[] 2515 ], 2516 2517 2518 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2519 ASM_SIMP_TAC std_ss [EVERY_MEM, MEM_FILTER, MEM_MAP, IN_arm2set', 2520 IN_INSERT, IN_LIST_TO_SET] THEN 2521 pairLib.GEN_BETA_TAC THEN 2522 SIMP_TAC std_ss [ARMel_11] THEN 2523 REPEAT STRIP_TAC THEN 2524 Cases_on `y` THEN Cases_on `y'` THEN 2525 FULL_SIMP_TAC std_ss [] THEN 2526 Cases_on `q = q'` THEN ASM_REWRITE_TAC[] THEN 2527 Cases_on `r'' = arm_prog$reg q' (STATE_ARM_MEM step_num s)` THEN ASM_SIMP_TAC std_ss [] THEN 2528 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2529 FULL_SIMP_TAC std_ss [MEM_FILTER], 2530 2531 2532 SIMP_TAC std_ss [IN_arm2set'], 2533 2534 UNDISCH_HD_TAC THEN 2535 SIMP_TAC std_ss [MEM_MAP] THEN 2536 pairLib.GEN_BETA_TAC THEN 2537 SIMP_TAC std_ss [ARMel_distinct], 2538 2539 UNDISCH_HD_TAC THEN 2540 SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, GSYM IMP_DISJ_THM, 2541 EXTENSION, IN_DEF] THEN 2542 METIS_TAC [ARMel_distinct], 2543 2544 2545 UNDISCH_HD_TAC THEN 2546 SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, MEM_ENUMERATE, ELIM_PFORALL_PEXISTS, GSYM RIGHT_FORALL_OR_THM, M_set_thm, IN_INSERT, NOT_IN_EMPTY, ARMel_distinct], 2547 2548 2549 2550 FULL_SIMP_TAC std_ss [SET_EQ_SUBSET, UNION_SUBSET, INSERT_SUBSET, EMPTY_SUBSET] THEN 2551 Q.PAT_ASSUM `BIGUNION Y SUBSET arm2set' X s` MP_TAC THEN 2552 MATCH_MP_TAC (prove (``(!e. e IN S1 ==> (e IN S2 = e IN S3)) ==> ((S1 SUBSET S2) ==> (S1 SUBSET S3))``, PROVE_TAC[SUBSET_DEF])) THEN 2553 SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, MEM_ENUMERATE, ELIM_PFORALL_PEXISTS, 2554 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_FORALL_IMP_THM, LENGTH_MAP] THEN 2555 REPEAT GEN_TAC THEN 2556 Cases_on `p1 < LENGTH tprog` THEN ASM_REWRITE_TAC[] THEN 2557 `!e'. ((p1 = e' MOD 1073741824) /\ e' < LENGTH tprog) = (e' = p1)` by ALL_TAC THEN1 ( 2558 GEN_TAC THEN EQ_TAC THEN ASM_SIMP_TAC arith_ss [] 2559 ) THEN 2560 ASM_SIMP_TAC arith_ss [M_set_thm, IN_INSERT, NOT_IN_EMPTY, DISJ_IMP_THM, IN_arm2set', IN_BIGUNION, IN_IMAGE, 2561 GSYM RIGHT_EXISTS_AND_THM, addr32_NEQ_addr32, addr32_11, IN_COUNT, WORD_EQ_ADD_LCANCEL, 2562 n2w_11, dimword_30, mem_byte_def, mem_def], 2563 2564 2565 SIMP_TAC std_ss [IN_DISJOINT, NOT_IN_EMPTY, IN_INTER, IN_LIST_TO_SET, MEM_MAP, 2566 IN_BIGUNION, ELIM_PFORALL_PEXISTS, MEM_ENUMERATE, LENGTH_MAP, 2567 GSYM RIGHT_FORALL_OR_THM, M_set_thm, IN_INSERT, ARMel_distinct], 2568 2569 MATCH_MP_TAC (prove (``(!e. e IN S1 ==> ~(e IN S2)) ==> DISJOINT S1 S2``, SIMP_TAC std_ss [IN_DISJOINT] THEN PROVE_TAC[])) THEN 2570 SIMP_TAC std_ss [IN_DISJOINT, NOT_IN_EMPTY, IN_INTER, IN_LIST_TO_SET, MEM_MAP, 2571 IN_BIGUNION, ELIM_PFORALL_PEXISTS, MEM_ENUMERATE, LENGTH_MAP, M_set_thm, IN_INSERT, 2572 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN 2573 REPEAT GEN_TAC THEN 2574 Cases_on `p1 < LENGTH tprog` THEN ASM_REWRITE_TAC[] THEN 2575 SIMP_TAC std_ss [DISJ_IMP_THM, IN_DEF, ARMel_distinct], 2576 2577 2578 2579 2580 FULL_SIMP_TAC list_ss [IN_arm2set', IN_INSERT, reg_def, armTheory.FETCH_PC_def, 2581 pcINC_def, pcADD_def, wLENGTH_def, addr32_ADD, addr32_n2w] THEN 2582 FULL_SIMP_TAC std_ss [SET_EQ_SUBSET] THEN 2583 Q.PAT_ASSUM `Y SUBSET arm2set' X s` MP_TAC THEN 2584 SIMP_TAC std_ss [SUBSET_DEF, IN_UNION, IN_INSERT, NOT_IN_EMPTY, 2585 DISJ_IMP_THM, FORALL_AND_THM, IN_arm2set', reg_def] THEN 2586 PROVE_TAC[WORD_ADD_COMM], 2587 2588 2589 UNDISCH_HD_TAC THEN 2590 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2591 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2592 ASM_SIMP_TAC std_ss [MEM_MAP, MEM_FILTER] THEN 2593 Cases_on `y` THEN 2594 SIMP_TAC std_ss [ARMel_11] THEN 2595 Cases_on `q = 15w` THEN ASM_SIMP_TAC std_ss [] THEN 2596 DISJ2_TAC THEN DISJ2_TAC THEN 2597 Cases_on `y'` THEN 2598 SIMP_TAC std_ss [] THEN 2599 Cases_on `q' = 15w` THEN ASM_SIMP_TAC std_ss [] THEN 2600 DISJ2_TAC THEN 2601 SIMP_TAC std_ss [MEM, preARMTheory.word4_distinct], 2602 2603 2604 2605 UNDISCH_HD_TAC THEN 2606 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2607 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2608 ASM_SIMP_TAC std_ss [IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, MEM_FILTER] THEN 2609 REPEAT STRIP_TAC THEN 2610 Cases_on `Reg 15w (addr32 (pcINC (MAP enc tprog) p)) IN s'` THEN ASM_REWRITE_TAC[] THEN 2611 GEN_TAC THEN 2612 Cases_on `r = 15w` THENL [ 2613 DISJ2_TAC THEN DISJ2_TAC THEN 2614 Cases_on `y` THEN 2615 SIMP_TAC std_ss [] THEN 2616 Cases_on `q = r` THEN ASM_SIMP_TAC std_ss [] THEN 2617 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2618 ASM_REWRITE_TAC[MEM_FILTER, MEM, PAIR_EQ, word4_distinct], 2619 2620 2621 DISJ1_TAC THEN 2622 SIMP_TAC std_ss [EXTENSION] THEN 2623 Q_TAC EXISTS_TAC `Reg 15w (addr32 (pcINC (MAP enc tprog) p))` THEN 2624 ASM_SIMP_TAC std_ss [IN_DEF, ARMel_11] 2625 ], 2626 2627 2628 UNDISCH_HD_TAC THEN 2629 SIMP_TAC std_ss [MEM_MAP, IN_BIGUNION, IN_LIST_TO_SET, 2630 GSYM RIGHT_FORALL_OR_THM, ELIM_PFORALL_PEXISTS, M_set_thm, IN_INSERT, ARMel_distinct, 2631 NOT_IN_EMPTY], 2632 2633 2634 SIMP_TAC std_ss [EXTENSION, IN_SING, IN_DELETE, IN_DIFF] THEN 2635 `!p1 e. (p1 < LENGTH tprog) ==> 2636 (((((n2w p1):word30) = n2w e) /\ 2637 e < LENGTH tprog) = (e = p1))` by ALL_TAC THEN1 ( 2638 REPEAT STRIP_TAC THEN 2639 EQ_TAC THEN 2640 ASM_SIMP_TAC arith_ss [n2w_11, dimword_30] 2641 ) THEN 2642 FULL_SIMP_TAC std_ss [prove (``DISJOINT S1 S2 = (!e. e IN S1 ==> (~(e IN S2)))``, SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN PROVE_TAC[]), 2643 IN_BIGUNION, IN_LIST_TO_SET, MEM_MAP, IN_arm2set', IN_INSERT, ELIM_PFORALL_PEXISTS, 2644 SUBSET_DEF, GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM, MEM_ENUMERATE, LENGTH_MAP, 2645 GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_FORALL_OR_THM, 2646 prove (``e IN (\e. P e) = P e``, SIMP_TAC std_ss [IN_DEF]), ARMel_11, ARMel_distinct, 2647 M_set_thm, NOT_IN_EMPTY, DISJ_IMP_THM, IN_UNION, FORALL_AND_THM, 2648 RIGHT_AND_OVER_OR, IN_IMAGE, addr32_NEQ_addr32, addr32_11, WORD_EQ_ADD_LCANCEL, 2649 IN_COUNT] THEN 2650 GEN_TAC THEN 2651 Cases_on `x = Undef F` THENL [ 2652 ASM_SIMP_TAC std_ss [IN_arm2set', ARMel_distinct], 2653 2654 ASM_SIMP_TAC std_ss [] THEN 2655 REWRITE_TAC[GSYM DISJ_ASSOC] THEN 2656 MATCH_MP_TAC (prove (``(~a ==> b) ==> (a \/ b)``, PROVE_TAC[])) THEN 2657 SIMP_TAC std_ss [arm2set'_def, IN_UNION, GSPECIFICATION, IN_INSERT, IN_BIGUNION, NOT_IN_EMPTY, 2658 DISJ_IMP_THM, FORALL_AND_THM, ARMel_distinct, GSYM LEFT_FORALL_IMP_THM, IN_IMAGE, 2659 GSYM RIGHT_EXISTS_AND_THM, IN_COUNT, RIGHT_AND_OVER_OR, ARMel_11, GSYM RIGHT_EXISTS_IMP_THM, 2660 IN_LIST_TO_SET, MEM_MAP, ELIM_PFORALL_PEXISTS] THEN 2661 REPEAT CONJ_TAC THENL [ 2662 GEN_TAC THEN 2663 Cases_on `a = 15w` THEN ASM_SIMP_TAC std_ss [] THEN 2664 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2665 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2666 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2667 Q.PAT_ASSUM `EVERY P output_regs_list` MP_TAC THEN 2668 ASM_SIMP_TAC std_ss [MEM_MAP, MEM_FILTER, ELIM_PFORALL_PEXISTS, EVERY_MEM] THEN 2669 Cases_on `MEM a oregs_words` THEN ASM_SIMP_TAC std_ss [] THEN 2670 METIS_TAC[], 2671 2672 2673 REPEAT GEN_TAC THEN 2674 Q.EXISTS_TAC `e` THEN 2675 Cases_on `e < LENGTH tprog` THEN ASM_SIMP_TAC std_ss [] THEN 2676 SIMP_TAC std_ss [LEFT_AND_OVER_OR, DISJ_IMP_THM], 2677 2678 2679 ASM_SIMP_TAC std_ss [] 2680 ] 2681 ] 2682 ] 2683]) 2684 2685 2686*) 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697val SPEC_LIST___MS_PC = prove (`` 2698!xs ys st x y rt z cd b a w p. 2699(spec_list xs ys (st,x) (F,y) (rt,z) (cd,b) * 2700 ms a w * ARMpc p) = 2701(spec_list ((15w, SOME (addr32 p))::xs) (xM_seq (a, w)::ys) (st,x) (T,F) (rt,z) (cd,b))``, 2702 2703SIMP_TAC (std_ss++star_ss) [spec_list_def, xR_list_def, rest_list_def, xM_list_def, 2704 ARMpc_def, R30_def, emp_STAR]); 2705 2706 2707 2708val ms_sem_THM = prove (`` 2709!p tprog s. 2710(ms_sem p (MAP enc tprog) s) = 2711(!e. (e < LENGTH tprog) ==> (s.memory (ADDR30 (addr32 p + n2w (e * 4))) = enc (EL e tprog)))``, 2712 2713Induct_on `tprog` THENL [ 2714 SIMP_TAC list_ss [ms_sem_def], 2715 2716 ASM_SIMP_TAC list_ss [ms_sem_def, arm_progTheory.mem_def] THEN 2717 WEAKEN_HD_TAC THEN 2718 SUBGOAL_TAC `!p n. addr32 p + n2w (4 * SUC n) = addr32 (p + 1w) + n2w (4 * n)` THEN1 ( 2719 REPEAT WEAKEN_HD_TAC THEN 2720 SIMP_TAC std_ss [addr32_def] THEN 2721 WORDS_TAC THEN 2722 SIMP_TAC arith_ss [bitTheory.TIMES_2EXP_def, word_add_def, w2n_n2w, dimword_30] THEN 2723 SIMP_TAC arith_ss [GSYM word_add_n2w, n2w_w2n, MOD_COMMON_FACTOR, SUC_ONE_ADD, LEFT_ADD_DISTRIB] THEN 2724 REPEAT GEN_TAC THEN 2725 CONV_TAC (LHS_CONV (SIMP_CONV std_ss [Once (GSYM MOD_PLUS)])) THEN 2726 CONV_TAC (RHS_CONV (SIMP_CONV std_ss [Once (GSYM MOD_PLUS)])) THEN 2727 REWRITE_TAC[] 2728 ) THEN 2729 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2730 Cases_on `e` THENL [ 2731 ASM_SIMP_TAC list_ss [WORD_ADD_0, systemTheory.ADDR30_def, GSYM arm_progTheory.addr30_def, 2732 addr30_addr32], 2733 2734 FULL_SIMP_TAC list_ss [] 2735 ], 2736 2737 `0 < SUC (LENGTH tprog)` by SIMP_TAC list_ss [] THEN 2738 RES_TAC THEN 2739 FULL_SIMP_TAC list_ss [WORD_ADD_0, systemTheory.ADDR30_def, GSYM arm_progTheory.addr30_def, 2740 addr30_addr32], 2741 2742 `SUC e < SUC (LENGTH tprog)` by ASM_SIMP_TAC std_ss [] THEN 2743 RES_TAC THEN 2744 FULL_SIMP_TAC list_ss [] THEN 2745 METIS_TAC[] 2746 ] 2747]) 2748 2749 2750val xR_list_sem_APPEND = prove ( 2751 ``!l1 l2 s. xR_list_sem (l1 ++ l2) s = 2752 xR_list_sem l1 s /\ xR_list_sem l2 s``, 2753 Induct_on `l1` THENL [ 2754 SIMP_TAC list_ss [xR_list_sem_def], 2755 2756 Cases_on `h` THEN Cases_on `r` THEN 2757 ASM_SIMP_TAC std_ss [APPEND, xR_list_sem_def, CONJ_ASSOC] 2758 ]) 2759 2760val xR_list_sem_NONE = prove ( 2761 ``!l s. xR_list_sem (MAP (\x. (x, NONE)) l) s``, 2762 2763 Induct_on `l` THEN 2764 ASM_SIMP_TAC list_ss [xR_list_sem_def]) 2765 2766val xR_list_sem_SOME = prove ( 2767 ``!l s. xR_list_sem (MAP (\(x, y). (x, SOME y)) l) s = 2768 EVERY (\(x,y). arm_prog$reg x s = y) l``, 2769 2770 Induct_on `l` THENL [ 2771 SIMP_TAC list_ss [xR_list_sem_def], 2772 2773 Cases_on `h` THEN 2774 ASM_SIMP_TAC list_ss [xR_list_sem_def] 2775 ]) 2776 2777val ms_sem_MEMORY = prove ( 2778 ``!a xs s1 s2. (s1.memory = s2.memory) ==> 2779 (ms_sem a xs s1 = ms_sem a xs s2)``, 2780 2781 Induct_on `xs` THEN ( 2782 ASM_SIMP_TAC list_ss [ms_sem_def, arm_progTheory.mem_def] THEN 2783 PROVE_TAC[] 2784 )) 2785 2786 2787val ALL_DISTINCT_APPEND = store_thm ("ALL_DISTINCT_APPEND", 2788 ``!l1 l2. ALL_DISTINCT (l1++l2) = 2789 (ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ 2790 (!e. MEM e l1 ==> ~(MEM e l2)))``, 2791 2792 Induct_on `l1` THENL [ 2793 SIMP_TAC list_ss [], 2794 2795 ASM_SIMP_TAC list_ss [DISJ_IMP_THM, FORALL_AND_THM] THEN 2796 PROVE_TAC[] 2797 ]) 2798 2799val spec_list_expand_ss = rewrites 2800 [spec_list_def,xR_list_def,xM_list_def,rest_list_def,spec_list_sem_def, 2801 xR_list_sem_def,xM_list_sem_def,rest_list_sem_def,ms_sem_def, 2802 xM_list_addresses_def,ms_address_set_def,spec_list_select_def, 2803 xM_list_address_set_def,FOLDR,UNION_EMPTY,UNION_APPEND,GSYM 2804CONJ_ASSOC,ms_def, 2805 MAP,FST,STAR_ASSOC,EVAL ``SUC 0 <= 2**30``,LENGTH,blank_ms_def]; 2806 2807val TRANSLATION_SPEC_SEP_thm = store_thm ("TRANSLATION_SPEC_SEP_thm", 2808``!prog uregs oregs f tprog uregs_words unknown_changed_regs_list stat rv9 rv8 rv7 2809 rv6 rv5 rv4 rv3 rv2 rv14 rv13 rv12 rv11 rv10 rv1 rv0 regs_list 2810 output_regs_list oregs_words input_regs_list. 2811 2812 (~(CONTAINS_MEMORY_DOPER prog) /\ (WELL_FORMED prog) /\ (IS_WELL_FORMED_CTL_STRUCTURE prog) /\ (UNCHANGED uregs prog) /\ 2813 (CTL_STRUCTURE2INSTRUCTION_LIST prog = tprog) /\ 2814 (LENGTH tprog < 2**(dimindex (:24) - 1) -1) /\ 2815 (!st r. (MEM r oregs_words) ==> ((state2reg_fun (run_ir prog st) r) = ((f (state2reg_fun st)) r))) /\ 2816 (!f1 f2. (!q. MEM q input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==> 2817 (!r. MEM r oregs_words ==> (f f1 r = f f2 r))) /\ 2818 ([(0w:word4, rv0); (1w:word4, rv1); (2w:word4, rv2); (3w:word4, rv3); 2819 (4w:word4, rv4); (5w:word4, rv5); (6w:word4, rv6); (7w:word4, rv7); 2820 (8w:word4, rv8); (9w:word4, rv9); (10w:word4, rv10); (11w:word4, rv11); 2821 (12w:word4, rv12); (13w:word4, rv13); (14w:word4, rv14)] = regs_list) /\ 2822 (!x. MEM x oregs ==> ~MEM x uregs) /\ 2823 (MAP MREG2REG uregs = uregs_words) /\ 2824 (MAP MREG2REG oregs = oregs_words) /\ 2825 (FILTER (\x. ~ (MEM (FST x) uregs_words)) regs_list = input_regs_list) /\ 2826 ((FILTER (\x. (MEM (FST x) oregs_words)) (MAP (\(r, v). (r, f (LIST_TO_FUN 0w regs_list) r)) regs_list)) = output_regs_list) /\ 2827 (FILTER (\x. ~(MEM x oregs_words)) (MAP FST input_regs_list) = unknown_changed_regs_list) 2828 ) ==> 2829 2830 ARM_PROG (spec_list (MAP (\(x,y). (x, SOME y)) input_regs_list) [] (T, stat) (F, ir1) (F, ir2) (F, ir3)) (MAP enc tprog) {} ( 2831 SEP_EXISTS stat. (spec_list (APPEND (MAP (\(x,y). (x, SOME y)) output_regs_list) (MAP (\x. (x, NONE)) unknown_changed_regs_list)) [] (T, stat) (F, ir1) (F,ir2) (F,ir3))) {}``, 2832 2833REPEAT STRIP_TAC THEN 2834FULL_SIMP_TAC list_ss [GSYM ARM_PROG_INTRO1, dimindex_24, LENGTH_MAP, SPEC_LIST___MS_PC, SEP_EXISTS_ABSORB_STAR] THEN 2835SIMP_TAC std_ss [ARM_RUN_SEMANTICS, SEP_EXISTS_THM, LET_THM, spec_list_thm] THEN 2836SIMP_TAC (list_ss++spec_list_expand_ss) [LENGTH_MAP, arm_instTheory.ALL_DISJOINT_def, 2837 MEM_MAP, MAP_MAP_o, combinTheory.o_DEF, ELIM_PFORALL_PEXISTS] THEN 2838`(\x. FST ((\(x:REGISTER,y:DATA). (x,SOME y)) x)) = FST` by ALL_TAC THEN1 ( 2839 SIMP_TAC std_ss [FUN_EQ_THM, ELIM_PFORALL_PEXISTS] 2840) THEN 2841ASM_SIMP_TAC std_ss [] THEN WEAKEN_HD_TAC THEN 2842REPEAT STRIP_TAC THEN 2843ASSUME_TAC (SIMP_RULE std_ss [dimindex_24] TRANSLATION_SPEC_thm) THEN 2844Q_SPECL_NO_ASSUM 0 [`prog`, `\st st'. (EVERY (\r. st' r = f st r) oregs_words /\ EVERY (\r. ~(r = 15w) ==> (st' r = st r)) uregs_words)`, `s`] THEN 2845PROVE_CONDITION_NO_ASSUM 0 THEN1 ( 2846 Q_TAC GSYM_DEF_TAC `uregs_words` THEN 2847 ASM_SIMP_TAC std_ss [EVERY_MEM] THEN 2848 FULL_SIMP_TAC std_ss [SET_EQ_SUBSET, UNCHANGED_THM, toREG_def, read_thm, EVERY_MEM, MEM_MAP, MREG2REG_def, armTheory.FETCH_PC_def, arm_progTheory.reg_def, GSYM ms_sem_THM] THEN 2849 2850 REPEAT STRIP_TAC THEN 2851 `?st'. (run_ir prog st) = st'` by PROVE_TAC[] THEN 2852 Cases_on `st` THEN Cases_on `st'` THEN 2853 Q_TAC GSYM_DEF_TAC `r` THEN 2854 ASM_SIMP_TAC std_ss [state2reg_fun_def] THEN 2855 `q ' r = read (run_ir prog (q,r')) (REG (index_of_reg y))` by METIS_TAC[] THEN 2856 ASM_REWRITE_TAC[read_thm] 2857) THEN 2858FULL_SIMP_TAC std_ss [xR_list_sem_SOME] THEN 2859Q.EXISTS_TAC `step_num` THEN 2860ASM_SIMP_TAC std_ss [LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM, xR_list_sem_APPEND, 2861 xR_list_sem_NONE, xR_list_sem_SOME] THEN 2862REPEAT STRIP_TAC THENL [ 2863 FULL_SIMP_TAC list_ss [arm_progTheory.reg_def, armTheory.FETCH_PC_def] THEN 2864 SIMP_TAC list_ss [pcINC_def, 2865 wLENGTH_def, pcADD_def, addr32_ADD, WORD_ADD_COMM, WORD_EQ_ADD_LCANCEL, 2866 addr32_n2w], 2867 2868 Q.PAT_ASSUM `EVERY P oregs_words` MP_TAC THEN 2869 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2870 ASM_SIMP_TAC list_ss [EVERY_MEM, MEM_FILTER, MEM_MAP, ELIM_PFORALL_PEXISTS, 2871 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN 2872 REPEAT STRIP_TAC THEN 2873 RES_TAC THEN 2874 Q.PAT_ASSUM `arm_mem_state2reg_fun X p1 = Y` MP_TAC THEN 2875 `?p1'. p1 = MREG2REG p1'` by METIS_TAC[MEM_MAP] THEN 2876 ASM_REWRITE_TAC [] THEN 2877 SIMP_TAC std_ss [arm_mem_state2reg_fun2REG_READ, arm_progTheory.reg_def, state_mode_def, state_mode_def, MREG_NOT_PC] THEN 2878 STRIP_TAC THEN 2879 Q.PAT_ASSUM `!f1 f2. P f1 f2` (fn thm => MATCH_MP_TAC (SIMP_RULE std_ss [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] thm)) THEN 2880 FULL_SIMP_TAC std_ss [EVERY_MEM] THEN 2881 REPEAT STRIP_TAC THEN 2882 Cases_on `q` THEN 2883 `~(q' = 15w)` by PROVE_TAC[] THEN 2884 RES_TAC THEN 2885 POP_ASSUM MP_TAC THEN 2886 ASM_SIMP_TAC std_ss [arm_mem_state2reg_fun_def, LET_THM, LIST_TO_FUN_def, 2887 arm_progTheory.reg_def, armTheory.REG_READ_def, state_mode_def] THEN 2888 STRIP_TAC THEN 2889 Q.PAT_ASSUM `MEM (q', r) input_regs_list` MP_TAC THEN 2890 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2891 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2892 ASM_SIMP_TAC std_ss [MEM_FILTER, MEM, LEFT_AND_OVER_OR, DISJ_IMP_THM, LIST_TO_FUN_def, 2893 n2w_11, dimword_4], 2894 2895 2896 PROVE_TAC[ms_sem_MEMORY], 2897 METIS_TAC[PAIR], 2898 2899 POP_ASSUM MP_TAC THEN 2900 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2901 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2902 ASM_SIMP_TAC std_ss [MEM_FILTER, MEM_MAP, ELIM_PFORALL_PEXISTS, MEM, n2w_11, dimword_4], 2903 2904 POP_ASSUM MP_TAC THEN 2905 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2906 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2907 ASM_SIMP_TAC std_ss [MEM_FILTER, MEM_MAP, ELIM_PFORALL_PEXISTS, MEM, n2w_11, dimword_4], 2908 2909 2910 2911 2912 SIMP_TAC std_ss [ALL_DISTINCT_APPEND] THEN 2913 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2914 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2915 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2916 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2917 ASM_SIMP_TAC std_ss [] THEN 2918 2919 let 2920 val MAP_ID = prove (``!l. MAP (\x. x) l = l``, 2921 Induct_on `l` THEN ASM_SIMP_TAC list_ss []); 2922 val MAP_FST = prove (``!l l2. (MAP FST (FILTER (\(x :REGISTER # DATA). MEM (FST x) l2) l)) = 2923 FILTER (\x. MEM x l2) (MAP FST l)``, 2924 Induct_on `l` THEN ASM_SIMP_TAC list_ss [COND_RATOR, COND_RAND]); 2925 val MAP_FST2 = prove (``!l l2. (MAP FST (FILTER (\x. ~MEM (FST x) l2) l)) = 2926 FILTER (\x. ~MEM x l2) (MAP FST l)``, 2927 Induct_on `l` THEN ASM_SIMP_TAC list_ss [COND_RATOR, COND_RAND]); 2928 val PAIR_BETA = prove (``(\(x, y). P x y) x = P (FST x) (SND x)``, 2929 Cases_on `x` THEN SIMP_TAC std_ss []) 2930 in 2931 ASM_SIMP_TAC std_ss [MAP_MAP_o, combinTheory.o_DEF, MAP_ID, MAP_FST, MAP_FST2, PAIR_BETA, FILTER_FILTER] 2932 end THEN 2933 2934 SIMP_TAC std_ss [MAP, MEM_FILTER] THEN 2935 2936 MATCH_MP_TAC ( 2937 prove (``ALL_DISTINCT l ==> (ALL_DISTINCT (FILTER P1 l) /\ 2938 ALL_DISTINCT (FILTER P2 l))``, PROVE_TAC[ALL_DISTINCT_IMPLIES_FILTER])) THEN 2939 2940 SIMP_TAC std_ss [ALL_DISTINCT, MEM, n2w_11, dimword_4], 2941 2942 2943 2944 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2945 Q_TAC GSYM_DEF_TAC `output_regs_list` THEN 2946 Q_TAC GSYM_DEF_TAC `unknown_changed_regs_list` THEN 2947 ASM_SIMP_TAC list_ss [EXTENSION, IN_LIST_TO_SET, MEM_MAP, ELIM_PFORALL_PEXISTS, MEM_FILTER, 2948 GSYM RIGHT_EXISTS_AND_THM] THEN 2949 SUBGOAL_TAC `!x. MEM x oregs_words ==> ~(MEM x uregs_words)` THEN1 ( 2950 Q_TAC GSYM_DEF_TAC `oregs_words` THEN 2951 Q_TAC GSYM_DEF_TAC `uregs_words` THEN 2952 ASM_SIMP_TAC std_ss [MEM_MAP, GSYM LEFT_FORALL_IMP_THM, MREG2REG_11] 2953 ) THEN 2954 POP_ASSUM MP_TAC THEN 2955 REPEAT WEAKEN_HD_TAC THEN 2956 METIS_TAC[], 2957 2958 2959 2960 ASM_SIMP_TAC std_ss [arm2set''_EQ, IN_LIST_TO_SET, MEM, mem_byte_def, arm_progTheory.mem_def, 2961 owrt_visible_def, set_status_def, arm_evalTheory.CPSR_READ_WRITE, 2962 arm_evalTheory.CPSR_WRITE_WRITE, arm_evalTheory.CPSR_WRITE_READ, 2963 arm_evalTheory.SET_NZCV_IDEM, arm_progTheory.reg_def, MEM_MAP, 2964 ELIM_PFORALL_PEXISTS] THEN 2965 REPEAT STRIP_TAC THEN 2966 SUBGOAL_TAC `MEM r uregs_words` THEN1 ( 2967 CCONTR_TAC THEN 2968 Q.PAT_ASSUM `!p2. ~(MEM (r, p2) input_regs_list)` MP_TAC THEN 2969 Q_TAC GSYM_DEF_TAC `input_regs_list` THEN 2970 Q_TAC GSYM_DEF_TAC `regs_list` THEN 2971 ASM_SIMP_TAC std_ss [MEM_FILTER, MEM, EXISTS_OR_THM] THEN 2972 Q.PAT_ASSUM `~(r = 15w)` MP_TAC THEN 2973 REPEAT WEAKEN_HD_TAC THEN 2974 `r IN UNIV` by REWRITE_TAC [IN_UNIV] THEN 2975 POP_ASSUM MP_TAC THEN 2976 SIMP_TAC std_ss [WORD_UNIV_IMAGE_COUNT, IN_IMAGE, dimword_4] THEN 2977 REWRITE_TAC[COUNT_SUC, IN_INSERT, (REDEPTH_CONV numLib.num_CONV) ``16``] THEN 2978 SIMP_TAC std_ss [COUNT_ZERO, NOT_IN_EMPTY, LEFT_AND_OVER_OR, EXISTS_OR_THM] THEN 2979 SIMP_TAC std_ss [DISJ_IMP_THM] 2980 ) THEN 2981 FULL_SIMP_TAC std_ss [EVERY_MEM] THEN 2982 RES_TAC THEN 2983 POP_ASSUM MP_TAC THEN 2984 SIMP_TAC std_ss [arm_mem_state2reg_fun_def, LET_THM] THEN 2985 ASM_SIMP_TAC std_ss [LET_THM, 2986 arm_evalTheory.CPSR_WRITE_READ, arm_evalTheory.DECODE_IFMODE_SET_NZCV, 2987 armTheory.REG_READ_def, state_mode_def] 2988]) 2989 2990 2991 2992 2993 2994val _ = export_theory(); 2995