Library CompOptCert.optimizer.CSEProofStep

Require Import RelationClasses.
Require Import List.
Require Import Basics.
Require Import Coqlib.

Require Import sflib.
From Paco Require Import paco.

Require Import Basic.
Require Import Axioms.
Require Import Loc.
Require Import DenseOrder.
Require Import Language.
Require Import ZArith.
Require Import Maps.
Require Import FSets.
Require Import FSetInterface.
Require Import Lattice.
Require Import Event.
Require Import Syntax.
Require Import Semantics.

Require Import Memory.
Require Import Cell.
Require Import Time.
Require Import Thread.
Require Import Local.
Require Import CompAuxDef.

Require Import Kildall.
Require Import AveAnalysis.
Require Import CorrectOpt.
Require Import MsgMapping.
Require Import CSE.
Require Import LocalSim.
Require Import LibTactics.
Require Import Event.
Require Import View.
Require Import TView.

Require Import CSEProofAux.
Require Import CSEProofMState.

Theorem cse_match_state_implies_si:
∀ inj lo (st_tgt st_src: Language.state rtl_lang)
              (lc_tgt lc_src: Local.t)
              (mem_tgt mem_src: Memory.t)
              sc_tgt sc_src
              b,
  cse_match_state inj lo
    (Thread.mk rtl_lang st_tgt lc_tgt sc_tgt mem_tgt) (Thread.mk rtl_lang st_src lc_src sc_src mem_src) b →
  @SI rtl_lang nat inj lo (st_tgt, lc_tgt, mem_tgt) (st_src, lc_src, mem_src) DelaySet.dset_init.
Proof.
    intros.
    inv H.
    inv INVARIANT.
    inv MATCH_LOCAL.
    destruct lc_tgt as (tview_tgt, prm_tgt) eqn:EqLcTgt.
    destruct lc_src as (tview_src, prm_src) eqn:EqLcSrc.

    eapply SI_intro; simpls; eauto.
    3: {
    destruct H0. unfolds Mem_at_eq.
    intros. rewrite H0. unfolds Mem_approxEq_loc. tauto.
    }
    {
    
    intros.
    destruct H0.
    destruct PREEMPT.
    {
        unfolds eq_ident_mapping.
        destruct H3.
        destruct H4 as (PREEMPT & EQ_INJ).
        unfold eq_inj in EQ_INJ.
        rewrite EQ_INJ in H1.
        eapply H5 in H1.
        rewrite <- H1.
        rewrite <- TVIEW_EQ.
        trivial.
    }
    {

        unfolds eq_ident_mapping.
        destruct H3.
        unfold incr_inj in H4.
        apply H4 in H1.
        eapply H5 in H1.
        rewrite <- H1.
        rewrite <- TVIEW_EQ.
        trivial.
    }
    }
    {

        ∃ (@DelaySet.dset_init nat).
        splits.
        eapply DelaySet.init_dset_subset.
        rewrite PROMISES_EQ.
        eapply rel_promises_intro; eauto.
        {
        intros.
        pose proof (DelaySet.dset_gempty nat loc t).
        rewrite H2 in H1. discriminate.
        }
        {
        intros.
        ∃ t f val R; eauto. splits; eauto.
        destruct H0.
        rewrite PROMISES_EQ in INJ_PROMISES.
        unfolds mem_injected.
        eapply INJ_PROMISES in H1. destruct H1.

        unfolds eq_ident_mapping. destruct H2.
        destruct PREEMPT as [(B&EQ_INJ) | (B&INCR_INJ)].
        { unfolds eq_inj.
            pose proof H1.
            apply EQ_INJ in H1.
            apply H3 in H1.
            rewrite <- H1 in H4; trivial.
        }
        { unfolds incr_inj.
            pose proof H1.
            apply INCR_INJ in H1.
            apply H3 in H1.
            rewrite <- H1 in H4; trivial.
        }
        }
    {
        intros.
        ∃ t'.
        splits.
        2: { right. repeat eexists; eauto. }
        destruct H0.

        rewrite PROMISES_EQ in INJ_PROMISES.
        unfolds mem_injected.
        eapply INJ_PROMISES in H1. destruct H1.
        unfolds eq_ident_mapping. destruct H2.
        destruct PREEMPT as [(B&EQ_INJ) | (B&INCR_INJ)].
        { unfolds eq_inj.
        pose proof H1.
        apply EQ_INJ in H1.
        apply H3 in H1.
        rewrite <- H1 in H4; trivial.
        }
        { unfolds incr_inj.
        pose proof H1.
        apply INCR_INJ in H1.
        apply H3 in H1.
        rewrite <- H1 in H4; trivial.
        }
    }
    }
Qed.

Theorem cse_match_state_implies_abort_preserving:
  ∀ inj lo e_tgt e_src b,
  (cse_match_state inj lo e_tgt e_src b ∧ Thread.is_abort e_tgt lo)
  → Thread.is_abort e_src lo.
