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