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

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

(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
(* The Hello World example - a distributed protocol, allowing anyone send
anyone a greeting message. *)

Module GreeterProtocol.
Section GreeterProtocol.


Variable fixed_nodes : seq nid.

Section GreeterCoh.

(* All nodes are welcome to participate in the protocol *)
Definition nodes (d : dstatelet) : pred nid := mem fixed_nodes.

(* Defining coherence predicate for the greeter statelet *)

Definition hello := [:: 3; 1; 1; 0].
Definition counter := ptr_nat 1.

(* All messages have fixed shape *)
Definition soupCoh : Pred soup :=
  [Pred s | valid s /\
            forall m msg,
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
              find m s = Some msg ->
              let: from := from msg in
              let: tag := tag (content msg) in
              let: val := tms_cont (content msg) in
              [/\ from \in fixed_nodes, 
                  tag == 0 & behead val == hello]].

(* Coherence for the local state ensures that is has just one counter,
   which we will later use to count incoming messages  *)
Definition localCoh : Pred heap :=
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  [Pred h | exists n : nat, h = counter :-> n].

(* Overall coherence *)
Definition greeter_coh d : Prop :=
  let: dl := dstate d in
  let: ds := dsoup d in
  [/\ soupCoh ds, dom dl =i fixed_nodes,
   valid dl &
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
   forall n, n \in fixed_nodes -> localCoh (getLocal n d)].

(* Axioms of the coherence predicate *)
Lemma l1 d: greeter_coh d -> valid (dstate d).
(* Goal: hook_complete (W l nodes) *)
Proof. by case. Qed.

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

Lemma l3 d: greeter_coh d -> dom (dstate d) =i nodes d.
(* Goal: hook_complete (W l nodes) *)
Proof. by case. Qed.

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

Section GreeterSend.

Section SendBase.

Notation coh := GreeterCoh.

(* Defining send and receive transitions *)
Definition greet_safe (this n : nid) (d : dstatelet) msg :=
  [/\ this \in fixed_nodes,
      n \in fixed_nodes,
      exists m, msg == m :: hello &
      coh d].

Section GreetAux.

Variables (this : nid) (d : dstatelet)
          (C : coh d).

Lemma lcoh n : n \in fixed_nodes -> localCoh (getLocal n d).
Proof. by move=> H; case: C => _ _ _/(_ n H). Qed.

Lemma cohN n v :
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  n \in fixed_nodes ->
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  find counter (getLocal n d) = Some v ->
  dyn_tp v = nat.
Proof. by move=>H; case: (lcoh H)=>m->; rewrite findPt /=; case=><-. Qed.

Definition getN n (pf : n \in fixed_nodes) : nat := 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  match find counter (getLocal n d) as f return _ = f -> _ with
    Some v => fun epf => icast (sym_eq (cohN pf epf)) (dyn_val v)
  | None => fun epf => 0
  end (erefl _).

Lemma getNK n (Hn : n \in fixed_nodes) m:
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  getLocal n d = counter :-> m -> getN Hn = m.
Proof.
(* Goal: forall _ : @eq Heap.heap (getLocal n d) (@heap_pts nat counter m), @eq nat (@getN n Hn) m *)
move=>E; rewrite /getN; move: (cohN)=>H.
(* Goal: hook_complete (W l nodes) *)
by move: (H n)=>{H}; rewrite E=>H/=; apply: eqc.
Qed.

End GreetAux.

Lemma this_in_pf this to d msg :
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  greet_safe this to d msg -> this \in fixed_nodes.
(* Goal: hook_complete (W l nodes) *)
Proof. by case. Qed.

Lemma greet_safe_coh this to d m : greet_safe this to d m -> coh d.
(* Goal: hook_complete (W l nodes) *)
Proof. by case. Qed.

Definition greet_step (this to : nid) (d : dstatelet)
           (msg : seq nat)
           (pf: greet_safe this to d msg)
  : option heap :=
  if (behead msg == hello) && (to \in fixed_nodes)
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  then Some (counter :-> (getN (greet_safe_coh pf) (this_in_pf pf)).+1)
  else None.
 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
Lemma greet_safe_in this to d m : greet_safe this to d m ->
                                  this \in nodes d /\ to \in nodes d.
(* Goal: hook_complete (W l nodes) *)
Proof. by case. Qed.

Lemma greet_safe_def this to d msg :
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
      greet_safe this to d msg <->
      exists b pf, @greet_step this to d msg pf = Some b.
Proof.
(* Goal: iff (greet_safe this to d msg) (@ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b)))) *)
split=>[H|].
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- exists (counter :-> (getN (greet_safe_coh H) (this_in_pf H)).+1), H.
(* Goal: @eq (option Heap.heap) (@greet_step this to d msg H) (@Some Heap.heap (@heap_pts nat counter (S (@getN d (@greet_safe_coh this to d msg H) this (@this_in_pf this to d msg H))))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  rewrite/greet_step; case: (H)=>H1 H2 H3 H4.
(* Goal: @eq (option Heap.heap) (if andb (@eq_op (seq_eqType nat_eqType) (@behead nat msg) hello) (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes)) then @Some (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts nat counter (S (@getN d (@greet_safe_coh this to d msg (@And4 (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (@ex nat (fun m : nat => is_true (@eq_op (seq_eqType nat_eqType) msg (@cons nat m hello)))) (@Coherence.sort nodes GreeterCoh d) H1 H2 H3 H4)) this (@this_in_pf this to d msg (@And4 (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (@ex nat (fun m : nat => is_true (@eq_op (seq_eqType nat_eqType) msg (@cons nat m hello)))) (@Coherence.sort nodes GreeterCoh d) H1 H2 H3 H4))))) else @None (@UMC.sort ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@Some Heap.heap (@heap_pts nat counter (S (@getN d (@greet_safe_coh this to d msg (@And4 (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (@ex nat (fun m : nat => is_true (@eq_op (seq_eqType nat_eqType) msg (@cons nat m hello)))) (@Coherence.sort nodes GreeterCoh d) H1 H2 H3 H4)) this (@this_in_pf this to d msg (@And4 (is_true (@in_mem nid this (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (is_true (@in_mem nid to (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) fixed_nodes))) (@ex nat (fun m : nat => is_true (@eq_op (seq_eqType nat_eqType) msg (@cons nat m hello)))) (@Coherence.sort nodes GreeterCoh d) H1 H2 H3 H4)))))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  move: (And4 H1 H2 H3 H4)=>C; rewrite H2; case: H3=>m H3.
(* Goal: hook_complete (W l nodes) *)
  by move/eqP: H3=>H3; subst msg=>/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
by case=>h[pf]; rewrite/greet_step; case:ifP=>///andP[/eqP->H]_; split.
Qed.

Definition greet_tag := 0.

(* We might need to put this statement into a separate definition *)
Lemma greet_step_coh this to d msg (pf : greet_safe this to d msg) b :
  let: f := dstate d in
  let: s := dsoup d  in
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  Some b = greet_step pf ->         
  let: f' := upd this b f in
  let: tms := TMsg greet_tag msg in 
  let: s' := (post_msg s (Msg tms this to true)).1 in 
  coh (DStatelet f' s').
Proof.
rewrite/greet_step; case:ifP=>///andP[/eqP Z1 H][]Z'; subst b=>/=.
case:pf=>[F1]F2 F3 [Cs D]Cl Cn.
split=>//=; do?[by rewrite validU/=].
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- split; first by rewrite valid_fresh; case: Cs.
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
  move=>m msg'; rewrite findUnR ?domPt ?inE ?valid_fresh; last by case: Cs.
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
  case: ifP=>[/eqP Z|_]; last by case: Cs=>_ Cs; move/Cs.
  case:F3=>[m']/eqP E; subst msg.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  by subst m; rewrite findPt/=; case=><-.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- move=>n; rewrite domU inE/=; case: ifP=>[/eqP Z| _]//; subst n.
(* Goal: hook_complete (W l nodes) *)
  by rewrite Cl F1.
move: (And4 F1 F2 F3 (And4 Cs D Cl Cn)) => S.
move=>n Hn; exists (if n == this
                    then (getN (greet_safe_coh S) (this_in_pf S)).+1
                    else (getN (greet_safe_coh S) Hn)); rewrite /getLocal/=.
(* Goal: @eq (option Heap.heap) (@greet_step this to d msg H) (@Some Heap.heap (@heap_pts nat counter (S (@getN d (@greet_safe_coh this to d msg H) this (@this_in_pf this to d msg H))))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
rewrite findU; case Z: (n == this)=>/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- by move/eqP: Z=>Z; subst n; move: (And4 Cs D Cl Cn)=>C; rewrite Cl.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
case: (Cn n Hn)=>m E; move: (E); rewrite /getLocal=>->; congr (_ :-> _).
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
by move: (getNK (greet_safe_coh S) Hn E)=><-.
Qed.

End SendBase.

(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
(*  Defined the send-transition of the greeter  *)
Definition greeter_send_trans :=
  SendTrans greet_safe_coh greet_safe_in greet_safe_def greet_step_coh.

End GreeterSend.

Variable l : Label.

(* Defining the protocol *)
Program Definition GreeterProt : protocol :=
  @Protocol _ l _ [:: greeter_send_trans] [::] _ _.

End GreeterProtocol.

Module Exports.
Section Exports.

Definition getN := getN.
Definition getNK := getNK.
Definition GreeterProtocol := GreeterProt.
Definition gsend := greeter_send_trans.
Definition hello := hello.
Definition counter := counter.
Definition greet_safe_coh := greet_safe_coh.

End Exports.
End Exports.

End GreeterProtocol.

Export GreeterProtocol.Exports.

Section GreeterPrograms.

Variable l : Label.
Variable nodes : seq nid.

Definition gp := GreeterProtocol nodes l.

(* Simplest world with one protocol *)
(* TODO: simplify this using canonicals *)
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
Definition W : world := (l \\-> gp, Unit).

Variable this : nid.

Lemma grEq : (getProtocol W l) = gp.
Proof. by rewrite /getProtocol findPt. Qed.

(* Defining an action for greeting on top of the corresponding transition *)
(* Sends and argument number and a suffix *)
Program Definition greet_act n :=
  @send_action_wrapper W gp this l grEq (gsend nodes) _ (n :: hello).
Next Obligation. by rewrite InE. Qed.

Hypothesis P1 : this \in nodes.

Program Definition read_act :=
  @skip_action_wrapper W this l gp grEq nat (fun s pf => getN pf P1).

Notation loc i := (getLocal this (getStatelet i l)).
Notation msgs i := (dsoup (getStatelet i l)).

Definition greeter_spec to :=
  {n : nat}, DHT [this, W]
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  (fun i => loc i = counter :-> n /\ to \in nodes,
   fun r m => 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
       [/\ loc m = counter :-> n.+1, 
        head 0 r = n &
        exists z b, find z (msgs m) = Some (Msg (TMsg 0 (n :: hello)) this to b)]).

Program Definition greet to : greeter_spec to :=
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  Do (n <-- act read_act;
      act (greet_act n to)).

Next Obligation.
(* Goal: iff (greet_safe this to d msg) (@ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b)))) *)
apply ghC=>s1 n [Hloc] Hto C1.

apply: step.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- apply: act_rule. 
  move=> s2 R1.
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
  split; first by move: R1=> /rely_coh[]; rewrite /read_act/=/Actions.skip_safe. 
  move=> y s2' s3 [Sf1]/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  rewrite /Actions.skip_step => -[] C2 ? ? R2; subst s2'; subst.

(* Applying inference rule for actions *)
apply: act_rule=>s4 R3.
(* Dealing with rely *)

(* Proving the precondition *)
(* Goal: iff (greet_safe this to d msg) (@ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b)))) *)
split=>[|r s5 s6 [Sf2] St R4].
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- split; case/rely_coh: R3=>C3 C4=>//.
  + split=>//; first by eauto.
(* Goal: hook_complete (W l nodes) *)
    by case: C4=>_ _ _ _/(_ l); rewrite grEq.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  + by apply/andP; split=>//; move: (cohD C4)=><-; rewrite domPt inE; apply/eqP.
  move=>???/=.
  move => F.
  apply sym_eq in F.
  move: F.
(* Goal: hook_complete (W l nodes) *)
  by move/find_some; rewrite /Actions.filter_hooks umfilt0 dom0.
(*Bookkeeping for the postconidtion *)
case: St=>Z1[h]/=[St]Z2; subst.

(* Making use of the stepping relation *)
rewrite /GreeterProtocol.greet_step/= Hto in St; case: St=>Z'; subst h.
(* Rewriting the state getter *)
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
erewrite !getNK in R4; first last. 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- by rewrite (rely_loc' l R3) (rely_loc' l R2) (rely_loc' l R1); exact: Hloc.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- by rewrite (rely_loc' l R1); exact: Hloc.
(* rewriting via rely *)
case/rely_coh: (R3)=>C3 C4.
(* Goal: hook_complete (W l nodes) *)
erewrite getNK; last by rewrite (rely_loc' l R1); exact: Hloc.
rewrite (rely_loc' l R4); split=>//.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- rewrite /getLocal/getStatelet findU eqxx/= (cohS C4)/= findU eqxx/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  rewrite getsE /=; last by rewrite -(cohD C4) domPt inE; apply/eqP.
(* Goal: hook_complete (W l nodes) *)
  by rewrite (cohVl (coh_coh l C4)).

(* Reasoning about message soup *)
exists (fresh (msgs s4)).
case: (rely_send_other' R4 (m := fresh (msgs s4)) (l := l)
                        (tm := {| tag := GreeterProtocol.greet_tag; tms_cont := n :: hello |})
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
                        (to := to) (b := true)); last by move=>b[->]/= _; exists b.
rewrite /getStatelet findU eqxx/= (cohS C4)/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
rewrite getsE /=; last by rewrite -(cohD C4) domPt inE; apply/eqP.
rewrite joinC findPtUn // joinC valid_fresh.
(* Goal: hook_complete (W l nodes) *)
by apply: (cohVs (coh_coh l C4)).
Qed.

Definition greeter_spec2 n to :=
  DHT [this, W]
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  (fun i => loc i = counter :-> n /\ to \in nodes, 
   fun r m =>
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
     loc m = counter :-> n.+2 /\ head 0 r = n.+1).


Program Definition greet2 n to : greeter_spec2 n to :=
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  Do (r <-- greet to;
      greet to).

Next Obligation.
move=>i/=[H1 H2].
(* Switch to the continuation *)
apply: step.
apply: (gh_ex (g := n)); apply: call_rule=>//.
move=>? j[Hcount Hhead _] Cj.
apply: (gh_ex (g := n.+1)); apply: call_rule=>//.
(* Goal: hook_complete (W l nodes) *)
by move=>r m[X1 X2 _]. 
Qed.

End GreeterPrograms.


Section CombineGreeters.

Variables (l1 l2 : Label) (nodes : seq nid) (this : nid).
Variable (lab_disj : l2 != l1).

Definition gp1 := GreeterProtocol nodes l1.
Definition gp2 := GreeterProtocol nodes l2.


Definition V := (W l1 nodes) \+ (W l2 nodes).

Lemma validV : valid V.
Proof.
(* Goal: is_true (@PCM.valid (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) V) *)
rewrite /V; apply/andP=>/=.
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
split; first by rewrite validPtUn/= validPt/= domPt inE/=.
(* Goal: hook_complete (W l nodes) *)
by rewrite unitR valid_unit.
Qed.

Notation loc i k := (getLocal this (getStatelet i k)).
Notation msgs i k := (dsoup (getStatelet i k)).

Hypothesis T : this \in nodes.


Definition greet_prog1 := greet2 l1 T.
Definition greet_prog2 := greet2 l2 T.

Definition greeter_spec3 n1 n2 to :=
  DHT [this, V]
  (fun i =>
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
     [/\ loc i l1 = counter :-> n1,
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
      loc i l2 = counter :-> n2 &
      to \in nodes], 
   fun r m =>
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
     [/\ loc m l1 = counter :-> n1.+2,
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
      loc m l2 = counter :-> n2.+2 &
      r = n1 + n2 + 2]).

Lemma hook_complete_unit (c : context) : hook_complete (c, Unit).
Proof. by move=>????; rewrite dom0. Qed.

Lemma hooks_consistent_unit (c : context) : hooks_consistent c Unit.
Proof. by move=>????; rewrite dom0. Qed.

Program Definition greet3 n1 n2 to : greeter_spec3 n1 n2 to :=
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
  Do (r1 <-- iinject (greet_prog1 n1 to);
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
      r2 <-- iinject (greet_prog2 n2 to);
      ret _ _ (head 0 r1 + head 0 r2)).

Next Obligation. exact Unit. Defined.
Next Obligation. 
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
rewrite -(unitR V)/V.
have V: valid (W l1 nodes \+ W l2 nodes \+ Unit) by rewrite unitR validV.
apply: (injectL V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
(* Goal: hook_complete (W l nodes) *)
by move=>??????; rewrite dom0.
Qed.
Next Obligation. exact Unit. Defined.
Next Obligation.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
rewrite -(unitR V)/V.
have V: valid (W l1 nodes \+ W l2 nodes \+ Unit) by rewrite unitR validV.
apply: (injectR V); do?[apply: hook_complete_unit | apply: hooks_consistent_unit].
(* Goal: hook_complete (W l nodes) *)
by move=>??????; rewrite dom0.
Defined.

Lemma hcomp l : hook_complete (W l nodes).
Proof. by move=>????; rewrite dom0. Qed.

Next Obligation.
move=>i/=[H1]H2 N.
apply: vrf_coh=>C.
apply: step.
move: (coh_split C (@hcomp l1) (@hcomp l2))=>[i1[j1]][C1 C2 Z]; subst i.
apply: inject_rule=>//.
have E1 : loc (i1 \+ j1) l1 = loc i1 l1
  by rewrite (locProjL C _ C1)// domPt inE/=.
(* Goal: is_true (@PCM.valid (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) V) *)
rewrite E1 in H1; apply: call_rule=>// r1 m1 [Q1 Z1] C1' j' C' R1.
have E2 : loc (i1 \+ j1) l2 = loc j1 l2.
(* Goal: hook_complete (W l nodes) *)
  by rewrite (locProjR C _ C2)// domPt inE/=.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
rewrite E2 -(rely_loc' l2 R1) in H2.
apply: step.
(* Goal: is_true (@PCM.valid (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) V) *)
rewrite joinC; apply: inject_rule.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- case: (rely_coh R1)=>/= _.
(* Goal: hook_complete (W l nodes) *)
  by rewrite injExtL//(cohW C). 
apply: call_rule=>//r2 m2 [E3]Z2 C3 j'' C3' R2.
(* Goal: and (is_true (@PCM.valid (union_mapPCM Label protocol) (@PCM.join (union_mapPCM Label protocol) (@um_pts Label protocol l1 (gp l1 nodes)) (@um_pts Label protocol l2 (gp l2 nodes))))) (is_true (@PCM.valid (union_mapPCM hook_domain hook_type) (@PCM.join (union_mapPCM hook_domain hook_type) (@PCM.unit (union_mapPCM hook_domain hook_type)) (@PCM.unit (union_mapPCM hook_domain hook_type))))) *)
apply: ret_rule=>m3 R3[G1]G2 G3; split; last first.
(* Playing with locality of transitions, propagating once obtained
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
   results from intermediate states to the post-state. *)
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- by rewrite Z1 Z2 -[_.+1]addn1 -[n2.+1]addn1
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
             addnAC !addnA !addn1 -addn2.
(* Goal: @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))) *)
(* Goal: forall _ : @ex Heap.heap (fun b : Heap.heap => @ex (greet_safe this to d msg) (fun pf : greet_safe this to d msg => @eq (option Heap.heap) (@greet_step this to d msg pf) (@Some Heap.heap b))), greet_safe this to d msg *)
- rewrite (rely_loc' l2 R3) joinC; rewrite joinC in C3'.
(* Goal: hook_complete (W l nodes) *)
  by rewrite (locProjR C3' _ C3)// domPt inE/=.
rewrite (rely_loc' l1 R3).
move/rely_coh: (R2)=>[]; rewrite injExtR ?(cohW C)// =>_ C5.
rewrite joinC in C3' *.
rewrite (locProjL C3' _ C5)//?/ddom ?domPt ?inE//=.
(* Goal: hook_complete (W l nodes) *)
by rewrite (rely_loc' l1 R2). 
Qed.

End CombineGreeters.
