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

Module CalculatorProtocol.
Section CalculatorProtocol.

Definition input := seq nat.

(* Partially defined function, e.g., 
   addition or multiplication require precisely two arguments *)

Variable f : input -> option nat.
Variable prec : input -> bool.
Hypothesis prec_valid :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  forall i, prec i -> exists v, f i = Some v.

(* Calculator nodes *)
Variable cs: seq nid.
Variable cls : seq nid.
(* All nodes *)
Notation nodes := (cs ++ cls).
(* All nodes are unique *)
Hypothesis Huniq : uniq nodes.

(* Protocol:

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- "Clients" can send messages with requests as long as the request
  satisfies the precondition prec.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- "Clients" can receive messages from "servers" (i.e., calculators).

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- "Servers" can receive messages as long as they satisfy the
  precondition and record the sender and the arguments in the
  permission list.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- "Servers" can respond to clients accordingly, given that the result
  satisfies the arguments.

*)


(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
(* Defining state-space *)

(* Calculator server state *)
Definition st := ptr_nat 1.
(* 
Calculator state: 
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  - client node id
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  - server node id
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  - client-provided id (e.g., hash of the input)
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  - client input
*)

Definition perm := (nid * nat * (seq nat))%type.
Definition cstate := seq perm.

Definition all_valid (s : cstate) := all (fun e => prec e.2) s.

(* Local state coherence *)
Definition localCoh (n : nid) : Pred heap :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  [Pred h | exists (s : cstate), h = st :-> s /\ all_valid s].


(* Tags *)
Definition req : nat := 0.
Definition resp : nat := 1.

Definition tags := [:: req; resp].

(* Coherent messages *)
Definition cohMsg (ms: msg TaggedMessage) : Prop :=
  let body := content ms in
  if tag body == resp then
    [/\ from ms \in cs, to ms \in cls &
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m))) *)
(* Goal: calcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m)) *)
        exists v args, tms_cont body = [:: v] ++ args]
  else [/\ tag body == req,
        from ms \in cls, to ms \in cs &
        exists args,
          tms_cont body = args /\
          prec args].

Definition soupCoh : Pred soup :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  [Pred s | valid s /\ forall m ms, find m s = Some ms -> cohMsg ms].

Definition calcoh d : Prop :=
  let: dl := dstate d in
  let: ds := dsoup d in
  [/\ soupCoh ds, dom dl =i nodes,
   valid dl &
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
   forall n, n \in nodes -> localCoh n (getLocal n d)].

(* Axioms of the coherence predicate *)
Lemma l1 d: calcoh d -> valid (dstate d).
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
Proof. by case. Qed.

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

Lemma l3 d: calcoh d -> dom (dstate d) =i nodes.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
Proof. by case. Qed.

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

(* TODO: This lemma seems very generic, it is exactly the same in TPC.
   Refactor it! *)
Lemma consume_coh d m : CalCoh d -> soupCoh (consume_msg (dsoup d) m).
Proof.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
move=>C; split=>[|m' msg]; first by apply: consume_valid; rewrite (cohVs C).
(* Goal: forall _ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) m' (consume_msg (dsoup d) m)) (@Some (State.msg TaggedMessage) msg), cohMsg msg *)
case X: (m == m');[move/eqP: X=><-{m'}|].
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- case/(find_mark (cohVs C))=>tms[E]->{msg}.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
  by case:(C); case=>_/(_ m tms E).
