progress

1 files changed, 15 insertions, 3 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 34dc108b..f991ff93 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2347,8 +2347,8 @@ 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 e_msubl a b c := Eop Omsubl (a ::: b ::: c ::: Enil).
+Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil). 
   
 Definition a_var1 := Eletvar (4%nat).
 Definition a_d_var1 := Eletvar (3%nat).
@@ -2419,5 +2419,17 @@ 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_ite Tlong (Ccompl0 Clt) (e_msubl step1_var3 step2_var3 b_var3)
              (e_addlimm step2_var3 Int64.mone) step2_var3.
+
+Lemma e_step3_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_setup3 expr_a expr_b (e_step3))
+           (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_div_long', step2_real_div_long, approx_inv_longu, step1_div_longu.
+repeat (econstructor + apply eval_lift + eassumption).
+Qed.