Optimizing Asmblockdeps proof

Proof is now two times faster (from 60 to 30 seconds)

1 files changed, 92 insertions, 58 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index a913313b..71b7c317 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -1224,18 +1224,6 @@ Proof.
   intros. congruence.
 Qed.
 
-(* Lemma sr_ireg_pos_ppos: forall (sr: state) r,
-  sr (ireg_to_pos r) = sr (# r).
-Proof.
-  intros. simpl. reflexivity.
-Qed.
-
-Lemma sr_freg_pos_ppos: forall (sr: state) r,
-  sr (freg_to_pos r) = sr (# r).
-Proof.
-  intros. simpl. reflexivity.
-Qed. *)
-
 Lemma ireg_pos_ppos: forall r,
   ireg_to_pos r = # r.
 Proof.
@@ -1314,6 +1302,49 @@ Proof.
   intros; destruct r; discriminate.
 Qed.
 
+Ltac DPRM pr :=
+  destruct pr as [drDPRF|crDPRF|]; 
+      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
+      | destruct crDPRF|].
+
+Ltac DPRF pr :=
+  destruct pr as [drDPRF|crDPRF|]; 
+      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|]
+      | destruct frDPRF]
+      | destruct crDPRF|].
+
+Lemma preg_not_pmem: forall r,
+  pmem <> # r.
+Proof.
+  intros. DPRF r; simpl; discriminate.
+Qed.
+
+Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
+
+Lemma dreg_not_CN: forall (r: dreg),
+  2 <> (#r).
+Proof.
+  intros; DIRN1 r; [ apply ireg_not_CN | discriminate | apply freg_not_CN].
+Qed.
+
+Lemma dreg_not_CZ: forall (r: dreg),
+  3 <> (#r).
+Proof.
+  intros; DIRN1 r; [ apply ireg_not_CZ | discriminate | apply freg_not_CZ].
+Qed.
+
+Lemma dreg_not_CC: forall (r: dreg),
+  4 <> (#r).
+Proof.
+  intros; DIRN1 r; [ apply ireg_not_CC | discriminate | apply freg_not_CC].
+Qed.
+
+Lemma dreg_not_CV: forall (r: dreg),
+  5 <> (#r).
+Proof.
+  intros; DIRN1 r; [ apply ireg_not_CV | discriminate | apply freg_not_CV].
+Qed.
+
 Lemma sr_update_both: forall sr rsr r1 rr v
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
   (sr <[ (#r1) <- Val (v) ]>) (#rr) =
@@ -1358,8 +1389,6 @@ Ltac replace_ppos :=
   try replace (7) with (#XSP) by eauto;
   try replace (24) with (#X16) by auto.
 
-Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl.
-
 Ltac DDRM dr :=
   destruct dr as [irsDDRF|frDDRF]; 
       [destruct irsDDRF
@@ -1370,17 +1399,6 @@ Ltac DDRM dr :=
       [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|]
       | destruct frDDRF]. *)
 
-Ltac DPRF pr :=
-  destruct pr as [drDPRF|crDPRF|]; 
-      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF as [irrDPRF|]; [destruct irrDPRF|]
-      | destruct frDPRF]
-      | destruct crDPRF|].
-
-Ltac DPRM pr :=
-  destruct pr as [drDPRF|crDPRF|]; 
-      [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |]
-      | destruct crDPRF|].
-
 (* Ltac DPRI pr :=
   destruct pr as [drDPRI|crDPRI|]; 
       [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|]
@@ -1399,6 +1417,10 @@ Ltac discriminate_ppos :=
   try apply freg_not_CZ;
   try apply freg_not_CC;
   try apply freg_not_CV;
+  try apply dreg_not_CN;
+  try apply dreg_not_CZ;
+  try apply dreg_not_CC;
+  try apply dreg_not_CV;
   try(simpl; discriminate).
 
 Ltac replace_pc := try replace (6) with (#PC) by eauto.
@@ -1581,10 +1603,11 @@ Proof.
     + (* OArithARRRR0 *) simpl; Simpl sr.
     + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); Simpl sr.
   - (* PArithComparisonPP *)
-    DIRN1 r2; DIRN1 r1; destruct i;
-    repeat Simpl_rep sr; Simpl_exists sr;
-    unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp;
-    simpl; intros rr; try destruct sz;
+    simpl; destruct i;
+    unfold arith_eval_comparison_pp, arith_prepare_comparison_pp; simpl;
+    fold (ppos r2); fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr;
+    Simpl sr;
+    try destruct sz;
     try (eapply compare_single_res; eauto);
     try (eapply compare_long_res; eauto);
     try (eapply compare_float_res; eauto).
@@ -1597,13 +1620,14 @@ Proof.
       try (eapply compare_long_res; eauto);
       try (eapply compare_int_res; eauto)).
   - (* PArithComparisonP *)
-    DIRN1 r1; destruct i;
-    repeat Simpl_rep sr; Simpl_exists sr;
-    unfold arith_eval_comparison_p; destruct arith_prepare_comparison_p;
-    simpl; try intros rr; try destruct sz;
+    simpl; destruct i;
+    unfold arith_eval_comparison_p, arith_prepare_comparison_p; simpl;
+    fold(ppos r1); try rewrite !H0; repeat Simpl_rep sr;
+    Simpl sr;
+    try destruct sz;
+    try (eapply compare_int_res; eauto);
     try (eapply compare_single_res; eauto);
     try (eapply compare_long_res; eauto);
-    try (eapply compare_int_res; eauto);
     try (eapply compare_float_res; eauto).
   - (* Pcset *)
     simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval;
@@ -1614,8 +1638,7 @@ Proof.
   - (* Pfmovi *)
     simpl; destruct r1; simpl; destruct fsz; Simpl sr.
   - (* Pcsel *)
-    simpl. destruct c; simpl;
-    DIRN1 r1; DIRN1 r2; Simpl_rep sr; DDRM rd; Simpl_exists sr; try intros rr; Simpl_update.
+    destruct c; simpl; DIRN1 rd; fold (ppos r2); fold (ppos r1); Simpl sr.
   - (* Pfnmul *)
     simpl; destruct fsz; Simpl sr.
 Qed.
@@ -1668,7 +1691,8 @@ Local Ltac preg_eq_discr r rd :=
         injection MEMAL2; intros Hm2 Hb2; try rewrite Hm2, Hb2;
         rewrite Hm, Hb; rewrite MEMS; reflexivity.
       * eauto.
-      * intros rr; DPRF rr; repeat Simpl_exists sr.
+      * intros rr. rewrite assign_diff; try apply preg_not_pmem; try rewrite sp_xsp.
+        replace 37 with (#X29) by auto; repeat (Simpl_update; intros).
     + simpl; repeat Simpl_exists sr. erewrite H. destruct (Mem.alloc _ _ _) eqn:HMEMAL2.
         injection MEMAL; intros Hm Hb. 
         try rewrite Hm, Hb; clear Hm Hb.
@@ -1679,7 +1703,10 @@ Local Ltac preg_eq_discr r rd :=
     + destruct (rsr SP) eqn:EQSP; simpl; rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD; try reflexivity.
       destruct (Mem.free _ _ _) eqn:EQFREE; try reflexivity. rewrite assign_diff; discriminate_ppos.
       replace_regs_pos sr; sr_val_rwrt. rewrite <- sp_xsp; rewrite EQSP; rewrite MLOAD. rewrite EQFREE.
-      Simpl_exists sr. intros rr; DPRF rr; repeat Simpl_exists sr.
+      replace 24 with (#X16) by auto; rewrite sp_xsp; Simpl sr.
+      intros rr'; destruct (PregEq.eq XSP rr').
+      * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
+      * rewrite Pregmap.gso, !assign_diff; auto; apply ppos_discr in n; auto.
     + rewrite <- sp_xsp; rewrite MLOAD; reflexivity.
 Qed.
 
@@ -1778,27 +1805,34 @@ Proof.
     replace_pc. rewrite (H0 PC).
     unfold control_eval. destruct Ge. simpl. unfold incrPC.
     try (eexists; split; [  | split ]); eauto.
-    intros rr; DPRF rr; Simpl_update.
-    68: rewrite sr_gss, Pregmap.gss;
-        try rewrite Pregmap.gso; discriminate_ppos; fold (ppos r); rewrite H0; auto.
-    all: repeat Simpl_rep sr; rewrite !Pregmap.gso; discriminate_ppos; auto.
+    intros rr; destruct (PregEq.eq PC rr).
+    + replace_pc; rewrite e; rewrite !Pregmap.gss, !sr_gss;
+      rewrite Pregmap.gso; fold (ppos r); try rewrite H0; auto.
+      rewrite <- e; destruct r; discriminate.
+    + replace_pc; rewrite Pregmap.gso, assign_diff; auto; apply ppos_discr in n; auto;
+      rewrite Pregmap.gss, sr_gss. destruct (PregEq.eq X30 rr); replace 38 with (#X30) by auto.
+      * rewrite e; rewrite Pregmap.gss, sr_gss; auto.
+      * replace_pc; rewrite !Pregmap.gso, !assign_diff; auto; apply ppos_discr in n0; auto;
+        apply ppos_discr; eauto.
   - (* Obtbl *)
-    replace_pc. rewrite (H0 PC).
-    unfold control_eval. destruct Ge. simpl. unfold incrPC.
-    destruct r1.
-    17: rewrite Pregmap.gss, sr_gss; try reflexivity.
-    all: rewrite !Pregmap.gso, !assign_diff; discriminate_ppos;
-    rewrite ireg_pos_ppos; try erewrite H0; destruct (rsr _);
-    try destruct (list_nth_z _ _); try reflexivity;
-    unfold goto_label, goto_label_deps; destruct (label_pos _ _ _);
-    try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz));
-    try reflexivity; discriminate_ppos; simpl; Simpl_exists sr;
-    intros rr;
-    destruct (PregEq.eq X16 rr); [ subst; Simpl_update |];
-    destruct (PregEq.eq X17 rr); [ subst; Simpl_update |];
-    destruct (PregEq.eq PC rr); [ subst; Simpl_update |];
-    rewrite !Pregmap.gso; auto; apply ppos_discr in n; apply ppos_discr in n0; apply ppos_discr in n1;
-    simpl in *;repeat Simpl_rep sr; auto.
+    replace_pc; rewrite (H0 PC);
+    unfold control_eval; destruct Ge; simpl; unfold incrPC.
+    destruct (PregEq.eq X16 r1).
+    + fold (ppos r1); rewrite <- e; rewrite Pregmap.gss, sr_gss; reflexivity.
+    + rewrite !Pregmap.gso; auto; rewrite ppos_discr in n;
+      fold (ppos r1); replace 24 with (#X16) by auto; try rewrite !assign_diff; auto;
+      discriminate_ppos; rewrite H0; destruct (rsr r1) eqn:EQR;
+      try (try rewrite EQR; reflexivity).
+      try destruct (list_nth_z _ _); try reflexivity;
+      unfold goto_label, goto_label_deps; destruct (label_pos _ _ _);
+      try rewrite 2Pregmap.gso, Pregmap.gss; destruct (Val.offset_ptr (rsr PC) (Ptrofs.repr sz));
+      try reflexivity; discriminate_ppos. Simpl sr.
+      destruct (PregEq.eq X16 rr); [ subst; Simpl_update |];
+      destruct (PregEq.eq X17 rr); [ subst; Simpl_update |];
+      destruct (PregEq.eq PC rr); [ subst; Simpl_update |].
+      rewrite !Pregmap.gso; auto;
+      apply ppos_discr in n0; apply ppos_discr in n1; apply ppos_discr in n2;
+      rewrite !assign_diff; auto.
 Qed.
 
 Theorem bisimu_exit ex sz rsr mr sr: