Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas.

Set Implicit Arguments.
Local Open Scope string_scope.

Section GPS_Logic.

Variable IE : interp_env.

Inductive assn :=
  | Pure (P : Prop)
  | Base (P : RProp)
  | Conj (P P' : assn)
  | Disj (P P' : assn)
  | Impl (P P' : assn)
  | Forall A (PP: A → assn)
  | Exists A (PP: A → assn)
  | Star (P P' : assn)
  | Box (P : assn)
  | Uninit (l : nat)
  | Pt (k : fraction) (l v : nat)
  | At (l : nat) (τ : protTy) (s: prot_state τ)
  | Gres (gres : ghost_resource)
  | Escr (escr : escrowTy).

Program Definition Rat l τ s :=
  {| RP_car := fun r ⇒ ∃ S, res_get r l = p_at τ S ∧ In s (SL_list S) |}.

Fixpoint assn_sem (P : assn) { struct P } :=
  match P with
    | Pure P ⇒ Rpure P
    | Base P ⇒ P
    | Conj P P' ⇒ Rconj (assn_sem P) (assn_sem P')
    | Disj P P' ⇒ Rdisj (assn_sem P) (assn_sem P')
    | Impl P P' ⇒ Rimpl (assn_sem P) (assn_sem P')
    | Forall A PP ⇒ Rforall (fun x ⇒ assn_sem (PP x))
    | Exists A PP ⇒ Rexists (fun x ⇒ assn_sem (PP x))
    | Star P P' ⇒ Rstar (assn_sem P) (assn_sem P')
    | Box P ⇒ Rbox (assn_sem P)
    | Uninit l ⇒ Runinit l
    | Pt k l v ⇒ Rpt k l v
    | At l s τ ⇒ Rat l s τ
    | Gres g ⇒ Rgres g
    | Escr σ ⇒ Rescr σ
  end.

Definition gimp (P Q : RProp) :=
  ∀ r (SAT: P r), ghost_move IE r Q.

Definition triple P (e : exp) QQ :=
  ∃ P',
    gimp P P' ∧
    ∀ r' (SAT': P' r') n,
      safe IE n e (fun n ⇒ QQ n) r'.

Definition implies (P Q : RProp) := ∀ r (SAT: P r), Q r.

Definition riff (P Q : RProp) := ∀ r, P r ↔ Q r.

Lemma riff_refl P : riff P P.

Lemma riff_sym P Q : riff P Q → riff Q P.

Lemma riff_trans P Q R : riff P Q → riff Q R → riff P R.

Require Import Setoid.

Global Add Parametric Relation : _ riff
  reflexivity proved by riff_refl
  symmetry proved by riff_sym
  transitivity proved by riff_trans
 as riff_rel.

Global Add Parametric Morphism: implies with signature riff ⇒ riff ⇒ iff as implies_mor.

Global Add Parametric Morphism: RP_car with signature riff ⇒ eq ⇒ iff as RP_car_mor.

Global Add Parametric Morphism: Rstar with signature riff ⇒ riff ⇒ riff as Rstar_mor.

Global Add Parametric Morphism: Rconj with signature riff ⇒ riff ⇒ riff as Rconj_mor.

Global Add Parametric Morphism: Rdisj with signature riff ⇒ riff ⇒ riff as Rdisj_mor.

Global Add Parametric Morphism: Rimpl with signature riff ⇒ riff ⇒ riff as Rimpl_mor.

Global Add Parametric Morphism: Rbox with signature riff ⇒ riff as Rbox_mor.

Global Add Parametric Morphism A : (@Rforall A)
  with signature (eq ⇒ riff) ⇒ riff as Rforall_mor.

Global Add Parametric Morphism A : (@Rexists A)
  with signature (eq ⇒ riff) ⇒ riff as Rexists_mor.

Global Add Parametric Morphism: ghost_move
  with signature (eq ⇒ eq ⇒ riff ⇒ iff) as gm_mor.

Global Add Parametric Morphism: gimp
  with signature (riff ⇒ riff ⇒ iff) as gimp_mor.

Global Add Parametric Morphism: safe
  with signature (eq ⇒ eq ⇒ eq ⇒ (eq ⇒ riff) ⇒ eq ⇒ iff) as safe_mor.

Global Add Parametric Morphism: triple
  with signature (riff ⇒ eq ⇒ (eq ⇒ riff) ⇒ iff) as triple_mor.

Lemma Rstar_true P : riff (Rstar P Rtrue) P.

Lemma RstarA P Q R : riff (Rstar (Rstar P Q) R) (Rstar P (Rstar Q R)).