(* Goal: localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
rewrite eq_sym in X.
(* Goal: @Coherence.sort (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType (@cat nid cs cls) x) CalCoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@fst soup (Ordered.sort mid) (post_msg (dsoup d) (@Msg TaggedMessage (TMsg req msg) this to true)))) *)
rewrite (mark_other (cohVs C) X)=>E.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by case:(C); case=>_; move/(_ m' msg E).
Qed.

Lemma trans_updDom this d s :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  this \in nodes -> CalCoh d -> dom (upd this s (dstate d)) =i nodes.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>D C z; rewrite -(cohDom C) domU inE/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: ifP=>///eqP->{z}; rewrite (cohDom C) D; apply: cohVl C.
Qed.

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

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
Lemma cs_in_nodes n : n \in cs -> n \in nodes.
Proof. by rewrite mem_cat=>->. Qed.

Lemma cohSt n d (C : CalCoh d) s:
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  find st (getLocal n d) = Some s ->
  dyn_tp s = cstate.
Proof.
(* Goal: forall _ : @eq (option (@dynamic Type (fun x : Type => x))) (@UMC.find ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC st (getLocal n d)) (@Some (@dynamic Type (fun x : Type => x)) s), @eq Type (@dyn_tp Type (fun x : Type => x) s) cstate *)
case: (C)=>_ _ _ G; case H: (n \in nodes).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by move:(G _ H); case=>s'[]->_; rewrite findPt//=; case=><-.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
rewrite /getLocal; rewrite -(cohDom C) in H.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: dom_find H=>//->; rewrite find0E.
Qed.

Definition getSt n d (C : CalCoh d) : cstate :=
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  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 : CalCoh d)  s :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  getLocal n d = st :-> s -> getSt n C = s.
Proof.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m))) *)
move=>E; rewrite /getSt/=.
(* Goal: forall (_ : localCoh n (getLocal n i)) (_ : @eq cstate (@getSt n j C') (@getSt n i C)), @eq Heap.heap (getLocal n j) (getLocal n i) *)
move: (cohSt C); rewrite !E/==>H. 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by apply: eqc.
Qed.

Lemma getStE n i j C C' (pf : n \in nodes) :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  getLocal n j = getLocal n i ->
  @getSt n j C' = @getSt n i C.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
case: {-1}(C)=>_ _ _/(_ _ pf).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
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: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  @getSt n j C' = @getSt n i C ->
  getLocal n j = getLocal n i.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
case: {-1}(C)=>_ _ _/(_ _ pf).
(* Goal: forall (_ : localCoh n (getLocal n i)) (_ : @eq cstate (@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: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
case: {-1}(C')=>_ _ _/(_ _ pf)=>[][s'][E']_.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by rewrite (getStK C' E') in H; subst s'. 
Qed.

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

Notation coh := CalCoh.

(*** Server Transitions ***)

Section ServerReceiveTransition.

Definition sr_wf d (_ : coh d) (this from : nid) msg :=
  prec msg.

Definition sr_step : receive_step_t coh :=
  fun this (from : nid) (m : seq nat) d (pf : coh d) (pt : this \in nodes) =>
    if this \in cs
    then let s := getSt this pf in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
         st :-> ((from, this, m) :: s)
    else getLocal this d.

(* This looks extremely similar to TPC, so, perhaps this should be
   refactored as well. *)
Lemma sr_step_coh : r_step_coh_t sr_wf req sr_step.
Proof.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>d from this m C pf tms D F Wf T/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /sr_step; case X: (this \in cs); last first.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m))) *)
(* Goal: calcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by apply: trans_updDom.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m))) *)
(* Goal: calcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by rewrite validU; apply: cohVl C.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  by move=>n Ni/=; case: (C)=>_ _ _/(_ n Ni)=>L; rewrite -(getLocalU)// (cohVl C).
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by apply: trans_updDom.  
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by rewrite validU; apply: cohVl C.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m))) *)
move=>n Ni/=; rewrite /localCoh/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /getLocal/=findU; case: ifP=>B/=; last by case: (C)=>_ _ _/(_ n Ni). 
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap match (if andb (@pred_of_simpl (Ordered.sort nat_ordType) (@UMC.cond nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) this) (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d)) then @Some Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts cstate st s)) (is_true (all_valid s))) *)
move/eqP: B X=>Z/eqP X; subst n; rewrite (cohVl C)/=.
(* Goal: is_true (all_valid (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) *)
have Y: all_valid (getSt this C).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: {-1}(C)=>_ _ _/(_ _ pf)[]s[]/(getStK C)->.
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (@heap_pts cstate st s)) (is_true (all_valid s))) *)
exists ((from, this, tms_cont tms) :: (getSt this C)); split=>//. 
(* Goal: is_true (all_valid (@cons (prod (prod nat nid) (list nat)) (@pair (prod nat nid) (list nat) (@pair nat nid from this) (tms_cont tms)) (@getSt this d C))) *)
rewrite /all_valid/= in Y *; rewrite Y.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by rewrite /sr_wf in Wf; rewrite Wf.
Qed.

Definition server_recv_trans := ReceiveTrans sr_step_coh.

End ServerReceiveTransition.

Section ServerSendTransition.

Definition entry_finder (to : nid) msg :=
  let: ans := head 0 msg in
  fun e : perm => 
    let: (n, _, args) := e in
    [&& n == to, f args == Some ans &
        msg == ans :: args].

