1(* The actual instructions *) 2(* Author: Oliver Schwarz *) 3 4open HolKernel boolLib bossLib Parse proofManagerLib; 5open arm_coretypesTheory arm_seq_monadTheory arm_opsemTheory arm_stepTheory; 6open MMUTheory MMU_SetupTheory inference_rulesTheory switching_lemma_helperTheory; 7open tacticsLib ARM_proverLib ARM_prover_toolsLib; 8open user_lemma_basicsTheory user_lemma_primitive_operationsTheory; 9open wordsTheory wordsLib; 10 11val _ = new_theory("user_lemma_instructions"); 12val _ = ParseExtras.temp_loose_equality() 13 14val _ = temp_overload_on ("return", ``constT``); 15val _ = diminish_srw_ss ["one"] 16val _ = augment_srw_ss [rewrites [oneTheory.FORALL_ONE]] 17val _ = BasicProvers.temp_delsimps ["UPDATE_EQ", "UPDATE_APPLY_ID_RWT"] 18 19val _ = goalStack.chatting := !Globals.interactive 20 21(* import simplist *) 22val _ = simp_thms_list := (CONJUNCTS simplist_export_thm); 23 24 25(************************************************************) 26(***************** A. Status Accesses ********************) 27(************************************************************) 28 29 30val _ = g `preserve_relation_mmu (status_access_instruction <|proc:=0|> (enc, inst)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 31val _ = e (Cases_on `inst` THEN FULL_SIMP_TAC (srw_ss()) []); 32(* status to register *) 33val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 34val _ = go_on 4; 35(* register to status *) 36val _ = go_on 1; 37(* immediate to status *) 38val _ = go_on 1; 39(* change processor state *) 40val _ = go_on 1; 41(* set endianness *) 42val _ = go_on 1; 43val status_access_instruction_comb_thm = save_comb_thm ("status_access_instruction_comb_thm", top_thm(), ``status_access_instruction``); 44 45 46(************************************************************) 47(********************** B. Branching *********************) 48(************************************************************) 49 50 51val _ = g `preserve_relation_mmu (branch_link_exchange_imm_instr <|proc := 0|> e (Branch_Link_Exchange_Immediate b b0 c)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 52val _ = e(Cases_on `b0` THEN FULL_SIMP_TAC (srw_ss()) []); 53val _ = go_on 1; 54val _ = e(Cases_on `e` THEN FULL_SIMP_TAC (srw_ss()) []); 55val _ = go_on 4; 56val branch_link_exchange_imm_instr_comb_thm = save_comb_thm("branch_link_exchange_imm_instr_comb_thm", top_thm(), ``branch_link_exchange_imm_instr``); 57 58 59 60val _ = g `preserve_relation_mmu (branch_instruction <|proc := 0|> (e,i)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 61val _ = e(FULL_SIMP_TAC (srw_ss()) [branch_instruction_def]); 62val _ = e(Cases_on `i` THEN FULL_SIMP_TAC (srw_ss()) []); 63val _ = go_on 10; 64val branch_instruction_comb_thm = save_comb_thm("branch_instruction_comb_thm", top_thm(), ``branch_instruction``); 65 66 67 68(************************************************************) 69(******************* C. Memory Access ********************) 70(************************************************************) 71 72 73val _ = g `preserve_relation_mmu 74 ((current_mode_is_user_or_system <|proc := 0|> 75 ||| current_instr_set <|proc := 0|>) >>= 76 (��(is_user_or_system,iset). 77 if is_user_or_system ��� (iset = InstrSet_ThumbEE) then 78 errorT "store_return_state_instr: unpredictable" 79 else 80 (read_reg_mode <|proc := 0|> (13w,c) 81 ||| read_reg <|proc := 0|> 14w 82 ||| read_spsr <|proc := 0|>) >>= 83 (��(base,lr,spsr). 84 (increment_pc <|proc := 0|> enc 85 ||| write_memA <|proc := 0|> 86 (if b ��� b0 then 87 (if b0 then base else base + 0xFFFFFFF8w) + 4w 88 else if b0 then 89 base 90 else 91 base + 0xFFFFFFF8w,4) (bytes (lr,4)) 92 ||| write_memA <|proc := 0|> 93 ((if b ��� b0 then 94 (if b0 then base else base + 0xFFFFFFF8w) + 4w 95 else if b0 then 96 base 97 else 98 base + 0xFFFFFFF8w) + 4w,4) 99 (bytes (encode_psr spsr,4)) 100 ||| condT b1 101 (write_reg_mode <|proc := 0|> (13w,c) 102 (if b0 then 103 base + 8w 104 else 105 base + 0xFFFFFFF8w))) >>= 106 (��(u1,u2,u3,u4). return ())))) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar`; 107val _ = e(FULL_SIMP_TAC (srw_ss()) [user_simp_par_or_eqv_rel_lem]); 108val _ = go_on 1; 109val store_return_state_instr_help_let_thm = save_thm ("store_return_state_instr_help_let_thm", top_thm()); 110 111 112val store_return_state_instr_help_let_comb_thm = store_thm ("store_return_state_instr_help_let_comb_thm", 113 ``preserve_relation_mmu 114 ((current_mode_is_user_or_system <|proc := 0|> 115 ||| current_instr_set <|proc := 0|>) >>= 116 (��(is_user_or_system,iset). 117 if is_user_or_system ��� (iset = InstrSet_ThumbEE) then 118 errorT "store_return_state_instr: unpredictable" 119 else 120 (read_reg_mode <|proc := 0|> (13w,c) 121 ||| read_reg <|proc := 0|> 14w 122 ||| read_spsr <|proc := 0|>) >>= 123 (��(base,lr,spsr). 124 (increment_pc <|proc := 0|> enc 125 ||| write_memA <|proc := 0|> 126 (if b ��� b0 then 127 (if b0 then base else base + 0xFFFFFFF8w) + 4w 128 else if b0 then 129 base 130 else 131 base + 0xFFFFFFF8w,4) (bytes (lr,4)) 132 ||| write_memA <|proc := 0|> 133 ((if b ��� b0 then 134 (if b0 then base else base + 0xFFFFFFF8w) + 4w 135 else if b0 then 136 base 137 else 138 base + 0xFFFFFFF8w) + 4w,4) 139 (bytes (encode_psr spsr,4)) 140 ||| condT b1 141 (write_reg_mode <|proc := 0|> (13w,c) 142 (if b0 then 143 base + 8w 144 else 145 base + 0xFFFFFFF8w))) >>= 146 (��(u1,u2,u3,u4). return ())))) 147 (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar``, 148 ASSUME_TAC store_return_state_instr_help_let_thm 149 THEN ASSUME_TAC (SPECL [``16w:word5``, ``27w:word5``] comb_mode_thm) 150 THEN ASSUME_TAC (SPECL [``(assert_mode 16w):(arm_state->bool)``, 151 ``(assert_mode 27w):(arm_state->bool)``, 152 ``(comb_mode 16w 27w):(arm_state->bool)``, 153 ``(assert_mode 16w):(arm_state->bool)``] (INST_TYPE [alpha |-> type_of(``()``)] preserve_relation_comb_v2_thm)) 154 THEN RES_TAC); 155val _ = add_to_simplist store_return_state_instr_help_let_comb_thm; 156 157 158 159 160val store_multiple_part = ``(��(base,cpsr). 161 (let mode = if system then 16w else cpsr.M and 162 length = n2w (4 * bit_count registers) and 163 lowest = lowest_set_bit registers 164 in 165 let base_address = if addr then base else base ��� length 166 in 167 let start_address = 168 if indx ��� addr then 169 base_address + 4w 170 else 171 base_address 172 in 173 let address i = 174 start_address + 175 n2w (4 * (bit_count_upto (i + 1) registers ��� 1)) 176 in 177 forT 0 14 178 (��i. 179 condT ((registers:word16) ' i) 180 (if (i = w2n n) ��� wback ��� i ��� lowest then 181 write_memA <|proc:=0|> (address i,4) BITS32_UNKNOWN 182 else 183 read_reg_mode <|proc:=0|> (n2w i,mode) >>= 184 (��d. 185 write_memA <|proc:=0|> (address i,4) 186 (bytes (d,4))))) >>= 187 (��unit_list. 188 (condT (registers ' 15) 189 (pc_store_value <|proc:=0|> >>= 190 (��pc. 191 write_memA <|proc:=0|> (address 15,4) 192 (bytes (pc,4)))) ||| increment_pc <|proc:=0|> enc 193 ||| condT wback 194 (if addr then 195 write_reg <|proc:=0|> n (base + length) 196 else 197 write_reg <|proc:=0|> n (base ��� length))) >>= 198 (��(u1,u2,u3). return ())))):bool[32] # ARMpsr -> unit M``; 199 200 201val store_multiple_part_simp = store_thm( 202 "store_multiple_part_simp", 203 `` (preserve_relation_mmu( 204 (read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= 205 (��(base,cpsr). 206 (let mode = if system then 16w else cpsr.M and 207 length = n2w (4 * bit_count registers) and 208 lowest = lowest_set_bit registers 209 in 210 let base_address = if addr then base else base ��� length 211 in 212 let start_address = 213 if indx ��� addr then 214 base_address + 4w 215 else 216 base_address 217 in 218 let address i = 219 start_address + 220 n2w (4 * (bit_count_upto (i + 1) registers ��� 1)) 221 in 222 forT 0 14 223 (��i. 224 condT ((registers:word16) ' i) 225 (if (i = w2n n) ��� wback ��� i ��� lowest then 226 write_memA <|proc:=0|> (address i,4) BITS32_UNKNOWN 227 else 228 read_reg_mode <|proc:=0|> (n2w i,mode) >>= 229 (��d. 230 write_memA <|proc:=0|> (address i,4) 231 (bytes (d,4))))) >>= 232 (��unit_list. 233 (condT (registers ' 15) 234 (pc_store_value <|proc:=0|> >>= 235 (��pc. 236 write_memA <|proc:=0|> (address 15,4) 237 (bytes (pc,4)))) ||| increment_pc <|proc:=0|> enc 238 ||| condT wback 239 (if addr then 240 write_reg <|proc:=0|> n (base + length) 241 else 242 write_reg <|proc:=0|> n (base ��� length))) >>= 243 (��(u1,u2,u3). return ()))))) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar) 244 = 245 (preserve_relation_mmu 246 ((read_reg <|proc:=0|> n ||| read_cpsr <|proc:=0|>) >>= 247 (��(base,cpsr). 248 (let mode = if system then 16w else 16w and 249 length = n2w (4 * bit_count registers) and 250 lowest = lowest_set_bit registers 251 in 252 let base_address = if addr then base else base ��� length 253 in 254 let start_address = 255 if indx ��� addr then 256 base_address + 4w 257 else 258 base_address 259 in 260 let address i = 261 start_address + 262 n2w (4 * (bit_count_upto (i + 1) registers ��� 1)) 263 in 264 forT 0 14 265 (��i. 266 condT ((registers:word16) ' i) 267 (if (i = w2n n) ��� wback ��� i ��� lowest then 268 write_memA <|proc:=0|> (address i,4) BITS32_UNKNOWN 269 else 270 read_reg_mode <|proc:=0|> (n2w i,mode) >>= 271 (��d. 272 write_memA <|proc:=0|> (address i,4) 273 (bytes (d,4))))) >>= 274 (��unit_list. 275 (condT (registers ' 15) 276 (pc_store_value <|proc:=0|> >>= 277 (��pc. 278 write_memA <|proc:=0|> (address 15,4) 279 (bytes (pc,4)))) ||| increment_pc <|proc:=0|> enc 280 ||| condT wback 281 (if addr then 282 write_reg <|proc:=0|> n (base + length) 283 else 284 write_reg <|proc:=0|> n (base ��� length))) >>= 285 (��(u1,u2,u3). return ()))))) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar)``, 286 FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def, assert_mode_def, ARM_MODE_def, ARM_READ_CPSR_def] 287 THEN EQ_TAC 288 THEN (REPEAT STRIP_TAC) 289 THEN ASSUME_TAC (SPECL [``s1:arm_state``, ``n:word4``, store_multiple_part] (INST_TYPE [alpha |-> type_of(``()``)] read_reg_read_cpsr_par_effect_lem)) 290 THEN ASSUME_TAC (SPECL [``s2:arm_state``, ``n:word4``, store_multiple_part] (INST_TYPE [alpha |-> type_of(``()``)] read_reg_read_cpsr_par_effect_lem)) 291 THEN RES_TAC 292 THEN UNDISCH_ALL_TAC 293 THEN RW_TAC (srw_ss()) []); 294 295 296 297 298val _ = g `!n. preserve_relation_mmu 299 ((read_reg <|proc := 0|> n ||| read_cpsr <|proc := 0|>) >>= 300 (��(base,cpsr). 301 forT 0 14 302 (��i. 303 condT ((c0:word16) ' i) 304 (if (i = (w2n n)) ��� b2 ��� i ��� lowest_set_bit c0 then 305 write_memA <|proc := 0|> 306 (n2w (4 * (bit_count_upto (w2n n + 1) c0 ��� 1)) + 307 if b ��� b0 then 308 (if b0 then 309 base 310 else 311 base + -1w * n2w (4 * bit_count c0)) + 4w 312 else if b0 then 313 base 314 else 315 base + -1w * n2w (4 * bit_count c0),4) 316 BITS32_UNKNOWN 317 else 318 read_reg_mode <|proc := 0|> 319 (n2w i,if b1 then 16w else cpsr.M) >>= 320 (��d. 321 write_memA <|proc := 0|> 322 (n2w (4 * (bit_count_upto (i + 1) c0 ��� 1)) + 323 if b ��� b0 then 324 (if b0 then 325 base 326 else 327 base + -1w * n2w (4 * bit_count c0)) + 328 4w 329 else if b0 then 330 base 331 else 332 base + -1w * n2w (4 * bit_count c0),4) 333 (bytes (d,4))))) >>= 334 (��unit_list. 335 (condT (c0 ' 15) 336 (pc_store_value <|proc := 0|> >>= 337 (��pc. 338 write_memA <|proc := 0|> 339 (n2w (4 * (bit_count_upto 16 c0 ��� 1)) + 340 if b ��� b0 then 341 (if b0 then 342 base 343 else 344 base + -1w * n2w (4 * bit_count c0)) + 4w 345 else if b0 then 346 base 347 else 348 base + -1w * n2w (4 * bit_count c0),4) 349 (bytes (pc,4)))) 350 ||| increment_pc <|proc := 0|> enc 351 ||| condT b2 352 (if b0 then 353 write_reg <|proc := 0|> n 354 (base + n2w (4 * bit_count c0)) 355 else 356 write_reg <|proc := 0|> n 357 (base + -1w * n2w (4 * bit_count c0)))) >>= 358 (��(u1,u2,u3). return ())))) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar`; 359val _ = e(STRIP_TAC); 360val _ = e(ASSUME_TAC (SPECL [``b2:bool``, ``b1:bool``, ``c0:word16``, ``n:word4``, ``b:bool``, ``enc:Encoding``, ``b0:bool``] (GEN_ALL store_multiple_part_simp))); 361val _ = e(FULL_SIMP_TAC (srw_ss()) [LET_DEF]); 362val _ = go_on 1; 363val store_multiple_part_thm = save_thm ("store_multiple_part_thm", top_thm()); 364val store_multiple_part_thm_n = save_thm ("store_multiple_part_thm_n", (SPEC ``n:word4`` store_multiple_part_thm)); 365val store_multiple_part_thm_13 = save_thm ("store_multiple_part_thm_13", (SIMP_RULE (srw_ss()) [] (SPEC ``13w:word4`` store_multiple_part_thm))); 366val store_multiple_part_thm_15 = save_thm ("store_multiple_part_thm_15", (SIMP_RULE (srw_ss()) [] (SPEC ``15w:word4`` store_multiple_part_thm))); 367 368val _ = add_to_simplist store_multiple_part_thm; 369val _ = add_to_simplist store_multiple_part_thm_n; 370val _ = add_to_simplist store_multiple_part_thm_13; 371val _ = add_to_simplist store_multiple_part_thm_15; 372 373 374val load_multiple_part = 375 ``(��(base,cpsr). 376 forT 0 14 377 (��i. 378 condT (c0 ' i) 379 (read_memA <|proc := 0|> 380 (n2w (4 * (bit_count_upto (i + 1) c0 ��� 1)) + 381 if b ��� b0 then 382 (if b0 then 383 base 384 else 385 base + -1w * n2w (4 * bit_count c0)) + 4w 386 else if b0 then 387 base 388 else 389 base + -1w * n2w (4 * bit_count c0),4) >>= 390 (��d. 391 write_reg_mode <|proc := 0|> 392 (n2w i,if b1 ��� ��c0 ' 15 then 16w else cpsr.M) 393 (word32 d)))) >>= 394 (��unit_list. 395 condT b2 396 (if (��(c0:word16) ' (w2n n)) then 397 if b0 then 398 write_reg <|proc := 0|> n 399 (base + n2w (4 * bit_count c0)) 400 else 401 write_reg <|proc := 0|> n 402 (base + -1w * n2w (4 * bit_count c0)) 403 else 404 write_reg <|proc := 0|> n UNKNOWN) >>= 405 (��u. 406 if c0 ' 15 then 407 read_memA <|proc := 0|> 408 (n2w (4 * (bit_count_upto 16 c0 ��� 1)) + 409 if b ��� b0 then 410 (if b0 then 411 base 412 else 413 base + -1w * n2w (4 * bit_count c0)) + 4w 414 else if b0 then 415 base 416 else 417 base + -1w * n2w (4 * bit_count c0),4) >>= 418 (��d. 419 if b1 then 420 current_mode_is_user_or_system <|proc := 0|> >>= 421 (��is_user_or_system. 422 if is_user_or_system then 423 errorT "load_multiple_instr: unpredictable" 424 else 425 read_spsr <|proc := 0|> >>= 426 (��spsr. 427 cpsr_write_by_instr <|proc := 0|> 428 (encode_psr spsr,15w,T) >>= 429 (��u. 430 branch_write_pc <|proc := 0|> 431 (word32 d)))) 432 else 433 load_write_pc <|proc := 0|> (word32 d)) 434 else 435 increment_pc <|proc := 0|> enc))):(word32 # ARMpsr -> unit M)``; 436 437 438val _ = g `!n. preserve_relation_mmu 439 ((read_reg <|proc := 0|> n ||| read_cpsr <|proc := 0|>) >>= (^load_multiple_part)) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar`; 440val _ = e(STRIP_TAC); 441val _ = e(ASSUME_TAC (SPECL [``n:word4``, load_multiple_part, ``(assert_mode 16w)``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:unit`] cpsr_par_simp_rel_lem))); 442val _ = e(FULL_SIMP_TAC (srw_ss()) []); 443val _ = go_on 1; 444val load_multiple_part_thm = top_thm(); 445val load_multiple_part_thm_13 = save_thm ("load_multiple_part_thm_13", (SIMP_RULE (srw_ss()) [] (SPEC ``13w:word4`` load_multiple_part_thm))); 446val load_multiple_part_thm_15 = save_thm ("load_multiple_part_thm_15", (SIMP_RULE (srw_ss()) [] (SPEC ``15w:word4`` load_multiple_part_thm))); 447val _ = add_to_simplist load_multiple_part_thm; 448val _ = add_to_simplist load_multiple_part_thm_13; 449val _ = add_to_simplist load_multiple_part_thm_15; 450 451 452 453 454val _ = g `preserve_relation_mmu (load_store_instruction <|proc:=0|> (enc,inst))(assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 455val _ = e(FULL_SIMP_TAC (srw_ss()) [load_store_instruction_def]); 456val _ = e(Cases_on `inst` THEN FULL_SIMP_TAC (srw_ss()) []); 457(* load *) 458val _ = go_on_p 1; 459(* store *) 460val _ = go_on_p 1; 461(* load halfword *) 462val _ = go_on_p 1; 463(* store halfword *) 464val _ = go_on_p 1; 465(* load dual *) 466val _ = go_on_p 1; 467(* store dual *) 468val _ = go_on_p 1; 469(* load multiple *) 470val _ = go_on_p 1; 471(* store multiple *) 472val _ = go_on_p 1; 473(* load exclusive *) 474val _ = go_on_p 1; 475(* store exclusive *) 476val _ = go_on_p 1; 477(* load exclusive doubleword *) 478val _ = go_on_p 1; 479(* store exclusive doubleword *) 480val _ = go_on_p 1; 481(* load exclusive halfword *) 482val _ = go_on_p 1; 483(* store exclusive halfword *) 484val _ = go_on_p 1; 485(* load exclusive byte *) 486val _ = go_on_p 1; 487(* store exclusive byte *) 488val _ = go_on_p 1; 489(* store return state *) 490val _ = e(FULL_SIMP_TAC (srw_ss()) [store_return_state_instr_def, instruction_def, run_instruction_def, LET_DEF]); 491val _ = go_on_p 1; 492(* return from exception *) 493val _ = go_on_p 1; 494val load_store_instruction_comb_thm = save_comb_thm("load_store_instruction_comb_thm", top_thm(), ``load_store_instruction``); 495 496 497 498 499(************************************************************) 500(******************* D. Coprocessors *********************) 501(************************************************************) 502 503 504val _ = g `preserve_relation_mmu (coprocessor_instruction <|proc:=0|> (enc,cond,inst)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 505val _ = e(FULL_SIMP_TAC (srw_ss()) [coprocessor_instruction_def]); 506val _ = e((REPEAT (CASE_TAC)) THEN FULL_SIMP_TAC (srw_ss()) [coprocessor_load_instr_def, coprocessor_store_instr_def, coprocessor_register_to_arm_instr_def, arm_register_to_coprocessor_instr_def, coprocessor_register_to_arm_two_instr_def, arm_register_to_coprocessor_two_instr_def, coprocessor_data_processing_instr_def, LET_DEF]); 507val _ = go_on_p 7; 508val coprocessor_instruction_comb_thm = save_comb_thm("coprocessor_instruction_comb_thm", top_thm(), ``coprocessor_instruction``); 509 510 511 512(************************************************************) 513(****************** E. Data Processing ********************) 514(************************************************************) 515 516(* write flags for triples *) 517 518val _ = g `preserve_relation_mmu (write_flags <|proc := 0|> (a,b,c)) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar`; 519val _ = e(pairLib.PairCases_on `c`); 520val _ = go_on 1; 521val write_flags_triple_thm = top_thm(); 522val _ = add_to_simplist write_flags_triple_thm; 523 524(* data processing instr *) 525 526val data_processing_pre_part = ``((if ((c:word4) = 13w) ��� (c = 15w) ��� (enc ��� Encoding_Thumb2 ��� (c0 = 15w)) then 527 return 0w 528 else 529 read_reg <|proc := 0|> c0) 530 ||| address_mode1 <|proc := 0|> (enc = Encoding_Thumb2) a 531 ||| read_flags <|proc := 0|>) 532 : ((word32 # (word32 # bool) # bool # bool #bool # bool) M)``; 533val data_processing_pre_part_thm = prove_and_save_e(``^data_processing_pre_part``, "data_processing_pre_part_thm"); 534 535 536val data_processing_core_part = ``(��((rn :bool[32]),((shifted :bool[32]),(C_shift :bool)),(N :bool), 537 (Z :bool),(C :bool),(V :bool)). 538 ((if ((3 :num) -- (2 :num)) (c :bool[4]) = (2w :bool[4]) then 539 increment_pc <|proc := (0 :num)|> enc 540 else if (c1 :bool[4]) = (15w :bool[4]) then 541 if (b :bool) then 542 read_spsr <|proc := (0 :num)|> >>= 543 (��(spsr :ARMpsr). 544 cpsr_write_by_instr <|proc := (0 :num)|> 545 (encode_psr spsr,(15w :bool[4]),T) >>= 546 (��(u :unit). 547 branch_write_pc <|proc := (0 :num)|> 548 (FST (data_processing_alu c rn shifted C)))) 549 else 550 alu_write_pc <|proc := (0 :num)|> 551 (FST (data_processing_alu c rn shifted C)) 552 else 553 (increment_pc <|proc := (0 :num)|> enc 554 ||| write_reg <|proc := (0 :num)|> c1 555 (FST (data_processing_alu c rn shifted C))) >>= 556 (��((u1 :unit),(u2 :unit)). return ())) 557 ||| if 558 b ��� 559 (c1 ��� (15w :bool[4]) ��� 560 (((3 :num) -- (2 :num)) c = (2w :bool[4]))) 561 then 562 if 563 (c ' (2 :num) ��� c ' (1 :num)) ��� 564 (��c ' (3 :num) ��� ��c ' (2 :num)) 565 then 566 write_flags <|proc := (0 :num)|> 567 (word_msb (FST (data_processing_alu c rn shifted C)), 568 FST (data_processing_alu c rn shifted C) = 569 (0w 570 :bool[32]), 571 SND (data_processing_alu c rn shifted C)) 572 else 573 write_flags <|proc := (0 :num)|> 574 (word_msb (FST (data_processing_alu c rn shifted C)), 575 FST (data_processing_alu c rn shifted C) = 576 (0w 577 :bool[32]),C_shift,V) 578 else 579 return ()) >>= (��((u1 :unit),(u2 :unit)). return ())):(word32 # (word32 # bool) # bool # bool #bool # bool -> unit M)``; 580 581val _ = g `���y. preserve_relation_mmu(^data_processing_core_part y) (assert_mode 16w) (assert_mode 16w) priv_mode_constraints priv_mode_similar`; 582val _ = e(STRIP_TAC); 583val _ = e(pairLib.PairCases_on `y`); 584val _ = e(FULL_SIMP_TAC (srw_ss()) []); 585val _ = go_on 1; 586val data_processing_core_part_thm1 = top_thm(); 587val data_processing_core_part_thm2 = SIMP_RULE (srw_ss()) [(SPECL [data_processing_core_part, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``] (INST_TYPE [alpha |-> (Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`), beta |-> type_of (``()``)] second_abs_lemma))] data_processing_core_part_thm1; 588val _ = add_to_simplist data_processing_core_part_thm1; 589val _ = add_to_simplist data_processing_core_part_thm2; 590 591 592val _ = g `preserve_relation_mmu ((^data_processing_pre_part) >>= (^data_processing_core_part)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 593val _ = e(FULL_SIMP_TAC (srw_ss()) [seqT_preserves_relation_uu_thm, comb_monot_thm, data_processing_core_part_thm2, data_processing_pre_part_thm, trans_priv_mode_constraints_thm]); 594val _ = e(ASSUME_TAC data_processing_core_part_thm2); 595val _ = e(ASSUME_TAC data_processing_pre_part_thm); 596val _ = e(ASSUME_TAC (SPEC ``(assert_mode 16w):(arm_state->bool)`` comb_monot_thm)); 597val _ = e(ASSUME_TAC (SPECL [data_processing_pre_part, data_processing_core_part,``16w:word5``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`, beta |-> type_of (``()``)] seqT_preserves_relation_uu_thm))); 598val _ = e(FULL_SIMP_TAC (srw_ss()) [preserve_relation_comb_16_27_thm, trans_priv_mode_constraints_thm]); 599val data_processing_help_thm = top_thm(); 600val _ = add_to_simplist data_processing_help_thm; 601 602(* multiply long - write flags - part *) 603 604val multiply_long_instr_part_thm = store_thm( 605 "multiply_long_instr_part_thm", 606 ``preserve_relation_mmu 607 ((��(C_flag,V_flag). 608 write_flags <|proc := 0|> 609 (word_msb 610 ((if b then (sw2sw (rm:word32):word64) * (sw2sw (rn:word32):word64) else w2w rm * w2w rn) + 611 if b0 then rdhi @@ rdlo else 0w), 612 (if b then (sw2sw rm :word64) * sw2sw rn else w2w rm * w2w rn) + 613 (if b0 then (rdhi:word32) @@ (rdlo:word32) else (0w:word64)) = 614 0w,C_flag,V_flag)) 615 (if (version:num) = 4 then (UNKNOWN,UNKNOWN) else (C,V))) 616 (assert_mode 16w) (assert_mode 16w) priv_mode_constraints 617 priv_mode_similar``, 618 RW_TAC (srw_ss()) [(GEN_ALL write_flags_thm)]); 619val _ = add_to_simplist multiply_long_instr_part_thm; 620 621(* instructions *) 622 623val _ = g `preserve_relation_mmu (data_processing_instruction <|proc := 0|> (enc,inst)) (assert_mode 16w) (comb_mode 16w 27w) priv_mode_constraints priv_mode_similar`; 624val _ = e (Cases_on `inst` THEN FULL_SIMP_TAC (srw_ss()) []); 625(*30 subgoals *) 626(* data processing *) 627val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, data_processing_instr, LET_DEF] THEN PairedLambda.GEN_BETA_TAC); 628val _ = e(Q.ABBREV_TAC `xx = (shifted, C_shift)`); 629val _ = go_on_p 1; 630(* add sub *) 631val _ = go_on_p 1; 632(* move halfword *) 633val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 634val _ = go_on_p 4; 635(* multiply*) 636val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 637val _ = go_on_p 4; 638(* multiply subtract *) 639val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 640val _ = go_on_p 4; 641(* signed halword multiply *) 642val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def]); 643val _ = e(Cases_on `enc` THEN Cases_on `c=0w` THEN Cases_on `c=1w` THEN Cases_on `b0` THEN Cases_on `c=2w` THEN FULL_SIMP_TAC (srw_ss()) []); 644val _ = go_on_p 32; 645(* signed multiply dual *) 646val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 647val _ = go_on_p 4; 648(* signed multiply long dual *) 649val _ = go_on_p 1; 650(* signed most significant multiply *) 651val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 652val _ = go_on_p 4; 653(* signed most significant multiply subtract *) 654val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 655val _ = go_on_p 4; 656(* multiply long *) 657val _ = go_on_p 1; 658(* multiply accumulate accumulate *) 659val _ = go_on_p 1; 660(* saturate *) 661val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, saturate_instr, LET_DEF] THEN REPEAT CASE_TAC THEN PairedLambda.GEN_BETA_TAC); 662val _ = go_on_p 8; 663(* saturate 16 *) 664val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, saturate_16_instr, LET_DEF] THEN REPEAT CASE_TAC THEN PairedLambda.GEN_BETA_TAC); 665val _ = go_on_p 8; 666(* saturating add subtract *) 667val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, saturating_add_subtract_instr, LET_DEF] THEN Cases_on `enc` THEN PairedLambda.GEN_BETA_TAC THEN FULL_SIMP_TAC (srw_ss()) []); 668val _ = go_on_p 4; 669(* pack halfword *) 670val _ = e (FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, pack_halfword_instr_def]); 671val _ = e (Cases_on `decode_imm_shift ((1 :+ b) 0w,c1)` THEN FULL_SIMP_TAC (srw_ss()) []); 672val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 673val _ = go_on_p 4; 674(* extend byte *) 675val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 676val _ = go_on_p 4; 677(* extend_byte_16 *) 678val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 679val _ = go_on_p 4; 680(* extend halword *) 681val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 682val _ = go_on_p 4; 683(* bit field clear insert *) 684val _ = go_on_p 1; 685(* count leading zeroes *) 686val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 687val _ = go_on_p 4; 688(* reverse bits *) 689val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 690val _ = go_on_p 4; 691(* byte reverse word *) 692val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 693val _ = go_on_p 4; 694(* byte reverse packed halfword *) 695val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 696val _ = go_on_p 4; 697(* byte reverse signed halword *) 698val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 699val _ = go_on_p 4; 700(* bit field extract *) 701val _ = go_on_p 1; 702(* select bytes *) 703val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 704val _ = go_on_p 4; 705(* unsigned sum absolute differences *) 706val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) []); 707val _ = go_on_p 4; 708(* parallel add subtract *) 709val _ = e(Cases_on `enc` THEN FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_def, parallel_add_subtract_instr, LET_DEF] THEN PairedLambda.GEN_BETA_TAC THEN FULL_SIMP_TAC (srw_ss()) []); 710val _ = go_on_p 4; 711(* divide *) 712val _ = go_on_p 1; 713(* now save *) 714val data_processing_instruction_comb_thm = save_comb_thm("data_processing_instruction_comb_thm", top_thm(), ``data_processing_instruction``); 715 716 717 718(************************************************************) 719(********************** F. Misc ***********************) 720(************************************************************) 721 722 723 724 725val read_info_constlem = store_thm( 726 "read_info_constlem", 727 ``!s. ?x. ((read_info <|proc:=0|>) s) = ValueState x s``, 728 RW_TAC (srw_ss()) [read_info_def, readT_def]); 729 730 731val read_info_thm = prove_and_save_s(``read_info <|proc:=0|>``, "read_info_thm"); 732 733 734val _ = g `preserve_relation_mmu (miscellaneous_instruction <|proc:=0|> (enc,inst)) (assert_mode 16w) mode_mix priv_mode_constraints_v2a priv_mode_similar`; 735val _ = e(FULL_SIMP_TAC (srw_ss()) [miscellaneous_instruction_def]); 736val _ = e(REPEAT (CASE_TAC THEN FULL_SIMP_TAC (srw_ss()) [])); 737(* NOP *) 738val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 739val _ = go_on_p 1; 740(* yield *) 741val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 742val _ = e(Cases_on `enc = Encoding_ARM` THEN FULL_SIMP_TAC (srw_ss()) [yield_instr, hint_yield_def]); 743val _ = go_on_p 2; 744(* wait for event *) 745val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 746val _ = e(Cases_on `enc = Encoding_ARM` THEN FULL_SIMP_TAC (srw_ss()) [wait_for_event_instr_def, instruction_def, run_instruction_def]); 747val _ = go_on_p 2; 748(* wait for interrupt *) 749val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 750val _ = e(Cases_on `enc = Encoding_ARM` THEN FULL_SIMP_TAC (srw_ss()) [wait_for_interrupt_instr_def, instruction_def, run_instruction_def]); 751val _ = go_on_p 2; 752(* send event *) 753val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 754val _ = e(Cases_on `enc = Encoding_ARM` THEN FULL_SIMP_TAC (srw_ss()) [send_event_instr_def, instruction_def, run_instruction_def]); 755val _ = go_on_p 2; 756(* debug *) 757val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 758val _ = e(Cases_on `enc = Encoding_ARM` THEN FULL_SIMP_TAC (srw_ss()) [debug_instr_def, instruction_def, run_instruction_def]); 759val _ = go_on_p 2; 760(* breakpoint *) 761val _ = e(MODE_MIX_TAC ``little_mode_mix``); 762val _ = e(FULL_SIMP_TAC (srw_ss()) [breakpoint_instr]); 763val _ = e(SUBGOAL_THEN ``!info. preserve_relation_mmu (if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>) (assert_mode 16w) little_mode_mix priv_mode_constraints_v1 priv_mode_similar`` 764 (fn th => ASSUME_TAC th 765 THEN ASSUME_TAC (SPEC ``(��info. if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>)`` (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] second_abs_lemma)) 766 THEN ASSUME_TAC trans_priv_mode_constraints_thm 767 THEN ASSUME_TAC (SPECL [``(read_info <|proc:=0|>):(ARMinfo M)``, ``( \info. (if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>))``, ``16w:word5``, ``little_mode_mix``, ``little_mode_mix``, ``priv_mode_constraints_v1``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] seqT_preserves_relation_comb_thm)) 768 THEN FULL_SIMP_TAC (srw_ss()) [little_mode_mix_comb_16_thm, (CONJUNCT1 (CONJUNCT2 (CONJUNCT2 read_info_thm)))])); 769val _ = e(STRIP_TAC); 770val _ = e(CASE_TAC); 771val _ = e(LITTLE_MODE_MIX_TAC ``comb_mode 16w 27w``); 772val _ = e(FULL_SIMP_TAC (srw_ss()) [take_undef_instr_exception_comb_thm]); 773val _ = e(LITTLE_MODE_MIX_TAC ``comb_mode 16w 23w``); 774val _ = e(FULL_SIMP_TAC (srw_ss()) [take_prefetch_abort_exception_comb_thm]); 775(* data memory barrier *) 776val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 777val _ = go_on_p 1; 778(* data synch barrier *) 779val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 780val _ = go_on_p 1; 781(* inst synch barrier *) 782val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 783val _ = go_on_p 1; 784(* swap *) 785val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 786val _ = go_on_p 1; 787(* preload data *) 788val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 789val _ = go_on_p 1; 790(* preload instr *) 791val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 792val _ = go_on_p 1; 793(* svc *) 794val _ = e(MODE_MIX_TAC ``comb_mode 16w 19w``); 795val _ = e(FULL_SIMP_TAC (srw_ss()) [take_svc_exception_comb_thm]); 796(* secure monitor call *) 797val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 798val _ = go_on_p 1; 799(* enter x leave x *) 800val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 801val _ = go_on_p 1; 802(* clear exclusive *) 803val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 804val _ = e(FULL_SIMP_TAC (srw_ss()) [clear_exclusive_instr_def, clear_exclusive_local_def, LET_DEF]); 805val _ = go_on_p 1; 806(* if-then *) 807val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 808val _ = go_on_p 1; 809val miscellaneous_instruction_comb_thm = save_comb_thm("miscellaneous_instruction_comb_thm", top_thm(), ``miscellaneous_instruction``); 810 811 812 813(************************************************************) 814(******************** G. arm_instr *********************) 815(************************************************************) 816 817 818val IT_advance_constlem = store_thm( 819 "IT_advance_constlem", 820 ``((s.psrs(0,CPSR)).IT = 0w) ==> (((IT_advance <|proc :=0|>) s) = (ValueState () s))``, 821 EVAL_TAC 822 THEN RW_TAC (srw_ss()) [] 823 THENL [`!(x:unit). x = ()` by (Cases_on `x` THEN EVAL_TAC) 824 THEN SPEC_ASSUM_TAC (``!x. X``, [``ARB:unit``]) 825 THEN FULL_SIMP_TAC (srw_ss()) [], 826 ALL_TAC, 827 ALL_TAC] 828 THEN UNDISCH_ALL_TAC 829 THEN EVAL_TAC 830 THEN RW_TAC (srw_ss()) [] 831 THEN Cases_on `s` 832 THEN FULL_SIMP_TAC (srw_ss()) [arm_state_psrs_fupd] 833 THEN ASSUME_TAC (SPEC ``f0:num#PSRName->ARMpsr`` (GEN_ALL psrs_update_in_update_thm)) 834 THEN Q.ABBREV_TAC `x = (f0 (0,CPSR)).IT` 835 THEN RW_TAC (srw_ss()) [arm_state_psrs_fupd]); 836 837val condition_passed_constlem = store_thm( 838 "condition_passed_constlem", 839 ``!s cond. ?x. (condition_passed <|proc:=0|> cond) s = ValueState x s``, 840 EVAL_TAC THEN RW_TAC (srw_ss()) [] THEN RW_TAC (srw_ss()) []); 841 842val condition_passed_similar_lem = store_thm( 843 "condition_passed_similar_lem", 844 ``!s1 s2 cond. (similar g s1 s2) ==> (?pass. (((condition_passed <|proc:=0|> cond) s1 = ValueState pass s1) /\ ((condition_passed <|proc:=0|> cond) s2 = ValueState pass s2)))``, 845 RW_TAC (srw_ss()) [] 846 THEN IMP_RES_TAC similarity_implies_equal_av_thm 847 THEN UNDISCH_TAC ``similar g s1 s2`` 848 THEN EVAL_TAC THEN RW_TAC (srw_ss()) [] THEN RW_TAC (srw_ss()) []); 849 850 851val arm_instr_core_def = Define `arm_instr_core ii (pass:bool) (enc:Encoding) (cond:word4) (inst:ARMinstruction) = 852 if pass then 853 case inst of 854 Unpredictable => errorT "decode: unpredictable" 855 | Undefined => take_undef_instr_exception ii 856 | Branch b => branch_instruction ii (enc,b) 857 | DataProcessing d => data_processing_instruction ii (enc,d) 858 | StatusAccess s => status_access_instruction ii (enc,s) 859 | LoadStore l => load_store_instruction ii (enc,l) 860 | Miscellaneous m => miscellaneous_instruction ii (enc,m) 861 | Coprocessor c => coprocessor_instruction ii (enc,cond,c) 862 else 863 increment_pc ii enc`; 864 865 866 867val _ = g `preserve_relation_mmu (arm_instr_core <|proc:=0|> pass enc cond inst) (assert_mode 16w) mode_mix priv_mode_constraints_v2a priv_mode_similar`; 868val _ = e(RW_TAC (srw_ss()) [arm_instr_core_def]); 869val _ = e(CASE_TAC); 870(* 8 cases *) 871(* error *) 872val _ = e(MODE_MIX_TAC ``assert_mode 16w``); 873val _ = go_on 1; 874(* take undef instr exception *) 875val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 876val _ = e(FULL_SIMP_TAC (srw_ss()) [take_undef_instr_exception_comb_thm]); 877(* branch instruction *) 878val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 879val _ = e(FULL_SIMP_TAC (srw_ss()) [branch_instruction_comb_thm]); 880(* data processing instruction *) 881val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 882val _ = e(FULL_SIMP_TAC (srw_ss()) [data_processing_instruction_comb_thm]); 883(* status access instruction *) 884val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 885val _ = e(FULL_SIMP_TAC (srw_ss()) [status_access_instruction_comb_thm]); 886(* load store instruction *) 887val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 888val _ = e(FULL_SIMP_TAC (srw_ss()) [load_store_instruction_comb_thm]); 889(* misc instruction *) 890val _ = e(FULL_SIMP_TAC (srw_ss()) [miscellaneous_instruction_comb_thm]); 891(* coprocessor instruction *) 892val _ = e(MODE_MIX_TAC ``comb_mode 16w 27w``); 893val _ = e(FULL_SIMP_TAC (srw_ss()) [coprocessor_instruction_comb_thm]); 894(* increment PC *) 895val _ = e(MODE_MIX_TAC ``assert_mode 16w``); 896val _ = e(FULL_SIMP_TAC (srw_ss()) [increment_pc_thm]); 897val arm_instr_core_comb_thm = save_comb_thm("arm_instr_core_comb_thm", top_thm(), ``arm_instr_core``); 898 899 900val arm_instr_alternative_def = store_thm( 901 "arm_instr_alternative_def", 902 ``arm_instr ii (enc,cond,inst) = 903 (condition_passed ii cond >>= 904 (��pass. 905 arm_instr_core ii pass enc cond inst)) >>= 906 (��u. 907 condT 908 (case inst of 909 Unpredictable => T 910 | Undefined => T 911 | Branch v6 => T 912 | DataProcessing v7 => T 913 | StatusAccess v8 => T 914 | LoadStore v9 => T 915 | Miscellaneous (Hint v33) => T 916 | Miscellaneous (Breakpoint v34) => T 917 | Miscellaneous (Data_Memory_Barrier v35) => T 918 | Miscellaneous (Data_Synchronization_Barrier v36) => T 919 | Miscellaneous (Instruction_Synchronization_Barrier v37) => 920 T 921 | Miscellaneous (Swap v38 v39 v40 v41) => T 922 | Miscellaneous (Preload_Data v42 v43 v44 v45) => T 923 | Miscellaneous (Preload_Instruction v46 v47 v48) => T 924 | Miscellaneous (Supervisor_Call v49) => T 925 | Miscellaneous (Secure_Monitor_Call v50) => T 926 | Miscellaneous (Enterx_Leavex v51) => T 927 | Miscellaneous Clear_Exclusive => T 928 | Miscellaneous (If_Then v52 v53) => F 929 | Coprocessor v11 => T) (IT_advance ii))``, 930 RW_TAC (srw_ss()) [arm_instr_core_def, arm_instr_def]); 931 932 933val arm_instr_comb_thm = store_thm("arm_instr_comb_thm", 934 ``preserve_relation_mmu (arm_instr <|proc:=0|> (enc, cond, inst)) (assert_mode 16w) mode_mix priv_mode_constraints_v2a priv_mode_similar``, 935 RW_TAC (srw_ss()) [arm_instr_alternative_def, preserve_relation_mmu_def, seqT_def, condT_def] 936 THEN (ASSUME_TAC (SPECL [``s1:arm_state``, ``s2:arm_state``, ``cond:word4``] condition_passed_similar_lem) 937 THEN NTAC 2 (UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) [untouched_refl]) 938 THEN ASSUME_TAC reflex_priv_mode_constraints_v2a_thm 939 THEN IMP_RES_TAC reflexive_comp_def 940 THEN UNDISCH_ALL_TAC 941 THEN RW_TAC (srw_ss()) [] 942 THENL [FULL_SIMP_TAC (srw_ss()) [mode_mix_def, assert_mode_def], 943 FULL_SIMP_TAC (srw_ss()) [mode_mix_def, assert_mode_def], 944 IMP_RES_TAC similarity_implies_equal_av_thm, 945 IMP_RES_TAC similarity_implies_equal_av_thm, 946 ALL_TAC] 947 THEN Cases_on `arm_instr_core <|proc := 0|> pass enc cond inst s2` 948 THEN ASSUME_TAC arm_instr_core_comb_thm 949 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def] 950 THEN UNDISCH_ALL_TAC 951 THEN RW_TAC (srw_ss()) [] 952 THEN SPEC_ASSUM_TAC (``!g s1 s2. X``, [``g:word32``, ``s1:arm_state``, ``s2:arm_state``]) 953 THEN UNDISCH_ALL_TAC 954 THEN RW_TAC (srw_ss()) [constT_def] 955 THEN IMP_RES_TAC similarity_implies_equal_av_thm 956 THEN UNDISCH_ALL_TAC 957 THEN RW_TAC (srw_ss()) [] 958 THEN Cases_on `ARM_MODE s1' = 16w` 959 THEN IMP_RES_TAC similarity_implies_equal_av_thm 960 THEN IMP_RES_TAC similarity_implies_equal_mode_thm 961 THEN FULL_SIMP_TAC (srw_ss()) []) 962 THENL [ASSUME_TAC (CONJUNCT1 (CONJUNCT2 IT_advance_thm)) 963 THEN FULL_SIMP_TAC (srw_ss()) [preserve_relation_mmu_def, assert_mode_def, priv_mode_constraints_v2a_def] 964 THEN SPEC_ASSUM_TAC (``!g s1 s2. X``, [``g:word32``, ``s1':arm_state``, ``b:arm_state``]) 965 THEN IMP_RES_TAC untouched_mmu_setup_lem 966 THEN (NTAC 2 ((`(ARM_MODE s1' = 16w) /\ (ARM_MODE b = 16w)` by FULL_SIMP_TAC (srw_ss()) []) 967 THEN FULL_SIMP_TAC (srw_ss()) [] 968 THEN RES_TAC 969 THEN FULL_SIMP_TAC (srw_ss()) [])) 970 THEN METIS_TAC [untouched_trans, trans_priv_mode_constraints_thm, trans_fun_def, mode_mix_def], 971 `((s1'.psrs (0,CPSR)).IT = 0w) /\ ((b.psrs (0,CPSR)).IT = 0w)` by FULL_SIMP_TAC (srw_ss()) [priv_mode_constraints_v2a_def, priv_mode_constraints_v1_def, LET_DEF] 972 THEN IMP_RES_TAC IT_advance_constlem 973 THEN UNDISCH_ALL_TAC THEN RW_TAC (srw_ss()) []]); 974 975 976 977val _ = export_theory(); 978