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

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

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Definition left_inverse {A B : Type} (op: A -> B) (inv : B -> A) :=
  forall x, inv (op x) = x.

Definition fresh_id (xs : seq (nid * nat)) : nat :=
(* Goal: @eq_mem nid (@mem nid (seq_predType (Ordered.eqType (@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)))) (@UMC.dom (@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 (union_mapUMC (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)))) (@mem nat (seq_predType nat_eqType) nodes) *)
(* Goal: forall (n : nid) (_ : is_true (@in_mem nid n (@mem nid (seq_predType (Ordered.eqType (@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)))) (@UMC.dom (@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 (union_mapUMC (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)))))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) *)
   (last 0 (sort oleq (unzip2 xs))).+1.      

Lemma zip_in2 (A B : eqType) (a : A) (b : B) xs:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  (a, b) \in xs -> b \in unzip2 xs.
Proof.
(* Goal: forall _ : is_true (@in_mem (prod (Equality.sort A) (Equality.sort B)) (@pair (Equality.sort A) (Equality.sort B) a b) (@mem (prod (Equality.sort A) (Equality.sort B)) (seq_predType (prod_eqType A B)) xs)), is_true (@in_mem (Equality.sort B) b (@mem (Equality.sort B) (seq_predType B) (@unzip2 (Equality.sort A) (Equality.sort B) xs))) *)
elim:xs=>//x xs Hi; rewrite inE.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case/orP; last by move/Hi=>/=; rewrite inE=>->; rewrite orbC. 
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by case: x=>x y/=/eqP[]Z1 Z2; subst x y; rewrite inE eqxx.
Qed.

Lemma fresh_not_in z xs : (z, fresh_id xs) \notin xs.
Proof.
suff X: ~((z, fresh_id xs) \in xs) by apply/negP.
(* 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), cohMsg msg *)
rewrite /fresh_id=>H.
move: (zip_in2 H)=>{H}X; set ls := (unzip2 xs) in X.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))))) *)
have G: sorted oleq (sort oleq ls).
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- apply: (@sort_sorted [eqType of nat] oleq _).
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
  by rewrite /oleq/=/ord/=; move=>a b; case: ltngtP.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
rewrite -(mem_sort oleq) in X.
(* Goal: @r_step_coh_t (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType nodes x) QCoh rc_wf rtag receive_step *)
move: (sorted_last_key_max 0 G X).
(* Goal: @r_step_coh_t (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType nodes x) QCoh rc_wf rtag receive_step *)
move: (last 0 (sort oleq ls))=>n.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
by rewrite /oleq/=/ord orbC -leq_eqVlt ltnn. 
Qed.

(* Simple protocol for querying a state *)

Module QueryProtocol.
Section  QueryProtocol.

(* Arbitrary data type *)
Variable Data : Type.
Variable nodes : seq nat.

(* Serialize/decerialize functions *)
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Variable serialize : Data -> seq nat.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Variable deserialize : seq nat -> Data.
Hypothesis ds_inverse : left_inverse serialize deserialize.

(* Protocol state *)
Definition st := ptr_nat 1.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Pending requests (client-side): node, request id *)
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Pending responses (server-side): node, response id *)
Definition reqs := seq (nid * nat)%type.
Definition resp := seq (nid * nat)%type.

Definition qstate := (reqs * resp)%type.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* All responses and requests are unique per-node *)
Definition localCoh (n : nid) : Pred heap :=
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  [Pred h | exists (s : qstate), h = st :-> s /\ (uniq s.1 && uniq s.2)].

(* Tags *)
Definition treq : nat := 0.
Definition tresp : nat := 1.
Definition tags := [:: treq; tresp].

