From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
From DiSeL
Require Import Actions Injection Process Always HoareTriples InferenceRules.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Module LockProtocol.
Section LockProtocol.

Variable server : nid.
Variable clients : seq nid.

Hypothesis Hnin : server \notin clients.
Hypothesis Huniq : uniq clients.

Lemma client_not_server n : n \in clients -> (n == server) = false.
Proof.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
  move=>H.
(* Goal: forall _ : client_send_safe this to d m, and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
  case E: (n == server)=>//.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
  move/eqP in E. subst n.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
  move: (Hnin).
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by rewrite H.
Qed.

Definition nodes := [:: server] ++ clients.

Lemma client_nodes n : n \in clients -> n \in nodes.
Proof.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by rewrite inE orbC/= =>->.
Qed.

Notation epoch := nat (only parsing).

Record server_state :=
  ServerState {
      outstanding : seq nid;
      current_epoch : epoch;
      current_holder : option nid
    }.

Inductive client_state :=
| NotHeld
| Held of epoch.

Definition acquire_tag := 0.
Definition grant_tag := 1.
Definition release_tag := 2.

Definition msg_from_server ms e :=
  (tag ms == grant_tag) && (tms_cont ms == [:: e]).

Definition msg_from_client ms :=
  ((tag ms == acquire_tag) || (tag ms == release_tag)) &&
  (tms_cont ms == [::]).

Definition coh_msg pkt e :=
  if from pkt == server
  then to pkt \in clients /\ msg_from_server (content pkt) e
  else if from pkt \in clients
  then to pkt == server /\ msg_from_client (content pkt)
  else False.

Definition st := ptr_nat 1.

Definition client_local_coh (cs : client_state) :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  [Pred h | h = st :-> cs].

Definition server_local_coh (ss : server_state) :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  [Pred h | h = st :-> ss].

Definition local_coh (n : nid) :=
  [Pred h | valid h /\
   if n == server
   then exists ss, server_local_coh ss h
   else n \in clients /\
        exists cs, client_local_coh cs h].

Definition soup_coh : Pred soup :=
  [Pred s |
    valid s /\
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    forall m ms, find m s = Some ms -> active ms -> exists e, coh_msg ms e].

Lemma soup_coh_post_msg d m:
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    soup_coh (dsoup d) -> (exists e, coh_msg m e) -> soup_coh (post_msg (dsoup d) m).1.
Proof.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
move=>[H1 H2][y]Cm; split=>[|i ms/=]; first by rewrite valid_fresh.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite findUnL; last by rewrite valid_fresh.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
case: ifP=>E; first by move/H2.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by move/findPt_inv=>[Z G]; subst i m; exists y.
Qed.

Definition state_coh d :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  forall n, n \in nodes -> local_coh n (getLocal n d).

Definition lock_coh d :=
  let: dl := dstate d in
  let: ds := dsoup d in
  [/\ soup_coh ds
   , dom dl =i nodes
   , valid dl
   & state_coh d].

Lemma l1 d: lock_coh d -> valid (dstate d).
Proof. by case. Qed.

Lemma l2 d: lock_coh d -> valid (dsoup d).
Proof. by case; case. Qed.

Lemma l3 d: lock_coh d -> dom (dstate d) =i nodes.
Proof. by case. Qed.

Definition LockCoh := CohPred (CohPredMixin l1 l2 l3).

Lemma consume_coh d m : LockCoh d -> soup_coh (consume_msg (dsoup d) m).
Proof.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
move=>C; split=>[|m' msg]; first by apply: consume_valid; rewrite (cohVs C).
(* Goal: forall (_ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) m' (consume_msg (dsoup d) m)) (@Some (State.msg TaggedMessage) msg)) (_ : is_true (@active TaggedMessage msg)), @ex (Equality.sort nat_eqType) (fun e : Equality.sort nat_eqType => coh_msg msg e) *)
case X: (m == m');[move/eqP: X=><-{m'}|].
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- case/(find_mark (cohVs C))=>tms[E]->{msg}.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by case:(C); case=>_/(_ m tms E).
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite eq_sym in X.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite (mark_other (cohVs C) X)=>E.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by case:(C); case=>_; move/(_ m' msg E).
Qed.

Lemma coh_dom_upd this d s :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  this \in nodes -> LockCoh d -> dom (upd this s (dstate d)) =i nodes.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>D C z; rewrite -(cohDom C) domU inE/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
by case: ifP=>///eqP->{z}; rewrite (cohDom C) D; apply: cohVl C.
Qed.

Definition server_send_step (ss : server_state) (to : nid) : server_state :=
  if to \in clients
  then if outstanding ss is _ :: out'
       then ServerState out' (S (current_epoch ss)) (Some to)
       else ss
  else ss.

Definition client_send_step (cs : client_state) : client_state :=
  NotHeld. (* ! *)



Definition server_recv_step (ss : server_state) (from : nid)
           (mtag : nat) (mbody : seq nat) : server_state :=
  if mtag == acquire_tag
  then
    ServerState (rcons (outstanding ss) from) (current_epoch ss) (current_holder ss)
  else (* mtag == release_tag *)
    ServerState (outstanding ss) (current_epoch ss) None.


Definition client_recv_step (cs : client_state) (from : nid)
           (mtag : nat) (mbody : seq nat) : client_state :=
  if mbody is [:: e]
  then Held e
  else NotHeld.

Section GetterLemmas.

Lemma getLocal_coh n d (C : LockCoh d):
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  n \in nodes ->
  valid (getLocal n d) /\
  if n == server
  then exists (ss : server_state),
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
      getLocal n d = st :-> ss
  else (n \in clients) /\
       exists (cs : client_state),
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
           getLocal n d = st :-> cs.
Proof.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by case: C=>_ _ _ /(_ n)G; rewrite /local_coh/=.
Qed.

Lemma getLocal_server_st_tp d (C : LockCoh d) s:
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  find st (getLocal server d) = Some s ->
  dyn_tp s = server_state.
Proof.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have pf: server \in nodes by rewrite inE eqxx.
(* Goal: forall _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal server d)) (@Some (@dynamic Type (fun x : Type => x)) s), @eq Type (@dyn_tp Type (fun x : Type => x) s) server_state *)
move: (getLocal_coh C pf); rewrite eqxx; move =>[V][s']Z; rewrite Z in V *.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite findPt /=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
by case =><-.
Qed.

Lemma getLocal_client_st_tp n d (C : LockCoh d) (H : n \in clients) s:
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  find st (getLocal n d) = Some s ->
  dyn_tp s = client_state.
Proof.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have pf: n \in nodes by rewrite inE/= orbC H.
(* Goal: @eq client_state ((if @in_mem nat c (@mem nat (seq_predType nat_eqType) clients) as b return (forall _ : @protect_term Prop (@eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) b), client_state) then fun X : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) true => match @UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d) as f return (forall _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) f, client_state) with | Some v => fun epf : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@Some (@dynamic Type (fun x : Type => x)) v) => @cast Type (fun x : Type => x) client_state (@dyn_tp Type (fun x : Type => x) v) (@Logic.eq_sym Type (@dyn_tp Type (fun x : Type => x) v) client_state (@getLocal_client_st_tp c d C X v epf)) (@dyn_val Type (fun x : Type => x) v) | None => fun _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@None (@dynamic Type (fun x : Type => x))) => NotHeld end (@Logic.eq_refl (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d))) else fun _ : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) false => NotHeld) (@Logic.eq_refl bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)))) m *)
move: (getLocal_coh C pf); rewrite H=>[[V]].
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite client_not_server//.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>[_][cs] L. rewrite L in V *.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite findPt /=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
by case=> <-.
Qed.

