More general version of load preservation lemma.

Problem with the ptr bounds.

1 files changed, 25 insertions, 7 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 051fedb1..96cbf232 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -977,17 +977,27 @@ Qed.
 
 Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence).
 
-Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a:
-  match_internal n (State rs1 m1) (State rs2 m2) ->
-  exec_load lk chk f a rd rs1 m1 = Next rs1' m1' ->
-  exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2'.
+Lemma load_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (HLOAD: exec_load lk chk f a rd rs1 m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
 Proof.
   intros.
   unfold exec_load, Asm.exec_load in *.
-  inversion H as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
   rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
   destruct (Mem.loadv _ _ _).
-  + inversion H; auto. repeat (econstructor; eauto).
+  + inversion HLOAD; auto. repeat (econstructor; eauto).
+    * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto.
+      destruct (PregEq.eq r rd).
+      { subst. rewrite !Pregmap.gss; auto. }
+      { rewrite !Pregmap.gso; auto. }
+    * unfold Asm.nextinstr. rewrite Pregmap.gss. rewrite !Pregmap.gso; try congruence.
+      rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n).
+      rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite EQPC.
+      reflexivity. omega.
   + next_stuck_cong.
 Qed.
 
@@ -1003,8 +1013,11 @@ Proof.
   intros.
   destruct bi.
   2: {
-    simpl in*. destruct ld. 
+    simpl in*. destruct ld.
     { monadInv TRANSBI. destruct rd as [[r|]|]; try congruence. inversion EQ; subst.
+
+      (*exploit load_preserved; eauto.*)
+
       simpl in *. unfold exec_load, Asm.exec_load in *.
       inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
       rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
@@ -1019,6 +1032,11 @@ Proof.
     all:admit.
     
   } all:admit.
+(*rs1 # x <- v r = Asm.nextinstr rs2 # x <- v r*)
+   (*Next (Asm.nextinstr rs2 # x <- v) m1' = Next rs2' m2*)
+  (*rs1 # x <- v r =*)
+(*(rs2 # x <- v) # PC <- (Val.offset_ptr (rs2 # x <- v PC) Ptrofs.one) r*)
+
 Admitted.
 
 Lemma exec_body_simulation_star': forall