open HolKernel boolLib Parse

local open TNet_oksTheory TNet_typesTheory in end
open bossLib simpLib

infix THEN THENL
infix 8 by

val _ = new_theory "TNet_auxfns";

(* -------------------------------------------------- *)
(*                SCHEDULING PARAMETERS               *)
(* -------------------------------------------------- *)

(* maximum host op scheduling delay: *)
val dsched_def = Define`dsched = time (1/100)`;

(* maximum outqueue scheduling delay: *)
val doq_def = Define`doq = time (1/100)`;

(* -------------------------------------------------- *)

val orderings_def =  (* all orderings of a set *)
  Define`
  orderings s l = (LIST_TO_SET l = s)    /\
                  (LENGTH l      = CARD s) `;


(* various relatively simple auxiliary functions *)

val enqueue_def =  (* 2.3.18 *)
  Define`
  (enqueue (m, oq, T) = {(oq, T, F)})  (* queue is already full *) /\
  (enqueue (m, Timed(oqu,d), F) = {(if oqu = []
                                    then Timed([m],doq)
                                    else Timed((m::oqu),d),
                                    oqf', T) | oqf' IN {T; F}})`;

val dequeue_def =  (* 2.3.18 *)
  Define`
    dequeue (Timed(oqu,d), oqf) =
      if oqu = [] then {}
      else { (m,Timed(oqu',d'),oqf')
           | (m = LAST oqu) /\ (oqu' = FRONT oqu) /\
             (d' = if oqu' = [] then time_infty else doq) /\
             oqf' IN {oqf /\ (oqu' <> []); F}}`;

val outroute_def = (* 2.3.7 *)
  Define`
    outroute (ifdset, i) =
        if i IN LOOPBACK then {localhost}
        else { r.primary | r IN ifdset /\ (r.ipset <> LOOPBACK)}`;

val dosend_def = (* 2.3.19 *)
  Define`
   (dosend (ifds, (NONE, data), (SOME i1, SOME p1, SOME i2, ps2), oq, oqf) =
      enqueue(<| src := i1; dest := i2; body := UDP(SOME p1, ps2, data)|>,
              oq, oqf)) /\
   (dosend (ifds, (SOME(i,p), data), (NONE, SOME p1, NONE, NONE), oq, oqf) =
      BIGUNION { enqueue(<| src := i'; dest := i;
                            body := UDP(SOME p1, SOME p, data) |>,
                         oq, oqf)
               | i' IN outroute(ifds, i)}) /\
   (dosend (ifds, (SOME(i,p), data),
            (SOME i1, SOME p1, is2, ps2), oq, oqf) =
    enqueue(<| src := i1; dest := i;
               body := UDP(SOME p1, SOME p, data) |>,
            oq, oqf))`;

val unused_def = (* 2.3.3 *)
  Define`
    unused s = { Port p | 1 <= p /\ p <= 65535 /\
                          ~?s'. (s'.ps1 = SOME (Port p)) /\ s' IN s}`;

val ephemeral_def = (* 2.3.3 *)
  Define`ephemeral (Port p) = 1024 <= p /\ p <= 4999`;

val ephemeralErrors_def = (* 2.3.10 *)
  Define`ephemeralErrors = {EAGAIN; EADDRINUSE}`;

val privileged_def = (* 2.3.3 *)
  Define`privileged (Port p) = 0 <= p /\ p <= 1023`;

(* contexts, represented as functions *)

val socklist_context_def =
    Define`socklist_context (SC : socket -> socket list) =
             ?s1 s2. !s. SC s = APPEND s1 (s :: s2)`;

(* define a pair of functions to get the socket lists s1 and s2 out of a
   socklist context *)

val scs_functions_def = new_specification {
  consts = [{const_name = "scs1", fixity = Prefix},
            {const_name = "scs2", fixity = Prefix}],
  name = "scs_functions_def",
  sat_thm =
  (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV SKOLEM_CONV)) o
   GEN_ALL o
   SIMP_RULE std_ss [GSYM RIGHT_EXISTS_IMP_THM] o
   #1 o EQ_IMP_RULE o
   SPEC_ALL) socklist_context_def};

