signature TNet_hostLTSTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val Time_Pass_d_def : thm
    val Time_Pass_def : thm
    val Time_Pass_h0_def : thm
    val Time_Pass_ts_def : thm
    val Time_Pass_xd_arg_munge_def : thm
    val Time_Pass_xd_tupled_primitive_def : thm
    val Urgent_def : thm
    val host_redn : thm
    val host_redn'_def : thm
    val revimp_def : thm
  
  (*  Theorems  *)
    val Time_Pass_xd_def : thm
    val Time_Pass_xd_ind : thm
    val host_redn_cases : thm
    val host_redn_ind : thm
    val host_redn_rules : thm
  
  val TNet_hostLTS_grammars : parse_type.grammar * term_grammar.grammar
(*
   [TNet_host0] Parent theory of "TNet_hostLTS"
   
   [Time_Pass_d_def]
   Definition
   |- !dur d.
        Time_Pass_d dur d =
        (let d' = d - dur in (if d' >= time_zero then SOME d' else NONE))
   
   [Time_Pass_def]
   Definition
   |- !dur h.
        Time_Pass dur h =
        (let h0' = Time_Pass_h0 dur h and urg = Urgent h in
           case (h0',urg) of
              (v2,v3) ->
                case v2 of
                   NONE -> NONE
                || SOME v5 -> case v3 of T -> NONE || F -> SOME v5)
   
   [Time_Pass_h0_def]
   Definition
   |- !dur h.
        Time_Pass_h0 dur h =
        (let ts0' = Time_Pass_ts dur h.ts and oq0' = Time_Pass_xd dur h.oq
           in
           case (ts0',oq0') of
              (v2,v3) ->
                case v2 of
                   NONE -> NONE
                || SOME v5 ->
                     case v3 of
                        NONE -> NONE
                     || SOME v7 -> SOME (h with <|ts := v5; oq := v7|>))
   
   [Time_Pass_ts_def]
   Definition
   |- !dur ts.
        Time_Pass_ts dur ts =
        (let ts0' = Time_Pass_xd dur o_f ts in
           (if
              FEVERY ((\t. ?t'. SOME t' = Time_Pass_xd dur t) o SND) ts
            then
              SOME ((\t. @t'. SOME t' = Time_Pass_xd dur t) o_f ts)
            else
              NONE))
   
   [Time_Pass_xd_arg_munge_def]
   Definition
   |- !x x1. Time_Pass_xd x x1 = Time_Pass_xd_tupled (x,x1)
   
   [Time_Pass_xd_tupled_primitive_def]
   Definition
   |- Time_Pass_xd_tupled =
      WFREC (@R. WF R)
        (\Time_Pass_xd_tupled a.
           case a of
              (v,v1) ->
                case v1 of
                   Timed v2 ->
                     case v2 of
                        (v3,v4) ->
                          case Time_Pass_d v v4 of
                             NONE -> NONE
                          || SOME v -> SOME (Timed (v3,v)))
   
   [Urgent_def]
   Definition
   |- !h.
        Urgent h =
        (?FC ifds tid d s p1 m ps3 ps4 data ifid mq.
           F_context FC /\
           (h =
            FC
              (ifds,tid,Timed (Recvfrom2 s.fd,d),
               s with
               <|ps1 := SOME p1; es := NONE;
                 mq := (m with body := UDP (ps3,ps4,data),ifid)::mq|>))) \/
        (?FC tid d ifds s p1 e.
           F_context FC /\
           (h =
            FC
              (ifds,tid,Timed (Recvfrom2 s.fd,d),
               s with <|ps1 := SOME p1; es := SOME e|>))) \/
        (?ts tid d readseq readseq' writeseq writeseq'.
           (h.ts =
            FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d))) /\
           (readseq' =
            FILTER
              (\fd.
                 ?s.
                   MEM s h.s /\ (s.fd = fd) /\
                   ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
           (writeseq' =
            FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
              writeseq) /\ ((readseq' <> []) \/ (writeseq' <> []))) \/
        (?SC ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'.
           (h.ts =
            FUPDATE ts
              (tid,Timed (Sendto2 (s.fd,ips,is1,ps1,is2,ps2,data),d))) /\
           (h.s = SC (s with es := NONE)) /\ socklist_context SC /\
           ((oq',oqf',T) IN
            dosend
              (h.ifds,(ips,data),(s.is1,s.ps1,s.is2,s.ps2),h.oq,h.oqf) /\
            ((ips <> NONE) \/ (s.is2 <> NONE)) \/
            (oq',oqf',T) IN
            dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
           string_size data <= UDPpayloadMax) \/
        (?FC tid d ifds s junk e.
           (h =
            FC
              (ifds,tid,Timed (Sendto2 (s.fd,junk),d),
               s with es := SOME e)) /\ F_context FC) \/
        ?ts tid d fd ips data is1 ps1 is2 ps2 SC s.
          (h.ts =
           FUPDATE ts
             (tid,Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d))) /\
          (h.s = SC (s with es := NONE)) /\ socklist_context SC /\
          (?oq' oqf'.
             (oq',oqf',T) IN
             dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
          (string_size data > UDPpayloadMax \/
           (ips = NONE) /\ (s.is2 = NONE))
   
   [host_redn]
   Definition
   |- host_redn =
      (\a0 a1 a2 a3 a4.
         !host_redn'.
           (!a0 a1 a2 a3 a4.
              (?h ts tid d fd.
                 (a0 = socket_1) /\ (a1 = succeed) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,socket ())) /\
                 (a4 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Ret (OK fd),dsched));
                    s :=
                      Sock (fd,NONE,NONE,NONE,NONE,NONE,Flags (F,F),[])::
                          h.s|>) /\ fd NOTIN sockfds h.s) \/
              (?h ts tid d e.
                 (a0 = socket_2) /\ (a1 = badfail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,socket ())) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
                 e IN {EMFILE; ENFILE}) \/
              (?FC tid d p1' ifds fd es f mq.
                 (a0 = bind_1) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,bind (fd,NONE,NONE))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,NONE,SOME p1',NONE,NONE,es,f,mq))) /\
                 F_context FC /\ p1' IN unused FC INTER ephemeral) \/
              (?FC tid d p1' ifds fd i es f mq.
                 (a0 = bind_2) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,bind (fd,SOME i,NONE))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,SOME i,SOME p1',NONE,NONE,es,f,mq))) /\
                 F_context FC /\ i IN ifds /\
                 p1' IN unused FC INTER ephemeral) \/
              (?FC tid d ifds fd es f mq p.
                 (a0 = bind_3) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,bind (fd,NONE,SOME p))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,NONE,SOME p,NONE,NONE,es,f,mq))) /\
                 F_context FC /\ p NOTIN privileged /\
                 !s.
                   s IN FC /\ (s.ps1 = SOME p) ==>
                   f.reuseaddr /\ s.f.reuseaddr) \/
              (?FC tid d ifds fd es f mq i p.
                 (a0 = bind_4) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,bind (fd,SOME i,SOME p))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,SOME i,SOME p,NONE,NONE,es,f,mq))) /\
                 F_context FC /\ i IN ifds /\ p NOTIN privileged /\
                 !s.
                   s IN FC ==>
                   (s.ps1 = SOME p) /\
                   ((s.is1 = NONE) \/ (s.is1 = SOME i)) ==>
                   f.reuseaddr /\ s.f.reuseaddr) \/
              (?FC tid d ifds s fd is p.
                 (a0 = bind_5) /\ (a1 = fail) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,bind (fd,is,SOME p))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EACCES),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 p IN privileged) \/
              (?FC tid d ifds s fd is p.
                 (a0 = bind_6) /\ (a1 = fail) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,bind (fd,is,SOME p))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EADDRINUSE),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 ~!s'.
                    s' IN FC ==>
                    (s'.ps1 = SOME p) /\
                    ((s'.is1 = NONE) \/ (is = NONE) \/ (is = s'.is1)) ==>
                    s.f.reuseaddr /\ s'.f.reuseaddr) \/
              (?FC tid d ifds s fd i ps.
                 (a0 = bind_7) /\ (a1 = fail) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,bind (fd,SOME i,ps))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EADDRNOTAVAIL),dsched),
                     s with fd := fd)) /\ F_context FC /\ i NOTIN ifds) \/
              (?FC tid d ifds s fd p1 is ps.
                 (a0 = bind_8) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with <|fd := fd; ps1 := SOME p1|>)) /\
                 (a3 = Lh_call (tid,bind (fd,is,ps))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EINVAL),dsched),
                     s with <|fd := fd; ps1 := SOME p1|>)) /\
                 F_context FC) \/
              (?FC tid d ifds fd es f mq is e.
                 (a0 = bind_9) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,bind (fd,is,NONE))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 F_context FC /\ (unused FC INTER ephemeral = {}) /\
                 e IN ephemeralErrors) \/
              (?FC tid d ifds fd ps1 i1 p1' es f mq i ps.
                 (a0 = connect_1) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,ps1,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,connect (fd,i,ps))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,SOME i1,SOME p1',SOME i,ps,es,f,mq))) /\
                 F_context FC /\ i1 IN outroute (ifds,i) /\
                 p1' IN autobind (ps1,FC)) \/
              (?FC tid d ifds fd i1 p1 is2 ps2 es f mq i ps.
                 (a0 = connect_2) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,SOME i1,SOME p1,is2,ps2,es,f,mq))) /\
                 (a3 = Lh_call (tid,connect (fd,i,ps))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,SOME i1,SOME p1,SOME i,ps,es,f,mq))) /\
                 F_context FC) \/
              (?FC tid d ifds fd es f mq i ps s e.
                 (a0 = connect_3) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,connect (fd,i,ps))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 (unused FC INTER ephemeral = {}) /\
                 e IN ephemeralErrors /\
                 socket_ok ifds (s with fd := fd)) \/
              (?FC tid d ifds fd is1 p1 is2 ps2 es f mq.
                 (a0 = disconnect_1) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,is1,SOME p1,is2,ps2,es,f,mq))) /\
                 (a3 = Lh_call (tid,disconnect fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
                 F_context FC) \/
              (?FC tid d ifds fd es f mq p1.
                 (a0 = disconnect_2) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,disconnect fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
                 F_context FC /\ p1 IN unused FC INTER ephemeral) \/
              (?FC tid d ifds fd es f mq e s.
                 (a0 = disconnect_3) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
                 (a3 = Lh_call (tid,disconnect fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 (unused FC INTER ephemeral = {}) /\
                 e IN ephemeralErrors /\
                 socket_ok ifds (s with fd := fd)) \/
              (?FC tid d ifds s fd.
                 (a0 = getsockname_1) /\ (a1 = succeed) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,getsockname fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK (s.is1,s.ps1)),dsched),
                     s with fd := fd)) /\ F_context FC) \/
              (?FC tid d ifds s fd.
                 (a0 = getpeername_1) /\ (a1 = succeed) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,getpeername fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK (s.is2,s.ps2)),dsched),
                     s with fd := fd)) /\ F_context FC) \/
              (?FC tid d ifds s fd.
                 (a0 = geterr_1) /\ (a1 = succeed) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,geterr fd)) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK s.es),dsched),
                     s with <|fd := fd; es := NONE|>)) /\ F_context FC) \/
              (?FC tid d ifds s fd opt b.
                 (a0 = getsockopt_1) /\ (a1 = succeed) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,getsockopt (fd,opt))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK b),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 ((opt = SO_BSDCOMPAT) ==> (b = s.f.bsdcompat)) /\
                 ((opt = SO_REUSEADDR) ==> (b = s.f.reuseaddr))) \/
              (?FC tid d ifds s fd opt b f'.
                 (a0 = setsockopt_1) /\ (a1 = succeed) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
                 (a3 = Lh_call (tid,setsockopt (fd,opt,b))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK ()),dsched),
                     s with <|fd := fd; f := f'|>)) /\ F_context FC /\
                 ((opt = SO_BSDCOMPAT) ==>
                  (f' = s.f with bsdcompat := b)) /\
                 ((opt = SO_REUSEADDR) ==>
                  (f' = s.f with reuseaddr := b))) \/
              (?SC h ts tid d s ips data nb oq' oqf' p1'.
                 (a0 = sendto_1) /\ (a1 = succeed) /\
                 (a2 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Run,d));
                    s := SC (s with es := NONE)|>) /\
                 (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
                 (a4 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                    s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                    oq := oq'; oqf := oqf'|>) /\ socklist_context SC /\
                 p1' IN autobind (s.ps1,SC) /\
                 (oq',oqf',T) IN
                 dosend
                   (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,
                    h.oqf) /\ string_size data <= UDPpayloadMax /\
                 ((ips <> NONE) \/ (s.is2 <> NONE))) \/
              (?SC h ts tid d s ips data p1' oq' oqf'.
                 (a0 = sendto_2) /\ (a1 = enter2) /\
                 (a2 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Run,d));
                    s := SC (s with es := NONE)|>) /\
                 (a3 = Lh_call (tid,sendto (s.fd,ips,data,F))) /\
                 (a4 =
                  h with
                  <|ts :=
                      FUPDATE ts
                        (tid,
                         Timed
                           (Sendto2
                              (s.fd,ips,s.is1,SOME p1',s.is2,s.ps2,data),
                            time_infty));
                    s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                    oq := oq'; oqf := oqf'|>) /\ socklist_context SC /\
                 p1' IN autobind (s.ps1,SC) /\
                 (oq',oqf',F) IN
                 dosend
                   (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,
                    h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE))) \/
              (?SC h ts tid d s ips data p1' oq' oqf'.
                 (a0 = sendto_3) /\ (a1 = fail) /\
                 (a2 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Run,d));
                    s := SC (s with es := NONE)|>) /\
                 (a3 = Lh_call (tid,sendto (s.fd,ips,data,T))) /\
                 (a4 =
                  h with
                  <|ts :=
                      FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched));
                    s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                    oq := oq'; oqf := oqf'|>) /\ socklist_context SC /\
                 p1' IN autobind (s.ps1,SC) /\
                 (oq',oqf',F) IN
                 dosend
                   (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,
                    h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE))) \/
              (?FC tid d ifds fd is1 ps1 f mq data nb p1'.
                 (a0 = sendto_4) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,is1,ps1,NONE,NONE,NONE,f,mq))) /\
                 (a3 = Lh_call (tid,sendto (fd,NONE,data,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL ENOTCONN),dsched),
                     Sock (fd,is1,SOME p1',NONE,NONE,NONE,f,mq))) /\
                 F_context FC /\ p1' IN autobind (ps1,FC)) \/
              (?FC tid d ifds s p1 e ips data nb.
                 (a0 = sendto_5) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with <|ps1 := SOME p1; es := SOME e|>)) /\
                 (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with <|ps1 := SOME p1; es := NONE|>)) /\
                 F_context FC) \/
              (?FC tid d ifds s ips data nb ps1'.
                 (a0 = sendto_6) /\ (a1 = fail) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s)) /\
                 (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EMSGSIZE),dsched),
                     s with ps1 := ps1')) /\ F_context FC /\
                 string_size data > UDPpayloadMax /\
                 ps1' IN {s.ps1} UNION IMAGE SOME (autobind (s.ps1,FC))) \/
              (?FC tid d ifds fd ips data nb f mq e s.
                 (a0 = sendto_7) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,NONE,f,mq))) /\
                 (a3 = Lh_call (tid,sendto (fd,ips,data,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 (autobind (NONE,FC) = {}) /\ e IN ephemeralErrors /\
                 socket_ok ifds (s with fd := fd)) \/
              (?SC h ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'.
                 (a0 = sendto_8) /\ (a1 = slowsucceed) /\
                 (a2 =
                  h with
                  <|ts :=
                      FUPDATE ts
                        (tid,
                         Timed
                           (Sendto2 (s.fd,ips,is1,ps1,is2,ps2,data),d));
                    s := SC (s with es := NONE)|>) /\ (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                    s := SC (s with es := NONE); oq := oq';
                    oqf := oqf'|>) /\ socklist_context SC /\
                 ((oq',oqf',T) IN
                  dosend
                    (h.ifds,(ips,data),(s.is1,s.ps1,s.is2,s.ps2),h.oq,
                     h.oqf) /\ ((ips <> NONE) \/ (s.is2 <> NONE)) \/
                  (oq',oqf',T) IN
                  dosend
                    (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf) /\
                  ((ips <> NONE) \/ (is2 <> NONE))) /\
                 string_size data <= UDPpayloadMax) \/
              (?FC tid d ifds s ips data e.
                 (a0 = sendto_9) /\ (a1 = slowfail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Sendto2 (s.fd,ips,data),d),
                     s with es := SOME e)) /\ (a3 = Lh_tau) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with es := NONE)) /\ F_context FC) \/
              (?h ts tid d fd ips is1 ps1 is2 ps2 e data SC s.
                 (a0 = sendto_10) /\ (a1 = slowfail) /\
                 (a2 =
                  h with
                  <|ts :=
                      FUPDATE ts
                        (tid,
                         Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d));
                    s := SC (s with es := NONE)|>) /\ (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched));
                    s := SC (s with es := NONE)|>) /\
                 socklist_context SC /\
                 (?oq' oqf'.
                    (oq',oqf',T) IN
                    dosend
                      (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
                 (string_size data > UDPpayloadMax /\ (e = EMSGSIZE) \/
                  (s.is2 = NONE) /\ (ips = NONE) /\ (e = ENOTCONN))) \/
              (?FC tid d ifds s i3 i4 ifid mq nb p1 ps3 ps4 data.
                 (a0 = recvfrom_1) /\ (a1 = succeed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with
                     <|ps1 := SOME p1; es := NONE;
                       mq :=
                         (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)) /\
                 (a3 = Lh_call (tid,recvfrom (s.fd,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
                     s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
                 F_context FC) \/
              (?FC tid d ifds s p1'.
                 (a0 = recvfrom_2) /\ (a1 = enter2) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with <|es := NONE; mq := []|>)) /\
                 (a3 = Lh_call (tid,recvfrom (s.fd,F))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Recvfrom2 s.fd,time_infty),
                     s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
                 F_context FC /\ p1' IN autobind (s.ps1,FC)) \/
              (?FC tid d ifds s p1'.
                 (a0 = recvfrom_3) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with <|es := NONE; mq := []|>)) /\
                 (a3 = Lh_call (tid,recvfrom (s.fd,T))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL EAGAIN),dsched),
                     s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
                 F_context FC /\ p1' IN autobind (s.ps1,FC)) \/
              (?FC tid d ifds s p1 e nb.
                 (a0 = recvfrom_4) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     s with <|ps1 := SOME p1; es := SOME e|>)) /\
                 (a3 = Lh_call (tid,recvfrom (s.fd,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with <|ps1 := SOME p1; es := NONE|>)) /\
                 F_context FC) \/
              (?FC tid d ifds fd nb f e s.
                 (a0 = recvfrom_5) /\ (a1 = fail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Run,d),
                     Sock (fd,NONE,NONE,NONE,NONE,NONE,f,[]))) /\
                 (a3 = Lh_call (tid,recvfrom (fd,nb))) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with fd := fd)) /\ F_context FC /\
                 (autobind (NONE,FC) = {}) /\ e IN ephemeralErrors /\
                 socket_ok ifds (s with fd := fd)) \/
              (?FC tid d ifds s p1 mq i3 i4 ps3 ps4 data ifid.
                 (a0 = recvfrom_6) /\ (a1 = slowsucceed) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Recvfrom2 s.fd,d),
                     s with
                     <|ps1 := SOME p1; es := NONE;
                       mq :=
                         (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
                     s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
                 F_context FC) \/
              (?FC tid d ifds s p1 e.
                 (a0 = recvfrom_7) /\ (a1 = slowfail) /\
                 (a2 =
                  FC
                    (ifds,tid,Timed (Recvfrom2 s.fd,d),
                     s with <|ps1 := SOME p1; es := SOME e|>)) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  FC
                    (ifds,tid,Timed (Ret (FAIL e),dsched),
                     s with <|ps1 := SOME p1; es := NONE|>)) /\
                 F_context FC) \/
              (?h ts tid d s1 s2 s.
                 (a0 = close_1) /\ (a1 = succeed) /\
                 (a2 =
                  h with
                  <|ts := FUPDATE ts (tid,Timed (Run,d));
                    s := APPEND s1 (s::s2)|>) /\
                 (a3 = Lh_call (tid,close s.fd)) /\
                 (a4 =
                  h with
                  <|ts :=
                      zombify s.fd o_f
                      FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                    s := APPEND s1 s2|>) /\ T) \/
              (?h ts tid d d' readseq writeseq tms.
                 (a0 = select_1) /\ (a1 = enter2) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,select (readseq,writeseq,tms))) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,Timed (Select2 (readseq,writeseq),d'))) /\
                 LIST_TO_SET (APPEND readseq writeseq) SUBSET
                 sockfds h.s /\ (!i. (tms = SOME i) ==> 0 <= i) /\
                 (d' =
                  case tms of
                     NONE -> time_infty
                  || SOME v -> time (real_of_int v / 1000000))) \/
              (?h ts tid d readseq writeseq tm.
                 (a0 = select_2) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,select (readseq,writeseq,SOME tm))) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
                 tm < 0) \/
              (?h ts tid d readseq readseq' writeseq writeseq'.
                 (a0 = select_3) /\ (a1 = slowsucceed) /\
                 (a2 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,Timed (Select2 (readseq,writeseq),d))) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,
                       Timed (Ret (OK (readseq',writeseq')),dsched))) /\
                 (readseq' =
                  FILTER
                    (\fd.
                       ?s.
                         MEM s h.s /\ (s.fd = fd) /\
                         ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
                 (writeseq' =
                  FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
                    writeseq) /\
                 ((readseq' <> []) \/ (writeseq' <> []))) \/
              (?h ts tid readseq readseq' writeseq writeseq'.
                 (a0 = select_4) /\ (a1 = slowsucceed) /\
                 (a2 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,
                       Timed (Select2 (readseq,writeseq),time_zero))) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,
                       Timed (Ret (OK (readseq',writeseq')),dsched))) /\
                 (readseq' =
                  FILTER
                    (\fd.
                       ?s.
                         MEM s h.s /\ (s.fd = fd) /\
                         ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
                 (writeseq' =
                  FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
                    writeseq) /\ (readseq' = []) /\ (writeseq' = [])) \/
              (?h ts tid d tm d'.
                 (a0 = delay_1) /\ (a1 = enter2) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,delay tm)) /\
                 (a4 = h with ts := FUPDATE ts (tid,Timed (Delay2,d'))) /\
                 tm >= 0 /\ (d' = time (real_of_int tm / 1000000))) \/
              (?h ts tid d tm.
                 (a0 = delay_2) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,delay tm)) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
                 tm < 0) \/
              (?h ts tid.
                 (a0 = delay_3) /\ (a1 = slowsucceed) /\
                 (a2 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Delay2,time_zero))) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
                 T) \/
              (?h ts tid d iflist ifset.
                 (a0 = getifaddrs_1) /\ (a1 = succeed) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,getifaddrs ())) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (OK iflist),dsched))) /\
                 iflist IN orderings ifset /\
                 (ifset =
                  {(hifd.ifid,hifd.primary,ipslist,hifd.netmask)
                   |
                   hifd IN h.ifds /\ ipslist IN orderings hifd.ipset})) \/
              (?h ts tid d v.
                 (a0 = console_print_1) /\ (a1 = enter2) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,print_endline_flush v)) /\
                 (a4 =
                  h with ts := FUPDATE ts (tid,Timed (Print2 v,dsched))) /\
                 T) \/
              (?h ts tid d v.
                 (a0 = console_print_2) /\ (a1 = misc) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Print2 v,d))) /\
                 (a3 = Lh_console v) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
                 T) \/
              (?h ts tid d v.
                 (a0 = convert_port_1) /\ (a1 = succeed) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,port_of_int v)) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts
                      (tid,Timed (Ret (OK (Port (Num v))),dsched))) /\
                 1 <= v /\ v <= 65535) \/
              (?h ts tid d v.
                 (a0 = convert_port_2) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,port_of_int v)) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
                 (v < 1 \/ v > 65535)) \/
              (?h ts tid d v i.
                 (a0 = convert_ip_1) /\ (a1 = succeed) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,ip_of_string v)) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (OK i),dsched))) /\
                 valid_ip_string v /\ (i = ipstr_to_ip v)) \/
              (?h ts tid d v.
                 (a0 = convert_ip_2) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,ip_of_string v)) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
                 ~valid_ip_string v) \/
              (?h ts tid d readseq writeseq tms.
                 (a0 = notsockfd_1) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,select (readseq,writeseq,tms))) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EBADF),dsched))) /\
                 ?fd.
                   MEM fd (APPEND readseq writeseq) /\
                   fd NOTIN sockfds h.s) \/
              (?h ts tid d fd opn e.
                 (a0 = notsockfd_2) /\ (a1 = fail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,opn)) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
                 opn IN OP fd /\ fd NOTIN sockfds h.s /\
                 e IN {ENOTSOCK; EBADF}) \/
              (?h ts tid d opn.
                 (a0 = intr_1) /\ (a1 = slowfail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (opn,d))) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EINTR),dsched))) /\
                 ((?v. opn = Sendto2 v) \/ (?v. opn = Recvfrom2 v) \/
                  (?v. opn = Select2 v) \/ (?v. opn = Print2 v) \/
                  (opn = Delay2) \/ (opn = Zombie))) \/
              (?h ts tid d e.
                 (a0 = badmem_1) /\ (a1 = badfail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,socket ())) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
                 e IN {ENOMEM; ENOBUFS}) \/
              (?FC ifds tid d s opn e.
                 (a0 = badmem_2) /\ (a1 = badfail) /\
                 (a2 = FC (ifds,tid,Timed (Run,d),s)) /\
                 (a3 = Lh_call (tid,opn)) /\
                 (a4 = FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
                 F_context FC /\ opn IN OP s.fd /\
                 e IN {ENOMEM; ENOBUFS}) \/
              (?FC ifds tid t d s e.
                 (a0 = badmem_3) /\ (a1 = badfail) /\
                 (a2 = FC (ifds,tid,Timed (t,d),s)) /\ (a3 = Lh_tau) /\
                 (a4 = FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
                 F_context FC /\ t IN OP2 s.fd /\
                 e IN {ENOMEM; ENOBUFS}) \/
              (?h ts tid d v e.
                 (a0 = badmem_4) /\ (a1 = badfail) /\
                 (a2 =
                  h with ts := FUPDATE ts (tid,Timed (Select2 v,d))) /\
                 (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
                 e IN {ENOMEM; ENOBUFS}) \/
              (?h ts tid d.
                 (a0 = exit_1) /\ (a1 = exit) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,exit ())) /\
                 (a4 =
                  h with ts := FUPDATE ts (tid,Timed (Exit,dsched))) /\
                 T) \/
              (?h ts tid d.
                 (a0 = exit_2) /\ (a1 = exit) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Exit,d))) /\
                 (a3 = Lh_exit) /\
                 (a4 = h with <|ts := FEMPTY; s := []|>) /\ T) \/
              (?h ts tid d v.
                 (a0 = ret_1) /\ (a1 = misc) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Ret v,d))) /\
                 (a3 = Lh_return (tid,v)) /\
                 (a4 =
                  h with ts := FUPDATE ts (tid,Timed (Run,time_infty))) /\
                 T) \/
              (?h ts tid d tid'.
                 (a0 = create_1) /\ (a1 = succeed) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,create ())) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE (FUPDATE ts (tid,Timed (Ret (OK tid'),dsched)))
                      (tid',Timed (Run,time_infty))) /\
                 tid' NOTIN {tid} UNION FDOM ts) \/
              (?h ts tid d.
                 (a0 = create_2) /\ (a1 = badfail) /\
                 (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
                 (a3 = Lh_call (tid,create ())) /\
                 (a4 =
                  h with
                  ts :=
                    FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched))) /\
                 T) \/
              (?body i1 i2 oq' oqf'.
                 (a0 = delivery_out_1) /\ (a1 = misc) /\
                 (a3 = Lh_sendmsg (IP (i1,i2,body))) /\
                 (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
                 (IP (i1,i2,body),oq',oqf') IN dequeue (a2.oq,a2.oqf) /\
                 i2 NOTIN LOOPBACK UNION MARTIAN /\ i1 NOTIN MARTIAN) \/
              (?oq' oqf'.
                 (a0 = delivery_out_martian) /\ (a1 = misc) /\
                 (a3 = Lh_tau) /\
                 (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
                 ?i1 i2 body.
                   (IP (i1,i2,body),oq',oqf') IN dequeue (a2.oq,a2.oqf) /\
                   i2 IN MARTIAN) \/
              (?h SC s i3 i4 ifd ps3 ps4 data.
                 (a0 = delivery_in_udp_1) /\ (a1 = misc) /\
                 (a2 = h with s := SC s) /\
                 (a3 = Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data)))) /\
                 (a4 =
                  h with
                  s :=
                    SC
                      (s with
                       mq :=
                         APPEND s.mq
                           [(IP (i3,i4,UDP (ps3,ps4,data)),ifd.ifid)])) /\
                 socklist_context SC /\
                 s IN lookup (SC s) (i3,ps3,i4,ps4) /\ ifd IN h.ifds /\
                 i4 IN ifd.ipset /\ i4 NOTIN LOOPBACK /\
                 i3 NOTIN MARTIAN UNION LOOPBACK) \/
              (?i3 i4 oq' oqf' ps3 ps4 data ok.
                 (a0 = delivery_in_udp_2) /\ (a1 = misc) /\
                 (a3 = Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data)))) /\
                 (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
                 i4 IN a2.ifds /\ (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
                 (oq',oqf',ok) IN
                 {(a2.oq,a2.oqf,T)} UNION
                 enqueue
                   (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),a2.oq,
                    a2.oqf) /\ i4 NOTIN LOOPBACK /\
                 i3 NOTIN MARTIAN UNION LOOPBACK) \/
              (?i3 i4 body.
                 (a0 = delivery_in_martian_3) /\ (a1 = misc) /\
                 (a3 = Lh_recvmsg (IP (i3,i4,body))) /\ (a4 = a2) /\
                 i4 IN a2.ifds /\ i4 NOTIN LOOPBACK /\
                 (loopback (IP (i3,i4,body)) \/
                  martian (IP (i3,i4,body)))) \/
              (?h s SC es' i3' i4' i3 ps3 i4 ps4 body.
                 (a0 = delivery_in_icmp_1) /\ (a1 = misc) /\
                 (a2 = h with s := SC s) /\
                 (a3 = Lh_recvmsg (IP (i4',i3',body))) /\
                 (a4 = h with s := SC (s with es := es')) /\
                 socklist_context SC /\
                 ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
                  (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
                 s IN lookup (SC s) (i3,ps3,i4,ps4) /\ i3' IN h.ifds /\
                 ~(loopback (IP (i4',i3',body)) \/
                   martian (IP (i4',i3',body))) /\
                 (es' =
                  (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
                     SOME ECONNREFUSED
                   else
                     s.es))) \/
              (?i3' i4' i3 ps3 i4 ps4 body.
                 (a0 = delivery_in_icmp_2) /\ (a1 = misc) /\
                 (a3 = Lh_recvmsg (IP (i4',i3',body))) /\ (a4 = a2) /\
                 i3' IN a2.ifds /\
                 ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
                  (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
                 (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
                 ~(loopback (IP (i4',i3',body)) \/
                   martian (IP (i4',i3',body)))) \/
              (?h i3 i4 SC s ifid oq' oqf' ps3 ps4 data.
                 (a0 = delivery_loopback_udp_1) /\ (a1 = misc) /\
                 (a2 = h with s := SC s) /\ (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  <|s :=
                      SC
                        (s with
                         mq :=
                           APPEND s.mq
                             [(IP (i3,i4,UDP (ps3,ps4,data)),ifid)]);
                    oq := oq'; oqf := oqf'|>) /\ socklist_context SC /\
                 (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
                 dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
                 s IN lookup (SC s) (i3,ps3,i4,ps4) /\
                 <|ifid := ifid; ipset := LOOPBACK; primary := localhost;
                   netmask := NETMASK (255 * 2 ** 24)|> IN h.ifds) \/
              (?i3 i4 oq' oq'' oqf' oqf'' ps3 ps4 data ok.
                 (a0 = delivery_loopback_udp_2) /\ (a1 = misc) /\
                 (a3 = Lh_tau) /\
                 (a4 = a2 with <|oq := oq''; oqf := oqf''|>) /\
                 (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
                 dequeue (a2.oq,a2.oqf) /\ i4 IN LOOPBACK /\
                 (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
                 (oq'',oqf'',ok) IN
                 enqueue
                   (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',
                    oqf')) \/
              (?h SC s es' oq' oqf' i3' i4' i3 ps3 i4 ps4.
                 (a0 = delivery_loopback_icmp_1) /\ (a1 = misc) /\
                 (a2 = h with s := SC s) /\ (a3 = Lh_tau) /\
                 (a4 =
                  h with
                  <|s := SC (s with es := es'); oq := oq';
                    oqf := oqf'|>) /\ socklist_context SC /\
                 (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',
                  oqf') IN dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
                 s IN lookup (SC s) (i4,ps4,i3,ps3) /\
                 (es' =
                  (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
                     SOME ECONNREFUSED
                   else
                     s.es))) \/
              (?i3' i4' oq' oqf' i3 ps3 i4 ps4.
                 (a0 = delivery_loopback_icmp_2) /\ (a1 = misc) /\
                 (a3 = Lh_tau) /\
                 (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
                 (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',
                  oqf') IN dequeue (a2.oq,a2.oqf) /\ i3' IN LOOPBACK /\
                 (lookup a2.s (i4,ps4,i3,ps3) = {})) \/
              (?d.
                 (a0 = epsilon_1) /\ (a1 = misc) /\ (a3 = Lh_epsilon d) /\
                 d > 0 /\ (Time_Pass d a2 = SOME a4)) ==>
              host_redn' a0 a1 a2 a3 a4) ==>
           host_redn' a0 a1 a2 a3 a4)
   
   [host_redn'_def]
   Definition
   |- !h0 l h. h0 -- l ---> h = ?rid rcat. rid /* rcat */ h0 -- l --> h
   
   [revimp_def]  Definition  |- !q p. q <== p = p ==> q
   
   [Time_Pass_xd_def]
   Theorem
   |- Time_Pass_xd dur (Timed (x,d)) =
      case Time_Pass_d dur d of
         NONE -> NONE
      || SOME v -> SOME (Timed (x,v))
   
   [Time_Pass_xd_ind]
   Theorem
   |- !P. (!dur x d. P dur (Timed (x,d))) ==> !v v1. P v v1
   
   [host_redn_cases]
   Theorem
   |- !a0 a1 a2 a3 a4.
        a0 /* a1 */ a2 -- a3 --> a4 =
        (?h ts tid d fd.
           (a0 = socket_1) /\ (a1 = succeed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,socket ())) /\
           (a4 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Ret (OK fd),dsched));
              s :=
                Sock (fd,NONE,NONE,NONE,NONE,NONE,Flags (F,F),[])::
                    h.s|>) /\ fd NOTIN sockfds h.s) \/
        (?h ts tid d e.
           (a0 = socket_2) /\ (a1 = badfail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,socket ())) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
           e IN {EMFILE; ENFILE}) \/
        (?FC tid d p1' ifds fd es f mq.
           (a0 = bind_1) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,bind (fd,NONE,NONE))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,NONE,SOME p1',NONE,NONE,es,f,mq))) /\
           F_context FC /\ p1' IN unused FC INTER ephemeral) \/
        (?FC tid d p1' ifds fd i es f mq.
           (a0 = bind_2) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,bind (fd,SOME i,NONE))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,SOME i,SOME p1',NONE,NONE,es,f,mq))) /\
           F_context FC /\ i IN ifds /\
           p1' IN unused FC INTER ephemeral) \/
        (?FC tid d ifds fd es f mq p.
           (a0 = bind_3) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,bind (fd,NONE,SOME p))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,NONE,SOME p,NONE,NONE,es,f,mq))) /\ F_context FC /\
           p NOTIN privileged /\
           !s.
             s IN FC /\ (s.ps1 = SOME p) ==>
             f.reuseaddr /\ s.f.reuseaddr) \/
        (?FC tid d ifds fd es f mq i p.
           (a0 = bind_4) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,bind (fd,SOME i,SOME p))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,SOME i,SOME p,NONE,NONE,es,f,mq))) /\
           F_context FC /\ i IN ifds /\ p NOTIN privileged /\
           !s.
             s IN FC ==>
             (s.ps1 = SOME p) /\ ((s.is1 = NONE) \/ (s.is1 = SOME i)) ==>
             f.reuseaddr /\ s.f.reuseaddr) \/
        (?FC tid d ifds s fd is p.
           (a0 = bind_5) /\ (a1 = fail) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,bind (fd,is,SOME p))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EACCES),dsched),
               s with fd := fd)) /\ F_context FC /\ p IN privileged) \/
        (?FC tid d ifds s fd is p.
           (a0 = bind_6) /\ (a1 = fail) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,bind (fd,is,SOME p))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EADDRINUSE),dsched),
               s with fd := fd)) /\ F_context FC /\
           ~!s'.
              s' IN FC ==>
              (s'.ps1 = SOME p) /\
              ((s'.is1 = NONE) \/ (is = NONE) \/ (is = s'.is1)) ==>
              s.f.reuseaddr /\ s'.f.reuseaddr) \/
        (?FC tid d ifds s fd i ps.
           (a0 = bind_7) /\ (a1 = fail) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,bind (fd,SOME i,ps))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EADDRNOTAVAIL),dsched),
               s with fd := fd)) /\ F_context FC /\ i NOTIN ifds) \/
        (?FC tid d ifds s fd p1 is ps.
           (a0 = bind_8) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               s with <|fd := fd; ps1 := SOME p1|>)) /\
           (a3 = Lh_call (tid,bind (fd,is,ps))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EINVAL),dsched),
               s with <|fd := fd; ps1 := SOME p1|>)) /\ F_context FC) \/
        (?FC tid d ifds fd es f mq is e.
           (a0 = bind_9) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,bind (fd,is,NONE))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL e),dsched),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\ F_context FC /\
           (unused FC INTER ephemeral = {}) /\ e IN ephemeralErrors) \/
        (?FC tid d ifds fd ps1 i1 p1' es f mq i ps.
           (a0 = connect_1) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,ps1,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,connect (fd,i,ps))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,SOME i1,SOME p1',SOME i,ps,es,f,mq))) /\
           F_context FC /\ i1 IN outroute (ifds,i) /\
           p1' IN autobind (ps1,FC)) \/
        (?FC tid d ifds fd i1 p1 is2 ps2 es f mq i ps.
           (a0 = connect_2) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,SOME i1,SOME p1,is2,ps2,es,f,mq))) /\
           (a3 = Lh_call (tid,connect (fd,i,ps))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,SOME i1,SOME p1,SOME i,ps,es,f,mq))) /\
           F_context FC) \/
        (?FC tid d ifds fd es f mq i ps s e.
           (a0 = connect_3) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,connect (fd,i,ps))) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
           F_context FC /\ (unused FC INTER ephemeral = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd)) \/
        (?FC tid d ifds fd is1 p1 is2 ps2 es f mq.
           (a0 = disconnect_1) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,is1,SOME p1,is2,ps2,es,f,mq))) /\
           (a3 = Lh_call (tid,disconnect fd)) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
           F_context FC) \/
        (?FC tid d ifds fd es f mq p1.
           (a0 = disconnect_2) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,disconnect fd)) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
           F_context FC /\ p1 IN unused FC INTER ephemeral) \/
        (?FC tid d ifds fd es f mq e s.
           (a0 = disconnect_3) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
           (a3 = Lh_call (tid,disconnect fd)) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
           F_context FC /\ (unused FC INTER ephemeral = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd)) \/
        (?FC tid d ifds s fd.
           (a0 = getsockname_1) /\ (a1 = succeed) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,getsockname fd)) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK (s.is1,s.ps1)),dsched),
               s with fd := fd)) /\ F_context FC) \/
        (?FC tid d ifds s fd.
           (a0 = getpeername_1) /\ (a1 = succeed) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,getpeername fd)) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK (s.is2,s.ps2)),dsched),
               s with fd := fd)) /\ F_context FC) \/
        (?FC tid d ifds s fd.
           (a0 = geterr_1) /\ (a1 = succeed) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,geterr fd)) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK s.es),dsched),
               s with <|fd := fd; es := NONE|>)) /\ F_context FC) \/
        (?FC tid d ifds s fd opt b.
           (a0 = getsockopt_1) /\ (a1 = succeed) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,getsockopt (fd,opt))) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (OK b),dsched),s with fd := fd)) /\
           F_context FC /\
           ((opt = SO_BSDCOMPAT) ==> (b = s.f.bsdcompat)) /\
           ((opt = SO_REUSEADDR) ==> (b = s.f.reuseaddr))) \/
        (?FC tid d ifds s fd opt b f'.
           (a0 = setsockopt_1) /\ (a1 = succeed) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s with fd := fd)) /\
           (a3 = Lh_call (tid,setsockopt (fd,opt,b))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK ()),dsched),
               s with <|fd := fd; f := f'|>)) /\ F_context FC /\
           ((opt = SO_BSDCOMPAT) ==> (f' = s.f with bsdcompat := b)) /\
           ((opt = SO_REUSEADDR) ==> (f' = s.f with reuseaddr := b))) \/
        (?SC h ts tid d s ips data nb oq' oqf' p1'.
           (a0 = sendto_1) /\ (a1 = succeed) /\
           (a2 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Run,d));
              s := SC (s with es := NONE)|>) /\
           (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
           (a4 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
              s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
              oqf := oqf'|>) /\ socklist_context SC /\
           p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',T) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           string_size data <= UDPpayloadMax /\
           ((ips <> NONE) \/ (s.is2 <> NONE))) \/
        (?SC h ts tid d s ips data p1' oq' oqf'.
           (a0 = sendto_2) /\ (a1 = enter2) /\
           (a2 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Run,d));
              s := SC (s with es := NONE)|>) /\
           (a3 = Lh_call (tid,sendto (s.fd,ips,data,F))) /\
           (a4 =
            h with
            <|ts :=
                FUPDATE ts
                  (tid,
                   Timed
                     (Sendto2 (s.fd,ips,s.is1,SOME p1',s.is2,s.ps2,data),
                      time_infty));
              s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
              oqf := oqf'|>) /\ socklist_context SC /\
           p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',F) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           ((ips <> NONE) \/ (s.is2 <> NONE))) \/
        (?SC h ts tid d s ips data p1' oq' oqf'.
           (a0 = sendto_3) /\ (a1 = fail) /\
           (a2 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Run,d));
              s := SC (s with es := NONE)|>) /\
           (a3 = Lh_call (tid,sendto (s.fd,ips,data,T))) /\
           (a4 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched));
              s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
              oqf := oqf'|>) /\ socklist_context SC /\
           p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',F) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           ((ips <> NONE) \/ (s.is2 <> NONE))) \/
        (?FC tid d ifds fd is1 ps1 f mq data nb p1'.
           (a0 = sendto_4) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,is1,ps1,NONE,NONE,NONE,f,mq))) /\
           (a3 = Lh_call (tid,sendto (fd,NONE,data,nb))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL ENOTCONN),dsched),
               Sock (fd,is1,SOME p1',NONE,NONE,NONE,f,mq))) /\
           F_context FC /\ p1' IN autobind (ps1,FC)) \/
        (?FC tid d ifds s p1 e ips data nb.
           (a0 = sendto_5) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               s with <|ps1 := SOME p1; es := SOME e|>)) /\
           (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL e),dsched),
               s with <|ps1 := SOME p1; es := NONE|>)) /\ F_context FC) \/
        (?FC tid d ifds s ips data nb ps1'.
           (a0 = sendto_6) /\ (a1 = fail) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s)) /\
           (a3 = Lh_call (tid,sendto (s.fd,ips,data,nb))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EMSGSIZE),dsched),
               s with ps1 := ps1')) /\ F_context FC /\
           string_size data > UDPpayloadMax /\
           ps1' IN {s.ps1} UNION IMAGE SOME (autobind (s.ps1,FC))) \/
        (?FC tid d ifds fd ips data nb f mq e s.
           (a0 = sendto_7) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,NONE,f,mq))) /\
           (a3 = Lh_call (tid,sendto (fd,ips,data,nb))) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
           F_context FC /\ (autobind (NONE,FC) = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd)) \/
        (?SC h ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'.
           (a0 = sendto_8) /\ (a1 = slowsucceed) /\
           (a2 =
            h with
            <|ts :=
                FUPDATE ts
                  (tid,Timed (Sendto2 (s.fd,ips,is1,ps1,is2,ps2,data),d));
              s := SC (s with es := NONE)|>) /\ (a3 = Lh_tau) /\
           (a4 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
              s := SC (s with es := NONE); oq := oq'; oqf := oqf'|>) /\
           socklist_context SC /\
           ((oq',oqf',T) IN
            dosend
              (h.ifds,(ips,data),(s.is1,s.ps1,s.is2,s.ps2),h.oq,h.oqf) /\
            ((ips <> NONE) \/ (s.is2 <> NONE)) \/
            (oq',oqf',T) IN
            dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf) /\
            ((ips <> NONE) \/ (is2 <> NONE))) /\
           string_size data <= UDPpayloadMax) \/
        (?FC tid d ifds s ips data e.
           (a0 = sendto_9) /\ (a1 = slowfail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Sendto2 (s.fd,ips,data),d),
               s with es := SOME e)) /\ (a3 = Lh_tau) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with es := NONE)) /\
           F_context FC) \/
        (?h ts tid d fd ips is1 ps1 is2 ps2 e data SC s.
           (a0 = sendto_10) /\ (a1 = slowfail) /\
           (a2 =
            h with
            <|ts :=
                FUPDATE ts
                  (tid,Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d));
              s := SC (s with es := NONE)|>) /\ (a3 = Lh_tau) /\
           (a4 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched));
              s := SC (s with es := NONE)|>) /\ socklist_context SC /\
           (?oq' oqf'.
              (oq',oqf',T) IN
              dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
           (string_size data > UDPpayloadMax /\ (e = EMSGSIZE) \/
            (s.is2 = NONE) /\ (ips = NONE) /\ (e = ENOTCONN))) \/
        (?FC tid d ifds s i3 i4 ifid mq nb p1 ps3 ps4 data.
           (a0 = recvfrom_1) /\ (a1 = succeed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               s with
               <|ps1 := SOME p1; es := NONE;
                 mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)) /\
           (a3 = Lh_call (tid,recvfrom (s.fd,nb))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
               s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
           F_context FC) \/
        (?FC tid d ifds s p1'.
           (a0 = recvfrom_2) /\ (a1 = enter2) /\
           (a2 =
            FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>)) /\
           (a3 = Lh_call (tid,recvfrom (s.fd,F))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Recvfrom2 s.fd,time_infty),
               s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
           F_context FC /\ p1' IN autobind (s.ps1,FC)) \/
        (?FC tid d ifds s p1'.
           (a0 = recvfrom_3) /\ (a1 = fail) /\
           (a2 =
            FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>)) /\
           (a3 = Lh_call (tid,recvfrom (s.fd,T))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL EAGAIN),dsched),
               s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
           F_context FC /\ p1' IN autobind (s.ps1,FC)) \/
        (?FC tid d ifds s p1 e nb.
           (a0 = recvfrom_4) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               s with <|ps1 := SOME p1; es := SOME e|>)) /\
           (a3 = Lh_call (tid,recvfrom (s.fd,nb))) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL e),dsched),
               s with <|ps1 := SOME p1; es := NONE|>)) /\ F_context FC) \/
        (?FC tid d ifds fd nb f e s.
           (a0 = recvfrom_5) /\ (a1 = fail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Run,d),
               Sock (fd,NONE,NONE,NONE,NONE,NONE,f,[]))) /\
           (a3 = Lh_call (tid,recvfrom (fd,nb))) /\
           (a4 =
            FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
           F_context FC /\ (autobind (NONE,FC) = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd)) \/
        (?FC tid d ifds s p1 mq i3 i4 ps3 ps4 data ifid.
           (a0 = recvfrom_6) /\ (a1 = slowsucceed) /\
           (a2 =
            FC
              (ifds,tid,Timed (Recvfrom2 s.fd,d),
               s with
               <|ps1 := SOME p1; es := NONE;
                 mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)) /\
           (a3 = Lh_tau) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
               s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
           F_context FC) \/
        (?FC tid d ifds s p1 e.
           (a0 = recvfrom_7) /\ (a1 = slowfail) /\
           (a2 =
            FC
              (ifds,tid,Timed (Recvfrom2 s.fd,d),
               s with <|ps1 := SOME p1; es := SOME e|>)) /\
           (a3 = Lh_tau) /\
           (a4 =
            FC
              (ifds,tid,Timed (Ret (FAIL e),dsched),
               s with <|ps1 := SOME p1; es := NONE|>)) /\ F_context FC) \/
        (?h ts tid d s1 s2 s.
           (a0 = close_1) /\ (a1 = succeed) /\
           (a2 =
            h with
            <|ts := FUPDATE ts (tid,Timed (Run,d));
              s := APPEND s1 (s::s2)|>) /\
           (a3 = Lh_call (tid,close s.fd)) /\
           (a4 =
            h with
            <|ts :=
                zombify s.fd o_f
                FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
              s := APPEND s1 s2|>) /\ T) \/
        (?h ts tid d d' readseq writeseq tms.
           (a0 = select_1) /\ (a1 = enter2) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,select (readseq,writeseq,tms))) /\
           (a4 =
            h with
            ts :=
              FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d'))) /\
           LIST_TO_SET (APPEND readseq writeseq) SUBSET sockfds h.s /\
           (!i. (tms = SOME i) ==> 0 <= i) /\
           (d' =
            case tms of
               NONE -> time_infty
            || SOME v -> time (real_of_int v / 1000000))) \/
        (?h ts tid d readseq writeseq tm.
           (a0 = select_2) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,select (readseq,writeseq,SOME tm))) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
           tm < 0) \/
        (?h ts tid d readseq readseq' writeseq writeseq'.
           (a0 = select_3) /\ (a1 = slowsucceed) /\
           (a2 =
            h with
            ts := FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d))) /\
           (a3 = Lh_tau) /\
           (a4 =
            h with
            ts :=
              FUPDATE ts
                (tid,Timed (Ret (OK (readseq',writeseq')),dsched))) /\
           (readseq' =
            FILTER
              (\fd.
                 ?s.
                   MEM s h.s /\ (s.fd = fd) /\
                   ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
           (writeseq' =
            FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
              writeseq) /\ ((readseq' <> []) \/ (writeseq' <> []))) \/
        (?h ts tid readseq readseq' writeseq writeseq'.
           (a0 = select_4) /\ (a1 = slowsucceed) /\
           (a2 =
            h with
            ts :=
              FUPDATE ts
                (tid,Timed (Select2 (readseq,writeseq),time_zero))) /\
           (a3 = Lh_tau) /\
           (a4 =
            h with
            ts :=
              FUPDATE ts
                (tid,Timed (Ret (OK (readseq',writeseq')),dsched))) /\
           (readseq' =
            FILTER
              (\fd.
                 ?s.
                   MEM s h.s /\ (s.fd = fd) /\
                   ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
           (writeseq' =
            FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
              writeseq) /\ (readseq' = []) /\ (writeseq' = [])) \/
        (?h ts tid d tm d'.
           (a0 = delay_1) /\ (a1 = enter2) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,delay tm)) /\
           (a4 = h with ts := FUPDATE ts (tid,Timed (Delay2,d'))) /\
           tm >= 0 /\ (d' = time (real_of_int tm / 1000000))) \/
        (?h ts tid d tm.
           (a0 = delay_2) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,delay tm)) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
           tm < 0) \/
        (?h ts tid.
           (a0 = delay_3) /\ (a1 = slowsucceed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Delay2,time_zero))) /\
           (a3 = Lh_tau) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
           T) \/
        (?h ts tid d iflist ifset.
           (a0 = getifaddrs_1) /\ (a1 = succeed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,getifaddrs ())) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (OK iflist),dsched))) /\
           iflist IN orderings ifset /\
           (ifset =
            {(hifd.ifid,hifd.primary,ipslist,hifd.netmask)
             |
             hifd IN h.ifds /\ ipslist IN orderings hifd.ipset})) \/
        (?h ts tid d v.
           (a0 = console_print_1) /\ (a1 = enter2) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,print_endline_flush v)) /\
           (a4 = h with ts := FUPDATE ts (tid,Timed (Print2 v,dsched))) /\
           T) \/
        (?h ts tid d v.
           (a0 = console_print_2) /\ (a1 = misc) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Print2 v,d))) /\
           (a3 = Lh_console v) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
           T) \/
        (?h ts tid d v.
           (a0 = convert_port_1) /\ (a1 = succeed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,port_of_int v)) /\
           (a4 =
            h with
            ts :=
              FUPDATE ts (tid,Timed (Ret (OK (Port (Num v))),dsched))) /\
           1 <= v /\ v <= 65535) \/
        (?h ts tid d v.
           (a0 = convert_port_2) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,port_of_int v)) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
           (v < 1 \/ v > 65535)) \/
        (?h ts tid d v i.
           (a0 = convert_ip_1) /\ (a1 = succeed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,ip_of_string v)) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (OK i),dsched))) /\
           valid_ip_string v /\ (i = ipstr_to_ip v)) \/
        (?h ts tid d v.
           (a0 = convert_ip_2) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,ip_of_string v)) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
           ~valid_ip_string v) \/
        (?h ts tid d readseq writeseq tms.
           (a0 = notsockfd_1) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,select (readseq,writeseq,tms))) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EBADF),dsched))) /\
           ?fd.
             MEM fd (APPEND readseq writeseq) /\ fd NOTIN sockfds h.s) \/
        (?h ts tid d fd opn e.
           (a0 = notsockfd_2) /\ (a1 = fail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,opn)) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
           opn IN OP fd /\ fd NOTIN sockfds h.s /\
           e IN {ENOTSOCK; EBADF}) \/
        (?h ts tid d opn.
           (a0 = intr_1) /\ (a1 = slowfail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (opn,d))) /\
           (a3 = Lh_tau) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EINTR),dsched))) /\
           ((?v. opn = Sendto2 v) \/ (?v. opn = Recvfrom2 v) \/
            (?v. opn = Select2 v) \/ (?v. opn = Print2 v) \/
            (opn = Delay2) \/ (opn = Zombie))) \/
        (?h ts tid d e.
           (a0 = badmem_1) /\ (a1 = badfail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,socket ())) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
           e IN {ENOMEM; ENOBUFS}) \/
        (?FC ifds tid d s opn e.
           (a0 = badmem_2) /\ (a1 = badfail) /\
           (a2 = FC (ifds,tid,Timed (Run,d),s)) /\
           (a3 = Lh_call (tid,opn)) /\
           (a4 = FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
           F_context FC /\ opn IN OP s.fd /\ e IN {ENOMEM; ENOBUFS}) \/
        (?FC ifds tid t d s e.
           (a0 = badmem_3) /\ (a1 = badfail) /\
           (a2 = FC (ifds,tid,Timed (t,d),s)) /\ (a3 = Lh_tau) /\
           (a4 = FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
           F_context FC /\ t IN OP2 s.fd /\ e IN {ENOMEM; ENOBUFS}) \/
        (?h ts tid d v e.
           (a0 = badmem_4) /\ (a1 = badfail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Select2 v,d))) /\
           (a3 = Lh_tau) /\
           (a4 =
            h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
           e IN {ENOMEM; ENOBUFS}) \/
        (?h ts tid d.
           (a0 = exit_1) /\ (a1 = exit) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,exit ())) /\
           (a4 = h with ts := FUPDATE ts (tid,Timed (Exit,dsched))) /\
           T) \/
        (?h ts tid d.
           (a0 = exit_2) /\ (a1 = exit) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Exit,d))) /\
           (a3 = Lh_exit) /\ (a4 = h with <|ts := FEMPTY; s := []|>) /\
           T) \/
        (?h ts tid d v.
           (a0 = ret_1) /\ (a1 = misc) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Ret v,d))) /\
           (a3 = Lh_return (tid,v)) /\
           (a4 = h with ts := FUPDATE ts (tid,Timed (Run,time_infty))) /\
           T) \/
        (?h ts tid d tid'.
           (a0 = create_1) /\ (a1 = succeed) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,create ())) /\
           (a4 =
            h with
            ts :=
              FUPDATE (FUPDATE ts (tid,Timed (Ret (OK tid'),dsched)))
                (tid',Timed (Run,time_infty))) /\
           tid' NOTIN {tid} UNION FDOM ts) \/
        (?h ts tid d.
           (a0 = create_2) /\ (a1 = badfail) /\
           (a2 = h with ts := FUPDATE ts (tid,Timed (Run,d))) /\
           (a3 = Lh_call (tid,create ())) /\
           (a4 =
            h with
            ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched))) /\
           T) \/
        (?body i1 i2 oq' oqf'.
           (a0 = delivery_out_1) /\ (a1 = misc) /\
           (a3 = Lh_sendmsg (IP (i1,i2,body))) /\
           (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
           (IP (i1,i2,body),oq',oqf') IN dequeue (a2.oq,a2.oqf) /\
           i2 NOTIN LOOPBACK UNION MARTIAN /\ i1 NOTIN MARTIAN) \/
        (?oq' oqf'.
           (a0 = delivery_out_martian) /\ (a1 = misc) /\ (a3 = Lh_tau) /\
           (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
           ?i1 i2 body.
             (IP (i1,i2,body),oq',oqf') IN dequeue (a2.oq,a2.oqf) /\
             i2 IN MARTIAN) \/
        (?h SC s i3 i4 ifd ps3 ps4 data.
           (a0 = delivery_in_udp_1) /\ (a1 = misc) /\
           (a2 = h with s := SC s) /\
           (a3 = Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data)))) /\
           (a4 =
            h with
            s :=
              SC
                (s with
                 mq :=
                   APPEND s.mq
                     [(IP (i3,i4,UDP (ps3,ps4,data)),ifd.ifid)])) /\
           socklist_context SC /\ s IN lookup (SC s) (i3,ps3,i4,ps4) /\
           ifd IN h.ifds /\ i4 IN ifd.ipset /\ i4 NOTIN LOOPBACK /\
           i3 NOTIN MARTIAN UNION LOOPBACK) \/
        (?i3 i4 oq' oqf' ps3 ps4 data ok.
           (a0 = delivery_in_udp_2) /\ (a1 = misc) /\
           (a3 = Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data)))) /\
           (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\ i4 IN a2.ifds /\
           (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
           (oq',oqf',ok) IN
           {(a2.oq,a2.oqf,T)} UNION
           enqueue
             (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),a2.oq,a2.oqf) /\
           i4 NOTIN LOOPBACK /\ i3 NOTIN MARTIAN UNION LOOPBACK) \/
        (?i3 i4 body.
           (a0 = delivery_in_martian_3) /\ (a1 = misc) /\
           (a3 = Lh_recvmsg (IP (i3,i4,body))) /\ (a4 = a2) /\
           i4 IN a2.ifds /\ i4 NOTIN LOOPBACK /\
           (loopback (IP (i3,i4,body)) \/ martian (IP (i3,i4,body)))) \/
        (?h s SC es' i3' i4' i3 ps3 i4 ps4 body.
           (a0 = delivery_in_icmp_1) /\ (a1 = misc) /\
           (a2 = h with s := SC s) /\
           (a3 = Lh_recvmsg (IP (i4',i3',body))) /\
           (a4 = h with s := SC (s with es := es')) /\
           socklist_context SC /\
           ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
            (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
           s IN lookup (SC s) (i3,ps3,i4,ps4) /\ i3' IN h.ifds /\
           ~(loopback (IP (i4',i3',body)) \/
             martian (IP (i4',i3',body))) /\
           (es' =
            (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
               SOME ECONNREFUSED
             else
               s.es))) \/
        (?i3' i4' i3 ps3 i4 ps4 body.
           (a0 = delivery_in_icmp_2) /\ (a1 = misc) /\
           (a3 = Lh_recvmsg (IP (i4',i3',body))) /\ (a4 = a2) /\
           i3' IN a2.ifds /\
           ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
            (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
           (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
           ~(loopback (IP (i4',i3',body)) \/
             martian (IP (i4',i3',body)))) \/
        (?h i3 i4 SC s ifid oq' oqf' ps3 ps4 data.
           (a0 = delivery_loopback_udp_1) /\ (a1 = misc) /\
           (a2 = h with s := SC s) /\ (a3 = Lh_tau) /\
           (a4 =
            h with
            <|s :=
                SC
                  (s with
                   mq :=
                     APPEND s.mq [(IP (i3,i4,UDP (ps3,ps4,data)),ifid)]);
              oq := oq'; oqf := oqf'|>) /\ socklist_context SC /\
           (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
           s IN lookup (SC s) (i3,ps3,i4,ps4) /\
           <|ifid := ifid; ipset := LOOPBACK; primary := localhost;
             netmask := NETMASK (255 * 2 ** 24)|> IN h.ifds) \/
        (?i3 i4 oq' oq'' oqf' oqf'' ps3 ps4 data ok.
           (a0 = delivery_loopback_udp_2) /\ (a1 = misc) /\
           (a3 = Lh_tau) /\ (a4 = a2 with <|oq := oq''; oqf := oqf''|>) /\
           (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
           dequeue (a2.oq,a2.oqf) /\ i4 IN LOOPBACK /\
           (lookup a2.s (i3,ps3,i4,ps4) = {}) /\
           (oq'',oqf'',ok) IN
           enqueue
             (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf')) \/
        (?h SC s es' oq' oqf' i3' i4' i3 ps3 i4 ps4.
           (a0 = delivery_loopback_icmp_1) /\ (a1 = misc) /\
           (a2 = h with s := SC s) /\ (a3 = Lh_tau) /\
           (a4 =
            h with
            <|s := SC (s with es := es'); oq := oq'; oqf := oqf'|>) /\
           socklist_context SC /\
           (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
           s IN lookup (SC s) (i4,ps4,i3,ps3) /\
           (es' =
            (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
               SOME ECONNREFUSED
             else
               s.es))) \/
        (?i3' i4' oq' oqf' i3 ps3 i4 ps4.
           (a0 = delivery_loopback_icmp_2) /\ (a1 = misc) /\
           (a3 = Lh_tau) /\ (a4 = a2 with <|oq := oq'; oqf := oqf'|>) /\
           (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
           dequeue (a2.oq,a2.oqf) /\ i3' IN LOOPBACK /\
           (lookup a2.s (i4,ps4,i3,ps3) = {})) \/
        ?d.
          (a0 = epsilon_1) /\ (a1 = misc) /\ (a3 = Lh_epsilon d) /\
          d > 0 /\ (Time_Pass d a2 = SOME a4)
   
   [host_redn_ind]
   Theorem
   |- !host_redn'.
        (!h ts tid d fd.
           fd NOTIN sockfds h.s ==>
           host_redn' socket_1 succeed
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,socket ()))
             (h with
              <|ts := FUPDATE ts (tid,Timed (Ret (OK fd),dsched));
                s :=
                  Sock (fd,NONE,NONE,NONE,NONE,NONE,Flags (F,F),[])::
                      h.s|>)) /\
        (!h ts tid d e.
           e IN {EMFILE; ENFILE} ==>
           host_redn' socket_2 badfail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,socket ()))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched)))) /\
        (!FC tid d p1' ifds fd es f mq.
           F_context FC /\ p1' IN unused FC INTER ephemeral ==>
           host_redn' bind_1 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,bind (fd,NONE,NONE)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,NONE,SOME p1',NONE,NONE,es,f,mq)))) /\
        (!FC tid d p1' ifds fd i es f mq.
           F_context FC /\ i IN ifds /\
           p1' IN unused FC INTER ephemeral ==>
           host_redn' bind_2 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,bind (fd,SOME i,NONE)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,SOME i,SOME p1',NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds fd es f mq p.
           F_context FC /\ p NOTIN privileged /\
           (!s.
              s IN FC /\ (s.ps1 = SOME p) ==>
              f.reuseaddr /\ s.f.reuseaddr) ==>
           host_redn' bind_3 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,bind (fd,NONE,SOME p)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,NONE,SOME p,NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds fd es f mq i p.
           F_context FC /\ i IN ifds /\ p NOTIN privileged /\
           (!s.
              s IN FC ==>
              (s.ps1 = SOME p) /\ ((s.is1 = NONE) \/ (s.is1 = SOME i)) ==>
              f.reuseaddr /\ s.f.reuseaddr) ==>
           host_redn' bind_4 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,bind (fd,SOME i,SOME p)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,SOME i,SOME p,NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds s fd is p.
           F_context FC /\ p IN privileged ==>
           host_redn' bind_5 fail
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,bind (fd,is,SOME p)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EACCES),dsched),
                 s with fd := fd))) /\
        (!FC tid d ifds s fd is p.
           F_context FC /\
           ~(!s'.
               s' IN FC ==>
               (s'.ps1 = SOME p) /\
               ((s'.is1 = NONE) \/ (is = NONE) \/ (is = s'.is1)) ==>
               s.f.reuseaddr /\ s'.f.reuseaddr) ==>
           host_redn' bind_6 fail
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,bind (fd,is,SOME p)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EADDRINUSE),dsched),
                 s with fd := fd))) /\
        (!FC tid d ifds s fd i ps.
           F_context FC /\ i NOTIN ifds ==>
           host_redn' bind_7 fail
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,bind (fd,SOME i,ps)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EADDRNOTAVAIL),dsched),
                 s with fd := fd))) /\
        (!FC tid d ifds s fd p1 is ps.
           F_context FC ==>
           host_redn' bind_8 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 s with <|fd := fd; ps1 := SOME p1|>))
             (Lh_call (tid,bind (fd,is,ps)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EINVAL),dsched),
                 s with <|fd := fd; ps1 := SOME p1|>))) /\
        (!FC tid d ifds fd es f mq is e.
           F_context FC /\ (unused FC INTER ephemeral = {}) /\
           e IN ephemeralErrors ==>
           host_redn' bind_9 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,bind (fd,is,NONE)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds fd ps1 i1 p1' es f mq i ps.
           F_context FC /\ i1 IN outroute (ifds,i) /\
           p1' IN autobind (ps1,FC) ==>
           host_redn' connect_1 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,ps1,NONE,NONE,es,f,mq)))
             (Lh_call (tid,connect (fd,i,ps)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,SOME i1,SOME p1',SOME i,ps,es,f,mq)))) /\
        (!FC tid d ifds fd i1 p1 is2 ps2 es f mq i ps.
           F_context FC ==>
           host_redn' connect_2 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,SOME i1,SOME p1,is2,ps2,es,f,mq)))
             (Lh_call (tid,connect (fd,i,ps)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,SOME i1,SOME p1,SOME i,ps,es,f,mq)))) /\
        (!FC tid d ifds fd es f mq i ps s e.
           F_context FC /\ (unused FC INTER ephemeral = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
           host_redn' connect_3 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,connect (fd,i,ps)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd))) /\
        (!FC tid d ifds fd is1 p1 is2 ps2 es f mq.
           F_context FC ==>
           host_redn' disconnect_1 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,is1,SOME p1,is2,ps2,es,f,mq)))
             (Lh_call (tid,disconnect fd))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds fd es f mq p1.
           F_context FC /\ p1 IN unused FC INTER ephemeral ==>
           host_redn' disconnect_2 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,disconnect fd))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq)))) /\
        (!FC tid d ifds fd es f mq e s.
           F_context FC /\ (unused FC INTER ephemeral = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
           host_redn' disconnect_3 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,es,f,mq)))
             (Lh_call (tid,disconnect fd))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd))) /\
        (!FC tid d ifds s fd.
           F_context FC ==>
           host_redn' getsockname_1 succeed
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,getsockname fd))
             (FC
                (ifds,tid,Timed (Ret (OK (s.is1,s.ps1)),dsched),
                 s with fd := fd))) /\
        (!FC tid d ifds s fd.
           F_context FC ==>
           host_redn' getpeername_1 succeed
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,getpeername fd))
             (FC
                (ifds,tid,Timed (Ret (OK (s.is2,s.ps2)),dsched),
                 s with fd := fd))) /\
        (!FC tid d ifds s fd.
           F_context FC ==>
           host_redn' geterr_1 succeed
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,geterr fd))
             (FC
                (ifds,tid,Timed (Ret (OK s.es),dsched),
                 s with <|fd := fd; es := NONE|>))) /\
        (!FC tid d ifds s fd opt b.
           F_context FC /\
           ((opt = SO_BSDCOMPAT) ==> (b = s.f.bsdcompat)) /\
           ((opt = SO_REUSEADDR) ==> (b = s.f.reuseaddr)) ==>
           host_redn' getsockopt_1 succeed
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,getsockopt (fd,opt)))
             (FC (ifds,tid,Timed (Ret (OK b),dsched),s with fd := fd))) /\
        (!FC tid d ifds s fd opt b f'.
           F_context FC /\
           ((opt = SO_BSDCOMPAT) ==> (f' = s.f with bsdcompat := b)) /\
           ((opt = SO_REUSEADDR) ==> (f' = s.f with reuseaddr := b)) ==>
           host_redn' setsockopt_1 succeed
             (FC (ifds,tid,Timed (Run,d),s with fd := fd))
             (Lh_call (tid,setsockopt (fd,opt,b)))
             (FC
                (ifds,tid,Timed (Ret (OK ()),dsched),
                 s with <|fd := fd; f := f'|>))) /\
        (!SC h ts tid d s ips data nb oq' oqf' p1'.
           socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',T) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           string_size data <= UDPpayloadMax /\
           ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
           host_redn' sendto_1 succeed
             (h with
              <|ts := FUPDATE ts (tid,Timed (Run,d));
                s := SC (s with es := NONE)|>)
             (Lh_call (tid,sendto (s.fd,ips,data,nb)))
             (h with
              <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                oq := oq'; oqf := oqf'|>)) /\
        (!SC h ts tid d s ips data p1' oq' oqf'.
           socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',F) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
           host_redn' sendto_2 enter2
             (h with
              <|ts := FUPDATE ts (tid,Timed (Run,d));
                s := SC (s with es := NONE)|>)
             (Lh_call (tid,sendto (s.fd,ips,data,F)))
             (h with
              <|ts :=
                  FUPDATE ts
                    (tid,
                     Timed
                       (Sendto2 (s.fd,ips,s.is1,SOME p1',s.is2,s.ps2,data),
                        time_infty));
                s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                oq := oq'; oqf := oqf'|>)) /\
        (!SC h ts tid d s ips data p1' oq' oqf'.
           socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
           (oq',oqf',F) IN
           dosend
             (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
           ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
           host_redn' sendto_3 fail
             (h with
              <|ts := FUPDATE ts (tid,Timed (Run,d));
                s := SC (s with es := NONE)|>)
             (Lh_call (tid,sendto (s.fd,ips,data,T)))
             (h with
              <|ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched));
                s := SC (s with <|es := NONE; ps1 := SOME p1'|>);
                oq := oq'; oqf := oqf'|>)) /\
        (!FC tid d ifds fd is1 ps1 f mq data nb p1'.
           F_context FC /\ p1' IN autobind (ps1,FC) ==>
           host_redn' sendto_4 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,is1,ps1,NONE,NONE,NONE,f,mq)))
             (Lh_call (tid,sendto (fd,NONE,data,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL ENOTCONN),dsched),
                 Sock (fd,is1,SOME p1',NONE,NONE,NONE,f,mq)))) /\
        (!FC tid d ifds s p1 e ips data nb.
           F_context FC ==>
           host_redn' sendto_5 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 s with <|ps1 := SOME p1; es := SOME e|>))
             (Lh_call (tid,sendto (s.fd,ips,data,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),
                 s with <|ps1 := SOME p1; es := NONE|>))) /\
        (!FC tid d ifds s ips data nb ps1'.
           F_context FC /\ string_size data > UDPpayloadMax /\
           ps1' IN {s.ps1} UNION IMAGE SOME (autobind (s.ps1,FC)) ==>
           host_redn' sendto_6 fail (FC (ifds,tid,Timed (Run,d),s))
             (Lh_call (tid,sendto (s.fd,ips,data,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EMSGSIZE),dsched),
                 s with ps1 := ps1'))) /\
        (!FC tid d ifds fd ips data nb f mq e s.
           F_context FC /\ (autobind (NONE,FC) = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
           host_redn' sendto_7 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,NONE,f,mq)))
             (Lh_call (tid,sendto (fd,ips,data,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd))) /\
        (!SC h ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'.
           socklist_context SC /\
           ((oq',oqf',T) IN
            dosend
              (h.ifds,(ips,data),(s.is1,s.ps1,s.is2,s.ps2),h.oq,h.oqf) /\
            ((ips <> NONE) \/ (s.is2 <> NONE)) \/
            (oq',oqf',T) IN
            dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf) /\
            ((ips <> NONE) \/ (is2 <> NONE))) /\
           string_size data <= UDPpayloadMax ==>
           host_redn' sendto_8 slowsucceed
             (h with
              <|ts :=
                  FUPDATE ts
                    (tid,
                     Timed (Sendto2 (s.fd,ips,is1,ps1,is2,ps2,data),d));
                s := SC (s with es := NONE)|>) Lh_tau
             (h with
              <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                s := SC (s with es := NONE); oq := oq'; oqf := oqf'|>)) /\
        (!FC tid d ifds s ips data e.
           F_context FC ==>
           host_redn' sendto_9 slowfail
             (FC
                (ifds,tid,Timed (Sendto2 (s.fd,ips,data),d),
                 s with es := SOME e)) Lh_tau
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),
                 s with es := NONE))) /\
        (!h ts tid d fd ips is1 ps1 is2 ps2 e data SC s.
           socklist_context SC /\
           (?oq' oqf'.
              (oq',oqf',T) IN
              dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
           (string_size data > UDPpayloadMax /\ (e = EMSGSIZE) \/
            (s.is2 = NONE) /\ (ips = NONE) /\ (e = ENOTCONN)) ==>
           host_redn' sendto_10 slowfail
             (h with
              <|ts :=
                  FUPDATE ts
                    (tid,Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d));
                s := SC (s with es := NONE)|>) Lh_tau
             (h with
              <|ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched));
                s := SC (s with es := NONE)|>)) /\
        (!FC tid d ifds s i3 i4 ifid mq nb p1 ps3 ps4 data.
           F_context FC ==>
           host_redn' recvfrom_1 succeed
             (FC
                (ifds,tid,Timed (Run,d),
                 s with
                 <|ps1 := SOME p1; es := NONE;
                   mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>))
             (Lh_call (tid,recvfrom (s.fd,nb)))
             (FC
                (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
                 s with <|ps1 := SOME p1; es := NONE; mq := mq|>))) /\
        (!FC tid d ifds s p1'.
           F_context FC /\ p1' IN autobind (s.ps1,FC) ==>
           host_redn' recvfrom_2 enter2
             (FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>))
             (Lh_call (tid,recvfrom (s.fd,F)))
             (FC
                (ifds,tid,Timed (Recvfrom2 s.fd,time_infty),
                 s with <|es := NONE; mq := []; ps1 := SOME p1'|>))) /\
        (!FC tid d ifds s p1'.
           F_context FC /\ p1' IN autobind (s.ps1,FC) ==>
           host_redn' recvfrom_3 fail
             (FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>))
             (Lh_call (tid,recvfrom (s.fd,T)))
             (FC
                (ifds,tid,Timed (Ret (FAIL EAGAIN),dsched),
                 s with <|es := NONE; mq := []; ps1 := SOME p1'|>))) /\
        (!FC tid d ifds s p1 e nb.
           F_context FC ==>
           host_redn' recvfrom_4 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 s with <|ps1 := SOME p1; es := SOME e|>))
             (Lh_call (tid,recvfrom (s.fd,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),
                 s with <|ps1 := SOME p1; es := NONE|>))) /\
        (!FC tid d ifds fd nb f e s.
           F_context FC /\ (autobind (NONE,FC) = {}) /\
           e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
           host_redn' recvfrom_5 fail
             (FC
                (ifds,tid,Timed (Run,d),
                 Sock (fd,NONE,NONE,NONE,NONE,NONE,f,[])))
             (Lh_call (tid,recvfrom (fd,nb)))
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd))) /\
        (!FC tid d ifds s p1 mq i3 i4 ps3 ps4 data ifid.
           F_context FC ==>
           host_redn' recvfrom_6 slowsucceed
             (FC
                (ifds,tid,Timed (Recvfrom2 s.fd,d),
                 s with
                 <|ps1 := SOME p1; es := NONE;
                   mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>))
             Lh_tau
             (FC
                (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
                 s with <|ps1 := SOME p1; es := NONE; mq := mq|>))) /\
        (!FC tid d ifds s p1 e.
           F_context FC ==>
           host_redn' recvfrom_7 slowfail
             (FC
                (ifds,tid,Timed (Recvfrom2 s.fd,d),
                 s with <|ps1 := SOME p1; es := SOME e|>)) Lh_tau
             (FC
                (ifds,tid,Timed (Ret (FAIL e),dsched),
                 s with <|ps1 := SOME p1; es := NONE|>))) /\
        (!h ts tid d s1 s2 s.
           T ==>
           host_redn' close_1 succeed
             (h with
              <|ts := FUPDATE ts (tid,Timed (Run,d));
                s := APPEND s1 (s::s2)|>) (Lh_call (tid,close s.fd))
             (h with
              <|ts :=
                  zombify s.fd o_f
                  FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
                s := APPEND s1 s2|>)) /\
        (!h ts tid d d' readseq writeseq tms.
           LIST_TO_SET (APPEND readseq writeseq) SUBSET sockfds h.s /\
           (!i. (tms = SOME i) ==> 0 <= i) /\
           (d' =
            case tms of
               NONE -> time_infty
            || SOME v -> time (real_of_int v / 1000000)) ==>
           host_redn' select_1 enter2
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,select (readseq,writeseq,tms)))
             (h with
              ts :=
                FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d')))) /\
        (!h ts tid d readseq writeseq tm.
           tm < 0 ==>
           host_redn' select_2 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,select (readseq,writeseq,SOME tm)))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched)))) /\
        (!h ts tid d readseq readseq' writeseq writeseq'.
           (readseq' =
            FILTER
              (\fd.
                 ?s.
                   MEM s h.s /\ (s.fd = fd) /\
                   ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
           (writeseq' =
            FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
              writeseq) /\ ((readseq' <> []) \/ (writeseq' <> [])) ==>
           host_redn' select_3 slowsucceed
             (h with
              ts := FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d)))
             Lh_tau
             (h with
              ts :=
                FUPDATE ts
                  (tid,Timed (Ret (OK (readseq',writeseq')),dsched)))) /\
        (!h ts tid readseq readseq' writeseq writeseq'.
           (readseq' =
            FILTER
              (\fd.
                 ?s.
                   MEM s h.s /\ (s.fd = fd) /\
                   ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
           (writeseq' =
            FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
              writeseq) /\ (readseq' = []) /\ (writeseq' = []) ==>
           host_redn' select_4 slowsucceed
             (h with
              ts :=
                FUPDATE ts
                  (tid,Timed (Select2 (readseq,writeseq),time_zero)))
             Lh_tau
             (h with
              ts :=
                FUPDATE ts
                  (tid,Timed (Ret (OK (readseq',writeseq')),dsched)))) /\
        (!h ts tid d tm d'.
           tm >= 0 /\ (d' = time (real_of_int tm / 1000000)) ==>
           host_redn' delay_1 enter2
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,delay tm))
             (h with ts := FUPDATE ts (tid,Timed (Delay2,d')))) /\
        (!h ts tid d tm.
           tm < 0 ==>
           host_redn' delay_2 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,delay tm))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched)))) /\
        (!h ts tid.
           T ==>
           host_redn' delay_3 slowsucceed
             (h with ts := FUPDATE ts (tid,Timed (Delay2,time_zero)))
             Lh_tau
             (h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched)))) /\
        (!h ts tid d iflist ifset.
           iflist IN orderings ifset /\
           (ifset =
            {(hifd.ifid,hifd.primary,ipslist,hifd.netmask)
             |
             hifd IN h.ifds /\ ipslist IN orderings hifd.ipset}) ==>
           host_redn' getifaddrs_1 succeed
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,getifaddrs ()))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (OK iflist),dsched)))) /\
        (!h ts tid d v.
           T ==>
           host_redn' console_print_1 enter2
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,print_endline_flush v))
             (h with ts := FUPDATE ts (tid,Timed (Print2 v,dsched)))) /\
        (!h ts tid d v.
           T ==>
           host_redn' console_print_2 misc
             (h with ts := FUPDATE ts (tid,Timed (Print2 v,d)))
             (Lh_console v)
             (h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched)))) /\
        (!h ts tid d v.
           1 <= v /\ v <= 65535 ==>
           host_redn' convert_port_1 succeed
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,port_of_int v))
             (h with
              ts :=
                FUPDATE ts
                  (tid,Timed (Ret (OK (Port (Num v))),dsched)))) /\
        (!h ts tid d v.
           v < 1 \/ v > 65535 ==>
           host_redn' convert_port_2 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,port_of_int v))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched)))) /\
        (!h ts tid d v i.
           valid_ip_string v /\ (i = ipstr_to_ip v) ==>
           host_redn' convert_ip_1 succeed
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,ip_of_string v))
             (h with ts := FUPDATE ts (tid,Timed (Ret (OK i),dsched)))) /\
        (!h ts tid d v.
           ~valid_ip_string v ==>
           host_redn' convert_ip_2 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,ip_of_string v))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched)))) /\
        (!h ts tid d readseq writeseq tms.
           (?fd.
              MEM fd (APPEND readseq writeseq) /\ fd NOTIN sockfds h.s) ==>
           host_redn' notsockfd_1 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,select (readseq,writeseq,tms)))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EBADF),dsched)))) /\
        (!h ts tid d fd opn e.
           opn IN OP fd /\ fd NOTIN sockfds h.s /\
           e IN {ENOTSOCK; EBADF} ==>
           host_redn' notsockfd_2 fail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,opn))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched)))) /\
        (!h ts tid d opn.
           (?v. opn = Sendto2 v) \/ (?v. opn = Recvfrom2 v) \/
           (?v. opn = Select2 v) \/ (?v. opn = Print2 v) \/
           (opn = Delay2) \/ (opn = Zombie) ==>
           host_redn' intr_1 slowfail
             (h with ts := FUPDATE ts (tid,Timed (opn,d))) Lh_tau
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EINTR),dsched)))) /\
        (!h ts tid d e.
           e IN {ENOMEM; ENOBUFS} ==>
           host_redn' badmem_1 badfail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,socket ()))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched)))) /\
        (!FC ifds tid d s opn e.
           F_context FC /\ opn IN OP s.fd /\ e IN {ENOMEM; ENOBUFS} ==>
           host_redn' badmem_2 badfail (FC (ifds,tid,Timed (Run,d),s))
             (Lh_call (tid,opn))
             (FC (ifds,tid,Timed (Ret (FAIL e),dsched),s))) /\
        (!FC ifds tid t d s e.
           F_context FC /\ t IN OP2 s.fd /\ e IN {ENOMEM; ENOBUFS} ==>
           host_redn' badmem_3 badfail (FC (ifds,tid,Timed (t,d),s)) Lh_tau
             (FC (ifds,tid,Timed (Ret (FAIL e),dsched),s))) /\
        (!h ts tid d v e.
           e IN {ENOMEM; ENOBUFS} ==>
           host_redn' badmem_4 badfail
             (h with ts := FUPDATE ts (tid,Timed (Select2 v,d))) Lh_tau
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched)))) /\
        (!h ts tid d.
           T ==>
           host_redn' exit_1 exit
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,exit ()))
             (h with ts := FUPDATE ts (tid,Timed (Exit,dsched)))) /\
        (!h ts tid d.
           T ==>
           host_redn' exit_2 exit
             (h with ts := FUPDATE ts (tid,Timed (Exit,d))) Lh_exit
             (h with <|ts := FEMPTY; s := []|>)) /\
        (!h ts tid d v.
           T ==>
           host_redn' ret_1 misc
             (h with ts := FUPDATE ts (tid,Timed (Ret v,d)))
             (Lh_return (tid,v))
             (h with ts := FUPDATE ts (tid,Timed (Run,time_infty)))) /\
        (!h ts tid d tid'.
           tid' NOTIN {tid} UNION FDOM ts ==>
           host_redn' create_1 succeed
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,create ()))
             (h with
              ts :=
                FUPDATE (FUPDATE ts (tid,Timed (Ret (OK tid'),dsched)))
                  (tid',Timed (Run,time_infty)))) /\
        (!h ts tid d.
           T ==>
           host_redn' create_2 badfail
             (h with ts := FUPDATE ts (tid,Timed (Run,d)))
             (Lh_call (tid,create ()))
             (h with
              ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched)))) /\
        (!body h i1 i2 oq' oqf'.
           (IP (i1,i2,body),oq',oqf') IN dequeue (h.oq,h.oqf) /\
           i2 NOTIN LOOPBACK UNION MARTIAN /\ i1 NOTIN MARTIAN ==>
           host_redn' delivery_out_1 misc h (Lh_sendmsg (IP (i1,i2,body)))
             (h with <|oq := oq'; oqf := oqf'|>)) /\
        (!h oq' oqf'.
           (?i1 i2 body.
              (IP (i1,i2,body),oq',oqf') IN dequeue (h.oq,h.oqf) /\
              i2 IN MARTIAN) ==>
           host_redn' delivery_out_martian misc h Lh_tau
             (h with <|oq := oq'; oqf := oqf'|>)) /\
        (!h SC s i3 i4 ifd ps3 ps4 data.
           socklist_context SC /\ s IN lookup (SC s) (i3,ps3,i4,ps4) /\
           ifd IN h.ifds /\ i4 IN ifd.ipset /\ i4 NOTIN LOOPBACK /\
           i3 NOTIN MARTIAN UNION LOOPBACK ==>
           host_redn' delivery_in_udp_1 misc (h with s := SC s)
             (Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data))))
             (h with
              s :=
                SC
                  (s with
                   mq :=
                     APPEND s.mq
                       [(IP (i3,i4,UDP (ps3,ps4,data)),ifd.ifid)]))) /\
        (!h i3 i4 oq' oqf' ps3 ps4 data ok.
           i4 IN h.ifds /\ (lookup h.s (i3,ps3,i4,ps4) = {}) /\
           (oq',oqf',ok) IN
           {(h.oq,h.oqf,T)} UNION
           enqueue
             (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),h.oq,h.oqf) /\
           i4 NOTIN LOOPBACK /\ i3 NOTIN MARTIAN UNION LOOPBACK ==>
           host_redn' delivery_in_udp_2 misc h
             (Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data))))
             (h with <|oq := oq'; oqf := oqf'|>)) /\
        (!h i3 i4 body.
           i4 IN h.ifds /\ i4 NOTIN LOOPBACK /\
           (loopback (IP (i3,i4,body)) \/ martian (IP (i3,i4,body))) ==>
           host_redn' delivery_in_martian_3 misc h
             (Lh_recvmsg (IP (i3,i4,body))) h) /\
        (!h s SC es' i3' i4' i3 ps3 i4 ps4 body.
           socklist_context SC /\
           ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
            (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
           s IN lookup (SC s) (i3,ps3,i4,ps4) /\ i3' IN h.ifds /\
           ~(loopback (IP (i4',i3',body)) \/
             martian (IP (i4',i3',body))) /\
           (es' =
            (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
               SOME ECONNREFUSED
             else
               s.es)) ==>
           host_redn' delivery_in_icmp_1 misc (h with s := SC s)
             (Lh_recvmsg (IP (i4',i3',body)))
             (h with s := SC (s with es := es'))) /\
        (!h i3' i4' i3 ps3 i4 ps4 body.
           i3' IN h.ifds /\
           ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
            (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
           (lookup h.s (i3,ps3,i4,ps4) = {}) /\
           ~(loopback (IP (i4',i3',body)) \/
             martian (IP (i4',i3',body))) ==>
           host_redn' delivery_in_icmp_2 misc h
             (Lh_recvmsg (IP (i4',i3',body))) h) /\
        (!h i3 i4 SC s ifid oq' oqf' ps3 ps4 data.
           socklist_context SC /\
           (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
           s IN lookup (SC s) (i3,ps3,i4,ps4) /\
           <|ifid := ifid; ipset := LOOPBACK; primary := localhost;
             netmask := NETMASK (255 * 2 ** 24)|> IN h.ifds ==>
           host_redn' delivery_loopback_udp_1 misc (h with s := SC s)
             Lh_tau
             (h with
              <|s :=
                  SC
                    (s with
                     mq :=
                       APPEND s.mq [(IP (i3,i4,UDP (ps3,ps4,data)),ifid)]);
                oq := oq'; oqf := oqf'|>)) /\
        (!h i3 i4 oq' oq'' oqf' oqf'' ps3 ps4 data ok.
           (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
           (lookup h.s (i3,ps3,i4,ps4) = {}) /\
           (oq'',oqf'',ok) IN
           enqueue
             (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') ==>
           host_redn' delivery_loopback_udp_2 misc h Lh_tau
             (h with <|oq := oq''; oqf := oqf''|>)) /\
        (!h SC s es' oq' oqf' i3' i4' i3 ps3 i4 ps4.
           socklist_context SC /\
           (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
           s IN lookup (SC s) (i4,ps4,i3,ps3) /\
           (es' =
            (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
               SOME ECONNREFUSED
             else
               s.es)) ==>
           host_redn' delivery_loopback_icmp_1 misc (h with s := SC s)
             Lh_tau
             (h with
              <|s := SC (s with es := es'); oq := oq'; oqf := oqf'|>)) /\
        (!h i3' i4' oq' oqf' i3 ps3 i4 ps4.
           (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
           dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
           (lookup h.s (i4,ps4,i3,ps3) = {}) ==>
           host_redn' delivery_loopback_icmp_2 misc h Lh_tau
             (h with <|oq := oq'; oqf := oqf'|>)) /\
        (!h h' d.
           d > 0 /\ (Time_Pass d h = SOME h') ==>
           host_redn' epsilon_1 misc h (Lh_epsilon d) h') ==>
        !a0 a1 a2 a3 a4.
          a0 /* a1 */ a2 -- a3 --> a4 ==> host_redn' a0 a1 a2 a3 a4
   
   [host_redn_rules]
   Theorem
   |- (!h ts tid d fd.
         fd NOTIN sockfds h.s ==>
         socket_1 /* succeed */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,socket ()) -->
         h with
         <|ts := FUPDATE ts (tid,Timed (Ret (OK fd),dsched));
           s :=
             Sock (fd,NONE,NONE,NONE,NONE,NONE,Flags (F,F),[])::h.s|>) /\
      (!h ts tid d e.
         e IN {EMFILE; ENFILE} ==>
         socket_2 /* badfail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,socket ()) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
      (!FC tid d p1' ifds fd es f mq.
         F_context FC /\ p1' IN unused FC INTER ephemeral ==>
         bind_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,bind (fd,NONE,NONE)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,NONE,SOME p1',NONE,NONE,es,f,mq))) /\
      (!FC tid d p1' ifds fd i es f mq.
         F_context FC /\ i IN ifds /\ p1' IN unused FC INTER ephemeral ==>
         bind_2 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,bind (fd,SOME i,NONE)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,SOME i,SOME p1',NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds fd es f mq p.
         F_context FC /\ p NOTIN privileged /\
         (!s.
            s IN FC /\ (s.ps1 = SOME p) ==>
            f.reuseaddr /\ s.f.reuseaddr) ==>
         bind_3 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,bind (fd,NONE,SOME p)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,NONE,SOME p,NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds fd es f mq i p.
         F_context FC /\ i IN ifds /\ p NOTIN privileged /\
         (!s.
            s IN FC ==>
            (s.ps1 = SOME p) /\ ((s.is1 = NONE) \/ (s.is1 = SOME i)) ==>
            f.reuseaddr /\ s.f.reuseaddr) ==>
         bind_4 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,bind (fd,SOME i,SOME p)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,SOME i,SOME p,NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds s fd is p.
         F_context FC /\ p IN privileged ==>
         bind_5 /* fail */ FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,bind (fd,is,SOME p)) -->
         FC (ifds,tid,Timed (Ret (FAIL EACCES),dsched),s with fd := fd)) /\
      (!FC tid d ifds s fd is p.
         F_context FC /\
         ~(!s'.
             s' IN FC ==>
             (s'.ps1 = SOME p) /\
             ((s'.is1 = NONE) \/ (is = NONE) \/ (is = s'.is1)) ==>
             s.f.reuseaddr /\ s'.f.reuseaddr) ==>
         bind_6 /* fail */ FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,bind (fd,is,SOME p)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL EADDRINUSE),dsched),
            s with fd := fd)) /\
      (!FC tid d ifds s fd i ps.
         F_context FC /\ i NOTIN ifds ==>
         bind_7 /* fail */ FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,bind (fd,SOME i,ps)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL EADDRNOTAVAIL),dsched),
            s with fd := fd)) /\
      (!FC tid d ifds s fd p1 is ps.
         F_context FC ==>
         bind_8 /* fail */
         FC (ifds,tid,Timed (Run,d),s with <|fd := fd; ps1 := SOME p1|>)
           -- Lh_call (tid,bind (fd,is,ps)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL EINVAL),dsched),
            s with <|fd := fd; ps1 := SOME p1|>)) /\
      (!FC tid d ifds fd es f mq is e.
         F_context FC /\ (unused FC INTER ephemeral = {}) /\
         e IN ephemeralErrors ==>
         bind_9 /* fail */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,bind (fd,is,NONE)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL e),dsched),
            Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds fd ps1 i1 p1' es f mq i ps.
         F_context FC /\ i1 IN outroute (ifds,i) /\
         p1' IN autobind (ps1,FC) ==>
         connect_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,ps1,NONE,NONE,es,f,mq))
           -- Lh_call (tid,connect (fd,i,ps)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,SOME i1,SOME p1',SOME i,ps,es,f,mq))) /\
      (!FC tid d ifds fd i1 p1 is2 ps2 es f mq i ps.
         F_context FC ==>
         connect_2 /* succeed */
         FC
           (ifds,tid,Timed (Run,d),
            Sock (fd,SOME i1,SOME p1,is2,ps2,es,f,mq))
           -- Lh_call (tid,connect (fd,i,ps)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,SOME i1,SOME p1,SOME i,ps,es,f,mq))) /\
      (!FC tid d ifds fd es f mq i ps s e.
         F_context FC /\ (unused FC INTER ephemeral = {}) /\
         e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
         connect_3 /* fail */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,connect (fd,i,ps)) -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
      (!FC tid d ifds fd is1 p1 is2 ps2 es f mq.
         F_context FC ==>
         disconnect_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,is1,SOME p1,is2,ps2,es,f,mq))
           -- Lh_call (tid,disconnect fd) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds fd es f mq p1.
         F_context FC /\ p1 IN unused FC INTER ephemeral ==>
         disconnect_2 /* succeed */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,disconnect fd) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            Sock (fd,NONE,SOME p1,NONE,NONE,es,f,mq))) /\
      (!FC tid d ifds fd es f mq e s.
         F_context FC /\ (unused FC INTER ephemeral = {}) /\
         e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
         disconnect_3 /* fail */
         FC (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,es,f,mq))
           -- Lh_call (tid,disconnect fd) -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
      (!FC tid d ifds s fd.
         F_context FC ==>
         getsockname_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,getsockname fd) -->
         FC
           (ifds,tid,Timed (Ret (OK (s.is1,s.ps1)),dsched),
            s with fd := fd)) /\
      (!FC tid d ifds s fd.
         F_context FC ==>
         getpeername_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,getpeername fd) -->
         FC
           (ifds,tid,Timed (Ret (OK (s.is2,s.ps2)),dsched),
            s with fd := fd)) /\
      (!FC tid d ifds s fd.
         F_context FC ==>
         geterr_1 /* succeed */ FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,geterr fd) -->
         FC
           (ifds,tid,Timed (Ret (OK s.es),dsched),
            s with <|fd := fd; es := NONE|>)) /\
      (!FC tid d ifds s fd opt b.
         F_context FC /\ ((opt = SO_BSDCOMPAT) ==> (b = s.f.bsdcompat)) /\
         ((opt = SO_REUSEADDR) ==> (b = s.f.reuseaddr)) ==>
         getsockopt_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,getsockopt (fd,opt)) -->
         FC (ifds,tid,Timed (Ret (OK b),dsched),s with fd := fd)) /\
      (!FC tid d ifds s fd opt b f'.
         F_context FC /\
         ((opt = SO_BSDCOMPAT) ==> (f' = s.f with bsdcompat := b)) /\
         ((opt = SO_REUSEADDR) ==> (f' = s.f with reuseaddr := b)) ==>
         setsockopt_1 /* succeed */
         FC (ifds,tid,Timed (Run,d),s with fd := fd)
           -- Lh_call (tid,setsockopt (fd,opt,b)) -->
         FC
           (ifds,tid,Timed (Ret (OK ()),dsched),
            s with <|fd := fd; f := f'|>)) /\
      (!SC h ts tid d s ips data nb oq' oqf' p1'.
         socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
         (oq',oqf',T) IN
         dosend
           (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
         string_size data <= UDPpayloadMax /\
         ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
         sendto_1 /* succeed */
         h with
         <|ts := FUPDATE ts (tid,Timed (Run,d));
           s := SC (s with es := NONE)|>
           -- Lh_call (tid,sendto (s.fd,ips,data,nb)) -->
         h with
         <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
           s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
           oqf := oqf'|>) /\
      (!SC h ts tid d s ips data p1' oq' oqf'.
         socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
         (oq',oqf',F) IN
         dosend
           (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
         ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
         sendto_2 /* enter2 */
         h with
         <|ts := FUPDATE ts (tid,Timed (Run,d));
           s := SC (s with es := NONE)|>
           -- Lh_call (tid,sendto (s.fd,ips,data,F)) -->
         h with
         <|ts :=
             FUPDATE ts
               (tid,
                Timed
                  (Sendto2 (s.fd,ips,s.is1,SOME p1',s.is2,s.ps2,data),
                   time_infty));
           s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
           oqf := oqf'|>) /\
      (!SC h ts tid d s ips data p1' oq' oqf'.
         socklist_context SC /\ p1' IN autobind (s.ps1,SC) /\
         (oq',oqf',F) IN
         dosend
           (h.ifds,(ips,data),(s.is1,SOME p1',s.is2,s.ps2),h.oq,h.oqf) /\
         ((ips <> NONE) \/ (s.is2 <> NONE)) ==>
         sendto_3 /* fail */
         h with
         <|ts := FUPDATE ts (tid,Timed (Run,d));
           s := SC (s with es := NONE)|>
           -- Lh_call (tid,sendto (s.fd,ips,data,T)) -->
         h with
         <|ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched));
           s := SC (s with <|es := NONE; ps1 := SOME p1'|>); oq := oq';
           oqf := oqf'|>) /\
      (!FC tid d ifds fd is1 ps1 f mq data nb p1'.
         F_context FC /\ p1' IN autobind (ps1,FC) ==>
         sendto_4 /* fail */
         FC (ifds,tid,Timed (Run,d),Sock (fd,is1,ps1,NONE,NONE,NONE,f,mq))
           -- Lh_call (tid,sendto (fd,NONE,data,nb)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL ENOTCONN),dsched),
            Sock (fd,is1,SOME p1',NONE,NONE,NONE,f,mq))) /\
      (!FC tid d ifds s p1 e ips data nb.
         F_context FC ==>
         sendto_5 /* fail */
         FC
           (ifds,tid,Timed (Run,d),s with <|ps1 := SOME p1; es := SOME e|>)
           -- Lh_call (tid,sendto (s.fd,ips,data,nb)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL e),dsched),
            s with <|ps1 := SOME p1; es := NONE|>)) /\
      (!FC tid d ifds s ips data nb ps1'.
         F_context FC /\ string_size data > UDPpayloadMax /\
         ps1' IN {s.ps1} UNION IMAGE SOME (autobind (s.ps1,FC)) ==>
         sendto_6 /* fail */ FC (ifds,tid,Timed (Run,d),s)
           -- Lh_call (tid,sendto (s.fd,ips,data,nb)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL EMSGSIZE),dsched),
            s with ps1 := ps1')) /\
      (!FC tid d ifds fd ips data nb f mq e s.
         F_context FC /\ (autobind (NONE,FC) = {}) /\
         e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
         sendto_7 /* fail */
         FC
           (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,NONE,f,mq))
           -- Lh_call (tid,sendto (fd,ips,data,nb)) -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
      (!SC h ts tid d s ips is1 ps1 is2 ps2 data oq' oqf'.
         socklist_context SC /\
         ((oq',oqf',T) IN
          dosend
            (h.ifds,(ips,data),(s.is1,s.ps1,s.is2,s.ps2),h.oq,h.oqf) /\
          ((ips <> NONE) \/ (s.is2 <> NONE)) \/
          (oq',oqf',T) IN
          dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf) /\
          ((ips <> NONE) \/ (is2 <> NONE))) /\
         string_size data <= UDPpayloadMax ==>
         sendto_8 /* slowsucceed */
         h with
         <|ts :=
             FUPDATE ts
               (tid,Timed (Sendto2 (s.fd,ips,is1,ps1,is2,ps2,data),d));
           s := SC (s with es := NONE)|> -- Lh_tau -->
         h with
         <|ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
           s := SC (s with es := NONE); oq := oq'; oqf := oqf'|>) /\
      (!FC tid d ifds s ips data e.
         F_context FC ==>
         sendto_9 /* slowfail */
         FC
           (ifds,tid,Timed (Sendto2 (s.fd,ips,data),d),s with es := SOME e)
           -- Lh_tau -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with es := NONE)) /\
      (!h ts tid d fd ips is1 ps1 is2 ps2 e data SC s.
         socklist_context SC /\
         (?oq' oqf'.
            (oq',oqf',T) IN
            dosend (h.ifds,(ips,data),(is1,ps1,is2,ps2),h.oq,h.oqf)) /\
         (string_size data > UDPpayloadMax /\ (e = EMSGSIZE) \/
          (s.is2 = NONE) /\ (ips = NONE) /\ (e = ENOTCONN)) ==>
         sendto_10 /* slowfail */
         h with
         <|ts :=
             FUPDATE ts
               (tid,Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d));
           s := SC (s with es := NONE)|> -- Lh_tau -->
         h with
         <|ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched));
           s := SC (s with es := NONE)|>) /\
      (!FC tid d ifds s i3 i4 ifid mq nb p1 ps3 ps4 data.
         F_context FC ==>
         recvfrom_1 /* succeed */
         FC
           (ifds,tid,Timed (Run,d),
            s with
            <|ps1 := SOME p1; es := NONE;
              mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)
           -- Lh_call (tid,recvfrom (s.fd,nb)) -->
         FC
           (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
            s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
      (!FC tid d ifds s p1'.
         F_context FC /\ p1' IN autobind (s.ps1,FC) ==>
         recvfrom_2 /* enter2 */
         FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>)
           -- Lh_call (tid,recvfrom (s.fd,F)) -->
         FC
           (ifds,tid,Timed (Recvfrom2 s.fd,time_infty),
            s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
      (!FC tid d ifds s p1'.
         F_context FC /\ p1' IN autobind (s.ps1,FC) ==>
         recvfrom_3 /* fail */
         FC (ifds,tid,Timed (Run,d),s with <|es := NONE; mq := []|>)
           -- Lh_call (tid,recvfrom (s.fd,T)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL EAGAIN),dsched),
            s with <|es := NONE; mq := []; ps1 := SOME p1'|>)) /\
      (!FC tid d ifds s p1 e nb.
         F_context FC ==>
         recvfrom_4 /* fail */
         FC
           (ifds,tid,Timed (Run,d),s with <|ps1 := SOME p1; es := SOME e|>)
           -- Lh_call (tid,recvfrom (s.fd,nb)) -->
         FC
           (ifds,tid,Timed (Ret (FAIL e),dsched),
            s with <|ps1 := SOME p1; es := NONE|>)) /\
      (!FC tid d ifds fd nb f e s.
         F_context FC /\ (autobind (NONE,FC) = {}) /\
         e IN ephemeralErrors /\ socket_ok ifds (s with fd := fd) ==>
         recvfrom_5 /* fail */
         FC
           (ifds,tid,Timed (Run,d),Sock (fd,NONE,NONE,NONE,NONE,NONE,f,[]))
           -- Lh_call (tid,recvfrom (fd,nb)) -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s with fd := fd)) /\
      (!FC tid d ifds s p1 mq i3 i4 ps3 ps4 data ifid.
         F_context FC ==>
         recvfrom_6 /* slowsucceed */
         FC
           (ifds,tid,Timed (Recvfrom2 s.fd,d),
            s with
            <|ps1 := SOME p1; es := NONE;
              mq := (IP (i3,i4,UDP (ps3,ps4,data)),ifid)::mq|>)
           -- Lh_tau -->
         FC
           (ifds,tid,Timed (Ret (OK (i3,ps3,data)),dsched),
            s with <|ps1 := SOME p1; es := NONE; mq := mq|>)) /\
      (!FC tid d ifds s p1 e.
         F_context FC ==>
         recvfrom_7 /* slowfail */
         FC
           (ifds,tid,Timed (Recvfrom2 s.fd,d),
            s with <|ps1 := SOME p1; es := SOME e|>) -- Lh_tau -->
         FC
           (ifds,tid,Timed (Ret (FAIL e),dsched),
            s with <|ps1 := SOME p1; es := NONE|>)) /\
      (!h ts tid d s1 s2 s.
         T ==>
         close_1 /* succeed */
         h with
         <|ts := FUPDATE ts (tid,Timed (Run,d)); s := APPEND s1 (s::s2)|>
           -- Lh_call (tid,close s.fd) -->
         h with
         <|ts :=
             zombify s.fd o_f FUPDATE ts (tid,Timed (Ret (OK ()),dsched));
           s := APPEND s1 s2|>) /\
      (!h ts tid d d' readseq writeseq tms.
         LIST_TO_SET (APPEND readseq writeseq) SUBSET sockfds h.s /\
         (!i. (tms = SOME i) ==> 0 <= i) /\
         (d' =
          case tms of
             NONE -> time_infty
          || SOME v -> time (real_of_int v / 1000000)) ==>
         select_1 /* enter2 */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,select (readseq,writeseq,tms)) -->
         h with
         ts := FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d'))) /\
      (!h ts tid d readseq writeseq tm.
         tm < 0 ==>
         select_2 /* fail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,select (readseq,writeseq,SOME tm)) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
      (!h ts tid d readseq readseq' writeseq writeseq'.
         (readseq' =
          FILTER
            (\fd.
               ?s.
                 MEM s h.s /\ (s.fd = fd) /\
                 ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
         (writeseq' =
          FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
            writeseq) /\ ((readseq' <> []) \/ (writeseq' <> [])) ==>
         select_3 /* slowsucceed */
         h with ts := FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),d))
           -- Lh_tau -->
         h with
         ts :=
           FUPDATE ts
             (tid,Timed (Ret (OK (readseq',writeseq')),dsched))) /\
      (!h ts tid readseq readseq' writeseq writeseq'.
         (readseq' =
          FILTER
            (\fd.
               ?s.
                 MEM s h.s /\ (s.fd = fd) /\
                 ((s.mq <> []) \/ (s.es <> NONE))) readseq) /\
         (writeseq' =
          FILTER (\fd. ?s. MEM s h.s /\ (s.fd = fd) /\ (h.oqf = F))
            writeseq) /\ (readseq' = []) /\ (writeseq' = []) ==>
         select_4 /* slowsucceed */
         h with
         ts :=
           FUPDATE ts (tid,Timed (Select2 (readseq,writeseq),time_zero))
           -- Lh_tau -->
         h with
         ts :=
           FUPDATE ts
             (tid,Timed (Ret (OK (readseq',writeseq')),dsched))) /\
      (!h ts tid d tm d'.
         tm >= 0 /\ (d' = time (real_of_int tm / 1000000)) ==>
         delay_1 /* enter2 */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,delay tm) -->
         h with ts := FUPDATE ts (tid,Timed (Delay2,d'))) /\
      (!h ts tid d tm.
         tm < 0 ==>
         delay_2 /* fail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,delay tm) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
      (!h ts tid.
         T ==>
         delay_3 /* slowsucceed */
         h with ts := FUPDATE ts (tid,Timed (Delay2,time_zero))
           -- Lh_tau -->
         h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
      (!h ts tid d iflist ifset.
         iflist IN orderings ifset /\
         (ifset =
          {(hifd.ifid,hifd.primary,ipslist,hifd.netmask)
           |
           hifd IN h.ifds /\ ipslist IN orderings hifd.ipset}) ==>
         getifaddrs_1 /* succeed */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,getifaddrs ()) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (OK iflist),dsched))) /\
      (!h ts tid d v.
         T ==>
         console_print_1 /* enter2 */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,print_endline_flush v) -->
         h with ts := FUPDATE ts (tid,Timed (Print2 v,dsched))) /\
      (!h ts tid d v.
         T ==>
         console_print_2 /* misc */
         h with ts := FUPDATE ts (tid,Timed (Print2 v,d))
           -- Lh_console v -->
         h with ts := FUPDATE ts (tid,Timed (Ret (OK ()),dsched))) /\
      (!h ts tid d v.
         1 <= v /\ v <= 65535 ==>
         convert_port_1 /* succeed */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,port_of_int v) -->
         h with
         ts := FUPDATE ts (tid,Timed (Ret (OK (Port (Num v))),dsched))) /\
      (!h ts tid d v.
         v < 1 \/ v > 65535 ==>
         convert_port_2 /* fail */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,port_of_int v) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
      (!h ts tid d v i.
         valid_ip_string v /\ (i = ipstr_to_ip v) ==>
         convert_ip_1 /* succeed */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,ip_of_string v) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (OK i),dsched))) /\
      (!h ts tid d v.
         ~valid_ip_string v ==>
         convert_ip_2 /* fail */
         h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,ip_of_string v) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EINVAL),dsched))) /\
      (!h ts tid d readseq writeseq tms.
         (?fd.
            MEM fd (APPEND readseq writeseq) /\ fd NOTIN sockfds h.s) ==>
         notsockfd_1 /* fail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,select (readseq,writeseq,tms)) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EBADF),dsched))) /\
      (!h ts tid d fd opn e.
         opn IN OP fd /\ fd NOTIN sockfds h.s /\ e IN {ENOTSOCK; EBADF} ==>
         notsockfd_2 /* fail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,opn) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
      (!h ts tid d opn.
         (?v. opn = Sendto2 v) \/ (?v. opn = Recvfrom2 v) \/
         (?v. opn = Select2 v) \/ (?v. opn = Print2 v) \/ (opn = Delay2) \/
         (opn = Zombie) ==>
         intr_1 /* slowfail */ h with ts := FUPDATE ts (tid,Timed (opn,d))
           -- Lh_tau -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EINTR),dsched))) /\
      (!h ts tid d e.
         e IN {ENOMEM; ENOBUFS} ==>
         badmem_1 /* badfail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,socket ()) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
      (!FC ifds tid d s opn e.
         F_context FC /\ opn IN OP s.fd /\ e IN {ENOMEM; ENOBUFS} ==>
         badmem_2 /* badfail */ FC (ifds,tid,Timed (Run,d),s)
           -- Lh_call (tid,opn) -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
      (!FC ifds tid t d s e.
         F_context FC /\ t IN OP2 s.fd /\ e IN {ENOMEM; ENOBUFS} ==>
         badmem_3 /* badfail */ FC (ifds,tid,Timed (t,d),s) -- Lh_tau -->
         FC (ifds,tid,Timed (Ret (FAIL e),dsched),s)) /\
      (!h ts tid d v e.
         e IN {ENOMEM; ENOBUFS} ==>
         badmem_4 /* badfail */
         h with ts := FUPDATE ts (tid,Timed (Select2 v,d)) -- Lh_tau -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL e),dsched))) /\
      (!h ts tid d.
         T ==>
         exit_1 /* exit */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,exit ()) -->
         h with ts := FUPDATE ts (tid,Timed (Exit,dsched))) /\
      (!h ts tid d.
         T ==>
         exit_2 /* exit */ h with ts := FUPDATE ts (tid,Timed (Exit,d))
           -- Lh_exit --> h with <|ts := FEMPTY; s := []|>) /\
      (!h ts tid d v.
         T ==>
         ret_1 /* misc */ h with ts := FUPDATE ts (tid,Timed (Ret v,d))
           -- Lh_return (tid,v) -->
         h with ts := FUPDATE ts (tid,Timed (Run,time_infty))) /\
      (!h ts tid d tid'.
         tid' NOTIN {tid} UNION FDOM ts ==>
         create_1 /* succeed */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,create ()) -->
         h with
         ts :=
           FUPDATE (FUPDATE ts (tid,Timed (Ret (OK tid'),dsched)))
             (tid',Timed (Run,time_infty))) /\
      (!h ts tid d.
         T ==>
         create_2 /* badfail */ h with ts := FUPDATE ts (tid,Timed (Run,d))
           -- Lh_call (tid,create ()) -->
         h with ts := FUPDATE ts (tid,Timed (Ret (FAIL EAGAIN),dsched))) /\
      (!body h i1 i2 oq' oqf'.
         (IP (i1,i2,body),oq',oqf') IN dequeue (h.oq,h.oqf) /\
         i2 NOTIN LOOPBACK UNION MARTIAN /\ i1 NOTIN MARTIAN ==>
         delivery_out_1 /* misc */ h -- Lh_sendmsg (IP (i1,i2,body)) -->
         h with <|oq := oq'; oqf := oqf'|>) /\
      (!h oq' oqf'.
         (?i1 i2 body.
            (IP (i1,i2,body),oq',oqf') IN dequeue (h.oq,h.oqf) /\
            i2 IN MARTIAN) ==>
         delivery_out_martian /* misc */ h -- Lh_tau -->
         h with <|oq := oq'; oqf := oqf'|>) /\
      (!h SC s i3 i4 ifd ps3 ps4 data.
         socklist_context SC /\ s IN lookup (SC s) (i3,ps3,i4,ps4) /\
         ifd IN h.ifds /\ i4 IN ifd.ipset /\ i4 NOTIN LOOPBACK /\
         i3 NOTIN MARTIAN UNION LOOPBACK ==>
         delivery_in_udp_1 /* misc */ h with s := SC s
           -- Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data))) -->
         h with
         s :=
           SC
             (s with
              mq :=
                APPEND s.mq [(IP (i3,i4,UDP (ps3,ps4,data)),ifd.ifid)])) /\
      (!h i3 i4 oq' oqf' ps3 ps4 data ok.
         i4 IN h.ifds /\ (lookup h.s (i3,ps3,i4,ps4) = {}) /\
         (oq',oqf',ok) IN
         {(h.oq,h.oqf,T)} UNION
         enqueue
           (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),h.oq,h.oqf) /\
         i4 NOTIN LOOPBACK /\ i3 NOTIN MARTIAN UNION LOOPBACK ==>
         delivery_in_udp_2 /* misc */ h
           -- Lh_recvmsg (IP (i3,i4,UDP (ps3,ps4,data))) -->
         h with <|oq := oq'; oqf := oqf'|>) /\
      (!h i3 i4 body.
         i4 IN h.ifds /\ i4 NOTIN LOOPBACK /\
         (loopback (IP (i3,i4,body)) \/ martian (IP (i3,i4,body))) ==>
         delivery_in_martian_3 /* misc */ h
           -- Lh_recvmsg (IP (i3,i4,body)) --> h) /\
      (!h s SC es' i3' i4' i3 ps3 i4 ps4 body.
         socklist_context SC /\
         ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
          (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
         s IN lookup (SC s) (i3,ps3,i4,ps4) /\ i3' IN h.ifds /\
         ~(loopback (IP (i4',i3',body)) \/ martian (IP (i4',i3',body))) /\
         (es' =
          (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
             SOME ECONNREFUSED
           else
             s.es)) ==>
         delivery_in_icmp_1 /* misc */ h with s := SC s
           -- Lh_recvmsg (IP (i4',i3',body)) -->
         h with s := SC (s with es := es')) /\
      (!h i3' i4' i3 ps3 i4 ps4 body.
         i3' IN h.ifds /\
         ((body = ICMP_HOST_UNREACH (i3,ps3,i4,ps4)) \/
          (body = ICMP_PORT_UNREACH (i3,ps3,i4,ps4))) /\
         (lookup h.s (i3,ps3,i4,ps4) = {}) /\
         ~(loopback (IP (i4',i3',body)) \/ martian (IP (i4',i3',body))) ==>
         delivery_in_icmp_2 /* misc */ h
           -- Lh_recvmsg (IP (i4',i3',body)) --> h) /\
      (!h i3 i4 SC s ifid oq' oqf' ps3 ps4 data.
         socklist_context SC /\
         (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
         dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
         s IN lookup (SC s) (i3,ps3,i4,ps4) /\
         <|ifid := ifid; ipset := LOOPBACK; primary := localhost;
           netmask := NETMASK (255 * 2 ** 24)|> IN h.ifds ==>
         delivery_loopback_udp_1 /* misc */ h with s := SC s -- Lh_tau -->
         h with
         <|s :=
             SC
               (s with
                mq := APPEND s.mq [(IP (i3,i4,UDP (ps3,ps4,data)),ifid)]);
           oq := oq'; oqf := oqf'|>) /\
      (!h i3 i4 oq' oq'' oqf' oqf'' ps3 ps4 data ok.
         (IP (i3,i4,UDP (ps3,ps4,data)),oq',oqf') IN
         dequeue (h.oq,h.oqf) /\ i4 IN LOOPBACK /\
         (lookup h.s (i3,ps3,i4,ps4) = {}) /\
         (oq'',oqf'',ok) IN
         enqueue
           (IP (i4,i3,ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') ==>
         delivery_loopback_udp_2 /* misc */ h -- Lh_tau -->
         h with <|oq := oq''; oqf := oqf''|>) /\
      (!h SC s es' oq' oqf' i3' i4' i3 ps3 i4 ps4.
         socklist_context SC /\
         (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
         dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
         s IN lookup (SC s) (i4,ps4,i3,ps3) /\
         (es' =
          (if (s.is2 <> NONE) \/ ~s.f.bsdcompat then
             SOME ECONNREFUSED
           else
             s.es)) ==>
         delivery_loopback_icmp_1 /* misc */ h with s := SC s -- Lh_tau -->
         h with <|s := SC (s with es := es'); oq := oq'; oqf := oqf'|>) /\
      (!h i3' i4' oq' oqf' i3 ps3 i4 ps4.
         (IP (i4',i3',ICMP_PORT_UNREACH (i3,ps3,i4,ps4)),oq',oqf') IN
         dequeue (h.oq,h.oqf) /\ i3' IN LOOPBACK /\
         (lookup h.s (i4,ps4,i3,ps3) = {}) ==>
         delivery_loopback_icmp_2 /* misc */ h -- Lh_tau -->
         h with <|oq := oq'; oqf := oqf'|>) /\
      !h h' d.
        d > 0 /\ (Time_Pass d h = SOME h') ==>
        epsilon_1 /* misc */ h -- Lh_epsilon d --> h'
   
   
*)
end