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.
Proof.
  ins.
  exploit heap_loc_rel_allocated_strong; try eassumption; try done.
  intro ALL; desc.
  assert (cpreIN: In cpre V) by ( desf; eapply hist_closedD; eauto).
  clear ALL3 ALL4.

  destruct (classic (w = c)) as [EQ | NEQ].
  {
    subst c.
    assert (cpreVALID := VALID _ cpreIN).
    red in cpreVALID; rewrite ALL0 in cpreVALID; desc.
    red in qU; desc.
    rewrite (qU0 _ ALL) in ×.
    rewrite ALL1 in ×.
    desf; rewrite hupds in *; desf.
    cut (cpre = wpre).
      by ins; desf; rewrite MAPw in *; desf; rewrite hupds in ×.
    assert (wVALID := VALID _ INw).
    red in LAB; desf; desf.
    × red in wVALID; rewrite Heq in wVALID; desc; clear DISJ.
      unfold unique in *; desf.
      by rewrite <- (pU1 _ SBw), <- (pU1 _ ALL).
    × red in wVALID; rewrite Heq in wVALID; desc. done.
  }

  {
    exploit (exists_path_with_location_throughout FIN ACYCLIC CONS_RF CONS_A HC VALID wpre cpre);
      try eassumption; eauto.

    by apply (HC w); vauto.

    by intro N; rewrite N in ×.

    by intro; congruence.

    by rewrite ALL2; vauto.

    ins; desf.

    {
      assert (PV: hbpath_valid lab sb rf hmap (hb_sb wpre w :: path ++ hb_sb cpre c :: nil)).
      {
        red in CONNECT; desf.
          by rewrite ALL0 in LAB.
        red; unnw; repeat split; ins.
        × red; ins.
          apply olast_inv in CONNECT2; desf.
          destruct prefix as [ | edge path]; ins.
            by repeat (destruct path1; ins; desf).
          rewrite <- app_assoc in DECOMP; ins.
          destruct path1 as [ | edgeA pathA]; ins; desf.
          des_list_tail path2 pathZ edgeZ.
          + rewrite <- (app_nil_l (hb_sb _ _ :: _)), <- (app_nil_l (edge2 :: _)),
                    !app_comm_cons, !app_assoc in H0.
            do 2 (apply app_inj_tail in H0; desf).
          + rewrite <- (app_nil_l (hb_sb _ _ :: _)), !app_comm_cons, !app_assoc in H0.
            apply app_inj_tail in H0; desf.
            rewrite !app_comm_cons, H0 in CONNECT.
            eby eapply (proj1 CONNECT).
        × rewrite In_app in IN; ins; desf; try (eby eapply VALID).
          by apply (proj1 (proj2 CONNECT)).
        × rewrite In_app in IN; ins; desf; ins.
          by apply VALID, (HC (hb_fst fst)); vauto.
          by apply (proj2 (proj2 CONNECT)).
          by apply VALID.
      }
      exploit nonatomic_loc_on_path; eauto.
      { instantiate (1 := l).
        ins; rewrite In_app in *; ins; desf.
        × rewrite MAPw in MAP; desf.
          by intro N; rewrite N in HW.
        × eby eapply ALL3.
        × rewrite ALL1 in MAP; desf; congruence.
      }
      { ∃ (hb_sb wpre w); unnw; split; ins; eauto.
        rewrite MAPw in MAP; desf; eauto.
      }
        by find_in_list.

      by rewrite ALL2; ins.
    }

    {
      assert (PV: hbpath_valid lab sb rf hmap (hb_sb cpre c :: path ++ hb_sb wpre w :: nil)).
      {
        red in CONNECT; desf.
        { red; unnw; repeat split; ins; desf; ins.
          × red; ins.
            destruct path1 as [ | edge path1]; ins; desf.
            apply (f_equal (@length _)) in H0.
            rewrite length_app in H0; ins; omega.
          × by apply VALID.
          × by apply VALID, (HC w); vauto.
        }
        red; unnw; repeat split; ins.
        × red; ins.
          apply olast_inv in CONNECT2; desf.
          destruct prefix as [ | edge path]; ins.
            by repeat (destruct path1; ins; desf).
          rewrite <- app_assoc in DECOMP; ins.
          destruct path1 as [ | edgeA pathA]; ins; desf.
          des_list_tail path2 pathZ edgeZ.
          + rewrite <- (app_nil_l (hb_sb _ _ :: _)), <- (app_nil_l (edge2 :: _)),
                    !app_comm_cons, !app_assoc in H0.
            do 2 (apply app_inj_tail in H0; desf).
          + rewrite <- (app_nil_l (hb_sb _ _ :: _)), !app_comm_cons, !app_assoc in H0.
            apply app_inj_tail in H0; desf.
            rewrite !app_comm_cons, H0 in CONNECT.
            eby eapply (proj1 CONNECT).
        × rewrite In_app in IN; ins; desf; try (eby eapply VALID).
          by apply (proj1 (proj2 CONNECT)).
        × rewrite In_app in IN; ins; desf; ins.
          by apply VALID.
          by apply (proj2 (proj2 CONNECT)).
          by apply VALID, (HC w); vauto.
      }
      exploit nonatomic_loc_on_path; eauto.
      { instantiate (1 := l).
        ins; rewrite In_app in *; ins; desf.
        × rewrite ALL1 in MAP; desf; congruence.
        × eby eapply ALL3.
        × rewrite MAPw in MAP; desf.
          by intro N; rewrite N in HW.
      }
      { ∃ (hb_sb wpre w); unnw; split; ins; try find_in_list.
        rewrite MAPw in MAP; desf; eauto.
      }
        by find_in_list.

      by rewrite ALL2; ins.
    }
  }

  Grab Existential Variables. edone.
