Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsSepAlg GpsModel GpsModelLemmas.
Require Import GpsGlobal GpsVisible GpsGlobalHelper.

Local Open Scope string_scope.

Set Implicit Arguments.

Lemma in_sb_add :
  ∀ a acts b L r,
    In a acts →
    NoDup acts →
    L (Tsb a b) = res_emp →
    in_sb acts (upd L (Tsb a b) r) b = r +!+ in_sb acts L b.
Proof.
  unfold in_sb; ins; rewrite replace_edge_emp; ins.
  eapply nodup_map; congruence.
  eapply in_map_iff; eauto.
Qed.

Lemma incoming_add b acts L a r :
  In a acts →
  NoDup acts →
  L (Tsb a b) = res_emp →
  incoming acts (upd L (Tsb a b) r) b = r +!+ incoming acts L b.
Proof.
  unfold incoming, in_rf, in_esc; ins; rewrite in_sb_add, ?map_upd_irr; ins;
  try (by intro X; apply in_map_iff in X; desf); rewrite !res_plusA; ins.
Qed.

Lemma outgoing_ext_one acts L EE b r :
  outgoing acts L EE b = res_emp →
  outgoing acts (upd L (TsbS b) (L (TsbS b) +!+ r)) EE b = r.
Proof.
  unfold outgoing, out_sb, out_rf, out_esc; rupd.
  rewrite !map_upd_irr; try (by intro; rewrite in_map_iff in *; desf).
  rewrite !res_plusA, (res_plusAC r); intros ->; apply res_plus_emp_r.
Qed.

Lemma outgoing_upd2 b acts L EE a r r_rem c :
  In a acts →
  ¬ In b acts →
  L (TsbS a) = r +!+ r_rem →
  L (Tsb a b) = res_emp →
  outgoing (b :: acts) (upd (upd L (Tsb a b) r) (TsbS a) r_rem) EE c =
  outgoing (b :: acts) L EE c.
Proof.
  unfold outgoing, out_sb, out_rf, out_esc; ins;
  rewrite !map_upd_irr; try (by intro; rewrite in_map_iff in *; desf).
  by unfold upd; desf; rewrite H1, H2, res_plus_emp_l, !res_plusA, (res_plusAC r).
Qed.

