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

Set Implicit Arguments.

Lemma no_atomic_reads_from_na_one PS PSg :
  ∀ 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 gw
    (MAPw: hmap (hb_sb wpre w) = Hdef hw gw)
    (HW: is_lvalue (hw l))
    rpre r (ST: In rpre V) (TT: sb rpre r)
    (NIN: ¬ In r V)
    hT gT (MAPt: hmap (hb_sb rpre r) = Hdef hT gT)
    PT QT isrmwT permT initT (HT: hT l = @HVra PS PSg PT QT isrmwT permT initT),
  False.

Definition get_acq_perm PS PSg (hv: HeapVal PS PSg) :=
  match hv with
    | HVra _ QQ _ _ _ ⇒ QQ
    | _ ⇒ Wemp
  end.

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

Lemma annotated_rfs_and_sinks PS PSg :
  ∀ 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 g (MAPw: hmap (hb_sb wpre wri) = Hdef hf g) (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 PS PSg 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.
  Transparent assn_sem.