Definition getSt_server d (C : LockCoh d) : server_state :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  match find st (getLocal server d) as f return _ = f -> _ with
    Some v => fun epf => icast (sym_eq (getLocal_server_st_tp C epf)) (dyn_val v)
  | _ => fun epf => ServerState [::] 0 None
  end (erefl _).

Lemma getSt_server_K d (C : LockCoh d) m :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  getLocal server d = st :-> m -> getSt_server C = m.
Proof.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>E; rewrite /getSt_server/=.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have pf: server \in nodes by rewrite inE eqxx.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have V: valid (getLocal server d) by case: (getLocal_coh C pf).
(* Goal: @eq client_state ((if @in_mem nat c (@mem nat (seq_predType nat_eqType) clients) as b return (forall _ : @protect_term Prop (@eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) b), client_state) then fun X : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) true => match @UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d) as f return (forall _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) f, client_state) with | Some v => fun epf : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@Some (@dynamic Type (fun x : Type => x)) v) => @cast Type (fun x : Type => x) client_state (@dyn_tp Type (fun x : Type => x) v) (@Logic.eq_sym Type (@dyn_tp Type (fun x : Type => x) v) client_state (@getLocal_client_st_tp c d C X v epf)) (@dyn_val Type (fun x : Type => x) v) | None => fun _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@None (@dynamic Type (fun x : Type => x))) => NotHeld end (@Logic.eq_refl (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d))) else fun _ : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) false => NotHeld) (@Logic.eq_refl bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)))) m *)
move: (getLocal_server_st_tp C); rewrite !E=>/= H.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by apply: eqc.
Qed.

