Progress in exec_basic_simu

- New ltacs
- simplifications
- new subcases
- two lemmas for nextinstr agree

1 files changed, 148 insertions, 104 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 8003b975..173ce8f8 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -977,6 +977,79 @@ Qed.
 
 Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence).
 
+Ltac inv_ok_eq :=
+  repeat match goal with
+  | [EQ: OK ?x = OK ?y |- _ ]
+      => inversion EQ; clear EQ; subst
+  end.
+
+Ltac reg_rwrt :=
+  match goal with
+  | [e: DR _ = DR _ |- _ ]
+      => rewrite e in *
+  end.
+
+Ltac destruct_reg_inv :=
+  repeat match goal with
+  | [ H : match ?reg with _ => _ end = _ |- _ ]
+      => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt
+  end.
+
+Ltac destruct_ireg_inv :=
+  repeat match goal with
+  | [ H : match ?reg with _ => _ end = _ |- _ ]
+      => destruct reg as [[r|]|]; try congruence; try inv_ok_eq; subst
+  end.
+
+Ltac destruct_reg_size :=
+  simpl in *;
+  match goal with
+  | [ |- context [ match ?reg with _ => _ end ] ]
+      => destruct reg; try congruence
+  end.
+
+Ltac find_rwrt_ag :=
+  simpl in *;
+  match goal with
+  | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ]
+      => repeat rewrite <- AG; try congruence
+  end.
+
+Ltac inv_matchi :=
+  match goal with
+  | [ MATCHI : match_internal _ _ _ |- _ ]
+      => inversion MATCHI; subst; find_rwrt_ag
+  end.
+
+Ltac destruct_ir0_reg :=
+  match goal with
+  | [ |- context [ ir0 _ _ ?r ] ]
+      => unfold ir0 in *; destruct r; find_rwrt_ag; eauto
+  end.
+
+Ltac update_x_access_x :=
+  subst; rewrite !Pregmap.gss; auto.
+
+Ltac update_x_access_r :=
+  rewrite !Pregmap.gso; auto.
+
+Lemma nextinstr_agree_but_pc rs1 rs2: forall
+  (AG: forall r, r <> PC -> rs1 r = rs2 r),
+  forall r, r <> PC -> rs1 r = Asm.nextinstr rs2 r.
+Proof.
+  intros; unfold Asm.nextinstr in *; rewrite Pregmap.gso in *; eauto.
+Qed.
+
+Lemma ptrofs_nextinstr_agree rs1 rs2 n: forall
+  (BOUNDED : 0 <= n <= Ptrofs.max_unsigned)
+  (AGPC : Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC),
+  Val.offset_ptr (rs1 PC) (Ptrofs.repr (n + 1)) = Asm.nextinstr rs2 PC.
+Proof.
+  intros; unfold Asm.nextinstr; rewrite Pregmap.gss.
+  rewrite <- Ptrofs.unsigned_one; rewrite <- (Ptrofs.unsigned_repr n); eauto;
+  rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto.
+Qed.
+
 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))
@@ -990,14 +1063,9 @@ Proof.
   rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
   destruct (Mem.loadv _ _ _).
   + 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.
+    * eapply nextinstr_agree_but_pc; intros.
+      destruct (PregEq.eq r rd); try update_x_access_x; try update_x_access_r.
+    * eapply ptrofs_nextinstr_agree; eauto.
   + next_stuck_cong.
 Qed.
 
@@ -1014,12 +1082,9 @@ Proof.
   rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
   destruct (Mem.storev _ _ _ _).
   + inversion HSTORE; auto. repeat (econstructor; eauto).
-    * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto.
+    * eapply nextinstr_agree_but_pc; intros.
       subst. apply EQR. auto.
-    * unfold Asm.nextinstr. rewrite Pregmap.gss.
-      rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n).
-      rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. subst. rewrite EQPC.
-      reflexivity. omega.
+    * eapply ptrofs_nextinstr_agree; subst; eauto.
   + next_stuck_cong.
 Qed.
 