Definition cohMsg (ms: msg TaggedMessage) : Prop :=
  let body := content ms in
  (* If a message is a request, it carries a request number *)                                                           
  if tag body == treq then exists req_num, tms_cont body = [:: req_num]
  (* Otherwise it's a response and serialized data *)                                                           
  else exists resp_num sdata, tms_cont body = resp_num :: sdata.

Definition soupCoh : Pred soup :=
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  [Pred s | valid s /\ forall m ms, find m s = Some ms -> cohMsg ms].

Definition qcoh d : Prop :=
  let: dl := dstate d in
  let: ds := dsoup d in
  [/\ soupCoh ds, valid dl, dom dl =i nodes &
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
      forall n, n \in dom dl -> localCoh n (getLocal n d)].

(* Axioms of the coherence predicate *)
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma l1 d: qcoh d -> valid (dstate d).
Proof. by case. Qed.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma l2 d: qcoh d -> valid (dsoup d).
Proof. by case; case. Qed.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma l3 d: qcoh d -> dom (dstate d) =i nodes.
Proof. by case. Qed.

(* Wrapping up the coherence predicate *)
Definition QCoh := CohPred (CohPredMixin l1 l2 l3).

(*********************************************************************)
(**********                Coherence lemmas                  *********)
(*********************************************************************)

Lemma send_soupCoh d m : 
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
    soupCoh (dsoup d) -> cohMsg m -> soupCoh (post_msg (dsoup d) m).1.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
move=>[H1 H2]Cm; split=>[|i ms/=]; first by rewrite valid_fresh.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
rewrite findUnL; last by rewrite valid_fresh.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (if @in_mem (Ordered.sort mid) i (@mem (Equality.sort (Ordered.eqType mid)) (seq_predType (Ordered.eqType mid)) (@UMC.dom mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) (dsoup d))) then @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (dsoup d) else @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup d)) m)) (@Some (msg TaggedMessage) ms), cohMsg ms *)
case: ifP=>E; [by move/H2|by move/findPt_inv=>[Z G]; subst i m].
Qed.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma consume_coh d m : QCoh d -> soupCoh (consume_msg (dsoup d) m).
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
move=>C; split=>[|m' msg]; first by apply: consume_valid; rewrite (cohVs C).
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case X: (m == m');[move/eqP: X=><-{m'}|].
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- case/(find_mark (cohVs C))=>tms[E]->{msg}.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
  by case:(C); case=>_/(_ m tms E).
(* Goal: qcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@receive_step this from (tms_cont tms) d C pf) (dstate d)) (consume_msg (dsoup d) m)) *)
rewrite eq_sym in X.
(* 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), cohMsg msg *)
rewrite (mark_other (cohVs C) X)=>E.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by case:(C); case=>_; move/(_ m' msg E).
Qed.

Lemma trans_updDom this d s :
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  this \in nodes -> QCoh d -> dom (upd this s (dstate d)) =i nodes.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
move=>D C z; rewrite -(cohDom C) domU inE/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
by case: ifP=>///eqP->{z}; rewrite (cohDom C) D; apply: cohVl C.
Qed.

(****************************************************)
(********* Getter lemmas for local state ************)
(****************************************************)

(************** TODO: Refactor this!!! **************)
Lemma cohSt n d (C : QCoh d) s:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  find st (getLocal n d) = Some s ->
  dyn_tp s = qstate.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case: (C)=>_ _ D G; case H: (n \in nodes); rewrite -D in H.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by move:(G _ H); case=>s'[]->_; rewrite findPt//=; case=><-.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
by rewrite /getLocal; case: dom_find H=>//->; rewrite find0E.
Qed.

Definition getSt n d (C : QCoh d) : qstate :=
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  match find st (getLocal n d) as f return _ = f -> _ with
    Some v => fun epf => icast (sym_eq (cohSt C epf)) (dyn_val v)
  | _ => fun epf => ([::], [::])
  end (erefl _).

Lemma getStK n d (C : QCoh d)  s :
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  getLocal n d = st :-> s -> getSt n C = s.
Proof.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by move=>E; rewrite /getSt/=; move: (cohSt C); rewrite !E/==>H; apply: eqc.
Qed.

Lemma getStE n i j C C' (pf : n \in nodes) :
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  getLocal n j = getLocal n i ->
  @getSt n j C' = @getSt n i C.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case: {-1}(C)=>_ _ D G; rewrite -D in pf; move:(G _ pf).
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
by move=>[s][E]_; rewrite (getStK C E) E; move/(getStK C' )->.
Qed.

Lemma getStE' n i j C C' (pf : n \in nodes) :
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  @getSt n j C' = @getSt n i C ->
  getLocal n j = getLocal n i.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case: {-1}(C)=>_ _ D G; rewrite -D in pf; move:(G _ pf).
(* Goal: forall (_ : localCoh n (getLocal n i)) (_ : @eq qstate (@getSt n j C') (@getSt n i C)), @eq Heap.heap (getLocal n j) (getLocal n i) *)
move=>[s][E]_; rewrite (getStK C E) E=>H.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case: {-1}(C')=>_ _ D'/(_ n)=>G'; rewrite D' in G'; rewrite D in pf.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by move/G': pf=>[s'][E']_; rewrite (getStK C' E') in H; subst s'. 
Qed.

(****************************************************)

Notation coh := QCoh.

(*********************
Takes:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- initial state q
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a recipient node to
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a transition tag tag
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a request id to be spent (in the case of response)

Returns 
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a new local state 
**********************)
Definition send_step_fun (q : qstate) (to : nid) (tag : nat) (rid: nat) : qstate :=
  let: (xs, ys) := q in
  if tag == treq then ((to, fresh_id xs) :: xs, ys)
  else if (tag == tresp) && ((to, rid) \in ys)
       then (xs, seq.rem (to, rid) ys)
       else q.

Lemma send_step_uniq q to tag rid:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  uniq q.1 -> uniq q.2 ->
  uniq (send_step_fun q to tag rid).1  /\ uniq (send_step_fun q to tag rid).2.
Proof.
(* Goal: forall (_ : is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@fst (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) q))) (_ : is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@snd (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) q))), and (is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs (list (prod nid nat)) (receive_step_fun q from tag rid)))) (is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs (list (prod nid nat)) (receive_step_fun q from tag rid)))) *)
case: q=>xs ys/= U1 U2; rewrite /send_step_fun; case: ifP=>_/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by rewrite U1 U2; rewrite fresh_not_in.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by case: ifP=>_//=; rewrite U1 rem_uniq //.
Qed.


