1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_ops";
2
3open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory;
4open combinTheory finite_mapTheory addressTheory;
5
6open decompilerLib progTheory set_sepTheory helperLib;
7open lisp_typeTheory lisp_invTheory lisp_gcTheory lisp_equalTheory;
8open ppc_encodeLib x86_encodeLib;
9open prog_armLib prog_ppcLib prog_x86Lib;
10
11val decompile_arm = decompile prog_armLib.arm_tools;
12val decompile_ppc = decompile prog_ppcLib.ppc_tools;
13val decompile_x86 = decompile prog_x86Lib.x86_tools;
14
15infix \\
16val op \\ = op THEN;
17val _ = map Parse.hide ["r0","r1","r2","r3","r4","r5","r6","r7","r8","r9","r10","r11","r12","r13"];
18val RW = REWRITE_RULE;
19val RW1 = ONCE_REWRITE_RULE;
20
21val aLISP_def = Define `
22  aLISP (x1,x2,x3,x4,x5,x6,limit) =
23    SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s.
24     ~(aR 2w) * aR 3w r3 * aR 4w r4 * aR 5w r5 * aR 6w r6 * aR 7w r7 * aR 8w r8 * aR 9w a *
25     aMEMORY df f * aMEMORY dm m * aBYTE_MEMORY dg g *
26       cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`;
27
28val pLISP_def = Define `
29  pLISP (x1,x2,x3,x4,x5,x6,limit) =
30    SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s.
31     ~(pR 0w) * ~(pR 2w) * pR 3w r3 * pR 4w r4 * pR 5w r5 * pR 6w r6 * pR 7w r7 * pR 8w r8 * pR 9w a *
32     pMEMORY df f * pMEMORY dm m * pBYTE_MEMORY dg g *
33       cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`;
34
35val xLISP_def = Define `
36  xLISP (x1,x2,x3,x4,x5,x6,limit) =
37    SEP_EXISTS a r3 r4 r5 r6 r7 r8 df f dm m dg g s.
38     xR EAX r3 * xR ECX r4 * xR EDX r5 * xR EBX r6 * xR EDI r7 * xR ESI r8 * xR EBP a *
39     xMEMORY df f * xMEMORY dm m * xBYTE_MEMORY dg g *
40       cond (lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g))`;
41
42fun x86_reg 1 = "eax" | x86_reg 2 = "ecx" | x86_reg 3 = "edx"
43  | x86_reg 4 = "ebx" | x86_reg 5 = "edi" | x86_reg 6 = "esi" | x86_reg _ = fail()
44
45val _ = set_echo 0;
46
47
48(* automation *)
49
50fun dest_sep_exists tm = let
51  val (x,y) = dest_comb tm
52  val _ = if (fst o dest_const) x = "SEP_EXISTS" then () else fail()
53  in dest_abs y end;
54
55fun dest_sep_cond tm =
56  if (fst o dest_const o fst o dest_comb) tm = "cond"
57  then snd (dest_comb tm) else fail();
58
59fun prove_spec th imp def pre_tm post_tm = let
60  val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th
61  val tm = (cdr o concl o SPEC_ALL) def
62  val tm = repeat (snd o dest_sep_exists) tm
63  val fill = list_dest dest_star tm
64  val res = list_dest dest_star p
65  val res2 = filter (not o can dest_sep_cond) res
66  val fill2 = filter (not o can dest_sep_cond) fill
67  val res3 = map dest_comb (filter (not o can dest_sep_hide) res2)
68  val fill3 = map dest_comb (filter (not o can dest_sep_hide) fill2)
69  fun rename [] (y1,y2) = (y2,y2)
70    | rename ((x1,x2)::xs) (y1,y2) = if x1 ~~ y1 then (y2,x2)
71                                     else rename xs (y1,y2)
72  val s = map (fn (x,y) => x |-> y) (map (rename fill3) res3)
73  val th = INST s th
74  val th = UNDISCH_ALL (RW [SPEC_MOVE_COND] (SIMP_RULE (bool_ss++sep_cond_ss)  [] th))
75  val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th
76  val fill = list_dest dest_star tm
77  val res = list_dest dest_star p
78  val f = list_mk_star (filter (fn x => not (tmem x res)) fill) (type_of (hd fill))
79  val th = SPEC f (MATCH_MP SPEC_FRAME th)
80  val pre = (fst o dest_imp o snd o dest_imp) (concl imp) handle e => ``T:bool``
81  val (_,p,_,_) = dest_spec (concl (PURE_REWRITE_RULE [GSYM SPEC_MOVE_COND] (DISCH pre th)))
82  val x = (snd o dest_star) p
83  val th = SPEC x (MATCH_MP SPEC_FRAME th)
84  val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN th)
85  val goal = (cdr o car o concl) th
86  fun AUTO_EXISTS_TAC (asm,tm) = let
87      fun ex tm = let
88        val (v,tm) = dest_exists tm
89        in v :: ex tm end handle e => []
90      val xs = ex tm
91      val x = hd (list_dest dest_conj (repeat (snd o dest_exists) tm))
92      val assum = [``lisp_inv (Dot x1 x2,x2,x3,x4,x5,x6,limit)
93        (w1,w2,w3,w4,w5,w6,a',x',xs',s,dm,m,dg,g)``,
94       ``lisp_inv (x1,x2,x3,x4,x5,x6,limit)
95        (r3,r4,r5,r6,r7,r8,a,df,f,s,dm,m,dg,g)``]
96       val tm2 = hd (filter (can (match_term x)) asm)
97       val (s,_) = match_term x tm2
98       val ys = map (subst s) xs
99       fun exx [] = ALL_TAC | exx (x::xs) = EXISTS_TAC x THEN exx xs
100       in exx ys (asm,tm) end
101  val lemma = prove(goal,
102    REWRITE_TAC [STAR_ASSOC]
103    \\ SIMP_TAC (std_ss++sep_cond_ss) []
104    \\ REWRITE_TAC [SEP_IMP_MOVE_COND]
105    \\ REPEAT STRIP_TAC
106    \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp)
107    \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC))
108    \\ ASM_SIMP_TAC std_ss [LET_DEF]
109    \\ SIMP_TAC std_ss [def,SEP_CLAUSES]
110    \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS]
111    \\ REPEAT STRIP_TAC
112    \\ SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR]
113    \\ AUTO_EXISTS_TAC
114    \\ FULL_SIMP_TAC std_ss []
115    \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_MULT_COMM WORD_MULT_ASSOC]
116    \\ METIS_TAC [])
117  val th = MATCH_MP th lemma
118  val th = RW [GSYM SPEC_MOVE_COND] (DISCH_ALL th)
119  val tm = (cdr o concl o SPEC_ALL) def
120  fun ff tm = let val (x,y) = dest_sep_exists tm in x :: ff y end handle e => []
121  val zs = ff tm
122  fun gg [] th = th
123    | gg (x::xs) th = gg xs (EXISTS_PRE [ANTIQUOTE x] th)
124  val th = gg zs th
125  val th = MATCH_MP SPEC_STRENGTHEN th
126  val th = SPEC (mk_cond_star(pre_tm,pre)) th
127  val goal = (cdr o car o concl) th
128  val lemma = prove(goal,
129    SIMP_TAC std_ss [def,SEP_CLAUSES]
130    \\ SIMP_TAC (bool_ss++sep_cond_ss) []
131    \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS,cond_STAR]
132    \\ REPEAT STRIP_TAC
133    \\ AUTO_EXISTS_TAC
134    \\ FULL_SIMP_TAC std_ss []
135    \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp)
136    \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC))
137    \\ FULL_SIMP_TAC std_ss []
138    \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ METIS_TAC [])
139  val th = MATCH_MP th lemma
140  val th = RW [SEP_CLAUSES] th
141  in th end;
142
143fun set_pc th = let
144  val (_,_,_,q) = (dest_spec o concl o UNDISCH_ALL) th
145  val tm = find_term (fn x => tmem (car x) [``xPC``,``aPC``,``pPC``] handle e => false) q
146  in subst [``p:word32``|->cdr tm] end
147
148
149(* cons *)
150
151val ARM_LISP_CONS = save_thm("ARM_LISP_CONS",let
152  val th = arm_alloc_thm
153  val imp = lisp_inv_cons
154  val def = aLISP_def
155  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
156  val post_tm = set_pc th ``aLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
157  val res = prove_spec th imp def pre_tm post_tm
158  val (_,_,c,_) = dest_spec (concl res)
159  val def = new_definition("arm_alloc_code",mk_eq(``(arm_alloc_code:word32->(word32 # word32) set) p``,c))
160  val res = RW [GSYM def] res
161  in res end);
162
163val PPC_LISP_CONS = save_thm("PPC_LISP_CONS",let
164  val th = RW [ppc_alloc_EQ] ppc_alloc_thm
165  val imp = lisp_inv_cons
166  val def = pLISP_def
167  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
168  val post_tm = set_pc th ``pLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
169  val res = prove_spec th imp def pre_tm post_tm
170  val (_,_,c,_) = dest_spec (concl res)
171  val def = new_definition("ppc_alloc_code",mk_eq(``(ppc_alloc_code:word32->(word32 # word32) set) p``,c))
172  val res = RW [GSYM def] res
173  in res end);
174
175val X86_LISP_CONS = save_thm("X86_LISP_CONS",let
176  val th = RW [x86_alloc_EQ] x86_alloc_thm
177  val imp = lisp_inv_cons
178  val def = xLISP_def
179  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
180  val post_tm = set_pc th ``xLISP (Dot x1 x2,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
181  val res = prove_spec th imp def pre_tm post_tm
182  val (_,_,c,_) = dest_spec (concl res)
183  val def = new_definition("x86_alloc_code",mk_eq(``(x86_alloc_code:word32->(word32 # word8 list # bool) set) p``,c))
184  val res = RW [GSYM def] res
185  in res end);
186
187
188(* equal *)
189
190val ARM_LISP_EQUAL = save_thm("ARM_LISP_EQUAL",let
191  val th = arm_eq_thm
192  val imp = lisp_inv_equal
193  val def = aLISP_def
194  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
195  val post_tm = set_pc th ``aLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
196  val res = prove_spec th imp def pre_tm post_tm
197  val (_,_,c,_) = dest_spec (concl res)
198  val def = new_definition("arm_equal_code",mk_eq(``(arm_equal_code:word32->(word32 # word32) set) p``,c))
199  val res = RW [GSYM def] res
200  in res end);
201
202val PPC_LISP_EQUAL = save_thm("PPC_LISP_EQUAL",let
203  val th = ppc_eq_thm
204  val imp = lisp_inv_equal
205  val def = pLISP_def
206  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
207  val post_tm = set_pc th ``pLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
208  val res = prove_spec th imp def pre_tm post_tm
209  val (_,_,c,_) = dest_spec (concl res)
210  val def = new_definition("ppc_equal_code",mk_eq(``(ppc_equal_code:word32->(word32 # word32) set) p``,c))
211  val res = RW [GSYM def] res
212  in res end);
213
214val X86_LISP_EQUAL = save_thm("X86_LISP_EQUAL",let
215  val th = x86_eq_thm
216  val imp = lisp_inv_equal
217  val def = xLISP_def
218  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
219  val post_tm = set_pc th ``xLISP (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
220  val res = prove_spec th imp def pre_tm post_tm
221  val (_,_,c,_) = dest_spec (concl res)
222  val def = new_definition("x86_equal_code",mk_eq(``(x86_equal_code:word32->(word32 # word8 list # bool) set) p``,c))
223  val res = RW [GSYM def] res
224  in res end);
225
226
227(* isDot and isSym *)
228
229fun ARM_LISP_ISDOT i = let
230  val _ = print "a"
231  val (arm_spec,_,sts,_) = arm_tools
232  val ((th,_,_),_) = arm_spec ("E31"^(int_to_string (i+2))^"0003")
233  val th = HIDE_POST_RULE ``aS1 psrN`` th
234  val th = HIDE_POST_RULE ``aS1 psrC`` th
235  val th = HIDE_POST_RULE ``aS1 psrV`` th
236  val th = HIDE_PRE_STATUS_RULE sts th
237  val def = aLISP_def
238  val imp = lisp_inv_test
239  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
240  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (isDot x) * ~(aS1 psrC) * ~(aS1 psrV)``
241  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
242  val th = RW [ALIGNED_INTRO] th
243  val th = RW [ALIGNED_def] th
244  val result = prove_spec th imp def pre_tm post_tm
245  in save_thm("ARM_LISP_ISDOT" ^ int_to_string i,result) end;
246
247fun X86_LISP_ISDOT i = let
248  val _ = print "x"
249  val s = "test " ^ (x86_reg i) ^ ", 3"
250  val s = x86_encode s
251  val (spec,_,sts,_) = x86_tools
252  val ((th,_,_),_) = spec s
253  val th = HIDE_PRE_STATUS_RULE sts th
254  val th = HIDE_POST_RULE ``xS1 X_PF`` th
255  val th = HIDE_POST_RULE ``xS1 X_SF`` th
256  val th = HIDE_POST_RULE ``xS1 X_AF`` th
257  val th = HIDE_POST_RULE ``xS1 X_OF`` th
258  val th = HIDE_POST_RULE ``xS1 X_CF`` th
259  val def = xLISP_def
260  val imp = lisp_inv_test
261  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
262  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (isDot x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
263  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
264  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
265  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
266  val result = prove_spec th imp def pre_tm post_tm
267  in save_thm("X86_LISP_ISDOT" ^ int_to_string i,result) end;
268
269fun PPC_LISP_ISDOT i = let
270  val _ = print "p"
271  val s = "andi. 2, " ^ int_to_string (i+2) ^ ", 3"
272  val s = ppc_encode s
273  val (spec,_,sts,_) = ppc_tools
274  val ((th,_,_),_) = spec s
275  val th = HIDE_PRE_STATUS_RULE sts th
276  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
277  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th
278  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
279  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
280  val def = pLISP_def
281  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
282  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (isDot(x))) * ~(pS1 PPC_CARRY) *
283      ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)``
284  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
285  val imp = lisp_inv_test
286  val th = HIDE_POST_RULE ``pR 2w`` th
287  val th = HIDE_PRE_RULE ``pR 2w`` th
288  val result = prove_spec th imp def pre_tm post_tm
289  in save_thm("PPC_LISP_ISDOT" ^ int_to_string i,result) end;
290
291val _ = map ARM_LISP_ISDOT [1,2,3,4,5,6]
292val _ = map X86_LISP_ISDOT [1,2,3,4,5,6]
293val _ = map PPC_LISP_ISDOT [1,2,3,4,5,6]
294
295fun ARM_LISP_ISSTR i = let
296  val (arm_spec,_,sts,_) = arm_tools
297  val ((th,_,_),_) = arm_spec ("E31"^(int_to_string (i+2))^"0001")
298  val th = HIDE_POST_RULE ``aS1 psrN`` th
299  val th = HIDE_POST_RULE ``aS1 psrC`` th
300  val th = HIDE_POST_RULE ``aS1 psrV`` th
301  val th = HIDE_PRE_STATUS_RULE sts th
302  val th = RW [Q.SPEC `n2w n` WORD_AND_COMM] th
303  val def = aLISP_def
304  val imp = lisp_inv_test
305  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
306  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ ~(isSym x) * ~(aS1 psrC) * ~(aS1 psrV)``
307  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
308  val result = prove_spec th imp def pre_tm post_tm
309  in save_thm("ARM_LISP_ISSTR" ^ int_to_string i,result) end;
310
311fun X86_LISP_ISSTR i = let
312  val _ = print "x"
313  val s = "test " ^ (x86_reg i) ^ ", 1"
314  val s = x86_encode s
315  val (spec,_,sts,_) = x86_tools
316  val ((th,_,_),_) = spec s
317  val th = HIDE_PRE_STATUS_RULE sts th
318  val th = HIDE_POST_RULE ``xS1 X_PF`` th
319  val th = HIDE_POST_RULE ``xS1 X_SF`` th
320  val th = HIDE_POST_RULE ``xS1 X_AF`` th
321  val th = HIDE_POST_RULE ``xS1 X_OF`` th
322  val th = HIDE_POST_RULE ``xS1 X_CF`` th
323  val def = xLISP_def
324  val imp = lisp_inv_test
325  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
326  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME ~(isSym x)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
327  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
328  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
329  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
330  val result = prove_spec th imp def pre_tm post_tm
331  in save_thm("X86_LISP_ISSTR" ^ int_to_string i,result) end;
332
333fun PPC_LISP_ISSTR i = let
334  val _ = print "p"
335  val s = "andi. 2, " ^ int_to_string (i+2) ^ ", 1"
336  val s = ppc_encode s
337  val (spec,_,sts,_) = ppc_tools
338  val ((th,_,_),_) = spec s
339  val th = HIDE_PRE_STATUS_RULE sts th
340  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
341  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th
342  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
343  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
344  val def = pLISP_def
345  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
346  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (~isSym(x))) * ~(pS1 PPC_CARRY) *
347      ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)``
348  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
349  val imp = lisp_inv_test
350  val th = HIDE_POST_RULE ``pR 2w`` th
351  val th = HIDE_PRE_RULE ``pR 2w`` th
352  val result = prove_spec th imp def pre_tm post_tm
353  in save_thm("PPC_LISP_ISSTR" ^ int_to_string i,result) end;
354
355val _ = map ARM_LISP_ISSTR [1,2,3,4,5,6]
356val _ = map X86_LISP_ISSTR [1,2,3,4,5,6]
357val _ = map PPC_LISP_ISSTR [1,2,3,4,5,6]
358
359
360(* assign Sym "nil", Sym "t" *)
361
362fun swap_thm 1 = lisp_inv_swap1
363  | swap_thm 2 = lisp_inv_swap2
364  | swap_thm 3 = lisp_inv_swap3
365  | swap_thm 4 = lisp_inv_swap4
366  | swap_thm 5 = lisp_inv_swap5
367  | swap_thm 6 = lisp_inv_swap6
368  | swap_thm _ = fail()
369
370fun ARM_LISP_CONST (c,n,task,thc) i = let
371  val _ = print "a"
372  val s = "E3A0"^(int_to_string (i+2))^"0"^n
373  val (spec,_,_,_) = arm_tools
374  val ((th,_,_),_) = spec s
375  val imp = lisp_inv_move
376  val def = aLISP_def
377  val swap = swap_thm i
378  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
379  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
380  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
381  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)``
382  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c]
383  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
384  val post_tm = cdr (concl (INST s (REFL post_tm)))
385  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
386  val tm2 = cdr (concl (INST s (INST sw (REFL tm))))
387  val result = prove_spec th imp def pre_tm post_tm
388  val r1 = save_thm("ARM_LISP_CONST" ^ int_to_string i ^ n,result)
389  val r2 = save_thm("ARM_LISP_CONST" ^ int_to_string i ^ "_" ^ task,
390           RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result)
391  in (r1,r2) end
392
393val ARM_LISP_CONST_NIL   = ARM_LISP_CONST (``(Sym "nil"):SExp``, "03", "EVAL", lisp_inv_nil)
394val ARM_LISP_CONST_T     = ARM_LISP_CONST (``(Sym "t"):SExp``, "0F", "CONT", lisp_inv_t)
395val ARM_LISP_CONST_QUOTE = ARM_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote)
396
397val _ = map ARM_LISP_CONST_NIL [1,2,3,4,5,6]
398val _ = map ARM_LISP_CONST_T [1,2,3,4,5,6]
399val _ = map ARM_LISP_CONST_QUOTE [1,2,3,4,5,6]
400
401fun X86_LISP_CONST (c,n,task,thc) i = let
402  val _ = print "x"
403  val m = Arbnum.toString(Arbnum.fromHexString n)
404  val s = "mov " ^ x86_reg i ^ ", " ^ m
405  val s = x86_encode s
406  val (spec,_,_,_) = x86_tools
407  val ((th,_,_),_) = spec s
408  val imp = lisp_inv_move
409  val def = xLISP_def
410  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
411  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
412  val swap = swap_thm i
413  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
414  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
415  val pre_tm = mk_star(pre_tm, (snd o dest_star o cdr o car o car o concl) th)
416  val post_tm = mk_star(post_tm, (snd o dest_star o cdr o concl) th)
417  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c]
418  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
419  val post_tm = cdr (concl (INST s (REFL post_tm)))
420  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
421  val tm2 = cdr (concl (INST s (INST sw (REFL tm))))
422  val result = prove_spec th imp def pre_tm post_tm
423  val r1 = save_thm("X86_LISP_CONST" ^ int_to_string i ^ n,result)
424  val r2 = save_thm("X86_LISP_CONST" ^ int_to_string i ^ "_" ^ task,
425           RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result)
426  in (r1,r2) end
427
428val X86_LISP_CONST_NIL   = X86_LISP_CONST (``(Sym "nil"):SExp``, "03", "EVAL", lisp_inv_nil)
429val X86_LISP_CONST_T     = X86_LISP_CONST (``(Sym "t"):SExp``, "0F", "CONT", lisp_inv_t)
430val X86_LISP_CONST_QUOTE = X86_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote)
431
432val _ = map X86_LISP_CONST_NIL [1,2,3,4,5,6]
433val _ = map X86_LISP_CONST_T [1,2,3,4,5,6]
434val _ = map X86_LISP_CONST_QUOTE [1,2,3,4,5,6]
435
436fun PPC_LISP_CONST (c,n,task,thc) i = let
437  val _ = print "p"
438  val m = Arbnum.toString(Arbnum.fromHexString n)
439  val s = "addi " ^ int_to_string (i+2) ^ ", 0, " ^ m
440  val s = ppc_encode s
441  val (spec,_,_,_) = ppc_tools
442  val ((th,_,_),_) = spec s
443  val th = RW [WORD_OR_CLAUSES] th
444  val def = pLISP_def
445  val swap = swap_thm i
446  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
447  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
448  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
449  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 4w)``
450  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> c]
451  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
452  val post_tm = cdr (concl (INST s (REFL post_tm)))
453  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
454  val tm2 = cdr (concl (INST s (INST sw (REFL tm))))
455  val result = prove_spec th imp def pre_tm post_tm
456  val r1 = save_thm("PPC_LISP_CONST" ^ int_to_string i ^ n,result)
457  val r2 = save_thm("PPC_LISP_CONST" ^ int_to_string i ^ "_" ^ task,
458           RW [GSYM TASK_EVAL_def,GSYM TASK_CONT_def,GSYM TASK_FUNC_def] result)
459  in (r1,r2) end
460
461val PPC_LISP_CONST_NIL   = PPC_LISP_CONST (``(Sym "nil"):SExp``, "3", "EVAL", lisp_inv_nil)
462val PPC_LISP_CONST_T     = PPC_LISP_CONST (``(Sym "t"):SExp``, "F", "CONT", lisp_inv_t)
463val PPC_LISP_CONST_QUOTE = PPC_LISP_CONST (``(Sym "quote"):SExp``, "1B", "FUNC", lisp_inv_quote)
464
465val _ = map PPC_LISP_CONST_NIL [1,2,3,4,5,6]
466val _ = map PPC_LISP_CONST_T [1,2,3,4,5,6]
467val _ = map PPC_LISP_CONST_QUOTE [1,2,3,4,5,6]
468
469
470(* assign 0 or 1 *)
471
472val lisp_inv_0 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `0` o UNDISCH) lisp_inv_Val
473val lisp_inv_1 = (DISCH_ALL o SIMP_RULE std_ss [] o Q.SPEC `1` o UNDISCH) lisp_inv_Val
474
475fun ARM_LISP_VAL thc i = let
476  val _ = print "a"
477  val v = find_term (can (match_term ``Val n``)) (concl thc)
478  val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc)
479  val n = int_to_string (numSyntax.int_of_term (cdr n))
480  val s = "E3A0"^(int_to_string (i+2))^"00"^n
481  val (spec,_,_,_) = arm_tools
482  val ((th,_,_),_) = spec s
483  val def = aLISP_def
484  val swap = swap_thm i
485  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
486  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
487  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
488  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)``
489  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v]
490  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
491  val post_tm = cdr (concl (INST s (REFL post_tm)))
492  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
493  val tm2 = cdr (concl (INST s (INST sw (REFL tm))))
494  val result = prove_spec th imp def pre_tm post_tm
495  val r1 = save_thm("ARM_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result)
496  in r1 end
497
498val _ = map (ARM_LISP_VAL lisp_inv_0) [1,2,3,4,5,6]
499val _ = map (ARM_LISP_VAL lisp_inv_1) [1,2,3,4,5,6]
500
501fun X86_LISP_VAL thc i = let
502  val _ = print "x"
503  val v = find_term (can (match_term ``Val n``)) (concl thc)
504  val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc)
505  val n = int_to_string (numSyntax.int_of_term (cdr n))
506  val s = "mov " ^ x86_reg i ^ ", " ^ n
507  val s = x86_encode s
508  val (spec,_,_,_) = x86_tools
509  val ((th,_,_),_) = spec s
510  val def = xLISP_def
511  val swap = swap_thm i
512  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
513  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
514  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip``
515  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip``
516  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v]
517  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
518  val post_tm = cdr (concl (INST s (REFL post_tm)))
519  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
520  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
521  val result = prove_spec th imp def pre_tm post_tm
522  val r1 = save_thm("X86_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result)
523  in r1 end
524
525val _ = map (X86_LISP_VAL lisp_inv_0) [1,2,3,4,5,6]
526val _ = map (X86_LISP_VAL lisp_inv_1) [1,2,3,4,5,6]
527
528fun PPC_LISP_VAL thc i = let
529  val _ = print "p"
530  val v = find_term (can (match_term ``Val n``)) (concl thc)
531  val n = find_term (can (match_term ``(n2w n):word32``)) (concl thc)
532  val n = int_to_string (numSyntax.int_of_term (cdr n))
533  val s = "addi " ^ (int_to_string (i+2)) ^ ", 0, " ^ n
534  val s = ppc_encode s
535  val (spec,_,_,_) = ppc_tools
536  val ((th,_,_),_) = spec s
537  val def = pLISP_def
538  val swap = swap_thm i
539  val imp = DISCH_ALL (MATCH_MP swap (UNDISCH thc))
540  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH swap))
541  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
542  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)``
543  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> v]
544  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("0x" ^ n ^ "w:word32")]]
545  val post_tm = cdr (concl (INST s (REFL post_tm)))
546  val result = prove_spec th imp def pre_tm post_tm
547  val r1 = save_thm("PPC_LISP_VAL_" ^ int_to_string i ^ "_" ^ n,result)
548  in r1 end
549
550val _ = map (PPC_LISP_VAL lisp_inv_0) [1,2,3,4,5,6]
551val _ = map (PPC_LISP_VAL lisp_inv_1) [1,2,3,4,5,6]
552
553
554(* move *)
555
556fun ARM_LISP_MOVE (i,j) = let
557  val _ = print "a"
558  val inst = "E1A0"^(int_to_string (i+2))^"00"^(int_to_string (j+2))
559  val (spec,_,_,_) = arm_tools
560  val ((th,_,_),_) = spec inst
561  val imp = lisp_inv_move
562  val def = aLISP_def
563  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
564  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)``
565  val s = [[QUOTE ("x" ^ int_to_string i)] |-> [QUOTE ("x" ^ int_to_string j)]]
566  val sw = [[QUOTE ("w" ^ int_to_string i)] |-> [QUOTE ("w" ^ int_to_string j)]]
567  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
568  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
569  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
570  val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp])
571  val result = prove_spec th imp def pre_tm post_tm
572  in save_thm("ARM_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end
573
574fun X86_LISP_MOVE (i,j) = let
575  val _ = print "x"
576  val s = "mov " ^ x86_reg i ^ ", " ^ x86_reg j
577  val s = x86_encode s
578  val (spec,_,_,_) = x86_tools
579  val ((th,_,_),_) = spec s
580  val imp = lisp_inv_move
581  val def = xLISP_def
582  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
583  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
584  val pre_tm = mk_star(pre_tm, (snd o dest_star o cdr o car o car o concl) th)
585  val post_tm = mk_star(post_tm, (snd o dest_star o cdr o concl) th)
586  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("x" ^ int_to_string j)]]
587  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("w" ^ int_to_string j)]]
588  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
589  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
590  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
591  val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp])
592  val result = prove_spec th imp def pre_tm post_tm
593  in save_thm("X86_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end
594
595fun PPC_LISP_MOVE (i,j) = let
596  val _ = print "p"
597  val s = "or " ^ int_to_string (i+2) ^ ", " ^ int_to_string (j+2) ^ ", " ^ int_to_string (j+2)
598  val s = ppc_encode s
599  val (spec,_,_,_) = ppc_tools
600  val ((th,_,_),_) = spec s
601  val th = RW [WORD_OR_CLAUSES] th
602  val imp = lisp_inv_move
603  val def = pLISP_def
604  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
605  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)``
606  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("x" ^ int_to_string j)]]
607  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("w" ^ int_to_string j)]]
608  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
609  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
610  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
611  val imp = prove(mk_imp(tm,tm2),METIS_TAC [imp])
612  val result = prove_spec th imp def pre_tm post_tm
613  in save_thm("PPC_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end
614
615fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys
616fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys
617val list = filter (fn (x,y) => not (x = y)) (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
618val _ = map ARM_LISP_MOVE list
619val _ = map X86_LISP_MOVE list
620val _ = map PPC_LISP_MOVE list
621
622
623(* car *)
624
625fun ARM_LISP_CAR (i,j) = let
626  val _ = print "a"
627  val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"000"
628  val (spec,_,_,_) = arm_tools
629  val ((th,_,_),_) = spec inst
630  val def = aLISP_def
631  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
632  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)``
633  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term [QUOTE ("CAR x" ^ int_to_string j ^ ":SExp")]]
634  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("(xs:word32->word32) w" ^ int_to_string j ^ ":word32")]]
635  val post_tm = subst s post_tm
636  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
637  val tm2 = subst s (subst sw tm)
638  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
639  val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")]
640  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),METIS_TAC [lisp_inv_car,lisp_inv_address])
641  val result = prove_spec th imp def pre_tm post_tm
642  in save_thm("ARM_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end
643
644fun X86_LISP_CAR (i,j) = let
645  val _ = print "x"
646  val s = "mov " ^ x86_reg i ^ ", [" ^ x86_reg j ^ "]"
647  val s = x86_encode s
648  val (spec,_,_,_) = x86_tools
649  val ((th,_,_),_) = spec s
650  val def = xLISP_def
651  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
652  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
653  val pc1 = find_term (can (match_term ``xPC p``)) ((cdr o car o car o concl) th)
654  val pc2 = find_term (can (match_term ``xPC p``)) ((cdr o concl) th)
655  val pre_tm = mk_star(pre_tm,pc1)
656  val post_tm = mk_star(post_tm,pc2)
657  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CAR x" ^ int_to_string j)]]
658  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
659  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) w" ^ int_to_string j)]]
660  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
661  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
662  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
663  val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")]
664  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),
665    NTAC 2 STRIP_TAC
666    \\ IMP_RES_TAC lisp_inv_car
667    \\ IMP_RES_TAC lisp_inv_address
668    \\ ASM_SIMP_TAC std_ss [])
669  val result = prove_spec th imp def pre_tm post_tm
670  in save_thm("X86_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end
671
672fun PPC_LISP_CAR (i,j) = let
673  val _ = print "p"
674  val s = "lwz "^int_to_string(i+2)^",0("^int_to_string(j+2)^")"
675  val s = ppc_encode s
676  val (spec,_,_,_) = ppc_tools
677  val ((th,_,_),_) = spec s
678  val def = pLISP_def
679  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
680  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)``
681  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CAR x" ^ int_to_string j)]]
682  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
683  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) w" ^ int_to_string j)]]
684  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
685  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
686  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
687  val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " IN (x:word32 set) /\\ (w" ^ int_to_string j ^ " && 3w = 0w)")]
688  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),
689    NTAC 2 STRIP_TAC
690    \\ IMP_RES_TAC lisp_inv_car
691    \\ IMP_RES_TAC lisp_inv_address
692    \\ ASM_SIMP_TAC std_ss [])
693  val result = prove_spec th imp def pre_tm post_tm
694  in save_thm("PPC_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end
695
696val _ = map ARM_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
697val _ = map X86_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
698val _ = map PPC_LISP_CAR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
699
700
701(* cdr *)
702
703fun ARM_LISP_CDR (i,j) = let
704  val _ = print "a"
705  val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"004"
706  val (spec,_,_,_) = arm_tools
707  val ((th,_,_),_) = spec inst
708  val def = aLISP_def
709  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
710  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 4w)``
711  val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term [QUOTE ("CDR x" ^ int_to_string j ^ ":SExp")]]
712  val sw = [Term [QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> Term [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w):word32")]]
713  val post_tm = subst s post_tm
714  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
715  val tm2 = subst s (subst sw tm)
716  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
717  val tm4 = Term [QUOTE ("(w" ^ int_to_string j ^ " + 4w) IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")]
718  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),
719    REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES]
720    \\ REWRITE_TAC [ALIGNED_def] \\ METIS_TAC [lisp_inv_cdr,lisp_inv_address])
721  val result = prove_spec th imp def pre_tm post_tm
722  in save_thm("ARM_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end
723
724fun X86_LISP_CDR (i,j) = let
725  val _ = print "x"
726  val s = "mov " ^ x86_reg i ^ ", [" ^ x86_reg j ^ "+4]"
727  val s = x86_encode s
728  val (spec,_,_,_) = x86_tools
729  val ((th,_,_),_) = spec s
730  val def = xLISP_def
731  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
732  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit)``
733  val pc1 = find_term (can (match_term ``xPC p``)) ((cdr o car o car o concl) th)
734  val pc2 = find_term (can (match_term ``xPC p``)) ((cdr o concl) th)
735  val pre_tm = mk_star(pre_tm,pc1)
736  val post_tm = mk_star(post_tm,pc2)
737  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CDR x" ^ int_to_string j)]]
738  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
739  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w)")]]
740  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
741  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
742  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
743  val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " + 4w IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")]
744  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),
745    NTAC 2 STRIP_TAC
746    \\ REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES]
747    \\ REWRITE_TAC [ALIGNED_def]
748    \\ IMP_RES_TAC lisp_inv_cdr
749    \\ IMP_RES_TAC lisp_inv_address
750    \\ ASM_SIMP_TAC std_ss [])
751  val result = prove_spec th imp def pre_tm post_tm
752  in save_thm("X86_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end
753
754fun PPC_LISP_CDR (i,j) = let
755  val _ = print "p"
756  val s = "lwz "^int_to_string(i+2)^",4("^int_to_string(j+2)^")"
757  val s = ppc_encode s
758  val (spec,_,_,_) = ppc_tools
759  val ((th,_,_),_) = spec s
760  val def = pLISP_def
761  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
762  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w)``
763  val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CDR x" ^ int_to_string j)]]
764  val post_tm = cdr (concl (Q.INST s (REFL post_tm)))
765  val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(xs:word32->word32) (w" ^ int_to_string j ^ " + 4w)")]]
766  val tm = ``lisp_inv (x1,x2,x3,x4,x5,x6,limit) (w1,w2,w3,w4,w5,w6,a,x,xs,s,rest)``
767  val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm))))
768  val tm3 = Term [QUOTE ("isDot x" ^ int_to_string j)]
769  val tm4 = Term [QUOTE ("w" ^ int_to_string j ^ " + 4w IN (x:word32 set) /\\ ((w" ^ int_to_string j ^ " + 4w) && 3w = 0w)")]
770  val imp = prove(mk_imp(tm,mk_imp(tm3,mk_conj(tm2,tm4))),
771    NTAC 2 STRIP_TAC
772    \\ REWRITE_TAC [ALIGNED_INTRO,ALIGNED_CLAUSES]
773    \\ REWRITE_TAC [ALIGNED_def]
774    \\ IMP_RES_TAC lisp_inv_cdr
775    \\ IMP_RES_TAC lisp_inv_address
776    \\ ASM_SIMP_TAC std_ss [])
777  val result = prove_spec th imp def pre_tm post_tm
778  in save_thm("PPC_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end
779
780val _ = map ARM_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
781val _ = map X86_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
782val _ = map PPC_LISP_CDR (cross [1,2,3,4,5,6] [1,2,3,4,5,6])
783
784
785(* add *)
786
787val ARM_LISP_ADD = let
788  val (th,def) = decompile_arm "ha" `
789    E0833004 (* add r3,r3,r4 *)
790    E2433002 (* sub r3,r3,#2 *)`
791  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
792  val imp = lisp_inv_ADD
793  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
794  val def = aLISP_def
795  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
796  val post_tm = ``aLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * aPC (p + 0x8w)``
797  val result = prove_spec th imp def pre_tm post_tm
798  in save_thm("ARM_LISP_ADD",result) end;
799
800val X86_LISP_ADD = let
801  val (th,def) = decompile_x86 "ha" `
802    01C8   (* add eax,ecx *)
803    83E802 (* sub eax,2 *)`
804  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
805  val imp = lisp_inv_ADD
806  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
807  val def = xLISP_def
808  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
809  val post_tm = ``xLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * xPC (p + 0x5w) * ~xS``
810  val result = prove_spec th imp def pre_tm post_tm
811  in save_thm("X86_LISP_ADD",result) end;
812
813val PPC_LISP_ADD = let
814  val (th,def) = decompile_ppc "ha" `
815    7C632214 (* add 3,3,4 *)
816    3863FFFE (* addi 3,3,-2 *)`
817  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
818  val imp = lisp_inv_ADD
819  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
820  val def = pLISP_def
821  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
822  val post_tm = ``pLISP (LISP_ADD x1 x2,x2,x3,x4,x5,x6,limit) * pPC (p + 0x8w)``
823  val result = prove_spec th imp def pre_tm post_tm
824  in save_thm("PPC_LISP_ADD",result) end;
825
826
827(* sub *)
828
829val ARM_LISP_SUB = let
830  val (th,def) = decompile_arm "ha" `
831    E0433004 (* sub r3,r3,r4 *)
832    E2833002 (* add r3,r3,#2 *)`
833  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
834  val imp = lisp_inv_SUB
835  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
836  val def = aLISP_def
837  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
838  val post_tm = ``aLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * aPC (p + 0x8w)``
839  val result = prove_spec th imp def pre_tm post_tm
840  in save_thm("ARM_LISP_SUB",result) end;
841
842val X86_LISP_SUB = let
843  val (th,def) = decompile_x86 "ha" `
844    29C8   (* sub eax,ecx *)
845    83C002 (* add eax,2 *)`
846  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
847  val imp = lisp_inv_SUB
848  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
849  val def = xLISP_def
850  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
851  val post_tm = ``xLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * xPC (p + 0x5w) * ~xS``
852  val result = prove_spec th imp def pre_tm post_tm
853  in save_thm("X86_LISP_SUB",result) end;
854
855val PPC_LISP_SUB = let
856  val (th,def) = decompile_ppc "ha" `
857    7C641810 (* subfc 3,4,3 *)
858    38630002 (* addi 3,3,2 *)`
859  val th = SIMP_RULE std_ss [def,LET_DEF,SEP_CLAUSES] th
860  val imp = lisp_inv_SUB
861  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
862  val def = pLISP_def
863  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
864  val post_tm = ``pLISP (LISP_SUB x1 x2,x2,x3,x4,x5,x6,limit) * pPC (p + 0x8w) * ~pS``
865  val result = prove_spec th imp def pre_tm post_tm
866  in save_thm("PPC_LISP_SUB",result) end;
867
868(* sub1 and add1 *)
869
870fun ARM_LISP_SUB1 i = let
871  val (arm_spec,_,sts,_) = arm_tools
872  val st = int_to_string (i+2)
873  val ((th,_,_),_) = arm_spec ("E24"^st^st^"004")
874  val imp = lisp_inv_SUB1
875  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
876  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
877  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
878  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
879  val imp = RW1 [GSYM AND_IMP_INTRO] imp
880  val def = aLISP_def
881  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
882  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w)``
883  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
884  val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)``
885  val post_tm = subst [v|->tm] post_tm
886  val result = prove_spec th imp def pre_tm post_tm
887  in save_thm("ARM_LISP_SUB1_" ^ (int_to_string i),result) end;
888
889fun ARM_LISP_ADD1 i = let
890  val (arm_spec,_,sts,_) = arm_tools
891  val st = int_to_string (i+2)
892  val ((th,_,_),_) = arm_spec ("E28"^st^st^"004")
893  val imp = lisp_inv_ADD1
894  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
895  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
896  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
897  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
898  val imp = RW1 [GSYM AND_IMP_INTRO] imp
899  val def = aLISP_def
900  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
901  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w)``
902  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
903  val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)``
904  val post_tm = subst [v|->tm] post_tm
905  val result = prove_spec th imp def pre_tm post_tm
906  in save_thm("ARM_LISP_ADD1_" ^ (int_to_string i),result) end;
907
908val _ = map ARM_LISP_SUB1 [1,2,3,4,5,6]
909val _ = map ARM_LISP_ADD1 [1,2,3,4,5,6]
910
911fun X86_LISP_SUB1 i = let
912  val st = x86_reg i
913  val s = x86_encode ("sub "^st^",4")
914  val (spec,_,sts,_) = x86_tools
915  val ((th,_,_),_) = spec s
916  val th = HIDE_STATUS_RULE true sts th
917  val imp = lisp_inv_SUB1
918  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
919  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
920  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
921  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
922  val imp = RW1 [GSYM AND_IMP_INTRO] imp
923  val def = xLISP_def
924  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
925  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
926  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
927  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
928  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
929  val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)``
930  val post_tm = subst [v|->tm] post_tm
931  val result = prove_spec th imp def pre_tm post_tm
932  in save_thm("X86_LISP_SUB1_" ^ (int_to_string i),result) end;
933
934fun X86_LISP_ADD1 i = let
935  val st = x86_reg i
936  val s = x86_encode ("add "^st^",4")
937  val (spec,_,sts,_) = x86_tools
938  val ((th,_,_),_) = spec s
939  val th = HIDE_STATUS_RULE true sts th
940  val imp = lisp_inv_ADD1
941  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
942  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
943  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
944  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
945  val imp = RW1 [GSYM AND_IMP_INTRO] imp
946  val def = xLISP_def
947  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
948  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
949  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
950  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
951  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
952  val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)``
953  val post_tm = subst [v|->tm] post_tm
954  val result = prove_spec th imp def pre_tm post_tm
955  in save_thm("X86_LISP_ADD1_" ^ (int_to_string i),result) end;
956
957val _ = map X86_LISP_SUB1 [1,2,3,4,5,6]
958val _ = map X86_LISP_ADD1 [1,2,3,4,5,6]
959
960fun PPC_LISP_SUB1 i = let
961  val st = int_to_string (i+2)
962  val s = ppc_encode ("addi "^st^","^st^",-4")
963  val (spec,_,sts,_) = ppc_tools
964  val ((th,_,_),_) = spec s
965  val imp = lisp_inv_SUB1
966  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
967  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
968  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
969  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
970  val imp = RW1 [GSYM AND_IMP_INTRO] imp
971  val def = pLISP_def
972  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
973  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w)``
974  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
975  val tm = subst [``x:SExp``|->v] ``LISP_SUB x (Val 1)``
976  val post_tm = subst [v|->tm] post_tm
977  val result = prove_spec th imp def pre_tm post_tm
978  in save_thm("PPC_LISP_SUB1_" ^ (int_to_string i),result) end;
979
980fun PPC_LISP_ADD1 i = let
981  val st = int_to_string (i+2)
982  val s = ppc_encode ("addi "^st^","^st^",4")
983  val (spec,_,sts,_) = ppc_tools
984  val ((th,_,_),_) = spec s
985  val imp = lisp_inv_ADD1
986  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
987  val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i)))
988  val imp = UNDISCH (RW [AND_IMP_INTRO] imp)
989  val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp)
990  val imp = RW1 [GSYM AND_IMP_INTRO] imp
991  val def = pLISP_def
992  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p``
993  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w)``
994  val v = Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]
995  val tm = subst [``x:SExp``|->v] ``LISP_ADD x (Val 1)``
996  val post_tm = subst [v|->tm] post_tm
997  val result = prove_spec th imp def pre_tm post_tm
998  in save_thm("PPC_LISP_ADD1_" ^ (int_to_string i),result) end;
999
1000val _ = map PPC_LISP_SUB1 [1,2,3,4,5,6]
1001val _ = map PPC_LISP_ADD1 [1,2,3,4,5,6]
1002
1003
1004(* less *)
1005
1006val ARM_LISP_LESS = let
1007  val (arm_spec,_,sts,_) = arm_tools
1008  val ((th,_,_),_) = arm_spec "E1530004"
1009  val imp = lisp_inv_LESS
1010  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1011  val imp = RW1 [EQ_SYM_EQ] imp
1012  val th = RW [GSYM WORD_NOT_LOWER] th
1013  val th = HIDE_PRE_STATUS_RULE sts th
1014  val th = HIDE_POST_RULE ``aS1 psrN`` th
1015  val th = HIDE_POST_RULE ``aS1 psrZ`` th
1016  val th = HIDE_POST_RULE ``aS1 psrV`` th
1017  val def = aLISP_def
1018  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1019  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * ~(aS1 psrZ) * aS1 psrC ~(getVal x1 < getVal x2) * ~(aS1 psrV)``
1020  val result = prove_spec th imp def pre_tm post_tm
1021  in save_thm("ARM_LISP_LESS",result) end;
1022
1023val X86_LISP_LESS = let
1024  val s = x86_encode "cmp eax,ecx"
1025  val (spec,_,sts,_) = x86_tools
1026  val ((th,_,_),_) = spec s
1027  val imp = lisp_inv_LESS
1028  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1029  val imp = RW1 [EQ_SYM_EQ] imp
1030  val th = RW [GSYM WORD_NOT_LOWER] th
1031  val th = HIDE_PRE_STATUS_RULE sts th
1032  val th = HIDE_POST_RULE ``xS1 X_PF`` th
1033  val th = HIDE_POST_RULE ``xS1 X_SF`` th
1034  val th = HIDE_POST_RULE ``xS1 X_AF`` th
1035  val th = HIDE_POST_RULE ``xS1 X_OF`` th
1036  val th = HIDE_POST_RULE ``xS1 X_ZF`` th
1037  val def = xLISP_def
1038  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
1039  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC (eip + 0x2w) * ~(xS1 X_AF) * ~(xS1 X_OF) *
1040        ~(xS1 X_SF) * ~(xS1 X_ZF) * ~(xS1 X_PF) * xS1 X_CF (SOME (getVal x1 < getVal x2))``
1041  val result = prove_spec th imp def pre_tm post_tm
1042  in save_thm("X86_LISP_LESS",result) end;
1043
1044val PPC_LISP_LESS = let
1045  val s = ppc_encode "cmplw 3,4"
1046  val (spec,_,sts,_) = ppc_tools
1047  val ((th,_,_),_) = spec s
1048  val imp = lisp_inv_LESS
1049  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1050  val imp = RW1 [EQ_SYM_EQ] imp
1051  val th = RW [GSYM WORD_NOT_LOWER] th
1052  val th = HIDE_PRE_STATUS_RULE sts th
1053  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
1054  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x2w)`` th
1055  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
1056  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
1057  val def = pLISP_def
1058  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1059  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p + 0x4w) *
1060    pS1 (PPC_CR0 0x0w) (SOME (getVal x1 < getVal x2)) * ~pS1 PPC_CARRY *
1061    ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x2w) * ~pS1 (PPC_CR0 0x3w)``
1062  val result = prove_spec th imp def pre_tm post_tm
1063  in save_thm("PPC_LISP_LESS",result) end;
1064
1065
1066(* mult, div and mod *)
1067
1068open divideTheory;
1069
1070val ARM_LISP_MULT = let
1071  val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_arm_thm
1072  val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1073  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1074  val th = SPEC (mk_var("r5",``:word32``)) th
1075  val imp = lisp_inv_MULT
1076  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1077  val def = aLISP_def
1078  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p``
1079  val post_tm = set_pc th ``aLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p``
1080  val result = prove_spec th imp def pre_tm post_tm
1081  in save_thm("ARM_LISP_MULT",result) end;
1082
1083val PPC_LISP_MULT = let
1084  val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_ppc_thm
1085  val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th
1086  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1087  val th = SPEC (mk_var("r5",``:word32``)) th
1088  val imp = lisp_inv_MULT
1089  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1090  val def = pLISP_def
1091  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1092  val post_tm = set_pc th ``pLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS``
1093  val result = prove_spec th imp def pre_tm post_tm
1094  in save_thm("PPC_LISP_MULT",result) end;
1095
1096val X86_LISP_MULT = let
1097  val th = SIMP_RULE std_ss [lisp_word_mul_def,LET_DEF,SEP_CLAUSES] lisp_word_mul_x86_thm
1098  val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1099  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1100  val th = Q.SPEC `edx` th
1101  val imp = lisp_inv_MULT
1102  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1103  val def = xLISP_def
1104  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
1105  val post_tm = set_pc th ``xLISP (LISP_MULT x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS``
1106  val result = prove_spec th imp def pre_tm post_tm
1107  in save_thm("X86_LISP_MULT",result) end;
1108
1109val ARM_LISP_DIV = let
1110  val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_arm_thm
1111  val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `aR 5w` SEP_HIDE_def])) th
1112  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1113  val th = SPEC (mk_var("r5",``:word32``)) th
1114  val imp = lisp_inv_DIV
1115  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1116  val def = aLISP_def
1117  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1118  val post_tm = set_pc th ``aLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p * ~aS``
1119  val result = prove_spec th imp def pre_tm post_tm
1120  in save_thm("ARM_LISP_DIV",result) end;
1121
1122val PPC_LISP_DIV = let
1123  val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_ppc_thm
1124  val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th
1125  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1126  val th = SPEC (mk_var("r5",``:word32``)) th
1127  val imp = lisp_inv_DIV
1128  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1129  val def = pLISP_def
1130  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1131  val post_tm = set_pc th ``pLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS``
1132  val result = prove_spec th imp def pre_tm post_tm
1133  in save_thm("PPC_LISP_DIV",result) end;
1134
1135val X86_LISP_DIV = let
1136  val th = SIMP_RULE std_ss [lisp_word_div_def,LET_DEF,SEP_CLAUSES] lisp_word_div_x86_thm
1137  val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1138  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1139  val th = Q.SPEC `edx` th
1140  val imp = lisp_inv_DIV
1141  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1142  val def = xLISP_def
1143  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
1144  val post_tm = set_pc th ``xLISP (LISP_DIV x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS``
1145  val result = prove_spec th imp def pre_tm post_tm
1146  in save_thm("X86_LISP_DIV",result) end;
1147
1148val ARM_LISP_MOD = let
1149  val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_arm_thm
1150  val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `aR 5w` SEP_HIDE_def])) th
1151  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1152  val th = SPEC (mk_var("r5",``:word32``)) th
1153  val imp = lisp_inv_MOD
1154  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1155  val def = aLISP_def
1156  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1157  val post_tm = set_pc th ``aLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * aPC p * ~aS``
1158  val result = prove_spec th imp def pre_tm post_tm
1159  in save_thm("ARM_LISP_MOD",result) end;
1160
1161val PPC_LISP_MOD = let
1162  val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_ppc_thm
1163  val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [Q.ISPEC `pR 5w` SEP_HIDE_def])) th
1164  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1165  val th = SPEC (mk_var("r5",``:word32``)) th
1166  val imp = lisp_inv_MOD
1167  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1168  val def = pLISP_def
1169  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1170  val post_tm = set_pc th ``pLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * pPC p * ~pS``
1171  val result = prove_spec th imp def pre_tm post_tm
1172  in save_thm("PPC_LISP_MOD",result) end;
1173
1174val X86_LISP_MOD = let
1175  val th = SIMP_RULE std_ss [lisp_word_mod_def,LET_DEF,SEP_CLAUSES] lisp_word_mod_x86_thm
1176  val th = RW [Q.SPEC `f y` SEP_HIDE_def] th
1177  val th = SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th
1178  val th = Q.SPEC `edx` th
1179  val imp = lisp_inv_MOD
1180  val imp = RW1 [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1181  val def = xLISP_def
1182  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC p * ~xS``
1183  val post_tm = set_pc th ``xLISP (LISP_MOD x1 x2,Sym "nil",Sym "nil",x4,x5,x6,limit) * xPC p * ~xS``
1184  val result = prove_spec th imp def pre_tm post_tm
1185  in save_thm("X86_LISP_MOD",result) end;
1186
1187
1188(* test eq *)
1189
1190val ARM_LISP_EQ = let
1191  val _ = print "a"
1192  val i = 1
1193  val j = 2
1194  val (arm_spec,_,sts,_) = arm_tools
1195  val inst = "E13"^(int_to_string (i+2))^"000"^(int_to_string (j+2))
1196  val ((th,_,_),_) = arm_spec inst
1197  val th = RW [WORD_EQ_XOR_ZERO] th
1198  val th = HIDE_POST_RULE ``aS1 psrN`` th
1199  val th = HIDE_POST_RULE ``aS1 psrC`` th
1200  val th = HIDE_POST_RULE ``aS1 psrV`` th
1201  val th = HIDE_PRE_STATUS_RULE sts th
1202  val def = aLISP_def
1203  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1204  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = y:SExp) * ~(aS1 psrC) * ~(aS1 psrV)``
1205  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1206  val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm
1207  val imp = lisp_inv_eq
1208  val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1209  val result = prove_spec th imp def pre_tm post_tm
1210  in save_thm("ARM_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end;
1211
1212val X86_LISP_EQ = let
1213  val _ = print "x"
1214  val i = 1
1215  val j = 2
1216  val s = "cmp " ^ (x86_reg i) ^ ", " ^ (x86_reg j)
1217  val s = x86_encode s
1218  val (spec,_,sts,_) = x86_tools
1219  val ((th,_,_),_) = spec s
1220  val th = RW [WORD_EQ_SUB_ZERO] th
1221  val th = HIDE_PRE_STATUS_RULE sts th
1222  val th = HIDE_POST_RULE ``xS1 X_PF`` th
1223  val th = HIDE_POST_RULE ``xS1 X_SF`` th
1224  val th = HIDE_POST_RULE ``xS1 X_AF`` th
1225  val th = HIDE_POST_RULE ``xS1 X_OF`` th
1226  val th = HIDE_POST_RULE ``xS1 X_CF`` th
1227  val def = xLISP_def
1228  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
1229  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = y:SExp)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
1230  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1231  val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm
1232  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
1233  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
1234  val imp = lisp_inv_eq
1235  val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1236  val result = prove_spec th imp def pre_tm post_tm
1237  in save_thm("X86_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end;
1238
1239val PPC_LISP_EQ = let
1240  val _ = print "p"
1241  val i = 1
1242  val j = 2
1243  val s = "cmpw " ^ (int_to_string (i+2)) ^ ", " ^ (int_to_string (j+2))
1244  val s = ppc_encode s
1245  val (spec,_,sts,_) = ppc_tools
1246  val ((th,_,_),_) = spec s
1247  val th = RW [WORD_EQ_SUB_ZERO] th
1248  val th = HIDE_PRE_STATUS_RULE sts th
1249  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
1250  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th
1251  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
1252  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
1253  val def = pLISP_def
1254  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1255  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = y:SExp)) * ~(pS1 PPC_CARRY) *
1256      ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)``
1257  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1258  val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm
1259  val imp = lisp_inv_eq
1260  val imp = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] imp))
1261  val result = prove_spec th imp def pre_tm post_tm
1262  in save_thm("PPC_LISP_EQ" ^ (int_to_string i) ^ (int_to_string j),result) end;
1263
1264
1265(* test symbol *)
1266
1267fun ARM_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1268  val _ = print "a"
1269  val (arm_spec,_,sts,_) = arm_tools
1270  val s = Arbnum.toHexString(Arbnum.fromInt j)
1271  val s = if size(s) < 2 then "0" ^ s else s
1272  val ((th,_,_),_) = arm_spec ("E33"^(int_to_string (i+2))^"00"^s)
1273  val th = RW [WORD_EQ_XOR_ZERO] th
1274  val th = HIDE_POST_RULE ``aS1 psrN`` th
1275  val th = HIDE_POST_RULE ``aS1 psrC`` th
1276  val th = HIDE_POST_RULE ``aS1 psrV`` th
1277  val th = HIDE_PRE_STATUS_RULE sts th
1278  val def = aLISP_def
1279  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1280  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = Sym str) * ~(aS1 psrC) * ~(aS1 psrV)``
1281  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1282  val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm
1283  val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i)))
1284  val imp = RW1 [EQ_SYM_EQ] imp
1285  val result = prove_spec th imp def pre_tm post_tm
1286  val result = RW [GSYM rw] result
1287  in save_thm("ARM_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end;
1288
1289fun X86_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1290  val _ = print "x"
1291  val s = "cmp " ^ (x86_reg i) ^ ", " ^ int_to_string j
1292  val s = x86_encode s
1293  val (spec,_,sts,_) = x86_tools
1294  val ((th,_,_),_) = spec s
1295  val th = RW [WORD_EQ_SUB_ZERO] th
1296  val th = HIDE_PRE_STATUS_RULE sts th
1297  val th = HIDE_POST_RULE ``xS1 X_PF`` th
1298  val th = HIDE_POST_RULE ``xS1 X_SF`` th
1299  val th = HIDE_POST_RULE ``xS1 X_AF`` th
1300  val th = HIDE_POST_RULE ``xS1 X_OF`` th
1301  val th = HIDE_POST_RULE ``xS1 X_CF`` th
1302  val def = xLISP_def
1303  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
1304  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = Sym str)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
1305  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1306  val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm
1307  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
1308  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
1309  val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i)))
1310  val imp = RW1 [EQ_SYM_EQ] imp
1311  val result = prove_spec th imp def pre_tm post_tm
1312  val result = RW [GSYM rw] result
1313  in save_thm("X86_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end;
1314
1315fun PPC_LISP_EQ_SYMBOL (i,name,rw) (j,str) = let
1316  val _ = print "p"
1317  val s = "cmpwi " ^ (int_to_string (i+2)) ^ ", " ^ int_to_string j
1318  val s = ppc_encode s
1319  val (spec,_,sts,_) = ppc_tools
1320  val ((th,_,_),_) = spec s
1321  val th = RW [WORD_EQ_SUB_ZERO] th
1322  val th = HIDE_PRE_STATUS_RULE sts th
1323  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
1324  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th
1325  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
1326  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
1327  val def = pLISP_def
1328  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1329  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = Sym str)) * ~(pS1 PPC_CARRY) *
1330      ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)``
1331  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1332  val post_tm = subst [``str:string`` |-> (stringSyntax.fromMLstring str)] post_tm
1333  val imp = DISCH_ALL (MATCH_MP lisp_inv_builtin (UNDISCH (swap_thm i)))
1334  val imp = RW1 [EQ_SYM_EQ] imp
1335  val result = prove_spec th imp def pre_tm post_tm
1336  val result = RW [GSYM rw] result
1337  in save_thm("PPC_LISP_SYMBOL" ^ name ^ "_" ^ (int_to_string j),result) end;
1338
1339val list = let
1340  val th = SIMP_CONV std_ss [builtin_symbols_set_def,word_add_n2w] ``builtin_symbols_set 3w``
1341  val xs = (helperLib.list_dest (pred_setSyntax.dest_insert) o snd o dest_eq o concl) th
1342  val xs = map pairSyntax.dest_pair (tl (rev xs))
1343  val xs = map (fn (x,y) => (numSyntax.int_of_term ((snd (dest_comb x))), stringSyntax.fromHOLstring y)) xs
1344  in rev xs end
1345
1346val _ = map (ARM_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list];
1347val _ = map (X86_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list];
1348val _ = map (PPC_LISP_EQ_SYMBOL (1,"_EXP",TRUTH)) [hd list];
1349
1350val _ = map (ARM_LISP_EQ_SYMBOL (2,"",TRUTH)) list;
1351val _ = map (X86_LISP_EQ_SYMBOL (2,"",TRUTH)) list;
1352val _ = map (PPC_LISP_EQ_SYMBOL (2,"",TRUTH)) list;
1353
1354val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil")
1355val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t")
1356val _ = ARM_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote")
1357
1358val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil")
1359val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t")
1360val _ = X86_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote")
1361
1362val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_EVAL_def) (3,"nil")
1363val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_CONT_def) (15,"t")
1364val _ = PPC_LISP_EQ_SYMBOL (4,"_TASK",TASK_FUNC_def) (27,"quote")
1365
1366
1367(* test for zero *)
1368
1369val lisp_inv_test_zero = (SIMP_RULE std_ss [] o Q.SPEC `0`) lisp_inv_eq_0
1370
1371fun ARM_LISP_EQ_ZERO i = let
1372  val _ = print "a"
1373  val (arm_spec,_,sts,_) = arm_tools
1374  val ((th,_,_),_) = arm_spec ("E33"^(int_to_string (i+2))^"0002")
1375  val th = RW [WORD_EQ_XOR_ZERO] th
1376  val th = HIDE_POST_RULE ``aS1 psrN`` th
1377  val th = HIDE_POST_RULE ``aS1 psrC`` th
1378  val th = HIDE_POST_RULE ``aS1 psrV`` th
1379  val th = HIDE_PRE_STATUS_RULE sts th
1380  val def = aLISP_def
1381  val pre_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC p * ~aS``
1382  val post_tm = ``aLISP (x1,x2,x3,x4,x5,x6,limit) * aPC (p + 0x4w) * ~(aS1 psrN) * aS1 psrZ (x = Val 0) * ~(aS1 psrC) * ~(aS1 psrV)``
1383  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1384  val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i)))
1385  val imp = RW1 [EQ_SYM_EQ] imp
1386  val result = prove_spec th imp def pre_tm post_tm
1387  in save_thm("ARM_LISP_EQ_ZERO_" ^ (int_to_string i),result) end;
1388
1389fun X86_LISP_EQ_ZERO i = let
1390  val _ = print "x"
1391  val s = "cmp " ^ (x86_reg i) ^ ", 2"
1392  val s = x86_encode s
1393  val (spec,_,sts,_) = x86_tools
1394  val ((th,_,_),_) = spec s
1395  val th = RW [WORD_EQ_SUB_ZERO] th
1396  val th = HIDE_PRE_STATUS_RULE sts th
1397  val th = HIDE_POST_RULE ``xS1 X_PF`` th
1398  val th = HIDE_POST_RULE ``xS1 X_SF`` th
1399  val th = HIDE_POST_RULE ``xS1 X_AF`` th
1400  val th = HIDE_POST_RULE ``xS1 X_OF`` th
1401  val th = HIDE_POST_RULE ``xS1 X_CF`` th
1402  val def = xLISP_def
1403  val pre_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * ~xS``
1404  val post_tm = ``xLISP (x1,x2,x3,x4,x5,x6,limit) * xPC eip * xS1 X_ZF (SOME (x = Val 0)) * ~xS1 X_PF * ~xS1 X_SF * ~xS1 X_AF * ~xS1 X_OF * ~xS1 X_CF``
1405  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1406  val tm = find_term (can (match_term ``xPC (eip + n2w n)``)) (concl th)
1407  val post_tm = subst [``eip:word32`` |-> cdr tm] post_tm
1408  val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i)))
1409  val imp = RW1 [EQ_SYM_EQ] imp
1410  val result = prove_spec th imp def pre_tm post_tm
1411  in save_thm("X86_LISP_EQ_ZERO_" ^ (int_to_string i),result) end;
1412
1413fun PPC_LISP_EQ_ZERO i = let
1414  val _ = print "p"
1415  val s = "cmpwi " ^ (int_to_string (i+2)) ^ ", 2"
1416  val s = ppc_encode s
1417  val (spec,_,sts,_) = ppc_tools
1418  val ((th,_,_),_) = spec s
1419  val th = RW [WORD_EQ_SUB_ZERO] th
1420  val th = HIDE_PRE_STATUS_RULE sts th
1421  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x1w)`` th
1422  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x0w)`` th
1423  val th = HIDE_POST_RULE ``pS1 (PPC_CR0 0x3w)`` th
1424  val th = HIDE_POST_RULE ``pS1 (PPC_CARRY)`` th handle e => th
1425  val def = pLISP_def
1426  val pre_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC p * ~pS``
1427  val post_tm = ``pLISP (x1,x2,x3,x4,x5,x6,limit) * pPC (p+4w) * pS1 (PPC_CR0 2w) (SOME (x = Val 0)) * ~(pS1 PPC_CARRY) *
1428      ~pS1 (PPC_CR0 0x1w) * ~pS1 (PPC_CR0 0x0w) * ~pS1 (PPC_CR0 0x3w)``
1429  val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm
1430  val imp = DISCH_ALL (MATCH_MP lisp_inv_test_zero (UNDISCH (swap_thm i)))
1431  val imp = RW1 [EQ_SYM_EQ] imp
1432  val result = prove_spec th imp def pre_tm post_tm
1433  in save_thm("PPC_LISP_EQ_ZERO_" ^ (int_to_string i),result) end;
1434
1435val _ = map ARM_LISP_EQ_ZERO [1,2,3,4,5,6];
1436val _ = map X86_LISP_EQ_ZERO [1,2,3,4,5,6];
1437val _ = map PPC_LISP_EQ_ZERO [1,2,3,4,5,6];
1438
1439
1440val _ = export_theory();
1441