1(* ========================================================================= *) 2(* FILE : arm_rulesScript.sml *) 3(* DESCRIPTION : Derived rules for the ARM Instruction Set Model *) 4(* *) 5(* AUTHORS : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2006 - 2007 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["systemTheory", "wordsLib", "armLib", "arm_evalTheory"]; 11*) 12 13open HolKernel boolLib Parse bossLib; 14open Q arithmeticTheory bitTheory wordsTheory wordsLib; 15open updateTheory armTheory systemTheory arm_evalTheory; 16 17val _ = new_theory "arm_rules"; 18val _ = ParseExtras.temp_loose_equality() 19 20(* ------------------------------------------------------------------------- *) 21 22infix \\ << >> 23 24val op \\ = op THEN; 25val op << = op THENL; 26val op >> = op THEN1; 27 28val std_ss = std_ss ++ boolSimps.LET_ss; 29val arith_ss = arith_ss ++ boolSimps.LET_ss; 30 31val FST_COND_RAND = ISPEC `FST` COND_RAND; 32val SND_COND_RAND = ISPEC `SND` COND_RAND; 33 34fun UNABBREVL_RULE l t = 35 GEN_ALL (foldl (fn (x,t) => armLib.UNABBREV_RULE x t) (SPEC_ALL t) l); 36 37(* ------------------------------------------------------------------------- *) 38 39val MOD_0 = 40 (GSYM o REWRITE_RULE [ZERO_LT_dimword] o SPEC `dimword (:32)`) ZERO_MOD; 41 42val MOD_2EXP_32 = 43 simpLib.SIMP_PROVE (std_ss++wordsLib.SIZES_ss) [MOD_2EXP_def,dimword_def] 44 ``MOD_2EXP 32 n = n MOD dimword (:32)``; 45 46val MSB_lem = (GSYM o GEN_ALL o SIMP_CONV std_ss 47 [BIT_def,BITS_def,MOD_2EXP_def,SUC_SUB,EXP_1,GSYM ODD_MOD2_LEM]) ``BIT x n``; 48 49val ALU_ADD = prove( 50 `!c a b. ADD a b c = 51 let r = a + b + (if c then 1w else 0w) in 52 ((word_msb r, r = 0w, BIT 32 (w2n a + w2n b + (if c then 1 else 0)), 53 (word_msb a = word_msb b) /\ ~(word_msb a = word_msb r)), r)`, 54 REPEAT STRIP_TAC \\ Cases_on `a` \\ Cases_on `b` 55 \\ RW_TAC arith_ss [ADD_def,ALU_arith_def,DIVMOD_2EXP,SBIT_def,WORD_ADD_0] 56 \\ SIMP_TAC std_ss [ADD_ASSOC,GSYM word_add_n2w,w2n_n2w,n2w_mod, 57 MOD_2EXP_32,MOD_PLUS,ZERO_LT_TWOEXP] 58 \\ ONCE_REWRITE_TAC [MOD_0] 59 \\ REWRITE_TAC [GSYM n2w_11,GSYM word_add_n2w,n2w_mod] 60 \\ METIS_TAC [MSB_lem]); 61 62(* ......................................................................... *) 63 64val NOT_MAX_SUC_LT = prove( 65 `!a. ~(a = UINT_MAXw:'a word) ==> w2n a + 1 < dimword(:'a)`, 66 REWRITE_TAC [GSYM w2n_11] 67 \\ RW_TAC std_ss [w2n_lt, DECIDE ``a < b /\ ~(a = b - 1) ==> a + 1 < b``, 68 word_T_def, UINT_MAX_def, ZERO_LT_dimword, w2n_n2w]); 69 70val ALU_SUB_ = prove( 71 `!n n'. n < dimword(:32) ==> 72 (BIT 32 (n + w2n (- (n2w n') + - (1w:word32)) + 1) = 73 BIT 32 (n + w2n (- (n2w n'):word32)) \/ (n2w n' = 0w:word32))`, 74 REPEAT STRIP_TAC 75 \\ REWRITE_TAC [WORD_NEG,GSYM WORD_ADD_ASSOC,WORD_ADD_0, 76 EVAL ``1w + (~1w + 1w):word32``] 77 \\ Cases_on `n2w n' = 0w:word32` 78 << [ 79 FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) 80 [GSYM ADD_ASSOC,BIT_def,BITS_THM,UINT_MAX_def,WORD_NOT_0, 81 ONCE_REWRITE_RULE [ADD_COMM] DIV_MULT_1, word_T_def,w2n_n2w], 82 `~(~n2w n' = UINT_MAXw:word32)` by METIS_TAC [WORD_NOT_0,WORD_NOT_NOT] 83 \\ IMP_RES_TAC NOT_MAX_SUC_LT 84 \\ FULL_SIMP_TAC (std_ss++wordsLib.SIZES_ss) 85 [ADD_ASSOC, REWRITE_RULE [GSYM w2n_11, w2n_n2w] word_add_def, 86 EVAL ``w2n (1w:word32)``]]); 87 88val ALU_SUB = prove( 89 `!c a b. SUB a b c = 90 let r = a - b - (if c then 0w else 1w) in 91 ((word_msb r, r = 0w, 92 if c then 93 a >=+ b 94 else 95 BIT 32 (w2n a + w2n ~b), 96 ~(word_msb a = word_msb b) /\ ~(word_msb a = word_msb r)), r)`, 97 REPEAT STRIP_TAC \\ Cases_on `a` THEN Cases_on `b` 98 \\ RW_TAC arith_ss [SUB_def,ADD_def,ALU_arith_def,DIVMOD_2EXP,WORD_ADD_0, 99 word_hs_def,nzcv_def] 100 \\ RW_TAC std_ss [ADD_ASSOC,GSYM word_add_n2w,w2n_n2w,n2w_w2n,n2w_mod, 101 MOD_2EXP_32,MOD_PLUS,ZERO_LT_TWOEXP,WORD_ADD_0, 102 WORD_NOT,word_sub_def,WORD_NEG_0,MSB_lem,ALU_SUB_, 103 (GEN_ALL o SYM o REWRITE_RULE [GSYM MOD_0] o 104 INST [`n` |-> `0`] o SPEC_ALL o INST_TYPE [`:'a` |-> `:32`]) n2w_11] 105 \\ METIS_TAC [GSYM dimindex_32,WORD_MSB_1COMP, 106 GSYM (REWRITE_RULE [word_sub_def] WORD_NOT), 107 WORD_ADD_ASSOC,WORD_ADD_LINV,WORD_ADD_0]); 108 109(* ......................................................................... *) 110 111val w2n_n2w_bits = REWRITE_RULE [MOD_DIMINDEX] w2n_n2w; 112 113val word_bits_n2w_32 = (GSYM o SIMP_RULE (std_ss++SIZES_ss) [] o 114 INST_TYPE [`:'a` |-> `:32`] o SPECL [`31`,`0`]) word_bits_n2w; 115 116val ALU_MUL = prove( 117 `!a b:word32. (31 >< 0) ((w2w a):word64 * w2w b) = a * b`, 118 SIMP_TAC (arith_ss++SIZES_ss) [w2w_def,word_mul_n2w,word_extract_def, 119 word_bits_n2w,w2n_n2w_bits,BITS_COMP_THM2] 120 \\ SIMP_TAC (arith_ss++fcpLib.FCP_ss++SIZES_ss) 121 [word_mul_def,word_bits_n2w_32,word_bits_def]); 122 123val ALU_MLA = prove( 124 `!a b c:word32. (31 >< 0) (((w2w a):word64) + w2w b * w2w c) = a + b * c`, 125 SIMP_TAC (arith_ss++SIZES_ss) [w2w_def,word_mul_n2w,word_add_n2w, 126 word_extract_def,word_bits_n2w,w2n_n2w_bits,BITS_COMP_THM2] 127 \\ SIMP_TAC (arith_ss++fcpLib.FCP_ss++SIZES_ss) [GSYM word_add_n2w,n2w_w2n, 128 GSYM word_mul_def,word_bits_n2w_32,word_bits_def]); 129 130val concat32 = (SIMP_RULE (std_ss++SIZES_ss) 131 [fcpTheory.index_sum,w2w_id,EXTRACT_ALL_BITS] o SPECL [`63`,`31`,`0`] o 132 INST_TYPE [`:'a` |-> `:64`, `:'b` |-> `:32`, 133 `:'c` |-> `:32`, `:'d` |-> `:64`]) CONCAT_EXTRACT; 134 135val mul32 = prove( 136 `!a b:word32. (31 >< 0) (((w2w a):word64) * w2w b) = a * b`, 137 SIMP_TAC (arith_ss++SIZES_ss) [BITS_COMP_THM2,w2w_def,word_mul_n2w, 138 word_extract_def,word_bits_n2w,w2n_n2w_bits] 139 \\ SIMP_TAC (arith_ss++fcpLib.FCP_ss++SIZES_ss) 140 [word_bits_def,word_bits_n2w_32,GSYM word_mul_def]); 141 142val smul32_lem = prove( 143 `!n. BITS 31 0 (a * b) = BITS 31 0 (BITS 31 0 a * BITS 31 0 b)`, 144 SIMP_TAC pure_ss [BITS_ZERO3,MOD_TIMES2,ZERO_LT_TWOEXP] \\ REWRITE_TAC []); 145 146val smul32_lem2 = prove( 147 `!n. BITS 31 0 (SIGN_EXTEND 32 64 n) = BITS 31 0 n`, 148 RW_TAC (pure_ss++boolSimps.LET_ss) [SIGN_EXTEND_def,numLib.num_CONV ``32``, 149 (EQT_ELIM o EVAL) ``2 ** 64 - 2 ** 32 = (2 ** 32 - 1) * 2 ** 32``, 150 (GSYM o REWRITE_RULE [SYM (numLib.num_CONV ``32``)] o SPEC `31`) BITS_ZERO3, 151 BITS_SUM2] 152 \\ SIMP_TAC std_ss [BITS_COMP_THM2]); 153 154val smul32 = prove( 155 `!a b:word32. (31 >< 0) (((sw2sw a):word64) * sw2sw b) = a * b`, 156 SIMP_TAC (arith_ss++SIZES_ss) [BITS_COMP_THM2,w2w_def,sw2sw_def, 157 word_extract_def,word_bits_n2w,w2n_n2w_bits,word_mul_n2w, 158 Once smul32_lem,smul32_lem2] 159 \\ REWRITE_TAC [GSYM smul32_lem] 160 \\ SIMP_TAC (arith_ss++fcpLib.FCP_ss++SIZES_ss) 161 [word_bits_def,word_bits_n2w_32,GSYM word_mul_def]); 162 163val WORD_UMULL = store_thm("WORD_UMULL", 164 `!a:word32 b:word32. 165 ((63 >< 32) ((w2w a * w2w b):word64)):word32 @@ (a * b) = 166 (w2w a * w2w b):word64`, 167 METIS_TAC [concat32,mul32]); 168 169val WORD_SMULL = store_thm("WORD_SMULL", 170 `!a:word32 b:word32. 171 ((63 >< 32) ((sw2sw a * sw2sw b):word64)):word32 @@ (a * b) = 172 (sw2sw a * sw2sw b):word64`, 173 METIS_TAC [concat32,smul32]); 174 175(* ------------------------------------------------------------------------- *) 176 177val basic_context = 178 [``CONDITION_PASSED2 (NZCV cpsr) c``, 179 ``~state.undefined``, 180 ``Abbrev (Reg = REG_READ state.registers mode)``, 181 ``Abbrev (mode = DECODE_MODE ((4 >< 0) (cpsr:word32)))``, 182 ``Abbrev (cpsr = CPSR_READ state.psrs)``]; 183 184fun cntxt c i = list_mk_conj 185 (mk_eq(``state.memory ((31 >< 2) (state.registers r15))``,i):: 186 (c @ basic_context)); 187 188val word_index = METIS_PROVE [word_index_n2w] 189 ``!i n. i < dimindex (:'a) ==> (((n2w n):'a word) ' i = BIT i n)``; 190 191val CARRY_NZCV = METIS_PROVE [CARRY_def,NZCV_def] ``CARRY (NZCV x) = x ' 29``; 192 193fun DISCH_AND_IMP t = 194 (GEN_ALL o SIMP_RULE (srw_ss()) [REG_WRITE_INC_PC,AND_IMP_INTRO] o 195 DISCH t o SPEC_ALL); 196 197val PC_ss = rewrites [TO_WRITE_READ6,REG_WRITE_WRITE]; 198 199val SPEC_TO_PC = (SIMP_RULE (std_ss++PC_ss) [] o 200 INST [`Rd` |-> `15w:word4`] o SPEC_ALL); 201 202val ARM_ss = rewrites [FST_COND_RAND,SND_COND_RAND,NEXT_ARM_MMU, 203 RUN_ARM_def,OUT_ARM_def,DECODE_PSR_def,TRANSFERS_def,TRANSFER_def, 204 FETCH_PC_def,addr30_def,CARRY_NZCV,n2w_11,word_bits_n2w,w2n_w2w, 205 word_index,BITS_THM,BIT_ZERO,(GEN_ALL o SPECL [`b`,`NUMERAL n`]) BIT_def, 206 OUT_CP_def, RUN_CP_def, 207 cond_pass_enc_data_proc, 208 cond_pass_enc_data_proc2, cond_pass_enc_data_proc3,cond_pass_enc_coproc, 209 cond_pass_enc_mla_mul,cond_pass_enc_br,cond_pass_enc_swi, 210 cond_pass_enc_ldr_str,cond_pass_enc_ldm_stm,cond_pass_enc_swp, 211 cond_pass_enc_mrs,cond_pass_enc_msr]; 212 213fun SYMBOLIC_EVAL_CONV frag context = GEN_ALL (Thm.DISCH context (SIMP_CONV 214 (srw_ss()++boolSimps.LET_ss++SIZES_ss++armLib.PBETA_ss++ARM_ss++frag) 215 [Thm.ASSUME context] ``NEXT_ARM_MMU cp state``)); 216 217(* ......................................................................... *) 218 219val UNDEF_ss = 220 rewrites [EXCEPTION_def,decode_enc_swi,exception2mode_def,exceptions2num_thm]; 221 222val ARM_UNDEF = SYMBOLIC_EVAL_CONV UNDEF_ss ``state.undefined``; 223 224(* ......................................................................... *) 225 226val nop_context = 227 [``Abbrev (cpsr = CPSR_READ state.psrs)``, 228 ``~CONDITION_PASSED2 (NZCV cpsr) c``, 229 ``~state.undefined``]; 230 231fun nop_cntxt i = list_mk_conj 232 (mk_eq(``state.memory ((31 >< 2) (state.registers r15))``,i):: nop_context); 233 234val NOP_ss = rewrites []; 235 236fun eval_nop t = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 237 (subst [``f:condition -> bool -> word4 -> 238 word4 -> addr_mode1 -> arm_instruction`` |-> t] 239 ``enc ((f:condition -> bool -> word4 -> 240 word4 -> addr_mode1 -> arm_instruction) c s Rd Rm Op2)``)); 241 242val ARM_AND_NOP = eval_nop ``instruction$AND`` 243val ARM_EOR_NOP = eval_nop ``instruction$EOR`` 244val ARM_SUB_NOP = eval_nop ``instruction$SUB`` 245val ARM_RSB_NOP = eval_nop ``instruction$RSB`` 246val ARM_ADD_NOP = eval_nop ``instruction$ADD`` 247val ARM_ADC_NOP = eval_nop ``instruction$ADC`` 248val ARM_SBC_NOP = eval_nop ``instruction$SBC`` 249val ARM_RSC_NOP = eval_nop ``instruction$RSC`` 250val ARM_ORR_NOP = eval_nop ``instruction$ORR`` 251val ARM_BIC_NOP = eval_nop ``instruction$BIC`` 252 253val ARM_MOV_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 254 ``enc (instruction$MOV c s Rd Op2)``); 255 256val ARM_MVN_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 257 ``enc (instruction$MVN c s Rd Op2)``); 258 259val ARM_TST_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 260 ``enc (instruction$TST c Rm Op2)``); 261 262val ARM_TEQ_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 263 ``enc (instruction$TEQ c Rm Op2)``); 264 265val ARM_CMP_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 266 ``enc (instruction$CMP c Rm Op2)``); 267 268val ARM_CMN_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 269 ``enc (instruction$CMN c Rm Op2)``); 270 271val ARM_MUL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 272 ``enc (instruction$MUL c s Rd Rs Rm)``); 273 274val ARM_MLA_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 275 ``enc (instruction$MLA c s Rd Rs Rm Rn)``); 276 277val ARM_UMULL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 278 ``enc (instruction$UMULL c s RdLo RdHi Rs Rm)``); 279 280val ARM_UMLAL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 281 ``enc (instruction$UMLAL c s RdLo RdHi Rs Rm)``); 282 283val ARM_SMULL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 284 ``enc (instruction$SMULL c s RdLo RdHi Rs Rm)``); 285 286val ARM_SMLAL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 287 ``enc (instruction$SMLAL c s RdLo RdHi Rs Rm)``); 288 289val ARM_B_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 290 ``enc (instruction$B c offset)``); 291 292val ARM_BL_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 293 ``enc (instruction$BL c offset)``); 294 295val ARM_SWI_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 296 ``enc (instruction$SWI c)``); 297 298val ARM_UND_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 299 ``enc (instruction$UND c)``); 300 301val ARM_LDR_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 302 ``enc (instruction$LDR c b opt Rd Rn Op2)``); 303 304val ARM_STR_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 305 ``enc (instruction$STR c b opt Rd Rn Op2)``); 306 307val ARM_SWP_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 308 ``enc (instruction$SWP c b Rd Rm Rn)``); 309 310val ARM_LDM_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 311 ``enc (instruction$LDM c s opt Rd list)``); 312 313val ARM_STM_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 314 ``enc (instruction$STM c s opt Rd list)``); 315 316val ARM_MRS_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 317 ``enc (instruction$MRS c r Rd)``); 318 319val ARM_MSR_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 320 ``enc (instruction$MSR c psrd op2)``); 321 322val ARM_CDP_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 323 ``enc (instruction$CDP c CPn Cop1 CRd CRn CRm Cop2)``); 324 325val ARM_LDC_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 326 ``enc (instruction$LDC c n options CPn CRd Rn offset)``); 327 328val ARM_STC_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 329 ``enc (instruction$STC c n options CPn CRd Rn offset)``); 330 331val ARM_MRC_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 332 ``enc (instruction$MRC c CPn Cop1 Rd CRn CRm Cop2)``); 333 334val ARM_MCR_NOP = SYMBOLIC_EVAL_CONV NOP_ss (nop_cntxt 335 ``enc (instruction$MCR c CPn Cop1 Rd CRn CRm Cop2)``); 336 337(* ......................................................................... *) 338 339val BRANCH_ss = rewrites [BRANCH_def,REG_READ_def,decode_enc_br,decode_br_enc]; 340 341val ARM_B = UNABBREVL_RULE [`cpsr`,`Reg`,`mode`] 342 (SYMBOLIC_EVAL_CONV BRANCH_ss (cntxt [] ``enc (instruction$B c offset)``)); 343 344val ARM_BL = UNABBREVL_RULE [`Reg`] 345 (SYMBOLIC_EVAL_CONV BRANCH_ss (cntxt [] ``enc (instruction$BL c offset)``)); 346 347val SWI_EX_ss = 348 rewrites [EXCEPTION_def,exception2mode_def,exceptions2num_thm, 349 decode_cp_enc_coproc,decode_enc_swi,decode_enc_coproc,decode_27_enc_coproc]; 350 351val ARM_SWI = UNABBREVL_RULE [`Reg`,`mode`] 352 (SYMBOLIC_EVAL_CONV SWI_EX_ss (cntxt [] ``enc (instruction$SWI c)``)); 353 354val ARM_UND = UNABBREVL_RULE [`Reg`,`mode`] 355 (SYMBOLIC_EVAL_CONV SWI_EX_ss (cntxt [] ``enc (instruction$UND c)``)); 356 357(* ......................................................................... *) 358 359val LSL_NOT_ZERO = prove( 360 `!n. ~(n = 0w:word5) ==> ~(w2w n = 0w:word8)`, 361 Cases \\ RW_TAC bool_ss [dimword_def,ZERO_MOD,ZERO_LT_TWOEXP, 362 w2w_def,n2w_11,w2n_n2w,dimindex_5,dimindex_8] 363 \\ ASSUME_TAC (DECIDE ``5 < 8``) \\ IMP_RES_TAC TWOEXP_MONO 364 \\ METIS_TAC [MOD_2EXP_LT,LESS_TRANS,LESS_MOD]); 365 366val WORD_NEG_cor = 367 METIS_PROVE [WORD_NEG,WORD_ADD_ASSOC,WORD_ADD_COMM,word_sub_def] 368 ``~a + b + 1w = b - a``; 369 370val WORD_1COMP_ZERO = 371 METIS_PROVE [WORD_NOT_NOT,WORD_NOT_T] ``!a. (~a = 0w) = (a = UINT_MAXw)``; 372 373val SND_ROR = prove( 374 `!a n c. SND (ROR a n c) = a #>> w2n n`, 375 RW_TAC std_ss [ROR_def,LSL_def,SHIFT_ZERO,word_0_n2w]); 376 377val DP_rws = 378 [DATA_PROCESSING_def,ARITHMETIC_def,TEST_OR_COMP_def,ALU_def, 379 ALU_ADD,ALU_SUB,LSL_def,LSR_def,AND_def,ORR_def,EOR_def,ALU_logic_def, 380 SET_NZC_def,WORD_ADD_0,WORD_SUB_RZERO,WORD_EQ_SUB_RADD,WORD_HIGHER_EQ, 381 REG_READ_INC_PC,WORD_NEG_cor,WORD_1COMP_ZERO, 382 (SIMP_RULE bool_ss [] o ISPEC `\x:iclass. x = y`) COND_RAND, 383 (SIMP_RULE bool_ss [] o ISPEC `\r. REG_READ r m n`) COND_RAND, 384 (SIMP_RULE (srw_ss()) [] o Q.ISPEC `\x. -1w * x`) COND_RAND, 385 decode_enc_data_proc, decode_data_proc_enc, 386 decode_enc_data_proc2,decode_data_proc_enc2, 387 decode_enc_data_proc3,decode_data_proc_enc3]; 388 389val DP_ss = rewrites DP_rws; 390 391val abbrev_mode1 = 392 ``Abbrev (op2 = ADDR_MODE1 state.registers mode ((cpsr:word32) ' 29) 393 (IS_DP_IMMEDIATE Op2) ((11 >< 0) (addr_mode1_encode Op2)))``; 394 395val ARM_TST = SYMBOLIC_EVAL_CONV DP_ss (cntxt 396 [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$TST c Rm Op2)``); 397 398val ARM_TEQ = SYMBOLIC_EVAL_CONV DP_ss (cntxt 399 [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$TEQ c Rm Op2)``); 400 401val ARM_CMP = SYMBOLIC_EVAL_CONV DP_ss (cntxt 402 [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$CMP c Rm Op2)``); 403 404val ARM_CMN = SYMBOLIC_EVAL_CONV DP_ss (cntxt 405 [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$CMN c Rm Op2)``); 406 407(* ......................................................................... *) 408 409fun eval_op t = 410 SYMBOLIC_EVAL_CONV DP_ss (cntxt [``~(Rm = 15w:word4)``,abbrev_mode1] 411 (subst [``f:condition -> bool -> word4 -> 412 word4 -> addr_mode1 -> arm_instruction`` |-> t] 413 ``enc ((f:condition -> bool -> word4 -> 414 word4 -> addr_mode1 -> arm_instruction) c s Rd Rm Op2)``)); 415 416val ARM_AND = eval_op ``instruction$AND``; 417val ARM_EOR = eval_op ``instruction$EOR``; 418val ARM_SUB = eval_op ``instruction$SUB``; 419val ARM_RSB = eval_op ``instruction$RSB``; 420val ARM_ADD = eval_op ``instruction$ADD``; 421val ARM_ORR = eval_op ``instruction$ORR``; 422val ARM_BIC = eval_op ``instruction$BIC``; 423val ARM_ADC = eval_op ``instruction$ADC``; 424val ARM_SBC = eval_op ``instruction$SBC``; 425val ARM_RSC = eval_op ``instruction$RSC``; 426 427val ARM_MOV = 428 SYMBOLIC_EVAL_CONV DP_ss (cntxt [``~(Rm = 15w:word4)``,abbrev_mode1] 429 ``enc (instruction$MOV c s Rd Op2)``); 430 431val ARM_MVN = 432 SYMBOLIC_EVAL_CONV DP_ss (cntxt [``~(Rm = 15w:word4)``,abbrev_mode1] 433 ``enc (instruction$MVN c s Rd Op2)``); 434 435(* ......................................................................... *) 436 437val DP_ss = 438 rewrites (DP_rws @ [IS_DP_IMMEDIATE_def, ADDR_MODE1_def]); 439 440fun eval_op t = 441 SYMBOLIC_EVAL_CONV DP_ss (cntxt [] 442 (subst [``f:condition -> bool -> word4 -> 443 word4 -> addr_mode1 -> arm_instruction`` |-> t] 444 ``enc ((f:condition -> bool -> word4 -> 445 word4 -> addr_mode1 -> arm_instruction) c F Rd 15w 446 (Dp_immediate rot imm))``)); 447 448val ARM_ADD_TO_PC = eval_op ``instruction$ADD``; 449val ARM_SUB_TO_PC = eval_op ``instruction$SUB``; 450 451(* ......................................................................... *) 452 453val MLA_MUL_ss = rewrites [MLA_MUL_def,ALU_multiply_def,SET_NZC_def, 454 REG_READ_INC_PC,ALU_MUL,ALU_MLA,WORD_ADD_0,REG_READ_WRITE, 455 decode_enc_mla_mul,decode_mla_mul_enc]; 456 457val ARM_MUL = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 458 [``~(Rd = 15w:word4)``,``~(Rd = Rm:word4)``] 459 ``enc (instruction$MUL c s Rd Rm Rs)``); 460 461val ARM_MLA = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 462 [``~(Rd = 15w:word4)``,``~(Rd = Rm:word4)``] 463 ``enc (instruction$MLA c s Rd Rm Rs Rn)``); 464 465val ARM_UMULL = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 466 [``~(RdHi = 15w:word4)``,``~(RdLo = 15w:word4)``,``~(RdHi = RdLo:word4)``, 467 ``~(RdHi = Rm:word4)``,``~(RdLo = Rm:word4)``] 468 ``enc (instruction$UMULL c s RdLo RdHi Rm Rs)``); 469 470val ARM_UMLAL = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 471 [``~(RdHi = 15w:word4)``,``~(RdLo = 15w:word4)``,``~(RdHi = RdLo:word4)``, 472 ``~(RdHi = Rm:word4)``,``~(RdLo = Rm:word4)``] 473 ``enc (instruction$UMLAL c s RdLo RdHi Rm Rs)``); 474 475val ARM_SMULL = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 476 [``~(RdHi = 15w:word4)``,``~(RdLo = 15w:word4)``,``~(RdHi = RdLo:word4)``, 477 ``~(RdHi = Rm:word4)``,``~(RdLo = Rm:word4)``] 478 ``enc (instruction$SMULL c s RdLo RdHi Rm Rs)``); 479 480val ARM_SMLAL = SYMBOLIC_EVAL_CONV MLA_MUL_ss (cntxt 481 [``~(RdHi = 15w:word4)``,``~(RdLo = 15w:word4)``,``~(RdHi = RdLo:word4)``, 482 ``~(RdHi = Rm:word4)``,``~(RdLo = Rm:word4)``] 483 ``enc (instruction$SMLAL c s RdLo RdHi Rm Rs)``); 484 485(* ......................................................................... *) 486 487val BW = prove( 488 `!c f d g0 g1 g2. 489 (case (if c then Byte (f d) else Word d) of 490 Byte b => g0 b 491 | Half hw => g1 hw 492 | Word w => g2 w) = 493 (if c then g0 (f d) else g2 d)`, SRW_TAC [] []); 494 495val LDR_STR_ss = 496 rewrites [LDR_STR_def,MEM_WRITE_def,BW, 497 listTheory.HD,word_bits_n2w,w2w_n2w,BITS_THM, 498 WORD_ADD_0,REG_WRITE_INC_PC,REG_READ_WRITE,REG_READ_INC_PC, 499 decode_enc_ldr_str,decode_ldr_str_enc]; 500 501val abbrev_mode2 = 502 ``Abbrev (addr_mode2 = ADDR_MODE2 state.registers mode ((cpsr:word32) ' 29) 503 (IS_DT_SHIFT_IMMEDIATE offset) opt.Pre opt.Up Rn 504 ((11 >< 0) (addr_mode2_encode offset))) /\ 505 Abbrev (addr = FST addr_mode2) /\ 506 Abbrev (wb_addr = SND addr_mode2)``; 507 508val ARM_LDR = SYMBOLIC_EVAL_CONV LDR_STR_ss 509 (cntxt [abbrev_mode2,``~(Rn = 15w:word4)``] 510 ``enc (instruction$LDR c b opt Rd Rn offset)``); 511 512val ARM_STR = SYMBOLIC_EVAL_CONV LDR_STR_ss 513 (cntxt [abbrev_mode2,``~(Rd = 15w:word4)``,``~(Rn = 15w:word4)``] 514 ``enc (instruction$STR c b opt Rd Rn offset)``); 515 516val ARM_LDR_PC = SIMP_RULE (std_ss++PC_ss) [] 517 (SYMBOLIC_EVAL_CONV LDR_STR_ss 518 (cntxt [abbrev_mode2,``Rn = 15w:word4``] 519 ``enc (instruction$LDR c b opt Rd Rn offset)``)); 520 521val ARM_STR_PC = SIMP_RULE (std_ss++PC_ss) [] 522 (SYMBOLIC_EVAL_CONV LDR_STR_ss 523 (cntxt [abbrev_mode2,``~(Rd = 15w:word4)``,``Rn = 15w:word4``] 524 ``enc (instruction$STR c b opt Rd Rn offset)``)); 525 526(* ......................................................................... *) 527 528val SWP_ss = 529 rewrites [SWP_def,MEM_WRITE_def,BW, 530 listTheory.HD,word_bits_n2w,w2w_n2w,BITS_THM, 531 WORD_ADD_0,REG_WRITE_INC_PC,REG_READ_WRITE,REG_READ_INC_PC, 532 decode_enc_swp,decode_swp_enc]; 533 534val ARM_SWP = SYMBOLIC_EVAL_CONV SWP_ss (cntxt [``~(Rm = 15w:word4)``] 535 ``enc (instruction$SWP c b Rd Rm Rn)``); 536 537(* ......................................................................... *) 538 539val FOLDL_INDUCT = prove( 540 `!f e P l. (!x y. P x ==> P (f x y)) /\ P e ==> P (FOLDL f e l)`, 541 Induct_on `l` \\ ASM_SIMP_TAC (srw_ss()++listSimps.LIST_ss) []); 542 543val TRANSFER_LDM_ = prove( 544 `!x y. (SND (SND x) = mem) ==> 545 (SND (SND (TRANSFER cpi x (MemRead y))) = mem)`, 546 Cases_on `x` \\ Cases_on `r` \\ SRW_TAC [] [TRANSFER_def] 547 \\ ASM_REWRITE_TAC []); 548 549val TRANSFER_LDM = SIMP_RULE std_ss [TRANSFER_LDM_] 550 (ISPECL [`\x y. TRANSFER cpi x (MemRead y)`, 551 `(cpin:word32 option list,data:word32 list,mem:mem)`, 552 `\q:word32 option list # word32 list # mem. SND (SND q) = mem`] 553 FOLDL_INDUCT); 554 555val TRANSFER_LDM2___ = prove( 556 `!data cpin m l. 557 LENGTH (FST (SND 558 (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,data,m) l))) = 559 LENGTH data + LENGTH l`, 560 Induct_on `l` 561 \\ ASM_SIMP_TAC (srw_ss()++listSimps.LIST_ss++ARITH_ss) [TRANSFER_def]); 562 563val TRANSFER_LDM2__ = prove( 564 `!rd cpin m l. 565 LENGTH (FST (SND 566 (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,[],m) 567 (ADDRESS_LIST rd (LENGTH l))))) = LENGTH l`, 568 SIMP_TAC list_ss [TRANSFER_LDM2___,ADDRESS_LIST_def, 569 rich_listTheory.LENGTH_GENLIST]); 570 571val TRANSFER_LDM2_ = prove( 572 `!m d l. FST (SND (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,d,m) l)) = 573 d ++ MAP (\x. m (addr30 x)) l`, 574 Induct_on `l` \\ ASM_SIMP_TAC (srw_ss()++listSimps.LIST_ss) [TRANSFER_def, 575 GSYM rich_listTheory.SNOC_APPEND,my_listTheory.APPEND_SNOC1]); 576 577val TRANSFER_LDM2 = prove( 578 `!cpin m P U rd l. 579 let addr_mode4 = ADDR_MODE4 P U rd l in 580 FIRSTN (LENGTH (FST addr_mode4)) 581 (FST (SND (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,[],m) 582 (FST (SND addr_mode4))))) = 583 MAP (m o addr30) (FST (SND addr_mode4))`, 584 REPEAT STRIP_TAC 585 \\ `!rd. FIRSTN (LENGTH (REGISTER_LIST l)) 586 (FST (SND (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,[],m) 587 (ADDRESS_LIST (FIRST_ADDRESS P U rd 588 (WB_ADDRESS U rd (LENGTH (REGISTER_LIST l)))) 589 (LENGTH (REGISTER_LIST l)))))) = 590 (FST (SND (FOLDL (\x y. TRANSFER F x (MemRead y)) (cpin,[],m) 591 (ADDRESS_LIST (FIRST_ADDRESS P U rd 592 (WB_ADDRESS U rd (LENGTH (REGISTER_LIST l)))) 593 (LENGTH (REGISTER_LIST l))))))` 594 by METIS_TAC [TRANSFER_LDM2__,rich_listTheory.FIRSTN_LENGTH_ID] 595 \\ SRW_TAC [boolSimps.LET_ss] [ADDR_MODE4_def] 596 \\ SRW_TAC [] 597 [ADDRESS_LIST_def,TRANSFER_LDM2_,my_listTheory.MAP_GENLIST] 598 \\ MATCH_MP_TAC my_listTheory.GENLIST_FUN_EQ 599 \\ SIMP_TAC std_ss []); 600 601val TRANSFER_LDM2 = SIMP_RULE (bool_ss++boolSimps.LET_ss) [] TRANSFER_LDM2; 602 603val TRANSFER_STM = prove( 604 `!cpin data m r mode l. 605 SND (SND (FOLDL (TRANSFER F) (cpin,data,m) (STM_LIST r mode l))) = 606 FOLDL (\mem (rp,rd). MEM_WRITE mem rd (Word (REG_READ r mode rp))) m l`, 607 Induct_on `l` \\ TRY (Cases_on `h`) 608 \\ ASM_SIMP_TAC (srw_ss()++listSimps.LIST_ss) [TRANSFER_def,STM_LIST_def] 609 \\ ASM_SIMP_TAC std_ss [GSYM STM_LIST_def]); 610 611val LDM_STM_ss = 612 rewrites [LDM_STM_def,MEM_WRITE_def, 613 rich_listTheory.FIRSTN_LENGTH_ID,my_listTheory.FOLDL_MAP2, 614 listTheory.HD,word_bits_n2w,w2w_n2w,BITS_THM, 615 WORD_ADD_0,REG_WRITE_INC_PC,REG_READ_WRITE,REG_READ_INC_PC, 616 TRANSFER_LDM, TRANSFER_LDM2, TRANSFER_STM, LDM_LIST_def, 617 decode_enc_ldm_stm,decode_ldm_stm_enc]; 618 619val abbrev_mode4 = 620 ``Abbrev (addr_mode4 = ADDR_MODE4 opt.Pre opt.Up (Reg (Rd:word4)) list) /\ 621 Abbrev (rp_list = FST addr_mode4) /\ 622 Abbrev (addr_list = FST (SND addr_mode4)) /\ 623 Abbrev (wb = SND (SND addr_mode4))``; 624 625val ARM_LDM = (GEN_ALL o Thm.DISCH abbrev_mode4 o 626 SIMP_RULE std_ss [Thm.ASSUME abbrev_mode4] o SPEC_ALL) 627 (SYMBOLIC_EVAL_CONV LDM_STM_ss (cntxt [``Abbrev (l = REGISTER_LIST list)``] 628 ``enc (instruction$LDM c s opt Rd list)``)); 629 630val ARM_STM = (GEN_ALL o Thm.DISCH abbrev_mode4 o 631 SIMP_RULE std_ss [Thm.ASSUME abbrev_mode4] o SPEC_ALL) 632 (SYMBOLIC_EVAL_CONV LDM_STM_ss (cntxt [``Abbrev (l = REGISTER_LIST list)``] 633 ``enc (instruction$STM c s opt Rd list)``)); 634 635(* ......................................................................... *) 636 637val lem = prove(`!b r x y. 638 (if b then <| reg := r; psr := x |> else <| reg := r; psr := y |>) = 639 <| reg := r; psr := if b then x else y |>`, SRW_TAC [] []); 640 641val MRS_MSR_ss = rewrites [MSR_def,MRS_def,lem, 642 immediate_enc,decode_enc_msr,decode_msr_enc,decode_enc_mrs,decode_mrs_enc]; 643 644val ARM_MSR = 645 SYMBOLIC_EVAL_CONV MRS_MSR_ss 646 (cntxt [``Abbrev ((R,flags,ctrl) = DECODE_PSRD psrd) /\ 647 Abbrev (src = if IS_MSR_IMMEDIATE op2 then 648 SND (IMMEDIATE F ((11 >< 0) (msr_mode_encode op2))) 649 else 650 Reg (((3 >< 0) (((11 >< 0) 651 (msr_mode_encode op2)) : word12)) : word4)) /\ 652 Abbrev (f:word32->word32 = word_modify (\i b. 653 28 <= i /\ (if flags then src ' i else b) \/ 654 8 <= i /\ i <= 27 /\ b \/ 655 i <= 7 /\ 656 (if ctrl /\ ~USER mode then src ' i else b)))``] 657 ``enc (instruction$MSR c psrd op2)``); 658 659val ARM_MRS = 660 (SYMBOLIC_EVAL_CONV MRS_MSR_ss (cntxt [] ``enc (instruction$MRS c r Rd)``)); 661 662(* ------------------------------------------------------------------------- *) 663 664val EVERY_N_LDC = prove( 665 `!n. EVERY (\x. ~IS_SOME x) (GENLIST (K NONE) n)`, 666 STRIP_TAC \\ MATCH_MP_TAC my_listTheory.EVERY_GENLIST \\ SRW_TAC [] []); 667 668val SYM_WORD_RULE = ONCE_REWRITE_RULE 669 [Thm.INST_TYPE [alpha |-> ``:word4``] EQ_SYM_EQ]; 670 671val ADDRESS_LIST_0 = SIMP_CONV (srw_ss()) 672 [ADDRESS_LIST_def,rich_listTheory.GENLIST] ``ADDRESS_LIST x 0``; 673 674val ZIP_COND = SIMP_CONV (bool_ss++boolSimps.LIFT_COND_ss) [] 675 ``ZIP (if a then b else c, if a then d else e)``; 676 677val COPROC_ss = rewrites [SYM_WORD_RULE MRC_def,LDC_STC_def,MCR_OUT_def, 678 PROVE [] ``!b x y. (if ~b then x else y) = (if b then y else x)``, 679 ISPEC `cp_output_absent` COND_RAND, ISPEC `cp_output_data` COND_RAND, 680 ISPEC `regs_reg` COND_RAND, ISPEC `regs_psr` COND_RAND, 681 ISPEC `SPLITP IS_NONE` COND_RAND, ISPEC `SPLITP IS_NONE` COND_RAND, 682 ISPEC `LENGTH` COND_RAND, ISPEC `ADDRESS_LIST x` COND_RAND, 683 ISPEC `FOLDL f e` COND_RAND, 684 FST_COND_RAND, ZIP_COND, EVAL ``ELL 1 [a; b]``, ADDRESS_LIST_0, 685 rich_listTheory.LENGTH_GENLIST, CONJUNCT1 rich_listTheory.SPLITP, 686 MATCH_MP (SPEC_ALL my_listTheory.SPLITP_EVERY) (SPEC_ALL EVERY_N_LDC), 687 decode_enc_coproc,decode_cp_enc_coproc,decode_ldc_stc_enc, 688 decode_ldc_stc_20_enc,decode_27_enc_coproc,decode_mrc_mcr_rd_enc]; 689 690val ARM_CDP = UNABBREVL_RULE [`Reg`] 691 (SYMBOLIC_EVAL_CONV COPROC_ss (cntxt [] 692 ``enc (instruction$CDP c CPn Cop1 CRd CRn CRm Cop2)``)); 693 694val ARM_LDC = UNABBREVL_RULE [`Reg`] 695 (SYMBOLIC_EVAL_CONV COPROC_ss (cntxt [] 696 ``enc (instruction$LDC c n options CPn CRd Rn offset)``)); 697 698val ARM_STC = UNABBREVL_RULE [`Reg`] 699 (SYMBOLIC_EVAL_CONV COPROC_ss (cntxt [] 700 ``enc (instruction$STC c n options CPn CRd Rn offset)``)); 701 702val ARM_MRC = (UNABBREVL_RULE [`Reg`] o SYM_WORD_RULE) 703 (SYMBOLIC_EVAL_CONV COPROC_ss (cntxt [] 704 ``enc (instruction$MRC c CPn Cop1 Rd CRn CRm Cop2)``)); 705 706val ARM_MCR = UNABBREVL_RULE [`Reg`] 707 (SYMBOLIC_EVAL_CONV COPROC_ss (cntxt [] 708 ``enc (instruction$MCR c CPn Cop1 Rd CRn CRm Cop2)``)); 709 710(* ------------------------------------------------------------------------- *) 711 712val _ = save_thm("ARM_UNDEF", ARM_UNDEF); 713 714val _ = save_thm("ARM_B_NOP", ARM_B_NOP); 715val _ = save_thm("ARM_BL_NOP", ARM_BL_NOP); 716val _ = save_thm("ARM_SWI_NOP", ARM_SWI_NOP); 717val _ = save_thm("ARM_AND_NOP", ARM_AND_NOP); 718val _ = save_thm("ARM_EOR_NOP", ARM_EOR_NOP); 719val _ = save_thm("ARM_SUB_NOP", ARM_SUB_NOP); 720val _ = save_thm("ARM_RSB_NOP", ARM_RSB_NOP); 721val _ = save_thm("ARM_ADD_NOP", ARM_ADD_NOP); 722val _ = save_thm("ARM_ADC_NOP", ARM_ADC_NOP); 723val _ = save_thm("ARM_SBC_NOP", ARM_SBC_NOP); 724val _ = save_thm("ARM_RSC_NOP", ARM_RSC_NOP); 725val _ = save_thm("ARM_TST_NOP", ARM_TST_NOP); 726val _ = save_thm("ARM_TEQ_NOP", ARM_TEQ_NOP); 727val _ = save_thm("ARM_CMP_NOP", ARM_CMP_NOP); 728val _ = save_thm("ARM_CMN_NOP", ARM_CMN_NOP); 729val _ = save_thm("ARM_ORR_NOP", ARM_ORR_NOP); 730val _ = save_thm("ARM_MOV_NOP", ARM_MOV_NOP); 731val _ = save_thm("ARM_BIC_NOP", ARM_BIC_NOP); 732val _ = save_thm("ARM_MVN_NOP", ARM_MVN_NOP); 733val _ = save_thm("ARM_MUL_NOP", ARM_MUL_NOP); 734val _ = save_thm("ARM_MLA_NOP", ARM_MLA_NOP); 735val _ = save_thm("ARM_UMULL_NOP", ARM_UMULL_NOP); 736val _ = save_thm("ARM_UMLAL_NOP", ARM_UMLAL_NOP); 737val _ = save_thm("ARM_SMULL_NOP", ARM_SMULL_NOP); 738val _ = save_thm("ARM_SMLAL_NOP", ARM_SMLAL_NOP); 739val _ = save_thm("ARM_LDR_NOP", ARM_LDR_NOP); 740val _ = save_thm("ARM_STR_NOP", ARM_STR_NOP); 741val _ = save_thm("ARM_LDM_NOP", ARM_LDM_NOP); 742val _ = save_thm("ARM_STM_NOP", ARM_STM_NOP); 743val _ = save_thm("ARM_SWP_NOP", ARM_SWP_NOP); 744val _ = save_thm("ARM_MRS_NOP", ARM_MRS_NOP); 745val _ = save_thm("ARM_MSR_NOP", ARM_MSR_NOP); 746val _ = save_thm("ARM_UND_NOP", ARM_UND_NOP); 747val _ = save_thm("ARM_CDP_NOP", ARM_CDP_NOP); 748val _ = save_thm("ARM_LDC_NOP", ARM_LDC_NOP); 749val _ = save_thm("ARM_STC_NOP", ARM_STC_NOP); 750val _ = save_thm("ARM_MRC_NOP", ARM_MRC_NOP); 751val _ = save_thm("ARM_MCR_NOP", ARM_MCR_NOP); 752 753val _ = save_thm("ARM_B", ARM_B); 754val _ = save_thm("ARM_BL", ARM_BL); 755val _ = save_thm("ARM_SWI", ARM_SWI); 756val _ = save_thm("ARM_UND", ARM_UND); 757 758val _ = save_thm("ARM_TST", ARM_TST); 759val _ = save_thm("ARM_TEQ", ARM_TEQ); 760val _ = save_thm("ARM_CMP", ARM_CMP); 761val _ = save_thm("ARM_CMN", ARM_CMN); 762 763val _ = save_thm("ARM_AND", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_AND); 764val _ = save_thm("ARM_EOR", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_EOR); 765val _ = save_thm("ARM_SUB", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_SUB); 766val _ = save_thm("ARM_RSB", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_RSB); 767val _ = save_thm("ARM_ADD", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_ADD); 768val _ = save_thm("ARM_ORR", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_ORR); 769val _ = save_thm("ARM_MOV", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_MOV); 770val _ = save_thm("ARM_BIC", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_BIC); 771val _ = save_thm("ARM_MVN", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_MVN); 772val _ = save_thm("ARM_ADC", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_ADC); 773val _ = save_thm("ARM_SBC", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_SBC); 774val _ = save_thm("ARM_RSC", DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_RSC); 775 776val _ = save_thm("ARM_AND_PC", SPEC_TO_PC ARM_AND); 777val _ = save_thm("ARM_EOR_PC", SPEC_TO_PC ARM_EOR); 778val _ = save_thm("ARM_SUB_PC", SPEC_TO_PC ARM_SUB); 779val _ = save_thm("ARM_RSB_PC", SPEC_TO_PC ARM_RSB); 780val _ = save_thm("ARM_ADD_PC", SPEC_TO_PC ARM_ADD); 781val _ = save_thm("ARM_ORR_PC", SPEC_TO_PC ARM_ORR); 782val _ = save_thm("ARM_MOV_PC", SPEC_TO_PC ARM_MOV); 783val _ = save_thm("ARM_BIC_PC", SPEC_TO_PC ARM_BIC); 784val _ = save_thm("ARM_MVN_PC", SPEC_TO_PC ARM_MVN); 785val _ = save_thm("ARM_ADC_PC", SPEC_TO_PC ARM_ADC); 786val _ = save_thm("ARM_SBC_PC", SPEC_TO_PC ARM_SBC); 787val _ = save_thm("ARM_RSC_PC", SPEC_TO_PC ARM_RSC); 788 789val _ = save_thm("ARM_SUB_TO_PC", 790 DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_SUB_TO_PC); 791 792val _ = save_thm("ARM_ADD_TO_PC", 793 DISCH_AND_IMP `~(Rd = 15w:word4)` ARM_ADD_TO_PC); 794 795val _ = save_thm("ARM_SUB_TO_PC_PC", SPEC_TO_PC ARM_SUB_TO_PC); 796val _ = save_thm("ARM_ADD_TO_PC_PC", SPEC_TO_PC ARM_ADD_TO_PC); 797 798val _ = save_thm("ARM_MUL", ARM_MUL); 799val _ = save_thm("ARM_MLA", ARM_MLA); 800val _ = save_thm("ARM_UMULL", ARM_UMULL); 801val _ = save_thm("ARM_UMLAL", ARM_UMLAL); 802val _ = save_thm("ARM_SMULL", ARM_SMULL); 803val _ = save_thm("ARM_SMLAL", ARM_SMLAL); 804 805val _ = save_thm("ARM_LDR", ARM_LDR); 806val _ = save_thm("ARM_STR", ARM_STR); 807val _ = save_thm("ARM_LDM", ARM_LDM); 808val _ = save_thm("ARM_STM", ARM_STM); 809val _ = save_thm("ARM_SWP", ARM_SWP); 810val _ = save_thm("ARM_LDR_PC", ARM_LDR_PC); 811val _ = save_thm("ARM_STR_PC", ARM_STR_PC); 812 813val _ = save_thm("ARM_MRS",ARM_MRS); 814val _ = save_thm("ARM_MSR",ARM_MSR); 815 816val _ = save_thm("ARM_CDP", ARM_CDP); 817val _ = save_thm("ARM_LDC", ARM_LDC); 818val _ = save_thm("ARM_STC", ARM_STC); 819val _ = save_thm("ARM_MRC", ARM_MRC); 820val _ = save_thm("ARM_MCR", ARM_MCR); 821 822(* ------------------------------------------------------------------------- *) 823 824val _ = export_theory(); 825