1141394Sdelphijopen HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_init"; 2141394Sdelphijopen lisp_sexpTheory lisp_consTheory lisp_invTheory lisp_codegenTheory; 3141443Sru 4141394Sdelphij(* --- *) 5141394Sdelphij 6141394Sdelphijopen wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 7141394Sdelphijopen combinTheory finite_mapTheory addressTheory helperLib; 8141394Sdelphijopen set_sepTheory bitTheory fcpTheory stringTheory; 9141432Sdelphij 10141443Sruval wstd_ss = std_ss ++ SIZES_ss ++ rewrites [DECIDE ``n<256 ==> (n:num)<18446744073709551616``,ORD_BOUND]; 11141394Sdelphij 12201386Sedopen stop_and_copyTheory; 13201386Sedopen codegenLib decompilerLib prog_x64Lib prog_x64Theory progTheory; 14141394Sdelphijopen 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 FORALL_EXISTS = METIS_PROVE [] ``(!x. P x ==> Q) = ((?x. P x) ==> Q)`` 23val IMP_IMP = METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)`` 24 25val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst; 26val REST = LISP |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 27val STAT = LISP |> car |> car |> cdr; 28val VAR_REST = LISP |> car |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr |> cdr; 29 30val align_blast = blastLib.BBLAST_PROVE 31 ``(a && 3w = 0w) ==> ((a - w && 3w = 0w) = (w && 3w = 0w:word64))`` 32 33val align_add_blast = blastLib.BBLAST_PROVE 34 ``(a && 3w = 0w) ==> ((a + w && 3w = 0w) = (w && 3w = 0w:word64))`` 35 36 37(* setup symbol table *) 38 39val bytes2words_def = tDefine "bytes2words" ` 40 bytes2words xs = if LENGTH xs <= 4 then [bytes2word (TAKE 4 (xs ++ [0w;0w;0w;0w]))]:word32 list else 41 bytes2word (TAKE 4 xs) :: bytes2words (DROP 4 xs)` 42 (WF_REL_TAC `measure (LENGTH)` \\ SIMP_TAC std_ss [LENGTH_DROP] \\ DECIDE_TAC) 43 44val BINIT_SYMBOLS_def = Define `BINIT_SYMBOLS = INIT_SYMBOLS ++ ["PEQUAL"]`; 45 46val INIT_SYMBOL_ASSERTION = 47 EVAL ``(FOLDR (\x y. STRLEN x + y + 1) 1 BINIT_SYMBOLS) MOD 4`` 48 |> concl |> dest_eq |> snd |> (fn x => if x = ``0`` then () else fail()); 49 50val (init_func_spec,init_func_def) = let 51 val tm = (snd o dest_eq o concl o EVAL) ``bytes2words (symbol_list BINIT_SYMBOLS)`` 52 val xs = tm |> listSyntax.dest_list |> fst 53 val ((th1,_,_),_) = x64_spec_byte_memory "C700" 54 val ((th2,_,_),_) = x64_spec_byte_memory (x64_encodeLib.x64_encode "add r0,4") 55 val th = SPEC_COMPOSE_RULE [th1,th2] 56 val (_,_,sts,_) = x64_tools 57 val th = HIDE_STATUS_RULE true sts th 58 val tms = find_terml (can (match_term ``((7 >< 0) (w:'a word)):word8``)) (concl th) 59 val imm32 = hd (free_vars (hd tms)) 60 fun th_inst w = RW (map (EVAL o subst [imm32|->w]) tms) (INST [imm32|->w] th) 61 val res = SPEC_COMPOSE_RULE (map th_inst xs) 62 val f_tm = find_term (can (match_term ``(a =+ w) f``)) (concl res) 63 val lhs_tm = ``(init_func (g:word64->word8) (r0:word64)):word64->word8`` 64 val def = new_definition("init_func",mk_eq(lhs_tm,f_tm)) 65 val res = RW [GSYM def] res 66 val res = SIMP_RULE wstd_ss [w2w_def,w2n_n2w,w2n_lsr] res 67 val res = RW1 [GSYM n2w_mod] res 68 val res = SIMP_RULE (std_ss++SIZES_ss++sep_cond_ss) [] res 69 val lhs_pre = ``(init_func_pre (dg:word64 set) (r0:word64)):bool`` 70 val f_pre = (hd o hyp o UNDISCH o RW [progTheory.SPEC_MOVE_COND]) res 71 val pre = new_definition("init_func_pre",mk_eq(lhs_pre,f_pre)) 72 val res = RW [GSYM pre] res 73 val def = CONJ def pre 74 in (res,def) end 75 76val _ = let 77 val th = init_func_spec 78 val pc = find_term (can (match_term (``zPC xx``))) (cdr (concl th)) 79 val post = ``let (r0,g) = (r0 + n2w (LENGTH (symbol_list BINIT_SYMBOLS)),init_func g r0) in 80 x * zR 0x0w r0 * zBYTE_MEMORY dg g * ~zS`` 81 val post = subst [mk_var("x",type_of pc)|->pc] post 82 val (th,goal) = SPEC_WEAKEN_RULE th post 83 val lemma = prove(goal, 84 SIMP_TAC std_ss [EVAL ``LENGTH (symbol_list BINIT_SYMBOLS)``,LET_DEF] 85 \\ SIMP_TAC (std_ss++star_ss) [SEP_IMP_REFL]) 86 val th = MP th lemma 87 val i = numSyntax.int_of_term (find_term numSyntax.is_numeral pc) 88 val _ = add_decompiled ("init_func",th,i,SOME i) 89 in () end; 90 91val one_fun2set_IMP = prove( 92 ``(one (a,x) * p) (fun2set (g,dg DIFF xs)) ==> 93 p (fun2set (g,dg DIFF (a INSERT xs))) /\ a IN dg``, 94 SIMP_TAC std_ss [one_fun2set,IN_DIFF] 95 \\ sg `dg DIFF (a INSERT xs) = dg DIFF xs DELETE a` 96 \\ FULL_SIMP_TAC std_ss [] 97 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_INSERT,IN_DELETE] 98 \\ METIS_TAC []); 99 100val DIFF_EMPTY_LEMMA = prove( 101 ``fun2set (g,dg) = fun2set (g,dg DIFF {})``, 102 SIMP_TAC std_ss [DIFF_EMPTY]); 103 104val LENGTH_EQ_IMP = prove( 105 ``!xs y ys. 106 (LENGTH xs = LENGTH (y::ys)) ==> ?z zs. (xs = z::zs) /\ (LENGTH zs = LENGTH ys)``, 107 Cases \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11]); 108 109val init_func_lemma = prove( 110 ``(LENGTH xs = LENGTH (symbol_list BINIT_SYMBOLS)) ==> 111 (one_byte_list a (xs ++ ys)) (fun2set(g,dg)) /\ 520 <= LENGTH ys ==> 112 init_func_pre dg a /\ 113 (one_symbol_list a BINIT_SYMBOLS (LENGTH (symbol_list BINIT_SYMBOLS ++ ys)) (fun2set(init_func g a,dg)))``, 114 SIMP_TAC std_ss [one_symbol_list_def,SEP_EXISTS_THM,cond_STAR] 115 \\ REPEAT STRIP_TAC THEN1 116 (POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 117 \\ SIMP_TAC std_ss [EVAL ``symbol_list BINIT_SYMBOLS``] \\ STRIP_TAC 118 \\ NTAC 500 (IMP_RES_TAC LENGTH_EQ_IMP \\ POP_ASSUM MP_TAC 119 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ STRIP_TAC) 120 \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,LENGTH] 121 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,word_arith_lemma1,APPEND] 122 \\ FULL_SIMP_TAC std_ss [init_func_def,INSERT_SUBSET,EMPTY_SUBSET] 123 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [DIFF_EMPTY_LEMMA])) 124 \\ REPEAT (STRIP_TAC 125 \\ IMP_RES_TAC one_fun2set_IMP 126 \\ POP_ASSUM MP_TAC 127 \\ POP_ASSUM MP_TAC 128 \\ REPEAT (POP_ASSUM (K ALL_TAC))) 129 \\ SIMP_TAC std_ss []) 130 \\ Q.EXISTS_TAC `ys` \\ ASM_SIMP_TAC std_ss [] 131 \\ STRIP_TAC THEN1 EVAL_TAC 132 \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 133 \\ SIMP_TAC std_ss [EVAL ``symbol_list BINIT_SYMBOLS``] \\ STRIP_TAC 134 \\ NTAC 500 (IMP_RES_TAC LENGTH_EQ_IMP \\ POP_ASSUM MP_TAC 135 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ STRIP_TAC) 136 \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,LENGTH] 137 \\ FULL_SIMP_TAC std_ss [one_byte_list_def,word_arith_lemma1,APPEND] 138 \\ FULL_SIMP_TAC std_ss [init_func_def] 139 \\ REPEAT STRIP_TAC \\ SEP_WRITE_TAC); 140 141val init_func_thm = prove( 142 ``1024 <= LENGTH xs ==> 143 (one_byte_list a xs) (fun2set(g,dg)) ==> 144 ?ys. 145 init_func_pre dg a /\ 520 <= LENGTH ys /\ 146 (one_symbol_list a BINIT_SYMBOLS (LENGTH (symbol_list BINIT_SYMBOLS ++ ys)) (fun2set(init_func g a,dg))) /\ 147 (LENGTH xs = LENGTH (symbol_list BINIT_SYMBOLS ++ ys))``, 148 `LENGTH (symbol_list BINIT_SYMBOLS) <= 504` by EVAL_TAC \\ FULL_SIMP_TAC std_ss [] 149 \\ REPEAT STRIP_TAC 150 \\ `LENGTH (symbol_list BINIT_SYMBOLS) <= LENGTH xs` by DECIDE_TAC 151 \\ IMP_RES_TAC (Q.SPECL [`xs`,`LENGTH ys`] SPLIT_LIST_LESS_EQ) 152 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 153 \\ `520 <= LENGTH xs2` by DECIDE_TAC 154 \\ IMP_RES_TAC init_func_lemma \\ Q.EXISTS_TAC `xs2` 155 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND]); 156 157val ref_stack_space_SUC = prove( 158 ``!n a. 159 ref_stack_space a (SUC n) = 160 SEP_EXISTS w. one (a - n2w (4 * n) - 4w,w) * ref_stack_space a n``, 161 Induct THEN1 SIMP_TAC std_ss [ref_stack_space_def,SEP_CLAUSES,WORD_SUB_RZERO] 162 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 163 \\ SIMP_TAC std_ss [Once ref_stack_space_def,SEP_CLAUSES,STAR_ASSOC] 164 \\ SIMP_TAC std_ss [Once ref_stack_space_def,SEP_CLAUSES,STAR_ASSOC] 165 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,ADD1,word_arith_lemma1,LEFT_ADD_DISTRIB, 166 AC ADD_COMM ADD_ASSOC] 167 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM,SEP_EXISTS_THM] \\ METIS_TAC []); 168 169val ref_stack_space_above_ADD = prove( 170 ``!n m a. 171 ref_stack_space_above a (n + m) = 172 ref_stack_space (a + 4w + n2w (4 * n)) n * 173 ref_stack_space_above (a + n2w (4 * n)) m``, 174 Induct THEN1 SIMP_TAC std_ss [ref_stack_space_def,SEP_CLAUSES,WORD_ADD_0] 175 \\ ASM_SIMP_TAC std_ss [ref_stack_space_SUC,WORD_ADD_0,ADD,ref_stack_space_above_def] 176 \\ SIMP_TAC std_ss [word_arith_lemma1] 177 \\ SIMP_TAC std_ss [word_arith_lemma4,DECIDE ``~(SUC n < n)``, 178 DECIDE ``4 + 4 * SUC n - (4 * n + 4) = 4``] 179 \\ FULL_SIMP_TAC (std_ss++star_ss) [ADD1,LEFT_ADD_DISTRIB, 180 AC ADD_COMM ADD_ASSOC,SEP_CLAUSES]); 181 182val lisp_init_def = Define ` 183 lisp_init (a1,a2,sl,sl1,e,ex,cs) (io:io_streams) (df,f,dg,g,dd,d,sp,sa1,sa_len,ds) = 184 ?x xs hs. 185 (ref_mem a1 (\x. H_EMP) 0 e * ref_mem a2 (\x. H_EMP) 0 e * 186 ref_static sp ([a1; a2; n2w e; n2w sl; sa1; sa_len; x; ex] ++ cs ++ ds) * 187 (* ref_stack_space (sp + 256w + 4w * n2w (sl + 1)) (sl + 6 + 1) *) 188 ref_stack_space_above (sp + 228w) (sl + 6 + 1 + sl1)) 189 (fun2set (f,df)) /\ 190 e < 2147483648 /\ sl + 1 < 2**64 /\ 1024 <= w2n sa_len /\ sl1 < 2**30 /\ 191 (LENGTH cs = 10) /\ (LENGTH ds = 10) /\ (w2n (EL 3 cs) < 2**30) /\ 192 (a1 && 0x3w = 0x0w) /\ (a2 && 0x3w = 0x0w) /\ (sp && 0x3w = 0x0w) /\ 193 (w2n sa_len = LENGTH xs) /\ (one_byte_list sa1 xs) (fun2set(g,dg)) /\ 194 w2n sa1 + w2n sa_len < 2**64 /\ (w2n (EL 5 cs) < 2**30) /\ 195 (w2n (EL 5 ds) <= e) /\ (EL 7 ds = n2w sl1) /\ 196 (one_byte_list (EL 4 cs) hs) (fun2set(d,dd)) /\ (LENGTH hs = w2n (EL 5 cs))`; 197 198val (mc_full_init_spec,mc_full_init_def) = basic_decompile_strings x64_tools "mc_full_init" 199 (SOME (``(r7:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``, 200 ``(r0:word64,r1:word64,r2:word64,r3:word64,r6:word64,r7:word64,r8:word64,r9:word64,r10:word64,r11:word64,r12:word64,r13:word64,r14:word64,r15:word64,df:word64 set,f:word64->word32,dg:word64 set,g:word64->word8)``)) 201 (assemble "x64" ` 202 mov r3,[r7+24] 203 mov r15,[r7+16] 204 mov r0,[r7+32] 205 mov r1,[r7+40] 206 mov r2,[r7+8] 207 mov r6,[r7] 208 mov r8,[r7+96] 209 mov r9,[r7+104] 210 mov r10,[r7+88] 211 add r1,r0 212 insert init_func 213 mov [r7+40],r0 214 mov [r7+48],r1 215 mov [r7+24],r2 216 mov r1d,1 217 xor r14,r14 218 add r15,r15 219 mov r0,r3 220 shl r0,2 221 dec r0 222 add r0,256 223 lea r12,[r7+r0] 224 add r0,r7 225 xor r11,r11 226 mov [r7+152],r0 227 mov [r7+160],r8 228 mov [r7+168],r9 229 mov [r7+216],r10 230 mov [r7+208],r11 231 mov [r7+192],r12 232 add r7,256 233 xor r2,r2 234 not r2 235 mov [r7+4*r3],r2d 236 mov r0d,3 237 mov r2,r0 238 mov r8,r0 239 mov r9,r0 240 mov r10,r0 241 mov r11,r0 242 mov r12,r0 243 mov r13,r0 244 `); 245 246val _ = save_thm("mc_full_init_spec",mc_full_init_spec); 247 248val mc_full_init_blast = blastLib.BBLAST_PROVE 249 ``(w2w ((w2w (w >>> 32)):word32) << 32 !! w2w ((w2w (w:word64)):word32) = w) /\ 250 ((63 >< 32) w = (w2w (w >>> 32)):word32) /\ ((31 >< 0) w = (w2w w):word32)``; 251 252val mc_full_init_blast_select = blastLib.BBLAST_PROVE 253 ``(w2w (w2w w1 << 32 !! (w2w:word32->word64) w2) = w2:word32) /\ 254 (w2w ((w2w w1 << 32 !! (w2w:word32->word64) w2) >>> 32) = w1:word32)``; 255 256val expand_list = prove( 257 ``!cs. (LENGTH cs = 10) ==> 258 ?c0 c1 c2 c3 c4 c5 c6 c7 c8 c9. cs = [c0;c1;c2;c3;c4;c5;c6;c7;c8;c9]``, 259 Cases \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 260 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 261 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 262 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 263 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 264 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 265 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 266 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 267 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 268 \\ Cases_on `t` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 269 \\ Cases_on `t'` \\ SIMP_TAC std_ss [LENGTH,ADD1,CONS_11,NOT_CONS_NIL] 270 \\ DECIDE_TAC); 271 272val EL_LEMMA = prove( 273 ``!x y zs. EL 1 (x::y::zs) = y``, 274 SIMP_TAC bool_ss [GSYM (EVAL ``SUC 0``),TL,HD,EL]); 275 276val NO_CODE_def = Define ` 277 NO_CODE = BC_CODE ((\x:num.(NONE:bc_inst_type option)),0)`; 278 279val one_fun2set_IMP = prove( 280 ``(one (a,x)) (fun2set (f,df)) ==> (f a = x) /\ a IN df``, 281 REPEAT STRIP_TAC 282 \\ IMP_RES_TAC (REWRITE_RULE [SEP_CLAUSES] (Q.SPECL [`a`,`x`,`emp`] one_fun2set))); 283 284val mc_full_init_thm = prove( 285 ``lisp_init (a1,a2,sl,sl1,e,ex,cs) (io) (df,f,dg,g,dd,d,sp,sa1,sa_len,ds) ==> 286 ?w0 w1 w2 w3 w4 w5 tw0 tw1 tw2 wi we wsp bp bp2 sa2 sa3 fi gi. 287 mc_full_init_pre (sp,df,f,dg,g) /\ 288 (mc_full_init (sp,df,f,dg,g) = (tw0,tw1,tw2,wsp,bp,sp+256w,w2w w0,w2w w1,w2w w2,w2w w3,w2w w4,w2w w5,wi,we,df,fi,dg,gi)) /\ 289 let (x0,x1,x2,x3,x4,x5,xs,xs1,xbp,sp,f,g,ds,code,amnt,ok) = (Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",Sym "NIL",[],[],0,sp+256w,fi,gi,UPDATE_NTH 6 (sp + 256w + 4w * n2w sl - 1w) (UPDATE_NTH 8 0w (UPDATE_NTH 9 (EL 3 cs) (UPDATE_NTH 3 (EL 5 cs) (UPDATE_NTH 2 (EL 4 cs) (UPDATE_NTH 1 (sp + 256w + n2w (4 * sl) - 1w) ds))))),NO_CODE,w2n (EL 3 cs),T) in ^LISP``, 290 SIMP_TAC std_ss [LET_DEF,lisp_init_def] 291 \\ ONCE_REWRITE_TAC [ref_stack_space_above_ADD] 292 \\ `sp + 0xE4w + 0x4w + n2w (4 * (sl + 6 + 1)) = 293 sp + 0x100w + 4w * n2w (sl + 1)` by 294 (FULL_SIMP_TAC std_ss [word_arith_lemma1,word_mul_n2w,LEFT_ADD_DISTRIB] 295 \\ Q.SPEC_TAC (`4*sl`,`x`) \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC]) 296 \\ FULL_SIMP_TAC std_ss [STAR_ASSOC] \\ REPEAT STRIP_TAC 297 \\ Q.LIST_EXISTS_TAC [`3w`,`3w`,`3w`,`3w`,`3w`,`3w`,`3w`,`1w`,`3w`] 298 \\ Q.LIST_EXISTS_TAC [`0w`,`n2w (2 * e)`,`n2w sl`] 299 \\ Q.LIST_EXISTS_TAC [`a1`,`a2`,`sa1+n2w(LENGTH(symbol_list BINIT_SYMBOLS))`,`sa1+sa_len`] 300 \\ FULL_SIMP_TAC wstd_ss [w2w_def,w2n_n2w] 301 \\ FULL_SIMP_TAC std_ss [mc_full_init_def,ref_full_stack_def] 302 \\ FULL_SIMP_TAC std_ss [WORD_ADD_SUB] 303 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND, 304 word64_3232_def,word_arith_lemma1,STAR_ASSOC,INSERT_SUBSET,EMPTY_SUBSET] 305 \\ FULL_SIMP_TAC std_ss [align_add_blast,n2w_and_3] 306 \\ SEP_R_TAC \\ FULL_SIMP_TAC std_ss [mc_full_init_blast] 307 \\ SIMP_TAC std_ss [word_add_n2w,DECIDE ``2*n = n+n``] 308 \\ `init_func_pre dg sa1` by METIS_TAC [init_func_thm] 309 \\ FULL_SIMP_TAC std_ss [GSYM ADD1,ref_stack_space_def] 310 \\ FULL_SIMP_TAC std_ss [ADD1,GSYM word_add_n2w,WORD_LEFT_ADD_DISTRIB] 311 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC,WORD_ADD_SUB,SEP_CLAUSES,STAR_ASSOC,word_mul_n2w] 312 \\ SIMP_TAC std_ss [CONJ_ASSOC] 313 \\ STRIP_TAC THEN1 314 (REVERSE STRIP_TAC THEN1 315 (FULL_SIMP_TAC std_ss [GSYM word_mul_n2w] \\ Q.SPEC_TAC (`(n2w sl):word64`,`slw`) 316 \\ Q.PAT_X_ASSUM `sp && 3w = 0w` MP_TAC \\ blastLib.BBLAST_TAC) 317 \\ REVERSE STRIP_TAC THEN1 318 (FULL_SIMP_TAC std_ss [SEP_EXISTS_THM,AC WORD_ADD_COMM WORD_ADD_ASSOC] \\ SEP_R_TAC) 319 \\ IMP_RES_TAC expand_list 320 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,SEP_EXISTS_THM, 321 word64_3232_def,APPEND,word_arith_lemma1,STAR_ASSOC,SEP_CLAUSES, 322 ref_static_APPEND] 323 \\ REPEAT (Q.PAT_X_ASSUM `(p_p * q_q) (fun2set (f_f,df_df))` 324 (STRIP_ASSUME_TAC o MATCH_MP fun2set_STAR_IMP)) 325 \\ IMP_RES_TAC one_fun2set_IMP \\ FULL_SIMP_TAC std_ss [DIFF_UNION] 326 \\ FULL_SIMP_TAC std_ss [IN_DIFF]) 327 \\ ASM_SIMP_TAC std_ss [] 328 \\ `n2w (4 * sl) = (n2w sl << 2):word64` by FULL_SIMP_TAC std_ss [WORD_MUL_LSL,word_mul_n2w] 329 \\ ASM_SIMP_TAC std_ss [] 330 \\ SIMP_TAC std_ss [lisp_inv_def,IS_TRUE_def] 331 \\ NTAC 6 (Q.EXISTS_TAC `H_DATA (INR (n2w 0))`) 332 \\ Q.EXISTS_TAC `\x.H_EMP` 333 \\ Q.LIST_EXISTS_TAC [`0`,`[]`,`[]`,`["PEQUAL"]`,`T`] 334 \\ ASM_SIMP_TAC wstd_ss [LENGTH,w2n_n2w,DECIDE ``2*n = n+n``,word_add_n2w] 335 \\ `sl < 18446744073709551616` by DECIDE_TAC 336 \\ ASM_SIMP_TAC std_ss [LENGTH_UPDATE_NTH] 337 \\ REPEAT STRIP_TAC THEN1 338 (SIMP_TAC (srw_ss()) [ok_split_heap_def,APPEND,UNION_SUBSET, 339 ADDR_SET_THM,EMPTY_SUBSET,memory_ok_def,EXTENSION,NOT_IN_EMPTY] 340 \\ SIMP_TAC (srw_ss()) [SUBSET_DEF,IN_DEF,D1_def,R0_def]) 341 THEN1 342 (FULL_SIMP_TAC std_ss [EVERY_DEF,ZIP,APPEND] 343 \\ FULL_SIMP_TAC std_ss [lisp_x_def] \\ Q.EXISTS_TAC `0` \\ EVAL_TAC) 344 THEN1 345 (FULL_SIMP_TAC std_ss [MAP,ref_heap_addr_def] \\ EVAL_TAC) 346 THEN1 347 (FULL_SIMP_TAC wstd_ss [align_add_blast] \\ EVAL_TAC) 348 THEN1 349 (IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [] \\ EVAL_TAC) 350 THEN1 351 (IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [] \\ EVAL_TAC) 352 THEN1 353 (IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [EL_CONS] \\ EVAL_TAC) 354 THEN1 355 (IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [EL_CONS] \\ EVAL_TAC) 356 THEN1 357 (FULL_SIMP_TAC std_ss [EL_UPDATE_NTH]) 358 THEN1 359 (IMP_RES_TAC expand_list \\ FULL_SIMP_TAC std_ss [EL_CONS] \\ EVAL_TAC) 360 THEN1 361 (IMP_RES_TAC expand_list 362 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS,APPEND] 363 \\ FULL_SIMP_TAC std_ss [ref_static_def,LET_DEF,APPEND,ref_full_stack_def, 364 word_arith_lemma1,word64_3232_def,word_arith_lemma1,STAR_ASSOC,word_mul_n2w, 365 word_arith_lemma3,word_arith_lemma4,WORD_ADD_0,ref_stack_def,SEP_EXISTS_THM, 366 ref_static_APPEND,ref_static_def,LENGTH] 367 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 368 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 369 \\ FULL_SIMP_TAC std_ss [EVAL ``(w2w (~0x0w:word64)):word32``] 370 \\ FULL_SIMP_TAC wstd_ss [w2n_n2w,SEP_CLAUSES,mc_full_init_blast_select] 371 \\ `f (sp + 0x6Cw) = w2w (c5' >>> 32)` by SEP_READ_TAC 372 \\ `f (sp + 0x68w) = w2w (c5')` by SEP_READ_TAC 373 \\ `f (sp + 0x64w) = w2w (c4' >>> 32)` by SEP_READ_TAC 374 \\ `f (sp + 0x60w) = w2w (c4')` by SEP_READ_TAC 375 \\ `f (sp + 0x5Cw) = w2w (c3' >>> 32)` by SEP_READ_TAC 376 \\ `f (sp + 0x58w) = w2w (c3')` by SEP_READ_TAC 377 \\ ASM_SIMP_TAC std_ss [] 378 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC,word_arith_lemma4] 379 \\ `sp + 0xE4w + n2w (4 * (sl + 6 + 1)) = sp + n2w sl << 2 + 0x100w` by 380 (SIMP_TAC std_ss [GSYM ADD_ASSOC,LEFT_ADD_DISTRIB,WORD_MUL_LSL] 381 \\ SIMP_TAC bool_ss [GSYM word_add_n2w,GSYM word_mul_n2w,DECIDE ``256 = 0x1C + 0xE4:num``] 382 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC]) 383 \\ FULL_SIMP_TAC std_ss [] 384 \\ SEP_WRITE_TAC) 385 THEN1 386 (FULL_SIMP_TAC std_ss [symtable_inv_def,GSYM BINIT_SYMBOLS_def] 387 \\ IMP_RES_TAC init_func_thm 388 \\ Cases_on `sa1` \\ Cases_on `sa_len` 389 \\ FULL_SIMP_TAC wstd_ss [word_add_n2w,w2n_n2w] 390 \\ Q.PAT_X_ASSUM `n' = xxx` ASSUME_TAC \\ FULL_SIMP_TAC std_ss [] 391 \\ NO_TAC) 392 THEN1 393 (IMP_RES_TAC expand_list 394 \\ FULL_SIMP_TAC std_ss [EL_CONS,UPDATE_NTH_CONS,APPEND] 395 \\ SIMP_TAC std_ss [code_heap_def] 396 \\ Q.LIST_EXISTS_TAC [`[]`,`hs`] 397 \\ ASM_SIMP_TAC std_ss [bs2bytes_def,bc_symbols_ok_def,APPEND,WRITE_CODE_def, 398 NO_CODE_def,WORD_ADD_0,EL_UPDATE_NTH,code_ptr_def])) 399 |> SIMP_RULE std_ss [LET_DEF]; 400 401val mc_full_init_pre_thm = store_thm("mc_full_init_pre_thm", 402 ``mc_full_init_pre (sp,df,f,dg,g) /\ 403 lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds) = 404 lisp_init (a1,a2,sl,sl1,e,ex,cs) io (df,f,dg,g,dd,d,sp,sa1,sa_len,ds)``, 405 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 406 \\ MP_TAC mc_full_init_thm \\ ASM_SIMP_TAC std_ss [] 407 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []); 408 409val _ = save_thm("mc_full_init_thm",mc_full_init_thm); 410 411 412val _ = export_theory(); 413