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