Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting Program extralib MMergesort.
Require Import GpsSepAlg GpsFraction c11 exps.

Set Implicit Arguments.
Obligation Tactic := intros; desc; try done.

Structure protTy := mkProtTy
  { prot_state : Type ;
    prot_id : nat ;
    prot_trans : relation prot_state ;
    prot_trans_ord : order _ prot_trans }.

Inductive escrowTy := mkEscrowTy (n : nat).

Definition eq_escrow (x y: escrowTy) :=
   match x, y with
     | mkEscrowTy n1, mkEscrowTy n2 ⇒ n1 == n2
   end.

Lemma eq_escrowP: ∀ x y, reflect (x = y) (eq_escrow x y).

Canonical Structure escrowTy_eqMixin := EqMixin eq_escrowP.
Canonical Structure escrowTy_eqType := Eval hnf in EqType escrowTy escrowTy_eqMixin.

Lemma prot_trans_trans : ∀ τ x y z,
  prot_trans τ x y → prot_trans τ y z → prot_trans τ x z.

Lemma prot_trans_refl : ∀ τ x, prot_trans τ x x.

Definition dec_prot_trans τ x y :=
  if excluded_middle_informative (prot_trans τ x y) then true else false.

Record slist (τ : protTy) :=
  { SL_list : list (prot_state τ) ;
    SL_nemp : SL_list ≠ nil ;
    SL_ndup : NoDup SL_list ;
    SL_sort : StronglySorted (prot_trans τ) SL_list }.

Lemma Sorted_prot τ l :
  (∀ x y, In x l → In y l → prot_trans τ x y ∨ prot_trans τ y x) →
  StronglySorted (prot_trans τ) (sort (dec_prot_trans τ) l).

Program Definition mk_slist (τ : protTy) (l : list (prot_state τ)) :
  option (slist τ) :=
  if excluded_middle_informative
       (l ≠ nil ∧ ∀ x y, In x l → In y l →
                    prot_trans τ x y ∨ prot_trans τ y x)
  then Some {| SL_list := undup (sort (dec_prot_trans τ) l) ;
               SL_ndup := nodup_undup _ |}
  else None.

Program Definition mk_slist_singl τ s : slist τ :=
  {| SL_list := s :: nil |}.

Program Definition get_state τ (l : slist τ) : prot_state τ :=
  match rev (SL_list l) with
    | nil ⇒ !
    | x :: _ ⇒ x
  end.