(*********************
Takes:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- initial state q
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a sender node from
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a transition tag tag
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a request id to be processed (added or removed)

Returns 
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- a new local state 
**********************)
Definition receive_step_fun (q : qstate) (from : nid) (tag : nat) (rid : nat) :=
  let: (xs, ys) := q in
  if (tag == treq) && ((from, rid) \notin ys)
  then (xs, (from, rid) :: ys)
  else if (tag == tresp) && ((from, rid) \in xs)
       then (seq.rem (from, rid) xs, ys)
       else q.

Lemma receive_step_uniq q from tag rid:
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
  uniq q.1 -> uniq q.2 ->
  uniq (receive_step_fun q from tag rid).1  /\
  uniq (receive_step_fun q from tag rid).2.
Proof.
(* Goal: forall (_ : is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@fst (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) q))) (_ : is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@snd (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) (list (Equality.sort (prod_eqType nat_eqType nat_eqType))) q))), and (is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs (list (prod nid nat)) (receive_step_fun q from tag rid)))) (is_true (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs (list (prod nid nat)) (receive_step_fun q from tag rid)))) *)
case: q=>xs ys/= U1 U2; rewrite /receive_step_fun; case: ifP=>B/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by rewrite U1 U2 andbC/=; case/andP:B=>_->.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by case:ifP=>///andP[_ B']/=; rewrite U2 rem_uniq.
Qed.

Section GenericQuerySendTransitions.

Definition Hn this to := this \in nodes /\ to \in nodes.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Definition mkLocal (q : qstate) := st :-> q.

(* Send tag *)
Variable stag : nat.

(* Generic precondition *)

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Variable prec : qstate -> nid -> seq nat -> Prop.

(* Making sure that the precondition is legit *)
Definition prec_safe :=
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
    forall this to q m, Hn this to -> prec q to m ->
                      cohMsg (Msg (TMsg stag m) this to true).

Hypothesis psafe : prec_safe.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Generic send-safety *)
Definition send_safe (this n : nid)
           (d : dstatelet) (msg : seq nat) :=
  Hn this n /\ exists (C : coh d), prec (getSt this C) n msg.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma send_safe_coh this to d m : send_safe this to d m -> coh d.
