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