Program Definition getSt_client c d (C : LockCoh d) (pf : c \in nodes) : client_state.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
case X: (c \in clients); last by exact: NotHeld.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
exact: (match find st (getLocal c d) as f return _ = f -> _ with
    Some v => fun epf => icast (sym_eq (getLocal_client_st_tp C X epf)) (dyn_val v)
  | _ => fun epf => NotHeld
  end (erefl _)).
Defined.

Lemma getSt_client_K c d (C : LockCoh d) (pf : c \in nodes) m :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  c \in clients -> getLocal c d = st :-> m -> getSt_client C pf = m.
Proof.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>X E; rewrite /getSt_client/=.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have V: valid (getLocal c d) by case: (getLocal_coh C pf).
(* Goal: @eq client_state ((if @in_mem nat c (@mem nat (seq_predType nat_eqType) clients) as b return (forall _ : @protect_term Prop (@eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) b), client_state) then fun X : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) true => match @UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d) as f return (forall _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) f, client_state) with | Some v => fun epf : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@Some (@dynamic Type (fun x : Type => x)) v) => @cast Type (fun x : Type => x) client_state (@dyn_tp Type (fun x : Type => x) v) (@Logic.eq_sym Type (@dyn_tp Type (fun x : Type => x) v) client_state (@getLocal_client_st_tp c d C X v epf)) (@dyn_val Type (fun x : Type => x) v) | None => fun _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d)) (@None (@dynamic Type (fun x : Type => x))) => NotHeld end (@Logic.eq_refl (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal c d))) else fun _ : @eq bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)) false => NotHeld) (@Logic.eq_refl bool (@in_mem nat c (@mem nat (seq_predType nat_eqType) clients)))) m *)
move: (getLocal_client_st_tp C); rewrite X !E=>/= H.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by apply: eqc.
Qed.

End GetterLemmas.

Section ServerGenericSendTransitions.

Definition HServ this to := (this == server /\ to \in clients).

Variable the_tag : nat.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Variable prec : server_state -> nid -> seq nid -> Prop.

Hypothesis prec_safe :
  forall this to s m,
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    HServ this to ->
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    prec s to m ->
    coh_msg (Msg (TMsg the_tag m) this to true) (current_epoch s).

Notation coh := LockCoh.

Definition server_send_safe (this n : nid)
           (d : dstatelet) (msg : seq nat) :=
  HServ this n /\
  exists (C : coh d), prec (getSt_server C) n msg.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma server_send_safe_coh this to d m : server_send_safe this to d m -> coh d.
Proof. by case=>_[]. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma server_send_this_in this to : HServ this to -> this \in nodes.
Proof. by case=>/eqP->; rewrite inE eqxx. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma server_send_to_in this to : HServ this to -> to \in nodes.
Proof. by case=>_; rewrite /nodes inE/= orbC=>->. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma server_send_safe_in this to d m : server_send_safe this to d m ->
                                  this \in nodes /\ to \in nodes.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
by case=>[]=>G _; move/server_send_to_in: (G)->; case: G=>/eqP-> _; rewrite inE eqxx.
Qed.


