1open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_codegen"; 2val _ = ParseExtras.temp_loose_equality() 3open lisp_sexpTheory lisp_consTheory lisp_invTheory lisp_symbolsTheory; 4 5(* --- *) 6 7open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 8open combinTheory finite_mapTheory addressTheory helperLib; 9open set_sepTheory bitTheory fcpTheory stringTheory; 10 11val wstd_ss = std_ss ++ SIZES_ss ++ rewrites [DECIDE ``n<256 ==> (n:num)<18446744073709551616``,ORD_BOUND]; 12 13open stop_and_copyTheory; 14open codegenLib decompilerLib prog_x64Lib prog_x64Theory progTheory; 15open lisp_parseTheory; 16 17infix \\ 18val op \\ = op THEN; 19val RW = REWRITE_RULE; 20val RW1 = ONCE_REWRITE_RULE; 21fun SUBGOAL q = REVERSE (sg q) 22 23val _ = augment_srw_ss [rewrites [listTheory.DROP_def, listTheory.TAKE_def]] 24 25val align_blast = blastLib.BBLAST_PROVE 26 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 27 28val align_add_blast = blastLib.BBLAST_PROVE 29 ``(a && 3w = 0w) ==> ((a + w && 3w = 0w) = (w && 3w = 0w:word64))`` 30 31val FORALL_EXISTS = METIS_PROVE [] ``(!x. P x ==> Q) = ((?x. P x) ==> Q)`` 32val IMP_IMP = METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)`` 33 34val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst; 35val REST = LISP |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 36val STAT = LISP |> car |> car |> cdr; 37val VAR_REST = LISP |> car |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 38 39 40(* is_quote *) 41 42val (thm,mc_is_quote_def) = basic_decompile_strings x64_tools "mc_is_quote" 43 (SOME (``(r0:word64,r6:word64,df:word64 set,f:word64->word32)``, 44 ``(r1:word64,r6:word64,df:word64 set,f:word64->word32)``)) 45 (assemble "x64" ` 46 test r0,1 47 jne FALSE 48 mov r1d,[r6+4*r0] 49 mov r0d,[r6+4*r0+4] 50 cmp r1,19 51 jne FALSE 52 test r0,1 53 jne FALSE 54 mov r1d,[r6+4*r0+4] 55 cmp r1,3 56 jne FALSE 57TRUE: mov r1d,1 58 jmp EXIT 59FALSE: xor r1,r1 60EXIT:`) 61 62val mc_is_quote_blast = blastLib.BBLAST_PROVE 63 ``((31 -- 0) (w2w (w:word32)):word64 = w2w w) /\ 64 ((w2w w && 0x1w = 0x0w:word64) = (w && 0x1w = 0x0w))`` 65 66val mc_is_quote_thm = prove( 67 ``^LISP ==> 68 mc_is_quote_pre (w2w w0,bp,df,f) /\ 69 (mc_is_quote (w2w w0,bp,df,f) = (if isQuote x0 then 1w else 0w,bp,df,f))``, 70 SIMP_TAC std_ss [isQuote_def,mc_is_quote_def,LET_DEF,mc_is_quote_blast] 71 \\ STRIP_TAC \\ IMP_RES_TAC lisp_inv_type \\ ASM_SIMP_TAC std_ss [] 72 \\ Cases_on `isDot x0` \\ FULL_SIMP_TAC std_ss [] 73 \\ IMP_RES_TAC lisp_inv_car 74 \\ IMP_RES_TAC (el 3 (CONJUNCTS lisp_inv_Sym)) 75 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 76 \\ Cases_on `CAR x0 = Sym "QUOTE"` \\ ASM_SIMP_TAC std_ss [] 77 \\ IMP_RES_TAC lisp_inv_cdr 78 \\ IMP_RES_TAC lisp_inv_type \\ ASM_SIMP_TAC std_ss [] 79 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 80 \\ Cases_on `isDot (CDR x0)` \\ ASM_SIMP_TAC std_ss [] 81 \\ IMP_RES_TAC lisp_inv_cdr 82 \\ IMP_RES_TAC (el 1 (CONJUNCTS lisp_inv_Sym)) 83 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 84 \\ Cases_on `CDR (CDR x0) = Sym "NIL"` \\ ASM_SIMP_TAC std_ss []); 85 86val (mc_is_quote_full_spec,mc_is_quote_full_def) = basic_decompile_strings x64_tools "mc_is_quote_full" 87 (SOME (``(r8:word64,r6:word64,df:word64 set,f:word64->word32)``, 88 ``(r0:word64,r1:word64,r8:word64,r6:word64,df:word64 set,f:word64->word32)``)) 89 (assemble "x64" ` 90 mov r0,r8 91 insert mc_is_quote 92 mov r0d,3 93 mov r8d,11 94 test r1,r1 95 cmove r8,r0 96 mov r1d,1 97 `) 98 99val _ = save_thm("mc_is_quote_full_spec",mc_is_quote_full_spec); 100 101val mc_is_quote_full_thm = prove( 102 ``^LISP ==> 103 ?v0. mc_is_quote_full_pre (w2w w0,bp,df,f) /\ 104 (mc_is_quote_full (w2w w0,bp,df,f) = (tw0,tw1,w2w v0,bp,df,f)) /\ 105 let (w0,x0) = (v0,LISP_TEST (isQuote x0)) in ^LISP``, 106 FULL_SIMP_TAC std_ss [mc_is_quote_full_def,LET_DEF] \\ STRIP_TAC 107 \\ IMP_RES_TAC mc_is_quote_thm \\ ASM_SIMP_TAC std_ss [] 108 \\ `(tw0 = 3w) /\ (tw1 = 1w)` by FULL_SIMP_TAC std_ss [lisp_inv_def] 109 \\ Cases_on `isQuote x0` \\ FULL_SIMP_TAC wstd_ss [n2w_11,LISP_TEST_def] 110 THEN1 (Q.EXISTS_TAC `0xBw` \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 111 \\ IMP_RES_TAC (el 2 (CONJUNCTS lisp_inv_Sym))) 112 THEN1 (Q.EXISTS_TAC `0x3w` \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 113 \\ IMP_RES_TAC (el 1 (CONJUNCTS lisp_inv_Sym)))) |> SIMP_RULE std_ss [LET_DEF]; 114 115val _ = save_thm("mc_is_quote_full_thm",mc_is_quote_full_thm); 116 117 118(* lookup constant *) 119 120val (mc_const_load_spec,mc_const_load_def) = basic_decompile_strings x64_tools "mc_const_load" 121 (SOME (``(r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``, 122 ``(r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``)) 123 (assemble "x64" ` 124 mov r2,[r7-64] 125 mov r8d,[r2+r8] 126 `) 127 128val PULL_EXISTS_OVER_CONJ = METIS_PROVE [] 129 ``((?x. P x) /\ Q = ?x. P x /\ Q) /\ (Q /\ (?x. P x) = ?x. P x /\ Q)`` 130 131val ref_heap_addr_alt = store_thm("ref_heap_addr_alt", 132 ``(ref_heap_addr (H_ADDR a) = n2w a << 1) /\ 133 (ref_heap_addr (H_DATA (INL w)) = w2w w << 2 + 0x1w) /\ 134 (ref_heap_addr (H_DATA (INR v)) = w2w v << 3 + 0x3w)``, 135 SIMP_TAC std_ss [ref_heap_addr_def] \\ blastLib.BBLAST_TAC); 136 137val mc_const_load_blast = prove( 138 ``w2w ((0x1w:word32) + w2w w << 2) = (0x1w:word64) + w2w (w:word30) << 2``, 139 blastLib.BBLAST_TAC); 140 141val gc_w2w_lemma = prove( 142 ``!w. ((w2w:word64->word32) ((w2w:word32->word64) w) = w) /\ 143 ((31 -- 0) ((w2w:word32->word64) w) = w2w w) /\ 144 ((31 >< 0) bp = (w2w bp):word32) /\ 145 ((63 >< 32) bp = (w2w (bp >>> 32)):word32) /\ 146 (w2w ((w2w (bp >>> 32)):word32) << 32 !! w2w ((w2w bp):word32) = bp:word64)``, 147 blastLib.BBLAST_TAC); 148 149val mc_const_load_thm = prove( 150 ``^LISP ==> getVal x0 < LENGTH xs1 /\ isVal x0 ==> 151 ?w0i tw2i. 152 mc_const_load_pre (tw2,sp,w2w w0,df,f) /\ 153 (mc_const_load (tw2,sp,w2w w0,df,f) = (tw2i,sp,w2w w0i,df,f)) /\ 154 let (x0,tw2,w0) = (EL (getVal x0) xs1, tw2i, w0i) in ^LISP``, 155 FULL_SIMP_TAC std_ss [LET_DEF,mc_const_load_def] \\ REPEAT STRIP_TAC 156 \\ IMP_RES_TAC lisp_inv_ds_read 157 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,gc_w2w_lemma] 158 \\ `sp && 0x3w = 0x0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 159 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,isVal_thm,getVal_def] 160 \\ Q.EXISTS_TAC `f (w2w w0 + EL 6 ds)` \\ FULL_SIMP_TAC std_ss [] 161 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` ASSUME_TAC 162 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,PULL_EXISTS_OVER_CONJ,EVERY_DEF,lisp_x_def] 163 \\ Q.LIST_EXISTS_TAC [`EL a ss1`,`s1`,`s2`,`s3`,`s4`,`s5`] 164 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 165 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,EVERY_DEF,LENGTH,ADD1,ZIP,EVERY_DEF,getVal_def] 166 \\ `?ss3 s ss4. (ss1 = ss3 ++ s::ss4) /\ (LENGTH ss3 = a)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 167 \\ `?xs3 x xs4. (xs1 = xs3 ++ x::xs4) /\ (LENGTH xs3 = a)` by METIS_TAC [SPLIT_LIST,APPEND_ASSOC,APPEND] 168 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,ZIP,EVERY_DEF,EVERY_APPEND,GSYM APPEND_ASSOC] 169 \\ FULL_SIMP_TAC std_ss [ZIP,APPEND,EVERY_DEF] 170 \\ FULL_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2,LENGTH_APPEND,LENGTH,EL,HD] 171 \\ SIMP_TAC std_ss [GSYM CONJ_ASSOC] \\ STRIP_TAC THEN1 172 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 173 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 174 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n] \\ REPEAT STRIP_TAC 175 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 176 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 177 \\ Q.PAT_X_ASSUM `EVERY xx yy` MP_TAC 178 \\ FULL_SIMP_TAC std_ss [ZIP_APPEND,EVERY_APPEND,ZIP,EVERY_DEF] \\ STRIP_TAC 179 \\ Q.PAT_X_ASSUM `ref_heap_addr (H_DATA (INL (n2w a))) = w0` (MP_TAC o GSYM) 180 \\ FULL_SIMP_TAC std_ss [RW1 [WORD_ADD_COMM] ref_heap_addr_alt,mc_const_load_blast] 181 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] 182 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC,WORD_SUB_ADD] \\ STRIP_TAC 183 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,APPEND_ASSOC] 184 \\ FULL_SIMP_TAC std_ss [ref_stack_def,Once ref_stack_APPEND,APPEND] 185 \\ Cases_on `wsp` 186 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC,word_mul_n2w,word_arith_lemma1,w2n_n2w] 187 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL,word_mul_n2w] 188 \\ FULL_SIMP_TAC std_ss [GSYM LEFT_ADD_DISTRIB,LENGTH_APPEND,word_arith_lemma1] 189 \\ Q.PAT_X_ASSUM `LENGTH ss + n = sl` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 190 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC] \\ SEP_R_TAC 191 \\ ASM_SIMP_TAC std_ss [align_add_blast,n2w_and_3,RW1[MULT_COMM]MOD_EQ_0]) 192 |> SIMP_RULE std_ss [LET_DEF]; 193 194val _ = save_thm("mc_const_load_spec",mc_const_load_spec); 195val _ = save_thm("mc_const_load_thm",mc_const_load_thm); 196 197 198(* store new constant *) 199 200val (mc_const_store_spec,mc_const_store_def) = basic_decompile_strings x64_tools "mc_const_store" 201 (SOME (``(r0:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``, 202 ``(r0:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32)``)) 203 (assemble "x64" ` 204 mov r0,[r7-48] 205 mov r2,[r7-64] 206 shl r0,2 207 inc r2 208 dec QWORD [r7-56] 209 inc QWORD [r7-48] 210 mov [r0+r2],r8d 211 xor r8,r8 212 not r8 213 mov [r0+r2+4],r8d 214 inc r0 215 mov r8d,r0 216 mov r0d,3 217 `) 218 219val EL_UPDATE_NTH = store_thm("EL_UPDATE_NTH", 220 ``!xs n k x. EL n (UPDATE_NTH k x xs) = 221 if (k = n) /\ k < LENGTH xs then x else EL n xs``, 222 Induct \\ Cases_on `k` \\ SIMP_TAC std_ss [LENGTH,UPDATE_NTH_def] 223 THEN1 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] \\ FULL_SIMP_TAC std_ss [ADD1]) 224 \\ Cases_on `n'` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] 225 \\ FULL_SIMP_TAC std_ss [ADD1]); 226 227val mc_const_store_blast = blastLib.BBLAST_PROVE 228 ``(31 -- 0) (w:word64) = w2w ((w2w w):word32)`` 229 230val mc_const_store_thm = prove( 231 ``~(EL 7 ds = 0w) /\ ^LISP ==> 232 ?w0i tw2i fi. 233 mc_const_store_pre (tw0,tw2,sp,w2w w0,df,f) /\ 234 (mc_const_store (tw0,tw2,sp,w2w w0,df,f) = (tw0,tw2i,sp,w2w w0i,df,fi)) /\ 235 let (x0,xs1,tw2,w0,f,ds) = (Val (LENGTH xs1), xs1 ++ [x0], 236 tw2i, w0i, fi, UPDATE_NTH 7 (EL 7 ds - 1w) (UPDATE_NTH 8 (EL 8 ds + 1w) ds)) in ^LISP``, 237 FULL_SIMP_TAC std_ss [LET_DEF,mc_const_store_def] \\ REPEAT STRIP_TAC 238 \\ IMP_RES_TAC lisp_inv_ds_read 239 \\ FULL_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET,gc_w2w_lemma] 240 \\ `sp && 0x3w = 0x0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 241 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,isVal_thm,getVal_def] 242 \\ Q.EXISTS_TAC `w2w (EL 8 ds) << 2 + 0x1w` \\ FULL_SIMP_TAC std_ss [] 243 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` ASSUME_TAC 244 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,PULL_EXISTS_OVER_CONJ,EVERY_DEF,lisp_x_def] 245 \\ Q.LIST_EXISTS_TAC [`s1`,`s2`,`s3`,`s4`,`s5`] 246 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1 ++ [s0]`,`sym`,`b`] 247 \\ FULL_SIMP_TAC std_ss [LENGTH_UPDATE_NTH,EL_UPDATE_NTH] 248 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,LENGTH_APPEND,WORD_SUB_ADD,LENGTH] 249 \\ FULL_SIMP_TAC std_ss [n2w_11,MAP,CONS_11,ref_heap_addr_alt,word_arith_lemma2] 250 \\ `(sl1 - LENGTH ss1) < 18446744073709551616` by DECIDE_TAC 251 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [] 252 \\ `~(sl1 < LENGTH ss1 + 1) /\ LENGTH ss1 + 1 <= sl1` by DECIDE_TAC 253 \\ Q.PAT_X_ASSUM `LENGTH xs = LENGTH ss` ASSUME_TAC 254 \\ FULL_SIMP_TAC std_ss [SUB_PLUS,ZIP_APPEND,EVERY_APPEND,EVERY_DEF,ZIP] 255 \\ `sp + n2w (4 * sl) - 0x1w + n2w (LENGTH ss1) << 2 + 0x1w = 256 sp + n2w (4 * sl) + n2w (LENGTH ss1) << 2` by WORD_DECIDE_TAC 257 \\ `LENGTH ss1 < 1073741824 /\ LENGTH ss1 < 18446744073709551616` by DECIDE_TAC 258 \\ `(4 * LENGTH ss1 + 1) < 18446744073709551616` by DECIDE_TAC 259 \\ `0xFFFFFFFFFFFFFFFFw = 0xFFFFFFFFw:word32` by EVAL_TAC 260 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,GSYM LEFT_ADD_DISTRIB, 261 align_add_blast,n2w_and_3,RW1[MULT_COMM]MOD_EQ_0,GSYM CONJ_ASSOC, 262 EVAL ``w2n (~0x0w:word64)``,WORD_MUL_LSL,word_mul_n2w,word_arith_lemma1, 263 mc_const_store_blast] \\ STRIP_TAC THEN1 264 (FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ref_heap_addr_def] 265 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,ADDR_SET_def,GSPECIFICATION,lisp_x_def] 266 \\ FULL_SIMP_TAC std_ss [MEM,MEM_APPEND,n2w_w2n] \\ REPEAT STRIP_TAC 267 \\ Q.PAT_X_ASSUM `!x. bb \/ bbb ==> bbbb` MATCH_MP_TAC 268 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) []) 269 \\ Q.PAT_X_ASSUM `LENGTH cs = 10` MP_TAC 270 \\ IMP_RES_TAC expand_list 271 \\ FULL_SIMP_TAC std_ss [UPDATE_NTH_CONS, 272 GSYM (SIMP_RULE std_ss [word_mul_n2w] (Q.SPECL [`n2w a`,`32`] WORD_MUL_LSL))] 273 \\ `(sl1 - LENGTH ss1 - 1) < 18446744073709551616` by DECIDE_TAC 274 \\ FULL_SIMP_TAC std_ss [GSYM w2w_def] 275 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` MP_TAC 276 \\ FULL_SIMP_TAC std_ss [EL_CONS] \\ NTAC 2 STRIP_TAC 277 \\ Q.ABBREV_TAC `aa = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex]` 278 \\ `LENGTH aa = 8` by (Q.UNABBREV_TAC `aa` \\ EVAL_TAC) 279 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_static_APPEND,LENGTH_APPEND] 280 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,ref_static_def,LET_DEF,word64_3232_def,STAR_ASSOC] 281 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] 282 \\ Q.ABBREV_TAC `ss2 = ss ++ ss1` 283 \\ SIMP_TAC std_ss [ref_stack_APPEND,ref_stack_def,STAR_ASSOC] 284 \\ FULL_SIMP_TAC std_ss [RW [APPEND_NIL,ref_stack_def] (Q.SPECL [`xs`,`[]`] ref_stack_APPEND)] 285 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC] 286 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) 287 [APPLY_UPDATE_THM,RW [GSYM word_sub_def] (Q.SPECL [`w`,`-x`,`-y`] WORD_EQ_ADD_LCANCEL), 288 WORD_EQ_NEG,n2w_11,word_add_n2w] 289 \\ Cases_on `sl1 - LENGTH ss1` THEN1 (`F` by DECIDE_TAC) 290 \\ FULL_SIMP_TAC std_ss [] 291 \\ `sp + 0x4w * wsp + n2w (4 * LENGTH ss2) = 292 sp + n2w (4 * (sl + LENGTH ss1))` by 293 (Cases_on `wsp` \\ FULL_SIMP_TAC std_ss [word_mul_n2w,w2n_n2w] 294 \\ Q.UNABBREV_TAC `ss2` 295 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,LENGTH_APPEND,GSYM LEFT_ADD_DISTRIB] 296 \\ NTAC 3 AP_TERM_TAC \\ DECIDE_TAC) 297 \\ Q.UNABBREV_TAC `ss2` 298 \\ FULL_SIMP_TAC std_ss [ref_stack_space_above_def,STAR_ASSOC, 299 SEP_CLAUSES,LEFT_ADD_DISTRIB,SEP_EXISTS_THM,LENGTH_APPEND] 300 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 301 \\ REVERSE STRIP_TAC THEN1 SEP_READ_TAC 302 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD_ASSOC,GSYM word_add_n2w,WORD_ADD_ASSOC] 303 \\ SEP_W_TAC 304 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 305 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] 306 \\ POP_ASSUM MP_TAC 307 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w] 308 \\ `n < 18446744073709551616` by DECIDE_TAC 309 \\ FULL_SIMP_TAC (std_ss++star_ss) [] 310 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC]) 311 |> SIMP_RULE std_ss [LET_DEF]; 312 313val _ = save_thm("mc_const_store_spec",mc_const_store_spec); 314val _ = save_thm("mc_const_store_thm",mc_const_store_thm); 315 316 317(* xbp set *) 318 319val (mc_xbp_set_spec,mc_xbp_set_def) = basic_decompile_strings x64_tools "mc_xbp_set" 320 (SOME (``(r2:word64,r3:word64,r7:word64,df:word64 set,f:word64->word32)``, 321 ``(r2:word64,r3:word64,r7:word64,df:word64 set,f:word64->word32)``)) 322 (assemble "x64" ` 323 lea r2,[4*r3+r7-1] 324 mov [r7-104],r2 325 `) 326 327val UPDATE_NTH_1 = prove(``UPDATE_NTH 1 x (y1::y2::ys) = y1::x::ys``, EVAL_TAC); 328 329val mc_xbp_set_thm = prove( 330 ``^LISP ==> 331 ?tw2i fi. 332 mc_xbp_set_pre (tw2,wsp,sp,df,f) /\ 333 (mc_xbp_set (tw2,wsp,sp,df,f) = (tw2i,wsp,sp,df,fi)) /\ 334 let (xbp,tw2,ds,f) = (LENGTH xs, tw2i, UPDATE_NTH 1 (sp + 4w * wsp - 1w) ds, fi) in ^LISP``, 335 SIMP_TAC std_ss [mc_xbp_set_def,LET_DEF,INSERT_SUBSET,EMPTY_SUBSET] \\ STRIP_TAC 336 \\ `(sp - 0x64w IN df /\ sp - 0x68w IN df)` by 337 (IMP_RES_TAC lisp_inv_ds_read \\ ASM_SIMP_TAC std_ss []) 338 \\ FULL_SIMP_TAC std_ss [LET_DEF,lisp_inv_def] 339 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 340 \\ ASM_SIMP_TAC std_ss [] 341 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`] 342 \\ Q.LIST_EXISTS_TAC [`m`,`i`,`ss`,`ss1`,`sym`,`b`] 343 \\ FULL_SIMP_TAC std_ss [LENGTH_UPDATE_NTH,EL_UPDATE_NTH] 344 \\ Q.PAT_X_ASSUM `xxx = sl` (ASSUME_TAC o GSYM o RW1[ADD_COMM]) 345 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 346 (FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,GSYM word_add_n2w, 347 WORD_ADD_ASSOC,WORD_ADD_SUB,WORD_EQ_ADD_LCANCEL,WORD_EQ_ADD_RCANCEL] 348 \\ FULL_SIMP_TAC std_ss [GSYM word_mul_n2w,n2w_w2n]) 349 \\ Cases_on `ds` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 350 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 351 \\ Q.PAT_X_ASSUM `xxx (fun2set (f,df))` MP_TAC 352 \\ FULL_SIMP_TAC std_ss [ref_full_stack_def,ref_static_APPEND,LENGTH,LENGTH_APPEND] 353 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,UPDATE_NTH_1] 354 \\ Q.ABBREV_TAC `xssss = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex]` 355 \\ FULL_SIMP_TAC std_ss [ref_static_def,word64_3232_def,LET_DEF] 356 \\ FULL_SIMP_TAC std_ss [word_arith_lemma3,word_arith_lemma2,word_arith_lemma1, 357 STAR_ASSOC,gc_w2w_lemma] 358 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 359 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC) |> SIMP_RULE std_ss [LET_DEF]; 360 361val _ = save_thm("mc_xbp_set_spec",mc_xbp_set_spec); 362val _ = save_thm("mc_xbp_set_thm",mc_xbp_set_thm); 363 364 365(* load based on xbp *) 366 367val (mc_xbp_load_spec,mc_xbp_load_def) = basic_decompile_strings x64_tools "mc_xbp_load" 368 (SOME (``(r2:word64,r7:word64,r9:word64,df:word64 set,f:word64->word32)``, 369 ``(r2:word64,r7:word64,r9:word64,r12:word64,df:word64 set,f:word64->word32)``)) 370 (assemble "x64" ` 371 mov r2,[r7-104] 372 mov r12d,[r2+r9] 373 `) 374 375val BLAST_LEMMA = prove(``w << 2 !! 1w = w << 2 + 1w:word32``,blastLib.BBLAST_TAC); 376 377val EL_UPDATE_NTH = store_thm("EL_UPDATE_NTH", 378 ``!xs n k x. EL n (UPDATE_NTH k x xs) = 379 if (k = n) /\ k < LENGTH xs then x else EL n xs``, 380 Induct \\ Cases_on `k` \\ SIMP_TAC std_ss [LENGTH,UPDATE_NTH_def] 381 THEN1 (Cases_on `n` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] \\ FULL_SIMP_TAC std_ss [ADD1]) 382 \\ Cases_on `n'` \\ FULL_SIMP_TAC std_ss [EL,HD,TL] 383 \\ FULL_SIMP_TAC std_ss [ADD1]); 384 385val UPDATE_NTH_1 = prove(``UPDATE_NTH 1 x (y1::y2::ys) = y1::x::ys``, EVAL_TAC); 386 387val mc_xbp_load_blast = blastLib.BBLAST_PROVE 388 ``((31 -- 0) (w2w w1) = (w2w w2):word64) = (w1 = w2:word32)`` 389 390val mc_xbp_load_thm = prove( 391 ``^LISP ==> isVal x1 /\ getVal x1 < xbp /\ xbp <= LENGTH xs ==> 392 ?tw2i w4i. 393 mc_xbp_load_pre (tw2,sp,w2w w1,df,f) /\ 394 (mc_xbp_load (tw2,sp,w2w w1,df,f) = (tw2i,sp,w2w w1,w2w w4i,df,f)) /\ 395 let (x4,tw2,w4) = (EL ((LENGTH xs + getVal x1) - xbp) xs,tw2i,w4i) in ^LISP``, 396 Cases_on `isVal x1` \\ FULL_SIMP_TAC std_ss [LET_DEF] 397 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def] \\ STRIP_TAC 398 \\ SIMP_TAC std_ss [mc_xbp_load_def,LET_DEF,INSERT_SUBSET,EMPTY_SUBSET] 399 \\ IMP_RES_TAC lisp_inv_ds_read \\ ASM_SIMP_TAC std_ss [] 400 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 401 \\ NTAC 2 STRIP_TAC \\ FULL_SIMP_TAC std_ss [mc_xbp_load_blast] 402 \\ Q.ABBREV_TAC `n = LENGTH xs + a - xbp` 403 \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by 404 (FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11,EVERY_DEF,lisp_x_def] 405 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (MP_TAC o GSYM) 406 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,BLAST_LEMMA] 407 \\ REPEAT STRIP_TAC 408 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL] 409 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC 410 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 411 \\ ONCE_REWRITE_TAC [ADD_COMM] 412 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_ADD,WORD_ADD_ASSOC] 413 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3] 414 \\ Q.PAT_X_ASSUM `LENGTH ss + w2n wsp = sl` (MP_TAC o GSYM) 415 \\ ASM_SIMP_TAC std_ss [] \\ Q.SPEC_TAC (`wsp`,`w`) 416 \\ Cases \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,w2n_n2w] 417 \\ `~(4 * (LENGTH ss + n') < 4 * xbp - 4 * a)` by DECIDE_TAC 418 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL,word_arith_lemma4] 419 \\ REPEAT STRIP_TAC \\ AP_TERM_TAC \\ Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 420 \\ ASM_SIMP_TAC std_ss [] 421 \\ `n < LENGTH xs` by (Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 422 \\ IMP_RES_TAC lisp_inv_swap4 423 \\ IMP_RES_TAC (RW[AND_IMP_INTRO]lisp_inv_load_lemma) 424 \\ ASM_SIMP_TAC std_ss [] 425 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 426 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 427 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3] 428 \\ MATCH_MP_TAC lisp_inv_swap4 429 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ ASM_SIMP_TAC std_ss [] 430 \\ Q.EXISTS_TAC `tw2` \\ ASM_SIMP_TAC std_ss []) 431 |> SIMP_RULE std_ss [LET_DEF]; 432 433val _ = save_thm("mc_xbp_load_spec",mc_xbp_load_spec); 434val _ = save_thm("mc_xbp_load_thm",mc_xbp_load_thm); 435 436 437(* load amnt *) 438 439val (mc_load_amnt_spec,mc_load_amnt_def) = basic_decompile_strings x64_tools "mc_load_amnt" 440 (SOME (``(r7:word64,df:word64 set,f:word64->word32)``, 441 ``(r7:word64,r9:word64,df:word64 set,f:word64->word32)``)) 442 (assemble "x64" ` 443 mov r9d,[r7-40] 444 shl r9d,2 445 inc r9d 446 `) 447 448val mc_load_amnt_thm = prove( 449 ``^LISP ==> 450 ?w1i. 451 mc_load_amnt_pre (sp,df,f) /\ 452 (mc_load_amnt (sp,df,f) = (sp,w2w w1i,df,f)) /\ 453 let (x1,w1) = (Val amnt,w1i) in ^LISP``, 454 FULL_SIMP_TAC std_ss [mc_load_amnt_def,LET_DEF,mc_xbp_load_blast] \\ STRIP_TAC 455 \\ IMP_RES_TAC lisp_inv_swap1 456 \\ IMP_RES_TAC lisp_inv_amnt_read 457 \\ Q.EXISTS_TAC `w2w ((w2w (f (sp - 0x24w)) << 32 !! (w2w:word32->word64) (f (sp - 0x28w))) << 2 + 0x1w)` 458 \\ IMP_RES_TAC lisp_inv_swap1 459 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL] 460 \\ Q.SPEC_TAC (`f (sp - 0x24w)`,`w`) 461 \\ Q.SPEC_TAC (`f (sp - 0x28w)`,`w1`) 462 \\ blastLib.BBLAST_TAC); 463 464val _ = save_thm("mc_load_amnt_spec",mc_load_amnt_spec); 465val _ = save_thm("mc_load_amnt_thm",mc_load_amnt_thm); 466 467 468(* pops by x1 *) 469 470val (mc_pops_by_var_spec,mc_pops_by_var_def) = basic_decompile_strings x64_tools "mc_pops_by_var" 471 (SOME (``(r2:word64,r3:word64,r9:word64)``, 472 ``(r2:word64,r3:word64,r9:word64)``)) 473 (assemble "x64" ` 474 mov r2,r9 475 shr r2,2 476 add r3,r2 477 `) 478 479val mc_pops_by_var_thm = prove( 480 ``^LISP ==> isVal x1 /\ getVal x1 <= LENGTH xs ==> 481 ?tw2i wspi. 482 mc_pops_by_var_pre (tw2,wsp,w2w w1) /\ 483 (mc_pops_by_var (tw2,wsp,w2w w1) = (tw2i,wspi,w2w w1)) /\ 484 let (xs,wsp,tw2) = (DROP (getVal x1) xs,wspi,tw2i) in ^LISP``, 485 Cases_on `isVal x1` \\ FULL_SIMP_TAC std_ss [] 486 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def,LET_DEF,mc_pops_by_var_def] 487 \\ REPEAT STRIP_TAC 488 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ ASM_SIMP_TAC std_ss [] 489 \\ Q.EXISTS_TAC `tw2` \\ ASM_SIMP_TAC std_ss [] 490 \\ SUBGOAL `wsp + w2w w1 >>> 2 = wsp + n2w a` THEN1 491 (ASM_SIMP_TAC std_ss [] 492 \\ MATCH_MP_TAC(RW[AND_IMP_INTRO]lisp_inv_pops_lemma) 493 \\ ASM_SIMP_TAC std_ss []) 494 \\ FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11,EVERY_DEF,lisp_x_def] 495 \\ Q.PAT_X_ASSUM `xxx = w1` (MP_TAC o GSYM) 496 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def] 497 \\ SUBGOAL `n2w a = (w2w:word30->word64) (n2w a)` THEN1 498 (FULL_SIMP_TAC std_ss [] 499 \\ Q.SPEC_TAC (`(n2w a):word30`,`w`) \\ blastLib.BBLAST_TAC) 500 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]); 501 502val _ = save_thm("mc_pops_by_var_spec",mc_pops_by_var_spec); 503val _ = save_thm("mc_pops_by_var_thm",mc_pops_by_var_thm); 504 505 506(* store based on xbp *) 507 508val (mc_xbp_store_spec,mc_xbp_store_def) = basic_decompile_strings x64_tools "mc_xbp_store" 509 (SOME (``(r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32)``, 510 ``(r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32)``)) 511 (assemble "x64" ` 512 mov r2,[r7-104] 513 mov [r2+r9],r8d 514 `) 515 516val mc_xbp_store_blast = blastLib.BBLAST_PROVE 517 ``w2w ((w2w w):word64) = (w:word32)`` 518 519val mc_xbp_store_thm = prove( 520 ``^LISP ==> isVal x1 /\ getVal x1 < xbp /\ xbp <= LENGTH xs ==> 521 ?tw2i fi. 522 mc_xbp_store_pre (tw2,sp,w2w w0,w2w w1,df,f) /\ 523 (mc_xbp_store (tw2,sp,w2w w0,w2w w1,df,f) = (tw2i,sp,w2w w0,w2w w1,df,fi)) /\ 524 let (xs,tw2,f) = (UPDATE_NTH ((LENGTH xs + getVal x1) - xbp) x0 xs,tw2i,fi) in ^LISP``, 525 Cases_on `isVal x1` \\ FULL_SIMP_TAC std_ss [LET_DEF] 526 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def] \\ STRIP_TAC 527 \\ SIMP_TAC std_ss [mc_xbp_store_def,LET_DEF,INSERT_SUBSET,EMPTY_SUBSET] 528 \\ IMP_RES_TAC lisp_inv_ds_read \\ ASM_SIMP_TAC std_ss [] 529 \\ Q.PAT_X_ASSUM `lisp_inv xxx yyy zzz` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 530 \\ NTAC 2 STRIP_TAC \\ FULL_SIMP_TAC std_ss [mc_xbp_load_blast] 531 \\ Q.ABBREV_TAC `n = LENGTH xs + a - xbp` 532 \\ `EL 1 ds + w2w w1 = sp + 0x4w * wsp + 0x4w * n2w n` by 533 (FULL_SIMP_TAC std_ss [lisp_inv_def,MAP,CONS_11,EVERY_DEF,lisp_x_def] 534 \\ Q.PAT_X_ASSUM `ref_heap_addr s1 = w1` (MP_TAC o GSYM) 535 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_def,BLAST_LEMMA] 536 \\ REPEAT STRIP_TAC 537 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL] 538 \\ `(4 * a + 1) < 4294967296` by DECIDE_TAC 539 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [word_mul_n2w,word_add_n2w,w2n_n2w] 540 \\ ONCE_REWRITE_TAC [ADD_COMM] 541 \\ SIMP_TAC std_ss [GSYM word_add_n2w,WORD_SUB_ADD,WORD_ADD_ASSOC] 542 \\ ASM_SIMP_TAC std_ss [word_arith_lemma3] 543 \\ Q.PAT_X_ASSUM `LENGTH ss + w2n wsp = sl` (MP_TAC o GSYM) 544 \\ ASM_SIMP_TAC std_ss [] \\ Q.SPEC_TAC (`wsp`,`w`) 545 \\ Cases \\ ASM_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,w2n_n2w] 546 \\ `~(4 * (LENGTH ss + n') < 4 * xbp - 4 * a)` by DECIDE_TAC 547 \\ ASM_SIMP_TAC std_ss [WORD_EQ_ADD_LCANCEL,word_arith_lemma4] 548 \\ REPEAT STRIP_TAC \\ AP_TERM_TAC \\ Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 549 \\ ASM_SIMP_TAC std_ss [] 550 \\ `n < LENGTH xs` by (Q.UNABBREV_TAC `n` \\ DECIDE_TAC) 551 \\ IMP_RES_TAC (RW[AND_IMP_INTRO]lisp_inv_store_lemma) 552 \\ ASM_SIMP_TAC std_ss [] 553 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 554 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 555 \\ FULL_SIMP_TAC std_ss [align_blast,n2w_and_3,mc_xbp_store_blast] 556 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ ASM_SIMP_TAC std_ss [] 557 \\ Q.EXISTS_TAC `tw2` \\ ASM_SIMP_TAC std_ss []) 558 |> SIMP_RULE std_ss [LET_DEF]; 559 560val _ = save_thm("mc_xbp_store_spec",mc_xbp_store_spec); 561val _ = save_thm("mc_xbp_store_thm",mc_xbp_store_thm); 562 563 564(* read code_ptr code *) 565 566val (mc_read_snd_code_spec,mc_read_snd_code_def) = basic_decompile_strings x64_tools "mc_read_snd_code" 567 (SOME (``(r7:word64,r8:word64,df:word64 set,f:word64->word32)``, 568 ``(r7:word64,r8:word64,df:word64 set,f:word64->word32)``)) 569 (assemble "x64" ` 570 mov r8,[r7-96] 571 sub r8,[r7-160] 572 shl r8,2 573 inc r8 574 `) 575 576val mc_read_snd_code_thm = prove( 577 ``^LISP ==> 578 ?v0. 579 mc_read_snd_code_pre (sp,w2w w0,df,f) /\ 580 (mc_read_snd_code (sp,w2w w0,df,f) = (sp,w2w v0,df,f)) /\ 581 let (x0,w0) = (Val (code_ptr code),v0) in ^LISP``, 582 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_read_snd_code_def,LET_DEF] 583 \\ IMP_RES_TAC lisp_inv_cs_read \\ IMP_RES_TAC lisp_inv_ds_read 584 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 585 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 586 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 587 \\ Q.EXISTS_TAC `n2w (4 * (code_ptr code) + 1)` 588 \\ `code_ptr code < 1073741824` by 589 (FULL_SIMP_TAC std_ss [lisp_inv_def,code_heap_def] \\ DECIDE_TAC) 590 \\ REVERSE STRIP_TAC 591 THEN1 (MATCH_MP_TAC lisp_inv_Val_n2w \\ ASM_SIMP_TAC std_ss []) 592 \\ `EL 2 ds - EL 4 cs = n2w (code_ptr code)` by 593 (FULL_SIMP_TAC std_ss [lisp_inv_def,code_heap_def] 594 \\ ONCE_REWRITE_TAC [WORD_ADD_COMM] \\ SIMP_TAC std_ss [WORD_ADD_SUB]) 595 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 596 \\ `(4 * code_ptr code + 1) < 4294967296` by DECIDE_TAC 597 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 598 |> SIMP_RULE std_ss [LET_DEF]; 599 600val _ = save_thm("mc_read_snd_code_spec",mc_read_snd_code_spec); 601val _ = save_thm("mc_read_snd_code_thm",mc_read_snd_code_thm); 602 603 604(* safe versions of car and cdr, i.e. total versions *) 605 606val SAFE_CAR_def = Define `SAFE_CAR x = CAR x`; 607val SAFE_CDR_def = Define `SAFE_CDR x = CDR x`; 608 609val (mc_safe_car_spec,mc_safe_car_def) = basic_decompile_strings x64_tools "mc_safe_car" 610 (SOME (``(r0:word64,r6:word64,r8:word64,df:word64 set,f:word64->word32)``, 611 ``(r0:word64,r6:word64,r8:word64,df:word64 set,f:word64->word32)``)) 612 (assemble "x64" ` 613 test r8,1 614 cmovne r8,r0 615 jne L 616 mov r8d, [r6+4*r8] 617L: `) 618 619val (mc_safe_cdr_spec,mc_safe_cdr_def) = basic_decompile_strings x64_tools "mc_safe_cdr" 620 (SOME (``(r0:word64,r6:word64,r8:word64,df:word64 set,f:word64->word32)``, 621 ``(r0:word64,r6:word64,r8:word64,df:word64 set,f:word64->word32)``)) 622 (assemble "x64" ` 623 test r8,1 624 cmovne r8,r0 625 jne L 626 mov r8d, [r6+4*r8+4] 627L: `) 628 629val mc_safe_car_pre_def = CONJUNCT2 mc_safe_car_def 630val mc_safe_cdr_pre_def = CONJUNCT2 mc_safe_cdr_def 631 632val mc_safe_car_blast = blastLib.BBLAST_PROVE 633 ``((w2w (w0:word32) && 0x1w = 0x0w:word64) = (w0 && 1w = 0w)) /\ 634 ((((31 -- 0) ((w2w w))) = (w2w (v:word32)):word64) = (w = v))`` 635 636val mc_safe_car_lemma = prove( 637 ``^LISP ==> 638 ?w0i. 639 mc_safe_car_pre (tw0,bp,w2w w0,df,f) /\ 640 (mc_safe_car (tw0,bp,w2w w0,df,f) = (tw0,bp,w2w w0i,df,f)) /\ 641 let (x0,w0) = (SAFE_CAR x0,w0i) in ^LISP``, 642 FULL_SIMP_TAC std_ss [SAFE_CAR_def,SAFE_CDR_def] 643 \\ FULL_SIMP_TAC std_ss [mc_safe_car_def,mc_safe_cdr_def,LET_DEF] 644 \\ FULL_SIMP_TAC std_ss [mc_safe_car_blast] \\ STRIP_TAC 645 \\ IMP_RES_TAC lisp_inv_type \\ ASM_SIMP_TAC std_ss [] 646 \\ Cases_on `isDot x0` \\ ASM_SIMP_TAC std_ss [] THEN1 647 (IMP_RES_TAC lisp_inv_car \\ IMP_RES_TAC lisp_inv_cdr 648 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,mc_safe_car_blast]) 649 \\ `(CAR x0 = Sym "NIL") /\ (CDR x0 = Sym "NIL")` by 650 (Cases_on `x0` \\ FULL_SIMP_TAC std_ss [isDot_def,CAR_def,CDR_def]) 651 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `3w` 652 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 653 \\ IMP_RES_TAC lisp_inv_nil 654 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 655 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 656 |> SIMP_RULE std_ss [LET_DEF]; 657 658val mc_safe_car_thm = prove( 659 ``^LISP ==> 660 (?w0i. 661 mc_safe_car_pre (tw0,bp,w2w w0,df,f) /\ 662 (mc_safe_car (tw0,bp,w2w w0,df,f) = (tw0,bp,w2w w0i,df,f)) /\ 663 let (x0,w0) = (SAFE_CAR x0,w0i) in ^LISP) /\ 664 (?w1i. 665 mc_safe_car_pre (tw0,bp,w2w w1,df,f) /\ 666 (mc_safe_car (tw0,bp,w2w w1,df,f) = (tw0,bp,w2w w1i,df,f)) /\ 667 let (x1,w1) = (SAFE_CAR x1,w1i) in ^LISP) /\ 668 (?w2i. 669 mc_safe_car_pre (tw0,bp,w2w w2,df,f) /\ 670 (mc_safe_car (tw0,bp,w2w w2,df,f) = (tw0,bp,w2w w2i,df,f)) /\ 671 let (x2,w2) = (SAFE_CAR x2,w2i) in ^LISP) /\ 672 (?w3i. 673 mc_safe_car_pre (tw0,bp,w2w w3,df,f) /\ 674 (mc_safe_car (tw0,bp,w2w w3,df,f) = (tw0,bp,w2w w3i,df,f)) /\ 675 let (x3,w3) = (SAFE_CAR x3,w3i) in ^LISP) /\ 676 (?w4i. 677 mc_safe_car_pre (tw0,bp,w2w w4,df,f) /\ 678 (mc_safe_car (tw0,bp,w2w w4,df,f) = (tw0,bp,w2w w4i,df,f)) /\ 679 let (x4,w4) = (SAFE_CAR x4,w4i) in ^LISP) /\ 680 (?w5i. 681 mc_safe_car_pre (tw0,bp,w2w w5,df,f) /\ 682 (mc_safe_car (tw0,bp,w2w w5,df,f) = (tw0,bp,w2w w5i,df,f)) /\ 683 let (x5,w5) = (SAFE_CAR x5,w5i) in ^LISP)``, 684 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [LET_DEF] 685 THEN1 (IMP_RES_TAC mc_safe_car_lemma \\ METIS_TAC []) 686 THEN1 (IMP_RES_TAC lisp_inv_swap1 \\ IMP_RES_TAC mc_safe_car_lemma 687 \\ METIS_TAC [lisp_inv_swap1]) 688 THEN1 (IMP_RES_TAC lisp_inv_swap2 \\ IMP_RES_TAC mc_safe_car_lemma 689 \\ METIS_TAC [lisp_inv_swap2]) 690 THEN1 (IMP_RES_TAC lisp_inv_swap3 \\ IMP_RES_TAC mc_safe_car_lemma 691 \\ METIS_TAC [lisp_inv_swap3]) 692 THEN1 (IMP_RES_TAC lisp_inv_swap4 \\ IMP_RES_TAC mc_safe_car_lemma 693 \\ METIS_TAC [lisp_inv_swap4]) 694 THEN1 (IMP_RES_TAC lisp_inv_swap5 \\ IMP_RES_TAC mc_safe_car_lemma 695 \\ METIS_TAC [lisp_inv_swap5])) 696 |> SIMP_RULE std_ss [LET_DEF]; 697 698val mc_safe_cdr_lemma = prove( 699 ``^LISP ==> 700 ?w0i. 701 mc_safe_cdr_pre (tw0,bp,w2w w0,df,f) /\ 702 (mc_safe_cdr (tw0,bp,w2w w0,df,f) = (tw0,bp,w2w w0i,df,f)) /\ 703 let (x0,w0) = (SAFE_CDR x0,w0i) in ^LISP``, 704 FULL_SIMP_TAC std_ss [SAFE_CAR_def,SAFE_CDR_def] 705 \\ FULL_SIMP_TAC std_ss [mc_safe_car_def,mc_safe_cdr_def,LET_DEF] 706 \\ FULL_SIMP_TAC std_ss [mc_safe_car_blast] \\ STRIP_TAC 707 \\ IMP_RES_TAC lisp_inv_type \\ ASM_SIMP_TAC std_ss [] 708 \\ Cases_on `isDot x0` \\ ASM_SIMP_TAC std_ss [] THEN1 709 (IMP_RES_TAC lisp_inv_car \\ IMP_RES_TAC lisp_inv_cdr 710 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM,mc_safe_car_blast]) 711 \\ `(CAR x0 = Sym "NIL") /\ (CDR x0 = Sym "NIL")` by 712 (Cases_on `x0` \\ FULL_SIMP_TAC std_ss [isDot_def,CAR_def,CDR_def]) 713 \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `3w` 714 \\ `tw0 = 3w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 715 \\ IMP_RES_TAC lisp_inv_nil 716 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [] 717 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 718 |> SIMP_RULE std_ss [LET_DEF]; 719 720val mc_safe_cdr_thm = prove( 721 ``^LISP ==> 722 (?w0i. 723 mc_safe_cdr_pre (tw0,bp,w2w w0,df,f) /\ 724 (mc_safe_cdr (tw0,bp,w2w w0,df,f) = (tw0,bp,w2w w0i,df,f)) /\ 725 let (x0,w0) = (SAFE_CDR x0,w0i) in ^LISP) /\ 726 (?w1i. 727 mc_safe_cdr_pre (tw0,bp,w2w w1,df,f) /\ 728 (mc_safe_cdr (tw0,bp,w2w w1,df,f) = (tw0,bp,w2w w1i,df,f)) /\ 729 let (x1,w1) = (SAFE_CDR x1,w1i) in ^LISP) /\ 730 (?w2i. 731 mc_safe_cdr_pre (tw0,bp,w2w w2,df,f) /\ 732 (mc_safe_cdr (tw0,bp,w2w w2,df,f) = (tw0,bp,w2w w2i,df,f)) /\ 733 let (x2,w2) = (SAFE_CDR x2,w2i) in ^LISP) /\ 734 (?w3i. 735 mc_safe_cdr_pre (tw0,bp,w2w w3,df,f) /\ 736 (mc_safe_cdr (tw0,bp,w2w w3,df,f) = (tw0,bp,w2w w3i,df,f)) /\ 737 let (x3,w3) = (SAFE_CDR x3,w3i) in ^LISP) /\ 738 (?w4i. 739 mc_safe_cdr_pre (tw0,bp,w2w w4,df,f) /\ 740 (mc_safe_cdr (tw0,bp,w2w w4,df,f) = (tw0,bp,w2w w4i,df,f)) /\ 741 let (x4,w4) = (SAFE_CDR x4,w4i) in ^LISP) /\ 742 (?w5i. 743 mc_safe_cdr_pre (tw0,bp,w2w w5,df,f) /\ 744 (mc_safe_cdr (tw0,bp,w2w w5,df,f) = (tw0,bp,w2w w5i,df,f)) /\ 745 let (x5,w5) = (SAFE_CDR x5,w5i) in ^LISP)``, 746 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [LET_DEF] 747 THEN1 (IMP_RES_TAC mc_safe_cdr_lemma \\ METIS_TAC []) 748 THEN1 (IMP_RES_TAC lisp_inv_swap1 \\ IMP_RES_TAC mc_safe_cdr_lemma 749 \\ METIS_TAC [lisp_inv_swap1]) 750 THEN1 (IMP_RES_TAC lisp_inv_swap2 \\ IMP_RES_TAC mc_safe_cdr_lemma 751 \\ METIS_TAC [lisp_inv_swap2]) 752 THEN1 (IMP_RES_TAC lisp_inv_swap3 \\ IMP_RES_TAC mc_safe_cdr_lemma 753 \\ METIS_TAC [lisp_inv_swap3]) 754 THEN1 (IMP_RES_TAC lisp_inv_swap4 \\ IMP_RES_TAC mc_safe_cdr_lemma 755 \\ METIS_TAC [lisp_inv_swap4]) 756 THEN1 (IMP_RES_TAC lisp_inv_swap5 \\ IMP_RES_TAC mc_safe_cdr_lemma 757 \\ METIS_TAC [lisp_inv_swap5])) 758 |> SIMP_RULE std_ss [LET_DEF]; 759 760val _ = save_thm("mc_safe_car_spec",mc_safe_car_spec); 761val _ = save_thm("mc_safe_cdr_spec",mc_safe_cdr_spec); 762val _ = save_thm("mc_safe_car_thm",mc_safe_car_thm); 763val _ = save_thm("mc_safe_cdr_thm",mc_safe_cdr_thm); 764 765 766(* code heap space test *) 767 768val mc_code_heap_space_thm = prove( 769 ``^LISP ==> 770 (let tw2 = 3w in ^LISP) /\ 771 ((w2w (f (sp - 0x54w)) << 32 !! w2w (f (sp - 0x58w))) = EL 3 ds) /\ 772 {sp - 0x54w; sp - 0x58w} SUBSET df /\ (sp - 0x54w && 0x3w = 0x0w) /\ 773 (sp - 0x58w && 0x3w = 0x0w)``, 774 STRIP_TAC \\ SIMP_TAC std_ss [LET_DEF] 775 \\ IMP_RES_TAC lisp_inv_cs_read \\ IMP_RES_TAC lisp_inv_ds_read 776 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 777 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 778 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 779 \\ MATCH_MP_TAC lisp_inv_ignore_tw2 \\ METIS_TAC []) 780 |> SIMP_RULE std_ss [LET_DEF]; 781 782val _ = save_thm("mc_code_heap_space_thm",mc_code_heap_space_thm); 783 784 785(* lemmas for code heap write *) 786 787val expand_list = prove( 788 ``!cs. (LENGTH cs = 10) ==> 789 ?c0 c1 c2 c3 c4 c5 c6 c7 c8 c9. cs = [c0;c1;c2;c3;c4;c5;c6;c7;c8;c9]``, 790 Cases \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 791 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 792 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 793 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 794 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 795 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 796 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 797 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 798 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 799 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 800 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11,NOT_CONS_NIL] 801 \\ DECIDE_TAC); 802 803val expand_list2 = prove( 804 ``!cs. (LENGTH cs = 10) ==> ?c0 c1 c2 c3 cs2. cs = (c0::c1::c2::c3::cs2)``, 805 REPEAT STRIP_TAC \\ IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [CONS_11]); 806 807val WRITE_CODE_APPEND = prove( 808 ``!xs ys code. 809 WRITE_CODE code (xs ++ ys) = WRITE_CODE (WRITE_CODE code xs) ys``, 810 Induct \\ Cases_on `code` \\ Cases_on `p` \\ ASM_SIMP_TAC std_ss [WRITE_CODE_def,APPEND]); 811 812val SND_WRITE_CODE = prove( 813 ``!code x. code_ptr (WRITE_CODE code [x]) = code_ptr code + bc_length x``, 814 Cases \\ Cases \\ Cases_on `p` \\ SIMP_TAC std_ss [WRITE_CODE_def,code_ptr_def]); 815 816val bc_symbols_ok_APPEND = prove( 817 ``!xs ys. bc_symbols_ok sym (xs ++ ys) = 818 bc_symbols_ok sym xs /\ bc_symbols_ok sym ys``, 819 Induct \\ SIMP_TAC std_ss [APPEND,bc_symbols_ok_def] \\ Cases_on `h` 820 \\ ASM_SIMP_TAC std_ss [APPEND,bc_symbols_ok_def,CONJ_ASSOC]); 821 822val code_length_def = Define ` 823 (code_length [] = 0) /\ 824 (code_length (x::xs) = bc_length x + code_length xs)`; 825 826val bs2bytes_APPEND = prove( 827 ``!xs ys k sym. 828 bs2bytes (k,sym) (xs ++ ys) = 829 bs2bytes (k,sym) xs ++ bs2bytes (k + code_length xs,sym) ys``, 830 Induct \\ ASM_SIMP_TAC std_ss [APPEND,bs2bytes_def,code_length_def] 831 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC,ADD_ASSOC]); 832 833val bc_length_lemma = prove( 834 ``0x100w <+ w /\ (LENGTH hs = w2n w) /\ n + w2n (w:word64) < 1073741824 ==> 835 bc_length x <= LENGTH hs``, 836 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ `w2n w < 1073741824` by DECIDE_TAC 837 \\ Cases_on `w` \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,word_lo_n2w] 838 \\ Cases_on `x` \\ REPEAT (Cases_on `l`) 839 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def, 840 IMMEDIATE32_def,APPEND] \\ REPEAT DECIDE_TAC); 841 842val SUC_EQ_LENGTH = prove( 843 ``(SUC n <= LENGTH xs) = ?y ys. (xs = (y::ys)) /\ (n <= LENGTH ys)``, 844 Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,NOT_CONS_NIL,CONS_11]); 845 846val DROP_CONS = prove( 847 ``DROP n (x::xs) = if n = 0 then x::xs else DROP (n-1) xs``, 848 SRW_TAC [] []); 849 850val LENGTH_bs2bytes = prove( 851 ``!bs code. 852 (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs = code) ==> 853 (LENGTH (bs2bytes (0,sym) bs) = code_ptr code)``, 854 HO_MATCH_MP_TAC rich_listTheory.SNOC_INDUCT 855 \\ SIMP_TAC std_ss [bs2bytes_def,WRITE_CODE_def,LENGTH,SNOC_APPEND] 856 \\ SIMP_TAC std_ss [WRITE_CODE_APPEND,SND_WRITE_CODE] 857 \\ SIMP_TAC std_ss [bs2bytes_APPEND,LENGTH_APPEND,bs2bytes_def,LENGTH,code_ptr_def] 858 \\ REPEAT STRIP_TAC \\ Cases_on `x` \\ REPEAT (Cases_on `l`) \\ EVAL_TAC); 859 860val write_lemma = prove( 861 ``!w ys. (w2n w = LENGTH ys + k) /\ n + (LENGTH ys + k) < 1073741824 ==> 862 (w2n (w - n2w k) = LENGTH ys)``, 863 Cases \\ FULL_SIMP_TAC wstd_ss [w2n_n2w] 864 \\ ASM_SIMP_TAC wstd_ss [GSYM word_add_n2w,WORD_ADD_SUB,w2n_n2w] 865 \\ REPEAT STRIP_TAC \\ `LENGTH ys < dimword (:'a)` by DECIDE_TAC 866 \\ ASM_SIMP_TAC std_ss []); 867 868val mc_code_heap_blast = blastLib.BBLAST_PROVE 869 ``(w2w ((w2w (w >>> 32)):word32) << 32 !! w2w ((w2w (w:word64)):word32) = w) /\ 870 ((63 >< 32) w = (w2w (w >>> 32)):word32) /\ ((31 >< 0) w = (w2w w):word32)``; 871 872val WRITE_CODE_IMP_code_length = prove( 873 ``!bs code k m. 874 (WRITE_CODE (BC_CODE (m,k)) bs = code) ==> 875 (code_length bs + k = code_ptr code)``, 876 SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 877 \\ Induct \\ ASM_SIMP_TAC std_ss [WRITE_CODE_def,code_length_def,code_ptr_def] 878 \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 879 880 881(* generate approximate code for a few of the bytecode instructions *) 882 883fun approx_code inst = let 884 val xs = EVAL (mk_comb(``bc_ref (i,sym)``,inst)) 885 |> concl |> dest_eq |> snd |> listSyntax.dest_list |> fst 886 |> map (fn tm => if can (numSyntax.int_of_term o cdr) tm then tm else ``0w:word64``) 887 |> map (numSyntax.int_of_term o cdr) 888 |> map (fn n => n mod 256) 889 |> map (fn x => if x < 128 then x else x - 256) 890 val enc = x64_encodeLib.x64_encode 891 fun my_int_to_string n = if n < 0 then "-" ^ int_to_string (0-n) else int_to_string n 892 fun encs (i,[]) = [] 893 | encs (i,(x::xs)) = ("mov BYTE [r2+"^ int_to_string i ^"]," ^ my_int_to_string x) 894 :: encs (i+1,xs) 895 val l = length xs 896 val code = (["mov r2,[r7-96]"] @ encs (0,xs) @ 897 ["mov r2,[r7-88]"] @ 898 ["sub r2," ^ int_to_string l] @ 899 ["add QWORD [r7-96]," ^ int_to_string l] @ 900 ["mov [r7-88],r2"]) 901 val _ = print "\n\n" 902 val _ = map (fn x => print (" " ^ x ^ "\n")) code 903 val _ = print "\n\n" 904 in () end 905 906 907(* code heap -- write iCONST_NUM, same as iCONST_SYM *) 908 909val (mc_write_num_spec,mc_write_num_def) = basic_decompile_strings x64_tools "mc_write_num" 910 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 911 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 912 (assemble "x64" ` 913 mov r2,[r7-96] 914 mov r1,r8 915 mov BYTE [r2+0],72 916 mov BYTE [r2+1],-123 917 mov BYTE [r2+2],-37 918 mov BYTE [r2+3],62 919 mov BYTE [r2+4],72 920 mov BYTE [r2+5],117 921 mov BYTE [r2+6],9 922 mov BYTE [r2+7],-117 923 mov BYTE [r2+8],-47 924 mov BYTE [r2+9],72 925 mov BYTE [r2+10],-1 926 mov BYTE [r2+11],-89 927 mov BYTE [r2+12],56 928 mov BYTE [r2+13],-1 929 mov BYTE [r2+14],-1 930 mov BYTE [r2+15],-1 931 mov BYTE [r2+16],72 932 mov BYTE [r2+17],-1 933 mov BYTE [r2+18],-53 934 mov BYTE [r2+19],68 935 mov BYTE [r2+20],-119 936 mov BYTE [r2+21],4 937 mov BYTE [r2+22],-97 938 mov BYTE [r2+23],65 939 mov BYTE [r2+24],-72 940 mov BYTE [r2+25],r1b 941 shr r1,8 942 mov BYTE [r2+26],r1b 943 shr r1,8 944 mov BYTE [r2+27],r1b 945 shr r1,8 946 mov BYTE [r2+28],r1b 947 mov r2,[r7-88] 948 sub r2,29 949 add QWORD [r7-96],29 950 mov [r7-88],r2 951 mov r1d,1 952 `) 953 954val const_num_blast = blastLib.BBLAST_PROVE 955 ``(w2w (w2w (w:word30) << 2 + 0x1w:word32) = w2w w << 2 + 0x1w:word64) /\ 956 (w2w (w2w (v:29 word) << 3 + 0x3w:word32) = w2w v << 3 + 0x3w:word64) /\ 957 (w2w ((ww:word32) >>> 8) = (w2w ((w2w ww >>> 8):word64)):word8) /\ 958 (w2w ((ww:word32) >>> 16) = (w2w ((w2w ww >>> 16):word64)):word8) /\ 959 (w2w ((ww:word32) >>> 24) = (w2w ((w2w ww >>> 24):word64)):word8)`` 960 961val inst = ``iCONST_NUM (getVal x0)`` 962val mc_write_num_thm = prove( 963 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==> 964 ?fi di tw2i. 965 mc_write_num_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 966 (mc_write_num (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 967 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 968 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_write_num_def,LET_DEF] 969 \\ IMP_RES_TAC lisp_inv_ds_read 970 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 971 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 972 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 973 \\ SIMP_TAC std_ss [CONJ_ASSOC] 974 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 975 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 976 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 977 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 978 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 979 \\ STRIP_TAC THEN1 980 (Q.ABBREV_TAC `cs2 = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex] ++ cs` 981 \\ `LENGTH cs2 = 18` by 982 (Q.UNABBREV_TAC `cs2` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 983 \\ IMP_RES_TAC expand_list2 984 \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC)) 985 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS] 986 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 987 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 988 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 989 ref_static_APPEND,ref_static_def,LENGTH,mc_code_heap_blast,IMMEDIATE32_def] 990 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 991 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 992 \\ SEP_WRITE_TAC) 993 \\ ASM_SIMP_TAC std_ss [IMMEDIATE32_def,APPEND,LENGTH,LSR_ADD] 994 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ] 995 \\ EXISTS_TAC ``bs ++ [^inst]`` 996 \\ EXISTS_TAC ``DROP (bc_length ^inst) (hs:word8 list)`` 997 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,IMMEDIATE32_def,APPEND] 998 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND,bc_symbols_ok_APPEND,bc_ref_def, 999 bc_symbols_ok_def,SND_WRITE_CODE,bc_length_def,word_arith_lemma1] 1000 \\ FULL_SIMP_TAC std_ss [LENGTH,bs2bytes_APPEND] 1001 \\ FULL_SIMP_TAC std_ss [bs2bytes_def,APPEND_NIL,bc_ref_def,IMMEDIATE32_def,APPEND] 1002 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr xssss = yssss` (ASSUME_TAC o GSYM) 1003 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11] 1004 \\ Q.PAT_X_ASSUM `isVal x0` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [isVal_thm] 1005 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt,lisp_x_def,getVal_def] 1006 \\ FULL_SIMP_TAC std_ss [const_num_blast] 1007 \\ `w2w ((n2w a):word30) = (n2w a):word64` by 1008 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1009 \\ FULL_SIMP_TAC std_ss [] 1010 \\ IMP_RES_TAC bc_length_lemma 1011 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [bc_length_def,bc_ref_def, 1012 LENGTH,SUC_EQ_LENGTH,APPEND,IMMEDIATE32_def] o SPEC inst) 1013 \\ FULL_SIMP_TAC std_ss [DROP_CONS,DROP_0] 1014 \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM) 1015 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM ADD_ASSOC] 1016 \\ IMP_RES_TAC write_lemma \\ ASM_SIMP_TAC std_ss [] 1017 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1018 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def] 1019 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC,LENGTH_APPEND,LENGTH,GSYM ADD_ASSOC, 1020 word_arith_lemma1] 1021 \\ IMP_RES_TAC LENGTH_bs2bytes \\ FULL_SIMP_TAC std_ss [] 1022 \\ Q.PAT_X_ASSUM `xxx (fun2set (d,dd))` ASSUME_TAC 1023 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1024 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 1025 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1026 \\ `(1 + 4 * a) < 2**32` by (FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 1027 \\ FULL_SIMP_TAC std_ss [] 1028 \\ `w2w ((n2w (1 + 4 * a)):word32) = (n2w (1 + 4 * a)):word64` by 1029 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1030 \\ ASM_SIMP_TAC std_ss [] 1031 \\ SEP_W_TAC 1032 \\ `(1 + 4 * a) < 2**64` by (FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 1033 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1034 |> SIMP_RULE std_ss []; 1035 1036val LIST_FIND_SOME_IMP = prove( 1037 ``!xs x a i. (LIST_FIND x a xs = SOME i) ==> MEM a xs``, 1038 Induct \\ SRW_TAC [] [LIST_FIND_def,MEM] \\ RES_TAC \\ ASM_SIMP_TAC std_ss []); 1039 1040val inst = ``iCONST_SYM (getSym x0)`` 1041val mc_write_sym_thm = prove( 1042 ``^LISP /\ 0x100w <+ EL 3 ds ==> isSym x0 ==> 1043 ?fi di tw2i. 1044 mc_write_num_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1045 (mc_write_num (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1046 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1047 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_write_num_def,LET_DEF] 1048 \\ IMP_RES_TAC lisp_inv_ds_read 1049 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 1050 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1051 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 1052 \\ SIMP_TAC std_ss [CONJ_ASSOC] 1053 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1054 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 1055 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1056 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 1057 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 1058 \\ STRIP_TAC THEN1 1059 (Q.ABBREV_TAC `cs2 = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex] ++ cs` 1060 \\ `LENGTH cs2 = 18` by 1061 (Q.UNABBREV_TAC `cs2` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 1062 \\ IMP_RES_TAC expand_list2 1063 \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC)) 1064 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS] 1065 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 1066 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 1067 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 1068 ref_static_APPEND,ref_static_def,LENGTH,mc_code_heap_blast,IMMEDIATE32_def] 1069 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 1070 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1071 \\ SEP_WRITE_TAC) 1072 \\ ASM_SIMP_TAC std_ss [IMMEDIATE32_def,APPEND,LENGTH,LSR_ADD] 1073 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ] 1074 \\ EXISTS_TAC ``bs ++ [^inst]`` 1075 \\ EXISTS_TAC ``DROP (bc_length ^inst) (hs:word8 list)`` 1076 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,IMMEDIATE32_def,APPEND] 1077 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND,bc_symbols_ok_APPEND,bc_ref_def, 1078 bc_symbols_ok_def,SND_WRITE_CODE,bc_length_def,word_arith_lemma1] 1079 \\ FULL_SIMP_TAC std_ss [LENGTH,bs2bytes_APPEND] 1080 \\ FULL_SIMP_TAC std_ss [bs2bytes_def,APPEND_NIL,bc_ref_def,IMMEDIATE32_def,APPEND] 1081 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr xssss = yssss` (ASSUME_TAC o GSYM) 1082 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11] 1083 \\ Q.PAT_X_ASSUM `isSym x0` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [isSym_thm] 1084 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt,lisp_x_def,getSym_def] 1085 \\ IMP_RES_TAC LIST_FIND_SOME_IMP 1086 \\ FULL_SIMP_TAC std_ss [const_num_blast] 1087 \\ `w2w ((n2w k):29 word) = (n2w k):word64` by 1088 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1089 \\ FULL_SIMP_TAC std_ss [] 1090 \\ IMP_RES_TAC bc_length_lemma 1091 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [bc_length_def,bc_ref_def, 1092 LENGTH,SUC_EQ_LENGTH,APPEND,IMMEDIATE32_def] o SPEC inst) 1093 \\ FULL_SIMP_TAC std_ss [DROP_CONS,DROP_0] 1094 \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM) 1095 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM ADD_ASSOC] 1096 \\ IMP_RES_TAC write_lemma \\ ASM_SIMP_TAC std_ss [] 1097 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1098 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def] 1099 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC,LENGTH_APPEND,LENGTH,GSYM ADD_ASSOC, 1100 word_arith_lemma1] 1101 \\ IMP_RES_TAC LENGTH_bs2bytes \\ FULL_SIMP_TAC std_ss [] 1102 \\ Q.PAT_X_ASSUM `xxx (fun2set (d,dd))` ASSUME_TAC 1103 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1104 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 1105 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1106 \\ `(3 + 8 * k) < 2**32` by (FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 1107 \\ FULL_SIMP_TAC std_ss [] 1108 \\ `w2w ((n2w (3 + 8 * k)):word32) = (n2w (3 + 8 * k)):word64` by 1109 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1110 \\ ASM_SIMP_TAC std_ss [] \\ SEP_W_TAC 1111 \\ `(3 + 8 * k) < 2**64` by (FULL_SIMP_TAC wstd_ss [] \\ DECIDE_TAC) 1112 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1113 |> SIMP_RULE std_ss []; 1114 1115 1116(* code heap -- write iJUMP, iJNIL, iCALL *) 1117 1118val (mc_write_jump_spec,mc_write_jump_def) = basic_decompile_strings x64_tools "mc_write_jump" 1119 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1120 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1121 (assemble "x64" ` 1122 mov r2,[r7-96] 1123 mov r1,r8 1124 shr r1,2 1125 add r1,[r7-160] 1126 sub r1,r2 1127 sub r1,6 1128 mov BYTE [r2],72 1129 mov BYTE [r2+1],-23 1130 mov BYTE [r2+2],r1b 1131 shr r1,8 1132 mov BYTE [r2+3],r1b 1133 shr r1,8 1134 mov BYTE [r2+4],r1b 1135 shr r1,8 1136 mov BYTE [r2+5],r1b 1137 mov r2,[r7-88] 1138 sub r2,6 1139 add QWORD [r7-96],6 1140 mov [r7-88],r2 1141 mov r1d,1 1142 `) 1143 1144val (mc_write_call_spec,mc_write_call_def) = basic_decompile_strings x64_tools "mc_write_call" 1145 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1146 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1147 (assemble "x64" ` 1148 mov r2,[r7-96] 1149 mov r1,r8 1150 shr r1,2 1151 add r1,[r7-160] 1152 sub r1,r2 1153 sub r1,6 1154 mov BYTE [r2],72 1155 mov BYTE [r2+1],-24 1156 mov BYTE [r2+2],r1b 1157 shr r1,8 1158 mov BYTE [r2+3],r1b 1159 shr r1,8 1160 mov BYTE [r2+4],r1b 1161 shr r1,8 1162 mov BYTE [r2+5],r1b 1163 mov r2,[r7-88] 1164 sub r2,6 1165 add QWORD [r7-96],6 1166 mov [r7-88],r2 1167 mov r1d,1 1168 `) 1169 1170val (mc_write_jnil_spec,mc_write_jnil_def) = basic_decompile_strings x64_tools "mc_write_jnil" 1171 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1172 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1173 (assemble "x64" ` 1174 mov r2,[r7-96] 1175 mov r1,r8 1176 shr r1,2 1177 add r1,[r7-160] 1178 sub r1,r2 1179 sub r1,21 1180 mov BYTE [r2+0],77 1181 mov BYTE [r2+1],-117 1182 mov BYTE [r2+2],-56 1183 mov BYTE [r2+3],68 1184 mov BYTE [r2+4],-117 1185 mov BYTE [r2+5],4 1186 mov BYTE [r2+6],-97 1187 mov BYTE [r2+7],72 1188 mov BYTE [r2+8],-1 1189 mov BYTE [r2+9],-61 1190 mov BYTE [r2+10],73 1191 mov BYTE [r2+11],-125 1192 mov BYTE [r2+12],-7 1193 mov BYTE [r2+13],3 1194 mov BYTE [r2+14],72 1195 mov BYTE [r2+15],15 1196 mov BYTE [r2+16],-124 1197 mov BYTE [r2+17],r1b 1198 shr r1,8 1199 mov BYTE [r2+18],r1b 1200 shr r1,8 1201 mov BYTE [r2+19],r1b 1202 shr r1,8 1203 mov BYTE [r2+20],r1b 1204 mov r2,[r7-88] 1205 sub r2,21 1206 add QWORD [r7-96],21 1207 mov [r7-88],r2 1208 mov r1d,1 1209 `) 1210 1211val mc_write_jump_blast = blastLib.BBLAST_PROVE 1212 ``((w2w:word64->word8) ((w2w:word32->word64) (w - v) >>> 24) = w2w ((w2w w - (w2w:word32->word64) v) >>> 24)) /\ 1213 ((w2w:word64->word8) ((w2w:word32->word64) (w - v) >>> 16) = w2w ((w2w w - (w2w:word32->word64) v) >>> 16)) /\ 1214 ((w2w:word64->word8) ((w2w:word32->word64) (w - v) >>> 8) = w2w ((w2w w - (w2w:word32->word64) v) >>> 8)) /\ 1215 ((w2w:word64->word8) ((w2w:word32->word64) (w - v)) = w2w ((w2w w - (w2w:word32->word64) v))) /\ 1216 ((w2w:word32->word8) (x - y) = (w2w:word64->word8) (w2w x - w2w y))`` 1217 1218fun iJUMP_TAC inst = 1219 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_write_jump_def,mc_write_call_def,mc_write_jnil_def,LET_DEF] 1220 \\ IMP_RES_TAC lisp_inv_ds_read 1221 \\ IMP_RES_TAC lisp_inv_cs_read 1222 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 1223 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1224 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 1225 \\ SIMP_TAC std_ss [CONJ_ASSOC] 1226 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1227 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 1228 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1229 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 1230 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 1231 \\ STRIP_TAC THEN1 1232 (Q.ABBREV_TAC `cs2 = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex] ++ cs` 1233 \\ `LENGTH cs2 = 18` by 1234 (Q.UNABBREV_TAC `cs2` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 1235 \\ IMP_RES_TAC expand_list2 1236 \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC)) 1237 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS] 1238 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 1239 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 1240 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 1241 ref_static_APPEND,ref_static_def,LENGTH,mc_code_heap_blast,IMMEDIATE32_def] 1242 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 1243 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1244 \\ SEP_WRITE_TAC) 1245 \\ ASM_SIMP_TAC std_ss [IMMEDIATE32_def,APPEND,LENGTH,LSR_ADD] 1246 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ] 1247 \\ EXISTS_TAC ``bs ++ [^inst]`` 1248 \\ EXISTS_TAC ``DROP (bc_length ^inst) (hs:word8 list)`` 1249 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,IMMEDIATE32_def,APPEND] 1250 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND,bc_symbols_ok_APPEND,bc_ref_def, 1251 bc_symbols_ok_def,SND_WRITE_CODE,bc_length_def,word_arith_lemma1] 1252 \\ FULL_SIMP_TAC std_ss [LENGTH,bs2bytes_APPEND] 1253 \\ FULL_SIMP_TAC std_ss [bs2bytes_def,APPEND_NIL,bc_ref_def,IMMEDIATE32_def,APPEND] 1254 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr xssss = yssss` (ASSUME_TAC o GSYM) 1255 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11] 1256 \\ Q.PAT_X_ASSUM `isVal x0` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [isVal_thm] 1257 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt,lisp_x_def,getVal_def] 1258 \\ FULL_SIMP_TAC std_ss [const_num_blast] 1259 \\ `w2w ((n2w a):word30) = (n2w a):word64` by 1260 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1261 \\ FULL_SIMP_TAC std_ss [] 1262 \\ IMP_RES_TAC bc_length_lemma 1263 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [bc_length_def,bc_ref_def, 1264 LENGTH,SUC_EQ_LENGTH,APPEND,IMMEDIATE32_def] o SPEC inst) 1265 \\ FULL_SIMP_TAC std_ss [DROP_CONS,DROP_0] 1266 \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM) 1267 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM ADD_ASSOC] 1268 \\ IMP_RES_TAC write_lemma \\ ASM_SIMP_TAC std_ss [] 1269 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1270 \\ `(n2w a << 2 + 0x1w) >>> 2 = (n2w a):word64` by 1271 (ONCE_REWRITE_TAC [WORD_ADD_COMM] \\ SIMP_TAC std_ss [WORD_ADD_SUB] 1272 \\ `n2w a <+ n2w (2**30):word64` by 1273 (`a < (2**64)` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 1274 \\ FULL_SIMP_TAC wstd_ss [word_lo_n2w]) 1275 \\ POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`(n2w a):word64`,`w`) 1276 \\ blastLib.BBLAST_TAC) 1277 \\ ASM_SIMP_TAC std_ss [WORD_SUB_PLUS,WORD_ADD_SUB] 1278 \\ `code_length bs = code_ptr code` by METIS_TAC [WRITE_CODE_IMP_code_length,ADD_0] 1279 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def] 1280 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC,LENGTH_APPEND,LENGTH,GSYM ADD_ASSOC, 1281 word_arith_lemma1] 1282 \\ IMP_RES_TAC LENGTH_bs2bytes \\ FULL_SIMP_TAC std_ss [] 1283 \\ Q.PAT_X_ASSUM `xxx (fun2set (d,dd))` ASSUME_TAC 1284 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1285 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 1286 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1287 \\ FULL_SIMP_TAC std_ss [mc_write_jump_blast] 1288 \\ `((w2w:word32->word64) (n2w a) = n2w a) /\ 1289 ((w2w:word32->word64) (n2w (code_ptr code)) = n2w (code_ptr code)) /\ 1290 ((w2w:word32->word64) (n2w (code_ptr code + 6)) = n2w (code_ptr code + 6)) /\ 1291 ((w2w:word32->word64) (n2w (code_ptr code + 21)) = n2w (code_ptr code + 21))` by 1292 (`a < 4294967296 /\ code_ptr code < 4294967296 /\ 1293 code_ptr code + 6 < 4294967296 /\ code_ptr code + 21 < 4294967296` by DECIDE_TAC 1294 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11]) 1295 \\ ASM_SIMP_TAC std_ss [] 1296 \\ SEP_WRITE_TAC 1297 1298val inst = ``iJUMP (getVal x0)`` 1299val mc_write_jump_thm = prove( 1300 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==> 1301 ?fi di tw2i. 1302 mc_write_jump_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1303 (mc_write_jump (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1304 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1305 iJUMP_TAC inst) |> SIMP_RULE std_ss []; 1306 1307val inst = ``iCALL (getVal x0)`` 1308val mc_write_call_thm = prove( 1309 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==> 1310 ?fi di tw2i. 1311 mc_write_call_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1312 (mc_write_call (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1313 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1314 iJUMP_TAC inst) |> SIMP_RULE std_ss []; 1315 1316val inst = ``iJNIL (getVal x0)`` 1317val mc_write_jnil_thm = prove( 1318 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==> 1319 ?fi di tw2i. 1320 mc_write_jnil_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1321 (mc_write_jnil (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1322 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1323 iJUMP_TAC inst) |> SIMP_RULE std_ss []; 1324 1325 1326(* code heap -- write iPOPS, iSTORE, iLOAD *) 1327 1328val (mc_write_pops_spec,mc_write_pops_def) = basic_decompile_strings x64_tools "mc_write_pops" 1329 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1330 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1331 (assemble "x64" ` 1332 mov r2,[r7-96] 1333 mov r1,r8 1334 shr r1,2 1335 mov BYTE [r2+0],72 1336 mov BYTE [r2+1],-127 1337 mov BYTE [r2+2],-61 1338 mov BYTE [r2+3],r1b 1339 shr r1,8 1340 mov BYTE [r2+4],r1b 1341 shr r1,8 1342 mov BYTE [r2+5],r1b 1343 shr r1,8 1344 mov BYTE [r2+6],r1b 1345 mov r2,[r7-88] 1346 sub r2,7 1347 add QWORD [r7-96],7 1348 mov [r7-88],r2 1349 mov r1d,1 1350 `) 1351 1352val (mc_write_store_spec,mc_write_store_def) = basic_decompile_strings x64_tools "mc_write_store" 1353 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1354 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1355 (assemble "x64" ` 1356 mov r2,[r7-96] 1357 mov r1,r8 1358 sub r1,1 1359 mov BYTE [r2+0],68 1360 mov BYTE [r2+1],-119 1361 mov BYTE [r2+2],-124 1362 mov BYTE [r2+3],-97 1363 mov BYTE [r2+4],r1b 1364 shr r1,8 1365 mov BYTE [r2+5],r1b 1366 shr r1,8 1367 mov BYTE [r2+6],r1b 1368 shr r1,8 1369 mov BYTE [r2+7],r1b 1370 mov BYTE [r2+8],68 1371 mov BYTE [r2+9],-117 1372 mov BYTE [r2+10],4 1373 mov BYTE [r2+11],-97 1374 mov BYTE [r2+12],72 1375 mov BYTE [r2+13],-1 1376 mov BYTE [r2+14],-61 1377 mov r2,[r7-88] 1378 sub r2,15 1379 add QWORD [r7-96],15 1380 mov [r7-88],r2 1381 mov r1d,1 1382 `) 1383 1384val (mc_write_load_spec,mc_write_load_def) = basic_decompile_strings x64_tools "mc_write_load" 1385 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1386 ``(r1:word64,r2:word64,r7:word64,r8:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1387 (assemble "x64" ` 1388 mov r2,[r7-96] 1389 mov r1,r8 1390 sub r1,1 1391 mov BYTE [r2+0],72 1392 mov BYTE [r2+1],-123 1393 mov BYTE [r2+2],-37 1394 mov BYTE [r2+3],62 1395 mov BYTE [r2+4],72 1396 mov BYTE [r2+5],117 1397 mov BYTE [r2+6],9 1398 mov BYTE [r2+7],-117 1399 mov BYTE [r2+8],-47 1400 mov BYTE [r2+9],72 1401 mov BYTE [r2+10],-1 1402 mov BYTE [r2+11],-89 1403 mov BYTE [r2+12],56 1404 mov BYTE [r2+13],-1 1405 mov BYTE [r2+14],-1 1406 mov BYTE [r2+15],-1 1407 mov BYTE [r2+16],72 1408 mov BYTE [r2+17],-1 1409 mov BYTE [r2+18],-53 1410 mov BYTE [r2+19],68 1411 mov BYTE [r2+20],-119 1412 mov BYTE [r2+21],4 1413 mov BYTE [r2+22],-97 1414 mov BYTE [r2+23],68 1415 mov BYTE [r2+24],-117 1416 mov BYTE [r2+25],-124 1417 mov BYTE [r2+26],-97 1418 mov BYTE [r2+27],r1b 1419 shr r1,8 1420 mov BYTE [r2+28],r1b 1421 shr r1,8 1422 mov BYTE [r2+29],r1b 1423 shr r1,8 1424 mov BYTE [r2+30],r1b 1425 mov r2,[r7-88] 1426 sub r2,31 1427 add QWORD [r7-96],31 1428 mov [r7-88],r2 1429 mov r1d,1 1430 `) 1431 1432val mc_write_pops_blast = blastLib.BBLAST_PROVE 1433 ``((w2w:word32->word8) x = (w2w:word64->word8) (w2w x))`` 1434 1435fun iPOPS_TAC inst = 1436 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_write_pops_def,mc_write_load_def,mc_write_store_def,LET_DEF] 1437 \\ IMP_RES_TAC lisp_inv_ds_read 1438 \\ IMP_RES_TAC lisp_inv_cs_read 1439 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 1440 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1441 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 1442 \\ SIMP_TAC std_ss [CONJ_ASSOC] 1443 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1444 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 1445 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1446 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 1447 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 1448 \\ STRIP_TAC THEN1 1449 (Q.ABBREV_TAC `cs2 = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex] ++ cs` 1450 \\ `LENGTH cs2 = 18` by 1451 (Q.UNABBREV_TAC `cs2` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 1452 \\ IMP_RES_TAC expand_list2 1453 \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC)) 1454 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS] 1455 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 1456 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 1457 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 1458 ref_static_APPEND,ref_static_def,LENGTH,mc_code_heap_blast,IMMEDIATE32_def] 1459 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 1460 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1461 \\ SEP_WRITE_TAC) 1462 \\ ASM_SIMP_TAC std_ss [IMMEDIATE32_def,APPEND,LENGTH, 1463 Q.SPECL [`w`,`8`,`8`] LSR_ADD, Q.SPECL [`w`,`8`,`16`] LSR_ADD] 1464 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ] 1465 \\ EXISTS_TAC ``bs ++ [^inst]`` 1466 \\ EXISTS_TAC ``DROP (bc_length ^inst) (hs:word8 list)`` 1467 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,IMMEDIATE32_def,APPEND] 1468 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND,bc_symbols_ok_APPEND,bc_ref_def, 1469 bc_symbols_ok_def,SND_WRITE_CODE,bc_length_def,word_arith_lemma1] 1470 \\ FULL_SIMP_TAC std_ss [LENGTH,bs2bytes_APPEND] 1471 \\ FULL_SIMP_TAC std_ss [bs2bytes_def,APPEND_NIL,bc_ref_def,IMMEDIATE32_def,APPEND] 1472 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr xssss = yssss` (ASSUME_TAC o GSYM) 1473 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,CONS_11] 1474 \\ Q.PAT_X_ASSUM `isVal x0` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [isVal_thm] 1475 \\ FULL_SIMP_TAC std_ss [ref_heap_addr_alt,lisp_x_def,getVal_def] 1476 \\ FULL_SIMP_TAC std_ss [const_num_blast] 1477 \\ `w2w ((n2w a):word30) = (n2w a):word64` by 1478 (ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1479 \\ FULL_SIMP_TAC std_ss [] 1480 \\ IMP_RES_TAC bc_length_lemma 1481 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [bc_length_def,bc_ref_def, 1482 LENGTH,SUC_EQ_LENGTH,APPEND,IMMEDIATE32_def] o SPEC inst) 1483 \\ FULL_SIMP_TAC std_ss [DROP_CONS,DROP_0] 1484 \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM) 1485 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM ADD_ASSOC] 1486 \\ IMP_RES_TAC write_lemma \\ ASM_SIMP_TAC std_ss [] 1487 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1488 \\ `(n2w a << 2 + 0x1w) >>> 2 = (n2w a):word64` by 1489 (ONCE_REWRITE_TAC [WORD_ADD_COMM] \\ SIMP_TAC std_ss [WORD_ADD_SUB] 1490 \\ `n2w a <+ n2w (2**30):word64` by 1491 (`a < (2**64)` by (FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 1492 \\ FULL_SIMP_TAC wstd_ss [word_lo_n2w]) 1493 \\ POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`(n2w a):word64`,`w`) 1494 \\ blastLib.BBLAST_TAC) 1495 \\ ASM_SIMP_TAC std_ss [WORD_SUB_PLUS,WORD_ADD_SUB] 1496 \\ SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w] 1497 \\ `(w2w:word32->word64) (n2w (4 * a)) = n2w (4 * a)` by 1498 (`(4 * a) < 4294967296` by DECIDE_TAC 1499 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11]) 1500 \\ ASM_SIMP_TAC std_ss [] 1501 \\ `code_length bs = code_ptr code` by METIS_TAC [WRITE_CODE_IMP_code_length,ADD_0] 1502 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def] 1503 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC,LENGTH_APPEND,LENGTH,GSYM ADD_ASSOC, 1504 word_arith_lemma1] 1505 \\ IMP_RES_TAC LENGTH_bs2bytes \\ FULL_SIMP_TAC std_ss [] 1506 \\ Q.PAT_X_ASSUM `xxx (fun2set (d,dd))` ASSUME_TAC 1507 \\ SEP_R_TAC \\ ASM_SIMP_TAC std_ss [] 1508 \\ FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w,word_add_n2w] 1509 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1510 \\ FULL_SIMP_TAC std_ss [mc_write_jump_blast] 1511 \\ `((w2w:word32->word64) (n2w a) = n2w a) /\ 1512 ((w2w:word32->word64) (n2w (code_ptr code)) = n2w (code_ptr code))` by 1513 (`a < 4294967296 /\ code_ptr code < 4294967296` by DECIDE_TAC 1514 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,n2w_11]) 1515 \\ ASM_SIMP_TAC std_ss [mc_write_pops_blast] 1516 \\ SEP_WRITE_TAC 1517 1518 1519val inst = ``iPOPS (getVal x0)`` 1520val mc_write_pops_thm = prove( 1521 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 ==> 1522 ?fi di tw2i. 1523 mc_write_pops_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1524 (mc_write_pops (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1525 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1526 iPOPS_TAC inst) |> SIMP_RULE std_ss []; 1527 1528val inst = ``iSTORE (getVal x0)`` 1529val mc_write_store_thm = prove( 1530 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 /\ getVal x0 < 536870912 ==> 1531 ?fi di tw2i. 1532 mc_write_store_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1533 (mc_write_store (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1534 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1535 iPOPS_TAC inst) |> SIMP_RULE std_ss []; 1536 1537val inst = ``iLOAD (getVal x0)`` 1538val mc_write_load_thm = prove( 1539 ``^LISP /\ 0x100w <+ EL 3 ds ==> isVal x0 /\ getVal x0 < 536870912 ==> 1540 ?fi di tw2i. 1541 mc_write_load_pre (tw1,tw2,sp,w2w w0,df,f,dd,d) /\ 1542 (mc_write_load (tw1,tw2,sp,w2w w0,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,df,fi,dd,di)) /\ 1543 let (code,f,d,tw2,ds) = (WRITE_CODE code [^inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length ^inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length ^inst)) ds)) in ^LISP``, 1544 iPOPS_TAC inst) |> SIMP_RULE std_ss []; 1545 1546 1547(* code heap -- write const instructions *) 1548 1549local 1550val ready_formats = let (* derive Hoare triples for mov BYTE [r2+???],??? *) 1551 fun foo i = let 1552 val e = x64_encodeLib.x64_encode ("mov BYTE [r2+"^(int_to_string i)^"],34") 1553 val e = String.substring(e,0,size(e)-2) 1554 val (x,_) = x64_spec e 1555 in (e,x) end 1556 fun genlist i n f = if i = n then [] else 1557 (print (int_to_string (256-i) ^ " "); f i :: genlist (i+1) n f) 1558 in genlist 0 256 foo end 1559in 1560fun instantiate_ready_format s = let 1561 val e = String.substring(s,0,size(s)-2) 1562 val t = String.substring(s,size(s)-2,2) 1563 fun list_find x [] = fail() 1564 | list_find x ((y,z)::xs) = if x = y then z else list_find x xs 1565 val (th,i,j) = list_find e ready_formats 1566 val n = numSyntax.mk_numeral(Arbnum.fromHexString t) 1567 val th = INST [mk_var("imm8",``:word8``)|->``(n2w ^n):word8``] th 1568 val tm = find_term (can (match_term ``SIGN_EXTEND x y z MOD 256``)) (concl th) 1569 val th = RW [EVAL tm] th 1570 in (th,i,j) end handle Subsript => fail() 1571end; 1572 1573fun get_code_for_bc_inst inst = let 1574 val ys = EVAL (mk_comb(``bc_ref (i,sym)``,inst)) 1575 |> concl |> dest_eq |> snd |> listSyntax.dest_list |> fst 1576 |> map (fn tm => if wordsSyntax.is_w2w tm then ``0w:word64`` else tm) 1577 |> map (numSyntax.int_of_term o cdr) 1578 |> map (fn n => n mod 256) 1579 val xs = ys |> map (fn x => if x < 128 then x else x - 256) 1580 val enc = x64_encodeLib.x64_encode 1581 fun my_int_to_string n = if n < 0 then "-" ^ int_to_string (0-n) else int_to_string n 1582 fun encs (i,[]) = [] 1583 | encs (i,(x::xs)) = ("mov BYTE [r2+"^ int_to_string i ^"]," ^ my_int_to_string x) 1584 :: encs (i+1,xs) 1585 val l = length xs 1586 val (c1,c2,c3) = (["mov r2,[r7-96]"], encs (0,xs), 1587 ["mov r2,[r7-88]"] @ 1588 ["sub r2," ^ int_to_string l] @ 1589 ["add QWORD [r7-96]," ^ int_to_string l] @ 1590 ["mov [r7-88],r2"]) 1591 in (map enc c1 @ map enc c2 @ map enc c3,ys) end 1592 1593fun straight_line_decompile func_name code in_out_vars = let 1594 val _ = print "\nStraight-line decompile, " 1595 val (spec,_,sts,pc) = x64_tools 1596 fun my_spec s = (instantiate_ready_format s,NONE) handle HOL_ERR _ => spec s 1597 fun simple_spec s = let val ((th,_,_),_) = my_spec s in HIDE_STATUS_RULE true sts th end; 1598 val counter = ref 0 1599 val total = length code 1600 fun next x = (counter := 1+(!counter); print ("\n" ^ int_to_string (!counter) ^ " of " ^ int_to_string total ^ " "); x) 1601 val thms = map simple_spec code 1602 val th = SPEC_COMPOSE_RULE thms 1603 val th = SIMP_RULE (std_ss++sep_cond_ss) [] th 1604 val th = Q.INST [`rip`|->`p`] th 1605 val (_,p,_,q) = dest_spec (concl (UNDISCH_ALL (RW [progTheory.SPEC_MOVE_COND] th))) 1606 val ps = filter (not o can dest_sep_hide) (list_dest dest_star p) 1607 val qs = filter (not o can dest_sep_hide) (list_dest dest_star q) 1608 val ps = filter (fn tm => (car tm !~ pc) handle HOL_ERR _ => true) ps 1609 val qs = filter (fn tm => (car tm !~ pc) handle HOL_ERR _ => true) qs 1610 fun safe_car tm = car tm handle HOL_ERR _ => tm 1611 val sorter = sort (fn t1 => fn t2 => term_to_string (safe_car t1) <= term_to_string (safe_car t2)) 1612 val ps = sorter ps 1613 val qs = sorter qs 1614 val px = list_mk_star(ps)(type_of (hd ps)) 1615 val qx = list_mk_star(qs)(type_of (hd qs)) 1616 val s = fst (match_term px qx) 1617 val result = subst s in_out_vars 1618 val ty = type_of (pairSyntax.mk_pabs(in_out_vars,in_out_vars)) 1619 val def = new_definition(func_name,mk_eq(mk_comb(mk_var(func_name,ty),in_out_vars),result)) 1620 val ty = type_of (pairSyntax.mk_pabs(in_out_vars,``T:bool``)) 1621 val pre_result = th |> RW [progTheory.SPEC_MOVE_COND] |> concl |> dest_imp |> fst 1622 handle HOL_ERR _ => ``T`` 1623 val pre = new_definition(func_name ^ "_pre",mk_eq(mk_comb(mk_var(func_name ^ "_pre",ty),in_out_vars),pre_result)) 1624 val th = RW [GSYM pre] th 1625 val new_q = subst (map (fn {redex= x, residue=y} => y |-> x) s) q 1626 val rhs = def |> SPEC_ALL |> concl |> dest_eq |> fst 1627 val new_q = pairSyntax.mk_anylet([(in_out_vars,rhs)],new_q) 1628 val (th,goal) = SPEC_WEAKEN_RULE th new_q 1629 val lemma = prove(goal,SIMP_TAC (std_ss++star_ss) [LET_DEF,def,SEP_IMP_REFL]) 1630 val th = MP th lemma 1631 val x = CONJ (SPEC_ALL def) (SPEC_ALL pre) 1632 val _ = print "done!\n" 1633 in (th,x) end; 1634 1635val one_write_list_def = Define ` 1636 (one_write_list a [] f = f) /\ 1637 (one_write_list (a:word64) (x::xs) f = one_write_list (a + 1w) xs ((a =+ x) f))`; 1638 1639val one_address_list_def = Define ` 1640 (one_address_list a [] = []) /\ 1641 (one_address_list (a:word64) (x::xs) = a::one_address_list (a+1w) xs)`; 1642 1643val STAR5_LEMMA = prove( 1644 ``STAR x1 x2 * x3 * x4 * x5 = x1 * x3 * x2 * x4 * x5``, 1645 SIMP_TAC (std_ss++star_ss) []); 1646 1647val one_write_list_lemma = prove( 1648 ``!xs b a x y p q d. 1649 (p * one (a,x) * one_byte_list b (MAP FST xs) * q) 1650 (fun2set (one_write_list b (MAP FST xs) d,dd)) ==> 1651 (p * one (a,y) * one_byte_list b (MAP FST xs) * q) 1652 (fun2set (one_write_list b (MAP FST xs) ((a =+ y) d),dd))``, 1653 Induct \\ SIMP_TAC std_ss [MAP,one_write_list_def] 1654 THEN1 (REPEAT STRIP_TAC \\ SEP_WRITE_TAC) 1655 \\ FULL_SIMP_TAC std_ss [one_write_list_def,one_byte_list_def,STAR_ASSOC] 1656 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1657 \\ ONCE_REWRITE_TAC [STAR5_LEMMA] 1658 \\ REPEAT STRIP_TAC \\ RES_TAC \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `y`) 1659 \\ `~(b = a)` by SEP_NEQ_TAC \\ METIS_TAC [UPDATE_COMMUTES]); 1660 1661val one_write_list_thm = prove( 1662 ``!xs p q d a. 1663 (p * one_byte_list a (MAP SND xs) * q) (fun2set (d,dd)) ==> 1664 (p * one_byte_list a (MAP FST xs) * q) 1665 (fun2set (one_write_list a (MAP FST xs) d,dd)) /\ 1666 EVERY (\a. a IN dd) (one_address_list a xs)``, 1667 Induct \\ SIMP_TAC std_ss [MAP,one_byte_list_def,one_write_list_def, 1668 STAR_ASSOC,one_address_list_def,EVERY_DEF] \\ REPEAT STRIP_TAC \\ RES_TAC 1669 \\ SEP_R_TAC \\ IMP_RES_TAC one_write_list_lemma \\ FULL_SIMP_TAC std_ss []); 1670 1671 1672fun generate_and_verify_write_const (name,inst) = let 1673 val _ = print ("\n\n"^name^"\n\n") 1674 val (code,ys) = get_code_for_bc_inst inst 1675 val func_name = ("mc_write_" ^ name) 1676 val in_out_vars = 1677 ``(r2:word64,r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)`` 1678 val (spec_thm,def_thm) = straight_line_decompile name code in_out_vars 1679 val ds = map (car o fst o dest_eq o concl) (CONJUNCTS def_thm) 1680 val def = el 1 ds 1681 val pre = el 2 ds 1682 val goal = 1683 ``^LISP /\ 0x100w <+ EL 3 ds ==> 1684 ?fi di tw2i. 1685 pre (tw2,sp,df,f,dd,d) /\ 1686 (def (tw2,sp,df,f,dd,d) = (tw2i,sp,df,fi,dd,di)) /\ 1687 let (code,f,d,tw2,ds) = (WRITE_CODE code [inst],fi,di,tw2i,UPDATE_NTH 2 (EL 2 ds + n2w (bc_length inst)) (UPDATE_NTH 3 (EL 3 ds - n2w (bc_length inst)) ds)) in ^LISP`` 1688 |> subst [mk_var("inst",type_of inst)|->inst] 1689 |> subst [mk_var("pre",type_of pre)|->pre] 1690 |> subst [mk_var("def",type_of def)|->def] 1691 val write_list_th = 1692 map (fn x => pairSyntax.mk_pair(genvar(``:word8``),genvar(``:word8``))) ys 1693 |> (fn xs => listSyntax.mk_list(xs,type_of (hd xs))) 1694 |> (fn tm => Q.SPECL [`p`,`q`,`d`,`a + n2w n`] (SPEC tm one_write_list_thm)) 1695 |> SIMP_RULE std_ss [EVERY_DEF,MAP,one_address_list_def,word_arith_lemma1, 1696 one_write_list_def,one_byte_list_def,STAR_ASSOC,SEP_CLAUSES] 1697(* 1698set_goal([],goal) 1699*) 1700 val tac = 1701 (REPEAT STRIP_TAC \\ SIMP_TAC std_ss [def_thm,LET_DEF] 1702 \\ IMP_RES_TAC lisp_inv_ds_read 1703 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 1704 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1705 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 1706 \\ SIMP_TAC std_ss [CONJ_ASSOC] 1707 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1708 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 1709 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1710 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 1711 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 1712 \\ STRIP_TAC THEN1 1713 (Q.ABBREV_TAC `cs2 = [a1; a2; n2w e; bp2; sa1; sa2; sa3; ex] ++ cs` 1714 \\ `LENGTH cs2 = 18` by 1715 (Q.UNABBREV_TAC `cs2` \\ FULL_SIMP_TAC std_ss [LENGTH,LENGTH_APPEND]) 1716 \\ IMP_RES_TAC expand_list2 1717 \\ REPEAT (Q.PAT_X_ASSUM `EL yyy ds = xxxx` (K ALL_TAC)) 1718 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS] 1719 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 1720 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 1721 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 1722 ref_static_APPEND,ref_static_def,LENGTH,mc_code_heap_blast] 1723 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 1724 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1725 \\ SEP_WRITE_TAC) 1726 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ] 1727 \\ EXISTS_TAC ``bs ++ [^inst]`` 1728 \\ EXISTS_TAC ``DROP (bc_length ^inst) (hs:word8 list)`` 1729 \\ FULL_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def] 1730 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND,bc_symbols_ok_APPEND,bc_ref_def, 1731 bc_symbols_ok_def,SND_WRITE_CODE,bc_length_def,word_arith_lemma1] 1732 \\ FULL_SIMP_TAC std_ss [LENGTH,bs2bytes_APPEND] 1733 \\ FULL_SIMP_TAC std_ss [bs2bytes_def,APPEND_NIL,bc_ref_def] 1734 \\ IMP_RES_TAC bc_length_lemma 1735 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [bc_length_def,bc_ref_def, 1736 LENGTH,SUC_EQ_LENGTH] o SPEC inst) 1737 \\ FULL_SIMP_TAC std_ss [DROP_CONS,DROP_0] 1738 \\ Q.PAT_X_ASSUM `xxx = w2n (EL 3 ds)` (ASSUME_TAC o GSYM) 1739 \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,GSYM ADD_ASSOC] 1740 \\ IMP_RES_TAC write_lemma \\ ASM_SIMP_TAC std_ss [] 1741 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM] 1742 \\ Q.PAT_X_ASSUM `xxx (fun2set (d,dd))` ASSUME_TAC 1743 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,one_byte_list_def] 1744 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,STAR_ASSOC,LENGTH_APPEND,LENGTH,GSYM ADD_ASSOC, 1745 word_arith_lemma1] 1746 \\ IMP_RES_TAC LENGTH_bs2bytes \\ FULL_SIMP_TAC std_ss [] 1747 \\ IMP_RES_TAC (GEN_ALL write_list_th) \\ ASM_SIMP_TAC std_ss []) 1748 val correct_thm = prove(goal,tac) |> SIMP_RULE std_ss [LET_DEF]; 1749 in CONJ spec_thm correct_thm end 1750 1751(* 1752 1753val my_consts = LIST_CONJ (map generate_and_verify_write_const 1754 [("isymbol_less",``iDATA (opSYMBOL_LESS)``)]) 1755 1756*) 1757 1758val all_const_insts = 1759 [("ipop",``iPOP``), 1760 ("isymbol_less",``iDATA (opSYMBOL_LESS)``), 1761 ("ijump_sym",``iJUMP_SYM``), 1762 ("icall_sym",``iCALL_SYM``), 1763 ("ireturn",``iRETURN``), 1764 ("ifail",``iFAIL``), 1765 ("icompile",``iCOMPILE``), 1766 ("iprint",``iPRINT``), 1767 ("icons",``iDATA (opCONS)``), 1768 ("iequal",``iDATA (opEQUAL)``), 1769 ("iless",``iDATA (opLESS)``), 1770 ("iadd",``iDATA (opADD)``), 1771 ("isub",``iDATA (opSUB)``), 1772 ("iconsp",``iDATA (opCONSP)``), 1773 ("inatp",``iDATA (opNATP)``), 1774 ("isymbolp",``iDATA (opSYMBOLP)``), 1775 ("icar",``iDATA (opCAR)``), 1776 ("icdr",``iDATA (opCDR)``), 1777 ("ilookup",``iCONST_LOOKUP``)] 1778 1779val consts = LIST_CONJ (map generate_and_verify_write_const all_const_insts); 1780 1781 1782(* code heap -- update iJUMP, iJNIL *) 1783 1784val (mc_update_jump_spec,mc_update_jump_def) = basic_decompile_strings x64_tools "mc_update_jump" 1785 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1786 ``(r1:word64,r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1787 (assemble "x64" ` 1788 mov r1,r8 1789 mov r2,r9 1790 shr r1,2 1791 shr r2,2 1792 sub r1,r2 1793 sub r1,6 1794 add r2,[r7-160] 1795 mov BYTE [r2+2],r1b 1796 shr r1,8 1797 mov BYTE [r2+3],r1b 1798 shr r1,8 1799 mov BYTE [r2+4],r1b 1800 shr r1,8 1801 mov BYTE [r2+5],r1b 1802 mov r1d,1 1803 `) 1804 1805val (mc_update_jnil_spec,mc_update_jnil_def) = basic_decompile_strings x64_tools "mc_update_jnil" 1806 (SOME (``(r1:word64,r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 1807 ``(r1:word64,r2:word64,r7:word64,r8:word64,r9:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 1808 (assemble "x64" ` 1809 mov r1,r8 1810 mov r2,r9 1811 shr r1,2 1812 shr r2,2 1813 sub r1,r2 1814 sub r1,21 1815 add r2,[r7-160] 1816 mov BYTE [r2+17],r1b 1817 shr r1,8 1818 mov BYTE [r2+18],r1b 1819 shr r1,8 1820 mov BYTE [r2+19],r1b 1821 shr r1,8 1822 mov BYTE [r2+20],r1b 1823 mov r1d,1 1824 `) 1825 1826val REPLACE_CODE_def = Define ` 1827 REPLACE_CODE (BC_CODE (c1,c2)) p x = BC_CODE ((p =+ SOME x) c1,c2)`; 1828 1829val SND_REPLACE_CODE = prove( 1830 ``!code p x. code_ptr (REPLACE_CODE code p x) = code_ptr code``, 1831 Cases \\ Cases_on `p` \\ FULL_SIMP_TAC std_ss [REPLACE_CODE_def,code_ptr_def]); 1832 1833val CODE_UPDATE_def = Define ` 1834 CODE_UPDATE x (BC_CODE (c,n)) = BC_CODE ((n =+ SOME x) c, n + bc_length x)`; 1835 1836val WRITE_CODE_SNOC = prove( 1837 ``!xs x c. WRITE_CODE c (xs ++ [x]) = CODE_UPDATE x (WRITE_CODE c xs)``, 1838 Induct \\ Cases_on `c` \\ Cases_on `p` 1839 \\ ASM_SIMP_TAC std_ss [APPEND,WRITE_CODE_def,CODE_UPDATE_def]); 1840 1841val WRITE_CODE_code_length = prove( 1842 ``!bs m k q. 1843 (WRITE_CODE (BC_CODE (m,k)) bs = BC_CODE (q,n)) ==> 1844 (code_length bs = n - k) /\ k <= n``, 1845 Induct \\ SIMP_TAC (srw_ss()) [WRITE_CODE_def,code_length_def] 1846 \\ REPEAT STRIP_TAC \\ RES_TAC 1847 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC); 1848 1849val code_length_IM_SPLIT = prove( 1850 ``!bs n code x. 1851 (code_mem code n = SOME x) /\ 1852 (WRITE_CODE (BC_CODE ((\x.NONE),0)) bs = code) ==> 1853 ?bs1 bs2. (bs = bs1 ++ [x] ++ bs2) /\ (code_length bs1 = n)``, 1854 HO_MATCH_MP_TAC SNOC_INDUCT 1855 \\ SIMP_TAC std_ss [code_length_def,WRITE_CODE_def,code_mem_def] 1856 \\ REPEAT STRIP_TAC 1857 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_SNOC,SNOC_APPEND] 1858 \\ Cases_on `WRITE_CODE (BC_CODE ((\x. NONE),0)) bs` \\ Cases_on `p` 1859 \\ FULL_SIMP_TAC std_ss [code_mem_def,CODE_UPDATE_def,APPLY_UPDATE_THM] 1860 \\ Cases_on `r = n` \\ FULL_SIMP_TAC std_ss [] THEN1 1861 (IMP_RES_TAC WRITE_CODE_code_length \\ Q.LIST_EXISTS_TAC [`bs`,`[]`] 1862 \\ FULL_SIMP_TAC std_ss [APPEND_NIL]) 1863 \\ RES_TAC \\ Q.LIST_EXISTS_TAC [`bs1`,`bs2 ++ [x]`] 1864 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC]); 1865 1866val code_length_APPEND = prove( 1867 ``!xs ys. code_length (xs ++ ys) = code_length xs + code_length ys``, 1868 Induct \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss [ADD_ASSOC]); 1869 1870val bc_length_NOT_ZERO = prove( 1871 ``!x. 0 < bc_length x``, 1872 Cases \\ EVAL_TAC \\ Cases_on `l` \\ EVAL_TAC); 1873 1874val WRITE_CODE_REPLACE_CODE_IMP = prove( 1875 ``!bs2 bs1 code m. 1876 (bc_length x = bc_length y) /\ 1877 (WRITE_CODE (BC_CODE (m,0)) (bs1 ++ [x] ++ bs2) = code) ==> 1878 (WRITE_CODE (BC_CODE (m,0)) (bs1 ++ [y] ++ bs2) = 1879 REPLACE_CODE code (code_length bs1) y)``, 1880 HO_MATCH_MP_TAC SNOC_INDUCT 1881 \\ SIMP_TAC std_ss [code_length_def,WRITE_CODE_def,code_mem_def] 1882 \\ REVERSE (REPEAT STRIP_TAC) THEN1 1883 (FULL_SIMP_TAC std_ss [SNOC_APPEND,APPEND_ASSOC,WRITE_CODE_SNOC] 1884 \\ Q.PAT_X_ASSUM `!x.b` (ASSUME_TAC o Q.SPECL [`bs1`,`m`]) 1885 \\ ASM_SIMP_TAC std_ss [] 1886 \\ Cases_on `WRITE_CODE (BC_CODE (m,0)) (bs1 ++ [x] ++ bs2)` 1887 \\ Cases_on `p` 1888 \\ IMP_RES_TAC WRITE_CODE_code_length 1889 \\ FULL_SIMP_TAC std_ss [code_length_APPEND,code_length_def] 1890 \\ `0 < bc_length x` by FULL_SIMP_TAC std_ss [bc_length_NOT_ZERO] 1891 \\ `~(r = code_length bs1)` by DECIDE_TAC 1892 \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,APPLY_UPDATE_THM] 1893 \\ METIS_TAC []) 1894 \\ FULL_SIMP_TAC std_ss [APPEND_NIL,WRITE_CODE_SNOC] 1895 \\ Cases_on `WRITE_CODE (BC_CODE (m,0)) bs1` \\ Cases_on `p` 1896 \\ IMP_RES_TAC WRITE_CODE_code_length 1897 \\ FULL_SIMP_TAC std_ss [REPLACE_CODE_def,CODE_UPDATE_def] 1898 \\ FULL_SIMP_TAC std_ss [combinTheory.UPDATE_EQ]); 1899 1900val LENGTH_bs2bytes_EQ = prove( 1901 ``!bs k sym. LENGTH (bs2bytes (k,sym) bs) = code_length bs``, 1902 Induct \\ ASM_SIMP_TAC std_ss [bs2bytes_def,LENGTH,code_length_def,LENGTH_APPEND] 1903 \\ Cases \\ EVAL_TAC \\ SIMP_TAC std_ss [] 1904 \\ Cases_on `l` \\ EVAL_TAC \\ SIMP_TAC std_ss []); 1905 1906val code_length_APPEND = prove( 1907 ``!xs ys. code_length (xs ++ ys) = code_length xs + code_length ys``, 1908 Induct \\ ASM_SIMP_TAC std_ss [APPEND,code_length_def,ADD_ASSOC]); 1909 1910val replace_jump_balst = blastLib.BBLAST_PROVE 1911 ``(w2w:word32->word64) (w2w (w:30 word) << 2 !! 1w) >>> 2 = w2w w`` 1912 1913val replace_jump_balst2 = blastLib.BBLAST_PROVE 1914 ``((w2w:word32->word8) ((w - v) >>> 24) = w2w ((w2w w - (w2w:word32->word64) v) >>> 24)) /\ 1915 ((w2w:word32->word8) ((w - v) >>> 16) = w2w ((w2w w - (w2w:word32->word64) v) >>> 16)) /\ 1916 ((w2w:word32->word8) ((w - v) >>> 8) = w2w ((w2w w - (w2w:word32->word64) v) >>> 8)) /\ 1917 ((w2w:word32->word8) ((w - v)) = w2w ((w2w w - (w2w:word32->word64) v)))`` 1918 1919fun REPLACE_JUMP_TAC inst = 1920 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [mc_update_jump_def,mc_update_jnil_def,LET_DEF] 1921 \\ IMP_RES_TAC lisp_inv_ds_read 1922 \\ IMP_RES_TAC lisp_inv_cs_read 1923 \\ ASM_SIMP_TAC std_ss [INSERT_SUBSET,EMPTY_SUBSET] 1924 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 1925 \\ ASM_SIMP_TAC std_ss [align_blast,n2w_and_3] 1926 \\ SIMP_TAC std_ss [CONJ_ASSOC] 1927 \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1928 \\ SIMP_TAC std_ss [PULL_EXISTS_OVER_CONJ] 1929 \\ Q.LIST_EXISTS_TAC [`s0`,`s1`,`s2`,`s3`,`s4`,`s5`,`m`,`i`,`ss`,`ss1`,`sym`,`b`] 1930 \\ ASM_SIMP_TAC std_ss [EL_UPDATE_NTH,LENGTH_UPDATE_NTH] 1931 \\ ASM_SIMP_TAC std_ss [bc_length_def,LENGTH,bc_ref_def,GSYM CONJ_ASSOC] 1932 \\ ASM_SIMP_TAC std_ss [IMMEDIATE32_def,APPEND,LENGTH,LSR_ADD] 1933 \\ FULL_SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_OVER_CONJ,SND_REPLACE_CODE] 1934 \\ `?bs1 bs2. (bs = bs1 ++ [^(car inst) 0] ++ bs2) /\ (code_length bs1 = getVal x1)` by METIS_TAC [code_length_IM_SPLIT] 1935 \\ FULL_SIMP_TAC std_ss [] 1936 \\ Q.EXISTS_TAC `bs1 ++ [^inst] ++ bs2` \\ Q.EXISTS_TAC `hs` 1937 \\ IMP_RES_TAC WRITE_CODE_REPLACE_CODE_IMP 1938 \\ FULL_SIMP_TAC std_ss [] 1939 \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_APPEND,bs2bytes_APPEND,bs2bytes_def, 1940 bc_symbols_ok_def,APPEND_NIL,bc_ref_def,IMMEDIATE32_def,one_byte_list_def, 1941 one_byte_list_APPEND,APPEND,LENGTH_APPEND,LENGTH,SEP_CLAUSES,STAR_ASSOC, 1942 word_arith_lemma1,GSYM ADD_ASSOC,LENGTH_bs2bytes_EQ,code_length_APPEND, 1943 code_length_def,bc_length_def] 1944 \\ `(w2w w0 >>> 2 = (n2w (getVal x0)):word64) /\ getVal x0 < 2**30 /\ 1945 (w2w w1 >>> 2 = (n2w (getVal x1)):word64) /\ getVal x1 < 2**30` by 1946 (FULL_SIMP_TAC std_ss [isVal_thm,getVal_def] 1947 \\ Q.PAT_X_ASSUM `MAP ref_heap_addr [s0; s1; s2; s3; s4; s5] = xx` (ASSUME_TAC o GSYM) 1948 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,CONS_11,MAP,lisp_x_def,ref_heap_addr_def] 1949 \\ FULL_SIMP_TAC std_ss [replace_jump_balst] 1950 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w,WORD_MUL_LSL,word_add_n2w,word_mul_n2w]) 1951 \\ ASM_SIMP_TAC std_ss [] 1952 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,AC WORD_ADD_ASSOC WORD_ADD_COMM] 1953 \\ ASM_SIMP_TAC std_ss [GSYM WORD_SUB_PLUS,word_add_n2w] 1954 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [replace_jump_balst2] 1955 \\ `(((w2w:word32->word64) (n2w (getVal x0)) = n2w (getVal x0))) /\ 1956 (((w2w:word32->word64) (n2w (getVal x1)) = n2w (getVal x1))) /\ 1957 (((w2w:word32->word64) (n2w (getVal x1 + 6)) = n2w (getVal x1 + 6))) /\ 1958 (((w2w:word32->word64) (n2w (getVal x1 + 21)) = n2w (getVal x1 + 21)))` by 1959 (IMP_RES_TAC (DECIDE ``n < 1073741824 ==> (n:num) < 4294967296 /\ n+6 < 4294967296 /\ n+21 < 4294967296``) 1960 \\ ASM_SIMP_TAC wstd_ss [w2w_def,w2n_n2w]) 1961 \\ ASM_SIMP_TAC std_ss [] 1962 \\ SEP_WRITE_TAC 1963 1964val inst = ``iJUMP (getVal x0)`` 1965val mc_update_jump_thm = prove( 1966 ``^LISP /\ 0x100w <+ EL 3 ds ==> 1967 isVal x0 /\ isVal x1 /\ (code_mem code (getVal x1) = SOME (^(car inst) 0)) ==> 1968 ?di tw2i. 1969 mc_update_jump_pre (tw1,tw2,sp,w2w w0,w2w w1,df,f,dd,d) /\ 1970 (mc_update_jump (tw1,tw2,sp,w2w w0,w2w w1,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,w2w w1,df,f,dd,di)) /\ 1971 let (code,d,tw2) = (REPLACE_CODE code (getVal x1) ^inst,di,tw2i) in ^LISP``, 1972 REPLACE_JUMP_TAC inst) |> SIMP_RULE std_ss [LET_DEF]; 1973 1974val inst = ``iJNIL (getVal x0)`` 1975val mc_update_jnil_thm = prove( 1976 ``^LISP /\ 0x100w <+ EL 3 ds ==> 1977 isVal x0 /\ isVal x1 /\ (code_mem code (getVal x1) = SOME (^(car inst) 0)) ==> 1978 ?di tw2i. 1979 mc_update_jnil_pre (tw1,tw2,sp,w2w w0,w2w w1,df,f,dd,d) /\ 1980 (mc_update_jnil (tw1,tw2,sp,w2w w0,w2w w1,df,f,dd,d) = (tw1,tw2i,sp,w2w w0,w2w w1,df,f,dd,di)) /\ 1981 let (code,d,tw2) = (REPLACE_CODE code (getVal x1) ^inst,di,tw2i) in ^LISP``, 1982 REPLACE_JUMP_TAC inst) |> SIMP_RULE std_ss [LET_DEF]; 1983 1984 1985(* store all code heap write/replace *) 1986 1987val numsym = LIST_CONJ [CONJ (mc_write_num_spec) (mc_write_num_thm), 1988 CONJ (mc_write_num_spec) (mc_write_sym_thm)]; 1989val pops = LIST_CONJ [CONJ (mc_write_pops_spec) (mc_write_pops_thm), 1990 CONJ (mc_write_load_spec) (mc_write_load_thm), 1991 CONJ (mc_write_store_spec) (mc_write_store_thm)]; 1992val calls = LIST_CONJ [CONJ (mc_write_call_spec) (mc_write_call_thm), 1993 CONJ (mc_write_jump_spec) (mc_write_jump_thm), 1994 CONJ (mc_write_jnil_spec) (mc_write_jnil_thm)]; 1995val updates = LIST_CONJ [CONJ mc_update_jump_spec mc_update_jump_thm, 1996 CONJ mc_update_jnil_spec mc_update_jnil_thm] 1997 1998val lisp_inv_write_consts_thm = save_thm("lisp_inv_write_consts_thm", 1999 LIST_CONJ [numsym,updates,pops,calls,consts]); 2000 2001 2002(* load pointer into code (used by eval) *) 2003 2004val (mc_calc_addr_spec,mc_calc_addr_def) = basic_decompile_strings x64_tools "mc_calc_addr" 2005 (SOME (``(r2:word64,r7:word64,r10:word64,df:word64 set,f:word64->word32)``, 2006 ``(r2:word64,r7:word64,r10:word64,df:word64 set,f:word64->word32)``)) 2007 (assemble "x64" ` 2008 mov r2,r10 2009 shr r2,2 2010 add r2,[r7-160] 2011 `) 2012 2013val _ = save_thm("mc_calc_addr_spec",mc_calc_addr_spec); 2014 2015val mc_calc_addr_thm = store_thm("mc_calc_addr_thm", 2016 ``^LISP ==> isVal x2 ==> 2017 ?tw2i. mc_calc_addr_pre (tw2,sp,w2w w2,df,f) /\ 2018 (mc_calc_addr (tw2,sp,w2w w2,df,f) = (tw2i,sp,w2w w2,df,f)) /\ 2019 (tw2i = EL 4 cs + n2w (getVal x2)) /\ 2020 let tw2 = tw2i in ^LISP``, 2021 FULL_SIMP_TAC std_ss [LET_DEF,mc_calc_addr_def] \\ NTAC 2 STRIP_TAC 2022 \\ FULL_SIMP_TAC std_ss [isVal_thm,getVal_def,INSERT_SUBSET,EMPTY_SUBSET] 2023 \\ IMP_RES_TAC lisp_inv_cs_read \\ FULL_SIMP_TAC std_ss [] 2024 \\ `sp && 3w = 0w` by FULL_SIMP_TAC std_ss [lisp_inv_def] 2025 \\ STRIP_TAC THEN1 (POP_ASSUM MP_TAC THEN blastLib.BBLAST_TAC) 2026 \\ `w2w w2 >>> 2 = (n2w a):word64` by 2027 (FULL_SIMP_TAC std_ss [lisp_inv_def,EVERY_DEF,MAP,CONS_11] 2028 \\ Q.PAT_X_ASSUM `ref_heap_addr s2 = w2` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 2029 \\ FULL_SIMP_TAC std_ss [lisp_x_def,ref_heap_addr_alt] 2030 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,WORD_MUL_LSL,word_mul_n2w, 2031 word_add_n2w,GSYM w2n_11,w2n_lsr] 2032 \\ `4 * a + 1 < 4294967296` by DECIDE_TAC 2033 \\ `(4 * a + 1) < 18446744073709551616` by DECIDE_TAC 2034 \\ `a < 18446744073709551616` by DECIDE_TAC 2035 \\ ASM_SIMP_TAC std_ss [DIV_EQ_X] \\ DECIDE_TAC) 2036 \\ ASM_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 2037 \\ MATCH_MP_TAC (GEN_ALL lisp_inv_ignore_tw2) \\ METIS_TAC []); 2038 2039 2040(* return stack *) 2041 2042val stack_tm = 2043 [``SPEC X64_MODEL 2044 (zPC p * zR 0x2w r2 * stack (rbp:word64) qs) 2045 {(p,[0x48w; 0xFFw; 0xD2w])} 2046 (zPC r2 * zR 0x2w r2 * stack (rbp:word64) ((p+3w)::qs))``, 2047 ``SPEC X64_MODEL 2048 (zPC p * zR 0x2w r2 * stack (rbp:word64) qs) 2049 {(p,[0x48w; 0x52w])} 2050 (zPC (p+2w) * zR 0x2w r2 * stack (rbp:word64) (r2::qs))``, 2051 ``SPEC X64_MODEL 2052 (zPC p * stack (rbp:word64) qs * cond ~(qs = [])) 2053 {(p,[0x48w; 0xC3w])} 2054 (zPC (HD qs) * stack (rbp:word64) (TL qs))``, 2055 ``SPEC X64_MODEL 2056 (zPC p * zR 0x2w r2 * stack (rbp:word64) qs * cond ~(qs = [])) 2057 {(p,[0x48w; 0x5Aw])} 2058 (zPC (p+2w) * zR 0x2w (HD qs) * stack (rbp:word64) (TL qs))``, 2059 ``SPEC X64_MODEL 2060 (zPC p * stack (rbp:word64) qs) 2061 {(p,[0x48w; 0xE8w; w2w imm32; w2w (imm32 >>> 8); w2w (imm32 >>> 16); w2w (imm32 >>> 24)])} 2062 (zPC (p + n2w (6 + SIGN_EXTEND 32 64 (w2n (imm32:word32)))) * 2063 stack (rbp:word64) ((p + 0x6w)::qs))``] 2064 |> list_mk_conj 2065 |> (fn tm => list_mk_forall (filter (fn v => fst (dest_var v) <> "stack") 2066 (free_vars tm), tm)); 2067 2068val zSTACK_def = Define ` (* improve at some point... *) 2069 zSTACK rbp xs = SEP_EXISTS stack. stack rbp xs * cond ^stack_tm` 2070 2071val zSTACK_PROPS = store_thm("zSTACK_PROPS", 2072 subst [hd (free_vars stack_tm)|->``zSTACK``] stack_tm, 2073 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [zSTACK_def,SEP_CLAUSES] 2074 \\ HO_MATCH_MP_TAC SPEC_EXISTS_EXISTS 2075 \\ FULL_SIMP_TAC std_ss [SPEC_MOVE_COND,STAR_ASSOC,SEP_CLAUSES]); 2076 2077val lisp_inv_stack = prove( 2078 ``!qs2 tw3. ^LISP ==> let qs = qs2 in let tw2 = tw3 in ^LISP``, 2079 SIMP_TAC std_ss [lisp_inv_def,LET_DEF]) |> SIMP_RULE std_ss [LET_DEF]; 2080 2081val _ = save_thm("lisp_inv_stack",lisp_inv_stack); 2082 2083 2084val _ = export_theory(); 2085