Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel.
Require Import fslhmap fslhmapna fslhmapa fsltriple.
Require Import GpsSepAlg.

Set Implicit Arguments.

Theorem rule_store_rel PS PSg typ E E' (P: assn PS PSg) (TYP: release_typ typ) (NORM: normalizable P) :
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E' P)) P)
         (Estore typ E E')
         (fun _ ⇒ Arainit E).
Proof.
  eapply triple_helper_start; ins; desf; ins; subst.

  red in VALID; desc; red in VALIDS; desc.

  apply NORM in pSAT2; desf.

  eapply safe_final3s with (h := (hsingl _ _ E (HVra (hupd Wemp E' (mk_assn_mod P)) Remp false
                                                     (Some HLCnormal) (Some HLCnormal))
                                  +!+ hFR +!+ h'))
                           (hs := lupd hN HLnabla)
                           (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    ∃ ((hsingl _ _ E (HVra (hupd Wemp E' (mk_assn_mod P)) Remp false (Some HLCnormal) None)) +!+ h').
    repeat eexists; try edone.
    { revert pDEF; rewrite pEQ, !hplusA, (hplusC hFR), (hplusC hN); clear.
      intros D U.
      rewrite <- !hplusA in D; eapply hplus_not_undef_l in D; rewrite hplusA in D.
      destruct (h' +!+ hFR); ins.
      rewrite hplus_unfold in *; desf; desf.
      destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; ins.
      specialize (HEAPcompat v); clear D.
      unfold hupd in *; desf; desf; ins; desf; desf; split; vauto.
      ins; desf; vauto.
      generalize (HEAPcompat0 E'); clear; unfold Acombinable, mupd; ins; desf; vauto.
    }
    { clear; rewrite (hplusAC (hsingl _ _ _ _)), <- !hplusA, hplus_hsingl; try by vauto.
      ins; desf; repeat f_equal.
      extensionality v; unfold hupd; desf; desf; f_equal.
      by apply AsimD; vauto.
    }
  red in CONS; desc; ins.
  pose proof (has_rf_succs fst FIN Crf); desc; red; ins; desf; unfold NW.
  ∃ gres_emp; split.
     by unfold ga_clear; split; ins; desf.
  eapply hdef_alt in pDEF; desf.
  eexists prev, next.
  unfold mupd at 1 2 3 4 5 6; desf; desf.
  repeat (eexists; try edone).
  right; split; [by destruct TYP; desf|].

  assert (Ndef: hN ≠ Hundef) by (by intro U; rewrite U, !hplus_undef_l, !hplus_undef_r in *).
  assert (rfsEMP: hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
  {
    rewrite hsum_eq_emp; ins.
    repeat (rewrite In_map in *; desf).
    eapply RESTR; eauto.
  }

  eexists rfs, hN,
          (hsingl _ _ E (HVra Wemp Remp false None (Some HLCnormal)) +!+ hFR +!+ h'),
          (mk_assn_mod P), hemp, hemp; rewrite !hplus_emp_r; repeat (split; simpl; vauto); try (by ins; desf).
  { rewrite pDEF in ×.
    rewrite hdef_initializeE2, pEQ, !hplusA.
      rewrite !(hplusAC h'); f_equal.
      rewrite !(hplusAC hFR); f_equal.
      rewrite <- (hplusC hN), !(hplusAC hN); f_equal.
      rewrite !hplus_init1.
      f_equal. f_equal. f_equal.
      clear; exten; ins.
      by unfold mupd, hupd; desf; desf.
    rewrite hplusA in pEQ; symmetry in pEQ; eapply hplus_has_atomic_l in pEQ; ins; desf; eauto.
    by rewrite hupds.
  }
  { unfold mupd; desf; desf.
    by rewrite <- !hplusA, hplus_init1.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l.
    unfold mupd; desf; desf.
    rewrite hplusC.
    eapply hplus_sim_def.
      by apply lupd_sim.
    rewrite hplusAC, (hplusC hFR).
    rewrite pDEF, !hplusA in pEQ; clear - pEQ.
    destruct (hN +!+ h' +!+ hFR).
      by rewrite hplus_undef_r in pEQ; congruence.
    rewrite hplus_unfold in *; desf; desf.
    destruct n; unnw; split; ins.
    specialize (HEAPcompat v); unfold hupd; desf; desf.
    rewrite hupds in HEAPcompat; ins; desf; desf.
    split; ins.
    generalize (HEAPcompat0 v); clear; ins; desf; desf; unfold mupd in *; desf; desf.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l.
    unfold mupd; desf; desf.
    by apply Hsim_sym, lupd_sim.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l; unfold mupd; desf; desf.
    by apply lupd_label.
  }
  { eexists hN; split; [by rewrite assn_sem_assn_norm | ].
    do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l; unfold mupd; desf; desf.
    split; [apply Hsim_sym, lupd_sim | done].
    by intro U; rewrite U, !hplus_undef_l, !hplus_undef_r in ×.
  }
  by right; destruct TYP; desf.
Qed.

Theorem rule_store_rlx PS PSg typ E E' (P: assn PS PSg) (AT: typ ≠ ATna):
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E' P)) (Atriangle P))
         (Estore typ E E')
         (fun _ ⇒ Arainit E).
Proof.
  eapply triple_helper_start; ins; desf; ins; subst.

  red in VALID; desc; red in VALIDS; desc.

  eapply safe_final3s with (h := (hsingl _ _ E (HVra (hupd Wemp E' (mk_assn_mod P)) Remp false
                                                     (Some HLCnormal) (Some HLCnormal)) +!+ hFR))
                           (hs := lupd h' HLnabla)
                           (ga' := ga_clear ga fst); eauto.
    by ins; apply ga_clear_agrees; congruence.
    by eauto using ga_clear_fin.
    ∃ ((hsingl _ _ E (HVra (hupd Wemp E' (mk_assn_mod P)) Remp false (Some HLCnormal) None))).
    repeat eexists; try edone.
    { revert pDEF; rewrite pEQ, !hplusA, (hplusC h2); clear.
      intros D U.
      rewrite <- hplusA in D; eapply hplus_not_undef_l in D.
      destruct hFR; ins.
      rewrite hplus_unfold in *; desf; desf.
      destruct n; unnw; rewrite gres_plusC, gres_plus_emp_r; split; ins.
      specialize (HEAPcompat v); clear D.
      unfold hupd in *; desf; desf; ins; desf; desf; split; vauto.
      ins; desf; vauto.
      generalize (HEAPcompat0 E'); clear; unfold Acombinable, mupd; ins; desf; vauto.
    }
    { clear. rewrite (hplusC hFR), <- !hplusA, hplus_hsingl; try by vauto.
      ins; desf; repeat f_equal.
      extensionality v; unfold hupd; desf; desf; f_equal.
      by apply AsimD; vauto.
    }
  red in CONS; desc; ins.
  pose proof (has_rf_succs fst FIN Crf); desc; red; ins; desf; unfold NW.
  eapply hdef_alt in pDEF; desf.
  ∃ gres_emp; split.
     by unfold ga_clear; split; ins; desf.
  eexists prev, next.
  unfold mupd at 1 2 3 4 5 6; desf; desf.
  repeat (eexists; try edone).
  right; split; [done|].

  assert (rfsEMP: hsum (map hmap (map (hb_rf fst) rfs)) = hemp).
  {
    rewrite hsum_eq_emp; ins.
    repeat (rewrite In_map in *; desf).
    eapply RESTR; eauto.
  }

  eexists rfs, h2,
          (hsingl _ _ E (HVra Wemp Remp false None (Some HLCnormal)) +!+ hFR),
          (mk_assn_mod P), hemp, hemp; rewrite !hplus_emp_r; repeat (split; simpl; vauto); try (by ins; desf).
  { unfold mupd; desf; desf.
    rewrite pEQ, !hplusA in *; clear - pDEF.
    rewrite (hplusC hFR).
    remember (h2 +!+ hFR) as h; clear Heqh.
    rewrite hdef_initializeE2, <- pDEF, hplusA, (hplusC h).
      rewrite <- !hplusA, !hplus_init1.
      repeat f_equal.
      by clear; exten; ins; unfold hupd, mupd; desf; desf.
    eapply hplus_has_atomic_l in pDEF; ins; desf; eauto.
    by rewrite hupds.
  }
  { unfold mupd; desf; desf.
    by rewrite <- hplusA, hplus_init1.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l.
    unfold mupd; desf; desf.
    rewrite hplusC.
    eapply hplus_sim_def.
      eby eapply lupd_sim, assn_sem_def.
    eapply hplus_sim_def.
      by exact pSAT4.
    rewrite pDEF, !hplusA in pEQ; clear - pEQ.
    rewrite hplusAC.
    destruct (h2 +!+ hFR).
      by rewrite hplus_undef_r in pEQ; congruence.
    rewrite hplus_unfold in *; desf; desf.
    destruct n; unnw; split; ins.
    specialize (HEAPcompat v); unfold hupd; desf; desf.
    rewrite hupds in HEAPcompat; ins; desf; desf.
    split; ins.
    generalize (HEAPcompat0 v); clear; ins; desf; desf; unfold mupd in *; desf; desf.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l.
    unfold mupd; desf; desf.
    eapply Hsim_sym, Hsim_trans; try edone.
    eby eapply lupd_sim, assn_sem_def.
  }
  { do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l; unfold mupd; desf; desf.
    eby eapply lupd_label, assn_sem_def.
  }
  { eexists h'; split; [by rewrite assn_sem_assn_norm | ].
    do 2 (rewrite map_upd_irr; ins).
    rewrite rfsEMP, hplus_emp_l; unfold mupd; desf; desf.
    split; [eby eapply Hsim_sym, lupd_sim, assn_sem_def | done].
  }
Qed.