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 pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX Protocols.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module WorldGetters.
Section WorldGetters.

(* It's okay to have duplicating nodes in this list *)

(* World is a dependent partial map of protocols *)

Definition context := union_map Label protocol.

(* 
The hooks are dependencies between:

1. a hook's unique id
2. a core protocol
3. a client protocol
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
4. a send-transition (represented by its tag) of a client protocol

*)
Definition hook_domain := [ordType of ((nat * Label) * (Label * nat))%type].

(*

A hook is a constraint from the local state wrt. core protocol (1st
heap argument), relating the local state wrt. the client protocol (2ns
heap argument), message to be sent, and the destination node id.

*)
Definition hook_type := heap -> heap -> seq nat -> nid -> Prop.

Definition hooks := union_map hook_domain hook_type.
Definition world := (context * hooks)%type.

Definition getc (w: world) : context := fst w.
Coercion getc : world >-> context.

Definition geth (w: world) : hooks := snd w.
Coercion geth : world >-> hooks.

Variable w : world.

Variables (p : protocol).

(* The function is, in fact, partially defined and returns Empty
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
   Protocol for a non-present label. *)
Definition getProtocol i : protocol:=
  match find i (getc w) with
  | Some p => p
  | None => EmptyProt i 
  end.

End WorldGetters.
End WorldGetters.

Export WorldGetters.

(* Defining coherence of a state with respect to the world *)

Module Worlds.

Module Core.
Section Core.

(* The following definition ties together worlds and states *)

Definition hooks_consistent (c : context) (h : hooks) : Prop :=
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  forall z lc ls t, ((z, lc), (ls, t)) \in dom h ->
  (lc \in dom c) && (ls \in dom c).

Definition hook_complete w := hooks_consistent (getc w) (geth w).

Lemma hook_complete0 c : hook_complete (c, Unit).
(* Goal: @eq protocol (getProtocol mkWorld (plab p)) p *)
Proof. by move=>????; rewrite dom0. Qed.

Definition Coh (w : world) : Pred state := fun s =>
  let: c := fst w in
  let: h := snd w in                                           
  [/\ valid w, valid s, hook_complete w,
      dom c =i dom s &
      forall l, coh (getProtocol w l) (getStatelet s l)].

Lemma cohW w s : Coh w s -> valid w.
Proof. by case w=>[c h]; case. Qed.

Lemma cohS w s : Coh w s -> valid s.
Proof. by case w=>[c h]; case. Qed.

Lemma cohH w s : Coh w s -> hook_complete w.
Proof. by case w=>[c h]; case. Qed.

Lemma cohD w s : Coh w s -> dom (getc w) =i dom s.
Proof. by case w=>[c h]; case. Qed.

Lemma coh_coh w s l : Coh w s -> coh (getProtocol w l) (getStatelet s l).
Proof. by case w=>[c h]; case. Qed.

(* Now we need to establish a bunch of natural properties with respect
   to coherence of worlds and states. *)

Lemma unit_coh w s :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  Coh w s -> w = Unit <-> s = Unit.
Proof.
(* Goal: forall _ : @eq (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 t1) (@PCM.join (union_mapPCM Label dstatelet) s2 t2), @eq (PCM.sort (union_mapPCM Label dstatelet)) s1 s2 *)
case: (w)=>[c h].
(* Goal: forall _ : Coh (@pair context hooks c h) s, iff (@eq world (@pair context hooks c h) (@PCM.unit (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)))) (@eq state s (@PCM.unit (union_mapPCM Label dstatelet))) *)
case=>V V' Hc E H; split.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
case=>Z1 Z2; subst c h; rewrite dom0 in E; last by rewrite (dom0E V').
(* Goal: forall _ : @eq state s (@PCM.unit (union_mapPCM Label dstatelet)), @eq world (@pair context hooks c h) (@PCM.unit (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type))) *)
move=>Z; subst s; move/andP: V=>/=[V1 V2].
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
have Z: c = Unit by apply: (dom0E V1); move=>z; rewrite E dom0.
(* Goal: @eq world (@pair context hooks c h) (@PCM.unit (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type))) *)
subst c; suff Z: (h = Unit) by subst h.
(* Goal: @eq hooks h (@PCM.unit (union_mapPCM hook_domain hook_type)) *)
simpl in Hc; clear E H V1 V'.
(* Goal: @eq hooks h (@PCM.unit (union_mapPCM hook_domain hook_type)) *)
apply: (dom0E V2); move=> x; case X: (x \in dom h)=>//.
(* Goal: @eq protocol (getProtocol mkWorld (plab p)) p *)
by move: x X=>[[z lc] [ls t]]/Hc/andP[]; rewrite !dom0. 
Qed.

