Adding a lemma next_instr_preserved

this is useful in the exec_basic_simu proof

1 files changed, 56 insertions, 7 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 07d1dffb..4851da90 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1001,6 +1001,41 @@ Proof.
   + next_stuck_cong.
 Qed.
 
+Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (NEXTI: Next rs1 # x <- v m1 = Next rs1' m1'),
+  exists (rs2' : regset) (m2' : mem),
+  Next (Asm.nextinstr rs2 # x <- v) m2 = Next rs2' m2'
+  /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2').
+Proof.
+  intros.
+  inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
+  inversion NEXTI. repeat (econstructor; eauto).
+  * intros. unfold Asm.nextinstr.
+    rewrite (Pregmap.gso (i := PC) (j := x)); try congruence.
+    rewrite (Pregmap.gso (i := r) (j := PC)); try congruence.
+    destruct (PregEq.eq r x).
+    { subst. rewrite !Pregmap.gss; auto. }
+    { rewrite !Pregmap.gso; try congruence. auto. }
+  * unfold Asm.nextinstr.
+    rewrite Pregmap.gss. rewrite !(Pregmap.gso (i := PC) (j := x)); try congruence.
+    rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto.
+    rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite EQPC; eauto.
+Qed.
+
+(*Lemma arithp_preserved n rs1 m1 rs2 m2 rs2' rd i tf v: forall
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
+  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
+  (rd': type_reg (arithp_args_type i))
+  (NEXTI: reg_of_preg (arithp_args_type i) rd = OK rd')
+  (RS2P: (Asm.nextinstr rs2 # rd <- v) = rs2')
+  (HV: (arith_eval_p lk i) = v),
+  Asm.exec_instr tge tf (arithp_to_instruction i rd') rs2 m2 = Next rs2' m2
+  /\ match_internal (n + 1) (State (rs1 # rd <- v) m1) (State rs2' m2).
+Proof.
+Admitted.*)
+
 Lemma exec_basic_simulation:
   forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
@@ -1014,17 +1049,31 @@ Proof.
   intros.
   destruct bi.
   - (* PArith *)
-    simpl in *. repeat destruct i. monadInv TRANSBI. destruct rd as [[r|]|]; try congruence.inversion EQ; subst. simpl in *.
-
-    inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-    unfold Asm.nextinstr. rewrite (Pregmap.gso (i := PC) (j := x)); try congruence.
-    
-    rewrite <- EQPC.
-
+    simpl in *; destruct i.
+    + (* Padrp *)
+      destruct i; monadInv TRANSBI;
+      destruct rd as [[r|]|]; try congruence; inversion EQ; subst;
+      exploit next_inst_preserved; eauto;
+      intros; simpl in *; try destruct sz; eauto.
+    + (* Pmovz *)
+      destruct i;
+      try ( destruct sumbool_rec; try congruence);
+      try (monadInv TRANSBI; simpl in *; destruct rd; try congruence; inversion EQ; subst;
+      try (destruct i; try congruence; inversion EQ; subst; rewrite e in *);
+      try (destruct rs; try congruence; inversion EQ1; subst);
+      try (inversion MATCHI; subst; rewrite <- AG; try congruence);
+      exploit next_inst_preserved; eauto).
+      try (intros; simpl in *; try destruct sz; eauto).
+      (*intros; simpl in *; try destruct sz; eauto.*)
+            
+      all:admit.
     all:admit.
+
+  (*
   - (* PLoad *)
     simpl in*. destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto;
     intros; simpl in *; destruct sz; eauto.
+  *)
 Admitted.
 
 Lemma exec_body_simulation_star': forall