signature TNet_oksTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BADCLASS_def : thm
    val LOOPBACK_def : thm
    val MARTIAN_def : thm
    val MULTICAST_def : thm
    val UDPpayloadMax_def : thm
    val ZERONET_def : thm
    val body_ips_primitive_def : thm
    val host_ok_def : thm
    val ifd_set_ok_def : thm
    val in_ifds_def : thm
    val localhost_def : thm
    val loopback_def : thm
    val martian_def : thm
    val mask_arg_munge_def : thm
    val mask_tupled_primitive_def : thm
    val msg_ok_def : thm
    val msg_oq_ok_def : thm
    val netmask_ok_def : thm
    val not_in_ifds_def : thm
    val num_of_mask_def : thm
    val sock_with_fd_def : thm
    val socket_ok_def : thm
    val socket_srcdest_ok_def : thm
    val sockfds_def : thm
  
  (*  Theorems  *)
    val LOOPBACK_MARTIAN_DISJOINT : thm
    val body_ips_def : thm
    val body_ips_ind : thm
    val localhost_IN_LOOPBACK : thm
    val mask_def : thm
    val mask_ind : thm
    val sockfds_FINITE : thm
    val sockfds_thm : thm
  
  val TNet_oks_grammars : parse_type.grammar * term_grammar.grammar
