signature TNet_NetworksTheory = sig type thm = Thm.thm (* Definitions *) val Empty_def : thm val Extern : thm val HC : thm val Host : thm val HostId : thm val In : thm val Intern : thm val L_callHost : thm val L_callModule : thm val L_callStore : thm val L_conn : thm val L_console : thm val L_crash : thm val L_exit : thm val L_hostTau : thm val L_recvmsg : thm val L_retFromHost : thm val L_retFromStore : thm val L_retFromThread : thm val L_sendmsg : thm val L_threadTau : thm val L_time : thm val Lb : thm val Lm : thm val Ln : thm val Module : thm val Msg : thm val MsgProd_def : thm val Out : thm val Par : thm val Store : thm val StoreRet : thm val TNet_Networks0_def : thm val TNet_Networks10_def : thm val TNet_Networks11_def : thm val TNet_Networks12_def : thm val TNet_Networks13_def : thm val TNet_Networks14_def : thm val TNet_Networks15_def : thm val TNet_Networks16_def : thm val TNet_Networks17_def : thm val TNet_Networks18_def : thm val TNet_Networks19_def : thm val TNet_Networks1_def : thm val TNet_Networks20_def : thm val TNet_Networks21_def : thm val TNet_Networks22_def : thm val TNet_Networks23_def : thm val TNet_Networks24_def : thm val TNet_Networks25_def : thm val TNet_Networks26_def : thm val TNet_Networks27_def : thm val TNet_Networks28_def : thm val TNet_Networks2_def : thm val TNet_Networks3_def : thm val TNet_Networks4_def : thm val TNet_Networks5_def : thm val TNet_Networks6_def : thm val TNet_Networks7_def : thm val TNet_Networks8_def : thm val TNet_Networks9_def : thm val Tau : thm val Thread : thm val ThreadCreate : thm val dirn_BIJ : thm val dirn_TY_DEF : thm val dirn_case_def : thm val dirn_size_def : thm val dpropmax_def : thm val dpropmin_def : thm val dstore_def : thm val dthread_def : thm val execution_def : thm val hostComponent_TY_DEF : thm val hostComponent_case_def : thm val hostComponent_repfns : thm val hostComponent_size_def : thm val hostId_TY_DEF : thm val hostId_case_def : thm val hostId_repfns : thm val hostId_size_def : thm val host_component_ok_primitive_def : thm val host_ips_arg_munge_def : thm val host_ips_tupled_primitive_def : thm val hosts_primitive_def : thm val label0_TY_DEF : thm val label0_case_def : thm val label0_repfns : thm val label0_size_def : thm val label1_TY_DEF : thm val label1_case_def : thm val label1_repfns : thm val label1_size_def : thm val label2_TY_DEF : thm val label2_case_def : thm val label2_repfns : thm val label2_size_def : thm val label_TY_DEF : thm val label_case_def : thm val label_repfns : thm val label_size_def : thm val msg_dest_ips_arg_munge_def : thm val msg_dest_ips_tupled_primitive_def : thm val msg_src_ips_arg_munge_def : thm val msg_src_ips_tupled_primitive_def : thm val net_in_def : thm val network_TY_DEF : thm val network_case_def : thm val network_complete_ok_def : thm val network_lifted_lts : thm val network_lts : thm val network_ok_primitive_def : thm val network_repfns : thm val network_size_def : thm val origin_BIJ : thm val origin_TY_DEF : thm val origin_case_def : thm val origin_size_def : thm val sc : thm val store_ok_def : thm val sync_arg_munge_def : thm val sync_tupled_primitive_def : thm val thread_snippet_in_hc_arg_munge_def : thm val thread_snippet_in_hc_tupled_primitive_def : thm val thread_snippet_in_net_arg_munge_def : thm val thread_snippet_in_net_tupled_primitive_def : thm val threadids_arg_munge_def : thm val threadids_hc_primitive_def : thm val threadids_tupled_primitive_def : thm val visible_arg_munge_def : thm val visible_tupled_primitive_def : thm (* Theorems *) val dirn2num_11 : thm val dirn2num_In : thm val dirn2num_ONTO : thm val dirn2num_Out : thm val dirn2num_Tau : thm val dirn2num_num2dirn : thm val dirn_Axiom : thm val dirn_EQ_dirn : thm val dirn_case_cong : thm val dirn_distinct : thm val dirn_induction : thm val dirn_nchotomy : thm val hostComponent_11 : thm val hostComponent_Axiom : thm val hostComponent_case_cong : thm val hostComponent_distinct : thm val hostComponent_induction : thm val hostComponent_nchotomy : thm val hostId_11 : thm val hostId_Axiom : thm val hostId_case_cong : thm val hostId_induction : thm val hostId_nchotomy : thm val host_component_ok_def : thm val host_component_ok_ind : thm val host_ips_def : thm val host_ips_ind : thm val hosts_def : thm val hosts_ind : thm val label0_11 : thm val label0_Axiom : thm val label0_case_cong : thm val label0_distinct : thm val label0_induction : thm val label0_nchotomy : thm val label1_11 : thm val label1_Axiom : thm val label1_case_cong : thm val label1_distinct : thm val label1_induction : thm val label1_nchotomy : thm val label2_11 : thm val label2_Axiom : thm val label2_case_cong : thm val label2_distinct : thm val label2_induction : thm val label2_nchotomy : thm val label_11 : thm val label_Axiom : thm val label_case_cong : thm val label_distinct : thm val label_induction : thm val label_nchotomy : thm val msg_dest_ips_def : thm val msg_dest_ips_ind : thm val msg_src_ips_def : thm val msg_src_ips_ind : thm val network_11 : thm val network_Axiom : thm val network_case_cong : thm val network_distinct : thm val network_induction : thm val network_lifted_lts_cases : thm val network_lifted_lts_ind : thm val network_lifted_lts_rules : thm val network_nchotomy : thm val network_ok_def : thm val network_ok_ind : thm val num2dirn_11 : thm val num2dirn_ONTO : thm val num2dirn_dirn2num : thm val num2origin_11 : thm val num2origin_ONTO : thm val num2origin_origin2num : thm val origin2num_11 : thm val origin2num_Extern : thm val origin2num_Intern : thm val origin2num_ONTO : thm val origin2num_num2origin : thm val origin_Axiom : thm val origin_EQ_origin : thm val origin_case_cong : thm val origin_distinct : thm val origin_induction : thm val origin_nchotomy : thm val sc_cases : thm val sc_ind : thm val sc_rules : thm val sync_def : thm val sync_ind : thm val thread_snippet_in_hc_def : thm val thread_snippet_in_hc_ind : thm val thread_snippet_in_net_def : thm val thread_snippet_in_net_ind : thm val threadids_def : thm val threadids_hc_def : thm val threadids_hc_ind : thm val threadids_ind : thm val visible_def : thm val visible_ind : thm val TNet_Networks_grammars : parse_type.grammar * term_grammar.grammar val mc_store_ty : Type.hol_type val mc_store_aty : Term.term (* [TNet_hostLTS] Parent theory of "TNet_Networks" [TNet_threadAx] Parent theory of "TNet_Networks" [Empty_def] Definition |- Empty = TNet_Networks7 [Extern] Definition |- Extern = num2origin 1 [HC] Definition |- HC = TNet_Networks10 [Host] Definition |- Host = TNet_Networks1 [HostId] Definition |- HostId = TNet_Networks0 [In] Definition |- In = num2dirn 0 [Intern] Definition |- Intern = num2origin 0 [L_callHost] Definition |- L_callHost = TNet_Networks11 [L_callModule] Definition |- L_callModule = TNet_Networks13 [L_callStore] Definition |- L_callStore = TNet_Networks12 [L_conn] Definition |- L_conn = TNet_Networks24 [L_console] Definition |- L_console = TNet_Networks25 [L_crash] Definition |- L_crash = TNet_Networks19 [L_exit] Definition |- L_exit = TNet_Networks20 [L_hostTau] Definition |- L_hostTau = TNet_Networks23 [L_recvmsg] Definition |- L_recvmsg = TNet_Networks18 [L_retFromHost] Definition |- L_retFromHost = TNet_Networks14 [L_retFromStore] Definition |- L_retFromStore = TNet_Networks15 [L_retFromThread] Definition |- L_retFromThread = TNet_Networks16 [L_sendmsg] Definition |- L_sendmsg = TNet_Networks17 [L_threadTau] Definition |- L_threadTau = TNet_Networks22 [L_time] Definition |- L_time = TNet_Networks21 [Lb] Definition |- Lb = TNet_Networks26 [Lm] Definition |- Lm = TNet_Networks27 [Ln] Definition |- Ln = TNet_Networks28 [Module] Definition |- Module = TNet_Networks2 [Msg] Definition |- Msg = TNet_Networks9 [MsgProd_def] Definition |- (!m df. MsgProd m 0 df = Empty) /\ !m i df. MsgProd m (SUC i) df = Msg (Timed (m,df i)) Par MsgProd m i df [Out] Definition |- Out = num2dirn 1 [Par] Definition |- $Par = TNet_Networks8 [Store] Definition |- Store = TNet_Networks3 [StoreRet] Definition |- StoreRet = TNet_Networks4 [TNet_Networks0_def] Definition |- TNet_Networks0 = (\a. mk_hostId ((\a. CONSTR 0 a (\n. BOTTOM)) a)) [TNet_Networks10_def] Definition |- TNet_Networks10 = (\a. mk_network ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks11_def] Definition |- TNet_Networks11 = (\a. mk_label0 ((\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks12_def] Definition |- TNet_Networks12 = (\a. mk_label0 ((\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks13_def] Definition |- TNet_Networks13 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks14_def] Definition |- TNet_Networks14 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks15_def] Definition |- TNet_Networks15 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks16_def] Definition |- TNet_Networks16 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks17_def] Definition |- TNet_Networks17 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks18_def] Definition |- TNet_Networks18 = (\a. mk_label0 ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks19_def] Definition |- TNet_Networks19 = (\a. mk_label1 ((\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks1_def] Definition |- TNet_Networks1 = (\a. mk_hostComponent ((\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks20_def] Definition |- TNet_Networks20 = (\a. mk_label1 ((\a. CONSTR (SUC 0) (a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks21_def] Definition |- TNet_Networks21 = (\a. mk_label1 ((\a. CONSTR (SUC (SUC 0)) ((@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks22_def] Definition |- TNet_Networks22 = (\a. mk_label2 ((\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks23_def] Definition |- TNet_Networks23 = mk_label2 (CONSTR (SUC 0) ((@v. T),(@v. T),@v. T) (\n. BOTTOM)) [TNet_Networks24_def] Definition |- TNet_Networks24 = (\a. mk_label2 ((\a. CONSTR (SUC (SUC 0)) ((@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks25_def] Definition |- TNet_Networks25 = (\a. mk_label2 ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks26_def] Definition |- TNet_Networks26 = (\a. mk_label ((\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks27_def] Definition |- TNet_Networks27 = (\a. mk_label ((\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks28_def] Definition |- TNet_Networks28 = (\a. mk_label ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks2_def] Definition |- TNet_Networks2 = (\a. mk_hostComponent ((\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks3_def] Definition |- TNet_Networks3 = (\a. mk_hostComponent ((\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks4_def] Definition |- TNet_Networks4 = (\a. mk_hostComponent ((\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a)) [TNet_Networks5_def] Definition |- TNet_Networks5 = (\a. mk_hostComponent ((\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a)) [TNet_Networks6_def] Definition |- TNet_Networks6 = (\a. mk_hostComponent ((\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a)) [TNet_Networks7_def] Definition |- TNet_Networks7 = mk_network (CONSTR 0 ((@v. T),@v. T) (\n. BOTTOM)) [TNet_Networks8_def] Definition |- TNet_Networks8 = (\a0 a1. mk_network ((\a0 a1. CONSTR (SUC 0) ((@v. T),@v. T) (FCONS a0 (FCONS a1 (\n. BOTTOM)))) (dest_network a0) (dest_network a1))) [TNet_Networks9_def] Definition |- TNet_Networks9 = (\a. mk_network ((\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a)) [Tau] Definition |- Tau = num2dirn 2 [Thread] Definition |- Thread = TNet_Networks5 [ThreadCreate] Definition |- ThreadCreate = TNet_Networks6 [dirn_BIJ] Definition |- (!a. num2dirn (dirn2num a) = a) /\ !r. (\n. n < 3) r = (dirn2num (num2dirn r) = r) [dirn_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\n. n < 3) rep' [dirn_case_def] Definition |- (!x0 x1 x2. (case In of In -> x0 || Out -> x1 || Tau -> x2) = x0) /\ (!x0 x1 x2. (case Out of In -> x0 || Out -> x1 || Tau -> x2) = x1) /\ !x0 x1 x2. (case Tau of In -> x0 || Out -> x1 || Tau -> x2) = x2 [dirn_size_def] Definition |- !x. dirn_size x = 0 [dpropmax_def] Definition |- dpropmax = time 10 [dpropmin_def] Definition |- dpropmin = time 1 [dstore_def] Definition |- dstore = time 1 [dthread_def] Definition |- dthread = time 1 [execution_def] Definition |- !k states labels. execution k states labels = k >= 0 /\ !i. i >= 0 /\ i < k ==> states i --- labels i ---> states (SUC i) /\ visible (states i) (labels i) [hostComponent_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'hostComponent'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'hostComponent' a0) ==> 'hostComponent' a0) rep' [hostComponent_case_def] Definition |- (!f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (Host a) = f a) /\ (!f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (Module a) = f1 a) /\ (!f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (Store a) = f2 a) /\ (!f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (StoreRet a) = f3 a) /\ (!f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (Thread a) = f4 a) /\ !f f1 f2 f3 f4 f5 a. case f f1 f2 f3 f4 f5 (ThreadCreate a) = f5 a [hostComponent_repfns] Definition |- (!a. mk_hostComponent (dest_hostComponent a) = a) /\ !r. (\a0. !'hostComponent'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'hostComponent' a0) ==> 'hostComponent' a0) r = (dest_hostComponent (mk_hostComponent r) = r) [hostComponent_size_def] Definition |- (!f a. hostComponent_size f (Host a) = 1 + (\(x,y). (case x of T -> 0 || F -> 0) + host_size y) a) /\ (!f a. hostComponent_size f (Module a) = 1 + thread_size f a) /\ (!f a. hostComponent_size f (Store a) = 1) /\ (!f a. hostComponent_size f (StoreRet a) = 1 + timed_size (\(x,y). tid_size x + (\(x,y). TLang_type_size x + TLang_size y) y) a) /\ (!f a. hostComponent_size f (Thread a) = 1 + timed_size (\(x,y). tid_size x + (\(x,y). origin_size x + thread_size f y) y) a) /\ !f a. hostComponent_size f (ThreadCreate a) = 1 + timed_size (\(x,y). tid_size x + (\(x,y). origin_size x + (\(x,y). thread_size f x + thread_size f y) y) y) a [hostId_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'hostId'. (!a0. (?a. a0 = (\a. CONSTR 0 a (\n. BOTTOM)) a) ==> 'hostId' a0) ==> 'hostId' a0) rep' [hostId_case_def] Definition |- !f a. case f (HostId a) = f a [hostId_repfns] Definition |- (!a. mk_hostId (dest_hostId a) = a) /\ !r. (\a0. !'hostId'. (!a0. (?a. a0 = (\a. CONSTR 0 a (\n. BOTTOM)) a) ==> 'hostId' a0) ==> 'hostId' a0) r = (dest_hostId (mk_hostId r) = r) [hostId_size_def] Definition |- !a. hostId_size (HostId a) = 1 + string_size a [host_component_ok_primitive_def] Definition |- host_component_ok = WFREC (@R. WF R) (\host_component_ok a. case a of Host v1 -> (case v1 of (v7,v8) -> host_ok v8) || Module v2 -> thread_ok v2 /\ v2.initial IN v2.Module || Store v3 -> store_ok v3 || StoreRet v4 -> (case v4 of Timed v9 -> case v9 of (v10,v11) -> case v10 of (v12,v13) -> case v13 of (v14,v15) -> tlang_typing v15 v14) || Thread v5 -> (case v5 of Timed v16 -> case v16 of (v17,v18) -> case v17 of (v19,v20) -> case v20 of (v21,v22) -> thread_ok v22 /\ v22.initial NOTIN v22.Module /\ v22.initial NOTIN v22.Term) || ThreadCreate v6 -> case v6 of Timed v23 -> case v23 of (v24,v25) -> case v24 of (v26,v27) -> case v27 of (v28,v29) -> case v29 of (v30,v31) -> thread_ok v30 /\ thread_ok v31 /\ v30.initial IN v30.Rettl (retType (create ())) /\ v31.initial IN v31.Prog) [host_ips_arg_munge_def] Definition |- !x x1. host_ips x x1 = host_ips_tupled (x,x1) [host_ips_tupled_primitive_def] Definition |- host_ips_tupled = WFREC (@R. WF R /\ (!N2 i N1. R (N1,i) (N1 Par N2,i)) /\ !N1 i N2. R (N2,i) (N1 Par N2,i)) (\host_ips_tupled a. case a of (v,v1) -> case v of Empty -> F || v2 Par v3 -> host_ips_tupled (v2,v1) \/ host_ips_tupled (v3,v1) || Msg v4 -> F || HC v5 -> case v5 of (v6,v7) -> case v7 of Host v14 -> (case v14 of (v22,v23) -> v1 IN v23.ifds /\ v1 NOTIN LOOPBACK) || Module v15 -> F || Store v16 -> F || StoreRet v17 -> F || Thread v18 -> F || ThreadCreate v19 -> F) [hosts_primitive_def] Definition |- hosts = WFREC (@R. WF R /\ (!N2 N1. R N1 (N1 Par N2)) /\ !N1 N2. R N2 (N1 Par N2)) (\hosts a. case a of Empty -> {} || v Par v1 -> hosts v UNION hosts v1 || Msg v2 -> {} || HC v3 -> case v3 of (v4,v5) -> (if ?x. v5 = Host x then {v4} else {})) [label0_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'label0'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label0' a0) ==> 'label0' a0) rep' [label0_case_def] Definition |- (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_callHost a) = f a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_callStore a) = f1 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_callModule a) = f2 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_retFromHost a) = f3 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_retFromStore a) = f4 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_retFromThread a) = f5 a) /\ (!f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_sendmsg a) = f6 a) /\ !f f1 f2 f3 f4 f5 f6 f7 a. case f f1 f2 f3 f4 f5 f6 f7 (L_recvmsg a) = f7 a [label0_repfns] Definition |- (!a. mk_label0 (dest_label0 a) = a) /\ !r. (\a0. !'label0'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,(@v. T),(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC 0)))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC 0))))) ((@v. T),(@v. T),(@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC 0)))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC (SUC (SUC (SUC (SUC 0))))))) ((@v. T),(@v. T),(@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label0' a0) ==> 'label0' a0) r = (dest_label0 (mk_label0 r) = r) [label0_size_def] Definition |- (!a. label0_size (L_callHost a) = 1 + (\(x,y). tid_size x + LIB_interface_size y) a) /\ (!a. label0_size (L_callStore a) = 1 + (\(x,y). tid_size x + STORE_interface_size y) a) /\ (!a. label0_size (L_callModule a) = 1 + (\(x,y). tid_size x + MODULE_interface_size y) a) /\ (!a. label0_size (L_retFromHost a) = 1 + (\(x,y). tid_size x + TLang_size y) a) /\ (!a. label0_size (L_retFromStore a) = 1 + (\(x,y). tid_size x + TLang_size y) a) /\ (!a. label0_size (L_retFromThread a) = 1 + (\(x,y). tid_size x + TLang_size y) a) /\ (!a. label0_size (L_sendmsg a) = 1 + msg_size a) /\ !a. label0_size (L_recvmsg a) = 1 + msg_size a [label1_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'label1'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),a) (\n. BOTTOM)) a) ==> 'label1' a0) ==> 'label1' a0) rep' [label1_case_def] Definition |- (!f f1 f2 a. case f f1 f2 (L_crash a) = f a) /\ (!f f1 f2 a. case f f1 f2 (L_exit a) = f1 a) /\ !f f1 f2 a. case f f1 f2 (L_time a) = f2 a [label1_repfns] Definition |- (!a. mk_label1 (dest_label1 a) = a) /\ !r. (\a0. !'label1'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),a) (\n. BOTTOM)) a) ==> 'label1' a0) ==> 'label1' a0) r = (dest_label1 (mk_label1 r) = r) [label1_size_def] Definition |- (!a. label1_size (L_crash a) = 1 + hostId_size a) /\ (!a. label1_size (L_exit a) = 1 + hostId_size a) /\ !a. label1_size (L_time a) = 1 [label2_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'label2'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (a0 = CONSTR (SUC 0) ((@v. T),(@v. T),@v. T) (\n. BOTTOM)) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label2' a0) ==> 'label2' a0) rep' [label2_case_def] Definition |- (!f v f1 f2 a. case f v f1 f2 (L_threadTau a) = f a) /\ (!f v f1 f2. case f v f1 f2 L_hostTau = v) /\ (!f v f1 f2 a. case f v f1 f2 (L_conn a) = f1 a) /\ !f v f1 f2 a. case f v f1 f2 (L_console a) = f2 a [label2_repfns] Definition |- (!a. mk_label2 (dest_label2 a) = a) /\ !r. (\a0. !'label2'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (a0 = CONSTR (SUC 0) ((@v. T),(@v. T),@v. T) (\n. BOTTOM)) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label2' a0) ==> 'label2' a0) r = (dest_label2 (mk_label2 r) = r) [label2_size_def] Definition |- (!a. label2_size (L_threadTau a) = 1 + tid_size a) /\ (label2_size L_hostTau = 0) /\ (!a. label2_size (L_conn a) = 1 + case a of T -> 0 || F -> 0) /\ !a. label2_size (L_console a) = 1 + string_size a [label_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0. !'label'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label' a0) ==> 'label' a0) rep' [label_case_def] Definition |- (!f f1 f2 a. case f f1 f2 (Lb a) = f a) /\ (!f f1 f2 a. case f f1 f2 (Lm a) = f1 a) /\ !f f1 f2 a. case f f1 f2 (Ln a) = f2 a [label_repfns] Definition |- (!a. mk_label (dest_label a) = a) /\ !r. (\a0. !'label'. (!a0. (?a. a0 = (\a. CONSTR 0 (a,(@v. T),@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC 0) ((@v. T),a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0 = (\a. CONSTR (SUC (SUC 0)) ((@v. T),(@v. T),a) (\n. BOTTOM)) a) ==> 'label' a0) ==> 'label' a0) r = (dest_label (mk_label r) = r) [label_size_def] Definition |- (!a. label_size (Lb a) = 1 + (\(x,y). hostId_size x + (\(x,y). dirn_size x + label0_size y) y) a) /\ (!a. label_size (Lm a) = 1 + label1_size a) /\ !a. label_size (Ln a) = 1 + (\(x,y). hostId_size x + label2_size y) a [msg_dest_ips_arg_munge_def] Definition |- !x x1. msg_dest_ips x x1 = msg_dest_ips_tupled (x,x1) [msg_dest_ips_tupled_primitive_def] Definition |- msg_dest_ips_tupled = WFREC (@R. WF R /\ (!N2 i N1. R (N1,i) (N1 Par N2,i)) /\ !N1 i N2. R (N2,i) (N1 Par N2,i)) (\msg_dest_ips_tupled a. case a of (v,v1) -> case v of Empty -> F || v2 Par v3 -> msg_dest_ips_tupled (v2,v1) \/ msg_dest_ips_tupled (v3,v1) || Msg v4 -> (case v4 of Timed v6 -> case v6 of (v7,v8) -> v1 = v7.dest) || HC v5 -> case v5 of (v9,v10) -> F) [msg_src_ips_arg_munge_def] Definition |- !x x1. msg_src_ips x x1 = msg_src_ips_tupled (x,x1) [msg_src_ips_tupled_primitive_def] Definition |- msg_src_ips_tupled = WFREC (@R. WF R /\ (!N2 i N1. R (N1,i) (N1 Par N2,i)) /\ !N1 i N2. R (N2,i) (N1 Par N2,i)) (\msg_src_ips_tupled a. case a of (v,v1) -> case v of Empty -> F || v2 Par v3 -> msg_src_ips_tupled (v2,v1) \/ msg_src_ips_tupled (v3,v1) || Msg v4 -> (case v4 of Timed v6 -> case v6 of (v7,v8) -> v1 = v7.src) || HC v5 -> case v5 of (v9,v10) -> F) [net_in_def] Definition |- (!nhc. net_in nhc Empty = F) /\ (!nhc N1 N2. net_in nhc (N1 Par N2) = net_in nhc N1 \/ net_in nhc N2) /\ (!nhc mt. net_in nhc (Msg mt) = F) /\ !nhc nhc'. net_in nhc (HC nhc') = (nhc = nhc') [network_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\a0'. !'network'. (!a0'. (a0' = CONSTR 0 ((@v. T),@v. T) (\n. BOTTOM)) \/ (?a0 a1. (a0' = (\a0 a1. CONSTR (SUC 0) ((@v. T),@v. T) (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\ 'network' a0 /\ 'network' a1) \/ (?a. a0' = (\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0' = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),a) (\n. BOTTOM)) a) ==> 'network' a0') ==> 'network' a0') rep' [network_case_def] Definition |- (!v f f1 f2. case v f f1 f2 Empty = v) /\ (!v f f1 f2 a0 a1. case v f f1 f2 (a0 Par a1) = f a0 a1) /\ (!v f f1 f2 a. case v f f1 f2 (Msg a) = f1 a) /\ !v f f1 f2 a. case v f f1 f2 (HC a) = f2 a [network_complete_ok_def] Definition |- !N. network_complete_ok N = network_ok N /\ !n. (?hc. net_in (n,hc) N) ==> ?b h m st. net_in (n,Host (b,h)) N /\ net_in (n,Module m) N /\ net_in (n,Store st) N [network_lifted_lts] Definition |- network_lifted_lts = (\a0 a1 a2. !network_lifted_lts' network_lts'. (!a0 a1 a2. (?l. (a1 = SOME l) /\ network_lts' a0 l a2) \/ (a1 = NONE) /\ T ==> network_lifted_lts' a0 a1 a2) /\ (!a3 a4 a5. (?d n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Msg (Timed (m,d))) /\ dpropmin <= d /\ d <= dpropmax) \/ (?df n m k. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = MsgProd m k df) /\ k >= 2 /\ !i. 0 <= i /\ i < k ==> dpropmin <= df i /\ df i <= dpropmax) \/ (?n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Empty) /\ T) \/ (?n m. (a3 = Msg (Timed (m,time_zero))) /\ (a4 = Lb (n,Out,L_recvmsg m)) /\ (a5 = Empty) /\ T) \/ (?d tim m. (a3 = Msg (Timed (m,tim + d))) /\ (a4 = Lm (L_time d)) /\ (a5 = Msg (Timed (m,tim))) /\ d > 0) \/ (?d. (a3 = Empty) /\ (a4 = Lm (L_time d)) /\ (a5 = Empty) /\ 0 < d) \/ (?h n conn h' fv tid. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,In,L_callHost (tid,fv))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_call (tid,fv) ---> h') \/ (?h h' tid v n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,Out,L_retFromHost (tid,v))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_return (tid,v) ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,Out,L_sendmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (F,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_recvmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h))) /\ h -- Lh_recvmsg m ---> h') \/ (?h s h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_console s)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_console s ---> h') \/ (?n h h' conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_tau ---> h') \/ (?h d h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_epsilon d ---> h') \/ (?n conn h. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_conn ~conn)) /\ (a5 = HC (n,Host (~conn,h))) /\ T) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STnew (tlty,v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) NOTIN FDOM st) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In, L_callStore (tid,STset (tlty,Loc (tlty,x),v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n, StoreRet (Timed ((tid,TLty_one,TL_one ()),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) IN FDOM st) \/ (?st tlty x v n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STget (tlty,Loc (tlty,x))))) /\ (a5 = HC (n,Store st) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ (FAPPLY st (Loc (tlty,x)) = v)) \/ (?n tid tlty v d. (a3 = HC (n,StoreRet (Timed ((tid,tlty,v),d)))) /\ (a4 = Lb (n,Out,L_retFromStore (tid,v))) /\ (a5 = Empty)) \/ (?d n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Store st)) /\ 0 < d) \/ (?d tim n y. (a3 = HC (n,StoreRet (Timed (y,tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,StoreRet (Timed (y,tim)))) /\ 0 < d) \/ (?t t' fmv n tid. (a3 = HC (n,Module t)) /\ (a4 = Lb (n,In,L_callModule (tid,fmv))) /\ (a5 = HC (n,Thread (Timed ((tid,Extern,t'),dthread))) Par HC (n,Module t)) /\ t --- Lt_callModuleIn fmv ->>> t') \/ (?d n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Module t)) /\ 0 < d) \/ (?t t' n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_tau ->>> t') \/ (?t t' v n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetHostIn v ->>> t') \/ (?t t' v n tid org. (a3 = HC (n,Thread (Timed ((tid,org,t),dthread)))) /\ (a4 = Lb (n,In,L_retFromStore (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetStoreIn v ->>> t') \/ (?t t' fhv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,fhv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callHostOut fhv ->>> t') \/ (?t t' fsv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callStore (tid,fsv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callStoreOut fsv ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Extern,t),d)))) /\ (a4 = Lb (n,Out,L_retFromThread (tid,v))) /\ (a5 = Empty) /\ t --- Lt_RETOut v ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Intern,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,Intern,t'),time_infty)))) /\ t --- Lt_RETOut v ->>> t') \/ (?d n tid t tim org. (a3 = HC (n,Thread (Timed ((tid,org,t),tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t),tim)))) /\ 0 < d) \/ (?t t' s2 n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,create ()))) /\ (a5 = HC (n, ThreadCreate (Timed ((tid,org,t',t with initial := s2), time_infty)))) /\ t --- Lt_callHostCreateOut s2 ->>> t') \/ (?t' t'' tid tid' n t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (OK tid')))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread))) Par HC (n,Thread (Timed ((tid,Intern,t2),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (OK tid')) ->>> t'') \/ (?t' t'' e n tid t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (FAIL e)))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (FAIL e)) ->>> t'') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_crash n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n hcb. (a3 = HC (n,hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?n conn h h'. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_exit ---> h') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_exit n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Store FEMPTY)) /\ T) \/ (?n x. (a3 = HC (n,StoreRet x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Module t)) /\ T) \/ (?n x. (a3 = HC (n,Thread x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n x. (a3 = HC (n,ThreadCreate x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?N0 ll0 ll1 N0' N1 N1'. (a3 = N0 Par N1) /\ (a5 = N0' Par N1') /\ network_lifted_lts' N0 ll0 N0' /\ network_lifted_lts' N1 ll1 N1' /\ (sync ll0 ll1 = SOME a4)) \/ (?N0 N0'. network_lts' N0 a4 N0' /\ sc a3 N0 /\ sc N0' a5) ==> network_lts' a3 a4 a5) ==> network_lifted_lts' a0 a1 a2) [network_lts] Definition |- network_lts = (\a3 a4 a5. !network_lifted_lts' network_lts'. (!a0 a1 a2. (?l. (a1 = SOME l) /\ network_lts' a0 l a2) \/ (a1 = NONE) /\ T ==> network_lifted_lts' a0 a1 a2) /\ (!a3 a4 a5. (?d n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Msg (Timed (m,d))) /\ dpropmin <= d /\ d <= dpropmax) \/ (?df n m k. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = MsgProd m k df) /\ k >= 2 /\ !i. 0 <= i /\ i < k ==> dpropmin <= df i /\ df i <= dpropmax) \/ (?n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Empty) /\ T) \/ (?n m. (a3 = Msg (Timed (m,time_zero))) /\ (a4 = Lb (n,Out,L_recvmsg m)) /\ (a5 = Empty) /\ T) \/ (?d tim m. (a3 = Msg (Timed (m,tim + d))) /\ (a4 = Lm (L_time d)) /\ (a5 = Msg (Timed (m,tim))) /\ d > 0) \/ (?d. (a3 = Empty) /\ (a4 = Lm (L_time d)) /\ (a5 = Empty) /\ 0 < d) \/ (?h n conn h' fv tid. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,In,L_callHost (tid,fv))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_call (tid,fv) ---> h') \/ (?h h' tid v n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,Out,L_retFromHost (tid,v))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_return (tid,v) ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,Out,L_sendmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (F,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_recvmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h))) /\ h -- Lh_recvmsg m ---> h') \/ (?h s h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_console s)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_console s ---> h') \/ (?n h h' conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_tau ---> h') \/ (?h d h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_epsilon d ---> h') \/ (?n conn h. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_conn ~conn)) /\ (a5 = HC (n,Host (~conn,h))) /\ T) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STnew (tlty,v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) NOTIN FDOM st) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In, L_callStore (tid,STset (tlty,Loc (tlty,x),v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n, StoreRet (Timed ((tid,TLty_one,TL_one ()),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) IN FDOM st) \/ (?st tlty x v n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STget (tlty,Loc (tlty,x))))) /\ (a5 = HC (n,Store st) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ (FAPPLY st (Loc (tlty,x)) = v)) \/ (?n tid tlty v d. (a3 = HC (n,StoreRet (Timed ((tid,tlty,v),d)))) /\ (a4 = Lb (n,Out,L_retFromStore (tid,v))) /\ (a5 = Empty)) \/ (?d n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Store st)) /\ 0 < d) \/ (?d tim n y. (a3 = HC (n,StoreRet (Timed (y,tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,StoreRet (Timed (y,tim)))) /\ 0 < d) \/ (?t t' fmv n tid. (a3 = HC (n,Module t)) /\ (a4 = Lb (n,In,L_callModule (tid,fmv))) /\ (a5 = HC (n,Thread (Timed ((tid,Extern,t'),dthread))) Par HC (n,Module t)) /\ t --- Lt_callModuleIn fmv ->>> t') \/ (?d n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Module t)) /\ 0 < d) \/ (?t t' n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_tau ->>> t') \/ (?t t' v n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetHostIn v ->>> t') \/ (?t t' v n tid org. (a3 = HC (n,Thread (Timed ((tid,org,t),dthread)))) /\ (a4 = Lb (n,In,L_retFromStore (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetStoreIn v ->>> t') \/ (?t t' fhv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,fhv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callHostOut fhv ->>> t') \/ (?t t' fsv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callStore (tid,fsv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callStoreOut fsv ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Extern,t),d)))) /\ (a4 = Lb (n,Out,L_retFromThread (tid,v))) /\ (a5 = Empty) /\ t --- Lt_RETOut v ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Intern,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,Intern,t'),time_infty)))) /\ t --- Lt_RETOut v ->>> t') \/ (?d n tid t tim org. (a3 = HC (n,Thread (Timed ((tid,org,t),tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t),tim)))) /\ 0 < d) \/ (?t t' s2 n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,create ()))) /\ (a5 = HC (n, ThreadCreate (Timed ((tid,org,t',t with initial := s2), time_infty)))) /\ t --- Lt_callHostCreateOut s2 ->>> t') \/ (?t' t'' tid tid' n t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (OK tid')))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread))) Par HC (n,Thread (Timed ((tid,Intern,t2),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (OK tid')) ->>> t'') \/ (?t' t'' e n tid t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (FAIL e)))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (FAIL e)) ->>> t'') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_crash n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n hcb. (a3 = HC (n,hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?n conn h h'. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_exit ---> h') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_exit n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Store FEMPTY)) /\ T) \/ (?n x. (a3 = HC (n,StoreRet x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Module t)) /\ T) \/ (?n x. (a3 = HC (n,Thread x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n x. (a3 = HC (n,ThreadCreate x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?N0 ll0 ll1 N0' N1 N1'. (a3 = N0 Par N1) /\ (a5 = N0' Par N1') /\ network_lifted_lts' N0 ll0 N0' /\ network_lifted_lts' N1 ll1 N1' /\ (sync ll0 ll1 = SOME a4)) \/ (?N0 N0'. network_lts' N0 a4 N0' /\ sc a3 N0 /\ sc N0' a5) ==> network_lts' a3 a4 a5) ==> network_lts' a3 a4 a5) [network_ok_primitive_def] Definition |- network_ok = WFREC (@R. WF R /\ (!N' N. R N (N Par N')) /\ !N N'. R N' (N Par N')) (\network_ok a. case a of Empty -> T || v Par v1 -> network_ok v /\ network_ok v1 /\ ~(?i. host_ips v i /\ host_ips v1 i) /\ (!n x x'. ~(net_in (n,Host x) v /\ net_in (n,Host x') v1)) /\ (!n y y'. ~(net_in (n,Module y) v /\ net_in (n,Module y') v1)) /\ (!n z z'. ~(net_in (n,Store z) v /\ net_in (n,Store z') v1)) /\ (!n tid. ~(thread_snippet_in_net (n,tid) v /\ thread_snippet_in_net (n,tid) v1)) /\ (!n tid t d b h org. net_in (n,Thread (Timed ((tid,org,t),d))) (v Par v1) /\ net_in (n,Host (b,h)) (v Par v1) ==> tid IN FDOM h.ts) /\ (!n tid t t' d b h org. net_in (n,ThreadCreate (Timed ((tid,org,t,t'),d))) (v Par v1) /\ net_in (n,Host (b,h)) (v Par v1) ==> tid IN FDOM h.ts) || Msg v2 -> (case v2 of Timed v4 -> case v4 of (v5,v6) -> msg_ok v5 /\ time_zero <= v6 /\ v6 < time_infty) || HC v3 -> case v3 of (v7,v8) -> host_component_ok v8) [network_repfns] Definition |- (!a. mk_network (dest_network a) = a) /\ !r. (\a0'. !'network'. (!a0'. (a0' = CONSTR 0 ((@v. T),@v. T) (\n. BOTTOM)) \/ (?a0 a1. (a0' = (\a0 a1. CONSTR (SUC 0) ((@v. T),@v. T) (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\ 'network' a0 /\ 'network' a1) \/ (?a. a0' = (\a. CONSTR (SUC (SUC 0)) (a,@v. T) (\n. BOTTOM)) a) \/ (?a. a0' = (\a. CONSTR (SUC (SUC (SUC 0))) ((@v. T),a) (\n. BOTTOM)) a) ==> 'network' a0') ==> 'network' a0') r = (dest_network (mk_network r) = r) [network_size_def] Definition |- (!f. network_size f Empty = 0) /\ (!f a0 a1. network_size f (a0 Par a1) = 1 + (network_size f a0 + network_size f a1)) /\ (!f a. network_size f (Msg a) = 1 + timed_size msg_size a) /\ !f a. network_size f (HC a) = 1 + (\(x,y). hostId_size x + hostComponent_size f y) a [origin_BIJ] Definition |- (!a. num2origin (origin2num a) = a) /\ !r. (\n. n < 2) r = (origin2num (num2origin r) = r) [origin_TY_DEF] Definition |- ?rep'. TYPE_DEFINITION (\n. n < 2) rep' [origin_case_def] Definition |- (!x0 x1. (case Intern of Intern -> x0 || Extern -> x1) = x0) /\ !x0 x1. (case Extern of Intern -> x0 || Extern -> x1) = x1 [origin_size_def] Definition |- !x. origin_size x = 0 [sc] Definition |- sc = (\a0 a1. !sc'. (!a0 a1. (a1 = a0 Par Empty) \/ (?N N'. (a0 = N Par N') /\ (a1 = N' Par N)) \/ (?N N' N''. (a0 = N Par (N' Par N'')) /\ (a1 = N Par N' Par N'')) \/ (?N1 N1' N2 N2'. (a0 = N1 Par N2) /\ (a1 = N2' Par N2') /\ sc' N1 N1' /\ sc' N2 N2') \/ (a1 = a0) \/ sc' a1 a0 \/ (?N'. sc' a0 N' /\ sc' N' a1) ==> sc' a0 a1) ==> sc' a0 a1) [store_ok_def] Definition |- !st. store_ok st = !i tlty. Loc (tlty,i) IN FDOM st ==> tlang_typing (FAPPLY st (Loc (tlty,i))) tlty [sync_arg_munge_def] Definition |- !x x1. sync x x1 = sync_tupled (x,x1) [sync_tupled_primitive_def] Definition |- sync_tupled = WFREC (@R. WF R) (\sync_tupled a. case a of (v,v1) -> case v of NONE -> (case v1 of NONE -> NONE || SOME v3 -> case v3 of Lb v4 -> SOME (Lb v4) || Lm v5 -> NONE || Ln v6 -> SOME (Ln v6)) || SOME v2 -> case v2 of Lb v7 -> (case v7 of (v16,v17) -> case v17 of (v24,v25) -> case v1 of NONE -> SOME (Lb (v16,v24,v25)) || SOME v26 -> case v26 of Lb v27 -> (case v27 of (v30,v31) -> case v31 of (v32,v33) -> (if (v16 = v30) /\ (v25 = v33) /\ ((v24 = In) /\ (v32 = Out) \/ (v32 = In) /\ (v24 = Out)) then SOME (Lb (v16,Tau, v25)) else NONE)) || Lm v28 -> NONE || Ln v29 -> NONE) || Lm v8 -> (case v1 of NONE -> NONE || SOME v34 -> case v34 of Lb v35 -> NONE || Lm v36 -> (if v8 = v36 then SOME (Lm v8) else NONE) || Ln v37 -> NONE) || Ln v9 -> case v1 of NONE -> SOME (Ln v9) || SOME v38 -> case v38 of Lb v39 -> NONE || Lm v40 -> NONE || Ln v41 -> NONE) [thread_snippet_in_hc_arg_munge_def] Definition |- !x x1. thread_snippet_in_hc x x1 = thread_snippet_in_hc_tupled (x,x1) [thread_snippet_in_hc_tupled_primitive_def] Definition |- thread_snippet_in_hc_tupled = WFREC (@R. WF R) (\thread_snippet_in_hc_tupled a. case a of (v,v1) -> case v1 of Host v2 -> F || Module v3 -> F || Store v4 -> F || StoreRet v5 -> F || Thread v6 -> (case v6 of Timed v8 -> case v8 of (v9,v10) -> case v9 of (v11,v12) -> case v12 of (v13,v14) -> v = v11) || ThreadCreate v7 -> case v7 of Timed v15 -> case v15 of (v16,v17) -> case v16 of (v18,v19) -> case v19 of (v20,v21) -> case v21 of (v22,v23) -> v = v18) [thread_snippet_in_net_arg_munge_def] Definition |- !x x1. thread_snippet_in_net x x1 = thread_snippet_in_net_tupled (x,x1) [thread_snippet_in_net_tupled_primitive_def] Definition |- thread_snippet_in_net_tupled = WFREC (@R. WF R /\ (!N2 N1 nt. R (nt,N1) (nt,N1 Par N2)) /\ !N1 N2 nt. R (nt,N2) (nt,N1 Par N2)) (\thread_snippet_in_net_tupled a. case a of (v,v1) -> case v1 of Empty -> F || v2 Par v3 -> thread_snippet_in_net_tupled (v,v2) \/ thread_snippet_in_net_tupled (v,v3) || Msg v4 -> F || HC v5 -> case v5 of (v6,v7) -> (FST v = v6) /\ thread_snippet_in_hc (SND v) v7) [threadids_arg_munge_def] Definition |- !x x1. threadids x x1 = threadids_tupled (x,x1) [threadids_hc_primitive_def] Definition |- threadids_hc = WFREC (@R. WF R) (\threadids_hc a. case a of Host v -> (case v of (v6,v7) -> {}) || Module v1 -> {} || Store v2 -> {} || StoreRet v3 -> {} || Thread v4 -> (case v4 of Timed v8 -> case v8 of (v9,v10) -> case v9 of (v11,v12) -> case v12 of (v13,v14) -> {v11}) || ThreadCreate v5 -> case v5 of Timed v15 -> case v15 of (v16,v17) -> case v16 of (v18,v19) -> case v19 of (v20,v21) -> case v21 of (v22,v23) -> {v18}) [threadids_tupled_primitive_def] Definition |- threadids_tupled = WFREC (@R. WF R /\ (!N2 n N1. R (N1,n) (N1 Par N2,n)) /\ !N1 n N2. R (N2,n) (N1 Par N2,n)) (\threadids_tupled a. case a of (v,v1) -> case v of Empty -> {} || v2 Par v3 -> threadids_tupled (v2,v1) UNION threadids_tupled (v3,v1) || Msg v4 -> {} || HC v5 -> case v5 of (v6,v7) -> (if v1 <> v6 then {} else threadids_hc v7)) [visible_arg_munge_def] Definition |- !x x1. visible x x1 = visible_tupled (x,x1) [visible_tupled_primitive_def] Definition |- visible_tupled = WFREC (@R. WF R) (\visible_tupled a. case a of (v,v1) -> case v1 of Lb v2 -> (case v2 of (v5,v6) -> case v6 of (v7,v8) -> case v7 of In -> (case v8 of L_callHost v9 -> (case v9 of (v17,v18) -> v17 NOTIN threadids v v5) || L_callStore v10 -> (case v10 of (v19,v20) -> v19 NOTIN threadids v v5) || L_callModule v11 -> (case v11 of (v21,v22) -> v21 NOTIN threadids v v5) || L_retFromHost v12 -> (case v12 of (v23,v24) -> F) || L_retFromStore v13 -> (case v13 of (v25,v26) -> F) || L_retFromThread v14 -> (case v14 of (v27,v28) -> F) || L_sendmsg v15 -> v5 NOTIN hosts v /\ v15.src NOTIN host_ips v /\ v15.dest IN host_ips v || L_recvmsg v16 -> F) || Out -> (case v8 of L_callHost v29 -> (case v29 of (v37,v38) -> F) || L_callStore v30 -> (case v30 of (v39,v40) -> F) || L_callModule v31 -> (case v31 of (v41,v42) -> F) || L_retFromHost v32 -> (case v32 of (v43,v44) -> v43 NOTIN threadids v v5) || L_retFromStore v33 -> (case v33 of (v45,v46) -> v45 NOTIN threadids v v5) || L_retFromThread v34 -> (case v34 of (v47,v48) -> T) || L_sendmsg v35 -> F || L_recvmsg v36 -> v5 NOTIN hosts v /\ v36.src IN host_ips v /\ v36.dest NOTIN host_ips v) || Tau -> T) || Lm v3 -> (case v3 of L_crash v49 -> T || L_exit v50 -> v50 IN hosts v || L_time v51 -> T) || Ln v4 -> T) [dirn2num_11] Theorem |- !a a'. (dirn2num a = dirn2num a') = (a = a') [dirn2num_In] Theorem |- dirn2num In = 0 [dirn2num_ONTO] Theorem |- !r. r < 3 = ?a. r = dirn2num a [dirn2num_Out] Theorem |- dirn2num Out = 1 [dirn2num_Tau] Theorem |- dirn2num Tau = 2 [dirn2num_num2dirn] Theorem |- !r. r < 3 = (dirn2num (num2dirn r) = r) [dirn_Axiom] Theorem |- !x0 x1 x2. ?f. (f In = x0) /\ (f Out = x1) /\ (f Tau = x2) [dirn_EQ_dirn] Theorem |- !a a'. (a = a') = (dirn2num a = dirn2num a') [dirn_case_cong] Theorem |- !M M' x0 x1 x2. (M = M') /\ ((M' = In) ==> (x0 = x0')) /\ ((M' = Out) ==> (x1 = x1')) /\ ((M' = Tau) ==> (x2 = x2')) ==> ((case M of In -> x0 || Out -> x1 || Tau -> x2) = case M' of In -> x0' || Out -> x1' || Tau -> x2') [dirn_distinct] Theorem |- ~(In = Out) /\ ~(In = Tau) /\ ~(Out = Tau) [dirn_induction] Theorem |- !P. P In /\ P Out /\ P Tau ==> !a. P a [dirn_nchotomy] Theorem |- !a. (a = In) \/ (a = Out) \/ (a = Tau) [hostComponent_11] Theorem |- (!a a'. (Host a = Host a') = (a = a')) /\ (!a a'. (Module a = Module a') = (a = a')) /\ (!a a'. (Store a = Store a') = (a = a')) /\ (!a a'. (StoreRet a = StoreRet a') = (a = a')) /\ (!a a'. (Thread a = Thread a') = (a = a')) /\ !a a'. (ThreadCreate a = ThreadCreate a') = (a = a') [hostComponent_Axiom] Theorem |- !f0 f1 f2 f3 f4 f5. ?fn. (!a. fn (Host a) = f0 a) /\ (!a. fn (Module a) = f1 a) /\ (!a. fn (Store a) = f2 a) /\ (!a. fn (StoreRet a) = f3 a) /\ (!a. fn (Thread a) = f4 a) /\ !a. fn (ThreadCreate a) = f5 a [hostComponent_case_cong] Theorem |- !M M' f f1 f2 f3 f4 f5. (M = M') /\ (!a. (M' = Host a) ==> (f a = f' a)) /\ (!a. (M' = Module a) ==> (f1 a = f1' a)) /\ (!a. (M' = Store a) ==> (f2 a = f2' a)) /\ (!a. (M' = StoreRet a) ==> (f3 a = f3' a)) /\ (!a. (M' = Thread a) ==> (f4 a = f4' a)) /\ (!a. (M' = ThreadCreate a) ==> (f5 a = f5' a)) ==> (case f f1 f2 f3 f4 f5 M = case f' f1' f2' f3' f4' f5' M') [hostComponent_distinct] Theorem |- (!a' a. ~(Host a = Module a')) /\ (!a' a. ~(Host a = Store a')) /\ (!a' a. ~(Host a = StoreRet a')) /\ (!a' a. ~(Host a = Thread a')) /\ (!a' a. ~(Host a = ThreadCreate a')) /\ (!a' a. ~(Module a = Store a')) /\ (!a' a. ~(Module a = StoreRet a')) /\ (!a' a. ~(Module a = Thread a')) /\ (!a' a. ~(Module a = ThreadCreate a')) /\ (!a' a. ~(Store a = StoreRet a')) /\ (!a' a. ~(Store a = Thread a')) /\ (!a' a. ~(Store a = ThreadCreate a')) /\ (!a' a. ~(StoreRet a = Thread a')) /\ (!a' a. ~(StoreRet a = ThreadCreate a')) /\ !a' a. ~(Thread a = ThreadCreate a') [hostComponent_induction] Theorem |- !P. (!p. P (Host p)) /\ (!t. P (Module t)) /\ (!f. P (Store f)) /\ (!t. P (StoreRet t)) /\ (!t. P (Thread t)) /\ (!t. P (ThreadCreate t)) ==> !h. P h [hostComponent_nchotomy] Theorem |- !h. (?p. h = Host p) \/ (?t. h = Module t) \/ (?f. h = Store f) \/ (?t. h = StoreRet t) \/ (?t. h = Thread t) \/ ?t. h = ThreadCreate t [hostId_11] Theorem |- !a a'. (HostId a = HostId a') = (a = a') [hostId_Axiom] Theorem |- !f. ?fn. !a. fn (HostId a) = f a [hostId_case_cong] Theorem |- !M M' f. (M = M') /\ (!a. (M' = HostId a) ==> (f a = f' a)) ==> (case f M = case f' M') [hostId_induction] Theorem |- !P. (!s. P (HostId s)) ==> !h. P h [hostId_nchotomy] Theorem |- !h. ?s. h = HostId s [host_component_ok_def] Theorem |- (host_component_ok (Host (b,h)) = host_ok h) /\ (host_component_ok (Module s) = thread_ok s /\ s.initial IN s.Module) /\ (host_component_ok (Store st) = store_ok st) /\ (host_component_ok (StoreRet (Timed ((tid,tlty,v),d))) = tlang_typing v tlty) /\ (host_component_ok (Thread (Timed ((tid,org,s),d))) = thread_ok s /\ s.initial NOTIN s.Module /\ s.initial NOTIN s.Term) /\ (host_component_ok (ThreadCreate (Timed ((tid,org,s,s'),d))) = thread_ok s /\ thread_ok s' /\ s.initial IN s.Rettl (retType (create ())) /\ s'.initial IN s'.Prog) [host_component_ok_ind] Theorem |- !P. (!b h. P (Host (b,h))) /\ (!s. P (Module s)) /\ (!st. P (Store st)) /\ (!tid tlty v d. P (StoreRet (Timed ((tid,tlty,v),d)))) /\ (!tid org s d. P (Thread (Timed ((tid,org,s),d)))) /\ (!tid org s s' d. P (ThreadCreate (Timed ((tid,org,s,s'),d)))) ==> !v. P v [host_ips_def] Theorem |- (host_ips Empty i = F) /\ (host_ips (N1 Par N2) i = host_ips N1 i \/ host_ips N2 i) /\ (host_ips (Msg v0) i = F) /\ (host_ips (HC (v1,Host (conn,h))) i = i IN h.ifds /\ i NOTIN LOOPBACK) /\ (host_ips (HC (v2,ThreadCreate v13)) i = F) /\ (host_ips (HC (v2,Thread v12)) i = F) /\ (host_ips (HC (v2,StoreRet v11)) i = F) /\ (host_ips (HC (v2,Store v10)) i = F) /\ (host_ips (HC (v2,Module v9)) i = F) [host_ips_ind] Theorem |- !P. (!i. P Empty i) /\ (!N1 N2 i. P N1 i /\ P N2 i ==> P (N1 Par N2) i) /\ (!v0 i. P (Msg v0) i) /\ (!v1 conn h i. P (HC (v1,Host (conn,h))) i) /\ (!v2 v13 i. P (HC (v2,ThreadCreate v13)) i) /\ (!v2 v12 i. P (HC (v2,Thread v12)) i) /\ (!v2 v11 i. P (HC (v2,StoreRet v11)) i) /\ (!v2 v10 i. P (HC (v2,Store v10)) i) /\ (!v2 v9 i. P (HC (v2,Module v9)) i) ==> !v v1. P v v1 [hosts_def] Theorem |- (hosts Empty = {}) /\ (hosts (N1 Par N2) = hosts N1 UNION hosts N2) /\ (hosts (Msg mt) = {}) /\ (hosts (HC (n,hc)) = (if ?x. hc = Host x then {n} else {})) [hosts_ind] Theorem |- !P. P Empty /\ (!N1 N2. P N1 /\ P N2 ==> P (N1 Par N2)) /\ (!mt. P (Msg mt)) /\ (!n hc. P (HC (n,hc))) ==> !v. P v [label0_11] Theorem |- (!a a'. (L_callHost a = L_callHost a') = (a = a')) /\ (!a a'. (L_callStore a = L_callStore a') = (a = a')) /\ (!a a'. (L_callModule a = L_callModule a') = (a = a')) /\ (!a a'. (L_retFromHost a = L_retFromHost a') = (a = a')) /\ (!a a'. (L_retFromStore a = L_retFromStore a') = (a = a')) /\ (!a a'. (L_retFromThread a = L_retFromThread a') = (a = a')) /\ (!a a'. (L_sendmsg a = L_sendmsg a') = (a = a')) /\ !a a'. (L_recvmsg a = L_recvmsg a') = (a = a') [label0_Axiom] Theorem |- !f0 f1 f2 f3 f4 f5 f6 f7. ?fn. (!a. fn (L_callHost a) = f0 a) /\ (!a. fn (L_callStore a) = f1 a) /\ (!a. fn (L_callModule a) = f2 a) /\ (!a. fn (L_retFromHost a) = f3 a) /\ (!a. fn (L_retFromStore a) = f4 a) /\ (!a. fn (L_retFromThread a) = f5 a) /\ (!a. fn (L_sendmsg a) = f6 a) /\ !a. fn (L_recvmsg a) = f7 a [label0_case_cong] Theorem |- !M M' f f1 f2 f3 f4 f5 f6 f7. (M = M') /\ (!a. (M' = L_callHost a) ==> (f a = f' a)) /\ (!a. (M' = L_callStore a) ==> (f1 a = f1' a)) /\ (!a. (M' = L_callModule a) ==> (f2 a = f2' a)) /\ (!a. (M' = L_retFromHost a) ==> (f3 a = f3' a)) /\ (!a. (M' = L_retFromStore a) ==> (f4 a = f4' a)) /\ (!a. (M' = L_retFromThread a) ==> (f5 a = f5' a)) /\ (!a. (M' = L_sendmsg a) ==> (f6 a = f6' a)) /\ (!a. (M' = L_recvmsg a) ==> (f7 a = f7' a)) ==> (case f f1 f2 f3 f4 f5 f6 f7 M = case f' f1' f2' f3' f4' f5' f6' f7' M') [label0_distinct] Theorem |- (!a' a. ~(L_callHost a = L_callStore a')) /\ (!a' a. ~(L_callHost a = L_callModule a')) /\ (!a' a. ~(L_callHost a = L_retFromHost a')) /\ (!a' a. ~(L_callHost a = L_retFromStore a')) /\ (!a' a. ~(L_callHost a = L_retFromThread a')) /\ (!a' a. ~(L_callHost a = L_sendmsg a')) /\ (!a' a. ~(L_callHost a = L_recvmsg a')) /\ (!a' a. ~(L_callStore a = L_callModule a')) /\ (!a' a. ~(L_callStore a = L_retFromHost a')) /\ (!a' a. ~(L_callStore a = L_retFromStore a')) /\ (!a' a. ~(L_callStore a = L_retFromThread a')) /\ (!a' a. ~(L_callStore a = L_sendmsg a')) /\ (!a' a. ~(L_callStore a = L_recvmsg a')) /\ (!a' a. ~(L_callModule a = L_retFromHost a')) /\ (!a' a. ~(L_callModule a = L_retFromStore a')) /\ (!a' a. ~(L_callModule a = L_retFromThread a')) /\ (!a' a. ~(L_callModule a = L_sendmsg a')) /\ (!a' a. ~(L_callModule a = L_recvmsg a')) /\ (!a' a. ~(L_retFromHost a = L_retFromStore a')) /\ (!a' a. ~(L_retFromHost a = L_retFromThread a')) /\ (!a' a. ~(L_retFromHost a = L_sendmsg a')) /\ (!a' a. ~(L_retFromHost a = L_recvmsg a')) /\ (!a' a. ~(L_retFromStore a = L_retFromThread a')) /\ (!a' a. ~(L_retFromStore a = L_sendmsg a')) /\ (!a' a. ~(L_retFromStore a = L_recvmsg a')) /\ (!a' a. ~(L_retFromThread a = L_sendmsg a')) /\ (!a' a. ~(L_retFromThread a = L_recvmsg a')) /\ !a' a. ~(L_sendmsg a = L_recvmsg a') [label0_induction] Theorem |- !P. (!p. P (L_callHost p)) /\ (!p. P (L_callStore p)) /\ (!p. P (L_callModule p)) /\ (!p. P (L_retFromHost p)) /\ (!p. P (L_retFromStore p)) /\ (!p. P (L_retFromThread p)) /\ (!m. P (L_sendmsg m)) /\ (!m. P (L_recvmsg m)) ==> !l. P l [label0_nchotomy] Theorem |- !l. (?p. l = L_callHost p) \/ (?p. l = L_callStore p) \/ (?p. l = L_callModule p) \/ (?p. l = L_retFromHost p) \/ (?p. l = L_retFromStore p) \/ (?p. l = L_retFromThread p) \/ (?m. l = L_sendmsg m) \/ ?m. l = L_recvmsg m [label1_11] Theorem |- (!a a'. (L_crash a = L_crash a') = (a = a')) /\ (!a a'. (L_exit a = L_exit a') = (a = a')) /\ !a a'. (L_time a = L_time a') = (a = a') [label1_Axiom] Theorem |- !f0 f1 f2. ?fn. (!a. fn (L_crash a) = f0 a) /\ (!a. fn (L_exit a) = f1 a) /\ !a. fn (L_time a) = f2 a [label1_case_cong] Theorem |- !M M' f f1 f2. (M = M') /\ (!a. (M' = L_crash a) ==> (f a = f' a)) /\ (!a. (M' = L_exit a) ==> (f1 a = f1' a)) /\ (!a. (M' = L_time a) ==> (f2 a = f2' a)) ==> (case f f1 f2 M = case f' f1' f2' M') [label1_distinct] Theorem |- (!a' a. ~(L_crash a = L_exit a')) /\ (!a' a. ~(L_crash a = L_time a')) /\ !a' a. ~(L_exit a = L_time a') [label1_induction] Theorem |- !P. (!h. P (L_crash h)) /\ (!h. P (L_exit h)) /\ (!r. P (L_time r)) ==> !l. P l [label1_nchotomy] Theorem |- !l. (?h. l = L_crash h) \/ (?h. l = L_exit h) \/ ?r. l = L_time r [label2_11] Theorem |- (!a a'. (L_threadTau a = L_threadTau a') = (a = a')) /\ (!a a'. (L_conn a = L_conn a') = (a = a')) /\ !a a'. (L_console a = L_console a') = (a = a') [label2_Axiom] Theorem |- !f0 f1 f2 f3. ?fn. (!a. fn (L_threadTau a) = f0 a) /\ (fn L_hostTau = f1) /\ (!a. fn (L_conn a) = f2 a) /\ !a. fn (L_console a) = f3 a [label2_case_cong] Theorem |- !M M' f v f1 f2. (M = M') /\ (!a. (M' = L_threadTau a) ==> (f a = f' a)) /\ ((M' = L_hostTau) ==> (v = v')) /\ (!a. (M' = L_conn a) ==> (f1 a = f1' a)) /\ (!a. (M' = L_console a) ==> (f2 a = f2' a)) ==> (case f v f1 f2 M = case f' v' f1' f2' M') [label2_distinct] Theorem |- (!a. ~(L_threadTau a = L_hostTau)) /\ (!a' a. ~(L_threadTau a = L_conn a')) /\ (!a' a. ~(L_threadTau a = L_console a')) /\ (!a. ~(L_hostTau = L_conn a)) /\ (!a. ~(L_hostTau = L_console a)) /\ !a' a. ~(L_conn a = L_console a') [label2_induction] Theorem |- !P. (!t. P (L_threadTau t)) /\ P L_hostTau /\ (!b. P (L_conn b)) /\ (!s. P (L_console s)) ==> !l. P l [label2_nchotomy] Theorem |- !l. (?t. l = L_threadTau t) \/ (l = L_hostTau) \/ (?b. l = L_conn b) \/ ?s. l = L_console s [label_11] Theorem |- (!a a'. (Lb a = Lb a') = (a = a')) /\ (!a a'. (Lm a = Lm a') = (a = a')) /\ !a a'. (Ln a = Ln a') = (a = a') [label_Axiom] Theorem |- !f0 f1 f2. ?fn. (!a. fn (Lb a) = f0 a) /\ (!a. fn (Lm a) = f1 a) /\ !a. fn (Ln a) = f2 a [label_case_cong] Theorem |- !M M' f f1 f2. (M = M') /\ (!a. (M' = Lb a) ==> (f a = f' a)) /\ (!a. (M' = Lm a) ==> (f1 a = f1' a)) /\ (!a. (M' = Ln a) ==> (f2 a = f2' a)) ==> (case f f1 f2 M = case f' f1' f2' M') [label_distinct] Theorem |- (!a' a. ~(Lb a = Lm a')) /\ (!a' a. ~(Lb a = Ln a')) /\ !a' a. ~(Lm a = Ln a') [label_induction] Theorem |- !P. (!p. P (Lb p)) /\ (!l. P (Lm l)) /\ (!p. P (Ln p)) ==> !l. P l [label_nchotomy] Theorem |- !l. (?p. l = Lb p) \/ (?l'. l = Lm l') \/ ?p. l = Ln p [msg_dest_ips_def] Theorem |- (msg_dest_ips Empty i = F) /\ (msg_dest_ips (N1 Par N2) i = msg_dest_ips N1 i \/ msg_dest_ips N2 i) /\ (msg_dest_ips (Msg (Timed (msg',d))) i = (i = msg'.dest)) /\ (msg_dest_ips (HC (v0,v1)) i = F) [msg_dest_ips_ind] Theorem |- !P. (!i. P Empty i) /\ (!N1 N2 i. P N1 i /\ P N2 i ==> P (N1 Par N2) i) /\ (!msg' d i. P (Msg (Timed (msg',d))) i) /\ (!v0 v1 i. P (HC (v0,v1)) i) ==> !v v1. P v v1 [msg_src_ips_def] Theorem |- (msg_src_ips Empty i = F) /\ (msg_src_ips (N1 Par N2) i = msg_src_ips N1 i \/ msg_src_ips N2 i) /\ (msg_src_ips (Msg (Timed (msg',d))) i = (i = msg'.src)) /\ (msg_src_ips (HC (v0,v1)) i = F) [msg_src_ips_ind] Theorem |- !P. (!i. P Empty i) /\ (!N1 N2 i. P N1 i /\ P N2 i ==> P (N1 Par N2) i) /\ (!msg' d i. P (Msg (Timed (msg',d))) i) /\ (!v0 v1 i. P (HC (v0,v1)) i) ==> !v v1. P v v1 [network_11] Theorem |- (!a0 a1 a0' a1'. (a0 Par a1 = a0' Par a1') = (a0 = a0') /\ (a1 = a1')) /\ (!a a'. (Msg a = Msg a') = (a = a')) /\ !a a'. (HC a = HC a') = (a = a') [network_Axiom] Theorem |- !f0 f1 f2 f3. ?fn. (fn Empty = f0) /\ (!a0 a1. fn (a0 Par a1) = f1 a0 a1 (fn a0) (fn a1)) /\ (!a. fn (Msg a) = f2 a) /\ !a. fn (HC a) = f3 a [network_case_cong] Theorem |- !M M' v f f1 f2. (M = M') /\ ((M' = Empty) ==> (v = v')) /\ (!a0 a1. (M' = a0 Par a1) ==> (f a0 a1 = f' a0 a1)) /\ (!a. (M' = Msg a) ==> (f1 a = f1' a)) /\ (!a. (M' = HC a) ==> (f2 a = f2' a)) ==> (case v f f1 f2 M = case v' f' f1' f2' M') [network_distinct] Theorem |- (!a1 a0. ~(Empty = a0 Par a1)) /\ (!a. ~(Empty = Msg a)) /\ (!a. ~(Empty = HC a)) /\ (!a1 a0 a. ~(a0 Par a1 = Msg a)) /\ (!a1 a0 a. ~(a0 Par a1 = HC a)) /\ !a' a. ~(Msg a = HC a') [network_induction] Theorem |- !P. P Empty /\ (!n n0. P n /\ P n0 ==> P (n Par n0)) /\ (!t. P (Msg t)) /\ (!p. P (HC p)) ==> !n. P n [network_lifted_lts_cases] Theorem |- (!a0 a1 a2. a0 --- a1 -->> a2 = (?l. (a1 = SOME l) /\ a0 --- l ---> a2) \/ (a1 = NONE) /\ T) /\ !a3 a4 a5. a3 --- a4 ---> a5 = (?d n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Msg (Timed (m,d))) /\ dpropmin <= d /\ d <= dpropmax) \/ (?df n m k. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = MsgProd m k df) /\ k >= 2 /\ !i. 0 <= i /\ i < k ==> dpropmin <= df i /\ df i <= dpropmax) \/ (?n m. (a3 = Empty) /\ (a4 = Lb (n,In,L_sendmsg m)) /\ (a5 = Empty) /\ T) \/ (?n m. (a3 = Msg (Timed (m,time_zero))) /\ (a4 = Lb (n,Out,L_recvmsg m)) /\ (a5 = Empty) /\ T) \/ (?d tim m. (a3 = Msg (Timed (m,tim + d))) /\ (a4 = Lm (L_time d)) /\ (a5 = Msg (Timed (m,tim))) /\ d > 0) \/ (?d. (a3 = Empty) /\ (a4 = Lm (L_time d)) /\ (a5 = Empty) /\ 0 < d) \/ (?h n conn h' fv tid. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,In,L_callHost (tid,fv))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_call (tid,fv) ---> h') \/ (?h h' tid v n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lb (n,Out,L_retFromHost (tid,v))) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_return (tid,v) ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,Out,L_sendmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (F,h'))) /\ h -- Lh_sendmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (T,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h'))) /\ h -- Lh_recvmsg m ---> h') \/ (?h m h' n. (a3 = HC (n,Host (F,h))) /\ (a4 = Lb (n,In,L_recvmsg m)) /\ (a5 = HC (n,Host (T,h))) /\ h -- Lh_recvmsg m ---> h') \/ (?h s h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_console s)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_console s ---> h') \/ (?n h h' conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_hostTau)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_tau ---> h') \/ (?h d h' n conn. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_epsilon d ---> h') \/ (?n conn h. (a3 = HC (n,Host (conn,h))) /\ (a4 = Ln (n,L_conn ~conn)) /\ (a5 = HC (n,Host (~conn,h))) /\ T) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STnew (tlty,v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) NOTIN FDOM st) \/ (?v tlty x st n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STset (tlty,Loc (tlty,x),v)))) /\ (a5 = HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,TLty_one,TL_one ()),dstore)))) /\ tlang_typing v tlty /\ Loc (tlty,x) IN FDOM st) \/ (?st tlty x v n tid. (a3 = HC (n,Store st)) /\ (a4 = Lb (n,In,L_callStore (tid,STget (tlty,Loc (tlty,x))))) /\ (a5 = HC (n,Store st) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ (FAPPLY st (Loc (tlty,x)) = v)) \/ (?n tid tlty v d. (a3 = HC (n,StoreRet (Timed ((tid,tlty,v),d)))) /\ (a4 = Lb (n,Out,L_retFromStore (tid,v))) /\ (a5 = Empty)) \/ (?d n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Store st)) /\ 0 < d) \/ (?d tim n y. (a3 = HC (n,StoreRet (Timed (y,tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,StoreRet (Timed (y,tim)))) /\ 0 < d) \/ (?t t' fmv n tid. (a3 = HC (n,Module t)) /\ (a4 = Lb (n,In,L_callModule (tid,fmv))) /\ (a5 = HC (n,Thread (Timed ((tid,Extern,t'),dthread))) Par HC (n,Module t)) /\ t --- Lt_callModuleIn fmv ->>> t') \/ (?d n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Module t)) /\ 0 < d) \/ (?t t' n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_tau ->>> t') \/ (?t t' v n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetHostIn v ->>> t') \/ (?t t' v n tid org. (a3 = HC (n,Thread (Timed ((tid,org,t),dthread)))) /\ (a4 = Lb (n,In,L_retFromStore (tid,v))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ t --- Lt_RetStoreIn v ->>> t') \/ (?t t' fhv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,fhv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callHostOut fhv ->>> t') \/ (?t t' fsv n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callStore (tid,fsv))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ t --- Lt_callStoreOut fsv ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Extern,t),d)))) /\ (a4 = Lb (n,Out,L_retFromThread (tid,v))) /\ (a5 = Empty) /\ t --- Lt_RETOut v ->>> t') \/ (?t t' v n tid d. (a3 = HC (n,Thread (Timed ((tid,Intern,t),d)))) /\ (a4 = Ln (n,L_threadTau tid)) /\ (a5 = HC (n,Thread (Timed ((tid,Intern,t'),time_infty)))) /\ t --- Lt_RETOut v ->>> t') \/ (?d n tid t tim org. (a3 = HC (n,Thread (Timed ((tid,org,t),tim + d)))) /\ (a4 = Lm (L_time d)) /\ (a5 = HC (n,Thread (Timed ((tid,org,t),tim)))) /\ 0 < d) \/ (?t t' s2 n tid d org. (a3 = HC (n,Thread (Timed ((tid,org,t),d)))) /\ (a4 = Lb (n,Out,L_callHost (tid,create ()))) /\ (a5 = HC (n, ThreadCreate (Timed ((tid,org,t',t with initial := s2),time_infty)))) /\ t --- Lt_callHostCreateOut s2 ->>> t') \/ (?t' t'' tid tid' n t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (OK tid')))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread))) Par HC (n,Thread (Timed ((tid,Intern,t2),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (OK tid')) ->>> t'') \/ (?t' t'' e n tid t2 d org. (a3 = HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) /\ (a4 = Lb (n,In,L_retFromHost (tid,TL_err (FAIL e)))) /\ (a5 = HC (n,Thread (Timed ((tid,org,t''),dthread)))) /\ t' --- Lt_RetHostIn (TL_err (FAIL e)) ->>> t'') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_crash n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n hcb. (a3 = HC (n,hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_crash n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?n conn h h'. (a3 = HC (n,Host (conn,h))) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Host (conn,h'))) /\ h -- Lh_exit ---> h') \/ (?n x. (a3 = Msg x) /\ (a4 = Lm (L_exit n)) /\ (a5 = Msg x) /\ T) \/ (?n. (a3 = Empty) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n st. (a3 = HC (n,Store st)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Store FEMPTY)) /\ T) \/ (?n x. (a3 = HC (n,StoreRet x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n t. (a3 = HC (n,Module t)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n,Module t)) /\ T) \/ (?n x. (a3 = HC (n,Thread x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n x. (a3 = HC (n,ThreadCreate x)) /\ (a4 = Lm (L_exit n)) /\ (a5 = Empty) /\ T) \/ (?n n' hcb. (a3 = HC (n',hcb)) /\ (a4 = Lm (L_exit n)) /\ (a5 = HC (n',hcb)) /\ (n <> n')) \/ (?N0 ll0 ll1 N0' N1 N1'. (a3 = N0 Par N1) /\ (a5 = N0' Par N1') /\ N0 --- ll0 -->> N0' /\ N1 --- ll1 -->> N1' /\ (sync ll0 ll1 = SOME a4)) \/ ?N0 N0'. N0 --- a4 ---> N0' /\ sc a3 N0 /\ sc N0' a5 [network_lifted_lts_ind] Theorem |- !network_lifted_lts' network_lts'. (!d n m. dpropmin <= d /\ d <= dpropmax ==> network_lts' Empty (Lb (n,In,L_sendmsg m)) (Msg (Timed (m,d)))) /\ (!df n m k. k >= 2 /\ (!i. 0 <= i /\ i < k ==> dpropmin <= df i /\ df i <= dpropmax) ==> network_lts' Empty (Lb (n,In,L_sendmsg m)) (MsgProd m k df)) /\ (!n m. T ==> network_lts' Empty (Lb (n,In,L_sendmsg m)) Empty) /\ (!n m. T ==> network_lts' (Msg (Timed (m,time_zero))) (Lb (n,Out,L_recvmsg m)) Empty) /\ (!d tim m. d > 0 ==> network_lts' (Msg (Timed (m,tim + d))) (Lm (L_time d)) (Msg (Timed (m,tim)))) /\ (!d. 0 < d ==> network_lts' Empty (Lm (L_time d)) Empty) /\ (!h n conn h' fv tid. h -- Lh_call (tid,fv) ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Lb (n,In,L_callHost (tid,fv))) (HC (n,Host (conn,h')))) /\ (!h h' tid v n conn. h -- Lh_return (tid,v) ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Lb (n,Out,L_retFromHost (tid,v))) (HC (n,Host (conn,h')))) /\ (!h m h' n. h -- Lh_sendmsg m ---> h' ==> network_lts' (HC (n,Host (T,h))) (Lb (n,Out,L_sendmsg m)) (HC (n,Host (T,h')))) /\ (!h m h' n. h -- Lh_sendmsg m ---> h' ==> network_lts' (HC (n,Host (F,h))) (Ln (n,L_hostTau)) (HC (n,Host (F,h')))) /\ (!h m h' n. h -- Lh_recvmsg m ---> h' ==> network_lts' (HC (n,Host (T,h))) (Lb (n,In,L_recvmsg m)) (HC (n,Host (T,h')))) /\ (!h m h' n. h -- Lh_recvmsg m ---> h' ==> network_lts' (HC (n,Host (F,h))) (Lb (n,In,L_recvmsg m)) (HC (n,Host (T,h)))) /\ (!h s h' n conn. h -- Lh_console s ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Ln (n,L_console s)) (HC (n,Host (conn,h')))) /\ (!n h h' conn. h -- Lh_tau ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Ln (n,L_hostTau)) (HC (n,Host (conn,h')))) /\ (!h d h' n conn. h -- Lh_epsilon d ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Lm (L_time d)) (HC (n,Host (conn,h')))) /\ (!n conn h. T ==> network_lts' (HC (n,Host (conn,h))) (Ln (n,L_conn ~conn)) (HC (n,Host (~conn,h)))) /\ (!v tlty x st n tid. tlang_typing v tlty /\ Loc (tlty,x) NOTIN FDOM st ==> network_lts' (HC (n,Store st)) (Lb (n,In,L_callStore (tid,STnew (tlty,v)))) (HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore))))) /\ (!v tlty x st n tid. tlang_typing v tlty /\ Loc (tlty,x) IN FDOM st ==> network_lts' (HC (n,Store st)) (Lb (n,In,L_callStore (tid,STset (tlty,Loc (tlty,x),v)))) (HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,TLty_one,TL_one ()),dstore))))) /\ (!st tlty x v n tid. (FAPPLY st (Loc (tlty,x)) = v) ==> network_lts' (HC (n,Store st)) (Lb (n,In,L_callStore (tid,STget (tlty,Loc (tlty,x))))) (HC (n,Store st) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore))))) /\ (!n tid tlty v d. network_lts' (HC (n,StoreRet (Timed ((tid,tlty,v),d)))) (Lb (n,Out,L_retFromStore (tid,v))) Empty) /\ (!d n st. 0 < d ==> network_lts' (HC (n,Store st)) (Lm (L_time d)) (HC (n,Store st))) /\ (!d tim n y. 0 < d ==> network_lts' (HC (n,StoreRet (Timed (y,tim + d)))) (Lm (L_time d)) (HC (n,StoreRet (Timed (y,tim))))) /\ (!t t' fmv n tid. t --- Lt_callModuleIn fmv ->>> t' ==> network_lts' (HC (n,Module t)) (Lb (n,In,L_callModule (tid,fmv))) (HC (n,Thread (Timed ((tid,Extern,t'),dthread))) Par HC (n,Module t))) /\ (!d n t. 0 < d ==> network_lts' (HC (n,Module t)) (Lm (L_time d)) (HC (n,Module t))) /\ (!t t' n tid d org. t --- Lt_tau ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),d)))) (Ln (n,L_threadTau tid)) (HC (n,Thread (Timed ((tid,org,t'),dthread))))) /\ (!t t' v n tid d org. t --- Lt_RetHostIn v ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),d)))) (Lb (n,In,L_retFromHost (tid,v))) (HC (n,Thread (Timed ((tid,org,t'),dthread))))) /\ (!t t' v n tid org. t --- Lt_RetStoreIn v ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),dthread)))) (Lb (n,In,L_retFromStore (tid,v))) (HC (n,Thread (Timed ((tid,org,t'),dthread))))) /\ (!t t' fhv n tid d org. t --- Lt_callHostOut fhv ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),d)))) (Lb (n,Out,L_callHost (tid,fhv))) (HC (n,Thread (Timed ((tid,org,t'),time_infty))))) /\ (!t t' fsv n tid d org. t --- Lt_callStoreOut fsv ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),d)))) (Lb (n,Out,L_callStore (tid,fsv))) (HC (n,Thread (Timed ((tid,org,t'),time_infty))))) /\ (!t t' v n tid d. t --- Lt_RETOut v ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,Extern,t),d)))) (Lb (n,Out,L_retFromThread (tid,v))) Empty) /\ (!t t' v n tid d. t --- Lt_RETOut v ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,Intern,t),d)))) (Ln (n,L_threadTau tid)) (HC (n,Thread (Timed ((tid,Intern,t'),time_infty))))) /\ (!d n tid t tim org. 0 < d ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),tim + d)))) (Lm (L_time d)) (HC (n,Thread (Timed ((tid,org,t),tim))))) /\ (!t t' s2 n tid d org. t --- Lt_callHostCreateOut s2 ->>> t' ==> network_lts' (HC (n,Thread (Timed ((tid,org,t),d)))) (Lb (n,Out,L_callHost (tid,create ()))) (HC (n, ThreadCreate (Timed ((tid,org,t',t with initial := s2),time_infty))))) /\ (!t' t'' tid tid' n t2 d org. t' --- Lt_RetHostIn (TL_err (OK tid')) ->>> t'' ==> network_lts' (HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) (Lb (n,In,L_retFromHost (tid,TL_err (OK tid')))) (HC (n,Thread (Timed ((tid,org,t''),dthread))) Par HC (n,Thread (Timed ((tid,Intern,t2),dthread))))) /\ (!t' t'' e n tid t2 d org. t' --- Lt_RetHostIn (TL_err (FAIL e)) ->>> t'' ==> network_lts' (HC (n,ThreadCreate (Timed ((tid,org,t',t2),d)))) (Lb (n,In,L_retFromHost (tid,TL_err (FAIL e)))) (HC (n,Thread (Timed ((tid,org,t''),dthread))))) /\ (!n x. T ==> network_lts' (Msg x) (Lm (L_crash n)) (Msg x)) /\ (!n. T ==> network_lts' Empty (Lm (L_crash n)) Empty) /\ (!n hcb. T ==> network_lts' (HC (n,hcb)) (Lm (L_crash n)) Empty) /\ (!n n' hcb. (n <> n') ==> network_lts' (HC (n',hcb)) (Lm (L_crash n)) (HC (n',hcb))) /\ (!n conn h h'. h -- Lh_exit ---> h' ==> network_lts' (HC (n,Host (conn,h))) (Lm (L_exit n)) (HC (n,Host (conn,h')))) /\ (!n x. T ==> network_lts' (Msg x) (Lm (L_exit n)) (Msg x)) /\ (!n. T ==> network_lts' Empty (Lm (L_exit n)) Empty) /\ (!n st. T ==> network_lts' (HC (n,Store st)) (Lm (L_exit n)) (HC (n,Store FEMPTY))) /\ (!n x. T ==> network_lts' (HC (n,StoreRet x)) (Lm (L_exit n)) Empty) /\ (!n t. T ==> network_lts' (HC (n,Module t)) (Lm (L_exit n)) (HC (n,Module t))) /\ (!n x. T ==> network_lts' (HC (n,Thread x)) (Lm (L_exit n)) Empty) /\ (!n x. T ==> network_lts' (HC (n,ThreadCreate x)) (Lm (L_exit n)) Empty) /\ (!n n' hcb. (n <> n') ==> network_lts' (HC (n',hcb)) (Lm (L_exit n)) (HC (n',hcb))) /\ (!N l N'. network_lts' N l N' ==> network_lifted_lts' N (SOME l) N') /\ (!N N'. T ==> network_lifted_lts' N NONE N') /\ (!N0 ll0 ll1 N0' N1 N1' l. network_lifted_lts' N0 ll0 N0' /\ network_lifted_lts' N1 ll1 N1' /\ (sync ll0 ll1 = SOME l) ==> network_lts' (N0 Par N1) l (N0' Par N1')) /\ (!N N' N0 N0' l. network_lts' N0 l N0' /\ sc N N0 /\ sc N0' N' ==> network_lts' N l N') ==> (!a0 a1 a2. a0 --- a1 -->> a2 ==> network_lifted_lts' a0 a1 a2) /\ !a3 a4 a5. a3 --- a4 ---> a5 ==> network_lts' a3 a4 a5 [network_lifted_lts_rules] Theorem |- (!d n m. dpropmin <= d /\ d <= dpropmax ==> Empty --- Lb (n,In,L_sendmsg m) ---> Msg (Timed (m,d))) /\ (!df n m k. k >= 2 /\ (!i. 0 <= i /\ i < k ==> dpropmin <= df i /\ df i <= dpropmax) ==> Empty --- Lb (n,In,L_sendmsg m) ---> MsgProd m k df) /\ (!n m. T ==> Empty --- Lb (n,In,L_sendmsg m) ---> Empty) /\ (!n m. T ==> Msg (Timed (m,time_zero)) --- Lb (n,Out,L_recvmsg m) ---> Empty) /\ (!d tim m. d > 0 ==> Msg (Timed (m,tim + d)) --- Lm (L_time d) ---> Msg (Timed (m,tim))) /\ (!d. 0 < d ==> Empty --- Lm (L_time d) ---> Empty) /\ (!h n conn h' fv tid. h -- Lh_call (tid,fv) ---> h' ==> HC (n,Host (conn,h)) --- Lb (n,In,L_callHost (tid,fv)) ---> HC (n,Host (conn,h'))) /\ (!h h' tid v n conn. h -- Lh_return (tid,v) ---> h' ==> HC (n,Host (conn,h)) --- Lb (n,Out,L_retFromHost (tid,v)) ---> HC (n,Host (conn,h'))) /\ (!h m h' n. h -- Lh_sendmsg m ---> h' ==> HC (n,Host (T,h)) --- Lb (n,Out,L_sendmsg m) ---> HC (n,Host (T,h'))) /\ (!h m h' n. h -- Lh_sendmsg m ---> h' ==> HC (n,Host (F,h)) --- Ln (n,L_hostTau) ---> HC (n,Host (F,h'))) /\ (!h m h' n. h -- Lh_recvmsg m ---> h' ==> HC (n,Host (T,h)) --- Lb (n,In,L_recvmsg m) ---> HC (n,Host (T,h'))) /\ (!h m h' n. h -- Lh_recvmsg m ---> h' ==> HC (n,Host (F,h)) --- Lb (n,In,L_recvmsg m) ---> HC (n,Host (T,h))) /\ (!h s h' n conn. h -- Lh_console s ---> h' ==> HC (n,Host (conn,h)) --- Ln (n,L_console s) ---> HC (n,Host (conn,h'))) /\ (!n h h' conn. h -- Lh_tau ---> h' ==> HC (n,Host (conn,h)) --- Ln (n,L_hostTau) ---> HC (n,Host (conn,h'))) /\ (!h d h' n conn. h -- Lh_epsilon d ---> h' ==> HC (n,Host (conn,h)) --- Lm (L_time d) ---> HC (n,Host (conn,h'))) /\ (!n conn h. T ==> HC (n,Host (conn,h)) --- Ln (n,L_conn ~conn) ---> HC (n,Host (~conn,h))) /\ (!v tlty x st n tid. tlang_typing v tlty /\ Loc (tlty,x) NOTIN FDOM st ==> HC (n,Store st) --- Lb (n,In,L_callStore (tid,STnew (tlty,v))) ---> HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ (!v tlty x st n tid. tlang_typing v tlty /\ Loc (tlty,x) IN FDOM st ==> HC (n, Store st) --- Lb (n,In, L_callStore (tid,STset (tlty,Loc (tlty,x),v))) ---> HC (n,Store (FUPDATE st (Loc (tlty,x),v))) Par HC (n,StoreRet (Timed ((tid,TLty_one,TL_one ()),dstore)))) /\ (!st tlty x v n tid. (FAPPLY st (Loc (tlty,x)) = v) ==> HC (n, Store st) --- Lb (n,In, L_callStore (tid,STget (tlty,Loc (tlty,x)))) ---> HC (n,Store st) Par HC (n,StoreRet (Timed ((tid,tlty,v),dstore)))) /\ (!n tid tlty v d. HC (n, StoreRet (Timed ((tid,tlty,v), d))) --- Lb (n,Out,L_retFromStore (tid,v)) ---> Empty) /\ (!d n st. 0 < d ==> HC (n,Store st) --- Lm (L_time d) ---> HC (n,Store st)) /\ (!d tim n y. 0 < d ==> HC (n,StoreRet (Timed (y,tim + d))) --- Lm (L_time d) ---> HC (n,StoreRet (Timed (y,tim)))) /\ (!t t' fmv n tid. t --- Lt_callModuleIn fmv ->>> t' ==> HC (n,Module t) --- Lb (n,In,L_callModule (tid,fmv)) ---> HC (n,Thread (Timed ((tid,Extern,t'),dthread))) Par HC (n,Module t)) /\ (!d n t. 0 < d ==> HC (n,Module t) --- Lm (L_time d) ---> HC (n,Module t)) /\ (!t t' n tid d org. t --- Lt_tau ->>> t' ==> HC (n, Thread (Timed ((tid,org,t),d))) --- Ln (n,L_threadTau tid) ---> HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ (!t t' v n tid d org. t --- Lt_RetHostIn v ->>> t' ==> HC (n, Thread (Timed ((tid,org,t),d))) --- Lb (n,In,L_retFromHost (tid,v)) ---> HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ (!t t' v n tid org. t --- Lt_RetStoreIn v ->>> t' ==> HC (n, Thread (Timed ((tid,org,t), dthread))) --- Lb (n,In,L_retFromStore (tid,v)) ---> HC (n,Thread (Timed ((tid,org,t'),dthread)))) /\ (!t t' fhv n tid d org. t --- Lt_callHostOut fhv ->>> t' ==> HC (n, Thread (Timed ((tid,org,t),d))) --- Lb (n,Out,L_callHost (tid,fhv)) ---> HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ (!t t' fsv n tid d org. t --- Lt_callStoreOut fsv ->>> t' ==> HC (n, Thread (Timed ((tid,org,t), d))) --- Lb (n,Out,L_callStore (tid,fsv)) ---> HC (n,Thread (Timed ((tid,org,t'),time_infty)))) /\ (!t t' v n tid d. t --- Lt_RETOut v ->>> t' ==> HC (n, Thread (Timed ((tid,Extern,t), d))) --- Lb (n,Out,L_retFromThread (tid,v)) ---> Empty) /\ (!t t' v n tid d. t --- Lt_RETOut v ->>> t' ==> HC (n, Thread (Timed ((tid,Intern,t),d))) --- Ln (n,L_threadTau tid) ---> HC (n,Thread (Timed ((tid,Intern,t'),time_infty)))) /\ (!d n tid t tim org. 0 < d ==> HC (n,Thread (Timed ((tid,org,t),tim + d))) --- Lm (L_time d) ---> HC (n,Thread (Timed ((tid,org,t),tim)))) /\ (!t t' s2 n tid d org. t --- Lt_callHostCreateOut s2 ->>> t' ==> HC (n, Thread (Timed ((tid,org,t), d))) --- Lb (n,Out,L_callHost (tid,create ())) ---> HC (n, ThreadCreate (Timed ((tid,org,t',t with initial := s2),time_infty)))) /\ (!t' t'' tid tid' n t2 d org. t' --- Lt_RetHostIn (TL_err (OK tid')) ->>> t'' ==> HC (n, ThreadCreate (Timed ((tid,org,t',t2), d))) --- Lb (n,In, L_retFromHost (tid,TL_err (OK tid'))) ---> HC (n,Thread (Timed ((tid,org,t''),dthread))) Par HC (n,Thread (Timed ((tid,Intern,t2),dthread)))) /\ (!t' t'' e n tid t2 d org. t' --- Lt_RetHostIn (TL_err (FAIL e)) ->>> t'' ==> HC (n, ThreadCreate (Timed ((tid,org,t',t2), d))) --- Lb (n,In, L_retFromHost (tid,TL_err (FAIL e))) ---> HC (n,Thread (Timed ((tid,org,t''),dthread)))) /\ (!n x. T ==> Msg x --- Lm (L_crash n) ---> Msg x) /\ (!n. T ==> Empty --- Lm (L_crash n) ---> Empty) /\ (!n hcb. T ==> HC (n,hcb) --- Lm (L_crash n) ---> Empty) /\ (!n n' hcb. (n <> n') ==> HC (n',hcb) --- Lm (L_crash n) ---> HC (n',hcb)) /\ (!n conn h h'. h -- Lh_exit ---> h' ==> HC (n,Host (conn,h)) --- Lm (L_exit n) ---> HC (n,Host (conn,h'))) /\ (!n x. T ==> Msg x --- Lm (L_exit n) ---> Msg x) /\ (!n. T ==> Empty --- Lm (L_exit n) ---> Empty) /\ (!n st. T ==> HC (n,Store st) --- Lm (L_exit n) ---> HC (n,Store FEMPTY)) /\ (!n x. T ==> HC (n,StoreRet x) --- Lm (L_exit n) ---> Empty) /\ (!n t. T ==> HC (n,Module t) --- Lm (L_exit n) ---> HC (n,Module t)) /\ (!n x. T ==> HC (n,Thread x) --- Lm (L_exit n) ---> Empty) /\ (!n x. T ==> HC (n,ThreadCreate x) --- Lm (L_exit n) ---> Empty) /\ (!n n' hcb. (n <> n') ==> HC (n',hcb) --- Lm (L_exit n) ---> HC (n',hcb)) /\ (!N l N'. N --- l ---> N' ==> N --- SOME l -->> N') /\ (!N N'. T ==> N --- NONE -->> N') /\ (!N0 ll0 ll1 N0' N1 N1' l. N0 --- ll0 -->> N0' /\ N1 --- ll1 -->> N1' /\ (sync ll0 ll1 = SOME l) ==> N0 Par N1 --- l ---> N0' Par N1') /\ !N N' N0 N0' l. N0 --- l ---> N0' /\ sc N N0 /\ sc N0' N' ==> N --- l ---> N' [network_nchotomy] Theorem |- !n. (n = Empty) \/ (?n' n0. n = n' Par n0) \/ (?t. n = Msg t) \/ ?p. n = HC p [network_ok_def] Theorem |- (network_ok Empty = T) /\ (network_ok (Msg (Timed (m,d))) = msg_ok m /\ time_zero <= d /\ d < time_infty) /\ (network_ok (HC (n,hc)) = host_component_ok hc) /\ (network_ok (N Par N') = network_ok N /\ network_ok N' /\ ~(?i. host_ips N i /\ host_ips N' i) /\ (!n x x'. ~(net_in (n,Host x) N /\ net_in (n,Host x') N')) /\ (!n y y'. ~(net_in (n,Module y) N /\ net_in (n,Module y') N')) /\ (!n z z'. ~(net_in (n,Store z) N /\ net_in (n,Store z') N')) /\ (!n tid. ~(thread_snippet_in_net (n,tid) N /\ thread_snippet_in_net (n,tid) N')) /\ (!n tid t d b h org. net_in (n,Thread (Timed ((tid,org,t),d))) (N Par N') /\ net_in (n,Host (b,h)) (N Par N') ==> tid IN FDOM h.ts) /\ !n tid t t' d b h org. net_in (n,ThreadCreate (Timed ((tid,org,t,t'),d))) (N Par N') /\ net_in (n,Host (b,h)) (N Par N') ==> tid IN FDOM h.ts) [network_ok_ind] Theorem |- !P. P Empty /\ (!m d. P (Msg (Timed (m,d)))) /\ (!n hc. P (HC (n,hc))) /\ (!N N'. P N /\ P N' ==> P (N Par N')) ==> !v. P v [num2dirn_11] Theorem |- !r r'. r < 3 ==> r' < 3 ==> ((num2dirn r = num2dirn r') = (r = r')) [num2dirn_ONTO] Theorem |- !a. ?r. (a = num2dirn r) /\ r < 3 [num2dirn_dirn2num] Theorem |- !a. num2dirn (dirn2num a) = a [num2origin_11] Theorem |- !r r'. r < 2 ==> r' < 2 ==> ((num2origin r = num2origin r') = (r = r')) [num2origin_ONTO] Theorem |- !a. ?r. (a = num2origin r) /\ r < 2 [num2origin_origin2num] Theorem |- !a. num2origin (origin2num a) = a [origin2num_11] Theorem |- !a a'. (origin2num a = origin2num a') = (a = a') [origin2num_Extern] Theorem |- origin2num Extern = 1 [origin2num_Intern] Theorem |- origin2num Intern = 0 [origin2num_ONTO] Theorem |- !r. r < 2 = ?a. r = origin2num a [origin2num_num2origin] Theorem |- !r. r < 2 = (origin2num (num2origin r) = r) [origin_Axiom] Theorem |- !x0 x1. ?f. (f Intern = x0) /\ (f Extern = x1) [origin_EQ_origin] Theorem |- !a a'. (a = a') = (origin2num a = origin2num a') [origin_case_cong] Theorem |- !M M' x0 x1. (M = M') /\ ((M' = Intern) ==> (x0 = x0')) /\ ((M' = Extern) ==> (x1 = x1')) ==> ((case M of Intern -> x0 || Extern -> x1) = case M' of Intern -> x0' || Extern -> x1') [origin_distinct] Theorem |- ~(Intern = Extern) [origin_induction] Theorem |- !P. P Extern /\ P Intern ==> !a. P a [origin_nchotomy] Theorem |- !a. (a = Intern) \/ (a = Extern) [sc_cases] Theorem |- !a0 a1. sc a0 a1 = (a1 = a0 Par Empty) \/ (?N N'. (a0 = N Par N') /\ (a1 = N' Par N)) \/ (?N N' N''. (a0 = N Par (N' Par N'')) /\ (a1 = N Par N' Par N'')) \/ (?N1 N1' N2 N2'. (a0 = N1 Par N2) /\ (a1 = N2' Par N2') /\ sc N1 N1' /\ sc N2 N2') \/ (a1 = a0) \/ sc a1 a0 \/ ?N'. sc a0 N' /\ sc N' a1 [sc_ind] Theorem |- !sc'. (!N. sc' N (N Par Empty)) /\ (!N N'. sc' (N Par N') (N' Par N)) /\ (!N N' N''. sc' (N Par (N' Par N'')) (N Par N' Par N'')) /\ (!N1 N1' N2 N2'. sc' N1 N1' /\ sc' N2 N2' ==> sc' (N1 Par N2) (N2' Par N2')) /\ (!N. sc' N N) /\ (!N N'. sc' N N' ==> sc' N' N) /\ (!N N' N''. sc' N N' /\ sc' N' N'' ==> sc' N N'') ==> !a0 a1. sc a0 a1 ==> sc' a0 a1 [sc_rules] Theorem |- (!N. sc N (N Par Empty)) /\ (!N N'. sc (N Par N') (N' Par N)) /\ (!N N' N''. sc (N Par (N' Par N'')) (N Par N' Par N'')) /\ (!N1 N1' N2 N2'. sc N1 N1' /\ sc N2 N2' ==> sc (N1 Par N2) (N2' Par N2')) /\ (!N. sc N N) /\ (!N N'. sc N N' ==> sc N' N) /\ !N N' N''. sc N N' /\ sc N' N'' ==> sc N N'' [sync_def] Theorem |- (sync NONE (SOME (Lb x1)) = SOME (Lb x1)) /\ (sync (SOME (Lb (v10',v18,v19))) NONE = SOME (Lb (v10',v18,v19))) /\ (sync NONE (SOME (Ln x3)) = SOME (Ln x3)) /\ (sync (SOME (Ln x4)) NONE = SOME (Ln x4)) /\ (sync NONE (SOME (Lm x5)) = NONE) /\ (sync (SOME (Lm x5)) NONE = NONE) /\ (sync (SOME (Lb (h1,d1,x6))) (SOME (Lb (h2,d2,x7))) = (if (h1 = h2) /\ (x6 = x7) /\ ((d1 = In) /\ (d2 = Out) \/ (d2 = In) /\ (d1 = Out)) then SOME (Lb (h1,Tau,x6)) else NONE)) /\ (sync (SOME (Lm x10)) (SOME (Lm x11)) = (if x10 = x11 then SOME (Lm x10) else NONE)) /\ (sync (SOME (Ln x8)) (SOME (Ln x9)) = NONE) /\ (sync NONE NONE = NONE) /\ (sync (SOME (Lb (v12,v20,v21))) (SOME (Lm v1)) = NONE) /\ (sync (SOME (Lm v2)) (SOME (Lb v3)) = NONE) /\ (sync (SOME (Lb (v14,v22,v23))) (SOME (Ln v5)) = NONE) /\ (sync (SOME (Ln v6)) (SOME (Lb v7)) = NONE) /\ (sync (SOME (Lm v8)) (SOME (Ln v9)) = NONE) /\ (sync (SOME (Ln v10)) (SOME (Lm v11)) = NONE) [sync_ind] Theorem |- !P. (!x1. P NONE (SOME (Lb x1))) /\ (!v10 v18 v19. P (SOME (Lb (v10,v18,v19))) NONE) /\ (!x3. P NONE (SOME (Ln x3))) /\ (!x4. P (SOME (Ln x4)) NONE) /\ (!x5. P NONE (SOME (Lm x5))) /\ (!x5. P (SOME (Lm x5)) NONE) /\ (!h1 d1 x6 h2 d2 x7. P (SOME (Lb (h1,d1,x6))) (SOME (Lb (h2,d2,x7)))) /\ (!x10 x11. P (SOME (Lm x10)) (SOME (Lm x11))) /\ (!x8 x9. P (SOME (Ln x8)) (SOME (Ln x9))) /\ P NONE NONE /\ (!v12 v20 v21 v1. P (SOME (Lb (v12,v20,v21))) (SOME (Lm v1))) /\ (!v2 v3. P (SOME (Lm v2)) (SOME (Lb v3))) /\ (!v14 v22 v23 v5. P (SOME (Lb (v14,v22,v23))) (SOME (Ln v5))) /\ (!v6 v7. P (SOME (Ln v6)) (SOME (Lb v7))) /\ (!v8 v9. P (SOME (Lm v8)) (SOME (Ln v9))) /\ (!v10 v11. P (SOME (Ln v10)) (SOME (Lm v11))) ==> !v v1. P v v1 [thread_snippet_in_hc_def] Theorem |- (thread_snippet_in_hc tid (Host v0) = F) /\ (thread_snippet_in_hc tid (Module v1) = F) /\ (thread_snippet_in_hc tid (Store v2) = F) /\ (thread_snippet_in_hc tid (StoreRet v3) = F) /\ (thread_snippet_in_hc tid (Thread (Timed ((tid',v4,v5),v6))) = (tid = tid')) /\ (thread_snippet_in_hc tid (ThreadCreate (Timed ((tid',v7,v8,v9),v10))) = (tid = tid')) [thread_snippet_in_hc_ind] Theorem |- !P. (!tid v0. P tid (Host v0)) /\ (!tid v1. P tid (Module v1)) /\ (!tid v2. P tid (Store v2)) /\ (!tid v3. P tid (StoreRet v3)) /\ (!tid tid' v4 v5 v6. P tid (Thread (Timed ((tid',v4,v5),v6)))) /\ (!tid tid' v7 v8 v9 v10. P tid (ThreadCreate (Timed ((tid',v7,v8,v9),v10)))) ==> !v v1. P v v1 [thread_snippet_in_net_def] Theorem |- (thread_snippet_in_net nt Empty = F) /\ (thread_snippet_in_net nt (N1 Par N2) = thread_snippet_in_net nt N1 \/ thread_snippet_in_net nt N2) /\ (thread_snippet_in_net nt (Msg mt) = F) /\ (thread_snippet_in_net nt (HC (n',hc')) = (FST nt = n') /\ thread_snippet_in_hc (SND nt) hc') [thread_snippet_in_net_ind] Theorem |- !P. (!nt. P nt Empty) /\ (!nt N1 N2. P nt N1 /\ P nt N2 ==> P nt (N1 Par N2)) /\ (!nt mt. P nt (Msg mt)) /\ (!nt n' hc'. P nt (HC (n',hc'))) ==> !v v1 v2. P (v,v1) v2 [threadids_def] Theorem |- (threadids Empty n = {}) /\ (threadids (N1 Par N2) n = threadids N1 n UNION threadids N2 n) /\ (threadids (Msg mt) n = {}) /\ (threadids (HC (n',hc)) n = (if n <> n' then {} else threadids_hc hc)) [threadids_hc_def] Theorem |- (threadids_hc (Host (b,h)) = {}) /\ (threadids_hc (Module s) = {}) /\ (threadids_hc (Store st) = {}) /\ (threadids_hc (StoreRet v0) = {}) /\ (threadids_hc (Thread (Timed ((tid,org,t),d))) = {tid}) /\ (threadids_hc (ThreadCreate (Timed ((tid,org,t,t'),d))) = {tid}) [threadids_hc_ind] Theorem |- !P. (!b h. P (Host (b,h))) /\ (!s. P (Module s)) /\ (!st. P (Store st)) /\ (!v0. P (StoreRet v0)) /\ (!tid org t d. P (Thread (Timed ((tid,org,t),d)))) /\ (!tid org t t' d. P (ThreadCreate (Timed ((tid,org,t,t'),d)))) ==> !v. P v [threadids_ind] Theorem |- !P. (!n. P Empty n) /\ (!N1 N2 n. P N1 n /\ P N2 n ==> P (N1 Par N2) n) /\ (!mt n. P (Msg mt) n) /\ (!n' hc n. P (HC (n',hc)) n) ==> !v v1. P v v1 [visible_def] Theorem |- (visible N (Ln v0) = T) /\ (visible N (Lm (L_crash n)) = T) /\ (visible N (Lm (L_time d)) = T) /\ (visible N (Lm (L_exit n)) = n IN hosts N) /\ (visible N (Lb (n,Tau,l)) = T) /\ (visible N (Lb (n,In,L_callHost (tid,fhv))) = tid NOTIN threadids N n) /\ (visible N (Lb (n,In,L_callStore (tid,fsv))) = tid NOTIN threadids N n) /\ (visible N (Lb (n,In,L_callModule (tid,fmv))) = tid NOTIN threadids N n) /\ (visible N (Lb (n,In,L_retFromHost (tid,v))) = F) /\ (visible N (Lb (n,In,L_retFromStore (tid,v))) = F) /\ (visible N (Lb (n,In,L_retFromThread (tid,v))) = F) /\ (visible N (Lb (n,In,L_sendmsg m)) = n NOTIN hosts N /\ m.src NOTIN host_ips N /\ m.dest IN host_ips N) /\ (visible N (Lb (n,In,L_recvmsg m)) = F) /\ (visible N (Lb (n,Out,L_callHost (tid,fhv))) = F) /\ (visible N (Lb (n,Out,L_callStore (tid,fsv))) = F) /\ (visible N (Lb (n,Out,L_callModule (tid,fmv))) = F) /\ (visible N (Lb (n,Out,L_retFromHost (tid,v))) = tid NOTIN threadids N n) /\ (visible N (Lb (n,Out,L_retFromStore (tid,v))) = tid NOTIN threadids N n) /\ (visible N (Lb (n,Out,L_retFromThread (tid,v))) = T) /\ (visible N (Lb (n,Out,L_sendmsg m)) = F) /\ (visible N (Lb (n,Out,L_recvmsg m)) = n NOTIN hosts N /\ m.src IN host_ips N /\ m.dest NOTIN host_ips N) [visible_ind] Theorem |- !P. (!N v0. P N (Ln v0)) /\ (!N n. P N (Lm (L_crash n))) /\ (!N d. P N (Lm (L_time d))) /\ (!N n. P N (Lm (L_exit n))) /\ (!N n l. P N (Lb (n,Tau,l))) /\ (!N n tid fhv. P N (Lb (n,In,L_callHost (tid,fhv)))) /\ (!N n tid fsv. P N (Lb (n,In,L_callStore (tid,fsv)))) /\ (!N n tid fmv. P N (Lb (n,In,L_callModule (tid,fmv)))) /\ (!N n tid v. P N (Lb (n,In,L_retFromHost (tid,v)))) /\ (!N n tid v. P N (Lb (n,In,L_retFromStore (tid,v)))) /\ (!N n tid v. P N (Lb (n,In,L_retFromThread (tid,v)))) /\ (!N n m. P N (Lb (n,In,L_sendmsg m))) /\ (!N n m. P N (Lb (n,In,L_recvmsg m))) /\ (!N n tid fhv. P N (Lb (n,Out,L_callHost (tid,fhv)))) /\ (!N n tid fsv. P N (Lb (n,Out,L_callStore (tid,fsv)))) /\ (!N n tid fmv. P N (Lb (n,Out,L_callModule (tid,fmv)))) /\ (!N n tid v. P N (Lb (n,Out,L_retFromHost (tid,v)))) /\ (!N n tid v. P N (Lb (n,Out,L_retFromStore (tid,v)))) /\ (!N n tid v. P N (Lb (n,Out,L_retFromThread (tid,v)))) /\ (!N n m. P N (Lb (n,Out,L_sendmsg m))) /\ (!N n m. P N (Lb (n,Out,L_recvmsg m))) ==> !v v1. P v v1 *) end