1(* 2quietdec := true; 3 4app load ["arithmeticTheory", "wordsTheory", "wordsLib", "pairTheory", "whileTheory", "finite_mapTheory", 5 "listTheory", "pred_setSimps", "pred_setTheory", "preARMTheory", "CFLTheory", "bigInstTheory", 6 "simplifier", "HSLTheory"]; 7 8open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory whileTheory 9 listTheory pred_setSimps pred_setTheory finite_mapTheory preARMTheory CFLTheory bigInstTheory 10 simplifier HSLTheory; 11 12quietdec := false; 13*) 14 15open HolKernel Parse boolLib bossLib numLib arithmeticTheory wordsTheory wordsLib pairTheory whileTheory 16 listTheory pred_setSimps pred_setTheory finite_mapTheory preARMTheory CFLTheory bigInstTheory 17 simplifier HSLTheory; 18 19(*---------------------------------------------------------------------------------*) 20(* This theory is about an implementation of function calls *) 21(* The pre-call processing and post-call processing are fulfilled using *) 22(* fixed routines that comply with ARM Function Call Standard *) 23(* *) 24(* This implementation ensures that: *) 25(* (1) the caller's frame and callee's frame locate in separate areas *) 26(* in the memory. *) 27(* (2) the parameter/result passing and the body execution don't change *) 28(* the values of stack variables in the caller's frame except those for *) 29(* receiving results. *) 30(* (3) all register variables are pushed into memory before parameter passing *) 31(* on function entry and then poped from memory before result passing on *) 32(* function exit. *) 33(*---------------------------------------------------------------------------------*) 34 35val _ = new_theory "funCall"; 36 37(*---------------------------------------------------------------------------------*) 38(* Convert expressions *) 39(*---------------------------------------------------------------------------------*) 40 41val conv_exp_def = Define ` 42 (conv_exp (inR r) = isR (data_reg_index r)) /\ 43 (conv_exp (inC c) = isC c) /\ 44 (conv_exp (inE v) = isV (12 + v))`; 45 46(*---------------------------------------------------------------------------------*) 47(* Compare an HSL state and CFL state *) 48(*---------------------------------------------------------------------------------*) 49 50val same_content_def = Define ` 51 same_content ((rg,sk):TSTATE) (st:DSTATE) m = 52 (!r. rg ' (data_reg_index r) = reade st (conv_exp (inR r))) /\ 53 (!i. i < m ==> (sk ' i = reade st (conv_exp (inE i)))) 54 `; 55 56val same_content_thm = Q.store_thm ( 57 "same_content_htm", 58 `!s st m. same_content s st m = 59 !x. valid_TEXP x m ==> (tread s x = reade st (conv_exp x))`, 60 61 SIMP_TAC std_ss [FORALL_TSTATE, FORALL_DSTATE] THEN 62 RW_TAC std_ss [same_content_def] THEN 63 EQ_TAC THEN 64 RW_TAC std_ss [] THENL [ 65 Cases_on `x` THEN 66 FULL_SIMP_TAC std_ss [tread_def, conv_exp_def, reade_def, read_thm, valid_TEXP_def, within_bound_def], 67 POP_ASSUM (ASSUME_TAC o Q.SPEC `inR r`) THEN 68 FULL_SIMP_TAC std_ss [tread_def, conv_exp_def, reade_def, read_thm, valid_TEXP_def, within_bound_def], 69 Q.PAT_ASSUM `!x.k` (ASSUME_TAC o Q.SPEC `inE i`) THEN 70 FULL_SIMP_TAC std_ss [tread_def, conv_exp_def, reade_def, read_thm, valid_TEXP_def, within_bound_def] 71 ] 72 ); 73 74 75val same_content_read = Q.store_thm ( 76 "same_content_read", 77 `!s st m. same_content s st m /\ EVERY (\x.valid_TEXP x m) lst ==> 78 (MAP (tread s) lst = MAP (reade st o conv_exp) lst)`, 79 80 SIMP_TAC std_ss [FORALL_TSTATE, FORALL_DSTATE] THEN 81 RW_TAC std_ss [same_content_def] THEN 82 Induct_on `lst` THEN 83 RW_TAC list_ss [] THEN 84 Cases_on `h` THEN 85 FULL_SIMP_TAC std_ss [tread_def, conv_exp_def, reade_def, read_thm, valid_TEXP_def, within_bound_def] 86 ); 87 88(*---------------------------------------------------------------------------------*) 89(* Sufficient conditions to implement function calls correctly *) 90(*---------------------------------------------------------------------------------*) 91 92val FC_OUTPUT_LEM = Q.store_thm ( 93 "FC_OUTPUT_LEM", 94 `!s st m1 m2. valid_arg_list (caller_i, caller_o, callee_i, callee_o) /\ 95 WELL_FORMED (SC (SC pre body) post) /\ EVERY (\x.valid_TEXP x m2) callee_o ==> 96 let s1 = transfer (empty_s,s) (callee_i,caller_i) in 97 let st1 = run_cfl pre st in 98 let st2 = run_cfl body st1 in 99 (MAP (reade st o conv_exp) caller_i = MAP (reade st1 o conv_exp) callee_i) /\ 100 same_content (run_hsl S_hsl s1) st2 m2 /\ 101 (MAP (reade st2 o conv_exp) callee_o = MAP (reade (run_cfl post st2) o conv_exp) caller_o) 102 ==> 103 (MAP (tread (run_hsl (Fc (caller_i, callee_i) S_hsl (caller_o, callee_o) (m1,m2)) s)) caller_o = 104 MAP (reade (run_cfl (SC (SC pre body) post) st) o conv_exp) caller_o)`, 105 106 RW_TAC std_ss [valid_arg_list_def, run_hsl_def, WELL_FORMED_thm, SEMANTICS_OF_CFL] THEN 107 `(MAP (tread (transfer (s,s2) (caller_o,callee_o))) caller_o = MAP (tread s2) callee_o) /\ 108 (MAP (tread s) caller_i = MAP (tread s1) callee_i)` by (Q.UNABBREV_TAC `s1` THEN METIS_TAC [TRANSFER_THM]) THEN 109 Q.UNABBREV_TAC `s2` THEN Q.UNABBREV_TAC `s1` THEN 110 `MAP (tread (run_hsl S_hsl (transfer (empty_s,s) (callee_i,caller_i)))) callee_o = 111 MAP (reade (run_cfl body (run_cfl pre st)) o conv_exp) callee_o` by METIS_TAC [same_content_read] THEN 112 FULL_SIMP_TAC std_ss [] 113 ); 114 115 116val MAP_LEM_1 = Q.store_thm ( 117 "MAP_LEM_1", 118 `!x l f g. MEM x l /\ (MAP f l = MAP g l) ==> (f x = g x)`, 119 Induct_on `l` THEN RW_TAC list_ss [] THEN 120 METIS_TAC [] 121 ); 122 123val FC_SUFFICIENT_COND_LEM = Q.store_thm ( 124 "FC_SUFFICIENT_COND_LEM", 125 126 `!s st m1 m2. valid_arg_list (caller_i, caller_o, callee_i, callee_o) /\ 127 WELL_FORMED (SC (SC pre body) post) /\ EVERY (\x.valid_TEXP x m2) callee_o /\ 128 same_content s st m1 129 ==> 130 let s1 = transfer (empty_s,s) (callee_i,caller_i) in 131 let st1 = run_cfl pre st in 132 let st2 = run_cfl body st1 in 133 (MAP (reade st o conv_exp) caller_i = MAP (reade st1 o conv_exp) callee_i) /\ 134 same_content (run_hsl S_hsl s1) st2 m2 /\ 135 (MAP (reade st2 o conv_exp) callee_o = MAP (reade (run_cfl post st2) o conv_exp) caller_o) /\ 136 137 (!x. ~(MEM x caller_o) /\ valid_TEXP x m1 ==> 138 (reade (run_cfl (SC (SC pre body) post) st) (conv_exp x) = reade st (conv_exp x))) 139 ==> 140 same_content (run_hsl (Fc (caller_i, callee_i) S_hsl (caller_o, callee_o) (m1,m2)) s) 141 (run_cfl (SC (SC pre body) post) st) m1`, 142 143 RW_TAC std_ss [] THEN 144 Q.UNABBREV_TAC `s1` THEN Q.UNABBREV_TAC `st1` THEN Q.UNABBREV_TAC `st2` THEN 145 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] FC_OUTPUT_LEM) THEN 146 Q.ABBREV_TAC `st1 = run_cfl (SC (SC pre body) post) st` THEN 147 FULL_SIMP_TAC std_ss [same_content_thm] THEN 148 REPEAT STRIP_TAC THEN 149 Cases_on `MEM x caller_o` THENL [ 150 Q.PAT_ASSUM `!m1.x` (ASSUME_TAC o Q.SPEC `m1`) THEN 151 IMP_RES_TAC MAP_LEM_1 THEN 152 FULL_SIMP_TAC std_ss [], 153 154 FULL_SIMP_TAC std_ss [valid_arg_list_def, run_hsl_def, LET_THM] THEN 155 METIS_TAC [TRANSFER_INTACT] 156 ] 157 ); 158 159(*---------------------------------------------------------------------------------*) 160(* Pre-call processing *) 161(*---------------------------------------------------------------------------------*) 162 163(* We save all registers instead of those modified by the callee for the sake of *) 164(* easier proof *) 165 166val saved_regs_list_def = Define ` 167 saved_regs_list = [isR 0; isR 1; isR 2; isR 3; isR 4; isR 5; isR 6; isR 7; isR 8; isR fp; isR ip; isR lr]`; 168 169val mov_pointers_def = Define ` 170 mov_pointers = 171 [MMOV R12 (MR R13); (* mov ip sp *) 172 MSUB R11 R12 (MC 1w)] (* sub fp ip 1 *) 173 `; 174 175(* k = max (length caller_i, length caller_o) - length caller_i, n = #stack_variables *) 176 177val pre_call_def = Define ` 178 pre_call (caller_i, callee_i) k n = 179 (MSUB R13 R13 (MC (n2w k))) :: 180 push_list (saved_regs_list ++ caller_i) ++ 181 [MADD R13 R13 (MC 12w)] ++ 182 mov_pointers ++ 183 pop_list callee_i ++ 184 [MSUB R13 R11 (MC (n2w (12 + n)))] 185 `; 186 187(*---------------------------------------------------------------------------------*) 188(* Theorems about pre-call processing *) 189(*---------------------------------------------------------------------------------*) 190 191val MAP_LEM_2 = Q.store_thm ( 192 "MAP_LEM_2", 193 `!l f g. (MAP f l = MAP g l) = (!i. i < LENGTH l ==> (f (EL i l) = g (EL i l)))`, 194 Induct_on `l` THEN RW_TAC list_ss [] THEN 195 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 196 Induct_on `i` THEN RW_TAC list_ss [], 197 POP_ASSUM (ASSUME_TAC o Q.SPEC `0`) THEN 198 FULL_SIMP_TAC list_ss [], 199 Q.PAT_ASSUM `!i.k` (ASSUME_TAC o Q.SPEC `SUC i`) THEN 200 FULL_SIMP_TAC list_ss [] 201 ] 202 ); 203 204val MAP_LEM_3 = Q.store_thm ( 205 "MAP_LEM_3", 206 `!l1 l2 f g. (!i. i < LENGTH l1 ==> (f (EL i l1) = g (EL i l2))) /\ 207 (LENGTH l1 = LENGTH l2) ==> (MAP f l1 = MAP g l2)`, 208 Induct_on `l1` THEN Induct_on `l2` THEN 209 RW_TAC list_ss [] THENL [ 210 Q.PAT_ASSUM `!i.k` (ASSUME_TAC o Q.SPEC `0`) THEN 211 FULL_SIMP_TAC list_ss [], 212 `(!i. i < LENGTH l1 ==> (f (EL i l1) = g (EL i l2)))` by ( 213 RW_TAC std_ss [] THEN 214 Q.PAT_ASSUM `!i.k` (ASSUME_TAC o Q.SPEC `SUC i`) THEN 215 FULL_SIMP_TAC list_ss []) THEN 216 METIS_TAC [] 217 ] 218 ); 219 220(* A valid parameter (which is trasferred from the caller to the callee) can be a stack variable, a constant and a register variable *) 221(* A valid argument (which accepts the parameter), on the other hand, can only be either a stack variable or register variable *) 222 223val valid_MEXP_def = Define ` 224 (valid_MEXP (isV i) bound = within_bound i (12 + bound)) /\ 225 (valid_MEXP (isR r) bound = valid_regs r) /\ 226 (valid_MEXP (isC c) bound = T) /\ 227 (valid_MEXP (isM m) bound = F)`; 228 229val valid_MEXP_1_def = Define ` 230 (valid_MEXP_1 (isV i) bound = within_bound i (12 + bound)) /\ 231 (valid_MEXP_1 (isR r) bound = valid_exp_1 (isR r)) /\ 232 (valid_MEXP_1 (isC c) bound = T) /\ 233 (valid_MEXP_1 (isM m) bound = F)`; 234 235val VALID_MEXP_MEXP_1 = Q.store_thm ( 236 "VALID_MEXP_MEXP_1", 237 `!m l. EVERY (\x.valid_MEXP x m) l ==> 238 EVERY (\x.valid_MEXP_1 x m) l`, 239 GEN_TAC THEN MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 240 Cases_on `x` THEN RW_TAC std_ss [valid_MEXP_1_def, valid_MEXP_def] THEN 241 FULL_SIMP_TAC std_ss [valid_regs_def, valid_exp_1_def] 242 ); 243 244val VALID_MEXP_1_exp_3 = Q.store_thm ( 245 "VALID_MEXP_1_exp_3", 246 `!m l. EVERY (\x.valid_MEXP_1 x m) l ==> 247 EVERY valid_exp_3 l`, 248 GEN_TAC THEN MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 249 Cases_on `x` THEN RW_TAC std_ss [valid_MEXP_1_def, valid_exp_3_def, valid_exp_1_def] 250 ); 251 252val VALID_TEXP_MEXP_1 = Q.store_thm ( 253 "VALID_TEXP_MEXP_1", 254 `!l m. EVERY (\x.valid_TEXP x m) l ==> 255 EVERY (\x. valid_MEXP_1 x m) (MAP conv_exp l)`, 256 Induct_on `l` THEN 257 SIMP_TAC list_ss [] THEN 258 Cases_on `h` THEN RW_TAC arith_ss [conv_exp_def,valid_exp_def,valid_MEXP_1_def,valid_TEXP_def, within_bound_def] THEN 259 Cases_on `T'` THEN RW_TAC std_ss [valid_exp_1_def, data_reg_index_def, valid_regs_def, 260 from_reg_index_thm, index_of_reg_def] 261 ); 262 263val VALID_TEXP_MEXP = Q.store_thm ( 264 "VALID_TEXP_MEXP", 265 `!l m. EVERY (\x.valid_TEXP x m) l ==> 266 EVERY (\x. valid_MEXP x m) (MAP conv_exp l)`, 267 Induct_on `l` THEN 268 SIMP_TAC list_ss [] THEN 269 Cases_on `h` THEN RW_TAC arith_ss [conv_exp_def,valid_exp_def,valid_MEXP_def,valid_TEXP_def, within_bound_def] THEN 270 Cases_on `T'` THEN RW_TAC std_ss [valid_exp_1_def, data_reg_index_def, valid_regs_def, 271 from_reg_index_thm, index_of_reg_def] 272 ); 273 274val VALID_MEXP_exp = Q.store_thm ( 275 "VALID_MEXP_exp", 276 `!l m. EVERY (\x.valid_MEXP x m) l ==> EVERY valid_exp l`, 277 Induct_on `l` THEN 278 SIMP_TAC list_ss [] THEN 279 Cases_on `h` THEN RW_TAC arith_ss [conv_exp_def,valid_exp_def,valid_MEXP_def, within_bound_def] THEN 280 METIS_TAC [] 281 ); 282 283 284(* standard frame structure 285 ip | saved lr | 286 fp | saved sp | 287 | saved fp | 288 | saved r8 | 289 | ... | 290 | saved r0 | 291 | local V0 | the first local(stack) variable 292 | ... | 293 | local Vm | the last local(stack) variable 294 sp | | the first avaible empty slot 295*) 296 297val standard_frame_def = Define ` 298 standard_frame st m = 299 (w2n (read st SP) <= w2n (read st FP) - (12 + m)) /\ 300 locate_ge (read st FP) (12 + m)`; 301 302(*---------------------------------------------------------------------------------*) 303(* The caller pushes parameters into the stack *) 304(*---------------------------------------------------------------------------------*) 305 306val LEGAL_PUSH_EXP_LEM = Q.store_thm ( 307 "LEGAL_PUSH_EXP_LEM", 308 `!st l m. standard_frame st m /\ EVERY (\x.valid_MEXP_1 x m) l 309 ==> 310 (!i. i < LENGTH l ==> legal_push_exp st (EL i l) (PRE (LENGTH l) - i))`, 311 312 RW_TAC std_ss [standard_frame_def, legal_push_exp_def] THEN 313 FULL_SIMP_TAC std_ss [EVERY_EL] THEN RES_TAC THEN 314 Cases_on `EL i l` THEN 315 FULL_SIMP_TAC std_ss [conv_exp_def, addr_in_range_def, in_range_def, addr_of_def, valid_MEXP_1_def, 316 valid_exp_1_def, within_bound_def] THEN 317 IMP_RES_TAC LOCATE_GE_GROW_LT THEN 318 IMP_RES_TAC grow_lt_lem_1 THEN 319 FULL_SIMP_TAC std_ss [locate_ge_def] THEN 320 Q.ABBREV_TAC `x = read st SP` THEN 321 Cases_on `w2n (read st FP) <= n + w2n (x:word32)` THEN 322 RW_TAC std_ss [] THEN RW_TAC arith_ss [] 323 ); 324 325val tac1 = (fn g => 326 ((CONV_TAC (DEPTH_CONV ( 327 REWRITE_CONV [Once mdecode_def] THENC 328 SIMP_CONV finmap_ss [write_thm, read_thm, toMEM_def, toEXP_def, toREG_def, index_of_reg_def]))) THEN 329 FULL_SIMP_TAC std_ss [word_0_n2w, GSYM WORD_SUB_PLUS]) 330 g); 331 332 333val PRE_CALL_PUSH_ARGUMENTS = Q.store_thm ( 334 "PRE_CALL_PUSH_ARGUMENTS", 335 `!st l m k. locate_ge (read st SP) (k + LENGTH l) /\ 336 standard_frame st m /\ EVERY (\x.valid_MEXP_1 x m) l 337 ==> 338 !i. i < LENGTH l ==> 339 ((run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: push_list l)) st) '' 340 (isM (w2n (read st SP) - k - PRE (LENGTH l) + i)) = st '' (EL i l))`, 341 342 SIMP_TAC std_ss [FORALL_DSTATE] THEN 343 RW_TAC std_ss [CFL_SEMANTICS_BLK] THEN 344 tac1 THEN 345 FULL_SIMP_TAC std_ss [read_thm, SP_def] THEN 346 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 13 - n2w k),mem)` THEN 347 `locate_ge (read st1 SP) (LENGTH l) /\ standard_frame st1 m /\ 348 (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [ 349 Q.UNABBREV_TAC `st1` THEN 350 IMP_RES_TAC locate_ge_lem_1 THEN 351 FULL_SIMP_TAC finmap_ss [read_thm, locate_ge_def, SP_def, FP_def, standard_frame_def] THEN 352 `w2n ((n2w k):word32) = k` by ( 353 WORDS_TAC THEN `w2n (regs ' 13) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 354 `k < dimword (:32)` by RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN WORDS_TAC THEN RW_TAC arith_ss []) THEN 355 Q.PAT_ASSUM `!i.k` (ASSUME_TAC o Q.SPEC `(n2w k):word32`) THEN 356 FULL_SIMP_TAC arith_ss [], 357 358 `legal_push_exp st1 (EL i l) (PRE (LENGTH l) - i)` by METIS_TAC [LEGAL_PUSH_EXP_LEM] THEN 359 IMP_RES_TAC VALID_MEXP_1_exp_3 THEN 360 IMP_RES_TAC PUSH_LIST_FUNCTIONALITY THEN 361 FULL_SIMP_TAC std_ss [EVERY_EL] THEN RES_TAC THEN 362 Q.UNABBREV_TAC `st1` THEN 363 Cases_on `EL i l` THEN 364 FULL_SIMP_TAC finmap_ss [reade_def, read_thm, fp_def, valid_exp_3_def, valid_MEXP_1_def, valid_exp_1_def] 365 ] 366 ); 367 368val above_lem_1 = Q.store_thm ( 369 "above_lem_1", 370 `!st n. i > w2n (read st SP) 371 ==> ~addr_in_range st (isM i) (w2n (read st SP),w2n (read st SP) - n)`, 372 RW_TAC arith_ss [addr_in_range_def, in_range_def, addr_of_def] 373 ); 374 375val PRE_CALL_SANITY_1 = Q.store_thm ( 376 "PRE_CALL_SANITY_1", 377 `!st l k m. locate_ge (read st SP) (k + LENGTH l) /\ EVERY (\x.valid_MEXP_1 x m) l 378 ==> 379 let st' = run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: push_list l)) st in 380 (!i. i > w2n (read st SP) ==> (st '' (isM i) = st' '' (isM i))) /\ 381 (w2n (read st' SP) = w2n (read st SP) - (k + LENGTH l))`, 382 383 SIMP_TAC std_ss [FORALL_DSTATE] THEN 384 REPEAT GEN_TAC THEN STRIP_TAC THEN 385 SIMP_TAC std_ss [CFL_SEMANTICS_BLK] THEN 386 tac1 THEN 387 FULL_SIMP_TAC std_ss [LET_THM, read_thm, SP_def] THEN 388 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 13 - n2w k),mem)` THEN 389 `locate_ge (read st1 SP) (LENGTH l) /\ (w2n (regs ' 13) - k = w2n (read st1 SP))` by ALL_TAC THENL [ 390 Q.UNABBREV_TAC `st1` THEN 391 IMP_RES_TAC locate_ge_lem_1 THEN 392 FULL_SIMP_TAC finmap_ss [read_thm, locate_ge_def, SP_def, FP_def] THEN 393 `w2n ((n2w k):word32) = k` by ( 394 WORDS_TAC THEN `w2n (regs ' 13) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 395 `k < dimword (:32)` by RW_TAC arith_ss [] THEN POP_ASSUM MP_TAC THEN WORDS_TAC THEN RW_TAC arith_ss []) THEN 396 Q.PAT_ASSUM `!i.k` (ASSUME_TAC o Q.SPEC `(n2w k):word32`) THEN 397 FULL_SIMP_TAC arith_ss [], 398 399 RW_TAC std_ss [] THENL [ 400 `i > w2n (read st1 SP)` by RW_TAC arith_ss [] THEN 401 IMP_RES_TAC above_lem_1 THEN 402 POP_ASSUM (ASSUME_TAC o Q.SPEC `LENGTH (l:CFL_EXP list)`) THEN 403 FULL_SIMP_TAC std_ss [] THEN 404 `valid_exp_1 (isM i)` by RW_TAC std_ss [valid_exp_1_def] THEN 405 IMP_RES_TAC VALID_MEXP_1_exp_3 THEN 406 RW_TAC std_ss [PUSH_LIST_SANITY] THEN 407 Q.UNABBREV_TAC `st1` THEN 408 FULL_SIMP_TAC finmap_ss [reade_def], 409 410 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 411 FULL_SIMP_TAC arith_ss [SP_def, locate_ge_def] 412 ] 413 ] 414 ); 415 416 417(*---------------------------------------------------------------------------------*) 418(* The callee pops the parameters out of the stack *) 419(*---------------------------------------------------------------------------------*) 420 421val LEGAL_POP_EXP_LEM = Q.store_thm ( 422 "LEGAL_POP_EXP_LEM", 423 `!st l m. w2n (read st FP) <= w2n (read st SP) /\ EVERY (\x.valid_TEXP x m) l 424 ==> 425 EVERY (\x.~addr_in_range st x (w2n (read st SP) + LENGTH (MAP conv_exp l), w2n (read st SP))) (MAP conv_exp l)`, 426 427 REPEAT STRIP_TAC THEN 428 IMP_RES_TAC VALID_EXP_LEM THEN 429 FULL_SIMP_TAC list_ss [EVERY_EL, rich_listTheory.EL_MAP] THEN 430 RW_TAC std_ss [] THEN RES_TAC THEN 431 Cases_on `EL n l` THEN 432 FULL_SIMP_TAC std_ss [conv_exp_def, addr_in_range_def, in_range_def, addr_of_def, valid_exp_def, 433 valid_regs_lem, within_bound_def] THEN 434 RW_TAC arith_ss [] 435 ); 436 437val UNIQUE_LIST_11 = Q.store_thm ( 438 "UNIQUE_LIST_11", 439 `!l st. locate_ge (read st FP) (12 + m) /\ EVERY (\x. valid_TEXP x m) l /\ unique_list l ==> 440 unique_exp_list st (MAP conv_exp l)`, 441 442 Induct_on `l` THEN RW_TAC list_ss [unique_exp_list_def, unique_list_def] THEN 443 FULL_SIMP_TAC list_ss [EVERY_EL, rich_listTheory.EL_MAP] THEN 444 RW_TAC std_ss [] THEN 445 REPEAT (Q.PAT_ASSUM `!n.k` (ASSUME_TAC o Q.SPEC `n`)) THEN 446 IMP_RES_TAC locate_ge_lem_1 THEN 447 Cases_on `EL n l` THEN Cases_on `h` THEN 448 FULL_SIMP_TAC std_ss [locate_ge_def, conv_exp_def, eq_exp_def, eq_addr_def, addr_of_def, valid_TEXP_def] THENL [ 449 Cases_on `T''` THEN Cases_on `T'` THEN 450 FULL_SIMP_TAC std_ss [data_reg_index_def], 451 METIS_TAC [], 452 FULL_SIMP_TAC std_ss [within_bound_def] THEN RW_TAC arith_ss [] THEN STRIP_TAC THEN 453 FULL_SIMP_TAC arith_ss [] 454 ] 455 ); 456 457val grow_lt_lem_2 = Q.store_thm ( 458 "grow_lt_lem_2", 459 `grow_lt (x:word32) (k:num) ==> 460 !i. i <= k ==> (w2n (x + n2w i) = w2n x + i)`, 461 RW_TAC arith_ss [grow_lt_def, word_add_def, w2n_n2w] 462 ); 463 464val notC_LEM = Q.store_thm ( 465 "notC_LEM", 466 `!l. EVERY notC l ==> 467 EVERY ($~ o is_C) (MAP conv_exp l)`, 468 Induct_on `l` THEN 469 RW_TAC list_ss [] THEN 470 Cases_on `h` THEN 471 FULL_SIMP_TAC std_ss [conv_exp_def, notC_def, is_C_def] 472 ); 473 474val PRE_CALL_POP_ARGUMENTS = Q.store_thm ( 475 "PRE_CALL_POP_ARGUMENTS", 476 `!st l m. grow_lt (read st SP) (12 + LENGTH l) /\ locate_ge (read st SP) (m + 1) /\ EVERY notC l /\ 477 unique_list l /\ EVERY (\x.valid_TEXP x m) l /\ (MAP conv_exp l = l') 478 ==> 479 !i. i < LENGTH l' ==> 480 ((run_cfl (BLK ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list l')) st) '' (EL i l') = 481 st '' (isM (12 + w2n (read st SP) + SUC i)))`, 482 483 SIMP_TAC std_ss [FORALL_DSTATE, mov_pointers_def] THEN 484 RW_TAC std_ss [APPEND, CFL_SEMANTICS_BLK] THEN 485 NTAC 3 tac1 THEN 486 FULL_SIMP_TAC std_ss [read_thm, SP_def] THEN 487 Q.ABBREV_TAC `st1 = (regs |+ (11,regs ' 13 + 12w - 1w) |+ (12,regs ' 13 + 12w) |+ (13,regs ' 13 + 12w),mem)` THEN 488 489 `grow_lt (read st1 SP) (LENGTH (MAP conv_exp l)) /\ w2n (read st1 FP) <= w2n (read st1 SP) /\ 490 locate_ge (read st1 FP) (12 + m) /\ (w2n (regs ' 13) + 12 = w2n (read st1 SP))` by ALL_TAC THENL [ 491 Q.UNABBREV_TAC `st1` THEN 492 IMP_RES_TAC locate_ge_lem_1 THEN 493 IMP_RES_TAC grow_lt_lem_2 THEN 494 `LENGTH (MAP conv_exp l) = LENGTH l` by METIS_TAC [LENGTH_MAP] THEN 495 FULL_SIMP_TAC finmap_ss [read_thm, locate_ge_def, grow_lt_def, SP_def, FP_def] THEN 496 `12w - 1w = (11w:word32)` by WORDS_TAC THEN 497 RW_TAC arith_ss [WORD_ADD_SUB_ASSOC], 498 499 IMP_RES_TAC UNIQUE_LIST_11 THEN 500 IMP_RES_TAC VALID_TEXP_MEXP THEN 501 IMP_RES_TAC VALID_MEXP_exp THEN 502 IMP_RES_TAC LEGAL_POP_EXP_LEM THEN 503 `i < LENGTH l` by METIS_TAC [LENGTH_MAP] THEN 504 IMP_RES_TAC notC_LEM THEN 505 IMP_RES_TAC POP_LIST_FUNCTIONALITY THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 506 FULL_SIMP_TAC arith_ss [EVERY_EL] THEN 507 Q.UNABBREV_TAC `st1` THEN 508 RW_TAC finmap_ss [reade_def, read_thm] 509 ] 510 ); 511 512 513val above_lem_2 = Q.store_thm ( 514 "above_lem_2", 515 `!i l st. EVERY (\x. valid_MEXP x m) l /\ i > w2n (read st FP) 516 ==> EVERY (\x. ~eq_exp st (isM i) x) l`, 517 518 RW_TAC std_ss [] THEN 519 Q.PAT_ASSUM `EVERY k l` MP_TAC THEN 520 MATCH_MP_TAC listTheory.EVERY_MONOTONIC THEN 521 Cases_on `x` THEN RW_TAC arith_ss [eq_exp_def, valid_MEXP_def, eq_addr_def, addr_of_def] 522 ); 523 524 525val PRE_CALL_SANITY_2 = Q.store_thm ( 526 "PRE_CALL_SANITY_2", 527 `!st. grow_lt (read st SP) (12 + LENGTH l) /\ EVERY (\x.valid_MEXP x m) l 528 ==> 529 let st' = run_cfl (BLK ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list l)) st in 530 (!i. i > 12 + w2n (read st SP) ==> (st '' (isM i) = st' '' (isM i))) /\ 531 (w2n (read st' SP) = w2n (read st SP) + 12 + (LENGTH l)) /\ 532 (w2n (read st' FP) = w2n (read st SP) + 11) /\ 533 (w2n (read st' IP) = w2n (read st' FP) + 1)`, 534 535 SIMP_TAC std_ss [FORALL_DSTATE, mov_pointers_def] THEN 536 SIMP_TAC std_ss [APPEND, CFL_SEMANTICS_BLK] THEN 537 NTAC 3 tac1 THEN 538 SIMP_TAC std_ss [read_thm, FP_def, SP_def, LET_THM] THEN 539 REPEAT GEN_TAC THEN STRIP_TAC THEN 540 Q.ABBREV_TAC `st1 = (regs |+ (11,regs ' 13 + 12w - 1w) |+ (12,regs ' 13 + 12w) |+ (13,regs ' 13 + 12w),mem)` THEN 541 542 `grow_lt (read st1 SP) (LENGTH l) /\ (w2n (regs ' 13) + 12 = w2n (read st1 SP)) /\ 543 (w2n (regs ' 13) + 11 = w2n (read st1 FP)) /\ (w2n (read st1 IP) = w2n (read st1 FP) + 1)` by ( 544 Q.UNABBREV_TAC `st1` THEN IMP_RES_TAC grow_lt_lem_2 THEN 545 FULL_SIMP_TAC finmap_ss [read_thm, grow_lt_def, SP_def, FP_def, IP_def] THEN 546 `12w - 1w = (11w:word32)` by WORDS_TAC THEN 547 RW_TAC arith_ss [WORD_ADD_SUB_ASSOC]) THEN 548 549 IMP_RES_TAC VALID_MEXP_exp THEN STRIP_TAC THENL [ 550 REPEAT STRIP_TAC THEN 551 `i > w2n (read st1 FP)` by RW_TAC arith_ss [] THEN 552 IMP_RES_TAC above_lem_2 THEN 553 `valid_exp_2 (isM i)` by RW_TAC std_ss [valid_exp_2_def] THEN 554 RW_TAC std_ss [POP_LIST_SANITY] THEN 555 Q.UNABBREV_TAC `st1` THEN 556 FULL_SIMP_TAC finmap_ss [reade_def], 557 558 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] POP_LIST_SP_FP) THEN 559 FULL_SIMP_TAC arith_ss [SP_def, FP_def, IP_def] 560 ] 561 ); 562 563val above_lem_3 = Q.store_thm ( 564 "above_lem_3", 565 `!i l st. EVERY (\x. valid_TEXP x m) l /\ i > w2n (read st FP) - 12 566 ==> EVERY (\x. ~eq_exp st (isM i) x) (MAP conv_exp l)`, 567 568 Induct_on `l` THEN RW_TAC list_ss [] THEN 569 Cases_on `h` THEN RW_TAC arith_ss [eq_exp_def, valid_MEXP_def, eq_addr_def, addr_of_def, 570 conv_exp_def, within_bound_def] 571 ); 572 573val PRE_CALL_SANITY_2' = Q.store_thm ( 574 "PRE_CALL_SANITY_2'", 575 `!st. grow_lt (read st SP) (12 + LENGTH l) /\ EVERY (\x.valid_TEXP x m) l 576 ==> 577 let st' = run_cfl (BLK ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp l))) st in 578 (!i. i > w2n (read st SP) - 1 ==> (st '' (isM i) = st' '' (isM i)))`, 579 580 SIMP_TAC std_ss [FORALL_DSTATE, mov_pointers_def] THEN 581 SIMP_TAC std_ss [APPEND, CFL_SEMANTICS_BLK] THEN 582 NTAC 3 tac1 THEN 583 RW_TAC std_ss [SP_def, LET_THM] THEN 584 Q.ABBREV_TAC `st1 = (regs |+ (11,regs ' 13 + 12w - 1w) |+ (12,regs ' 13 + 12w) |+ (13,regs ' 13 + 12w),mem)` THEN 585 `grow_lt (read st1 SP) (LENGTH (MAP conv_exp l)) /\ (w2n (read st1 FP) = w2n (read (regs,mem) SP) + 11)` 586 by (Q.UNABBREV_TAC `st1` THEN IMP_RES_TAC grow_lt_lem_2 THEN 587 `12w - 1w = (11w:word32)` by WORDS_TAC THEN FULL_SIMP_TAC finmap_ss [read_thm, grow_lt_def, LENGTH_MAP, 588 FP_def, SP_def] THEN RW_TAC arith_ss [WORD_ADD_SUB_ASSOC]) THEN 589 590 `i > w2n (read st1 FP) - 12` by RW_TAC arith_ss [SP_def] THEN 591 IMP_RES_TAC above_lem_3 THEN 592 IMP_RES_TAC VALID_TEXP_MEXP THEN 593 IMP_RES_TAC VALID_MEXP_exp THEN 594 `valid_exp_2 (isM i)` by RW_TAC std_ss [valid_exp_2_def] THEN 595 RW_TAC std_ss [POP_LIST_SANITY] THEN 596 Q.UNABBREV_TAC `st1` THEN 597 FULL_SIMP_TAC finmap_ss [reade_def] 598 ); 599 600(*---------------------------------------------------------------------------------*) 601(* Lemmas bout pre-call processing *) 602(*---------------------------------------------------------------------------------*) 603 604val valid_MEXP_1_saved_regs = Q.store_thm ( 605 "valid_MEXP_1_saved_regs", 606 `!m. EVERY (\x. valid_MEXP_1 x m) saved_regs_list`, 607 RW_TAC list_ss [saved_regs_list_def, valid_MEXP_1_def] THEN 608 RW_TAC std_ss [valid_exp_1_def, from_reg_index_thm, index_of_reg_def, fp_def, lr_def, ip_def] 609 ); 610 611val PRE_CALL_PASS_ARGUMENTS_LEM_1 = Q.store_thm ( 612 "PRE_CALL_PASS_ARGUMENTS_LEM_1", 613 `!st st' k l. 614 locate_ge (read st SP) (k + 13 + LENGTH l + m) /\ 615 (w2n (read st' SP) = w2n (read st SP) - (k + LENGTH (saved_regs_list ++ l))) ==> 616 grow_lt (read st' SP) (12 + LENGTH l) /\ locate_ge (read st' SP) (m + 1)`, 617 618 RW_TAC list_ss [grow_lt_def, locate_ge_def, saved_regs_list_def] THENL [ 619 `w2n (read st SP) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 620 RW_TAC arith_ss [], 621 WORDS_TAC 622 ] 623 ); 624 625val PRE_CALL_PASS_ARGUMENTS_LEM_2 = Q.store_thm ( 626 "PRE_CALL_PASS_ARGUMENTS_LEM_2", 627 `!x k m i j. locate_ge x (k + m) /\ 0 < m ==> 628 (j + (w2n x - (k + m)) + SUC i = w2n x - k - PRE m + (j + i))`, 629 RW_TAC std_ss [locate_ge_def, PRE_SUB1, SUC_ONE_ADD] THEN 630 Cases_on `m` THEN 631 RW_TAC arith_ss [] 632 ); 633 634val EL_APPEND_3 = Q.store_thm ( 635 "EL_APPEND_3", 636 `!l1 l2 n. EL (LENGTH l1 + n) (l1 ++ l2) = EL n l2`, 637 RW_TAC arith_ss [rich_listTheory.EL_APPEND2] 638 ); 639 640(*---------------------------------------------------------------------------------*) 641(* The pre-call processing passes the parameters. *) 642(* We need to keep track of how sp,fp and ip are changed. *) 643(* Note that r0-r8,fp,ip and lr are also pushed into the stack *) 644(*---------------------------------------------------------------------------------*) 645 646val tac3 = 647 Q.ABBREV_TAC `l1 = [MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i)` THEN 648 REWRITE_TAC [RUN_CFL_BLK_APPEND] THEN 649 `EVERY (\x.valid_MEXP_1 x m1) (saved_regs_list ++ MAP conv_exp caller_i)` by 650 METIS_TAC [EVERY_APPEND, valid_MEXP_1_saved_regs, VALID_TEXP_MEXP_1] THEN 651 Q.ABBREV_TAC `st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k)):: 652 push_list (saved_regs_list ++ MAP conv_exp caller_i))) st` THEN 653 `LENGTH (MAP conv_exp caller_i) = LENGTH caller_i` by METIS_TAC [LENGTH_MAP] THEN 654 `locate_ge (read st SP) (k + LENGTH (saved_regs_list ++ MAP conv_exp caller_i))` by 655 FULL_SIMP_TAC list_ss [locate_ge_def, saved_regs_list_def] THEN 656 `grow_lt (read st' SP) (12 + LENGTH callee_i) /\ locate_ge (read st' SP) (m2 + 1)` by 657 (Q.UNABBREV_TAC `st'` THEN METIS_TAC [PRE_CALL_PASS_ARGUMENTS_LEM_1, 658 SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1]) THEN 659 Q.UNABBREV_TAC `l1` 660 ; 661 662 663val PRE_CALL_SANITY_3 = Q.store_thm ( 664 "PRE_CALL_SANITY_3", 665 ` locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 666 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 667 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 668 ==> 669 let st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k))::push_list (saved_regs_list ++ MAP conv_exp caller_i) ++ 670 ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i)))) st in 671 (!i. i > w2n (read st SP) ==> (st '' (isM i) = st' '' (isM i))) /\ 672 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 673 (w2n (read st' IP) = w2n (read st' FP) + 1)`, 674 675 REPEAT GEN_TAC THEN STRIP_TAC THEN 676 SIMP_TAC std_ss [LET_THM] THEN 677 tac3 THEN 678 IMP_RES_TAC VALID_TEXP_MEXP THEN 679 `grow_lt (read st' SP) (12 + LENGTH (MAP conv_exp callee_i))` by METIS_TAC [LENGTH_MAP] THEN 680 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_2) THEN 681 NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN RW_TAC std_ss [] THENL [ 682 683 REPEAT (Q.PAT_ASSUM `w2n x = y` (K ALL_TAC)) THEN 684 `i > 12 + w2n (read st' SP)` by 685 (`w2n (read st' SP) = w2n (read st SP) - (k + LENGTH (saved_regs_list ++ MAP conv_exp caller_i))` by 686 (Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1]) THEN 687 `LENGTH saved_regs_list = 12` by RW_TAC list_ss [saved_regs_list_def] THEN 688 FULL_SIMP_TAC list_ss [locate_ge_def]) THEN 689 RES_TAC THEN POP_ASSUM ((fn th => REWRITE_TAC [th]) o GSYM) THEN 690 Q.UNABBREV_TAC `st'` THEN 691 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1), 692 693 Q.UNABBREV_TAC `st'` THEN 694 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1) THEN 695 RW_TAC std_ss [] THEN NTAC 11 (POP_ASSUM (K ALL_TAC)) THEN 696 `LENGTH saved_regs_list = 12` by RW_TAC list_ss [saved_regs_list_def] THEN 697 FULL_SIMP_TAC list_ss [locate_ge_def] 698 ] 699 ); 700 701 702val PRE_CALL_SAVED_REGS_LEM = Q.store_thm ( 703 "PRE_CALL_SAVED_REGS_LEM", 704 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 705 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 706 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 707 ==> 708 let st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k))::push_list (saved_regs_list ++ MAP conv_exp caller_i) ++ 709 ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i)))) st in 710 !i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))`, 711 712 REPEAT GEN_TAC THEN STRIP_TAC THEN 713 SIMP_TAC std_ss [LET_THM] THEN 714 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_3) THEN NTAC 40 (POP_ASSUM (K ALL_TAC)) THEN 715 RW_TAC std_ss [] THEN POP_ASSUM MP_TAC THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 716 tac3 THEN 717 IMP_RES_TAC VALID_TEXP_MEXP THEN 718 `grow_lt (read st' SP) (12 + LENGTH (MAP conv_exp callee_i))` by METIS_TAC [LENGTH_MAP] THEN 719 `w2n (read st SP) - (k + LENGTH caller_i) - 1 - 10 + i > w2n (read st' SP) - 1` by 720 (`w2n (read st' SP) = w2n (read st SP) - (k + LENGTH (saved_regs_list ++ MAP conv_exp caller_i))` by 721 (Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1]) THEN 722 `LENGTH saved_regs_list = 12` by RW_TAC list_ss [saved_regs_list_def] THEN 723 RW_TAC std_ss [LENGTH_APPEND] THEN NTAC 17 (POP_ASSUM (K ALL_TAC)) THEN 724 FULL_SIMP_TAC arith_ss [locate_ge_def] 725 ) THEN 726 IMP_RES_TAC (GSYM (SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_2')) THEN 727 RW_TAC std_ss [] THEN POP_ASSUM MP_TAC THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 728 729 `LENGTH saved_regs_list = 12` by RW_TAC list_ss [saved_regs_list_def] THEN STRIP_TAC THEN 730 `w2n (read st SP) - (k + LENGTH caller_i) - 1 - 10 + i = 731 w2n (read st SP) - k - PRE (LENGTH (saved_regs_list ++ MAP conv_exp caller_i)) + i` by ( 732 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 16 (POP_ASSUM (K ALL_TAC)) THEN 733 RW_TAC std_ss [LENGTH_APPEND, LENGTH_MAP] THEN 734 FULL_SIMP_TAC arith_ss [locate_ge_def, PRE_SUB1]) THEN 735 RW_TAC std_ss [] THEN 736 737 `i < LENGTH (saved_regs_list ++ MAP conv_exp caller_i)` by METIS_TAC 738 [LENGTH_APPEND, LENGTH_MAP, LESS_IMP_LESS_ADD] THEN 739 IMP_RES_TAC PRE_CALL_PUSH_ARGUMENTS THEN 740 Q.UNABBREV_TAC `st'` THEN 741 RW_TAC list_ss [rich_listTheory.EL_APPEND1] 742 ); 743 744(*---------------------------------------------------------------------------------*) 745(* Pre-call processing accomplished the argument passing task *) 746(*---------------------------------------------------------------------------------*) 747 748val PRE_CALL_PASS_ARGUMENTS_LEM = Q.store_thm ( 749 "PRE_CALL_PASS_ARGUMENTS_LEM", 750 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 751 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 752 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 753 ==> 754 !i. i < LENGTH caller_i ==> 755 ((run_cfl (BLK (MSUB R13 R13 (MC (n2w k))::push_list (saved_regs_list ++ MAP conv_exp caller_i) ++ 756 ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i)))) st) '' 757 (EL i (MAP conv_exp callee_i)) = st '' (EL i (MAP conv_exp caller_i)))`, 758 759 RW_TAC bool_ss [] THEN 760 tac3 THEN 761 IMP_RES_TAC PRE_CALL_POP_ARGUMENTS THEN NTAC 31 (POP_ASSUM (K ALL_TAC)) THEN 762 `i < LENGTH (MAP conv_exp callee_i)` by METIS_TAC [LENGTH_MAP] THEN 763 FULL_SIMP_TAC std_ss [] THEN RES_TAC THEN 764 RW_TAC std_ss [] THEN NTAC 5 (POP_ASSUM (K ALL_TAC)) THEN 765 766 `LENGTH saved_regs_list = 12` by RW_TAC list_ss [saved_regs_list_def] THEN 767 `0 < LENGTH (saved_regs_list ++ MAP conv_exp caller_i)` by RW_TAC list_ss [] THEN 768 `12 + w2n (read st' SP) + SUC i = w2n (read st SP) - k - 769 PRE (LENGTH (saved_regs_list ++ MAP conv_exp caller_i)) + (12 + i)` by 770 (Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1, 771 PRE_CALL_PASS_ARGUMENTS_LEM_2]) THEN 772 RW_TAC std_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 773 Q.UNABBREV_TAC `st'` THEN 774 `12 + i < LENGTH (saved_regs_list ++ MAP conv_exp caller_i)` by RW_TAC list_ss [] THEN 775 IMP_RES_TAC PRE_CALL_PUSH_ARGUMENTS THEN 776 RW_TAC list_ss [] THEN 777 METIS_TAC [EL_APPEND_3, ADD_SYM] 778 ); 779 780 781(*---------------------------------------------------------------------------------*) 782(* Some Lemmas *) 783(*---------------------------------------------------------------------------------*) 784 785val MOD_LE = Q.store_thm ( 786 "MOD_LE", 787 `!i n. 0 < n ==> i MOD n <= i`, 788 REPEAT STRIP_TAC THEN 789 IMP_RES_TAC (Q.SPECL [`\j. j <= i`,`i`,`n`] MOD_ELIM) THEN 790 FULL_SIMP_TAC arith_ss [] 791 ); 792 793val locate_ge_lem_3 = Q.store_thm ( 794 "locate_ge_lem_3", 795 `!x k.locate_ge x k ==> !i. i <= k ==> (w2n (x - n2w i) = w2n x - i)`, 796 REPEAT STRIP_TAC THEN 797 IMP_RES_TAC locate_ge_lem_1 THEN 798 POP_ASSUM (ASSUME_TAC o Q.SPEC `n2w i:word32`) THEN 799 FULL_SIMP_TAC std_ss [locate_ge_def] THEN 800 `w2n x < dimword (:32)` by RW_TAC arith_ss [w2n_lt] THEN 801 `w2n (n2w i:word32) = i` by RW_TAC arith_ss [w2n_n2w] THEN 802 METIS_TAC [MOD_LE, LESS_EQ_TRANS] 803 ); 804 805val sub_sp_lem_1 = Q.store_thm ( 806 "sub_sp_lem_1", 807 `!st m. locate_ge (read st FP) (12 + m) ==> 808 let st1 = run_cfl (BLK [MSUB R13 R11 (MC (n2w (12 + m)))]) st in 809 (!i. st1 '' isM i = st '' isM i) /\ 810 (w2n (read st1 FP) = w2n (read st FP)) /\ 811 (w2n (read st1 IP) = w2n (read st IP)) /\ 812 (w2n (read st1 SP) = w2n (read st FP) - (12 + m)) /\ 813 (!l. EVERY (\x.valid_TEXP x m) l ==> !i. i < LENGTH l ==> 814 (st1 '' (EL i (MAP conv_exp l)) = st '' (EL i (MAP conv_exp l))))`, 815 816 SIMP_TAC std_ss [FORALL_DSTATE, APPEND, CFL_SEMANTICS_BLK] THEN 817 tac1 THEN 818 RW_TAC finmap_ss [LET_THM, FP_def, IP_def, SP_def, read_thm, reade_def] THENL [ 819 IMP_RES_TAC locate_ge_lem_3 THEN RW_TAC arith_ss [], 820 821 IMP_RES_TAC VALID_TEXP_MEXP THEN 822 IMP_RES_TAC VALID_MEXP_exp THEN 823 `i < LENGTH (MAP conv_exp l)` by METIS_TAC [LENGTH_MAP] THEN 824 FULL_SIMP_TAC std_ss [EVERY_EL] THEN RES_TAC THEN 825 Cases_on `EL i (MAP conv_exp l)` THEN 826 FULL_SIMP_TAC finmap_ss [tread_def, conv_exp_def, reade_def, read_thm, 827 valid_exp_def, valid_regs_lem, fp_def, within_bound_def] 828 ] 829 ); 830 831(*---------------------------------------------------------------------------------*) 832(* An optimization on the implementation of register saving *) 833(*---------------------------------------------------------------------------------*) 834 835val [FOLDL_NIL, FOLDL_CONS] = CONJUNCTS FOLDL; 836 837val PUSH_TAC = 838 CONV_TAC (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, pushL_def])) THEN 839 REWRITE_TAC [GSYM rich_listTheory.MAP_REVERSE, REVERSE_DEF, APPEND, MAP, LENGTH] THEN 840 SIMP_TAC finmap_ss [read_thm] THEN 841 CONV_TAC (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL) 842 THENC RATOR_CONV (RAND_CONV (DEPTH_CONV pairLib.GEN_BETA_CONV 843 THENC REWRITE_CONV [read_thm, write_thm, pair_case_def] 844 THENC reduceLib.REDUCE_CONV)))) THEN 845 SIMP_TAC finmap_ss [write_thm]; 846 847val tac4 = (fn g => 848 ((CONV_TAC (DEPTH_CONV ( 849 REWRITE_CONV [Once mdecode_def] THENC 850 SIMP_CONV finmap_ss [write_thm, read_thm, toEXP_def, toMEM_def, toREG_def, index_of_reg_def])))) 851 g); 852 853val saved_regs_list_thm_1 = Q.store_thm ( 854 "saved_regs_list_thm_1", 855 `!st. locate_ge (read st SP) 12 ==> 856 (run_cfl (BLK (push_list (saved_regs_list))) st = 857 run_cfl (BLK [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]) st)`, 858 859 SIMP_TAC std_ss [FORALL_DSTATE, saved_regs_list_def, push_list_def, push_one_def] THEN 860 RW_TAC std_ss [APPEND, CFL_SEMANTICS_BLK, from_reg_index_thm, fp_def, ip_def, lr_def] THEN 861 NTAC 25 tac4 THEN PUSH_TAC THEN 862 `(1w + 1w = 2w:word32) /\ (2w + 1w = 3w:word32) /\ (3w + 1w = 4w:word32) /\ (4w + 1w = 5w:word32) /\ 863 (5w + 1w = 6w:word32) /\ (6w + 1w = 7w:word32) /\ (7w + 1w = 8w:word32) /\ (8w + 1w = 9w:word32) /\ 864 (9w + 1w = 10w:word32) /\ (10w + 1w = 11w:word32) /\ (11w + 1w = 12w:word32)` by WORDS_TAC THEN 865 RW_TAC std_ss [GSYM WORD_SUB_PLUS, WORD_ADD_ASSOC] THEN 866 IMP_RES_TAC locate_ge_lem_3 THEN 867 FULL_SIMP_TAC arith_ss [SP_def, read_thm] 868 ); 869 870val push_list_append = Q.store_thm ( 871 "push_list_append", 872 `!l1 l2. push_list (l1 ++ l2) = push_list l2 ++ push_list l1`, 873 Induct_on `l1` THEN RW_TAC list_ss [push_list_def] 874 ); 875 876val saved_regs_list_thm_2 = Q.store_thm ( 877 "saved_regs_list_thm_2", 878 `!st l m. locate_ge (read st SP) (k + 12 + LENGTH l) /\ EVERY (\x.valid_MEXP_1 x m) l ==> 879 (run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: push_list (saved_regs_list ++ l))) st = 880 run_cfl (BLK ((MSUB R13 R13 (MC (n2w k))) :: (APPEND (push_list l) [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st)`, 881 882 RW_TAC std_ss [GSYM APPEND, push_list_append, RUN_CFL_BLK_APPEND] THEN 883 `locate_ge (read st SP) (k + LENGTH l)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 884 Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R13 (MC (n2w k))::push_list l)) st` THEN 885 `w2n (read st1 SP) = w2n (read st SP) - (k + LENGTH l)` by (Q.UNABBREV_TAC `st1` THEN 886 METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_1]) THEN 887 `locate_ge (read st1 SP) 12` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 888 RW_TAC std_ss [saved_regs_list_thm_1] 889 ); 890 891val pre_call_2_def = Define ` 892 pre_call_2 (caller_i, callee_i) k n = 893 (MSUB R13 R13 (MC (n2w k))) :: 894 push_list caller_i ++ 895 [MPUSH 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ 896 [MADD R13 R13 (MC 12w)] ++ 897 mov_pointers ++ 898 pop_list callee_i ++ 899 [MSUB R13 R11 (MC (n2w (12 + n)))] 900 `; 901 902 903val saved_regs_list_thm_3 = Q.store_thm ( 904 "saved_regs_list_thm_3", 905 `!st l k m1 m2. locate_ge (read st SP) (k + 12 + LENGTH caller_i) /\ EVERY (\x.valid_TEXP x m1) caller_i ==> 906 (run_cfl (BLK (pre_call (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st = 907 run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st)`, 908 909 RW_TAC std_ss [pre_call_def, pre_call_2_def] THEN 910 IMP_RES_TAC VALID_TEXP_MEXP_1 THEN 911 `MSUB R13 R13 (MC (n2w k)):: push_list (saved_regs_list ++ MAP conv_exp caller_i) ++ [MADD R13 R13 (MC 12w)] ++ 912 mov_pointers ++ pop_list (MAP conv_exp callee_i) ++ [MSUB R13 R11 (MC (n2w (12 + m2)))] = 913 MSUB R13 R13 (MC (n2w k)):: push_list (saved_regs_list ++ MAP conv_exp caller_i) ++ ([MADD R13 R13 (MC 12w)] ++ 914 mov_pointers ++ pop_list (MAP conv_exp callee_i) ++ [MSUB R13 R11 (MC (n2w (12 + m2)))])` by RW_TAC list_ss [] THEN 915 `MSUB R13 R13 (MC (n2w k))::push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ 916 [MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i) ++ [MSUB R13 R11 (MC (n2w (12 + m2)))] = 917 MSUB R13 R13 (MC (n2w k))::(push_list (MAP conv_exp caller_i) ++ [MPUSH 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]]) 918 ++ ([MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i) ++ [MSUB R13 R11 919 (MC (n2w (12 + m2)))])` by RW_TAC list_ss [] THEN 920 RW_TAC bool_ss [] THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 921 `locate_ge (read st SP) (k + 12 + LENGTH (MAP conv_exp caller_i))` by METIS_TAC [LENGTH_MAP] THEN 922 METIS_TAC [RUN_CFL_BLK_APPEND, saved_regs_list_thm_2] 923 ); 924 925(*---------------------------------------------------------------------------------*) 926(* Main theorems about pre-call processing *) 927(*---------------------------------------------------------------------------------*) 928 929val PRE_CALL_SANITY_THM = Q.store_thm ( 930 "PRE_CALL_SANITY_THM", 931 ` locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 932 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 933 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 934 ==> 935 let st' = run_cfl (BLK (pre_call (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st in 936 (!i. i > w2n (read st SP) ==> (st '' (isM i) = st' '' (isM i))) /\ 937 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 938 (w2n (read st' IP) = w2n (read st' FP) + 1) /\ 939 (w2n (read st' SP) = w2n (read st' FP) - (12 + m2))`, 940 941 REPEAT GEN_TAC THEN STRIP_TAC THEN 942 SIMP_TAC std_ss [pre_call_def, Once RUN_CFL_BLK_APPEND] THEN 943 Q.ABBREV_TAC `st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k)):: push_list (saved_regs_list ++ MAP conv_exp caller_i) 944 ++ [MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i))) st` THEN 945 `(!i. i > w2n (read st SP) ==> (st '' isM i = st' '' isM i)) /\ 946 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 947 (w2n (read st' IP) = w2n (read st' FP) + 1)` by ( 948 Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_3, APPEND_ASSOC]) THEN 949 `locate_ge (read st' FP) (12 + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 950 RW_TAC std_ss [LET_THM, SIMP_RULE std_ss [LET_THM] sub_sp_lem_1] 951 ); 952 953val PRE_CALL_SAVED_REGS_THM = Q.store_thm ( 954 "PRE_CALL_SAVED_REGS_THM", 955 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 956 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 957 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 958 ==> 959 let st' = run_cfl (BLK (pre_call (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st in 960 !i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))`, 961 962 REPEAT GEN_TAC THEN STRIP_TAC THEN 963 SIMP_TAC std_ss [pre_call_def, Once RUN_CFL_BLK_APPEND] THEN 964 Q.ABBREV_TAC `st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k)):: push_list (saved_regs_list ++ MAP conv_exp caller_i) 965 ++ [MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i))) st` THEN 966 `!i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))` by ( 967 Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SAVED_REGS_LEM, APPEND_ASSOC]) THEN 968 `(w2n (read st SP) - (k + LENGTH callee_i) - 1 = w2n (read st' FP))` by ( 969 Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_3, APPEND_ASSOC]) THEN 970 `locate_ge (read st' FP) (12 + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 971 RW_TAC std_ss [LET_THM, SIMP_RULE std_ss [LET_THM] sub_sp_lem_1] 972 ); 973 974 975val PRE_CALL_PASS_ARGUMENTS_THM = Q.store_thm ( 976 "PRE_CALL_PASS_ARGUMENTS_THM", 977 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 978 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 979 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 980 ==> 981 !i. i < LENGTH caller_i ==> 982 ((run_cfl (BLK (pre_call (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) '' 983 (EL i (MAP conv_exp callee_i)) = st '' (EL i (MAP conv_exp caller_i)))`, 984 985 REPEAT GEN_TAC THEN STRIP_TAC THEN 986 SIMP_TAC std_ss [pre_call_def, Once RUN_CFL_BLK_APPEND] THEN 987 Q.ABBREV_TAC `st' = run_cfl (BLK (MSUB R13 R13 (MC (n2w k)):: push_list (saved_regs_list ++ MAP conv_exp caller_i) 988 ++ [MADD R13 R13 (MC 12w)] ++ mov_pointers ++ pop_list (MAP conv_exp callee_i))) st` THEN 989 `!i. i < LENGTH caller_i ==> (st' '' (EL i (MAP conv_exp callee_i)) = st '' (EL i (MAP conv_exp caller_i)))` by ( 990 Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_PASS_ARGUMENTS_LEM, APPEND_ASSOC]) THEN 991 `(w2n (read st SP) - (k + LENGTH callee_i) - 1 = w2n (read st' FP))` by ( 992 Q.UNABBREV_TAC `st'` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_3, APPEND_ASSOC]) THEN 993 `locate_ge (read st' FP) (12 + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 994 RW_TAC std_ss [LET_THM, SIMP_RULE std_ss [LET_THM] sub_sp_lem_1] 995 ); 996 997(*---------------------------------------------------------------------------------*) 998(* Main theorems about pre-call processing *) 999(* After the optimization on register saving *) 1000(*---------------------------------------------------------------------------------*) 1001 1002val PRE_CALL_SANITY_THM_2 = Q.store_thm ( 1003 "PRE_CALL_SANITY_THM_2", 1004 ` locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 1005 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 1006 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 1007 ==> 1008 let st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st in 1009 (!i. i > w2n (read st SP) ==> (st '' (isM i) = st' '' (isM i))) /\ 1010 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 1011 (w2n (read st' IP) = w2n (read st' FP) + 1) /\ 1012 (w2n (read st' SP) = w2n (read st' FP) - (12 + m2))`, 1013 1014 REPEAT GEN_TAC THEN STRIP_TAC THEN 1015 `locate_ge (read st SP) (k + 12 + LENGTH caller_i)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1016 METIS_TAC [saved_regs_list_thm_3, PRE_CALL_SANITY_THM] 1017 ); 1018 1019val PRE_CALL_SAVED_REGS_THM_2 = Q.store_thm ( 1020 "PRE_CALL_SAVED_REGS_THM_2", 1021 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 1022 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 1023 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 1024 ==> 1025 let st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st in 1026 !i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))`, 1027 1028 REPEAT GEN_TAC THEN STRIP_TAC THEN 1029 `locate_ge (read st SP) (k + 12 + LENGTH caller_i)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1030 METIS_TAC [saved_regs_list_thm_3, PRE_CALL_SAVED_REGS_THM] 1031 ); 1032 1033val PRE_CALL_PASS_ARGUMENTS_THM_2 = Q.store_thm ( 1034 "PRE_CALL_PASS_ARGUMENTS_THM_2", 1035 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 1036 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 1037 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 1038 ==> 1039 !i. i < LENGTH caller_i ==> 1040 ((run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) '' 1041 (EL i (MAP conv_exp callee_i)) = st '' (EL i (MAP conv_exp caller_i)))`, 1042 1043 REPEAT GEN_TAC THEN STRIP_TAC THEN 1044 `locate_ge (read st SP) (k + 12 + LENGTH caller_i)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1045 METIS_TAC [saved_regs_list_thm_3, PRE_CALL_PASS_ARGUMENTS_THM] 1046 ); 1047 1048(*---------------------------------------------------------------------------------*) 1049 1050(*---------------------------------------------------------------------------------*) 1051(* Post-call processing *) 1052(*---------------------------------------------------------------------------------*) 1053 1054val post_call_def = Define ` 1055 post_call (caller_o, callee_o) n = 1056 (MADD R13 R12 (MC (n2w (LENGTH callee_o)))) :: (* add sp ip #callee_o *) 1057 push_list callee_o ++ 1058 [MSUB R13 R11 (MC 11w)] ++ (* sub sp fp 12 *) 1059 [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ 1060 pop_list caller_o ++ 1061 [MSUB R13 R11 (MC (n2w (12 + n)))] 1062 `; 1063 1064(*---------------------------------------------------------------------------------*) 1065(* The callee pushed results into the stack *) 1066(*---------------------------------------------------------------------------------*) 1067 1068val LEGAL_PUSH_EXP_LEM_2 = Q.store_thm ( 1069 "LEGAL_PUSH_EXP_LEM_2", 1070 `!st l m. w2n (read st FP) + LENGTH l < w2n (read st SP) /\ EVERY (\x.valid_MEXP x m) l 1071 ==> 1072 (!i. i < LENGTH l ==> legal_push_exp st (EL i l) (PRE (LENGTH l) - i))`, 1073 1074 RW_TAC std_ss [legal_push_exp_def] THENL [ 1075 FULL_SIMP_TAC std_ss [EVERY_EL] THEN RES_TAC THEN 1076 Cases_on `EL i l` THEN 1077 FULL_SIMP_TAC std_ss [conv_exp_def, addr_in_range_def, in_range_def, addr_of_def, valid_MEXP_def, 1078 valid_regs_lem, within_bound_def] THEN 1079 `w2n (read st FP) <= n + w2n (read st SP)` by RW_TAC arith_ss [] THEN 1080 RW_TAC std_ss [] THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1081 Cases_on `w2n (read st SP) < PRE (LENGTH l) - i + (w2n (read st FP) - n)` THEN 1082 `PRE (LENGTH l) - i < LENGTH l /\ (w2n (read st FP) - n <= w2n (read st SP))` by RW_TAC arith_ss [] THEN 1083 RW_TAC arith_ss [LESS_MONO_ADD_EQ], 1084 1085 IMP_RES_TAC VALID_MEXP_exp THEN 1086 METIS_TAC [EVERY_EL, valid_exp_thm] 1087 ] 1088 ); 1089 1090 1091val POST_CALL_PUSH_RESULTS = Q.store_thm ( 1092 "POST_CALL_PUSH_RESULTS", 1093 `!st l m k. grow_lt (read st IP) (LENGTH l) /\ EVERY (\x.valid_MEXP x m) l /\ 1094 (w2n (read st IP) = w2n (read st FP) + 1) ==> 1095 !i. i < LENGTH l ==> 1096 ((run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH l))) :: push_list l)) st) '' 1097 (isM (w2n (read st FP) + 1 + SUC i)) = st '' (EL i l))`, 1098 1099 SIMP_TAC std_ss [FORALL_DSTATE] THEN 1100 RW_TAC std_ss [CFL_SEMANTICS_BLK] THEN 1101 tac1 THEN 1102 FULL_SIMP_TAC std_ss [read_thm, SP_def] THEN 1103 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 12 + n2w (LENGTH l)),mem)` THEN 1104 `locate_ge (read st1 SP) (LENGTH l) /\ w2n (read st1 FP) + LENGTH l < w2n (read st1 SP) /\ 1105 (w2n (read st1 SP) = w2n (read (regs,mem) IP) + LENGTH l)` by (Q.UNABBREV_TAC `st1` THEN 1106 IMP_RES_TAC grow_lt_lem_1 THEN 1107 FULL_SIMP_TAC finmap_ss [read_thm, locate_ge_def, SP_def, FP_def, IP_def, grow_lt_def]) THEN 1108 1109 `legal_push_exp st1 (EL i l) (PRE (LENGTH l) - i)` by METIS_TAC [LEGAL_PUSH_EXP_LEM_2] THEN 1110 IMP_RES_TAC VALID_MEXP_MEXP_1 THEN 1111 IMP_RES_TAC VALID_MEXP_1_exp_3 THEN 1112 IMP_RES_TAC PUSH_LIST_FUNCTIONALITY THEN 1113 `w2n (read st1 SP) - PRE (LENGTH l) + i = w2n (read (regs,mem) FP) + 1 + SUC i` by 1114 FULL_SIMP_TAC arith_ss [PRE_SUB1, locate_ge_def] THEN 1115 FULL_SIMP_TAC std_ss [EVERY_EL] THEN RES_TAC THEN 1116 Q.UNABBREV_TAC `st1` THEN 1117 Cases_on `EL i l` THEN 1118 FULL_SIMP_TAC finmap_ss [reade_def, read_thm, fp_def, valid_exp_3_def, valid_MEXP_1_def, valid_exp_1_def] 1119 ); 1120 1121val below_lem_1 = Q.store_thm ( 1122 "below_lem_1", 1123 `!st n. i <= w2n (read st SP) - n 1124 ==> ~addr_in_range st (isM i) (w2n (read st SP),w2n (read st SP) - n)`, 1125 RW_TAC arith_ss [addr_in_range_def, in_range_def, addr_of_def] 1126 ); 1127 1128val POST_CALL_SANITY_1 = Q.store_thm ( 1129 "POST_CALL_SANITY_1", 1130 `!st l m k. grow_lt (read st IP) (LENGTH l) /\ EVERY (\x.valid_MEXP x m) l /\ 1131 (w2n (read st IP) = w2n (read st FP) + 1) 1132 ==> 1133 let st' = run_cfl (BLK ((MADD R13 R12 (MC (n2w (LENGTH l)))) :: push_list l)) st in 1134 (!i. (i > w2n (read st IP) + LENGTH l \/ i <= w2n (read st IP)) ==> (st '' (isM i) = st' '' (isM i))) /\ 1135 (w2n (read st' IP) = w2n (read st IP)) /\ (w2n (read st' FP) = w2n (read st FP)) /\ 1136 (w2n (read st' SP) = w2n (read st IP))`, 1137 1138 SIMP_TAC std_ss [FORALL_DSTATE] THEN 1139 SIMP_TAC std_ss [CFL_SEMANTICS_BLK] THEN 1140 tac1 THEN 1141 FULL_SIMP_TAC std_ss [read_thm, SP_def] THEN 1142 REPEAT GEN_TAC THEN STRIP_TAC THEN 1143 Q.ABBREV_TAC `st1 = (regs |+ (13,regs ' 12 + n2w (LENGTH l)),mem)` THEN 1144 `locate_ge (read st1 SP) (LENGTH l) /\ w2n (read st1 FP) + LENGTH l < w2n (read st1 SP) /\ 1145 (w2n (read st1 SP) = w2n (read (regs,mem) IP) + LENGTH l)` by (Q.UNABBREV_TAC `st1` THEN 1146 IMP_RES_TAC grow_lt_lem_1 THEN 1147 FULL_SIMP_TAC finmap_ss [read_thm, locate_ge_def, SP_def, FP_def, IP_def, grow_lt_def]) THEN 1148 RW_TAC std_ss [LET_THM] THENL [ 1149 1150 `i > w2n (read st1 SP)` by RW_TAC arith_ss [] THEN 1151 IMP_RES_TAC above_lem_1 THEN 1152 POP_ASSUM (ASSUME_TAC o Q.SPEC `LENGTH (l:CFL_EXP list)`) THEN 1153 FULL_SIMP_TAC std_ss [] THEN 1154 `valid_exp_1 (isM i)` by RW_TAC std_ss [valid_exp_1_def] THEN 1155 IMP_RES_TAC VALID_MEXP_MEXP_1 THEN 1156 IMP_RES_TAC VALID_MEXP_1_exp_3 THEN 1157 RW_TAC std_ss [PUSH_LIST_SANITY] THEN 1158 Q.UNABBREV_TAC `st1` THEN 1159 FULL_SIMP_TAC finmap_ss [reade_def], 1160 1161 `i <= w2n (read st1 SP) - LENGTH (l:CFL_EXP list)` by RW_TAC arith_ss [] THEN 1162 IMP_RES_TAC below_lem_1 THEN 1163 `valid_exp_1 (isM i)` by RW_TAC std_ss [valid_exp_1_def] THEN 1164 IMP_RES_TAC VALID_MEXP_MEXP_1 THEN 1165 IMP_RES_TAC VALID_MEXP_1_exp_3 THEN 1166 RW_TAC std_ss [PUSH_LIST_SANITY] THEN 1167 Q.UNABBREV_TAC `st1` THEN 1168 FULL_SIMP_TAC finmap_ss [reade_def], 1169 1170 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 1171 Q.UNABBREV_TAC `st1` THEN 1172 FULL_SIMP_TAC finmap_ss [IP_def, FP_def, read_thm], 1173 1174 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 1175 Q.UNABBREV_TAC `st1` THEN 1176 FULL_SIMP_TAC finmap_ss [IP_def, FP_def, read_thm], 1177 1178 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] PUSH_LIST_SP_FP) THEN 1179 Q.UNABBREV_TAC `st1` THEN 1180 FULL_SIMP_TAC finmap_ss [SP_def, FP_def, read_thm] 1181 ] 1182 ); 1183 1184(*---------------------------------------------------------------------------------*) 1185(* Registers saved in the stack are restored *) 1186(*---------------------------------------------------------------------------------*) 1187 1188val POP_TAC = 1189 CONV_TAC (DEPTH_CONV (REWRITE_CONV [Once mdecode_def, popL_def])) THEN 1190 REWRITE_TAC [MAP, LENGTH] THEN 1191 SIMP_TAC finmap_ss [read_thm] THEN 1192 CONV_TAC (DEPTH_CONV ((REWR_CONV FOLDL_CONS ORELSEC REWR_CONV FOLDL_NIL) 1193 THENC RATOR_CONV (RAND_CONV (DEPTH_CONV pairLib.GEN_BETA_CONV 1194 THENC REWRITE_CONV [read_thm, write_thm, pair_case_def] 1195 THENC reduceLib.REDUCE_CONV)))) THEN 1196 SIMP_TAC finmap_ss [write_thm]; 1197 1198 1199val EVAL_POP_SAVED_REGS_LIST = Q.store_thm ( 1200 "EVAL_POP_SAVED_REGS_LIST", 1201 1202 `!regs mem. locate_ge (read (regs,mem) FP) 11 ==> 1203 (run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) (regs,mem) = 1204 (regs |+ (0,mem ' (w2n (regs ' 11) - 10)) |+ 1205 (1,mem ' (w2n (regs ' 11) - 9)) |+ (2,mem ' (w2n (regs ' 11) - 8)) |+ 1206 (3,mem ' (w2n (regs ' 11) - 7)) |+ (4,mem ' (w2n (regs ' 11) - 6)) |+ 1207 (5,mem ' (w2n (regs ' 11) - 5)) |+ (6,mem ' (w2n (regs ' 11) - 4)) |+ 1208 (7,mem ' (w2n (regs ' 11) - 3)) |+ (8,mem ' (w2n (regs ' 11) - 2)) |+ 1209 (11,mem ' (w2n (regs ' 11) - 1)) |+ (12,mem ' (w2n (regs ' 11))) |+ 1210 (13,regs ' 11 + 1w) |+ (14,mem ' (w2n (regs ' 11) + 1)),mem))`, 1211 1212 RW_TAC std_ss [APPEND, CFL_SEMANTICS_BLK, from_reg_index_thm, fp_def, ip_def, lr_def] THEN 1213 NTAC 2 tac4 THEN POP_TAC THEN 1214 IMP_RES_TAC locate_ge_lem_1 THEN 1215 `grow_lt (read (regs,mem) FP - 11w) 11` by ( 1216 IMP_RES_TAC LOCATE_GE_GROW_LT THEN `w2n (11w:word32) = 11` by WORDS_TAC THEN 1217 FULL_SIMP_TAC std_ss [locate_ge_def]) THEN 1218 IMP_RES_TAC grow_lt_lem_2 THEN 1219 FULL_SIMP_TAC std_ss [FP_def, read_thm] THEN 1220 Q.ABBREV_TAC `x = regs ' 11 - 11w` THEN 1221 WORDS_TAC THEN Q.UNABBREV_TAC `x` THEN 1222 RW_TAC arith_ss [GSYM WORD_ADD_SUB_SYM, WORD_ADD_SUB_ASSOC] THEN 1223 `w2n (11w:word32) <= 11` by WORDS_TAC THEN 1224 RW_TAC std_ss [] THEN WORDS_TAC THEN 1225 FULL_SIMP_TAC arith_ss [locate_ge_def] 1226 ); 1227 1228val EVAL_POP_SAVED_REGS_LIST_2 = Q.store_thm ( 1229 "EVAL_POP_SAVED_REGS_LIST_2", 1230 1231 `!regs mem. locate_ge (read (regs,mem) FP) 11 ==> 1232 (run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ pop_list saved_regs_list)) (regs,mem) = 1233 (regs |+ (0,mem ' (w2n (regs ' 11) - 10)) |+ 1234 (1,mem ' (w2n (regs ' 11) - 9)) |+ (2,mem ' (w2n (regs ' 11) - 8)) |+ 1235 (3,mem ' (w2n (regs ' 11) - 7)) |+ (4,mem ' (w2n (regs ' 11) - 6)) |+ 1236 (5,mem ' (w2n (regs ' 11) - 5)) |+ (6,mem ' (w2n (regs ' 11) - 4)) |+ 1237 (7,mem ' (w2n (regs ' 11) - 3)) |+ (8,mem ' (w2n (regs ' 11) - 2)) |+ 1238 (11,mem ' (w2n (regs ' 11) - 1)) |+ (12,mem ' (w2n (regs ' 11))) |+ 1239 (13,regs ' 11 + 1w) |+ (14,mem ' (w2n (regs ' 11) + 1)),mem))`, 1240 1241 SIMP_TAC std_ss [FORALL_DSTATE, saved_regs_list_def, pop_list_def, pop_one_def] THEN 1242 RW_TAC std_ss [APPEND, CFL_SEMANTICS_BLK, from_reg_index_thm, fp_def, ip_def, lr_def] THEN 1243 NTAC 25 tac4 THEN 1244 RW_TAC std_ss [GSYM WORD_ADD_ASSOC] THEN 1245 1246 IMP_RES_TAC locate_ge_lem_1 THEN 1247 `grow_lt (read (regs,mem) FP - 11w) 11` by ( 1248 IMP_RES_TAC LOCATE_GE_GROW_LT THEN `w2n (11w:word32) = 11` by WORDS_TAC THEN 1249 FULL_SIMP_TAC std_ss [locate_ge_def]) THEN 1250 IMP_RES_TAC grow_lt_lem_2 THEN 1251 FULL_SIMP_TAC std_ss [FP_def, read_thm] THEN 1252 Q.ABBREV_TAC `x = regs ' 11 - 11w` THEN 1253 WORDS_TAC THEN Q.UNABBREV_TAC `x` THEN 1254 RW_TAC arith_ss [GSYM WORD_ADD_SUB_SYM, WORD_ADD_SUB_ASSOC] THEN 1255 `w2n (11w:word32) <= 11` by WORDS_TAC THEN 1256 RW_TAC std_ss [] THEN WORDS_TAC THEN 1257 FULL_SIMP_TAC arith_ss [locate_ge_def] 1258 ); 1259 1260val POP_SAVED_REGS_LIST_SANITY_1 = Q.store_thm ( 1261 "POP_SAVED_REGS_LIST_SANITY_1", 1262 `!st. locate_ge (read st FP) 11 /\ grow_lt (read st FP) 1 ==> 1263 let st' = run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st in 1264 (!i. st' '' (isM i) = st '' (isM i)) /\ 1265 (w2n (read st' IP) = w2n (st '' (isM (w2n (read st FP))))) /\ 1266 (w2n (read st' FP) = w2n (st '' (isM (w2n (read st FP) - 1)))) /\ 1267 (w2n (read st' SP) = w2n (read st FP) + 1) /\ 1268 (w2n (read st' SP) = w2n (read st FP + 1w))`, 1269 1270 SIMP_TAC std_ss [FORALL_DSTATE] THEN 1271 REPEAT GEN_TAC THEN STRIP_TAC THEN 1272 IMP_RES_TAC EVAL_POP_SAVED_REGS_LIST THEN 1273 IMP_RES_TAC grow_lt_lem_2 THEN 1274 FULL_SIMP_TAC std_ss [FP_def, read_thm] THEN 1275 RW_TAC finmap_ss [LET_THM, reade_def, read_thm, FP_def, IP_def, SP_def] 1276 ); 1277 1278(*---------------------------------------------------------------------------------*) 1279(* The caller pops the results out of the stack *) 1280(*---------------------------------------------------------------------------------*) 1281 1282val LEGAL_POP_EXP_LEM_2 = Q.store_thm ( 1283 "LEGAL_POP_EXP_LEM_2", 1284 `!st l m. w2n (read st SP) + LENGTH (MAP conv_exp l) + (12 + m) <= w2n (read st FP) /\ EVERY (\x.valid_TEXP x m) l 1285 ==> 1286 EVERY (\x.~addr_in_range st x (w2n (read st SP) + LENGTH (MAP conv_exp l), w2n (read st SP))) (MAP conv_exp l)`, 1287 1288 REPEAT STRIP_TAC THEN 1289 IMP_RES_TAC VALID_EXP_LEM THEN 1290 FULL_SIMP_TAC list_ss [EVERY_EL, rich_listTheory.EL_MAP] THEN 1291 RW_TAC std_ss [] THEN RES_TAC THEN 1292 Cases_on `EL n l` THEN 1293 FULL_SIMP_TAC std_ss [conv_exp_def, addr_in_range_def, in_range_def, addr_of_def, valid_exp_def, valid_TEXP_def, 1294 valid_regs_lem, within_bound_def] THEN 1295 RW_TAC arith_ss [] 1296 ); 1297 1298val POST_CALL_POP_RESULTS = Q.store_thm ( 1299 "POST_CALL_POP_RESULTS", 1300 `!st l m. locate_ge (read st FP + 1w) 12 /\ 1301 w2n (read st FP) + 1 + LENGTH l + (12 + m) <= w2n (st '' (isM (w2n (read st FP) - 1))) /\ 1302 EVERY notC l /\ unique_list l /\ EVERY (\x.valid_TEXP x m) l /\ (MAP conv_exp l = l') 1303 ==> 1304 !i. i < LENGTH l' ==> 1305 ((run_cfl (BLK ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l')) st) '' 1306 (EL i l') = st '' (isM ((w2n (read st FP) + 1) + SUC i)))`, 1307 1308 RW_TAC std_ss [APPEND, Once RUN_CFL_BLK_APPEND] THEN 1309 Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN 1310 `locate_ge (read st FP) 11 /\ grow_lt (read st FP) 1` by ( 1311 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1312 `grow_lt (read st FP) 1` by FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def] THEN 1313 IMP_RES_TAC grow_lt_lem_1 THEN FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def]) THEN 1314 1315 `(!i. st '' (isM i) = st1 '' (isM i)) /\ (w2n (st '' (isM (w2n (read st FP) - 1))) = w2n (read st1 FP)) /\ 1316 (w2n (read st FP) + 1 = w2n (read st1 SP)) /\ (read st FP + 1w = read st1 SP)` 1317 by (Q.UNABBREV_TAC `st1` THEN 1318 METIS_TAC [rich_listTheory.CONS_APPEND, SIMP_RULE std_ss [LET_THM] POP_SAVED_REGS_LIST_SANITY_1, w2n_11]) THEN 1319 FULL_SIMP_TAC std_ss [] THEN NTAC 7 (POP_ASSUM (K ALL_TAC)) THEN 1320 1321 `grow_lt (read st1 SP) (LENGTH (MAP conv_exp l)) /\ locate_ge (read st1 FP) (12 + m)` by (`w2n (read st1 FP) 1322 < dimword (:32)` by METIS_TAC [w2n_lt] THEN RW_TAC arith_ss [grow_lt_def, locate_ge_def, LENGTH_MAP]) THEN 1323 `w2n (read st1 SP) + LENGTH (MAP conv_exp l) + (12 + m) <= w2n (read st1 FP)` by METIS_TAC [LENGTH_MAP] THEN 1324 1325 IMP_RES_TAC UNIQUE_LIST_11 THEN 1326 IMP_RES_TAC LEGAL_POP_EXP_LEM_2 THEN 1327 IMP_RES_TAC VALID_TEXP_MEXP THEN 1328 IMP_RES_TAC VALID_MEXP_exp THEN 1329 IMP_RES_TAC LEGAL_POP_EXP_LEM_2 THEN 1330 `i < LENGTH l` by METIS_TAC [LENGTH_MAP] THEN 1331 IMP_RES_TAC notC_LEM THEN 1332 IMP_RES_TAC POP_LIST_FUNCTIONALITY THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1333 FULL_SIMP_TAC std_ss [EVERY_EL] 1334 ); 1335 1336val word_add_lem_1 = Q.store_thm ( 1337 "word_add_lem_1", 1338 `!x y k. (w2n x = w2n y + k) ==> (x:word32 = y + n2w k)`, 1339 METIS_TAC [word_add_n2w, n2w_w2n] 1340 ); 1341 1342val POST_CALL_PASS_RESULTS_LEM = Q.store_thm ( 1343 "POST_CALL_PASS_RESULTS_LEM", 1344 1345 `!st l m1 m2 k. (w2n (read st IP) = w2n (read st FP) + 1) /\ locate_ge (read st IP) 12 /\ 1346 w2n (read st IP) + LENGTH caller_o + (12 + m1) <= w2n (st '' isM (w2n (read st FP) - 1)) /\ 1347 EVERY (\x. valid_TEXP x m2) callee_o /\ 1348 EVERY notC caller_o /\ unique_list caller_o /\ EVERY (\x.valid_TEXP x m1) caller_o /\ 1349 (LENGTH callee_o = LENGTH caller_o) 1350 ==> 1351 !i. i < LENGTH caller_o ==> 1352 ((run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))) :: push_list (MAP conv_exp callee_o) 1353 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ 1354 pop_list (MAP conv_exp caller_o)))) st) '' (EL i (MAP conv_exp caller_o)) = 1355 st '' (EL i (MAP conv_exp callee_o)))`, 1356 1357 RW_TAC bool_ss [] THEN 1358 REWRITE_TAC [Once RUN_CFL_BLK_APPEND] THEN 1359 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1360 push_list (MAP conv_exp callee_o))) st` THEN 1361 `grow_lt (read st IP) (LENGTH (MAP conv_exp callee_o))` by ( 1362 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1363 FULL_SIMP_TAC arith_ss [LENGTH_MAP, grow_lt_def]) THEN 1364 IMP_RES_TAC VALID_TEXP_MEXP THEN 1365 1366 `locate_ge (read st1 FP + 1w) 12 /\ (w2n (read st1 FP) = w2n (read st FP)) /\ 1367 w2n (read st1 FP) + 1 + LENGTH caller_o + (12 + m1) <= w2n (st1 '' (isM (w2n (read st1 FP) - 1)))` by ( 1368 `w2n (read st FP) - 1 <= w2n (read st IP)` by RW_TAC arith_ss [] THEN 1369 `(w2n (read st1 IP) = w2n (read st IP)) /\ (w2n (read st1 FP) = w2n (read st FP)) /\ 1370 (st1 '' (isM (w2n (read st FP) - 1)) = st '' (isM (w2n (read st FP) - 1)))` by 1371 (Q.UNABBREV_TAC `st1` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_1]) THEN 1372 IMP_RES_TAC word_add_lem_1 THEN METIS_TAC [w2n_11]) THEN 1373 1374 IMP_RES_TAC POST_CALL_POP_RESULTS THEN NTAC 32 (POP_ASSUM (K ALL_TAC)) THEN 1375 `i < LENGTH (MAP conv_exp caller_o)` by METIS_TAC [LENGTH_MAP] THEN 1376 FULL_SIMP_TAC std_ss [] THEN NTAC 5 (POP_ASSUM (K ALL_TAC)) THEN 1377 Q.UNABBREV_TAC `st1` THEN 1378 METIS_TAC [POST_CALL_PUSH_RESULTS, LENGTH_MAP] 1379 ); 1380 1381(*---------------------------------------------------------------------------------*) 1382(* Status after the caller restores pops results out *) 1383(*---------------------------------------------------------------------------------*) 1384 1385val eq_exp_lem_1 = Q.store_thm ( 1386 "eq_exp_lem_1", 1387 `!e l st m. ~(MEM e l) /\ valid_TEXP e m /\ locate_ge (read st FP) (12 + m) /\ EVERY (\x.valid_TEXP x m) l ==> 1388 EVERY (\x. ~eq_exp st (conv_exp e) x) (MAP conv_exp l)`, 1389 1390 RW_TAC std_ss [EVERY_EL, LENGTH_MAP, rich_listTheory.EL_MAP, MEM_EL] THEN 1391 REPEAT (Q.PAT_ASSUM `!n.k` (ASSUME_TAC o Q.SPEC `n`)) THEN RW_TAC std_ss [] THEN 1392 Cases_on `EL n l` THEN Cases_on `e` THEN 1393 FULL_SIMP_TAC std_ss [conv_exp_def, eq_exp_def, eq_addr_def, addr_of_def, valid_exp_def, 1394 valid_TEXP_def, within_bound_def, locate_ge_def] THENL [ 1395 Cases_on `T''` THEN Cases_on `T'` THEN RW_TAC std_ss [data_reg_index_def], 1396 RW_TAC std_ss [], 1397 RES_TAC THEN STRIP_TAC THEN 1398 `n'' + 12 <= w2n (read st FP) /\ n' + 12 <= w2n (read st FP)` by RW_TAC arith_ss [] THEN 1399 FULL_SIMP_TAC arith_ss [SUB_CANCEL] 1400 ] 1401 ); 1402 1403val tac5 = 1404 Q.ABBREV_TAC `st1 = run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st` THEN 1405 `locate_ge (read st FP) 11 /\ grow_lt (read st FP) 1` by ( 1406 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1407 `grow_lt (read st FP) 1` by FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def] THEN 1408 IMP_RES_TAC grow_lt_lem_1 THEN FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def]) THEN 1409 `(!i. st '' (isM i) = st1 '' (isM i)) /\ (w2n (st '' (isM (w2n (read st FP) - 1))) = w2n (read st1 FP)) /\ 1410 (w2n (read st FP) + 1 = w2n (read st1 SP)) /\ (read st FP + 1w = read st1 SP)` 1411 by (Q.UNABBREV_TAC `st1` THEN 1412 METIS_TAC [rich_listTheory.CONS_APPEND, SIMP_RULE std_ss [LET_THM] POP_SAVED_REGS_LIST_SANITY_1, w2n_11]) THEN 1413 FULL_SIMP_TAC std_ss [] THEN 1414 `grow_lt (read st1 SP) (LENGTH (MAP conv_exp l)) /\ locate_ge (read st1 FP) (12 + m)` by (`w2n (read st1 FP) 1415 < dimword (:32)` by METIS_TAC [w2n_lt] THEN RW_TAC arith_ss [grow_lt_def, locate_ge_def, LENGTH_MAP]) THEN 1416 `w2n (read st1 SP) + LENGTH (MAP conv_exp l) + (12 + m) <= w2n (read st1 FP)` by METIS_TAC [LENGTH_MAP] 1417 ; 1418 1419val VALID_TEXP_MEXP_SINGLE = Q.store_thm ( 1420 "VALID_TEXP_MEXP_SINGLE", 1421 `!e m. valid_TEXP e m ==> valid_MEXP (conv_exp e) m`, 1422 Cases_on `e` THEN RW_TAC arith_ss [conv_exp_def,valid_exp_def,valid_MEXP_def,valid_TEXP_def, within_bound_def] THEN 1423 Cases_on `T'` THEN RW_TAC std_ss [valid_exp_1_def, data_reg_index_def, valid_regs_def, 1424 from_reg_index_thm, index_of_reg_def] 1425 ); 1426 1427val VALID_MEXP_exp_SINGLE = Q.store_thm ( 1428 "VALID_MEXP_exp_SINGLE", 1429 `!e m. valid_MEXP e m ==> valid_exp e`, 1430 Cases_on `e` THEN RW_TAC arith_ss [conv_exp_def,valid_exp_def, valid_MEXP_def] 1431 ); 1432 1433val eval_saved_regs_list_lem = Q.store_thm ( 1434 "eval_saved_regs_list_lem", 1435 `!x. locate_ge x 11 /\ (!i. i < 12 ==> (st '' isM (w2n (x:word32) - 10 + i) = st0 '' EL i saved_regs_list)) ==> 1436 (st '' isM (w2n x + 1) = st0 '' isR lr) /\ (st '' isM (w2n x) = st0 '' isR ip) /\ 1437 (st '' isM (w2n x - 1) = st0 '' isR fp) /\ (st '' isM (w2n x - 2) = st0 '' isR 8) /\ 1438 (st '' isM (w2n x - 3) = st0 '' isR 7) /\ (st '' isM (w2n x - 4) = st0 '' isR 6) /\ 1439 (st '' isM (w2n x - 5) = st0 '' isR 5) /\ (st '' isM (w2n x - 6) = st0 '' isR 4) /\ 1440 (st '' isM (w2n x - 7) = st0 '' isR 3) /\ (st '' isM (w2n x - 8) = st0 '' isR 2) /\ 1441 (st '' isM (w2n x - 9) = st0 '' isR 1) /\ (st '' isM (w2n x - 10) = st0 '' isR 0)`, 1442 1443 REPEAT GEN_TAC THEN STRIP_TAC THEN 1444 `0 < 12 /\ 1 < 12 /\ 2 < 12 /\ 3 < 12 /\ 4 < 12 /\ 5 < 12 /\ 6 < 12 /\ 7 < 12 /\ 8 < 12 /\ 9 < 12 /\ 10 < 12 /\ 1445 11 < 12` by RW_TAC arith_ss [] THEN 1446 RES_TAC THEN 1447 FULL_SIMP_TAC list_ss [saved_regs_list_def, locate_ge_def] THEN 1448 `~(w2n (x:word32) <= 10)` by RW_TAC arith_ss [] THEN 1449 FULL_SIMP_TAC arith_ss [SUB_RIGHT_ADD] 1450 ); 1451 1452val POST_CALL_SANITY_2 = Q.store_thm ( 1453 "POST_CALL_SANITY_2", 1454 1455 `!st0 st e l m. 1456 locate_ge (read st FP + 1w) 12 /\ 1457 w2n (read st FP) + 1 + LENGTH l + (12 + m) <= w2n (st '' (isM (w2n (read st FP) - 1))) /\ 1458 (!i. i < 12 ==> (st '' (isM (w2n (read st FP) - 10 + i)) = st0 '' (EL i saved_regs_list))) 1459 ==> 1460 let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]]))) st in 1461 (!i. st' '' isM i = st '' isM i) /\ 1462 (w2n (read st' FP) = w2n (read st0 FP)) /\ (w2n (read st' IP) = w2n (read st0 IP)) /\ 1463 (w2n (read st' SP) = w2n (read st FP) + 1)`, 1464 1465 REPEAT GEN_TAC THEN STRIP_TAC THEN 1466 SIMP_TAC std_ss [APPEND] THEN 1467 `locate_ge (read st FP) 11 /\ grow_lt (read st FP) 1` by ( 1468 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1469 `grow_lt (read st FP) 1` by FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def] THEN 1470 IMP_RES_TAC grow_lt_lem_1 THEN FULL_SIMP_TAC arith_ss [locate_ge_def, grow_lt_def]) THEN 1471 FULL_SIMP_TAC std_ss [LET_THM, SIMP_RULE list_ss [LET_THM] POP_SAVED_REGS_LIST_SANITY_1] THEN 1472 Q.ABBREV_TAC `x = read st FP` THEN 1473 `(st '' isM (w2n x) = st0 '' isR ip) /\ (st '' isM (w2n x - 1) = st0 '' isR fp)` by 1474 METIS_TAC [eval_saved_regs_list_lem] THEN 1475 FULL_SIMP_TAC std_ss [reade_def, read_thm, FP_def, IP_def, fp_def, ip_def] 1476 ); 1477 1478val POST_CALL_SANITY_3 = Q.store_thm ( 1479 "POST_CALL_SANITY_3", 1480 1481 `!st0 st e l m. 1482 locate_ge (read st FP + 1w) 12 /\ 1483 w2n (read st FP) + 1 + LENGTH l + (12 + m) <= w2n (st '' (isM (w2n (read st FP) - 1))) /\ 1484 EVERY notC l /\ unique_list l /\ EVERY (\x.valid_TEXP x m) l /\ (MAP conv_exp l = l') /\ 1485 (!i. i < 12 ==> (st '' (isM (w2n (read st FP) - 10 + i)) = st0 '' (EL i saved_regs_list))) 1486 ==> 1487 let st' = run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st in 1488 (!i. i > w2n (read st0 FP) - 12 ==> (st '' isM i = st' '' isM i)) /\ 1489 (w2n (read st' FP) = w2n (read st0 FP)) /\ (w2n (read st' IP) = w2n (read st0 IP)) /\ 1490 (w2n (read st' SP) = w2n (read st FP) + 1 + LENGTH l)`, 1491 1492 REPEAT GEN_TAC THEN STRIP_TAC THEN 1493 SIMP_TAC std_ss [APPEND, Once RUN_CFL_BLK_APPEND] THEN 1494 IMP_RES_TAC POST_CALL_SANITY_2 THEN 1495 IMP_RES_TAC VALID_TEXP_MEXP THEN IMP_RES_TAC VALID_MEXP_exp THEN 1496 tac5 THEN 1497 Q.PAT_ASSUM ` MAP conv_exp l = l'` (ASSUME_TAC o GSYM) THEN 1498 FULL_SIMP_TAC std_ss [LET_THM] THEN 1499 FULL_SIMP_TAC std_ss [SIMP_RULE std_ss [LET_THM] POP_LIST_SP_FP, LENGTH_MAP] THEN 1500 STRIP_TAC THENL [ 1501 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN REPEAT STRIP_TAC THEN 1502 `valid_exp_2 (isM i)` by METIS_TAC [valid_exp_2_def] THEN 1503 `i > w2n (read st1 FP) - 12` by (Q.UNABBREV_TAC `st1` THEN METIS_TAC [rich_listTheory.CONS_APPEND]) THEN 1504 IMP_RES_TAC above_lem_3 THEN 1505 METIS_TAC [POP_LIST_SANITY, LENGTH_MAP], 1506 1507 NTAC 8 (POP_ASSUM (K ALL_TAC)) THEN 1508 Q.UNABBREV_TAC `st1` THEN 1509 METIS_TAC [rich_listTheory.CONS_APPEND] 1510 ] 1511 ); 1512 1513val POST_CALL_SANITY_4 = Q.store_thm ( 1514 "POST_CALL_SANITY_4", 1515 1516 `!st0 st e l m. 1517 locate_ge (read st FP + 1w) 12 /\ 1518 w2n (read st FP) + 1 + LENGTH l + (12 + m) <= w2n (st '' (isM (w2n (read st FP) - 1))) /\ 1519 valid_TEXP e m /\ ~(MEM e l) /\ 1520 EVERY notC l /\ unique_list l /\ EVERY (\x.valid_TEXP x m) l /\ (MAP conv_exp l = l') /\ 1521 (!i. i < 12 ==> (st '' (isM (w2n (read st FP) - 10 + i)) = st0 '' (EL i saved_regs_list))) /\ 1522 (!n. n < m ==> (st '' (isM (w2n (read st0 FP) - (12 + n))) = st0 '' (isM (w2n (read st0 FP) - (12 + n))))) 1523 ==> 1524 ((run_cfl (BLK (([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list l'))) st) '' 1525 (conv_exp e) = st0 '' (conv_exp e))`, 1526 1527 RW_TAC std_ss [APPEND, Once RUN_CFL_BLK_APPEND] THEN 1528 `w2n (read (run_cfl (BLK (MSUB R13 R11 (MC 11w)::[MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]])) st) FP) = w2n(read st0 FP)` 1529 by METIS_TAC [SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_2, rich_listTheory.CONS_APPEND] THEN 1530 IMP_RES_TAC VALID_TEXP_MEXP THEN IMP_RES_TAC VALID_MEXP_exp THEN 1531 IMP_RES_TAC VALID_TEXP_MEXP_SINGLE THEN IMP_RES_TAC VALID_MEXP_exp_SINGLE THEN 1532 IMP_RES_TAC valid_exp_thm THEN 1533 tac5 THEN 1534 IMP_RES_TAC eq_exp_lem_1 THEN 1535 RW_TAC std_ss [POP_LIST_SANITY] THEN NTAC 4 (POP_ASSUM (K ALL_TAC)) THEN 1536 Cases_on `e` THEN FULL_SIMP_TAC std_ss [conv_exp_def, valid_exp_def, valid_MEXP_def] THENL [ 1537 1538 NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN POP_ASSUM (MP_TAC) THEN POP_ASSUM (K ALL_TAC) THEN 1539 NTAC 2 (POP_ASSUM (MP_TAC)) THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN POP_ASSUM (MP_TAC) THEN 1540 NTAC 5 (POP_ASSUM (K ALL_TAC)) THEN POP_ASSUM (MP_TAC) THEN REPEAT (POP_ASSUM (K ALL_TAC)) THEN 1541 `?regs mem. st = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN 1542 RW_TAC std_ss [] THEN Q.UNABBREV_TAC `st1` THEN 1543 POP_ASSUM (ASSUME_TAC o GSYM) THEN 1544 RW_TAC std_ss [SIMP_RULE list_ss [] EVAL_POP_SAVED_REGS_LIST] THEN 1545 IMP_RES_TAC (GEN_ALL eval_saved_regs_list_lem) THEN 1546 NTAC 12 (POP_ASSUM MP_TAC) THEN RW_TAC std_ss [reade_def, read_thm, FP_def] THEN 1547 NTAC 14 (POP_ASSUM (K ALL_TAC)) THEN 1548 Cases_on `T'` THEN FULL_SIMP_TAC finmap_ss [data_reg_index_def], 1549 1550 RW_TAC std_ss [reade_def], 1551 1552 FULL_SIMP_TAC arith_ss [within_bound_def] THEN 1553 `!st n. st '' (isV (n + 12)) = reade st (isM (w2n (read st FP) - (12 + n)))` by 1554 (SIMP_TAC std_ss [FORALL_DSTATE, read_thm, reade_def, fp_def, FP_def, ADD_SYM]) THEN 1555 FULL_SIMP_TAC std_ss [] THEN METIS_TAC [ADD_SYM] 1556 ] 1557 ); 1558 1559val POST_CALL_RESTORED_REGS_LEM = Q.store_thm ( 1560 "POST_CALL_RESTORED_REGS_LEM", 1561 1562 `!st l m1 m2 e. (w2n (read st IP) = w2n (read st FP) + 1) /\ locate_ge (read st IP) 12 /\ 1563 w2n (read st IP) + LENGTH caller_o + (12 + m1) <= w2n (st '' isM (w2n (read st FP) - 1)) /\ 1564 (!i. i < 12 ==> (st '' (isM (w2n (read st FP) - 10 + i)) = st0 '' (EL i saved_regs_list))) /\ 1565 (!n. n < m1 ==> (st '' (isM (w2n (read st0 FP) - (12 + n))) = st0 '' (isM (w2n (read st0 FP) - (12 + n))))) /\ 1566 w2n (read st0 FP) - (12 + m1) >= w2n (read st IP) + LENGTH callee_o /\ 1567 valid_TEXP e m1 /\ ~(MEM e caller_o) /\ 1568 EVERY (\x. valid_TEXP x m2) callee_o /\ EVERY notC caller_o /\ unique_list caller_o /\ 1569 EVERY (\x.valid_TEXP x m1) caller_o /\ (LENGTH callee_o = LENGTH caller_o) 1570 ==> 1571 ((run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))) :: push_list (MAP conv_exp callee_o) 1572 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o)))) 1573 st) '' (conv_exp e) = st0 '' (conv_exp e))`, 1574 1575 RW_TAC bool_ss [] THEN 1576 REWRITE_TAC [Once RUN_CFL_BLK_APPEND] THEN 1577 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1578 push_list (MAP conv_exp callee_o))) st` THEN 1579 `grow_lt (read st IP) (LENGTH (MAP conv_exp callee_o))` by ( 1580 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1581 FULL_SIMP_TAC arith_ss [LENGTH_MAP, grow_lt_def]) THEN 1582 IMP_RES_TAC VALID_TEXP_MEXP THEN 1583 1584 `(!i. i < 12 ==> (w2n (read st FP) - 10 + i <= w2n (read st IP))) /\ (!n. w2n (read st FP) - (12 + n) <= 1585 w2n (read st IP)) /\ w2n (read st FP) - 1 <= w2n (read st IP)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1586 `(read st1 FP = read st FP) /\ (read st1 IP = read st IP) /\ 1587 (st1 '' isM (w2n (read st1 FP) - 1) = st '' isM (w2n (read st FP) - 1)) /\ 1588 (!i. i < 12 ==> (st1 '' (isM (w2n (read st1 FP) - 10 + i)) = st0 '' (EL i saved_regs_list)))` 1589 by (Q.UNABBREV_TAC `st1` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_1, w2n_11]) THEN 1590 1591 `(!n. n < m1 ==> (st1 '' (isM (w2n (read st0 FP) - (12 + n))) = st0 '' (isM (w2n (read st0 FP) - (12 + n)))))` by ( 1592 RW_TAC std_ss [] THEN 1593 `!a:num b c. a > b /\ b >= c ==> a > c` by RW_TAC arith_ss [] THEN 1594 `(!i. i > w2n (read st0 FP) - (12+m1) ==> (st1 '' isM i = st '' isM i))` by ( 1595 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_1) THEN NTAC 9 (POP_ASSUM (K ALL_TAC)) THEN 1596 RW_TAC std_ss [] THEN Q.UNABBREV_TAC `st1` THEN METIS_TAC [LENGTH_MAP]) THEN 1597 RW_TAC arith_ss []) THEN 1598 1599 IMP_RES_TAC word_add_lem_1 THEN 1600 NTAC 6 (POP_ASSUM MP_TAC) THEN NTAC 7 (POP_ASSUM (K ALL_TAC)) THEN 1601 NTAC 8 (POP_ASSUM MP_TAC) THEN NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN REPEAT STRIP_TAC THEN 1602 METIS_TAC [POST_CALL_SANITY_4] 1603 ); 1604 1605val POST_CALL_SANITY_LEM = Q.store_thm ( 1606 "POST_CALL_SANITY_LEM", 1607 1608 `!st l m1 m2 e. (w2n (read st IP) = w2n (read st FP) + 1) /\ locate_ge (read st IP) 12 /\ 1609 w2n (read st IP) + LENGTH caller_o + (12 + m1) <= w2n (st '' isM (w2n (read st FP) - 1)) /\ 1610 w2n (read st0 FP) - 12 >= w2n (read st IP) + LENGTH caller_o /\ 1611 (!i. i < 12 ==> (st '' (isM (w2n (read st FP) - 10 + i)) = st0 '' (EL i saved_regs_list))) /\ 1612 EVERY (\x. valid_TEXP x m2) callee_o /\ EVERY notC caller_o /\ unique_list caller_o /\ 1613 EVERY (\x.valid_TEXP x m1) caller_o /\ (LENGTH callee_o = LENGTH caller_o) 1614 ==> 1615 let st' = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o))))::push_list (MAP conv_exp callee_o) 1616 ++ ([MSUB R13 R11 (MC 11w)] ++ [MPOP 13 [0;1;2;3;4;5;6;7;8;fp;ip;lr]] ++ pop_list (MAP conv_exp caller_o)))) st 1617 in 1618 (!i. i > w2n (read st0 FP) - 12 ==> (st '' isM i = st' '' isM i)) /\ 1619 (w2n (read st' FP) = w2n (read st0 FP)) /\ (w2n (read st' IP) = w2n (read st0 IP)) /\ 1620 (w2n (read st' SP) = w2n (read st FP) + 1 + LENGTH caller_o)`, 1621 1622 REPEAT GEN_TAC THEN STRIP_TAC THEN 1623 REWRITE_TAC [Once RUN_CFL_BLK_APPEND] THEN 1624 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1625 push_list (MAP conv_exp callee_o))) st` THEN 1626 1627 `grow_lt (read st IP) (LENGTH (MAP conv_exp callee_o))` by ( 1628 `w2n (st '' isM (w2n (read st FP) - 1)) < dimword (:32)` by METIS_TAC [w2n_lt] THEN 1629 FULL_SIMP_TAC arith_ss [LENGTH_MAP, grow_lt_def]) THEN 1630 IMP_RES_TAC VALID_TEXP_MEXP THEN 1631 1632 `(!i. i < 12 ==> (w2n (read st FP) - 10 + i <= w2n (read st IP))) /\ w2n (read st FP) - 1 <= w2n (read st IP) /\ 1633 (!a:num b c. a > b /\ b >= c ==> a > c)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1634 `(read st1 FP = read st FP) /\ (read st1 IP = read st IP) /\ 1635 (st1 '' isM (w2n (read st1 FP) - 1) = st '' isM (w2n (read st FP) - 1)) /\ 1636 (!i. i < 12 ==> (st1 '' (isM (w2n (read st1 FP) - 10 + i)) = st0 '' (EL i saved_regs_list)))` 1637 by (Q.UNABBREV_TAC `st1` THEN METIS_TAC [SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_1, w2n_11]) THEN 1638 `(!i. i > w2n (read st0 FP) - 12 ==> (st1 '' isM i = st '' isM i))` by ( 1639 IMP_RES_TAC (SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_1) THEN NTAC 9 (POP_ASSUM (K ALL_TAC)) THEN 1640 RW_TAC std_ss [] THEN Q.UNABBREV_TAC `st1` THEN METIS_TAC [LENGTH_MAP]) THEN 1641 1642 IMP_RES_TAC word_add_lem_1 THEN 1643 `locate_ge (read st1 FP + 1w) 12 /\ w2n (read st1 FP) + 1 + LENGTH caller_o + (12 + m1) <= 1644 w2n (st1 '' isM (w2n (read st1 FP) - 1))` by METIS_TAC [] THEN 1645 NTAC 8 (POP_ASSUM MP_TAC) THEN NTAC 6 (POP_ASSUM (K ALL_TAC)) THEN 1646 NTAC 5 (POP_ASSUM MP_TAC) THEN REPEAT (POP_ASSUM (K ALL_TAC)) THEN REPEAT STRIP_TAC THEN 1647 IMP_RES_TAC POST_CALL_SANITY_3 THEN NTAC 60 (POP_ASSUM (K ALL_TAC)) THEN 1648 FULL_SIMP_TAC std_ss [LET_THM] 1649 ); 1650 1651(*---------------------------------------------------------------------------------*) 1652(* Main theorems about post-call processing *) 1653(*---------------------------------------------------------------------------------*) 1654 1655val valid_post_call_def = Define ` 1656 valid_post_call (st0,st) (m1,m2) (callee_o,caller_o) = 1657 (w2n (read st IP) = w2n (read st FP) + 1) /\ locate_ge (read st IP) 12 /\ 1658 w2n (read st IP) + LENGTH caller_o + (12 + m1) <= w2n (st '' isM (w2n (read st FP) - 1)) /\ 1659 w2n (read st0 FP) - (12 + m1) >= w2n (read st IP) + LENGTH callee_o /\ 1660 (!i. i < 12 ==> (st '' isM (w2n (read st FP) - 10 + i) = st0 '' EL i saved_regs_list)) /\ 1661 EVERY (\x. valid_TEXP x m2) callee_o /\ EVERY notC caller_o /\ unique_list caller_o /\ 1662 EVERY (\x. valid_TEXP x m1) caller_o /\ (LENGTH callee_o = LENGTH caller_o)`; 1663 1664 1665val POST_CALL_SANITY_THM = Q.store_thm ( 1666 "POST_CALL_SANITY_THM", 1667 `!st st0 m1 m2 caller_o callee_o. 1668 valid_post_call (st0,st) (m1,m2) (callee_o,caller_o) 1669 ==> 1670 let st' = run_cfl (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1)) st in 1671 (!i. i > w2n (read st0 FP) - 12 ==> (st '' isM i = st' '' isM i)) /\ 1672 (w2n (read st' FP) = w2n (read st0 FP)) /\ (w2n (read st' IP) = w2n (read st0 IP)) /\ 1673 (w2n (read st' SP) = w2n (read st0 FP) - (12 + m1))`, 1674 1675 REPEAT GEN_TAC THEN REWRITE_TAC [valid_post_call_def] THEN STRIP_TAC THEN 1676 `w2n (read st0 FP) - 12 >= w2n (read st IP) + LENGTH caller_o` by RW_TAC arith_ss [] THEN 1677 SIMP_TAC std_ss [post_call_def, Once RUN_CFL_BLK_APPEND] THEN 1678 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1679 push_list (MAP conv_exp callee_o) ++ [MSUB R13 R11 (MC 11w)] ++ 1680 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN 1681 1682 ` (!i. i > w2n (read st0 FP) - 12 ==> (st '' isM i = st1 '' isM i)) /\ 1683 (w2n (read st1 FP) = w2n (read st0 FP)) /\ (w2n (read st1 IP) = w2n (read st0 IP)) /\ 1684 (w2n (read st1 SP) = w2n (read st FP) + 1 + LENGTH caller_o)` by 1685 (Q.UNABBREV_TAC `st1` THEN METIS_TAC [SIMP_RULE bool_ss [LET_THM, APPEND_ASSOC] POST_CALL_SANITY_LEM]) THEN 1686 1687 `locate_ge (read st1 FP) (12 + m1)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1688 RW_TAC std_ss [LET_THM, SIMP_RULE std_ss [LET_THM] sub_sp_lem_1] 1689 ); 1690 1691val POST_CALL_PASS_RESULTS_THM = Q.store_thm ( 1692 "POST_CALL_PASS_RESULTS_THM", 1693 1694 `!st m1 m2 caller_o callee_o. 1695 valid_post_call (st0,st) (m1,m2) (callee_o,caller_o) 1696 ==> 1697 !i. i < LENGTH caller_o ==> 1698 (run_cfl (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1)) st '' 1699 EL i (MAP conv_exp caller_o) = st '' EL i (MAP conv_exp callee_o))`, 1700 1701 REPEAT GEN_TAC THEN REWRITE_TAC [valid_post_call_def] THEN STRIP_TAC THEN 1702 `w2n (read st0 FP) - 12 >= w2n (read st IP) + LENGTH caller_o` by RW_TAC arith_ss [] THEN 1703 SIMP_TAC std_ss [post_call_def, Once RUN_CFL_BLK_APPEND] THEN 1704 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1705 push_list (MAP conv_exp callee_o) ++ [MSUB R13 R11 (MC 11w)] ++ 1706 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN 1707 1708 RW_TAC std_ss [] THEN 1709 `st1 '' EL i (MAP conv_exp caller_o) = st '' EL i (MAP conv_exp callee_o)` by 1710 (ASSUME_TAC (SPEC_ALL POST_CALL_PASS_RESULTS_LEM) THEN 1711 Q.UNABBREV_TAC `st1` THEN FULL_SIMP_TAC list_ss [LET_THM]) THEN 1712 `w2n (read st1 FP) = w2n (read st0 FP)` by 1713 (Q.UNABBREV_TAC `st1` THEN METIS_TAC [SIMP_RULE bool_ss [LET_THM, APPEND_ASSOC] POST_CALL_SANITY_LEM]) THEN 1714 1715 `locate_ge (read st1 FP) (12 + m1)` by FULL_SIMP_TAC arith_ss [locate_ge_def] THEN 1716 RW_TAC std_ss [LET_THM, SIMP_RULE std_ss [LET_THM] sub_sp_lem_1] 1717 ); 1718 1719val POST_CALL_RESTORED_REGS_THM = Q.store_thm ( 1720 "POST_CALL_RESTORED_REGS_THM", 1721 1722 `!st m1 m2 caller_o callee_o. 1723 valid_post_call (st0,st) (m1,m2) (callee_o,caller_o) /\ 1724 (!n. n < m1 ==> (st '' isM (w2n (read st0 FP) - (12 + n)) = st0 '' isM (w2n (read st0 FP) - (12 + n)))) /\ 1725 ~MEM e caller_o /\ valid_TEXP e m1 1726 ==> 1727 (run_cfl (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1)) st '' 1728 (conv_exp e) = st0 '' (conv_exp e))`, 1729 1730 REPEAT GEN_TAC THEN REWRITE_TAC [valid_post_call_def] THEN STRIP_TAC THEN 1731 SIMP_TAC std_ss [post_call_def, Once RUN_CFL_BLK_APPEND] THEN 1732 Q.ABBREV_TAC `st1 = run_cfl (BLK (MADD R13 R12 (MC (n2w (LENGTH (MAP conv_exp callee_o)))):: 1733 push_list (MAP conv_exp callee_o) ++ [MSUB R13 R11 (MC 11w)] ++ 1734 [MPOP 13 [0; 1; 2; 3; 4; 5; 6; 7; 8; fp; ip; lr]] ++ pop_list (MAP conv_exp caller_o))) st` THEN 1735 1736 `st0 '' (conv_exp e) = st1 '' (conv_exp e)` by ( 1737 `w2n (read st0 FP) >= m1 + (LENGTH callee_o + (w2n (read st IP) + 12))` by RW_TAC arith_ss [] THEN 1738 ASSUME_TAC (SPEC_ALL POST_CALL_RESTORED_REGS_LEM) THEN 1739 Q.UNABBREV_TAC `st1` THEN FULL_SIMP_TAC list_ss [LET_THM]) THEN 1740 1741 `?regs mem. st1 = (regs,mem)` by METIS_TAC [ABS_PAIR_THM] THEN 1742 RW_TAC std_ss [CFL_SEMANTICS_BLK] THEN tac1 THEN 1743 Cases_on `e` THEN 1744 FULL_SIMP_TAC finmap_ss [valid_TEXP_def, conv_exp_def, reade_def, read_thm, fp_def] THEN 1745 Cases_on `T'` THEN FULL_SIMP_TAC std_ss [data_reg_index_def] 1746 ); 1747 1748(*---------------------------------------------------------------------------------*) 1749(* Lemmas for proving main theorems about function calls *) 1750(*---------------------------------------------------------------------------------*) 1751 1752val same_fp_ip_sp_def = Define ` 1753 same_fp_ip_sp st1 st0 = 1754 (w2n (read st1 FP) = w2n (read st0 FP)) /\ 1755 (w2n (read st1 IP) = w2n (read st0 IP)) /\ 1756 (w2n (read st1 SP) = w2n (read st0 SP))`; 1757 1758val status_intact_def = Define ` 1759 status_intact st1 st0 = 1760 same_fp_ip_sp st1 st0 /\ 1761 (!i. i > w2n (read st0 FP) - 12 ==> (st1 '' isM i = st0 '' isM i))`; 1762 1763val PRE_CALL_FP_IP_IN_MEM = Q.store_thm ( 1764 "PRE_CALL_FP_IP_IN_MEM", 1765 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 1766 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 1767 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 1768 ==> 1769 let st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st in 1770 (st' '' (isM (w2n (read st' FP) - 10 + 10)) = read st IP) /\ 1771 (st' '' (isM (w2n (read st' FP) - 10 + 9)) = read st FP)`, 1772 1773 REPEAT GEN_TAC THEN STRIP_TAC THEN 1774 IMP_RES_TAC PRE_CALL_SAVED_REGS_THM_2 THEN NTAC 13 (POP_ASSUM (K ALL_TAC)) THEN 1775 FULL_SIMP_TAC std_ss [LET_THM] THEN 1776 RW_TAC list_ss [saved_regs_list_def, reade_def, IP_def, FP_def, ip_def, fp_def] 1777 ); 1778 1779val fun_call_lem_1 = Q.store_thm ( 1780 "fun_call_lem_1", 1781 `!k j st st' st2. locate_ge (read st SP) (k + 13 + j + m2) /\ standard_frame st m1 /\ 1782 (w2n (read st2 FP) = w2n (read st' FP)) /\ 1783 (w2n (read st SP) - (k + j) - 1 = w2n (read st' FP)) ==> 1784 (!i. i < 12 ==> w2n (read st' FP) - 10 + i > w2n (read st2 FP) - 12) /\ 1785 (w2n (read st' FP) - 10 + 9 = w2n (read st' FP) - 1)`, 1786 RW_TAC arith_ss [locate_ge_def, standard_frame_def] 1787 ); 1788 1789val fun_call_lem_2 = Q.store_thm ( 1790 "fun_call_lem_2", 1791 `!x y. locate_ge x (MAX n1 n2 + 13 + m2) /\ 1792 (MAX n1 n2 - n1 = k) /\ (w2n x - (k + n1) - 1 = y) ==> 1793 12 + m2 <= y /\ y + n2 < w2n x`, 1794 RW_TAC arith_ss [locate_ge_def, MAX_DEF] 1795 ); 1796 1797val fun_call_lem_3 = Q.store_thm ( 1798 "fun_call_lem_3", 1799 `!k n1 n2 st st' st2. 1800 standard_frame st m1 /\ 1801 (w2n (read st2 FP) = w2n (read st' FP)) /\ (w2n (read st2 IP) = w2n (read st' FP) + 1) /\ 1802 locate_ge (read st SP) (MAX n1 n2 + 13 + m2) /\ 1803 (MAX n1 n2 - n1 = k) /\ 1804 (w2n (read st SP) - (k + n1) - 1 = w2n (read st' FP)) 1805 ==> 1806 (w2n (read st2 IP) = w2n (read st2 FP) + 1) /\ locate_ge (read st2 IP) 12 /\ 1807 w2n (read st2 IP) + n2 + (12 + m1) <= w2n (read st FP) /\ 1808 w2n (read st FP) - (12 + m1) >= w2n (read st2 IP) + n2 /\ 1809 (!i. i > w2n (read st FP) - 12 ==> i > w2n (read st SP) /\ i > w2n (read st' FP) - 12)`, 1810 1811 REPEAT GEN_TAC THEN STRIP_TAC THEN 1812 IMP_RES_TAC fun_call_lem_2 THEN 1813 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN NTAC 2 STRIP_TAC THEN 1814 FULL_SIMP_TAC arith_ss [locate_ge_def, standard_frame_def] 1815 ); 1816 1817val VALID_BEFORE_POST_CALL = Q.store_thm ( 1818 "VALID_BEFORE_POST_CALL", 1819 `!st m1 m2 caller_i callee_i caller_o callee_o. 1820 locate_ge (read st SP) (MAX (LENGTH caller_i) (LENGTH caller_o) + 13 + m2) /\ 1821 (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 1822 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i) = k) /\ 1823 (st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) /\ 1824 status_intact (run_cfl S_body st') st' /\ 1825 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) /\ WELL_FORMED S_body 1826 ==> 1827 valid_post_call (st, run_cfl S_body st') (m1,m2) (callee_o,caller_o)`, 1828 1829 REPEAT GEN_TAC THEN STRIP_TAC THEN 1830 `standard_frame st m1` by FULL_SIMP_TAC arith_ss [standard_frame_def, locate_ge_def] THEN 1831 FULL_SIMP_TAC std_ss [LET_THM, CFL_SEMANTICS_SC, WELL_FORMED_thm] THEN 1832 Q.PAT_ASSUM `st' = kk` (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1833 `locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def, MAX_DEF] THEN 1834 1835 `!i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))` by 1836 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SAVED_REGS_THM_2]) THEN 1837 `(st' '' isM (w2n (read st' FP) - 10 + 10) = read st IP) /\ (st' '' isM (w2n (read st' FP) - 10 + 9) = read st FP)` 1838 by (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_FP_IP_IN_MEM]) THEN 1839 `(!i. i > w2n (read st SP) ==> (st' '' (isM i) = st '' (isM i))) /\ 1840 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 1841 (w2n (read st' IP) = w2n (read st' FP) + 1) /\ (w2n (read st' SP) = w2n (read st' FP) - (12 + m2))` by 1842 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_THM_2]) THEN 1843 1844 Q.PAT_ASSUM `run_cfl x y = k` (K ALL_TAC) THEN 1845 Q.ABBREV_TAC `st2 = run_cfl S_body st'` THEN 1846 Q.ABBREV_TAC `st3 = run_cfl (BLK (post_call (MAP conv_exp caller_o,MAP conv_exp callee_o) m1)) st2` THEN 1847 Q.PAT_ASSUM `w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1` (ASSUME_TAC o GSYM) THEN 1848 FULL_SIMP_TAC std_ss [status_intact_def, same_fp_ip_sp_def] THEN 1849 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN NTAC 2 STRIP_TAC THEN 1850 1851 `!i. i < 12 ==> w2n (read st' FP) - 10 + i > w2n (read st2 FP) - 12` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1] THEN 1852 `st2 '' isM (w2n (read st2 FP) - 1) = read st FP` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1, DECIDE ``9 < 12``] THEN 1853 `!i. i < 12 ==> (st2 '' isM (w2n (read st2 FP) - 10 + i) = st '' EL i saved_regs_list)` by METIS_TAC [] THEN 1854 1855 `(w2n (read st SP) - (k + LENGTH caller_i) - 1 = w2n (read st' FP)) /\ 1856 (MAX (LENGTH callee_i) (LENGTH caller_o) - LENGTH callee_i = k)` by METIS_TAC [VALID_FC_1_def] THEN 1857 IMP_RES_TAC (Q.SPECL [`k`, `LENGTH (caller_i:TEXP list)`, `LENGTH (caller_o:TEXP list)`, `st`, `st'`, `st2`] fun_call_lem_3) THEN 1858 NTAC 78 (POP_ASSUM (K ALL_TAC)) THEN 1859 FULL_SIMP_TAC bool_ss [valid_post_call_def, VALID_FC_1_def] THEN 1860 METIS_TAC [] 1861 ); 1862 1863(*---------------------------------------------------------------------------------*) 1864(* Main theorems about pre-call processing and post-call processing *) 1865(* The pre-call processing and post-call processing do accomplish parameter *) 1866(* passing and result passing repsectively *) 1867(*---------------------------------------------------------------------------------*) 1868 1869val PRE_CALL_PRE_CALL_THM = Q.store_thm ( 1870 "PRE_CALL_PRE_CALL_THM", 1871 `!st l m1 m2 k. locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2) /\ standard_frame st m1 /\ 1872 EVERY notC callee_i /\ unique_list callee_i /\ EVERY (\x.valid_TEXP x m2) callee_i /\ 1873 EVERY (\x. valid_TEXP x m1) caller_i /\ (LENGTH callee_i = LENGTH caller_i) 1874 ==> 1875 (MAP (reade st o conv_exp) caller_i = 1876 MAP (reade (run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) 1877 o conv_exp) callee_i)`, 1878 1879 RW_TAC std_ss [] THEN 1880 MATCH_MP_TAC MAP_LEM_3 THEN RW_TAC std_ss [] THEN 1881 METIS_TAC [SIMP_RULE std_ss [rich_listTheory.EL_MAP] PRE_CALL_PASS_ARGUMENTS_THM_2] 1882 ); 1883 1884 1885val POST_CALL_PRE_CALL_THM = Q.store_thm ( 1886 "POST_CALL_PRE_CALL_THM", 1887 `!st m1 m2 caller_o callee_o. 1888 valid_post_call (st0,st) (m1,m2) (callee_o,caller_o) ==> 1889 (MAP (reade st o conv_exp) callee_o = 1890 MAP (reade (run_cfl (BLK (post_call (MAP conv_exp caller_o,MAP conv_exp callee_o) m1)) st) 1891 o conv_exp) caller_o)`, 1892 1893 RW_TAC std_ss [] THEN 1894 `LENGTH caller_o = LENGTH callee_o` by FULL_SIMP_TAC std_ss [valid_post_call_def] THEN 1895 MATCH_MP_TAC MAP_LEM_3 THEN RW_TAC std_ss [] THEN 1896 METIS_TAC [rich_listTheory.EL_MAP, POST_CALL_PASS_RESULTS_THM] 1897 ); 1898 1899(*---------------------------------------------------------------------------------*) 1900(* Main theorems about function calls *) 1901(* The values fp,ip and sp are recovered after the function call; *) 1902(* the caller's frame will not be altered unneccessarily (i.e. only those for *) 1903(* receiving results from the callee will be changed). This guarantees the *) 1904(* separation of the caller's frame (activation record) and the callee's frame *) 1905(*---------------------------------------------------------------------------------*) 1906 1907val FUN_CALL_SANITY_THM = Q.store_thm ( 1908 "FUN_CALL_SANITY_THM", 1909 `!st m1 m2 caller_i callee_i caller_o callee_o. 1910 locate_ge (read st SP) (MAX (LENGTH caller_i) (LENGTH caller_o) + 13 + m2) /\ 1911 standard_frame st m1 /\ (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 1912 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i) = k) /\ 1913 (st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) /\ 1914 status_intact (run_cfl S_body st') st' /\ 1915 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) /\ WELL_FORMED S_body 1916 ==> 1917 let st1 = run_cfl (SC (SC (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) S_body) 1918 (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1))) st in 1919 status_intact st1 st`, 1920 1921 REPEAT GEN_TAC THEN STRIP_TAC THEN 1922 FULL_SIMP_TAC std_ss [LET_THM, CFL_SEMANTICS_SC, WELL_FORMED_thm] THEN 1923 Q.PAT_ASSUM `st' = kk` (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1924 `locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def, MAX_DEF] THEN 1925 1926 `!i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))` by 1927 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SAVED_REGS_THM_2]) THEN 1928 `(st' '' isM (w2n (read st' FP) - 10 + 10) = read st IP) /\ (st' '' isM (w2n (read st' FP) - 10 + 9) = read st FP)` 1929 by (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_FP_IP_IN_MEM]) THEN 1930 `(!i. i > w2n (read st SP) ==> (st' '' (isM i) = st '' (isM i))) /\ 1931 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 1932 (w2n (read st' IP) = w2n (read st' FP) + 1) /\ (w2n (read st' SP) = w2n (read st' FP) - (12 + m2))` by 1933 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_THM_2]) THEN 1934 1935 Q.PAT_ASSUM `run_cfl x y = k` (K ALL_TAC) THEN 1936 Q.ABBREV_TAC `st2 = run_cfl S_body st'` THEN 1937 Q.ABBREV_TAC `st3 = run_cfl (BLK (post_call (MAP conv_exp caller_o,MAP conv_exp callee_o) m1)) st2` THEN 1938 Q.PAT_ASSUM `w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1` (ASSUME_TAC o GSYM) THEN 1939 FULL_SIMP_TAC std_ss [status_intact_def, same_fp_ip_sp_def] THEN 1940 NTAC 2 (POP_ASSUM MP_TAC) THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN NTAC 2 STRIP_TAC THEN 1941 1942 `!i. i < 12 ==> w2n (read st' FP) - 10 + i > w2n (read st2 FP) - 12` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1] THEN 1943 `st2 '' isM (w2n (read st2 FP) - 1) = read st FP` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1, DECIDE ``9 < 12``] THEN 1944 `!i. i < 12 ==> (st2 '' isM (w2n (read st2 FP) - 10 + i) = st '' EL i saved_regs_list)` by METIS_TAC [] THEN 1945 1946 `(w2n (read st SP) - (k + LENGTH caller_i) - 1 = w2n (read st' FP)) /\ 1947 (MAX (LENGTH callee_i) (LENGTH caller_o) - LENGTH callee_i = k)` by METIS_TAC [VALID_FC_1_def] THEN 1948 IMP_RES_TAC (Q.SPECL [`k`, `LENGTH (caller_i:TEXP list)`, `LENGTH (caller_o:TEXP list)`, `st`, `st'`, `st2`] fun_call_lem_3) THEN 1949 NTAC 78 (POP_ASSUM (K ALL_TAC)) THEN 1950 `valid_post_call (st,st2) (m1,m2) (callee_o,caller_o)` by ( 1951 FULL_SIMP_TAC bool_ss [valid_post_call_def, VALID_FC_1_def] THEN METIS_TAC []) THEN 1952 Q.UNABBREV_TAC `st3` THEN 1953 METIS_TAC [SIMP_RULE std_ss [LET_THM] POST_CALL_SANITY_THM] 1954 ); 1955 1956val FUN_CALL_VALUE_RESTORING = Q.store_thm ( 1957 "FUN_CALL_VALUE_RESTORING", 1958 1959 `!st m1 m2 caller_i callee_i caller_o callee_o. 1960 locate_ge (read st SP) (MAX (LENGTH caller_i) (LENGTH caller_o) + 13 + m2) /\ 1961 standard_frame st m1 /\ (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 1962 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i) = k) /\ 1963 (st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) /\ 1964 status_intact (run_cfl S_body st') st' /\ 1965 ~MEM e caller_o /\ valid_TEXP e m1 /\ 1966 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) /\ WELL_FORMED S_body 1967 ==> 1968 let st1 = run_cfl (SC (SC (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) S_body) 1969 (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1))) st in 1970 st1 '' (conv_exp e) = st '' (conv_exp e)`, 1971 1972 REPEAT GEN_TAC THEN STRIP_TAC THEN 1973 FULL_SIMP_TAC std_ss [LET_THM, CFL_SEMANTICS_SC, WELL_FORMED_thm] THEN 1974 Q.PAT_ASSUM `st' = kk` (ASSUME_TAC o GSYM) THEN ASM_REWRITE_TAC [] THEN 1975 `locate_ge (read st SP) (k + 13 + LENGTH caller_i + m2)` by FULL_SIMP_TAC arith_ss [locate_ge_def, MAX_DEF] THEN 1976 1977 `!i. i < 12 ==> (st' '' (isM (w2n (read st' FP) - 10 + i)) = st '' (EL i saved_regs_list))` by 1978 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SAVED_REGS_THM_2]) THEN 1979 `(st' '' isM (w2n (read st' FP) - 10 + 9) = read st FP)` by (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_FP_IP_IN_MEM]) THEN 1980 1981 `(!i. i > w2n (read st SP) ==> (st' '' (isM i) = st '' (isM i))) /\ 1982 (w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1) /\ 1983 (w2n (read st' IP) = w2n (read st' FP) + 1) /\ (w2n (read st' SP) = w2n (read st' FP) - (12 + m2))` by 1984 (METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_THM_2]) THEN 1985 1986 `!n. n < m1 ==> w2n (read st FP) - (12 + n) > w2n (read st SP) /\ w2n (read st FP) - (12 + n) > w2n (read st' FP) - 12` by 1987 (ASM_REWRITE_TAC [] THEN NTAC 6 (POP_ASSUM (K ALL_TAC)) THEN 1988 FULL_SIMP_TAC arith_ss [standard_frame_def, locate_ge_def]) THEN 1989 1990 Q.PAT_ASSUM `run_cfl x y = k` (K ALL_TAC) THEN 1991 Q.ABBREV_TAC `st2 = run_cfl S_body st'` THEN 1992 `!n. n < m1 ==> (st2 '' isM (w2n (read st FP) - (12 + n)) = st '' isM (w2n (read st FP) - (12 + n)))` by 1993 METIS_TAC [VALID_FC_1_def, SIMP_RULE std_ss [LET_THM] PRE_CALL_SANITY_THM_2, status_intact_def] THEN 1994 POP_ASSUM MP_TAC THEN NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN 1995 1996 Q.ABBREV_TAC `st3 = run_cfl (BLK (post_call (MAP conv_exp caller_o,MAP conv_exp callee_o) m1)) st2` THEN 1997 Q.PAT_ASSUM `w2n (read st' FP) = w2n (read st SP) - (k + LENGTH callee_i) - 1` (ASSUME_TAC o GSYM) THEN 1998 FULL_SIMP_TAC std_ss [status_intact_def, same_fp_ip_sp_def] THEN 1999 2000 `!i. i < 12 ==> w2n (read st' FP) - 10 + i > w2n (read st2 FP) - 12` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1] THEN 2001 `st2 '' isM (w2n (read st2 FP) - 1) = read st FP` by METIS_TAC [VALID_FC_1_def, fun_call_lem_1, DECIDE ``9 < 12``] THEN 2002 `!i. i < 12 ==> (st2 '' isM (w2n (read st2 FP) - 10 + i) = st '' EL i saved_regs_list)` by METIS_TAC [] THEN 2003 2004 `(w2n (read st SP) - (k + LENGTH caller_i) - 1 = w2n (read st' FP)) /\ 2005 (MAX (LENGTH callee_i) (LENGTH caller_o) - LENGTH callee_i = k)` by METIS_TAC [VALID_FC_1_def] THEN 2006 IMP_RES_TAC (Q.SPECL [`k`, `LENGTH (caller_i:TEXP list)`, `LENGTH (caller_o:TEXP list)`, `st`, `st'`, `st2`] fun_call_lem_3) THEN 2007 NTAC 104 (POP_ASSUM (K ALL_TAC)) THEN 2008 `valid_post_call (st,st2) (m1,m2) (callee_o,caller_o)` by ( 2009 FULL_SIMP_TAC bool_ss [valid_post_call_def, VALID_FC_1_def] THEN METIS_TAC []) THEN 2010 Q.UNABBREV_TAC `st3` THEN STRIP_TAC THEN 2011 METIS_TAC [POST_CALL_RESTORED_REGS_THM] 2012 ); 2013 2014(*---------------------------------------------------------------------------------*) 2015(* Theorems showing that this implementation of function calls is correct *) 2016(*---------------------------------------------------------------------------------*) 2017 2018val sp_locate_lem_1 = Q.store_thm ( 2019 "sp_locate_lem_1", 2020 `!x i1 i2 m2. locate_ge x (MAX i1 i2 + 13 + m2) ==> 2021 locate_ge x (MAX i1 i2 - i1 + 13 + i1 + m2)`, 2022 RW_TAC std_ss [locate_ge_def, MAX_DEF] THEN 2023 RW_TAC arith_ss [] 2024 ); 2025 2026val FC_IMPLEMENTATION_LEM = Q.store_thm ( 2027 "FC_IMPLEMENTATION_LEM", 2028 2029 `!st m1 m2 caller_i callee_i caller_o callee_o. 2030 VALID_FC_1 (caller_i,callee_i,callee_o,caller_o) (m1,m2) /\ WELL_FORMED S_body /\ 2031 locate_ge (read st SP) (MAX (LENGTH caller_i) (LENGTH caller_o) + 13 + m2) /\ 2032 (w2n (read st SP) = w2n (read st FP) - (12 + m1)) /\ 2033 (MAX (LENGTH caller_i) (LENGTH caller_o) - (LENGTH caller_i) = k) /\ 2034 (st' = run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) st) /\ 2035 status_intact (run_cfl S_body st') st' /\ 2036 same_content s st m1 /\ 2037 same_content (run_hsl S_hsl (transfer (empty_s,s) (callee_i,caller_i))) (run_cfl S_body st') m2 2038 ==> 2039 same_content (run_hsl (Fc (caller_i, callee_i) S_hsl (caller_o, callee_o) (m1,m2)) s) 2040 (run_cfl (SC (SC (BLK (pre_call_2 (MAP conv_exp caller_i, MAP conv_exp callee_i) k m2)) S_body) 2041 (BLK (post_call (MAP conv_exp caller_o, MAP conv_exp callee_o) m1))) st) m1`, 2042 2043 RW_TAC std_ss [] THEN 2044 MATCH_MP_TAC (SIMP_RULE std_ss [LET_THM, AND_IMP_INTRO] FC_SUFFICIENT_COND_LEM) THEN 2045 RW_TAC std_ss [] THENL [ 2046 FULL_SIMP_TAC std_ss [valid_arg_list_def, VALID_FC_1_def], 2047 RW_TAC std_ss [WELL_FORMED_thm], 2048 FULL_SIMP_TAC std_ss [VALID_FC_1_def], 2049 `standard_frame st m1` by FULL_SIMP_TAC arith_ss [standard_frame_def, locate_ge_def] THEN 2050 IMP_RES_TAC sp_locate_lem_1 THEN 2051 METIS_TAC [VALID_FC_1_def, PRE_CALL_PRE_CALL_THM], 2052 Q.ABBREV_TAC `st' = run_cfl S_body (run_cfl (BLK (pre_call_2 (MAP conv_exp caller_i,MAP conv_exp callee_i) 2053 (MAX (LENGTH caller_i) (LENGTH caller_o) - LENGTH caller_i) m2)) st)` THEN 2054 `valid_post_call (st,st') (m1,m2) (callee_o,caller_o)` by ( 2055 Q.UNABBREV_TAC `st'` THEN METIS_TAC [VALID_BEFORE_POST_CALL]) THEN 2056 METIS_TAC [POST_CALL_PRE_CALL_THM], 2057 `standard_frame st m1` by FULL_SIMP_TAC arith_ss [standard_frame_def, locate_ge_def] THEN 2058 METIS_TAC [SIMP_RULE std_ss [LET_THM] FUN_CALL_VALUE_RESTORING] 2059 ] 2060 ); 2061 2062(*---------------------------------------------------------------------------------*) 2063 2064val _ = export_theory(); 2065 2066