Lemma RstarC P Q : riff (Rstar P Q) (Rstar Q P).

Lemma RstarAC P Q R : riff (Rstar P (Rstar Q R)) (Rstar Q (Rstar P R)).

Lemma Rstar_singl a b :
  res_plus a b ≠ Rundef →
  riff (Rstar (Rsingl a) (Rsingl b)) (Rsingl (res_plus a b)).

Lemma star_disj P Q R :
  riff (Rstar P (Rdisj Q R)) (Rdisj (Rstar P Q) (Rstar P R)).

Lemma star_exists A P (QQ : A → RProp) :
  riff (Rstar P (Rexists QQ)) (Rexists (fun x ⇒ Rstar P (QQ x))).

Lemma guar_def r_pre r' α r rx :
  guar IE r_pre r' α r rx →
  r ≠ Rundef ∧ rx ≠ Rundef.

Lemma res_get_plus_naE r r' (D: res_plus r r' ≠ Rundef) k l v :
  res_get (res_plus r r') l = p_na k v →
  ∃ k', res_get r l = p_na k' v ∨ res_get r' l = p_na k' v.

Lemma res_get_plus_naI r r' (D: res_plus r r' ≠ Rundef) k l v :
  res_get r l = p_na k v ∨ res_get r' l = p_na k v →
  ∃ k', res_get (res_plus r r') l = p_na k' v.