Lemma Coh0 (w : world) (s : state) :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  w = Unit -> s = Unit -> Coh w s.
Proof.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
move=>->->{w s}; split; rewrite ?dom0=>//=; last first.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
- by move=>l; rewrite /getProtocol /getStatelet !find0E.
(* Goal: @eq protocol (getProtocol mkWorld (plab p)) p *)
by move=>z lc ls t; rewrite dom0.  
Qed.

Lemma CohUn (w1 w2 : world) (s1 s2 : state) :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  Coh w1 s1 -> Coh w2 s2 ->
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  valid (w1 \+ w2) -> Coh (w1 \+ w2) (s1 \+ s2).
Proof.
(* Goal: forall (_ : Coh w1 s1) (_ : Coh w2 s2) (_ : is_true (@PCM.valid (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) w1 w2))), Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) w1 w2) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
case: w1=>[c1 h1]; case: w2=>[c2 h2]; move=>C1 C2 V.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
case: (C1)=>_ G1 K1 J1 H1; case: (C2)=>_ G2 K2 J2 H2.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
case/andP: V=>V V'; simpl in V, V'.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
have X: valid (s1 \+ s2).
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
- case: validUn=>//; [by rewrite G1|by rewrite G2|move=>l; rewrite -J1 -J2=>D1 D2].
(* Goal: @eq protocol (getProtocol mkWorld (plab p)) p *)
  by case: validUn V=>//=V1 V2; move/(_ _ D1); rewrite D2.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
have Y: dom (c1 \+ c2) =i dom (s1 \+ s2).
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
- by move=>z; rewrite !domUn !inE/=;rewrite V X/= J1 J2.
have Z1:  valid ((c1, h1) \+ (c2, h2)) by rewrite /valid/= V V'.
(* Goal: Coh (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) *)
split=>//[|l]; last first.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
- rewrite /getProtocol /getStatelet.
(* Goal: forall _ : @eq (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 t1) (@PCM.join (union_mapPCM Label dstatelet) s2 t2), @eq (PCM.sort (union_mapPCM Label dstatelet)) s1 s2 *)
  case: (dom_find l (s1 \+ s2))=>[|v]Z.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  - by move/find_none: (Z); rewrite -Y; case: dom_find=>//->_; rewrite Z.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  move/find_some: (Z)=>D; rewrite Z; rewrite -Y in D=> E.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) v *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  case: dom_find D=>// p Z' _ _; rewrite Z'.
