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

Section CalculatorServerLib.

Variable l : Label.
Variable f : input -> option nat.
Variable prec : input -> bool.
Variables (cs cls : seq nid).
Notation nodes := (cs ++ cls).
Hypothesis Huniq : uniq nodes.

Notation cal := (CalculatorProtocol f prec cs cls l).
Notation sts := (snd_trans cal).
Notation rts := (rcv_trans cal).
Notation W := (mkWorld cal).

(* A server node *)
Variable sv : nid.
Hypothesis  Hs : sv \in cs.
Notation loc i := (getLocal sv (getStatelet i l)).

(***********************)
(* Server receive loop *)
(***********************)

Export CalculatorProtocol.

Program Definition tryrecv_req_act := act (@tryrecv_action_wrapper W sv
      (fun k _ t b => (k == l) && (t == req)) _).
Next Obligation. by case/andP:H=>/eqP->; rewrite domPt inE/=. Qed.

(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
(* Receive-transition for the calculator *)
Program Definition tryrecv_req :
  {ps : reqs}, DHT [sv, W]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  (fun i => loc i = st :-> ps,
   fun (r : option perm) m =>
     match r with
     | Some (from, t, args) =>
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
       [/\ loc m = st :-> ((from, sv, args) :: ps),
        prec args & from \in cls]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
     | None => loc m = st :-> ps
     end) 
  := Do tryrecv_req_act.    
Next Obligation.
(* Goal: @verify sv (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) i1 (send_ans_act to (@cons nat ans args)) (fun (r : list nat) (m : state) => and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args))) *)
apply: ghC=>i1 ps E1 C1.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
apply: act_rule=>i2 R1; split=>//=; first by apply: (proj2 (rely_coh R1)).
(* Goal: forall (_ : @eq (option hook_type) (@UMC.find (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type) (@pair (prod (Ordered.sort nat_ordType) (Ordered.sort Label)) (prod (Ordered.sort Label) (Ordered.sort nat_ordType)) (@pair (Ordered.sort nat_ordType) (Ordered.sort Label) _z_ _lc_) (@pair (Ordered.sort Label) (Ordered.sort nat_ordType) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)))) (@PCM.unit (@union_map_classPCM (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type)))) (@Some hook_type _hk_)) (_ : 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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
move=>r i3 i4[_]/=St R3.
(* Goal: match r as r' return (forall _ : @eq (option perm) r' r, Prop) with | Some p => let (p0, args) as p0 return (forall _ : @eq (option perm) (@Some perm p0) r, Prop) := p in let (from, t) as p1 return (forall _ : @eq (option perm) (@Some perm (@pair (prod nid nat) (list nat) p1 args)) r, Prop) := p0 in fun _ : @eq (option perm) (@Some perm (@pair (prod nid nat) (list nat) (@pair nid nat from t) args)) r => and3 (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nid nid) (list nat))) st (@cons (prod (prod nid nid) (list nat)) (@pair (prod nid nid) (list nat) (@pair nid nid from sv) args) ps))) (is_true (prec args)) (is_true (@in_mem nid from (@mem nat (seq_predType nat_eqType) cls))) | None => fun _ : @eq (option perm) (@None perm) r => @eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts reqs st ps) end (@Logic.eq_refl (option perm) r) *)
case: St=>C2; case.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
- by move=>[]?->Z; subst i3;rewrite (rely_loc' _ R3) (rely_loc' _ R1).
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
case=>k[m][tms][from][rt][pf'][[F]]H1 H2 H3/andP[/eqP Z]H4/= Z'->; subst k i3. 
move: rt  pf' (coh_s l C2) H1 H2 H3 H4 R3.
rewrite prEq=>rt  pf' cohs H1 H2 H3 H4 R3.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
case: H1 H4; last by case=>//=->. 
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
move=>Z _; subst rt; move: H3; rewrite /msg_wf/=/sr_wf=>->; split=>//.
(* Goal: and (@a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2) (forall (y : list nat) (k m : state) (_ : @ex (@a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2) (fun pf : @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 => @a_step (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 pf k y)) (_ : network_rely (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) sv k m), and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) y (@cons nat ans args))) *)
set d := (getStatelet i2 l).
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
have P1: valid (dstate d) by apply: (cohVl cohs).
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
have P2: valid i2 by apply: (cohS (proj2 (rely_coh R1))).
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
have P3: l \in dom i2 by rewrite -(cohD(proj2(rely_coh R1)))domPt inE/=.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
rewrite -(rely_loc' _ R1) in E1.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
- by rewrite (rely_loc' _ R3)/= locE//=/sr_step Hs/= (getStK cohs E1).
(* Goal: is_true (@in_mem nid from (@mem nat (seq_predType nat_eqType) cls)) *)
case: (cohs)=>Cs _ _ _. move/esym: F=> F.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by case: Cs=>_/(_ _ _ F); rewrite /cohMsg/= H2/=; case.
Qed.

Definition receive_req_loop_cond (res : option (nid * input)) := res == None.

Definition receive_req_loop_inv (ps : reqs) :=
  fun (r : option (nid * input)) i =>
    match r with
     | Some (from, args) =>
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
       [/\ loc i = st :-> ((from, sv, args) :: ps),
        prec args & from \in cls]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
     | None => loc i = st :-> ps
    end.

Program Definition receive_req_loop :
  {ps : reqs}, DHT [sv, W]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  (fun i => loc i = st :-> ps,
   fun (r : option (nid * input)) m =>
     exists from args,
     [/\ r = Some (from, args),
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
      loc m = st :-> ((from, sv, args) :: ps),
      from \in cls &
      prec args]) := 
  Do _ (@while sv W _ _ receive_req_loop_cond receive_req_loop_inv _
        (fun r => Do _ (
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
           r <-- tryrecv_req;
           match r with
           | Some (from, _, args) => ret _ _ (Some (from, args))
           | None => ret _ _ None
           end)) None).

Next Obligation. by apply: with_spec x. Defined.
Next Obligation.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by move:H; rewrite /receive_req_loop_inv (rely_loc' _ H0).
Qed.
Next Obligation.
apply:ghC=>i1 ps/=[/eqP H1]L1 C1; subst r.
apply: step; apply: (gh_ex (g:=ps)).
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
apply: call_rule=>//r i2/=; case: r; last first.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
- by move=>L2 C2; apply: ret_rule=>i3 R2; rewrite -(rely_loc' _ R2) in L2.
case=>[[from to] args]E2 C2; apply: ret_rule=>i3 R2/=.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by rewrite (rely_loc' _ R2). 
Qed.
Next Obligation.
apply: ghC=>i ps E1 C1; apply: (gh_ex (g:=ps)).
(* Goal: @verify sv (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) i1 (send_ans_act to (@cons nat ans args)) (fun (r : list nat) (m : state) => and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args))) *)
apply: call_rule=>//res m[].
rewrite /receive_req_loop_cond; case: res=>//=[[from args]]_ [H1 H2]C2.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by exists from, args. 
Qed.

Program Definition blocking_receive_req :
  {ps : reqs}, DHT [sv, W]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  (fun i => loc i = st :-> ps,
   fun (r : nid * input) m =>
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
     [/\ loc m = st :-> ((r.1, sv, r.2) :: ps),
      r.1 \in cls &
      prec r.2]) :=
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  Do _ (r <-- receive_req_loop;
        match r with
        | Some res => ret _ _ res
        | None => ret _ _ (0, [::])
        end).
Next Obligation.
apply: ghC=>i ps E1 C1; apply: step; apply: (gh_ex (g:=ps)).
(* Goal: @verify sv (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) i1 (send_ans_act to (@cons nat ans args)) (fun (r : list nat) (m : state) => and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args))) *)
apply: call_rule=>//res i2[from][args][Z]E2 H1 H2 C2.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by subst res; apply: ret_rule=>i3 R2/=; rewrite (rely_loc' _ R2).
Qed.


(***************************)
(* Server sending messages *)
(***************************)


(* Generic server' send that assumes a permission to respond *)

Program Definition send_ans_act to msg :=
  act (@send_action_wrapper W cal sv l (prEq cal)
        (server_send_trans f prec cs cls) _ msg to).
Next Obligation. by rewrite /cal_sends /InMem/=; left. Qed.

Program Definition send_answer (to : nid) (args : seq nat) (ans : nat) :
  {ps : reqs}, DHT [sv, W]
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  (fun i => [/\ loc i = st :-> ps, to \in cls,
             (to, sv, args) \in ps &
             f args = Some ans],                    
   fun (r : seq nat) m =>
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
       [/\ loc m = st :-> (remove_elem ps (to, sv, args)) &
       r = ans :: args]) 
  := Do send_ans_act to (ans :: args).    
Next Obligation.
(* Goal: @verify sv (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) i1 (send_ans_act to (@cons nat ans args)) (fun (r : list nat) (m : state) => and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args))) *)
apply: ghC=>i1 ps [L1]H1 H2 H3 C1.
(* Goal: @verify sv (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) i1 (send_ans_act to (@cons nat ans args)) (fun (r : list nat) (m : state) => and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args))) *)
apply: act_rule=>i2 R1.
(* Goal: forall (_ : @eq (option hook_type) (@UMC.find (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type) (@pair (prod (Ordered.sort nat_ordType) (Ordered.sort Label)) (prod (Ordered.sort Label) (Ordered.sort nat_ordType)) (@pair (Ordered.sort nat_ordType) (Ordered.sort Label) _z_ _lc_) (@pair (Ordered.sort Label) (Ordered.sort nat_ordType) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)))) (@PCM.unit (@union_map_classPCM (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type)))) (@Some hook_type _hk_)) (_ : 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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
move: (proj2 (rely_coh R1))=>C2.
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i3 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
case: (C2)=>_ _ _ _/(_ l); rewrite prEq=>C.
(* Goal: and (@a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2) (forall (y : list nat) (k m : state) (_ : @ex (@a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2) (fun pf : @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 => @a_step (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 pf k y)) (_ : network_rely (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) sv k m), and (@eq Heap.heap (getLocal sv (getStatelet m l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) y (@cons nat ans args))) *)
set d := (getStatelet i2 l).
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
split=>//[|r i3 i4[Sf]St R3].
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
- split=>//; first 1 last.
(* Goal: all_hooks_fire (@Actions.filter_hooks (Exports.CalculatorProtocol f prec cs cls l) l (server_send_trans f prec cs cls) (geth (mkWorld (Exports.CalculatorProtocol f prec cs cls l)))) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)) i2 sv (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  + by rewrite/Actions.can_send mem_cat Hs/=
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
       -(cohD C2)/= domPt/= inE eqxx.
(* Goal: all_hooks_fire (@Actions.filter_hooks (Exports.CalculatorProtocol f prec cs cls l) l (server_send_trans f prec cs cls) (geth (mkWorld (Exports.CalculatorProtocol f prec cs cls l)))) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)) i2 sv (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  + rewrite/Actions.filter_hooks umfilt0=>???.
(* Goal: forall (_ : @eq (option hook_type) (@UMC.find (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type) (@pair (prod (Ordered.sort nat_ordType) (Ordered.sort Label)) (prod (Ordered.sort Label) (Ordered.sort nat_ordType)) (@pair (Ordered.sort nat_ordType) (Ordered.sort Label) _z_ _lc_) (@pair (Ordered.sort Label) (Ordered.sort nat_ordType) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)))) (@PCM.unit (@union_map_classPCM (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type)))) (@Some hook_type _hk_)) (_ : 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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
    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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
    apply sym_eq in F.
(* Goal: forall (_ : @eq (option hook_type) (@UMC.find (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type) (@pair (prod (Ordered.sort nat_ordType) (Ordered.sort Label)) (prod (Ordered.sort Label) (Ordered.sort nat_ordType)) (@pair (Ordered.sort nat_ordType) (Ordered.sort Label) _z_ _lc_) (@pair (Ordered.sort Label) (Ordered.sort nat_ordType) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)))) (@PCM.unit (@union_map_classPCM (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type)))) (@Some hook_type _hk_)) (_ : 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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
    move: F.
(* Goal: forall (_ : @eq (option hook_type) (@UMC.find (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type) (@pair (prod (Ordered.sort nat_ordType) (Ordered.sort Label)) (prod (Ordered.sort Label) (Ordered.sort nat_ordType)) (@pair (Ordered.sort nat_ordType) (Ordered.sort Label) _z_ _lc_) (@pair (Ordered.sort Label) (Ordered.sort nat_ordType) l (@t_snd (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls)))) (@PCM.unit (@union_map_classPCM (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type (union_mapUMC (prod_ordType (prod_ordType nat_ordType Label) (prod_ordType Label nat_ordType)) hook_type)))) (@Some hook_type _hk_)) (_ : 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 sv (getStatelet i2 _lc_)) (getLocal sv (getStatelet i2 l)) (@cons nat ans args) to *)
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
    move/find_some.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
    by rewrite dom0.
(* Goal: @send_safe (Protocols.nodes (Exports.CalculatorProtocol f prec cs cls l)) (coh (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) sv to (getStatelet i2 l) (@cons nat ans args) *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  split=>//; split=>//.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
  exists C; rewrite -(rely_loc' _ R1) in L1; rewrite (getStK C L1).
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
  by apply/hasP; exists (to, sv, args)=>//=; rewrite H3 !eqxx.
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
rewrite (rely_loc' _ R3)=>{R3}.
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
case: St=>->[b]/=[][]->->/=; split=>//.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
have P1: valid (dstate (getStatelet i2 l)). by apply: (cohVl C).
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
have P2: valid i2 by apply: (cohS (proj2 (rely_coh R1))).
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
have P3: l \in dom i2 by rewrite -(cohD(proj2(rely_coh R1))) domPt inE/=. 
(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
rewrite -(rely_loc' _ R1) in L1.
(* Goal: @eq Heap.heap (getLocal sv (getStatelet (@UMC.upd Label dstatelet (union_mapUMC Label dstatelet) l (DStatelet (@UMC.upd nat_ordType Heap.heap (union_mapUMC nat_ordType Heap.heap) sv (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem (@getSt prec cs cls sv (getStatelet i2 l) (@ss_safe_coh f prec cs cls sv to (getStatelet i2 l) (@cons nat ans args) (@Actions.safe_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (server_send_trans f prec cs cls) (@cons nat ans args) to i2 Sf))) (@pair (prod nid nid) (list nat) (@pair nid nid to sv) args))) (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 resp (@cons nat ans args)) sv to true)))) i2) l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args))) *)
by rewrite (pf_irr (ss_safe_coh _ ) C) locE// (getStK C L1).
Qed.

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

(* Goal: @a_safe (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (list nat) sv (@send_action_wrapper (mkWorld (Exports.CalculatorProtocol f prec cs cls l)) (Exports.CalculatorProtocol f prec cs cls l) sv l (prEq (Exports.CalculatorProtocol f prec cs cls l)) (server_send_trans f prec cs cls) send_ans_act_obligation_1 (@cons nat ans args) to) i2 *)
(* Goal: and (@eq Heap.heap (getLocal sv (getStatelet i4 l)) (@heap_pts (list (prod (prod nat nat) (list nat))) st (remove_elem ps (@pair (prod nat nat) (list nat) (@pair nat nat to sv) args)))) (@eq (list nat) r (@cons nat ans args)) *)
2 person-hours

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


End CalculatorServerLib.
