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 arm8Theory 10 11val _ = new_theory "arm8_step" 12 13(* ------------------------------------------------------------------------ *) 14 15val _ = List.app (fn f => f ()) 16 [numLib.prefer_num, wordsLib.prefer_word, wordsLib.guess_lengths] 17 18(* ------------------------------------------------------------------------ *) 19 20val NextStateARM8_def = Define` 21 NextStateARM8 s0 = 22 let s1 = Next s0 in if s1.exception = NoException then SOME s1 else NONE` 23 24val NextStateARM8 = ustore_thm("NextStateARM8", 25 `(s.exception = NoException) ==> 26 (Fetch (s with branch_hint := NONE) = (w, s with branch_hint := NONE)) /\ 27 (Decode w = ast) /\ 28 (!s. Run ast s = f x s) /\ 29 (f x (s with branch_hint := NONE) = s1) /\ 30 (s1.exception = s.exception) ==> 31 (NextStateARM8 s = SOME (if s1.branch_hint = NONE then 32 s1 with <| PC := s1.PC + 4w |> 33 else s1))`, 34 lrw [NextStateARM8_def, Next_def] 35 ) 36 37(* ------------------------------------------------------------------------ *) 38 39val mem_half_def = Define` 40 mem_half (m:word64 -> word8) a = (m (a + 1w) @@ m a) : word16` 41 42val mem_word_def = Define` 43 mem_word (m:word64 -> word8) a = 44 (m (a + 3w) @@ m (a + 2w) @@ m (a + 1w) @@ m a) : word32` 45 46val mem_dword_def = Define` 47 mem_dword (m:word64 -> word8) a = 48 (m (a + 7w) @@ m (a + 6w) @@ m (a + 5w) @@ m (a + 4w) @@ 49 m (a + 3w) @@ m (a + 2w) @@ m (a + 1w) @@ m a) : word64` 50 51(* ------------------------------------------------------------------------ *) 52 53fun concat_tac l = 54 ntac (List.length l) strip_tac 55 \\ map_every bitstringLib.Cases_on_v2w l 56 \\ lfs [markerTheory.Abbrev_def] 57 \\ REPEAT (once_rewrite_tac [bitstringTheory.word_concat_v2w_rwt] 58 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.fixwidth_id_imp]) 59 60val concat16 = Q.store_thm("concat16", 61 `!w1:word8 w2:word8. w2v w1 ++ w2v w2 = w2v (w1 @@ w2)`, 62 concat_tac [`w1`,`w2`] 63 ) 64 65val concat32 = Q.store_thm("concat32", 66 `!w1:word8 w2:word8 w3:word16. 67 w2v w1 ++ (w2v w2 ++ w2v w3) = w2v (w1 @@ w2 @@ w3)`, 68 concat_tac [`w1`,`w2`,`w3`] 69 ) 70 71val concat64 = Q.store_thm("concat64", 72 `!w1:word8 w2:word8 w3:word8 w4:word8 w5:word32. 73 w2v w1 ++ (w2v w2 ++ (w2v w3 ++ (w2v w4 ++ w2v w5))) = 74 w2v (w1 @@ w2 @@ w3 @@ w4 @@ w5)`, 75 concat_tac [`w1`,`w2`,`w3`,`w4`,`w5`] 76 ) 77 78val fields = Q.store_thm("fields", 79 `(!w:word8. v2w (field 7 0 (w2v w)) = w) /\ 80 (!w:word16. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 81 (!w:word16. v2w (field 7 0 (w2v w)) = ( 7 >< 0) w : word8) /\ 82 (!w:word32. v2w (field 31 24 (w2v w)) = (31 >< 24) w : word8) /\ 83 (!w:word32. v2w (field 23 16 (w2v w)) = (23 >< 16) w : word8) /\ 84 (!w:word32. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 85 (!w:word32. v2w (field 7 0 (w2v w)) = ( 7 >< 0) w : word8) /\ 86 (!w:word64. v2w (field 63 56 (w2v w)) = (63 >< 56) w : word8) /\ 87 (!w:word64. v2w (field 55 48 (w2v w)) = (55 >< 48) w : word8) /\ 88 (!w:word64. v2w (field 47 40 (w2v w)) = (47 >< 40) w : word8) /\ 89 (!w:word64. v2w (field 39 32 (w2v w)) = (39 >< 32) w : word8) /\ 90 (!w:word64. v2w (field 31 24 (w2v w)) = (31 >< 24) w : word8) /\ 91 (!w:word64. v2w (field 23 16 (w2v w)) = (23 >< 16) w : word8) /\ 92 (!w:word64. v2w (field 15 8 (w2v w)) = (15 >< 8) w : word8) /\ 93 (!w:word64. v2w (field 7 0 (w2v w)) = ( 7 >< 0) w : word8)`, 94 REPEAT strip_tac 95 \\ bitstringLib.Cases_on_v2w `w` 96 \\ simp [bitstringTheory.w2v_v2w, bitstringTheory.word_extract_v2w, 97 bitstringTheory.word_bits_v2w, bitstringTheory.w2w_v2w] 98 \\ fs [markerTheory.Abbrev_def, bitstringTheory.field_id_imp] 99 ) 100 101val get_bytes = Q.store_thm("get_bytes", 102 `((31 >< 24) 103 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 104 b23; b22; b21; b20; b19; b18; b17; b16; 105 b15; b14; b13; b12; b11; b10; b9; b8; 106 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 107 v2w [b31; b30; b29; b28; b27; b26; b25; b24]: word8) /\ 108 ((23 >< 16) 109 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 110 b23; b22; b21; b20; b19; b18; b17; b16; 111 b15; b14; b13; b12; b11; b10; b9; b8; 112 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 113 v2w [b23; b22; b21; b20; b19; b18; b17; b16]: word8) /\ 114 ((15 >< 8) 115 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 116 b23; b22; b21; b20; b19; b18; b17; b16; 117 b15; b14; b13; b12; b11; b10; b9; b8; 118 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 119 v2w [b15; b14; b13; b12; b11; b10; b9; b8]: word8) /\ 120 ((7 >< 0) 121 (v2w [b31; b30; b29; b28; b27; b26; b25; b24; 122 b23; b22; b21; b20; b19; b18; b17; b16; 123 b15; b14; b13; b12; b11; b10; b9; b8; 124 b7; b6; b5; b4; b3; b2; b1; b0]: word32) = 125 v2w [b7; b6; b5; b4; b3; b2; b1; b0]: word8)`, 126 blastLib.BBLAST_TAC 127 ) 128 129val bit_field_insert_thms = Theory.save_thm("bit_field_insert_thms", 130 utilsLib.map_conv blastLib.BBLAST_PROVE 131 [ 132 ``!a b. bit_field_insert 15 0 (a: word16) (b: word32) = 133 (31 >< 16) b @@ a``, 134 ``!a b. bit_field_insert 31 16 (a: word16) (b: word32) = 135 a @@ (15 >< 0) b``, 136 ``!a b. bit_field_insert 15 0 (a: word16) (b: word64) = 137 (63 >< 16) b @@ a``, 138 ``!a b. bit_field_insert 31 16 (a: word16) (b: word64) = 139 (63 >< 32) b @@ a @@ ((15 >< 0) b)``, 140 ``!a b. bit_field_insert 47 32 (a: word16) (b: word64) = 141 (63 >< 48) b @@ a @@ ((31 >< 0) b)``, 142 ``!a b. bit_field_insert 63 48 (a: word16) (b: word64) = 143 a @@ ((47 >< 0) b)`` 144 ] 145 ) 146 147val concat_bytes = Q.store_thm("concat_bytes", 148 `(!w: word32. 149 (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w = w) /\ 150 (!w: word32 v: word32. 151 (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w @@ v = 152 w @@ v) /\ 153 (!w: word64. 154 (63 >< 56) w @@ (55 >< 48) w @@ (47 >< 40) w @@ (39 >< 32) w @@ 155 (31 >< 24) w @@ (23 >< 16) w @@ (15 >< 8) w @@ (7 >< 0) w = w)`, 156 blastLib.BBLAST_TAC 157 ) 158 159(* ------------------------------------------------------------------------ *) 160 161val notoverflow = METIS_PROVE [integer_wordTheory.overflow] 162 ``!x y. (word_msb x = word_msb (x + y)) ==> (w2i (x + y) = w2i x + w2i y)`` 163 164val word_msb_sum1a = Q.prove( 165 `!x y. (word_msb x = word_msb y) /\ word_msb (x + y) ==> 166 word_msb (x + y + 1w)`, 167 Cases \\ Cases 168 \\ lrw [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 169 \\ Cases_on `INT_MIN (:'a) <= n` 170 \\ Cases_on `INT_MIN (:'a) <= n'` 171 \\ lfs [] 172 >- (imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 173 \\ pop_assum (K all_tac) 174 \\ `p < INT_MIN (:'a) /\ p' < INT_MIN (:'a)` 175 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 176 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 177 \\ `(p + (p' + (dimword (:'a) + 1)) = dimword (:'a) + (p + p' + 1)) /\ 178 (p + (p' + dimword (:'a)) = dimword (:'a) + (p + p'))` by lrw [] 179 \\ pop_assum SUBST_ALL_TAC \\ pop_assum SUBST1_TAC 180 \\ full_simp_tac bool_ss 181 [arithmeticTheory.ADD_MODULUS_RIGHT, wordsTheory.ZERO_LT_dimword] 182 \\ `p + p' + 1 < dimword (:'a)` 183 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 184 \\ lfs []) 185 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 186 \\ `n + n' + 1 < dimword (:'a)` 187 by lrw [wordsTheory.dimword_IS_TWICE_INT_MIN] 188 \\ lfs [] 189 ) 190 191val word_msb_sum1b = Q.prove( 192 `!x y. (word_msb x <> word_msb y) /\ ~word_msb (x + y) ==> 193 (word_msb (x + y) = word_msb (x + y + 1w))`, 194 Cases \\ Cases 195 \\ simp_tac std_ss 196 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_add_n2w] 197 \\ lrw [] 198 \\ Cases_on `n < INT_MIN (:'a)` 199 \\ Cases_on `n' < INT_MIN (:'a)` 200 \\ lfs [arithmeticTheory.NOT_LESS, arithmeticTheory.NOT_LESS_EQUAL] 201 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 202 \\ lfs [arithmeticTheory.NOT_LESS] 203 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 204 \\ pop_assum (K all_tac) 205 \\ `p < INT_MIN (:'a)` by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 206 \\ lrw [arithmeticTheory.ADD_MODULUS_LEFT] 207 ) 208 209val word_msb_sum1c = Q.prove( 210 `!x y. word_msb (x + y + 1w) /\ ~word_msb (x + y) ==> (x + y = INT_MAXw)`, 211 Cases \\ Cases 212 \\ `INT_MIN (:'a) - 1 < dimword (:'a)` 213 by (assume_tac wordsTheory.INT_MIN_LT_DIMWORD \\ decide_tac) 214 \\ simp_tac std_ss 215 [wordsTheory.word_msb_n2w_numeric, wordsTheory.word_H_def, 216 wordsTheory.INT_MAX_def, wordsTheory.word_add_n2w] 217 \\ lrw [] 218 \\ lfs [arithmeticTheory.NOT_LESS_EQUAL] 219 \\ Cases_on `n + (n' + 1) < dimword (:'a)` 220 \\ lfs [arithmeticTheory.NOT_LESS] 221 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 222 \\ pop_assum (K all_tac) 223 \\ `p < dimword (:'a)` by lfs [] 224 \\ Cases_on `n + n' < dimword (:'a)` 225 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT, arithmeticTheory.NOT_LESS] 226 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 227 \\ pop_assum (K all_tac) 228 \\ lfs [arithmeticTheory.ADD_MODULUS_LEFT] 229 ) 230 231val AddWithCarry = Q.store_thm("AddWithCarry", 232 `!x y carry_in. 233 AddWithCarry (x,y,carry_in) = 234 let (r, c, v) = add_with_carry (x,y,carry_in) in 235 (r, word_msb r, r = 0w, c, v)`, 236 REPEAT strip_tac 237 \\ simp [AddWithCarry_def, wordsTheory.add_with_carry_def] 238 \\ simp [GSYM wordsTheory.word_add_n2w] 239 \\ Cases_on `carry_in` 240 \\ simp [integer_wordTheory.overflow] 241 \\ Cases_on `dimindex(:'a) = 1` 242 >- (imp_res_tac wordsTheory.dimindex_1_cases 243 \\ pop_assum (fn th => (strip_assume_tac (Q.SPEC `x` th) 244 \\ strip_assume_tac (Q.SPEC `y` th))) 245 \\ simp [wordsTheory.word_index, wordsTheory.word_msb_def, 246 wordsTheory.word_2comp_def, integer_wordTheory.w2i_def, 247 wordsTheory.dimword_def]) 248 \\ Cases_on `word_msb (x + y) <> word_msb (1w : 'a word)` 249 \\ `~word_msb 1w` 250 by lrw [wordsTheory.word_msb_n2w, DECIDE ``0n < n /\ n <> 1 ==> ~(n <= 1)``] 251 \\ fs [integer_wordTheory.different_sign_then_no_overflow, 252 integer_wordTheory.overflow, integer_wordTheory.w2i_1] 253 >- (Cases_on `word_msb x <=> word_msb y` \\ simp [word_msb_sum1a]) 254 \\ Cases_on `word_msb x = word_msb y` 255 \\ simp [GSYM integer_wordTheory.different_sign_then_no_overflow] 256 >- (Cases_on `word_msb (x + y + 1w)` 257 \\ lfs [notoverflow, integer_wordTheory.w2i_1] 258 >- (imp_res_tac word_msb_sum1c 259 \\ lfs [integer_wordTheory.w2i_INT_MINw] 260 \\ Cases_on `x` 261 \\ Cases_on `y` 262 \\ lfs [wordsTheory.word_msb_n2w_numeric] 263 \\ Cases_on `INT_MIN (:'a) <= n'` 264 \\ lfs [integer_wordTheory.w2i_n2w_pos, 265 integer_wordTheory.w2i_n2w_neg, 266 wordsTheory.word_add_n2w, 267 wordsTheory.word_L_def, 268 wordsTheory.word_2comp_def, 269 integerTheory.INT_ADD_CALCULATE] 270 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 271 \\ `p + p' < dimword (:'a)` 272 by lfs [wordsTheory.dimword_IS_TWICE_INT_MIN] 273 \\ lfs [GSYM wordsTheory.dimword_IS_TWICE_INT_MIN] 274 \\ `(p + (p' + dimword (:'a)) = (p + p') + dimword (:'a)) /\ 275 (INT_MIN (:'a) + dimword (:'a) - 1 = 276 dimword (:'a) + (INT_MIN (:'a) - 1))` 277 by lfs [] 278 \\ ntac 2 (pop_assum SUBST_ALL_TAC) 279 \\ full_simp_tac bool_ss 280 [arithmeticTheory.ADD_MODULUS_LEFT, 281 arithmeticTheory.ADD_MODULUS_RIGHT, 282 wordsTheory.ZERO_LT_dimword] 283 \\ lfs [wordsTheory.BOUND_ORDER] 284 \\ metis_tac [arithmeticTheory.ADD_ASSOC, 285 wordsTheory.dimword_sub_int_min, 286 wordsTheory.ZERO_LT_INT_MIN, 287 DECIDE ``0n < n ==> (n - 1 + 1 = n)``]) 288 \\ metis_tac [integer_wordTheory.overflow, integer_wordTheory.w2i_1]) 289 \\ `word_msb (x + y) <=> word_msb (x + y + 1w)` by imp_res_tac word_msb_sum1b 290 \\ simp [notoverflow, integer_wordTheory.w2i_1] 291 ) 292 293val nzcv = Term.mk_var ("nzcv", ``:bool # bool # bool # bool``) 294 295val SetTheFlags = Theory.save_thm("SetTheFlags", 296 SetTheFlags_def 297 |> Q.SPECL [`setflags`, `FST ^nzcv`, `FST (SND ^nzcv)`, 298 `FST (SND (SND ^nzcv))`, `SND (SND (SND ^nzcv))`] 299 |> SIMP_RULE std_ss [] 300 ) 301 302(* ------------------------------------------------------------------------ *) 303 304val Replicate_32_64 = Q.store_thm("Replicate_32_64", 305 `(!b. Replicate [b] = if b then 0xFFFFFFFFw else 0w: word32) /\ 306 (!b. Replicate [b] = if b then 0xFFFFFFFFFFFFFFFFw else 0w: word64)`, 307 rw [Replicate_def] \\ EVAL_TAC 308 ) 309 310val ConditionTest = Theory.save_thm("ConditionTest", 311 utilsLib.map_conv 312 (REWRITE_CONV [ConditionTest_def] THENC wordsLib.WORD_EVAL_CONV) 313 (List.tabulate 314 (16, fn i => 315 ``ConditionTest (^(wordsSyntax.mk_wordii (i, 4)), n, z, c, v)``)) 316 ) 317 318val ExtendWord = Theory.save_thm("ExtendWord", 319 utilsLib.map_conv (REWRITE_CONV [ExtendWord_def]) 320 [``ExtendWord (w, T)``, ``ExtendWord (w, F)``] 321 ) 322 323val ExtendValue_0 = Q.store_thm("ExtendValue_0", 324 `(!v: word64. ExtendValue (v, ExtendType_UXTX, 0) = v) /\ 325 (!v: word32. ExtendValue (w2w v, ExtendType_UXTW, 0) = w2w v: word64)`, 326 simp [ExtendValue_def, Extend_def, bitstringTheory.field_id_imp, 327 bitstringTheory.shiftl_replicate_F, bitstringTheory.replicate_def] 328 \\ blastLib.BBLAST_TAC 329 \\ simp [bitstringTheory.testbit_el, bitstringTheory.testbit_geq_len, 330 bitstringTheory.length_field, bitstringTheory.el_field, 331 bitstringTheory.el_w2v] 332 \\ blastLib.BBLAST_TAC 333 ) 334 335(* ------------------------------------------------------------------------ *) 336 337(* 338val CountLeadingZeroBits16 = Q.store_thm("CountLeadingZeroBits16", 339 `!w:word16. 340 CountLeadingZeroBits w = if w = 0w then 16 else 15 - w2n (word_log2 w)`, 341 lrw [CountLeadingZeroBits_def, HighestSetBit_def] 342 \\ `LOG2 (w2n w) < 16` 343 by metis_tac [wordsTheory.LOG2_w2n_lt, EVAL ``dimindex(:16)``] 344 \\ lrw [integer_wordTheory.w2i_def, wordsTheory.word_log2_def, 345 wordsTheory.word_msb_n2w_numeric, 346 intLib.ARITH_PROVE ``j < 16 ==> (Num (15 - &j) = 15 - j)``] 347 ) 348 349val CountLeadingZeroBits32 = Q.store_thm("CountLeadingZeroBits32", 350 `!w:word32. 351 CountLeadingZeroBits w = if w = 0w then 32 else 31 - w2n (word_log2 w)`, 352 lrw [CountLeadingZeroBits_def, HighestSetBit_def] 353 \\ `LOG2 (w2n w) < 32` 354 by metis_tac [wordsTheory.LOG2_w2n_lt, EVAL ``dimindex(:32)``] 355 \\ lrw [integer_wordTheory.w2i_def, wordsTheory.word_log2_def, 356 wordsTheory.word_msb_n2w_numeric, 357 intLib.ARITH_PROVE ``j < 32 ==> (Num (31 - &j) = 31 - j)``] 358 ) 359*) 360 361(* ------------------------------------------------------------------------ *) 362 363val Align = Q.store_thm("Align", 364 `(!w. Align (w, 1) = align 0 w) /\ 365 (!w. Align (w, 2) = align 1 w) /\ 366 (!w. Align (w, 4) = align 2 w) /\ 367 (!w. Align (w, 8) = align 3 w) /\ 368 (!w. Align (w, 16) = align 4 w)`, 369 simp [arm8Theory.Align_def, alignmentTheory.align_w2n] 370 ) 371 372val Aligned = Q.store_thm("Aligned", 373 `(!w. Aligned (w, 1) = aligned 0 w) /\ 374 (!w. Aligned (w, 2) = aligned 1 w) /\ 375 (!w. Aligned (w, 4) = aligned 2 w) /\ 376 (!w. Aligned (w, 8) = aligned 3 w) /\ 377 (!w. Aligned (w, 16) = aligned 4 w)`, 378 simp [arm8Theory.Aligned_def, Align, alignmentTheory.aligned_def, 379 boolTheory.EQ_SYM_EQ] 380 ) 381 382(* ------------------------------------------------------------------------ *) 383 384val DecodeLogicalOp = Q.store_thm("DecodeLogicalOp", 385 `!b1 b0. DecodeLogicalOp (v2w [b1; b0]) = 386 (if b1 /\ b0 \/ ~(b1 \/ b0) then LogicalOp_AND 387 else if b0 then LogicalOp_ORR 388 else LogicalOp_EOR, 389 b1 /\ b0)`, 390 REWRITE_TAC [DecodeLogicalOp_def] \\ Cases \\ Cases \\ EVAL_TAC 391 ) 392 393val DecodeRevOp = Q.store_thm("DecodeRevOp", 394 `!b1 b0. num2RevOp (w2n (v2w [b1; b0] : word2)) = 395 if b1 then if b0 then RevOp_REV64 else RevOp_REV32 396 else if b0 then RevOp_REV16 397 else RevOp_RBIT`, 398 Cases \\ Cases \\ EVAL_TAC \\ REWRITE_TAC [arm8Theory.num2RevOp_thm] 399 ) 400 401val DecodeInzeroExtend = utilsLib.ustore_thm("DecodeInzeroExtend", 402 `~(x0 /\ x1) ==> 403 ((if ~x0 /\ ~x1 then (T,T) 404 else if ~x0 /\ x1 then (F,F) 405 else if x0 /\ ~x1 then (T,F) 406 else ARB) = (~x1, ~(x0 \/ x1)))`, 407 Cases_on `x1` 408 \\ Cases_on `x0` 409 \\ EVAL_TAC 410 ) 411 412val DecodeLem = Q.store_thm("DecodeLem", 413 `(!a b c d e f g h i. 414 (if a then (if b then c else d, e, f) else (g, h, i)) = 415 (if a then if b then c else d else g, 416 if a then e else h, 417 if a then f else i)) /\ 418 (!a b. (a \/ b) /\ ~b = a /\ ~b)`, 419 rw [] \\ decide_tac 420 ) 421 422val LoadCheck = Q.store_thm("LoadCheck", 423 `!b. ((if b then MemOp_LOAD else MemOp_STORE) <> MemOp_LOAD) = ~b`, 424 rw [] 425 ) 426 427(* ------------------------------------------------------------------------ *) 428 429val cond_rand_thms = utilsLib.mk_cond_rand_thms [pairSyntax.fst_tm] 430 431fun datatype_thms thms = 432 thms @ 433 [cond_rand_thms, GSYM mem_half_def, GSYM mem_word_def, GSYM mem_dword_def] @ 434 utilsLib.datatype_rewrites true "arm8" ["arm8_state"] 435 436val DATATYPE_CONV = REWRITE_CONV (datatype_thms []) 437val HYP_DATATYPE_RULE = utilsLib.ALL_HYP_CONV_RULE DATATYPE_CONV 438 439val st = ``s: arm8_state`` 440val EV0 = utilsLib.STEP (datatype_thms, st) 441fun EV s thms c tm = utilsLib.save_as s (hd (EV0 thms c [] tm)) 442 443val EL0 = [``^st.PSTATE.EL = 0w``] 444val NOT_TBIT = [``^st.TCR_EL1.TBI1 = F``, ``^st.TCR_EL1.TBI0 = F``] 445val NOT_E0E = [``^st.SCTLR_EL1.E0E = F``] 446val NOT_SA0 = [``^st.SCTLR_EL1.SA0 = F``] 447 448(* register access *) 449 450val X_rwt = EV "X_rwt" [X_def] [] ``X n`` 451val write'X_rwt = EV "write'X_rwt" [write'X_def] [] ``write'X (n, d)`` 452 453val SP_rwt = EV "SP_rwt" [SP_def] [EL0] ``SP`` 454val write'SP_rwt = EV "write'SP_rwt" [write'SP_def] [EL0] ``write'SP d`` 455 456val BranchTo_rwt = 457 EV "BranchTo_rwt" [BranchTo_def, Hint_Branch_def] [EL0 @ NOT_TBIT] 458 ``BranchTo (target, branch_type)`` 459 460val CheckSPAlignment_rwt = 461 EV "CheckSPAlignment_rwt" [CheckSPAlignment_def, SP_rwt] 462 [EL0 @ NOT_SA0] 463 ``CheckSPAlignment`` 464 465val CheckAlignment_rwt = 466 EV "CheckAlignment_rwt" [CheckAlignment_def, SP_rwt] 467 [[``Aligned (address:word64, n)``]] 468 ``CheckAlignment (address, n, acctype, iswrite)`` 469 470val BigEndian_rwt = 471 EV "BigEndian_rwt" [BigEndian_def] [EL0 @ NOT_E0E] ``BigEndian`` 472 473(* ---------------------------- *) 474 475(* read mem *) 476 477val align_rule = 478 utilsLib.ALL_HYP_CONV_RULE 479 (SIMP_CONV std_ss [Aligned, alignmentTheory.aligned_0]) o 480 HYP_DATATYPE_RULE o hd 481 482fun mem_ev s = 483 utilsLib.save_as ("mem" ^ s) o align_rule o 484 EV0 [Mem_def, BigEndian_rwt, CheckAlignment_rwt, wordsTheory.WORD_ADD_0, 485 state_transformerTheory.FOR_def, state_transformerTheory.BIND_DEF, 486 listTheory.APPEND_NIL, bitstringTheory.v2w_w2v, 487 concat16, concat32, concat64] [] [] 488 489val mem1 = mem_ev "1" 490 ``Mem (address, 1, acctype) : arm8_state -> word8 # arm8_state`` 491 492val mem2 = mem_ev "2" 493 ``Mem (address, 2, acctype) : arm8_state -> word16 # arm8_state`` 494 495val mem4 = mem_ev "4" 496 ``Mem (address, 4, acctype) : arm8_state -> word32 # arm8_state`` 497 498val mem8 = mem_ev "8" 499 ``Mem (address, 8, acctype) : arm8_state -> word64 # arm8_state`` 500 501(* ---------------------------- *) 502 503(* write mem *) 504 505fun mem_ev s = 506 utilsLib.save_as ("write'mem" ^ s) o align_rule o 507 EV0 [write'Mem_def, BigEndian_rwt, CheckAlignment_rwt, fields, 508 state_transformerTheory.FOR_def, state_transformerTheory.BIND_DEF] [] [] 509 510val write'mem1 = mem_ev "1" ``write'Mem (d:word8, address, 1, acctype)`` 511val write'mem2 = mem_ev "2" ``write'Mem (d:word16, address, 2, acctype)`` 512val write'mem4 = mem_ev "4" ``write'Mem (d:word32, address, 4, acctype)`` 513val write'mem8 = mem_ev "8" ``write'Mem (d:word64, address, 8, acctype)`` 514 515(* ------------------------------------------------------------------------ *) 516 517val () = export_theory () 518