signature TNet_host_theorem2Theory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val htsType_def : thm
    val label_ok_primitive_def : thm
    val outputq_ok_primitive_def : thm
    val uniquely_valued_def : thm
    val uniqval_find_def : thm
  
  (*  Theorems  *)
    val Time_Pass_preserves_host_ok : thm
    val badfail_characterise : thm
    val comp_host_ok : thm
    val enqueue_ok : thm
    val enter2_characterise : thm
    val exit_characterise : thm
    val exit_rids : thm
    val fail_characterise : thm
    val failing_rids : thm
    val host_ok_invariant : thm
    val host_ok_thm : thm
    val label_ok_def : thm
    val label_ok_ind : thm
    val misc_characterise : thm
    val misc_rids : thm
    val outputq_ok_def : thm
    val outputq_ok_ind : thm
    val simple_sock_with_fd_fiddle : thm
    val slowfail_characterise : thm
    val slowsucceed_characterise : thm
    val sock_with_fd_fiddle : thm
    val succeed_characterise : thm
  
  val TNet_host_theorem2_grammars : parse_type.grammar * term_grammar.grammar
(*
   [TNet_host_theorem1] Parent theory of "TNet_host_theorem2"
   
   [htsType_def]
   Definition
   |- (htsType Run = {}) /\ (htsType Zombie = {}) /\
      (htsType Delay2 = {TLty_err TLty_one}) /\
      (!t. htsType (Ret t) = tlang_typing t) /\
      (!v0. htsType (Sendto2 v0) = {TLty_err TLty_one}) /\
      (!v1.
         htsType (Recvfrom2 v1) =
         {TLty_err
            (TLty_pair
               (TLty_ip,TLty_pair (TLty_lift TLty_port,TLty_string)))}) /\
      (!v2.
         htsType (Select2 v2) =
         {TLty_err (TLty_pair (TLty_list TLty_fd,TLty_list TLty_fd))}) /\
      (!v3. htsType (Print2 v3) = {TLty_err TLty_one}) /\
      (htsType Exit = {TLty_void})
   
   [label_ok_primitive_def]
   Definition
   |- label_ok =
      WFREC (@R. WF R)
        (\label_ok a.
           case a of
              Lh_call v6 -> T
           || Lh_return v7 -> T
           || Lh_sendmsg v8 -> T
           || Lh_recvmsg v9 ->
                (case v9.body of
                    UDP v3 ->
                      (case v3 of
                          (v8,v9) ->
                            case v9 of
                               (v12,v13) ->
                                 string_size v13 <= UDPpayloadMax)
                 || ICMP_HOST_UNREACH v4 -> T
                 || ICMP_PORT_UNREACH v5 -> T)
           || Lh_console v10 -> T
           || Lh_tau -> T
           || Lh_epsilon v11 -> T
           || Lh_exit -> T)
   
   [outputq_ok_primitive_def]
   Definition
   |- outputq_ok =
      WFREC (@R. WF R)
        (\outputq_ok a.
           case a of
              (v,v1) ->
                case v of
                   Timed v2 ->
                     case v2 of
                        (v3,v4) ->
                          ((v3 = []) ==> ~v1) /\ EVERY msg_oq_ok v3)
   
   [uniquely_valued_def]
   Definition
   |- (!f. uniquely_valued f [] = T) /\
      !f h t.
        uniquely_valued f (h::t) =
        EVERY (\x. ~(f x = f h)) t /\ uniquely_valued f t
   
   [uniqval_find_def]
   Definition
   |- !f e h t.
        uniqval_find f e (h::t) =
        (if f h = e then h else uniqval_find f e t)
   
   [Time_Pass_preserves_host_ok]
   Theorem
   |- !h0 dur h. host_ok h0 /\ (Time_Pass dur h0 = SOME h) ==> host_ok h
   
   [badfail_characterise]
   Theorem
   |- !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)))
   
   [comp_host_ok]
   Theorem
   |- !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
   
   [enqueue_ok]
   Theorem
   |- !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')
   
   [enter2_characterise]
   Theorem
   |- !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
   
   [exit_characterise]
   Theorem
   |- !rid h0 l h. host_ok h0 /\ rid /* exit */ h0 -- l --> h ==> host_ok h
   
   [exit_rids]
   Theorem
   |- !rid h0 l h. rid /* exit */ h0 -- l --> h ==> rid IN {exit_1; exit_2}
   
   [fail_characterise]
   Theorem
   |- !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')
   
   [failing_rids]
   Theorem
   |- !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}
   
   [host_ok_invariant]
   Theorem
   |- !h rid rcat l h'.
        host_ok h /\ label_ok l ==>
        rid /* rcat */ h -- l --> h' ==>
        host_ok h'
   
   [host_ok_thm]
   Theorem
   |- !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
   
   [label_ok_def]
   Theorem
   |- (label_ok (Lh_recvmsg m) =
       case m.body of
          UDP v3 ->
            (case v3 of
                (v8,v9) ->
                  case v9 of (v12,v13) -> string_size v13 <= UDPpayloadMax)
       || ICMP_HOST_UNREACH v4 -> T
       || ICMP_PORT_UNREACH v5 -> T) /\ (label_ok Lh_exit = T) /\
      (label_ok (Lh_epsilon v5) = T) /\ (label_ok Lh_tau = T) /\
      (label_ok (Lh_console v4) = T) /\ (label_ok (Lh_sendmsg v2) = T) /\
      (label_ok (Lh_return v1) = T) /\ (label_ok (Lh_call v) = T)
   
   [label_ok_ind]
   Theorem
   |- !P.
        (!m. P (Lh_recvmsg m)) /\ P Lh_exit /\ (!v5. P (Lh_epsilon v5)) /\
        P Lh_tau /\ (!v4. P (Lh_console v4)) /\ (!v2. P (Lh_sendmsg v2)) /\
        (!v1. P (Lh_return v1)) /\ (!v. P (Lh_call v)) ==>
        !v. P v
   
   [misc_characterise]
   Theorem
   |- !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))
   
   [misc_rids]
   Theorem
   |- !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}
   
   [outputq_ok_def]
   Theorem
   |- outputq_ok (Timed (oql,d),oqf) =
      ((oql = []) ==> ~oqf) /\ EVERY msg_oq_ok oql
   
   [outputq_ok_ind]
   Theorem
   |- !P. (!oql d oqf. P (Timed (oql,d),oqf)) ==> !v v1. P (v,v1)
   
   [simple_sock_with_fd_fiddle]
   Theorem
   |- !fd s SC.
        uniquely_valued socket_fd (SC s) /\ (s.fd = fd) /\
        socklist_context SC ==>
        (sock_with_fd fd (SC s) = s)
   
   [slowfail_characterise]
   Theorem
   |- !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))
   
   [slowsucceed_characterise]
   Theorem
   |- !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
   
   [sock_with_fd_fiddle]
   Theorem
   |- !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'))
   
   [succeed_characterise]
   Theorem
   |- !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
   
   
*)
end