Preuves du branchement avec des float

1 files changed, 242 insertions, 25 deletions

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index b3519064..060f1a85 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -222,8 +222,6 @@ Qed.
 *)
 *)
 
-Definition yolo := 4.
-
 Lemma opimm64_correct:
   forall (op: arith_name_rrr)
          (opi: arith_name_rri64)
@@ -427,6 +425,22 @@ Proof.
     rewrite H0. simpl; auto.
 Qed.
 
+Lemma swap_comparison_cmpf_eq:
+  forall v1 v2 cmp,
+  (Val.cmpf cmp v1 v2) = (Val.cmpf (swap_comparison cmp) v2 v1).
+Proof.
+  intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto.
+  rewrite Float.cmp_swap. auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
+
 Lemma transl_compf_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
   exists rs',
@@ -436,26 +450,80 @@ Lemma transl_compf_correct:
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
-Proof. Admitted.
-(*   intros. esplit. split.
-- unfold transl_compl. apply exec_straight_one; simpl; eauto.
-- split.
-  + intros; Simpl.
-  + intros.
-    remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'.
-    simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
-    { 
-      assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)).
-      { rewrite Heqrs'. auto. }
-      rewrite H0. rewrite <- H.
-      remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool.
-      destruct cmp; simpl;
-      unfold compare_long;
-      unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
-      destruct b0; simpl; auto.
-    }
-    rewrite H0. simpl; auto.
-Qed. *)
+Proof.
+  intros. unfold transl_comp_float64. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma cmpf_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpf_bool Cne v1 v2 = option_map negb (Val.cmpf_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpf_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpf_bool Ceq v1 v2 = option_map negb (Val.cmpf_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma option_map_negb_negb:
+  forall v,
+  option_map negb (option_map negb v) = v.
+Proof.
+  destruct v; simpl; auto. rewrite negb_involutive. reflexivity.
+Qed.
+
+Lemma notbool_option_map_negb:
+  forall v, Val.notbool (Val.of_optbool v) = Val.of_optbool (option_map negb v).
+Proof.
+  unfold Val.notbool. unfold Val.of_optbool.
+  destruct v; auto. destruct b; auto.
+Qed.
+
+Lemma swap_comparison_cmpf_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpf_bool cmp v1 v2 = Val.cmpf_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. rewrite Float.cmp_swap. reflexivity.
+Qed.
 
 Lemma transl_compnotf_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
@@ -466,7 +534,56 @@ Lemma transl_compnotf_correct:
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
-Proof. Admitted.
+Proof.
+  intros. unfold transl_comp_notfloat64. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT.
+          * rewrite cmpf_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpf_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_float _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_float ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpf_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpf_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_float;
+          unfold Val.cmpf; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool:
+  forall cmp ft v1 v2,
+  ftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
 
 Lemma transl_compfs_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
@@ -477,7 +594,66 @@ Lemma transl_compfs_correct:
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
-Proof. Admitted.
+Proof.
+  intros. unfold transl_comp_float32. destruct (ftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto;
+          destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
+
+Lemma swap_comparison_cmpfs_bool_notftest:
+  forall cmp ft v1 v2,
+  notftest_for_cmp cmp = Reversed ft ->
+  Val.cmpfs_bool cmp v1 v2 = Val.cmpfs_bool (swap_comparison cmp) v2 v1.
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_swap. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq:
+  forall v1 v2,
+  Val.cmpfs_bool Cne v1 v2 = option_map negb (Val.cmpfs_bool Ceq v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. reflexivity.
+Qed.
+
+Lemma cmpfs_bool_ne_eq_rev:
+  forall v1 v2,
+  Val.cmpfs_bool Ceq v1 v2 = option_map negb (Val.cmpfs_bool Cne v1 v2).
+Proof.
+  intros. unfold Val.cmpfs_bool. destruct v1; destruct v2; auto. rewrite Float32.cmp_ne_eq. simpl. rewrite negb_involutive. reflexivity.
+Qed.
 
 Lemma transl_compnotfs_correct:
   forall cmp r1 r2 lbl k rs m tbb b,
@@ -488,7 +664,48 @@ Lemma transl_compnotfs_correct:
        exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m
         = eval_branch fn lbl (nextblock tbb rs') m (Some b))
   .
-Proof. Admitted.
+Proof.
+  intros. unfold transl_comp_notfloat32. destruct (notftest_for_cmp cmp) eqn:FT.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r1) (rs r2))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2)) as cmpbool.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT.
+          * rewrite cmpfs_bool_ne_eq; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite cmpfs_bool_ne_eq_rev. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+  * esplit. split.
+    - apply exec_straight_one; simpl; eauto.
+    - split.
+      + intros; Simpl.
+      + intros. remember (rs # RTMP <- (compare_single _ _ _)) as rs'.
+        simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b).
+        { 
+          assert ((nextblock tbb rs') # RTMP = (compare_single ft (rs r2) (rs r1))).
+          { rewrite Heqrs'. auto. }
+          rewrite H0. rewrite <- H.
+          remember (Val.cmpfs_bool cmp rs#r1 rs#r2) as cmpbool.
+          erewrite swap_comparison_cmpfs_bool_notftest in Heqcmpbool; eauto.
+          destruct cmp; simpl;
+          unfold compare_single;
+          unfold Val.cmpfs; simpl in FT; inversion FT; simpl in Heqcmpbool.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+          * rewrite notbool_option_map_negb. rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto.
+        }
+        rewrite H0. simpl; auto.
+Qed.
 
 Lemma transl_complu_correct:
   forall cmp r1 r2 lbl k rs m tbb b,