Definition server_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf : server_send_safe this to d msg) :=
  let C := server_send_safe_coh pf in
  let s := getSt_server C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  Some (st :-> server_send_step s to).

Lemma server_step_coh : s_step_coh_t coh the_tag server_step.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>this to d msg pf h[]->{h}.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have C : (coh d) by case: pf=>?[].
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have E: this = server by case: pf=>[][]/eqP.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- apply: soup_coh_post_msg; first by case:(server_send_safe_coh pf).
(* Goal: forall _ : client_send_safe this to d m, and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
  case: (pf)=>H[C']P/=.
  eexists.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by apply: (prec_safe _ P).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by apply: coh_dom_upd=>//; case: (server_send_safe_in pf).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by rewrite validU; apply: cohVl C.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>n Ni. rewrite /local_coh/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /getLocal/=findU; case: ifP=>B; last by case: C=>_ _ _/(_ n Ni).
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end)) (if @eq_op nat_eqType n server then @ex server_state (fun ss : server_state => @eq Heap.heap match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts server_state st ss)) else and (is_true (@in_mem nid n (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts client_state st cs)))) *)
move/eqP: B=>Z; subst n this; rewrite eqxx (cohVl C)/=.
(* Goal: and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
split.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by rewrite validPt.
by eexists.
Qed.

Lemma server_step_def this to d msg :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
      server_send_safe this to d msg <->
      exists b pf, @server_step this to d msg pf = Some b.
Proof.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
split=>[pf/=|]; last by case=>?[].
set b := let C := server_send_safe_coh pf in
         let s := getSt_server C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
         st :-> (server_send_step s to).
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by exists b, pf.
Qed.

Definition server_send_trans :=
  SendTrans server_send_safe_coh server_send_safe_in server_step_def server_step_coh.

End ServerGenericSendTransitions.

Section ServerSendTransitions.

Definition server_send_grant_prec (ss : server_state) to m :=
  exists rest e,
    ss = ServerState (to :: rest) e None /\
    m = [:: e].

Program Definition server_send_grant_trans : send_trans LockCoh :=
  @server_send_trans grant_tag server_send_grant_prec _.
Next Obligation.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
case: H=>/eqP->H; rewrite /coh_msg eqxx; split=>//=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
case: H0=>[rest] [e] []-> ->/=. by rewrite /msg_from_server /= eqxx.
Qed.

End ServerSendTransitions.

Section ServerGenericReceiveTransitions.

Notation coh := LockCoh.

Variable the_tag : nat.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Variable server_recv_wf : forall d, coh d -> nid -> nid -> TaggedMessage -> bool.

Definition rs_step : receive_step_t coh :=
  fun this (from : nid) (m : seq nat) d (pf : coh d) (pt : this \in nodes) =>
    if (this == server)
    then let s := getSt_server pf in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
         st :-> server_recv_step s from the_tag m
    else getLocal this d.

Lemma rs_step_coh : r_step_coh_t server_recv_wf the_tag rs_step.
Proof.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>d from this m C pf tms D F Wf T/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /rs_step; case X: (this == server); last first.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by apply: coh_dom_upd.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  + by rewrite validU; apply: cohVl C.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  by move=>n Ni/=; case: (C)=>_ _ _/(_ n Ni)=>L; rewrite -(getLocalU)// (cohVl C).
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by apply: coh_dom_upd.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by rewrite validU; apply: cohVl C.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>n Ni/=; rewrite /local_coh/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /getLocal/=findU; case: ifP=>B/=; last by case: (C)=>_ _ _/(_ n Ni).
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end)) (if @eq_op nat_eqType n server then @ex server_state (fun ss : server_state => @eq Heap.heap match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts server_state st ss)) else and (is_true (@in_mem nid n (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap match (if @PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d) then @Some Heap.heap (@heap_pts server_state st (server_recv_step (@getSt_server d C) from the_tag (tms_cont tms))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts client_state st cs)))) *)
move/eqP: B X=>Z/eqP X; subst n this; rewrite eqxx (cohVl C)/=.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
split; first by rewrite validPt.
by eexists.
Qed.

Definition rs_recv_trans := ReceiveTrans rs_step_coh.