@@ -1034,63 +1099,11 @@ 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.
+  * eapply nextinstr_agree_but_pc; intros.
+    destruct (PregEq.eq r x); try update_x_access_x; try update_x_access_r.
+  * eapply ptrofs_nextinstr_agree; eauto.
 Qed.
 
-Ltac inv_ok_eq :=
-  repeat match goal with
-  | [EQ: OK ?x = OK ?y |- _ ]
-      => inversion EQ; clear EQ; subst
-  end.
-
-Ltac reg_rwrt :=
-  match goal with
-  | [e: DR _ = DR _ |- _ ]
-      => rewrite e in *
-  end.
-
-Ltac destruct_reg_inv :=
-  repeat match goal with
-  | [ H : match ?reg with _ => _ end = _ |- _ ]
-      => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt
-  end.
-
-Ltac destruct_reg_size :=
-  simpl in *;
-  repeat match goal with
-  | [ |- context [ match ?reg with _ => _ end = _ ] ]
-      => destruct reg; try congruence
-  end.
-
-Ltac find_rwrt_ag :=
-  simpl in *;
-  match goal with
-  | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ]
-      => repeat rewrite <- AG; try congruence
-  end.
-
-Ltac inv_matchi :=
-  match goal with
-  | [ MATCHI : match_internal _ _ _ |- _ ]
-      => inversion MATCHI; subst; find_rwrt_ag
-  end.
-
-Ltac destruct_ir0_reg :=
-  match goal with
-  | [ |- context [ ir0 _ _ ?r ] ]
-      => unfold ir0 in *; destruct r; find_rwrt_ag; eauto
-  end.
-
-
 Lemma match_internal_nextinstr_switch:
   forall n s rs2 m2 r v,
   r <> PC ->
@@ -1099,12 +1112,9 @@ Lemma match_internal_nextinstr_switch:
 Proof.
   unfold Asm.nextinstr; intros n s rs2 m2 r v NOTPC1 MI.
   inversion MI; subst; constructor; auto.
-  - intros r' NOTPC2;
-    rewrite Pregmap.gso; try congruence.
+  - eapply nextinstr_agree_but_pc; intros.
     rewrite AG; try congruence.
-    destruct (PregEq.eq r r').
-    + subst. rewrite !Pregmap.gss; try congruence.
-    + rewrite !Pregmap.gso; try congruence.
+    destruct (PregEq.eq r r0); try update_x_access_x; try update_x_access_r.
   - rewrite !Pregmap.gss, !Pregmap.gso; try congruence.
     rewrite AGPC.
     rewrite Pregmap.gso, Pregmap.gss; try congruence.
@@ -1148,7 +1158,7 @@ Proof.
       try (destruct_reg_inv);
       try (inv_matchi);
       try (exploit next_inst_preserved; eauto);
-      try (destruct_reg_size).
+      try (repeat destruct_reg_size).
     + (* PArithPPP *)
       destruct i;
       try (monadInv TRANSBI);
@@ -1178,34 +1188,60 @@ Proof.
       try (destruct_reg_size);
       try (destruct_ir0_reg).
     + (* PArithComparisonPP *)
-      destruct i.
-      {
+      destruct i;
       try (monadInv TRANSBI);
       try (inv_matchi);
-      try (destruct_reg_inv).
-      simpl in *.
-      inversion BASIC; clear BASIC; subst.
-      eexists; eexists; split; eauto.
-      unfold compare_long.
-      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]).
-      econstructor; eauto.
-      * intros. unfold Asm.nextinstr.
-        rewrite Pregmap.gso; eauto.
-      * unfold Asm.nextinstr. rewrite Pregmap.gss.
-        rewrite <- Ptrofs.unsigned_one. rewrite <- (Ptrofs.unsigned_repr n); eauto.
-        rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite AGPC; eauto.
-      }
-
-
-
+      try (destruct_reg_inv);
+      simpl in *;
+      inversion BASIC; clear BASIC; subst;
+      eexists; eexists; split; eauto;
       unfold compare_long, compare_int, compare_float, compare_single;
