Helper lemmas for triples


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

Set Implicit Arguments.

We develop the following helper lemma in order to simplify the proofs of various RSL proof rules.

Lemma triple_helper_start PS PSg P e QQ :
  ( res acts_cmd lab sb fst lst
      (SEM : exp_sem e res acts_cmd lab sb fst lst) acts_ctx rf mo sc
      (CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc Model_hb_rf_acyclic)
      (UNIQ : NoDup (acts_cmd ++ acts_ctx))
      prev (FST : unique (sb^~ fst) prev)
      next (LST : unique (sb lst) next)
      n V (V_PREV : In prev V)
      (V_CTX : x : actid, In x V In x acts_ctx)
      (HC : hist_closed sb rf V)
      hmap
      (VALID : hmap_valids_strong lab sb rf hmap V)
      (pDEF : hmap (hb_sb prev fst) @Hundef PS PSg) hp hFR
      (pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
      (pSAT : assn_sem P hp)
      (NIN : ¬ In fst V)
      (HC : hist_closed sb rf (fst :: V))
      (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst),
    hmap',
     agrees sb rf V hmap hmap'
     (hmap_valids_strong lab sb rf hmap' (fst :: V))
     safe acts_cmd acts_ctx lab sb rf n (fst :: V) hmap' lst
       (with_opt res
                 (fun res h hFR' hq, h @Hundef PS PSg h = hq +!+ hFR +!+ hFR'
                                           assn_sem (QQ res) hq)))
  triple P e QQ.
Proof.
  intros until n.
  induction n; ins; unfold NW; repeat split; ins; desf.
  × by exfalso; rewrite nodup_app in UNIQ; desf; eauto using exp_sem_lst.
  × eapply IHn; eauto using In_cons; [by ins; desf; eauto| |];
    destruct FST; rewrite (proj1 (HEQ _ V_PREV _)) in pDEF, pEQ; eauto.
  × cut (a = fst).
    {
      ins; subst; eapply H; eauto using exp_sem_lst_reach.
    }
    {
      assert (M: In fst (a :: V)).
        by eapply (hist_closed_trans HC'); eauto using exp_sem_fst_reach, In_eq.
      ins; desf; apply V_CTX in M; ins.
      by exfalso; rewrite !nodup_app in *; desf; eauto using exp_sem_fst.
    }
Qed.

Configuration safety is invariant over Permutations of acts_cmd.

Lemma Permutation_safe1 PS PSg :
   l l' (P : Permutation l l') acts lab sb rf n V hmap lst Q,
    @safe PS PSg l acts lab sb rf n V hmap lst Q
    safe l' acts lab sb rf n V hmap lst Q.
Proof.
  induction n; ins; desc; repeat split; unfold NW; ins; eauto.
  edestruct GUAR; desc; eauto.
  eby eapply Permutation_in; try eapply Permutation_sym.
Qed.

We now develop a number of lemmas for establishing configuration safety of final configurations.

Lemma map_upd_irr (A: eqType) B C (hmap : A B) x y f (l : list C) :
  ( a, In a l f a x)
  map (mupd hmap x y) (map f l) = map hmap (map f l).
Proof.
  unfold mupd; induction l; ins; desf; f_equal; eauto.
  exfalso; intuition eauto.
Qed.

Definition ga_agrees (ga ga': val option actid) e := x, ga x = Some e ga' x = Some e.

Definition ga_clear (ga: val option actid) e l :=
  if excluded_middle_informative(ga l = Some e) then None else ga l.

Lemma ga_agrees_same: ga e, ga_agrees ga ga e.
Proof.
  red; ins.
Qed.

Lemma ga_agrees_sym: ga ga' e, ga_agrees ga ga' e ga_agrees ga' ga e.
Proof.
  unfold ga_agrees; split; desf; ins; firstorder.
Qed.

Lemma ga_clear_agrees: ga e e', e e' ga_agrees ga (ga_clear ga e) e'.
Proof.
  unfold ga_agrees, ga_clear; ins; desf.
  split; ins; desf.
Qed.

Lemma ga_clear_fin ga e:
 ( max, n, max < n ga n = None)
  max, n, max < n ga_clear ga e n = None.
Proof.
  ins; desf.
   max; ins.
  unfold ga_clear; desf.
  by apply H.
Qed.

Lemma valid_ext PS PSg :
   lab sb rf hmap ga ga' e V
      (VAL : @hmap_valid PS PSg lab sb rf hmap ga e) (IN: In e V)
      (GAA : ga_agrees ga ga' e)
      (HC : hist_closed sb rf V) a (NIN: ¬ In a V) b h,
    hmap_valid lab sb rf (mupd hmap (hb_sb a b) h) ga' e.
Proof.
  unfold hmap_valid, unique; ins; desf; desc;
    try (destruct DISJ; desc); try revert TYP; desf; unfold NW;
    ins; gnew; split; try (by ins; split; ins; [apply GAA, NG | apply NG, GAA]);
    try (by repeat (eexists; try edone); unfold mupd; desf; desf; eauto 8;
            destruct NIN; eapply HC; eauto; apply hc_edge_sb).

  {
     pres, posts; repeat (split; try done).
      by rewrite map_upd_irr; ins; red; intros; desf; eapply pOK in H; eauto with hb.
    rewrite !map_upd_irr; ins; intro; desf.
    destruct NIN; eapply HC; eauto.
    by apply hc_edge_sb, pOK.
  }

  {
     pre, post, hf, g; repeat (split; try done).
      by clear TYP; unfold mupd; desf; desf; exfalso; eauto with hb.
      by unfold mupd; ins; desf; desf; destruct NIN; eapply HC; eauto; apply hc_edge_sb.
    right; split; eauto.
     rfs, hr, hF, P; repeat (split; try done);
      try ( h'; repeat (split; try done));
      solve [by rewrite map_upd_irr | clear TYP; unfold mupd; desf; desf].
  }

  {
     pre, post, hf, g; repeat (split; try done).
      by clear TYP; unfold mupd; desf; desf; exfalso; eauto with hb.
    right; split; try done.
     rfs, hr, hF, P, sbg, rfg; repeat (split; try done);
      try ( h'; repeat (split; try done));
      try solve [by rewrite map_upd_irr | clear TYP; unfold mupd; desf; desf].
    clear TYP; rewrite map_upd_irr; try done.
    unfold mupd; ins; desf; desf.
  }

  {
     pre, post, rfsIn, rfsOut; repeat (split; try done).
      by rewrite map_upd_irr; ins; unfold mupd; desf; desf; eauto with hb.
    rewrite map_upd_irr; ins.
    unfold mupd at 1 2 4 ; desf; desf.
      by exfalso; eauto with hb.
    repeat (eexists; try edone).
    rewrite map_upd_irr; ins.
  }

  {
     pre, post; repeat (split; try done).
      by unfold mupd; desf; desf; exfalso; eauto with hb.
     hF, hrel, hrel', hacq, hacq'; repeat (split; try done);
      by unfold mupd; desf; desf; exfalso; eauto with hb.
  }
Qed.

Lemma valid_ext_sink PS PSg :
   lab sb rf hmap ga ga' e V
      (VAL : @hmap_valid PS PSg lab sb rf hmap ga e) (IN: In e V)
      (GAA : ga_agrees ga ga' e)
      (HC : hist_closed sb rf V) a (NIN: ¬ In a V) h,
    hmap_valid lab sb rf (mupd hmap (hb_sink a) h) ga' e.
Proof.
  ins.
  assert (EQ: mupd hmap (hb_sink a) h (hb_sink e) = hmap (hb_sink e)) by (unfold mupd; desf; desf).

  unfold hmap_valid, unique in *; ins; desf; desc;
  try (destruct DISJ; desc); try revert TYP; desf; unfold NW;
  ins; gnew; split; try (by ins; split; ins; [apply GAA, NG | apply NG, GAA]);
    try (by repeat (eexists; try edone); unfold mupd; desf; desf; eauto 8;
            destruct NIN; eapply HC; eauto; apply hc_edge_sb).

  {
     pres, posts; repeat (split; try done).
    by rewrite map_upd_irr, EQ; ins.
    by rewrite !map_upd_irr, EQ; ins.
  }

  {
     pre, post, hf, g; repeat (split; try done).
    right; split; eauto.
     rfs, hr, hF, P; repeat (split; try done); try ( h'; repeat (split; try done));
           try (by rewrite map_upd_irr); clear TYP; unfold mupd; desf; desf.
  }

  {
     pre, post, hf, g; repeat (split; try done).
    right; split; try done.
    by rfs, hr, hF, P, sbg, rfg; repeat (split; try done); try ( h'; repeat (split; try done));
                              rewrite map_upd_irr, EQ.
  }
  
  {
     pre, post, rfsIn, rfsOut; repeat (split; try done).
      by rewrite map_upd_irr; ins; unfold mupd; desf; desf; eauto with hb.
    rewrite map_upd_irr; ins.
    unfold mupd at 1 2 4 ; desf; desf.
    repeat (eexists; try edone).
    rewrite map_upd_irr; ins.
  }
Qed.

Lemma hmap_irr_change_valid PS PSg:
   lab sb rf hmap hmap' ga ga' e
    (VALID: @hmap_valid PS PSg lab sb rf hmap ga e)
    (GAA : ga_agrees ga ga' e)
    (IRR: edge, hb_fst edge = e hb_snd edge = Some e hmap' edge = hmap edge),
  hmap_valid lab sb rf hmap' ga' e.
Proof.
  ins; red; desf; red in VALID; rewrite Heq in VALID; desc;
  ins; gnew; split; try (by ins; split; ins; [apply GAA, NG | apply NG, GAA]).

  {
    cut (<< P : hsum (map hmap' (map (hb_sb^~ e) pres)) = hsum (map hmap (map (hb_sb^~ e) pres)) >>
         << P': hsum (map hmap' (map (hb_sb e) posts)) = hsum (map hmap (map (hb_sb e) posts)) >>
         << S : hmap' (hb_sink e) = hmap (hb_sink e) >>).
      by ins; desf; pres, posts; unfold NW; repeat (split; try done); rewrite ?P, ? P', ?S.

    unnw; repeat split; eauto; f_equal; apply map_eq; ins; apply IRR; rewrite In_map in IN; desf; eauto.
  }

  {
     pre, post, hf, g; unfold NW; repeat (split; try done).
      by rewrite <- pEQ; apply IRR; eauto.
      by intro U; destruct DEF; rewrite <- U; symmetry; apply IRR; eauto.
    desf; [left | right; QQ, isrmw]; rewrite <- qEQ; apply IRR; eauto.
  }

  {
    assert (OK: hmap' (hb_sb pre e) = hmap (hb_sb pre e) hmap' (hb_sb e post) = hmap (hb_sb e post)).
      by split; apply IRR; eauto.
    desc.
     pre, post, hf, g; unfold NW; repeat (split; try done); try congruence.
    destruct DISJ; desc.
    {
      left; repeat split; try done; try congruence.
      by ins; erewrite <- ?rEQ; apply IRR; eauto.
      by ins; erewrite <- ?sEQ; apply IRR; eauto.
    }
    {
      assert(rOK: hsum (map hmap' (map (hb_rf^~ e) rfs)) = hsum (map hmap (map (hb_rf^~ e) rfs))).
        by clear TYP; f_equal; apply map_eq; ins; apply In_map in IN; desf; apply IRR; eauto.
      right; repeat split; try done; try congruence.
       rfs, hr, hF, P; repeat (split; try done); try congruence; rewrite ?rOK; ins; desc; try done.
      eby eexists; repeat split.
      by ins; rewrite <- ?sEQ; apply IRR; eauto.
    }
  }

  {
    assert (OK: hmap' (hb_sb pre e) = hmap (hb_sb pre e) hmap' (hb_sb e post) = hmap (hb_sb e post)).
      by split; apply IRR; eauto.
    desc.
     pre, post, hf, g; unfold NW; repeat (split; try done); try congruence.
    destruct DISJ; desc.
    {
      left; repeat split; try done; try congruence.
      by Perm; congruence.
      by ins; erewrite <- ?rEQ; apply IRR; eauto.
      by ins; erewrite <- ?sEQ; apply IRR; eauto.
    }
    {
      assert (rOK: hsum (map hmap' (map (hb_rf e) rfs)) = hsum (map hmap (map (hb_rf e) rfs))).
        by clear TYP; f_equal; apply map_eq; ins; apply In_map in IN; desf; apply IRR; eauto.
      assert (sOK: hmap' (hb_sink e) = hmap (hb_sink e)) by (apply IRR; eauto).
      right; repeat split; try done; try congruence.
       rfs, hr, hF, P, sbg, rfg; repeat (split; try done); try congruence;
        rewrite ?rOK, ?sOK; ins; desc; try done.
      eby eexists; repeat split.
    }
  }

  {
    assert (OK: hmap' (hb_sb pre e) = hmap (hb_sb pre e) hmap' (hb_sb e post) = hmap (hb_sb e post)
                 hmap' (hb_sink e) = hmap (hb_sink e)).
      by repeat split; apply IRR; eauto.
    assert(rOK: hsum (map hmap' (map (hb_rf^~ e) rfsIn)) = hsum (map hmap (map (hb_rf^~ e) rfsIn))
                hsum (map hmap' (map (hb_rf e) rfsOut)) = hsum (map hmap (map (hb_rf e) rfsOut))).
      by split; f_equal; apply map_eq; ins; apply In_map in IN; desf; apply IRR; eauto.
    ins; desc.
     pre, post, rfsIn, rfsOut; repeat (split; try done); try congruence.
    eby P, QQ, hrel, hrel', hacq, hacq', ht, hF, sbg, rfg; repeat split; try congruence; try done;
        eexists; repeat split.
  }

  {
    assert (OK: hmap' (hb_sb pre e) = hmap (hb_sb pre e) hmap' (hb_sb e post) = hmap (hb_sb e post)).
      by split; apply IRR; eauto.
    desc.
     pre, post; unfold NW; repeat (split; try done); try congruence.
     hF, hrel, hrel', hacq, hacq'; repeat (split; try done); congruence.
  }
Qed.

Lemma safe_mod PS PSg :
   acts_cmd acts_ctx lab sb rf n V hmap lst QQ
    (H : @safe PS PSg acts_cmd acts_ctx lab sb rf n V hmap lst QQ)
    acts_cmd' (E1: x (NIN: ¬ In x V) (IN: In x acts_cmd'), In x acts_cmd)
    acts_ctx' (E2: x (NIN: ¬ In x V) (IN: In x acts_ctx'), In x acts_ctx),
    safe acts_cmd' acts_ctx' lab sb rf n V hmap lst QQ.
Proof.
  induction n; ins; desf; unfold NW; repeat (split; ins).
    by eapply IHn; ins; desf; eauto; eapply RELY; eauto; eapply E2.
  exploit GUAR; eauto; intro; desf.
   hmap'; intuition.
Qed.

Lemma safe_final1 PS PSg :
   acts_cmd acts_ctx lab sb rf lst
      (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
      V Q n hmap
      (HC: hist_closed sb rf (lst :: V))
      (VALID: @hmap_valids_strong PS PSg lab sb rf hmap (lst :: V))
      (POST: next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
    safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap lst Q.
Proof.
   intros until n.
   generalize (lst :: V), (In_eq lst V); clear - LR; induction n; ins.
   unfold NW; intuition (desf; eauto).
     by eapply IHn; eauto using In_cons; ins;
        rewrite <- (proj1 (HEQ _ H next)); eauto.
   by destruct NIN; generalize (LR _ INcmd), H, HC; clear;
      induction 1; ins; eauto with hb.
Qed.

Lemma safe_final_plain PS PSg :
   acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
    (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC': hist_closed sb rf (lst :: V))
    (VLD: e (IN: In e V), hmap_valid lab sb rf hmap ga e)
    (RESTR: e (NIN: ¬ In e V) edge,
              (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge V) hmap edge = @hemp PS PSg))
    (GAA: e (IN: In e V), ga_agrees ga ga' e)
    (GA'fin: max, n, max < n ga' n = None)
    (LST: unique (fun xsb lst x) next)
    (POST: Q h : Prop)
    (VALID': hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) ga' lst)
    (NIN: ¬ In lst V),
     hmap',
      agrees sb rf V hmap hmap'
      hmap_valids_strong lab sb rf hmap' (lst :: V)
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Proof.
  ins; desc; (mupd hmap (hb_sb lst next) h).
  assert (A: agrees sb rf V hmap (mupd hmap (hb_sb lst next) h)).
    by split; unfold mupd; desf; desf.
  assert (HV: hmap_valids_strong lab sb rf (mupd hmap (hb_sb lst next) h) (lst :: V)).
  {
    split.
      by eexists; split; eauto; unnw; ins; desf; eapply valid_ext; eauto.
    unnw; ins.
    apply not_or_and in NIN0; unfold mupd; desf; desf.
    × eapply RESTR; eauto.
    × ins; desf; destruct H0; red; ins; eauto.
    × eapply RESTR; eauto.
      right; split; try done.
      intro SB; destruct H0; clear - SB.
      red in SB; split; desf; find_in_list.
  }
  repeat (split; try done).
  eapply safe_final1; ins; unfold mupd; desf; eauto.
  eapply LST in SB; congruence.
Qed.

Lemma safe_final_plain2 PS PSg :
   acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
    (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC': hist_closed sb rf (lst :: V))
    (VLD: e (IN: In e V), hmap_valid lab sb rf hmap ga e)
    (RESTR: e (NIN: ¬ In e V) edge,
              (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge V) hmap edge = @hemp PS PSg))
    (GAA: e (IN: In e V), ga_agrees ga ga' e)
    (GA'fin: max, n, max < n ga' n = None)
    (LST: unique (fun xsb lst x) next)
    (POST: Q h : Prop)
    (VALID': hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) ga' lst)
    (NIN: ¬ In lst V),
     hmap',
      agrees sb rf V hmap hmap'
      hmap_valids_strong lab sb rf hmap' (lst :: V)
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Proof.
  ins; pose (hmap' := (mupd hmap (hb_sb lst next) h)).
  ins; hmap'.
  assert (A: agrees sb rf V hmap hmap').
    by unfold hmap'; split; unfold mupd; desf; desf.
  assert (HV: hmap_valids_strong lab sb rf hmap' (lst :: V)).
  {
    split; subst hmap'.
    × unnw; red; ins; desf.
       ga'; split; eauto.
      red; ins; desf.
      eapply valid_ext; eauto.
    × unfold mupd; red; ins; desf; desf.
        by destruct NIN0; eauto.
        by eapply (RESTR (hb_fst edge)); eauto.
        by destruct H0; vauto.
      eapply (RESTR e); eauto.
      right; split; eauto.
      intro; destruct H0; unfold is_sb_out in *; desf; vauto.
  }
  repeat (split; try done).
  eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
  eapply LST in SB; congruence.
Qed.

Lemma safe_final3 PS PSg :
   acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
    (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC': hist_closed sb rf (lst :: V))
    (VLD: e (IN: In e V), hmap_valid lab sb rf hmap ga e)
    (RESTR: e (NIN: ¬ In e V) edge,
              (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge V) hmap edge = @hemp PS PSg))
    (GAA: e (IN: In e V), ga_agrees ga ga' e)
    (GA'fin: max, n, max < n ga' n = None)
    (LST: unique (fun xsb lst x) next)
    (POST: Q h : Prop)
    (VALID': hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) ga' lst)
    (NIN: ¬ In lst V),
     hmap',
      agrees sb rf V hmap hmap'
      hmap_valids_strong lab sb rf hmap' (lst :: V)
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Proof.
  ins; (mupd hmap (hb_sb lst next) h).
  assert (A: agrees sb rf V hmap (mupd hmap (hb_sb lst next) h)).
    by split; unfold mupd; desf; desf.
  assert (HV: hmap_valids_strong lab sb rf (mupd hmap (hb_sb lst next) h) (lst :: V)).
  {
    split; unnw; try red; ins.
    × ga'; split; eauto.
      red; ins; desf.
      eapply valid_ext; eauto.
    × unfold mupd; des_if.
      + subst; simpls; desf.
        by destruct NIN0; eauto.
        by destruct H0.
      + apply (RESTR e).
          by intro; destruct NIN0; eauto.
        desf; eauto.
        right; split; eauto.
        intro SB; destruct H0.
        unfold is_sb_out in *; split; desf; vauto.
  }
  repeat (split; try done).
  eapply safe_final1; ins; unfold mupd; desf; eauto.
  eapply LST in SB; congruence.
Qed.

Lemma safe_final3s PS PSg :
   acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h hs
    (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC': hist_closed sb rf (lst :: V))
    (VLD: e (IN: In e V), hmap_valid lab sb rf hmap ga e)
    (RESTR: e (NIN: ¬ In e V) edge,
              (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge V) hmap edge = @hemp PS PSg))
    (GAA: e (IN: In e V), ga_agrees ga ga' e)
    (GA'fin: max, n, max < n ga' n = None)
    (LST: unique (fun xsb lst x) next)
    (POST: Q h : Prop)
    (VALID': hmap_valid lab sb rf (mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs) ga' lst)
    (NIN: ¬ In lst V),
     hmap',
      agrees sb rf V hmap hmap'
      hmap_valids_strong lab sb rf hmap' (lst :: V)
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Proof.
  ins; pose (hmap' := mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs).
   hmap'.
  assert (A: agrees sb rf V hmap hmap').
    by subst hmap'; split; unfold mupd; desf; desf.
  assert (HV: hmap_valids_strong lab sb rf hmap' (lst :: V)).
  {
    subst hmap'; split; unnw; try red; ins.
    × ga'; split; eauto.
      red; ins; desf.
      eapply valid_ext_sink; eauto.
      eapply valid_ext; eauto.
      red; ins.
    × unfold mupd; des_if.
      + subst; simpls; desf.
        by destruct NIN0; eauto.
      + desf.
        by destruct NIN0; eauto.
        by destruct H0.
      + apply (RESTR e).
          by intro; destruct NIN0; eauto.
        desf; eauto.
        right; split; eauto.
        intro SB; destruct H0.
        unfold is_sb_out in *; split; desf; vauto.
  }
  repeat (split; try done).
  eapply safe_final1; ins; unfold mupd; desf; eauto.
  subst hmap'; eapply LST in SB; unfold mupd; desf; desf.
Qed.

Lemma safe_final4a PS PSg :
   acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q wri next hr hsinkw h hs
    (LR: x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
    (HC: hist_closed sb rf V)
    (HC': hist_closed sb rf (lst :: V))
    (VLD: e (IN: In e V), hmap_valid lab sb rf hmap ga e)
    (RESTR: e (NIN: ¬ In e V) edge,
              (hb_fst edge = e (hb_snd edge = Some e ¬ is_sb_out edge V) hmap edge = @hemp PS PSg))
    (GAA: e (IN: In e V), ga_agrees ga ga' e)
    (GA'fin: max, n, max < n ga' n = None)
    (LST: unique (fun xsb lst x) next)
    (RF: rf lst = Some wri)
    (POST: Q h : Prop)
    (VALID': hmap_valid lab sb rf (mupd
                                       (mupd
                                            (mupd
                                                 (mupd
                                                      hmap
                                                  (hb_rf wri lst) hr)
                                            (hb_sink wri) hsinkw)
                                       (hb_sb lst next) h)
                                  (hb_sink lst) hs) ga'
                              lst)
    (VALID'': hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri lst) hr) (hb_sink wri) hsinkw) ga' wri)
    (NIN: ¬ In lst V),
     hmap',
      agrees sb rf V hmap hmap'
      hmap_valids_strong lab sb rf hmap' (lst :: V)
      safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Proof.
  ins; pose (hmap' := mupd
                          (mupd
                               (mupd
                                    (mupd
                                         hmap
                                    (hb_rf wri lst) hr)
                               (hb_sink wri) hsinkw)
                          (hb_sb lst next) h)
                      (hb_sink lst) hs).
   hmap'.
  assert (A: agrees sb rf V hmap hmap').
    by subst hmap'; split; unfold mupd; desf; desf.
  assert (HV: hmap_valids_strong lab sb rf hmap' (lst :: V)).
  {
    subst hmap'; split; unnw; try red; ins.
    × ga'; split; eauto.
      red; ins; desf.
      eapply valid_ext_sink; try (by apply ga_agrees_same); eauto.
      eapply valid_ext; try (by apply ga_agrees_same); eauto.
      destruct (classic (e = wri)) as [EQ|NEQ]; desf.
      eapply hmap_irr_change_valid with (hmap := hmap) (ga := ga); eauto.
      destruct edge; unfold mupd; desf; desf; ins; desf.
    × unfold mupd; des_if.
      + subst; simpls; desf.
        by destruct NIN0; eauto.
      + subst; ins; desf.
        by destruct NIN0; eauto.
        by destruct H0; red; ins; eauto.
      + subst; ins; desf.
        destruct NIN0.
        apply (HC' lst); vauto.
      + subst; ins; desf.
        - destruct NIN0.
          apply (HC' lst); vauto.
        - destruct NIN0; eauto.
      + apply (RESTR e).
          by intro; destruct NIN0; eauto.
        desf; eauto.
        right; split; eauto.
        intro SB; destruct H0.
        unfold is_sb_out in *; split; desf; vauto.
  }
  repeat (split; try done).
  eapply safe_final1; ins; unfold hmap', mupd; desf; eauto;
  eapply LST in SB; congruence.
Qed.

This page has been generated by coqdoc