LockServ.v

Require Import List.
Import ListNotations.

Set Implicit Arguments. 

Module GenHandler. 
  Definition GenHandler (W S O A : Type) : Type := S -> A * S * list W * list O % type.

  Definition ret {W S O A : Type} (a : A) : GenHandler W S O A := fun s => (a, s, [], []).

  Definition bind {W S O A B : Type} (m : GenHandler W S O A) (f : A -> GenHandler W S O B) : GenHandler W S O B :=
    fun s => 
      let '(a, s', ws1, os1) := m s in
      let '(b, s'', ws2, os2) := f a s' in
      (b, s'', ws2 ++ ws1, os2 ++ os1).

  Notation "'do' x <- m ; f" := (bind m (fun x => f)) (at level 60).

  Definition send {W S O} (w : W) : GenHandler W S O unit := fun s => (tt, s, [w], []).

  Definition output {W S O} (o : O) : GenHandler W S O unit := fun s => (tt, s, [], [o]).

  Definition mod {W S O} (f : S -> S) : GenHandler W S O unit := fun s => (tt, f s, [], []).

  Definition put {W S O} (s : S) : GenHandler W S O unit := fun _ => (tt, s, [], []).

  Definition get {W S O} : GenHandler W S O S := fun s => (s, s, [], []).

  Definition runGenHandler {W S O A} (s : S) (h : GenHandler W S O A) : A * S * list W * list O % type := h s.

  Definition nop {W S O : Type} := @ret W S O _ tt.

  Notation "a >> b" := (bind a (fun _ => b)) (at level 50).

  Definition when {W S O A} (b : bool) (m : GenHandler W S O A) : GenHandler W S O unit :=
    if b then m >> ret tt else nop.
End GenHandler.

Import GenHandler. 

Definition null {A : Type} (xs : list A) : bool :=
  match xs with
    | [] => true
    | _ => false
  end.

Section Verdi.
  Variable name input msg output : Type.

  Hypothesis name_eq_dec : forall a b : name, {a = b} + {a <> b}.

  Variable data : name -> Type.

  Definition VerdiHandler (S : Type) := (GenHandler (name * msg) S output unit).

  Variable net_handlers : forall n : name, name -> msg -> VerdiHandler (data n).
  Variable input_handlers : forall n : name, input -> VerdiHandler (data n).

  Record VerdiPacket :=
    mkPacket {
        pSrc : name;
        pDst : name;
        pMsg : msg
      }.

  Record VerdiNetwork :=
    mkNetwork {
        nwState : forall n : name, data n;
        nwPackets : list VerdiPacket
      }.

  Definition update
             {A : Type} {B : A -> Type}
             (A_eq_dec : forall a b : A, {a = b} + {a <> b})
             (f : forall a : A, B a)
             (a : A) (b : B a) 
             (x : A) : B x :=
    match A_eq_dec a x with
      | left H => eq_rect a B b x H
      | right _ => f x
    end.

  Inductive step : VerdiNetwork -> VerdiNetwork -> list output -> Prop :=
  | S_input : forall net net' i nm u s ms os,
                runGenHandler (nwState net nm) (input_handlers i) =
                (u, s, ms, os) ->
                net' = mkNetwork (update name_eq_dec (nwState net) nm s)
                                 (map (fun m => mkPacket nm (fst m) (snd m)) ms ++ nwPackets net) ->
                step net net' os
  | S_deliver : forall net net' xs p ys u s ms os,
                  nwPackets net = xs ++ p :: ys ->
                  runGenHandler (nwState net (pDst p)) (net_handlers (pSrc p) (pMsg p)) =
                  (u, s, ms, os) -> 
                  net' = mkNetwork (update name_eq_dec (nwState net) (pDst p) s)
                                   (map (fun m => mkPacket (pDst p) (fst m) (snd m)) ms ++ xs ++ ys) ->
                  step net net' os.
  Inductive step_star : VerdiNetwork -> VerdiNetwork -> list output -> Prop :=
  | SS_refl : forall net, step_star net net []
  | SS_step : forall net os1 net' os2 net'',
                step      net  net'  os1 ->
                step_star net' net'' os2 ->
                step_star net  net'' (os2 ++ os1).

