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

Set Implicit Arguments.

Soundness of atomic load rules

A helper lemma


Definition preciseish P :=
   hP (SEM: assn_sem P hP) hP´ (SEM´: assn_sem P hP´)
         hF (DEF: hplus hP hF Hundef) hF´ (EQ: hplus hP hF = hplus hP´ hF´),
  hP = hP´ Hsim hF hF´.

Lemma precise_nabla P: precise Ppreciseish (Anabla P).
Proof.
  red; ins; desf.
  assert (EQ´: h´0 = lupd hP HLnormal) by (by apply lupd_eq; [apply Hsim_sym | ]).
  assert (EQ´´: = lupd hP´ HLnormal) by (by apply lupd_eq; [apply Hsim_sym | ]).
  subst.
  exploit (H _ SEM0 _ SEM´0 (lupd hF HLnormal)).
    by rewrite <- lupd_hplus_dist; unfold lupd; desf.
    by instantiate (1 := lupd hF´ HLnormal); rewrite <- !lupd_hplus_dist, EQ.
  intro LUPD; desf.
  split.
  × apply lupd_eq_lupd in LUPD.
    eby eapply exact_label_sim.
    eby eapply hplus_not_undef_l.
  × eapply lupd_eq_lupd; try edone.
    eby eapply hplus_not_undef_r.
Qed.

Acquire load


Theorem rule_load_acq typ E QQ (PREC: v, precise (QQ v)) (NORM: v, normalizable (QQ v))
   (TYP : acquire_typ typ) :
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload typ E)
         (fun vAstar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (QQ v))).