(* don't want this to be polymorphic, so that we can prove the injectivity
   theorem below *)
val mk_sc_def = Define`mk_sc s1 s2 (s:socket) = APPEND s1 (s :: s2)`;
val mk_sc_scontext = store_thm(
  "mk_sc_scontext",
  ``!s1 s2. socklist_context (mk_sc s1 s2)``,
  SIMP_TAC std_ss [socklist_context_def, mk_sc_def] THEN PROVE_TAC []);

val always_a_different_socket = store_thm(
  "always_a_different_socket",
  ``!s:socket. ?s'. ~(s' = s)``,
  GEN_TAC THEN Q.EXISTS_TAC `s with mq := (ARB :: s.mq)` THEN
  RW_TAC list_ss [TNet_typesTheory.socket_component_equality]);

val mk_sc_11 = store_thm(
  "mk_sc_11",
  ``!s1 s2 s3 s4. (mk_sc s1 s2 = mk_sc s3 s4) = (s1 = s3) /\ (s2 = s4)``,
  SIMP_TAC std_ss [mk_sc_def, FUN_EQ_THM] THEN
  Induct THEN SIMP_TAC list_ss [] THEN REPEAT GEN_TAC THEN
  Cases_on `s3` THEN
  ASM_SIMP_TAC list_ss [EXISTS_OR_THM, always_a_different_socket,
                        GSYM always_a_different_socket, FORALL_AND_THM,
                        CONJ_ASSOC]);

val sc_inversions = store_thm(
  "sc_inversions",
  ``!s1 s2. (scs1 (mk_sc s1 s2) = s1) /\ (scs2 (mk_sc s1 s2) = s2)``,
  REPEAT GEN_TAC THEN
  `socklist_context (mk_sc s1 s2)` by PROVE_TAC [mk_sc_scontext] THEN
  IMP_RES_TAC scs_functions_def THEN
  FULL_SIMP_TAC std_ss [GSYM mk_sc_def, GSYM FUN_EQ_THM, mk_sc_11] THEN
  PROVE_TAC []);

val sc_characterise = store_thm(
  "sc_characterise",
  ``!SC. socklist_context SC ==> ?s1 s2. (SC = mk_sc s1 s2)``,
  REPEAT STRIP_TAC THEN
  MAP_EVERY Q.EXISTS_TAC [`scs1 SC`, `scs2 SC`] THEN
  ASM_SIMP_TAC std_ss [scs_functions_def, FUN_EQ_THM, mk_sc_def]);

val F_context_def =
  Define`
    F_context (FC : ((ifd -> bool) # tid # hostThreadState timed # socket) -> host) =
       ?SC ts oq oqf.
          socklist_context SC /\
          !ifds tid t s.
              FC (ifds, tid, t, s) =
              <| ifds := ifds; ts := FUPDATE ts (tid,t); s := SC s; oq := oq; oqf := oqf |>`;

val FC_functions_def =
    new_specification
    {
     consts = [{const_name = "fc_sc", fixity = Prefix},
               {const_name = "fc_ts", fixity = Prefix},
               {const_name = "fc_oq", fixity = Prefix},
               {const_name = "fc_oqf", fixity = Prefix}],
     name = "FC_functions_def",
     sat_thm =
     (CONV_RULE (TOP_DEPTH_CONV (CHANGED_CONV SKOLEM_CONV)) o
      GEN_ALL o
      SIMP_RULE std_ss [GSYM RIGHT_EXISTS_IMP_THM] o
      #1 o EQ_IMP_RULE o
      SPEC_ALL) F_context_def};

val FC_accessors = store_thm(
  "FC_accessors",
  ``!FC ifds tid t s.
       F_context FC ==>
       ((FC(ifds,tid,t,s)).ts = FUPDATE (fc_ts FC) (tid,t)) /\
       ((FC(ifds,tid,t,s)).ifds = ifds) /\
       ((FC(ifds,tid,t,s)).oq = fc_oq FC) /\
       ((FC(ifds,tid,t,s)).oqf = fc_oqf FC) /\
       ((FC(ifds,tid,t,s)).s = APPEND (scs1 (fc_sc FC)) (s:: scs2 (fc_sc FC)))``,
  SRW_TAC [] [FC_functions_def] THEN
  `socklist_context (fc_sc FC)` by PROVE_TAC [FC_functions_def] THEN
  PROVE_TAC [scs_functions_def]);

