progress

1 files changed, 36 insertions, 23 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index f991ff93..457b280b 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2386,48 +2386,61 @@ Definition b_d_var2 := Eletvar (2%nat).
 Definition binv_d_var2 := Eletvar (1%nat).
 Definition step1_var2 := Eletvar (0%nat).
 
-Definition e_step2 :=
+Definition e_step2 := e_msubl a_var2 b_var2 step1_var2.
+
+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_long_of_float_ne
-       (e_mulf (e_float_of_long step1_var2)
+       (e_mulf (e_float_of_long step2_var3)
           (e_fmaddf
-             binv_d_var2
+             binv_d_var3
              (e_fmsubf (e_float_const ExtFloat.one)
-                binv_d_var2
-                b_d_var2 )
-             binv_d_var2)).
+                binv_d_var3
+                b_d_var3 )
+             binv_d_var3)).
 
-Lemma e_step2_correct :
+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_setup2 expr_a expr_b (e_step2))
-           (step2_div_long' (step1_div_longu (Vlong a) (Vlong b)) (Vlong b))).
+         (eval_expr ge sp cmenv memenv le (e_setup3 expr_a expr_b (e_step3))
+           (step2_div_long' (Val.subl (Vlong a) (Val.mull (Vlong b) (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.
 
-Definition e_setup3 a b rest := (e_setup2 a b (Elet e_step2 rest)).
+Definition e_setup4 a b rest := (e_setup3 a b (Elet e_step3 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 a_var4 := Eletvar (7%nat).
+Definition a_d_var4 := Eletvar (6%nat).
+Definition b_var4 := Eletvar (5%nat).
+Definition b_d_var4 := Eletvar (4%nat).
+Definition binv_d_var4 := Eletvar (3%nat).
+Definition step1_var4 := Eletvar (2%nat).
+Definition step2_var4 := Eletvar (1%nat).
+Definition step3_var4 := Eletvar (0%nat).
 
-Definition e_step3 :=
-  e_ite Tlong (Ccompl0 Clt) (e_msubl step1_var3 step2_var3 b_var3)
-             (e_addlimm step2_var3 Int64.mone) step2_var3.
+Definition e_step4 :=
+  e_ite Tlong (Ccompl0 Clt) (e_msubl step2_var4 step3_var4 b_var4)
+             (e_addlimm step3_var4 Int64.mone) step3_var4.
 
-Lemma e_step3_correct :
+Lemma e_step4_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))).
+         (eval_expr ge sp cmenv memenv le (e_setup4 expr_a expr_b (e_step4))
+           (step2_div_long (Val.subl (Vlong a) (Val.mull (Vlong b) (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.