End Verdi. 

Section LockServ. 
  Inductive Name :=
  | Client : nat -> Name
  | Server : Name.

  Inductive Msg :=
  | Lock   : Msg
  | Unlock : Msg
  | Locked : Msg.

  Definition Input := Msg.
  Definition Output := Msg.

  Definition name_eq_dec : forall a b : Name, {a = b} + {a <> b}.
    decide equality. decide equality. 
  Qed.

  Notation ClientData := bool.
  Notation ServerData := (list Name).

  Definition data (n : Name) : Type :=
    match n with
      | Client _ => ClientData
      | Server => ServerData
    end % type.

  Definition Handler := VerdiHandler Name Msg Output.
  Definition network := VerdiNetwork Msg data.

  Definition ClientNetHandler (n : nat) (m : Msg) : Handler ClientData :=
    match m with
      | Locked => put true >> output Locked
      | _ => nop
    end.

  Definition ClientIOHandler (n : nat) (m : Msg) : Handler ClientData :=
    match m with
      | Lock => send (Server, Lock)
      | Unlock => do holding <- get ;
                     when holding (put false >> send (Server, Unlock))
      | _ => nop
    end.

  Definition ServerNetHandler (src : Name) (m : Msg) : Handler ServerData :=
    do q <- get ; 
    match m with
      | Lock => when (null q) (send (src, Locked)) >> put (q ++ [src])
      | Unlock => match q with
                    | _ :: x :: xs => put (x :: xs) >> send (x, Locked)
                    | _ => put []
                  end
      | _ => nop
    end.

  Definition ServerIOHandler (m : Msg) : Handler ServerData := nop.

  Definition NetHandler (nm src : Name) (m : Msg) : Handler (data nm).
    refine
      (match nm as nm' return nm' = nm -> _ with
         | Server => fun pf => _
         | Client n => fun pf => _
       end eq_refl).
    - subst. exact (ClientNetHandler n m).
    - subst. exact (ServerNetHandler src m).
  Defined.

  Definition InputHandler (nm : Name) (i : Msg) : Handler (data nm).
    refine
      (match nm as nm' return nm' = nm -> _ with
         | Server => fun pf => _
         | Client n => fun pf => _
       end eq_refl).
    - subst. exact (ClientIOHandler n i).
    - subst. exact (ServerIOHandler i).
  Defined.

  Definition locks_correct (net : network) : Prop :=
    forall n,
      nwState net (Client n) = true ->
      exists t,
        nwState net Server = Client n :: t.

  Definition locks_correct_unlock (net : network) : Prop :=
    forall p,
      In p (nwPackets net) ->
      pMsg p = Unlock -> 
      exists n, 
        pSrc p = Client n /\
        (exists t, nwState net Server = Client n :: t) /\
        nwState net (Client n) = false.

  Definition locks_correct_locked (net : network) : Prop :=
    forall p,
       In p (nwPackets net) ->
       pMsg p = Locked -> 
       exists n, 
         pDst p = Client n /\
         (exists t, nwState net Server = Client n :: t) /\
         nwState net (Client n) = false.

  Definition at_most_one (m : Msg) (net : network) : Prop :=
    forall p,
      In p (nwPackets net) ->
      pMsg p = m ->
      exists xs ys,
        nwPackets net = xs ++ p :: ys /\
        (forall z, In z xs -> pMsg z <> m) /\
        (forall z, In z ys -> pMsg z <> m).

  Definition never_both (m1 m2 : Msg) (net : network) : Prop :=
    forall p1 p2,
      In p1 (nwPackets net) ->
      In p2 (nwPackets net) ->
      pMsg p1 = m1 ->
      pMsg p2 = m2 ->
      False.