1(* ========================================================================= *) 2(* FILE : arm_evalScript.sml *) 3(* DESCRIPTION : Various theorems about the ISA and instruction encoding *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2005-2007 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["pred_setSimps", "rich_listTheory", "wordsLib", "armLib", 11 "updateTheory", "instructionTheory", "systemTheory"]; 12*) 13 14open HolKernel boolLib Parse bossLib; 15open Q rich_listTheory arithmeticTheory wordsLib wordsTheory bitTheory; 16open combinTheory updateTheory armTheory systemTheory instructionTheory; 17 18val _ = new_theory "arm_eval"; 19 20(* ------------------------------------------------------------------------- *) 21 22infix << >> 23 24val op << = op THENL; 25val op >> = op THEN1; 26 27val std_ss = std_ss ++ boolSimps.LET_ss; 28val arith_ss = arith_ss ++ boolSimps.LET_ss; 29 30val fcp_ss = armLib.fcp_ss; 31val SIZES_ss = wordsLib.SIZES_ss; 32 33val _ = wordsLib.guess_lengths(); 34 35(* ------------------------------------------------------------------------- *) 36 37val REG_READ6_def = Define` 38 REG_READ6 reg mode n = 39 if n = 15w then 40 FETCH_PC reg 41 else 42 REG_READ reg mode n`; 43 44val REG_WRITEL_def = Define` 45 (REG_WRITEL r m [] = r) /\ 46 (REG_WRITEL r m ((n,d)::l) = REG_WRITE (REG_WRITEL r m l) m n d)`; 47 48(* ------------------------------------------------------------------------- *) 49 50val STATE_ARM_MMU_NEXT = store_thm("STATE_ARM_MMU_NEXT", 51 `!t a b c. (STATE_ARM_MMU ops t a = b) /\ (NEXT_ARM_MMU ops b = c) ==> 52 (STATE_ARM_MMU ops (t + 1) a = c)`, 53 RW_TAC bool_ss [STATE_ARM_MMU_def,GSYM arithmeticTheory.ADD1]); 54 55(* ------------------------------------------------------------------------- *) 56 57val register2num_lt_neq = store_thm("register2num_lt_neq", 58 `!x y. register2num x < register2num y ==> ~(x = y)`, 59 METIS_TAC [prim_recTheory.LESS_NOT_EQ, register2num_11]); 60 61val psr2num_lt_neq = store_thm("psr2num_lt_neq", 62 `!x y. psr2num x < psr2num y ==> ~(x = y)`, 63 METIS_TAC [prim_recTheory.LESS_NOT_EQ, psr2num_11]); 64 65val REGISTER_RANGES = 66 (SIMP_RULE (std_ss++SIZES_ss) [] o Thm.INST_TYPE [alpha |-> ``:4``]) w2n_lt; 67 68val mode_reg2num_15 = (GEN_ALL o 69 SIMP_RULE (arith_ss++SIZES_ss) [w2n_n2w] o 70 SPECL [`m`,`15w`]) mode_reg2num_def; 71 72val mode_reg2num_lt = store_thm("mode_reg2num_lt", 73 `!w m w. mode_reg2num m w < 31`, 74 ASSUME_TAC REGISTER_RANGES 75 \\ RW_TAC std_ss [mode_reg2num_def,USER_def,DECIDE ``n < 16 ==> n < 31``] 76 \\ Cases_on `m` 77 \\ FULL_SIMP_TAC arith_ss [mode_distinct,mode_case_def, 78 DECIDE ``a < 16 /\ b < 16 ==> (a + b < 31)``, 79 DECIDE ``a < 16 /\ ~(a = 15) ==> (a + 16 < 31)``]); 80 81val not_reg_eq_lem = prove(`!v w. ~(v = w) ==> ~(w2n v = w2n w)`, 82 REPEAT Cases \\ SIMP_TAC std_ss [w2n_n2w,n2w_11]); 83 84val not_reg_eq = store_thm("not_reg_eq", 85 `!v w m1 m2. ~(v = w) ==> ~(mode_reg2num m1 v = mode_reg2num m2 w)`, 86 NTAC 4 STRIP_TAC 87 \\ `w2n v < 16 /\ w2n w < 16` by REWRITE_TAC [REGISTER_RANGES] 88 \\ Cases_on `m1` \\ Cases_on `m2` 89 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss) 90 [USER_def,mode_reg2num_def,not_reg_eq_lem] 91 \\ COND_CASES_TAC \\ ASM_SIMP_TAC arith_ss [not_reg_eq_lem] 92 \\ COND_CASES_TAC \\ ASM_SIMP_TAC arith_ss [not_reg_eq_lem]); 93 94val not_pc = (GEN_ALL o REWRITE_RULE [mode_reg2num_15] o 95 SPECL [`v`,`15w`]) not_reg_eq; 96 97val r15 = SYM (List.nth (CONJUNCTS num2register_thm, 15)) 98val READ_TO_READ6 = store_thm("READ_TO_READ6", 99 `!r m n d. (REG_READ (REG_WRITE r usr 15w (d - 8w)) m n = 100 REG_READ6 (REG_WRITE r usr 15w d) m n)`, 101 RW_TAC (std_ss++SIZES_ss) [REG_READ_def,REG_READ6_def,FETCH_PC_def, 102 REG_WRITE_def,UPDATE_def,WORD_SUB_ADD,mode_reg2num_15] 103 \\ PROVE_TAC [r15,num2register_11,mode_reg2num_lt,not_pc,DECIDE ``15 < 31``]); 104 105val TO_WRITE_READ6 = store_thm("TO_WRITE_READ6", 106 `(!r. FETCH_PC r = REG_READ6 r usr 15w) /\ 107 (!r. INC_PC r = REG_WRITE r usr 15w (REG_READ6 r usr 15w + 4w)) /\ 108 (!r m d. REG_WRITE r m 15w d = REG_WRITE r usr 15w d) /\ 109 (!r m. REG_READ6 r m 15w = REG_READ6 r usr 15w)`, 110 RW_TAC std_ss [INC_PC_def,REG_READ6_def,REG_WRITE_def,REG_READ_def, 111 FETCH_PC_def,mode_reg2num_15]); 112 113val REG_WRITE_WRITE = store_thm("REG_WRITE_WRITE", 114 `!r m n d1 d2. REG_WRITE (REG_WRITE r m n d1) m n d2 = REG_WRITE r m n d2`, 115 RW_TAC bool_ss [REG_WRITE_def,UPDATE_EQ]); 116 117val REG_WRITE_WRITE_COMM = store_thm("REG_WRITE_WRITE_COMM", 118 `!r m n1 n2 d1 d2. 119 ~(n1 = n2) ==> 120 (REG_WRITE (REG_WRITE r m n1 d1) m n2 d2 = 121 REG_WRITE (REG_WRITE r m n2 d2) m n1 d1)`, 122 RW_TAC std_ss [REG_WRITE_def,UPDATE_COMMUTES,not_reg_eq, 123 mode_reg2num_lt,num2register_11]); 124 125val REG_WRITE_WRITE_PC = store_thm("REG_WRITE_WRITE_PC", 126 `!r m1 m2 n d p. 127 REG_WRITE (REG_WRITE r m1 15w p) m2 n d = 128 if n = 15w then 129 REG_WRITE r usr 15w d 130 else 131 REG_WRITE (REG_WRITE r m2 n d) usr 15w p`, 132 RW_TAC std_ss [TO_WRITE_READ6,REG_WRITE_WRITE] 133 \\ ASM_SIMP_TAC std_ss [REG_WRITE_def,UPDATE_COMMUTES,not_pc, 134 mode_reg2num_15,mode_reg2num_lt,num2register_11]); 135 136val REG_READ_WRITE_THM = prove( 137 `(!r m n1 n2 d. REG_READ6 (REG_WRITE r m n1 d) m n2 = 138 if n1 = n2 then d else REG_READ6 r m n2) /\ 139 !r m n d. (REG_WRITE r m n (REG_READ6 r m n) = r)`, 140 RW_TAC std_ss [REG_READ6_def,REG_READ_def,REG_WRITE_def,FETCH_PC_def, 141 UPDATE_APPLY_IMP_ID,mode_reg2num_15] \\ SIMP_TAC std_ss [UPDATE_def] 142 \\ PROVE_TAC [r15,not_pc,not_reg_eq,mode_reg2num_lt,num2register_11, 143 DECIDE ``15 < 31``]); 144 145val REG_READ_WRITE_PC_THM = 146 let val thm = (SPEC_ALL o CONJUNCT1) REG_READ_WRITE_THM in 147 CONJ 148 ((SIMP_RULE arith_ss [TO_WRITE_READ6] o INST [`n2` |-> `15w`]) thm) 149 ((SIMP_RULE arith_ss [TO_WRITE_READ6] o INST [`n1` |-> `15w`]) thm) 150 end; 151 152val REG_READ_WRITE_NEQ = store_thm("REG_READ_WRITE_NEQ", 153 `!r m1 m2 n1 n2 d. ~(n1 = n2) ==> 154 (REG_READ6 (REG_WRITE r m1 n1 d) m2 n2 = REG_READ6 r m2 n2)`, 155 RW_TAC std_ss [REG_READ6_def,REG_READ_def,REG_WRITE_def,FETCH_PC_def, 156 UPDATE_APPLY_IMP_ID,mode_reg2num_15] \\ SIMP_TAC std_ss [UPDATE_def] 157 \\ PROVE_TAC [r15,not_pc,not_reg_eq,mode_reg2num_lt,num2register_11, 158 DECIDE ``15 < 31``]); 159 160val REG_READ_READ6 = store_thm("REG_READ_READ6", 161 `!r m n. ~(n = 15w) ==> (REG_READ6 r m n = REG_READ r m n)`, 162 SIMP_TAC bool_ss [REG_READ6_def]); 163 164val REG_READ_WRITE_PC = 165 (GEN_ALL o SIMP_RULE std_ss [REG_READ_READ6] o INST [`n2` |-> `n`] o 166 DISCH `~(n2 = 15w)` o CONJUNCT2) REG_READ_WRITE_PC_THM; 167 168val REG_READ_INC_PC = store_thm("REG_READ_INC_PC", 169 `!r m n. ~(n = 15w) ==> (REG_READ (INC_PC r) m n = REG_READ r m n)`, 170 SIMP_TAC bool_ss [TO_WRITE_READ6,REG_READ_WRITE_PC]); 171 172val REG_WRITE_INC_PC = store_thm("REG_WRITE_INC_PC", 173 `!r m n. ~(n = 15w) ==> 174 (REG_WRITE (INC_PC r) m n d = INC_PC (REG_WRITE r m n d))`, 175 SIMP_TAC bool_ss [TO_WRITE_READ6,REG_READ_WRITE_NEQ,REG_WRITE_WRITE_PC]); 176 177val REG_READ_WRITE = save_thm("REG_READ_WRITE", 178 (GEN_ALL o SIMP_RULE std_ss [REG_READ_READ6] o 179 DISCH `~(n = 15w)` o SPEC_ALL o CONJUNCT2) REG_READ_WRITE_THM); 180 181val REG_WRITE_READ = 182 (GEN_ALL o SIMP_RULE std_ss [REG_READ_READ6] o 183 DISCH `~(n2 = 15w)` o SPEC_ALL o CONJUNCT1) REG_READ_WRITE_THM; 184 185val INC_PC = save_thm("INC_PC", 186 (SIMP_RULE std_ss [REG_READ6_def,FETCH_PC_def] o 187 hd o tl o CONJUNCTS) TO_WRITE_READ6); 188 189val REG_WRITEL = store_thm("REG_WRITEL", 190 `!r m l. REG_WRITEL r m l = FOLDR (\h r. REG_WRITE r m (FST h) (SND h)) r l`, 191 Induct_on `l` \\ TRY (Cases_on `h`) \\ ASM_SIMP_TAC list_ss [REG_WRITEL_def]); 192 193val REG_WRITE_WRITEL = store_thm("REG_WRITE_WRITEL", 194 `!r m n d. REG_WRITE r m n d = REG_WRITEL r m [(n,d)]`, 195 SIMP_TAC std_ss [REG_WRITEL_def]); 196 197val REG_WRITEL_WRITEL = store_thm("REG_WRITEL_WRITEL", 198 `!r m l1 l2. REG_WRITEL (REG_WRITEL r m l1) m l2 = REG_WRITEL r m (l2 ++ l1)`, 199 SIMP_TAC std_ss [REG_WRITEL,rich_listTheory.FOLDR_APPEND]); 200 201val REG_WRITE_WRITE_THM = store_thm("REG_WRITE_WRITE_THM", 202 `!m n r m e d. x <=+ y ==> 203 (REG_WRITE (REG_WRITE r m x e) m y d = 204 if x = y then 205 REG_WRITE r m y d 206 else 207 REG_WRITE (REG_WRITE r m y d) m x e)`, 208 RW_TAC std_ss [WORD_LOWER_OR_EQ,WORD_LO,REG_WRITE_WRITE] 209 \\ METIS_TAC [REG_WRITE_def,not_reg_eq,UPDATE_COMMUTES, 210 mode_reg2num_lt,num2register_11]); 211 212val REG_READ_WRITEL = store_thm("REG_READ_WRITEL", 213 `(!r m n. REG_READ (REG_WRITEL r m []) m n = REG_READ r m n) /\ 214 (!r m n a b l. ~(n = 15w) ==> 215 (REG_READ (REG_WRITEL r m ((a,b)::l)) m n = 216 if a = n then b else REG_READ (REG_WRITEL r m l) m n))`, 217 RW_TAC std_ss [REG_WRITEL_def,REG_WRITE_READ]); 218 219val mode_reg2num_15 = (GEN_ALL o SIMP_RULE (arith_ss++SIZES_ss) [w2n_n2w] o 220 SPECL [`m`,`15w`]) mode_reg2num_def; 221 222val lem = (SIMP_RULE std_ss[REG_READ_WRITE_PC_THM, 223 TO_WRITE_READ6,WORD_ADD_SUB] o SPECL [`r`,`m`,`15w`,`d + 8w`]) READ_TO_READ6; 224 225val lem2 = prove( 226 `!r m m2 n d. ~(n = 15w) ==> 227 (REG_READ (REG_WRITE r m n d) m2 15w = REG_READ r m2 15w)`, 228 RW_TAC std_ss [REG_READ_def,REG_WRITE_def,UPDATE_def, 229 mode_reg2num_lt,num2register_11] 230 \\ PROVE_TAC [r15,mode_reg2num_lt,armTheory.num2register_11, 231 mode_reg2num_15,not_reg_eq]); 232 233val REG_READ_WRITEL_PC = store_thm("REG_READ_WRITEL_PC", 234 `!r m m2 a b l. REG_READ (REG_WRITEL r m ((a,b)::l)) m2 15w = 235 if a = 15w then b + 8w else REG_READ (REG_WRITEL r m l) m2 15w`, 236 RW_TAC std_ss [REG_WRITEL_def,TO_WRITE_READ6,lem,lem2]); 237 238val REG_READ_WRITEL_PC2 = store_thm("REG_READ_WRITEL_PC2", 239 `!r m a b l. (REG_WRITEL r m ((a,b)::l)) r15 = 240 if a = 15w then b else (REG_WRITEL r m l) r15`, 241 RW_TAC std_ss [REG_WRITEL_def,REG_WRITE_def,UPDATE_def, 242 mode_reg2num_lt,num2register_11] 243 \\ PROVE_TAC [r15,mode_reg2num_lt,armTheory.num2register_11, 244 mode_reg2num_15,not_reg_eq]); 245 246(* ------------------------------------------------------------------------- *) 247 248val LESS_THM = 249 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 250 251fun Cases_on_nzcv tm = 252 FULL_STRUCT_CASES_TAC (SPEC tm (armLib.tupleCases 253 ``(n,z,c,v):bool#bool#bool#bool``)); 254 255val SET_NZCV_IDEM = store_thm("SET_NZCV_IDEM", 256 `!a b c. SET_NZCV a (SET_NZCV b c) = SET_NZCV a c`, 257 REPEAT STRIP_TAC \\ Cases_on_nzcv `a` \\ Cases_on_nzcv `b` 258 \\ RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 259 [SET_NZCV_def,word_modify_def]); 260 261val DECODE_NZCV_SET_NZCV = store_thm("DECODE_NZCV_SET_NZCV", 262 `(!a b c d n. (SET_NZCV (a,b,c,d) n) ' 31 = a) /\ 263 (!a b c d n. (SET_NZCV (a,b,c,d) n) ' 30 = b) /\ 264 (!a b c d n. (SET_NZCV (a,b,c,d) n) ' 29 = c) /\ 265 (!a b c d n. (SET_NZCV (a,b,c,d) n) ' 28 = d)`, 266 RW_TAC (fcp_ss++SIZES_ss) [SET_NZCV_def,word_modify_def]); 267 268val DECODE_IFMODE_SET_NZCV = store_thm("DECODE_IFMODE_SET_NZCV", 269 `(!a n. (27 -- 8) (SET_NZCV a n) = (27 -- 8) n) /\ 270 (!a n. (SET_NZCV a n) ' 7 = n ' 7) /\ 271 (!a n. (SET_NZCV a n) ' 6 = n ' 6) /\ 272 (!a n. (SET_NZCV a n) ' 5 = n ' 5) /\ 273 (!a n. (4 >< 0) (SET_NZCV a n) = (4 >< 0) n)`, 274 RW_TAC bool_ss [] \\ Cases_on_nzcv `a` 275 \\ SIMP_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 276 [SET_NZCV_def,word_modify_def,word_extract_def,word_bits_def]); 277 278val DECODE_IFMODE_SET_IFMODE = store_thm("DECODE_IFMODE_SET_IFMODE", 279 `(!i f m n. (SET_IFMODE i f m n) ' 7 = i) /\ 280 (!i f m n. (SET_IFMODE i f m n) ' 6 = f) /\ 281 (!i f m n. (4 >< 0) (SET_IFMODE i f m n) = mode_num m)`, 282 RW_TAC (fcp_ss++ARITH_ss++SIZES_ss) [SET_IFMODE_def,word_modify_def, 283 word_extract_def,word_bits_def,w2w]); 284 285val SET_IFMODE_IDEM = store_thm("SET_IFMODE_IDEM", 286 `!a b c d e f g. SET_IFMODE a b c (SET_IFMODE d e f g) = SET_IFMODE a b c g`, 287 SIMP_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 288 [SET_IFMODE_def,word_modify_def]); 289 290val SET_IFMODE_NZCV_SWP = store_thm("SET_IFMODE_NZCV_SWP", 291 `!a b c d e. SET_IFMODE a b c (SET_NZCV d e) = 292 SET_NZCV d (SET_IFMODE a b c e)`, 293 REPEAT STRIP_TAC \\ Cases_on_nzcv `d` 294 \\ RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 295 [SET_NZCV_def,SET_IFMODE_def,word_modify_def] 296 \\ Cases_on `i < 5` \\ ASM_SIMP_TAC arith_ss [] 297 \\ Cases_on `i < 28` \\ ASM_SIMP_TAC arith_ss []); 298 299val DECODE_NZCV_SET_IFMODE = store_thm("DECODE_NZCV_SET_IFMODE", 300 `(!i f m n. (SET_IFMODE i f m n) ' 31 = n ' 31) /\ 301 (!i f m n. (SET_IFMODE i f m n) ' 30 = n ' 30) /\ 302 (!i f m n. (SET_IFMODE i f m n) ' 29 = n ' 29) /\ 303 (!i f m n. (SET_IFMODE i f m n) ' 28 = n ' 28) /\ 304 (!i f m n. (27 -- 8) (SET_IFMODE i f m n) = (27 -- 8) n) /\ 305 (!i f m n. (SET_IFMODE i f m n) ' 5 = n ' 5)`, 306 RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 307 [SET_IFMODE_def,word_modify_def,word_bits_def]); 308 309val SET_NZCV_ID = store_thm("SET_NZCV_ID", 310 `!a. SET_NZCV (a ' 31,a ' 30,a ' 29,a ' 28) a = a`, 311 SRW_TAC [fcpLib.FCP_ss,SIZES_ss] [SET_NZCV_def,word_modify_def] 312 \\ FULL_SIMP_TAC std_ss [LESS_THM]); 313 314(* ------------------------------------------------------------------------- *) 315 316val SPSR_READ_THM = store_thm("SPSR_READ_THM", 317 `!psr mode cpsr. 318 (CPSR_READ psr = cpsr) ==> 319 ((if USER mode then cpsr else SPSR_READ psr mode) = SPSR_READ psr mode)`, 320 RW_TAC bool_ss [CPSR_READ_def,SPSR_READ_def,mode2psr_def,USER_def] 321 \\ REWRITE_TAC [mode_case_def]); 322 323val SPSR_READ_THM2 = store_thm("SPSR_READ_THM2", 324 `!psr mode cpsr. USER mode ==> (SPSR_READ psr mode = CPSR_READ psr)`, 325 METIS_TAC [SPSR_READ_THM]); 326 327val CPSR_WRITE_READ = store_thm("CPSR_WRITE_READ", 328 `(!psr m x. CPSR_READ (SPSR_WRITE psr m x) = CPSR_READ psr) /\ 329 (!psr x. CPSR_READ (CPSR_WRITE psr x) = x)`, 330 RW_TAC bool_ss [CPSR_READ_def,CPSR_WRITE_def,SPSR_WRITE_def,UPDATE_def, 331 USER_def,mode2psr_def] 332 \\ Cases_on `m` \\ FULL_SIMP_TAC bool_ss [mode_case_def,psr_distinct]); 333 334val CPSR_READ_WRITE = store_thm("CPSR_READ_WRITE", 335 `(!psr. CPSR_WRITE psr (CPSR_READ psr) = psr) /\ 336 (!psr mode. USER mode ==> (CPSR_WRITE psr (SPSR_READ psr mode) = psr))`, 337 RW_TAC bool_ss [CPSR_READ_def,CPSR_WRITE_def,SPSR_READ_def, 338 UPDATE_APPLY_IMP_ID,USER_def,mode2psr_def] 339 \\ REWRITE_TAC [mode_case_def,APPLY_UPDATE_ID]); 340 341val CPSR_WRITE_WRITE = store_thm("CPSR_WRITE_WRITE", 342 `!psr a b. CPSR_WRITE (CPSR_WRITE psr a) b = CPSR_WRITE psr b`, 343 SIMP_TAC bool_ss [CPSR_WRITE_def,UPDATE_EQ]); 344 345val USER_usr = save_thm("USER_usr", 346 simpLib.SIMP_PROVE bool_ss [USER_def] ``USER usr``); 347 348val PSR_WRITE_COMM = store_thm("PSR_WRITE_COMM", 349 `!psr m x y. SPSR_WRITE (CPSR_WRITE psr x) m y = 350 CPSR_WRITE (SPSR_WRITE psr m y) x`, 351 RW_TAC bool_ss [SPSR_WRITE_def,CPSR_WRITE_def,USER_def,mode2psr_def] 352 \\ Cases_on `m` 353 \\ FULL_SIMP_TAC bool_ss [mode_distinct,mode_case_def,psr_distinct, 354 UPDATE_COMMUTES]); 355 356val SPSR_READ_WRITE = store_thm("SPSR_READ_WRITE", 357 `!psr m. SPSR_WRITE psr m (SPSR_READ psr m) = psr`, 358 RW_TAC std_ss [SPSR_READ_def,SPSR_WRITE_def,mode2psr_def] 359 \\ Cases_on `m` \\ SIMP_TAC (srw_ss()) [UPDATE_APPLY_IMP_ID]); 360 361val SPSR_WRITE_THM = store_thm("SPSR_WRITE_THM", 362 `!psr m x. USER m ==> (SPSR_WRITE psr m x = psr)`, 363 SIMP_TAC std_ss [SPSR_WRITE_def]); 364 365val SPSR_WRITE_WRITE = store_thm("SPSR_WRITE_WRITE", 366 `!psr m x y. SPSR_WRITE (SPSR_WRITE psr m x) m y = SPSR_WRITE psr m y`, 367 RW_TAC std_ss [SPSR_WRITE_def,UPDATE_EQ]); 368 369val SPSR_WRITE_READ = store_thm("SPSR_WRITE_READ", 370 `!psr m x. ~USER m ==> (SPSR_READ (SPSR_WRITE psr m x) m = x) /\ 371 (SPSR_READ (CPSR_WRITE psr x) m = SPSR_READ psr m)`, 372 RW_TAC std_ss [SPSR_WRITE_def,CPSR_WRITE_def,SPSR_READ_def,UPDATE_def] 373 \\ Cases_on `m` \\ FULL_SIMP_TAC (srw_ss()) [USER_def,mode2psr_def]); 374 375(* ------------------------------------------------------------------------- *) 376 377val word_ss = armLib.fcp_ss ++ wordsLib.SIZES_ss ++ ARITH_ss; 378 379val lem = prove( 380 `!w:word32 i. i < 5 ==> (((4 >< 0) w) ' i = w ' i)`, 381 RW_TAC word_ss [word_extract_def,word_bits_def,w2w]); 382 383val w2n_mod = prove( 384 `!a:'a word b. (a = n2w b) = (w2n a = b MOD dimword (:'a))`, 385 Cases \\ REWRITE_TAC [n2w_11,w2n_n2w]); 386 387val PSR_CONS = store_thm("PSR_CONS", 388 `!w:word32. w = 389 let m = DECODE_MODE ((4 >< 0) w) in 390 if m = safe then 391 SET_NZCV (w ' 31, w ' 30, w ' 29, w ' 28) ((27 -- 0) w) 392 else 393 SET_NZCV (w ' 31, w ' 30, w ' 29, w ' 28) 394 (SET_IFMODE (w ' 7) (w ' 6) m (0xFFFFF20w && w))`, 395 RW_TAC word_ss [SET_IFMODE_def,SET_NZCV_def,word_modify_def,n2w_def] 396 \\ RW_TAC word_ss [word_bits_def] 397 << [ 398 `(i = 31) \/ (i = 30) \/ (i = 29) \/ (i = 28) \/ (i < 28)` 399 by DECIDE_TAC 400 \\ ASM_SIMP_TAC arith_ss [], 401 `(i = 31) \/ (i = 30) \/ (i = 29) \/ (i = 28) \/ 402 (7 < i /\ i < 28) \/ (i = 7) \/ (i = 6) \/ (i = 5) \/ (i < 5)` 403 by DECIDE_TAC 404 \\ ASM_SIMP_TAC (word_ss++ARITH_ss) [word_and_def] 405 << [ 406 FULL_SIMP_TAC std_ss [LESS_THM] 407 \\ FULL_SIMP_TAC arith_ss [] \\ EVAL_TAC, 408 EVAL_TAC, 409 `~(mode_num m = 0w)` 410 by (Cases_on `m` \\ RW_TAC std_ss [mode_num_def] \\ EVAL_TAC) 411 \\ POP_ASSUM MP_TAC \\ UNABBREV_TAC `m` 412 \\ `w ' i = (((4 >< 0) w):word5) ' i` by METIS_TAC [lem] 413 \\ ASM_REWRITE_TAC [] \\ ABBREV_TAC `x = ((4 >< 0) w):word5` 414 \\ Cases_on `(x = 16w) \/ (x = 17w) \/ (x = 18w) \/ (x = 19w) \/ 415 (x = 23w) \/ (x = 27w) \/ (x = 31w)` 416 \\ FULL_SIMP_TAC std_ss [] \\ SRW_TAC 417 [fcpLib.FCP_ss,wordsLib.SIZES_ss,ARITH_ss,boolSimps.LET_ss] 418 [DECODE_MODE_def,mode_num_def] 419 \\ POP_ASSUM MP_TAC 420 \\ FULL_SIMP_TAC (srw_ss()++wordsLib.SIZES_ss) [w2n_mod]]]); 421 422val word_modify_PSR = save_thm("word_modify_PSR", 423 SIMP_CONV std_ss [SET_NZCV_def,SET_IFMODE_def] 424 ``word_modify f (SET_NZCV (n,z,c,v) x)``); 425 426val word_modify_PSR2 = save_thm("word_modify_PSR2", 427 SIMP_CONV std_ss [SET_NZCV_def,SET_IFMODE_def] 428 ``word_modify f (SET_NZCV (n,z,c,v) (SET_IFMODE imask fmask m x))``); 429 430val CPSR_WRITE_n2w = save_thm("CPSR_WRITE_n2w", GEN_ALL 431 ((PURE_ONCE_REWRITE_CONV [PSR_CONS] THENC PURE_REWRITE_CONV [CPSR_WRITE_def]) 432 ``CPSR_WRITE psr (n2w n)``)); 433 434val SPSR_WRITE_n2w = save_thm("SPSR_WRITE_n2w", GEN_ALL 435 ((PURE_ONCE_REWRITE_CONV [PSR_CONS] THENC PURE_REWRITE_CONV [SPSR_WRITE_def]) 436 ``SPSR_WRITE psr mode (n2w n)``)); 437 438(* ------------------------------------------------------------------------- *) 439 440val decode_opcode_def = with_flag (priming, SOME "") Define` 441 decode_opcode i = 442 case i of 443 AND cond s Rd Rn Op2 => 0w:word4 444 | EOR cond s Rd Rn Op2 => 1w 445 | SUB cond s Rd Rn Op2 => 2w 446 | RSB cond s Rd Rn Op2 => 3w 447 | ADD cond s Rd Rn Op2 => 4w 448 | ADC cond s Rd Rn Op2 => 5w 449 | SBC cond s Rd Rn Op2 => 6w 450 | RSC cond s Rd Rn Op2 => 7w 451 | TST cond Rn Op2 => 8w 452 | TEQ cond Rn Op2 => 9w 453 | CMP cond Rn Op2 => 10w 454 | CMN cond Rn Op2 => 11w 455 | ORR cond s Rd Rn Op2 => 12w 456 | MOV cond s Rd Op2 => 13w 457 | BIC cond s Rd Rn Op2 => 14w 458 | MVN cond s Rd Op2 => 15w 459 | _ => ARB`; 460 461val DECODE_PSRD_def = Define` 462 (DECODE_PSRD CPSR_c = (F,F,T)) /\ (DECODE_PSRD CPSR_f = (F,T,F)) /\ 463 (DECODE_PSRD CPSR_a = (F,T,T)) /\ (DECODE_PSRD SPSR_c = (T,F,T)) /\ 464 (DECODE_PSRD SPSR_f = (T,T,F)) /\ (DECODE_PSRD SPSR_a = (T,T,T))`; 465 466val IS_DP_IMMEDIATE_def = Define` 467 (IS_DP_IMMEDIATE (Dp_immediate rot i) = T) /\ 468 (IS_DP_IMMEDIATE (Dp_shift_immediate sh imm) = F) /\ 469 (IS_DP_IMMEDIATE (Dp_shift_register sh reg) = F)`; 470 471val IS_DTH_IMMEDIATE_def = Define` 472 (IS_DTH_IMMEDIATE (Dth_immediate i) = T) /\ 473 (IS_DTH_IMMEDIATE (Dth_register r) = F)`; 474 475val IS_DT_SHIFT_IMMEDIATE_def = Define` 476 (IS_DT_SHIFT_IMMEDIATE (Dt_immediate i) = F) /\ 477 (IS_DT_SHIFT_IMMEDIATE (Dt_shift_immediate sh imm) = T)`; 478 479val IS_MSR_IMMEDIATE_def = Define` 480 (IS_MSR_IMMEDIATE (Msr_immediate rot i) = T) /\ 481 (IS_MSR_IMMEDIATE (Msr_register r) = F)`; 482 483fun Cases_on_nzcv tm = FULL_STRUCT_CASES_TAC (SPEC tm (armLib.tupleCases 484 ``(n,z,c,v):bool#bool#bool#bool``)); 485 486val word_index = METIS_PROVE [word_index_n2w] 487 ``!i n. i < dimindex (:'a) ==> (((n2w n):bool ** 'a) ' i = BIT i n)``; 488 489val fcp_ss = arith_ss++fcpLib.FCP_ss++wordsLib.SIZES_ss; 490 491val condition_encode_lem = prove( 492 `!cond i. i < 28 ==> ~(condition_encode cond ' i)`, 493 SIMP_TAC (arith_ss++fcpLib.FCP_ss++wordsLib.SIZES_ss) 494 [condition_encode_def,word_index,w2w,word_lsl_def]); 495 496fun b_of_b t = (GEN_ALL o SIMP_RULE std_ss [BITS_THM] o 497 SPECL [`6`,`0`,`x`,t]) BIT_OF_BITS_THM2; 498 499val shift_encode_lem = prove( 500 `!r. (!i. 6 < i /\ i < 32 ==> ~(shift_encode r ' i)) /\ 501 ~(shift_encode r ' 4)`, 502 Cases \\ SIMP_TAC (arith_ss++fcpLib.FCP_ss++wordsLib.SIZES_ss) 503 [shift_encode_def,word_index,w2w,word_or_def, 504 b_of_b `32`, b_of_b `64`, b_of_b `96`] \\ EVAL_TAC); 505 506val extract_out_of_range = prove( 507 `!w:'a word i h. 508 (h + 1 - l < i) /\ i < dimindex(:'b) ==> ~((((h >< l) w):'b word) ' i)`, 509 SRW_TAC [ARITH_ss,fcpLib.FCP_ss] [word_extract_def,word_bits_def,w2w] 510 \\ Cases_on `i < dimindex (:'a)` \\ SRW_TAC [ARITH_ss,fcpLib.FCP_ss] []); 511 512val INDEX_RAND = 513 (GEN_ALL o SIMP_RULE bool_ss [] o ISPEC `\x:word32. x ' i`) COND_RAND; 514 515val BIT_NUMERAL = CONJ (SPECL [`0`,`NUMERAL n`] BIT_def) 516 (SPECL [`NUMERAL b`,`NUMERAL n`] BIT_def); 517 518val BITS_NUMERAL = (GEN_ALL o SPECL [`h`,`l`,`NUMERAL n`]) BITS_def; 519 520val BITS_NUMERAL_ss = let open numeral_bitTheory numeralTheory in rewrites 521 [BITS_NUMERAL, BITS_ZERO2, NUMERAL_DIV_2EXP, NUMERAL_iDIV2, 522 NUMERAL_SFUNPOW_iDIV2, NUMERAL_SFUNPOW_iDUB, NUMERAL_SFUNPOW_FDUB, 523 FDUB_iDIV2, FDUB_iDUB, FDUB_FDUB, iDUB_removal, 524 numeral_suc, numeral_imod_2exp, MOD_2EXP, NORM_0] 525end; 526 527val word_frags = [fcpLib.FCP_ss,wordsLib.SIZES_ss,BITS_NUMERAL_ss, 528 rewrites [SIMP_RULE std_ss [] DECODE_ARM_THM, INDEX_RAND,BIT_def, 529 shift_encode_lem,word_or_def,word_index,w2w,word_lsl_def, 530 condition_encode_lem,instruction_encode_def]]; 531 532(* ......................................................................... *) 533 534val decode_enc_br = store_thm("decode_enc_br", 535 `(!cond offset. DECODE_ARM (enc (instruction$B cond offset)) = br) /\ 536 (!cond offset. DECODE_ARM (enc (instruction$BL cond offset)) = br)`, 537 SRW_TAC word_frags []); 538 539val decode_enc_swi = store_thm("decode_enc_swi", 540 `!cond. DECODE_ARM (enc (instruction$SWI cond)) = swi_ex`, 541 SRW_TAC word_frags []); 542 543val decode_enc_data_proc_ = prove( 544 `!cond op s rd rn Op2. ~(op ' 3) \/ (op ' 2) ==> 545 (DECODE_ARM (data_proc_encode cond op s rn rd Op2) = data_proc)`, 546 Cases_on `Op2` 547 \\ SRW_TAC word_frags [data_proc_encode_def,addr_mode1_encode_def]); 548 549val decode_enc_data_proc__ = prove( 550 `!cond op s rd rn Op2. 551 (DECODE_ARM (data_proc_encode cond op T rd 0w Op2) = data_proc)`, 552 Cases_on `Op2` 553 \\ SRW_TAC word_frags [data_proc_encode_def,addr_mode1_encode_def]); 554 555val decode_enc_data_proc = prove( 556 `!f. f IN {instruction$AND; instruction$EOR; 557 instruction$SUB; instruction$RSB; 558 instruction$ADD; instruction$ADC; 559 instruction$SBC; instruction$RSC; 560 instruction$ORR; instruction$BIC} ==> 561 (!cond s rd rn Op2. DECODE_ARM (enc (f cond s rd rn Op2)) = data_proc)`, 562 SRW_TAC [] [instruction_encode_def] 563 \\ SRW_TAC [fcpLib.FCP_ss,wordsLib.SIZES_ss,BITS_NUMERAL_ss] 564 [BIT_def,word_index,decode_enc_data_proc_]); 565 566val decode_enc_data_proc2 = prove( 567 `!f. f IN {instruction$TST; instruction$TEQ; 568 instruction$CMP; instruction$CMN} ==> 569 (!cond rn Op2. DECODE_ARM (enc (f cond rn Op2)) = data_proc)`, 570 SRW_TAC [] [instruction_encode_def] \\ SRW_TAC [] [decode_enc_data_proc__]); 571 572val decode_enc_data_proc3 = prove( 573 `!f. f IN {instruction$MOV; instruction$MVN} ==> 574 (!cond s rd Op2. DECODE_ARM (enc (f cond s rd Op2)) = data_proc)`, 575 SRW_TAC [] [instruction_encode_def] 576 \\ SRW_TAC [fcpLib.FCP_ss,wordsLib.SIZES_ss,BITS_NUMERAL_ss] 577 [BIT_def,word_index,decode_enc_data_proc_]); 578 579val decode_enc_mla_mul = store_thm("decode_enc_mla_mul", 580 `(!cond s rd rm rs. 581 DECODE_ARM (enc (instruction$MUL cond s rd rm rs)) = mla_mul) /\ 582 (!cond s rd rm rs rn. 583 DECODE_ARM (enc (instruction$MLA cond s rd rm rs rn)) = mla_mul) /\ 584 (!cond s rdhi rdlo rm rs. 585 DECODE_ARM (enc (instruction$UMULL cond s rdlo rdhi rm rs)) = mla_mul) /\ 586 (!cond s rdhi rdlo rm rs. 587 DECODE_ARM (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) = mla_mul) /\ 588 (!cond s rdhi rdlo rm rs. 589 DECODE_ARM (enc (instruction$SMULL cond s rdlo rdhi rm rs)) = mla_mul) /\ 590 (!cond s rdhi rdlo rm rs. 591 DECODE_ARM (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) = mla_mul)`, 592 SRW_TAC word_frags []); 593 594val decode_enc_ldr_str = store_thm("decode_enc_ldr_str", 595 `(!cond b opt rd rn offset. 596 DECODE_ARM (enc (instruction$LDR cond b opt rd rn offset)) = ldr_str) /\ 597 (!cond b opt rd rn offset. 598 DECODE_ARM (enc (instruction$STR cond b opt rd rn offset)) = ldr_str)`, 599 REPEAT STRIP_TAC \\ Cases_on `offset` \\ TRY (Cases_on `s`) 600 \\ SRW_TAC word_frags [addr_mode2_encode_def,options_encode_def, 601 shift_encode_def,word_modify_def]); 602 603val decode_enc_ldrh_strh = store_thm("decode_enc_ldrh_strh", 604 `(!cond s h opt rd rn offset. 605 DECODE_ARM (enc (instruction$LDRH cond s h opt rd rn offset)) = 606 ldrh_strh) /\ 607 (!cond opt rd rn offset. 608 DECODE_ARM (enc (instruction$STRH cond opt rd rn offset)) = ldrh_strh)`, 609 REPEAT STRIP_TAC \\ Cases_on `offset` 610 \\ SRW_TAC word_frags [addr_mode3_encode_def,options_encode2_def, 611 word_modify_def,extract_out_of_range] 612 \\ METIS_TAC []); 613 614val decode_enc_ldm_stm = store_thm("decode_enc_ldm_stm", 615 `(!cond s opt rn list. 616 DECODE_ARM (enc (instruction$LDM cond s opt rn list)) = ldm_stm) /\ 617 (!cond s opt rn list. 618 DECODE_ARM (enc (instruction$STM cond s opt rn list)) = ldm_stm)`, 619 SRW_TAC word_frags [options_encode_def,word_modify_def]); 620 621val decode_enc_swp = store_thm("decode_enc_swp", 622 `!cond b rd rm rn. DECODE_ARM (enc (instruction$SWP cond b rd rm rn)) = swp`, 623 SRW_TAC word_frags []); 624 625val decode_enc_mrs = store_thm("decode_enc_mrs", 626 `!cond r rd. DECODE_ARM (enc (instruction$MRS cond r rd)) = mrs`, 627 SRW_TAC word_frags []); 628 629val decode_enc_msr = store_thm("decode_enc_msr", 630 `!cond psrd op. DECODE_ARM (enc (instruction$MSR cond psrd op)) = msr`, 631 REPEAT STRIP_TAC \\ Cases_on `psrd` \\ Cases_on `op` 632 \\ SRW_TAC word_frags [msr_psr_encode_def,msr_mode_encode_def]); 633 634val decode_enc_coproc = store_thm("decode_enc_coproc", 635 `(!cond cpn cop1 crd crn crm cop2. 636 DECODE_ARM (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = 637 cdp_und) /\ 638 (!cond. DECODE_ARM (enc (instruction$UND cond)) = cdp_und) /\ 639 (!cond cpn cop1 rd crn crm cop2. 640 DECODE_ARM (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = 641 mrc) /\ 642 (!cond cpn cop1 rd crn crm cop2. 643 DECODE_ARM (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = mcr) /\ 644 (!cond n opt cpn crd rn offset. 645 DECODE_ARM (enc (instruction$STC cond n opt cpn crd rn offset)) = 646 ldc_stc) /\ 647 (!cond n opt cpn crd rn offset. 648 DECODE_ARM (enc (instruction$LDC cond n opt cpn crd rn offset)) = 649 ldc_stc)`, 650 SRW_TAC word_frags [options_encode_def,word_modify_def]); 651 652val decode_cp_enc_coproc = store_thm("decode_cp_enc_coproc", 653 `(!cond cpn cop1 crd crn crm cop2. 654 DECODE_CP (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = 655 cdp_und) /\ 656 (!cond. DECODE_CP (enc (instruction$UND cond)) = cdp_und) /\ 657 (!cond cpn cop1 rd crn crm cop2. 658 DECODE_CP (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = mrc) /\ 659 (!cond cpn cop1 rd crn crm cop2. 660 DECODE_CP (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = mcr) /\ 661 (!cond n opt cpn crd rn offset. 662 DECODE_CP (enc (instruction$STC cond n opt cpn crd rn offset)) = 663 ldc_stc) /\ 664 (!cond n opt cpn crd rn offset. 665 DECODE_CP (enc (instruction$LDC cond n opt cpn crd rn offset)) = 666 ldc_stc)`, 667 SRW_TAC word_frags [DECODE_CP_def,options_encode_def,word_modify_def]); 668 669val decode_27_enc_coproc = store_thm("decode_27_enc_coproc", 670 `(!cond cpn cop1 crd crn crm cop2. 671 enc (instruction$CDP cond cpn cop1 crd crn crm cop2) ' 27) /\ 672 (!cond. enc (instruction$UND cond) ' 27 = F) /\ 673 (!cond cpn cop1 rd crn crm cop2. 674 enc (instruction$MRC cond cpn cop1 rd crn crm cop2) ' 27) /\ 675 (!cond cpn cop1 rd crn crm cop2. 676 enc (instruction$MCR cond cpn cop1 rd crn crm cop2) ' 27) /\ 677 (!cond n opt cpn crd rn offset. 678 enc (instruction$STC cond n opt cpn crd rn offset) ' 27) /\ 679 (!cond n opt cpn crd rn offset. 680 enc (instruction$LDC cond n opt cpn crd rn offset) ' 27)`, 681 SRW_TAC word_frags [options_encode_def,word_modify_def]); 682 683(* ......................................................................... *) 684 685val word_frags = 686 [ARITH_ss,fcpLib.FCP_ss,wordsLib.SIZES_ss,BITS_NUMERAL_ss, 687 rewrites [INDEX_RAND,word_or_def,word_index,w2w,word_lsl_def, 688 word_bits_def,word_extract_def,condition_encode_lem, 689 instruction_encode_def,shift_encode_lem,BIT_NUMERAL,BIT_ZERO]]; 690 691val decode_br_enc = store_thm("decode_br_enc", 692 `(!cond offset. 693 DECODE_BRANCH (enc (instruction$B cond offset)) = (F, offset)) /\ 694 (!cond offset. 695 DECODE_BRANCH (enc (instruction$BL cond offset)) = (T, offset))`, 696 SRW_TAC word_frags [DECODE_BRANCH_def] 697 \\ ASM_SIMP_TAC bool_ss [BIT_SHIFT_THM3, 698 (SYM o EVAL) ``11 * 2 ** 24``,(SYM o EVAL) ``10 * 2 ** 24``]); 699 700val shift_immediate_enc_lem = prove( 701 `(!i r. (w2w:word32->word8) 702 ((11 -- 7) (w2w (i:word5) << 7 || w2w (r:word4))) = w2w i) /\ 703 (!i r. (w2w:word32->word8) 704 ((11 -- 7) (w2w (i:word5) << 7 || 32w || w2w (r:word4))) = w2w i) /\ 705 (!i r. (w2w:word32->word8) 706 ((11 -- 7) (w2w (i:word5) << 7 || 64w || w2w (r:word4))) = w2w i) /\ 707 (!i r. (w2w:word32->word8) 708 ((11 -- 7) (w2w (i:word5) << 7 || 96w || w2w (r:word4))) = w2w i) /\ 709 (!i r. (w2w:word32->word2) ((6 -- 5) (i << 7 || w2w (r:word4))) = 0w) /\ 710 (!i r. (w2w:word32->word2) ((6 -- 5) (i << 7 || 32w || w2w (r:word4))) = 1w) /\ 711 (!i r. (w2w:word32->word2) ((6 -- 5) (i << 7 || 64w || w2w (r:word4))) = 2w) /\ 712 (!i r. (w2w:word32->word2) ((6 -- 5) (i << 7 || 96w || w2w (r:word4))) = 3w) /\ 713 (!i r. (w2w:word32->word4) ((3 -- 0) (i << 7 || w2w (r:word4))) = r) /\ 714 (!i r. (w2w:word32->word4) ((3 -- 0) (i << 7 || 32w || w2w (r:word4))) = r) /\ 715 (!i r. (w2w:word32->word4) ((3 -- 0) (i << 7 || 64w || w2w (r:word4))) = r) /\ 716 (!i r. (w2w:word32->word4) ((3 -- 0) (i << 7 || 96w || w2w (r:word4))) = r)`, 717 SRW_TAC word_frags [] \\ FULL_SIMP_TAC std_ss [LESS_THM] 718 \\ SRW_TAC word_frags []); 719 720val shift_immediate_enc_lem2 = prove( 721 `(!i r. (w2w:word32->word8) ((11 -- 7) 722 (33554432w || w2w (i:word5) << 7 || w2w (r:word4))) = w2w i) /\ 723 (!i r. (w2w:word32->word8) ((11 -- 7) 724 (33554432w || w2w (i:word5) << 7 || 32w || w2w (r:word4))) = w2w i) /\ 725 (!i r. (w2w:word32->word8) ((11 -- 7) 726 (33554432w || w2w (i:word5) << 7 || 64w || w2w (r:word4))) = w2w i) /\ 727 (!i r. (w2w:word32->word8) ((11 -- 7) 728 (33554432w || w2w (i:word5) << 7 || 96w || w2w (r:word4))) = w2w i) /\ 729 (!i r. (w2w:word32->word2) ((6 -- 5) 730 (33554432w || i << 7 || w2w (r:word4))) = 0w) /\ 731 (!i r. (w2w:word32->word2) ((6 -- 5) 732 (33554432w || i << 7 || 32w || w2w (r:word4))) = 1w) /\ 733 (!i r. (w2w:word32->word2) ((6 -- 5) 734 (33554432w || i << 7 || 64w || w2w (r:word4))) = 2w) /\ 735 (!i r. (w2w:word32->word2) ((6 -- 5) 736 (33554432w || i << 7 || 96w || w2w (r:word4))) = 3w) /\ 737 (!i r. (w2w:word32->word4) ((3 -- 0) 738 (33554432w || i << 7 || w2w (r:word4))) = r) /\ 739 (!i r. (w2w:word32->word4) ((3 -- 0) 740 (33554432w || i << 7 || 32w || w2w (r:word4))) = r) /\ 741 (!i r. (w2w:word32->word4) ((3 -- 0) 742 (33554432w || i << 7 || 64w || w2w (r:word4))) = r) /\ 743 (!i r. (w2w:word32->word4) ((3 -- 0) 744 (33554432w || i << 7 || 96w || w2w (r:word4))) = r)`, 745 SRW_TAC word_frags [] \\ FULL_SIMP_TAC std_ss [LESS_THM] 746 \\ SRW_TAC word_frags []); 747 748val shift_register_enc_lem = prove( 749 `(!i r. (w2w:word32->word4) ((11 -- 8) 750 (16w || w2w (i:word4) << 8 || w2w (r:word4))) = i) /\ 751 (!i r. (w2w:word32->word4) ((11 -- 8) 752 (16w || w2w (i:word4) << 8 || 32w || w2w (r:word4))) = i) /\ 753 (!i r. (w2w:word32->word4) ((11 -- 8) 754 (16w || w2w (i:word4) << 8 || 64w || w2w (r:word4))) = i) /\ 755 (!i r. (w2w:word32->word4) ((11 -- 8) 756 (16w || w2w (i:word4) << 8 || 96w || w2w (r:word4))) = i) /\ 757 (!i r. (w2w:word32->word2) ((6 -- 5) 758 (16w || i << 8 || w2w (r:word4))) = 0w) /\ 759 (!i r. (w2w:word32->word2) ((6 -- 5) 760 (16w || i << 8 || 32w || w2w (r:word4))) = 1w) /\ 761 (!i r. (w2w:word32->word2) ((6 -- 5) 762 (16w || i << 8 || 64w || w2w (r:word4))) = 2w) /\ 763 (!i r. (w2w:word32->word2) ((6 -- 5) 764 (16w || i << 8 || 96w || w2w (r:word4))) = 3w) /\ 765 (!i r. (w2w:word32->word4) ((3 -- 0) 766 (16w || i << 8 || w2w (r:word4))) = r) /\ 767 (!i r. (w2w:word32->word4) ((3 -- 0) 768 (16w || i << 8 || 32w || w2w (r:word4))) = r) /\ 769 (!i r. (w2w:word32->word4) ((3 -- 0) 770 (16w || i << 8 || 64w || w2w (r:word4))) = r) /\ 771 (!i r. (w2w:word32->word4) ((3 -- 0) 772 (16w || i << 8 || 96w || w2w (r:word4))) = r)`, 773 SRW_TAC word_frags [] \\ FULL_SIMP_TAC std_ss [LESS_THM] 774 \\ SRW_TAC word_frags []); 775 776val immediate_enc = store_thm("immediate_enc", 777 `(!c r i. IMMEDIATE c ((11 >< 0) (addr_mode1_encode (Dp_immediate r i))) = 778 arm$ROR (w2w i) (2w * w2w r) c) /\ 779 !c r i. IMMEDIATE c ((11 >< 0) (msr_mode_encode (Msr_immediate r i))) = 780 arm$ROR (w2w i) (2w * w2w r) c`, 781 SRW_TAC (boolSimps.LET_ss::word_frags) 782 [IMMEDIATE_def,addr_mode1_encode_def,msr_mode_encode_def] 783 \\ (MATCH_MP_TAC (METIS_PROVE [] ``!a b c d x. (a = b) /\ (c = d) ==> 784 (ROR a c x = ROR b d x)``) 785 \\ STRIP_TAC << [ALL_TAC, 786 MATCH_MP_TAC (PROVE [] ``!a b. (a = b) ==> (2w:word8 * a = 2w * b)``)] 787 \\ SRW_TAC word_frags [WORD_EQ] 788 << [Cases_on `i' < 12` \\ SRW_TAC word_frags [] 789 \\ Cases_on `i' < 8` \\ SRW_TAC word_frags [], 790 Cases_on `i' < 4` \\ SRW_TAC word_frags []] 791 \\ POP_ASSUM_LIST (ASSUME_TAC o hd) 792 \\ FULL_SIMP_TAC std_ss [LESS_THM] 793 \\ SRW_TAC word_frags [])); 794 795val immediate_enc2 = store_thm("immediate_enc2", 796 `!i. (11 >< 0) (addr_mode2_encode (Dt_immediate i)) = i`, 797 SRW_TAC word_frags [addr_mode2_encode_def,w2w] 798 \\ Cases_on `i' < 12` \\ SRW_TAC word_frags []); 799 800val immediate_enc3 = store_thm("immediate_enc3", 801 `(!i. (11 >< 8) (addr_mode3_encode (Dth_immediate i)) = (7 >< 4) i) /\ 802 !i. (3 >< 0) (addr_mode3_encode (Dth_immediate i)) = (3 >< 0) i`, 803 SRW_TAC word_frags [addr_mode3_encode_def,w2w] 804 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 805 806val register_enc3 = store_thm("register_enc3", 807 `!i. (3 >< 0) (addr_mode3_encode (Dth_register r)) = r`, 808 SRW_TAC word_frags [addr_mode3_encode_def,w2w]); 809 810val lem = simpLib.SIMP_PROVE (std_ss++WORD_BIT_EQ_ss) [] 811 ``~(i = 0w:word5) ==> ~((4 >< 0) i = 0w:word8)``; 812 813val lem2 = simpLib.SIMP_PROVE (std_ss++WORD_ARITH_ss++WORD_ARITH_EQ_ss) [] 814 ``-1w = 3w:word2``; 815 816val shift_immediate_enc = store_thm("shift_immediate_enc", 817 `!reg m c sh i. SHIFT_IMMEDIATE reg m c 818 ((11 >< 0) (addr_mode1_encode (Dp_shift_immediate sh i))) = 819 if i = 0w then 820 case sh of 821 LSL Rm => arm$LSL (REG_READ reg m Rm) 0w c 822 | LSR Rm => arm$LSR (REG_READ reg m Rm) 32w c 823 | ASR Rm => arm$ASR (REG_READ reg m Rm) 32w c 824 | ROR Rm => word_rrx(c, REG_READ reg m Rm) 825 else 826 case sh of 827 LSL Rm => arm$LSL (REG_READ reg m Rm) (w2w i) c 828 | LSR Rm => arm$LSR (REG_READ reg m Rm) (w2w i) c 829 | ASR Rm => arm$ASR (REG_READ reg m Rm) (w2w i) c 830 | ROR Rm => arm$ROR (REG_READ reg m Rm) (w2w i) c`, 831 REPEAT STRIP_TAC \\ Cases_on `sh` \\ Cases_on `i = 0w` \\ IMP_RES_TAC lem 832 \\ SRW_TAC [boolSimps.LET_ss, WORD_EXTRACT_ss] 833 [SHIFT_IMMEDIATE_def,SHIFT_IMMEDIATE2_def,addr_mode1_encode_def, 834 shift_encode_def,shift_immediate_enc_lem,lem2]); 835 836val shift_immediate_enc2 = store_thm("shift_immediate_enc2", 837 `!reg m c sh i. SHIFT_IMMEDIATE reg m c 838 ((11 >< 0) (addr_mode2_encode (Dt_shift_immediate sh i))) = 839 if i = 0w then 840 case sh of 841 LSL Rm => arm$LSL (REG_READ reg m Rm) 0w c 842 | LSR Rm => arm$LSR (REG_READ reg m Rm) 32w c 843 | ASR Rm => arm$ASR (REG_READ reg m Rm) 32w c 844 | ROR Rm => word_rrx(c, REG_READ reg m Rm) 845 else 846 case sh of 847 LSL Rm => arm$LSL (REG_READ reg m Rm) (w2w i) c 848 | LSR Rm => arm$LSR (REG_READ reg m Rm) (w2w i) c 849 | ASR Rm => arm$ASR (REG_READ reg m Rm) (w2w i) c 850 | ROR Rm => arm$ROR (REG_READ reg m Rm) (w2w i) c`, 851 REPEAT STRIP_TAC \\ Cases_on `sh` \\ Cases_on `i = 0w` \\ IMP_RES_TAC lem 852 \\ SRW_TAC [boolSimps.LET_ss, WORD_EXTRACT_ss] 853 [SHIFT_IMMEDIATE_def,SHIFT_IMMEDIATE2_def,addr_mode2_encode_def, 854 shift_encode_def,shift_immediate_enc_lem2,lem2]); 855 856val shift_register_enc = store_thm("shift_register_enc", 857 `!reg m c sh r. SHIFT_REGISTER reg m c 858 ((11 >< 0) (addr_mode1_encode (Dp_shift_register sh r))) = 859 let rs = (7 >< 0) (REG_READ reg m r) in 860 case sh of 861 LSL Rm => arm$LSL (REG_READ (INC_PC reg) m Rm) rs c 862 | LSR Rm => arm$LSR (REG_READ (INC_PC reg) m Rm) rs c 863 | ASR Rm => arm$ASR (REG_READ (INC_PC reg) m Rm) rs c 864 | ROR Rm => arm$ROR (REG_READ (INC_PC reg) m Rm) rs c`, 865 REPEAT STRIP_TAC \\ Cases_on `sh` 866 \\ SRW_TAC [boolSimps.LET_ss, WORD_EXTRACT_ss] 867 [SHIFT_REGISTER_def,SHIFT_REGISTER2_def,addr_mode1_encode_def, 868 shift_encode_def,shift_register_enc_lem,lem2]); 869 870val shift_register_enc2 = store_thm("shift_register_enc2", 871 `!r. (3 >< 0) ((11 >< 0) (msr_mode_encode (Msr_register r))) = r`, 872 SRW_TAC (boolSimps.LET_ss::word_frags) [msr_mode_encode_def]); 873 874val shift_immediate_shift_register = store_thm("shift_immediate_shift_register", 875 `(!reg m c sh r. 876 (11 >< 0) (addr_mode1_encode (Dp_shift_register sh r)) ' 4) /\ 877 (!reg m c sh i. 878 ~((11 >< 0) (addr_mode1_encode (Dp_shift_immediate sh i)) ' 4))`, 879 NTAC 6 STRIP_TAC \\ Cases_on `sh` 880 \\ SRW_TAC word_frags [addr_mode1_encode_def]); 881 882val decode_data_proc_enc_ = prove( 883 `!cond op s rd rn Op2. 884 DECODE_DATAP (data_proc_encode cond op s rn rd Op2) = 885 (IS_DP_IMMEDIATE Op2,op,s,rn,rd,(11 >< 0) (addr_mode1_encode Op2))`, 886 Cases_on `Op2` 887 \\ SRW_TAC word_frags [IS_DP_IMMEDIATE_def,DECODE_DATAP_def, 888 addr_mode1_encode_def,data_proc_encode_def] 889 \\ ASM_SIMP_TAC bool_ss [BIT_SHIFT_THM3,(SYM o EVAL) ``256 * 2 ** 12``] 890 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 891 892val decode_data_proc_enc = prove( 893 `!f. f IN {instruction$AND; instruction$EOR; 894 instruction$SUB; instruction$RSB; 895 instruction$ADD; instruction$ADC; 896 instruction$SBC; instruction$RSC; 897 instruction$ORR; instruction$BIC} ==> 898 (!cond s rd rn Op2. 899 DECODE_DATAP (enc (f cond s rd rn Op2)) = 900 (IS_DP_IMMEDIATE Op2,decode_opcode (f cond s rd rn Op2), 901 s,rn,rd,(11 >< 0) (addr_mode1_encode Op2)))`, 902 SRW_TAC [] [instruction_encode_def,decode_opcode_def] 903 \\ SRW_TAC [] [decode_data_proc_enc_]); 904 905val decode_data_proc_enc2 = prove( 906 `!f. f IN {instruction$TST; instruction$TEQ; 907 instruction$CMP; instruction$CMN} ==> 908 (!cond rn Op2. 909 DECODE_DATAP (enc (f cond rn Op2)) = 910 (IS_DP_IMMEDIATE Op2,decode_opcode (f cond rn Op2), 911 T,rn,0w,(11 >< 0) (addr_mode1_encode Op2)))`, 912 SRW_TAC [] [instruction_encode_def,decode_opcode_def] 913 \\ SRW_TAC [] [decode_data_proc_enc_]); 914 915val decode_data_proc_enc3 = prove( 916 `!f. f IN {instruction$MOV; instruction$MVN} ==> 917 (!cond s rd Op2. 918 DECODE_DATAP (enc (f cond s rd Op2)) = 919 (IS_DP_IMMEDIATE Op2,decode_opcode (f cond s rd Op2), 920 s,0w,rd,(11 >< 0) (addr_mode1_encode Op2)))`, 921 SRW_TAC [] [instruction_encode_def,decode_opcode_def] 922 \\ SRW_TAC [] [decode_data_proc_enc_]); 923 924val decode_mla_mul_enc = store_thm("decode_mla_mul_enc", 925 `(!cond s rd rm rs. 926 DECODE_MLA_MUL (enc (instruction$MUL cond s rd rm rs)) = 927 (F,F,F,s,rd,0w,rs,rm)) /\ 928 (!cond s rd rm rs rn. 929 DECODE_MLA_MUL (enc (instruction$MLA cond s rd rm rs rn)) = 930 (F,F,T,s,rd,rn,rs,rm)) /\ 931 (!cond s rdhi rdlo rm rs. 932 DECODE_MLA_MUL (enc (instruction$UMULL cond s rdlo rdhi rm rs)) = 933 (T,F,F,s,rdhi,rdlo,rs,rm)) /\ 934 (!cond s rdhi rdlo rm rs. 935 DECODE_MLA_MUL (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) = 936 (T,F,T,s,rdhi,rdlo,rs,rm)) /\ 937 (!cond s rdhi rdlo rm rs. 938 DECODE_MLA_MUL (enc (instruction$SMULL cond s rdlo rdhi rm rs)) = 939 (T,T,F,s,rdhi,rdlo,rs,rm)) /\ 940 (!cond s rdhi rdlo rm rs. 941 DECODE_MLA_MUL (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) = 942 (T,T,T,s,rdhi,rdlo,rs,rm))`, 943 REPEAT STRIP_TAC \\ SRW_TAC word_frags [DECODE_MLA_MUL_def] 944 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 945 946val decode_ldr_str_enc = Count.apply store_thm("decode_ldr_str_enc", 947 `(!cond b opt rd rn offset. 948 DECODE_LDR_STR (enc (instruction$LDR cond b opt rd rn offset)) = 949 (IS_DT_SHIFT_IMMEDIATE offset, opt.Pre, opt.Up, b, opt.Wb, 950 T, rn, rd, (11 >< 0) (addr_mode2_encode offset))) /\ 951 (!cond b opt rd rn offset. 952 DECODE_LDR_STR (enc (instruction$STR cond b opt rd rn offset)) = 953 (IS_DT_SHIFT_IMMEDIATE offset, opt.Pre, opt.Up, b, opt.Wb, 954 F, rn, rd, (11 >< 0) (addr_mode2_encode offset)))`, 955 REPEAT STRIP_TAC \\ Cases_on `offset` \\ TRY (Cases_on `sh`) 956 \\ SRW_TAC word_frags [DECODE_LDR_STR_def,IS_DT_SHIFT_IMMEDIATE_def, 957 addr_mode2_encode_def,options_encode_def,word_modify_def] 958 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 959 960val decode_ldrh_strh_enc = Count.apply store_thm("decode_ldrh_strh_enc", 961 `(!cond s h opt rd rn offset. 962 DECODE_LDRH_STRH (enc (instruction$LDRH cond s h opt rd rn offset)) = 963 let x = addr_mode3_encode offset in 964 (opt.Pre, opt.Up, IS_DTH_IMMEDIATE offset, opt.Wb, T, 965 rn, rd, (11 >< 8) x, s, h \/ (~h /\ ~s), (3 >< 0) x)) /\ 966 (!cond opt rd rn offset. 967 DECODE_LDRH_STRH (enc (instruction$STRH cond opt rd rn offset)) = 968 let x = addr_mode3_encode offset in 969 (opt.Pre, opt.Up, IS_DTH_IMMEDIATE offset, opt.Wb, F, 970 rn, rd, (11 >< 8) x, F, T, (3 >< 0) x))`, 971 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ Cases_on `offset` 972 \\ SRW_TAC word_frags [DECODE_LDRH_STRH_def,IS_DTH_IMMEDIATE_def, 973 addr_mode3_encode_def,options_encode2_def,word_modify_def] 974 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 975 976val decode_ldm_stm_enc = store_thm("decode_ldm_stm_enc", 977 `(!cond s opt rn l. 978 DECODE_LDM_STM (enc (instruction$LDM cond s opt rn l)) = 979 (opt.Pre, opt.Up, s, opt.Wb, T, rn, l)) /\ 980 (!cond s opt rn l. 981 DECODE_LDM_STM (enc (instruction$STM cond s opt rn l)) = 982 (opt.Pre, opt.Up, s, opt.Wb, F, rn, l))`, 983 SRW_TAC word_frags [DECODE_LDM_STM_def,options_encode_def,word_modify_def] 984 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 985 986val decode_swp_enc = store_thm("decode_swp_enc", 987 `!cond b rd rm rn. 988 DECODE_SWP (enc (instruction$SWP cond b rd rm rn)) = (b,rn,rd,rm)`, 989 SRW_TAC word_frags [DECODE_SWP_def] \\ FULL_SIMP_TAC std_ss [LESS_THM] 990 \\ SRW_TAC word_frags []); 991 992val decode_mrs_enc = store_thm("decode_mrs_enc", 993 `!cond r rd. DECODE_MRS (enc (instruction$MRS cond r rd)) = (r, rd)`, 994 SRW_TAC word_frags [DECODE_MRS_def] 995 \\ ASM_SIMP_TAC (bool_ss++ARITH_ss) [BIT_SHIFT_THM3, 996 (SYM o EVAL) ``271 * 2 ** 16``,(SYM o EVAL) ``335 * 2 ** 16``]); 997 998val decode_msr_enc = store_thm("decode_msr_enc", 999 `!cond psrd Op2. 1000 DECODE_MSR (enc (instruction$MSR cond psrd Op2)) = 1001 let (r,bit19,bit16) = DECODE_PSRD psrd 1002 and opnd = (11 >< 0) (msr_mode_encode Op2) in 1003 (IS_MSR_IMMEDIATE Op2,r,bit19,bit16,(3 >< 0) opnd,opnd)`, 1004 REPEAT STRIP_TAC \\ Cases_on `Op2` \\ Cases_on `psrd` 1005 \\ SRW_TAC (boolSimps.LET_ss::word_frags) [DECODE_MSR_def,DECODE_PSRD_def, 1006 IS_MSR_IMMEDIATE_def,msr_psr_encode_def,msr_mode_encode_def] 1007 \\ ASM_SIMP_TAC (bool_ss++ARITH_ss) [BIT_SHIFT_THM3, 1008 (SYM o EVAL) ``4623 * 2 ** 12``, (SYM o EVAL) ``1168 * 2 ** 12``, 1009 (SYM o EVAL) ``1152 * 2 ** 12``, (SYM o EVAL) ``1040 * 2 ** 12``, 1010 (SYM o EVAL) ``144 * 2 ** 12``, (SYM o EVAL) ``128 * 2 ** 12``, 1011 (SYM o EVAL) ``16 * 2 ** 12``]); 1012 1013val decode_mrc_mcr_rd_enc = store_thm("decode_mrc_mcr_rd_enc", 1014 `(!cond cpn cop1 rd crn crm cop2. 1015 (15 >< 12) (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = rd) /\ 1016 !cond cpn cop1 rd crn crm cop2. 1017 (15 >< 12) (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = rd`, 1018 SRW_TAC word_frags [] \\ FULL_SIMP_TAC std_ss [LESS_THM] 1019 \\ SRW_TAC word_frags []); 1020 1021val decode_ldc_stc_enc = store_thm("decode_ldc_stc_enc", 1022 `(!cond n opt cpn crd rn offset. 1023 DECODE_LDC_STC (enc (instruction$LDC cond n opt cpn crd rn offset)) = 1024 (opt.Pre, opt.Up, n, opt.Wb, T, rn, crd, cpn, offset)) /\ 1025 (!cond n opt cpn crd rn offset. 1026 DECODE_LDC_STC (enc (instruction$STC cond n opt cpn crd rn offset)) = 1027 (opt.Pre, opt.Up, n, opt.Wb, F, rn, crd, cpn, offset))`, 1028 SRW_TAC word_frags [DECODE_LDC_STC_def,options_encode_def,word_modify_def] 1029 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 1030 1031val decode_ldc_stc_20_enc = store_thm("decode_ldc_stc_20_enc", 1032 `(!cond n opt cpn crd rn offset. 1033 enc (instruction$LDC cond n opt cpn crd rn offset) ' 20) /\ 1034 !cond n opt cpn crd rn offset. 1035 ~(enc (instruction$STC cond n opt cpn crd rn offset) ' 20)`, 1036 SRW_TAC word_frags [DECODE_LDC_STC_def,options_encode_def,word_modify_def] 1037 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 1038 1039val decode_cdp_enc = store_thm("decode_cdp_enc", 1040 `(!cond cpn cop1 crd crn crm cop2. 1041 DECODE_CDP (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = 1042 (cop1,crn,crd,cpn,cop2,crm)) /\ 1043 !cond cpn cop1 crd crn crm cop2. 1044 DECODE_CPN (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = cpn`, 1045 SRW_TAC word_frags [DECODE_CDP_def,DECODE_CPN_def] 1046 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 1047 1048val decode_mrc_mcr_enc = store_thm("decode_mrc_mcr_enc", 1049 `(!cond cpn cop1 rd crn crm cop2. 1050 DECODE_MRC_MCR (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = 1051 (cop1,crn,rd,cpn,cop2,crm)) /\ 1052 (!cond cpn cop1 rd crn crm cop2. 1053 DECODE_CPN (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = cpn) /\ 1054 (!cond cpn cop1 rd crn crm cop2. 1055 DECODE_MRC_MCR (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = 1056 (cop1,crn,rd,cpn,cop2,crm)) /\ 1057 (!cond cpn cop1 rd crn crm cop2. 1058 DECODE_CPN (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = cpn)`, 1059 SRW_TAC word_frags [DECODE_MRC_MCR_def,DECODE_CPN_def] 1060 \\ FULL_SIMP_TAC std_ss [LESS_THM] \\ SRW_TAC word_frags []); 1061 1062(* ......................................................................... *) 1063 1064val BITS_ZERO5 = prove( 1065 `!h l n. n < 2 ** l ==> (BITS h l n = 0)`, 1066 SRW_TAC [] [BITS_THM,LESS_DIV_EQ_ZERO,ZERO_LT_TWOEXP]); 1067 1068val BITS_w2n_ZERO = prove( 1069 `!w: bool ** 'a. dimindex (:'a) <= l ==> (BITS h l (w2n w) = 0)`, 1070 METIS_TAC [dimword_def,TWOEXP_MONO2,LESS_LESS_EQ_TRANS,BITS_ZERO5,w2n_lt]); 1071 1072val WORD_BITS_LSL = prove( 1073 `!h l n w:bool ** 'a. 1074 n <= h /\ n <= l /\ l <= h /\ h < dimindex (:'a) ==> 1075 ((h -- l) (w << n) = ((h - n) -- (l - n)) w)`, 1076 SRW_TAC [fcpLib.FCP_ss] [WORD_EQ,word_lsl_def,word_bits_def] 1077 \\ Cases_on `i + l < dimindex (:'a)` 1078 \\ FULL_SIMP_TAC (arith_ss++fcpLib.FCP_ss) [NOT_LESS_EQUAL,NOT_LESS]); 1079 1080val condition_code_lem = prove( 1081 `!cond. condition_encode cond ' 28 = cond IN {NE;CC;PL;VC;LS;LT;LE;NV}`, 1082 Cases \\ RW_TAC (std_ss++wordsLib.SIZES_ss++ 1083 pred_setSimps.PRED_SET_ss++BITS_NUMERAL_ss) 1084 [BIT_def,condition2num_thm,word_rol_def,word_ror_n2w,word_lsl_n2w, 1085 w2w_n2w,word_index,condition_encode_def]); 1086 1087val condition_code_lem2 = prove( 1088 `!cond. ~(condition_encode cond ' 28) = cond IN {EQ;CS;MI;VS;HI;GE;GT;AL}`, 1089 Cases \\ SRW_TAC [] [condition_code_lem]); 1090 1091val condition_code_lem = 1092 SIMP_RULE (bool_ss++pred_setSimps.PRED_SET_ss) [] condition_code_lem; 1093 1094val condition_code_lem2 = 1095 SIMP_RULE (bool_ss++pred_setSimps.PRED_SET_ss) [] condition_code_lem2; 1096 1097val condition_code_lem3 = prove( 1098 `!cond. num2condition (w2n ((31 -- 29) (condition_encode cond))) = 1099 case cond of 1100 EQ => EQ | NE => EQ | CS => CS | CC => CS 1101 | MI => MI | PL => MI | VS => VS | VC => VS 1102 | HI => HI | LS => HI | GE => GE | LT => GE 1103 | GT => GT | LE => GT | AL => AL | NV => AL`, 1104 Cases \\ SRW_TAC [boolSimps.LET_ss] 1105 [condition_encode_def,condition2num_thm,num2condition_thm,word_bits_n2w, 1106 word_rol_def,word_ror_n2w,word_lsl_n2w,w2w_n2w,w2n_n2w] 1107 \\ EVAL_TAC ); 1108 1109val word_ss = srw_ss()++fcpLib.FCP_ss++wordsLib.SIZES_ss++BITS_NUMERAL_ss++ 1110 rewrites [word_or_def,word_index,w2w,word_lsl_def,word_bits_def, 1111 shift_encode_lem,BIT_def]; 1112 1113val pass_frags = 1114 [ARITH_ss,wordsLib.SIZES_ss,BITS_NUMERAL_ss,boolSimps.LET_ss, 1115 rewrites [CONDITION_PASSED_def,CONDITION_PASSED2_def, 1116 GSYM WORD_BITS_OVER_BITWISE,WORD_OR_CLAUSES,BITS_w2n_ZERO,WORD_BITS_LSL, 1117 word_bits_n2w,w2w_def,instruction_encode_def,condition_code_lem3]]; 1118 1119val condition_addr_mode1 = prove( 1120 `(!op2. (31 -- 29) (addr_mode1_encode op2) = 0w) /\ 1121 !op2. ~((addr_mode1_encode op2) ' 28)`, 1122 NTAC 2 STRIP_TAC \\ Cases_on `op2` \\ TRY (Cases_on `s`) 1123 \\ SRW_TAC [WORD_BIT_EQ_ss] [addr_mode1_encode_def,shift_encode_def]); 1124 1125val condition_addr_mode2 = prove( 1126 `(!op2. (31 -- 29) (addr_mode2_encode op2) = 0w) /\ 1127 !op2. ~((addr_mode2_encode op2) ' 28)`, 1128 NTAC 2 STRIP_TAC \\ Cases_on `op2` \\ TRY (Cases_on `s`) 1129 \\ SRW_TAC [WORD_BIT_EQ_ss] [addr_mode2_encode_def,shift_encode_def]); 1130 1131val condition_addr_mode3 = prove( 1132 `(!op2. (31 -- 29) (addr_mode3_encode op2) = 0w) /\ 1133 !op2. ~((addr_mode3_encode op2) ' 28)`, 1134 NTAC 2 STRIP_TAC \\ Cases_on `op2` 1135 \\ SRW_TAC [WORD_BIT_EQ_ss] [addr_mode3_encode_def]); 1136 1137val condition_msr_mode = prove( 1138 `(!op2. (31 -- 29) (msr_mode_encode op2) = 0w) /\ 1139 !op2. ~((msr_mode_encode op2) ' 28)`, 1140 NTAC 2 STRIP_TAC \\ Cases_on `op2` 1141 \\ SRW_TAC [WORD_BIT_EQ_ss] [msr_mode_encode_def]); 1142 1143val condition_msr_psr = prove( 1144 `(!psrd. (31 -- 29) (msr_psr_encode psrd) = 0w) /\ 1145 !psrd. ~((msr_psr_encode psrd) ' 28)`, 1146 NTAC 2 STRIP_TAC \\ Cases_on `psrd` 1147 \\ SRW_TAC [WORD_BIT_EQ_ss] [msr_psr_encode_def]); 1148 1149val condition_options = prove( 1150 `(!x opt. (31 -- 29) (options_encode x opt) = 0w) /\ 1151 !x opt. ~((options_encode x opt) ' 28)`, 1152 NTAC 2 STRIP_TAC 1153 \\ SRW_TAC [WORD_BIT_EQ_ss] [options_encode_def,word_modify_def]); 1154 1155val condition_options2 = prove( 1156 `(!x opt. (31 -- 29) (options_encode2 x opt) = 0w) /\ 1157 !x opt. ~((options_encode2 x opt) ' 28)`, 1158 NTAC 2 STRIP_TAC 1159 \\ SRW_TAC [WORD_BIT_EQ_ss] [options_encode2_def,word_modify_def]); 1160 1161val PASS_TAC = REPEAT STRIP_TAC \\ Cases_on_nzcv `flgs` 1162 \\ SRW_TAC pass_frags [condition_addr_mode1,condition_addr_mode2, 1163 condition_addr_mode3,condition_msr_mode,condition_msr_psr, 1164 condition_options,condition_options2,data_proc_encode_def] 1165 \\ FULL_SIMP_TAC word_ss [BITS_w2n_ZERO,condition_addr_mode1, 1166 condition_addr_mode2,condition_addr_mode3,condition_msr_mode, 1167 condition_msr_psr,condition_options,condition_options2] 1168 \\ RULE_ASSUM_TAC (REWRITE_RULE [condition_code_lem2]) 1169 \\ FULL_SIMP_TAC (srw_ss()) [condition_code_lem]; 1170 1171(* ......................................................................... *) 1172 1173val cond_pass_enc_br = store_thm("cond_pass_enc_br", 1174 `(!cond flgs offset. 1175 CONDITION_PASSED flgs (enc (instruction$B cond offset)) = 1176 CONDITION_PASSED2 flgs cond) /\ 1177 (!cond flgs offset. 1178 CONDITION_PASSED flgs (enc (instruction$BL cond offset)) = 1179 CONDITION_PASSED2 flgs cond)`, 1180 PASS_TAC); 1181 1182val cond_pass_enc_swi = store_thm("cond_pass_enc_swi", 1183 `!cond flgs. CONDITION_PASSED flgs (enc (instruction$SWI cond)) = 1184 CONDITION_PASSED2 flgs cond`, 1185 PASS_TAC); 1186 1187val cond_pass_enc_data_proc_ = prove( 1188 `!cond op s rd rn op2. 1189 CONDITION_PASSED flgs (data_proc_encode cond op s rd rn op2) = 1190 CONDITION_PASSED2 flgs cond`, 1191 PASS_TAC); 1192 1193val cond_pass_enc_data_proc = prove( 1194 `!f. f IN {instruction$AND; instruction$EOR; 1195 instruction$SUB; instruction$RSB; 1196 instruction$ADD; instruction$ADC; 1197 instruction$SBC; instruction$RSC; 1198 instruction$ORR; instruction$BIC} ==> 1199 (!cond s rd rn op2. 1200 CONDITION_PASSED flgs (enc (f cond s rd rn op2)) = 1201 CONDITION_PASSED2 flgs cond)`, 1202 SRW_TAC [] [instruction_encode_def] \\ SRW_TAC [] [cond_pass_enc_data_proc_]); 1203 1204val cond_pass_enc_data_proc2 = prove( 1205 `!f. f IN {instruction$TST; instruction$TEQ; 1206 instruction$CMP; instruction$CMN} ==> 1207 (!cond rn op2. 1208 CONDITION_PASSED flgs (enc (f cond rn op2)) = 1209 CONDITION_PASSED2 flgs cond)`, 1210 SRW_TAC [] [instruction_encode_def] \\ SRW_TAC [] [cond_pass_enc_data_proc_]); 1211 1212val cond_pass_enc_data_proc3 = prove( 1213 `!f. f IN {instruction$MOV; instruction$MVN} ==> 1214 (!cond s rd op2. 1215 CONDITION_PASSED flgs (enc (f cond s rd op2)) = 1216 CONDITION_PASSED2 flgs cond)`, 1217 SRW_TAC [] [instruction_encode_def] \\ SRW_TAC [] [cond_pass_enc_data_proc_]); 1218 1219val cond_pass_enc_mla_mul = store_thm("cond_pass_enc_mla_mul", 1220 `(!cond s rd rm rs. 1221 CONDITION_PASSED flgs (enc (instruction$MUL cond s rd rm rs)) = 1222 CONDITION_PASSED2 flgs cond) /\ 1223 (!cond s rd rm rs rn. 1224 CONDITION_PASSED flgs (enc (instruction$MLA cond s rd rm rs rn)) = 1225 CONDITION_PASSED2 flgs cond) /\ 1226 (!cond s rdhi rdlo rm rs. 1227 CONDITION_PASSED flgs (enc (instruction$UMULL cond s rdlo rdhi rm rs)) = 1228 CONDITION_PASSED2 flgs cond) /\ 1229 (!cond s rdhi rdlo rm rs. 1230 CONDITION_PASSED flgs (enc (instruction$UMLAL cond s rdlo rdhi rm rs)) = 1231 CONDITION_PASSED2 flgs cond) /\ 1232 (!cond s rdhi rdlo rm rs. 1233 CONDITION_PASSED flgs (enc (instruction$SMULL cond s rdlo rdhi rm rs)) = 1234 CONDITION_PASSED2 flgs cond) /\ 1235 (!cond s rdhi rdlo rm rs. 1236 CONDITION_PASSED flgs (enc (instruction$SMLAL cond s rdlo rdhi rm rs)) = 1237 CONDITION_PASSED2 flgs cond)`, 1238 PASS_TAC); 1239 1240val cond_pass_enc_ldr_str = store_thm("cond_pass_enc_ldr_str", 1241 `(!cond b opt rd rn offset. 1242 CONDITION_PASSED flgs (enc (instruction$LDR cond b opt rd rn offset)) = 1243 CONDITION_PASSED2 flgs cond) /\ 1244 (!cond b opt rd rn offset. 1245 CONDITION_PASSED flgs (enc (instruction$STR cond b opt rd rn offset)) = 1246 CONDITION_PASSED2 flgs cond)`, 1247 PASS_TAC); 1248 1249val cond_pass_enc_ldrh_strh = store_thm("cond_pass_enc_ldrh_strh", 1250 `(!cond s h opt rd rn offset. 1251 CONDITION_PASSED flgs (enc (instruction$LDRH cond s h opt rd rn offset)) = 1252 CONDITION_PASSED2 flgs cond) /\ 1253 (!cond opt rd rn offset. 1254 CONDITION_PASSED flgs (enc (instruction$STRH cond opt rd rn offset)) = 1255 CONDITION_PASSED2 flgs cond)`, 1256 PASS_TAC); 1257 1258val cond_pass_enc_ldm_stm = store_thm("cond_pass_enc_ldm_stm", 1259 `(!cond s opt rn list. 1260 CONDITION_PASSED flgs (enc (instruction$LDM cond s opt rn list)) = 1261 CONDITION_PASSED2 flgs cond) /\ 1262 (!cond s opt rn list. 1263 CONDITION_PASSED flgs (enc (instruction$STM cond s opt rn list)) = 1264 CONDITION_PASSED2 flgs cond)`, 1265 PASS_TAC); 1266 1267val cond_pass_enc_swp = store_thm("cond_pass_enc_swp", 1268 `!cond b rd rm rn. 1269 CONDITION_PASSED flgs (enc (instruction$SWP cond b rd rm rn)) = 1270 CONDITION_PASSED2 flgs cond`, 1271 PASS_TAC); 1272 1273val cond_pass_enc_mrs = store_thm("cond_pass_enc_mrs", 1274 `!cond r rd. 1275 CONDITION_PASSED flgs (enc (instruction$MRS cond r rd)) = 1276 CONDITION_PASSED2 flgs cond`, 1277 PASS_TAC); 1278 1279val cond_pass_enc_msr = store_thm("cond_pass_enc_msr", 1280 `!cond psrd op. 1281 CONDITION_PASSED flgs (enc (instruction$MSR cond psrd op)) = 1282 CONDITION_PASSED2 flgs cond`, 1283 PASS_TAC); 1284 1285val cond_pass_enc_coproc = store_thm("cond_pass_enc_coproc", 1286 `(!cond cpn cop1 crd crn crm cop2. 1287 CONDITION_PASSED flgs 1288 (enc (instruction$CDP cond cpn cop1 crd crn crm cop2)) = 1289 CONDITION_PASSED2 flgs cond) /\ 1290 (!cond. CONDITION_PASSED flgs (enc (instruction$UND cond)) = 1291 CONDITION_PASSED2 flgs cond) /\ 1292 (!cond cpn cop1 rd crn crm cop2. 1293 CONDITION_PASSED flgs 1294 (enc (instruction$MRC cond cpn cop1 rd crn crm cop2)) = 1295 CONDITION_PASSED2 flgs cond) /\ 1296 (!cond cpn cop1 rd crn crm cop2. 1297 CONDITION_PASSED flgs 1298 (enc (instruction$MCR cond cpn cop1 rd crn crm cop2)) = 1299 CONDITION_PASSED2 flgs cond) /\ 1300 (!cond n opt cpn crd rn offset. 1301 CONDITION_PASSED flgs 1302 (enc (instruction$STC cond n opt cpn crd rn offset)) = 1303 CONDITION_PASSED2 flgs cond) /\ 1304 (!cond n opt cpn crd rn offset. 1305 CONDITION_PASSED flgs 1306 (enc (instruction$LDC cond n opt cpn crd rn offset)) = 1307 CONDITION_PASSED2 flgs cond)`, 1308 PASS_TAC); 1309 1310(* ......................................................................... *) 1311 1312val condition_encode = save_thm("condition_encode", 1313 LIST_CONJ (map (fn x => EVAL ``condition_encode ^x``) 1314 ((snd o strip_comb o snd o dest_comb o concl) datatype_condition))); 1315 1316(* ......................................................................... *) 1317 1318fun MAP_SPEC t l = LIST_CONJ (map (fn x => 1319 SIMP_RULE (srw_ss()++pred_setSimps.PRED_SET_ss) 1320 [decode_opcode_def] (SPEC x t)) l); 1321 1322val opc1 = 1323 [`instruction$AND`, `instruction$EOR`, `instruction$SUB`, `instruction$RSB`, 1324 `instruction$ADD`, `instruction$ADC`, `instruction$SBC`, `instruction$RSC`, 1325 `instruction$ORR`, `instruction$BIC`]; 1326 1327val opc2 = 1328 [`instruction$TST`, `instruction$TEQ`, `instruction$CMP`, `instruction$CMN`]; 1329 1330val opc3 = [`instruction$MOV`, `instruction$MVN`]; 1331 1332val cond_pass_enc_data_proc = save_thm("cond_pass_enc_data_proc", 1333 MAP_SPEC cond_pass_enc_data_proc opc1); 1334 1335val cond_pass_enc_data_proc2 = save_thm("cond_pass_enc_data_proc2", 1336 MAP_SPEC cond_pass_enc_data_proc2 opc2); 1337 1338val cond_pass_enc_data_proc3 = save_thm("cond_pass_enc_data_proc3", 1339 MAP_SPEC cond_pass_enc_data_proc3 opc3); 1340 1341val decode_data_proc_enc = save_thm("decode_data_proc_enc", 1342 MAP_SPEC decode_data_proc_enc opc1); 1343 1344val decode_data_proc_enc2 = save_thm("decode_data_proc_enc2", 1345 MAP_SPEC decode_data_proc_enc2 opc2); 1346 1347val decode_data_proc_enc3 = save_thm("decode_data_proc_enc3", 1348 MAP_SPEC decode_data_proc_enc3 opc3); 1349 1350val decode_enc_data_proc = save_thm("decode_enc_data_proc", 1351 MAP_SPEC decode_enc_data_proc opc1); 1352 1353val decode_enc_data_proc2 = save_thm("decode_enc_data_proc2", 1354 MAP_SPEC decode_enc_data_proc2 opc2); 1355 1356val decode_enc_data_proc3 = save_thm("decode_enc_data_proc3", 1357 MAP_SPEC decode_enc_data_proc3 opc3); 1358 1359(* ------------------------------------------------------------------------- *) 1360 1361val _ = export_theory(); 1362