1(* Oliver *) 2 3open HolKernel boolLib bossLib Parse; 4open MMUTheory; 5open Cond_rewrite blastLib; 6 7val _ = new_theory "MMU_Setup"; 8 9(* === MMU requirements === *) 10val guest1_min_adr_def = Define `guest1_min_adr = 0x100000w:word32`; 11val guest1_max_adr_def = Define `guest1_max_adr= 0x3FFFFFw:word32`; 12val guest2_min_adr_def = Define `guest2_min_adr = 0x400000w:word32`; 13val guest2_max_adr_def = Define `guest2_max_adr = 0x6FFFFFw:word32`; 14 15val _ = new_constant ("guest1", ``:word32``); 16val _ = new_constant ("guest2", ``:word32``); 17 18val you_and_me_axiom = new_axiom("you_and_me_axiom", ``guest1 <> guest2``); 19val you_and_me_thm = store_thm("you_and_me_thm", ``guest1 <> guest2``, FULL_SIMP_TAC (srw_ss()) [you_and_me_axiom]); 20 21val inequal_by_inequalities_gt_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a > x) /\ (b <= x) ==> (a <> b)``; 22 23val inequal_by_inequalities_lt_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a < x) /\ (b >= x) ==> (a <> b)``; 24 25val inequal_by_inequalities_gtu_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a >+ x) /\ (b <=+ x) ==> (a <> b)``; 26 27val inequal_by_inequalities_ltu_lem = blastLib.BBLAST_PROVE ``!(x:word32) (a:word32) (b:word32). (a <+ x) /\ (b >=+ x) ==> (a <> b)``; 28 29 30 31val inequal_by_inequalities = save_thm( 32 "inequal_by_inequalities", 33(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gtu_lem) 34(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_gtu_lem) 35(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_ltu_lem) 36(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_ltu_lem) 37(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_gtu_lem) 38(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_gtu_lem) 39(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_ltu_lem) 40(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_ltu_lem) 41(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_gt_lem) 42(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_gt_lem) 43(CONJ (SPEC ``guest1_min_adr:word32`` inequal_by_inequalities_lt_lem) 44(CONJ (SPEC ``guest1_max_adr:word32`` inequal_by_inequalities_lt_lem) 45(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_gt_lem) 46(CONJ (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_gt_lem) 47(CONJ (SPEC ``guest2_min_adr:word32`` inequal_by_inequalities_lt_lem) 48 (SPEC ``guest2_max_adr:word32`` inequal_by_inequalities_lt_lem))))))))))))))))); 49 50 51val negated_inequalities_lem = blastLib.BBLAST_PROVE ``!(x:word32) (y:word32). 52 ((~(y <= x)) ==> (y > x)) 53 /\ ((~(y < x)) ==> (y >= x)) 54 /\ ((~(y > x)) ==> (y <= x)) 55 /\ ((~(y >= x)) ==> (y < x)) ``; 56 57val negated_inequalities_unsigned_lem = blastLib.BBLAST_PROVE ``!(x:word32) (y:word32). 58 ((~(y <=+ x)) ==> (y >+ x)) 59 /\ ((~(y <+ x)) ==> (y >=+ x)) 60 /\ ((~(y >+ x)) ==> (y <=+ x)) 61 /\ ((~(y >=+ x)) ==> (y <+ x)) ``; 62 63 64val negated_inequalities = save_thm("negated_inequalities", 65 (CONJ (SPEC ``guest1_min_adr:word32`` negated_inequalities_unsigned_lem) 66 (CONJ (SPEC ``guest1_max_adr:word32`` negated_inequalities_unsigned_lem) 67 (CONJ (SPEC ``guest2_min_adr:word32`` negated_inequalities_unsigned_lem) 68 (CONJ (SPEC ``guest2_max_adr:word32`` negated_inequalities_unsigned_lem) 69 (CONJ (SPEC ``guest1_min_adr:word32`` negated_inequalities_lem) 70 (CONJ (SPEC ``guest1_max_adr:word32`` negated_inequalities_lem) 71 (CONJ (SPEC ``guest2_min_adr:word32`` negated_inequalities_lem) 72 (SPEC ``guest2_max_adr:word32`` negated_inequalities_lem))))))))); 73 74 75val address_cases = save_thm( 76 "address_cases", blastLib.BBLAST_PROVE ``!(b:word32) (a:word32) (X:bool) (Y:bool). 77(((a <= b) ==> X) ==> (((a > b) \/ Y) ==> X) ==> X) /\ 78(((a >= b) ==> X) ==> ((Y \/ (a < b)) ==> X) ==> X) /\ 79(((a <=+ b) ==> X) ==> (((a >+ b) \/ Y) ==> X) ==> X) /\ 80(((a >=+ b) ==> X) ==> ((Y \/ (a <+ b)) ==> X) ==> X)``); 81 82 83 84val negated_and_or = save_thm( 85 "negated_and_or", 86 blastLib.BBLAST_PROVE 87``!(a:word32). 88((~(a > guest2_max_adr ��� a < guest2_min_adr)) = (a <= guest2_max_adr /\ a >= guest2_min_adr)) /\ 89((~(a ��� guest1_max_adr ��� a ��� guest1_min_adr)) = (a > guest1_max_adr \/ a < guest1_min_adr)) /\ 90((~(a > guest1_max_adr ��� a < guest1_min_adr)) = (a <= guest1_max_adr /\ a >= guest1_min_adr)) /\ 91((~(a ��� guest2_max_adr ��� a ��� guest2_min_adr)) = (a > guest2_max_adr \/ a < guest2_min_adr)) /\ 92((~(a > guest2_max_adr ��� a < guest1_min_adr)) = (a <= guest2_max_adr /\ a >= guest1_min_adr)) /\ 93((~(a >+ guest2_max_adr ��� a <+ guest2_min_adr)) = (a <=+ guest2_max_adr /\ a >=+ guest2_min_adr)) /\ 94((~(a <=+ guest1_max_adr ��� a >=+ guest1_min_adr)) = (a >+ guest1_max_adr \/ a <+ guest1_min_adr)) /\ 95((~(a >+ guest1_max_adr ��� a <+ guest1_min_adr)) = (a <=+ guest1_max_adr /\ a >=+ guest1_min_adr)) /\ 96((~(a <=+ guest2_max_adr ��� a >=+ guest2_min_adr)) = (a >+ guest2_max_adr \/ a <+ guest2_min_adr)) /\ 97((~(a >+ guest2_max_adr ��� a <+ guest1_min_adr)) = (a <=+ guest2_max_adr /\ a >=+ guest1_min_adr)) /\ 98((~(a > 0x2FFFFFw ��� a < 0x200000w)) = (a <= 0x2FFFFFw /\ a >= 0x200000w)) /\ 99((~(a ��� 0x1FFFFFw ��� a ��� 0x100000w)) = (a > 0x1FFFFFw \/ a < 0x100000w)) /\ 100((~(a > 0x1FFFFFw ��� a < 0x100000w)) = (a <= 0x1FFFFFw /\ a >= 0x100000w)) /\ 101((~(a ��� 0x2FFFFFw ��� a ��� 0x200000w)) = (a > 0x2FFFFFw \/ a < 0x200000w)) /\ 102((~(a > 0x2FFFFFw ��� a < 0x100000w)) = (a <= 0x2FFFFFw /\ a >= 0x100000w))``); 103 104 105 106(* address border *) 107 108val address_border_concrete = save_thm( 109 "address_border_concrete", blastLib.BBLAST_PROVE ``!(a:word32). (a ��� 0x1FFFFFw \/ a ��� 0x200000w) /\ (a ��� 0x3FFFFFw \/ a ��� 0x400000w) /\ (a <=+ 0x3FFFFFw \/ a >=+ 0x400000w)``); 110 111val address_border = store_thm( 112 "address_border", 113 ``!(a:word32). (a <=+ guest1_max_adr \/ a >=+ guest2_min_adr)``, 114 FULL_SIMP_TAC (srw_ss()) [address_border_concrete, guest1_max_adr_def, guest2_min_adr_def]); 115 116 117(* transitivity for all <, <=, >, >= *) 118val address_trans = store_thm( 119 "address_trans", 120 ``!(x:word32). 121((x <+ guest1_min_adr) ==> (x <=+ guest1_min_adr)) /\ 122((x <+ guest1_min_adr) ==> (x <+ guest1_max_adr)) /\ 123((x <+ guest1_min_adr) ==> (x <=+ guest1_max_adr)) /\ 124((x <+ guest1_min_adr) ==> (x <+ guest2_min_adr)) /\ 125((x <+ guest1_min_adr) ==> (x <=+ guest2_min_adr)) /\ 126((x <+ guest1_min_adr) ==> (x <+ guest2_max_adr)) /\ 127((x <+ guest1_min_adr) ==> (x <=+ guest2_max_adr)) /\ 128((x <=+ guest1_min_adr) ==> (x <+ guest1_max_adr)) /\ 129((x <=+ guest1_min_adr) ==> (x <=+ guest1_max_adr)) /\ 130((x <=+ guest1_min_adr) ==> (x <+ guest2_min_adr)) /\ 131((x <=+ guest1_min_adr) ==> (x <=+ guest2_min_adr)) /\ 132((x <=+ guest1_min_adr) ==> (x <+ guest2_max_adr)) /\ 133((x <=+ guest1_min_adr) ==> (x <=+ guest2_max_adr)) /\ 134((x <+ guest1_max_adr) ==> (x <=+ guest1_max_adr)) /\ 135((x <+ guest1_max_adr) ==> (x <+ guest2_min_adr)) /\ 136((x <+ guest1_max_adr) ==> (x <=+ guest2_min_adr)) /\ 137((x <+ guest1_max_adr) ==> (x <+ guest2_max_adr)) /\ 138((x <+ guest1_max_adr) ==> (x <=+ guest2_max_adr)) /\ 139((x <=+ guest1_max_adr) ==> (x <+ guest2_min_adr)) /\ 140((x <=+ guest1_max_adr) ==> (x <=+ guest2_min_adr)) /\ 141((x <=+ guest1_max_adr) ==> (x <+ guest2_max_adr)) /\ 142((x <=+ guest1_max_adr) ==> (x <=+ guest2_max_adr)) /\ 143((x <+ guest2_min_adr) ==> (x <=+ guest1_max_adr)) /\ 144((x <+ guest2_min_adr) ==> (x <=+ guest2_min_adr)) /\ 145((x <+ guest2_min_adr) ==> (x <+ guest2_max_adr)) /\ 146((x <+ guest2_min_adr) ==> (x <=+ guest2_max_adr)) /\ 147((x <=+ guest2_min_adr) ==> (x <+ guest2_max_adr)) /\ 148((x <=+ guest2_min_adr) ==> (x <=+ guest2_max_adr)) /\ 149((x <+ guest2_max_adr) ==> (x <=+ guest2_max_adr)) /\ 150((x >+ guest2_max_adr) ==> (x >=+ guest2_max_adr)) /\ 151((x >+ guest2_max_adr) ==> (x >+ guest2_min_adr)) /\ 152((x >+ guest2_max_adr) ==> (x >=+ guest2_min_adr)) /\ 153((x >+ guest2_max_adr) ==> (x >+ guest1_max_adr)) /\ 154((x >+ guest2_max_adr) ==> (x >=+ guest1_max_adr)) /\ 155((x >+ guest2_max_adr) ==> (x >+ guest1_min_adr)) /\ 156((x >+ guest2_max_adr) ==> (x >=+ guest1_min_adr)) /\ 157((x >=+ guest2_max_adr) ==> (x >+ guest2_min_adr)) /\ 158((x >=+ guest2_max_adr) ==> (x >=+ guest2_min_adr)) /\ 159((x >=+ guest2_max_adr) ==> (x >+ guest1_max_adr)) /\ 160((x >=+ guest2_max_adr) ==> (x >=+ guest1_max_adr)) /\ 161((x >=+ guest2_max_adr) ==> (x >+ guest1_min_adr)) /\ 162((x >=+ guest2_max_adr) ==> (x >=+ guest1_min_adr)) /\ 163((x >+ guest2_min_adr) ==> (x >=+ guest2_min_adr)) /\ 164((x >+ guest2_min_adr) ==> (x >+ guest1_max_adr)) /\ 165((x >+ guest2_min_adr) ==> (x >=+ guest1_max_adr)) /\ 166((x >+ guest2_min_adr) ==> (x >+ guest1_min_adr)) /\ 167((x >+ guest2_min_adr) ==> (x >=+ guest1_min_adr)) /\ 168((x >=+ guest2_min_adr) ==> (x >+ guest1_max_adr)) /\ 169((x >=+ guest2_min_adr) ==> (x >=+ guest1_max_adr)) /\ 170((x >=+ guest2_min_adr) ==> (x >+ guest1_min_adr)) /\ 171((x >=+ guest2_min_adr) ==> (x >=+ guest1_min_adr)) /\ 172((x >+ guest1_max_adr) ==> (x >=+ guest1_max_adr)) /\ 173((x >+ guest1_max_adr) ==> (x >+ guest1_min_adr)) /\ 174((x >+ guest1_max_adr) ==> (x >=+ guest1_min_adr)) /\ 175((x >=+ guest1_max_adr) ==> (x >+ guest1_min_adr)) /\ 176((x >=+ guest1_max_adr) ==> (x >=+ guest1_min_adr)) /\ 177((x >+ guest1_min_adr) ==> (x >=+ guest1_min_adr))``, 178FULL_SIMP_TAC (srw_ss()) [guest1_min_adr_def, guest1_max_adr_def, guest2_min_adr_def, guest2_max_adr_def] THEN blastLib.BBLAST_TAC); 179 180 181val address_complete = store_thm( 182 "address_complete", 183 ``!(add1:word32). (add1 <=+ guest1_max_adr ��� add1 >=+ guest1_min_adr) \/ 184 (add1 <=+ guest2_max_adr ��� add1 >=+ guest2_min_adr) \/ 185 (add1 >+ guest2_max_adr ��� add1 <+ guest1_min_adr)``, 186 FULL_SIMP_TAC (srw_ss()) [guest1_min_adr_def, guest1_max_adr_def, guest2_min_adr_def, guest2_max_adr_def] THEN blastLib.BBLAST_TAC); 187 188 189(* what we assume when guests are running *) 190val mmu_requirements_def = Define `mmu_requirements state id = 191!add1 is_write u p m. 192 ((u,p,m) = permitted_byte add1 193 is_write 194 state.coprocessors.state.cp15.C1 195 state.coprocessors.state.cp15.C2 196 state.coprocessors.state.cp15.C3 197 F 198 state.memory) 199==> 200 u 201/\ ( ((add1 <=+ guest1_max_adr) /\ (add1 >=+ guest1_min_adr)) ==> (p = (id=guest1)) ) 202/\ ( ((add1 <=+ guest2_max_adr) /\ (add1 >=+ guest2_min_adr)) ==> (p = (id=guest2)) ) 203/\ ( ((add1 >+ guest2_max_adr) \/ (add1 <+ guest1_min_adr)) ==> (~p) ) 204/\ ((state.coprocessors.state.cp15.C2 && (0xFFFFC000w:bool[32])) >=+ 0w) 205/\ ((state.coprocessors.state.cp15.C2 && (0xFFFFC000w:bool[32])) <+ guest1_min_adr) 206/\ (((state.coprocessors.state.cp15.C2 && (0xFFFFC000w:bool[32])) + 4w * 4095w + 3w) <+ guest1_min_adr)`; 207 208 209(* some consequences from the above for permitted_byte_pure *) 210val mmu_requirements_pure_def = Define `mmu_requirements_pure state id = 211!add1 is_write. 212( ((add1 <=+ guest1_max_adr) /\ (add1 >=+ guest1_min_adr)) ==> 213 ((id=guest1) = permitted_byte_pure add1 214 is_write 215 state.coprocessors.state.cp15.C1 216 state.coprocessors.state.cp15.C2 217 state.coprocessors.state.cp15.C3 218 F 219 state.memory)) /\ 220( ((add1 <=+ guest2_max_adr ) /\ (add1 >=+ guest2_min_adr)) ==> 221 ((id=guest2) = permitted_byte_pure add1 222 is_write 223 state.coprocessors.state.cp15.C1 224 state.coprocessors.state.cp15.C2 225 state.coprocessors.state.cp15.C3 226 F 227 state.memory)) /\ 228( ((add1 >+ guest2_max_adr ) \/ (add1 <+ guest1_min_adr)) ==> 229 (~ permitted_byte_pure add1 230 is_write 231 state.coprocessors.state.cp15.C1 232 state.coprocessors.state.cp15.C2 233 state.coprocessors.state.cp15.C3 234 F 235 state.memory))`; 236 237 238(* lemma: mmu_requirements_pure follows from mmu_requirements *) 239val mmu_requirements_simp = store_thm( 240 "mmu_requirements_simp", 241 ``!s g. mmu_requirements s g ==> mmu_requirements_pure s g``, 242 PURE_ONCE_REWRITE_TAC [mmu_requirements_pure_def] 243 THEN NTAC 5 STRIP_TAC 244 THEN Cases_on `permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory` 245 THEN pairLib.PairCases_on `r` 246 THEN NTAC 2 STRIP_TAC 247 THEN TRY DISCH_TAC 248 THENL[`q /\ (r0 = (g=guest1))` by METIS_TAC [mmu_requirements_def] 249 THEN METIS_TAC [permitted_byte_simp], 250 `q /\ (r0 = (g=guest2))` by METIS_TAC [mmu_requirements_def] 251 THEN METIS_TAC [permitted_byte_simp], 252 `q /\ ~r0` by METIS_TAC [mmu_requirements_def] 253 THEN METIS_TAC [permitted_byte_simp] 254 ] 255); 256 257 258(* lemma: mmu_requirements don't change by access list update *) 259 260val mmu_requirement_accesses_update_lem = store_thm( 261 "mmu_requirement_accesses_update_lem", 262 ``!add1 x s g. 263 ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_READ add1)) g)) 264 /\ ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_WRITE add1 x)) g))``, 265 FULL_SIMP_TAC (srw_ss()) [mmu_requirements_def]); 266 267val mmu_requirement_accesses_update_lem2 = store_thm( 268 "mmu_requirement_accesses_update_lem2", 269 ``!add1 x s g. 270 ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_READ add1) o other) g)) 271 /\ ((mmu_requirements s g) = (mmu_requirements (s with accesses updated_by CONS (MEM_WRITE add1 x) o other) g))``, 272 FULL_SIMP_TAC (srw_ss()) [mmu_requirements_def]); 273 274 275 276(* lemma: same setup --> same access rights *) 277 278val same_setup_same_rights_lem = store_thm( 279 "same_setup_same_rights_lem", 280 ``! s1 s2 g add1 is_write. 281 mmu_requirements_pure s1 g ==> 282 mmu_requirements_pure s2 g 283 ==> 284 (permitted_byte_pure add1 is_write s1.coprocessors.state.cp15.C1 285 s1.coprocessors.state.cp15.C2 286 s1.coprocessors.state.cp15.C3 287 F s1.memory 288 = permitted_byte_pure add1 is_write s2.coprocessors.state.cp15.C1 289 s2.coprocessors.state.cp15.C2 290 s2.coprocessors.state.cp15.C3 291 F s2.memory)``, 292 REPEAT STRIP_TAC 293 THEN MP_TAC (SPEC ``add1:word32`` negated_and_or) 294 THEN MP_TAC (SPEC ``add1:word32`` address_border) 295 THEN FULL_SIMP_TAC (srw_ss()) [mmu_requirements_pure_def] 296 THEN METIS_TAC []); 297 298 299val same_setup_same_check_accesses_lem = store_thm( 300 "same_setup_same_check_accesses_lem", 301 ``! s1 s2 g accesses. 302 mmu_requirements_pure s1 g ==> 303 mmu_requirements_pure s2 g 304 ==> 305 (check_accesses_pure accesses s1.coprocessors.state.cp15.C1 306 s1.coprocessors.state.cp15.C2 307 s1.coprocessors.state.cp15.C3 F s1.memory 308 =check_accesses_pure accesses s2.coprocessors.state.cp15.C1 309 s2.coprocessors.state.cp15.C2 310 s2.coprocessors.state.cp15.C3 F s2.memory)``, 311 REPEAT STRIP_TAC 312 THEN Induct_on `accesses` 313 THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def] 314 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 315 THEN STRIP_TAC 316 THEN CASE_TAC 317 THEN ASSUME_TAC (SPECL [``s1:arm_state``, ``s2:arm_state``, ``g:word32``, ``c:word32``] same_setup_same_rights_lem) 318 THEN FULL_SIMP_TAC (srw_ss()) []); 319 320 321val same_setup_same_av_pure_lem = store_thm( 322 "same_setup_same_av_pure_lem", 323 ``! s1 s2 g. 324 mmu_requirements_pure s1 g ==> 325 mmu_requirements_pure s2 g ==> 326 (s1.accesses = s2.accesses) 327 ==> 328 (access_violation_pure s1 = access_violation_pure s2)``, 329 REPEAT STRIP_TAC 330 THEN RW_TAC (srw_ss()) [access_violation_pure_def] 331 THEN METIS_TAC [same_setup_same_check_accesses_lem]); 332 333 334 335(* === well-defined MMU setup allows (simpler) computation of access violation === *) 336 337val access_violation_req = store_thm ( 338 "access_violation_req", 339 ``!s id. (mmu_requirements s id) 340 ==> (access_violation s = access_violation_pure s)``, 341 REPEAT STRIP_TAC 342 THEN Cond_rewrite.COND_REWRITE1_TAC (SPEC ``s:arm_state`` access_violation_simp_FST) 343 THEN FULL_SIMP_TAC (srw_ss()) [access_violation_full_def] 344 THEN `!add1 is_write. 345 ((u,p,m) = (permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory)) 346 ==> u` by METIS_TAC [mmu_requirements_def] 347 THEN `!add1 is_write. 348 FST (permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory)` 349 by (RW_TAC (srw_ss()) [] 350 THEN Cases_on `permitted_byte add1 is_write s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory` 351 THEN pairLib.PairCases_on `r` 352 THEN FULL_SIMP_TAC (srw_ss()) [] 353 THEN METIS_TAC[mmu_requirements_def] 354 ) 355 THEN METIS_TAC [ check_accesses_understand]); 356 357 358 359 360val same_setup_same_av_lem = store_thm( 361 "same_setup_same_av_lem", 362 ``! s1 s2 g. 363 mmu_requirements s1 g ==> 364 mmu_requirements s2 g ==> 365 (s1.accesses = s2.accesses) 366 ==> 367 (access_violation s1 = access_violation s2)``, 368 REPEAT STRIP_TAC 369 THEN IMP_RES_TAC access_violation_req 370 THEN IMP_RES_TAC mmu_requirements_simp 371 THEN ASSUME_TAC same_setup_same_av_pure_lem 372 THEN METIS_TAC []); 373 374(* malicious_read and malicious_write *) 375 376val malicious_read = store_thm ( 377 "malicious_read", 378 ``!s t address. (t = s with accesses updated_by CONS (MEM_READ address)) ==> 379 (~ permitted_byte_pure address F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory \/ 380 ~ permitted_byte_pure address F t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory) 381 ==> access_violation_pure t``, 382 REPEAT STRIP_TAC 383 THEN `?restlist. t.accesses = (MEM_READ address)::restlist` by (EXISTS_TAC ``s.accesses`` THEN FULL_SIMP_TAC (srw_ss()) []) 384 THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) [] 385 THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) [] 386 THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def] 387 THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def] 388 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 389); 390 391 392val malicious_read2 = store_thm ( 393 "malicious_read2", 394 ``!s t address. (t = s with accesses updated_by CONS (MEM_READ address) o other) ==> 395 (~ permitted_byte_pure address F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory \/ 396 ~ permitted_byte_pure address F t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory) 397 ==> access_violation_pure t``, 398 REPEAT STRIP_TAC 399 THEN `?restlist. t.accesses = (MEM_READ address)::restlist` by (EXISTS_TAC ``(other (s.accesses)):(memory_access list)`` THEN FULL_SIMP_TAC (srw_ss()) []) 400 THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) [] 401 THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) [] 402 THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def] 403 THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def] 404 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF]); 405 406 407val malicious_write = store_thm ( 408 "malicious_write", 409 ``!s t address value. (t = s with accesses updated_by CONS (MEM_WRITE address value)) ==> 410 (~ permitted_byte_pure address T s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory \/ 411 ~ permitted_byte_pure address T t.coprocessors.state.cp15.C1 t.coprocessors.state.cp15.C2 t.coprocessors.state.cp15.C3 F t.memory) 412 ==> access_violation_pure t``, 413 REPEAT STRIP_TAC 414 THEN `?restlist. t.accesses = (MEM_WRITE address value)::restlist` by (EXISTS_TAC ``s.accesses`` THEN FULL_SIMP_TAC (srw_ss()) []) 415 THEN `t.memory = s.memory` by FULL_SIMP_TAC (srw_ss()) [] 416 THEN `t.coprocessors = s.coprocessors` by FULL_SIMP_TAC (srw_ss()) [] 417 THEN PURE_ONCE_REWRITE_TAC [access_violation_pure_def] 418 THEN PURE_ONCE_REWRITE_TAC [check_accesses_pure_def] 419 THEN FULL_SIMP_TAC (srw_ss()) [LET_DEF] 420); 421 422 423 424(* predicate "word aligned around address add is readable" *) 425 426 427val aligned_word_readable_def = Define `aligned_word_readable s is_thumb add1 = 428 ( permitted_byte_pure (add1) F s.coprocessors.state.cp15.C1 s.coprocessors.state.cp15.C2 s.coprocessors.state.cp15.C3 F s.memory 429 /\ (is_thumb ==> ( permitted_byte_pure (align(add1,2)) F s.coprocessors.state.cp15.C1 430 s.coprocessors.state.cp15.C2 431 s.coprocessors.state.cp15.C3 F s.memory 432 /\ permitted_byte_pure (align (add1,2) + 1w) F s.coprocessors.state.cp15.C1 433 s.coprocessors.state.cp15.C2 434 s.coprocessors.state.cp15.C3 F s.memory)) 435 436 /\ (~is_thumb ==> ( permitted_byte_pure (align(add1,4)) F s.coprocessors.state.cp15.C1 437 s.coprocessors.state.cp15.C2 438 s.coprocessors.state.cp15.C3 F s.memory 439 /\ permitted_byte_pure (align (add1,4) + 1w) F s.coprocessors.state.cp15.C1 440 s.coprocessors.state.cp15.C2 441 s.coprocessors.state.cp15.C3 F s.memory 442 /\ permitted_byte_pure (align (add1,4) + 2w) F s.coprocessors.state.cp15.C1 443 s.coprocessors.state.cp15.C2 444 s.coprocessors.state.cp15.C3 F s.memory 445 /\ permitted_byte_pure (align (add1,4) + 3w) F s.coprocessors.state.cp15.C1 446 s.coprocessors.state.cp15.C2 447 s.coprocessors.state.cp15.C3 F s.memory)))`; 448 449 450val _ = export_theory(); 451