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

Set Implicit Arguments.

Theorem rule_store_rel typ E E´ P (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.

  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); eauto.
    ∃ ((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; destruct n; intro v.
      specialize (h v); clear D.
      unfold hupd in *; desf; desf; ins; desf; desf; split; vauto.
      ins; desf; vauto.
      generalize (h0 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.
  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 (proj2 VALID); eauto.
  }

  eexists rfs, hN,
          (hsingl E (HVra Wemp Remp false None (Some HLCnormal)) +!+ hFR +!+ h´),
          (mk_assn_mod P);
    repeat (split; simpl; vauto); try (by ins; desf).
  { unfold mupd; desf; desf.
    rewrite pEQ, !hplusA in *; clear - pDEF.
    rewrite (hplusC hFR), hplusA, (hplusAC hN).
    remember (hN +!+ h´ +!+ hFR) as h; clear Heqh.
    cut (∃ PP QQ isrmw perm init, hf E = HVra PP QQ isrmw perm init).
    {
      intro RA; desf.
      erewrite hdef_initializeE; try exact RA.
      rewrite <- pDEF, hplusA, (hplusC h), <- hplusA; f_equal.
      rewrite hplus_hsingl; [ | by ins; split; vauto].
      ins; repeat f_equal; extensionality v.
        2: apply AsimD; vauto.
      unfold hupd, mupd; desf; desf.
      apply AsimD; rewrite <- e; apply Asim_sym, Asim_assn_norm.
    }
    apply hplus_def_inv in pDEF; desf.
    generalize (DEFv E), (PLUSv E); clear; unfold hupd; ins; desf; desf.
    eby ins; desf; repeat eexists.
  }
  { unfold mupd; desf; desf.
    rewrite <- !hplusA.
    f_equal. f_equal.
    rewrite hplus_hsingl; [ | by ins; split; vauto].
    ins; repeat f_equal; unfold hupd; desf; extensionality v; desf; apply AsimD; [
        rewrite <- e; apply Asim_assn_norm| by vauto].
  }
  { 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,; [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 E E´ P :
  triple (Astar (Arel E (mupd (fun _ ⇒ Afalse) E´ P)) (Atriangle P))
         (Estore ATrlx E E´)
         (fun _ ⇒ Arainit E).
Proof.
  eapply triple_helper_start; ins; desf; ins; subst.

  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); eauto.
    ∃ ((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; destruct n; intro v.
      specialize (h v); clear D.
      unfold hupd in *; desf; desf; ins; desf; desf; split; vauto.
      ins; desf; vauto.
      generalize (h0 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.
  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 (proj2 VALID); eauto.
  }

  eexists rfs, h2,
          (hsingl E (HVra Wemp Remp false None (Some HLCnormal)) +!+ hFR),
          (mk_assn_mod P);
    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.
    cut (∃ PP QQ isrmw perm init, hf E = HVra PP QQ isrmw perm init).
    {
      intro RA; desf.
      erewrite hdef_initializeE; try exact RA.
      rewrite <- pDEF, hplusA, (hplusC h), <- hplusA; f_equal.
      rewrite hplus_hsingl; [ | by ins; split; vauto].
      ins; repeat f_equal; extensionality v.
        2: apply AsimD; vauto.
      unfold hupd, mupd; desf; desf.
      apply AsimD; rewrite <- e; apply Asim_sym, Asim_assn_norm.
    }
    apply hplus_def_inv in pDEF; desf.
    generalize (DEFv E), (PLUSv E); clear; unfold hupd; ins; desf; desf.
    eby ins; desf; repeat eexists.
  }
  { unfold mupd; desf; desf.
    rewrite <- !hplusA.
    f_equal. f_equal.
    rewrite hplus_hsingl; [ | by ins; split; vauto].
    ins; repeat f_equal; unfold hupd; desf; extensionality v; desf; apply AsimD; [
        rewrite <- e; apply Asim_assn_norm| by vauto].
  }
  { 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´,; [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.