Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel.
Require Import rslhmap rslhmapna rslhmapa rsltriple rslmodel.

Set Implicit Arguments.

Lemma no_acq_reads_from_na_one :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    wpre w (INw: In w V)
    l v (LAB: is_writeLV (lab w) l v)
    (SBw: sb wpre w) hw
    (MAPw: hmap (hb_sb wpre w) = Hdef hw)
    (HW: is_val (hw l))
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
    PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
  False.
Proof.
  intros.
  exploit (heap_loc_na_allocated FIN ACYCLIC CONS_A HC VALID
                                    (hb_sb wpre w) SBw); ins; eauto with hb.
  desc; intros.
  assert (In cpre V) by (desf; eauto with hb).
  clear SBw INw MAPw HW x4.
  edestruct (wellformed_only_reads_helper (fun A ⇒ False))
    with (v := v) (T := hb_sb rpre r :: nil); eauto; ins; desf.
  by instantiate (1 := nil); vauto.
  by ins.
  by ins.
  by ins.
  by red; ins; desf; ins; desf; eauto using t_step with hb.
  by rewrite hsum_one.
  by intros; eapply vshift_hack in VS; desf; rewrite G in *; desf.

  intros; eapply vshift_hack in VS; desf; rewrite G in *; desf.
  by erewrite ALLOC in x3; eauto; []; desf.
Qed.

Lemma load_helper1 :
  ∀ mt lab sb fst acts_ctx rf mo sc
    (CONS : weakConsistent (fst :: acts_ctx) lab sb rf mo sc mt)
    V (HC : hist_closed mt lab sb rf mo V)
    hmap (VALID : hmap_valids lab sb rf hmap V)
    prev (V_PREV : In prev V)
    (FST : unique (sb^~ fst) prev)
    (NIN : ¬ In fst V)
    hoo (Z : hmap (hb_sb prev fst) = Hdef hoo)
    E PP QQ QQ0
    (Z0 : hoo E =
          HVra PP (fun x : val ⇒ mk_assn_mod (Astar (QQ x) (QQ0 x))) false true)
    wri (INwri : In wri V)
    pre (pU : unique (sb^~ wri) pre)
    post
    hf (pEQ0 : hmap (hb_sb pre wri) = Hdef hf)
    typW vW (EQ : lab wri = Astore typW E vW)
    (WRI : is_writeLV (lab wri) E vW)
    sws hsink P
    (UPD : vshift (Hdef (initialize hf E))
                  (hsingl E (HVra (hupd Wemp vW P) Remp false true) +!+
                   hmap (hb_sb wri post) +!+
                   hsum (map (mclearw hmap wri V) (map (hb_sw wri) sws)) +!+ hsink))
    (TRAN : assn_sem (sval P) (hsum (map (mclearw hmap wri V) (map (hb_sw wri) sws)) +!+ hsink))
    (swsND : NoDup sws)
    (swsOK : ∀ x : nat, In x sws ↔ ann_sw lab rf wri x),
   ∃ h1 hsink' : heap, hsink = h1 +!+ hsink' ∧ assn_sem (QQ vW) h1.
