Removing addptrofs draft, next will be merging

1 files changed, 55 insertions, 116 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 9d1826ac..9f94828f 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -42,8 +42,7 @@ Set Implicit Arguments.
 
 Inductive oreg: Type :=
   | X0_L: oreg
-  | X0_R: oreg
-  | SP_S: oreg.
+  | X0_R: oreg.
 
 Inductive condition : Type :=
   | Ccomp (c: comparison)       (**r signed integer comparison *)
@@ -187,7 +186,6 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp (cond: condition)   (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
   (* Expansed conditions *)
-  | OEmoveSP 
   | OEseqw (optR: option oreg)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnew (optR: option oreg)                  (**r [rd <- rs1 != rs2] signed *)
   | OEsequw (optR: option oreg)                 (**r [rd <- rs1 == rs2] unsigned *)
@@ -281,12 +279,11 @@ Global Opaque eq_condition eq_addressing eq_operation.
 Definition zero32 := (Vint Int.zero).
 Definition zero64 := (Vlong Int64.zero).
   
-Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz sp: val): B :=
+Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B :=
   match optR with
   | None => sem v1 v2
   | Some X0_L => sem vz v1
   | Some X0_R => sem v1 vz
-  | Some SP_S => sem v1 sp
   end.
 
 (** Mayundef evaluation according to the above defined type *)
@@ -337,22 +334,22 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
   | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
   (* Expansed branches *)
-  | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 Vundef
-  | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 Vundef
-  | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef
-  | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef
-  | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 Vundef
-  | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef
-  | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 Vundef
-  | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 Vundef
-  | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 Vundef
-  | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 Vundef
-  | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef
-  | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef
-  | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 Vundef
-  | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef
-  | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 Vundef
-  | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 Vundef
+  | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32
+  | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32
+  | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
+  | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
+  | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32
+  | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32
+  | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32
+  | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32
+  | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64
+  | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64
+  | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
+  | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
+  | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64
+  | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64
+  | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64
+  | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64
   | _, _ => None
   end.
 
@@ -466,41 +463,32 @@ Definition eval_operation
   | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
   (* Expansed conditions *)
-  | OEmoveSP, nil => Some (get_sp sp)
-  | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32 Vundef)
-  | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32 Vundef)
-  | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef)
-  | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef)
-  | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32 Vundef)
-  | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef)
+  | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32)
+  | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32)
+  | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
+  | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
+  | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32)
+  | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
   | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
   | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
-  | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32 Vundef)
-  | OEaddiw ((Some SP_S) as optR) n, v1::nil =>
-      let sp' := Val.add (Vint n) (get_sp sp) in
-      Some (apply_bin_oreg optR Val.add v1 Vundef Vundef sp')
-  | OEaddiw optR n, v1::nil =>
-      Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef (get_sp sp))
+  | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32)
+  | OEaddiw optR n, v1::nil => Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef)
   | OEandiw n, v1::nil => Some (Val.and (Vint n) v1)
   | OEoriw n, v1::nil => Some (Val.or (Vint n) v1)
-  | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64 Vundef))
-  | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64 Vundef))
-  | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef))
-  | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef))
-  | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64 Vundef))
-  | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef))
+  | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64))
+  | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64))
+  | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
+  | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
+  | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64))
+  | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64))
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
   | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
   | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
   | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
-  | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64 Vundef)
-  | OEaddil ((Some SP_S) as optR) n, v1::nil =>
-      let sp' := Val.addl (Vlong n) (get_sp sp) in
-      Some (apply_bin_oreg optR Val.addl v1 Vundef Vundef sp')
-  | OEaddil optR n, v1::nil =>
-      Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef (get_sp sp))
+  | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64)
+  | OEaddil optR n, v1::nil => Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef)
   | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1)
   | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1)
   | OEloadli n, nil => Some (Vlong n)
@@ -598,14 +586,6 @@ Definition type_of_mayundef mu :=
   | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong)
   end.
 
-Definition type_addsp (is_long: bool): list typ * typ :=
-  if Archi.ptr64 then (
-    if is_long then (Tlong :: nil, Tptr)
-    else (nil, Tint))
-  else (
-    if is_long then (nil, Tlong)
-    else (Tint :: nil, Tptr)).
-
 Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
