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