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 DepMaps Protocols Worlds NetworkSem Rely.
From DiSeL
Require Import Actions Injection Process Always HoareTriples InferenceRules.
From DiSeL
Require Import InductiveInv While.
From DiSeL
Require Import TwoPhaseProtocol.

Module TwoPhaseParticipant.
Section TwoPhaseParticipant.

Variable l : Label.
Variables (cn : nid) (pts : seq nid) (others : seq nid).
Hypothesis Hnin : cn \notin pts.
Hypothesis PtsNonEmpty : pts != [::].

Definition tpc := TwoPhaseCommitProtocol others Hnin l.
Notation W := (mkWorld tpc).

Variable p : nid.
Hypothesis Hpin : p \in pts.

Section ParticipantImplementation.

(************** Atomic actions **************)

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Three receive-actions *)

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* This action actually encompasses two receive-transitions *)
Program Definition tryrecv_prep_req := act (@tryrecv_action_wrapper W p
      (fun k _ t b => (k == l) && (t == prep_req)) _).
(* TODO: automate these kinds of proofs *)
Next Obligation. by case/andP: H=>/eqP->_; rewrite /ddom domPt inE/=. Qed.

(*

[Overly cautious filtering]

This action uses different filter for the tags of incoming messages
depending on what was this participant's answer to the initial prepare
request. If the answer what "yes", then the expected incomming
messages can be of the type "commit" and "abort" (as some other
participant may decide to abort). However, if this participant said
"no", the only expected message is "abort".

This filter can be removed if the inductive invariant is established
upfront, hence we can formally _prove_ that any incoming message will
be of this shape. However, we decided to postpone this proof and do it separately, therefore, making the implementation "overly cautious".

*)

Program Definition tryrecv_commabrt_req c :=
  act (@tryrecv_action_wrapper W p
  (fun k _ t b => (k == l) &&
  (if c then (t == commit_req) || (t == abort_req) else (t == abort_req))) _).
Next Obligation. by case/andP: H=>/eqP->_; rewrite /ddom domPt inE/=. Qed.

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Four send-actions, e -- id of the current era *)

Program Definition send_yes e to :=
  act (@send_action_wrapper W tpc p l (prEq tpc) (pn_send_yes_trans others Hnin) _ [:: e] to).
Next Obligation. by rewrite !InE; right; right; right; left. Qed.

Program Definition send_no e to :=
  act (@send_action_wrapper W tpc p l (prEq tpc) (pn_send_no_trans others Hnin) _ [:: e] to).
Next Obligation. by rewrite !InE; right; right; right; right; left. Qed.

Program Definition send_commit_ack e to :=
  act (@send_action_wrapper W tpc p l (prEq tpc) (pn_commit_ack_trans others Hnin) _ [:: e] to).
Next Obligation. by rewrite !InE; right; right; right; right; right; left. Qed.

Program Definition send_abort_ack e to :=
  act (@send_action_wrapper W tpc p l (prEq tpc) (pn_abort_ack_trans others Hnin) _ [:: e] to).
Next Obligation. by rewrite !InE; do![right]. Qed.


(************** Participant code **************)

Arguments TPCProtocol.TPCCoh [cn pts others].
Notation coh := (@TPCProtocol.TPCCoh cn pts others).
Notation getS s := (getStatelet s l).
Notation loc i := (getLocal p (getStatelet i l)).

(* Read current round *)

Notation Pin := (TPCProtocol.pts_in cn others Hpin).

Program Definition read_round_p :
  {(ecl : (nat * PState) * Log)}, DHT [p, W]
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i => loc i = st :-> ecl.1 \+ log :-> ecl.2, 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
   fun r m => loc m = st :-> ecl.1 \+ log :-> ecl.2 /\
              exists (pf : coh (getS m)), r = (getStP Hnin pf Pin).1) :=
  Do (act (@skip_action_wrapper W p l tpc (prEq tpc) _
                                (fun s pf => (getStP Hnin pf Pin).1))).
