finished proof but still why need for decomposition

1 files changed, 56 insertions, 16 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index a1ab09b8..c08103b1 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2075,8 +2075,7 @@ Definition full_div_longu a b m :=
   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_big := Val.longofintu (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Cge a b)) 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
@@ -2245,8 +2244,7 @@ Definition full2_div_longu a b m :=
   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_big := Val.longofintu (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Cge a b)) 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
@@ -2350,7 +2348,11 @@ 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_cmplimm c v n := Eop (Ocmp (Ccomplimm c n)) (v ::: Enil).
+Definition e_cmpluimm c v n := Eop (Ocmp (Ccompluimm c n)) (v ::: Enil).
 Definition e_addl a b := Eop Oaddl (a ::: b ::: Enil).
+Definition e_or a b := Eop Oor (a ::: b ::: Enil).
+Definition e_cast32unsigned a := Eop Ocast32unsigned (a ::: Enil).
+Definition e_cmplu c a b := Eop (Ocmp (Ccomplu c)) (a ::: b ::: Enil).
 
 Definition a_var1 := Eletvar (4%nat).
 Definition a_d_var1 := Eletvar (3%nat).
@@ -2451,7 +2453,6 @@ 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).
@@ -2477,14 +2478,53 @@ Proof.
 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.
- *)
+Definition e_setup6 a b rest := (e_setup5 a b (Elet e_step5 rest)).
+
+Definition a_var6 := Eletvar (9%nat).
+Definition a_d_var6 := Eletvar (8%nat).
+Definition b_var6 := Eletvar (7%nat).
+Definition b_d_var6 := Eletvar (6%nat).
+Definition binv_d_var6 := Eletvar (5%nat).
+Definition step1_var6 := Eletvar (4%nat).
+Definition step2_var6 := Eletvar (3%nat).
+Definition step3_var6 := Eletvar (2%nat).
+Definition step4_var6 := Eletvar (1%nat).
+Definition twostep_var6 := Eletvar (0%nat).
+
+Definition e_step6 := e_cmplimm Clt b_var6 Int64.zero.
+
+Definition e_setup7 a b rest := e_setup6 a b (Elet e_step6 rest).
+
+Definition a_var7 := Eletvar (10%nat).
+Definition a_d_var7 := Eletvar (9%nat).
+Definition b_var7 := Eletvar (8%nat).
+Definition b_d_var7 := Eletvar (7%nat).
+Definition binv_d_var7 := Eletvar (6%nat).
+Definition step1_var7 := Eletvar (5%nat).
+Definition step2_var7 := Eletvar (5%nat).
+Definition step3_var7 := Eletvar (3%nat).
+Definition step4_var7 := Eletvar (2%nat).
+Definition twostep_var7 := Eletvar (1%nat).
+Definition is_big_var7 := Eletvar (0%nat).
+
+Definition e_is_one :=  e_cmpluimm Cle b_var7 Int64.one.
+Definition e_is_special := e_or is_big_var7 e_is_one.
+Definition e_if_big := e_cast32unsigned (e_cmplu Cge a_var7 b_var7).
+Definition e_if_special := e_ite Tlong (Ccompu0 Cne) is_big_var7 e_if_big a_var7.
+Definition e_step7 := e_ite Tlong (Ccompu0 Cne) e_is_special e_if_special twostep_var7.
+
+Lemma e_step7_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_setup7 expr_a expr_b (e_step7))
+           (full2_div_longu (Vlong a) (Vlong b) memenv)).
+Proof.
+  intros.
+  Local Transparent full2_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, full2_div_longu.
+  repeat (econstructor + apply eval_lift + eassumption).
+  cbn.
+  repeat f_equal.
+  destruct (Int64.lt b Int64.zero); cbn; change (Int.eq Int.one Int.zero) with false; change (Int.eq Int.zero Int.zero) with true; cbn; reflexivity.
+Qed.