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 fsltriple2.
Require Import drf ihc initread.
Require Import GpsSepAlg.

Set Implicit Arguments.

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_concurrent_readers_transfer_no_ownership PS PSg:
  ∀ fst acts lab sb rf mo sc
    (CONS : weakConsistent (fst :: acts) lab sb rf mo sc Model_hb_rf_acyclic)
    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 sb rf V)
    hmap (VALID : hmap_valids_strong lab sb rf hmap V)
    (NIN : ¬ In fst V)
    hoo goo (Z : hmap (hb_sb prev fst) = Hdef hoo goo)
    PP QQ labW labR (Z0 : hoo E = @HVra PS PSg PP (fun x : val ⇒ mk_assn_mod (QQ x)) true labW labR)
    wri (RF : rf fst = Some wri)
    rfs (INrfs: ∀ x, In x rfs → rf x = Some wri),
  hsum (map hmap (map (hb_rf wri) rfs)) = hemp.

Opaque Aexists.

Definition rmw_precondition PS PSg P l QQrel QQacq :=
  @Astar PS PSg (Arel l QQrel) (Astar (Armwacq l QQacq) (Astar (Arainit l) P)).

Definition satisfying PS PSg (phi: val → Prop) (AA: val → assn PS PSg) z :=
  if excluded_middle_informative (phi z) then AA z else Afalse.

Theorem rule_cas_ar PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AR: acquire_release_typ rmw_typ)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else RR x)),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi AA) else RR x).
      Opaque assn_sem.
      Transparent assn_sem.
        Opaque assn_sem.
        Transparent assn_sem.
      Opaque assn_sem.
      Transparent assn_sem.

Theorem rule_cas_rel PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi: val → Prop)
    (NORM: normalizable P)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (REL: release_typ rmw_typ)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi (fun y ⇒ Anabla (AA y))) else RR x).
      Opaque assn_sem.
      Transparent assn_sem.
        Opaque assn_sem.
        Transparent assn_sem.
      Opaque assn_sem.
      Transparent assn_sem.

Theorem rule_cas_acq PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (ACQ: acquire_typ rmw_typ)
    (FAIL: triple (rmw_precondition (Atriangle P) E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi AA) else RR x).
      Opaque assn_sem.
      Transparent assn_sem.
        Opaque assn_sem.
        Transparent assn_sem.
      Opaque assn_sem.
      Transparent assn_sem.

Theorem rule_cas_rlx PS PSg :
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq AA TT RR (phi : val → Prop)
    (IMPacq: implies (QQacq E') (Aexists (fun z ⇒ Astar (AA z) (TT z))))
    (IMPrel: ∀ z, implies (Astar P (TT z)) (satisfying phi (fun _ ⇒ (QQrel E'')) z))
    (AT: rmw_typ ≠ ATna)
    (FAIL: triple (rmw_precondition (Atriangle P) E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else (RR x))),
  triple (rmw_precondition (Atriangle P) E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Aexists (satisfying phi (fun y ⇒ Anabla (AA y))) else RR x).
      Opaque assn_sem.
      Transparent assn_sem.
        Opaque assn_sem.
        Transparent assn_sem.
      Opaque assn_sem.
      Transparent assn_sem.

Theorem rule_cas_shortcut PS PSg:
  ∀ rmw_typ load_typ E E' E'' (P: assn PS PSg) QQrel QQacq RR
    (UNSAT: implies (Astar (QQacq E') P) Afalse)
    (FAIL: triple (rmw_precondition P E QQrel QQacq)
                  (Eload load_typ E)
                  (fun x ⇒ if x == E' then Atrue else RR x)),
  triple (rmw_precondition P E QQrel QQacq)
         (Ecas rmw_typ load_typ E E' E'')
         (fun x ⇒ if x == E' then Afalse else RR x).