Proof. by case=>_[]. Qed.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma send_this_in this to : Hn this to -> this \in nodes.
Proof. by case. Qed.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Lemma send_safe_in this to d m : send_safe this to d m ->
                                 this \in nodes /\ to \in nodes.
Proof. by case. Qed.

Definition send_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf : send_safe this to d msg) :=
  let C := send_safe_coh pf in 
  let q := getSt this C in
  Some (mkLocal (send_step_fun q to stag (head 0 msg))). 

Lemma send_step_coh : s_step_coh_t coh stag send_step.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
move=>this to d msg pf h[]->{h}.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))))) *)
have C : (coh d) by case: pf=>?[].
(* 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), cohMsg msg *)
split=>/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- apply: send_soupCoh; first by case:(send_safe_coh pf).
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
  by case: (pf)=>H[C']P/=;move: (psafe H P).
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by rewrite validU; apply: cohVl C.    
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by apply: trans_updDom=>//; case: (send_safe_in pf).
(* Goal: @r_step_coh_t (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType nodes x) QCoh rc_wf rtag receive_step *)
move=>n Ni. rewrite /localCoh/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
rewrite /getLocal/=findU; case: ifP=>B; rewrite domU inE B/= in Ni; last first.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by case: C=>_ _ _/(_ n Ni).  
move/eqP: B=>Z; subst n; rewrite/= (cohVl C)/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
case: (send_safe_in pf); rewrite -(cohDom C)=>D _.
case: C=>_ _ _/(_ this D); case=>q[H/andP[U1 U2]].
exists (send_step_fun (getSt this (send_safe_coh pf)) to stag (head 0 msg)). 
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by split=>//; apply/andP; rewrite (getStK _ H); apply: send_step_uniq.
Qed.

Lemma send_safe_def this to d msg :
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
      send_safe this to d msg <->
      exists b pf, @send_step this to d msg pf = Some b.
Proof.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
split=>[pf/=|]; last by case=>?[]. 
set b := let C := send_safe_coh pf in 
         let q := getSt this C in
         mkLocal (send_step_fun q to stag (head 0 msg)). 
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by exists b, pf. 
Qed.

Definition qsend_trans :=
  SendTrans send_safe_coh send_safe_in send_safe_def send_step_coh.

End GenericQuerySendTransitions.

Definition send_req_prec (q : qstate) (to : nid) (payload : seq nat) :=
  payload = [::(fresh_id q.1)].

(* Making sure that the precondition is legit *)
Lemma send_req_prec_safe : prec_safe treq send_req_prec.
Proof.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by move=>this to q m Hn Hp; rewrite /cohMsg; exists (fresh_id q.1). 
Qed.

Definition send_resp_prec (q : qstate) (to : nid) (payload : seq nat) :=
  exists rid d, payload = rid :: (serialize d) /\
                (to, rid) \in q.2.

Lemma send_resp_prec_safe : prec_safe tresp send_resp_prec.
Proof.
(* Goal: forall (n : nid) (_ : is_true (@in_mem nid n (@mem nid (seq_predType (Ordered.eqType (@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)))) (@UMC.dom (@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 (union_mapUMC (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)))))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) *)
move=>this from q m Hn Hp; rewrite /cohMsg/=.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by case: Hp=>rid[d][H1]H2; exists rid, (serialize d).
Qed.


(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Concrete send-transitions *)
Definition qsend_req  := qsend_trans send_req_prec_safe.
Definition qsend_resp := qsend_trans send_resp_prec_safe.

Section GenericQueryReceiveTransitions.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Send-prepare *)
Variable rtag : nat.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
Variable rc_wf : forall d, coh d -> nid -> nid -> TaggedMessage -> bool.

Definition receive_step : receive_step_t coh :=
  fun this (from : nid) (msg : seq nat) d (pf : coh d) (pt : this \in nodes) =>
    let q := getSt this pf in
    mkLocal (receive_step_fun q from rtag (head 0 msg)).

