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.
Proof.
  ins.
  eapply atomicity_is_globally_exclusive; try exact (is_lvalue_implies_is_nonatomic _ HW);
                                            try exact MAPt; eauto; ins; eauto with hb.
  by rewrite HT.
Qed.

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) >>).
Proof.
  Opaque assn_sem.
  ins.
  assert (VALID' := VALID); red in VALID'; desc; red in VALIDS; desc.

  assert (VALIDwri := (VLD _ 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 DEF.

  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 := VLD _ (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 PS PSg) (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: assn PS PSg), 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: assn PS PSg), 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 (VLD _ (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 VLD TRAN.
    induction ann_rfs' as [ | b ann_rfs'']; ins.
    × rewrite hsum_nil; split; vauto.
      eexists; repeat split; vauto.
      by apply Hsim_refl.
    × 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 (VLD _ (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 (VLD _ (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 VLD.
      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 (VLD _ (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 VLD; 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 (VLD _ (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 VLD.
      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 (VLD _ (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 VLD; 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.