1(* ------------------------------------------------------------------------ 2 Definitions and theorems used by ARMv6-M step evaluator (m0_stepLib) 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6 7open utilsLib 8open wordsLib blastLib updateTheory 9open state_transformerTheory alignmentTheory m0Theory 10 11val _ = new_theory "m0_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 NextStateM0_def = Define` 21 NextStateM0 s0 = 22 let s1 = Next s0 in if s1.exception = NoException then SOME s1 else NONE` 23 24val NextStateM0_thumb = ustore_thm("NextStateM0_thumb", 25 `(s.exception = NoException) ==> 26 (Fetch s = (Thumb v, s)) /\ 27 (DecodeThumb v (s with pcinc := 2w) = (ast, s with pcinc := 2w)) /\ 28 (!s. Run ast s = f x s) /\ 29 (f x (s with pcinc := 2w) = s1) /\ 30 (s1.exception = s.exception) ==> 31 (NextStateM0 s = SOME s1)`, 32 lrw [NextStateM0_def, Next_def, Decode_def] 33 ) 34 35val NextStateM0_thumb2 = ustore_thm("NextStateM0_thumb2", 36 `(s.exception = NoException) ==> 37 (Fetch s = (Thumb2 v, s)) /\ 38 (DecodeThumb2 v (s with pcinc := 4w) = (ast, s with pcinc := 4w)) /\ 39 (!s. Run ast s = f x s) /\ 40 (f x (s with pcinc := 4w) = s1) /\ 41 (s1.exception = s.exception) ==> 42 (NextStateM0 s = SOME s1)`, 43 lrw [NextStateM0_def, Next_def, Decode_def] 44 ) 45 46(* ------------------------------------------------------------------------ *) 47 48val LDM1_def = Define` 49 LDM1 (f: word4 -> RName) b (registers: word9) s r j = 50 (if word_bit j registers then 51 f (n2w j) =+ 52 let a = b + if j = 0 then 0w else 4w * n2w (bit_count_upto j registers) 53 in 54 if s.AIRCR.ENDIANNESS then 55 s.MEM a @@ s.MEM (a + 1w) @@ s.MEM (a + 2w) @@ s.MEM (a + 3w) 56 else 57 s.MEM (a + 3w) @@ s.MEM (a + 2w) @@ s.MEM (a + 1w) @@ s.MEM a 58 else 59 I) r` 60 61val LDM_UPTO_def = Define` 62 LDM_UPTO f i (registers: word9) (b: word32, s) = 63 (b + 4w * n2w (bit_count_upto (i + 1) registers), 64 s with REG := FOLDL (LDM1 f b registers s) s.REG (COUNT_LIST (i + 1)))` 65 66val STM1_def = Define` 67 STM1 f (b: word32) (registers: 'a word) s m j = 68 (if word_bit j registers then 69 let a = b + if j = 0 then 0w else 4w * n2w (bit_count_upto j registers) 70 and r = s.REG (f (n2w j: word4)) 71 in 72 (a + 3w =+ if s.AIRCR.ENDIANNESS then (7 >< 0) r else (31 >< 24) r) o 73 (a + 2w =+ if s.AIRCR.ENDIANNESS then (15 >< 8) r else (23 >< 16) r) o 74 (a + 1w =+ if s.AIRCR.ENDIANNESS then (23 >< 16) r else (15 >< 8) r) o 75 (a =+ if s.AIRCR.ENDIANNESS then (31 >< 24) r else (7 >< 0) r) 76 else 77 I) m` 78 79val STM_UPTO_def = Define` 80 STM_UPTO f i (registers: 'a word) (b: word32, s) = 81 (b + 4w * n2w (bit_count_upto (i + 1) registers), 82 s with MEM := FOLDL (STM1 f b registers s) s.MEM (COUNT_LIST (i + 1)))` 83 84(* ------------------------------------------------------------------------ *) 85 86val R_name_def = Define` 87 R_name b (n: word4) = 88 case n of 89 0w => RName_0 | 1w => RName_1 | 2w => RName_2 90 | 3w => RName_3 | 4w => RName_4 | 5w => RName_5 91 | 6w => RName_6 | 7w => RName_7 | 8w => RName_8 92 | 9w => RName_9 | 10w => RName_10 | 11w => RName_11 93 | 12w => RName_12 | 13w => if b then RName_SP_process else RName_SP_main 94 | 14w => RName_LR | _ => RName_PC` 95 96(* ------------------------------------------------------------------------ *) 97 98val R_x_not_pc = Q.prove( 99 `!d. d <> 15w ==> R_name b d <> RName_PC`, 100 wordsLib.Cases_word_value 101 \\ rw [R_name_def] 102 ) 103 |> Drule.SPEC_ALL 104 |> usave_as "R_x_not_pc" 105 106val R_x_pc = Q.store_thm("R_x_pc", 107 `!b x. (R_name b x = RName_PC) = (x = 15w)`, 108 REPEAT strip_tac 109 \\ Cases_on `x = 15w` 110 \\ asm_simp_tac (srw_ss()) [R_name_def, DISCH_ALL R_x_not_pc] 111 ) 112 113val reverse_endian_def = Define` 114 reverse_endian (w: word32) = 115 (7 >< 0) w @@ (15 >< 8) w @@ (23 >< 16) w @@ (31 >< 24) w` 116 117(* ------------------------------------------------------------------------ *) 118 119val notoverflow = METIS_PROVE [integer_wordTheory.overflow] 120 ``!x y. (word_msb x = word_msb (x + y)) ==> (w2i (x + y) = w2i x + w2i y)`` 121 122val word_msb_sum1a = Q.prove( 123 `!x y. (word_msb x = word_msb y) /\ word_msb (x + y) ==> 124 word_msb (x + y + 1w)`, 125 Cases \\ Cases 126 \\ lrw [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 127 \\ Cases_on `INT_MIN (:'a) <= n` 128 \\ Cases_on `INT_MIN (:'a) <= n'` 129 \\ lfs [] 130 >- (imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 131 \\ pop_assum (K all_tac) 132 \\ `p < INT_MIN (:'a) /\ p' < INT_MIN (:'a)` 133 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 134 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 135 \\ `(p + (p' + (dimword (:'a) + 1)) = dimword (:'a) + (p + p' + 1)) /\ 136 (p + (p' + dimword (:'a)) = dimword (:'a) + (p + p'))` by lrw [] 137 \\ pop_assum SUBST_ALL_TAC \\ pop_assum SUBST1_TAC 138 \\ full_simp_tac bool_ss 139 [arithmeticTheory.ADD_MODULUS_RIGHT, wordsTheory.ZERO_LT_dimword] 140 \\ `p + p' + 1 < dimword (:'a)` 141 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 142 \\ lfs []) 143 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 144 \\ `n + n' + 1 < dimword (:'a)` 145 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 146 \\ lfs [] 147 ) 148 149val word_msb_sum1b = Q.prove( 150 `!x y. (word_msb x <> word_msb y) /\ ~word_msb (x + y) ==> 151 (word_msb (x + y) = word_msb (x + y + 1w))`, 152 Cases \\ Cases 153 \\ simp_tac std_ss 154 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 155 \\ lrw [] 156 \\ Cases_on `n < INT_MIN (:'a)` 157 \\ Cases_on `n' < INT_MIN (:'a)` 158 \\ lfs [arithmeticTheory.NOT_LESS, arithmeticTheory.NOT_LESS_EQUAL] 159 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 160 \\ lfs [arithmeticTheory.NOT_LESS] 161 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 162 \\ pop_assum (K all_tac) 163 \\ `p < INT_MIN (:'a)` by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 164 \\ lrw [arithmeticTheory.ADD_MODULUS_LEFT] 165 ) 166 167val word_msb_sum1c = Q.prove( 168 `!x y. word_msb (x + y + 1w) /\ ~word_msb (x + y) ==> (x + y = INT_MAXw)`, 169 Cases \\ Cases 170 \\ `INT_MIN (:'a) - 1 < dimword (:'a)` 171 by (assume_tac wordsTheory.INT_MIN_LT_DIMWORD \\ decide_tac) 172 \\ simp_tac std_ss 173 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_H_def, 174 wordsTheory.INT_MAX_def, wordsTheory.word_add_n2w] 175 \\ lrw [] 176 \\ lfs [arithmeticTheory.NOT_LESS_EQUAL] 177 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 178 \\ lfs [arithmeticTheory.NOT_LESS] 179 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 180 \\ pop_assum (K all_tac) 181 \\ `p < dimword (:'a)` by lfs [] 182 \\ Cases_on `n + n' < dimword (:'a)` 183 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT, arithmeticTheory.NOT_LESS] 184 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 185 \\ pop_assum (K all_tac) 186 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT] 187 ) 188 189val AddWithCarry = Q.store_thm("AddWithCarry", 190 `!x y carry_in. AddWithCarry (x,y,carry_in) = add_with_carry (x,y,carry_in)`, 191 REPEAT strip_tac 192 \\ simp [AddWithCarry_def, wordsTheory.add_with_carry_def] 193 \\ simp [GSYM wordsTheory.word_add_n2w] 194 \\ Cases_on `carry_in` 195 \\ simp [integer_wordTheory.overflow] 196 \\ Cases_on `dimindex(:'a) = 1` 197 >- (imp_res_tac wordsTheory.dimindex_1_cases 198 \\ pop_assum (fn th => (strip_assume_tac (Q.SPEC `x` th) 199 \\ strip_assume_tac (Q.SPEC `y` th))) 200 \\ simp [wordsTheory.word_index, wordsTheory.word_msb_def, 201 wordsTheory.word_2comp_def, integer_wordTheory.w2i_def, 202 wordsTheory.dimword_def]) 203 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)` 204 \\ `~word_msb 1w` 205 by lrw [wordsTheory.word_msb_n2w, DECIDE ``0n < n /\ n <> 1 ==> ~(n <= 1)``] 206 \\ fs [integer_wordTheory.different_sign_then_no_overflow, 207 integer_wordTheory.overflow, integer_wordTheory.w2i_1] 208 >- (Cases_on `word_msb x <=> word_msb y` \\ simp [word_msb_sum1a]) 209 \\ Cases_on `word_msb x = word_msb y` 210 \\ simp [GSYM integer_wordTheory.different_sign_then_no_overflow] 211 >- (Cases_on `word_msb (x + y + 1w)` 212 \\ lfs [notoverflow, integer_wordTheory.w2i_1] 213 >- (imp_res_tac word_msb_sum1c 214 \\ lfs [integer_wordTheory.w2i_INT_MINw] 215 \\ Cases_on `x` 216 \\ Cases_on `y` 217 \\ lfs [wordsTheory.word_msb_n2w_numeric] 218 \\ Cases_on `INT_MIN (:'a) <= n'` 219 \\ lfs [integer_wordTheory.w2i_n2w_pos, 220 integer_wordTheory.w2i_n2w_neg, 221 wordsTheory.word_add_n2w, 222 wordsTheory.word_L_def, 223 wordsTheory.word_2comp_def, 224 integerTheory.INT_ADD_CALCULATE] 225 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 226 \\ `p + p' < dimword (:'a)` 227 by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 228 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 229 \\ `(p + (p' + dimword (:'a)) = (p + p') + dimword (:'a)) /\ 230 (INT_MIN (:'a) + dimword (:'a) - 1 = 231 dimword (:'a) + (INT_MIN (:'a) - 1))` 232 by lfs [] 233 \\ ntac 2 (pop_assum SUBST_ALL_TAC) 234 \\ full_simp_tac bool_ss 235 [arithmeticTheory.ADD_MODULUS_LEFT, 236 arithmeticTheory.ADD_MODULUS_RIGHT, 237 wordsTheory.ZERO_LT_dimword] 238 \\ lfs [wordsTheory.BOUND_ORDER] 239 \\ metis_tac [arithmeticTheory.ADD_ASSOC, 240 wordsTheory.dimword_sub_int_min, 241 wordsTheory.ZERO_LT_INT_MIN, 242 DECIDE ``0n < n ==> (n - 1 + 1 = n)``]) 243 \\ metis_tac [integer_wordTheory.overflow, integer_wordTheory.w2i_1]) 244 \\ `word_msb (x + y) <=> word_msb (x + y + 1w)` by imp_res_tac word_msb_sum1b 245 \\ simp [notoverflow, integer_wordTheory.w2i_1] 246 ) 247 248(* ------------------------------------------------------------------------ *) 249 250val CountLeadingZeroBits8 = Q.store_thm("CountLeadingZeroBits8", 251 `!w:word8. 252 CountLeadingZeroBits w = if w = 0w then 8 else 7 - w2n (word_log2 w)`, 253 lrw [CountLeadingZeroBits_def, HighestSetBit_def] 254 \\ `LOG2 (w2n w) < 8` 255 by metis_tac [wordsTheory.LOG2_w2n_lt, EVAL ``dimindex(:8)``] 256 \\ lrw [integer_wordTheory.w2i_def, wordsTheory.word_log2_def, 257 wordsTheory.word_msb_n2w_numeric, 258 intLib.ARITH_PROVE ``j < 8 ==> (Num (7 - &j) = 7 - j)``] 259 ) 260 261val FOLDL_cong = Q.store_thm("FOLDL_cong", 262 `!l r f g a b. 263 (LENGTH l = LENGTH r) /\ (a = b) /\ 264 (!i x. i < LENGTH l ==> (f x (EL i l) = g x (EL i r))) ==> 265 (FOLDL f a l = FOLDL g b r)`, 266 Induct \\ lrw [] 267 \\ Cases_on `r` \\ lfs [] 268 \\ metis_tac [prim_recTheory.LESS_0, listTheory.EL, listTheory.HD, 269 listTheory.EL_restricted, arithmeticTheory.LESS_MONO_EQ] 270 ) 271 272val FOR_BASE = Q.store_thm("FOR_BASE", 273 `!f s. FOR (n, n, f) s = f n s`, 274 simp [Once state_transformerTheory.FOR_def]) 275 276val FOR_FOLDL = Q.store_thm("FOR_FOLDL", 277 `!i j f s. 278 i <= j ==> 279 (FOR (i, j, f) s = 280 ((), FOLDL (\x n. SND (f (n + i) x)) s (COUNT_LIST (j - i + 1))))`, 281 ntac 2 strip_tac \\ Induct_on `j - i` 282 \\ lrw [Once state_transformerTheory.FOR_def, pairTheory.UNCURRY, 283 state_transformerTheory.BIND_DEF] 284 >- (`i = j` by decide_tac 285 \\ simp [] 286 \\ EVAL_TAC 287 \\ Cases_on `f j s` 288 \\ simp [oneTheory.one]) 289 \\ `v = j - (i + 1)` by decide_tac 290 \\ qpat_assum `!j i. P` (qspecl_then [`j`, `i + 1`] imp_res_tac) 291 \\ Cases_on `i + 1 < j` 292 >- (`j + 1 - i = SUC (j - i)` by decide_tac 293 \\ lrw [rich_listTheory.COUNT_LIST_def] 294 \\ match_mp_tac FOLDL_cong 295 \\ lrw [rich_listTheory.COUNT_LIST_GENLIST, listTheory.MAP_GENLIST, 296 arithmeticTheory.ADD1]) 297 \\ `j = i + 1` by decide_tac 298 \\ simp [] 299 \\ EVAL_TAC 300 ) 301 302val FOLDL_AUG = Q.prove( 303 `!f a l. 304 FOLDL (\x i. f x i) a l = 305 FST (FOLDL (\y i. (f (FST y) i, ())) (a, ()) l)`, 306 Induct_on `l` \\ lrw [] 307 ) 308 309val BitCount = Q.store_thm("BitCount", 310 `!w. BitCount w = bit_count w`, 311 lrw [BitCount_def, wordsTheory.bit_count_def, wordsTheory.bit_count_upto_def, 312 wordsTheory.word_bit_def] 313 \\ `0 <= dimindex(:'a) - 1` by lrw [] 314 \\ simp 315 [FOR_FOLDL 316 |> Q.ISPECL [`0n`, `dimindex(:'a) - 1`, 317 `\i state: num # unit. 318 ((), 319 if i <= dimindex(:'a) - 1 /\ w ' i then 320 (FST state + 1, ()) 321 else 322 state)`], 323 sum_numTheory.SUM_FOLDL] 324 \\ REWRITE_TAC 325 [FOLDL_AUG 326 |> Q.ISPECL 327 [`\x:num i. x + if w ' i then 1 else 0`, `0`, 328 `COUNT_LIST (dimindex ((:'a) :'a itself))`] 329 |> SIMP_RULE (srw_ss())[]] 330 \\ MATCH_MP_TAC (METIS_PROVE [] ``(x = y) ==> (FST x = FST y)``) 331 \\ MATCH_MP_TAC listTheory.FOLDL_CONG 332 \\ lrw [rich_listTheory.MEM_COUNT_LIST, 333 DECIDE ``0n < n ==> (n - 1 + 1 = n)``] 334 \\ Cases_on `a` 335 \\ simp [] 336 ) 337 338val bit_count_upto_1 = Q.prove( 339 `!registers: 'a word. 340 4w * n2w (bit_count_upto 1 registers) = 341 if word_bit 0 registers then 4w else 0w: word32`, 342 EVAL_TAC \\ lrw [wordsTheory.word_bit_def] 343 ) 344 345val bit_count_sub = Q.prove( 346 `!r: 'a word. 347 n2w (bit_count_upto (dimindex(:'a) - 1) r) - n2w (bit_count r) = 348 if r ' (dimindex(:'a) - 1) then -1w else 0w`, 349 REPEAT strip_tac 350 \\ simp [wordsTheory.bit_count_def] 351 \\ Cases_on `dimindex(:'a)` 352 >- lfs [DECIDE ``0 < n ==> (n <> 0n)``] 353 \\ simp [arithmeticTheory.SUC_SUB1, GSYM wordsTheory.word_add_n2w, 354 wordsTheory.WORD_LEFT_ADD_DISTRIB, wordsTheory.bit_count_upto_SUC] 355 \\ rw []) 356 |> Thm.INST_TYPE [Type.alpha |-> ``:16``] 357 |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [] 358 |> Conv.CONV_RULE (Conv.DEPTH_CONV (wordsLib.WORD_BIT_INDEX_CONV false)) 359 |> save_as "bit_count_sub" 360 361val bit_count_lt_1 = Q.store_thm("bit_count_lt_1", 362 `!w. bit_count w < 1 = (w = 0w)`, 363 rewrite_tac [DECIDE ``a < 1n = (a = 0)``, wordsTheory.bit_count_is_zero] 364 ) 365 366(* ------------------------------------------------------------------------ *) 367 368val Align = Q.store_thm("Align", 369 `(!w. Align (w, 1) = align 0 w) /\ 370 (!w. Align (w, 2) = align 1 w) /\ 371 (!w. Align (w, 4) = align 2 w)`, 372 simp [m0Theory.Align_def, alignmentTheory.align_w2n] 373 ) 374 375val Aligned = Q.store_thm("Aligned", 376 `(!w. Aligned (w, 1) = aligned 0 w) /\ 377 (!w. Aligned (w, 2) = aligned 1 w) /\ 378 (!w. Aligned (w, 4) = aligned 2 w)`, 379 simp [m0Theory.Aligned_def, Align, alignmentTheory.aligned_def, 380 boolTheory.EQ_SYM_EQ] 381 ) 382 383val Aligned_concat4 = Q.store_thm("Aligned_concat4", 384 `!p a: word8 b: word8 c: word8 d: word8. 385 aligned 2 (if p then a @@ b @@ c @@ d else d @@ c @@ b @@ a) = 386 aligned 2 (if p then d else a)`, 387 lrw [alignmentTheory.aligned_extract] \\ blastLib.BBLAST_TAC 388 ) 389 390val Aligned_SP = utilsLib.ustore_thm("Aligned_SP", 391 `aligned 2 (sp:word32) ==> (sp + 4w * a && 0xFFFFFFFCw = sp + 4w * a)`, 392 simp [alignmentTheory.aligned_extract] 393 \\ blastLib.BBLAST_TAC 394 ) 395 396val Aligned_Branch9 = utilsLib.ustore_thm("Aligned_Branch9", 397 `aligned 1 (w:word32) ==> 398 (((31 >< 1) 399 (w + 400 sw2sw (v2w [x0; x1; x2; x3; x4; x5; x6; x7; F]: word9))) 401 @@ (0w: word1) = 402 w + 403 v2w [x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; 404 x0; x0; x0; x0; x0; x0; x0; x0; x1; x2; x3; x4; x5; x6; x7; F])`, 405 simp [alignmentTheory.aligned_extract] 406 \\ blastLib.BBLAST_TAC 407 ) 408 409val Aligned_Branch12 = utilsLib.ustore_thm("Aligned_Branch12", 410 `aligned 1 (w:word32) ==> 411 (((31 >< 1) 412 (w + 413 sw2sw (v2w [x0; x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; F]: word12))) 414 @@ (0w: word1) = 415 w + 416 v2w [x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; 417 x0; x0; x0; x0; x0; x1; x2; x3; x4; x5; x6; x7; x8; x9; x10; F])`, 418 simp [alignmentTheory.aligned_extract] 419 \\ blastLib.BBLAST_TAC 420 ) 421 422val Aligned_Branch_Wide6 = utilsLib.ustore_thm("Aligned_Branch_Wide6", 423 `aligned 1 (w:word32) ==> 424 (((31 >< 1) 425 (w + 426 sw2sw ((v2w [x0]:word1) @@ (v2w [x1]:word1) @@ (v2w [x2]:word1) @@ 427 (v2w [x3; x4; x5; x6; x7; x8]:word6) @@ 428 (v2w [x9; x10; x11; x12; x13; x14; 429 x15; x16; x17; x18; x19; F]:word12))) 430 @@ (0w: word1)) = 431 w + 432 v2w [x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x0; x1; x2; x3; x4; 433 x5; x6; x7; x8; x9; x10; x11; x12; x13; x14; x15; x16; x17; x18; 434 x19; F])`, 435 simp [alignmentTheory.aligned_extract] 436 \\ blastLib.BBLAST_TAC 437 ) 438 439val Aligned_Branch_Wide10 = utilsLib.ustore_thm("Aligned_Branch_Wide10", 440 `aligned 1 (w:word32) ==> 441 (((31 >< 1) 442 (w + 443 sw2sw ((v2w [x0]:word1) @@ ~(v2w [x1a] ?? v2w [x1b] : word1) @@ 444 ~(v2w [x2a] ?? v2w [x2b]:word1) @@ 445 (v2w [x3; x4; x5; x6; x7; x8; x9; x10; x11; x12]:word10) @@ 446 (v2w [x13; x14; x15; x16; x17; x18; 447 x19; x20; x21; x22; x23; F]:word12))) 448 @@ (0w: word1)) = 449 w + 450 v2w [x0; x0; x0; x0; x0; x0; x0; x0; x1a = x1b; x2a = x2b; x3; x4; x5; 451 x6; x7; x8; x9; x10; x11; x12; x13; x14; x15; x16; x17; x18; x19; 452 x20; x21; x22; x23; F])`, 453 simp [alignmentTheory.aligned_extract] 454 \\ blastLib.BBLAST_TAC 455 ) 456 457(* 458val Aligned_BranchEx = utilsLib.ustore_thm("Aligned_BranchEx", 459 `~word_bit 0 (r: word32) ==> 460 (((31 >< 1) r : 31 word @@ (0w: word1)) = r)`, 461 blastLib.BBLAST_TAC 462 ) 463*) 464 465val Aligned_BranchLink = utilsLib.ustore_thm("Aligned_BranchLink", 466 `aligned 1 (w:word32) ==> 467 (((31 >< 1) (w + 4w) : 31 word @@ (1w: word1)) = (w + 4w) !! 1w)`, 468 simp [alignmentTheory.aligned_extract] 469 \\ blastLib.BBLAST_TAC 470 ) 471 472val Aligned_BranchLinkEx = utilsLib.ustore_thm("Aligned_BranchLinkEx", 473 `aligned 1 (w:word32) ==> 474 (((31 >< 1) (w + 4w - 2w) : 31 word @@ (1w: word1)) = (w + 2w) !! 1w)`, 475 simp [alignmentTheory.aligned_extract] 476 \\ blastLib.BBLAST_TAC 477 ) 478 479val tm = Term.subst [``b0:bool`` |-> boolSyntax.F] (bitstringSyntax.mk_vec 32 0) 480 481val Aligned_Branch = Q.store_thm("Aligned_Branch", 482 `(aligned 1 (pc:word32) ==> aligned 1 (pc + 4w + ^tm)) = T`, 483 rw [alignmentTheory.aligned_extract] 484 \\ blastLib.FULL_BBLAST_TAC 485 ) 486 487val Aligned_LoadStore = Q.store_thm("Aligned_LoadStore", 488 `aligned 1 (w: 31 word @@ (0w: word1))`, 489 rw [alignmentTheory.aligned_extract] 490 \\ blastLib.FULL_BBLAST_TAC 491 ) 492 493val Aligned4_base_pc = Q.store_thm("Aligned4_base_pc", 494 `aligned 2 495 (align 2 pc + 496 w2w (v2w [b7; b6; b5; b4; b3; b2; b1; b0; F; F] : word10): word32)`, 497 simp [alignmentTheory.aligned_extract, alignmentTheory.align_def] 498 \\ blastLib.FULL_BBLAST_TAC 499 ) 500 501(* ------------------------------------------------------------------------ *) 502 503val word_bit_0_of_load = Q.store_thm("word_bit_0_of_load", 504 `!x a:word8 b:word8 c:word8 d:word8. 505 word_bit 0 (if x then a @@ b @@ c @@ d else d @@ c @@ b @@ a) = 506 word_bit 0 (if x then d else a)`, 507 lrw [] 508 \\ blastLib.BBLAST_TAC 509 ) 510 511(* ------------------------------------------------------------------------ *) 512 513val take_id_imp = 514 metisLib.METIS_PROVE [listTheory.TAKE_LENGTH_ID] 515 ``!n w:'a list. (n = LENGTH w) ==> (TAKE n w = w)`` 516 517fun concat_tac l = 518 ntac (List.length l) strip_tac 519 \\ map_every bitstringLib.Cases_on_v2w l 520 \\ lfs [markerTheory.Abbrev_def] 521 \\ REPEAT (once_rewrite_tac [bitstringTheory.word_concat_v2w_rwt] 522 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.fixwidth_id_imp]) 523 524fun extract_bytes_tac l = 525 lrw [] 526 \\ map_every bitstringLib.Cases_on_v2w l 527 \\ lfs [markerTheory.Abbrev_def] 528 \\ ntac (List.length l - 1) 529 (once_rewrite_tac [bitstringTheory.word_concat_v2w_rwt] 530 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.fixwidth_id_imp]) 531 \\ lrw [bitstringTheory.field_def, bitstringTheory.shiftr_def, 532 listTheory.TAKE_APPEND1, take_id_imp, bitstringTheory.fixwidth_id_imp] 533 \\ lrw [bitstringTheory.fixwidth_def, rich_listTheory.DROP_APPEND2] 534 535val concat16 = Q.store_thm("concat16", 536 `!w1:word8 w2:word8. w2v w1 ++ w2v w2 = w2v (w1 @@ w2)`, 537 concat_tac [`w1`,`w2`] 538 ) 539 540val concat32 = Q.store_thm("concat32", 541 `!w1:word8 w2:word8 w3:word16. 542 w2v w1 ++ (w2v w2 ++ w2v w3) = w2v (w1 @@ w2 @@ w3)`, 543 concat_tac [`w1`,`w2`,`w3`] 544 ) 545 546val extract16 = Q.store_thm("extract16", 547 `!w1:word8 w2:word8. 548 field 7 0 (w2v (w1 @@ w2)) ++ field 15 8 (w2v (w1 @@ w2)) = 549 w2v (w2 @@ w1)`, 550 extract_bytes_tac [`w1`, `w2`] 551 ) 552 553val extract32 = Q.prove( 554 `!w1:word8 w2:word8 w3:word8 w4:word8. 555 let r = w1 @@ w2 @@ w3 @@ w4 in 556 field 7 0 (w2v r) ++ (field 15 8 (w2v r) ++ 557 (field 23 16 (w2v r) ++ (field 31 24 (w2v r)))) = 558 w2v (w4 @@ w3 @@ w2 @@ w1)`, 559 extract_bytes_tac [`w1`, `w2`, `w3`, `w4`]) 560 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) [] 561 |> save_as "extract32" 562 563(* ------------------------------------------------------------------------ *) 564 565fun field_thm a b h l = 566 bitstringTheory.extract_v2w 567 |> Thm.INST_TYPE 568 [Type.alpha |-> fcpSyntax.mk_int_numeric_type a, 569 Type.beta |-> fcpSyntax.mk_int_numeric_type b] 570 |> Q.SPECL [h, l] 571 |> SIMP_RULE (srw_ss()) [] 572 |> Conv.GSYM 573 574val field16 = Q.store_thm("field16", 575 `(!w: word16. 576 v2w (field 15 8 (field 7 0 (w2v w) ++ field 15 8 (w2v w))) = 577 (7 >< 0) w : word8) /\ 578 (!w: word16. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 579 (!w: word16. 580 v2w (field 7 0 (field 7 0 (w2v w) ++ field 15 8 (w2v w))) = 581 (15 >< 8) w : word8) /\ 582 (!w: word16. v2w (field 7 0 (w2v w)) = (7 >< 0) w : word8)`, 583 lrw [bitstringTheory.field_concat_left, bitstringTheory.field_concat_right, 584 bitstringTheory.field_id_imp] 585 \\ simp [field_thm 16 8 `7` `0`, field_thm 16 8 `15` `8`] 586 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 587 ) 588 589val field32 = Q.store_thm("field32", 590 `(!w: word32. 591 v2w (field 31 24 592 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 593 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 594 (7 >< 0) w : word8) /\ 595 (!w: word32. v2w (field 31 24 (w2v w)) = (31 >< 24) w : word8) /\ 596 (!w: word32. 597 v2w (field 23 16 598 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 599 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 600 (15 >< 8) w : word8) /\ 601 (!w: word32. v2w (field 23 16 (w2v w)) = (23 >< 16) w : word8) /\ 602 (!w: word32. 603 v2w (field 15 8 604 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 605 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 606 (23 >< 16) w : word8) /\ 607 (!w: word32. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 608 (!w: word32. 609 v2w (field 7 0 610 (field 7 0 (w2v w) ++ (field 15 8 (w2v w) ++ 611 (field 23 16 (w2v w) ++ field 31 24 (w2v w))))) = 612 (31 >< 24) w : word8) /\ 613 (!w: word32. v2w (field 7 0 (w2v w)) = (7 >< 0) w : word8)`, 614 lrw [bitstringTheory.field_concat_left, bitstringTheory.field_concat_right, 615 bitstringTheory.field_id_imp] 616 \\ simp [field_thm 32 8 `7` `0`, field_thm 32 8 `15` `8`, 617 field_thm 32 8 `23` `16`, field_thm 32 8 `31` `24`] 618 \\ srw_tac [wordsLib.WORD_EXTRACT_ss] [] 619 ) 620 621(* ------------------------------------------------------------------------ *) 622 623val get_bytes = Q.store_thm("get_bytes", 624 `((31 >< 24) 625 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 626 b23; b22; b21; b20; b19; b18; b17; b16; 627 b15; b14; b13; b12; b11; b10; b9; b8; 628 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 629 v2w [b31; b30; b29; b28; b27; b26; b25; b24]: word8) /\ 630 ((23 >< 16) 631 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 632 b23; b22; b21; b20; b19; b18; b17; b16; 633 b15; b14; b13; b12; b11; b10; b9; b8; 634 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 635 v2w [b23; b22; b21; b20; b19; b18; b17; b16]: word8) /\ 636 ((15 >< 8) 637 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 638 b23; b22; b21; b20; b19; b18; b17; b16; 639 b15; b14; b13; b12; b11; b10; b9; b8; 640 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 641 v2w [b15; b14; b13; b12; b11; b10; b9; b8]: word8) /\ 642 ((7 >< 0) 643 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 644 b23; b22; b21; b20; b19; b18; b17; b16; 645 b15; b14; b13; b12; b11; b10; b9; b8; 646 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 647 v2w [b7; b6; b5; b4; b3; b2; b1; b0]: word8) /\ 648 ((15 >< 8) 649 (v2w [b15; b14; b13; b12; b11; b10; b9; b8; 650 b7; b6; b5; b4; b3; b2; b1; b0]: word16) = 651 v2w [b15; b14; b13; b12; b11; b10; b9; b8]: word8) /\ 652 ((7 >< 0) 653 (v2w [b15; b14; b13; b12; b11; b10; b9; b8; 654 b7; b6; b5; b4; b3; b2; b1; b0]: word16) = 655 v2w [b7; b6; b5; b4; b3; b2; b1; b0]: word8)`, 656 blastLib.BBLAST_TAC 657 ) 658 659val concat_bytes = Q.store_thm("concat_bytes", 660 `!w: word32. (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w = w`, 661 blastLib.BBLAST_TAC 662 ) 663 664val reverse_endian_bytes = Q.store_thm("reverse_endian_bytes", 665 `!w: word32. 666 ((7 >< 0) (reverse_endian w) = (31 >< 24) w) /\ 667 ((15 >< 8) (reverse_endian w) = (23 >< 16) w) /\ 668 ((23 >< 16) (reverse_endian w) = (15 >< 8) w) /\ 669 ((31 >< 24) (reverse_endian w) = (7 >< 0) w)`, 670 rw [reverse_endian_def] 671 \\ blastLib.BBLAST_TAC 672 ) 673 674val reverse_endian_id = Q.store_thm("reverse_endian_id", 675 `!w. reverse_endian (reverse_endian w) = w`, 676 rw [reverse_endian_def, reverse_endian_bytes, concat_bytes] 677 ) 678 679(* ------------------------------------------------------------------------ *) 680 681val v2w_13_15_rwts = Q.store_thm("v2w_13_15_rwts", 682 `((v2w [F; b2; b1; b0] = 13w: word4) = F) /\ 683 ((v2w [b2; F; b1; b0] = 13w: word4) = F) /\ 684 ((v2w [b2; b1; T; b0] = 13w: word4) = F) /\ 685 ((v2w [b2; b1; b0; F] = 13w: word4) = F) /\ 686 ((v2w [F; b2; b1; b0] = 15w: word4) = F) /\ 687 ((v2w [b2; F; b1; b0] = 15w: word4) = F) /\ 688 ((v2w [b2; b1; F; b0] = 15w: word4) = F) /\ 689 ((v2w [b2; b1; b0; F] = 15w: word4) = F)`, 690 blastLib.BBLAST_TAC) 691 692fun enumerate_v2w n = 693 let 694 open Arbnum 695 val m = toInt (pow (two, fromInt n)) 696 in 697 List.tabulate 698 (m, fn i => bitstringLib.v2w_n2w_CONV 699 (bitstringSyntax.padded_fixedwidth_of_num 700 (Arbnum.fromInt i, n))) 701 |> Drule.LIST_CONJ 702 end 703 704val v2w_ground2 = Theory.save_thm("v2w_ground2", enumerate_v2w 2) 705val v2w_ground4 = Theory.save_thm("v2w_ground4", enumerate_v2w 4) 706 707val Decode_simp_extra = Q.prove( 708 `w2n (v2w [b2; b1; b0] : word3) = w2n (v2w [F; b2; b1; b0] : word4)`, 709 wordsLib.n2w_INTRO_TAC 4 710 \\ blastLib.BBLAST_TAC 711 ) 712 713val Decode_simps = Q.store_thm("Decode_simps", 714 `(v2w [b3; b2; b1; b0] <+ (8w: word4) = ~b3) /\ 715 (w2w (v2w [b2; b1; b0] : word3) = v2w [F; b2; b1; b0] : word4) /\ 716 ((v2w [b3] : word1) @@ v2w [b2; b1; b0] : word3 = 717 v2w [b3; b2; b1; b0] : word4) /\ 718 (w2w (v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8) = 719 v2w [F; b7; b6; b5; b4; b3; b2; b1; b0] : word9) /\ 720 (v2w [b4; b3; b2; b1; b0] : word5 @@ (0w: word1) = 721 v2w [b4; b3; b2; b1; b0; F] : word6) /\ 722 (v2w [b4; b3; b2; b1; b0] : word5 @@ (0w: word2) = 723 v2w [b4; b3; b2; b1; b0; F; F] : word7) /\ 724 (v2w [b6; b5; b4; b3; b2; b1; b0] : word7 @@ (0w: word2) = 725 v2w [b6; b5; b4; b3; b2; b1; b0; F; F] : word9) /\ 726 (v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8 @@ (0w: word1) = 727 v2w [b7; b6; b5; b4; b3; b2; b1; b0; F] : word9) /\ 728 (v2w [b7; b6; b5; b4; b3; b2; b1; b0] : word8 @@ (0w: word2) = 729 v2w [b7; b6; b5; b4; b3; b2; b1; b0; F; F] : word10) /\ 730 (v2w [b10; b9; b8; b7; b6; b5; b4; b3; b2; b1; b0] : word11 @@ (0w: word1) = 731 v2w [b10; b9; b8; b7; b6; b5; b4; b3; b2; b1; b0; F] : word12) 732 `, 733 lrw [] 734 \\ blastLib.BBLAST_TAC 735 ) 736 737val Decode_simps = Theory.save_thm ("Decode_simps", 738 ([Decode_simp_extra, Decode_simps] @ 739 List.tabulate 740 (8, fn i => let 741 val w = wordsSyntax.mk_wordii (i, 3) 742 in 743 blastLib.BBLAST_CONV ``v2w [a; b; c] = ^w`` 744 end)) |> Drule.LIST_CONJ) 745 746val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt", 747 `!imm2 w C s. 748 Shift_C (w: word32, SRType_LSL, imm2, C) s = 749 ((w << imm2, if imm2 = 0 then C else testbit 32 (shiftl (w2v w) imm2)), 750 s)`, 751 lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F]) 752 753local 754 val lem = 755 (SIMP_RULE (srw_ss()) [] o Q.SPECL [`v`, `32`] o 756 Thm.INST_TYPE [Type.alpha |-> ``:33``]) bitstringTheory.word_index_v2w 757in 758 val shift32 = Q.prove( 759 `!w:word32 imm. 760 ((w2w w : 33 word) << imm) ' 32 = testbit 32 (shiftl (w2v w) imm)`, 761 strip_tac 762 \\ bitstringLib.Cases_on_v2w `w` 763 \\ fs [bitstringTheory.w2v_v2w, bitstringTheory.w2w_v2w, 764 bitstringTheory.word_lsl_v2w, bitstringTheory.word_index_v2w, 765 lem, markerTheory.Abbrev_def]) 766end 767 768val Shift_C_LSL_rwt = Q.store_thm("Shift_C_LSL_rwt", 769 `!imm2 w C s. 770 Shift_C (w: word32, SRType_LSL, imm2, C) s = 771 ((w << imm2, if imm2 = 0 then C else ((w2w w : 33 word) << imm2) ' 32), 772 s)`, 773 lrw [Shift_C_def, LSL_C_def, bitstringTheory.shiftl_replicate_F, shift32] 774 ) 775 776val Shift_C_DecodeImmShift_rwt = Q.prove( 777 `!typ imm5 w C s. 778 Shift_C (w: word32, 779 FST (DecodeImmShift (typ, imm5)), 780 SND (DecodeImmShift (typ, imm5)), 781 C) s = 782 let amount = w2n imm5 in 783 (if typ = 0w 784 then if imm5 = 0w 785 then (w, C) 786 else (w << amount, ((w2w w : 33 word) << amount) ' 32) 787 else if typ = 1w 788 then if imm5 = 0w 789 then (0w, word_msb w) 790 else (w >>> amount, amount <= 32 /\ word_bit (amount - 1) w) 791 else if typ = 2w 792 then if imm5 = 0w 793 then (w >> 32, word_msb w) 794 else (w >> amount, word_bit (MIN 32 amount - 1) w) 795 else if imm5 = 0w 796 then SWAP (word_rrx (C, w)) 797 else (w #>> amount, word_msb (w #>> amount)), s)`, 798 strip_tac 799 \\ wordsLib.Cases_on_word_value `typ` 800 \\ simp [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def, 801 DecodeImmShift_def, pairTheory.SWAP_def, shift32] 802 \\ lrw [wordsTheory.word_rrx_def, wordsTheory.word_bit_def, 803 wordsTheory.word_msb_def, wordsTheory.word_lsb_def, 804 bitstringTheory.shiftl_replicate_F] 805 \\ fs [] 806 \\ blastLib.BBLAST_TAC 807 \\ simp [bitstringTheory.testbit, bitstringTheory.el_field, 808 bitstringTheory.el_w2v]) 809 |> Q.SPEC `v2w [a; b]: word2` 810 |> Conv.CONV_RULE 811 (Conv.STRIP_QUANT_CONV 812 (Conv.RHS_CONV 813 (pairLib.let_CONV 814 THENC Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV))) 815 |> Drule.GEN_ALL 816 |> save_as "Shift_C_DecodeImmShift_rwt" 817 818val Shift_C_DecodeRegShift_rwt = Q.prove( 819 `!typ amount w C s. 820 Shift_C (w: word32, DecodeRegShift typ, amount, C) s = 821 (if typ = 0w 822 then (w << amount, 823 if amount = 0 then C else ((w2w w : 33 word) << amount) ' 32) 824 else if typ = 1w 825 then (w >>> amount, 826 if amount = 0 then C 827 else amount <= 32 /\ word_bit (amount - 1) w) 828 else if typ = 2w 829 then (w >> amount, 830 if amount = 0 then C else word_bit (MIN 32 amount - 1) w) 831 else (w #>> amount, 832 if amount = 0 then C else word_msb (w #>> amount)), s)`, 833 strip_tac 834 \\ wordsLib.Cases_on_word_value `typ` 835 \\ simp [Shift_C_def, LSL_C_def, LSR_C_def, ASR_C_def, ROR_C_def, RRX_C_def, 836 DecodeRegShift_def, shift32] 837 \\ lrw [wordsTheory.word_bit_def, bitstringTheory.shiftl_replicate_F, 838 wordsTheory.word_msb_def, wordsTheory.word_lsb_def] 839 \\ fs []) 840 |> Q.SPEC `v2w [a; b]: word2` 841 |> Conv.CONV_RULE 842 (Conv.STRIP_QUANT_CONV 843 (Conv.RHS_CONV (Conv.DEPTH_CONV bitstringLib.v2w_eq_CONV))) 844 |> Drule.GEN_ALL 845 |> save_as "Shift_C_DecodeRegShift_rwt" 846 847val DecodeRegShift_rwt = Theory.save_thm ("DecodeRegShift_rwt", 848 utilsLib.map_conv (REWRITE_CONV [DecodeRegShift_def] THENC EVAL) 849 [``DecodeRegShift 0w``, ``DecodeRegShift 1w``, 850 ``DecodeRegShift 2w``, ``DecodeRegShift 3w``]) 851 852val FST_SWAP = Q.store_thm("FST_SWAP", 853 `!x. FST (SWAP x) = SND x`, 854 Cases \\ simp [pairTheory.SWAP_def] 855 ) 856 857(* ------------------------------------------------------------------------ *) 858 859local 860 val t = ``LDM_UPTO f i r (b, s)`` 861in 862 val LDM_UPTO_components = 863 Drule.LIST_CONJ 864 (List.map (GEN_ALL o SIMP_CONV (srw_ss()) [LDM_UPTO_def]) 865 [``FST ^t``, ``(SND ^t).MEM``, ``(SND ^t).CONTROL``, 866 ``(SND ^t).AIRCR``]) 867 |> save_as "LDM_UPTO_components" 868end 869 870local 871 val LDM1_PC = Q.prove( 872 `!n p b registers s r. 873 n < 15 ==> (LDM1 (R_name p) b registers s r n RName_PC = r RName_PC)`, 874 REPEAT strip_tac 875 \\ RULE_ASSUM_TAC (Conv.CONV_RULE wordsLib.LESS_CONV) 876 \\ full_simp_tac bool_ss [] 877 \\ fs [R_name_def, LDM1_def, combinTheory.UPDATE_def] 878 \\ lrw []) 879in 880 val LDM_UPTO_PC = Q.store_thm("LDM_UPTO_PC", 881 `!p b r s. FOLDL (LDM1 (R_name p) b r s) s.REG (COUNT_LIST 8) RName_PC = 882 s.REG RName_PC`, 883 rw [EVAL ``COUNT_LIST 8``, LDM1_PC]) 884end 885 886val LDM_UPTO_RUN = Q.store_thm("LDM_UPTO_RUN", 887 `!l f b r s w reg. 888 FOLDL (LDM1 f b r (s with pcinc := w)) reg l = 889 FOLDL (LDM1 f b r s) reg l`, 890 Induct \\ lrw [LDM1_def]); 891 892local 893 val rearrange = Q.prove( 894 `(b + if P then 4w else 0w, 895 s with REG := (if P then (x =+ y) else I) s.REG) = 896 (if P then 897 (b + 4w, s with REG := (x =+ y) s.REG) 898 else 899 (b, s))`, 900 lrw [updateTheory.APPLY_UPDATE_ID] \\ lrw [m0_state_component_equality]) 901 |> Drule.GEN_ALL 902in 903 val LDM_UPTO_0 = 904 ``LDM_UPTO f 0 registers (b, s)`` 905 |> SIMP_CONV (srw_ss()++boolSimps.LET_ss) 906 [bit_count_upto_1, LDM_UPTO_def, LDM1_def, EVAL ``COUNT_LIST 1``, 907 rearrange] 908 |> Conv.GSYM 909 |> save_as "LDM_UPTO_0" 910end 911 912val LDM_UPTO_SUC = 913 Q.prove( 914 `!n f registers b s. 915 n < 8 ==> 916 ((let x = LDM_UPTO f n registers (b, s) in 917 if word_bit (SUC n) registers then 918 (FST x + 4w, 919 SND x with REG := LDM1 f b registers s ((SND x).REG) (SUC n)) 920 else 921 x) = LDM_UPTO f (SUC n) registers (b, s))`, 922 lrw [LDM_UPTO_def, DECIDE ``SUC n + 1 = SUC (n + 1)``, 923 wordsTheory.bit_count_upto_def, sum_numTheory.SUM_def, 924 wordsTheory.WORD_MULT_SUC, wordsTheory.word_bit_def] 925 \\ RULE_ASSUM_TAC (REWRITE_RULE [arithmeticTheory.ADD1]) 926 \\ fs [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC, 927 GSYM arithmeticTheory.ADD1] 928 \\ CONV_TAC (Conv.RHS_CONV (ONCE_REWRITE_CONV [LDM1_def])) 929 \\ simp [wordsTheory.word_bit_def]) 930 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) 931 [numTheory.NOT_SUC, arithmeticTheory.SUC_SUB1, LDM1_def, 932 LDM_UPTO_components] 933 |> save_as "LDM_UPTO_SUC" 934 935(* ------------------------------------------------------------------------ *) 936 937val STM_UPTO_components = 938 Drule.LIST_CONJ 939 (List.map (GEN_ALL o SIMP_CONV (srw_ss()) [STM_UPTO_def] o Parse.Term) 940 [`FST (STM_UPTO f i r (b, s))`, 941 `(SND (STM_UPTO f i r (b, s))).REG`, 942 `(SND (STM_UPTO f i r (b, s))).CONTROL`, 943 `(SND (STM_UPTO f i r (b, s))).AIRCR`]) 944 |> save_as "STM_UPTO_components" 945 946val STM_UPTO_RUN = Q.store_thm("STM_UPTO_RUN", 947 `!l f b r s w mem. 948 FOLDL (STM1 f b r (s with pcinc := w)) mem l = 949 FOLDL (STM1 f b r s) mem l`, 950 Induct \\ lrw [STM1_def]); 951 952local 953 val rearrange = Q.prove( 954 `(b + if P then 4w else 0w, 955 s with MEM := (if P then x else I) s.MEM) = 956 (if P then 957 (b + 4w, s with MEM := x s.MEM) 958 else 959 (b, s))`, 960 lrw [updateTheory.APPLY_UPDATE_ID] \\ lrw [m0_state_component_equality]) 961 |> Drule.GEN_ALL 962in 963 val STM_UPTO_0 = 964 ``STM_UPTO f 0 registers (b, s)`` 965 |> SIMP_CONV (srw_ss()++boolSimps.LET_ss) 966 [bit_count_upto_1, STM_UPTO_def, STM1_def, EVAL ``COUNT_LIST 1``, 967 rearrange] 968 |> Conv.GSYM 969 |> save_as "STM_UPTO_0" 970end 971 972val STM_UPTO_SUC = 973 Q.prove( 974 `!n f registers:'a word b s. 975 n < dimindex(:'a) - 1 ==> 976 ((let x = STM_UPTO f n registers (b, s) in 977 if word_bit (SUC n) registers then 978 (FST x + 4w, 979 SND x with MEM := STM1 f b registers s ((SND x).MEM) (SUC n)) 980 else 981 x) = STM_UPTO f (SUC n) registers (b, s))`, 982 lrw [STM_UPTO_def, DECIDE ``SUC n + 1 = SUC (n + 1)``, 983 wordsTheory.bit_count_upto_def, sum_numTheory.SUM_def, 984 wordsTheory.WORD_MULT_SUC, wordsTheory.word_bit_def] 985 \\ RULE_ASSUM_TAC (REWRITE_RULE [arithmeticTheory.ADD1]) 986 \\ fs [rich_listTheory.COUNT_LIST_SNOC, listTheory.FOLDL_SNOC, 987 GSYM arithmeticTheory.ADD1] 988 \\ CONV_TAC (Conv.RHS_CONV (ONCE_REWRITE_CONV [STM1_def])) 989 \\ simp [wordsTheory.word_bit_def] 990 ) 991 |> SIMP_RULE (bool_ss++boolSimps.LET_ss) 992 [numTheory.NOT_SUC, arithmeticTheory.SUC_SUB1, STM1_def, 993 STM_UPTO_components, combinTheory.o_THM] 994 |> save_as "STM_UPTO_SUC" 995 996val bit_count_9_m_8 = Q.store_thm("bit_count_9_m_8", 997 `!r: word9. word_bit 8 r ==> (bit_count_upto 8 r = bit_count r - 1)`, 998 lrw [wordsTheory.bit_count_def, wordsTheory.word_bit_def, 999 wordsTheory.bit_count_upto_SUC 1000 |> Q.ISPECL [`r:word9`, `8`] 1001 |> numLib.REDUCE_RULE 1002 ] 1003 ) 1004 1005val word_bit_9_expand = Q.store_thm("word_bit_9_expand", 1006 `!a: word4. 1007 word_bit (w2n a) (v2w [F; b7; b6; b5; b4; b3; b2; b1; b0] : word9) = 1008 b7 /\ (a = 7w) \/ b6 /\ (a = 6w) \/ b5 /\ (a = 5w) \/ b4 /\ (a = 4w) \/ 1009 b3 /\ (a = 3w) \/ b2 /\ (a = 2w) \/ b1 /\ (a = 1w) \/ b0 /\ (a = 0w)`, 1010 simp [bitstringTheory.bit_v2w] 1011 \\ wordsLib.Cases_word_value 1012 \\ simp [bitstringTheory.testbit_el] 1013 ) 1014 1015(* ------------------------------------------------------------------------ *) 1016 1017val () = export_theory () 1018