Lemma receive_step_coh : r_step_coh_t rc_wf rtag receive_step.
Proof.
(* Goal: @r_step_coh_t (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType nodes x) QCoh rc_wf rtag receive_step *)
move=>d from this m C pf tms D F Wf T/=.
(* Goal: qcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@receive_step this from (tms_cont tms) d C pf) (dstate d)) (consume_msg (dsoup d) m)) *)
rewrite /receive_step.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- split=>/=; first by apply: consume_coh.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
  + by rewrite validU; apply: cohVl C.
(* Goal: @eq_mem nid (@mem nid (seq_predType (Ordered.eqType (@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)))) (@UMC.dom (@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 (union_mapUMC (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)))) (@mem nat (seq_predType nat_eqType) nodes) *)
(* Goal: forall (n : nid) (_ : is_true (@in_mem nid n (@mem nid (seq_predType (Ordered.eqType (@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)))) (@UMC.dom (@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 (union_mapUMC (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)))))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) *)
  + by apply: trans_updDom.
(* Goal: qcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@receive_step this from (tms_cont tms) d C pf) (dstate d)) (consume_msg (dsoup d) m)) *)
move=>n Ni; rewrite /localCoh/=.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (dstate d)) (consume_msg (dsoup d) m))) (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
rewrite /getLocal/=findU; case: ifP=>/=B; rewrite domU inE B/= in Ni; last first.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
- by case: (C)=>_ _ _/(_ n Ni).  
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
rewrite Ni; exists (receive_step_fun (getSt this C) from rtag (head 0 tms)).
(* Goal: and (@eq Heap.heap (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) (@heap_pts qstate st (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))))) *)
split=>//; clear Wf.
(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
have X: forall n, n \in dom (dstate d) -> localCoh n (getLocal n d) by case: C.
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))))) *)
case:(X this D)=>q[H/andP[U1 U2]]; rewrite (getStK _ H).
(* Goal: is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms))))) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp (receive_step_fun q from rtag (@head nat O (tms_cont tms)))))) *)
by apply/andP; apply: receive_step_uniq.  
Qed.

Definition qrecv_trans := ReceiveTrans receive_step_coh.

End GenericQueryReceiveTransitions.

Definition query_msg_wf d (C : coh d) (this from : nid) :=
  [pred m : TaggedMessage | (tag m == treq) || (tag m == tresp)].

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Concrete receive-transitions *)
Definition qrecv_req  := qrecv_trans treq query_msg_wf.
Definition qrecv_resp := qrecv_trans tresp query_msg_wf.

Section Protocol.

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* All send-transitions *)
Definition query_sends := [:: qsend_req; qsend_resp ].

(* Goal: @ex qstate (fun s : qstate => and (@eq Heap.heap match @UMC.find nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n (dstate d) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* Goal: @ex qstate (fun s : qstate => and (@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 (mkLocal (receive_step_fun (@getSt this d C) from rtag (@head nat O (tms_cont tms)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts qstate st s)) (is_true (andb (@uniq (prod_eqType nat_eqType nat_eqType) (@fst reqs resp s)) (@uniq (prod_eqType nat_eqType nat_eqType) (@snd reqs resp s))))) *)
(* All receive-transitions *)
Definition query_receives := [:: qrecv_req; qrecv_resp ].

(* Definint quety protocol *)
Program Definition QueryProtocol l : protocol :=
  @Protocol _ l _ query_sends query_receives _ _.

End Protocol.
End QueryProtocol.

Module Exports.
Section Exports.

(*  Tags *)
Definition treq := treq.
Definition tresp := tresp.

Definition getSt := getSt.
Definition getStK := getStK.
Definition getStE := getStE.
Definition getStE' := getStE'.

Definition qsend_req := qsend_req.
Definition qsend_resp := qsend_resp.
Definition qrecv_req := qrecv_req.
Definition qrecv_resp := qrecv_resp.

Definition query_msg_wf := query_msg_wf.
Definition qst := st.

Definition QueryProtocol := QueryProtocol.

End Exports.
End Exports.

End QueryProtocol.

Export QueryProtocol.Exports.
