progress

1 files changed, 36 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 2c6a49c5..619fcfa6 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2324,11 +2324,15 @@ 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_float_of_long a := Eop Ofloatoflong (a ::: Enil).
 Definition e_single_of_longu a := Eop Osingleoflongu (a ::: Enil).
 Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil).
+Definition e_long_of_float_ne a := Eop Olongoffloat_ne (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 e_float_const c := Eop (Ofloatconst c) Enil.
+Definition e_fmaddf a b c := Eop Ofmaddf (a ::: b ::: c ::: Enil).
+Definition e_fmsubf a b c := Eop Ofmsubf (a ::: b ::: c ::: Enil).
 Definition a_var1 := Eletvar (4%nat).
 Definition a_d_var1 := Eletvar (3%nat).
 Definition b_var1 := Eletvar (2%nat).
@@ -2355,4 +2359,34 @@ Proof.
   { eassumption. }
   { cbn. apply eval_lift. apply eval_lift. eassumption. }
 Qed.
-  
+
+Definition e_setup2 a b rest := (e_setup1 a b (Elet e_step1 rest)).
+
+Definition a_var2 := Eletvar (5%nat).
+Definition a_d_var2 := Eletvar (4%nat).
+Definition b_var2 := Eletvar (3%nat).
+Definition b_d_var2 := Eletvar (2%nat).
+Definition binv_d_var2 := Eletvar (1%nat).
+Definition step1_var2 := Eletvar (0%nat).
+
+Definition e_step2 :=
+ e_long_of_float_ne
+       (e_mulf (e_float_of_long step1_var2)
+          (e_fmaddf
+             binv_d_var2
+             (e_fmsubf (e_float_const ExtFloat.one)
+                binv_d_var2
+                b_d_var2 )
+             binv_d_var2)).
+
+Lemma e_step2_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_setup2 expr_a expr_b (e_step2))
+           (step2_div_long' (step1_div_longu (Vlong a) (Vlong b)) (Vlong b))).
+Proof.
+intros.  
+unfold e_setup2, e_setup1, e_step2, step2_div_long', step2_real_div_long, approx_inv_longu.
+repeat (econstructor + apply eval_lift + eassumption).
+Qed.