Proof.
  eapply triple_helper_start; ins; desc; clarify; ins.

  rewrite hplus_init1 in *; ins.

  assert (Z : hoo PP QQ0 isrmw labW labR, hmap (hb_sb prev fst) = Hdef hoo
          hoo E = HVra PP (fun xmk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw labW (ohlplus HLnormal labR)
          (isrmw x, assn_norm (QQ x) = Aemp assn_norm (QQ x) = Afalse)).
  {
    rewrite pEQ in *; clear -pDEF.
    destruct hFR; ins; rewrite hplus_unfold in *; desf.
    specialize (h E); rewrite hupds in *; ins; desf.
    {
      eexists _, Wemp, (fun _Aemp), false, None, None,; [done | ].
      ins; rewrite Heq, hupds, hvplusC; ins; split; ins.
      f_equal; extensionality v; apply AsimD, Asim_sym, Asim_star_emp.
    }
    { eexists _, RR, (fun vsval (QQ0 v)), isrmwflag, perm, init,; [done | ].
      ins; rewrite Heq, hupds in *; ins; split.
      × f_equal; [extensionality v | ]; desf.
        + extensionality v; generalize (h v); clear; ins.
          unfold hv_acq_def, hv_rval in H; desf.
          - apply assn_mod_eqI; Asim_simpl.
            eapply Asim_trans.
              by apply Asim_star_emp_l.
            apply Asim_star; [ | by apply Asim_refl].
            by rewrite <- H; apply Asim_sym, Asim_assn_norm.
          - apply assn_mod_eqI; Asim_simpl.
            rewrite H0; eapply Asim_trans.
              by apply Asim_sym, Asim_star_false.
            apply Asim_star; [ | by apply Asim_refl].
            by rewrite <- H; apply Asim_sym, Asim_assn_norm.
        + by extensionality v; apply AsimD, Asim_star; [apply Asim_sym, Asim_assn_norm | apply Asim_refl].
      × ins; desf; specialize (h x); unfold hv_acq_def, hv_rval in h; desf; eauto.
    }
  }

  desc.

  assert ( wri, << RF : rf fst = Some wri >> << WRI: is_writeLV (lab wri) E v >>).
  {
    red in CONS; desc; generalize (Crf fst); intro CrfFST; desf.
      repeat eexists; desf; simpls.
      by rewrite SEM1 in *; ins; desf.

    exfalso.
    exploit (initialization_always_before (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                          Crf HC (proj1 VALID)); eauto.
      by simpl; apply FST.
      by simpl; exploit (HC0 fst); vauto; apply hc_edge_sb, FST.
      by instantiate (2 := E); instantiate (1 := HLnormal);
         rewrite Z0; clear; simpl; desf; red; eauto; inv Heq; eauto.
    intro; desf.
    eapply (CrfFST a); eauto.
      2: eby rewrite SEM1.
    red in FST; desc;clear - FST HB.
    apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }

  desf.

  assert (INwri: In wri V).
  {
    exploit (HC0 fst); vauto.
    simpl; intro; desf.
    exfalso; red in CONS; desc; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC); vauto.
  }

  destruct (eqP (assn_norm (QQ v)) Aemp) as [EMP|NEMP].

  {
    assert (T: (fun x : valmk_assn_mod (hupd QQ v Aemp x)) =
               (fun x : valmk_assn_mod (QQ x))).
    {
      clear - EMP; exten; intro y; unfold hupd; desf; desf.
      by apply assn_mod_eqI1; ins.
    }

    eapply safe_final3s with
       (h := hsingl E (HVra Wemp (fun xmk_assn_mod (hupd QQ v Aemp x)) false None HLnormal) +!+ hFR)
       (hs := hsingl E (HVra Wemp Remp false None None)); eauto.
    × hemp; rewrite hplus_emp_r.
      repeat eexists; repeat split; eauto; try done.
      + rewrite pEQ in pDEF; clear - pDEF EMP.
        rewrite hdef_alt in pDEF; desf.
        apply hplus_def_inv in pDEF; desf.
        intro U; rewrite hplus_unfold in U; desf.
        destruct n; ins.
        specialize (DEFv v0).
        unfold hupd; desf; ins; desf; rewrite ?hupds in DEFv; ins; desf.
        split; ins; desf; desf.
        rewrite assn_norm_emp.
        by specialize (DEFv v); rewrite EMP in DEFv.
      + by instantiate (1 := hemp); rewrite hplus_emp_r, hplus_init1.
      + by rewrite hplus_emp_r.
      + by apply assn_sem_assn_norm; rewrite EMP.
    × red; desf.
      eexists,,hoo; repeat split; try (by apply FST); try by (apply LST).
        by unfold mupd; desf; desf.
      right; split; [by destruct TYP; desf | ].
      destruct hFR as [|hFR]; try done.
      eexists (wri :: nil), hemp,
              (hsingl E (HVra Wemp (fun x : valmk_assn_mod (QQ x)) false None HLnormal) +!+ Hdef hFR),
              (mk_assn_mod Aemp).
      assert (RFemp: hmap (hb_rf wri fst) = hemp).
      {
        eapply (proj2 VALID); eauto.
        right; split; ins.
        clear; intro SB; red in SB; desf.
      }
      unnw; repeat (split; try by (clear Z0; ins; desf; vauto)); intros.
      + clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + hemp; repeat split; try by vauto.
        clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + unfold mupd; desf; desf.
        unnw; repeat f_equal.
        clear - EMP; extensionality x.
        unfold hupd; desf; desf.
      + rewrite Z in pEQ; clear - pEQ Z0.
        assert (empEQ: hupd Remp v (mk_assn_mod Aemp) = Remp) by (extensionality x; unfold hupd; desf; desf).
        rewrite empEQ, hplusAC, <- hplusA, hplus_init1, hplus_unfold; desf.
      + unfold mupd; desf; desf.
        rewrite Z in pEQ; clear - pEQ EMP.
        rewrite hplus_unfold; desf.
        destruct n; ins.
        symmetry in pEQ; apply hplus_def_inv in pEQ; desf.
        specialize (DEFv v0); clear PLUSv; unfold hupd in *; ins; desf; desf.
        ins; desf.
        split; ins; desf; desf.
        specialize (DEFv v); rewrite assn_norm_emp; congruence.
      + unfold mupd; desf; desf. rewrite hplus_emp_l.
        rewrite hplusAC, <-hplusA, hplus_init1.
        unnw; repeat f_equal.
        clear - EMP; extensionality x.
        unfold hupd; desf; desf.
        apply AsimD.
        by rewrite <- EMP; apply Asim_sym, Asim_assn_norm.
  }

  generalize ((proj1 VALID) _ INwri); intro M.
  red in M; destruct (lab wri) eqn: EQ; ins; desc; subst l v.
  assert (WRI: is_writeLV (lab wri) E v0) by (rewrite EQ; done).
  desc; destruct DISJ; desc; subst; try done.
  {
    red in CONS; desc; ins.
    edestruct (no_atomic_reads_from_na_one FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                           Ca Crf HC (proj1 VALID) pre _ INwri _ _
                                           WRI (proj1 pU) pEQ0 IV prev fst V_PREV (proj1 FST) NIN);
      eauto using hupds.
  }


  assert (XXX: PW QW isrmwW permW initW, hf E = HVra PW QW isrmwW permW initW PW v0 = P).
  {
    rewrite qEQ, hplusA in UPD.
    symmetry in UPD; apply hplus_def_inv in UPD; desc.
    inv UPD.
    generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds.
    clear - TRAN0.
    ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
    by rewrite e in TRAN0; ins.
  }




  {

    assert (Y: h1 hsink, hmap (hb_sink wri) = h1 +!+ hsink assn_sem (Anabla (QQ v0)) h1).
    {
      destruct isrmw.
      × exfalso.         destruct (Z1 eq_refl v0) as [MM|MM]; try done.
        desc; subst; red in CONS; desc.
        assert (WWW := wellformed_one_w); red in WWW.
        destruct FST, pU, qU; eapply WWW in TRAN0; clear WWW;
        try exact HC; try exact Z0; try exact XXX; try exact Z; try exact (proj1 VALID); try eassumption; eauto; [].
        ins; desc.
        apply (sim_assn_sem (Asim_assn_norm _)) in TRAN4; ins; desc.
        by apply (sim_assn_sem (Asim_assn_norm _)) in TRAN8; rewrite MM in ×.
      × red in CONS; desc; ins.
        exploit annotated_rfs_and_sinks; try exact HC; try eassumption; eauto.
          by apply pU.
          by rewrite XXX.
          {
             
            ins.
            destruct (classic (In x V)).
            × assert (RMW´ := proj1 VALID x H).
              clear - RMW RMW´.
              red in RMW´; desf.
            × eapply (proj2 VALID); try by exact H.
              right; split; unfold is_sb_out; ins.
              by intro; desc.
         }
        ins; desc.
        destruct x0; desc.
        {
          unnw; subst ann_rfs; ins.
          rewrite rfEQ, hsum_nil, hplus_emp_l in ×.
          subst P.
          exploit (wellformed_one_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
                                    pre wri INwri EQ (proj1 pU) pEQ0 XXX prev fst V_PREV (proj1 FST) NIN); eauto.
          intro WF; ins; desc.
          rewrite assn_sem_assn_norm in *; ins; desc.
          subst h1; subst .
           (lupd h0 HLnabla), (lupd (h3 +!+ h2) HLnabla).
          repeat (apply conj).
            by rewrite <- lupd_hplus_dist, <- hplusA; apply lupd_eq.
            by apply lupd_label; intro U; rewrite U, !hplus_undef_l in ×.
          eexists; repeat (apply conj); try edone.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U, !hplus_undef_l in ×.
          by repeat (apply exact_label_hplus_dist in TRAN2; desc).
        }
        {
          remember (hb_sb prev fst :: map hb_sink ann_rfs) as T.
          assert (NDt : NoDup T).
          {
            subst T; apply nodup_cons.
            split.
              by rewrite In_map; intro; desc.
            apply nodup_map; ins.
            clear Z0 TYP0; intro; desf.
          }
          assert (INt: edge : hbcase, In edge TIn (hb_fst edge) V).
          {
            clear TYP0 Z0; subst T; ins; desf.
            rewrite In_map in *; desf; ins; intuition.
          }
          assert (VALIDt: edge : hbcase, In edge Tedge_valid lab sb rf edge).
          {
            clear TYP0 Z0; subst T; ins; desf.
              by ins; apply FST.
            rewrite In_map in *; desf; ins.
            apply SUBSET, rfsOK in H0.
            red; desf; specialize (Crf x); rewrite H0, Heq in Crf; ins; desf.
          }
          assert (INDEP: independent sb rf T).
          {
            clear Z0 TYP0; subst T; red; ins; desf; ins; rewrite ?In_map in *; desf; ins.
            by destruct NIN; apply INann_rfs.
            eby destruct NIN; eapply hist_closedD.
            by destruct NIN; eapply hist_closedD; try edone; apply INann_rfs.
          }
          assert (HT: hT, hsum (map hmap T) = Hdef hT
                       PT QT isrmwT permT initT, hT E = HVra PT QT isrmwT permT initT
                             QT v0 = mk_assn_mod (Astar (Astar (QQ v0) (QQ0 v0)) (sval QQread))).
          {
            clear TYP0; revert Z0; subst T.
            exploit independent_heap_compat; try exact HC; try eassumption; eauto.
              by exact (proj1 VALID).
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; rewrite In_map in *; desf; intuition.
              by ins; desf; [apply FST | rewrite In_map in *; desf].
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; exploit (VALIDt (hb_sink a)); ins; eauto.
            intros SUM ?; desc.
            eexists,; try edone.
            ins; rewrite hsum_cons, Z, SINKS in SUM.
            clear - SUM Z0.
            apply hplus_def_inv in SUM; desc.
            inv SUM.
            generalize (PLUSv E); rewrite Z0, hupds; clear; ins.
            repeat eexists; eauto.
            clear; ins; apply AsimD.
            apply Asim_star.
            by apply Asim_sym, Asim_assn_norm.
            by rewrite hupds; apply Asim_refl.
          }
          subst P; desc.
          exploit (wellformed_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
                   pre wri INwri EQ (proj1 pU) pEQ0 XXX NDt INt VALIDt INDEP HT HT0); try exact TRAN0.
          rewrite HT1; intro WF; simpls; desc.
          rewrite assn_sem_assn_norm in ×.
          subst .
          rewrite rfEQ in ×.
          clear - PREC NORM PRECISE NORMALIZABLE rfsSIM TRAN TRAN0 TRAN1 TRAN2 TRAN READS READS0 READS1 READS2
                  WF WF1 WF2.
          ins; desf.
          assert (EQ: hsum (map hmap (map (hb_rf wri) ann_rfs)) +!+ hmap (hb_sink wri)
                      = lupd (h4 +!+ h5 +!+ h3 +!+ h2) HLnabla) by (by rewrite !hplusA in TRAN1; apply lupd_eq).
          assert (EQ´: hsum (map hmap (map (hb_rf wri) ann_rfs)) = lupd h´0 HLnabla) by (by apply lupd_eq).
          rewrite EQ´, !(hplusAC h3), !lupd_hplus_dist in EQ.
          specialize (NORMALIZABLE _ WF4); desc.
          subst h3.
          rewrite lupd_hplus_dist, hplusA in EQ.
          apply precise_nabla in PRECISE.
          assert (SAT0: assn_sem (Anabla (sval QQread)) (lupd h´0 HLnabla)).
          {
            split.
              eby eapply lupd_label, assn_sem_def.
             h´0; repeat (apply conj); try done.
            eby eapply Hsim_sym, lupd_sim, assn_sem_def.
          }
          assert (SATn: assn_sem (Anabla (sval QQread)) (lupd hN HLnabla)).
          {
            split.
              eby eapply lupd_label, assn_sem_def.
             hN; repeat (apply conj); try done.
            eby eapply Hsim_sym, lupd_sim, assn_sem_def.
          }
          assert (DEF: lupd h´0 HLnabla +!+ hmap (hb_sink wri) Hundef).
          {
            rewrite EQ´ in rfsSIM.
            red in rfsSIM; desc; congruence.
          }
          exploit (PRECISE _ SAT0 _ SATn _ DEF).
            by exact EQ.
          intro DECOMP; desc.
          apply exact_label_sim with (lbl := HLnabla) in DECOMP0.
            2: by apply exact_label_hplus_dist in TRAN; desc.
            2: by rewrite <- !lupd_hplus_dist in *; apply lupd_label;
               red in DECOMP0; desc; intro U; rewrite U in ×.
          specialize (NORM _ _ WF6); desc.
          subst h4.
          rewrite lupd_hplus_dist, hplusA, hplusAC in DECOMP0.
          eexists,,; [by exact DECOMP0 | ].
          split; [by apply lupd_label; intro U; rewrite U, !hplus_undef_r in × | ].
          eexists; repeat apply conj; try exact NORM; try edone.
          eby eapply Hsim_sym, lupd_sim, assn_sem_def.
      }
    }

    clear Z Z0 Z1; desc.

    assert (WOK: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) wri).
    {
      red; rewrite EQ.
      eexists,,; repeat (split; try edone); right; split; try done.
       rfs, hr, hF, P.
      assert(SAME: hsum (map (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) (map (hb_rf wri) rfs))
                   +!+ mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink (hb_sink wri)
                   = hsum (map hmap (map (hb_rf wri) rfs)) +!+ hmap (hb_sink wri)).
      {
        clear TYP0.
        rewrite <- rfsOK in RF.
        apply In_implies_perm in RF as [rfs´ PERM].
        rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
        rewrite !hsum_cons.
        rewrite !map_upd_irr; ins.
          2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
        unfold mupd; desf; desf.
        desf.
        symmetry; rewrite (hplusC h1), Y, !hplusA, <- hplus_emp_l.
        f_equal.
        eapply (proj2 VALID); eauto.
        right; split; ins.
        unfold is_sb_out; intro; desf.
      }

      rewrite <- SAME in *; unnw; repeat (split; try done).
      eby eexists,.
    }

    clear TYP0.

    assert (FOO: hmap_valids lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) V).
    {
      red.
      intros; destruct (eqP e wri); desf.
      eapply hmap_irr_change_valid.
        by apply VALID.
      ins; unfold mupd; desf; desf; ins; desf.
    }

    ins; desc.

    assert (DEF: hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))
                 +!+ h´0 +!+ hFR Hundef).
    {
      red in CONS; desc; ins.
      exploit (independent_heap_compat FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Crf Ca HC FOO
                                           (T := hb_rf wri fst :: hb_sb prev fst :: nil));
        try solve [ by rewrite NoDup_two | ins; desf; apply FST].
        by eapply independent_two; ins; eauto; try (by apply FST); intro; desf; eauto with hb.
      intro DEF; desc.
      ins; rewrite hsum_two in DEF.
      unfold mupd in DEF; desf; desf.
      pattern h in DEF; eapply ex_intro in DEF; rewrite <- hdef_alt, pEQ in DEF.
      apply (hplus_sim_def _ Y2) in DEF.
      assert (D: hsingl E (HVra Wemp (fun x : valmk_assn_mod (QQ x)) false None (Some HLCnormal))
                 =
                 hsingl E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None)
                 +!+
                 hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))).
      {
        clear; rewrite hplus_hsingl; simpl; vauto.
        repeat f_equal; desf.
        extensionality v.
        apply AsimD.
        unfold hupd; desf; desf; ins.
        by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_r].
        by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_l].
      }
      rewrite hplusAC, D, hplusA in DEF.
      by intro U; rewrite U, hplus_undef_r in DEF.
    }

    eapply safe_final4a with
      (h := hsingl E (HVra Wemp (fun x : valmk_assn_mod ((hupd QQ v0 Aemp) x)) false None (Some HLCnormal))
             +!+ h´0 +!+ hFR)
      (hs := hsingl E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None));
    eauto.

    { hemp; rewrite hplus_emp_r.
      eexists; repeat split; try done.
      eby rewrite <- hplusA.
      eexists _, (hsingl E (HVra Wemp Remp false None (Some HLCnormal)) +!+ h´0); repeat (split; try edone).
        by intro U; rewrite <- hplusA, U, hplus_undef_l in DEF.
        by rewrite <- hplusA, hplus_init1.
      eexists _, h´0; repeat (split; try edone).
      rewrite <- ohlplus_none_l in DEF at 1.
      rewrite <- (ohlplus_none_l (Some HLCnormal)) in DEF.
      by intro U; rewrite <- hplus_init1, hplusA, <- (hplusA _ h´0), U, hplus_undef_l, hplus_undef_r in DEF.
    }

    { red; rewrite SEM1.
      rewrite hdef_alt in pDEF; desc.
      eexists _, _, hf0; repeat (split; try edone).
        by unfold NW, mupd; desf; desf.
      right.
      split; [destruct TYP; congruence | ].
      eexists (wri :: nil), (lupd h1 HLnormal), _, (mk_assn_mod (QQ v0)).
      repeat (apply conj; try edone); ins; rewrite ?hsum_one; unfold mupd; desf; desf.
      × split; ins; desf; eauto.
      × h´0; repeat split; try done.
        by simpl; rewrite assn_sem_assn_norm.
      × apply lupd_sim.
        red in Y2; desf.
      × instantiate
          (1 := hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None None) +!+ hFR).
        rewrite <- hplusA, hplus_hsingl, <- pDEF, pEQ; vauto.
        ins; unnw; repeat f_equal; extensionality v; desf.
        clear; apply AsimD.
        unfold hupd; desf; desf; ins.
        by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
           [apply Asim_star_emp_r | apply Asim_assn_norm].
        by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
           [apply Asim_star_emp_l | apply Asim_assn_norm].
      × rewrite (hplusAC h´0), (hplusAC (lupd _ _)).
        rewrite <- (hplusA (hsingl _ _) (hsingl _ _)), (hplusC (hsingl _ _) (hsingl _ _)), hplus_init1; simpl.
        unnw; f_equal.
        apply lupd_eq; try done.
        by apply Hsim_sym.
      × right; repeat split; try (destruct TYP; congruence).
        apply lupd_label.
        red in Y2; desf.
      × by unnw; rewrite <- precise_assn_norm.
      × by unnw; rewrite <- normalizable_assn_norm.
    }
  }


