progress

1 files changed, 44 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 457b280b..a1ab09b8 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2348,8 +2348,10 @@ 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_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 e_ite ty c vc v1 v2 := Eop (Osel c ty) (v1 ::: v2 ::: vc ::: Enil).
+Definition e_cmplimm c v n := Eop (Ocmp (Ccomplimm c n)) (v ::: Enil).
+Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
+
 Definition a_var1 := Eletvar (4%nat).
 Definition a_d_var1 := Eletvar (3%nat).
 Definition b_var1 := Eletvar (2%nat).
@@ -2446,3 +2448,43 @@ 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.
+
+Definition e_setup5 a b rest := (e_setup4 a b (Elet e_step4 rest)).
+
+
+Definition a_var5 := Eletvar (8%nat).
+Definition a_d_var5 := Eletvar (7%nat).
+Definition b_var5 := Eletvar (6%nat).
+Definition b_d_var5 := Eletvar (5%nat).
+Definition binv_d_var5 := Eletvar (4%nat).
+Definition step1_var5 := Eletvar (3%nat).
+Definition step2_var5 := Eletvar (2%nat).
+Definition step3_var5 := Eletvar (1%nat).
+Definition step4_var5 := Eletvar (0%nat).
+
+Definition e_step5 := e_addl step1_var5 step4_var5.
+
+Lemma e_step5_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_setup5 expr_a expr_b (e_step5))
+           (twostep_div_longu (Vlong a) (Vlong b))).
+Proof.
+  intros.
+  Local Transparent twostep_div_longu.
+  repeat unfold e_setup2, e_setup1, e_step2, step2_div_long, step2_div_long', step2_real_div_long, approx_inv_longu, step1_div_longu, twostep_div_longu.
+repeat (econstructor + apply eval_lift + eassumption).
+Qed.
+
+(*
+  let is_big := Val.cmpl_bool Clt b (Vlong Int64.zero) in
+  let is_one := Val.cmplu_bool (Mem.valid_pointer m) Cle b (Vlong Int64.one) in
+  let is_special := Val.or (Val.of_optbool is_big) (Val.of_optbool is_one) in
+  let if_big := Val.select (Val.cmplu_bool (Mem.valid_pointer m) Clt a b)
+                           (Vlong Int64.zero) (Vlong Int64.one) Tlong in
+  let if_special := Val.select is_big if_big a Tlong in
+  Val.select (Val.cmp_bool Cne is_special (Vint Int.zero))
+             if_special
+             (twostep_div_longu a b) Tlong.
+ *)