1(* ========================================================================= *) 2(* FILE : lemmasScript.sml *) 3(* DESCRIPTION : A collection of lemmas used to verify correctness *) 4(* *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2001 - 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["wordsLib", "armTheory", "coreTheory", "armLib"]; 11*) 12 13open HolKernel boolLib bossLib; 14open Q numLib combinTheory arithmeticTheory; 15open bitTheory wordsLib wordsTheory armTheory coreTheory; 16 17val _ = new_theory "lemmas"; 18 19(* ------------------------------------------------------------------------- *) 20 21infix << >> 22 23val op << = op THENL; 24val op >> = op THEN1; 25 26val std_ss = std_ss ++ boolSimps.LET_ss; 27val arith_ss = arith_ss ++ boolSimps.LET_ss; 28 29val fcp_ss = armLib.fcp_ss; 30val SIZES_ss = wordsLib.SIZES_ss; 31 32val tt = set_trace "types"; 33 34(* ------------------------------------------------------------------------- *) 35 36val arm6inp_nchotomy = save_thm("arm6inp_nchotomy", 37 armLib.tupleCases 38 ``(NRESET:bool, ABORT:bool, NFQ:bool, NIQ:bool, 39 DATA:word32, CPA:bool, CPB:bool)``); 40 41val arm6_nchotomy = save_thm("arm6_nchotomy", 42 armLib.combCases ``ARM6 (DP reg psr areg din alua alub dout) 43 (CTRL pipea pipeaval pipeb pipebval ireg iregval ointstart onewinst 44 endinst obaselatch opipebll nxtic nxtis nopc1 oorst resetlatch onfq 45 ooonfq oniq oooniq pipeaabt pipebabt iregabt2 dataabt2 aregn2 mrq2 46 nbw nrw sctrlreg psrfb oareg mask orp oorp mul mul2 borrow2 mshift)``); 47 48fun Cases_on_arm6inp tm = FULL_STRUCT_CASES_TAC (SPEC tm arm6inp_nchotomy); 49 50val form_7tuple = save_thm("form_7tuple", 51 (GEN_ALL o simpLib.SIMP_PROVE std_ss []) 52 ``(a:bool # bool # bool # bool # word32 # bool # bool) = 53 (FST a,FST (SND a),FST (SND (SND a)),FST (SND (SND (SND a))), 54 FST (SND (SND (SND (SND a)))),FST (SND (SND (SND (SND (SND a))))), 55 SND (SND (SND (SND (SND (SND a))))))``); 56 57val SNEXT_NEXT_ARM6 = save_thm("SNEXT_NEXT_ARM6", 58 (ONCE_REWRITE_RULE [form_7tuple] o SIMP_RULE (srw_ss()) [] o 59 SPEC `<|state := a; inp := i|>` o 60 REWRITE_RULE [FUN_EQ_THM] o ISPEC `NEXT_ARM6`) io_onestepTheory.SNEXT_def); 61 62val COND_PAIR = save_thm("COND_PAIR", 63 (GEN_ALL o PROVE []) ``(if e then (a,b) else (c,d)) = 64 (if e then a else c,if e then b else d)``); 65 66(* ------------------------------------------------------------------------- *) 67 68val NOT_RESET_EXISTS = store_thm("NOT_RESET_EXISTS", 69 `!t inp. ~IS_RESET inp t ==> 70 ?ABORT NFQ NIQ DATA CPA CPB. 71 (inp t = (T,IS_ABORT inp t,NFQ,NIQ,DATA,CPA,CPB))`, 72 RW_TAC std_ss [IS_RESET_def,IS_ABORT_def] 73 THEN Cases_on_arm6inp `inp (t:num)` 74 THEN FULL_SIMP_TAC std_ss [PROJ_NRESET_def,PROJ_ABORT_def]); 75 76val NOT_RESET_EXISTS2 = store_thm("NOT_RESET_EXISTS2", 77 `!t inp. ~IS_RESET inp t ==> 78 ?ABORT NFQ NIQ DATA CPA CPB. (inp t = (T,ABORT,NFQ,NIQ,DATA,CPA,CPB))`, 79 RW_TAC std_ss [IS_RESET_def] \\ Cases_on_arm6inp `inp (t:num)` 80 \\ FULL_SIMP_TAC std_ss [PROJ_NRESET_def]); 81 82val MASK_MASK = store_thm("MASK_MASK", 83 `!ic mask rp rp2. 84 MASK ic t3 (MASK ic t3 mask rp) rp2 = MASK ic t3 mask rp`, 85 RW_TAC std_ss [MASK_def]); 86 87val SND_LSL = store_thm("SND_LSL", 88 `!n a c. SND (LSL a n c) = a << w2n n`, 89 RW_TAC arith_ss [LSL_def,SHIFT_ZERO,word_0_n2w]); 90 91val LSL_ZERO = save_thm("LSL_ZERO", 92 (REWRITE_RULE [SHIFT_ZERO,word_0_n2w] o SPEC `0w`) SND_LSL); 93 94val LSL_TWO = save_thm("LSL_TWO", 95 (SIMP_RULE (arith_ss++SIZES_ss) [w2n_n2w] o SPEC `2w`) SND_LSL); 96 97val SND_ROR = store_thm("SND_ROR", 98 `!a n c. SND (ROR a n c) = a #>> w2n n`, 99 RW_TAC std_ss [ROR_def,LSL_def,SHIFT_ZERO,word_0_n2w]); 100 101val IMMEDIATE_THM = store_thm("IMMEDIATE_THM", 102 `!c i:word32. 103 IMMEDIATE c ((11 >< 0) i) = ROR ((7 -- 0) i) (2w * (11 >< 8) i) c`, 104 SIMP_TAC (arith_ss++SIZES_ss) 105 [IMMEDIATE_def,MIN_DEF,word_extract_def,word_bits_w2w,w2w_id,w2w_w2w, 106 WORD_BITS_COMP_THM]); 107 108val IMMEDIATE_THM2 = store_thm("IMMEDIATE_THM2", 109 `!c i. SND (IMMEDIATE c i) = SND (IMMEDIATE F i)`, 110 RW_TAC std_ss [IMMEDIATE_def,ROR_def,LSL_def]); 111 112val SHIFT_IMMEDIATE_THM2 = store_thm("SHIFT_IMMEDIATE_THM2", 113 `!r m c i. SHIFT_IMMEDIATE r m c ((11 >< 0) i) = 114 let rm = REG_READ r m ((3 >< 0) i) in 115 SHIFT_IMMEDIATE2 ((11 >< 7) i) ((6 >< 5) i) rm c`, 116 SIMP_TAC (arith_ss++SIZES_ss) [SHIFT_IMMEDIATE_def,MIN_DEF,WORD_BITS_COMP_THM, 117 word_extract_def,word_bits_w2w,w2w_w2w]); 118 119val SHIFT_REGISTER_THM2 = store_thm("SHIFT_REGISTER_THM2", 120 `!r m c i. SHIFT_REGISTER r m c ((11 >< 0) i) = 121 let shift = (7 >< 0) (REG_READ r m ((11 >< 8) i)) 122 and rm = REG_READ (INC_PC r) m ((3 >< 0) i) in 123 SHIFT_REGISTER2 shift ((6 >< 5) i) rm c`, 124 SIMP_TAC (arith_ss++SIZES_ss) [SHIFT_REGISTER_def,MIN_DEF,WORD_BITS_COMP_THM, 125 word_extract_def,word_bits_w2w,w2w_w2w]); 126 127val w2w_extract = store_thm("w2w_extract", 128 `!w:bool ** 'a. w2w (((h >< l) w):bool ** 'b) = 129 (MIN h (dimindex (:'b) - 1 + l) -- l) w`, 130 SIMP_TAC arith_ss [word_extract_def,w2w_w2w,w2w_id, 131 WORD_BITS_COMP_THM]); 132 133val CONCAT_MSR = store_thm("CONCAT_MSR", 134 `!b i. 8 <= i /\ i <= 27 /\ b \/ i <= 7 /\ b = i < 28 /\ b`, 135 Cases \\ SIMP_TAC arith_ss []); 136 137(* ------------------------------------------------------------------------- *) 138 139val LESS_THM = 140 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 141 142val TEST_OR_COMP_LEM = prove( 143 `!n. (BITS 24 23 n = 2) = BIT 24 n /\ ~BIT 23 n`, 144 STRIP_TAC \\ SPECL_THEN [`24`,`23`,`n`] 145 (ASSUME_TAC o SIMP_RULE arith_ss []) BITSLT_THM 146 \\ FULL_SIMP_TAC arith_ss [LESS_THM, 147 simpLib.SIMP_PROVE arith_ss [BIT_def,BITS_COMP_THM2] 148 ``(!n. BIT 24 n = BIT 1 (BITS 24 23 n)) /\ 149 (!n. BIT 23 n = BIT 0 (BITS 24 23 n))``] \\ EVAL_TAC); 150 151val start_tac = 152 SIMP_TAC (arith_ss++SIZES_ss) [TEST_OR_COMP_def,ARITHMETIC_def, 153 WORD_BITS_COMP_THM,word_extract_def,word_bits_w2w] 154 \\ Cases \\ SIMP_TAC (std_ss++SIZES_ss) [word_bits_n2w,w2w_def] 155 \\ ASM_SIMP_TAC bool_ss [w2n_n2w,n2w_11,MOD_DIMINDEX]; 156 157val TEST_OR_COMP_THM = store_thm("TEST_OR_COMP_THM", 158 `!i:word32. TEST_OR_COMP ((24 >< 21) i) = i %% 24 /\ ~(i %% 23)`, 159 start_tac \\ SIMP_TAC (fcp_ss++SIZES_ss) [n2w_def,EVAL ``BITS 3 0 2``, 160 BITS_COMP_THM2,TEST_OR_COMP_LEM]); 161 162val ARITHMETIC_THM = store_thm("ARITHMETIC_THM", 163 `!i:word32. ARITHMETIC ((24 >< 21) i) = 164 (i %% 23 \/ i %% 22) /\ (~(i %% 24) \/ ~(i %% 23))`, 165 start_tac \\ SIMP_TAC (fcp_ss++SIZES_ss) [n2w_def,BIT_def,BITS_COMP_THM2]); 166 167val ARITHMETIC_THM2 = store_thm("ARITHMETIC_THM2", 168 `!i:word32. ~(i %% 23) /\ ~(i %% 22) \/ i %% 24 /\ i %% 23 = 169 ~ARITHMETIC ((24 >< 21) i)`, RW_TAC bool_ss [ARITHMETIC_THM]); 170 171(* ------------------------------------------------------------------------- *) 172 173val ADD4_ADD4 = store_thm("ADD4_ADD4", 174 `(!a. a + 4w + 4w = a + 8w)`, 175 SIMP_TAC arith_ss [GSYM WORD_ADD_ASSOC,word_add_n2w]); 176 177val ONE_COMP_THREE_ADD = store_thm("ONE_COMP_THREE_ADD", 178 `!a:word32. a - 8w + 4w = ~3w + a`, 179 STRIP_TAC \\ `~3w + a = a + ~3w` by PROVE_TAC [WORD_ADD_COMM] 180 \\ POP_ASSUM SUBST1_TAC \\ RW_TAC bool_ss [WORD_NOT] 181 \\ EVAL_TAC \\ REWRITE_TAC [GSYM WORD_ADD_ASSOC,WORD_EQ_ADD_LCANCEL] 182 \\ EVAL_TAC); 183 184val REGISTER_RANGES = 185 (SIMP_RULE (std_ss++SIZES_ss) [] o Thm.INST_TYPE [alpha |-> ``:4``]) w2n_lt; 186 187val mode_reg2num_15 = (GEN_ALL o 188 SIMP_RULE (arith_ss++SIZES_ss) [w2n_n2w] o 189 SPECL [`m`,`15w`]) mode_reg2num_def; 190 191val mode_reg2num_lt = store_thm("mode_reg2num_lt", 192 `!w m w. mode_reg2num m w < 31`, 193 ASSUME_TAC REGISTER_RANGES 194 \\ RW_TAC std_ss [mode_reg2num_def,USER_def,DECIDE ``n < 16 ==> n < 31``] 195 \\ Cases_on `m` 196 \\ FULL_SIMP_TAC arith_ss [mode_distinct,mode_case_def, 197 DECIDE ``a < 16 /\ b < 16 ==> (a + b < 31)``, 198 DECIDE ``a < 16 /\ ~(a = 15) ==> (a + 16 < 31)``]); 199 200val not_reg_eq_lem = prove(`!v w. ~(v = w) ==> ~(w2n v = w2n w)`, 201 REPEAT Cases \\ SIMP_TAC std_ss [w2n_n2w,n2w_11]); 202 203val not_reg_eq = store_thm("not_reg_eq", 204 `!v w m1 m2. ~(v = w) ==> ~(mode_reg2num m1 v = mode_reg2num m2 w)`, 205 NTAC 4 STRIP_TAC 206 \\ `w2n v < 16 /\ w2n w < 16` by REWRITE_TAC [REGISTER_RANGES] 207 \\ Cases_on `m1` \\ Cases_on `m2` 208 \\ ASM_SIMP_TAC (srw_ss()++boolSimps.LET_ss) 209 [USER_def,mode_reg2num_def,not_reg_eq_lem] 210 \\ COND_CASES_TAC \\ ASM_SIMP_TAC arith_ss [not_reg_eq_lem] 211 \\ COND_CASES_TAC \\ ASM_SIMP_TAC arith_ss [not_reg_eq_lem]); 212 213val not_pc = (GEN_ALL o REWRITE_RULE [mode_reg2num_15] o 214 SPECL [`v`,`15w`]) not_reg_eq; 215 216val r15 = SYM (List.nth (CONJUNCTS num2register_thm, 15)) 217val READ_TO_READ6 = store_thm("READ_TO_READ6", 218 `!r m n d. (REG_READ (REG_WRITE r usr 15w (d - 8w)) m n = 219 REG_READ6 (REG_WRITE r usr 15w d) m n)`, 220 RW_TAC (std_ss++SIZES_ss) [REG_READ_def,REG_READ6_def,FETCH_PC_def, 221 REG_WRITE_def,UPDATE_def,WORD_SUB_ADD,mode_reg2num_15] 222 \\ PROVE_TAC [r15,num2register_11,mode_reg2num_lt,not_pc,DECIDE ``15 < 31``]); 223 224val TO_WRITE_READ6 = store_thm("TO_WRITE_READ6", 225 `(!r. FETCH_PC r = REG_READ6 r usr 15w) /\ 226 (!r. INC_PC r = REG_WRITE r usr 15w (REG_READ6 r usr 15w + 4w)) /\ 227 (!r. SUB8_PC r = REG_WRITE r usr 15w (REG_READ6 r usr 15w - 8w)) /\ 228 (!r m d. REG_WRITE r m 15w d = REG_WRITE r usr 15w d) /\ 229 (!r m. REG_READ6 r m 15w = REG_READ6 r usr 15w)`, 230 RW_TAC std_ss [INC_PC_def,REG_READ6_def,REG_WRITE_def,REG_READ_def, 231 FETCH_PC_def,SUB8_PC_def,mode_reg2num_15]); 232 233val REG_WRITE_WRITE = store_thm("REG_WRITE_WRITE", 234 `!r m n d1 d2. REG_WRITE (REG_WRITE r m n d1) m n d2 = REG_WRITE r m n d2`, 235 RW_TAC bool_ss [REG_WRITE_def,UPDATE_EQ]); 236 237val REG_WRITE_WRITE_COMM = store_thm("REG_WRITE_WRITE_COMM", 238 `!r m n1 n2 d1 d2. 239 ~(n1 = n2) ==> 240 (REG_WRITE (REG_WRITE r m n1 d1) m n2 d2 = 241 REG_WRITE (REG_WRITE r m n2 d2) m n1 d1)`, 242 RW_TAC std_ss [REG_WRITE_def,UPDATE_COMMUTES,not_reg_eq, 243 mode_reg2num_lt,num2register_11]); 244 245val REG_WRITE_WRITE_PC = store_thm("REG_WRITE_WRITE_PC", 246 `!r m1 m2 n d p. 247 REG_WRITE (REG_WRITE r m1 15w p) m2 n d = 248 if n = 15w then 249 REG_WRITE r usr 15w d 250 else 251 REG_WRITE (REG_WRITE r m2 n d) usr 15w p`, 252 RW_TAC std_ss [TO_WRITE_READ6,REG_WRITE_WRITE] 253 \\ ASM_SIMP_TAC std_ss [REG_WRITE_def,UPDATE_COMMUTES,not_pc, 254 mode_reg2num_15,mode_reg2num_lt,num2register_11]); 255 256val REG_READ_WRITE = store_thm("REG_READ_WRITE", 257 `(!r m n1 n2 d. REG_READ6 (REG_WRITE r m n1 d) m n2 = 258 if n1 = n2 then d else REG_READ6 r m n2) /\ 259 !r m n d. (REG_WRITE r m n (REG_READ6 r m n) = r)`, 260 RW_TAC std_ss [REG_READ6_def,REG_READ_def,REG_WRITE_def,FETCH_PC_def, 261 APPLY_UPDATE_ID,mode_reg2num_15] \\ SIMP_TAC std_ss [UPDATE_def] 262 \\ PROVE_TAC [r15,not_pc,not_reg_eq,mode_reg2num_lt,num2register_11, 263 DECIDE ``15 < 31``]); 264 265val REG_READ_WRITE_PC = save_thm("REG_READ_WRITE_PC", 266 let val thm = (SPEC_ALL o CONJUNCT1) REG_READ_WRITE in 267 CONJ 268 ((SIMP_RULE arith_ss [TO_WRITE_READ6] o INST [`n2` |-> `15w`]) thm) 269 ((SIMP_RULE arith_ss [TO_WRITE_READ6] o INST [`n1` |-> `15w`]) thm) 270 end); 271 272val REG_READ_WRITE_NEQ = store_thm("REG_READ_WRITE_NEQ", 273 `!r m1 m2 n1 n2 d. ~(n1 = n2) ==> 274 (REG_READ6 (REG_WRITE r m1 n1 d) m2 n2 = REG_READ6 r m2 n2)`, 275 RW_TAC std_ss [REG_READ6_def,REG_READ_def,REG_WRITE_def,FETCH_PC_def, 276 APPLY_UPDATE_ID,mode_reg2num_15] \\ SIMP_TAC std_ss [UPDATE_def] 277 \\ PROVE_TAC [r15,not_pc,not_reg_eq,mode_reg2num_lt,num2register_11, 278 DECIDE ``15 < 31``]); 279 280val REG_READ6_TO_READ_SUB8 = store_thm("REG_READ6_TO_READ_SUB8", 281 `!r m n. REG_READ6 r m n = REG_READ (SUB8_PC r) m n`, 282 RW_TAC bool_ss [TO_WRITE_READ6,READ_TO_READ6,REG_READ_WRITE]); 283 284val SUB8_INV = store_thm("SUB8_INV", 285 `!r. SUB8_PC (ADD8_PC r) = r`, 286 RW_TAC std_ss [SUB8_PC_def,ADD8_PC_def,UPDATE_EQ] 287 \\ REWRITE_TAC [FUN_EQ_THM] 288 \\ RW_TAC std_ss [UPDATE_def,WORD_ADD_SUB]); 289 290(* ------------------------------------------------------------------------- *) 291 292val IF_NEG = store_thm("IF_NEG", 293 `!a b c. (if ~a then b else c) = (if a then c else b)`, PROVE_TAC []); 294 295val UP_DOWN_THM = store_thm("UP_DOWN_THM", 296 `!b x y. (if b then x + y else x - y) = UP_DOWN b x y`, 297 RW_TAC bool_ss [UP_DOWN_def]); 298 299(* ------------------------------------------------------------------------- *) 300 301val DECODE_INST_NOT_UNEXEC = store_thm("DECODE_INST_NOT_UNEXEC", 302 `!n. ~(DECODE_INST n = unexec)`, RW_TAC std_ss [DECODE_INST_def]); 303 304val tac = Cases 305 \\ RW_TAC bool_ss [combinTheory.o_THM,MIN_DEF,DECODE_INST_def,BITS_COMP_THM2, 306 MOD_DIMINDEX,w2w_def,w2n_n2w,word_extract_def,word_bits_n2w] 307 \\ FULL_SIMP_TAC (fcp_ss++SIZES_ss++ARITH_ss) 308 [BIT_def,BITS_COMP_THM2,n2w_def]; 309 310val DATA_PROC_IMP_NOT_BIT4 = store_thm("DATA_PROC_IMP_NOT_BIT4", 311 `!i. (DECODE_INST i = data_proc) /\ ~(i %% 25) ==> 312 ~(((11 >< 0) i):word12 %% 4)`, tac); 313 314val REG_SHIFT_IMP_BITS = store_thm("REG_SHIFT_IMP_BITS", 315 `!i. (DECODE_INST i = reg_shift) ==> 316 ~(i %% 25) /\ ((11 >< 0) i):word12 %% 4`, tac); 317 318val LDR_IMP_BITS = store_thm("LDR_IMP_BITS", 319 `!i. (DECODE_INST i = ldr) ==> (i %% 20)`, 320 RW_TAC arith_ss [DECODE_INST_def]); 321 322val STR_IMP_BITS = store_thm("STR_IMP_BITS", 323 `!i. (DECODE_INST i = str) ==> ~(i %% 20)`, 324 RW_TAC arith_ss [DECODE_INST_def]); 325 326val DECODE_INST_LDM = store_thm("DECODE_INST_LDM", 327 `!i. (DECODE_INST i = ldm) ==> i %% 20`, 328 RW_TAC arith_ss [DECODE_INST_def]); 329 330val DECODE_INST_STM = store_thm("DECODE_INST_STM", 331 `!i. (DECODE_INST i = stm) ==> ~(i %% 20)`, 332 RW_TAC arith_ss [DECODE_INST_def]); 333 334(* ------------------------------------------------------------------------- *) 335 336val n2w_mod32 = (REWRITE_RULE [dimword_def,dimindex_32] o 337 Thm.INST_TYPE [alpha |-> ``:32``]) n2w_mod; 338 339val ALUOUT_ALU_logic = store_thm("ALUOUT_ALU_logic", 340 `!a. SND (ALU_logic a) = a`, 341 SIMP_TAC std_ss [ALU_logic_def]); 342 343val NZ_ALU_logic = store_thm("NZ_ALU_logic", 344 `(!a. FST (FST (ALU_logic a)) = word_msb a) /\ 345 (!a. FST (SND (FST (ALU_logic a))) = (a = 0w))`, 346 SIMP_TAC std_ss [ALU_logic_def]); 347 348val ALUOUT_ADD = store_thm("ALUOUT_ADD", 349 `!a b. SND (ADD a b F) = a + b`, 350 SIMP_TAC arith_ss [ADD_def,ALU_arith_def,DIVMOD_2EXP,word_add_def] 351 \\ SIMP_TAC bool_ss [n2w_mod32,MOD_2EXP_def]); 352 353val NZ_ADD_lem = prove( 354 `!c. (!a b. FST (FST (ADD a b c)) = word_msb (SND (ADD a b c))) /\ 355 !a b. FST (SND (FST (ADD a b c))) = (SND (ADD a b c) = 0w)`, 356 SIMP_TAC (std_ss++SIZES_ss) [ADD_def,ALU_arith_def,DIVMOD_2EXP, 357 MOD_MOD,MOD_2EXP_def,n2w_11]); 358 359val NZ_ADD = save_thm("NZ_ADD", 360 (REWRITE_RULE [ALUOUT_ADD] o SPEC `F`) NZ_ADD_lem); 361 362val ALUOUT_ADD_CARRY = store_thm("ALUOUT_ADD_CARRY", 363 `!a b. SND (ADD a b T) = a + b + 1w`, 364 REWRITE_TAC [GSYM WORD_ADD_ASSOC] 365 \\ SIMP_TAC arith_ss [dimword_def,ADD_def,ALU_arith_def,DIVMOD_2EXP, 366 w2n_n2w,word_add_def] 367 \\ SIMP_TAC bool_ss [n2w_mod32,MOD_PLUS_RIGHT,MOD_2EXP_def,ZERO_LT_TWOEXP] 368 \\ SIMP_TAC bool_ss [dimword_def,n2w_11,MOD_PLUS_RIGHT,ZERO_LT_TWOEXP]); 369 370val ALUOUT_SUB = store_thm("ALUOUT_SUB", 371 `!a b. SND (SUB a b T) = a - b`, 372 SIMP_TAC std_ss 373 [SUB_def,ALUOUT_ADD_CARRY,WORD_NOT,GSYM WORD_ADD_SUB_ASSOC,WORD_SUB_ADD] 374 \\ REWRITE_TAC [word_sub_def]); 375 376val NZ_SUB_lem = prove( 377 `!c. (!a b. FST (FST (SUB a b c)) = word_msb (SND (SUB a b c))) /\ 378 !a b. FST (SND (FST (SUB a b c))) = (SND (SUB a b c) = 0w)`, 379 SIMP_TAC (std_ss++SIZES_ss) [SUB_def,ADD_def,ALU_arith_def,DIVMOD_2EXP, 380 MOD_MOD,MOD_2EXP_def,n2w_11]); 381 382val NZ_SUB = save_thm("NZ_SUB", 383 (REWRITE_RULE [ALUOUT_SUB] o SPEC `T`) NZ_SUB_lem); 384 385(* ------------------------------------------------------------------------- *) 386 387val lem = prove( 388 `!n wl. 0 < wl /\ ~(wl - 1 < n) ==> (n MOD wl = n)`, 389 RW_TAC bool_ss [NOT_LESS,LESS_MOD, 390 DECIDE ``0 < wl /\ n <= wl - 1 ==> n < wl``]); 391 392val SLICE_ROR_THM = store_thm("SLICE_ROR_THM", 393 `!h l a. ((h '' l) a) #>> l = (h -- l) a`, 394 REPEAT STRIP_TAC \\ Cases_on `l = 0` 395 >> ASM_REWRITE_TAC [WORD_SLICE_BITS_THM,SHIFT_ZERO] 396 \\ Cases_on `a` 397 \\ RW_TAC arith_ss [MIN_DEF,word_slice_n2w,word_bits_n2w,BITS_COMP_THM2, 398 SLICE_THM,w2n_n2w] 399 << [ 400 Cases_on `h < l` >> ASM_SIMP_TAC arith_ss [BITS_ZERO,ZERO_SHIFT] 401 \\ `l <= dimindex (:'a) - 1` by DECIDE_TAC, 402 Cases_on `dimindex (:'a) - 1 < l` 403 >> ASM_SIMP_TAC arith_ss [BITS_ZERO,ZERO_SHIFT]] 404 \\ RW_TAC arith_ss [BITS_ZERO3,ADD1,lem,word_ror_n2w, 405 ZERO_LT_TWOEXP,ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0] 406 \\ ASM_SIMP_TAC arith_ss [BITS_SLICE_THM2, 407 (GSYM o ONCE_REWRITE_RULE [MULT_COMM]) SLICE_THM]); 408 409val SHIFT_ALIGN = store_thm("SHIFT_ALIGN", 410 `!x:word32. w2n (8w:word8 * w2w (((1 >< 0) x):word2)) = 411 8 * w2n (((1 >< 0) x):word2)`, 412 STRIP_TAC \\ ISPEC_THEN `((1 >< 0) x):word2` ASSUME_TAC w2n_lt 413 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) [w2w_def,word_mul_n2w,w2n_n2w]); 414 415(* ------------------------------------------------------------------------- *) 416 417fun Cases_on_nzcv tm = 418 FULL_STRUCT_CASES_TAC (SPEC tm (armLib.tupleCases 419 ``(n,z,c,v):bool#bool#bool#bool``)); 420 421val SET_NZCV_IDEM = store_thm("SET_NZCV_IDEM", 422 `!a b c. SET_NZCV a (SET_NZCV b c) = SET_NZCV a c`, 423 REPEAT STRIP_TAC \\ Cases_on_nzcv `a` \\ Cases_on_nzcv `b` 424 \\ RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 425 [SET_NZCV_def,word_modify_def]); 426 427val DECODE_NZCV_SET_NZCV = store_thm("DECODE_NZCV_SET_NZCV", 428 `(!a b c d n. (SET_NZCV (a,b,c,d) n) %% 31 = a) /\ 429 (!a b c d n. (SET_NZCV (a,b,c,d) n) %% 30 = b) /\ 430 (!a b c d n. (SET_NZCV (a,b,c,d) n) %% 29 = c) /\ 431 (!a b c d n. (SET_NZCV (a,b,c,d) n) %% 28 = d)`, 432 RW_TAC (fcp_ss++SIZES_ss) [SET_NZCV_def,word_modify_def]); 433 434val DECODE_IFMODE_SET_NZCV = store_thm("DECODE_IFMODE_SET_NZCV", 435 `(!a n. (27 -- 8) (SET_NZCV a n) = (27 -- 8) n) /\ 436 (!a n. (SET_NZCV a n) %% 7 = n %% 7) /\ 437 (!a n. (SET_NZCV a n) %% 6 = n %% 6) /\ 438 (!a n. (SET_NZCV a n) %% 5 = n %% 5) /\ 439 (!a n. (4 >< 0) (SET_NZCV a n) = (4 >< 0) n)`, 440 RW_TAC bool_ss [] \\ Cases_on_nzcv `a` 441 \\ SIMP_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 442 [SET_NZCV_def,word_modify_def,word_extract_def,word_bits_def]); 443 444val DECODE_IFMODE_SET_IFMODE = store_thm("DECODE_IFMODE_SET_IFMODE", 445 `(!i f m n. (SET_IFMODE i f m n) %% 7 = i) /\ 446 (!i f m n. (SET_IFMODE i f m n) %% 6 = f) /\ 447 (!i f m n. (4 >< 0) (SET_IFMODE i f m n) = mode_num m)`, 448 RW_TAC (fcp_ss++ARITH_ss++SIZES_ss) [SET_IFMODE_def,word_modify_def, 449 word_extract_def,word_bits_def,w2w]); 450 451val SET_IFMODE_IDEM = store_thm("SET_IFMODE_IDEM", 452 `!a b c d e f g. SET_IFMODE a b c (SET_IFMODE d e f g) = SET_IFMODE a b c g`, 453 SIMP_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 454 [SET_IFMODE_def,word_modify_def]); 455 456val SET_IFMODE_NZCV_SWP = store_thm("SET_IFMODE_NZCV_SWP", 457 `!a b c d e. SET_IFMODE a b c (SET_NZCV d e) = 458 SET_NZCV d (SET_IFMODE a b c e)`, 459 REPEAT STRIP_TAC \\ Cases_on_nzcv `d` 460 \\ RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 461 [SET_NZCV_def,SET_IFMODE_def,word_modify_def] 462 \\ Cases_on `i < 5` \\ ASM_SIMP_TAC arith_ss [] 463 \\ Cases_on `i < 28` \\ ASM_SIMP_TAC arith_ss []); 464 465val DECODE_NZCV_SET_IFMODE = store_thm("DECODE_NZCV_SET_IFMODE", 466 `(!i f m n. (SET_IFMODE i f m n) %% 31 = n %% 31) /\ 467 (!i f m n. (SET_IFMODE i f m n) %% 30 = n %% 30) /\ 468 (!i f m n. (SET_IFMODE i f m n) %% 29 = n %% 29) /\ 469 (!i f m n. (SET_IFMODE i f m n) %% 28 = n %% 28) /\ 470 (!i f m n. (27 -- 8) (SET_IFMODE i f m n) = (27 -- 8) n) /\ 471 (!i f m n. (SET_IFMODE i f m n) %% 5 = n %% 5)`, 472 RW_TAC (fcp_ss++boolSimps.CONJ_ss++ARITH_ss++SIZES_ss) 473 [SET_IFMODE_def,word_modify_def,word_bits_def]); 474 475val DECODE_MODE_THM = store_thm("DECODE_MODE_THM", 476 `!m psr x y. DECODE_MODE ((4 >< 0) (SET_IFMODE x y m psr)) = m`, 477 Cases \\ RW_TAC (arith_ss++SIZES_ss) [DECODE_IFMODE_SET_IFMODE, 478 DECODE_MODE_def,mode_num_def,n2w_11]); 479 480val DECODE_MODE_mode_num = store_thm("DECODE_MODE_mode_num", 481 `!m. DECODE_MODE (mode_num m) = m`, 482 Cases \\ SIMP_TAC (srw_ss()++SIZES_ss) 483 [DECODE_MODE_def,mode_num_def,n2w_11]); 484 485(* ------------------------------------------------------------------------- *) 486 487val SPSR_READ_THM = store_thm("SPSR_READ_THM", 488 `!psr mode cpsr. 489 (CPSR_READ psr = cpsr) ==> 490 ((if USER mode then cpsr else SPSR_READ psr mode) = SPSR_READ psr mode)`, 491 RW_TAC bool_ss [CPSR_READ_def,SPSR_READ_def,mode2psr_def,USER_def] 492 \\ REWRITE_TAC [mode_case_def]); 493 494val SPSR_READ_THM2 = store_thm("SPSR_READ_THM2", 495 `!psr mode cpsr. USER mode ==> (SPSR_READ psr mode = CPSR_READ psr)`, 496 METIS_TAC [SPSR_READ_THM]); 497 498val CPSR_WRITE_READ = store_thm("CPSR_WRITE_READ", 499 `(!psr m x. CPSR_READ (SPSR_WRITE psr m x) = CPSR_READ psr) /\ 500 (!psr x. CPSR_READ (CPSR_WRITE psr x) = x)`, 501 RW_TAC bool_ss [CPSR_READ_def,CPSR_WRITE_def,SPSR_WRITE_def,UPDATE_def, 502 USER_def,mode2psr_def] 503 \\ Cases_on `m` \\ FULL_SIMP_TAC bool_ss [mode_case_def,psrs_distinct]); 504 505val CPSR_READ_WRITE = store_thm("CPSR_READ_WRITE", 506 `(!psr. CPSR_WRITE psr (CPSR_READ psr) = psr) /\ 507 (!psr mode. USER mode ==> (CPSR_WRITE psr (SPSR_READ psr mode) = psr))`, 508 RW_TAC bool_ss [CPSR_READ_def,CPSR_WRITE_def,SPSR_READ_def,APPLY_UPDATE_ID, 509 USER_def,mode2psr_def] 510 \\ REWRITE_TAC [mode_case_def,APPLY_UPDATE_ID]); 511 512val CPSR_WRITE_WRITE = store_thm("CPSR_WRITE_WRITE", 513 `!psr a b. CPSR_WRITE (CPSR_WRITE psr a) b = CPSR_WRITE psr b`, 514 SIMP_TAC bool_ss [CPSR_WRITE_def,UPDATE_EQ]); 515 516val USER_usr = save_thm("USER_usr", 517 simpLib.SIMP_PROVE bool_ss [USER_def] ``USER usr``); 518 519val PSR_WRITE_COMM = store_thm("PSR_WRITE_COMM", 520 `!psr m x y. SPSR_WRITE (CPSR_WRITE psr x) m y = 521 CPSR_WRITE (SPSR_WRITE psr m y) x`, 522 RW_TAC bool_ss [SPSR_WRITE_def,CPSR_WRITE_def,USER_def,mode2psr_def] 523 \\ Cases_on `m` 524 \\ FULL_SIMP_TAC bool_ss [mode_distinct,mode_case_def,psrs_distinct, 525 UPDATE_COMMUTES]); 526 527val SPSR_READ_WRITE = store_thm("SPSR_READ_WRITE", 528 `!psr m. SPSR_WRITE psr m (SPSR_READ psr m) = psr`, 529 RW_TAC std_ss [SPSR_READ_def,SPSR_WRITE_def,mode2psr_def] 530 \\ Cases_on `m` 531 \\ SIMP_TAC (srw_ss()) [APPLY_UPDATE_ID]); 532 533(* ------------------------------------------------------------------------- *) 534 535val _ = export_theory(); 536