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 fslmodel.
Require Import ihc path drf.

Set Implicit Arguments.

Lemma no_atomic_reads_from_na_one :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf 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 permT initT (HT: hT l = HVra PT QT isrmwT permT initT),
  False.

Definition get_acq_perm hv :=
  match hv with
    | HVra _ QQ _ _ _ ⇒ QQ
    | _ ⇒ Wemp
  end.

Definition get_dropped_perm l v h :=
  match h with
    | Hdef h ⇒ get_acq_perm (h l) v
    | _ ⇒ mk_assn_mod Aemp
  end.

Lemma annotated_rfs_and_sinks :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    V (HC : hist_closed sb rf V) hmap (VALID : hmap_valids_strong lab sb rf hmap V)
    wri l vW typW (WRI: lab wri = Astore typW l vW) (INwri: In wri V)
    wpre (SB: sb wpre wri) hf (MAPw: hmap (hb_sb wpre wri) = Hdef hf) (AT: is_atomic (hf l))
    rfs (rfsOK: ∀ x, In x rfs ↔ rf x = Some wri) (NDrf: NoDup rfs)
    (NORMW: ∀ x (IN: In x rfs) (RMW: is_rmw (lab x)), hmap (hb_rf wri x) = hemp),
  ∃ ann_rfs,
    << rfEQ: hsum (map hmap (map (hb_rf wri) rfs)) = hsum (map hmap (map (hb_rf wri) ann_rfs)) >> ∧
    << NDann_rfs: NoDup ann_rfs >> ∧ << SUBSET: ∀ x, In x ann_rfs → In x rfs >> ∧
    << INann_rfs: ∀ x, In x ann_rfs → In x V >> ∧
    (<< NO_READS: ann_rfs = nil >> ∨
     ∃ QQread,
     << SINKS: hsum (map hmap (map hb_sink ann_rfs)) =
                    hsingl l (HVra Wemp (hupd Remp vW QQread) false None None) >> ∧
     << READS: assn_sem (Anabla (sval QQread)) (hsum (map hmap (map (hb_rf wri) ann_rfs))) >> ∧
     << PRECISE: precise (sval QQread) >> ∧
     << NORMALIZABLE: normalizable (sval QQread) >>).
  Opaque assn_sem.
    Transparent assn_sem. Opaque assn_sem.
      Transparent assn_sem. Opaque assn_sem.