Start of the postpasschedproof, redefining verify schedule lemmas

1 files changed, 42 insertions, 36 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index ef7f803d..23cdf1ab 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -2232,28 +2232,6 @@ Proof.
   * discriminate.
 Qed.
 
-Lemma incrPC_set_res_commut res: forall d vres rs,  
-  incrPC d (set_res (map_builtin_res DR res) vres rs) =
-  set_res (map_builtin_res DR res) vres (incrPC d rs).
-Proof.
-  induction res; simpl; auto.
-  - intros; apply functional_extensionality.
-    unfold incrPC; intros x0.
-    destruct (PregEq.eq x0 PC).
-    + subst; rewrite! Pregmap.gss; auto.
-    + rewrite Pregmap.gso; auto.
-      destruct (PregEq.eq x x0).
-      * subst; rewrite! Pregmap.gss; auto.
-      * rewrite !Pregmap.gso; auto.
-  - intros; rewrite IHres2. f_equal. auto.
-Qed.
-
-Lemma incrPC_undef_regs_commut l : forall d rs,
-  incrPC d (undef_regs (map preg_of l) rs) = undef_regs (map preg_of l) (incrPC d rs).
-Proof.
-  induction l; simpl; auto.
-Admitted.
-
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
@@ -2280,7 +2258,7 @@ Proof.
     inversion H4. econstructor. }
     { inversion H2; subst.
       destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
-    intros H4. eexists; eexists; split; try reflexivity.
+intros H4. eexists; eexists; split; try reflexivity.
     destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
     inversion H4. rewrite H3. econstructor. }
   - (* Builtin *)
@@ -2297,18 +2275,46 @@ Proof.
     destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
     intros H4. eexists; eexists; split; try reflexivity.
     inversion H2; subst. inversion H4; subst.
-    assert (EQ: forall r, r<>PC -> rs1 r = rs2 r).
-    { unfold incrPC in H5. intros x H; replace (rs1 x) with ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1)))) x).
-      + rewrite H5; rewrite Pregmap.gso; auto.
-      + rewrite Pregmap.gso; auto.
-    }
-   econstructor; eauto.
-    + rewrite <- (EQ SP); try discriminate.
+    econstructor; eauto.
+    + unfold incrPC in H5.
+      replace (rs2 SP) with (rs1 SP).
       replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto.
-      apply functional_extensionality.
-      intros; apply EQ; try discriminate. 
-    + rewrite !incrPC_set_res_commut, !incrPC_undef_regs_commut; rewrite H5. auto.
-Qed.
+      * apply functional_extensionality.
+        intros r; destruct (PregEq.eq r PC); try discriminate.
+        replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto.
+        rewrite H5; rewrite Pregmap.gso; auto.
+      * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto.
+        rewrite H5; rewrite Pregmap.gso; auto; try discriminate.
+    + admit.
+    
+(*  generalize (H0 (trans_state (State rs m))); clear H0.
+  intros H0 m' t0 (rs1 & m1 & H1 & H2).
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
+  exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
+  unfold bbstep, estep.
+  rewrite H1; simpl.
+  unfold has_builtin in BLT.
+  destruct (exit p1) eqn:EQEX1. destruct c.
+  - inversion H2; subst.
+    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|] eqn:EQBDY2; try congruence.
+    unfold trans_block, exec in *.
+    exploit (bisimu_body); eauto. erewrite H1. simpl.
+    (*destruct (exec_body _ _ (body p2) _ _) eqn:EQBDY1.*)
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 rs m); try (unfold Stuck in EBB; congruence).
+  intros H1 (s2' & exp2 & MS'). unfold exec in exp2, H1. rewrite exp2 in H0.
+  destruct H0 as (m2' & H0 & H2). discriminate. rewrite H0 in H1.
+  destruct (bbstep Ge.(_lk) Ge.(_genv) Ge.(_fn) p2 rs m); simpl in H1.
+  * unfold match_states in H1, MS'. destruct s, s0.
+    destruct H1 as (s' & H1 & H3 & H4). inv H1. inv MS'.
+    replace (_rs0) with (_rs).
+    - replace (_m0) with (_m); auto. congruence.
+    - apply functional_extensionality. intros r.
+      generalize (H1 r). intros Hr. congruence.
+  * discriminate.*)
+
+Admitted.
+  
+(*Qed.*)
 
 (** Used for debug traces *)
 
@@ -2717,8 +2723,8 @@ Theorem bblock_simu_test_correct verb p1 p2 :
   WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2.
 Proof.
   wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto.
-Qed.
-(*Qed.*)
+  Admitted.
+(* Qed. *)
 Hint Resolve bblock_simu_test_correct: wlp.
 
 (** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *)