Proof of Pfmovimm fine tuned OK, moving float checks in Asm

Also some simplifications in Asmblockdeps

1 files changed, 96 insertions, 240 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 7bdc734e..a913313b 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -960,21 +960,9 @@ Proof.
   simpl; try discriminate; try reflexivity.
 Qed.
 
-Lemma ppos_discr: forall r r', r <> r' -> ppos r <> ppos r'.
+Lemma ppos_discr: forall r r', r <> r' <-> ppos r <> ppos r'.
 Proof.
-  destruct r as [dr|cr|]; destruct r' as [dr'|cr'|];
-  try destruct dr as [ir|fr]; try destruct dr' as [ir'|fr'];
-  try destruct ir as [irr|]; try destruct ir' as [irr'|].
-  all: try discriminate; try contradiction.
-  1: intros; unfold ppos; apply ireg_to_pos_discr; congruence.
-  1,2,11,18: intros; unfold ppos; try destruct irr; try destruct irr'; discriminate.
-  1,3: intros; unfold ppos; try destruct irr; try destruct fr; try destruct irr'; try destruct fr'; discriminate.
-  1,2,7,13: intros; unfold ppos; try destruct fr; try destruct fr'; discriminate.
-  1: intros; unfold ppos; apply freg_to_pos_discr; congruence.
-  1,4: intros; unfold ppos; try destruct irr; try destruct irr'; try destruct cr; try destruct cr'; discriminate.
-  2,4: intros; unfold ppos; try destruct fr; try destruct fr'; try destruct cr; try destruct cr'; discriminate.
-  1,2,4,5: intros; unfold ppos; try destruct cr; try destruct cr'; discriminate.
-  1: intros; unfold ppos; try destruct cr; try destruct cr'; congruence.
+  split; unfold not; try intros; try apply ppos_equal in H0; try discriminate; try contradiction.
 Qed.
 
 Lemma ppos_pmem_discr: forall r, pmem <> ppos r.
@@ -1236,16 +1224,28 @@ Proof.
   intros. congruence.
 Qed.
 