End ServerGenericReceiveTransitions.

Section ServerReceiveTransitions.

Definition s_matches_tag (ss : server_state) from t :=
  (t == acquire_tag) ||
  ((t == release_tag) && (current_holder ss == Some from)).

Definition server_msg_wf d (C : LockCoh d) (this from : nid) :=
  [pred m : TaggedMessage | s_matches_tag (getSt_server C) from (tag m)].

Definition server_recv_acquire_trans := rs_recv_trans acquire_tag server_msg_wf.

Definition server_recv_release_trans := rs_recv_trans release_tag server_msg_wf.

End ServerReceiveTransitions.


Section ClientGenericSendTransitions.

Definition HClient this to := (this \in clients /\ to == server).

Variable the_tag : nat.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Variable prec : client_state -> nid -> seq nat -> Prop.

Hypothesis prec_safe :
  forall this to s m,
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    HClient this to ->
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
    prec s to m ->
    msg_from_client (TMsg the_tag m).

Notation coh := LockCoh.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma client_send_this_in this to : HClient this to -> this \in nodes.
Proof. case=>H _. by apply /client_nodes. Qed.

Definition client_send_safe (this n : nid)
           (d : dstatelet) (msg : seq nat) :=
  HClient this n /\
  exists (HC : HClient this n) (C : coh d), prec (getSt_client C (client_send_this_in HC)) n msg.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma client_send_safe_coh this to d m : client_send_safe this to d m -> coh d.
Proof. by case => _[?][C]. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma client_send_to_in this to : HClient this to -> to \in nodes.
Proof. by case=>_ /eqP->; rewrite /nodes inE/= eqxx. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Lemma client_send_safe_in this to d m : client_send_safe this to d m ->
                                  this \in nodes /\ to \in nodes.
Proof.
(* Goal: forall _ : client_send_safe this to d m, and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
case=>_[HC][C]_.
(* Goal: and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
split.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- exact: (client_send_this_in HC).
(* Goal: is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes)) *)
exact: (client_send_to_in HC).
Qed.

Definition client_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf : client_send_safe this to d msg) :=
  let C := client_send_safe_coh pf in
  let s := getSt_client C (client_send_this_in (proj1 pf)) in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  Some (st :-> client_send_step s).

Lemma client_step_coh : s_step_coh_t coh the_tag client_step.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>this to d msg pf h[]->{h}.
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have C : (coh d) by exact: (client_send_safe_coh pf).
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
have E: this \in clients by case: pf=>_[][].
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- apply: soup_coh_post_msg; first by case:(client_send_safe_coh pf).
(* Goal: forall _ : client_send_safe this to d m, and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
  case: (pf)=>_[H][C']P/=.
  exists 0.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
  rewrite/coh_msg/= client_not_server// E.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
  split; first by case: (H).
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  by apply: (prec_safe H P).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by apply: coh_dom_upd=>//; case: (client_send_safe_in pf).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by rewrite validU; apply: cohVl C.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>n Ni. rewrite /local_coh/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /getLocal/=findU; case: ifP=>B; last by case: C=>_ _ _/(_ n Ni).
(* Goal: @eq bool true false *)
move/eqP: B=>Z; subst n.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite client_not_server// (cohVl C)/=.
(* Goal: and (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) nodes))) *)
split.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by rewrite validPt.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>//.
by eexists.
Qed.

Lemma client_step_def this to d msg :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
      client_send_safe this to d msg <->
      exists b pf, @client_step this to d msg pf = Some b.
Proof.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
split=>[pf/=|]; last by case=>?[].
set b := let C := client_send_safe_coh pf in
         let s := getSt_client C (client_send_this_in (proj1 pf)) in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
         st :-> (client_send_step s).
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by exists b, pf.
Qed.

Definition client_send_trans :=
  SendTrans client_send_safe_coh client_send_safe_in client_step_def client_step_coh.

End ClientGenericSendTransitions.

Section ClientSendTransitions.

Definition client_send_acquire_prec (cs : client_state) (to : nid) (m : seq nat) :=
  cs = NotHeld /\
  m = [::].