Grab Existential Variables. edone.
Qed.

Relaxed load


Theorem rule_load_rlx E QQ (PREC: v, precise (QQ v)) (NORM: v, normalizable (QQ v)) :
  triple (Astar (Aacq E QQ) (Arainit E))
         (Eload ATrlx E)
         (fun vAstar (Aacq E (hupd QQ v Aemp)) (Astar (Arainit E) (Anabla (QQ v)))).
Proof.
  eapply triple_helper_start; ins; desc; clarify; ins.

  rewrite hplus_init1 in *; ins.

  assert (Z : hoo PP QQ0 isrmw labW labR, hmap (hb_sb prev fst) = Hdef hoo
          hoo E = HVra PP (fun xmk_assn_mod (Astar (QQ x) (QQ0 x))) isrmw labW (ohlplus HLnormal labR)
          (isrmw x, assn_norm (QQ x) = Aemp assn_norm (QQ x) = Afalse)).
  {
    rewrite pEQ in *; clear -pDEF.
    destruct hFR; ins; rewrite hplus_unfold in *; desf.
    specialize (h E); rewrite hupds in *; ins; desf.
    {
      eexists _, Wemp, (fun _Aemp), false, None, None,; [done | ].
      ins; rewrite Heq, hupds, hvplusC; ins; split; ins.
      f_equal; extensionality v; apply AsimD, Asim_sym, Asim_star_emp.
    }
    { eexists _, RR, (fun vsval (QQ0 v)), isrmwflag, perm, init,; [done | ].
      ins; rewrite Heq, hupds in *; ins; split.
      × f_equal; [extensionality v | ]; desf.
        + extensionality v; generalize (h v); clear; ins.
          unfold hv_acq_def, hv_rval in H; desf.
          - apply assn_mod_eqI; Asim_simpl.
            eapply Asim_trans.
              by apply Asim_star_emp_l.
            apply Asim_star; [ | by apply Asim_refl].
            by rewrite <- H; apply Asim_sym, Asim_assn_norm.
          - apply assn_mod_eqI; Asim_simpl.
            rewrite H0; eapply Asim_trans.
              by apply Asim_sym, Asim_star_false.
            apply Asim_star; [ | by apply Asim_refl].
            by rewrite <- H; apply Asim_sym, Asim_assn_norm.
        + by extensionality v; apply AsimD, Asim_star; [apply Asim_sym, Asim_assn_norm | apply Asim_refl].
      × ins; desf; specialize (h x); unfold hv_acq_def, hv_rval in h; desf; eauto.
    }
  }

  desc.

  assert ( wri, << RF : rf fst = Some wri >> << WRI: is_writeLV (lab wri) E v >>).
  {
    red in CONS; desc; generalize (Crf fst); intro CrfFST; desf.
      repeat eexists; desf; simpls.
      by rewrite SEM1 in *; ins; desf.

    exfalso.
    exploit (initialization_always_before (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                          Crf HC (proj1 VALID)); eauto.
      by simpl; apply FST.
      by simpl; exploit (HC0 fst); vauto; apply hc_edge_sb, FST.
      by instantiate (2 := E); instantiate (1 := HLnormal);
         rewrite Z0; clear; simpl; desf; red; eauto; inv Heq; eauto.
    intro; desf.
    eapply (CrfFST a); eauto.
      2: eby rewrite SEM1.
    red in FST; desc;clear - FST HB.
    apply clos_refl_trans_hbE in HB; desf; eauto with hb.
  }

  desf.

  assert (INwri: In wri V).
  {
    exploit (HC0 fst); vauto.
    simpl; intro; desf.
    exfalso; red in CONS; desc; eapply (AcyclicStrong_implies_IrreflexiveHBuRF ACYC); vauto.
  }

  destruct (eqP (assn_norm (QQ v)) Aemp) as [EMP|NEMP].

  {
    assert (T: (fun x : valmk_assn_mod (hupd QQ v Aemp x)) =
               (fun x : valmk_assn_mod (QQ x))).
    {
      clear - EMP; exten; intro y; unfold hupd; desf; desf.
      by apply assn_mod_eqI1; ins.
    }

    eapply safe_final3s with
       (h := hsingl E (HVra Wemp (fun xmk_assn_mod (hupd QQ v Aemp x)) false None HLnormal) +!+ hFR)
       (hs := hsingl E (HVra Wemp Remp false None None)); eauto.
    × hemp; rewrite hplus_emp_r.
      repeat eexists; repeat split; eauto; try done.
      + rewrite pEQ in pDEF; clear - pDEF EMP.
        rewrite hdef_alt in pDEF; desf.
        apply hplus_def_inv in pDEF; desf.
        intro U; rewrite hplus_unfold in U; desf.
        destruct n; ins.
        specialize (DEFv v0).
        unfold hupd; desf; ins; desf; rewrite ?hupds in DEFv; ins; desf.
        split; ins; desf; desf.
        rewrite assn_norm_emp.
        by specialize (DEFv v); rewrite EMP in DEFv.
      + by instantiate (1 := (fun _ : valHVnone)); rewrite hplus_emp_r, hplus_init1.
      + by rewrite hplus_emp_r.
      + vauto.
      + by rewrite <- assn_sem_assn_norm, EMP.
      + vauto.
      + vauto.
    × red; desf.
      eexists,,hoo; repeat split; try (by apply FST); try by (apply LST).
        by unfold mupd; desf; desf.
      right; split; [done | ].
      destruct hFR as [|hFR]; try done.
      eexists (wri :: nil), hemp,
              (hsingl E (HVra Wemp (fun x : valmk_assn_mod (QQ x)) false None HLnormal) +!+ Hdef hFR),
              (mk_assn_mod Aemp).
      assert (RFemp: hmap (hb_rf wri fst) = hemp).
      {
        eapply (proj2 VALID); eauto.
        right; split; ins.
        clear; intro SB; red in SB; desf.
      }
      unnw; repeat (split; try by (clear Z0; ins; desf; vauto)); intros.
      + clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + hemp; repeat split; try by vauto.
        clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + clear Z0; ins; rewrite hsum_one; unfold mupd; desf; desf.
        rewrite RFemp; vauto.
      + unfold mupd; desf; desf.
        unnw; repeat f_equal.
        clear - EMP; extensionality x.
        unfold hupd; desf; desf.
      + rewrite Z in pEQ; clear - pEQ Z0.
        assert (empEQ: hupd Remp v (mk_assn_mod Aemp) = Remp) by (extensionality x; unfold hupd; desf; desf).
        rewrite empEQ, hplusAC, <- hplusA, hplus_init1, hplus_unfold; desf.
      + unfold mupd; desf; desf.
        rewrite Z in pEQ; clear - pEQ EMP.
        rewrite hplus_unfold; desf.
        destruct n; ins.
        symmetry in pEQ; apply hplus_def_inv in pEQ; desf.
        specialize (DEFv v0); clear PLUSv; unfold hupd in *; ins; desf; desf.
        ins; desf.
        split; ins; desf; desf.
        specialize (DEFv v); rewrite assn_norm_emp; congruence.
      + unfold mupd; desf; desf. rewrite hplus_emp_l.
        rewrite hplusAC, <-hplusA, hplus_init1.
        unnw; repeat f_equal.
        clear - EMP; extensionality x.
        unfold hupd; desf; desf.
        apply AsimD.
        by rewrite <- EMP; apply Asim_sym, Asim_assn_norm.
  }

  generalize ((proj1 VALID) _ INwri); intro M.
  red in M; destruct (lab wri) eqn: EQ; ins; desc; subst l v.
  assert (WRI: is_writeLV (lab wri) E v0) by (rewrite EQ; done).
  desc; destruct DISJ; desc; subst; try done.
  {
    red in CONS; desc; ins.
    edestruct (no_atomic_reads_from_na_one FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC)
                                           Ca Crf HC (proj1 VALID) pre _ INwri _ _
                                           WRI (proj1 pU) pEQ0 IV prev fst V_PREV (proj1 FST) NIN);
      eauto using hupds.
  }


  assert (XXX: PW QW isrmwW permW initW, hf E = HVra PW QW isrmwW permW initW PW v0 = P).
  {
    rewrite qEQ, hplusA in UPD.
    symmetry in UPD; apply hplus_def_inv in UPD; desc.
    inv UPD.
    generalize (PLUSv E), (DEFv E); unfold initialize; rewrite !hupds.
    clear - TRAN0.
    ins; desf; repeat eexists; instantiate; ins; rewrite ?hupds; desf;
    by rewrite e in TRAN0; ins.
  }




  {

    assert (Y: h1 hsink, hmap (hb_sink wri) = h1 +!+ hsink assn_sem (Anabla (QQ v0)) h1).
    {
      destruct isrmw.
      × exfalso.         destruct (Z1 eq_refl v0) as [MM|MM]; try done.
        desc; subst; red in CONS; desc.
        assert (WWW := wellformed_one_w); red in WWW.
        destruct FST, pU, qU; eapply WWW in TRAN0; clear WWW;
        try exact HC; try exact Z0; try exact XXX; try exact Z; try exact (proj1 VALID); try eassumption; eauto; [].
        ins; desc.
        apply (sim_assn_sem (Asim_assn_norm _)) in TRAN4; ins; desc.
        by apply (sim_assn_sem (Asim_assn_norm _)) in TRAN8; rewrite MM in ×.
      × red in CONS; desc; ins.
        exploit annotated_rfs_and_sinks; try exact HC; try eassumption; eauto.
          by apply pU.
          by rewrite XXX.
          {
             
            ins.
            destruct (classic (In x V)).
            × assert (RMW´ := proj1 VALID x H).
              clear - RMW RMW´.
              red in RMW´; desf.
            × eapply (proj2 VALID); try by exact H.
              right; split; unfold is_sb_out; ins.
              by intro; desc.
          }
        ins; desc.
        destruct x0; desc.
        {
          unnw; subst ann_rfs; ins.
          rewrite rfEQ, hsum_nil, hplus_emp_l in ×.
          subst P.
          exploit (wellformed_one_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
                                    pre wri INwri EQ (proj1 pU) pEQ0 XXX prev fst V_PREV (proj1 FST) NIN); eauto.
          intro WF; ins; desc.
          rewrite assn_sem_assn_norm in *; ins; desc.
          subst h1; subst .
           (lupd h0 HLnabla), (lupd (h3 +!+ h2) HLnabla).
          repeat (apply conj).
            by rewrite <- lupd_hplus_dist, <- hplusA; apply lupd_eq.
            by apply lupd_label; intro U; rewrite U, !hplus_undef_l in ×.
          eexists; repeat (apply conj); try edone.
          by apply Hsim_sym, lupd_sim; intro U; rewrite U, !hplus_undef_l in ×.
          by repeat (apply exact_label_hplus_dist in TRAN2; desc).
        }
        {
          remember (hb_sb prev fst :: map hb_sink ann_rfs) as T.
          assert (NDt : NoDup T).
          {
            subst T; apply nodup_cons.
            split.
              by rewrite In_map; intro; desc.
            apply nodup_map; ins.
            clear Z0 TYP; intro; desf.
          }
          assert (INt: edge : hbcase, In edge TIn (hb_fst edge) V).
          {
            clear Z0 TYP; subst T; ins; desf.
            rewrite In_map in *; desf; ins; intuition.
          }
          assert (VALIDt: edge : hbcase, In edge Tedge_valid lab sb rf edge).
          {
            clear TYP Z0; subst T; ins; desf.
              by ins; apply FST.
            rewrite In_map in *; desf; ins.
            apply SUBSET, rfsOK in H0.
            red; desf; specialize (Crf x); rewrite H0, Heq in Crf; ins; desf.
          }
          assert (INDEP: independent sb rf T).
          {
            clear Z0 TYP; subst T; red; ins; desf; ins; rewrite ?In_map in *; desf; ins.
            by destruct NIN; apply INann_rfs.
            eby destruct NIN; eapply hist_closedD.
            by destruct NIN; eapply hist_closedD; try edone; apply INann_rfs.
          }
          assert (HT: hT, hsum (map hmap T) = Hdef hT
                       PT QT isrmwT permT initT, hT E = HVra PT QT isrmwT permT initT
                             QT v0 = mk_assn_mod (Astar (Astar (QQ v0) (QQ0 v0)) (sval QQread))).
          {
            clear TYP; revert Z0; subst T.
            exploit independent_heap_compat; try exact HC; try eassumption; eauto.
              by exact (proj1 VALID).
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; rewrite In_map in *; desf; intuition.
              by ins; desf; [apply FST | rewrite In_map in *; desf].
              by ins; desf; rewrite In_map in *; desf.
              by ins; desf; exploit (VALIDt (hb_sink a)); ins; eauto.
            intros SUM ?; desc.
            eexists,; try edone.
            ins; rewrite hsum_cons, Z, SINKS in SUM.
            clear - SUM Z0.
            apply hplus_def_inv in SUM; desc.
            inv SUM.
            generalize (PLUSv E); rewrite Z0, hupds; clear; ins.
            repeat eexists; eauto.
            clear; ins; apply AsimD.
            apply Asim_star.
            by apply Asim_sym, Asim_assn_norm.
            by rewrite hupds; apply Asim_refl.
          }
          subst P; desc.
          exploit (wellformed_w FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Ca Crf HC (proj1 VALID)
                   pre wri INwri EQ (proj1 pU) pEQ0 XXX NDt INt VALIDt INDEP HT HT0); try exact TRAN0.
          rewrite HT1; intro WF; simpls; desc.
          rewrite assn_sem_assn_norm in ×.
          subst .
          rewrite rfEQ in ×.
          clear - PREC NORM PRECISE NORMALIZABLE rfsSIM TRAN TRAN0 TRAN1 TRAN2 TRAN READS READS0 READS1 READS2
                  WF WF1 WF2.
          ins; desf.
          assert (EQ: hsum (map hmap (map (hb_rf wri) ann_rfs)) +!+ hmap (hb_sink wri)
                      = lupd (h4 +!+ h5 +!+ h3 +!+ h2) HLnabla) by (by rewrite !hplusA in TRAN1; apply lupd_eq).
          assert (EQ´: hsum (map hmap (map (hb_rf wri) ann_rfs)) = lupd h´0 HLnabla) by (by apply lupd_eq).
          rewrite EQ´, !(hplusAC h3), !lupd_hplus_dist in EQ.
          specialize (NORMALIZABLE _ WF4); desc.
          subst h3.
          rewrite lupd_hplus_dist, hplusA in EQ.
          apply precise_nabla in PRECISE.
          assert (SAT0: assn_sem (Anabla (sval QQread)) (lupd h´0 HLnabla)).
          {
            split.
              eby eapply lupd_label, assn_sem_def.
             h´0; repeat (apply conj); try done.
            eby eapply Hsim_sym, lupd_sim, assn_sem_def.
          }
          assert (SATn: assn_sem (Anabla (sval QQread)) (lupd hN HLnabla)).
          {
            split.
              eby eapply lupd_label, assn_sem_def.
             hN; repeat (apply conj); try done.
            eby eapply Hsim_sym, lupd_sim, assn_sem_def.
          }
          assert (DEF: lupd h´0 HLnabla +!+ hmap (hb_sink wri) Hundef).
          {
            rewrite EQ´ in rfsSIM.
            red in rfsSIM; desc; congruence.
          }
          exploit (PRECISE _ SAT0 _ SATn _ DEF).
            by exact EQ.
          intro DECOMP; desc.
          apply exact_label_sim with (lbl := HLnabla) in DECOMP0.
            2: by apply exact_label_hplus_dist in TRAN; desc.
            2: by rewrite <- !lupd_hplus_dist in *; apply lupd_label;
               red in DECOMP0; desc; intro U; rewrite U in ×.
          specialize (NORM _ _ WF6); desc.
          subst h4.
          rewrite lupd_hplus_dist, hplusA, hplusAC in DECOMP0.
          eexists,,; [by exact DECOMP0 | ].
          split; [by apply lupd_label; intro U; rewrite U, !hplus_undef_r in × | ].
          eexists; repeat apply conj; try exact NORM; try edone.
          eby eapply Hsim_sym, lupd_sim, assn_sem_def.
      }
    }

    clear Z Z0 Z1; desc.

    assert (WOK: hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) wri).
    {
      red; rewrite EQ.
      eexists,,; repeat (split; try edone); right; split; try done.
       rfs, hr, hF, P.
      assert(SAME: hsum (map (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) (map (hb_rf wri) rfs))
                   +!+ mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink (hb_sink wri)
                   = hsum (map hmap (map (hb_rf wri) rfs)) +!+ hmap (hb_sink wri)).
      {
        clear TYP.
        rewrite <- rfsOK in RF.
        apply In_implies_perm in RF as [rfs´ PERM].
        rewrite !(hsum_perm (map_perm _ (map_perm _ PERM))); ins.
        rewrite !hsum_cons.
        rewrite !map_upd_irr; ins.
          2: by intro; desf; apply Permutation_NoDup, nodup_cons in PERM; ins; desf.
        unfold mupd; desf; desf.
        desf.
        symmetry; rewrite (hplusC h1), Y, !hplusA, <- hplus_emp_l.
        f_equal.
        eapply (proj2 VALID); eauto.
        right; split; ins.
        unfold is_sb_out; intro; desf.
      }

      rewrite <- SAME in *; unnw; repeat (split; try done).
      eby eexists,.
    }

    clear TYP.

    assert (FOO: hmap_valids lab sb rf (mupd (mupd hmap (hb_rf wri fst) h1) (hb_sink wri) hsink) V).
    {
      red.
      intros; destruct (eqP e wri); desf.
      eapply hmap_irr_change_valid.
        by apply VALID.
      ins; unfold mupd; desf; desf; ins; desf.
    }

    ins; desc.

    assert (DEF: hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))
                 +!+ h´0 +!+ hFR Hundef).
    {
      red in CONS; desc; ins.
      exploit (independent_heap_compat FIN (AcyclicStrong_implies_IrreflexiveHBuRF ACYC) Crf Ca HC FOO
                                           (T := hb_rf wri fst :: hb_sb prev fst :: nil));
        try solve [ by rewrite NoDup_two | ins; desf; apply FST].
        by eapply independent_two; ins; eauto; try (by apply FST); intro; desf; eauto with hb.
      intro DEF; desc.
      ins; rewrite hsum_two in DEF.
      unfold mupd in DEF; desf; desf.
      pattern h in DEF; eapply ex_intro in DEF; rewrite <- hdef_alt, pEQ in DEF.
      apply (hplus_sim_def _ Y2) in DEF.
      assert (D: hsingl E (HVra Wemp (fun x : valmk_assn_mod (QQ x)) false None (Some HLCnormal))
                 =
                 hsingl E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None)
                 +!+
                 hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None (Some HLCnormal))).
      {
        clear; rewrite hplus_hsingl; simpl; vauto.
        repeat f_equal; desf.
        extensionality v.
        apply AsimD.
        unfold hupd; desf; desf; ins.
        by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_r].
        by rewrite assn_norm_emp; eapply Asim_trans; [apply Asim_assn_norm | apply Asim_star_emp_l].
      }
      rewrite hplusAC, D, hplusA in DEF.
      by intro U; rewrite U, hplus_undef_r in DEF.
    }

    eapply safe_final4a with
      (h := hsingl E (HVra Wemp (fun x : valmk_assn_mod ((hupd QQ v0 Aemp) x)) false None (Some HLCnormal))
             +!+ h1 +!+ hFR)
      (hs := hsingl E (HVra Wemp (hupd Remp v0 (mk_assn_mod (QQ v0))) false None None));
    eauto.

    { hemp; rewrite hplus_emp_r.
      eexists; repeat split; try done.
      × rewrite hplusAC; rewrite hplusAC in DEF.
        eapply hplus_sim_def; try exact DEF.
        by apply Hsim_sym.
      × by rewrite <- hplusA.
      × eexists _, (hsingl E (HVra Wemp Remp false None (Some HLCnormal)) +!+ h1); repeat (split; try edone).
          rewrite <- hplusA in DEF.
          apply hplus_not_undef_l in DEF.
          rewrite hplusC; rewrite hplusC in DEF.
          eapply hplus_sim_def; try exact DEF.
          by apply Hsim_sym.
          by rewrite <- hplusA, hplus_init1.
        eexists _, h1; repeat (split; try edone).
        + rewrite <- ohlplus_none_l in DEF at 1.
          rewrite <- (ohlplus_none_l (Some HLCnormal)) in DEF.
          rewrite <- hplus_init1, hplusA, <- (hplusA _ h´0) in DEF.
          apply hplus_not_undef_r, hplus_not_undef_l in DEF.
          rewrite hplusC; rewrite hplusC in DEF.
          eapply hplus_sim_def; try exact DEF.
          by apply Hsim_sym.
        + eexists; repeat (apply conj); solve [exact Y1 | exact Y2 | exact Y3].
    }

    { red; rewrite SEM1.
      rewrite hdef_alt in pDEF; desc.
      eexists _, _, hf0; repeat (split; try edone).
        by unfold NW, mupd; desf; desf.
      right.
      split; [done | ].
      eexists (wri :: nil), h1, _, (mk_assn_mod (QQ v0)).
      repeat (apply conj; try edone); ins; rewrite ?hsum_one; unfold mupd; desf; desf.
      × split; ins; desf; eauto.
      × h´0; repeat split; try done.
        by simpl; rewrite assn_sem_assn_norm.
      × apply Hsim_refl.
        red in Y0; desf.
      × instantiate
          (1 := hsingl E (HVra Wemp (fun x : valmk_assn_mod (hupd QQ v0 Aemp x)) false None None) +!+ hFR).
        rewrite <- hplusA, hplus_hsingl, <- pDEF, pEQ; vauto.
        ins; unnw; repeat f_equal; extensionality v; desf.
        clear; apply AsimD.
        unfold hupd; desf; desf; ins.
        by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
           [apply Asim_star_emp_r | apply Asim_assn_norm].
        by rewrite assn_norm_emp; eapply Asim_trans; apply Asim_sym;
           [apply Asim_star_emp_l | apply Asim_assn_norm].
      × rewrite hplusAC; rewrite hplusAC in DEF.
        eapply hplus_sim_def; try exact DEF.
        by apply Hsim_sym.
      × rewrite !(hplusC h1), <- !hplusA.
        unnw; repeat f_equal.
        rewrite hplusC, hplus_init1; simpl.
        unnw; f_equal.
      × eauto.
      × by unnw; rewrite <- precise_assn_norm.
      × by unnw; rewrite <- normalizable_assn_norm.
    }
  }

Grab Existential Variables. edone.
Qed.


This page has been generated by coqdoc