1(* interactive use: 2 3quietdec := true; 4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath; 5 6app load ["numLib", "preARMTheory", "pred_setSimps", "pred_setTheory", 7 "rich_listTheory", "ARMCompositionTheory", "ILTheory", "wordsTheory"]; 8 9quietdec := false; 10*) 11 12 13open HolKernel Parse boolLib bossLib numLib relationTheory arithmeticTheory preARMTheory pairTheory 14 pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory ARMCompositionTheory ILTheory wordsTheory; 15 16 17val _ = new_theory "rules"; 18val _ = hide "cond"; 19 20(*---------------------------------------------------------------------------------*) 21(* Simplifier on finite maps *) 22(*---------------------------------------------------------------------------------*) 23 24val set_ss = std_ss ++ SET_SPEC_ss ++ PRED_SET_ss; 25 26(*---------------------------------------------------------------------------------*) 27(* Inference based on Hoare Logic *) 28(*---------------------------------------------------------------------------------*) 29 30(*---------------------------------------------------------------------------------*) 31(* read from an data state *) 32(*---------------------------------------------------------------------------------*) 33val _ = Hol_datatype ` 34 REXP = RR of MREG 35 | RM of MMEM 36 | RC of DATA 37 | PR of REXP # REXP 38 `; 39 40 41val mread_def = Define ` 42 (mread st (RR r) = read st (toREG r)) /\ 43 (mread st (RM m) = read st (toMEM m)) /\ 44 (mread st (RC c) = c)`; 45 46val _ = add_rule {term_name = "mread", fixity = Suffix 60, 47 pp_elements = [TOK "<", TM, TOK ">"], 48 paren_style = OnlyIfNecessary, 49 block_style = (AroundSameName, (PP.INCONSISTENT, 0))} handle HOL_ERR e => print (#message e); 50 51 52(*---------------------------------------------------------------------------------*) 53(* The fp and sp point to the default positions *) 54(*---------------------------------------------------------------------------------*) 55 56val proper_def = Define ` 57 proper = (\(regs,mem):DSTATE. (regs ' 11w = 100w) /\ (regs ' 13w = 100w))`; 58 59 60(*---------------------------------------------------------------------------------*) 61(* Hoare Logic Style Specification *) 62(*---------------------------------------------------------------------------------*) 63 64val HSPEC_def = Define ` 65 HSPEC P ir Q = !st. P st ==> Q (run_ir ir st)`; 66 67val _ = type_abbrev("HSPEC_TYPE", type_of (Term `HSPEC`)); 68 69(* 70val _ = add_rule {term_name = "HSPEC", 71 fixity = Infix (HOLgrammars.RIGHT, 3), 72 pp_elements = [HardSpace 1, TOK "(", TM, TOK ")", HardSpace 1], 73 paren_style = OnlyIfNecessary, 74 block_style = (AroundEachPhrase, 75 (PP.INCONSISTENT, 0))}; 76*) 77 78(*---------------------------------------------------------------------------------*) 79(* Sequential Composition *) 80(*---------------------------------------------------------------------------------*) 81 82val SC_RULE = Q.store_thm ( 83 "SC_RULE", 84 `!P Q R ir1 ir2. WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 85 HSPEC P ir1 Q /\ HSPEC Q ir2 R ==> 86 HSPEC P (SC ir1 ir2) R`, 87 RW_TAC std_ss [HSPEC_def] THEN 88 METIS_TAC [IR_SEMANTICS_SC] 89 ); 90 91(*---------------------------------------------------------------------------------*) 92(* Block Rule *) 93(* Block of assigment *) 94(*---------------------------------------------------------------------------------*) 95 96val BLK_EQ_SC = Q.store_thm ( 97 "BLK_EQ_SC", 98 `!stm stmL st. (run_ir (BLK (stm::stmL)) st = run_ir (SC (BLK [stm]) (BLK stmL)) st) /\ 99 (run_ir (BLK (SNOC stm stmL)) st = run_ir (SC (BLK stmL) (BLK [stm])) st)`, 100 101 REPEAT GEN_TAC THEN 102 `WELL_FORMED (BLK [stm]) /\ WELL_FORMED (BLK stmL)` by 103 METIS_TAC [BLOCK_IS_WELL_FORMED] THEN 104 STRIP_TAC THENL [ 105 `run_ir (BLK [stm]) st = mdecode st stm` by ( 106 RW_TAC list_ss [run_ir_def, run_arm_def, translate_def, Once RUNTO_ADVANCE] THEN 107 RW_TAC list_ss [GSYM uploadCode_def, UPLOADCODE_LEM] THEN 108 RW_TAC list_ss [GSYM TRANSLATE_ASSIGMENT_CORRECT, ARMCompositionTheory.get_st_def, Once RUNTO_ADVANCE] 109 ) THEN 110 RW_TAC list_ss [IR_SEMANTICS_BLK, IR_SEMANTICS_SC], 111 112 RW_TAC list_ss [SNOC_APPEND, run_ir_def, translate_def] THEN 113 `mk_SC (translate (BLK stmL)) [translate_assignment stm] = translate (BLK (stmL ++ [stm]))` by ( 114 RW_TAC list_ss [ARMCompositionTheory.mk_SC_def] THEN 115 Induct_on `stmL` THENL [ 116 RW_TAC list_ss [translate_def], 117 RW_TAC list_ss [translate_def] THEN 118 METIS_TAC [BLOCK_IS_WELL_FORMED] 119 ]) THEN 120 METIS_TAC [] 121 ] 122 ); 123 124val EMPTY_BLK_AXIOM = Q.store_thm ( 125 "EMPTY_BLK_AXIOM", 126 `!P Q. (!st. P st ==> Q st) ==> 127 HSPEC P (BLK []) Q`, 128 RW_TAC std_ss [HSPEC_def, IR_SEMANTICS_BLK] 129 ); 130 131val BLK_RULE = Q.store_thm ( 132 "BLK_RULE", 133 `!P Q R stm stmL. HSPEC Q (BLK [stm]) R /\ 134 HSPEC P (BLK stmL) Q ==> 135 HSPEC P (BLK (SNOC stm stmL)) R`, 136 RW_TAC std_ss [HSPEC_def] THEN 137 RW_TAC std_ss [BLK_EQ_SC] THEN 138 METIS_TAC [HSPEC_def, SC_RULE, BLOCK_IS_WELL_FORMED] 139 ); 140 141 142(*---------------------------------------------------------------------------------*) 143(* Conditional Jumps *) 144(*---------------------------------------------------------------------------------*) 145 146val CJ_RULE = Q.store_thm ( 147 "CJ_RULE", 148 `!P Q cond ir1 ir2 st. WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 149 HSPEC (\st.eval_il_cond cond st /\ P st) ir1 Q /\ HSPEC (\st.~eval_il_cond cond st /\ P st) ir2 Q ==> 150 HSPEC P (CJ cond ir1 ir2) Q`, 151 RW_TAC std_ss [HSPEC_def] THEN 152 METIS_TAC [IR_SEMANTICS_CJ] 153 ); 154 155 156val CJ_RULE_2 = Q.store_thm ( 157 "CJ_RULE_2", 158 `!P Q cond ir1 ir2 st. WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 159 HSPEC P ir1 Q /\ HSPEC P ir2 Q ==> 160 HSPEC P (CJ cond ir1 ir2) Q`, 161 RW_TAC std_ss [HSPEC_def] THEN 162 METIS_TAC [IR_SEMANTICS_CJ] 163 ); 164 165(*---------------------------------------------------------------------------------*) 166(* Tail Recursion *) 167(*---------------------------------------------------------------------------------*) 168 169val TR_RULE = Q.store_thm ( 170 "TR_RULE", 171 `!cond ir P Q. 172 WELL_FORMED ir /\ WF_TR (translate_condition cond, translate ir) /\ 173 HSPEC P ir P ==> HSPEC P (TR cond ir) P`, 174 RW_TAC std_ss [HSPEC_def] THEN 175 METIS_TAC [HOARE_TR_IR] 176 ); 177 178(*---------------------------------------------------------------------------------*) 179(* Well-founded Tail Recursion *) 180(*---------------------------------------------------------------------------------*) 181 182val WF_DEF_2 = Q.store_thm ( 183 "WF_DEF_2", 184 `WF R = !P. (?w. P w) ==> ?min. P min /\ !b. R b min ==> ~P b`, 185 RW_TAC std_ss [relationTheory.WF_DEF] 186 ); 187 188val WF_TR_LEM_1 = Q.store_thm ( 189 "WF_TR_LEM_1", 190 `!cond ir st. WELL_FORMED ir /\ 191 WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0)) ==> 192 WF_TR (translate_condition cond,translate ir)`, 193 194 RW_TAC std_ss [WELL_FORMED_SUB_thm, WF_TR_def, WF_Loop_def, run_ir_def, run_arm_def] THEN 195 POP_ASSUM MP_TAC THEN Q.ABBREV_TAC `arm = translate ir` THEN STRIP_TAC THEN 196 Q.EXISTS_TAC `\s1 s0. if eval_il_cond cond (get_st s0) then F else (get_st s1 = get_st (runTo (upload arm (\i. ARB) (FST (FST s0))) 197 (FST (FST s0) + LENGTH (translate ir)) s0))` THEN 198 STRIP_TAC THENL [ 199 FULL_SIMP_TAC std_ss [WF_DEF_2, GSYM RIGHT_FORALL_IMP_THM] THEN 200 STRIP_TAC THEN 201 POP_ASSUM (ASSUME_TAC o Q.SPEC `\st. ?pc cpsr pcS. (P:STATEPCS->bool) (((pc,cpsr,st),pcS):STATEPCS)`) THEN 202 STRIP_TAC THEN 203 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 204 `?st pc cpsr pcS. w = ((pc,cpsr,st),pcS)` by METIS_TAC [ABS_PAIR_THM] THEN 205 FULL_SIMP_TAC std_ss [] THEN RES_TAC THEN 206 Q.EXISTS_TAC `((pc',cpsr',st0),pcS')` THEN 207 RW_TAC std_ss [Once get_st_def] THEN RES_TAC THEN 208 `get_st (runTo (upload arm (\i. ARB) pc') (pc'+LENGTH arm) ((pc',cpsr',st0),pcS')) = 209 get_st (runTo (upload arm (\i. ARB) 0) (LENGTH arm) ((0,0w,st0),{}))` by 210 METIS_TAC [well_formed_def, get_st_def, DSTATE_IRRELEVANT_PCS, status_independent_def, FST, DECIDE (Term `!x.0 + x = x`)] THEN 211 METIS_TAC [FST,SND,get_st_def, ABS_PAIR_THM], 212 213 RW_TAC std_ss [get_st_def, eval_il_cond_def] THEN 214 METIS_TAC [WELL_FORMED_INSTB] 215 ] 216 ); 217 218val WF_TR_LEM_2 = Q.store_thm ( 219 "WF_TR_LEM_2", 220 `!cond ir prj_f f cond_f. 221 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ (!st. prj_f (run_ir ir st) = f (prj_f st)) /\ 222 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==> 223 WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0))`, 224 225 RW_TAC std_ss [WF_DEF_2] THEN 226 Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN 227 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 228 RES_TAC THEN 229 Q.EXISTS_TAC `y` THEN 230 RW_TAC std_ss [] THEN 231 `~cond_f (prj_f y)` by METIS_TAC [] THEN 232 RES_TAC THEN 233 Q.PAT_ASSUM `!t1.p` (ASSUME_TAC o Q.SPEC `prj_f (st1:DSTATE)`) THEN 234 METIS_TAC [] 235 ); 236 237val WF_TR_LEM_3 = Q.store_thm ( 238 "WF_TR_LEM_3", 239 `!cond_f f. (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) ==> 240 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0))`, 241 RW_TAC std_ss [] THEN 242 MATCH_MP_TAC WF_SUBSET THEN 243 Q.EXISTS_TAC `R` THEN 244 RW_TAC std_ss [] 245 ); 246 247val WF_TR_THM_1 = Q.store_thm ( 248 "WF_TR_THM_1", 249 `!cond ir prj_f f cond_f pre_p. 250 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ 251 (!st. pre_p st ==> (prj_f (run_ir ir st) = f (prj_f st))) /\ 252 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==> 253 WF (\st1 st0. (pre_p st0) /\ ~(eval_il_cond cond st0) /\ (st1 = run_ir ir st0))`, 254 255 RW_TAC std_ss [WF_DEF_2] THEN 256 Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN 257 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 258 RES_TAC THEN 259 Q.EXISTS_TAC `y` THEN 260 RW_TAC std_ss [] THEN 261 `~cond_f (prj_f y)` by METIS_TAC [] THEN 262 RES_TAC THEN 263 Q.PAT_ASSUM `!y1.p` (ASSUME_TAC o Q.SPEC `prj_f (run_ir ir y)`) THEN 264 METIS_TAC [] 265 ); 266 267(*---------------------------------------------------------------------------------*) 268(* Hoare Rules on Projection on Inputs and Ouputs (represented *) 269(* by projective functions *) 270(* The pre-conditions and post-conditions (on data other than inputs and *) 271(* outputs) are also specified *) 272(*---------------------------------------------------------------------------------*) 273 274val PSPEC_def = Define ` 275 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) = 276 !v x. HSPEC (\st. pre_p st /\ (stk_f st = x) /\ (in_f st = v)) 277 ir (\st. post_p st /\ (stk_f st = x) /\ (out_f st = f v))`; 278 279val _ = type_abbrev("PSPEC_TYPE", type_of (Term `PSPEC`)); 280 281val PSPEC_STACK = Q.store_thm ( 282 "PSPEC_STACK", 283 `!ir pre_p post_p stk_f in_f f out_f x. 284 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 285 ==> 286 HSPEC (\st. pre_p st /\ (stk_f st = x)) ir (\st. post_p st /\ (stk_f st = x))`, 287 RW_TAC std_ss [PSPEC_def, HSPEC_def] 288 ); 289 290val PSPEC_CHARACTERISTIC = Q.store_thm ( 291 "PSPEC_CHARACTERISTIC", 292 `!ir pre_p post_p stk_f in_f f out_f. 293 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 294 ==> 295 HSPEC (\st. pre_p st /\ (in_f st = v)) ir (\st. post_p st /\ (out_f st = f v))`, 296 RW_TAC std_ss [PSPEC_def, HSPEC_def] 297 ); 298 299val PRJ_SHUFFLE_RULE = Q.store_thm ( 300 "PRJ_SHUFFLE_RULE", 301 `!ir pre_p post_p stk_f in_f f out_f shuffle_f. 302 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 303 ==> 304 PSPEC ir (pre_p, post_p) stk_f (in_f, shuffle_f o f, shuffle_f o out_f)`, 305 RW_TAC std_ss [PSPEC_def, HSPEC_def] 306 ); 307 308val PRJ_SHUFFLE_RULE2 = Q.store_thm ( 309 "PRJ_SHUFFLE_RULE2", 310 `!ir pre_p post_p stk_f in_f f out_f g in_f'. 311 PSPEC ir (pre_p, post_p) stk_f (in_f, f, out_f) /\ (g o in_f' = f o in_f) 312 ==> 313 PSPEC ir (pre_p,post_p) stk_f (in_f', g, out_f)`, 314 RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN 315 METIS_TAC [FUN_EQ_THM, combinTheory.o_THM] 316 ); 317 318val PRJ_SC_RULE = Q.store_thm ( 319 "PRJ_SC_RULE", 320 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2. 321 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 322 PSPEC ir1 (pre_p1,post_p1) stk_f (in_f1,f1,out_f1) /\ PSPEC ir2 (post_p1,post_p2) stk_f (out_f1,f2,out_f2) 323 ==> 324 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`, 325 326 RW_TAC std_ss [PSPEC_def] THEN 327 METIS_TAC [SC_RULE] 328 ); 329 330val PRJ_CJ_RULE = Q.store_thm ( 331 "PRJ_CJ_RULE", 332 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f. 333 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 334 PSPEC ir_t (pre_p,post_p) stk_f (in_f,f1,out_f) /\ 335 PSPEC ir_f (pre_p, post_p) stk_f (in_f,f2,out_f) /\ (!st. cond_f (in_f st) = eval_il_cond cond st) 336 ==> 337 PSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk_f (in_f, (\v.if cond_f v then f1 v else f2 v), out_f)`, 338 339 RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN 340 METIS_TAC [IR_SEMANTICS_CJ] 341 ); 342 343(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *) 344val PRJ_TR_RULE = Q.store_thm ( 345 "PRJ_TR_RULE", 346 `!cond ir pre_p stk_f cond_f prj_f f. 347 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0)) /\ 348 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ PSPEC ir (pre_p,pre_p) stk_f (prj_f,f,prj_f) ==> 349 PSPEC (TR cond ir) (pre_p,pre_p) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`, 350 351 RW_TAC std_ss [PSPEC_def] THEN 352 RW_TAC std_ss [HSPEC_def] THENL [ 353 FULL_SIMP_TAC std_ss [HSPEC_def] THEN 354 METIS_TAC [SIMP_RULE std_ss [HSPEC_def] TR_RULE, WF_TR_LEM_1], 355 356 IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_STACK) THEN 357 POP_ASSUM (ASSUME_TAC o Q.SPEC `(stk_f:DSTATE->'a) st`) THEN 358 IMP_RES_TAC WF_TR_LEM_1 THEN 359 IMP_RES_TAC (Q.SPECL [`cond`,`ir`,`\st1. pre_p st1 /\ ((stk_f:DSTATE->'a) 360 st1 = (stk_f:DSTATE->'a) st)`] TR_RULE) THEN 361 POP_ASSUM (ASSUME_TAC o Q.SPEC `st` o SIMP_RULE std_ss [HSPEC_def]) THEN 362 METIS_TAC [], 363 364 IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_CHARACTERISTIC) THEN 365 Q.PAT_ASSUM `!v x.p` (K ALL_TAC) THEN 366 `WF_TR (translate_condition cond,translate ir)` by METIS_TAC [WF_TR_LEM_1] THEN 367 FULL_SIMP_TAC std_ss [WELL_FORMED_SUB_thm, HSPEC_def, run_ir_def, run_arm_def, translate_def, eval_il_cond_def] THEN 368 Q.ABBREV_TAC `arm = translate ir` THEN 369 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`translate_condition cond`,`arm`,`(\i. ARB)`,`(0,0w,st):STATE`,`{}`] 370 ARMCompositionTheory.UNROLL_TR_LEM)) THEN 371 POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN 372 FULL_SIMP_TAC std_ss [FUNPOW, ARMCompositionTheory.get_st_def] THEN 373 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 374 Induct_on `loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,st),{})` THENL [ 375 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW,ARMCompositionTheory.get_st_def] THEN 376 IMP_RES_TAC ARMCompositionTheory.LOOPNUM_BASIC THEN 377 FULL_SIMP_TAC arith_ss [Once WHILE, ARMCompositionTheory.get_st_def], 378 379 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW] THEN 380 IMP_RES_TAC ARMCompositionTheory.LOOPNUM_INDUCTIVE THEN 381 `v = loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,SND (SND (FST (runTo (upload arm (\i.ARB) 0) (LENGTH arm) 382 ((0,0w,st),{}))))),{})` by METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`), 383 ARMCompositionTheory.LOOPNUM_INDEPENDENT_OF_CPSR_PCS, ARMCompositionTheory.get_st_def, 384 FST, SND, ARMCompositionTheory.DSTATE_IRRELEVANT_PCS,ARMCompositionTheory.well_formed_def] THEN 385 RES_TAC THEN Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN 386 FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 387 Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 388 Q.PAT_ASSUM `~x` (ASSUME_TAC o SIMP_RULE std_ss [ARMCompositionTheory.get_st_def]) THEN 389 RW_TAC std_ss [Once WHILE] THEN 390 Q.UNABBREV_TAC `arm` THEN 391 `run_ir ir st = SND (SND (FST (runTo (upload (translate ir) (\i. ARB) 0) (LENGTH (translate ir)) 392 ((0,0w,st),{}))))` by RW_TAC arith_ss [ 393 ARMCompositionTheory.get_st_def, run_ir_def, run_arm_def] THEN 394 METIS_TAC [SND,FST,ARMCompositionTheory.get_st_def,ARMCompositionTheory.FUNPOW_DSTATE, ABS_PAIR_THM] 395 ] 396 ] 397 ); 398 399val PRJ_TR_RULE_2 = Q.store_thm ( 400 "PRJ_TR_RULE_2", 401 `!cond ir stk_f cond_f prj_f f. 402 WELL_FORMED ir /\ (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ 403 (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) /\ 404 PSPEC ir ((\st.T),(\st.T)) stk_f (prj_f,f,prj_f) ==> 405 PSPEC (TR cond ir) ((\st.T),(\st.T)) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`, 406 407 SIMP_TAC std_ss [PSPEC_def, HSPEC_def] THEN 408 REPEAT GEN_TAC THEN NTAC 2 STRIP_TAC THEN 409 `WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0))` by METIS_TAC [WF_TR_LEM_2, WF_TR_LEM_3] THEN 410 METIS_TAC [SIMP_RULE std_ss [PSPEC_def, HSPEC_def] (Q.SPECL [`cond`,`ir`,`\st.T`] PRJ_TR_RULE)] 411 ); 412 413 414(*---------------------------------------------------------------------------------*) 415(* Rules for Conditions (projective function version) *) 416(*---------------------------------------------------------------------------------*) 417 418val PRJ_STRENGTHEN_RULE = Q.store_thm ( 419 "PRJ_STRENGTHEN_RULE", 420 `!ir pre_p pre_p' post_p stk_f in_f f out_f. 421 WELL_FORMED ir /\ 422 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. pre_p' st ==> pre_p st) ==> 423 PSPEC ir (pre_p',post_p) stk_f (in_f,f,out_f)`, 424 RW_TAC std_ss [PSPEC_def, HSPEC_def] 425 ); 426 427val PRJ_WEAKEN_RULE = Q.store_thm ( 428 "PRJ_WEAKEN_RULE", 429 `!ir pre_p post_p post_p' stk_f in_f f out_f. 430 WELL_FORMED ir /\ 431 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. post_p st ==> post_p' st) ==> 432 PSPEC ir (pre_p,post_p') stk_f (in_f,f,out_f)`, 433 RW_TAC std_ss [PSPEC_def, HSPEC_def] 434 ); 435 436(*---------------------------------------------------------------------------------*) 437(* Rules for Stack (projective function version) *) 438(*---------------------------------------------------------------------------------*) 439 440val valid_push_def = Define ` 441 valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f') = 442 !st st'. (stk_f st' = stk_f st) /\ (out_f st' = f (in_f st)) ==> 443 (stk_f' st' = stk_f' st) /\ (out_f' st' = g (in_f' st))`; 444 445val PRJ_POP_RULE = Q.store_thm ( 446 "PRJ_POP_RULE", 447 `!ir pre_p post_p stk_f in_f f out_f stk_f' in_f' g out_f'. 448 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ 449 valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f') 450 ==> 451 PSPEC ir (pre_p,post_p) stk_f' (in_f', g, out_f')`, 452 RW_TAC list_ss [PSPEC_def, HSPEC_def, valid_push_def] 453 ); 454 455val P_intact_def = Define ` 456 P_intact (P,Q) (stk_f,stk_g) = 457 !st st'. (stk_f st' = stk_f st) /\ P st /\ Q st' 458 ==> (stk_g st' = stk_g st)`; 459 460val PRJ_PUSH_RULE = Q.store_thm ( 461 "PRJ_PUSH_RULE", 462 `!ir pre_p post_p stk_f in_f f out_f e_f stk_g. 463 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ 464 P_intact (pre_p,post_p) (stk_f,stk_g) 465 ==> PSPEC ir (pre_p,post_p) stk_g (in_f, f, out_f)`, 466 RW_TAC list_ss [PSPEC_def, HSPEC_def, P_intact_def] 467 ); 468 469(*---------------------------------------------------------------------------------*) 470(* Hoare Rules on Projection on Inputs and Ouputs (represented by vectors) *) 471(* To overcome the type restriction on tuples in HOL definitions *) 472(*---------------------------------------------------------------------------------*) 473 474(* Vectors *) 475 476val _ = Hol_datatype ` 477 VEXP = SG of DATA (* registers *) 478 | VT of VEXP # VEXP (* pairs *) 479 `; 480 481val readv_def = Define ` 482 (readv st (PR (a,b)) = VT (readv st a, readv st b)) /\ 483 (readv st x = SG (mread st x))`; 484 485 486(* Vector Stack, modelled as a list of expression vectors *) 487 488val push_def = Define ` 489 push x stk = x :: stk`; 490 491val top_def = Define ` 492 top = HD`; 493 494val pop_def = Define ` 495 pop = TL`; 496 497(* Specification on vectors *) 498 499val VSPEC_def = Define ` 500 VSPEC ir (pre_p,post_p) stk (iv,f,ov) = 501 PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov)) 502 `; 503 504val _ = type_abbrev("VSPEC_TYPE", type_of (Term `VSPEC`)); 505 506val V_SHUFFLE_RULE = Q.store_thm ( 507 "V_SHUFFLE_RULE", 508 `!ir stk iv f ov g iv'. 509 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv)) 510 ==> 511 VSPEC ir (pre_p,post_p) stk (iv', g, ov)`, 512 RW_TAC std_ss [VSPEC_def, PSPEC_def, HSPEC_def] 513 ); 514 515val V_SC_RULE = Q.store_thm ( 516 "V_SC_RULE", 517 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2. 518 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 519 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2) 520 ==> 521 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`, 522 RW_TAC std_ss [VSPEC_def] THEN 523 METIS_TAC [PRJ_SC_RULE] 524 ); 525 526val V_CJ_RULE = Q.store_thm ( 527 "V_CJ_RULE", 528 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov. 529 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 530 VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\ 531 VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st) 532 ==> 533 VSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk (iv, (\v.if cond_f v then f1 v else f2 v), ov)`, 534 RW_TAC std_ss [VSPEC_def] THEN 535 FULL_SIMP_TAC std_ss [PRJ_CJ_RULE] 536 ); 537 538(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *) 539 540val V_TR_RULE = Q.store_thm ( 541 "V_TR_RULE", 542 `!cond ir pre_p stk cond_f iv f. 543 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0)) /\ 544 (!st. cond_f (readv st iv) = eval_il_cond cond st) /\ VSPEC ir (pre_p,pre_p) stk (iv,f,iv) ==> 545 VSPEC (TR cond ir) (pre_p,pre_p) stk (iv, WHILE ($~ o cond_f) f, iv)`, 546 547 RW_TAC std_ss [VSPEC_def] THEN 548 FULL_SIMP_TAC std_ss [PRJ_TR_RULE] 549 ); 550 551(*---------------------------------------------------------------------------------*) 552(* Rules for Conditions (vector version) *) 553(*---------------------------------------------------------------------------------*) 554 555val V_STRENGTHEN_RULE = Q.store_thm ( 556 "V_STRENGTHEN_RULE", 557 `!ir pre_p pre_p' post_p stk iv f ov. 558 WELL_FORMED ir /\ 559 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. pre_p' st ==> pre_p st) ==> 560 VSPEC ir (pre_p',post_p) stk (iv,f,ov)`, 561 RW_TAC std_ss [VSPEC_def] THEN 562 METIS_TAC [PRJ_STRENGTHEN_RULE] 563 ); 564 565val V_WEAKEN_RULE = Q.store_thm ( 566 "V_WEAKEN_RULE", 567 `!ir pre_p post_p post_p' stk iv f ov. 568 WELL_FORMED ir /\ 569 PSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. post_p st ==> post_p' st) ==> 570 PSPEC ir (pre_p,post_p') stk (iv,f,ov)`, 571 RW_TAC std_ss [VSPEC_def] THEN 572 METIS_TAC [PRJ_WEAKEN_RULE] 573 ); 574 575(*---------------------------------------------------------------------------------*) 576(* Rules for Stack (vector version) *) 577(*---------------------------------------------------------------------------------*) 578 579val V_POP_RULE = Q.store_thm ( 580 "V_POP_RULE", 581 `!ir pre_p post_p stk iv f ov e g. 582 VSPEC ir (pre_p,post_p) (e::stk) (iv,f,ov) /\ 583 (!st. g (readv st (PR(iv,e))) = VT (f (readv st iv), readv st e)) ==> 584 VSPEC ir (pre_p,post_p) stk (PR(iv,e), g, PR(ov,e))`, 585 RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, readv_def] 586 ); 587 588val V_intact_def = Define ` 589 V_intact (P,Q,e) = 590 ?x. (!st.P st ==> (readv st e = x)) /\ (!st.Q st ==> (readv st e = x))`; 591 592 593val V_PUSH_RULE = Q.store_thm ( 594 "V_PUSH_RULE", 595 `!ir pre_p post_p stk iv f ov e. 596 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ V_intact(pre_p, post_p, e) 597 ==> 598 VSPEC ir (pre_p,post_p) (e::stk) (iv, f, ov)`, 599 RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, V_intact_def, readv_def] THEN 600 METIS_TAC [] 601 ); 602 603 604(*---------------------------------------------------------------------------------*) 605(* Rules for Well-formedness *) 606(*---------------------------------------------------------------------------------*) 607 608val WELL_FORMED_TR_RULE = Q.store_thm ( 609 "WELL_FORMED_TR_RULE", 610 `!cond ir context_f. 611 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_ir ir st0)) ==> 612 WELL_FORMED (TR cond ir)`, 613 614 RW_TAC std_ss [] THEN 615 METIS_TAC [IR_TR_IS_WELL_FORMED, WF_TR_LEM_1] 616 ); 617 618 619 620val IR_CJ_UNCHANGED = store_thm ("IR_CJ_UNCHANGED", 621``!cond ir_t ir_f s. 622 (WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 623 UNCHANGED s ir_t /\ UNCHANGED s ir_f) ==> 624 UNCHANGED s (CJ cond ir_t ir_f)``, 625 626 627REWRITE_TAC[UNCHANGED_def] THEN 628REPEAT STRIP_TAC THEN 629ASM_SIMP_TAC std_ss [SEMANTICS_OF_IR] THEN 630PROVE_TAC[]); 631 632 633val IR_SC_UNCHANGED = store_thm ("IR_SC_UNCHANGED", 634``!ir1 ir2 s. 635 (WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 636 UNCHANGED s ir1 /\ UNCHANGED s ir2) ==> 637 UNCHANGED s (SC ir1 ir2)``, 638 639 640REWRITE_TAC[UNCHANGED_def] THEN 641REPEAT STRIP_TAC THEN 642ASM_SIMP_TAC std_ss [SEMANTICS_OF_IR] THEN 643PROVE_TAC[]) 644 645val UNCHANGED_TR_RULE = store_thm ("UNCHANGED_TR_RULE", 646``!c ir s. 647 (WELL_FORMED (TR c ir) /\ UNCHANGED s ir) ==> 648 UNCHANGED s (TR c ir)``, 649 650 REWRITE_TAC [UNCHANGED_def, WELL_FORMED_def] THEN 651 REPEAT STRIP_TAC THEN 652 ASM_SIMP_TAC std_ss [IR_SEMANTICS_TR___FUNPOW] THEN 653 Q.ABBREV_TAC `n = (shortest (eval_il_cond c) (run_ir ir) st)` THEN 654 POP_ASSUM (fn x => ALL_TAC) THEN 655 Induct_on `n` THENL [ 656 REWRITE_TAC[FUNPOW], 657 REWRITE_TAC[FUNPOW_SUC] THEN PROVE_TAC[] 658 ]); 659 660 661 662 663val IR_CJ_USED_STACK = store_thm ("IR_CJ_USED_STACK", 664``!cond ir_t ir_f s s'. 665 (WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 666 USED_STACK s' ir_f /\ USED_STACK s ir_t) ==> 667 USED_STACK (MAX s s') (CJ cond ir_t ir_f)``, 668 669 670REPEAT STRIP_TAC THEN 671`(s <= MAX s s') /\ (s' <= MAX s s')` by SIMP_TAC arith_ss [] THEN 672`(USED_STACK (MAX s s') ir_f) /\ 673 (USED_STACK (MAX s s') ir_t)` by PROVE_TAC [USED_STACK_ENLARGE] THEN 674 675FULL_SIMP_TAC std_ss [USED_STACK_THM, SEMANTICS_OF_IR] THEN 676METIS_TAC[]) 677 678 679val IR_CJ_UNCHANGED_STACK = store_thm ("IR_CJ_UNCHANGED_STACK", 680``!cond ir_t ir_f l s s'. 681 (WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 682 UNCHANGED_STACK l s' ir_f /\ UNCHANGED_STACK l s ir_t) ==> 683 UNCHANGED_STACK l (MAX s s') (CJ cond ir_t ir_f)``, 684 685SIMP_TAC std_ss [UNCHANGED_STACK_def, IR_CJ_USED_STACK, IR_CJ_UNCHANGED]) 686 687 688 689val IR_SC_USED_STACK = store_thm ("IR_SC_USED_STACK", 690``!x ir1 ir2 s s'. 691 (WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 692 USED_STACK s ir1 /\ USED_STACK s' ir2 /\ 693 (s' + x < 2**30) /\ (s < 2**30) /\ 694 (!r m. read (run_ir ir1 (r,m)) (REG 13) = 695 read (r,m) (REG 13) - n2w (4*x))) ==> 696 USED_STACK (MAX s (s'+x)) (SC ir1 ir2)``, 697 698 699 REPEAT STRIP_TAC THEN 700 FULL_SIMP_TAC std_ss [USED_STACK_THM, SEMANTICS_OF_IR] THEN 701 REPEAT STRIP_TAC THEN 702 703 `read (run_ir ir1 (r,m)) (REG 13) = (read (r,m) (REG 13) - (n2w (4*x)))` by METIS_TAC[] THEN 704 `?r'' m''. run_ir ir1 (r,m) = (r'',m'')` by METIS_TAC[pairTheory.PAIR] THEN 705 FULL_SIMP_TAC std_ss [toREG_def, read_thm, index_of_reg_def, MEM_MAP, MEM_LIST_COUNT] THEN 706 `m ' l = m'' ' l` by METIS_TAC[] THEN 707 ASM_SIMP_TAC std_ss [] THEN 708 RES_TAC THEN 709 POP_ASSUM MATCH_MP_TAC THEN 710 FULL_SIMP_TAC arith_ss [word_sub_def, word_2comp_n2w, dimword_32, 711 dimword_30] THEN 712 GEN_TAC THEN 713 Q.PAT_ASSUM `!off:num. P off` (fn thm => MP_TAC 714 (SPEC ``(off:num) + (x:num)`` thm)) THEN 715 Cases_on `off < s'` THEN ASM_REWRITE_TAC[] THEN 716 ONCE_REWRITE_TAC [prove(``(4294967296:num - 4 * x) = (1073741824 - x)*4``, DECIDE_TAC)] THEN 717 ASM_SIMP_TAC arith_ss [MEM_ADDR_ADD_CONST_MULT, GSYM WORD_ADD_ASSOC, word_add_n2w] THEN 718 ONCE_REWRITE_TAC[GSYM n2w_mod] THEN 719 SIMP_TAC arith_ss [dimword_30, dimword_4] THEN 720 `((2147483648 - (off + x)) = 721 (1073741824 + (1073741824 - (off + x))))` by DECIDE_TAC THEN 722 ASM_SIMP_TAC std_ss [ADD_MODULUS_RIGHT]) 723 724 725 726 727 728val IR_SC_USED_STACK = store_thm ("IR_SC_USED_STACK", 729``!x y ir1 ir2 s s'. 730 (WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 731 USED_STACK s ir1 /\ USED_STACK s' ir2 /\ 732 (s' + x < 2**30) /\ (s < 2**30) /\ (y <= x) /\ 733 (!r m. read (run_ir ir1 (r,m)) (REG 13) = 734 read (r,m) (REG 13) - n2w (4*y))) ==> 735 USED_STACK (MAX s (s'+x)) (SC ir1 ir2)``, 736 737 REPEAT STRIP_TAC THEN 738 FULL_SIMP_TAC std_ss [USED_STACK_THM, SEMANTICS_OF_IR] THEN 739 REPEAT STRIP_TAC THEN 740 741 `read (run_ir ir1 (r,m)) (REG 13) = (read (r,m) (REG 13) - (n2w (4*y)))` by METIS_TAC[] THEN 742 `?r'' m''. run_ir ir1 (r,m) = (r'',m'')` by METIS_TAC[pairTheory.PAIR] THEN 743 FULL_SIMP_TAC std_ss [toREG_def, read_thm, index_of_reg_def, MEM_MAP, MEM_LIST_COUNT] THEN 744 `m ' l = m'' ' l` by METIS_TAC[] THEN 745 ASM_SIMP_TAC std_ss [] THEN 746 RES_TAC THEN 747 POP_ASSUM MATCH_MP_TAC THEN 748 FULL_SIMP_TAC arith_ss [word_sub_def, word_2comp_n2w, dimword_32, 749 dimword_30] THEN 750 GEN_TAC THEN 751 Q.PAT_ASSUM `!off:num. P off` (fn thm => MP_TAC 752 (SPEC ``(off:num) + (y:num)`` thm)) THEN 753 Cases_on `off < s'` THEN ASM_REWRITE_TAC[] THEN 754 ONCE_REWRITE_TAC [prove(``(4294967296:num - 4 * y) = (1073741824 - y)*4``, DECIDE_TAC)] THEN 755 ASM_SIMP_TAC arith_ss [MEM_ADDR_ADD_CONST_MULT, GSYM WORD_ADD_ASSOC, word_add_n2w] THEN 756 ONCE_REWRITE_TAC[GSYM n2w_mod] THEN 757 SIMP_TAC arith_ss [dimword_30, dimword_4] THEN 758 `((2147483648 - (off + y)) = 759 (1073741824 + (1073741824 - (off + y))))` by DECIDE_TAC THEN 760 ASM_SIMP_TAC std_ss [ADD_MODULUS_RIGHT]) 761 762 763 764val IR_SC_USED_STACK___FC_CASE1 = store_thm ("IR_SC_USED_STACK___FC_CASE1", 765``!ir1 ir2 s s' s''. 766 (USED_STACK (s+s') ir1 /\ (USED_STACK s'' ir2 /\ 767 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 768 (s + s' + s'' < 2**30) /\ 769 (!r m. read (run_ir ir1 (r,m)) (REG 13) = 770 read (r,m) (REG 13) - n2w (4*s)))) ==> 771 USED_STACK (s+s'+s'') (SC ir1 ir2)``, 772 773 REPEAT STRIP_TAC THEN 774 `(s:num) + s' + s'' = MAX (s+s') (s'' + (s+s'))` by ALL_TAC THEN1 ( 775 SIMP_TAC arith_ss [MAX_DEF] 776 ) THEN 777 ASM_REWRITE_TAC[] THEN 778 MATCH_MP_TAC IR_SC_USED_STACK THEN 779 Q_TAC EXISTS_TAC `s` THEN 780 FULL_SIMP_TAC std_ss []) 781 782 783val IR_SC_USED_STACK___FC_CASE2 = store_thm ("IR_SC_USED_STACK___FC_CASE2", 784``!ir1 ir2 s s'. 785 (USED_STACK s ir1 /\ (USED_STACK s' ir2 /\ 786 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 787 (s + s' < 2**30) /\ 788 (!r m. read (run_ir ir1 (r,m)) (REG 13) = 789 read (r,m) (REG 13) - n2w (4*s)))) ==> 790 USED_STACK (s+s') (SC ir1 ir2)``, 791 792 REPEAT STRIP_TAC THEN 793 `(s:num) + s' = MAX s (s' + s)` by ALL_TAC THEN1 ( 794 SIMP_TAC std_ss [MAX_DEF] THEN 795 Cases_on `0 < s'` THEN ASM_SIMP_TAC arith_ss [] 796 ) THEN 797 ASM_REWRITE_TAC[] THEN 798 MATCH_MP_TAC IR_SC_USED_STACK THEN 799 Q_TAC EXISTS_TAC `s` THEN 800 FULL_SIMP_TAC std_ss []) 801 802 803val IR_SC_UNCHANGED_STACK = store_thm ("IR_SC_UNCHANGED_STACK", 804``!ir1 ir2 l s s'. 805 (WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 806 UNCHANGED_STACK l s ir1 /\ UNCHANGED_STACK l s' ir2 /\ 807 MEM R13 l) ==> 808 UNCHANGED_STACK l (MAX s s') (SC ir1 ir2)``, 809 810 811 SIMP_TAC std_ss [UNCHANGED_STACK_def, IR_SC_UNCHANGED] THEN 812 REPEAT STRIP_TAC THEN 813 `(s <= MAX s s') /\ (s' <= MAX s s')` by SIMP_TAC arith_ss [] THEN 814 `(USED_STACK (MAX s s') ir1) /\ 815 (USED_STACK (MAX s s') ir2)` by PROVE_TAC [USED_STACK_ENLARGE] THEN 816 FULL_SIMP_TAC std_ss [USED_STACK_THM, UNCHANGED_THM, EVERY_MEM, 817 SEMANTICS_OF_IR] THEN 818 REPEAT STRIP_TAC THEN 819 820 FULL_SIMP_TAC std_ss [read_thm] THEN 821 `(read (r,m) (toREG R13) = 822 read (run_ir ir1 (r,m)) (toREG R13))` by METIS_TAC[] THEN 823 `?r'' m''. run_ir ir1 (r,m) = (r'',m'')` by METIS_TAC[pairTheory.PAIR] THEN 824 FULL_SIMP_TAC std_ss [toREG_def, read_thm, index_of_reg_def] THEN 825 METIS_TAC[]) 826 827val UNCHANGED_STACK_TR_RULE = store_thm ("UNCHANGED_STACK_TR_RULE", 828``!c ir l s. 829 (WELL_FORMED (TR c ir) /\ UNCHANGED_STACK l s ir /\ MEM R13 l) ==> 830 UNCHANGED_STACK l s (TR c ir)``, 831 832 833 SIMP_TAC std_ss [UNCHANGED_STACK_def] THEN 834 REPEAT GEN_TAC THEN 835 MATCH_MP_TAC (prove (``((X ==> A) /\ (X /\ A ==> b)) ==> (X ==> (A /\ b))``, METIS_TAC[])) THEN 836 STRIP_TAC THEN1 SIMP_TAC std_ss [UNCHANGED_TR_RULE] THEN 837 SIMP_TAC std_ss [UNCHANGED_THM, EVERY_MEM, WELL_FORMED_def] THEN 838 REPEAT STRIP_TAC THEN 839 SIMP_TAC std_ss [USED_STACK_THM] THEN 840 NTAC 2 GEN_TAC THEN 841 842 `read (r,m) (toREG R13) = read (run_ir (TR c ir) (r,m)) (toREG R13)` by PROVE_TAC[] THEN 843 POP_ASSUM MP_TAC THEN 844 POP_ASSUM (fn thm => ALL_TAC) THEN 845 `!st. read (run_ir ir st) (toREG R13) = read st (toREG R13)` by PROVE_TAC[pairTheory.PAIR] THEN 846 POP_ASSUM MP_TAC THEN 847 Q.PAT_ASSUM `!r. MEM r l ==> P r` (fn thm => ALL_TAC) THEN 848 ASM_SIMP_TAC std_ss [IR_SEMANTICS_TR___FUNPOW, toREG_def, index_of_reg_def] THEN 849 Q.ABBREV_TAC `n = (shortest (eval_il_cond c) (run_ir ir) (r, m))` THEN 850 POP_ASSUM (fn x => ALL_TAC) THEN 851 FULL_SIMP_TAC std_ss [USED_STACK_THM] THEN 852 REPEAT DISCH_TAC THEN 853 Induct_on `n` THENL [ 854 SIMP_TAC std_ss [FUNPOW], 855 856 ASM_SIMP_TAC std_ss [FUNPOW_SUC] THEN 857 REPEAT STRIP_TAC THEN 858 `?r'' m''. (FUNPOW (run_ir ir) n (r,m)) = (r'',m'')` by METIS_TAC[pairTheory.PAIR] THEN 859 FULL_SIMP_TAC std_ss [read_thm] THEN 860 METIS_TAC[] 861 ]); 862 863 864val UNCHANGED_STACK___READ_STACK_IMP = 865 store_thm ("UNCHANGED_STACK___READ_STACK_IMP", 866``!s st l ir n. ((0 < n) /\ (n + l < 2**30) /\ MEM R13 s) ==> 867(UNCHANGED_STACK s l ir ==> 868(read (run_ir ir st) (toMEM (R13, POS n)) = read st (toMEM (R13, POS n))))``, 869 870REPEAT STRIP_TAC THEN 871`read (run_ir ir st) (REG 13) = read st (REG 13)` by ALL_TAC THEN1 ( 872 FULL_SIMP_TAC std_ss [UNCHANGED_STACK_def, UNCHANGED_THM, EVERY_MEM] THEN 873 RES_TAC THEN 874 Cases_on `st` THEN 875 FULL_SIMP_TAC std_ss [toREG_def, index_of_reg_def] 876) THEN 877 878`?r m. run_ir ir st = (r, m)` by METIS_TAC[pairTheory.PAIR] THEN 879Cases_on `st` THEN 880FULL_SIMP_TAC std_ss [toMEM_def, index_of_reg_def, read_thm, 881 UNCHANGED_STACK_def, USED_STACK_def, MEM_MAP, MEM_LIST_COUNT] THEN 882Q.PAT_ASSUM `!r''. P r''` (fn thm => MP_TAC (SPECL [ 883 ``q:REGISTER |-> DATA``, 884 ``r':ADDR |-> DATA``, 885 ``r:REGISTER |-> DATA``, 886 ``m:ADDR |-> DATA``] thm)) THEN 887ASM_SIMP_TAC std_ss [prove (``(a \/ b) = (~a ==> b)``, PROVE_TAC[])] THEN 888STRIP_TAC THEN 889POP_ASSUM (fn thm => MATCH_MP_TAC (GSYM thm)) THEN 890GEN_TAC THEN 891SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL, word_sub_def, word_2comp_n2w, 892 n2w_11, dimword_30] THEN 893Cases_on `off < l` THEN ASM_SIMP_TAC std_ss [] THEN 894Cases_on `off = 0` THEN 895ASM_SIMP_TAC arith_ss []) 896 897val _ = export_theory(); 898