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 4 tacticsLib ARM_prover_extLib; 5 6val _ = new_theory("priv_constraints_lr"); 7 8 9(****************************************************************) 10(* CONSTRAINTS ON LINK REGISTER IN PRIVILEGED MODE *) 11(* Narges *) 12(****************************************************************) 13 14val let_ss = simpLib.mk_simpset [boolSimps.LET_ss] ; 15val _ = goalStack.chatting := !Globals.interactive 16 17val prove_abs_LR_const_action = 18 fn (a, thms, abody_thm, expr) => 19 let 20 val _ = set_goal([], `` 21 (priv_LR_constraints_abs ^a ^expr (mode:bool[5]) ) ``) 22 val (a_abs,a_body) = pairLib.dest_pabs a; 23 val unbeta_thm= (PairRules.UNPBETA_CONV a_abs a_body) 24 val unbeta_a = mk_comb (a, a_abs) 25 val snd = get_type_inst (type_of(a_body) , false) 26 val a_body_type = get_type_inst (snd, true); 27 val proved_unbeta_lemma = prove( 28 ``(priv_LR_constraints ^a_body ^expr mode)= 29 (priv_LR_constraints ^unbeta_a ^expr mode)``, 30 (ASSUME_TAC (SPECL [a_body,``^unbeta_a``, expr,``mode:bool[5]``] 31 (INST_TYPE [beta |-> a_body_type, 32 alpha |-> ``:arm_state``] 33 (List.nth(thms,0))))) 34 THEN ASSUME_TAC unbeta_thm 35 THEN RES_TAC); 36 37 val proved_preserve_unbeta_a = 38 prove(`` (priv_LR_constraints ^unbeta_a ^expr mode )``, 39 (ASSUME_TAC (proved_unbeta_lemma)) 40 THEN (ASSUME_TAC abody_thm) 41 THEN (FULL_SIMP_TAC (srw_ss()) [])); 42 43 val abs_type = type_of a_abs 44 val (abs_args, abs_body) = generate_uncurry_abs a 45 val tacs = (ASSUME_TAC proved_preserve_unbeta_a) 46 val gen_preserve_unbeta_thm = generalize_theorem proved_preserve_unbeta_a a; 47 val tacs = tacs THEN (ASSUME_TAC gen_preserve_unbeta_thm) 48 THEN (ASSUME_TAC ( 49 SPECL[a, expr,``mode:bool[5]``] 50 (INST_TYPE [alpha |-> abs_type, 51 beta |-> ``:arm_state``, 52 gamma |-> a_body_type] 53 (List.nth(thms,1))))) 54 THEN (RW_TAC (srw_ss()) []) 55 THEN (FULL_SIMP_TAC (srw_ss()) []) 56 THEN (UNDISCH_ALL_TAC THEN 57 (RW_TAC (srw_ss()) []) 58 THEN (FULL_SIMP_TAC (srw_ss()) [])) 59 val _ = e (tacs) 60 val proved_thm = top_thm() 61 val _ = proofManagerLib.drop(); 62 in 63 (proved_thm,tacs) 64 end 65 66val untouched_LR_abs_def = 67 Define `untouched_LR_abs f mode = 68 !s a c s'. (f a s = ValueState c s') ==> 69 let lr = get_lr_by_mode mode 70 in 71 (((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M) /\ 72 (s'.registers (0, lr) = 73 s.registers (0, lr)))`; 74 75val untouched_LR_def = 76 Define `untouched_LR f mode = 77 !s c s'. (f s = ValueState c s') ==> 78 (* (ARM_MODE s' = 19w) ==> *) 79 let lr = get_lr_by_mode mode 80 in 81 (((s'.psrs (0,CPSR)).M=(s.psrs (0,CPSR)).M) /\ 82 (s'.registers (0, lr) = 83 s.registers (0, lr)))`; 84 85val priv_LR_constraints_def = 86 Define `priv_LR_constraints f lr_value mode = 87 ! s s' a . (f s = ValueState a s') ==> 88 (~access_violation s') ==> 89 ((s'.psrs (0,CPSR)).M= mode) ==> 90 let lr = get_lr_by_mode mode 91 in 92 (*((s'.psrs(0,CPSR)).M = 19w) ==>*) 93 ((s'.registers (0, lr) = 94 lr_value))`; 95 96 97val priv_LR_constraints_abs_def = 98 Define `priv_LR_constraints_abs f lr_value mode = 99 ! s s' a c. (f c s = ValueState a s') ==> 100 (~access_violation s') ==> 101 ((s'.psrs (0,CPSR)).M= mode) ==> 102 let lr = get_lr_by_mode mode 103 in 104 (*((s'.psrs(0,CPSR)).M = 19w) ==>*) 105 ((s'.registers (0, lr) = 106 lr_value))`; 107 108 109(********************* proof rules *******************************) 110 111val seqT_priv_LR_constraints_before_thm = 112 store_thm("seqT_priv_LR_constraints_before_thm", 113 `` ! g f pc mode . priv_LR_constraints_abs f pc mode ==> 114 priv_LR_constraints (g >>= f) pc mode ``, 115 (RW_TAC (srw_ss()) [seqT_def, 116 priv_LR_constraints_def, 117 priv_LR_constraints_abs_def]) 118 THEN FULL_SIMP_TAC (let_ss) [] 119 THEN ASSUME_TAC 120 (SPECL [``g:'a M``, ``f: 'a -> 'b M``, 121 ``s:arm_state``,``a:'b``, 122 ``s':arm_state``(* ,``b:arm_state``, *) 123 (* ``a':'a`` *)] 124 seqT_access_violation_thm) 125 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 126 THEN Cases_on `g s` 127 THEN FULL_SIMP_TAC (srw_ss()) [] 128 THEN Cases_on `access_violation b` 129 (* THEN Q.UNABBREV_TAC `spsr` *) 130 THEN PAT_X_ASSUM ``! s s' a c .X ==> Z`` 131 (fn thm => ASSUME_TAC 132 (SPECL [``b:arm_state``,``s':arm_state``, 133 ``a:'b``,``a':'a``] thm)) 134 THEN FULL_SIMP_TAC (srw_ss()) [] 135 THEN RES_TAC 136 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 137 ); 138 139val parT_priv_LR_constraints_before_thm = 140 store_thm("parT_priv_LR_constraints_before_thm", 141 `` ! g f pc mode . priv_LR_constraints f pc mode ==> 142 priv_LR_constraints (g ||| f) pc mode ``, 143 RW_TAC (srw_ss()) 144 [parT_def,seqT_def, 145 priv_LR_constraints_def, 146 untouched_LR_def,constT_def] 147 THEN FULL_SIMP_TAC (let_ss) [] 148 THEN IMP_RES_TAC 149 (SIMP_RULE bool_ss 150 [seqT_def,parT_def,constT_def] 151 (SPECL [``g:'a M``, ``f: 'b M``, 152 ``s:arm_state``,``a:('a#'b)``, 153 ``s':arm_state`` ,``b:arm_state``, 154 ``a':'a`` ] 155 parT_access_violation_thm)) 156 THEN Cases_on `g s` 157 THEN Cases_on `f b` 158 (* THEN Q.UNABBREV_TAC `spsr` *) 159 THEN FULL_SIMP_TAC (srw_ss()) [] 160 THEN PAT_X_ASSUM ``! s s' a .(f s = ValueState a s') ==> Z`` (fn thm => ASSUME_TAC 161 (SPECL [``b:arm_state``,``b':arm_state``,``a'':'b``] thm)) 162 THEN Cases_on `access_violation b` 163 THEN Cases_on `access_violation b'` 164 THEN RES_TAC 165 THEN FULL_SIMP_TAC (srw_ss()) [] 166 THEN FIRST_PROVE [ FULL_SIMP_TAC (srw_ss()) [] 167 THEN RW_TAC (srw_ss()) [] , 168 (UNDISCH_ALL_TAC 169 THEN RW_TAC (srw_ss()) [] 170 THEN FULL_SIMP_TAC (srw_ss()) [])]); 171 172val seqT_priv_LR_constraints_after_thm = 173 store_thm("seqT_priv_LR_constraints_after_thm", 174 `` ! g f pc mode . 175 priv_LR_constraints g pc mode ==> 176 ( untouched_LR_abs f mode ) ==> 177 priv_LR_constraints (g >>= f) pc mode ``, 178 (RW_TAC (srw_ss()) [seqT_def, 179 priv_LR_constraints_def, 180 priv_LR_constraints_abs_def, 181 untouched_LR_abs_def]) THEN 182 FULL_SIMP_TAC (let_ss) [] THEN 183 Cases_on `g s` THEN 184 FULL_SIMP_TAC (srw_ss()) [] THEN 185 Cases_on `access_violation b` 186 THEN Q.UNABBREV_TAC `lr` 187 THEN PAT_X_ASSUM ``! s s' a .X ==> Z`` 188 (fn thm => ASSUME_TAC 189 (SPECL [``s:arm_state``,``b:arm_state``, 190 ``a':'a``] thm)) 191 192 THEN PAT_X_ASSUM ``! s1 a c s2. X`` 193 (fn thm => ASSUME_TAC 194 (SPECL [``b:arm_state``,``a':'a``, 195 ``a:'b``,``s':arm_state``] thm)) 196 197 THEN RES_TAC 198 THEN UNDISCH_ALL_TAC 199 THEN RW_TAC (srw_ss()) [] 200 THEN FULL_SIMP_TAC (srw_ss()) [get_lr_by_mode_def] 201 THEN FULL_SIMP_TAC (srw_ss()) []); 202 203val parT_priv_LR_constraints_after_thm = 204 store_thm("parT_priv_LR_constraints_after_thm", 205`` ! g f pc mode . priv_LR_constraints g pc mode ==> 206 (untouched_LR f mode ) ==> 207 priv_LR_constraints (g ||| f) pc mode ``, 208 (RW_TAC (srw_ss()) 209 [parT_def,seqT_def, 210 priv_LR_constraints_def, 211 untouched_LR_def,constT_def]) 212 THEN FULL_SIMP_TAC (let_ss) []THEN 213 Cases_on `g s` THEN 214 Cases_on `f b` THEN 215 Cases_on `access_violation b` THEN 216 Cases_on `access_violation b'` THEN 217 Q.UNABBREV_TAC `lr` THEN 218 FULL_SIMP_TAC (srw_ss()) [] THEN 219 PAT_X_ASSUM ``! s a s' .(f s = ValueState a s') ==> Z`` 220 (fn thm => ASSUME_TAC 221 (SPECL [``b:arm_state``,``a'':'b``,``b':arm_state``] thm)) 222 THEN PAT_X_ASSUM ``! s1 c s2. X`` 223 (fn thm => ASSUME_TAC 224 (SPECL [``s:arm_state``,``b:arm_state``,``a':'a``] thm)) 225 THEN RES_TAC 226 THEN UNDISCH_ALL_TAC 227 THEN RW_TAC (srw_ss()) [] 228 THEN FULL_SIMP_TAC (srw_ss()) [get_lr_by_mode_def] 229 ); 230 231 232val seqT_LR_trans_untouched_thm = 233 store_thm("seqT_LR_trans_untouched_thm", 234 `` !f g mode . 235 (untouched_LR f mode ) ==> 236 (untouched_LR_abs g mode ) ==> 237 (untouched_LR (f>>=g) mode)``, 238 (RW_TAC (srw_ss()) [seqT_def,untouched_LR_abs_def, 239 untouched_LR_def]) 240THEN Cases_on `f s` 241 THEN FULL_SIMP_TAC (let_ss) [] 242 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> X`` 243 (fn thm => ASSUME_TAC 244 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 245 THEN RES_TAC 246 THEN Cases_on `access_violation b` 247 THEN FULL_SIMP_TAC (srw_ss()) [] 248 THEN RW_TAC (srw_ss()) [] 249 THEN PAT_X_ASSUM ``! s a c s'. _`` 250 (fn thm => ASSUME_TAC 251 (SPECL [``b:arm_state``,``a:'a``, 252 ``c:'b``,``s':arm_state``] thm)) 253 THEN RES_TAC 254 THEN FULL_SIMP_TAC (srw_ss()) [] 255 THEN RW_TAC (srw_ss()) []); 256 257val parT_LR_trans_untouched_thm = 258 store_thm("parT_LR_trans_untouched_thm", 259 `` !f g mode. 260 (untouched_LR f mode ) ==> 261 (untouched_LR g mode ) ==> 262 (untouched_LR (f ||| g) mode )``, 263 (RW_TAC (srw_ss()) [seqT_def,parT_def,constT_def, 264 untouched_LR_def]) 265 THEN Cases_on `f s` 266 THEN Cases_on `access_violation b` 267 THEN Cases_on `g b` 268 THEN Cases_on `access_violation b'` 269 THEN FULL_SIMP_TAC (let_ss) [] 270 THEN PAT_X_ASSUM ``! s c s'. X`` 271 (fn thm => ASSUME_TAC 272 (SPECL [``b:arm_state``,``a':'b``, 273 ``b':arm_state``] thm)) 274 THEN PAT_X_ASSUM ``! s1 c s2. (f _ = ValueState _ _) ==> _`` 275 (fn thm => ASSUME_TAC 276 (SPECL [``s:arm_state``,``a:'a``,``b:arm_state``] thm)) 277 THEN RES_TAC 278 THEN FULL_SIMP_TAC (srw_ss()) [] 279 THEN RW_TAC (srw_ss()) [] 280 ); 281 282 283val LR_first_abs_lemma = 284 store_thm ("LR_first_abs_lemma", 285 ``!f g x mode . (f=g) ==> ((priv_LR_constraints f x mode) = 286 (priv_LR_constraints g x mode))``, 287 RW_TAC (srw_ss()) []); 288 289 290val LR_second_abs_lemma = 291 store_thm ("LR_second_abs_lemma", 292 ``! f x mode . (! y. priv_LR_constraints (f y) x mode ) = 293 priv_LR_constraints_abs f x mode ``, 294 RW_TAC (srw_ss()) [priv_LR_constraints_def,priv_LR_constraints_abs_def] 295 THEN METIS_TAC []); 296 297 298(********************* end of proof rules *******************************) 299(******************* basic lemmas **************************************) 300 301val read_cpsr_fixed_lem = 302 store_thm("read_cpsr_fixed_lem", 303``!s . read_cpsr <|proc := 0|> s = ValueState (s.psrs (0,CPSR)) s``, 304 EVAL_TAC 305 THEN RW_TAC (srw_ss()) []); 306 307val write_lr_reg_lrc_thm = 308 store_thm("write_lr_reg_lrc_thm", 309``! value mode. priv_LR_constraints (write_reg <|proc:=0|> 14w value) value mode``, 310 311RW_TAC (bool_ss) [write_reg_def, 312 seqT_def,errorT_def,priv_LR_constraints_def] 313 THEN Cases_on `read_cpsr <|proc := 0|> s` 314 THEN FULL_SIMP_TAC (srw_ss()) [] 315 THEN Cases_on `access_violation b` 316 THENL [ 317 FULL_SIMP_TAC (srw_ss()) [] 318 THEN RW_TAC (srw_ss()) [] 319 THEN FULL_SIMP_TAC (srw_ss()) [], 320 Q.UNABBREV_TAC `lr` 321 THEN ( NTAC 3 (UNDISCH_ALL_TAC 322 THEN EVAL_TAC 323 THEN FULL_SIMP_TAC (srw_ss()) [] 324 THEN RW_TAC (srw_ss()) [])) 325 ]); 326 327val read_cpsr_lrc_ut_thm = 328 store_thm("read_cpsr_lrc_ut_thm", 329 `` ! mode. 330 (untouched_LR (read_cpsr <|proc:=0|> ) mode)``, 331EVAL_TAC 332THEN RW_TAC (srw_ss()) [] ); 333 334val branch_to_lrc_ut_thm = 335 store_thm("branch_to_lrc_ut_thm", 336``!adr mode . untouched_LR ( 337 branch_to <|proc:=0|> adr) mode ``, 338EVAL_TAC 339THEN RW_TAC (srw_ss()) [] 340THEN UNDISCH_ALL_TAC 341THEN EVAL_TAC 342THEN RW_TAC (srw_ss()) [] 343THEN FULL_SIMP_TAC (srw_ss()) []); 344 345val constT_lrc_ut_thm = 346 store_thm("constT_lrc_ut_thm", 347`` untouched_LR_abs (��(u1:unit,u2:unit,u3:unit,u4:unit). constT ()) mode``, 348EVAL_TAC 349THEN RW_TAC (srw_ss()) [] ); 350 351val ui_write_cpsr_LR_ut_thm = 352 store_thm("ui_write_cpsr_LR_ut_thm", 353``untouched_LR ( 354 read_cpsr <|proc:=0|> >>= 355 (��cpsr. 356 write_cpsr <|proc:=0|> 357 (cpsr with 358 <|I := T; IT := 0w; J := F; T := sctlr.TE; 359 E := sctlr.EE|>))) mode``, 360EVAL_TAC 361THEN RW_TAC (srw_ss()) [] 362THEN UNDISCH_ALL_TAC 363THEN EVAL_TAC 364THEN RW_TAC (srw_ss()) [] 365THEN FULL_SIMP_TAC (srw_ss()) []); 366 367val irq_write_cpsr_LR_ut_thm = 368 store_thm("irq_write_cpsr_LR_ut_thm", 369``untouched_LR ( 370 read_cpsr <|proc:=0|> >>= 371 (��cpsr. 372 write_cpsr <|proc:=0|> 373 (cpsr with 374 <|I := T; 375 A := 376 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 377 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 378 E := sctlr.EE|>))) mode``, 379EVAL_TAC 380THEN RW_TAC (srw_ss()) [] 381THEN UNDISCH_ALL_TAC 382THEN EVAL_TAC 383THEN RW_TAC (srw_ss()) [] 384THEN FULL_SIMP_TAC (srw_ss()) []); 385 386val fiq_write_cpsr_LR_ut_thm = 387 store_thm("fiq_write_cpsr_LR_ut_thm", 388``untouched_LR ( 389 read_cpsr <|proc:=0|> >>= 390 (��cpsr. 391 write_cpsr <|proc:=0|> 392 (cpsr with 393 <|I := T; 394 F := 395 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 396 cpsr.F); 397 A := 398 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 399 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 400 E := sctlr.EE|>))) mode``, 401EVAL_TAC 402THEN RW_TAC (srw_ss()) [] 403THEN UNDISCH_ALL_TAC 404THEN EVAL_TAC 405THEN RW_TAC (srw_ss()) [] 406THEN FULL_SIMP_TAC (srw_ss()) []); 407 408 409 410val ab_write_cpsr_LR_ut_thm = 411 store_thm("ab_write_cpsr_LR_ut_thm", 412``untouched_LR ( 413 read_cpsr <|proc:=0|> >>= 414 (��cpsr. 415 write_cpsr <|proc:=0|> 416 (cpsr with 417 <|I := T; 418 A := 419 ((��have_security_exta ��� ��scr.NS ��� scr.AW) ��� 420 cpsr.A); IT := 0w; J := F; T := sctlr.TE; 421 E := sctlr.EE|>))) mode``, 422EVAL_TAC 423THEN RW_TAC (srw_ss()) [] 424THEN UNDISCH_ALL_TAC 425THEN EVAL_TAC 426THEN RW_TAC (srw_ss()) [] 427THEN FULL_SIMP_TAC (srw_ss()) []); 428 429 430fun get_take_exp_writing_part_LR_thm a' rw_cpsr_thm lr_arg vt = 431 432 let 433 val (l,r,rb1)= decompose_term a'; 434 val (l2,r2,rb2)= decompose_term rb1 435 val (l3,r3,rb3)= decompose_term rb2 436 val (l4,r4,rb4)= decompose_term l3 437 val (l5,r5,rb5)= decompose_term r4 438 val (l6,r6,rb6)= decompose_term r5; 439 440 (* proof of r5 *) 441 val thm1 = LIST_MP [ rw_cpsr_thm, 442 (SPECL [vt, 443 ``mode:bool[5]``] 444 branch_to_lrc_ut_thm)] 445 (SPECL [l6,r6,``mode:bool[5]``] 446 (INST_TYPE [alpha |-> ``:unit``, 447 beta |-> ``:unit``] 448 parT_LR_trans_untouched_thm)); 449 (* proof of r4 *) 450 val thm2 = LIST_MP [ 451 (SPECL [lr_arg, 452 ``mode:bool[5]``] 453 write_lr_reg_lrc_thm), 454 thm1] 455 (SPECL [l5,r5,lr_arg, 456 ``mode:bool[5]``] 457 (INST_TYPE [alpha |-> ``:unit``, 458 beta |-> ``:(unit#unit)``] 459 parT_priv_LR_constraints_after_thm)); 460 (* proof of l3 *) 461 val thm3 = 462 MP (SPECL [l4,r4,lr_arg,``mode:bool[5]``] 463 (INST_TYPE [alpha |-> ``:unit``, 464 beta |-> ``:(unit#unit#unit)``] 465 parT_priv_LR_constraints_before_thm)) thm2; 466 (* proof of rb2 *) 467 val thm4 = LIST_MP [ 468 thm3, 469 constT_lrc_ut_thm] 470 (SPECL [l3,r3,lr_arg,``mode:bool[5]``] 471 (INST_TYPE [beta |-> ``:unit``, 472 alpha |-> ``:(unit#unit#unit#unit)``] 473 seqT_priv_LR_constraints_after_thm)); 474 (* proof of rb1 *) 475 val (thm5 , _) = prove_abs_LR_const_action 476 (r2, [LR_first_abs_lemma, 477 LR_second_abs_lemma], 478 thm4, lr_arg); 479 val thm6 = MP (SPECL [l2,r2,lr_arg,``mode:bool[5]``] 480 (INST_TYPE [beta |-> ``:unit``, 481 alpha |-> ``:(unit#unit)``] 482 seqT_priv_LR_constraints_before_thm)) thm5; 483 in 484 (GEN_ALL thm6) 485 end 486 487 488val take_undef_writing_part_LR_thm = 489 save_thm ("take_undef_writing_part_LR_thm", 490 let 491 val vt = ``(ExcVectorBase + 4w:bool[32])`` 492 val rw_cpsr_thm = ui_write_cpsr_LR_ut_thm 493 val a = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 494 ``take_undef_instr_exception <|proc:=0|> `` 495 val (_, a') = (dest_eq (concl a)) 496 in 497 get_take_exp_writing_part_LR_thm a' rw_cpsr_thm ``(if cpsr:ARMpsr.T then 498 (pc:word32) ��� 2w else pc ��� 4w)`` vt 499 end 500 ); 501 502 503val take_data_abort_writing_part_LR_thm = 504 save_thm ("take_data_abort_writing_part_LR_thm", 505 let val vt = ``(ExcVectorBase + 16w:bool[32])`` 506 val rw_cpsr_thm = ab_write_cpsr_LR_ut_thm; 507 val a = SIMP_CONV (bool_ss) [take_data_abort_exception_def] 508 ``take_data_abort_exception <|proc:=0|> `` 509 val (_, a') = (dest_eq (concl a)) 510 val lr_arg = ``(if cpsr:ARMpsr.T then 511 (pc:word32) else pc ��� 4w)``; 512 in 513 get_take_exp_writing_part_LR_thm a' rw_cpsr_thm lr_arg vt 514 end 515 ); 516 517 518val take_fiq_writing_part_LR_thm = 519 save_thm ("take_fiq_writing_part_LR_thm", 520 let val vt = ``(ExcVectorBase + 28w:bool[32])`` 521 val rw_cpsr_thm = fiq_write_cpsr_LR_ut_thm 522 val a = SIMP_CONV (bool_ss) [take_fiq_exception_def] 523 ``take_fiq_exception <|proc:=0|> `` 524 val (_, a') = (dest_eq (concl a)) 525 val lr_arg = ``(if cpsr:ARMpsr.T then 526 (pc:word32) else pc ��� 4w)`` 527 in 528 get_take_exp_writing_part_LR_thm a' rw_cpsr_thm lr_arg vt 529 end 530 ); 531 532val take_irq_writing_part_LR_thm = 533 save_thm ("take_irq_writing_part_LR_thm", 534 let val vt = ``(ExcVectorBase + 24w:bool[32])`` 535 val rw_cpsr_thm = irq_write_cpsr_LR_ut_thm 536 val a = SIMP_CONV (bool_ss) [take_irq_exception_def] 537 ``take_irq_exception <|proc:=0|> `` 538 val (_, a') = (dest_eq (concl a)) 539 val lr_arg = ``(if cpsr:ARMpsr.T then 540 (pc:word32) else pc ��� 4w)`` 541 in 542 get_take_exp_writing_part_LR_thm a' rw_cpsr_thm lr_arg vt 543 end 544 ); 545 546val take_prefetch_abort_writing_part_LR_thm = 547 save_thm ("take_prefetch_abort_writing_part_LR_thm", 548 let val vt = ``(ExcVectorBase + 12w:bool[32])`` 549 val rw_cpsr_thm = ab_write_cpsr_LR_ut_thm 550 val a = SIMP_CONV (bool_ss) [take_prefetch_abort_exception_def] 551 ``take_prefetch_abort_exception <|proc:=0|> `` 552 val (_, a') = (dest_eq (concl a)) 553 val lr_arg = ``(if cpsr:ARMpsr.T then 554 (pc:word32) else pc ��� 4w)`` 555 in 556 get_take_exp_writing_part_LR_thm a' rw_cpsr_thm lr_arg vt 557 end 558 ); 559 560 561val take_svc_writing_part_LR_thm = 562 save_thm ("take_svc_writing_part_LR_thm", 563 let val vt = ``(ExcVectorBase + 8w:bool[32])`` 564 val rw_cpsr_thm = ui_write_cpsr_LR_ut_thm 565 val a = SIMP_CONV (bool_ss) [take_svc_exception_def] 566 ``take_svc_exception <|proc:=0|> `` 567 val (_, a') = (dest_eq (concl a)) 568 val (_,_,rb) = decompose_term a' 569 val lr_arg = ``(if cpsr:ARMpsr.T then 570 ((pc:word32) - 2w) else pc ��� 4w)`` 571 572 in 573 get_take_exp_writing_part_LR_thm rb rw_cpsr_thm lr_arg vt 574 end); 575 576 577val satisfy_LR_constraints_def = 578 Define ` satisfy_LR_constraints f mode value = 579 ! s s' a . 580 (f s = ValueState a s') ==> 581 ((s'.psrs(0,CPSR)).M = mode) ==> 582 (~access_violation s') ==> 583 (s'.registers (0, get_lr_by_mode (mode)) = 584 (if (s.psrs (0,CPSR)).T then 585 (get_pc_value s - 2w) + value 586 else 587 (get_pc_value s) - 4w))`; 588 589val satisfy_LR_constraints_abs_def = 590 Define ` satisfy_LR_constraints_abs f mode value = 591 ! s c s' a . 592 (f c s = ValueState a s') ==> 593 ((s'.psrs(0,CPSR)).M = mode) ==> 594 (~access_violation s') ==> 595 (s'.registers (0, get_lr_by_mode (mode)) = 596 (if (s.psrs (0,CPSR)).T then 597 (get_pc_value s - 2w) + value 598 else 599 (get_pc_value s) - 4w ))`; 600 601 602 603fun prove_take_exception_LR_constraints te te_def wp_thm fixed_rp_thm fixed_cpsr_thm 604 fixed_pc_thm2 const_comp_rp_thm sl_elm2 605 spec_lists ltype = 606 let 607 val (l,r,rb1)= decompose_term te 608 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 609 val spec_list = List.nth(spec_lists,0) 610 val spec_list2 = List.nth(spec_lists,1) 611 val spec_list3 = List.nth(spec_lists,2) 612 in 613 RW_TAC (bool_ss) [te_def, 614 satisfy_LR_constraints_def 615 ] 616 THEN Cases_on [QUOTE ("("^(term_to_string l) ^ ") s")] 617 THEN IMP_RES_TAC seqT_access_violation_thm 618 THEN IMP_RES_SIMP_TAC [const_comp_def] const_comp_rp_thm 619 THEN RW_TAC (bool_ss) [] 620 THEN FIRST_PROVE 621 [ 622 IMP_RES_TAC hlp_seqT_thm 623 THEN TRY (PAT_X_ASSUM ``!a. X`` (fn thm => ASSUME_SPEC_TAC sl_elm2 thm)) 624 THEN PAT_X_ASSUM ``X a' b'= ValueState a s'`` 625 (fn thm => ASSUME_TAC (PairRules.PBETA_RULE thm)) 626 THEN ASSUME_TAC ( SPECL 627 spec_list (GEN_ALL (SIMP_RULE (bool_ss) [priv_LR_constraints_def] 628 wp_thm))) 629 THEN ASSUME_TAC (SPECL spec_list3 fixed_cpsr_thm) 630 THEN ASSUME_TAC (SPECL spec_list3 fixed_pc_thm2) 631 THEN RES_TAC 632 THEN FULL_SIMP_TAC (let_ss) [] 633 THEN FULL_SIMP_TAC (srw_ss()) [] 634 THEN RES_TAC 635 , 636 IMP_RES_TAC (SPEC r ( 637 INST_TYPE [beta |-> ``:unit``, 638 alpha |-> ltype ] 639 hlp_errorT_thm)) 640 THEN 641 PAT_X_ASSUM ``! (s:arm_state) . X `` 642 (fn thm => ASSUME_TAC (SPEC ``s:arm_state`` thm)) 643 THEN RW_TAC (srw_ss()) [] 644 THEN FULL_SIMP_TAC (srw_ss()) [] 645 ] 646 end; 647 648val take_undef_instr_exception_LR_thm = 649 store_thm ("take_undef_instr_exception_LR_thm", 650 `` ! mode. 651 satisfy_LR_constraints (take_undef_instr_exception <|proc:=0|> ) 652 mode (0w:word32)``, 653 let 654 val athm = SIMP_CONV (bool_ss) [take_undef_instr_exception_def] 655 ``take_undef_instr_exception <|proc:=0|>`` 656 val (_, te) = (dest_eq (concl athm)) 657 val te_def = take_undef_instr_exception_def 658 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 659 val spec_list = (mk_spec_list sl_elm2)@ 660 [``b:arm_state``, ``s':arm_state``,``a:unit``] 661 val spec_list2 = [``b:arm_state``] @ (mk_spec_list2 (sl_elm2)) 662 val spec_list3 = [``b:arm_state``] @ (rev (mk_spec_list2 (sl_elm2))) 663 val spec_lists = [spec_list]@[spec_list2]@[spec_list3] 664 val wp_thm = take_undef_writing_part_LR_thm 665 val fixed_rp_thm = fixed_undef_svc_exception_rp_thm2; 666 val fixed_cpsr_thm = fixed_cpsr_undef_svc_thm2 667 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm 668 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)`` 669 val fixed_pc_thm2 = fixed_pc_undef_svc_thm2 670 in 671 prove_take_exception_LR_constraints te te_def 672 take_undef_writing_part_LR_thm 673 fixed_rp_thm 674 fixed_cpsr_thm fixed_pc_thm2 675 const_comp_rp_thm 676 sl_elm2 spec_lists ltype 677 end); 678 679val take_svc_exception_LR_thm = 680 store_thm ("take_svc_exception_LR_thm", 681 let 682 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 683 ``take_svc_exception <|proc:=0|> ``; 684 val (_, a) = (dest_eq (concl athm)) 685 val (l,r,rb1)= decompose_term a 686 in 687 `` ! mode. satisfy_LR_constraints ^rb1 mode 0w`` 688 end 689, 690 let 691 val athm = SIMP_CONV (bool_ss) [take_svc_exception_def] 692 ``take_svc_exception <|proc:=0|> ``; 693 val (_, a) = (dest_eq (concl athm)) 694 val (l,r,te)= decompose_term a 695 val te_def = take_svc_exception_def 696 val sl_elm2 = ``(a':(word32 # word32 # ARMpsr # CP15scr # CP15sctlr))`` 697 val spec_list = (mk_spec_list sl_elm2)@ 698 [``b:arm_state``, ``s':arm_state``,``a:unit``] 699 val spec_list2 = [``b:arm_state``] @ (mk_spec_list2 (sl_elm2)) 700 val spec_list3 = [``b:arm_state``] @ (rev (mk_spec_list2 (sl_elm2))) 701 val spec_lists = [spec_list]@[spec_list2]@[spec_list3]; 702 val wp_thm = take_svc_writing_part_LR_thm 703 val fixed_rp_thm = fixed_undef_svc_exception_rp_thm2 704 val fixed_cpsr_thm = fixed_cpsr_undef_svc_thm2 705 val const_comp_rp_thm = const_comp_take_undef_svc_exception_rp_thm 706 val ltype = ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr)`` 707 val fixed_pc_thm2 = fixed_pc_undef_svc_thm2 708 in 709 prove_take_exception_LR_constraints te te_def 710 wp_thm 711 fixed_rp_thm 712 fixed_cpsr_thm fixed_pc_thm2 713 const_comp_rp_thm 714 sl_elm2 spec_lists ltype 715 end); 716 717 718 719val take_data_abort_exception_LR_thm = 720 store_thm ("take_data_abort_exception_LR_thm", 721 `` ! mode. satisfy_LR_constraints (take_data_abort_exception <|proc:=0|>) mode 2w `` 722 , 723 let 724 val athm = SIMP_CONV (bool_ss) [take_data_abort_exception_def] 725 ``take_data_abort_exception <|proc:=0|> ``; 726 val (_, te) = (dest_eq (concl athm)) 727 val te_def = take_data_abort_exception_def 728 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))``; 729 val spec_list = (mk_spec_list3 sl_elm2)@ 730 [``b:arm_state``, ``s':arm_state``,``a:unit``]; 731 val spec_list2 = [``b:arm_state``] @ (mk_spec_list4 (sl_elm2)) 732 val spec_list3 = [``b:arm_state``] @ (rev (mk_spec_list4 (sl_elm2))) 733 val spec_lists = [spec_list]@[spec_list2]@[spec_list3]; 734 val wp_thm = take_data_abort_writing_part_LR_thm 735 val fixed_rp_thm = fixed_abort_irq_exception_rp_thm2 736 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm2; 737 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` 738 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 739 val fixed_pc_thm2 = fixed_pc_abt_irq_thm2 740 in 741 prove_take_exception_LR_constraints te te_def 742 wp_thm 743 fixed_rp_thm 744 fixed_cpsr_thm 745 fixed_pc_thm2 746 const_comp_rp_thm 747 sl_elm2 spec_lists 748 ltype 749 end); 750 751 752val take_prefetch_abort_exception_LR_thm = 753 store_thm ("take_prefetch_abort_exception_LR_thm", 754 `` ! mode. satisfy_LR_constraints (take_prefetch_abort_exception <|proc:=0|>) mode 2w `` 755 , 756 let 757 val athm = SIMP_CONV (bool_ss) [take_prefetch_abort_exception_def] 758 ``take_prefetch_abort_exception <|proc:=0|> ``; 759 val (_, te) = (dest_eq (concl athm)) 760 val te_def = take_prefetch_abort_exception_def 761 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))``; 762 val spec_list = (mk_spec_list3 sl_elm2)@ 763 [``b:arm_state``, ``s':arm_state``,``a:unit``]; 764 val spec_list2 = [``b:arm_state``] @ (mk_spec_list4 (sl_elm2)) 765 val spec_list3 = [``b:arm_state``] @ (rev (mk_spec_list4 (sl_elm2))) 766 val spec_lists = [spec_list]@[spec_list2]@[spec_list3]; 767 val wp_thm = take_prefetch_abort_writing_part_LR_thm 768 val fixed_rp_thm = fixed_abort_irq_exception_rp_thm2 769 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm2; 770 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` 771 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 772 val fixed_pc_thm2 = fixed_pc_abt_irq_thm2 773 in 774 prove_take_exception_LR_constraints te te_def 775 wp_thm 776 fixed_rp_thm 777 fixed_cpsr_thm 778 fixed_pc_thm2 779 const_comp_rp_thm 780 sl_elm2 spec_lists 781 ltype 782 end); 783 784val take_irq_exception_LR_thm = 785 store_thm ("take_irq_exception_LR_thm", 786 `` ! mode. satisfy_LR_constraints (take_irq_exception <|proc:=0|>) mode 2w `` 787 , 788 let 789 val athm = SIMP_CONV (bool_ss) [take_irq_exception_def] 790 ``take_irq_exception <|proc:=0|> ``; 791 val (_, te) = (dest_eq (concl athm)) 792 val te_def = take_irq_exception_def 793 val sl_elm2 = ``(a':(word32 # word32 # bool# ARMpsr # CP15scr # CP15sctlr))``; 794 val spec_list = (mk_spec_list3 sl_elm2)@ 795 [``b:arm_state``, ``s':arm_state``,``a:unit``]; 796 val spec_list2 = [``b:arm_state``] @ (mk_spec_list4 (sl_elm2)) 797 val spec_list3 = [``b:arm_state``] @ (rev (mk_spec_list4 (sl_elm2))) 798 val spec_lists = [spec_list]@[spec_list2]@[spec_list3]; 799 val wp_thm = take_irq_writing_part_LR_thm 800 val fixed_rp_thm = fixed_abort_irq_exception_rp_thm2 801 val fixed_cpsr_thm = fixed_cpsr_abt_irq_thm2; 802 val ltype = ``:(word32 # word32 # bool # ARMpsr # CP15scr # CP15sctlr)`` 803 val const_comp_rp_thm = const_comp_take_abort_irq_exception_rp_thm 804 val fixed_pc_thm2 = fixed_pc_abt_irq_thm2 805 in 806 prove_take_exception_LR_constraints te te_def 807 wp_thm 808 fixed_rp_thm 809 fixed_cpsr_thm 810 fixed_pc_thm2 811 const_comp_rp_thm 812 sl_elm2 spec_lists 813 ltype 814 end); 815 816 817val _ = export_theory(); 818