1open HolKernel Parse boolLib bossLib; val _ = new_theory "lisp_bytecode_step"; 2val _ = ParseExtras.temp_loose_equality() 3 4open lisp_sexpTheory lisp_invTheory lisp_opsTheory lisp_bigopsTheory; 5open lisp_codegenTheory lisp_initTheory lisp_symbolsTheory; 6open lisp_sexpTheory lisp_invTheory lisp_parseTheory; 7open lisp_semanticsTheory lisp_compilerTheory lisp_compiler_opTheory progTheory; 8open compilerLib decompilerLib codegenLib prog_x64Lib prog_x64Theory; 9 10open wordsTheory arithmeticTheory wordsLib listTheory pred_setTheory pairTheory; 11open combinTheory finite_mapTheory addressTheory helperLib sumTheory; 12open set_sepTheory bitTheory fcpTheory stringTheory optionTheory relationTheory; 13open stop_and_copyTheory lisp_consTheory; 14 15infix \\ 16val op \\ = op THEN; 17val RW = REWRITE_RULE; 18val RW1 = ONCE_REWRITE_RULE; 19 20 21val PULL_EXISTS_IMP = METIS_PROVE [] ``((?x. P x) ==> Q) = (!x. P x ==> Q)``; 22val PULL_FORALL_IMP = METIS_PROVE [] ``(Q ==> !x. P x) = (!x. Q ==> P x)``; 23 24fun MERGE_CODE th = let 25 val th = MATCH_MP SPEC_X64_MERGE_CODE th 26 val th = CONV_RULE (RATOR_CONV (SIMP_CONV std_ss [LENGTH,ADD1])) th 27 val th = RW [APPEND] th 28 val _ = not (is_imp (concl th)) orelse fail() 29 in MERGE_CODE th end handle HOL_ERR _ => th; 30 31 32val zLISP_BYTECODE_def = Define ` 33 zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs,p,rs,bc) (stack,input,xbp,rstack,amnt,w) = 34 (SEP_EXISTS x1 x2 x3 x4. 35 zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) 36 (HD (xs ++ Sym "NIL"::stack),x1,x2,x3,x4,bc_state_tree bc, 37 TL (xs ++ Sym "NIL"::stack),bc.consts, 38 IO_STREAMS input bc.io_out,xbp,rs ++ rstack, 39 BC_CODE (bc.code,bc.code_end),amnt,bc.ok) * zPC p * ~zS * 40 cond (bc_inv bc)) \/ zLISP_FAIL (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu)`; 41 42val SPEC_PULL_EXISTS = prove( 43 ``(?x. SPEC m p c (q x)) ==> SPEC m p c (SEP_EXISTS x. q x)``, 44 REPEAT STRIP_TAC \\ `SEP_IMP (q x) ((SEP_EXISTS x. q x))` suffices_by 45 (STRIP_TAC THEN IMP_RES_TAC SPEC_WEAKEN) 46 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ METIS_TAC []); 47 48val SPEC_REMOVE_POST = prove( 49 ``SPEC m p c q ==> SPEC m p c (q \/ q2)``, 50 `SEP_IMP q (q \/ q2)` by FULL_SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] 51 \\ METIS_TAC [SPEC_WEAKEN]); 52 53fun SPEC_EX q = HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC q 54 55val BYTECODE_TAC = 56 `bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 57 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 58 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x1` 59 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2` 60 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x3` 61 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 62 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 63 64val HD_TL = prove( 65 ``HD (xs ++ y::ys)::TL (xs ++ y::ys) = xs ++ y::ys``, 66 Cases_on `xs` \\ FULL_SIMP_TAC std_ss [APPEND,HD,TL]); 67 68val UPDATE_NTH_APPEND1 = prove( 69 ``!xs ys n x. 70 n < LENGTH xs ==> 71 (UPDATE_NTH n x (xs ++ ys) = UPDATE_NTH n x xs ++ ys)``, 72 Induct \\ SIMP_TAC std_ss [LENGTH,APPEND,UPDATE_NTH_CONS] 73 \\ REPEAT STRIP_TAC \\ Cases_on `n = 0` 74 \\ FULL_SIMP_TAC std_ss [APPEND,CONS_11] 75 \\ Q.PAT_X_ASSUM `!ys.bbb` MATCH_MP_TAC \\ DECIDE_TAC); 76 77val code_abbrevs_def = Define ` 78 code_abbrevs cs = 79 abbrev_code_for_compile_inst (cs,EL 9 cs) UNION 80 abbrev_code_for_compile (cs,EL 8 cs) UNION 81 abbrev_code_for_parse (cs,EL 3 cs) UNION 82 abbrev_code_for_print (EL 7 cs) UNION 83 abbrev_code_for_equal (EL 6 cs) UNION 84 abbrev_code_for_cons (EL 5 cs)`; 85 86val SPEC_CODE_ABBREV = prove( 87 ``SPEC m p (c INSERT d) q ==> !d2. d SUBSET d2 ==> SPEC m p (c INSERT d2) q``, 88 REPEAT STRIP_TAC \\ `(c INSERT d2) = (c INSERT d) UNION d2` suffices_by METIS_TAC [SPEC_ADD_CODE] 89 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_INSERT,IN_UNION,SUBSET_DEF] \\ METIS_TAC []); 90 91val (_,_,sts,_) = prog_x64Lib.x64_tools 92 93fun lisp_pc_s th = let 94 val (_,_,_,q) = dest_spec (concl th) 95 val c = MOVE_OUT_CONV ``zPC`` THENC MOVE_OUT_CONV ``zS`` 96 val d = if can dest_star q then I else (RATOR_CONV o RAND_CONV) 97 val c = PRE_CONV c THENC POST_CONV (d c) 98 in CONV_RULE c th end 99 100val pattern = ``(p1,xs1) INSERT (p2:word64,xs2:word8 list) INSERT s`` 101fun sort_swap_conv tm = let 102 val m = fst (match_term pattern tm) 103 val p1 = subst m (mk_var("p1",``:word64``)) 104 val p2 = subst m (mk_var("p2",``:word64``)) 105 fun foo tm = if is_var tm then 0 else tm |> cdr |> cdr |> numSyntax.int_of_term 106 val _ = foo p2 < foo p1 orelse fail() 107 val (x1,s1) = pred_setSyntax.dest_insert tm 108 val (x2,s2) = pred_setSyntax.dest_insert s1 109 in ISPECL [x1,x2,s2] INSERT_COMM end 110 111fun SORT_CODE th = CONV_RULE (REDEPTH_CONV sort_swap_conv) th 112 113fun fix_code th = th 114 |> SIMP_RULE std_ss [INSERT_UNION_INSERT,UNION_EMPTY] 115 |> SORT_CODE 116 |> MERGE_CODE 117 |> MATCH_MP SPEC_CODE_ABBREV |> Q.SPEC `code_abbrevs cs` 118 |> CONV_RULE ((RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss 119 [SUBSET_DEF,code_abbrevs_def,NOT_IN_EMPTY,IN_UNION])) 120 |> RW [] 121 122fun prepare_monop th = th |> fix_code |> RW [SAFE_CAR_def,SAFE_CDR_def] 123 |> HIDE_STATUS_RULE true sts |> lisp_pc_s |> DISCH T 124 125fun prepare_binop th = th |> fix_code 126 |> HIDE_STATUS_RULE true sts |> lisp_pc_s 127 |> Q.INST [`xs`|->`x::xs`] 128 |> SIMP_RULE std_ss [SPEC_MOVE_COND,NOT_CONS_NIL,HD,TL,SEP_CLAUSES] 129 |> DISCH T; 130 131val LENGTH_EQ_LEMMA = prove( 132 ``((1 = LENGTH args) ==> ?arg1. args = [arg1]) /\ 133 ((2 = LENGTH args) ==> ?arg1 arg2. args = [arg1;arg2])``, 134 Cases_on `args` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 135 \\ FULL_SIMP_TAC std_ss [DECIDE ``(1 = n + 1) = (n = 0)``,LENGTH_NIL] 136 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,CONS_11] 137 \\ FULL_SIMP_TAC std_ss [DECIDE ``(2 = n + 1+1) = (n = 0)``,LENGTH_NIL]); 138 139val X64_LISP_iSTEP_DATA = prove( 140 ``!op_name xs1 p1 r1 bc1 xs2 p2 r2 bc2 syms. 141 (bc1.code p1 = SOME (iDATA op_name)) /\ 142 iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 143 SPEC X64_MODEL 144 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,w + n2w p1,MAP (\n. w + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,w)) 145 ((w + n2w p1,bc_ref (p1,syms) (THE (bc1.code p1))) INSERT code_abbrevs cs) 146 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs2,w + n2w p2,MAP (\n. w + n2w n) r2,bc2) (stack,input,xbp,rstack,amnt,w))``, 147 ONCE_REWRITE_TAC [iSTEP_cases] \\ SIMP_TAC std_ss [] 148 \\ REVERSE (REPEAT STRIP_TAC) 149 \\ FULL_SIMP_TAC (srw_ss()) [CONTAINS_BYTECODE_def] 150 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 151 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL]) 152 \\ Q.PAT_X_ASSUM `op_name' = op_name` (fn th => FULL_SIMP_TAC std_ss [th]) 153 \\ FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def] \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 154 \\ FULL_SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,SEP_CLAUSES,SPEC_MOVE_COND] 155 \\ REPEAT STRIP_TAC 156 \\ `bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 157 \\ Cases_on `op_name` 158 \\ ASM_SIMP_TAC std_ss [bc_ref_def,BC_STEP_def,bc_length_def,LENGTH, 159 GSYM word_add_n2w,WORD_ADD_ASSOC] 160 \\ FULL_SIMP_TAC std_ss [EVAL_DATA_OP_def] 161 \\ Q.PAT_X_ASSUM `xxx = f` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 162 \\ IMP_RES_TAC LENGTH_EQ_LEMMA 163 \\ FULL_SIMP_TAC std_ss [REVERSE_DEF,LENGTH,APPEND,HD,TL,EL_CONS] 164 THEN1 165 (SPEC_EX `arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 166 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_CONS) \\ SIMP_TAC std_ss []) 167 THEN1 168 (SPEC_EX `Sym "NIL"` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 169 \\ MATCH_MP_TAC SPEC_REMOVE_POST 170 \\ SIMP_TAC std_ss [LISP_EQUAL_def] \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 171 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_EQUAL) \\ SIMP_TAC std_ss []) 172 THEN1 173 (SPEC_EX `NFIX arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 174 \\ MATCH_MP_TAC SPEC_REMOVE_POST 175 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_LESS) \\ SIMP_TAC std_ss []) 176 THEN1 177 (SPEC_EX `Sym "NIL"` \\ SPEC_EX `Sym "NIL"` 178 \\ SPEC_EX `Sym "NIL"` \\ SPEC_EX `x4` 179 \\ MATCH_MP_TAC SPEC_REMOVE_POST 180 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_SYMBOL_LESS) 181 \\ SIMP_TAC std_ss []) 182 THEN1 183 (SPEC_EX `NFIX arg1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 184 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_ADD) \\ SIMP_TAC std_ss []) 185 THEN1 186 (SPEC_EX `NFIX arg2` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 187 \\ MATCH_MP_TAC SPEC_REMOVE_POST 188 \\ MATCH_MP_TAC (prepare_binop X64_BYTECODE_SUB) \\ SIMP_TAC std_ss []) 189 THEN1 190 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 191 \\ MATCH_MP_TAC SPEC_REMOVE_POST 192 \\ MATCH_MP_TAC (prepare_monop X64_BYTECODE_CONSP) \\ SIMP_TAC std_ss []) 193 THEN1 194 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 195 \\ MATCH_MP_TAC SPEC_REMOVE_POST 196 \\ MATCH_MP_TAC (prepare_monop X64_BYTECODE_NATP) \\ SIMP_TAC std_ss []) 197 THEN1 198 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 199 \\ MATCH_MP_TAC SPEC_REMOVE_POST 200 \\ MATCH_MP_TAC (prepare_monop X64_BYTECODE_SYMBOLP) \\ SIMP_TAC std_ss []) 201 THEN1 202 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 203 \\ MATCH_MP_TAC SPEC_REMOVE_POST 204 \\ MATCH_MP_TAC (prepare_monop X64_BYTECODE_CAR) \\ SIMP_TAC std_ss []) 205 THEN1 206 (SPEC_EX `x1` \\ SPEC_EX `x2` \\ SPEC_EX `x3` \\ SPEC_EX `x4` 207 \\ MATCH_MP_TAC SPEC_REMOVE_POST 208 \\ MATCH_MP_TAC (prepare_monop X64_BYTECODE_CDR) \\ SIMP_TAC std_ss [])); 209 210val ipop = X64_BYTECODE_POP 211 |> fix_code |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND]; 212 213val ipops = X64_BYTECODE_POPS 214 |> fix_code |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 215 |> SIMP_RULE std_ss [w2w_def] |> DISCH ``w2n (j:word30) = LENGTH (ys:SExp list)`` 216 |> SIMP_RULE std_ss [] |> SIMP_RULE std_ss [GSYM w2w_def] 217 |> Q.INST [`xs`|->`ys++zs`] |> SIMP_RULE std_ss [LENGTH_APPEND] 218 |> RW [rich_listTheory.BUTFIRSTN_LENGTH_APPEND] 219 |> Q.INST [`j`|->`n2w (LENGTH (ys:SExp list))`] 220 221val iload = X64_BYTECODE_LOAD 222 |> fix_code |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 223 |> DISCH ``(w2w:29 word->word32) j = n2w i`` 224 |> SIMP_RULE std_ss [word_mul_n2w,AND_IMP_INTRO] 225 |> Q.INST [`j`|->`n2w i`,`x0`|->`HD (xs++y::ys)`,`xs`|->`TL (xs++y::ys)`] 226 |> RW [HD_TL] 227 |> DISCH ``EL (w2n ((n2w i):29 word)) (xs ++ y::ys:SExp list) = EL i xs`` 228 |> SIMP_RULE std_ss [word_mul_n2w,AND_IMP_INTRO] 229 230val istore = X64_BYTECODE_STORE 231 |> fix_code |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 232 |> DISCH ``(w2w:29 word->word32) j = n2w i`` 233 |> DISCH ``(w2n:29 word->num) j = i`` 234 |> SIMP_RULE std_ss [word_mul_n2w,GSYM AND_IMP_INTRO] 235 |> Q.INST [`j`|->`n2w i`,`xs`|->`xs++y::ys`] 236 |> SIMP_RULE std_ss [word_mul_n2w,AND_IMP_INTRO,GSYM LENGTH_NIL] 237 |> DISCH ``UPDATE_NTH i x0 (xs ++ y::ys) = UPDATE_NTH i x0 xs ++ y::ys:SExp list`` 238 |> SIMP_RULE std_ss [word_mul_n2w,AND_IMP_INTRO,GSYM LENGTH_NIL] 239 240val ireturn = X64_LISP_RET |> fix_code 241 |> (fn th => SPEC_FRAME_RULE th ``~zS``) |> DISCH T 242 243val ifail = X64_LISP_RAW_RUNTIME_ERROR |> fix_code |> DISCH T 244 245val iprint = 246 SPEC_COMPOSE_RULE [X64_LISP_PRINT_SEXP,X64_LISP_PRINT_NEWLINE] 247 |> fix_code |> SIMP_RULE std_ss [IO_WRITE_APPEND] 248 |> Q.INST [`io`|->`IO_STREAMS input bc1.io_out`] 249 |> SIMP_RULE std_ss [IO_WRITE_def,APPEND_ASSOC] 250 |> DISCH T 251 252val sw2sw_2compl = blastLib.BBLAST_PROVE 253 ``!w:word32. w <+ 0x80000000w ==> (sw2sw (-w) = -(sw2sw w):word64)``; 254 255val IGNORE_SIGN_EXTEND = prove( 256 ``!m n k. k < 2**n /\ n <= m ==> (SIGN_EXTEND (SUC n) m k = k)``, 257 SIMP_TAC std_ss [SIGN_EXTEND_def,LET_DEF] \\ REPEAT STRIP_TAC 258 \\ ASM_SIMP_TAC std_ss [bitTheory.BIT_def,bitTheory.BITS_THM] 259 \\ ASM_SIMP_TAC std_ss [LESS_DIV_EQ_ZERO] 260 \\ ASM_SIMP_TAC std_ss [EXP] \\ DECIDE_TAC); 261 262val ADDRESS_LEMMA = prove( 263 ``!k. k < 1000 ==> 264 p1 < 1073741824 /\ p2 < 1073741824 ==> 265 (w + n2w p1 + n2w (k + SIGN_EXTEND 32 64 (w2n (n2w p2 - n2w p1 - (n2w k):word32))) = 266 w + n2w p2:word64)``, 267 STRIP_TAC \\ STRIP_TAC \\ SIMP_TAC std_ss [GSYM WORD_SUB_PLUS,word_add_n2w] 268 \\ SIMP_TAC std_ss [word_arith_lemma2] 269 \\ REVERSE (Cases_on `p2 < p1 + k`) \\ ASM_SIMP_TAC std_ss [] THEN1 270 (REPEAT STRIP_TAC \\ SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w] 271 \\ `(p2 - (p1 + k)) < 4294967296` by DECIDE_TAC 272 \\ ASM_SIMP_TAC std_ss [GSYM word_add_n2w] 273 \\ `p2 - (p1 + k) < 2**31` by (SIMP_TAC std_ss [] \\ DECIDE_TAC) 274 \\ IMP_RES_TAC (Q.SPEC `64` IGNORE_SIGN_EXTEND) 275 \\ FULL_SIMP_TAC std_ss [ADD1,word_arith_lemma1] 276 \\ AP_TERM_TAC \\ AP_TERM_TAC \\ DECIDE_TAC) 277 \\ REPEAT STRIP_TAC 278 \\ ASM_SIMP_TAC std_ss [GSYM word_add_n2w, 279 INST_TYPE [``:'a``|->``:32``,``:'b``|->``:64``] sw2sw_def 280 |> SIMP_RULE (std_ss++SIZES_ss) [] |> GSYM] 281 \\ `p1 + k - p2 < 2**31 /\ (p1 + k - p2) < 4294967296` by (SIMP_TAC std_ss [] \\ DECIDE_TAC) 282 \\ `n2w (p1 + k - p2) <+ 0x80000000w:word32` by 283 (FULL_SIMP_TAC (std_ss++SIZES_ss) [word_lo_n2w]) 284 \\ IMP_RES_TAC sw2sw_2compl \\ ASM_SIMP_TAC std_ss [] 285 \\ IMP_RES_TAC (Q.SPEC `64` IGNORE_SIGN_EXTEND) 286 \\ FULL_SIMP_TAC std_ss [ADD1,word_arith_lemma1] 287 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [sw2sw_def,w2n_n2w] 288 \\ SIMP_TAC std_ss [GSYM WORD_ADD_ASSOC] \\ AP_TERM_TAC 289 \\ SIMP_TAC std_ss [WORD_ADD_ASSOC,word_add_n2w] 290 \\ SIMP_TAC std_ss [GSYM word_sub_def] 291 \\ `~(p1 + k < p1 + k - p2)`by DECIDE_TAC 292 \\ ASM_SIMP_TAC std_ss [word_arith_lemma2] 293 \\ AP_TERM_TAC \\ DECIDE_TAC); 294 295val JUMP_ADDRESS_LEMMA = SIMP_RULE std_ss [] (Q.SPEC `6` ADDRESS_LEMMA); 296val JNIL_ADDRESS_LEMMA = SIMP_RULE std_ss [] (Q.SPEC `21` ADDRESS_LEMMA); 297val JNIL_ADDRESS_LEMMA2 = SIMP_RULE std_ss [] (Q.SPEC `14` ADDRESS_LEMMA); 298 299val (ijump_raw,ijump) = let 300 val ((th,_,_),_) = prog_x64Lib.x64_spec "48E9" 301 val th = Q.INST [`imm32`|->`n2w p2 - n2w p1 - 6w`,`rip`|->`w + n2w p1`] th 302 |> DISCH ``p1 < 1073741824 /\ p2 < 1073741824`` 303 |> SIMP_RULE std_ss [JUMP_ADDRESS_LEMMA] 304 |> RW [GSYM SPEC_MOVE_COND] 305 |> MATCH_MP SPEC_FRAME 306 |> Q.SPEC `zLISP (a1,a2,sl,sl1,e,ex,cs,ok,rbp,ddd) 307 (x0,x1,x2,x3,x4,x5,xs,io,xbp,qs,code,amnt) * ~zS` 308 |> lisp_pc_s |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 309 val th2 = DISCH_ALL (fix_code (UNDISCH th)) 310 in (th,th2) end 311 312val icall = let 313 val th = X64_LISP_CALL_IMM 314 val th = fix_code th 315 val th = Q.INST [`imm32`|->`n2w p2 - n2w p1 - 6w`,`p`|->`w + n2w p1`] th 316 |> DISCH ``p1 < 1073741824 /\ p2 < 1073741824`` 317 |> SIMP_RULE std_ss [JUMP_ADDRESS_LEMMA] 318 |> RW [GSYM SPEC_MOVE_COND] 319 |> MATCH_MP SPEC_FRAME 320 |> Q.SPEC `~zS` 321 |> lisp_pc_s |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 322 in th end; 323 324val inum = SPEC_COMPOSE_RULE [X64_LISP_PUSH_0,X64_LISP_ASSIGN_ANY_VAL] 325 |> fix_code |> RW [SPEC_MOVE_COND] 326 327val ilookup = X64_LISP_CONST_LOAD 328 |> MATCH_MP SPEC_FRAME |> Q.SPEC `~zS` 329 |> fix_code |> lisp_pc_s 330 |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 331 |> Q.INST [`x0`|->`Val x`] |> SIMP_RULE std_ss [getVal_def,isVal_def] 332 333val icall_sym = X64_BYTECODE_CALL_SYM |> fix_code |> lisp_pc_s 334 |> Q.INST [`p`|->`w + n2w p1`] 335 |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 336 |> DISCH_ALL |> RW [AND_IMP_INTRO] 337 338val ijump_sym = X64_BYTECODE_JUMP_SYM |> fix_code |> lisp_pc_s 339 |> Q.INST [`p`|->`w + n2w p1`] 340 |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 341 342val (ijnil1,ijnil2) = let 343 fun the (SOME x) = x | the _ = fail() 344 val ((th1,_,_),x) = x64_spec "480F84" 345 val (th2,_,_) = the x 346 val th1 = SPEC_COMPOSE_RULE [X64_LISP_MOVE10, X64_BYTECODE_POP, 347 X64_LISP_TEST_SYM_0_1,th1] 348 val th1 = RW [precond_def] th1 |> Q.INST [`xs`|->`x::xs`] 349 |> HIDE_STATUS_RULE true sts |> lisp_pc_s |> fix_code 350 |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES,ADD_ASSOC] 351 |> Q.INST [`imm32`|->`n2w p2 - n2w p1 - 21w`,`p`|->`w + n2w p1`] 352 |> DISCH ``p1 < 1073741824 /\ p2 < 1073741824`` 353 |> SIMP_RULE (std_ss++sep_cond_ss) [JNIL_ADDRESS_LEMMA,SPEC_MOVE_COND] 354 |> RW [AND_IMP_INTRO] 355 val th2 = SPEC_COMPOSE_RULE [X64_LISP_MOVE10, X64_BYTECODE_POP, 356 X64_LISP_TEST_SYM_0_1,th2] 357 val th2 = RW [precond_def] th2 |> Q.INST [`xs`|->`x::xs`] 358 |> HIDE_STATUS_RULE true sts |> lisp_pc_s |> fix_code 359 |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES,ADD_ASSOC] 360 |> Q.INST [`imm32`|->`n2w p2 - n2w p1 - 21w`,`p`|->`w + n2w p1`] 361 |> SIMP_RULE (std_ss++sep_cond_ss) [JNIL_ADDRESS_LEMMA,SPEC_MOVE_COND] 362 in (th1,th2) end; 363 364val BC_PRINT_LEMMA = prove( 365 ``(bc_state_tree (BC_PRINT bc s) = bc_state_tree bc) /\ 366 ((BC_PRINT bc s).code = bc.code) /\ 367 ((BC_PRINT bc s).code_end = bc.code_end) /\ 368 (bc_inv (BC_PRINT bc s) = bc_inv bc)``, 369 SIMP_TAC (srw_ss()) [bc_state_tree_def,BC_PRINT_def,const_tree_def, 370 bc_inv_def,BC_CODE_OK_def]); 371 372val X64_LISP_iSTEP_MOST_CASES = prove( 373 ``bc_symbols_ok syms [THE (bc1.code p1)] /\ 374 ~(bc1.code p1 = SOME iCOMPILE) /\ 375 (!s. ~(bc1.code p1 = SOME (iCONST_SYM s))) /\ 376 p1 < 1073741824 /\ 377 iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 378 SPEC X64_MODEL 379 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,EL 4 cs + n2w p1,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 380 ((EL 4 cs + n2w p1,bc_ref (p1,syms) (THE (bc1.code p1))) INSERT code_abbrevs cs) 381 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs2,EL 4 cs + n2w p2,MAP (\n. EL 4 cs + n2w n) r2,bc2) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 382 Cases_on `?op_name. bc1.code p1 = SOME (iDATA op_name)` 383 THEN1 (METIS_TAC [X64_LISP_iSTEP_DATA]) 384 \\ ONCE_REWRITE_TAC [iSTEP_cases] \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 385 \\ FULL_SIMP_TAC std_ss [BC_STEP_def,CONTAINS_BYTECODE_def,bc_ref_def] 386 \\ SIMP_TAC std_ss [zLISP_BYTECODE_def] 387 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 388 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 389 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 390 THEN1 (* pop *) 391 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST \\ MATCH_MP_TAC ipop 392 \\ Cases_on `xs2` \\ SIMP_TAC (srw_ss()) []) 393 THEN1 (* pops *) 394 (BYTECODE_TAC \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC] 395 \\ MATCH_MP_TAC SPEC_REMOVE_POST \\ MATCH_MP_TAC ipops 396 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [w2n_n2w]) 397 THEN1 (* num *) 398 (BYTECODE_TAC \\ SIMP_TAC std_ss [word_add_n2w] 399 \\ Cases_on `xs1 ++ Sym "NIL"::stack` 400 THEN1 (Cases_on `xs1` \\ FULL_SIMP_TAC (srw_ss()) []) 401 \\ FULL_SIMP_TAC std_ss [HD,TL] 402 \\ MATCH_MP_TAC inum \\ ASM_SIMP_TAC std_ss []) 403 THEN1 (* sym *) 404 (FULL_SIMP_TAC (srw_ss()) []) 405 THEN1 (* lookup *) 406 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 407 \\ MATCH_MP_TAC ilookup \\ ASM_SIMP_TAC std_ss []) 408 THEN1 (* data *) 409 (FULL_SIMP_TAC (srw_ss()) []) 410 THEN1 (* iload *) 411 (BYTECODE_TAC \\ MATCH_MP_TAC iload 412 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,LENGTH_APPEND] 413 \\ ASM_SIMP_TAC std_ss [rich_listTheory.EL_APPEND1] \\ DECIDE_TAC) 414 THEN1 (* istore *) 415 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST \\ MATCH_MP_TAC istore 416 \\ ASM_SIMP_TAC (std_ss++SIZES_ss) [w2w_def,w2n_n2w,LENGTH_APPEND] 417 \\ ASM_SIMP_TAC std_ss [LENGTH_UPDATE_NTH,LENGTH_APPEND,LENGTH,ADD1] 418 \\ ASM_SIMP_TAC std_ss [UPDATE_NTH_APPEND1] \\ DECIDE_TAC) 419 THEN1 (* ijump *) 420 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 421 \\ MATCH_MP_TAC ijump \\ ASM_SIMP_TAC std_ss []) 422 THEN1 (* icall *) 423 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 424 \\ SIMP_TAC std_ss [MAP,GSYM word_add_n2w,WORD_ADD_ASSOC,APPEND] 425 \\ MATCH_MP_TAC icall \\ ASM_SIMP_TAC std_ss []) 426 THEN1 (* ireturn *) 427 (BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 428 \\ FULL_SIMP_TAC std_ss [MAP,APPEND] 429 \\ MATCH_MP_TAC ireturn \\ SIMP_TAC std_ss []) 430 THEN1 (* ijnil *) 431 (`bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 432 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 433 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x` 434 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2` 435 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x3` 436 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 437 \\ Cases_on `xs2 ++ Sym "NIL"::stack` 438 THEN1 (Cases_on `xs2` \\ FULL_SIMP_TAC (srw_ss()) []) 439 \\ FULL_SIMP_TAC std_ss [HD,TL,MAP,GSYM word_add_n2w,WORD_ADD_ASSOC] 440 \\ MATCH_MP_TAC SPEC_REMOVE_POST 441 \\ Cases_on `x = Sym "NIL"` \\ FULL_SIMP_TAC std_ss [] 442 THEN1 (MATCH_MP_TAC (GEN_ALL ijnil1) \\ ASM_SIMP_TAC std_ss []) 443 \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w,WORD_ADD_ASSOC] 444 \\ MATCH_MP_TAC (GEN_ALL ijnil2) \\ ASM_SIMP_TAC std_ss []) 445 THEN1 (* ijump_sym *) 446 (`bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 447 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 448 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val p2` 449 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val p2` 450 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val n` 451 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 452 \\ Cases_on `xs2 ++ Sym "NIL"::stack` 453 THEN1 (Cases_on `xs2` \\ FULL_SIMP_TAC (srw_ss()) []) 454 \\ FULL_SIMP_TAC std_ss [HD,TL,MAP,GSYM word_add_n2w,WORD_ADD_ASSOC] 455 \\ MATCH_MP_TAC (GEN_ALL ijump_sym) \\ ASM_SIMP_TAC std_ss []) 456 THEN1 (* icall_sym *) 457 (`bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 458 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 459 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val p2` 460 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val p2` 461 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Val n` 462 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 463 \\ Cases_on `xs2 ++ Sym "NIL"::stack` 464 THEN1 (Cases_on `xs2` \\ FULL_SIMP_TAC (srw_ss()) []) 465 \\ FULL_SIMP_TAC std_ss [HD,TL,MAP,GSYM word_add_n2w,WORD_ADD_ASSOC,APPEND] 466 \\ MATCH_MP_TAC (GEN_ALL icall_sym) \\ ASM_SIMP_TAC std_ss []) 467 THEN1 (* ifail *) 468 (BYTECODE_TAC \\ ONCE_REWRITE_TAC [SEP_DISJ_COMM] 469 \\ MATCH_MP_TAC SPEC_REMOVE_POST 470 \\ MATCH_MP_TAC ifail \\ SIMP_TAC std_ss []) 471 THEN1 (* iprint *) 472 (BYTECODE_TAC \\ ASM_SIMP_TAC std_ss [BC_PRINT_LEMMA,SEP_CLAUSES] 473 \\ SIMP_TAC (srw_ss()) [BC_PRINT_def] \\ MATCH_MP_TAC iprint 474 \\ SIMP_TAC std_ss []) 475 THEN1 (* ok false *) 476 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 477 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE])); 478 479val X64_LISP_iSTEP_LAST_RETURN_LEMMA = prove( 480 ``(bc1.code 0 = SOME iRETURN) ==> 481 SPEC X64_MODEL 482 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,EL 4 cs + 0w,[],bc1) (stack,input,xbp,r::rstack,amnt,EL 4 cs)) 483 ((EL 4 cs + 0w,bc_ref (p1,syms) (THE (bc1.code 0))) INSERT code_abbrevs cs) 484 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,r,[],bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 485 FULL_SIMP_TAC std_ss [BC_STEP_def,CONTAINS_BYTECODE_def,bc_ref_def] 486 \\ SIMP_TAC std_ss [zLISP_BYTECODE_def] 487 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 488 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 489 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 490 \\ BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 491 \\ FULL_SIMP_TAC std_ss [MAP,APPEND] 492 \\ MATCH_MP_TAC ireturn \\ SIMP_TAC std_ss []); 493 494val SPEC_X64_STRENGTHEN_CODE = prove( 495 ``SPEC X64_MODEL p ((w,xs) INSERT dd) q ==> 496 SPEC X64_MODEL p ((w,xs) INSERT dd) q``, 497 SIMP_TAC std_ss []); 498 499val SPEC_PRE_DISJ_REMOVE = prove( 500 ``SPEC x (p \/ r) c (q \/ r) = SPEC x p c (q \/ r)``, 501 SIMP_TAC std_ss [SPEC_PRE_DISJ] \\ REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 502 \\ ASM_SIMP_TAC std_ss [] 503 \\ MATCH_MP_TAC (SIMP_RULE std_ss [PULL_FORALL_IMP,AND_IMP_INTRO] SPEC_WEAKEN) 504 \\ Q.EXISTS_TAC `r` \\ SIMP_TAC std_ss [SPEC_REFL] 505 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def]); 506 507val cond_EXISTS = prove( 508 ``cond (?x. P x) = SEP_EXISTS x. cond (P x)``, 509 SIMP_TAC std_ss [cond_def,SEP_EXISTS,FUN_EQ_THM] \\ METIS_TAC []); 510 511val code_mem_BOUND = prove( 512 ``!bs bc n. code_ptr bc + code_length bs <= n ==> 513 (code_mem (WRITE_CODE bc bs) n = code_mem bc n)``, 514 Induct \\ Cases_on `bc` \\ Cases_on `p` 515 \\ SIMP_TAC std_ss [code_length_def,WRITE_CODE_def,code_ptr_def] \\ STRIP_TAC 516 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `BC_CODE ((r =+ SOME h) q,r + bc_length h)`) 517 \\ FULL_SIMP_TAC std_ss [code_ptr_def,ADD_ASSOC] \\ REPEAT STRIP_TAC 518 \\ RES_TAC \\ SIMP_TAC std_ss [code_mem_def,APPLY_UPDATE_THM] 519 \\ `0 < bc_length h` by 520 (Cases_on `h` \\ EVAL_TAC \\ Cases_on `l` \\ EVAL_TAC) 521 \\ `~(r = n)` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss []); 522 523val code_length_LESS = prove( 524 ``!bs. (code_mem (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs) p = SOME x) ==> 525 p < code_length bs``, 526 REPEAT STRIP_TAC \\ CCONTR_TAC \\ Q.PAT_X_ASSUM `xx = yy` MP_TAC 527 \\ `code_ptr (BC_CODE ((\x. NONE),0)) + code_length bs <= p` by 528 (FULL_SIMP_TAC std_ss [code_ptr_def] \\ DECIDE_TAC) 529 \\ IMP_RES_TAC code_mem_BOUND \\ ASM_SIMP_TAC std_ss [] 530 \\ FULL_SIMP_TAC std_ss [code_mem_def]); 531 532val WRITE_CODE_APPEND = prove( 533 ``!xs ys x. WRITE_CODE x (xs ++ ys) = WRITE_CODE (WRITE_CODE x xs) ys``, 534 Induct \\ Cases_on `x` \\ Cases_on `p` 535 \\ ASM_SIMP_TAC std_ss [WRITE_CODE_def,APPEND]); 536 537val WRITE_CODE_MEM_LEMMA = prove( 538 ``!bs m l m1 l1. 539 (WRITE_CODE (BC_CODE (m,l)) bs = BC_CODE (m1,l1)) ==> 540 !p x. (m1 p = SOME x) ==> MEM x bs \/ (m p = SOME x)``, 541 Induct \\ SIMP_TAC (srw_ss()) [MEM,WRITE_CODE_def] 542 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 543 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 544 \\ Cases_on `l = p` \\ FULL_SIMP_TAC std_ss []); 545 546val WRITE_CODE_MEM = prove( 547 ``!bs. (code_mem (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs) p = SOME x) ==> MEM x bs``, 548 REPEAT STRIP_TAC 549 \\ Cases_on `WRITE_CODE (BC_CODE ((\x. NONE),0)) bs` \\ Cases_on `p'` 550 \\ MP_TAC (Q.SPECL [`bs`,`\x.NONE`,`0`,`q`,`r`] WRITE_CODE_MEM_LEMMA) 551 \\ FULL_SIMP_TAC std_ss [code_mem_def] \\ METIS_TAC []); 552 553val MEM_bc_symbols_ok = prove( 554 ``!xs. MEM x xs /\ bc_symbols_ok sym xs ==> bc_symbols_ok sym [x]``, 555 Induct \\ SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC 556 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def]); 557 558val bc_symbols_ok_IMP = prove( 559 ``bc_symbols_ok sym bs /\ 560 (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs = BC_CODE (bc1.code,bc1.code_end)) /\ 561 (bc1.code p1 = SOME x) ==> 562 bc_symbols_ok sym [x]``, 563 REPEAT STRIP_TAC \\ MP_TAC (Q.INST [`p`|->`p1`] (SPEC_ALL WRITE_CODE_MEM)) 564 \\ ASM_SIMP_TAC std_ss [code_mem_def] \\ METIS_TAC [MEM_bc_symbols_ok]); 565 566val SPEC_SUBSET_CODE_UNION = prove( 567 ``!x p c q. SPEC x p (c UNION d) q ==> 568 !c'. c SUBSET c' ==> SPEC x p (c' UNION d) q``, 569 REPEAT STRIP_TAC 570 \\ `(c UNION d) SUBSET (c' UNION d)` by 571 (FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 572 \\ METIS_TAC [SPEC_SUBSET_CODE]); 573 574val CODE_POOL_UNION_LEMMA = prove( 575 ``!c1 c2 i. 576 ?r. CODE_POOL i c1 * CODE_POOL i c2 = CODE_POOL i (c1 UNION c2) * r``, 577 REPEAT STRIP_TAC \\ REWRITE_TAC [CODE_POOL_def,IMAGE_UNION,BIGUNION_UNION,STAR_def] 578 \\ Q.EXISTS_TAC `cond (DISJOINT (BIGUNION (IMAGE i c1)) (BIGUNION (IMAGE i c2)))` 579 \\ SIMP_TAC std_ss [SPLIT_def,cond_def,UNION_EMPTY,DISJOINT_EMPTY] 580 \\ FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ METIS_TAC []); 581 582val SPEC_CODE_UNION = store_thm("SPEC_CODE_UNION", 583 ``!x p c d q. SPEC x p (c UNION d) q ==> 584 SPEC x (CODE_POOL ((FST (SND (SND x))):'a -> 'b -> bool) c * p) d 585 (CODE_POOL (FST (SND (SND x))) c * q)``, 586 STRIP_TAC \\ `?x1 x2 x3 x4 x5. x = (x1,x2,x3,x4,x5)` by METIS_TAC [PAIR] 587 \\ FULL_SIMP_TAC std_ss [SPEC_def,RUN_def] \\ REPEAT STRIP_TAC 588 \\ MP_TAC (Q.ISPEC `x3:'a->'b->bool` (Q.SPECL [`c`,`d`] (GSYM CODE_POOL_UNION_LEMMA))) 589 \\ REPEAT STRIP_TAC 590 \\ Q.PAT_X_ASSUM `!state. bbb` (MP_TAC o Q.SPECL [`state`,`r * r'`]) 591 \\ FULL_SIMP_TAC std_ss [AC STAR_ASSOC STAR_COMM]); 592 593val SPEC_zCODE_SPLIT_UNION = prove( 594 ``SPEC X64_MODEL p (c UNION d) q ==> 595 SPEC X64_MODEL (p * zCODE c) d (q * zCODE c)``, 596 SIMP_TAC std_ss [X64_MODEL_def,zCODE_def] \\ REPEAT STRIP_TAC 597 \\ IMP_RES_TAC SPEC_CODE_UNION \\ FULL_SIMP_TAC (std_ss++star_ss) []); 598 599val SPEC_DERIVE = prove( 600 ``SPEC m p c q /\ SEP_IMP p1 p /\ SEP_IMP q q1 ==> SPEC m p1 c q1``, 601 METIS_TAC [SPEC_STRENGTHEN,SPEC_WEAKEN]); 602 603fun INST_EXISTS_TAC (hyps,goal) = let 604 val (v,tm) = dest_exists goal 605 val w = mk_var(implode (filter (fn x => x <> #"'") (explode (fst (dest_var v)))), type_of v) 606 in EXISTS_TAC w (hyps,goal) end handle HOL_ERR _ => NO_TAC (hyps,goal) 607 608val SEP_IMP_LEMMA = prove( 609 ``SEP_IMP (p1 * m) q1 /\ SEP_IMP (p2 * m) q2 ==> 610 SEP_IMP ((p1 \/ p2) * m) (q1 \/ q2)``, 611 SIMP_TAC std_ss [SEP_CLAUSES] 612 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_DISJ_def] \\ METIS_TAC []); 613 614val SEP_EXISTS_DISJ_REV = prove( 615 ``(SEP_EXISTS x. p x \/ q) = (SEP_EXISTS x. p x) \/ q``, 616 SIMP_TAC std_ss [SEP_CLAUSES]); 617 618val WRITE_CODE_IMP_LENGTH = prove( 619 ``!bs n x. (WRITE_CODE (BC_CODE (x,n)) bs = BC_CODE (q,p)) ==> 620 (p = n + code_length bs)``, 621 Induct \\ SIMP_TAC (srw_ss()) [WRITE_CODE_def,code_length_def] 622 \\ REPEAT STRIP_TAC \\ RES_TAC \\ DECIDE_TAC); 623 624val code_mem_SPLIT = prove( 625 ``!bs n p1. 626 ((code_mem (WRITE_CODE (BC_CODE ((\x.NONE),n)) bs)) p1 = SOME x) ==> 627 ?bs1 bs2. (bs = bs1 ++ [x] ++ bs2) /\ (p1 = code_length bs1 + n)``, 628 HO_MATCH_MP_TAC SNOC_INDUCT 629 \\ SIMP_TAC std_ss [WRITE_CODE_def,MEM,code_mem_def] 630 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [SNOC_APPEND] 631 \\ FULL_SIMP_TAC std_ss [WRITE_CODE_APPEND] 632 \\ Cases_on `(WRITE_CODE (BC_CODE ((\x. NONE),n)) bs)` 633 \\ Cases_on `p` \\ FULL_SIMP_TAC std_ss [WRITE_CODE_def,code_mem_def] 634 \\ FULL_SIMP_TAC std_ss [APPLY_UPDATE_THM] 635 \\ Cases_on `r = p1` \\ FULL_SIMP_TAC std_ss [] THEN1 636 (Q.LIST_EXISTS_TAC [`bs`,`[]`] \\ FULL_SIMP_TAC std_ss [APPEND_NIL] 637 \\ IMP_RES_TAC WRITE_CODE_IMP_LENGTH \\ DECIDE_TAC) 638 \\ Q.PAT_X_ASSUM `!xx.bbb` (MP_TAC o Q.SPECL [`n`,`p1`]) 639 \\ FULL_SIMP_TAC std_ss [code_mem_def] 640 \\ REPEAT STRIP_TAC 641 \\ Q.LIST_EXISTS_TAC [`bs1`,`bs2 ++ [x']`] 642 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC]); 643 644val WRITE_CODE_NONE_LEMMA = prove( 645 ``(WRITE_CODE (BC_CODE ((\x.NONE),n)) bs = BC_CODE (c,m)) ==> 646 !p1. (c p1 = SOME x) ==> ?bs1 bs2. (bs = bs1 ++ [x] ++ bs2) /\ 647 (p1 = code_length bs1 + n)``, 648 REPEAT STRIP_TAC \\ MP_TAC (SPEC_ALL code_mem_SPLIT) 649 \\ FULL_SIMP_TAC std_ss [code_mem_def]); 650 651val bs2bytes_APPEND = prove( 652 ``!xs ys i. bs2bytes (i,sym) (xs ++ ys) = 653 bs2bytes (i,sym) xs ++ bs2bytes (code_length xs + i,sym) ys``, 654 Induct \\ ASM_SIMP_TAC std_ss [APPEND,bs2bytes_def,code_length_def] 655 \\ SIMP_TAC std_ss [APPEND_ASSOC,AC ADD_COMM ADD_ASSOC]); 656 657val bs_symbol_ok_APPEND = prove( 658 ``!xs ys. bc_symbols_ok sym (xs ++ ys) = bc_symbols_ok sym xs /\ bc_symbols_ok sym ys``, 659 Induct \\ SIMP_TAC std_ss [APPEND,bc_symbols_ok_def] \\ Cases_on `h` 660 \\ FULL_SIMP_TAC std_ss [APPEND,bc_symbols_ok_def,CONJ_ASSOC]); 661 662val LENGTH_bs2bytes = prove( 663 ``!bs sym n. LENGTH (bs2bytes (n,sym) bs) = code_length bs``, 664 Induct \\ ASM_SIMP_TAC std_ss [bs2bytes_def,code_length_def,LENGTH, 665 bc_length_def,LENGTH_APPEND] 666 \\ Cases \\ EVAL_TAC \\ SIMP_TAC std_ss [] 667 \\ Cases_on `l` \\ EVAL_TAC \\ SIMP_TAC std_ss []); 668 669val code_heap_IMP = prove( 670 ``code_heap (BC_CODE (bc1.code,bc1.code_end)) (sym,w1,w2,w3,dd,d) /\ 671 (bc1.code p1 = SOME x) ==> 672 bc_symbols_ok sym [x] /\ 673 ?xx. (one_byte_list (w1 + n2w p1) (bc_ref (p1,sym) x) * xx) (fun2set (d,dd))``, 674 SIMP_TAC std_ss [code_heap_def] \\ STRIP_TAC 675 \\ IMP_RES_TAC WRITE_CODE_NONE_LEMMA 676 \\ FULL_SIMP_TAC std_ss [bs2bytes_APPEND,bs_symbol_ok_APPEND] 677 \\ FULL_SIMP_TAC std_ss [one_byte_list_APPEND,LENGTH_APPEND,GSYM word_add_n2w] 678 \\ FULL_SIMP_TAC std_ss [WORD_ADD_ASSOC,bs2bytes_def,APPEND_NIL,LENGTH_bs2bytes] 679 \\ Q.PAT_X_ASSUM `ddd (fun2set (d,dd))` MP_TAC 680 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 681 \\ ONCE_REWRITE_TAC [STAR_COMM] 682 \\ SIMP_TAC std_ss [GSYM STAR_ASSOC] 683 \\ REPEAT STRIP_TAC 684 \\ ONCE_REWRITE_TAC [STAR_COMM] 685 \\ METIS_TAC []); 686 687val zLISP_BYTECODE_MOVE_CODE = prove( 688 ``(!ddd syms cu. 689 (bc1.code p1 = SOME x) /\ bc_symbols_ok syms [x] ==> 690 SPEC X64_MODEL 691 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,pp1,r1,bc1) (stack,input,xbp,rstack1,amnt,EL 4 cs)) 692 ((EL 4 cs + n2w p1,bc_ref (p1,syms) x) INSERT code_abbrevs cs) 693 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs2,pp2,r2,bc2) (stack,input,xbp,rstack2,amnt,EL 4 cs))) ==> 694 (bc1.code p1 = SOME x) ==> 695 SPEC X64_MODEL 696 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,pp1,r1,bc1) (stack,input,xbp,rstack1,amnt,EL 4 cs)) 697 (code_abbrevs cs) 698 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs2,pp2,r2,bc2) (stack,input,xbp,rstack2,amnt,EL 4 cs))``, 699 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 700 \\ Q.PAT_X_ASSUM `!ddd.bb` (ASSUME_TAC o Q.SPEC `NONE`) 701 \\ FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,SPEC_PRE_DISJ_REMOVE] 702 \\ SIMP_TAC std_ss [Once zLISP_def,Once zCODE_MEMORY_def,Once lisp_inv_def] 703 \\ FULL_SIMP_TAC std_ss [SEP_CLAUSES,zCODE_UNCHANGED_def,cond_EXISTS] 704 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ REPEAT STRIP_TAC 705 \\ SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND] \\ REPEAT STRIP_TAC 706 \\ Q.PAT_X_ASSUM `!xx.bb` (MP_TAC o Q.SPECL [`INIT_SYMBOLS ++ sym`,`SOME (dd,d)`]) 707 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 708 THEN1 (FULL_SIMP_TAC std_ss [code_heap_def] \\ METIS_TAC [bc_symbols_ok_IMP]) 709 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [X64_SPEC_EXLPODE_CODE_LEMMA] 710 \\ IMP_RES_TAC SPEC_SUBSET_CODE_UNION 711 \\ POP_ASSUM (MP_TAC o Q.SPEC `zCODE_SET dd d`) 712 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 713 (SIMP_TAC std_ss [zCODE_SET_def,SUBSET_DEF,GSPECIFICATION] 714 \\ SIMP_TAC std_ss [PULL_EXISTS_IMP,CONS_11] 715 \\ IMP_RES_TAC code_heap_IMP 716 \\ POP_ASSUM (K ALL_TAC) 717 \\ POP_ASSUM MP_TAC 718 \\ Q.SPEC_TAC (`bc_ref (p1,INIT_SYMBOLS ++ sym) x`,`xs`) 719 \\ Q.SPEC_TAC (`xx`,`res`) 720 \\ Q.SPEC_TAC (`p1`,`i`) 721 \\ Induct_on `xs` \\ SIMP_TAC std_ss [LENGTH] 722 \\ SIMP_TAC std_ss [one_byte_list_def] 723 \\ NTAC 4 STRIP_TAC \\ Cases 724 THEN1 (FULL_SIMP_TAC std_ss [EL,HD,WORD_ADD_0] \\ SEP_R_TAC \\ SIMP_TAC std_ss []) 725 \\ SIMP_TAC std_ss [EL,TL] \\ POP_ASSUM MP_TAC 726 \\ ONCE_REWRITE_TAC [STAR_COMM] 727 \\ SIMP_TAC std_ss [STAR_ASSOC] 728 \\ ONCE_REWRITE_TAC [STAR_COMM] 729 \\ SIMP_TAC std_ss [word_add_n2w,GSYM WORD_ADD_ASSOC] 730 \\ STRIP_TAC \\ RES_TAC 731 \\ STRIP_TAC \\ RES_TAC 732 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [word_arith_lemma1] 733 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,ADD1]) 734 \\ POP_ASSUM (K ALL_TAC) \\ REPEAT STRIP_TAC 735 \\ IMP_RES_TAC SPEC_zCODE_SPLIT_UNION 736 \\ POP_ASSUM MP_TAC \\ POP_ASSUM (K ALL_TAC) 737 \\ REPEAT STRIP_TAC 738 \\ IMP_RES_TAC SPEC_DERIVE 739 \\ FULL_SIMP_TAC std_ss [PULL_FORALL_IMP,AND_IMP_INTRO] 740 \\ POP_ASSUM MATCH_MP_TAC 741 \\ REPEAT STRIP_TAC THEN1 742 (SIMP_TAC std_ss [SEP_EXISTS_DISJ_REV] \\ MATCH_MP_TAC SEP_IMP_LEMMA 743 \\ SIMP_TAC std_ss [zLISP_def,zCODE_UNCHANGED_def,SEP_CLAUSES,zCODE_MEMORY_def] 744 \\ REPEAT STRIP_TAC THEN1 745 (REPEAT (POP_ASSUM (K ALL_TAC)) 746 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ REPEAT STRIP_TAC 747 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 748 \\ REPEAT (Q.PAT_X_ASSUM `dddd = ddddd` (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 749 \\ REPEAT INST_EXISTS_TAC 750 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES,zCODE_MEMORY_def]) 751 \\ FULL_SIMP_TAC std_ss [zLISP_FAIL_def] 752 \\ SIMP_TAC std_ss [zLISP_def,zCODE_UNCHANGED_def,SEP_CLAUSES,zCODE_MEMORY_def] 753 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 754 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] \\ REPEAT STRIP_TAC 755 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR] 756 \\ REPEAT (Q.PAT_X_ASSUM `dddd = ddddd` (fn th => FULL_SIMP_TAC std_ss [th])) 757 \\ Q.LIST_EXISTS_TAC [`SOME T`,`vars`] 758 \\ POP_ASSUM MP_TAC \\ Q.SPEC_TAC (`vars`,`x`) 759 \\ SIMP_TAC std_ss [FORALL_PROD,zLISP_def,SEP_CLAUSES,SEP_EXISTS_THM] 760 \\ REPEAT STRIP_TAC 761 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,zCODE_UNCHANGED_def] 762 \\ REPEAT (Q.PAT_X_ASSUM `dddd = ddddd` (fn th => FULL_SIMP_TAC std_ss [GSYM th])) 763 \\ REPEAT INST_EXISTS_TAC 764 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES,zCODE_MEMORY_def]) 765 \\ SIMP_TAC std_ss [SEP_CLAUSES,zLISP_def,zCODE_UNCHANGED_def] 766 \\ SIMP_TAC std_ss [lisp_inv_def,cond_EXISTS,SEP_CLAUSES] 767 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] 768 \\ REPEAT STRIP_TAC 769 \\ REPEAT INST_EXISTS_TAC 770 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [cond_STAR,zCODE_UNCHANGED_def] 771 \\ FULL_SIMP_TAC (std_ss++star_ss) [SEP_CLAUSES,zCODE_MEMORY_def]); 772 773val X64_LISP_iSTEP_LAST_RETURN = prove( 774 ``(bc1.code 0 = SOME iRETURN) ==> 775 SPEC X64_MODEL 776 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 4 cs,[],bc1) (stack,input,xbp,r::rstack,amnt,EL 4 cs)) 777 (code_abbrevs cs) 778 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,r,[],bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 779 FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 780 \\ MATCH_MP_TAC zLISP_BYTECODE_MOVE_CODE \\ REPEAT STRIP_TAC 781 \\ IMP_RES_TAC X64_LISP_iSTEP_LAST_RETURN_LEMMA 782 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [WORD_ADD_0,bc_ref_def]); 783 784val icompile = 785 X64_LISP_COMPILE_INST |> lisp_pc_s 786 |> Q.INST [`p`|->`EL 9 cs`] |> MATCH_MP SPEC_SUBSET_CODE 787 |> Q.SPEC `(code_abbrevs cs)` 788 |> CONV_RULE ((RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss 789 [SUBSET_DEF,code_abbrevs_def,NOT_IN_EMPTY,IN_UNION])) |> RW [] 790 |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 791 792val icompile_fail = 793 X64_LISP_COMPILE_INST_FAIL |> lisp_pc_s 794 |> Q.INST [`p`|->`EL 9 cs`] |> MATCH_MP SPEC_SUBSET_CODE 795 |> Q.SPEC `(code_abbrevs cs)` 796 |> CONV_RULE ((RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss 797 [SUBSET_DEF,code_abbrevs_def,NOT_IN_EMPTY,IN_UNION])) |> RW [] 798 |> SIMP_RULE (std_ss++sep_cond_ss) [SPEC_MOVE_COND] 799 |> CONV_RULE ((RAND_CONV o RAND_CONV) 800 (SIMP_CONV std_ss [zLISP_def,lisp_inv_def,IS_TRUE_def,SEP_CLAUSES])) 801 802val X64_LISP_iSTEP_COMPILE_PART2 = prove( 803 ``(bc1.code p1 = SOME iCOMPILE) /\ 804 iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 805 SPEC X64_MODEL 806 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 9 cs,r::MAP (\n. w + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 807 (code_abbrevs cs) 808 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs2,r,MAP (\n. w + n2w n) r2,bc2) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 809 ONCE_REWRITE_TAC [iSTEP_cases] \\ SIMP_TAC std_ss [] \\ REVERSE (REPEAT STRIP_TAC) 810 \\ FULL_SIMP_TAC (srw_ss()) [BC_STEP_def,CONTAINS_BYTECODE_def,bc_ref_def] 811 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 812 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 813 THEN1 814 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,HD,TL,APPEND] 815 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 816 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 817 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_inv_BC_COMPILE,SEP_CLAUSES] 818 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 819 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 820 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 821 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 822 \\ CONV_TAC ((RAND_CONV) 823 (SIMP_CONV (srw_ss()) [zLISP_def,lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,BC_FAIL_def])) 824 \\ MATCH_MP_TAC icompile_fail \\ ASM_SIMP_TAC std_ss []) 825 \\ FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,HD,TL,APPEND] 826 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 827 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 828 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_inv_BC_COMPILE,SEP_CLAUSES] 829 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 830 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 831 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "NIL"` 832 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `Sym "T"` 833 \\ ASM_SIMP_TAC std_ss [BC_COMPILE_io_out] 834 \\ MATCH_MP_TAC icompile \\ ASM_SIMP_TAC std_ss []); 835 836val icompile_part1 = 837 X64_LISP_CALL_EL9 |> fix_code |> Q.INST [`p`|->`n2w p1 + EL 4 cs`] 838 |> SIMP_RULE std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 839 |> MATCH_MP SPEC_FRAME |> Q.SPEC `~zS` 840 841val X64_LISP_iSTEP_COMPILE_PART1 = prove( 842 ``iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 843 (bc1.code p1 = SOME iCOMPILE) ==> 844 SPEC X64_MODEL 845 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 4 cs + n2w p1,MAP (\n. w + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 846 (code_abbrevs cs) 847 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 9 cs, (EL 4 cs + n2w p2)::MAP (\n. w + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 848 STRIP_TAC \\ MATCH_MP_TAC zLISP_BYTECODE_MOVE_CODE \\ REPEAT STRIP_TAC 849 \\ FULL_SIMP_TAC std_ss [bc_ref_def] 850 \\ REVERSE (FULL_SIMP_TAC std_ss [iSTEP_cases,CONTAINS_BYTECODE_def]) 851 \\ FULL_SIMP_TAC (srw_ss()) [BC_STEP_def,bc_ref_def,LENGTH] 852 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 853 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 854 \\ SIMP_TAC std_ss [zLISP_BYTECODE_def] 855 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 856 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 857 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 858 \\ BYTECODE_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 859 \\ FULL_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 860 \\ FULL_SIMP_TAC std_ss [icompile_part1]); 861 862val X64_LISP_iSTEP_COMPILE = let 863 val th1 = UNDISCH_ALL X64_LISP_iSTEP_COMPILE_PART1 864 val th2 = UNDISCH X64_LISP_iSTEP_COMPILE_PART2 |> Q.INST [`r`|->`EL 4 cs + n2w p2`] 865 val th = DISCH_ALL (SPEC_COMPOSE_RULE [th1,th2]) |> RW [AND_IMP_INTRO] 866 in th end; 867 868val X64_LISP_iSTEP_CONST_SYM_PART1 = prove( 869 ``iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 870 (bc1.code p1 = SOME (iCONST_SYM s)) ==> 871 SPEC X64_MODEL 872 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 4 cs + n2w p1,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 873 (code_abbrevs cs) 874 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) ((if xs1 = [] then Sym "NIL" else HD xs1)::xs1,EL 4 cs + n2w p1 + 23w,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 875 STRIP_TAC \\ MATCH_MP_TAC zLISP_BYTECODE_MOVE_CODE \\ REPEAT STRIP_TAC 876 \\ FULL_SIMP_TAC std_ss [bc_ref_def] 877 \\ REVERSE (FULL_SIMP_TAC std_ss [iSTEP_cases,CONTAINS_BYTECODE_def]) 878 \\ FULL_SIMP_TAC (srw_ss()) [BC_STEP_def,bc_ref_def,LENGTH] 879 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 880 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 881 \\ `0x48w::0x85w::0xDBw::0x3Ew::0x48w::0x75w::0x9w::0x8Bw::0xD1w:: 882 0x48w::0xFFw::0xA7w::0x38w::0xFFw::0xFFw::0xFFw::0x48w::0xFFw:: 883 0xCBw::0x44w::0x89w::0x4w::0x9Fw::0x41w::0xB8w:: 884 IMMEDIATE32 (n2w (8 * THE (LIST_FIND 0 x syms) + 3)) = 885 0x48w::0x85w::0xDBw::0x3Ew::0x48w::0x75w::0x9w::0x8Bw::0xD1w:: 886 0x48w::0xFFw::0xA7w::0x38w::0xFFw::0xFFw::0xFFw::0x48w::0xFFw:: 887 0xCBw::0x44w::0x89w::0x4w::0x9Fw::[] ++ 0x41w::0xB8w:: 888 IMMEDIATE32 (n2w (8 * THE (LIST_FIND 0 x syms) + 3))` by 889 FULL_SIMP_TAC std_ss [APPEND] 890 \\ FULL_SIMP_TAC std_ss [] 891 \\ MATCH_MP_TAC (GEN_ALL (RW [AND_IMP_INTRO] SPEC_X64_MERGE_CODE)) 892 \\ FULL_SIMP_TAC std_ss [LENGTH] 893 \\ MATCH_MP_TAC (SPEC_SUBSET_CODE |> SPEC_ALL |> UNDISCH 894 |> Q.INST [`c`|->`x1 INSERT s`] |> Q.SPEC `x1 INSERT y1 INSERT s` 895 |> SIMP_RULE std_ss [INSERT_SUBSET] 896 |> SIMP_RULE std_ss [SUBSET_DEF,IN_INSERT] |> DISCH_ALL) 897 \\ SIMP_TAC std_ss [zLISP_BYTECODE_def] 898 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 899 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 900 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 901 \\ BYTECODE_TAC 902 \\ Cases_on `xs1` \\ FULL_SIMP_TAC std_ss [HD,TL,APPEND,NOT_CONS_NIL] 903 \\ FULL_SIMP_TAC std_ss [fix_code X64_LISP_PUSH_0]); 904 905fun str_remove_primes v = (implode o filter (fn x => not (x = #"'")) o explode) v 906fun EX_TAC (hs,goal) = let 907 val v = fst (dest_exists goal) 908 val v = mk_var(str_remove_primes (fst (dest_var v)), type_of v) 909 in EXISTS_TAC v (hs,goal) end; 910 911val DIFF_DELETE = prove( 912 ``s DIFF t DELETE x = s DIFF (x INSERT t)``, 913 SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_DELETE,IN_INSERT] \\ METIS_TAC []); 914 915val SPEC_zCODE_SET_LEMMA = prove( 916 ``SPEC X64_MODEL p {(w,xs)} q /\ one_byte_list w xs (fun2set (d,dd DIFF dx)) ==> 917 SPEC X64_MODEL p (zCODE_SET dd d) q``, 918 REPEAT STRIP_TAC \\ IMP_RES_TAC X64_SPEC_EXLPODE_CODE 919 \\ SIMP_TAC std_ss [zCODE_SET_def] 920 \\ MATCH_MP_TAC (SIMP_RULE std_ss [PULL_FORALL_IMP,AND_IMP_INTRO] SPEC_SUBSET_CODE) 921 \\ Q.EXISTS_TAC `{(w + n2w n,[EL n xs]) | n | n < LENGTH xs}` 922 \\ ASM_SIMP_TAC std_ss [] 923 \\ Q.PAT_X_ASSUM `one_byte_list w xs (fun2set (d,dd DIFF dx))` MP_TAC 924 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 925 \\ Q.SPEC_TAC (`w`,`w`) \\ Q.SPEC_TAC (`dx`,`dx`) \\ Q.SPEC_TAC (`xs`,`xs`) 926 \\ Induct \\ FULL_SIMP_TAC std_ss [LENGTH,GSPECIFICATION,SUBSET_DEF] 927 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS_IMP,CONS_11,PULL_FORALL_IMP] 928 \\ SIMP_TAC std_ss [one_byte_list_def,one_fun2set,IN_DIFF] 929 \\ NTAC 4 STRIP_TAC \\ Cases_on `n` 930 \\ ASM_SIMP_TAC std_ss [WORD_ADD_0,EL,HD,TL] \\ STRIP_TAC 931 \\ FULL_SIMP_TAC std_ss [DIFF_DELETE] \\ RES_TAC 932 \\ FULL_SIMP_TAC std_ss [word_arith_lemma1,ADD1,AC ADD_COMM ADD_ASSOC]); 933 934val SPEC_zCODE_SET = prove( 935 ``SPEC X64_MODEL p {(w,xs)} q /\ one_byte_list w xs (fun2set (d,dd DIFF dx)) ==> 936 SPEC X64_MODEL p (zCODE_SET dd d) q``, 937 METIS_TAC [SPEC_zCODE_SET_LEMMA,SPEC_X64_STRENGTHEN_CODE]); 938 939val X64_ASSIGN = let 940 val ((th,_,_),_) = x64_spec "41B8" 941 in RW [SIGN_EXTEND_MOD,GSYM w2w_def] th |> Q.INST [`imm32` |-> `w0n`] end; 942 943val MEM_IMP_LIST_FIND = prove( 944 ``!xs n x. MEM x xs ==> ?k. (LIST_FIND n x xs = SOME k) /\ k - n < LENGTH xs``, 945 Induct \\ SIMP_TAC std_ss [MEM,LIST_FIND_def] \\ NTAC 3 STRIP_TAC 946 \\ Cases_on `x = h` \\ FULL_SIMP_TAC std_ss [LENGTH] 947 \\ REPEAT STRIP_TAC \\ RES_TAC 948 \\ POP_ASSUM (MP_TAC o Q.SPEC `n+1`) \\ REPEAT STRIP_TAC 949 \\ FULL_SIMP_TAC std_ss [] 950 \\ DECIDE_TAC); 951 952val X64_LISP_iSTEP_CONST_SYM_PART2 = prove( 953 ``iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 954 (bc1.code p1 = SOME (iCONST_SYM s)) ==> 955 SPEC X64_MODEL 956 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (y::xs1,EL 4 cs + n2w p1 + 23w,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 957 (code_abbrevs cs) 958 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (Sym s::xs1,EL 4 cs + n2w p2,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 959 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [zLISP_BYTECODE_def] 960 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 961 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 962 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_REMOVE_POST 963 \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 964 \\ Q.SPEC_TAC (`xs1 ++ Sym "NIL"::stack`,`stack1`) \\ REPEAT STRIP_TAC 965 \\ BYTECODE_TAC 966 \\ REVERSE (FULL_SIMP_TAC (srw_ss()) [iSTEP_cases,CONTAINS_BYTECODE_def]) 967 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 968 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 969 \\ FULL_SIMP_TAC std_ss [BC_STEP_def,bc_length_def,bc_ref_def,LENGTH_APPEND, 970 LENGTH,APPEND,IMMEDIATE32_def] \\ FULL_SIMP_TAC std_ss [GSYM word_add_n2w] 971 \\ Q.SPEC_TAC (`MAP (\n. n2w n + EL 4 cs) r1`,`rs2`) \\ STRIP_TAC 972 \\ Q.SPEC_TAC (`IO_STREAMS input bc1.io_out`,`io2`) \\ STRIP_TAC 973 \\ Q.SPEC_TAC (`bc_state_tree bc1`,`x5`) \\ STRIP_TAC 974 \\ ASM_SIMP_TAC std_ss [AC WORD_ADD_ASSOC WORD_ADD_COMM] 975 \\ ASM_SIMP_TAC std_ss [WORD_ADD_ASSOC] 976 \\ Q.ABBREV_TAC `p = n2w p1 + EL 4 cs` 977 \\ SIMP_TAC (std_ss++sep_cond_ss) [zLISP_def,SEP_CLAUSES,GSYM SPEC_PRE_EXISTS, 978 SPEC_MOVE_COND,zCODE_MEMORY_def] \\ REPEAT STRIP_TAC 979 \\ MATCH_MP_TAC (SPEC_SUBSET_CODE |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL 980 |> DISCH_ALL |> RW [AND_IMP_INTRO] |> GEN_ALL) 981 \\ Q.EXISTS_TAC `{}` \\ FULL_SIMP_TAC std_ss [EMPTY_SUBSET] 982 \\ POP_ASSUM (STRIP_ASSUME_TAC o RW [lisp_inv_def]) 983 \\ `?k. (LIST_FIND 0 s (INIT_SYMBOLS ++ sym) = SOME k) /\ k < 536870912 /\ 984 ?dx. (one_byte_list (p + 0x17w) 985 ([0x41w; 0xB8w] ++ IMMEDIATE32 (n2w (8 * THE (LIST_FIND 0 s ((INIT_SYMBOLS ++ sym))) + 3)))) 986 (fun2set (d,dd DIFF dx))` by 987 (IMP_RES_TAC code_heap_IMP \\ POP_ASSUM (K ALL_TAC) 988 \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def] 989 \\ `?k. (LIST_FIND 0 s (INIT_SYMBOLS ++ sym) = SOME k) /\ 990 (k - 0 < LENGTH (INIT_SYMBOLS ++ sym))` by METIS_TAC [MEM_IMP_LIST_FIND] 991 \\ FULL_SIMP_TAC std_ss [symtable_inv_def] 992 \\ FULL_SIMP_TAC std_ss [symtable_inv_def,one_symbol_list_def, 993 SEP_CLAUSES,SEP_EXISTS_THM,cond_STAR] 994 \\ STRIP_TAC THEN1 DECIDE_TAC 995 \\ FULL_SIMP_TAC std_ss [bc_ref_def,APPEND] 996 \\ Q.PAT_X_ASSUM `ddd (fun2set (d,dd))` MP_TAC 997 \\ ONCE_REWRITE_TAC [STAR_COMM] \\ Q.UNABBREV_TAC `p` 998 \\ NTAC 23 (SIMP_TAC std_ss [Once one_byte_list_def,word_arith_lemma1,GSYM ADD_ASSOC]) 999 \\ SIMP_TAC std_ss [STAR_ASSOC] 1000 \\ `n2w p1 + EL 4 cs + 0x17w = EL 4 cs + n2w p1 + 0x17w` by 1001 SIMP_TAC std_ss [AC WORD_ADD_COMM WORD_ADD_ASSOC] 1002 \\ ASM_SIMP_TAC std_ss [word_arith_lemma1] 1003 \\ METIS_TAC [fun2set_STAR_IMP]) 1004 \\ Q.ABBREV_TAC `w0n = n2w (8 * THE (LIST_FIND 0 s (INIT_SYMBOLS ++ sym)) + 3):word32` 1005 \\ NTAC 6 (HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ EX_TAC) 1006 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `w0n` 1007 \\ REPEAT (HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ EX_TAC) 1008 \\ Q.PAT_ABBREV_TAC `ii = lisp_inv zzz zzzz zzzzzz` 1009 \\ `ii` by 1010 (Q.UNABBREV_TAC `ii` \\ FULL_SIMP_TAC std_ss [lisp_inv_def] 1011 \\ Q.EXISTS_TAC `H_DATA (INR (n2w (THE (LIST_FIND 0 s (INIT_SYMBOLS ++ sym)))))` 1012 \\ REPEAT EX_TAC \\ FULL_SIMP_TAC std_ss [] 1013 \\ FULL_SIMP_TAC std_ss [APPEND,EVERY_DEF,stop_and_copyTheory.lisp_x_def] 1014 \\ Q.UNABBREV_TAC `w0n` 1015 \\ FULL_SIMP_TAC std_ss [MAP,CONS_11,ref_heap_addr_alt] 1016 \\ STRIP_TAC THEN1 (Cases_on `s0` 1017 \\ FULL_SIMP_TAC std_ss [ok_split_heap_def,UNION_SUBSET,ADDR_SET_THM,INSERT_SUBSET]) 1018 \\ FULL_SIMP_TAC std_ss [w2w_def,GSYM word_add_n2w,WORD_EQ_ADD_CANCEL] 1019 \\ FULL_SIMP_TAC (std_ss++SIZES_ss) [WORD_MUL_LSL,word_mul_n2w,w2n_n2w]) 1020 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] \\ Q.UNABBREV_TAC `ii` 1021 \\ CONV_TAC (PRE_CONV (MOVE_OUT_CONV ``zCODE``)) 1022 \\ CONV_TAC (POST_CONV (MOVE_OUT_CONV ``zCODE``)) 1023 \\ FULL_SIMP_TAC std_ss [RW1 [STAR_COMM] X64_SPEC_CODE] 1024 \\ MATCH_MP_TAC (GEN_ALL SPEC_zCODE_SET) 1025 \\ Q.LIST_EXISTS_TAC [`[0x41w; 0xB8w] ++ IMMEDIATE32 w0n`,`p + 0x17w`,`dx`] 1026 \\ FULL_SIMP_TAC std_ss [APPEND,IMMEDIATE32_def] 1027 \\ (fn (hs,goal) => let 1028 val (_,p,_,_) = dest_spec goal 1029 val lemma = GEN_ALL (Q.SPECL [`p`,`{}`] (Q.ISPEC `X64_MODEL` SPEC_REFL)) 1030 in ASSUME_TAC (SPEC p lemma) (hs,goal) end) 1031 \\ POP_ASSUM (fn th => ASSUME_TAC (SPEC_COMPOSE_RULE [th,X64_ASSIGN])) 1032 \\ FULL_SIMP_TAC (std_ss++star_ss) []); 1033 1034val X64_LISP_iSTEP_CONST_SYM = let 1035 val th1 = UNDISCH_ALL X64_LISP_iSTEP_CONST_SYM_PART1 1036 val th2 = UNDISCH_ALL X64_LISP_iSTEP_CONST_SYM_PART2 1037 |> Q.INST [`y`|->`(if xs1 = [] then Sym "NIL" else HD xs1)`] 1038 val th = DISCH_ALL (SPEC_COMPOSE_RULE [th1,th2]) |> RW [AND_IMP_INTRO] 1039 in th end; 1040 1041val code_ptr_WRITE_CODE = prove( 1042 ``!bs bc. code_ptr (WRITE_CODE bc bs) = code_ptr bc + code_length bs``, 1043 Induct \\ Cases_on `bc` \\ Cases_on `p` 1044 \\ ASM_SIMP_TAC std_ss [WRITE_CODE_def,code_length_def,code_ptr_def] 1045 \\ DECIDE_TAC); 1046 1047val code_heap_IMP = prove( 1048 ``!code. code_heap code (sym,base_ptr,curr_ptr,space_left,dh,h) /\ 1049 ~(code_mem code p = NONE) ==> p < 2**30``, 1050 SIMP_TAC std_ss [code_heap_def,PULL_EXISTS_IMP,GSYM AND_IMP_INTRO] 1051 \\ REPEAT STRIP_TAC 1052 \\ Cases_on `code_mem (WRITE_CODE (BC_CODE ((\x. NONE),0)) bs) p` 1053 \\ FULL_SIMP_TAC std_ss [] 1054 \\ IMP_RES_TAC code_length_LESS 1055 \\ FULL_SIMP_TAC std_ss [code_ptr_WRITE_CODE,code_ptr_def] \\ DECIDE_TAC); 1056 1057val LISP = lisp_inv_def |> SPEC_ALL |> concl |> dest_eq |> fst 1058val lisp_inv_IMP = prove( 1059 ``^LISP ==> !p. ~(code_mem code p = NONE) ==> p < 2**30``, 1060 SIMP_TAC bool_ss [lisp_inv_def] \\ REPEAT STRIP_TAC \\ METIS_TAC [code_heap_IMP]); 1061 1062val zLISP = zLISP_def |> SPEC_ALL |> concl |> dest_eq |> fst 1063val zLISP_IMP = prove( 1064 ``^zLISP s ==> !p. ~(code_mem code p = NONE) ==> p < 2**30``, 1065 SIMP_TAC bool_ss [zLISP_def,cond_STAR,SEP_EXISTS_THM] \\ METIS_TAC [lisp_inv_IMP]); 1066 1067val zLISP_BOUND = prove( 1068 ``~(code_mem code p = NONE) ==> (^zLISP = ^zLISP * cond (p < 2**30))``, 1069 SIMP_TAC std_ss [cond_STAR,FUN_EQ_THM] \\ METIS_TAC [SIMP_RULE std_ss[]zLISP_IMP]); 1070 1071val zLISP_BYTECODE_PC_BOUND = prove( 1072 ``(~(bc1.code p = NONE) /\ p < 2**30 ==> 1073 SPEC X64_MODEL 1074 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,wp1,r1,bc1) (stack1,input1,xbp1,rstack1,amnt1,w)) c 1075 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs2,wp2,r2,bc2) (stack2,input2,xbp2,rstack2,amnt2,w))) ==> 1076 ~(bc1.code p = NONE) ==> 1077 SPEC X64_MODEL 1078 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs1,wp1,r1,bc1) (stack1,input1,xbp1,rstack1,amnt1,w)) c 1079 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (xs2,wp2,r2,bc2) (stack2,input2,xbp2,rstack2,amnt2,w))``, 1080 SIMP_TAC std_ss [zLISP_BYTECODE_def,GSYM SPEC_PRE_EXISTS] 1081 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1082 \\ FULL_SIMP_TAC std_ss [SPEC_PRE_DISJ] 1083 \\ FULL_SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ REPEAT STRIP_TAC 1084 \\ `~(code_mem (BC_CODE (bc1.code,bc1.code_end)) p = NONE)` by 1085 ASM_SIMP_TAC std_ss [code_mem_def] 1086 \\ IMP_RES_TAC zLISP_BOUND \\ POP_ASSUM (fn th => SIMP_TAC std_ss [Once th]) 1087 \\ FULL_SIMP_TAC (std_ss++sep_cond_ss) [SPEC_MOVE_COND]); 1088 1089val X64_LISP_iSTEP = store_thm("X64_LISP_iSTEP", 1090 ``!xs1 p1 r1 bc1 xs2 p2 r2 bc2. 1091 iSTEP (xs1,p1,r1,bc1) (xs2,p2,r2,bc2) ==> 1092 SPEC X64_MODEL 1093 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 4 cs + n2w p1,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1094 (code_abbrevs cs) 1095 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs2,EL 4 cs + n2w p2,MAP (\n. EL 4 cs + n2w n) r2,bc2) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1096 NTAC 8 STRIP_TAC \\ Cases_on `bc1.code p1 = SOME iCOMPILE` 1097 THEN1 (STRIP_TAC \\ MATCH_MP_TAC X64_LISP_iSTEP_COMPILE \\ ASM_SIMP_TAC std_ss []) 1098 \\ Cases_on `?s. bc1.code p1 = SOME (iCONST_SYM s)` THEN1 1099 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1100 \\ REVERSE (FULL_SIMP_TAC (srw_ss()) [iSTEP_cases,CONTAINS_BYTECODE_def]) 1101 \\ REVERSE (FULL_SIMP_TAC (srw_ss()) [iSTEP_cases,CONTAINS_BYTECODE_def]) 1102 THEN1 (FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 1103 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 1104 \\ MP_TAC X64_LISP_iSTEP_CONST_SYM 1105 \\ FULL_SIMP_TAC (srw_ss()) [iSTEP_cases,CONTAINS_BYTECODE_def]) 1106 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1107 \\ REVERSE (Cases_on `?xx. bc1.code p1 = SOME xx`) THEN1 1108 (FULL_SIMP_TAC (srw_ss()) [iSTEP_cases,CONTAINS_BYTECODE_def] 1109 \\ FULL_SIMP_TAC std_ss [zLISP_BYTECODE_def,zLISP_def, 1110 lisp_inv_def,IS_TRUE_def,SEP_CLAUSES,SPEC_REFL,SPEC_FALSE_PRE]) 1111 \\ FULL_SIMP_TAC std_ss [] 1112 \\ POP_ASSUM MP_TAC \\ MATCH_MP_TAC zLISP_BYTECODE_MOVE_CODE \\ REPEAT STRIP_TAC 1113 \\ `~(bc1.code p1 = NONE)` by (FULL_SIMP_TAC std_ss []) 1114 \\ POP_ASSUM MP_TAC \\ MATCH_MP_TAC zLISP_BYTECODE_PC_BOUND 1115 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 1116 \\ `bc_ref (p1,syms) xx = bc_ref (p1,syms) (THE (bc1.code p1))` by 1117 FULL_SIMP_TAC std_ss [] 1118 \\ ONCE_ASM_REWRITE_TAC [] 1119 \\ MATCH_MP_TAC X64_LISP_iSTEP_MOST_CASES \\ ASM_SIMP_TAC std_ss []); 1120 1121val X64_LISP_RTC_iSTEP = prove( 1122 ``!x y. RTC iSTEP x y ==> 1123 !xs1 p1 r1 bc1 xs2 p2 r2 bc2. 1124 (x = (xs1,p1,r1,bc1)) /\ (y = (xs2,p2,r2,bc2)) ==> 1125 SPEC X64_MODEL 1126 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs1,EL 4 cs + n2w p1,MAP (\n. EL 4 cs + n2w n) r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1127 (code_abbrevs cs) 1128 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) (xs2,EL 4 cs + n2w p2,MAP (\n. EL 4 cs + n2w n) r2,bc2) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1129 HO_MATCH_MP_TAC RTC_INDUCT 1130 \\ SIMP_TAC std_ss [SPEC_REFL,PULL_FORALL_IMP,GSYM AND_IMP_INTRO,FORALL_PROD] 1131 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC X64_LISP_iSTEP 1132 \\ POP_ASSUM (IMP_RES_TAC o MATCH_MP (RW [GSYM AND_IMP_INTRO] SPEC_COMPOSE) o SPEC_ALL) 1133 \\ FULL_SIMP_TAC std_ss [UNION_IDEMPOT]) 1134 |> SIMP_RULE std_ss [PULL_FORALL_IMP]; 1135 1136 1137(* composition of compile, jump-to-code and execution of code *) 1138 1139val SPEC_PRE_POST_COND = prove( 1140 ``SPEC m (p * cond b) c q = SPEC m (p * cond b) c (q * cond b)``, 1141 SIMP_TAC std_ss [SPEC_MOVE_COND,SEP_CLAUSES]); 1142 1143val BYTECODE = zLISP_BYTECODE_def |> SPEC_ALL |> concl |> dest_eq |> fst 1144 1145val SPEC_INTRO_FAIL = prove( 1146 ``SPEC m (pp) c (^BYTECODE) ==> 1147 SPEC m (pp \/ zLISP_FAIL (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu)) c (^BYTECODE)``, 1148 FULL_SIMP_TAC std_ss [SPEC_PRE_DISJ,zLISP_BYTECODE_def] 1149 \\ ONCE_REWRITE_TAC [SEP_DISJ_COMM] \\ REPEAT STRIP_TAC 1150 \\ MATCH_MP_TAC SPEC_REMOVE_POST \\ SIMP_TAC std_ss [SPEC_REFL]); 1151 1152val X64_BYTECODE_POP_LEMMA = prove( 1153 ``SPEC X64_MODEL 1154 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) 1155 ([result],p,[],bc) 1156 (Sym "NIL"::xs,input,xbp,qs,amnt,EL 4 cs)) 1157 {(p,[0x48w; 0xFFw; 0xC3w])} 1158 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) 1159 ([result],p + 0x3w,[],bc) 1160 (xs,input,xbp,qs,amnt,EL 4 cs))``, 1161 SIMP_TAC std_ss [zLISP_BYTECODE_def,APPEND,HD,TL] 1162 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 1163 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS] \\ REPEAT STRIP_TAC 1164 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x1` 1165 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2` 1166 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x3` 1167 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 1168 \\ Cases_on `bc_inv bc` \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES,SPEC_REFL] 1169 \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO \\ MATCH_MP_TAC SPEC_REMOVE_POST 1170 \\ MATCH_MP_TAC (DISCH T (SIMP_RULE (srw_ss()) [SEP_CLAUSES] 1171 (Q.INST [`xs`|->`Sym "NIL"::Sym "NIL"::xs`, 1172 `ddd`|->`SOME T`] X64_LISP_POP))) \\ ASM_SIMP_TAC std_ss []); 1173 1174val zBYTECODE_EVAL_THM = let 1175 val th = SPEC_COMPOSE_RULE [X64_LISP_COMPILE_FOR_EVAL, 1176 Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`] X64_LISP_JUMP_TO_CODE_FOR_EVAL] 1177 |> SIMP_RULE std_ss [getVal_def,isVal_def,SEP_CLAUSES] 1178 |> RW1 [SPEC_PRE_POST_COND] 1179 |> Q.INST [`io`|->`IO_STREAMS input bc.io_out`,`ok`|->`bc.ok`] 1180 val (th,goal) = SPEC_WEAKEN_RULE th `` 1181 zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) 1182 ([],EL 4 cs + n2w bc.code_end, 1183 MAP (\n. EL 4 cs + n2w n) [0],BC_ONLY_COMPILE ([],sexp2term body,bc)) 1184 (xs,input,xbp,p + 0x6Cw::qs,amnt,EL 4 cs)`` 1185 val lemma = prove(goal, 1186 SIMP_TAC std_ss [zLISP_BYTECODE_def,SEP_IMP_MOVE_COND,HD,APPEND,TL,MAP, 1187 WORD_ADD_0,BC_ONLY_COMPILE_io_out,SEP_CLAUSES, 1188 SIMP_RULE std_ss [LET_DEF] mc_compile_for_eval_thm] 1189 \\ SIMP_TAC std_ss [SEP_IMP_def,SEP_EXISTS_THM] 1190 \\ REPEAT STRIP_TAC \\ METIS_TAC []) 1191 val th = MP th lemma 1192 val th2 = X64_LISP_RTC_iSTEP 1193 |> Q.SPECL [`[]`,`bc.code_end`,`[0]`,`BC_ONLY_COMPILE ([],sexp2term body,bc)`, 1194 `[result]`,`0`,`[]`,`bc8`] 1195 |> UNDISCH |> Q.INST [`stack`|->`xs`,`rstack`|->`p + 0x6Cw::qs`] 1196 val th = SPEC_COMPOSE_RULE [th,th2] 1197 val th = RW [MAP,WORD_ADD_0] th 1198 val th2 = UNDISCH X64_LISP_iSTEP_LAST_RETURN 1199 |> Q.INST [`xs1`|->`[result]`,`stack`|->`xs`,`r`|->`p+0x6Cw`, 1200 `rstack`|->`qs`,`bc1`|->`bc8`] 1201 val th = SPEC_COMPOSE_RULE [th,th2] 1202 val th = RW [UNION_IDEMPOT,GSYM UNION_ASSOC] th 1203 val th = RW [UNION_IDEMPOT,UNION_ASSOC] th 1204 val th = th |> Q.GEN `x4` |> Q.GEN `x3` |> Q.GEN `x2` |> Q.GEN `x1` 1205 val th = SIMP_RULE std_ss [SPEC_PRE_EXISTS] th 1206 val th = MATCH_MP SPEC_INTRO_FAIL th 1207 val th = Q.INST [`xs`|->`Sym "NIL"::xs`] th 1208 val (th,goal) = SPEC_STRENGTHEN_RULE th `` 1209 zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,NONE) 1210 ([body],p,[],bc) 1211 (xs,input,xbp,qs,amnt,EL 4 cs)`` 1212 val lemma = prove(goal, 1213 SIMP_TAC (std_ss++star_ss) [zLISP_BYTECODE_def,APPEND,TL,HD,SEP_IMP_REFL]) 1214 val th = MP th lemma 1215 val th2 = Q.INST [`p`|->`p+0x6Cw`,`bc`|->`bc8`] X64_BYTECODE_POP_LEMMA 1216 val th = SPEC_COMPOSE_RULE [th,th2] 1217 in th end; 1218 1219 1220(* derive similar theorems for read, print, print newline etc. *) 1221 1222(* print *) 1223 1224val iprint = 1225 SPEC_COMPOSE_RULE [X64_LISP_PRINT_SEXP,X64_LISP_PRINT_NEWLINE] 1226 |> SIMP_RULE std_ss [IO_WRITE_APPEND] 1227 |> Q.INST [`io`|->`IO_STREAMS input bc1.io_out`] 1228 |> SIMP_RULE std_ss [IO_WRITE_def,APPEND_ASSOC] 1229 |> DISCH T 1230 1231val code = iprint |> concl |> rand |> rator |> rand 1232val pc = iprint |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1233 1234val X64_LISP_BYTECODE_PRINT = prove( 1235 ``SPEC X64_MODEL 1236 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],p,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1237 ^code 1238 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc,r1,BC_PRINT bc1 (sexp2string x0 ++ "\n")) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1239 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1240 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1241 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1242 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1243 \\ BYTECODE_TAC \\ ASM_SIMP_TAC std_ss [BC_PRINT_LEMMA,SEP_CLAUSES] 1244 \\ SIMP_TAC (srw_ss()) [BC_PRINT_def] 1245 \\ MATCH_MP_TAC iprint \\ SIMP_TAC std_ss []); 1246 1247(* parse *) 1248 1249val iparse = 1250 X64_LISP_PARSE_SEXP 1251 |> Q.INST [`io`|->`IO_STREAMS input bc1.io_out`,`xs`|->`Sym "NIL"::stack`,`xbp`|->`SUC (LENGTH (stack:SExp list))`] 1252 |> RW [LENGTH] |> DISCH T 1253 1254val code = iparse |> concl |> rand |> rator |> rand 1255val pc = iparse |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1256 1257val next_sexp_INTRO = prove( 1258 ``IO_STREAMS (getINPUT (next_sexp (IO_STREAMS input bc1.io_out))) bc1.io_out = 1259 next_sexp (IO_STREAMS input bc1.io_out)``, 1260 SIMP_TAC std_ss [next_sexp_def,IO_INPUT_APPLY_def,getINPUT_def, 1261 REPLACE_INPUT_IO_def]); 1262 1263val X64_LISP_BYTECODE_PARSE = prove( 1264 ``SPEC X64_MODEL 1265 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],p,r1,bc1) (stack,input,SUC (LENGTH stack),rstack,amnt,EL 4 cs)) 1266 ^code 1267 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([read_sexp (IO_STREAMS input bc1.io_out)],^pc,r1,bc1) (stack,getINPUT (next_sexp (IO_STREAMS input bc1.io_out)),SUC (LENGTH stack),rstack,amnt,EL 4 cs))``, 1268 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1269 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1270 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1271 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1272 \\ BYTECODE_TAC \\ ASM_SIMP_TAC std_ss [next_sexp_INTRO,SEP_CLAUSES] 1273 \\ MATCH_MP_TAC iparse \\ ASM_SIMP_TAC std_ss []); 1274 1275(* eof *) 1276 1277val ieof = 1278 X64_LISP_TEST_EOF 1279 |> Q.INST [`io`|->`IO_STREAMS input bc1.io_out`] 1280 |> SIMP_RULE std_ss [LENGTH,getINPUT_def,IO_INPUT_APPLY_def,REPLACE_INPUT_IO_def,combinTheory.o_DEF] 1281 |> DISCH T 1282 1283val code = ieof |> concl |> rand |> rator |> rand 1284val pc = ieof |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1285 1286val X64_LISP_BYTECODE_EOF = prove( 1287 ``SPEC X64_MODEL 1288 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],p,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1289 ^code 1290 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([LISP_TEST (FST (is_eof input))],^pc,r1,bc1) (stack,SND (is_eof input),xbp,rstack,amnt,EL 4 cs))``, 1291 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1292 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1293 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1294 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1295 \\ BYTECODE_TAC \\ ASM_SIMP_TAC std_ss [next_sexp_INTRO,SEP_CLAUSES] 1296 \\ MATCH_MP_TAC SPEC_REMOVE_POST 1297 \\ MATCH_MP_TAC ieof \\ ASM_SIMP_TAC std_ss []); 1298 1299 1300(* jump *) 1301 1302val pre = ijump_raw |> concl |> dest_imp |> fst 1303val code = ijump_raw |> concl |> rand |> rator |> rand 1304val pc1 = ijump_raw |> concl |> rand |> rator |> find_term (can (match_term ``zPC p``)) |> rand 1305val pc2 = ijump_raw |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1306 1307val X64_LISP_BYTECODE_JUMP = prove( 1308 ``^pre ==> SPEC X64_MODEL 1309 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc1,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1310 ^code 1311 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc2,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1312 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1313 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1314 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1315 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1316 \\ BYTECODE_TAC \\ ASM_SIMP_TAC std_ss [next_sexp_INTRO,SEP_CLAUSES] 1317 \\ MATCH_MP_TAC SPEC_REMOVE_POST 1318 \\ MATCH_MP_TAC ijump_raw \\ ASM_SIMP_TAC std_ss []); 1319 1320 1321(* jnil *) 1322 1323val (ijnil1_raw,ijnil2_raw) = let 1324 fun the (SOME x) = x | the _ = fail() 1325 val ((th1,_,_),x) = x64_spec "480F85" 1326 val (th2,_,_) = the x 1327 val th1 = SPEC_COMPOSE_RULE [X64_LISP_MOVE10,X64_LISP_TEST_SYM_0_1,th1] 1328 val th1 = RW [precond_def] th1 |> Q.INST [`xs`|->`x::xs`] 1329 |> HIDE_STATUS_RULE true sts |> lisp_pc_s 1330 |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES,ADD_ASSOC] 1331 |> Q.INST [`imm32`|->`n2w p2 - n2w p1 - 14w`,`p`|->`w + n2w p1`] 1332 |> DISCH ``p1 < 1073741824 /\ p2 < 1073741824`` 1333 |> SIMP_RULE (std_ss++sep_cond_ss) [JNIL_ADDRESS_LEMMA2,SPEC_MOVE_COND] 1334 |> RW [AND_IMP_INTRO] 1335 |> Q.INST [`p1`|->`0`,`w`|->`p`,`p2`|->`p3`] 1336 |> SIMP_RULE (std_ss++sep_cond_ss) [WORD_ADD_0] 1337 val th2 = SPEC_COMPOSE_RULE [X64_LISP_MOVE10,X64_LISP_TEST_SYM_0_1,th2] 1338 val th2 = RW [precond_def] th2 |> Q.INST [`xs`|->`x::xs`] 1339 |> HIDE_STATUS_RULE true sts |> lisp_pc_s 1340 |> SIMP_RULE std_ss [HD,TL,NOT_CONS_NIL,SEP_CLAUSES,ADD_ASSOC] 1341 |> Q.INST [`imm32`|->`n2w p2 - n2w p1 - 14w`,`p`|->`w + n2w p1`] 1342 |> SIMP_RULE (std_ss++sep_cond_ss) [JNIL_ADDRESS_LEMMA2,SPEC_MOVE_COND] 1343 |> Q.INST [`p1`|->`0`,`w`|->`p`,`p2`|->`p3`] 1344 |> SIMP_RULE (std_ss++sep_cond_ss) [WORD_ADD_0] 1345 in (th1,th2) end; 1346 1347val pre = ijnil1_raw |> concl |> dest_imp |> fst 1348val code = ijnil1_raw |> concl |> rand |> rator |> rand 1349val pc1 = ijnil1_raw |> concl |> rand |> rator |> find_term (can (match_term ``zPC p``)) |> rand 1350val pc2 = ijnil1_raw |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1351 1352val X64_LISP_BYTECODE_JNIL1 = prove( 1353 ``^pre ==> SPEC X64_MODEL 1354 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc1,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1355 ^code 1356 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc2,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1357 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1358 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1359 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1360 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1361 \\ `bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 1362 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 1363 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x0` 1364 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2` 1365 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x3` 1366 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 1367 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 1368 \\ MATCH_MP_TAC SPEC_REMOVE_POST 1369 \\ MATCH_MP_TAC ijnil1_raw \\ ASM_SIMP_TAC std_ss []); 1370 1371val pre = ijnil2_raw |> concl |> dest_imp |> fst 1372val code = ijnil2_raw |> concl |> rand |> rator |> rand 1373val pc1 = ijnil2_raw |> concl |> rand |> rator |> find_term (can (match_term ``zPC p``)) |> rand 1374val pc2 = ijnil2_raw |> concl |> rand |> rand |> find_term (can (match_term ``zPC p``)) |> rand 1375 1376val X64_LISP_BYTECODE_JNIL2 = prove( 1377 ``^pre ==> SPEC X64_MODEL 1378 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc1,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs)) 1379 ^code 1380 (zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x0],^pc2,r1,bc1) (stack,input,xbp,rstack,amnt,EL 4 cs))``, 1381 SIMP_TAC std_ss [zLISP_BYTECODE_def] 1382 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC SPEC_PRE_DISJ_INTRO 1383 \\ SIMP_TAC std_ss [GSYM SPEC_PRE_EXISTS,HD,TL,APPEND,SPEC_MOVE_COND] 1384 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [bc_symbols_ok_def,SEP_CLAUSES] 1385 \\ `bc1.instr_length = bc_length` by FULL_SIMP_TAC std_ss [bc_inv_def] 1386 \\ FULL_SIMP_TAC std_ss [bc_length_def,bc_ref_def,LENGTH,GSYM word_add_n2w,WORD_ADD_ASSOC,IMMEDIATE32_def,APPEND] 1387 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x0` 1388 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x2` 1389 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x3` 1390 \\ HO_MATCH_MP_TAC SPEC_PULL_EXISTS \\ Q.EXISTS_TAC `x4` 1391 \\ ASM_SIMP_TAC std_ss [SEP_CLAUSES] 1392 \\ MATCH_MP_TAC SPEC_REMOVE_POST 1393 \\ MATCH_MP_TAC ijnil2_raw \\ ASM_SIMP_TAC std_ss []); 1394 1395 1396(* compose together *) 1397 1398val zLISP_BYTECODE_SHORT_def = Define ` 1399 zLISP_BYTECODE_SHORT 1400 (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu,x,p,rs,bc,stack,input,xbp,rstack,amnt,w) = 1401 zLISP_BYTECODE (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) ([x],p,rs,bc) 1402 (stack,input,xbp,rstack,amnt,w)`; 1403 1404val f1 = PURE_REWRITE_RULE [AND_IMP_INTRO] o 1405 (fn th => if is_imp (concl th) then th else DISCH T th) o 1406 DISCH_ALL o RW [GSYM zLISP_BYTECODE_SHORT_def] o 1407 Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`,`r1`|->`[]`,`xbp`|->`SUC (LENGTH (stack:SExp list))`] 1408 1409 1410val case1 = SPEC_COMPOSE_RULE [ 1411 UNDISCH (f1 X64_LISP_BYTECODE_EOF), 1412 UNDISCH (f1 X64_LISP_BYTECODE_JNIL1)] 1413 1414val case2 = SPEC_COMPOSE_RULE [ 1415 UNDISCH (f1 X64_LISP_BYTECODE_EOF), 1416 UNDISCH (f1 X64_LISP_BYTECODE_JNIL2), 1417 UNDISCH (f1 X64_LISP_BYTECODE_PARSE), 1418 UNDISCH_ALL (SIMP_RULE std_ss [] (DISCH ``term2sexp body = xxx`` (f1 zBYTECODE_EVAL_THM))), 1419 UNDISCH (f1 X64_LISP_BYTECODE_PRINT), 1420 UNDISCH (RW [WORD_ADD_0] (Q.INST [`p2`|->`0`] (f1 X64_LISP_BYTECODE_JUMP)))] 1421 1422fun guess_length_of_code def = let 1423 val tm = def |> SPEC_ALL |> concl |> cdr 1424 fun dest_code_piece tm = let 1425 val (x,y) = pairSyntax.dest_pair tm 1426 (* val (y,z) = pairSyntax.dest_pair y *) 1427 val (v,n) = wordsSyntax.dest_word_add x 1428 val _ = dest_var v 1429 val n = (numSyntax.int_of_term o cdr) n 1430 in n + (y |> listSyntax.dest_list |> fst |> length) end 1431 val xs = map dest_code_piece (find_terms (can dest_code_piece) tm) 1432 val max = foldl (fn (x,y) => if x < y then y else x) 0 xs 1433 in max end; 1434 1435val (READ_EVAL_PRINT_LOOP_BASE,READ_EVAL_PRINT_LOOP_STEP) = let 1436 val n = guess_length_of_code (DISCH T case2) 1437 val k = concl case1 1438 |> find_term (can (match_term ``n2w (n + p2)``)) 1439 |> find_term (numSyntax.is_numeral) |> numSyntax.int_of_term 1440 val p3 = numSyntax.term_of_int (n - k) 1441 val th1 = INST [``p3:num``|->p3] case1 1442 |> SIMP_RULE (std_ss++SIZES_ss) [w2w_def,w2n_n2w,w2n_lsr] 1443 val th2 = INST [``p3:num``|->p3] case2 1444 |> SIMP_RULE (std_ss++SIZES_ss) [w2w_def,w2n_n2w,w2n_lsr,word_2comp_n2w] 1445 |> RW1 [GSYM n2w_mod] 1446 |> SIMP_RULE (std_ss++SIZES_ss) [w2w_def,w2n_n2w,w2n_lsr,word_2comp_n2w] 1447 val (_,_,c,_) = dest_spec (concl th2) 1448 val th1 = SPEC c (MATCH_MP SPEC_SUBSET_CODE th1) 1449 val goal = fst (dest_imp (concl th1)) 1450 val lemma = prove(goal, 1451 REWRITE_TAC [INSERT_SUBSET,UNION_SUBSET,IN_INSERT,IN_UNION,EMPTY_SUBSET]) 1452 val th1 = MP th1 lemma 1453 in (th1,th2) end 1454 1455val _ = save_thm("READ_EVAL_PRINT_LOOP_BASE",READ_EVAL_PRINT_LOOP_BASE); 1456val _ = save_thm("READ_EVAL_PRINT_LOOP_STEP",READ_EVAL_PRINT_LOOP_STEP); 1457 1458val _ = export_theory(); 1459