Program Definition client_send_acquire_trans : send_trans LockCoh :=
  @client_send_trans acquire_tag client_send_acquire_prec _.
Next Obligation.
(* Goal: is_true (msg_from_client (TMsg release_tag m)) *)
apply/andP=>/=.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>//.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by case: H0=>_/eqP.
Qed.

Definition client_send_release_prec (cs : client_state) (to : nid) (m : seq nat) :=
  (exists e, cs = Held e) /\
  m = [::].

Program Definition client_send_release_trans : send_trans LockCoh :=
  @client_send_trans release_tag client_send_release_prec _.
Next Obligation.
(* Goal: is_true (msg_from_client (TMsg release_tag m)) *)
apply/andP=>/=.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>//.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by case: H0=>_/eqP.
Qed.

End ClientSendTransitions.

Section ClientGenericReceiveTransitions.

Notation coh := LockCoh.

Variable the_tag : nat.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
Variable client_recv_wf : forall d, coh d -> nid -> nid -> TaggedMessage -> bool.

Definition rc_step : receive_step_t coh :=
  fun this (from : nid) (m : seq nat) d (pf : coh d) (pt : this \in nodes) =>
    if (this \in clients)
    then let s := getSt_client pf pt in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
         st :-> client_recv_step s from the_tag m
    else getLocal this d.

Lemma rc_step_coh : r_step_coh_t client_recv_wf the_tag rc_step.
Proof.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>d from this m C pf tms D F Wf T/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /rc_step; case X: (this \in clients); last first.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m)) *)
(* Goal: lock_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by apply: coh_dom_upd.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
  + by rewrite validU; apply: cohVl C.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  have Y: forall z : nat_eqType, z \in nodes -> local_coh z (getLocal z d)
      by case: (C).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
  by move=>n Ni/=; move: (Y n Ni)=>L; rewrite -(getLocalU)// (cohVl C).
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by apply: coh_dom_upd.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
- by rewrite validU; apply: cohVl C.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move=>n Ni/=; rewrite /local_coh/=.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
rewrite /getLocal/=findU; case: ifP=>B/=; last by case: (C)=>_ _ _/(_ n Ni).
(* Goal: @eq bool true false *)
move/eqP: B X=>Z/eqP X/= ;rewrite !(cohVl C); subst n.
(* Goal: and (is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))))) (if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)))) *)
split; first done.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
move/eqP: X => X.
(* Goal: if @eq_op nat_eqType this server then @ex server_state (fun ss : server_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts server_state st ss)) else and (is_true (@in_mem nid this (@mem nat (seq_predType nat_eqType) clients))) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
rewrite client_not_server X//.
(* Goal: and (is_true true) (@ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs))) *)
split=>//.
(* Goal: @ex client_state (fun cs : client_state => @eq Heap.heap (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (@heap_pts client_state st cs)) *)
by eexists _.
Qed.

Definition rc_recv_trans := ReceiveTrans rc_step_coh.

End ClientGenericReceiveTransitions.

Section ClientReceiveTransitions.

Definition client_msg_wf d (_ : LockCoh d) (this from : nid) :=
  [pred m : TaggedMessage | true].

Definition client_receive_grant_trans := rc_recv_trans grant_tag client_msg_wf.

End ClientReceiveTransitions.

Section Protocol.

Variable l : Label.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
(* All send-transitions *)
Definition lock_sends :=
  [::
     server_send_grant_trans;
     client_send_acquire_trans;
     client_send_release_trans
  ].

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d))) *)
(* Goal: state_coh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts client_state st (client_recv_step (@getSt_client this d C pf) from the_tag (tms_cont tms))) (dstate d)) (consume_msg (dsoup d) m)) *)
(* All receive-transitions *)
Definition lock_receives :=
  [::
     server_recv_acquire_trans;
     server_recv_release_trans;
     client_receive_grant_trans
  ].

Program Definition LockProtocol : protocol :=
  @Protocol _ l _ lock_sends lock_receives _ _.

End Protocol.
End LockProtocol.

Module Exports.
Section Exports.

Definition LockProtocol := LockProtocol.

End Exports.
End Exports.

End LockProtocol.

Export LockProtocol.Exports.