(*
   [TNet_types] Parent theory of "TNet_oks"
   
   [container] Parent theory of "TNet_oks"
   
   [int_arith] Parent theory of "TNet_oks"
   
   [BADCLASS_def]
   Definition
   |- BADCLASS =
      {i | mask (NETMASK 4) i = mask (NETMASK 4) (ip (240 * 2 ** 24))}
   
   [LOOPBACK_def]
   Definition
   |- LOOPBACK =
      {i | mask (NETMASK 8) i = mask (NETMASK 8) (ip (127 * 2 ** 24))}
   
   [MARTIAN_def]
   Definition
   |- MARTIAN = MULTICAST UNION BADCLASS UNION ZERONET
   
   [MULTICAST_def]
   Definition
   |- MULTICAST =
      {i | mask (NETMASK 4) i = mask (NETMASK 4) (ip (224 * 2 ** 24))}
   
   [UDPpayloadMax_def]  Definition  |- UDPpayloadMax = 65507
   
   [ZERONET_def]
   Definition
   |- ZERONET = {i | mask (NETMASK 8) i = mask (NETMASK 8) (ip 0)}
   
   [body_ips_primitive_def]
   Definition
   |- body_ips =
      WFREC (@R. WF R)
        (\body_ips a.
           case a of
              UDP v -> {}
           || ICMP_HOST_UNREACH v1 ->
                (case v1 of
                    (v3,v4) ->
                      case v4 of (v5,v6) -> case v6 of (v7,v8) -> {v3; v7})
           || ICMP_PORT_UNREACH v2 ->
                case v2 of
                   (v9,v10) ->
                     case v10 of
                        (v11,v12) -> case v12 of (v13,v14) -> {v9; v13})
   
   [host_ok_def]
   Definition
   |- !h.
        host_ok h =
        ifd_set_ok h.ifds /\
        (!v tid d.
           FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Ret v,d)) ==>
           ?ty. tlang_typing v (TLty_err ty)) /\
        EVERY (socket_ok h.ifds) h.s /\
        (!oq d.
           (h.oq = Timed (oq,d)) ==>
           EVERY msg_oq_ok oq /\ ((oq = []) ==> (h.oqf = F))) /\
        (!fd tid d ips is1 ps1 is2 ps2 data.
           FDOM h.ts tid /\
           (FAPPLY h.ts tid =
            Timed (Sendto2 (fd,ips,is1,ps1,is2,ps2,data),d)) ==>
           fd IN sockfds h.s /\ ((sock_with_fd fd h.s).ps1 <> NONE) /\
           (ps1 <> NONE) /\ socket_srcdest_ok h.ifds (is1,ps1,is2,ps2) /\
           ((ips <> NONE) \/ (is2 <> NONE))) /\
        (!fd tid d.
           FDOM h.ts tid /\ (FAPPLY h.ts tid = Timed (Recvfrom2 fd,d)) ==>
           fd IN sockfds h.s /\ ((sock_with_fd fd h.s).ps1 <> NONE)) /\
        (!tid rseq wseq d.
           FDOM h.ts tid /\
           (FAPPLY h.ts tid = Timed (Select2 (rseq,wseq),d)) ==>
           LIST_TO_SET (APPEND rseq wseq) SUBSET sockfds h.s /\
           time_zero <= d) /\
        (CARD (sockfds h.s) = LENGTH (MAP socket_fd h.s))
   
   [ifd_set_ok_def]
   Definition
   |- !ifdset.
        ifd_set_ok ifdset =
        FINITE ifdset /\
        (!x y.
           x IN ifdset /\ y IN ifdset /\ (x.ifid = y.ifid) ==> (x = y)) /\
        (!x. x IN ifdset ==> x.primary IN x.ipset) /\
        (!x.
           x IN ifdset ==>
           !i j.
             i IN x.ipset /\ j IN x.ipset ==>
             (mask x.netmask i = mask x.netmask j)) /\
        (!x y.
           x IN ifdset /\ y IN ifdset /\ (x <> y) ==>
           DISJOINT x.ipset y.ipset) /\
        (?!x.
           x IN ifdset /\ (x.ipset = LOOPBACK) /\
           (x.primary = localhost) /\ (x.netmask = NETMASK 24)) /\
        (?x. x IN ifdset /\ DISJOINT x.ipset LOOPBACK) /\
        !x. x IN ifdset ==> DISJOINT x.ipset MARTIAN
   
   [in_ifds_def]
   Definition
   |- !i ifds. i IN ifds = ?x. x IN ifds /\ i IN x.ipset
   
   [localhost_def]  Definition  |- localhost = ip (127 * 2 ** 24 + 1)
   
   [loopback_def]
   Definition
   |- !m.
        loopback m =
        ~DISJOINT ({m.src; m.dest} UNION body_ips m.body) LOOPBACK
   
   [martian_def]
   Definition
   |- !m.
        martian m =
        ~DISJOINT ({m.src; m.dest} UNION body_ips m.body) MARTIAN
   
   [mask_arg_munge_def]
   Definition
   |- !x x1. mask x x1 = mask_tupled (x,x1)
   
   [mask_tupled_primitive_def]
   Definition
   |- mask_tupled =
      WFREC (@R. WF R)
        (\mask_tupled a.
           case a of
              (v,v1) ->
                case v of
                   NETMASK v2 ->
                     case v1 of
                        ip v3 ->
                          ip (v3 DIV 2 ** (32 - v2) * 2 ** (32 - v2)))
   
   [msg_ok_def]
   Definition
   |- !m.
        msg_ok m =
        case m.body of
           UDP v3 ->
             (case v3 of
                 (v8,v9) ->
                   case v9 of
                      (v12,v13) -> string_size v13 <= UDPpayloadMax)
        || ICMP_HOST_UNREACH v4 -> T
        || ICMP_PORT_UNREACH v5 -> T
   
   [msg_oq_ok_def]
   Definition
   |- !m.
        msg_oq_ok m =
        msg_ok m /\ m.src NOTIN MARTIAN /\
        (!i3 ps1 i4 ps2.
           (m.body = ICMP_PORT_UNREACH (i3,ps1,i4,ps2)) ==>
           DISJOINT {i3; i4} MARTIAN) /\
        !i3 ps1 i4 ps2. m.body <> ICMP_HOST_UNREACH (i3,ps1,i4,ps2)
   
   [netmask_ok_def]  Definition  |- !n. netmask_ok (NETMASK n) = n <= 32
   
   [not_in_ifds_def]  Definition  |- !i ifds. i NOTIN ifds = ~(i IN ifds)
   
   [num_of_mask_def]
   Definition
   |- !n.
        num_of_mask (NETMASK n) =
        (2 ** 32 - 1) DIV 2 ** (32 - n) * 2 ** (32 - n)
   
   [sock_with_fd_def]
   Definition
   |- !fd s ss.
        sock_with_fd fd (s::ss) =
        (if s.fd = fd then s else sock_with_fd fd ss)
   
   [socket_ok_def]
   Definition
   |- !ifds s.
        socket_ok ifds s =
        socket_srcdest_ok ifds (s.is1,s.ps1,s.is2,s.ps2) /\
        (!m ifid. MEM (m,ifid) s.mq ==> msg_ok m /\ ~martian m) /\
        ((s.is1 = NONE) /\ (s.ps1 = NONE) /\ (s.is2 = NONE) /\
         (s.ps2 = NONE) ==>
         (s.mq = []) /\ (s.es = NONE))
   
   [socket_srcdest_ok_def]
   Definition
   |- !ifds is1 ps1 is2 ps2.
        socket_srcdest_ok ifds (is1,ps1,is2,ps2) =
        (is1 = NONE) /\ (ps1 = NONE) /\ (is2 = NONE) /\ (ps2 = NONE) \/
        (?p1.
           (is1 = NONE) /\ (ps1 = SOME p1) /\ (is2 = NONE) /\
           (ps2 = NONE)) \/
        (?i1 p1.
           (is1 = SOME i1) /\ i1 IN ifds /\ (ps1 = SOME p1) /\
           (is2 = NONE) /\ (ps2 = NONE)) \/
        ?i1 p1 i2.
          (is1 = SOME i1) /\ i1 IN ifds /\ (ps1 = SOME p1) /\
          (is2 = SOME i2)
   
   [sockfds_def]
   Definition
   |- !sl. sockfds sl = {f | MEM f (MAP socket_fd sl)}
   
   [LOOPBACK_MARTIAN_DISJOINT]  Theorem  |- DISJOINT LOOPBACK MARTIAN
   
   [body_ips_def]
   Theorem
   |- (body_ips (UDP v0) = {}) /\
      (body_ips (ICMP_HOST_UNREACH (i1,ps1,i2,ps2)) = {i1; i2}) /\
      (body_ips (ICMP_PORT_UNREACH (i1,ps1,i2,ps2)) = {i1; i2})
   
   [body_ips_ind]
   Theorem
   |- !P.
        (!v0. P (UDP v0)) /\
        (!i1 ps1 i2 ps2. P (ICMP_HOST_UNREACH (i1,ps1,i2,ps2))) /\
        (!i1 ps1 i2 ps2. P (ICMP_PORT_UNREACH (i1,ps1,i2,ps2))) ==>
        !v. P v
   
   [localhost_IN_LOOPBACK]  Theorem  |- localhost IN LOOPBACK
   
   [mask_def]
   Theorem
   |- mask (NETMASK m) (ip n) = ip (n DIV 2 ** (32 - m) * 2 ** (32 - m))
   
   [mask_ind]
   Theorem
   |- !P. (!m n. P (NETMASK m) (ip n)) ==> !v v1. P v v1
   
   [sockfds_FINITE]  Theorem  |- !sl. FINITE (sockfds sl)
   
   [sockfds_thm]
   Theorem
   |- (sockfds [] = {}) /\
      (!s ss. sockfds (s::ss) = s.fd INSERT sockfds ss) /\
      !ss1 ss2. sockfds (APPEND ss1 ss2) = sockfds ss1 UNION sockfds ss2
   
   
*)
end