@@ -701,7 +681,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osingleoflong => (Tlong :: nil, Tsingle)
   | Osingleoflongu => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
-  | OEmoveSP => (nil, Tptr)
   | OEseqw _ => (Tint :: Tint :: nil, Tint)
   | OEsnew _ => (Tint :: Tint :: nil, Tint)
   | OEsequw _ => (Tint :: Tint :: nil, Tint)
@@ -713,7 +692,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OExoriw _ => (Tint :: nil, Tint)
   | OEluiw _ => (nil, Tint)
   | OEaddiw None _ => (Tint :: nil, Tint)
-  | OEaddiw (Some SP_S) _ => type_addsp false
   | OEaddiw (Some _) _ => (nil, Tint)
   | OEandiw _ => (Tint :: nil, Tint)
   | OEoriw _ => (Tint :: nil, Tint)
@@ -730,7 +708,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OExoril _ => (Tlong :: nil, Tlong)
   | OEluil _ => (nil, Tlong)
   | OEaddil None _ => (Tlong :: nil, Tlong)
-  | OEaddil (Some SP_S) _ => type_addsp true
   | OEaddil (Some _) _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
   | OEmayundef mu => type_of_mayundef mu
@@ -959,9 +936,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0; cbn; trivial.
   (* cmp *)
   - destruct (eval_condition cond vl m)... destruct b...
-  (* OEmoveSP *)
-  - destruct sp; unfold Tptr; destruct Archi.ptr64 eqn:?;
-    simpl; trivial.
   (* OEseqw *)
   - destruct optR as [[]|]; simpl; unfold Val.cmp;
     destruct Val.cmp_bool... all: destruct b...
@@ -986,12 +960,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEsltiuw *)
   - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
   (* OEaddiw *)
+  - destruct optR as [[]|]; simpl in *; trivial.
   - destruct optR as [[]|]; simpl in *; trivial;
-    destruct vl; inv H0; simpl; trivial;
-    destruct vl; inv H2; simpl; trivial;
-    destruct v0; simpl; trivial;
-    destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial;
-    unfold type_addsp, Tptr; try rewrite HA; simpl; trivial.
+    apply type_add.
   (* OEandiw *)
   - destruct v0...
   (* OEoriw *)
@@ -1024,12 +995,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OEsltiul *)
   - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
   (* OEaddil *)
+  - destruct optR as [[]|]; simpl in *; trivial.
   - destruct optR as [[]|]; simpl in *; trivial;
-    destruct vl; inv H0; simpl; trivial;
-    destruct vl; inv H2; simpl; trivial;
-    destruct v0; simpl; trivial;
-    destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial;
-    unfold type_addsp, Tptr; try rewrite HA; simpl; trivial.
+    apply type_addl.
   (* OEandil *)
   - destruct v0...
   (* OEoril *)
@@ -1099,7 +1067,6 @@ Proof.
   all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
   all: try (destruct vl3 as [ | vh4 vl4]; try discriminate).
   all: try destruct optR as [[]|]; simpl in H0; try discriminate.
-  all: unfold type_addsp in *; simpl in *.
   all: try destruct Archi.ptr64; simpl in *; try discriminate.
   all: try destruct mu; simpl in *; try discriminate.
 Qed.
@@ -1226,9 +1193,6 @@ Definition shift_stack_addressing (delta: Z) (addr: addressing) :=
 Definition shift_stack_operation (delta: Z) (op: operation) :=
   match op with
   | Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta))
-  | OEmoveSP => Oaddrstack (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta))
-  | OEaddiw (Some SP_S) n => OEaddiw (Some SP_S) (Ptrofs.to_int (Ptrofs.add (Ptrofs.of_int n) (Ptrofs.repr delta)))
-  | OEaddil (Some SP_S) n => OEaddil (Some SP_S) (Ptrofs.to_int64 (Ptrofs.add (Ptrofs.of_int64 n) (Ptrofs.repr delta)))
   | _ => op
   end.
 
@@ -1260,20 +1224,7 @@ Lemma eval_shift_stack_operation:
   eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
 Proof.
   intros. destruct op eqn:E; simpl; auto; destruct vl; auto.
