1open HolKernel boolLib bossLib
2open blastLib stateLib
3open set_sepTheory progTheory temporal_stateTheory arm_stepTheory
4
5val () = new_theory "arm_prog"
6
7(* ------------------------------------------------------------------------ *)
8
9val _ =
10   stateLib.sep_definitions "arm"
11      [["CPSR"], ["FP", "FPSCR"]]
12      [["undefined"], ["CurrentCondition"], ["Encoding"]]
13      arm_stepTheory.NextStateARM_def
14
15val arm_instr_def = Define`
16   arm_instr (a, i: word32) =
17   { (arm_c_MEM a, arm_d_word8 ((7 >< 0) i));
18     (arm_c_MEM (a + 1w), arm_d_word8 ((15 >< 8) i));
19     (arm_c_MEM (a + 2w), arm_d_word8 ((23 >< 16) i));
20     (arm_c_MEM (a + 3w), arm_d_word8 ((31 >< 24) i)) }`
21
22val ARM_MODEL_def = Define`
23   ARM_MODEL = (STATE arm_proj, NEXT_REL (=) NextStateARM, arm_instr,
24                ($= :arm_state -> arm_state -> bool), (K F: arm_state -> bool))`
25
26val ARM_IMP_SPEC = Theory.save_thm ("ARM_IMP_SPEC",
27   stateTheory.IMP_SPEC
28   |> Q.ISPECL [`arm_proj`, `NextStateARM`, `arm_instr`]
29   |> REWRITE_RULE [GSYM ARM_MODEL_def]
30   )
31
32val ARM_IMP_TEMPORAL = Theory.save_thm ("ARM_IMP_TEMPORAL",
33   temporal_stateTheory.IMP_TEMPORAL
34   |> Q.ISPECL [`arm_proj`, `NextStateARM`, `arm_instr`,
35                `(=): arm_state -> arm_state -> bool`, `K F: arm_state -> bool`]
36   |> REWRITE_RULE [GSYM ARM_MODEL_def]
37   )
38
39(* ------------------------------------------------------------------------ *)
40
41(* Aliases *)
42
43val arm_FP_REG_def = DB.definition "arm_FP_REG_def"
44val arm_REG_def = DB.definition "arm_REG_def"
45val arm_MEM_def = DB.definition "arm_MEM_def"
46
47val (arm_FP_REGISTERS_def, arm_FP_REGISTERS_INSERT) =
48   stateLib.define_map_component ("arm_FP_REGISTERS", "fpr", arm_FP_REG_def)
49
50val (arm_REGISTERS_def, arm_REGISTERS_INSERT) =
51   stateLib.define_map_component ("arm_REGISTERS", "reg", arm_REG_def)
52
53val (arm_MEMORY_def, arm_MEMORY_INSERT) =
54   stateLib.define_map_component ("arm_MEMORY", "mem", arm_MEM_def)
55
56val arm_WORD_def = Define`
57   arm_WORD a (i: word32) =
58   arm_MEM a ((7 >< 0) i) *
59   arm_MEM (a + 1w) ((15 >< 8) i) *
60   arm_MEM (a + 2w) ((23 >< 16) i) *
61   arm_MEM (a + 3w) ((31 >< 24) i)`;
62
63val arm_BE_WORD_def = Define`
64   arm_BE_WORD a (i: word32) =
65   arm_MEM a ((31 >< 24) i) *
66   arm_MEM (a + 1w) ((23 >< 16) i) *
67   arm_MEM (a + 2w) ((15 >< 8) i) *
68   arm_MEM (a + 3w) ((7 >< 0) i)`;
69
70val arm_WORD_MEMORY_def = Define`
71  arm_WORD_MEMORY dmem mem =
72  {BIGUNION { BIGUNION (arm_WORD a (mem a)) | a IN dmem /\ aligned 2 a}}`
73
74val arm_BE_WORD_MEMORY_def = Define`
75  arm_BE_WORD_MEMORY dmem mem =
76  {BIGUNION { BIGUNION (arm_BE_WORD a (mem a)) | a IN dmem /\ aligned 2 a}}`
77
78val arm_CONFIG_def = Define`
79   arm_CONFIG (vfp, arch, bigend, thumb, mode) =
80      arm_VFPExtension vfp *
81      arm_Extensions Extension_Security F *
82      arm_Architecture arch *
83      arm_exception NoException * arm_CPSR_J F *
84      arm_CPSR_E bigend * arm_CPSR_T thumb *
85      arm_CPSR_M mode * cond (GoodMode mode)`;
86
87val arm_PC_def = Define`
88   arm_PC pc = arm_REG RName_PC pc * cond (aligned 2 pc)`;
89
90val aS_def = Define `
91   aS (n,z,c,v) = arm_CPSR_N n * arm_CPSR_Z z * arm_CPSR_C c * arm_CPSR_V v`;
92
93(* ------------------------------------------------------------------------ *)
94
95val aS_HIDE = Q.store_thm("aS_HIDE",
96   `~aS = ~arm_CPSR_N * ~arm_CPSR_Z * ~arm_CPSR_C * ~arm_CPSR_V`,
97   SIMP_TAC std_ss [SEP_HIDE_def, aS_def, SEP_CLAUSES, FUN_EQ_THM]
98   \\ SIMP_TAC std_ss [SEP_EXISTS]
99   \\ METIS_TAC [aS_def, pairTheory.PAIR]
100   )
101
102val arm_CPSR_T_F = Q.store_thm("arm_CPSR_T_F",
103   `( n ==> (arm_CPSR_N T = arm_CPSR_N n)) /\
104    (~n ==> (arm_CPSR_N F = arm_CPSR_N n)) /\
105    ( z ==> (arm_CPSR_Z T = arm_CPSR_Z z)) /\
106    (~z ==> (arm_CPSR_Z F = arm_CPSR_Z z)) /\
107    ( c ==> (arm_CPSR_C T = arm_CPSR_C c)) /\
108    (~c ==> (arm_CPSR_C F = arm_CPSR_C c)) /\
109    ( v ==> (arm_CPSR_V T = arm_CPSR_V v)) /\
110    (~v ==> (arm_CPSR_V F = arm_CPSR_V v))`,
111    simp []
112    )
113
114(* ------------------------------------------------------------------------ *)
115
116val arm_PC_INTRO = Q.store_thm("arm_PC_INTRO",
117   `SPEC m (p1 * arm_PC pc) code (p2 * arm_REG RName_PC pc') ==>
118    (aligned 2 pc ==> aligned 2 pc') ==>
119    SPEC m (p1 * arm_PC pc) code (p2 * arm_PC pc')`,
120   REPEAT STRIP_TAC
121   \\ FULL_SIMP_TAC std_ss [arm_PC_def, SPEC_MOVE_COND, STAR_ASSOC, SEP_CLAUSES]
122   )
123
124val arm_TEMPORAL_PC_INTRO = Q.store_thm("arm_TEMPORAL_PC_INTRO",
125   `TEMPORAL_NEXT m (p1 * arm_PC pc) code (p2 * arm_REG RName_PC pc') ==>
126    (aligned 2 pc ==> aligned 2 pc') ==>
127    TEMPORAL_NEXT m (p1 * arm_PC pc) code (p2 * arm_PC pc')`,
128   REPEAT STRIP_TAC
129   \\ FULL_SIMP_TAC std_ss
130         [arm_PC_def, TEMPORAL_NEXT_MOVE_COND, STAR_ASSOC, SEP_CLAUSES]
131   )
132
133fun mk_addr (b, s) =
134   List.tabulate
135      (25, fn i => if i < 2 then b
136                   else Term.mk_var (s ^ Int.toString i, Type.bool))
137   |> (fn l => bitstringSyntax.mk_v2w
138                  (listSyntax.mk_list (List.rev l, Type.bool), ``:32``))
139
140val x = mk_addr (boolSyntax.T, "x")
141val y = mk_addr (boolSyntax.F, "y")
142
143val Aligned_Branch = Q.store_thm("Aligned_Branch",
144   `(aligned 2 (pc:word32) ==>
145     aligned 2 (if b then pc - (^x + 1w) else pc + ^y)) = T`,
146   rw [alignmentTheory.aligned_extract]
147   \\ blastLib.FULL_BBLAST_TAC
148   )
149
150(* ------------------------------------------------------------------------ *)
151
152val lem = Q.prove(
153  `!x. ((\s. x = s) = {x})`,
154  rewrite_tac [GSYM stateTheory.SEP_EQ_SINGLETON, set_sepTheory.SEP_EQ_def]
155  \\ simp [FUN_EQ_THM]
156  \\ REPEAT strip_tac
157  \\ eq_tac
158  \\ simp []
159  )
160
161val lem1 = Q.prove(
162   `!i. i < 4 ==> n2w i <+ (4w: word32)`,
163   simp [wordsTheory.word_lo_n2w])
164
165val lem2 = Q.prove(
166   `aligned 2 (a: word32) /\ aligned 2 b /\ x <+ 4w /\ y <+ 4w ==>
167    ((a + x = b + y) = (a = b) /\ (x = y))`,
168   simp [alignmentTheory.aligned_extract]
169   \\ blastLib.BBLAST_TAC
170   )
171
172fun thm v x y =
173   stateTheory.MAPPED_COMPONENT_INSERT
174   |> Q.ISPECL
175        [`\a:word32. aligned 2 a`, `4n`, `\a i. arm_c_MEM (a + n2w i)`,
176         `\v:word32 i. arm_d_word8 (EL i ^v)`, x, y]
177   |> Conv.CONV_RULE
178        (Conv.LAND_CONV
179            (SIMP_CONV (srw_ss())
180               [arm_MEM_def, arm_WORD_def, arm_BE_WORD_def,
181                pred_setTheory.INSERT_UNION_EQ, lem,
182                set_sepTheory.STAR_def, set_sepTheory.SPLIT_def,
183                blastLib.BBLAST_PROVE
184                   ``a <> a + 1w:word32 /\ a <> a + 2w /\ a <> a + 3w``])
185         THENC REWRITE_CONV [])
186
187val v4 = ``[( 7 ><  0) v; (15 ><  8) v;
188            (23 >< 16) v; (31 >< 24) (v:word32)]:word8 list``
189
190val be_v4 = ``[(31 >< 24) v; (23 >< 16) v;
191               (15 ><  8) v; ( 7 ><  0) (v:word32)]:word8 list``
192
193
194(* Need ``(\a. ..) c`` below for automation to work *)
195val arm_WORD_MEMORY_INSERT = Q.store_thm("arm_WORD_MEMORY_INSERT",
196   `!f df c d.
197     c IN df /\ (\a. aligned 2 a) c ==>
198     (arm_WORD c d * arm_WORD_MEMORY (df DELETE c) f =
199      arm_WORD_MEMORY df ((c =+ d) f))`,
200   match_mp_tac (thm v4 `arm_WORD` `arm_WORD_MEMORY`)
201   \\ rw [arm_WORD_MEMORY_def]
202   \\ `(i = j) = (n2w i = n2w j: word32)` by simp []
203   \\ asm_rewrite_tac []
204   \\ match_mp_tac lem2
205   \\ simp [lem1]
206   )
207
208val arm_BE_WORD_MEMORY_INSERT = Q.store_thm("arm_BE_WORD_MEMORY_INSERT",
209   `!f df c d.
210     c IN df /\ (\a. aligned 2 a) c ==>
211     (arm_BE_WORD c d * arm_BE_WORD_MEMORY (df DELETE c) f =
212      arm_BE_WORD_MEMORY df ((c =+ d) f))`,
213   match_mp_tac (thm be_v4 `arm_BE_WORD` `arm_BE_WORD_MEMORY`)
214   \\ rw [arm_BE_WORD_MEMORY_def]
215   \\ `(i = j) = (n2w i = n2w j: word32)` by simp []
216   \\ asm_rewrite_tac []
217   \\ match_mp_tac lem2
218   \\ simp [lem1]
219   )
220
221(* ------------------------------------------------------------------------ *)
222
223(*
224  Theorems for moving literal loads (e.g. ldr r1, [pc, #4]) into the code pool
225*)
226
227val arm_instr_star = Q.prove(
228   `!a w.
229       {arm_instr (a, w)} =
230       arm_MEM a ((7 >< 0) w) *
231       arm_MEM (a + 1w) ((15 >< 8) w) *
232       arm_MEM (a + 2w) ((23 >< 16) w) *
233       arm_MEM (a + 3w) ((31 >< 24) w)`,
234   srw_tac [wordsLib.WORD_ARITH_EQ_ss]
235       [pred_setTheory.INSERT_UNION_EQ, arm_instr_def, arm_MEM_def,
236        set_sepTheory.STAR_def, set_sepTheory.SPLIT_def]
237   \\ simp [boolTheory.FUN_EQ_THM]
238   \\ metis_tac []
239   )
240
241val arm_instr_star_not_disjoint = Q.prove(
242   `!a w p.
243      ~DISJOINT (arm_instr (a, w)) p ==>
244        ({p} *
245         arm_MEM a ((7 >< 0) w) *
246         arm_MEM (a + 1w) ((15 >< 8) w) *
247         arm_MEM (a + 2w) ((23 >< 16) w) *
248         arm_MEM (a + 3w) ((31 >< 24) w) = SEP_F)`,
249   rw [set_sepTheory.STAR_def, set_sepTheory.SPLIT_def,
250       arm_instr_def, arm_MEM_def, pred_setTheory.DISJOINT_DEF]
251   \\ simp [boolTheory.FUN_EQ_THM, set_sepTheory.SEP_F_def]
252   \\ Cases_on `(arm_c_MEM a,arm_d_word8 ((7 >< 0) w)) IN p`          \\ simp []
253   \\ Cases_on `(arm_c_MEM (a + 1w),arm_d_word8 ((15 >< 8) w)) IN p`  \\ simp []
254   \\ Cases_on `(arm_c_MEM (a + 2w),arm_d_word8 ((23 >< 16) w)) IN p` \\ simp []
255   \\ Cases_on `(arm_c_MEM (a + 3w),arm_d_word8 ((31 >< 24) w)) IN p` \\ simp []
256   \\ fs [pred_setTheory.INSERT_INTER]
257   )
258
259val MOVE_TO_TEMPORAL_ARM_CODE_POOL = Q.store_thm
260  ("MOVE_TO_TEMPORAL_ARM_CODE_POOL",
261   `!a w c p q.
262       TEMPORAL_NEXT ARM_MODEL
263        (p *
264         arm_MEM a ((7 >< 0) w) *
265         arm_MEM (a + 1w) ((15 >< 8) w) *
266         arm_MEM (a + 2w) ((23 >< 16) w) *
267         arm_MEM (a + 3w) ((31 >< 24) w))
268        c
269        (q *
270         arm_MEM a ((7 >< 0) w) *
271         arm_MEM (a + 1w) ((15 >< 8) w) *
272         arm_MEM (a + 2w) ((23 >< 16) w) *
273         arm_MEM (a + 3w) ((31 >< 24) w)) =
274       TEMPORAL_NEXT ARM_MODEL
275        (cond (DISJOINT (arm_instr (a, w)) (BIGUNION (IMAGE arm_instr c))) * p)
276        ((a, w) INSERT c)
277        q`,
278    REPEAT strip_tac
279    \\ once_rewrite_tac [GSYM temporal_stateTheory.TEMPORAL_NEXT_CODE]
280    \\ rewrite_tac [ARM_MODEL_def, stateTheory.CODE_POOL,
281                    pred_setTheory.IMAGE_INSERT,
282                    pred_setTheory.IMAGE_EMPTY,
283                    pred_setTheory.BIGUNION_INSERT,
284                    pred_setTheory.BIGUNION_EMPTY]
285    \\ Cases_on `DISJOINT (arm_instr (a, w)) (BIGUNION (IMAGE arm_instr c))`
286    \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES,
287           temporal_stateTheory.TEMPORAL_NEXT_FALSE_PRE,
288           AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM]
289    \\ imp_res_tac arm_instr_star_not_disjoint
290    \\ fs [set_sepTheory.SEP_CLAUSES,
291           temporal_stateTheory.TEMPORAL_NEXT_FALSE_PRE,
292           AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM]
293    )
294
295val MOVE_TO_ARM_CODE_POOL = Q.store_thm("MOVE_TO_ARM_CODE_POOL",
296   `!a w c p q.
297       SPEC ARM_MODEL
298        (p *
299         arm_MEM a ((7 >< 0) w) *
300         arm_MEM (a + 1w) ((15 >< 8) w) *
301         arm_MEM (a + 2w) ((23 >< 16) w) *
302         arm_MEM (a + 3w) ((31 >< 24) w))
303        c
304        (q *
305         arm_MEM a ((7 >< 0) w) *
306         arm_MEM (a + 1w) ((15 >< 8) w) *
307         arm_MEM (a + 2w) ((23 >< 16) w) *
308         arm_MEM (a + 3w) ((31 >< 24) w)) =
309       SPEC ARM_MODEL
310        (cond (DISJOINT (arm_instr (a, w)) (BIGUNION (IMAGE arm_instr c))) * p)
311        ((a, w) INSERT c)
312        q`,
313    REPEAT strip_tac
314    \\ once_rewrite_tac [GSYM progTheory.SPEC_CODE]
315    \\ rewrite_tac [ARM_MODEL_def, stateTheory.CODE_POOL,
316                    pred_setTheory.IMAGE_INSERT,
317                    pred_setTheory.IMAGE_EMPTY,
318                    pred_setTheory.BIGUNION_INSERT,
319                    pred_setTheory.BIGUNION_EMPTY]
320    \\ Cases_on `DISJOINT (arm_instr (a, w)) (BIGUNION (IMAGE arm_instr c))`
321    \\ rw [stateTheory.UNION_STAR, arm_instr_star, set_sepTheory.SEP_CLAUSES,
322           progTheory.SPEC_FALSE_PRE,
323           AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM]
324    \\ imp_res_tac arm_instr_star_not_disjoint
325    \\ fs [set_sepTheory.SEP_CLAUSES, progTheory.SPEC_FALSE_PRE,
326           AC set_sepTheory.STAR_ASSOC set_sepTheory.STAR_COMM]
327    )
328
329val sub_intro = Theory.save_thm("sub_intro",
330   simpLib.SIMP_PROVE (srw_ss()) []
331      ``(a + (-b + c) = a - b + c : word32) /\ (a + -b = a - b)``
332   )
333
334val tac = asm_simp_tac (srw_ss()++wordsLib.WORD_CANCEL_ss)
335             [pred_setTheory.INSERT_INTER]
336
337(*
338val top = utilsLib.rhsc (wordsLib.WORD_EVAL_CONV ``word_T - 2w : word32``)
339*)
340
341val DISJOINT_arm_instr = Q.store_thm("DISJOINT_arm_instr",
342   `!a pc x y.
343      3w <+ a /\ a <+ 0xFFFFFFFDw ==>
344      DISJOINT (arm_instr (pc + a, x)) (arm_instr (pc, y))`,
345   rw [arm_instr_def, pred_setTheory.DISJOINT_DEF]
346   \\ `a + 1w <> 0w` by blastLib.FULL_BBLAST_TAC
347   \\ `a + 2w <> 0w` by blastLib.FULL_BBLAST_TAC
348   \\ `a + 3w <> 0w` by blastLib.FULL_BBLAST_TAC
349   \\ `a <> 0w` by blastLib.FULL_BBLAST_TAC
350   \\ `3w <> a` by blastLib.FULL_BBLAST_TAC
351   \\ `2w <> a` by blastLib.FULL_BBLAST_TAC
352   \\ `1w <> a` by blastLib.FULL_BBLAST_TAC
353   \\ tac
354   )
355
356val lem = Q.prove(
357   `!a x y. arm_instr (a + 4w, x) INTER arm_instr (a, y) = {}`,
358   rw [arm_instr_def, pred_setTheory.DISJOINT_DEF]
359   \\ tac
360   )
361
362val DISJOINT_arm_instr_2 = Q.prove(
363   `!a pc x1 x2 y.
364      DISJOINT (arm_instr (pc + a, x1))
365               (arm_instr (pc + a + 4w, x2) UNION arm_instr (pc, y)) =
366      DISJOINT (arm_instr (pc + a, x1)) (arm_instr (pc, y))`,
367   rw [pred_setTheory.DISJOINT_DEF, lem]
368   \\ metis_tac [pred_setTheory.INTER_COMM]
369   )
370
371val rearrange =
372   blastLib.BBLAST_PROVE ``a + (b + c + d) = a + (b + c) + d : word32``
373
374fun disjoint_arm_instr q =
375   DISJOINT_arm_instr
376   |> Q.SPEC q
377   |> Drule.SPEC_ALL
378   |> Conv.CONV_RULE (LAND_CONV blastLib.BBLAST_CONV)
379   |> REWRITE_RULE [rearrange]
380   |> Drule.GEN_ALL
381
382fun disjoint_arm_instr_2 q =
383   DISJOINT_arm_instr_2
384   |> Q.SPEC q
385   |> REWRITE_RULE [sub_intro, wordsTheory.WORD_ADD_ASSOC,
386                    GSYM wordsTheory.WORD_ADD_SUB_ASSOC]
387   |> Drule.GEN_ALL
388
389val disjoint_arm_instr_thms = Theory.save_thm("disjoint_arm_instr_thms",
390   Drule.LIST_CONJ
391     ([disjoint_arm_instr `(w2w (w: word8) + 8w) + 4w`,
392       disjoint_arm_instr `w2w (w: word8) + 8w`,
393       disjoint_arm_instr `w2w (w: word12) + 8w`,
394       disjoint_arm_instr
395         `^(bitstringSyntax.mk_v2w (bitstringSyntax.mk_bstring 10 0, ``:32``))
396          + 8w`,
397       disjoint_arm_instr
398         `(^(bitstringSyntax.mk_v2w (bitstringSyntax.mk_bstring 10 0, ``:32``))
399           + 8w) + 4w`] @
400      List.map disjoint_arm_instr_2 [`a`, `-a`, `a + b`, `a - b`])
401   )
402
403(* ------------------------------------------------------------------------ *)
404
405val () = export_theory()
406