Qed.

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) >>).
Proof.
  Opaque assn_sem.
  ins.
  assert (VALIDwri := (proj1 VALID _ INwri)).
  red in VALIDwri; rewrite WRI in VALIDwri.
  desc; destruct DISJ; desc; try clear TYP; ins; desf.
    by rewrite (proj2 pU _ SB), MAPw in *; unfold is_atomic in AT; desf.
  assert (EQ: hsum (map hmap (map (hb_rf wri) rfs0)) = hsum (map hmap (map (hb_rf wri) rfs))).
    by apply hsum_perm, map_perm, map_perm, NoDup_Permutation; ins; rewrite rfsOK, rfsOK0.

  rewrite EQ in *; clear EQ rfsND rfsOK0 rfs0.

  assert (∃ 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 >> ∧
            << NEMP: ∀ x, In x ann_rfs → hmap (hb_rf wri x) ≠ hemp >> ∧
            << INann_rfs: ∀ x, In x ann_rfs → In x V >> ∧
            << INV: ∀ x, In x ann_rfs → In x V >> ∧
            << READ: ∀ x, In x ann_rfs → ∃ typR, lab x = Aload typR l vW >>).
  {
    rewrite (hsum_perm (map_perm _ (map_perm _
            (Permutation_filter_split rfs (fun x ⇒ mydec (hmap (hb_rf wri x) ≠ hemp)))))).
    rewrite !map_app, hsum_app.
    assert (EMP: hsum (map hmap (@map actid _ (hb_rf wri)
                   (filter (fun x : actid ⇒ negb (mydec (hmap (hb_rf wri x) ≠ hemp))) rfs))) = hemp).
    {
      apply hsum_eq_emp; ins.
      repeat (rewrite In_map in *; desf).
      rewrite In_filter in *; desf.
      unfold mydec in *; desf.
      by apply NNPP.
    }
    rewrite EMP, hplus_emp_r; clear EMP.
    eexists; repeat apply conj; try edone.
      by apply NoDup_filter.
      by unnw; ins; rewrite In_filter in *; desf.
      by unnw; ins; rewrite In_filter in *; unfold mydec in *; desf.
    { unnw; ins; rewrite In_filter in *; desf; unfold mydec in *; desf.
      apply NNPP; intro NIN; destruct n.
      eapply (proj2 VALID); eauto; ins.
      unfold is_sb_out; ins; tauto.
    }
    { unnw; ins; rewrite In_filter in *; desf; unfold mydec in *; desf.
      apply NNPP; intro NIN; destruct n.
      eapply (proj2 VALID); eauto; ins.
      unfold is_sb_out; ins; tauto.
    }
    {
      unnw; ins; rewrite In_filter in *; desf; unfold mydec in *; desf.
      specialize (NORMW _ H).
      rewrite rfsOK in H.
      specialize (CONS_RF x); rewrite H in CONS_RF; desf.
      rewrite WRI in *; ins; desc; subst l0; subst v.
      red in CONS_RF; desf; desf.
      eby eexists.
      by rewrite NORMW in n; rewrite ?Heq.
    }
  }

  apply assn_sem_def, hplus_not_undef_l in TRAN.
  clear typW wpre hf pre post hf0 hr hF P
        WRI SB MAPw pU qU pEQ qEQ NA UPD rfsSIM INwri AT NORMW.

  desc; eexists; repeat (apply conj); try edone.
  rewrite rfEQ in ×.

  assert (SINK: ∀ x (IN: In x ann_rfs),
              hmap (hb_sink x) =
              hsingl l (HVra Wemp (hupd Remp vW (get_dropped_perm l vW (hmap (hb_sink x)))) false None None)).
  {
    ins.
    assert (VALIDx := proj1 VALID _ (INV _ IN)).
    specialize (NEMP _ IN).
    specialize (READ _ IN); desc.
    red in VALIDx; rewrite READ in VALIDx; desc.
    destruct DISJ; desc; try clear TYP; desf.
    rewrite !sEQ.
    repeat f_equal; ins.
    rewrite hupds; ins.
    by rewrite hupds.
  }

  destruct (classic (ann_rfs = nil)) as [ | READS_EXIST]; [by eauto | right].

  remember (map (get_dropped_perm l vW) (map hmap (map hb_sink ann_rfs))) as dropped_perm_list eqn:DP.
  ∃ (mk_assn_mod (foldr Astar (map sval dropped_perm_list) Aemp)); repeat apply conj.

  {
    subst dropped_perm_list.
    clear - SINK READS_EXIST.
    destruct ann_rfs as [ | a ann_rfs´]; ins.
    clear READS_EXIST.
    unnw; induction ann_rfs´ as [ | b ann_rfs´´]; ins.
    × rewrite SINK; eauto.
      rewrite hsum_one.
      unnw; repeat f_equal.
      rewrite SINK at 2; try by eauto.
      repeat (ins; rewrite !hupds).
      apply assn_mod_eqI; Asim_simpl.
    × rewrite !hsum_cons, hplusAC.
      assert (hmap (hb_sink a) +!+ hsum (map hmap (map hb_sink ann_rfs´´))
              = hsum (hmap (hb_sink a) :: map hmap (map hb_sink ann_rfs´´))) by (by rewrite hsum_cons).
      rewrite H; clear H.
      rewrite IHann_rfs´´.
        2: by ins; desf; intuition.
      rewrite SINK; try by eauto.
      rewrite hplus_hsingl; vauto.
      ins; repeat f_equal.
        by extensionality v; desf.
      extensionality v.
      unfold hupd; desf; desf; apply assn_mod_eqI; Asim_simpl.
      assert (ASAC: ∀ P Q R X, Asim (Astar P (Astar Q R)) X → Asim (Astar Q (Astar P R)) X).
        by clear; ins; generalize (Asim_starAC Q P R); ins; eapply Asim_trans; eauto.
      apply ASAC, Asim_star.
        by apply Asim_refl.
      apply Asim_star.
        2: by apply Asim_refl.
      ins; desf; desf.
        by apply Asim_refl.
  }

  {
    subst dropped_perm_list; unfold NW.
    destruct ann_rfs as [ | a ann_rfs´]; ins.
    clear READS_EXIST.
    assert (NORMeq: ∀ P, Anabla (assn_norm P) = assn_norm (Anabla P)) by ins.
    rewrite NORMeq, assn_sem_assn_norm, nabla_star_dist.
    Transparent assn_sem. hnf. Opaque assn_sem.
    eexists,; repeat apply conj; try eby rewrite ?hsum_cons.
    { generalize (proj1 VALID _ (INV _ (or_introl eq_refl))).
      specialize (READ _ (or_introl eq_refl)); desc.
      specialize (NEMP _ (or_introl eq_refl)).
      specialize (SUBSET _ (or_introl eq_refl)); rewrite rfsOK in SUBSET.
      clear - READ NEMP SUBSET.
      intro VALID.
      red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      assert (rfs = wri :: nil) by (apply NoDup_eq_one; ins; rewrite rfsOK in *; desf); subst rfs.
      ins; rewrite hsum_one in ×.
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
    }
    rewrite hsum_cons in TRAN; apply hplus_not_undef_r in TRAN.
    clear - INV NEMP SUBSET rfsOK READ VALID TRAN.
    induction ann_rfs´ as [ | b ann_rfs´´]; ins.
    × rewrite hsum_nil; split; vauto.
      eexists; repeat split; vauto.
    × rewrite nabla_star_dist.
      Transparent assn_sem. hnf. Opaque assn_sem.
        eexists,; repeat apply conj; try by rewrite ?hsum_cons.
        2: by apply IHann_rfs´´; solve [ ins; try apply SUBSET; try apply NEMP; try apply INV; desf; eauto |
                                         eby rewrite hsum_cons in TRAN; eapply hplus_not_undef_r ].
      clear IHann_rfs´´.
      generalize (proj1 VALID _ (INV _ (or_intror (or_introl eq_refl)))).
      specialize (SUBSET _ (or_intror (or_introl eq_refl))); rewrite rfsOK in SUBSET.
      specialize (READ _ (or_intror (or_introl eq_refl))); desc.
      specialize (NEMP _ (or_intror (or_introl eq_refl))).
      clear - READ NEMP SUBSET.
      intros VALID.
      red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      assert (rfs = wri :: nil) by (apply NoDup_eq_one; ins; rewrite rfsOK in *; desf); subst rfs.
      ins; rewrite hsum_one in ×.
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
  }

  {
    subst dropped_perm_list; ins.
    unfold NW; rewrite <- precise_assn_norm.
    destruct ann_rfs as [ | a ann_rfs´]; ins.
    clear READS_EXIST.
    apply precise_star.
    { generalize (proj1 VALID _ (INV _ (or_introl eq_refl))).
      specialize (NEMP _ (or_introl eq_refl)).
      specialize (READ _ (or_introl eq_refl)); desc.
      clear - READ NEMP.
      intro VALID; red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
    }
    {
      clear - INV NEMP READ VALID.
      induction ann_rfs´ as [ | b ann_rfs´´]; ins.
      apply precise_star.
        2: by apply IHann_rfs´´; ins; try apply SUBSET; try apply NEMP; try apply INV; desf; eauto.
      clear IHann_rfs´´.
      generalize (proj1 VALID _ (INV _ (or_intror (or_introl eq_refl)))).
      specialize (READ _ (or_intror (or_introl eq_refl))); desc.
      specialize (NEMP _ (or_intror (or_introl eq_refl))).
      clear VALID; intro VALID; red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
    }
  }

  {
    subst dropped_perm_list; ins.
    unfold NW; rewrite <- normalizable_assn_norm.
    destruct ann_rfs as [ | a ann_rfs´]; ins.
    clear READS_EXIST.
    apply normalizable_star.
    { generalize (proj1 VALID _ (INV _ (or_introl eq_refl))).
      specialize (NEMP _ (or_introl eq_refl)).
      specialize (READ _ (or_introl eq_refl)); desc.
      clear - READ NEMP.
      intro VALID; red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
    }
    {
      clear - INV NEMP READ VALID.
      induction ann_rfs´ as [ | b ann_rfs´´]; ins.
      apply normalizable_star.
        2: by apply IHann_rfs´´; ins; try apply SUBSET; try apply NEMP; try apply INV; desf; eauto.
      clear IHann_rfs´´.
      generalize (proj1 VALID _ (INV _ (or_intror (or_introl eq_refl)))).
      specialize (READ _ (or_intror (or_introl eq_refl))); desc.
      specialize (NEMP _ (or_intror (or_introl eq_refl))).
      clear VALID; intro VALID; red in VALID; rewrite READ in VALID; desc.
      destruct DISJ; desc; try clear TYP; [congruence | ].
      rewrite sEQ; ins.
      rewrite hupds; ins.
      by rewrite hupds.
    }
  }
  Transparent assn_sem.
Qed.