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