-  - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
-  - rewrite !Ptrofs.add_zero_l; auto.
-  - destruct optR as [[]|]; simpl; auto.
-  - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto.
-    destruct v, Archi.ptr64 eqn:EA; simpl; try rewrite EA; simpl; auto.
-    rewrite Ptrofs.add_zero_l; auto.
-    rewrite Ptrofs.of_int_to_int; auto.
-    rewrite (Ptrofs.add_commut (Ptrofs.of_int n) (Ptrofs.repr delta)); reflexivity.
-  - destruct optR as [[]|]; simpl; auto.
-  - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto.
-    destruct Archi.ptr64 eqn:EA; auto.
-    rewrite Ptrofs.add_zero_l; auto.
-    rewrite Ptrofs.of_int64_to_int64; auto.
-    rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n) (Ptrofs.repr delta)); reflexivity.
+  rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
 Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
@@ -1533,8 +1484,8 @@ Qed.
 Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR,
   Val.inject f v v' ->
   Val.inject f v0 v'0 ->
-  Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32 Vundef)
-  (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef).
+  Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
+  (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32).
 Proof.
   intros until optR. intros HV1 HV2.
   destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; 
@@ -1544,11 +1495,9 @@ Proof.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
   + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
-  + exploit eval_cmpu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef).
+  + exploit eval_cmpu_bool_inj'. eapply HV1. instantiate (1:=v'0).
     eauto. eapply Heqo.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
-  + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
-    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
 Qed.
 
 Lemma eval_cmplu_bool_inj': forall b c v v' v0 v0',
@@ -1577,8 +1526,8 @@ Qed.
 Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR,
   Val.inject f v v' ->
   Val.inject f v0 v'0 ->
-  Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64 Vundef))
-  (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)).
+  Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64))
+  (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)).
 Proof.
   intros until optR. intros HV1 HV2.
   destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; 
@@ -1588,11 +1537,9 @@ Proof.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
   + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
-  + exploit eval_cmplu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef).
+  + exploit eval_cmplu_bool_inj'. eapply HV1. instantiate (1:=v'0).
     eauto. eapply Heqo.
     intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
-  + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
-    intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
 Qed.
 
 Lemma eval_condition_inj:
@@ -1857,9 +1804,6 @@ Proof.
     exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
     destruct b; simpl; constructor.
     simpl; constructor.
-  (* moveSP *)
-  - unfold get_sp; inv H; auto.
-    econstructor; eauto.
   (* OEseqw *)
   - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp;
     inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
@@ -1883,14 +1827,11 @@ Proof.
   (* OEsltiuw *)
   - apply eval_cmpu_bool_inj; auto.
   (* OEaddiw *)
-  - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists;
-    try fold (Val.add (Vint n) (get_sp sp1));
-    try fold (Val.add (Vint n) (get_sp sp2));
-    (*try destruct (get_sp sp1), (get_sp sp2);*)
-    apply Val.add_inject; auto.
-    apply Val.add_inject; auto.
-    destruct sp1, sp2; simpl; auto;
-    inv H.
+  - destruct optR as [[]|]; auto; simpl.
+    rewrite Int.add_zero_l; auto.
+    rewrite Int.add_commut, Int.add_zero_l; auto.
+  - destruct optR as [[]|]; auto; simpl;
+    eapply Val.add_inject; auto.
   (* OEandiw *)
   - inv H4; cbn; auto.
   (* OEoriw *)
@@ -1922,13 +1863,11 @@ Proof.
   (* OEsltiul *)
   - apply eval_cmplu_bool_inj; auto.
   (* OEaddil *)
-  - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists;
-    try fold (Val.addl (Vlong n) (get_sp sp1));
-    try fold (Val.addl (Vlong n) (get_sp sp2));
-    apply Val.addl_inject; auto.
-    apply Val.addl_inject; auto.
-    destruct sp1, sp2; simpl; auto;
-    inv H.
+  - destruct optR as [[]|]; auto; simpl.
+    rewrite Int64.add_zero_l; auto.
+    rewrite Int64.add_commut, Int64.add_zero_l; auto.
+  - destruct optR as [[]|]; auto; simpl;
+    eapply Val.addl_inject; auto.
   (* OEandil *)
   - inv H4; cbn; auto.
   (* OEoril *)