From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
From DiSeL
Require Import NewStatePredicates.
From DiSeL
Require Import SeqLib.
From DiSeL
Require Import Actions Injection Process Always HoareTriples InferenceRules.
From DiSeL
Require Import TwoPhaseProtocol TwoPhaseCoordinator TwoPhaseParticipant.
From DiSeL
Require TwoPhaseInductiveProof.
From DiSeL
Require Import QueryProtocol QueryHooked.

Section QueryPlusTPC.

(* Querying on behalf of the coordinator (it's easier this way, thanks *)
(* to cn_agreement lemma). In order to query on behald of the *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
(* participan, a different invariant-based fact should be proven. *)

(****************************************************************)
(*************         Basic definitions       ******************)
(****************************************************************)

Variables (lc lq : Label).
Variables (cn : nid) (pts : seq nid).
Hypothesis Lab_neq: lq != lc.
Hypothesis Hnin : cn \notin pts.
Hypothesis Puniq : uniq pts.
Hypothesis PtsNonEmpty : pts != [::].

(* Core protocol *)
Definition pc : protocol := TwoPhaseInductiveProof.tpc_with_inv lc [::] Hnin.
Definition Data : Type := (nat * Log).
Definition qnodes := cn :: pts.

(* Serialization of logs *)
Variable serialize : Data -> seq nat.
Variable deserialize : seq nat -> Data.
Hypothesis ds_inverse : left_inverse serialize deserialize.

(* This one is in the init state *)
Definition local_indicator (d : Data) :=
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  [Pred h | h = st :-> (d.1, CInit) \+ log :-> d.2].

(* Data is just a log *)
Definition core_state_to_data n h (d : Data)  :=
  if n == cn
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  then h = st :-> (d.1, CInit) \+ log :-> d.2
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  else h = st :-> (d.1, PInit) \+ log :-> d.2.                       

Lemma core_state_to_data_inj n h d d' :
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  core_state_to_data n h d -> core_state_to_data n h d' -> d = d'.
Proof.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite/core_state_to_data.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
case:ifP=>_ E; rewrite E ![_ \+ log :-> _]joinC=>{E}E.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
- have V: valid (log :-> d.2 \+ st :-> (d.1, CInit)).
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  - by case: validUn=>//k; rewrite !domPt !inE/==>/eqP<-. 
(* Goal: @eq Data d d' *)
  case: (hcancelV V E)=>E2=>{V E}V E. 
(* Goal: @eq Data d d' *)
  case: (hcancelPtV V E)=>E1.
(* Goal: hooks *)
  by rewrite [d]surjective_pairing [d']surjective_pairing E1 E2.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
have V: valid (log :-> d.2 \+ st :-> (d.1, PInit)).
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
- by case: validUn=>//k; rewrite !domPt !inE/==>/eqP<-. 
(* Goal: @eq Data d d' *)
case: (hcancelV V E)=>E2=>{V E}V E. 
(* Goal: @eq Data d d' *)
case: (hcancelPtV V E)=>E1.
(* Goal: hooks *)
by rewrite [d]surjective_pairing [d']surjective_pairing E1 E2.
Qed.

Lemma cn_in_qnodes : cn \in qnodes.
Proof. by rewrite inE eqxx. Qed.

Notation getLc s n := (getLocal n (getStatelet s lc)).
Notation cn_agree := TwoPhaseInductiveInv.cn_log_agreement.

(****************************************************************)
(*************   Necessary properties of TPC   ******************)
(****************************************************************)

Lemma core_state_stable_step z s d s' n :
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  cn != z -> network_step (mkWorld pc) z s s' ->
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  n \in qnodes ->
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  local_indicator d (getLc s cn) ->
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  core_state_to_data n (getLc s n) d  -> 
  core_state_to_data n (getLc s' n) d.
Proof.
(* Goal: forall (_ : is_true (negb (@eq_op nat_eqType cn z))) (_ : network_step (mkWorld pc) z s s') (_ : is_true (@in_mem (Equality.sort nat_eqType) n (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) qnodes))) (_ : @Pred_of_Simpl (PCM.sort (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC)) (local_indicator d) (getLocal cn (getStatelet s lc))) (_ : core_state_to_data n (getLocal n (getStatelet s lc)) d), core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
move=>N S Qn L H0; case: (step_coh S)=>C1 C2.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
have R: network_rely (plab pc \\-> pc, Unit) cn s s' by exists 1, z, s'. 
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
rewrite -(rely_loc' _ R) in L.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
case: C2=>V1 V2 _ D /(_ lc)/=; rewrite prEq=>/=[[C2] Inv].
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
case/orP: Qn=>[|P]; first by move/eqP=>Z; subst n; rewrite /core_state_to_data eqxx.  
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
move: (@cn_agree lc cn pts [::] Hnin (getStatelet s' lc) d.1 d.2 n C2 L Inv P)=>H. 
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite /core_state_to_data; case:ifP=>//; by move=>/eqP Z; subst n. 
Qed.

(***************  Intermediate definitions **********************)

(* Composite world *)
Definition W := QueryHooked.W lq pc Data qnodes serialize core_state_to_data.

Notation loc_qry s := (getLocal cn (getStatelet s lq)).
Notation loc_tpc' s n := (getLocal n (getStatelet s lc)).
Notation loc_tpc s := (loc_tpc' s cn).
Notation qry_init := (query_init_state lq Data qnodes serialize cn).

Lemma loc_imp_core s d n :
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  Coh W s -> n \in qnodes -> local_indicator d (loc_tpc s) ->
  core_state_to_data n (loc_tpc' s n) d.
Proof.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
move=>C Nq E.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
case/orP: Nq=>[|P]; first by move/eqP=>z; subst n; rewrite /core_state_to_data eqxx. 
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
case: (C)=>_ _ _ _/(_ lc); rewrite prEqC//=; case=> C2 Inv.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
move: (@cn_agree lc cn pts [::] Hnin (getStatelet s lc) d.1 d.2 n C2 E Inv P)=>->.
(* Goal: core_state_to_data n (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts PStateT st (@pair nat PState (@fst nat Log d) PInit)) (@heap_pts Log log (@snd nat Log d))) d *)
rewrite /core_state_to_data; case:ifP=>//.
(* Goal: forall _ : is_true (@eq_op nat_eqType n cn), @eq (PCM.sort (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC)) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts PStateT st (@pair nat PState (@fst nat Log d) PInit)) (@heap_pts Log log (@snd nat Log d))) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat CState) st (@pair nat CState (@fst nat Log d) CInit)) (@heap_pts Log log (@snd nat Log d))) *)
move=>/eqP Z; subst n; move/negbTE: Hnin=>Z.
(* Goal: @eq (PCM.sort (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC)) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts PStateT st (@pair nat PState (@fst nat Log d) PInit)) (@heap_pts Log log (@snd nat Log d))) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat CState) st (@pair nat CState (@fst nat Log d) CInit)) (@heap_pts Log log (@snd nat Log d))) *)
suff X: cn \in pts by rewrite X in Z.
(* Goal: is_true (@in_mem nid cn (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) pts)) *)
done.
Qed.

(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
Lemma find_empty l i : l \notin dom i -> getStatelet i l = empty_dstatelet.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
Proof. by rewrite /getStatelet; case: dom_find=>//->. Qed.
       

Definition cn_request_log :=
  request_data_program _ pc _ _ _ _ ds_inverse _ core_state_to_data_inj Lab_neq _ cn_in_qnodes
                       local_indicator core_state_stable_step (0, [::]).

(* Coordinator loop *)
Definition coordinator ds :=
  with_inv (TwoPhaseInductiveProof.ii _ _ _)
           (coordinator_loop_zero lc cn pts [::] Hnin Puniq PtsNonEmpty ds).

  
(****************************************************************)
(*************   Overall program combining the two  *************)
(****************************************************************)

(* The following program first initiates a series  of TPC rounds as a *)
(* coordinator, and then, on behalf of the coordinator queries a *)
(* particular pariticipant via the side protocol for querying. The *)
(* goal is to show that the resul obtained from querying is coherent *)
(* with respect to coordinator's state. *)

Program Definition coordinate_and_query (ds : seq data) to :
  {rr : seq (nid * nat) * seq (nid * nat)}, DHT [cn, W]
  (fun i =>
      let: (reqs, resp) := rr in 
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
     [/\ loc_tpc i = st :-> (0, CInit) \+ log :-> ([::] : seq (bool * data)),
        to \in qnodes,
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
        loc_qry i = qst :-> (reqs, resp) &
        qry_init to i],
   fun (res : Data) m =>
     let: (reqs, resp) := rr in
     exists (chs : seq bool),
       let: d := (size ds, seq.zip chs ds) in
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
       [/\ loc_tpc m = st :-> (d.1, CInit) \+ log :-> d.2,
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
        loc_qry m = qst :-> (reqs, resp),
        qry_init to m &
        res = d]) 
  := Do _ (
      iinject (coordinator ds);;    
      cn_request_log to).

Next Obligation.
(* Goal: hooks *)
by exact : (query_hookz lq pc Data qnodes serialize core_state_to_data).
Defined.

Next Obligation.
(* Goal: injects (mkWorld (@InductiveInv.PWIExports.ProtocolWithIndInv (@TwoPhaseInductiveProof.tpc lc cn pts (@Datatypes.nil nid) Hnin) (fun (d : dstatelet) (_ : pred nid) => TwoPhaseInductiveInv.Inv cn pts d) (@TwoPhaseInductiveProof.ii lc cn pts (@Datatypes.nil nid) Hnin))) (QueryHooked.W lq pc Data qnodes serialize core_state_to_data) coordinate_and_query_obligation_2 *)
exact: (injW lq pc Data qnodes serialize core_state_to_data Lab_neq).
Defined.

Next Obligation.
apply:ghC=>i0[rq rs][P1 P2 P3 P4]C0; apply: step.
(*Preparing to split the state. *)
move: (C0)=>CD0; rewrite /W eqW in CD0; move: (coh_hooks CD0)=>{CD0}CD0.
case: (coh_split CD0); try apply: hook_complete0.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
move=>i1[j1][C1 D1 Z].
subst i0; apply: inject_rule=>//.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
have E : loc_tpc (i1 \+ j1) = loc_tpc i1 by rewrite (locProjL CD0 _ C1)// domPt inE andbC eqxx.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite E{E} in P1.
apply: with_inv_rule'. 
apply: call_rule=>//_ i2 [chs]L2 C2 Inv j2 CD2/= R.
(* Massaging the complementary state *)
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
have E : loc_qry (i1 \+ j1) = loc_qry j1 by rewrite (locProjR CD0 _ D1)// domPt inE andbC eqxx.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
rewrite E {E} -(rely_loc' _ R) in P3.
(* Goal: @eq Data d d' *)
case: (rely_coh R)=>_ D2.
rewrite /W eqW in CD2; move: (coh_hooks CD2)=>{CD2}CD2.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite /mkWorld/= in C2.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
have C2': i2 \In Coh (plab pc \\-> pc, Unit).
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
- split=>//=.
  + by rewrite /valid/= valid_unit validPt.
  + by apply: (cohS C2).
  + by apply: hook_complete0.  
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  + by move=>z; rewrite -(cohD C2) !domPt.
(* Goal: forall (_ : is_true (negb (@eq_op nat_eqType cn z))) (_ : network_step (mkWorld pc) z s s') (_ : is_true (@in_mem (Equality.sort nat_eqType) n (@mem (Equality.sort nat_eqType) (seq_predType nat_eqType) qnodes))) (_ : @Pred_of_Simpl (PCM.sort (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC)) (local_indicator d) (getLocal cn (getStatelet s lc))) (_ : core_state_to_data n (getLocal n (getStatelet s lc)) d), core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
  move=>l; case B: (lc == l).
  + move/eqP:B=>B; subst l; rewrite /getProtocol findPt; split=>//.
(* Goal: hooks *)
    by move: (coh_coh lc C2); rewrite /getProtocol findPt.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  have X: l \notin dom i2 by rewrite -(cohD C2) domPt inE; move/negbT: B.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
  rewrite /getProtocol/= (find_empty _ _ X).
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  have Y: l \notin dom (lc \\-> pc) by rewrite domPt inE; move/negbT: B.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
  by case: dom_find Y=>//->_. 
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
have D2': j2 \In Coh (lq \\-> pq lq Data qnodes serialize, Unit)
    by apply: (cohUnKR CD2 _); try apply: hook_complete0.

(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
rewrite -(locProjL CD2 _ C2') in L2; last by rewrite domPt inE eqxx.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
rewrite -(locProjR CD2 _ D2') in P3; last by rewrite domPt inE eqxx.
clear C2 D2.

(* So what's important is for the precondition ofattachment to be *)
(* independent of the core protocol. *)  
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite injWQ in R.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
rewrite /query_init_state/= in P4.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
rewrite (locProjR CD0 _ D1) in P4; last by rewrite domPt inE eqxx.
(* Goal: core_state_to_data n (getLocal n (getStatelet s' lc)) d *)
have Q4: qry_init to j2.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
- by apply: (query_init_rely' lq Data qnodes serialize cn to _ _ P4 R).
clear P4.
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
rewrite /query_init_state/= -(locProjR CD2 _ D2') in Q4;
  last by rewrite domPt inE eqxx.

(* Now ready to use the spec for querying. *)
apply (gh_ex (g:=(rq, rs, (size ds, seq.zip chs ds)))).
(* Goal: is_true (@PCM.valid (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@PCM.join (@union_map_classPCM ptr_ordType (@axioms.dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts Log log (@snd nat Log d)) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log d) PInit)))) *)
(* Goal: @eq Data d d' *)
apply: call_rule=>//=; last by move=>d m[->->T1 T2->]_; eexists _. 
move=>CD2'; split=>//.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
case/orP: P2=>[|P]; first by move/eqP=>Z; subst to; rewrite /core_state_to_data eqxx.  
rewrite !(locProjL CD2 _ C2') in L2 *;
  last by rewrite domPt inE eqxx.
move: (coh_coh lc C2'); rewrite prEq; case=>C3 _.
(* Goal: core_state_to_data n (getLocal n (getStatelet s lc)) d *)
rewrite /core_state_to_data; case:ifP=>//[|_]; first by move=>/eqP Z; subst to. 
(* Goal: hooks *)
by apply: (@cn_agree lc cn pts [::] Hnin _ _ _ to C3 _ Inv).
Qed.

End QueryPlusTPC.
