open HolKernel Parse boolLib open bossLib simpLib open boolSimps infix THEN THENC THENL ++ ORELSE |-> ORELSE_TCL infix 8 by val host_redn_cases = TNet_hostLTSTheory.host_redn_cases val retType_def = TNet_LIBinterfaceTheory.retType_def val host_ok_def = TNet_oksTheory.host_ok_def val socket_ok_def = TNet_oksTheory.socket_ok_def val socket_srcdest_ok_def = TNet_oksTheory.socket_srcdest_ok_def val sockfds_thm = TNet_oksTheory.sockfds_thm val SPECIFICATION = pred_setTheory.SPECIFICATION val GSPECIFICATION = pred_setTheory.GSPECIFICATION val scs_functions_def = TNet_auxfnsTheory.scs_functions_def val Sock_def = TNet_typesTheory.Sock_def val sock_with_fd_def = TNet_oksTheory.sock_with_fd_def open TNet_host_theorem1Theory fun srw_ss() = BasicProvers.get_srw_ss() val undo_abbrevs = REPEAT (FIRST_X_ASSUM (SUBST_ALL_TAC o SYM o assert (is_var o rhs o concl))) fun dest_negeq t = let val t0 = dest_neg t in (lhs t0, rhs t0) end val QCONTR_TAC = TRY (FIRST_X_ASSUM (MP_TAC o assert (op = o dest_negeq o concl)) THEN REWRITE_TAC []) val _ = BasicProvers.augment_srw_ss [ rewrites [finite_mapTheory.FAPPLY_FUPDATE, TNet_typesTheory.neq_def, TNet_typesTheory.NOTIN_def] ] val _ = new_theory "TNet_host_theorem2"; val OL_ss = let open TNet_typesTheory in rewrites [FAIL'_def, OK'_def, OK'_bool_def, OK'_error_def, OK'_errorlift_def, neq_def, OK'_fd_def, OK'_fdlistpair_def, OK'_getifaddrs_ret_def, OK'_ip_def, OK'_ipportlift_def, OK'_msglift_def, OK'_tid_def, OK'_one_def, OK'_option_def, OK'_pair_def, OK'_port_def, TLang_typing_thm, TNet_oksTheory.not_in_ifds_def] end val PRED_SET_ss = pred_setSimps.PRED_SET_ss val ARITH_ss = numSimps.ARITH_ss val FC_accessors = prove( ``!FC ifds tid t s. F_context FC ==> ((FC(ifds,tid,t,s)).ts = FUPDATE (fc_ts FC) (tid,t)) /\ ((FC(ifds,tid,t,s)).ifds = ifds) /\ ((FC(ifds,tid,t,s)).oq = fc_oq FC) /\ ((FC(ifds,tid,t,s)).oqf = fc_oqf FC) /\ ((FC(ifds,tid,t,s)).s = fc_sc FC s)``, SRW_TAC [][TNet_auxfnsTheory.FC_functions_def]); val FC_SC_OK = prove( ``!FC. F_context FC ==> socklist_context (fc_sc FC)``, SRW_TAC [][TNet_auxfnsTheory.FC_functions_def]); val SC_MEM = prove( ``!SC. socklist_context SC ==> !s. MEM s (SC s)``, SRW_TAC [][scs_functions_def]); val htsType_def = Define` (htsType Run = {}) /\ (htsType Zombie = {}) /\ (htsType Delay2 = {TLty_err TLty_one}) /\ (htsType (Ret t) = tlang_typing t) /\ (htsType (Sendto2 _) = { TLty_err TLty_one }) /\ (htsType (Recvfrom2 _) = { TLty_err (TLty_pair(TLty_ip, TLty_pair(TLty_lift TLty_port, TLty_string))) }) /\ (htsType (Select2 _) = { TLty_err (TLty_pair(TLty_list TLty_fd, TLty_list TLty_fd)) }) /\ (htsType (Print2 _) = { TLty_err TLty_one }) /\ (htsType Exit = { TLty_void })`; val outroute_in_ifds = prove( ``!ifds. ifd_set_ok ifds ==> !i i1. i1 IN outroute(ifds,i) ==> i1 IN ifds``, SRW_TAC [PRED_SET_ss] [TNet_oksTheory.in_ifds_def, TNet_oksTheory.ifd_set_ok_def, TNet_auxfnsTheory.outroute_def, pred_setTheory.GSPECIFICATION] THENL [ FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE EXISTS_UNIQUE_CONV) THEN PROVE_TAC [TNet_oksTheory.localhost_IN_LOOPBACK], PROVE_TAC [] ]); val EVERY_SC = prove( ``!P s. socklist_context SC ==> (EVERY P (SC s) = EVERY P (scs1 SC) /\ P s /\ EVERY P (scs2 SC))``, SIMP_TAC (srw_ss()) [scs_functions_def]); val ps_lemma = prove( ``{x} y = (y = x)``, CONV_TAC (LHS_CONV (REWR_CONV (GSYM SPECIFICATION))) THEN SIMP_TAC (std_ss ++ PRED_SET_ss) []); val length_SC = prove( ``!SC s. socklist_context SC ==> (LENGTH (SC s) = SUC (LENGTH (scs1 SC) + LENGTH (scs2 SC)))``, SRW_TAC [ARITH_ss] [scs_functions_def]); val sockfds_SC = prove( ``!SC s. socklist_context SC ==> (sockfds (SC s) = s.fd INSERT (sockfds (scs1 SC) UNION sockfds (scs2 SC)))``, SRW_TAC [ARITH_ss] [scs_functions_def, sockfds_thm] THEN PROVE_TAC [pred_setTheory.UNION_COMM, pred_setTheory.INSERT_UNION_EQ]); val socket_srcdest_ok_thm = prove( ``!ifds i1 p1 i2 ps2. socket_srcdest_ok ifds (NONE,NONE,NONE,NONE) /\ socket_srcdest_ok ifds (NONE,SOME p1,NONE,NONE) /\ (socket_srcdest_ok ifds (SOME i1, SOME p1, NONE, NONE) = i1 IN ifds) /\ (socket_srcdest_ok ifds (SOME i1, SOME p1, SOME i2, ps2) = i1 IN ifds)``, SRW_TAC [] [socket_srcdest_ok_def]); val new_ps1_socket_srcdest_ok = prove( ``!ifds is1 ps1 p1 is2 ps2. socket_srcdest_ok ifds (is1,ps1,is2,ps2) ==> socket_srcdest_ok ifds (is1,SOME p1,is2,ps2)``, SRW_TAC [] [socket_srcdest_ok_def]); val ifd_set_ok_MARTIAN = prove( ``ifd_set_ok ifds ==> (i IN ifds ==> ~(i IN MARTIAN)) /\ (i IN outroute(ifds,j) ==> ~(i IN MARTIAN))``, SRW_TAC [OL_ss, PRED_SET_ss][TNet_auxfnsTheory.outroute_def, TNet_oksTheory.ifd_set_ok_def, TNet_oksTheory.in_ifds_def, pred_setTheory.GSPECIFICATION] THENL [ PROVE_TAC [pred_setTheory.IN_DISJOINT], FIRST_X_ASSUM (STRIP_ASSUME_TAC o CONV_RULE EXISTS_UNIQUE_CONV) THEN PROVE_TAC [pred_setTheory.IN_DISJOINT], PROVE_TAC [pred_setTheory.IN_DISJOINT], PROVE_TAC [pred_setTheory.IN_DISJOINT] ]); val SOME_is2_SOME_is1 = prove( ``!ifds is1 ps1 is2 ps2 i. socket_srcdest_ok ifds (is1,ps1,is2,ps2) ==> (is2 = SOME i) ==> ?j. is1 = SOME j``, SRW_TAC [][socket_srcdest_ok_def]); val dosend_failing = prove( ``!ifds ips data is1 p1 is2 ps2 oq oqf oq' oqf'. socket_srcdest_ok ifds (is1,SOME p1,is2,ps2) /\ ((?i. is2 = SOME i) \/ (?i p. ips = SOME (i,p))) /\ (oq',oqf',F) IN dosend(ifds, (ips,data), (is1,SOME p1,is2,ps2), oq, oqf) ==> (oq' = oq) /\ (oqf' = oqf) /\ (oqf = T)``, REPEAT GEN_TAC THEN `?oql d. oq = Timed(oql, d)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN `(?i p. ips = SOME (i,p)) \/ (ips = NONE)` by PROVE_TAC [TypeBase.nchotomy_of "option", TypeBase.nchotomy_of "prod"] THEN SRW_TAC [][socket_srcdest_ok_def] THEN Cases_on `oqf` THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ TNet_auxfnsTheory.dosend_def, TNet_auxfnsTheory.enqueue_def, pred_setTheory.IN_BIGUNION, pred_setTheory.GSPECIFICATION, pairTheory.UNCURRY] THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [pred_setTheory.GSPECIFICATION]); val outputq_ok_def = Define`outputq_ok (Timed(oql,d),oqf) = ((oql = []) ==> ~oqf) /\ EVERY msg_oq_ok oql`; val oq_cases = prove( ``!oq : msg list timed. ?oql d. oq = Timed(oql, d)``, PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"]); val dosend_msg_oq_ok = prove( ``!ifds oq oqf is1 is2 p1 ps2 ips oq' oqf' b data. ifd_set_ok ifds ==> outputq_ok(oq,oqf) ==> ((?i. is2 = SOME i) \/ (?i p. ips = SOME (i,p))) ==> (oq',oqf',b) IN dosend (ifds,(ips,data),(is1,SOME p1,is2,ps2),oq,oqf) ==> ((b = F) \/ string_size data <= UDPpayloadMax) ==> socket_srcdest_ok ifds (is1, SOME p1,is2,ps2) ==> outputq_ok(oq',oqf')``, REPEAT GEN_TAC THEN `?oql d. oq = Timed(oql, d)` by PROVE_TAC [oq_cases] THEN `(?i p. ips = SOME (i,p)) \/ (ips = NONE)` by PROVE_TAC [TypeBase.nchotomy_of "option", TypeBase.nchotomy_of "prod"] THEN Cases_on `oqf` THEN SRW_TAC [][socket_srcdest_ok_def] THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ TNet_auxfnsTheory.dosend_def, TNet_auxfnsTheory.enqueue_def, pred_setTheory.IN_BIGUNION, pred_setTheory.GSPECIFICATION, pairTheory.UNCURRY, outputq_ok_def] THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss ++ OL_ss) [ pred_setTheory.GSPECIFICATION, pairTheory.UNCURRY, TNet_oksTheory.msg_oq_ok_def, TNet_oksTheory.msg_ok_def, outputq_ok_def] THEN COND_CASES_TAC THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss ++ OL_ss) [ pred_setTheory.GSPECIFICATION, pairTheory.UNCURRY, TNet_oksTheory.msg_oq_ok_def, TNet_oksTheory.msg_ok_def, outputq_ok_def] THEN PROVE_TAC [ifd_set_ok_MARTIAN]); val OP_returns_errtype = prove( ``!f fd. f IN OP fd ==> ?ty. retType f = TLty_err ty``, SRW_TAC [] [TNet_host0Theory.OP_def, SPECIFICATION] THEN SRW_TAC [] [retType_def]); open mnUtils SatisfySimps val uniquely_valued_def = Define`(uniquely_valued f [] = T) /\ (uniquely_valued f (h::t) = EVERY (\x. ~(f x = f h)) t /\ uniquely_valued f t)`; val FOLDR_INSERT_commutes = prove( ``!l s e f. FOLDR $INSERT (e INSERT s) l = e INSERT (FOLDR $INSERT s l)``, Induct THEN SRW_TAC [][listTheory.FOLDR] THEN PROVE_TAC [pred_setTheory.INSERT_COMM]); val FOLDR_INSERT_FINITE = prove( ``!l s. FINITE (FOLDR $INSERT s l) = FINITE s``, Induct THEN SRW_TAC [PRED_SET_ss][listTheory.FOLDR]); val IN_FOLDR_INSERT = prove( ``!l e s. e IN FOLDR $INSERT s l = e IN s \/ MEM e l``, Induct THEN SRW_TAC [PRED_SET_ss][listTheory.FOLDR] THEN PROVE_TAC []); val CARD_FOLDR_INSERT = prove( ``!l. CARD (FOLDR $INSERT {} l) <= LENGTH l``, Induct THEN SRW_TAC [ARITH_ss, PRED_SET_ss][listTheory.FOLDR, FOLDR_INSERT_FINITE]); val card_len_uniqval = prove( ``!l. uniquely_valued f l = (CARD (FOLDR $INSERT {} (MAP f l)) = LENGTH l)``, Induct THEN SRW_TAC [PRED_SET_ss][listTheory.FOLDR, uniquely_valued_def] THEN REPEAT STRIP_TAC THEN POP_ASSUM (K ALL_TAC) THEN SIMP_TAC (std_ss ++ PRED_SET_ss ++ COND_elim_ss ++ ARITH_ss) [ FOLDR_INSERT_FINITE, IN_FOLDR_INSERT, listTheory.MEM_MAP, listTheory.EVERY_MEM] THEN EQ_TAC THEN REPEAT STRIP_TAC THEN PROVE_TAC [DECIDE ``!n. ~(SUC n <= n)``, listTheory.LENGTH_MAP, CARD_FOLDR_INSERT]); val uniqval_find_def = Define` uniqval_find f e (h::t) = if f h = e then h else uniqval_find f e t`; val uniqval_find_works = prove( ``!l f k e. MEM e l /\ (f e = k) /\ uniquely_valued f l ==> (uniqval_find f k l = e)``, Induct THEN SRW_TAC [][uniqval_find_def, uniquely_valued_def] THENL [ FULL_SIMP_TAC std_ss [listTheory.EVERY_MEM] THEN PROVE_TAC [], ASM_SIMP_TAC std_ss [] ]); val sock_with_fd_uniqval_find = prove( ``!sl s fd. MEM s sl /\ (s.fd = fd) ==> (sock_with_fd fd sl = uniqval_find socket_fd fd sl)``, Induct THEN SRW_TAC [][uniqval_find_def,sock_with_fd_def] THEN FIRST_X_ASSUM (MP_TAC o SPECL [``s:socket``, ``s.fd``]) THEN ASM_REWRITE_TAC []); val sockfds_FOLDR_INSERT = prove( ``!sl. sockfds sl = FOLDR $INSERT {} (MAP socket_fd sl)``, Induct THEN SRW_TAC [][sockfds_thm, listTheory.FOLDR]); val host_ok_thm = store_thm( "host_ok_thm", ``!h. host_ok h = ifd_set_ok h.ifds /\ EVERY (socket_ok h.ifds) h.s /\ outputq_ok(h.oq, h.oqf) /\ (!v tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Ret v, d)) ==> ?ty. tlang_typing v (TLty_err ty)) /\ (!fd tid d ips is1 ps1 is2 ps2 data. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data), d)) ==> fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE) /\ ~(ps1 = NONE) /\ socket_srcdest_ok h.ifds (is1,ps1,is2,ps2) /\ (~(ips = NONE) \/ ~(is2 = NONE))) /\ (!fd tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Recvfrom2 fd, d)) ==> fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE)) /\ (!tid rseq wseq d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Select2(rseq,wseq), d)) ==> LIST_TO_SET (APPEND rseq wseq) SUBSET sockfds h.s /\ time_zero <= d) /\ uniquely_valued socket_fd h.s``, SIMP_TAC (std_ss ++ OL_ss) [host_ok_def, outputq_ok_def] THEN GEN_TAC THEN EQ_TAC THEN SRW_TAC [SATISFY_ss] [sockfds_FOLDR_INSERT, card_len_uniqval] THEN `?oql d. h.oq = Timed(oql,d)` by PROVE_TAC [oq_cases] THEN FULL_SIMP_TAC (srw_ss()) [outputq_ok_def]); val LIST_TO_SET_FOLDR_INSERT = prove( ``!l. LIST_TO_SET l = FOLDR $INSERT {} l``, Induct THEN SRW_TAC[][containerTheory.LIST_TO_SET, listTheory.FOLDR]); val uniquely_valued_APPEND = prove( ``!l1 l2 f. uniquely_valued f (APPEND l1 l2) = uniquely_valued f l1 /\ uniquely_valued f l2 /\ DISJOINT (LIST_TO_SET (MAP f l1)) (LIST_TO_SET (MAP f l2))``, Induct THEN SRW_TAC [PRED_SET_ss][uniquely_valued_def, listTheory.FOLDR, LIST_TO_SET_FOLDR_INSERT, IN_FOLDR_INSERT, listTheory.EVERY_MEM, listTheory.MEM_MAP] THEN EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN PROVE_TAC []); val uniquely_valued_SC = prove( ``!SC s. socklist_context SC ==> (uniquely_valued socket_fd (SC s) = uniquely_valued socket_fd (APPEND (scs1 SC) (s :: scs2 SC)))``, SRW_TAC [][scs_functions_def]); val better_uniquely_valued_SC = prove( ``!SC m p s i e. socklist_context SC ==> (uniquely_valued socket_fd (SC (s with mq := m)) = uniquely_valued socket_fd (SC s)) /\ (uniquely_valued socket_fd (SC (s with ps1 := p)) = uniquely_valued socket_fd (SC s)) /\ (uniquely_valued socket_fd (SC (s with is1 := i)) = uniquely_valued socket_fd (SC s)) /\ (uniquely_valued socket_fd (SC (s with ps2 := p)) = uniquely_valued socket_fd (SC s)) /\ (uniquely_valued socket_fd (SC (s with is2 := i)) = uniquely_valued socket_fd (SC s)) /\ (uniquely_valued socket_fd (SC (s with es := e)) = uniquely_valued socket_fd (SC s))``, SIMP_TAC (srw_ss()) [uniquely_valued_SC, uniquely_valued_def, uniquely_valued_APPEND]); val socket_ok_components = prove( ``!s t. socket_ok ifds t ==> (t.is1 = s.is1) /\ (t.is2 = s.is2) /\ (t.ps2 = s.ps2) /\ ((t.ps1 = s.ps1) \/ (?p. s.ps1 = SOME p)) /\ ((s.ps1 = NONE) ==> (s.es = NONE) /\ (s.mq = [])) /\ (t.mq = s.mq) ==> socket_ok ifds s``, SRW_TAC [][socket_ok_def] THENL [ FULL_SIMP_TAC std_ss [socket_srcdest_ok_def], PROVE_TAC [], PROVE_TAC [], FULL_SIMP_TAC std_ss [socket_srcdest_ok_def], PROVE_TAC [], PROVE_TAC [] ]); val socket_ok_ps1_NONE = prove( ``!s ifds. socket_ok ifds s ==> (s.ps1 = NONE) ==> (s.es = NONE) /\ (s.mq = [])``, SRW_TAC [][socket_ok_def, socket_srcdest_ok_def] THEN FULL_SIMP_TAC (srw_ss()) []); val FAPPLY_FUPD_EQ = prove( ``!fmap k1 v1 k2 v2. (FAPPLY (FUPDATE fmap (k1, v1)) k2 = v2) = (k1 = k2) /\ (v1 = v2) \/ ~(k1 = k2) /\ (FAPPLY fmap k2 = v2)``, SRW_TAC [][finite_mapTheory.FAPPLY_FUPDATE_THM, EQ_IMP_THM]); val socket_ok_vary_fd = prove( ``!ifds fd v. socket_ok ifds v ==> socket_ok ifds (v with fd := fd)``, SRW_TAC [][socket_ok_def]); val failing_rids = store_thm( "failing_rids", ``!rid h0 l h. rid /* fail */ h0 -- l --> h ==> rid IN {bind_5; bind_6; bind_7; bind_8; bind_9; connect_3; disconnect_3; sendto_3; sendto_4; sendto_5; sendto_6; sendto_7; recvfrom_3; recvfrom_4; recvfrom_5; select_2; delay_2; convert_port_2; convert_ip_2; notsockfd_1; notsockfd_2}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val _ = print "Building table of rules by rule-identifier\n"; val _ = print "(This always takes a while.)\n"; val rules_by_rid = let val rid_ts = TypeBase.constructors_of "rule_ids" val simpls = TypeBase.simpls_of "rule_ids" val tac = REWRITE_CONV simpls val do_disj = STRIP_QUANT_CONV (LAND_CONV (tac THENC numLib.REDUCE_CONV)) fun do_case t = (print (Lib.quote (#1 (dest_const t))^ " "); (#1 (dest_const t), (REWRITE_RULE [] o CONV_RULE (STRIP_QUANT_CONV (RHS_CONV (EVERY_DISJ_CONV do_disj))) o SPEC t) host_redn_cases)) in map do_case rid_ts end; fun rid s = Lib.assoc s rules_by_rid val _ = print "\nTable done!\n"; fun claim ss thl = REPEAT (POP_ASSUM MP_TAC) THEN SRW_TAC ss thl THEN PROVE_TAC thl val sock_with_fd_fiddle = store_thm( "sock_with_fd_fiddle", ``!P SC s s' fd. uniquely_valued socket_fd (SC s) /\ fd IN sockfds (SC s) /\ P (sock_with_fd fd (SC s)) /\ (P s ==> P s') /\ uniquely_valued socket_fd (SC s') /\ (s'.fd = s.fd) /\ socklist_context SC ==> P (sock_with_fd fd (SC s'))``, REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ scs_functions_def, uniquely_valued_APPEND, uniquely_valued_def, sockfds_FOLDR_INSERT, IN_FOLDR_INSERT, listTheory.MEM_MAP] THENL [ FIRST_X_ASSUM (SUBST_ALL_TAC o assert (is_var o lhs o concl)) THEN `MEM y (APPEND (scs1 SC) (s:: scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `y.fd` (SUBST_ALL_TAC o REWRITE_RULE [])) sock_with_fd_uniqval_find THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `y.fd`] MP_TAC) uniqval_find_works THEN ASM_SIMP_TAC (srw_ss()) [uniquely_valued_def, uniquely_valued_APPEND] THEN DISCH_THEN SUBST_ALL_TAC THEN `MEM y (APPEND (scs1 SC) (s'::scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `y.fd` (SUBST_ALL_TAC o REWRITE_RULE [])) sock_with_fd_uniqval_find THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `y.fd`] MP_TAC) uniqval_find_works THEN SRW_TAC [] [uniquely_valued_def, uniquely_valued_APPEND], FIRST_X_ASSUM (SUBST_ALL_TAC o assert (is_var o lhs o concl))THEN `MEM s (APPEND (scs1 SC) (s :: scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `s.fd` (SUBST_ALL_TAC o REWRITE_RULE [])) sock_with_fd_uniqval_find THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `s.fd`] MP_TAC) uniqval_find_works THEN ASM_SIMP_TAC (srw_ss()) [uniquely_valued_def, uniquely_valued_APPEND] THEN DISCH_THEN SUBST_ALL_TAC THEN `MEM s' (APPEND (scs1 SC) (s'::scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `s'.fd` MP_TAC) sock_with_fd_uniqval_find THEN SRW_TAC [][] THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `s.fd`] MP_TAC) uniqval_find_works THEN SRW_TAC [] [uniquely_valued_def, uniquely_valued_APPEND], FIRST_X_ASSUM (SUBST_ALL_TAC o assert (is_var o lhs o concl)) THEN `MEM y (APPEND (scs1 SC) (s:: scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `y.fd` (SUBST_ALL_TAC o REWRITE_RULE [])) sock_with_fd_uniqval_find THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `y.fd`] MP_TAC) uniqval_find_works THEN ASM_SIMP_TAC (srw_ss()) [uniquely_valued_def, uniquely_valued_APPEND] THEN DISCH_THEN SUBST_ALL_TAC THEN `MEM y (APPEND (scs1 SC) (s'::scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `y.fd` (SUBST_ALL_TAC o REWRITE_RULE [])) sock_with_fd_uniqval_find THEN nres_search_then 1 true [][] (Q.ISPECL_THEN [`socket_fd`, `y.fd`] MP_TAC) uniqval_find_works THEN SRW_TAC [] [uniquely_valued_def, uniquely_valued_APPEND] ]); val simple_sock_with_fd_fiddle = store_thm( "simple_sock_with_fd_fiddle", ``!fd s SC. uniquely_valued socket_fd (SC s) /\ (s.fd = fd) /\ socklist_context SC ==> (sock_with_fd fd (SC s) = s)``, REPEAT STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) [scs_functions_def] THEN `MEM s (APPEND (scs1 SC) (s::scs2 SC))` by SRW_TAC [][] THEN nres_search_then 1 false [][] (Q.SPEC_THEN `fd` MP_TAC) sock_with_fd_uniqval_find THEN ASM_SIMP_TAC std_ss [] THEN DISCH_THEN (K ALL_TAC) THEN nres_search_then 1 false [][] (Q.ISPECL_THEN [`socket_fd`, `fd`] MATCH_MP_TAC) uniqval_find_works THEN ASM_SIMP_TAC std_ss []); open finite_mapTheory val host_ok_change_to_ret = prove( ``!FC ifds tid ts s t ty d d'. F_context FC ==> host_ok (FC(ifds,tid,Timed(ts, d),s)) ==> tlang_typing t (TLty_err ty) ==> host_ok (FC(ifds,tid,Timed(Ret t,d'),s))``, SIMP_TAC (srw_ss()) [FC_accessors, host_ok_thm, FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN PROVE_TAC [FDOM_FUPDATE]); val simple_FUPD_11 = prove( ``!fm k v1 v2. (FUPDATE fm (k,v1) = FUPDATE fm (k,v2)) = (v1 = v2)``, SIMP_TAC (srw_ss()) [FDOM_FUPDATE, GSYM fmap_EQ_THM, FDOM_FUPDATE, FDOM_FEMPTY, FUN_EQ_THM, DISJ_IMP_THM, FORALL_AND_THM] THEN PROVE_TAC []); val FUPD_11a = prove( ``!fm1 fm2 k v1 v2. ~FDOM fm1 k /\ ~FDOM fm2 k ==> ((FUPDATE fm1 (k,v1) = FUPDATE fm2 (k,v2)) = (v1 = v2) /\ (fm1 = fm2))``, REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ ALL_TAC, ASM_REWRITE_TAC [] ] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [GSYM fmap_EQ_THM, FDOM_FUPDATE, FUN_EQ_THM] THEN STRIP_TAC THEN `!x. FDOM fm1 x = FDOM fm2 x` by PROVE_TAC [] THEN `v1 = v2` by PROVE_TAC [FAPPLY_FUPDATE_THM] THEN POP_ASSUM SUBST_ALL_TAC THEN PROVE_TAC [FAPPLY_FUPDATE_THM]); val FUPD_11b = prove( ``!fm1 fm2 k v1 v2. ~(v1 = v2) ==> ~(FUPDATE fm1 (k, v1) = FUPDATE fm2 (k, v2))``, REPEAT GEN_TAC THEN STRIP_TAC THEN SIMP_TAC (srw_ss()) [GSYM fmap_EQ_THM] THEN DISJ2_TAC THEN Q.EXISTS_TAC `k` THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPDATE]); val FUPD_11c = prove( ``!fm1 fm2 k1 k2 v1 v2 v3. ~(v2 = v3) /\ ~(v1 = v3) ==> ~(FUPDATE fm1 (k1, v3) = FUPDATE (FUPDATE fm2 (k1, v1)) (k2, v2))``, REPEAT GEN_TAC THEN STRIP_TAC THEN SIMP_TAC (srw_ss()) [GSYM fmap_EQ_THM] THEN DISJ2_TAC THEN Q.EXISTS_TAC `k1` THEN ASM_SIMP_TAC (srw_ss() ++ COND_elim_ss) [FDOM_FUPDATE, FAPPLY_FUPDATE_THM]); val FUPD_11d = prove( ``!fm k1 k2 v1 v2 v3. ~(v1 = v2) ==> ((FUPDATE fm (k1, v1) = FUPDATE (FUPDATE fm (k1, v2)) (k2, v3)) = (k1 = k2) /\ (v1 = v3))``, REPEAT GEN_TAC THEN STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC (srw_ss()) [FUPDATE_EQ] THEN SIMP_TAC (srw_ss()) [GSYM fmap_EQ_THM] THEN STRIP_TAC THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `k1`) THEN ASM_SIMP_TAC (srw_ss() ++ COND_elim_ss) [FAPPLY_FUPDATE_THM, FDOM_FUPDATE] THEN DECIDE_TAC); val FUPD_11 = prove( ``!fm k1 v1 k2 v2. (FUPDATE fm (k1,v1) = FUPDATE fm (k2,v2)) = ((k1 = k2) /\ (v1 = v2) \/ ~(k1 = k2) /\ k1 IN FDOM fm /\ k2 IN FDOM fm /\ (FAPPLY fm k1 = v1) /\ (FAPPLY fm k2 = v2))``, HO_MATCH_MP_TAC finite_mapTheory.fmap_INDUCT THEN REPEAT STRIP_TAC THENL [ SIMP_TAC std_ss [SPECIFICATION, finite_mapTheory.FDOM_FEMPTY, finite_mapTheory.FDOM_FUPDATE, GSYM finite_mapTheory.fmap_EQ_THM, FUN_EQ_THM] THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ PROVE_TAC [], `k1 = k2` by PROVE_TAC [] THEN POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC std_ss [finite_mapTheory.FAPPLY_FUPDATE], ASM_SIMP_TAC std_ss [], ASM_SIMP_TAC std_ss [] ], EQ_TAC THEN REPEAT STRIP_TAC THENL [ Cases_on `k1 = x` THENL [ POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (ASSUME_TAC o REWRITE_RULE [finite_mapTheory.FUPDATE_EQ]) THEN Cases_on `k2 = x` THENL [ POP_ASSUM SUBST_ALL_TAC THEN POP_ASSUM (ASSUME_TAC o REWRITE_RULE [FUPDATE_EQ, simple_FUPD_11]) THEN ASM_REWRITE_TAC [], `FUPDATE fm (x,v1) = FUPDATE (FUPDATE fm (k2,v2)) (x,y)` by PROVE_TAC [FUPDATE_COMMUTES] THEN `(y = v1) /\ (fm = FUPDATE fm (k2,v2))` by PROVE_TAC [FDOM_FUPDATE, FUPD_11a] THEN NTAC 2 (POP_ASSUM SUBST1_TAC) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM, FDOM_FUPDATE, SPECIFICATION] ], (* ~(k1 = x) *) Cases_on `k2 = x` THENL [ POP_ASSUM SUBST_ALL_TAC THEN RULE_ASSUM_TAC (REWRITE_RULE [FUPDATE_EQ]) THEN `FUPDATE fm (x,v2) = FUPDATE (FUPDATE fm (k1,v1)) (x,y)` by PROVE_TAC [FUPDATE_COMMUTES] THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, SPECIFICATION] THEN `(y = v2) /\ (fm = FUPDATE fm (k1,v1))` by PROVE_TAC [FDOM_FUPDATE, FUPD_11a] THEN NTAC 2 (POP_ASSUM SUBST1_TAC) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM, FDOM_FUPDATE], `FUPDATE (FUPDATE fm (k1,v1)) (x,y) = FUPDATE (FUPDATE fm (k2,v2)) (x,y)` by PROVE_TAC [FUPDATE_COMMUTES] THEN `FUPDATE fm (k1,v1) = FUPDATE fm (k2,v2)` by PROVE_TAC [FDOM_FUPDATE, FUPD_11a] THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, SPECIFICATION, FAPPLY_FUPDATE_THM] THEN PROVE_TAC [SPECIFICATION] ] ], ASM_REWRITE_TAC [], SIMP_TAC (srw_ss()) [GSYM fmap_EQ_THM, FUN_EQ_THM, FDOM_FUPDATE] THEN REPEAT STRIP_TAC THENL [ FULL_SIMP_TAC (srw_ss()) [SPECIFICATION, FDOM_FUPDATE] THEN PROVE_TAC [], POP_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM], POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [ FAPPLY_FUPDATE_THM, SPECIFICATION, FDOM_FUPDATE] THEN REPEAT (FIRST_X_ASSUM (SUBST_ALL_TAC o assert (is_var o lhs o concl))) THEN PROVE_TAC [], Cases_on `x' = k1` THENL [ POP_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM], Cases_on `x' = k2` THENL [ POP_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM], ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM] ] ] ] ] ]); val SC_11 = prove( ``!SC. socklist_context SC ==> !s1 s2. (SC s1 = SC s2) = (s1 = s2)``, SRW_TAC [][scs_functions_def]); val host_ok_every_socket_ok = prove( ``!h. host_ok h ==> EVERY (socket_ok h.ifds) h.s``, REPEAT STRIP_TAC THEN IMP_RES_TAC host_ok_thm); val host_ok_socket_ok = prove( ``!h. host_ok h ==> !s. MEM s h.s ==> socket_ok h.ifds s``, ACCEPT_TAC (REWRITE_RULE [listTheory.EVERY_MEM] host_ok_every_socket_ok)); val host_ok_ifd_set_ok = prove( ``!h. host_ok h ==> ifd_set_ok h.ifds``, SRW_TAC [] [host_ok_thm]); val host_ok_outputq_ok = prove( ``!h. host_ok h ==> outputq_ok(h.oq,h.oqf)``, SRW_TAC [] [host_ok_thm]); val host_ok_ret_ts_ok = prove( ``!h. host_ok h ==> !v tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed(Ret v,d)) ==> ?ty. tlang_typing v (TLty_err ty)``, SRW_TAC [][host_ok_thm]); val host_ok_uniquely_valued = prove( ``!h. host_ok h ==> uniquely_valued socket_fd h.s``, GEN_TAC THEN STRIP_TAC THEN IMP_RES_TAC host_ok_thm); val host_ok_sendto_ok = prove( ``!h. host_ok h ==> !fd tid d ips is1 ps1 is2 ps2 data. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d)) ==> fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE) /\ ~(ps1 = NONE) /\ socket_srcdest_ok h.ifds (is1,ps1,is2,ps2) /\ (~(ips = NONE) \/ ~(is2 = NONE))``, SRW_TAC [][host_ok_thm]); val host_ok_recvfrom_ok = prove( ``!h. host_ok h ==> !fd tid d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Recvfrom2 fd,d)) ==> fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE)``, SRW_TAC [][host_ok_thm]); val host_ok_select_ok = prove( ``!h. host_ok h ==> !tid rseq wseq d. FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Select2 (rseq,wseq),d)) ==> LIST_TO_SET (APPEND rseq wseq) SUBSET sockfds h.s /\ time_zero <= d``, SRW_TAC [][host_ok_thm]); val sock_with_fd_fd = prove( ``!fd slist. fd IN sockfds slist ==> ((sock_with_fd fd slist).fd = fd)``, GEN_TAC THEN Induct THEN SRW_TAC [PRED_SET_ss][sockfds_thm, sock_with_fd_def]); val uniquely_valued_diff_socks = prove( ``!s1 s2. socklist_context SC /\ (s1.fd = s2.fd) ==> (uniquely_valued socket_fd (SC s1) = uniquely_valued socket_fd (SC s2))``, REPEAT STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [uniquely_valued_def, uniquely_valued_APPEND, uniquely_valued_SC]); val sock_with_fd_MEM = prove( ``!fd slist. fd IN sockfds slist ==> MEM (sock_with_fd fd slist) slist``, GEN_TAC THEN Induct THEN SRW_TAC [PRED_SET_ss][sockfds_thm, sock_with_fd_def]); val ignore_disjs = REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) val _ = print "About to prove super useful component-wise proof rule for host_ok... " val comp_host_ok = store_thm( "comp_host_ok", ``!h0 h. host_ok h0 /\ (h.ifds = h0.ifds) /\ ((h.s = h0.s) \/ (?SC s0 s. socklist_context SC /\ (h.s = SC s) /\ (h0.s = SC s0) /\ socket_ok h0.ifds s /\ (s.fd = s0.fd) /\ ((s.ps1 = NONE) ==> (s0.ps1 = NONE)))) /\ ((h.oqf = h0.oqf) /\ (h.oq = h0.oq) \/ outputq_ok (h.oq,h.oqf)) /\ ((h.ts = h0.ts) \/ (?tid t ty d. (h.ts = FUPDATE h0.ts (tid, Timed(Ret t, d))) /\ tlang_typing t (TLty_err ty)) \/ (?tid fd d ips is1 ps1 is2 ps2 data. (h.ts = FUPDATE h0.ts (tid, Timed(Sendto2(fd,ips,is1,ps1,is2,ps2,data),d))) /\ fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE) /\ ~(ps1 = NONE) /\ socket_srcdest_ok h.ifds (is1,ps1,is2,ps2) /\ (~(ips = NONE) \/ ~(is2 = NONE))) \/ (?fd tid d. (h.ts = FUPDATE h0.ts (tid, Timed(Recvfrom2 fd, d))) /\ fd IN sockfds h.s /\ ~((sock_with_fd fd h.s).ps1 = NONE)) \/ (?tid rseq wseq d. (h.ts = FUPDATE h0.ts (tid, Timed(Select2(rseq,wseq), d))) /\ LIST_TO_SET (APPEND rseq wseq) SUBSET sockfds h.s /\ time_zero <= d) \/ (?tid d. (h.ts = FUPDATE h0.ts (tid, Timed(Delay2, d)))) \/ (?tid data d. (h.ts = FUPDATE h0.ts (tid, Timed(Print2 data, d)))) \/ (?tid d. (h.ts = FUPDATE h0.ts (tid, Timed(Run, d)))) \/ (?tid d. (h.ts = FUPDATE h0.ts (tid, Timed(Exit,d))))) ==> host_ok h``, REPEAT GEN_TAC THEN REPEAT (DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC)) THEN SIMP_TAC (srw_ss())[host_ok_thm] THEN `EVERY (socket_ok h.ifds) h.s /\ (sockfds h.s = sockfds h0.s) /\ !fd. fd IN sockfds h.s ==> ((sock_with_fd fd h.s).ps1 = NONE) ==> ((sock_with_fd fd h0.s).ps1 = NONE)` by (FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``socket_ok`` o concl)) THEN IMP_RES_TAC host_ok_every_socket_ok THEN ASM_SIMP_TAC (srw_ss()) [] THEN ignore_disjs THEN Q.PAT_ASSUM `EVERY (socket_ok h0.ifds) h0.s` MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [EVERY_SC, sockfds_SC] THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC THEN `uniquely_valued socket_fd (SC s0)` by PROVE_TAC [host_ok_uniquely_valued] THEN `uniquely_valued socket_fd (SC s)` by PROVE_TAC [uniquely_valued_diff_socks] THEN Q.SPECL_THEN [`\x. (x.ps1 = NONE) ==> ((sock_with_fd x.fd (SC s0)).ps1 = NONE)`, `SC`, `s0`, `s`, `fd`] (MP_TAC o BETA_RULE) sock_with_fd_fiddle THEN ASM_SIMP_TAC (srw_ss()) [sockfds_SC, sock_with_fd_fd, simple_sock_with_fd_fiddle]) THEN REPEAT CONJ_TAC THENL [ (* ifd_set_ok *) ASM_REWRITE_TAC [] THEN IMP_RES_TAC host_ok_thm, (* every socket ok *) FIRST_ASSUM ACCEPT_TAC, (* outputq_ok *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``outputq_ok`` o concl)) THEN ASM_REWRITE_TAC [] THEN IMP_RES_TAC host_ok_thm, (* ret states have typed values *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``tlang_typing`` o concl)) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE] THEN IMP_RES_TAC host_ok_ret_ts_ok THEN REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) THEN PROVE_TAC [], (* sendto2 states are ok *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``tlang_typing`` o concl)) THEN REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE] THEN RULE_ASSUM_TAC (REWRITE_RULE [listTheory.EVERY_MEM]) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN TRY (res_search_then false [][] MP_TAC host_ok_sendto_ok) THEN ASM_SIMP_TAC (srw_ss())[] THEN QCONTR_TAC THEN PROVE_TAC [], (* recvfrom2 state *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``tlang_typing`` o concl)) THEN REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE] THEN RULE_ASSUM_TAC (REWRITE_RULE [listTheory.EVERY_MEM]) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN TRY (res_search_then false [] [] ASSUME_TAC host_ok_recvfrom_ok) THEN PROVE_TAC [], (* select2 state *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``tlang_typing`` o concl)) THEN REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE] THEN RULE_ASSUM_TAC (REWRITE_RULE [listTheory.EVERY_MEM]) THEN REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN TRY (res_search_then false [] [] ASSUME_TAC host_ok_select_ok) THEN PROVE_TAC [], (* uniquely valued h.s *) FIRST_X_ASSUM (STRIP_ASSUME_TAC o assert (free_in ``socklist_context`` o concl)) THEN `uniquely_valued socket_fd h0.s` by IMP_RES_TAC host_ok_uniquely_valued THEN REPEAT (Q.PAT_ASSUM `p \/ q` (K ALL_TAC)) THEN PROVE_TAC [uniquely_valued_diff_socks] ]); val _ = print "done\n"; val host_ok_socket_srcdest_ok = prove( ``!h SC s. host_ok h /\ (h.s = SC s) /\ socklist_context SC ==> socket_srcdest_ok h.ifds (s.is1,s.ps1,s.is2,s.ps2)``, SRW_TAC [][host_ok_thm] THEN FULL_SIMP_TAC (srw_ss()) [EVERY_SC, socket_ok_def]); val FC_host_ok_socket_ok = prove( ``!ifds tid ts s. F_context FC /\ host_ok (FC(ifds,tid,ts,s)) ==> socket_ok ifds s``, REPEAT STRIP_TAC THEN IMP_RES_THEN MP_TAC host_ok_socket_ok THEN ASM_SIMP_TAC (srw_ss()) [FC_accessors] THEN PROVE_TAC [FC_SC_OK, SC_MEM]); fun progress s (asl,w) = (print ("Tactic progress: "^s ^"\n"); ALL_TAC (asl,w)) val fail_characterise = store_thm( "fail_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* fail */ h0 -- l --> h ==> host_ok h /\ ?tid. (?f. (l = Lh_call(tid,f)) /\ (?ty. retType f = TLty_err ty)) /\ (h.ifds = h0.ifds) /\ (h.oq = h0.oq) /\ (h.oqf = h0.oqf) /\ (?d d'. (FAPPLY h0.ts tid = Timed(Run, d)) /\ ( ?e. FAPPLY h.ts tid = Timed(Ret (FAIL e), d')))``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) failing_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ (* rid = bind_5 *) progress "fail - bind_5" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_5", FC_accessors, retType_def] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] host_ok_change_to_ret) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN PROVE_TAC [], (* rid = bind_6 *) progress "fail - bind_6" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_6", FC_accessors, retType_def] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] host_ok_change_to_ret) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN PROVE_TAC [], (* rid = bind_7 *) progress "fail - bind_7" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_7", FC_accessors, retType_def] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] host_ok_change_to_ret) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN PROVE_TAC [], (* rid = bind_8 *) progress "fail - bind_8" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_8", FC_accessors, retType_def] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] host_ok_change_to_ret) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN PROVE_TAC [], (* rid = bind_9 *) progress "fail - bind_9" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_9", FC_accessors, retType_def] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] host_ok_change_to_ret) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN PROVE_TAC [], (* rid = connect_3 *) progress "fail - connect_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "connect_3", FC_accessors, retType_def] THEN IMP_RES_TAC FC_SC_OK THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, Sock_def, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN (* h.s component *) DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [ `fc_sc FC`, `Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)`, `s with fd := fd`] THEN ASM_SIMP_TAC (srw_ss()) [Sock_def], (* rid = disconnect_3 *) progress "fail - disconnect_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "disconnect_3", FC_accessors, retType_def] THEN IMP_RES_TAC FC_SC_OK THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, Sock_def, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [ `fc_sc FC`, `Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)`, `s with fd := fd`] THEN ASM_SIMP_TAC (srw_ss()) [Sock_def], (* rid = sendto_3 *) progress "fail - sendto_3" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_3", retType_def, FC_accessors] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [retType_def] THEN Q.SUBGOAL_THEN `(?i. s.is2 = SOME i) \/ (?i p. ips = SOME (i, p))` ASSUME_TAC THENL [ PROVE_TAC [TypeBase.nchotomy_of "option", TypeBase.nchotomy_of "prod"], ALL_TAC ] THEN `socket_srcdest_ok h'.ifds (s.is1,s.ps1,s.is2,s.ps2)` by FULL_SIMP_TAC (srw_ss()) [host_ok_thm, EVERY_SC, socket_ok_def] THEN `socket_srcdest_ok h'.ifds (s.is1,SOME p1',s.is2,s.ps2)` by PROVE_TAC [new_ps1_socket_srcdest_ok] THEN res_search false [] [] dosend_failing THEN ASM_SIMP_TAC (srw_ss())[] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, SC_11, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s with es := NONE`, `s with <| ps1 := SOME p1'; es := NONE |>`] THEN ASM_SIMP_TAC (srw_ss())[] THEN (* socket_ok *) `h0.s = SC (s with es := NONE)` by ASM_SIMP_TAC (srw_ss())[] THEN ignore_disjs THEN `socket_ok h0.ifds (s with es := NONE)` by PROVE_TAC [SC_MEM, host_ok_socket_ok] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] socket_ok_components) THEN Q.EXISTS_TAC `s with es := NONE` THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [], (* rid = sendto_4 *) progress "fail - sendto_4" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_4", retType_def, FC_accessors] THEN Q.ABBREV_TAC `s0 = Sock(fd,is1,ps1,NONE,NONE,NONE,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,is1,SOME p1',NONE,NONE,NONE,f,mq)` THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss()) [Sock_def], (* rid = sendto_5 *) progress "fail - sendto_5" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_5", retType_def, FC_accessors] THEN Q.ABBREV_TAC `s0 = s with <| ps1 := SOME p1; es := SOME e |>` THEN Q.ABBREV_TAC `s' = s with <| ps1 := SOME p1; es := NONE |>` THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [] THEN NO_TAC) THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] socket_ok_components) THEN Q.EXISTS_TAC `s0` THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN SIMP_TAC (srw_ss())[] THEN NO_TAC) THEN `(h0.ifds = ifds) /\ (h0.s = fc_sc FC s0)` by ASM_SIMP_TAC (srw_ss()) [FC_accessors] THEN PROVE_TAC [host_ok_socket_ok, SC_MEM], (* rid = sendto_6 *) progress "fail - sendto_6" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_6", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN `(ps1' = s.ps1) \/ ?p. ps1' = SOME p` by FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[] THENL [ASM_SIMP_TAC (srw_ss())[], ALL_TAC] THEN POP_ASSUM SUBST_ALL_TAC THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s`, `s with ps1 := SOME p`] THEN ASM_SIMP_TAC (srw_ss())[] THEN `socket_ok ifds s` by PROVE_TAC [FC_host_ok_socket_ok] THEN nres_search_then 1 false [] [] MATCH_MP_TAC socket_ok_components THEN SIMP_TAC (srw_ss())[], (* rid = sendto_7 *) progress "fail - sendto_7" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_7", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `Sock(fd,NONE,NONE,NONE,NONE,NONE,f,mq)`, `s with fd := fd`] THEN ASM_SIMP_TAC (srw_ss()) [Sock_def], (* rid = recvfrom_3 *) progress "fail - recvfrom_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_3", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN Q.ABBREV_TAC `s0 = s with <| es := NONE; mq := [] |>` THEN Q.ABBREV_TAC `s' = s0 with ps1 := SOME p1'` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[], (* rid = recvfrom_4 *) progress "fail - recvfrom_4" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_4", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN Q.ABBREV_TAC `s0 = s with <| ps1 := SOME p1; es := SOME e|>` THEN Q.ABBREV_TAC `s' = s with <| ps1 := SOME p1; es := NONE |>` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[], (* rid = recvfrom_5 *) progress "fail - recvfrom_5" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_5", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `Sock(fd,NONE,NONE,NONE,NONE,NONE,f,[])`, `s with fd := fd`] THEN ASM_SIMP_TAC (srw_ss()) [Sock_def], (* rid = select_2 *) progress "fail - select_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "select_2", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11], (* rid = delay_2 *) progress "fail - delay_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "delay_2", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11], (* rid = convert_port_2 *) progress "fail - convert_port_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "convert_port_2", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11], (* rid = convert_ip_2 *) progress "fail - convert_ip_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "convert_ip_2", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11], (* rid = notsockfd_1 *) progress "fail - notsockfd_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "notsockfd_1", retType_def, FC_accessors] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11], (* rid = notsockfd_2 *) progress "fail - notsockfd_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "notsockfd_2", retType_def, FC_accessors] THEN CONJ_TAC THENL [ALL_TAC, PROVE_TAC [OP_returns_errtype]] THEN MATCH_MP_TAC comp_host_ok THEN IMP_RES_TAC FC_SC_OK THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, SC_11] ] ); val _ = print "\nProved characterisation for fail category\n"; val slowfail_rids = prove( ``!h0 l h rid. rid /* slowfail */ h0 -- l --> h ==> rid IN {sendto_9; sendto_10; recvfrom_7; intr_1}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val slowfail_characterise = store_thm( "slowfail_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* slowfail */ h0 -- l --> h ==> host_ok h /\ ?tid e d. FAPPLY h0.ts tid IN OP2 /\ (l = Lh_tau) /\ (FAPPLY h.ts tid = Timed(Ret (FAIL e), d))``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) slowfail_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "slowfail - sendto_9" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_9", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN DISJ2_TAC THEN IMP_RES_TAC FC_SC_OK THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s with es := SOME e`, `s with es := NONE`] THEN ASM_SIMP_TAC (srw_ss()) [] THEN `socket_ok ifds (s with es := SOME e)` by PROVE_TAC [FC_host_ok_socket_ok] THEN FIRST_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN IMP_RES_THEN MP_TAC socket_ok_ps1_NONE THEN SIMP_TAC (srw_ss()) [], progress "slowfail - sendto_10" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_10", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "slowfail - recvfrom_7" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_7", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN DISJ2_TAC THEN IMP_RES_TAC FC_SC_OK THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s with <| ps1 := SOME p1; es := SOME e|>`, `s with <| ps1 := SOME p1; es := NONE|>`] THEN ASM_SIMP_TAC (srw_ss()) [] THEN `socket_ok ifds (s with <| ps1 := SOME p1; es := SOME e|>)` by PROVE_TAC [FC_host_ok_socket_ok] THEN FIRST_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN IMP_RES_THEN MP_TAC socket_ok_ps1_NONE THEN SIMP_TAC (srw_ss()) [], progress "slowfail - intr_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "intr_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] ] ); val _ = print "\nProved characterisation for slowfail category\n"; val OP_types_all_errs = prove( ``!opn fd. opn IN OP fd ==> ?ty. retType opn = TLty_err ty``, SRW_TAC [][SPECIFICATION,TNet_host0Theory.OP_def] THEN SRW_TAC [][retType_def]); val IN_fdOP2 = GEN_ALL ((REWR_CONV SPECIFICATION THENC REWRITE_CONV [TNet_host0Theory.OP2_def]) ``opn IN OP2 fd``) val badfail_rids = prove( ``!rid h0 l h. rid /* badfail */ h0 -- l --> h ==> rid IN {socket_2; badmem_1; badmem_2; badmem_3; badmem_4; create_2}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val badfail_characterise = store_thm( "badfail_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* badfail */ h0 -- l --> h ==> host_ok h /\ ((?tid f ty. (l = Lh_call(tid, f)) /\ (retType f = TLty_err ty) /\ ?d d'. (FAPPLY h0.ts tid = Timed(Run, d)) /\ ?e. FAPPLY h.ts tid = Timed(Ret (FAIL e), d')) \/ (?tid d e. (l = Lh_tau) /\ FAPPLY h0.ts tid IN OP2 /\ (FAPPLY h.ts tid = Timed(Ret (FAIL e), d))))``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) badfail_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "badfail - socket_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "socket_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "badfail - badmem_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "badmem_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "badfail - badmem_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "badmem_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def] THEN CONJ_TAC THENL [ALL_TAC, PROVE_TAC [OP_types_all_errs]] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "badfail - badmem_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "badmem_3", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, LEFT_AND_EXISTS_THM, IN_fdOP2] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "badfail - badmem_4" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "badmem_4", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, LEFT_AND_EXISTS_THM, IN_fdOP2] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "badfail - create_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "create_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, LEFT_AND_EXISTS_THM, IN_fdOP2] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] ]); val _ = print "\nProved characterisation for badfail category\n"; val _ = print "That's all the failure categories done; 3 / 8\n"; val ps_lemma2 = prove( ``!x. {} x = F``, GEN_TAC THEN CONV_TAC (LHS_CONV (REWR_CONV (GSYM SPECIFICATION))) THEN SRW_TAC [PRED_SET_ss][]); val OP2_types_all_errs = prove( ``!t d. Timed(t,d) IN OP2 ==> !ty. ty IN htsType t ==> ?ty0. ty = TLty_err ty0``, SRW_TAC [] [OP2_def, SPECIFICATION] THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [htsType_def, ps_lemma, ps_lemma2]); val EVERY_FRONT = prove( ``!l. ~(l = []) ==> EVERY P l ==> EVERY P (FRONT l)``, Induct THEN SRW_TAC [][listTheory.FRONT_DEF]); val dequeue_def = TNet_auxfnsTheory.dequeue_def val dequeue_ok = prove( ``!m oq' oqf' oq oqf. (m,oq',oqf') IN dequeue(oq,oqf) ==> outputq_ok(oq,oqf) ==> outputq_ok(oq',oqf')``, REPEAT GEN_TAC THEN `?oql d oql' d'. (oq = Timed(oql,d)) /\ (oq' = Timed(oql',d'))` by PROVE_TAC [oq_cases] THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[dequeue_def, outputq_ok_def] THEN COND_CASES_TAC THEN SIMP_TAC (srw_ss() ++ PRED_SET_ss) [GSPECIFICATION, pairTheory.UNCURRY, pairTheory.EXISTS_PROD, EVERY_FRONT] THEN STRIP_TAC THEN REPEAT (FIRST_X_ASSUM (SUBST_ALL_TAC o assert(is_var o lhs o concl))) THEN ASM_SIMP_TAC (srw_ss()) [EVERY_FRONT]); val LAST_is_MEM = prove( ``!l. ~(l = []) ==> MEM (LAST l) l``, Induct THEN SRW_TAC [][listTheory.LAST_DEF]); val dequeue_is_member = prove( ``!m oq' oqf' oql d oqf. (m,oq',oqf') IN dequeue(Timed(oql,d),oqf) ==> MEM m oql``, SRW_TAC [PRED_SET_ss][dequeue_def, GSPECIFICATION, pairTheory.UNCURRY, LAST_is_MEM]); val dequeue_msg_oq_ok = prove( ``!m oq' oqf' oq oqf. (m,oq',oqf') IN dequeue(oq,oqf) ==> outputq_ok (oq,oqf) ==> msg_oq_ok m``, REPEAT STRIP_TAC THEN `?oql d. oq = Timed(oql,d)` by PROVE_TAC [oq_cases] THEN FULL_SIMP_TAC (srw_ss())[] THEN res_search false [] [] dequeue_is_member THEN FULL_SIMP_TAC (srw_ss())[outputq_ok_def, listTheory.EVERY_MEM]); val ps1_NONE_all_NONE = prove( ``!ifds s. socket_ok ifds s /\ (s.ps1 = NONE) ==> (s.is1 = NONE) /\ (s.is2 = NONE) /\ (s.ps2 = NONE)``, SRW_TAC [][socket_ok_def, socket_srcdest_ok_def] THEN FULL_SIMP_TAC std_ss []); val EVERY_LAST = prove( ``!l. ~(l = []) ==> EVERY P l ==> P (LAST l)``, Induct THEN SRW_TAC [][listTheory.LAST_DEF]); val label_ok_def = Define`(label_ok (Lh_recvmsg m) = case m.body of UDP(x,y,body) -> string_size body <= UDPpayloadMax || z -> T) /\ (label_ok _ = T)`; val succeed_rids = prove( ``!rid h0 l h. rid /* succeed */ h0 -- l --> h ==> rid IN {socket_1; bind_1; bind_2; bind_3; bind_4; connect_1; connect_2; disconnect_1; disconnect_2; getsockname_1; getpeername_1; geterr_1; getsockopt_1; setsockopt_1; sendto_1; recvfrom_1; close_1; getifaddrs_1; convert_port_1; convert_ip_1; create_1}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val IN_tlang_typing = prove( ``!ty t. ty IN tlang_typing t = tlang_typing t ty``, SIMP_TAC (srw_ss()) [SPECIFICATION]); val real_ts_cases = prove( ``!ts. (ts = Run) \/ (ts = Exit) \/ (ts = Zombie) \/ (?tm. ts = Ret tm) \/ (?fd ips is ps data. ts = Sendto2(fd,ips,is,ps,data)) \/ (?fd. ts = Recvfrom2 fd) \/ (?rs ws. ts = Select2(rs,ws)) \/ (ts = Delay2) \/ (?s. ts = Print2 s)``, Cases THEN SRW_TAC [][] THEN PROVE_TAC [TypeBase.nchotomy_of "prod"]); val zombify_EQ_Ret = prove( ``!fd ts v d. (zombify fd ts = Timed(Ret v,d)) = (ts = Timed(Ret v,d))``, REPEAT GEN_TAC THEN `?ts0 d0. ts = Timed(ts0,d0)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN POP_ASSUM SUBST_ALL_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ts0` real_ts_cases) THEN SRW_TAC [] [TNet_auxfnsTheory.zombify_def]); val zombify_EQ_Sendto = prove( ``!fd1 ts fd2 otherstuff d. (zombify fd1 ts = Timed(Sendto2(fd2,otherstuff),d)) = (ts = Timed(Sendto2(fd2,otherstuff), d)) /\ ~(fd1 = fd2)``, REPEAT GEN_TAC THEN `?ts0 d0. ts = Timed(ts0,d0)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN POP_ASSUM SUBST_ALL_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ts0` real_ts_cases) THEN SRW_TAC [] [TNet_auxfnsTheory.zombify_def] THENL [ tautLib.TAUT_TAC, EQ_TAC THEN SRW_TAC [][] THEN SRW_TAC [][] ]); val zombify_EQ_Recvfrom = prove( ``!fd1 ts fd2 d. (zombify fd1 ts = Timed(Recvfrom2 fd2, d)) = (ts = Timed(Recvfrom2 fd2, d)) /\ ~(fd1 = fd2)``, REPEAT GEN_TAC THEN `?ts0 d0. ts = Timed(ts0,d0)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN POP_ASSUM SUBST_ALL_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ts0` real_ts_cases) THEN SRW_TAC [] [TNet_auxfnsTheory.zombify_def] THENL [ tautLib.TAUT_TAC, EQ_TAC THEN SRW_TAC [][] THEN SRW_TAC [][] ]); val zombify_EQ_Select = prove( ``!fd1 ts rseq wseq. (zombify fd1 ts = Timed(Select2(rseq,wseq),d)) = ?rseq0 wseq0. (ts = Timed(Select2(rseq0,wseq0), d)) /\ (rseq = FILTER (\fd. ~(fd = fd1)) rseq0) /\ (wseq = FILTER (\fd. ~(fd = fd1)) wseq0)``, REPEAT GEN_TAC THEN EQ_TAC THEN `?ts0 d0. ts = Timed(ts0,d0)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN POP_ASSUM SUBST_ALL_TAC THEN STRUCT_CASES_TAC (Q.SPEC `ts0` real_ts_cases) THEN SRW_TAC [] [TNet_auxfnsTheory.zombify_def]); val sock_with_fd_APPEND = prove( ``!slist1 slist2 fd. sock_with_fd fd (APPEND slist1 slist2) = if fd IN sockfds slist1 then sock_with_fd fd slist1 else sock_with_fd fd slist2``, Induct THEN SRW_TAC [PRED_SET_ss][sockfds_thm, sock_with_fd_def] THEN FULL_SIMP_TAC (srw_ss())[]); val LIST_TO_SET_APPEND = prove( ``!l1 l2. LIST_TO_SET (APPEND l1 l2) = LIST_TO_SET l1 UNION LIST_TO_SET l2``, Induct THEN SRW_TAC [PRED_SET_ss][containerTheory.LIST_TO_SET, pred_setTheory.INSERT_UNION_EQ]); val LIST_TO_SET_FILTER = prove( ``!l P. LIST_TO_SET (FILTER P l) = LIST_TO_SET l INTER {x | P x}``, Induct THEN SRW_TAC [PRED_SET_ss][containerTheory.LIST_TO_SET, listTheory.FILTER] THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [pred_setTheory.EXTENSION, EQ_IMP_THM, DISJ_IMP_THM, FORALL_AND_THM, RIGHT_AND_OVER_OR, GSPECIFICATION]); val succeed_characterise = store_thm( "succeed_characterise", ``!h0 rid l h. host_ok h0 /\ rid /* succeed */ h0 -- l --> h ==> host_ok h /\ ?tid f d ts d'. (l = Lh_call(tid, f)) /\ (FAPPLY h0.ts tid = Timed(Run,d)) /\ (FAPPLY h.ts tid = Timed(ts, d')) /\ retType f IN htsType ts``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) succeed_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "succeed - socket_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "socket_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN IMP_RES_THEN MP_TAC host_ok_ifd_set_ok THEN IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN IMP_RES_THEN MP_TAC host_ok_every_socket_ok THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [host_ok_thm, FAPPLY_FUPD_EQ, DISJ_IMP_THM, FORALL_AND_THM, Sock_def, FDOM_FUPDATE, sockfds_thm, socket_ok_def, socket_srcdest_ok_thm] THEN NTAC 3 STRIP_TAC THEN REPEAT CONJ_TAC THENL [ (* ret states ok *) REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FAPPLY_FUPD_EQ] THEN nres_search_then 1 false [] [] MATCH_MP_TAC host_ok_ret_ts_ok THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, RIGHT_AND_OVER_OR, EXISTS_OR_THM] THEN PROVE_TAC [FAPPLY_FUPDATE_THM], (* sendto ok *) REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN QCONTR_TAC THEN nres_search_then 1 false [] [] MP_TAC host_ok_sendto_ok THEN ASM_SIMP_TAC (srw_ss()) [FC_accessors, FAPPLY_FUPD_EQ, FDOM_FUPDATE] THEN DISCH_THEN (MP_TAC o Q.SPECL [`fd'`, `tid'`]) THEN ASM_SIMP_TAC (srw_ss())[] THEN DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN `~(fd' = fd)` by (DISCH_THEN SUBST_ALL_TAC THEN RES_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [sock_with_fd_def], (* recvfrom ok *) REPEAT GEN_TAC THEN STRIP_TAC THEN undo_abbrevs THEN QCONTR_TAC THEN nres_search_then 1 false [] [] MP_TAC host_ok_recvfrom_ok THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, FDOM_FUPDATE, RIGHT_AND_OVER_OR, DISJ_IMP_THM, FORALL_AND_THM] THEN DISCH_THEN (res_search_then false [] [] ASSUME_TAC) THEN `~(fd' = fd)` by (DISCH_THEN SUBST_ALL_TAC THEN RES_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [sock_with_fd_def], (* select ok *) SIMP_TAC (srw_ss()) [FORALL_AND_THM, RIGHT_AND_OVER_OR, DISJ_IMP_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN nres_search_then 1 false [] [] MP_TAC host_ok_select_ok THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ, FDOM_FUPDATE, RIGHT_AND_OVER_OR, DISJ_IMP_THM, FORALL_AND_THM] THEN DISCH_THEN (res_search_then false [] [] ASSUME_TAC) THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [pred_setTheory.SUBSET_DEF], (* uniquely valued guff *) IMP_RES_THEN MP_TAC host_ok_uniquely_valued THEN ASM_SIMP_TAC (srw_ss()) [uniquely_valued_def, listTheory.EVERY_MEM] THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [sockfds_FOLDR_INSERT, IN_FOLDR_INSERT, listTheory.MEM_MAP] THEN PROVE_TAC [] ], progress "succeed - bind_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,NONE,SOME p1',NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[Sock_def], progress "succeed - bind_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,SOME i,SOME p1',NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[Sock_def, socket_ok_def, socket_srcdest_ok_thm], progress "succeed - bind_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_3", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,NONE,SOME p,NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[Sock_def], progress "succeed - bind_4" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "bind_4", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,SOME i,SOME p,NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[Sock_def, socket_ok_def, socket_srcdest_ok_thm], progress "connect_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "connect_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,ps1,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,SOME i1,SOME p1',SOME i,ps,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN IMP_RES_THEN MP_TAC host_ok_ifd_set_ok THEN ASM_SIMP_TAC (srw_ss() ++ SATISFY_ss)[Sock_def, socket_ok_def, socket_srcdest_ok_def, outroute_in_ifds, FC_accessors], progress "connect_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "connect_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,SOME i1,SOME p1,is2,ps2,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,SOME i1,SOME p1,SOME i,ps,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN SRW_TAC [SATISFY_ss] [Sock_def, socket_ok_def, socket_srcdest_ok_def], progress "succeed - disconnect_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "disconnect_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,is1,SOME p1,is2,ps2,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,NONE,SOME p1,NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN SRW_TAC [SATISFY_ss] [Sock_def, socket_ok_def, socket_srcdest_ok_def], progress "succeed - disconnect_2" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "disconnect_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = Sock(fd,NONE,NONE,NONE,NONE,es,f,mq)` THEN Q.ABBREV_TAC `s = Sock(fd,NONE,SOME p1,NONE,NONE,es,f,mq)` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s`] THEN IMP_RES_TAC FC_SC_OK THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [Sock_def] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN SRW_TAC [SATISFY_ss] [Sock_def, socket_ok_def, socket_srcdest_ok_def], progress "succeed - getsockname_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "getsockname_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN CONJ_TAC THENL [ALL_TAC, Cases_on `s.is1` THEN Cases_on `s.ps1` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[]] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN SIMP_TAC (srw_ss() ++ OL_ss) [RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM, LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM] THEN PROVE_TAC [TypeBase.nchotomy_of "option"], progress "succeed - getpeername_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "getpeername_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN CONJ_TAC THENL [ALL_TAC, Cases_on `s.is2` THEN Cases_on `s.ps2` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[]] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN SIMP_TAC (srw_ss() ++ OL_ss) [RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM, LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM] THEN PROVE_TAC [TypeBase.nchotomy_of "option"], progress "succeed - geterr_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "geterr_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN CONJ_TAC THENL [ALL_TAC, Cases_on `s.es` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[]] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN CONJ_TAC THENL [ DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s with fd := fd`, `s with <| fd := fd; es := NONE |>`] THEN ASM_SIMP_TAC (srw_ss()) [FC_SC_OK] THEN `socket_ok ifds (s with fd := fd)` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN SRW_TAC [SATISFY_ss][socket_ok_def, socket_srcdest_ok_def], SIMP_TAC (srw_ss() ++ OL_ss) [RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM, LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM] THEN PROVE_TAC [TypeBase.nchotomy_of "option"] ], progress "succeed - getsockopt_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "getsockopt_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "succeed - setsockopt_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "setsockopt_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s with fd := fd`, `s with <| fd := fd; f := f'|>`] THEN ASM_SIMP_TAC (srw_ss()) [FC_SC_OK] THEN `socket_ok ifds (s with fd := fd)` by PROVE_TAC [FC_host_ok_socket_ok] THEN FIRST_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN IMP_RES_THEN MP_TAC socket_ok_ps1_NONE THEN SIMP_TAC (srw_ss()) [], progress "succeed - sendto_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN `MEM (s with es := NONE) h0.s` by ASM_SIMP_TAC (srw_ss()) [SC_MEM] THEN `h0.ifds = h'.ifds` by ASM_SIMP_TAC (srw_ss()) [] THEN `socket_ok h0.ifds (s with es := NONE)` by PROVE_TAC [host_ok_socket_ok] THEN CONJ_TAC THENL [ (* h.s ok *) DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s with es := NONE`, `s with <| ps1 := SOME p1'; es := NONE|>`] THEN ASM_SIMP_TAC (srw_ss())[] THEN MATCH_MP_TAC (REWRITE_RULE [AND_IMP_INTRO] socket_ok_components) THEN Q.EXISTS_TAC `s with es := NONE` THEN SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [], (* outputq_ok *) `ifd_set_ok h0.ifds` by IMP_RES_TAC host_ok_ifd_set_ok THEN `ifd_set_ok h'.ifds` by PROVE_TAC [] THEN `outputq_ok(h0.oq,h0.oqf)` by IMP_RES_TAC host_ok_outputq_ok THEN `socket_srcdest_ok h0.ifds (s.is1,s.ps1,s.is2,s.ps2)` by (FULL_SIMP_TAC (srw_ss()) [socket_ok_def]) THEN `socket_srcdest_ok h'.ifds (s.is1,SOME p1',s.is2,s.ps2)` by PROVE_TAC [new_ps1_socket_srcdest_ok] THEN Q.SUBGOAL_THEN `(?i. s.is2 = SOME i) \/ (?i p. ips = SOME(i,p))` ASSUME_TAC THENL [PROVE_TAC [TypeBase.nchotomy_of "prod", TypeBase.nchotomy_of "option"], ALL_TAC] THEN DISJ2_TAC THEN nres_search_then 3 false [] [] MP_TAC dosend_msg_oq_ok THEN DISCH_THEN (MATCH_MP_TAC o REWRITE_RULE [AND_IMP_INTRO]) THEN ASM_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [] ], progress "succeed - recvfrom_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN CONJ_TAC THENL [ALL_TAC, Cases_on `ps3` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[]] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN CONJ_TAC THENL [ Q.ABBREV_TAC `s0 = s with <| ps1 := SOME p1; es := NONE; mq := (IP(i3,i4,UDP(ps3,ps4,data)),ifid)::mq |>` THEN Q.ABBREV_TAC `s' = s with <| ps1 := SOME p1; es := NONE; mq := mq |>` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [FC_SC_OK] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN SIMP_TAC (srw_ss() ++ SATISFY_ss) [socket_ok_def], Cases_on `ps3` THEN SIMP_TAC (srw_ss() ++ OL_ss)[] ], progress "succeed - close_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "close_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN CONJ_TAC THENL [ ALL_TAC, SIMP_TAC (srw_ss() ++ OL_ss) [ FDOM_FUPDATE, o_f_DEF, htsType_def, IN_tlang_typing, TNet_auxfnsTheory.zombify_def ] ] THEN ASM_SIMP_TAC (srw_ss()) [host_ok_thm] THEN REPEAT CONJ_TAC THENL [ (* ifd set *) IMP_RES_THEN MP_TAC host_ok_ifd_set_ok THEN ASM_SIMP_TAC (srw_ss()) [], (* s1 half of socket list ok *) IMP_RES_THEN MP_TAC host_ok_every_socket_ok THEN ASM_SIMP_TAC (srw_ss()) [], (* s2 half of socket list ok *) IMP_RES_THEN MP_TAC host_ok_every_socket_ok THEN ASM_SIMP_TAC (srw_ss()) [], (* outputq_ok *) IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN ASM_SIMP_TAC (srw_ss()) [], (* ret threads ok *) ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, o_f_DEF, FDOM_FUPDATE, TNet_auxfnsTheory.zombify_def, zombify_EQ_Ret, FAPPLY_FUPD_EQ] THEN REPEAT STRIP_TAC THEN undo_abbrevs THEN QCONTR_TAC THEN SRW_TAC [OL_ss][] THEN nres_search_then 1 false [] [] MATCH_MP_TAC host_ok_ret_ts_ok THEN SRW_TAC [][FAPPLY_FUPD_EQ, FDOM_FUPDATE] THEN PROVE_TAC [], (* sendto threads ok *) ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, o_f_DEF, FDOM_FUPDATE, DISJ_IMP_THM, FORALL_AND_THM, TNet_auxfnsTheory.zombify_def, zombify_EQ_Sendto, FAPPLY_FUPD_EQ] THEN REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN nres_search_then 1 false [] [] MP_TAC host_ok_sendto_ok THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN DISCH_THEN (MP_TAC o Q.SPECL [`fd`, `tid'`]) THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[sockfds_thm,sock_with_fd_APPEND, sock_with_fd_def], (* recvfrom threads OK *) ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, o_f_DEF, FDOM_FUPDATE, DISJ_IMP_THM, FORALL_AND_THM, TNet_auxfnsTheory.zombify_def, zombify_EQ_Recvfrom, FAPPLY_FUPD_EQ] THEN REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN nres_search_then 1 false [] [] MP_TAC host_ok_recvfrom_ok THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN DISCH_THEN (MP_TAC o Q.SPECL [`fd`, `tid'`]) THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[sockfds_thm,sock_with_fd_APPEND, sock_with_fd_def], (* select threads ok *) ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, o_f_DEF, FDOM_FUPDATE, DISJ_IMP_THM, FORALL_AND_THM, TNet_auxfnsTheory.zombify_def, zombify_EQ_Select, FAPPLY_FUPD_EQ] THEN REPEAT GEN_TAC THEN REPEAT (DISCH_THEN STRIP_ASSUME_TAC) THEN nres_search_then 1 false [] [] MP_TAC host_ok_select_ok THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN DISCH_THEN (MP_TAC o Q.SPEC `tid'`) THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[sockfds_thm,sock_with_fd_APPEND, sock_with_fd_def, LIST_TO_SET_APPEND, LIST_TO_SET_FILTER] THEN SIMP_TAC (srw_ss() ++ PRED_SET_ss) [pred_setTheory.SUBSET_DEF, DISJ_IMP_THM, FORALL_AND_THM, GSPECIFICATION] THEN mesonLib.MESON_TAC [], (* uniquely valued *) IMP_RES_THEN MP_TAC host_ok_uniquely_valued THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [uniquely_valued_APPEND, uniquely_valued_def, containerTheory.LIST_TO_SET, pred_setTheory.IN_DISJOINT] THEN mesonLib.MESON_TAC [] ], progress "succeed - getifaddrs_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "getifaddrs_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing, listTheory.MEM_MAP, pairTheory.UNCURRY, LEFT_IMP_EXISTS_THM] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d, listTheory.MEM_MAP, pairTheory.UNCURRY, LEFT_IMP_EXISTS_THM, LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM] THEN mesonLib.MESON_TAC [], progress "succeed - convert_port_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "convert_port_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "succeed - convert_ip_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "convert_ip_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "succeed - create_1" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [rid "create_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, EXISTS_OR_THM, RIGHT_AND_OVER_OR, retType_def, htsType_def, IN_tlang_typing] THEN ASM_SIMP_TAC (srw_ss()) [host_ok_thm, FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN REPEAT CONJ_TAC THENL [ (* ifds ok *) IMP_RES_THEN MP_TAC host_ok_ifd_set_ok THEN ASM_SIMP_TAC (srw_ss())[], (* sockets ok *) IMP_RES_THEN MP_TAC host_ok_every_socket_ok THEN ASM_SIMP_TAC (srw_ss())[], (* outputq ok *) IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN ASM_SIMP_TAC (srw_ss())[], (* ret states ok *) REPEAT STRIP_TAC THEN undo_abbrevs THEN QCONTR_TAC THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [] THEN nres_search_then 1 false [] [] MP_TAC host_ok_ret_ts_ok THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN PROVE_TAC [], (* sendto states ok *) nres_search_then 1 false [] [] MP_TAC host_ok_sendto_ok THEN ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN mesonLib.MESON_TAC [], (* recvfrom states ok *) nres_search_then 1 false [] [] MP_TAC host_ok_recvfrom_ok THEN ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN mesonLib.MESON_TAC [], (* select states ok *) nres_search_then 1 false [] [] MP_TAC host_ok_select_ok THEN ASM_SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, DISJ_IMP_THM, FORALL_AND_THM, FDOM_FUPDATE, FAPPLY_FUPD_EQ] THEN mesonLib.MESON_TAC [], (* uniquely_valued *) IMP_RES_THEN MP_TAC host_ok_uniquely_valued THEN ASM_SIMP_TAC (srw_ss())[] ] ]); val _ = print "\nProved characterisation for succeed category (4/8)\n"; val MEM_FILTER = prove( ``!l P x. MEM x (FILTER P l) = MEM x l /\ P x``, Induct THEN SRW_TAC [][listTheory.FILTER] THEN PROVE_TAC []); val slowsucceed_rids = prove( ``!rid h0 l h. rid /* slowsucceed */ h0 -- l --> h ==> rid IN {sendto_8; recvfrom_6; select_3; select_4; delay_3}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val ips_is2_imp = prove( ``!ips is2. ~(ips = NONE) \/ ~(is2 = NONE) ==> (?i:ip. is2 = SOME i) \/ (?i:ip p:port. ips = SOME(i,p))``, PROVE_TAC [TypeBase.nchotomy_of "option", TypeBase.nchotomy_of "prod"]); val slowsucceed_characterise = store_thm( "slowsucceed_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* slowsucceed */ h0 -- l --> h ==> host_ok h /\ ?tid ts v d0 d. (FAPPLY h.ts tid = Timed(Ret(TL_err(OK v)), d)) /\ (FAPPLY h0.ts tid = Timed(ts, d0)) /\ FAPPLY h0.ts tid IN OP2 /\ (l = Lh_tau) /\ !ty. ty IN htsType ts ==> tlang_typing (TL_err (OK v)) ty``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) slowsucceed_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "slowsucceed - sendto_8" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_8", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2, retType_def, htsType_def] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPD_EQ] THEN CONJ_TAC THENL [ ALL_TAC, Q.EXISTS_TAC `tid` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss)[htsType_def] ] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN IMP_RES_THEN MP_TAC host_ok_ifd_set_ok THEN IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN NTAC 2 STRIP_TAC THEN nres_search_then 2 false [] [] MP_TAC dosend_msg_oq_ok THEN ASM_SIMP_TAC (srw_ss())[] THEN Q.PAT_ASSUM `p \/ q` (DISJ_CASES_THEN (CONJUNCTS_THEN ASSUME_TAC)) THEN res_search_then true [][] ASSUME_TAC ips_is2_imp THENL [ `?p1. s.ps1 = SOME p1` by (nres_search_then 1 false [] [] MP_TAC host_ok_sendto_ok THEN DISCH_THEN (MP_TAC o Q.SPECL [`s.fd`, `tid`]) THEN nres_search_then 1 false [] [] MP_TAC host_ok_uniquely_valued THEN ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, simple_sock_with_fd_fiddle] THEN mesonLib.MESON_TAC [TypeBase.nchotomy_of "option"]), `?p1. socket_srcdest_ok h'.ifds (is1,SOME p1,is2,ps2) /\ (ps1 = SOME p1)` by (nres_search_then 1 false [] [] MP_TAC host_ok_sendto_ok THEN DISCH_THEN (MP_TAC o Q.SPECL [`s.fd`, `tid`]) THEN ASM_SIMP_TAC (srw_ss())[FDOM_FUPDATE] THEN mesonLib.MESON_TAC [TypeBase.nchotomy_of "option"]) ] THEN POP_ASSUM (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th]) THEN ASSUME_TAC th) THEN DISCH_THEN (nres_search_then 3 false [] [] MP_TAC) THEN DISCH_THEN (fn th => DISJ2_TAC THEN MATCH_MP_TAC th) THEN ASM_SIMP_TAC (srw_ss())[] THEN IMP_RES_THEN MP_TAC host_ok_socket_ok THEN DISCH_THEN (MP_TAC o Q.SPEC `s with es := NONE`) THEN ASM_SIMP_TAC (srw_ss()) [SC_MEM, socket_ok_def] THEN ASM_SIMP_TAC (srw_ss()) [socket_srcdest_ok_def] THEN POP_ASSUM STRIP_ASSUME_TAC THEN ASM_SIMP_TAC (srw_ss())[], progress "slowsucceed - recvfrom_6" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_6", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN CONJ_TAC THENL [ ALL_TAC, Q.EXISTS_TAC `tid` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [htsType_def] THEN Cases_on `ps3` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[] ] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN CONJ_TAC THENL [ALL_TAC, Cases_on `ps3` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss)[] ] THEN DISJ2_TAC THEN Q.ABBREV_TAC `s0 = s with <| ps1 := SOME p1; es := NONE; mq := (IP(i3,i4,UDP(ps3,ps4,data)),ifid)::mq|>` THEN Q.ABBREV_TAC `s' = s with <| ps1 := SOME p1; es := NONE; mq := mq |>` THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[FC_SC_OK] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[socket_ok_def, DISJ_IMP_THM, FORALL_AND_THM] THEN STRIP_TAC, progress "slowsucceed - select_3" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "select_3", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FAPPLY_FUPD_EQ] THEN CONJ_TAC THENL [ ALL_TAC, Q.EXISTS_TAC `tid` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [htsType_def, listTheory.MEM_MAP, MEM_FILTER, LEFT_IMP_EXISTS_THM] ] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN SIMP_TAC (srw_ss() ++ OL_ss) [listTheory.MEM_MAP, MEM_FILTER, LEFT_AND_EXISTS_THM, RIGHT_AND_EXISTS_THM, LEFT_IMP_EXISTS_THM] THEN mesonLib.MESON_TAC [], progress "slowsucceed - select_4" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "select_4", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FAPPLY_FUPD_EQ] THEN CONJ_TAC THENL [ ALL_TAC, Q.EXISTS_TAC `tid` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [htsType_def] ] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN mesonLib.MESON_TAC [], progress "slowsucceed - delay_3" THEN FULL_SIMP_TAC (srw_ss() ++ OL_ss) [rid "delay_3", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN CONJ_TAC THENL [ ALL_TAC, Q.EXISTS_TAC `tid` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [htsType_def] ] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] ]); val _ = "\nProved characterisation for slowsucceed category (5/8)\n"; val enter2_rids = prove( ``!rid h0 l h. rid /* enter2 */ h0 -- l --> h ==> rid IN {sendto_2; recvfrom_2; select_1; delay_1; console_print_1}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val enter2_characterise = store_thm( "enter2_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* enter2 */ h0 -- l --> h ==> host_ok h /\ ?tid f d0 ts d. (l = Lh_call(tid, f)) /\ (FAPPLY h0.ts tid = Timed(Run, d0)) /\ (FAPPLY h.ts tid IN OP2) /\ (FAPPLY h.ts tid = Timed(ts, d)) /\ retType f IN htsType ts``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) enter2_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "enter2 - sendto_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "sendto_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = s with es := NONE` THEN Q.ABBREV_TAC `s' = s0 with ps1 := SOME p1'` THEN `h0.s = SC s0` by SRW_TAC [][] THEN `socket_ok h0.ifds s0` by PROVE_TAC [SC_MEM, host_ok_socket_ok] THEN `uniquely_valued socket_fd (SC s0)` by PROVE_TAC [host_ok_uniquely_valued] THEN `(s0.fd = s'.fd) /\ (s.fd = s'.fd)` by SRW_TAC [][] THEN `uniquely_valued socket_fd (SC s')` by PROVE_TAC [uniquely_valued_diff_socks] THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [sockfds_SC, simple_sock_with_fd_fiddle] THEN FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP ips_is2_imp) THEN `socket_srcdest_ok h'.ifds (s.is1,SOME p1',s.is2,s.ps2)` by (Q.PAT_ASSUM `socket_ok foo bar` MP_TAC THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [socket_ok_def] THEN mesonLib.MESON_TAC [new_ps1_socket_srcdest_ok]) THEN res_search false [][] dosend_failing THEN ASM_SIMP_TAC (srw_ss())[] THEN CONJ_TAC THENL [ALL_TAC, undo_abbrevs THEN SRW_TAC [][]] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (ASM_SIMP_TAC (srw_ss()) [] THEN undo_abbrevs THEN SRW_TAC [][] THEN NO_TAC) THEN Q.PAT_ASSUM `socket_ok foo bar` MP_TAC THEN ASM_SIMP_TAC (srw_ss())[] THEN DISCH_THEN (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SRW_TAC [][], progress "enter2 - recvfrom_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "recvfrom_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN IMP_RES_TAC FC_SC_OK THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [sockfds_SC] THEN Q.ABBREV_TAC `s0 = s with <| es := NONE; mq := []|>` THEN Q.ABBREV_TAC `s' = s0 with ps1 := SOME p1'` THEN CONJ_TAC THENL [ DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`fc_sc FC`, `s0`, `s'`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [] THEN NO_TAC) THEN `socket_ok ifds s0` by PROVE_TAC [FC_host_ok_socket_ok] THEN POP_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[], `(s'.fd = s.fd) /\ (s0.fd = s.fd)` by (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[]) THEN IMP_RES_THEN MP_TAC host_ok_uniquely_valued THEN ASM_SIMP_TAC (srw_ss()) [FC_accessors] THEN STRIP_TAC THEN `uniquely_valued socket_fd (fc_sc FC s')` by PROVE_TAC [uniquely_valued_diff_socks] THEN ASM_SIMP_TAC (srw_ss()) [simple_sock_with_fd_fiddle] THEN undo_abbrevs THEN SIMP_TAC (srw_ss())[] ], progress "enter2 - select_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "select_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Cases_on `tms` THEN ASM_SIMP_TAC (srw_ss())[ TNet_typesTheory.time_lt_def, TNet_typesTheory.time_lte_def, TNet_typesTheory.time_zero_def, TNet_typesTheory.time_infty_def, TNet_typesTheory.time_def ] THEN `0 <= x` by PROVE_TAC [] THEN `?n:num. x = &n` by (POP_ASSUM MP_TAC THEN CONV_TAC intLib.COOPER_CONV) THEN POP_ASSUM SUBST_ALL_TAC THEN ASM_SIMP_TAC (srw_ss()) [TNet_host0Theory.real_of_int_def, intLib.COOPER_PROVE ``!n:num. &n < 0i = ~(0i <= &n)``, integerTheory.NUM_OF_INT] THEN `~(1000000 = 0r)` by SIMP_TAC (srw_ss()) [realTheory.REAL_INJ] THEN FIRST_ASSUM (fn th => CONV_TAC (LAND_CONV (REWR_CONV (MATCH_MP realTheory.REAL_EQ_LMUL2 th)))) THEN `0r < 1000000` by SIMP_TAC (srw_ss()) [realTheory.REAL_LT] THEN FIRST_ASSUM (fn th => CONV_TAC (RAND_CONV (REWR_CONV (GSYM (MATCH_MP realTheory.REAL_LT_LMUL th))))) THEN ASM_SIMP_TAC std_ss [realTheory.REAL_DIV_LMUL, realTheory.REAL_INJ, realTheory.REAL_MUL_RZERO, realTheory.REAL_LT] THEN Q.PAT_ASSUM `0i <= &n` MP_TAC THEN CONV_TAC intLib.COOPER_CONV, progress "enter2 - delay1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delay_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "enter2 - console_print_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "console_print_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] ]); val _ = print "\nProved characterisation for enter2 (6/8)\n"; val misc_rids = store_thm( "misc_rids", ``!rid h0 l h. rid /* misc */ h0 -- l --> h ==> rid IN {console_print_2; ret_1; delivery_out_1; delivery_out_martian; delivery_in_udp_1; delivery_in_udp_2; delivery_in_martian_3; delivery_in_icmp_1; delivery_in_icmp_2; delivery_loopback_udp_1; delivery_loopback_udp_2; delivery_loopback_icmp_1; delivery_loopback_icmp_2; epsilon_1}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val enqueue_ok = store_thm( "enqueue_ok", ``!oq' oqf' ok m oq0 oqf0. (oq',oqf',ok) IN enqueue(m,oq0,oqf0) /\ outputq_ok(oq0,oqf0) /\ msg_oq_ok m ==> outputq_ok(oq',oqf')``, REPEAT GEN_TAC THEN `?oql d. oq0 = Timed(oql,d)` by PROVE_TAC [oq_cases] THEN Cases_on `oqf0` THEN ASM_SIMP_TAC(srw_ss()) [TNet_auxfnsTheory.enqueue_def] THEN SRW_TAC [PRED_SET_ss][GSPECIFICATION, outputq_ok_def]); val lookup_SOME_ps1 = prove( ``!ifds s slist data. socket_ok ifds s ==> s IN lookup slist data ==> ?p. s.ps1 = SOME p``, REPEAT STRIP_TAC THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN `s.ps1 = NONE` by PROVE_TAC [TypeBase.nchotomy_of "option"] THEN IMP_RES_TAC ps1_NONE_all_NONE THEN FULL_SIMP_TAC (srw_ss()) [GSPECIFICATION, TNet_auxfnsTheory.match_def, TNet_auxfnsTheory.score_def, TNet_auxfnsTheory.lookup_def]); fun ts_tactic thm = nres_search_then 1 false [][]ASSUME_TAC thm THEN SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, o_f_DEF] THEN REPEAT GEN_TAC THEN Q.PAT_ASSUM `FEVERY P h0.ts` MP_TAC THEN SIMP_TAC (srw_ss()) [FEVERY_DEF, combinTheory.o_THM] THEN DISCH_THEN (MP_TAC o Q.SPEC `tid`) THEN NTAC 2 STRIP_TAC THEN POP_ASSUM (fn th => POP_ASSUM (fn impth => CHOOSE_THEN (ASSUME_TAC o SYM) (MATCH_MP impth th)) THEN ASSUME_TAC th) THEN ASM_SIMP_TAC (srw_ss())[] THEN DISCH_THEN SUBST_ALL_TAC THEN Q.PAT_ASSUM `Time_Pass_xd dur foo = SOME (Timed(x:hostThreadState, bar))` MP_TAC THEN `?ts d4. FAPPLY h0.ts tid = Timed(ts,d4)` by PROVE_TAC [TypeBase.nchotomy_of "timed", TypeBase.nchotomy_of "prod"] THEN ASM_SIMP_TAC (srw_ss()) [TNet_hostLTSTheory.Time_Pass_xd_def] THEN Cases_on `Time_Pass_d dur d4` THEN ASM_SIMP_TAC (srw_ss())[] THEN DISCH_THEN (CONJUNCTS_THEN SUBST_ALL_TAC) val Time_Pass_preserves_host_ok = store_thm( "Time_Pass_preserves_host_ok", ``!h0 dur h. host_ok h0 /\ (Time_Pass dur h0 = SOME h) ==> host_ok h``, REPEAT GEN_TAC THEN SIMP_TAC (srw_ss()) [TNet_hostLTSTheory.Time_Pass_def] THEN Cases_on `Urgent h0` THEN ASM_SIMP_TAC (srw_ss())[] THENL [ Cases_on `Time_Pass_h0 dur h0` THEN ASM_SIMP_TAC (srw_ss())[], ALL_TAC ] THEN SIMP_TAC (srw_ss()) [TNet_hostLTSTheory.Time_Pass_h0_def] THEN Cases_on `Time_Pass_ts dur h0.ts` THEN ASM_SIMP_TAC (srw_ss()) [] THEN Cases_on `Time_Pass_xd dur h0.oq` THEN ASM_SIMP_TAC (srw_ss()) [] THEN POP_ASSUM MP_TAC THEN `?oql d. h0.oq = Timed(oql,d)` by PROVE_TAC [oq_cases] THEN ASM_SIMP_TAC (srw_ss()) [TNet_hostLTSTheory.Time_Pass_xd_def, TNet_hostLTSTheory.Time_Pass_d_def] THEN COND_CASES_TAC THEN SIMP_TAC (srw_ss())[] THEN STRIP_TAC THEN undo_abbrevs THEN Q.PAT_ASSUM `Time_Pass_ts dur h0.ts = SOME x` MP_TAC THEN SIMP_TAC (srw_ss())[TNet_hostLTSTheory.Time_Pass_ts_def] THEN COND_CASES_TAC THEN SIMP_TAC (srw_ss())[] THEN REPEAT STRIP_TAC THEN undo_abbrevs THEN SIMP_TAC (srw_ss()) [host_ok_thm] THEN REPEAT CONJ_TAC THENL [ (* ifds ok *) PROVE_TAC [host_ok_ifd_set_ok], (* sockets ok *) PROVE_TAC [host_ok_every_socket_ok], (* outputq_ok *) IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN ASM_SIMP_TAC (srw_ss()) [outputq_ok_def], (* ret states ok *) ts_tactic host_ok_ret_ts_ok THEN PROVE_TAC [], (* sendto states ok *) ts_tactic host_ok_sendto_ok THEN PROVE_TAC [], (* recvfrom states ok *) ts_tactic host_ok_recvfrom_ok THEN PROVE_TAC [], (* select states ok *) ts_tactic host_ok_select_ok THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [TNet_hostLTSTheory.Time_Pass_d_def] THEN SRW_TAC [][] THEN PROVE_TAC [TNet_typesTheory.time_gte_def, TNet_typesTheory.time_lte_def], (* uniquely_valued *) PROVE_TAC [host_ok_uniquely_valued] ]); val misc_characterise = store_thm( "misc_characterise", ``!rid h0 l h. host_ok h0 /\ label_ok l /\ rid /* misc */ h0 -- l --> h ==> host_ok h /\ ((l = Lh_tau) ==> (h.ts = h0.ts))``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) misc_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "misc - console_print_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "console_print_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "misc - ret_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "ret_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "misc - delivery_out_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_out_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN PROVE_TAC [host_ok_outputq_ok,dequeue_ok], progress "misc - delivery_out_martian" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_out_martian", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN PROVE_TAC [host_ok_outputq_ok,dequeue_ok], progress "misc - delivery_in_udp_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_in_udp_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = s` THEN POP_ASSUM (K ALL_TAC) THEN Q.ABBREV_TAC `s = s0 with mq := APPEND s0.mq [(IP(i3,i4,UDP(ps3,ps4,data)),ifd'.ifid)]` THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s0`, `s`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[] THEN NO_TAC) THEN `h0.s = SC s0` by ASM_SIMP_TAC (srw_ss())[] THEN `socket_ok h0.ifds s0` by PROVE_TAC [SC_MEM, host_ok_socket_ok] THEN POP_ASSUM MP_TAC THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss()) [socket_ok_def, DISJ_IMP_THM, FORALL_AND_THM] THEN STRIP_TAC THEN REPEAT CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC) THENL [ Q.PAT_ASSUM `label_ok l` MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [TNet_oksTheory.msg_ok_def, TNet_typesTheory.IP_def, label_ok_def], ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ TNet_oksTheory.martian_def, TNet_typesTheory.IP_def, TNet_oksTheory.body_ips_def, pred_setTheory.IN_DISJOINT] THEN `i4 IN h0.ifds` by (ASM_SIMP_TAC (srw_ss() ++ SATISFY_ss) [ TNet_oksTheory.in_ifds_def]) THEN PROVE_TAC [pred_setTheory.IN_UNION, ifd_set_ok_MARTIAN, host_ok_ifd_set_ok], `socket_ok h0.ifds s0` by PROVE_TAC [SC_MEM, host_ok_socket_ok] THEN res_search false [] [] lookup_SOME_ps1 THEN SRW_TAC [][] ], progress "misc - delivery_in_udp_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_in_udp_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [] THEN IMP_RES_THEN ASSUME_TAC host_ok_outputq_ok THEN nres_search_then 2 false [] [] MP_TAC enqueue_ok THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ TNet_oksTheory.msg_oq_ok_def, TNet_typesTheory.IP_def, TNet_oksTheory.msg_ok_def, pred_setTheory.IN_DISJOINT] THEN PROVE_TAC [host_ok_ifd_set_ok, ifd_set_ok_MARTIAN], progress "misc - delivery_in_martian_3" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_in_martian_3", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def], progress "misc - delivery_in_icmp_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_in_icmp_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s`, `s with es := if ~(s.is2 = NONE) \/ ~s.f.bsdcompat then SOME ECONNREFUSED else s.es`] THEN ASM_SIMP_TAC (srw_ss()) [] THEN `(h0.ifds = h.ifds) /\ (h'.ifds = h.ifds) /\ (h0.s = SC s)` by SRW_TAC [][] THEN `socket_ok h'.ifds s` by PROVE_TAC [host_ok_socket_ok, SC_MEM] THEN res_search false [] [] lookup_SOME_ps1 THEN FIRST_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN ASM_SIMP_TAC (srw_ss()) [], progress "misc - delivery_in_icmp_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_in_icmp_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def], progress "misc - delivery_loopback_udp_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_loopback_udp_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN Q.ABBREV_TAC `s0 = s` THEN POP_ASSUM (K ALL_TAC) THEN Q.ABBREV_TAC `s = s0 with mq := APPEND s0.mq [(IP(i3,i4,UDP(ps3,ps4,data)),ifid)]` THEN CONJ_TAC THENL [ DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s0`, `s`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN SRW_TAC [][] THEN NO_TAC) THEN nres_search_then 1 false [] [] MP_TAC host_ok_socket_ok THEN DISCH_THEN (MP_TAC o Q.SPEC `s0`) THEN ASM_SIMP_TAC (srw_ss()) [SC_MEM] THEN undo_abbrevs THEN SIMP_TAC (srw_ss()) [socket_ok_def, DISJ_IMP_THM, FORALL_AND_THM] THEN STRIP_TAC THEN Q.ABBREV_TAC `m = IP(i3,i4,UDP(ps3,ps4,data))` THEN `h'.oq = h0.oq` by SRW_TAC [][] THEN `?oql d. h0.oq = Timed(oql,d)` by PROVE_TAC [oq_cases] THEN `MEM m oql` by PROVE_TAC [dequeue_is_member] THEN IMP_RES_TAC host_ok_outputq_ok THEN `msg_oq_ok m /\ msg_ok m` by (POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss())[outputq_ok_def, listTheory.EVERY_MEM] THEN ASM_SIMP_TAC (srw_ss()) [TNet_oksTheory.msg_oq_ok_def]) THEN REPEAT CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC) THENL [ Q.PAT_ASSUM `msg_oq_ok m` MP_TAC THEN undo_abbrevs THEN MP_TAC TNet_oksTheory.LOOPBACK_MARTIAN_DISJOINT THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [ TNet_oksTheory.martian_def, TNet_oksTheory.msg_oq_ok_def, TNet_oksTheory.body_ips_def, TNet_typesTheory.IP_def, pred_setTheory.IN_DISJOINT] THEN PROVE_TAC [], SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [GSPECIFICATION, TNet_auxfnsTheory.match_def, TNet_auxfnsTheory.score_def, TNet_auxfnsTheory.lookup_def] ], IMP_RES_THEN MP_TAC dequeue_ok THEN IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN ASM_SIMP_TAC (srw_ss())[] ], progress "misc - delivery_loopback_udp_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_loopback_udp_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN nres_search_then 1 false [] [] MP_TAC enqueue_ok THEN nres_search_then 1 false [] [] MP_TAC dequeue_ok THEN IMP_RES_TAC host_ok_outputq_ok THEN res_search_then false [] [] MP_TAC dequeue_msg_oq_ok THEN ASM_SIMP_TAC (srw_ss())[TNet_oksTheory.msg_oq_ok_def, TNet_typesTheory.IP_def, TNet_oksTheory.msg_ok_def] THEN REPEAT STRIP_TAC THEN DISJ2_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN MP_TAC TNet_oksTheory.LOOPBACK_MARTIAN_DISJOINT THEN ASM_SIMP_TAC (srw_ss() ++ PRED_SET_ss) [pred_setTheory.IN_DISJOINT] THEN PROVE_TAC [], progress "misc - delivery_loopback_icmp_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_loopback_icmp_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN CONJ_TAC THENL [ DISJ2_TAC THEN Q.ABBREV_TAC `s0 = s` THEN POP_ASSUM (K ALL_TAC) THEN Q.ABBREV_TAC `s = s0 with es := if ~(s0.is2 = NONE) \/ ~s0.f.bsdcompat then SOME ECONNREFUSED else s0.es` THEN MAP_EVERY Q.EXISTS_TAC [`SC`, `s0`, `s`] THEN REPEAT CONJ_TAC THEN TRY (undo_abbrevs THEN SRW_TAC [][] THEN NO_TAC) THEN IMP_RES_THEN (MP_TAC o Q.SPEC `s0`) host_ok_socket_ok THEN ASM_SIMP_TAC (srw_ss()) [SC_MEM] THEN STRIP_TAC THEN res_search false [] [] lookup_SOME_ps1 THEN FIRST_ASSUM (MATCH_MP_TAC o MATCH_MP socket_ok_components) THEN undo_abbrevs THEN ASM_SIMP_TAC (srw_ss())[], IMP_RES_THEN MP_TAC host_ok_outputq_ok THEN ASM_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [dequeue_ok] ], progress "misc - delivery_loopback_icmp_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "delivery_loopback_icmp_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d] THEN PROVE_TAC [host_ok_outputq_ok, dequeue_ok], progress "misc - epsilon_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "epsilon_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN PROVE_TAC [Time_Pass_preserves_host_ok] ]); val _ = print "\nProved characterisation for misc category (7/8)\n"; val exit_rids = store_thm( "exit_rids", ``!rid h0 l h. rid /* exit */ h0 -- l --> h ==> rid IN {exit_1; exit_2}``, SRW_TAC [PRED_SET_ss][host_redn_cases] THEN ASM_REWRITE_TAC []); val exit_characterise = store_thm( "exit_characterise", ``!rid h0 l h. host_ok h0 /\ rid /* exit */ h0 -- l --> h ==> host_ok h ``, REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [pred_setTheory.NOT_IN_EMPTY, pred_setTheory.IN_INSERT]) exit_rids THEN POP_ASSUM SUBST_ALL_TAC THENL [ progress "exit - exit_1" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "exit_1", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN MATCH_MP_TAC comp_host_ok THEN Q.EXISTS_TAC `h0` THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss) [FC_accessors, FUPD_11, FUPD_11a, FUPD_11b, FUPD_11c, FUPD_11d], progress "exit - exit_2" THEN POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss() ++ OL_ss) [rid "exit_2", FC_accessors, FAPPLY_FUPD_EQ, IN_OP2] THEN DISCH_THEN (REPEAT_TCL (CHOOSE_THEN ORELSE_TCL CONJUNCTS_THEN) ASSUME_TAC) THEN ASM_SIMP_TAC (srw_ss() ++ OL_ss ++ PRED_SET_ss) [ FC_accessors, FAPPLY_FUPD_EQ, retType_def, htsType_def] THEN SIMP_TAC (srw_ss()) [host_ok_thm, uniquely_valued_def, FDOM_FEMPTY] THEN MAP_EVERY (IMP_RES_THEN MP_TAC) [host_ok_ifd_set_ok, host_ok_outputq_ok] THEN SRW_TAC [][] ]); val _ = print "\nProved characterisation for exit category (8/8)\n"; val _ = print "Hurrah!\n"; val host_ok_invariant = store_thm( "host_ok_invariant", ``!h rid rcat l h'. host_ok h /\ label_ok l ==> rid /* rcat */ h -- l --> h' ==> host_ok h'``, REPEAT STRIP_TAC THEN Cases_on `rcat` THENL [ PROVE_TAC [succeed_characterise], PROVE_TAC [fail_characterise], PROVE_TAC [badfail_characterise], PROVE_TAC [slowsucceed_characterise], PROVE_TAC [slowfail_characterise], PROVE_TAC [exit_characterise], PROVE_TAC [enter2_characterise], PROVE_TAC [misc_characterise] ]); (* val htsType_empty = prove( ``!h. host_ok h ==> !tid ts d. (FAPPLY h.ts = Timed(ts,d)) /\ (htsType ts = {}) ==> (ts = Run)``, SRW_TAC [][host_ok_thm] THEN Cases_on `h.t` THEN FULL_SIMP_TAC (srw_ss() ++ PRED_SET_ss)[htsType_def, pred_setTheory.EXTENSION] THEN SIMP_TAC std_ss [SPECIFICATION] THEN PROVE_TAC []); val noRet_def = Define` noRet h0 h = ?l rid rcat. label_ok l /\ rid /* rcat */ h0 -- l --> h /\ !v. ~(l = Lh_return v)`; val noRet1_subject_reduction = store_thm( "noRet1_subject_reduction", ``!h0 h tid ts0 d0. noRet h0 h ==> host_ok h0 /\ (FAPPLY h0.ts tid = Timed(ts0, d0)) /\ ~(htsType ts0 = {}) /\ FDOM h.ts tid /\ (* i.e. not just exited *) (!d'. ~(FAPPLY h.ts tid = Timed(Zombie, d))) ==> host_ok h /\ ?d ts. (FAPPLY h0.ts tid = Timed(ts, d)) /\ (htsType ts = htsType ts0)``, (htsType h.t = htsType h0.t)``, REPEAT GEN_TAC THEN SIMP_TAC (srw_ss()) [noRet_def, LEFT_IMP_EXISTS_THM] THEN REPEAT STRIP_TAC THEN res_search false [] [] host_ok_invariant THEN Cases_on `l` THEN FULL_SIMP_TAC (srw_ss()) [label_ok_def]); val noRet_subject_reduction = store_thm( "noRet_subject_reduction", ``!h0 h. RTC noRet h0 h ==> host_ok h0 /\ ~(htsType h0.t = {}) ==> host_ok h /\ (htsType h.t = htsType h0.t)``, HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [] THEN PROVE_TAC [noRet1_subject_reduction]); val well_typed_calls = store_thm( "well_typed_calls", ``!h0 rid1 rcat1 f h1 h2 h r rid2 rcat2. host_ok h0 /\ rid1 /* rcat1 */ h0 -- Lh_call f --> h1 /\ RTC noRet h1 h2 ==> rid2 /* rcat2 */ h2 -- Lh_return r --> h ==> tlang_typing r (retType f)``, REPEAT STRIP_TAC THEN IMP_RES_TAC ((SIMP_RULE (srw_ss()) [label_ok_def] o Q.INST [`h` |-> `h0`, `h'` |-> `h1`, `l` |-> `Lh_call f`] o SPEC_ALL) host_ok_invariant) THEN `~(htsType h1.t = {})` by (STRIP_TAC THEN FULL_SIMP_TAC (std_ss ++ PRED_SET_ss)[]) THEN `(htsType h2.t = htsType h1.t) /\ host_ok h2` by PROVE_TAC [noRet_subject_reduction] THEN res_search false [] [] ((SIMP_RULE (srw_ss()) [label_ok_def] o Q.INST [`h` |-> `h2`, `h'` |-> `h`, `l` |-> `Lh_return r`] o SPEC_ALL) host_ok_invariant) THEN PROVE_TAC []); *) val _ = export_theory();