Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling

4 files changed, 335 insertions, 170 deletions

diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index a0b7f4d..abc4181 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -366,13 +366,15 @@ Section SEMANTICS.
 Context {A : Type}.
 
 Record ctx : Type := mk_ctx {
-  ctx_rs: regset;
-  ctx_ps: predset;
-  ctx_mem: mem;
+  ctx_is: instr_state;
   ctx_sp: val;
   ctx_ge: Genv.t A unit;
 }.
 
+Definition ctx_rs ctx := is_rs (ctx_is ctx).
+Definition ctx_ps ctx := is_ps (ctx_is ctx).
+Definition ctx_mem ctx := is_mem (ctx_is ctx).
+
 Inductive sem_value : ctx -> expression -> val -> Prop :=
 | Sbase_reg:
     forall r ctx,
@@ -656,11 +658,36 @@ Lemma ge_preserved_same:
 Proof. unfold ge_preserved; auto. Qed.
 #[local] Hint Resolve ge_preserved_same : core.
 
+Inductive match_states : instr_state -> instr_state -> Prop :=
+| match_states_intro:
+  forall ps ps' rs rs' m m',
+    (forall x, rs !! x = rs' !! x) ->
+    (forall x, ps !! x = ps' !! x) ->
+    m = m' ->
+    match_states (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').
+
+Lemma match_states_refl x : match_states x x.
+Proof. destruct x; constructor; crush. Qed.
+
+Lemma match_states_commut x y : match_states x y -> match_states y x.
+Proof. inversion 1; constructor; crush. Qed.
+
+Lemma match_states_trans x y z :
+  match_states x y -> match_states y z -> match_states x z.
+Proof. repeat inversion 1; constructor; crush. Qed.
+
+#[global]
+Instance match_states_Equivalence : Equivalence match_states :=
+  { Equivalence_Reflexive := match_states_refl ;
+    Equivalence_Symmetric := match_states_commut ;
+    Equivalence_Transitive := match_states_trans ; }.
+
 Inductive similar {A B} : @ctx A -> @ctx B -> Prop :=
 | similar_intro :
-    forall rs ps mem sp ge tge,
+    forall ist ist' sp ge tge,
     ge_preserved ge tge ->
-    similar (mk_ctx rs ps mem sp ge) (mk_ctx rs ps mem sp tge).
+    match_states ist ist' ->
+    similar (mk_ctx ist sp ge) (mk_ctx ist' sp tge).
 
 Definition beq_pred_expr_once (pe1 pe2: pred_expr) : bool :=
   match pe1, pe2 with
@@ -977,7 +1004,7 @@ Section CORRECT.
     induction e using expression_ind2
       with (P0 := fun p => forall v v',
                     sem_val_list ictx p v -> sem_val_list octx p v' -> v = v');
-    inv HSIM; repeat progress simplify;
+    inv HSIM; match goal with H: context [match_states] |- _ => inv H end; repeat progress simplify;
     try solve [match goal with
                | H: sem_value _ _ _, H2: sem_value _ _ _ |- _ => inv H; inv H2; auto
                | H: sem_mem _ _ _, H2: sem_mem _ _ _ |- _ => inv H; inv H2; auto
@@ -990,23 +1017,54 @@ Section CORRECT.
                IH: forall _ _, sem_val_list _ _ _ -> sem_val_list _ _ _ -> _ = _ |- _ =>
                assert (X: l1 = l2) by (apply IH; auto)
              | H: ge_preserved _ _ |- _ => inv H
+             | |- context [ctx_rs] => unfold ctx_rs; cbn
+             | H: context [ctx_mem] |- _ => unfold ctx_mem in H; cbn
              end; crush.
-    - inv H1. inv H0. simplify.
-      assert (lv0 = lv). apply IHe; eauto. subst.
-      inv H. rewrite H1 in H13.
-      assert (a0 = a1) by crush. subst.
-      assert (m'1 = m'0). apply IHe0; eauto. subst.
-      crush.
-    - inv H0. inv H1. simplify.
-      assert (lv = lv0). { apply IHe2; eauto. } subst.
-      assert (a1 = a0). { inv H.  rewrite H1 in H12. crush. } subst.
-      assert (v0 = v1). { apply IHe1; auto. } subst.
-      assert (m'0 = m'1). { apply IHe3; auto. } subst.
-      crush.
-    - inv H0. inv H1. f_equal. apply IHe; auto.
+    - repeat match goal with H: sem_value _ _ _ |- _ => inv H end; simplify;
+      assert (lv0 = lv) by (apply IHe; eauto); subst;
+      match goal with H: ge_preserved _ _ |- _ => inv H end;
+      match goal with H: context [Op.eval_addressing _ _ _ _ = Op.eval_addressing _ _ _ _] |- _
+                      => rewrite H in * end;
+      assert (a0 = a1) by crush;
+      assert (m'2 = m'1) by (apply IHe0; eauto); crush.
+    - inv H0; inv H3. simplify.
+      assert (lv = lv0) by ( apply IHe2; eauto). subst.
+      assert (a1 = a0). { inv H. rewrite H3 in *. crush. }
+      assert (v0 = v1). { apply IHe1; auto. }
+      assert (m'1 = m'2). { apply IHe3; auto. } crush.
+    - inv H0. inv H3. f_equal. apply IHe; auto.
       apply IHe0; auto.
   Qed.
 
+  Lemma sem_value_mem_corr:
+    forall e v m,
+      (sem_value ictx e v -> sem_value octx e v)
+      /\ (sem_mem ictx e m -> sem_mem octx e m).
+  Proof using HSIM.
+    induction e using expression_ind2
+      with (P0 := fun p => forall v,
+                    sem_val_list ictx p v -> sem_val_list octx p v);
+    inv HSIM; match goal with H: context [match_states] |- _ => inv H end; repeat progress simplify.
+    - inv H0. unfold ctx_rs, ctx_ps, ctx_mem in *; cbn. rewrite H1. constructor.
+    - inv H0. unfold ctx_rs, ctx_ps, ctx_mem in *; cbn. constructor.
+    - inv H0. apply IHe in H6. econstructor; try eassumption.
+      unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H. crush.
+    - inv H0.
+    - inv H0. eapply IHe in H10. eapply IHe0 in H8; auto.
+      econstructor; try eassumption.
+      unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush.
+    - inv H0.
+    - inv H0.
+    - inv H0. eapply IHe1 in H11; auto. eapply IHe2 in H12; auto. eapply IHe3 in H9; auto.
+      econstructor; try eassumption.
+      unfold ctx_rs, ctx_ps, ctx_mem in *; cbn in *. inv H; crush.
+    - inv H0.
+    - inv H0.
+    - inv H0. econstructor.
+    - inv H0. eapply IHe in H6; auto. eapply IHe0 in H8.
+      econstructor; eassumption.
+  Qed.
+
   Lemma sem_value_det:
     forall e v v',
       sem_value ictx e v -> sem_value octx e v' -> v = v'.
@@ -1014,6 +1072,13 @@ Section CORRECT.
     intros. eapply sem_value_mem_det; eauto; apply Mem.empty.
   Qed.
 
+  Lemma sem_value_corr:
+    forall e v,
+      sem_value ictx e v -> sem_value octx e v.
+  Proof using HSIM.
+    intros. eapply sem_value_mem_corr; eauto; apply Mem.empty.
+  Qed.
+
   Lemma sem_mem_det:
     forall e v v',
       sem_mem ictx e v -> sem_mem octx e v' -> v = v'.
@@ -1021,6 +1086,13 @@ Section CORRECT.
     intros. eapply sem_value_mem_det; eauto; apply (Vint (Int.repr 0%Z)).
   Qed.
 
+  Lemma sem_mem_corr:
+    forall e v,
+      sem_mem ictx e v -> sem_mem octx e v.
+  Proof using HSIM.
+    intros. eapply sem_value_mem_corr; eauto; apply (Vint (Int.repr 0%Z)).
+  Qed.
+
   Lemma sem_val_list_det:
     forall e l l',
       sem_val_list ictx e l -> sem_val_list octx e l' -> l = l'.
@@ -1031,12 +1103,34 @@ Section CORRECT.
       apply IHe; eauto.
   Qed.
 
+  Lemma sem_val_list_corr:
+    forall e l,
+      sem_val_list ictx e l -> sem_val_list octx e l.
+  Proof using HSIM.
+    induction e; simplify.
+    - inv H; constructor.
+    - inv H. apply sem_value_corr in H3; auto; try apply Mem.empty;
+      apply IHe in H5; constructor; assumption.
+  Qed.
+
   Lemma sem_pred_det:
     forall e v v',
       sem_pred ictx e v -> sem_pred octx e v' -> v = v'.
   Proof using HSIM.
-    try solve [inversion 1]; pose proof sem_value_det; pose proof sem_val_list_det; inv HSIM; simplify.
-    inv H2; inv H3; auto. assert (lv = lv0) by (eapply H0; eauto). crush.
+    try solve [inversion 1]; pose proof sem_value_det; pose proof sem_val_list_det; inv HSIM;
+      match goal with H: match_states _ _ |- _ => inv H end; simplify.
+    inv H2; inv H5; auto. assert (lv = lv0) by (eapply H0; eauto). subst. unfold ctx_mem in *.
+    crush.
+  Qed.
+
+  Lemma sem_pred_corr:
+    forall e v,
+      sem_pred ictx e v -> sem_pred octx e v.
+  Proof using HSIM.
+    try solve [inversion 1]; pose proof sem_value_corr; pose proof sem_val_list_corr; inv HSIM;
+      match goal with H: match_states _ _ |- _ => inv H end; simplify.
+    inv H2; auto. apply H0 in H5. econstructor; eauto.
+    unfold ctx_ps; cbn. rewrite H4. constructor.
   Qed.
 
   #[local] Opaque PTree.set.
@@ -1116,7 +1210,7 @@ Section CORRECT.
         sem_pred_tree isem ictx h t v ->
         sem_pred_tree osem octx h' t' v' ->
         v = v'.
-    Proof.
+    Proof using HSIM SEMSIM.
       intros. inv H4. inv H5.
       destruct (Pos.eq_dec e e0); subst.
       { eapply norm_expr_constant in H3; [|eassumption].
@@ -1133,7 +1227,11 @@ Section CORRECT.
           pose proof H0. eapply norm_expr_forall_impl in H0; [| | | |eassumption]; try eassumption.
           unfold "⇒" in H0. unfold eval_predf in *. apply H0 in H6.
           rewrite negate_correct in H6. apply negb_true_iff in H6.
-          inv HSIM. crush. }
+          inv HSIM. match goal with H: match_states _ _ |- _ => inv H end.
+          unfold ctx_ps, ctx_mem, ctx_rs in *. simplify.
+          pose proof eval_predf_pr_equiv pr0 ps ps' H17. unfold eval_predf in *.
+          rewrite H5 in H6. crush.
+        }
         { unfold beq_pred_expr in H. repeat (destruct_match; []). inv H2.
           rewrite Heqp0 in H3. inv H3. simplify.
           eapply forall_ptree_true in H3. 2: { eapply H11. }
@@ -1224,18 +1322,30 @@ Section CORRECT.
 
   End SEM_PRED.
 
-  Inductive match_instr_state : instr_state -> instr_state -> Prop :=
-  | match_instr_state_intro : forall i1 i2,
-      is_mem i1 = is_mem i2 ->
-      (forall x, (is_rs i1) !! x = (is_rs i2) !! x) ->
-      (forall x, (is_ps i1) !! x = (is_ps i2) !! x) ->
-      match_instr_state i1 i2.
+  Section SEM_PRED_CORR.
+
+    Context (B: Type).
+    Context (isem: @ctx fd -> expression -> B -> Prop).
+    Context (osem: @ctx tfd -> expression -> B -> Prop).
+    Context (SEMCORR: forall e v, isem ictx e v -> osem octx e v).
+
+    Lemma sem_pred_tree_corr:
+      forall x x' v t t' h h',
+             beq_pred_expr x x' = true ->
+             predicated_mutexcl x -> predicated_mutexcl x' ->
+             norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x (PTree.empty _) = (t, h) ->
+             norm_expression (Pos.max (max_pred_expr x) (max_pred_expr x')) x' h = (t', h') ->
+             sem_pred_tree isem ictx h t v ->
+             sem_pred_tree osem octx h' t' v.
+    Proof using SEMCORR. Admitted.
+
+  End SEM_PRED_CORR.
 
   Lemma check_correct: forall (fa fb : forest) i i',
       check fa fb = true ->
       sem ictx fa i ->
       sem octx fb i' ->
-      match_instr_state i i'.
+      match_states i i'.
   Proof using HSIM.
     intros.
     unfold check, get_forest in *; intros;
@@ -1257,6 +1367,13 @@ Section CORRECT.
     }
 Admitted.
 
+  Lemma check_correct2:
+    forall (fa fb : forest) i,
+      check fa fb = true ->
+      sem ictx fa i ->
+      exists i', sem octx fb i' /\ match_states i i'.
+  Proof. Admitted.
+
 End CORRECT.
 
 Lemma get_empty:
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 7e204e7..6b4b5be 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -111,6 +111,29 @@ Proof.
   unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0.
 Qed.
 
+#[local] Open Scope pred_op.
+
+Lemma eval_predf_Pand :
+  forall ps p p',
+    eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_Por :
+  forall ps p p',
+    eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
+Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
+
+Lemma eval_predf_pr_equiv :
+  forall p ps ps',
+    (forall x, ps !! x = ps' !! x) ->
+    eval_predf ps p = eval_predf ps' p.
+Proof.
+  induction p; simplify; auto;
+    try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+  [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
+  erewrite IHp1; try eassumption; erewrite IHp2; eauto.
+Qed.
+
 Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   match rl, vl with
   | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 14d354f..87458e7 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -131,21 +131,10 @@ Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Pro
   /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl =
                          Op.eval_addressing tge sp addr vl).
 
-Lemma ge_preserved_same:
-  forall A B ge, @ge_preserved A B A B ge ge.
-Proof. unfold ge_preserved; auto. Qed.
 #[local] Hint Resolve ge_preserved_same : rtlpar.
 
 Ltac rtlpar_crush := crush; eauto with rtlpar.
 
-Inductive match_states : instr_state -> instr_state -> Prop :=
-| match_states_intro:
-  forall ps ps' rs rs' m m',
-    (forall x, rs !! x = rs' !! x) ->
-    (forall x, ps !! x = ps' !! x) ->
-    m = m' ->
-    match_states (mk_instr_state rs ps  m) (mk_instr_state rs' ps' m').
-
 Inductive match_states_ld : instr_state -> instr_state -> Prop :=
 | match_states_ld_intro:
   forall ps ps' rs rs' m m',
@@ -154,13 +143,13 @@ Inductive match_states_ld : instr_state -> instr_state -> Prop :=
     Mem.extends m m' ->
     match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m').
 
-Lemma sems_det:
+(*Lemma sems_det:
   forall A ge tge sp f rs ps m,
   ge_preserved ge tge ->
   forall v v' mv mv',
   (@sem_value A (mk_ctx rs ps m sp ge) f v /\ @sem_value A (mk_ctx rs ps m sp tge) f v' -> v = v') /\
   (@sem_mem A (mk_ctx rs ps m sp ge) f mv /\ @sem_mem A (mk_ctx rs ps m sp tge) f mv' -> mv = mv').
-Proof. Abort.
+Proof. Abort.*)
 
 (*Lemma sem_value_det:
   forall A ge tge sp st f v v',
@@ -420,24 +409,11 @@ RTLBlock to abstract translation
 Correctness of translation from RTLBlock to the abstract interpretation language.
 |*)
 
-Lemma match_states_refl x : match_states x x.
-Proof. destruct x; constructor; crush. Qed.
-
-Lemma match_states_commut x y : match_states x y -> match_states y x.
-Proof. inversion 1; constructor; crush. Qed.
-
-Lemma match_states_trans x y z :
-  match_states x y -> match_states y z -> match_states x z.
-Proof. repeat inversion 1; constructor; crush. Qed.
-
 Ltac inv_simp :=
   repeat match goal with
   | H: exists _, _ |- _ => inv H
   end; simplify.
 
-Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st.
-Proof. destruct st; repeat constructor. Qed.
-
 Lemma abstract_interp_empty3 :
   forall A ge sp st st',
     @sem A ge sp st empty st' ->
@@ -541,11 +517,6 @@ Lemma abstr_comp :
   x = update x0 i.
 Proof. induction l; intros; crush; eapply IHl; eauto. 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 check_list_l_false :
   forall l x r,
   check_dest_l (l ++ x :: nil) r = false ->
@@ -581,19 +552,7 @@ Proof.
   apply check_list_l_false in H. tauto.
 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. inv_simp.
-  econstructor. split.
-  econstructor; eauto. eauto.
-Qed.
+
 
 Lemma sem_update_RBnop :
   forall A ge sp st f st',
@@ -788,25 +747,6 @@ Proof.
   eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store.
 Qed.
 
-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 ge sp tst (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. inv_simp.
-    rewrite abstract_seq.
-    exploit IHbb; try eassumption; []; inv_simp.
-    exploit sem_update. apply H1. apply match_states_commut; eassumption.
-    eauto. inv_simp. econstructor. split. apply H3.
-    auto. }
-Qed.
-
 Lemma abstr_sem_val_mem :
   forall A B ge tge st tst sp a,
     ge_preserved ge tge ->
@@ -938,6 +878,62 @@ Lemma step_instr_seq_same :
   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 sem_separate :
+  forall A (ge: @RTLBlockInstr.genv A) b a sp st st',
+    sem ge sp st (abstract_sequence empty (a ++ b)) st' ->
+    exists st'',
+         sem ge sp st (abstract_sequence empty a) st''
+      /\ sem ge sp st'' (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; inv_simp.
+    exploit IHb; eauto; inv_simp.
+    econstructor; split; eauto.
+    rewrite abstract_seq.
+    eapply sem_update2; eauto.
+  }
+Qed.
+
+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) ->
@@ -956,18 +952,53 @@ 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'.
+    @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;
-  repeat econstructor; try erewrite match_states_list;
+  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.
+  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 :
@@ -978,8 +1009,8 @@ Lemma step_instr_list_matches :
                            /\ match_states st' tst'.
 Proof.
   induction a; intros; inv H;
-  try (exploit step_instr_matches; eauto; []; inv_simp;
-       exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto.
+  try (exploit step_instr_matches; eauto; []; simplify;
+       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
 Qed.
 
 Lemma step_instr_seq_matches :
@@ -990,8 +1021,8 @@ Lemma step_instr_seq_matches :
                            /\ match_states st' tst'.
 Proof.
   induction a; intros; inv H;
-  try (exploit step_instr_list_matches; eauto; []; inv_simp;
-       exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto.
+  try (exploit step_instr_list_matches; eauto; []; simplify;
+       exploit IHa; eauto; []; simplify); repeat econstructor; eauto.
 Qed.
 
 Lemma step_instr_block_matches :
@@ -1002,66 +1033,71 @@ Lemma step_instr_block_matches :
                            /\ match_states st' tst'.
 Proof.
   induction bb; intros; inv H;
-  try (exploit step_instr_seq_matches; eauto; []; inv_simp;
-       exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto.
+  try (exploit step_instr_seq_matches; eauto; []; simplify;
+       exploit IHbb; eauto; []; simplify); repeat econstructor; eauto.
 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''.
+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.
-  Admitted.
+  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 sem_separate :
-  forall A (ge: @RTLBlockInstr.genv A) b a sp st st',
-    sem ge sp st (abstract_sequence empty (a ++ b)) st' ->
-    exists st'',
-         sem ge sp st (abstract_sequence empty a) st''
-      /\ sem ge sp st'' (abstract_sequence empty b) st'.
+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 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 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; inv_simp.
-    exploit IHb; eauto; inv_simp.
-    econstructor; split; eauto.
+  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.
-    eapply sem_update2; eauto.
-  }
+    exploit IHbb; try eassumption; []; simplify.
+    exploit sem_update. apply H1. symmetry; eassumption.
+    eauto. simplify. econstructor. split. apply H3.
+    auto. }
 Qed.
 
-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:
-  forall bb bb' cfi ge tge sp st st' tst,
+  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 ->
+    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.
-  exploit rtlblock_trans_correct; try eassumption; []; inv_simp.
+  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.
@@ -1072,18 +1108,6 @@ Proof.
   econstructor; congruence.
 Qed.
 
-(*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.*)
-*)
-
 (*|
 Top-level functions
 ===================
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index bb1cf97..fc3272a 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-(*Require Import compcert.backend.Registers.
+Require Import compcert.backend.Registers.
 Require Import compcert.common.AST.
 Require Import compcert.common.Errors.
 Require Import compcert.common.Linking.
@@ -36,20 +36,22 @@ Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
 
 Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
 | match_stackframe:
-    forall f tf res sp pc rs rs',
+    forall f tf res sp pc rs rs' ps ps',
       transl_function f = OK tf ->
       (forall x, rs !! x = rs' !! x) ->
-      match_stackframes (Stackframe res f sp pc rs)
-                        (Stackframe res tf sp pc rs').
+      (forall x, ps !! x = ps' !! x) ->
+      match_stackframes (Stackframe res f sp pc rs ps)
+                        (Stackframe res tf sp pc rs' ps).
 
 Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
 | match_state:
-    forall sf f sp pc rs rs' m sf' tf
+    forall sf f sp pc rs rs' m sf' tf ps ps'
       (TRANSL: transl_function f = OK tf)
       (STACKS: list_forall2 match_stackframes sf sf')
-      (REG: forall x, rs !! x = rs' !! x),
-      match_states (State sf f sp pc rs m)
-                   (State sf' tf sp pc rs' m)
+      (REG: forall x, rs !! x = rs' !! x)
+      (REG: forall x, ps !! x = ps' !! x),
+      match_states (State sf f sp pc rs ps m)
+                   (State sf' tf sp pc rs' ps' m)
 | match_returnstate:
     forall stack stack' v m
       (STACKS: list_forall2 match_stackframes stack stack'),
@@ -284,7 +286,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
         match_states s r ->
         exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'.
   Proof using TRANSL.
-    induction 1; repeat semantics_simpl;
+    (*induction 1; repeat semantics_simpl;
     try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)].
     { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp).
       eapply eval_builtin_args_eq. eapply REG.
@@ -301,7 +303,7 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
       unfold regmap_optget. destruct or. rewrite REG. constructor; eauto.
       constructor; eauto.
     }
-  Qed.
+  Qed.*) Admitted.
 
   Theorem transl_step_correct :
     forall (S1 : RTLBlock.state) t S2,
@@ -377,4 +379,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
   Qed.
 
 End CORRECTNESS.
-*)