Next Obligation.  
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: ghC=>i [[e c]lg]/= E _.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
apply: act_rule=>j R; split=>[|r k m]; first by case: (rely_coh R).
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case=>/=H1[Cj]Z; subst j=>->R'.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
split; first by rewrite (rely_loc' l R') (rely_loc' _ R).
(* Goal: @ex (TPCProtocol.tpc_coh cn pts others (getStatelet m l)) (fun pf : TPCProtocol.tpc_coh cn pts others (getStatelet m l) => @eq nat (@fst nat PState (@getStP cn pts others Hnin p (getStatelet k l) (@Actions.safe_local (mkWorld tpc) l tpc (prEq tpc) k H1) (@TPCProtocol.pts_in cn pts others p Hpin))) (@fst nat PState (@getStP cn pts others Hnin p (getStatelet m l) pf (@TPCProtocol.pts_in cn pts others p Hpin)))) *)
case: (rely_coh R')=>_; case=>_ _ _ _/(_ l)=>/= pf; rewrite prEq in pf.
(* Goal: @ex (TPCProtocol.tpc_coh cn pts others (getStatelet m l)) (fun pf : TPCProtocol.tpc_coh cn pts others (getStatelet m l) => @eq nat (@fst nat PState (@getStP cn pts others Hnin p (getStatelet k l) (@Actions.safe_local (mkWorld tpc) l tpc (prEq tpc) k H1) (@TPCProtocol.pts_in cn pts others p Hpin))) (@fst nat PState (@getStP cn pts others Hnin p (getStatelet m l) pf (@TPCProtocol.pts_in cn pts others p Hpin)))) *)
exists pf; move: (rely_loc' l R').
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
move => E'.
(* Goal: @eq nat (@fst nat PState (@getStP cn pts others Hnin p (getStatelet k l) (@Actions.safe_local (mkWorld tpc) l tpc (prEq tpc) k H1) (@TPCProtocol.pts_in cn pts others p Hpin))) (@fst nat PState (@getStP cn pts others Hnin p (getStatelet m l) pf (@TPCProtocol.pts_in cn pts others p Hpin))) *)
apply sym_eq in E'.
(* Goal: @eq nat (@fst nat PState (@getStP cn pts others Hnin p (getStatelet k l) (@Actions.safe_local (mkWorld tpc) l tpc (prEq tpc) k H1) (@TPCProtocol.pts_in cn pts others p Hpin))) (@fst nat PState (@getStP cn pts others Hnin p (getStatelet m l) pf (@TPCProtocol.pts_in cn pts others p Hpin))) *)
suff X: getStP Hnin (Actions.safe_local (prEq tpc) H1) Pin = getStP Hnin pf Pin by rewrite X.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by apply: (TPCProtocol.getStPE Hnin pf _ Pin Hpin E').
Qed.

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Step 1 receive perp-messages *)

Export TPCProtocol.

(* Ending condition *)
Definition rp_prep_req_cond (res : option data) := res == None.

(* Invariant relates the argument and the shape of the state *)
Definition rp_prep_req_inv (e : nat) (lg : Log) : cont (option data) :=
  fun res i =>
    if res is Some d
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    then loc i = st :-> (e, PGotRequest d) \+ log :-> lg
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    else loc i = st :-> (e, PInit) \+ log :-> lg.

Program Definition receive_prep_req_loop (e : nat):
  {(lg : Log)}, DHT [p, W]
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i => loc i = st :-> (e, PInit) \+ log :-> lg,
   fun res m => exists d, res = Some d /\
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
       loc m = st :-> (e, PGotRequest d) \+ log :-> lg)
  :=
  Do _ (@while p W _ _ rp_prep_req_cond (rp_prep_req_inv e) _
        (fun _ => Do _ (
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
           r <-- tryrecv_prep_req;
           match r with
           | Some (from, tg, body) =>
             if (from == cn) && (head 0 body == e)
             then ret _ _ (Some (behead body))
             else ret _ _ None
           | None => ret _ _ None
           end              
        )) None).

Next Obligation. by apply: with_spec x. Defined.
Next Obligation. by move:H; rewrite /rp_prep_req_inv (rely_loc' _ H0). Qed.
Next Obligation.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply:ghC=>i1 lg[/eqP->{H}/=E1]C1; apply: step.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
apply: act_rule=>i2/=R1; split; first by case: (rely_coh R1).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>[[[from e']d i3 i4]|i3 i4]; last first.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- case=>S/=[]?; case; last by case=>?[?][?][?][?][?][].
  case=>_ _ Z; subst i3=>R2; apply: ret_rule=>i5 R4/=.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
  by rewrite (rely_loc' _ R4) (rely_loc' _ R2)(rely_loc' _ R1).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Sf[]C2[]=>[|[l'][mid][tms][from'][rt][pf][][E]Hin E2 Hw/=]; first by case.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case/andP=>/eqP Z G->[]Z1 Z2 Z3 R2; subst l' from' e' d.
move: rt pf (coh_s (w:=W) l (s:=i2) C2) Hin R2 E2 Hw G E; rewrite prEq/=.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
move=>rt pf Cj' Hin R E2 Hw G E.
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have D: rt = pn_receive_got_prep_trans _ Hnin.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- move: Hin G; by do! [case=>/=; first by move=>->].  
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
subst rt=>{G}.
have P1: valid (dstate (getS i2))
  by apply: (@cohVl _ coh); case: (Cj')=>P1 P2 P3 P4; split=>//=; done.
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have P2: valid i2 by apply: (cohS (proj2 (rely_coh R1))).
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have P3: l \in dom i2 by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
case: ifP=>G1; apply: ret_rule=>//i5 R4.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- rewrite /rp_prep_req_inv; rewrite (rely_loc' _ R4) (rely_loc' _ R) locE//=.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
  rewrite /TPCProtocol.rp_step Hpin/=. case/andP:G1=>/eqP=>Z1/eqP H2; subst from.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  rewrite -(rely_loc' _ R1) in E1; rewrite (getStL_Kp _ pf E1)(getStP_K Hnin _ pf Hpin E1).
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
  by rewrite/pstep_recv/= H2 !eqxx/= .
rewrite /rp_prep_req_inv; rewrite (rely_loc' _ R4) (rely_loc' _ R) locE//=.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite /TPCProtocol.rp_step Hpin/=.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite -(rely_loc' _ R1) in E1; rewrite (getStL_Kp _ pf E1)(getStP_K Hnin _ pf Hpin E1).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite/pstep_recv/=.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
by move/negbT: G1; rewrite Bool.negb_andb; case/orP=>->//=; rewrite orbC. 
Qed.

Next Obligation.
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: ghC=>i1 lg E1 C1/=.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply: (gh_ex (g:=lg)); apply: call_rule=>//r i2 [H1]H2 C2.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite /rp_prep_req_cond/rp_prep_req_inv in H1 H2.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
by case: r H1 H2=>//d _->; exists d.
Qed.

(* Step 2: Respond yes or no to the coordinator *)

Program Definition resp_to_req (e : nat) (doCommit : bool) :
  {(dl : (data * Log))}, DHT [p, W]
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i => loc i = st :-> (e, PGotRequest dl.1) \+ log :-> dl.2,
   fun (_ : seq nat) m => 
     let:  (d, lg) := dl in
     if doCommit
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     then loc m = st :-> (e, PRespondedYes d) \+ log :-> lg
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     else loc m = st :-> (e, PRespondedNo d) \+ log :-> lg)
  := Do (if doCommit then send_yes e cn else send_no e cn).
Next Obligation.
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply:ghC=>i [d lg]E1 C1.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have Pre: forall i2, network_rely W p i i2 ->
          Actions.send_act_safe W (p:=tpc) p l
          (if doCommit
           then (pn_send_yes_trans (cn:=cn) (pts:=pts) others Hnin)
           else (pn_send_no_trans (cn:=cn) (pts:=pts) others Hnin)) [:: e] cn i2.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- move=>i2 R1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
  split; first by case: (rely_coh R1).
(* Goal: is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2))) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM Label dstatelet (union_mapUMC Label dstatelet)) i2) *)
  + have X: HPn cn pts p cn by [].
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    case: (proj2 (rely_coh R1))=>_ _ _ _/(_ l); rewrite (prEq tpc)=>C.
    case: doCommit; split=>//; exists X, C, e, d;
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    by rewrite -(rely_loc' _ R1) in E1; rewrite (getStP_K _ _ _ _ E1).
(* Goal: is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2))) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM Label dstatelet (union_mapUMC Label dstatelet)) i2) *)
  + rewrite /Actions.can_send /nodes inE/= mem_cat Hpin orbC.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/= eqxx.
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  rewrite /Actions.filter_hooks umfilt0=>???.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  move => F.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  apply sym_eq in F.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  move: F.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
  by move/find_some; rewrite dom0.

