1(* This theory covers the semi-automatic proofs on primitive operations *) 2(* and simplification concepts needed to show the user lemma *) 3(* Author: Oliver Schwarz *) 4 5open HolKernel boolLib bossLib Parse proofManagerLib; 6open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory arm_stepTheory; 7open MMUTheory MMU_SetupTheory inference_rulesTheory switching_lemma_helperTheory switching_lemmaTheory; 8open tacticsLib ARM_proverLib ARM_prover_toolsLib; 9open user_lemma_basicsTheory; 10open wordsTheory wordsLib; 11 12val _ = new_theory("user_lemma_primitive_operations"); 13 14val _ = goalStack.chatting := !Globals.interactive 15val _ = temp_overload_on ("return", ``constT``); 16 17 18(************************************************************) 19(***************** Massaging Exceptions *****************) 20(************************************************************) 21 22 23val take_svc_exception_comb_thm = save_thm("take_svc_exception_comb_thm", take_svc_exception_thm); 24 25 26val take_undef_instr_exception_comb_thm = 27 save_thm("take_undef_instr_exception_comb_thm", MATCH_MP pmc_31_downgrade (take_undef_instr_exception_thm)); 28 29 30val take_prefetch_abort_exception_comb_thm = 31 save_thm("take_prefetch_abort_exception_comb_thm", MATCH_MP pmc_31_downgrade (take_prefetch_abort_exception_thm)); 32 33 34val take_data_abort_exception_comb_thm = 35 save_thm("take_data_abort_exception_comb_thm", MATCH_MP pmc_31_downgrade (take_data_abort_exception_thm)); 36 37 38val take_irq_exception_comb_thm = 39 save_thm("take_irq_exception_comb_thm", MATCH_MP pmc_31_downgrade (take_irq_exception_thm)); 40 41 42 43(************************************************************) 44(*************** A. CPSR simplifications *****************) 45(************************************************************) 46 47 48 49 50 51(********************** simplifications ***************************) 52(******************* A.1. effects of reading *********************) 53 54 55val const_comp_def = Define `const_comp G = (!s s' x. ((G s = ValueState x s') ==> (s=s')))`; 56 57val read_reg_constlem = store_thm( 58 "read_reg_constlem", 59 ``!n. const_comp (read_reg <|proc:=0|> n)``, 60 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 61 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 62 THEN FULL_SIMP_TAC (srw_ss()) [] 63 THEN UNDISCH_ALL_TAC 64 65 THEN RW_TAC (srw_ss()) []))); 66 67val read_sctlr_constlem = store_thm( 68 "read_sctlr_constlem", 69 ``const_comp (read_sctlr <|proc:=0|> )``, 70 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 71 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 72 THEN FULL_SIMP_TAC (srw_ss()) [] 73 THEN UNDISCH_ALL_TAC 74 THEN RW_TAC (srw_ss()) []))); 75 76 77val read_scr_constlem = store_thm( 78 "read_scr_constlem", 79 ``const_comp (read_scr <|proc:=0|> )``, 80 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 81 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 82 THEN FULL_SIMP_TAC (srw_ss()) [] 83 THEN UNDISCH_ALL_TAC 84 THEN RW_TAC (srw_ss()) []))); 85 86 87val exc_vector_base_constlem = store_thm( 88 "exc_vector_base_constlem", 89 ``const_comp (exc_vector_base <|proc:=0|> )``, 90 FULL_SIMP_TAC (srw_ss()) [const_comp_def] 91 THEN EVAL_TAC THEN (REPEAT (RW_TAC (srw_ss()) [] 92 THEN FULL_SIMP_TAC (srw_ss()) [] 93 THEN UNDISCH_ALL_TAC 94 THEN RW_TAC (srw_ss()) []))); 95 96 97 98val read_cpsr_effect_lem = store_thm( 99 "read_cpsr_effect_lem", 100 ``!s H . ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) s = (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (s.psrs (0, CPSR)))) s)``, 101 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 102 THEN FULL_SIMP_TAC (srw_ss()) [] 103 THEN RES_TAC 104 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 105 106 107 108val read_cpsr_effect_fixed_lem = store_thm( 109 "read_cpsr_effect_fixed_lem", 110 ``!s H xI xF. ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr with <|M := 16w; I:= xI; F:= xF|>))) s = (read_cpsr <|proc:=0|> >>= (\ (cpsr). H ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|> ))) s)``, 111 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 112 THEN FULL_SIMP_TAC (srw_ss()) [] 113 THEN RES_TAC 114 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 115 116 117 118 119val read_cpsr_par_effect_lem = store_thm( 120 "read_cpsr_par_effect_lem", 121 ``!s A H . (const_comp A) ==> (((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, cpsr))) s = ((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, s.psrs (0, CPSR)))) s)``, 122 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 123 THEN Cases_on `A s` 124 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 125 THEN RES_TAC 126 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 127 128 129val read_cpsr_par_effect_fixed_lem = store_thm( 130 "read_cpsr_par_effect_fixed_lem", 131 ``!s A H xI xF. (const_comp A) ==> (((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, (cpsr with <|M := 16w; I:= xI; F:= xF|>) ))) s = ((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, (s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>))) s)``, 132 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 133 THEN Cases_on `A s` 134 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 135 THEN RES_TAC 136 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 137 138 139 140val read_cpsr_par_effect_with_16_lem = store_thm( 141 "read_cpsr_par_effect_with_16_lem", 142 ``!s A H. (const_comp A) ==> (((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, (cpsr with M := 16w) ))) s = ((A ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, (s.psrs (0, CPSR)) with M := 16w))) s)``, 143 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 144 THEN Cases_on `A s` 145 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 146 THEN RES_TAC 147 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 148 149 150val read_cpsr_triple_par_effect_lem = store_thm( 151 "read_cpsr_triple_par_effect_lem", 152 ``!s A B H . (const_comp A) ==> ((((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, cpsr, b))) s) 153 = (((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, (s.psrs (0, CPSR)),b))) s))``, 154 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 155 THEN Cases_on `A s` 156 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 157 THEN RES_TAC 158 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 159 THEN Cases_on `B b` 160 THEN RW_TAC (srw_ss()) []); 161 162 163val read_cpsr_triple_par_effect_lem2 = store_thm( 164 "read_cpsr_triple_par_effect_lem2", 165 ``!s A B H . (const_comp A) ==> (const_comp B) ==> ((((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, cpsr))) s) 166 = (((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, (s.psrs (0, CPSR))))) s))``, 167 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 168 THEN Cases_on `A s` 169 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 170 THEN Cases_on `B b` 171 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 172 THEN RES_TAC 173 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 174 175 176val read_cpsr_triple_par_effect_with_16_lem = store_thm( 177 "read_cpsr_triple_par_effect_with_16_lem", 178 ``!s A B H . (const_comp A) ==> ((((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, (cpsr with M := 16w), b))) s) 179 = (((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, ((s.psrs (0, CPSR)) with M := 16w),b))) s))``, 180 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 181 THEN Cases_on `A s` 182 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 183 THEN RES_TAC 184 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 185 THEN Cases_on `B b` 186 THEN RW_TAC (srw_ss()) []); 187 188 189val read_cpsr_triple_par_effect_with_16_lem2 = store_thm( 190 "read_cpsr_triple_par_effect_with_16_lem2", 191 ``!s A B H . (const_comp A) ==> (const_comp B) ==> ((((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, (cpsr with M := 16w)))) s) 192 = (((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, ((s.psrs (0, CPSR)) with M := 16w)))) s))``, 193 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 194 THEN Cases_on `A s` 195 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 196 THEN Cases_on `B b` 197 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 198 THEN RES_TAC 199 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 200 201val read_cpsr_triple_par_effect_fixed_lem = store_thm( 202 "read_cpsr_triple_par_effect_fixed_lem", 203 ``!s A B H xI xF. (const_comp A) ==> ((((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, (cpsr with <|M := 16w; I:= xI; F:= xF|>), b))) s) 204 = (((A ||| read_cpsr <|proc:=0|> ||| B) >>= (\ (a, cpsr, b). H (a, ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>),b))) s))``, 205 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 206 THEN Cases_on `A s` 207 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 208 THEN RES_TAC 209 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 210 THEN Cases_on `B b` 211 THEN RW_TAC (srw_ss()) []); 212 213 214val read_cpsr_triple_par_effect_fixed_lem2 = store_thm( 215 "read_cpsr_triple_par_effect_fixed_lem2", 216 ``!s A B H xI xF. (const_comp A) ==> (const_comp B) ==> ((((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, (cpsr with <|M := 16w; I:= xI; F:= xF|>)))) s) 217 = (((A ||| B ||| read_cpsr <|proc:=0|>) >>= (\ (a, b, cpsr). H (a, b, ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>)))) s))``, 218 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 219 THEN Cases_on `A s` 220 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 221 THEN Cases_on `B b` 222 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 223 THEN RES_TAC 224 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def]); 225 226 227 228val read_cpsr_quintuple_par_effect_lem = store_thm( 229 "read_cpsr_quintule_par_effect_lem", 230 ``!s A B C D H . (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 231 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, cpsr, d))) s) 232 = (((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, (s.psrs (0, CPSR)), d))) s))``, 233 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 234 THEN Cases_on `A s` 235 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 236 THEN Cases_on `B b` 237 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 238 THEN Cases_on `C 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, readT_def] 242 THEN Cases_on `D b` 243 THEN RW_TAC (srw_ss()) []); 244 245 246val read_cpsr_quintuple_par_effect_lem2 = store_thm( 247 "read_cpsr_quintule_par_effect_lem2", 248 ``!s A B D E H . (const_comp A) ==> (const_comp B) ==> 249 ((((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, cpsr, d, e))) s) 250 = (((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, (s.psrs (0, CPSR)), d, e))) s))``, 251 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 252 THEN Cases_on `A s` 253 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 254 THEN Cases_on `B b` 255 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 256 THEN RES_TAC 257 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 258 THEN Cases_on `D b` 259 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 260 THEN Cases_on `E b'` 261 THEN RW_TAC (srw_ss()) []); 262 263 264val read_cpsr_quintuple_par_effect_with_16_lem = store_thm( 265 "read_cpsr_quintule_par_effect_with_16_lem", 266 ``!s A B C D H . (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 267 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, (cpsr with M := 16w), d))) s) 268 = (((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))``, 269 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 270 THEN Cases_on `A s` 271 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 272 THEN Cases_on `B b` 273 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 274 THEN Cases_on `C b'` 275 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 276 THEN RES_TAC 277 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 278 THEN Cases_on `D b` 279 THEN RW_TAC (srw_ss()) []); 280 281 282val read_cpsr_quintuple_par_effect_with_16_lem2 = store_thm( 283 "read_cpsr_quintule_par_effect_with_16_lem2", 284 ``!s A B D E H . (const_comp A) ==> (const_comp B) ==> 285 ((((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, (cpsr with M := 16w), d, e))) s) 286 = (((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))``, 287 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 288 THEN Cases_on `A s` 289 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 290 THEN Cases_on `B b` 291 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 292 THEN RES_TAC 293 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 294 THEN Cases_on `D b` 295 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 296 THEN Cases_on `E b'` 297 THEN RW_TAC (srw_ss()) []); 298 299 300 301val read_cpsr_quintuple_par_effect_fixed_lem = store_thm( 302 "read_cpsr_quintule_par_effect_fixed_lem", 303 ``!s A B C D H xI xF. (const_comp A) ==> (const_comp B) ==> (const_comp C) ==> 304 ((((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, (cpsr with <|M := 16w; I:= xI; F:= xF|>), d))) s) 305 = (((A ||| B ||| C ||| read_cpsr <|proc:=0|> ||| D) >>= (\ (a, b, c, cpsr, d). H (a, b, c, ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>), d))) s))``, 306 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 307 THEN Cases_on `A s` 308 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 309 THEN Cases_on `B b` 310 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 311 THEN Cases_on `C b'` 312 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 313 THEN RES_TAC 314 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 315 THEN Cases_on `D b` 316 THEN RW_TAC (srw_ss()) []); 317 318 319val read_cpsr_quintuple_par_effect_fixed_lem2 = store_thm( 320 "read_cpsr_quintule_par_effect_fixed_lem2", 321 ``!s A B D E H xI xF. (const_comp A) ==> (const_comp B) ==> 322 ((((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, (cpsr with <|M := 16w; I:= xI; F:= xF|>), d, e))) s) 323 = (((A ||| B ||| read_cpsr <|proc:=0|> ||| D ||| E) >>= (\ (a, b, cpsr, d, e). H (a, b, ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>), d, e))) s))``, 324 RW_TAC (srw_ss()) [parT_def, seqT_def, constT_def] 325 THEN Cases_on `A s` 326 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 327 THEN Cases_on `B b` 328 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 329 THEN RES_TAC 330 THEN RW_TAC (srw_ss()) [read_cpsr_def, read__psr_def, constT_def, readT_def] 331 THEN Cases_on `D b` 332 THEN FULL_SIMP_TAC (srw_ss()) [const_comp_def] 333 THEN Cases_on `E b'` 334 THEN RW_TAC (srw_ss()) []); 335 336 337val read_reg_read_cpsr_par_effect_lem = store_thm( 338 "read_reg_read_cpsr_par_effect_lem", 339 ``!s n H. ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, cpsr ))) s = ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, s.psrs (0, CPSR)))) s``, 340 RW_TAC (srw_ss()) [read_reg_constlem, read_cpsr_par_effect_lem]); 341 342 343 344val read_reg_read_cpsr_par_effect_fixed_lem = store_thm( 345 "read_reg_read_cpsr_par_effect_fixed_lem", 346 ``!s n H xI xF. ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, (cpsr with <|M := 16w; I:= xI; F:= xF|>)))) s = ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (b, cpsr). H (b, ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>) ))) s``, 347 RW_TAC (srw_ss()) [read_reg_constlem, read_cpsr_par_effect_fixed_lem]); 348 349 350 351(********************** simplifications ***************************) 352(************ A.2. computations applied to states ***************) 353 354 355val cpsr_simp_lem = store_thm( 356 "cpsr_simp_lem", 357 ``!s H . (assert_mode 16w s) ==> 358 (((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) s) 359 = ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H ((s.psrs (0, CPSR)) with M := 16w))) s))``, 360 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_cpsr_effect_lem, ARM_READ_CPSR_def] 361 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] 362 THEN METIS_TAC []); 363 364 365val cpsr_simp_ext_lem = store_thm( 366 "cpsr_simp_ext_lem", 367 ``!s H. (assert_mode 16w s) ==> 368 ((s.psrs(0,CPSR)).I = xI) ==> 369 ((s.psrs(0,CPSR)).F = xF) ==> 370 (((read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) s) 371 = ((read_cpsr <|proc:=0|> >>= (\ (cpsr). H ((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>))) s))``, 372 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_cpsr_effect_lem, ARM_READ_CPSR_def] 373 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with <|I := (s.psrs (0,CPSR)).I; F := (s.psrs (0,CPSR)).F; M := 16w|>))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 374 THEN METIS_TAC []); 375 376 377val cpsr_par_simp_lem = store_thm( 378 "cpsr_par_simp_lem", 379 ``!s H n. (assert_mode 16w s) ==> 380 ((((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (a, cpsr). H (a, cpsr))) s) 381 = (((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (a, cpsr). H (a, (s.psrs (0, CPSR)) with M := 16w))) s))``, 382 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_reg_constlem, read_cpsr_par_effect_lem, ARM_READ_CPSR_def] 383 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] 384 THEN METIS_TAC []); 385 386 387val cpsr_triple_simp_ext_lem = store_thm( 388 "cpsr_triple_simp_ext_lem", 389 ``!s H . (assert_mode 16w s) ==> 390 ((s.psrs(0,CPSR)).I = xI) ==> 391 ((s.psrs(0,CPSR)).F = xF) ==> 392 ((((read_reg <|proc:=0|> 15w ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (b,cpsr,d). H (b,cpsr,d))) s) 393 = (((read_reg <|proc:=0|> 15w ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (b,cpsr,d). H (b,((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|>),d))) s))``, 394 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_reg_constlem, read_cpsr_triple_par_effect_lem, ARM_READ_CPSR_def] 395 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with <|I := (s.psrs (0,CPSR)).I; F := (s.psrs (0,CPSR)).F; M := 16w|>))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 396 THEN METIS_TAC []); 397 398 399val cpsr_triple_simp_ext_lem2 = store_thm( 400 "cpsr_triple_simp_ext_lem2", 401 ``!s H . (assert_mode 16w s) ==> 402 ((s.psrs(0,CPSR)).I = xI) ==> 403 ((s.psrs(0,CPSR)).F = xF) ==> 404 ((((read_sctlr <|proc := (0 :num)|> 405 ||| read_scr <|proc := (0 :num)|> 406 ||| read_cpsr <|proc:=0|> ) >>= (\ (sctlr,scr,cpsr). H (sctlr,scr,cpsr))) s) 407 = (((read_sctlr <|proc := (0 :num)|> 408 ||| read_scr <|proc := (0 :num)|> 409 ||| read_cpsr <|proc:=0|> ) >>= (\ (sctlr,scr,cpsr). H (sctlr,scr,((s.psrs (0, CPSR)) with <|M := 16w; I:= xI; F:= xF|> )))) s))``, 410 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_sctlr_constlem, read_scr_constlem, read_cpsr_triple_par_effect_lem2, ARM_READ_CPSR_def] 411 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with <|I := (s.psrs (0,CPSR)).I; F := (s.psrs (0,CPSR)).F; M := 16w|> ))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 412 THEN METIS_TAC []); 413 414 415val cpsr_quintuple_simp_ext_lem = store_thm( 416 "cpsr_quintuple_simp_ext_lem", 417 ``!s H a n m. (assert_mode 16w s) ==> 418 ((s.psrs(0,CPSR)).I = xI) ==> 419 ((s.psrs(0,CPSR)).F = xF) ==> 420 ((((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) 421 = (((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; I:= xI; F:= xF|>), d))) s))``, 422 RW_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, read_reg_constlem, read_cpsr_quintuple_par_effect_lem, ARM_READ_CPSR_def] 423 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with <|I := (s.psrs (0,CPSR)).I; F := (s.psrs (0,CPSR)).F; M := 16w|>))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 424 THEN METIS_TAC []); 425 426 427val cpsr_quintuple_simp_ext_lem2 = store_thm( 428 "cpsr_quintuple_simp_ext_lem2", 429 ``!s H x . (assert_mode 16w s) ==> 430 ((s.psrs(0,CPSR)).I = xI) ==> 431 ((s.psrs(0,CPSR)).F = xF) ==> 432 ((((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) 433 = (((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; I:= xI; F:= xF|>), d, e))) s))``, 434 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] 435 THEN `((s.psrs (0,CPSR)).M = 16w) ==> ((s.psrs (0,CPSR)) = ((s.psrs (0,CPSR)) with <|I := (s.psrs (0,CPSR)).I; F := (s.psrs (0,CPSR)).F; M := 16w|>))` by RW_TAC (srw_ss()) [arm_coretypesTheory.ARMpsr_component_equality] 436 THEN METIS_TAC []); 437 438 439 440 441(********************** simplifications ***************************) 442(****** A.3. computations wrapped by preserving predicate *******) 443 444val (simp_ext_lem, const_lem_list, H_sig, effect_fixed_lem, additional_spec_list) = 445(cpsr_simp_ext_lem, 446 [read_reg_constlem], 447 ``:(ARMpsr ->('a M))``, 448 (read_cpsr_effect_fixed_lem), 449 ([]:Parse.term list)); 450 451 452 453fun CPSR_SIMP_TAC simp_ext_lem const_lem_list H_sig effect_fixed_lem additional_spec_list s2prime = 454 RW_TAC (srw_ss()) [] 455 THEN EQ_TAC 456 THEN RW_TAC (srw_ss()) [preserve_relation_mmu_def, fix_flags_def, fixed_flags_def] 457 THEN RW_TAC (srw_ss()) const_lem_list 458 THEN SPEC_ASSUM_TAC (``!g s1 s2. X``, [``g:word32``, ``s1:arm_state``, ``s2:arm_state``]) 459 THEN NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [assert_mode_def]) 460 THENL[ DISJ1_TAC 461 THEN MAP_EVERY EXISTS_TAC [``a:'a``, ``s1':arm_state``, s2prime], 462 DISJ2_TAC 463 THEN EXISTS_TAC ``e:string``, 464 DISJ1_TAC 465 THEN MAP_EVERY EXISTS_TAC [``a:'a``, ``s1':arm_state``, s2prime], 466 DISJ2_TAC 467 THEN EXISTS_TAC ``e:string``] 468 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s1:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem)) 469 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s2:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem)) 470 THEN ASSUME_TAC (SPECL (List.concat [[``s1:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem) 471 THEN ASSUME_TAC (SPECL (List.concat [[``s2:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem) 472 THEN SPEC_ASSUM_TAC (``!(a:word4) (n:word4) (m:word4). X``, [``aa:word4``, ``nn:word4``, ``mm:word4``]) THEN SPEC_ASSUM_TAC (``!(x:word4). X``, [``x:word4``]) 473 THEN UNDISCH_ALL_TAC 474 THEN RW_TAC (srw_ss()) [assert_mode_def] 475 THEN FULL_SIMP_TAC (srw_ss()) const_lem_list; 476 477 478val cpsr_simp_rel_lem = store_thm( 479 "cpsr_simp_rel_lem", 480 ``!H inv2 uf uy. 481 (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) (assert_mode 16w) (inv2) uf uy) 482 = (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr with M := 16w)))(assert_mode 16w) (inv2) uf uy)``, 483 RW_TAC (srw_ss()) [cpsr_simp_lem, preserve_relation_mmu_def]); 484 485 486val cpsr_simp_rel_ext_lem = store_thm( 487 "cpsr_simp_rel_ext_lem", 488 ``!H inv2 uf uy xI xF. 489 (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy)) 490 = (preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (\ (cpsr). H (cpsr with <|M := 16w; I:= xI; F:= xF|>)))(assert_mode 16w) (inv2) uf (fix_flags xI xF uy))``, 491 FIRST [ 492 CPSR_SIMP_TAC cpsr_simp_ext_lem 493 [read_reg_constlem] 494 ``:(ARMpsr ->('a M))`` 495 (read_cpsr_effect_fixed_lem) 496 ([]:Parse.term list) 497 ``s2':arm_state`` 498 THEN NO_TAC, 499 CPSR_SIMP_TAC cpsr_simp_ext_lem 500 [read_reg_constlem] 501 ``:(ARMpsr ->('a M))`` 502 (read_cpsr_effect_fixed_lem) 503 ([]:Parse.term list) 504 ``s2'':arm_state``]); 505 506val cpsr_par_simp_rel_lem = store_thm( 507 "cpsr_par_simp_rel_lem", 508 ``!n H inv2 uf uy. 509 (preserve_relation_mmu ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (a, cpsr). H (a, cpsr))) (assert_mode 16w) (inv2) uf uy) 510 = (preserve_relation_mmu ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= (\ (a, cpsr). H (a, cpsr with M := 16w)))(assert_mode 16w) (inv2) uf uy)``, 511 RW_TAC (srw_ss()) [cpsr_par_simp_lem, preserve_relation_mmu_def, read_reg_constlem, read_cpsr_par_effect_with_16_lem]); 512 513 514val cpsr_triple_simp_rel_ext_lem = store_thm( 515 "cpsr_triple_simp_rel_ext_lem", 516 ``!H inv2 uf uy xI xF. 517 (preserve_relation_mmu ((read_reg <|proc:=0|> 15w ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (b,cpsr,d). H (b,cpsr,d))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy)) 518 = (preserve_relation_mmu ((read_reg <|proc:=0|> 15w ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (b,cpsr,d). H (b,(cpsr with <|M := 16w; I:= xI; F:= xF|>),d))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy))``, 519 FIRST [ 520 CPSR_SIMP_TAC cpsr_triple_simp_ext_lem 521 [(SPEC ``15w:word4`` read_reg_constlem)] 522 ``:(word32 # ARMpsr # word32 ->('a M))`` 523 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem) 524 [``(read_reg <|proc := 0|> 15w):(word32 M)``, ``(read_teehbr <|proc := 0|>):(word32 M)``] 525 ``s2'':arm_state`` 526 THEN NO_TAC, 527 CPSR_SIMP_TAC cpsr_triple_simp_ext_lem 528 [(SPEC ``15w:word4`` read_reg_constlem)] 529 ``:(word32 # ARMpsr # word32 ->('a M))`` 530 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem) 531 [``(read_reg <|proc := 0|> 15w):(word32 M)``, ``(read_teehbr <|proc := 0|>):(word32 M)``] 532 ``s2':arm_state``] 533); 534 535 536val cpsr_triple_simp_rel_ext_lem2 = store_thm( 537 "cpsr_triple_simp_rel_ext_lem2", 538 ``!H inv2 uf uy xI xF. 539 (preserve_relation_mmu ((read_sctlr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_cpsr <|proc:=0|>) >>= (\ (a,b,cpsr). H (a,b,cpsr))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy)) 540 = (preserve_relation_mmu ((read_sctlr <|proc:=0|> ||| read_scr <|proc:=0|> ||| read_cpsr <|proc:=0|>) >>= (\ (a,b,cpsr). H (a,b,(cpsr with <|M := 16w; I:= xI; F:= xF|>)))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy))``, 541 FIRST [ 542 CPSR_SIMP_TAC cpsr_triple_simp_ext_lem2 543 [read_sctlr_constlem, read_scr_constlem] 544 ``:(CP15sctlr # CP15scr # ARMpsr ->('a M))`` 545 (INST_TYPE [alpha |-> Type `:CP15sctlr`, beta |-> Type `:CP15scr`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem2) 546 [``(read_sctlr <|proc := 0|>):(CP15sctlr M)``, ``(read_scr <|proc := 0|>):(CP15scr M)``] 547 ``s2':arm_state`` 548 THEN NO_TAC, 549 CPSR_SIMP_TAC cpsr_triple_simp_ext_lem2 550 [read_sctlr_constlem, read_scr_constlem] 551 ``:(CP15sctlr # CP15scr # ARMpsr ->('a M))`` 552 (INST_TYPE [alpha |-> Type `:CP15sctlr`, beta |-> Type `:CP15scr`, gamma |-> alpha] read_cpsr_triple_par_effect_fixed_lem2) 553 [``(read_sctlr <|proc := 0|>):(CP15sctlr M)``, ``(read_scr <|proc := 0|>):(CP15scr M)``] 554 ``s2'':arm_state``] 555); 556 557 558val cpsr_quintuple_simp_rel_ext_lem = store_thm( 559 "cpsr_quintuple_simp_rel_ext_lem", 560 ``!aa nn mm H inv2 uf uy xI xF . 561 (preserve_relation_mmu ((read_reg <|proc:=0|> aa ||| read_reg <|proc:=0|> nn ||| read_reg <|proc:=0|> mm ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (aa, bb, cc, cpsr, dd). H (aa, bb, cc, cpsr, dd))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy)) 562 = (preserve_relation_mmu ((read_reg <|proc:=0|> aa ||| read_reg <|proc:=0|> nn ||| read_reg <|proc:=0|> mm ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= (\ (aa, bb, cc, cpsr, dd). H (aa, bb, cc, (cpsr with <|M := 16w; I:= xI; F:= xF|>), dd))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy))``, 563FIRST 564 [CPSR_SIMP_TAC cpsr_quintuple_simp_ext_lem 565 [read_reg_constlem] 566 ``:(word32 # word32 # word32 # ARMpsr # word32->('a M))`` 567 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> Type `:word32`, delta |-> Type `:word32`, Type `:'e` |-> alpha] read_cpsr_quintuple_par_effect_fixed_lem) 568 [``(read_reg <|proc:=0|> aa) :word32 M``, ``(read_reg <|proc:=0|> nn) :word32 M`` , ``(read_reg <|proc:=0|> mm) :word32 M`` , ``(read_teehbr <|proc:=0|> ):word32 M`` ] 569 ``s2'':arm_state`` 570 THEN NO_TAC, 571 CPSR_SIMP_TAC cpsr_quintuple_simp_ext_lem 572 [read_reg_constlem] 573 ``:(word32 # word32 # word32 # ARMpsr # word32->('a M))`` 574 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> Type `:word32`, delta |-> Type `:word32`, Type `:'e` |-> alpha] read_cpsr_quintuple_par_effect_fixed_lem) 575 [``(read_reg <|proc:=0|> aa) :word32 M``, ``(read_reg <|proc:=0|> nn) :word32 M`` , ``(read_reg <|proc:=0|> mm) :word32 M`` , ``(read_teehbr <|proc:=0|> ):word32 M`` ] 576 ``s2':arm_state`` 577 ]); 578 579 580val cpsr_quintuple_simp_rel_ext_lem2 = store_thm( 581 "cpsr_quintuple_simp_rel_ext_lem2", 582 ``!x H inv2 uf uy xI xF. 583 (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|>) >>= (\ (a, b, cpsr, d, e). H (a, b, cpsr, d, e)))) (assert_mode 16w) (inv2) uf (fix_flags xI xF uy)) 584 = (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|>) >>= (\ (a, b, cpsr, d, e). H (a, b, (cpsr with <|M := 16w; I:= xI; F:= xF|>), d, e))))(assert_mode 16w) (inv2) uf (fix_flags xI xF uy))``, 585 FIRST 586 [ CPSR_SIMP_TAC cpsr_quintuple_simp_ext_lem2 587 [read_reg_constlem, exc_vector_base_constlem, read_scr_constlem, read_sctlr_constlem] 588 ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr ->('a M))`` 589 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> Type `:CP15scr`, delta |-> Type `:CP15sctlr`, Type `:'e` |-> alpha] read_cpsr_quintuple_par_effect_fixed_lem2) 590 [``(read_reg <|proc:=0|> x) :word32 M``, ``(exc_vector_base <|proc:=0|>) :word32 M`` , ``(read_scr <|proc:=0|>) :CP15scr M`` , ``(read_sctlr <|proc:=0|> ):CP15sctlr M`` ] 591 ``s2':arm_state`` 592 THEN NO_TAC, 593 CPSR_SIMP_TAC cpsr_quintuple_simp_ext_lem2 594 [read_reg_constlem, exc_vector_base_constlem, read_scr_constlem, read_sctlr_constlem] 595 ``:(word32 # word32 # ARMpsr # CP15scr # CP15sctlr ->('a M))`` 596 (INST_TYPE [alpha |-> Type `:word32`, beta |-> Type `:word32`, gamma |-> Type `:CP15scr`, delta |-> Type `:CP15sctlr`, Type `:'e` |-> alpha] read_cpsr_quintuple_par_effect_fixed_lem2) 597 [``(read_reg <|proc:=0|> x) :word32 M``, ``(exc_vector_base <|proc:=0|>) :word32 M`` , ``(read_scr <|proc:=0|>) :CP15scr M`` , ``(read_sctlr <|proc:=0|> ):CP15sctlr M`` ] 598 ``s2'':arm_state``] 599); 600 601 602 603 604(************************************************************) 605(********** B. registers, memory, minor things ***********) 606(************************************************************) 607 608 609 610(* ========= read_reg ============*) 611 612 613val _ = g `preserve_relation_mmu (LookUpRName <|proc:=0|> (t,M)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 614val _ = go_on 1; 615val LookUpRName_thm = save_thm("LookUpRName_thm", top_thm()); 616 617 618 619g `(~ access_violation s) ==> (((LookUpRName <|proc := 0|> (nw,16w)) s) = ValueState reg s') ==> (reg IN {RName_0usr; RName_1usr; RName_2usr; RName_3usr; RName_4usr; RName_5usr; RName_6usr; RName_7usr; RName_8usr; RName_9usr; RName_10usr; RName_11usr; RName_12usr; RName_SPusr; RName_LRusr; RName_PC})`; 620e(EVAL_TAC); 621e(RW_TAC (srw_ss()) [] THEN METIS_TAC []); 622val lookup_read__reg_help_lem1 = top_thm(); 623 624 625g `(nw <> 15w) ==> (access_violation s) ==> ((((LookUpRName <|proc := 0|> (nw,16w) >>= (��rname. read__reg <|proc := 0|> rname)) s) = ValueState ARB s)) `; 626e(EVAL_TAC); 627e(RW_TAC (srw_ss()) []); 628e(IMP_RES_TAC (blastLib.BBLAST_PROVE ``((nw:word4) <> (0w:word4)) ==> (nw <> 1w) ==> (nw <> 2w) ==> (nw <> 3w) ==> (nw <> 4w) ==> (nw <> 5w) ==> (nw <> 6w) ==> (nw <> 7w) ==> (nw <> 8w) ==> (nw <> 9w) ==> (nw <> 10w) ==> (nw <> 11w) ==> (nw <> 12w) ==> (nw <> 13w) ==> (nw <> 14w) ==> (nw = 15w)``)); 629val lookup_read__reg_help_lem2 = top_thm(); 630 631 632g `(nw = 15w) ==> (access_violation s) ==> (((LookUpRName <|proc := 0|> (nw,16w) >>= (��rname. read__reg <|proc := 0|> rname)) s) = Error "LookUpRName: n = 15w") `; 633e(EVAL_TAC); 634e(RW_TAC (srw_ss()) []); 635val lookup_read__reg_help_lem3 = top_thm(); 636 637 638g ` preserve_relation_mmu (LookUpRName <|proc := 0|> (nw,16w) >>= (��rname. read__reg <|proc := 0|> rname)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 639e(RW_TAC (srw_ss()) [preserve_relation_mmu_def, empty_unt_def, empty_sim_def]); 640e(`access_violation s1 = access_violation s2` by METIS_TAC [similar_def]); 641e(Cases_on `access_violation s1`); 642(* access violation from beginning *) 643e(`access_violation s2` by FULL_SIMP_TAC (srw_ss()) []); 644e(Cases_on `nw = 15w`); 645(* nw = 15 *) 646e(IMP_RES_TAC lookup_read__reg_help_lem3); 647e(RW_TAC (srw_ss()) []); 648(* nw <> 15 *) 649e(IMP_RES_TAC lookup_read__reg_help_lem2); 650e(RW_TAC (srw_ss()) [untouched_refl]); 651(* no access violation from beginning *) 652e(`~ access_violation s2` by FULL_SIMP_TAC (srw_ss()) []); 653e(ASSUME_TAC (SPECL [``nw:word4``,``16w:word5``] (GEN_ALL LookUpRName_thm))); 654e(FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def, empty_sim_def, empty_unt_def]); 655e(SPEC_ASSUM_TAC (``!g s1 s2. X``, [``g:word32``, ``s1:arm_state``, ``s2:arm_state``])); 656e(UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []); 657(* received same value in Lookup *) 658e(`access_violation s1' = access_violation s2'` by METIS_TAC [similar_def]); 659e(FULL_SIMP_TAC (srw_ss()) [seqT_def, read__reg_def, constT_def, readT_def]); 660e(RW_TAC (srw_ss()) []); 661e(ASSUME_TAC (SPECL [``s1':arm_state``, ``s1:arm_state``, ``a:RName``, ``nw:word4``] (GEN_ALL lookup_read__reg_help_lem1))); 662e(FULL_SIMP_TAC (srw_ss()) [similar_def, equal_user_register_def]); 663e(SPEC_ASSUM_TAC (``!(reg:RName). X``, [``a:RName``])); 664e(UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []); 665(* Error in Lookup *) 666e(RW_TAC (srw_ss()) [seqT_def]); 667val lookup_read__reg_thm = top_thm(); 668add_to_simplist lookup_read__reg_thm; 669 670 671g `preserve_relation_mmu (read_reg_mode <|proc:=0|> (nw, 16w)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 672go_on 1; 673val read_reg_mode_thm = save_thm ("read_reg_mode_thm", (MATCH_MP extras_lem2 (top_thm()))); 674 675 676g `preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (��cpsr. read_reg_mode <|proc:=0|> (n,16w))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 677go_on 1; 678val read_cpsr_read_reg_mode_16_thm = save_thm("read_cpsr_read_reg_mode_16_thm", top_thm()); 679 680 681g `preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (��cpsr. read_reg_mode <|proc:=0|> (n,cpsr.M))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 682e(ASSUME_TAC (SPECL [``(\c. read_reg_mode <|proc:=0|> (n, c.M))``, ``assert_mode 16w``] (INST_TYPE [alpha |-> Type `:word32`] cpsr_simp_rel_lem))); 683e(ASSUME_TAC read_cpsr_read_reg_mode_16_thm); 684e(FULL_SIMP_TAC (srw_ss()) []); 685val read_cpsr_read_reg_mode_thm = top_thm(); 686add_to_simplist read_cpsr_read_reg_mode_thm; 687 688 689val (read_reg_empty_thm, _) = prove_it ``read_reg <|proc:=0|> n`` ``assert_mode 16w`` ``assert_mode 16w`` ``empty_unt`` ``empty_sim``; 690val read_reg_thm = save_thm("read_reg_thm", MATCH_MP extras_lem2 read_reg_empty_thm); 691 692 693 694 695 696(* ========= write_reg ============*) 697 698 699g `(nw <> 15w) ==> (access_violation s) ==> ((((LookUpRName <|proc := 0|> (nw,16w) >>= ( \ rname. write__reg <|proc := 0|> rname value)) s) = (ValueState () s))) `; 700e(EVAL_TAC); 701e(RW_TAC (srw_ss()) [] 702 THEN `!(x:unit). x = ()` by (Cases_on `x` THEN EVAL_TAC) 703 THEN SPEC_ASSUM_TAC (``!x. X``, [``ARB:unit``]) 704 THEN FULL_SIMP_TAC (srw_ss()) []); 705e(IMP_RES_TAC (blastLib.BBLAST_PROVE ``((nw:word4) <> (0w:word4)) ==> (nw <> 1w) ==> (nw <> 2w) ==> (nw <> 3w) ==> (nw <> 4w) ==> (nw <> 5w) ==> (nw <> 6w) ==> (nw <> 7w) ==> (nw <> 8w) ==> (nw <> 9w) ==> (nw <> 10w) ==> (nw <> 11w) ==> (nw <> 12w) ==> (nw <> 13w) ==> (nw <> 14w) ==> (nw = 15w)``)); 706val lookup_write__reg_help_lem2 = top_thm(); 707 708 709g `(nw = 15w) ==> (access_violation s) ==> (((LookUpRName <|proc := 0|> (nw,16w) >>= (��rname. write__reg <|proc := 0|> rname value)) s) = Error "LookUpRName: n = 15w") `; 710e(EVAL_TAC); 711e(RW_TAC (srw_ss()) []); 712val lookup_write__reg_help_lem3 = top_thm(); 713 714 715g ` preserve_relation_mmu (LookUpRName <|proc := 0|> (nw,16w) >>= (��rname. write__reg <|proc := 0|> rname value)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 716e(RW_TAC (srw_ss()) [preserve_relation_mmu_def, empty_unt_def, empty_sim_def]); 717e(`access_violation s1 = access_violation s2` by METIS_TAC [similar_def]); 718e(Cases_on `access_violation s1`); 719(* access violation from beginning *) 720e(`access_violation s2` by FULL_SIMP_TAC (srw_ss()) []); 721e(Cases_on `nw = 15w`); 722(* nw = 15 *) 723e(IMP_RES_TAC lookup_write__reg_help_lem3); 724e(RW_TAC (srw_ss()) []); 725(* nw <> 15 *) 726e(IMP_RES_TAC lookup_write__reg_help_lem2); 727e(RW_TAC (srw_ss()) [untouched_refl]); 728(* no access violation from beginning *) 729e(`~ access_violation s2` by FULL_SIMP_TAC (srw_ss()) []); 730e(ASSUME_TAC (SPECL [``nw:word4``,``16w:word5``] (GEN_ALL LookUpRName_thm))); 731e(FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def, empty_sim_def, empty_unt_def]); 732e(SPEC_ASSUM_TAC (``!g s1 s2. X``, [``g:word32``, ``s1:arm_state``, ``s2:arm_state``])); 733e(UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []); 734(* received same value in Lookup *) 735e(DISJ1_TAC); 736e(`access_violation s1' = access_violation s2'` by METIS_TAC [similar_def]); 737e(Cases_on `access_violation s2'` THEN FULL_SIMP_TAC (srw_ss()) [seqT_def, write__reg_def, constT_def, writeT_def]); 738e(RW_TAC (srw_ss()) []); 739(*** untouched 1 *) 740e(IMP_RES_TAC (SPECL [``s1':arm_state``, ``s1:arm_state``, ``a:RName``, ``nw:word4``] (GEN_ALL lookup_read__reg_help_lem1)) 741 THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def, untouched_def, LET_DEF] 742 THEN RW_TAC (srw_ss()) [] 743 THEN REPEAT (UNDISCH_MATCH_TAC ``(reg:RName) <> rn_u``) 744 THEN EVAL_TAC 745 THEN UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []); 746(*** untouched 2 *) 747e (IMP_RES_TAC (SPECL [``s2':arm_state``, ``s2:arm_state``, ``a:RName``, ``nw:word4``] (GEN_ALL lookup_read__reg_help_lem1)) 748 THEN FULL_SIMP_TAC (srw_ss()) [assert_mode_def, untouched_def, LET_DEF] 749 THEN RW_TAC (srw_ss()) [] 750 THEN REPEAT (UNDISCH_MATCH_TAC ``(reg:RName) <> rn_u``) 751 THEN EVAL_TAC 752 THEN UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []); 753(*** mode 1 *) 754e(FULL_SIMP_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, ARM_READ_CPSR_def]); 755(*** mode w *) 756e(FULL_SIMP_TAC (srw_ss()) [assert_mode_def, ARM_MODE_def, ARM_READ_CPSR_def]); 757(*** similar *) 758e(UNDISCH_TAC ``similar g s1' s2'``); 759e(EVAL_TAC); 760e((REPEAT (STRIP_TAC)) THEN FULL_SIMP_TAC (srw_ss()) []); 761e(IMP_RES_TAC untouched_mmu_setup_lem); 762e(ASSUME_TAC (SPECL [``s1':arm_state``, ``s1' with registers updated_by ((0,a) =+ value)``, ``g:word32``] trivially_untouched_av_lem)); 763e(ASSUME_TAC (SPECL [``s2':arm_state``, ``s2' with registers updated_by ((0,a) =+ value)``, ``g:word32``] trivially_untouched_av_lem)); 764e(FULL_SIMP_TAC (srw_ss()) []); 765(* Error in Lookup *) 766e(RW_TAC (srw_ss()) [seqT_def]); 767val lookup_write__reg_thm = top_thm(); 768add_to_simplist lookup_write__reg_thm; 769 770 771g `preserve_relation_mmu (write_reg_mode <|proc:=0|> (nw, 16w) value) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 772go_on 1; 773val write_reg_mode_thm = save_thm ("write_reg_mode_thm", (MATCH_MP extras_lem2 (top_thm()))); 774 775 776g `preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (��cpsr. write_reg_mode <|proc:=0|> (n,16w) value)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 777go_on 1; 778val read_cpsr_read_reg_mode_16_thm = save_thm("read_cpsr_write_reg_mode_16_thm", top_thm()); 779 780 781g `preserve_relation_mmu (read_cpsr <|proc:=0|> >>= (��cpsr. write_reg_mode <|proc:=0|> (n,cpsr.M) value)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 782e(ASSUME_TAC (SPECL [``(\c. write_reg_mode <|proc:=0|> (n, c.M) value)``, ``assert_mode 16w``] (INST_TYPE [alpha |-> Type `:unit`] cpsr_simp_rel_lem))); 783e(ASSUME_TAC read_cpsr_read_reg_mode_16_thm); 784e(FULL_SIMP_TAC (srw_ss()) []); 785val read_cpsr_write_reg_mode_thm = top_thm(); 786add_to_simplist read_cpsr_write_reg_mode_thm; 787 788 789val (write_reg_empty_thm, _) = prove_it ``write_reg <|proc:=0|> n value`` ``assert_mode 16w`` ``assert_mode 16w`` ``empty_unt`` ``empty_sim``; 790val write_reg_thm = save_thm("write_reg_thm", MATCH_MP extras_lem2 write_reg_empty_thm); 791 792 793 794(* ===================================================================== *) 795 796 797(* arch version *) 798 799val arch_version_alternative_def = store_thm( 800 "arch_version_alternative_def", 801 ``arch_version ii = (read_arch ii >>= (\arch. constT(version_number arch)))``, 802 RW_TAC (srw_ss()) [arch_version_def, constT_def, seqT_def]); 803 804g `preserve_relation_mmu (arch_version <|proc:=0|>) 805 (assert_mode 16w) (assert_mode 16w) strict_unt empty_sim`; 806e(RW_TAC (srw_ss()) [arch_version_alternative_def]); 807go_on 1; 808val arch_version_thm = save_thm("arch_version_thm", (MATCH_MP extras_lem4 (SPEC_ALL (top_thm())))); 809 810 811(* ===================================================================== *) 812 813(* address mode *) 814 815 816g `preserve_relation_mmu (thumb_expand_imm_c (imm12,c_in)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 817e(RW_TAC (srw_ss()) [thumb_expand_imm_c_def, LET_DEF] 818 THEN Cases_on `(9 >< 8) (imm12:word12) = (0w:word2)` THEN Cases_on `(9 >< 8) imm12 = (1w:word2)` THEN Cases_on `(9 >< 8) imm12 = (2w:word2)` THEN Cases_on `(9 >< 8) imm12 = (3w:word2)` 819 THEN ASSUME_TAC (blastLib.BBLAST_PROVE ``((((9 >< 8) (imm12:word12)) <> (0w:word2)) /\ (((9 >< 8) imm12) <> (1w:word2)) /\ (((9 >< 8) imm12) <> (2w:word2)) /\ (((9 >< 8) imm12) <> (3w:word2))) ==> F``) 820 THEN UNDISCH_ALL_TAC 821 THEN RW_TAC (srw_ss()) []); 822go_on 11; 823val thumb_expand_imm_c_thm = save_thm("thumb_expand_imm_c_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 824 825 826 827val _ = g `preserve_relation_mmu (address_mode1 <|proc:=0|> enc mode1) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 828val _ = e(Cases_on `mode1` THEN RW_TAC (srw_ss()) [address_mode1_def, LET_DEF]); 829val _ = go_on 1; 830val _ = e(PairedLambda.GEN_BETA_TAC); 831val _ = go_on 1; 832val _ = go_on 1; 833val address_mode1_thm = save_thm("address_mode1_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 834 835 836val _ = g `preserve_relation_mmu (address_mode2 <|proc:=0|> indx addr rn mode2) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 837val _ = e(Cases_on `mode2` THEN RW_TAC (srw_ss()) [address_mode2_def, LET_DEF]); 838val _ = go_on 4; 839val _ = e(PairedLambda.GEN_BETA_TAC); 840val _ = go_on 1; 841val address_mode2_thm = save_thm("address_mode2_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 842 843 844val _ = g `preserve_relation_mmu (address_mode3 <|proc:=0|> indx addr rn mode3) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 845val _ = e(Cases_on `mode3` THEN RW_TAC (srw_ss()) [address_mode3_def, LET_DEF]); 846val _ = go_on 4; 847val _ = e(PairedLambda.GEN_BETA_TAC); 848val _ = go_on 1; 849val address_mode3_thm = save_thm("address_mode3_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 850 851 852 853(* ===================================================================== *) 854 855 856val _ = g `preserve_relation_mmu (read_memA_with_priv <|proc:=0|> (addr, n, p)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 857val _ = go_on 1; 858 859 860val read_memA_with_priv_thm = prove_and_save_s (``read_memA_with_priv <|proc:=0|> (addr, n, p)``, "read_memA_with_priv_thm"); 861 862 863val read_memA_with_priv_loop_body_thm = prove_and_save (``��i. read_memA_with_priv <|proc:=0|> (address + n2w i,1,privileged)``, "read_memA_with_priv_loop_body_thm"); 864 865val read_memA_with_priv_loop_thm = store_thm( 866 "read_memA_with_priv_loop_thm", 867 ``preserve_relation_mmu (forT 0 (size ��� 1) 868 (��i. 869 read_memA_with_priv <|proc:=0|> 870 (address + n2w i,1,privileged))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim``, 871 ASSUME_TAC read_memA_with_priv_loop_body_thm 872 THEN FULL_SIMP_TAC (srw_ss()) [trans_empty_unt_thm, reflex_empty_unt_thm, reflex_empty_sim_thm, forT_preserving_thm]); 873val _ = add_to_simplist read_memA_with_priv_loop_thm; 874 875val _ = g `preserve_relation_mmu (read_memU_with_priv <|proc:=0|> (address:word32, size:num, privileged:bool)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 876val _ = e(FULL_SIMP_TAC (srw_ss()) [read_memU_with_priv_def, LET_DEF]); 877val _ = go_on 1; 878val read_memU_with_priv_thm = save_thm ("read_memU_with_priv_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 879 880 881val write_memA_with_priv_empty_thm = prove_and_save (``write_memA_with_priv <|proc:=0|> (addr, size, p) vl``, "write_memA_with_priv_empty_thm"); 882val write_memA_with_priv_thm = save_thm("write_memA_wih_priv_thm", (MATCH_MP extras_lem2 (SPEC_ALL write_memA_with_priv_empty_thm))); 883 884val write_memA_with_priv_loop_body_thm = prove_and_save (``��i. write_memA_with_priv <|proc:=0|> (address + n2w i,1,privileged) [EL i value]``, "write_memA_with_priv_loop_body_thm"); 885 886val write_memA_with_priv_loop_thm = store_thm( 887 "write_memA_with_priv_loop_thm", 888 ``preserve_relation_mmu (forT 0 (size ��� 1) (��i. write_memA_with_priv <|proc:=0|> (address + n2w i,1,privileged) [EL i value])) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim``, 889 ASSUME_TAC write_memA_with_priv_loop_body_thm 890 THEN FULL_SIMP_TAC (srw_ss()) [trans_empty_unt_thm, reflex_empty_unt_thm, reflex_empty_sim_thm, forT_preserving_thm]); 891val _ = add_to_simplist write_memA_with_priv_loop_thm; 892 893val write_memU_with_priv_empty_thm = prove_and_save (``write_memU_with_priv <|proc:=0|> (address:word32, size:num, privileged:bool) x``, "write_memU_with_priv_empty_thm"); 894val write_memU_with_priv_thm = save_thm ("write_memU_with_priv_thm", (MATCH_MP extras_lem2 (SPEC_ALL (write_memU_with_priv_empty_thm)))); 895 896 897val _ = g `preserve_relation_mmu (set_exclusive_monitors <|proc:=0|> (addr, n)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 898val _ = e(FULL_SIMP_TAC (srw_ss()) [set_exclusive_monitors_def, LET_DEF]); 899val _ = go_on 1; 900val set_exclusive_monitors_thm = save_thm("set_exclusive_monitors_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 901 902 903val _ = g `preserve_relation_mmu 904 ((��(passed,state'). 905 write_monitor <|proc := 0|> (monitor with state := state') >>= 906 (��u. return passed)) 907 ((��(local_passed,x'). 908 (��(passed,x). 909 (if passed then 910 (��y. (��(u,x). (T,x)) (monitor.ClearExclusiveLocal 0 y)) 911 else 912 (��y. (F,y))) x) 913 ((if memaddrdesc.memattrs.shareable then 914 (��y. 915 (��(global_passed,x). (local_passed ��� global_passed,x)) 916 (monitor.IsExclusiveGlobal 917 (memaddrdesc.paddress,<|proc := 0|>,n) y)) 918 else 919 (��y. (local_passed,y))) x')) 920 (monitor.IsExclusiveLocal (memaddrdesc.paddress,<|proc := 0|>,n) 921 monitor.state))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim `; 922val _ = e(Cases_on `(monitor.IsExclusiveLocal (memaddrdesc.paddress,<|proc := 0|>,n) 923 monitor.state)` 924 THEN RW_TAC (srw_ss()) [] 925 THEN Cases_on `(monitor.IsExclusiveGlobal 926 (memaddrdesc.paddress,<|proc := 0|>,n) r)` 927 THEN RW_TAC (srw_ss()) [] 928 THEN Cases_on ` (monitor.ClearExclusiveLocal 0 r')` 929 THEN Cases_on ` (monitor.ClearExclusiveLocal 0 r)` 930 THEN RW_TAC (srw_ss()) []); 931val _ = go_on 4; 932val exclusive_monitors_pass_help_thm = save_thm("exclusive_monitors_pass_help_thm", top_thm()); 933val _ = add_to_simplist exclusive_monitors_pass_help_thm; 934 935 936val _= g `preserve_relation_mmu (exclusive_monitors_pass <|proc:=0|> (addr,n)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 937val _ = e(FULL_SIMP_TAC (srw_ss()) [exclusive_monitors_pass_def, seqE_def, constE_def, LET_DEF]); 938val _ = go_on 1; 939val exclusive_monitors_pass_thm = save_thm("exclusive_monitors_pass_thm", (MATCH_MP extras_lem2 (SPEC_ALL (top_thm())))); 940 941 942 943(************************************************************) 944(************** C. more PSR related lemmas ****************) 945(************************************************************) 946 947 948 949val read_cpsr_thm = prove_and_save_s(``read_cpsr <|proc:=0|>``, "read_cpsr_thm"); 950 951 952val read_cpsr_abs_thm = store_thm("read_cpsr_abs_thm", 953 ``!uy. preserve_relation_mmu_abs (\cp. read_cpsr <|proc:=0|>) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints uy``, 954 (RW_TAC (srw_ss()) [preserve_relation_mmu_abs_def,similar_def, assert_mode_def, priv_mode_constraints_def, read_cpsr_def,read__psr_def,readT_def,untouched_def] THEN FULL_SIMP_TAC (srw_ss()) [])); 955 956 957val read_cpsr_comb_thm = store_thm("read_cpsr_comb_thm", 958 ``!invr uy. preserve_relation_mmu (read_cpsr <|proc:=0|>) invr invr empty_unt uy``, 959 (RW_TAC (srw_ss()) [preserve_relation_mmu_def,similar_def, assert_mode_def,read_cpsr_def,read__psr_def,readT_def,untouched_def, empty_unt_def] THEN FULL_SIMP_TAC (srw_ss()) [])); 960 961 962val write_cpsr_thm = store_thm( 963 "write_cpsr_thm", 964 `` !k k'. preserve_relation_mmu ( write_cpsr <|proc :=0 |> (cpsr with <|I := xI; F := xF; M := k'|>)) (assert_mode k) (assert_mode k') empty_unt (fix_flags xI xF empty_sim)``, 965 `!psr. (psr <> CPSR) ==> (0 <> PSRName2num psr)` by (EVAL_TAC THEN RW_TAC (srw_ss()) []) 966 THEN RW_TAC (srw_ss()) [preserve_relation_mmu_def,write_cpsr_def,write__psr_def,writeT_def,similar_def,untouched_def,assert_mode_def, fix_flags_def, fixed_flags_def, empty_sim_def, empty_unt_def] 967 THEN EVAL_TAC 968 THEN FULL_SIMP_TAC (srw_ss()) [] 969 THEN FULL_SIMP_TAC (srw_ss()) [equal_user_register_def] 970 THEN ASSUME_TAC (SPECL [``s1:arm_state``, ``s1 with psrs updated_by ((0,CPSR) =+ cpsr with <|I := xI; F := (s2.psrs (0,CPSR)).F; M := k'|>)``, ``g:word32``] trivially_untouched_av_lem) 971 THEN ASSUME_TAC (SPECL [``s2:arm_state``, ``s2 with psrs updated_by ((0,CPSR) =+ cpsr with <|I := xI; F := (s2.psrs (0,CPSR)).F; M := k'|>)``, ``g:word32``] trivially_untouched_av_lem) 972 THEN UNDISCH_ALL_TAC 973 THEN RW_TAC (srw_ss()) []); 974 975 976 977(* write cpsr with several components*) 978 979 980val write_cpsr_E_IFM_thm = store_thm( 981 "write_cpsr_E_IFM_thm", 982 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|E := something; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 983 Q.ABBREV_TAC `cpsr2 = (cpsr with E := something)` 984 THEN `cpsr with <|E := something; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` by (Q.UNABBREV_TAC `cpsr2` 985 THEN FULL_SIMP_TAC (srw_ss()) []) 986 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 987val _ = add_to_simplist write_cpsr_E_IFM_thm; 988 989val write_cpsr_IT_IFM_thm = store_thm( 990 "write_cpsr_IT_IFM_thm", 991 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|IT := something; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 992 Q.ABBREV_TAC `cpsr2 = (cpsr with IT := something)` 993 THEN `cpsr with <|IT := something; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` by (Q.UNABBREV_TAC `cpsr2` 994 THEN FULL_SIMP_TAC (srw_ss()) []) 995 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 996val _ = add_to_simplist write_cpsr_IT_IFM_thm; 997 998 999val write_cpsr_GE_IFM_thm = store_thm( 1000 "write_cpsr_GE_IFM_thm", 1001 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|GE := something; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 1002 Q.ABBREV_TAC `cpsr2 = (cpsr with GE := something)` 1003 THEN `cpsr with <|GE := something; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` 1004 by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) 1005 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 1006val _ = add_to_simplist write_cpsr_GE_IFM_thm; 1007 1008 1009val write_cpsr_Q_IFM_thm = store_thm( 1010 "write_cpsr_Q_IFM_thm", 1011 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|Q := something; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 1012 Q.ABBREV_TAC `cpsr2 = (cpsr with Q := something)` 1013 THEN `cpsr with <|Q := something; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` 1014 by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) 1015 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 1016val _ = add_to_simplist write_cpsr_Q_IFM_thm; 1017 1018 1019 1020val write_cpsr_J_T_IFM_thm = store_thm( 1021 "write_cpsr_J_T_IFM_thm", 1022 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|J := j; I := xI; F := xF; T := t; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 1023 Q.ABBREV_TAC `cpsr2 = (cpsr with <|J := j; T := t|>)` 1024 THEN `cpsr with <|J := j; T := t; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` 1025 by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) 1026 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 1027val _ = add_to_simplist write_cpsr_J_T_IFM_thm; 1028 1029 1030val write_cpsr_flags_IFM_thm = store_thm( 1031 "write_cpsr_flags_IFM_thm", 1032 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|N := n; Z := z; C := c; V := v; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 1033 Q.ABBREV_TAC `cpsr2 = (cpsr with <|N := n; Z := z; C := c; V := v|>)` 1034 THEN `cpsr with <|N := n; Z := z; C := c; V := v; M := 16w; I := xI; F := xF|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` 1035 by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) 1036 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 1037val _ = add_to_simplist write_cpsr_flags_IFM_thm; 1038 1039 1040val write_cpsr_all_components_thm = store_thm( 1041 "write_cpsr_all_components_thm", 1042 ``preserve_relation_mmu (write_cpsr <|proc := 0|> (cpsr with <|N:=n; Z:=z; C:=c; V:=v; Q:=q; IT:=it; J:=j; GE:=ge; E:=e; T:=t; I := xI; F := xF; M := 16w|>)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)``, 1043 Q.ABBREV_TAC `cpsr2 = (cpsr with <|N:=n; Z:=z; C:=c; V:=v; Q:=q; IT:=it; J:=j; GE:=ge; E:=e; T:=t|>)` 1044 THEN `cpsr with <|N:=n; Z:=z; C:=c; V:=v; Q:=q; IT:=it; J:=j; GE:=ge; E:=e; T:=t; I := xI; F := xF; M := 16w|> = (cpsr2) with <|M := 16w; I := xI; F := xF|>` 1045 by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) 1046 THEN FULL_SIMP_TAC (srw_ss()) [write_cpsr_thm]); 1047val _ = add_to_simplist write_cpsr_all_components_thm; 1048 1049 1050 1051(************* applications of simplifications ********************) 1052 1053 1054 1055(* write e *) 1056 1057val _ = g `!e. preserve_relation_mmu (write_e <|proc:=0|> e) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1058val _ = e(STRIP_TAC); 1059val _ = e(ASSUME_TAC (SPECL [``(write_e <|proc := 0|> e):(unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> type_of(``()``)] fix_flags_lem))); 1060val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1061val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1062val _ = e(RW_TAC (srw_ss()) [write_e_def]); 1063val _ = e(ASSUME_TAC (SPECL [``(��cpsr. write_cpsr <|proc := 0|> (cpsr with E := e)):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1064val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1065val _ = go_on 1; 1066val write_e_empty_thm = save_thm("write_e_empty_thm", top_thm()); 1067val write_e_thm = save_thm("write_e_thm", MATCH_MP extras_lem2 (SPEC_ALL write_e_empty_thm)); 1068 1069 1070(* write ge *) 1071 1072val _ = g `!e. preserve_relation_mmu (write_ge <|proc:=0|> ge) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1073val _ = e(STRIP_TAC); 1074val _ = e(ASSUME_TAC (SPECL [``(write_ge <|proc := 0|> ge):(unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> type_of(``()``)] fix_flags_lem))); 1075val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1076val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1077val _ = e(RW_TAC (srw_ss()) [write_ge_def]); 1078val _ = e(ASSUME_TAC (SPECL [``(��cpsr. write_cpsr <|proc := 0|> (cpsr with GE := ge)):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1079val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1080val _ = go_on 1; 1081val write_ge_empty_thm = save_thm("write_ge_empty_thm", top_thm()); 1082val write_ge_thm = save_thm("write_ge_thm", MATCH_MP extras_lem2 (SPEC_ALL write_ge_empty_thm)); 1083 1084 1085 1086(* write is et state*) 1087 1088 1089val _ = g `!e. preserve_relation_mmu (write_isetstate <|proc:=0|> isetstate) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1090val _ = e(STRIP_TAC); 1091val _ = e(ASSUME_TAC (SPECL [``(write_isetstate <|proc := 0|> isetstate):(unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> type_of(``()``)] fix_flags_lem))); 1092val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1093val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1094val _ = e(RW_TAC (srw_ss()) [write_isetstate_def]); 1095val _ = e(ASSUME_TAC (SPECL [``(��cpsr. write_cpsr <|proc := 0|> (cpsr with <|J := (isetstate:word2) ' 1; T := isetstate ' 0 |>)):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1096val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1097val _ = go_on 1; 1098val write_isetstate_empty_thm = save_thm("write_isetstate_empty_thm", top_thm()); 1099val write_isetstate_thm = save_thm("write_isetstate_thm", MATCH_MP extras_lem2 (SPEC_ALL write_isetstate_empty_thm)); 1100 1101 1102 1103(* write flags *) 1104 1105val _ = g `!e. preserve_relation_mmu (write_flags<|proc:=0|> (n,z,c,v)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1106val _ = e(STRIP_TAC); 1107val _ = e(ASSUME_TAC (SPECL [``(write_flags <|proc := 0|> (n,z,c,v)):(unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> type_of(``()``)] fix_flags_lem))); 1108val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1109val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1110val _ = e(RW_TAC (srw_ss()) [write_flags_def]); 1111val _ = e(ASSUME_TAC (SPECL [``(��cpsr. write_cpsr <|proc := 0|> (cpsr with <|N := n; Z := z; C := c; V := v|>)):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1112val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1113val _ = go_on 1; 1114val write_flags_empty_thm = save_thm("write_flags_empty_thm", top_thm()); 1115val write_flags_thm = save_thm("write_flags_thm", MATCH_MP extras_lem2 (SPEC_ALL write_flags_empty_thm)); 1116 1117 1118 1119 1120(* IT advance *) 1121val _ = g `preserve_relation_mmu (read_cpsr <|proc:=0|> >>= 1122 (��cpsr. 1123 if (cpsr.IT = 0w) ��� cpsr.T then 1124 write_cpsr <|proc:=0|> (cpsr with IT := ITAdvance cpsr.IT) 1125 else 1126 errorT "IT_advance: unpredictable")) (assert_mode 16w) (assert_mode 16w) (empty_unt) (fix_flags xI xF empty_sim)`; 1127val _ = e(ASSUME_TAC (SPECL [``(��cpsr. if (cpsr.IT = 0w) ��� cpsr.T then 1128 write_cpsr <|proc:=0|> (cpsr with IT := ITAdvance cpsr.IT) 1129 else 1130 errorT "IT_advance: unpredictable"):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1131val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1132val _ = go_on 1; 1133val it_advance_help_thm = MATCH_MP ((CONJUNCT2 (SPEC_ALL fix_flags_lem))) (GEN_ALL (top_thm())); 1134val _ = add_to_simplist it_advance_help_thm; 1135val IT_advance_empty_thm = prove_and_save(``IT_advance <|proc:=0|>``, "IT_advance_empty_thm"); 1136val IT_advance_thm = save_thm("IT_advance_thm", MATCH_MP extras_lem2 (SPEC_ALL IT_advance_empty_thm)); 1137 1138 1139(* set q *) 1140 1141val _ = g `!e. preserve_relation_mmu (set_q <|proc:=0|>) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1142val _ = e(STRIP_TAC); 1143val _ = e(ASSUME_TAC (SPECL [``(set_q <|proc := 0|> ):(unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> type_of(``()``)] fix_flags_lem))); 1144val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1145val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1146val _ = e(RW_TAC (srw_ss()) [set_q_def]); 1147val _ = e(ASSUME_TAC (SPECL [``(��cpsr. write_cpsr <|proc := 0|> (cpsr with Q := T)):(ARMpsr -> unit M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> type_of(``()``)] cpsr_simp_rel_ext_lem))); 1148val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1149val _ = go_on 1; 1150val set_q_empty_thm = save_thm("set_q_empty_thm", top_thm()); 1151val set_q_thm = save_thm("set_q_thm", MATCH_MP extras_lem2 (SPEC_ALL set_q_empty_thm)); 1152 1153 1154(* read spsr *) 1155 1156 1157val _ = g `preserve_relation_mmu (read_spsr <|proc:=0|>) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 1158val _ = e(ASSUME_TAC (SPECL [``(read_spsr <|proc := 0|> ):(ARMpsr M)``, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``empty_sim``] (INST_TYPE [alpha |-> Type `:ARMpsr`] fix_flags_lem))); 1159val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1160val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1161val _ = e(RW_TAC (srw_ss()) [read_spsr_def]); 1162val _ = e(ASSUME_TAC (SPECL [``(��cpsr. 1163 bad_mode <|proc := 0|> cpsr.M >>= 1164 (��bad_mode. 1165 if bad_mode then 1166 errorT "read_spsr: unpredictable" 1167 else 1168 case cpsr.M of 1169 17w => read__psr <|proc := 0|> SPSR_fiq 1170 | 18w => read__psr <|proc := 0|> SPSR_irq 1171 | 19w => read__psr <|proc := 0|> SPSR_svc 1172 | 22w => read__psr <|proc := 0|> SPSR_mon 1173 | 23w => read__psr <|proc := 0|> SPSR_abt 1174 | 27w => read__psr <|proc := 0|> SPSR_und 1175 | _ => errorT "read_spsr: unpredictable")):(ARMpsr -> ARMpsr M)``, ``(assert_mode 16w):(arm_state->bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``] (INST_TYPE [alpha |-> Type `:ARMpsr`] cpsr_simp_rel_ext_lem))); 1176val _ = e(FULL_SIMP_TAC (srw_ss()) []); 1177val _ = go_on 1; 1178val read_spsr_empty_thm = save_thm("read_spsr_empty_thm", top_thm()); 1179val read_spsr_thm = save_thm("read_spsr_thm", MATCH_MP extras_lem2 (SPEC_ALL read_spsr_empty_thm)); 1180 1181 1182(* if-then *) 1183val _ = g ` preserve_relation_mmu 1184 (read_cpsr <|proc :=0|> >>= 1185 (\cpsr. 1186 (increment_pc <|proc :=0|> Encoding_Thumb ||| 1187 write_cpsr <|proc :=0|> (cpsr with IT := (something))) >>= (��(u1,u2). return ()))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim `; 1188val _ = e(ASSUME_TAC (SPECL [``(read_cpsr <|proc :=0|> >>= 1189 (\cpsr. 1190 (increment_pc <|proc :=0|> Encoding_Thumb ||| 1191 write_cpsr <|proc :=0|> (cpsr with IT := (something))) >>= (��(u1,u2). return ()))):(unit M)``, ``(assert_mode 16w: arm_state -> bool)``, ``(assert_mode 16w: arm_state -> bool)``, ``empty_unt``, ``empty_sim``](INST_TYPE [alpha |-> type_of (``()``)] fix_flags_lem))); 1192val _ = e(NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [])); 1193val _ = e(PAT_X_ASSUM ``X`` FORCE_REV_REWRITE_TAC); 1194val _ = e(RW_TAC (srw_ss()) []); 1195val _ = e(ASSUME_TAC (SPECL [``(\cpsr. (increment_pc <|proc := 0|> Encoding_Thumb 1196 ||| write_cpsr <|proc := 0|> (cpsr with IT := something)) >>= 1197 (��(u1,u2). return ())):(ARMpsr -> unit M)``, ``(assert_mode 16w: arm_state -> bool)``, ``empty_unt``, ``(empty_sim):(word32->arm_state->arm_state->bool)``, ``xI:bool``, ``xF:bool``](INST_TYPE [alpha |-> type_of (``()``)] cpsr_simp_rel_ext_lem))); 1198val _ = e (FULL_SIMP_TAC (srw_ss()) [parT_def]); 1199val _ = go_on 1; 1200val if_then_instr_help_lem1 = save_thm( 1201 "if_then_instr_help_lem1", MATCH_MP extras_lem2 (top_thm())); 1202 1203 1204val if_then_instr_help_lem2 = store_thm( 1205 "if_then_instr_hel_lem2", 1206 `` preserve_relation_mmu (read_cpsr <|proc :=0|> >>= 1207 (\cpsr. 1208 (increment_pc <|proc :=0|> Encoding_Thumb ||| 1209 write_cpsr <|proc :=0|> (cpsr with IT := (firstcond @@ mask))) >>= (��(u1,u2). return ()))) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar``, 1210 ASSUME_TAC (SPECL [``xI:bool``, ``xF:bool``, ``(firstcond @@ mask):word8``] (GEN_ALL if_then_instr_help_lem1)) 1211 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_comb_16_27_thm]); 1212val _ = add_to_simplist if_then_instr_help_lem2; 1213 1214 1215 1216val if_then_instr_comb_thm = prove_and_save_p (``if_then_instr <|proc:=0|> (If_Then firstcond mask)``, "if_then_instr_comb_thm", ``if_then_instr``); 1217 1218 1219 1220(* check array *) 1221 1222val _ = g` preserve_relation_mmu ((read_reg <|proc:=0|> 15w ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| 1223 read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= 1224 (\(pc,rn,rm,cpsr,teehbr). 1225 if rn <=+ rm then 1226 ((write_reg <|proc:=0|> 14w ((0 :+ T) pc) ||| 1227 write_cpsr <|proc:=0|> (cpsr with IT := 0w)) >>= 1228 ( \ (u1:unit,u2:unit). 1229 branch_write_pc <|proc:=0|> (teehbr + 0xFFFFFFF8w))) 1230 else 1231 increment_pc <|proc:=0|> Encoding_ThumbEE))(assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)`; 1232val _ = e(ASSUME_TAC (SPECL [``15w:word4``, ``n:word4``, ``m:word4``, ``(\(pc,rn,rm,cpsr,teehbr). 1233 if rn <=+ rm then 1234 ((write_reg <|proc:=0|> 14w ((0 :+ T) pc) ||| 1235 write_cpsr <|proc:=0|> (cpsr with IT := 0w)) >>= 1236 ( \ (u1:unit,u2:unit). 1237 branch_write_pc <|proc:=0|> (teehbr + 0xFFFFFFF8w))) 1238 else 1239 increment_pc <|proc:=0|> Encoding_ThumbEE):(word32 # word32 # word32 # ARMpsr # word32 -> unit M)``, ``(assert_mode 16w: arm_state -> bool)`` ](INST_TYPE [alpha |-> type_of (``()``)] cpsr_quintuple_simp_rel_ext_lem))); 1240val _ = e (FULL_SIMP_TAC (srw_ss()) [parT_def]); 1241val _ = go_on 1; 1242val check_array_instr_help_lem1 = save_thm( 1243 "check_array_instr_help_lem1", (MATCH_MP extras_lem2 (MATCH_MP ((CONJUNCT2 (SPEC_ALL fix_flags_lem))) (GENL [``xI:bool``, ``xF:bool``] (top_thm()))))); 1244 1245 1246val check_array_instr_help_lem2 = store_thm( 1247 "check_array_instr_help_lem2", 1248 `` preserve_relation_mmu ((read_reg <|proc:=0|> 15w ||| read_reg <|proc:=0|> n ||| read_reg <|proc:=0|> m ||| 1249 read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= 1250 (\(pc,rn,rm,cpsr,teehbr). 1251 if rn <=+ rm then 1252 ((write_reg <|proc:=0|> 14w ((0 :+ T) pc) ||| 1253 write_cpsr <|proc:=0|> (cpsr with IT := 0w)) >>= 1254 ( \ (u1:unit,u2:unit). 1255 branch_write_pc <|proc:=0|> (teehbr + 0xFFFFFFF8w))) 1256 else 1257 increment_pc <|proc:=0|> Encoding_ThumbEE))(assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar``, 1258 ASSUME_TAC check_array_instr_help_lem1 1259 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_comb_16_27_thm]); 1260val _ = add_to_simplist check_array_instr_help_lem2; 1261 1262val check_array_instr_comb_thm = prove_and_save_p (``check_array_instr <|proc:=0|> (Check_Array n m)``, "check_array_instr_comb_thm", ``check_array_instr``); 1263 1264 1265(* null check if thumbee *) 1266 1267val _ = g `preserve_relation_mmu((read_reg <|proc:=0|> 15w ||| read_cpsr <|proc:=0|> ||| read_teehbr <|proc:=0|>) >>= 1268 (\(pc,cpsr,teehbr). 1269 (write_reg <|proc:=0|> 14w ((0 :+ T) pc) ||| 1270 write_cpsr <|proc:=0|> (cpsr with IT := 0w)) >>= 1271 (\(u1:unit, u2:unit). 1272 branch_write_pc <|proc:=0|> (teehbr + 0xFFFFFFFCw))))(assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)`; 1273val _ = e(ASSUME_TAC (SPECL [`` (\(pc,cpsr,teehbr). 1274 (write_reg <|proc:=0|> 14w ((0 :+ T) pc) ||| 1275 write_cpsr <|proc:=0|> (cpsr with IT := 0w)) >>= 1276 (\(u1:unit, u2:unit). 1277 branch_write_pc <|proc:=0|> (teehbr + 0xFFFFFFFCw))):(word32 # ARMpsr # word32 -> unit M)``, ``(assert_mode 16w: arm_state -> bool)``] (INST_TYPE [alpha |-> type_of (``()``)] cpsr_triple_simp_rel_ext_lem))); 1278val _ = e (FULL_SIMP_TAC (srw_ss()) [parT_def]); 1279val _ = go_on 1; 1280val null_check_if_thumbee_help_lem = (MATCH_MP extras_lem2 (MATCH_MP ((CONJUNCT2 (SPEC_ALL fix_flags_lem))) (GENL [``xI:bool``, ``xF:bool``] (top_thm())))); 1281val _ = add_to_simplist null_check_if_thumbee_help_lem; 1282 1283 1284 1285 1286(************************************************************) 1287(******* D. taking privilege levels into account **********) 1288(************************************************************) 1289 1290 1291 1292val current_mode_is_user_or_system_eval_lem = store_thm( 1293 "current_mode_is_user_or_system_eval_lem", 1294 ``!s x s'. 1295 (assert_mode 16w s) ==> 1296 (~ (access_violation s)) ==> 1297 (current_mode_is_user_or_system <|proc:=0|> s = ValueState x s') 1298 ==> x``, 1299 EVAL_TAC THEN RW_TAC (srw_ss()) []); 1300 1301val current_mode_is_user_or_system_eval_lem2 = store_thm( 1302 "current_mode_is_user_or_system_eval_lem2", 1303 ``!s x s'. 1304 (assert_mode 16w s) ==> 1305 (current_mode_is_user_or_system <|proc:=0|> s = ValueState x s') ==> 1306 (~ (access_violation s')) 1307 ==> x``, 1308 EVAL_TAC 1309 THEN REPEAT STRIP_TAC 1310 THEN Cases_on `access_violation s` THEN FULL_SIMP_TAC (srw_ss()) [] 1311 THENL [METIS_TAC [], UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []]); 1312 1313 1314val priv_simp_lem = store_thm( 1315 "priv_simp_lem", 1316 ``!s ifcomp elsecomp. 1317 (assert_mode 16w s) ==> 1318 (((current_mode_is_priviledged <|proc:=0|> >>= 1319 (\current_mode_is_priviledged. 1320 if current_mode_is_priviledged then 1321 ifcomp 1322 else 1323 elsecomp)) s) 1324 = 1325 ((current_mode_is_priviledged <|proc:=0|> >>= 1326 (\current_mode_is_priviledged. 1327 elsecomp)) s))``, 1328 EVAL_TAC THEN RW_TAC (srw_ss()) []); 1329 1330 1331val user_simp_lem = store_thm( 1332 "user_simp_lem", 1333 ``!s E elsecomp. 1334 (assert_mode 16w s) ==> 1335 (((current_mode_is_user_or_system <|proc := 0|> >>= 1336 (��is_user_or_system_mode. 1337 if is_user_or_system_mode then 1338 errorT E 1339 else 1340 elsecomp)) s) 1341 = 1342 ((current_mode_is_user_or_system <|proc := 0|> >>= 1343 (��is_user_or_system_mode. 1344 errorT E)) s))``, 1345 EVAL_TAC THEN RW_TAC (srw_ss()) []); 1346 1347val user_simp_or_lem = store_thm( 1348 "user_simp_or_lem", 1349 ``!s E A elsecomp. 1350 (assert_mode 16w s) ==> 1351 (((current_mode_is_user_or_system <|proc := 0|> >>= 1352 (��is_user_or_system_mode. 1353 if is_user_or_system_mode \/ A then 1354 errorT E 1355 else 1356 elsecomp)) s) 1357 = 1358 ((current_mode_is_user_or_system <|proc := 0|> >>= 1359 (��is_user_or_system_mode. 1360 errorT E)) s))``, 1361 EVAL_TAC THEN RW_TAC (srw_ss()) []); 1362 1363 1364val user_simp_par_or_lem = store_thm( 1365 "user_simp_par_or_lem", 1366 ``!s E A P elsecomp. 1367 (assert_mode 16w s) ==> 1368 ((((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1369 (��(is_user_or_system_mode,otherparam). 1370 if is_user_or_system_mode \/ A then 1371 errorT E 1372 else 1373 elsecomp)) s) 1374 = 1375 (((current_mode_is_user_or_system <|proc := 0|> ||| P )>>= 1376 (��(is_user_or_system_mode,otherparam). 1377 errorT E)) s))``, 1378 EVAL_TAC 1379 THEN RW_TAC (srw_ss()) [] 1380 THEN Cases_on `P s` 1381 THEN FULL_SIMP_TAC (srw_ss()) [] 1382 THEN Cases_on `access_violation b` 1383 THEN FULL_SIMP_TAC (srw_ss()) []); 1384 1385 1386 1387 1388val user_simp_par_or_and_lem = store_thm( 1389 "user_simp_par_or_and_lem", 1390 ``!s E A P elsecomp. 1391 (assert_mode 16w s) ==> 1392 ((((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1393 (��(is_user_or_system_mode,otherparam). 1394 if is_user_or_system_mode \/ (A /\ otherparam) then 1395 errorT E 1396 else 1397 elsecomp)) s) 1398 = 1399 (((current_mode_is_user_or_system <|proc := 0|> ||| P )>>= 1400 (��(is_user_or_system_mode,otherparam). 1401 errorT E)) s))``, 1402 EVAL_TAC 1403 THEN RW_TAC (srw_ss()) [] 1404 THEN Cases_on `P s` 1405 THEN FULL_SIMP_TAC (srw_ss()) [] 1406 THEN Cases_on `access_violation b` 1407 THEN FULL_SIMP_TAC (srw_ss()) []); 1408 1409 1410val user_simp_par_or_eqv_lem = store_thm( 1411 "user_simp_par_or_eqv_lem", 1412 ``!s E x P elsecomp. 1413 (assert_mode 16w s) ==> 1414 ((((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1415 (��(is_user_or_system_mode,otherparam). 1416 if is_user_or_system_mode \/ (otherparam = x) then 1417 errorT E 1418 else 1419 elsecomp)) s) 1420 = 1421 (((current_mode_is_user_or_system <|proc := 0|> ||| P )>>= 1422 (��(is_user_or_system_mode,otherparam). 1423 errorT E)) s))``, 1424 EVAL_TAC 1425 THEN RW_TAC (srw_ss()) [] 1426 THEN Cases_on `P s` 1427 THEN FULL_SIMP_TAC (srw_ss()) [] 1428 THEN Cases_on `access_violation b` 1429 THEN FULL_SIMP_TAC (srw_ss()) []); 1430 1431 1432 1433val priv_simp_rel_lem = store_thm( 1434 "priv_simp_rel_lem", 1435 ``!ifcomp elsecomp inv2 uf uy. 1436 (preserve_relation_mmu 1437 (current_mode_is_priviledged <|proc:=0|> >>= 1438 (\current_mode_is_priviledged. 1439 if current_mode_is_priviledged then 1440 ifcomp 1441 else 1442 elsecomp)) (assert_mode 16w) (inv2) uf uy) 1443 = 1444 (preserve_relation_mmu 1445 (current_mode_is_priviledged <|proc:=0|> >>= 1446 (\current_mode_is_priviledged. 1447 elsecomp)) (assert_mode 16w) (inv2) uf uy)``, 1448 RW_TAC (srw_ss()) [priv_simp_lem, preserve_relation_mmu_def]); 1449 1450 1451 1452val user_simp_rel_lem = store_thm( 1453 "user_simp_rel_lem", 1454 ``!E elsecomp uf uy. 1455 (preserve_relation_mmu 1456 ((current_mode_is_user_or_system <|proc := 0|> >>= 1457 (��is_user_or_system_mode. 1458 if is_user_or_system_mode then 1459 (errorT E: 'a M) 1460 else 1461 elsecomp))) (assert_mode 16w) (assert_mode 16w) uf uy) 1462 = 1463 (preserve_relation_mmu 1464 ((current_mode_is_user_or_system <|proc := 0|> >>= 1465 (��is_user_or_system_mode. 1466 (errorT E: 'a M)))) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1467 RW_TAC (srw_ss()) [user_simp_lem, preserve_relation_mmu_def]); 1468 1469 1470val user_simp_or_rel_lem = store_thm( 1471 "user_simp_or_rel_lem", 1472 ``!E A elsecomp uf uy. 1473 (preserve_relation_mmu 1474 ((current_mode_is_user_or_system <|proc := 0|> >>= 1475 (��is_user_or_system_mode. 1476 if is_user_or_system_mode \/ A then 1477 (errorT E: 'a M) 1478 else 1479 elsecomp))) (assert_mode 16w) (assert_mode 16w) uf uy) 1480 = 1481 (preserve_relation_mmu 1482 ((current_mode_is_user_or_system <|proc := 0|> >>= 1483 (��is_user_or_system_mode. 1484 (errorT E: 'a M)))) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1485 RW_TAC (srw_ss()) [user_simp_or_lem, preserve_relation_mmu_def]); 1486 1487 1488val user_simp_par_or_rel_lem = store_thm( 1489 "user_simp_par_or_rel_lem", 1490 ``!E A (P:'b M) elsecomp uf uy. 1491 (preserve_relation_mmu 1492 (((current_mode_is_user_or_system <|proc := 0|> ||| P) >>= 1493 (��(is_user_or_system_mode,otherparam). 1494 if is_user_or_system_mode \/ A then 1495 (errorT E: 'a M) 1496 else 1497 elsecomp))) (assert_mode 16w) (assert_mode 16w) uf uy) 1498 = 1499 (preserve_relation_mmu 1500 (((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1501 (��(is_user_or_system_mode,otherparam). 1502 (errorT E: 'a M)))) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1503 RW_TAC (srw_ss()) [user_simp_par_or_lem, preserve_relation_mmu_def]); 1504 1505 1506val user_simp_par_or_eqv_rel_lem = store_thm( 1507 "user_simp_par_or_eqv_rel_lem", 1508 ``!E x (P:'b M) elsecomp uf uy. 1509 (preserve_relation_mmu 1510 (((current_mode_is_user_or_system <|proc := 0|> ||| P) >>= 1511 (��(is_user_or_system_mode,otherparam). 1512 if is_user_or_system_mode \/ (otherparam = x) then 1513 (errorT E: 'a M) 1514 else 1515 elsecomp))) (assert_mode 16w) (assert_mode 16w) uf uy) 1516 = 1517 (preserve_relation_mmu 1518 (((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1519 (��(is_user_or_system_mode,otherparam). 1520 (errorT E: 'a M)))) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1521 RW_TAC (srw_ss()) [user_simp_par_or_eqv_lem, preserve_relation_mmu_def]); 1522 1523 1524val user_simp_par_or_and_rel_lem = store_thm( 1525 "user_simp_par_or_and_rel_lem", 1526 ``!E A P elsecomp uf uy. 1527 (preserve_relation_mmu 1528 (((current_mode_is_user_or_system <|proc := 0|> ||| P) >>= 1529 (��(is_user_or_system_mode,otherparam). 1530 if is_user_or_system_mode \/ (A /\ otherparam) then 1531 (errorT E: 'a M) 1532 else 1533 elsecomp))) (assert_mode 16w) (assert_mode 16w) uf uy) 1534 = 1535 (preserve_relation_mmu 1536 (((current_mode_is_user_or_system <|proc := 0|> ||| P)>>= 1537 (��(is_user_or_system_mode,otherparam). 1538 (errorT E: 'a M)))) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1539 RW_TAC (srw_ss()) [user_simp_par_or_and_lem, preserve_relation_mmu_def]); 1540 1541 1542 1543val priv_simp_preserves_help_comb_thm = prove_and_save_p_helper (``current_mode_is_priviledged <|proc := 0|> >>= 1544 (\current_mode_is_priviledged. take_undef_instr_exception <|proc:=0|>)``, "priv_simp_preserves_comb_help_thm"); 1545 1546val user_simp_preserves_help_thm = prove_and_save (``current_mode_is_user_or_system <|proc := 0|> >>= 1547 (��is_user_or_system_mode. (errorT E))``, "user_simp_preserves_help_thm"); 1548 1549 1550 1551val priv_simp_preserves_comb_thm = store_thm( 1552 "priv_simp_preserves_comb_thm", 1553 ``!ifcomp. 1554 (preserve_relation_mmu 1555 (current_mode_is_priviledged <|proc:=0|> >>= 1556 (\current_mode_is_priviledged. 1557 if current_mode_is_priviledged then 1558 ifcomp 1559 else 1560 take_undef_instr_exception <|proc:=0|>)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar)``, 1561 RW_TAC (srw_ss()) [priv_simp_rel_lem, priv_simp_preserves_help_comb_thm]); 1562 1563 1564 1565val user_simp_preserves_empty_thm = store_thm( 1566 "user_simp_preserves_empty_thm", 1567 ``!E elsecomp. (preserve_relation_mmu 1568 ((current_mode_is_user_or_system <|proc := 0|> >>= 1569 (��is_user_or_system_mode. 1570 if is_user_or_system_mode then 1571 errorT E 1572 else 1573 elsecomp))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim)``, 1574 RW_TAC (srw_ss()) [user_simp_rel_lem, user_simp_preserves_help_thm]); 1575 1576val user_simp_preserves_thm = (MATCH_MP extras_lem2 (SPEC_ALL user_simp_preserves_empty_thm)); 1577 1578val user_simp_or_preserves_empty_thm = store_thm( 1579 "user_simp_or_preserves_empty_thm", 1580 ``!E A elsecomp. (preserve_relation_mmu 1581 ((current_mode_is_user_or_system <|proc := 0|> >>= 1582 (��is_user_or_system_mode. 1583 if is_user_or_system_mode \/ A then 1584 errorT E 1585 else 1586 elsecomp))) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim)``, 1587 RW_TAC (srw_ss()) [user_simp_or_rel_lem, user_simp_preserves_help_thm]); 1588 1589val user_simp_or_preserves_thm = (MATCH_MP extras_lem2 (SPEC_ALL user_simp_or_preserves_empty_thm)); 1590 1591 1592val _ = add_to_simplist user_simp_preserves_thm; 1593val _ = add_to_simplist user_simp_or_preserves_thm; 1594val _ = add_to_simplist priv_simp_preserves_comb_thm; 1595 1596 1597 1598(************************************************************) 1599(********************* E. Coprocessors *******************) 1600(************************************************************) 1601 1602 1603 1604val coproc_accepted_ax = new_axiom("coproc_accepted_ax", 1605 ``!s s' inst accept. (assert_mode 16w s) ==> (coproc_accepted <|proc:=0|> inst s = ValueState accept s') ==> (~accept)``); 1606 1607 1608val coproc_accepted_constlem = store_thm( 1609 "coproc_accepted_constlem", 1610 ``!s inst. ?x. coproc_accepted <|proc:=0|> inst s = ValueState x s``, 1611 REPEAT STRIP_TAC THEN EVAL_TAC THEN RW_TAC (srw_ss()) []) 1612 1613 1614val coproc_accepted_usr_def = store_thm( 1615 "coproc_accepted_usr_def", 1616 ``!s inst. (assert_mode 16w s) ==> (coproc_accepted <|proc:=0|> inst s = ValueState F s)``, 1617 RW_TAC (srw_ss()) [] 1618 THEN Cases_on `coproc_accepted <|proc := 0|> inst s` 1619 THEN FULL_SIMP_TAC (srw_ss()) [] 1620 THEN IMP_RES_TAC coproc_accepted_ax 1621 THEN ASSUME_TAC (SPECL [``s:arm_state``, ``inst:CPinstruction``] coproc_accepted_constlem) 1622 THEN (NTAC 2 (FULL_SIMP_TAC (srw_ss()) []))); 1623 1624 1625val coproc_accepted_empty_thm = store_thm( 1626 "coproc_accepted_empty_thm", 1627 ``!inst. preserve_relation_mmu (coproc_accepted <|proc:=0|> inst) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim``, 1628 RW_TAC (srw_ss()) [coproc_accepted_usr_def, preserve_relation_mmu_def, untouched_def, empty_unt_def, empty_sim_def] THEN RW_TAC (srw_ss()) []); 1629 1630val coproc_accepted_thm = save_thm("coproc_accepted_thm", (MATCH_MP extras_lem2 (SPEC_ALL coproc_accepted_empty_thm))); 1631 1632 1633val coproc_accepted_simp_lem = store_thm( 1634 "coproc_accepted_simp_lem", 1635 ``!s inst ifcomp elsecomp. 1636 (assert_mode 16w s) ==> 1637 ((coproc_accepted <|proc:=0|> inst >>= 1638 (��accepted. 1639 if ��accepted then 1640 ifcomp 1641 else 1642 elsecomp)) s 1643 = 1644 (coproc_accepted <|proc:=0|> inst >>= 1645 (��accepted.ifcomp)) s)``, 1646 REPEAT STRIP_TAC 1647 THEN FULL_SIMP_TAC (srw_ss()) [seqT_def] 1648 THEN Cases_on `coproc_accepted <|proc := 0|> inst s` 1649 THEN IMP_RES_TAC coproc_accepted_ax 1650 THEN FULL_SIMP_TAC (srw_ss()) []); 1651 1652 1653val coproc_accepted_simp_rel_lem = store_thm( 1654 "coproc_accepted_simp_rel_lem", 1655 ``!coproc ThisInstr ifcomp elsecomp inv2 uf uy. 1656 (preserve_relation_mmu 1657 (coproc_accepted <|proc:=0|> (coproc,ThisInstr) >>= 1658 (��accepted. 1659 if ��accepted then 1660 ifcomp 1661 else 1662 elsecomp)) (assert_mode 16w) (inv2) uf uy) 1663 = 1664 (preserve_relation_mmu 1665 (coproc_accepted <|proc:=0|> (coproc,ThisInstr) >>= 1666 (��accepted. ifcomp)) (assert_mode 16w) (inv2) uf uy)``, 1667 RW_TAC (srw_ss()) [coproc_accepted_simp_lem, preserve_relation_mmu_def]); 1668 1669 1670 1671val coproc_accepted_simp_preserves_help_comb_thm = prove_and_save_p_helper (``coproc_accepted <|proc := 0|> (coproc,ThisInstr) >>= 1672 (\accepted. take_undef_instr_exception <|proc:=0|>)``, "coproc_accepted_simp_preserves_comb_help_thm"); 1673 1674 1675 1676val coproc_accepted_simp_preserves_comb_thm = store_thm( 1677 "coproc_accepted_simp_preserves_comb_thm", 1678 ``!coproc ThisInstr elsecomp. 1679 preserve_relation_mmu 1680 (coproc_accepted <|proc:=0|> (coproc,ThisInstr) >>= 1681 (��accepted. 1682 if ��accepted then 1683 take_undef_instr_exception <|proc:=0|> 1684 else 1685 elsecomp)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints 1686 priv_mode_similar``, 1687 RW_TAC (srw_ss()) [coproc_accepted_simp_rel_lem, coproc_accepted_simp_preserves_help_comb_thm]); 1688 1689 1690val _ = add_to_simplist coproc_accepted_simp_preserves_comb_thm; 1691 1692 1693 1694(************************************************************) 1695(******** F. Once again PSRs: *psr_write_by_instr *********) 1696(************************************************************) 1697 1698 1699 1700(* cpsr_write_by_instr *) 1701 1702 1703val cpsr_write_by_instr_part1 = 1704``(��(priviledged,is_secure,nsacr,badmode). 1705 if 1706 (bytemask:word4) ' 0 ��� priviledged ��� 1707 (badmode ��� ��is_secure ��� ((((4 >< 0) (value:word32)):word5)= 22w) ��� 1708 ��is_secure ��� ((((4 >< 0) value):word5) = 17w) ��� nsacr.RFR) 1709 then 1710 errorT "cpsr_write_by_instr: unpredictable" 1711 else 1712 (read_sctlr <|proc := 0|> ||| read_scr <|proc := 0|> 1713 ||| read_cpsr <|proc := 0|>) >>= 1714 (��(sctlr,scr,cpsr). 1715 write_cpsr <|proc := 0|> 1716 (cpsr with 1717 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1718 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1719 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1720 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1721 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1722 IT := 1723 if affect_execstate then 1724 if bytemask ' 3 then 1725 if bytemask ' 1 then 1726 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1727 else 1728 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1729 else if bytemask ' 1 then 1730 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1731 else 1732 cpsr.IT 1733 else 1734 cpsr.IT; 1735 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1736 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1737 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1738 A := if bytemask ' 1 ��� priviledged ��� (is_secure ��� scr.AW) then value ' 8 else cpsr.A; 1739 I := if bytemask ' 0 ��� priviledged then value ' 7 else cpsr.I; 1740 F := if bytemask ' 0 ��� priviledged ��� (is_secure ��� scr.FW) /\ (��sctlr.NMFI ��� ��value ' 6) then value ' 6 else cpsr.F; 1741 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T; 1742 M := if bytemask ' 0 ��� priviledged then (4 >< 0) value else cpsr.M|>))) 1743 :(bool # bool # CP15nsacr # bool -> unit M)``; 1744 1745 1746val cpsr_write_by_instr_part2 = 1747``(��(sctlr,scr,cpsr). 1748 write_cpsr <|proc := 0|> 1749 (cpsr with 1750 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1751 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1752 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1753 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1754 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1755 IT := 1756 if affect_execstate then 1757 if bytemask ' 3 then 1758 if bytemask ' 1 then 1759 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1760 else 1761 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1762 else if bytemask ' 1 then 1763 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1764 else 1765 cpsr.IT 1766 else 1767 cpsr.IT; 1768 J := 1769 if bytemask ' 3 ��� affect_execstate then 1770 value ' 24 1771 else 1772 cpsr.J; 1773 GE := 1774 if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1775 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1776 A := cpsr.A; I := cpsr.I; F := cpsr.F; 1777 T := 1778 if bytemask ' 0 ��� affect_execstate then 1779 value ' 5 1780 else 1781 cpsr.T; M := cpsr.M|>)) 1782 :(CP15sctlr # CP15scr # ARMpsr -> unit M)``; 1783 1784val cpsr_write_by_instr_components_without_mode = `` (cpsr with 1785 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1786 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1787 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1788 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1789 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1790 IT := 1791 if affect_execstate then 1792 if bytemask ' 3 then 1793 if bytemask ' 1 then 1794 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1795 else 1796 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1797 else if bytemask ' 1 then 1798 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1799 else 1800 cpsr.IT 1801 else 1802 cpsr.IT; 1803 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1804 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1805 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1806 A := cpsr.A; I := cpsr.I; F := cpsr.F; 1807 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T|>)``; 1808 1809val cpsr_write_by_instr_components_without_IFM = `` (cpsr with 1810 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1811 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1812 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1813 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1814 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1815 IT := 1816 if affect_execstate then 1817 if bytemask ' 3 then 1818 if bytemask ' 1 then 1819 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1820 else 1821 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1822 else if bytemask ' 1 then 1823 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1824 else 1825 cpsr.IT 1826 else 1827 cpsr.IT; 1828 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1829 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1830 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1831 A := cpsr.A; 1832 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T|>)``; 1833 1834 1835val cpsr_write_by_instr_components_with_mode = `` (cpsr with 1836 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1837 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1838 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1839 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1840 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1841 IT := 1842 if affect_execstate then 1843 if bytemask ' 3 then 1844 if bytemask ' 1 then 1845 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1846 else 1847 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1848 else if bytemask ' 1 then 1849 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1850 else 1851 cpsr.IT 1852 else 1853 cpsr.IT; 1854 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1855 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1856 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1857 A := cpsr.A; I := cpsr.I; F := cpsr.F; 1858 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T; 1859 M := 16w|>)``; 1860 1861 1862val cpsr_write_by_instr_components_complete = `` (cpsr with 1863 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1864 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1865 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1866 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1867 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1868 IT := 1869 if affect_execstate then 1870 if bytemask ' 3 then 1871 if bytemask ' 1 then 1872 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1873 else 1874 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1875 else if bytemask ' 1 then 1876 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1877 else 1878 cpsr.IT 1879 else 1880 cpsr.IT; 1881 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1882 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1883 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1884 A := cpsr.A; I := xI; F := xF; 1885 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T; 1886 M := 16w|>)``; 1887 1888 1889val cpsr_write_by_instr_unpriv_def = Define `cpsr_write_by_instr_unpriv (value:word32, bytemask:word4, affect_execstate:bool) = ((current_mode_is_priviledged <|proc := 0|> 1890 ||| is_secure <|proc := 0|> ||| read_nsacr <|proc := 0|> 1891 ||| bad_mode <|proc := 0|> ((4 >< 0) value)) >>= 1892 (��(p,s,n,b). 1893 (read_sctlr <|proc := 0|> ||| read_scr <|proc := 0|> 1894 ||| read_cpsr <|proc := 0|>) >>= 1895 (��(sctlr,scr,cpsr). 1896 write_cpsr <|proc := 0|> 1897 (cpsr with 1898 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1899 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1900 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1901 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1902 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1903 IT := 1904 if affect_execstate then 1905 if bytemask ' 3 then 1906 if bytemask ' 1 then 1907 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1908 else 1909 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1910 else if bytemask ' 1 then 1911 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1912 else 1913 cpsr.IT 1914 else 1915 cpsr.IT; 1916 J := 1917 if bytemask ' 3 ��� affect_execstate then 1918 value ' 24 1919 else 1920 cpsr.J; 1921 GE := 1922 if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1923 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1924 A := cpsr.A; I := cpsr.I; F := cpsr.F; 1925 T := 1926 if bytemask ' 0 ��� affect_execstate then 1927 value ' 5 1928 else 1929 cpsr.T; M := cpsr.M|>))))`; 1930 1931 1932 1933val priv_simp_lem2 = store_thm( 1934 "priv_simp_lem2", 1935 ``!s x H . (assert_mode 16w s) ==> 1936 ((((current_mode_is_priviledged <|proc:=0|> ||| is_secure <|proc:=0|> ||| read_nsacr <|proc:=0|> ||| bad_mode <|proc:=0|> x) >>= (\ (p,s,n,b). H (p,s,n,b))) s) 1937 = (((current_mode_is_priviledged <|proc:=0|> ||| is_secure <|proc:=0|> ||| read_nsacr <|proc:=0|> ||| bad_mode <|proc:=0|> x) >>= (\ (p,s,n,b). H (F,s,n,b))) s))``, 1938 EVAL_TAC THEN RW_TAC (srw_ss()) []); 1939 1940 1941val cpsr_write_by_instr_simp_lem = store_thm( 1942 "cpsr_write_by_instr_simp_lem", 1943 ``!s value bytemask affect_execstate. (assert_mode 16w s) ==> 1944 (cpsr_write_by_instr <|proc:=0|> (value,bytemask,affect_execstate) s 1945 = cpsr_write_by_instr_unpriv (value,bytemask,affect_execstate) s)``, 1946 RW_TAC (srw_ss()) [cpsr_write_by_instr, cpsr_write_by_instr_unpriv_def] 1947 THEN IMP_RES_TAC (SPECL [``s:arm_state``, ``((4 >< 0)(value:word32)):word5``, cpsr_write_by_instr_part1] (INST_TYPE [alpha |-> (type_of(``()``))] priv_simp_lem2)) 1948 THEN FULL_SIMP_TAC (srw_ss()) []); 1949 1950 1951val cpsr_write_by_instr_simp_rel_lem = store_thm( 1952 "cpsr_write_by_instr_simp_rel_lem", 1953 ``!value bytemask affect_execstate uf uy. 1954 (preserve_relation_mmu (cpsr_write_by_instr <|proc:=0|> (value,bytemask,affect_execstate)) (assert_mode 16w) (assert_mode 16w) uf uy) 1955 = (preserve_relation_mmu (cpsr_write_by_instr_unpriv (value,bytemask,affect_execstate)) (assert_mode 16w) (assert_mode 16w) uf uy)``, 1956 RW_TAC (srw_ss()) [cpsr_write_by_instr_simp_lem, preserve_relation_mmu_def]); 1957 1958 1959val _ = g `preserve_relation_mmu 1960 (write_cpsr <|proc := 0|> (^cpsr_write_by_instr_components_complete)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim)`; 1961val _ = e (Q.ABBREV_TAC `cpsr2 = ^cpsr_write_by_instr_components_without_IFM`); 1962val _ = e(`^cpsr_write_by_instr_components_complete = (cpsr2) with <|I:= xI; F:= xF; M := 16w|>` by (Q.UNABBREV_TAC `cpsr2` THEN FULL_SIMP_TAC (srw_ss()) []) THEN 1963 FULL_SIMP_TAC (srw_ss()) []); 1964val _ = go_on 1; 1965val write_cpsr_by_instruction_all_components_thm = save_thm( 1966 "write_cpsr_by_instruction_all_components_thm", top_thm()); 1967val _ = add_to_simplist (write_cpsr_by_instruction_all_components_thm); 1968 1969 1970val _ = g `(preserve_relation_mmu ((read_sctlr <|proc := 0|> ||| read_scr <|proc := 0|> 1971 ||| read_cpsr <|proc := 0|>) >>= 1972 (�� (sctlr,scr,cpsr). 1973 write_cpsr <|proc := 0|> 1974 (cpsr with 1975 <|N := if bytemask ' 3 then value ' 31 else cpsr.N; 1976 Z := if bytemask ' 3 then value ' 30 else cpsr.Z; 1977 C := if bytemask ' 3 then value ' 29 else cpsr.C; 1978 V := if bytemask ' 3 then value ' 28 else cpsr.V; 1979 Q := if bytemask ' 3 then value ' 27 else cpsr.Q; 1980 IT := 1981 if affect_execstate then 1982 if bytemask ' 3 then 1983 if bytemask ' 1 then 1984 (((15 >< 10) value):word6) @@ (((26 >< 25) value):word2) 1985 else 1986 (((7 >< 2) cpsr.IT):word6) @@ (((26 >< 25) value):word2) 1987 else if bytemask ' 1 then 1988 (((15 >< 10) value):word6) @@ (((1 >< 0) cpsr.IT):word2) 1989 else 1990 cpsr.IT 1991 else 1992 cpsr.IT; 1993 J := if bytemask ' 3 ��� affect_execstate then value ' 24 else cpsr.J; 1994 GE := if bytemask ' 2 then (19 >< 16) value else cpsr.GE; 1995 E := if bytemask ' 1 then value ' 9 else cpsr.E; 1996 A := cpsr.A; I := cpsr.I; F := cpsr.F; 1997 T := if bytemask ' 0 ��� affect_execstate then value ' 5 else cpsr.T; 1998 M := cpsr.M|>))) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim))`; 1999val _ = e(ASSUME_TAC (SPECL [cpsr_write_by_instr_part2, ``(assert_mode 16w: arm_state -> bool)``] (INST_TYPE [alpha |-> type_of (``()``)] cpsr_triple_simp_rel_ext_lem2))); 2000val _ = e (FULL_SIMP_TAC (srw_ss()) []); 2001val _ = go_on 1; 2002val write_cpsr_by_instruction_help_lem = save_thm( 2003 "write_cpsr_by_instruction_help_lem", top_thm()); 2004val _ = add_to_simplist write_cpsr_by_instruction_help_lem; 2005 2006 2007val _ = g `(preserve_relation_mmu (cpsr_write_by_instr <|proc:=0|> (value,bytemask,affect_execstate)) (assert_mode 16w) (assert_mode 16w) empty_unt (fix_flags xI xF empty_sim))`; 2008val _ = e (FULL_SIMP_TAC (srw_ss()) [cpsr_write_by_instr_simp_rel_lem, cpsr_write_by_instr_unpriv_def]); 2009val _ = go_on 1; 2010val cpsr_write_by_instr_thm = save_thm("cpsr_write_by_instr_thm", (MATCH_MP extras_lem2 (MATCH_MP ((CONJUNCT2 (SPEC_ALL fix_flags_lem))) (GENL [``xI:bool``, ``xF:bool``] (top_thm()))))); 2011 2012 2013 2014(* spsr_write_by_instr *) 2015 2016 2017val _ = g `preserve_relation_mmu (spsr_write_by_instr <|proc:=0|> (vl, bm)) (assert_mode 16w) (assert_mode 16w) empty_unt empty_sim`; 2018val _ = e(FULL_SIMP_TAC (srw_ss()) [user_simp_par_or_and_rel_lem, spsr_write_by_instr_def]); 2019val _ = go_on 1; 2020val spsr_write_by_instr_thm = save_thm ("spsr_write_by_instr_thm", (MATCH_MP extras_lem2 (top_thm()))); 2021 2022 2023 2024(*****************************************************************) 2025(**** G. Common operations that are provable automatically *****) 2026(*****************************************************************) 2027 2028 2029val increment_pc_thm = prove_and_save_e (``increment_pc <|proc:=0|> enc``, "increment_pc_thm"); 2030 2031 2032val load_write_pc_thm = prove_and_save_e (``load_write_pc <|proc:=0|> addr``, "load_write_pc_thm"); 2033 2034val alu_write_pc_thm = prove_and_save_e (``alu_write_pc <|proc:=0|> addr``, "alu_write_pc_thm"); 2035 2036val arm_expand_imm_thm = prove_and_save_e (``arm_expand_imm <|proc:=0|> imm12``, "arm_expand_imm_thm"); 2037 2038val shift_thm = prove_and_save_e (``shift (value, type, amount, carry_in)``, "shift_thm"); 2039 2040val read_flags_thm = prove_and_save_e (``read_flags <|proc:=0|>``, "read_flags_thm"); 2041 2042 2043val read_memU_thm = prove_and_save_e (``read_memU <|proc:=0|> (addr, n)``, "read_memU_thm"); 2044 2045val read_memU_unpriv_thm = prove_and_save_e (``read_memU_unpriv <|proc:=0|> (addr, n)``, "read_memU_unpriv_thm"); 2046 2047val read_memA_thm = prove_and_save_s (``read_memA <|proc:=0|> (addr, n)``, "read_memA_thm"); 2048 2049val write_memU_thm = prove_and_save_e (``write_memU <|proc:=0|> (addr, n) x``, "write_memU_thm"); 2050 2051val write_memU_unpriv_thm = prove_and_save_e (``write_memU_unpriv <|proc:=0|> (addr, n) x``, "write_memU_unpriv_thm"); 2052 2053val write_memA_thm = prove_and_save_e (``write_memA <|proc:=0|> (addr, n) x``, "write_memA_thm"); 2054 2055val read_reg_literal_thm = prove_and_save_e (``read_reg_literal <|proc:=0|> n``, "read_reg_literal_thm"); 2056 2057val big_endian_thm = prove_and_save_s (``big_endian <|proc:=0|>``, "big_endian_thm"); 2058 2059val unaligned_support_thm = prove_and_save_e (``unaligned_support <|proc:=0|>``, "unaligned_support_thm"); 2060 2061val pc_store_value_thm = prove_and_save_e (``pc_store_value <|proc:=0|>``, "pc_store_value_thm"); 2062 2063val is_secure_thm = prove_and_save_e(``is_secure <|proc:=0|>``, "is_secure_thm"); 2064 2065val read_nsacr_thm = prove_and_save_e(``read_nsacr <|proc:=0|>``, "read_nsacr_thm"); 2066 2067val current_instr_set_thm = prove_and_save_s(``current_instr_set <|proc:=0|>``, "current_instr_set_thm"); 2068 2069val branch_write_pc_thm = prove_and_save_e(``branch_write_pc <|proc:=0|> d``, "branch_write_pc_thm"); 2070 2071val no_operation_instr_comb_thm = prove_and_save_p (``no_operation_instr <|proc := 0|> enc``, "no_operation_instr_comb_thm", ``no_operation_instr``); 2072 2073 2074val simplist_export_thm = save_thm( 2075 "simplist_export_thm", 2076 LIST_CONJ (!simp_thms_list)); 2077 2078 2079 2080val _ = export_theory(); 2081