1 2open HolKernel Parse boolLib bossLib; 3open arithmeticTheory listTheory pairTheory finite_mapTheory stringTheory; 4open source_valuesTheory source_syntaxTheory x64asm_syntaxTheory mp_then 5 BasicProvers source_semanticsTheory source_propertiesTheory alignmentTheory 6 combinTheory optionTheory alistTheory wordsTheory wordsLib 7 x64asm_syntaxTheory x64asm_semanticsTheory x64asm_propertiesTheory 8 codegenTheory relationTheory lprefix_lubTheory llistTheory; 9 10val _ = new_theory "codegen_proofs"; 11 12 13(* definitions of invariants and relations *) 14 15Definition code_in_def: 16 code_in n [] code = T ��� 17 code_in n (x::xs) code = 18 (lookup n code = SOME x ��� code_in (n+1) xs code) 19End 20 21Definition init_code_in_def: 22 init_code_in instructions ��� 23 ���start. code_in 0 (init start) instructions 24End 25 26Definition code_rel_def: 27 code_rel fs ds instructions ��� 28 init_code_in instructions ��� 29 ���n params body. 30 lookup_fun n ds = SOME (params,body) ��� 31 ���pos. ALOOKUP fs n = SOME pos ��� 32 code_in pos (flatten (FST 33 (c_defun pos fs (Defun n params body))) []) instructions 34End 35 36Definition state_rel_def: 37 state_rel fs (s:source_semantics$state) (t:x64asm_semantics$state) ��� 38 s.input = t.input ��� 39 s.output = t.output ��� 40 code_rel fs s.funs t.instructions ��� 41 ���r14 r15. 42 t.regs R12 = SOME 16w ��� 43 t.regs R13 = SOME 0x7FFFFFFFFFFFFFFFw ��� 44 t.regs R14 = SOME r14 ��� 45 t.regs R15 = SOME r15 ��� 46 memory_writable r14 r15 t.memory 47End 48 49Definition has_stack_def: 50 has_stack t xs <=> 51 ���w ws. xs = Word w :: ws ��� t.regs RAX = SOME w ��� t.stack = ws 52End 53 54Definition v_inv_def: 55 v_inv t (Num n) w = (n < 2 ** 63 ��� w = n2w n) ��� 56 v_inv t (Pair x1 x2) w = 57 ���w1 w2. 58 read_mem (w+0w) t = SOME w1 ��� v_inv t x1 w1 ��� 59 read_mem (w+8w) t = SOME w2 ��� v_inv t x2 w2 ��� 60 w ��� 0w (* the address must not be the null pointer *) 61End 62 63Definition env_ok_def: 64 env_ok env vs curr t <=> 65 LENGTH vs = LENGTH curr ��� 66 ���n v. env n = SOME v ��� 67 find n vs 0 < LENGTH curr ��� 68 ���w. EL (find n vs 0) curr = (Word w) ��� v_inv t v w 69End 70 71 72(* setting up the proof goal *) 73 74val goal = 75 ``��env e s. 76 ���res s1 t tail' vs fs cs l1 curr rest. 77 eval env e s = (res,s1) ��� res ��� Err Crash ��� 78 c_exp tail' t.pc vs fs e = (cs,l1) ��� 79 state_rel fs s t ��� env_ok env vs curr t ��� 80 has_stack t (curr ++ rest) ��� ODD (LENGTH rest) ��� 81 code_in t.pc (flatten cs []) t.instructions ��� 82 ���outcome. 83 steps (State t,s.clock) outcome ��� 84 case outcome of 85 | (Halt ec output, ck) => output ��� s1.output ��� ec = 1w 86 | (State t1, ck) => 87 state_rel fs s1 t1 ��� ck = s1.clock ��� 88 ���v. res = Res v ==> 89 ���w. v_inv t1 v w ��� 90 if tail' then 91 has_stack t1 (Word w :: rest) ��� fetch t1 = SOME Ret 92 else 93 has_stack t1 (Word w :: curr ++ rest) ��� t1.pc = l1`` 94 95val goals = 96 ``��env es s. 97 ���res s1 t vs fs cs l1 curr rest. 98 evals env es s = (res,s1) ��� res ��� Err Crash ��� 99 c_exps t.pc vs fs es = (cs,l1) ��� 100 state_rel fs s t ��� env_ok env vs curr t ��� 101 has_stack t (curr ++ rest) ��� ODD (LENGTH rest) ��� 102 code_in t.pc (flatten cs []) t.instructions ��� 103 ���outcome. 104 steps (State t,s.clock) outcome ��� 105 case outcome of 106 | (Halt ec output,ck) => output ��� s1.output ��� ec = 1w 107 | (State t1,ck) => 108 state_rel fs s1 t1 ��� ck = s1.clock ��� 109 ���vs. res = Res vs ==> 110 ���ws. LIST_REL (v_inv t1) vs ws ��� 111 has_stack t1 (MAP Word (REVERSE ws) ++ curr ++ rest) ��� 112 t1.pc = l1`` 113 114local 115 val ind_thm = eval_ind |> ISPECL [goal,goals] 116 |> CONV_RULE (DEPTH_CONV BETA_CONV) |> REWRITE_RULE []; 117 val ind_goals = ind_thm |> concl |> dest_imp |> fst |> ASSUME |> CONJUNCTS |> map concl 118in 119 fun get_goal s = first (can (find_term (can (match_term (Term [QUOTE s]))))) ind_goals 120 fun compile_correct_tm () = ind_thm |> concl |> rand 121 fun the_ind_thm () = ind_thm 122 fun strip tm = tm |> ASSUME |> SIMP_RULE std_ss [PULL_FORALL] |> SPEC_ALL |> concl 123end 124 125 126(* various lemmas *) 127 128Theorem even_len_simp[simp]: 129 ���xs. even_len xs = EVEN (LENGTH xs) ��� odd_len xs = ODD (LENGTH xs) 130Proof 131 Induct \\ fs [even_len_def,ODD,EVEN_ODD] 132QED 133 134Theorem steps_v_inv: 135 steps (State t0,n) (State t1,m) ��� v_inv t0 a w ��� v_inv t1 a w 136Proof 137 rw [] \\ pop_assum mp_tac 138 \\ qid_spec_tac ���w��� \\ Induct_on ���a��� \\ fs [v_inv_def] 139 \\ imp_res_tac steps_consts \\ fs [] \\ metis_tac [] 140QED 141 142Theorem flatten_acc: 143 ���p acc. flatten p acc = flatten p [] ++ acc 144Proof 145 once_rewrite_tac [EQ_SYM_EQ] 146 \\ Induct_on ���p��� \\ simp_tac std_ss [flatten_def] \\ fs [] 147 \\ last_assum (once_rewrite_tac o single o GSYM) 148 \\ first_assum (once_rewrite_tac o single o GSYM) 149 \\ fs [] 150QED 151 152Theorem code_in_append[simp]: 153 ���xs ys n code. 154 code_in n (xs ++ ys) code ��� 155 code_in n xs code ��� code_in (n + LENGTH xs) ys code 156Proof 157 Induct \\ fs [code_in_def,ADD1,AC CONJ_COMM CONJ_ASSOC] 158QED 159 160Theorem c_exp_length: 161 (���t l vs fs x c l1. c_exp t l vs fs x = (c,l1) ��� l1 = l + LENGTH (flatten c [])) ��� 162 (���l vs fs xs c l1. c_exps l vs fs xs = (c,l1) ��� l1 = l + LENGTH (flatten c [])) 163Proof 164 ho_match_mp_tac c_exp_ind_alt \\ rw [] \\ fs [c_exp_alt] 165 \\ rpt (pairarg_tac \\ fs []) 166 \\ rw [] \\ fs [flatten_def] 167 \\ rw [] \\ fs [c_if_def,c_test_def] 168 \\ rw [] \\ fs [flatten_def] 169 \\ rw [] \\ fs [c_if_def,c_test_def,c_const_def,AllCaseEqs()] 170 \\ rw [] \\ fs [c_if_def,c_test_def,c_const_def,AllCaseEqs(),c_var_def,make_ret_def] 171 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 172 \\ once_rewrite_tac [flatten_acc] \\ fs [] 173 \\ once_rewrite_tac [flatten_acc] \\ fs [] 174 \\ Cases_on ���c_exps l vs fs xs��� \\ fs [c_call_def] 175 \\ every_case_tac 176 \\ rw [] \\ fs [c_if_def,c_test_def,c_const_def,AllCaseEqs(),c_var_def] 177 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 178 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 179 \\ fs [make_ret_def] 180 \\ rw [] \\ fs [c_if_def,c_test_def,c_const_def,AllCaseEqs(),c_var_def] 181 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 182 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 183 \\ rpt (pop_assum mp_tac) 184 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def] 185 \\ rw [] \\ Cases_on ���test��� \\ fs [c_test_def] 186QED 187 188Theorem find_acc: 189 ���n vs k. find n vs k = find n vs 0 + k 190Proof 191 once_rewrite_tac [EQ_SYM_EQ] 192 \\ Induct_on ���vs��� \\ fs [find_def] \\ rw [] 193 \\ Cases_on ���h��� \\ fs [find_def] 194 \\ last_assum (once_rewrite_tac o single o GSYM) 195 \\ decide_tac 196QED 197 198Theorem v_inv_ignore[simp]: 199 v_inv (t with stack := s) a w = v_inv t a w ��� 200 v_inv (t with pc := p) a w = v_inv t a w ��� 201 v_inv (t with regs := r) a w = v_inv t a w 202Proof 203 qid_spec_tac ���w��� \\ Induct_on ���a��� \\ fs [v_inv_def,read_mem_def] 204QED 205 206fun is_bool tm = type_of tm = type_of T; 207 208Theorem bool_ind: 209 ���P. P F ��� (P F ��� P T) ��� ���b. P b 210Proof 211 rw [] \\ Cases_on ���b��� \\ fs [] 212QED 213 214Theorem has_stack_even: 215 has_stack t xs ��� EVEN (LENGTH t.stack) = ODD (LENGTH xs) 216Proof 217 fs [has_stack_def] \\ rw [] \\ fs [ODD,EVEN_ODD] 218QED 219 220Theorem memory_writable_new: 221 memory_writable x y m ��� x ��� y:word64 ��� 222 can_write_mem_at m x ��� 223 can_write_mem_at m (x + 8w) ��� 224 x ��� 0w ��� 225 ���w1 w2. memory_writable (x+16w) y ((x+8w =+ SOME w2) ((x =+ SOME w1) m)) 226Proof 227 fs [memory_writable_def] \\ strip_tac 228 \\ Cases_on ���x��� \\ Cases_on ���y��� \\ fs [] 229 \\ fs [WORD_LS] \\ fs [aligned_w2n] 230 \\ fs [MOD_EQ_0_DIVISOR] \\ rpt var_eq_tac \\ fs [] 231 \\ fs [WORD_LO,word_add_n2w] \\ rw [] 232 THEN1 233 (first_x_assum match_mp_tac 234 \\ fs [WORD_LO] \\ qexists_tac ���2 * d��� \\ fs []) 235 THEN1 236 (first_x_assum match_mp_tac 237 \\ fs [WORD_LO] \\ qexists_tac ���2 * d + 1��� \\ fs []) 238 THEN1 (qexists_tac ���d + 1��� \\ fs []) 239 \\ fs [PULL_EXISTS] 240 \\ fs [can_write_mem_def,APPLY_UPDATE_THM] 241 \\ Cases_on ���a��� \\ fs [] 242QED 243 244Theorem v_inv_update: 245 ���t v w a b x y. 246 v_inv t v w ��� 247 t.memory a = SOME NONE ��� 248 t.memory b = SOME NONE ��� 249 v_inv (t with memory := (b =+ y) ((a =+ x) t.memory)) v w 250Proof 251 Induct_on ���v��� \\ fs [v_inv_def] 252 \\ fs [read_mem_def,APPLY_UPDATE_THM] 253 \\ rw [] \\ fs [] \\ rw [] \\ fs [] 254QED 255 256Triviality blast_lemma = blastLib.BBLAST_PROVE ���w ��� w + 8w:word64���; 257 258val step_tac = 259 ho_match_mp_tac IMP_step \\ fs [] 260 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 261 \\ simp [take_branch_cases,APPLY_UPDATE_THM,PULL_EXISTS,set_pc_def] 262 \\ fs [write_reg_def,has_stack_def,inc_def,set_pc_def,set_stack_def, 263 EVEN,APPLY_UPDATE_THM,ODD,ODD_ADD,blast_lemma,write_mem_def, 264 EVEN_ODD,ODD,take_branch_cases,unset_reg_def]; 265 266Theorem give_up: 267 code_rel fs ds t.instructions ��� 268 t.regs R15 = SOME w ��� 269 t.pc = give_up (ODD (LENGTH t.stack)) ��� 270 steps (State t,n) (Halt 1w t.output,n) 271Proof 272 fs [code_rel_def,init_code_in_def,init_def,code_in_def] \\ rw [] 273 THEN1 274 (match_mp_tac steps_trans 275 \\ ntac 3 step_tac 276 \\ ho_match_mp_tac IMP_start \\ fs [] 277 \\ once_rewrite_tac [steps_cases] \\ fs []) 278 \\ match_mp_tac steps_trans 279 \\ ntac 2 step_tac 280 \\ ho_match_mp_tac IMP_start \\ fs [] 281 \\ once_rewrite_tac [steps_cases] \\ fs [] 282QED 283 284 285(* proving the cases *) 286 287Theorem c_exp_Const: 288 ^(get_goal "eval _ (Const _)") 289Proof 290 CONV_TAC (RESORT_FORALL_CONV 291 (fn tms => filter is_bool tms @ filter (not o is_bool) tms)) 292 \\ ho_match_mp_tac bool_ind 293 \\ fs [] \\ reverse (rw []) 294 THEN1 295 (qpat_x_assum ���c_exp T _ _ _ _ = _��� mp_tac 296 \\ simp [Once c_exp_alt] 297 \\ Cases_on ���c_exp F t.pc vs fs (Const n)��� \\ fs [] 298 \\ fs [make_ret_def] 299 \\ rw [] \\ fs [flatten_def] 300 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 301 \\ fs [flatten_def] 302 \\ once_rewrite_tac [flatten_acc] \\ fs [] 303 \\ rw [] \\ first_x_assum drule \\ fs [] 304 \\ rpt (disch_then drule) \\ rw [] 305 \\ Cases_on ���outcome��� \\ fs [] 306 \\ reverse (Cases_on ���q'���) \\ fs [] 307 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 308 \\ reverse (Cases_on ���res���) \\ fs [] 309 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 310 \\ rw [] \\ rename [���steps (State t0,s0.clock) (State t1,s1.clock)���] 311 \\ fs [has_stack_def] 312 \\ qpat_x_assum ���_ = t1.stack��� (assume_tac o GSYM) 313 \\ qexists_tac ���State (t1 with <| pc := t1.pc + 1; stack := rest |>), s1.clock��� 314 \\ fs [code_in_def,state_rel_def,fetch_def] 315 \\ imp_res_tac c_exp_length \\ fs [] 316 \\ imp_res_tac steps_inst \\ fs [] 317 \\ match_mp_tac (steps_rules |> CONJUNCTS |> last) 318 \\ goal_assum (first_assum o mp_then Any mp_tac) 319 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 320 \\ ���fetch t1 = SOME (Add_RSP (LENGTH vs))��� by fs [fetch_def] 321 \\ once_rewrite_tac [step_cases] \\ fs [] 322 \\ fs [set_stack_def,inc_def,state_component_equality] 323 \\ qexists_tac ���curr��� \\ fs [env_ok_def]) 324 \\ fs [eval_def] \\ rw [] \\ fs [v_inv_def,PULL_EXISTS] 325 \\ reverse (fs [c_exp_alt,c_const_def,AllCaseEqs()]) \\ rw [] 326 \\ TRY 327 (qabbrev_tac ���ss = curr ++ rest��� 328 \\ fs [has_stack_def,flatten_def,code_in_def] 329 \\ ho_match_mp_tac IMP_step \\ fs [] 330 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 331 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM,set_pc_def,set_stack_def] 332 \\ ho_match_mp_tac IMP_step \\ fs [] 333 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 334 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM,set_pc_def,set_stack_def] 335 \\ ho_match_mp_tac IMP_start \\ fs [] 336 \\ fs [state_rel_def,APPLY_UPDATE_THM] \\ NO_TAC) 337 \\ imp_res_tac has_stack_even 338 \\ pop_assum (assume_tac o GSYM) 339 \\ fs [has_stack_def,flatten_def,code_in_def] 340 \\ ho_match_mp_tac IMP_step \\ fs [] 341 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 342 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM,set_pc_def,set_stack_def, 343 take_branch_cases] 344 \\ qmatch_goalsub_abbrev_tac ���State t1��� 345 \\ ���state_rel fs s t1��� by fs [state_rel_def,Abbr���t1���] 346 \\ fs [state_rel_def] 347 \\ drule give_up \\ fs [] 348 \\ fs [Abbr���t1���] 349 \\ fs [env_ok_def,EVEN_ODD] \\ rfs [] 350 \\ disch_then (qspec_then ���s.clock��� mp_tac) 351 \\ ���ODD (LENGTH curr) = ODD (LENGTH t.stack)��� by 352 (Cases_on ���curr��� \\ fs [] 353 \\ Cases_on ���rest��� \\ fs [ODD,EVEN_ODD] 354 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) \\ fs [ODD_ADD]) 355 \\ fs [] \\ strip_tac 356 \\ goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] 357QED 358 359Theorem c_exp_Var: 360 ^(get_goal "eval _ (Var _)") 361Proof 362 CONV_TAC (RESORT_FORALL_CONV 363 (fn tms => filter is_bool tms @ filter (not o is_bool) tms)) 364 \\ ho_match_mp_tac bool_ind 365 \\ fs [] \\ reverse (rw []) 366 THEN1 367 (qpat_x_assum ���c_exp T _ _ _ _ = _��� mp_tac 368 \\ simp [Once c_exp_alt] 369 \\ rename [���Var v���] \\ rename [���state_rel _ s t���] 370 \\ Cases_on ���c_exp F t.pc vs fs (Var v)��� \\ fs [] 371 \\ fs [make_ret_def] 372 \\ rw [] \\ fs [flatten_def] 373 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 374 \\ fs [flatten_def] 375 \\ once_rewrite_tac [flatten_acc] \\ fs [] 376 \\ rw [] \\ first_x_assum drule \\ fs [] 377 \\ rpt (disch_then drule) \\ rw [] 378 \\ Cases_on ���outcome��� \\ fs [] 379 \\ reverse (Cases_on ���q'���) \\ fs [] 380 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 381 \\ reverse (Cases_on ���res���) \\ fs [] 382 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 383 \\ rw [] \\ rename [���steps (State t0,s0.clock) (State t1,s1.clock)���] 384 \\ fs [has_stack_def] 385 \\ qpat_x_assum ���_ = t1.stack��� (assume_tac o GSYM) 386 \\ qexists_tac ���State (t1 with <| pc := t1.pc + 1; stack := rest |>), s1.clock��� 387 \\ fs [code_in_def,state_rel_def,fetch_def] 388 \\ imp_res_tac c_exp_length \\ fs [] 389 \\ imp_res_tac steps_inst \\ fs [] 390 \\ match_mp_tac (steps_rules |> CONJUNCTS |> last) 391 \\ goal_assum (first_assum o mp_then Any mp_tac) 392 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 393 \\ ���fetch t1 = SOME (Add_RSP (LENGTH vs))��� by fs [fetch_def] 394 \\ once_rewrite_tac [step_cases] \\ fs [] 395 \\ fs [set_stack_def,inc_def,state_component_equality] 396 \\ qexists_tac ���curr��� \\ fs [env_ok_def]) 397 \\ fs [eval_def,AllCaseEqs()] \\ rw [] 398 \\ rename [���Var v���] \\ rename [���state_rel _ s t���] 399 \\ fs [env_ok_def] 400 \\ first_x_assum drule \\ rw [] 401 \\ fs [c_exp_alt,c_var_def] 402 \\ fs [AllCaseEqs()] \\ rw [] 403 \\ fs [flatten_def,code_in_def] 404 THEN1 405 (Cases_on ���vs��� \\ fs [] \\ rw [] \\ fs [] \\ fs [find_def] 406 \\ qpat_x_assum ���_ = 0��� mp_tac 407 \\ once_rewrite_tac [find_acc] \\ fs [AllCaseEqs()] 408 \\ rw [] \\ Cases_on ���curr��� \\ fs [] 409 \\ fs [has_stack_def] \\ rw [] 410 \\ qexists_tac ���(State (t with <| pc := t.pc+1; stack := Word w::t.stack |>), s.clock)��� 411 \\ fs [] \\ fs [state_rel_def] 412 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 413 \\ ���fetch t = SOME (Push RAX)��� by fs [fetch_def] 414 \\ once_rewrite_tac [step_cases] \\ fs [] 415 \\ fs [set_stack_def,inc_def,state_component_equality]) 416 \\ rename [���k < LENGTH _���] 417 \\ qexists_tac ���(State (t with <| pc := t.pc+2; 418 regs := (RAX =+ SOME w) t.regs; 419 stack := (HD curr) :: t.stack |>), s.clock)��� 420 \\ fs [state_rel_def] 421 \\ fs [has_stack_def,APPLY_UPDATE_THM] 422 \\ Cases_on ���curr��� \\ fs [] \\ rpt var_eq_tac 423 \\ match_mp_tac (steps_rules |> CONJUNCTS |> last) 424 \\ qexists_tac ���State (t with <| pc := t.pc+1; 425 stack := Word w' :: t.stack |>)��� 426 \\ qexists_tac ���s.clock��� \\ rw [] 427 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 428 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def] 429 \\ fs [set_stack_def,inc_def,write_reg_def,state_component_equality] 430 \\ qexists_tac ���w��� \\ fs [] 431 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) \\ fs [] 432 \\ Cases_on ���k��� \\ fs [rich_listTheory.EL_APPEND1] 433QED 434 435val op_init_tac = 436 rw [] \\ fs [eval_def,c_exp_alt] 437 \\ Cases_on ���evals env xs s��� \\ fs [] 438 \\ pairarg_tac \\ fs [] \\ rw [] 439 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 440 \\ fs [flatten_def] 441 \\ once_rewrite_tac [flatten_acc] \\ fs [] \\ rw [] 442 \\ Cases_on ���q = Err Crash��� \\ fs [] 443 \\ first_x_assum drule \\ fs [] 444 \\ rpt (disch_then drule) \\ rw [] 445 \\ reverse (Cases_on ���q���) \\ fs [] \\ rw [] 446 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 447 \\ imp_res_tac eval_op_mono 448 \\ Cases_on ���outcome��� \\ fs [] 449 \\ reverse (Cases_on ���q���) \\ fs [] 450 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 451 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS) 452 \\ rename [���eval_op _ vs s0 = _���] 453 \\ first_x_assum (qspec_then ���vs��� strip_assume_tac) \\ fs [] \\ rw [] 454 \\ rename [���steps (State t1,s1.clock) (State t2,s2.clock)���] 455 \\ ho_match_mp_tac IMP_steps \\ goal_assum (first_assum o mp_then Any mp_tac) 456 \\ imp_res_tac c_exp_length 457 \\ fs [c_op_def,c_head_def,c_tail_def,c_cons_def,c_add_def,c_sub_def, 458 c_div_def,c_read_def,c_write_def,code_in_def] 459 \\ imp_res_tac steps_inst; 460 461Theorem c_exp_Cons: 462 ~tail' ��� f = Cons ��� 463 ^(strip (get_goal "eval _ (Op _ _)")) 464Proof 465 op_init_tac 466 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] 467 \\ rw [] \\ fs [env_ok_def] \\ rw [] \\ fs [] \\ rfs [] 468 \\ imp_res_tac has_stack_even 469 \\ fs [has_stack_def] 470 \\ qpat_x_assum ���_ = t2.stack��� (assume_tac o GSYM) 471 \\ ���init_code_in t1.instructions��� by fs [state_rel_def,code_rel_def] 472 \\ fs [init_code_in_def,code_in_def,init_def,EVEN,ODD] 473 THEN1 474 (ho_match_mp_tac IMP_step \\ fs [] 475 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 476 \\ fs [write_reg_def,has_stack_def,inc_def,set_pc_def,set_stack_def] 477 \\ ntac 2 step_tac 478 \\ fs [state_rel_def] 479 \\ IF_CASES_TAC \\ rw [] 480 THEN1 (ntac 3 step_tac \\ ho_match_mp_tac IMP_start \\ fs []) 481 \\ drule memory_writable_new \\ fs [] \\ strip_tac 482 \\ fs [can_write_mem_def] 483 \\ ntac 6 step_tac 484 \\ ho_match_mp_tac IMP_start \\ fs [APPLY_UPDATE_THM] 485 \\ fs [v_inv_def,read_mem_def,APPLY_UPDATE_THM,blast_lemma] 486 \\ rw [] \\ match_mp_tac v_inv_update \\ fs []) 487 THEN1 488 (ho_match_mp_tac IMP_step \\ fs [] 489 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 490 \\ fs [write_reg_def,has_stack_def,inc_def] 491 \\ ntac 2 step_tac 492 \\ fs [state_rel_def,ODD,EVEN] 493 \\ IF_CASES_TAC \\ rw [] 494 THEN1 (ntac 3 step_tac \\ ho_match_mp_tac IMP_start \\ fs []) 495 \\ drule memory_writable_new \\ fs [] \\ strip_tac 496 \\ fs [can_write_mem_def] 497 \\ ntac 5 step_tac 498 \\ ho_match_mp_tac IMP_start \\ fs [APPLY_UPDATE_THM] 499 \\ fs [v_inv_def,read_mem_def,APPLY_UPDATE_THM,blast_lemma] 500 \\ rw [] \\ match_mp_tac v_inv_update \\ fs []) 501QED 502 503Theorem c_exp_Head: 504 ~tail' ��� f = Head ��� 505 ^(strip (get_goal "eval _ (Op _ _)")) 506Proof 507 op_init_tac \\ step_tac 508 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 509 \\ fs [] \\ rw [] \\ fs [] 510 \\ fs [has_stack_def,wordsTheory.w2w_def,v_inv_def] 511 \\ ho_match_mp_tac IMP_start \\ fs [] 512 \\ fs [write_reg_def,inc_def,state_rel_def,APPLY_UPDATE_THM] 513QED 514 515Theorem c_exp_Tail: 516 ~tail' ��� f = Tail ��� 517 ^(strip (get_goal "eval _ (Op _ _)")) 518Proof 519 op_init_tac \\ step_tac 520 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 521 \\ fs [] \\ rw [] \\ fs [] 522 \\ fs [has_stack_def,wordsTheory.w2w_def,v_inv_def] 523 \\ ho_match_mp_tac IMP_start \\ fs [] 524 \\ fs [write_reg_def,inc_def,state_rel_def,APPLY_UPDATE_THM] 525QED 526 527Theorem c_exp_Add: 528 ~tail' ��� f = Add ��� 529 ^(strip (get_goal "eval _ (Op _ _)")) 530Proof 531 op_init_tac 532 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 533 \\ fs [] \\ rw [] \\ fs [v_inv_def,GSYM PULL_FORALL] \\ rw [] \\ fs [] 534 \\ imp_res_tac has_stack_even 535 \\ fs [has_stack_def] 536 \\ qpat_x_assum ���_ = t2.stack��� (assume_tac o GSYM) 537 \\ ntac 3 step_tac 538 \\ fs [state_rel_def,word_add_n2w] 539 \\ reverse IF_CASES_TAC \\ fs [] 540 THEN1 (ho_match_mp_tac IMP_start \\ fs [APPLY_UPDATE_THM] 541 \\ fs [v_inv_def,read_mem_def,FLOOKUP_UPDATE,blast_lemma]) 542 \\ qmatch_goalsub_abbrev_tac ���State t3,nn��� 543 \\ ���code_rel fs s1.funs t3.instructions��� by fs [Abbr���t3���] 544 \\ drule give_up 545 \\ fs [Abbr���t3���,APPLY_UPDATE_THM,ODD,EVEN_ODD,env_ok_def] 546 \\ disch_then (qspec_then ���nn��� assume_tac) 547 \\ goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] 548QED 549 550Theorem c_exp_Sub: 551 ~tail' ��� f = Sub ��� 552 ^(strip (get_goal "eval _ (Op _ _)")) 553Proof 554 op_init_tac 555 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 556 \\ fs [] \\ rw [] \\ fs [v_inv_def] \\ rw [] \\ fs [] 557 \\ step_tac 558 \\ qpat_x_assum ���_ = t2.stack��� (assume_tac o GSYM) \\ fs [set_stack_def] 559 \\ step_tac 560 \\ IF_CASES_TAC \\ fs [NOT_LESS] 561 \\ imp_res_tac (DECIDE ���n ��� m ��� n-m=0���) \\ asm_rewrite_tac [] 562 \\ simp [GSYM PULL_FORALL,v_inv_def,set_pc_def] 563 THEN1 564 (ntac 2 step_tac 565 \\ ho_match_mp_tac IMP_start \\ fs [] 566 \\ fs [write_reg_def,inc_def,state_rel_def,APPLY_UPDATE_THM] 567 \\ rename [���n < m���] \\ ���n ��� m��� by fs [] 568 \\ fs [LESS_EQ_EXISTS] \\ rw [] \\ fs [GSYM word_add_n2w]) 569 \\ ntac 3 step_tac 570 \\ ho_match_mp_tac IMP_start \\ fs [] 571 \\ fs [write_reg_def,inc_def,state_rel_def,APPLY_UPDATE_THM] 572QED 573 574Theorem c_exp_Div: 575 ~tail' ��� f = Div ��� 576 ^(strip (get_goal "eval _ (Op _ _)")) 577Proof 578 op_init_tac 579 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 580 \\ fs [] \\ rw [] \\ fs [] \\ step_tac 581 \\ qpat_x_assum ���_ = t2.stack��� (assume_tac o GSYM) 582 \\ ntac 3 step_tac 583 \\ fs [v_inv_def] \\ rw [] \\ fs [] 584 \\ ho_match_mp_tac IMP_start \\ fs [] 585 \\ fs [state_rel_def,v_inv_def,DIV_LT_X,APPLY_UPDATE_THM] 586QED 587 588Theorem c_exp_Read: 589 ~tail' ��� f = Read ��� 590 ^(strip (get_goal "eval _ (Op _ _)")) 591Proof 592 op_init_tac 593 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 594 \\ fs [] \\ rw [] \\ fs [v_inv_def,GSYM PULL_FORALL,align_def] 595 \\ rename [���env_ok env vs curr t1���] 596 \\ Cases_on ���EVEN (LENGTH vs)��� \\ fs [code_in_def] 597 THEN1 598 (fs [has_stack_def] 599 \\ ntac 3 step_tac 600 \\ ���ODD (LENGTH (curr ++ rest))��� by 601 (rewrite_tac [LENGTH_APPEND] \\ rfs [EVEN_ODD,ODD_ADD,env_ok_def]) 602 \\ pop_assum mp_tac \\ asm_rewrite_tac [LENGTH,EVEN] 603 \\ simp [LENGTH,EVEN,ODD_EVEN] \\ rw [] 604 \\ Cases_on ���t2.input��� \\ fs [PULL_EXISTS,read_char_def] 605 \\ step_tac \\ ho_match_mp_tac IMP_start \\ fs [] 606 \\ ���ORD h < 256��� by fs [ORD_BOUND] 607 \\ fs [state_rel_def,v_inv_def,APPLY_UPDATE_THM,next_def]) 608 THEN1 609 (fs [has_stack_def] 610 \\ ntac 2 step_tac 611 \\ ���EVEN (LENGTH (curr ++ rest))��� by 612 (rewrite_tac [LENGTH_APPEND] \\ rfs [EVEN_ODD,ODD_ADD,env_ok_def]) 613 \\ pop_assum mp_tac 614 \\ asm_rewrite_tac [LENGTH,EVEN] 615 \\ simp [LENGTH,EVEN,ODD_EVEN] \\ rw [] 616 \\ Cases_on ���t2.input��� \\ fs [PULL_EXISTS,read_char_def] 617 \\ ho_match_mp_tac IMP_start \\ fs [] 618 \\ ���ORD h < 256��� by fs [ORD_BOUND] 619 \\ fs [state_rel_def,v_inv_def,APPLY_UPDATE_THM,next_def]) 620QED 621 622Theorem c_exp_Write: 623 ~tail' ��� f = Write ��� 624 ^(strip (get_goal "eval _ (Op _ _)")) 625Proof 626 op_init_tac 627 \\ fs [eval_op_def,AllCaseEqs(),fail_def,return_def] \\ rw [] 628 \\ fs [] \\ rw [] \\ fs [v_inv_def,GSYM PULL_FORALL,align_def] 629 \\ rename [���env_ok env vs curr t1���] 630 \\ Cases_on ���EVEN (LENGTH vs)��� \\ fs [code_in_def] 631 THEN1 632 (ntac 3 step_tac 633 \\ CONV_TAC (RESORT_EXISTS_CONV rev) \\ rfs [] 634 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 635 \\ ���ODD (LENGTH (curr ++ rest))��� by 636 (rewrite_tac [LENGTH_APPEND] \\ rfs [EVEN_ODD,ODD_ADD,env_ok_def]) 637 \\ pop_assum mp_tac 638 \\ asm_rewrite_tac [LENGTH,EVEN] 639 \\ simp [LENGTH,EVEN,ODD_EVEN] \\ rw [] 640 \\ fs [unset_reg_def,put_char_def] 641 \\ ntac 2 step_tac 642 \\ ho_match_mp_tac IMP_start \\ fs [] 643 \\ fs [state_rel_def,APPLY_UPDATE_THM]) 644 THEN1 645 (ntac 2 step_tac 646 \\ CONV_TAC (RESORT_EXISTS_CONV rev) \\ rfs [] 647 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 648 \\ ���EVEN (LENGTH (curr ++ rest))��� by 649 (rewrite_tac [LENGTH_APPEND] \\ rfs [EVEN_ODD,ODD_ADD,env_ok_def]) 650 \\ pop_assum mp_tac 651 \\ asm_rewrite_tac [LENGTH,EVEN] 652 \\ simp [LENGTH,EVEN,ODD_EVEN] \\ rw [] 653 \\ fs [unset_reg_def,put_char_def] 654 \\ step_tac 655 \\ ho_match_mp_tac IMP_start \\ fs [] 656 \\ fs [state_rel_def,APPLY_UPDATE_THM]) 657QED 658 659Theorem c_exp_Op: 660 ^(get_goal "eval _ (Op _ _)") 661Proof 662 fs [PULL_FORALL] 663 \\ CONV_TAC (RESORT_FORALL_CONV 664 (fn tms => filter is_bool tms @ filter (not o is_bool) tms)) 665 \\ ho_match_mp_tac bool_ind 666 \\ fs [] \\ reverse (rw []) 667 THEN1 668 (qpat_x_assum ���c_exp T _ _ _ _ = _��� mp_tac 669 \\ simp [Once c_exp_alt] 670 \\ Cases_on ���c_exp F t.pc vs fs (Op f xs)��� \\ fs [] 671 \\ fs [make_ret_def] 672 \\ rw [] \\ fs [flatten_def] 673 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 674 \\ fs [flatten_def] 675 \\ once_rewrite_tac [flatten_acc] \\ fs [] 676 \\ rw [] \\ first_x_assum drule \\ fs [] 677 \\ rpt (disch_then drule) \\ rw [] 678 \\ Cases_on ���outcome��� \\ fs [] 679 \\ reverse (Cases_on ���q'���) \\ fs [] 680 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 681 \\ reverse (Cases_on ���res���) \\ fs [] 682 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 683 \\ rw [] \\ rename [���steps (State t0,s0.clock) (State t1,s1.clock)���] 684 \\ last_x_assum kall_tac 685 \\ first_x_assum (qspec_then ���a��� mp_tac) \\ fs [] \\ strip_tac 686 \\ fs [has_stack_def] 687 \\ qpat_x_assum ���_ = t1.stack��� (assume_tac o GSYM) 688 \\ qexists_tac ���State (t1 with <| pc := t1.pc + 1; stack := rest |>), s1.clock��� 689 \\ fs [code_in_def,state_rel_def,fetch_def] 690 \\ imp_res_tac c_exp_length \\ fs [] 691 \\ imp_res_tac steps_inst \\ fs [] 692 \\ match_mp_tac (steps_rules |> CONJUNCTS |> last) 693 \\ goal_assum (first_assum o mp_then Any mp_tac) 694 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 695 \\ ���fetch t1 = SOME (Add_RSP (LENGTH vs))��� by fs [fetch_def] 696 \\ once_rewrite_tac [step_cases] \\ fs [] 697 \\ fs [set_stack_def,inc_def,state_component_equality] 698 \\ qexists_tac ���curr��� \\ fs [env_ok_def]) 699 \\ Cases_on ���f��� \\ rw [] 700 \\ EVERY ([c_exp_Cons, c_exp_Head, c_exp_Tail, c_exp_Add, 701 c_exp_Sub, c_exp_Div, c_exp_Read, c_exp_Write] 702 |> map (drule o SIMP_RULE std_ss [] o GEN_ALL)) 703 \\ rpt (disch_then (fn th => (drule_all th \\ strip_tac) ORELSE all_tac)) 704 \\ qexists_tac ���outcome��� \\ fs [] 705QED 706 707Theorem c_test_thm: 708 state_rel fs s t ��� 709 LIST_REL (v_inv t) args ws ��� 710 take_branch test args s = (Res b,s) ��� 711 has_stack t (MAP Word (REVERSE ws) ��� rest) ��� 712 has_stack k rest ��� 713 code_in t.pc (c_test test l4) t.instructions ��� 714 ���t1. 715 steps (State t,s.clock) (State t1,s.clock) ��� 716 state_rel fs s t1 ��� has_stack t1 rest ��� 717 t1.pc = if b then l4 else t.pc + 4 718Proof 719 Cases_on ���test��� \\ fs [] 720 \\ fs [source_semanticsTheory.take_branch_def,fail_def,AllCaseEqs(),return_def] 721 \\ rw [] \\ fs [] \\ rw [] \\ fs [] 722 \\ fs [v_inv_def] \\ rw [] 723 \\ fs [has_stack_def] 724 \\ qpat_x_assum ���_ = _.stack��� (assume_tac o GSYM) \\ fs [] 725 \\ fs [c_test_def,code_in_def] 726 \\ ho_match_mp_tac IMP_steps_state 727 \\ ntac 4 (ho_match_mp_tac IMP_step \\ fs [] 728 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def] 729 \\ fs [write_reg_def,has_stack_def,inc_def,set_stack_def]) 730 \\ fs [x64asm_semanticsTheory.take_branch_cases,PULL_EXISTS, 731 APPLY_UPDATE_THM,set_pc_def] 732 \\ qmatch_goalsub_abbrev_tac ���State tt��� 733 \\ qexists_tac ���(State tt,s.clock)��� \\ fs [] 734 \\ qexists_tac ���tt��� \\ fs [] 735 \\ once_rewrite_tac [steps_cases] \\ fs [] 736 \\ rw [Abbr���tt���] \\ fs [state_rel_def,APPLY_UPDATE_THM] 737QED 738 739Theorem c_exp_If: 740 ^(get_goal "eval _ (If _ _ _ _)") 741Proof 742 rw [] \\ fs [eval_def,c_exp_alt,c_if_def] 743 \\ Cases_on ���evals env xs s��� \\ fs [] 744 \\ rpt (pairarg_tac \\ fs []) \\ rw [] 745 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 746 \\ fs [flatten_def] 747 \\ once_rewrite_tac [flatten_acc] \\ fs [] 748 \\ once_rewrite_tac [flatten_acc] \\ fs [] 749 \\ once_rewrite_tac [flatten_acc] \\ fs [] 750 \\ rpt strip_tac \\ rpt var_eq_tac \\ fs [code_in_def] 751 \\ Cases_on ���q = Err Crash��� \\ fs [] 752 \\ first_x_assum drule \\ fs [] 753 \\ rpt (disch_then drule) \\ rw [] 754 \\ reverse (Cases_on ���q���) \\ fs [] \\ rw [] 755 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 756 \\ rename [���take_branch test args s5���] 757 \\ Cases_on ���take_branch test args s5��� \\ fs [] 758 \\ rename [���_ = (taken,s6)���] 759 \\ ���s6 = s5��� by 760 (fs [AllCaseEqs(),source_semanticsTheory.take_branch_def,fail_def,return_def] \\ rw []) 761 \\ rw [] 762 \\ PairCases_on ���outcome��� \\ fs [] 763 \\ reverse (Cases_on ���outcome0���) \\ fs [] 764 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 765 \\ fs [AllCaseEqs()] 766 \\ rw [] \\ fs [] \\ imp_res_tac eval_mono 767 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS \\ fs []) 768 \\ qpat_x_assum ���_ = (res,s1)��� mp_tac 769 \\ simp [AllCaseEqs(),source_semanticsTheory.take_branch_def,fail_def, 770 return_def,PULL_EXISTS] 771 \\ reverse (rw []) \\ fs [] 772 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 773 \\ rfs [] \\ rename [���state_rel fs s5 t5���] 774 \\ imp_res_tac c_exp_length \\ fs [] 775 \\ rpt var_eq_tac \\ fs [] 776 \\ ho_match_mp_tac IMP_steps \\ goal_assum (first_assum o mp_then Any mp_tac) 777 \\ pop_assum (assume_tac o GSYM) 778 \\ qmatch_asmsub_abbrev_tac ���c_test _ l4��� \\ fs [] 779 \\ ���LENGTH (c_test test l4) = 4��� by (Cases_on ���test��� \\ fs [c_test_def]) 780 \\ fs [] 781 \\ ���t.instructions = t5.instructions��� by (imp_res_tac steps_inst \\ fs []) \\ fs [] 782 \\ drule_all (c_test_thm |> Q.INST [���rest���|->���curr++rest���] 783 |> SIMP_RULE (srw_ss()) []) 784 \\ strip_tac 785 \\ ho_match_mp_tac IMP_steps \\ goal_assum (first_assum o mp_then Any mp_tac) 786 \\ pop_assum (assume_tac o GSYM) 787 \\ Cases_on ���b��� \\ fs [] 788 THEN1 789 (first_x_assum drule \\ fs [] 790 \\ disch_then (qspecl_then [���curr���,���rest���] mp_tac) 791 \\ reverse impl_tac THEN1 (metis_tac []) 792 \\ fs [] \\ imp_res_tac steps_inst \\ fs [] 793 \\ fs [env_ok_def] \\ rw [] \\ res_tac \\ fs [] 794 \\ imp_res_tac steps_v_inv \\ fs [] 795 \\ Cases_on ���tail'��� \\ fs []) 796 \\ qpat_x_assum ���_ = t5.pc��� (assume_tac o GSYM) \\ fs [] 797 \\ first_x_assum drule \\ fs [] 798 \\ disch_then (qspecl_then [���curr���,���rest���] mp_tac) 799 \\ impl_tac THEN1 800 (fs [] \\ imp_res_tac steps_inst \\ fs [] 801 \\ fs [env_ok_def] \\ rw [] \\ res_tac \\ fs [] 802 \\ imp_res_tac steps_v_inv \\ fs []) 803 \\ strip_tac 804 \\ ho_match_mp_tac IMP_steps \\ fs [] 805 \\ goal_assum (first_assum o mp_then Any mp_tac) 806 \\ PairCases_on ���outcome��� \\ fs [] 807 \\ reverse (Cases_on ���outcome0���) \\ fs [] 808 THEN1 (ho_match_mp_tac IMP_start \\ fs []) 809 \\ reverse (Cases_on ���res���) \\ fs [] 810 THEN1 (ho_match_mp_tac IMP_start \\ fs []) 811 \\ rename [���COND taill���] \\ Cases_on ���taill��� \\ fs [] 812 THEN1 (ho_match_mp_tac IMP_start \\ fs [] \\ fs [has_stack_def]) 813 \\ imp_res_tac steps_inst 814 \\ fs [has_stack_def,code_in_def] 815 \\ step_tac 816 \\ ho_match_mp_tac IMP_start \\ fs [] 817 \\ fs [state_rel_def] 818QED 819 820Theorem c_exp_Let: 821 ^(get_goal "eval _ (Let _ _ _)") 822Proof 823 fs [eval_def,c_exp_alt] \\ rw [] 824 \\ rpt (pairarg_tac \\ fs []) 825 \\ rpt var_eq_tac 826 \\ Cases_on ���eval env x s��� \\ fs [] 827 \\ Cases_on ���q = Err Crash��� \\ fs [] 828 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 829 \\ fs [flatten_def] 830 \\ once_rewrite_tac [flatten_acc] \\ fs [] 831 \\ once_rewrite_tac [flatten_acc] \\ fs [] 832 \\ strip_tac 833 \\ first_x_assum drule 834 \\ rpt (disch_then drule) 835 \\ strip_tac 836 \\ Cases_on ���outcome��� 837 \\ rename [���steps _ (r1,r2)���] 838 \\ reverse (Cases_on ���r1���) \\ fs [] 839 THEN1 840 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 841 \\ fs [AllCaseEqs()] \\ rw [] 842 \\ imp_res_tac eval_mono 843 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS) 844 \\ reverse (Cases_on ���q���) \\ fs [] 845 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] \\ rw []) 846 \\ rename [���eval env���vname ��� SOME v��� y s2 = (res,s3)���] \\ rw [] 847 \\ first_x_assum drule \\ fs [] 848 \\ disch_then (qspecl_then [���Word w :: curr���,���rest���] mp_tac) 849 \\ impl_tac THEN1 850 (imp_res_tac c_exp_length \\ fs [] 851 \\ imp_res_tac steps_inst \\ fs [] 852 \\ rw [] \\ fs [env_ok_def] \\ rw [] 853 \\ rw [] \\ fs [find_def] \\ rw [] 854 \\ once_rewrite_tac [find_acc] \\ fs [ADD1] 855 \\ fs [GSYM ADD1,APPLY_UPDATE_THM] 856 \\ imp_res_tac steps_v_inv \\ fs [] \\ res_tac \\ fs []) 857 \\ strip_tac 858 \\ Cases_on ���tail'��� 859 THEN1 860 (qexists_tac ���outcome��� 861 \\ conj_tac THEN1 (Cases_on ���outcome��� \\ imp_res_tac steps_rules \\ fs []) 862 \\ Cases_on ���outcome��� 863 \\ fs [AllCaseEqs()] \\ rw [] 864 \\ Cases_on ���q��� \\ fs [] 865 \\ imp_res_tac eval_mono 866 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS \\ fs [PULL_EXISTS] 867 \\ rw [] \\ rpt (goal_assum (first_assum o mp_then Any mp_tac))) 868 \\ fs [] 869 \\ Cases_on ���outcome��� \\ fs [] 870 \\ reverse (Cases_on ���q���) \\ fs [] 871 THEN1 872 (rename [���steps (State s8,s2.clock) (Halt Failure out,r5)���] 873 \\ qexists_tac ���Halt Failure out,r5��� \\ fs [] 874 \\ imp_res_tac steps_rules \\ fs []) 875 \\ reverse (Cases_on ���res���) \\ fs [] 876 THEN1 877 (qexists_tac ���State s'',s3.clock��� \\ fs [] 878 \\ imp_res_tac steps_rules \\ fs []) 879 \\ rename [���steps (State t7,s2.clock) (State t8,s3.clock)���] \\ rw [] 880 \\ qexists_tac ���(State (t8 with <| pc := t8.pc+1; stack := TL t8.stack |>), s3.clock)��� 881 \\ fs [] \\ rpt strip_tac 882 \\ TRY (fs [state_rel_def] \\ NO_TAC) 883 THEN1 884 (match_mp_tac (steps_rules |> CONJUNCTS |> last) 885 \\ goal_assum (first_assum o mp_then Any mp_tac) 886 \\ match_mp_tac (steps_rules |> CONJUNCTS |> last) 887 \\ goal_assum (first_assum o mp_then Any mp_tac) 888 \\ match_mp_tac (steps_rules |> CONJUNCTS |> el 2) 889 \\ fs [code_in_def] 890 \\ imp_res_tac c_exp_length \\ fs [] 891 \\ imp_res_tac steps_inst \\ fs [] 892 \\ ���fetch t8 = SOME (Add_RSP 1)��� by fs [fetch_def] 893 \\ once_rewrite_tac [step_cases] \\ fs [] 894 \\ fs [set_stack_def,inc_def,state_component_equality] 895 \\ qexists_tac ���[HD t8.stack]��� \\ fs [] 896 \\ fs [has_stack_def] 897 \\ qpat_x_assum ���_ = t8.stack��� (assume_tac o GSYM) \\ fs []) 898 \\ goal_assum (first_assum o mp_then Any mp_tac) 899 \\ fs [has_stack_def] \\ rfs [] 900 \\ metis_tac [TL] 901QED 902 903val Call_init_tac = rw [] \\ rpt (pop_assum mp_tac) \\ Cases_on ���tail'��� 904val [Call_tail,Call_not_tail] = 905 ([],get_goal "eval _ (Call _ _)") 906 |> Call_init_tac |> fst |> map snd 907 908Definition write_regs_def: 909 write_regs [] rs = rs ��� 910 write_regs ((x,y)::xs) rs = (x =+ SOME y) (write_regs xs rs) 911End 912 913Overload ARGS[inferior] = ���[RDI;RDX;RBX;RBP]��� 914 915Definition pops_regs_def: 916 pops_regs (ws:word64 list) rs = 917 if ws = [] ��� 5 < LENGTH ws then rs else 918 write_regs (ZIP(REVERSE (TAKE ((LENGTH ws)-1) ARGS), ws)) rs 919End 920 921Theorem c_pops_thm: 922 has_stack t (MAP Word (REVERSE ws) ++ rest) ��� 923 code_in t.pc (c_pops (xs:exp list) (vs:num option list)) 924 t.instructions ��� code_rel fs ds t.instructions ��� 925 t.regs R15 = SOME r15 ��� 926 LENGTH xs = LENGTH ws ��� (EVEN (LENGTH vs) = ODD (LENGTH rest)) ��� 927 ���outcome. 928 steps (State t,n) outcome ��� 929 case outcome of 930 | (Halt ec output,m) => t.output = output ��� ec = 1w 931 | (State t1,m) => m = n ��� LENGTH ws ��� 5 ��� 932 t1 = t with <| regs := pops_regs ws t.regs; 933 pc := t.pc + LENGTH (c_pops xs vs); 934 stack := rest |> 935Proof 936 fs [c_pops_def,pops_regs_def] 937 \\ Cases_on ���xs = []��� \\ fs [] 938 THEN1 939 (Cases_on ���ws = []��� \\ fs [] 940 \\ fs [has_stack_def] \\ rw [] \\ fs [code_in_def] 941 \\ step_tac 942 \\ ho_match_mp_tac IMP_start 943 \\ once_rewrite_tac [steps_cases] \\ fs [state_component_equality]) 944 \\ Cases_on ���ws = []��� \\ fs [] 945 \\ IF_CASES_TAC 946 THEN1 947 (fs [LENGTH_EQ_NUM_compute] \\ rw [] \\ fs [ZIP_def,write_regs_def] 948 \\ ho_match_mp_tac IMP_start \\ fs [state_component_equality] 949 \\ fs [has_stack_def]) 950 \\ Cases_on ���xs��� \\ fs [] \\ rename [���LENGTH xs���] 951 \\ Cases_on ���xs��� \\ fs [] \\ rename [���LENGTH xs���] 952 \\ Cases_on ���xs��� \\ fs [] 953 THEN1 954 (fs [LENGTH_EQ_NUM_compute] \\ rw [] 955 \\ fs [ZIP_def,write_regs_def,code_in_def,has_stack_def] 956 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) 957 \\ step_tac 958 \\ ho_match_mp_tac IMP_start 959 \\ once_rewrite_tac [steps_cases] \\ fs [state_component_equality]) 960 \\ rename [���LENGTH xs���] \\ Cases_on ���xs��� \\ fs [] 961 THEN1 962 (fs [LENGTH_EQ_NUM_compute] \\ rw [] 963 \\ fs [ZIP_def,write_regs_def,code_in_def,has_stack_def] 964 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) 965 \\ ntac 2 step_tac 966 \\ ho_match_mp_tac IMP_start 967 \\ once_rewrite_tac [steps_cases] \\ fs [state_component_equality]) 968 \\ rename [���LENGTH xs���] \\ Cases_on ���xs��� \\ fs [] 969 THEN1 970 (fs [LENGTH_EQ_NUM_compute] \\ rw [] 971 \\ fs [ZIP_def,write_regs_def,code_in_def,has_stack_def] 972 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) 973 \\ ntac 3 step_tac 974 \\ ho_match_mp_tac IMP_start 975 \\ once_rewrite_tac [steps_cases] \\ fs [state_component_equality]) 976 \\ rename [���LENGTH xs���] \\ Cases_on ���xs��� \\ fs [] 977 THEN1 978 (fs [LENGTH_EQ_NUM_compute] \\ rw [] 979 \\ fs [ZIP_def,write_regs_def,code_in_def,has_stack_def] 980 \\ qpat_x_assum ���_ = t.stack��� (assume_tac o GSYM) 981 \\ ntac 4 step_tac 982 \\ ho_match_mp_tac IMP_start 983 \\ once_rewrite_tac [steps_cases] \\ fs [state_component_equality]) 984 THEN1 985 (fs [code_in_def] \\ rpt strip_tac 986 \\ step_tac 987 \\ qmatch_goalsub_abbrev_tac ���State t1��� 988 \\ ���code_rel fs ds t1.instructions��� by fs [Abbr���t1���] 989 \\ drule (GEN_ALL give_up) 990 \\ fs [Abbr���t1���,has_stack_def] 991 \\ disch_then (qspec_then ���n��� mp_tac) 992 \\ qsuff_tac ���ODD (LENGTH t.stack) = ODD (LENGTH ws + LENGTH vs)��� 993 THEN1 (strip_tac \\ fs [ODD_ADD] \\ strip_tac 994 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 995 \\ ���ODD (LENGTH t.stack) = ~ODD (LENGTH (Word w :: t.stack))��� by fs [ODD] 996 \\ asm_rewrite_tac [] 997 \\ qpat_x_assum ���_ = _ :: t.stack��� (assume_tac o GSYM) 998 \\ asm_rewrite_tac [] \\ fs [EVEN_ODD,ODD_ADD] 999 \\ fs [ODD_EVEN] \\ fs [EVEN] \\ metis_tac []) 1000QED 1001 1002Theorem c_pushes_thm: 1003 c_pushes params pos = (c,vs1,l1) ��� 1004 code_in t.pc (flatten c []) t.instructions ��� 1005 t.regs = pops_regs ws regs ��� 1006 t.stack = rest ��� LENGTH params ��� 5 ��� 1007 t.regs RAX = SOME w ��� 1008 (ws ��� [] ��� LAST ws = w) ��� 1009 LIST_REL (v_inv t) args ws ��� 1010 LENGTH ws = LENGTH params ��� 1011 state_rel fs r t ��� 1012 ���new_curr t5. 1013 steps (State t,n) (State t5,n) ��� 1014 t5.pc = t.pc + LENGTH (flatten c []) ��� 1015 l1 = pos + LENGTH (flatten c []) ��� 1016 has_stack t5 (new_curr ++ rest) ��� 1017 env_ok (make_env params args empty_env) vs1 new_curr t5 ��� 1018 state_rel fs r t5 ��� 1019 t5.instructions = t.instructions 1020Proof 1021 rw [] 1022 \\ ���(���n. ~MEM n ARGS ��� regs n = t.regs n)��� by 1023 (fs [] \\ Cases \\ fs [pops_regs_def] \\ rw [] \\ fs [] 1024 \\ Cases_on ���params��� \\ fs [] \\ Cases_on ���ws��� \\ fs [] \\ rw [] 1025 \\ rpt (rename [���LENGTH params = LENGTH ws���] 1026 \\ Cases_on ���params��� \\ fs [] \\ Cases_on ���ws��� \\ fs [] 1027 \\ rw [ZIP_def,write_regs_def,APPLY_UPDATE_THM])) 1028 \\ Cases_on ���ws��� \\ fs [] 1029 THEN1 1030 (rw [] \\ fs [c_pushes_def] \\ rw [] 1031 \\ fs [flatten_def,code_in_def,pops_regs_def,make_env_def] 1032 \\ qexists_tac ���[Word w]��� \\ fs [] 1033 \\ qexists_tac ���t��� \\ fs [] 1034 \\ fs [has_stack_def,env_ok_def,empty_env_def]) 1035 \\ rw [] \\ rename [���SUC (LENGTH ws)���] 1036 \\ Cases_on ���ws��� \\ fs [] 1037 THEN1 1038 (rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1039 \\ fs [c_pushes_def] \\ rw [] \\ fs [flatten_def] 1040 \\ rename [���make_env [k] [x]���] 1041 \\ qexists_tac ���[Word h]��� 1042 \\ qexists_tac ���t��� \\ fs [] 1043 \\ fs [has_stack_def] 1044 \\ fs [env_ok_def,make_env_def,APPLY_UPDATE_THM] \\ rw [] 1045 \\ EVAL_TAC \\ fs [empty_env_def]) 1046 \\ rw[] \\ fs [] \\ rw [] \\ rename [���SUC (LENGTH ws)���] 1047 \\ Cases_on ���ws��� \\ fs [] 1048 THEN1 1049 (rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1050 \\ fs [c_pushes_def] \\ rw [] \\ fs [flatten_def] 1051 \\ qexists_tac ���[Word h'; Word h]��� \\ fs [] 1052 \\ fs [code_in_def,pops_regs_def,ZIP_def,write_regs_def] 1053 \\ ho_match_mp_tac IMP_steps_alt 1054 \\ step_tac 1055 \\ fs [GSYM PULL_EXISTS] 1056 \\ ho_match_mp_tac IMP_start \\ fs [] 1057 \\ qmatch_goalsub_abbrev_tac ���State t1��� 1058 \\ qexists_tac ���t1��� 1059 \\ fs [Abbr���t1���,has_stack_def,APPLY_UPDATE_THM] 1060 \\ fs [state_rel_def,APPLY_UPDATE_THM] 1061 \\ fs [env_ok_def,make_env_def,empty_env_def,APPLY_UPDATE_THM] 1062 \\ rw [] \\ EVAL_TAC \\ fs []) 1063 \\ rw[] \\ fs [] \\ rw [] \\ rename [���SUC (LENGTH ws)���] 1064 \\ Cases_on ���ws��� \\ fs [] 1065 THEN1 1066 (rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1067 \\ fs [c_pushes_def] \\ rw [] \\ fs [flatten_def] 1068 \\ qexists_tac ���[Word h''; Word h'; Word h]��� \\ fs [] 1069 \\ fs [code_in_def,pops_regs_def,ZIP_def,write_regs_def] 1070 \\ ho_match_mp_tac IMP_steps_alt 1071 \\ ntac 2 (ho_match_mp_tac IMP_step \\ fs [] 1072 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1073 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN] 1074 \\ fs [GSYM PULL_EXISTS]) 1075 \\ ho_match_mp_tac IMP_start \\ fs [] 1076 \\ qmatch_goalsub_abbrev_tac ���State t1��� 1077 \\ qexists_tac ���t1��� 1078 \\ fs [Abbr���t1���,has_stack_def,APPLY_UPDATE_THM] 1079 \\ fs [state_rel_def,APPLY_UPDATE_THM] 1080 \\ fs [env_ok_def,make_env_def,empty_env_def,APPLY_UPDATE_THM] 1081 \\ rw [] \\ EVAL_TAC \\ fs []) 1082 \\ rw[] \\ fs [] \\ rw [] \\ rename [���SUC (LENGTH ws)���] 1083 \\ Cases_on ���ws��� \\ fs [] 1084 THEN1 1085 (rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1086 \\ fs [c_pushes_def] \\ rw [] \\ fs [flatten_def] 1087 \\ qexists_tac ���[Word h'''; Word h''; Word h'; Word h]��� \\ fs [] 1088 \\ fs [code_in_def,pops_regs_def,ZIP_def,write_regs_def] 1089 \\ ho_match_mp_tac IMP_steps_alt 1090 \\ ntac 3 (ho_match_mp_tac IMP_step \\ fs [] 1091 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1092 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN] 1093 \\ fs [GSYM PULL_EXISTS]) 1094 \\ ho_match_mp_tac IMP_start \\ fs [] 1095 \\ qmatch_goalsub_abbrev_tac ���State t1��� 1096 \\ qexists_tac ���t1��� 1097 \\ fs [Abbr���t1���,has_stack_def,APPLY_UPDATE_THM] 1098 \\ fs [state_rel_def,APPLY_UPDATE_THM] 1099 \\ fs [env_ok_def,make_env_def,empty_env_def,APPLY_UPDATE_THM] 1100 \\ rw [] \\ EVAL_TAC \\ fs []) 1101 \\ rw[] \\ fs [] \\ rw [] \\ rename [���SUC (LENGTH ws)���] 1102 \\ Cases_on ���ws��� \\ fs [] 1103 THEN1 1104 (rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1105 \\ fs [c_pushes_def] \\ rw [] \\ fs [flatten_def] 1106 \\ qexists_tac ���[Word h''''; Word h'''; Word h''; Word h'; Word h]��� \\ fs [] 1107 \\ fs [code_in_def,pops_regs_def,ZIP_def,write_regs_def] 1108 \\ ho_match_mp_tac IMP_steps_alt 1109 \\ ntac 4 (ho_match_mp_tac IMP_step \\ fs [] 1110 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1111 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN] 1112 \\ fs [GSYM PULL_EXISTS]) 1113 \\ ho_match_mp_tac IMP_start \\ fs [] 1114 \\ qmatch_goalsub_abbrev_tac ���State t1��� 1115 \\ qexists_tac ���t1��� 1116 \\ fs [Abbr���t1���,has_stack_def,APPLY_UPDATE_THM] 1117 \\ fs [state_rel_def,APPLY_UPDATE_THM] 1118 \\ fs [env_ok_def,make_env_def,empty_env_def,APPLY_UPDATE_THM] 1119 \\ rw [] \\ EVAL_TAC \\ fs []) 1120 \\ rw [] \\ fs [LENGTH_EQ_NUM_compute] \\ rw [] 1121QED 1122 1123Theorem lookup_thm: 1124 ���fs t pos. ALOOKUP fs t = SOME pos ��� lookup t fs = pos 1125Proof 1126 Induct \\ fs [FORALL_PROD,AllCaseEqs(),lookup_def] \\ rw [] 1127 \\ res_tac \\ fs [] 1128QED 1129 1130Theorem pops_regs: 1131 pops_regs ws regs RAX = regs RAX ��� 1132 pops_regs ws regs R12 = regs R12 ��� 1133 pops_regs ws regs R13 = regs R13 ��� 1134 pops_regs ws regs R14 = regs R14 ��� 1135 pops_regs ws regs R15 = regs R15 1136Proof 1137 fs [pops_regs_def] \\ IF_CASES_TAC \\ fs [] \\ Cases_on ���ws��� \\ fs [] 1138 \\ rpt (rename [���LENGTH tt���] \\ Cases_on ���tt��� \\ fs [ZIP_def] THEN1 EVAL_TAC) 1139QED 1140 1141Theorem c_exp_Call_tail: 1142 ^Call_tail 1143Proof 1144 rw [] \\ fs [eval_def] 1145 \\ Cases_on ���evals env xs s��� \\ fs [] 1146 \\ Cases_on ���q = Err Crash��� \\ fs [] 1147 \\ fs [c_exp_alt] 1148 \\ Cases_on ���c_exps t'.pc vs fs xs��� \\ fs [] 1149 \\ fs [c_call_def] \\ rw [] 1150 \\ fs [flatten_def] 1151 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 1152 \\ once_rewrite_tac [flatten_acc] \\ fs [code_in_def] 1153 \\ strip_tac 1154 \\ first_x_assum drule_all 1155 \\ strip_tac 1156 \\ Cases_on ���outcome��� 1157 \\ rename [���steps (State t',s.clock) (ss,n)���] 1158 \\ reverse (Cases_on ���ss���) \\ fs [] 1159 THEN1 1160 (goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] 1161 \\ fs [AllCaseEqs(),get_env_and_body_def,fail_def,return_def] 1162 \\ rw [] \\ imp_res_tac eval_mono \\ fs [] 1163 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS) 1164 \\ reverse (Cases_on ���q���) \\ fs [] 1165 THEN1 (goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] \\ rw []) 1166 \\ rw [] 1167 \\ Cases_on ���get_env_and_body t a r��� \\ fs [] 1168 \\ reverse (Cases_on ���q���) 1169 THEN1 1170 (fs [] \\ rw [] \\ goal_assum (first_x_assum o mp_then Any mp_tac) 1171 \\ fs [get_env_and_body_def,AllCaseEqs(),fail_def] \\ rw []) 1172 \\ fs [AllCaseEqs()] \\ rw [] 1173 \\ fs [AllCaseEqs(),get_env_and_body_def,fail_def] \\ rw [] 1174 \\ rfs [] 1175 \\ rename [���steps (State t1,s.clock) (State t2,r.clock)���] 1176 \\ ho_match_mp_tac IMP_steps 1177 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1178 \\ rename [���evals env xs s = (Res args,r)���] 1179 \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND] 1180 \\ drule (GEN_ALL c_pops_thm) 1181 \\ imp_res_tac steps_inst \\ fs [] 1182 \\ imp_res_tac c_exp_length \\ fs [] 1183 \\ disch_then drule 1184 \\ ������r15. t2.regs R15 = SOME r15��� by fs [state_rel_def] \\ fs [] 1185 \\ pop_assum kall_tac 1186 \\ disch_then (qspecl_then [���r.clock���,���fs���,���r.funs���] mp_tac) 1187 \\ impl_tac 1188 THEN1 1189 (imp_res_tac LIST_REL_LENGTH 1190 \\ imp_res_tac evals_length \\ fs [] 1191 \\ fs [state_rel_def,ODD_ADD,env_ok_def,EVEN_ODD]) 1192 \\ strip_tac 1193 \\ ho_match_mp_tac IMP_steps 1194 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1195 \\ Cases_on ���outcome��� \\ fs [] 1196 \\ reverse (Cases_on ���q���) \\ fs [] \\ rw [] 1197 THEN1 1198 (ho_match_mp_tac IMP_start \\ fs [] 1199 \\ imp_res_tac eval_mono \\ fs [state_rel_def] \\ rfs []) 1200 \\ ho_match_mp_tac IMP_step \\ fs [] 1201 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1202 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN] 1203 \\ CONV_TAC (RESORT_EXISTS_CONV rev) \\ rfs [] 1204 \\ qexists_tac ���rest��� 1205 \\ qexists_tac ���curr��� \\ fs [] 1206 \\ ���LENGTH vs = LENGTH curr��� by fs [env_ok_def] \\ fs [] 1207 \\ Cases_on ���r.clock��� \\ fs [] 1208 \\ ho_match_mp_tac IMP_step' 1209 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1210 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN, 1211 take_branch_cases,set_pc_def] 1212 \\ fs [env_and_body_def,fail_def,AllCaseEqs()] \\ rw [] 1213 \\ ���code_rel fs r.funs t2.instructions��� by fs [state_rel_def] 1214 \\ fs [code_rel_def] 1215 \\ first_x_assum drule 1216 \\ strip_tac \\ fs [name_of_def] 1217 \\ imp_res_tac lookup_thm \\ fs [] 1218 \\ fs [c_defun_def] 1219 \\ rpt (pairarg_tac \\ fs [flatten_def]) 1220 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 1221 \\ once_rewrite_tac [flatten_acc] 1222 \\ fs [code_in_def] \\ rw [] 1223 \\ qmatch_goalsub_abbrev_tac ���State t3��� 1224 \\ drule c_pushes_thm 1225 \\ ���t1.instructions = t3.instructions��� by fs [Abbr���t3���] \\ fs [] 1226 \\ ���code_in t3.pc (flatten c0 []) t3.instructions��� by fs [Abbr���t3���] 1227 \\ disch_then drule 1228 \\ ���t3.regs = pops_regs ws t2.regs��� by fs [Abbr���t3���] 1229 \\ disch_then drule 1230 \\ ���LIST_REL (v_inv t3) args ws��� by 1231 (first_x_assum (fn th => mp_tac th \\ match_mp_tac LIST_REL_mono) 1232 \\ fs [Abbr���t3���]) 1233 \\ disch_then (first_assum o mp_then Any mp_tac) 1234 \\ ������w'. t3.regs RAX = SOME w'��� by 1235 rfs [has_stack_def,Abbr���t3���,pops_regs] 1236 \\ fs [] 1237 \\ disch_then (qspecl_then [���r���,���n���,���fs���] mp_tac) 1238 \\ impl_tac 1239 THEN1 (imp_res_tac LIST_REL_LENGTH \\ fs [] 1240 \\ fs [state_rel_def,Abbr���t3���,pops_regs] 1241 \\ rfs [has_stack_def] 1242 \\ Cases_on ���ws = []��� \\ fs [] 1243 \\ ������x l. ws = SNOC x l��� by metis_tac [SNOC_CASES] \\ fs []) 1244 \\ strip_tac 1245 \\ ho_match_mp_tac IMP_steps 1246 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [Abbr���t3���] 1247 \\ qpat_x_assum ���t5.pc = _��� (assume_tac o GSYM) \\ fs [] 1248 \\ first_x_assum drule \\ fs [] 1249 \\ disch_then match_mp_tac \\ fs [] 1250 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1251 \\ fs [state_rel_def] 1252QED 1253 1254Theorem c_exp_Call_not_tail: 1255 ^Call_not_tail 1256Proof 1257 rw [] \\ fs [eval_def] 1258 \\ Cases_on ���evals env xs s��� \\ fs [] 1259 \\ Cases_on ���q = Err Crash��� \\ fs [] 1260 \\ fs [c_exp_alt] 1261 \\ Cases_on ���c_exps t'.pc vs fs xs��� \\ fs [] 1262 \\ fs [c_call_def] \\ rw [] 1263 \\ fs [flatten_def] 1264 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 1265 \\ once_rewrite_tac [flatten_acc] \\ fs [code_in_def] 1266 \\ strip_tac 1267 \\ first_x_assum drule_all 1268 \\ strip_tac 1269 \\ Cases_on ���outcome��� 1270 \\ rename [���steps (State t',s.clock) (ss,n)���] 1271 \\ reverse (Cases_on ���ss���) \\ fs [] 1272 THEN1 1273 (goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] 1274 \\ fs [AllCaseEqs(),get_env_and_body_def,fail_def,return_def] 1275 \\ rw [] \\ imp_res_tac eval_mono \\ fs [] 1276 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS) 1277 \\ reverse (Cases_on ���q���) \\ fs [] 1278 THEN1 (goal_assum (first_x_assum o mp_then Any mp_tac) \\ fs [] \\ rw []) 1279 \\ rw [] 1280 \\ Cases_on ���get_env_and_body t a r��� \\ fs [] 1281 \\ reverse (Cases_on ���q���) 1282 THEN1 1283 (fs [] \\ rw [] \\ goal_assum (first_x_assum o mp_then Any mp_tac) 1284 \\ fs [get_env_and_body_def,AllCaseEqs(),fail_def] \\ rw []) 1285 \\ fs [AllCaseEqs()] \\ rw [] 1286 \\ fs [AllCaseEqs(),get_env_and_body_def,fail_def] \\ rw [] 1287 \\ rfs [] 1288 \\ rename [���steps (State t1,s.clock) (State t2,r.clock)���] 1289 \\ ho_match_mp_tac IMP_steps 1290 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1291 \\ rename [���evals env xs s = (Res args,r)���] 1292 \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND] 1293 \\ drule (GEN_ALL c_pops_thm) 1294 \\ imp_res_tac steps_inst \\ fs [] 1295 \\ imp_res_tac c_exp_length \\ fs [] 1296 \\ disch_then drule 1297 \\ ������r15. t2.regs R15 = SOME r15��� by fs [state_rel_def] \\ fs [] 1298 \\ pop_assum kall_tac 1299 \\ disch_then (qspecl_then [���r.clock���,���fs���,���r.funs���] mp_tac) 1300 \\ impl_tac 1301 THEN1 1302 (imp_res_tac LIST_REL_LENGTH 1303 \\ imp_res_tac evals_length \\ fs [] 1304 \\ fs [state_rel_def,ODD_ADD,env_ok_def,EVEN_ODD]) 1305 \\ strip_tac 1306 \\ ho_match_mp_tac IMP_steps 1307 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1308 \\ Cases_on ���outcome��� \\ fs [] 1309 \\ reverse (Cases_on ���q���) \\ fs [] \\ rw [] 1310 THEN1 1311 (ho_match_mp_tac IMP_start \\ fs [] 1312 \\ imp_res_tac eval_mono \\ fs [state_rel_def] \\ rfs []) 1313 \\ reverse (Cases_on ���EVEN (LENGTH vs)���) \\ fs [align_def,code_in_def] 1314 THEN1 1315 (Cases_on ���r.clock��� \\ fs [] 1316 \\ ho_match_mp_tac IMP_step' \\ fs [] 1317 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1318 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN,set_pc_def] 1319 \\ qmatch_goalsub_abbrev_tac ���State t4��� 1320 \\ fs [env_and_body_def,fail_def,AllCaseEqs()] \\ rw [] 1321 \\ ���code_rel fs r.funs t4.instructions��� by fs [state_rel_def,Abbr���t4���] 1322 \\ fs [code_rel_def] 1323 \\ first_x_assum drule 1324 \\ strip_tac \\ fs [name_of_def] 1325 \\ imp_res_tac lookup_thm \\ fs [] 1326 \\ fs [c_defun_def] 1327 \\ rpt (pairarg_tac \\ fs [flatten_def]) 1328 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 1329 \\ once_rewrite_tac [flatten_acc] 1330 \\ fs [code_in_def] \\ rw [] 1331 \\ drule c_pushes_thm 1332 \\ ���t1.instructions = t4.instructions��� by fs [Abbr���t4���] \\ fs [] 1333 \\ ���code_in t4.pc (flatten c0 []) t4.instructions��� by fs [Abbr���t4���] 1334 \\ disch_then drule 1335 \\ ���t4.regs = pops_regs ws t2.regs��� by fs [Abbr���t4���] 1336 \\ disch_then drule 1337 \\ ���LIST_REL (v_inv t4) args ws��� by 1338 (first_x_assum (fn th => mp_tac th \\ match_mp_tac LIST_REL_mono) 1339 \\ fs [Abbr���t4���]) 1340 \\ disch_then (first_assum o mp_then Any mp_tac) 1341 \\ ������w'. t4.regs RAX = SOME w'��� by 1342 rfs [has_stack_def,Abbr���t4���,pops_regs] 1343 \\ fs [] 1344 \\ disch_then (qspecl_then [���r���,���n���,���fs���] mp_tac) 1345 \\ impl_tac 1346 THEN1 (imp_res_tac LIST_REL_LENGTH \\ fs [] 1347 \\ fs [state_rel_def,Abbr���t4���,pops_regs] 1348 \\ rfs [has_stack_def] 1349 \\ Cases_on ���ws = []��� \\ fs [] 1350 \\ ������x l. ws = SNOC x l��� by metis_tac [SNOC_CASES] \\ fs []) 1351 \\ strip_tac 1352 \\ ho_match_mp_tac IMP_steps 1353 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [Abbr���t4���] 1354 \\ qpat_x_assum ���t5.pc = _��� (assume_tac o GSYM) \\ fs [] 1355 \\ first_x_assum drule \\ fs [] 1356 \\ disch_then (first_assum o mp_then (Pos (el 3)) mp_tac) 1357 \\ impl_tac 1358 THEN1 (rfs [ODD,ODD_ADD,EVEN_ODD,env_ok_def] \\ fs [state_rel_def]) 1359 \\ strip_tac \\ PairCases_on���outcome��� 1360 \\ reverse (Cases_on ���outcome0���) \\ fs [] \\ rw [] 1361 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 1362 \\ reverse (Cases_on ���res���) \\ fs [] 1363 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 1364 \\ ho_match_mp_tac IMP_steps 1365 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1366 \\ step_tac 1367 \\ fs [PULL_EXISTS,has_stack_def] 1368 \\ qpat_x_assum ���_ = _.stack��� (assume_tac o GSYM) \\ fs [] 1369 \\ ho_match_mp_tac IMP_start \\ fs [] 1370 \\ fs [state_rel_def]) 1371 THEN1 1372 (Cases_on ���r.clock��� \\ fs [] 1373 \\ ho_match_mp_tac IMP_step \\ fs [] 1374 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1375 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM, 1376 EVEN,set_pc_def,fetch_def,pops_regs] 1377 \\ ������rax. t2.regs RAX = SOME rax��� by fs [has_stack_def] \\ fs [] 1378 \\ pop_assum kall_tac 1379 \\ ho_match_mp_tac IMP_step' \\ fs [] 1380 \\ once_rewrite_tac [step_cases] \\ fs [fetch_def,PULL_EXISTS] 1381 \\ fs [write_reg_def,set_stack_def,inc_def,APPLY_UPDATE_THM,EVEN,set_pc_def] 1382 \\ qmatch_goalsub_abbrev_tac ���State t4��� 1383 \\ fs [env_and_body_def,fail_def,AllCaseEqs()] \\ rw [] 1384 \\ ���code_rel fs r.funs t4.instructions��� by fs [state_rel_def,Abbr���t4���] 1385 \\ fs [code_rel_def] 1386 \\ first_x_assum drule 1387 \\ strip_tac \\ fs [name_of_def] 1388 \\ imp_res_tac lookup_thm \\ fs [] 1389 \\ fs [c_defun_def] 1390 \\ rpt (pairarg_tac \\ fs [flatten_def]) 1391 \\ qpat_x_assum ���code_in _ _ _��� mp_tac 1392 \\ once_rewrite_tac [flatten_acc] 1393 \\ fs [code_in_def] \\ rw [] 1394 \\ drule c_pushes_thm 1395 \\ ���t1.instructions = t4.instructions��� by fs [Abbr���t4���] \\ fs [] 1396 \\ ���code_in t4.pc (flatten c0 []) t4.instructions��� by fs [Abbr���t4���] 1397 \\ disch_then drule 1398 \\ ���t4.regs = pops_regs ws t2.regs��� by fs [Abbr���t4���] 1399 \\ disch_then drule 1400 \\ ���LIST_REL (v_inv t4) args ws��� by 1401 (first_x_assum (fn th => mp_tac th \\ match_mp_tac LIST_REL_mono) 1402 \\ fs [Abbr���t4���]) 1403 \\ disch_then (first_assum o mp_then Any mp_tac) 1404 \\ ������w'. t4.regs RAX = SOME w'��� by 1405 rfs [has_stack_def,Abbr���t4���,pops_regs] 1406 \\ fs [] 1407 \\ disch_then (qspecl_then [���r���,���n���,���fs���] mp_tac) 1408 \\ impl_tac 1409 THEN1 (imp_res_tac LIST_REL_LENGTH \\ fs [] 1410 \\ fs [state_rel_def,Abbr���t4���,pops_regs] 1411 \\ rfs [has_stack_def] 1412 \\ Cases_on ���ws = []��� \\ fs [] 1413 \\ ������x l. ws = SNOC x l��� by metis_tac [SNOC_CASES] \\ fs []) 1414 \\ strip_tac 1415 \\ ho_match_mp_tac IMP_steps 1416 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [Abbr���t4���] 1417 \\ qpat_x_assum ���t5.pc = _��� (assume_tac o GSYM) \\ fs [] 1418 \\ first_x_assum drule \\ fs [] 1419 \\ disch_then (first_assum o mp_then (Pos (el 3)) mp_tac) 1420 \\ impl_tac 1421 THEN1 (rfs [ODD,ODD_ADD,EVEN_ODD,env_ok_def] \\ fs [state_rel_def]) 1422 \\ strip_tac \\ PairCases_on���outcome��� 1423 \\ reverse (Cases_on ���outcome0���) \\ fs [] \\ rw [] 1424 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 1425 \\ reverse (Cases_on ���res���) \\ fs [] 1426 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 1427 \\ ho_match_mp_tac IMP_steps 1428 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1429 \\ step_tac 1430 \\ fs [PULL_EXISTS,has_stack_def] 1431 \\ qpat_x_assum ���_ = _.stack��� (assume_tac o GSYM) \\ fs [] 1432 \\ imp_res_tac steps_inst \\ fs [] 1433 \\ step_tac 1434 \\ ho_match_mp_tac IMP_start \\ fs [] 1435 \\ fs [state_rel_def,APPLY_UPDATE_THM]) 1436QED 1437 1438Theorem c_exp_Call: 1439 ^(get_goal "eval _ (Call _ _)") 1440Proof 1441 Call_init_tac \\ rewrite_tac [c_exp_Call_tail,c_exp_Call_not_tail] 1442QED 1443 1444Theorem c_exps_nil: 1445 ^(get_goal "evals _ []") 1446Proof 1447 fs [eval_def,c_exp_alt] \\ rw [] 1448 \\ qexists_tac ���State t, s.clock��� \\ fs [] 1449 \\ simp [Once steps_cases] 1450QED 1451 1452Theorem c_exps_cons: 1453 ^(get_goal "evals _ (_::_)") 1454Proof 1455 fs [eval_def,c_exp_alt] \\ rw [] 1456 \\ rpt (pairarg_tac \\ fs []) 1457 \\ rpt var_eq_tac 1458 \\ Cases_on ���eval env x s��� \\ fs [] 1459 \\ Cases_on ���q = Err Crash��� \\ fs [] 1460 \\ first_x_assum drule \\ fs [] 1461 \\ rpt (disch_then drule) 1462 \\ impl_tac THEN1 1463 (qpat_x_assum ���code_in _ _ _��� mp_tac 1464 \\ fs [flatten_def] \\ simp [Once flatten_acc]) 1465 \\ strip_tac 1466 \\ Cases_on ���outcome��� 1467 \\ rename [���steps _ (r1,r2)���] 1468 \\ reverse (Cases_on ���r1���) \\ fs [] 1469 THEN1 1470 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1471 \\ fs [AllCaseEqs()] \\ rw [] 1472 \\ imp_res_tac eval_mono 1473 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS) 1474 \\ reverse (Cases_on ���q���) \\ fs [] 1475 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] \\ rw []) 1476 \\ Cases_on ���evals env xs r��� \\ fs [] 1477 \\ Cases_on ���q = Err Crash��� \\ fs [] \\ rw [] 1478 \\ first_x_assum drule \\ fs [] 1479 \\ disch_then (qspecl_then [���Word w :: curr���,���rest���] mp_tac) 1480 \\ impl_tac THEN1 1481 (qpat_x_assum ���code_in _ _ _��� mp_tac 1482 \\ fs [flatten_def] \\ simp [Once flatten_acc] 1483 \\ imp_res_tac c_exp_length \\ fs [] 1484 \\ imp_res_tac steps_inst \\ fs [] \\ rw [] 1485 \\ fs [env_ok_def] \\ rw [] 1486 \\ first_x_assum drule 1487 \\ rw [] \\ fs [find_def] 1488 \\ once_rewrite_tac [find_acc] \\ fs [ADD1] 1489 \\ fs [GSYM ADD1] 1490 \\ imp_res_tac steps_v_inv \\ fs []) 1491 \\ strip_tac 1492 \\ qexists_tac ���outcome��� 1493 \\ conj_tac THEN1 (Cases_on ���outcome��� \\ imp_res_tac steps_rules \\ fs []) 1494 \\ Cases_on ���outcome��� 1495 \\ fs [AllCaseEqs()] \\ rw [] 1496 \\ Cases_on ���q'��� \\ fs [] 1497 \\ imp_res_tac eval_mono 1498 \\ imp_res_tac rich_listTheory.IS_PREFIX_TRANS \\ fs [PULL_EXISTS] 1499 \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND] 1500 \\ rpt (goal_assum (first_assum o mp_then Any mp_tac)) 1501 \\ imp_res_tac steps_v_inv \\ fs [] 1502QED 1503 1504 1505(* putting all the cases together *) 1506 1507Theorem c_exp_correct: 1508 ^(compile_correct_tm()) 1509Proof 1510 match_mp_tac (the_ind_thm()) 1511 \\ EVERY (map strip_assume_tac [c_exp_Const, c_exp_Var, 1512 c_exp_Op, c_exp_If, c_exp_Let, c_exp_Call, c_exps_nil, c_exps_cons]) 1513 \\ asm_rewrite_tac [] 1514QED 1515 1516Theorem c_exp_Evals: 1517 (env,[x],s) ---> ([v],s1) ��� 1518 c_exp is_tail t.pc vs fs x = (code,l1) ��� state_rel fs s t ��� 1519 env_ok env vs curr t ��� has_stack t (curr ��� rest) ��� 1520 ODD (LENGTH rest) ��� code_in t.pc (flatten code []) t.instructions ��� 1521 ���outcome. 1522 RTC step (State t) outcome ��� 1523 case outcome of 1524 | (Halt ec output) => output ��� s1.output ��� ec = 1w 1525 | (State t1) => 1526 state_rel fs s1 t1 ��� 1527 ���w. v_inv t1 v w ��� 1528 if is_tail then 1529 has_stack t1 (Word w::rest) ��� fetch t1 = SOME Ret 1530 else 1531 has_stack t1 (Word w::curr ++ rest) ��� t1.pc = l1 1532Proof 1533 rw [] \\ drule Eval_imp_evals \\ strip_tac 1534 \\ fs [eval_def,AllCaseEqs()] 1535 \\ drule (CONJUNCT1 c_exp_correct) \\ fs [] 1536 \\ disch_then drule \\ fs [] 1537 \\ disch_then (qspecl_then [���curr���,���rest���] mp_tac) 1538 \\ impl_tac THEN1 fs [state_rel_def] 1539 \\ strip_tac 1540 \\ PairCases_on ���outcome��� \\ fs [] 1541 \\ qexists_tac ���outcome0��� \\ fs [] 1542 \\ imp_res_tac steps_imp_RTC_step \\ fs [] 1543 \\ TOP_CASE_TAC \\ fs [] \\ qexists_tac ���w��� \\ fs [] 1544 \\ TOP_CASE_TAC \\ fs [] 1545QED 1546 1547(* compilation of enitre program *) 1548 1549Triviality FST_SND: 1550 FST = (��(x,y). x) ��� SND = (��(x,y). y) 1551Proof 1552 fs [FUN_EQ_THM,FORALL_PROD] 1553QED 1554 1555Theorem c_decs_append: 1556 ���xs ys l fs fs' l' c. 1557 c_decs l fs (xs ++ ys) = (c,fs',l') ��� 1558 let (c1,fs1,l1) = c_decs l fs xs in 1559 let (c2,fs2,l2) = c_decs l1 fs ys in 1560 l' = l2 ��� 1561 fs' = fs1 ++ fs2 ��� 1562 flatten c [] = flatten (Append c1 c2) [] 1563Proof 1564 Induct \\ fs [c_decs_def] 1565 THEN1 fs [flatten_def] 1566 \\ rw [] \\ fs [FST_SND] \\ fs [] 1567 \\ rpt (pairarg_tac \\ fs []) 1568 \\ rpt var_eq_tac \\ fs [] 1569 \\ first_x_assum drule 1570 \\ fs [] \\ strip_tac 1571 \\ rpt var_eq_tac \\ fs [] 1572 \\ fs [flatten_def] 1573QED 1574 1575Theorem c_exp_11: 1576 (���t l vs fs1 e fs2 c1 l1 c2 l2. 1577 c_exp t l vs fs1 e = (c1,l1) ��� 1578 c_exp t l vs fs2 e = (c2,l2) ��� l1 = l2) ��� 1579 (���l vs fs1 e fs2 c1 l1 c2 l2. 1580 c_exps l vs fs1 e = (c1,l1) ��� 1581 c_exps l vs fs2 e = (c2,l2) ��� l1 = l2) 1582Proof 1583 ho_match_mp_tac c_exp_ind_alt \\ rw [] 1584 \\ fs [c_exp_alt,c_if_def,c_call_def,make_ret_def] 1585 \\ rpt (pairarg_tac \\ fs []) \\ fs [make_ret_def] 1586 \\ rpt var_eq_tac \\ fs [] 1587 \\ res_tac \\ fs [] 1588 \\ rpt (pairarg_tac \\ fs []) \\ fs [make_ret_def] 1589 \\ rpt var_eq_tac \\ fs [] 1590 \\ res_tac \\ fs [] 1591 \\ rpt (pairarg_tac \\ fs []) \\ fs [make_ret_def] 1592 \\ rpt var_eq_tac \\ fs [] 1593 \\ res_tac \\ fs [] 1594 THEN1 1595 (Cases_on ���c_exps l vs fs1 e��� \\ Cases_on ���c_exps l vs fs2 e��� \\ fs [] 1596 \\ res_tac \\ fs [] \\ fs [c_call_def,AllCaseEqs()] 1597 \\ rpt var_eq_tac \\ fs [] 1598 \\ res_tac \\ fs [align_def] \\ rw [] \\ fs []) 1599 \\ first_assum (qspec_then ���fs1��� mp_tac) \\ fs [] 1600 \\ first_x_assum (qspec_then ���fs2��� mp_tac) \\ fs [] 1601QED 1602 1603Theorem c_defun_length_11: 1604 c_defun l fs1 d = (c1,l1) ��� c_defun l fs2 d = (c2,l2) ��� l1 = l2 1605Proof 1606 Cases_on ���d��� \\ fs [c_defun_def] \\ rw [] 1607 \\ rpt (pairarg_tac \\ fs []) \\ fs [] 1608 \\ rpt var_eq_tac \\ fs [] 1609 \\ imp_res_tac c_exp_11 \\ fs [] 1610QED 1611 1612Theorem c_decs_length_11: 1613 ���l fs1 fs2 ds c1 c2 fs'1 l1 fs'2 l2. 1614 c_decs l fs1 ds = (c1,fs'1,l1) ��� 1615 c_decs l fs2 ds = (c2,fs'2,l2) ��� 1616 l1 = l2 ��� fs'1 = fs'2 1617Proof 1618 Induct_on ���ds��� \\ fs [c_decs_def] 1619 \\ rpt gen_tac \\ strip_tac 1620 \\ qabbrev_tac ���p1 = c_defun (l + 1) fs1 h��� 1621 \\ qabbrev_tac ���p2 = c_defun (l + 1) fs2 h��� 1622 \\ qabbrev_tac ���q1 = c_decs (SND p1) fs1 ds��� 1623 \\ qabbrev_tac ���q2 = c_decs (SND p2) fs2 ds��� 1624 \\ PairCases_on ���p1��� \\ PairCases_on ���p2��� \\ fs [] 1625 \\ PairCases_on ���q1��� \\ PairCases_on ���q2��� \\ fs [] 1626 \\ fs [markerTheory.Abbrev_def] 1627 \\ metis_tac [c_defun_length_11] 1628QED 1629 1630Theorem c_defun_length: 1631 c_defun l fs d = (c1,l1) ��� l1 = LENGTH (flatten c1 []) + l 1632Proof 1633 Cases_on ���d��� \\ fs [c_defun_def] 1634 \\ rpt (pairarg_tac \\ fs []) \\ rw [] 1635 \\ fs [flatten_def] \\ once_rewrite_tac [flatten_acc] \\ fs [] 1636 \\ imp_res_tac c_exp_length \\ fs [] \\ rw [] 1637 \\ fs [c_pushes_def,AllCaseEqs()] 1638 \\ rw [] \\ fs [flatten_def] 1639QED 1640 1641Theorem c_decs_length: 1642 ���ds l fs c1 fs1 l1. 1643 c_decs l fs ds = (c1,fs1,l1) ��� l1 = LENGTH (flatten c1 []) + l 1644Proof 1645 Induct \\ fs [c_decs_def] \\ fs [flatten_def] \\ rw [] 1646 \\ Cases_on ���c_defun (l + 1) fs h��� \\ fs [] 1647 \\ Cases_on ���c_decs r fs ds��� \\ fs [] \\ PairCases_on ���r'��� \\ fs [] 1648 \\ res_tac \\ fs [] 1649 \\ imp_res_tac c_defun_length \\ rw [] \\ fs [flatten_def] 1650 \\ once_rewrite_tac [flatten_acc] \\ fs [] 1651QED 1652 1653Theorem lookup_LENGTH: 1654 ���xs h ys. lookup (LENGTH xs) (xs ��� h::ys) = SOME h 1655Proof 1656 Induct \\ fs [x64asm_semanticsTheory.lookup_def] 1657QED 1658 1659Theorem IMP_code_in_append: 1660 ���xs ys k. k = LENGTH xs ��� code_in k ys (xs ++ ys) 1661Proof 1662 Induct_on ���ys��� \\ fs [code_in_def,lookup_LENGTH] \\ rw [] 1663 \\ first_x_assum (qspec_then ���xs ++ [h]��� mp_tac) 1664 \\ fs [] \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND] \\ fs [] 1665QED 1666 1667Theorem IMP_code_in_append2: 1668 ���xs ys zs k. k = LENGTH xs ��� code_in k ys (xs ++ ys ++ zs) 1669Proof 1670 Induct_on ���ys��� \\ fs [code_in_def,lookup_LENGTH] \\ rw [] 1671 \\ first_x_assum (qspec_then ���xs ++ [h]��� mp_tac) 1672 \\ fs [] \\ full_simp_tac std_ss [GSYM APPEND_ASSOC,APPEND] 1673 \\ fs [lookup_LENGTH] 1674QED 1675 1676Theorem c_decs_code_in: 1677 ���ds l fs0 fs c1 k n params body xs acc. 1678 c_decs l fs0 ds = (c1,fs,k) ��� 1679 lookup_fun n ds = SOME (params,body) ��� 1680 LENGTH xs = l ��� 1681 ���pos. 1682 ALOOKUP fs n = SOME pos ��� 1683 code_in pos (flatten (FST (c_defun pos fs0 (Defun n params body))) []) 1684 (xs ��� flatten c1 acc) 1685Proof 1686 Induct \\ fs [c_decs_def,lookup_fun_def] \\ rw [] 1687 \\ Cases_on ���c_defun (LENGTH xs + 1) fs0 h��� \\ fs [] 1688 \\ Cases_on ���c_decs r fs0 ds��� \\ fs [] 1689 \\ rpt var_eq_tac 1690 \\ Cases_on ���h��� \\ fs [] 1691 \\ fs [lookup_fun_def,name_of_def] 1692 \\ rw [] 1693 \\ rw [] \\ imp_res_tac c_defun_length \\ fs [] \\ rw [] 1694 \\ fs [flatten_def] 1695 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def,code_in_def] 1696 \\ once_rewrite_tac [flatten_acc] \\ fs [flatten_def,code_in_def] 1697 THEN1 1698 (rename [���xs ++ x::(ys ++ zs ++ acc)���] 1699 \\ ���xs ��� x::(ys ��� zs ++ acc) = (xs ��� [x]) ++ ys ��� (zs ++ acc)��� by fs [] 1700 \\ asm_rewrite_tac [] 1701 \\ match_mp_tac IMP_code_in_append2 \\ fs []) 1702 \\ qmatch_asmsub_abbrev_tac ���c_decs pos1��� \\ rfs [] 1703 \\ rename [���xs ++ x::(ys ++ _ ++ acc)���] 1704 \\ ���xs ��� x::(ys ��� flatten q' [] ��� acc) = (xs ��� x::ys) ��� flatten q' acc��� 1705 by fs [GSYM flatten_acc] 1706 \\ asm_rewrite_tac [] 1707 \\ first_x_assum match_mp_tac \\ fs [] 1708 \\ unabbrev_all_tac \\ fs [ADD1] 1709 \\ Cases_on ���r'��� \\ fs [] 1710QED 1711 1712Theorem codegen_thm: 1713 eval empty_env main s = (res,s1) ��� res ��� Err Crash ��� 1714 s.funs = funs ��� 1715 t.pc = 0 ��� 1716 t.instructions = codegen (Program funs main) ��� 1717 t.stack = [] ��� 1718 t.input = s.input ��� 1719 t.output = s.output ��� 1720 t.regs R14 = SOME r14 ��� 1721 t.regs R15 = SOME r15 ��� 1722 memory_writable r14 r15 t.memory ��� 1723 ���outcome. 1724 steps (State t,s.clock) outcome ��� 1725 case outcome of 1726 | (State t1,ck) => t1.output = s1.output ��� ck = s1.clock ��� res = Err TimeOut 1727 | (Halt ec output,ck) => if ec ��� 0w then output ��� s1.output 1728 else output = s1.output ��� ���v. res = Res v 1729Proof 1730 rw [] \\ fs [codegen_def] 1731 \\ rpt (pairarg_tac \\ fs []) 1732 \\ qpat_x_assum ���t.instructions = _��� mp_tac 1733 \\ simp [flatten_def] \\ once_rewrite_tac [flatten_acc] \\ fs [] 1734 \\ rw [] \\ fs [] 1735 \\ ntac 4 (ho_match_mp_tac IMP_step \\ fs [] 1736 \\ once_rewrite_tac [step_cases] 1737 \\ simp [fetch_def,init_def,x64asm_semanticsTheory.lookup_def] 1738 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM, 1739 set_pc_def,set_stack_def,LENGTH_EQ_NUM_compute]) 1740 \\ qmatch_goalsub_abbrev_tac ���State t2��� 1741 \\ ���code_in t2.pc (flatten (FST (c_defun t2.pc fs (Defun (name "main") [] main))) []) 1742 t.instructions��� by 1743 (drule c_decs_append \\ fs [] 1744 \\ rpt (pairarg_tac \\ fs []) \\ rw [] \\ fs [c_decs_def] 1745 \\ imp_res_tac c_decs_length_11 \\ rpt var_eq_tac 1746 \\ qmatch_goalsub_abbrev_tac ���FST ff��� 1747 \\ ���t2.pc = k + 1��� by fs [Abbr���t2���] \\ fs [] 1748 \\ PairCases_on ���ff��� \\ fs [] \\ rpt var_eq_tac 1749 \\ qmatch_asmsub_abbrev_tac ���Comment com��� \\ fs [flatten_def] 1750 \\ once_rewrite_tac [flatten_acc] \\ fs [code_in_def] 1751 \\ imp_res_tac c_decs_length \\ fs [] 1752 \\ qmatch_goalsub_abbrev_tac ���init kk ++ flatten c1 [] ++ cc::_��� 1753 \\ ���init kk ��� flatten c1 [] ��� cc::flatten ff0 [] = 1754 (init kk ��� flatten c1 [] ��� [cc]) ++ flatten ff0 []��� by fs [] 1755 \\ pop_assum (asm_rewrite_tac o single) 1756 \\ match_mp_tac IMP_code_in_append 1757 \\ fs [Abbr���kk���] \\ EVAL_TAC) 1758 \\ fs [c_defun_def] 1759 \\ rpt (pairarg_tac \\ fs []) 1760 \\ fs [c_pushes_def] \\ rw [] 1761 \\ fs [flatten_def] 1762 \\ drule (c_exp_correct |> CONJUNCT1) \\ fs [] 1763 \\ disch_then drule 1764 \\ disch_then (qspecl_then [���[Word 0w]���,���[RetAddr 4]���] mp_tac) 1765 \\ impl_tac THEN1 1766 (fs [has_stack_def,Abbr���t2���] \\ rfs [APPLY_UPDATE_THM] 1767 \\ fs [env_ok_def,empty_env_def,state_rel_def,APPLY_UPDATE_THM] 1768 \\ fs [code_rel_def,init_code_in_def] 1769 \\ conj_tac THEN1 (qexists_tac ���k+1��� \\ fs [] \\ EVAL_TAC) 1770 \\ imp_res_tac c_decs_append \\ rfs [] 1771 \\ rpt (pairarg_tac \\ fs []) 1772 \\ imp_res_tac c_decs_length_11 \\ rpt var_eq_tac 1773 \\ pop_assum kall_tac \\ rw [] 1774 \\ ���LENGTH (init (k+1)) = LENGTH (init 0)��� by EVAL_TAC 1775 \\ drule_all c_decs_code_in \\ fs [flatten_def]) 1776 \\ strip_tac 1777 \\ PairCases_on ���outcome��� \\ reverse (Cases_on ���outcome0���) \\ fs [] 1778 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) \\ fs []) 1779 \\ reverse (Cases_on ���res���) \\ fs [] 1780 THEN1 (goal_assum (first_assum o mp_then Any mp_tac) 1781 \\ fs [state_rel_def] \\ Cases_on ���e��� \\ fs []) 1782 \\ ho_match_mp_tac IMP_steps \\ fs [] 1783 \\ goal_assum (first_assum o mp_then Any mp_tac) 1784 \\ fs [fetch_def,has_stack_def] 1785 \\ ho_match_mp_tac IMP_step \\ fs [] 1786 \\ once_rewrite_tac [step_cases] 1787 \\ simp [fetch_def,init_def,x64asm_semanticsTheory.lookup_def] 1788 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM, 1789 set_pc_def,set_stack_def,LENGTH_EQ_NUM_compute,PULL_EXISTS] 1790 \\ imp_res_tac steps_inst \\ fs [Abbr���t2���] 1791 \\ ntac 2 (ho_match_mp_tac IMP_step \\ fs [] 1792 \\ once_rewrite_tac [step_cases] 1793 \\ simp [fetch_def,init_def,x64asm_semanticsTheory.lookup_def] 1794 \\ fs [write_reg_def,inc_def,APPLY_UPDATE_THM, 1795 set_pc_def,set_stack_def,LENGTH_EQ_NUM_compute]) 1796 \\ ho_match_mp_tac IMP_start \\ fs [] 1797 \\ fs [state_rel_def] 1798QED 1799 1800Theorem codegen_terminates: 1801 (input, prog) prog_terminates output1 ��� 1802 (input, codegen prog) asm_terminates output2 ��� 1803 output1 = output2 1804Proof 1805 Cases_on ���prog��� 1806 \\ rw [prog_terminates_def,asm_terminates_def,Eval_eq_evals,init_state_ok_def] 1807 \\ fs [eval_def,AllCaseEqs()] 1808 \\ drule codegen_thm \\ fs [] 1809 \\ disch_then drule \\ fs [] 1810 \\ fs [init_state_def] \\ rw [] 1811 \\ PairCases_on ���outcome��� \\ fs [] 1812 \\ Cases_on ���outcome0��� \\ fs [] 1813 \\ imp_res_tac steps_imp_RTC_step \\ fs [] 1814 \\ imp_res_tac RTC_step_determ \\ fs [] 1815QED 1816 1817Theorem codegen_diverges: 1818 prog_avoids_crash input prog ��� 1819 (input, codegen prog) asm_diverges output ��� 1820 (input, prog) prog_diverges output 1821Proof 1822 rw [prog_avoids_crash_def,asm_diverges_def,prog_diverges_def,init_state_ok_def] 1823 THEN1 1824 (CCONTR_TAC \\ fs [prog_timesout_def] 1825 \\ last_x_assum (qspec_then ���k��� assume_tac) 1826 \\ Cases_on ���eval_from k t.input prog��� \\ fs [] 1827 \\ reverse (Cases_on ���q���) 1828 THEN1 (Cases_on ���e��� \\ fs [] \\ rw [] \\ fs []) \\ fs [] 1829 \\ rw [] \\ Cases_on ���prog��� \\ fs [eval_from_def] 1830 \\ drule codegen_thm \\ fs [] 1831 \\ fs [init_state_def] 1832 \\ goal_assum (first_assum o mp_then Any mp_tac) \\ fs [] 1833 \\ CCONTR_TAC \\ fs [] 1834 \\ Cases_on ���outcome��� \\ fs [] 1835 \\ Cases_on ���q��� \\ fs [] 1836 \\ drule steps_IMP_NRC_step \\ strip_tac 1837 \\ rename [���NRC _ kk���] 1838 \\ first_x_assum (qspec_then ���kk��� mp_tac) \\ strip_tac 1839 \\ imp_res_tac NRC_step_determ \\ fs []) 1840 \\ match_mp_tac IMP_build_lprefix_lub_EQ 1841 \\ rewrite_tac [lprefix_chain_step] 1842 \\ conj_asm1_tac THEN1 1843 (unabbrev_all_tac 1844 \\ fs [lprefix_chain_def,prog_output_def,PULL_EXISTS] 1845 \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) 1846 \\ fs [llistTheory.LPREFIX_fromList,llistTheory.from_toList] 1847 \\ rpt gen_tac 1848 \\ ���k ��� k' ��� k' ��� k��� by fs [] 1849 \\ Cases_on ���eval_from k t.input prog��� \\ fs [] 1850 \\ Cases_on ���eval_from k' t.input prog��� \\ fs [] 1851 \\ imp_res_tac eval_from_prefix \\ fs []) 1852 \\ rw [lprefix_rel_def] \\ fs [PULL_EXISTS] 1853 THEN1 1854 (imp_res_tac RTC_NRC \\ rename [���NRC _ kk���] \\ rw [] 1855 \\ qexists_tac ���kk��� \\ last_x_assum (qspec_then ���kk��� assume_tac) 1856 \\ Cases_on ���eval_from kk t.input prog��� \\ fs [] 1857 \\ Cases_on ���prog��� \\ fs [eval_from_def,prog_output_def] 1858 \\ drule codegen_thm \\ fs [] 1859 \\ disch_then drule \\ fs [] 1860 \\ fs [init_state_def] \\ rw [] 1861 \\ PairCases_on ���outcome��� \\ fs [] 1862 \\ Cases_on ���outcome0��� \\ fs [] 1863 THEN1 1864 (imp_res_tac eval_TimeOut_clock \\ rw [] \\ fs [] 1865 \\ imp_res_tac asm_output_PREFIX 1866 \\ rfs [LPREFIX_fromList,from_toList]) 1867 \\ drule steps_IMP_NRC_step \\ strip_tac 1868 \\ rename [���NRC _ kk���] 1869 \\ first_x_assum (qspec_then ���kk��� mp_tac) \\ strip_tac 1870 \\ imp_res_tac NRC_step_determ \\ fs []) 1871 \\ last_x_assum (qspec_then ���k��� assume_tac) 1872 \\ Cases_on ���eval_from k t.input prog��� \\ fs [LNTH_fromList] \\ rw [] 1873 \\ Cases_on ���prog��� \\ fs [eval_from_def,prog_output_def] 1874 \\ drule codegen_thm \\ fs [] 1875 \\ disch_then drule \\ fs [] 1876 \\ fs [init_state_def] \\ rw [] 1877 \\ PairCases_on ���outcome��� \\ fs [] 1878 \\ Cases_on ���outcome0��� \\ fs [] 1879 THEN1 1880 (rw [] \\ qexists_tac ���s��� \\ fs [] 1881 \\ drule steps_IMP_NRC_step \\ strip_tac 1882 \\ imp_res_tac NRC_RTC) 1883 \\ drule steps_IMP_NRC_step \\ strip_tac 1884 \\ rename [���NRC _ kk���] 1885 \\ first_x_assum (qspec_then ���kk��� mp_tac) \\ strip_tac 1886 \\ imp_res_tac NRC_step_determ \\ fs [] 1887QED 1888 1889val _ = export_theory(); 1890