1(* ------------------------------------------------------------------------ 2 Definitions and theorems used by MIPS step evaluator (mips_stepLib) 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6 7open utilsLib 8open wordsLib blastLib 9open alignmentTheory mipsTheory 10 11val _ = new_theory "mips_step" 12 13(* ------------------------------------------------------------------------ *) 14 15val _ = List.app (fn f => f ()) 16 [numLib.prefer_num, wordsLib.prefer_word, wordsLib.guess_lengths] 17 18(* ------------------------------------------------------------------------ *) 19 20val NextStateMIPS_def = Define` 21 NextStateMIPS s0 = 22 let s1 = Next s0 in if s1.exception = NoException then SOME s1 else NONE` 23 24val exceptionSignalled_id = Q.prove( 25 `!s. ~s.exceptionSignalled ==> (s with exceptionSignalled := F = s)`, 26 lrw [mips_state_component_equality]) 27 28val tac = 29 lrw [NextStateMIPS_def, Next_def, AddressTranslation_def, 30 exceptionSignalled_id] 31 \\ Cases_on `(Run (Decode w) s).BranchTo` 32 \\ Cases_on `(Run (Decode w) s).BranchDelay` 33 \\ TRY (Cases_on `x`) 34 \\ lrw [] 35 \\ fs [mips_state_component_equality] 36 37val NextStateMIPS_nodelay = utilsLib.ustore_thm("NextStateMIPS_nodelay", 38 `(s.exception = NoException) /\ 39 (s.BranchDelay = NONE) /\ 40 ~s.exceptionSignalled ==> 41 (Fetch s = (SOME w, s)) /\ 42 (Decode w = i) /\ 43 (Run i s = next_state) /\ 44 (next_state.exception = s.exception) /\ 45 (next_state.BranchDelay = NONE) /\ 46 (next_state.BranchTo = b) ==> 47 (NextStateMIPS s = 48 SOME (next_state with 49 <| PC := case b of SOME (T, a) => a | _ => next_state.PC + 4w; 50 BranchDelay := case b of SOME (F, a) => SOME (SOME a) 51 | SOME (T, _) => SOME NONE 52 | _ => NONE; 53 BranchTo := NONE; 54 exceptionSignalled := F; 55 CP0 := next_state.CP0 with 56 Count := next_state.CP0.Count + 1w |>))`, 57 tac 58 ) 59 60val NextStateMIPS_delay = utilsLib.ustore_thm("NextStateMIPS_delay", 61 `(s.exception = NoException) /\ 62 (s.BranchDelay = SOME d) /\ 63 ~s.exceptionSignalled ==> 64 (Fetch s = (SOME w, s)) /\ 65 (Decode w = i) /\ 66 (Run i s = next_state) /\ 67 (next_state.exception = s.exception) /\ 68 (next_state.BranchDelay = s.BranchDelay) /\ 69 (next_state.BranchTo = NONE) ==> 70 (NextStateMIPS s = 71 SOME (next_state with 72 <| PC := case d of SOME a => a | NONE => next_state.PC + 4w; 73 BranchDelay := NONE; 74 exceptionSignalled := F; 75 CP0 := next_state.CP0 with 76 Count := next_state.CP0.Count + 1w |>))`, 77 tac 78 ) 79 80(* exceptions can occur in the branch delay slot *) 81val NextStateMIPS_exception = utilsLib.ustore_thm("NextStateMIPS_exception", 82 `(s.exception = NoException) /\ 83 (s.BranchDelay = SOME d) /\ 84 ~s.exceptionSignalled ==> 85 (Fetch s = (SOME w, s)) /\ 86 (Decode w = i) /\ 87 (Run i s = next_state) /\ 88 (next_state.exception = s.exception) /\ 89 (next_state.BranchDelay = if b then NONE else s.BranchDelay) /\ 90 (next_state.BranchTo = NONE) ==> 91 (NextStateMIPS s = 92 SOME (next_state with 93 <| PC := if b then 94 next_state.PC + 4w 95 else 96 (case d of SOME a => a | NONE => next_state.PC + 4w); 97 BranchDelay := NONE; 98 exceptionSignalled := F; 99 CP0 := next_state.CP0 with 100 Count := next_state.CP0.Count + 1w |>))`, 101 tac 102 ) 103 104(* ------------------------------------------------------------------------ *) 105 106val not31 = Q.store_thm("not31", 107 `x0 /\ x1 /\ x2 /\ x3 /\ x4 = (v2w [x0; x1; x2; x3; x4] = (31w: word5))`, 108 blastLib.BBLAST_TAC 109 ) 110 111val v2w_0_rwts = Q.store_thm("v2w_0_rwts", 112 `((v2w [F; F; F; F; F] = 0w: word5)) /\ 113 ((v2w [T; b3; b2; b1; b0] = 0w: word5) = F) /\ 114 ((v2w [b3; T; b2; b1; b0] = 0w: word5) = F) /\ 115 ((v2w [b3; b2; T; b1; b0] = 0w: word5) = F) /\ 116 ((v2w [b3; b2; b1; T; b0] = 0w: word5) = F) /\ 117 ((v2w [b3; b2; b1; b0; T] = 0w: word5) = F)`, 118 blastLib.BBLAST_TAC 119 ) 120 121val NotWordValue0 = Q.store_thm("NotWordValue0", 122 `!b x. ~NotWordValue 0w`, 123 lrw [NotWordValue_def] 124 ) 125 126val NotWordValueCond = Q.store_thm("NotWordValueCond", 127 `!b x. NotWordValue (if b then 0w else x) = ~b /\ NotWordValue x`, 128 lrw [NotWordValue0] 129 ) 130 131val sw16_to_sw64 = Q.store_thm("sw16_to_sw64", 132 `!a:word16. sw2sw (sw2sw a : word32) = sw2sw a : word64`, 133 rw [wordsTheory.sw2sw_sw2sw] 134 ) 135 136val get_bytes = Q.store_thm("get_bytes", 137 `((31 >< 24) 138 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 139 b23; b22; b21; b20; b19; b18; b17; b16; 140 b15; b14; b13; b12; b11; b10; b9; b8; 141 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 142 v2w [b31; b30; b29; b28; b27; b26; b25; b24]: word8) /\ 143 ((23 >< 16) 144 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 145 b23; b22; b21; b20; b19; b18; b17; b16; 146 b15; b14; b13; b12; b11; b10; b9; b8; 147 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 148 v2w [b23; b22; b21; b20; b19; b18; b17; b16]: word8) /\ 149 ((15 >< 8) 150 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 151 b23; b22; b21; b20; b19; b18; b17; b16; 152 b15; b14; b13; b12; b11; b10; b9; b8; 153 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 154 v2w [b15; b14; b13; b12; b11; b10; b9; b8]: word8) /\ 155 ((7 >< 0) 156 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 157 b23; b22; b21; b20; b19; b18; b17; b16; 158 b15; b14; b13; b12; b11; b10; b9; b8; 159 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 160 v2w [b7; b6; b5; b4; b3; b2; b1; b0]: word8)`, 161 blastLib.BBLAST_TAC 162 ) 163 164val cast_thms = Q.store_thm("cast_thms", 165 `!w: word32. sw2sw ((31 >< 0) (w2w w : word64) : word32) = sw2sw w : word64`, 166 blastLib.BBLAST_TAC 167 ) 168 169(* ------------------------------------------------------------------------ *) 170 171val tac = 172 wordsLib.Cases_word_value 173 \\ simp [] 174 \\ ntac 2 strip_tac 175 \\ blastLib.BBLAST_TAC 176 177val select_byte_le = Q.store_thm("select_byte_le", 178 `!b:word3 a:word64 f:word64->word8. 179 (7 + 8 * w2n b >< 8 * w2n b) 180 (f (a + 7w) @@ 181 f (a + 6w) @@ 182 f (a + 5w) @@ 183 f (a + 4w) @@ 184 f (a + 3w) @@ 185 f (a + 2w) @@ 186 f (a + 1w) @@ 187 f a) = f (a + w2w b)`, 188 tac 189 ) 190 191val select_byte_be = Q.store_thm("select_byte_be", 192 `!b:word3 a:word64 f:word64->word8. 193 (7 + 8 * w2n b >< 8 * w2n b) 194 (f a @@ 195 f (a + 1w) @@ 196 f (a + 2w) @@ 197 f (a + 3w) @@ 198 f (a + 4w) @@ 199 f (a + 5w) @@ 200 f (a + 6w) @@ 201 f (a + 7w)) = f (a + w2w (b ?? 7w))`, 202 tac 203 ) 204 205val select_half_le = Q.prove( 206 `!b:word3 f:word64->word8 a:word64. 207 ~word_bit 0 b ==> 208 ((15 + 8 * w2n b >< 8 * w2n b) 209 (f (a + 7w) @@ 210 f (a + 6w) @@ 211 f (a + 5w) @@ 212 f (a + 4w) @@ 213 f (a + 3w) @@ 214 f (a + 2w) @@ 215 f (a + 1w) @@ 216 f a) = (f (a + w2w b + 1w) @@ f (a + w2w b)) : word16)`, 217 tac 218 ) 219 220val select_half_be = Q.prove( 221 `!b:word3 f:word64->word8 a:word64. 222 ~word_bit 0 b ==> 223 ((15 + 8 * w2n b >< 8 * w2n b) 224 (f a @@ 225 f (a + 1w) @@ 226 f (a + 2w) @@ 227 f (a + 3w) @@ 228 f (a + 4w) @@ 229 f (a + 5w) @@ 230 f (a + 6w) @@ 231 f (a + 7w)) = 232 (f (a + w2w (b ?? 6w)) @@ f (a + w2w (b ?? 6w) + 1w)) : word16)`, 233 tac 234 ) 235 236val select_word_le = Q.prove( 237 `!b:word3 f:word64->word8 a:word64. 238 ((1 >< 0) b = 0w:word2) ==> 239 ((31 + 8 * w2n b >< 8 * w2n b) 240 (f (a + 7w) @@ 241 f (a + 6w) @@ 242 f (a + 5w) @@ 243 f (a + 4w) @@ 244 f (a + 3w) @@ 245 f (a + 2w) @@ 246 f (a + 1w) @@ 247 f a) = 248 (f (a + w2w b + 3w) @@ f (a + w2w b + 2w) @@ 249 f (a + w2w b + 1w) @@ f (a + w2w b)) : word32)`, 250 tac 251 ) 252 253val select_word_be = Q.prove( 254 `!b:word3 f:word64->word8 a:word64. 255 ((1 >< 0) b = 0w:word2) ==> 256 ((31 + 8 * w2n b >< 8 * w2n b) 257 (f a @@ 258 f (a + 1w) @@ 259 f (a + 2w) @@ 260 f (a + 3w) @@ 261 f (a + 4w) @@ 262 f (a + 5w) @@ 263 f (a + 6w) @@ 264 f (a + 7w)) = 265 (f (a + w2w (b ?? 4w)) @@ f (a + w2w (b ?? 4w) + 1w) @@ 266 f (a + w2w (b ?? 4w) + 2w) @@ f (a + w2w (b ?? 4w) + 3w)) : word32)`, 267 tac 268 ) 269 270val select_parts = Q.store_thm("select_parts", 271 `!a0: word8 a1: word8 a2: word8 a3: word8 a4: word8 a5: word8 a6: word8 272 a7: word8. 273 let w = a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0 274 in 275 ((7 >< 0) w = a0) /\ 276 ((15 >< 0) w = (a1 @@ a0) : word16) /\ 277 ((23 >< 0) w = (a2 @@ a1 @@ a0) : word24) /\ 278 ((31 >< 0) w = (a3 @@ a2 @@ a1 @@ a0) : word32) /\ 279 ((39 >< 0) w = (a4 @@ a3 @@ a2 @@ a1 @@ a0) : 40 word) /\ 280 ((47 >< 0) w = (a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : word48) /\ 281 ((55 >< 0) w = (a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1 @@ a0) : 56 word) /\ 282 ((63 >< 0) w = w) /\ 283 ((39 >< 32) w = a4) /\ 284 ((47 >< 32) w = (a5 @@ a4) : word16) /\ 285 ((55 >< 32) w = (a6 @@ a5 @@ a4) : word24) /\ 286 ((63 >< 32) w = (a7 @@ a6 @@ a5 @@ a4) : word32) /\ 287 ((31 >< 8) w = (a3 @@ a2 @@ a1) : word24) /\ 288 ((31 >< 16) w = (a3 @@ a2) : word16) /\ 289 ((31 >< 24) w = a3) /\ 290 ((63 >< 8) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2 @@ a1) : 56 word) /\ 291 ((63 >< 16) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3 @@ a2) : word48) /\ 292 ((63 >< 24) w = (a7 @@ a6 @@ a5 @@ a4 @@ a3) : 40 word) /\ 293 ((63 >< 32) w = (a7 @@ a6 @@ a5 @@ a4) : word32) /\ 294 ((63 >< 40) w = (a7 @@ a6 @@ a5) : word24) /\ 295 ((63 >< 48) w = (a7 @@ a6) : word16) /\ 296 ((63 >< 56) w = a7 : word8)`, 297 SIMP_TAC (srw_ss()++boolSimps.LET_ss++wordsLib.WORD_EXTRACT_ss) [] 298 ) 299 300(* ------------------------------------------------------------------------ *) 301 302val bit_0_2_0 = Theory.save_thm("bit_0_2_0", 303 blastLib.BBLAST_PROVE 304 ``word_bit 0 (((2 >< 0) (a:word64)) : word3) = word_bit 0 a`` 305 ) 306 307val bit_0_2_0_6 = Theory.save_thm("bit_0_2_0_6", 308 blastLib.BBLAST_PROVE 309 ``word_bit 0 (((2 >< 0) (a:word64)) : word3 ?? 6w) = word_bit 0 a`` 310 ) 311 312val bit_1_0_2_0 = Theory.save_thm("bit_1_0_2_0", 313 blastLib.BBLAST_PROVE 314 ``(1 >< 0) (((2 >< 0) (a:word64)) : word3) = ((1 >< 0) a) : word2`` 315 ) 316 317val bit_1_0_2_0_4 = Theory.save_thm("bit_1_0_2_0_4", 318 blastLib.BBLAST_PROVE 319 ``(1 >< 0) (((2 >< 0) (a:word64)) : word3 ?? 4w) = 320 ((1 >< 0) a) : word2`` 321 ) 322 323val st = ``s:mips_state`` 324val addr = ``sw2sw (offset:word16) + if base = 0w then 0w else ^st.gpr base`` 325 326local 327 val tm_le = ``(2 >< 0) ^addr : word3`` 328 val pctm_le = ``(2 >< 0) ^st.PC : word3`` 329 fun select s tm thm = 330 Theory.save_thm(s, 331 (Drule.UNDISCH o 332 REWRITE_RULE 333 [wordsTheory.WORD_XOR_ASSOC, wordsTheory.WORD_XOR_CLAUSES, 334 bit_0_2_0, bit_0_2_0_6, bit_1_0_2_0, bit_1_0_2_0_4] o 335 Drule.SPECL [tm, ``^st.MEM``, ``a:word64``]) thm) 336in 337 val select_half_le = select "select_half_le" tm_le select_half_le 338 val select_half_be = select "select_half_be" ``^tm_le ?? 6w`` select_half_be 339 val select_pc_le = select "select_pc_le" pctm_le select_word_le 340 val select_pc_be = select "select_pc_be" ``^pctm_le ?? 4w`` select_word_be 341 val select_word_le = select "select_word_le" tm_le select_word_le 342 val select_word_be = select "select_word_be" ``^tm_le ?? 4w`` select_word_be 343end 344 345val address_align = Q.store_thm("address_align", 346 `!a:word64 b:word3. 347 ((((63 >< 3) a) : 61 word) @@ (b : word3)) && ~7w = a && ~7w`, 348 blastLib.BBLAST_TAC) 349 350val address_align2 = Q.store_thm("address_align2", 351 `!a:word64. (((63 >< 3) a) : 61 word) @@ ((2 >< 0) a : word3) = a`, 352 blastLib.BBLAST_TAC) 353 354val cond_sign_extend = Q.store_thm("cond_sign_extend", 355 `!a b. (if b then w2w a else sw2sw a) = (if b then w2w else sw2sw) a`, 356 rw []) 357 358val byte_address = Q.store_thm("byte_address", 359 `!a:word64. (a && ~7w) + w2w (((2 >< 0) a) : word3) = a`, 360 blastLib.BBLAST_TAC) 361 362val double_aligned = Theory.save_thm("double_aligned", 363 blastLib.BBLAST_PROVE 364 ``!a:word64. ((2 >< 0) a = 0w:word3) ==> (a && ~7w = a)`` 365 |> Thm.SPEC addr 366 |> Drule.UNDISCH 367 ) 368 369val Aligned_thms = Q.store_thm("Aligned_thms", 370 `(!w. Aligned (w, 1w) = aligned 1 w) /\ 371 (!w: word64. ~word_bit 0 w = aligned 1 w) /\ 372 (!w. Aligned (w, 3w) = aligned 2 w) /\ 373 (!w: word64. ((1 >< 0) w = 0w: word2) = aligned 2 w) /\ 374 (!w. Aligned (w, 7w) = aligned 3 w) /\ 375 (!w: word64. ((2 >< 0) w = 0w: word3) = aligned 3 w) 376 `, 377 rw [Aligned_def, alignmentTheory.aligned_bitwise_and] 378 \\ blastLib.BBLAST_TAC 379 ) 380 381(* ------------------------------------------------------------------------ *) 382 383(* ------ 384 Theorems of the form 385 |- !w b. ((7 + x) + 8 * w2n b >< x + 8 * w2n b) (w << (8 * w2n b)) = 386 (7 + x >< x) w 387 ------ *) 388local 389 fun try_undisch thm = Option.getOpt (Lib.total Drule.UNDISCH thm, thm) 390 val undisch_conjuncts = 391 List.map (try_undisch o Drule.SPEC_ALL) o Drule.CONJUNCTS 392 val tac = 393 REPEAT conj_tac 394 \\ wordsLib.Cases_word_value 395 \\ EVAL_TAC 396 val hlem = Q.prove( 397 `!b:word3. ~word_bit 0 b ==> 15 + 8 * w2n b < 64`, 398 tac 399 ) 400 val wlem = Q.prove( 401 `(!b:word3. ((1 >< 0) b = 0w: word2) ==> 15 + 8 * w2n b < 64) /\ 402 (!b:word3. ((1 >< 0) b = 0w: word2) ==> 23 + 8 * w2n b < 64) /\ 403 (!b:word3. ((1 >< 0) b = 0w: word2) ==> 31 + 8 * w2n b < 64)`, 404 tac 405 ) 406 val tm = ``8 * w2n (b:word3)`` 407 fun ebyte thm i = 408 let 409 val a = numSyntax.mk_plus (numLib.term_of_int i, tm) 410 val b = numSyntax.mk_plus (numLib.term_of_int (i + 7), tm) 411 in 412 wordsTheory.WORD_EXTRACT_LSL 413 |> Drule.ISPECL [b, a, tm, ``w:word64``] 414 |> SIMP_RULE (srw_ss()) [DECIDE ``a - (b + a) = 0n``] 415 |> REWRITE_RULE (undisch_conjuncts thm) 416 end 417in 418 val extract_byte = Theory.save_thm("extract_byte", 419 ebyte (wordsLib.WORD_DECIDE ``7 + 8 * w2n (b:word3) < 64``) 0) 420 val extract_half = Theory.save_thm("extract_half", 421 Drule.LIST_CONJ (List.map (ebyte hlem) [8])) 422 val extract_word = Theory.save_thm("extract_word", 423 Drule.LIST_CONJ (List.map (ebyte wlem) [8, 16, 24])) 424end 425 426(* ------------------------------------------------------------------------ *) 427 428val StoreMemory = 429 StoreMemory_def 430 |> Drule.SPEC_ALL 431 |> Conv.CONV_RULE (Conv.X_FUN_EQ_CONV st) 432 |> Thm.SPEC st 433 |> Conv.RIGHT_CONV_RULE PairedLambda.GEN_BETA_CONV 434 435val ls_thm = 436 wordsLib.WORD_DECIDE ``!a b:'a word. a <=+ b /\ b <=+ a = (a = b)`` 437 438val ls_lem = 439 blastLib.BBLAST_PROVE 440 ``((2 >< 0) (a: word64) = (b: word3)) /\ (w2w b = c) ==> 441 ((0xFFFFFFFFFFFFFFF8w && a) + c = a)`` 442 443val ls_lem0 = 444 SIMP_RULE (srw_ss()) [] (Q.INST [`b` |-> `0w`, `c` |-> `0w`] ls_lem) 445 446val ls_lem1 = 447 blastLib.BBLAST_PROVE 448 ``((2 >< 0) (a: word64) = (b: word3)) /\ (w2w b + 1w = c) ==> 449 ((0xFFFFFFFFFFFFFFF8w && a) + c = a + 1w)`` 450 451val ls_lem2 = 452 blastLib.BBLAST_PROVE 453 ``((2 >< 0) (a: word64) = (b: word3)) /\ (w2w b + 2w = c) ==> 454 ((0xFFFFFFFFFFFFFFF8w && a) + c = a + 2w)`` 455 456val ls_lem3 = 457 blastLib.BBLAST_PROVE 458 ``((2 >< 0) (a: word64) = (b: word3)) /\ (w2w b + 3w = c) ==> 459 ((0xFFFFFFFFFFFFFFF8w && a) + c = a + 3w)`` 460 461val ls_lem4 = 462 blastLib.BBLAST_PROVE 463 ``0xFFFFFFFFFFFFFFF8w && (a ?? w2w (b : word3)) = 464 0xFFFFFFFFFFFFFFF8w && a : word64`` 465 466val StoreMemory_byte = Q.store_thm("StoreMemory_byte", 467 `!s MemElem vAddr. 468 ~s.exceptionSignalled ==> 469 (StoreMemory (0w,0w,F,MemElem,vAddr,F) s = 470 (T, s with 471 <|LLbit := NONE; 472 MEM := 473 let a = (2 >< 0) vAddr: word3 in 474 let b = if BigEndianMem s then a ?? 7w else a in 475 let c = 8 * w2n b in 476 (vAddr =+ (7 + c >< c) MemElem) s.MEM|>))`, 477 rpt strip_tac 478 \\ asm_simp_tac (srw_ss()) 479 [StoreMemory, AddressTranslation_def, AdjustEndian_def, WriteData_def, 480 ls_lem, ls_thm, ls_lem4, wordsTheory.w2w_0, wordsTheory.WORD_ADD_0] 481 \\ wordsLib.Cases_on_word_value `(2 >< 0) vAddr: word3` 482 \\ lrw [ls_lem, ls_lem0, ls_lem4] 483 ) 484 485val ls_thm2 = 486 blastLib.BBLAST_PROVE 487 ``~word_bit 0 (a:word3) ==> 488 (a <=+ b /\ b <=+ a + 1w = (a = b) \/ (a + 1w = b))`` 489 490val StoreMemory_half = Q.store_thm("StoreMemory_half", 491 `Aligned (vAddr,1w) ==> ~s.exceptionSignalled ==> 492 (StoreMemory (1w,1w,T,MemElem,vAddr,F) s = 493 (T, 494 s with 495 <|LLbit := NONE; 496 MEM := 497 let a = (2 >< 0) vAddr: word3 in 498 if BigEndianMem s then 499 let b = 8 * w2n (a ?? 6w) in 500 (vAddr + 1w =+ (7 + b >< b) MemElem) 501 ((vAddr =+ (15 + b >< 8 + b) MemElem) s.MEM) 502 else 503 let b = 8 * w2n a in 504 (vAddr + 1w =+ (15 + b >< 8 + b) MemElem) 505 ((vAddr =+ (7 + b >< b) MemElem) s.MEM)|>))`, 506 rpt strip_tac 507 \\ asm_simp_tac (srw_ss()) 508 [StoreMemory, AddressTranslation_def, AdjustEndian_def, WriteData_def, 509 ls_thm2] 510 \\ `~word_bit 0 (((2 >< 0) vAddr) : word3)` 511 by (fs [Aligned_def] \\ blastLib.FULL_BBLAST_TAC) 512 \\ wordsLib.Cases_on_word_value `(2 >< 0) vAddr: word3` 513 \\ fs [ls_lem, ls_lem0, ls_lem1, ls_lem4] 514 \\ asm_simp_tac (srw_ss()) [] 515 \\ lrw [] 516 ) 517 518val ls_thm3 = 519 blastLib.BBLAST_PROVE 520 ``((1 >< 0) (a:word3) = 0w:word2) ==> 521 (a <=+ b /\ b <=+ a + 3w = 522 (a = b) \/ (a + 1w = b) \/ (a + 2w = b) \/ (a + 3w = b))`` 523 524val StoreMemory_word = Q.store_thm("StoreMemory_word", 525 `Aligned (vAddr,3w) ==> ~s.exceptionSignalled ==> 526 (StoreMemory (3w,3w,T,MemElem,vAddr,F) s = 527 (T, 528 s with 529 <|LLbit := NONE; 530 MEM := 531 let a = (2 >< 0) vAddr: word3 in 532 if BigEndianMem s then 533 let b = 8 * w2n (a ?? 4w) in 534 (vAddr + 3w =+ (7 + b >< b) MemElem) 535 ((vAddr + 2w =+ (15 + b >< 8 + b) MemElem) 536 ((vAddr + 1w =+ (23 + b >< 16 + b) MemElem) 537 ((vAddr =+ (31 + b >< 24 + b) MemElem) s.MEM))) 538 else 539 let b = 8 * w2n a in 540 (vAddr + 3w =+ (31 + b >< 24 + b) MemElem) 541 ((vAddr + 2w =+ (23 + b >< 16 + b) MemElem) 542 ((vAddr + 1w =+ (15 + b >< 8 + b) MemElem) 543 ((vAddr =+ (7 + b >< b) MemElem) s.MEM)))|>))`, 544 rpt strip_tac 545 \\ `(1 >< 0) (((2 >< 0) vAddr) : word3) = 0w: word2` 546 by (fs [Aligned_def] \\ blastLib.FULL_BBLAST_TAC) 547 \\ asm_simp_tac (srw_ss()) 548 [StoreMemory, AddressTranslation_def, AdjustEndian_def, WriteData_def, 549 ls_thm3] 550 \\ wordsLib.Cases_on_word_value `(2 >< 0) vAddr: word3` 551 \\ fs [ls_lem, ls_lem0, ls_lem1, ls_lem2, ls_lem3, ls_lem4] 552 \\ asm_simp_tac (srw_ss()) [] 553 \\ lrw [] 554 ) 555 556val ls_thm4 = 557 blastLib.BBLAST_PROVE 558 ``((a:word3) = 0w:word3) ==> (a <=+ b /\ b <=+ a + 7w)`` 559 560val StoreMemory_doubleword = Q.store_thm("StoreMemory_doubleword", 561 `Aligned (vAddr,7w) ==> ~s.exceptionSignalled ==> 562 (StoreMemory (7w,7w,T,MemElem,vAddr,F) s = 563 (T, 564 s with 565 <|LLbit := NONE; 566 MEM := 567 if BigEndianMem s then 568 (vAddr + 7w =+ (7 >< 0) MemElem) 569 ((vAddr + 6w =+ (15 >< 8) MemElem) 570 ((vAddr + 5w =+ (23 >< 16) MemElem) 571 ((vAddr + 4w =+ (31 >< 24) MemElem) 572 ((vAddr + 3w =+ (39 >< 32) MemElem) 573 ((vAddr + 2w =+ (47 >< 40) MemElem) 574 ((vAddr + 1w =+ (55 >< 48) MemElem) 575 ((vAddr =+ (63 >< 56) MemElem) s.MEM))))))) 576 else 577 (vAddr + 7w =+ (63 >< 56) MemElem) 578 ((vAddr + 6w =+ (55 >< 48) MemElem) 579 ((vAddr + 5w =+ (47 >< 40) MemElem) 580 ((vAddr + 4w =+ (39 >< 32) MemElem) 581 ((vAddr + 3w =+ (31 >< 24) MemElem) 582 ((vAddr + 2w =+ (23 >< 16) MemElem) 583 ((vAddr + 1w =+ (15 >< 8) MemElem) 584 ((vAddr =+ (7 >< 0) MemElem) s.MEM)))))))|>))`, 585 rpt strip_tac 586 \\ `(2 >< 0) vAddr = 0w: word3` 587 by (fs [Aligned_def] \\ blastLib.FULL_BBLAST_TAC) 588 \\ asm_simp_tac (srw_ss()) 589 [StoreMemory, AddressTranslation_def, AdjustEndian_def, WriteData_def, 590 ls_thm4] 591 \\ lrw [ls_lem, ls_lem0, ls_lem1, ls_lem2, ls_lem3, ls_lem4] 592 ) 593 594(* ------------------------------------------------------------------------ *) 595 596val cond_update_memory = Q.store_thm("cond_update_memory", 597 `(!a: word64 b x0 x1 x2 x3 m. 598 (if b then 599 (a + 3w =+ x0) ((a + 2w =+ x1) ((a + 1w =+ x2) ((a =+ x3) m))) 600 else m) = 601 (a + 3w =+ (if b then x0 else m (a + 3w))) 602 ((a + 2w =+ (if b then x1 else m (a + 2w))) 603 ((a + 1w =+ (if b then x2 else m (a + 1w))) 604 ((a =+ (if b then x3 else m a)) m)))) /\ 605 (!a: word64 b x0 x1 x2 x3 x4 x5 x6 x7 m. 606 (if b then 607 (a + 7w =+ x0) ((a + 6w =+ x1) ((a + 5w =+ x2) ((a + 4w =+ x3) 608 ((a + 3w =+ x4) ((a + 2w =+ x5) ((a + 1w =+ x6) ((a =+ x7) m))))))) 609 else m) = 610 (a + 7w =+ (if b then x0 else m (a + 7w))) 611 ((a + 6w =+ (if b then x1 else m (a + 6w))) 612 ((a + 5w =+ (if b then x2 else m (a + 5w))) 613 ((a + 4w =+ (if b then x3 else m (a + 4w))) 614 ((a + 3w =+ (if b then x4 else m (a + 3w))) 615 ((a + 2w =+ (if b then x5 else m (a + 2w))) 616 ((a + 1w =+ (if b then x6 else m (a + 1w))) 617 ((a =+ (if b then x7 else m a)) m))))))))`, 618 rw [combinTheory.UPDATE_def, FUN_EQ_THM] 619 ) 620 621(* ------------------------------------------------------------------------ *) 622 623val branch_delay = Q.store_thm("branch_delay", 624 `(!b x y. 625 (case (if b then (F, x) else (T, y)) of 626 (T, a) => SOME NONE 627 | (F, a) => SOME (SOME a)) = 628 (if b then SOME (SOME x) else SOME NONE)) /\ 629 (!b x y. 630 (case (if b then (F, x) else (T, y)) of 631 (T, a) => a 632 | (F, a) => y) = y) /\ 633 (!b x y. 634 (if b then 635 (case THE (if b then SOME (F, x) else NONE) of 636 (T, a) => SOME NONE 637 | (F, a) => SOME (SOME a)) 638 else 639 NONE) = 640 (if b then SOME (SOME x) else NONE)) /\ 641 (!b x y. 642 (if b then 643 (case THE (if b then SOME (F, x) else NONE) of 644 (T, a) => a 645 | (F, a) => y) 646 else 647 y) = y) /\ 648 (!b. (if b then T else F) = b) /\ 649 (!b x y. 650 (if b then x else y) + 4w = (if b then x + 4w else y + 4w)) /\ 651 (!x. x + 4w + 4w = x + 8w)`, 652 rw [] \\ fs []) 653 654(* ------------------------------------------------------------------------ *) 655 656val cond_word1 = Q.store_thm("cond_word1", 657 `(if w = 0w : word1 then a else if w = 1w then b else c) = 658 (if w = 0w then a else b)`, 659 wordsLib.Cases_on_word_value `w` \\ simp []) 660 661val cond_word2 = Q.store_thm("cond_word2", 662 `(if w = 0w : word2 then a 663 else if w = 1w then b 664 else if w = 2w then c 665 else if w = 3w then d else e) = 666 (if w = 0w then a 667 else if w = 1w then b 668 else if w = 2w then c 669 else d)`, 670 wordsLib.Cases_on_word_value `w` \\ simp []) 671 672val cond_word3 = Q.store_thm("cond_word3", 673 `(if w = 0w : word3 then a 674 else if w = 1w then b 675 else if w = 2w then c 676 else if w = 3w then d 677 else if w = 4w then e 678 else if w = 5w then f 679 else if w = 6w then g 680 else if w = 7w then h else i) = 681 (if w = 0w then a 682 else if w = 1w then b 683 else if w = 2w then c 684 else if w = 3w then d 685 else if w = 4w then e 686 else if w = 5w then f 687 else if w = 6w then g 688 else h)`, 689 wordsLib.Cases_on_word_value `w` \\ simp []) 690 691val () = export_theory () 692