1open HolKernel boolLib bossLib Parse; 2open integerTheory stringTheory alistTheory listTheory rich_listTheory llistTheory pred_setTheory relationTheory; 3open pairTheory optionTheory finite_mapTheory arithmeticTheory pathTheory; 4open path_auxTheory simple_traceTheory lprefix_lubTheory; 5open for_ndTheory; 6 7val _ = set_trace "Goalstack.print_goal_at_top" 0; 8val _ = ParseExtras.temp_tight_equality(); 9 10val _ = new_theory "oracleSem"; 11 12val lfilter_map_thm = Q.store_thm ("lfilter_map_thm", 13`(lfilter_map f [||] = [||]) ��� 14 (lfilter_map f (x:::l) = 15 case f x of 16 | NONE => lfilter_map f l 17 | SOME y => y:::lfilter_map f l)`, 18 rw [lfilter_map_def] >> 19 every_case_tac >> 20 fs []); 21 22 (* 23val _ = Datatype ` 24 io_result = 25 | Terminate ('a list) 26 | Diverge ('a llist) 27 | Crash`; 28 *) 29 30val _ = type_abbrev ("oracle", ``:num -> 'st -> 'v -> 'st # 'v``); 31 32val _ = Datatype ` 33 fbs_res = 34 Timeout 35 | Error 36 | Val 'a`; 37 38val _ = Datatype ` 39 ofbs = <| eval : 'st -> 'env -> 'prog -> 'st # 'v fbs_res; 40 init_st : 'o -> 'st; 41 init_env : 'env; 42 set_clock : num -> 'st -> 'st; 43 get_clock : 'st -> num; 44 get_oracle_events : 'st -> 'a list |>`; 45 46val eval_with_clock_def = Define ` 47 eval_with_clock sem c st p = 48 sem.eval (sem.set_clock c st) sem.init_env p`; 49 50val ofbs_sem_def = Define ` 51 (ofbs_sem sem p (Terminate io_list) ��� 52 ?oracle k st r. 53 eval_with_clock sem k (sem.init_st oracle) p = (st, r) ��� 54 r ��� Timeout ��� r ��� Error ��� 55 sem.get_oracle_events st = io_list) ��� 56 (ofbs_sem sem p (Diverge io_trace) ��� 57 ?oracle. 58 (!k. ?st. eval_with_clock sem k (sem.init_st oracle) p = (st, Timeout)) ��� 59 lprefix_lub {fromList (sem.get_oracle_events (FST (eval_with_clock sem k (sem.init_st oracle) p))) | k | T} io_trace) ��� 60 (ofbs_sem sem p Crash ��� 61 ?oracle k st. 62 eval_with_clock sem k (sem.init_st oracle) p = (st, Error))`; 63 64val _ = Datatype ` 65 osmall = <| step : 'st -> 'st option; 66 is_result : 'st -> bool; 67 load : 'o -> 'prog -> 'st; 68 unload : 'st -> 'a list |>`; 69 70val step_rel_def = Define ` 71 step_rel sem = (\s1 s2. sem.step s1 = SOME s2)^*`; 72 73val osmall_sem_def = Define ` 74 (osmall_sem sem p (Terminate io_list) ��� 75 ?oracle s. 76 step_rel sem (sem.load oracle p) s ��� sem.step s = NONE ��� sem.is_result s ��� 77 sem.unload s = io_list) ��� 78 (osmall_sem sem p (Diverge io_trace) ��� 79 ?oracle. 80 (!s. step_rel sem (sem.load oracle p) s ��� sem.step s ��� NONE) ��� 81 lprefix_lub {fromList (sem.unload s) | s | step_rel sem (sem.load oracle p) s} io_trace) ��� 82 (osmall_sem sem p Crash ��� 83 ?oracle s. 84 step_rel sem (sem.load oracle p) s ��� sem.step s = NONE ��� ��sem.is_result s)`; 85 86val is_prefix_pres = Q.prove ( 87`!sem_s. 88 (!s1 s2. sem_s.step s1 = SOME s2 ��� isPREFIX (sem_s.unload s1) (sem_s.unload s2)) 89 ��� 90 !s1 s2. 91 (��s1 s2. sem_s.step s1 = SOME s2)^* s1 s2 92 ��� 93 isPREFIX (sem_s.unload s1) (sem_s.unload s2)`, 94 rpt gen_tac >> 95 DISCH_TAC >> 96 ho_match_mp_tac RTC_INDUCT >> 97 rw [] >> 98 res_tac >> 99 metis_tac [IS_PREFIX_TRANS]); 100 101val small_chain_def = Define ` 102 small_chain sem_s oracle p = 103 {fromList (sem_s.unload s) | s | step_rel sem_s (sem_s.load oracle p) s}`; 104 105val fbs_chain_def = Define ` 106 fbs_chain sem_f oracle p = 107 {fromList (sem_f.get_oracle_events (FST (eval_with_clock sem_f k (sem_f.init_st oracle) p))) | k | T}`; 108 109val small_chain_thm = Q.prove ( 110`!sem_s oracle p. 111 (���s1 s2. sem_s.step s1 = SOME s2 ��� sem_s.unload s1 ��� sem_s.unload s2) 112 ��� 113 lprefix_chain (small_chain sem_s oracle p)`, 114 rw [small_chain_def, lprefix_chain_def, LPREFIX_def] >> 115 rw [from_toList] >> 116 fs [step_rel_def, check_trace_thm] >> 117 `LENGTH tr ��� LENGTH tr' ��� LENGTH tr' ��� LENGTH tr` by decide_tac 118 >- ( 119 qabbrev_tac `tr'' = DROP (LENGTH tr - 1) tr'` >> 120 `LAST tr = HD tr''` by metis_tac [check_trace_twice_suff] >> 121 `LENGTH tr - 1 < LENGTH tr' ��� LENGTH tr - 1 ��� LENGTH tr'` by (simp [] >> Cases_on `tr'` >> fs []) >> 122 `check_trace sem_s.step tr''` by metis_tac [check_trace_drop] >> 123 `LAST tr' = LAST tr''` by metis_tac [last_drop] >> 124 rw [] >> 125 `tr'' ��� []` by (unabbrev_all_tac >> fs [DROP_EQ_NIL] >> decide_tac) >> 126 `(��s1 s2. sem_s.step s1 = SOME s2)^* (HD tr'') (LAST tr'')` by metis_tac [check_trace_thm] >> 127 metis_tac [is_prefix_pres]) 128 >- ( 129 qabbrev_tac `tr'' = DROP (LENGTH tr' - 1) tr` >> 130 `LAST tr' = HD tr''` by metis_tac [check_trace_twice_suff] >> 131 `LENGTH tr' - 1 < LENGTH tr ��� LENGTH tr' - 1 ��� LENGTH tr` by (simp [] >> Cases_on `tr` >> fs []) >> 132 `check_trace sem_s.step tr''` by metis_tac [check_trace_drop] >> 133 `LAST tr = LAST tr''` by metis_tac [last_drop] >> 134 rw [] >> 135 `tr'' ��� []` by (unabbrev_all_tac >> fs [DROP_EQ_NIL] >> decide_tac) >> 136 `(��s1 s2. sem_s.step s1 = SOME s2)^* (HD tr'') (LAST tr'')` by metis_tac [check_trace_thm] >> 137 metis_tac [is_prefix_pres])); 138 139val fbs_chain_thm = Q.prove ( 140`!sem_f oracle p. 141 (!k1 k2 p. k1 ��� k2 ��� 142 sem_f.get_oracle_events (FST (eval_with_clock sem_f k1 (sem_f.init_st oracle) p)) ��� 143 sem_f.get_oracle_events (FST (eval_with_clock sem_f k2 (sem_f.init_st oracle) p))) 144 ��� 145 lprefix_chain (fbs_chain sem_f oracle p)`, 146 rw [fbs_chain_def, lprefix_chain_def, LPREFIX_def] >> 147 rw [from_toList] >> 148 `k ��� k' ��� k' ��� k` by decide_tac >> 149 metis_tac []); 150 151val osmall_fbs_equiv_lem = Q.prove ( 152`!sem_s sem_f oracle p f. 153 lprefix_chain (fbs_chain sem_f oracle p) ��� 154 lprefix_chain (small_chain sem_s oracle p) ��� 155 (���s1 s2. sem_s.step s1 = SOME s2 ��� sem_s.unload s1 ��� sem_s.unload s2) ��� 156 unbounded f ��� 157 (���c p st. 158 eval_with_clock sem_f c (sem_f.init_st oracle) p = (st,Timeout) ��� 159 ���tr. 160 f c ��� LENGTH tr ��� tr ��� [] ��� HD tr = sem_s.load oracle p ��� 161 check_trace sem_s.step tr ��� 162 sem_f.get_oracle_events st = sem_s.unload (LAST tr)) ��� 163 (���k. ���st. eval_with_clock sem_f k (sem_f.init_st oracle) p = (st,Timeout)) 164 ��� 165 equiv_lprefix_chain (fbs_chain sem_f oracle p) (small_chain sem_s oracle p)`, 166 rw [] >> 167 `!ll. ll ��� small_chain sem_s oracle p ��� LFINITE ll` by ( 168 rw [small_chain_def] >> 169 rw [LFINITE_fromList]) >> 170 rw [equiv_lprefix_chain_thm2] 171 >- ( 172 fs [fbs_chain_def] >> 173 last_x_assum (qspecl_then [`k`, `p`] mp_tac) >> 174 Cases_on `eval_with_clock sem_f k (sem_f.init_st oracle) p` >> 175 rw [] >> 176 first_x_assum (qspec_then `k` mp_tac) >> 177 simp [small_chain_def] >> 178 rw [PULL_EXISTS, step_rel_def, check_trace_thm] >> 179 qexists_tac `tr` >> 180 rw [] 181 >- metis_tac [] >> 182 rfs [LNTH_fromList] >> 183 rw [] >> 184 metis_tac []) 185 >- ( 186 fs [small_chain_def] >> 187 rw [] >> 188 fs [step_rel_def, check_trace_thm] >> 189 `?c. LENGTH tr < f c` by (fs [unbounded_def] >> decide_tac) >> 190 last_x_assum (qspecl_then [`c`, `p`] mp_tac) >> 191 rw [] >> 192 Cases_on `eval_with_clock sem_f c (sem_f.init_st oracle) p` >> 193 fs [] >> 194 first_x_assum (qspec_then `c` assume_tac) >> 195 rfs [] >> 196 fs [] >> 197 rw [] >> 198 `LENGTH tr < LENGTH tr'` by decide_tac >> 199 simp [fbs_chain_def, PULL_EXISTS, llist_shorter_fromList] >> 200 qexists_tac `c` >> 201 qabbrev_tac `tr'' = DROP (LENGTH tr - 1) tr'` >> 202 `LAST tr = HD tr''` by metis_tac [check_trace_twice_suff, LESS_OR_EQ] >> 203 `LENGTH tr - 1 < LENGTH tr' ��� LENGTH tr - 1 ��� LENGTH tr'` by (simp [] >> Cases_on `tr` >> fs []) >> 204 `check_trace sem_s.step tr''` by metis_tac [check_trace_drop] >> 205 `LAST tr' = LAST tr''` by metis_tac [last_drop] >> 206 `tr'' ��� []` by (unabbrev_all_tac >> fs [DROP_EQ_NIL] >> decide_tac) >> 207 `(��s1 s2. sem_s.step s1 = SOME s2)^* (HD tr'') (LAST tr'')` by metis_tac [check_trace_thm] >> 208 imp_res_tac is_prefix_pres >> 209 fs [] >> 210 metis_tac [IS_PREFIX_LENGTH, LESS_TRANS, LESS_OR_EQ])); 211 212val equiv_lprefix_chain_sym = Q.prove ( 213`!ls1 ls2. equiv_lprefix_chain ls1 ls2 ��� equiv_lprefix_chain ls2 ls1`, 214 rw [equiv_lprefix_chain_def] >> 215 metis_tac []); 216 217val osmall_fbs_equiv = Q.store_thm ("osmall_fbs_equiv", 218`!sem_f sem_s. 219 (���s1 s2. sem_s.step s1 = SOME s2 ��� sem_s.unload s1 ��� sem_s.unload s2) ��� 220 (!oracle k1 k2 p. k1 ��� k2 ��� 221 sem_f.get_oracle_events (FST (eval_with_clock sem_f k1 (sem_f.init_st oracle) p)) ��� 222 sem_f.get_oracle_events (FST (eval_with_clock sem_f k2 (sem_f.init_st oracle) p))) ��� 223 (?f. 224 unbounded f ��� 225 !oracle c p st. 226 eval_with_clock sem_f c (sem_f.init_st oracle) p = (st, Timeout) ��� 227 ?tr. f c ��� LENGTH tr ��� tr ��� [] ��� HD tr = sem_s.load oracle p ��� check_trace sem_s.step tr ��� 228 sem_f.get_oracle_events st = sem_s.unload (LAST tr)) ��� 229 (!oracle c p st r. 230 eval_with_clock sem_f c (sem_f.init_st oracle) p = (st,r) ��� r ��� Timeout ��� 231 ?r'. step_rel sem_s (sem_s.load oracle p) r' ��� sem_s.step r' = NONE ��� 232 (r = Error ��� ~sem_s.is_result r') ��� 233 (r ��� Error ��� sem_f.get_oracle_events st = sem_s.unload r')) 234 ��� 235 !p r. 236 ofbs_sem sem_f p r ��� osmall_sem sem_s p r`, 237 rw [] >> 238 Cases_on `r` >> 239 rw [osmall_sem_def, ofbs_sem_def] >> 240 eq_tac >> 241 simp [] 242 >- metis_tac [] 243 >- ( 244 fs [step_rel_def] >> 245 rw [] >> 246 qexists_tac `oracle` >> 247 Cases_on `?k st r. eval_with_clock sem_f k (sem_f.init_st oracle) p = (st,r) ��� r ��� Timeout` >> 248 fs [] 249 >- ( 250 MAP_EVERY qexists_tac [`k`, `st`, `r`] >> 251 simp [] >> 252 res_tac >> 253 `r' = s` by metis_tac [step_rel_determ] >> 254 fs []) 255 >- ( 256 fs [check_trace_thm] >> 257 `?c. LENGTH tr < f c` by (fs [unbounded_def] >> decide_tac) >> 258 last_x_assum (qspecl_then [`oracle`, `c`, `p`] mp_tac) >> 259 Cases_on `eval_with_clock sem_f c (sem_f.init_st oracle) p` >> 260 simp [] >> 261 `r = Timeout` by metis_tac [] >> 262 rw [] >> 263 `LENGTH tr < LENGTH tr'` by decide_tac >> 264 metis_tac [trace_extends])) 265 >- ( 266 DISCH_TAC >> 267 fs [] >> 268 simp [] >> 269 qexists_tac `oracle` >> 270 conj_asm1_tac 271 >- ( 272 simp [step_rel_def, check_trace_thm, PULL_EXISTS, PULL_FORALL] >> 273 gen_tac >> 274 rw [] >> 275 `?c. LENGTH tr < f c` by (fs [unbounded_def] >> decide_tac) >> 276 first_x_assum (qspec_then `c` mp_tac) >> 277 last_x_assum (qspecl_then [`oracle`, `c`, `p`] mp_tac) >> 278 rpt DISCH_TAC >> 279 fs [] >> 280 fs [] >> 281 `LENGTH tr < LENGTH tr'` by decide_tac >> 282 rw [] >> 283 metis_tac [trace_extends]) 284 >- ( 285 fs [GSYM fbs_chain_def, GSYM small_chain_def] >> 286 match_mp_tac lprefix_lub_new_chain >> 287 qexists_tac `fbs_chain sem_f oracle p` >> 288 metis_tac [fbs_chain_thm, small_chain_thm,osmall_fbs_equiv_lem, equiv_lprefix_chain_sym])) 289 >- ( 290 DISCH_TAC >> 291 fs [] >> 292 simp [PULL_FORALL] >> 293 qexists_tac `oracle` >> 294 gen_tac >> 295 Cases_on `?c st r. eval_with_clock sem_f c (sem_f.init_st oracle) p = (st,r) ��� r ��� Timeout` >> 296 fs [] >> 297 rw [] 298 >- metis_tac [] 299 >- metis_tac [] 300 >- ( 301 first_x_assum (qspec_then `k` mp_tac) >> 302 Cases_on `eval_with_clock sem_f k (sem_f.init_st oracle) p` >> 303 rw []) 304 >- ( 305 fs [GSYM fbs_chain_def, GSYM small_chain_def] >> 306 match_mp_tac lprefix_lub_new_chain >> 307 qexists_tac `small_chain sem_s oracle p` >> 308 metis_tac [pair_CASES, fbs_chain_thm, small_chain_thm,osmall_fbs_equiv_lem, equiv_lprefix_chain_sym])) 309 >- metis_tac [fetch "-" "fbs_res_distinct"] 310 >- ( 311 fs [step_rel_def] >> 312 rw [] >> 313 qexists_tac `oracle` >> 314 Cases_on `?k st r. eval_with_clock sem_f k (sem_f.init_st oracle) p = (st,r) ��� r ��� Timeout` >> 315 fs [] 316 >- ( 317 MAP_EVERY qexists_tac [`k`, `st`] >> 318 simp [] >> 319 res_tac >> 320 `r' = s` by metis_tac [step_rel_determ] >> 321 fs []) 322 >- ( 323 fs [check_trace_thm] >> 324 `?c. LENGTH tr < f c` by (fs [unbounded_def] >> decide_tac) >> 325 last_x_assum (qspecl_then [`oracle`, `c`, `p`] mp_tac) >> 326 Cases_on `eval_with_clock sem_f c (sem_f.init_st oracle) p` >> 327 simp [] >> 328 `r = Timeout` by metis_tac [] >> 329 rw [] >> 330 `LENGTH tr < LENGTH tr'` by decide_tac >> 331 metis_tac [trace_extends]))); 332 333val same_result_def = Define ` 334 (same_result sem_f sem_s (st, Val a) s ��� 335 sem_f.get_oracle_events st = sem_s.unload s ��� 336 sem_s.is_result s ��� 337 sem_s.step s = NONE) ��� 338 (same_result sem_f sem_s (st, Error) s ��� 339 ��sem_s.is_result s ��� 340 sem_s.step s = NONE) ��� 341 (same_result sem_f sem_s (st, Timeout) s ��� 342 sem_f.get_oracle_events st = sem_s.unload s ��� 343 ?s'. sem_s.step s = SOME s')`; 344 345val osmall_fbs_equiv2 = Q.store_thm ("osmall_fbs_equiv2", 346`!sem_f sem_s. 347 (���s1 s2. sem_s.step s1 = SOME s2 ��� sem_s.unload s1 ��� sem_s.unload s2) ��� 348 (!oracle k1 k2 p. k1 ��� k2 ��� 349 sem_f.get_oracle_events (FST (eval_with_clock sem_f k1 (sem_f.init_st oracle) p)) ��� 350 sem_f.get_oracle_events (FST (eval_with_clock sem_f k2 (sem_f.init_st oracle) p))) ��� 351 (!oracle c p. 352 SND (eval_with_clock sem_f c (sem_f.init_st oracle) p) = Timeout ��� 353 sem_f.get_clock (FST (eval_with_clock sem_f c (sem_f.init_st oracle) p)) = 0) ��� 354 (?f. 355 unbounded f ��� 356 !oracle c p st r. 357 eval_with_clock sem_f c (sem_f.init_st oracle) p = (st, r) ��� 358 ?tr. f (c - sem_f.get_clock st) ��� LENGTH tr ��� tr ��� [] ��� HD tr = sem_s.load oracle p ��� check_trace sem_s.step tr ��� 359 same_result sem_f sem_s (st, r) (LAST tr)) 360 ��� 361 !p r. 362 ofbs_sem sem_f p r ��� osmall_sem sem_s p r`, 363 rpt gen_tac >> 364 DISCH_TAC >> 365 match_mp_tac osmall_fbs_equiv >> 366 rw [] 367 >- ( 368 qexists_tac `f` >> 369 rw [] >> 370 res_tac >> 371 fs [same_result_def] >> 372 qexists_tac `tr` >> 373 simp [] >> 374 last_x_assum (qspecl_then [`oracle`, `c`, `p`] mp_tac) >> 375 rw [] >> 376 fs []) 377 >- ( 378 res_tac >> 379 rw [step_rel_def, check_trace_thm] >> 380 reverse (Cases_on `r`) >> 381 fs [same_result_def] >> 382 metis_tac [])); 383 384val _ = export_theory (); 385