Lemma prepare_step :
  ∀ b acts amap sb rf mo sc
    (CONS: Consistent (b :: acts) amap sb rf mo sc)
    (NIN : ¬ In b acts)
    (ND : NoDup (b :: acts)) a
    (SB : sb a b) amap_old sb_old rf_old mo_old sc_old
    (OCON: Consistent acts amap_old sb_old rf_old mo_old sc_old) L EE
    (LR : label_restr acts amap_old sb_old rf_old L EE)
    (NDE : NoDup EE) r r_rem
    (LAB : L (TsbS a) = r +!+ r_rem) IE
    (V : ∀ a, In a acts → valid_node IE acts acts amap_old rf_old L EE a)
    (CC : compat amap_old sb_old rf_old L)
    (CO : conform acts amap_old mo_old L acts)
    (ECO : ∀ sigma, exch_conform IE acts amap_old sb_old rf_old L L EE sigma)
    (GAC : ghost_alloc_conform acts L EE)
    (Ea : ∀ x, In x acts → amap x = amap_old x)
    (Esb : ∀ x y, sb x y ↔ sb_old x y ∨ x = a ∧ y = b)
    (Erf : ∀ x, x ≠ b → rf x = rf_old x)
    (Emo : ∀ x, x ≠ b → ∀ y, y ≠ b → (mo x y ↔ mo_old x y))
    (Esc : ∀ x, x ≠ b → ∀ y, y ≠ b → (sc x y ↔ sc_old x y)),
  ∃ L',
    << V : ∀ a, In a acts → valid_node IE (b :: acts) acts amap rf L' EE a >> ∧
    << CC : compat amap sb rf L' >> ∧
    << CO : conform (b :: acts) amap mo L' acts >> ∧
    << ECO : ∀ sigma, exch_conform IE (b::acts) amap sb rf
                (upd L' (TsbS b) (L' (TsbS b) +!+ in_sb (b :: acts) L' b))
                (upd L' (TsbS b) (L' (TsbS b) +!+ in_sb (b :: acts) L' b)) EE sigma >> ∧
    << GAC: ghost_alloc_conform (b::acts)
               (upd L' (TsbS b) (L' (TsbS b) +!+ in_sb (b :: acts) L' b)) EE >> ∧
    << LAB : L' (TsbS a) = r_rem >> ∧
    << LSB : in_sb (b :: acts) L' b = r >> ∧
    << LR : label_restr (b :: acts) amap sb rf L' EE >> ∧
    << Irf : in_rf (b :: acts) L' b = res_emp >> ∧
    << Iesc: in_esc (b :: acts) L' b = res_emp >> ∧
    << Isb : ∀ a', a' ≠ a → L' (Tsb a' b) = res_emp >> ∧
    << O : outgoing (b :: acts) L' EE b = res_emp >> ∧
    << LEQ : ∀ a', a' ≠ a → L' (TsbS a') = L (TsbS a') >> ∧
    << PC : prefix_closed sb rf acts >>.
Proof.
  ins; unfold NW.
  assert (NEQ: a ≠ b).
    by intro; subst; red in CONS; desc; edestruct ACYC; eauto using t_step.
  ∃ (upd (upd L (Tsb a b) r) (TsbS a) r_rem).

  assert (INa : In a acts).
    by red in CONS; desc; apply FIN, proj1 in SB; ins; desf.

  assert (SBbx : ∀ x, L (Tsb b x) = res_emp).
    by intros; apply LR; intro X; eapply (proj2 (proj1 OCON)) in X; desf.
  assert (SBxb : ∀ x, L (Tsb x b) = res_emp).
    by intros; apply LR; intro X; eapply (proj2 (proj1 OCON)) in X; desf.

  assert (RFbx : ∀ x, L (Trf b x) = res_emp).
    by intros; apply LR; intro X; eapply (Consistent_sw_in OCON) in X; desf.
  assert (RFxb : ∀ x, L (Trf x b) = res_emp).
    by intros; apply LR; intro X; eapply (Consistent_sw_in OCON) in X; desf.

  assert (ESCbx : ∀ x, L (Tesc b x) = res_emp).
    by intros; apply LR; intro X; eapply (Consistent_hb_in OCON) in X; desf.
  assert (ESCxb : ∀ x, L (Tesc x b) = res_emp).
    by intros; apply LR; intro X; eapply (Consistent_hb_in OCON) in X; desf.

  assert (SBimp: ∀ a b, sb_old a b → sb a b).
    by intros; rewrite Esb; vauto.

  assert (SWimp: ∀ a b,
       synchronizes_with amap_old rf_old a b →
       synchronizes_with amap rf a b).
    ins; red; red in H; desf.
    assert (In a0 acts) by (by apply (proj1 (proj1 OCON)); intro X; rewrite X in *).
    assert (In b0 acts) by (by apply (proj1 (proj1 OCON)); intro X; rewrite X in *).
    rewrite Erf, !Ea; ins; congruence.

  assert (HBimp: ∀ a b,
       happens_before amap_old sb_old rf_old a b →
       happens_before amap sb rf a b).
    by induction 1; unfold imm_happens_before in *; desf;
       eauto using hb_trans, hb_sw, hb_sb.

  split; ins.
  red; unfold NW.
  specialize (V _ H); red in V; desf; ∃ r0.
  rewrite replace_out_sb; vauto.
  unfold incoming, out_rf, out_esc, in_rf, in_esc in ×.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; ins; desf; congruence).
  unfold in_sb, out_sb in *; ins; rupd; try congruence.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; ins; desf; congruence).
  rewrite !SBbx, !RFbx, !ESCbx, SBxb, RFxb, ESCxb, !res_plus_emp_l; ins.
  rewrite (Ea _ H), ?escr_ffun_upd_irr; try done.
  repeat (split; try done).
    ins; rupd; rewrite Ea in RMW, IACQ; rewrite Erf in RF; ins; eauto; congruence.
    ins; rupd; eapply VrfS; ins; rewrite <- Ea in RMW, IACQ;
    rewrite <- Erf in RF; eauto; congruence.

  by rewrite LAB, SBxb, res_plus_emp_l.

  split.
    rewrite updC; ins; apply compat_upd2; ins.
        red; ins; eapply CC; eauto; ins; eapply IND with (te:=te) (te':=te'); eauto.
        by rewrite mhbE in *; desf; eauto.
      by rewrite LAB, res_plusC; vauto.
    by rewrite LAB, SBxb, (res_plusC r); vauto.

  assert (SIMP: in_sb (b :: acts) (upd (upd L (Tsb a b) r) (TsbS a) r_rem) b = r).
    unfold in_sb; ins; rupd; try congruence; rewrite SBxb, res_plus_emp_l.
    inv ND; eapply In_NoDup_Permutation in INa; eauto; desf.
    rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INa))); ins; rupd.
    rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; ins; desf; congruence).
    by rewrite rsum_map_map_eq_empI, res_plus_emp_r; ins.
  rewrite SIMP; clear SIMP.

  assert (O : outgoing (b :: acts) (upd (upd L (Tsb a b) r) (TsbS a) r_rem) EE b =
          res_emp).
    unfold outgoing, out_sb, out_rf, out_esc, in_rf, in_esc; ins; rupd; try congruence.
    rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; ins; desf; congruence).
    by repeat first [apply rsum_map_map_eq_empI; ins | apply res_plus_eq_empI| by apply LR; auto].
  rewrite O.

  assert (II : incoming (b :: acts) L b = res_emp).
    unfold incoming, in_sb, in_rf, in_esc; ins; rupd; try congruence.
    by repeat first [apply rsum_map_map_eq_empI; ins | apply res_plus_eq_empI| by apply LR; auto].

  assert (LR': label_restr (b :: acts) amap sb rf
             (upd (upd L (Tsb a b) r) (TsbS a) r_rem) EE).
    apply lr_upd_sbS; auto using in_cons.
    apply lr_upd_sb; auto using in_cons.
    by red; unfold NW; repeat split; ins; apply LR; desf; vauto;
       try left; intro; desf; destruct H; auto.

  split; rupd.
    red; ins.
    rewrite Emo in *; try congruence.
    rewrite (Ea _ INa0), (Ea _ INb) in ×.
    exploit CO; try exact MO; eauto.
    by unfold out_rf; ins; rupd; rewrite !RFxb, !map_upd_irr, !res_plus_emp_l;
       ins; rewrite in_map_iff; intro; desf.

  unfold outgoing, out_sb, out_rf, out_esc, in_rf, in_esc; ins; rupd; try congruence.
  rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; ins; desf; congruence).
  rewrite !RFbx, !ESCbx, !res_plus_emp_l.

  repeat (split; try done); unfold NW; ins; rupd;
  eauto using rsum_map_map_eq_empI; try congruence.

  assert (INESC: ∀ a, in_esc (b :: acts) L a = in_esc acts L a).
    by ins; unfold in_esc; ins; rewrite ESCbx, res_plus_emp_l.

  assert (∀ a', incoming (b :: acts) L a' = incoming acts L a').
    clear -SBbx RFbx ESCbx; unfold incoming, in_sb, in_rf, in_esc; ins.
    by rewrite SBbx, RFbx, ESCbx, !res_plus_emp_l.

  assert (∀ a', outgoing (b :: acts) L EE a' = outgoing acts L EE a').
    clear -SBxb RFxb ESCxb; unfold outgoing, out_sb, out_rf, out_esc; ins.
    by rewrite SBxb, RFxb, ESCxb, !res_plus_emp_l.

  rewrite 2!updC with (l := Tsb a b); ins.
  eapply exch_conform_irr1; ins.
  rewrite updC; try congruence.
  eapply exch_conform_dec_irr1; ins; rupd; ins; try congruence.
  2: by rewrite LAB; apply res_lt_plus_l, res_lt_refl.
  2: by intro X; eapply (CC (TsbS a :: nil)); ins; desf; rewrite X.
  rewrite !(updC (l:=TsbS b)); ins; try congruence.
  rewrite !outgoing_upd_irr in O; ins.
  eapply exch_conform_upd3 with (rr := L (TsbS b)); ins; try congruence; eauto;
  rewrite ?updI, ?SBxb, ?SBxb, ?O, ?res_plus_emp_l, ?res_plus_emp_r in *; ins.
  2: by rewrite res_plusC.
  2: by intro X; eapply (CC (TsbS a :: nil)); ins; desf; rewrite LAB.
  red; ins; rupd.
  assert (XX: L (TsbS b) = res_emp) by (apply LR; ins).
  rewrite XX, res_plus_emp_l in ×.
  unfold upd in ESC; desf; ins.
    edestruct (ECO sigma (TsbS a)) as (a' & M & M'); ins.
      rewrite LAB, res_escr_plus; eauto.
      by intro X; eapply (CC (TsbS a :: nil)); ins; desf; rewrite LAB, X.
    ∃ a'; split; rupd; rewrite H, H0; desf; eauto.
    by left; rewrite mhbE in *; desf; eauto using hb_trans.
  edestruct (ECO sigma edge) as (a' & M & M'); ins.
  ∃ a'; split; rupd; rewrite H, H0; desf; eauto.
  by left; rewrite mhbE in *; desf; eauto using hb_trans.

  red; intros; rewrite 2!incoming_upd_irr in *; try done.
  rewrite <- !updC with (l := TsbS b) in *; try congruence.
  rewrite outgoing_upd2 in *; ins; rupd; try (by intro; desf).
  desf; rewrite ?outgoing_ext_one in *; ins; desf;
  try rewrite incoming_add, II, res_plus_emp_r in *; desf; eauto using in_cons.
  revert INC INC' OUT OUT'.
  unfold outgoing, incoming, out_sb, in_sb, out_rf, in_rf, out_esc, in_esc; simpl;
    rupd; rewrite ?map_upd_irr; try (intro X; desf; rewrite in_map_iff in X; desf).
  rewrite !SBbx, !SBxb, !RFbx, !RFxb, !ESCbx, !ESCxb, !res_plus_emp_l.
  by ins; eapply GAC; eauto.

  rewrite Esb in SB0; desf.
  by eapply (Consistent_prefix_closed OCON) in SB0; eauto.

  rewrite Erf in RF; desf; try congruence.
  by eapply (Consistent_prefix_closed OCON) in RF; eauto.

  congruence.
Qed.