Proof.
  intros.
  destruct H as (MatchState, AbortTgt).
  destruct e_tgt as (st_tgt, lc_tgt, sc_tgt, mem_tgt) eqn:EqETgt.
  destruct e_src as (st_src, lc_src, sc_src, mem_src) eqn:EqESrc.
  unfolds Thread.is_abort.
  destruct AbortTgt as (CsstTgt & AbortTgt).
  destruct AbortTgt as [StuckTgt | [RWOrdNotMatch | UpdOrdNotMatch]];
  destruct lc_tgt as (tview_tgt, prm_tgt) eqn:EqLcTgt;
  destruct lc_src as (tview_src, prm_src) eqn:EqLcSrc;
  assert (LcEq: lc_tgt = lc_src).
  {
    inv MatchState.
    inv MATCH_LOCAL.
    inv MATCH_RTL_STATE;
    simpls;
    rewrite <- TVIEW_EQ;
    rewrite <- PROMISES_EQ;
    trivial.
  }
  -

    splits; eauto; simpls.
    {
      rewrite <- EqLcSrc.
      rewrite <- LcEq.
      rewrite <- EqLcTgt in CsstTgt.
      trivial.
    }
    left.

    eapply not_or_and in StuckTgt.
    destruct StuckTgt as (NotStepTgt, NotDoneTgt).
    eapply and_not_or.
    destruct st_tgt as (regs_tgt, blk_tgt, cdhp_tgt, cont_tgt, code_tgt).
    destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src).
    splits.
    {

      inv MatchState.
      inv MATCH_LOCAL.
      inv MATCH_RTL_STATE.

      simpls.
      inversion MATCH_FRAME.
      simpls.
      intro.
      apply NotStepTgt.
      destruct H as (e & st_src' & STEP).
      destruct st_src' as (regs_src', blk_src', cdhp_src', cont_src', code_src') eqn:EqStSrcMid.
      inversion STEP.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (ProgramEvent.silent) {|
                State.regs := regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          eapply State.step_skip; eauto.
          rewrite B_TGT.
          unfolds transform_inst.
          rewrite TRSF_INST.
          trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (ProgramEvent.silent) {|
                State.regs := RegFun.add r (RegFile.eval_expr e0 regs_src) regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          eapply transform_assign_rhs_eval_eq in TRSF_INST; eauto.
          destruct TRSF_INST as (e' & I' & EQEVAL).
          eapply State.step_assign with (r:=r) (e:= e'); eauto.
          rewrite I' in B_TGT; trivial.
          rewrite EQEVAL; rewrite REG_EQ. trivial.
       -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×

          unfolds transform_inst.
          pose proof (classic (or = Ordering.plain)).
          destruct H0.
          2: {
            destruct or; try contradiction; eauto;
            ∃ (e) {|
              State.regs := RegFun.add r v regs_tgt;
              State.blk := b_tgt';
              State.cdhp := cdhp_tgt;
              State.cont := cont_tgt;
              State.code := code_tgt
            |};
            rewrite <- H;
            eapply State.step_load with (r:=r); eauto;
            rewrite <- TRSF_INST in B_TGT; trivial.
          }
          destruct or; try contradiction; try discriminate; eauto.
          remember (AveLat.GetRegByLoc loc (AveAI.getFirst analysis_blk)) as cse.
          destruct cse eqn:EqCse; try discriminate; eauto.
          2: {

              ∃ (e) {|
              State.regs := RegFun.add r v regs_tgt;
              State.blk := b_tgt';
              State.cdhp := cdhp_tgt;
              State.cont := cont_tgt;
              State.code := code_tgt
            |}.
            rewrite <- H.
            eapply State.step_load with (r:=r); eauto.
            rewrite <- TRSF_INST in B_TGT; trivial.
          }
          

          rename t into reg'.
          ∃ (ProgramEvent.silent) {|
               
                State.regs := RegFun.add r (RegFile.eval_expr (Inst.expr_reg reg') regs_tgt) regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.

          eapply State.step_assign with (r:=r) (e:= (Inst.expr_reg reg')); eauto.
          rewrite <- TRSF_INST in B_TGT; trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (e) {|
                State.regs := regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          rewrite <- H.
          eapply State.step_store with(e:=e0); eauto.
          rewrite B_TGT.
          unfolds transform_inst.
          rewrite TRSF_INST.
          trivial.
          rewrite REG_EQ.
          rewrite <- H in STEP. inversion STEP. trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
          ×
            ∃ (e) {|
                  State.regs := regs_tgt;
                  State.blk := b_tgt';
                  State.cdhp := cdhp_tgt;
                  State.cont := cont_tgt;
                  State.code := code_tgt
                |}.
            rewrite <- H.
          eapply State.step_out with(e:=e0); eauto.
          rewrite B_TGT.
          unfolds transform_inst.
          rewrite TRSF_INST.
          trivial.
          rewrite REG_EQ.
          rewrite <- H in STEP. inversion STEP. trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
          ×
            ∃ (e) {|
                  State.regs := RegFun.add r Integers.Int.one regs_tgt;
                  State.blk := b_tgt';
                  State.cdhp := cdhp_tgt;
                  State.cont := cont_tgt;
                  State.code := code_tgt
                |}.
            rewrite <- H.
          eapply State.step_cas_same with (r:=r) (er:=er) (ew:=ew); eauto.
          rewrite B_TGT.
          unfolds transform_inst.
          rewrite TRSF_INST.
          trivial.
          rewrite REG_EQ. trivial.
          rewrite REG_EQ. trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
          ×
            ∃ (e) {|
                  State.regs := RegFun.add r Integers.Int.zero regs_tgt;
                  State.blk := b_tgt';
                  State.cdhp := cdhp_tgt;
                  State.cont := cont_tgt;
                  State.code := code_tgt
                |}.
            rewrite <- H.
          eapply State.step_cas_flip with (r:=r) (er:=er) (ew:=ew); eauto.
          rewrite B_TGT.
          unfolds transform_inst.
          rewrite TRSF_INST.
          trivial.
          rewrite REG_EQ.
          rewrite VALR.
          trivial.
      -

        rewrite BLK0 in TRANSF_BLK.
        unfold transform_blk in TRANSF_BLK.
        assert (blk_tgt = BBlock.call f fret). {
          destruct blk_tgt; destruct analysis_blk; try discriminate; eauto.
        }
        rewrite <- H10 in FIND_FUNC.
        eapply cse_wf_transform_blk in OPT; eauto.
        destruct OPT as (cdhp_tgt' & blk_tgt' & TgtCdhp & TgtBlk).
        eapply eq_sym in TRANSL_CDHP.
        eapply cse_wf_transform_cdhp in TRANSL_CDHP; eauto.
        destruct TRANSL_CDHP as (b'' & TCDHP).
        ∃ e {|
                  State.regs := RegFile.init;
                  State.blk := blk_tgt';
                  State.cdhp := cdhp_tgt';
                  State.cont := Continuation.stack regs_tgt b'' cdhp_tgt cont_tgt;
                  State.code := code_tgt
                |}.
        rewrite <- H.
        eapply State.step_call; eauto.
      -

        ∃ e.
        inversion MATCH_CONT.
        × destruct DONE.
          rewrite BLK0 in STEP.
          rewrite H11 in STEP.
          inversion STEP; try discriminate; eauto.
        ×
          ∃ {|
            State.regs := regs_t;
            State.blk := blk_t;
            State.cdhp := cdhp_t;
            State.cont := cont_tgt';
            State.code := code_tgt
          |}.
        rewrite <- H.
        eapply State.step_ret; eauto.
        unfold transform_blk in TRANSF_BLK.
        rewrite BLK0 in TRANSF_BLK.
        destruct analysis_blk; try discriminate; eauto.
      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (e) {|
                State.regs := regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          rewrite <- H.
        eapply State.step_fence_rel; eauto.
        rewrite B_TGT.
        unfolds transform_inst.
        rewrite TRSF_INST.
        trivial.

      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (e) {|
                State.regs := regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          rewrite <- H.
        eapply State.step_fence_acq; eauto.
        rewrite B_TGT.
        unfolds transform_inst.
        rewrite TRSF_INST.
        trivial.

      -

        rewrite BLK0 in TRANSF_BLK.
        eapply transform_blk_induction in TRANSF_BLK; eauto.
        destruct TRANSF_BLK as (i' & b_tgt' & B_TGT & TRSF).
        destruct TRSF as (TRSF_INST & TRSF_BLK).
        ×
          ∃ (e) {|
                State.regs := regs_tgt;
                State.blk := b_tgt';
                State.cdhp := cdhp_tgt;
                State.cont := cont_tgt;
                State.code := code_tgt
              |}.
          rewrite <- H.
        eapply State.step_fence_sc; eauto.
        rewrite B_TGT.
        unfolds transform_inst.
        rewrite TRSF_INST.
        trivial.
      -

         ∃ e.
         eapply eq_sym in TRANSL_CDHP.
         rewrite <- H8 in TGT.
         eapply cse_wf_transform_cdhp with (f:=f) in TRANSL_CDHP; eauto.
         destruct TRANSL_CDHP as (b_tgt' & TCDHP).
         rewrite <- H.
         ∃ {|
          State.regs := regs_tgt;
          State.blk := b_tgt';
          State.cdhp := cdhp_tgt;
          State.cont := cont_tgt;
          State.code := code_tgt
          |}.
          eapply State.step_jmp; eauto.
          unfold transform_blk in TRANSF_BLK.
          rewrite BLK0 in TRANSF_BLK.
          destruct analysis_blk; try discriminate; eauto.
      -

        ∃ e.
        destruct BRANCH as [(CdhpSrc & Cond) | (CdhpSrc & Cond)].
        ×
        eapply eq_sym in TRANSL_CDHP.
        rewrite <- H8 in CdhpSrc.
        eapply cse_wf_transform_cdhp with (f:=f1) in TRANSL_CDHP; eauto.
        destruct TRANSL_CDHP as (b_tgt' & TCDHP).
        rewrite <- H.
        ∃ {|
          State.regs := regs_tgt;
          State.blk := b_tgt';
          State.cdhp := cdhp_tgt;
          State.cont := cont_tgt;
          State.code := code_tgt
          |}.
        eapply State.step_be; eauto.
        unfold transform_blk in TRANSF_BLK.
        rewrite BLK0 in TRANSF_BLK.
        destruct analysis_blk; try discriminate; eauto.
        left. splits; eauto.
        rewrite REG_EQ; rewrite H6; rewrite <- COND in Cond; eauto.
        ×
          eapply eq_sym in TRANSL_CDHP.
          rewrite <- H8 in CdhpSrc.
          eapply cse_wf_transform_cdhp with (f:=f2) in TRANSL_CDHP; eauto.
          destruct TRANSL_CDHP as (b_tgt' & TCDHP).
          rewrite <- H.
          ∃ {|
            State.regs := regs_tgt;
            State.blk := b_tgt';
            State.cdhp := cdhp_tgt;
            State.cont := cont_tgt;
            State.code := code_tgt
            |}.
          eapply State.step_be; eauto.
          unfold transform_blk in TRANSF_BLK.
          rewrite BLK0 in TRANSF_BLK.
          destruct analysis_blk; try discriminate; eauto.
          right. splits; eauto.
          rewrite REG_EQ; rewrite H6; rewrite <- COND in Cond; eauto.
    }
    {

      inv MatchState.
      inv MATCH_LOCAL.
      inv MATCH_RTL_STATE.

      simpls.
      inversion MATCH_FRAME.
      simpls.
      intro.
      apply NotDoneTgt.
      unfolds State.is_terminal; simpls.
      inv MATCH_CONT.
      destruct DONE; trivial. subst.
      destruct H. subst.
      simpl. destruct (AveAI.br_from_i analysis !! l i); eauto.
      destruct H. discriminate.
    }
  -

    {

      inv MatchState.
      inv MATCH_LOCAL.
      inv MATCH_RTL_STATE;
      simpls;
      rewrite <- TVIEW_EQ;
      rewrite <- PROMISES_EQ;
      trivial.
    }
    -
    splits; eauto; simpls.
    {
      rewrite <- EqLcSrc.
      rewrite <- LcEq.
      rewrite <- EqLcTgt in CsstTgt.
      trivial.
    }
    inv MatchState.
    inv MATCH_LOCAL.
    inv MATCH_RTL_STATE.

    simpls.
    inversion MATCH_FRAME.
    simpls.
    right.
    trivial. left.
    destruct RWOrdNotMatch as (st_tgt' & x & o & v & RW & NOT_MATCH).
    destruct RW.
      × inversion H.
         {
          destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src) eqn:EqStSrc.
          rewrite <- H0 in REG_EQ.
          simpls.
          rewrite <- H0 in TRANSF_BLK; simpls. rewrite BLK0 in TRANSF_BLK.
          pose proof TRANSF_BLK.
          eapply load_transformed_by_load in H5.
          destruct H5 as (b'' & H').
          eexists.
          ∃ x o v.
          splits; eauto.
          left.
          eapply State.step_load; eauto.
         }
         {
          destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src) eqn:EqStSrc.
          rewrite <- H0 in REG_EQ.
          simpls.
          rewrite <- H0 in TRANSF_BLK; simpls. rewrite BLK0 in TRANSF_BLK.
          pose proof TRANSF_BLK.
          eapply cas_transformed_by_cas in H5.
          destruct H5 as (b'' & H').
          eexists.
          ∃ x o v.
          splits; eauto.
          left.
          eapply State.step_cas_flip with (er:= er); eauto.
          {
            rewrite REG_EQ in VALR. rewrite VALR.
            unfold Integers.Int.cmp. trivial.
          }
         }
      × inversion H.
        destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src) eqn:EqStSrc.
        rewrite <- H0 in REG_EQ.
        simpls.
        rewrite REG_EQ in VAL.
        rewrite <- H0 in TRANSF_BLK; simpls. rewrite BLK0 in TRANSF_BLK.
        pose proof TRANSF_BLK.
        eapply store_transformed_by_store in H5.
        destruct H5 as (b'' & H').
        eexists.
        ∃ x o v.
        splits; eauto.
        right.
        eapply State.step_store with (e:=e); eauto.
  -

    {

      inv MatchState.
      inv MATCH_LOCAL.
      inv MATCH_RTL_STATE;
      simpls;
      rewrite <- TVIEW_EQ;
      rewrite <- PROMISES_EQ;
      trivial.
    }
    -
    splits; eauto; simpls.
    {
      rewrite <- EqLcSrc.
      rewrite <- LcEq.
      rewrite <- EqLcTgt in CsstTgt.
      trivial.
    }
    inv MatchState.
    inv MATCH_LOCAL.
    inv MATCH_RTL_STATE.

    simpls.
    inversion MATCH_FRAME.
    simpls.
    right; right.
    destruct UpdOrdNotMatch as (st_tgt' & x & vr & vw & or & ow & UPD & NOT_MATCH).
    inversion UPD.
    destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src) eqn:EqStSrc.
    rewrite <- H5 in REG_EQ.
    simpls.
    rewrite <- H5 in TRANSF_BLK; simpls. rewrite BLK0 in TRANSF_BLK.
    pose proof TRANSF_BLK.
    eapply cas_transformed_by_cas in H.
    destruct H as (b'' & H).
    eexists.
    ∃ x vr vw or ow.
    splits; eauto.
    eapply State.step_cas_same with (er:= er); eauto.
    {
      rewrite REG_EQ in VALR. rewrite VALR.
      unfold Integers.Int.cmp. trivial.
    }
    {
      rewrite REG_EQ in VALW. rewrite VALW.
      unfold Integers.Int.cmp. trivial.
    }
Qed.

Theorem cse_match_state_preserving_na_silent:
  ∀ te lo inj st_tgt st_src sc_tgt lc_src lc_tgt mem_tgt sc_src mem_src b st_tgt' lc_tgt' sc_tgt' mem_tgt',
    Thread.program_step te lo
        (@Thread.mk rtl_lang st_tgt lc_tgt sc_tgt mem_tgt)
        (@Thread.mk rtl_lang st_tgt' lc_tgt' sc_tgt' mem_tgt')
    →
    ThreadEvent.silent = te
    →
    (cse_match_state inj lo
      (Thread.mk rtl_lang st_tgt lc_tgt sc_tgt mem_tgt)
      (Thread.mk rtl_lang st_src lc_src sc_src mem_src) b)
    →
      (∃ st_src' lc_src' sc_src' mem_src' te,
          (te = ThreadEvent.silent ∨ ThreadEvent.is_na_read te)
          ∧
          Thread.program_step te lo (@Thread.mk rtl_lang st_src lc_src sc_src mem_src)
                                    (@Thread.mk rtl_lang st_src' lc_src' sc_src' mem_src')
          ∧
          (cse_match_state inj lo
          (Thread.mk rtl_lang st_tgt' lc_tgt' sc_tgt' mem_tgt') (Thread.mk rtl_lang st_src' lc_src' sc_src' mem_src') false)
      ).
Proof.
  intros.
  destruct st_tgt as (regs_tgt, blk_tgt, cdhp_tgt, cont_tgt, code_tgt).
  destruct st_tgt' as (regs_tgt', blk_tgt', cdhp_tgt', cont_tgt', code_tgt').
  destruct st_src as (regs_src, blk_src, cdhp_src, cont_src, code_src); simpls.
  inv H1.
  pose proof MATCH_LOCAL as MATCH_LOCAL'.
  inv MATCH_LOCAL.
  inv MATCH_RTL_STATE; simpls.
  inv MATCH_FRAME; simpls.
  inv H; simpls.
  inversion STATE; simpls; subst.

  -
    remember (transform_cdhp cdhp_src analysis) as cdhp_tgt.
    remember (transform_blk blk_src (AveAI.br_from_i analysis !! l i)) as blk_tgt.
    eapply eq_sym in Heqblk_tgt.
    rewrite BLK0 in Heqblk_tgt.
    eapply transform_blk_induction' in Heqblk_tgt; eauto.
    destruct Heqblk_tgt as (inst & b_src' & EqBlkSrc & TRSF).
    destruct TRSF as (TRSF_INST & TRSF_BLK).
    ×
      ∃ {|
          State.regs := regs_tgt';
          State.blk := b_src';
          State.cdhp := cdhp_src;
          State.cont := cont_src;
          State.code := code_src
        |} lc_src sc_src mem_src (ThreadEvent.silent).
      splits; eauto.
      {

          eapply Thread.program_step_intro; simpls; eauto.
          eapply State.step_skip; eauto.
          eapply skip_transformed_inst_by_skip in TRSF_INST.
          rewrite <- TRSF_INST; trivial.
      }
      {

        inversion LOCAL.
        eapply cse_match_state_intro with(inj':=inj'); simpls; eauto.
        {

          rewrite <- H5. rewrite <- H4. trivial.
        }
        {
            eapply cse_match_local_state_intro;
            try rewrite <- H3; eauto.
            eapply cse_match_rtl_state_intro; eauto.
            simpls.
            eapply cse_match_frame_intro with(i:=i+1); eauto.
            rewrite EqBlkSrc in PARTIAL_BLK.
            eapply bb_from_i_plus_one; eauto.
            rewrite AveAI.get_tail_from_i_eq_i_plus_one in TRSF_BLK; eauto.
            {
              destruct ANALYSIS.
              2: {

                pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top).
                eapply H7 in H.
                folds AveAI.b.
                rewrite H.
                eapply always_match_top.
              }
              eapply Ave_B.wf_transf_blk_step in H; eauto.
              unfolds Ave_B.transf_step.
              rewrite EqBlkSrc in H.
              eapply skip_transformed_inst_by_skip in TRSF_INST.
              rewrite TRSF_INST in H.
              unfolds Ave_I.transf.
              rewrite <- H.
              trivial.
            }
            {
              eapply subblk_same_succ in EqBlkSrc.
              rewrite <- EqBlkSrc; trivial.
              destruct ANALYSIS.
              2: {
                intros.
                eapply (AveAI.get_head_from_eval) with (l:=lp) in H; eauto.
                folds AveAI.b.
                rewrite H.
                eapply AveLat.ge_top.
              }
              eapply Ave_B.wf_transf_blk_getlast in H; eauto.
              rewrite <- H. trivial.
            }
            {
              destruct ANALYSIS as [ANALYSIS | ANALYSIS].
              eapply transf_step_psrv_loc_fact_valid; eauto.
              eapply Ave_B.wf_transf_blk_step; eauto.
              pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top) as A.
              apply A in ANALYSIS.
              folds AveAI.b.
              rewrite ANALYSIS.
              eapply top_is_loc_fact_valid.
            }
        }
        {
          right.
          splits; trivial.
          destruct PREEMPT as [(_&EQ_INJ) | (_&INCR_INJ)].
          apply eq_inj_implies_incr; trivial.
          trivial.
        }
        {
          rewrite <- H3; rewrite <- H5.
          trivial.
        }
        {
          rewrite <- H4; rewrite <- H5.
          trivial.
        }
        {
          rewrite <- H5.
          trivial.
        }
      }
  -

    remember (transform_cdhp cdhp_src analysis) as cdhp_tgt.
    remember (transform_blk blk_src (AveAI.br_from_i analysis !! l i)) as blk_tgt.
    eapply eq_sym in Heqblk_tgt.
    rewrite BLK0 in Heqblk_tgt.
    eapply transform_blk_induction' in Heqblk_tgt; eauto.
    destruct Heqblk_tgt as (inst & b_src' & EqBlkSrc & TRSF).
    destruct TRSF as (TRSF_INST & TRSF_BLK).
    ×
      eapply assign_transformed_inst_by_assign_or_na_load in TRSF_INST.
      destruct TRSF_INST as [ASSIGN|[(loc & r' & LOAD & GET_REG & E) | (expr & r' & ASSIGN & GET_REG & E)]].
      {

        ∃ {|
            State.regs := RegFun.add r (RegFile.eval_expr e regs_src) regs_src;
            State.blk := b_src';
            State.cdhp := cdhp_src;
            State.cont := cont_src;
            State.code := code_src
          |} lc_src sc_src mem_src (ThreadEvent.silent).
        splits; eauto.
        {

            eapply Thread.program_step_intro; simpls.
            eapply State.step_assign; eauto.
            rewrite <- ASSIGN; trivial.
            eapply Local.step_silent; eauto.
        }
        {

          inversion LOCAL.
          eapply cse_match_state_intro with(inj':=inj'); simpls; eauto.
          {

            rewrite <- H5. rewrite <- H4. trivial.
          }
          {
            eapply cse_match_local_state_intro;
            try rewrite <- H3; eauto.
            eapply cse_match_rtl_state_intro; eauto.
            simpls.
            eapply cse_match_frame_intro with(i:=i+1); eauto.
            rewrite EqBlkSrc in PARTIAL_BLK.
            eapply bb_from_i_plus_one; eauto.
            rewrite AveAI.get_tail_from_i_eq_i_plus_one in TRSF_BLK; eauto.
            {
              destruct ANALYSIS.
              2: {

                pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top).
                eapply H7 in H.
                folds AveAI.b.
                rewrite H.
                eapply always_match_top.
              }
              eapply Ave_B.wf_transf_blk_step in H; eauto.
              unfolds Ave_B.transf_step.
              rewrite EqBlkSrc in H.
              rewrite ASSIGN in H.
              pose proof MATCH_AI as MATCH_AI'.
              unfold match_abstract_interp in MATCH_AI.
              unfold match_abstract_interp.
              remember (AveAI.getFirst (AveAI.br_from_i analysis !! l i)) as ai.
              remember (AveAI.getFirst (AveAI.br_from_i analysis !! l (i + 1))) as ai'.
              unfold Ave_I.transf in H.
              remember (AveLat.opt_expr_with_ave e (AveLat.kill_reg ai r)) as opt_e.
              remember (AveLat.GetRegByExpr opt_e (AveLat.kill_reg ai r)) as GetReg.
              destruct GetReg eqn:EqGetReg.
              {
                destruct ai eqn:EqAi.
                {
                  unfold AveLat.kill_reg in H. rewrite <- H. trivial.
                }
                {
                  unfold AveLat.kill_reg in H. rewrite <- H.
                  intros.
                  rename t into r'.
                  simpls. discriminate.
                }
                {
                  unfold AveLat.kill_reg in H. rewrite <- H.
                  intros.
                  rename t into r'.
                  des_ifH H.
                  2: {
                    intros.
                    assert (W.In tu tuples). {
                      eapply W.filter_1 in H7; trivial.
                      eapply AveTuple.compat_bool_freeOfReg.
                    }
                    specialize (MATCH_AI tu H8).

                    unfolds match_abstract_fact.
                    destruct tu eqn:EqTu.
                    {

                      assert (r ≠ reg). {
                        destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                        {
                          subst. discriminate.
                        }
                        {
                          subst. discriminate.
                        }
                        {
                          inv H.
                          eapply W.filter_2 in H7.
                          unfolds AveTuple.freeOfReg.
                          eapply sflib__andb_split in H7.
                          destruct H7.
                          unfolds negb.
                          destruct (reg =? r)%positive eqn:RegEq.
                          try discriminate; eauto.
                          rewrite Pos.eqb_sym in RegEq.
                          eapply Pos.eqb_neq; eauto.
                          eapply AveTuple.compat_bool_freeOfReg.
                        }
                      }

                      inv H.

                      pose proof H9.
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                      folds Const.t.
                      rewrite H9.
                      assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        intro.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        des_ifH H1; try discriminate; eauto.
                        rewrite H0 in H2. discriminate.
                        eapply (AveTuple.compat_bool_freeOfReg r).
                      }
                      eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr e regs_src)) in H0.
                        folds Const.t.
                        rewrite <- H0.
                        trivial.
                    }
                    {

                      assert (r ≠ reg). {
                        destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                        {
                          subst. discriminate.
                        }
                        {
                          subst. discriminate.
                        }
                        {
                          inv H.
                          eapply W.filter_2 in H7.
                          unfolds AveTuple.freeOfReg.
                          unfolds negb.
                          destruct (reg =? r)%positive eqn:RegEq.
                          try discriminate; eauto.
                          rewrite Pos.eqb_sym in RegEq.
                          eapply Pos.eqb_neq; eauto.
                          eapply AveTuple.compat_bool_freeOfReg.
                        }
                      }
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                      folds Const.t.
                      rewrite H9.
                      trivial.
                    }
                  }
                  intros.
                  pose proof (classic (tu = AveTuple.AExpr r' (Inst.expr_reg r))) as IS_R_R'.
                  destruct IS_R_R' as [IS_R_R' | NOT_R_R'].
                  {

                    rewrite IS_R_R'.
                    unfolds match_abstract_fact.
                      unfolds AveLat.GetRegByExpr.
                      pose proof Heqai'.
                      remember (RegFile.eval_expr e regs_src) as val.
                      unfold RegFile.eval_expr. rewrite RegFun.add_spec_eq.
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn: KillReg; try discriminate.
                      remember (W.choose (W.filter (AveTuple.isSameExpr opt_e) tuples0)) as Choose.
                      destruct Choose eqn:EqChoose; try discriminate.
                      inversion H2.
                      eapply eq_sym in HeqChoose.
                      eapply W.choose_1 in HeqChoose.
                      pose proof HeqChoose.
                      eapply W.filter_1 in HeqChoose.
                      eapply W.filter_2 in H10.
                      unfold AveTuple.isSameExpr in H10.
                      destruct e0 eqn:EqE; try discriminate.
                      eapply Inst.beq_expr_eq in H10.
                      unfolds AveTuple.get_reg.
                      inversion HeqGetReg.
                      subst reg.
                      assert (r' ≠ r). {
                        eapply AveLat.mem_of_kill_reg_implies_neq with (tuples:=tuples) (r:=r)in KillReg; eauto.
                        unfolds AveTuple.get_reg. trivial.
                      }
                      subst val.
                      inv STATE; try discriminate.
                      rewrite Loc_add_neq; eauto.
                      assert (regs_src r' = RegFile.eval_expr e regs_src). {
                        clear - MATCH_AI' MATCH_AI HeqChoose KillReg.
                        remember ((AveLat.opt_expr_with_ave e (AveLat.CSet tuples0))) as opt_e.
                        remember (AveTuple.AExpr r' opt_e) as tu.
                        unfolds AveLat.kill_reg. inversion KillReg.
                        rewrite <- H0 in HeqChoose.
                        eapply W.filter_1 in HeqChoose.
                        specialize (MATCH_AI tu HeqChoose).
                        rewrite Heqtu in MATCH_AI.
                        rewrite MATCH_AI.
                        eapply eq_sym.
                        subst opt_e.
                        eapply match_ai_implies_opt_expr_eval_eq; eauto.
                        eapply ge_prsv_match_ai; eauto.
                        {
                          unfold AveAI.ge.
                          unfold AveDS.L.ge.
                          unfold W.Subset.
                          intros.
                          rewrite <- H0 in H.
                          eapply W.filter_1 in H; eauto.
                          eapply AveTuple.compat_bool_freeOfReg.
                        }
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                      trivial.
                      eapply AveTuple.compat_bool_isSameExpr.
                      eapply AveTuple.compat_bool_isSameExpr.
                  }
                  

                  assert (W.In tu tuples). {
                    eapply W.add_3 in H7.
                    eapply W.filter_1 in H7; trivial.
                    eapply AveTuple.compat_bool_freeOfReg.
                    intro. rewrite H8 in NOT_R_R'. contradiction.
                  }
                  specialize (MATCH_AI tu H8).
                  unfolds match_abstract_fact.
                  destruct tu eqn:EqTu.
                  {

                    assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inv H.
                        eapply W.add_3 in H7.
                        2: {
                          intro.
                          rewrite H in NOT_R_R'.
                          contradiction.
                        }
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        destruct (reg =? r)%positive eqn:RegEq.
                        try discriminate; eauto.
                        rewrite Pos.eqb_sym in RegEq.
                        eapply Pos.eqb_neq; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                    }

                    inv H.
                    eapply W.add_3 in H7; eauto.
                    pose proof H9.
                    eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                    folds Const.t.
                    rewrite H9.
                    assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                      eapply W.filter_2 in H7.
                      unfolds AveTuple.freeOfReg.
                      intro.
                      eapply sflib__andb_split in H7.
                      destruct H7.
                      unfolds negb.
                      des_ifH H1; try discriminate; eauto.
                      rewrite H0 in H2. discriminate.
                      eapply (AveTuple.compat_bool_freeOfReg r).
                    }
                    eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr e regs_src)) in H0.
                      folds Const.t.
                      rewrite <- H0.
                      trivial.
                  }
                  {

                    assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inv H.
                        eapply W.add_3 in H7.
                        2: {
                          intro.
                          rewrite H in NOT_R_R'.
                          contradiction.
                        }
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        unfolds negb.
                        destruct (reg =? r)%positive eqn:RegEq.
                        try discriminate; eauto.
                        rewrite Pos.eqb_sym in RegEq.
                        eapply Pos.eqb_neq; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                    }
                    eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                    folds Const.t.
                    rewrite H9.
                    trivial.
                  }
                }
              }
              {
                destruct ai eqn:EqAi.
                {
                  unfold AveLat.kill_reg in H. rewrite <- H. trivial.
                }
                {
                  unfold AveLat.kill_reg in H. rewrite <- H.
                  intros.
                  destruct (negb (RegSet.mem r (Inst.regs_of_expr opt_e))) eqn:MEM.
                  2: {
                    contradiction.
                  }
                  intros.

                  pose proof classic (tu = (AveTuple.AExpr r opt_e)).
                  destruct H8.
                  2: {
                    eapply W.add_3 in H7.
                    2: {
                      intro.
                      rewrite H9 in H8; contradiction.
                    }
                    pose proof W.empty_1. unfolds W.Empty.
                    specialize (H9 tu).
                    contradiction.
                  }
                  rewrite H8.
                  unfold match_abstract_fact.
                  rewrite Loc_add_eq.
                  subst opt_e.
                  unfolds AveLat.kill_reg.
                  assert (RegFile.eval_expr (AveLat.opt_expr_with_ave e AveLat.Undef)
                  (RegFun.add r (RegFile.eval_expr e regs_src) regs_src) = RegFile.eval_expr (AveLat.opt_expr_with_ave e AveLat.Undef) regs_src). {
                    eapply eq_sym.
                    eapply regs_add_nonfree_var_eq_eval_expr.
                    intro.
                    rewrite H9 in MEM.
                    unfolds negb.
                    discriminate.
                  }
                  rewrite H9.
                  eapply match_ai_implies_opt_expr_eval_eq; eauto.
                }
                {
                  remember (AveLat.kill_reg (AveLat.CSet tuples) r ) as Kill.
                  destruct Kill; try discriminate; eauto.
                  destruct (negb (RegSet.mem r (Inst.regs_of_expr opt_e))) eqn:MEM.
                  2: {
                    rewrite <- H.
                    intros.
                    assert (W.In tu tuples). {
                      unfold AveLat.kill_reg in HeqKill.
                      inv HeqKill.
                      eapply W.filter_1 in H7; subst; trivial.
                      eapply AveTuple.compat_bool_freeOfReg.
                    }
                    specialize (MATCH_AI tu H8).
                    unfolds match_abstract_fact.
                    destruct tu eqn:EqTu.
                    {

                      assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inversion HeqKill.
                        rewrite H10 in H7.
                        unfold AveLat.kill_reg in EqKillReg.
                        inversion EqKillReg.
                        rewrite <- H11 in H7.
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        destruct (reg =? r)%positive eqn:RegEq.
                        try discriminate; eauto.
                        rewrite Pos.eqb_sym in RegEq.
                        eapply Pos.eqb_neq; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                      }
                      inversion HeqKill.
                      rewrite H11 in H7.

                      pose proof H9.
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                      folds Const.t.
                      rewrite H9.
                      assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                        eapply W.filter_2 in H7.
                        unfold AveTuple.freeOfReg in H7.
                        intro.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        des_ifH H13; try discriminate; eauto.
                        eapply (AveTuple.compat_bool_freeOfReg r).
                      }
                      eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr e regs_src)) in H12.
                      folds Const.t.
                      rewrite <- H12.
                      trivial.
                    }
                    {

                      assert (r ≠ reg). {
                        destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                        {
                          subst. discriminate.
                        }
                        {
                          subst. discriminate.
                        }
                        {
                          inversion HeqKill.
                          rewrite H10 in H7.
                          unfold AveLat.kill_reg in EqKillReg.
                          inversion EqKillReg.
                          rewrite <- H11 in H7.
                          eapply W.filter_2 in H7.
                          unfolds AveTuple.freeOfReg.
                          unfolds negb.
                          destruct (reg =? r)%positive eqn:RegEq.
                          try discriminate; eauto.
                          rewrite Pos.eqb_sym in RegEq.
                          eapply Pos.eqb_neq; eauto.
                          eapply AveTuple.compat_bool_freeOfReg.
                        }
                      }
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H9.
                      folds Const.t.
                      rewrite H9.
                      trivial.
                    }
                  }
                  rewrite <- H.
                  intros.
                  unfolds match_abstract_fact.
                  destruct tu eqn:EqTu.
                  {

                    pose proof (classic (tu = AveTuple.AExpr r opt_e)).
                    destruct H8.
                    {

                      rewrite EqTu in H8.
                      inversion H8. subst expr. subst reg.
                      rewrite Loc_add_eq.
                      subst opt_e.
                      unfolds AveLat.kill_reg.
                      assert (RegFile.eval_expr (AveLat.opt_expr_with_ave e (AveLat.CSet tuples0))
                      (RegFun.add r (RegFile.eval_expr e regs_src) regs_src) = RegFile.eval_expr (AveLat.opt_expr_with_ave e (AveLat.CSet tuples0)) regs_src). {
                        eapply eq_sym.
                        eapply regs_add_nonfree_var_eq_eval_expr.
                        intro.
                        rewrite H9 in MEM.
                        unfolds negb.
                        discriminate.
                      }
                      rewrite H9.
                      eapply match_ai_implies_opt_expr_eval_eq; eauto.
                      eapply ge_prsv_match_ai; eauto.
                      inversion HeqKill.
                      {
                        unfold AveAI.ge.
                        unfold AveDS.L.ge.
                        unfold W.Subset.
                        intros.
                        eapply W.filter_1 in H10; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                    }
                    {

                      eapply W.add_3 in H7; eauto.
                      2: {subst; eauto. }
                      clear H8.
                      assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inversion HeqKill.
                        rewrite H9 in H7.
                        unfold AveLat.kill_reg in EqKillReg.
                        inversion EqKillReg.
                        rewrite <- H10 in H7.
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        destruct (reg =? r)%positive eqn:RegEq.
                        try discriminate; eauto.
                        rewrite Pos.eqb_sym in RegEq.
                        eapply Pos.eqb_neq; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                      }
                      inversion HeqKill.
                      rewrite H10 in H7.

                      pose proof H8.
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H8.
                      folds Const.t.
                      rewrite H8.
                      assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                        eapply W.filter_2 in H7.
                        unfold AveTuple.freeOfReg in H7.
                        intro.
                        eapply sflib__andb_split in H7.
                        destruct H7.
                        unfolds negb.
                        des_ifH H12; try discriminate; eauto.
                        eapply (AveTuple.compat_bool_freeOfReg r).
                      }
                      eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr e regs_src)) in H11.
                      folds Const.t.
                      rewrite <- H11.
                      trivial.
                      assert (W.In tu tuples). {
                        eapply W.filter_1 in H7; subst; trivial.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                      specialize (MATCH_AI tu H12).
                      rewrite EqTu in MATCH_AI. trivial.
                    }
                  }
                  {

                    assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inversion HeqKill.
                        rewrite H9 in H7.
                        unfold AveLat.kill_reg in EqKillReg.
                        inversion EqKillReg.
                        rewrite <- H10 in H7.
                        eapply W.add_3 in H7.
                        2: {intro. discriminate. }
                        eapply W.filter_2 in H7.
                        unfolds AveTuple.freeOfReg.
                        unfolds negb.
                        destruct (reg =? r)%positive eqn:RegEq.
                        try discriminate; eauto.
                        rewrite Pos.eqb_sym in RegEq.
                        eapply Pos.eqb_neq; eauto.
                        eapply AveTuple.compat_bool_freeOfReg.
                      }
                    }
                    eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr e regs_src)) (regs:=regs_src) in H8.
                    folds Const.t.
                    rewrite H8.
                    assert (W.In tu tuples). {
                      eapply W.add_3 in H7.
                      inv HeqKill.
                      eapply W.filter_1 in H7; subst; trivial.
                      eapply AveTuple.compat_bool_freeOfReg.
                      intro; discriminate.
                    }
                    specialize (MATCH_AI tu H9). subst; trivial.
                  }
                }
              }
            }
            {
              eapply subblk_same_succ in EqBlkSrc.
              rewrite <- EqBlkSrc; trivial.
              destruct ANALYSIS.
              2: {
                intros.
                eapply (AveAI.get_head_from_eval) with (l:=lp) in H; eauto.
                folds AveAI.b.
                rewrite H.
                eapply AveLat.ge_top.
              }
              eapply Ave_B.wf_transf_blk_getlast in H; eauto.
              rewrite <- H. trivial.
            }
            {
              destruct ANALYSIS as [ANALYSIS | ANALYSIS].
              eapply transf_step_psrv_loc_fact_valid; eauto.
              eapply Ave_B.wf_transf_blk_step; eauto.
              pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top) as A.
              apply A in ANALYSIS.
              folds AveAI.b.
              rewrite ANALYSIS.
              eapply top_is_loc_fact_valid.
            }
        }
          {
            right.
            splits; trivial.
            destruct PREEMPT as [(_&EQ_INJ) | (_&INCR_INJ)].
            apply eq_inj_implies_incr; trivial.
            trivial.
          }
          {
            rewrite <- H3; rewrite <- H5.
            trivial.
          }
          {
            rewrite <- H4; rewrite <- H5.
            trivial.
          }
          {
            rewrite <- H5.
            trivial.
          }
        }
      }
      {

      assert (loc_fact_valid (AveAI.getFirst (AveAI.br_from_i analysis !! l (i + 1)))). {
        {
          destruct ANALYSIS as [ANALYSIS | ANALYSIS].
          eapply transf_step_psrv_loc_fact_valid; eauto.
          eapply Ave_B.wf_transf_blk_step; eauto.
          pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top) as A.
          apply A in ANALYSIS.
          folds AveAI.b.
          rewrite ANALYSIS.
          eapply top_is_loc_fact_valid.
        }
      }
      rename H into LOC_FACT_VALID.
        ∃ {|
            State.regs := RegFun.add r (RegFile.eval_expr e regs_src) regs_src;
            State.blk := b_src';
            State.cdhp := cdhp_src;
            State.cont := cont_src;
            State.code := code_src
          |} lc_src sc_src mem_src.

        remember ((AveAI.getFirst (AveAI.br_from_i analysis !! l i))) as ai.
        pose proof GET_REG as GET_REG'.
        unfold AveLat.GetRegByLoc in GET_REG.
        destruct ai eqn:EqAi; try discriminate; eauto.
        remember (W.choose (W.filter (AveTuple.isSameLoc loc) tuples)) as ai_tmp.
        destruct ai_tmp eqn:EqAiTmp; try discriminate; eauto.
        rename e0 into tu.
        eapply eq_sym in Heqai_tmp.
        eapply W.choose_1 in Heqai_tmp.
        pose proof Heqai_tmp as TU.
        eapply W.filter_1 in Heqai_tmp.
        eapply W.filter_2 in TU.
        unfold AveTuple.isSameLoc in TU.
        destruct tu eqn:EqTu; try discriminate; eauto.
        pose proof (MATCH_AI tu).
        rewrite <- EqTu in Heqai_tmp.
        apply H in Heqai_tmp.
        clear H.
        unfolds match_abstract_fact. rewrite EqTu in Heqai_tmp.
        destruct Heqai_tmp as (NON_ATOMIC & t & f & R & PLN & RLX & MSG).
        eapply Pos.eqb_eq in TU.
        rewrite <- TU in MSG.
        2: {eapply AveTuple.compat_bool_isSameLoc. }
        2: {eapply AveTuple.compat_bool_isSameLoc. }
        pose proof MSG as MSG'.
        assert (regs_src reg = regs_src r'). {
          inv GET_REG. trivial. }
        rename H into REG_R'.

        assert (∃ te, te = ThreadEvent.read loc t (RegFile.eval_expr e regs_src) R Ordering.plain). {
          eexists; eauto.
        }
        destruct H as (te & TE).
        ∃ te.
        splits; eauto.
        {
          right. unfold ThreadEvent.is_na_read. rewrite TE. trivial.
        }
        {

            eapply Thread.program_step_intro; simpls.
            unfold ThreadEvent.get_program_event.
            rewrite TE.
            eapply State.step_load; eauto.
            rewrite <- LOAD; trivial.
            rewrite TE.
            eapply Local.step_read; eauto.

            eapply Local.read_step_intro with (from:=f); eauto.
            {
              rewrite MSG.
              rewrite E.
              unfold RegFile.eval_expr.
              assert (regs_src reg = regs_src r'). {
                inv GET_REG. trivial. }
              rewrite H.
              trivial.
            }
            {
              subst.
              unfold Ordering.mem_ord_match.
              rewrite NON_ATOMIC. trivial.
            }
            {
              econs; subst; eauto.
              replace (Ordering.le Ordering.relaxed Ordering.plain) with false; trivial.
              unfold is_true.
              intro. discriminate.
            }
            {
              assert (lc_src = lc_tgt). {eapply cse_match_local_state_implies_eq_local; eauto. }
              pose proof TU as TU'.
              subst. destruct lc_tgt eqn:EqLcTgt; simpls.
              unfold TView.read_tview.
              replace (Ordering.le Ordering.relaxed Ordering.plain) with false; trivial.
              replace (Ordering.le Ordering.acqrel Ordering.plain) with false; trivial.
              unfold View.singleton_ur_if.
              unfold View.singleton_rw.
              unfold View.join; unfold View.bot; simpls.
              repeat rewrite TimeMap.join_bot.
              destruct tview eqn:EqTview; simpls; eauto.
              destruct cur eqn:EqCur; simpls; eauto.
              destruct acq eqn:EqAcq; simpls; eauto.
              assert (TimeMap.join rlx (TimeMap.singleton loc0 t) = rlx). {
                eapply TimeMap.le_join_l; eauto.
                unfold TimeMap.singleton.
                unfold TimeMap.le. intro.
                pose proof (classic (loc = loc0)).
                destruct H.
                rewrite H. rewrite Loc_add_eq; eauto.
                rewrite Loc_add_neq; eauto.
                unfold LocFun.init.
                eapply Time.bot_spec.
              }
              assert (TimeMap.join rlx0 (TimeMap.singleton loc0 t) = rlx0). {
                inv LOCAL_WF.
                inv TVIEW_WF.
                simpls.
                inv CUR_ACQ. simpls.
                eapply TimeMap.le_join_l.
                assert (TimeMap.le (TimeMap.singleton loc0 t) rlx). {
                  unfold TimeMap.singleton.
                  unfold TimeMap.le. intro.
                  pose proof (classic (loc = loc0)).
                  destruct H0.
                  rewrite H0. rewrite Loc_add_eq; eauto.
                  rewrite Loc_add_neq; eauto.
                  unfold LocFun.init.
                  eapply Time.bot_spec.
                }
                unfolds TimeMap.le.
                intros.
                specialize (RLX0 loc).
                specialize (H0 loc).
                auto_solve_time_rel.
              }
              rewrite H.
              rewrite H0.
              trivial.
            }
        }
        {

          inversion LOCAL.
          eapply cse_match_state_intro with(inj':=inj'); simpls; eauto.
          {

            rewrite <- H5. rewrite <- H4. trivial.
          }
          {
              eapply cse_match_local_state_intro;
              try rewrite <- H3; eauto.
              eapply cse_match_rtl_state_intro; eauto.
              simpls.
              eapply cse_match_frame_intro with(i:=i+1); eauto.
              rewrite EqBlkSrc in PARTIAL_BLK.
              eapply bb_from_i_plus_one; eauto.
              rewrite AveAI.get_tail_from_i_eq_i_plus_one in TRSF_BLK; eauto.
              {

                destruct ANALYSIS.
                2: {

                pose proof (AveAI.get_first_from_eval analysis l (i+1) AveLat.top).
                eapply H7 in H.
                folds AveAI.b.
                rewrite H.
                eapply always_match_top.
              }
              eapply Ave_B.wf_transf_blk_step in H; eauto.
              unfolds Ave_B.transf_step.
              rewrite EqBlkSrc in H.
              rewrite LOAD in H.
              unfolds Ave_I.transf.
                rewrite <- H.
                subst.
                unfolds match_abstract_interp.
                rename loc0 into loc.
                remember (AveAI.getFirst (AveAI.br_from_i analysis !! l i)) as ai.
                remember (AveLat.GetRegByLoc loc (AveLat.kill_reg ai r)) as ai'.
                destruct ai eqn:EqAi.
                {
                  discriminate.
                }
                { discriminate.
                }
                remember (AveAI.getFirst (AveAI.br_from_i analysis !! l (i + 1))) as ai''.
                destruct ai'' eqn:EqAi''.
                {subst. rewrite H.
                  destruct (AveLat.kill_reg (AveLat.CSet tuples0) r ) eqn:Eq1;
                  destruct (AveLat.GetRegByLoc loc (AveLat.kill_reg (AveLat.CSet tuples) r)) eqn:Eq2; try discriminate; eauto.
                }
                {subst. rewrite H.
                  destruct (AveLat.kill_reg (AveLat.CSet tuples0) r ) eqn:Eq1;
                  destruct (AveLat.GetRegByLoc loc (AveLat.kill_reg (AveLat.CSet tuples) r)) eqn:Eq2; try discriminate; eauto.
                }
                rewrite H.
                intros.
                unfolds match_abstract_fact.
                destruct tu eqn:EqTu.
                {

                  destruct ai' eqn:EqAi'.
                  {
                    rename t0 into reg'.
                    pose proof (classic (tu = AveTuple.AExpr reg' (Inst.expr_reg r))).
                    destruct H1.
                    {

                      assert (r' = reg'). {
                        assert (W.In (AveTuple.AVar r' loc) tuples). {
                          clear - GET_REG'.
                          remember (W.choose (W.filter (AveTuple.isSameLoc loc) tuples)) as Choose.
                          destruct Choose eqn:EqChoose; try discriminate.
                          eapply eq_sym in HeqChoose.
                          eapply W.choose_1 in HeqChoose.
                          pose proof HeqChoose.
                          eapply W.filter_1 in HeqChoose.
                          eapply W.filter_2 in H.
                          unfolds AveTuple.isSameLoc.
                          destruct e eqn:EqE; try discriminate.
                          eapply Pos.eqb_eq in H. subst loc0.
                          unfolds AveTuple.get_reg. inv GET_REG'. trivial.
                          eapply AveTuple.compat_bool_isSameLoc.
                          eapply AveTuple.compat_bool_isSameLoc.
                        }
                        assert (W.In (AveTuple.AVar reg' loc) tuples). {
                          inv Heqai.
                          clear - Heqai'.
                          unfolds AveLat.GetRegByLoc.
                          remember (AveLat.kill_reg (AveLat.CSet tuples0) r) as KillReg.
                          destruct KillReg; try discriminate; eauto.
                          remember (W.choose (W.filter (AveTuple.isSameLoc loc) tuples)) as Choose.
                          destruct Choose; try discriminate.
                          inv Heqai'.
                          eapply eq_sym in HeqChoose.
                          eapply W.choose_1 in HeqChoose.
                          pose proof HeqChoose.
                          eapply W.filter_1 in HeqChoose.
                          eapply W.filter_2 in H.
                          unfolds AveTuple.isSameLoc.
                          destruct e eqn:EqE; try discriminate.
                          eapply Pos.eqb_eq in H. subst loc0.
                          unfolds AveTuple.get_reg.
                          unfolds AveLat.kill_reg.
                          inv HeqKillReg.
                          eapply W.filter_1 in HeqChoose. trivial.
                          eapply AveTuple.compat_bool_freeOfReg.
                          eapply AveTuple.compat_bool_isSameLoc.
                          eapply AveTuple.compat_bool_isSameLoc.
                        }
                        specialize (LOC_FACT r' reg' loc H2 H3). trivial.
                      }
                      rename H2 into CHOOSE_EQ.
                      rewrite H1 in EqTu.
                      inversion EqTu.
                      rewrite <- H3.
                      unfolds transform_inst.
                      unfolds AveLat.GetRegByLoc.
                      pose proof Heqai'.
                      remember (RegFile.eval_expr (Inst.expr_reg r') regs_src) as val.
                      unfold RegFile.eval_expr. rewrite RegFun.add_spec_eq.
                      destruct (AveLat.kill_reg (AveLat.CSet tuples0) r) eqn: KillReg; try discriminate.
                      remember (W.choose (W.filter (AveTuple.isSameLoc loc) tuples2)) as Choose.
                      destruct Choose eqn:EqChoose; try discriminate.
                      inversion H2.
                      eapply eq_sym in HeqChoose.
                      eapply W.choose_1 in HeqChoose.
                      pose proof HeqChoose.
                      eapply W.filter_1 in HeqChoose.
                      eapply W.filter_2 in H5.
                      unfold AveTuple.isSameLoc in H5.
                      destruct e eqn:EqE; try discriminate.
                      eapply Pos.eqb_eq in H5.
                      unfolds AveTuple.get_reg.
                      subst reg'. subst reg0.
                      assert (reg1 ≠ r). {
                        eapply AveLat.mem_of_kill_reg_implies_neq with (tuples:=tuples0) (r:=r)in KillReg; eauto.
                        unfolds AveTuple.get_reg. trivial.
                      }
                      inv STATE; try discriminate.
                      rewrite Loc_add_neq; eauto.
                      eapply AveTuple.compat_bool_isSameLoc.
                      eapply AveTuple.compat_bool_isSameLoc.
                    }
                    {
                      

                      inv GET_REG.
                      rename reg0 into reg.
                      assert (r ≠ reg). {
                        destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                        {
                          subst. discriminate.
                        }
                        {
                          subst. discriminate.
                        }
                        {
                          inv H.
                          eapply W.add_3 in H0.
                          2: {
                            intro.
                            inversion H. simpls. try contradiction.
                            rewrite <- H in H1.
                            simpls. subst.
                            try contradiction.
                          }
                          remember (AveLat.kill_reg (AveLat.CSet tuples) r) as _ai.
                          remember (AveTuple.AExpr reg expr) as tu.
                          eapply W.filter_2 in H0.
                          unfold AveTuple.freeOfReg in H0. subst tu.
                          eapply sflib__andb_split in H0.
                          destruct H0.
                          unfolds negb.
                          destruct (reg =? r)%positive eqn:RegEq.
                          try discriminate; eauto.
                          rewrite Pos.eqb_sym in RegEq.
                          eapply Pos.eqb_neq; eauto.
                          eapply AveTuple.compat_bool_freeOfReg.
                        }
                      }
                      inv H.
                      eapply W.add_3 in H0; eauto.
                      pose proof H0.
                      eapply W.filter_1 in H0.
                      inv Heqai.
                      pose proof (MATCH_AI (AveTuple.AExpr reg expr)).
                      apply H3 in H0.
                      pose proof H2.
                      eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr (Inst.expr_reg r') regs_src)) (regs:=regs_src) in H2.
                      folds Const.t.
                      rewrite H2.
                      assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                        eapply W.filter_2 in H.
                        unfolds AveTuple.freeOfReg.
                        intro.
                        eapply sflib__andb_split in H.
                        destruct H.
                        unfolds negb.
                        des_ifH H; try discriminate; eauto.
                        rewrite H5 in H6. discriminate.
                        eapply (AveTuple.compat_bool_freeOfReg r).
                      }
                      eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr (Inst.expr_reg r') regs_src)) in H5.
                      folds Const.t.
                      rewrite <- H5.
                      trivial.
                      eapply (AveTuple.compat_bool_freeOfReg r).
                    }
                  }
                  {
                    inv GET_REG.
                    inv Heqai.
                    rename reg0 into reg.
                    rename tuples0 into tuples.
                    assert (r ≠ reg). {
                      destruct (AveLat.kill_reg (AveLat.CSet tuples) r) eqn:EqKillReg.
                      {
                        subst. discriminate.
                      }
                      {
                        subst. discriminate.
                      }
                      {
                        inv H.
                        eapply W.add_3 in H0.
                        2: {
                          intro. try discriminate.
                        }
                        remember (AveLat.kill_reg (AveLat.CSet tuples) r) as _ai.
                        remember (AveTuple.AExpr reg expr) as tu.
                        eapply AveLat.mem_of_kill_reg_implies_neq with (tuples':=tuples0) (tuples:=tuples) (r:=r) in H0; eauto.
                        unfolds AveTuple.get_reg. rewrite Heqtu in H0.
                        intro. rewrite H in H0. contradiction.
                      }
                    }
                    inv H.
                    eapply W.add_3 in H0; eauto.
                    2: {
                      intro. discriminate.
                    }
                    pose proof H0.
                    eapply W.filter_1 in H0.
                    pose proof (MATCH_AI (AveTuple.AExpr reg expr)).
                    apply H2 in H0.
                    pose proof H1.
                    eapply regs_add_neg with (r:=r) (v:=(RegFile.eval_expr (Inst.expr_reg r') regs_src)) (regs:=regs_src) in H1.
                    folds Const.t.
                    rewrite H1.
                    assert (¬RegSet.mem r (Inst.regs_of_expr expr)). {
                      eapply W.filter_2 in H.
                      unfolds AveTuple.freeOfReg.
                      intro.
                      eapply sflib__andb_split in H.
                      destruct H.
                      unfolds negb.
                      des_ifH H; try discriminate; eauto.
                      rewrite H4 in H5. discriminate.
                      eapply (AveTuple.compat_bool_freeOfReg r).
                    }
                    eapply regs_add_nonfree_var_eq_eval_expr with (regs:=regs_src) (val:=(RegFile.eval_expr (Inst.expr_reg r') regs_src)) in H4.
                    folds Const.t.
                    rewrite <- H4.
                    trivial.
                    eapply (AveTuple.compat_bool_freeOfReg r).
                  }
                }
                {