progress

1 files changed, 18 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 619fcfa6..572df195 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2333,6 +2333,10 @@ 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 e_addlimm a b := Eop (Oaddlimm b) (a ::: Enil).
+Definition e_msub a b c := Eop Omsub (a ::: b ::: c ::: Enil).
+Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (vc ::: v1 ::: v2 ::: Enil). 
+  
 Definition a_var1 := Eletvar (4%nat).
 Definition a_d_var1 := Eletvar (3%nat).
 Definition b_var1 := Eletvar (2%nat).
@@ -2390,3 +2394,17 @@ 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.
+
+Definition e_setup3 a b rest := (e_setup2 a b (Elet e_step2 rest)).
+
+Definition a_var3 := Eletvar (6%nat).
+Definition a_d_var3 := Eletvar (5%nat).
+Definition b_var3 := Eletvar (4%nat).
+Definition b_d_var3 := Eletvar (3%nat).
+Definition binv_d_var3 := Eletvar (2%nat).
+Definition step1_var3 := Eletvar (1%nat).
+Definition step2_var3 := Eletvar (0%nat).
+
+Definition e_step3 :=
+  e_ite Tlong (Ccompl0 Clt) (e_msub a_var3 step2_var3 b_var3)
+             (e_addlimm step2_var3 Int64.mone) step2_var3.