Lemma res_get_plus_na_fullI r r' (D: res_plus r r' ≠ Rundef) l v :
  res_get r l = p_na pe_full v ∨ res_get r' l = p_na pe_full v →
  res_get (res_plus r r') l = p_na pe_full v.


Lemma Rstar_at l τ s P r :
  Rstar (Rat l τ s) P r ↔
  P r ∧ ∃ S, res_get r l = p_at τ S ∧ In s (SL_list S).

Lemma RP_strip_ext (P : RProp) r r' :
  P (res_strip r) →
  res_plus r r' ≠ Rundef →
  P (res_strip (res_plus r r')).

Lemma RP_ext_upd (P : RProp) r l pi :
  P r →
  prot_plus (res_get r l) pi = Some pi →
  P (res_upd r l pi).

Lemma implies_true : ∀ P, implies P Rtrue.

Lemma implies_false : ∀ P, implies Rfalse P.

Theorem Rbox1 P : implies (Rbox P) P.

Theorem Rbox2 P : implies (Rbox P) (Rbox (Rbox P)).

Theorem Rstar_box P Q r :
  Rstar P (Rbox Q) r ↔ P r ∧ Q (res_strip r).

Corollary Rbox_dupl P :
  riff (Rbox P) (Rstar (Rbox P) (Rbox P)).

Theorem implies_box_pure P :
  implies (Rpure P) (Rbox (Rpure P)).

Corollary Rbox_pure P : riff (Rbox (Rpure P)) (Rpure P).

Corollary Rstar_pure P Q r :
  Rstar P (Rpure Q) r ↔ P r ∧ Q.

Theorem implies_box_at l τ s :
  implies (Rat l τ s) (Rbox (Rat l τ s)).

Corollary Rbox_at l τ s :
  riff (Rbox (Rat l τ s)) (Rat l τ s).

Corollary Rat_dupl l τ s :
  riff (Rat l τ s) (Rstar (Rat l τ s) (Rat l τ s)).

Theorem implies_box_escr σ :
  implies (Rescr σ) (Rbox (Rescr σ)).

Corollary Rbox_escr σ : riff (Rbox (Rescr σ)) (Rescr σ).

Corollary Rescr_dupl σ :
  riff (Rescr σ) (Rstar (Rescr σ) (Rescr σ)).

Lemma Rstar_mono P P' Q Q' :
  implies P P' →
  implies Q Q' →
  implies (Rstar P Q) (Rstar P' Q').

Lemma RexistsI A (QQ: A → RProp) x :
  implies (QQ x) (Rexists QQ).

Lemma RexistsE A (PP: A → RProp) Q :
  (∀ x, implies (PP x) Q) →
  implies (Rexists PP) Q.

Lemma Rstar_forget_r P P' Q :
  implies P Q →
  implies (Rstar P P') Q.

Lemma Rstar_forget_l P P' Q :
  implies P' Q →
  implies (Rstar P P') Q.

Theorem Rstar_gres1 g g' r :
  Rstar (Rgres g) (Rgres g') r ↔
  ∃ g'', gres_plus g g' = Some g'' ∧ (Rgres g'') r.

Theorem Rstar_at0 l τ s tau' s' :
  implies (Rstar (Rat l τ s) (Rat l tau' s'))
          (Rpure (τ = tau')).

Theorem Rstar_at1 l τ s s' :
  implies (Rstar (Rat l τ s) (Rat l τ s'))
          (Rpure (prot_trans τ s s' ∨ prot_trans τ s' s)).

Theorem star_pt_pt k k' l v v' :
  fraction_plus k k' = None →
  riff (Rstar (Rpt k l v) (Rpt k' l v')) Rfalse.

Lemma GM_singl r : r ≠ Rundef → ghost_move IE r (Rsingl r).

Lemma GM_frame r1 r2 (Q F : RProp) :
  ghost_move IE r1 Q →
  F r2 →
  res_plus r1 r2 ≠ Rundef →
  ghost_move IE (res_plus r1 r2) (Rstar Q F).

Lemma RgresI g r :
  r ≠ Rundef →
  res_lt (Rdef (fun _ ⇒ p_bot) g (fun _ ⇒ false)) r →
  Rgres g r.

Theorem gimp_implies P Q :
  implies P Q →
  gimp P Q.

Corollary gimp_refl P : gimp P P.

Theorem gimp_trans :
  ∀ P Q R,
    gimp P Q →
    gimp Q R →
    gimp P R.

Theorem gimp_frame P Q F :
  gimp P Q →
  gimp (Rstar P F) (Rstar Q F).

Corollary gimp_frame_l P Q F :
  gimp P Q →
  gimp (Rstar F P) (Rstar F Q).

Corollary gimp_star P Q P' Q' :
  gimp P Q →
  gimp P' Q' →
  gimp (Rstar P P') (Rstar Q Q').

Theorem gimp_eintro σ P Q :
  interp_exch IE σ = (P, Q) →
  gimp P (Rescr σ).

Theorem gimp_eintro2 σ P Q :
  interp_exch IE σ = (P, Q) →
  gimp Q (Rescr σ).

Theorem gimp_eelim σ P Q :
  interp_exch IE σ = (P, Q) →
  gimp (Rstar P (Rescr σ)) Q.

Theorem gimp_eelim2 σ P Q :
  interp_exch IE σ = (P, Q) →
  gimp (Rstar Q (Rescr σ)) P.

Theorem gimp_or P1 P2 Q :
  gimp P1 Q →
  gimp P2 Q →
  gimp (Rdisj P1 P2) Q.

Theorem gimp_exists A PP Q :
  (∀ x : A, gimp (PP x) Q) →
  gimp (Rexists PP) Q.

Theorem gimp_gintro g :
  gimp Rtrue (Rexists (fun γ ⇒ Rgres (gres_one γ g))).

Theorem gimp_gupd γ g g' :
  (∀ gF, salg_plus (projT1 g) g' gF = None →
              salg_plus (projT1 g) (projT2 g) gF = None) →
  gimp (Rgres (gres_one γ (Some g)))
       (Rgres (gres_one γ (Some (existT _ _ g')))).

Lemma Permutation_consD A l (a: A) m :
  Permutation l (a :: m) →
  ∃ l1 l2, l = l1 ++ a :: l2 ∧ Permutation (l1 ++ l2) m.

Lemma Permutation_nodup_subsetD :
  ∀ A (m l rem l' : list A),
    Permutation l (m ++ rem) →
    NoDup l →
    NoDup l' →
    (∀ a, In a l → In a l') →
    ∃ rem',
      Permutation l' (m ++ rem') ∧
      (∀ x, In x rem → In x rem') ∧
      disjoint m rem'.

Theorem rule_conseq :
  ∀ P P' e QQ QQ'
         (PRE: gimp P' P)
         (T: triple P e QQ)
         (POST: ∀ n, gimp (QQ n) (QQ' n)),
    triple P' e QQ'.

Corollary rule_pconseq :
  ∀ P P' e QQ
         (PRE: gimp P' P)
         (T: triple P e QQ),
    triple P' e QQ.

Theorem rule_frame :
  ∀ P e QQ F (T: triple P e QQ),
    triple (Rstar P F) e (fun v ⇒ Rstar (QQ v) F).

Theorem rule_false e QQ : triple Rfalse e QQ.

Theorem rule_disj :
  ∀ P e QQ (T: triple P e QQ)
         P' (T: triple P' e QQ),
    triple (Rdisj P P') e QQ.

Theorem rule_exists :
  ∀ A PP e QQ (T: ∀ x: A, triple (PP x) e QQ),
    triple (Rexists PP) e QQ.

Lemma triple_conj_pure :
  ∀ (P : Prop) P' e QQ (T: ∀ (HYP: P), triple P' e QQ),
    triple (Rconj (Rpure P) P') e QQ.

Theorem rule_val P v :
  triple P (Evalue v) (fun z ⇒ if z == v then P else Rfalse).

Lemma safe_let :
  ∀ n r' e QQ (T : safe IE n e QQ r')
    e' QQ' (T' : ∀ v,
       ∃ P' : RProp,
         gimp (QQ v) P' ∧
         (∀ r', P' r' → ∀ n' (LT: lt n' n), safe IE n' (e' v) QQ' r')),
  safe IE n (Elet e e') QQ' r'.

Theorem rule_let :
  ∀ P e QQ (T: triple P e QQ) e' QQ'
    (T': ∀ v, triple (QQ v) (e' v) QQ'),
    triple P (Elet e e') QQ'.

Corollary rule_seq :
  ∀ P e Q (T: triple P e (fun _ ⇒ Q)) e' QQ'
    (T': triple Q e' QQ'),
    triple P (Elet e (fun _ ⇒ e')) QQ'.

Theorem rule_repeat :
  ∀ P e QQ
         (T: triple P e QQ)
         (IMP: implies (QQ 0) P),
    triple P (Erepeat e) (fun r ⇒ Rconj (Rpure (r ≠ 0)) (QQ r)).

Theorem rule_fork P e :
  triple P e (fun _ ⇒ Rtrue) →
  triple P (Efork e) (fun _ ⇒ Rtrue).

Theorem rule_alloc_one :
    triple (Rtrue) (Ealloc 0) (fun z ⇒ Runinit z).

Theorem rule_read_na k l v :
  triple (Rpt k l v) (Eload RATna l) (fun z ⇒ Rconj (Rpt k l v) (Rpure (z = v))).

Theorem rule_write_na l v v' :
  triple (Rpt pe_full l v) (Estore WATna l v') (fun _ ⇒ Rpt pe_full l v').

Theorem rule_write_na_uninit l v' :
  triple (Runinit l) (Estore WATna l v') (fun _ ⇒ Rpt pe_full l v').

Theorem rule_read_acq :
  ∀ τ s P QQ
         (IMP: ∀ s' (FUT: prot_trans τ s s') z,
                 implies (Rstar (interp_prot IE τ s' z) P)
                         (Rbox (QQ s' z))) typ (TYP: is_acquire_rtyp typ) l,
    triple (Rstar (Rat l τ s) P) (Eload typ l)
           (fun z ⇒ Rexists (fun s' ⇒ Rstar (Rat l τ s') (Rstar P (Rbox (QQ s' z))))).

Theorem rule_store_rel_uninit :
  ∀ typ (REL: is_release_wtyp typ) l v τ s,
    triple (Rstar (Runinit l) (interp_prot IE τ s v))
           (Estore typ l v)
           (fun _ ⇒ Rat l τ s).

Theorem rule_store_rel :
  ∀ typ (REL: is_release_wtyp typ) τ s v P Q s''
         (GHP: gimp P (Rstar (interp_prot IE τ s'' v) Q))
         (IMP: ∀ s' (FUT: prot_trans τ s s') v' r
                      (SAT: Rstar (interp_prot IE τ s' v') P r),
                 prot_trans τ s' s'') l,
    triple (Rstar (Rat l τ s) P) (Estore typ l v)
           (fun _ ⇒ Rstar (Rat l τ s'') Q).

Theorem rule_cas :
  ∀ typ1 (R1: is_release_utyp typ1) (A1: is_acquire_utyp typ1)
    typ2 (A2: is_acquire_rtyp typ2) τ s vo vn P Q R
    (GHP: ∀ s' (FUT: prot_trans τ s s'),
          gimp (Rstar (interp_prot IE τ s' vo) P)
               (Rexists (fun s'' ⇒ Rconj (Rpure (prot_trans τ s' s''))
                                (Rstar (interp_prot IE τ s'' vn) (Q s''))))) l
    (IMP: ∀ s'' (FUT: prot_trans τ s s'') y (NEQ: y ≠ vo),
                 implies (Rstar (interp_prot IE τ s'' y) P) (Rbox (R s''))),
  triple (Rstar (Rat l τ s) P)
         (Ecas typ1 typ2 l vo vn)
         (fun z ⇒ Rexists (fun s'' ⇒
                      Rstar (Rat l τ s'')
                            (if z == 0 then Rstar P (Rbox (R s''))
                             else (Q s'')))).

End GPS_Logic.