From d8a3b4a525bcd3ea17d1585ec2e93f3d2dcacba6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 19:27:56 +0100 Subject: progress --- kvx/FPDivision64.v | 46 ++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 44 insertions(+), 2 deletions(-) (limited to 'kvx') 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. + *) -- cgit