Definition can_send (s : cstate) to msg :=
  has (entry_finder to msg) s.

Definition ss_safe (this to : nid)
           (d : dstatelet) (msg : seq nat) :=
  to \in cls /\ this \in cs /\
  exists (C : coh d), 
  has (entry_finder to msg) (getSt this C).         

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
Lemma ss_safe_coh this to d m : ss_safe this to d m -> coh d.
Proof. by case=>_[]_[]. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
Lemma ss_safe_in this to d m : ss_safe this to d m ->
                             this \in nodes /\ to \in nodes.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by rewrite !mem_cat; case=>->[->]_; split=>//; rewrite orbC.
Qed.

Lemma ss_safe_this this to d m :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  ss_safe this to d m -> this \in cs.
Proof. by case=>_[?][]. Qed.

Definition ss_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf : ss_safe this to d msg) :=
  let C := ss_safe_coh pf in 
  let s := getSt this C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  Some (st :-> remove_elem s (to, this, (behead msg))).

Lemma ss_step_coh : s_step_coh_t coh resp ss_step.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>this to d msg pf h[]->{h}.
(* Goal: is_true (all_valid (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) *)
have C : (coh d) by case: pf=>?[_][].
(* Goal: @Coherence.sort (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType (@cat nid cs cls) x) CalCoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@fst soup (Ordered.sort mid) (post_msg (dsoup d) (@Msg TaggedMessage (TMsg req msg) this to true)))) *)
split=>/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- split=>[|i ms/=]; first by rewrite valid_fresh (cohVs C).
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
  rewrite findUnL; last by rewrite valid_fresh (cohVs C). 
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
  case: ifP=>E; first by case: C=>[[Vs]]H _ _ _; move/H.
(* Goal: forall _ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))) (@Some (State.msg TaggedMessage) ms), cohMsg ms *)
(* 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 (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)))) (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)) *)
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  move/findPt_inv=>[Z G]; subst i ms.
  split; rewrite ?(proj2 (ss_safe_in pf))?(ss_safe_this pf)//.
  case: pf=>?[C'][tf]/hasP[]=>[[[n]]]h args
             _/andP[/eqP]Z1/andP[/eqP Z2]/eqP Z3//=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  case: pf=>[_][_][C']/hasP[[[x1] x2]]x3 H/andP[Z1]/andP[Z2]/eqP->.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
  by exists (head 0 msg), x3. 
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- move=>z.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  move: (getSt this (ss_safe_coh pf) )=>G.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  rewrite -(cohDom C) domU inE/= (cohVl C).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  by case: ifP=>///eqP->{z}; rewrite (cohDom C)(proj1 (ss_safe_in pf)). 
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by rewrite validU; apply: cohVl C.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>n Ni. rewrite /localCoh/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /getLocal/=findU; case: ifP=>B/=; last by case: C=>_ _ _/(_ n Ni). 
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap match (if andb (@pred_of_simpl (Ordered.sort nat_ordType) (@UMC.cond nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) this) (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d)) then @Some Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts cstate st s)) (is_true (all_valid s))) *)
move/eqP: B=>Z; subst n; rewrite (cohVl C).
exists (remove_elem (getSt this (ss_safe_coh pf)) (to, this, behead msg)).
split=>//; apply: remove_elem_all.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: {-1}(ss_safe_coh pf)=>_ _ _/(_ _ Ni)[]s[]/(getStK (ss_safe_coh pf))->.
Qed.

Lemma ss_safe_def this to d msg :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
      ss_safe this to d msg <->
      exists b pf, @ss_step this to d msg pf = Some b.
Proof.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
split=>[pf/=|]; last by case=>?[]. 
set b := let C := ss_safe_coh pf in 
         let s := getSt this C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
         st :-> remove_elem s (to, this, (behead msg)).
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by exists b, pf. 
Qed.

Definition server_send_trans :=
  SendTrans ss_safe_coh ss_safe_in ss_safe_def ss_step_coh.

End ServerSendTransition.

(**************************)
(*** Client transitions ***)
(**************************)

Section ClientSendTransition.

