1(* interactive use: 2 3quietdec := true; 4loadPath := (concat Globals.HOLDIR "/examples/dev/sw") :: !loadPath; 5 6app load ["numLib", "relationTheory", "arithmeticTheory", "preARMTheory", "pairTheory", 7 "pred_setSimps", "pred_setTheory", "listTheory", "rich_listTheory", "whileTheory", "ARMCompositionTheory", 8 "CFLTheory"]; 9 10quietdec := false; 11*) 12 13 14open HolKernel Parse boolLib bossLib numLib relationTheory arithmeticTheory preARMTheory pairTheory 15 pred_setSimps pred_setTheory listTheory rich_listTheory whileTheory ARMCompositionTheory CFLTheory; 16 17 18val _ = new_theory "CFL_Rules"; 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 30val _ = Globals.priming := NONE; 31 32(*---------------------------------------------------------------------------------*) 33(* read from an data state *) 34(*---------------------------------------------------------------------------------*) 35 36val _ = Hol_datatype ` 37 REXP = RR of MREG 38 | RM of MMEM 39 | RC of DATA 40 | PR of REXP # REXP 41 `; 42 43val mread_def = Define ` 44 (mread st (RR r) = read st (toREG r)) /\ 45 (mread st (RM m) = read st (toMEM m)) /\ 46 (mread st (RC c) = c)`; 47 48val _ = add_rule {term_name = "mread", fixity = Suffix 60, 49 pp_elements = [TOK "<", TM, TOK ">"], 50 paren_style = OnlyIfNecessary, 51 block_style = (AroundSameName, (PP.INCONSISTENT, 0))} handle HOL_ERR e => print (#message e); 52 53 54(*---------------------------------------------------------------------------------*) 55(* The fp and sp point to the default positions *) 56(*---------------------------------------------------------------------------------*) 57 58val proper_def = Define ` 59 proper = (\(regs,mem):DSTATE. (regs ' 11 = 100w) /\ (regs ' 13 = 100w))`; 60 61 62(*---------------------------------------------------------------------------------*) 63(* Hoare Logic Style Specification *) 64(*---------------------------------------------------------------------------------*) 65 66val HSPEC_def = Define ` 67 HSPEC P S_cfl Q = !st. P st ==> Q (run_cfl S_cfl st)`; 68 69val _ = type_abbrev("HSPEC_TYPE", type_of (Term `HSPEC`)); 70 71(* 72val _ = add_rule {term_name = "HSPEC", 73 fixity = Infix (HOLgrammars.RIGHT, 3), 74 pp_elements = [HardSpace 1, TOK "(", TM, TOK ")", HardSpace 1], 75 paren_style = OnlyIfNecessary, 76 block_style = (AroundEachPhrase, 77 (PP.INCONSISTENT, 0))}; 78*) 79 80(*---------------------------------------------------------------------------------*) 81(* Sequential Composition *) 82(*---------------------------------------------------------------------------------*) 83 84val CFL_SC_RULE = Q.store_thm ( 85 "CFL_SC_RULE", 86 `!P Q R S1 S2. WELL_FORMED S1 /\ WELL_FORMED S2 /\ 87 HSPEC P S1 Q /\ HSPEC Q S2 R ==> 88 HSPEC P (SC S1 S2) R`, 89 RW_TAC std_ss [HSPEC_def] THEN 90 METIS_TAC [CFL_SEMANTICS_SC] 91 ); 92 93(*---------------------------------------------------------------------------------*) 94(* Block Rule *) 95(* Block of assigment *) 96(*---------------------------------------------------------------------------------*) 97 98val BLK_EQ_SC = Q.store_thm ( 99 "BLK_EQ_SC", 100 `!stm stmL st. (run_cfl (BLK (stm::stmL)) st = run_cfl (SC (BLK [stm]) (BLK stmL)) st) /\ 101 (run_cfl (BLK (SNOC stm stmL)) st = run_cfl (SC (BLK stmL) (BLK [stm])) st)`, 102 103 REPEAT GEN_TAC THEN 104 `WELL_FORMED (BLK [stm]) /\ WELL_FORMED (BLK stmL)` by 105 METIS_TAC [BLOCK_IS_WELL_FORMED] THEN 106 STRIP_TAC THENL [ 107 `run_cfl (BLK [stm]) st = mdecode st stm` by ( 108 RW_TAC list_ss [run_cfl_def, run_arm_def, translate_def, Once RUNTO_ADVANCE] THEN 109 RW_TAC list_ss [GSYM uploadCode_def, UPLOADCODE_LEM] THEN 110 RW_TAC list_ss [GSYM TRANSLATE_ASSIGMENT_CORRECT, ARMCompositionTheory.get_st_def, Once RUNTO_ADVANCE] 111 ) THEN 112 RW_TAC list_ss [CFL_SEMANTICS_BLK, CFL_SEMANTICS_SC], 113 114 RW_TAC list_ss [SNOC_APPEND, run_cfl_def, translate_def] THEN 115 `mk_SC (translate (BLK stmL)) [translate_assignment stm] = translate (BLK (stmL ++ [stm]))` by ( 116 RW_TAC list_ss [ARMCompositionTheory.mk_SC_def] THEN 117 Induct_on `stmL` THENL [ 118 RW_TAC list_ss [translate_def], 119 RW_TAC list_ss [translate_def] THEN 120 METIS_TAC [BLOCK_IS_WELL_FORMED] 121 ]) THEN 122 METIS_TAC [] 123 ] 124 ); 125 126val EMPTY_BLK_AXIOM = Q.store_thm ( 127 "EMPTY_BLK_AXIOM", 128 `!P Q. (!st. P st ==> Q st) ==> 129 HSPEC P (BLK []) Q`, 130 RW_TAC std_ss [HSPEC_def, CFL_SEMANTICS_BLK] 131 ); 132 133val CFL_BLK_RULE = Q.store_thm ( 134 "BLK_RULE", 135 `!P Q R stm stmL. HSPEC Q (BLK [stm]) R /\ 136 HSPEC P (BLK stmL) Q ==> 137 HSPEC P (BLK (SNOC stm stmL)) R`, 138 RW_TAC std_ss [HSPEC_def] THEN 139 RW_TAC std_ss [BLK_EQ_SC] THEN 140 METIS_TAC [HSPEC_def, CFL_SC_RULE, BLOCK_IS_WELL_FORMED] 141 ); 142 143 144(*---------------------------------------------------------------------------------*) 145(* Conditional Jumps *) 146(*---------------------------------------------------------------------------------*) 147 148val CFL_CJ_RULE = Q.store_thm ( 149 "CFL_CJ_RULE", 150 `!P Q cond S1 S2 st. WELL_FORMED S1 /\ WELL_FORMED S2 /\ 151 HSPEC (\st.eval_il_cond cond st /\ P st) S1 Q /\ HSPEC (\st.~eval_il_cond cond st /\ P st) S2 Q ==> 152 HSPEC P (CJ cond S1 S2) Q`, 153 RW_TAC std_ss [HSPEC_def] THEN 154 METIS_TAC [CFL_SEMANTICS_CJ] 155 ); 156 157 158val CFL_CJ_RULE_2 = Q.store_thm ( 159 "CFL_CJ_RULE_2", 160 `!P Q cond S1 S2 st. WELL_FORMED S1 /\ WELL_FORMED S2 /\ 161 HSPEC P S1 Q /\ HSPEC P S2 Q ==> 162 HSPEC P (CJ cond S1 S2) Q`, 163 RW_TAC std_ss [HSPEC_def] THEN 164 METIS_TAC [CFL_SEMANTICS_CJ] 165 ); 166 167(*---------------------------------------------------------------------------------*) 168(* Tail Recursion *) 169(*---------------------------------------------------------------------------------*) 170 171val CFL_TR_RULE = Q.store_thm ( 172 "CFL_TR_RULE", 173 `!cond S_body P Q. 174 WELL_FORMED S_body /\ WF_TR (translate_condition cond, translate S_body) /\ 175 HSPEC P S_body P ==> HSPEC P (TR cond S_body) P`, 176 RW_TAC std_ss [HSPEC_def] THEN 177 METIS_TAC [HOARE_TR_CFL] 178 ); 179 180(*---------------------------------------------------------------------------------*) 181(* Well-founded Tail Recursion *) 182(*---------------------------------------------------------------------------------*) 183 184val WF_DEF_2 = Q.store_thm ( 185 "WF_DEF_2", 186 `WF R = !P. (?w. P w) ==> ?min. P min /\ !b. R b min ==> ~P b`, 187 RW_TAC std_ss [relationTheory.WF_DEF] 188 ); 189 190val WF_TR_LEM_1 = Q.store_thm ( 191 "WF_TR_LEM_1", 192 `!cond ir. WELL_FORMED ir /\ 193 WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) ==> 194 WF_TR (translate_condition cond,translate ir)`, 195 196 RW_TAC std_ss [WELL_FORMED_SUB_thm, WF_TR_def, WF_Loop_def, run_cfl_def, run_arm_def] THEN 197 POP_ASSUM MP_TAC THEN Q.ABBREV_TAC `arm = translate ir` THEN STRIP_TAC THEN 198 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))) 199 (FST (FST s0) + LENGTH (translate ir)) s0))` THEN 200 STRIP_TAC THENL [ 201 FULL_SIMP_TAC std_ss [WF_DEF_2, GSYM RIGHT_FORALL_IMP_THM] THEN 202 STRIP_TAC THEN 203 POP_ASSUM (ASSUME_TAC o Q.SPEC `\st. ?pc cpsr pcS. (P:STATEPCS->bool) (((pc,cpsr,st),pcS):STATEPCS)`) THEN 204 STRIP_TAC THEN 205 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 206 `?st pc cpsr pcS. w = ((pc,cpsr,st),pcS)` by METIS_TAC [ABS_PAIR_THM] THEN 207 FULL_SIMP_TAC std_ss [] THEN RES_TAC THEN 208 Q.EXISTS_TAC `((pc',cpsr',st0),pcS')` THEN 209 RW_TAC std_ss [Once get_st_def] THEN RES_TAC THEN 210 `get_st (runTo (upload arm (\i. ARB) pc') (pc'+LENGTH arm) ((pc',cpsr',st0),pcS')) = 211 get_st (runTo (upload arm (\i. ARB) 0) (LENGTH arm) ((0,0w,st0),{}))` by 212 METIS_TAC [well_formed_def, get_st_def, DSTATE_IRRELEVANT_PCS, status_independent_def, FST, DECIDE (Term `!x.0 + x = x`)] THEN 213 METIS_TAC [FST,SND,get_st_def, ABS_PAIR_THM], 214 215 RW_TAC std_ss [get_st_def, eval_il_cond_def] THEN 216 METIS_TAC [WELL_FORMED_INSTB] 217 ] 218 ); 219 220val WF_TR_LEM_2 = Q.store_thm ( 221 "WF_TR_LEM_2", 222 `!cond ir prj_f f cond_f. 223 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ (!st. prj_f (run_cfl ir st) = f (prj_f st)) /\ 224 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==> 225 WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0))`, 226 227 RW_TAC std_ss [WF_DEF_2] THEN 228 Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN 229 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 230 RES_TAC THEN 231 Q.EXISTS_TAC `y` THEN 232 RW_TAC std_ss [] THEN 233 `~cond_f (prj_f y)` by METIS_TAC [] THEN 234 RES_TAC THEN 235 Q.PAT_ASSUM `!t1.p` (ASSUME_TAC o Q.SPEC `prj_f (st1:DSTATE)`) THEN 236 METIS_TAC [] 237 ); 238 239val WF_TR_LEM_3 = Q.store_thm ( 240 "WF_TR_LEM_3", 241 `!cond_f f. (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) ==> 242 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0))`, 243 RW_TAC std_ss [] THEN 244 MATCH_MP_TAC WF_SUBSET THEN 245 Q.EXISTS_TAC `R` THEN 246 RW_TAC std_ss [] 247 ); 248 249val WF_TR_THM_1 = Q.store_thm ( 250 "WF_TR_THM_1", 251 `!cond ir prj_f f cond_f pre_p. 252 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ 253 (!st. pre_p st ==> (prj_f (run_cfl ir st) = f (prj_f st))) /\ 254 WF (\t1 t0. ~cond_f t0 /\ (t1 = f t0)) ==> 255 WF (\st1 st0. (pre_p st0) /\ ~(eval_il_cond cond st0) /\ (st1 = run_cfl ir st0))`, 256 257 RW_TAC std_ss [WF_DEF_2] THEN 258 Q.PAT_ASSUM `!P.p` (ASSUME_TAC o Q.SPEC `\t:'a. ?y:DSTATE. (prj_f y = t) /\ P y`) THEN 259 FULL_SIMP_TAC std_ss [GSYM RIGHT_EXISTS_IMP_THM] THEN 260 RES_TAC THEN 261 Q.EXISTS_TAC `y` THEN 262 RW_TAC std_ss [] THEN 263 `~cond_f (prj_f y)` by METIS_TAC [] THEN 264 RES_TAC THEN 265 Q.PAT_ASSUM `!y1.p` (ASSUME_TAC o Q.SPEC `prj_f (run_cfl ir y)`) THEN 266 METIS_TAC [] 267 ); 268 269(*---------------------------------------------------------------------------------*) 270(* Hoare Rules on Projection on Inputs and Ouputs (represented *) 271(* by projective functions *) 272(* The pre-conditions and post-conditions (on data other than inputs and *) 273(* outputs) are also specified *) 274(*---------------------------------------------------------------------------------*) 275 276val PSPEC_def = Define ` 277 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) = 278 !v x. HSPEC (\st. pre_p st /\ (stk_f st = x) /\ (in_f st = v)) 279 ir (\st. post_p st /\ (stk_f st = x) /\ (out_f st = f v))`; 280 281val _ = type_abbrev("PSPEC_TYPE", type_of (Term `PSPEC`)); 282 283val PSPEC_STACK = Q.store_thm ( 284 "PSPEC_STACK", 285 `!ir pre_p post_p stk_f in_f f out_f x. 286 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 287 ==> 288 HSPEC (\st. pre_p st /\ (stk_f st = x)) ir (\st. post_p st /\ (stk_f st = x))`, 289 RW_TAC std_ss [PSPEC_def, HSPEC_def] 290 ); 291 292val PSPEC_CHARACTERISTIC = Q.store_thm ( 293 "PSPEC_CHARACTERISTIC", 294 `!ir pre_p post_p stk_f in_f f out_f. 295 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 296 ==> 297 HSPEC (\st. pre_p st /\ (in_f st = v)) ir (\st. post_p st /\ (out_f st = f v))`, 298 RW_TAC std_ss [PSPEC_def, HSPEC_def] 299 ); 300 301val PRJ_SHUFFLE_RULE = Q.store_thm ( 302 "PRJ_SHUFFLE_RULE", 303 `!ir pre_p post_p stk_f in_f f out_f shuffle_f. 304 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) 305 ==> 306 PSPEC ir (pre_p, post_p) stk_f (in_f, shuffle_f o f, shuffle_f o out_f)`, 307 RW_TAC std_ss [PSPEC_def, HSPEC_def] 308 ); 309 310val PRJ_SHUFFLE_RULE2 = Q.store_thm ( 311 "PRJ_SHUFFLE_RULE2", 312 `!ir pre_p post_p stk_f in_f f out_f g in_f'. 313 PSPEC ir (pre_p, post_p) stk_f (in_f, f, out_f) /\ (g o in_f' = f o in_f) 314 ==> 315 PSPEC ir (pre_p,post_p) stk_f (in_f', g, out_f)`, 316 RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN 317 METIS_TAC [FUN_EQ_THM, combinTheory.o_THM] 318 ); 319 320val PRJ_SC_RULE = Q.store_thm ( 321 "PRJ_SC_RULE", 322 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2. 323 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 324 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) 325 ==> 326 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`, 327 328 RW_TAC std_ss [PSPEC_def] THEN 329 METIS_TAC [CFL_SC_RULE] 330 ); 331 332val PRJ_CJ_RULE = Q.store_thm ( 333 "PRJ_CJ_RULE", 334 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f. 335 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 336 PSPEC ir_t (pre_p,post_p) stk_f (in_f,f1,out_f) /\ 337 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) 338 ==> 339 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)`, 340 341 RW_TAC std_ss [PSPEC_def, HSPEC_def] THEN 342 METIS_TAC [CFL_SEMANTICS_CJ] 343 ); 344 345(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *) 346 347val PRJ_TR_RULE = Q.store_thm ( 348 "PRJ_TR_RULE", 349 `!cond ir pre_p stk_f cond_f prj_f f. 350 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) /\ 351 (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ PSPEC ir (pre_p,pre_p) stk_f (prj_f,f,prj_f) ==> 352 PSPEC (TR cond ir) (pre_p,pre_p) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`, 353 354 RW_TAC std_ss [PSPEC_def] THEN 355 RW_TAC std_ss [HSPEC_def] THENL [ 356 FULL_SIMP_TAC std_ss [HSPEC_def] THEN 357 METIS_TAC [SIMP_RULE std_ss [HSPEC_def] CFL_TR_RULE, WF_TR_LEM_1], 358 359 IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_STACK) THEN 360 POP_ASSUM (ASSUME_TAC o Q.SPEC `(stk_f:DSTATE->'a) st`) THEN 361 IMP_RES_TAC WF_TR_LEM_1 THEN 362 IMP_RES_TAC (Q.SPECL [`cond`,`ir`,`\st1. pre_p st1 /\ ((stk_f:DSTATE->'a) 363 st1 = (stk_f:DSTATE->'a) st)`] CFL_TR_RULE) THEN 364 POP_ASSUM (ASSUME_TAC o Q.SPEC `st` o SIMP_RULE std_ss [HSPEC_def]) THEN 365 METIS_TAC [], 366 367 IMP_RES_TAC (SIMP_RULE std_ss [PSPEC_def] PSPEC_CHARACTERISTIC) THEN 368 Q.PAT_ASSUM `!v x.p` (K ALL_TAC) THEN 369 `WF_TR (translate_condition cond,translate ir)` by METIS_TAC [WF_TR_LEM_1] THEN 370 FULL_SIMP_TAC std_ss [WELL_FORMED_SUB_thm, HSPEC_def, run_cfl_def, run_arm_def, translate_def, eval_il_cond_def] THEN 371 Q.ABBREV_TAC `arm = translate ir` THEN 372 IMP_RES_TAC (SIMP_RULE set_ss [] (Q.SPECL [`translate_condition cond`,`arm`,`(\i. ARB)`,`(0,0w,st):STATE`,`{}`] 373 ARMCompositionTheory.UNROLL_TR_LEM)) THEN 374 POP_ASSUM (ASSUME_TAC o Q.SPEC `st`) THEN 375 FULL_SIMP_TAC std_ss [FUNPOW, ARMCompositionTheory.get_st_def] THEN 376 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 377 Induct_on `loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,st),{})` THENL [ 378 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW,ARMCompositionTheory.get_st_def] THEN 379 IMP_RES_TAC ARMCompositionTheory.LOOPNUM_BASIC THEN 380 FULL_SIMP_TAC arith_ss [Once WHILE, ARMCompositionTheory.get_st_def], 381 382 REWRITE_TAC [Once EQ_SYM_EQ] THEN RW_TAC std_ss [FUNPOW] THEN 383 IMP_RES_TAC ARMCompositionTheory.LOOPNUM_INDUCTIVE THEN 384 `v = loopNum (translate_condition cond) arm (\i.ARB) ((0,0w,SND (SND (FST (runTo (upload arm (\i.ARB) 0) (LENGTH arm) 385 ((0,0w,st),{}))))),{})` by METIS_TAC [ABS_PAIR_THM,DECIDE (Term`!x.0+x=x`), 386 ARMCompositionTheory.LOOPNUM_INDEPENDENT_OF_CPSR_PCS, ARMCompositionTheory.get_st_def, 387 FST, SND, ARMCompositionTheory.DSTATE_IRRELEVANT_PCS,ARMCompositionTheory.well_formed_def] THEN 388 RES_TAC THEN Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN 389 FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 390 Q.PAT_ASSUM `v = x` (ASSUME_TAC o GSYM) THEN FULL_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) THEN 391 Q.PAT_ASSUM `~x` (ASSUME_TAC o SIMP_RULE std_ss [ARMCompositionTheory.get_st_def]) THEN 392 RW_TAC std_ss [Once WHILE] THEN 393 Q.UNABBREV_TAC `arm` THEN 394 `run_cfl ir st = SND (SND (FST (runTo (upload (translate ir) (\i. ARB) 0) (LENGTH (translate ir)) 395 ((0,0w,st),{}))))` by RW_TAC arith_ss [ 396 ARMCompositionTheory.get_st_def, run_cfl_def, run_arm_def] THEN 397 METIS_TAC [SND,FST,ARMCompositionTheory.get_st_def,ARMCompositionTheory.FUNPOW_DSTATE, ABS_PAIR_THM] 398 ] 399 ] 400 ); 401 402val PRJ_TR_RULE_2 = Q.store_thm ( 403 "PRJ_TR_RULE_2", 404 `!cond ir stk_f cond_f prj_f f. 405 WELL_FORMED ir /\ (!st. cond_f (prj_f st) = eval_il_cond cond st) /\ 406 (?R. WF R /\ !t0 t1. ~cond_f t0 ==> R (f t0) t0) /\ 407 PSPEC ir ((\st.T),(\st.T)) stk_f (prj_f,f,prj_f) ==> 408 PSPEC (TR cond ir) ((\st.T),(\st.T)) stk_f (prj_f, WHILE ($~ o cond_f) f, prj_f)`, 409 410 SIMP_TAC std_ss [PSPEC_def, HSPEC_def] THEN 411 REPEAT GEN_TAC THEN NTAC 2 STRIP_TAC THEN 412 `WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0))` by METIS_TAC [WF_TR_LEM_2, WF_TR_LEM_3] THEN 413 METIS_TAC [SIMP_RULE std_ss [PSPEC_def, HSPEC_def] (Q.SPECL [`cond`,`ir`,`\st.T`] PRJ_TR_RULE)] 414 ); 415 416 417(*---------------------------------------------------------------------------------*) 418(* Rules for Conditions (projective function version) *) 419(*---------------------------------------------------------------------------------*) 420 421val PRJ_STRENGTHEN_RULE = Q.store_thm ( 422 "PRJ_STRENGTHEN_RULE", 423 `!ir pre_p pre_p' post_p stk_f in_f f out_f. 424 WELL_FORMED ir /\ 425 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. pre_p' st ==> pre_p st) ==> 426 PSPEC ir (pre_p',post_p) stk_f (in_f,f,out_f)`, 427 RW_TAC std_ss [PSPEC_def, HSPEC_def] 428 ); 429 430val PRJ_WEAKEN_RULE = Q.store_thm ( 431 "PRJ_WEAKEN_RULE", 432 `!ir pre_p post_p post_p' stk_f in_f f out_f. 433 WELL_FORMED ir /\ 434 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ (!st. post_p st ==> post_p' st) ==> 435 PSPEC ir (pre_p,post_p') stk_f (in_f,f,out_f)`, 436 RW_TAC std_ss [PSPEC_def, HSPEC_def] 437 ); 438 439(*---------------------------------------------------------------------------------*) 440(* Rules for Stack (projective function version) *) 441(*---------------------------------------------------------------------------------*) 442 443val valid_push_def = Define ` 444 valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f') = 445 !st st'. (stk_f st' = stk_f st) /\ (out_f st' = f (in_f st)) ==> 446 (stk_f' st' = stk_f' st) /\ (out_f' st' = g (in_f' st))`; 447 448val PRJ_POP_RULE = Q.store_thm ( 449 "PRJ_POP_RULE", 450 `!ir pre_p post_p stk_f in_f f out_f stk_f' in_f' g out_f'. 451 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ 452 valid_push (stk_f,in_f,f,out_f) (stk_f',in_f',g,out_f') 453 ==> 454 PSPEC ir (pre_p,post_p) stk_f' (in_f', g, out_f')`, 455 RW_TAC list_ss [PSPEC_def, HSPEC_def, valid_push_def] 456 ); 457 458val P_intact_def = Define ` 459 P_intact (P,Q) (stk_f,stk_g) = 460 !st st'. (stk_f st' = stk_f st) /\ P st /\ Q st' 461 ==> (stk_g st' = stk_g st)`; 462 463val PRJ_PUSH_RULE = Q.store_thm ( 464 "PRJ_PUSH_RULE", 465 `!ir pre_p post_p stk_f in_f f out_f e_f stk_g. 466 PSPEC ir (pre_p,post_p) stk_f (in_f,f,out_f) /\ 467 P_intact (pre_p,post_p) (stk_f,stk_g) 468 ==> PSPEC ir (pre_p,post_p) stk_g (in_f, f, out_f)`, 469 RW_TAC list_ss [PSPEC_def, HSPEC_def, P_intact_def] 470 ); 471 472(*---------------------------------------------------------------------------------*) 473(* Hoare Rules on Projection on Inputs and Ouputs (represented by vectors) *) 474(* To overcome the type restriction on tuples in HOL definitions *) 475(*---------------------------------------------------------------------------------*) 476 477(* Vectors *) 478 479val _ = Hol_datatype ` 480 VEXP = SG of DATA (* registers *) 481 | VT of VEXP # VEXP (* pairs *) 482 `; 483 484val readv_def = Define ` 485 (readv st (PR (a,b)) = VT (readv st a, readv st b)) /\ 486 (readv st x = SG (mread st x))`; 487 488 489(* Vector Stack, modelled as a list of expression vectors *) 490 491val push_def = Define ` 492 push x stk = x :: stk`; 493 494val top_def = Define ` 495 top = HD`; 496 497val pop_def = Define ` 498 pop = TL`; 499 500(* Specification on vectors *) 501 502val VSPEC_def = Define ` 503 VSPEC ir (pre_p,post_p) stk (iv,f,ov) = 504 PSPEC ir (pre_p,post_p) (\st. MAP (readv st) stk) ((\st.readv st iv), f, (\st.readv st ov)) 505 `; 506 507val _ = type_abbrev("VSPEC_TYPE", type_of (Term `VSPEC`)); 508 509val V_SHUFFLE_RULE = Q.store_thm ( 510 "V_SHUFFLE_RULE", 511 `!ir stk iv f ov g iv'. 512 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. g (readv st iv') = f (readv st iv)) 513 ==> 514 VSPEC ir (pre_p,post_p) stk (iv', g, ov)`, 515 RW_TAC std_ss [VSPEC_def, PSPEC_def, HSPEC_def] 516 ); 517 518val V_SC_RULE = Q.store_thm ( 519 "V_SC_RULE", 520 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2. 521 WELL_FORMED ir1 /\ WELL_FORMED ir2 /\ 522 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2) 523 ==> 524 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`, 525 RW_TAC std_ss [VSPEC_def] THEN 526 METIS_TAC [PRJ_SC_RULE] 527 ); 528 529val V_CJ_RULE = Q.store_thm ( 530 "V_CJ_RULE", 531 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 ov. 532 WELL_FORMED ir_t /\ WELL_FORMED ir_f /\ 533 VSPEC ir_t (pre_p,post_p) stk (iv,f1,ov) /\ 534 VSPEC ir_f (pre_p, post_p) stk (iv,f2,ov) /\ (!st. cond_f (readv st iv) = eval_il_cond cond st) 535 ==> 536 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)`, 537 RW_TAC std_ss [VSPEC_def] THEN 538 FULL_SIMP_TAC std_ss [PRJ_CJ_RULE] 539 ); 540 541(* Need the theorems in ARMCompositionTheory to prove the PROJ_TR_RULE *) 542 543val V_TR_RULE = Q.store_thm ( 544 "V_TR_RULE", 545 `!cond ir pre_p stk cond_f iv f. 546 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) /\ 547 (!st. cond_f (readv st iv) = eval_il_cond cond st) /\ VSPEC ir (pre_p,pre_p) stk (iv,f,iv) ==> 548 VSPEC (TR cond ir) (pre_p,pre_p) stk (iv, WHILE ($~ o cond_f) f, iv)`, 549 550 RW_TAC std_ss [VSPEC_def] THEN 551 FULL_SIMP_TAC std_ss [PRJ_TR_RULE] 552 ); 553 554(*---------------------------------------------------------------------------------*) 555(* Rules for Conditions (vector version) *) 556(*---------------------------------------------------------------------------------*) 557 558val V_STRENGTHEN_RULE = Q.store_thm ( 559 "V_STRENGTHEN_RULE", 560 `!ir pre_p pre_p' post_p stk iv f ov. 561 WELL_FORMED ir /\ 562 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. pre_p' st ==> pre_p st) ==> 563 VSPEC ir (pre_p',post_p) stk (iv,f,ov)`, 564 RW_TAC std_ss [VSPEC_def] THEN 565 METIS_TAC [PRJ_STRENGTHEN_RULE] 566 ); 567 568val V_WEAKEN_RULE = Q.store_thm ( 569 "V_WEAKEN_RULE", 570 `!ir pre_p post_p post_p' stk iv f ov. 571 WELL_FORMED ir /\ 572 PSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ (!st. post_p st ==> post_p' st) ==> 573 PSPEC ir (pre_p,post_p') stk (iv,f,ov)`, 574 RW_TAC std_ss [VSPEC_def] THEN 575 METIS_TAC [PRJ_WEAKEN_RULE] 576 ); 577 578(*---------------------------------------------------------------------------------*) 579(* Rules for Stack (vector version) *) 580(*---------------------------------------------------------------------------------*) 581 582val V_POP_RULE = Q.store_thm ( 583 "V_POP_RULE", 584 `!ir pre_p post_p stk iv f ov e g. 585 VSPEC ir (pre_p,post_p) (e::stk) (iv,f,ov) /\ 586 (!st. g (readv st (PR(iv,e))) = VT (f (readv st iv), readv st e)) ==> 587 VSPEC ir (pre_p,post_p) stk (PR(iv,e), g, PR(ov,e))`, 588 RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, readv_def] 589 ); 590 591val V_intact_def = Define ` 592 V_intact (P,Q,e) = 593 ?x. (!st.P st ==> (readv st e = x)) /\ (!st.Q st ==> (readv st e = x))`; 594 595 596val V_PUSH_RULE = Q.store_thm ( 597 "V_PUSH_RULE", 598 `!ir pre_p post_p stk iv f ov e. 599 VSPEC ir (pre_p,post_p) stk (iv,f,ov) /\ V_intact(pre_p, post_p, e) 600 ==> 601 VSPEC ir (pre_p,post_p) (e::stk) (iv, f, ov)`, 602 RW_TAC list_ss [VSPEC_def, PSPEC_def, HSPEC_def, V_intact_def, readv_def] THEN 603 METIS_TAC [] 604 ); 605 606 607(*---------------------------------------------------------------------------------*) 608(* Rules for Well-formedness *) 609(*---------------------------------------------------------------------------------*) 610 611val WELL_FORMED_TR_RULE = Q.store_thm ( 612 "WELL_FORMED_TR_RULE", 613 `!cond ir context_f. 614 WELL_FORMED ir /\ WF (\st1 st0. ~eval_il_cond cond st0 /\ (st1 = run_cfl ir st0)) ==> 615 WELL_FORMED (TR cond ir)`, 616 617 RW_TAC std_ss [] THEN 618 METIS_TAC [CFL_TR_IS_WELL_FORMED, WF_TR_LEM_1] 619 ); 620 621val _ = export_theory(); 622