1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_ops"; 2val _ = ParseExtras.temp_loose_equality() 3open lisp_symbolsTheory lisp_sexpTheory lisp_consTheory lisp_invTheory; 4open lisp_equalTheory lisp_codegenTheory lisp_initTheory lisp_symbolsTheory; 5 6(* --- *) 7 8open compilerLib codegenLib decompilerLib; 9open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 10open combinTheory finite_mapTheory addressTheory bitTheory; 11 12open progTheory set_sepTheory helperLib; 13open prog_x64Theory prog_x64Lib x64_encodeLib; 14open stop_and_copyTheory; 15 16infix \\ 17val op \\ = op THEN; 18val RW = REWRITE_RULE; 19val RW1 = ONCE_REWRITE_RULE; 20 21val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst; 22val REST = LISP |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 23val STATINV = LISP |> car |> car |> cdr; 24val VAR_REST = LISP |> car |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 25 26(* 27 28Use of cs list: 29 EL 0..2 cs -- used by zIO 30 EL 3 cs -- used by parser, size of array to allocate (init only) 31 EL 4 cs -- code heap: pointer to start of code heap 32 EL 5 cs -- code heap: length (in bytes) of code heap (init only) 33 34 EL 3 cs -- code pointer: parse DONE 35 EL 5 cs -- code pointer: gc DONE 36 EL 6 cs -- code pointer: equal DONE 37 EL 7 cs -- code pointer: print DONE 38 EL 8 cs -- code pointer: compile DONE 39 EL 9 cs -- code pointer: compile instruction DONE 40 41*) 42 43 44val zCODE_MEMORY_def = Define ` 45 (zCODE_MEMORY NONE dd d = emp) /\ 46 (zCODE_MEMORY (SOME F) dd d = zBYTE_MEMORY dd d) /\ 47 (zCODE_MEMORY (SOME T) dd d = zCODE (zCODE_SET dd d))`; 48 49val zCODE_UNCHANGED_def = Define ` 50 (zCODE_UNCHANGED NONE dd d = emp) /\ 51 (zCODE_UNCHANGED (SOME x) dd d = cond (x = (dd,d)))`; 52 53val zLISP_ALT_def = Define ` 54 zLISP_ALT side (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) = 55 SEP_EXISTS tw0 tw1 tw2 wsp bp sp w0 w1 w2 w3 w4 w5 wi we df f dg g bp2 ds sa1 sa2 sa3 dd d. 56 zR 0w tw0 * zR 1w tw1 * zR 2w tw2 * zR 3w wsp * zR 6w bp * zR 7w sp * 57 zR 8w (w2w w0) * zR 9w (w2w w1) * zR 10w (w2w w2) * 58 zR 11w (w2w w3) * zR 12w (w2w w4) * zR 13w (w2w w5) * zSTACK rbp qs * 59 zR 14w wi * zR 15w we * zMEMORY df f * zBYTE_MEMORY dg g * zCODE_MEMORY ddd dd d * 60 zIO (EL 0 cs,EL 1 cs,EL 2 cs,EL 0 ds) io * zCODE_UNCHANGED cu dd d * 61 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST) 62 (w0,w1,w2,w3,w4,w5,df,f,^REST) /\ 63 side wsp wi we ds tw2)`; 64 65val zLISP_R_def = Define ` 66 zLISP_R (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) = 67 SEP_EXISTS tw0 tw1 tw2 wsp bp sp w0 w1 w2 w3 w4 w5 wi we df f dg g bp2 ds sa1 sa2 sa3 dd d. 68 zR 0w tw0 * zR 2w (EL 1 cs) * zR 3w wsp * zR 6w bp * zR 7w sp * 69 zR 8w (w2w w0) * zR 9w (w2w w1) * zR 10w (w2w w2) * 70 zR 11w (w2w w3) * zR 12w (w2w w4) * zR 13w (w2w w5) * zSTACK rbp qs * 71 zR 14w wi * zR 15w we * zMEMORY df f * zBYTE_MEMORY dg g * zCODE_MEMORY ddd dd d * 72 zIO_R (EL 0 cs,EL 1 cs,EL 2 cs) io * zCODE_UNCHANGED cu dd d * 73 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST) 74 (w0,w1,w2,w3,w4,w5,df,f,^REST))`; 75 76val zLISP_INIT_def = Define ` 77 zLISP_INIT (a1,a2,sl,sl1,e,ex,rbp,cs,qs,ddd,cu) io = 78 SEP_EXISTS df f dg g sp sa1 sa_len ds dd d. 79 zBYTE_MEMORY dg g * zCODE_MEMORY ddd dd d * zMEMORY df f * ~zR 0x0w * 80 ~zR 0x1w * ~zR 0x2w * ~zR 0x3w * ~zR 0x6w * zR 0x7w sp * zSTACK rbp qs * 81 ~zR 0xBw * ~zR 0x9w * ~zR 0xDw * ~zR 0x8w * ~zR 0xCw * ~zR 0xAw * 82 ~zR 0xEw * ~zR 0xFw * zIO (EL 0 cs,EL 1 cs,EL 2 cs,EL 0 ds) io * 83 zCODE_UNCHANGED cu dd d * 84 cond (lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds))`; 85 86val zLISP_raw = Define `zLISP = zLISP_ALT (\wsp wi we ds tw2. T)`; 87val zLISP_def = SIMP_CONV std_ss [zLISP_ALT_def,zLISP_raw] 88 ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 89val _ = save_thm("zLISP_def",zLISP_def); 90 91val SEP_IMP_zLISP_ALT_zLISP = prove( 92 ``SEP_IMP (zLISP_ALT side vars1 vars2 * p) (zLISP vars1 vars2 * p)``, 93 Q.SPEC_TAC (`vars1`,`vars1`) \\ Q.SPEC_TAC (`vars2`,`vars2`) 94 \\ SIMP_TAC std_ss [FORALL_PROD] \\ REPEAT STRIP_TAC 95 \\ MATCH_MP_TAC SEP_IMP_STAR \\ SIMP_TAC std_ss [SEP_IMP_REFL] 96 \\ SIMP_TAC std_ss [zLISP_def,zLISP_ALT_def] 97 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM,cond_STAR] \\ METIS_TAC []); 98 99val STAT = zLISP_def |> SPEC_ALL |> concl |> dest_eq |> fst |> car |> cdr; 100 101val zLISP_FAIL_def = Define ` 102 zLISP_FAIL (a1,a2,sl,sl1,e,ex,cs,rbp,dd,cu) = 103 SEP_EXISTS ddd vars. zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) vars * 104 ~zS * zPC ex * cond ((dd = NONE) ==> (ddd = dd))`; 105 106val _ = set_echo 0; 107val (i,j) = (2,4) 108val (spec,_,sts,_) = x64_tools 109 110(* automation *) 111 112fun dest_sep_exists tm = let 113 val (x,y) = dest_comb tm 114 val _ = if (fst o dest_const) x = "SEP_EXISTS" then () else fail() 115 in dest_abs y end; 116 117fun dest_sep_cond tm = 118 if (fst o dest_const o fst o dest_comb) tm = "cond" 119 then snd (dest_comb tm) else fail(); 120 121val prove_spec_blast = prove( 122 ``((w2w (w1:word32) && 0x1w = 0x0w:word64) = (w1 && 0x1w = 0x0w)) /\ 123 ((w2w w1 = (w2w w2):word64) = (w1 = (w2:word32))) /\ 124 ((w2w w1 <+ (w2w w2):word64) = (w1 <+ (w2:word32))) /\ 125 (w2w ((w2w w1):word64) = w1) /\ 126 ((31 -- 0) (w2w w1 - 0x4w) = (w2w (w1 - 4w)):word64) /\ 127 ((w2w ((w2w w):word32)):word64 = (31 -- 0) w)``, 128 blastLib.BBLAST_TAC); 129 130val prove_spec_eval = LIST_CONJ [EVAL ``(w2w:word32->word64) 1w``, 131 EVAL ``(w2w:word32->word64) 3w``, 132 EVAL ``(w2w:word32->word64) 5w``, 133 EVAL ``(w2w:word32->word64) 11w``]; 134 135fun AUTO_EXISTS_TAC (asm,tm) = let 136 fun ex tm = let 137 val (v,tm) = dest_exists tm 138 in v :: ex tm end handle e => [] 139 val xs = ex tm 140 val x = hd (list_dest dest_conj (repeat (snd o dest_exists) tm)) 141 val tm2 = hd (filter (can (match_term ``lisp_inv xx yy zz``)) asm) 142 val (s,_) = match_term x tm2 143 val ys = map (subst s) xs 144 fun exx [] = ALL_TAC | exx (x::xs) = EXISTS_TAC x THEN exx xs 145 in exx ys (asm,tm) end 146 147fun prove_spec th imp def pre_tm post_tm = let 148 val lemma = SIMP_CONV std_ss [SEP_HIDE_def] ``~zR x`` 149 val th = CONV_RULE (RATOR_CONV (REWRITE_CONV [lemma])) th 150 val th = SPEC_ALL (SIMP_RULE std_ss [SEP_CLAUSES,GSYM SPEC_PRE_EXISTS] th) 151 val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th 152 val tm = (cdr o concl o SPEC_ALL) def 153 val tm = repeat (snd o dest_sep_exists) tm 154 val fill = list_dest dest_star tm 155 val res = list_dest dest_star p 156 val res2 = filter (not o can dest_sep_cond) res 157 val fill2 = filter (not o can dest_sep_cond) fill 158 val res3 = map dest_comb (filter (not o can dest_sep_hide) res2) 159 val fill3 = map dest_comb (filter (not o can dest_sep_hide) fill2) 160 fun rename [] (y1,y2) = (y2,y2) 161 | rename ((x1,x2)::xs) (y1,y2) = if x1 ~~ y1 then (y2,x2) 162 else rename xs (y1,y2) 163 val s = map (fn (x,y) => x |-> y) 164 (filter (fn x => is_var (fst x)) 165 (map (fn (x,y) => if is_comb x then (cdr x,cdr y handle HOL_ERR _ => y) else (x,y)) (map (rename fill3) res3))) 166 val th = INST s th 167 val th = UNDISCH_ALL (RW [SPEC_MOVE_COND] (SIMP_RULE (bool_ss++sep_cond_ss) [] th)) 168 val (m,p,_,q) = (dest_spec o concl o SPEC_ALL) th 169 val fill = list_dest dest_star tm 170 val res = list_dest dest_star p 171 val fs = (filter (fn x => not (tmem x res)) fill) 172 val fs = if can (find_term (aconv ``zCODE_MEMORY``)) (concl th) then 173 filter (fn tm => repeat car tm !~ ``zCODE_MEMORY``) fs else fs 174 val f = list_mk_star fs (type_of (hd fill)) 175 val th = SPEC f (MATCH_MP SPEC_FRAME th) 176 val pre = (fst o dest_imp o snd o dest_imp) (concl imp) handle e => ``T:bool`` 177 val (_,p,_,_) = dest_spec (concl (PURE_REWRITE_RULE [GSYM SPEC_MOVE_COND] (DISCH pre th))) 178 val x = (snd o dest_star) p 179 val tmi = (fst o dest_eq o concl o SPEC_ALL) def 180 val tmj = hd (list_dest dest_star pre_tm) 181 val th = INST (fst (match_term tmi tmj)) th 182 val th = SPEC x (MATCH_MP SPEC_FRAME th) 183 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN th) 184 val goal = (cdr o car o concl) th 185 val lemma = prove(goal, 186(* 187 set_goal([],goal) 188*) 189 REWRITE_TAC [STAR_ASSOC,prove_spec_blast] 190 \\ SIMP_TAC (std_ss++sep_cond_ss) [] 191 \\ REWRITE_TAC [SEP_IMP_MOVE_COND] 192 \\ REPEAT STRIP_TAC 193 \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp) 194 \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC)) 195 \\ ASM_SIMP_TAC std_ss [LET_DEF,prove_spec_blast] 196 \\ SIMP_TAC std_ss [def,SEP_CLAUSES] 197 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] 198 \\ REPEAT STRIP_TAC 199 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 200 \\ REPEAT (Q.PAT_X_ASSUM `!xxx.bbb` (ASSUME_TAC o SPEC_ALL)) 201 \\ AUTO_EXISTS_TAC 202 \\ FULL_SIMP_TAC std_ss [prove_spec_eval,prove_spec_blast,EL_UPDATE_NTH] 203 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_n2w,bitTheory.BITS_THM] 204 \\ FULL_SIMP_TAC (std_ss++star_ss) [AC WORD_MULT_COMM WORD_MULT_ASSOC] 205 \\ METIS_TAC []) 206 val th = MATCH_MP th lemma 207 val th = RW [GSYM SPEC_MOVE_COND] (DISCH_ALL th) 208 val tm = (cdr o concl o SPEC_ALL) def 209 fun ff tm = let val (x,y) = dest_sep_exists tm in x :: ff y end handle e => [] 210 val zs = ff tm 211 fun gg [] th = th 212 | gg (x::xs) th = gg xs (EXISTS_PRE [ANTIQUOTE x] th) 213 val th = gg zs th 214 val th = MATCH_MP SPEC_STRENGTHEN th 215 val th = SPEC (mk_cond_star(pre_tm,pre)) th 216 val goal = (cdr o car o concl) th 217 val lemma = prove(goal, 218(* 219 set_goal([],goal) 220*) 221 SIMP_TAC std_ss [def,SEP_CLAUSES] 222 \\ SIMP_TAC (bool_ss++sep_cond_ss) [] 223 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM,cond_STAR] 224 \\ REPEAT STRIP_TAC 225 \\ AUTO_EXISTS_TAC 226 \\ FULL_SIMP_TAC std_ss [] 227 \\ IMP_RES_TAC (SIMP_RULE std_ss [] imp) 228 \\ FULL_SIMP_TAC std_ss [] 229 \\ REPEAT (Q.PAT_X_ASSUM `xx ==> yy` (K ALL_TAC)) 230 \\ FULL_SIMP_TAC std_ss [] 231 \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ METIS_TAC []) 232 val th = MATCH_MP th lemma 233 val th = RW [SEP_CLAUSES] th 234 in th end; 235 236fun set_pc th = let 237 val (_,_,_,q) = (dest_spec o concl o UNDISCH_ALL) th 238 val tm = find_term (fn x => tmem (car x) [``zPC``,``xPC``,``aPC``,``pPC``] 239 handle e => false) q 240 in subst [``p:word64``|->cdr tm,``rip:word64``|->cdr tm] end 241 242fun swap_thm 0 = lisp_inv_swap0 243 | swap_thm 1 = lisp_inv_swap1 244 | swap_thm 2 = lisp_inv_swap2 245 | swap_thm 3 = lisp_inv_swap3 246 | swap_thm 4 = lisp_inv_swap4 247 | swap_thm 5 = lisp_inv_swap5 248 | swap_thm _ = fail() 249 250fun x64_reg n = "r" ^ (int_to_string (n+8)) 251 252fun generate_swap i j = 253 if i = 0 then swap_thm j else 254 if j = 0 then swap_thm i else 255 if i = j then swap_thm 1 else 256 DISCH_ALL (MATCH_MP (swap_thm i) (MATCH_MP (swap_thm j) (UNDISCH (swap_thm i)))); 257 (* e.g. to swap 4 and 5 do generate_swap 4 5 *) 258 259fun generate_copy i j = 260 if i = j then generate_swap 0 0 else 261 if j = 1 then let 262 val sw0 = generate_swap 0 i 263 val sw1 = generate_swap 0 1 264 val th = MATCH_MP lisp_inv_copy (MATCH_MP sw1 (UNDISCH sw0)) 265 in DISCH_ALL (MATCH_MP sw0 th) end 266 else if i = 1 then let 267 val sw0 = generate_swap 0 j 268 val th = MATCH_MP lisp_inv_copy (UNDISCH sw0) 269 in DISCH_ALL (MATCH_MP sw0 th) end 270 else let 271 val sw0 = generate_swap 1 i 272 val sw1 = generate_swap 0 j 273 val th = MATCH_MP lisp_inv_copy (MATCH_MP sw1 (UNDISCH sw0)) 274 in DISCH_ALL (MATCH_MP sw0 (MATCH_MP sw1 th)) end; 275 (* e.g. to copy 5 into 3 do generate_copy 3 5 *) 276 277val all_regs = [0,1,2,3,4,5]; 278 279val all_reg_pairs = let 280 fun pairs x [] = [] | pairs x (y::ys) = (x,y) :: pairs x ys 281 fun cross [] ys = [] | cross (x::xs) ys = pairs x ys @ cross xs ys 282 in cross [0,1,2,3,4,5] [0,1,2,3,4,5] end; 283 284val all_distinct_reg_pairs = filter (fn (x,y) => not (x = y)) all_reg_pairs; 285 286fun save_lisp_thm (name,th) = let 287 val th = Q.INST [`rip`|->`p`] th 288 val _ = add_compiled [th] 289 in save_thm(name,th) end; 290 291 292(* stack operations *) 293 294val X64_LISP_CALL_R2 = save_thm("X64_LISP_CALL_R2", let 295 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 1 296 val imp = lisp_inv_stack |> Q.SPECL [`p+3w::qs`,`tw2`] 297 val def = zLISP_ALT_def 298 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 299 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+3w::qs,code,amnt,ok) * zPC r2`` 300 val res = prove_spec th imp def pre_tm post_tm 301 val res = RW [GSYM zLISP_raw] res 302 in res end); 303 304val X64_LISP_PUSH_R2 = save_thm("X64_LISP_PUSH_R2", let 305 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 2 306 val imp = lisp_inv_stack |> Q.SPECL [`r2::qs`,`tw2`] 307 val def = zLISP_ALT_def 308 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 309 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,r2::qs,code,amnt,ok) * zPC (p+2w)`` 310 val res = prove_spec th imp def pre_tm post_tm 311 val res = RW [GSYM zLISP_raw] res 312 in res end); 313 314val X64_LISP_RET = save_thm("X64_LISP_RET", let 315 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 3 316 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL 317 val def = zLISP_def 318 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 319 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (HD qs)`` 320 val res = prove_spec th imp def pre_tm post_tm 321 val res = res |> Q.INST [`qs`|->`q::qs`] |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES] 322 in res end); 323 324val X64_LISP_ALT_RET = save_thm("X64_LISP_ALT_RET", let 325 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 3 326 val th = SPEC_FRAME_RULE th ``~zS`` 327 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`tw2`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL 328 val def = zLISP_ALT_def 329 val pre_tm = ``zLISP_ALT b ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 330 val post_tm = ``zLISP_ALT b ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (HD qs) * ~zS`` 331 val res = prove_spec th imp def pre_tm post_tm 332 val res = res |> Q.INST [`qs`|->`q::qs`] |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES] 333 in res end); 334 335val X64_LISP_POP_R2 = save_thm("X64_LISP_POP_R2", let 336 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 4 337 val imp = lisp_inv_stack |> Q.SPECL [`TL qs`,`HD qs`] |> UNDISCH |> DISCH ``~(qs:word64 list = [])`` |> DISCH_ALL 338 val def = zLISP_ALT_def 339 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 340 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = HD qs) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (p+2w)`` 341 val res = prove_spec th imp def pre_tm post_tm 342 val res = res |> Q.INST [`qs`|->`q::qs`] |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES] 343 val res = RW [GSYM zLISP_raw] res 344 in res end); 345 346val X64_LISP_CALL_IMM = save_thm("X64_LISP_CALL_IMM", let 347 val th = zSTACK_PROPS |> SPEC_ALL |> CONJUNCTS |> el 5 348 val imp = lisp_inv_stack |> Q.SPECL [`p+6w::qs`,`tw2`] 349 val def = zLISP_def 350 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 351 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+6w::qs,code,amnt,ok) * zPC (p + n2w (6 + SIGN_EXTEND 32 64 (w2n (imm32:word32))))`` 352 val res = prove_spec th imp def pre_tm post_tm 353 in res end); 354 355 356(* move *) 357 358fun X64_LISP_MOVE (i,j) = let 359 val _ = print "z" 360 val s = "mov " ^ x64_reg i ^ ", " ^ x64_reg j 361 val s = x64_encode s 362 val (spec,_,_,_) = x64_tools 363 val ((th,_,_),_) = spec s 364 val def = zLISP_def 365 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 366 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 367 val (_,pre,_,post) = dest_spec (concl th) 368 val pre_tm = mk_star(pre_tm,find_term (can (match_term ``zPC x``)) pre) 369 val post_tm = mk_star(post_tm,find_term (can (match_term ``zPC x``)) post) 370 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("x" ^ int_to_string j)]] 371 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("w" ^ int_to_string j)]] 372 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 373 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 374 (w0,w1,w2,w3,w4,w5,df,f,^REST)`` 375 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 376 val imp = generate_copy i j 377 val result = prove_spec th imp def pre_tm post_tm 378 in save_lisp_thm("X64_LISP_MOVE" ^ int_to_string i ^ int_to_string j,result) end 379 380val _ = map X64_LISP_MOVE all_distinct_reg_pairs; 381 382 383(* car *) 384 385fun generate_car i = let 386 val th = CONJUNCT1 (UNDISCH (UNDISCH lisp_inv_car)) 387 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 388 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 389 val th1 = CONJUNCT2 (UNDISCH (UNDISCH lisp_inv_car)) 390 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 391 val th2 = UNDISCH (RW [AND_IMP_INTRO] th) 392 val th3 = UNDISCH (RW [AND_IMP_INTRO] th1) 393 in RW [GSYM AND_IMP_INTRO] (DISCH_ALL (CONJ th2 th3)) end; 394 395val car_blast = prove( 396 ``!w:word32 v u:word64. 397 ((31 -- 0) (w2w w) = (w2w w):word64) /\ 398 (4w * v + u = u + 4w * v)``, 399 blastLib.BBLAST_TAC); 400 401fun X64_LISP_CAR (i,j) = let 402 val _ = print "z" 403 val s = "mov " ^ x64_reg i ^ "d, [r6+4*" ^ x64_reg j ^ "]" 404 val s = x64_encode s 405 val (spec,_,_,_) = x64_tools 406 val ((th,_,_),_) = spec s 407 val def = zLISP_def 408 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 409 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 410 val (_,pre,_,post) = dest_spec (concl th) 411 val pre_tm = mk_star(pre_tm,find_term (can (match_term ``zPC x``)) pre) 412 val post_tm = mk_star(post_tm,find_term (can (match_term ``zPC x``)) post) 413 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CAR x" ^ int_to_string j)]] 414 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(f:word64->word32) (bp + 0x4w * w2w w" ^ int_to_string j ^ ")")]] 415 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 416 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 417 (w0,w1,w2,w3,w4,w5,df,f,^REST)`` 418 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 419 val imp = generate_copy i j 420 val imp = DISCH_ALL (MATCH_MP (generate_car i) (UNDISCH imp)) 421 val th = RW [car_blast] th 422 val result = prove_spec th imp def pre_tm post_tm 423 in save_lisp_thm("X64_LISP_CAR" ^ int_to_string i ^ int_to_string j,result) end 424 425val _ = map X64_LISP_CAR all_reg_pairs; 426 427 428(* cdr *) 429 430fun generate_cdr i = let 431 val th = CONJUNCT1 (UNDISCH (UNDISCH lisp_inv_cdr)) 432 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 433 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 434 val th1 = CONJUNCT2 (UNDISCH (UNDISCH lisp_inv_cdr)) 435 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 436 val th2 = UNDISCH (RW [AND_IMP_INTRO] th) 437 val th3 = UNDISCH (RW [AND_IMP_INTRO] th1) 438 in RW [GSYM AND_IMP_INTRO] (DISCH_ALL (CONJ th2 th3)) end; 439 440val cdr_blast = prove( 441 ``!w:word32 v u:word64. 442 ((31 -- 0) (w2w w) = (w2w w):word64) /\ 443 (4w * v + u + 4w = u + 4w * v + 4w)``, 444 blastLib.BBLAST_TAC); 445 446fun X64_LISP_CDR (i,j) = let 447 val _ = print "z" 448 val s = "mov " ^ x64_reg i ^ "d, [r6+4*" ^ x64_reg j ^ "+4]" 449 val s = x64_encode s 450 val (spec,_,_,_) = x64_tools 451 val ((th,_,_),_) = spec s 452 val def = zLISP_def 453 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 454 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`` 455 val (_,pre,_,post) = dest_spec (concl th) 456 val pre_tm = mk_star(pre_tm,find_term (can (match_term ``zPC x``)) pre) 457 val post_tm = mk_star(post_tm,find_term (can (match_term ``zPC x``)) post) 458 val s = [[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> [QUOTE ("CDR x" ^ int_to_string j)]] 459 val sw = [[QUOTE ("w" ^ int_to_string i ^ ":word32")] |-> [QUOTE ("(f:word64->word32) (bp + 0x4w * w2w w" ^ int_to_string j ^ "+4w)")]] 460 val post_tm = cdr (concl (Q.INST s (REFL post_tm))) 461 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 462 (w0,w1,w2,w3,w4,w5,df,f,^REST)`` 463 val tm2 = cdr (concl (Q.INST s (Q.INST sw (REFL tm)))) 464 val imp = generate_copy i j 465 val imp = DISCH_ALL (MATCH_MP (generate_cdr i) (UNDISCH imp)) 466 val th = RW [cdr_blast] th 467 val result = prove_spec th imp def pre_tm post_tm 468 in save_lisp_thm("X64_LISP_CDR" ^ int_to_string i ^ int_to_string j,result) end 469 470val _ = map X64_LISP_CDR all_reg_pairs; 471 472 473(* isDot *) 474 475fun X64_LISP_ISDOT i = let 476 val _ = print "z" 477 val s = "test " ^ (x64_reg i) ^ ", 1" 478 val s = x64_encode s 479 val (spec,_,sts,_) = x64_tools 480 val ((th,_,_),_) = spec s 481 val th = HIDE_PRE_STATUS_RULE sts th 482 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 483 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 484 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 485 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 486 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 487 val def = zLISP_def 488 val imp = DISCH_ALL (MATCH_MP lisp_inv_type (UNDISCH (swap_thm i))) 489 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 490 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isDot x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 491 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 492 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 493 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 494 val result = prove_spec th imp def pre_tm post_tm 495 in save_lisp_thm("X64_LISP_ISDOT" ^ int_to_string i,result) end; 496 497val _ = map X64_LISP_ISDOT all_regs; 498 499 500(* isSym *) 501 502fun generate_sym i = let 503 val th = CONJUNCT2 (UNDISCH lisp_inv_isSym) 504 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 505 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 506 val th1 = CONJUNCT1 (UNDISCH lisp_inv_isSym) 507 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 508 val th2 = UNDISCH (RW [AND_IMP_INTRO] th) 509 val th3 = UNDISCH (RW [AND_IMP_INTRO] th1) 510 in RW [GSYM AND_IMP_INTRO] (DISCH_ALL (CONJ th2 th3)) end; 511 512fun X64_LISP_ISSYM i = let 513 val _ = print "z" 514 val s = "mov r2, " ^ (x64_reg i) 515 val s = x64_encode s 516 val (spec,_,sts,_) = x64_tools 517 val ((th1,_,_),_) = spec (x64_encode ("mov r2, " ^ (x64_reg i))) 518 val ((th2,_,_),_) = spec (x64_encode ("and r2, r0")) 519 val ((th3,_,_),_) = spec (x64_encode ("cmp r0, r2")) 520 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 521 val th = HIDE_PRE_STATUS_RULE sts th 522 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 523 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 524 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 525 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 526 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 527 val th = GSYM th 528 val def = zLISP_def 529 val imp = generate_sym i 530 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 531 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isSym x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 532 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 533 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 534 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 535 val result = prove_spec th imp def pre_tm post_tm 536 in save_lisp_thm("X64_LISP_ISSYM" ^ int_to_string i,result) end; 537 538val _ = map X64_LISP_ISSYM all_regs; 539 540 541(* isVal *) 542 543fun generate_val i = let 544 val th = CONJUNCT2 (UNDISCH lisp_inv_isVal) 545 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 546 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 547 val th1 = CONJUNCT1 (UNDISCH lisp_inv_isVal) 548 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 549 val th2 = UNDISCH (RW [AND_IMP_INTRO] th) 550 val th3 = UNDISCH (RW [AND_IMP_INTRO] th1) 551 in RW [GSYM AND_IMP_INTRO] (DISCH_ALL (CONJ th2 th3)) end; 552 553fun X64_LISP_ISVAL i = let 554 val _ = print "z" 555 val s = "mov r2, " ^ (x64_reg i) 556 val s = x64_encode s 557 val (spec,_,sts,_) = x64_tools 558 val ((th1,_,_),_) = spec (x64_encode ("mov r2, " ^ (x64_reg i))) 559 val ((th2,_,_),_) = spec (x64_encode ("and r2, r0")) 560 val ((th3,_,_),_) = spec (x64_encode ("cmp r1, r2")) 561 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 562 val th = HIDE_PRE_STATUS_RULE sts th 563 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 564 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 565 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 566 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 567 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 568 val th = GSYM th 569 val def = zLISP_def 570 val imp = generate_val i 571 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 572 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isVal x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 573 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 574 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 575 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 576 val result = prove_spec th imp def pre_tm post_tm 577 in save_lisp_thm("X64_LISP_ISVAL" ^ int_to_string i,result) end; 578 579val _ = map X64_LISP_ISVAL all_regs; 580 581 582(* eq zero *) 583 584fun X64_LISP_EQZERO i = let 585 val _ = print "z" 586 val s = "cmp r1, " ^ (x64_reg i) 587 val s = x64_encode s 588 val (spec,_,sts,_) = x64_tools 589 val ((th,_,_),_) = spec s 590 val th = HIDE_PRE_STATUS_RULE sts th 591 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 592 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 593 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 594 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 595 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 596 val def = zLISP_def 597 val imp = UNDISCH lisp_inv_eq_zero 598 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) 599 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 600 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = Val 0)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 601 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 602 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 603 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 604 val result = prove_spec th imp def pre_tm post_tm 605 in save_lisp_thm("X64_LISP_EQZERO" ^ int_to_string i,result) end; 606 607val _ = map X64_LISP_EQZERO all_regs; 608 609 610(* eq val *) 611 612val lisp_inv_eq_val = prove( 613 ``!n. n < 1073741824 /\ ^LISP ==> ((w2w w0 = n2w (4 * n + 1):word64) = (x0 = Val n))``, 614 REPEAT STRIP_TAC \\ IMP_RES_TAC lisp_inv_swap1 615 \\ IMP_RES_TAC lisp_inv_Val_n2w 616 \\ IMP_RES_TAC (RW [isDot_def] (Q.INST [`x0`|->`Val n`] lisp_inv_eq)) 617 \\ CONV_TAC (BINOP_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) 618 \\ Cases_on `w0` \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [n2w_11,w2w_def,w2n_n2w] 619 \\ `(4 * n + 1) < 4294967296` by DECIDE_TAC 620 \\ `(4 * n + 1) < 18446744073709551616` by DECIDE_TAC 621 \\ `n' < 18446744073709551616` by DECIDE_TAC 622 \\ FULL_SIMP_TAC std_ss []); 623 624fun X64_LISP_EQ_VAL n i = let 625 val _ = print "z" 626 val s = "cmp " ^ (x64_reg i) ^ ", " ^ int_to_string (4 * n + 1) 627 val s = x64_encode s 628 val (spec,_,sts,_) = x64_tools 629 val ((th,_,_),_) = spec s 630 val th = HIDE_PRE_STATUS_RULE sts th 631 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 632 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 633 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 634 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 635 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 636 val def = zLISP_def 637 val imp = UNDISCH (SIMP_RULE std_ss [] (SPEC (numSyntax.term_of_int n) lisp_inv_eq_val)) 638 val imp = DISCH_ALL (MATCH_MP (DISCH_ALL imp) (UNDISCH (swap_thm i))) 639 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 640 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = Val n)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 641 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")],``n:num``|->numSyntax.term_of_int n] post_tm 642 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 643 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 644 val result = prove_spec th imp def pre_tm post_tm 645 in save_lisp_thm("X64_LISP_EQ_VAL_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end; 646 647val _ = map (X64_LISP_EQ_VAL 1) all_regs; 648val _ = map (X64_LISP_EQ_VAL 2) all_regs; 649val _ = map (X64_LISP_EQ_VAL 3) all_regs; 650val _ = map (fn n => X64_LISP_EQ_VAL n 0) [3,4,5,6,7,8,9,10,11,12,13,14,15]; 651 652(* eq *) 653 654fun X64_LISP_EQ (i,j) = if j <= i then (TRUTH,TRUTH) else let 655 val _ = print "z" 656 val s = "cmp " ^ (x64_reg i) ^ ", " ^ (x64_reg j) 657 val s = x64_encode s 658 val (spec,_,sts,_) = x64_tools 659 val ((th,_,_),_) = spec s 660 val th = HIDE_PRE_STATUS_RULE sts th 661 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 662 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 663 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 664 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 665 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 666 val def = zLISP_def 667 val lemma = CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM markerTheory.Abbrev_def])) lisp_inv_eq 668 val lemma = RW [GSYM AND_IMP_INTRO] (RW1 [CONJ_COMM] (RW [AND_IMP_INTRO] lemma)) 669 val lemma = if j = 1 then lemma else DISCH_ALL (MATCH_MP lemma (UNDISCH (generate_swap 1 j))) 670 val lemma = if i = 0 then lemma else DISCH_ALL (MATCH_MP lemma (UNDISCH (generate_swap 0 i))) 671 val imp = lemma 672 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 673 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = y:SExp)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 674 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]] post_tm 675 val post_tm = subst [``y:SExp``|->Term [QUOTE ("x" ^ int_to_string j ^ ": SExp")]] post_tm 676 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 677 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 678 val result = prove_spec th imp def pre_tm post_tm 679 val result2 = RW1 [EQ_SYM_EQ,DISJ_COMM] result 680 val _ = save_lisp_thm("X64_LISP_EQ" ^ int_to_string i ^ int_to_string j,result) 681 val _ = save_lisp_thm("X64_LISP_EQ" ^ int_to_string j ^ int_to_string i,result2) 682 in (result,result2) end; 683 684val _ = map X64_LISP_EQ all_reg_pairs; 685 686 687(* less *) 688 689val X64_LISP_LESS = let 690 val _ = print "z" 691 val s = "cmp " ^ (x64_reg 0) ^ ", " ^ (x64_reg 1) 692 val s = x64_encode s 693 val (spec,_,sts,_) = x64_tools 694 val ((th,_,_),_) = spec s 695 val th = HIDE_PRE_STATUS_RULE sts th 696 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 697 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 698 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 699 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 700 val th = HIDE_POST_RULE ``zS1 Z_ZF`` th 701 val def = zLISP_def 702 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 703 val imp = RW1 [lemma] lisp_inv_less 704 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 705 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_CF (SOME (getVal x0 < getVal x1)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_ZF`` 706 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 707 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 708 val result = prove_spec th imp def pre_tm post_tm 709 in save_lisp_thm("X64_LISP_LESS",result) end; 710 711val X64_LISP_EVEN = let 712 val _ = print "z" 713 val s = "test r8, 4" 714 val s = x64_encode s 715 val (spec,_,sts,_) = x64_tools 716 val ((th,_,_),_) = spec s 717 val th = HIDE_PRE_STATUS_RULE sts th 718 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 719 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 720 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 721 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 722 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 723 val th = Q.INST [`r8`|->`w2w (a:word32)`,`rip`|->`p`] th 724 val def = zLISP_def 725 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 726 val imp = RW1 [lemma] lisp_inv_even 727 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 728 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME (EVEN (getVal x0))) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 729 val result = prove_spec th imp def pre_tm post_tm 730 in save_lisp_thm("X64_LISP_EVEN",result) end; 731 732 733(* assign 0 and 1 to all regs *) 734 735val SIGN_EXTEND_MOD = store_thm("SIGN_EXTEND_MOD", 736 ``SIGN_EXTEND 32 64 (w2n imm32) MOD 4294967296 = w2n (imm32:word32)``, 737 SIMP_TAC std_ss [SIGN_EXTEND_def,LET_DEF] \\ SRW_TAC [] [] 738 \\ (SIMP_RULE (std_ss++SIZES_ss) [] (INST_TYPE [``:'a``|->``:32``] w2n_lt) 739 |> Q.SPEC `imm32` |> ASSUME_TAC) \\ FULL_SIMP_TAC std_ss [] 740 \\ REWRITE_TAC [GSYM (EVAL ``4294967295 * 4294967296``)] 741 \\ IMP_RES_TAC MOD_MULT \\ FULL_SIMP_TAC std_ss []); 742 743val imm32_lemma = prove( 744 ``n < 2**30 ==> 745 (SIGN_EXTEND 32 64 (w2n (n2w (4 * n + 1):word32)) MOD 4294967296 = 4 * n + 1)``, 746 SIMP_TAC std_ss [SIGN_EXTEND_MOD] 747 \\ SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] \\ DECIDE_TAC); 748 749val bound_lemma = prove( 750 ``n < 1073741824 ==> 4 * n + 1 < 4294967296``, 751 DECIDE_TAC); 752 753val X64_LISP_ASSIGN_ANY_VAL = save_thm("X64_LISP_ASSIGN_ANY_VAL",let 754 val (spec,_,sts,_) = x64_tools 755 val ((th,_,_),_) = spec "41B8" 756 val def = zLISP_def 757 val th = Q.INST [`imm32`|->`n2w (4 * n + 1)`,`rip`|->`p`] th 758 |> DISCH ``n < 2**30`` |> SIMP_RULE bool_ss [imm32_lemma] 759 |> RW [GSYM SPEC_MOVE_COND] |> SIMP_RULE std_ss [] 760 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 761 val post_tm = set_pc th ``zLISP ^STAT (Val n,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 762 val imp = lisp_inv_Val_n2w |> SPEC_ALL |> RW1 [GSYM AND_IMP_INTRO] 763 |> UNDISCH_ALL 764 |> (fn th => CONJ th (UNDISCH bound_lemma)) 765 |> DISCH_ALL 766 val result = prove_spec th imp def pre_tm post_tm 767 in result end); 768 769fun generate_assign_val n i = let 770 val th1 = SIMP_RULE std_ss [] (SPEC n lisp_inv_Val_n2w); 771 val th5 = UNDISCH th1 772 val th5 = DISCH_ALL (MATCH_MP (swap_thm i) th5) 773 val th5 = DISCH_ALL (MATCH_MP th5 (UNDISCH (swap_thm i))) 774 in th5 end; 775 776fun X64_LISP_ASSIGN_VAL n i = let 777 val _ = print "z" 778 val s = "mov " ^ (x64_reg i) ^ "d, " ^ int_to_string (4 * n + 1) 779 val s = x64_encode s 780 val (spec,_,sts,_) = x64_tools 781 val ((th,_,_),_) = spec s 782 val def = zLISP_def 783 val n_tm = numSyntax.term_of_int n 784 val imp = generate_assign_val n_tm i 785 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 786 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 787 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->mk_comb(``Val ``,n_tm)] post_tm 788 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 789 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 790 val result = prove_spec th imp def pre_tm post_tm 791 in save_lisp_thm("X64_LISP_ASSIGN_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end; 792 793val _ = map (X64_LISP_ASSIGN_VAL 0) all_regs; 794val _ = map (X64_LISP_ASSIGN_VAL 1) all_regs; 795val _ = map (fn n => X64_LISP_ASSIGN_VAL n 0) [2,3,4,5,6,7,8,9,10,11,12,13,14,15]; 796val _ = map (fn n => X64_LISP_ASSIGN_VAL n 1) [2,3,4,5,6,7,8,9,10,11,12,13,14,15]; 797 798 799(* assign/test sym *) 800 801val lisp_inv_sym_assigns = map (DISCH_ALL o CONJUNCT1 o UNDISCH) (CONJUNCTS lisp_inv_Sym); 802val lisp_inv_sym_tests = map (DISCH_ALL o CONJUNCT2 o UNDISCH) (CONJUNCTS lisp_inv_Sym); 803 804fun generate_assign_sym n i = let 805 val th = UNDISCH (el (n+1) lisp_inv_sym_assigns) 806 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 807 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 808 in th end; 809 810fun generate_test_sym n i = let 811 val th = el (n+1) lisp_inv_sym_tests 812 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 813 in th end; 814 815fun X64_LISP_ASSIGN_SYM n i = let 816 val _ = print "z" 817 val imp = generate_assign_sym n i 818 val k = cdr (find_term wordsSyntax.is_n2w (concl imp)) 819 val k = numSyntax.int_of_term k 820 val s = "mov " ^ (x64_reg i) ^ "d, " ^ (int_to_string k) 821 val s = x64_encode s 822 val (spec,_,sts,_) = x64_tools 823 val ((th,_,_),_) = spec s 824 val def = zLISP_def 825 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 826 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 827 val sym = find_term (can (match_term ``Sym s``)) (concl imp) 828 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->sym] post_tm 829 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 830 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 831 val result = prove_spec th imp def pre_tm post_tm 832 in save_lisp_thm("X64_LISP_ASSIGN_SYM_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end; 833 834fun X64_LISP_TEST_SYM n i = let 835 val _ = print "z" 836 val imp = generate_test_sym n i 837 val k = cdr (find_term wordsSyntax.is_n2w (concl imp)) 838 val k = numSyntax.int_of_term k 839 val s = "cmp " ^ (x64_reg i) ^ ", " ^ (int_to_string k) 840 val s = x64_encode s 841 val (spec,_,sts,_) = x64_tools 842 val ((th,_,_),_) = spec s 843 val th = HIDE_PRE_STATUS_RULE sts th 844 val th = HIDE_POST_RULE ``zS1 Z_PF`` th 845 val th = HIDE_POST_RULE ``zS1 Z_SF`` th 846 val th = HIDE_POST_RULE ``zS1 Z_AF`` th 847 val th = HIDE_POST_RULE ``zS1 Z_OF`` th 848 val th = HIDE_POST_RULE ``zS1 Z_CF`` th 849 val def = zLISP_def 850 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 851 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = res:SExp)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF`` 852 val sym = find_term (can (match_term ``Sym s``)) (concl imp) 853 val post_tm = subst [``x:SExp``|->Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")],``res:SExp``|->sym] post_tm 854 val tm = find_term (can (match_term ``zPC (eip + n2w n)``)) (concl th) 855 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 856 val result = prove_spec th imp def pre_tm post_tm 857 in save_lisp_thm("X64_LISP_TEST_SYM_" ^ int_to_string n ^ "_" ^ int_to_string i,result) end; 858 859fun X64_LISP_SYM n i = (X64_LISP_ASSIGN_SYM n i, X64_LISP_TEST_SYM n i); 860 861fun ilist i [] = [] | ilist i (x::xs) = i::ilist (i+1) xs; 862val all_syms = ilist 0 lisp_inv_sym_tests; 863 864val _ = map (X64_LISP_SYM 0) all_regs; (* NIL *) 865val _ = map (X64_LISP_SYM 1) all_regs; (* T *) 866val _ = map (X64_LISP_SYM 2) all_regs; (* QUOTE *) 867val _ = map (fn x => X64_LISP_SYM x 0) all_syms; 868 869 870(* error *) 871 872val X64_LISP_ERROR = save_thm("X64_LISP_ERROR",let 873 val s = "jmp [r7-200]" 874 val s = x64_encode s 875 val (spec,_,sts,_) = x64_tools 876 val ((th,_,_),_) = spec s 877 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 878 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC ex`` 879 val imp = lisp_inv_error 880 val def = zLISP_def 881 val res = prove_spec th imp def pre_tm post_tm 882 val res = SPEC_FRAME_RULE res ``~zS`` 883 val post_tm = ``zLISP_FAIL (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu)`` 884 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN res) 885 val goal = (cdr o car o concl) th 886 val lemma = prove(goal, 887 SIMP_TAC std_ss [zLISP_FAIL_def,SEP_EXISTS_THM,SEP_IMP_def] 888 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `ddd` 889 \\ Q.EXISTS_TAC `(x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)` 890 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES]) 891 val th = MP th lemma 892 in th end); 893 894val X64_LISP_SET_OK_F = save_lisp_thm("X64_LISP_SET_OK_F",let 895 val th = X64_LISP_ERROR 896 val (th,goal) = SPEC_WEAKEN_RULE th 897 ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) 898 (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,F) * zPC (rip+7w) * ~zS \/ 899 zLISP_FAIL (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu)`` 900 val lemma = prove(goal,SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]) 901 val th = MP th lemma 902 in th end); 903 904 905(* is_quote *) 906 907val X64_LISP_IS_QUOTE = save_lisp_thm("X64_LISP_IS_QUOTE",let 908 val th = mc_is_quote_full_spec 909 val imp = mc_is_quote_full_thm 910 val def = zLISP_def 911 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 912 val post_tm = set_pc th ``zLISP ^STAT (LISP_TEST (isQuote x0),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 913 val res = prove_spec th imp def pre_tm post_tm 914 in res end); 915 916 917(* gc *) 918 919val X64_LISP_GC = save_lisp_thm("X64_LISP_GC",let 920 val th = lisp_consTheory.mc_full_thm 921 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_gc 922 val def = zLISP_def 923 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 924 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 925 val res = prove_spec th imp def pre_tm post_tm 926 in res end); 927 928 929(* calls to code pointers *) 930 931val align_blast = blastLib.BBLAST_PROVE 932 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 933 934val imp4 = prove( 935 ``^LISP ==> (sp - 0x6Cw && 0x3w = 0x0w) /\ (sp - 0x70w && 0x3w = 0x0w) /\ 936 (sp - 0x74w && 0x3w = 0x0w) /\ (sp - 0x78w && 0x3w = 0x0w) /\ 937 (sp - 0x7Cw && 0x3w = 0x0w) /\ (sp - 0x80w && 0x3w = 0x0w) /\ 938 (sp - 0x84w && 0x3w = 0x0w) /\ (sp - 0x88w && 0x3w = 0x0w) /\ 939 (sp - 0x8Cw && 0x3w = 0x0w) /\ (sp - 0x90w && 0x3w = 0x0w) /\ 940 (sp - 0x98w && 0x3w = 0x0w) /\ (sp - 0x94w && 0x3w = 0x0w) /\ 941 (sp - 0x9Cw && 0x3w = 0x0w) /\ (sp - 0xA0w && 0x3w = 0x0w) /\ 942 (sp - 0xC8w && 0x3w = 0x0w) /\ (sp - 0xA4w && 0x3w = 0x0w) /\ 943 (sp - 0xC4w && 0x3w = 0x0w) /\ (sp - 0xA8w && 0x3w = 0x0w) /\ 944 (sp - 0xC0w && 0x3w = 0x0w) /\ (sp - 0xACw && 0x3w = 0x0w) /\ 945 (sp - 0xBCw && 0x3w = 0x0w) /\ (sp - 0xB0w && 0x3w = 0x0w) /\ 946 (sp - 0xB8w && 0x3w = 0x0w) /\ (sp - 0xB4w && 0x3w = 0x0w)``, 947 SIMP_TAC std_ss [lisp_inv_def] \\ STRIP_TAC 948 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3]) |> UNDISCH 949 950fun X64_LISP_CALL_EL i = save_thm("X64_LISP_CALL_EL" ^ (int_to_string i),let 951 val addr = "mov r2,[r7-" ^ int_to_string (192 - 8 * i) ^ "]" 952 val ((th,_,_),_) = x64_spec (x64_encodeLib.x64_encode addr) 953 val th = Q.INST [`rip`|->`p`] th 954 val th = RW [INSERT_SUBSET,EMPTY_SUBSET] th 955 val tm = subst [``i:num``|->numSyntax.term_of_int i] ``(EL i cs):word64`` 956 val imp0 = UNDISCH (INST [``temp:word64``|->tm] lisp_inv_ignore_tw2) 957 val imp1 = el (3*i+10+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 958 val imp2 = el (3*i+11+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 959 val imp3 = el (3*i+12+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 960 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) 961 val def = zLISP_ALT_def 962 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 963 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 964 val res = prove_spec th imp def pre_tm post_tm 965 val res = SPEC_COMPOSE_RULE [res,Q.INST [`r2`|->`^tm`] X64_LISP_CALL_R2] 966 val res = RW [GSYM zLISP_raw] res 967 in res end); 968 969val X64_LISP_CALL_EL3 = X64_LISP_CALL_EL 3; 970val X64_LISP_CALL_EL5 = X64_LISP_CALL_EL 5; 971val X64_LISP_CALL_EL6 = X64_LISP_CALL_EL 6; 972val X64_LISP_CALL_EL7 = X64_LISP_CALL_EL 7; 973val X64_LISP_CALL_EL8 = X64_LISP_CALL_EL 8; 974val X64_LISP_CALL_EL9 = X64_LISP_CALL_EL 9; 975 976 977(* store r2 into cs *) 978 979val write_cs_blast = blastLib.BBLAST_PROVE 980 ``(w2w ((w2w (w >>> 32)):word32) << 32 !! w2w ((w2w (w:word64)):word32) = w) /\ 981 ((63 >< 32) w = (w2w (w >>> 32)):word32) /\ ((31 >< 0) w = (w2w w):word32)``; 982 983fun X64_LISP_WRITE_CS i = save_thm("X64_LISP_WRITE_CS" ^ (int_to_string i),let 984 val addr = "mov [r7-" ^ int_to_string (192 - 8 * i) ^ "],r2" 985 val ((th,_,_),_) = x64_spec (x64_encodeLib.x64_encode addr) 986 val th = Q.INST [`rip`|->`p`] th 987 val th = RW [INSERT_SUBSET,EMPTY_SUBSET] th 988 val tm = subst [``i:num``|->numSyntax.term_of_int i] ``(UPDATE_NTH i r2 cs):word64 list`` 989 val imp1 = if i = 3 then last (CONJUNCTS (UNDISCH (Q.INST [`w`|->`tw2`] lisp_inv_cs_write))) 990 else el (10-i) (CONJUNCTS (UNDISCH (Q.INST [`w`|->`tw2`] lisp_inv_cs_write))) 991 val imp2 = el (3*i+11+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 992 val imp3 = el (3*i+12+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 993 val imp = DISCH_ALL (LIST_CONJ [imp1,imp2,imp3,imp4]) 994 val NEW_STAT = subst [mk_var("cs",``:word64 list``) |-> tm] STAT 995 val def = zLISP_ALT_def 996 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 997 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^NEW_STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 998 val th = RW [write_cs_blast] th 999 val finder = find_term (fn tm => is_comb tm andalso combinSyntax.is_update (car tm)) 1000 val tm1 = finder (concl (Q.INST [`r7`|->`sp`,`r2`|->`tw2`] th)) 1001 val tm2 = finder (concl imp) 1002 val goal = mk_eq(tm1,tm2) 1003 val lemma = prove(goal,MATCH_MP_TAC UPDATE_COMMUTES \\ blastLib.BBLAST_TAC) 1004 val th = RW1 [lemma] th 1005 val res = prove_spec th imp def pre_tm post_tm 1006 val res = SPEC_COMPOSE_RULE [X64_LISP_POP_R2,(Q.INST [`r2`|->`q`] res)] 1007 val res = RW [GSYM zLISP_raw] res 1008 in res end); 1009 1010val X64_LISP_WRITE_CS3 = X64_LISP_WRITE_CS 3; 1011val X64_LISP_WRITE_CS5 = X64_LISP_WRITE_CS 5; 1012val X64_LISP_WRITE_CS6 = X64_LISP_WRITE_CS 6; 1013val X64_LISP_WRITE_CS7 = X64_LISP_WRITE_CS 7; 1014val X64_LISP_WRITE_CS8 = X64_LISP_WRITE_CS 8; 1015val X64_LISP_WRITE_CS9 = X64_LISP_WRITE_CS 9; 1016 1017 1018(* equal *) 1019 1020val X64_LISP_EQUAL = save_lisp_thm("X64_LISP_EQUAL",let 1021 val th = mc_full_equal_spec 1022 val imp = mc_full_equal_thm 1023 val def = zLISP_def 1024 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1025 val post_tm = set_pc th ``zLISP ^STAT (LISP_TEST (x0 = x1:SExp),Sym "NIL",x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1026 val res = prove_spec th imp def pre_tm post_tm 1027 val res = Q.INST [`qs`|->`q::qs`] res 1028 val res = SPEC_COMPOSE_RULE [res,X64_LISP_RET] 1029 val (_,_,c,_) = dest_spec (concl res) 1030 val name = mk_var("abbrev_code_for_equal",mk_type("fun",[``:word64``,type_of c])) 1031 val def = Define [ANTIQUOTE (mk_eq(mk_comb(name,``p:word64``),c))] 1032 val res = RW [GSYM def] res 1033 val res = SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_CALL_EL6",res] 1034 in res end); 1035 1036 1037(* add, add1 *) 1038 1039val select_twice = blastLib.BBLAST_PROVE 1040 ``((31 -- 0) ((31 -- 0) w) = (31 -- 0) w:word64) /\ 1041 ((31 -- 0) (w2w a - 0x1w:word64) = w2w ((a:word32) - 1w)) /\ 1042 ((31 -- 0) (w2w a) = (w2w a):word64) /\ 1043 ((31 -- 0) (w2w a + w2w b) = (w2w (a + b)):word64) /\ 1044 ((31 -- 0) (w2w a + 4w) = (w2w (a + 4w)):word64)``; 1045 1046val SEP_IMP_LEMMA = prove( 1047 ``SEP_IMP p (p \/ q) /\ SEP_IMP p (q \/ p)``, 1048 SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]); 1049 1050val SPEC_MERGE_LEMMA = prove( 1051 ``SPEC m (p * cond b) c1 q1 ==> 1052 SPEC m (p * cond ~b) c2 q2 ==> 1053 SPEC m (p) (c1 UNION c2) (q1 \/ q2)``, 1054 Cases_on `b` \\ SIMP_TAC std_ss [SEP_CLAUSES,SPEC_FALSE_PRE] 1055 \\ METIS_TAC [SPEC_ADD_CODE,SEP_IMP_LEMMA,SPEC_WEAKEN,UNION_COMM]); 1056 1057val X64_LISP_ADD = save_lisp_thm("X64_LISP_ADD",let 1058 val add_code = 1059 (codegenLib.assemble "x64" ` 1060 dec r8d 1061 add r8d,r9d 1062 jnb L 1063 mov r8,r1 1064 mov r2d, 2 1065 jmp [r7-200] 1066 L: `) 1067 val (spec,_,sts,_) = x64_tools 1068 val ((th1,_,_),_) = spec (el 1 add_code) 1069 val ((th2,_,_),_) = spec (el 2 add_code) 1070 val ((th3,_,_),th3a) = spec (el 3 add_code) 1071 val ((th4,_,_),_) = spec (el 4 add_code) 1072 val ((th5,_,_),_) = spec (el 5 add_code) 1073 fun the (SOME x) = x | the _ = fail(); 1074 val (th3b,_,_) = the th3a 1075 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 1076 val th = HIDE_STATUS_RULE true sts th 1077 val th = Q.INST [`r8`|->`w2w (a:word32)`] th 1078 val th = Q.INST [`r9`|->`w2w (b:word32)`] th 1079 val th = RW [select_twice] th 1080 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,GSYM NOT_LESS,precond_def] th 1081 val imp = lisp_inv_add 1082 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1083 val post_tm = set_pc th ``zLISP ^STAT (LISP_ADD x0 x1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1084 val def = zLISP_def 1085 val res1 = prove_spec th imp def pre_tm post_tm 1086 val th = SPEC_COMPOSE_RULE [th1,th2,th3b,th4,th5] 1087 val th = HIDE_STATUS_RULE true sts th 1088 val th = Q.INST [`r8`|->`w2w (a:word32)`] th 1089 val th = Q.INST [`r9`|->`w2w (b:word32)`] th 1090 val th = RW [select_twice] th 1091 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,precond_def] th 1092 val imp = lisp_inv_add_nop 1093 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1094 val post_tm = set_pc th ``zLISP ^STAT (Val 0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1095 val res = prove_spec th imp def pre_tm post_tm 1096 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 1097 val lemma = prove(``cond b * cond c = cond (b /\ c)``,SIMP_TAC std_ss [SEP_CLAUSES]) 1098 val res1 = RW [GSYM lemma, STAR_ASSOC] res1 1099 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 1100 val set_lemma = prove( 1101 ``{x1;x2;x3} UNION {x1;x2;x3;x4;x5;x6} = {x1;x2;x3;x4;x5;x6}``, 1102 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 1103 val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2 1104 val res = RW [STAR_ASSOC] (RW [set_lemma,lemma,GSYM STAR_ASSOC] res) 1105 in res end); 1106 1107fun generate_add1 i = let 1108 val th = CONJUNCT1 (UNDISCH (UNDISCH lisp_inv_add1)) 1109 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 1110 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 1111 val th1 = CONJUNCT2 (UNDISCH (UNDISCH lisp_inv_add1)) 1112 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 1113 val th2 = UNDISCH th 1114 val th3 = UNDISCH th1 1115 val tm = fst (dest_imp (concl th2)) 1116 in DISCH_ALL (DISCH tm (CONJ (UNDISCH th2) (UNDISCH th3))) end; 1117 1118fun generate_add1_nop i = let 1119 val th = CONJUNCT1 (UNDISCH (UNDISCH lisp_inv_add1_nop)) 1120 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 1121 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 1122 val th1 = CONJUNCT2 (UNDISCH (UNDISCH lisp_inv_add1_nop)) 1123 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 1124 val th2 = UNDISCH th 1125 val th3 = UNDISCH th1 1126 val tm = fst (dest_imp (concl th2)) 1127 in DISCH_ALL (DISCH tm (CONJ (UNDISCH th2) (UNDISCH th3))) end; 1128 1129fun X64_LISP_ADD1 i = let 1130 val add_code = 1131 (codegenLib.assemble "x64" ` 1132 add r8d,4 1133 jnb L 1134 mov r8,r1 1135 mov r2d, 2 1136 jmp [r7-200] 1137 L: `) 1138 val ((th1,_,_),_) = spec (x64_encode ("add " ^ (x64_reg i) ^ "d, 4")) 1139 val ((th2,_,_),th2a) = spec (el 2 add_code) 1140 val ((th3,_,_),_) = spec (x64_encode ("mov " ^ (x64_reg i) ^ ", r1")) 1141 val ((th4,_,_),_) = spec (el 4 add_code) 1142 fun the (SOME x) = x | the _ = fail(); 1143 val (th2b,_,_) = the th2a 1144 val th = SPEC_COMPOSE_RULE [th1,th2] 1145 val th = HIDE_STATUS_RULE true sts th 1146 val th = Q.INST [[QUOTE (x64_reg i ^ ":word64")]|->`w2w (a:word32)`] th 1147 val th = RW [select_twice] th 1148 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,GSYM NOT_LESS,precond_def] th 1149 val imp = generate_add1 i 1150 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1151 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1152 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|-> 1153 Term [QUOTE ("LISP_ADD (x" ^ int_to_string i ^ ": SExp) (Val 1)")]] post_tm 1154 val def = zLISP_def 1155 val res1 = prove_spec th imp def pre_tm post_tm 1156 val th = SPEC_COMPOSE_RULE [th1,th2b,th3,th4] 1157 val th = HIDE_STATUS_RULE true sts th 1158 val th = Q.INST [[QUOTE (x64_reg i ^ ":word64")]|->`w2w (a:word32)`] th 1159 val th = RW [select_twice] th 1160 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,precond_def] th 1161 val imp = generate_add1_nop i 1162 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1163 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1164 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->``Val 0``] post_tm 1165 val res = prove_spec th imp def pre_tm post_tm 1166 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 1167 val lemma = prove(``cond b * cond c = cond (b /\ c)``,SIMP_TAC std_ss [SEP_CLAUSES]) 1168 val res1 = RW [GSYM lemma, STAR_ASSOC] res1 1169 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 1170 val set_lemma = prove( 1171 ``{x1;x2} UNION {x1;x2;x4;x5;x6} = {x1;x2;x4;x5;x6}``, 1172 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 1173 val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA res1) res2 1174 val res = RW [STAR_ASSOC] (RW [set_lemma,lemma,GSYM STAR_ASSOC] res) 1175 in save_lisp_thm("X64_LISP_ADD1_" ^ int_to_string i,res) end; 1176 1177val _ = map X64_LISP_ADD1 all_regs; 1178 1179 1180(* sub, sub1 *) 1181 1182val X64_LISP_SUB = save_lisp_thm("X64_LISP_SUB",let 1183 val (thm,temp_func_def) = decompile_io_strings x64_tools "temp_func" 1184 (SOME (``(r1:word64,r8:word64,r9:word64)``,``(r1:word64,r8:word64,r9:word64)``)) 1185 (codegenLib.assemble "x64" ` 1186 inc r8d 1187 sub r8d,r9d 1188 cmovb r8d,r1d `) 1189 val PUSH_IF = METIS_PROVE [] 1190 ``((if b then (x,y,z) else (x,y2,z)) = (x,(if b then y else y2), z))`` 1191 val temp_def = SIMP_RULE std_ss [LET_DEF,PUSH_IF] temp_func_def 1192 val sub_blast = prove( 1193 ``((31 -- 0) ((31 -- 0) (w2w a + 0x1w) - w2w b) = (w2w ((a+1w)-b:word32)):word64) /\ 1194 ((31 -- 0) ((31 -- 0) (w2w a + 0x1w)) = (w2w (a + 1w)):word64) /\ 1195 (w2w a <+ (w2w b):word64 = a <+ b)``, 1196 blastLib.BBLAST_TAC) 1197 val sub_blast2 = prove( 1198 ``((31 -- 0) a = w2w ((w2w (a:word64)):word32)) /\ 1199 ((if b then w2w x else w2w y) = w2w (if b then x else y))``, 1200 STRIP_TAC THEN1 blastLib.BBLAST_TAC \\ METIS_TAC []) 1201 val th = SIMP_RULE std_ss [temp_def,LET_DEF] thm 1202 |> Q.INST [`r8`|->`w2w (a:word32)`,`r9`|->`w2w (b:word32)`] 1203 |> RW [car_blast,sub_blast] |> RW [sub_blast2] 1204 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1205 val imp = RW1 [lemma] lisp_inv_sub 1206 val def = zLISP_def 1207 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1208 val post_tm = set_pc th ``zLISP ^STAT (LISP_SUB x0 x1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1209 val res = prove_spec th imp def pre_tm post_tm 1210 in res end); 1211 1212fun generate_sub1 i = let 1213 val th = UNDISCH (UNDISCH lisp_inv_sub1) 1214 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 1215 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 1216 in th end; 1217 1218fun X64_LISP_SUB1 i = let 1219 val _ = print "z" 1220 val s = "sub " ^ (x64_reg i) ^ "d, 4" 1221 val s = x64_encode s 1222 val (spec,_,sts,_) = x64_tools 1223 val ((th,_,_),_) = spec s 1224 val th = HIDE_STATUS_RULE true sts th 1225 val def = zLISP_def 1226 val imp = generate_sub1 i 1227 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1228 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1229 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->Term [QUOTE ("LISP_SUB (x" ^ int_to_string i ^ ": SExp) (Val 1)")]] post_tm 1230 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1231 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1232 val result = prove_spec th imp def pre_tm post_tm 1233 in save_lisp_thm("X64_LISP_SUB1_" ^ int_to_string i,result) end; 1234 1235val _ = map X64_LISP_SUB1 all_regs; 1236 1237val X64_LISP_DIV2 = let 1238 val _ = print "z" 1239 val (spec,_,sts,_) = x64_tools 1240 val ((th1,_,_),_) = spec (x64_encode "shr r8, 3") 1241 val ((th2,_,_),_) = spec (x64_encode "shl r8, 2") 1242 val ((th3,_,_),_) = spec (x64_encode "inc r8") 1243 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 1244 val th = HIDE_STATUS_RULE true sts th 1245 val th = Q.INST [`r8:word64`|->`w2w (a:word32)`] th 1246 val th = Q.INST [`a`|->`r8`,`rip`|->`p`] th 1247 val lemma = blastLib.BBLAST_PROVE 1248 ``w2w a >>> 3 << 2 + 0x1w = (w2w:word32->word64) (a >>> 3 << 2 + 0x1w)`` 1249 val th = RW [lemma] th 1250 val def = zLISP_def 1251 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1252 val imp = RW1 [lemma] lisp_inv_div2 1253 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1254 val post_tm = set_pc th ``zLISP ^STAT (Val (getVal x0 DIV 2),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1255 val result = prove_spec th imp def pre_tm post_tm 1256 in save_lisp_thm("X64_LISP_DIV2",result) end; 1257 1258 1259(* safe car and cdr *) 1260 1261fun X64_LISP_SAFE_CAR_AUX i = let 1262 val _ = print "z" 1263 val enc = x64_encodeLib.x64_encode 1264 val hex = enc ("mov "^ x64_reg i ^"d, [r6+4*"^ x64_reg i ^"]") 1265 val code = [enc ("test "^ x64_reg i ^",1"), 1266 enc ("cmovne "^ x64_reg i ^",r0"), 1267 enc ("jne " ^ int_to_string (size hex div 2)), 1268 hex] 1269 val (th,f) = basic_decompile_strings x64_tools "foo" NONE code 1270 val def = SIMP_RULE std_ss [LET_DEF] (CONJ (GSYM mc_safe_car_def) (GSYM mc_safe_car_pre_def)) 1271 val f = RW [def] (SIMP_RULE std_ss [LET_DEF,def] f) 1272 val th = RW [f] th 1273 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_car_thm))) 1274 val def = zLISP_def 1275 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1276 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1277 val s = [Term[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term[QUOTE ("SAFE_CAR x" ^ int_to_string i)]] 1278 val post_tm = subst s post_tm 1279 val res = prove_spec th imp def pre_tm post_tm 1280 in res end; 1281 1282fun X64_LISP_SAFE_CDR_AUX i = let 1283 val _ = print "z" 1284 val enc = x64_encodeLib.x64_encode 1285 val hex = enc ("mov "^ x64_reg i ^"d, [r6+4*"^ x64_reg i ^"+4]") 1286 val code = [enc ("test "^ x64_reg i ^",1"), 1287 enc ("cmovne "^ x64_reg i ^",r0"), 1288 enc ("jne " ^ int_to_string (size hex div 2)), 1289 hex] 1290 val (th,f) = basic_decompile_strings x64_tools "foo" NONE code 1291 val def = SIMP_RULE std_ss [LET_DEF] (CONJ (GSYM mc_safe_cdr_def) (GSYM mc_safe_cdr_pre_def)) 1292 val f = RW [def] (SIMP_RULE std_ss [LET_DEF,def] f) 1293 val th = RW [f] th 1294 val imp = DISCH_ALL (el (i+1) (CONJUNCTS (UNDISCH mc_safe_cdr_thm))) 1295 val def = zLISP_def 1296 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1297 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1298 val s = [Term[QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> Term[QUOTE ("SAFE_CDR x" ^ int_to_string i)]] 1299 val post_tm = subst s post_tm 1300 val res = prove_spec th imp def pre_tm post_tm 1301 in res end; 1302 1303val ALL_X64_LISP_SAFE_CAR = map X64_LISP_SAFE_CAR_AUX [0,1,2,3,4,5] 1304val ALL_X64_LISP_SAFE_CDR = map X64_LISP_SAFE_CDR_AUX [0,1,2,3,4,5] 1305 1306fun X64_LISP_SAFE_CAR_CDR (i,j) = (print "z"; 1307 if i = j then let 1308 val postfix = (int_to_string i) ^ (int_to_string j) 1309 val th_car = el (i+1) ALL_X64_LISP_SAFE_CAR 1310 val th_cdr = el (i+1) ALL_X64_LISP_SAFE_CDR 1311 val _ = save_lisp_thm("X64_LISP_SAFE_CAR" ^ postfix,th_car) 1312 val _ = save_lisp_thm("X64_LISP_SAFE_CDR" ^ postfix,th_cdr) 1313 in (th_car,th_cdr) end else let 1314 val postfix = (int_to_string i) ^ (int_to_string j) 1315 val th = fetch "-" ("X64_LISP_MOVE" ^ postfix) 1316 val th_car = SPEC_COMPOSE_RULE [th,el (i+1) ALL_X64_LISP_SAFE_CAR] 1317 val th_cdr = SPEC_COMPOSE_RULE [th,el (i+1) ALL_X64_LISP_SAFE_CDR] 1318 val _ = save_lisp_thm("X64_LISP_SAFE_CAR" ^ postfix,th_car) 1319 val _ = save_lisp_thm("X64_LISP_SAFE_CDR" ^ postfix,th_cdr) 1320 in (th_car,th_cdr) end); 1321 1322val _ = map X64_LISP_SAFE_CAR_CDR all_reg_pairs; 1323 1324 1325(* sfix *) 1326 1327val fix_lemma = prove( 1328 ``(b ==> SPEC m p c (q1 * q)) ==> 1329 (~b ==> SPEC m p c (q2 * q)) ==> 1330 SPEC m p c ((if b then q1 else q2) * q)``, 1331 METIS_TAC []); 1332 1333val SFIX_def = Define `SFIX s = if isSym s then s else Sym "NIL"`; 1334 1335fun X64_LISP_SFIX i = let 1336 val _ = print "z" 1337 val s = "cmovne " ^ (x64_reg i) ^ "d, r0d" 1338 val s = x64_encode s 1339 val (spec,_,sts,_) = x64_tools 1340 val ((th1,_,_),ex) = spec s 1341 fun the (SOME x) = x | the _ = fail(); 1342 val (th2,_,_) = the ex 1343 val def = zLISP_def 1344 val imp = lisp_inv_swap0 1345 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond z_zf`` 1346 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)`` 1347 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th2) 1348 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1349 val result2 = prove_spec th2 imp def pre_tm post_tm 1350 val imp = UNDISCH lisp_inv_nil 1351 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 1352 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 1353 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond ~z_zf`` 1354 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)`` 1355 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->``Sym "NIL"``] post_tm 1356 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th1) 1357 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1358 val result1 = prove_spec th1 imp def pre_tm post_tm 1359 val res1 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result1) 1360 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) 1361 val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1) 1362 val test = fetch "-" ("X64_LISP_ISSYM" ^ int_to_string i) 1363 val res = SPEC_COMPOSE_RULE [test,res] 1364 val res = HIDE_STATUS_RULE true sts res 1365 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1366 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->Term [QUOTE ("SFIX x" ^ int_to_string i ^ ": SExp")]] post_tm 1367 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl res) 1368 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1369 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN res) 1370 val goal = (cdr o car o concl) th 1371 val lemma = prove(goal,SRW_TAC [] [] \\ ASM_SIMP_TAC std_ss [SEP_IMP_def,SFIX_def]) 1372 val th = MP th lemma 1373 in save_lisp_thm("X64_LISP_SFIX_" ^ int_to_string i,th) end; 1374 1375val _ = map X64_LISP_SFIX all_regs; 1376 1377 1378(* nfix *) 1379 1380val NFIX_def = Define `NFIX s = if isVal s then s else Val 0`; 1381 1382fun X64_LISP_NFIX i = let 1383 val _ = print "z" 1384 val s = "cmovne " ^ (x64_reg i) ^ "d, r1d" 1385 val s = x64_encode s 1386 val (spec,_,sts,_) = x64_tools 1387 val ((th1,_,_),ex) = spec s 1388 fun the (SOME x) = x | the _ = fail(); 1389 val (th2,_,_) = the ex 1390 val def = zLISP_def 1391 val imp = lisp_inv_swap0 1392 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond z_zf`` 1393 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)`` 1394 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th2) 1395 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1396 val result2 = prove_spec th2 imp def pre_tm post_tm 1397 val imp = UNDISCH lisp_inv_zero 1398 val imp = DISCH_ALL (MATCH_MP (swap_thm i) imp) 1399 val imp = DISCH_ALL (MATCH_MP imp (UNDISCH (swap_thm i))) 1400 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond ~z_zf`` 1401 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)`` 1402 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->``Val 0``] post_tm 1403 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th1) 1404 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1405 val result1 = prove_spec th1 imp def pre_tm post_tm 1406 val res1 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result1) 1407 val res2 = RW [GSYM STAR_ASSOC] (RW [precond_def,SPEC_MOVE_COND] result2) 1408 val res = RW [STAR_ASSOC] (MATCH_MP (MATCH_MP fix_lemma res2) res1) 1409 val test = fetch "-" ("X64_LISP_ISVAL" ^ int_to_string i) 1410 val res = SPEC_COMPOSE_RULE [test,res] 1411 val res = HIDE_STATUS_RULE true sts res 1412 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1413 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->Term [QUOTE ("NFIX x" ^ int_to_string i ^ ": SExp")]] post_tm 1414 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl res) 1415 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1416 val th = SPEC post_tm (MATCH_MP SPEC_WEAKEN res) 1417 val goal = (cdr o car o concl) th 1418 val lemma = prove(goal,SRW_TAC [] [] \\ ASM_SIMP_TAC std_ss [SEP_IMP_def,NFIX_def]) 1419 val th = MP th lemma 1420 in save_lisp_thm("X64_LISP_NFIX_" ^ int_to_string i,th) end; 1421 1422val _ = map X64_LISP_NFIX all_regs; 1423 1424 1425(* print statistics -- used before and after gc *) 1426 1427val stats = [(``1``, mc_print_stats1_spec, mc_print_stats1_thm, "1"), 1428 (``2``, mc_print_stats2_spec, mc_print_stats2_thm, "2")] 1429 1430fun X64_LISP_PRINT_STATS (tm,th,imp,name) = let 1431 val th = Q.INST [`ior`|->`EL 0 cs`, 1432 `iow`|->`EL 1 cs`, 1433 `iod`|->`EL 2 cs`, 1434 `ioi`|->`EL 0 ds`, 1435 `r8`|->`w2w (w0:word32)`] th 1436 val imp = SIMP_RULE std_ss [LET_DEF] imp 1437 val def = zLISP_def 1438 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1439 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,IO_STATS ^tm io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1440 val res = prove_spec th imp def pre_tm post_tm 1441 in save_lisp_thm("X64_LISP_PRINT_STATS" ^ name, res) end; 1442 1443val X64_LISP_PRINT_STATS_BEGIN = X64_LISP_PRINT_STATS (el 1 stats); 1444val X64_LISP_PRINT_STATS_END = X64_LISP_PRINT_STATS (el 2 stats); 1445 1446 1447(* push and cons test *) 1448 1449val SPEC_MERGE_LEMMA = prove( 1450 ``SPEC m p c q ==> SPEC m p (c UNION c') (q \/ q') /\ 1451 SPEC m p (c' UNION c) (q' \/ q)``, 1452 `SEP_IMP q (q \/ q')` by SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] 1453 \\ `SEP_IMP q (q' \/ q)` by SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] 1454 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC SPEC_WEAKEN 1455 \\ METIS_TAC [SPEC_ADD_CODE,UNION_COMM]); 1456 1457val push_lemma = prove( 1458 ``SPEC X64_MODEL 1459 (zLISP_ALT b1 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c1 q1 ==> 1460 SPEC X64_MODEL 1461 (zLISP_ALT b2 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c2 q2 ==> 1462 (!wsp wi we ds tw2. b1 wsp wi we ds tw2 \/ b2 wsp wi we ds tw2) ==> 1463 SPEC X64_MODEL 1464 (zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) (c1 UNION c2) (q1 \/ q2)``, 1465 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_def,SEP_CLAUSES,GSYM SPEC_PRE_EXISTS, 1466 SPEC_MOVE_COND,zLISP_ALT_def] 1467 \\ REPEAT STRIP_TAC 1468 \\ Q.PAT_X_ASSUM `!wsp wi we ds tw2. b1 wsp wi we ds tw2 \/ b2 wsp wi we ds tw2` (STRIP_ASSUME_TAC o SPEC_ALL) 1469 \\ RES_TAC \\ METIS_TAC [SPEC_MERGE_LEMMA]); 1470 1471val X64_LISP_PUSH_TEST = let 1472 val branch_taken_prefix = "3E" 1473 val x1 = x64_encodeLib.x64_encode "test r3,r3" 1474 val x2 = branch_taken_prefix ^ (x64_encodeLib.x64_encode "jne 9") 1475 val x3 = x64_encodeLib.x64_encode "mov r2d,r1d" 1476 val x4 = x64_encodeLib.x64_encode "jmp [r7-200]" 1477 val (spec,_,sts,_) = x64_tools 1478 val ((th1,_,_),_) = spec x1 1479 val ((th2,_,_),th2a) = spec x2 1480 val ((th3,_,_),_) = spec x3 1481 fun the (SOME x) = x | the _ = fail(); 1482 val (th2b,_,_) = the th2a 1483 val th = SPEC_COMPOSE_RULE [th1,th2b,th3] 1484 val th = HIDE_STATUS_RULE true sts th 1485 val th = RW [precond_def] th 1486 val def = zLISP_ALT_def 1487 val imp = Q.INST [`temp`|->`(31 -- 0) tw1`] lisp_inv_ignore_tw2 1488 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1489 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1490 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1491 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1492 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1493 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1494 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1495 val post1_tm = subst [``rip:word64`` |-> cdr tm] post1_tm 1496 val result2 = prove_spec th imp def pre_tm post_tm 1497 val (th,goal) = SPEC_WEAKEN_RULE result2 post1_tm 1498 val lemma = prove(goal,SIMP_TAC std_ss [GSYM STAR_ASSOC,SEP_IMP_zLISP_ALT_zLISP]) 1499 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] 1500 val th = SPEC_COMPOSE_RULE [th1,th2] 1501 val th = HIDE_STATUS_RULE true sts th 1502 val th = RW [precond_def] th 1503 val def = zLISP_ALT_def 1504 val imp = lisp_inv_swap0 1505 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1506 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1507 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1508 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1509 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1510 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1511 val res1 = prove_spec th imp def pre_tm post_tm 1512 val th = MATCH_MP push_lemma (RW [GSYM STAR_ASSOC] res1) 1513 val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2) 1514 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [markerTheory.Abbrev_def])) th 1515 val set_lemma = prove( 1516 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``, 1517 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 1518 val th = RW [STAR_ASSOC,set_lemma] th 1519 in th end; 1520 1521val X64_LISP_CONS_TEST = let 1522 val cons_test_code = 1523 (codegenLib.assemble "x64" ` 1524 cmp r14,r15 1525 jne L 1526 xor r2d,r2d 1527 jmp [r7-200] 1528 L: `) 1529 val (spec,_,sts,_) = x64_tools 1530 val ((th1,_,_),_) = spec (el 1 cons_test_code) 1531 val ((th2,_,_),th2a) = spec (el 2 cons_test_code) 1532 val ((th3,_,_),_) = spec (el 3 cons_test_code) 1533 fun the (SOME x) = x | the _ = fail(); 1534 val (th2b,_,_) = the th2a 1535 val th = SPEC_COMPOSE_RULE [th1,th2b,th3] 1536 val th = HIDE_STATUS_RULE true sts th 1537 val th = RW [precond_def] th 1538 val def = zLISP_ALT_def 1539 val imp = Q.INST [`temp`|->`0w`] lisp_inv_ignore_tw2 1540 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1541 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1542 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1543 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1544 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1545 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1546 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1547 val post1_tm = subst [``rip:word64`` |-> cdr tm] post1_tm 1548 val result2 = prove_spec th imp def pre_tm post_tm 1549 val (th,goal) = SPEC_WEAKEN_RULE result2 post1_tm 1550 val lemma = prove(goal,SIMP_TAC std_ss [GSYM STAR_ASSOC,SEP_IMP_zLISP_ALT_zLISP]) 1551 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] 1552 val th = SPEC_COMPOSE_RULE [th1,th2] 1553 val th = HIDE_STATUS_RULE true sts th 1554 val th = RW [precond_def] th 1555 val def = zLISP_ALT_def 1556 val imp = lisp_inv_swap0 1557 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1558 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1559 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1560 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1561 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1562 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1563 val res1 = prove_spec th imp def pre_tm post_tm 1564 val th = MATCH_MP push_lemma (RW [GSYM STAR_ASSOC] res1) 1565 val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2) 1566 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [markerTheory.Abbrev_def])) th 1567 val set_lemma = prove( 1568 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``, 1569 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 1570 val th = RW [STAR_ASSOC,set_lemma] th 1571 in th end; 1572 1573val SPEC_DISJ_FRAME_LEMMA = prove( 1574 ``(s \/ SEP_F = s) /\ (SEP_F \/ s = s)``, 1575 SIMP_TAC std_ss [FUN_EQ_THM,SEP_DISJ_def,SEP_F_def]); 1576 1577val SPEC_DISJ_FRAME = prove( 1578 ``!x p c q. SPEC x p c q ==> !r. SPEC x (p \/ r) c (q \/ r)``, 1579 METIS_TAC [SPEC_MERGE,SPEC_REFL,UNION_IDEMPOT,SPEC_DISJ_FRAME_LEMMA]); 1580 1581val SPEC_DISJ_COMPOSE = prove( 1582 ``SPEC m q c2 q1 ==> 1583 SPEC m p c1 (q \/ q2) ==> 1584 SPEC m p (c1 UNION c2) (q1 \/ q2)``, 1585 REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_COMPOSE \\ Q.EXISTS_TAC `q \/ q2` 1586 \\ ASM_SIMP_TAC std_ss [SPEC_DISJ_FRAME]); 1587 1588val X64_LISP_FULL_GC = let 1589 val lemma = prove(``!x n. IO_STATS n x = x``,Cases THEN SIMP_TAC std_ss [IO_STATS_def]) 1590 val th0 = fetch "-" "X64_LISP_CALL_EL5" 1591 val th1 = X64_LISP_PRINT_STATS_BEGIN 1592 val th2 = X64_LISP_GC 1593 val th3 = X64_LISP_PRINT_STATS_END 1594 val th4 = X64_LISP_CONS_TEST 1595 val th5 = Q.INST [`b`|->`(\wsp wi we ds tw2. Abbrev (wi <> we))`] X64_LISP_ALT_RET 1596 val th = RW [lemma] (SPEC_COMPOSE_RULE [th1,th2,th3,th4]) 1597 val th = MATCH_MP (MATCH_MP SPEC_DISJ_COMPOSE th5) (Q.INST [`qs`|->`q::qs`] th) 1598 val th = RW [INSERT_UNION_EQ,UNION_EMPTY] th 1599 val (_,_,c,_) = dest_spec (concl th) 1600 val name = mk_var("abbrev_code_for_cons",mk_type("fun",[``:word64``,type_of c])) 1601 val def = Define [ANTIQUOTE (mk_eq(mk_comb(name,``p:word64``),c))] 1602 val th = RW [GSYM def] th 1603 val th = SPEC_COMPOSE_RULE [th0,th] 1604 in th end; 1605 1606val X64_LISP_CONS_TEST_WITH_GC = let 1607 val branch_taken_prefix = "3E" 1608 val x1 = x64_encodeLib.x64_encode "cmp r14,r15" 1609 val x2 = branch_taken_prefix ^ (x64_encodeLib.x64_encode "jne 10") 1610 val (spec,_,sts,_) = x64_tools 1611 val ((th1,_,_),_) = spec x1 1612 val ((th2,_,_),th2a) = spec x2 1613 fun the (SOME x) = x | the _ = fail(); 1614 val (th2b,_,_) = the th2a 1615 (* case: gc call *) 1616 val th = SPEC_COMPOSE_RULE [th1,th2b] 1617 val th = HIDE_STATUS_RULE true sts th 1618 val th = RW [precond_def] th 1619 val th = Q.INST [`rip` |-> `p`] th 1620 val def = zLISP_ALT_def 1621 val imp = lisp_inv_swap0 1622 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1623 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1624 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1625 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1626 val res2 = prove_spec th imp def pre_tm post_tm 1627 val res2 = RW [GSYM zLISP_raw] res2 1628 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_FULL_GC] 1629 (* case: no gc call *) 1630 val th = SPEC_COMPOSE_RULE [th1,th2] 1631 val th = HIDE_STATUS_RULE true sts th 1632 val th = RW [precond_def] th 1633 val th = Q.INST [`rip` |-> `p`] th 1634 val def = zLISP_ALT_def 1635 val imp = lisp_inv_swap0 1636 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 1637 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 1638 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1639 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1640 val res1 = prove_spec th imp def pre_tm post_tm 1641 val th = MATCH_MP push_lemma (RW [GSYM STAR_ASSOC] res1) 1642 val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2) 1643 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [markerTheory.Abbrev_def])) th 1644 val set_lemma = prove( 1645 ``(x1 INSERT s) UNION (x1 INSERT t) = x1 INSERT (s UNION t)``, 1646 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 1647 val th = RW [STAR_ASSOC,set_lemma,UNION_EMPTY] th 1648 val th = RW [SEP_CLAUSES,GSYM SEP_DISJ_ASSOC] th 1649 in th end; 1650 1651 1652(* push *) 1653 1654val SPEC_DISJ_COMPOSE = prove( 1655 ``SPEC m q c2 q1 ==> 1656 SPEC m p c1 (q \/ q2) ==> 1657 SPEC m p (c1 UNION c2) (q1 \/ q2)``, 1658 REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_COMPOSE \\ Q.EXISTS_TAC `q \/ q2` 1659 \\ ASM_SIMP_TAC std_ss [SPEC_DISJ_FRAME]); 1660 1661fun X64_LISP_PUSH i = let 1662 val _ = print "z" 1663 val (spec,_,sts,_) = x64_tools 1664 val ((th1,_,_),_) = spec (x64_encode ("dec r3")) 1665 val ((th2,_,_),_) = spec (x64_encode ("mov [r7+4*r3], " ^ x64_reg i ^ "d")) 1666 val th = SPEC_COMPOSE_RULE [th1,th2] 1667 val th = HIDE_STATUS_RULE true sts th 1668 val th = RW [car_blast] th 1669 val def = zLISP_ALT_def 1670 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp <> 0x0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1671 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,x::xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1672 val s = [``x:SExp`` |-> (Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")])] 1673 val post_tm = subst s post_tm 1674 val imp = UNDISCH (CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM markerTheory.Abbrev_def])) lisp_inv_push) 1675 val assum = hd (hyp imp) 1676 val thi = CONJUNCT1 (UNDISCH (imp)) 1677 val thi = DISCH_ALL (MATCH_MP (swap_thm i) thi) 1678 val thi = DISCH_ALL (MATCH_MP thi (UNDISCH (swap_thm i))) 1679 val thj = CONJUNCT2 (UNDISCH (imp)) 1680 val thj = DISCH_ALL (MATCH_MP (DISCH_ALL thj) (UNDISCH (swap_thm i))) 1681 val imp = (CONJ (UNDISCH_ALL thi) (UNDISCH_ALL thj)) 1682 val assum2 = hd (filter (fn x => x !~ assum) (hyp imp)) 1683 val imp = DISCH assum2 imp 1684 val result = prove_spec th imp def pre_tm post_tm 1685 val result = RW [GSYM zLISP_raw] result 1686 val th = MATCH_MP (MATCH_MP SPEC_DISJ_COMPOSE result) X64_LISP_PUSH_TEST 1687 val th = SIMP_RULE std_ss [INSERT_UNION_EQ,UNION_EMPTY,word_arith_lemma1] th 1688 in save_lisp_thm("X64_LISP_PUSH_" ^ int_to_string i,th) end; 1689 1690val _ = map X64_LISP_PUSH all_regs; 1691 1692 1693(* cons *) 1694 1695val lisp_inv_cons_alt = 1696 CONV_RULE ((RATOR_CONV o RAND_CONV) (ONCE_REWRITE_CONV [GSYM markerTheory.Abbrev_def])) lisp_inv_cons; 1697 1698fun aux_swap th i j = let 1699 val thi = CONJUNCT1 (UNDISCH_ALL th) 1700 val thi = DISCH_ALL (MATCH_MP (generate_swap i j) thi) 1701 val thi = DISCH_ALL (MATCH_MP thi (UNDISCH (generate_swap i j))) 1702 val thj = CONJUNCT2 (UNDISCH_ALL th) 1703 val thj = DISCH_ALL (MATCH_MP (DISCH_ALL thj) (UNDISCH (generate_swap i j))) 1704 in CONJ (UNDISCH_ALL thi) (UNDISCH_ALL thj) end 1705 1706fun generate_cons i j = 1707 if i = 0 andalso j = 1 then UNDISCH_ALL lisp_inv_cons_alt else 1708 if i = 0 then aux_swap lisp_inv_cons_alt 1 j else 1709 if i = 1 then let 1710 val th = aux_swap lisp_inv_cons_alt 0 1 1711 val th = aux_swap th 0 j 1712 in th end 1713 else if j = 1 then aux_swap lisp_inv_cons_alt 0 i else let 1714 val th = aux_swap lisp_inv_cons_alt 0 i 1715 val th = aux_swap th 1 j 1716 in th end; 1717 1718fun X64_LISP_CONS (i,j) = if i = j then TRUTH else let 1719 val _ = print "z" 1720 val (spec,_,sts,_) = x64_tools 1721 val ((th1,_,_),_) = spec (x64_encode ("mov [r6+4*r14+4], " ^ x64_reg j ^ "d")) 1722 val ((th2,_,_),_) = spec (x64_encode ("mov [r6+4*r14], " ^ x64_reg i ^ "d")) 1723 val ((th3,_,_),_) = spec (x64_encode ("mov " ^ x64_reg i ^ "d, r14d")) 1724 val ((th4,_,_),_) = spec (x64_encode ("add r14,2")) 1725 val th = SPEC_COMPOSE_RULE [th1,th2,th3,th4] 1726 val th = HIDE_STATUS_RULE true sts th 1727 val th = Q.INST [[QUOTE (x64_reg i ^ ":word64")]|->`w2w (a:word32)`] th 1728 val th = Q.INST [[QUOTE (x64_reg j ^ ":word64")]|->`w2w (b:word32)`] th 1729 val th = RW [car_blast] th 1730 val def = zLISP_ALT_def 1731 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi <> we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1732 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1733 val s = [Term [QUOTE ("x" ^ int_to_string i ^ ":SExp")] |-> 1734 Term [QUOTE ("Dot x" ^ int_to_string i ^ " x" ^ int_to_string j)]] 1735 val post_tm = subst s post_tm 1736 val imp = generate_cons i j 1737 val h = lisp_inv_cons_alt |> concl |> dest_imp |> fst 1738 val assum = hd (filter (fn x => x !~ h) (hyp imp)) 1739 val imp = DISCH assum imp 1740 val result = prove_spec th imp def pre_tm post_tm 1741 val result = RW [GSYM zLISP_raw] result 1742 val th = MATCH_MP (MATCH_MP SPEC_DISJ_COMPOSE result) X64_LISP_CONS_TEST_WITH_GC 1743 val th = SIMP_RULE std_ss [word_arith_lemma1,INSERT_UNION_EQ] th 1744 in save_lisp_thm("X64_LISP_CONS_" ^ int_to_string i ^ int_to_string j,th) end; 1745 1746val _ = map X64_LISP_CONS all_distinct_reg_pairs; 1747 1748 1749(* pop *) 1750 1751val X64_LISP_POP = save_lisp_thm("X64_LISP_POP",let 1752 val _ = print "z" 1753 val s = "inc r3" 1754 val s = x64_encode s 1755 val (spec,_,sts,_) = x64_tools 1756 val ((th,_,_),_) = spec s 1757 val th = HIDE_STATUS_RULE true sts th 1758 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1759 val imp = RW1 [lemma] lisp_inv_pop 1760 val def = zLISP_def 1761 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1762 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,TL xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1763 val res = prove_spec th imp def pre_tm post_tm 1764 in res end); 1765 1766 1767(* top *) 1768 1769fun generate_top i = let 1770 val th = CONJUNCT1 (UNDISCH (UNDISCH lisp_inv_top)) 1771 val th = DISCH_ALL (MATCH_MP (swap_thm i) th) 1772 val th = DISCH_ALL (MATCH_MP th (UNDISCH (swap_thm i))) 1773 val th1 = CONJUNCT2 (UNDISCH (UNDISCH lisp_inv_top)) 1774 val th1 = DISCH_ALL (MATCH_MP (DISCH_ALL th1) (UNDISCH (swap_thm i))) 1775 val th2 = UNDISCH (RW [AND_IMP_INTRO] th) 1776 val th3 = UNDISCH (RW [AND_IMP_INTRO] th1) 1777 in RW [GSYM AND_IMP_INTRO] (DISCH_ALL (CONJ th2 th3)) end; 1778 1779fun X64_LISP_TOP i = let 1780 val _ = print "z" 1781 val s = "mov " ^ (x64_reg i) ^ "d, [r7+4*r3]" 1782 val s = x64_encode s 1783 val (spec,_,sts,_) = x64_tools 1784 val ((th,_,_),_) = spec s 1785 val def = zLISP_def 1786 val imp = generate_top i 1787 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1788 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1789 val post_tm = subst [Term [QUOTE ("x" ^ int_to_string i ^ ": SExp")]|->``(HD xs):SExp``] post_tm 1790 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 1791 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 1792 val th = RW [car_blast] th 1793 val result = prove_spec th imp def pre_tm post_tm 1794 in save_lisp_thm("X64_LISP_TOP_" ^ int_to_string i,result) end; 1795 1796val _ = map X64_LISP_TOP all_regs; 1797 1798 1799(* load *) 1800 1801val load_blast = prove( 1802 ``!j. n2w (SIGN_EXTEND 32 64 (w2n ((0x4w:word32) * w2w (j:29 word)))) = 1803 4w * (w2w j):word64``, 1804 Cases \\ ASM_SIMP_TAC std_ss [w2w_def,w2n_n2w,word_mul_n2w] 1805 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 1806 \\ `(4 * n) < 4294967296` by DECIDE_TAC 1807 \\ `(4 * n) < 2147483648` by DECIDE_TAC 1808 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 1809 \\ FULL_SIMP_TAC std_ss [SIGN_EXTEND_def,LET_DEF] 1810 \\ FULL_SIMP_TAC std_ss [BIT_def,BITS_THM,LESS_DIV_EQ_ZERO]); 1811 1812val X64_LISP_LOAD = save_lisp_thm("X64_LISP_LOAD",let 1813 val s = "mov r8d, [r7+4*r3+6000]" 1814 val s = x64_encode s 1815 val (spec,_,sts,_) = x64_tools 1816 val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8)) 1817 val th = RW [GSYM w2w_def,car_blast] th 1818 val th = Q.INST [`imm32`|->`4w*w2w (j:29 word)`] th 1819 val th = RW [load_blast] th 1820 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1821 val imp = RW1[lemma]lisp_inv_load 1822 val def = zLISP_def 1823 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1824 val post_tm = set_pc th ``zLISP ^STAT (EL (w2n (j:29 word)) xs,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1825 val res = prove_spec th imp def pre_tm post_tm 1826 in res end); 1827 1828 1829(* store *) 1830 1831val X64_LISP_STORE = save_lisp_thm("X64_LISP_STORE",let 1832 val s = "mov [r7+4*r3+256], r8d" 1833 val s = x64_encode s 1834 val (spec,_,sts,_) = x64_tools 1835 val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8)) 1836 val th = RW [GSYM w2w_def,car_blast] th 1837 val th = Q.INST [`imm32`|->`4w*w2w (j:29 word)`] th 1838 val th = RW [load_blast] th 1839 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1840 val imp = RW1[lemma]lisp_inv_store 1841 val def = zLISP_def 1842 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1843 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,UPDATE_NTH (w2n (j:29 word)) x0 xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1844 val res = prove_spec th imp def pre_tm post_tm 1845 in res end); 1846 1847 1848(* pops *) 1849 1850val X64_LISP_POPS_LEMMA = prove( 1851 ``SIGN_EXTEND 32 64 (w2n ((w2w imm30):word32)) = w2n (imm30:word30)``, 1852 Cases_on `imm30` \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [bitTheory.SIGN_EXTEND_def, 1853 LET_DEF,bitTheory.BIT_def,bitTheory.BITS_THM,w2w_def,w2n_n2w] 1854 \\ `n < 4294967296` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1855 \\ `n < 2147483648` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss [] 1856 \\ IMP_RES_TAC LESS_DIV_EQ_ZERO \\ ASM_SIMP_TAC std_ss []); 1857 1858val X64_LISP_POPS = save_lisp_thm("X64_LISP_POPS",let 1859 val _ = print "z" 1860 val s = "add r3,5000" 1861 val s = x64_encode s 1862 val (spec,_,sts,_) = x64_tools 1863 val ((th,_,_),_) = spec (String.substring(s,0,size(s)-8)) 1864 val th = Q.INST [`imm32`|->`w2w (imm30:word30)`] th 1865 val th = HIDE_STATUS_RULE true sts th 1866 val th = RW [X64_LISP_POPS_LEMMA,GSYM w2w_def] th 1867 val th = Q.INST [`imm30`|->`j`] th 1868 val lemma = METIS_PROVE [] ``(b==>c==>d) = (c==>b==>d)`` 1869 val imp = RW1 [lemma] (SIMP_RULE std_ss [LET_DEF] lisp_inv_pops) 1870 val def = zLISP_def 1871 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1872 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,DROP (w2n (j:word30)) xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 1873 val res = prove_spec th imp def pre_tm post_tm 1874 in res end); 1875 1876 1877(* print various strings *) 1878 1879val prints = [(``"\n"``, mc_print_nl_spec,mc_print_nl_thm,"NEWLINE"), 1880 (``"'"``, mc_print_qt_spec,mc_print_qt_thm,"QUOTE"), 1881 (``"("``, mc_print_open_spec,mc_print_open_thm,"OPEN"), 1882 (``")"``, mc_print_close_spec,mc_print_close_thm,"CLOSE"), 1883 (``" . "``, mc_print_dot_spec,mc_print_dot_thm,"DOT"), 1884 (``" "``, mc_print_sp_spec,mc_print_sp_thm,"SPACE")] 1885 1886fun X64_LISP_PRINT (tm,th,imp,name) = let 1887 val th = Q.INST [`ior`|->`EL 0 cs`, 1888 `x`|->`EL 1 cs`, 1889 `y`|->`EL 2 cs`, 1890 `z`|->`EL 0 ds`] th 1891 val imp = SIMP_RULE std_ss [LET_DEF] imp 1892 val def = zLISP_def 1893 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1894 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,IO_WRITE io ^tm,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1895 val res = prove_spec th imp def pre_tm post_tm 1896 in save_lisp_thm("X64_LISP_PRINT_" ^ name, res) end; 1897 1898val _ = map X64_LISP_PRINT prints; 1899 1900 1901(* print number *) 1902 1903val X64_LISP_PRINT_NUMBER = save_lisp_thm("X64_LISP_PRINT_NUMBER",let 1904 val th = Q.INST [`ior`|->`EL 0 cs`, 1905 `x`|->`EL 1 cs`, 1906 `y`|->`EL 2 cs`, 1907 `z`|->`EL 0 ds`] mc_print_num_full_spec 1908 val imp = mc_print_num_full_thm 1909 val def = zLISP_def 1910 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1911 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,xs,xs1,IO_WRITE io (num2str (getVal x0)),xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1912 val res = prove_spec th imp def pre_tm post_tm 1913 in res end); 1914 1915 1916(* print symbol *) 1917 1918val X64_LISP_PRINT_SYMBOL = save_lisp_thm("X64_LISP_PRINT_SYMBOL",let 1919 val th = Q.INST [`ior`|->`EL 0 cs`, 1920 `x`|->`EL 1 cs`, 1921 `y`|->`EL 2 cs`, 1922 `z`|->`EL 0 ds`] mc_print_sym_full_spec 1923 val imp = mc_print_sym_full_thm 1924 val def = zLISP_def 1925 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1926 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,xs,xs1,IO_WRITE io (sym2str (getSym x0)),xbp,qs,code,amnt,ok) * zPC p * ~zS`` 1927 val res = prove_spec th imp def pre_tm post_tm 1928 in res end); 1929 1930 1931(* init *) 1932 1933val X64_LISP_INIT = save_thm("X64_LISP_INIT",let 1934 val th = SPEC_FRAME_RULE mc_full_init_spec ``zIO (EL 0 cs,EL 1 cs,EL 2 cs,EL 0 ds) io * zCODE_MEMORY ddd dd d * zSTACK rbp qs * zCODE_UNCHANGED cu dd d * cond (lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds))`` 1935 val th = Q.INST [`r7`|->`sp`] th 1936 val post = set_pc th ``zLISP ^STAT (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",[],[],io,0,qs,NO_CODE,w2n (EL 3 cs),T) * zPC p * ~zS`` 1937 val (th,goal) = SPEC_WEAKEN_RULE th post 1938 val lemma = prove(goal, 1939 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,STAR_ASSOC] \\ STRIP_TAC 1940 \\ IMP_RES_TAC mc_full_init_thm \\ ASM_SIMP_TAC std_ss [LET_DEF,zLISP_def] 1941 \\ ASM_SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS_THM,SEP_CLAUSES,cond_STAR] 1942 \\ Q.PAT_X_ASSUM `!qs.bbb` (MP_TAC o SPEC_ALL) \\ STRIP_TAC 1943 \\ ASM_SIMP_TAC std_ss [] 1944 \\ REPEAT STRIP_TAC \\ AUTO_EXISTS_TAC \\ ASM_SIMP_TAC std_ss [] 1945 \\ FULL_SIMP_TAC (std_ss++star_ss) [EL_UPDATE_NTH]) 1946 val th = MP th lemma 1947 val th = foldr (uncurry Q.GEN) th [`df`,`f`,`dg`,`g`,`sp`,`sa1`,`sa_len`,`ds`,`dd`,`d`] 1948 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 1949 val pre = ``zLISP_INIT (a1,a2,sl,sl1,e,ex,rbp,cs,qs,ddd,cu) io * zPC p * ~zS`` 1950 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 1951 val lemma = prove(goal, 1952 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_INIT_def,SEP_CLAUSES] 1953 \\ SIMP_TAC (std_ss++star_ss) [] \\ SIMP_TAC std_ss [STAR_ASSOC] 1954 \\ ASM_SIMP_TAC std_ss [SEP_IMP_REFL,mc_full_init_pre_thm]) 1955 val th = MP th lemma 1956 in th end); 1957 1958 1959(* Produce "syntax error" *) 1960 1961val remove_parse_stack_def = PmatchHeuristics.with_classic_heuristic Define ` 1962 (remove_parse_stack (Sym "NIL"::xs) = xs) /\ 1963 (remove_parse_stack (Sym "CONS"::[]) = []) /\ 1964 (remove_parse_stack (Sym "CONS"::x::xs) = remove_parse_stack xs) /\ 1965 (remove_parse_stack (Val n::xs) = remove_parse_stack xs) /\ 1966 (remove_parse_stack (Sym "CAR"::xs) = remove_parse_stack xs) /\ 1967 (remove_parse_stack (Sym "CDR"::xs) = remove_parse_stack xs) /\ 1968 (remove_parse_stack (Sym "QUOTE"::xs) = remove_parse_stack xs)`; 1969 1970val X64_LISP_SYNTAX_ERROR = save_lisp_thm("X64_LISP_SYNTAX_ERROR",let 1971 val s = x64_encode "mov r2d,5" 1972 val (spec,_,sts,_) = x64_tools 1973 val ((th,_,_),_) = spec s 1974 val imp = Q.INST [`temp`|->`5w`] lisp_inv_ignore_tw2 1975 val def = zLISP_def 1976 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1977 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1978 val res = prove_spec th imp def pre_tm post_tm 1979 val th = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 1980 val s2 = x64_encode "jmp [r7-200]" 1981 val s_len = numSyntax.term_of_int (size (s ^ s2) div 2) 1982 val (_,_,_,post2_tm) = dest_spec (concl th) 1983 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,remove_parse_stack xs,xs1,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)`` 1984 val (th,goal) = SPEC_WEAKEN_RULE th (mk_sep_disj(post1_tm,post2_tm)) 1985 val lemma = prove(goal,SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]) 1986 val th = MP th lemma 1987 in th end); 1988 1989val X64_LISP_RAW_RUNTIME_ERROR = save_thm("X64_LISP_RAW_RUNTIME_ERROR",let 1990 val s = x64_encode "mov r2d,4" 1991 val (spec,_,sts,_) = x64_tools 1992 val ((th,_,_),_) = spec s 1993 val imp = Q.INST [`temp`|->`4w`] lisp_inv_ignore_tw2 1994 val def = zLISP_def 1995 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1996 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 1997 val res = prove_spec th imp def pre_tm post_tm 1998 val th = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 1999 in th end); 2000 2001val X64_LISP_RUNTIME_ERROR = save_lisp_thm("X64_LISP_RUNTIME_ERROR",let 2002 val s = x64_encode "mov r2d,4" 2003 val (spec,_,sts,_) = x64_tools 2004 val ((th,_,_),_) = spec s 2005 val th = X64_LISP_RAW_RUNTIME_ERROR 2006 val s2 = x64_encode "jmp [r7-200]" 2007 val s_len = numSyntax.term_of_int (size (s ^ s2) div 2) 2008 val (_,_,_,post2_tm) = dest_spec (concl th) 2009 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,remove_parse_stack xs,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)`` 2010 val (th,goal) = SPEC_WEAKEN_RULE th (mk_sep_disj(post1_tm,post2_tm)) 2011 val lemma = prove(goal,SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]) 2012 val th = MP th lemma 2013 in th end); 2014 2015val no_such_function_def = Define `no_such_function x0 = x0:SExp`; 2016val X64_LISP_ERROR_11 = save_lisp_thm("X64_LISP_ERROR_11",let 2017 val s = x64_encode "mov r2d,11" 2018 val (spec,_,sts,_) = x64_tools 2019 val ((th,_,_),_) = spec s 2020 val imp = Q.INST [`temp`|->`11w`] lisp_inv_ignore_tw2 2021 val def = zLISP_def 2022 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 2023 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip`` 2024 val res = prove_spec th imp def pre_tm post_tm 2025 val th = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 2026 val s2 = x64_encode "jmp [r7-200]" 2027 val s_len = numSyntax.term_of_int (size (s ^ s2) div 2) 2028 val (_,_,_,post2_tm) = dest_spec (concl th) 2029 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (no_such_function x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)`` 2030 val (th,goal) = SPEC_WEAKEN_RULE th (mk_sep_disj(post1_tm,post2_tm)) 2031 val lemma = prove(goal,SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]) 2032 val th = MP th lemma 2033 in th end); 2034 2035 2036(* LISP_R intro and elim *) 2037 2038val (mc_lisp_r_intro_spec,mc_lisp_r_intro_def) = basic_decompile_strings x64_tools "mc_lisp_r_intro" 2039 (SOME (``(r1:word64,r2:word64,r7:word64,df:word64 set,f:word64->word32)``, 2040 ``(r1:word64,r2:word64,r7:word64,df:word64 set,f:word64->word32)``)) 2041 (assemble "x64" ` 2042 mov r2,[r7-184] 2043 mov r1,[r7-112] `); 2044 2045val align_blast = blastLib.BBLAST_PROVE 2046 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 2047 2048val X64_LISP_R_INTRO = let 2049 val th = SPEC_FRAME_RULE mc_lisp_r_intro_spec 2050 ``zR 0x0w tw0 * zR 0x3w wsp * 2051 zR 0x6w bp * zR 0x8w (w2w w0) * zR 0x9w (w2w w1) * 2052 zR 0xAw (w2w w2) * zR 0xBw (w2w w3) * zR 0xCw (w2w w4) * 2053 zR 0xDw (w2w w5) * zR 0xEw wi * zR 0xFw we * zSTACK rbp qs * 2054 zBYTE_MEMORY dg g * zCODE_MEMORY ddd dd d * zIO (EL 0 cs,EL 1 cs,EL 2 cs,EL 0 ds) io * 2055 zCODE_UNCHANGED cu dd d * 2056 cond 2057 (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 2058 (w0,w1,w2,w3,w4,w5,df,f,dg,g,bp,bp2,wsp,wi,we,tw0,tw1,tw2,sp, 2059 ds,sa1,sa2,sa3,dd,d))`` 2060 val th = Q.INST [`r7`|->`sp`,`r1`|->`tw1`,`r2`|->`tw2`] th 2061 val post = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2062 val (th,goal) = SPEC_WEAKEN_RULE th post 2063 val lemma = prove(goal, 2064 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,STAR_ASSOC] \\ STRIP_TAC 2065 \\ FULL_SIMP_TAC std_ss [mc_lisp_r_intro_def] 2066 \\ IMP_RES_TAC lisp_inv_cs_read 2067 \\ IMP_RES_TAC lisp_inv_ds_read 2068 \\ ASM_SIMP_TAC std_ss [LET_DEF] 2069 \\ ASM_SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS_THM,SEP_CLAUSES,cond_STAR,zLISP_R_def] 2070 \\ REPEAT STRIP_TAC \\ AUTO_EXISTS_TAC \\ ASM_SIMP_TAC std_ss [] 2071 \\ SIMP_TAC std_ss [zIO_R_def,SEP_CLAUSES,SEP_EXISTS_THM] 2072 \\ Q.EXISTS_TAC `EL 0 ds` \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2073 val th = MP th lemma 2074 val th = foldr (uncurry Q.GEN) th [`tw0`,`tw1`,`tw2`,`wsp`,`bp`,`sp`,`w0`,`w1`,`w2`,`w3`,`w4`,`w5`,`wi`,`we`,`df`,`f`,`dg`,`g`,`bp2`,`ds`,`sa1`,`sa2`,`sa3`,`dd`,`d`] 2075 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 2076 val pre = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2077 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 2078 val lemma2 = prove( 2079 ``mc_lisp_r_intro_pre (r1,r2,sp,df,f) /\ ^LISP = ^LISP``, 2080 REPEAT STRIP_TAC \\ EQ_TAC \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2081 \\ FULL_SIMP_TAC std_ss [mc_lisp_r_intro_def] 2082 \\ IMP_RES_TAC lisp_inv_cs_read 2083 \\ IMP_RES_TAC lisp_inv_ds_read 2084 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2085 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,LET_DEF,align_blast] 2086 \\ FULL_SIMP_TAC std_ss [n2w_and_3]) 2087 val lemma = prove(goal, 2088 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_def,SEP_CLAUSES] 2089 \\ SIMP_TAC (std_ss++star_ss) [] \\ SIMP_TAC std_ss [STAR_ASSOC] 2090 \\ ASM_SIMP_TAC std_ss [SEP_IMP_REFL,lemma2]) 2091 val th = MP th lemma 2092 in th end; 2093 2094val (mc_lisp_r_elim_spec,mc_lisp_r_elim_def) = basic_decompile_strings x64_tools "mc_lisp_r_elim" 2095 (SOME (``(r1:word64,r2:word64,r7:word64,df:word64 set,f:word64->word32)``, 2096 ``(r1:word64,r2:word64,r7:word64,df:word64 set,f:word64->word32)``)) 2097 (assemble "x64" ` 2098 mov [r7-112],r1 2099 mov r1d,1 2100 mov r2,r1`); 2101 2102val mc_lisp_r_elim_blast = blastLib.BBLAST_PROVE 2103 ``(w2w ((w2w (w >>> 32)):word32) << 32 !! w2w ((w2w (w:word64)):word32) = w) /\ 2104 ((63 >< 32) w = (w2w (w >>> 32)):word32) /\ ((31 >< 0) w = (w2w w):word32)``; 2105 2106val X64_LISP_R_ELIM = let 2107 val th = SPEC_FRAME_RULE mc_lisp_r_elim_spec 2108 ``zR 0x0w tw0 * zR 0x3w wsp * 2109 zR 0x6w bp * zR 0x8w (w2w w0) * zR 0x9w (w2w w1) * 2110 zR 0xAw (w2w w2) * zR 0xBw (w2w w3) * zR 0xCw (w2w w4) * 2111 zR 0xDw (w2w w5) * zR 0xEw wi * zR 0xFw we * zSTACK rbp qs * 2112 zBYTE_MEMORY dg g * zCODE_MEMORY ddd dd d * zIO (EL 0 cs,EL 1 cs,EL 2 cs,r1) io * 2113 zCODE_UNCHANGED cu dd d * 2114 cond 2115 (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 2116 (w0,w1,w2,w3,w4,w5,df,f,dg,g,bp,bp2,wsp,wi,we,tw0,tw1,tw2,sp, 2117 ds,sa1,sa2,sa3,dd,d))`` 2118 val th = Q.INST [`r7`|->`sp`,`r1`|->`r1`,`r2`|->`EL 1 cs`] th 2119 val post = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2120 val (th,goal) = SPEC_WEAKEN_RULE th post 2121 val lemma = prove(goal, 2122 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,STAR_ASSOC] \\ STRIP_TAC 2123 \\ SIMP_TAC std_ss [zIO_R_def,SEP_CLAUSES,SEP_EXISTS_THM] 2124 \\ FULL_SIMP_TAC std_ss [mc_lisp_r_elim_def] 2125 \\ IMP_RES_TAC lisp_inv_cs_read 2126 \\ IMP_RES_TAC lisp_inv_ds_read 2127 \\ ASM_SIMP_TAC std_ss [LET_DEF] 2128 \\ ASM_SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS_THM,SEP_CLAUSES,cond_STAR,zLISP_def] 2129 \\ FULL_SIMP_TAC std_ss [mc_lisp_r_elim_blast] 2130 \\ IMP_RES_TAC (DISCH_ALL (el 2 (CONJUNCTS (UNDISCH lisp_inv_ds_write)))) 2131 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `r1`) 2132 \\ IMP_RES_TAC (GEN_ALL lisp_inv_ignore_tw2) 2133 \\ POP_ASSUM (K ALL_TAC) 2134 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `1w`) 2135 \\ REPEAT STRIP_TAC \\ AUTO_EXISTS_TAC \\ ASM_SIMP_TAC std_ss [] 2136 \\ `EL 0 (UPDATE_NTH 0 r1 ds) = r1` by 2137 (FULL_SIMP_TAC std_ss [lisp_inv_def] 2138 \\ Cases_on `ds` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 2139 \\ ASM_SIMP_TAC std_ss [UPDATE_NTH_def,EL,HD]) 2140 \\ `tw1 = 1w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2141 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2142 val th = MP th lemma 2143 val th = Q.INST [`r1`|->`ioi`] th 2144 val th = foldr (uncurry Q.GEN) th [`tw0`,`tw1`,`tw2`,`wsp`,`bp`,`sp`,`w0`,`w1`,`w2`,`w3`,`w4`,`w5`,`wi`,`we`,`df`,`f`,`dg`,`g`,`bp2`,`ds`,`sa1`,`sa2`,`sa3`,`dd`,`d`,`ioi`] 2145 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 2146 val pre = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2147 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 2148 val lemma2 = prove( 2149 ``mc_lisp_r_elim_pre (ioi,EL 1 cs,sp,df,f) /\ ^LISP = ^LISP``, 2150 REPEAT STRIP_TAC \\ EQ_TAC \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2151 \\ FULL_SIMP_TAC std_ss [mc_lisp_r_elim_def] 2152 \\ IMP_RES_TAC lisp_inv_cs_read 2153 \\ IMP_RES_TAC lisp_inv_ds_read 2154 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2155 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,LET_DEF,align_blast] 2156 \\ FULL_SIMP_TAC std_ss [n2w_and_3]) 2157 val lemma = prove(goal, 2158 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_R_def,SEP_CLAUSES,zIO_R_def] 2159 \\ SIMP_TAC (std_ss++star_ss) [] \\ SIMP_TAC std_ss [STAR_ASSOC] 2160 \\ ASM_SIMP_TAC std_ss [SEP_IMP_REFL,lemma2]) 2161 val th = MP th lemma 2162 in th end; 2163 2164 2165(* test for EOF *) 2166 2167val X64_LISP_TEST_EOF = save_lisp_thm("X64_LISP_TEST_EOF",let 2168 val th = Q.INST [`x`|->`EL 0 cs`, 2169 `r2`|->`EL 1 cs`, 2170 `y`|->`EL 2 cs`] mc_test_eof_spec 2171 val imp = SIMP_RULE std_ss [LET_DEF] mc_test_eof_thm 2172 val def = zLISP_R_def 2173 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2174 val post_tm = set_pc th ``zLISP_R ^STAT ( 2175 LISP_TEST (FST (is_eof (getINPUT io))),x1,x2,x3,x4,x5,xs,xs1, 2176 IO_INPUT_APPLY (SND o is_eof) io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2177 val res = prove_spec th imp def pre_tm post_tm 2178 val res = SPEC_COMPOSE_RULE [X64_LISP_R_INTRO,res,X64_LISP_R_ELIM] 2179 in res end); 2180 2181 2182(* next token *) 2183 2184val next_token1_def = Define `next_token1 s = FST (FST (next_token s))`; 2185val next_token2_def = Define `next_token2 s = SND (FST (next_token s))`; 2186 2187val X64_LISP_NEXT_TOKEN = save_lisp_thm("X64_LISP_NEXT_TOKEN",let 2188 (* part 1 *) 2189 val th = SPEC_FRAME_RULE mc_next_token_spec 2190 ``zR 0x3w wsp * zR 0x6w bp * zR 0xCw (w2w w4) * zR 0xDw (w2w w5) * zR 0xEw wi * 2191 zCODE_MEMORY ddd dd d * zSTACK rbp qs * 2192 zCODE_UNCHANGED cu dd d * 2193 cond (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST) 2194 (w0,w1,w2,w3,w4,w5,df,f,dg,g,bp,bp2,wsp,wi,we,tw0,tw1,tw2, 2195 sp,ds,sa1,sa2,sa3,dd,d))`` 2196 val th = Q.INST [`r7`|->`sp`,`r15`|->`we`,`r2`|->`EL 1 cs`,`x`|->`EL 0 cs`,`y`|->`EL 2 cs`] th 2197 val post = set_pc th ``SEP_EXISTS io1 ok1 zX z0 z1. zLISP_R ^STAT (if ok1 then z0 else zX,if ok1 then z1 else Sym "NIL",Sym "NIL", 2198 Sym "NIL",x4,x5,xs,xs1,io1,xbp,qs,code,amnt,ok) * zPC p * ~zS * cond (if ok1 then FST (next_token (getINPUT io)) = (z0,z1) else isVal zX) * cond (ok1 ==> (IO_INPUT_APPLY (SND o next_token) io = io1))`` 2199 val (th,goal) = SPEC_WEAKEN_RULE th post 2200 val lemma = prove(goal, 2201 SIMP_TAC std_ss [SEP_IMP_MOVE_COND,STAR_ASSOC] \\ STRIP_TAC 2202 \\ IMP_RES_TAC mc_next_token_thm \\ ASM_SIMP_TAC std_ss [LET_DEF] 2203 \\ IMP_RES_TAC lisp_inv_ignore_io \\ POP_ASSUM (K ALL_TAC) 2204 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `IO_INPUT_APPLY (SND o next_token) io`) 2205 \\ ASM_SIMP_TAC std_ss [LET_DEF,zLISP_R_def] 2206 \\ ASM_SIMP_TAC (std_ss++sep_cond_ss) [SEP_IMP_def,SEP_EXISTS_THM,SEP_CLAUSES,cond_STAR] 2207 \\ REPEAT STRIP_TAC \\ Q.LIST_EXISTS_TAC [`io2`,`ok1`,`zX`,`z0`,`z1`] 2208 \\ ASM_SIMP_TAC std_ss [] 2209 \\ AUTO_EXISTS_TAC \\ ASM_SIMP_TAC std_ss [] 2210 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 2211 \\ METIS_TAC [lisp_inv_ignore_io]) 2212 val th = MP th lemma 2213 val th = foldr (uncurry Q.GEN) th [`tw0`,`tw1`,`tw2`,`wsp`,`bp`,`sp`,`w0`,`w1`,`w2`,`w3`,`w4`,`w5`,`wi`,`we`,`df`,`f`,`dg`,`g`,`bp2`,`ds`,`sa1`,`sa2`,`sa3`,`dd`,`d`] 2214 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 2215 val pre = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2216 val (th,goal) = SPEC_STRENGTHEN_RULE th pre 2217 val lemma2 = prove( 2218 ``mc_next_token_pre (sp,we,io,dg,g,df,f) /\ ^LISP = ^LISP``, 2219 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 2220 \\ IMP_RES_TAC mc_next_token_thm \\ ASM_SIMP_TAC std_ss [LET_DEF]) 2221 val lemma = prove(goal, 2222 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_R_def,SEP_CLAUSES] 2223 \\ SIMP_TAC (std_ss++star_ss) [] \\ SIMP_TAC std_ss [STAR_ASSOC] 2224 \\ ASM_SIMP_TAC std_ss [SEP_IMP_REFL,lemma2] 2225 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] 2226 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [cond_STAR] 2227 \\ AUTO_EXISTS_TAC \\ ASM_SIMP_TAC std_ss [] 2228 \\ FULL_SIMP_TAC std_ss [SEP_HIDE_def,SEP_CLAUSES,SEP_EXISTS_THM] 2229 \\ Q.LIST_EXISTS_TAC [`x`,`tw0`,`w2w w3`,`w2w w1`,`w2w w0`,`w2w w2`] 2230 \\ FULL_SIMP_TAC (std_ss++star_ss) []) 2231 val th = MP th lemma 2232 val th = SPEC_COMPOSE_RULE [X64_LISP_R_INTRO,th] 2233 val (_,_,_,q) = dest_spec (concl th) 2234 val lemma = prove( 2235 (subst [mk_var("qq",type_of q)|->q] o set_pc th) 2236 ``SEP_IMP qq (zLISP_R ^STAT 2237 (next_token1 (getINPUT io),next_token2 (getINPUT io),Sym "NIL",Sym "NIL",x4,x5,xs,xs1,IO_INPUT_APPLY (SND o next_token) io,xbp,qs,code,amnt,ok) * 2238 zPC p * ~zS * cond ~(next_token2 (getINPUT io) = Sym "NIL") \/ 2239 SEP_EXISTS z0 io. 2240 zLISP_R ^STAT 2241 (z0,Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS)``, 2242 SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM,SEP_DISJ_def,cond_STAR] 2243 \\ REPEAT STRIP_TAC \\ REVERSE (Cases_on `ok1`) 2244 THEN1 (DISJ2_TAC \\ FULL_SIMP_TAC (std_ss++star_ss) [] \\ METIS_TAC []) 2245 \\ FULL_SIMP_TAC std_ss [next_token2_def,next_token1_def] 2246 \\ Cases_on `z1 = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [] 2247 \\ METIS_TAC []) 2248 val part1 = MATCH_MP (MATCH_MP SPEC_WEAKEN th) lemma 2249 (* part 2 *) 2250 val code = 2251 (assemble "x64" ` 2252 cmp r9,3 2253 jne SKIP 2254 mov [r7-112],r1 2255 mov r1d,1 2256 mov r2,r1 2257 mov r2,r8 2258 shr r2,2 2259 jmp [r7-200] 2260 SKIP: `); 2261 val (spec,_,sts,_) = x64_tools 2262 val ((th1,_,_),_) = spec (el 1 code) 2263 val ((th2a,_,_),th2c) = spec (el 2 code) 2264 fun the (SOME x) = x | the _ = fail(); 2265 val (th2b,_,_) = the th2c 2266 val ((th3,_,_),_) = spec (el 6 code) 2267 val ((th4,_,_),_) = spec (el 7 code) 2268 (* path A *) 2269 val thA = SPEC_COMPOSE_RULE [th1,th2a] 2270 val thA = HIDE_STATUS_RULE true sts thA 2271 val imp = prove( 2272 ``^LISP ==> ~(x1 = Sym "NIL") ==> ~(w2w w1 = 3w:word64) /\ ^LISP``, 2273 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] THEN1 2274 (IMP_RES_TAC lisp_inv_swap1 \\ IMP_RES_TAC (hd (CONJUNCTS lisp_inv_Sym)) 2275 \\ FULL_SIMP_TAC std_ss []) 2276 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ METIS_TAC []) |> SIMP_RULE std_ss [LET_DEF] 2277 val th = RW [precond_def] (Q.INST [`r8`|->`w2w (v:word32)`,`r9`|->`w2w (w:word32)`,`rip`|->`p`] thA) 2278 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2279 val post_tm = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2280 val def = zLISP_R_def 2281 val thA = prove_spec th imp def pre_tm post_tm 2282 (* path B *) 2283 val thB = SPEC_COMPOSE_RULE [th1,th2b] 2284 val thB = HIDE_STATUS_RULE true sts thB 2285 val imp = prove( 2286 ``^LISP ==> (x1 = Sym "NIL") ==> (w2w w1 = 3w:word64) /\ ^LISP``, 2287 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] THEN1 2288 (IMP_RES_TAC lisp_inv_swap1 \\ IMP_RES_TAC (hd (CONJUNCTS lisp_inv_Sym)) 2289 \\ FULL_SIMP_TAC std_ss []) 2290 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ METIS_TAC []) |> SIMP_RULE std_ss [LET_DEF] 2291 val th = RW [precond_def] (Q.INST [`r8`|->`w2w (v:word32)`,`r9`|->`w2w (w:word32)`,`rip`|->`p`] thB) 2292 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2293 val post_tm = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2294 val def = zLISP_R_def 2295 val thB = prove_spec th imp def pre_tm post_tm 2296 val thB = SPEC_COMPOSE_RULE [thB,X64_LISP_R_ELIM] 2297 val th = SPEC_COMPOSE_RULE [th3,th4] 2298 val th = HIDE_STATUS_RULE true sts th 2299 val th = RW [precond_def] (Q.INST [`r8`|->`w2w (v:word32)`,`r9`|->`w2w (w:word32)`,`rip`|->`p`] th) 2300 val imp = prove( 2301 ``^LISP ==> let tw2 = w2w w0 >>> 2 in ^LISP``, 2302 SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2303 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ METIS_TAC []) |> SIMP_RULE std_ss [LET_DEF] 2304 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2305 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2306 val def = zLISP_def 2307 val th = prove_spec th imp def pre_tm post_tm 2308 val thB = SPEC_COMPOSE_RULE [thB,th,X64_LISP_ERROR] 2309 val thB = RW [SEP_CLAUSES] (Q.INST [`x1`|->`Sym "NIL"`,`x2`|->`Sym "NIL"`,`x3`|->`Sym "NIL"`,`x0`|->`z0`] thB) 2310 val thB = foldr (uncurry Q.GEN) thB [`z0`,`io`] 2311 val thB = SIMP_RULE std_ss [SPEC_PRE_EXISTS] thB 2312 (* path A \/ B *) 2313 val SPEC_BASIC_MERGE = RW [SEP_CLAUSES,GSYM AND_IMP_INTRO] 2314 (GEN_ALL (Q.SPECL [`x`,`p1`,`p2`,`c1`,`SEP_F`] SPEC_MERGE)) 2315 val th = remove_primes (MATCH_MP (MATCH_MP SPEC_BASIC_MERGE thA) thB) 2316 val set_lemma = prove( 2317 ``({} UNION s = s) /\ ((x INSERT s) UNION (x INSERT t) = x INSERT (s UNION t))``, 2318 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 2319 val part2 = RW [set_lemma] th 2320 (* part1 and part2 *) 2321 val imp = RW[GSYM AND_IMP_INTRO](RW1[CONJ_COMM]SPEC_COMPOSE) 2322 val th = MATCH_MP (MATCH_MP imp part2) part1 2323 val th = SIMP_RULE std_ss [INSERT_UNION_EQ,UNION_EMPTY,word_arith_lemma1] th 2324 val th = SPEC_COMPOSE_RULE [th,X64_LISP_R_ELIM] 2325 in th end); 2326 2327 2328(* xbp related ops *) 2329 2330val X64_LISP_XBP_SET = let 2331 val th = mc_xbp_set_spec 2332 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_set_thm 2333 val def = zLISP_def 2334 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2335 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,LENGTH xs,qs,code,amnt,ok) * zPC p`` 2336 val res = prove_spec th imp def pre_tm post_tm 2337 in save_lisp_thm("X64_LISP_XBP_SET",res) end; 2338 2339val X64_LISP_XBP_LOAD = let 2340 val th = mc_xbp_load_spec 2341 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_load_thm 2342 val def = zLISP_def 2343 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2344 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,EL (LENGTH xs + getVal x1 - xbp) xs,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2345 val res = prove_spec th imp def pre_tm post_tm 2346 in save_lisp_thm("X64_LISP_XBP_LOAD",res) end; 2347 2348val X64_LISP_XBP_STORE = let 2349 val th = mc_xbp_store_spec 2350 val imp = SIMP_RULE std_ss [LET_DEF] mc_xbp_store_thm 2351 val def = zLISP_def 2352 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2353 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,UPDATE_NTH (LENGTH xs + getVal x1 - xbp) x0 xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2354 val res = prove_spec th imp def pre_tm post_tm 2355 in save_lisp_thm("X64_LISP_XBP_STORE",res) end; 2356 2357 2358(* load const amnt *) 2359 2360val X64_LISP_LOAD_AMNT = let 2361 val th = mc_load_amnt_spec 2362 val imp = SIMP_RULE std_ss [LET_DEF] mc_load_amnt_thm 2363 val def = zLISP_def 2364 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2365 val post_tm = set_pc th ``zLISP ^STAT (x0,Val amnt,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2366 val res = prove_spec th imp def pre_tm post_tm 2367 in save_lisp_thm("X64_LISP_LOAD_AMNT",res) end; 2368 2369 2370(* pops by a var *) 2371 2372val X64_LISP_POPS_BY_VAR = let 2373 val th = mc_pops_by_var_spec 2374 val imp = SIMP_RULE std_ss [LET_DEF] mc_pops_by_var_thm 2375 val def = zLISP_def 2376 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2377 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,DROP (getVal x1) xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2378 val res = prove_spec th imp def pre_tm post_tm 2379 in save_lisp_thm("X64_LISP_POPS_BY_VAR",res) end; 2380 2381 2382(* read SND code *) 2383 2384val X64_LISP_READ_SND_CODE = let 2385 val th = mc_read_snd_code_spec 2386 val imp = mc_read_snd_code_thm 2387 val def = zLISP_def 2388 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2389 val post_tm = set_pc th ``zLISP ^STAT (Val (code_ptr code),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2390 val res = prove_spec th imp def pre_tm post_tm 2391 in save_lisp_thm("X64_LISP_READ_SND_CODE",res) end; 2392 2393 2394(* const load *) 2395 2396val X64_LISP_CONST_LOAD = let 2397 val th = mc_const_load_spec 2398 val imp = mc_const_load_thm 2399 val def = zLISP_def 2400 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2401 val post_tm = set_pc th ``zLISP ^STAT (EL (getVal x0) xs1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2402 val res = prove_spec th imp def pre_tm post_tm 2403 in save_lisp_thm("X64_LISP_CONST_LOAD",res) end; 2404 2405 2406(* const store *) 2407 2408val imp4x = prove( 2409 ``^LISP ==> (sp - 0x6Cw && 0x3w = 0x0w) /\ (sp - 0x70w && 0x3w = 0x0w) /\ 2410 (sp - 0x64w && 0x3w = 0x0w) /\ (sp - 0x68w && 0x3w = 0x0w) /\ 2411 (sp - 0x5Cw && 0x3w = 0x0w) /\ (sp - 0x60w && 0x3w = 0x0w) /\ 2412 (sp - 0x54w && 0x3w = 0x0w) /\ (sp - 0x58w && 0x3w = 0x0w) /\ 2413 (sp - 0x4Cw && 0x3w = 0x0w) /\ (sp - 0x50w && 0x3w = 0x0w) /\ 2414 (sp - 0x44w && 0x3w = 0x0w) /\ (sp - 0x48w && 0x3w = 0x0w) /\ 2415 (sp - 0x3Cw && 0x3w = 0x0w) /\ (sp - 0x40w && 0x3w = 0x0w) /\ 2416 (sp - 0x34w && 0x3w = 0x0w) /\ (sp - 0x38w && 0x3w = 0x0w) /\ 2417 (sp - 0x2Cw && 0x3w = 0x0w) /\ (sp - 0x30w && 0x3w = 0x0w) /\ 2418 (sp - 0x24w && 0x3w = 0x0w) /\ (sp - 0x28w && 0x3w = 0x0w)``, 2419 SIMP_TAC std_ss [lisp_inv_def] \\ STRIP_TAC 2420 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3]) |> UNDISCH 2421 2422fun X64_LISP_LOAD_EL i = let 2423 val addr = "mov r2,[r7-" ^ int_to_string (112 - 8 * i) ^ "]" 2424 val ((th,_,_),_) = x64_spec (x64_encodeLib.x64_encode addr) 2425 val th = Q.INST [`rip`|->`p`] th 2426 val th = RW [INSERT_SUBSET,EMPTY_SUBSET] th 2427 val tm = subst [``i:num``|->numSyntax.term_of_int i] ``(EL i ds):word64`` 2428 val imp0 = UNDISCH (INST [``temp:word64``|->tm] lisp_inv_ignore_tw2) 2429 val imp1 = el (3*i+1) (CONJUNCTS (UNDISCH lisp_inv_ds_read)) 2430 val imp2 = el (3*i+2) (CONJUNCTS (UNDISCH lisp_inv_ds_read)) 2431 val imp3 = el (3*i+3) (CONJUNCTS (UNDISCH lisp_inv_ds_read)) 2432 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4x]) 2433 val def = zLISP_ALT_def 2434 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2435 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2436 val res = prove_spec th imp def pre_tm post_tm 2437 in res end; 2438 2439val const_store_test_lemma = prove( 2440 ``SPEC X64_MODEL 2441 (zLISP_ALT b1 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c1 q1 ==> 2442 SPEC X64_MODEL 2443 (zLISP_ALT b2 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c2 q2 ==> 2444 SPEC X64_MODEL 2445 (zLISP_ALT (\wsp wi we ds tw2. b1 wsp wi we ds tw2 \/ b2 wsp wi we ds tw2) 2446 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) (c1 UNION c2) (q1 \/ q2)``, 2447 SIMP_TAC (std_ss++sep_cond_ss) [zLISP_def,SEP_CLAUSES,GSYM SPEC_PRE_EXISTS, 2448 SPEC_MOVE_COND,zLISP_ALT_def] \\ METIS_TAC [SPEC_MERGE_LEMMA]); 2449 2450val X64_LISP_TEST_R2_EQ_ZERO = let 2451 val branch_taken_prefix = "3E" 2452 val x1 = x64_encodeLib.x64_encode "test r2,r2" 2453 val x2 = branch_taken_prefix ^ (x64_encodeLib.x64_encode "jne 12") 2454 val x3 = x64_encodeLib.x64_encode "mov r2d,12" 2455 val x4 = x64_encodeLib.x64_encode "jmp [r7-200]" 2456 val (spec,_,sts,_) = x64_tools 2457 val ((th1,_,_),_) = spec x1 2458 val ((th2,_,_),th2a) = spec x2 2459 val ((th3,_,_),_) = spec x3 2460 fun the (SOME x) = x | the _ = fail(); 2461 val (th2b,_,_) = the th2a 2462 val th = SPEC_COMPOSE_RULE [th1,th2b,th3] 2463 val th = HIDE_STATUS_RULE true sts th 2464 val th = RW [precond_def] th 2465 val def = zLISP_ALT_def 2466 val imp = Q.INST [`temp`|->`12w`] lisp_inv_ignore_tw2 2467 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 2468 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 2469 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ((tw2 = EL 7 ds) /\ (tw2 = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2470 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2471 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2472 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 2473 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 2474 val post1_tm = subst [``rip:word64`` |-> cdr tm] post1_tm 2475 val result2 = prove_spec th imp def pre_tm post_tm 2476 val res2 = RW [GSYM zLISP_raw] result2 2477 val res2 = SPEC_COMPOSE_RULE [res2,X64_LISP_ERROR] 2478 val th = SPEC_COMPOSE_RULE [th1,th2] 2479 val th = HIDE_STATUS_RULE true sts th 2480 val th = RW [precond_def] th 2481 val def = zLISP_ALT_def 2482 val imp = lisp_inv_swap0 2483 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 2484 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 2485 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ((tw2 = EL 7 ds) /\ ~(tw2 = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2486 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (~(EL 7 ds = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2487 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 2488 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 2489 val res1 = prove_spec th imp def pre_tm post_tm 2490 val th = MATCH_MP const_store_test_lemma (RW [GSYM STAR_ASSOC] res1) 2491 val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2) 2492 val set_lemma = prove( 2493 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``, 2494 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 2495 val th = RW [STAR_ASSOC,set_lemma] th 2496 val lemma = prove(``(\wsp wi we ds tw2. 2497 (tw2 = EL 7 ds) /\ tw2 <> 0x0w \/ 2498 (tw2 = EL 7 ds) /\ (tw2 = 0x0w)) = 2499 (\wsp wi we ds tw2. (tw2 = EL 7 ds))``, METIS_TAC []) 2500 val th = SIMP_RULE std_ss [markerTheory.Abbrev_def,lemma] th 2501 in th end; 2502 2503val X64_LISP_CONST_STORE = let 2504 val th = mc_const_store_spec 2505 val imp = mc_const_store_thm 2506 val def = zLISP_ALT_def 2507 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. ~(EL 7 ds = 0x0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2508 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (Val (LENGTH xs1),x1,x2,x3,x4,x5,xs,xs1 ++ [x0],io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2509 val res = prove_spec th imp def pre_tm post_tm 2510 val res = RW [GSYM zLISP_raw] res 2511 val th1 = X64_LISP_LOAD_EL 7 |> RW [GSYM zLISP_raw] 2512 val th2 = X64_LISP_TEST_R2_EQ_ZERO 2513 val th3 = res 2514 val res = SPEC_COMPOSE_RULE [th1,th2,th3] 2515 in save_lisp_thm("X64_LISP_CONST_STORE",res) end; 2516 2517 2518(* check for space in code heap *) 2519 2520val X64_LISP_CODE_TEST = let 2521 val stack_test_code = 2522 (codegenLib.assemble "x64" ` 2523 cmp QWORD [r7-88],256 2524 mov r2d,3 2525 ja L 2526 jmp [r7-200] 2527 L: `) 2528 val (spec,_,sts,_) = x64_tools 2529 val ((th1,_,_),_) = spec (el 1 stack_test_code) 2530 val ((th2,_,_),_) = spec (el 2 stack_test_code) 2531 val ((th3,_,_),th3a) = spec (el 3 stack_test_code) 2532 fun the (SOME x) = x | the _ = fail(); 2533 val (th3b,_,_) = the th3a 2534 val th = SPEC_COMPOSE_RULE [th1,th2,th3b] 2535 val th = HIDE_STATUS_RULE true sts th 2536 val th = RW [precond_def] th 2537 val def = zLISP_ALT_def 2538 val imp = mc_code_heap_space_thm 2539 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 2540 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 2541 val th = RW [GSYM WORD_LOWER_OR_EQ] th 2542 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2543 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2544 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2545 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 2546 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 2547 val post1_tm = subst [``rip:word64`` |-> cdr tm] post1_tm 2548 val result2 = prove_spec th imp def pre_tm post_tm 2549 val (th,goal) = SPEC_WEAKEN_RULE result2 post1_tm 2550 val lemma = prove(goal,SIMP_TAC std_ss [GSYM STAR_ASSOC,SEP_IMP_zLISP_ALT_zLISP]) 2551 val res2 = SPEC_COMPOSE_RULE [MP th lemma,X64_LISP_ERROR] 2552 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 2553 val th = HIDE_STATUS_RULE true sts th 2554 val lemma = GSYM (SIMP_CONV std_ss [WORD_LOWER_OR_EQ] ``~(x <=+ y:'a word)``) 2555 val th = RW [precond_def,lemma] th 2556 val def = zLISP_ALT_def 2557 val imp = mc_code_heap_space_thm 2558 val lemma = METIS_PROVE [] ``cond b = cond (Abbrev b)`` 2559 val th = RW1 [lemma] (SIMP_RULE (std_ss++sep_cond_ss) [] th) 2560 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2561 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2562 val tm = find_term (can (match_term ``zPC (p + n2w n)``)) (concl th) 2563 val post_tm = subst [``rip:word64`` |-> cdr tm] post_tm 2564 val res1 = prove_spec th imp def pre_tm post_tm 2565 val th = MATCH_MP push_lemma (RW [GSYM STAR_ASSOC] res1) 2566 val th = MATCH_MP th (RW [GSYM STAR_ASSOC] res2) 2567 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [markerTheory.Abbrev_def])) th 2568 val set_lemma = prove( 2569 ``{x1;x2;x3} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``, 2570 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 2571 val th = RW [STAR_ASSOC,set_lemma] th 2572 val th = RW [WORD_NOT_LOWER_EQUAL] th 2573 in th end; 2574 2575 2576(* code heap - write *) 2577 2578val code_write_counter = ref 0; 2579 2580fun X64_LISP_WRITE save (th,imp) = let 2581 val th = Q.INST [`dg`|->`dd`,`g`|->`d`] th 2582 val imp = SIMP_RULE std_ss [LET_DEF] imp 2583 val s = [``ddd:bool option``|->``SOME F``,``cu:((bool[64] -> bool) # (bool[64] -> bool[8])) option``|->``NONE:((bool[64] -> bool) # (bool[64] -> bool[8])) option``] 2584 val NEWSTAT = subst s STAT 2585 val def = RW [zCODE_MEMORY_def,SEP_CLAUSES,zCODE_UNCHANGED_def] (INST s (SPEC_ALL zLISP_ALT_def)) 2586 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. 0x100w <+ EL 3 ds) ^NEWSTAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2587 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^NEWSTAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2588 val code = find_term (can (match_term LISP)) (imp |> concl |> cdr) 2589 val (s,_) = match_term LISP code 2590 val post_tm = subst s post_tm 2591 val res = prove_spec th imp def pre_tm post_tm 2592 val res = UNDISCH_ALL (RW [SPEC_MOVE_COND] res) 2593 val th2 = Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`] X64_LISP_CODE_TEST 2594 val th = MATCH_MP (MATCH_MP SPEC_DISJ_COMPOSE res) (RW [markerTheory.Abbrev_def] th2) 2595 val th = SIMP_RULE std_ss [INSERT_UNION_EQ,UNION_EMPTY,word_arith_lemma1] th 2596 val th = RW [GSYM zLISP_raw] th 2597 val th = RW [GSYM SPEC_MOVE_COND] (DISCH_ALL th) 2598 val name = "X64_LISP_WRITE_" ^ int_to_string (!code_write_counter) 2599 val _ = (code_write_counter := !code_write_counter+1) 2600 val _ = if save then save_lisp_thm(name,th) else th 2601 in th end; 2602 2603val (X64_LISP_WRITE_THMS,iLOAD_LEMMA,iSTORE_LEMMA) = let 2604 val xs = CONJUNCTS lisp_inv_write_consts_thm 2605 fun fsts (x::y::xs) = x::fsts xs | fsts _ = [] 2606 fun snds (x::y::xs) = y::snds xs | snds _ = [] 2607 val xs = zip (fsts xs) (snds xs) 2608 fun is_iSTORE (x,y) = can (find_term (aconv ``iSTORE``)) (concl y) 2609 fun is_iLOAD (x,y) = can (find_term (aconv ``iLOAD``)) (concl y) 2610 val ys = filter (fn x => not (is_iSTORE x) andalso not (is_iLOAD x)) xs 2611 in (map (X64_LISP_WRITE true) ys, 2612 X64_LISP_WRITE false (first is_iLOAD xs), 2613 X64_LISP_WRITE false (first is_iSTORE xs)) end; 2614 2615val lisp_inv_load_test = prove( 2616 ``^LISP ==> 2617 isVal x0 /\ getVal x0 < 536870912 ==> 2618 (let tw2 = 0x80000001w in ^LISP) /\ 2619 w2w w0 <+ 0x80000001w:word64``, 2620 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [LET_DEF] 2621 THEN1 (MATCH_MP_TAC lisp_inv_ignore_tw2 \\ ASM_SIMP_TAC std_ss []) 2622 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2623 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,isVal_thm,EVERY_DEF,lisp_x_def] 2624 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,isVal_thm,EVERY_DEF,lisp_x_def] 2625 \\ Q.PAT_X_ASSUM `s0 = bbb` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt] 2626 \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 2627 \\ FULL_SIMP_TAC std_ss [getVal_def] 2628 \\ REPEAT STRIP_TAC 2629 \\ Q.PAT_X_ASSUM `w2w (n2w a) << 2 + 0x1w = w0` (ASSUME_TAC o GSYM) 2630 \\ FULL_SIMP_TAC std_ss [] 2631 \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_def,WORD_MUL_LSL,word_mul_n2w, 2632 word_add_n2w,word_lo_n2w,w2n_n2w] 2633 \\ `a < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2634 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2635 \\ `(4 * a + 1) < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2636 \\ DECIDE_TAC) |> SIMP_RULE std_ss [LET_DEF]; 2637 2638val lisp_inv_load_test_nop = prove( 2639 ``^LISP ==> 2640 isVal x0 /\ ~(getVal x0 < 536870912) ==> 2641 (let tw2 = 0x80000001w in ^LISP) /\ 2642 ~(w2w w0 <+ 0x80000001w:word64)``, 2643 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [LET_DEF] 2644 THEN1 (MATCH_MP_TAC lisp_inv_ignore_tw2 \\ ASM_SIMP_TAC std_ss []) 2645 \\ POP_ASSUM MP_TAC 2646 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 2647 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,isVal_thm,EVERY_DEF,lisp_x_def] 2648 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,isVal_thm,EVERY_DEF,lisp_x_def] 2649 \\ Q.PAT_X_ASSUM `s0 = bbb` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt] 2650 \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 2651 \\ FULL_SIMP_TAC std_ss [getVal_def] 2652 \\ REPEAT STRIP_TAC 2653 \\ POP_ASSUM MP_TAC 2654 \\ Q.PAT_X_ASSUM `w2w (n2w a) << 2 + 0x1w = w0` (ASSUME_TAC o GSYM) 2655 \\ FULL_SIMP_TAC std_ss [] 2656 \\ SIMP_TAC (std_ss++SIZES_ss) [w2w_def,WORD_MUL_LSL,word_mul_n2w, 2657 word_add_n2w,word_lo_n2w,w2n_n2w] 2658 \\ `a < 1073741824` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2659 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2660 \\ `(4 * a + 1) < 18446744073709551616` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss [] 2661 \\ DECIDE_TAC) |> SIMP_RULE std_ss [LET_DEF]; 2662 2663val SPEC_MERGE_LEMMA2 = prove( 2664 ``SPEC m (p * cond g * cond b) c1 q1 ==> 2665 SPEC m (p * cond g * cond ~b) c2 q2 ==> 2666 SPEC m (p * cond g) (c1 UNION c2) (q1 * cond g * cond b \/ q2)``, 2667 Cases_on `b` \\ Cases_on `g` \\ SIMP_TAC std_ss [SEP_CLAUSES,SPEC_FALSE_PRE] 2668 \\ METIS_TAC [SPEC_ADD_CODE,SEP_IMP_LEMMA,SPEC_WEAKEN,UNION_COMM]); 2669 2670val X64_LISP_LOAD_TEST = let 2671 val add_code = 2672 (codegenLib.assemble "x64" ` 2673 mov r2,2147483649 2674 cmp r8d,r2d 2675 jb L 2676 jmp [r7-200] 2677 L: `) 2678 val (spec,_,sts,_) = x64_tools 2679 val ((th1,_,_),_) = spec (el 1 add_code) 2680 val ((th2,_,_),_) = spec (el 2 add_code) 2681 val ((th3,_,_),th3a) = spec (el 3 add_code) 2682 fun the (SOME x) = x | the _ = fail(); 2683 val (th3b,_,_) = the th3a 2684 val th = SPEC_COMPOSE_RULE [th1,th2,th3] 2685 val th = HIDE_STATUS_RULE true sts th 2686 val th = Q.INST [`r8`|->`w2w (a:word32)`] th 2687 val th = RW [select_twice,EVAL ``(31 -- 0) 0x80000001w:word64``] th 2688 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,GSYM NOT_LESS,precond_def] th 2689 val imp = lisp_inv_load_test 2690 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2691 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2692 val def = zLISP_def 2693 val res1 = prove_spec th imp def pre_tm post_tm 2694 val th = SPEC_COMPOSE_RULE [th1,th2,th3b] 2695 val th = HIDE_STATUS_RULE true sts th 2696 val th = Q.INST [`r8`|->`w2w (a:word32)`] th 2697 val th = RW [select_twice,EVAL ``(31 -- 0) 0x80000001w:word64``] th 2698 val th = SIMP_RULE (std_ss++SIZES_ss) [w2n_w2w,precond_def] th 2699 val imp = lisp_inv_load_test_nop 2700 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS`` 2701 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2702 val res = prove_spec th imp def pre_tm post_tm 2703 val res2 = SPEC_COMPOSE_RULE [res,X64_LISP_ERROR] 2704 val lemma = prove(``cond b * cond c = cond (b /\ c)``,SIMP_TAC std_ss [SEP_CLAUSES]) 2705 val res1 = RW [GSYM lemma, STAR_ASSOC] res1 2706 val res2 = RW [GSYM lemma, STAR_ASSOC] res2 2707 val set_lemma = prove( 2708 ``{x1;x2;x3} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``, 2709 SIMP_TAC std_ss [EXTENSION,IN_UNION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC []) 2710 val res = MATCH_MP (MATCH_MP SPEC_MERGE_LEMMA2 res1) res2 2711 val res = RW [STAR_ASSOC] (RW [set_lemma,lemma,GSYM STAR_ASSOC] res) 2712 in res end; 2713 2714val X64_LISP_WRITE_iLOAD = save_lisp_thm("X64_LISP_WRITE_iLOAD", 2715 SPEC_COMPOSE_RULE [Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`] X64_LISP_LOAD_TEST,iLOAD_LEMMA]); 2716 2717val X64_LISP_WRITE_iSTORE = save_lisp_thm("X64_LISP_WRITE_iSTORE", 2718 SPEC_COMPOSE_RULE [Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`] X64_LISP_LOAD_TEST,iSTORE_LEMMA]); 2719 2720 2721(* call generated code *) 2722 2723val X64_LISP_JUMP_R2 = let 2724 val s = x64_encode "jmp r2" 2725 val (spec,_,sts,_) = x64_tools 2726 val ((th,_,_),_) = spec s 2727 val th = Q.INST [`rip`|->`p`] th 2728 val imp = lisp_inv_swap0 2729 val def = zLISP_ALT_def 2730 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2731 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC r2`` 2732 val res = prove_spec th imp def pre_tm post_tm 2733 val res = RW [GSYM zLISP_raw] res 2734 in res end; 2735 2736val X64_LISP_JUMP_TO_EL4CS_R2 = let 2737 val th = mc_calc_addr_spec 2738 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm 2739 val def = zLISP_ALT_def 2740 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2741 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2742 val res = prove_spec th imp def pre_tm post_tm 2743 val res = RW [GSYM zLISP_raw] res 2744 val res = SPEC_COMPOSE_RULE [res,Q.INST [`r2`|->`EL 4 cs + n2w (getVal x2)`] X64_LISP_JUMP_R2] 2745 in res end; 2746 2747fun X64_LISP_PUSH_EL i = let 2748 val addr = "mov r2,[r7-" ^ int_to_string (192 - 8 * i) ^ "]" 2749 val ((th,_,_),_) = x64_spec (x64_encodeLib.x64_encode addr) 2750 val th = Q.INST [`rip`|->`p`] th 2751 val th = RW [INSERT_SUBSET,EMPTY_SUBSET] th 2752 val tm = subst [``i:num``|->numSyntax.term_of_int i] ``(EL i cs):word64`` 2753 val imp0 = UNDISCH (INST [``temp:word64``|->tm] lisp_inv_ignore_tw2) 2754 val imp1 = el (3*i+10+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 2755 val imp2 = el (3*i+11+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 2756 val imp3 = el (3*i+12+3) (CONJUNCTS (UNDISCH lisp_inv_cs_read)) 2757 val imp = DISCH_ALL (LIST_CONJ [imp0,imp1,imp2,imp3,imp4]) 2758 val def = zLISP_ALT_def 2759 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2760 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 2761 val res = prove_spec th imp def pre_tm post_tm 2762 val res = SPEC_COMPOSE_RULE [res,Q.INST [`r2`|->`^tm`] X64_LISP_PUSH_R2] 2763 val res = RW [GSYM zLISP_raw] res 2764 in res end; 2765 2766val pattern = ``(p1,xs1,b1) INSERT (p2:word64,xs2:word8 list,b2:bool) INSERT s`` 2767fun sort_swap_conv tm = let 2768 val m = fst (match_term pattern tm) 2769 val p1 = subst m (mk_var("p1",``:word64``)) 2770 val p2 = subst m (mk_var("p2",``:word64``)) 2771 fun foo tm = if is_var tm then 0 else tm |> cdr |> cdr |> numSyntax.int_of_term 2772 val _ = foo p2 < foo p1 orelse fail() 2773 val (x1,s1) = pred_setSyntax.dest_insert tm 2774 val (x2,s2) = pred_setSyntax.dest_insert s1 2775 in ISPECL [x1,x2,s2] INSERT_COMM end 2776 2777fun SORT_CODE th = CONV_RULE (REDEPTH_CONV sort_swap_conv) th 2778 2779val X64_LISP_JUMP_TO_CODE_FOR_EVAL = save_thm("X64_LISP_JUMP_TO_CODE_FOR_EVAL",let 2780 val i = 4 2781 val addr = "mov r2,[r7-" ^ int_to_string (192 - 8 * i) ^ "]" 2782 val code = assemble "x64" ` 2783 jmp L 2784G: mov r2,[r7-160] 2785 push r2 2786 mov r2,r10 2787 shr r2,2 2788 add r2,[r7-160] 2789 jmp r2 2790L: jmp G` 2791 val s = hd code 2792 val (spec,_,sts,_) = x64_tools 2793 val ((th,_,_),_) = spec s 2794 val th0 = Q.INST [`rip`|->`p`] th 2795 val th1 = X64_LISP_PUSH_EL 4 2796 val th2 = X64_LISP_JUMP_TO_EL4CS_R2 2797 val call = Q.INST [`imm32`|->`0w - 0x20w`] X64_LISP_CALL_IMM 2798 |> SIMP_RULE (std_ss++SIZES_ss) [word_arith_lemma2,word_2comp_n2w] 2799 val tm = find_term (can (match_term ``n2w (m + n)``)) (concl call) 2800 val call_thm = RW [EVAL tm] call 2801 val res = SPEC_COMPOSE_RULE [th0,call_thm,th1,th2] 2802 val (_,_,c,_) = dest_spec (concl res) 2803 val f = EVAL 2804 THENC ONCE_REWRITE_CONV [GSYM n2w_mod] 2805 THENC SIMP_CONV (std_ss++SIZES_ss) [] 2806 val res = SORT_CODE (RW [f c] res) 2807 in res end); 2808 2809val X64_LISP_JUMP_TO_CODE_NO_RET = let 2810 val th = mc_calc_addr_spec 2811 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm 2812 val def = zLISP_ALT_def 2813 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2814 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2815 val res = prove_spec th imp def pre_tm post_tm 2816 val res = RW [GSYM zLISP_raw] res 2817 val res = SPEC_COMPOSE_RULE [res,Q.INST [`r2`|->`EL 4 cs + n2w (getVal x2)`] X64_LISP_JUMP_R2] 2818 in save_thm("X64_LISP_JUMP_TO_CODE_NO_RET",res) end; 2819 2820val X64_LISP_JUMP_TO_CODE = let 2821 val th = mc_calc_addr_spec 2822 val imp = SIMP_RULE std_ss [LET_DEF] mc_calc_addr_thm 2823 val def = zLISP_ALT_def 2824 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2825 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2826 val res = prove_spec th imp def pre_tm post_tm 2827 val res = RW [GSYM zLISP_raw] res 2828 val res = SPEC_COMPOSE_RULE [res,Q.INST [`r2`|->`EL 4 cs + n2w (getVal x2)`] X64_LISP_CALL_R2] 2829 in save_thm("X64_LISP_JUMP_TO_CODE",res) end; 2830 2831 2832(* converting code into data *) 2833 2834val PULL_FORALL_IMP = METIS_PROVE [] ``(Q ==> !x. P x) = (!x. Q ==> P x)``; 2835 2836val zBYTE_MEMORY_Z_thm = prove( 2837 ``zBYTE_MEMORY dd d = zBYTE_MEMORY_Z dd d``, 2838 SIMP_TAC std_ss [zBYTE_MEMORY_Z_def,zBYTE_MEMORY_def]); 2839 2840val X64_LISP_WEAKEN_CODE = store_thm("X64_LISP_WEAKEN_CODE", 2841 ``SPEC X64_MODEL 2842 (zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)) {} 2843 (zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME F,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok))``, 2844 SIMP_TAC std_ss [zLISP_def] 2845 \\ REPEAT (HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS \\ REPEAT STRIP_TAC) 2846 \\ REPEAT (MATCH_MP_TAC (SIMP_RULE std_ss [PULL_FORALL_IMP] SPEC_FRAME)) 2847 \\ REPEAT (MATCH_MP_TAC (RW1 [STAR_COMM] (SIMP_RULE std_ss [PULL_FORALL_IMP] SPEC_FRAME))) 2848 \\ MATCH_MP_TAC (MATCH_MP SPEC_WEAKEN (SPEC_ALL SPEC_REFL)) 2849 \\ SIMP_TAC std_ss [zCODE_MEMORY_def,zCODE_IMP_BYTE_MEMORY,zBYTE_MEMORY_Z_thm]); 2850 2851 2852(* converting data into code *) 2853 2854val X64_LISP_STRENGTHEN_CODE = save_thm("X64_LISP_STRENGTHEN_CODE",let 2855 val ((th0,_,_),_) = x64_spec (x64_encode "mov r15, r3") 2856 val ((th1,_,_),_) = x64_spec (x64_encode "xor rax, rax") 2857 val th4 = RW [GSYM zR_def] (Q.INST [`rip`|->`p`,`df`|->`dd`,`f`|->`d`] X64_SPEC_CPUID) 2858 val ((th5,_,_),_) = x64_spec (x64_encode "mov r3, r15") 2859 val ((th6,_,_),_) = x64_spec (x64_encode "mov r15,[r7-240]") 2860 val ((th7,_,_),_) = x64_spec (x64_encode "add r15,r15") 2861 val ((th8,_,_),_) = x64_spec (x64_encode "mov r0d, 3") 2862 val ((th9,_,_),_) = x64_spec (x64_encode "mov r1d, 1") 2863 val th = SPEC_COMPOSE_RULE [th0,th1,th4,th5,th6,th7,th8,th9] 2864 val (spec,_,sts,_) = x64_tools 2865 val th = HIDE_STATUS_RULE true sts th 2866 val thi = RW [GSYM zCODE_MEMORY_def,GSYM zBYTE_MEMORY_Z_thm] th 2867 val PULL_EXISTS_CONJ = METIS_PROVE [] ``(?x. P x) /\ Q = ?x. P x /\ Q`` 2868 val lemma = prove( 2869 ``^LISP ==> 2870 (let we = ((w2w (f (sp - 0xECw)) << 32 !! w2w (f (sp - 0xF0w))) + 2871 (w2w (f (sp - 0xECw)) << 32 !! w2w (f (sp - 0xF0w)))) in 2872 let tw0 = 3w in let tw1 = 1w in let tw2 = ARB in ^LISP) /\ 2873 {sp - 0xECw; sp - 0xF0w} SUBSET df /\ (sp - 0xECw && 0x3w = 0x0w) /\ 2874 (sp - 0xF0w && 0x3w = 0x0w)``, 2875 SIMP_TAC std_ss [LET_DEF] \\ STRIP_TAC \\ IMP_RES_TAC lisp_inv_cs_read 2876 \\ ASM_SIMP_TAC std_ss [word_add_n2w,INSERT_SUBSET,EMPTY_SUBSET] 2877 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,PULL_EXISTS_CONJ] 2878 \\ Q.LIST_EXISTS_TAC (map (fn tm => [ANTIQUOTE tm]) 2879 (butlast (list_dest dest_exists (cdr (concl (SPEC_ALL lisp_inv_def)))))) 2880 \\ FULL_SIMP_TAC std_ss [DECIDE ``2*e = e+e:num``] 2881 \\ Q.PAT_X_ASSUM `sp && 3w = 0w` MP_TAC 2882 \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ blastLib.BBLAST_TAC) 2883 |> SIMP_RULE std_ss [LET_DEF]; 2884 val th = Q.INST [`rip`|->`p`] thi 2885 val imp = lemma 2886 val def = zLISP_def 2887 val pre_tm = ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME F,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2888 val post_tm = set_pc th ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 2889 val res = prove_spec th imp def pre_tm post_tm 2890 in res end); 2891 2892 2893 2894(* implementations of LISP_TEST *) 2895 2896val X64_LISP_TEST = let 2897 fun the NONE = hd [] | the (SOME x) = x 2898 val ((th1,_,_),_) = x64_spec (x64_encode "mov r2d,11") 2899 val ((th2,_,_),th2a) = x64_spec (x64_encode "cmove r8,r2") 2900 val ((th3,_,_),th3a) = x64_spec (x64_encode "cmovne r8d,r0d") 2901 val (th2a,_,_) = the th2a 2902 val (th3a,_,_) = the th3a 2903 val pass1 = SPEC_COMPOSE_RULE [th1,th2,th3a] 2904 val pass2 = SPEC_COMPOSE_RULE [th1,th2a,th3] 2905 val th1 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass1 2906 val th2 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass2 2907 val th1 = RW [SEP_CLAUSES] (Q.INST [`z_zf`|->`T`,`rip`|->`p`] th1) 2908 val th2 = RW [SEP_CLAUSES] (Q.INST [`z_zf`|->`F`,`rip`|->`p`] th2) 2909 (* case 1 *) 2910 val th = th1 2911 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) 2912 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 2913 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 2914 val def = zLISP_def 2915 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)`` 2916 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)`` 2917 val res1 = prove_spec th imp def pre_tm post_tm 2918 (* case 2 *) 2919 val th = th2 2920 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil 2921 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 2922 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 2923 val def = zLISP_def 2924 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)`` 2925 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)`` 2926 val res2 = prove_spec th imp def pre_tm post_tm 2927 (* combine *) 2928 val lemma = CONJ (GSYM (EVAL ``LISP_TEST F``)) (GSYM (EVAL ``LISP_TEST T``)) 2929 val res1 = RW [lemma] res1 2930 val res2 = RW [lemma] res2 2931 val goal = subst [``T``|->``sf:bool``] (concl res1) 2932 val res = prove(goal,Cases_on `sf` THEN SIMP_TAC std_ss [res1,res2]) 2933 in res end; 2934 2935val X64_LISP_NOT_TEST = let 2936 fun the NONE = hd [] | the (SOME x) = x 2937 val ((th1,_,_),_) = x64_spec (x64_encode "mov r2d,11") 2938 val ((th2,_,_),th2a) = x64_spec (x64_encode "cmovne r8,r2") 2939 val ((th3,_,_),th3a) = x64_spec (x64_encode "cmove r8d,r0d") 2940 val (th2a,_,_) = the th2a 2941 val (th3a,_,_) = the th3a 2942 val pass1 = SPEC_COMPOSE_RULE [th1,th2,th3a] 2943 val pass2 = SPEC_COMPOSE_RULE [th1,th2a,th3] 2944 val th1 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass1 2945 val th2 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass2 2946 val th1 = RW [SEP_CLAUSES] (Q.INST [`z_zf`|->`F`,`rip`|->`p`] th1) 2947 val th2 = RW [SEP_CLAUSES] (Q.INST [`z_zf`|->`T`,`rip`|->`p`] th2) 2948 (* case 1 *) 2949 val th = th1 2950 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) 2951 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 2952 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 2953 val def = zLISP_def 2954 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)`` 2955 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)`` 2956 val res1 = prove_spec th imp def pre_tm post_tm 2957 (* case 2 *) 2958 val th = th2 2959 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil 2960 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 2961 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 2962 val def = zLISP_def 2963 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)`` 2964 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)`` 2965 val res2 = prove_spec th imp def pre_tm post_tm 2966 (* combine *) 2967 val lemma = CONJ (GSYM (EVAL ``LISP_TEST ~F``)) (GSYM (EVAL ``LISP_TEST ~T``)) 2968 val res1 = PURE_REWRITE_RULE [lemma] res1 2969 val res2 = PURE_REWRITE_RULE [lemma] res2 2970 val goal = subst [``T``|->``sf:bool``] (concl res2) 2971 val res = prove(goal,Cases_on `sf` 2972 THEN ASSUME_TAC res1 THEN ASSUME_TAC res2 2973 THEN FULL_SIMP_TAC std_ss [LISP_TEST_def]) 2974 in res end; 2975 2976val X64_LISP_TEST_CF = let 2977 fun the NONE = hd [] | the (SOME x) = x 2978 val ((th1,_,_),_) = x64_spec (x64_encode "mov r2d,11") 2979 val ((th2,_,_),th2a) = x64_spec (x64_encode "cmovb r8,r2") 2980 val ((th3,_,_),th3a) = x64_spec (x64_encode "cmovnb r8d,r0d") 2981 val (th2a,_,_) = the th2a 2982 val (th3a,_,_) = the th3a 2983 val pass1 = SPEC_COMPOSE_RULE [th1,th2,th3a] 2984 val pass2 = SPEC_COMPOSE_RULE [th1,th2a,th3] 2985 val th1 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass1 2986 val th2 = SIMP_RULE (std_ss++sep_cond_ss) [precond_def] pass2 2987 val th1 = RW [SEP_CLAUSES] (Q.INST [`z_cf`|->`T`,`rip`|->`p`] th1) 2988 val th2 = RW [SEP_CLAUSES] (Q.INST [`z_cf`|->`F`,`rip`|->`p`] th2) 2989 (* case 1 *) 2990 val th = th1 2991 val imp = SPEC_ALL (SIMP_RULE std_ss [LET_DEF] lisp_inv_T) 2992 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 2993 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 2994 val def = zLISP_def 2995 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME T)`` 2996 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME T)`` 2997 val res1 = prove_spec th imp def pre_tm post_tm 2998 (* case 2 *) 2999 val th = th2 3000 val imp = SIMP_RULE std_ss [LET_DEF] lisp_inv_nil 3001 val imp2 = Q.INST [`temp`|->`0xBw`] lisp_inv_ignore_tw2 3002 val imp = DISCH_ALL (MATCH_MP imp2 (UNDISCH imp)) 3003 val def = zLISP_def 3004 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME F)`` 3005 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME F)`` 3006 val res2 = prove_spec th imp def pre_tm post_tm 3007 (* combine *) 3008 val lemma = CONJ (GSYM (EVAL ``LISP_TEST F``)) (GSYM (EVAL ``LISP_TEST T``)) 3009 val res1 = RW [lemma] res1 3010 val res2 = RW [lemma] res2 3011 val goal = subst [``T``|->``cf:bool``] (concl res1) 3012 val res = prove(goal,Cases_on `cf` THEN SIMP_TAC std_ss [res1,res2]) 3013 in res end; 3014 3015 3016(* prove a few theorems which imply that the bytecode does the right thing *) 3017 3018val X64_POP0 = SPEC_COMPOSE_RULE [X64_LISP_TOP 0,X64_LISP_POP] 3019val X64_POP1 = SPEC_COMPOSE_RULE [X64_LISP_TOP 1,X64_LISP_POP] 3020 3021val X64_LISP_SWAP1 = let 3022 val ((th,_,_),_) = x64_spec (x64_encode "xchg r8,r9") 3023 val th = Q.INST [`rip`|->`p`] th 3024 val imp = lisp_inv_swap1 3025 val def = zLISP_def 3026 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 3027 val post_tm = set_pc th ``zLISP ^STAT (x1,x0,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p`` 3028 val res = prove_spec th imp def pre_tm post_tm 3029 in res end; 3030 3031val X64_LISP_SYMBOL_LESS = let 3032 val th = mc_symbol_less_spec 3033 val imp = mc_symbol_less_thm 3034 val def = zLISP_def 3035 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 3036 val post_tm = set_pc th ``zLISP ^STAT (LISP_SYMBOL_LESS x0 x1,Sym "NIL",Sym "NIL",Sym "NIL",x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS`` 3037 val res = prove_spec th imp def pre_tm post_tm 3038 in res end; 3039 3040fun BC_save name th = save_thm("X64_BYTECODE_" ^ name,th) 3041 3042val _ = BC_save "POP" X64_POP0 3043val X64_LISP_SAFE_CAR = BC_save "CAR" (fetch "-" "X64_LISP_SAFE_CAR00") 3044val X64_LISP_SAFE_CDR = BC_save "CDR" (fetch "-" "X64_LISP_SAFE_CDR00") 3045 3046val X64_CONSP = BC_save "CONSP" let 3047 val th = SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_ISDOT0",X64_LISP_TEST] 3048 val th = RW [GSYM LISP_CONSP_def] th 3049 val (spec,_,sts,_) = x64_tools 3050 val th = HIDE_STATUS_RULE true sts th 3051 in th end; 3052 3053val X64_NATP = BC_save "NATP" let 3054 val th = SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_ISVAL0",X64_LISP_TEST] 3055 val th = RW [GSYM LISP_NUMBERP_def] th 3056 val (spec,_,sts,_) = x64_tools 3057 val th = HIDE_STATUS_RULE true sts th 3058 in th end; 3059 3060val X64_SYMBOLP = BC_save "SYMBOLP" let 3061 val th = SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_ISSYM0",X64_LISP_TEST] 3062 val th = RW [GSYM LISP_SYMBOLP_def] th 3063 val (spec,_,sts,_) = x64_tools 3064 val th = HIDE_STATUS_RULE true sts th 3065 in th end; 3066 3067val X64_ATOMP = BC_save "ATOMP" let 3068 val th = SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_ISDOT0",X64_LISP_NOT_TEST] 3069 val th = RW [GSYM LISP_ATOMP_def] th 3070 val (spec,_,sts,_) = x64_tools 3071 val th = HIDE_STATUS_RULE true sts th 3072 in th end; 3073 3074val isVal_NFIX = prove(``!x. isVal (NFIX x) /\ (getVal (NFIX x) = getVal x)``, Cases \\ EVAL_TAC); 3075val isSym_SFIX = prove(``!x. isSym (SFIX x) /\ (getSym (SFIX x) = getSym x)``, Cases \\ EVAL_TAC); 3076 3077val X64_ADD = BC_save "ADD" let 3078 val th0 = X64_POP1 3079 val th1 = fetch "-" "X64_LISP_NFIX_0" 3080 val th2 = fetch "-" "X64_LISP_NFIX_1" 3081 val th3 = X64_LISP_ADD 3082 val th = SPEC_COMPOSE_RULE [th0,th1,th2,th3] 3083 val th = RW [isVal_NFIX,isSym_SFIX,SEP_CLAUSES,LISP_ADD_def] th 3084 val th = RW1 [ADD_COMM] th 3085 val th = RW [GSYM LISP_ADD_def] th 3086 in th end; 3087 3088val X64_SUB = BC_save "SUB" let 3089 val th0 = X64_LISP_SWAP1 3090 val th1 = X64_POP0 3091 val th2 = fetch "-" "X64_LISP_NFIX_0" 3092 val th3 = fetch "-" "X64_LISP_NFIX_1" 3093 val th4 = X64_LISP_SUB 3094 val th = SPEC_COMPOSE_RULE [th0,th1,th2,th3,th4] 3095 val th = RW [isVal_NFIX,isSym_SFIX,SEP_CLAUSES,LISP_SUB_def] th 3096 val th = RW [GSYM LISP_SUB_def] th 3097 in th end; 3098 3099val X64_SYMBOL_LESS = BC_save "SYMBOL_LESS" let 3100 val th0 = X64_LISP_SWAP1 3101 val th1 = X64_POP0 3102 val th2 = fetch "-" "X64_LISP_SFIX_0" 3103 val th3 = fetch "-" "X64_LISP_SFIX_1" 3104 val th4 = X64_LISP_SYMBOL_LESS 3105 val th = SPEC_COMPOSE_RULE [th0,th1,th2,th3,th4] 3106 val th = RW [isVal_NFIX,isSym_SFIX,SEP_CLAUSES,LISP_SYMBOL_LESS_def] th 3107 val th = RW [GSYM LISP_SYMBOL_LESS_def] th 3108 in th end; 3109 3110val X64_LESS = BC_save "LESS" let 3111 val th0 = X64_LISP_SWAP1 3112 val th1 = X64_POP0 3113 val th2 = fetch "-" "X64_LISP_NFIX_0" 3114 val th3 = fetch "-" "X64_LISP_NFIX_1" 3115 val th4 = X64_LISP_LESS 3116 val th5 = X64_LISP_TEST_CF 3117 val th = SPEC_COMPOSE_RULE [th0,th1,th2,th3,th4,th5] 3118 val th = RW [isVal_NFIX,isSym_SFIX,SEP_CLAUSES,LISP_LESS_def] th 3119 val th = RW [GSYM LISP_LESS_def] th 3120 in th end; 3121 3122val X64_CONS = BC_save "CONS" let 3123 val th0 = X64_LISP_SWAP1 3124 val th1 = X64_POP0 3125 val th2 = fetch "-" "X64_LISP_CONS_01" 3126 val th = SPEC_COMPOSE_RULE [th0,th1,th2] 3127 val th = RW [isVal_NFIX,isSym_SFIX,SEP_CLAUSES,GSYM LISP_CONS_def] th 3128 in th end; 3129 3130val X64_EQUAL = BC_save "EQUAL" let 3131 val th0 = X64_POP1 3132 val th1 = X64_LISP_EQUAL 3133 val th = SPEC_COMPOSE_RULE [th0,th1] 3134 in th end 3135 3136val X64_POPS = BC_save "POPS" X64_LISP_POPS 3137 3138val X64_LOAD = BC_save "LOAD" 3139 (SPEC_COMPOSE_RULE [fetch "-" "X64_LISP_PUSH_0",X64_LISP_LOAD]) 3140 3141val X64_STORE = BC_save "STORE" 3142 (SPEC_COMPOSE_RULE [X64_LISP_STORE,X64_POP0]) 3143 3144fun get_code th = let 3145 val (_,_,c,_) = dest_spec (concl th) 3146 fun dest_code_piece tm = let 3147 val (x,y) = pairSyntax.dest_pair tm 3148 val (y,z) = pairSyntax.dest_pair y 3149 val (v,n) = wordsSyntax.dest_word_add x handle HOL_ERR _ => (``n:num``,``(n2w 0):word64``) 3150 val _ = dest_var v 3151 val n = (numSyntax.int_of_term o cdr) n 3152 in (n,y) end 3153 val xs = map dest_code_piece (find_terms (can dest_code_piece) c) 3154 val xs = sort (fn (x,_) => fn (y,_) => x <= y) xs 3155 fun mk_appends [] = fail() 3156 | mk_appends [x] = snd x 3157 | mk_appends (x::xs) = listSyntax.mk_append(snd x,mk_appends xs) 3158 val cs = mk_appends xs |> QCONV (REWRITE_CONV [APPEND]) 3159 |> concl |> cdr 3160 in cs end; 3161 3162 3163val _ = print_compiler_grammar() 3164val _ = export_theory(); 3165