Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import Omega List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

Definition pre_write_prot_equiv IE acts amap (mo : relation actid) L b r_pre r' :=
  match amap b with
    | Aalloc l n ⇒
          ∀ loc, l ≤ loc ≤ l + n → res_get r' loc = p_bot
    | Astore typ l _ ⇒
        ∀ (ISREL: is_release_wtyp typ) tau S,
          res_get r_pre l ≠ p_bot →
          res_get r' l = p_at tau S →
          ∃ a,
            << INa : In a acts >> ∧
            << MO : immediate mo a b >> ∧
            << Wa : is_writeL (amap a) l >> ∧
          ∃ v_env,
            (∃ Sxxx, res_get (out_rf (b::acts) L a) l = p_at tau Sxxx ∧
                          slist_lt S Sxxx) ∧
            env_move IE r_pre l v_env (out_rf (b::acts) L a)
    | Armw typ l _ _ ⇒
        ∀ (ISACQ: is_acquire_utyp typ) (ISREL: is_release_utyp typ) tau S,
          res_get r_pre l = p_at tau S →
          ∃ Su,
            res_get r' l = p_at tau Su ∧ get_state S = get_state Su
    | _ ⇒ True
  end.

Lemma pwpe :
  ∀ b acts amap sb rf mo sc
    (CONS : Consistent (b :: acts) amap sb rf mo sc)
    (ND' : NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (PI : pres_in sb rf b acts)
    L IE
    (RELY : rely IE (in_sb (b :: acts) L b) (amap b)
      (in_sb (b :: acts) L b +!+ in_rf (b :: acts) L b))
    EE r
    (V : ∀ a : actid, In a acts → valid_node IE (b :: acts) (b::acts) amap rf L EE a)
    (CC : compat amap sb rf (upd L (TsbS b) (L (TsbS b) +!+ r)))
    (CO : conform (b :: acts) amap mo L acts)
    (VG : valid_ghost (incoming (b :: acts) L b)
      (r +!+ out_esc (b :: acts) L EE b))
  (RS : res_lt (res_strip (incoming (b :: acts) L b)) r)
  (NDE: NoDup EE)
  (LR : label_restr (b :: acts) amap sb rf L EE),
   pre_write_prot_equiv IE acts amap mo L b
     (in_sb (b :: acts) L b +!+ in_rf (b :: acts) L b) (incoming (b :: acts) L b).
Proof.
  red; ins; destruct (amap b) eqn: W; ins; desf; desf; ins.

Case "Aalloc".
  apply NNPP; intro IN.
  exploit visible_allocation; eauto; intro M; desf.
  red in CONS; desc; destruct (Ca _ _ _ M0 _ _ _ W); clarify; try omega.
  by edestruct ACYC; eauto.

Case "Astore".
  assert (GG := vghost_get_at _ VG RS _ H0); clear H0.

  assert (RG: ∃ S_pre, res_get (in_sb (b :: acts) L b +!+ in_rf (b :: acts) L b) l = p_at tau S_pre).
    eby eapply vghost_get_back; eauto; rewrite res_plusA.
  clear H; desf.

  edestruct res_get_plus with
    (r := in_sb (b :: acts) L b +!+ in_rf (b :: acts) L b)
    (r' := in_esc (b :: acts) L b) as (S' & EQ & SUB); eauto.
    unfold incoming in *; rewrite res_plusA; red in VG; desc; congruence.

  unfold incoming in VG.
  rewrite res_plusA in ×.
  exploit vghost_get_at; eauto.
  intro Z; rewrite Z in *; desf.

  exploit exists_immediate_helper; (try solve [clear CC; eauto]); eauto using compat_mon_upd.
    by rewrite W.
  intro AW; desf.
  unfold NW in ×.
  eexists; split; [|split; [|split]]; eauto.

  inv ND'.
  desf; generalize (V _ INa); intro V'; red in V'; desf.
  assert (DEF: in_sb (b :: acts) L b +!+ L (TrfS a) ≠ Rundef).
    by eapply helper_plus_insb_rfS_def; eauto using compat_mon_upd.

  assert (K := res_plus_get1 _ _ l DEF).

  unfold env_move, NW.

  assert (AG: ∃ v0, atomic_guar IE r0 l v0 (out_sb (b :: acts) L a)
                                            (out_rf (b :: acts) L a)).
    by red in GUAR; desf; desf; ins; desf; vauto.

  desf; generalize AG; red in AG; desc; intros; desf;
   revert DEF K; rewrite RELY, RG, Grf in *;
  rewrite VrfS, Grf; ins; desf; eauto using no_rmw_between; try by rewrite W in ×.

  SCase "initialization write".
    edestruct visible_atomic with (b:=b) (l:=l) as [c ?];
      try solve [clear CC; eauto]; eauto using compat_mon_upd; desf.
    assert (In c acts) by eauto using pres_in_hb.

    assert (get_state S' = s) by (destruct S'; ins; desf).

    destruct (eqP c a) as [|NEQ]; [subst; rewrite Grf in *; desf|].

    do 4 try (eexists; try edone); repeat split; repeat ∃ eq_refl; try edone.
    by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.

  red in CONS; desc; eapply Cmo in NEQ; desf; eauto.
  2: by eapply MO in NEQ; ins; eauto; eapply Cmo; eauto; rewrite W.

  eapply CO in NEQ; eauto.
  rewrite H4, Grf in *; ins; desf.
  rewrite <- eq_rect_eq in ×.
    do 4 try (eexists; try edone); repeat split; repeat ∃ eq_refl; try edone.
      by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.
    by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.
    by destruct (amap c); ins; desf.

  SCase "normal write".

  assert (get_state S' = s).
    by eapply get_state_eq_prove; ins; rewrite SEQ in *; desf;
       eauto using prot_trans_refl.

  edestruct visible_atomic with (b:=b) (l:=l) as [c ?];
      try solve [clear CC; eauto]; eauto using compat_mon_upd; desf.
    assert (In c acts) by eauto using pres_in_hb.

    destruct (eqP c a) as [|MO']; [subst; rewrite Grf in *; desf|].
  do 4 try (eexists; try edone); repeat split; repeat ∃ eq_refl; try edone.
  by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.

  red in CONS; desc; eapply Cmo in MO'; desf; eauto.
  2: by eapply MO in MO'; ins; eauto; eapply Cmo; eauto; rewrite W.

  eapply CO in MO'; eauto.
  rewrite H5, Grf in *; ins; desf.
  rewrite <- eq_rect_eq in ×.
  do 4 try (eexists; try edone); repeat split; repeat ∃ eq_refl; try edone.
    by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.
  by eapply slist_lt_trans; eauto; red; eauto using prot_trans_refl.
  by destruct (amap c); ins; desf.

Case "Armw".
  edestruct res_get_plus with (r' := in_esc (b :: acts) L b) as (S' & EQ & SUB); eauto.
  unfold incoming in *; rewrite res_plusA; red in VG; desc; congruence.
  rewrite res_plusA in ×.
  exploit visible_atomic; try solve [clear CC; eauto]; eauto using compat_mon_upd.
  intro M; desf.

  red in CONS; desc; red in Cmo; desc.
  specialize (Crf b).
  destruct (rf b) as [b_rf|] eqn: RF; desf.
  2: by edestruct Crf; eauto; rewrite W; ins.
  rewrite W in *; ins; desf.
  assert (INb: In b_rf acts) by (by eapply PI in RF).
  specialize (V _ INb); red in V; desf.

  destruct (classic (a = b_rf)) as [|NEQ]; desf.

  SCase "equal".
    rewrite <- (VrfM b) in M2; auto using in_eq.
    2: by rewrite W.
    ins; desf; desf.
    generalize H; unfold in_rf; rewrite res_plusC; intro.
    eapply res_get_sum with (l := map L (map (Trf^~ b) (b :: acts))) in M2; desf; eauto.
    2: by intro X; rewrite X in ×.
    2: by eapply in_map, in_map_iff; eauto using in_cons.
    eapply res_get_plus with (r' := in_sb (b :: acts) L b) in M2.
    2: by intro X; rewrite X in ×.
    desf; rewrite M2 in *; desf.

    eapply vghost_get_at in VG; try edone.
    eexists; split; eauto.
    eapply get_state_eq_incl_helper; eauto.
    eapply slist_lt_trans with S'; eauto.
      by red; eauto using prot_trans_refl.
    eapply slist_lt_trans with S'0; eauto.
    by red; eauto using prot_trans_refl.
    by rewrite W.

  SCase "non-equal".
    eapply Cmo1 in NEQ; desf; eauto.
    2: by edestruct Cwr; eauto; instantiate;
          rewrite W; ins; destruct (amap a).
    eapply CO in NEQ; eauto using pres_in_hb.
    rewrite M2, <- (VrfM b) in NEQ; auto using in_eq.
    2: by rewrite W.
    ins; desf; desf.
    generalize H; unfold in_rf; rewrite res_plusC; intro.
    eapply res_get_sum with (l := map L (map (Trf^~ b) (b :: acts))) in Heq;
      desf; eauto.
    2: by intro X; rewrite X in ×.
    2: by eapply in_map, in_map_iff; eauto using in_cons.
    eapply res_get_plus with (r' := in_sb (b :: acts) L b) in Heq.
    2: by intro X; rewrite X in ×.
    desf; rewrite Heq in *; desf.

    eapply vghost_get_at in VG; try edone.
    eexists; split; eauto.
    eapply get_state_eq_incl_helper; eauto.
    eapply slist_lt_trans with S'; eauto.
      by red; eauto using prot_trans_refl.
    eapply slist_lt_trans with S'0; eauto.
    eapply slist_lt_trans with s; eauto.
    by red; eauto using prot_trans_refl.
    by rewrite W.
    by destruct (amap a); ins; desf.
Qed.

Lemma wpe :
  ∀ IE b acts amap mo L r_pre r r' r'',
    pre_write_prot_equiv IE acts amap mo L b r_pre r →
    valid_ghost r (r' +!+ r'') →
    res_lt (res_strip r) r' →
    write_prot_equiv IE (amap b) r_pre r'.
Proof.
  unfold pre_write_prot_equiv, write_prot_equiv; ins; desf; ins.
  Case "Aalloc".
    exploit H; eauto; clear - H0; red in H0; desf; intro M; ins.
    destruct r'; ins; desf; inv_lplus loc.
    by rewrite M in *; unfold prot_plus in *; desf.
  Case "Awrite".
    exploit H; clear H; eauto using vghost_get_back_at; try congruence.
    by intro; desf; eauto 10.
  Case "Armw".
    exploit H; eauto; ins; desf; eauto using vghost_get_at.
Qed.