1open HolKernel boolLib bossLib Parse proofManagerLib; 2open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory arm_stepTheory; 3open MMUTheory MMU_SetupTheory inference_rulesTheory switching_lemma_helperTheory; 4open priv_constraints_lrTheory priv_constraints_spsrTheory; 5open tacticsLib ARM_prover_extLib; 6 7(*********************************************************************************) 8(* checking bisimulation for take exceptions in privileged mode *) 9(* Narges *) 10(*********************************************************************************) 11 12val _ = new_theory("priv_constraints_bisim"); 13 14val let_ss = simpLib.mk_simpset [boolSimps.LET_ss] ; 15val _ = diminish_srw_ss ["one"] 16val _ = augment_srw_ss [rewrites [oneTheory.FORALL_ONE]] 17 18val prove_abs_spsr_const_action = 19 fn (a, thms, abody_thm, expr,mode) => 20 let 21 val _ = set_goal([], `` 22 (priv_spsr_constraints_abs ^a ^expr ^mode) ``) 23 val (a_abs,a_body) = pairLib.dest_pabs a; 24 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 25 val unbeta_a = mk_comb (a, a_abs) 26 val snd = get_type_inst (type_of(a_body) , false) 27 val a_body_type = get_type_inst (snd, true); 28 val proved_unbeta_lemma = store_thm ("proved_unbeta_lemma", 29 ``(priv_spsr_constraints ^a_body ^expr ^mode)= 30 (priv_spsr_constraints ^unbeta_a ^expr ^mode)``, 31 (ASSUME_TAC (SPECL [a_body,``^unbeta_a``, expr,mode] 32 (INST_TYPE [beta |-> a_body_type, 33 alpha |-> ``:arm_state``] 34 (List.nth(thms,0))))) 35 THEN ASSUME_TAC unbeta_thm 36 THEN RES_TAC); 37 38 val proved_preserve_unbeta_a = 39 store_thm ("proved_preserve_unbeta_a", 40 `` (priv_spsr_constraints ^unbeta_a ^expr ^mode)``, 41 (ASSUME_TAC (proved_unbeta_lemma)) 42 THEN (ASSUME_TAC abody_thm) 43 THEN (FULL_SIMP_TAC (srw_ss()) [])); 44 45 val abs_type = type_of a_abs 46 val (abs_args, abs_body) = generate_uncurry_abs a 47 val tacs = (ASSUME_TAC proved_preserve_unbeta_a) 48 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a; 49 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 50 THEN (ASSUME_TAC ( 51 SPECL[a, expr,mode] 52 (INST_TYPE [alpha |-> abs_type, 53 beta |-> ``:arm_state``, 54 gamma |-> a_body_type] 55 (List.nth(thms,1))))) 56 THEN (RW_TAC (srw_ss()) []) 57 THEN (FULL_SIMP_TAC (srw_ss()) []) 58 THEN (UNDISCH_ALL_TAC THEN 59 (RW_TAC (srw_ss()) []) 60 THEN (FULL_SIMP_TAC (srw_ss()) [])) 61 val _ = e (tacs) 62 val proved_thm = top_thm() 63 val _ = proofManagerLib.drop(); 64 in 65 (proved_thm,tacs) 66 end 67 68 69val untouched_spsr_abs_def = 70 Define `untouched_spsr_abs f (mode:bool[5]) = 71 !s a c s'. (f a s = ValueState c s') ==> 72 let spsr = get_spsr_by_mode mode 73 in 74 ((s'.psrs (0,spsr))=(s.psrs (0,spsr))) 75 /\ 76 ((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M) 77 `; 78 79val untouched_spsr_def = 80 Define `untouched_spsr f (mode:bool[5]) = 81 !s c s'. (f s = ValueState c s') ==> 82 let spsr = get_spsr_by_mode mode 83 in (*(spsr<>CPSR) ==>*) 84 ((s'.psrs (0,spsr))=(s.psrs (0,spsr))) 85 /\ 86 ((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M) 87 `; 88 89val priv_spsr_constraints_def = 90 Define `priv_spsr_constraints f cpsr mode = 91 ! s s' a . (f s = ValueState a s') ==> 92 (~access_violation s') ==> 93 ((s'.psrs(0,CPSR)).M = mode) ==> 94 ( let spsr = get_spsr_by_mode mode 95 in (*(spsr<>CPSR) ==>*) 96 ((s'.psrs(0,spsr)) = cpsr ) 97 98 )`; 99 100 101val priv_spsr_constraints_abs_def = 102 Define `priv_spsr_constraints_abs f cpsr mode = 103 ! s s' a c . (f c s = ValueState a s') ==> 104 (~access_violation s') ==> 105 ((s'.psrs(0,CPSR)).M = mode) ==> 106 ( let spsr = get_spsr_by_mode mode 107 in (*(spsr<>CPSR) ==>*) 108 ((s'.psrs(0,spsr)) = cpsr ) 109 110 )`; 111 112(********************* proof rules *******************************) 113 114val seqT_priv_spsr_constraints_before_thm = 115 store_thm("seqT_priv_spsr_constraints_before_thm", 116 `` ! g f cpsr spsr. priv_spsr_constraints_abs f cpsr spsr ==> 117 priv_spsr_constraints (g >>= f) cpsr spsr ``, 118 (RW_TAC (srw_ss()) [seqT_def, 119 priv_spsr_constraints_def, 120 priv_spsr_constraints_abs_def]) 121 THEN FULL_SIMP_TAC (let_ss) [] 122 THEN ASSUME_TAC 123 (SPECL [``g:'a M``, ``f: 'a -> 'b M``, 124 ``s:arm_state``,``a:'b``, 125 ``s':arm_state``(* ,``b:arm_state``, *) 126 (* ``a':'a`` *)] 127 seqT_access_violation_thm) 128 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 129 THEN Cases_on `g s` 130 THEN FULL_SIMP_TAC (srw_ss()) [] 131 THEN Cases_on `access_violation b` 132 (* THEN Q.UNABBREV_TAC `spsr` *) 133 THEN PAT_X_ASSUM ``! s s' a c .X ==> Z`` 134 (fn thm => ASSUME_TAC 135 (SPECL [``b:arm_state``,``s':arm_state``, 136 ``a:'b``,``a':'a``] thm)) 137 THEN FULL_SIMP_TAC (srw_ss()) [] 138 THEN RES_TAC 139 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 140 ); 141 142val parT_priv_spsr_constraints_before_thm = 143 store_thm("parT_priv_spsr_constraints_before_thm", 144 `` !f g cpsr spsr . priv_spsr_constraints f cpsr spsr ==> 145 priv_spsr_constraints (g ||| f) cpsr spsr ``, 146 RW_TAC (srw_ss()) 147 [parT_def,seqT_def, 148 priv_spsr_constraints_def, 149 untouched_spsr_def,constT_def] 150 THEN FULL_SIMP_TAC (let_ss) [] 151 THEN IMP_RES_TAC 152 (SIMP_RULE bool_ss 153 [seqT_def,parT_def,constT_def] 154 (SPECL [``g:'a M``, ``f: 'b M``, 155 ``s:arm_state``,``a:('a#'b)``, 156 ``s':arm_state`` ,``b:arm_state``, 157 ``a':'a`` ] 158 parT_access_violation_thm)) 159 THEN Cases_on `g s` 160 THEN Cases_on `f b` 161 (* THEN Q.UNABBREV_TAC `spsr` *) 162 THEN FULL_SIMP_TAC (srw_ss()) [] 163 THEN PAT_X_ASSUM ``! s s' a. (f s = ValueState a s') ==> Z`` (fn thm => ASSUME_TAC 164 (SPECL [``b:arm_state``,``b':arm_state``,``a'':'a``] thm)) 165 THEN Cases_on `access_violation b` 166 THEN Cases_on `access_violation b'` 167 THEN RES_TAC 168 THEN FULL_SIMP_TAC (srw_ss()) [] 169 THEN FIRST_PROVE [ FULL_SIMP_TAC (srw_ss()) [] 170 THEN RW_TAC (srw_ss()) [] , 171 (UNDISCH_ALL_TAC 172 THEN RW_TAC (srw_ss()) [] 173 THEN FULL_SIMP_TAC (srw_ss()) [])]); 174 175val seqT_priv_spsr_constraints_after_thm = 176 store_thm("seqT_priv_spsr_constraints_after_thm", 177 `` !f g cpsr mode. 178 priv_spsr_constraints g cpsr mode ==> 179 (untouched_spsr_abs f mode) ==> 180 priv_spsr_constraints (g >>= f) cpsr mode``, 181 (RW_TAC (srw_ss()) [seqT_def, 182 priv_spsr_constraints_def, 183 priv_spsr_constraints_abs_def, 184 untouched_spsr_abs_def]) THEN 185 FULL_SIMP_TAC (let_ss) [] THEN 186 Cases_on `g s` THEN 187 FULL_SIMP_TAC (srw_ss()) [] THEN 188 Cases_on `access_violation b` 189 THEN Q.UNABBREV_TAC `spsr` 190 THEN PAT_X_ASSUM ``! s s' a .X ==> Z`` 191 (fn thm => ASSUME_TAC 192 (SPECL [``s:arm_state``,``b:arm_state``, 193 ``a':'a``] thm)) 194 195 THEN PAT_X_ASSUM ``! s1 a c s2. X`` 196 (fn thm => ASSUME_TAC 197 (SPECL [``b:arm_state``,``a':'a``, 198 ``a:'b``,``s':arm_state``] thm)) 199 200 THEN RES_TAC 201 THEN UNDISCH_ALL_TAC 202 THEN RW_TAC (srw_ss()) [] 203 THEN FULL_SIMP_TAC (srw_ss()) [] 204 THEN FULL_SIMP_TAC (srw_ss()) []); 205 206val parT_priv_spsr_constraints_after_thm = 207 store_thm("parT_priv_spsr_constraints_after_thm", 208`` !f g cpsr spsr. priv_spsr_constraints g cpsr spsr ==> 209 (untouched_spsr f spsr) ==> 210 priv_spsr_constraints (g ||| f) cpsr spsr``, 211 (RW_TAC (srw_ss()) 212 [parT_def,seqT_def, 213 priv_spsr_constraints_def, 214 untouched_spsr_def,constT_def]) 215 THEN FULL_SIMP_TAC (let_ss) []THEN 216 Cases_on `g s` THEN 217 Cases_on `f b` THEN 218 Cases_on `access_violation b` THEN 219 Cases_on `access_violation b'` THEN 220 (* Q.UNABBREV_TAC `spsr` THEN *) 221 FULL_SIMP_TAC (srw_ss()) [] THEN 222 PAT_X_ASSUM ``! s a s' .(f s = ValueState a s') ==> Z`` 223 (fn thm => ASSUME_TAC 224 (SPECL [``b:arm_state``,``a'':'a``,``b':arm_state``] thm)) 225 THEN PAT_X_ASSUM ``! s1 c s2. X`` 226 (fn thm => ASSUME_TAC 227 (SPECL [``s:arm_state``,``b:arm_state``,``a':'b``] thm)) 228 THEN RES_TAC 229 THEN UNDISCH_ALL_TAC 230 THEN RW_TAC (srw_ss()) [] 231 THEN FULL_SIMP_TAC (srw_ss()) [] 232 ); 233 234 235val seqT_trans_untouched_thm = 236 store_thm("seqT_trans_untouched_thm", 237 `` !f g mode. 238 (untouched_spsr f mode) ==> 239 (untouched_spsr_abs g mode) ==> 240 (untouched_spsr (f>>=g) mode)``, 241 (RW_TAC (srw_ss()) [seqT_def,untouched_spsr_abs_def, 242 untouched_spsr_def]) 243THEN Cases_on `f s` 244 THEN FULL_SIMP_TAC (let_ss) [] 245 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> _`` 246 (fn thm => ASSUME_TAC 247 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 248 THEN RES_TAC 249 THEN Cases_on `access_violation b` 250 THEN FULL_SIMP_TAC (srw_ss()) [] 251 THEN RW_TAC (srw_ss()) [] 252 THEN PAT_X_ASSUM ``! s a c s'. X`` 253 (fn thm => ASSUME_TAC 254 (SPECL [``b:arm_state``,``a:'a``, 255 ``c:'b``,``s':arm_state``] thm)) 256 THEN RES_TAC 257 THEN FULL_SIMP_TAC (srw_ss()) [] 258 THEN RW_TAC (srw_ss()) []); 259 260val parT_trans_untouched_thm = 261 store_thm("parT_trans_untouched_thm", 262 `` !f g spsr. 263 (untouched_spsr f spsr) ==> 264 (untouched_spsr g spsr) ==> 265 (untouched_spsr (f ||| g) spsr)``, 266 (RW_TAC (srw_ss()) [seqT_def,parT_def,constT_def, 267 untouched_spsr_def]) 268 THEN Cases_on `f s` 269 THEN Cases_on `access_violation b` 270 THEN Cases_on `g b` 271 THEN Cases_on `access_violation b'` 272 THEN FULL_SIMP_TAC (let_ss) [] 273 THEN PAT_X_ASSUM ``! s c s'. X`` 274 (fn thm => ASSUME_TAC 275 (SPECL [``b:arm_state``,``a':'b``, 276 ``b':arm_state``] thm)) 277 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> _`` 278 (fn thm => ASSUME_TAC 279 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 280 THEN RES_TAC 281 THEN FULL_SIMP_TAC (srw_ss()) [] 282 THEN RW_TAC (srw_ss()) [] 283 ); 284 285val spfc_first_abs_lemma = 286 store_thm ("spfc_first_abs_lemma", 287 ``!f g x y. (f=g) ==> ((priv_spsr_constraints f x y) = 288 (priv_spsr_constraints g x y))``, 289 RW_TAC (srw_ss()) []); 290 291 292val spfc_second_abs_lemma = 293 store_thm ("spfc_second_abs_lemma", 294 ``! f x z. (! y. priv_spsr_constraints (f y) x z) = 295 priv_spsr_constraints_abs f x z``, 296 RW_TAC (srw_ss()) [priv_spsr_constraints_def,priv_spsr_constraints_abs_def] 297 THEN METIS_TAC []); 298 299 300(********************* end of proof rules *******************************) 301(******************* basic lemmas **************************************) 302 303val read_cpsr_fixed_lem = 304 store_thm("read_cpsr_fixed_lem", 305``!s. read_cpsr <|proc := 0|> s = ValueState (s.psrs (0,CPSR)) s``, 306 EVAL_TAC 307 THEN RW_TAC (srw_ss()) []); 308 309(* if possible, try to optimize it *) 310val write_spsr_sfc_thm = 311 store_thm("write_spsr_sfc_thm", 312 ``! cpsr mode. priv_spsr_constraints (write_spsr <|proc := 0|> cpsr) 313 cpsr mode ``, 314 315 RW_TAC (bool_ss) [write_spsr_def,seqT_def,priv_spsr_constraints_def] 316 THEN Cases_on `read_cpsr <|proc := 0|> s` 317 THEN FIRST_PROVE [ 318 FULL_SIMP_TAC (srw_ss()) [] 319 THEN ASSUME_TAC (SPEC ``s:arm_state`` read_cpsr_fixed_lem) 320 THEN Cases_on `access_violation b` 321 THENL [ 322 FULL_SIMP_TAC (srw_ss()) [] 323 THEN RW_TAC (srw_ss()) [] 324 THEN FULL_SIMP_TAC (srw_ss()) [], 325 Cases_on ` bad_mode <|proc := 0|> a'.M b` 326 THENL 327 [ 328 FULL_SIMP_TAC (srw_ss()) [] 329 THEN Cases_on `access_violation b'` 330 THENL[ 331 FULL_SIMP_TAC (srw_ss()) [] 332 THEN RW_TAC (srw_ss()) [] 333 THEN FULL_SIMP_TAC (srw_ss()) [] 334 , 335 FULL_SIMP_TAC (srw_ss()) [] 336 THEN Cases_on `a''` 337 THENL [ 338 FULL_SIMP_TAC (srw_ss()) [] 339 (* THEN Q.UNABBREV_TAC `spsr` *) 340 THEN UNDISCH_ALL_TAC 341 THEN EVAL_TAC, 342 (* Q.UNABBREV_TAC `spsr` *) 343 (* THEN *) UNDISCH_ALL_TAC 344 THEN EVAL_TAC 345 THEN RW_TAC (srw_ss()) [] THEN 346 FULL_SIMP_TAC (srw_ss()) [] 347 THEN UNDISCH_ALL_TAC 348 THEN EVAL_TAC 349 THEN RW_TAC (srw_ss()) [] THEN 350 FULL_SIMP_TAC (srw_ss()) []]], 351 FULL_SIMP_TAC (srw_ss()) []]], 352 FULL_SIMP_TAC (srw_ss()) []]); 353 354 355val write_lr_reg_sfc_ut_thm = 356 store_thm("write_lr_reg_sfc_ut_thm", 357 ``! value mode. 358 (untouched_spsr (write_reg <|proc:=0|> 14w value) mode)``, 359 EVAL_TAC 360 THEN RW_TAC (srw_ss()) [] 361 THEN UNDISCH_ALL_TAC 362 THEN EVAL_TAC 363 THEN RW_TAC (srw_ss()) [] 364 THEN FULL_SIMP_TAC (srw_ss()) []); 365 366val read_cpsr_sfc_ut_thm = 367 store_thm("read_cpsr_sfc_ut_thm", 368 `` !mode. 369 (untouched_spsr (read_cpsr <|proc:=0|> ) mode )``, 370 EVAL_TAC 371 THEN RW_TAC (srw_ss()) [] ); 372 373val branch_to_sfc_ut_thm = 374 store_thm("branch_to_sfc_ut_thm", 375 ``!adr mode. untouched_spsr ( 376 branch_to <|proc:=0|> adr) mode``, 377 EVAL_TAC 378 THEN RW_TAC (srw_ss()) [] 379 THEN UNDISCH_ALL_TAC 380 THEN EVAL_TAC 381 THEN RW_TAC (srw_ss()) [] 382 THEN FULL_SIMP_TAC (srw_ss()) []); 383 384val constT_sfc_ut_thm = 385 store_thm("constT_sfc_ut_thm", 386 ``! mode. untouched_spsr_abs (��(u1:unit,u2:unit,u3:unit,u4:unit). 387 constT ()) mode``, 388 EVAL_TAC 389 THEN RW_TAC (srw_ss()) [] ); 390 391val ui_write_cpsr_spsr_ut_thm = 392 store_thm("ui_write_cpsr_spsr_ut_thm", 393``untouched_spsr ( 394 read_cpsr <|proc:=0|> >>= 395 (��cpsr. 396 write_cpsr <|proc:=0|> 397 (cpsr with 398 <|I := T; IT := 0w; J := F; T := sctlr.TE; 399 E := sctlr.EE|>))) 27w``, 400EVAL_TAC 401THEN RW_TAC (srw_ss()) [] 402THEN UNDISCH_ALL_TAC 403THEN EVAL_TAC 404THEN RW_TAC (srw_ss()) [] 405THEN FULL_SIMP_TAC (srw_ss()) []); 406 407val svc_write_cpsr_spsr_ut_thm = 408 store_thm("svc_write_cpsr_spsr_ut_thm", 409``untouched_spsr ( 410 read_cpsr <|proc:=0|> >>= 411 (��cpsr. 412 write_cpsr <|proc:=0|> 413 (cpsr with 414 <|I := T; IT := 0w; J := F; T := sctlr.TE; 415 E := sctlr.EE|>))) 19w``, 416EVAL_TAC 417THEN RW_TAC (srw_ss()) [] 418THEN UNDISCH_ALL_TAC 419THEN EVAL_TAC 420THEN RW_TAC (srw_ss()) [] 421THEN FULL_SIMP_TAC (srw_ss()) []); 422 423val irq_write_cpsr_spsr_ut_thm = 424 store_thm("irq_write_cpsr_spsr_ut_thm", 425``untouched_spsr ( 426 read_cpsr <|proc:=0|> >>= 427 (��cpsr. 428 write_cpsr <|proc:=0|> 429 (cpsr with 430 <|I := T; 431 A := 432 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 433 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 434 E := sctlr.EE|>))) 18w``, 435EVAL_TAC 436THEN RW_TAC (srw_ss()) [] 437THEN UNDISCH_ALL_TAC 438THEN EVAL_TAC 439THEN RW_TAC (srw_ss()) [] 440THEN FULL_SIMP_TAC (srw_ss()) []); 441 442 443val ab_write_cpsr_spsr_ut_thm = 444 store_thm("ab_write_cpsr_spsr_ut_thm", 445``untouched_spsr ( 446 read_cpsr <|proc:=0|> >>= 447 (��cpsr. 448 write_cpsr <|proc:=0|> 449 (cpsr with 450 <|I := T; 451 A := 452 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 453 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 454 E := sctlr.EE|>))) 23w``, 455EVAL_TAC 456THEN RW_TAC (srw_ss()) [] 457THEN UNDISCH_ALL_TAC 458THEN EVAL_TAC 459THEN RW_TAC (srw_ss()) [] 460THEN FULL_SIMP_TAC (srw_ss()) []); 461 462 463val fiq_write_cpsr_spsr_ut_thm = 464 store_thm("fiq_write_cpsr_spsr_ut_thm", 465``untouched_spsr ( 466 read_cpsr <|proc:=0|> >>= 467 (��cpsr. 468 write_cpsr <|proc:=0|> 469 (cpsr with 470 <|I := T; 471 F := 472 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 473 cpsr.F); 474 A := 475 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 476 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 477 E := sctlr.EE|>))) 17w``, 478 479EVAL_TAC 480THEN RW_TAC (srw_ss()) [] 481THEN UNDISCH_ALL_TAC 482THEN EVAL_TAC 483THEN RW_TAC (srw_ss()) [] 484THEN FULL_SIMP_TAC (srw_ss()) []); 485 486 487fun get_take_undef_writing_part_spsr_thm a' wr_sfc_ut_thm lr vt_index mode = 488 489 let val (l,r,rb1)= decompose_term a'; 490 val (l2,r2,rb2)= decompose_term rb1 491 val (l3,r3,rb3)= decompose_term rb2 492 val (l4,r4,rb4)= decompose_term l3 493 val (l5,r5,rb5)= decompose_term r4 494 val (l6,r6,rb6)= decompose_term r5; 495 (* proof of r5 *) 496 val thm1 = LIST_MP [ wr_sfc_ut_thm, 497 (SPECL [``(ExcVectorBase + ^vt_index)``, 498 mode ] branch_to_sfc_ut_thm)] 499 (SPECL [l6,r6,mode] 500 (INST_TYPE [alpha |-> ``:unit``, 501 beta |-> ``:unit``] 502 parT_trans_untouched_thm)); 503 (* proof of r4 *) 504 val thm2 = LIST_MP [ 505 (SPECL [lr, 506 mode] write_lr_reg_sfc_ut_thm), 507 thm1] 508 (SPECL [l5,r5,mode] 509 (INST_TYPE [alpha |-> ``:unit``, 510 beta |-> ``:(unit#unit)``] 511 parT_trans_untouched_thm)); 512 (* proof of l3 *) 513 val thm3 = LIST_MP [ 514 (SPECL [``cpsr:ARMpsr``,mode] write_spsr_sfc_thm), 515 thm2] 516 (SPECL [r4,l4,``cpsr:ARMpsr``,mode] 517 (INST_TYPE [beta |-> ``:unit``, 518 alpha |-> ``:(unit#unit#unit)``] 519 parT_priv_spsr_constraints_after_thm)); 520 (* proof of rb2 *) 521 val thm4 = LIST_MP [ 522 thm3, 523 SPEC mode constT_sfc_ut_thm] 524 (SPECL [r3,l3,``cpsr:ARMpsr``,mode] 525 (INST_TYPE [beta |-> ``:unit``, 526 alpha |-> ``:(unit#unit#unit#unit)``] 527 seqT_priv_spsr_constraints_after_thm)); 528 (* proof of rb1 *) 529 val (thm5 , _) = prove_abs_spsr_const_action (r2, [spfc_first_abs_lemma, 530 spfc_second_abs_lemma], 531 thm4, ``cpsr:ARMpsr``, 532 mode); 533 val thm6 = MP (SPECL [l2,r2,``cpsr:ARMpsr``,mode] 534 (INST_TYPE [beta |-> ``:unit``, 535 alpha |-> ``:(unit#unit)``] 536 seqT_priv_spsr_constraints_before_thm)) thm5; 537 in 538 (GEN_ALL thm6) 539 end 540 541val take_undef_writing_part_spf_thm = 542 save_thm ("take_undef_writing_part_spf_thm", 543 let 544 val a = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 545 ``take_undef_instr_exception <|proc:=0|> ``; 546 val (_, a') = (dest_eq (concl a)) 547 in 548 get_take_undef_writing_part_spsr_thm a' 549 ui_write_cpsr_spsr_ut_thm ``(if cpsr.T 550 then 551 pc ��� 2w:bool[32] 552 else 553 pc ��� 4w)`` ``4w:bool[32]`` ``27w:bool[5]`` 554 end 555); 556 557 558val take_data_abort_writing_part_spf_thm = 559 save_thm ("take_data_abort_writing_part_spf_thm", 560 let 561 val a = SIMP_CONV (bool_ss) [take_data_abort_exception_def] 562 ``take_data_abort_exception <|proc:=0|> ``; 563 val (_, a') = (dest_eq (concl a)); 564 in 565 get_take_undef_writing_part_spsr_thm a' 566 ab_write_cpsr_spsr_ut_thm 567 ``(if cpsr.T 568 then 569 pc:bool[32] 570 else 571 pc ��� 4w)`` ``16w:bool[32]`` ``23w:bool[5]`` 572 end 573); 574 575val take_prefetch_abort_writing_part_spf_thm = 576 save_thm ("take_prefetch_abort_writing_part_spf_thm", 577 let 578 val a = SIMP_CONV (bool_ss) [take_prefetch_abort_exception_def] 579 ``take_prefetch_abort_exception <|proc:=0|> `` 580 val (_, a') = (dest_eq (concl a)) 581 in 582 get_take_undef_writing_part_spsr_thm a' 583 ab_write_cpsr_spsr_ut_thm 584 ``(if cpsr.T 585 then 586 pc:bool[32] 587 else 588 pc ��� 4w)`` ``12w:bool[32]`` ``23w:bool[5]`` 589 end 590); 591 592val take_irq_writing_part_spf_thm = 593 save_thm ("take_irq_writing_part_spf_thm", 594 let 595 val a = SIMP_CONV (bool_ss) [take_irq_exception_def] 596 ``take_irq_exception <|proc:=0|> ``; 597 val (_, a') = (dest_eq (concl a)); 598 in 599 get_take_undef_writing_part_spsr_thm a' 600 irq_write_cpsr_spsr_ut_thm 601 ``(if cpsr.T 602 then 603 pc:bool[32] 604 else 605 pc ��� 4w)`` ``24w:bool[32]`` ``18w:bool[5]`` 606 end 607); 608 609val take_svc_writing_part_spf_thm = 610 save_thm ("take_svc_writing_part_spf_thm", 611 let 612 val a = SIMP_CONV (bool_ss) [take_svc_exception_def] 613 ``take_svc_exception <|proc:=0|> ``; 614 val (_, a') = (dest_eq (concl a)) 615 val (l,r,rbody) = decompose_term a'; 616 in 617 get_take_undef_writing_part_spsr_thm rbody 618 svc_write_cpsr_spsr_ut_thm ``(if cpsr.T 619 then 620 pc ��� 2w:bool[32] 621 else 622 pc ��� 4w)`` ``8w:bool[32]`` ``19w:bool[5]`` 623 end 624); 625 626 627val satisfy_SPSR_constraints_def = 628 Define ` satisfy_SPSR_constraints f m = 629 ! s s' a. 630 (f s = ValueState a s') ==> 631 (~access_violation s') ==> 632 ((s'.psrs(0,CPSR)).M = m) ==> 633 ((s'.psrs (0,get_spsr_by_mode(m))) = (s.psrs(0,CPSR)))`; 634 635 636fun prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 637 wp_thm const_comp_rp_thm sl_elm2 spec_lists 638 ltype = 639 let 640 val (l,r,rb1)= decompose_term te; 641 val spec_list = List.nth(spec_lists,0) 642 val spec_list2 = List.nth(spec_lists,1) 643 val (_,sr) = dest_eq ( concl (SIMP_RULE (srw_ss()) [] 644 (SPECL [``s:arm_state``,r] 645 (INST_TYPE [alpha |-> ``:unit``] 646 fixed_cpsr_thm)))); 647 val (_,simpr,_) = decompose_term sr; 648 649 in 650 RW_TAC (bool_ss) [te_def, 651 satisfy_SPSR_constraints_def] 652 THEN ASSUME_TAC (SPECL [``s:arm_state``,r] 653 (INST_TYPE [alpha |-> ``:unit``] 654 fixed_cpsr_thm)) 655 THEN FULL_SIMP_TAC (srw_ss()) [] 656 THEN FULL_SIMP_TAC (let_ss) [] 657 THEN PAT_X_ASSUM ``X=Y`` (fn thm => THROW_AWAY_TAC (concl thm)) 658 THEN ASSUME_TAC const_comp_rp_thm 659 THEN RW_TAC (srw_ss()) [priv_spsr_constraints_def, 660 priv_spsr_constraints_abs_def] 661 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 662 THEN (Cases_on [QUOTE ("("^(term_to_string l) ^ ") s")] 663 THEN IMP_RES_TAC seqT_access_violation_thm 664 THENL 665 [ RES_TAC 666 THEN RW_TAC (srw_ss()) [] 667 THEN IMP_RES_TAC hlp_seqT_thm 668 THEN PAT_X_ASSUM ``X a' b= ValueState a s'`` 669 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 670 THEN 671 ASSUME_TAC ( SPECL 672 spec_list (GEN_ALL (SIMP_RULE (bool_ss) [priv_spsr_constraints_def] 673 wp_thm))) 674 THEN PAT_X_ASSUM ``X ==> Y`` (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 675 THEN 676 ASSUME_TAC (SPECL spec_list2 fixed_cpsr_thm2) 677 THEN RES_TAC 678 THEN RES_TAC 679 THEN FULL_SIMP_TAC (srw_ss()) [get_spsr_by_mode_def] 680 THEN FULL_SIMP_TAC (let_ss) [] 681 THEN RW_TAC (srw_ss()) [] 682 , 683 IMP_RES_TAC (SPEC simpr ( 684 INST_TYPE [beta |-> ``:unit``, 685 alpha |-> ltype ] 686 hlp_errorT_thm)) 687 THEN 688 PAT_X_ASSUM ``! (s:arm_state) . X `` 689 (fn thm => ASSUME_TAC (SPEC ``s:arm_state`` thm)) 690 THEN RW_TAC (srw_ss()) [] 691 THEN FULL_SIMP_TAC (srw_ss()) [] 692 ]) 693 end; 694 695val take_svc_exception_spsr_thm = 696 store_thm ("take_svc_exception_spsr_thm", 697 let 698 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 699 ``take_svc_exception <|proc:=0|> `` 700 val (_, a) = (dest_eq (concl athm)) 701 val (_,_,rb)= decompose_term a; 702 in 703 `` satisfy_SPSR_constraints 704 ^rb 19w`` 705 end, 706 let 707 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 708 ``take_svc_exception <|proc:=0|> `` 709 val (_, a) = (dest_eq (concl athm)); 710 val (_,_,te)= decompose_term a; 711 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 712 val spec_list = (mk_spec_list sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 713 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list2 (sl_elm2)) 714 val spec_lists = [spec_list] @ [spec_list2]; 715 val te_def = take_svc_exception_def; 716 val fixed_cpsr_thm = fixed_cpsr_undef_svc_thm; 717 val fixed_cpsr_thm2 = fixed_cpsr_undef_svc_thm2; 718 val wp_thm = take_svc_writing_part_spf_thm; 719 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 720 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)``; 721 722 in 723 prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 724 wp_thm const_comp_rp_thm sl_elm2 spec_lists 725 ltype 726 end); 727 728val take_undef_instr_exception_spsr_thm = 729 store_thm ("take_undef_instr_exception_spsr_thm", 730 `` satisfy_SPSR_constraints 731 (take_undef_instr_exception <|proc:=0|>) 27w``, 732 let 733 val athm = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 734 ``take_undef_instr_exception <|proc:=0|> `` 735 val (_, te) = (dest_eq (concl athm)); 736 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 737 val spec_list = (mk_spec_list sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 738 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list2 (sl_elm2)) 739 val spec_lists = [spec_list] @ [spec_list2]; 740 val te_def = take_undef_instr_exception_def; 741 val fixed_cpsr_thm = fixed_cpsr_undef_svc_thm; 742 val fixed_cpsr_thm2 = fixed_cpsr_undef_svc_thm2; 743 val wp_thm = take_undef_writing_part_spf_thm; 744 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 745 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)``; 746 747 in 748 prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 749 wp_thm const_comp_rp_thm sl_elm2 spec_lists 750 ltype 751 end); 752 753 754val take_data_abort_exception_spsr_thm = 755 store_thm ("take_data_abort_exception_spsr_thm", 756 `` satisfy_SPSR_constraints 757 (take_data_abort_exception <|proc:=0|>) 23w``, 758 let 759 val athm = SIMP_CONV (bool_ss) [take_data_abort_exception_def] 760 ``take_data_abort_exception <|proc:=0|> `` 761 val (_, te) = (dest_eq (concl athm)); 762 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))`` 763 val spec_list = (mk_spec_list3 sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 764 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list4 (sl_elm2)) 765 val spec_lists = [spec_list] @ [spec_list2]; 766 val te_def = take_data_abort_exception_def; 767 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm; 768 val fixed_cpsr_thm2 = fixed_cpsr_abt_irq_thm2; 769 val wp_thm = take_data_abort_writing_part_spf_thm; 770 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 771 val ltype = ``:(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr)``; 772 773 in 774 prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 775 wp_thm const_comp_rp_thm sl_elm2 spec_lists 776 ltype 777 end); 778 779 780val take_prefetch_abort_exception_spsr_thm = 781 store_thm ("take_prefetch_abort_exception_spsr_thm", 782 `` satisfy_SPSR_constraints 783 (take_prefetch_abort_exception <|proc:=0|>) 23w``, 784 let 785 val athm = SIMP_CONV (bool_ss) [take_prefetch_abort_exception_def] 786 ``take_prefetch_abort_exception <|proc:=0|> `` 787 val (_, te) = (dest_eq (concl athm)); 788 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))`` 789 val spec_list = (mk_spec_list3 sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 790 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list4 (sl_elm2)) 791 val spec_lists = [spec_list] @ [spec_list2]; 792 val te_def = take_prefetch_abort_exception_def; 793 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm; 794 val fixed_cpsr_thm2 = fixed_cpsr_abt_irq_thm2; 795 val wp_thm = take_prefetch_abort_writing_part_spf_thm; 796 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 797 val ltype = ``:(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr)``; 798 799 in 800 prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 801 wp_thm const_comp_rp_thm sl_elm2 spec_lists 802 ltype 803 end); 804 805 806val take_irq_exception_spsr_thm = 807 store_thm ("take_irq_exception_spsr_thm", 808 `` satisfy_SPSR_constraints 809 (take_irq_exception <|proc:=0|>) 18w``, 810 let 811 val athm = SIMP_CONV (bool_ss) [take_irq_exception_def] 812 ``take_irq_exception <|proc:=0|> `` 813 val (_, te) = (dest_eq (concl athm)); 814 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))`` 815 val spec_list = (mk_spec_list3 sl_elm2)@[``b:arm_state``, ``s':arm_state``,``a:unit``] 816 val spec_list2 = [``b:arm_state``] @ List.rev (mk_spec_list4 (sl_elm2)) 817 val spec_lists = [spec_list] @ [spec_list2]; 818 val te_def = take_irq_exception_def; 819 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm; 820 val fixed_cpsr_thm2 = fixed_cpsr_abt_irq_thm2; 821 val wp_thm = take_irq_writing_part_spf_thm; 822 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 823 val ltype = ``:(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr)``; 824 825 in 826 prove_take_exception_spsr_constraints te te_def fixed_cpsr_thm fixed_cpsr_thm2 827 wp_thm const_comp_rp_thm sl_elm2 spec_lists 828 ltype 829 end); 830 831 832 833val preserve_priv_bisimilarity_def = 834Define `preserve_priv_bisimilarity f m = 835 ! s1 s1' a1 s2 s2' a2 g. 836 (f s1 = ValueState a1 s1') ==> 837 (f s2 = ValueState a2 s2') ==> 838 (~access_violation s1') ==> 839 (~access_violation s2') ==> 840 (s1.registers(0,RName_PC) = s2.registers(0,RName_PC)) ==> 841 ((s1.psrs(0,CPSR)) = (s2.psrs(0,CPSR))) ==> 842 ((s1'.psrs(0,CPSR)) = (s2'.psrs(0,CPSR))) ==> 843 ((s1'.psrs(0,CPSR)).M = m) ==> 844 ((s2'.psrs(0,CPSR)).M = m) ==> 845 (priv_mode_similar (g:bool[32]) s2' s1')`; 846 847 848(* 849val LR_SPSR_equality_implies_priv_bisimilarity_thm = 850 new_axiom ("LR_SPSR_equality_implies_priv_bisimilarity_thm", 851 ``! f m v. 852 satisfy_SPSR_constraints f m 853 ==> 854 satisfy_LR_constraints f m v 855 ==> 856 preserve_priv_bisimilarity f m 857 ``); 858*) 859val LR_SPSR_equality_implies_priv_bisimilarity_thm = 860 store_thm ("LR_SPSR_equality_implies_priv_bisimilarity_thm", 861 ``! f m v. 862 satisfy_SPSR_constraints f m 863 ==> 864 satisfy_LR_constraints f m v 865 ==> 866 preserve_priv_bisimilarity f m 867 ``, 868 RW_TAC (srw_ss()) [satisfy_SPSR_constraints_def, 869 satisfy_LR_constraints_def, 870 preserve_priv_bisimilarity_def, 871 ARM_MODE_def,priv_mode_similar_def, 872 ARM_READ_CPSR_def] 873 THEN UNABBREV_ALL_TAC 874 THEN NTAC 2 ( RES_TAC 875 THEN FULL_SIMP_TAC (srw_ss()) [get_pc_value_def] 876 THEN RW_TAC (srw_ss()) [])); 877 878val take_undef_instr_exception_priv_mode_similar_thm = 879 store_thm ("take_undef_instr_exception_priv_mode_similar_thm", 880``preserve_priv_bisimilarity (take_undef_instr_exception <|proc:=0|>) 27w`` 881 , 882 MP_TAC (SPEC ``27w:bool[5]`` take_undef_instr_exception_LR_thm) 883 THEN MP_TAC take_undef_instr_exception_spsr_thm 884 THEN METIS_TAC [LR_SPSR_equality_implies_priv_bisimilarity_thm] ); 885 886 887val take_data_abort_exception_priv_mode_similar_thm = 888 store_thm ("take_data_abort_exception_priv_mode_similar_thm", 889``preserve_priv_bisimilarity (take_data_abort_exception <|proc:=0|>) 23w`` 890 , 891 MP_TAC (SPEC ``23w:bool[5]`` take_data_abort_exception_LR_thm) 892 THEN MP_TAC take_data_abort_exception_spsr_thm 893 THEN METIS_TAC [LR_SPSR_equality_implies_priv_bisimilarity_thm] ); 894 895val take_prefetch_abort_exception_priv_mode_similar_thm = 896 store_thm ("take_prefetch_abort_exception_priv_mode_similar_thm", 897``preserve_priv_bisimilarity (take_prefetch_abort_exception <|proc:=0|>) 23w`` 898 , 899 MP_TAC (SPEC ``23w:bool[5]`` take_prefetch_abort_exception_LR_thm) 900 THEN MP_TAC take_prefetch_abort_exception_spsr_thm 901 THEN METIS_TAC [LR_SPSR_equality_implies_priv_bisimilarity_thm] ); 902 903val take_irq_exception_priv_mode_similar_thm = 904 store_thm ("take_irq_exception_priv_mode_similar_thm", 905``preserve_priv_bisimilarity (take_irq_exception <|proc:=0|>) 18w`` 906 , 907 MP_TAC (SPEC ``18w:bool[5]`` take_irq_exception_LR_thm) 908 THEN MP_TAC take_irq_exception_spsr_thm 909 THEN METIS_TAC [LR_SPSR_equality_implies_priv_bisimilarity_thm] ); 910 911val take_svc_exception_priv_mode_similar_thm = 912 store_thm ("take_svc_exception_priv_mode_similar_thm", 913 let 914 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 915 ``take_svc_exception <|proc:=0|> `` 916 val (_, a) = (dest_eq (concl athm)) 917 val (_,_,rb)= decompose_term a 918 in 919 ``preserve_priv_bisimilarity ^rb 19w`` 920 end 921 , 922 MP_TAC (SPEC ``19w:bool[5]`` take_svc_exception_LR_thm) 923 THEN MP_TAC take_svc_exception_spsr_thm 924 THEN METIS_TAC [LR_SPSR_equality_implies_priv_bisimilarity_thm] ); 925 926 927val _ = export_theory(); 928