1open HolKernel Parse boolLib bossLib BasicProvers; 2 3val _ = new_theory "for_compile"; 4 5(* 6 7This file proves correctness of a compiler for the FOR language 8defined in forScript.sml. The compiler targets a simple assembly-like 9language. We prove that the compiler preserves the top-level 10observable semantics. 11 12The compiler consists of three phasees: 13 - the first phase simplifies For loops and removes Dec 14 - the second phase compiles expressions into very simple assignments 15 - the third phase maps the FOR language into assmembly code 16 17*) 18 19open optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory; 20open forTheory listTheory arithmeticTheory; 21 22val _ = temp_tight_equality (); 23 24 25(* === PHASE 1 : simplifies For loops and removes Dec === *) 26 27val Loop_def = Define ` 28 Loop t = For (Num 1) (Num 1) t`; 29 30val phase1_def = Define ` 31 (phase1 (Exp e) = Exp e) /\ 32 (phase1 (Dec x t) = Seq (Exp (Assign x (Num 0))) (phase1 t)) /\ 33 (phase1 (Break) = Break) /\ 34 (phase1 (Seq t1 t2) = Seq (phase1 t1) (phase1 t2)) /\ 35 (phase1 (If e t1 t2) = If e (phase1 t1) (phase1 t2)) /\ 36 (phase1 (For e1 e2 t) = Loop (If e1 (Seq (phase1 t) (Exp e2)) Break))`; 37 38(* Verification of phase 1 *) 39 40val sem_e_break = store_thm("sem_e_break[simp]", 41 ``!b1 s. ~(sem_e s b1 = (Rbreak,r)) /\ ~(sem_e s b1 = (Rtimeout,r))``, 42 Induct \\ rpt strip_tac 43 \\ fs [sem_e_def] 44 \\ every_case_tac \\ fs [] \\ rfs []); 45 46val phase1_correct = store_thm("phase1_correct", 47 ``!s t. sem_t s (phase1 t) = sem_t s t``, 48 once_rewrite_tac [EQ_SYM_EQ] 49 \\ recInduct sem_t_ind 50 \\ rw [phase1_def,Loop_def] 51 \\ simp [sem_t_def_with_stop,sem_e_def] 52 \\ rpt (BasicProvers.TOP_CASE_TAC \\ simp [sem_t_def_with_stop]) 53 \\ fs [STOP_def]); 54 55val phase1_pres = store_thm("phase1_pres", 56 ``!t. semantics (phase1 t) = semantics t``, 57 fs [semantics_def,phase1_correct]); 58 59(* End of phase 1 verification -- 18 lines *) 60 61(* the rest is old redundant stuff *) 62 63val sem_t_Dec = store_thm("sem_t_Dec", 64 ``sem_t s (Dec v t) = 65 sem_t s (Seq (Exp (Assign v (Num 0))) t)``, 66 fs [sem_t_def,sem_e_def]); 67 68val sem_t_pull_if = prove( 69 ``sem_t s1 (if b then t1 else t2) = 70 (if b then sem_t s1 t1 else sem_t s1 t2)``, 71 SRW_TAC [] []); 72 73val sem_t_eval = save_thm("sem_t_eval", 74 (EVAL THENC REWRITE_CONV [sem_t_pull_if] THENC EVAL) 75 ``sem_t s (If b (Exp (Num 0)) Break)``); 76 77val sem_t_Loop = save_thm("sem_t_Loop", 78 ``sem_t s (Loop t)`` 79 |> (SIMP_CONV (srw_ss()) [Once sem_t_def,sem_e_def,Loop_def] THENC 80 REWRITE_CONV [GSYM Loop_def])); 81 82val sem_t_For_swap_body = prove( 83 ``(!s. sem_t s t1 = sem_t s t2) ==> 84 (sem_t s (For b1 b2 t1) = sem_t s (For b1 b2 t2))``, 85 STRIP_TAC 86 \\ completeInduct_on `s.clock` 87 \\ rw [sem_t_def_with_stop,sem_e_def,Once sem_t_Loop] 88 \\ every_case_tac \\ fs [PULL_FORALL,STOP_def] 89 \\ FIRST_X_ASSUM MATCH_MP_TAC 90 \\ fs [dec_clock_def] 91 \\ imp_res_tac sem_e_clock 92 \\ imp_res_tac sem_t_clock 93 \\ decide_tac); 94 95val sem_t_For = store_thm("sem_t_For", 96 ``!s b1 b2 t. sem_t s (For b1 b2 t) = 97 sem_t s (Loop (If b1 (Seq t (Exp b2)) Break))``, 98 REPEAT STRIP_TAC 99 \\ completeInduct_on `s.clock` 100 \\ rw [sem_t_def_with_stop,sem_e_def,Once sem_t_Loop] 101 \\ Cases_on `sem_e s b1` \\ fs [] 102 \\ Cases_on `q` \\ fs [] 103 \\ SRW_TAC [] [sem_t_def_with_stop] 104 \\ Cases_on `sem_t r t` \\ fs [] 105 \\ Cases_on `q` \\ fs [] 106 \\ Cases_on `sem_e r' b2` \\ fs [] 107 \\ Cases_on `q` \\ fs [] 108 \\ SRW_TAC [] [] 109 \\ fs [sem_e_break] 110 \\ fs [PULL_FORALL,STOP_def] 111 \\ FIRST_X_ASSUM MATCH_MP_TAC 112 \\ fs [dec_clock_def] 113 \\ imp_res_tac sem_e_clock 114 \\ imp_res_tac sem_t_clock 115 \\ decide_tac); 116 117 118(* === PHASE 2 : compiles expressions into very simple assignments === *) 119 120val comp_exp_def = Define ` 121 (comp_exp (Var v) s = Exp (Assign s (Var v))) /\ 122 (comp_exp (Num i) s = Exp (Assign s (Num i))) /\ 123 (comp_exp (Assign v e) s = 124 (Seq (comp_exp e s) (Exp (Assign v (Var s))))) /\ 125 (comp_exp (Add x y) s = 126 (Seq (comp_exp x s) 127 (Seq (comp_exp y (s++"'")) 128 (Exp (Assign s (Add (Var s) (Var (s++"'"))))))))`; 129 130val flatten_t_def = Define ` 131 (flatten_t (Exp e) n = comp_exp e n) /\ 132 (flatten_t (Dec x t) n = t) /\ 133 (flatten_t (Break) n = Break) /\ 134 (flatten_t (Seq t1 t2) n = Seq (flatten_t t1 n) (flatten_t t2 n)) /\ 135 (flatten_t (For e1 e2 t) n = For e1 e2 (flatten_t t n)) /\ 136 (flatten_t (If e t1 t2) n = 137 Seq (comp_exp e n) (If (Var n) (flatten_t t1 n) (flatten_t t2 n)))`; 138 139val MAX_def = Define `MAX n m = if n < m then m else n:num` 140 141val exp_max_def = Define ` 142 (exp_max (Var v) = LENGTH v) /\ 143 (exp_max (Add x y) = MAX (exp_max x) (exp_max y)) /\ 144 (exp_max (Assign v e) = MAX (LENGTH v) (exp_max e)) /\ 145 (exp_max _ = 0)`; 146 147val t_max_def = Define ` 148 (t_max (Exp e) = exp_max e) /\ 149 (t_max (Dec x t) = MAX (LENGTH x) (t_max t)) /\ 150 (t_max (Break) = 0) /\ 151 (t_max (Seq t1 t2) = MAX (t_max t1) (t_max t2)) /\ 152 (t_max (For e1 e2 t) = MAX (exp_max e1) (MAX (exp_max e2) (t_max t))) /\ 153 (t_max (If e t1 t2) = MAX (exp_max e) (MAX (t_max t1) (t_max t2)))`; 154 155val phase2_def = Define ` 156 phase2 t = flatten_t t ("temp" ++ REPLICATE (t_max t - 3) #"'")`; 157 158(* Verification of phase 2 *) 159 160val possible_var_name_def = Define ` 161 possible_var_name v s = !n. ~(v ++ REPLICATE n #"'" IN FDOM s)`; 162 163val possible_var_name_IMP_SUBMAP = prove( 164 ``possible_var_name n s.store /\ s.store SUBMAP t.store ==> 165 s.store SUBMAP t.store |+ (n,i)``, 166 fs [FLOOKUP_DEF,SUBMAP_DEF,FAPPLY_FUPDATE_THM] 167 \\ fs [possible_var_name_def] \\ REPEAT STRIP_TAC 168 \\ SRW_TAC [] [] \\ fs [] 169 \\ METIS_TAC [APPEND_NIL,rich_listTheory.REPLICATE]); 170 171val MAX_LESS = prove( 172 ``MAX n m < k <=> n < k /\ m < k``, 173 SRW_TAC [] [MAX_def] \\ DECIDE_TAC); 174 175val sem_e_possible_var_name = prove( 176 ``!e s i r. 177 (sem_e s e = (Rval i,r)) /\ exp_max e < STRLEN k ==> 178 possible_var_name k s.store ==> 179 possible_var_name k r.store``, 180 Induct \\ fs [sem_e_def] \\ REPEAT STRIP_TAC \\ every_case_tac \\ fs [] 181 THEN1 182 (FIRST_X_ASSUM (MP_TAC o Q.SPEC `r'`) 183 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `s`) 184 \\ fs [exp_max_def,MAX_LESS]) 185 \\ SRW_TAC [] [] \\ fs [exp_max_def,MAX_LESS] 186 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `s'`) \\ fs [] 187 \\ fs [store_var_def,possible_var_name_def] 188 \\ REPEAT STRIP_TAC \\ SRW_TAC [] [] 189 \\ fs [] \\ DECIDE_TAC); 190 191val r_cases_eq = prove_case_eq_thm { 192 case_def = forTheory.r_case_def, 193 nchotomy = forTheory.r_nchotomy 194}; 195 196val pair_cases_eq = Q.prove( 197 ���(pair_CASE p f = v) ��� ���q r. p = (q,r) ��� v = f q r���, 198 Cases_on `p` >> simp[] >> metis_tac[]); 199 200val bool_cases_eq = Q.prove( 201 ���(if p then q else r) = v ��� p /\ q = v ��� ��p ��� r = v���, 202 Cases_on `p` >> simp[]); 203 204val option_cases_eq = Q.prove( 205 ���(option_CASE opt n s = v) ��� 206 opt = NONE ��� n = v ��� ���sv. opt = SOME sv ��� s sv = v���, 207 Cases_on ���opt��� >> simp[]); 208 209val store_var_clock = Q.store_thm( 210 "store_var_clock[simp]", 211 ���(store_var v n s).clock = s.clock���, 212 simp[store_var_def]); 213 214local val fs = fsrw_tac[] in 215val comp_exp_correct = prove( 216 ``!e s t n res s1. 217 sem_e s e = (res,s1) /\ res <> Rfail /\ 218 possible_var_name n s.store /\ 219 s.store SUBMAP t.store /\ (t.clock = s.clock) /\ 220 exp_max e < LENGTH n ==> 221 ?t1. (sem_t t (comp_exp e n) = (res,t1)) /\ 222 s1.store SUBMAP t1.store /\ (t1.clock = s1.clock) /\ 223 (!v. (res = Rval v) ==> FLOOKUP t1.store n = SOME v) /\ 224 possible_var_name n s1.store /\ 225 (!k v. possible_var_name k s.store /\ 226 exp_max e < LENGTH k /\ LENGTH k < LENGTH n /\ 227 FLOOKUP t.store k = SOME v ==> 228 FLOOKUP t1.store k = SOME v)``, 229 Induct 230 >- (rpt gen_tac >> rename [���Var vnm���] >> 231 simp[sem_e_def, comp_exp_def, sem_t_def, option_cases_eq] >> csimp[] >> 232 rpt strip_tac >> rpt BasicProvers.VAR_EQ_TAC >> 233 imp_res_tac FLOOKUP_SUBMAP >> simp[store_var_def] >> 234 imp_res_tac possible_var_name_IMP_SUBMAP >> 235 simp[FLOOKUP_DEF, FAPPLY_FUPDATE_THM] >> rw[]) 236 >- (rpt gen_tac >> rename [���Num n���] >> 237 simp[sem_e_def, comp_exp_def, sem_t_def] >> rw[] >> 238 simp[store_var_def] >> 239 imp_res_tac possible_var_name_IMP_SUBMAP >> 240 simp[FLOOKUP_DEF, FAPPLY_FUPDATE_THM] >> rw[]) 241 >- (rpt gen_tac >> rename [���Add e1 e2���] >> 242 simp[sem_e_def, SimpL ���$==>���, pair_cases_eq, r_cases_eq] >> 243 rpt strip_tac >> fs[] >> 244 rpt BasicProvers.VAR_EQ_TAC >> fs[] >> 245 fs[exp_max_def, MAX_LESS] >> 246 dsimp[sem_t_def, comp_exp_def, pair_cases_eq, r_cases_eq] >> 247 rename [���sem_e s1 e1 = (Rval n1, s2)���, ���sem_e s2 e2 = (Rval n2, s3)���] >> 248 first_x_assum 249 (fn th => 250 mp_then.mp_then (mp_then.Pos hd) mp_tac th 251 (ASSUME ���sem_e s1 e1 = (Rval n1, s2)���)) >> 252 simp[] >> 253 rpt (disch_then (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac))>> 254 disch_then (qx_choose_then ���t1��� strip_assume_tac) >> simp[] >> 255 rename1 ���possible_var_name n s2.store��� >> 256 ���possible_var_name (STRCAT n "'") s2.store��� 257 by (fs[possible_var_name_def] >> rpt strip_tac >> 258 rename [���STRCAT (STRCAT nm "'") (REPLICATE c #"'")���] >> 259 first_x_assum (qspec_then ���SUC c��� mp_tac) >> 260 simp[] >> 261 full_simp_tac bool_ss [GSYM APPEND_ASSOC, APPEND]) >> 262 pop_assum mp_tac >> 263 first_x_assum (disch_then o mp_then.mp_then mp_then.Any mp_tac) >> 264 simp[] >> 265 rpt (disch_then (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac))>> 266 disch_then (qx_choose_then ���t2��� strip_assume_tac) >> simp[] >> 267 simp[sem_e_def, pair_cases_eq, r_cases_eq, option_cases_eq] >> 268 dsimp[] >> rw[] 269 >- (simp[store_var_def] >> 270 irule possible_var_name_IMP_SUBMAP >> simp[] >> 271 metis_tac[sem_e_possible_var_name]) 272 >- simp[store_var_def, FLOOKUP_DEF] 273 >- metis_tac[sem_e_possible_var_name] 274 >- (simp[store_var_def] >> 275 rename [���FLOOKUP (t2.store |+ (n, _)) k = SOME _���] >> 276 ���k ��� n��� by (strip_tac >> fs[]) >> 277 simp[FLOOKUP_UPDATE] >> first_x_assum irule >> simp[] >> 278 metis_tac[sem_e_possible_var_name])) 279 >- (rpt gen_tac >> rename [���Assign v e���] >> 280 simp[sem_e_def, SimpL ���$==>���, pair_cases_eq, r_cases_eq] >> 281 rw[] >> fs[sem_e_break, exp_max_def, MAX_LESS] >> 282 dsimp[comp_exp_def, sem_t_def, pair_cases_eq, r_cases_eq] >> 283 simp[sem_e_def, pair_cases_eq, r_cases_eq, option_cases_eq] >> 284 first_x_assum (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac) >> 285 simp[] >> 286 disch_then (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac) >> 287 disch_then (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac) >> 288 simp[] >> strip_tac >> simp[store_var_def] >> rw[] >> 289 fs[SUBMAP_DEF, FAPPLY_FUPDATE_THM, FLOOKUP_DEF] >> rw[] >> fs[] >> 290 fs[possible_var_name_def] >> rpt strip_tac >> 291 BasicProvers.VAR_EQ_TAC >> 292 full_simp_tac (srw_ss() ++ ARITH_ss) [])) 293end 294 295val phase2_subset_def = Define ` 296 (phase2_subset (Dec v t) = F) /\ 297 (phase2_subset (Exp e) = T) /\ 298 (phase2_subset Break = T) /\ 299 (phase2_subset (Seq t1 t2) = (phase2_subset t1 /\ phase2_subset t2)) /\ 300 (phase2_subset (If e t1 t2) = (phase2_subset t1 /\ phase2_subset t2)) /\ 301 (phase2_subset (For e1 e2 t) = ((e1 = Num 1) /\ (e2 = Num 1) /\ 302 phase2_subset t))` 303 304val sem_t_possible_var_name = prove( 305 ``!s e i r. 306 (sem_t s e = (i,r)) /\ t_max e < STRLEN k /\ i <> Rfail ==> 307 possible_var_name k s.store ==> 308 possible_var_name k r.store``, 309 HO_MATCH_MP_TAC sem_t_ind \\ REVERSE (REPEAT STRIP_TAC) 310 THEN1 311 (NTAC 4 (POP_ASSUM MP_TAC) 312 \\ ONCE_REWRITE_TAC [sem_t_def] 313 \\ fs [t_max_def,MAX_LESS] 314 \\ REPEAT STRIP_TAC 315 \\ Cases_on `sem_e s e1` \\ fs [] 316 \\ Cases_on `q` \\ fs [sem_e_break] 317 \\ Cases_on `i' = 0` \\ fs [] 318 \\ SRW_TAC [] [] \\ fs [t_max_def,MAX_LESS] 319 THEN1 (METIS_TAC [sem_e_possible_var_name]) 320 \\ Cases_on `sem_t r' e` \\ fs [] 321 \\ REVERSE (Cases_on `q`) \\ fs [] 322 \\ SRW_TAC [] [] \\ fs [] 323 THEN1 (METIS_TAC [sem_e_possible_var_name]) 324 THEN1 (METIS_TAC [sem_e_possible_var_name]) 325 \\ Cases_on `sem_e r'' e2` \\ Cases_on `q` \\ fs [sem_e_break] 326 \\ Cases_on `r'''.clock = 0` \\ fs[] 327 \\ METIS_TAC [sem_e_possible_var_name]) 328 \\ fs [sem_t_def,t_max_def,MAX_LESS] 329 THEN1 330 (Cases_on `sem_e s e` \\ fs [] \\ Cases_on `q` \\ fs [sem_e_break] 331 \\ Cases_on `i' = 0` \\ fs [] 332 \\ METIS_TAC [sem_e_possible_var_name]) 333 THEN1 (Cases_on `sem_t s e` \\ fs [] \\ Cases_on `q` \\ fs [sem_e_break]) 334 THEN1 (SRW_TAC [] []) 335 THEN1 336 (fs [store_var_def] 337 \\ FIRST_X_ASSUM MATCH_MP_TAC 338 \\ fs [possible_var_name_def] 339 \\ CCONTR_TAC \\ fs [] 340 \\ SRW_TAC [] [] \\ fs [] \\ DECIDE_TAC) 341 THEN1 342 (Cases_on `i` \\ fs [sem_e_break] 343 \\ IMP_RES_TAC sem_e_possible_var_name)) 344 |> Q.SPECL [`s`,`e`,`Rval i`,`r`] 345 |> SIMP_RULE (srw_ss()) []; 346 347val IMP_IMP = METIS_PROVE [] ``b /\ (b1 ==> b2) ==> ((b ==> b1) ==> b2)`` 348 349val flatten_t_correct = prove( 350 ``!s e t n res s1. 351 sem_t s e = (res,s1) /\ res <> Rfail /\ phase2_subset e /\ 352 possible_var_name n s.store /\ 353 s.store SUBMAP t.store /\ (t.clock = s.clock) /\ 354 t_max e < LENGTH n ==> 355 ?t1. (sem_t t (flatten_t e n) = (res,t1)) /\ 356 s1.store SUBMAP t1.store /\ (t1.clock = s1.clock) /\ 357 possible_var_name n s1.store /\ 358 (!k v. possible_var_name k s.store /\ 359 t_max e < LENGTH k /\ LENGTH k < LENGTH n /\ 360 FLOOKUP t.store k = SOME v ==> 361 FLOOKUP t1.store k = SOME v)``, 362 HO_MATCH_MP_TAC sem_t_ind \\ REPEAT STRIP_TAC \\ fs [phase2_subset_def] 363 THEN1 (* Exp *) 364 (fs [flatten_t_def,sem_t_def,t_max_def] 365 \\ MP_TAC (SPEC_ALL comp_exp_correct) 366 \\ fs [] \\ REPEAT STRIP_TAC \\ fs []) 367 THEN1 (* Break *) 368 (fs [sem_t_def,flatten_t_def] \\ SRW_TAC [] []) 369 THEN1 (* Seq *) 370 (fs [sem_t_def,flatten_t_def] \\ SRW_TAC [] [] 371 \\ fs [t_max_def,MAX_LESS] 372 \\ Cases_on `sem_t s e` \\ fs [] 373 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`t`,`n`]) 374 \\ `q <> Rfail` by (REPEAT STRIP_TAC \\ fs []) \\ fs [] 375 \\ REPEAT STRIP_TAC \\ fs [] 376 \\ Cases_on `q` \\ fs [] \\ SRW_TAC [] [] 377 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`t1:state`,`n`]) 378 \\ fs [] \\ REPEAT STRIP_TAC \\ fs [] 379 \\ REPEAT STRIP_TAC 380 \\ FIRST_X_ASSUM MATCH_MP_TAC \\ fs [] 381 \\ IMP_RES_TAC sem_t_possible_var_name) 382 THEN1 (* If *) 383 (fs [sem_t_def,flatten_t_def] 384 \\ Cases_on `sem_e s e` \\ fs [] 385 \\ `q <> Rfail` by (REPEAT STRIP_TAC \\ fs []) 386 \\ MP_TAC (Q.SPECL [`e`,`s`] comp_exp_correct) \\ fs [] 387 \\ REPEAT STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`t`,`n`]) 388 \\ fs [MAX_LESS,t_max_def] \\ REPEAT STRIP_TAC \\ fs [sem_e_def] 389 \\ REVERSE (Cases_on `q`) \\ fs [] \\ TRY (SRW_TAC [] [] \\ NO_TAC) 390 \\ Q.MATCH_ASSUM_RENAME_TAC `FLOOKUP t3.store n = SOME i` 391 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`t3:state`,`n`]) \\ fs [] 392 \\ Cases_on `i = 0` \\ fs [] \\ REPEAT STRIP_TAC \\ fs [] 393 \\ REPEAT STRIP_TAC 394 \\ FIRST_X_ASSUM MATCH_MP_TAC \\ fs [] 395 \\ IMP_RES_TAC sem_e_possible_var_name) 396 THEN1 (* For *) 397 (ASM_SIMP_TAC (srw_ss()) [sem_t_def_with_stop,flatten_t_def,sem_e_def] 398 \\ fs [sem_e_def,t_max_def] \\ SRW_TAC [] [] 399 \\ Q.PAT_ASSUM `sem_t s (For (Num 1) (Num 1) e) = (res,s1)` MP_TAC 400 \\ ONCE_REWRITE_TAC [sem_t_def] \\ fs [sem_e_def] 401 \\ REPEAT STRIP_TAC \\ Cases_on `sem_t s e` \\ fs [] 402 \\ `q <> Rfail` by (REPEAT STRIP_TAC \\ fs []) 403 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`t`,`n`]) 404 \\ fs [MAX_LESS,t_max_def] \\ REPEAT STRIP_TAC \\ fs [sem_e_def] 405 \\ REVERSE (Cases_on `q`) \\ fs [] \\ TRY (SRW_TAC [] [] \\ NO_TAC) 406 \\ Cases_on `r.clock = 0` \\ fs [] THEN1 (SRW_TAC [] []) 407 \\ fs [STOP_def] 408 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`dec_clock t1`,`n`]) 409 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 410 THEN1 (fs [dec_clock_def]) \\ REPEAT STRIP_TAC \\ fs [] 411 \\ fs [flatten_t_def] \\ REPEAT STRIP_TAC 412 \\ FIRST_X_ASSUM MATCH_MP_TAC \\ fs [] 413 \\ IMP_RES_TAC sem_t_possible_var_name)); 414 415val phase2_correct = flatten_t_correct 416 |> Q.SPECL [`s`,`t`,`s`,`"temp" ++ REPLICATE (t_max t - 3) #"'"`] 417 |> DISCH ``s.store = FEMPTY`` 418 |> SIMP_RULE (srw_ss()) [GSYM phase2_def,Once possible_var_name_def, 419 rich_listTheory.LENGTH_REPLICATE,DECIDE ``n < 4 + (n - 3:num)``, 420 PULL_FORALL] |> GEN_ALL; 421 422val pair_eq = prove( 423 ``(x = (y1,y2)) <=> (FST x = y1) /\ (SND x = y2)``, 424 Cases_on `x` \\ fs [] \\ METIS_TAC []); 425 426val phase2_correct_FST = prove( 427 ``phase2_subset t ==> 428 (FST (sem_t (s_with_clock c) t) = Rfail) \/ 429 (FST (sem_t (s_with_clock c) (phase2 t)) = 430 FST (sem_t (s_with_clock c) t))``, 431 REPEAT STRIP_TAC \\ CCONTR_TAC \\ fs [] 432 \\ MP_TAC (phase2_correct 433 |> Q.SPECL [`t`,`s_with_clock c`] 434 |> SIMP_RULE std_ss [pair_eq]) 435 \\ fs [s_with_clock_def]); 436 437val lemma = prove( 438 ``((if b then x1 else x2) <> x2) <=> (x1 <> x2) /\ b``, 439 Cases_on `b` \\ fs []) 440 441(* We prove that phase 2 preserves semantics if the source semantics 442 does not Crash (implied by successful type check) and if the syntax 443 of the compiler program fits with phase2_subset (i.e. syntax 444 produced by phase1) *) 445 446val phase2_pres = store_thm("phase2_pres", 447 ``!t. semantics t <> Crash /\ phase2_subset t ==> 448 semantics (phase2 t) = semantics t``, 449 REPEAT STRIP_TAC \\ fs [semantics_thm] 450 \\ REVERSE (SRW_TAC [] []) \\ fs [lemma] \\ fs [pair_eq] 451 \\ REPEAT (FIRST_X_ASSUM (MP_TAC o Q.SPEC `c:num`)) 452 \\ REPEAT STRIP_TAC \\ fs [] 453 \\ MP_TAC phase2_correct_FST \\ fs []); 454 455 456(* === PHASE 3 : maps the FOR language into assmembly code === *) 457 458(* We define the tagert assembly language *) 459 460val _ = Datatype ` 461reg = Reg string` 462 463val _ = Datatype ` 464instr = 465 Add reg reg reg 466 | Int reg int 467 | Jmp num 468 | JmpIf reg num`; 469 470val _ = Datatype ` 471state_a = <| store : state; pc : num; instrs : instr list |>`; 472 473val do_jump_def = Define ` 474do_jump s n = 475 if n > s.pc then 476 (Rval 0, s with pc := n) 477 else if s.store.clock = 0 then 478 (Rtimeout, s) 479 else 480 let st' = s.store with clock := s.store.clock - 1 in 481 (Rval 0, s with <| store := st'; pc := n |>)`; 482 483val inc_pc_def = Define ` 484inc_pc s = s with pc := s.pc + 1`; 485 486val sem_e_clock = prove( 487 ``!e x st' st. (sem_e st e = (x,st')) ==> (st'.clock = st.clock)``, 488 Induct \\ fs [sem_e_def] \\ REPEAT STRIP_TAC 489 \\ every_case_tac \\ SRW_TAC [] [] \\ fs [store_var_def] \\ METIS_TAC []) |> GSYM; 490 491val sem_a_def = tDefine "sem_a" ` 492sem_a s = 493 if s.pc < LENGTH s.instrs then 494 case EL s.pc s.instrs of 495 | Int (Reg r) i => 496 let (r,st) = sem_e s.store (Assign r (Num i)) in 497 let s' = s with store := st in 498 (case r of 499 | Rval _ => sem_a (inc_pc s') 500 | _ => (r, s')) 501 | Add (Reg r) (Reg r1) (Reg r2) => 502 let (r,st) = sem_e s.store (Assign r (Add (Var r1) (Var r2))) in 503 let s' = s with store := st in 504 (case r of 505 | Rval _ => sem_a (inc_pc s') 506 | _ => (r, s')) 507 | Jmp n' => 508 (case do_jump s n' of 509 | (Rval _, s') => sem_a s' 510 | r => r) 511 | JmpIf (Reg r) n' => 512 let (r,st) = sem_e s.store (Var r) in 513 let s' = s with store := st in 514 case r of 515 | Rval n => 516 if n <> 0 then 517 sem_a (inc_pc s') 518 else 519 (case do_jump s' n' of 520 | (Rval _, s') => sem_a s' 521 | r => r) 522 | _ => (r, s') 523 else if s.pc = LENGTH s.instrs then 524 (Rval 0, s) 525 else 526 (Rfail, s)` 527 (WF_REL_TAC `inv_image (measure I LEX measure I) 528 (\s. (s.store.clock,LENGTH s.instrs - s.pc))` 529 \\ fs [inc_pc_def,do_jump_def,LET_DEF] 530 \\ REPEAT STRIP_TAC 531 \\ every_case_tac \\ fs [] 532 \\ SRW_TAC [] [] \\ fs [] 533 \\ IMP_RES_TAC sem_e_clock 534 \\ DECIDE_TAC); 535 536val a_state_def = Define ` 537 a_state code clock = 538 <| store := s_with_clock clock; pc := 0; instrs := code |>`; 539 540val asm_semantics_def = Define ` 541 asm_semantics code = 542 if (?c s. sem_a (a_state code c) = (Rval 0,s)) then Terminate 543 else if (!c. ?s. sem_a (a_state code c) = (Rtimeout,s)) then Diverge 544 else Crash`; 545 546(* Definition of phase3 *) 547 548val phase3_def = Define ` 549 (phase3 n b (Dec v t) = []) /\ 550 (phase3 n b (Exp e) = 551 case e of 552 | Assign v (Var x) => 553 if x = v then [] else [Int (Reg v) 0; Add (Reg v) (Reg x) (Reg v)] 554 | Assign v (Add (Var v1) (Var v2)) => [Add (Reg v) (Reg v1) (Reg v2)] 555 | Assign v (Num i) => [Int (Reg v) i] 556 | _ => []) /\ 557 (phase3 n b Break = [Jmp b]) /\ 558 (phase3 n b (Seq t1 t2) = 559 let c1 = phase3 n b t1 in 560 let c2 = phase3 (n + LENGTH c1) b t2 in 561 c1 ++ c2) /\ 562 (phase3 n b (If e t1 t2) = 563 let c1 = phase3 (n + 1) b t1 in 564 let c2 = phase3 (n + 2 + LENGTH c1) b t2 in 565 [JmpIf (case e of Var v => Reg v | _ => Reg "") 566 (n + 2 + LENGTH c1)] ++ c1 ++ 567 [Jmp (n + 2 + LENGTH c1 + LENGTH c2)] ++ c2) /\ 568 (phase3 n b (For e1 e2 t) = 569 let c1 = phase3 n 0 t in 570 let c2 = phase3 n (n + 1 + LENGTH c1) t in 571 c2 ++ [Jmp n])` 572 573(* Verification of phase3 *) 574 575val LENGTH_phase3 = prove( 576 ``!t n b. LENGTH (phase3 n b t) = LENGTH (phase3 0 0 t)``, 577 Induct \\ fs [phase3_def,LET_DEF]); 578 579val phase3_subset_def = Define ` 580 (phase3_subset (Dec v t) = F) /\ 581 (phase3_subset (Exp e) <=> 582 (?v x. e = Assign v (Var x)) \/ 583 (?v i. e = Assign v (Num i)) \/ 584 (?v x y. e = Assign v (Add (Var x) (Var y)))) /\ 585 (phase3_subset Break = T) /\ 586 (phase3_subset (Seq t1 t2) = (phase3_subset t1 /\ phase3_subset t2)) /\ 587 (phase3_subset (If e t1 t2) <=> 588 (?w. e = Var w) /\ phase3_subset t1 /\ phase3_subset t2) /\ 589 (phase3_subset (For e1 e2 t) = ((e1 = Num 1) /\ (e2 = Num 1) /\ phase3_subset t))` 590 591val instr_lookup_lemma = prove( 592 ``(x.pc = LENGTH xs) /\ (x.instrs = xs ++ [y] ++ ys) ==> 593 x.pc < LENGTH x.instrs /\ (EL x.pc x.instrs = y)``, 594 fs [DECIDE ``n < n + 1 + m:num``,rich_listTheory.EL_LENGTH_APPEND] 595 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 596 \\ fs [rich_listTheory.EL_LENGTH_APPEND]); 597 598val EL_LENGTH_APPEND_LEMMA = 599 rich_listTheory.EL_LENGTH_APPEND 600 |> Q.SPECL [`[y] ++ ys`,`xs1++xs2`] 601 |> SIMP_RULE (srw_ss()) [] 602 603val EL_LEMMA = prove( 604 ``(LENGTH (xs1 ++ xs2 ++ xs3) = n) ==> 605 (EL n (xs1 ++ xs2 ++ xs3 ++ [y] ++ ys1 ++ ys2) = y)``, 606 Q.SPEC_TAC (`(xs1 ++ xs2 ++ xs3)`,`zs`) \\ SRW_TAC [] [] 607 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 608 \\ fs [rich_listTheory.EL_LENGTH_APPEND]); 609 610val state_rel_def = Define ` 611 state_rel s x = (x.store = s)`; 612 613local val rw = srw_tac[] val fs = fsrw_tac[] val rfs = rev_full_simp_tac(srw_ss()) in 614val phase3_lemma = prove( 615 ``!s1 t res s2 x xs ys b. 616 (sem_t s1 t = (res,s2)) /\ phase3_subset t /\ 617 state_rel s1 x /\ 618 (x.pc = LENGTH xs) /\ 619 (x.instrs = xs ++ phase3 (LENGTH xs) b t ++ ys) /\ 620 res <> Rfail /\ 621 (res = Rbreak ==> LENGTH (xs ++ phase3 (LENGTH xs) b t) <= b) ==> 622 ?x'. 623 (sem_a x = sem_a x') /\ 624 state_rel s2 x' /\ OMIT ( 625 (x'.instrs = x.instrs) /\ 626 (case res of 627 | Rfail => T 628 | Rbreak => (x'.pc = b) 629 | Rtimeout => (sem_a x' = (Rtimeout,x')) 630 | Rval v => (x'.pc = LENGTH (xs ++ phase3 (LENGTH xs) b t))))``, 631 REWRITE_TAC [state_rel_def,OMIT_def] 632 \\ HO_MATCH_MP_TAC sem_t_ind \\ REPEAT STRIP_TAC \\ fs [phase3_subset_def] 633 THEN1 (* Exp 1 *) 634 (fs [phase3_def,sem_t_def] \\ rfs [] 635 \\ Cases_on `v = x'` \\ fs [] THEN1 636 (fs [sem_e_def] 637 \\ Cases_on `FLOOKUP s1.store x'` \\ fs [] \\ SRW_TAC [] [] 638 \\ Q.EXISTS_TAC `x` \\ fs [store_var_def,state_component_equality] 639 \\ fs [FLOOKUP_DEF,fmap_EXT,FAPPLY_FUPDATE_THM] 640 \\ SRW_TAC [] [] \\ fs [EXTENSION] \\ METIS_TAC []) 641 \\ SIMP_TAC std_ss [Once sem_a_def] 642 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 643 \\ imp_res_tac (instr_lookup_lemma |> REWRITE_RULE [GSYM APPEND_ASSOC,APPEND]) 644 \\ fs [LET_DEF,rich_listTheory.EL_LENGTH_APPEND] 645 \\ fs [sem_e_def] \\ SRW_TAC [] [] 646 \\ Cases_on `FLOOKUP x.store.store x'` \\ fs [] \\ SRW_TAC [] [] 647 \\ SIMP_TAC std_ss [Once sem_a_def] 648 \\ fs [inc_pc_def,DECIDE ``n + 1 < n + 2 + m:num``] 649 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND, 650 rich_listTheory.EL_LENGTH_APPEND 651 |> Q.SPECL [`y::ys`,`xs ++ [x]`] 652 |> SIMP_RULE (srw_ss()) [] 653 |> SIMP_RULE std_ss [APPEND,GSYM APPEND_ASSOC]] 654 \\ fs [sem_e_def,store_var_def,FLOOKUP_DEF,FAPPLY_FUPDATE_THM,LET_DEF] 655 \\ Q.EXISTS_TAC `(x with 656 <|store := 657 x.store with store := x.store.store |+ (v,x''); 658 pc := LENGTH xs + 1 + 1|>)` 659 \\ fs [GSYM ADD_ASSOC]) 660 THEN1 (* Exp 2 *) 661 (fs [phase3_def,sem_t_def] \\ rfs [] 662 \\ SIMP_TAC std_ss [Once sem_a_def] 663 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 664 \\ imp_res_tac (instr_lookup_lemma |> REWRITE_RULE [GSYM APPEND_ASSOC,APPEND]) 665 \\ fs [LET_DEF,rich_listTheory.EL_LENGTH_APPEND] 666 \\ fs [sem_e_def] \\ SRW_TAC [] [] 667 \\ Q.EXISTS_TAC `(inc_pc (x with store := store_var v i x.store))` 668 \\ fs [inc_pc_def]) 669 THEN1 (* Exp 2 *) 670 (fs [phase3_def,sem_t_def] \\ rfs [] 671 \\ SIMP_TAC std_ss [Once sem_a_def] 672 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 673 \\ imp_res_tac (instr_lookup_lemma |> REWRITE_RULE [GSYM APPEND_ASSOC,APPEND]) 674 \\ fs [LET_DEF,rich_listTheory.EL_LENGTH_APPEND] 675 \\ fs [sem_e_def] \\ SRW_TAC [] [] 676 \\ every_case_tac \\ fs [] \\ SRW_TAC [] [] 677 \\ Q.EXISTS_TAC `(inc_pc (x with store := store_var v (i'' + i') x.store))` 678 \\ fs [inc_pc_def]) 679 THEN1 (* Break *) 680 (fs [sem_t_def] \\ SRW_TAC [] [] \\ fs [phase3_def,LET_DEF] 681 \\ SIMP_TAC std_ss [Once sem_a_def] 682 \\ imp_res_tac instr_lookup_lemma \\ fs [LET_DEF] 683 \\ fs [do_jump_def] 684 \\ `b > LENGTH xs` by DECIDE_TAC \\ fs [] 685 \\ Q.EXISTS_TAC `x with pc := b` 686 \\ fs [] \\ fs [state_component_equality]) 687 THEN1 (* Seq *) 688 (fs [sem_t_def] \\ SRW_TAC [] [] \\ fs [phase3_def,LET_DEF] 689 \\ Cases_on `sem_t x.store t` \\ fs [] 690 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`x`,`xs`, 691 `phase3 (LENGTH xs + LENGTH (phase3 (LENGTH (xs:instr list)) b t)) b t' 692 ++ ys`,`b`]) \\ fs [] 693 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 694 THEN1 (Cases_on `q` \\ fs [] \\ SRW_TAC [] [] \\ DECIDE_TAC) 695 \\ REPEAT STRIP_TAC \\ fs [] 696 \\ Q.MATCH_ASSUM_RENAME_TAC `x2.store = r` 697 \\ REVERSE (Cases_on `q`) \\ fs [] \\ SRW_TAC [] [] 698 \\ TRY (Q.EXISTS_TAC `x2` \\ fs [] \\ NO_TAC) 699 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`x2`,`xs ++ phase3 (LENGTH xs) b t`, 700 `ys`,`b`]) \\ fs [] 701 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 702 THEN1 (REPEAT STRIP_TAC \\ fs [] \\ DECIDE_TAC) 703 \\ REPEAT STRIP_TAC 704 \\ Q.MATCH_ASSUM_RENAME_TAC `x3.store = s2` 705 \\ Q.EXISTS_TAC `x3` \\ fs [] 706 \\ fs [ADD_ASSOC]) 707 THEN1 (* If *) 708 (fs [phase3_def,sem_t_def] 709 \\ SIMP_TAC std_ss [Once sem_a_def] \\ fs [LET_DEF] 710 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 711 \\ imp_res_tac (instr_lookup_lemma |> REWRITE_RULE [GSYM APPEND_ASSOC]) 712 \\ rfs [] \\ POP_ASSUM (K ALL_TAC) 713 \\ REVERSE (Cases_on `sem_e s1 (Var w)`) \\ fs [] 714 \\ REVERSE (Cases_on `q`) \\ fs [] 715 \\ SRW_TAC [] [] \\ fs [sem_e_break] 716 \\ REPEAT (POP_ASSUM MP_TAC) 717 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 718 \\ REPEAT STRIP_TAC 719 \\ Q.ABBREV_TAC `gg = (LENGTH xs + 2 + LENGTH (phase3 0 0 t1) + 720 LENGTH (phase3 0 0 t2))` 721 THEN1 (* false case *) 722 (FIRST_X_ASSUM (MP_TAC o Q.SPECL [`(inc_pc (x with store := r))`, 723 `xs ++ [JmpIf (Reg w) (LENGTH (xs:instr list) + 2 + LENGTH (phase3 0 0 t1))]`, 724 `[Jmp gg] ++ phase3 (LENGTH (xs:instr list) + 2 + LENGTH (phase3 0 0 t1)) 725 b t2 ++ ys`,`b`]) \\ fs [] 726 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 727 THEN1 (fs [inc_pc_def] \\ REPEAT STRIP_TAC \\ fs [] \\ DECIDE_TAC) 728 \\ REPEAT STRIP_TAC \\ fs [] 729 \\ Q.MATCH_ASSUM_RENAME_TAC `x2.store = s2` 730 \\ REVERSE (Cases_on `res`) \\ fs [] 731 \\ TRY (Q.EXISTS_TAC `x2` \\ fs [] \\ NO_TAC) 732 \\ SIMP_TAC std_ss [Once sem_a_def] \\ fs [LET_DEF] 733 \\ `LENGTH xs + 1 + LENGTH (phase3 0 0 t1) < 734 LENGTH xs + 1 + LENGTH (phase3 (LENGTH xs + 1) b t1) + 1 + 735 LENGTH (phase3 (LENGTH xs + 2 + LENGTH (phase3 0 0 t1)) b t2) + 736 LENGTH ys /\ 737 (EL (LENGTH xs + 1 + LENGTH (phase3 0 0 t1)) 738 (xs ++ [JmpIf (Reg w) (LENGTH xs + 2 + LENGTH (phase3 0 0 t1))] ++ 739 phase3 (LENGTH xs + 1) b t1 ++ [Jmp gg] ++ 740 phase3 (LENGTH xs + 2 + LENGTH (phase3 0 0 t1)) b t2 ++ ys) = 741 Jmp gg)` by 742 (ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 743 \\ REPEAT STRIP_TAC THEN1 DECIDE_TAC 744 \\ MATCH_MP_TAC EL_LEMMA 745 \\ fs [] \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs []) 746 \\ fs [do_jump_def] 747 \\ UNABBREV_ALL_TAC 748 \\ SRW_TAC [] [] 749 \\ TRY (`F` by DECIDE_TAC) 750 \\ Q.EXISTS_TAC `(x2 with pc := 751 LENGTH xs + 2 + LENGTH (phase3 0 0 t1) + LENGTH (phase3 0 0 t2))` 752 \\ fs [AC ADD_COMM ADD_ASSOC,ADD1] \\ DECIDE_TAC) 753 (* true case *) 754 \\ fs [do_jump_def,DECIDE ``n + 2 + m > n:num``] 755 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [ 756 `(x with <|store := r; pc := LENGTH (xs:instr list) + 757 2 + LENGTH (phase3 0 0 t1)|>)`, 758 `xs ++ [JmpIf (Reg w) (LENGTH xs + 2 + LENGTH (phase3 0 0 t1))] ++ 759 phase3 (LENGTH xs + 1) b t1 ++ [Jmp gg]`, `ys`,`b`]) \\ fs [] 760 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 761 (fs [AC ADD_COMM ADD_ASSOC,DECIDE ``1+(1+n) = 2 + n:num``] 762 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 763 \\ REPEAT STRIP_TAC \\ fs [] \\ DECIDE_TAC) 764 \\ REPEAT STRIP_TAC \\ fs [] 765 \\ Q.MATCH_ASSUM_RENAME_TAC `x2.store = s2` 766 \\ REPEAT (POP_ASSUM MP_TAC) 767 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 768 \\ REPEAT STRIP_TAC 769 \\ Q.EXISTS_TAC `x2` \\ fs [] 770 \\ fs [AC ADD_COMM ADD_ASSOC,DECIDE ``1+(1+n) = 2 + n:num``,ADD1] 771 \\ Cases_on `res` \\ fs []) 772 THEN1 (* For *) 773 (fs [sem_e_def] \\ SRW_TAC [] [] 774 \\ Q.PAT_ASSUM `sem_t x.store (For (Num 1) (Num 1) t) = (res,s2)` MP_TAC 775 \\ SIMP_TAC (srw_ss()) [sem_t_def_with_stop,sem_e_def] 776 \\ SIMP_TAC std_ss [STOP_def] 777 \\ Cases_on `sem_t x.store t` \\ fs [phase3_def,LET_DEF] 778 \\ STRIP_TAC 779 \\ FIRST_X_ASSUM (MP_TAC o Q.SPECL [`x`,`xs`, 780 `[Jmp (LENGTH (xs:instr list))] ++ ys`,`(LENGTH (xs:instr list) + 1 + 781 LENGTH (phase3 (LENGTH (xs:instr list)) 0 t))`]) \\ fs [] 782 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 783 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 784 THEN1 (REPEAT STRIP_TAC \\ fs []) 785 \\ REPEAT STRIP_TAC \\ fs [] 786 \\ Q.MATCH_ASSUM_RENAME_TAC `x2.store = r` 787 \\ REVERSE (Cases_on `q`) \\ fs [] \\ SRW_TAC [] [] 788 \\ TRY (Q.EXISTS_TAC `x2` \\ fs [AC ADD_COMM ADD_ASSOC] \\ NO_TAC) 789 \\ SIMP_TAC std_ss [Once sem_a_def] 790 \\ `x2.pc < LENGTH x2.instrs` by 791 (fs [] \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] \\ DECIDE_TAC) \\ fs [] 792 \\ `(EL (LENGTH xs + LENGTH (phase3 0 0 t)) (xs ++ 793 phase3 (LENGTH xs) (LENGTH xs + 1 + LENGTH (phase3 0 0 t)) t ++ 794 [Jmp (LENGTH xs)] ++ ys) = Jmp (LENGTH xs))` by 795 (`LENGTH (phase3 0 0 t) = 796 LENGTH (phase3 (LENGTH (xs:instr list)) 797 (LENGTH (xs:instr list) + 1 + LENGTH (phase3 0 0 t)) t)` by 798 (fs [] \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs []) 799 \\ POP_ASSUM (fn th => SIMP_TAC std_ss [Once th]) 800 \\ fs [EL_LENGTH_APPEND_LEMMA]) 801 \\ fs [do_jump_def,DECIDE ``~(n > n + k:num)``,LET_DEF] 802 \\ Cases_on `x2.store.clock = 0` \\ fs [] THEN1 803 (SRW_TAC [] [] \\ fs [] 804 \\ Q.EXISTS_TAC `x2` \\ fs [] 805 \\ SIMP_TAC std_ss [EQ_SYM_EQ] \\ fs [] 806 \\ ONCE_REWRITE_TAC [sem_a_def] 807 \\ fs [do_jump_def,DECIDE ``~(n > n + k:num)``,LET_DEF]) 808 \\ Q.PAT_ASSUM `!x. bb` MP_TAC 809 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [] 810 \\ REPEAT STRIP_TAC 811 \\ FIRST_X_ASSUM MATCH_MP_TAC 812 \\ fs [dec_clock_def] 813 \\ REPEAT STRIP_TAC \\ fs [] 814 \\ Q.PAT_ASSUM `xxx <= b` MP_TAC 815 \\ ONCE_REWRITE_TAC [LENGTH_phase3] \\ fs [])) 816end 817 818val _ = save_thm("phase3_lemma", 819 phase3_lemma |> REWRITE_RULE [state_rel_def]); 820 821val phase3_thm = phase3_lemma 822 |> REWRITE_RULE [state_rel_def,OMIT_def]; 823 824val phase3_correct = store_thm("phase3_correct", 825 ``!s1 t res s2 x xs ys b. 826 (sem_t s1 t = (res,s2)) /\ phase3_subset t /\ 827 (x.store = s1) /\ 828 (x.pc = 0) /\ 829 (x.instrs = phase3 0 0 t) /\ 830 res <> Rfail /\ res <> Rbreak ==> 831 ?res' x'. 832 (sem_a x = (res', x')) /\ 833 (x'.store = s2) /\ 834 (case res of 835 | Rval v => (res' = Rval 0) 836 | _ => (res' = res))``, 837 REPEAT STRIP_TAC 838 \\ MP_TAC (SPEC_ALL phase3_thm 839 |> Q.INST [`xs`|->`[]`,`ys`|->`[]`,`b`|->`0`]) 840 \\ fs [phase3_def] \\ REPEAT STRIP_TAC \\ fs [] 841 \\ Cases_on `res` \\ fs [rich_listTheory.EL_LENGTH_APPEND] 842 \\ SIMP_TAC std_ss [Once sem_a_def] 843 \\ fs [rich_listTheory.EL_LENGTH_APPEND]); 844 845(* We prove that phase3 preserves semantics if the source does not 846 crash and if the syntax fits within the subset defined by 847 phase3_subset. *) 848 849val phase3_pres = store_thm("phase3_pres", 850 ``!t. semantics t <> Crash /\ phase3_subset t ==> 851 asm_semantics (phase3 0 0 t) = semantics t``, 852 REPEAT STRIP_TAC \\ fs [semantics_thm] 853 \\ REVERSE (SRW_TAC [] []) 854 THEN1 METIS_TAC [] 855 THEN1 856 (fs [asm_semantics_def] 857 \\ REVERSE (sg `!c. ?s. sem_a (a_state (phase3 0 0 t) c) = (Rtimeout,s)`) 858 THEN1 (fs [] \\ SRW_TAC [] [] 859 \\ FIRST_X_ASSUM (MP_TAC o Q.SPEC `c`) \\ fs []) 860 \\ REPEAT STRIP_TAC 861 \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC `c`) 862 \\ MP_TAC (Q.SPECL [`s_with_clock c`,`t`] phase3_correct) \\ fs [] 863 \\ REPEAT STRIP_TAC 864 \\ POP_ASSUM (MP_TAC o Q.SPEC `a_state (phase3 0 0 t) c`) 865 \\ fs [a_state_def] \\ REPEAT STRIP_TAC \\ fs []) 866 \\ fs [asm_semantics_def] 867 \\ MATCH_MP_TAC (METIS_PROVE [] ``b ==> ((if b then x else y) = x)``) 868 \\ Q.EXISTS_TAC `c` 869 \\ MP_TAC (Q.SPECL [`s_with_clock c`,`t`] phase3_correct) \\ fs [] 870 \\ REPEAT STRIP_TAC 871 \\ POP_ASSUM (MP_TAC o Q.SPEC `a_state (phase3 0 0 t) c`) 872 \\ fs [a_state_def] \\ REPEAT STRIP_TAC \\ fs []); 873 874 875(* === The end-to-end compiler === *) 876 877val compile_def = Define ` 878 compile t = phase3 0 0 (phase2 (phase1 t))`; 879 880(* Verification of the compile function *) 881 882val phase2_subset_phase1 = prove( 883 ``!t. phase2_subset (phase1 t)``, 884 Induct \\ fs [phase1_def,phase2_subset_def,Loop_def]); 885 886val phase3_subset_comp_exp = prove( 887 ``!e n. phase3_subset (comp_exp e n)``, 888 Induct \\ fs [phase3_subset_def,comp_exp_def]); 889 890val phase3_subset_flatten_t = prove( 891 ``!t n. phase2_subset t ==> phase3_subset (flatten_t t n)``, 892 Induct \\ fs [phase2_subset_def,flatten_t_def,phase3_subset_def] 893 \\ fs [phase3_subset_comp_exp]); 894 895val phase3_subset_phase2_phase1 = prove( 896 ``!t. phase3_subset (phase2 (phase1 t))``, 897 fs [phase2_def] \\ REPEAT STRIP_TAC 898 \\ MATCH_MP_TAC phase3_subset_flatten_t 899 \\ fs [phase2_subset_phase1]); 900 901(* The compile function produces code that has observable behaviour 902 that is identical to the source program, if the course program does 903 not Crash. *) 904 905val compile_pres = store_thm("compile_pres", 906 ``!t. semantics t <> Crash ==> 907 (asm_semantics (compile t) = semantics t)``, 908 fs [compile_def] 909 \\ ONCE_REWRITE_TAC [GSYM phase1_pres] 910 \\ REPEAT STRIP_TAC 911 \\ IMP_RES_TAC phase2_pres 912 \\ fs [phase2_subset_phase1] 913 \\ POP_ASSUM (fn th => ONCE_REWRITE_TAC [GSYM th]) 914 \\ MATCH_MP_TAC phase3_pres 915 \\ fs [phase2_pres,phase2_subset_phase1,phase3_subset_phase2_phase1]); 916 917(* The simple type checker (defined in forScript.sml) ensures that the 918 source program cannot Crash. This leads to a cleaner top-level 919 correctness theorem for compile. *) 920 921val syntax_ok_def = Define ` 922 syntax_ok t = type_t F {} t`; 923 924val compile_correct = store_thm("compile_correct", 925 ``!t. syntax_ok t ==> 926 (asm_semantics (compile t) = semantics t)``, 927 METIS_TAC [type_soundness,syntax_ok_def,compile_pres]); 928 929val _ = set_trace "Goalstack.print_goal_at_top" 0; 930 931(* Start re-verification of phase1 in relational big step semantics *) 932 933val sem_e_reln_not = Q.prove( 934 `���s e res. sem_e_reln s e res ��� FST res ��� Rbreak ��� FST res ��� Rtimeout`, 935 ho_match_mp_tac sem_e_reln_ind>>rw[]) 936 937val semttac = simp[Once simple_sem_t_reln_cases,is_rval_def] 938val semetac = simp[Once sem_e_reln_cases] 939val sdtac = simp[Once simple_sem_t_div_cases] 940 941val phase1_correct_reln = store_thm("phase1_correct_reln", 942``���s t res. simple_sem_t_reln s t res ��� simple_sem_t_reln s (phase1 t) res``, 943 ho_match_mp_tac simple_sem_t_reln_strongind>>fs[phase1_def]>>rw[]>> 944 TRY(semttac>>metis_tac[]) 945 >- metis_tac[simple_sem_t_reln_cases,sem_e_reln_cases]>> 946 simp[Loop_def]>>semttac>> 947 ntac 8 semetac>> 948 metis_tac[simple_sem_t_reln_cases,is_rval_def,sem_e_reln_not,FST,sem_e_reln_cases,Loop_def]) 949 950val phase1_correct_div_lemma = Q.prove ( 951`���s t'. (���t. phase1 t = t' ��� simple_sem_t_div s t) ��� simple_sem_t_div s t'`, 952 ho_match_mp_tac simple_sem_t_div_coind>>rw[]>> 953 Cases_on`t`>>fs[phase1_def,Loop_def,PULL_EXISTS]>> 954 pop_assum mp_tac>> sdtac>>rw[] 955 >- metis_tac[simple_sem_t_div_cases,sem_e_reln_cases,simple_sem_t_reln_cases,is_rval_def]>> 956 TRY(metis_tac[phase1_correct_reln]) 957 >- 958 (semetac>>DISJ1_TAC>> 959 qexists_tac`If e0 (Seq t' (Exp e)) Break`>>fs[phase1_def]>> 960 metis_tac[simple_sem_t_div_cases]) 961 >> 962 semetac>>DISJ2_TAC>> 963 ntac 2 semetac>> 964 qexists_tac`n3`>>qexists_tac`s3`>>qexists_tac`For e0 e t'`>> 965 CONJ_TAC>- metis_tac[phase1_correct_reln,simple_sem_t_reln_cases]>> 966 fs[phase1_def,Loop_def]) 967 968val phase1_correct_div = store_thm("phase1_correct_div", 969``���s t. simple_sem_t_div s t ��� simple_sem_t_div s (phase1 t)``, 970 metis_tac[phase1_correct_div_lemma]) 971 972Theorem phase1_pres_rel: 973 ���t. rel_semantics t ��� Crash ��� rel_semantics (phase1 t) = rel_semantics t 974Proof 975 strip_tac>>fs[rel_semantics_def]>> 976 metis_tac[phase1_correct_reln,simple_sem_t_reln_not_div,phase1_correct_div] 977QED 978 979(* End verification for relational semantics -- 43 lines *) 980 981(* We now re-verify phase1 in the relational Pretty Big Step semantics (for terminating programs) *) 982 983val pb_sem_t_reln_Exp = ``pb_sem_t_reln s1' (Trm (Exp e)) r3'`` 984 |> SIMP_CONV (srw_ss()) [Once pb_sem_t_reln_cases,abort_def]; 985 986val sem_e_reln_Num = store_thm("sem_e_reln_Num[simp]", 987 ``sem_e_reln s (Num n) r1 <=> r1 = (Rval n,s)``, 988 fs [Once sem_e_reln_cases]); 989 990val pb_sem_t_reln_Forn2 = ``pb_sem_t_reln s (Forn 2 r3 n1 n1 t) (Ter r)`` 991 |> SIMP_CONV (srw_ss()) [Once pb_sem_t_reln_cases,abort_def]; 992 993val pb_sem_t_reln_Forn3 = ``pb_sem_t_reln s (Forn 3 r3 n1 n1 t) (Ter r)`` 994 |> SIMP_CONV (srw_ss()) [Once pb_sem_t_reln_cases,abort_def]; 995 996local 997 val rw = srw_tac[] val fs = fsrw_tac[] 998 val bp_step_tac = simp [Once pb_sem_t_reln_cases] \\ fs []; 999 val bp_size_step_tac = simp [Once pb_sem_t_size_reln_cases] \\ fs []; 1000in 1001val pb_sem_t_reln_IMP_phase1 = Q.store_thm("pb_sem_t_reln_IMP_phase1", 1002 `!s t r. 1003 pb_sem_t_reln s (Trm t) (Ter r) ��� 1004 pb_sem_t_reln s (Trm (phase1 t)) (Ter r)`, 1005 simp [Once pb_sem_t_size_reln_equiv,PULL_EXISTS] 1006 \\ completeInduct_on `n` \\ fs [PULL_FORALL] 1007 \\ Cases_on `t` \\ fs [phase1_def] 1008 \\ TRY (rw [] \\ fs [pb_sem_t_size_reln_equiv] 1009 \\ qexists_tac `n` \\ fs [] \\ NO_TAC) 1010 THEN1 (* Dec case *) 1011 (bp_size_step_tac \\ fs [] \\ rw [] 1012 \\ fs [AND_IMP_INTRO] \\ res_tac \\ fs [] 1013 \\ ntac 2 (bp_step_tac \\ fs [] \\ rw []) 1014 \\ rpt (fs [Once sem_e_reln_cases,is_rval_def])) 1015 THEN1 (* Seq case *) 1016 (bp_size_step_tac \\ fs [] \\ rw [] 1017 \\ fs [AND_IMP_INTRO] \\ res_tac \\ fs [] 1018 \\ fs [DECIDE ``0 < h' + 1n /\ h' < h + (h' + 1n)``] 1019 \\ bp_step_tac \\ rw [] \\ metis_tac []) 1020 THEN1 (* If case *) 1021 (bp_size_step_tac \\ fs [] \\ rw [] 1022 \\ fs [AND_IMP_INTRO] \\ res_tac \\ fs [] 1023 \\ bp_step_tac \\ rw [] \\ metis_tac []) 1024 (* the rest is For case *) 1025 \\ ntac 2 bp_size_step_tac \\ fs [] \\ rw [] 1026 THEN1 (* For stops *) 1027 (rw [Loop_def] 1028 \\ ntac 4 (bp_step_tac \\ fs [] \\ rw [sem_e_reln_Num]) 1029 \\ fs [pb_sem_t_reln_Forn2] \\ metis_tac []) 1030 THEN1 (* For runs the body *) 1031 (ntac 2 (pop_assum mp_tac) 1032 \\ bp_size_step_tac \\ fs [] \\ rw [Loop_def] 1033 \\ `!x. sem_e_reln s e0 x <=> (x = (Rval n',s'))` by 1034 metis_tac [sem_e_reln_determ] 1035 THEN1 (* Break in body *) 1036 (ntac 4 (bp_step_tac \\ fs [] \\ rw [sem_e_reln_Num]) 1037 \\ qexists_tac `(Ter (Rbreak,s''))` 1038 \\ fs [abort_def,is_rval_def,pb_sem_t_reln_Forn2] 1039 \\ metis_tac [DECIDE ``n<n+1+1:num``]) 1040 THEN1 (* For continues *) 1041 (ntac 4 (bp_step_tac \\ fs [] \\ rw [sem_e_reln_Num,is_rval_def]) 1042 \\ fs [pb_sem_t_reln_Exp] \\ disj1_tac 1043 \\ qexists_tac `Ter r2` \\ fs [] \\ rw [] 1044 THEN1 1045 (fs [AND_IMP_INTRO] \\ res_tac 1046 \\ metis_tac [DECIDE ``h' < h' + (h + 1 + 1) + 1n``]) 1047 \\ fs [abort_def,is_rval_def,pb_sem_t_reln_Forn2] 1048 \\ imp_res_tac sem_e_reln_not \\ fs[pb_sem_t_reln_Forn3] 1049 \\ qpat_x_assum `pb_sem_t_size_reln h s'' _ (Ter r)` mp_tac 1050 \\ bp_size_step_tac \\ fs [] \\ reverse (rw [Loop_def]) 1051 THEN1 (rpt disj2_tac \\ Cases_on `r` \\ fs [abort_def]) 1052 \\ disj1_tac 1053 \\ fs [AND_IMP_INTRO] \\ res_tac 1054 \\ rpt (pop_assum mp_tac \\ match_mp_tac IMP_IMP \\ conj_tac THEN1 decide_tac) 1055 \\ rw [] \\ fs [phase1_def,Loop_def]) 1056 \\ ntac 4 (bp_step_tac \\ fs [] \\ rw [sem_e_reln_Num]) 1057 \\ disj1_tac \\ rename [���abort T (Ter result)���] >> qexists_tac `Ter result` 1058 \\ Cases_on `result` \\ fs [is_rval_def,abort_def,pb_sem_t_reln_Forn2] 1059 \\ metis_tac [DECIDE ``n<n+1n+1``]) 1060 THEN1 (* For eval of exp fails *) 1061 (rename [���abort F (Ter result)���] >> Cases_on `result` \\ 1062 fs [abort_def,Loop_def] 1063 \\ ntac 3 (bp_step_tac \\ fs [] \\ rw [sem_e_reln_Num]) 1064 \\ disj1_tac >> 1065 rename [���sem_e_reln s0 e0 (r,s)���] >> 1066 qexists_tac `Ter (r,s)` \\ fs [] 1067 \\ fs [pb_sem_t_reln_Forn2,abort_def] 1068 \\ imp_res_tac sem_e_reln_not\\ fs [])); 1069end 1070 1071(* End verification in Pretty-Big-Step -- 81 lines 1072 Note: this verification does not cover divergence preservation. *) 1073 1074(* for presentation purposes: *) 1075 1076val phase1_abbrev = store_thm("phase1_abbrev", 1077 ``(phase1 (For g e t) = Loop (If g (Seq (phase1 t) (Exp e)) Break))/\ 1078 (phase1 (Dec x t) = Seq (Exp (Assign x (Num 0))) (phase1 t))``, 1079 fs [phase1_def]); 1080 1081val _ = export_theory (); 1082