-Lemma ireg_pos_ppos: forall (sr: state) r,
+(* Lemma sr_ireg_pos_ppos: forall (sr: state) r,
   sr (ireg_to_pos r) = sr (# r).
 Proof.
   intros. simpl. reflexivity.
 Qed.
 
-Lemma freg_pos_ppos: forall (sr: state) r,
+Lemma sr_freg_pos_ppos: forall (sr: state) r,
   sr (freg_to_pos r) = sr (# r).
 Proof.
   intros. simpl. reflexivity.
+Qed. *)
+
+Lemma ireg_pos_ppos: forall r,
+  ireg_to_pos r = # r.
+Proof.
+  intros. simpl. reflexivity.
+Qed.
+
+Lemma freg_pos_ppos: forall r,
+  freg_to_pos r = # r.
+Proof.
+  intros. simpl. reflexivity.
 Qed.
 
 Lemma ireg_not_pc: forall r,
@@ -1314,63 +1314,15 @@ Proof.
   intros; destruct r; discriminate.
 Qed.
 
-Lemma sr_ireg_update_both: forall sr rsr r1 rr v
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  (sr <[ ireg_to_pos r1 <- Val (v) ]>) (#rr) =
-  Val (rsr # r1 <- v rr).
-Proof.
-  intros. unfold assign.
-  destruct (PregEq.eq r1 rr); subst.
-  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
-  - rewrite Pregmap.gso; eauto.
-    destruct rr; try congruence.
-    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
-    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-Qed.
-
-Lemma sr_freg_update_both: forall sr rsr r1 rr v
+Lemma sr_update_both: forall sr rsr r1 rr v
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  (sr <[ freg_to_pos r1 <- Val (v) ]>) (#rr) =
+  (sr <[ (#r1) <- Val (v) ]>) (#rr) =
   Val (rsr # r1 <- v rr).
 Proof.
   intros. unfold assign.
-  destruct (PregEq.eq r1 rr); subst.
-  - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity.
-  - rewrite Pregmap.gso; eauto.
-    destruct rr; try congruence.
-    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence.
-    + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-    + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-Qed.
-
-Lemma sr_xsp_update_both: forall sr rsr rr v
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  (sr <[ #XSP <- Val (v) ]>) (#rr) =
-  Val (rsr # XSP <- v rr).
-Proof.
-  intros. unfold assign.
-  destruct (PregEq.eq XSP rr); subst.
-  - rewrite Pregmap.gss. simpl. reflexivity.
-  - rewrite Pregmap.gso; eauto.
-    destruct rr; try congruence.
-    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
-    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-    + simpl; try rewrite <- HEQV; unfold ppos; try congruence.
-Qed.
-
-Lemma sr_pc_update_both: forall sr rsr rr v
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  (sr <[ #PC <- Val (v) ]>) (#rr) =
-  Val (rsr # PC <- v rr).
-Proof.
-  intros. unfold assign.
-  destruct (PregEq.eq PC rr); subst.
-  - rewrite Pregmap.gss. simpl. reflexivity.
-  - rewrite Pregmap.gso; eauto.
-    destruct rr; try congruence.
-    + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.
-    + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.
+  destruct (R.eq_dec (#r1) (#rr)); subst.
+  - apply ppos_equal in e; subst; rewrite Pregmap.gss; reflexivity.
+  - rewrite Pregmap.gso; eapply ppos_discr in n; auto.
 Qed.
 
 Lemma sr_gss: forall sr pos v,
@@ -1402,9 +1354,9 @@ Ltac sr_memstate_rwrt :=
 
 Ltac replace_ppos :=
   try erewrite !ireg_pos_ppos;
-  try erewrite !freg_pos_ppos.
-
-Ltac DI0N0 ir0 := destruct ir0; subst; simpl.
+  try erewrite !freg_pos_ppos;
+  try replace (7) with (#XSP) by eauto;
+  try replace (24) with (#X16) by auto.
 
 Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
 
@@ -1413,10 +1365,10 @@ Ltac DDRM dr :=
       [destruct irsDDRF
       | idtac ].
 
-Ltac DDRF dr :=
+(* Ltac DDRF dr :=
   destruct dr as [irsDDRF|frDDRF]; 
       [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|]
-      | destruct frDDRF].
+      | destruct frDDRF]. *)
 
 Ltac DPRF pr :=
   destruct pr as [drDPRF|crDPRF|]; 
@@ -1429,11 +1381,11 @@ Ltac DPRM pr :=
       [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
       | destruct crDPRF|].
 
-Ltac DPRI pr :=
+(* Ltac DPRI pr :=
   destruct pr as [drDPRI|crDPRI|]; 
       [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|]
       | idtac
-      | idtac ].
+      | idtac ]. *)
 
 Ltac discriminate_ppos :=
   try apply ireg_not_pmem;
@@ -1479,36 +1431,18 @@ Ltac Simpl_rep sr :=
   ).
 
 Ltac Simpl_update :=
-  try eapply sr_ireg_update_both; eauto;
-  try eapply sr_freg_update_both; eauto;
-  try eapply sr_xsp_update_both; eauto;
-  try eapply sr_pc_update_both; eauto.
+  try eapply sr_update_both; eauto.
 
-Ltac Simpl sr := Simpl_exists sr; try (intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr); Simpl_update.
+Ltac Simpl sr := Simpl_exists sr; try (intros rr(* ; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr *)); Simpl_update.
 
 Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity.
 
-Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity.
-
-Ltac validate_crbit_flags c :=
-  destruct c;
-  [
-    do 3 (rewrite assign_diff; discriminate_ppos);
-    do 3 (rewrite Pregmap.gso; try discriminate);
-    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
-    do 2 (rewrite assign_diff; discriminate_ppos);
-    do 2 (rewrite Pregmap.gso; try discriminate);
-    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
-    do 1 (rewrite assign_diff; discriminate_ppos);
-    do 1 (rewrite Pregmap.gso; try discriminate);
-    rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
-    rewrite sr_gss; rewrite Pregmap.gss; reflexivity
-  ].
-
-Ltac destruct_reg_neq r1 r2 :=
+(* Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity. *)
+
+(* Ltac destruct_reg_neq r1 r2 :=
   destruct (PregEq.eq r1 r2); subst;
    [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
-     rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto].
+     rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. *)
 
 Lemma reg_update_overwrite: forall rsr sr r rd v1 v2
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
@@ -1522,22 +1456,34 @@ Proof.
     unfold not; intros. apply ppos_equal in H. congruence.
 Qed.
 
-Lemma compare_single_res_aux: forall sr mr rsr rr
-  (HMEM: sr pmem = Memstate mr)
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  ((((sr <[ 2 <- Val (_CN (v_compare_single Vundef Vundef)) ]>) <[ 3 <-
-   Val (_CZ (v_compare_single Vundef Vundef)) ]>) <[ 4 <-
-  Val (_CC (v_compare_single Vundef Vundef)) ]>) <[ 5 <-
- Val (_CV (v_compare_single Vundef Vundef)) ]>) (# rr) =
-Val
-  ((compare_single rsr Vundef Vundef) rr).
-Proof.
-  intros. unfold v_compare_single, compare_single.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
-Qed.
+Ltac replace_regs_cond_force :=
+  try replace (5) with (#CV) in * by auto;
+  try replace (4) with (#CC) in * by auto;
+  try replace (3) with (#CZ) in * by auto;
+  try replace (2) with (#CN) in * by auto.
+  
+Ltac validate_crbit_flags rr v1 v2 :=
+  destruct (R.eq_dec 5 (#rr)) as [eCV|eCV]; subst;
+  [ destruct v1; destruct v2; simpl;
+    replace_regs_cond_force; apply ppos_equal in eCV; subst;
+    rewrite Pregmap.gss; auto |
+  destruct (R.eq_dec 4 (#rr)) as [eCC|eCC]; subst;
+  [ destruct v1; destruct v2; simpl;
+      replace_regs_cond_force; apply ppos_equal in eCC; subst;
+      rewrite Pregmap.gso, Pregmap.gss; auto; try discriminate |
+  destruct (R.eq_dec 3 (#rr)) as [eCZ|eCZ]; subst;
+  [ destruct v1; destruct v2; simpl;
+      replace_regs_cond_force; apply ppos_equal in eCZ; subst;
+      rewrite 2Pregmap.gso, Pregmap.gss; auto; try discriminate |
+  destruct (R.eq_dec 2 (#rr)) as [eCN|eCN]; subst;
+  [ destruct v1; destruct v2; simpl;
+      replace_regs_cond_force; apply ppos_equal in eCN; subst;
+      rewrite 3Pregmap.gso, Pregmap.gss; auto; try discriminate |
+  destruct v1; destruct v2; simpl;
+  replace_regs_cond_force;
+  apply ppos_discr in eCV; apply ppos_discr in eCC;
+  apply ppos_discr in eCZ; apply ppos_discr in eCN;
+  rewrite 4Pregmap.gso; auto; try discriminate ]]]].
 
 Lemma compare_single_res: forall sr mr rsr rr v1 v2
   (HMEM: sr pmem = Memstate mr)
@@ -1549,31 +1495,8 @@ Lemma compare_single_res: forall sr mr rsr rr v1 v2
 Val
   ((compare_single rsr v1 v2) rr).
 Proof.
-  intros.
-  destruct v1; destruct v2;
-  try eapply compare_single_res_aux; eauto.
-  unfold v_compare_single, compare_single.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
-Qed.
-
-Lemma compare_float_res_aux: forall sr mr rsr rr
-  (HMEM: sr pmem = Memstate mr)
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  ((((sr <[ 2 <- Val (_CN (v_compare_float Vundef Vundef)) ]>) <[ 3 <-
-   Val (_CZ (v_compare_float Vundef Vundef)) ]>) <[ 4 <-
-  Val (_CC (v_compare_float Vundef Vundef)) ]>) <[ 5 <-
- Val (_CV (v_compare_float Vundef Vundef)) ]>) (# rr) =
-Val
-  ((compare_float rsr Vundef Vundef) rr).
-Proof.
-  intros. unfold v_compare_float, compare_float.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
+  intros. unfold v_compare_single, compare_single, assign.
+  validate_crbit_flags rr v1 v2.
 Qed.
 
 Lemma compare_float_res: forall sr mr rsr rr v1 v2
@@ -1586,31 +1509,8 @@ Lemma compare_float_res: forall sr mr rsr rr v1 v2
 Val
   ((compare_float rsr v1 v2) rr).
 Proof.
-  intros.
-  destruct v1; destruct v2;
-  try eapply compare_float_res_aux; eauto.
-  unfold v_compare_float, compare_float.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
-Qed.
-
-Lemma compare_long_res_aux: forall sr mr rsr rr
-  (HMEM: sr pmem = Memstate mr)
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  ((((sr <[ 2 <- Val (_CN (v_compare_long Vundef Vundef)) ]>) <[ 3 <-
-   Val (_CZ (v_compare_long Vundef Vundef)) ]>) <[ 4 <-
-  Val (_CC (v_compare_long Vundef Vundef)) ]>) <[ 5 <-
- Val (_CV (v_compare_long Vundef Vundef)) ]>) (# rr) =
-Val
-  ((compare_long rsr Vundef Vundef) rr).
-Proof.
-  intros. unfold v_compare_long, compare_long.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
+  intros. unfold v_compare_float, compare_float, assign.
+  validate_crbit_flags rr v1 v2.
 Qed.
 
 Lemma compare_long_res: forall sr mr rsr rr v1 v2
@@ -1623,31 +1523,8 @@ Lemma compare_long_res: forall sr mr rsr rr v1 v2
 Val
   ((compare_long rsr v1 v2) rr).
 Proof.
-  intros.
-  destruct v1; destruct v2;
-  try eapply compare_long_res_aux; eauto;
-  unfold v_compare_long, compare_long;
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
-Qed.
-
-Lemma compare_int_res_aux: forall sr mr rsr rr
-  (HMEM: sr pmem = Memstate mr)
-  (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
-  ((((sr <[ 2 <- Val (_CN (v_compare_int Vundef Vundef)) ]>) <[ 3 <-
-   Val (_CZ (v_compare_int Vundef Vundef)) ]>) <[ 4 <-
-  Val (_CC (v_compare_int Vundef Vundef)) ]>) <[ 5 <-
- Val (_CV (v_compare_int Vundef Vundef)) ]>) (# rr) =
-Val
-  ((compare_int rsr Vundef Vundef) rr).
-Proof.
-  intros. unfold v_compare_int, compare_int.
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
+  intros. unfold v_compare_long, compare_long, assign.
+  validate_crbit_flags rr v1 v2.
 Qed.
 
 Lemma compare_int_res: forall sr mr rsr rr v1 v2
@@ -1660,14 +1537,8 @@ Lemma compare_int_res: forall sr mr rsr rr v1 v2
 Val
   ((compare_int rsr v1 v2) rr).
 Proof.
-  intros.
-  destruct v1; destruct v2;
-  try eapply compare_int_res_aux; eauto;
-  unfold v_compare_int, compare_int;
-  (destruct rr;
-    [ DDRF d; discriminate_preg_flags |
-      validate_crbit_flags c |
-      discriminate_preg_flags ]).
+  intros. unfold v_compare_int, compare_int, assign.
+  validate_crbit_flags rr v1 v2.
 Qed.
 
 Section SECT_SEQ.
@@ -1686,15 +1557,13 @@ Proof.
   - (* PArithP *)
     destruct i.
     1,2,3: DIRN1 rd; Simpl sr.
-    all: admit.
     (* Special case for Pmovimms/Pmovimmd *)
-    (* all: DIRN1 rd; Simpl sr;
-         try (rewrite assign_diff; discriminate_ppos; reflexivity);
-         try replace 24 with (#X16) by auto;
-         try replace 7 with (#XSP) by auto;
-         try (Simpl_update; intros rr; destruct_reg_neq r rr);
-         try (Simpl_update; intros rr; destruct_reg_neq XSP rr);
-         try (Simpl_update; intros rr; destruct_reg_neq f0 rr). *)
+    all: simpl;
+      try(destruct (negb (is_immediate_float32 _)));
+      try(destruct (negb (is_immediate_float64 _)));
+      DIRN1 rd; Simpl sr;
+      try (rewrite assign_diff; discriminate_ppos; reflexivity);
+      try (intros rr'; Simpl_update).
   - (* PArithPP *)
     DIRN1 rs; DIRN1 rd; Simpl sr.
   - (* PArithPPP *)
@@ -1737,7 +1606,7 @@ Proof.
     try (eapply compare_int_res; eauto);
     try (eapply compare_float_res; eauto).
   - (* Pcset *)
-    simpl; (*DI0N0 rd.*) unfold eval_testcond, get_testcond_rlocs, cflags_eval;
+    simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval;
     unfold cond_eval_is; unfold flags_testcond_value, list_exp_eval; destruct c; simpl;
     repeat Simpl_rep sr; Simpl_exists sr;
     destruct_res_flag rsr;
@@ -1745,17 +1614,11 @@ Proof.
   - (* Pfmovi *)
     simpl; destruct r1; simpl; destruct fsz; Simpl sr.
   - (* Pcsel *)
-    simpl.
-    unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl;
-    repeat Simpl_rep sr;
-    (eexists; split; [| split]; [reflexivity | DDRM rd; Simpl_exists sr | idtac]).
-    all: intros rr; destruct (PregEq.eq rr rd);
-    [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity |
-    try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ].
+    simpl. destruct c; simpl;
+    DIRN1 r1; DIRN1 r2; Simpl_rep sr; DDRM rd; Simpl_exists sr; try intros rr; Simpl_update.
   - (* Pfnmul *)
     simpl; destruct fsz; Simpl sr.
-(* Qed. *)
-Admitted.
+Qed.
 
 Lemma sp_xsp:
   SP = XSP.
@@ -1785,10 +1648,7 @@ Local Ltac preg_eq_discr r rd :=
     destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H;
     unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv;
     try destruct (Mem.loadv _ _ _); simpl; auto.
-    all: eexists; split; [| split]; [ eauto | DDRF rd; eauto | idtac ];
-    intros rr; destruct (PregEq.eq rr rd); subst; [ rewrite Pregmap.gss; rewrite sr_gss; reflexivity |
-    rewrite assign_diff; try rewrite Pregmap.gso;
-    try rewrite H0; try (fold (ppos rd); eapply ppos_discr); auto].
+    all: DDRM rd; Simpl_exists sr; try intros rr; Simpl_update.
   - (* Store *)
     unfold exec_store, eval_addressing_rlocs_st, exp_eval;
     destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H;
@@ -1865,13 +1725,12 @@ Proof.
              try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
              try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
              try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
-             try (Simpl_exists sr; intros rr; destruct (PregEq.eq rr PC); subst;
-                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ]);
-             try (destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss;
-                  destruct Val.offset_ptr; try reflexivity; Simpl_exists sr;
-                  intros rr; destruct (PregEq.eq rr PC); subst;
-                  [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ];
-                  rewrite Pregmap.gso; auto)].
+             try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr);
+             destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss;
+             destruct Val.offset_ptr; try reflexivity; rewrite sr_update_overwrite; 
+             simpl; Simpl sr; (destruct (PregEq.eq rr PC); subst;
+                  [ rewrite sr_gss, Pregmap.gss; reflexivity |
+                  rewrite !assign_diff, !Pregmap.gso; replace_pc; auto; apply ppos_discr; auto]) ].
   - (* Ob *)
     replace_pc. rewrite (H0 PC). simpl.
     unfold goto_label, control_eval. destruct Ge.
@@ -1893,26 +1752,25 @@ Proof.
     1,2,3,4,5,6: destruct_res_flag rsr.
     7,8,9,10: do 2 (destruct_res_flag rsr).
     11,12 : do 3 (destruct_res_flag rsr).
-    1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| Simpl sr ];
+    1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
                       destruct (label_pos _ _ _); [| reflexivity]; replace_pc; 
                       rewrite !Pregmap.gss; destruct Val.offset_ptr;
                       try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr;
                       apply reg_update_overwrite; eauto.
-    1,3: destruct (andb); [| Simpl sr ];
+    1,3: destruct (andb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
          destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
          destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
          intros rr; apply reg_update_overwrite; eauto.
-    1,2: destruct (orb); [| Simpl sr ];
+    1,2: destruct (orb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ];
          destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss;
          destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr;
          intros rr; apply reg_update_overwrite; eauto.
   - (* Obl *)
     replace_pc. rewrite (H0 PC). simpl.
     unfold control_eval. destruct Ge.
-    rewrite sr_gss.
-    repeat Simpl_rep sr. Simpl_exists sr.
-    Simpl sr.
-    all: repeat (intros; replace_regs_pos sr; try replace (38) with (#X30) by eauto; unfold incrPC; Simpl_update).
+    rewrite sr_gss. Simpl sr.
+    replace_pc; try replace (38) with (#X30) by eauto; unfold incrPC. Simpl_update.
+    repeat (intros; Simpl_update).
   - (* Obs *)
     unfold control_eval. destruct Ge. replace_pc. rewrite (H0 PC). simpl; unfold incrPC.
     replace_pc; Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto.
@@ -1958,17 +1816,15 @@ Proof.
       rewrite assign_diff; auto.
       intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
       * rewrite sr_gss, Pregmap.gss. reflexivity.
-      * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto.
-
- (*simpl; inv MS. unfold control_eval; destruct Ge.
-      replace_pc; rewrite H0. congruence.*)
+      * rewrite assign_diff, Pregmap.gso; try rewrite H0;
+        auto; try rewrite ppos_discr in n; auto.
   - simpl. inv MS. eexists; split; [| split].
     + unfold control_eval; destruct Ge.
       replace_pc; rewrite (H0 PC); eauto.
     + rewrite assign_diff; auto.
     + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
       * rewrite sr_gss, Pregmap.gss. reflexivity.
-      * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto.
+      * rewrite assign_diff, Pregmap.gso; try rewrite H0; auto; try rewrite ppos_discr in n; auto.
 Qed.
 
 (* Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). *)