(* Goal: @Coherence.sort (Protocols.nodes p) (coh p) v *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  rewrite findUnL // in Z; rewrite findUnL // J1 in Z'.
  by case: ifP Z Z'=>_ F1 F2; [move: (H1 l)|move: (H2 l)];
     rewrite /getProtocol /getStatelet F1 F2.
by move=>z lc ls t/=; rewrite domUn inE=>/andP[_]/orP[];[move/K1|move/K2];
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
   move/andP=>[A1 A2]; rewrite !domUn !inE A1 A2 V -?(orbC true). 
Qed.

(* Coherence is trivially precise wrt. statelets *)
Lemma coh_prec w: precise (Coh w).
Proof.
(* Goal: forall (_ : is_true (negb (@eq_op nat_eqType n n'))) (_ : is_true (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) st)), @eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n' x st) s)) (getLocal n (DStatelet st s)) *)
move=>s1 s2 t1 t2 V C1 C2.
(* Goal: forall _ : @eq (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 t1) (@PCM.join (union_mapPCM Label dstatelet) s2 t2), @eq (PCM.sort (union_mapPCM Label dstatelet)) s1 s2 *)
case: C1 => H1 G1 K1 D1 _.
(* Goal: forall _ : @eq (PCM.sort (union_mapPCM Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 t1) (@PCM.join (union_mapPCM Label dstatelet) s2 t2), @eq (PCM.sort (union_mapPCM Label dstatelet)) s1 s2 *)
case: C2 => H2 G2 K2 D2 _ H.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
by apply: (@dom_prec _ _ _  s1 s2 t1 t2)=>//z; rewrite -D1 -D2.
Qed.

Lemma locE i n k x y :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  k \in dom i -> valid i -> valid (dstate (getStatelet i k)) ->
  getLocal n (getStatelet (upd k
       {| dstate := upd n x (dstate (getStatelet i k));
          dsoup := y |} i) k) = x.
Proof.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
move=>D V; rewrite /getStatelet; case:dom_find (D) =>//d->_ _.
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
by rewrite findU eqxx/= V /getLocal/= findU eqxx/==>->.
Qed.

Lemma locE' d n x y :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  valid (dstate d) ->
  getLocal n {| dstate := upd n x (dstate d);
                dsoup := y |} = x.
Proof. by move=>V; rewrite /getLocal findU eqxx/= V. Qed.

Lemma locU n n' x st s :
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  n != n' ->
(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
  valid st ->
  getLocal n {| dstate := upd n' x st; dsoup := s |} =
  getLocal n {| dstate := st; dsoup := s |}.
Proof.
(* Goal: forall (_ : is_true (negb (@eq_op nat_eqType n n'))) (_ : is_true (@PCM.valid (@union_map_classPCM nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap)) st)), @eq Heap.heap (getLocal n (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) n' x st) s)) (getLocal n (DStatelet st s)) *)
  move=> /negbTE N V.
(* Goal: @eq protocol (getProtocol mkWorld (plab p)) p *)
  by rewrite /getLocal findU/= N.
Qed.


Section MakeWorld.

Variable p : protocol.
Notation l := (plab p).

(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
Definition mkWorld : world := (l \\-> p, Unit).

Lemma prEq : (getProtocol mkWorld l) = p.
Proof. by rewrite /getProtocol findPt. Qed.
                          
(*

Here's an incomplete list of procedures and facts, which might be
useful eventually:

(* Goal: @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: forall _ : @eq (@UMC.sort Label dstatelet (union_mapUMC Label dstatelet)) (@PCM.join (union_mapPCM Label dstatelet) s1 s2) (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l v (@UMC.free Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2))), @Coherence.sort (Protocols.nodes match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) (coh match @UMC.find Label protocol (union_mapUMC Label protocol) l (getc (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2))) with | Some p => p | None => EmptyProt l end) match @UMC.find Label dstatelet (union_mapUMC Label dstatelet) l (@PCM.join (union_mapPCM Label dstatelet) s1 s2) with | Some d => d | None => empty_dstatelet end *)
(* Goal: hook_complete (@PCM.join (prodPCM (union_mapPCM Label protocol) (union_mapPCM hook_domain hook_type)) (@pair context hooks c1 h1) (@pair context hooks c2 h2)) *)
- Define getters for particular transitions of worlds;

 *)

End MakeWorld.

(* TODO: try_recv should be restricted by a set of labels and a set of
   protocols *)
End Core.
End Core.

End Worlds.

Export Worlds.Core.