(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: doCommit Pre=>Pre; apply: act_rule=>i2 R1/=; move:(Pre i2 R1)=>{Pre}Pre.

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Send yes-answer *)
(* Goal: and (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (forall (y : list nat) (k m : state) (_ : @ex (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (fun pf : @Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 => @Actions.send_act_step (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 pf k y)) (_ : network_rely (mkWorld tpc) p k m), @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
split=>//; move=>b i3 i4[Sf]St R3.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: {-1}(Sf)=>_/=[]_[H][]C'//; rewrite -(rely_loc' _ R1) in E1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)/=.
(* Goal: forall (_ : send_prep_resp_prec PAborted (@pair nat PState e (PAborted d)) (@cons nat e (@Datatypes.nil nat))) (_ : is_true (Actions.can_send tpc p l i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>e'[d'][][]Z1 Z2 _ G; subst d' e'.
(* Goal: forall _ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn, @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
move: St; rewrite/Actions.send_act_step/==>[][_][h][].
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite /pn_step -!(pf_irr C' (pn_safe_coh _))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
        -!(pf_irr (pn_this_in _ H) (pn_this_in _ _)).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)(getStL_Kp _ (pn_this_in _ H) E1)/=. 
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Z Z';subst h i3; rewrite (rely_loc' _ R3) locE//; last by apply: (cohVl C').
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
+ by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by apply: (cohS (proj2 (rely_coh R1))).

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Send no-answer *)
(* TODO: Remove proof duplication!!! *)  
(* Goal: and (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (forall (y : list nat) (k m : state) (_ : @ex (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (fun pf : @Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 => @Actions.send_act_step (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 pf k y)) (_ : network_rely (mkWorld tpc) p k m), @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
split=>//; move=>b i3 i4[Sf]St R3.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: {-1}(Sf)=>_/=[]_[H][]C'//; rewrite -(rely_loc' _ R1) in E1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)/=.
(* Goal: forall (_ : send_prep_resp_prec PAborted (@pair nat PState e (PAborted d)) (@cons nat e (@Datatypes.nil nat))) (_ : is_true (Actions.can_send tpc p l i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>e'[d'][][]Z1 Z2 _ G; subst d' e'.
(* Goal: forall _ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn, @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
move: St; rewrite/Actions.send_act_step/==>[][_][h][].
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite /pn_step -!(pf_irr C' (pn_safe_coh _))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
        -!(pf_irr (pn_this_in _ H) (pn_this_in _ _)).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)(getStL_Kp _ (pn_this_in _ H) E1)/=. 
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Z Z';subst h i3; rewrite (rely_loc' _ R3) locE//; last by apply: (cohVl C').
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
+ by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by apply: (cohS (proj2 (rely_coh R1))).
Qed.

(* Step 3 Receive commit/abort msg *)

Definition rp_commabrt_cond (res : option bool) := res == None.

(* Invariant relates the argument and the shape of the state *)
Definition rp_commabrt_inv (e : nat) (c: bool) (ld : (Log * data)) :
  cont (option bool) :=
  fun res i =>
    let: (lg, d) := ld in
    if res is Some b
    then if b
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
         then loc i = st :-> (e, PCommitted d) \+ log :-> (rcons lg (b, d))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
         else loc i = st :-> (e, PAborted d) \+ log :-> (rcons lg (b, d))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    else loc i = st :-> (e, if c then PRespondedYes d else PRespondedNo d) \+ log :-> lg.

Program Definition receive_commabrt_loop (e : nat) (c : bool):
  {(ld : (Log * data))}, DHT [p, W]
   (fun i => let: (lg, d) := ld in
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    loc i = st :-> (e, if c then PRespondedYes d else PRespondedNo d) \+ log :->lg,
    fun (res : option bool) m => let: (lg, d) := ld in
    exists b, res = Some b /\
    if b 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    then loc m = st :-> (e, PCommitted d) \+ log :-> (rcons lg (b, d))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    else loc m = st :-> (e, PAborted d) \+ log :-> (rcons lg (b, d)))
  :=
  Do _ (@while p W _ _ rp_commabrt_cond (rp_commabrt_inv e c) _
        (fun _ => Do _ (
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
           r <-- tryrecv_commabrt_req c;
           match r with
           | Some (from, tg, body) =>
             if (from == cn) && (head 0 body == e)
             then ret _ _ (Some (tg == commit_req))
             else ret _ _ None
           | None => ret _ _ None
           end              
        )) None).
Next Obligation. by apply: (with_spec x). Defined.
Next Obligation. by move:H; rewrite /rp_commabrt_inv (rely_loc' _ H0). Qed.
Next Obligation.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
apply:ghC=>i1 [lg d][/eqP->{H}/=E1]C1; apply: step.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
apply: act_rule=>i2/=R1; split; first by case: (rely_coh R1).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>[[[from e']v i3 i4]|i3 i4]; last first.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- case=>S/=[]?; case; last by case=>?[?][?][?][?][?][].
  case=>_ _ Z; subst i3=>R2; apply: ret_rule=>i5 R4/=.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
  rewrite /rp_commabrt_inv/= in E1 *.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
  by rewrite (rely_loc' _ R4) (rely_loc' _ R2) (rely_loc' _ R1).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Sf[]C2[]=>[|[l'][mid][tms][from'][rt][pf][][E]Hin E2 Hw/=]; first by case.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case/andP=>/eqP Z G->[]Z1 Z2 Z3 R2; subst l' from' e' v.
move: rt pf (coh_s (w:=W) l (s:=i2) C2) Hin R2 E2 Hw G E; rewrite prEq/=.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
move=>rt pf Cj' Hin R E2 Hw G E.
have P1: valid (dstate (getS i2))
  by apply: (@cohVl _ coh); case: (Cj')=>P1 P2 P3 P4; split=>//=; done.
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have P2: valid i2 by apply: (cohS (proj2 (rely_coh R1))).
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have P3: l \in dom i2 by rewrite-(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
(* See the remark [Overly cautious filtering] *)
have D: if c
        then rt = pn_receive_commit_ack_trans _ Hnin \/
             rt = pn_receive_abort_ack_trans _ Hnin
        else rt = pn_receive_abort_ack_trans _ Hnin.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
-  move: Hin G; clear E1; do![case=>/=; first by move=>->; case: c].
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
   by case;[|case=>//];move=>->; case:c=>//=; [left | right].
case: ifP=>G1; apply: ret_rule=>//i5 R4.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- rewrite /rp_commabrt_inv (rely_loc' _ R4) (rely_loc' _ R) locE//=.
  case/andP:G1=>/eqP=>Z1/eqP H2; subst from.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  rewrite -(rely_loc' _ R1) in E1.
  case: (c) E1 E2 D G=>/=E1 E2; case=>Z; subst rt; rewrite E2{E2}//==>_;
  rewrite/rp_step (getStL_Kp _ pf E1)(getStP_K Hnin _ pf Hpin E1) Hpin;
  by rewrite/pstep_recv/= H2 !eqxx/=. 
rewrite /rp_commabrt_inv; rewrite (rely_loc' _ R4) (rely_loc' _ R) locE//=.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite -(rely_loc' _ R1) in E1.
case: (c) E1 E2 D G=>/=E1 E2; case=>Z {E2}; subst rt=>//= _;
rewrite/rp_step (getStL_Kp _ pf E1)(getStP_K Hnin _ pf Hpin E1) Hpin;
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
by rewrite/pstep_recv/=; move/negbT: G1; rewrite Bool.negb_andb; case/orP=>->//=; rewrite orbC.
Qed.

Next Obligation.
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: ghC=>i1 [lg d] E1 C1/=.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply: (gh_ex (g:=(lg, d))); apply: call_rule=>//r i2 [H1]H2 C2. 
(* Goal: @ex bool (fun b : bool => and (@eq (option bool) r (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet i2 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet i2 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))))) *)
rewrite /rp_commabrt_cond/rp_commabrt_inv in H1 H2; case: r H1 H2=>//b _.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by exists b.
Qed.

(* Step 4 Send ack wrt commit/abort *)
 
Program Definition send_ack (e : nat) (hasCommitted : bool) :
  {(dl : (data * Log))}, DHT [p, W]
  (fun i =>  let:  (d, lg) := dl in
     if hasCommitted
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     then loc i = st :-> (e, PCommitted d) \+ log :-> lg
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     else loc i = st :-> (e, PAborted d) \+ log :-> lg,
   fun (_ : seq nat) m => 
     let:  (d, lg) := dl in
     if hasCommitted
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     then loc m = st :-> (e.+1, PInit) \+ log :-> lg
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     else loc m = st :-> (e.+1, PInit) \+ log :-> lg)
  := Do (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn).

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* TODO: automate this proof, as it's exactly the same as for the previous send-transition! *)
Next Obligation.
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply:ghC=>i [d lg]E1 C1.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
have Pre: forall i2, network_rely W p i i2 ->
          Actions.send_act_safe W (p:=tpc) p l
          (if hasCommitted
           then (pn_commit_ack_trans (cn:=cn) (pts:=pts) others Hnin)
           else (pn_abort_ack_trans (cn:=cn) (pts:=pts) others Hnin)) [:: e] cn i2.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- move=>i2 R1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
  split; first by case: (rely_coh R1).
(* Goal: is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2))) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM Label dstatelet (union_mapUMC Label dstatelet)) i2) *)
  + have X: HPn cn pts p cn by [].
(* Goal: @send_safe (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) p cn (getStatelet i2 l) (@cons nat e (@Datatypes.nil nat)) *)
(* Goal: is_true (Actions.can_send tpc p l i2) *)
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    case: (proj2 (rely_coh R1))=>_ _ _ _/(_ l); rewrite (prEq tpc)=>C.
    case: hasCommitted E1; split=>//; exists X, C, e, d;
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    by rewrite -(rely_loc' _ R1) in E1; rewrite (getStP_K _ _ _ _ E1).
(* Goal: is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2))) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM Label dstatelet (union_mapUMC Label dstatelet)) i2) *)
  + rewrite /Actions.can_send /nodes inE/= mem_cat Hpin orbC.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
    by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/= eqxx.
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  rewrite /Actions.filter_hooks umfilt0=>???.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  move => F.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  apply sym_eq in F.
(* Goal: forall (_ : is_true (@in_mem (Ordered.sort Label) _lc_ (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))) (_ : is_true (@in_mem (Ordered.sort Label) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2)))), _hk_ (getLocal p (getStatelet i2 _lc_)) (getLocal p (getStatelet i2 l)) (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  move: F.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
  by move/find_some; rewrite dom0.

(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: hasCommitted E1 Pre=>E1 Pre; apply: act_rule=>i2 R1/=; move:(Pre i2 R1)=>{Pre}Pre.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Send commit-ack *)
(* Goal: and (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (forall (y : list nat) (k m : state) (_ : @ex (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (fun pf : @Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 => @Actions.send_act_step (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 pf k y)) (_ : network_rely (mkWorld tpc) p k m), @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
split=>//; move=>b i3 i4[Sf]St R3.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: {-1}(Sf)=>_/=[]_[H][]C'//; rewrite -(rely_loc' _ R1) in E1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)/=.
(* Goal: forall (_ : send_prep_resp_prec PAborted (@pair nat PState e (PAborted d)) (@cons nat e (@Datatypes.nil nat))) (_ : is_true (Actions.can_send tpc p l i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>e'[d'][][]Z1 Z2 _ G; subst d' e'.
(* Goal: forall _ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn, @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
move: St; rewrite/Actions.send_act_step/==>[][_][h][].
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite /pn_step -!(pf_irr C' (pn_safe_coh _))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
        -!(pf_irr (pn_this_in _ H) (pn_this_in _ _)).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)(getStL_Kp _ (pn_this_in _ H) E1)/=. 
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Z Z';subst h i3; rewrite (rely_loc' _ R3) locE//; last by apply: (cohVl C').
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
+ by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by apply: (cohS (proj2 (rely_coh R1))).
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
(* Send abort-ack *)
(* TODO: Remove proof duplication!!! *)  
(* Goal: and (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (forall (y : list nat) (k m : state) (_ : @ex (@Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2) (fun pf : @Actions.send_act_safe (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 => @Actions.send_act_step (mkWorld tpc) tpc p l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 pf k y)) (_ : network_rely (mkWorld tpc) p k m), @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
split=>//; move=>b i3 i4[Sf]St R3.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
case: {-1}(Sf)=>_/=[]_[H][]C'//; rewrite -(rely_loc' _ R1) in E1.
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)/=.
(* Goal: forall (_ : send_prep_resp_prec PAborted (@pair nat PState e (PAborted d)) (@cons nat e (@Datatypes.nil nat))) (_ : is_true (Actions.can_send tpc p l i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>e'[d'][][]Z1 Z2 _ G; subst d' e'.
(* Goal: forall _ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn, @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
move: St; rewrite/Actions.send_act_step/==>[][_][h][].
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite /pn_step -!(pf_irr C' (pn_safe_coh _))
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
        -!(pf_irr (pn_this_in _ H) (pn_this_in _ _)).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some (PCM.sort (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC)) (@mkLocal PStateT (pstep_send (@getStP cn pts others Hnin p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) (@getStL cn pts others p (getStatelet i2 l) C' (@pn_this_in cn pts others p cn H)) false)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
rewrite (getStP_K Hnin C' (pn_this_in _ H) Hpin E1)(getStL_Kp _ (pn_this_in _ H) E1)/=. 
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
case=>Z Z';subst h i3; rewrite (rely_loc' _ R3) locE//; last by apply: (cohVl C').
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
+ by rewrite -(cohD (proj2 (rely_coh R1)))/ddom domPt inE/=.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by apply: (cohS (proj2 (rely_coh R1))).
Qed.


(*****************************************************)
(*      Full participant implementation              *)
(*****************************************************)

Definition get (r : option bool) : bool :=
  if r is Some b then b else false.

(* Just one round *)
Program Definition participant_round (doCommit : bool) :
  {(el : nat * Log)}, DHT [p, W] 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i =>  loc i = st :-> (el.1, PInit) \+ log :-> el.2,
   fun (_ : unit) m => exists (b : bool)(d: data),
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     loc m = st :-> (el.1.+1, PInit) \+ log :-> (rcons el.2 (b, d)))
  := 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  Do _ (e <-- read_round_p;
      receive_prep_req_loop e;;
      resp_to_req e doCommit;;
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
      r <-- receive_commabrt_loop e doCommit;                     
      send_ack e (get r);;
      ret _ _ tt).
Next Obligation.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply:ghC=>i1[e lg]/=E1 C1; apply: step.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
apply: (gh_ex (g:=(e, PInit, lg))); apply: call_rule=>//e' i2 [E2][pf]->C2.
have X: (getStP (cn:=cn) (others:=others) Hnin  pf Pin).1 = e
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  by move: (getStP_K Hnin pf Pin Hpin E2)=>->.
rewrite X; apply: step; apply: (gh_ex (g:=lg));
apply: call_rule=>//_ i3[d][_]E3 _.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply: step; apply: (gh_ex (g:=(d, lg))).
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: call_rule=>//_ i4 E4 _.
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply: step; apply: (gh_ex (g:=(lg, d))).
(* Goal: forall (_ : @eq (option Heap.heap) (@Some Heap.heap h) (@Some Heap.heap (@mkLocal PStateT (@pair (prod nat PState) Log (@pair nat PState (S e) PInit) lg)))) (_ : @eq (UMDef.tp Label dstatelet) i3 (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) p h (dstate (getStatelet i2 l))) (@PCM.join (union_mapPCM mid (msg TaggedMessage)) (dsoup (getStatelet i2 l)) (@um_pts nat_ordType (msg TaggedMessage) (@fresh (msg TaggedMessage) (dsoup (getStatelet i2 l))) (@Msg TaggedMessage (TMsg abort_ack (@cons nat e (@Datatypes.nil nat))) p cn true)))) i2)) (_ : all_hooks_fire (@Actions.filter_hooks tpc l (@Exports.pn_abort_ack_trans cn pts others Hnin) (@PCM.unit (union_mapPCM hook_domain hook_type))) l abort_ack i2 p (@cons nat e (@Datatypes.nil nat)) cn), @eq Heap.heap (getLocal p (getStatelet i4 l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) *)
apply: call_rule=>[|r i5 [b [Z E5]] _]; first by case: doCommit E4. 
subst r; apply: step; apply: (gh_ex (g:=(d, rcons lg (b, d)))).
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: call_rule=>//= _ i6 E6 _{E4}.
apply: ret_rule=>i7 R6 {E5}; exists b, d; rewrite (rely_loc' _ R6).
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by case: b E6.
Qed.

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

(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
4 person-hours

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

(*****************************************************)
(*    Waiting for a list of incoming transactions    *)
(*****************************************************)

Definition part_with_choices_loop_spec := forall (chs : seq bool),
  {(el : nat * Log)}, DHT [p, W] 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i =>  loc i = st :-> (el.1, PInit) \+ log :-> el.2,
   fun (_ : unit) m => exists (bs : seq bool)(ds : seq data),
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
     loc m = st :-> (el.1 + (size chs), PInit) \+ log :-> (el.2 ++ (seq.zip bs ds))).
                                               

Program Definition participant_with_choices_loop : part_with_choices_loop_spec :=
  fun choices  =>
    Do (fix rec choices :=
          (match choices with
           | c :: chs => participant_round c ;; rec chs
           | [::] => ret _ _ tt
           end)) choices.
Next Obligation.
apply:ghC=>i; elim: choices i=>//=[|c cs/= Hi]i1 [e lg] E1 C1. 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
- by apply: ret_rule=>i2 R1; exists [::], [::];
                        rewrite cats0 addn0 (rely_loc' _ R1).
(* Goal: @verify p (mkWorld tpc) (option bool) i1 (receive_commabrt_loop_obligation_1 e c (@while p (mkWorld tpc) (prod Log data) (option bool) rp_commabrt_cond (rp_commabrt_inv e c) (fun (a : prod Log data) (b : option bool) (s0 s1 : state) (H : rp_commabrt_inv e c a b s0) (H0 : network_rely (mkWorld tpc) p s0 s1) => receive_commabrt_loop_obligation_2 e c a b s0 s1 H H0) (fun b : option bool => @do' p (mkWorld tpc) (option bool) (@logvar (option bool) (prod Log data) (fun a : prod Log data => @binarify (option bool) (fun s : state => and (is_true (rp_commabrt_cond b)) (rp_commabrt_inv e c a b s)) (fun (b' : option bool) (s1 : state) => rp_commabrt_inv e c a b' s1))) (receive_commabrt_loop_obligation_3 (@bind p (mkWorld tpc) (option (prod (prod nid nat) (list nat))) (option bool) (tryrecv_commabrt_req c) (fun r : option (prod (prod nid nat) (list nat)) => match r as r' return (forall _ : @eq (option (prod (prod nid nat) (list nat))) r' r, DT p (mkWorld tpc) (option bool)) with | Some p0 => let (p1, body) as p1 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) p1) r, DT p (mkWorld tpc) (option bool)) := p0 in let (from, tg) as p2 return (forall _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) p2 body)) r, DT p (mkWorld tpc) (option bool)) := p1 in fun _ : @eq (option (prod (prod nid nat) (list nat))) (@Some (prod (prod nid nat) (list nat)) (@pair (prod nid nat) (list nat) (@pair nid nat from tg) body)) r => if andb (@eq_op nat_eqType from cn) (@eq_op nat_eqType (@head nat O body) e) then @ret p (mkWorld tpc) (option bool) (@Some bool (@eq_op nat_eqType tg commit_req)) else @ret p (mkWorld tpc) (option bool) (@None bool) | None => fun _ : @eq (option (prod (prod nid nat) (list nat))) (@None (prod (prod nid nat) (list nat))) r => @ret p (mkWorld tpc) (option bool) (@None bool) end (@Logic.eq_refl (option (prod (prod nid nat) (list nat))) r)))) (receive_commabrt_loop_obligation_4 e c b)) (@None bool))) (fun (res : option bool) (m : state) => @ex bool (fun b : bool => and (@eq (option bool) res (@Some bool b)) (if b then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d)))) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts (list (prod bool (list nat))) log (@rcons (prod bool (list nat)) lg (@pair bool (list nat) b d))))))) *)
apply: step; apply: (gh_ex (g:=(e, lg))).
(* Goal: @conseq (mkWorld tpc) (list nat) p (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (@logvar (list nat) (prod data Log) (fun dl : prod data Log => @binarify (list nat) (fun i : state => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PCommitted d))) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState e (PAborted d))) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)) (fun (_ : list nat) (m : state) => (let 'pair d lg as dl' := dl return (forall _ : @eq (prod data Log) dl' dl, Prop) in fun _ : @eq (prod data Log) (@pair data Log d lg) dl => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) (@Logic.eq_refl (prod data Log) dl)))) *)
apply: call_rule=>//_ i2[b][d]/=E2 C2/=.
(* Goal: is_true (@in_mem (Equality.sort (Ordered.eqType Label)) l (@mem (Equality.sort (Ordered.eqType Label)) (seq_predType (Ordered.eqType Label)) (@UMC.dom Label dstatelet (union_mapUMC Label dstatelet) i2))) *)
(* Goal: is_true (@PCM.valid (@union_map_classPCM Label dstatelet (union_mapUMC Label dstatelet)) i2) *)
move:(Hi i2 (e.+1, rcons lg (b, d)) E2 C2)=>/=.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
apply: vrf_mono=>_ i3[bs][ds]->.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
rewrite -[e.+1]addn1 -[(size cs).+1]addn1 addnAC addnA.
(* Goal: all_hooks_fire (@Actions.filter_hooks tpc l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (geth (mkWorld tpc))) l (@t_snd (Protocols.nodes tpc) (Protocols.Exports.coh tpc) (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin)) i2 p (@cons nat e (@Datatypes.nil nat)) cn *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
exists (b:: bs), (d :: ds)=>/=.
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
by rewrite -cats1 -!catA/=.
Qed.

(* Take a list of choices and loop until they run out *)
Program Definition participant_with_choices choices:
  DHT [p, W] 
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
  (fun i =>  loc i = st :-> (0, PInit) \+ log :-> ([::] : seq (bool * data)),
   fun (_ : unit) m => exists (bs : seq bool) (ds : seq data),
(* Goal: forall (i2 : state) (_ : network_rely (mkWorld tpc) p i i2), @Actions.send_act_safe (mkWorld tpc) tpc p l (if hasCommitted then @pn_commit_ack_trans cn pts others Hnin else @pn_abort_ack_trans cn pts others Hnin) (@cons nat e (@Datatypes.nil nat)) cn i2 *)
(* Goal: @verify p (mkWorld tpc) (list nat) i (if hasCommitted then send_commit_ack e cn else send_abort_ack e cn) (fun (_ : list nat) (m : state) => if hasCommitted then @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg)) else @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (S e) PInit)) (@heap_pts Log log lg))) *)
       loc m = st :-> (size choices, PInit) \+ log :-> (seq.zip bs ds))
  := Do (participant_with_choices_loop choices).
Next Obligation.
(* Goal: @conseq (mkWorld tpc) unit p (@with_spec p (mkWorld tpc) unit (@logvar unit (prod nat Log) (fun el : prod nat Log => @binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@fst nat Log el) PInit)) (@heap_pts Log log (@snd nat Log el)))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (addn (@fst nat Log el) (@size bool choices)) PInit)) (@heap_pts (list (prod bool (list nat))) log (@cat (prod bool (list nat)) (@snd nat Log el) (@seq.zip bool data bs ds))))))))) (participant_with_choices_loop choices)) (@binarify unit (fun i : state => @eq Heap.heap (getLocal p (getStatelet i l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState O PInit)) (@heap_pts (list (prod bool data)) log (@Datatypes.nil (prod bool data))))) (fun (_ : unit) (m : state) => @ex (list bool) (fun bs : list bool => @ex (list data) (fun ds : list data => @eq Heap.heap (getLocal p (getStatelet m l)) (@PCM.join (@union_map_classPCM ptr_ordType (@dynamic Type (fun x : Type => x)) heapUMC) (@heap_pts (prod nat PState) st (@pair nat PState (@size bool choices) PInit)) (@heap_pts (list (prod bool data)) log (@seq.zip bool data bs ds))))))) *)
by move=>i/=E; apply: (gh_ex (g:=(0, [::]))); apply: call_rule.
Qed.    

End ParticipantImplementation.
End TwoPhaseParticipant.

Module Exports.
Section Exports.

Definition participant_round := participant_round.
Definition participant_with_choices_loop := participant_with_choices_loop.
Definition participant_with_choices := participant_with_choices.

End Exports.
End Exports.

End TwoPhaseParticipant.


Export TwoPhaseParticipant.Exports.
