step1 expression is ok

1 files changed, 36 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 38eb6c1b..2c6a49c5 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2320,3 +2320,39 @@ Proof.
   rewrite Int64.repr_unsigned.
   reflexivity.
 Qed.
+
+Open Scope cminorsel_scope.
+Definition e_invfs a := Eop Oinvfs (a ::: Enil).
+Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil).
+Definition e_single_of_longu a := Eop Osingleoflongu (a ::: Enil).
+Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil).
+Definition e_longu_of_float_ne a := Eop Olonguoffloat_ne (a ::: Enil).
+Definition e_mulf a b := Eop Omulf (a ::: b ::: Enil).
+
+Definition a_var1 := Eletvar (4%nat).
+Definition a_d_var1 := Eletvar (3%nat).
+Definition b_var1 := Eletvar (2%nat).
+Definition b_d_var1 := Eletvar (1%nat).
+Definition binv_d_var1 := Eletvar (0%nat).
+
+Definition e_setup1 a b rest :=
+  Elet a (Elet (e_float_of_longu (Eletvar 0%nat))
+    (Elet (lift (lift b)) (Elet (e_float_of_longu (Eletvar 0%nat))
+      (Elet (e_float_of_single (e_invfs (e_single_of_longu (Eletvar 1%nat))))
+      rest)))).                  
+Definition e_step1 := e_longu_of_float_ne (e_mulf a_d_var1 binv_d_var1).
+
+Lemma e_step1_correct :
+  forall (ge : genv)  (sp: val) cmenv memenv (le : letenv)
+         (expr_a : expr) (a : int64) (EVAL_a : eval_expr ge sp cmenv memenv le expr_a (Vlong a))
+         (expr_b : expr) (b : int64) (EVAL_b : eval_expr ge sp cmenv memenv le expr_b (Vlong b)),
+         (eval_expr ge sp cmenv memenv le (e_setup1 expr_a expr_b (e_step1))
+                    (step1_div_longu (Vlong a) (Vlong b))).           
+Proof.
+  intros.
+  unfold e_setup1, step1_div_longu.
+  repeat econstructor.
+  { eassumption. }
+  { cbn. apply eval_lift. apply eval_lift. eassumption. }
+Qed.
+