Definition cs_safe (this to : nid)
           (d : dstatelet) (msg : seq nat) :=
  [/\ to \in cs, this \in cls, coh d & prec msg].         

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
Lemma cs_safe_coh this to d m : cs_safe this to d m -> coh d.
Proof. by case=>_[]. Qed.

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
Lemma cs_safe_in this to d m : cs_safe this to d m ->
                             this \in nodes /\ to \in nodes.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by rewrite !mem_cat; case=>->->/=_ _; split=>//; rewrite orbC. 
Qed.

Definition cs_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf : cs_safe this to d msg) :=
  let C := cs_safe_coh pf in 
  let s := getSt this C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  Some (st :-> ((this, to, msg)::s)).


Lemma cs_step_coh : s_step_coh_t coh req cs_step.
Proof.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>this to d msg pf h[]->{h}.
(* Goal: is_true (all_valid (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) *)
have C : (coh d) by case: pf=>?[].
(* Goal: @Coherence.sort (fun (_ : dstatelet) (x : Equality.sort nat_eqType) => @pred_of_eq_seq nat_eqType (@cat nid cs cls) x) CalCoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@fst soup (Ordered.sort mid) (post_msg (dsoup d) (@Msg TaggedMessage (TMsg req msg) this to true)))) *)
split=>/=.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- split=>[|i ms/=]; first by rewrite valid_fresh (cohVs C).
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
  rewrite findUnL; last by rewrite valid_fresh (cohVs C). 
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
  case: ifP=>E; first by case: C=>[[Vs]]H _ _ _; move/H.
(* Goal: forall _ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))) (@Some (State.msg TaggedMessage) ms), cohMsg ms *)
(* 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 (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)))) (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)) *)
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  move/findPt_inv=>[Z G]; subst i ms.
  split=>//; rewrite ?(proj2 (cs_safe_in pf));
  rewrite ?(proj2 (cs_safe_in pf))?(cs_safe_this pf)//=;
  by case: pf=>// _ _ _; exists msg.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- move=>z; move: (getSt this (cs_safe_coh pf))=>G.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  rewrite -(cohDom C) domU inE/= (cohVl C).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  by case: ifP=>///eqP->{z}; rewrite (cohDom C)(proj1 (cs_safe_in pf)). 
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by rewrite validU; apply: cohVl C.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>n Ni. rewrite /localCoh/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /getLocal/=findU; case: ifP=>B; last by case: C=>_ _ _/(_ n Ni). 
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap match (if andb (@pred_of_simpl (Ordered.sort nat_ordType) (@UMC.cond nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) this) (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d)) then @Some Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts cstate st s)) (is_true (all_valid s))) *)
move/eqP: B=>Z; subst n; rewrite (cohVl C)/=.
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (@heap_pts cstate st s)) (is_true (all_valid s))) *)
exists ((this, to, msg) :: getSt this (cs_safe_coh pf)); split=>//.
(* Goal: is_true (all_valid (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) *)
have Y: all_valid (getSt this (cs_safe_coh pf)).
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: {-1}(cs_safe_coh pf)=>_ _ _/(_ _ Ni)[]s[]/(getStK (cs_safe_coh pf))->.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by rewrite /=Y andbC/=; case: (pf).
Qed.

Lemma cs_safe_def this to d msg :
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
      cs_safe this to d msg <->
      exists b pf, @cs_step this to d msg pf = Some b.
Proof.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
split=>[pf/=|]; last by case=>?[]. 
set b := let C := cs_safe_coh pf in 
         let s := getSt this C in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
         st :-> ((this, to, msg)::s).
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option Heap.heap) (@cs_step this to d msg pf) (@Some Heap.heap b))) *)
by exists b, pf. 
Qed.

Definition client_send_trans :=
  SendTrans cs_safe_coh cs_safe_in cs_safe_def cs_step_coh.

End ClientSendTransition.

Section ClientReceiveTransition.

Definition cr_wf d (C : coh d) this from (msg : seq nat) :=
  let s := getSt this C in
  let: args := (behead msg) in
  [&& (this, from, args) \in s &
     size msg > 2].

Definition cr_step : receive_step_t coh := 
  fun this (from : nid) (m : seq nat) d (pf : coh d) (pt : this \in nodes) =>
    let s := getSt this pf : seq perm in
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
    st :-> remove_elem s (this, from, (behead m) : seq nat).

