1open HolKernel boolLib bossLib Parse proofManagerLib; 2open arm_opsemTheory arm_seq_monadTheory arm_coretypesTheory arm_stepTheory; 3open inference_rulesTheory tacticsLib ARM_prover_extLib; 4 5val _ = new_theory("switching_lemma_helper"); 6val _ = ParseExtras.temp_loose_equality() 7 8 9(****************************************************************) 10(* HELPING LEMMAS TO PROVE SWITCHING LEMMA *) 11(* Narges *) 12(****************************************************************) 13 14val get_security_ext_def = 15 Define `get_security_ext s = 16 (((ARMarch2num s.information.arch = 5) ��� 17 (ARMarch2num s.information.arch = 7)) ��� 18 Extension_Security ��� s.information.extensions)`; 19 20 21val vector_table_address_def = 22 Define ` vector_table_address (ExcVectorBase:bool[32]) (mode:bool[5]) = 23if (mode = 17w:bool[5]) 24then 25 [ExcVectorBase + 28w] 26else if (mode = 18w:bool[5]) 27then 28 [ExcVectorBase + 24w] 29else if (mode = 19w:bool[5]) 30then 31 [ExcVectorBase + 8w] 32else if (mode = 23w:bool[5]) 33then [ExcVectorBase + 16w; ExcVectorBase + 12w] 34else (*if (mode = 27w)*) 35 [ExcVectorBase + 4w] 36 `; 37 38val get_pc_value_def = 39Define `get_pc_value s1 = 40let is = (if (s1.psrs (0,CPSR)).J then 41 2 + if (s1.psrs (0,CPSR)).T then 1 else 0 42 else if (s1.psrs (0,CPSR)).T then 43 1 44 else 45 0) in 46(if InstrSet2num (if is MOD 4 = 47 0 48 then 49 InstrSet_ARM 50 else if is MOD 4 = 51 1 52 then 53 InstrSet_Thumb 54 else if is MOD 4 = 55 2 56 then 57 InstrSet_Jazelle 58 else if is MOD 4 = 59 3 60 then 61 InstrSet_ThumbEE 62 else 63 ARB) = 64 0 65 then 66 s1.registers (0,RName_PC) + 8w 67 else 68 (s1.registers (0,RName_PC) + 4w))`; 69 70(* 71val get_base_vector_table_def = 72 Define `get_base_vector_table y = 73 if (y.coprocessors.state.cp15.SCTLR.V) 74 then 75 0xFFFF0000w 76 else 77 if 78 (((ARMarch2num y.information.arch = 5) 79 ��� 80 (ARMarch2num y.information.arch = 7)) 81 ��� 82 Extension_Security ��� y.information.extensions) 83 then 84 (if 85 (��y.coprocessors.state.cp15.SCR.NS 86 ��� 87 ((y.psrs (0,CPSR)).M = 22w)) 88 then 89 y.coprocessors.state.cp15.VBAR.secure 90 else 91 y.coprocessors.state.cp15.VBAR.non_secure) 92 else 93 0w:word32`; 94*) 95val get_base_vector_table_def = 96 Define `get_base_vector_table y = 97 if (y.coprocessors.state.cp15.SCTLR.V) 98 then 99 0xFFFF0000w 100 else 101 if 102 (((ARMarch2num y.information.arch = 5) 103 ��� 104 (ARMarch2num y.information.arch = 7)) 105 ��� 106 Extension_Security ��� y.information.extensions) 107 then 108 (if 109 (��y.coprocessors.state.cp15.SCR.NS 110 ��� 111 ((y.psrs (0,CPSR)).M = 22w)) 112 then 113 y.coprocessors.state.cp15.VBAR 114 else 115 y.coprocessors.state.cp15.VBAR) 116 else 117 0w:word32`; 118 119 120fun define_pfc_goal a expr = 121 set_goal([], `` 122 (priv_flags_constraints ^a ^expr) ``); 123 124fun define_pfc_goal_abs a expr = 125 set_goal([], `` 126 (priv_flags_constraints_abs ^a ^expr) ``); 127 128 129val const_comp_def = Define `const_comp G = (!s s' x. ((G s = ValueState x s') ==> (s=s')))`; 130 131val read_reg_constlem = 132 store_thm( 133 "read_reg_constlem", 134 ``!n. const_comp (read_reg <|proc:=0|> n)``, 135 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 136 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 137 THEN FULL_SIMP_TAC (srw_ss()) [] 138 THEN UNDISCH_ALL_TAC 139 140 THEN RW_TAC (srw_ss()) []))); 141 142val read_sctlr_constlem = 143 store_thm( 144 "read_sctlr_constlem", 145 ``const_comp (read_sctlr <|proc:=0|> )``, 146 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 147 THEN EVAL_TAC 148 THEN (REPEAT (RW_TAC (srw_ss()) [] 149 THEN FULL_SIMP_TAC (srw_ss()) [] 150 THEN UNDISCH_ALL_TAC 151 THEN RW_TAC (srw_ss()) []))); 152 153 154val read_scr_constlem = 155 store_thm( 156 "read_scr_constlem", 157 ``const_comp (read_scr <|proc:=0|> )``, 158 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 159 THEN EVAL_TAC 160 THEN (REPEAT 161 (RW_TAC (srw_ss()) [] 162 THEN FULL_SIMP_TAC (srw_ss()) [] 163 THEN UNDISCH_ALL_TAC 164 THEN RW_TAC (srw_ss()) []))); 165 166val exc_vector_base_constlem = 167 store_thm( 168 "exc_vector_base_constlem", 169 ``const_comp (exc_vector_base <|proc:=0|> )``, 170 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 171 THEN EVAL_TAC 172 THEN RW_TAC (srw_ss()) [] 173 THEN NTAC 2 (UNDISCH_ALL_TAC 174 THEN RW_TAC (srw_ss()) [])); 175 176 177val read_cpsr_quintuple_par_effect_lem = store_thm( 178 "read_cpsr_quintuple_par_effect_lem", 179 ``!s A B C D H . (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 180 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, cpsr, d))) s) 181 = (((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, (s.psrs (0, CPSR)), d))) s))``, 182 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 183 THEN Cases_on `A s` 184 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 185 THEN Cases_on `B b` 186 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 187 THEN Cases_on `C b'` 188 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 189 THEN RES_TAC 190 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def] 191 THEN Cases_on `D b` 192 THEN RW_TAC (srw_ss()) []); 193 194val cpsr_quintuple_simp_lem = store_thm( 195 "cpsr_quintuple_simp_lem", 196 ``!s a n m H . (assert_mode 16w s) ==> 197 ((((read_reg <|proc:=0|> a ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (a, b, c, cpsr, d). H (a, b, c, cpsr, d))) s) 198 = (((read_reg <|proc:=0|> a ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (a, b, c, cpsr, d). H (a, b, c, ((s.psrs (0, CPSR)) with M := 16w), d))) s))``, 199 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_reg_constlem, read_cpsr_quintuple_par_effect_lem, ARM_READ_CPSR_def] 200 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with M:= 16w))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 201 THEN METIS_TAC []); 202 203 204val read_cpsr_quintuple_par_effect_with_16_lem = store_thm( 205 "read_cpsr_quintuple_par_effect_with_16_lem", 206 ``!s A B C D H . (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 207 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, (cpsr with M := 16w), d))) s) 208 = (((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, ((s.psrs (0, CPSR)) with M := 16w), d))) s))``, 209 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 210 THEN Cases_on `A s` 211 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 212 THEN Cases_on `B b` 213 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 214 THEN Cases_on `C b'` 215 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 216 THEN RES_TAC 217 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def] 218 THEN Cases_on `D b` 219 THEN RW_TAC (srw_ss()) []); 220 221 222val cpsr_quintuple_simp_rel_lem = store_thm( 223 "cpsr_quintuple_simp_rel_lem", 224 ``!a n m H inv2 uf uy. 225 (preserve_relation_mmu ((read_reg <|proc:=0|> a ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (pc, b, c, cpsr, d). H (pc, b, c, cpsr, d))) (assert_mode 16w) (inv2) uf uy) 226 = (preserve_relation_mmu ((read_reg <|proc:=0|> a ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (pc, b, c, cpsr, d). H (pc, b, c, (cpsr with M := 16w), d))) (assert_mode 16w) (inv2) uf uy)``, 227 RW_TAC (srw_ss()) [cpsr_quintuple_simp_lem, preserve_relation_mmu_def, read_reg_constlem, read_cpsr_quintuple_par_effect_with_16_lem]); 228 229 230val read_cpsr_quintuple_par_effect_lem2 = store_thm( 231 "read_cpsr_quintuple_par_effect_lem2", 232 ``!s A B D E H . (const_comp A) ==> (const_comp B) ==> 233 ((((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, cpsr, d, e))) s) 234 = (((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, (s.psrs (0, CPSR)), d, e))) s))``, 235 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 236 THEN Cases_on `A s` 237 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 238 THEN Cases_on `B b` 239 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 240 THEN RES_TAC 241 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def] 242 THEN Cases_on `D b` 243 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 244 THEN Cases_on `E b'` 245 THEN RW_TAC (srw_ss()) []); 246 247val read_cpsr_quintuple_par_effect_with_16_lem2 = store_thm( 248 "read_cpsr_quintuple_par_effect_with_16_lem2", 249 ``!s A B D E H . (const_comp A) ==> (const_comp B) ==> 250 ((((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, (cpsr with M := 16w), d, e))) s) 251 = (((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, ((s.psrs (0, CPSR)) with M := 16w), d, e))) s))``, 252 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 253 THEN Cases_on `A s` 254 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 255 THEN Cases_on `B b` 256 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 257 THEN RES_TAC 258 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def] 259 THEN Cases_on `D b` 260 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 261 THEN Cases_on `E b'` 262 THEN RW_TAC (srw_ss()) []); 263 264 265val cpsr_quintuple_simp_lem2 = store_thm( 266 "cpsr_quintuple_simp_lem2", 267 ``!s x H . (assert_mode 16w s) ==> 268 ((((read_reg <|proc:=0|> x ||| exc_vector_base <|proc:=0|> ||| read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= (\ (a, b, cpsr, d, e). H (a, b, cpsr, d, e))) s) 269 = (((read_reg <|proc:=0|> x ||| exc_vector_base <|proc:=0|> ||| read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= (\ (a, b, cpsr, d, e). H (a, b, ((s.psrs (0, CPSR)) with M := 16w), d, e))) s))``, 270 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_reg_constlem, exc_vector_base_constlem, read_cpsr_quintuple_par_effect_lem2, ARM_READ_CPSR_def] 271 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with M:= 16w))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 272 THEN METIS_TAC []); 273 274 275val cpsr_quintuple_simp_rel_lem2 = store_thm( 276 "cpsr_quintuple_simp_rel_lem2", 277 ``!x H inv2 uf uy. 278 (preserve_relation_mmu (((read_reg <|proc:=0|> x ||| exc_vector_base <|proc:=0|> ||| read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= (\ (pc, ExcVectorBase, cpsr, scr, sctlr). H (pc, ExcVectorBase, cpsr, scr, sctlr)))) (assert_mode 16w) (inv2) uf uy) 279 = (preserve_relation_mmu (((read_reg <|proc:=0|> x ||| exc_vector_base <|proc:=0|> ||| read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= (\ (pc, ExcVectorBase, cpsr, scr, sctlr). H (pc, ExcVectorBase, (cpsr with M := 16w), scr, sctlr))))(assert_mode 16w) (inv2) uf uy)``, 280 RW_TAC (srw_ss()) [cpsr_quintuple_simp_lem2, preserve_relation_mmu_def, read_reg_constlem, exc_vector_base_constlem, read_cpsr_quintuple_par_effect_with_16_lem2]); 281 282 283val read_cpsr_effect_lem = store_thm( 284 "read_cpsr_effect_lem", 285 ``!s H . ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) s = (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (s.psrs (0, CPSR)))) s)``, 286 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 287 THEN FULL_SIMP_TAC (srw_ss()) [] 288 THEN RES_TAC 289 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def]); 290 291 292val cpsr_simp_lem = store_thm( 293 "cpsr_simp_lem", 294 ``!s H u. (assert_mode u s) ==> 295 (((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) s) 296 = ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr with M := u))) s))``, 297 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_cpsr_effect_lem, ARM_READ_CPSR_def] 298 THEN `s.psrs (0,CPSR) = s.psrs (0,CPSR) with M := (s.psrs (0,CPSR)).M` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 299 THEN METIS_TAC []); 300 301val cpsr_simp_rel_lem = store_thm( 302 "cpsr_simp_rel_lem", 303 ``!H inv2 uf uy u. 304 (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) (assert_mode u) (inv2) uf uy) 305 = (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr with M := u)))(assert_mode u) (inv2) uf uy)``, 306 RW_TAC (srw_ss()) [preserve_relation_mmu_def] 307 THEN METIS_TAC [cpsr_simp_lem]); 308 309(* End of borrowed theorems *) 310 311val read_cpsr_constlem = 312 store_thm( 313 "read_cpsr_constlem", 314 ``const_comp (read_cpsr <|proc:=0|> )``, 315 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 316 THEN EVAL_TAC 317 THEN (REPEAT (RW_TAC (srw_ss()) [] 318 THEN FULL_SIMP_TAC (srw_ss()) [] 319 THEN UNDISCH_ALL_TAC 320 THEN RW_TAC (srw_ss()) []))); 321 322val parT_const_comp_thm = 323 store_thm( 324 "parT_const_comp_thm", 325 ``! f h. const_comp f ==> 326 const_comp h ==> 327 const_comp (f ||| h)`` 328 , 329 RW_TAC (srw_ss()) [parT_def,seqT_def,const_comp_def,constT_def] THEN 330 Cases_on ` f s ` THEN 331 RES_TAC THEN 332 FULL_SIMP_TAC (srw_ss()) [] THEN 333 Cases_on ` h b ` THEN 334 RES_TAC THEN 335 FULL_SIMP_TAC (srw_ss()) [] THEN 336 RW_TAC (srw_ss()) [] THEN 337 Cases_on ` access_violation b` THEN 338 FULL_SIMP_TAC (srw_ss()) []); 339 340 341val fixed_sctrl_undef_svc_thm1 = 342 store_thm( 343 "fixed_sctrl_undef_svc_thm1", 344 ``!s A B C D H . 345 (const_comp A) ==> 346 (const_comp B) ==> 347 (const_comp C) ==> 348 (const_comp D) ==> 349 ((((A ||| B ||| C ||| D 350 ||| read_sctlr <|proc:=0|>) >>= 351 (\ (a, b, c, d, e). H (a, b, c, d, e))) s) 352 = (((A ||| B ||| C ||| D ||| 353 read_sctlr <|proc:=0|>) >>= 354 (\ (a, b, c, d, e). H (a, b, c, d, s.coprocessors.state.cp15.SCTLR))) s)) 355``, 356 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 357 THEN Cases_on `A s` 358 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 359 THEN RES_TAC 360 THEN Cases_on `B s` 361 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 362 THEN RES_TAC 363 THEN Cases_on `C s` 364 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 365 THEN RES_TAC 366 THEN Cases_on `D s` 367 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 368 THEN RES_TAC 369 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,arm_seq_monadTheory.readT_def] 370 THEN RW_TAC (srw_ss()) [] 371 ); 372 373val fixed_cpsr_undef_svc_thm1 = 374 store_thm( 375 "fixed_cpsr_undef_svc_thm1", 376 ``!s A B C D H . 377 (const_comp A) ==> 378 (const_comp B) ==> 379 ((((A ||| B ||| read_cpsr <|proc := 0|> ||| C ||| D) >>= 380 (\ (a, b, c, d, e). H (a, b, c, d, e))) s) 381 = (((A ||| B ||| read_cpsr <|proc := 0|> ||| C ||| D) >>= 382 (\ (a, b, c, d, e). H (a, b, s.psrs (0,CPSR), d, e))) s)) 383``, 384 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 385 THEN Cases_on `A s` 386 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 387 THEN RES_TAC 388 THEN Cases_on `B s` 389 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 390 THEN RES_TAC 391 THEN FULL_SIMP_TAC (srw_ss()) [read_cpsr_def,read__psr_def,arm_seq_monadTheory.readT_def] 392 THEN RW_TAC (srw_ss()) [] 393 THEN Cases_on `C b` 394 THEN Cases_on ` access_violation b'` 395 THEN FULL_SIMP_TAC (srw_ss()) [] 396 THEN Cases_on `D b'` 397 THEN Cases_on ` access_violation b''` 398 THEN FULL_SIMP_TAC (srw_ss()) [] 399 400 ); 401 402val fixed_sctrl_abt_irq_thm1 = 403 store_thm( 404 "fixed_sctrl_abt_irq_thm1", 405 ``!s A B C D E H . 406 (const_comp A) ==> 407 (const_comp B) ==> 408 (const_comp C) ==> 409 (const_comp D) ==> 410 (const_comp E) ==> 411 ((((A ||| B ||| C ||| D ||| E 412 ||| read_sctlr <|proc:=0|>) >>= 413 (\ (a, b, c, d, e,f). H (a, b, c, d, e,f))) s) 414 = (((A ||| B ||| C ||| D ||| E ||| 415 read_sctlr <|proc:=0|>) >>= 416 (\ (a, b, c, d, e,f). H (a, b, c, d, e, s.coprocessors.state.cp15.SCTLR))) s)) 417``, 418 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 419 THEN Cases_on `A s` 420 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 421 THEN RES_TAC 422 THEN Cases_on `B s` 423 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 424 THEN RES_TAC 425 THEN Cases_on `C s` 426 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 427 THEN RES_TAC 428 THEN Cases_on `D s` 429 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 430 THEN RES_TAC 431 THEN Cases_on `E s` 432 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 433 THEN RES_TAC 434 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,arm_seq_monadTheory.readT_def] 435 THEN RW_TAC (srw_ss()) [] 436 ); 437 438 439val fixed_undef_svc_exception_rp_thm2 = store_thm( 440 "fixed_undef_svc_exception_rp_thm2", 441 ``!s e d c b a. 442 (~access_violation s) ==> 443 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 444 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 445 read_sctlr <|proc:=0|>) s) 446 = ValueState (a, b, c, d, e) s) ==> 447 ((a = get_pc_value s) 448 /\ 449 (b=get_base_vector_table s) 450 /\ 451 (c=s.psrs (0,CPSR )) 452 /\ 453 (d=s.coprocessors.state.cp15.SCR) 454 /\ 455 (e=s.coprocessors.state.cp15.SCTLR))``, 456 EVAL_TAC 457 THEN RW_TAC (srw_ss()) [] 458 ); 459 460 461val fixed_abort_irq_exception_rp_thm2 = store_thm( 462 "fixed_abort_irq_exception_rp_thm2", 463 ``!s f e d c b a . 464 (~access_violation s) ==> 465 (* (Extension_Security ��� s.information.extensions) ==> *) 466 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| have_security_ext <|proc:=0|> 467 ||| read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 468 = (ValueState (a, b, c, d, e, f) s)) ==> 469 ((a = get_pc_value s) 470 /\ 471 (b=get_base_vector_table s) 472 /\ 473 (c = (((ARMarch2num s.information.arch = 5) ��� 474 (ARMarch2num s.information.arch = 7)) ��� 475 Extension_Security ��� s.information.extensions)) 476 /\ 477 (d=s.psrs (0,CPSR )) 478 /\ 479 (e=s.coprocessors.state.cp15.SCR) 480 /\ 481 (f=s.coprocessors.state.cp15.SCTLR))``, 482 EVAL_TAC 483 THEN RW_TAC (srw_ss()) []); 484 485val have_security_ext_constlem = 486 store_thm( 487 "have_security_ext_constlem", 488 ``const_comp (have_security_ext <|proc := 0|>)``, 489 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 490 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 491 THEN FULL_SIMP_TAC (srw_ss()) [] 492 THEN UNDISCH_ALL_TAC 493 494 THEN RW_TAC (srw_ss()) []))); 495 496val const_comp_take_undef_svc_exception_rp_thm = 497 store_thm( 498 "const_comp_take_undef_svc_exception_rp_thm", 499 ``const_comp (read_reg <|proc := 0|> 15w 500 ||| exc_vector_base <|proc := 0|> 501 ||| read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 502 ||| read_sctlr <|proc := 0|>)``, 503 ASSUME_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) 504 THEN ASSUME_TAC read_cpsr_constlem 505 THEN ASSUME_TAC exc_vector_base_constlem 506 THEN ASSUME_TAC read_scr_constlem 507 THEN ASSUME_TAC read_sctlr_constlem 508 THEN 509 `const_comp (read_scr <|proc := 0|> 510 ||| read_sctlr <|proc := 0|>)` by 511 IMP_RES_TAC parT_const_comp_thm 512 THEN 513 `const_comp ( read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 514 ||| read_sctlr <|proc := 0|>)` by 515 IMP_RES_TAC parT_const_comp_thm 516 THEN 517 `const_comp (exc_vector_base <|proc := 0|> 518 ||| read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 519 ||| read_sctlr <|proc := 0|>)` by 520 IMP_RES_TAC parT_const_comp_thm 521 THEN 522 `const_comp (read_reg <|proc := 0|> 15w 523 ||| exc_vector_base <|proc := 0|> 524 ||| read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 525 ||| read_sctlr <|proc := 0|>)` 526 by IMP_RES_TAC parT_const_comp_thm); 527 528 529 530 531val const_comp_take_abort_irq_exception_rp_thm = 532 store_thm( 533 "const_comp_take_abort_irq_exception_rp_thm", 534 ``const_comp (read_reg <|proc := 0|> 15w ||| exc_vector_base <|proc := 0|> 535 ||| have_security_ext <|proc := 0|> 536 ||| read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 537 ||| read_sctlr <|proc := 0|>)``, 538 ASSUME_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) 539 THEN ASSUME_TAC read_cpsr_constlem 540 THEN ASSUME_TAC exc_vector_base_constlem 541 THEN ASSUME_TAC read_scr_constlem 542 THEN ASSUME_TAC have_security_ext_constlem 543 THEN ASSUME_TAC read_sctlr_constlem 544 THEN 545 `const_comp (read_scr <|proc := 0|> 546 ||| read_sctlr <|proc := 0|>)` by 547 IMP_RES_TAC parT_const_comp_thm 548 THEN 549 `const_comp ( read_cpsr <|proc := 0|> ||| read_scr <|proc := 0|> 550 ||| read_sctlr <|proc := 0|>)` by 551 IMP_RES_TAC parT_const_comp_thm 552 THEN 553 `const_comp (have_security_ext <|proc := 0|> ||| read_cpsr <|proc := 0|> 554 ||| read_scr <|proc := 0|> ||| read_sctlr <|proc := 0|>)` by 555 IMP_RES_TAC parT_const_comp_thm 556 THEN 557 `const_comp (exc_vector_base <|proc := 0|> 558 ||| have_security_ext <|proc := 0|> ||| 559 read_cpsr <|proc := 0|> 560 ||| read_scr <|proc := 0|> ||| read_sctlr <|proc := 0|>)` 561 by IMP_RES_TAC parT_const_comp_thm 562 THEN METIS_TAC [parT_const_comp_thm]); 563 564 565 566 567val fixed_undef_svc_exception_rp_thm3 = store_thm( 568 "fixed_undef_svc_exception_rp_thm3", 569 ``!s H. 570 ((s.psrs (0,CPSR)).M = 16w:bool[5] ) ==> 571 (~access_violation s) ==> 572 ((((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 573 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 574 read_sctlr <|proc:=0|>) >>= 575 (\ (a, b, c, d, e). (H: 576 (bool[32]#bool[32]#ARMpsr#CP15scr#CP15sctlr -> unit M)) (a, b, c, d, e))) s) 577 = (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 578 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 579 read_sctlr <|proc:=0|>) >>= 580 (\ (a, b, c, d, e). H ( 581 get_pc_value s, 582 get_base_vector_table s, 583 s.psrs (0,CPSR ) with M := 16w , 584 s.coprocessors.state.cp15.SCR, 585 s.coprocessors.state.cp15.SCTLR))) s))``, 586 EVAL_TAC 587 THEN RW_TAC (srw_ss()) [] 588 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with M:= 16w))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 589 THEN METIS_TAC [] 590 ); 591 592 593val fixed_abt_irq_exception_rp_thm3 = store_thm( 594 "fixed_abt_irq_exception_rp_thm3", 595 ``!s H. 596 ((s.psrs (0,CPSR)).M = 16w:bool[5] ) ==> 597 (~access_violation s) ==> 598 ((((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| have_security_ext <|proc := 0|> ||| 599 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 600 read_sctlr <|proc:=0|>) >>= 601 (\ (a, b, c, d, e,f). (H: 602 (bool[32]#bool[32]#bool#ARMpsr#CP15scr#CP15sctlr -> unit M)) (a, b, c, d, e,f))) s) 603 = (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| have_security_ext <|proc := 0|> ||| 604 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 605 read_sctlr <|proc:=0|>) >>= 606 (\ (a, b, c, d, e,f). H ( 607 get_pc_value s, 608 get_base_vector_table s, 609 get_security_ext s, 610 s.psrs (0,CPSR ) with M := 16w , 611 s.coprocessors.state.cp15.SCR, 612 s.coprocessors.state.cp15.SCTLR))) s))``, 613 EVAL_TAC 614 THEN RW_TAC (srw_ss()) [] 615 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with M:= 16w))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 616 THEN METIS_TAC [] 617 ); 618 619 620 621val fixed_VectorBase_undef_instr_exception_thm1 = store_thm( 622 "fixed_VectorBase_undef_instr_exception_thm1", 623 ``! e d c b a s. 624 (~access_violation s) ==> 625 (* (Extension_Security ��� s.information.extensions) ==> *) 626 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 627 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 628 read_sctlr <|proc:=0|>) s) 629 = ValueState (a, b, c, d, e) s) ==> 630 (b=get_base_vector_table s)``, 631 EVAL_TAC 632 THEN RW_TAC (srw_ss()) [] 633 ); 634 635val fixed_VectorBase_undef_instr_exception_thm2 = store_thm( 636 "fixed_VectorBase_undef_instr_exception_thm2", 637 ``!s H. 638 (~access_violation s) ==> 639 ((((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 640 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 641 read_sctlr <|proc:=0|>) >>= 642 (\ (a, b, c, d, e). (H: 643 (bool[32]#bool[32]#ARMpsr#CP15scr#CP15sctlr -> unit M)) (a, b, c, d, e))) s) 644 = (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 645 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 646 read_sctlr <|proc:=0|>) >>= 647 (\ (a, b, c, d, e). H ( 648 a , (get_base_vector_table s) 649 , 650 c, 651 d, 652 e))) s))``, 653 EVAL_TAC 654 THEN RW_TAC (srw_ss()) [] 655 656 ); 657 658val fixed_VectorBase_abort_irq_exception_thm1 = store_thm( 659 "fixed_VectorBase_abort_irq_exception_thm1", 660 ``! f e d c b a s. 661 (~access_violation s) ==> 662 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 663 have_security_ext <|proc:=0|> ||| 664 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 665 read_sctlr <|proc:=0|>) s) 666 = ValueState (a, b, c, d, e,f) s) ==> 667 (b=get_base_vector_table s 668 )``, 669 EVAL_TAC 670 THEN RW_TAC (srw_ss()) [] 671 ); 672 673val fixed_VectorBase_abort_irq_exception_thm2 = store_thm( 674 "fixed_VectorBase_abort_irq_exception_thm2", 675 ``!s H. 676 (~access_violation s) ==> 677 ((((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 678 have_security_ext <|proc:=0|> ||| 679 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 680 read_sctlr <|proc:=0|>) >>= 681 (\ (a, b, c, d, e,f). (H: 682 (bool[32]#bool[32]#bool#ARMpsr#CP15scr#CP15sctlr -> unit M)) (a, b, c, d, e,f))) s) 683 = (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 684 have_security_ext <|proc:=0|> ||| 685 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 686 read_sctlr <|proc:=0|>) >>= 687 (\ (a, b, c, d, e,f). H ( 688 a ,(get_base_vector_table s) 689 , 690 c, 691 d, 692 e, f))) s))``, 693 EVAL_TAC 694 THEN RW_TAC (srw_ss()) [] 695 696 ); 697 698 699val fixed_sctrl_undef_svc_thm2 = 700 store_thm( 701 "fixed_sctrl_undef_svc_thm2", 702 ``!s e d c b a. 703 (~access_violation s) ==> 704 (((read_reg <|proc:=0|> 15w ||| 705 exc_vector_base <|proc:=0|> ||| 706 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 707 = ValueState (a, b, c, d, e) s) ==> 708 (e = s.coprocessors.state.cp15.SCTLR) ``, 709 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] THEN 710 ASSUME_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) THEN 711 ASSUME_TAC exc_vector_base_constlem THEN 712 ASSUME_TAC read_cpsr_constlem THEN 713 ASSUME_TAC read_scr_constlem 714 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 715 THEN Cases_on `read_reg <|proc:=0|> 15w s` 716 THEN FULL_SIMP_TAC (srw_ss()) [] 717 THEN RES_TAC 718 THEN RW_TAC (srw_ss()) [] 719 THEN Cases_on `exc_vector_base <|proc:=0|> b'` 720 THEN RW_TAC (srw_ss()) [const_comp_def] 721 THEN RES_TAC 722 THEN Cases_on `read_cpsr <|proc:=0|> b'` 723 THEN RW_TAC (srw_ss()) [const_comp_def] 724 THEN RES_TAC 725 THEN Cases_on `read_scr <|proc:=0|> b'` 726 THEN RW_TAC (srw_ss()) [const_comp_def] 727 THEN RES_TAC 728 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,readT_def] 729 THEN RW_TAC (srw_ss()) [] 730 THEN Cases_on `access_violation b'` 731 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,readT_def] 732 THEN RW_TAC (srw_ss()) []); 733 734 735 736val fixed_sctrl_abt_irq_thm2 = 737 store_thm( 738 "fixed_sctrl_abt_irq_thm2", 739 ``!s f e d c b a. 740 (~access_violation s) ==> 741 (((read_reg <|proc:=0|> 15w ||| 742 exc_vector_base <|proc:=0|> 743 ||| have_security_ext <|proc:=0|> ||| 744 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 745 = ValueState (a, b, c, d, e,f) s) ==> 746 (f = s.coprocessors.state.cp15.SCTLR) ``, 747 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] THEN 748 ASSUME_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) THEN 749 ASSUME_TAC exc_vector_base_constlem THEN 750 ASSUME_TAC read_cpsr_constlem THEN 751 ASSUME_TAC read_scr_constlem THEN 752 ASSUME_TAC have_security_ext_constlem 753 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 754 THEN Cases_on `read_reg <|proc:=0|> 15w s` 755 THEN FULL_SIMP_TAC (srw_ss()) [] 756 THEN RES_TAC 757 THEN RW_TAC (srw_ss()) [] 758 THEN Cases_on `exc_vector_base <|proc:=0|> b'` 759 THEN RW_TAC (srw_ss()) [const_comp_def] 760 THEN RES_TAC 761 THEN Cases_on `read_cpsr <|proc:=0|> b'` 762 THEN RW_TAC (srw_ss()) [const_comp_def] 763 THEN RES_TAC 764 THEN Cases_on `read_scr <|proc:=0|> b'` 765 THEN RW_TAC (srw_ss()) [const_comp_def] 766 THEN RES_TAC 767 THEN Cases_on `have_security_ext <|proc:=0|> b'` 768 THEN RW_TAC (srw_ss()) [const_comp_def] 769 THEN RES_TAC 770 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,readT_def] 771 THEN RW_TAC (srw_ss()) [] 772 THEN Cases_on `access_violation b'` 773 THEN FULL_SIMP_TAC (srw_ss()) [read_sctlr_def,readT_def] 774 THEN RW_TAC (srw_ss()) []); 775 776 777 778val fixed_sctrl_undef_svc_thm = store_thm( 779 "fixed_sctrl_undef_svc_thm", 780 ``!s H . 781 ((((read_reg <|proc:=0|> 15w ||| 782 exc_vector_base <|proc:=0|> ||| 783 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 784 read_sctlr <|proc:=0|>) >>= (\ (pc,ExcVectorBase,cpsr,scr,sctlr). H (pc,ExcVectorBase,cpsr,scr,sctlr))) s) 785 = 786 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 787 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= 788 (\(pc,ExcVectorBase,cpsr,scr,sctlr). H (pc,ExcVectorBase,cpsr,scr, s.coprocessors.state.cp15.SCTLR))) s))``, 789 MP_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) 790 THEN MP_TAC read_cpsr_constlem 791 THEN MP_TAC exc_vector_base_constlem 792 THEN MP_TAC read_scr_constlem 793 THEN RW_TAC (srw_ss()) [fixed_sctrl_undef_svc_thm1] 794 ); 795 796val fixed_cpsr_undef_svc_thm = 797 store_thm ("fixed_cpsr_undef_svc_thm", 798 ``!s H . 799 ((((read_reg <|proc:=0|> 15w ||| 800 exc_vector_base <|proc:=0|> ||| 801 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 802 read_sctlr <|proc:=0|>) >>= 803 (\ (pc,ExcVectorBase,cpsr,scr,sctlr). H (pc,ExcVectorBase,cpsr,scr,sctlr))) s) 804 = (((read_reg <|proc:=0|> 15w ||| 805 exc_vector_base <|proc:=0|> ||| 806 read_cpsr <|proc:=0|> ||| 807 read_scr <|proc:=0|> ||| 808 read_sctlr <|proc:=0|>) >>= 809 (\ (pc,ExcVectorBase,cpsr,scr,sctlr). H (pc,ExcVectorBase,s.psrs (0,CPSR),scr,sctlr))) s))``, 810 MP_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) 811 THEN MP_TAC read_cpsr_constlem 812 THEN MP_TAC exc_vector_base_constlem 813 THEN MP_TAC read_scr_constlem 814 THEN RW_TAC (srw_ss()) [fixed_cpsr_undef_svc_thm1] 815 ); 816 817 818val fixed_sctrl_abt_irq_thm = store_thm( 819 "fixed_sctrl_abt_irq_thm", 820 ``!s H . 821 ((((read_reg <|proc:=0|> 15w ||| 822 exc_vector_base <|proc:=0|> ||| 823 have_security_ext <|proc := 0|> ||| 824 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 825 read_sctlr <|proc:=0|>) >>= (\ (pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr). H (pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr))) s) 826 = 827 (((read_reg <|proc:=0|> 15w ||| exc_vector_base <|proc:=0|> ||| 828 have_security_ext <|proc := 0|> ||| 829 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) >>= 830 (\(pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr). H (pc,ExcVectorBase,have_security_ext1,cpsr,scr, s.coprocessors.state.cp15.SCTLR))) s))``, 831 MP_TAC (SPEC ``15w:bool[4]`` read_reg_constlem) 832 THEN MP_TAC read_cpsr_constlem 833 THEN MP_TAC exc_vector_base_constlem 834 THEN MP_TAC read_scr_constlem 835 THEN MP_TAC have_security_ext_constlem 836 THEN RW_TAC (srw_ss()) [fixed_sctrl_abt_irq_thm1] 837 ); 838 839val read_cpsr_quintuple_par_effect_lem1 = store_thm( 840 "read_cpsr_quintuple_par_effect_lem1", 841 ``!s A B C D H . (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 842 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, c, cpsr, d,e). H (a, b, c, cpsr, d,e))) s) 843 = (((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, c, cpsr, d,e). H (a, b, c, (s.psrs (0, CPSR)), d,e))) s))``, 844 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 845 THEN Cases_on `A s` 846 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 847 THEN Cases_on `B b` 848 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 849 THEN Cases_on `C b'` 850 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 851 THEN RES_TAC 852 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, arm_seq_monadTheory.readT_def] 853 THEN Cases_on `D b` 854 THEN RW_TAC (srw_ss()) [] 855 THEN Cases_on `E b'` 856 THEN RW_TAC (srw_ss()) [] 857); 858 859 860val fixed_cpsr_abt_irq_thm = store_thm( 861 "fixed_cpsr_abt_irq_thm", 862 ``!s H . 863 ((((read_reg <|proc:=0|> 15w ||| 864 exc_vector_base <|proc:=0|> ||| 865 have_security_ext <|proc := 0|> ||| 866 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| 867 read_sctlr <|proc:=0|>) >>= 868 (\ (pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr). 869 H (pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr))) s) 870 = (((read_reg <|proc:=0|> 15w ||| 871 exc_vector_base <|proc:=0|> ||| 872 have_security_ext <|proc := 0|> ||| 873 read_cpsr <|proc:=0|> ||| 874 read_scr <|proc:=0|> ||| 875 read_sctlr <|proc:=0|>) >>= 876 (\ (pc,ExcVectorBase,have_security_ext1,cpsr,scr,sctlr). 877 H (pc,ExcVectorBase,have_security_ext1,s.psrs (0,CPSR),scr,sctlr))) s))``, 878RW_TAC (srw_ss()) [read_reg_constlem, exc_vector_base_constlem, have_security_ext_constlem, read_cpsr_quintuple_par_effect_lem1, ARM_READ_CPSR_def] 879); 880 881 882val fixed_cpsr_undef_svc_thm2 = 883 store_thm("fixed_cpsr_undef_svc_thm2", 884 ``!s a b c d e. 885 (~access_violation s) ==> 886 (((read_reg <|proc:=0|> 15w ||| 887 exc_vector_base <|proc:=0|> ||| 888 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 889 = ValueState (a, b, c, d, e) s) ==> 890 (c = s.psrs (0,CPSR)) ``, 891RW_TAC (srw_ss()) [fixed_undef_svc_exception_rp_thm2]); 892 893 894val fixed_cpsr_abt_irq_thm2 = 895 store_thm("fixed_cpsr_abt_irq_thm2", 896 ``!s a b c d e f. 897 (~access_violation s) ==> 898 (((read_reg <|proc := 0|> 15w ||| exc_vector_base <|proc := 0|> 899 ||| have_security_ext <|proc := 0|> ||| read_cpsr <|proc := 0|> 900 ||| read_scr <|proc := 0|> ||| read_sctlr <|proc := 0|>) s) 901 = ValueState (a, b, c, d, e ,f) s) ==> 902 (d = s.psrs (0,CPSR)) `` 903, 904RW_TAC (srw_ss()) [fixed_abort_irq_exception_rp_thm2]); 905 906 907val fixed_pc_undef_svc_thm2 = 908 store_thm("fixed_pc_undef_svc_thm2", 909 ``!s a b c d e. 910 (~access_violation s) ==> 911 (((read_reg <|proc:=0|> 15w ||| 912 exc_vector_base <|proc:=0|> ||| 913 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 914 = ValueState (a, b, c, d, e) s) ==> 915 (a = get_pc_value s)``, 916RW_TAC (srw_ss()) [fixed_undef_svc_exception_rp_thm2]); 917 918val fixed_pc_abt_irq_thm2 = 919 store_thm("fixed_pc_abt_irq_thm2", 920 ``!s a b c d e f. 921 (~access_violation s) ==> 922 (((read_reg <|proc:=0|> 15w ||| 923 exc_vector_base <|proc:=0|> 924||| have_security_ext <|proc := 0|> ||| 925 read_cpsr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_sctlr <|proc:=0|>) s) 926 = ValueState (a, b, c, d, e,f) s) ==> 927 (a = get_pc_value s)`` 928, 929RW_TAC (srw_ss()) [fixed_abort_irq_exception_rp_thm2]); 930 931 932(******************************************************) 933(*******************GENERAL THEOREMS ******************) 934(******************************************************) 935 936val hlp_seqT_thm = 937store_thm ("hlp_seqT_thm", 938 ``!f g s a s' a'. ((f >>= g) s = ValueState a s') ��� 939 (f s = ValueState a' s) ��� 940 ��access_violation s ��� 941 (g a' s = ValueState a s')``, 942 RW_TAC (srw_ss()) [seqT_def] 943 THEN FULL_SIMP_TAC (srw_ss()) [] 944 ); 945 946val hlp_errorT_thm = 947store_thm ("hlp_errorT_thm", 948 ``! g f s e. 949 (f s = Error e) ��� 950 ((f >>= g) s = Error e)``, 951 RW_TAC (srw_ss()) [seqT_def] 952 THEN FULL_SIMP_TAC (srw_ss()) [] 953 ); 954 955val seqT_access_violation_thm = 956store_thm ("seqT_access_violation_thm", 957 ``! g f s a s' s'' a'. 958 ((g >>= f) s = ValueState a s') ��� 959 (g s = ValueState a' s'') ==> 960 ��access_violation s' ��� 961 (��access_violation s'')``, 962 RW_TAC (srw_ss()) [seqT_def] 963 THEN FULL_SIMP_TAC (srw_ss()) [] 964 THEN Cases_on `access_violation s''` 965 THEN UNDISCH_ALL_TAC 966 THEN RW_TAC (srw_ss()) [seqT_def] 967 THEN FULL_SIMP_TAC (srw_ss()) [] 968 ); 969 970val parT_access_violation_thm = 971store_thm ("parT_access_violation_thm", 972 ``! g f s a s' s'' a'. 973 ((g ||| f) s = ValueState a s') ��� 974 (g s = ValueState a' s'') ==> 975 ��access_violation s' ��� 976 (��access_violation s'') 977 ``, 978 RW_TAC (srw_ss()) [seqT_def,parT_def,constT_def] 979 THEN FULL_SIMP_TAC (srw_ss()) [] 980 THEN Cases_on `access_violation s''` 981 THEN UNDISCH_ALL_TAC 982 THEN RW_TAC (srw_ss()) [seqT_def] 983 THEN FULL_SIMP_TAC (srw_ss()) [] 984 ); 985 986 987val const_comp_hlp_thm = 988 store_thm("const_comp_hlp_thm", 989``! f s s' a g. 990 (const_comp f) ==> 991 (f s = ValueState a s') ==> 992 (~access_violation s) ==> 993((f >>= g) s = g a s)`` 994 , 995 RW_TAC (srw_ss()) [const_comp_def,seqT_def] 996THEN RES_TAC 997THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def,seqT_def] 998); 999 1000val hlp_seqT2_thm = 1001 store_thm ("hlp_seqT2_thm", 1002 ``!f g s a s' b s1 e. ((f >>= g) s = ValueState a s') ==> 1003 ((f s = ValueState b s1) ==> 1004 (~access_violation s1) ==> 1005 (g b s1 = ValueState a s')) 1006 /\ ~(f s = Error e) 1007``, 1008RW_TAC (srw_ss()) [seqT_def] 1009THEN Cases_on `f s` 1010THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 1011); 1012 1013val hlp_seqT3_thm = 1014 store_thm ("hlp_seqT3_thm", 1015 ``!g f s e. 1016 (f s = Error e) ==> 1017 ((f >>= g) s = Error e) 1018``, 1019RW_TAC (srw_ss()) [seqT_def] 1020); 1021 1022 1023val hlp_seqT4_thm = 1024 store_thm ("hlp_seqT4_thm", 1025 ``!f H s1 s2 s1' s2' a1 g invr1 invr2 uf uy. 1026 (~access_violation s1') ==> 1027 (~access_violation s2') ==> 1028 (f s1 = ValueState a1 s1') ==> 1029 (f s2 = ValueState a1 s2') ==> 1030 (preserve_relation_mmu_abs H invr1 invr2 uf uy) ==> 1031 (mmu_requirements s1' g) ��� 1032 (mmu_requirements s2' g) ��� 1033 (similar g s1' s2') ��� 1034 (uy g s1' s2' )��� 1035 (invr1 s1' )��� 1036 (invr1 s2' )��� 1037 ((?a s1'' s2''. ((f >>= H) s1 = ValueState a s1'') 1038 /\ 1039 ((f >>= H) s2 = ValueState a s2'')) 1040 \/ 1041 (?e .((f >>= H) s1 = Error e) 1042 /\ 1043 ((f >>= H) s2 = Error e))) 1044 1045 ``, 1046 RW_TAC (srw_ss()) [preserve_relation_mmu_abs_def,seqT_def] 1047 THEN RES_TAC 1048 THEN PAT_X_ASSUM ``!c. X`` (fn thm => ASSUME_TAC (SPEC ``a1:'a`` thm)) 1049 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 1050 ); 1051 1052val similar_states_have_same_pc_thm = 1053 store_thm ("similar_states_have_same_pc_thm", 1054 ``! s1 s2 g. 1055 similar g s1 s2 ==> 1056 (s2.registers (0,RName_PC)= 1057 s1.registers (0,RName_PC))``, 1058 RW_TAC (srw_ss()) [similar_def,equal_user_register_def] 1059 ); 1060 1061val similar_states_have_same_cpsr_thm = 1062 store_thm ("similar_states_have_same_cpsr_thm", 1063 ``! s1 s2 g. 1064 similar g s1 s2 ==> 1065 (s2.psrs (0,CPSR)= 1066 s1.psrs (0,CPSR))``, 1067 RW_TAC (srw_ss()) [similar_def,equal_user_register_def] 1068 ); 1069val similar_states_have_same_mode_thm = 1070 store_thm ("similar_states_have_same_mode_thm", 1071 ``! u s1 s2 g. 1072 similar g s1 s2 ==> 1073 ((s2.psrs (0,CPSR)).M = u) ��� 1074 ((s1.psrs (0,CPSR)).M = u)``, 1075 RW_TAC (srw_ss()) [similar_def] 1076 ); 1077 1078val similar_states_have_same_av_thm1 = 1079 store_thm ("similar_states_have_same_av_thm1", 1080 ``! s1 s2 g. 1081 similar g s1 s2 ==> 1082 ( 1083 ((~access_violation s2) ==> 1084 (~access_violation s1)) 1085 /\ 1086 ((~access_violation s1) ==> 1087 (~access_violation s2))) 1088 ``, 1089 RW_TAC (srw_ss()) [similar_def] 1090 ); 1091 1092val similar_states_have_same_vec_tab_thm = 1093 store_thm ("similar_states_have_same_vec_tab_thm", 1094 ``! s1 s2 g. 1095 similar g s1 s2 ==> 1096 ( 1097 get_base_vector_table s1 = 1098 get_base_vector_table s2) 1099 ``, 1100 RW_TAC (srw_ss()) [similar_def, get_base_vector_table_def] 1101 ); 1102 1103 1104val similar_states_have_same_security_ext_thm = 1105 store_thm ("similar_states_have_same_security_ext_thm", 1106 ``! s1 s2 g. 1107 similar g s1 s2 ==> 1108 ( 1109 get_security_ext s1 = 1110 get_security_ext s2) 1111 ``, 1112 RW_TAC (srw_ss()) [similar_def, get_security_ext_def] 1113 ); 1114 1115val similar_states_have_same_read_pc_thm = 1116 store_thm ("similar_states_have_same_read_pc_thm", 1117 ``! s1 s2 g. 1118 similar g s1 s2 ==> 1119 ( 1120 get_pc_value s1 = 1121 get_pc_value s2) 1122 ``, 1123 RW_TAC (srw_ss()) [similar_def, get_pc_value_def,equal_user_register_def] 1124 THEN UNABBREV_ALL_TAC 1125 THEN EVAL_TAC 1126 THEN RW_TAC (srw_ss()) [] 1127 ); 1128 1129val similar_states_have_same_av_thm2 = 1130 store_thm ("similar_states_have_same_av_thm2", 1131 ``! s1 s2 g. 1132 similar g s1 s2 ==> 1133 ( 1134 ((access_violation s2) ==> 1135 (access_violation s1)) 1136 /\ 1137 ((access_violation s1) ==> 1138 (access_violation s2)))``, 1139 RW_TAC (srw_ss()) [similar_def] 1140 ); 1141 1142val untouched_states_implies_mmu_setup_thm = 1143 store_thm ("untouched_states_implies_mmu_setup_thm", 1144 ``! s1 t g. 1145 untouched g s1 t ==> 1146 ((s1.coprocessors.state.cp15.C1 = 1147 t.coprocessors.state.cp15.C1) /\ 1148 (s1.coprocessors.state.cp15.C2 = 1149 t.coprocessors.state.cp15.C2) /\ 1150 (s1.coprocessors.state.cp15.C3 = 1151 t.coprocessors.state.cp15.C3))``, 1152 RW_TAC (srw_ss()) [untouched_def] 1153 ); 1154 1155 1156(* only for arm_next: no svc constraints *) 1157val priv_mode_constraints_v1_def = 1158 Define `priv_mode_constraints_v1 (g:bool[32]) (state0:arm_state) state1 = 1159(state1.coprocessors.state.cp15 = 1160 state0.coprocessors.state.cp15) 1161 1162/\ 1163(state1.information = 1164 state0.information) 1165 1166/\ 1167((state1.psrs (0, CPSR)).F = 1168 (state0.psrs (0, CPSR)).F) 1169 1170/\ 1171((ARM_MODE state0 <> 16w) ==> 1172(ARM_MODE state1 <> 16w)) 1173 1174/\ 1175((ARM_MODE state1 <> 16w) ==> 1176(ARM_MODE state0 = 16w)) 1177 1178/\ 1179((ARM_MODE state1 = 16w) ==> 1180((state1.psrs (0, CPSR)).I = 1181 (state0.psrs (0, CPSR)).I)) 1182 1183/\ 1184((ARM_MODE state1 <> 16w) ==> 1185 (let spsr = get_spsr_by_mode (ARM_MODE state1) 1186 in 1187 ((state1.psrs (0, CPSR)).I = T) 1188 1189/\ 1190 ((state1.psrs (0, CPSR)).J = F) 1191 1192/\ 1193 ((state1.psrs (0, CPSR)).IT = 0w) 1194 1195/\ 1196 ((state1.psrs (0, CPSR)).E = 1197 (state0.coprocessors.state.cp15.SCTLR.EE)) 1198 1199/\ 1200~ (ARM_MODE state1 = 22w) 1201 1202/\ 1203~ (ARM_MODE state1 = 17w) 1204 1205/\ 1206~ (ARM_MODE state1 = 31w) 1207 1208/\ 1209(* program point to the handler of exception/interrupt in the vector table*) 1210((state1.registers (0, RName_PC) = 1211 (HD (vector_table_address (get_base_vector_table state0) 1212 ((state1.psrs (0, CPSR)).M)))) 1213\/ 1214(state1.registers (0, RName_PC) = 1215 (HD (TL (vector_table_address (get_base_vector_table state0) 1216 ((state1.psrs (0, CPSR)).M)))))) 1217 1218/\ 1219(* in non-abort modes, we have no access violations *) 1220((* (ARM_MODE state1 <> 23w) ==> *) 1221~(access_violation state1)) /\ 1222((state1.psrs(0,spsr)).M = 16w) /\ 1223((state1.psrs(0,spsr)).I = (state0.psrs(0,CPSR)).I) 1224 /\ 1225((state1.psrs(0,spsr)).F = (state0.psrs(0,CPSR)).F))) 1226`; 1227 1228(* only for arm_next : svc based on pc of previous state *) 1229val priv_mode_constraints_v2_def = 1230 Define `priv_mode_constraints_v2 (g:bool[32]) (state0:arm_state) state1 = 1231priv_mode_constraints_v1 g state0 state1 1232/\ 1233(* in svc mode, the link register is equal to old PC minus offset *) 1234((ARM_MODE state1 = 19w) ==> 1235 ((state1.registers (0, RName_LRsvc) = 1236 (if (state0.psrs (0,CPSR)).T 1237 then 1238 get_pc_value(state0) -2w 1239 else 1240 get_pc_value(state0) -4w 1241 )) 1242 /\ ((state1.psrs(0,SPSR_svc)) = (state0.psrs(0,CPSR))))) 1243`; 1244 1245(* only for arm_next : svc based on pc of previous state *) 1246val priv_mode_constraints_v2a_def = 1247 Define `priv_mode_constraints_v2a (g:bool[32]) (state0:arm_state) state1 = 1248priv_mode_constraints_v1 g state0 state1 1249/\ 1250(* in svc mode, the link register is equal to old PC minus offset *) 1251((ARM_MODE state1 = 19w) ==> 1252 ((state1.registers (0, RName_LRsvc) = 1253 (if (state0.psrs (0,CPSR)).T 1254 then 1255 get_pc_value(state0) -2w 1256 else 1257 get_pc_value(state0) -4w 1258 )) 1259 /\ ((state1.psrs(0,SPSR_svc)) = 1260 if (((ARMarch2num state0.information.arch = 6) ��� 1261 version_number state0.information.arch ��� 7) /\ 1262 (((state0.psrs (0,CPSR)).IT = 0w) ��� (state0.psrs (0,CPSR)).T)) 1263 then 1264 (state0.psrs(0,CPSR) with IT := ITAdvance ((state0.psrs(0,CPSR)).IT)) 1265 else 1266 (state0.psrs(0,CPSR))))) 1267`; 1268 1269 1270(* svc based on the borders *) 1271val priv_mode_constraints_v3_def = 1272Define `priv_mode_constraints_v3 (g:bool[32]) (state0:arm_state) state1 = 1273 priv_mode_constraints_v2a g state0 state1 1274/\ ((ARM_MODE state1 = 19w) ==> 1275 ( 1276 ((g = guest1) ==> 1277 ((((state1.psrs (0,SPSR_svc)).T) ==> (((state1.registers (0, RName_LRsvc) -2w) >=+ guest1_min_adr) /\ ((state1.registers (0, RName_LRsvc) -2w) <=+ guest1_max_adr))) 1278 /\ ((((state1.psrs (0,SPSR_svc)).T = F) /\ ((state1.psrs (0,SPSR_svc)).J = F)) ==> (((state1.registers (0, RName_LRsvc) -4w) >=+ guest1_min_adr) /\ ((state1.registers (0, RName_LRsvc) -4w) <=+ guest1_max_adr))))) 1279 /\ 1280 ((g = guest2) ==> 1281 ((((state1.psrs (0,SPSR_svc)).T) ==> (((state1.registers (0, RName_LRsvc) -2w) >=+ guest2_min_adr) /\ ((state1.registers (0, RName_LRsvc) -2w) <=+ guest2_max_adr))) 1282 /\ ((((state1.psrs (0,SPSR_svc)).T = F) /\ ((state1.psrs (0,SPSR_svc)).J = F)) ==> (((state1.registers (0, RName_LRsvc) -4w) >=+ guest2_min_adr) /\ ((state1.registers (0, RName_LRsvc) -4w) <=+ guest2_max_adr))))) 1283 ))`; 1284 1285 1286(* svc based on accessible bytes *) 1287val priv_mode_constraints_v4_def = 1288 Define `priv_mode_constraints_v4 (g:bool[32]) (state0:arm_state) state1 = 1289 priv_mode_constraints_v2a g state0 state1 1290/\ ((ARM_MODE state1 = 19w) ==> 1291 ( 1292 (((state1.psrs (0,SPSR_svc)).T) ==> aligned_word_readable state1 T (state1.registers (0, RName_LRsvc) -2w)) 1293 /\ ((((state1.psrs (0,SPSR_svc)).T = F) /\ ((state1.psrs (0,SPSR_svc)).J = F)) ==> aligned_word_readable state1 F (state1.registers (0, RName_LRsvc) -4w)) 1294 ))`; 1295 1296 1297val satisfy_priv_constraints_v3_def = 1298Define `satisfy_priv_constraints_v3 f m n = 1299 !g s1 s1' a . 1300 mmu_requirements s1 g ��� 1301 (ARM_MODE s1 = m) ==> 1302 (ARM_MODE s1' = n) ==> 1303 (f s1 = ValueState a s1') ==> 1304 (��access_violation s1) ==> 1305 (��access_violation s1') ==> 1306 priv_mode_constraints_v3 g s1 s1'`; 1307 1308val satisfy_priv_constraints_v2_def = 1309Define `satisfy_priv_constraints_v2 f m n = 1310 !g s1 s1' a . 1311 mmu_requirements s1 g ��� 1312 (ARM_MODE s1 = m) ==> 1313 (ARM_MODE s1' = n) ==> 1314 (f s1 = ValueState a s1') ==> 1315 (��access_violation s1) ==> 1316 (��access_violation s1') ==> 1317 priv_mode_constraints_v2 g s1 s1'`; 1318 1319val satisfy_priv_constraints_v2a_def = 1320Define `satisfy_priv_constraints_v2a f m n = 1321 !g s1 s1' a . 1322 mmu_requirements s1 g ��� 1323 (ARM_MODE s1 = m) ==> 1324 (ARM_MODE s1' = n) ==> 1325 (f s1 = ValueState a s1') ==> 1326 (��access_violation s1) ==> 1327 (��access_violation s1') ==> 1328 priv_mode_constraints_v2a g s1 s1'`; 1329 1330 1331val IT_advance_untouch_mmu_setup_thm = 1332 store_thm ("IT_advance_untouch_mmu_setup_thm", 1333 ``!s a s'. 1334 (IT_advance <|proc := 0|> s = ValueState a s') ==> 1335 ((s.coprocessors = s'.coprocessors) 1336 /\ 1337 (s.memory = s'.memory) 1338 /\ 1339 (s.accesses = s'.accesses)) 1340 `` 1341 , 1342 EVAL_TAC 1343 THEN RW_TAC (srw_ss()) [] 1344 THEN UNDISCH_ALL_TAC 1345 THEN (NTAC 2 (RW_TAC (srw_ss()) [])) 1346); 1347 1348 1349val IT_advance_keep_access_violation_thm = 1350 store_thm ("IT_advance_keep_access_violation_thm", 1351 ``!s a s' g. mmu_requirements s g ==> 1352 ��access_violation s ==> 1353 (IT_advance <|proc := 0|> s = ValueState a s') ==> 1354 ��access_violation s'`` 1355 , 1356 RW_TAC (srw_ss()) [seqT_def] 1357 THEN IMP_RES_TAC IT_advance_untouch_mmu_setup_thm 1358 THEN IMP_RES_TAC (SPECL [``s:arm_state``, 1359 ``s':arm_state``, 1360 ``g:bool[32]``] 1361 trivially_untouched_av_lem2) 1362 THEN UNDISCH_ALL_TAC 1363 THEN RW_TAC (srw_ss()) [] 1364 ); 1365 1366val IT_advance_untouch_security_ex_thm = 1367 store_thm ("IT_advance_untouch_security_ex_thm", 1368 ``!y s. 1369 Extension_Security ��� s.information.extensions ==> 1370 (IT_advance <|proc := 0|> s = ValueState a s') ==> 1371 Extension_Security ��� s'.information.extensions 1372 1373 `` 1374 , 1375 EVAL_TAC 1376 THEN RW_TAC (srw_ss()) [] 1377 THEN UNDISCH_ALL_TAC 1378 THEN (NTAC 2 (RW_TAC (srw_ss()) [])) 1379); 1380 1381 1382val _ = export_theory(); 1383