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.

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.
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.

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.

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.

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.