Proof.
  ins; red in CONS; desc.
  assert (XXX: ∃ PW QW isrmwW initW, hf E = HVra PW QW isrmwW initW ∧ PW vW = P).
  {
    rewrite vshift_hack in UPD.
    symmetry in UPD; apply hplus_def_inv in UPD; desf.
    generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds;
    clear - TRAN.
    ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
    by rewrite e in TRAN; ins.
  }
  desf.

  pose proof (read_loses_perm1 hmap lab sb rf E vW V swsND); desc.

  exploit (wellformed_one_w FIN IRR Ca HC VALID pre INwri EQ (proj1 pU) pEQ0 XXX
                          prev fst V_PREV (proj1 FST) NIN l); eauto using hupds.
    by ins; eapply EQl in IN; desc.
    by ins; eapply swsOK; eapply EQl in IN; desc.
    by ins; eapply EQl in IN; desc.
  eapply vshift_def, hdef_alt, hplus_not_undef_r in UPD.
  simpl; intro S; desf.
  eapply sim_assn_sem in S1; try eapply Asim_assn_norm.
  destruct S1 as (ha & hb & DEF & <- & S1 & _).
  cut (∃ hsink', hsink = ha +!+ hsink').
    by intro; desf; repeat eexists; vauto.

  revert S S0 UPD.
  eapply perm_from_subset with (l:=sws) in NDl; desc.
  2: by clear - EQl; intros ? X; rewrite In_map in X;
        destruct X as ([a b] & <- & X); apply EQl in X; desc.
  rewrite (hsum_perm (Permutation_map _ (Permutation_map _ NDl))), !map_app, hsum_app.

  destruct (eqP (assn_norm (QQ vW)) Aemp) as [EMP|NEMP].
    eapply sim_assn_sem in S1; [|apply Asim_sym, Asim_assn_norm].
    by rewrite EMP in S1; ins; desf; eexists; rewrite hplus_emp_l.

  assert (CONTRA: sval (mk_assn_mod (Astar (QQ vW) (QQ0 vW))) ≠ Aemp).
    by simpl; intro H; apply assn_norm_star_eq_emp in H; desf.

  assert (CONTRA': sval (mk_assn_mod (Astar (QQ vW) (QQ0 vW))) ≠ Afalse).
    by simpl; intro H; apply assn_norm_star_eq_false in H; desf;
       apply (sim_assn_sem (Asim_assn_norm _)) in S1; rewrite H in S1.

  assert (L: hsum (map (mclearw hmap wri V) (map (hb_sw wri) l'')) = hemp).
  {
    eapply (Permutation_NoDup NDl) in swsND.
    eapply nodup_app, proj2, proj2 in swsND.
    assert (M: ∀ r P, In r l'' → In r V →
            read_loses_perm hmap lab sb rf r E vW P → False).
      intros; exploit EQl'; eauto; [|intro; desf].
        by apply (Permutation_in _ (Permutation_sym NDl)), In_appI2.
      by eapply swsND in H; eauto; eapply In_map; vauto.
    assert (N: ∀ r, In r l'' → ann_sw lab rf wri r).
      intros; apply swsOK.
      by apply (Permutation_in _ (Permutation_sym NDl)), In_appI2.
    clear - EQ Crf N M VALID HC FST Z Z0 CONTRA CONTRA' IRR Ca INwri V_PREV.
    induction l''; ins; desf; rewrite hsum_cons, IHl'', hplus_emp_r; ins; eauto.

    apply/inP in Heq0; generalize (VALID _ Heq0); intro VAL.
    specialize (N _ (In_eq _ _)).
    specialize (fun P ⇒ M a P (In_eq _ _) Heq0); eauto.
    clear IHl'' Heq.
    generalize N; intros (_ & ACQ & RF).
    red in VAL; desf; desf; clear ACQ.

    destruct (M P); clear M.
    specialize (Crf a); rewrite RF in Crf; desc.
    rewrite EQ, Heq in *; ins; desf.
    do 4 eexists; unfold NW; repeat (split; try edone).
    assert (sws = wri :: nil); subst; ins.
      apply NoDup_eq_one; ins; rewrite swsOK in *; eauto.
      red in N; red in IN; desc; congruence.
    rewrite hsum_one in ×.
    red in N; desc; rewrite RF in *; desf.
    apply hdef_alt in qD; desc; rewrite qD in *; symmetry in qEQ.
    apply hplus_def_inv in pEQ'; desf.
    apply hplus_def_inv in qEQ; desf.
    apply hplus_def_inv in qEQ0; desf; eauto.

    specialize (DEFv l0); specialize (PLUSv l0);
    specialize (DEFv0 l0); specialize (PLUSv0 l0);
    specialize (DEFv1 l0); specialize (PLUSv1 l0); rewrite hupds in *; ins; desf;
    unfold hvplus in *; ins; desf; eauto;
    try solve [destruct FST, qU, CONTRA; eapply heap_loc_ra_no_own with (v:=v0) in Z0;
               try exact PLUSv0; eauto; ins; desf];
   repeat (eexists; try edone); instantiate; rewrite hupds; ins.
   by left; split; try done; Asim_simpl.
   by right; repeat (eexists; try edone); Asim_simpl; eauto using Asim.
   by left; split; try done; Asim_simpl; eauto using Asim.
   by right; repeat (eexists; try edone); Asim_simpl; eauto using Asim.

   specialize (Crf a); rewrite RF in Crf; desc.
   rewrite EQ, Heq in *; ins; desf.
   by destruct FST, pU, CONTRA; eapply heap_loc_ra_no_own with (v:=v0) in Z0;
      try exact PLUSv0; eauto; ins; destruct Z0; eauto with hb.
  }
   
   
  {
  unfold actid in *; rewrite L, hplus_emp_r.
  rewrite sim_assn_sem in S2; [|apply Asim_foldr_simpl].
  destruct S2 as (h2a & h2b & _ & <- & S2 & _).
  rewrite hplusAC.
  generalize (fun r P IN ⇒ proj2 (proj2 (proj1 (swsOK _) (proj1 (EQl r P IN))))) as X.
  generalize (fun r P IN ⇒ proj2 (proj2 (EQl r P IN))) as Y.
  generalize (fun r P IN ⇒ proj1 (proj2 (EQl r P IN))) as ZZ.
  clear TRAN; revert h2a S2; clear.

  induction l as [|[a b] l]; ins; subst;
    rewrite ?hsum_nil, ?hsum_cons, ?hplus_emp_l in *; vauto.
    by rewrite hplusA; vauto.
  desf; desf; apply/inP in Heq0; [|by exfalso; eauto].
  rewrite !hplusA in *; rewrite hplusAC in UPD.
  eapply IHl; eauto.
  specialize (Y _ _ (In_eq _ _)); ins.
  clear - S S0 S3 Y X.
  red in Y; desc.
  red in Lw; rewrite (X _ _ (In_eq _ _)) in *; clear Y0 X; desf.
  symmetry in S0.
  destruct b as [Q bbb]; unfold ssnd in *; simpls; clear bbb.
  apply PREC, proj2 in S0; congruence.
  }
Qed.

Lemma rmw_rf_uniq :
  ∀ lab sb rf mo
    (Crf : ConsistentRF_basic lab sb rf mo)
    (Cmo : ConsistentMO lab sb rf mo)
    (Crmw : AtomicRMW lab rf mo) a wri
    (RF1 : rf a = Some wri) b
    (RF2 : rf b = Some wri) typ1 l1 v1 v1'
    (LAB1 : lab a = Armw typ1 l1 v1 v1') l2 typ2 v2 v2'
    (LAB2 : lab b = Armw typ2 l2 v2 v2'),
    a = b.
Proof.
  ins; destruct (eqP a b) as [|NEQ]; ins; exfalso.
  assert (l1 = l2); subst.
    generalize (Crf a); rewrite RF1, LAB1; ins.
    generalize (Crf b); rewrite RF2, LAB2; ins; desf.
    by destruct (lab wri); ins; desf.
  eapply Crmw in RF1; [|by rewrite LAB1].
  eapply Crmw in RF2; [|by rewrite LAB2].
  red in Cmo; desc; eapply Cmo1 in NEQ; rewrite ?LAB1, ?LAB2; try done.
  destruct RF1, RF2, NEQ; eauto.
Qed.

Lemma rmw_helper0 :
  ∀ mt fst acts lab sb rf mo sc
    (CONS : weakConsistent (fst :: acts) lab sb rf mo sc mt)
    typ E E' E'' (LAB : lab fst = Armw typ E E' E'')
    prev (FST : unique (sb^~ fst) prev)
    V (V_PREV : In prev V)
    (HC : hist_closed mt lab sb rf mo V)
    hmap (VALID : hmap_valids lab sb rf hmap V)
    (NIN : ¬ In fst V)
    hoo (Z : hmap (hb_sb prev fst) = Hdef hoo)
    PP QQ (Z0 : hoo E = HVra PP (fun x : val ⇒ mk_assn_mod (QQ x)) true true)
    wri (RF : rf fst = Some wri)
    sws (INsws: ∀ x, In x sws → ann_sw lab rf wri x),
  hsum (map (mclearw hmap wri V) (map (hb_sw wri) sws)) = hemp.
Proof.
  induction sws; ins; desf; ins; rewrite hsum_cons, IHsws, hplus_emp_r; eauto.
  specialize (INsws _ (In_eq _ _)); generalize (proj2 INsws); ins; desc.
  red in CONS; desc.
  generalize (Crf a); rewrite H0; ins; desc; revert H.
  apply/inP in Heq0; generalize (VALID _ Heq0); intro VV.
  red in VV; desf; desf; intros _.
  2: by (assert (fst = a); subst; eauto using rmw_rf_uniq).
  ins; desf.
  assert (E = l); subst.
    generalize (Crf fst); rewrite RF, LAB; ins; desf.
    by destruct (lab wri); ins; desf.

  assert (sws0 = wri :: nil).
    apply NoDup_eq_one; ins; rewrite swsOK in *; eauto.
    red in IN; desc; congruence.
  subst; ins; rewrite hsum_one in ×.
  destruct FST, pU.
  eapply hplus_def_inv in pEQ'; desf.
  specialize (DEFv l); specialize (PLUSv l); rewrite hupds in *; ins; desf; ins; desc.
    by eapply heap_loc_ra_no_own with (edge' := hb_sb _ _) (h' := hf)
                                     (v:=v) (V:=V) in Z0; try exact PLUSv;
       eauto; ins; eauto with hb; instantiate;
       rewrite hupds in *; destruct Z0 as [Z0|Z0]; rewrite Z0 in *; ins; congruence.
    by specialize (DEFv v); rewrite hupds in *; destruct DEFv as [DEFv|[DEFv ?]];
       ins; rewrite DEFv in *; ins; congruence.
    by eapply heap_loc_ra_no_own with (edge' := hb_sb _ _) (h' := hf)
                                     (v:=v) (V:=V) in Z0; try exact PLUSv;
       eauto; ins; eauto with hb; instantiate;
       rewrite hupds in *; destruct Z0 as [Z0|Z0];
         [apply assn_norm_star_eq_emp, proj1 in Z0|
          apply assn_norm_star_eq_false in Z0; desf];
       destruct P as [P normP]; ins; rewrite !normP in *;
       rewrite Z0 in *; ins; congruence.
Qed.

Lemma rmw_helper1 :
  ∀ mt lab sb fst acts_ctx rf mo sc
    (CONS : weakConsistent (fst :: acts_ctx) lab sb rf mo sc mt)
    V (HC : hist_closed mt lab sb rf mo V)
    hmap (VALID : hmap_valids lab sb rf hmap V)
    prev (V_PREV : In prev V)
    (FST : unique (sb^~ fst) prev)
    (NIN : ¬ In fst V)
    hoo (Z : hmap (hb_sb prev fst) = Hdef hoo)
    E PP QQ
    (Z0 : hoo E = HVra PP (fun x : val ⇒ mk_assn_mod (QQ x)) true true)
    wri (INwri : In wri V)
    pre (pU : unique (sb^~ wri) pre)
    post
    hf (pEQ0 : hmap (hb_sb pre wri) = Hdef hf)
    typW vW (EQ : lab wri = Astore typW E vW)
    (WRI : is_writeLV (lab wri) E vW)
    sws hsink P
    (UPD : vshift (Hdef (initialize hf E))
                  (hsingl E (HVra (hupd Wemp vW P) Remp false true) +!+
                   hmap (hb_sb wri post) +!+ hsink))
    (TRAN : assn_sem (sval P) hsink)
    (swsND : NoDup sws)
    (swsOK : ∀ x : nat, In x sws ↔ ann_sw lab rf wri x),
   ∃ h1 hsink' : heap, hsink = h1 +!+ hsink' ∧ assn_sem (QQ vW) h1.
Proof.
  ins; red in CONS; desc.
  assert (XXX: ∃ PW QW isrmwW initW, hf E = HVra PW QW isrmwW initW ∧ PW vW = P).
  {
    rewrite vshift_hack in UPD.
    symmetry in UPD; apply hplus_def_inv in UPD; desf.
    generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds;
    clear - TRAN.
    ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
    by rewrite e in TRAN; ins.
  }
  desf.

  pose proof (read_loses_perm1 hmap lab sb rf E vW V swsND); desc.

  exploit (wellformed_one_w FIN IRR Ca HC VALID pre INwri EQ (proj1 pU) pEQ0 XXX
                          prev fst V_PREV (proj1 FST) NIN l); eauto using hupds.
    by ins; eapply EQl in IN; desc.
    by ins; eapply swsOK; eapply EQl in IN; desc.
    by ins; eapply EQl in IN; desc.
  simpl; intro S; desf.
  eapply sim_assn_sem in S1; try eapply Asim_assn_norm; eauto.
Qed.

Lemma rmw_helper2 :
  ∀ mt lab sb fst acts_ctx rf mo sc
    (CONS : weakConsistent (fst :: acts_ctx) lab sb rf mo sc mt)
    V (HC : hist_closed mt lab sb rf mo V)
    hmap (VALID : hmap_valids lab sb rf hmap V)
    prev (V_PREV : In prev V)
    (FST : unique (sb^~ fst) prev)
    (NIN : ¬ In fst V)
    hoo (Z : hmap (hb_sb prev fst) = Hdef hoo)
    E PP QQ
    (Z0 : hoo E = HVra PP (fun x : val ⇒ mk_assn_mod (QQ x)) true true)
    wri (INwri : In wri V)
    pre (pU : unique (sb^~ wri) pre)
    post
    swsIn
    (swsInOK: ∀ x, In x swsIn ↔ ann_sw lab rf x wri)
    (swsInND : NoDup swsIn)
    hf (pEQ0 : hmap (hb_sb pre wri) +!+
               hsum (map (mclearw hmap wri V) (map (hb_sw^~ wri) swsIn)) = Hdef hf)
    typW vV vW (EQ : lab wri = Armw typW E vV vW)
    (WRI : is_writeLV (lab wri) E vW)
    sws hsink PP'
    (UPD : vshift (Hdef hf)
          (hsingl E (HVra PP' Remp false false) +!+
           hmap (hb_sb wri post) +!+ hsink))
    (TRAN : assn_sem (sval (PP' vW)) hsink)
    (swsND : NoDup sws)
    (swsOK : ∀ x : nat, In x sws ↔ ann_sw lab rf wri x),
   ∃ h1 hsink' : heap, hsink = h1 +!+ hsink' ∧ assn_sem (QQ vW) h1.
Proof.
  ins; red in CONS; desc.
  assert (XXX: ∃ PW QW isrmwW initW, hf E = HVra PW QW isrmwW initW ∧ PW vW = PP' vW).
  {
    rewrite vshift_hack in UPD.
    symmetry in UPD; apply hplus_def_inv in UPD; desf.
    generalize (PLUSv E), (DEFv E); clear - TRAN; rewrite hupds.
    ins; desf; repeat (eexists; try edone); instantiate; simpl; desf;
    by rewrite e in ×.
  }
  desf.
  rewrite map_clearw_irr in pEQ0; ins; desf.
  pose proof (read_loses_perm1 hmap lab sb rf E vW V swsND); desc.
  exploit (wellformed_one FIN IRR Ca HC VALID pre INwri WRI (proj1 pU) swsInOK swsInND pEQ0 XXX
                          prev fst V_PREV (proj1 FST) NIN l); eauto using hupds.
    by ins; eapply EQl in IN; desc.
    by ins; eapply swsOK; eapply EQl in IN; desc.
    by ins; eapply EQl in IN; desc.
    eby rewrite XXX0.
  simpl; intro S; desf.
  eapply sim_assn_sem in S1; try eapply Asim_assn_norm; eauto.
Qed.