Lemma cr_step_coh : r_step_coh_t cr_wf resp cr_step.
Proof.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
move=>d from this m C pf tms D F Wf T/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /sr_step; case X: (this \in cs); last first.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m))) *)
(* Goal: calcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by apply: trans_updDom.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (getLocal this d) (dstate d)) (consume_msg (dsoup d) m))) *)
(* Goal: calcoh (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m)) *)
  + by rewrite validU; apply: cohVl C.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m))) *)
  move=>n Ni/=; rewrite /localCoh/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
  rewrite /getLocal/=findU; case: ifP=>B/=; last by case: (C)=>_ _ _/(_ n Ni). 
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap match (if andb (@pred_of_simpl (Ordered.sort nat_ordType) (@UMC.cond nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) this) (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d)) then @Some Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts cstate st s)) (is_true (all_valid s))) *)
  move/eqP: B X=>Z/eqP X; subst n; rewrite (cohVl C)/=.
  exists (remove_elem (getSt this C) (this, from, behead tms)).  
  split=>//; apply: remove_elem_all.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
  by case: {-1}(C)=>_ _ _/(_ _ Ni)[]s[]/(getStK (C))->.  
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
split=>/=; first by apply: consume_coh.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by apply: trans_updDom.  
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
- by rewrite validU; apply: cohVl C.
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from this) (tms_cont tms)) (@getSt this d C))) (dstate d)) (consume_msg (dsoup d) m))) *)
move=>n Ni/=; rewrite /localCoh/=.
(* Goal: iff (cs_safe this to d msg) (@ex (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (fun b : @UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC => @ex (cs_safe this to d msg) (fun pf : cs_safe this to d msg => @eq (option (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@cs_step this to d msg pf) (@Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) b)))) *)
rewrite /getLocal/=findU; case: ifP=>B/=; last by case: (C)=>_ _ _/(_ n Ni). 
(* Goal: @ex cstate (fun s : cstate => and (@eq Heap.heap match (if andb (@pred_of_simpl (Ordered.sort nat_ordType) (@UMC.cond nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) this) (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) (dstate d)) then @Some Heap.heap (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) else @None Heap.heap) with | Some h => h | None => @PCM.unit heapPCM end (@heap_pts cstate st s)) (is_true (all_valid s))) *)
move/eqP: B X=>Z/eqP X; subst n; rewrite (cohVl C)/=.
exists (remove_elem (getSt this C) (this, from, behead tms)).  
split=>//; apply: remove_elem_all.
(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
by case: {-1}(C)=>_ _ _/(_ _ Ni)[]s[]/(getStK (C))->.  
Qed.

Definition client_recv_trans := ReceiveTrans cr_step_coh.

End ClientReceiveTransition.


Section Protocol.

Variable l : Label.

Definition cal_sends :=    [:: server_send_trans; client_send_trans].
Definition cal_receives := [:: server_recv_trans; client_recv_trans].

Program Definition CalculatorProtocol : protocol :=
  @Protocol _ l _ cal_sends cal_receives _ _.

End Protocol.
End CalculatorProtocol.

Module Exports.

Definition CalculatorProtocol := CalculatorProtocol.

Definition CalCoh := CalCoh.

Definition server_send_trans := server_send_trans.
Definition server_recv_trans := server_recv_trans.
Definition client_send_trans := client_send_trans.
Definition client_recv_trans := client_recv_trans.

Definition req := req.
Definition resp := resp.
Notation input := (seq nat).
Definition cstate := cstate.

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

End Exports.

End CalculatorProtocol.

(**************************************************)
(*
Overall Implementation effort:

(* Goal: is_true (@PCM.valid (union_mapPCM (@Ordered.clone nid nat_ordType (@Ordered.Class nat nat_eqMixin nat_ordMixin) (fun x : phantom (Ordered.class_of nat) (@Ordered.Class nat nat_eqMixin nat_ordMixin) => x)) Heap.heap) (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d))) *)
(* Goal: forall (n : nat) (_ : is_true (@in_mem nat n (@mem nat (seq_predType nat_eqType) (@cat nid cs cls)))), localCoh n (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) this (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid this to) msg) (@getSt this d (@cs_safe_coh this to d msg pf)))) (dstate d)) (@PCM.join (union_mapPCM mid (State.msg TaggedMessage)) (dsoup d) (@um_pts nat_ordType (State.msg TaggedMessage) (@fresh (State.msg TaggedMessage) (dsoup d)) (@Msg TaggedMessage (TMsg req msg) this to true))))) *)
4 person-hours

*)
(**************************************************)
 
Export CalculatorProtocol.Exports.
