Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import fslhmap stepbackr.

Set Implicit Arguments.

Lemma initialization_always_before PS PSg:
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    hf g (MAP: hmap edge = @Hdef PS PSg hf g) l lbl (LAB: HVlabeledR (hf l) lbl),
  ∃ a, << STORE: is_writeL (lab a) l >> ∧
    ((<< LBL: lbl = HLnormal >> ∧ << HB: clos_refl_trans _ (happens_before lab sb rf mo) a (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLtriangle >> ∧ ∃ b, << REL: is_release_fence (lab b) >> ∧
                                               << HB: happens_before lab sb rf mo a b >> ∧
                                               << SB: clos_refl_trans _ sb b (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << SB: ¬ is_rf edge >>
                                  ∧ ∃ b b' c, << REL: is_release_write (lab b) >> ∧
                                                    << HB: clos_refl_trans _ (happens_before lab sb rf mo) a b >> ∧
                                                    << RSQ: release_seq lab sb rf mo b b' >> ∧
                                                    << RF: rf c = Some b' >> ∧
                                                    << SB: clos_refl_trans _ sb c (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << SB: ¬ is_rf edge >>
                                  ∧ ∃ b c c' d, << REL: is_release_fence (lab b) >> ∧
                                                      << HB: happens_before lab sb rf mo a b >> ∧
                                                      << SB1: clos_trans _ sb b c >> ∧
                                                      << RSQ: release_seq lab sb rf mo c c' >> ∧
                                                      << RF: rf d = Some c' >> ∧
                                                      << SB2: clos_refl_trans _ sb d (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << RF: ¬ is_sb edge >> ∧
                                  ∃ b, << REL: is_release_write (lab b) >> ∧
                                            << HB: clos_refl_trans _ (happens_before lab sb rf mo) a b >> ∧
                                            << RSQ: release_seq lab sb rf mo b (hb_fst edge) >>) ∨
     (<< LBL: lbl = HLnabla >> ∧ << RF: ¬ is_sb edge >> ∧
                                  ∃ b c, << REL: is_release_fence (lab b) >> ∧
                                              << HB: happens_before lab sb rf mo a b >> ∧
                                              << SB: clos_trans _ sb b c >> ∧
                                              << RSQ: release_seq lab sb rf mo c (hb_fst edge) >>)).
Proof.
  intros until hf; revert hf; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  red in VALID; desc.
  destruct lbl.

  {
    exploit step_back_from_normalR; eauto.
    ins; desf.
    × eexists; split; eauto.
      left; split; vauto.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      eexists; split; eauto.
      left; split; eauto.
      eapply rt_trans; eauto.
      apply rt_step; destruct edge'; ins; desf; vauto.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf; try by destruct edge'.
      + eexists; split; eauto.
        left; split; eauto.
        eapply rt_trans; eauto.
        apply rt_step, t_step.
        right; red.
        right; left.
        repeat split; eauto.
        eexists _, _; repeat split.
          3: by eassumption.
          2: by vauto.
        eapply rt_trans; eauto.
        apply rt_step.
        destruct edge'; ins; desf.
      + eexists; split; eauto.
        left; split; eauto.
        eapply rt_trans.
          eby apply rt_step.
        apply rt_step, t_step.
        right; red.
        repeat right.
        repeat split; eauto.
        eexists _, _, _; repeat split.
          4: by eassumption.
          3: by vauto.
          by rewrite clos_refl_transE; eauto.
        eapply rt_trans; eauto.
        apply rt_step.
        destruct edge'; ins; desf.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      + eexists; split; eauto.
        left; split; eauto.
        eapply rt_trans; eauto.
        eapply rt_step, t_step.
        right; red.
        left; desf; repeat split; ins.
        destruct edge'; ins; desf.
        eexists; split; try eassumption; vauto.
      + eexists; split; eauto.
        left; split; eauto.
        eapply rt_trans.
          eby apply rt_step.
        eapply rt_step, t_step.
        right; red.
        do 2 right; left.
        repeat split; eauto.
        destruct edge'; ins; desf.
        eexists _, _; repeat split; eauto.
        by rewrite clos_refl_transE; eauto.
  }

  {
    exploit step_back_from_triangleR; eauto.
    ins; desf.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      eexists; split; eauto.
      right; left.
      split; eauto.
      eexists; repeat split; eauto.
      eapply rt_trans; eauto.
      apply rt_step.
      destruct edge'; ins; desf.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      eexists; split; eauto.
      right; left.
      split; eauto.
      eexists; repeat split; eauto.
        2: by vauto.
      apply clos_refl_trans_hbE in HB; desf.
      + eapply t_trans; eauto.
        apply t_step; left.
        destruct edge'; ins; desf.
      + apply t_step; left.
        destruct edge'; ins; desf.
  }

  {
    exploit step_back_from_nablaR; eauto.
    ins; desf.

    × ∃ (hb_fst edge); clear IH; split; eauto.
      do 4 right; left.
      intuition.
      eexists; repeat split; vauto.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf; try by destruct edge'.
      + eexists; split; eauto.
        do 2 right; left.
        repeat split; eauto.
        eexists _, _, _; repeat split; eauto.
        eapply rt_trans; eauto.
        apply rt_step.
        destruct edge'; ins; desf.
      + eexists; split; eauto.
        do 3 right; left.
        repeat split; eauto.
        eexists _, _, _, _; repeat split; eauto.
        eapply rt_trans; eauto.
        apply rt_step.
        destruct edge'; ins; desf.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      + eexists; split; eauto.
        do 2 right; left.
        repeat split; eauto.
        destruct edge'; ins; desf.
        eexists _, _, _; repeat split; vauto.
      + eexists; split; eauto.
        do 3 right; left.
        repeat split; eauto.
        destruct edge'; ins; desf.
        eexists _, _, _, _; repeat split; vauto.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      eexists; split; eauto.
      repeat right.
      repeat split; eauto.
      eexists _, _; repeat split; eauto.
        2: by apply RS_refl.
      rewrite clos_refl_transE in SB; desf.
      + destruct edge'; ins; desf; vauto.
      + eapply t_trans; eauto.
        destruct edge'; ins; desf; vauto.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      eexists; split; eauto.
      do 4 right; left.
      repeat split; eauto.
      eexists; repeat split; vauto.
      eapply rt_trans; eauto.
      apply rt_step, t_step.
      left.
      red in SB'; desf; ins.
      congruence.
    × exploit (IH edge'); clear IH; eauto.
        by apply t_step; destruct edge'; ins; desf; vauto.
      ins; desf.
      + eexists; split; eauto.
        do 4 right; left.
        repeat split; try done.
        eexists; repeat split; eauto.
        eapply RS_rmw; eauto.
        destruct edge'; ins; desf.
      + eexists; split; eauto.
        repeat right.
        repeat split; try done.
        eexists _, _; repeat split; eauto.
        eapply RS_rmw; eauto.
        destruct edge'; ins; desf.
  }
Qed.

Theorem valid_implies_initialized_reads PS PSg :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: @hmap_valids PS PSg lab sb rf hmap V),
  initialized_reads V lab rf.
Proof.
  red; ins.
  assert (VALID' := VALID); red in VALID'; desc.
  exploit valid_readD; eauto; ins; desf.
    by destruct (lab a).
  exploit initialization_always_before; eauto; ins; desf.
    by eapply HC; eauto; vauto.
  intro.
  specialize (CONS_RF a); desf.
  assert (L: loc (lab a) = l) by (destruct (lab a); ins; desf).
  rewrite L in ×.
  eapply CONS_RF; eauto.
  apply clos_refl_trans_hbE in HB; desf; vauto.
  eapply t_trans; eauto.
  apply t_step; vauto.
Qed.