1(* 2quietdec := true; 3 4app load ["arithmeticTheory", "wordsTheory", "wordsLib", "pairTheory", "whileTheory", "finite_mapTheory", 5 "listTheory", "pred_setSimps", "pred_setTheory", "preARMTheory", "CFLTheory", "simplifier"]; 6 7open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory whileTheory 8 listTheory pred_setSimps pred_setTheory finite_mapTheory preARMTheory CFLTheory simplifier; 9 10quietdec := false; 11*) 12 13open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory whileTheory 14 listTheory pred_setSimps pred_setTheory finite_mapTheory preARMTheory CFLTheory simplifier; 15 16(*---------------------------------------------------------------------------------*) 17(* This theory is about stack-involved big instructions including: *) 18(* 1. push_list: push the values of a list of expression into the stack *) 19(* 2. pop_list: pop the values of a list of expression from the stack *) 20(* 3. copy_list: copy the values of a list of expression to another list *) 21(* through the stack *) 22(* 4. sr_list: save the values of a list of expression into the stack first, *) 23(* then restore them later *) 24(* *) 25(* For each big instruction, a sanity theorem shows which expressions will keep*) 26(* their values unchanged; a functionality theorem shows that how the *) 27(* values of affected expressions are changed. *) 28(* *) 29(* An expression could be a register variable, a constant or a stack variable *) 30(* since these instructions are mainly used by function calls (e.g. parameters *) 31(* passing), heap variables are not taken into account since they shouldn't be *) 32(* transferred through the stack *) 33(*---------------------------------------------------------------------------------*) 34 35val _ = new_theory "bigInst"; 36 37(*---------------------------------------------------------------------------------*) 38(* Expressions *) 39(*---------------------------------------------------------------------------------*) 40 41val _ = Hol_datatype ` 42 CFL_EXP = isR of num (* registers *) 43 | isC of word32 (* constants *) 44 | isV of num (* stack variables *) 45 | isM of num (* memory locations *) 46 `; 47 48val reade_def = Define ` 49 (reade st (isR r) = read st (REG r)) /\ 50 (reade st (isC c) = c) /\ 51 (reade st (isV k) = read st (MEM (fp, NEG k))) /\ 52 (reade st (isM m) = (SND st) ' m) 53 `; 54 55val writee_def = Define ` 56 (writee st (isR r, v) = write st (REG r) v) /\ 57 (writee st (isC c, v) = st) /\ 58 (writee st (isV k, v) = write st (MEM (fp, NEG k)) v) /\ 59 (writee st (isM m, v) = (FST st, (SND st) |+ (m, v))) 60 `; 61 62val _ = overload_on ("''", ``reade``); 63val _ = overload_on ("|#", ``writee``); 64val _ = set_fixity "''" (Infixl 500); (* dstate apply *) 65val _ = set_fixity "|#" (Infixl 600); (* dstate update *) 66 67 68val addr_of_def = Define ` 69 (addr_of st (isM m) = m) /\ 70 (addr_of st (isV v) = w2n (read st FP) - v)`; 71 72val eq_addr_def = Define ` 73 eq_addr st addr1 addr2 = 74 (addr_of st addr1 = addr_of st addr2)`; 75 76 77val eq_exp_def = Define ` 78 (eq_exp st (isR r1) (isR r2) = (r1 = r2)) /\ 79 (eq_exp st (isC c1) (isC c2) = (c1 = c2)) /\ 80 (eq_exp st (isV v1) (isV v2) = eq_addr st (isV v1) (isV v2)) /\ 81 (eq_exp st (isM m1) (isM m2) = eq_addr st (isM m1) (isM m2)) /\ 82 (eq_exp st (isM m) (isV v) = eq_addr st (isM m) (isV v)) /\ 83 (eq_exp st (isV v) (isM m) = eq_addr st (isV v) (isM m)) /\ 84 (eq_exp st (isR r) (isV v) = (r = fp)) /\ 85 (eq_exp st (isV v) (isR r) = (r = fp)) /\ 86 (eq_exp st _ _ = F) 87 `; 88 89val eq_exp_def = Define ` 90 (eq_exp st (isR r1) (isR r2) = (r1 = r2)) /\ 91 (eq_exp st (isC c1) (isC c2) = (c1 = c2)) /\ 92 (eq_exp st (isV v1) (isV v2) = eq_addr st (isV v1) (isV v2)) /\ 93 (eq_exp st (isM m1) (isM m2) = eq_addr st (isM m1) (isM m2)) /\ 94 (eq_exp st (isM m) (isV v) = eq_addr st (isM m) (isV v)) /\ 95 (eq_exp st (isV v) (isM m) = eq_addr st (isV v) (isM m)) /\ 96 (eq_exp st _ _ = F) 97 `; 98 99val is_C_def = Define ` 100 (is_C (isC c) = T) /\ 101 (is_C _ = F)`; 102 103val eq_exp_SYM = Q.store_thm ( 104 "eq_exp_SYM", 105 `!st e1 e2. eq_exp st e1 e2 = eq_exp st e2 e1`, 106 Cases_on `e1` THEN Cases_on `e2` THEN 107 RW_TAC std_ss [eq_exp_def, eq_addr_def] THEN 108 METIS_TAC [] 109 ); 110 111val NOT_EQ_isR_LEM = Q.store_thm ( 112 "NOT_EQ_isR_LEM", 113 `!e r. ~(e = isR r) = (!st. ~(eq_exp st (isR r) e))`, 114 Cases_on `e` THEN 115 RW_TAC std_ss [eq_exp_def] THEN 116 METIS_TAC [] 117 ); 118 119(*---------------------------------------------------------------------------------*) 120(* Different ways to restrict an expression *) 121(*---------------------------------------------------------------------------------*) 122 123val valid_regs_def = Define ` 124 (valid_regs r = 125 ~(r=9) /\ ~(r=10) /\ ~(r=11) /\ ~(r=12) /\ ~(r=13) /\ ~(r=14) /\ ~(r=15) /\ 126 (index_of_reg (from_reg_index r) = r)) /\ 127 (valid_regs _ = T)`; 128 129val valid_regs_lem = Q.store_thm ( 130 "valid_regs_lem", 131 `!r. valid_regs r ==> 132 ~(r=13) /\ ~(r=9) /\ ~(r=11) /\ 133 (index_of_reg (from_reg_index r) = r)`, 134 RW_TAC arith_ss [valid_regs_def] 135 ); 136 137val valid_exp_def = Define ` 138 (valid_exp (isR r) = valid_regs r) /\ 139 (valid_exp (isM m) = F) /\ 140 (valid_exp _ = T)`; 141 142val valid_exp_1_def = Define ` 143 (valid_exp_1 (isR r) = ~(r = 13) /\ ~(r = 9) /\ (index_of_reg (from_reg_index r) = r)) /\ 144 (valid_exp_1 (isM m) = T) /\ 145 (valid_exp_1 _ = T)`; 146 147val valid_exp_2_def = Define ` 148 (valid_exp_2 (isR r) = valid_regs r) /\ 149 (valid_exp_2 (isM m) = T) /\ 150 (valid_exp_2 _ = T)`; 151 152val valid_exp_3_def = Define ` 153 (valid_exp_3 (isR r) = (index_of_reg (from_reg_index r) = r)) /\ 154 (valid_exp_3 (isM m) = F) /\ 155 (valid_exp_3 _ = T)`; 156 157val valid_exp_thm = Q.store_thm ( 158 "valid_exp_thm", 159 `!e. valid_exp e ==> valid_exp_1 e /\ valid_exp_2 e /\ valid_exp_3 e`, 160 Cases_on `e` THEN RW_TAC std_ss [valid_exp_1_def, valid_exp_2_def, valid_exp_3_def, valid_exp_def, valid_regs_lem] 161 ); 162 163val VALID_EXP_LEM = Q.store_thm ( 164 "VALID_EXP_LEM", 165 `!l. EVERY valid_exp l ==> EVERY valid_exp_1 l /\ EVERY valid_exp_2 l /\ EVERY valid_exp_3 l`, 166 Induct_on `l` THEN SIMP_TAC list_ss [] THEN 167 RW_TAC std_ss [valid_exp_thm] 168 ); 169 170(*---------------------------------------------------------------------------------*) 171(* Theorems about expressions *) 172(*---------------------------------------------------------------------------------*) 173 174val READE_WRITEE = Q.store_thm ( 175 "READE_WRITEE", 176 `!st e v. ~(is_C e) ==> (st |# (e,v) '' e = v)`, 177 178 SIMP_TAC std_ss [FORALL_DSTATE] THEN 179 Cases_on `e` THEN 180 RW_TAC finmap_ss [is_C_def, reade_def, writee_def, read_thm, write_thm] THEN 181 Cases_on `p` THEN Cases_on `r` THEN 182 RW_TAC finmap_ss [read_thm, write_thm] 183 ); 184 185val READE_WRITEE_THM = Q.store_thm ( 186 "READE_WRITEE_THM", 187 `!st e v. ~(is_C e1) /\ valid_exp e1 ==> ((st |# (e1,v) '' e2 = if eq_exp st e1 e2 then v else st '' e2))`, 188 189 SIMP_TAC std_ss [FORALL_DSTATE] THEN 190 Cases_on `e1` THEN Cases_on `e2` THEN 191 RW_TAC std_ss [is_C_def, reade_def, writee_def, read_thm, write_thm, eq_exp_def, eq_addr_def] THEN 192 FULL_SIMP_TAC finmap_ss [valid_exp_def, valid_regs_def, fp_def, addr_of_def, FP_def, read_thm] 193 ); 194 195val READE_WRITEE_THM_2 = Q.store_thm ( 196 "READE_WRITEE_THM_2", 197 `!st e v. ~(eq_exp st e1 e2) /\ ~(e1 = isR fp) ==> ((st |# (e1,v) '' e2 = st '' e2))`, 198 199 SIMP_TAC std_ss [FORALL_DSTATE] THEN 200 Cases_on `e1` THEN Cases_on `e2` THEN 201 RW_TAC std_ss [reade_def, writee_def, read_thm, write_thm, eq_exp_def, eq_addr_def] THEN 202 FULL_SIMP_TAC finmap_ss [fp_def, addr_of_def, FP_def, read_thm] 203 ); 204 205val WRITEE_EQ = Q.store_thm ( 206 "WRITEE_EQ", 207 `!st e v1 v2. st |# (e,v1) |# (e,v2) = st |# (e,v2)`, 208 209 SIMP_TAC std_ss [FORALL_DSTATE] THEN 210 Cases_on `e` THEN 211 RW_TAC finmap_ss [reade_def, writee_def, read_thm, write_thm] 212 ); 213 214val WRITEE_COMMUTES = Q.store_thm ( 215 "WRITEE_COMMUTES", 216 `!st e1 e2 v1 v2. ~(eq_exp st e1 e2) /\ valid_exp e1 /\ valid_exp e2 217 ==> (st |# (e1,v1) |# (e2,v2) = st |# (e2,v2) |# (e1,v1))`, 218 219 SIMP_TAC std_ss [FORALL_DSTATE] THEN 220 Cases_on `e1` THEN Cases_on `e2` THEN 221 RW_TAC finmap_ss [valid_exp_def, valid_regs_lem, eq_exp_def, eq_addr_def, addr_of_def, reade_def, writee_def, 222 read_thm, write_thm, FUPDATE_COMMUTES, FP_def, fp_def] 223 ); 224 225(*---------------------------------------------------------------------------------*) 226(* Sufficient stack space is required *) 227(* Indicated by the value of sp *) 228(*---------------------------------------------------------------------------------*) 229 230val locate_ge_def = Define ` 231 locate_ge (x:word32) (k:num) = 232 k <= w2n x`; 233 234val w2n_sub_lem = Q.store_thm ( 235 "w2n_sub_lem", 236 `w2n i <= w2n k ==> 237 (w2n (k - i) = w2n k - w2n i)`, 238 RW_TAC std_ss [word_sub_def, word_add_def, w2n_n2w, word_2comp_def] THEN 239 `0 < dimword (:'a)` by METIS_TAC [ZERO_LT_dimword] THEN 240 RW_TAC std_ss [Once (GSYM MOD_PLUS)] THEN 241 RW_TAC std_ss [Once MOD_PLUS] THEN 242 RW_TAC arith_ss [SUB_LEFT_ADD] THENL [ 243 METIS_TAC [w2n_lt, LESS_EQ_ANTISYM], 244 RW_TAC std_ss [LESS_EQ_ADD_SUB, ADD_MODULUS] THEN 245 ASSUME_TAC (Q.SPEC `k` w2n_lt) THEN 246 RW_TAC arith_ss [LESS_EQ_ADD] 247 ] 248 ); 249 250val locate_ge_lem_1 = Q.store_thm ( 251 "locate_ge_lem_1", 252 `locate_ge (x:word32) (k:num) ==> 253 (!i. w2n i <= k ==> 254 (w2n (x - i) = w2n x - w2n i))`, 255 RW_TAC arith_ss [locate_ge_def, w2n_sub_lem] 256 ); 257 258val locate_ge_lem_2 = Q.store_thm ( 259 "locate_ge_lem_2", 260 `locate_ge x k ==> 261 (!i j. ~(i = j) /\ w2n i <= k /\ w2n j <= k ==> 262 ~(w2n (x - i) = w2n (x - j))) /\ 263 (!j. 1 <= w2n x ==> (w2n x - 1 + (j + 2) = w2n x + SUC j))`, 264 RW_TAC arith_ss [] THEN 265 IMP_RES_TAC locate_ge_lem_1 THEN 266 RW_TAC arith_ss [] THEN 267 FULL_SIMP_TAC std_ss [locate_ge_def] THEN 268 METIS_TAC [SUB_CANCEL, w2n_11, LESS_EQ_TRANS] 269 ); 270 271val locate_ge_thm = Q.store_thm ( 272 "locate_ge_thm", 273 `!x k. locate_ge x (SUC k) ==> 274 locate_ge x 1 /\ locate_ge x k`, 275 RW_TAC arith_ss [locate_ge_def] 276 ); 277 278(*---------------------------------------------------------------------------------*) 279(* Data registers are restricted to R0-R8 *) 280(* Frames are separate *) 281(* The temporary use of the stack won't affect existing data in the frame *) 282(*---------------------------------------------------------------------------------*) 283 284val in_range_def = Define ` 285 in_range (k:num) (ubound,lbound) = 286 k <= ubound /\ lbound < k`; 287 288val addr_in_range_def = Define ` 289 (addr_in_range st (isM m) bound = in_range m bound) /\ 290 (addr_in_range st (isV k) bound = in_range (addr_of st (isV k)) bound) /\ 291 (addr_in_range st _ _ = F)`; 292 293val ADDR_IN_RANGE_OUTSIDE = Q.store_thm ( 294 "ADDR_IN_RANGE_OUTSIDE", 295 `!st e x i. ~addr_in_range st e (x, x - SUC i) /\ SUC i <= x ==> 296 ~(eq_exp st e (isM (x - i)))`, 297 Cases_on `e` THEN 298 RW_TAC arith_ss [addr_in_range_def, in_range_def, eq_exp_def, eq_addr_def, addr_of_def] 299 ); 300 301val ADDR_IN_RANGE_OUTSIDE_2 = Q.store_thm ( 302 "ADDR_IN_RANGE_OUTSIDE_2", 303 `!st e i k. ~(addr_in_range st e (k + x, x)) /\ i < k ==> 304 ~(eq_exp st e (isM (SUC i + x)))`, 305 Cases_on `e` THEN 306 RW_TAC arith_ss [addr_in_range_def, in_range_def, eq_exp_def, eq_addr_def, addr_of_def] 307 ); 308 309val ADDR_IN_RANGE_INDUCT_1 = Q.store_thm ( 310 "ADDR_IN_RANGE_INDUCT_1", 311 `!x k e. ~addr_in_range st e (x, x - SUC k) ==> 312 ~addr_in_range st e (x, x - k)`, 313 Cases_on `e` THEN RW_TAC std_ss [addr_in_range_def, eq_exp_def, addr_of_def, eq_addr_def] THENL [ 314 FULL_SIMP_TAC std_ss [in_range_def] THEN 315 Q.ABBREV_TAC `y = w2n (read st FP)` THEN 316 Cases_on `x = SUC k + (y - n)` THENL [ 317 FULL_SIMP_TAC std_ss [SUC_ONE_ADD] THEN 318 RW_TAC arith_ss [], 319 RW_TAC arith_ss [] 320 ], 321 FULL_SIMP_TAC std_ss [in_range_def] THEN 322 RW_TAC arith_ss [] 323 ] 324 ); 325 326(*---------------------------------------------------------------------------------*) 327(* Auxiliary Theorems *) 328(*---------------------------------------------------------------------------------*) 329 330val RUN_CFL_BLK_APPEND = Q.store_thm ( 331 "RUN_CFL_BLK_APPEND", 332 `(!st. run_cfl (BLK []) st = st) /\ 333 (!st l1 l2. run_cfl (BLK (l1 ++ l2)) st = run_cfl (BLK l2) (run_cfl (BLK l1) st))`, 334 SIMP_TAC std_ss [CFL_SEMANTICS_BLK] THEN 335 Induct_on `l1` THEN 336 RW_TAC list_ss [CFL_SEMANTICS_BLK] 337 ); 338 339(*---------------------------------------------------------------------------------*) 340(* Store and load an individual data *) 341(* Push and pop an individual data *) 342(*---------------------------------------------------------------------------------*) 343 344val store_one_def = Define ` 345 (store_one (isR r) offset = 346 [MSTR (13,offset) (from_reg_index r)]) /\ 347 (store_one (isC c) offset = 348 [MMOV R9 (MC c); MSTR (13,offset) R9]) /\ 349 (store_one (isV k) offset = 350 [MLDR R9 (fp, NEG k); MSTR (13,offset) R9])`; 351 352val load_one_def = Define ` 353 (load_one (isR r) offset = 354 [MLDR (from_reg_index r) (13,offset)]) /\ 355 (load_one (isC c) offset = 356 []) /\ 357 (load_one (isV k) offset = 358 [MLDR R9 (13,offset); MSTR (fp, NEG (12 + k)) R9])`; 359 360val push_one_def = Define ` 361 (push_one (isR r) = 362 [MSTR (13,NEG 0) (from_reg_index r); MSUB R13 R13 (MC 1w)]) /\ 363 (push_one (isC c) = 364 [MMOV R9 (MC c); MSTR (13,NEG 0) R9; MSUB R13 R13 (MC 1w)]) /\ 365 (push_one (isV k) = 366 [MLDR R9 (fp, NEG k); MSTR (13,NEG 0) R9; MSUB R13 R13 (MC 1w)]) /\ 367 (push_one (isM m) = [MSUB R13 R13 (MC 1w)]) 368 `; 369 370val pop_one_def = Define ` 371 (pop_one (isR r) = 372 [MLDR (from_reg_index r) (13,POS 1); MADD R13 R13 (MC 1w)]) /\ 373 (pop_one (isC c) = 374 [MADD R13 R13 (MC 1w)]) /\ 375 (pop_one (isV k) = 376 [MLDR R9 (13, POS 1); MSTR (fp,NEG k) R9; MADD R13 R13 (MC 1w)]) /\ 377 (pop_one (isM m) = [MADD R13 R13 (MC 1w)]) 378 `; 379 380(*---------------------------------------------------------------------------------*) 381(* Properties about pushing / storing a single data *) 382(*---------------------------------------------------------------------------------*) 383 384val tac1 = (fn g => 385 ((CONV_TAC (DEPTH_CONV ( 386 REWRITE_CONV [Once mdecode_def] THENC 387 SIMP_CONV finmap_ss [write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]))) THEN 388 FULL_SIMP_TAC std_ss [word_0_n2w, GSYM WORD_SUB_PLUS]) 389 g); 390 391val push_one_lem = Q.store_thm ( 392 "push_one_lem", 393 `!st e. valid_exp_3 e ==> 394 ((run_cfl (BLK (push_one e)) st = st |# (isM (w2n (read st SP)), st '' e) |# (isR sp, st '' (isR sp) - 1w)) \/ 395 (?v. run_cfl (BLK (push_one e)) st = 396 st |# (isM (w2n (read st SP)), st '' e) |# (isR 9, v) |# (isR sp, st '' (isR sp) - 1w))) 397 `, 398 SIMP_TAC std_ss [FORALL_DSTATE] THEN 399 RW_TAC finmap_ss [reade_def, writee_def, read_thm, write_thm, SP_def, sp_def] THEN 400 Cases_on `e` THEN 401 FULL_SIMP_TAC std_ss [valid_exp_3_def, push_one_def,CFL_SEMANTICS_BLK, reade_def, read_thm] THENL [ 402 NTAC 4 tac1, 403 NTAC 6 tac1 THEN METIS_TAC [], 404 NTAC 6 tac1 THEN METIS_TAC [] 405 ] 406 ); 407 408(*---------------------------------------------------------------------------------*) 409(* Push a list of data into the stack *) 410(*---------------------------------------------------------------------------------*) 411 412val push_list_def = Define ` 413 (push_list [] = []) /\ 414 (push_list (x::xs) = push_list xs ++ push_one x)`; 415 416(*---------------------------------------------------------------------------------*) 417(* Lemmas about push_list *) 418(*---------------------------------------------------------------------------------*) 419 420val legal_push_exp_def = Define ` 421 legal_push_exp st e k = 422 ~(addr_in_range st e (w2n (read st SP), w2n (read st SP) - k)) /\ valid_exp_1 e`; 423 424val PUSH_ONE_SANITY = Q.store_thm ( 425 "PUSH_ONE_SANITY", 426 `!st h l. valid_exp_3 h /\ locate_ge (read st SP) (SUC (LENGTH l)) 427 ==> 428 let st1 = run_cfl (BLK (push_one h)) st in 429 locate_ge (read st1 SP) (LENGTH l)`, 430 431 SIMP_TAC std_ss [FORALL_DSTATE] THEN 432 REPEAT STRIP_TAC THEN 433 IMP_RES_TAC locate_ge_thm THEN 434 IMP_RES_TAC locate_ge_lem_1 THEN 435 IMP_RES_TAC push_one_lem THEN 436 POP_ASSUM (ASSUME_TAC o Q.SPEC `(regs,mem)`) THEN 437 RW_TAC std_ss [LET_THM] THEN 438 FULL_SIMP_TAC finmap_ss [LET_THM, locate_ge_def, reade_def, writee_def, write_thm, read_thm, SP_def, sp_def] THEN 439 `w2n (1w:word32) = 1` by WORDS_TAC THEN 440 FULL_SIMP_TAC arith_ss [] 441 ); 442 443 444val PUSH_LIST_SP_FP = Q.store_thm ( 445 "PUSH_LIST_SP_FP", 446 `!l st x. locate_ge (read st SP) (LENGTH l) 447 ==> let st' = run_cfl (BLK (push_list l)) st in 448 (w2n (read st' SP) = w2n (read st SP) - LENGTH l) /\ 449 (w2n (read st' FP) = w2n (read st FP)) /\ 450 (w2n (read st' IP) = w2n (read st IP))`, 451 452 Induct_on `l` THENL [ 453 RW_TAC list_ss [CFL_SEMANTICS_BLK, push_list_def], 454 455 SIMP_TAC list_ss [RUN_CFL_BLK_APPEND, push_list_def] THEN 456 REPEAT STRIP_TAC THEN 457 IMP_RES_TAC locate_ge_thm THEN 458 RES_TAC THEN 459 `?regs mem. run_cfl (BLK (push_list l)) st = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN 460 FULL_SIMP_TAC std_ss [read_thm, SP_def, FP_def, IP_def, LET_THM] THEN 461 `locate_ge ((regs ' 13):word32) 1` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 462 `(w2n (1w:word32) <= 1) /\ (w2n (1w:word32) = 1)` by WORDS_TAC THEN 463 IMP_RES_TAC locate_ge_lem_1 THEN 464 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 465 Cases_on `h` THEN 466 SIMP_TAC std_ss [push_one_def, CFL_SEMANTICS_BLK, read_thm] THENL [ 467 NTAC 6 tac1 THEN RW_TAC arith_ss [], 468 NTAC 9 tac1 THEN RW_TAC arith_ss [], 469 NTAC 9 tac1 THEN RW_TAC arith_ss [], 470 NTAC 4 tac1 THEN RW_TAC arith_ss [] 471 ] 472 ] 473 ); 474 475 476val PUSH_LIST_EXP_INTACT = Q.store_thm ( 477 "PUSH_LIST_EXP_INTACT", 478 `!l st x e. locate_ge (read st SP) (LENGTH l) 479 ==> (eq_exp st e x = eq_exp (run_cfl (BLK (push_list l)) st) e x)`, 480 RW_TAC std_ss [] THEN 481 IMP_RES_TAC PUSH_LIST_SP_FP THEN 482 Cases_on `e` THEN Cases_on `x` THEN 483 FULL_SIMP_TAC std_ss [eq_exp_def, eq_addr_def, addr_of_def, LET_THM, valid_exp_def] 484 ); 485 486(*---------------------------------------------------------------------------------*) 487(* Main Theorems about push_list *) 488(*---------------------------------------------------------------------------------*) 489 490val PUSH_LIST_SANITY = Q.store_thm ( 491 "PUSH_LIST_SANITY", 492 `!l st x. EVERY valid_exp_3 l /\ locate_ge (read st SP) (LENGTH l) 493 ==> !e. ~addr_in_range st e (w2n (read st SP),w2n (read st SP) - LENGTH l) /\ valid_exp_1 e ==> 494 ((run_cfl (BLK (push_list l)) st) '' e = st '' e)`, 495 496 Induct_on `l` THENL [ 497 RW_TAC std_ss [CFL_SEMANTICS_BLK, push_list_def], 498 RW_TAC list_ss [RUN_CFL_BLK_APPEND, push_list_def] THEN 499 IMP_RES_TAC locate_ge_thm THEN 500 IMP_RES_TAC ADDR_IN_RANGE_INDUCT_1 THEN 501 RES_TAC THEN 502 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN POP_ASSUM (K ALL_TAC) THEN 503 IMP_RES_TAC (Q.SPECL [`l`,`st`,`e`,`isM (w2n (read st SP) - LENGTH (l:CFL_EXP list))`] 504 PUSH_LIST_EXP_INTACT) THEN 505 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 506 507 Q.ABBREV_TAC `st1 = run_cfl (BLK (push_list l)) st` THEN 508 IMP_RES_TAC push_one_lem THEN 509 POP_ASSUM (ASSUME_TAC o Q.SPEC `st1`) THEN 510 RW_TAC std_ss [sp_def] THEN RW_TAC std_ss [] THEN 511 `(!st. ~(eq_exp st (isR 9) e)) /\ (!st.~(eq_exp st (isR 13) e))` by 512 METIS_TAC [NOT_EQ_isR_LEM, valid_exp_1_def] THEN 513 `~(eq_exp st1 (isM (w2n (read st SP) - LENGTH l)) e)` by 514 METIS_TAC [locate_ge_def, ADDR_IN_RANGE_OUTSIDE, eq_exp_SYM] THEN 515 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp) /\ ~(isM (w2n (read st SP) - LENGTH l) = isR fp)` 516 by RW_TAC std_ss [fp_def] THEN 517 RW_TAC std_ss [READE_WRITEE_THM_2] 518 ] 519 ); 520 521val PUSH_LIST_FUNCTIONALITY = Q.store_thm ( 522 "PUSH_LIST_FUNCTIONALITY", 523 `!l st. EVERY valid_exp_3 l /\ locate_ge (read st SP) (LENGTH l) ==> 524 !i. i < LENGTH l /\ legal_push_exp st (EL i l) (PRE (LENGTH l) - i) ==> 525 ((run_cfl (BLK (push_list l)) st) '' (isM (w2n (read st SP) - PRE (LENGTH l) + i)) = st '' (EL i l))`, 526 527 Induct_on `l` THENL [ 528 RW_TAC list_ss [], 529 530 RW_TAC list_ss [RUN_CFL_BLK_APPEND, push_list_def] THEN 531 IMP_RES_TAC locate_ge_thm THEN 532 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 533 IMP_RES_TAC (Q.SPECL [`l`,`st`,`e`,`isM (w2n (read st SP) - LENGTH (l:CFL_EXP list))`] 534 PUSH_LIST_EXP_INTACT) THEN 535 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 536 537 Q.ABBREV_TAC `st1 = run_cfl (BLK (push_list l)) st` THEN 538 IMP_RES_TAC push_one_lem THEN 539 POP_ASSUM (ASSUME_TAC o Q.SPEC `st1`) THEN 540 RW_TAC std_ss [sp_def] THEN RW_TAC std_ss [] THEN 541 542 (fn g => ( 543 Cases_on `i` THENL [ 544 FULL_SIMP_TAC list_ss [] THEN 545 `(!st1. ~(eq_exp st1 (isR 9) (isM (w2n (read st SP) - LENGTH l)))) /\ 546 (!st1. ~(eq_exp st1 (isR 13) (isM (w2n (read st SP) - LENGTH l))))` by RW_TAC std_ss [eq_exp_def] THEN 547 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp)` by RW_TAC std_ss [fp_def] THEN 548 RW_TAC std_ss [READE_WRITEE_THM_2] THEN 549 `~(is_C (isM (w2n (read st1 SP))))` by RW_TAC std_ss [is_C_def] THEN 550 Q.UNABBREV_TAC `st1` THEN 551 FULL_SIMP_TAC std_ss [legal_push_exp_def] THEN 552 METIS_TAC [PUSH_LIST_SANITY, READE_WRITEE], 553 554 FULL_SIMP_TAC list_ss [] THEN 555 `(w2n (read st SP) - LENGTH l + SUC n = w2n (read st SP) - PRE (LENGTH l) + n) /\ 556 (LENGTH l - SUC n = PRE (LENGTH l) - n)` by 557 (NTAC 7 (POP_ASSUM (K ALL_TAC)) THEN FULL_SIMP_TAC arith_ss [locate_ge_def]) THEN 558 FULL_SIMP_TAC std_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 559 `(!st1. ~(eq_exp st1 (isR 9) (isM (w2n (read st SP) - PRE (LENGTH l) + n)))) /\ 560 (!st1. ~(eq_exp st1 (isR 13) (isM (w2n (read st SP) - PRE (LENGTH l) + n))))` 561 by RW_TAC std_ss [eq_exp_def] THEN 562 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp)` by RW_TAC std_ss [fp_def] THEN 563 RW_TAC std_ss [READE_WRITEE_THM_2] THEN 564 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 565 566 `~(eq_exp st1 (isM (w2n (read st SP) - LENGTH l)) (isM (w2n (read st SP) - PRE (LENGTH l) + n)))` 567 by FULL_SIMP_TAC arith_ss [eq_exp_def, eq_addr_def, addr_of_def, locate_ge_def] THEN 568 `~(is_C (isM (w2n (read st1 SP) - LENGTH l)))` by RW_TAC std_ss [is_C_def] THEN 569 RW_TAC std_ss [READE_WRITEE_THM_2] THEN 570 METIS_TAC [] 571 ]) g) 572 ] 573 ); 574 575(*---------------------------------------------------------------------------------*) 576(* Properties about popping a single data *) 577(*---------------------------------------------------------------------------------*) 578 579val pop_one_lem = Q.store_thm ( 580 "pop_one_lem", 581 `!st e. valid_exp e ==> 582 (run_cfl (BLK (pop_one e)) st = 583 st |# (e, st '' (isM (w2n (read st SP) + 1))) |# (isR sp, st '' (isR sp) + 1w)) \/ 584 ?v. run_cfl (BLK (pop_one e)) st = 585 st |# (e, st '' (isM (w2n (read st SP) + 1))) |# (isR 9, v) |# (isR sp, st '' (isR sp) + 1w) 586 `, 587 SIMP_TAC std_ss [FORALL_DSTATE] THEN 588 RW_TAC finmap_ss [reade_def, writee_def, read_thm, write_thm, SP_def, sp_def] THEN 589 Cases_on `e` THEN 590 FULL_SIMP_TAC std_ss [valid_exp_def, valid_regs_lem, pop_one_def,CFL_SEMANTICS_BLK, 591 reade_def, read_thm, writee_def, write_thm] THENL [ 592 NTAC 4 tac1 THEN FULL_SIMP_TAC finmap_ss [valid_regs_lem] THEN 593 METIS_TAC [DECIDE ``~(9 = 13)``, FUPDATE_COMMUTES, FUPDATE_REFL, valid_regs_lem], 594 tac1 THEN METIS_TAC [DECIDE ``~(9 = 13)``, FUPDATE_COMMUTES, FUPDATE_REFL], 595 NTAC 6 tac1 THEN RW_TAC std_ss [fp_def] THEN METIS_TAC [] 596 ] 597 ); 598 599(*---------------------------------------------------------------------------------*) 600(* Pop from the stack a list of data *) 601(*---------------------------------------------------------------------------------*) 602 603val pop_list_def = Define ` 604 (pop_list [] = []) /\ 605 (pop_list (x::xs) = pop_one x ++ pop_list xs)`; 606 607(*---------------------------------------------------------------------------------*) 608(* When growing (to higher addresses), the stack shouldn't overflow *) 609(* Indicated by the value of sp *) 610(*---------------------------------------------------------------------------------*) 611 612val grow_lt_def = Define ` 613 grow_lt (x:word32) (k:num) = 614 w2n x + k < dimword (:32)`; 615 616val grow_lt_lem_1 = Q.store_thm ( 617 "grow_lt_lem_1", 618 `grow_lt (x:word32) (k:num) ==> 619 (w2n (x + n2w k) = w2n x + k)`, 620 RW_TAC arith_ss [grow_lt_def, word_add_def, w2n_n2w] 621 ); 622 623val grow_lt_thm = Q.store_thm ( 624 "grow_lt_thm", 625 `grow_lt x (SUC k) ==> 626 grow_lt x 1 /\ grow_lt x k`, 627 RW_TAC arith_ss [grow_lt_def] 628 ); 629 630(*---------------------------------------------------------------------------------*) 631(* Lemmas about pop_list *) 632(*---------------------------------------------------------------------------------*) 633 634val legal_pop_exp_def = Define ` 635 legal_pop_exp st e l = 636 EVERY (\x. ~(eq_exp st e x)) l /\ ~(is_C e) /\ valid_exp e 637 `; 638 639val LEGAL_POP_EXP_NOT_FP_SP = Q.store_thm ( 640 "LEGAL_POP_EXP_NOT_FP_SP", 641 `!e st k. legal_pop_exp st e k ==> 642 ~(e = isR 9) /\ ~(e = isR 13)`, 643 SIMP_TAC std_ss [legal_pop_exp_def] THEN 644 Cases_on `e` THEN 645 RW_TAC std_ss [valid_exp_def, valid_regs_def] 646 ); 647 648val POP_ONE_SANITY = Q.store_thm ( 649 "POP_ONE_SANITY", 650 `!st e h l. valid_exp_2 e /\ valid_exp h /\ grow_lt (read st SP) (SUC (LENGTH l)) /\ 651 ~eq_exp st e h ==> 652 let st1 = run_cfl (BLK (pop_one h)) st in 653 grow_lt (read st1 SP) (LENGTH l) /\ (st1 '' e = st '' e) 654 `, 655 SIMP_TAC std_ss [FORALL_DSTATE] THEN 656 REPEAT STRIP_TAC THEN 657 IMP_RES_TAC grow_lt_thm THEN 658 IMP_RES_TAC grow_lt_lem_1 THEN 659 Cases_on `h` THEN 660 FULL_SIMP_TAC std_ss [valid_exp_def, valid_regs_lem, pop_one_def,CFL_SEMANTICS_BLK, 661 read_thm, write_thm, SP_def, FP_def] THEN 662 (fn g => (NTAC 3 tac1 THEN FULL_SIMP_TAC finmap_ss [LET_THM, read_thm, valid_regs_lem] THEN 663 FULL_SIMP_TAC set_ss [FDOM_FUPDATE] THEN 664 FULL_SIMP_TAC arith_ss [grow_lt_def] THEN 665 Cases_on `e` THEN 666 IMP_RES_TAC valid_regs_lem THEN 667 FULL_SIMP_TAC finmap_ss [eq_exp_def, valid_exp_2_def, eq_addr_def, addr_of_def, valid_exp_def, is_C_def, 668 reade_def, read_thm, addr_in_range_def, in_range_def, fp_def, FP_def] THEN 669 FULL_SIMP_TAC arith_ss [valid_regs_lem] 670 ) g) 671 ); 672 673val POP_ONE_SANITY_2 = Q.store_thm ( 674 "POP_ONE_SANITY_2", 675 `!st h l. valid_exp_2 e /\ valid_exp h /\ grow_lt (read st SP) (SUC (LENGTH l)) ==> 676 let st1 = run_cfl (BLK (pop_one h)) st in 677 grow_lt (read st1 SP) (LENGTH l) 678 `, 679 SIMP_TAC std_ss [FORALL_DSTATE] THEN 680 REPEAT STRIP_TAC THEN 681 IMP_RES_TAC grow_lt_thm THEN 682 IMP_RES_TAC grow_lt_lem_1 THEN 683 Cases_on `h` THEN 684 FULL_SIMP_TAC std_ss [valid_exp_def, valid_regs_lem, pop_one_def,CFL_SEMANTICS_BLK, 685 read_thm, write_thm, SP_def, FP_def] THEN 686 (fn g => (NTAC 3 tac1 THEN FULL_SIMP_TAC finmap_ss [LET_THM, read_thm, valid_regs_lem] THEN 687 FULL_SIMP_TAC set_ss [FDOM_FUPDATE] THEN 688 FULL_SIMP_TAC arith_ss [grow_lt_def] THEN 689 FULL_SIMP_TAC finmap_ss [eq_exp_def, eq_addr_def, addr_of_def, valid_exp_def, valid_exp_2_def, is_C_def, 690 read_thm, addr_in_range_def, in_range_def, fp_def, FP_def] THEN 691 FULL_SIMP_TAC arith_ss [valid_regs_lem] 692 ) g) 693 ); 694 695val POP_ONE_ADDR_IN_RANGE = Q.store_thm ( 696 "POP_ONE_ADDR_IN_RANGE", 697 `!st e h l. EVERY valid_exp l /\ valid_exp h /\ grow_lt (read st SP) (SUC (LENGTH l)) /\ 698 EVERY (\x. ~addr_in_range st x (w2n (read st SP) + SUC (LENGTH l), w2n (read st SP))) l ==> 699 let st' = run_cfl (BLK (pop_one h)) st in 700 EVERY (\x. ~addr_in_range st' x (w2n (read st' SP) + LENGTH l, w2n (read st' SP))) l`, 701 702 SIMP_TAC std_ss [FORALL_DSTATE, LET_THM] THEN 703 REPEAT STRIP_TAC THEN 704 POP_ASSUM MP_TAC THEN 705 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 706 RW_TAC std_ss [] THEN 707 `?st'. run_cfl (BLK (pop_one h)) (regs,mem) = st'` by METIS_TAC [] THEN 708 FULL_SIMP_TAC std_ss [] THEN 709 POP_ASSUM MP_TAC THEN 710 IMP_RES_TAC grow_lt_thm THEN 711 IMP_RES_TAC grow_lt_lem_1 THEN 712 Cases_on `h` THEN 713 FULL_SIMP_TAC std_ss [valid_exp_def, valid_regs_lem, pop_one_def,CFL_SEMANTICS_BLK, 714 read_thm, write_thm, SP_def, FP_def] THEN 715 (fn g => (NTAC 3 tac1 THEN FULL_SIMP_TAC finmap_ss [LET_THM, read_thm, valid_regs_lem] THEN 716 (fn g => REWRITE_TAC [Once EQ_SYM_EQ] g) THEN 717 Cases_on `x` THEN 718 IMP_RES_TAC valid_regs_lem THEN 719 FULL_SIMP_TAC finmap_ss [addr_in_range_def, in_range_def, addr_of_def, 720 valid_exp_def, is_C_def, addr_in_range_def, in_range_def, fp_def, FP_def, read_thm] THEN 721 FULL_SIMP_TAC arith_ss [valid_regs_lem] 722 ) g) 723 ); 724 725val POP_LIST_SP_FP = Q.store_thm ( 726 "POP_LIST_SP_FP", 727 `!l st x. grow_lt (read st SP) (LENGTH l) /\ EVERY valid_exp l 728 ==> let st' = run_cfl (BLK (pop_list l)) st in 729 (w2n (read st' SP) = w2n (read st SP) + LENGTH l) /\ 730 (w2n (read st' FP) = w2n (read st FP)) /\ 731 (w2n (read st' IP) = w2n (read st IP)) `, 732 733 let val tac2 = FULL_SIMP_TAC finmap_ss [LET_THM,read_thm, SP_def, FP_def, IP_def, valid_regs_lem, grow_lt_lem_1] 734 THEN FULL_SIMP_TAC arith_ss [grow_lt_def, valid_regs_def] 735 in 736 Induct_on `l` THENL [ 737 RW_TAC list_ss [CFL_SEMANTICS_BLK, pop_list_def], 738 739 SIMP_TAC list_ss [RUN_CFL_BLK_APPEND, pop_list_def] THEN 740 REPEAT STRIP_TAC THEN 741 IMP_RES_TAC grow_lt_thm THEN 742 `let st1 = run_cfl (BLK (pop_one h)) st in 743 grow_lt (read st1 SP) (LENGTH l) /\ (w2n (read st1 SP) = SUC (w2n (read st SP))) /\ 744 (w2n (read st1 FP) = w2n (read st FP)) /\ (w2n (read st1 IP) = w2n (read st IP))` 745 by SIMP_TAC std_ss [grow_lt_def] THENL [ 746 `?regs mem. st = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN 747 Cases_on `h` THEN 748 FULL_SIMP_TAC list_ss [valid_exp_def, pop_one_def, CFL_SEMANTICS_BLK, read_thm] THENL [ 749 NTAC 2 tac1 THEN tac2, 750 tac1 THEN tac2, 751 NTAC 3 tac1 THEN tac2 752 ], 753 FULL_SIMP_TAC arith_ss [LET_THM] 754 ] 755 ] 756 end 757 ); 758 759val POP_ONE_EXP_LEM_1 = Q.store_thm ( 760 "POP_ONE_EXP_LEM_1", 761 `!h st i. grow_lt (read st SP) 1 /\ valid_exp h /\ ~(eq_exp st h (isM (SUC i + w2n (read st SP)))) ==> 762 let st' = run_cfl (BLK (pop_one h)) st in 763 (st '' (isM (SUC i + w2n (read st SP))) = st' '' (isM (i + w2n (read st' SP))))`, 764 765 let val tac2 = FULL_SIMP_TAC finmap_ss [LET_THM,read_thm, SP_def, FP_def, valid_regs_lem, fp_def] THEN 766 RW_TAC arith_ss [SUC_ONE_ADD] 767 in 768 SIMP_TAC std_ss [FORALL_DSTATE] THEN 769 REPEAT STRIP_TAC THEN 770 IMP_RES_TAC grow_lt_lem_1 THEN 771 Cases_on `h` THEN 772 FULL_SIMP_TAC list_ss [eq_exp_def, eq_addr_def, addr_of_def, valid_exp_def, pop_one_def, CFL_SEMANTICS_BLK, 773 read_thm, reade_def, SP_def, FP_def] THENL [ 774 NTAC 2 tac1 THEN tac2, 775 tac1 THEN tac2, 776 NTAC 3 tac1 THEN tac2 777 ] 778 end 779 ); 780 781val POP_LIST_EXP_INTACT = Q.store_thm ( 782 "POP_LIST_EXP_INTACT", 783 `!l st x e. grow_lt (read st SP) (LENGTH l) /\ EVERY valid_exp l 784 ==> (eq_exp st e x = eq_exp (run_cfl (BLK (pop_list l)) st) e x)`, 785 RW_TAC std_ss [] THEN 786 IMP_RES_TAC POP_LIST_SP_FP THEN 787 Cases_on `e` THEN Cases_on `x` THEN 788 FULL_SIMP_TAC std_ss [eq_exp_def, eq_addr_def, addr_of_def, LET_THM, valid_exp_def] 789 ); 790 791val POP_ONE_EXP_INTACT = Q.store_thm ( 792 "POP_ONE_EXP_INTACT", 793 `!l st e h. grow_lt (read st SP) 1 /\ valid_exp h /\ 794 EVERY (\x. ~eq_exp st e x) l ==> 795 EVERY (\x. ~eq_exp (run_cfl (BLK (pop_one h)) st) e x) l`, 796 REPEAT STRIP_TAC THEN 797 POP_ASSUM MP_TAC THEN 798 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 799 METIS_TAC [(SIMP_RULE list_ss [pop_list_def] o Q.SPECL [`[h]`,`st`]) POP_LIST_EXP_INTACT] 800 ); 801 802(*---------------------------------------------------------------------------------*) 803(* The pop list should contain unique elements *) 804(*---------------------------------------------------------------------------------*) 805 806val unique_exp_list_def = Define ` 807 (unique_exp_list st (h::l) = EVERY (\x. ~eq_exp st h x) l /\ unique_exp_list st l) /\ 808 (unique_exp_list st [] = T)`; 809 810val unique_exp_list_lem_1 = Q.store_thm ( 811 "unique_exp_list_lem_1", 812 `!i h l. i < LENGTH l /\ EVERY (\x. ~eq_exp st h x) l ==> ~eq_exp st (EL i l) h`, 813 Induct_on `l` THEN 814 RW_TAC list_ss [] THEN 815 Cases_on `i` THEN 816 RW_TAC list_ss [] THEN 817 METIS_TAC [eq_exp_SYM] 818 ); 819 820val unique_exp_list_lem_2 = Q.store_thm ( 821 "unique_exp_list_lem_2", 822 `unique_exp_list st l /\ EVERY valid_exp l /\ valid_exp h /\ grow_lt (read st SP) 1 ==> 823 unique_exp_list (run_cfl (BLK (pop_one h)) st) l`, 824 Induct_on `l` THEN 825 RW_TAC list_ss [unique_exp_list_def] THEN 826 METIS_TAC [POP_ONE_EXP_INTACT] 827 ); 828 829(*---------------------------------------------------------------------------------*) 830(* Main Theorems about pop_list *) 831(*---------------------------------------------------------------------------------*) 832 833val POP_LIST_SANITY = Q.store_thm ( 834 "POP_LIST_SANITY", 835 `!l st x. EVERY valid_exp l /\ grow_lt (read st SP) (LENGTH l) 836 ==> !e. EVERY (\x. ~eq_exp st e x) l /\ valid_exp_2 e ==> 837 ((run_cfl (BLK (pop_list l)) st) '' e = st '' e)`, 838 839 Induct_on `l` THENL [ 840 RW_TAC std_ss [CFL_SEMANTICS_BLK, pop_list_def], 841 842 RW_TAC list_ss [RUN_CFL_BLK_APPEND, pop_list_def] THEN 843 IMP_RES_TAC POP_ONE_SANITY THEN 844 Q.ABBREV_TAC `st' = run_cfl (BLK (pop_one h)) st` THEN 845 FULL_SIMP_TAC std_ss [LET_THM] THEN 846 IMP_RES_TAC grow_lt_thm THEN 847 METIS_TAC [POP_ONE_EXP_INTACT] 848 ] 849 ); 850 851 852val POP_LIST_FUNCTIONALITY = Q.store_thm ( 853 "POP_LIST_FUNCTIONALITY", 854 `!l st. EVERY valid_exp l /\ grow_lt (read st SP) (LENGTH l) /\ 855 unique_exp_list st l /\ EVERY (\x.~addr_in_range st x (w2n (read st SP) + LENGTH l, w2n (read st SP))) l 856 ==> !i. i < LENGTH l /\ ~(is_C (EL i l)) /\ valid_exp (EL i l) ==> 857 ((run_cfl (BLK (pop_list l)) st) '' (EL i l) = st '' (isM (w2n (read st SP) + SUC i)))`, 858 859 Induct_on `l` THENL [ 860 RW_TAC list_ss [], 861 862 RW_TAC list_ss [RUN_CFL_BLK_APPEND, pop_list_def, unique_exp_list_def] THEN 863 IMP_RES_TAC grow_lt_thm THEN 864 Cases_on `i` THENL [ 865 866 FULL_SIMP_TAC list_ss [] THEN 867 `(run_cfl (BLK (pop_one h)) st) '' h = st '' isM (w2n (read st SP) + 1)` by ALL_TAC THENL [ 868 IMP_RES_TAC pop_one_lem THEN POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN 869 RW_TAC std_ss [] THEN 870 `(!st1. ~(eq_exp st1 (isR 9) h)) /\ (!st1. ~(eq_exp st1 (isR sp) h))` by (Cases_on `h` THEN 871 FULL_SIMP_TAC std_ss [eq_exp_def, valid_exp_def, valid_regs_lem, sp_def]) THEN 872 `~(isR 9 = isR fp) /\ ~(isR sp = isR fp)` by RW_TAC std_ss [fp_def, sp_def] THEN 873 RW_TAC std_ss [READE_WRITEE_THM_2, READE_WRITEE], 874 875 IMP_RES_TAC valid_exp_thm THEN 876 IMP_RES_TAC POP_ONE_SANITY_2 THEN 877 IMP_RES_TAC POP_ONE_EXP_INTACT THEN POP_ASSUM (K ALL_TAC) THEN 878 FULL_SIMP_TAC std_ss [LET_THM] THEN 879 `legal_pop_exp (run_cfl (BLK (pop_one h)) st) h l` by METIS_TAC [legal_pop_exp_def] THEN 880 FULL_SIMP_TAC std_ss [legal_pop_exp_def] THEN 881 METIS_TAC [POP_LIST_SANITY] 882 ], 883 884 FULL_SIMP_TAC list_ss [] THEN 885 IMP_RES_TAC unique_exp_list_lem_1 THEN 886 IMP_RES_TAC valid_exp_thm THEN 887 IMP_RES_TAC POP_ONE_SANITY THEN 888 IMP_RES_TAC unique_exp_list_lem_2 THEN 889 IMP_RES_TAC (SIMP_RULE list_ss [] POP_ONE_ADDR_IN_RANGE) THEN 890 `~eq_exp st h (isM (SUC (SUC n) + w2n (read st SP)))` by (IMP_RES_TAC ADDR_IN_RANGE_OUTSIDE_2 THEN 891 FULL_SIMP_TAC arith_ss []) THEN 892 FULL_SIMP_TAC std_ss [LET_THM] THEN 893 METIS_TAC [Q.SPECL [`h`,`st`,`SUC n`] (SIMP_RULE std_ss [LET_THM] POP_ONE_EXP_LEM_1)] 894 ] 895 ] 896 ); 897 898(*---------------------------------------------------------------------------------*) 899(* Copy a list to another list *) 900(*---------------------------------------------------------------------------------*) 901 902val copy_list_def = Define ` 903 copy_list dstL srcL = push_list srcL ++ pop_list dstL`; 904 905(*---------------------------------------------------------------------------------*) 906(* Lemmas about copy_list *) 907(*---------------------------------------------------------------------------------*) 908 909val LOCATE_GE_GROW_LT = Q.store_thm ( 910 "LOCATE_GE_GROW_LT", 911 `locate_ge x k /\ (w2n x' = w2n x - k) ==> grow_lt x' k`, 912 RW_TAC arith_ss [locate_ge_def, grow_lt_def, w2n_lt] 913 ); 914 915val LEGAL_PUSH_EXP_DSTATE = Q.store_thm ( 916 "LEGAL_PUSH_EXP_DSTATE", 917 `legal_pop_exp st e l /\ (w2n (read st FP) = w2n (read st' FP)) ==> 918 legal_pop_exp st' e l`, 919 RW_TAC std_ss [legal_pop_exp_def] THEN 920 Q.PAT_ASSUM `EVERY x y` MP_TAC THEN 921 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 922 RW_TAC std_ss [] THEN 923 Cases_on `e` THEN Cases_on `x` THEN 924 FULL_SIMP_TAC std_ss [eq_exp_def, eq_addr_def, addr_of_def] THEN 925 METIS_TAC [] 926 ); 927 928val PUSH_LIST_ADDR_IN_RANGE = Q.store_thm ( 929 "PUSH_LIST_ADDR_IN_RANGE", 930 `!st l1 l2. EVERY valid_exp l1 /\ locate_ge (read st SP) (LENGTH l1) /\ 931 EVERY (\x. ~addr_in_range st x (w2n (read st SP), w2n (read st SP) - LENGTH l1)) l2 ==> 932 let st' = run_cfl (BLK (push_list l1)) st in 933 EVERY (\x. ~addr_in_range st' x (w2n (read st' SP) + LENGTH l1, w2n (read st' SP))) l2`, 934 935 RW_TAC std_ss [LET_THM] THEN 936 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 937 RW_TAC std_ss [] THEN 938 Q.PAT_ASSUM `EVERY x y` MP_TAC THEN 939 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 940 RW_TAC std_ss [] THEN 941 Cases_on `x` THEN 942 FULL_SIMP_TAC arith_ss [addr_in_range_def, in_range_def, addr_of_def, locate_ge_def] 943 ); 944 945val UNIQUE_LIST_THM = Q.store_thm ( 946 "UNIEQUE_LIST_THM", 947 `!st st'. (read st FP = read st' FP) /\ unique_exp_list st l ==> 948 unique_exp_list st' l`, 949 Induct_on `l` THEN 950 RW_TAC std_ss [unique_exp_list_def] THENL [ 951 Q.PAT_ASSUM `EVERY x y` MP_TAC THEN 952 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 953 RW_TAC std_ss [] THEN 954 Cases_on `h` THEN Cases_on `x` THEN 955 FULL_SIMP_TAC std_ss [eq_exp_def, eq_addr_def, addr_of_def] THEN 956 METIS_TAC [], 957 METIS_TAC [] 958 ] 959 ); 960 961 962val ADDR_IN_RANGE_LEGAL_EXP = Q.store_thm ( 963 "ADDR_IN_RANGE_LEGAL_EXP", 964 `!st l. EVERY valid_exp l /\ EVERY ($~ o is_C) l /\ locate_ge (read st SP) (LENGTH l) /\ 965 EVERY (\x. ~addr_in_range st x (w2n (read st SP), w2n (read st SP) - LENGTH l)) l 966 ==> !i. i < LENGTH l ==> legal_push_exp st (EL i l) (PRE (LENGTH l) - i)`, 967 968 RW_TAC std_ss [legal_push_exp_def, EVERY_EL] THEN 969 RES_TAC THEN REPEAT (Q.PAT_ASSUM `!n.x` (K ALL_TAC)) THEN 970 Cases_on `EL i l` THEN 971 FULL_SIMP_TAC std_ss [valid_exp_1_def, addr_in_range_def, in_range_def, addr_of_def, valid_exp_def, 972 valid_regs_lem, locate_ge_def] THEN 973 Q.ABBREV_TAC `x = w2n (read st SP)` THEN Q.ABBREV_TAC `y = w2n (read st FP)` THEN 974 FULL_SIMP_TAC std_ss [NOT_LESS, PRE_SUB1] THEN 975 `(1 + i) <= LENGTH l` by RW_TAC arith_ss [] THEN 976 RW_TAC std_ss [GSYM SUB_PLUS] THEN 977 FULL_SIMP_TAC arith_ss [SUB_RIGHT_ADD] 978 ); 979 980(*---------------------------------------------------------------------------------*) 981(* Main theorems about copy_list *) 982(*---------------------------------------------------------------------------------*) 983 984val COPY_LIST_SANITY = Q.store_thm ( 985 "COPY_LIST_SANITY", 986 `!st dstL srcL. EVERY valid_exp dstL /\ EVERY valid_exp srcL /\ (LENGTH srcL = LENGTH dstL) /\ 987 locate_ge (read st SP) (LENGTH srcL) 988 ==> !e. legal_push_exp st e (LENGTH dstL) /\ legal_pop_exp st e dstL ==> 989 ((run_cfl (BLK (copy_list dstL srcL)) st) '' e = st '' e)`, 990 991 RW_TAC std_ss [copy_list_def, RUN_CFL_BLK_APPEND] THEN 992 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 993 `grow_lt (read (run_cfl (BLK (push_list srcL)) st) SP) (LENGTH dstL)` by METIS_TAC [LOCATE_GE_GROW_LT] THEN 994 IMP_RES_TAC (REWRITE_RULE [Once EQ_SYM_EQ] LEGAL_PUSH_EXP_DSTATE) THEN 995 FULL_SIMP_TAC std_ss [legal_pop_exp_def, legal_push_exp_def] THEN 996 IMP_RES_TAC valid_exp_thm THEN 997 RW_TAC std_ss [POP_LIST_SANITY] THEN 998 METIS_TAC [PUSH_LIST_SANITY, VALID_EXP_LEM] 999 ); 1000 1001val COPY_LIST_FUNCTIONALITY = Q.store_thm ( 1002 "COPY_LIST_FUNCTIONALITY", 1003 `!st dstL srcL. EVERY valid_exp srcL /\ EVERY ($~ o is_C) srcL /\ EVERY ($~ o is_C) dstL /\ 1004 EVERY valid_exp dstL /\ 1005 locate_ge (read st SP) (LENGTH srcL) /\ unique_exp_list st dstL /\ 1006 EVERY (\x. ~addr_in_range st x (w2n (read st SP), w2n (read st SP) - LENGTH srcL)) srcL /\ 1007 EVERY (\x. ~addr_in_range st x (w2n (read st SP), w2n (read st SP) - LENGTH dstL)) dstL /\ 1008 (LENGTH dstL = LENGTH srcL) 1009 ==> !i. i < LENGTH dstL ==> 1010 (run_cfl (BLK (copy_list dstL srcL)) st '' (EL i dstL) = st '' (EL i srcL))`, 1011 1012 RW_TAC std_ss [copy_list_def, RUN_CFL_BLK_APPEND] THEN 1013 `let st' = run_cfl (BLK (push_list srcL)) st in EVERY (\x. ~addr_in_range st' x 1014 (w2n (read st' SP) + LENGTH dstL, w2n (read st' SP))) dstL` by METIS_TAC [PUSH_LIST_ADDR_IN_RANGE] THEN 1015 POP_ASSUM (ASSUME_TAC o SIMP_RULE std_ss [LET_THM]) THEN 1016 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 1017 `read st FP = read (run_cfl (BLK (push_list srcL)) st) FP` by METIS_TAC [w2n_11] THEN 1018 IMP_RES_TAC UNIQUE_LIST_THM THEN 1019 `grow_lt (read (run_cfl (BLK (push_list srcL)) st) SP) (LENGTH dstL)` by METIS_TAC [LOCATE_GE_GROW_LT] THEN 1020 `~is_C (EL i dstL) /\ valid_exp (EL i dstL)` by (FULL_SIMP_TAC std_ss [EVERY_EL] THEN METIS_TAC []) THEN 1021 IMP_RES_TAC valid_exp_thm THEN 1022 RW_TAC std_ss [POP_LIST_FUNCTIONALITY] THEN 1023 NTAC 8 (POP_ASSUM (K ALL_TAC)) THEN 1024 1025 `w2n (read st SP) - PRE (LENGTH srcL) + i = w2n (read st SP) - LENGTH srcL + SUC i` by 1026 FULL_SIMP_TAC arith_ss [locate_ge_def, PRE_SUB1] THEN 1027 `~is_C (EL i srcL) /\ valid_exp (EL i srcL)` by (FULL_SIMP_TAC std_ss [EVERY_EL] THEN 1028 METIS_TAC []) THEN 1029 `legal_push_exp st (EL i srcL) (PRE (LENGTH srcL) - i)` by METIS_TAC [ADDR_IN_RANGE_LEGAL_EXP] THEN 1030 METIS_TAC [PUSH_LIST_FUNCTIONALITY, VALID_EXP_LEM] 1031 ); 1032 1033(*---------------------------------------------------------------------------------*) 1034(* Save and restore a list *) 1035(*---------------------------------------------------------------------------------*) 1036 1037val sr_list_def = Define ` 1038 sr_list (dstL, l, srcL) = push_list srcL ++ l ++ pop_list dstL`; 1039 1040 1041(* Its properites are analogous to copy_list's *) 1042 1043(*---------------------------------------------------------------------------------*) 1044 1045val _ = export_theory(); 1046