val SC_unused_def =
  Define`
    SC_unused SC = unused (LIST_TO_SET (scs1 SC)) UNION
                   unused (LIST_TO_SET (scs2 SC))`;

val FC_unused_def = Define`FC_unused FC = SC_unused (fc_sc FC)`;

val _ = overload_on ("unused", ``SC_unused``);
val _ = overload_on ("unused", ``FC_unused``);

val FC_autobind_def =
  Define`
    (FC_autobind(NONE, FC) = FC_unused FC INTER ephemeral) /\
    (FC_autobind(SOME p, FC) = {p})`;

val SC_autobind_def =
  Define`(SC_autobind(NONE, SC) = SC_unused SC INTER ephemeral) /\
         (SC_autobind(SOME p, SC) = {p})`;

val _ = overload_on ("autobind", ``FC_autobind``);
val _ = overload_on ("autobind", ``SC_autobind``);

val sockets_of_FC =
  Define`
    sockets_of_FC FC =
      LIST_TO_SET (APPEND (scs1 (fc_sc FC)) (scs2 (fc_sc FC)))`;

val _ = overload_on ("socks", ``sockets_of_FC``);

val in_sockets_of_FC =
  Define`in_sockets_of_FC s FC = s IN sockets_of_FC FC`;

val _ = overload_on ("IN", ``in_sockets_of_FC``);


val _ = new_constant("valid_ip_string", ``:string -> bool``);
val _ = new_constant("ipstr_to_ip", ``:string -> ip``);

val match_def =  (* 2.3.20 *)
  Define`
    (match (NONE,NONE,NONE,NONE) _ = 0n) /\
    (match (NONE, SOME p1, NONE, NONE) (i3,ps3,i4,ps4) =
       if ps4 = SOME p1 then 1 else 0) /\
    (match (SOME i1, SOME p1, NONE, NONE) (i3,ps3,i4,ps4) =
       if (i1 = i4) /\ (SOME p1 = ps4) then 2 else 0) /\
    (match (SOME i1, SOME p1, SOME i2, NONE) (i3,ps3,i4,ps4) =
       if (i2 = i3) /\ (i1 = i4) /\ (SOME p1 = ps4) then 3 else 0) /\
    (match (SOME i1, SOME p1, SOME i2, SOME p2) (i3,ps3,i4,ps4) =
       if (SOME p2 = ps3) /\ (i2 = i3) /\ (i1 = i4) /\ (SOME p1 = ps4) then 4
       else 0)`;

val score_def =
  Define`score s quad = match(s.is1,s.ps1,s.is2,s.ps2) quad`;

val lookup_def =
  Define`lookup slist quad =
           { s | MEM s slist /\
                 let sn = score s quad in
                   sn > 0 /\
                   ~?s'. MEM s' slist /\ score s' quad > sn }`;

(* zombify function, takes a threadstate and a (now closed) fd.
   It returns a threadstate that is the same as the original, except that
   elements that were Sendto2 or Recvfrom2 on the closed fd
   become Zombie, and Select2 states are updated to lose all mention of the
   closed fd.

   This will be post-composed with the host's tid |-> threadstate map in
   the rule for a successful socket close. *)

val zombify_def =
  Define`zombify fd (Timed(ts, d)) =
           case ts of
              Sendto2(fd', otherstuff) -> if fd = fd' then
                                            Timed(Zombie, time_infty)
                                          else Timed(ts, d)
           || Recvfrom2 fd' -> if fd = fd' then Timed(Zombie, time_infty)
                               else Timed(ts, d)
           || Select2(rseq, wseq) ->
                  Timed(Select2(FILTER (\fd'. ~(fd' = fd)) rseq,
                                FILTER (\fd'. ~(fd' = fd)) wseq),
                        d)
           || otherwise -> Timed(ts, d)`;

val _ = export_theory();