Preuve des load/store registre registre. Reste des modifs mineures dans les preuves de Asmblockdeps

6 files changed, 196 insertions, 77 deletions

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 9d7b372e..408b8c31 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -1262,44 +1262,34 @@ Definition eval_offset (ofs: offset) : res ptrofs :=
       end
   end.
 
-Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
-                     (d: ireg) (a: ireg) (ptr: ptrofs) :=
-  match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
-  | None => Stuck
-  | Some v => Next (rs#d <- v) m
-  end
-.
-
 Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
   match (eval_offset ofs) with
-  | OK ptr => exec_load chunk rs m d a ptr
+  | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
+              | None => Stuck
+              | Some v => Next (rs#d <- v) m
+              end
   | _ => Stuck
   end.
 
 Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
-  match (rs ro) with
-  | Vptr _ ofs => exec_load chunk rs m d a ofs
-  | _ => Stuck
-  end.
-
-Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
-                      (s: ireg) (a: ireg) (ptr: ptrofs) :=
-  match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
+  match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
   | None => Stuck
-  | Some m' => Next rs m'
-  end
-.
+  | Some v => Next (rs#d <- v) m
+  end.
 
 Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
   match (eval_offset ofs) with
-  | OK ptr => exec_store chunk rs m s a ptr
+  | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
+              | None => Stuck
+              | Some m' => Next rs m'
+              end
   | _ => Stuck
   end.
 
 Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
-  match (rs ro) with
-  | Vptr _ ofs => exec_store chunk rs m s a ofs
-  | _ => Stuck
+  match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
+  | None => Stuck
+  | Some m' => Next rs m'
   end.
 
 Definition load_chunk n :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index e038a5ae..ac8fa6bd 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -831,7 +831,8 @@ Proof.
   - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto.
 
 (* Load *)
-  - simpl in H. destruct i.
+  - simpl in H. admit.
+  (* destruct i.
   (* Load Offset *)
     + destruct i. all:
       unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_load in H;
@@ -848,10 +849,11 @@ Proof.
         simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; rewrite ROFS;
         unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity
       | Simpl
-      | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+      | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. *)
 
 (* Store *)
-  - simpl in H. destruct i.
+  - simpl in H. admit.
+  (* destruct i.
   (* Store Offset *)
     + destruct i. all:
       unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_store in H;
@@ -869,7 +871,7 @@ Proof.
         unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity
       | Simpl
       | intros rr; destruct rr; Simpl ].
-
+ *)
 (* Allocframe *)
   - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate.
     inv H. inv H0. eexists. split; try split.
@@ -895,7 +897,7 @@ Proof.
     eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
 (* Pnop *)
   - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption.
-Qed.
+Admitted.
 
 Lemma forward_simu_body:
   forall bdy ge rs m rs' m' fn s,
@@ -1211,23 +1213,23 @@ Proof.
   (* Load Offset *)
     + destruct i. all:
     simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto;
-    unfold exec_load in H0; unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate.
+    unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate.
   (* Load Reg *)
-    + destruct i. all:
+    + admit. (* destruct i. all:
     simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg;
-    destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate.
+    destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate. *)
 
 (* PStore *)
   - destruct i.
   (* Store Offset *)
     + destruct i. all:
     simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto;
-    unfold exec_store in H0; simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate.
+    simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate.
   (* Store Reg *)
-    + destruct i. all:
+    + admit. (* destruct i. all:
     simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0;
     unfold exec_store_deps_reg; destruct (rs rofs); auto; unfold exec_store in H0; unfold exec_store_deps;
-    destruct (Mem.storev _ _ _ _); auto; discriminate.
+    destruct (Mem.storev _ _ _ _); auto; discriminate. *)
 
 (* Pallocframe *)
   - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0.
@@ -1241,7 +1243,7 @@ Proof.
     all: simpl; auto.
   - simpl. destruct rd; subst; try discriminate.
     all: simpl; auto.
-Qed.
+Admitted.
 
 Lemma forward_simu_body_stuck:
   forall bdy ge fn rs m s,
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 81474d30..70f188ec 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -1185,7 +1185,7 @@ Local Transparent destroyed_by_op.
     exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1.

     intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.

     exploit Mem.loadv_extends; eauto. intros [v' [C D]].

-    exploit transl_load_correct; eauto. admit.

+    exploit transl_load_correct; eauto.

     intros [rs2 [P [Q R]]].

 

     eapply exec_straight_body in P.

@@ -1212,7 +1212,7 @@ Local Transparent destroyed_by_op.
     intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A.

     assert (Val.lessdef (ms src) (rs1 (preg_of src))). eapply preg_val; eauto.

     exploit Mem.storev_extends; eauto. intros [m2' [C D]].

-    exploit transl_store_correct; eauto. admit. intros [rs2 [P Q]].

+    exploit transl_store_correct; eauto. intros [rs2 [P Q]].

 

     eapply exec_straight_body in P.

       2: eapply code_to_basics_id; eauto.

@@ -1227,7 +1227,7 @@ Local Transparent destroyed_by_op.
 

     eapply agree_undef_regs; eauto with asmgen.

     simpl; congruence.

-Admitted.

+Qed.

 

 Lemma exec_body_trans:

   forall l l' rs0 m0 rs1 m1 rs2 m2,

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 220f631e..5ccea246 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1749,7 +1749,7 @@ Proof.
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
-  unfold exec_load_offset. rewrite PtrEq. unfold exec_load. rewrite B, LOAD. eauto. Simpl. 
+  unfold exec_load_offset. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl. 
   split; intros; Simpl. auto.
 Qed.
 
@@ -1769,7 +1769,7 @@ Proof.
   intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
-  unfold exec_store_offset. rewrite PtrEq. unfold exec_store. rewrite B, C, STORE.
+  unfold exec_store_offset. rewrite PtrEq. rewrite B, C, STORE.
     eauto.
     discriminate.
     { intro. inv H. contradiction. }
@@ -1913,11 +1913,29 @@ Proof.
   inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
 Qed.
 
-Lemma transl_load_access_correct:
-  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
-  (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
-  transl_memory_access mk_instr addr args k = OK c ->
+Lemma transl_memory_access2_correct:
+  forall mk_instr addr args k c (rs: regset) m v,
+  transl_memory_access2 mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  exists base ro mro mr1 rs',
+     args = mr1 :: mro :: nil
+  /\ ireg_of mro = OK ro
+  /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
+  /\ Val.addl rs'#base rs'#ro = v
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until v; intros TR EV. 
+  unfold transl_memory_access2 in TR; destruct addr; ArgsInv.
+  inv EV. repeat eexists. eassumption. econstructor; eauto.
+Qed.
+
+Lemma transl_load_access2_correct:
+  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro) ->
+  transl_memory_access2 mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
   Mem.loadv chunk m v = Some v' ->
   exists rs',
@@ -1925,35 +1943,34 @@ Lemma transl_load_access_correct:
   /\ rs'#rd = v'
   /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros until v'; intros INSTR TR EV LOAD. 
-  exploit transl_memory_access_correct; eauto.
-  intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
+  intros until v'; intros ARGS IREGE INSTR TR EV LOAD. 
+  exploit transl_memory_access2_correct; eauto.
+  intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
   econstructor; split.
-  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
-  rewrite INSTR. unfold exec_load_offset. unfold exec_load. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_load_reg. rewrite B, LOAD. reflexivity. Simpl. 
   split; intros; Simpl. auto.
 Qed.
 
-Lemma transl_store_access_correct:
-  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
+Lemma transl_load_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
   (forall base ofs rs,
-     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
   transl_memory_access mk_instr addr args k = OK c ->
   eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
-  Mem.storev chunk m v rs#r1 = Some m' ->
-  r1 <> RTMP ->
+  Mem.loadv chunk m v = Some v' ->
   exists rs',
-     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
-  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+  /\ rs'#rd = v'
+  /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
 Proof.
-  intros until m'; intros INSTR TR EV STORE NOT31. 
+  intros until v'; intros INSTR TR EV LOAD. 
   exploit transl_memory_access_correct; eauto.
   intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
   econstructor; split.
   eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
-  rewrite INSTR. unfold exec_store_offset. unfold exec_store. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
-  intro. inv H. contradiction.
-  auto.
+  rewrite INSTR. unfold exec_load_offset. rewrite PtrEq, B, LOAD. reflexivity. Simpl. 
+  split; intros; Simpl. auto.
 Qed.
 
 Lemma transl_load_memory_access_ok:
@@ -1979,6 +1996,28 @@ Proof.
     | eauto ].
 Qed.
 
+Lemma transl_load_memory_access2_ok:
+  forall addr chunk args dst k c rs a v m,
+  addr = Aindexed2 ->
+  transl_load chunk addr args dst k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.loadv chunk m a = Some v ->
+  exists mk_instr mr0 mro rd ro,
+      args = mr0 :: mro :: nil
+   /\ preg_of dst = IR rd
+   /\ preg_of mro = IR ro
+   /\ transl_memory_access2 mk_instr addr args k = OK c
+   /\ forall base rs,
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro.
+Proof.
+  intros until m. intros ? TR ? ?.
+  unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; reflexivity
+  | eauto].
+Qed.
+
 Lemma transl_load_correct:
   forall chunk addr args dst k c (rs: regset) m a v,
   transl_load chunk addr args dst k = OK c ->
@@ -1993,20 +2032,68 @@ Proof.
   2-4: exploit transl_load_memory_access_ok; eauto; try discriminate;
     intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
     eapply transl_load_access_correct; eauto with asmgen.
-  admit.
-Admitted.
+  - exploit transl_load_memory_access2_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+    rewrite rdEq. eapply transl_load_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+Qed.
+
+Lemma transl_store_access2_correct:
+  forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk rs m r1 base ro) ->
+  transl_memory_access2 mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  Mem.storev chunk m v rs#r1 = Some m' ->
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access2_correct; eauto.
+  intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
+Lemma transl_store_access_correct:
+  forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
+  (forall base ofs rs,
+     exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
+  transl_memory_access mk_instr addr args k = OK c ->
+  eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+  Mem.storev chunk m v rs#r1 = Some m' ->
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access_correct; eauto.
+  intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. 
+  rewrite INSTR. unfold exec_store_offset. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
 
 Remark exec_store_offset_8_sign rs m x base ofs:
   exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold exec_store. unfold Mem.storev.
+  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
   destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity.
 Qed.
 
 Remark exec_store_offset_16_sign rs m x base ofs:
   exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs.
 Proof.
-  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold exec_store. unfold Mem.storev.
+  unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
   destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity.
 Qed.
 
@@ -2045,6 +2132,45 @@ Proof.
     eapply exec_store_offset_16_sign.
 Qed.
 
+Remark exec_store_reg_8_sign rs m x base ofs:
+  exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs.
+Proof.
+  unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_reg_16_sign rs m x base ofs:
+  exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs.
+Proof.
+  unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Lemma transl_store_memory_access2_ok:
+  forall addr chunk args src k c rs a m m',
+  addr = Aindexed2 ->
+  transl_store chunk addr args src k = OK c ->
+  eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists mk_instr chunk' rr mr0 mro ro,
+     args = mr0 :: mro :: nil
+  /\ preg_of mro = IR ro
+  /\ preg_of src = IR rr
+  /\ transl_memory_access2 mk_instr addr args k = OK c
+  /\ (forall base rs,
+       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk' rs m rr base ro)
+  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+  intros until m'. intros ? TR ? ?.
+  unfold transl_store in TR. subst addr. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ ArgsInv; reflexivity
+  | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRR _ x)); simpl; reflexivity
+  | eauto ].
+  - simpl. intros. eapply exec_store_reg_8_sign.
+  - simpl. intros. eapply exec_store_reg_16_sign.
+Qed.
+
 Lemma transl_store_correct:
   forall chunk addr args src k c (rs: regset) m a m',
   transl_store chunk addr args src k = OK c ->
@@ -2060,8 +2186,10 @@ Proof.
     rewrite D in STORE; clear D; 
     eapply transl_store_access_correct; eauto with asmgen; try congruence;
     destruct rr; try discriminate; destruct src; try discriminate.
-  admit.
-Admitted.
+  - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+    eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
+Qed.
 
 Lemma make_epilogue_correct:
   forall ge0 f m stk soff cs m' ms rs k tm,
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 77014bdc..c5f432a6 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -100,7 +100,7 @@ Lemma exec_load_offset_pc_var:
   exec_load_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_offset in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+  intros. unfold exec_load_offset in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -111,7 +111,7 @@ Lemma exec_load_reg_pc_var:
   exec_load_reg t rs m rd ra ro = Next rs' m' ->
   exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_load_reg in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (rs ro); try discriminate.
+  intros. unfold exec_load_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.loadv _ _ _).
   - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
   - discriminate.
@@ -122,7 +122,7 @@ Lemma exec_store_offset_pc_var:
   exec_store_offset ge t rs m rd ra ofs = Next rs' m' ->
   exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_offset in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate.
+  intros. unfold exec_store_offset in *. rewrite Pregmap.gso; try discriminate.
   destruct (eval_offset ge ofs); try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
@@ -134,8 +134,7 @@ Lemma exec_store_reg_pc_var:
   exec_store_reg t rs m rd ra ro = Next rs' m' ->
   exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
 Proof.
-  intros. unfold exec_store_reg in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate.
-  destruct (rs ro); try discriminate.
+  intros. unfold exec_store_reg in *. rewrite Pregmap.gso; try discriminate.
   destruct (Mem.storev _ _ _).
   - inv H. apply next_eq; auto.
   - discriminate.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index ed8edfde..d0e05389 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -943,10 +943,10 @@ Lemma exec_basic_instr_pc:
 Proof.
   intros. destruct b; try destruct i; try destruct i.
   all: try (inv H; Simpl).
-  1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_load_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
-  1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
-  1-10: try (unfold exec_store_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+  1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold exec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+  1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
+  1-10: try (unfold exec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
   - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
     destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.