-      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]).
-
+      try (destruct_reg_size);
+      try (destruct_reg_size);
+      try (destruct_reg_size);
+      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
+      try (econstructor; eauto);
+      try (eapply nextinstr_agree_but_pc; eauto);
+      try (eapply ptrofs_nextinstr_agree; eauto).
+      (* TODO find a solution to avoid destructing a lot of subcases *)
+           (** destruct sz.*)
+             (*{ [> Vsingle <]*)
+              (*try (exploit next_inst_preserved; eauto). intros.*)
+               (*destruct (rs1 x).*)
+               (*unfold Asm.nextinstr.*)
+               (*inversion MATCHI.*)
+             (*}*)
       all:admit.
     + (* PArithComparisonR0R *)
-      all:admit.
+      destruct i;
+      try (monadInv TRANSBI);
+      try (inv_matchi);
+      try (destruct_reg_inv);
+      try (destruct_reg_size);
+      simpl in *;
+      inversion BASIC; clear BASIC; subst;
+      eexists; eexists; split; eauto;
+      unfold compare_long, compare_int, compare_float, compare_single;
+      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
+      try (econstructor; eauto);
+      try (destruct_ir0_reg);
+      try (eapply nextinstr_agree_but_pc; eauto);
+      try (eapply ptrofs_nextinstr_agree; eauto).
     + (* PArithComparisonP *)
-      all:admit.
+      destruct i;
+      try (monadInv TRANSBI);
+      try (inv_matchi);
+      try (destruct_reg_inv);
+      try (destruct_reg_size);
+      simpl in *;
+      inversion BASIC; clear BASIC; subst;
+      eexists; eexists; split; eauto;
+      unfold compare_long, compare_int, compare_float, compare_single;
+      try (destruct_reg_size);
+      repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]);
+      try (econstructor; eauto);
+      try (eapply nextinstr_agree_but_pc; eauto);
+      try (eapply ptrofs_nextinstr_agree; eauto).
     + (* Pcset *)
       try (monadInv TRANSBI);
       try (inv_matchi);
@@ -1235,18 +1271,27 @@ Proof.
       try (exploit next_inst_preserved; eauto);
       try (find_rwrt_ag).
   - (* PLoad *)
-    destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto;
+    destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto;
     intros; simpl in *; destruct sz; eauto.
   - (* PStore *)
-    destruct st; monadInv TRANSBI; destruct r as [[r|]|]; try congruence; inversion EQ; subst; exploit store_preserved; eauto; simpl in *; inv_matchi; find_rwrt_ag.
+    destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto;
+    simpl in *; inv_matchi; find_rwrt_ag.
   - (* Pallocframe *)
     monadInv TRANSBI.
     simpl in *.
-    inversion MATCHI; subst.
-    destruct Mem.alloc.
-    inversion BASIC. repeat (econstructor; eauto).
-    unfold Asm.nextinstr. rewrite <- AG.
-    destruct (Mem.store _ _ _ _ _); try congruence; eauto.
+    inversion MATCHI; subst;
+    destruct Mem.alloc;
+    destruct Mem.store in BASIC;
+    inversion BASIC; subst; clear BASIC.
+    destruct Mem.store.
+    (* TODO find a way to complete this proof *)
+    + eexists; eexists; split; eauto.
+      repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]).
+      destruct (PregEq.eq SP PC); try (repeat congruence); discriminate.
+      -- admit.
+      -- eapply AG; destruct (PregEq.eq SP PC); try (repeat congruence); discriminate.
+    + repeat (econstructor; eauto).
+      admit.
       
     (* TODO *)
     all:admit.
@@ -1257,7 +1302,6 @@ Proof.
     try (monadInv TRANSBI);
     try (inv_matchi);
     try (exploit next_inst_preserved; eauto);
-    simpl in *;
     rewrite symbol_addresses_preserved; eauto.
   - (* Pcvtsw2x *)
     try (monadInv TRANSBI);