From 68149e3a492be432561e61356f570ba394ca1e3a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 10:18:46 +0100 Subject: progress --- kvx/FPDivision64.v | 38 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 2c6a49c5..619fcfa6 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2324,11 +2324,15 @@ Qed. Open Scope cminorsel_scope. Definition e_invfs a := Eop Oinvfs (a ::: Enil). Definition e_float_of_longu a := Eop Ofloatoflongu (a ::: Enil). +Definition e_float_of_long a := Eop Ofloatoflong (a ::: Enil). Definition e_single_of_longu a := Eop Osingleoflongu (a ::: Enil). Definition e_float_of_single a := Eop Ofloatofsingle (a ::: Enil). +Definition e_long_of_float_ne a := Eop Olongoffloat_ne (a ::: Enil). Definition e_longu_of_float_ne a := Eop Olonguoffloat_ne (a ::: Enil). Definition e_mulf a b := Eop Omulf (a ::: b ::: Enil). - +Definition e_float_const c := Eop (Ofloatconst c) Enil. +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 a_var1 := Eletvar (4%nat). Definition a_d_var1 := Eletvar (3%nat). Definition b_var1 := Eletvar (2%nat). @@ -2355,4 +2359,34 @@ Proof. { eassumption. } { cbn. apply eval_lift. apply eval_lift. eassumption. } Qed. - + +Definition e_setup2 a b rest := (e_setup1 a b (Elet e_step1 rest)). + +Definition a_var2 := Eletvar (5%nat). +Definition a_d_var2 := Eletvar (4%nat). +Definition b_var2 := Eletvar (3%nat). +Definition b_d_var2 := Eletvar (2%nat). +Definition binv_d_var2 := Eletvar (1%nat). +Definition step1_var2 := Eletvar (0%nat). + +Definition e_step2 := + e_long_of_float_ne + (e_mulf (e_float_of_long step1_var2) + (e_fmaddf + binv_d_var2 + (e_fmsubf (e_float_const ExtFloat.one) + binv_d_var2 + b_d_var2 ) + binv_d_var2)). + +Lemma e_step2_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))). +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. -- cgit