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