Lemma slist_eq τ (l l' : slist τ) :
  SL_list l = SL_list l' → l = l'.

Lemma slist_eq2 τ (l l' : slist τ) :
  (∀ x, In x (SL_list l) ↔ In x (SL_list l')) →
  l = l'.

Lemma sort_undup A (p : A → A → bool)
    (T: transitive _ p) (AS: antisymmetric _ p)
    (l : list A)
    (TOTAL: ∀ x y, In x l → In y l → p x y = true ∨ p y x = true) :
  sort p (undup l) = undup (sort p l).

Lemma undup_sort_undup A p (l : list A) :
  undup (sort p (undup l)) = sort p (undup l).

Lemma mk_slist_eq τ l l' :
  (∀ x, In x l ↔ In x l') →
  mk_slist τ l = mk_slist τ l'.

Lemma In_mk_slist τ x l S :
  mk_slist τ l = Some S → In x l → In x (SL_list S).

Lemma mk_slist_cons_in τ s S S' :
  mk_slist τ (s :: SL_list S) = Some S' →
  In s (SL_list S) →
  S = S'.

Lemma get_state_in τ (S: slist τ) : In (get_state S) (SL_list S).

Lemma get_state_lt τ (S: slist τ) s (IN: In s (SL_list S)) :
  prot_trans τ s (get_state S).

Inductive protocol :=
  | p_bot
  | p_uninit
  | p_na (k : fraction) (v : nat)
  | p_at (τ : protTy) (s : slist τ).

Inductive resource :=
  | Rundef
  | Rdef (pmap: nat → protocol)
         (gres: ghost_resource)
         (escr: escrowTy → bool).

Definition prot_plus (pi1 pi2 : protocol) :=
  match pi1, pi2 with
    | p_bot, _ ⇒ Some pi2
    | _, p_bot ⇒ Some pi1
    | p_at tau1 s1, p_at tau2 s2 ⇒
      match excluded_middle_informative (tau2 = tau1) with
        | left PF ⇒
          match mk_slist tau1 (SL_list s1 ++ eq_rect _ (fun τ ⇒ list (prot_state τ)) (SL_list s2) _ PF) with
            | Some s ⇒ Some (p_at tau1 s)
            | None ⇒ None
          end
        | _ ⇒ None
      end
    | p_na k1 v1, p_na k2 v2 ⇒
        if v1 == v2 then
          match fraction_plus k1 k2 with
            | Some k ⇒ Some (p_na k v1)
            | None ⇒ None
          end
        else None
    | _, _ ⇒ None
  end.

Definition res_emp : resource :=
  Rdef (fun _ ⇒ p_bot) gres_emp (fun _ ⇒ false).

Definition res_plus (x y : resource) : resource :=
  match x, y with
    | Rundef, _ ⇒ Rundef
    | _, Rundef ⇒ Rundef
    | Rdef pmap1 gres1 escr1, Rdef pmap2 gres2 escr2 ⇒
        match lift_plus prot_plus pmap1 pmap2 with
          | None ⇒ Rundef
          | Some pmap ⇒
            match gres_plus gres1 gres2 with
              | None ⇒ Rundef
              | Some gres ⇒
                Rdef pmap gres (fun σ ⇒ escr1 σ || escr2 σ)
            end
        end
  end.

Fixpoint rsum rl :=
  match rl with
    | nil ⇒ res_emp
    | a :: rl ⇒ res_plus a (rsum rl)
  end.

Definition res_get r loc :=
  match r with
    | Rundef ⇒ p_bot
    | Rdef pmap _ _ ⇒ pmap loc
  end.

Definition res_upd r loc pi :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef pmap gres escr ⇒
      Rdef (fun l ⇒ if l == loc then pi else pmap l) gres escr
  end.

Definition res_mupd r loc n pi :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef pmap gres escr ⇒
      Rdef (fun l ⇒ if excluded_middle_informative (loc ≤ l ≤ loc + n)
                     then pi else pmap l)
           gres escr
  end.

Definition res_gget r l :=
  match r with
    | Rundef ⇒ None
    | Rdef p g e ⇒ g l
  end.

Definition res_escr r σ :=
  match r with
      Rundef ⇒ False
    | Rdef p g e ⇒ e σ
  end.

Definition slist_lt τ (S: slist τ) (S': slist τ) :=
  ∀ s (SIN: In s (SL_list S)),
  ∃ s', In s' (SL_list S') ∧ prot_trans τ s s'.

Definition prot_trans_ok (pi1 pi2: protocol) :=
  match pi1, pi2 with
    | p_at tau1 sl1 , p_at tau2 sl2 ⇒
      ∃ (pf : tau2 = tau1),
        slist_lt sl1 (eq_rect _ slist sl2 _ pf)
    | _, _ ⇒ False
  end.

Lemma prot_plus_emp_l x : prot_plus p_bot x = Some x.

Lemma prot_plus_emp_r x : prot_plus x p_bot = Some x.

Lemma prot_plusC :
  ∀ x y, prot_plus x y = prot_plus y x.

Lemma prot_plusA :
  ∀ x y xy (P1: prot_plus x y = Some xy) z xyz
                (P2: prot_plus xy z = Some xyz),
    ∃ yz, prot_plus y z = Some yz ∧ prot_plus x yz = Some xyz.

Lemma res_plus_undef r : res_plus r Rundef = Rundef.

Lemma res_plusC x y : res_plus x y = res_plus y x.

Lemma res_plus_emp_l x : res_plus res_emp x = x.

Lemma res_plus_emp_r x : res_plus x res_emp = x.

Lemma res_plusA x y z : res_plus (res_plus x y) z = res_plus x (res_plus y z).

Lemma res_plusAC x y z : res_plus y (res_plus x z) = res_plus x (res_plus y z).

Ltac kundef :=
  match goal with
    H: _ ≠ Rundef |- _ ≠ Rundef ⇒
      let X := fresh in intro X; apply H;
      clear - X; rewrite X, ?res_plus_undef; simpl; done
  end.

Definition res_lt r r' := ∃ r_rem, res_plus r r_rem = r'.

Lemma res_lt_refl r : res_lt r r.

Lemma res_lt_trans x y z : res_lt x y → res_lt y z → res_lt x z.

Definition prot_strip (pi : protocol) :=
  match pi with
    | p_at _ _ ⇒ pi
    | _ ⇒ p_bot
  end.

Definition res_strip (r : resource) :=
  match r with
    | Rundef ⇒ Rundef
    | Rdef p g e ⇒ Rdef (fun loc ⇒ prot_strip (p loc)) (gres_strip g) e
  end.

Lemma res_strip_idemp r : res_strip (res_strip r) = res_strip r.

Lemma mk_slist_idemp τ s :
  mk_slist τ (SL_list s ++ SL_list s) = Some s.

Lemma res_plus_strip_idemp r : res_plus r (res_strip r) = r.

Lemma res_strip_plus r r' :
  res_plus r r' ≠ Rundef →
  res_strip (res_plus r r') = res_plus (res_strip r) (res_strip r').

Section Propositions.

Record RProp :=
  { RP_car :> resource → Prop ;
    RP_def : ¬ RP_car Rundef ;
    RP_ext : ∀ r (IN: RP_car r) r' (DEF: res_plus r r' ≠ Rundef),
      RP_car (res_plus r r') }.


Program Definition Rtrue := {| RP_car := fun r ⇒ r ≠ Rundef |}.
Program Definition Rfalse := {| RP_car := fun _ ⇒ False |}.

Program Definition Rpure P := {| RP_car := fun r ⇒ r ≠ Rundef ∧ P |}.

Program Definition Rsingl (r: resource) :=
  {| RP_car r'' := r'' ≠ Rundef ∧ ∃ r', r'' = res_plus r r' |}.

Program Definition Rstar (P1 P2: RProp) :=
  {| RP_car r := r ≠ Rundef ∧ ∃ r1 r2, P1 r1 ∧ P2 r2 ∧ r = res_plus r1 r2 |}.

Program Definition Rconj (P Q : RProp) :=
  {| RP_car := fun r ⇒ P r ∧ Q r |}.

Program Definition Rdisj (P Q : RProp) :=
  {| RP_car := fun r ⇒ P r ∨ Q r |}.

Program Definition Rimpl (P Q : RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧
                        (∀ r', P (res_plus r r') → Q (res_plus r r')) |}.

Program Definition Rforall A (PP : A → RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧ ∀ x, PP x r |}.

Program Definition Rexists A (PP : A → RProp) :=
  {| RP_car := fun r ⇒ r ≠ Rundef ∧ ∃ x, PP x r |}.

Program Definition Rbox (P: RProp) :=
  {| RP_car := fun r ⇒ P (res_strip r) |}.

Program Definition Runinit l :=
  {| RP_car := fun r ⇒ res_get r l = p_uninit |}.

Program Definition Rpt k l v :=
  {| RP_car := fun r ⇒ ∃ k', res_get r l = p_na k' v ∧ fraction_le k k' |}.

Definition Rgres g :=
  Rsingl (Rdef (fun _ ⇒ p_bot) g (fun _ ⇒ false)).

Program Definition Rescr σ :=
  {| RP_car := fun r ⇒ res_escr r σ |}.

End Propositions.

Structure interp_env :=
  { interp_prot : ∀ protTy, prot_state protTy → nat → RProp
  ; interp_exch : escrowTy → RProp × RProp
  ; interp_exchOK1 :
      ∀ σ r, ¬ Rstar (fst (interp_exch σ))
                              (fst (interp_exch σ)) r
  ; interp_exchOK2 :
      ∀ σ r, ¬ Rstar (snd (interp_exch σ))
                              (snd (interp_exch σ)) r }.

Section local_safety.

Variable IE : interp_env.

Definition env_move r loc val rX :=
  ∃ τ Srf,
  ≪ DEF: res_plus r rX ≠ Rundef ≫ ∧
  ≪ TOK: prot_trans_ok (res_get r loc) (res_get rX loc) ≫ ∧
  ≪ GRF: res_get rX loc = p_at τ Srf ≫ ∧
  ≪ SP : interp_prot IE τ (get_state Srf) val rX ≫.

Require Import c11.

Definition rely (r : resource) (α : act) (r': resource) :=
  match α with
    | Askip ⇒ r' = r ∧ r' ≠ Rundef
    | Aalloc l n ⇒ r' = r ∧ r' ≠ Rundef
    | Aload typ l v ⇒
         typ = RATna ∧ (∃ pmap gres escr,
                           r = Rdef pmap gres escr ∧
                           r' = r ∧ (∀ k v', pmap l = p_na k v' → v' = v))
       ∨ typ = RATrlx ∧ r' = r ∧ r' ≠ Rundef
       ∨ is_acquire_rtyp typ ∧
           ∃ rY,
             (∀ τ S, res_get r l = p_at τ S → env_move r l v rY) ∧
             r' = res_plus r (res_strip rY) ∧ r' ≠ Rundef
    | Astore typ l _ ⇒
        r' = r ∧ r' ≠ Rundef ∧
        (∀ (REL: is_release_wtyp typ) τ S, res_get r l = p_at τ S →
          ∃ v' rY, env_move r l v' rY)
    | Armw typ l v _ ⇒
      ∃ rY,
        (∀ (REL: is_release_utyp typ) (ACQ: is_acquire_utyp typ) τ S,
          res_get r l = p_at τ S → env_move r l v rY) ∧
        r' = res_plus r rY ∧ r' ≠ Rundef
  end.

Definition atomic_guar (r : resource) l v (r_sb r_rf: resource) :=
  ∃ τ s S',
    ≪ PI : interp_prot IE τ s v r_rf ≫ ∧
    ≪ REQ: res_plus r_sb r_rf = res_upd r l (p_at τ S') ≫ ∧
    ≪ Gsb: res_get r_sb l = p_at τ S' ≫ ∧
    ≪ Grf: res_get r_rf l = p_at τ S' ≫ ∧
    (≪ GET: res_get r l = p_uninit ≫ ∧
     ≪ SEQ: SL_list S' = s :: nil ≫
    ∨ ∃ S,
         ≪ GET : res_get r l = p_at τ S ≫ ∧
         ≪ LAST: ∀ s0, In s0 (SL_list S) → prot_trans τ s0 s ≫ ∧
         ≪ SEQ : ∀ s0, In s0 (SL_list S') ↔ s0 = s ∨ In s0 (SL_list S) ≫).

Definition guar (r_pre r : resource) (α : act) (r_sb r_rf: resource) :=
  match α with
    | Askip ⇒ r_sb = r ∧ r_rf = res_emp ∧ r ≠ Rundef
    | Aalloc l n ⇒ r_sb = res_mupd r l n p_uninit
                         ∧ r_rf = res_emp ∧ r ≠ Rundef
    | Aload typ l _ ⇒ r_sb = r ∧ r_rf = res_emp ∧
      ((∃ k v, res_get r l = p_na k v)
       ∨ is_acquire_rtyp typ ∧ (∃ τ S, res_get r l = p_at τ S))
    | Astore typ l v ⇒
          typ = WATna ∧ r_sb = res_upd r l (p_na pe_full v) ∧ r_rf = res_emp ∧
          (res_get r l = p_uninit ∨ ∃ v, res_get r l = p_na pe_full v)
       ∨ ≪ ISREL: is_release_wtyp typ ≫ ∧
          ≪ AG: atomic_guar r l v r_sb r_rf ≫ ∧
          ≪ NB: res_get r_pre l ≠ p_bot ≫ ∧
          ≪ WG: ∀ v' rE (RELY: env_move r_pre l v' rE),
                 prot_trans_ok (res_get rE l) (res_get r_rf l) ≫
    | Armw typ l _ v ⇒
        ≪ ISACQ: is_acquire_utyp typ ≫ ∧
        ≪ ISREL: is_release_utyp typ ≫ ∧
        ≪ AG: atomic_guar r l v r_sb r_rf ≫ ∧
        ≪ NB: res_get r_pre l ≠ p_bot ≫ ∧
        ≪ WG: ∃ τ S, res_get r l = p_at τ S ≫
  end.

Inductive ghost_elim (P1 P2 Q : RProp) r0 rE :=
  | GE_left
       (VINS: P1 rE)
       (IN' : ∀ r'', Rstar (Rsingl r0) P2 r'' → Q r'')
  | GE_right
       (VINS: P2 rE)
       (IN' : ∀ r'', Rstar (Rsingl r0) P1 r'' → Q r'').

Inductive ghost_move (r : resource) (Q : RProp) : Prop :=
  | GM_base (RINS: Q r)
  | GM_trans P (GM: ghost_move r P)
       (GM': ∀ r' (SAT: P r'), ghost_move r' Q)
  | GM_extend gone
       (PEQ : ∀ l r'' pmap g g' escr,
               gres_plus (gres_one l gone) g = Some g' →
               res_plus r (Rdef pmap g' escr) = r'' →
               r'' ≠ Rundef →
               Q r'')
  | GM_update p g e (REQ: r = Rdef p g e) g'
       (GDEF : ∀ gF, gres_plus g' gF = None → gres_plus g gF = None)
       (GDOM : ∀ gl, g gl = None → g' gl = None)
       (IN' : Q (Rdef p g' e))
  | GM_eintro σ r1 r2 P1 P2
       (ESCR: interp_exch IE σ = (P1 , P2))
       (REQ : r = res_plus r1 r2) (RDEF: r ≠ Rundef)
       (RINS: P1 r2 ∨ P2 r2)
       (IN' : Q (res_plus r1 (Rdef (fun _ ⇒ p_bot) gres_emp
                                   (fun s ⇒ s == σ))))
  | GM_eelim σ P1 P2 r0 rE
       (ESCR: interp_exch IE σ = (P1 , P2))
       (REQ : r = res_plus rE r0) (RDEF: r ≠ Rundef)
       (EIN : res_escr r σ)
       (GEL : ghost_elim P1 P2 Q r0 rE).

Lemma GM_weaken_post :
  ∀ r Q (GM: ghost_move r Q) (Q' : RProp)
         (IMP: ∀ r, Q r → Q' r),
  ghost_move r Q'.

Definition write_prot_equiv α r_pre r' :=
  match α with
    | Aalloc l n ⇒
          ∀ loc, l ≤ loc ≤ l + n → res_get r' loc = p_bot
    | Astore typ l _ ⇒
        ∀ (ISREL: is_release_wtyp typ) τ S_pre S,
          res_get r_pre l = p_at τ S_pre →
          res_get r' l = p_at τ S →
          ∃ r_env v_env,
            (∃ Sxxx, res_get r_env l = p_at τ Sxxx
                  ∧ slist_lt S Sxxx) ∧
            env_move r_pre l v_env r_env
    | Armw typ l _ _ ⇒
        ∀ (ISACQ: is_acquire_utyp typ) (ISREL: is_release_utyp typ) τ S,
          res_get r_pre l = p_at τ S →
          ∃ Su,
            res_get r' l = p_at τ Su ∧ get_state S = get_state Su
    | _ ⇒ True
  end.

Fixpoint safe n (e : exp) PP r :=
  match n with 0 ⇒ True | S n ⇒
    ≪ END: ∀ val, e = Evalue val → ghost_move r (PP val) ≫ ∧
    ≪ FORK: ∀ K (CTX: eval_ctx K) e', e = K (Efork e') →
         ∃ r1 r2, r = res_plus r1 r2 ∧
           safe n (K (Evalue 0)) PP r1 ∧
           safe n e' (fun _ ⇒ Rtrue) r2 ≫ ∧
    ≪ STEP: ∀ α e' (STEP: exp_step e α e') rF r_pre
               (RELY : rely (res_plus r rF) α r_pre),
         ∃ P',
           ghost_move r_pre P' ∧
           ∀ r' (IN': P' r') (WPE : write_prot_equiv α r_pre r'),
           ∃ r_post rx,
             guar r_pre r' α (res_plus r_post rF) rx ∧
             safe n e' PP r_post ≫
  end.

End local_safety.