1109998Smarkmopen HolKernel Parse boolLib bossLib; 2109998Smarkm 3109998Smarkmval _ = new_theory "for_nd_sem"; 4109998Smarkm 5109998Smarkm(* 6109998Smarkm 7109998SmarkmThis file defines a functional big-step semantics for the FOR language 8109998Smarkmsyntax given in for_ndScript.sml. The language has basic I/O and 9109998Smarkmnon-deterministic evaluation order. 10109998Smarkm 11109998SmarkmA simpler version of this language can be found in forScript.sml. 12109998Smarkm 13109998Smarkm*) 14109998Smarkm 15109998Smarkmopen optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory; 16109998Smarkmopen llistTheory integerTheory; 17109998Smarkmopen lprefix_lubTheory; 18109998Smarkmopen for_ndTheory; 19109998Smarkmopen lcsymtacs; 20109998Smarkm 21109998Smarkmval ect = BasicProvers.EVERY_CASE_TAC; 22109998Smarkm 23109998Smarkmval _ = temp_tight_equality (); 24109998Smarkm 25109998Smarkm(* The result of running a program. Rtimeout indicates an attempt to 26109998Smarkm loop with no clock left. Rfail indicates an undeclared variable 27109998Smarkm access or a Break not in a For. *) 28109998Smarkm 29109998Smarkmval _ = Datatype ` 30109998Smarkmr = Rval int 31109998Smarkm | Rbreak 32109998Smarkm | Rtimeout 33109998Smarkm | Rfail`; 34109998Smarkm 35109998Smarkmval r_distinct = fetch "-" "r_distinct"; 36109998Smarkmval r_11 = fetch "-" "r_11"; 37109998Smarkm 38109998Smarkmval _ = type_abbrev ("oracle", ``:(num -> 'a)``); 39109998Smarkm 40109998Smarkmval oracle_get_def = Define ` 41109998Smarkmoracle_get (f:'a oracle) = (f 0, f o ((+) 1))`; 42109998Smarkm 43109998Smarkm(* The state of the semantics. Here io_trace records all I/O that has 44109998Smarkm been done, input is the input stream, and non_det_o is an oracle 45109998Smarkm used to decide which subexpression of Add to evaluate first. *) 46109998Smarkm 47109998Smarkmval _ = Datatype ` 48109998Smarkmstate = <| store : string |-> int; clock : num; io_trace : (io_tag + bool) list; 49109998Smarkm input : char llist; non_det_o : bool oracle |>`; 50109998Smarkm 51109998Smarkmval state_component_equality = fetch "-" "state_component_equality"; 52109998Smarkm 53109998Smarkmval state_rw = Q.prove ( 54109998Smarkm`(!s c out n nd. <| store := s; clock := c; io_trace := out; input := n; non_det_o := nd |>.store = s) ��� 55109998Smarkm (!s nd. (s with non_det_o := nd).store = s.store) ��� 56109998Smarkm (!s. <| store := s.store; clock := s.clock; io_trace := s.io_trace; input := s.input; non_det_o := s.non_det_o |> = s)`, 57109998Smarkm rw [state_component_equality]); 58109998Smarkm 59109998Smarkmval permute_pair_def = Define ` 60109998Smarkmpermute_pair oracle (x,y) = 61109998Smarkm let (switch, oracle') = oracle_get oracle in 62109998Smarkm ((if switch then (y,x) else (x,y)), oracle', switch)`; 63109998Smarkm 64109998Smarkmval unpermute_pair_def = Define ` 65109998Smarkmunpermute_pair (x,y) switch = 66109998Smarkm if switch then 67109998Smarkm (y,x) 68109998Smarkm else 69109998Smarkm (x,y)`; 70109998Smarkm 71109998Smarkm(* Expression evaluation *) 72109998Smarkm 73109998Smarkmval sem_e_def = tDefine "sem_e" ` 74109998Smarkm(sem_e s (Var x) = 75109998Smarkm case FLOOKUP s.store x of 76109998Smarkm | NONE => (Rfail, s) 77109998Smarkm | SOME n => (Rval n, s)) ��� 78(sem_e s (Num num) = 79 (Rval num, s)) ��� 80(sem_e s (Add e1 e2) = 81 let ((fst_e, snd_e), nd_o, switch) = permute_pair s.non_det_o (e1, e2) in 82 case sem_e (s with <| non_det_o := nd_o; io_trace := s.io_trace ++ [INR switch] |> ) fst_e of 83 | (Rval fst_n, s1) => 84 (case sem_e s1 snd_e of 85 | (Rval snd_n, s2) => 86 let (n1, n2) = unpermute_pair (fst_n, snd_n) switch in 87 (Rval (n1 + n2), s2) 88 | r => r) 89 | r => r) ��� 90(sem_e s (Assign x e) = 91 case sem_e s e of 92 | (Rval n1, s1) => 93 (Rval n1, s1 with store := s1.store |+ (x, n1)) 94 | r => r) ��� 95(sem_e s Getchar = 96 let (v, rest) = getchar s.input in 97 (Rval v, s with <| input := rest; io_trace := s.io_trace ++ [INL (Itag v)] |>)) ��� 98(sem_e s (Putchar e) = 99 case sem_e s e of 100 | (Rval n1, s1) => (Rval n1, s1 with io_trace := s1.io_trace ++ [INL (Otag n1)]) 101 | r => r)` 102 (WF_REL_TAC `measure (e_size o SND)` >> 103 srw_tac [ARITH_ss] [] >> 104 fs [permute_pair_def, LET_THM, oracle_get_def] >> 105 ect >> 106 fs [] >> 107 srw_tac [ARITH_ss] []); 108 109val sem_e_ind = fetch "-" "sem_e_ind"; 110 111(* HOL4's definition requires a little help with the definition. In 112 particular, we need to help it see that the clock does not 113 decrease. To do this, we add a few redundant checks (check_clock) 114 to the definition of the sem_t function. These redundant checks are 115 removed later in the script. *) 116 117val sem_e_clock = Q.store_thm ("sem_e_clock", 118`!s e r s'. sem_e s e = (r, s') ��� s.clock = s'.clock`, 119 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >> 120 fs [LET_THM, permute_pair_def, oracle_get_def, unpermute_pair_def, getchar_def] >> 121 rw [] >> ect >> fs [] >> 122 ect >> fs [] >> rw []); 123 124val sem_e_store = Q.prove ( 125`!s e r s'. sem_e s e = (r, s') ��� FDOM s.store ��� FDOM s'.store`, 126 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >> 127 fs [SUBSET_DEF, LET_THM, permute_pair_def, oracle_get_def, 128 unpermute_pair_def, getchar_def] >> 129 rw [] >> ect >> fs [] >> 130 ect >> fs [] >> rw [] >> metis_tac []); 131 132val sem_e_res = Q.store_thm ("sem_e_res", 133`!s e r s'. sem_e s e = (r, s') ��� r ��� Rbreak ��� r ��� Rtimeout`, 134 ho_match_mp_tac sem_e_ind >> rw [sem_e_def] >> ect >> 135 fs [LET_THM, permute_pair_def, oracle_get_def, unpermute_pair_def, getchar_def] >> 136 rw [] >> ect >> fs [] >> 137 ect >> fs [] >> rw [] >> metis_tac []); 138 139val check_clock_def = Define ` 140check_clock s' s = 141 s' with clock := (if s'.clock ��� s.clock then s'.clock else s.clock)`; 142 143val dec_clock_def = Define ` 144dec_clock s = s with clock := s.clock - 1`; 145 146val dec_clock_store = Q.store_thm ("dec_clock_store[simp]", 147`!s. (dec_clock s).store = s.store`, 148 rw [dec_clock_def]); 149 150(* Statement evaluation -- with redundant check_clock *) 151 152val sem_t_def = tDefine "sem_t" ` 153(sem_t s (Exp e) = sem_e s e) ��� 154(sem_t s (Dec x t) = 155 sem_t (s with store := s.store |+ (x, 0)) t) ��� 156(sem_t s Break = (Rbreak, s)) ��� 157(sem_t s (Seq t1 t2) = 158 case sem_t s t1 of 159 | (Rval _, s1) => 160 sem_t (check_clock s1 s) t2 161 | r => r) ��� 162(sem_t s (If e t1 t2) = 163 case sem_e s e of 164 | (Rval n1, s1) => 165 if n1 = 0 then 166 sem_t s1 t2 167 else 168 sem_t s1 t1 169 | r => r) ��� 170(sem_t s (For e1 e2 t) = 171 case sem_e s e1 of 172 | (Rval n1, s1) => 173 if n1 = 0 then 174 (Rval 0, s1) 175 else 176 (case sem_t s1 t of 177 | (Rval _, s2) => 178 (case sem_e s2 e2 of 179 | (Rval _, s3) => 180 if s.clock ��� 0 ��� s3.clock ��� 0 then 181 sem_t (dec_clock (check_clock s3 s)) (For e1 e2 t) 182 else 183 (Rtimeout, s3) 184 | r => r) 185 | (Rbreak, s2) => 186 (Rval 0, s2) 187 | r => r) 188 | r => r)` 189 (WF_REL_TAC `(inv_image (measure I LEX measure t_size) 190 (\(s,t). (s.clock,t)))` 191 \\ REPEAT STRIP_TAC \\ TRY DECIDE_TAC 192 \\ fs [check_clock_def, dec_clock_def, LET_THM] 193 \\ rw [] 194 \\ imp_res_tac sem_e_clock 195 \\ DECIDE_TAC); 196 197val sem_t_clock = Q.store_thm ("sem_t_clock", 198`!s t r s'. sem_t s t = (r, s') ��� s'.clock ��� s.clock`, 199 ho_match_mp_tac (fetch "-" "sem_t_ind") >> 200 reverse (rpt strip_tac) >> pop_assum mp_tac >> 201 rw [Once sem_t_def] >> ect >> 202 imp_res_tac sem_e_clock >> fs [] >> 203 fs [check_clock_def, dec_clock_def, LET_THM] >> 204 TRY decide_tac >> rfs [] >> res_tac >> decide_tac); 205 206val check_clock_id = Q.store_thm ("check_clock_id", 207`!s s'. s.clock ��� s'.clock ��� check_clock s s' = s`, 208 rw [check_clock_def, state_component_equality]); 209 210val STOP_def = Define ` 211 STOP x = x`; 212 213(* Statement evaluation -- without redundant check_clock *) 214 215fun term_rewrite tms = let 216 fun f tm = ASSUME (list_mk_forall(free_vars tm,tm)) 217 in rand o concl o QCONV (REWRITE_CONV (map f tms)) end 218 219val sem_t_def_with_stop = store_thm ("sem_t_def_with_stop", 220 sem_t_def |> concl |> term_rewrite [``check_clock s3 s = s3``, 221 ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``, 222 ``sem_t (dec_clock s3) (For e1 e2 t) = 223 sem_t (dec_clock s3) (STOP (For e1 e2 t))``], 224 rpt strip_tac >> rw [Once sem_t_def,STOP_def] >> ect >> fs [] >> 225 imp_res_tac sem_t_clock >> 226 fs [dec_clock_def, LET_THM, check_clock_id] >> 227 rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >> 228 rw [state_component_equality] >> 229 rw [check_clock_def] >> 230 imp_res_tac sem_e_clock >> 231 fs [] >> `F` by decide_tac); 232 233val sem_t_def = 234 save_thm("sem_t_def",REWRITE_RULE [STOP_def] sem_t_def_with_stop); 235 236(* We also remove the redundant checks from the induction theorem. *) 237 238val sem_t_ind = store_thm ("sem_t_ind", 239 fetch "-" "sem_t_ind" 240 |> concl |> term_rewrite [``check_clock s3 s = s3``, 241 ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``], 242 ntac 2 strip_tac >> 243 ho_match_mp_tac (fetch "-" "sem_t_ind") >> rw [] >> 244 first_x_assum match_mp_tac >> 245 rw [] >> fs [] >> res_tac >> 246 imp_res_tac sem_t_clock >> 247 imp_res_tac sem_e_clock >> 248 fs [dec_clock_def, check_clock_id, LET_THM] >> 249 first_x_assum match_mp_tac >> 250 decide_tac); 251 252(* The top-level semantics defines what is externally observable. *) 253 254val init_st_def = Define ` 255init_st c nd i = 256 <| store := FEMPTY; clock := c; input := i; io_trace := []; non_det_o := nd |>`; 257 258(* There can be many observable behaviours because the semantics is 259 non-deterministic. *) 260 261val semantics_with_nd_def = Define ` 262(semantics_with_nd t input (Terminate io_trace) = 263 (* Terminate when there is a clock and some non-determinism oracle 264 that gives a value result *) 265 ?c nd i s. 266 sem_t (init_st c nd input) t = (Rval i, s) ��� 267 s.io_trace = io_trace) ��� 268(semantics_with_nd t input Crash = 269 (* Crash when there is a clock that gives a non-value, non-timeout 270 result. *) 271 ?c nd r s. 272 sem_t (init_st c nd input) t = (r, s) ��� 273 (r = Rbreak ��� r = Rfail)) ��� 274(semantics_with_nd t input (Diverge io_trace) = 275 ?nd. 276 (!c. ?s. sem_t (init_st c nd input) t = (Rtimeout, s)) ��� 277 lprefix_lub {fromList (SND (sem_t (init_st c nd input) t)).io_trace | c | T} io_trace)`; 278 279val semantics_def = Define ` 280(semantics t input (Terminate io_trace) = 281 (* Terminate when there is a clock and some non-determinism oracle 282 that gives a value result *) 283 ?c nd i s. 284 sem_t (init_st c nd input) t = (Rval i, s) ��� 285 FILTER ISL s.io_trace = io_trace) ��� 286(semantics t input Crash = 287 (* Crash when there is a clock that gives a non-value, non-timeout 288 result. *) 289 ?c nd r s. 290 sem_t (init_st c nd input) t = (r, s) ��� 291 (r = Rbreak ��� r = Rfail)) ��� 292(semantics t input (Diverge io_trace) = 293 ?nd. 294 (!c. ?s. sem_t (init_st c nd input) t = (Rtimeout, s)) ��� 295 lprefix_lub {fromList (FILTER ISL (SND (sem_t (init_st c nd input) t)).io_trace) | c | T} io_trace)`; 296 297 298(* === Misc lemmas === *) 299 300val sem_t_store = Q.prove ( 301`!s t r s'. sem_t s t = (r, s') ��� FDOM s.store ��� FDOM s'.store`, 302 ho_match_mp_tac sem_t_ind >> 303 rpt conj_tac >> 304 rpt gen_tac >> 305 DISCH_TAC >> 306 ONCE_REWRITE_TAC [sem_t_def] 307 >- (fs [sem_t_def] >> 308 metis_tac [sem_e_store]) 309 >- (fs [sem_t_def] >> 310 metis_tac []) 311 >- (fs [sem_t_def] >> 312 metis_tac []) 313 >- (ect >> 314 rw [] >> 315 metis_tac [sem_e_store, SUBSET_DEF]) 316 >- (ect >> 317 rw [] >> 318 metis_tac [sem_e_store, SUBSET_DEF]) 319 >- (Cases_on `sem_e s e1` >> 320 fs [] >> 321 Cases_on `q` >> 322 reverse (fs []) 323 >- (Cases_on `i = 0` >> 324 fs [] 325 >- metis_tac [sem_e_store, SUBSET_TRANS] >> 326 Cases_on `sem_t r t` >> 327 fs [] >> 328 Cases_on `q` >> 329 reverse (fs []) 330 >- (ect >> 331 fs [] >> 332 rw [] >> 333 rfs [] >> 334 metis_tac [sem_e_store, SUBSET_TRANS]) >> 335 metis_tac [sem_e_store, SUBSET_TRANS]) >> 336 metis_tac [sem_e_store, SUBSET_TRANS])); 337 338val sem_for_not_break = Q.store_thm ("sem_for_not_break", 339`!s t' t e1 e2 s' r. 340 sem_t s t' = (r, s') ��� 341 t' = For e1 e2 t 342 ��� 343 r ��� Rbreak`, 344 ho_match_mp_tac sem_t_ind >> 345 reverse (rpt conj_tac) 346 >- (rw [] >> 347 rw [sem_t_def_with_stop] >> 348 ect >> 349 fs [] >> 350 imp_res_tac sem_e_res >> 351 fs [STOP_def]) >> 352 rw [sem_t_def_with_stop] >> 353 ect >> 354 fs [] >> 355 imp_res_tac sem_e_res >> 356 fs []); 357 358 359(* === A simple type checker and its soundness === *) 360 361val type_permute_pair_lem = Q.prove ( 362`!s s1 e1 e2 fst_e snd_e new_nd. 363 type_e s e1 ��� 364 type_e s e2 ��� 365 permute_pair s1.non_det_o (e1,e2) = ((fst_e,snd_e),new_nd) 366 ��� 367 type_e s fst_e ��� 368 type_e s snd_e`, 369 rw [permute_pair_def, LET_THM, oracle_get_def] >> 370 rw []); 371 372val type_sound_e = Q.prove ( 373`!s1 e s. 374 type_e s e ��� s ��� FDOM s1.store 375 ��� 376 ?r s1'. 377 r ��� Rfail ��� 378 sem_e s1 e = (r, s1')`, 379 ho_match_mp_tac (fetch "-" "sem_e_ind") >> 380 rw [sem_e_def, type_e_def] 381 >- (ect >> 382 fs [FLOOKUP_DEF, SUBSET_DEF] >> 383 rw [] >> 384 metis_tac []) 385 >- (`?fst_e snd_e new_nd switch. permute_pair s1.non_det_o (e1, e2) = ((fst_e, snd_e), new_nd, switch)` 386 by metis_tac [pair_CASES] >> 387 fs [] >> 388 `type_e s fst_e ��� type_e s snd_e` by metis_tac [type_permute_pair_lem] >> 389 res_tac >> 390 fs [] >> 391 rw [] >> 392 `type_e (FDOM s1'.store) snd_e` 393 by (rw [] >> 394 match_mp_tac type_weakening_e >> 395 qexists_tac `s` >> 396 rw [] >> 397 imp_res_tac sem_e_store >> 398 fs [] >> 399 metis_tac [SUBSET_TRANS]) >> 400 fs [] >> 401 Cases_on `r` >> 402 fs [] >> 403 first_x_assum (fn th => pop_assum (fn th' => assume_tac (MATCH_MP (SIMP_RULE (srw_ss()) [GSYM AND_IMP_INTRO] th) th'))) >> 404 fs [state_rw] >> 405 ect >> 406 rw [] >> 407 fs [SUBSET_DEF, unpermute_pair_def] >> 408 rw []) >> 409 fs [getchar_def] >> 410 ect >> 411 fs [LET_THM] >> 412 rw [] >> 413 metis_tac []); 414 415(* Have to use sem_t_ind, and not type_t_ind or t_induction. This is 416 different from small-step-based type soundness *) 417 418val type_sound_t = Q.prove ( 419`!s1 t in_for s. 420 type_t in_for s t ��� s ��� FDOM s1.store 421 ��� 422 ?r s1'. 423 r ��� Rfail ��� 424 (~in_for ��� r ��� Rbreak) ��� 425 sem_t s1 t = (r, s1')`, 426 ho_match_mp_tac sem_t_ind >> 427 rw [type_t_def] >> 428 ONCE_REWRITE_TAC [sem_t_def] >> 429 rw [] 430 >- (imp_res_tac type_sound_e >> 431 rw [state_rw] >> 432 metis_tac [sem_e_res]) 433 >- (res_tac >> 434 fs [SUBSET_DEF]) 435 >- (res_tac >> 436 rw [] >> 437 Cases_on `r'` >> 438 rw [] >> 439 fs [] >> 440 rw [] >> 441 pop_assum match_mp_tac >> 442 metis_tac [type_weakening_t, sem_t_store]) 443 >- (imp_res_tac type_sound_e >> 444 rw [state_rw] >> 445 rw [] >> 446 Cases_on `r` >> 447 fs [] 448 >- (Cases_on `i = 0` >> 449 fs [] >> 450 first_x_assum match_mp_tac >> 451 metis_tac [type_weakening_t, sem_e_store]) 452 >- metis_tac [sem_e_res]) 453 >- (imp_res_tac type_sound_e >> 454 rw [state_rw] >> 455 reverse (Cases_on `r'''`) >> 456 fs [] >> 457 Cases_on `i = 0` >> 458 fs [] >> 459 rw [] 460 >- metis_tac [sem_e_res] 461 >- metis_tac [sem_e_res] >> 462 rfs [] >> 463 `type_t T (FDOM s1''.store) t` 464 by (rw [] >> 465 match_mp_tac type_weakening_t >> 466 metis_tac [sem_e_store, sem_t_store, SUBSET_TRANS, state_rw]) >> 467 res_tac >> 468 fs [] >> 469 Cases_on `r'` >> 470 rw [] >> 471 fs [] >> 472 rw [] >> 473 `type_e (FDOM s1'''.store) e2` 474 by (rw [] >> 475 match_mp_tac type_weakening_e >> 476 metis_tac [sem_e_store, sem_t_store, SUBSET_TRANS, state_rw]) >> 477 imp_res_tac type_sound_e >> 478 first_x_assum (qspec_then `s1'''` mp_tac) >> 479 rw [] >> 480 rw [state_rw] >> 481 rw [] >> 482 Cases_on `r'''''` >> 483 rw [] >> 484 fs [] 485 >- (first_x_assum match_mp_tac >> 486 qexists_tac `s` >> 487 rw [] >> 488 imp_res_tac sem_e_store >> 489 imp_res_tac sem_t_store >> 490 metis_tac [SUBSET_TRANS]) >> 491 metis_tac [sem_e_res])); 492 493val type_soundness = Q.store_thm ("type_soundness", 494`!t input. type_t F {} t ��� Crash ��� semantics_with_nd t input`, 495 rw [IN_DEF, semantics_with_nd_def] >> 496 imp_res_tac type_sound_t >> 497 fs [] >> 498 first_x_assum (qspec_then `init_st c nd input` assume_tac) >> 499 fs [] >> 500 metis_tac []); 501 502val _ = export_theory (); 503