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