1(* ------------------------------------------------------------------------ 2 Definitions and theorems used by ARM step evaluator (arm_stepLib) 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6 7open utilsLib 8open wordsLib blastLib 9open state_transformerTheory updateTheory alignmentTheory armTheory 10 11val _ = new_theory "arm_step" 12val _ = ParseExtras.temp_loose_equality() 13(* ------------------------------------------------------------------------ *) 14 15val _ = List.app (fn f => f ()) 16 [numLib.prefer_num, wordsLib.prefer_word, wordsLib.guess_lengths] 17 18(* ------------------------------------------------------------------------ *) 19 20val NextStateARM_def = Define` 21 NextStateARM s0 = 22 let s1 = Next s0 in if s1.exception = NoException then SOME s1 else NONE` 23 24val NextStateARM_arm = ustore_thm("NextStateARM_arm", 25 `(s.exception = NoException) ==> 26 (Fetch s = (ARM (v2w v), s with Encoding := Encoding_ARM)) /\ 27 (DecodeARM (v2w v) (s with Encoding := Encoding_ARM) = 28 (ast, s with <| CurrentCondition := c; 29 Encoding := Encoding_ARM; 30 undefined := F |>)) /\ 31 (!s. Run ast s = f x s) /\ 32 (f x (s with <| CurrentCondition := c; 33 Encoding := Encoding_ARM; 34 undefined := F |>) = s1) /\ 35 (s1.Encoding = Encoding_ARM) /\ 36 (s1.exception = s.exception) ==> 37 (NextStateARM s = SOME s1)`, 38 lrw [NextStateARM_def, Next_def, Decode_def, ITAdvance_def] 39 ) 40 41val NextStateARM_arm0 = ustore_thm("NextStateARM_arm0", 42 `(s.exception = NoException) ==> 43 (Fetch s = (ARM (v2w v), s with Encoding := Encoding_ARM)) /\ 44 (DecodeARM (v2w v) (s with Encoding := Encoding_ARM) = 45 (ast, s with <| CurrentCondition := c; 46 Encoding := Encoding_ARM; 47 undefined := F |>)) /\ 48 (!s. Run ast s = f s) /\ 49 (f (s with <| CurrentCondition := c; 50 Encoding := Encoding_ARM; 51 undefined := F |>) = s1) /\ 52 (s1.Encoding = Encoding_ARM) /\ 53 (s1.exception = s.exception) ==> 54 (NextStateARM s = SOME s1)`, 55 lrw [NextStateARM_def, Next_def, Decode_def, ITAdvance_def] 56 ) 57 58val NextStateARM_thumb = ustore_thm("NextStateARM_thumb", 59 `(s.exception = NoException) ==> 60 (Fetch s = (Thumb (v2w v), s with Encoding := Encoding_Thumb)) /\ 61 (DecodeThumb (v2w v) (s with Encoding := Encoding_Thumb) = 62 (ast, s with <| CurrentCondition := c; 63 Encoding := Encoding_Thumb; 64 undefined := F |>)) /\ 65 (!s. Run ast s = f x s) /\ 66 (f x (s with <| CurrentCondition := c; 67 Encoding := Encoding_Thumb; 68 undefined := F |>) = s1) /\ 69 (ITAdvance () s1 = s2) /\ 70 (s2.exception = s.exception) ==> 71 (NextStateARM s = SOME s2)`, 72 lrw [NextStateARM_def, Next_def, Decode_def] 73 ) 74 75(* ------------------------------------------------------------------------ *) 76 77val LDM1_def = Define` 78 LDM1 (f: word4 -> RName) b (registers: word16) s r j = 79 (if word_bit j registers then 80 f (n2w j) =+ 81 let a = b + if j = 0 then 0w else 4w * n2w (bit_count_upto j registers) 82 in 83 if s.CPSR.E then 84 s.MEM a @@ s.MEM (a + 1w) @@ s.MEM (a + 2w) @@ s.MEM (a + 3w) 85 else 86 s.MEM (a + 3w) @@ s.MEM (a + 2w) @@ s.MEM (a + 1w) @@ s.MEM a 87 else 88 I) r` 89 90val LDM_UPTO_def = Define` 91 LDM_UPTO f i (registers: word16) (b: word32, s) = 92 (b + 4w * n2w (bit_count_upto (i + 1) registers), 93 s with REG := FOLDL (LDM1 f b registers s) s.REG (COUNT_LIST (i + 1)))` 94 95val STM1_def = Define` 96 STM1 f (b: word32) (registers: word16) s m j = 97 (if word_bit j registers then 98 let a = b + if j = 0 then 0w else 4w * n2w (bit_count_upto j registers) 99 and r = s.REG (f (n2w j: word4)) 100 in 101 (a + 3w =+ if s.CPSR.E then (7 >< 0) r else (31 >< 24) r) o 102 (a + 2w =+ if s.CPSR.E then (15 >< 8) r else (23 >< 16) r) o 103 (a + 1w =+ if s.CPSR.E then (23 >< 16) r else (15 >< 8) r) o 104 (a =+ if s.CPSR.E then (31 >< 24) r else (7 >< 0) r) 105 else 106 I) m` 107 108val STM_UPTO_def = Define` 109 STM_UPTO f i (registers: word16) (b: word32, s) = 110 (b + 4w * n2w (bit_count_upto (i + 1) registers), 111 s with MEM := FOLDL (STM1 f b registers s) s.MEM (COUNT_LIST (i + 1)))` 112 113(* ------------------------------------------------------------------------ *) 114 115val DecodeRoundingMode_def = Define` 116 DecodeRoundingMode (m: word2) = 117 if m = 0w 118 then roundTiesToEven 119 else if m = 1w 120 then roundTowardPositive 121 else if m = 2w 122 then roundTowardNegative 123 else roundTowardZero`; 124 125(* For floating-point single precision access *) 126 127val SingleOfDouble_def = Define` 128 SingleOfDouble b (w:word64) = if b then (63 >< 32) w else (31 >< 0) w` 129 130val UpdateSingleOfDouble_def = Define` 131 UpdateSingleOfDouble b (v:word32) (w:word64) = 132 if b then 133 bit_field_insert 63 32 v w 134 else 135 bit_field_insert 31 0 v w`; 136 137(* ------------------------------------------------------------------------ *) 138 139val reverse_endian_def = Define` 140 reverse_endian (w: word32) = 141 (7 >< 0) w @@ (15 >< 8) w @@ (23 >< 16) w @@ (31 >< 24) w` 142 143(* ------------------------------------------------------------------------ *) 144 145val GoodMode_def = Define` 146 GoodMode (m: word5) = m IN {16w;17w;18w;19w;23w;27w;31w}` 147 148val R_mode_def = Define` 149 R_mode (m: word5) (n: word4) = 150 case m, n of 151 _, 0w => RName_0usr 152 | _, 1w => RName_1usr 153 | _, 2w => RName_2usr 154 | _, 3w => RName_3usr 155 | _, 4w => RName_4usr 156 | _, 5w => RName_5usr 157 | _, 6w => RName_6usr 158 | _, 7w => RName_7usr 159 | 17w, 8w => RName_8fiq 160 | _, 8w => RName_8usr 161 | 17w, 9w => RName_9fiq 162 | _, 9w => RName_9usr 163 | 17w, 10w => RName_10fiq 164 | _, 10w => RName_10usr 165 | 17w, 11w => RName_11fiq 166 | _, 11w => RName_11usr 167 | 17w, 12w => RName_12fiq 168 | _, 12w => RName_12usr 169 | 17w, 13w => RName_SPfiq 170 | 18w, 13w => RName_SPirq 171 | 19w, 13w => RName_SPsvc 172 | 22w, 13w => RName_SPmon 173 | 23w, 13w => RName_SPabt 174 | 26w, 13w => RName_SPhyp 175 | 27w, 13w => RName_SPund 176 | _, 13w => RName_SPusr 177 | 17w, 14w => RName_LRfiq 178 | 18w, 14w => RName_LRirq 179 | 19w, 14w => RName_LRsvc 180 | 22w, 14w => RName_LRmon 181 | 23w, 14w => RName_LRabt 182 | 27w, 14w => RName_LRund 183 | _, 14w => RName_LRusr 184 | _ => RName_PC` 185 186(* ------------------------------------------------------------------------ *) 187 188val R_mode = Q.store_thm("R_mode", 189 `(!m. R_mode m 0w = RName_0usr) /\ 190 (!m. R_mode m 1w = RName_1usr) /\ 191 (!m. R_mode m 2w = RName_2usr) /\ 192 (!m. R_mode m 3w = RName_3usr) /\ 193 (!m. R_mode m 4w = RName_4usr) /\ 194 (!m. R_mode m 5w = RName_5usr) /\ 195 (!m. R_mode m 6w = RName_6usr) /\ 196 (!m. R_mode m 7w = RName_7usr) /\ 197 (!m. R_mode m 15w = RName_PC)`, 198 simp [R_mode_def] 199 ) 200 201val R_x_not_pc = Q.prove( 202 `!d mode. d <> 15w ==> (R_mode mode d <> RName_PC)`, 203 wordsLib.Cases_word_value \\ simp [R_mode_def] \\ rw []) 204 |> Drule.SPEC_ALL 205 |> usave_as "R_x_not_pc" 206 207val R_x_pc = Q.store_thm("R_x_pc", 208 `!mode x. (R_mode mode x = RName_PC) = (x = 15w)`, 209 REPEAT strip_tac 210 \\ Cases_on `x = 15w` 211 \\ asm_simp_tac (srw_ss()) [R_mode_def, DISCH_ALL R_x_not_pc] 212 ) 213 214val BadMode = Q.prove( 215 `!mode s. GoodMode mode ==> (BadMode mode s = F)`, 216 rw [BadMode_def, GoodMode_def]) 217 |> Drule.SPEC_ALL 218 |> usave_as "BadMode" 219 220val NotMon = Q.prove( 221 `!mode. GoodMode mode ==> mode <> 22w`, 222 rw [GoodMode_def] \\ rw []) 223 |> Drule.SPEC_ALL 224 |> usave_as "NotMon" 225 226val NotHyp = Q.prove( 227 `!mode. GoodMode mode ==> mode <> 26w`, 228 rw [GoodMode_def] \\ rw []) 229 |> Drule.SPEC_ALL 230 |> usave_as "NotHyp" 231 232val R_mode_11 = Q.store_thm("R_mode_11", 233 `!r1 r2 m. (R_mode m r1 = R_mode m r2) = (r1 = r2)`, 234 wordsLib.Cases_word_value 235 \\ simp [R_mode_def] 236 \\ wordsLib.Cases_word_value 237 \\ simp [R_mode_def] 238 \\ rw [] 239 ) 240 241val IsSecure = Q.prove( 242 `!s. ~s.Extensions Extension_Security ==> (IsSecure () s = T)`, 243 rw [IsSecure_def, HaveSecurityExt_def, pred_setTheory.SPECIFICATION]) 244 |> Drule.SPEC_ALL 245 |> usave_as "IsSecure" 246 247val CurrentModeIsHyp = Q.prove( 248 `!mode s. GoodMode s.CPSR.M ==> (CurrentModeIsHyp () s = (F, s))`, 249 simp [CurrentModeIsHyp_def, DISCH_ALL BadMode, DISCH_ALL NotHyp]) 250 |> Drule.SPEC_ALL 251 |> usave_as "CurrentModeIsHyp" 252 253(* ------------------------------------------------------------------------ *) 254 255val ITAdvance_0 = ustore_thm("ITAdvance_0", 256 `(s.CPSR.IT = 0w) ==> (s with CPSR := s.CPSR with IT := 0w = s)`, 257 lrw [armTheory.arm_state_component_equality, 258 armTheory.PSR_component_equality] 259 ) 260 261(* ------------------------------------------------------------------------ *) 262 263val RoundingMode = Q.store_thm("RoundingMode", 264 `!s. RoundingMode s = DecodeRoundingMode s.FP.FPSCR.RMode`, 265 rw [DecodeRoundingMode_def, RoundingMode_def] 266 \\ blastLib.FULL_BBLAST_TAC 267 ) 268 269(* ------------------------------------------------------------------------ *) 270 271val notoverflow = METIS_PROVE [integer_wordTheory.overflow] 272 ``!x y. (word_msb x = word_msb (x + y)) ==> (w2i (x + y) = w2i x + w2i y)`` 273 274val word_msb_sum1a = Q.prove( 275 `!x y. (word_msb x = word_msb y) /\ word_msb (x + y) ==> 276 word_msb (x + y + 1w)`, 277 Cases \\ Cases 278 \\ lrw [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 279 \\ Cases_on `INT_MIN (:'a) <= n` 280 \\ Cases_on `INT_MIN (:'a) <= n'` 281 \\ lfs [] 282 >- (imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 283 \\ pop_assum (K all_tac) 284 \\ `p < INT_MIN (:'a) /\ p' < INT_MIN (:'a)` 285 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 286 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 287 \\ `(p + (p' + (dimword (:'a) + 1)) = dimword (:'a) + (p + p' + 1)) /\ 288 (p + (p' + dimword (:'a)) = dimword (:'a) + (p + p'))` by lrw [] 289 \\ pop_assum SUBST_ALL_TAC \\ pop_assum SUBST1_TAC 290 \\ full_simp_tac bool_ss 291 [arithmeticTheory.ADD_MODULUS_RIGHT, wordsTheory.ZERO_LT_dimword] 292 \\ `p + p' + 1 < dimword (:'a)` 293 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 294 \\ lfs []) 295 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 296 \\ `n + n' + 1 < dimword (:'a)` 297 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 298 \\ lfs [] 299 ) 300 301val word_msb_sum1b = Q.prove( 302 `!x y. (word_msb x <> word_msb y) /\ ~word_msb (x + y) ==> 303 (word_msb (x + y) = word_msb (x + y + 1w))`, 304 Cases \\ Cases 305 \\ simp_tac std_ss 306 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 307 \\ lrw [] 308 \\ Cases_on `n < INT_MIN (:'a)` 309 \\ Cases_on `n' < INT_MIN (:'a)` 310 \\ lfs [arithmeticTheory.NOT_LESS, arithmeticTheory.NOT_LESS_EQUAL] 311 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 312 \\ lfs [arithmeticTheory.NOT_LESS] 313 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 314 \\ pop_assum (K all_tac) 315 \\ `p < INT_MIN (:'a)` by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 316 \\ lrw [arithmeticTheory.ADD_MODULUS_LEFT] 317 ) 318 319val word_msb_sum1c = Q.prove( 320 `!x y. word_msb (x + y + 1w) /\ ~word_msb (x + y) ==> (x + y = INT_MAXw)`, 321 Cases \\ Cases 322 \\ `INT_MIN (:'a) - 1 < dimword (:'a)` 323 by (assume_tac wordsTheory.INT_MIN_LT_DIMWORD \\ decide_tac) 324 \\ simp_tac std_ss 325 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_H_def, 326 wordsTheory.INT_MAX_def, wordsTheory.word_add_n2w] 327 \\ lrw [] 328 \\ lfs [arithmeticTheory.NOT_LESS_EQUAL] 329 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 330 \\ lfs [arithmeticTheory.NOT_LESS] 331 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 332 \\ pop_assum (K all_tac) 333 \\ `p < dimword (:'a)` by lfs [] 334 \\ Cases_on `n + n' < dimword (:'a)` 335 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT, arithmeticTheory.NOT_LESS] 336 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 337 \\ pop_assum (K all_tac) 338 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT] 339 ) 340 341val AddWithCarry = Q.store_thm("AddWithCarry", 342 `!x y carry_in. AddWithCarry (x,y,carry_in) = add_with_carry (x,y,carry_in)`, 343 REPEAT strip_tac 344 \\ simp [AddWithCarry_def, wordsTheory.add_with_carry_def] 345 \\ simp [GSYM wordsTheory.word_add_n2w] 346 \\ Cases_on `carry_in` 347 \\ simp [integer_wordTheory.overflow] 348 \\ Cases_on `dimindex(:'a) = 1` 349 >- (imp_res_tac wordsTheory.dimindex_1_cases 350 \\ pop_assum (fn th => (strip_assume_tac (Q.SPEC `x` th) 351 \\ strip_assume_tac (Q.SPEC `y` th))) 352 \\ simp [wordsTheory.word_index, wordsTheory.word_msb_def, 353 wordsTheory.word_2comp_def, integer_wordTheory.w2i_def, 354 wordsTheory.dimword_def]) 355 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)` 356 \\ `~word_msb 1w` 357 by lrw [wordsTheory.word_msb_n2w, DECIDE ``0n < n /\ n <> 1 ==> ~(n <= 1)``] 358 \\ fs [integer_wordTheory.different_sign_then_no_overflow, 359 integer_wordTheory.overflow, integer_wordTheory.w2i_1] 360 >- (Cases_on `word_msb x <=> word_msb y` \\ simp [word_msb_sum1a]) 361 \\ Cases_on `word_msb x = word_msb y` 362 \\ simp [GSYM integer_wordTheory.different_sign_then_no_overflow] 363 >- (Cases_on `word_msb (x + y + 1w)` 364 \\ lfs [notoverflow, integer_wordTheory.w2i_1] 365 >- (imp_res_tac word_msb_sum1c 366 \\ lfs [integer_wordTheory.w2i_INT_MINw] 367 \\ Cases_on `x` 368 \\ Cases_on `y` 369 \\ lfs [wordsTheory.word_msb_n2w_numeric] 370 \\ Cases_on `INT_MIN (:'a) <= n'` 371 \\ lfs [integer_wordTheory.w2i_n2w_pos, 372 integer_wordTheory.w2i_n2w_neg, 373 wordsTheory.word_add_n2w, 374 wordsTheory.word_L_def, 375 wordsTheory.word_2comp_def, 376 integerTheory.INT_ADD_CALCULATE] 377 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 378 \\ `p + p' < dimword (:'a)` 379 by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 380 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 381 \\ `(p + (p' + dimword (:'a)) = (p + p') + dimword (:'a)) /\ 382 (INT_MIN (:'a) + dimword (:'a) - 1 = 383 dimword (:'a) + (INT_MIN (:'a) - 1))` 384 by lfs [] 385 \\ ntac 2 (pop_assum SUBST_ALL_TAC) 386 \\ full_simp_tac bool_ss 387 [arithmeticTheory.ADD_MODULUS_LEFT, 388 arithmeticTheory.ADD_MODULUS_RIGHT, 389 wordsTheory.ZERO_LT_dimword] 390 \\ lfs [wordsTheory.BOUND_ORDER] 391 \\ metis_tac [arithmeticTheory.ADD_ASSOC, 392 wordsTheory.dimword_sub_int_min, 393 wordsTheory.ZERO_LT_INT_MIN, 394 DECIDE ``0n < n ==> (n - 1 + 1 = n)``]) 395 \\ metis_tac [integer_wordTheory.overflow, integer_wordTheory.w2i_1]) 396 \\ `word_msb (x + y) <=> word_msb (x + y + 1w)` by imp_res_tac word_msb_sum1b 397 \\ simp [notoverflow, integer_wordTheory.w2i_1] 398 ) 399 400(* ------------------------------------------------------------------------ *) 401 402val CountLeadingZeroBits16 = Q.store_thm("CountLeadingZeroBits16", 403 `!w:word16. 404 CountLeadingZeroBits w = if w = 0w then 16 else 15 - w2n (word_log2 w)`, 405 lrw [CountLeadingZeroBits_def, HighestSetBit_def] 406 \\ `LOG2 (w2n w) < 16` 407 by metis_tac [wordsTheory.LOG2_w2n_lt, EVAL ``dimindex(:16)``] 408 \\ lrw [integer_wordTheory.w2i_def, wordsTheory.word_log2_def, 409 wordsTheory.word_msb_n2w_numeric, 410 intLib.ARITH_PROVE ``j < 16 ==> (Num (15 - &j) = 15 - j)``] 411 ) 412 413val CountLeadingZeroBits32 = Q.store_thm("CountLeadingZeroBits32", 414 `!w:word32. 415 CountLeadingZeroBits w = if w = 0w then 32 else 31 - w2n (word_log2 w)`, 416 lrw [CountLeadingZeroBits_def, HighestSetBit_def] 417 \\ `LOG2 (w2n w) < 32` 418 by metis_tac [wordsTheory.LOG2_w2n_lt, EVAL ``dimindex(:32)``] 419 \\ lrw [integer_wordTheory.w2i_def, wordsTheory.word_log2_def, 420 wordsTheory.word_msb_n2w_numeric, 421 intLib.ARITH_PROVE ``j < 32 ==> (Num (31 - &j) = 31 - j)``] 422 ) 423 424val FOLDL_AUG = Q.prove( 425 `!f a l. 426 FOLDL (\x i. f x i) a l = 427 FST (FOLDL (\y i. (f (FST y) i, ())) (a, ()) l)`, 428 Induct_on `l` \\ lrw [] 429 ) 430 431val FOLDL_cong = Q.store_thm("FOLDL_cong", 432 `!l r f g a b. 433 (LENGTH l = LENGTH r) /\ (a = b) /\ 434 (!i x. i < LENGTH l ==> (f x (EL i l) = g x (EL i r))) ==> 435 (FOLDL f a l = FOLDL g b r)`, 436 Induct \\ lrw [] 437 \\ Cases_on `r` \\ lfs [] 438 \\ metis_tac [prim_recTheory.LESS_0, listTheory.EL, listTheory.HD, 439 listTheory.EL_restricted, arithmeticTheory.LESS_MONO_EQ] 440 ) 441 442val FOR_BASE = Q.store_thm("FOR_BASE", 443 `!f s. FOR (n, n, f) s = f n s`, 444 simp [Once state_transformerTheory.FOR_def]) 445 446val FOR_FOLDL = Q.store_thm("FOR_FOLDL", 447 `!i j f s. 448 i <= j ==> 449 (FOR (i, j, f) s = 450 ((), FOLDL (\x n. SND (f (n + i) x)) s (COUNT_LIST (j - i + 1))))`, 451 ntac 2 strip_tac \\ Induct_on `j - i` 452 \\ lrw [Once state_transformerTheory.FOR_def, pairTheory.UNCURRY, 453 state_transformerTheory.BIND_DEF] 454 >- (`i = j` by decide_tac 455 \\ simp [] 456 \\ EVAL_TAC 457 \\ Cases_on `f j s` 458 \\ simp [oneTheory.one]) 459 \\ `v = j - (i + 1)` by decide_tac 460 \\ qpat_assum `!j i. P` (qspecl_then [`j`, `i + 1`] imp_res_tac) 461 \\ Cases_on `i + 1 < j` 462 >- (`j + 1 - i = SUC (j - i)` by decide_tac 463 \\ lrw [rich_listTheory.COUNT_LIST_def] 464 \\ match_mp_tac FOLDL_cong 465 \\ lrw [rich_listTheory.COUNT_LIST_GENLIST, listTheory.MAP_GENLIST, 466 arithmeticTheory.ADD1]) 467 \\ `j = i + 1` by decide_tac 468 \\ simp [] 469 \\ EVAL_TAC 470 ) 471 472val BitCount = Q.store_thm("BitCount", 473 `!w. BitCount w = bit_count w`, 474 lrw [BitCount_def, wordsTheory.bit_count_def, wordsTheory.bit_count_upto_def, 475 wordsTheory.word_bit_def] 476 \\ `0 <= dimindex(:'a) - 1` by lrw [] 477 \\ simp 478 [FOR_FOLDL 479 |> Q.ISPECL [`0n`, `dimindex(:'a) - 1`, 480 `\i state: num # unit. 481 ((), 482 if i <= dimindex(:'a) - 1 /\ w ' i then 483 (FST state + 1, ()) 484 else 485 state)`], 486 sum_numTheory.SUM_FOLDL] 487 \\ REWRITE_TAC 488 [FOLDL_AUG 489 |> Q.ISPECL 490 [`\x:num i. x + if w ' i then 1 else 0`, `0`, 491 `COUNT_LIST (dimindex ((:'a) :'a itself))`] 492 |> SIMP_RULE (srw_ss())[]] 493 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (FST x = FST y)``) 494 \\ MATCH_MP_TAC listTheory.FOLDL_CONG 495 \\ lrw [rich_listTheory.MEM_COUNT_LIST, 496 DECIDE ``0n < n ==> (n - 1 + 1 = n)``] 497 \\ Cases_on `a` 498 \\ simp [] 499 ) 500 501val bit_count_upto_1 = Q.prove( 502 `!registers: word16. 503 4w * n2w (bit_count_upto 1 registers) = 504 if word_bit 0 registers then 4w else 0w: word32`, 505 EVAL_TAC \\ lrw [wordsTheory.word_bit_def] 506 ) 507 508val bit_count_sub = Q.prove( 509 `!r: 'a word. 510 n2w (bit_count_upto (dimindex(:'a) - 1) r) - n2w (bit_count r) = 511 if r ' (dimindex(:'a) - 1) then -1w else 0w`, 512 REPEAT strip_tac 513 \\ simp [wordsTheory.bit_count_def] 514 \\ Cases_on `dimindex(:'a)` 515 >- lfs [DECIDE ``0 < n ==> (n <> 0n)``] 516 \\ simp [arithmeticTheory.SUC_SUB1, GSYM wordsTheory.word_add_n2w, 517 wordsTheory.WORD_LEFT_ADD_DISTRIB, wordsTheory.bit_count_upto_SUC] 518 \\ rw []) 519 |> Thm.INST_TYPE [Type.alpha |-> ``:16``] 520 |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [] 521 |> Conv.CONV_RULE (Conv.DEPTH_CONV (wordsLib.WORD_BIT_INDEX_CONV false)) 522 |> save_as "bit_count_sub" 523 524val bit_count_lt_1 = Q.store_thm("bit_count_lt_1", 525 `!w. bit_count w < 1 = (w = 0w)`, 526 rewrite_tac [DECIDE ``a < 1n = (a = 0)``, wordsTheory.bit_count_is_zero] 527 ) 528 529(* ------------------------------------------------------------------------ *) 530 531val Align = Q.store_thm("Align", 532 `(!w. Align (w, 1) = align 0 w) /\ 533 (!w. Align (w, 2) = align 1 w) /\ 534 (!w. Align (w, 4) = align 2 w) /\ 535 (!w. Align (w, 8) = align 3 w) /\ 536 (!w. Align (w, 16) = align 4 w)`, 537 simp [armTheory.Align_def, alignmentTheory.align_w2n] 538 ) 539 540val Aligned = Q.store_thm("Aligned", 541 `(!w. Aligned (w, 1) = aligned 0 w) /\ 542 (!w. Aligned (w, 2) = aligned 1 w) /\ 543 (!w. Aligned (w, 4) = aligned 2 w) /\ 544 (!w. Aligned (w, 8) = aligned 3 w) /\ 545 (!w. Aligned (w, 16) = aligned 4 w)`, 546 simp [armTheory.Aligned_def, Align, alignmentTheory.aligned_def, 547 boolTheory.EQ_SYM_EQ] 548 ) 549 550val aligned_23 = Q.store_thm("aligned_23", 551 `(!w: word32. ((1 >< 0) w = 0w: word2) = aligned 2 w) /\ 552 (!w: word32. ((2 >< 0) w = 0w: word3) = aligned 3 w)`, 553 simp [alignmentTheory.aligned_extract] 554 \\ blastLib.BBLAST_TAC 555 ) 556 557val AlignedAlign = ustore_thm("AlignedAlign", 558 `aligned p v ==> ((if b then align p v else v) = v)`, 559 lrw [alignmentTheory.aligned_def, alignmentTheory.align_align] 560 ) 561 562val Aligned_concat4 = Q.store_thm("Aligned_concat4", 563 `!p a: word8 b: word8 c: word8 d: word8. 564 aligned 2 (if p then a @@ b @@ c @@ d else d @@ c @@ b @@ a) = 565 aligned 2 (if p then d else a)`, 566 lrw [alignmentTheory.aligned_extract] 567 \\ blastLib.BBLAST_TAC 568 ) 569 570val Aligned4_bit0_t = utilsLib.ustore_thm ("Aligned4_bit0_t", 571 `aligned 2 (pc: word32) ==> ~word_bit 0 (pc + 4w)`, 572 simp [alignmentTheory.aligned_extract] 573 \\ blastLib.BBLAST_TAC 574 ) 575 576val Aligned4_bit1_t = utilsLib.ustore_thm ("Aligned4_bit1_t", 577 `aligned 2 (pc: word32) ==> ~word_bit 1 (pc + 4w)`, 578 simp [alignmentTheory.aligned_extract] 579 \\ blastLib.BBLAST_TAC 580 ) 581 582val Aligned4_bit0 = utilsLib.ustore_thm ("Aligned4_bit0", 583 `aligned 2 (pc: word32) ==> ~word_bit 0 (pc + 8w)`, 584 simp [alignmentTheory.aligned_extract] 585 \\ blastLib.BBLAST_TAC 586 ) 587 588val Aligned4_bit1 = utilsLib.ustore_thm ("Aligned4_bit1", 589 `aligned 2 (pc: word32) ==> ~word_bit 1 (pc + 8w)`, 590 simp [alignmentTheory.aligned_extract] 591 \\ blastLib.BBLAST_TAC 592 ) 593 594val Aligned_BranchTarget_thumb = 595 utilsLib.ustore_thm("Aligned_BranchTarget_thumb", 596 `aligned 1 (pc: word32) ==> 597 (aligned 1 (pc + (if b then 4w else 8w) + imm32) = aligned 1 imm32)`, 598 Cases_on `b` 599 \\ simp [alignmentTheory.aligned_extract] 600 \\ blastLib.BBLAST_TAC 601 ) 602 603val Aligned_BranchTarget_arm = utilsLib.ustore_thm("Aligned_BranchTarget_arm", 604 `aligned 2 (pc: word32) ==> 605 (aligned 2 (pc + (if b then 4w else 8w) + imm32) = aligned 2 imm32)`, 606 Cases_on `b` 607 \\ simp [alignmentTheory.aligned_extract] 608 \\ blastLib.BBLAST_TAC 609 ) 610 611val Aligned_Align_plus_minus = Q.store_thm("Aligned_Align_plus_minus", 612 `(!w x: word32. aligned 2 (align 2 w + x) = aligned 2 x) /\ 613 (!w x: word32. aligned 2 (align 2 w - x) = aligned 2 x) /\ 614 (!w x: word32. aligned 1 (align 2 w + x) = aligned 1 x) /\ 615 (!w x: word32. aligned 1 (align 2 w - x) = aligned 1 x)`, 616 lrw [alignmentTheory.aligned_extract, alignmentTheory.align_def] 617 \\ blastLib.BBLAST_TAC 618 ) 619 620val AlignedPC_plus_thumb = utilsLib.ustore_thm("AlignedPC_plus_thumb", 621 `aligned 1 (w: word32) ==> (align 1 (w + 4w + v) = w + align 1 v + 4w)`, 622 simp [alignmentTheory.aligned_extract, alignmentTheory.align_def] 623 \\ blastLib.BBLAST_TAC 624 ) 625 626val AlignedPC_plus_xthumb = utilsLib.ustore_thm("AlignedPC_plus_xthumb", 627 `aligned 1 (w: word32) ==> 628 (((31 >< 1) (w + 4w): 31 word) @@ (1w: word1) = w + 5w)`, 629 simp [alignmentTheory.aligned_extract] \\ blastLib.BBLAST_TAC 630 ) 631 632val AlignedPC_plus_align_arm = utilsLib.ustore_thm("AlignedPC_plus_align_arm", 633 `aligned 2 (w: word32) ==> 634 (align 2 (align 2 (w + 8w) + v) = w + align 2 v + 8w)`, 635 simp [alignmentTheory.aligned_extract, alignmentTheory.align_def] 636 \\ blastLib.BBLAST_TAC 637 ) 638 639val AlignedPC_plus_xarm = utilsLib.ustore_thm("AlignedPC_plus_xarm", 640 `aligned 2 (w: word32) ==> (align 1 (w + 8w + v) = w + align 1 v + 8w)`, 641 simp [alignmentTheory.aligned_extract, alignmentTheory.align_def] 642 \\ blastLib.BBLAST_TAC 643 ) 644 645val Aligned_plus_minus = utilsLib.ustore_thm("Aligned_plus_minus", 646 `aligned 2 (x: word32) ==> 647 (aligned 2 (if a then x + y else x - y) = aligned 2 y)`, 648 lrw [alignmentTheory.aligned_extract] \\ blastLib.FULL_BBLAST_TAC 649 ) 650 651val Aligned4_base_pc_plus = utilsLib.ustore_thm("Aligned4_base_pc_plus", 652 `aligned (if t then 1 else 2) (pc: word32) ==> 653 (aligned 2 (pc + (if t then 4w else 8w) + x) = 654 if t then aligned 2 (pc + x) else aligned 2 x)`, 655 lrw [alignmentTheory.aligned_extract] 656 \\ blastLib.FULL_BBLAST_TAC 657 ) 658 659val Aligned4_base_pc_minus = utilsLib.ustore_thm("Aligned4_base_pc_minus", 660 `aligned (if t then 1 else 2) (pc: word32) ==> 661 (aligned 2 (pc + (if t then 4w else 8w) - x) = 662 if t then aligned 2 (pc - x) else aligned 2 x)`, 663 lrw [alignmentTheory.aligned_extract] 664 \\ blastLib.FULL_BBLAST_TAC 665 ) 666 667val Aligned2_base_pc_plus = utilsLib.ustore_thm("Aligned2_base_pc_plus", 668 `aligned (if t then 1 else 2) (pc: word32) ==> 669 (aligned 1 (pc + (if t then 4w else 8w) + x) = aligned 1 x)`, 670 lrw [alignmentTheory.aligned_extract] 671 \\ blastLib.FULL_BBLAST_TAC 672 ) 673 674val Aligned2_base_pc_minus = utilsLib.ustore_thm("Aligned2_base_pc_minus", 675 `aligned (if t then 1 else 2) (pc: word32) ==> 676 (aligned 1 (pc + (if t then 4w else 8w) - x) = aligned 1 x)`, 677 lrw [alignmentTheory.aligned_extract] 678 \\ blastLib.FULL_BBLAST_TAC 679 ) 680 681val Align4_base_pc_plus = utilsLib.ustore_thm("Align4_base_pc_plus", 682 `aligned (if t then 1 else 2) (pc: word32) ==> 683 (align 2 (pc + if t then 4w else 8w) + x = 684 if t then align 2 pc + (x + 4w) else pc + (x + 8w))`, 685 lrw [alignmentTheory.aligned_extract, alignmentTheory.align_def] 686 \\ blastLib.FULL_BBLAST_TAC 687 ) 688 689val Align4_base_pc_minus = utilsLib.ustore_thm("Align4_base_pc_minus", 690 `aligned (if t then 1 else 2) (pc: word32) ==> 691 (align 2 (pc + if t then 4w else 8w) - x = 692 if t then align 2 pc - (x - 4w) else pc - (x - 8w))`, 693 lrw [alignmentTheory.aligned_extract, alignmentTheory.align_def] 694 \\ blastLib.FULL_BBLAST_TAC 695 ) 696 697(* ------------------------------------------------------------------------ *) 698 699val Align_branch_immediate = Q.store_thm("Align_branch_immediate", 700 `a + 701 align 2 702 (sw2sw ((v2w [x0; x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; x11; 703 x12; x13; x14; x15; x16; x17; x18; x19; x20; x21; 704 x22; x23]: word24 @@ (0w: word2)): 26 word): word32) = 705 if x0 then 706 a - 707 (v2w [~x1; ~x2; ~x3; ~x4; ~x5; ~x6; ~x7; ~x8; ~x9; ~x10; ~x11; ~x12; 708 ~x13; ~x14; ~x15; ~x16; ~x17; ~x18; ~x19; ~x20; ~x21; ~x22; ~x23; 709 T; T] + 1w) 710 else 711 a + 712 v2w [x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; x11; x12; x13; x14; x15; 713 x16; x17; x18; x19; x20; x21; x22; x23; F; F]`, 714 lrw [alignmentTheory.align_def] 715 \\ blastLib.FULL_BBLAST_TAC 716 ) 717 718val Align_branch_exchange_immediate = 719 Q.store_thm("Align_branch_exchange_immediate", 720 `a + 721 align 1 722 (sw2sw ((v2w [x0; x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; x11; 723 x12; x13; x14; x15; x16; x17; x18; x19; x20; x21; 724 x22; x23]: word24 @@ 725 (v2w [x24; F]: word2)): 26 word): word32) = 726 if x0 then 727 a - 728 (v2w [~x1; ~x2; ~x3; ~x4; ~x5; ~x6; ~x7; ~x8; ~x9; ~x10; ~x11; ~x12; 729 ~x13; ~x14; ~x15; ~x16; ~x17; ~x18; ~x19; ~x20; ~x21; ~x22; ~x23; 730 ~x24; T] + 1w) 731 else 732 a + 733 v2w [x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; x11; x12; x13; x14; x15; 734 x16; x17; x18; x19; x20; x21; x22; x23; x24; F]`, 735 lrw [alignmentTheory.align_def] 736 \\ blastLib.FULL_BBLAST_TAC 737 ) 738 739local 740 val t2 = ``(((31 >< 1) (i: word32) : 31 word) @@ (0w: word1)): word32`` 741 val lem = Q.prove( 742 `(!i:word32. ^t2 = align 1 i) /\ 743 (!i:word32. ((31 >< 2) i : 30 word) @@ (0w: word2) = align 2 i)`, 744 simp [alignmentTheory.align_def] 745 \\ blastLib.BBLAST_TAC 746 ) 747 val lem2 = Q.prove( 748 `(!i: word32. (if word_bit 0 i then ^t2 else i) = align 1 i)`, 749 lrw [lem, alignmentTheory.align_def] 750 \\ blastLib.FULL_BBLAST_TAC 751 ) 752in 753 val Align_LoadWritePC = Theory.save_thm("Align_LoadWritePC", 754 Thm.CONJ lem2 lem) 755end 756 757(* ------------------------------------------------------------------------ *) 758 759val take_id_imp = 760 metisLib.METIS_PROVE [listTheory.TAKE_LENGTH_ID] 761 ``!n w:'a list. (n = LENGTH w) ==> (TAKE n w = w)`` 762 763fun concat_tac l = 764 ntac (List.length l) strip_tac 765 \\ map_every bitstringLib.Cases_on_v2w l 766 \\ lfs [markerTheory.Abbrev_def] 767 \\ REPEAT (once_rewrite_tac [bitstringTheory.word_concat_v2w_rwt] 768 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.fixwidth_id_imp]) 769 770fun extract_bytes_tac l = 771 lrw [] 772 \\ map_every bitstringLib.Cases_on_v2w l 773 \\ lfs [markerTheory.Abbrev_def] 774 \\ ntac (List.length l - 1) 775 (once_rewrite_tac [bitstringTheory.word_concat_v2w_rwt] 776 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.fixwidth_id_imp]) 777 \\ lrw [bitstringTheory.field_def, bitstringTheory.shiftr_def, 778 listTheory.TAKE_APPEND1, take_id_imp, bitstringTheory.fixwidth_id_imp] 779 \\ lrw [bitstringTheory.fixwidth_def, rich_listTheory.DROP_APPEND2] 780 781val concat16 = Q.store_thm("concat16", 782 `!w1:word8 w2:word8. w2v w1 ++ w2v w2 = w2v (w1 @@ w2)`, 783 concat_tac [`w1`,`w2`] 784 ) 785 786val concat32 = Q.store_thm("concat32", 787 `!w1:word8 w2:word8 w3:word16. 788 w2v w1 ++ (w2v w2 ++ w2v w3) = w2v (w1 @@ w2 @@ w3)`, 789 concat_tac [`w1`,`w2`,`w3`] 790 ) 791 792val concat64 = Q.store_thm("concat64", 793 `!w1:word8 w2:word8 w3:word8 w4:word8 w5:word32. 794 w2v w1 ++ (w2v w2 ++ (w2v w3 ++ (w2v w4 ++ w2v w5))) = 795 w2v (w1 @@ w2 @@ w3 @@ w4 @@ w5)`, 796 concat_tac [`w1`,`w2`,`w3`,`w4`,`w5`] 797 ) 798 799val extract16 = Q.store_thm("extract16", 800 `!w1:word8 w2:word8. 801 field 7 0 (w2v (w1 @@ w2)) ++ field 15 8 (w2v (w1 @@ w2)) = 802 w2v (w2 @@ w1)`, 803 extract_bytes_tac [`w1`, `w2`] 804 ) 805 806val extract32 = Q.prove( 807 `!w1:word8 w2:word8 w3:word8 w4:word8. 808 let r = w1 @@ w2 @@ w3 @@ w4 in 809 field 7 0 (w2v r) ++ (field 15 8 (w2v r) ++ 810 (field 23 16 (w2v r) ++ (field 31 24 (w2v r)))) = 811 w2v (w4 @@ w3 @@ w2 @@ w1)`, 812 extract_bytes_tac [`w1`, `w2`, `w3`, `w4`]) 813 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) [] 814 |> save_as "extract32" 815 816val extract64 = Q.prove( 817 `!w1:word8 w2:word8 w3:word8 w4:word8 818 w5:word8 w6:word8 w7:word8 w8:word8. 819 let r = w1 @@ w2 @@ w3 @@ w4 @@ w5 @@ w6 @@ w7 @@ w8 in 820 field 7 0 (w2v r) ++ (field 15 8 (w2v r) ++ 821 (field 23 16 (w2v r) ++ (field 31 24 (w2v r) ++ 822 (field 39 32 (w2v r) ++ (field 47 40 (w2v r) ++ 823 (field 55 48 (w2v r) ++ (field 63 56 (w2v r)))))))) = 824 w2v (w8 @@ w7 @@ w6 @@ w5 @@ w4 @@ w3 @@ w2 @@ w1)`, 825 extract_bytes_tac [`w1`, `w2`, `w3`, `w4`,`w5`, `w6`, `w7`, `w8`]) 826 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) [] 827 |> save_as "extract64" 828 829val concat_bytes = Q.store_thm("concat_bytes", 830 `!w: word32. (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w = w`, 831 blastLib.BBLAST_TAC 832 ) 833 834val reverse_endian_bytes = Q.store_thm("reverse_endian_bytes", 835 `!w: word32. 836 ((7 >< 0) (reverse_endian w) = (31 >< 24) w) /\ 837 ((15 >< 8) (reverse_endian w) = (23 >< 16) w) /\ 838 ((23 >< 16) (reverse_endian w) = (15 >< 8) w) /\ 839 ((31 >< 24) (reverse_endian w) = (7 >< 0) w)`, 840 rw [reverse_endian_def] 841 \\ blastLib.BBLAST_TAC 842 ) 843 844val reverse_endian_id = Q.store_thm("reverse_endian_id", 845 `!w. reverse_endian (reverse_endian w) = w`, 846 rw [reverse_endian_def, reverse_endian_bytes, concat_bytes] 847 ) 848 849(* ------------------------------------------------------------------------ *) 850 851fun field_thm a b h l = 852 bitstringTheory.extract_v2w 853 |> Thm.INST_TYPE 854 [Type.alpha |-> fcpSyntax.mk_int_numeric_type a, 855 Type.beta |-> fcpSyntax.mk_int_numeric_type b] 856 |> Q.SPECL [h, l] 857 |> SIMP_RULE (srw_ss()) [] 858 |> Conv.GSYM 859 860val field16 = Q.store_thm("field16", 861 `(!w: word16. 862 v2w (field 15 8 (field 7 0 (w2v w) ++ field 15 8 (w2v w))) = 863 (7 >< 0) w : word8) /\ 864 (!w: word16. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 865 (!w: word16. 866 v2w (field 7 0 (field 7 0 (w2v w) ++ field 15 8 (w2v w))) = 867 (15 >< 8) w : word8) /\ 868 (!w: word16. v2w (field 7 0 (w2v w)) = (7 >< 0) w : word8)`, 869 lrw [bitstringTheory.field_concat_left, bitstringTheory.field_concat_right, 870 bitstringTheory.field_id_imp] 871 \\ simp [field_thm 16 8 `7` `0`, field_thm 16 8 `15` `8`] 872 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 873 ) 874 875val field32 = Q.store_thm("field32", 876 `(!w: word32. 877 v2w (field 31 24 878 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 879 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 880 (7 >< 0) w : word8) /\ 881 (!w: word32. v2w (field 31 24 (w2v w)) = (31 >< 24) w : word8) /\ 882 (!w: word32. 883 v2w (field 23 16 884 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 885 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 886 (15 >< 8) w : word8) /\ 887 (!w: word32. v2w (field 23 16 (w2v w)) = (23 >< 16) w : word8) /\ 888 (!w: word32. 889 v2w (field 15 8 890 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 891 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 892 (23 >< 16) w : word8) /\ 893 (!w: word32. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 894 (!w: word32. 895 v2w (field 7 0 896 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 897 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 898 (31 >< 24) w : word8) /\ 899 (!w: word32. v2w (field 7 0 (w2v w)) = (7 >< 0) w : word8)`, 900 lrw [bitstringTheory.field_concat_left, bitstringTheory.field_concat_right, 901 bitstringTheory.field_id_imp] 902 \\ simp [field_thm 32 8 `7` `0`, field_thm 32 8 `15` `8`, 903 field_thm 32 8 `23` `16`, field_thm 32 8 `31` `24`] 904 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 905 ) 906 907val fixwidth_w2v = Q.prove( 908 `!w : 'a word. fixwidth (dimindex (:'a)) (w2v w) = w2v w`, 909 simp []) 910 911val field_insert = Q.store_thm("field_insert", 912 `!msb lsb a : word32 b : word32. 913 v2w (field_insert msb lsb (field (msb - lsb) 0 (w2v a)) (w2v b)) : word32 = 914 bit_field_insert msb lsb a b`, 915 simp [bitstringTheory.field_insert_def, wordsTheory.bit_field_insert_def] 916 \\ once_rewrite_tac [GSYM fixwidth_w2v] 917 \\ simp_tac (bool_ss++fcpLib.FCP_ss) 918 [GSYM bitstringTheory.word_modify_v2w, bitstringTheory.v2w_w2v, 919 wordsTheory.WORD_MODIFY_BIT] 920 \\ simp [fixwidth_w2v] 921 \\ rw [] 922 \\ `(?p. p + lsb = i)` by metis_tac [arithmeticTheory.LESS_EQ_ADD_EXISTS] 923 \\ pop_assum (SUBST_ALL_TAC o GSYM) 924 \\ fs [] 925 \\ `?q. q + (lsb + p) = msb` 926 by metis_tac [arithmeticTheory.LESS_EQ_ADD_EXISTS] 927 \\ pop_assum (SUBST_ALL_TAC o GSYM) 928 \\ `SUC (p + q) - (q + 1) = p` by decide_tac 929 \\ simp [bitstringTheory.testbit, bitstringTheory.el_field, 930 bitstringTheory.el_w2v] 931 ) 932 933(* ------------------------------------------------------------------------ *) 934 935val get_bytes = Q.store_thm("get_bytes", 936 `((31 >< 24) 937 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 938 b23; b22; b21; b20; b19; b18; b17; b16; 939 b15; b14; b13; b12; b11; b10; b9; b8; 940 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 941 v2w [b31; b30; b29; b28; b27; b26; b25; b24]: word8) /\ 942 ((23 >< 16) 943 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 944 b23; b22; b21; b20; b19; b18; b17; b16; 945 b15; b14; b13; b12; b11; b10; b9; b8; 946 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 947 v2w [b23; b22; b21; b20; b19; b18; b17; b16]: word8) /\ 948 ((15 >< 8) 949 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 950 b23; b22; b21; b20; b19; b18; b17; b16; 951 b15; b14; b13; b12; b11; b10; b9; b8; 952 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 953 v2w [b15; b14; b13; b12; b11; b10; b9; b8]: word8) /\ 954 ((7 >< 0) 955 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 956 b23; b22; b21; b20; b19; b18; b17; b16; 957 b15; b14; b13; b12; b11; b10; b9; b8; 958 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 959 v2w [b7; b6; b5; b4; b3; b2; b1; b0]: word8)`, 960 blastLib.BBLAST_TAC 961 ) 962 963(* ------------------------------------------------------------------------ *) 964 965val get_vfp_imm32 = Q.store_thm("get_vfp_imm32", 966 `(31 >< 0) 967 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 968 b23; b22; b21; b20; b19; b18; b17; b16; 969 b15; b14; b13; b12; b11; b10; b9; b8; 970 b7; b6; b5; b4; b3; b2; b1; b0]: word64) = 971 v2w [b31; b30; b29; b28; b27; b26; b25; b24; 972 b23; b22; b21; b20; b19; b18; b17; b16; 973 b15; b14; b13; b12; b11; b10; b9; b8; 974 b7; b6; b5; b4; b3; b2; b1; b0]: word32`, 975 blastLib.BBLAST_TAC 976 ) 977 978val VFPExpandImm = Q.store_thm("VFPExpandImm", 979 `VFPExpandImm 980 ((v2w [b7; b6; b5; b4]:word4) @@ (v2w [b3; b2; b1; b0]:word4),b) = 981 if b then 982 v2w [b7; ~b6; b6; b6; b6; b6; b6; b5; b4; b3; b2; b1; b0; 983 F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F] 984 else 985 v2w [b7; ~b6; b6; b6; b6; b6; b6; b6; b6; b6; b5; b4; b3; b2; b1; b0; 986 F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; 987 F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; 988 F; F; F; F]`, 989 lrw [VFPExpandImm_def] 990 \\ blastLib.BBLAST_TAC 991 ) 992 993val fpscr_nzcv = Q.store_thm("fpscr_nzcv", 994 `!x:word4 fpscr. 995 rec'FPSCR (bit_field_insert 31 28 x (reg'FPSCR fpscr)) = 996 fpscr with <| N := x ' 3; Z := x ' 2; C := x ' 1; V := x ' 0 |>`, 997 utilsLib.REC_REG_BIT_FIELD_INSERT_TAC "arm" "FPSCR" `fpscr` 998 ) 999 1000val reg_fpscr = Theory.save_thm("reg_fpscr", utilsLib.mk_reg_thm "arm" "FPSCR") 1001 1002(* ------------------------------------------------------------------------ *) 1003 1004val v2w_13_15_rwts = Q.store_thm("v2w_13_15_rwts", 1005 `((v2w [F; b2; b1; b0] = 13w: word4) = F) /\ 1006 ((v2w [b2; F; b1; b0] = 13w: word4) = F) /\ 1007 ((v2w [b2; b1; T; b0] = 13w: word4) = F) /\ 1008 ((v2w [b2; b1; b0; F] = 13w: word4) = F) /\ 1009 ((v2w [F; b2; b1; b0] = 15w: word4) = F) /\ 1010 ((v2w [b2; F; b1; b0] = 15w: word4) = F) /\ 1011 ((v2w [b2; b1; F; b0] = 15w: word4) = F) /\ 1012 ((v2w [b2; b1; b0; F] = 15w: word4) = F)`, 1013 blastLib.BBLAST_TAC) 1014 1015fun enumerate_v2w n = 1016 let 1017 open Arbnum 1018 val m = toInt (pow (two, fromInt n)) 1019 in 1020 List.tabulate 1021 (m, fn i => bitstringLib.v2w_n2w_CONV 1022 (bitstringSyntax.padded_fixedwidth_of_num 1023 (Arbnum.fromInt i, n))) 1024 |> Drule.LIST_CONJ 1025 end 1026 1027val v2w_ground4 = Theory.save_thm("v2w_ground4", enumerate_v2w 4) 1028val v2w_ground5 = Theory.save_thm("v2w_ground5", enumerate_v2w 5) 1029 1030val bool_not_pc = Q.store_thm("bool_not_pc", 1031 `~(b3 /\ b2 /\ b1 /\ b0) = (v2w [b3; b2; b1; b0] <> 15w: word4)`, 1032 blastLib.BBLAST_TAC) 1033 1034val Decode_simps = Q.prove( 1035 `((3 >< 0) (0w : word8) = (0w : word4)) /\ 1036 (w2w (v2w [b2; b1; b0] : word3) = v2w [F; b2; b1; b0] : word4) /\ 1037 (w2w ((v2w [b5] : word1) @@ (v2w [b4; b3; b2; b1; b0] : word5) @@ 1038 (0w : word1)) = 1039 v2w [b5; b4; b3; b2; b1; b0; F] : word32) /\ 1040 (((v2w [b2] : word1) @@ (v2w [b1] : word1) @@ (v2w [b0] : word1) = 1041 0w:word3) = ~b2 /\ ~b1 /\ ~b0) /\ 1042 (word_msb (v2w [b3; b2; b1; b0] : word4) = b3) /\ 1043 ((v2w [b3] : word1) @@ v2w [b2; b1; b0] : word3 = 1044 v2w [b3; b2; b1; b0] : word4) /\ 1045 ((v2w [b4] : word1) @@ v2w [b3; b2; b1; b0] : word4 = 1046 v2w [b4; b3; b2; b1; b0] : word5) /\ 1047 (v2w [b4; b3; b2; b1] : word4 @@ (v2w [b0] : word1) = 1048 v2w [b4; b3; b2; b1; b0] : word5) /\ 1049 ((v2w [b3; b2; b1; b0] : word4) <+ 8w = ~b3) /\ 1050 ((v2w [b] : word1) @@ (0w : word1) = v2w [b; F] : word2) /\ 1051 (w2w ((v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8 @@ 1052 (0w: word2)) : word10) = 1053 v2w [b7; b6; b5; b4; b3; b2; b1; b0; F; F] : word32) /\ 1054 ((7 >< 4) (v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8) = 1055 v2w [b7; b6; b5; b4] : word4) /\ 1056 ((3 >< 0) (v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8) = 1057 v2w [b3; b2; b1; b0] : word4)`, 1058 lrw [] 1059 \\ blastLib.BBLAST_TAC 1060 ) 1061 1062val Decode_simps = Theory.save_thm ("Decode_simps", 1063 (Decode_simps :: 1064 List.tabulate 1065 (8, fn i => let 1066 val w = wordsSyntax.mk_wordii (i, 3) 1067 in 1068 blastLib.BBLAST_CONV ``v2w [a; b; c] = ^w`` 1069 end)) |> Drule.LIST_CONJ) 1070 1071val fpreg_div2 = Q.store_thm("fpreg_div2", 1072 `v2w [b4; b3; b2; b1; b0] // 2w = v2w [F; b4; b3; b2; b1] : word5`, 1073 blastLib.BBLAST_TAC) 1074 1075local 1076 val lem = 1077 (SIMP_RULE (srw_ss()) [] o Q.SPECL [`v`, `32`] o 1078 Thm.INST_TYPE [Type.alpha |-> ``:33``]) bitstringTheory.word_index_v2w 1079in 1080 val shift32 = Q.prove( 1081 `!w:word32 imm. 1082 ((w2w w : 33 word) << imm) ' 32 = testbit 32 (shiftl (w2v w) imm)`, 1083 strip_tac 1084 \\ bitstringLib.Cases_on_v2w `w` 1085 \\ fs [bitstringTheory.w2v_v2w, bitstringTheory.w2w_v2w, 1086 bitstringTheory.word_lsl_v2w, bitstringTheory.word_index_v2w, 1087 lem, markerTheory.Abbrev_def]) 1088end 1089 1090val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt", 1091 `!imm2 w C s. 1092 Shift_C (w: word32, SRType_LSL, imm2, C) s = 1093 ((w << imm2, if imm2 = 0 then C else ((w2w w : 33 word) << imm2) ' 32), 1094 s)`, 1095 lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F, shift32] 1096 ) 1097 1098val Shift_C_DecodeImmShift_rwt = Q.prove( 1099 `!typ imm5 w C s. 1100 Shift_C (w: word32, 1101 FST (DecodeImmShift (typ, imm5)), 1102 SND (DecodeImmShift (typ, imm5)), 1103 C) s = 1104 let amount = w2n imm5 in 1105 (if typ = 0w 1106 then if imm5 = 0w 1107 then (w, C) 1108 else (w << amount, ((w2w w : 33 word) << amount) ' 32) 1109 else if typ = 1w 1110 then if imm5 = 0w 1111 then (0w, word_msb w) 1112 else (w >>> amount, amount <= 32 /\ word_bit (amount - 1) w) 1113 else if typ = 2w 1114 then if imm5 = 0w 1115 then (w >> 32, word_msb w) 1116 else (w >> amount, word_bit (MIN 32 amount - 1) w) 1117 else if imm5 = 0w 1118 then SWAP (word_rrx (C, w)) 1119 else (w #>> amount, word_msb (w #>> amount)), s)`, 1120 strip_tac 1121 \\ wordsLib.Cases_on_word_value `typ` 1122 \\ simp [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def, 1123 DecodeImmShift_def, pairTheory.SWAP_def, shift32] 1124 \\ lrw [wordsTheory.word_rrx_def, wordsTheory.word_bit_def, 1125 wordsTheory.word_msb_def, wordsTheory.word_lsb_def, 1126 bitstringTheory.shiftl_replicate_F] 1127 \\ fs [] 1128 \\ blastLib.BBLAST_TAC 1129 \\ simp [bitstringTheory.testbit, bitstringTheory.el_field, 1130 bitstringTheory.el_w2v]) 1131 |> Q.SPEC `v2w [a; b]: word2` 1132 |> Conv.CONV_RULE 1133 (Conv.STRIP_QUANT_CONV 1134 (Conv.RHS_CONV 1135 (pairLib.let_CONV 1136 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV))) 1137 |> Drule.GEN_ALL 1138 |> save_as "Shift_C_DecodeImmShift_rwt" 1139 1140val Shift_C_DecodeRegShift_rwt = Q.prove( 1141 `!typ amount w C s. 1142 Shift_C (w: word32, DecodeRegShift typ, amount, C) s = 1143 (if typ = 0w 1144 then (w << amount, 1145 if amount = 0 then C else ((w2w w : 33 word) << amount) ' 32) 1146 else if typ = 1w 1147 then (w >>> amount, 1148 if amount = 0 then C 1149 else amount <= 32 /\ word_bit (amount - 1) w) 1150 else if typ = 2w 1151 then (w >> amount, 1152 if amount = 0 then C else word_bit (MIN 32 amount - 1) w) 1153 else (w #>> amount, 1154 if amount = 0 then C else word_msb (w #>> amount)), s)`, 1155 strip_tac 1156 \\ wordsLib.Cases_on_word_value `typ` 1157 \\ simp [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def, 1158 DecodeRegShift_def, shift32] 1159 \\ lrw [wordsTheory.word_bit_def, bitstringTheory.shiftl_replicate_F, 1160 wordsTheory.word_msb_def, wordsTheory.word_lsb_def] 1161 \\ fs []) 1162 |> Q.SPEC `v2w [a; b]: word2` 1163 |> Conv.CONV_RULE 1164 (Conv.STRIP_QUANT_CONV 1165 (Conv.RHS_CONV (Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV))) 1166 |> Drule.GEN_ALL 1167 |> save_as "Shift_C_DecodeRegShift_rwt" 1168 1169val FST_SWAP = Q.store_thm("FST_SWAP", 1170 `!x. FST (SWAP x) = SND x`, 1171 Cases \\ simp [pairTheory.SWAP_def] 1172 ) 1173 1174val ArchVersion_rwts = Q.prove( 1175 `(!s. ArchVersion () s < 6 = 1176 (s.Architecture = ARMv4) \/ 1177 (s.Architecture = ARMv4T) \/ 1178 (s.Architecture = ARMv5T) \/ 1179 (s.Architecture = ARMv5TE)) /\ 1180 (!s. ArchVersion () s >= 5 = 1181 (s.Architecture <> ARMv4) /\ 1182 (s.Architecture <> ARMv4T)) /\ 1183 (!s. (ArchVersion () s = 4) = 1184 ((s.Architecture = ARMv4) \/ 1185 (s.Architecture = ARMv4T))) /\ 1186 (!s. ArchVersion () s >= 6 = 1187 ((s.Architecture = ARMv6) \/ 1188 (s.Architecture = ARMv6K) \/ 1189 (s.Architecture = ARMv6T2) \/ 1190 (s.Architecture = ARMv7_A) \/ 1191 (s.Architecture = ARMv7_R))) /\ 1192 (!s. ArchVersion () s >= 7 = 1193 ((s.Architecture = ARMv7_A) \/ 1194 (s.Architecture = ARMv7_R)))`, 1195 lrw [ArchVersion_def] \\ Cases_on `s.Architecture` \\ lfs []) 1196 |> SIMP_RULE (srw_ss()) [] 1197 |> save_as "ArchVersion_rwts" 1198 1199val CurrentInstrSet_rwt = Q.prove( 1200 `((CurrentInstrSet x s = InstrSet_ARM) = ~s.CPSR.J /\ ~s.CPSR.T) /\ 1201 ((CurrentInstrSet x s = InstrSet_Thumb) = ~s.CPSR.J /\ s.CPSR.T) /\ 1202 ((CurrentInstrSet x s = InstrSet_Jazelle) = s.CPSR.J /\ ~s.CPSR.T) /\ 1203 ((CurrentInstrSet x s = InstrSet_ThumbEE) = s.CPSR.J /\ s.CPSR.T)`, 1204 lrw [CurrentInstrSet_def, ISETSTATE_def, bitstringTheory.word_concat_v2w] 1205 \\ blastLib.FULL_BBLAST_TAC 1206 ) 1207 1208fun after_srw tm = 1209 boolSyntax.rhs (Thm.concl (Conv.QCONV (SIMP_CONV (srw_ss()) []) tm)) 1210 1211val CurrentInstrSet_rwt = Theory.save_thm("CurrentInstrSet_rwt", 1212 REWRITE_RULE [ASSUME (after_srw ``~s.CPSR.J``)] 1213 (SIMP_RULE (srw_ss()) [] CurrentInstrSet_rwt)) 1214 1215(* ------------------------------------------------------------------------ *) 1216 1217val merge_cond = Theory.save_thm("merge_cond", 1218 METIS_PROVE [] 1219 ``(if x then a:'a else if y then a else b) = (if x \/ y then a else b)``) 1220 1221val not_cond = Theory.save_thm("not_cond", 1222 METIS_PROVE [] ``(if ~b then c:'a else d) = (if b then d else c)``) 1223 1224val isnot15 = Theory.save_thm("isnot15", 1225 blastLib.BBLAST_PROVE 1226 ``(n = 0w) \/ (n = 1w) \/ (n = 2w) \/ (n = 3w) \/ 1227 (n = 4w) \/ (n = 5w) \/ (n = 6w) \/ (n = 7w) \/ (n = 8w) \/ 1228 (n = 9w) \/ (n = 10w) \/ (n = 11w) \/ (n = 12w) \/ (n = 13w) \/ 1229 (n = 14w : word4) = (n <> 15w)``) 1230 1231val mustbe15 = Q.store_thm("mustbe15", 1232 `!w:word4. 1233 (if w = 0w then c0 else if w = 1w then c1 else if w = 2w then c2 else 1234 if w = 3w then c3 else if w = 4w then c4 else if w = 5w then c5 else 1235 if w = 6w then c6 else if w = 7w then c7 else if w = 8w then c8 else 1236 if w = 9w then c9 else if w = 10w then c10 else if w = 11w then c11 else 1237 if w = 12w then c12 else if w = 13w then c13 else if w = 14w then c14 else 1238 if w = 15w then c15 else c16) = 1239 (if w = 0w then c0 else if w = 1w then c1 else if w = 2w then c2 else 1240 if w = 3w then c3 else if w = 4w then c4 else if w = 5w then c5 else 1241 if w = 6w then c6 else if w = 7w then c7 else if w = 8w then c8 else 1242 if w = 9w then c9 else if w = 10w then c10 else if w = 11w then c11 else 1243 if w = 12w then c12 else if w = 13w then c13 else if w = 14w then c14 else 1244 c15)`, 1245 rw [] \\ blastLib.FULL_BBLAST_TAC 1246 ) 1247 1248(* ------------------------------------------------------------------------ *) 1249 1250local 1251 val t = ``LDM_UPTO f i r (b, s)`` 1252in 1253 val LDM_UPTO_components = 1254 Drule.LIST_CONJ 1255 (List.map (GEN_ALL o SIMP_CONV (srw_ss()) [LDM_UPTO_def]) 1256 [``FST ^t``, ``(SND ^t).MEM``, ``(SND ^t).CPSR``, 1257 ``(SND ^t).Architecture``, ``(SND ^t).Extensions``]) 1258 |> save_as "LDM_UPTO_components" 1259end 1260 1261local 1262 val LDM1_PC = Q.prove( 1263 `!n b registers s r m. 1264 n < 15 ==> 1265 (LDM1 (R_mode m) b registers s r n RName_PC = r RName_PC)`, 1266 REPEAT strip_tac 1267 \\ RULE_ASSUM_TAC (Conv.CONV_RULE wordsLib.LESS_CONV) 1268 \\ full_simp_tac bool_ss [] 1269 \\ fs [R_mode_def, LDM1_def, combinTheory.UPDATE_def] 1270 \\ lrw []) 1271in 1272 val LDM_UPTO_PC = Q.store_thm("LDM_UPTO_PC", 1273 `!b r s m. FOLDL (LDM1 (R_mode m) b r s) s.REG (COUNT_LIST 15) RName_PC = 1274 s.REG RName_PC`, 1275 rw [EVAL ``COUNT_LIST 15``, LDM1_PC]) 1276end 1277 1278val LDM_UPTO_RUN = Q.store_thm("LDM_UPTO_RUN", 1279 `!l f b r s c w u reg. 1280 FOLDL (LDM1 f b r 1281 (s with <|CurrentCondition := c; Encoding := w; undefined := u|>)) 1282 reg l = 1283 FOLDL (LDM1 f b r s) reg l`, 1284 Induct \\ lrw [LDM1_def]); 1285 1286local 1287 val rearrange = Q.prove( 1288 `(b + if P then 4w else 0w, 1289 s with REG := (if P then (x =+ y) else I) s.REG) = 1290 (if P then 1291 (b + 4w, s with REG := (x =+ y) s.REG) 1292 else 1293 (b, s))`, 1294 lrw [updateTheory.APPLY_UPDATE_ID] \\ lrw [arm_state_component_equality]) 1295 |> Drule.GEN_ALL 1296in 1297 val LDM_UPTO_0 = 1298 ``LDM_UPTO f 0 registers (b, s)`` 1299 |> SIMP_CONV (srw_ss()++boolSimps.LET_ss) 1300 [bit_count_upto_1, LDM_UPTO_def, LDM1_def, EVAL ``COUNT_LIST 1``, 1301 rearrange] 1302 |> Conv.GSYM 1303 |> save_as "LDM_UPTO_0" 1304end 1305 1306val LDM_UPTO_SUC = 1307 Q.prove( 1308 `!n f registers b s. 1309 n < 15 ==> 1310 ((let x = LDM_UPTO f n registers (b, s) in 1311 if word_bit (SUC n) registers then 1312 (FST x + 4w, 1313 SND x with REG := LDM1 f b registers s ((SND x).REG) (SUC n)) 1314 else 1315 x) = LDM_UPTO f (SUC n) registers (b, s))`, 1316 lrw [LDM_UPTO_def, DECIDE ``SUC n + 1 = SUC (n + 1)``, 1317 wordsTheory.bit_count_upto_def, sum_numTheory.SUM_def, 1318 wordsTheory.WORD_MULT_SUC, wordsTheory.word_bit_def] 1319 \\ RULE_ASSUM_TAC (REWRITE_RULE [arithmeticTheory.ADD1]) 1320 \\ fs [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC, 1321 GSYM arithmeticTheory.ADD1] 1322 \\ CONV_TAC (Conv.RHS_CONV (ONCE_REWRITE_CONV [LDM1_def])) 1323 \\ simp [wordsTheory.word_bit_def]) 1324 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) 1325 [numTheory.NOT_SUC, arithmeticTheory.SUC_SUB1, LDM1_def, 1326 LDM_UPTO_components] 1327 |> save_as "LDM_UPTO_SUC" 1328 1329(* ------------------------------------------------------------------------ *) 1330 1331local 1332 val t = ``STM_UPTO f i r (b, s)`` 1333in 1334 val STM_UPTO_components = 1335 Drule.LIST_CONJ 1336 (List.map (GEN_ALL o SIMP_CONV (srw_ss()) [STM_UPTO_def]) 1337 [``FST ^t``, ``(SND ^t).REG``, ``(SND ^t).CPSR``, 1338 ``(SND ^t).Extensions``]) 1339 |> save_as "STM_UPTO_components" 1340end 1341 1342val STM_UPTO_RUN = Q.store_thm("STM_UPTO_RUN", 1343 `!l f b r s c w u mem. 1344 FOLDL (STM1 f b r 1345 (s with <|CurrentCondition := c; Encoding := w; undefined := u|>)) 1346 mem l = 1347 FOLDL (STM1 f b r s) mem l`, 1348 Induct \\ lrw [STM1_def]); 1349 1350local 1351 val rearrange = Q.prove( 1352 `(b + if P then 4w else 0w, 1353 s with MEM := (if P then x else I) s.MEM) = 1354 (if P then 1355 (b + 4w, s with MEM := x s.MEM) 1356 else 1357 (b, s))`, 1358 lrw [updateTheory.APPLY_UPDATE_ID] \\ lrw [arm_state_component_equality]) 1359 |> Drule.GEN_ALL 1360in 1361 val STM_UPTO_0 = 1362 ``STM_UPTO f 0 registers (b, s)`` 1363 |> SIMP_CONV (srw_ss()++boolSimps.LET_ss) 1364 [bit_count_upto_1, STM_UPTO_def, STM1_def, EVAL ``COUNT_LIST 1``, 1365 rearrange] 1366 |> Conv.GSYM 1367 |> save_as "STM_UPTO_0" 1368end 1369 1370val STM_UPTO_SUC = 1371 Q.prove( 1372 `!n f registers b s. 1373 n < 15 ==> 1374 ((let x = STM_UPTO f n registers (b, s) in 1375 if word_bit (SUC n) registers then 1376 (FST x + 4w, 1377 SND x with MEM := STM1 f b registers s ((SND x).MEM) (SUC n)) 1378 else 1379 x) = STM_UPTO f (SUC n) registers (b, s))`, 1380 lrw [STM_UPTO_def, DECIDE ``SUC n + 1 = SUC (n + 1)``, 1381 wordsTheory.bit_count_upto_def, sum_numTheory.SUM_def, 1382 wordsTheory.WORD_MULT_SUC, wordsTheory.word_bit_def] 1383 \\ RULE_ASSUM_TAC (REWRITE_RULE [arithmeticTheory.ADD1]) 1384 \\ fs [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC, 1385 GSYM arithmeticTheory.ADD1] 1386 \\ CONV_TAC (Conv.RHS_CONV (ONCE_REWRITE_CONV [STM1_def])) 1387 \\ simp [wordsTheory.word_bit_def] 1388 ) 1389 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) 1390 [numTheory.NOT_SUC, arithmeticTheory.SUC_SUB1, STM1_def, 1391 STM_UPTO_components, combinTheory.o_THM] 1392 |> save_as "STM_UPTO_SUC" 1393 1394(* ------------------------------------------------------------------------ *) 1395 1396val () = export_theory () 1397