1(* ========================================================================= *) 2(* FILE : interruptsScript.sml *) 3(* DESCRIPTION : A collection of lemmas about exception/interrupt handling *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2004-2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["pred_setSimps", "io_onestepTheory", "armLib", "wordsLib", 11 "armTheory", "coreTheory", "lemmasTheory"]; 12*) 13 14open HolKernel boolLib bossLib; 15open Q arithmeticTheory wordsLib; 16open io_onestepTheory wordsTheory armTheory coreTheory lemmasTheory; 17 18val _ = new_theory "interrupts"; 19val _ = ParseExtras.temp_loose_equality() 20(* ------------------------------------------------------------------------- *) 21 22infix \\ 23val op \\ = op THEN; 24 25val std_ss = std_ss ++ boolSimps.LET_ss; 26val arith_ss = arith_ss ++ boolSimps.LET_ss; 27val ICLASS_ss = armLib.ICLASS_ss; 28val SIZES_ss = wordsLib.SIZES_ss; 29 30val ERR = mk_HOL_ERR "interrupts" 31 32fun Cases_on_arm6inp tm = FULL_STRUCT_CASES_TAC (SPEC tm arm6inp_nchotomy); 33fun Cases_arm6 (g as (_,w)) = 34 let val (Bvar,_) = with_exn dest_forall w (ERR "Cases_arm6" "not a forall") 35 in (GEN_TAC \\ FULL_STRUCT_CASES_TAC (Thm.SPEC Bvar arm6_nchotomy)) g 36 end 37 handle e => raise wrap_exn "Lemmas" "Cases_arm6" e; 38 39(* ------------------------------------------------------------------------- *) 40 41val EXISTS_LEAST_NOT_RESET = prove( 42 `!t i. i IN STRM_ARM6 /\ IS_RESET i t ==> 43 ?t2. IS_RESET i t2 /\ ~IS_RESET i (t2 + 1) /\ ~IS_RESET i (t2 + 2)`, 44 RW_TAC bool_ss [IN_DEF,STRM_ARM6_def] 45 \\ PAT_X_ASSUM `!t. ?t2. t < t2 /\ (IS_BUSY i t2 ==> IS_ABSENT i t2)` 46 (K ALL_TAC) 47 \\ FIRST_X_ASSUM (SPEC_THEN `t` 48 (STRIP_ASSUME_TAC o CONV_RULE numLib.EXISTS_LEAST_CONV)) 49 \\ POP_ASSUM (SPEC_THEN `t2 - 1` (ASSUME_TAC o SIMP_RULE arith_ss [])) 50 \\ EXISTS_TAC `t2 - 1` \\ Cases_on `t2` 51 \\ FULL_SIMP_TAC arith_ss [ADD1] \\ FULL_SIMP_TAC bool_ss [] 52 \\ `n = t` by DECIDE_TAC \\ ASM_REWRITE_TAC []); 53 54val LEAST_NOT_RESET = save_thm("LEAST_NOT_RESET", 55 GEN_ALL (MATCH_MP (PROVE [] ``((a ==> b) /\ (b ==> c)) ==> (a ==> c)``) 56 (CONJ (SPEC_ALL EXISTS_LEAST_NOT_RESET) ((SIMP_RULE std_ss [] o 57 SPEC `\t. IS_RESET i t /\ ~IS_RESET i (t + 1) /\ ~IS_RESET i (t + 2)`) 58 whileTheory.LEAST_EXISTS_IMP)))); 59 60val IS_RESET_LEM = prove( 61 `!i t. ~IS_RESET i t ==> FST (i t)`, 62 NTAC 2 STRIP_TAC \\ REWRITE_TAC [IS_RESET_def] 63 \\ SPEC_THEN `i t` (fn th => ONCE_REWRITE_TAC [th]) form_7tuple 64 \\ SIMP_TAC std_ss [PROJ_NRESET_def]); 65 66val IS_RESET_THM = store_thm("IS_RESET_THM", 67 `!i x. (!t. ~(t < x) \/ ~IS_RESET i t) ==> (!t. (t < x) ==> FST (i t))`, 68 PROVE_TAC [IS_RESET_LEM]); 69 70val IS_RESET_THM2 = store_thm("IS_RESET_THM2", 71 `!y x i. (!t. (t < x) ==> ~IS_RESET i t) /\ y <= x ==> 72 (!t. (t < y) ==> ~IS_RESET i t)`, 73 METIS_TAC [LESS_LESS_EQ_TRANS]); 74 75(* ------------------------------------------------------------------------- *) 76 77val arm6ctrl = ``CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart 78 onewinst endinst obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch 79 onfq ooonfq oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 mrq2 nbw 80 nrw sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 mshift``; 81 82val AFTER_RESET1_def = Define` 83 AFTER_RESET1 (ARM6 dp (^arm6ctrl)) = oorst /\ resetlatch`; 84 85val AFTER_RESET2_def = Define` 86 AFTER_RESET2 (ARM6 dp (^arm6ctrl)) = ~iregval /\ oorst /\ resetlatch`; 87 88val AFTER_RESET3_def = Define` 89 AFTER_RESET3 (ARM6 dp (^arm6ctrl)) = 90 ~iregval /\ opipebll /\ oorst /\ resetlatch`; 91 92val AFTER_RESET4_def = Define` 93 AFTER_RESET4 (ARM6 dp (^arm6ctrl)) = 94 pipeaval /\ pipebval /\ ~iregval /\ opipebll /\ oorst /\ resetlatch`; 95 96val AFTER_NRESET1_def = Define` 97 AFTER_NRESET1 (ARM6 dp (^arm6ctrl)) = 98 pipeaval /\ pipebval /\ ~iregval /\ opipebll /\ ~oorst /\ resetlatch`; 99 100val AFTER_NRESET2_def = Define` 101 AFTER_NRESET2 (ARM6 dp (^arm6ctrl)) = 102 pipeaval /\ pipebval /\ iregval /\ ointstart /\ endinst /\ onewinst /\ 103 opipebll /\ (nxtic = swi_ex) /\ (nxtis = t3) /\ ~nopc1 /\ 104 ~oorst /\ ~resetlatch /\ (aregn2 = 0w) /\ mrq2 /\ ~nrw /\ (mask = ARB)`; 105 106(* ------------------------------------------------------------------------- *) 107 108val IS_RESET_EXISTS = prove( 109 `(!i t. IS_RESET i t ==> 110 ?onfq oniq abort data cpa cpb. i t = (F,onfq,oniq,abort,data,cpa,cpb)) /\ 111 !i t. ~IS_RESET i t ==> 112 ?onfq oniq abort data cpa cpb. i t = (T,onfq,oniq,abort,data,cpa,cpb)`, 113 RW_TAC std_ss [IS_RESET_def] \\ Cases_on_arm6inp `i (t:num)` 114 \\ FULL_SIMP_TAC std_ss [PROJ_NRESET_def]); 115 116fun add_rws f rws = 117 let val cmp_set = f() 118 val _ = computeLib.add_thms rws cmp_set 119 (* val _ = computeLib.set_skip cmp_set ``COND`` NONE *) 120 in 121 cmp_set 122 end; 123 124fun reset_rws() = 125 add_rws computeLib.bool_compset 126 [pairTheory.FST,pairTheory.SND,LET_THM,pairTheory.UNCURRY_DEF, 127 REWRITE_RULE [DECODE_PSR_def,COND_PAIR] NEXT_ARM6_def, 128 RESETLATCH_def,AFTER_RESET1_def]; 129 130fun reset_rws2() = add_rws reset_rws 131 [AFTER_RESET2_def,IREGVAL_def,PIPESTATIREGWRITE_def]; 132 133fun reset_rws3() = add_rws reset_rws2 134 [AFTER_RESET3_def,PIPEBLL_def,ABORTINST_def,IC_def,NEWINST_def]; 135 136fun reset_rws4() = add_rws reset_rws3 137 [AFTER_RESET4_def,PIPEALL_def,PIPEAVAL_def,PIPESTATAWRITE_def, 138 PIPESTATBWRITE_def]; 139 140fun reset_rws5() = add_rws reset_rws4 141 [AFTER_NRESET1_def,ENDINST_def,RWA_def,PCCHANGE_def,RESETSTART_def]; 142 143fun reset_rws6() = add_rws reset_rws5 144 [AFTER_NRESET2_def,NOPC_def,AREGN1_def,NRW_def,NMREQ_def,MASK_def,NXTIC_def, 145 NXTIS_def,INTSEQ_def,iclass_EQ_iclass,iclass2num_thm]; 146 147val AFTER_RESET1_THM = prove( 148 `!a t i. IS_RESET i t ==> AFTER_RESET1 (NEXT_ARM6 a (i t))`, 149 Cases_arm6 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC IS_RESET_EXISTS 150 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws()))); 151 152val AFTER_RESET2_THM = prove( 153 `!a t i. AFTER_RESET1 a /\ IS_RESET i t ==> AFTER_RESET2 (NEXT_ARM6 a (i t))`, 154 Cases_arm6 \\ RW_TAC std_ss [AFTER_RESET1_def] \\ IMP_RES_TAC IS_RESET_EXISTS 155 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws2()))); 156 157val AFTER_RESET3_THM = prove( 158 `!a t i. AFTER_RESET2 a /\ IS_RESET i t ==> AFTER_RESET3 (NEXT_ARM6 a (i t))`, 159 Cases_arm6 \\ RW_TAC std_ss [AFTER_RESET2_def] \\ IMP_RES_TAC IS_RESET_EXISTS 160 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws3()))); 161 162val AFTER_RESET4_THM = prove( 163 `!a t i. AFTER_RESET3 a /\ IS_RESET i t ==> AFTER_RESET4 (NEXT_ARM6 a (i t))`, 164 Cases_arm6 \\ RW_TAC std_ss [AFTER_RESET3_def] \\ IMP_RES_TAC IS_RESET_EXISTS 165 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws4()))); 166 167val AFTER_NRESET1_THM = prove( 168 `!a t i. AFTER_RESET4 a /\ ~IS_RESET i t ==> 169 AFTER_NRESET1 (NEXT_ARM6 a (i t))`, 170 Cases_arm6 \\ RW_TAC std_ss [AFTER_RESET4_def] \\ IMP_RES_TAC IS_RESET_EXISTS 171 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws5()))); 172 173val AFTER_NRESET2_THM = prove( 174 `!a t i. AFTER_NRESET1 a /\ ~IS_RESET i t ==> 175 AFTER_NRESET2 (NEXT_ARM6 a (i t))`, 176 Cases_arm6 \\ RW_TAC std_ss [AFTER_NRESET1_def] \\ IMP_RES_TAC IS_RESET_EXISTS 177 \\ ASM_REWRITE_TAC [] \\ CONV_TAC (computeLib.CBV_CONV (reset_rws6())) 178 \\ SIMP_TAC std_ss []); 179 180val AFTER_NRESET2_THM2 = prove( 181 `!x. IS_RESET x.inp 0 /\ IS_RESET x.inp 1 /\ 182 IS_RESET x.inp 2 /\ IS_RESET x.inp 3 /\ 183 ~IS_RESET x.inp 4 /\ ~IS_RESET x.inp 5 ==> 184 AFTER_NRESET2 ((FUNPOW (SNEXT NEXT_ARM6) 6 x).state)`, 185 Cases \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 186 \\ IMP_RES_TAC (SPECL [`a`,`0`] AFTER_RESET1_THM) 187 \\ POP_ASSUM (SPEC_THEN `a` ASSUME_TAC) 188 \\ IMP_RES_TAC (SPECL [`a`,`1`] AFTER_RESET2_THM) 189 \\ IMP_RES_TAC (SPECL [`a`,`2`] AFTER_RESET3_THM) 190 \\ IMP_RES_TAC (SPECL [`a`,`3`] AFTER_RESET4_THM) 191 \\ IMP_RES_TAC (SPECL [`a`,`4`] AFTER_NRESET1_THM) 192 \\ IMP_RES_TAC (SPECL [`a`,`5`] AFTER_NRESET2_THM) 193 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss) 194 [numeralTheory.numeral_funpow,SNEXT_def,ADVANCE_def]); 195 196val lem = prove( 197 `!t1 t2 i. IS_RESET (ADVANCE t1 i) t2 = IS_RESET i (t1 + t2)`, 198 SIMP_TAC bool_ss [IS_RESET_def,ADVANCE_def]); 199 200val SPEC_AFTER_NRESET2 = save_thm("SPEC_AFTER_NRESET2", 201 (GEN_ALL o SIMP_RULE arith_ss [] o DISCH `2 < t` o SPEC_ALL o 202 INST [`t` |-> `t - 3`] o SIMP_RULE (srw_ss()) [lem] o 203 SPEC `<| state := a; inp := ADVANCE t i|>`) AFTER_NRESET2_THM2); 204 205val AFTER_NRESET2_THM3 = store_thm("AFTER_NRESET2_THM3", 206 `!a. AFTER_NRESET2 a ==> (INIT_ARM6 a = a)`, 207 Cases_arm6 \\ RW_TAC (std_ss++SIZES_ss) 208 [AFTER_NRESET2_def,INIT_ARM6_def,MASK_def,n2w_11]); 209 210val AFTER_NRESET2_THM4 = store_thm("AFTER_NRESET2_THM4", 211 `!a j k l m. AFTER_NRESET2 a ==> 212 (NEXT_ARM (ABS_ARM6 j) ((\(a,b,c) d. (a,b,c,d)) 213 (case ABS_ARM6 a 214 of ARM_EX v v1 v2 => 215 (exc2exception v2 v k,l,v1)) m) = ABS_ARM6 a)`, 216 Cases_arm6 \\ RW_TAC std_ss [AFTER_NRESET2_def,ABS_ARM6_def,PROJ_Reset_def, 217 NEXT_ARM_def,IS_Reset_def,exc2exception_def,num2exception_thm,word_0_n2w]); 218 219(* ------------------------------------------------------------------------- *) 220 221val lem = prove( 222 `!i t. i IN STRM_ARM6 /\ IS_RESET i t /\ ~IS_RESET i (t + 1) ==> 223 IS_RESET i (t - 1)`, 224 RW_TAC bool_ss [IN_DEF,STRM_ARM6_def] 225 \\ Cases_on `t` \\ FULL_SIMP_TAC arith_ss [ADD1] 226 \\ PAT_X_ASSUM `!t. IS_RESET i t ==> b` (SPEC_THEN `n + 1` IMP_RES_TAC) 227 \\ FULL_SIMP_TAC arith_ss []); 228 229val lem2 = prove( 230 `!i t. i IN STRM_ARM6 /\ IS_RESET i t /\ ~IS_RESET i (t + 1) ==> 231 IS_RESET i (t - 1) /\ IS_RESET i (t - 2)`, 232 REPEAT STRIP_TAC \\ IMP_RES_TAC lem 233 \\ FULL_SIMP_TAC bool_ss [IN_DEF,STRM_ARM6_def] 234 \\ Cases_on `t` \\ FULL_SIMP_TAC arith_ss [ADD1] 235 \\ PAT_X_ASSUM `!t. IS_RESET i t ==> b` (SPEC_THEN `n` IMP_RES_TAC) 236 \\ FULL_SIMP_TAC arith_ss []); 237 238val PREVIOUS_THREE_RESET = store_thm("PREVIOUS_THREE_RESET", 239 `!i t. i IN STRM_ARM6 /\ IS_RESET i t /\ ~IS_RESET i (t + 1) ==> 240 IS_RESET i (t - 1) /\ IS_RESET i (t - 2) /\ IS_RESET i (t - 3)`, 241 REPEAT STRIP_TAC \\ IMP_RES_TAC lem 242 \\ FULL_SIMP_TAC bool_ss [IN_DEF,STRM_ARM6_def] 243 \\ Cases_on `t` \\ FULL_SIMP_TAC arith_ss [ADD1] 244 \\ PAT_X_ASSUM `!t. IS_RESET i t ==> b` 245 (fn th => IMP_RES_TAC (SPEC `n` th) \\ ASSUME_TAC th) 246 \\ FULL_SIMP_TAC arith_ss [] 247 \\ POP_ASSUM (SPEC_THEN `n - 1` IMP_RES_TAC) 248 \\ FULL_SIMP_TAC arith_ss [] 249 \\ PROVE_TAC [DECIDE ``!n. ~(n = 0) ==> (n - 1 + 3 = n + 2)``]); 250 251val LEAST_RESET_GT_TWO = store_thm("LEAST_RESET_GT_TWO", 252 `!i t. i IN STRM_ARM6 /\ IS_RESET i t ==> 253 2 < (LEAST t. IS_RESET i t /\ ~IS_RESET i (t + 1) /\ 254 ~IS_RESET i (t + 2))`, 255 REPEAT STRIP_TAC \\ IMP_RES_TAC LEAST_NOT_RESET 256 \\ PAT_X_ASSUM `IS_RESET i t` (K ALL_TAC) 257 \\ IMP_RES_TAC PREVIOUS_THREE_RESET 258 \\ REPEAT (PAT_X_ASSUM `~a ==> b` (K ALL_TAC)) 259 \\ ABBREV_TAC `l = LEAST t. IS_RESET i t /\ ~IS_RESET i (t + 1) /\ 260 ~IS_RESET i (t + 2)` 261 \\ Cases_on `(l = 0) \/ (l = 1) \/ (l = 2)` 262 \\ FULL_SIMP_TAC arith_ss [IN_DEF,STRM_ARM6_def] 263 \\ POP_ASSUM (fn th => FULL_SIMP_TAC arith_ss [th]) 264 \\ PAT_X_ASSUM `!n. IS_RESET i t ==> b` IMP_RES_TAC 265 \\ FULL_SIMP_TAC arith_ss []); 266 267(* ------------------------------------------------------------------------- *) 268 269val AREGN1_THM = store_thm("AREGN1_THM", 270 `!resetstart dataabt1 fiqactl irqactl coproc1 iregabt2. 271 (AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2 = 2w) = 272 ~resetstart /\ ~dataabt1 /\ ~fiqactl /\ ~irqactl /\ ~coproc1 /\ ~iregabt2`, 273 RW_TAC (std_ss++SIZES_ss) [AREGN1_def,n2w_11]); 274 275val interrupt_exists = store_thm("interrupt_exists", 276 `!i f. ?aregn:word3. 277 ~(aregn IN {0w; 1w; 2w; 5w}) /\ 278 ((aregn = 7w) ==> f) /\ ((aregn = 6w) ==> i)`, 279 NTAC 2 STRIP_TAC \\ EXISTS_TAC `3w` 280 \\ RW_TAC (std_ss++SIZES_ss) [pred_setTheory.IN_INSERT,n2w_11, 281 pred_setTheory.NOT_IN_EMPTY]); 282 283val AREGN1_BIJ = store_thm("AREGN1_BIJ", 284 `!resetstart dataabt1 fiqactl irqactl coproc1 iregabt2. 285 exception2num (num2exception ( 286 w2n (AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2))) = 287 w2n (AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2)`, 288 SIMP_TAC std_ss [GSYM exception2num_num2exception, 289 (SIMP_RULE (std_ss++SIZES_ss) [] o 290 Thm.INST_TYPE [alpha |-> ``:3``]) w2n_lt]); 291 292(* ------------------------------------------------------------------------- *) 293 294val LESS_THM = 295 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 296 297val num2exception_word3 = store_thm("num2exception_word3", 298 `(!aregn:word3. (num2exception (w2n aregn) = reset) = (aregn = 0w)) /\ 299 (!aregn:word3. (num2exception (w2n aregn) = undefined) = (aregn = 1w)) /\ 300 (!aregn:word3. (num2exception (w2n aregn) = software) = (aregn = 2w)) /\ 301 (!aregn:word3. (num2exception (w2n aregn) = pabort) = (aregn = 3w)) /\ 302 (!aregn:word3. (num2exception (w2n aregn) = dabort) = (aregn = 4w)) /\ 303 (!aregn:word3. (num2exception (w2n aregn) = address) = (aregn = 5w)) /\ 304 (!aregn:word3. (num2exception (w2n aregn) = interrupt) = (aregn = 6w)) /\ 305 !aregn:word3. (num2exception (w2n aregn) = fast) = (aregn = 7w)`, 306 REPEAT STRIP_TAC \\ `w2n aregn < 8` 307 by PROVE_TAC [w2n_lt,EVAL ``dimword (:3)``] 308 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) 309 [num2exception_thm,exception_EQ_exception,exception2num_thm, 310 GSYM w2n_11,w2n_n2w,LESS_THM]); 311 312val INTERRUPT_ADDRESS = store_thm("INTERRUPT_ADDRESS", 313 `!aregn2:word3. n2w (4 * exception2num (num2exception (w2n aregn2))) = 314 4w:word32 * w2w aregn2`, 315 STRIP_TAC \\ `w2n aregn2 < 8` by PROVE_TAC [w2n_lt,EVAL ``dimword (:3)``] 316 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) 317 [word_mul_def,w2n_w2w,w2n_n2w,exception2num_num2exception]); 318 319val SOFTWARE_ADDRESS = save_thm("SOFTWARE_ADDRESS", 320 (REWRITE_RULE [EVAL ``w2n (2w:word3)``,num2exception_thm] o 321 SPEC `2w`) INTERRUPT_ADDRESS); 322 323val NOT_RESET = store_thm("NOT_RESET", 324 `!x n irqactl iregabt2 fiqactl dataabt1 coproc1. 325 ~IS_Reset (exc2exception (num2exception (w2n 326 (AREGN1 F dataabt1 fiqactl irqactl coproc1 iregabt2))) x n)`, 327 RW_TAC (std_ss++SIZES_ss) [IS_Reset_def,exc2exception_def,num2exception_thm, 328 AREGN1_def,w2n_n2w]); 329 330val NOT_RESET2 = store_thm("NOT_RESET2", 331 `!x ointstart n aregn. 332 ~(aregn IN {0w; 2w; 5w}) ==> 333 ~IS_Reset (exc2exception (num2exception (w2n 334 (if ointstart then aregn else 2w:word3))) x n)`, 335 RW_TAC (std_ss++SIZES_ss++pred_setSimps.PRED_SET_ss) [IS_Reset_def, 336 exc2exception_def,num2exception_thm,w2n_n2w] 337 \\ Cases_on `num2exception (w2n aregn)` 338 \\ FULL_SIMP_TAC (srw_ss()) [num2exception_word3]); 339 340val IS_Reset_IMP_EXISTS_SOME_Reset = store_thm("IS_Reset_IMP_EXISTS_SOME_Reset", 341 `!i. IS_Reset i ==> (?s. i = SOME (Reset s))`, 342 Cases \\ RW_TAC std_ss [IS_Reset_def] \\ Cases_on `x` 343 \\ FULL_SIMP_TAC std_ss [interrupts_case_def] \\ PROVE_TAC []); 344 345(* ------------------------------------------------------------------------- *) 346 347val SIMP_IS_Dabort = store_thm("SIMP_IS_Dabort", 348 `!x n irqactl iregabt2 fiqactl dataabt1 coproc1. 349 IS_Dabort (exc2exception (num2exception (w2n 350 (AREGN1 F dataabt1 fiqactl irqactl coproc1 iregabt2))) x n) = dataabt1`, 351 RW_TAC (std_ss++SIZES_ss) [IS_Dabort_def,AREGN1_def,exc2exception_def, 352 num2exception_thm,w2n_n2w]); 353 354val SIMP_PROJ_Dabort = store_thm("SIMP_PROJ_Dabort", 355 `!x n irqactl iregabt2 fiqactl coproc1. 356 PROJ_Dabort (exc2exception (num2exception (w2n 357 (AREGN1 F T fiqactl irqactl coproc1 iregabt2))) x n) = n`, 358 RW_TAC (std_ss++SIZES_ss) [PROJ_Dabort_def,AREGN1_def,exc2exception_def, 359 num2exception_thm,w2n_n2w]); 360 361val CP_NOT = prove( 362 `!ic. ic IN {cdp_und; mrc; mcr; stc; ldc} ==> ~(ic = mrs_msr)`, 363 RW_TAC (std_ss++pred_setSimps.PRED_SET_ss) []); 364 365(* 366val EXTRACT_UNDEFINED = 367 simpLib.SIMP_PROVE (std_ss++pred_setSimps.PRED_SET_ss) 368 [AC DISJ_ASSOC DISJ_COMM] 369 ``ic IN {reset; undefined; software; address} = 370 ic IN {reset; software; address} \/ (ic = undefined)``; 371*) 372 373val SIMP_interrupt2exception = store_thm("SIMP_interrupt2exception", 374 `!y reg psr ointstart n ireg i f aregn. 375 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 376 ~(DECODE_INST ireg = mrs_msr) /\ 377 (((aregn = 1w) ==> DECODE_INST ireg IN {cdp_und; mrc; mcr; stc; ldc}) /\ 378 ~(aregn IN {0w; 2w; 5w}) \/ 379 ~(aregn IN {0w; 1w; 2w; 5w})) /\ 380 ((aregn = 7w) ==> ~f) /\ ((aregn = 6w) ==> ~i) ==> 381 ((interrupt2exception (ARM_EX (ARM reg psr) ireg software) (i,f) 382 (exc2exception (num2exception ( 383 w2n (if ointstart then aregn else 2w:word3))) y n)) = 384 (num2exception (w2n (if ointstart then aregn else 2w))))`, 385 NTAC 9 STRIP_TAC \\ Cases_on `num2exception (w2n aregn)` 386 \\ Cases_on `ointstart` \\ ASM_SIMP_TAC (srw_ss()++SIZES_ss++ 387 boolSimps.LET_ss++ pred_setSimps.PRED_SET_ss) 388 [DECODE_PSR_def,w2n_n2w,exc2exception_def,num2exception_thm, 389 interrupt2exception_def] 390 \\ FULL_SIMP_TAC std_ss [num2exception_word3]); 391 392val SIMP_interrupt2exception2 = save_thm("SIMP_interrupt2exception2", 393 (GEN_ALL o REWRITE_RULE [] o INST [`ointstart` |-> `T`] o 394 SPEC_ALL) SIMP_interrupt2exception); 395 396val SIMP_interrupt2exception3 = store_thm("SIMP_interrupt2exception3", 397 `!y resetstart reg psr n irqactl iregabt2 ireg i fiqactl f dataabt1 coproc1. 398 DECODE_INST ireg IN {cdp_und; mrc; mcr; stc; ldc} /\ 399 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg /\ 400 (fiqactl ==> ~f) /\ (irqactl ==> ~i) ==> 401 ((interrupt2exception (ARM_EX (ARM reg psr) ireg software) (i,f) 402 (exc2exception (num2exception (w2n 403 (AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2))) y n)) = 404 (num2exception (w2n 405 (AREGN1 resetstart dataabt1 fiqactl irqactl coproc1 iregabt2))))`, 406 RW_TAC (std_ss++SIZES_ss) [DECODE_PSR_def,AREGN1_def,CP_NOT, 407 interrupt2exception_def,exc2exception_def,num2exception_thm,w2n_n2w]); 408 409val SIMP_interrupt2exception4 = store_thm("SIMP_interrupt2exception4", 410 `!y resetstart reg psr n irqactl iregabt2 ireg i fiqactl f exc dataabt1. 411 ((exc = software) ==> ~CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg) /\ 412 (fiqactl ==> ~f) /\ (irqactl ==> ~i) ==> 413 ((interrupt2exception (ARM_EX (ARM reg psr) ireg exc) (i,f) 414 (exc2exception (num2exception (w2n 415 (AREGN1 resetstart dataabt1 fiqactl irqactl F iregabt2))) y n)) = 416 (num2exception (w2n 417 (AREGN1 resetstart dataabt1 fiqactl irqactl F iregabt2))))`, 418 RW_TAC (std_ss++SIZES_ss) [DECODE_PSR_def,AREGN1_def, 419 interrupt2exception_def,exc2exception_def,num2exception_thm,w2n_n2w]); 420 421val SIMP_interrupt2exception5 = prove( 422 `!y resetstart reg psr n irqactl iregabt2 ireg i' fiqactl f' dataabt1. 423 CONDITION_PASSED (NZCV (CPSR_READ psr)) ireg ==> 424 (let (flags,i,f,m) = DECODE_PSR (CPSR_READ psr) 425 and old_flags = (DECODE_INST ireg = mrs_msr) in 426 (fiqactl ==> if old_flags then ~f else ~f') /\ 427 (irqactl ==> if old_flags then ~i else ~i')) ==> 428 ((interrupt2exception (ARM_EX (ARM reg psr) ireg software) (i',f') 429 (exc2exception (num2exception (w2n 430 (AREGN1 resetstart dataabt1 fiqactl irqactl F iregabt2))) y n)) = 431 (num2exception (w2n 432 (AREGN1 resetstart dataabt1 fiqactl irqactl F iregabt2))))`, 433 RW_TAC (std_ss++SIZES_ss) [DECODE_PSR_def,AREGN1_def, 434 interrupt2exception_def,exc2exception_def,num2exception_thm,w2n_n2w]); 435 436val SIMP_interrupt2exception5 = save_thm("SIMP_interrupt2exception5", 437 SIMP_RULE (std_ss++boolSimps.COND_elim_ss) 438 [DECODE_PSR_def] SIMP_interrupt2exception5); 439 440(* ------------------------------------------------------------------------- *) 441 442val _ = export_theory(); 443