1structure prog_x64Lib :> prog_x64Lib =
2struct
3
4open HolKernel boolLib bossLib;
5open wordsLib stringLib addressTheory pred_setTheory combinTheory;
6open set_sepTheory x64_Theory x64_Lib helperLib;
7open x64_seq_monadTheory x64_coretypesTheory x64_astTheory x64_icacheTheory;
8open prog_x64Theory wordsTheory x64_encodeLib;
9
10infix \\
11val op \\ = op THEN;
12
13val x64_status = zS_HIDE;
14val x64_pc = ``zPC``;
15val x64_exec_flag = ref true;
16val x64_code_write_perm = ref false;
17val x64_use_stack = ref false;
18fun set_x64_exec_flag b = (x64_exec_flag := b);
19fun set_x64_code_write_perm_flag b = (x64_code_write_perm := b);
20fun set_x64_use_stack b = (x64_use_stack := b);
21val Zreg_distinct = x64_decoderTheory.Zreg_distinct;
22
23datatype mpred_type = zMEM_AUTO | zMEM_BYTE_MEMORY | zMEM_MEMORY64;
24
25fun name_for_resource counter tm = let
26  val to_lower_drop_two = implode o tl o tl o explode o to_lower
27  in if type_of tm = ``:Zreg`` then let
28       val name = fst (dest_const tm)
29       val reg_name = snd (hd (filter (fn (x,y) => x = name)
30           [("RAX","r0"), ("RCX","r1"), ("RDX","r2"), ("RBX","r3"),
31            ("RSP","r4"), ("RBP","r5"), ("RSI","r6"), ("RDI","r7"),
32            ("zR8","r8"), ("zR9","r9"), ("zR10","r10"), ("zR11","r11"),
33            ("zR12","r12"), ("zR13","r13"), ("zR14","r14"),
34            ("zR15","r15")]))
35       in reg_name end
36     else if type_of tm = ``:Zeflags``
37          then "z_" ^ (to_lower_drop_two o fst o dest_const) tm else
38     (counter := 1 + !counter; ("x" ^ int_to_string (!counter))) end;
39
40val word2bytes_lemma = CONJ (EVAL ``word2bytes 2 (w:'a word)``)
41                            (EVAL ``word2bytes 4 (w:'a word)``)
42
43val w2n_MOD = prove(
44  ``!imm32. w2n (imm32:word32) MOD 4294967296 = w2n imm32``,
45  Cases THEN FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]);
46
47fun pre_process_thm th = let
48  val th = RW [ZREAD_MEM2_WORD64_THM,ZWRITE_MEM2_WORD64_THM,wordsTheory.WORD_ADD_0,
49               ZREAD_MEM2_WORD16_def,ZWRITE_MEM2_WORD16_def,bit_listTheory.bytes2word_def,
50               wordsTheory.ZERO_SHIFT,wordsTheory.WORD_OR_CLAUSES,word2bytes_lemma,EL_thm] th
51  val x = ref 0
52  fun all_distinct [] = []
53    | all_distinct (x::xs) = x :: all_distinct (filter (fn y => not (x = y)) xs)
54  val rs = find_terml (fn tm => type_of tm = ``:Zreg``) (concl th)
55  val fs = find_terml (fn tm => type_of tm = ``:Zeflags``) (concl th)
56  val ws = find_terml (can (match_term ``ZREAD_MEM2_WORD32 a``)) (concl th)
57  val ws = ws @ find_terml (can (match_term ``ZWRITE_MEM2_WORD32 a``)) (concl th)
58  val ws = all_distinct (map cdr ws)
59  val bs = find_terml (can (match_term ``ZREAD_MEM2 a``)) (concl th)
60  val bs = bs @ find_terml (can (match_term ``ZWRITE_MEM2 a``)) (concl th)
61  val bs = all_distinct (map cdr bs)
62  fun make_eq_tm pattern lhs name = let
63    val var = mk_var(name_for_resource x name, type_of pattern)
64    in mk_eq(subst [lhs |-> name] pattern,var) end
65  val rs2 = map (make_eq_tm ``ZREAD_REG r s`` ``r:Zreg``) rs
66  val fs2 = map (make_eq_tm ``ZREAD_EFLAG f s`` ``f:Zeflags``) fs
67  val ws2 = map (make_eq_tm ``ZREAD_MEM2_WORD32 a s`` ``a:word64``) ws
68  val bs2 = map (make_eq_tm ``ZREAD_MEM2 a s`` ``a:word64``) bs
69  val result = rs2 @ fs2 @ ws2 @ bs2 @ [``ZREAD_RIP s = rip``]
70  val th = foldr (uncurry DISCH) th result
71  val th = RW [AND_IMP_INTRO,GSYM CONJ_ASSOC,wordsTheory.WORD_XOR_CLAUSES,
72             wordsTheory.WORD_AND_CLAUSES,w2n_MOD] (SIMP_RULE std_ss [] th)
73  in th end;
74
75fun x64_pre_post g s = let
76  fun get_arg tm = (cdr o car) tm
77  val h = g
78  val xs = find_terml (can (match_term ``(ZREAD_REG x s = y)``)) h
79         @ find_terml (can (match_term ``(ZREAD_EFLAG x s = y)``)) h
80         @ find_terml (can (match_term ``(ZREAD_MEM2_WORD32 x s = y)``)) h
81         @ find_terml (can (match_term ``(ZREAD_MEM2 x s = y)``)) h
82  val xs = map (fn tm => ((get_arg o cdr o car) tm, cdr tm)) xs
83  val ys = find_terml (can (match_term ``ZWRITE_MEM2 a x``)) h
84         @ find_terml (can (match_term ``ZWRITE_MEM2_WORD32 a x``)) h
85         @ find_terml (can (match_term ``ZWRITE_EFLAG a x``)) h
86         @ find_terml (can (match_term ``ZWRITE_REG a x``)) h
87  val ys = map (fn tm => (get_arg tm, cdr tm)) ys
88  val new_rip = (cdr o hd) (find_terml (can (match_term ``ZWRITE_RIP e``)) h)
89  fun assigned_aux x y [] = y
90    | assigned_aux x y ((q,z)::zs) = if aconv x q then z else assigned_aux x y zs
91  fun get_assigned_value x y = assigned_aux x y ys
92  fun mk_pre_post_assertion (name,var) = let
93    val (pattern,name_tm,var_tm) =
94          if type_of name = ``:Zreg`` then
95            (``zR1 a w``,``a:Zreg``,``w:word64``)
96          else if type_of name = ``:Zeflags`` then
97            (``zS1 a w``,``a:Zeflags``,``w:bool option``)
98          else if type_of var = ``:word8`` then
99            (``~(zM1 a (SOME (w,zDATA_PERM ex)))``,``a:word64``,``w:word8``)
100          else if type_of var = ``:word32`` then
101            (``zM a w``,``a:word64``,``w:word32``)
102          else fail()
103    in (subst [name_tm|->name,var_tm|->var] pattern,
104        subst [name_tm|->name,var_tm|->get_assigned_value name var] pattern) end
105  val pre_post = map mk_pre_post_assertion xs
106  val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool``
107  val post = list_mk_star (map snd pre_post) ``:x64_set -> bool``
108  fun is_precond tm =
109   (not (can (match_term ``ZREAD_REG r s = v``) tm) andalso
110    not (can (match_term ``ZREAD_MEM2 r s = v``) tm) andalso
111    not (can (match_term ``ZREAD_MEM2_WORD32 r s = v``) tm) andalso
112    not (can (match_term ``CAN_ZWRITE_MEM r s``) tm) andalso
113    not (can (match_term ``CAN_ZREAD_MEM r s``) tm) andalso
114    not (can (match_term ``ZREAD_INSTR r s = v``) tm) andalso
115    not (can (match_term ``ZREAD_EFLAG r s = v``) tm) andalso
116    not (can (match_term ``ZREAD_RIP s = v``) tm)) handle e => true
117  val all_conds = (list_dest dest_conj o fst o dest_imp) h
118  val pre_conds = (filter is_precond) all_conds
119  val ss = foldr (fn (x,y) => (fst (dest_eq x) |-> snd (dest_eq x)) :: y handle e => y) []
120             (filter is_precond pre_conds)
121  val ss = ss @ map ((fn tm => mk_var((fst o dest_var o cdr) tm,``:bool option``) |-> tm) o cdr)
122    (filter (can (match_term ``ZREAD_EFLAG x s = SOME y``)) all_conds)
123  val pre = subst ss pre
124  val post = subst ss post
125  val pre = mk_star (``zPC rip``,pre)
126  val post = mk_star (mk_comb(``zPC``,new_rip),post)
127  val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds))
128  in (pre,post) end;
129
130val SING_SUBSET = prove(
131  ``!x:'a y. {x} SUBSET y = x IN y``,
132  REWRITE_TAC [INSERT_SUBSET,EMPTY_SUBSET]);
133
134fun introduce_zBYTE_MEMORY_ANY th = if
135  not (can (find_term (can (match_term ``zM1``))) (concl th))
136  then th else let
137  val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th
138  val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
139  val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th
140  val (_,p,_,q) = dest_spec(concl th)
141  val xs = (rev o list_dest dest_star) p
142  val tm = ``~(zM1 a x)``
143  val xs = filter (can (match_term tm)) xs
144  fun foo tm = (fst o pairSyntax.dest_pair o cdr o cdr o cdr) tm |->
145               mk_comb(mk_var("g",``:word64->word8``),(cdr o car o cdr) tm)
146  val th = INST (map foo xs) th
147  in if xs = [] then th else let
148    val (_,p,_,q) = dest_spec(concl th)
149    val xs = (rev o list_dest dest_star) p
150    val tm = ``~(zM1 a x)``
151    val xs = filter (can (match_term tm)) xs
152    val ys = (map (cdr o car o cdr) xs)
153    fun foo [] = mk_var("dg",``:word64 set``)
154      | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v)
155    val frame = mk_comb(mk_comb(``zBYTE_MEMORY_ANY ex``,foo ys),mk_var("g",``:word64->word8``))
156    val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th)
157    val th = RW [GSYM STAR_ASSOC] th
158    val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zBYTE_MEMORY_ANY_INSERT
159    fun compact th = let
160      val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th)
161      val rw = (INST (fst (match_term fff x)) o SPEC_ALL o GSYM) zBYTE_MEMORY_ANY_INSERT
162      val th = DISCH ((fst o dest_imp o concl) rw) th
163      val th = SIMP_RULE bool_ss [GSYM zBYTE_MEMORY_ANY_INSERT] th
164      in th end
165    val th = repeat compact th
166    val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th
167    val th = RW [APPLY_UPDATE_ID] th
168    val v = hd (filter (is_var) ys @ ys)
169    fun ss [] = ``{}:word64 set``
170      | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs)
171    val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("dg",``:word64 set``))
172    val u2 = u1
173    val u3 = (fst o dest_imp o concl) th
174    val goal = mk_imp(u2,u3)
175    val imp = prove(goal,
176      ONCE_REWRITE_TAC [ALIGNED_MOD_4]
177      THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO]
178      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
179      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
180      THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET]
181      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
182      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
183      THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
184      THEN ASM_SIMP_TAC std_ss []
185      THEN CCONTR_TAC
186      THEN FULL_SIMP_TAC std_ss []
187      THEN FULL_SIMP_TAC std_ss [])
188    val th = DISCH_ALL (MATCH_MP th (UNDISCH imp))
189    val th = RW [GSYM progTheory.SPEC_MOVE_COND] th
190    val th = remove_primes th
191    val th = REWRITE_RULE [SING_SUBSET] th
192    val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
193    in th end end
194
195fun introduce_zMEMORY th = if
196  not (can (find_term (can (match_term ``zM``))) (concl th))
197  then th else let
198  val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th
199  val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
200  val th = CONV_RULE (PRE_CONV STAR_REVERSE_CONV) th
201  val (_,p,_,q) = dest_spec(concl th)
202  val xs = (rev o list_dest dest_star) p
203  val tm = ``zM a x``
204  val xs = filter (can (match_term tm)) xs
205  fun foo tm = cdr tm |->
206               mk_comb(mk_var("f",``:word64->word32``),(cdr o car) tm)
207  val th = INST (map foo xs) th
208  in if xs = [] then th else let
209    val (_,p,_,q) = dest_spec(concl th)
210    val xs = (rev o list_dest dest_star) p
211    val tm = ``zM a x``
212    val xs = filter (can (match_term tm)) xs
213    val ys = (map (cdr o car) xs)
214    fun foo [] = mk_var("df",``:word64 set``)
215      | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v)
216    val frame = mk_comb(mk_comb(``zMEMORY``,foo ys),mk_var("f",``:word64->word32``))
217    val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th)
218    val th = RW [GSYM STAR_ASSOC] th
219    val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zMEMORY_INSERT
220    fun compact th = let
221      val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th)
222      val rw = (INST (fst (match_term fff x)) o SPEC_ALL o DISCH_ALL o GSYM o UNDISCH) zMEMORY_INSERT
223      val th = DISCH ((fst o dest_imp o concl) rw) th
224      val th = SIMP_RULE bool_ss [GSYM zMEMORY_INSERT] th
225      in th end
226    val th = repeat compact th
227    val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th
228    val th = RW [APPLY_UPDATE_ID] th
229    val v = hd (filter (is_var) ys @ ys)
230    fun ss [] = ``{}:word64 set``
231      | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs)
232    val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word64 set``))
233    val u3 = (fst o dest_imp o concl) th
234    val u2 = list_mk_conj (u1::filter is_eq (list_dest dest_conj u3))
235    val goal = mk_imp(u2,u3)
236    val imp = prove(goal,
237      ONCE_REWRITE_TAC [ALIGNED_MOD_4]
238      THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO]
239      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
240      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
241      THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET]
242      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
243      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
244      THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
245      THEN ASM_SIMP_TAC std_ss []
246      THEN CCONTR_TAC
247      THEN FULL_SIMP_TAC std_ss []
248      THEN FULL_SIMP_TAC std_ss [])
249    val th = DISCH_ALL (MATCH_MP th (UNDISCH imp))
250    val th = RW [GSYM progTheory.SPEC_MOVE_COND] th
251    val th = remove_primes th
252    val th = REWRITE_RULE [SING_SUBSET] th
253    val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
254    in th end end
255
256fun introduce_zM64 th = if
257  not (can (find_term (can (match_term ``zM``))) (concl th))
258  then th else let
259  val pattern = ``zM (a + 4w) x1 * zM a x2``
260  val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car
261            |> find_term (can (match_term pattern))
262  val x1 = (cdr o cdr o car) tag
263  val x2 = (cdr o cdr) tag
264  val a = (cdr o car o cdr) tag
265  val res = SPECL [a,mk_var("xx",``:word64``)] (RW1[STAR_COMM]zM64_def)
266  val y1 = (cdr o cdr o car) ((snd o dest_eq o concl) res)
267  val y2 = (cdr o cdr) ((snd o dest_eq o concl) res)
268  val th = RW [GSYM res,GSYM STAR_ASSOC] (INST [x1|->y1,x2|->y2] th)
269  val th = RW [STAR_ASSOC,LOAD64] th
270  in th end handle HOL_ERR _ => th;
271
272val is_spec_1 = true
273val is_spec_1 = false
274
275val SPEC_1_pat = temporalTheory.SPEC_1_def |> SPEC_ALL |> concl |> dest_eq |> fst
276fun dest_spec_1 tm =
277  if can (match_term SPEC_1_pat) tm then let
278    val (x1234,x5) = dest_comb tm
279    val (x123,x4) = dest_comb x1234
280    val (x12,x3) = dest_comb x123
281    val (x1,x2) = dest_comb x12
282    val (x0,x1) = dest_comb x1
283    in (x1,x2,x3,x4) end
284  else failwith("not a SPEC_1")
285
286fun introduce_zMEMORY64_spec_or_spec_1 th is_spec_1 =
287  let val th = introduce_zM64 th in
288  if not (can (find_term (can (match_term ``zM64``))) (concl th))
289  then th else let
290  val pre_conv = if is_spec_1 then RATOR_CONV o PRE_CONV else PRE_CONV
291  val th = CONV_RULE (pre_conv STAR_REVERSE_CONV) th
292  val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
293  val th = CONV_RULE (pre_conv STAR_REVERSE_CONV) th
294  val (_,p,_,q) = dest_spec(concl th) handle HOL_ERR _ => dest_spec_1(concl th)
295  val xs = (rev o list_dest dest_star) p
296  val tm = ``zM64 a x``
297  val xs = filter (can (match_term tm)) xs
298  fun foo tm = cdr tm |->
299               mk_comb(mk_var("f",``:word64->word64``),(cdr o car) tm)
300  val th = INST (map foo xs) th
301  in if xs = [] then th else let
302    val (_,p,_,q) = dest_spec(concl th) handle HOL_ERR _ => dest_spec_1(concl th)
303    val xs = (rev o list_dest dest_star) p
304    val tm = ``zM64 a x``
305    val xs = filter (can (match_term tm)) xs
306    val ys = (map (cdr o car) xs)
307    fun foo [] = mk_var("df",``:word64 set``)
308      | foo (v::vs) = pred_setSyntax.mk_delete(foo vs,v)
309    val frame = mk_comb(mk_comb(``zMEMORY64``,foo ys),mk_var("f",``:word64->word64``))
310    val th = SPEC frame (MATCH_MP progTheory.SPEC_FRAME th)
311             handle HOL_ERR _ =>
312             SPEC frame (MATCH_MP temporalTheory.SPEC_1_FRAME th)
313    val th = RW [GSYM STAR_ASSOC,SEP_CLAUSES] th
314    val fff = (fst o dest_eq o concl o UNDISCH_ALL o SPEC_ALL o GSYM) zMEMORY64_INSERT
315    fun compact th = let
316      val x = find_term (can (match_term fff)) ((car o car o concl o UNDISCH_ALL) th)
317      val rw = (INST (fst (match_term fff x)) o SPEC_ALL o DISCH_ALL o GSYM o UNDISCH) zMEMORY64_INSERT
318      val th = DISCH ((fst o dest_imp o concl) rw) th
319      val th = SIMP_RULE bool_ss [GSYM zMEMORY64_INSERT] th
320      in th end
321    val th = repeat compact th
322    val th = RW [STAR_ASSOC,AND_IMP_INTRO,GSYM CONJ_ASSOC] th
323    val th = RW [APPLY_UPDATE_ID] th
324    val v = hd (filter (is_var) ys @ ys)
325    fun ss [] = ``{}:word64 set``
326      | ss (v::vs) = pred_setSyntax.mk_insert(v,ss vs)
327    val u1 = pred_setSyntax.mk_subset(ss (rev ys),mk_var("df",``:word64 set``))
328    val u3 = (fst o dest_imp o concl) th
329    val u2 = list_mk_conj (u1::filter is_eq (list_dest dest_conj u3))
330    val goal = mk_imp(u2,u3)
331    val imp = prove(goal,
332      ONCE_REWRITE_TAC [ALIGNED_MOD_4]
333      THEN SIMP_TAC std_ss [WORD_ADD_0,WORD_SUB_RZERO]
334      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
335      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
336      THEN SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_DELETE,INSERT_SUBSET]
337      THEN SIMP_TAC std_ss [WORD_EQ_ADD_CANCEL,word_sub_def]
338      THEN SIMP_TAC (std_ss++SIZES_ss) [n2w_11,word_2comp_n2w]
339      THEN REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC
340      THEN ASM_SIMP_TAC std_ss []
341      THEN CCONTR_TAC
342      THEN FULL_SIMP_TAC std_ss []
343      THEN FULL_SIMP_TAC std_ss [])
344    val th = DISCH_ALL (MATCH_MP th (UNDISCH imp))
345    val th = RW [GSYM progTheory.SPEC_MOVE_COND,
346                 GSYM temporalTheory.SPEC_MOVE_1_COND] th
347    val th = remove_primes th
348    val th = REWRITE_RULE [SING_SUBSET] th
349    val th = SIMP_RULE (bool_ss++sep_cond_ss) [] th
350    in th end end end
351
352fun introduce_zMEMORY64 th = introduce_zMEMORY64_spec_or_spec_1 th false;
353fun introduce_zMEMORY64_1 th = introduce_zMEMORY64_spec_or_spec_1 th true;
354
355(*
356fun introduce_zSTACK th =
357  if not (can (find_term (fn x => x = ``RSP``)) (concl th)) then th else let
358  val pattern = ``zM (a + 4w) x1 * zM a x2``
359  val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car
360            |> find_term (can (match_term pattern))
361  val x1 = (cdr o cdr o car) tag
362  val x2 = (cdr o cdr) tag
363  val a = (cdr o car o cdr) tag
364  val _ = mem (mk_var("r4",``:word64``)) (free_vars a) orelse fail()
365  val res = SPECL [a,mk_var("xx",``:word64``)] (RW1[STAR_COMM]zM64_def)
366  val y1 = (cdr o cdr o car) ((snd o dest_eq o concl) res)
367  val y2 = (cdr o cdr) ((snd o dest_eq o concl) res)
368  val th = RW [GSYM res,GSYM STAR_ASSOC] (INST [x1|->y1,x2|->y2] th)
369  val th = RW [STAR_ASSOC,LOAD64] th
370  in th end handle HOL_ERR _ => th;
371*)
372
373fun calculate_length_and_jump th = let
374  val (_,_,c,q) = dest_spec (concl th)
375  val l = c |> car |> cdr |> cdr |> listSyntax.dest_list |> fst |> length
376  in
377    let val v = find_term (can (match_term ``zPC (p + n2w n)``)) q
378    in (th,l,SOME (0 + (numSyntax.int_of_term o cdr o cdr o cdr) v)) end
379  handle e =>
380    let val v = find_term (can (match_term ``zPC (p - n2w n)``)) q
381    in (th,l,SOME (0 - (numSyntax.int_of_term o cdr o cdr o cdr) v)) end
382  handle e =>
383    (th,l,NONE) end
384
385fun post_process_thm mpred no_status th = let
386  val th = if mpred = zMEM_MEMORY64 then introduce_zMEMORY64 th else th
387  (* val th = if mpred = zMEM_AUTO then introduce_zSTACK th else th *)
388  val th = RW [GSYM zR_def] th
389  val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [wordsTheory.word_mul_n2w,SEP_CLAUSES] th
390  val th = CONV_RULE FIX_WORD32_ARITH_CONV th
391  val th = if mpred = zMEM_AUTO then introduce_zMEMORY th else th
392  val th = introduce_zBYTE_MEMORY_ANY th
393  val th = SIMP_RULE (std_ss++sw2sw_ss++w2w_ss) [GSYM wordsTheory.WORD_ADD_ASSOC,
394    word_arith_lemma1,word_arith_lemma2,word_arith_lemma3,word_arith_lemma4] th
395  val th = CONV_RULE FIX_WORD32_ARITH_CONV th
396  val th = RW [wordsTheory.WORD_ADD_ASSOC,wordsTheory.WORD_ADD_0] th
397  fun f th = let
398    val x = find_term (can (match_term ``(THE x):'a``)) (concl th)
399    val y = optionSyntax.mk_some(mk_var(fst (dest_var (cdr x)),type_of x))
400    val th = INST [cdr x |-> y] th
401    val th = SIMP_RULE bool_ss [SEP_CLAUSES,optionLib.option_rws] th
402    in th end
403  val th = if no_status then th else repeat f th
404  val th = RW [ALIGNED_def] th
405  val th = SIMP_RULE std_ss [wordsTheory.WORD_EQ_SUB_ZERO,w2w_eq_n2w,w2w_CLAUSES] th
406  val th = th |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [WORD_w2w_OVER_BITWISE,
407                   WORD_w2w_n2w_OVER_BITWISE,w2w_OVER_ARITH,w2w_OVER_ARITH_n2w]
408              |> SIMP_RULE (std_ss++wordsLib.SIZES_ss) [w2w_w2w,w2w_id,w2n_n2w,
409                   WORD_ALL_BITS,WORD_BITS_BITS_ZERO,WORD_BITS_NOT_BITS_ZERO]
410  in calculate_length_and_jump th end;
411
412fun calc_code th = let
413  val tms = find_terml (can (match_term ``ZREAD_INSTR a s = SOME x``)) (concl th)
414  val tms = map dest_eq tms
415  fun addr tm = (Arbnum.toInt o numSyntax.dest_numeral o cdr o cdr o cdr o car) tm
416                handle e => 0
417  val tms = map (fn (x,y) => (addr x, cdr y)) tms
418  val code = map snd (sort (fn (x,_) => fn (y,_) => x <= y) tms)
419  in listSyntax.mk_list (code, ``:word8``) end;
420
421fun x64_prove_one_spec_or_spec_1 th c is_spec_1 = let
422  val g = concl th
423  val s = find_term (can (match_term ``X64_NEXT x = SOME y``)) g
424  val s = (snd o dest_comb o snd o dest_comb) s
425  val (pre,post) = x64_pre_post g s
426  val tm = if is_spec_1
427           then ``SPEC_1 X64_MODEL pre {(rip,c)} post SEP_F``
428           else ``SPEC X64_MODEL pre {(rip,c)} post``
429  val tm = subst [mk_var("pre",type_of pre) |-> pre,
430                  mk_var("post",type_of post) |-> post,
431                  mk_var("c",type_of c) |-> c] tm
432  val FLIP_TAC = CONV_TAC (ONCE_REWRITE_CONV [EQ_SYM_EQ])
433  val th1 = Q.INST [`s`|->`X64_ICACHE_UPDATE x (r,e,t,m,i)`] th
434  val th1 = RW [ZREAD_CLAUSES,ZWRITE_MEM2_WORD32_def] th1
435  val th1 = RW [ZWRITE_EFLAG_def,X64_ICACHE_UPDATE_def,ZWRITE_MEM2_def,
436        ZWRITE_REG_def,
437        APPLY_UPDATE_THM,WORD_EQ_ADD_CANCEL,x64_address_lemma,ZWRITE_RIP_def] th1
438  val th = prove(tm,
439(*
440    set_goal([],tm)
441*)
442    MATCH_MP_TAC (if is_spec_1 then IMP_X64_SPEC_1 else IMP_X64_SPEC)
443    \\ REPEAT STRIP_TAC
444    \\ EXISTS_TAC ((cdr o cdr o concl o UNDISCH) th1)
445    \\ STRIP_TAC \\ REWRITE_TAC [X64_ICACHE_UPDATE_def]
446    THENL [MATCH_MP_TAC th1,ALL_TAC]
447    \\ REPEAT (POP_ASSUM MP_TAC)
448    \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC,
449         STAR_x64_2set, IN_DELETE, APPLY_UPDATE_THM, Zreg_distinct,
450         GSYM ALIGNED_def, wordsTheory.n2w_11, Zeflags_distinct,
451         Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET,
452         EMPTY_SUBSET, SEP_CLAUSES,X64_ICACHE_UPDATE_def,ZCLEAR_ICACHE_def,
453         X64_ICACHE_REVERT_def,zM_def,WORD_EQ_ADD_CANCEL,x64_address_lemma]
454    \\ ONCE_REWRITE_TAC [CODE_POOL_x64_2set]
455    \\ REWRITE_TAC [listTheory.LENGTH,address_list_def]
456    \\ SIMP_TAC std_ss [arithmeticTheory.ADD1,X64_ICACHE_EXTRACT_def]
457    \\ SIMP_TAC (std_ss++wordsLib.SIZES_ss) [GSYM STAR_ASSOC,
458         STAR_x64_2set, IN_DELETE, APPLY_UPDATE_THM, Zreg_distinct,
459         GSYM ALIGNED_def, wordsTheory.n2w_11, Zeflags_distinct,
460         Q.SPECL [`s`,`x INSERT t`] SET_EQ_SUBSET, INSERT_SUBSET,
461         EMPTY_SUBSET,x64_pool_def,X64_ACCURATE_CLAUSES]
462    \\ SIMP_TAC std_ss [ZREAD_REG_def,ZREAD_EFLAG_def,ZREAD_RIP_def]
463    \\ NTAC 3 (FLIP_TAC \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO])
464    \\ SIMP_TAC std_ss [CAN_ZREAD_MEM,CAN_ZWRITE_MEM,IN_INSERT,word_arith_lemma1]
465    \\ SIMP_TAC std_ss [ZREAD_MEM2_WORD32_def,ZREAD_MEM2_WORD64_def,
466         ZREAD_MEM2_def,wordsTheory.WORD_ADD_0]
467    \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM]
468    \\ SIMP_TAC std_ss [CAN_ZREAD_MEM,CAN_ZWRITE_MEM,IN_INSERT,word_arith_lemma1]
469    \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM]
470    THEN1 (SIMP_TAC std_ss [GSYM arithmeticTheory.ADD_ASSOC]
471           \\ SIMP_TAC std_ss [bit_listTheory.bytes2word_thm,IN_zDATA_PERM]
472           \\ SIMP_TAC std_ss [arithmeticTheory.ADD_ASSOC]
473           \\ SIMP_TAC std_ss [markerTheory.Abbrev_def]
474           \\ REPEAT STRIP_TAC \\ FLIP_TAC \\ MATCH_MP_TAC (GEN_ALL ZREAD_INSTR_IMP)
475           \\ Q.EXISTS_TAC `T` \\ ASM_SIMP_TAC std_ss []
476           \\ FULL_SIMP_TAC std_ss [wordsTheory.word_add_n2w,GSYM wordsTheory.WORD_ADD_ASSOC])
477    \\ SIMP_TAC std_ss [word2bytes_thm,EL_thm,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET]
478    \\ FULL_SIMP_TAC std_ss [UPDATE_x64_2set'',word_arith_lemma1,
479         ALIGNED_CLAUSES,icache_revert_ID,X64_ACCURATE_UPDATE]
480    \\ SIMP_TAC std_ss [AND_IMP_INTRO]
481    \\ STRIP_TAC \\ IMP_RES_TAC X64_ACCURATE_IMP
482    \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [markerTheory.Abbrev_def]
483    \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,GSYM word_add_n2w]
484    \\ SIMP_TAC (std_ss++SIZES_ss) [WORD_EQ_ADD_CANCEL,n2w_11,INSERT_SUBSET,IN_INSERT,EMPTY_SUBSET])
485  val th = INST [``w:bool``|-> (if !x64_code_write_perm then T else F)] th
486  in RW [STAR_ASSOC,SEP_CLAUSES,markerTheory.Abbrev_def] th end;
487
488fun x64_prove_one_spec th c =
489  x64_prove_one_spec_or_spec_1 th c false;
490
491fun x64_prove_one_spec_1 th c =
492  x64_prove_one_spec_or_spec_1 th c true;
493
494fun x64_prove_specs mpred no_status s = let
495  val th = x64_step s
496  val th = if mpred = zMEM_BYTE_MEMORY then
497             RW [ZWRITE_MEM2_WORD32_def,ZREAD_MEM2_WORD32_def] th else th
498  val c = calc_code th
499  val th = pre_process_thm th
500  val th = RW [w2n_MOD] th
501(* val th = x64_prove_one_spec th c *)
502  in if (is_cond o cdr o cdr o snd o dest_imp o concl) th then let
503       val (x,y,z) = dest_cond (find_term is_cond (concl th))
504       fun replace_conv th tm = if (fst o dest_eq o concl) th = tm then th else ALL_CONV tm
505       fun prove_branch cth th = let
506         val tm1 = (fst o dest_imp o concl o ISPECL [x,y,z]) cth
507         val th1 = CONV_RULE (DEPTH_CONV (replace_conv (UNDISCH (ISPECL [x,y,z] cth)))) th
508         val th1 = (RW [AND_IMP_INTRO,GSYM CONJ_ASSOC] o DISCH_ALL) th1
509         val th1 = x64_prove_one_spec th1 c
510         val th1 = SIMP_RULE std_ss [SEP_CLAUSES] (DISCH tm1 th1)
511         val th1 = RW [CONTAINER_def] th1
512         val th1 = RW [RW [GSYM precond_def] (GSYM progTheory.SPEC_MOVE_COND)] th1
513         in post_process_thm mpred no_status th1 end
514       in (prove_branch CONTAINER_IF_T th, SOME (prove_branch CONTAINER_IF_F th)) end
515     else (post_process_thm mpred no_status (x64_prove_one_spec th c),NONE) end
516
517fun x64_jump (tm1:term) (tm2:term) (jump_length:int) (forward:bool) = ("",0)
518
519fun x64_spec_aux mpred = cache (x64_prove_specs mpred false);
520
521val x64_spec_aux_auto = cache (x64_prove_specs zMEM_AUTO false);
522val x64_spec_aux_byte = cache (x64_prove_specs zMEM_BYTE_MEMORY false);
523val x64_spec_aux_memory64 = cache (x64_prove_specs zMEM_MEMORY64 false);
524val x64_spec_aux_memory64_no_status = cache (x64_prove_specs zMEM_MEMORY64 true);
525
526fun apply_to_thm f ((th1,i1,j1),NONE) = ((f th1,i1,j1),NONE)
527  | apply_to_thm f ((th1,i1,j1),SOME (th2,i2,j2)) = ((f th1,i1,j1),SOME (f th2,i2,j2))
528
529fun x64_spec s = let
530  val (s,rename,_) = parse_renamer s
531  val ((th,i,j),other) = x64_spec_aux_auto s
532  val b = if !x64_exec_flag then T else F
533  val th = INST [``ex:bool``|->b] th
534  val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th
535  in apply_to_thm rename ((th,i,j),other) end
536
537fun x64_spec_byte_memory s = let
538  val (s,rename,_) = parse_renamer s
539  val ((th,i,j),other) = x64_spec_aux_byte s
540  val b = if !x64_exec_flag then T else F
541  val th = INST [``ex:bool``|->b] th
542  val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th
543  in apply_to_thm rename ((th,i,j),other) end
544
545fun x64_spec_memory64 s = let
546  val (s,rename,_) = parse_renamer s
547  val ((th,i,j),other) = x64_spec_aux_memory64 s
548  val b = if !x64_exec_flag then T else F
549  val th = INST [``ex:bool``|->b] th
550  val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th
551  in apply_to_thm rename ((th,i,j),other) end
552
553fun x64_spec_memory64_no_status s = let
554  val (s,rename,_) = parse_renamer s
555  val ((th,i,j),other) = x64_spec_aux_memory64_no_status s
556  val b = if !x64_exec_flag then T else F
557  val th = INST [``ex:bool``|->b] th
558  val th = RW [GSYM zBYTE_MEMORY_def,GSYM zBYTE_MEMORY_Z_def] th
559  in apply_to_thm rename ((th,i,j),other) end
560
561val x64_tools = (x64_spec, x64_jump, x64_status, x64_pc);
562val x64_tools_no_status = (x64_spec, x64_jump, TRUTH, x64_pc);
563val x64_tools_64 = (x64_spec_memory64, x64_jump, x64_status, x64_pc);
564val x64_tools_64_no_status = (x64_spec_memory64_no_status, x64_jump, TRUTH, x64_pc);
565
566
567(*
568
569  val mpred = zMEM_AUTO
570  val th = x64_spec (x64_encode "add r0,5");
571  val th = x64_spec (x64_encode "inc r11");
572  val th = x64_spec (x64_encode "je 40");
573  val th = x64_spec (x64_encode "loop -40");
574  val th = x64_spec "E9"; (* jmp imm32 *)
575  val th = x64_spec (x64_encode "add eax,5");
576  val th = x64_spec (x64_encode "cmove rax, rcx");
577  val th = x64_spec (x64_encode "mov al, [rax+rbx+4]");
578  val th = x64_spec (x64_encode "mov [rax+rbx+4], al");
579  val th = x64_spec (x64_encode "mov ax, [rax]");
580  val th = x64_spec (x64_encode "mov [rax], ax");
581  val th = x64_spec (x64_encode "add [rax], ax");
582  val th = x64_spec (x64_encode "add [rax], eax");
583  val th = x64_spec (x64_encode "add [rax], rax");
584  val th = x64_spec (x64_encode "call r2");
585  val th = x64_spec (x64_encode "ret");
586  val th = x64_spec (x64_encode "add rsp,80");
587  val th = x64_spec (x64_encode "push rax");
588  val th = x64_spec (x64_encode "pop rax");
589  val th = x64_spec (x64_encode "mov BYTE [r11+1],124");
590
591  val ((th,_,_),_) = x64_spec (x64_encode "mov [rax],r1b")
592  val th = th |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n,
593                   GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def]
594              |> Q.GEN `g` |> Q.GEN `dg`
595              |> Q.INST [`r0`|->`a+n2w (LENGTH (xs:word8 list))`]
596              |> MATCH_MP zCODE_HEAP_SNOC
597
598  val ((th,_,_),_) = x64_spec "C600"
599  val th = th |> REWRITE_RULE [SIGN_EXTEND_IGNORE,n2w_w2n,
600                   GSYM zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def]
601              |> Q.GEN `g` |> Q.GEN `dg`
602              |> Q.INST [`r0`|->`a+n2w (LENGTH (xs:word8 list))`,`imm8`|->`n2w k`]
603              |> MATCH_MP zCODE_HEAP_SNOC
604
605  val th = x64_spec_memory64 (x64_encode "add [rax], rax");
606  val th = x64_spec_memory64 (x64_encode "mov [rax+40], rbx");
607  val th = x64_spec_memory64 (x64_encode "mov rbx,[rax+40]");
608
609  val s = "mov r8d, [r7+4*r3+6000]"
610  val s = x64_encode s
611  val (spec,_,sts,_) = x64_tools
612  val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8))
613
614  val s = "mov [r7+4*r3+6000], r8d"
615  val s = x64_encode s
616  val (spec,_,sts,_) = x64_tools
617  val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8))
618
619  val th = x64_spec_memory64_no_status (x64_encode "adc r8,r9")
620  val th = x64_spec_memory64_no_status (x64_encode "je 400")
621
622*)
623
624end
625