Uncomment many more proofs

1 files changed, 751 insertions, 0 deletions

diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index d95c422..c0ba39f 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -30,6 +30,757 @@ Require Import vericert.hls.RTLBlock.
 Require Import vericert.hls.RTLPar.
 Require Import vericert.hls.RTLBlockInstr.
 Require Import vericert.hls.RTLPargen.
+Require Import vericert.hls.Predicate.
+Require Import vericert.hls.Abstr.
+
+#[local] Open Scope positive.
+#[local] Open Scope forest.
+#[local] Open Scope pred_op.
+
+(*|
+Abstract computations
+=====================
+|*)
+
+(*Definition is_regs i := match i with mk_instr_state rs _ => rs end.
+Definition is_mem i := match i with mk_instr_state _ m => m end.
+
+Inductive state_lessdef : instr_state -> instr_state -> Prop :=
+  state_lessdef_intro :
+    forall rs1 rs2 m1,
+    (forall x, rs1 !! x = rs2 !! x) ->
+    state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1).
+
+(*|
+RTLBlock to abstract translation
+--------------------------------
+
+Correctness of translation from RTLBlock to the abstract interpretation language.
+|*)
+
+Ltac inv_simp :=
+  repeat match goal with
+  | H: exists _, _ |- _ => inv H
+  end; simplify.
+
+*)
+
+Definition check_dest i r' :=
+  match i with
+  | RBop p op rl r => (r =? r')%positive
+  | RBload p chunk addr rl r => (r =? r')%positive
+  | _ => false
+  end.
+
+Lemma check_dest_dec i r : {check_dest i r = true} + {check_dest i r = false}.
+Proof. destruct (check_dest i r); tauto. Qed.
+
+Fixpoint check_dest_l l r :=
+  match l with
+  | nil => false
+  | a :: b => check_dest a r || check_dest_l b r
+  end.
+
+Lemma check_dest_l_forall :
+  forall l r,
+  check_dest_l l r = false ->
+  Forall (fun x => check_dest x r = false) l.
+Proof. induction l; crush. Qed.
+
+Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}.
+Proof. destruct (check_dest_l i r); tauto. Qed.
+
+Lemma check_dest_update :
+  forall f i r,
+  check_dest i r = false ->
+  (update f i) # (Reg r) = f # (Reg r).
+Proof.
+  destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush.
+Qed.
+
+Lemma check_dest_l_forall2 :
+  forall l r,
+  Forall (fun x => check_dest x r = false) l ->
+  check_dest_l l r = false.
+Proof.
+  induction l; crush.
+  inv H. apply orb_false_intro; crush.
+Qed.
+
+Lemma check_dest_l_ex2 :
+  forall l r,
+  (exists a, In a l /\ check_dest a r = true) ->
+  check_dest_l l r = true.
+Proof.
+  induction l; crush.
+  specialize (IHl r). inv H.
+  apply orb_true_intro; crush.
+  apply orb_true_intro; crush.
+  right. apply IHl. exists x. auto.
+Qed.
+
+Lemma check_list_l_false :
+  forall l x r,
+  check_dest_l (l ++ x :: nil) r = false ->
+  check_dest_l l r = false /\ check_dest x r = false.
+Proof.
+  simplify.
+  apply check_dest_l_forall in H. apply Forall_app in H.
+  simplify. apply check_dest_l_forall2; auto.
+  apply check_dest_l_forall in H. apply Forall_app in H.
+  simplify. inv H1. auto.
+Qed.
+
+Lemma check_dest_l_ex :
+  forall l r,
+  check_dest_l l r = true ->
+  exists a, In a l /\ check_dest a r = true.
+Proof.
+  induction l; crush.
+  destruct (check_dest a r) eqn:?; try solve [econstructor; crush].
+  simplify.
+  exploit IHl. apply H. simplify. econstructor. simplify. right. eassumption.
+  auto.
+Qed.
+
+Lemma check_list_l_true :
+  forall l x r,
+  check_dest_l (l ++ x :: nil) r = true ->
+  check_dest_l l r = true \/ check_dest x r = true.
+Proof.
+  simplify.
+  apply check_dest_l_ex in H; simplify.
+  apply in_app_or in H. inv H. left.
+  apply check_dest_l_ex2. exists x0. auto.
+  inv H0; auto.
+Qed.
+
+Lemma check_dest_l_dec2 l r :
+  {Forall (fun x => check_dest x r = false) l}
+  + {exists a, In a l /\ check_dest a r = true}.
+Proof.
+  destruct (check_dest_l_dec l r); [right | left];
+  auto using check_dest_l_ex, check_dest_l_forall.
+Qed.
+
+Lemma abstr_comp :
+  forall l i f x x0,
+  abstract_sequence f (l ++ i :: nil) = x ->
+  abstract_sequence f l = x0 ->
+  x = update x0 i.
+Proof. induction l; intros; crush; eapply IHl; eauto. Qed.
+
+(*
+
+Lemma gen_list_base:
+  forall FF ge sp l rs exps st1,
+  (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) ->
+  sem_val_list ge sp st1 (list_translation l exps) rs ## l.
+Proof.
+  induction l.
+  intros. simpl. constructor.
+  intros. simpl. eapply Scons; eauto.
+Qed.
+
+Lemma check_dest_update2 :
+  forall f r rl op p,
+  (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem).
+Proof. crush; rewrite map2; auto. Qed.
+
+Lemma check_dest_update3 :
+  forall f r rl p addr chunk,
+  (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem).
+Proof. crush; rewrite map2; auto. Qed.
+
+Lemma abstract_seq_correct_aux:
+  forall FF ge sp i st1 st2 st3 f,
+    @step_instr FF ge sp st3 i st2 ->
+    sem ge sp st1 f st3 ->
+    sem ge sp st1 (update f i) st2.
+Proof.
+  intros; inv H; simplify.
+  { simplify; eauto. } (*apply match_states_refl. }*)
+  { inv H0. inv H6. destruct st1. econstructor. simplify.
+    constructor. intros.
+    destruct (resource_eq (Reg res) (Reg x)). inv e.
+    rewrite map2. econstructor. eassumption. apply gen_list_base; eauto.
+    rewrite Regmap.gss. eauto.
+    assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. }
+    rewrite Regmap.gso by auto.
+    rewrite genmap1 by auto. auto.
+
+    rewrite genmap1; crush. }
+  { inv H0. inv H7. constructor. constructor. intros.
+    destruct (Pos.eq_dec dst x); subst.
+    rewrite map2. econstructor; eauto.
+    apply gen_list_base. auto. rewrite Regmap.gss. auto.
+    rewrite genmap1. rewrite Regmap.gso by auto. auto.
+    unfold not in *; intros. inv H0. auto.
+    rewrite genmap1; crush.
+  }
+  { inv H0. inv H7. constructor. constructor; intros.
+    rewrite genmap1; crush.
+    rewrite map2. econstructor; eauto.
+    apply gen_list_base; auto.
+  }
+Qed.
+
+Lemma regmap_list_equiv :
+  forall A (rs1: Regmap.t A) rs2,
+    (forall x, rs1 !! x = rs2 !! x) ->
+    forall rl, rs1##rl = rs2##rl.
+Proof. induction rl; crush. Qed.
+
+Lemma sem_update_Op :
+  forall A ge sp st f st' r l o0 o m rs v,
+  @sem A ge sp st f st' ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  match_states st' (mk_instr_state rs m) ->
+  exists tst,
+  sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst.
+Proof.
+  intros. inv H1. simplify.
+  destruct st.
+  econstructor. simplify.
+  { constructor.
+    { constructor. intros. destruct (Pos.eq_dec x r); subst.
+      { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto.
+        { inv H9. eapply gen_list_base; eauto. }
+        { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } }
+      { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } }
+    { inv H. rewrite genmap1; crush. eauto. } }
+  { constructor; eauto. intros.
+    destruct (Pos.eq_dec r x);
+    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
+Qed.
+
+Lemma sem_update_load :
+  forall A ge sp st f st' r o m a l m0 rs v a0,
+  @sem A ge sp st f st' ->
+  Op.eval_addressing ge sp a rs ## l = Some a0 ->
+  Mem.loadv m m0 a0 = Some v ->
+  match_states st' (mk_instr_state rs m0) ->
+  exists tst : instr_state,
+    sem ge sp st (update f (RBload o m a l r)) tst
+    /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst.
+Proof.
+  intros. inv H2. pose proof H. inv H. inv H9.
+  destruct st.
+  econstructor; simplify.
+  { constructor.
+    { constructor. intros.
+      destruct (Pos.eq_dec x r); subst.
+      { rewrite map2. econstructor; eauto. eapply gen_list_base. intros.
+        rewrite <- H6. eauto.
+        instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. }
+      { rewrite Regmap.gso by auto. rewrite genmap1; crush. } }
+    { rewrite genmap1; crush. eauto. } }
+  { constructor; auto; intros. destruct (Pos.eq_dec r x);
+    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
+Qed.
+
+Lemma sem_update_store :
+  forall A ge sp a0 m a l r o f st m' rs m0 st',
+  @sem A ge sp st f st' ->
+  Op.eval_addressing ge sp a rs ## l = Some a0 ->
+  Mem.storev m m0 a0 rs !! r = Some m' ->
+  match_states st' (mk_instr_state rs m0) ->
+  exists tst, sem ge sp st (update f (RBstore o m a l r)) tst
+              /\ match_states (mk_instr_state rs m') tst.
+Proof.
+  intros. inv H2. pose proof H. inv H. inv H9.
+  destruct st.
+  econstructor; simplify.
+  { econstructor.
+    { econstructor; intros. rewrite genmap1; crush. }
+    { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6.
+      eauto. specialize (H6 r). rewrite H6. eauto. } }
+  { econstructor; eauto. }
+Qed.
+
+Lemma sem_update :
+  forall A ge sp st x st' st'' st''' f,
+  sem ge sp st f st' ->
+  match_states st' st''' ->
+  @step_instr A ge sp st''' x st'' ->
+  exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst.
+Proof.
+  intros. destruct x; inv H1.
+  { econstructor. split.
+    apply sem_update_RBnop. eassumption.
+    apply match_states_commut. auto. }
+  { eapply sem_update_Op; eauto. }
+  { eapply sem_update_load; eauto. }
+  { eapply sem_update_store; eauto. }
+Qed.
+
+Lemma sem_update2_Op :
+  forall A ge sp st f r l o0 o m rs v,
+  @sem A ge sp st f (mk_instr_state rs m) ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m).
+Proof.
+  intros. destruct st. constructor.
+  inv H. inv H6.
+  { constructor; intros. simplify.
+    destruct (Pos.eq_dec r x); subst.
+    { rewrite map2. econstructor. eauto.
+      apply gen_list_base. eauto.
+      rewrite Regmap.gss. auto. }
+    { rewrite genmap1; crush. rewrite Regmap.gso; auto.  } }
+  { simplify. rewrite genmap1; crush. inv H. eauto. }
+Qed.
+
+Lemma sem_update2_load :
+  forall A ge sp st f r o m a l m0 rs v a0,
+    @sem A ge sp st f (mk_instr_state rs m0) ->
+    Op.eval_addressing ge sp a rs ## l = Some a0 ->
+    Mem.loadv m m0 a0 = Some v ->
+    sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0).
+Proof.
+  intros. simplify. inv H. inv H7. constructor.
+  { constructor; intros. destruct (Pos.eq_dec r x); subst.
+    { rewrite map2. rewrite Regmap.gss. econstructor; eauto.
+      apply gen_list_base; eauto. }
+    { rewrite genmap1; crush. rewrite Regmap.gso; eauto. }
+  }
+  { simplify. rewrite genmap1; crush. }
+Qed.
+
+Lemma sem_update2_store :
+  forall A ge sp a0 m a l r o f st m' rs m0,
+    @sem A ge sp st f (mk_instr_state rs m0) ->
+    Op.eval_addressing ge sp a rs ## l = Some a0 ->
+    Mem.storev m m0 a0 rs !! r = Some m' ->
+    sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m').
+Proof.
+  intros. simplify. inv H. inv H7. constructor; simplify.
+  { econstructor; intros. rewrite genmap1; crush. }
+  { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. }
+Qed.
+
+Lemma sem_update2 :
+  forall A ge sp st x st' st'' f,
+  sem ge sp st f st' ->
+  @step_instr A ge sp st' x st'' ->
+  sem ge sp st (update f x) st''.
+Proof.
+  intros.
+  destruct x; inv H0;
+  eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store.
+Qed.
+
+Lemma abstr_sem_val_mem :
+  forall A B ge tge st tst sp a,
+    ge_preserved ge tge ->
+    forall v m,
+    (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\
+    (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v).
+Proof.
+  intros * H.
+  apply expression_ind2 with
+
+    (P := fun (e1: expression) =>
+    forall v m,
+    (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\
+    (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v))
+
+    (P0 := fun (e1: expression_list) =>
+    forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv);
+  simplify; intros; simplify.
+  { inv H1. inv H2. constructor. }
+  { inv H2. inv H1. rewrite H0. constructor. }
+  { inv H3. }
+  { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto.
+    apply H0; simplify; eauto. constructor; eauto.
+    unfold ge_preserved in *. simplify. rewrite <- H2. auto.
+  }
+  { inv H3. }
+  { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto.
+    apply H0; simplify; eauto. constructor; eauto.
+    inv H. rewrite <- H4. eauto.
+    auto.
+  }
+  { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto.
+    apply H2; eauto. simplify; eauto. constructor; eauto.
+    apply H1; eauto. simplify; eauto. constructor; eauto.
+    inv H. rewrite <- H5. eauto. auto.
+  }
+  { inv H4. }
+  { inv H1. constructor. }
+  { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. }
+Qed.
+
+Lemma abstr_sem_value :
+  forall a A B ge tge sp st tst v,
+    @sem_value A ge sp st a v ->
+    ge_preserved ge tge ->
+    match_states st tst ->
+    @sem_value B tge sp tst a v.
+Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed.
+
+Lemma abstr_sem_mem :
+  forall a A B ge tge sp st tst v,
+    @sem_mem A ge sp st a v ->
+    ge_preserved ge tge ->
+    match_states st tst ->
+    @sem_mem B tge sp tst a v.
+Proof. intros; eapply abstr_sem_val_mem; eauto. Qed.
+
+Lemma abstr_sem_regset :
+  forall a a' A B ge tge sp st tst rs,
+    @sem_regset A ge sp st a rs ->
+    ge_preserved ge tge ->
+    (forall x, a # x = a' # x) ->
+    match_states st tst ->
+    exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x).
+Proof.
+  inversion 1; intros.
+  inv H7.
+  econstructor. simplify. econstructor. intros.
+  eapply abstr_sem_value; eauto. rewrite <- H6.
+  eapply H0. constructor; eauto.
+  auto.
+Qed.
+
+Lemma abstr_sem :
+  forall a a' A B ge tge sp st tst st',
+    @sem A ge sp st a st' ->
+    ge_preserved ge tge ->
+    (forall x, a # x = a' # x) ->
+    match_states st tst ->
+    exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
+Proof.
+  inversion 1; subst; intros.
+  inversion H4; subst.
+  exploit abstr_sem_regset; eauto; inv_simp.
+  do 3 econstructor; eauto.
+  rewrite <- H3.
+  eapply abstr_sem_mem; eauto.
+Qed.
+
+Lemma abstract_execution_correct':
+  forall A B ge tge sp st' a a' st tst,
+  @sem A ge sp st a st' ->
+  ge_preserved ge tge ->
+  check a a' = true ->
+  match_states st tst ->
+  exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'.
+Proof.
+  intros;
+  pose proof (check_correct a a' H1);
+  eapply abstr_sem; eauto.
+Qed.
+
+Lemma states_match :
+  forall st1 st2 st3 st4,
+  match_states st1 st2 ->
+  match_states st2 st3 ->
+  match_states st3 st4 ->
+  match_states st1 st4.
+Proof.
+  intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4.
+  inv H1. inv H2. inv H3; constructor.
+  unfold regs_lessdef in *. intros.
+  repeat match goal with
+         | H: forall _, _, r : positive |- _ => specialize (H r)
+         end.
+  congruence.
+  auto.
+Qed.
+
+Lemma step_instr_block_same :
+  forall ge sp st st',
+  step_instr_block ge sp st nil st' ->
+  st = st'.
+Proof. inversion 1; auto. Qed.
+
+Lemma step_instr_seq_same :
+  forall ge sp st st',
+  step_instr_seq ge sp st nil st' ->
+  st = st'.
+Proof. inversion 1; auto. Qed.
+
+Lemma sem_update' :
+  forall A ge sp st a x st',
+  sem ge sp st (update (abstract_sequence empty a) x) st' ->
+  exists st'',
+  @step_instr A ge sp st'' x st' /\
+  sem ge sp st (abstract_sequence empty a) st''.
+Proof.
+  Admitted.
+
+Lemma rtlpar_trans_correct :
+  forall bb ge sp sem_st' sem_st st,
+  sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' ->
+  match_states sem_st st ->
+  exists st', RTLPar.step_instr_block ge sp st bb st'
+              /\ match_states sem_st' st'.
+Proof.
+  induction bb using rev_ind.
+  { repeat econstructor. eapply abstract_interp_empty3 in H.
+    inv H. inv H0. constructor; congruence. }
+  { simplify. inv H0. repeat rewrite concat_app in H. simplify.
+    rewrite app_nil_r in H.
+    exploit sem_separate; eauto; inv_simp.
+    repeat econstructor. admit. admit.
+  }
+Admitted.
+
+(*Lemma abstract_execution_correct_ld:
+  forall bb bb' cfi ge tge sp st st' tst,
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    ge_preserved ge tge ->
+    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true ->
+    match_states_ld st tst ->
+    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
+                 /\ match_states st' tst'.
+Proof.
+  intros.*)
+*)
+
+Lemma match_states_list :
+  forall A (rs: Regmap.t A) rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall l, rs ## l = rs' ## l.
+Proof. induction l; crush. Qed.
+
+Lemma PTree_matches :
+  forall A (v: A) res rs rs',
+  (forall r, rs !! r = rs' !! r) ->
+  forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x.
+Proof.
+  intros; destruct (Pos.eq_dec x res); subst;
+  [ repeat rewrite Regmap.gss by auto
+  | repeat rewrite Regmap.gso by auto ]; auto.
+Qed.
+
+Lemma abstract_interp_empty3 :
+  forall A ctx st',
+    @sem A ctx empty st' -> match_states (ctx_is ctx) st'.
+Proof.
+  inversion 1; subst; simplify. destruct ctx.
+  destruct ctx_is.
+  constructor; intros.
+  - inv H0. specialize (H3 x). inv H3. inv H8. reflexivity.
+  - inv H1. specialize (H3 x). inv H3. inv H8. reflexivity.
+  - inv H2. inv H8. reflexivity.
+Qed.
+
+Lemma step_instr_matches :
+  forall A a ge sp st st',
+    @step_instr A ge sp st a st' ->
+    forall tst,
+      match_states st tst ->
+      exists tst', step_instr ge sp tst a tst'
+                   /\ match_states st' tst'.
+Proof.
+  induction 1; simplify;
+  match goal with H: match_states _ _ |- _ => inv H end;
+  try solve [repeat econstructor; try erewrite match_states_list;
+  try apply PTree_matches; eauto;
+  match goal with
+    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
+  end].
+  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    apply PTree_matches; assumption.
+    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    econstructor; auto.
+    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    apply PTree_matches; assumption.
+    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    econstructor; auto.
+    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+  - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+    match goal with
+    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
+    end.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
+    match goal with
+    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
+    end.
+    erewrite <- eval_predf_pr_equiv; eassumption.
+    match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
+    repeat econstructor; try erewrite match_states_list; eauto.
+    match goal with
+    H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
+    end.
+Qed.
+
+Lemma step_instr_list_matches :
+  forall a ge sp st st',
+  step_instr_list ge sp st a st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_list ge sp tst a tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction a; intros; inv H;
+  try (exploit step_instr_matches; eauto; []; simplify;
+       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
+Qed.
+
+Lemma step_instr_seq_matches :
+  forall a ge sp st st',
+  step_instr_seq ge sp st a st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_seq ge sp tst a tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction a; intros; inv H;
+  try (exploit step_instr_list_matches; eauto; []; simplify;
+       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
+Qed.
+
+Lemma step_instr_block_matches :
+  forall bb ge sp st st',
+  step_instr_block ge sp st bb st' ->
+  forall tst, match_states st tst ->
+              exists tst', step_instr_block ge sp tst bb tst'
+                           /\ match_states st' tst'.
+Proof.
+  induction bb; intros; inv H;
+  try (exploit step_instr_seq_matches; eauto; []; simplify;
+       exploit IHbb; eauto; []; simplify); repeat econstructor; eauto.
+Qed.
+
+Lemma rtlblock_trans_correct' :
+  forall bb ge sp st x st'',
+  RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' ->
+  exists st', RTLBlock.step_instr_list ge sp st bb st'
+              /\ step_instr ge sp st' x st''.
+Proof.
+  induction bb.
+  crush. exists st.
+  split. constructor. inv H. inv H6. auto.
+  crush. inv H. exploit IHbb. eassumption. simplify.
+  econstructor. split.
+  econstructor; eauto. eauto.
+Qed.
+
+Lemma abstract_interp_empty A st : @sem A st empty (ctx_is st).
+Proof. destruct st, ctx_is. simpl. repeat econstructor. Qed.
+
+Lemma abstract_seq :
+  forall l f i,
+    abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i.
+Proof. induction l; crush. Qed.
+
+Lemma abstract_sequence_update :
+  forall l r f,
+  check_dest_l l r = false ->
+  (abstract_sequence f l) # (Reg r) = f # (Reg r).
+Proof.
+  induction l using rev_ind; crush.
+  rewrite abstract_seq. rewrite check_dest_update. apply IHl.
+  apply check_list_l_false in H. tauto.
+  apply check_list_l_false in H. tauto.
+Qed.
+
+Lemma sem_separate :
+  forall A ctx b a st',
+    sem ctx (abstract_sequence empty (a ++ b)) st' ->
+    exists st'',
+         @sem A ctx (abstract_sequence empty a) st''
+      /\ @sem A (mk_ctx st'' (ctx_sp ctx) (ctx_ge ctx)) (abstract_sequence empty b) st'.
+Proof.
+  induction b using rev_ind; simplify.
+  { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. }
+  { simplify. rewrite app_assoc in H. rewrite abstract_seq in H.
+    exploit sem_update'; eauto; simplify.
+    exploit IHb; eauto; inv_simp.
+    econstructor; split; eauto.
+    rewrite abstract_seq.
+    eapply sem_update2; eauto.
+  }
+Qed.
+
+Lemma sem_update_RBnop :
+  forall A ctx f st',
+  @sem A ctx f st' -> sem ctx (update f RBnop) st'.
+Proof. auto. Qed.
+
+Lemma sem_update_Op :
+  forall A ge sp ist f st' r l o0 o m rs v,
+  @sem A (mk_ctx ist sp ge) f st' ->
+  Op.eval_operation ge sp o0 rs ## l m = Some v ->
+  match_states st' (mk_instr_state rs m ps) ->
+  exists tst,
+  sem (mk_ctx ist sp ge) (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m ps) tst.
+Proof.
+  intros. inv H1. simplify.
+  destruct st.
+  econstructor. simplify.
+  { constructor.
+    { constructor. intros. destruct (Pos.eq_dec x r); subst.
+      { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto.
+        { inv H9. eapply gen_list_base; eauto. }
+        { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } }
+      { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } }
+    { inv H. rewrite genmap1; crush. eauto. } }
+  { constructor; eauto. intros.
+    destruct (Pos.eq_dec r x);
+    subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. }
+Qed.
+
+Lemma sem_update :
+  forall A ge sp st x st' st'' st''' f,
+  sem (mk_ctx st sp ge) f st' ->
+  match_states st' st''' ->
+  @step_instr A ge sp st''' x st'' ->
+  exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst.
+Proof. Admitted.
+
+Lemma rtlblock_trans_correct :
+  forall bb ge sp st st',
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    forall tst,
+      match_states st tst ->
+      exists tst', sem (mk_ctx tst sp ge) (abstract_sequence empty bb) tst'
+                   /\ match_states st' tst'.
+Proof.
+  induction bb using rev_ind; simplify.
+  { econstructor. simplify. apply abstract_interp_empty.
+    inv H. auto. }
+  { apply rtlblock_trans_correct' in H. simplify.
+    rewrite abstract_seq.
+    exploit IHbb; try eassumption; []; simplify.
+    exploit sem_update. apply H1. symmetry; eassumption.
+    eauto. simplify. econstructor. split. apply H3.
+    auto. }
+Qed.
+
+Lemma abstract_execution_correct:
+  forall bb bb' cfi cfi' ge tge sp st st' tst,
+    RTLBlock.step_instr_list ge sp st bb st' ->
+    ge_preserved ge tge ->
+    schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi') = true ->
+    match_states st tst ->
+    exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
+                 /\ match_states st' tst'.
+Proof.
+  intros.
+  unfold schedule_oracle in *. simplify. unfold empty_trees in H4.
+  exploit rtlblock_trans_correct; try eassumption; []; simplify.
+(*)  exploit abstract_execution_correct';
+  try solve [eassumption | apply state_lessdef_match_sem; eassumption].
+  apply match_states_commut. eauto. inv_simp.
+  exploit rtlpar_trans_correct; try eassumption; []; inv_simp.
+  exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp.
+  repeat match goal with | H: match_states _ _ |- _ => inv H end.
+  do 2 econstructor; eauto.
+  econstructor; congruence.
+Qed.*)Admitted.
 
 Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
   match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.