1(* ========================================================================= *) 2(* FILE : multScript.sml *) 3(* DESCRIPTION : A collection of lemmas used to verify the multiply *) 4(* instructions *) 5(* AUTHOR : (c) Anthony Fox, University of Cambridge *) 6(* DATE : 2003 - 2005 *) 7(* ========================================================================= *) 8 9(* interactive use: 10 app load ["pred_setSimps", "wordsLib", "armLib", "iclass_compLib", 11 "armTheory", "coreTheory", "lemmasTheory", "interruptsTheory"]; 12*) 13 14open HolKernel boolLib bossLib; 15open Q arithmeticTheory whileTheory bitTheory wordsTheory wordsLib; 16open iclass_compLib io_onestepTheory; 17open armTheory coreTheory lemmasTheory interruptsTheory; 18 19val _ = new_theory "mult"; 20 21(* ------------------------------------------------------------------------- *) 22 23infix \\ << >> 24 25val op \\ = op THEN; 26val op << = op THENL; 27val op >> = op THEN1; 28 29val Abbr = BasicProvers.Abbr; 30 31val std_ss = std_ss ++ boolSimps.LET_ss; 32val arith_ss = arith_ss ++ boolSimps.LET_ss; 33 34val fcp_ss = armLib.fcp_ss; 35 36val WL = ``dimindex (:'a)``; 37 38val tt = set_trace "types"; 39 40val FST_COND_RAND = ISPEC `FST` COND_RAND; 41val SND_COND_RAND = ISPEC `SND` COND_RAND; 42 43(* ------------------------------------------------------------------------- *) 44 45val MULT_ALU6_ZERO = store_thm("MULT_ALU6_ZERO", 46 `!ireg borrow2 mul dataabt alua alub c. 47 SND (ALU6 mla_mul t3 ireg borrow2 mul dataabt alua alub c) = 48 if ireg %% 21 then alub else 0w`, 49 RW_TAC std_ss [ALUOUT_ALU_logic,ALU6_def]); 50 51val COMM_MULT_DIV = ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV; 52val COMM_DIV_MULT = ONCE_REWRITE_RULE [MULT_COMM] DIV_MULT; 53 54val COMP_VAL_BIT2 = prove( 55 `!a b c d. (~(\(w,a). w /\ (a = 15)) 56 if (c = 15) \/ (c = d) then (F,b) else (T,c))`, 57 RW_TAC std_ss [] \\ FULL_SIMP_TAC bool_ss []); 58 59val MIN_LEM = prove( 60 `!x t. 0 < t ==> (MIN 31 (2 * t + 29) = 31)`, 61 RW_TAC arith_ss [MIN_DEF]); 62 63val BORROW2 = prove( 64 `!n rs. 2 * n <= 32 ==> 65 (BORROW2 rs n = 66 ~(n = 0) /\ (((2 * (n - 1) + 1) >< (2 * (n - 1))) rs):word2 %% 1)`, 67 STRIP_TAC \\ Cases_on `n = 0` \\ 68 RW_TAC (fcp_ss++ARITH_ss++SIZES_ss) [MIN_DEF,LEFT_SUB_DISTRIB,BORROW2_def, 69 w2w,word_extract_def,word_bits_def]); 70 71val MULX_DONE_def = prove( 72 `!n rs. 2 * (SUC n) <= 32 ==> 73 (MULX mla_mul tn (MULZ mla_mul tn ((31 -- (2 * SUC n)) rs)) 74 (BORROW2 rs (SUC n)) 75 (MSHIFT mla_mul (BORROW2 rs n) 76 ((1 >< 0) ((31 -- (2 * n)) rs)) (n2w n)) = 77 MLA_MUL_DONE rs (SUC n))`, 78 STRIP_TAC \\ Cases 79 \\ RW_TAC (arith_ss++SIZES_ss) [MULX_def,MULZ_def,MSHIFT,MLA_MUL_DONE_def, 80 MIN_LEM,BITS_COMP_THM2,NOT_LESS,word_bits_n2w,word_extract_def] 81 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) 82 [w2w_def,w2n_n2w,word_mul_n2w,word_add_n2w,word_bits_n2w,n2w_11, 83 BITS_THM,COMM_DIV_MULT,COMM_MULT_DIV, 84 DECIDE ``!a b c. (a \/ b = a \/ c) = (~a ==> (b = c))``]); 85 86val word_extract = (GSYM o SIMP_RULE std_ss [] o 87 REWRITE_RULE [FUN_EQ_THM]) word_extract_def; 88 89val MULX_DONE_ZERO = 90 (SIMP_RULE std_ss [word_extract,GSYM w2w_def] o 91 SIMP_RULE (arith_ss++SIZES_ss) [w2w_def,word_extract_def,n2w_w2n,w2n_n2w, 92 WORD_ADD_0,WORD_MULT_CLAUSES,MSHIFT,BORROW2,WORD_BITS_COMP_THM] o 93 SPEC `0`) MULX_DONE_def; 94 95(* ------------------------------------------------------------------------- *) 96 97val EXISTS_DONE = prove( 98 `!rs. ?n. MLA_MUL_DONE rs n`, 99 RW_TAC bool_ss [MLA_MUL_DONE_def] 100 \\ EXISTS_TAC `16` \\ SIMP_TAC arith_ss []); 101 102val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o 103 SPECL [`\x. 2 * x <= WL`,`MLA_MUL_DONE rs`]) LEAST_ELIM; 104 105val SPEC_LESS_MULT_MONO = 106 (GEN_ALL o numLib.REDUCE_RULE o INST [`n` |-> `1`] o 107 SPEC_ALL) LESS_MULT_MONO; 108 109val DIV_TWO_MONO_EVEN = prove( 110 `!a b. a < 2 * b = a DIV 2 < b`, 111 REPEAT STRIP_TAC 112 \\ Cases_on `EVEN a` 113 >> (IMP_RES_TAC EVEN_EXISTS \\ 114 ASM_SIMP_TAC arith_ss [COMM_MULT_DIV,SPEC_LESS_MULT_MONO]) 115 \\ RULE_ASSUM_TAC (REWRITE_RULE [GSYM ODD_EVEN]) 116 \\ IMP_RES_TAC ODD_EXISTS 117 \\ ASM_SIMP_TAC arith_ss [ADD1,COMM_DIV_MULT,SPEC_LESS_MULT_MONO]); 118 119val DONE_LESS_EQUAL_WL = prove( 120 `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\ 121 MLA_MUL_DONE rs n ==> 2 * n <= 32`, 122 RW_TAC bool_ss [MLA_MUL_DONE_def,NOT_LESS] 123 << [ 124 FULL_SIMP_TAC arith_ss [BORROW2_def] 125 \\ SPOSE_NOT_THEN STRIP_ASSUME_TAC 126 \\ RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS_EQUAL]) 127 \\ IMP_RES_TAC DIV_TWO_MONO_EVEN 128 \\ PAT_X_ASSUM `!m. m < n ==> P` IMP_RES_TAC 129 \\ FULL_SIMP_TAC arith_ss [], 130 Cases_on `2 * n = 32` >> ASM_SIMP_TAC arith_ss [] 131 \\ `32 < 2 * n` by DECIDE_TAC 132 \\ IMP_RES_TAC DIV_TWO_MONO_EVEN 133 \\ PAT_X_ASSUM `!m. m < n ==> P` IMP_RES_TAC 134 \\ FULL_SIMP_TAC arith_ss []]); 135 136val DUR_LT_EQ_HWL = prove( 137 `!rs. 2 * (MLA_MUL_DUR rs) <= 32`, 138 REWRITE_TAC [MLA_MUL_DUR_def] \\ CONV_TAC (DEPTH_CONV ETA_CONV) 139 \\ PROVE_TAC [DONE_LESS_EQUAL_WL,lem]); 140 141(* ------------------------------------------------------------------------- *) 142 143val lem = (SIMP_RULE arith_ss [EXISTS_DONE,MLA_MUL_DONE_def] o 144 SPECL [`\x. ~(x = 0)`,`MLA_MUL_DONE rs`]) LEAST_ELIM; 145 146val DUR_NEQ_ZERO = prove( 147 `!rs. ~(MLA_MUL_DUR rs = 0)`, 148 REWRITE_TAC [MLA_MUL_DUR_def] \\ CONV_TAC (DEPTH_CONV ETA_CONV) 149 \\ PROVE_TAC [lem]); 150 151(* ------------------------------------------------------------------------- *) 152 153val DONE_DUR = prove( 154 `!rs. MLA_MUL_DONE rs (MLA_MUL_DUR rs)`, 155 REWRITE_TAC [MLA_MUL_DUR_def] 156 \\ CONV_TAC (DEPTH_CONV ETA_CONV) 157 \\ PROVE_TAC [LEAST_EXISTS_IMP,EXISTS_DONE]); 158 159val NOT_DONE_SUC = prove( 160 `!rs n. SUC n <= MLA_MUL_DUR rs ==> ~MLA_MUL_DONE rs n`, 161 RW_TAC bool_ss [MLA_MUL_DUR_def] 162 \\ RULE_ASSUM_TAC (CONV_RULE (DEPTH_CONV ETA_CONV)) 163 \\ ASM_SIMP_TAC arith_ss [LESS_LEAST]); 164 165(* ------------------------------------------------------------------------- *) 166 167val MIN_LEM = prove( 168 `!x t. 0 < t ==> (MIN x (x - 2 + 2 * t) = x)`, 169 RW_TAC arith_ss [MIN_DEF]); 170 171val BITS_X_SUB2 = prove( 172 `!n x rs. ~(n = 0) ==> 173 (((x - 2) -- 0) ((x -- (2 * n)) rs) = (x -- (2 * n)) rs)`, 174 SIMP_TAC arith_ss [WORD_BITS_COMP_THM,MIN_LEM]); 175 176val SPEC_MULT_LESS_EQ_SUC = 177 (GEN_ALL o REWRITE_RULE [SYM TWO] o INST [`p` |-> `1`] o 178 SPEC_ALL) MULT_LESS_EQ_SUC; 179 180val LEQ_MLA_MUL_DUR = prove( 181 `!n rs. n <= MLA_MUL_DUR rs ==> 2 * n <= 32`, 182 REPEAT STRIP_TAC 183 \\ RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SPEC_MULT_LESS_EQ_SUC]) 184 \\ PROVE_TAC [LESS_EQ_TRANS,DUR_LT_EQ_HWL]); 185 186val MUL1 = prove( 187 `!rs n. SUC n <= MLA_MUL_DUR rs ==> 188 ((1 >< 0) ((31 -- (2 * n)) rs):word2 = ((2 * n + 1) >< (2 * n)) rs)`, 189 RW_TAC arith_ss [ADD1,WORD_BITS_COMP_THM,MIN_DEF,word_extract_def] 190 \\ IMP_RES_TAC LEQ_MLA_MUL_DUR 191 \\ FULL_SIMP_TAC arith_ss []); 192 193val MUL1_SUC = prove( 194 `!n x. (x -- 2) ((x -- (2 * (n + 1))) rs) = 195 (x -- (2 * (n + 2))) rs`, 196 SIMP_TAC arith_ss [WORD_BITS_COMP_THM,MIN_DEF,LEFT_ADD_DISTRIB]); 197 198val COUNT1 = prove( 199 `!n b. (n * 2 + (if b then 1 else 0)) DIV 2 = n`, 200 RW_TAC arith_ss [COMM_MULT_DIV,COMM_DIV_MULT]); 201 202val BITS_X_SUB2_1 = (SIMP_RULE arith_ss [] o SPEC `1`) BITS_X_SUB2; 203val MUL1_SUC_1 = (SIMP_RULE arith_ss [] o SPEC `0`) MUL1_SUC; 204val COUNT1_ZERO = (SIMP_RULE arith_ss [] o SPEC `0`) COUNT1; 205 206val SPEC_MULX_DONE = 207 (GEN_ALL o SIMP_RULE bool_ss [] o DISCH `~(n = 0)` o 208 CONV_RULE (RAND_CONV (REWRITE_CONV [ADD1])) o 209 SIMP_RULE arith_ss [MUL1,MSHIFT,AND_IMP_INTRO, 210 MATCH_MP (DECIDE ``!a b. (a ==> b) ==> (a /\ b = a)``) 211 (SPECL [`SUC n`,`rs`] LEQ_MLA_MUL_DUR)] o 212 DISCH `SUC n <= MLA_MUL_DUR rs` o 213 SIMP_RULE arith_ss [SPEC `SUC n` BORROW2] o SPEC_ALL) MULX_DONE_def; 214 215val DONE_NEQ_ZERO = prove( 216 `!rs. ~MLA_MUL_DONE rs 0`, 217 SIMP_TAC arith_ss [MLA_MUL_DONE_def]); 218 219(* ------------------------------------------------------------------------- *) 220 221val LESS_THM = 222 CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV prim_recTheory.LESS_THM; 223 224val word2_VALUES = prove( 225 `!w:word2. (w = 0w) \/ (w = 1w) \/ (w = 2w) \/ (w = 3w)`, 226 STRIP_TAC \\ ISPEC_THEN `w` ASSUME_TAC w2n_lt 227 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) [GSYM w2n_11,w2n_n2w,LESS_THM]); 228 229val word2_bits = map (fn i => CONJ (EVAL ``BIT 0 ^i``) (EVAL ``BIT 1 ^i``)) 230 [``0``,``1``,``2``,``3``]; 231 232val word2_BITS = prove( 233 `(!w:word2. (w = 0w) = ~(w %% 1) /\ ~(w %% 0)) /\ 234 (!w:word2. (w = 1w) = ~(w %% 1) /\ (w %% 0)) /\ 235 (!w:word2. (w = 2w) = (w %% 1) /\ ~(w %% 0)) /\ 236 !w:word2. (w = 3w) = (w %% 1) /\ (w %% 0)`, 237 REPEAT STRIP_TAC \\ Cases_on `w` 238 \\ SIMP_TAC (fcp_ss++ARITH_ss++SIZES_ss) [LESS_THM,n2w_def] 239 \\ PROVE_TAC word2_bits); 240 241val BIT_VAR = prove( 242 `!w:word2. ~(w = 0w) /\ ~(w = 1w) ==> w %% 1`, 243 METIS_TAC [word2_VALUES,word2_BITS]); 244 245(* ------------------------------------------------------------------------- *) 246 247val CARRY_LEM = store_thm("CARRY_LEM", 248 `!cpsr. NZCV cpsr = FST (DECODE_PSR cpsr)`, 249 SIMP_TAC std_ss [DECODE_PSR_def]); 250 251val LSL_CARRY_SUBST = prove( 252 `!n C x c. ~(n = 0w) ==> (LSL x n c = LSL x n C)`, 253 SIMP_TAC std_ss [LSL_def]); 254 255(* ------------------------------------------------------------------------- *) 256 257val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o 258 SPECL [`\x. 2 * x < 32 ==> ~(BORROW2 rs x)`,`MLA_MUL_DONE rs`]) LEAST_ELIM; 259 260val DONE_EARLY_NOT_BORROW = prove( 261 `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\ MLA_MUL_DONE rs n ==> 262 2 * n < 32 ==> 263 ~BORROW2 rs n`, 264 RW_TAC arith_ss [MLA_MUL_DONE_def,BORROW2_def] 265 \\ FULL_SIMP_TAC bool_ss []); 266 267val DONE_EARLY_NOT_BORROW2 = prove( 268 `!rs. 2 * (MLA_MUL_DUR rs) < 32 ==> ~BORROW2 rs (MLA_MUL_DUR rs)`, 269 REWRITE_TAC [MLA_MUL_DUR_def] 270 \\ CONV_TAC (DEPTH_CONV ETA_CONV) 271 \\ PROVE_TAC [MATCH_MP lem DONE_EARLY_NOT_BORROW]); 272 273val BORROW_IMP_WL = prove( 274 `!rs. BORROW2 rs (MLA_MUL_DUR rs) ==> (2 * (MLA_MUL_DUR rs) = 32)`, 275 REPEAT STRIP_TAC 276 \\ Cases_on `2 * (MLA_MUL_DUR rs) < 32` 277 >> IMP_RES_TAC DONE_EARLY_NOT_BORROW2 278 \\ ASSUME_TAC (SPEC `rs` DUR_LT_EQ_HWL) 279 \\ DECIDE_TAC); 280 281val lem = (SIMP_RULE bool_ss [EXISTS_DONE] o 282 SPECL [`\x. w2n rs MOD 2 ** (2 * x) = w2n rs`,`MLA_MUL_DONE rs`]) LEAST_ELIM; 283 284val DONE_IMP_ZERO_MSBS = prove( 285 `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\ MLA_MUL_DONE rs n ==> 286 (w2n rs MOD 2 ** (2 * n) = w2n rs)`, 287 Cases_on `rs` 288 \\ STRIP_ASSUME_TAC (Thm.INST_TYPE [alpha |-> ``:32``] EXISTS_HB) 289 \\ `Abbrev (m = 31)` 290 by FULL_SIMP_TAC (arith_ss++SIZES_ss) [markerTheory.Abbrev_def] 291 \\ RW_TAC bool_ss [dimword_def,SUC_SUB1,w2n_n2w,MLA_MUL_DONE_def] 292 << [ 293 Cases_on `n'` >> FULL_SIMP_TAC arith_ss [ZERO_MOD] 294 \\ FULL_SIMP_TAC bool_ss [GSYM BITS_ZERO3, 295 DECIDE ``!n. 2 * SUC n = SUC (2 * n + 1)``] 296 \\ RW_TAC arith_ss [BITS_COMP_THM2,MIN_DEF] 297 \\ Cases_on `2 * n'' + 1 = 31` 298 >> FULL_SIMP_TAC (std_ss++SIZES_ss) [Abbr`m`] 299 \\ `2 * n'' + 2 <= 31` 300 by FULL_SIMP_TAC (arith_ss++SIZES_ss) [NOT_LESS] 301 \\ `SLICE 31 (SUC (2 * n'' + 1)) n = 0` 302 by (PAT_X_ASSUM `q = 0w` MP_TAC \\ 303 ASM_SIMP_TAC arith_ss [dimword_def,GSYM BITS_ZERO3,SLICE_THM,MIN_DEF, 304 BITS_COMP_THM2,ZERO_LT_TWOEXP,word_bits_n2w,n2w_11] \\ 305 SIMP_TAC arith_ss [Abbr`m`]) 306 \\ IMP_RES_TAC ((GSYM o SIMP_RULE arith_ss [ADD1,SLICE_ZERO_THM] o 307 SPECL [`31`,`2 * n'' + 1`,`0`]) SLICE_COMP_THM) 308 \\ POP_ASSUM (ASSUME_TAC o SPEC `n`) 309 \\ FULL_SIMP_TAC arith_ss [ADD1,Abbr`m`], 310 FULL_SIMP_TAC bool_ss [NOT_LESS] 311 \\ IMP_RES_TAC LESS_EQUAL_ADD 312 \\ POP_ASSUM (fn th => `2 * n' = SUC (31 + p)` 313 by SIMP_TAC arith_ss [th]) 314 \\ RW_TAC bool_ss [ADD_0,GSYM BITS_ZERO3,BITS_COMP_THM2,MIN_DEF] 315 \\ `p = 0` by DECIDE_TAC 316 \\ FULL_SIMP_TAC arith_ss [ADD1]]); 317 318val DUR_IMP_ZERO_MSBS = prove( 319 `!rs. w2n rs MOD 2 ** (2 * (MLA_MUL_DUR rs)) = w2n rs`, 320 REWRITE_TAC [MLA_MUL_DUR_def] 321 \\ CONV_TAC (DEPTH_CONV ETA_CONV) 322 \\ PROVE_TAC [MATCH_MP lem DONE_IMP_ZERO_MSBS]); 323 324val SPEC_LSL_LIMIT = (GEN_ALL o 325 SIMP_RULE (std_ss++SIZES_ss) [] o SPECL [`a`,`32`] o 326 Thm.INST_TYPE [alpha |-> ``:32``]) LSL_LIMIT; 327 328val RD_INVARIANT_def = Define` 329 RD_INVARIANT A (rm:word32) rs rn n = 330 (if BORROW2 rs n then 331 rm * n2w (w2n rs MOD 2 ** (2 * n)) - rm << (2 * n) 332 else 333 rm * n2w (w2n rs MOD 2 ** (2 * n))) + 334 (if A then rn else 0w)`; 335 336val BORROW2_LEM1 = prove( 337 `!rs:word32. rs %% 1 = ((1 >< 0) rs):word2 %% 1`, 338 Cases \\ SIMP_TAC (fcp_ss++SIZES_ss) 339 [n2w_def,word_extract_def,word_bits_def,w2w]); 340 341val MOD_4_BITS = prove( 342 `!a:word32. w2n a MOD 4 = w2n ((1 -- 0) a)`, 343 Cases 344 \\ STRIP_ASSUME_TAC (Thm.INST_TYPE [alpha |-> ``:32``] EXISTS_HB) 345 \\ ASM_SIMP_TAC bool_ss [dimword_def,GSYM BITS_ZERO3,BITS_COMP_THM2, 346 (EQT_ELIM o EVAL) ``4 = 2 ** SUC 1``,word_bits_n2w,w2n_n2w] 347 \\ FULL_SIMP_TAC (arith_ss++SIZES_ss) [MIN_DEF]); 348 349val RD_INVARIANT_ZERO = 350 (GEN_ALL o 351 SIMP_RULE arith_ss [BORROW2_def,WORD_MULT_CLAUSES,WORD_ADD_0] o 352 INST [`n` |-> `0`] o SPEC_ALL) RD_INVARIANT_def; 353 354val RD_INVARIANT_ONE = (GEN_ALL o 355 SIMP_RULE arith_ss [BORROW2_def,MOD_4_BITS,BORROW2_LEM1, 356 n2w_w2n,GSYM word_bits_n2w] o 357 INST [`n` |-> `1`] o SPEC_ALL) RD_INVARIANT_def; 358 359val RD_INVARIANT_LAST = store_thm("RD_INVARIANT_LAST", 360 `!a rm rs rn. 361 RD_INVARIANT a rm rs rn (MLA_MUL_DUR rs) = 362 rm * rs + (if a then rn else 0w)`, 363 RW_TAC bool_ss [RD_INVARIANT_def,BORROW_IMP_WL,DUR_IMP_ZERO_MSBS, 364 SPEC_LSL_LIMIT,n2w_w2n,WORD_ADD_0,WORD_SUB_RZERO]); 365 366(* ------------------------------------------------------------------------- *) 367 368val MUST_BE_TWO = PROVE [word2_VALUES] 369 ``!w:word2. ~(w = 0w) /\ ~(w = 1w) /\ ~(w = 3w) ==> (w = 2w)``; 370 371val MUST_BE_THREE = PROVE [word2_VALUES] 372 ``!w:word2. ~(w = 0w) /\ ~(w = 1w) /\ ~(w = 2w) ==> (w = 3w)``; 373 374(* ------------------------------------------------------------------------- *) 375 376val SPEC_SLICE_COMP = prove( 377 `!t a. ~(t = 0) ==> 378 (a MOD 2 ** (2 * (t + 1)) = 379 SLICE (2 * t + 1) (2 * t) a + a MOD 2 ** (2 * t))`, 380 REPEAT STRIP_TAC 381 \\ IMP_RES_TAC NOT_ZERO_ADD1 382 \\ ASM_SIMP_TAC arith_ss [DECIDE ``!p. 2 * SUC p = SUC (2 * p + 1)``, 383 GSYM BITS_ZERO3,GSYM SLICE_ZERO_THM,SLICE_COMP_RWT] 384 \\ SIMP_TAC arith_ss [SLICE_ZERO_THM,BITS_ZERO3,ADD1,LEFT_ADD_DISTRIB]); 385 386val SLICE_BITS_THM = prove( 387 `!h m l n. SLICE h l (BITS m 0 n) = SLICE (MIN h m) l n`, 388 RW_TAC arith_ss [SLICE_THM,BITS_COMP_THM2,MIN_DEF] 389 \\ `h = m` by DECIDE_TAC \\ ASM_REWRITE_TAC []); 390 391val MULT_MOD_SUC_T = prove( 392 `!t (a:word32) (b:word32). 393 a * n2w (w2n b MOD 2 ** (2 * (t + 1))) = 394 (a * n2w (w2n b MOD 2 ** (2 * t))) + 395 (a * w2w ((((2 * t + 1) >< (2 * t)) b):word2) << (2 * t))`, 396 REPEAT STRIP_TAC 397 \\ Cases_on `t = 0` 398 >> ASM_SIMP_TAC (arith_ss++SIZES_ss) [WORD_MULT_CLAUSES,WORD_ADD_0, 399 MOD_4_BITS,WORD_BITS_COMP_THM,WORD_SLICE_BITS_THM,SHIFT_ZERO, 400 word_extract_def,n2w_w2n,w2w_w2w,w2w_id] 401 \\ ASM_SIMP_TAC (arith_ss++SIZES_ss) [WORD_EQ_ADD_LCANCEL,SPEC_SLICE_COMP, 402 word_extract_def,w2w_w2w,w2w_id,GSYM word_add_n2w,GSYM WORD_SLICE_THM, 403 WORD_BITS_COMP_THM,WORD_LEFT_ADD_DISTRIB,WORD_ADD_COMM] 404 \\ Cases_on `b` \\ POP_ASSUM (K ALL_TAC) 405 \\ STRIP_ASSUME_TAC (Thm.INST_TYPE [alpha |-> ``:32``] EXISTS_HB) 406 \\ ASM_SIMP_TAC std_ss [dimword_def,GSYM BITS_ZERO3,SLICE_BITS_THM,SUC_SUB1, 407 word_slice_n2w,w2n_n2w]); 408 409val MULT_MOD_SUC_T = save_thm("MULT_MOD_SUC_T", 410 REWRITE_RULE [WORD_SLICE_THM] MULT_MOD_SUC_T); 411 412(* ------------------------------------------------------------------------- *) 413 414val LSL_MULT_EXP = prove( 415 `!w n. w << n = w * n2w (2 ** n)`, 416 Cases \\ POP_ASSUM (K ALL_TAC) 417 \\ RW_TAC bool_ss [word_lsl_n2w,word_mul_n2w] 418 \\ IMP_RES_TAC LESS_ADD_1 419 \\ POP_ASSUM (SUBST1_TAC o SIMP_RULE std_ss [DIMINDEX_GT_0, 420 DECIDE ``0 < n ==> (n - 1 + (p + 1) = p + n)``]) 421 \\ ONCE_REWRITE_TAC [GSYM n2w_mod] 422 \\ SIMP_TAC std_ss 423 [dimword_def,EXP_ADD,MULT_ASSOC,MOD_EQ_0,ZERO_MOD,ZERO_LT_TWOEXP]); 424 425val MULT_TWO_LSL = prove( 426 `!rm t. rm << (2 * t + 1) = (rm << (2 * t)) * n2w 2`, 427 SIMP_TAC arith_ss [LSL_MULT_EXP,GSYM WORD_MULT_ASSOC,word_mul_n2w, 428 GSYM ADD1,EXP]); 429 430val MULT_FOUR_LSL = prove( 431 `!t rm. rm << (2 * (t + 1)) = (rm << (2 * t)) * n2w 4`, 432 SIMP_TAC arith_ss [LSL_MULT_EXP,GSYM WORD_MULT_ASSOC,word_mul_n2w, 433 LEFT_ADD_DISTRIB,EXP_ADD]); 434 435val ALU6_MUL_def = Define` 436 ALU6_MUL borrow2 (mul:word2) (alua:word32) alub = 437 if ~borrow2 /\ (mul = 0w) \/ borrow2 /\ (mul = 3w) then 438 alua 439 else if borrow2 /\ (mul = 0w) \/ (mul = 1w) then 440 alua + alub 441 else 442 alua - alub`; 443 444val BORROW_LEM2 = prove( 445 `!rs n. 2 * (n + 1) <= 32 ==> 446 ((((2 * n + 1) >< (2 * n)) rs = 0w:word2) \/ 447 (((2 * n + 1) >< (2 * n)) rs = 1w:word2) ==> ~BORROW2 rs (n + 1)) /\ 448 ((((2 * n + 1) >< (2 * n)) rs = 2w:word2) \/ 449 (((2 * n + 1) >< (2 * n)) rs = 3w:word2) ==> BORROW2 rs (n + 1))`, 450 RW_TAC arith_ss [word_extract_def,word2_BITS, 451 (SIMP_RULE arith_ss [] o SPEC `n + 1`) BORROW2] 452 \\ FULL_SIMP_TAC (fcp_ss++SIZES_ss) [w2w,word_bits_def]); 453 454val WORD_ADD_SUB_LCANCEL = prove( 455 `!a b. (a + b = a - c) = (b = -c)`, 456 METIS_TAC [WORD_EQ_ADD_LCANCEL,word_sub_def]); 457 458val word2_word32 = 459 LIST_CONJ [EVAL ``w2w:word2->word32 0w``,EVAL ``w2w:word2->word32 1w``, 460 EVAL ``w2w:word2->word32 2w``,EVAL ``w2w:word2->word32 3w``]; 461 462val MSHIFT_lem = prove( 463 `!n. 2 * (n + 1) <= 32 ==> (w2n ((w2w:word4->word5) (n2w n) * 2w) = 2 * n)`, 464 RW_TAC (arith_ss++SIZES_ss) [w2w_def,w2n_n2w,word_mul_n2w]); 465 466val MSHIFT_lem2 = prove( 467 `!n. 2 * (n + 1) <= 32 ==> 468 (w2n ((w2w:word4->word5) (n2w n) * 2w + 1w) = 2 * n + 1)`, 469 RW_TAC (arith_ss++SIZES_ss) [w2w_def,w2n_n2w,word_mul_n2w,word_add_n2w]); 470 471val MUL_1EXP = prove( 472 `!a n. a * 1w << n = a << n`, 473 Cases \\ RW_TAC arith_ss [WORD_MULT_CLAUSES,word_lsl_n2w,word_mul_n2w]); 474 475val MUL_2EXP = prove( 476 `!a n. a * 2w << n = a << (n + 1)`, 477 Cases 478 \\ RW_TAC arith_ss [WORD_MULT_CLAUSES,EXP_ADD,word_lsl_n2w,word_mul_n2w] 479 \\ STRIP_ASSUME_TAC EXISTS_HB 480 \\ FULL_SIMP_TAC arith_ss [NOT_LESS] 481 << [`n' = m` by DECIDE_TAC, `m = 0` by DECIDE_TAC] 482 \\ ASM_SIMP_TAC arith_ss [Once (GSYM n2w_mod),ZERO_LT_TWOEXP,MOD_EQ_0, 483 simpLib.SIMP_PROVE arith_ss [EXP] 484 ``2 * (a * 2 ** b) = a * 2 ** SUC b``, 485 dimword_def,ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0]); 486 487val MUL_3EXP = prove( 488 `!a n. a * 3w << n = a << (n + 1) + a << n`, 489 Cases 490 \\ RW_TAC arith_ss [WORD_MULT_CLAUSES,EXP_ADD,GSYM LEFT_ADD_DISTRIB, 491 word_lsl_n2w,word_mul_n2w,word_add_n2w] 492 \\ STRIP_ASSUME_TAC EXISTS_HB 493 \\ FULL_SIMP_TAC arith_ss [NOT_LESS] 494 << [`n' = m` by DECIDE_TAC, 495 `m = 0` by DECIDE_TAC \\ 496 ONCE_REWRITE_TAC [DECIDE ``3 * n = n * 2 + n``]] 497 \\ ASM_SIMP_TAC std_ss [Once (GSYM n2w_mod),LEFT_ADD_DISTRIB, 498 ZERO_LT_TWOEXP,MOD_TIMES,dimword_def, 499 simpLib.SIMP_PROVE arith_ss [EXP] 500 ``3 * (a * 2 ** b) = a * 2 ** SUC b + a * 2 ** b``] 501 \\ METIS_TAC [n2w_mod,dimword_def,EVAL ``2 ** (SUC 0) = 2``]); 502 503val WORD_LEFT_ADD_DISTRIB_1 = 504 (GEN_ALL o REWRITE_RULE [WORD_MULT_CLAUSES] o 505 SPECL [`v`,`1w`] o GSYM) WORD_LEFT_ADD_DISTRIB; 506 507val WORD_NEG_RMUL_1 = 508 (GEN_ALL o REWRITE_RULE [WORD_MULT_CLAUSES] o 509 SPECL [`v << n`,`1w`]) WORD_NEG_RMUL; 510 511fun MUST_BE_TAC th = 512 TRY (armLib.RES_MP1_TAC [`w` |-> `(2 * n + 1 >< 2 * n) (rs:word32)`] th 513 >> ASM_SIMP_TAC bool_ss []); 514 515val word_add_n2w_mod = prove( 516 `!m n. ((n2w m):bool ** 'a) + n2w n = n2w ((m + n) MOD 2 ** ^WL)`, 517 PROVE_TAC [dimword_def,n2w_mod,word_add_n2w]); 518 519val _ = computeLib.add_thms [word_add_n2w_mod] computeLib.the_compset; 520 521val RD_INVARIANT_THM = store_thm("RD_INVARIANT_THM", 522 `!n a rm rs rn. 2 * (n + 1) <= 32 ==> 523 (RD_INVARIANT a rm rs rn (n + 1) = 524 let borrow2 = BORROW2 rs n 525 and mul = ((2 * n + 1) >< (2 * n)) rs 526 in 527 ALU6_MUL borrow2 mul (RD_INVARIANT a rm rs rn n) 528 (rm << w2n (MSHIFT2 borrow2 mul (n2w n))))`, 529 RW_TAC std_ss [BORROW_LEM2,MSHIFT2_def,RD_INVARIANT_def,ALU6_MUL_def] 530 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [BORROW_LEM2,n2w_11] 531 \\ MAP_EVERY MUST_BE_TAC [MUST_BE_TWO, MUST_BE_THREE] 532 \\ FULL_SIMP_TAC std_ss [BORROW_LEM2] 533 \\ ASM_SIMP_TAC bool_ss [MULT_MOD_SUC_T,WORD_EQ_ADD_LCANCEL,WORD_SUB_LZERO, 534 WORD_RCANCEL_SUB,WORD_ADD_SUB_LCANCEL,GSYM WORD_ADD_ASSOC, 535 WORD_ADD_SUB_ASSOC,GSYM WORD_ADD_SUB_SYM,WORD_ADD_0,WORD_SUB_REFL, 536 WORD_MULT_CLAUSES,CONJUNCT1 ZERO_SHIFT,MSHIFT_lem,MSHIFT_lem2, 537 MUL_1EXP,MUL_2EXP,MUL_3EXP,word2_word32] 538 \\ SIMP_TAC bool_ss [MULT_TWO_LSL,MULT_FOUR_LSL,word_sub_def, 539 AC WORD_ADD_ASSOC WORD_ADD_COMM,WORD_EQ_ADD_LCANCEL, 540 WORD_NEG_RMUL,GSYM WORD_LEFT_ADD_DISTRIB,WORD_LEFT_ADD_DISTRIB_1] 541 \\ REWRITE_TAC [WORD_NEG_RMUL_1,GSYM WORD_LEFT_ADD_DISTRIB] 542 \\ EVAL_TAC \\ REWRITE_TAC [WORD_MULT_CLAUSES]); 543 544val RD_INVARIANT_SUC = prove( 545 `!n a rs. 546 ~(n = 0) /\ SUC n <= MLA_MUL_DUR rs ==> 547 (((2 * n + 1) >< (2 * n)) rs = mul) ==> 548 ((if ~BORROW2 rs n /\ (mul = 0w:word2) \/ BORROW2 rs n /\ (mul = 3w) then 549 RD_INVARIANT a rm rs rn n 550 else 551 (if BORROW2 rs n /\ (mul = 0w) \/ (mul = 1w) then 552 RD_INVARIANT a rm rs rn n + 553 rm << w2n (w2w ((n2w n):word4) * (2w:word5) + 554 (if BORROW2 rs n /\ (mul = 1w) \/ 555 ~BORROW2 rs n /\ (mul = 2w) then 1w else 0w)) 556 else 557 RD_INVARIANT a rm rs rn n - 558 rm << w2n (w2w ((n2w n):word4) * (2w:word5) + 559 (if ~BORROW2 rs n /\ (mul = 2w) then 1w else 0w)))) = 560 RD_INVARIANT a rm rs rn (n + 1))`, 561 NTAC 4 STRIP_TAC 562 \\ IMP_RES_TAC (SPEC `SUC n` LEQ_MLA_MUL_DUR) 563 \\ RW_TAC arith_ss [RD_INVARIANT_THM,ALU6_MUL_def,MSHIFT2_def, 564 MSHIFT_lem,MSHIFT_lem2,WORD_ADD_0,ADD_0]); 565 566val RD_ONE = (GSYM o 567 SIMP_RULE arith_ss [RD_INVARIANT_def,BORROW2,MOD_4_BITS,n2w_w2n] o 568 SIMP_RULE (arith_ss++SIZES_ss) [RD_INVARIANT_ZERO,BORROW2_def,MSHIFT2_def, 569 ALU6_MUL_def,SHIFT_ZERO,WORD_MULT_CLAUSES,WORD_ADD_0,w2w_def, 570 w2n_n2w,EVAL ``1w:word2 = 2w``] o SPEC `0`) RD_INVARIANT_THM; 571 572val BORROW2_SUC = prove( 573 `!rs n. SUC n <= MLA_MUL_DUR rs ==> 574 (((2 * n + 1 >< 2 * n) rs):word2 %% 1 = BORROW2 rs (n + 1))`, 575 REPEAT STRIP_TAC \\ IMP_RES_TAC (SPEC `SUC n` LEQ_MLA_MUL_DUR) 576 \\ FULL_SIMP_TAC arith_ss [ADD1,BORROW2]); 577 578(* ------------------------------------------------------------------------- *) 579 580fun Cases_on_nzc tm = 581 SPEC_THEN tm FULL_STRUCT_CASES_TAC (armLib.tupleCases 582 ``(n,z,c):bool#bool#bool``); 583 584val SET_NZC_IDEM = prove( 585 `!a b xpsr. SET_NZC a (SET_NZC b xpsr) = SET_NZC a xpsr`, 586 REPEAT STRIP_TAC \\ Cases_on_nzc `a` \\ Cases_on_nzc `b` 587 \\ SIMP_TAC bool_ss [SET_NZC_def,SET_NZCV_IDEM,DECODE_NZCV_SET_NZCV]); 588 589val DECODE_MODE_SET_NZC = prove( 590 `!a psr. DECODE_MODE ((4 >< 0) (SET_NZC a psr)) = 591 DECODE_MODE ((4 >< 0) psr)`, 592 STRIP_TAC \\ Cases_on_nzc `a` 593 \\ SIMP_TAC bool_ss [SET_NZC_def,DECODE_MODE_def,DECODE_IFMODE_SET_NZCV]); 594 595val IF_FLAGS_SET_NZC = prove( 596 `!a psr n. (n = 6) \/ (n = 7) ==> ((SET_NZC a psr) %% n = psr %% n)`, 597 STRIP_TAC \\ Cases_on_nzc `a` \\ RW_TAC bool_ss [SET_NZC_def] 598 \\ SIMP_TAC bool_ss [DECODE_IFMODE_SET_NZCV]); 599 600val IF_FLAGS_SET_NZC_COND = prove( 601 `!a psr b n. (n = 6) \/ (n = 7) ==> 602 ((if b then SET_NZC a psr else psr) %% n = psr %% n)`, 603 METIS_TAC [IF_FLAGS_SET_NZC]); 604 605(* ------------------------------------------------------------------------- *) 606 607val MSHIFT_ZERO = prove( 608 `!a. w2w (((4 >< 1) (if a then 1w:word5 else 0w)) + 1w:word4) = 609 w2w (1w:word4):word5`, 610 RW_TAC std_ss [] \\ EVAL_TAC); 611 612val MSHIFT_SUC = prove( 613 `!n. (4 >< 1) 614 (w2w ((n2w n):word4) * (2w:word5) + (if b then 1w else 0w)) + 1w = 615 n2w (n + 1):word4`, 616 RW_TAC (arith_ss++SIZES_ss) [BITS_COMP_THM2, 617 (SIMP_RULE arith_ss [] o SPECL [`4`,`1`]) BITS_ZERO4, 618 (SIMP_RULE arith_ss [] o SPECL [`4`,`1`,`a`,`1`]) BITS_SUM, 619 word_extract_def,word_bits_n2w,n2w_11,MOD_DIMINDEX, 620 word_mul_n2w,word_add_n2w,w2w_n2w] 621 \\ SIMP_TAC std_ss [BITS_ZERO3,ONCE_REWRITE_RULE [ADD_COMM] MOD_PLUS_RIGHT] 622); 623 624val MSHIFT_lem3 = prove( 625 `SUC n <= MLA_MUL_DUR rs ==> n < 16`, 626 REPEAT STRIP_TAC \\ IMP_RES_TAC (SPEC `SUC n` LEQ_MLA_MUL_DUR) 627 \\ FULL_SIMP_TAC arith_ss [ADD1]); 628 629(* ------------------------------------------------------------------------- *) 630 631val arithi_ss = let open armLib in 632 arith_ss++ICLASS_ss++PBETA_ss++STATE_INP_ss++SIZES_ss end; 633 634val MLA_MUL_INVARIANT = Count.apply prove( 635 `!n x i mem reg psr alua pipeb ireg ointstart obaselatch onfq ooonfq 636 oniq oooniq pipeaabt pipebabt dataabt2 aregn2 sctrl psrfb orp. 637 Abbrev (pc = REG_READ6 reg usr 15w) /\ Abbrev (cpsr = CPSR_READ psr) /\ 638 Abbrev (nbs = DECODE_MODE ((4 >< 0) cpsr)) /\ 639 Abbrev (w = MLA_MUL_DUR (REG_READ6 reg nbs ((11 >< 8) ireg))) /\ 640 (!t. t < w + 1 ==> ~IS_RESET i t) /\ n <= w ==> 641 ?ointstart' obaselatch' onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' 642 iregabt' dataabt' aregn'. 643 ~(aregn' IN {0w; 1w; 2w; 5w}) /\ 644 ((aregn' = 7w) ==> ~(CPSR_READ psr %% 6)) /\ 645 ((aregn' = 6w) ==> ~(CPSR_READ psr %% 7)) /\ 646 let Rm = (3 >< 0) ireg and Rd = (19 >< 16) ireg 647 and rs = REG_READ6 reg nbs ((11 >< 8) ireg) 648 and rn = REG_READ6 reg nbs ((15 >< 12) ireg) in 649 let rm = REG_READ6 (INC_PC reg) nbs Rm in 650 (FUNPOW (SNEXT NEXT_ARM6) n <|state := ARM6 (DP 651 (if (Rd = 15w) \/ (Rd = Rm) then 652 REG_WRITE reg nbs 15w (pc + 4w) 653 else 654 REG_WRITE (REG_WRITE reg nbs 15w (pc + 4w)) nbs Rd 655 (if ireg %% 21 then rn else 0w)) 656 psr (pc + 4w) ireg alua rn dout) 657 (CTRL pipea T pipeb T ireg T ointstart F F obaselatch F mla_mul tn 658 F F F onfq ooonfq oniq oooniq pipeaabt pipebabt pipebabt dataabt2 659 aregn2 F T F sctrl psrfb ((1 >< 0) pc) ARB ARB orp ((1 >< 0) rs) 660 ((31 -- 2) rs) F (if (1 >< 0) rs = 2w:word2 then 1w else 0w)); 661 inp := ADVANCE 1 i|> = 662 (let mul = (1 >< 0) ((31 -- (2 * (n - 1))) rs) in 663 let rd = RD_INVARIANT (ireg %% 21) rm rs rn (n - 1) 664 and mshift = MSHIFT mla_mul (BORROW2 rs (n - 1)) mul (n2w (n - 1)) 665 and mul' = (1 >< 0) ((31 -- (2 * n)) rs) 666 and borrow2 = BORROW2 rs n in 667 let rd' = RD_INVARIANT (ireg %% 21) rm rs rn n 668 and newinst = MLA_MUL_DONE rs n in 669 let nxtic = if newinst then 670 if ointstart' then swi_ex else DECODE_INST pipeb 671 else mla_mul in 672 <| state := ARM6 (DP 673 (if (Rd = 15w) \/ (Rd = Rm) then 674 REG_WRITE reg nbs 15w (pc + 4w) 675 else 676 REG_WRITE (REG_WRITE reg nbs 15w (pc + 4w)) nbs Rd rd') 677 (if (n = 0) \/ ~(ireg %% 20) \/ (Rd = 15w) \/ (Rd = Rm) then 678 psr 679 else 680 CPSR_WRITE psr (SET_NZC (word_msb rd',rd' = 0w, 681 FST (LSL rm (w2w mshift) 682 (CARRY (FST (DECODE_PSR cpsr))))) cpsr)) 683 (pc + 4w) (if newinst then pipeb else ireg) 684 (if n = 0 then 685 alua 686 else if (Rd = 15w) \/ (Rd = Rm) then 687 REG_READ6 (REG_WRITE reg nbs 15w (pc + 4w)) nbs Rd 688 else 689 rd) 690 (if n = 0 then rn else rm << w2n mshift) 691 (if n = 0 then dout else rm)) 692 (CTRL 693 pipea T (if newinst then pipea else pipeb) T 694 (if newinst then pipeb else ireg) T ointstart' newinst newinst 695 obaselatch' newinst nxtic (if newinst then t3 else tn) 696 F F F onfq' ooonfq' oniq' oooniq' pipeaabt' pipebabt' 697 (if newinst then iregabt' else pipebabt') dataabt' 698 (if n = 0 then aregn2 else if ointstart' then aregn' else 2w) 699 (~(n = 0) /\ newinst) T F sctrl psrfb 700 (if n = 0 then (1 >< 0) pc else (1 >< 0) (pc + n2w 4)) 701 (MASK nxtic (if newinst then t3 else tn) ARB ARB) 702 ARB (if n = 0 then orp else ARB) mul' ((31 -- (2 * (n + 1))) rs) 703 borrow2 (MSHIFT mla_mul borrow2 mul' (n2w n))); 704 inp := ADVANCE n (ADVANCE 1 i)|>))`, 705 REPEAT STRIP_TAC 706 \\ SIMP_TAC bool_ss [LET_THM] 707 \\ ABBREV_TAC `Rm:word4 = (3 >< 0) ireg` 708 \\ ABBREV_TAC `Rd:word4 = (19 >< 16) ireg` 709 \\ ABBREV_TAC `rs = REG_READ6 reg nbs ((11 >< 8) ireg)` 710 \\ ABBREV_TAC `rn = REG_READ6 reg nbs ((15 >< 12) ireg)` 711 \\ ABBREV_TAC `rm = REG_READ6 (INC_PC reg) nbs Rm` 712 \\ Induct_on `n` 713 >> (SIMP_TAC (arith_ss++armLib.ICLASS_ss++armLib.STATE_INP_ss) 714 [state_arm6_11,ctrl_11,io_onestepTheory.state_out_literal_11,FUNPOW, 715 BORROW2_def,MSHIFT,RD_INVARIANT_ZERO,MASK_def,WORD_MULT_CLAUSES, 716 DONE_NEQ_ZERO,io_onestepTheory.ADVANCE_ZERO,WORD_ADD_0,w2w_0] 717 \\ SIMP_TAC std_ss [word_extract_def,WORD_BITS_COMP_THM] 718 \\ METIS_TAC [interrupt_exists]) 719 \\ REWRITE_TAC [FUNPOW_SUC] 720 \\ Cases_on `n = 0` 721 << [ 722 PAT_X_ASSUM `x ==> P` (K ALL_TAC) 723 \\ ASM_REWRITE_TAC [FUNPOW] 724 \\ REPEAT STRIP_TAC 725 \\ FULL_SIMP_TAC bool_ss [Abbr`pc`,REG_READ_WRITE,TO_WRITE_READ6] 726 \\ `~IS_RESET i 1` by ASM_SIMP_TAC arith_ss [] 727 \\ IMP_RES_TAC NOT_RESET_EXISTS 728 \\ ASM_SIMP_TAC std_ss [SNEXT,ADVANCE_def] \\ MLA_MUL_TAC 729 \\ ASM_SIMP_TAC arithi_ss 730 [FST_COND_RAND,SND_COND_RAND,IF_NEG,COMP_VAL_BIT2,BITS_X_SUB2_1, 731 LSL_ZERO,ALUOUT_ADD,ALUOUT_SUB,COUNT1_ZERO,MUL1_SUC_1,BORROW2, 732 MULX_DONE_ZERO,BITS_ZEROL,RD_INVARIANT_ZERO,SND_LSL,NZ_SUB, 733 ALUOUT_ALU_logic,NZ_ALU_logic,NZ_ADD,WORD_BITS_COMP_THM, 734 COND_PAIR,CARRY_LEM,state_arm6_11,dp_11] 735 \\ Cases_on `~(Rd = 15w) /\ ~(Rd = Rm)` 736 \\ FULL_SIMP_TAC (armLib.stdi_ss++SIZES_ss) 737 [(GSYM o ISPEC `word_msb`) COND_RAND,SHIFT_ZERO,n2w_11,word_0_n2w, 738 AREGN1_def,(GSYM o BETA_RULE o ISPEC `\x. x = 0w`) COND_RAND, 739 REG_READ_WRITE,TO_WRITE_READ6,REG_WRITE_WRITE,REG_READ_WRITE_PC, 740 MSHIFT_ZERO,IF_NEG,RD_INVARIANT_ONE,RD_ONE,WORD_EXTRACT_BITS_COMP, 741 w2w_0,WORD_MULT_CLAUSES,WORD_ADD_0,w2n_w2w,ctrl_11] 742 \\ UNABBREV_TAC `rm` \\ POP_ASSUM_LIST (K ALL_TAC) 743 \\ EXISTS_TAC `pipebabt` 744 \\ EXISTS_TAC `if dataabt2 \/ ~(cpsr %% 6) /\ ~ooonfq \/ pipebabt \/ 745 ~(cpsr %% 7) /\ ~oooniq 746 then 747 AREGN1 F dataabt2 (~(cpsr %% 6) /\ ~ooonfq) 748 (~(cpsr %% 7) /\ ~oooniq) F pipebabt 749 else 3w` 750 \\ RW_TAC std_ss [AREGN1_def] 751 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [pred_setTheory.IN_INSERT,n2w_11, 752 pred_setTheory.NOT_IN_EMPTY], 753 STRIP_TAC 754 \\ `n <= w` by DECIDE_TAC 755 \\ PAT_X_ASSUM `nn ==> P` IMP_RES_TAC 756 \\ ASM_SIMP_TAC arith_ss [NOT_DONE_SUC,BORROW2, 757 GSYM io_onestepTheory.ADVANCE_COMP,ADD1] 758 \\ POP_ASSUM (K ALL_TAC) 759 \\ FULL_SIMP_TAC bool_ss [Abbr`pc`,REG_READ_WRITE,TO_WRITE_READ6] 760 \\ `~IS_RESET i (n + 1)` by ASM_SIMP_TAC arith_ss [] 761 \\ IMP_RES_TAC NOT_RESET_EXISTS 762 \\ ASM_SIMP_TAC arith_ss [Abbr`w`,SNEXT,ADVANCE_def] \\ MLA_MUL_TAC 763 \\ ASM_SIMP_TAC arithi_ss 764 [GSYM ADVANCE_COMP,COND_PAIR,FST_COND_RAND,SND_COND_RAND, 765 (REWRITE_RULE [combinTheory.o_THM] o 766 ISPEC `DECODE_MODE o (4 >< 0)`) COND_RAND, 767 ISPEC `CPSR_READ` COND_RAND,IF_NEG,COMP_VAL_BIT2,COUNT1,ADD1, 768 (SIMP_RULE std_ss [] o SPECL [`n`,`31`]) BITS_X_SUB2,MSHIFT_SUC, 769 CPSR_WRITE_WRITE,CPSR_WRITE_READ,DECODE_MODE_SET_NZC,w2n_w2w, 770 SPEC_MULX_DONE,ALUOUT_ADD,ALUOUT_SUB,SND_LSL,ALUOUT_ALU_logic, 771 NZ_ALU_logic,NZ_ADD,NZ_SUB,CARRY_LEM,MUL1,MUL1_SUC,state_arm6_11] 772 \\ Cases_on `~(Rd = 15w) /\ ~(Rd = Rm)` 773 \\ FULL_SIMP_TAC bool_ss [dp_11,ctrl_11,RD_INVARIANT_SUC,BORROW2_SUC, 774 (GSYM o ISPEC `word_msb`) COND_RAND,IF_FLAGS_SET_NZC_COND, 775 (GSYM o BETA_RULE o ISPEC `\x. x = 0w`) COND_RAND, 776 TO_WRITE_READ6,REG_READ_WRITE,REG_READ_WRITE_PC, 777 SET_NZC_IDEM,REG_WRITE_WRITE,IF_NEG] 778 \\ EXISTS_TAC `pipebabt'` 779 \\ EXISTS_TAC `if dataabt' \/ ~(cpsr %% 6) /\ ~ooonfq' \/ 780 pipebabt' \/ ~(cpsr %% 7) /\ ~oooniq' 781 then 782 AREGN1 F dataabt' (~(cpsr %% 6) /\ ~ooonfq') 783 (~(cpsr %% 7) /\ ~oooniq') F pipebabt' 784 else 3w` 785 << [ 786 PAT_ABBREV_TAC `bigc = CARRY (FST (DECODE_PSR (SET_NZC (a,b,c) x)))` 787 \\ ABBREV_TAC `mul:word2 = ((2 * n + 1) >< (2 * n)) rs` 788 \\ PAT_ABBREV_TAC `mshift:word8 = w2w (w:word5)` 789 \\ `~(mshift = 0w)` 790 by (IMP_RES_TAC MSHIFT_lem3 \\ 791 RW_TAC (arith_ss++SIZES_ss) 792 [Abbr`mshift`,BITS_COMP_THM2,BITS_ZERO2,w2w_n2w,word_mul_n2w, 793 word_add_n2w,REWRITE_RULE [MOD_DIMINDEX] n2w_11, 794 (SIMP_RULE std_ss [] o SPEC `3`) BITS_ZEROL] \\ 795 ASM_SIMP_TAC arith_ss [ 796 (SIMP_RULE std_ss [] o SPEC `4`) BITS_ZEROL]) 797 \\ POP_ASSUM (fn th => ASSUME_TAC (MATCH_MP LSL_CARRY_SUBST th)) 798 \\ POP_ASSUM (fn th => SUBST1_TAC (SPECL 799 [`CARRY (FST (DECODE_PSR cpsr))`,`rm`,`bigc`] th)) 800 \\ REWRITE_TAC [], ALL_TAC, ALL_TAC] 801 \\ POP_ASSUM_LIST (K ALL_TAC) 802 \\ RW_TAC armLib.stdi_ss [AREGN1_def] 803 \\ FULL_SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss++SIZES_ss) [n2w_11] 804 ] 805); 806 807(* ------------------------------------------------------------------------- *) 808 809val MLA_MUL_INVARIANT = save_thm("MLA_MUL_INVARIANT", 810 (GEN_ALL o SIMP_RULE std_ss []) MLA_MUL_INVARIANT); 811 812val lem = SPEC `w = MLA_MUL_DUR (REG_READ6 reg nbs ((11 >< 8) ireg))` 813 markerTheory.Abbrev_def; 814 815val MLA_MUL_TN = save_thm("MLA_MUL_TN", 816 (GEN_ALL o SIMP_RULE std_ss [] o ONCE_REWRITE_RULE [GSYM lem] o 817 SIMP_RULE arith_ss [lem,TO_WRITE_READ6,RD_INVARIANT_LAST, 818 DONE_DUR,DUR_NEQ_ZERO] o 819 INST [`n` |-> `w`] o SPEC_ALL) MLA_MUL_INVARIANT); 820 821(* ------------------------------------------------------------------------- *) 822 823val _ = export_theory(); 824