From 6bd3c44a582d3d1f23fe4ed99dec8b59893e3a85 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 22:35:22 +0100 Subject: finished proof but still why need for decomposition --- kvx/FPDivision64.v | 72 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 56 insertions(+), 16 deletions(-) (limited to 'kvx') 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. -- cgit