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_cpsr_pcTheory priv_constraints_lrTheory priv_constraints_bisimTheory tacticsLib; 5open user_lemma_basicsTheory; 6(* user_lemma_primitive_operationsTheory;*) 7open ARM_proverLib; 8 9(****************************************************************) 10(* SWITCHING LEMMA *) 11(* Narges *) 12(****************************************************************) 13 14val _ = new_theory("switching_lemma"); 15 16val let_ss = simpLib.mk_simpset [boolSimps.LET_ss]; 17 18val _ = set_trace "Goalstack.show_proved_subtheorems" 0; 19 20val tautology_fun_def = Define `tautology_fun (g:word32) 21 (s1:arm_state) (s2:arm_state) = 22 (T)`; 23 24val have_same_mem_accesses_def = 25Define `have_same_mem_accesses (g:word32) 26 (s1:arm_state) (s2:arm_state) = 27 (s1.accesses = s2.accesses) /\ 28 (s1.memory = s2.memory)`; 29 30val assert_mode_no_access_violation_def = 31Define `assert_mode_no_access_violation k s= 32 (~ access_violation s) /\ 33 ((s.psrs (0,CPSR)).M = k) 34 `; 35 36val assert_mode_access_violation_def = 37Define `assert_mode_access_violation k s= 38 (access_violation s) /\ 39 ((s.psrs (0,CPSR)).M = k) 40 `; 41 42 43val take_svc_exception1_def = 44Define `take_svc_exception1 = 45(read_reg <|proc := 0|> 15w ||| exc_vector_base <|proc := 0|> 46 ||| read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 47 ||| read_sctlr <|proc := 0|>) >>= 48 (��(pc,ExcVectorBase,cpsr,scr,sctlr). 49 (condT (cpsr.M = 22w) 50 (write_scr <|proc := 0|> (scr with NS := F)) 51 ||| write_cpsr <|proc := 0|> (cpsr with M := 19w)) >>= 52 (��(u1,u2). 53 (write_spsr <|proc := 0|> cpsr 54 ||| write_reg <|proc := 0|> 14w 55 (if cpsr.T then 56 pc + 0xFFFFFFFEw 57 else 58 pc + 0xFFFFFFFCw) 59 ||| read_cpsr <|proc := 0|> >>= 60 (��cpsr. 61 write_cpsr <|proc := 0|> 62 (cpsr with 63 <|IT := 0w; J := F; E := sctlr.EE; I := T; 64 T := sctlr.TE|>)) 65 ||| branch_to <|proc := 0|> 66 (ExcVectorBase + 8w)) >>= 67 (��(u1,u2,u3,u4). constT ())))`; 68 69val trans_tautology_fun_thm = 70 store_thm("trans_tautology_fun_thm", 71 ``trans_fun tautology_fun``, 72 RW_TAC let_ss [ trans_fun_def,tautology_fun_def] 73 THEN RW_TAC (srw_ss()) [] ); 74 75val refl_rel_tautology_fun_thm = 76 store_thm("refl_rel_tautology_fun_thm", 77 ``refl_rel tautology_fun``, 78 RW_TAC (srw_ss()) [refl_rel_def, tautology_fun_def] 79 ); 80 81val reflex_tautology_fun_thm = 82 store_thm("reflex_tautology_fun_thm", 83 ``!u. (reflexive_comp tautology_fun (assert_mode u))`` 84 , 85 RW_TAC (srw_ss()) [reflexive_comp_def,tautology_fun_def,assert_mode_def]); 86 87 88val trans_have_same_mem_accesses_thm = 89 store_thm("trans_have_same_mem_accesses_thm", 90 ``trans_fun have_same_mem_accesses``, 91 RW_TAC let_ss [ trans_fun_def,have_same_mem_accesses_def] 92 THEN RW_TAC (srw_ss()) [] ); 93 94val reflex_have_same_mem_accesses_thm = 95 store_thm("reflex_have_same_mem_accesses_thm", 96 ``!u. (reflexive_comp have_same_mem_accesses (assert_mode u))`` 97 , 98 RW_TAC (srw_ss()) [reflexive_comp_def,have_same_mem_accesses_def,assert_mode_def]); 99 100val preserve_relation_in_priv_mode_thm_tac = 101 let 102 val tac = UNDISCH_ALL_TAC 103 THEN FULL_SIMP_TAC (bool_ss) [ARM_MODE_def,ARM_READ_CPSR_def, 104 assert_mode_def, 105 have_same_mem_accesses_def] 106 THEN RW_TAC (srw_ss()) [] 107 THEN RW_TAC (srw_ss()) [] 108 THEN IMP_RES_TAC similar_states_have_same_av_thm1 109 THEN IMP_RES_TAC similar_states_have_same_mode_thm 110 111 THEN IMP_RES_TAC untouched_states_implies_mmu_setup_thm 112 THEN IMP_RES_TAC trivially_untouched_av_lem2 113 THEN FULL_SIMP_TAC (srw_ss()) [] 114 in 115 RW_TAC (bool_ss) [preserve_relation_mmu_def,tautology_fun_def, 116 preserve_priv_bisimilarity_def, 117 satisfy_priv_constraints_v3_def, 118 satisfy_priv_constraints_v2a_def, 119 satisfy_priv_constraints_v2_def] 120 THEN PAT_X_ASSUM ``���g s1 s2.X`` (fn thm => 121 ASSUME_SPECL_TAC 122 [``g:bool[32]``,``s1:arm_state``, 123 ``s2:arm_state``] thm) 124 THEN FULL_SIMP_TAC (bool_ss) 125 [assert_mode_no_access_violation_def] 126 THEN UNDISCH_ALL_TAC 127 THEN FULL_SIMP_TAC (bool_ss) [] 128 THEN RW_TAC (srw_ss()) [] 129 THEN RW_TAC (srw_ss()) [] 130 THENL 131 [PAT_X_ASSUM ``���g s1 s2 a .X`` 132 (fn thm => 133 ASSUME_SPECL_TAC [``g:bool[32]``,``s1:arm_state``, 134 ``s1':arm_state``,``a:'a``] thm) THEN tac, 135 PAT_X_ASSUM ``���g s1 s2 a .X`` 136 (fn thm => 137 ASSUME_SPECL_TAC [``g:bool[32]``,``s2:arm_state``, 138 ``s2':arm_state``,``a:'a``] thm) 139 THEN tac, 140 PAT_X_ASSUM ``���g s1 s2 a .X`` 141 (fn thm => 142 THROW_AWAY_TAC (concl thm)) 143 THEN FULL_SIMP_TAC (bool_ss) [ARM_MODE_def,ARM_READ_CPSR_def, 144 assert_mode_def, 145 have_same_mem_accesses_def] 146 THEN IMP_RES_TAC similar_states_have_same_av_thm1 147 THEN IMP_RES_TAC similar_states_have_same_mode_thm 148 THEN IMP_RES_TAC untouched_states_implies_mmu_setup_thm 149 THEN IMP_RES_TAC trivially_untouched_av_lem2 150 THEN IMP_RES_TAC similar_states_have_same_cpsr_thm 151 THEN IMP_RES_TAC similar_states_have_same_pc_thm 152 THEN RES_TAC 153 THEN METIS_TAC []] 154 end 155 156val preserve_relation_in_priv_mode_v3_thm = 157 store_thm ("preserve_relation_in_priv_mode_v3_thm", 158 ``! f m n. 159 preserve_priv_bisimilarity f n ==> 160 (satisfy_priv_constraints_v3 f m n )==> 161 (preserve_relation_mmu 162 f 163 (assert_mode_no_access_violation m ) 164 (assert_mode n) have_same_mem_accesses tautology_fun) ==> 165 preserve_relation_mmu 166 f 167 (assert_mode_no_access_violation m ) 168 (assert_mode n) priv_mode_constraints_v3 priv_mode_similar``, 169 preserve_relation_in_priv_mode_thm_tac 170 ); 171 172val preserve_relation_in_priv_mode_v2a_thm = 173 store_thm ("preserve_relation_in_priv_mode_v2a_thm", 174 ``! f m n. 175 preserve_priv_bisimilarity f n ==> 176 (satisfy_priv_constraints_v2a f m n )==> 177 (preserve_relation_mmu 178 f 179 (assert_mode_no_access_violation m ) 180 (assert_mode n) have_same_mem_accesses tautology_fun) ==> 181 preserve_relation_mmu 182 f 183 (assert_mode_no_access_violation m ) 184 (assert_mode n) priv_mode_constraints_v2a priv_mode_similar``, 185 preserve_relation_in_priv_mode_thm_tac 186 ); 187 188val preserve_relation_in_priv_mode_v2_thm = 189 store_thm ("preserve_relation_in_priv_mode_v2_thm", 190 ``! f m n. 191 preserve_priv_bisimilarity f n ==> 192 (satisfy_priv_constraints_v2 f m n )==> 193 (preserve_relation_mmu 194 f 195 (assert_mode_no_access_violation m ) 196 (assert_mode n) have_same_mem_accesses tautology_fun) ==> 197 preserve_relation_mmu 198 f 199 (assert_mode_no_access_violation m ) 200 (assert_mode n) priv_mode_constraints_v2 priv_mode_similar``, 201 preserve_relation_in_priv_mode_thm_tac 202 ); 203 204val access_violation_implies_no_mode_changing_thm = 205 store_thm ("access_violation_implies_no_mode_changing_thm", 206 ``!f g . const_comp f ==> 207 (preserve_relation_mmu f (assert_mode 16w) 208 (assert_mode 16w) priv_mode_constraints_v3 priv_mode_similar 209 ==> 210 (preserve_relation_mmu (f>>=g) (assert_mode_access_violation 16w ) 211 (assert_mode_access_violation 16w ) 212 priv_mode_constraints_v3 priv_mode_similar)) 213 /\ 214 ( 215 preserve_relation_mmu f (assert_mode 16w) 216 (assert_mode 16w) priv_mode_constraints_v2a priv_mode_similar 217 ==> 218 (preserve_relation_mmu (f>>=g) (assert_mode_access_violation 16w ) 219 (assert_mode_access_violation 16w ) 220 priv_mode_constraints_v2a priv_mode_similar)) 221``, 222 RW_TAC (srw_ss()) [preserve_relation_mmu_def, 223 seqT_def, 224 const_comp_def, 225 assert_mode_def, 226 assert_mode_access_violation_def, 227 ARM_MODE_def, 228 ARM_READ_CPSR_def] 229 THEN PAT_X_ASSUM ``! g s1 s2.X`` 230 (fn thm => ASSUME_SPECL_TAC [``g':bool[32]``, 231 ``s1:arm_state``, 232 ``s2:arm_state``] thm) 233 THEN RES_TAC 234 THEN PAT_X_ASSUM ``! s s x.X`` 235 (fn thm => 236 ASSUME_SPECL_TAC [``s1:arm_state``, 237 ``s1':arm_state``, 238 ``a:'a``] thm 239 THEN ASSUME_SPECL_TAC [``s2:arm_state``, 240 ``s2':arm_state``, 241 ``a:'a``] thm) 242 THEN RES_TAC 243 THEN FULL_SIMP_TAC (srw_ss()) []); 244 245 246val access_violation_implies_no_mode_changing_v1_thm = 247 store_thm ("access_violation_implies_no_mode_changing_v1_thm", 248 ``!f g . const_comp f ==> 249 (preserve_relation_mmu f (assert_mode 16w) 250 (assert_mode 16w) priv_mode_constraints_v3 priv_mode_similar 251 ==> 252 (preserve_relation_mmu (f>>=g) (assert_mode_access_violation 16w ) 253 (assert_mode_access_violation 16w ) 254 priv_mode_constraints_v3 priv_mode_similar)) 255 /\ 256 ( 257 preserve_relation_mmu f (assert_mode 16w) 258 (assert_mode 16w) priv_mode_constraints_v2 priv_mode_similar 259 ==> 260 (preserve_relation_mmu (f>>=g) (assert_mode_access_violation 16w ) 261 (assert_mode_access_violation 16w ) 262 priv_mode_constraints_v2 priv_mode_similar)) 263``, 264 RW_TAC (srw_ss()) [preserve_relation_mmu_def, 265 seqT_def, 266 const_comp_def, 267 assert_mode_def, 268 assert_mode_access_violation_def, 269 ARM_MODE_def, 270 ARM_READ_CPSR_def] 271 THEN PAT_X_ASSUM ``! g s1 s2.X`` 272 (fn thm => ASSUME_SPECL_TAC [``g':bool[32]``, 273 ``s1:arm_state``, 274 ``s2:arm_state``] thm) 275 THEN RES_TAC 276 THEN PAT_X_ASSUM ``! s s x.X`` 277 (fn thm => 278 ASSUME_SPECL_TAC [``s1:arm_state``, 279 ``s1':arm_state``, 280 ``a:'a``] thm 281 THEN ASSUME_SPECL_TAC [``s2:arm_state``, 282 ``s2':arm_state``, 283 ``a:'a``] thm) 284 THEN RES_TAC 285 THEN FULL_SIMP_TAC (srw_ss()) []); 286 287 288val user_pr_taut_imp_priv_pr_thm = 289 store_thm ("user_pr_taut_imp_priv_pr_thm", 290``!f. preserve_relation_mmu 291 (f) 292 (assert_mode 16w ) 293 (assert_mode 16w ) tautology_fun tautology_fun 294 ==> 295 ((preserve_relation_mmu 296 (f) 297 (assert_mode 16w ) 298 (assert_mode 16w ) 299 priv_mode_constraints_v3 priv_mode_similar) 300 /\ 301 (preserve_relation_mmu 302 (f) 303 (assert_mode 16w ) 304 (assert_mode 16w ) 305 priv_mode_constraints_v2a priv_mode_similar) 306 /\ 307 (preserve_relation_mmu 308 (f) 309 (assert_mode 16w ) 310 (assert_mode 16w ) 311 priv_mode_constraints_v2 priv_mode_similar))`` 312, 313 RW_TAC (srw_ss()) [preserve_relation_mmu_def, 314 assert_mode_def, 315 tautology_fun_def] 316 THEN PAT_X_ASSUM ``! g s1 s2.X`` 317 (fn thm => ASSUME_SPECL_TAC [``g:bool[32]``, 318 ``s1:arm_state``, 319 ``s2:arm_state``] thm) 320 THEN RES_TAC 321 THEN FULL_SIMP_TAC (srw_ss()) [priv_mode_constraints_v3_def, 322 priv_mode_constraints_v2a_def, 323 priv_mode_constraints_v2_def, 324 priv_mode_constraints_v1_def, 325 priv_mode_similar_def, 326 ARM_MODE_def, 327 ARM_READ_CPSR_def 328 ] 329 THEN FULL_SIMP_TAC (let_ss) [untouched_def,ARM_MODE_def, 330 ARM_READ_CPSR_def] 331 THEN RW_TAC (srw_ss()) [] 332); 333 334 335 336val deduce_pr_from_pr_av_and_pr_no_av_thm = 337 store_thm ("deduce_pr_from_pr_av_and_pr_no_av_thm", 338``! m f uf uy is . 339 preserve_relation_mmu 340 f 341 (assert_mode_access_violation 16w ) 342 (assert_mode_access_violation 16w ) 343 uf uy 344 ==> 345 preserve_relation_mmu 346 f 347 (assert_mode_no_access_violation 16w ) 348 (assert_mode m) 349 uf uy 350 ==> 351 preserve_relation_mmu 352 f 353 (assert_mode 16w) 354 (comb_mode 16w m ) 355 uf uy 356 ``, 357 RW_TAC (srw_ss()) [preserve_relation_mmu_def] 358 THEN NTAC 2(PAT_X_ASSUM ``! g s1 s2.X`` 359 (fn thm => 360 ASSUME_SPECL_TAC [``g:bool[32]``, 361 ``s1:arm_state``, 362 ``s2:arm_state``] thm)) 363 THEN RES_TAC 364 THEN FULL_SIMP_TAC (srw_ss()) 365 [ assert_mode_access_violation_def, 366 assert_mode_no_access_violation_def, 367 assert_mode_def, 368 assert_mode_def, 369 comb_mode_def, 370 ARM_MODE_def, 371 ARM_READ_CPSR_def] 372 THEN Cases_on `access_violation s1` 373 THEN RES_TAC 374 THEN IMP_RES_TAC (SPEC ``16w:bool[5]`` similar_states_have_same_mode_thm) 375 THEN IMP_RES_TAC (similar_states_have_same_av_thm1) 376 THEN IMP_RES_TAC (similar_states_have_same_av_thm2) 377 THEN FULL_SIMP_TAC (srw_ss()) [] 378 ); 379 380 381(*val uy1 = ``priv_mode_similar``;*) 382val uf1 = ``have_same_mem_accesses``; 383val uy1 = ``tautology_fun``; 384val uargs = [uf1,uy1,``27w:bool[5]``,``_pthm``]; 385val pthms = [trans_have_same_mem_accesses_thm, 386 reflex_have_same_mem_accesses_thm, 387 tautology_fun_def, 388 have_same_mem_accesses_def, 389 errorT_thm]; 390 391fun prove_write_read_bisimilarity trm1 trm2 = 392 RW_TAC (let_ss) [preserve_relation_mmu_def, 393 read_cpsr_def,read__psr_def,readT_def, 394 write_cpsr_def,write__psr_def,writeT_def, 395 similar_def,untouched_def, have_same_mem_accesses_def, 396 seqT_def,errorT_def,tautology_fun_def, 397 priv_mode_similar_def,assert_mode_def] 398 THEN RW_TAC (srw_ss()) [] 399 THEN FULL_SIMP_TAC (srw_ss()) [] 400 THEN (FIRST_PROVE [ 401 UNDISCH_TAC ``s1.psrs (0,CPSR) = 402 s2.psrs (0,CPSR)`` 403 THEN EVAL_TAC 404 THEN RW_TAC (srw_ss()) [] 405 THEN RW_TAC (srw_ss()) [], 406 UNDISCH_TAC ``psr ��� CPSR`` 407 THEN EVAL_TAC 408 THEN RW_TAC (srw_ss()) [] 409 THEN RW_TAC (srw_ss()) [], 410 UNDISCH_TAC ``ARM_MODE s1 = 27w`` THEN 411 UNDISCH_TAC ``ARM_MODE s2 = 27w`` THEN 412 UNDISCH_TAC ``s1.psrs (0,CPSR) = s2.psrs (0,CPSR)`` 413 THEN EVAL_TAC 414 THEN RW_TAC (srw_ss()) [] 415 THEN RW_TAC (srw_ss()) [], 416 (UNDISCH_TAC ``equal_user_register s1 s2`` 417 THEN EVAL_TAC 418 THEN RW_TAC (srw_ss()) []), 419 ASSUME_TAC (SPECL [``s1:arm_state``, 420 trm1, ``g:bool[32]``] 421 trivially_untouched_av_lem2) 422 THEN ASSUME_TAC ( 423 SPECL [``s2:arm_state``, 424 trm2, ``g:bool[32]``] 425 trivially_untouched_av_lem2) 426 THEN RES_TAC 427 THEN FULL_SIMP_TAC (srw_ss()) [] 428 THEN METIS_TAC [] ]); 429 430 431val read_write_cpsr_abt_irq_thm = 432 store_thm("read_write_cpsr_abt_irq_thm", 433 ``!u. (u<>16w) ==> 434 preserve_relation_mmu 435 (read_cpsr <|proc:=0|> >>= 436 (��cpsr. 437 write_cpsr <|proc:=0|> 438 (cpsr with 439 <|I := T; 440 A := 441 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 442 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 443 E := sctlr.EE|>))) 444 (assert_mode u) (assert_mode u) ^uf1 ^uy1``, 445 let val trm1 = `` (s1 with 446 psrs updated_by 447 ((0,CPSR) =+ 448 s1.psrs (0,CPSR) with 449 <|IT := 0w; J := F; E := sctlr.EE; 450 A := 451 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 452 (s2.psrs (0,CPSR)).A); I := T; T := sctlr.TE|>))`` 453 val trm2 = `` (s2 with 454 psrs updated_by 455 ((0,CPSR) =+ 456 s2.psrs (0,CPSR) with 457 <|IT := 0w; J := F; E := sctlr.EE; 458 A := 459 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 460 (s2.psrs (0,CPSR)).A); I := T; T := sctlr.TE|>))`` 461 in 462 prove_write_read_bisimilarity trm1 trm2 463 end 464 ); 465 466val read_write_cpsr_undef_svc_thm = 467 store_thm("read_write_cpsr_undef_svc_thm", 468 ``!u. (u<>16w) ==> preserve_relation_mmu 469 (read_cpsr <|proc:=0|> >>= 470 (��cpsr. write_cpsr <|proc:=0|> 471 (cpsr with 472 <|IT := 0w; J := F; E := sctlr.EE; 473 I := T; T := sctlr.TE|>))) 474 (assert_mode u) (assert_mode u) ^uf1 ^uy1``, 475 let val trm1 = `` (s1 with 476 psrs updated_by 477 ((0,CPSR) =+ 478 s1.psrs (0,CPSR) with 479 <|IT := 0w; J := F; E := sctlr.EE; 480 I := T; T := sctlr.TE|>))`` 481 val trm2 = `` (s2 with 482 psrs updated_by 483 ((0,CPSR) =+ 484 s2.psrs (0,CPSR) with 485 <|IT := 0w; J := F; E := sctlr.EE; 486 I := T; T := sctlr.TE|>))`` 487 in 488 prove_write_read_bisimilarity trm1 trm2 489 end 490 ); 491 492 493val write_scr_cpsr_thm = 494 store_thm("write_scr_cpsr_thm", 495 `` ���g s1 s2 comp scr u. 496 ((comp = (condT (F) (write_scr <|proc := 0|> (scr with NS := F)) 497 ||| write_cpsr <|proc := 0|> ((s1.psrs (0,CPSR) with M := u)))) \/ 498 (comp = (condT (F) (write_scr <|proc := 0|> (scr with NS := F)) 499 ||| write_cpsr <|proc := 0|> ((s2.psrs (0,CPSR) with M := u))))) ==> 500 (~access_violation s1)==> 501 mmu_requirements s1 g ��� 502 mmu_requirements s2 g ��� 503 similar g s1 s2 ��� 504 (assert_mode 16w s1) ==> 505 (assert_mode 16w s2) ==> 506 (���a s1' s2'. 507 ( comp s1 = ValueState a s1') ��� 508 ( comp s2 = ValueState a s2') ��� 509 untouched g s1 s1' ��� untouched g s2 s2' 510 ��� (assert_mode u s1') /\ 511 (assert_mode u s2') /\ 512 (^uf1 g s1 s1') ��� 513 (^uf1 g s2 s2') /\ 514 similar g s1' s2' /\ 515 (~access_violation s1')/\ 516 (~access_violation s2')) ��� 517 ���e. (comp s1 = Error e) ��� (comp s2 = Error e)``, 518 let val trm1 = ``(s1 with 519 psrs updated_by ((0,CPSR) =+ s2.psrs (0,CPSR) with M := u))`` 520 val trm2 = ``(s2 with 521 psrs updated_by ((0,CPSR) =+ s2.psrs (0,CPSR) with M := u))`` 522 in 523 RW_TAC (let_ss) [preserve_relation_mmu_def, 524 write_cpsr_def,write__psr_def, 525 writeT_def,similar_def,untouched_def, 526 parT_def,constT_def,seqT_def,errorT_def, 527 tautology_fun_def, 528 priv_mode_similar_def,assert_mode_def, 529 condT_def,ARM_MODE_def, 530 ARM_READ_CPSR_def,have_same_mem_accesses_def] 531 THEN FULL_SIMP_TAC (srw_ss()) [] 532 THEN RW_TAC (srw_ss()) [] 533 THEN 534 FIRST_PROVE[ 535 (TRY (UNDISCH_TAC ``psr ��� CPSR``)) 536 THEN (TRY (UNDISCH_TAC 537 ``s1.psrs (0,CPSR) = s2.psrs (0,CPSR)``)) 538 THEN EVAL_TAC 539 THEN RW_TAC (srw_ss()) [] 540 THEN FULL_SIMP_TAC (let_ss) [], 541 UNDISCH_TAC ``equal_user_register s1 s2`` 542 THEN EVAL_TAC 543 THEN RW_TAC (srw_ss()) [] 544 , 545 ASSUME_TAC (SPECL [``s1:arm_state``, 546 trm1, ``g:bool[32]``] 547 trivially_untouched_av_lem2) 548 THEN ASSUME_TAC ( 549 SPECL [``s2:arm_state``, 550 trm2, ``g:bool[32]``] 551 trivially_untouched_av_lem2) 552 THEN RES_TAC 553 THEN FULL_SIMP_TAC (srw_ss()) [] 554 THEN METIS_TAC [] 555 , 556 TRY(UNDISCH_TAC 557 `` (((0,CPSR) =+ cpsr with M := u) s1.psrs (0,CPSR)).M = 16w``) 558 THEN (TRY(UNDISCH_TAC 559 `` (((0,CPSR) =+ cpsr with M := u) s2.psrs (0,CPSR)).M = 16w``)) 560 THEN EVAL_TAC 561 THEN RW_TAC (srw_ss()) []] 562 end 563 ); 564 565 566(* ================================================+++++========================== *) 567(* proof of preserve relation of write_spsr in no access violation case *) 568(* =====================================================+++++===================== *) 569 570 571val prove_write__psr_thm = 572fn mode => fn spsr => 573 let 574 val trm1 = `` (s1 with psrs updated_by ((0,^spsr) =+ cpsr with M := 16w))`` 575 val trm2 = `` (s2 with psrs updated_by ((0,^spsr) =+ cpsr with M := 16w))`` 576 in 577 RW_TAC (srw_ss()) [preserve_relation_mmu_def, 578 read_cpsr_def,read__psr_def,readT_def, 579 write_cpsr_def,write__psr_def,writeT_def, 580 similar_def,untouched_def, 581 seqT_def,errorT_def,tautology_fun_def, 582 priv_mode_similar_def, 583 assert_mode_def,have_same_mem_accesses_def] 584 THEN RW_TAC (srw_ss()) [] 585 THEN FULL_SIMP_TAC (let_ss) [] 586 THEN NTAC 9 (FIRST_PROVE [ 587 UNDISCH_TAC ``s1.psrs (0,CPSR) = s2.psrs (0,CPSR)`` 588 THEN EVAL_TAC 589 THEN RW_TAC (srw_ss()) [] 590 THEN RW_TAC (srw_ss()) [], 591 UNDISCH_TAC ``psr ��� CPSR`` 592 THEN TRY (UNDISCH_TAC ``psr ��� ^spsr``) 593 THEN EVAL_TAC 594 THEN RW_TAC (srw_ss()) [] 595 THEN RW_TAC (srw_ss()) [], 596 UNDISCH_TAC ``ARM_MODE s1 = ^mode`` THEN 597 UNDISCH_TAC ``ARM_MODE s2 = ^mode`` THEN 598 UNDISCH_TAC ``s1.psrs (0,CPSR) = s2.psrs (0,CPSR)`` 599 THEN EVAL_TAC 600 THEN RW_TAC (srw_ss()) [] 601 THEN RW_TAC (srw_ss()) [], 602 UNDISCH_TAC ``equal_user_register s1 s2`` 603 THEN EVAL_TAC 604 THEN RW_TAC (srw_ss()) [], 605 ASSUME_TAC (SPECL [``s1:arm_state``, 606 trm1, ``g:bool[32]``] 607 trivially_untouched_av_lem2) 608 THEN ASSUME_TAC ( 609 SPECL [``s2:arm_state``, 610 trm2, ``g:bool[32]``] 611 trivially_untouched_av_lem2) 612 THEN RES_TAC 613 THEN FULL_SIMP_TAC (srw_ss()) [] 614 THEN METIS_TAC [] ]) 615 end; 616 617 618val write__psr_und_thm = 619 store_thm("write__psr_und_thm", 620 `` preserve_relation_mmu (write__psr <|proc := 0|> 621 (SPSR_und) (cpsr with M := 16w)) 622 (assert_mode 27w) (assert_mode 27w) ^uf1 ^uy1 ``, 623 prove_write__psr_thm ``27w:bool[5]`` ``SPSR_und``); 624 625val write__psr_svc_thm = 626 store_thm("write__psr_undef_thm", 627 `` preserve_relation_mmu (write__psr <|proc := 0|> 628 (SPSR_svc) (cpsr with M := 16w)) 629 (assert_mode 19w) (assert_mode 19w) ^uf1 ^uy1 ``, 630 prove_write__psr_thm ``19w:bool[5]`` ``SPSR_svc``); 631 632val write__psr_irq_thm = 633 store_thm("write__psr_irq_thm", 634 `` preserve_relation_mmu (write__psr <|proc := 0|> 635 (SPSR_irq) (cpsr with M := 16w)) 636 (assert_mode 18w) (assert_mode 18w) ^uf1 ^uy1 ``, 637 prove_write__psr_thm ``18w:bool[5]`` ``SPSR_irq``); 638 639val write__psr_fiq_thm = 640 store_thm("write__psr_fiq_thm", 641 `` preserve_relation_mmu (write__psr <|proc := 0|> 642 (SPSR_fiq) (cpsr with M := 16w)) 643 (assert_mode 17w) (assert_mode 17w) ^uf1 ^uy1 ``, 644 prove_write__psr_thm ``17w:bool[5]`` ``SPSR_fiq``); 645 646val write__psr_abt_thm = 647 store_thm("write__svc_abt_thm", 648 `` preserve_relation_mmu (write__psr <|proc := 0|> 649 (SPSR_abt) (cpsr with M := 16w)) 650 (assert_mode 23w) (assert_mode 23w) ^uf1 ^uy1 ``, 651 prove_write__psr_thm ``23w:bool[5]`` ``SPSR_abt``); 652 653 654 655val prove_write_spsr_thm = 656fn mode => fn spsr => 657 let 658 val (l,r,rb) = 659 decompose_term (rhs (concl ( 660 SIMP_CONV (srw_ss()) [write_spsr_def] 661 ``(write_spsr <|proc := 0|> (cpsr with M := 16w))``))); 662 in 663 RW_TAC (srw_ss()) [write_spsr_def] 664 THEN ASSUME_TAC (SIMP_RULE (bool_ss) [] 665 (SPECL [r, 666 ``(assert_mode ^mode)``, uf1,uy1, mode] 667 (INST_TYPE [alpha |-> ``:unit``] 668 switching_lemma_helperTheory.cpsr_simp_rel_lem))) 669 THEN FULL_SIMP_TAC (srw_ss()) [] 670 THEN (WEAKEN_TAC is_eq) 671 THEN 672 (let val a = 673 ``(read_cpsr <|proc := 0|> >>= 674 (��cpsr'. 675 bad_mode <|proc := 0|> ^mode >>= 676 (��bad_mode. 677 if bad_mode then 678 errorT "write_spsr: unpredictable" 679 else 680 write__psr <|proc := 0|> ^spsr (cpsr with M := 16w))))`` 681 val () = global_mode := mode ; 682 val pthms = pthms @ [write__psr_und_thm,write__psr_svc_thm, 683 write__psr_abt_thm,write__psr_irq_thm, 684 write__psr_fiq_thm]; 685 val (thm,_) = prove a ``(assert_mode ^mode)`` 686 ``(assert_mode ^mode)`` 687 uargs pthms; 688 in 689 FULL_SIMP_TAC (srw_ss()) [thm] 690 end) 691 end 692 693val write_spsr_und_thm = 694 store_thm("write_spsr_und_thm", 695 ``preserve_relation_mmu (write_spsr <|proc := 0|> (cpsr with M := 16w)) 696 (assert_mode 27w) (assert_mode 27w) ^uf1 ^uy1 ``, 697 prove_write_spsr_thm ``27w:bool[5]`` ``SPSR_und ``); 698 699val write_spsr_svc_thm = 700 store_thm("write_spsr_svc_thm", 701 ``preserve_relation_mmu (write_spsr <|proc := 0|> (cpsr with M := 16w)) 702 (assert_mode 19w) (assert_mode 19w) ^uf1 ^uy1 ``, 703 prove_write_spsr_thm ``19w:bool[5]`` ``SPSR_svc ``); 704 705val write_spsr_abt_thm = 706 store_thm("write_spsr_abt_thm", 707 ``preserve_relation_mmu (write_spsr <|proc := 0|> (cpsr with M := 16w)) 708 (assert_mode 23w) (assert_mode 23w) ^uf1 ^uy1 ``, 709 prove_write_spsr_thm ``23w:bool[5]`` ``SPSR_abt ``); 710 711val write_spsr_irq_thm = 712 store_thm("write_spsr_irq_thm", 713 ``preserve_relation_mmu (write_spsr <|proc := 0|> (cpsr with M := 16w)) 714 (assert_mode 18w) (assert_mode 18w) ^uf1 ^uy1 ``, 715 prove_write_spsr_thm ``18w:bool[5]`` ``SPSR_irq ``); 716 717val write_spsr_fiq_thm = 718 store_thm("write_spsr_fiq_thm", 719 ``preserve_relation_mmu (write_spsr <|proc := 0|> (cpsr with M := 16w)) 720 (assert_mode 17w) (assert_mode 17w) ^uf1 ^uy1 ``, 721 prove_write_spsr_thm ``17w:bool[5]`` ``SPSR_fiq ``); 722 723val prove_write__reg_thm = 724fn mode => fn reg => fn reg_set => 725 let 726 val trm1 = ``(s1 with registers updated_by ((0,^reg) =+ value))`` 727 val trm2 = ``(s2 with registers updated_by ((0,^reg) =+ value))`` 728 in 729 RW_TAC (srw_ss()) [preserve_relation_mmu_def, 730 write__reg_def,writeT_def, 731 similar_def,untouched_def, 732 seqT_def,errorT_def,tautology_fun_def, 733 priv_mode_similar_def, 734 assert_mode_def,have_same_mem_accesses_def] 735 THEN RW_TAC (srw_ss()) [] 736 THEN FULL_SIMP_TAC (let_ss) [] 737 THEN FIRST_PROVE [ 738 Q.UNABBREV_TAC ([QUOTE reg_set]) 739 THEN FULL_SIMP_TAC (srw_ss()) [] 740 THEN UNDISCH_TAC ``reg ��� ^reg`` 741 THEN EVAL_TAC 742 THEN FULL_SIMP_TAC (srw_ss()) [], 743 744 UNDISCH_TAC ``ARM_MODE s1 = ^mode`` THEN 745 UNDISCH_TAC ``ARM_MODE s2 = ^mode`` 746 THEN EVAL_TAC 747 THEN RW_TAC (srw_ss()) [], 748 749 UNDISCH_TAC ``equal_user_register s1 s2`` 750 THEN EVAL_TAC 751 THEN RW_TAC (srw_ss()) [] 752 THEN METIS_TAC [], 753 ASSUME_TAC (SPECL [``s1:arm_state``, 754 trm1, ``g:bool[32]``] 755 trivially_untouched_av_lem2) 756 THEN ASSUME_TAC ( 757 SPECL [``s2:arm_state``, 758 trm2, ``g:bool[32]``] 759 trivially_untouched_av_lem2) 760 THEN RES_TAC 761 THEN FULL_SIMP_TAC (srw_ss()) [] 762 ] 763 end; 764 765 766val write__reg_und_thm = 767 store_thm("write__reg_und_thm", 768 ``(preserve_relation_mmu 769 (write__reg <|proc := 0|> RName_LRund value) 770 (assert_mode 27w) (assert_mode 27w) ^uf1 ^uy1)``, 771 prove_write__reg_thm ``27w:bool[5]`` ``RName_LRund`` "und_regs" 772 ); 773 774val write__reg_abt_thm = 775 store_thm("write__reg_abt_thm", 776 ``(preserve_relation_mmu 777 (write__reg <|proc := 0|> RName_LRabt value) 778 (assert_mode 23w) (assert_mode 23w) ^uf1 ^uy1)``, 779 prove_write__reg_thm ``23w:bool[5]`` ``RName_LRabt`` "abort_regs" 780 ); 781 782val write__reg_irq_thm = 783 store_thm("write__reg_irq_thm", 784 ``(preserve_relation_mmu 785 (write__reg <|proc := 0|> RName_LRirq value) 786 (assert_mode 18w) (assert_mode 18w) ^uf1 ^uy1)``, 787 prove_write__reg_thm ``18w:bool[5]`` ``RName_LRirq`` "irq_regs" 788 ); 789 790val write__reg_fiq_thm = 791 store_thm("write__reg_fiq_thm", 792 ``(preserve_relation_mmu 793 (write__reg <|proc := 0|> RName_LRfiq value) 794 (assert_mode 17w) (assert_mode 17w) ^uf1 ^uy1)``, 795 prove_write__reg_thm ``17w:bool[5]`` ``RName_LRfiq`` "fiq_regs" 796 ); 797 798val write__reg_svc_thm = 799 store_thm("write__reg_svc_thm", 800 ``(preserve_relation_mmu 801 (write__reg <|proc := 0|> RName_LRsvc value) 802 (assert_mode 19w) (assert_mode 19w) ^uf1 ^uy1)``, 803 prove_write__reg_thm ``19w:bool[5]`` ``RName_LRsvc`` "svc_regs" 804 ); 805 806val write__pc_und_thm = 807 store_thm("write__pc_und_thm", 808 ``(preserve_relation_mmu 809 (write__reg <|proc := 0|> RName_PC value) 810 (assert_mode 27w) (assert_mode 27w) ^uf1 ^uy1)``, 811 prove_write__reg_thm ``27w:bool[5]`` ``RName_PC:RName`` "user_regs" 812 ); 813val write__pc_abt_thm = 814 store_thm("write__pc_abt_thm", 815 ``(preserve_relation_mmu 816 (write__reg <|proc := 0|> RName_PC value) 817 (assert_mode 23w) (assert_mode 23w) ^uf1 ^uy1)``, 818 prove_write__reg_thm ``23w:bool[5]`` ``RName_PC:RName`` "user_regs" 819 ); 820val write__pc_irq_thm = 821 store_thm("write__pc_irq_thm", 822 ``(preserve_relation_mmu 823 (write__reg <|proc := 0|> RName_PC value) 824 (assert_mode 18w) (assert_mode 18w) ^uf1 ^uy1)``, 825 prove_write__reg_thm ``18w:bool[5]`` ``RName_PC:RName`` "user_regs" 826 ); 827val write__pc_svc_thm = 828 store_thm("write__pc_svc_thm", 829 ``(preserve_relation_mmu 830 (write__reg <|proc := 0|> RName_PC value) 831 (assert_mode 19w) (assert_mode 19w) ^uf1 ^uy1)``, 832 prove_write__reg_thm ``19w:bool[5]`` ``RName_PC:RName`` "user_regs" 833 ); 834val write__pc_fiq_thm = 835 store_thm("write__pc_fiq_thm", 836 ``(preserve_relation_mmu 837 (write__reg <|proc := 0|> RName_PC value) 838 (assert_mode 17w) (assert_mode 17w) ^uf1 ^uy1)``, 839 prove_write__reg_thm ``17w:bool[5]`` ``RName_PC:RName`` "user_regs" 840 ); 841 842val prove_write_link_reg_thm = 843 fn mode => fn lr => 844 `LookUpRName <|proc := 0|> (14w,^mode) >>= 845 (��rname. write__reg <|proc := 0|> rname value) = 846 LookUpRName <|proc := 0|> (14w,^mode) >>= 847 (��rname. write__reg <|proc := 0|> ^lr value)` 848 by (RW_TAC (srw_ss()) [LookUpRName_def,write__reg_def, 849 writeT_def,RBankSelect_def,bad_mode_def, 850 constT_def,seqT_def] THEN ABS_TAC 851 THEN RW_TAC (srw_ss()) []) 852 THEN RW_TAC (srw_ss()) [write_reg_def, 853 write_reg_mode_def] 854 (* THEN FULL_SIMP_TAC (srw_ss()) [] *) 855 THEN 856 let val l = ``(��cpsr. 857 (is_secure <|proc := 0|> ||| read_nsacr <|proc := 0|> 858 ||| current_instr_set <|proc := 0|>) >>= 859 (��(is_secure,nsacr,current_instr_set). 860 if 861 ��is_secure ��� ((cpsr.M = 22w) ��� (cpsr.M = 17w) ��� nsacr.RFR) 862 then 863 errorT "write_reg_mode: unpredictable" 864 else 865 LookUpRName <|proc := 0|> (14w,cpsr.M) >>= 866 (��rname. write__reg <|proc := 0|> rname value)))`` 867 val a = ``(read_cpsr <|proc := 0|> >>= 868 (��cpsr. 869 (is_secure <|proc := 0|> ||| read_nsacr <|proc := 0|> 870 ||| current_instr_set <|proc := 0|>) >>= 871 (��(is_secure,nsacr,current_instr_set). 872 LookUpRName <|proc := 0|> (14w,^mode) >>= 873 (��rname. write__reg <|proc := 0|> ^lr value))))`` 874 in 875 ASSUME_TAC (SIMP_RULE (bool_ss) [] 876 (SPECL [l, ``(assert_mode ^mode)``, 877 uf1,uy1,mode] 878 (INST_TYPE [alpha |-> ``:unit``] 879 switching_lemma_helperTheory.cpsr_simp_rel_lem))) 880 THEN FULL_SIMP_TAC (srw_ss()) [] 881 THEN REPEAT (WEAKEN_TAC is_eq) 882 THEN 883 (let 884 val pthms = pthms @ 885 [write__reg_und_thm, 886 write__reg_irq_thm, 887 write__reg_fiq_thm, 888 write__reg_svc_thm, 889 write__reg_abt_thm]; 890 val () = global_mode := mode; 891 val (thm,_) = prove a ``(assert_mode ^mode)`` 892 ``(assert_mode ^mode)`` 893 uargs pthms; 894 in 895 FULL_SIMP_TAC (srw_ss()) [thm] 896 end) 897 end; 898 899val write_reg_und_thm = 900 store_thm("write_reg_und_thm", 901 ``preserve_relation_mmu 902 (write_reg <|proc := 0|> 14w value) 903 (assert_mode 27w) (assert_mode 27w) ^uf1 ^uy1``, 904 prove_write_link_reg_thm ``27w:bool[5]`` ``RName_LRund`` 905 ); 906 907val write_reg_svc_thm = 908 store_thm("write_reg_svc_thm", 909 ``preserve_relation_mmu 910 (write_reg <|proc := 0|> 14w value) 911 (assert_mode 19w) (assert_mode 19w) ^uf1 ^uy1``, 912 prove_write_link_reg_thm ``19w:bool[5]`` ``RName_LRsvc`` 913 ); 914 915val write_reg_abt_thm = 916 store_thm("write_reg_abt_thm", 917 ``preserve_relation_mmu 918 (write_reg <|proc := 0|> 14w value) 919 (assert_mode 23w) (assert_mode 23w) ^uf1 ^uy1``, 920 prove_write_link_reg_thm ``23w:bool[5]`` ``RName_LRabt`` 921 ); 922 923val write_reg_irq_thm = 924 store_thm("write_reg_irq_thm", 925 ``preserve_relation_mmu 926 (write_reg <|proc := 0|> 14w value) 927 (assert_mode 18w) (assert_mode 18w) ^uf1 ^uy1``, 928 prove_write_link_reg_thm ``18w:bool[5]`` ``RName_LRirq`` 929 ); 930 931(* the body of write is different from the rest *) 932 933(* val write_reg_fiq_thm = *) 934(* store_thm("write_reg_fiq_thm", *) 935(* ``preserve_relation_mmu *) 936(* (write_reg <|proc := 0|> 14w value) *) 937(* (assert_mode 17w) (assert_mode 17w) ^uf1 ^uy1``, *) 938(* prove_write_link_reg_thm ``17w:bool[5]`` ``RName_LRfiq`` *) 939(* ); *) 940 941(* ================================================+++++========================== *) 942(* proof of preserve relation of writing part 943 of take exception in no access violation case *) 944(* =====================================================+++++===================== *) 945 946val write_scr_cpsr_preconds_def = 947 Define `write_scr_cpsr_preconds g s1 s2 = 948 (~access_violation s1) 949 /\ (mmu_requirements s1 g) 950 /\ (mmu_requirements s2 g) 951 /\ (similar g s1 s2) 952 /\ (tautology_fun g s1 s2) 953 /\ (��access_violation s1) 954 /\ ((s1.psrs (0,CPSR)).M = 16w) 955 /\ (��access_violation s2) 956 /\ ((s2.psrs (0,CPSR)).M = 16w )`; 957 958 959val TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC = 960fn mode => 961 let 962 val comp2 = ``(condT F (write_scr <|proc := 0|> (scr with NS := F)) 963 ||| write_cpsr <|proc := 0|> 964 (s2.psrs (0,CPSR) with M := ^mode))``; 965 in 966 RW_TAC (srw_ss()) [] 967 THEN ASSUME_TAC (SIMP_RULE (srw_ss()) 968 [assert_mode_def,ARM_MODE_def, 969 ARM_READ_CPSR_def,condT_def] 970 (SPECL [``g:bool[32]``,``s1:arm_state``, 971 ``s2:arm_state``, comp2, 972 ``scr:CP15scr``,mode] write_scr_cpsr_thm)) 973 THEN RES_TAC 974 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def,write_scr_cpsr_preconds_def] 975 THEN RW_TAC (srw_ss()) [] 976 THEN FULL_SIMP_TAC (srw_ss()) [] 977 end; 978 979val TAKE_EXCEPTION_MODE_CHANGING_VALUESTATE_TAC = 980 fn (si ,si' , a , b, mode) => 981 let 982 val l2 = ``(constT () 983 ||| write_cpsr <|proc := 0|> 984 (s2.psrs (0,CPSR) with M := ^mode))`` 985 val comp2 = ``(condT F (write_scr <|proc := 0|> (scr with NS := F)) 986 ||| write_cpsr <|proc := 0|> 987 (s2.psrs (0,CPSR) with M := ^mode))``; 988 in 989 ASSUME_TAC (REWRITE_RULE 990 [assert_mode_def,ARM_MODE_def, 991 ARM_READ_CPSR_def,condT_def] 992 (SPECL [``g:bool[32]``,``s1:arm_state``, 993 ``s2:arm_state``, comp2, 994 ``scr:CP15scr``,mode] write_scr_cpsr_thm)) 995 THEN RES_TAC 996 THEN REPEAT (WEAKEN_TAC is_imp) 997 THEN PAT_X_ASSUM ``X c s1= ValueState a b`` 998 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 999 THEN PAT_X_ASSUM ``X c' s2= ValueState a' b'`` 1000 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 1001 THEN PAT_X_ASSUM ``X c s1= ValueState a b`` 1002 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 1003 THEN FULL_SIMP_TAC (srw_ss()) [] 1004 THEN IMP_RES_TAC untouched_mmu_setup_lem 1005 THEN PAT_X_ASSUM ``���c g s1 s2. X `` 1006 (fn thm => ASSUME_TAC 1007 (SPECL [``a:unit#unit``,``g:bool[32]``, 1008 ``s1':arm_state``, 1009 ``s2':arm_state``] thm)) 1010 THEN RES_TAC 1011 THEN IMP_RES_TAC 1012 (SPECL [l2, ``H2:unit#unit->unit M``, si, a, 1013 b, ``a'':unit#unit``, 1014 si', ``e:string``] 1015 (INST_TYPE [alpha |-> ``:unit#unit``, 1016 beta |-> ``:unit``] hlp_seqT2_thm)) 1017 THEN IMP_RES_TAC (SIMP_RULE (srw_ss()) 1018 [ARM_MODE_def,ARM_READ_CPSR_def] 1019 untouched_trans) 1020 THEN FULL_SIMP_TAC (srw_ss()) [] 1021 THEN RW_TAC (srw_ss()) [] 1022 end; 1023 1024val take_exp_mode_changing_ut_thm = 1025 store_thm ("take_exp_mode_changing_ut_thm", 1026 ``! H2 s1 s2 g u. 1027 let f2 = (((if (s2.psrs (0,CPSR)).M = 22w then 1028 write_scr <|proc := 0|> (s2.coprocessors.state.cp15.SCR with NS := F) 1029 else 1030 constT ()) ||| write_cpsr <|proc := 0|> 1031 (s2.psrs (0,CPSR) with M := u)) >>= (H2:unit#unit->unit M)) 1032 in 1033 (write_scr_cpsr_preconds g s1 s2) 1034 ==> 1035 (preserve_relation_mmu_abs H2 (assert_mode u) (assert_mode u) 1036 have_same_mem_accesses tautology_fun) ==> 1037 ((? a b a' b'. (f2 s1 = ValueState a b) /\ (f2 s2 = ValueState a' b') 1038 /\ (untouched g s1 b ��� untouched g s2 b' ��� 1039 tautology_fun g b b')) 1040 \/ 1041 (?e. (f2 s1 =Error e) /\ (f2 s2 = Error e))) 1042 ``, 1043 FULL_SIMP_TAC (let_ss) [preserve_relation_mmu_abs_def, 1044 condT_def,tautology_fun_def, 1045 assert_mode_def,ARM_MODE_def, 1046 ARM_READ_CPSR_def,write_scr_cpsr_preconds_def] 1047 THEN RW_TAC (srw_ss()) [] 1048 THEN Cases_on 1049 `(constT () 1050 ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s1` 1051 THEN Cases_on 1052 `(constT () 1053 ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s2` 1054 THEN FIRST_PROVE 1055 [ TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]`` , 1056 RW_TAC (srw_ss()) [seqT_def] 1057 THEN FIRST_PROVE 1058 [ 1059 TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]``, 1060 TAKE_EXCEPTION_MODE_CHANGING_VALUESTATE_TAC ( 1061 ``s1:arm_state`` ,``s1':arm_state``, 1062 ``a:unit`` , ``b:arm_state``,``u:bool[5]``)] 1063 ] 1064 ); 1065 1066 1067val take_exp_mode_changing_same_access_thm = 1068 store_thm ("take_exp_mode_changing_same_access_thm", 1069 ``! H2 s1 s2 g u . 1070 let f2 = (((if (s2.psrs (0,CPSR)).M = 22w then 1071 write_scr <|proc := 0|> 1072 (s2.coprocessors.state.cp15.SCR with NS := F) 1073 else 1074 constT ()) ||| write_cpsr <|proc := 0|> 1075 (s2.psrs (0,CPSR) with M := u)) >>= (H2:unit#unit->unit M)) 1076 in 1077 (write_scr_cpsr_preconds g s1 s2) 1078 ==> 1079 (preserve_relation_mmu_abs H2 (assert_mode u) (assert_mode u) 1080 have_same_mem_accesses tautology_fun) ==> 1081 ((? a b a' b'. (f2 s1 = ValueState a b) /\ (f2 s2 = ValueState a' b') 1082 /\ (have_same_mem_accesses g s1 b ��� have_same_mem_accesses g s2 b')) 1083 \/ 1084 (?e. (f2 s1 = Error e) /\ (f2 s2 = Error e) )) 1085 ``, 1086 FULL_SIMP_TAC (let_ss) [preserve_relation_mmu_abs_def, 1087 condT_def,tautology_fun_def, 1088 assert_mode_def,ARM_MODE_def, 1089 ARM_READ_CPSR_def,write_scr_cpsr_preconds_def] 1090 THEN RW_TAC (srw_ss()) [] 1091 THEN Cases_on `(constT () ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s1` 1092 THEN Cases_on `(constT () ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s2` 1093 (*THEN FULL_SIMP_TAC (srw_ss()) []*) 1094 THEN FIRST_PROVE 1095 [ TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]``, 1096 RW_TAC (srw_ss()) [seqT_def] 1097 THEN FIRST_PROVE 1098 [ 1099 TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]``, 1100 TAKE_EXCEPTION_MODE_CHANGING_VALUESTATE_TAC 1101 ( 1102 ``s1:arm_state`` ,``s1':arm_state``, 1103 ``a:unit`` , ``b:arm_state``,``u:bool[5]``) 1104 THEN IMP_RES_TAC (SIMP_RULE (srw_ss()) 1105 [trans_fun_def] 1106 trans_have_same_mem_accesses_thm) 1107 THEN FULL_SIMP_TAC (srw_ss()) [] 1108 ]] 1109 ); 1110 1111 1112val take_exp_mode_changing_misc_thm = 1113 store_thm ("take_exp_mode_changing_misc_thm", 1114 ``! H2 s1 s2 g u. 1115 let f2 = (((if (s2.psrs (0,CPSR)).M = 22w then 1116 write_scr <|proc := 0|> 1117 (s2.coprocessors.state.cp15.SCR with NS := F) 1118 else 1119 constT ()) ||| write_cpsr <|proc := 0|> 1120 (s2.psrs (0,CPSR) with M := u)) >>= (H2:unit#unit->unit M)) 1121 in 1122 (preserve_relation_mmu_abs H2 (assert_mode u) (assert_mode u) 1123 have_same_mem_accesses tautology_fun) 1124 ==> 1125 (write_scr_cpsr_preconds g s1 s2) 1126 ==> 1127 ((? a a' b b'. (f2 s1 = ValueState a b) /\ (f2 s2 = ValueState a' b') 1128 /\ ((a' = a) ��� ((b.psrs (0,CPSR)).M = u) ��� 1129 ((b'.psrs (0,CPSR)).M = u) ��� similar g b b')) 1130 \/ 1131 (?e. (f2 s1 = Error e) /\ (f2 s2 = Error e) ))``, 1132 FULL_SIMP_TAC (let_ss) [preserve_relation_mmu_abs_def, 1133 condT_def,tautology_fun_def, 1134 assert_mode_def,ARM_MODE_def, 1135 ARM_READ_CPSR_def,write_scr_cpsr_preconds_def] 1136 THEN RW_TAC (srw_ss()) [] 1137 THEN Cases_on `(constT () ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s1` 1138 THEN Cases_on `(constT () ||| write_cpsr <|proc := 0|> (s2.psrs (0,CPSR) with M := u)) s2` 1139 (*THEN FULL_SIMP_TAC (srw_ss()) []*) 1140 THEN FIRST_PROVE 1141 [ TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]``, 1142 RW_TAC (srw_ss()) [seqT_def] 1143 THEN FIRST_PROVE 1144 [ 1145 TAKE_EXCEPTION_MODE_CHANGING_ERROR_TAC ``u:bool[5]``, 1146 TAKE_EXCEPTION_MODE_CHANGING_VALUESTATE_TAC 1147 ( 1148 ``s1:arm_state`` ,``s1':arm_state``, 1149 ``a:unit`` , ``b:arm_state``,``u:bool[5]``) 1150 THEN FULL_SIMP_TAC (srw_ss()) [] ]] ); 1151 1152val take_exp_mode_changing_thm = 1153 store_thm ("take_exp_mode_changing_thm", 1154 ``! H s1 s2 (* a a' b b' *) g u . 1155 let f = (((if (s2.psrs (0,CPSR)).M = 22w then 1156 write_scr <|proc := 0|> 1157 (s2.coprocessors.state.cp15.SCR with NS := F) 1158 else 1159 constT ()) ||| write_cpsr <|proc := 0|> 1160 (s2.psrs (0,CPSR) with M := u)) >>= (H:unit#unit->unit M)) 1161 in 1162 (write_scr_cpsr_preconds g s1 s2) 1163 ==> 1164 (preserve_relation_mmu_abs H (assert_mode u) (assert_mode u) 1165 have_same_mem_accesses tautology_fun) ==> 1166 ((? a b a' b'. (f s1 = ValueState a b) /\ (f s2 = ValueState a' b') 1167 /\((a' = a) ��� ((b.psrs (0,CPSR)).M = u) ��� 1168 ((b'.psrs (0,CPSR)).M = u) ��� similar g b b' /\ 1169 (have_same_mem_accesses g s1 b ��� have_same_mem_accesses g s2 b')/\ 1170 (untouched g s1 b ��� untouched g s2 b' /\ tautology_fun g b b'))) 1171 \/ 1172 (? e. (f s1=Error e) /\ (f s2 = Error e))) 1173 ``, 1174 let 1175 val vars = [``H:unit#unit->unit M``, ``s1:arm_state``, 1176 ``s2:arm_state``,``g:bool[32]``,``u:bool[5]``]; 1177 val comp2 = ``(condT F (write_scr <|proc := 0|> (scr with NS := F)) 1178 ||| write_cpsr <|proc := 0|> 1179 (s2.psrs (0,CPSR) with M := u))``; 1180 in 1181 FULL_SIMP_TAC (let_ss) [] 1182 THEN RW_TAC (srw_ss()) [] 1183 THEN MP_TAC (SPECL vars take_exp_mode_changing_ut_thm) 1184 THEN MP_TAC (SPECL vars take_exp_mode_changing_same_access_thm) 1185 THEN MP_TAC (SPECL vars take_exp_mode_changing_misc_thm) 1186 THEN FULL_SIMP_TAC (let_ss) [] 1187 THEN UNDISCH_ALL_TAC 1188 THEN RW_TAC (srw_ss()) [] 1189 THEN FULL_SIMP_TAC (srw_ss()) [] 1190 THEN RW_TAC (srw_ss()) [] 1191 end 1192 ); 1193 1194(****SHOULD BE REPLACED *************) 1195 1196(* val H'= ``(��(u1:unit,u2:unit).(write_spsr <|proc := 0|> (s2.psrs (0,CPSR) with M := 16w) *) 1197(* ||| write_reg <|proc := 0|> 14w *) 1198(* (if (s2.psrs (0,CPSR) with M := 16w).T then *) 1199(* get_pc_value s2 ��� 2w *) 1200(* else *) 1201(* get_pc_value s2 ��� 4w) *) 1202(* ||| read_cpsr <|proc := 0|> >>= *) 1203(* (��cpsr. *) 1204(* write_cpsr <|proc := 0|> *) 1205(* (cpsr with *) 1206(* <|I := T; IT := 0w; J := F; *) 1207(* T := s2.coprocessors.state.cp15.SCTLR.TE; *) 1208(* E := s2.coprocessors.state.cp15.SCTLR.EE|>)) *) 1209(* ||| branch_to <|proc := 0|> *) 1210(* (get_base_vector_table s2 + 4w)) *) 1211(* >>= *) 1212(* (��(u1,u2,u3,u4). constT ()))``; *) 1213 1214 1215fun prove_take_exception_nav_thm 1216 te_body te_def mode 1217 fixed_rp_thm const_comp_rp_thm 1218 read_part_thm write_part_thm wp_specl simpr 1219 = 1220 let val (lp,rp,_)= decompose_term te_body; 1221 val al_type = get_monad_type (type_of (lp)); 1222 in 1223 RW_TAC (bool_ss) [te_def, 1224 preserve_relation_mmu_def, 1225 assert_mode_no_access_violation_def] 1226 THEN Cases_on [QUOTE ("("^(term_to_string lp) ^ ") s1")] 1227 THEN Cases_on [QUOTE ("("^(term_to_string lp) ^ ") s2")] 1228 THEN FIRST_PROVE 1229 [ 1230 ASSUME_SPECL_SIMP_TAC 1231 [``g:bool[32]``, 1232 ``s1:arm_state``, 1233 ``s2:arm_state``] 1234 [preserve_relation_mmu_def,assert_mode_def, 1235 ARM_MODE_def,ARM_READ_CPSR_def] read_part_thm 1236 THEN RES_TAC 1237 THEN IMP_RES_SPEC_TAC rp 1238 (INST_TYPE [alpha |-> al_type, 1239 beta|-> ``:unit``] 1240 hlp_seqT3_thm) 1241 THEN FULL_SIMP_TAC (srw_ss()) [] 1242 THEN RW_TAC (srw_ss()) [] 1243 , 1244 Cases_on [QUOTE ("("^(term_to_string te_body) ^ ") s1")] 1245 THEN Cases_on [QUOTE ("("^(term_to_string te_body) ^ ") s2")] 1246 THEN IMP_RES_SPECL_TAC [``s:arm_state``, rp] 1247 fixed_rp_thm 1248 THEN FULL_SIMP_TAC (srw_ss()) [] 1249 THEN ASSUME_TAC const_comp_rp_thm 1250 THEN IMP_RES_SPECL_TAC [lp] (INST_TYPE [alpha |-> al_type, 1251 beta |-> ``:unit``] 1252 const_comp_hlp_thm) 1253 THEN FULL_SIMP_TAC (srw_ss()) [condT_def] 1254 THEN (VALID (NTAC 2 (WEAKEN_TAC is_forall))) 1255 THEN (VALID (PAT_X_ASSUM ``g a s = g' a s`` 1256 (fn thm => THROW_AWAY_TAC (concl thm)))) 1257 (*reduced to the right part *) 1258 THEN EVERY_ASSUM (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 1259 THEN IMP_RES_TAC similar_states_have_same_vec_tab_thm 1260 THEN IMP_RES_TAC similar_states_have_same_read_pc_thm 1261 THEN IMP_RES_TAC similar_states_have_same_security_ext_thm 1262 THEN PAT_X_ASSUM ``similar g s1 s2`` 1263 (fn thm => FULL_SIMP_TAC (srw_ss()) 1264 [REWRITE_RULE [similar_def, 1265 equal_user_register_def 1266 ] 1267 thm] 1268 THEN ASSUME_TAC thm ) 1269 THEN FULL_SIMP_TAC (srw_ss()) [] 1270 (* verything is based on s2 state and without lambda abs*) 1271 THEN ASSUME_SPECL_TAC wp_specl 1272 (GEN_ALL write_part_thm) 1273 THEN ASSUME_SPECL_SIMP_TAC 1274 [simpr,``s1:arm_state``,``s2:arm_state``, ``g:bool[32]``,mode] 1275 [write_scr_cpsr_preconds_def] 1276 (SIMP_RULE (let_ss) [] 1277 take_exp_mode_changing_thm) 1278 THEN FULL_SIMP_TAC (let_ss) [assert_mode_def,ARM_MODE_def, 1279 ARM_READ_CPSR_def] 1280 THEN IMP_RES_TAC similar_states_have_same_av_thm1 1281 THEN IMP_RES_TAC similar_states_have_same_mode_thm 1282 1283 THEN UNDISCH_ALL_TAC 1284 THEN FULL_SIMP_TAC (srw_ss()) [] 1285 THEN RW_TAC (srw_ss()) [] 1286 THEN METIS_TAC [hlp_seqT3_thm] 1287 ] 1288 end; 1289 1290 1291val get_take_abt_irq_simp_pars = 1292 fn x => ( 1293 ``��(u1:unit,u2:unit). 1294 (write_spsr <|proc := 0|> (cpsr with M := 16w) 1295 ||| write_reg <|proc := 0|> 14w 1296 (if (cpsr with M := 16w).T then pc else pc ��� 4w) 1297 ||| read_cpsr <|proc := 0|> >>= 1298 (��cpsr. 1299 write_cpsr <|proc := 0|> 1300 (cpsr with 1301 <|I := T; 1302 A := 1303 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 1304 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 1305 E := sctlr.EE|>)) 1306 ||| branch_to <|proc := 0|> (ExcVectorBase + ^x)) >>= 1307 (��(u1,u2,u3,u4). constT ())`` 1308 , 1309``(��(u1:unit,u2:unit). 1310 (write_spsr <|proc := 0|> (s2.psrs (0,CPSR) with M := 16w) 1311 ||| write_reg <|proc := 0|> 14w 1312 (if (s2.psrs (0,CPSR) with M := 16w).T then 1313 get_pc_value s2 1314 else 1315 get_pc_value s2 ��� 4w) 1316 ||| read_cpsr <|proc := 0|> >>= 1317 (��cpsr. 1318 write_cpsr <|proc := 0|> 1319 (cpsr with 1320 <|I := T; 1321 A := 1322 ((��get_security_ext s2 ��� 1323 ��s2.coprocessors.state.cp15.SCR.NS ��� 1324 s2.coprocessors.state.cp15.SCR.AW) ��� 1325 cpsr.A); IT := 0w; J := F; 1326 T := s2.coprocessors.state.cp15.SCTLR.TE; 1327 E := s2.coprocessors.state.cp15.SCTLR.EE|>)) 1328 ||| branch_to <|proc := 0|> 1329 (get_base_vector_table s2 + ^x)) >>= 1330 (��(u1,u2,u3,u4). constT ()))``); 1331 1332val get_take_undef_svc_simp_pars = 1333 fn x => ( ``��(u1:unit,u2:unit). 1334 (write_spsr <|proc := 0|> (cpsr with M := 16w) 1335 ||| write_reg <|proc := 0|> 14w 1336 (if (cpsr with M := 16w).T then pc ��� 2w else pc ��� 4w) 1337 ||| read_cpsr <|proc := 0|> >>= 1338 (��cpsr. 1339 write_cpsr <|proc := 0|> 1340 (cpsr with 1341 <|I := T; IT := 0w; J := F; T := sctlr.TE; 1342 E := sctlr.EE|>)) 1343 ||| branch_to <|proc := 0|> (ExcVectorBase + ^x)) >>= 1344 (��(u1,u2,u3,u4). constT ())``, 1345 ``(��(u1:unit,u2:unit). 1346 (write_spsr <|proc := 0|> (s2.psrs (0,CPSR) with M := 16w) 1347 ||| write_reg <|proc := 0|> 14w 1348 (if (s2.psrs (0,CPSR) with M := 16w).T then 1349 get_pc_value s2 -2w 1350 else 1351 get_pc_value s2 ��� 4w) 1352 ||| read_cpsr <|proc := 0|> >>= 1353 (��cpsr. 1354 write_cpsr <|proc := 0|> 1355 (cpsr with 1356 <|I := T; 1357 IT := 0w; J := F; 1358 T := s2.coprocessors.state.cp15.SCTLR.TE; 1359 E := s2.coprocessors.state.cp15.SCTLR.EE|>)) 1360 ||| branch_to <|proc := 0|> 1361 (get_base_vector_table s2 + ^x)) >>= 1362 (��(u1,u2,u3,u4). constT ()))``); 1363 1364 1365val take_data_abort_exception_nav_thm = 1366 store_thm ("take_data_abort_exception_nav_thm", 1367 ``preserve_relation_mmu 1368 (take_data_abort_exception <|proc := 0|> ) 1369 (assert_mode_no_access_violation 16w ) 1370 (assert_mode 23w) ^uf1 ^uy1``, 1371 let 1372 val (_,te_body) = 1373 (dest_eq o concl) (REWRITE_CONV [take_data_abort_exception_def] 1374 ``take_data_abort_exception <|proc:=0|> ``); 1375 val (lp,rp,_)= decompose_term te_body; 1376 (*proof of reading part *) 1377 val () = global_mode := ``16w:bool[5]``; 1378 val (read_part_thm,_) = 1379 prove lp ``(assert_mode 16w)`` ``(assert_mode 16w)`` uargs pthms; 1380 val (writing_part , simpr) = get_take_abt_irq_simp_pars 1381 ``16w:bool[32]`` 1382 1383 val () = global_mode := ``23w:bool[5]``; 1384 val pthms = [trans_have_same_mem_accesses_thm, 1385 reflex_have_same_mem_accesses_thm, 1386 tautology_fun_def, 1387 have_same_mem_accesses_def, 1388 errorT_thm, 1389 SIMP_RULE (srw_ss()) [] 1390 (SPEC ``23w:bool[5]`` read_write_cpsr_abt_irq_thm), 1391 write_spsr_abt_thm, 1392 write_reg_abt_thm, 1393 write__pc_abt_thm 1394 ]; 1395 val (write_part_thm,_) = prove writing_part 1396 ``(assert_mode 23w)`` ``(assert_mode 23w)`` 1397 uargs pthms; 1398 val wp_specl = [``(s2.coprocessors.state.cp15.SCTLR):CP15sctlr``, 1399 ``s2.coprocessors.state.cp15.SCR:CP15scr``, 1400 ``get_pc_value s2``, 1401 ``get_security_ext s2``, 1402 ``(s2.psrs (0,CPSR)):ARMpsr``, 1403 ``get_base_vector_table s2``]; 1404 val fixed_rp_thm = fixed_abt_irq_exception_rp_thm3; 1405 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1406 1407 in 1408 prove_take_exception_nav_thm 1409 te_body take_data_abort_exception_def ``23w:bool[5]`` 1410 fixed_rp_thm const_comp_rp_thm 1411 read_part_thm write_part_thm wp_specl simpr 1412 end); 1413 1414 1415val take_prefetch_abort_exception_nav_thm = 1416 store_thm ("take_prefetch_exception_nav_thm", 1417 ``preserve_relation_mmu 1418 (take_prefetch_abort_exception <|proc := 0|> ) 1419 (assert_mode_no_access_violation 16w ) 1420 (assert_mode 23w) ^uf1 ^uy1``, 1421 let 1422 val (_,te_body) = 1423 (dest_eq o concl) (REWRITE_CONV [take_prefetch_abort_exception_def] 1424 ``take_prefetch_abort_exception <|proc:=0|> ``); 1425 val (lp,rp,_)= decompose_term te_body; 1426 (*proof of reading part *) 1427 val () = global_mode := ``16w:bool[5]``; 1428 val (read_part_thm,_) = 1429 prove lp ``(assert_mode 16w)`` ``(assert_mode 16w)`` uargs pthms; 1430 1431 val (writing_part , simpr) = get_take_abt_irq_simp_pars 1432 ``12w:bool[32]`` 1433 1434 val () = global_mode := ``23w:bool[5]``; 1435 val pthms = [trans_have_same_mem_accesses_thm, 1436 reflex_have_same_mem_accesses_thm, 1437 tautology_fun_def, 1438 have_same_mem_accesses_def, 1439 errorT_thm, 1440 SIMP_RULE (srw_ss()) [] 1441 (SPEC ``23w:bool[5]`` read_write_cpsr_abt_irq_thm), 1442 write_spsr_abt_thm, 1443 write_reg_abt_thm, 1444 write__pc_abt_thm 1445 ]; 1446 val (write_part_thm,_) = prove writing_part 1447 ``(assert_mode 23w)`` ``(assert_mode 23w)`` 1448 uargs pthms; 1449 val wp_specl = [``(s2.coprocessors.state.cp15.SCTLR):CP15sctlr``, 1450 ``s2.coprocessors.state.cp15.SCR:CP15scr``, 1451 ``get_pc_value s2``, 1452 ``get_security_ext s2``, 1453 ``(s2.psrs (0,CPSR)):ARMpsr``, 1454 ``get_base_vector_table s2``]; 1455 val fixed_rp_thm = fixed_abt_irq_exception_rp_thm3; 1456 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1457 1458 in 1459 prove_take_exception_nav_thm 1460 te_body take_prefetch_abort_exception_def ``23w:bool[5]`` 1461 fixed_rp_thm const_comp_rp_thm 1462 read_part_thm write_part_thm wp_specl simpr 1463 end); 1464 1465 1466val take_irq_exception_nav_thm = 1467 store_thm ("take_irq_exception_nav_thm", 1468 ``preserve_relation_mmu 1469 (take_irq_exception <|proc := 0|> ) 1470 (assert_mode_no_access_violation 16w ) 1471 (assert_mode 18w) ^uf1 ^uy1``, 1472 let 1473 val (_,te_body) = 1474 (dest_eq o concl) (REWRITE_CONV [take_irq_exception_def] 1475 ``take_irq_exception <|proc:=0|> ``); 1476 val (lp,rp,_)= decompose_term te_body; 1477 (*proof of reading part *) 1478 val () = global_mode := ``16w:bool[5]``; 1479 val (read_part_thm,_) = 1480 prove lp ``(assert_mode 16w)`` ``(assert_mode 16w)`` uargs pthms; 1481 1482 val (writing_part , simpr) = get_take_abt_irq_simp_pars 1483 ``24w:bool[32]`` ; 1484 1485 val () = global_mode := ``18w:bool[5]``; 1486 val pthms = [trans_have_same_mem_accesses_thm, 1487 reflex_have_same_mem_accesses_thm, 1488 tautology_fun_def, 1489 have_same_mem_accesses_def, 1490 errorT_thm, 1491 SIMP_RULE bool_ss [] 1492 (SPEC ``18w:bool[5]`` read_write_cpsr_abt_irq_thm), 1493 write_spsr_irq_thm, 1494 write_reg_irq_thm, 1495 write__pc_irq_thm 1496 ]; 1497 val (write_part_thm,_) = prove writing_part 1498 ``(assert_mode 18w)`` ``(assert_mode 18w)`` 1499 uargs pthms; 1500 val wp_specl = [``(s2.coprocessors.state.cp15.SCTLR):CP15sctlr``, 1501 ``s2.coprocessors.state.cp15.SCR:CP15scr``, 1502 ``get_pc_value s2``, 1503 ``get_security_ext s2``, 1504 ``(s2.psrs (0,CPSR)):ARMpsr``, 1505 ``get_base_vector_table s2``]; 1506 val fixed_rp_thm = fixed_abt_irq_exception_rp_thm3; 1507 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm; 1508 1509 in 1510 prove_take_exception_nav_thm 1511 te_body take_irq_exception_def ``18w:bool[5]`` 1512 fixed_rp_thm const_comp_rp_thm 1513 read_part_thm write_part_thm wp_specl simpr 1514 end); 1515 1516 1517val take_undef_instr_exception_nav_thm = 1518 store_thm ("take_undef_instr_exception_nav_thm", 1519 ``preserve_relation_mmu 1520 (take_undef_instr_exception <|proc := 0|> ) 1521 (assert_mode_no_access_violation 16w ) 1522 (assert_mode 27w) ^uf1 ^uy1``, 1523 let 1524 val (_,te_body) = 1525 (dest_eq o concl) (REWRITE_CONV [take_undef_instr_exception_def] 1526 ``take_undef_instr_exception <|proc:=0|> ``); 1527 val (lp,rp,_)= decompose_term te_body; 1528 (*proof of reading part *) 1529 val () = global_mode := ``16w:bool[5]``; 1530 val (read_part_thm,_) = 1531 prove lp ``(assert_mode 16w)`` ``(assert_mode 16w)`` uargs pthms; 1532 1533 (*proof of writing part *) 1534 val (writing_part , simpr) = get_take_undef_svc_simp_pars ``4w:bool[32]`` 1535 1536 val () = global_mode := ``27w:bool[5]``; 1537 val pthms = [trans_have_same_mem_accesses_thm, 1538 reflex_have_same_mem_accesses_thm, 1539 tautology_fun_def, 1540 have_same_mem_accesses_def, 1541 errorT_thm, 1542 SIMP_RULE (srw_ss()) [] 1543 (SPEC ``27w:bool[5]`` read_write_cpsr_undef_svc_thm), 1544 write_spsr_und_thm, 1545 write_reg_und_thm, 1546 write__pc_und_thm 1547 ]; 1548 val (write_part_thm,_) = prove writing_part 1549 ``(assert_mode 27w)`` ``(assert_mode 27w)`` 1550 uargs pthms; 1551 val wp_specl = [``(s2.coprocessors.state.cp15.SCTLR):CP15sctlr``, 1552 ``get_pc_value s2``, 1553 ``(s2.psrs (0,CPSR)):ARMpsr``, 1554 ``get_base_vector_table s2``]; 1555 val fixed_rp_thm = fixed_undef_svc_exception_rp_thm3 1556 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 1557 1558 in 1559 prove_take_exception_nav_thm 1560 te_body take_undef_instr_exception_def ``27w:bool[5]`` 1561 fixed_rp_thm const_comp_rp_thm 1562 read_part_thm write_part_thm wp_specl simpr 1563 end); 1564 1565 1566val take_svc_exception_nav_thm = 1567 store_thm ("take_svc_exception_nav_thm", 1568 let 1569 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1570 ``take_svc_exception <|proc:=0|> ``; 1571 val (_, a) = (dest_eq (concl athm)) 1572 val (_,_,rb)= decompose_term a; 1573 in 1574 ``preserve_relation_mmu 1575 ^rb 1576 (assert_mode_no_access_violation 16w ) 1577 (assert_mode 19w) ^uf1 ^uy1`` 1578 end 1579 , 1580 let 1581 val (_,a) = 1582 (dest_eq o concl) (REWRITE_CONV [take_svc_exception_def] 1583 ``take_svc_exception <|proc:=0|> ``); 1584 val (_,_,te_body)= decompose_term a 1585 val (lp,rp,_)= decompose_term te_body 1586 (*proof of reading part *) 1587 val () = global_mode := ``16w:bool[5]`` 1588 val (read_part_thm,_) = 1589 prove lp ``(assert_mode 16w)`` ``(assert_mode 16w)`` uargs pthms; 1590 1591 (*proof of writing part *) 1592 val (writing_part , simpr) = get_take_undef_svc_simp_pars ``8w:bool[32]`` 1593 val () = global_mode := ``19w:bool[5]``; 1594 val pthms = [trans_have_same_mem_accesses_thm, 1595 reflex_have_same_mem_accesses_thm, 1596 tautology_fun_def, 1597 have_same_mem_accesses_def, 1598 errorT_thm, 1599 SIMP_RULE (srw_ss()) [] 1600 (SPEC ``19w:bool[5]`` read_write_cpsr_undef_svc_thm), 1601 write_spsr_svc_thm, 1602 write_reg_svc_thm, 1603 write__pc_svc_thm 1604 ]; 1605 val (write_part_thm,_) = prove writing_part 1606 ``(assert_mode 19w)`` ``(assert_mode 19w)`` 1607 uargs pthms; 1608 val wp_specl = [``(s2.coprocessors.state.cp15.SCTLR):CP15sctlr``, 1609 ``get_pc_value s2``, 1610 ``(s2.psrs (0,CPSR)):ARMpsr``, 1611 ``get_base_vector_table s2``]; 1612 val fixed_rp_thm = fixed_undef_svc_exception_rp_thm3 1613 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm; 1614 1615 in 1616 prove_take_exception_nav_thm 1617 te_body take_svc_exception_def ``19w:bool[5]`` 1618 fixed_rp_thm const_comp_rp_thm 1619 read_part_thm write_part_thm wp_specl simpr 1620 end); 1621 1622 1623(**************************************) 1624(******** privilaged constranits ******) 1625 1626fun prove_take_exception_ut_EE_F_flags_thm mode thm te = 1627 1628 RW_TAC (srw_ss()) [] 1629 THEN ASSUME_TAC 1630 (LIST_MP [thm, 1631 refl_rel_tautology_fun_thm] 1632 (SPECL [te, 1633 ``(assert_mode_no_access_violation 16w) ``, 1634 ``(assert_mode ^mode)``, 1635 uf1, uy1] 1636 (INST_TYPE [alpha |-> ``:unit``] 1637 downgrade_thm ))) 1638 THEN FULL_SIMP_TAC (bool_ss) [keep_untouched_relation_def] 1639 THEN PAT_X_ASSUM ``���g s s' a.X`` 1640 (fn thm => 1641 ASSUME_SPECL_TAC [``g:bool[32]``, 1642 ``s1:arm_state``, 1643 ``s1':arm_state``, 1644 ``a:unit``] 1645 thm) 1646 THEN RES_TAC 1647 THEN FULL_SIMP_TAC (srw_ss()) [untouched_def]; 1648 1649val take_undef_instr_exception_ut_EE_F_flags_thm = 1650store_thm ("take_undef_instr_exception_ut_EE_F_flags_thm", 1651``! s1 a s1' g . 1652 mmu_requirements s1 g ��� 1653 assert_mode_no_access_violation 16w s1 ��� 1654 (take_undef_instr_exception <|proc := 0|> s1 = ValueState a s1') ==> 1655 (((s1'.psrs (0,CPSR)).F = (s1.psrs (0,CPSR)).F) /\ 1656 (s1'.coprocessors.state.cp15= 1657 s1.coprocessors.state.cp15) 1658 /\ (s1.information = s1'.information ) 1659 /\ ((s1.psrs (0,CPSR)).F = (s1'.psrs (0,CPSR)).F))`` 1660, 1661prove_take_exception_ut_EE_F_flags_thm ``27w:bool[5]`` 1662 take_undef_instr_exception_nav_thm 1663 ``take_undef_instr_exception <|proc:=0|>`` 1664); 1665 1666 1667val take_svc_exception_ut_EE_F_flags_thm = 1668store_thm ("take_svc_exception_ut_EE_F_flags_thm", 1669 let 1670 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1671 ``take_svc_exception <|proc:=0|> ``; 1672 val (_, a) = (dest_eq (concl athm)) 1673 val (_,_,rb)= decompose_term a; 1674 in 1675 ``! s1 a s1' g . 1676 mmu_requirements s1 g ��� 1677 assert_mode_no_access_violation 16w s1 ��� 1678 (^rb s1 = ValueState a s1') ==> 1679 (((s1'.psrs (0,CPSR)).F = (s1.psrs (0,CPSR)).F) /\ 1680 (s1'.coprocessors.state.cp15= 1681 s1.coprocessors.state.cp15) 1682 /\ (s1.information = s1'.information ) 1683 /\ ((s1.psrs (0,CPSR)).F = (s1'.psrs (0,CPSR)).F))`` 1684 end 1685, 1686let val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1687 ``take_svc_exception <|proc:=0|> ``; 1688 val (_, a) = (dest_eq (concl athm)) 1689 val (_,_,rb)= decompose_term a 1690in 1691 prove_take_exception_ut_EE_F_flags_thm ``19w:bool[5]`` 1692 take_svc_exception_nav_thm 1693 rb 1694end 1695 ); 1696 1697 1698 1699val take_data_abort_exception_ut_EE_F_flags_thm = 1700store_thm ("take_data_abort_exception_ut_EE_F_flags_thm", 1701``! s1 a s1' g . 1702 mmu_requirements s1 g ��� 1703 assert_mode_no_access_violation 16w s1 ��� 1704 (take_data_abort_exception <|proc := 0|> s1 = ValueState a s1') ==> 1705 (((s1'.psrs (0,CPSR)).F = (s1.psrs (0,CPSR)).F) /\ 1706 (s1'.coprocessors.state.cp15= 1707 s1.coprocessors.state.cp15) 1708 /\ (s1.information = s1'.information ) 1709 /\ ((s1.psrs (0,CPSR)).F = (s1'.psrs (0,CPSR)).F))`` 1710, 1711prove_take_exception_ut_EE_F_flags_thm ``23w:bool[5]`` 1712 take_data_abort_exception_nav_thm 1713 ``take_data_abort_exception <|proc:=0|>`` 1714); 1715 1716val take_prefetch_abort_exception_ut_EE_F_flags_thm = 1717store_thm ("take_prefetch_abort_exception_ut_EE_F_flags_thm", 1718``! s1 a s1' g . 1719 mmu_requirements s1 g ��� 1720 assert_mode_no_access_violation 16w s1 ��� 1721 (take_prefetch_abort_exception <|proc := 0|> s1 = ValueState a s1') ==> 1722 (((s1'.psrs (0,CPSR)).F = (s1.psrs (0,CPSR)).F) /\ 1723 (s1'.coprocessors.state.cp15= 1724 s1.coprocessors.state.cp15) 1725 /\ (s1.information = s1'.information ) 1726 /\ ((s1.psrs (0,CPSR)).F = (s1'.psrs (0,CPSR)).F))`` 1727, 1728prove_take_exception_ut_EE_F_flags_thm ``23w:bool[5]`` 1729 take_prefetch_abort_exception_nav_thm 1730 ``take_prefetch_abort_exception <|proc:=0|>`` 1731); 1732 1733val take_irq_exception_ut_EE_F_flags_thm = 1734store_thm ("take_irq_exception_ut_EE_F_flags_thm", 1735``! s1 a s1' g . 1736 mmu_requirements s1 g ��� 1737 assert_mode_no_access_violation 16w s1 ��� 1738 (take_irq_exception <|proc := 0|> s1 = ValueState a s1') ==> 1739 (((s1'.psrs (0,CPSR)).F = (s1.psrs (0,CPSR)).F) /\ 1740 (s1'.coprocessors.state.cp15= 1741 s1.coprocessors.state.cp15) 1742 /\ (s1.information = s1'.information ) 1743 /\ ((s1.psrs (0,CPSR)).F = (s1'.psrs (0,CPSR)).F))`` 1744, 1745prove_take_exception_ut_EE_F_flags_thm ``18w:bool[5]`` 1746 take_irq_exception_nav_thm 1747 ``take_irq_exception <|proc:=0|>`` 1748); 1749 1750fun prove_take_exception_priv_constraints_thm 1751 cfc_thm 1752 spc_thm 1753 ut_EE_F_flags_thm 1754 spsr_thm 1755 lr_thm 1756 = 1757 let 1758 val sl = [``s1:arm_state``,``a:unit``,``s1':arm_state``] 1759 in 1760 RW_TAC (bool_ss) [priv_mode_constraints_v3_def,priv_mode_constraints_v2a_def, 1761 priv_mode_constraints_v2_def,satisfy_priv_constraints_v2_def, 1762 priv_mode_constraints_v1_def,satisfy_priv_constraints_v2a_def, 1763 satisfy_priv_constraints_v3_def] 1764 THEN FIRST_PROVE 1765 [ 1766 FULL_SIMP_TAC (srw_ss()) [], 1767 MP_TAC 1768 (SIMP_RULE (srw_ss()) [] (SPECL (sl @ [``g:bool[32]``]) 1769 ut_EE_F_flags_thm)) 1770 THEN FULL_SIMP_TAC (srw_ss()) [] 1771 THEN METIS_TAC [ARM_MODE_def, ARM_READ_CPSR_def, 1772 assert_mode_no_access_violation_def] 1773 , 1774 MP_TAC (SPECL sl 1775 cfc_thm) 1776 THEN FULL_SIMP_TAC (srw_ss()) [] 1777 , 1778 MP_SPECL_TAC sl 1779 spc_thm 1780 THEN FULL_SIMP_TAC (srw_ss()) 1781 [ARM_MODE_def,ARM_READ_CPSR_def] 1782 , 1783 MP_SPECL_TAC [``s1:arm_state``,``s1':arm_state``,``a:unit``] 1784 (SIMP_RULE (bool_ss) [satisfy_SPSR_constraints_def] spsr_thm) 1785 THEN (TRY (Q.UNABBREV_TAC `spsr`)) 1786 THEN FULL_SIMP_TAC (srw_ss()) [get_spsr_by_mode_def, 1787 ARM_MODE_def,ARM_READ_CPSR_def] 1788 , 1789 MP_SPECL_TAC [``s1:arm_state``,``s1':arm_state``,``a:unit``] 1790 (SIMP_RULE (bool_ss) [satisfy_LR_constraints_def] lr_thm) 1791 THEN FULL_SIMP_TAC (srw_ss()) [get_lr_by_mode_def, 1792 ARM_MODE_def,ARM_READ_CPSR_def] 1793 ] 1794 end; 1795 1796val take_undef_instr_exception_priv_constraints_thm = 1797store_thm ("take_undef_instr_exception_priv_constraints_thm", 1798`` satisfy_priv_constraints_v3 (take_undef_instr_exception <|proc := 0|>) 1799 16w 27w ``, 1800 prove_take_exception_priv_constraints_thm 1801 take_undef_instr_exception_cfc_thm 1802 take_undef_instr_exception_spc_thm 1803 take_undef_instr_exception_ut_EE_F_flags_thm 1804 take_undef_instr_exception_spsr_thm 1805 take_undef_instr_exception_LR_thm 1806 ); 1807 1808 1809val take_data_abort_exception_priv_constraints_thm = 1810store_thm ("take_data_abort_exception_priv_constraints_thm", 1811`` satisfy_priv_constraints_v3 (take_data_abort_exception <|proc := 0|>) 1812 16w 23w ``, 1813 prove_take_exception_priv_constraints_thm 1814 take_data_abort_exception_cfc_thm 1815 take_data_abort_exception_spc_thm 1816 take_data_abort_exception_ut_EE_F_flags_thm 1817 take_data_abort_exception_spsr_thm 1818 take_data_abort_exception_LR_thm 1819 ); 1820 1821val take_prefetch_abort_exception_priv_constraints_thm = 1822store_thm ("take_prefetch_abort_exception_priv_constraints_thm", 1823`` satisfy_priv_constraints_v3 (take_prefetch_abort_exception <|proc := 0|>) 1824 16w 23w ``, 1825 prove_take_exception_priv_constraints_thm 1826 take_prefetch_abort_exception_cfc_thm 1827 take_prefetch_abort_exception_spc_thm 1828 take_prefetch_abort_exception_ut_EE_F_flags_thm 1829 take_prefetch_abort_exception_spsr_thm 1830 take_prefetch_abort_exception_LR_thm 1831 ); 1832 1833val take_irq_exception_priv_constraints_thm = 1834store_thm ("take_irq_exception_priv_constraints_thm", 1835`` satisfy_priv_constraints_v3 (take_irq_exception <|proc := 0|>) 1836 16w 18w ``, 1837 prove_take_exception_priv_constraints_thm 1838 take_irq_exception_cfc_thm 1839 take_irq_exception_spc_thm 1840 take_irq_exception_ut_EE_F_flags_thm 1841 take_irq_exception_spsr_thm 1842 take_irq_exception_LR_thm 1843 ); 1844 1845val take_svc_exception_priv_constraints_thm = 1846store_thm ("take_svc_exception_priv_constraints_thm", 1847 let 1848 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1849 ``take_svc_exception <|proc:=0|> `` 1850 val (_, a) = (dest_eq (concl athm)) 1851 val (_,_,rb)= decompose_term a 1852 in 1853 `` satisfy_priv_constraints_v2 ^rb 16w 19w `` 1854 end 1855 , 1856 prove_take_exception_priv_constraints_thm 1857 take_svc_exception_cfc_thm 1858 take_svc_exception_spc_thm 1859 take_svc_exception_ut_EE_F_flags_thm 1860 take_svc_exception_spsr_thm 1861 take_svc_exception_LR_thm 1862 ); 1863 1864 1865(*******************************************************) 1866 1867val take_undef_instr_exception_priv_nav_thm = 1868 store_thm ("take_undef_instr_exception_priv_nav_thm", 1869 `` preserve_relation_mmu 1870 (take_undef_instr_exception <|proc := 0|> ) 1871 (assert_mode_no_access_violation 16w ) 1872 (assert_mode 27w) priv_mode_constraints_v3 priv_mode_similar`` 1873, 1874MP_TAC take_undef_instr_exception_priv_mode_similar_thm 1875THEN MP_TAC take_undef_instr_exception_priv_constraints_thm 1876THEN MP_TAC ( take_undef_instr_exception_nav_thm) 1877THEN METIS_TAC [preserve_relation_in_priv_mode_v3_thm]); 1878 1879 1880val take_data_abort_exception_priv_nav_thm = 1881 store_thm ("take_data_abort_exception_priv_nav_thm" 1882, `` preserve_relation_mmu 1883 (take_data_abort_exception <|proc := 0|> ) 1884 (assert_mode_no_access_violation 16w ) 1885 (assert_mode 23w) priv_mode_constraints_v3 priv_mode_similar`` 1886, 1887 MP_TAC take_data_abort_exception_priv_mode_similar_thm 1888THEN MP_TAC take_data_abort_exception_priv_constraints_thm 1889THEN MP_TAC ( take_data_abort_exception_nav_thm) 1890THEN METIS_TAC [preserve_relation_in_priv_mode_v3_thm]); 1891 1892val take_prefetch_abort_exception_priv_nav_thm = 1893 store_thm ("take_prefetch_abort_exception_priv_nav_thm" 1894, `` preserve_relation_mmu 1895 (take_prefetch_abort_exception <|proc := 0|> ) 1896 (assert_mode_no_access_violation 16w ) 1897 (assert_mode 23w) priv_mode_constraints_v3 priv_mode_similar`` 1898, 1899 MP_TAC take_prefetch_abort_exception_priv_mode_similar_thm 1900THEN MP_TAC take_prefetch_abort_exception_priv_constraints_thm 1901THEN MP_TAC take_prefetch_abort_exception_nav_thm 1902THEN METIS_TAC [preserve_relation_in_priv_mode_v3_thm]); 1903 1904val take_irq_exception_priv_nav_thm = 1905 store_thm ("take_irq_exception_priv_nav_thm" 1906, `` preserve_relation_mmu 1907 (take_irq_exception <|proc := 0|> ) 1908 (assert_mode_no_access_violation 16w ) 1909 (assert_mode 18w) priv_mode_constraints_v3 priv_mode_similar`` 1910, 1911 MP_TAC take_irq_exception_priv_mode_similar_thm 1912THEN MP_TAC take_irq_exception_priv_constraints_thm 1913THEN MP_TAC ( take_irq_exception_nav_thm) 1914THEN METIS_TAC [preserve_relation_in_priv_mode_v3_thm]); 1915 1916 1917val take_svc_exception_priv_nav_thm = 1918 store_thm ("take_svc_exception_priv_nav_thm" 1919, 1920 let 1921 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1922 ``take_svc_exception <|proc:=0|> ``; 1923 val (_, a) = (dest_eq (concl athm)) 1924 val (_,_,rb)= decompose_term a; 1925 in 1926 `` preserve_relation_mmu 1927 ^rb 1928 (assert_mode_no_access_violation 16w ) 1929 (assert_mode 19w) priv_mode_constraints_v2 priv_mode_similar`` 1930 end 1931, 1932 MP_TAC take_svc_exception_priv_mode_similar_thm 1933 THEN MP_TAC take_svc_exception_priv_constraints_thm 1934 THEN MP_TAC take_svc_exception_nav_thm 1935 THEN METIS_TAC [preserve_relation_in_priv_mode_v2_thm]); 1936 1937 1938val take_undef_instr_exception_av_thm = 1939 store_thm ("take_undef_instr_exception_av_thm", 1940``preserve_relation_mmu 1941 (take_undef_instr_exception <|proc := 0|>) 1942 (assert_mode_access_violation 16w) 1943 (assert_mode_access_violation 16w) 1944 priv_mode_constraints_v3 priv_mode_similar`` 1945 , 1946 let val (_,take_undef_exception_body) = 1947 (dest_eq o concl) (REWRITE_CONV [take_undef_instr_exception_def] 1948 ``take_undef_instr_exception <|proc:=0|> ``); 1949 val (al,ar,arb)= decompose_term take_undef_exception_body; 1950 val al_type = get_monad_type (type_of (al)); 1951 val () = global_mode := ``16w:bool[5]``; 1952 val pthms1 = [trans_tautology_fun_thm, 1953 reflex_tautology_fun_thm, 1954 tautology_fun_def, 1955 tautology_fun_def, 1956 errorT_thm 1957 ]; 1958 val uargs = [``tautology_fun``,``tautology_fun``, 1959 ``27w:bool[5]``,``_thm1``]; 1960 val (read_part_thm,_) = prove al ``(assert_mode 16w)`` 1961 ``(assert_mode 16w)`` uargs pthms1; 1962 in 1963 RW_TAC (srw_ss()) [take_undef_instr_exception_def] 1964 THEN MP_TAC const_comp_take_undef_svc_exception_rp_thm 1965 THEN MP_TAC (MP (SPEC al (INST_TYPE 1966 [alpha |-> al_type] 1967 user_pr_taut_imp_priv_pr_thm)) 1968 read_part_thm ) 1969 THEN METIS_TAC [access_violation_implies_no_mode_changing_thm] 1970 end); 1971 1972val take_svc_exception_av_thm = 1973 store_thm ("take_svc_exception_av_thm", 1974 let 1975 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1976 ``take_svc_exception <|proc:=0|> `` 1977 val (_, a) = (dest_eq (concl athm)) 1978 val (_,_,rb)= decompose_term a; 1979 in 1980 ``preserve_relation_mmu 1981 ^rb 1982 (assert_mode_access_violation 16w) 1983 (assert_mode_access_violation 16w) 1984 priv_mode_constraints_v2 priv_mode_similar`` 1985 end 1986 , 1987 let 1988 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 1989 ``take_svc_exception <|proc:=0|> `` 1990 val (_, a) = (dest_eq (concl athm)) 1991 val (_,_,body)= decompose_term a 1992 val (al,_,body)= decompose_term body; 1993 1994 val al_type = get_monad_type (type_of (al)); 1995 val () = global_mode := ``16w:bool[5]``; 1996 val pthms1 = [trans_tautology_fun_thm, 1997 reflex_tautology_fun_thm, 1998 tautology_fun_def, 1999 tautology_fun_def, 2000 errorT_thm 2001 ]; 2002 val uargs = [``tautology_fun``,``tautology_fun``, 2003 ``19w:bool[5]``,``_thm1``]; 2004 val (read_part_thm,_) = prove al ``(assert_mode 16w)`` 2005 ``(assert_mode 16w)`` uargs pthms1; 2006 in 2007 RW_TAC (srw_ss()) [take_svc_exception_def] 2008 THEN MP_TAC const_comp_take_undef_svc_exception_rp_thm 2009 THEN MP_TAC (MP (SPEC al (INST_TYPE 2010 [alpha |-> al_type] 2011 user_pr_taut_imp_priv_pr_thm)) 2012 read_part_thm ) 2013 THEN METIS_TAC [access_violation_implies_no_mode_changing_v1_thm] 2014 end); 2015 2016 2017val take_data_abort_exception_av_thm = 2018 store_thm ("take_data_abort_exception_av_thm", 2019``preserve_relation_mmu 2020 (take_data_abort_exception <|proc := 0|>) 2021 (assert_mode_access_violation 16w) 2022 (assert_mode_access_violation 16w) 2023 priv_mode_constraints_v3 priv_mode_similar`` 2024 , 2025 let val (_,te_body) = 2026 (dest_eq o concl) (REWRITE_CONV [take_data_abort_exception_def] 2027 ``take_data_abort_exception <|proc:=0|> ``); 2028 val (al,ar,arb)= decompose_term te_body; 2029 val al_type = get_monad_type (type_of (al)); 2030 val () = global_mode := ``16w:bool[5]``; 2031 val pthms1 = [trans_tautology_fun_thm, 2032 reflex_tautology_fun_thm, 2033 tautology_fun_def, 2034 tautology_fun_def, 2035 errorT_thm 2036 ]; 2037 val uargs = [``tautology_fun``,``tautology_fun``, 2038 ``27w:bool[5]``,``_thm1``]; 2039 val (read_part_thm,_) = prove al ``(assert_mode 16w)`` 2040 ``(assert_mode 16w)`` uargs pthms1; 2041 in 2042 RW_TAC (srw_ss()) [take_data_abort_exception_def] 2043 THEN MP_TAC const_comp_take_abort_irq_exception_rp_thm 2044 THEN MP_TAC (MP (SPEC al (INST_TYPE 2045 [alpha |-> al_type] 2046 user_pr_taut_imp_priv_pr_thm)) 2047 read_part_thm ) 2048 THEN METIS_TAC [access_violation_implies_no_mode_changing_thm] 2049 end); 2050 2051val take_prefetch_abort_exception_av_thm = 2052 store_thm ("take_prefetch_abort_exception_av_thm", 2053``preserve_relation_mmu 2054 (take_prefetch_abort_exception <|proc := 0|>) 2055 (assert_mode_access_violation 16w) 2056 (assert_mode_access_violation 16w) 2057 priv_mode_constraints_v3 priv_mode_similar`` 2058 , 2059 let val (_,te_body) = 2060 (dest_eq o concl) (REWRITE_CONV [take_prefetch_abort_exception_def] 2061 ``take_prefetch_abort_exception <|proc:=0|> ``); 2062 val (al,ar,arb)= decompose_term te_body; 2063 val al_type = get_monad_type (type_of (al)); 2064 val () = global_mode := ``16w:bool[5]``; 2065 val pthms1 = [trans_tautology_fun_thm, 2066 reflex_tautology_fun_thm, 2067 tautology_fun_def, 2068 tautology_fun_def, 2069 errorT_thm 2070 ]; 2071 val uargs = [``tautology_fun``,``tautology_fun``, 2072 ``27w:bool[5]``,``_thm1``]; 2073 val (read_part_thm,_) = prove al ``(assert_mode 16w)`` 2074 ``(assert_mode 16w)`` uargs pthms1; 2075 in 2076 RW_TAC (srw_ss()) [take_prefetch_abort_exception_def] 2077 THEN MP_TAC const_comp_take_abort_irq_exception_rp_thm 2078 THEN MP_TAC (MP (SPEC al (INST_TYPE 2079 [alpha |-> al_type] 2080 user_pr_taut_imp_priv_pr_thm)) 2081 read_part_thm ) 2082 THEN METIS_TAC [access_violation_implies_no_mode_changing_thm] 2083 end); 2084 2085 2086val take_irq_exception_av_thm = 2087 store_thm ("take_irq_exception_av_thm", 2088``preserve_relation_mmu 2089 (take_irq_exception <|proc := 0|>) 2090 (assert_mode_access_violation 16w) 2091 (assert_mode_access_violation 16w) 2092 priv_mode_constraints_v3 priv_mode_similar`` 2093 , 2094 let val (_,te_body) = 2095 (dest_eq o concl) (REWRITE_CONV [take_irq_exception_def] 2096 ``take_irq_exception <|proc:=0|> ``); 2097 val (al,ar,arb)= decompose_term te_body; 2098 val al_type = get_monad_type (type_of (al)); 2099 val () = global_mode := ``16w:bool[5]``; 2100 val pthms1 = [trans_tautology_fun_thm, 2101 reflex_tautology_fun_thm, 2102 tautology_fun_def, 2103 tautology_fun_def, 2104 errorT_thm 2105 ]; 2106 val uargs = [``tautology_fun``,``tautology_fun``, 2107 ``27w:bool[5]``,``_thm1``]; 2108 val (read_part_thm,_) = prove al ``(assert_mode 16w)`` 2109 ``(assert_mode 16w)`` uargs pthms1; 2110 in 2111 RW_TAC (srw_ss()) [take_irq_exception_def] 2112 THEN MP_TAC const_comp_take_abort_irq_exception_rp_thm 2113 THEN MP_TAC (MP (SPEC al (INST_TYPE 2114 [alpha |-> al_type] 2115 user_pr_taut_imp_priv_pr_thm)) 2116 read_part_thm ) 2117 THEN METIS_TAC [access_violation_implies_no_mode_changing_thm] 2118 end); 2119 2120 2121val take_undef_instr_exception_thm = 2122store_thm ("take_undef_instr_exception_thm", 2123``preserve_relation_mmu 2124 (take_undef_instr_exception <|proc := 0|> ) 2125 (assert_mode 16w ) 2126 (comb_mode 16w 27w ) 2127 priv_mode_constraints_v3 priv_mode_similar`` 2128, 2129ASSUME_TAC take_undef_instr_exception_av_thm 2130THEN ASSUME_TAC take_undef_instr_exception_priv_nav_thm 2131THEN RW_TAC (srw_ss()) [deduce_pr_from_pr_av_and_pr_no_av_thm]); 2132 2133 2134 2135val take_data_abort_exception_thm = 2136store_thm ("take_data_abort_exception_thm", 2137``preserve_relation_mmu 2138 (take_data_abort_exception <|proc := 0|> ) 2139 (assert_mode 16w ) 2140 (comb_mode 16w 23w ) 2141 priv_mode_constraints_v3 priv_mode_similar`` 2142, 2143ASSUME_TAC take_data_abort_exception_av_thm 2144THEN ASSUME_TAC take_data_abort_exception_priv_nav_thm 2145THEN RW_TAC (srw_ss()) [deduce_pr_from_pr_av_and_pr_no_av_thm]); 2146 2147 2148val take_prefetch_abort_exception_thm = 2149store_thm ("take_prefetch_abort_exception_thm", 2150``preserve_relation_mmu 2151 (take_prefetch_abort_exception <|proc := 0|> ) 2152 (assert_mode 16w ) 2153 (comb_mode 16w 23w ) 2154 priv_mode_constraints_v3 priv_mode_similar`` 2155, 2156ASSUME_TAC take_prefetch_abort_exception_av_thm 2157THEN ASSUME_TAC take_prefetch_abort_exception_priv_nav_thm 2158THEN RW_TAC (srw_ss()) [deduce_pr_from_pr_av_and_pr_no_av_thm]); 2159 2160val take_irq_exception_thm = 2161store_thm ("take_irq_exception_thm", 2162``preserve_relation_mmu 2163 (take_irq_exception <|proc := 0|> ) 2164 (assert_mode 16w ) 2165 (comb_mode 16w 18w ) 2166 priv_mode_constraints_v3 priv_mode_similar`` 2167, 2168ASSUME_TAC take_irq_exception_av_thm 2169THEN ASSUME_TAC take_irq_exception_priv_nav_thm 2170THEN RW_TAC (srw_ss()) [deduce_pr_from_pr_av_and_pr_no_av_thm]); 2171 2172val take_svc_exception_part2_def = 2173Define `take_svc_exception_part2 ii = 2174(read_reg ii 15w ||| exc_vector_base ii ||| read_cpsr ii 2175 ||| read_scr ii ||| read_sctlr ii) >>= 2176 (��(pc,ExcVectorBase,cpsr,scr,sctlr). 2177 (condT (cpsr.M = 22w) (write_scr ii (scr with NS := F)) 2178 ||| write_cpsr ii (cpsr with M := 19w)) >>= 2179 (��(u1,u2). 2180 (write_spsr ii cpsr 2181 ||| write_reg ii 14w 2182 (if cpsr.T then pc ��� 2w else pc ��� 4w) 2183 ||| read_cpsr ii >>= 2184 (��cpsr. 2185 write_cpsr ii 2186 (cpsr with 2187 <|I := T; IT := 0w; J := F; T := sctlr.TE; 2188 E := sctlr.EE|>)) 2189 ||| branch_to ii (ExcVectorBase + 8w)) >>= 2190 (��(u1,u2,u3,u4). constT ())))`; 2191 2192val take_svc_exception_part2_thm = 2193store_thm ("take_svc_exception_part2_thm", 2194``preserve_relation_mmu (take_svc_exception_part2 <|proc:=0|>) (assert_mode 16w ) 2195 (comb_mode 16w 19w ) 2196 priv_mode_constraints_v2 priv_mode_similar`` 2197 , 2198 FULL_SIMP_TAC (bool_ss) [take_svc_exception_part2_def] 2199 THEN ASSUME_TAC take_svc_exception_av_thm 2200 THEN ASSUME_TAC take_svc_exception_priv_nav_thm 2201 THEN RW_TAC (srw_ss()) [deduce_pr_from_pr_av_and_pr_no_av_thm] 2202 ) 2203 2204(** this axiom is proven in user_lemma_primitive_operationsTheory under the name IT_advance_thm*) 2205val IT_advance_thm1 = 2206 save_thm("IT_advance_thm1", 2207 new_axiom("IT_advance_thmX", ``preserve_relation_mmu (IT_advance <|proc:=0|>) 2208 (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar``)); 2209 2210val priv_mode_constraints_def = priv_mode_constraints_v1_def; 2211 2212val take_svc_exception_helper_thm = store_thm("take_svc_exception_helper_thm", 2213``! Z A . 2214preserve_relation_mmu (A) 2215 (assert_mode 16w ) 2216 (comb_mode 16w 19w ) 2217 priv_mode_constraints_v2 priv_mode_similar ==> 2218preserve_relation_mmu (Z) 2219 (assert_mode 16w ) 2220 (assert_mode 16w ) 2221 priv_mode_constraints_v1 priv_mode_similar ==> 2222(! state0 state1 a. (Z state0 = ValueState a state1) ==> 2223 (~access_violation state1) ==>(((get_pc_value state1) = (get_pc_value state0)) /\ 2224 ((state1.psrs(0,CPSR)) = 2225 if (((ARMarch2num state0.information.arch = 6) ��� 2226 version_number state0.information.arch ��� 7) /\ 2227 (((state0.psrs (0,CPSR)).IT = 0w) ��� (state0.psrs (0,CPSR)).T)) 2228 then 2229 (state0.psrs(0,CPSR) with IT := ITAdvance ((state0.psrs(0,CPSR)).IT)) 2230 else 2231 (state0.psrs(0,CPSR))))) ==> 2232preserve_relation_mmu (Z >>= (\x.A)) 2233 (assert_mode 16w ) 2234 (comb_mode 16w 19w ) 2235 priv_mode_constraints_v2a priv_mode_similar`` 2236, 2237 RW_TAC (bool_ss) [preserve_relation_mmu_def,seqT_def] 2238 THEN Cases_on ` Z s1` 2239 THEN Cases_on ` Z s2` 2240 THEN RW_TAC (srw_ss()) [seqT_def] 2241 THEN PAT_X_ASSUM ``���g:word32 s1 s2.X`` (fn thm => 2242 ASSUME_SPECL_TAC 2243 [``g:bool[32]``,``s1:arm_state``, 2244 ``s2:arm_state``] thm) 2245 2246 THEN UNDISCH_ALL_TAC 2247 THEN RW_TAC (bool_ss) [] 2248 THEN 2249 FIRST_PROVE 2250 [ 2251 FULL_SIMP_TAC (srw_ss()) [priv_mode_constraints_v2a_def,priv_mode_constraints_v2_def,assert_mode_def,comb_mode_def] 2252 , 2253 (`access_violation b = access_violation b'` by METIS_TAC [similar_def]) 2254 THEN FULL_SIMP_TAC (srw_ss()) [] 2255 , 2256 ASSUME_TAC seqT_access_violation_thm 2257 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 2258 THEN PAT_X_ASSUM ``���g:word32 s1 s2.X`` (fn thm => 2259 ASSUME_SPECL_TAC 2260 [``g:bool[32]``,``b:arm_state``, 2261 ``b':arm_state``] thm) 2262 THEN IMP_RES_TAC untouched_mmu_setup_lem 2263 THEN UNDISCH_ALL_TAC 2264 THEN RW_TAC (srw_ss()) [] 2265 THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def] 2266 THEN REPEAT STRIP_TAC 2267 THEN FIRST_PROVE 2268 [ 2269 IMP_RES_TAC untouched_trans 2270 THEN FULL_SIMP_TAC (srw_ss()) [] 2271 , 2272 FULL_SIMP_TAC (srw_ss()) [priv_mode_constraints_v2a_def, 2273 priv_mode_constraints_v2_def, 2274 assert_mode_def,comb_mode_def] 2275 THEN REPEAT STRIP_TAC 2276 THEN FIRST_PROVE 2277 [ 2278 FULL_SIMP_TAC (srw_ss()) [priv_mode_constraints_v2a_def,priv_mode_constraints_def, 2279 priv_mode_constraints_v2_def,assert_mode_def, 2280 comb_mode_def,LET_DEF,ARM_MODE_def, 2281 ARM_READ_CPSR_def] 2282 , 2283 IMP_RES_TAC similar_states_have_same_mode_thm 2284 THEN FULL_SIMP_TAC (srw_ss()) [ARM_MODE_def,ARM_READ_CPSR_def] 2285 , 2286 2287 PAT_X_ASSUM ``��� s1:arm_state s2.X`` (fn thm => 2288 ASSUME_SPECL_TAC 2289 [``s1:arm_state``, 2290 ``b:arm_state``, ``a:'a``] thm 2291 THEN ASSUME_SPECL_TAC 2292 [``s2:arm_state``, 2293 ``b':arm_state``, ``a:'a``] thm) 2294 2295 THEN UNDISCH_ALL_TAC 2296 THEN RW_TAC (srw_ss()) [] 2297 THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def] 2298 , 2299 2300 IMP_RES_TAC (SIMP_RULE bool_ss [trans_fun_def] trans_priv_mode_constraints_thm) 2301 ] 2302 ] 2303 ] 2304) 2305 2306 2307val IT_advance_svc_spsr_thm = 2308store_thm ("IT_advance_svc_spsr_thm", 2309``(! state0 state1 a. (IT_advance <|proc := 0|> state0 = ValueState a state1) ==> 2310 (~access_violation state1) ==> 2311(((get_pc_value state1) = (get_pc_value state0)) /\ 2312 ((state1.psrs(0,CPSR)) = 2313 if (((ARMarch2num state0.information.arch = 6) ��� 2314 version_number state0.information.arch ��� 7) /\ 2315 (((state0.psrs (0,CPSR)).IT = 0w) ��� (state0.psrs (0,CPSR)).T)) 2316 then 2317 (state0.psrs(0,CPSR) with IT := ITAdvance ((state0.psrs(0,CPSR)).IT)) 2318 else 2319 (state0.psrs(0,CPSR)))))`` 2320 , 2321 RW_TAC (srw_ss()) [] 2322 THEN PAT_X_ASSUM ``IT_advance <|proc := 0|> state0 = ValueState a state1`` (fn thm => ASSUME_TAC (EVAL_RULE thm)) 2323 THEN Cases_on `access_violation state0` 2324 THEN FIRST_PROVE 2325 [ 2326 FULL_SIMP_TAC (srw_ss()) [] 2327 , 2328 Cases_on `(ARMarch2num state0.information.arch = 6) ��� 2329 version_number state0.information.arch ��� 7` 2330 THEN 2331 Cases_on `((state0.psrs (0,CPSR)).IT = 0w) ��� (state0.psrs (0,CPSR)).T` 2332 THEN NTAC 2 (UNDISCH_ALL_TAC 2333 THEN FULL_SIMP_TAC (srw_ss()) [] 2334 THEN RW_TAC (srw_ss()) [] 2335 THEN EVAL_TAC 2336 THEN FULL_SIMP_TAC (srw_ss()) []) 2337 ] 2338 ); 2339 2340val take_svc_exception_thm = 2341 store_thm ("take_svc_exception_thm", 2342 ``preserve_relation_mmu (take_svc_exception <|proc := 0|>) 2343 (assert_mode 16w ) 2344 (comb_mode 16w 19w ) 2345 priv_mode_constraints_v2a priv_mode_similar ``, 2346 2347 FULL_SIMP_TAC (srw_ss()) [take_svc_exception_def] 2348 THEN ASSUME_TAC take_svc_exception_part2_thm 2349 THEN ASSUME_TAC IT_advance_thm1 2350 THEN ASSUME_TAC IT_advance_svc_spsr_thm 2351 THEN IMP_RES_TAC (INST_TYPE [beta |-> ``:unit`` ] take_svc_exception_helper_thm) 2352 THEN FULL_SIMP_TAC (srw_ss()) [take_svc_exception_part2_def] 2353 ); 2354 2355val _ = export_theory(); 2356