From 3e445a4f31b5b309b64cdf307830716f0001003f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 17:16:26 +0100 Subject: progress --- kvx/FPDivision64.v | 59 +++++++++++++++++++++++++++++++++--------------------- 1 file changed, 36 insertions(+), 23 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index f991ff93..457b280b 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2386,48 +2386,61 @@ Definition b_d_var2 := Eletvar (2%nat). Definition binv_d_var2 := Eletvar (1%nat). Definition step1_var2 := Eletvar (0%nat). -Definition e_step2 := +Definition e_step2 := e_msubl a_var2 b_var2 step1_var2. + +Definition e_setup3 a b rest := (e_setup2 a b (Elet e_step2 rest)). + +Definition a_var3 := Eletvar (6%nat). +Definition a_d_var3 := Eletvar (5%nat). +Definition b_var3 := Eletvar (4%nat). +Definition b_d_var3 := Eletvar (3%nat). +Definition binv_d_var3 := Eletvar (2%nat). +Definition step1_var3 := Eletvar (1%nat). +Definition step2_var3 := Eletvar (0%nat). + +Definition e_step3 := e_long_of_float_ne - (e_mulf (e_float_of_long step1_var2) + (e_mulf (e_float_of_long step2_var3) (e_fmaddf - binv_d_var2 + binv_d_var3 (e_fmsubf (e_float_const ExtFloat.one) - binv_d_var2 - b_d_var2 ) - binv_d_var2)). + binv_d_var3 + b_d_var3 ) + binv_d_var3)). -Lemma e_step2_correct : +Lemma e_step3_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))). + (eval_expr ge sp cmenv memenv le (e_setup3 expr_a expr_b (e_step3)) + (step2_div_long' (Val.subl (Vlong a) (Val.mull (Vlong b) (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. -Definition e_setup3 a b rest := (e_setup2 a b (Elet e_step2 rest)). +Definition e_setup4 a b rest := (e_setup3 a b (Elet e_step3 rest)). -Definition a_var3 := Eletvar (6%nat). -Definition a_d_var3 := Eletvar (5%nat). -Definition b_var3 := Eletvar (4%nat). -Definition b_d_var3 := Eletvar (3%nat). -Definition binv_d_var3 := Eletvar (2%nat). -Definition step1_var3 := Eletvar (1%nat). -Definition step2_var3 := Eletvar (0%nat). +Definition a_var4 := Eletvar (7%nat). +Definition a_d_var4 := Eletvar (6%nat). +Definition b_var4 := Eletvar (5%nat). +Definition b_d_var4 := Eletvar (4%nat). +Definition binv_d_var4 := Eletvar (3%nat). +Definition step1_var4 := Eletvar (2%nat). +Definition step2_var4 := Eletvar (1%nat). +Definition step3_var4 := Eletvar (0%nat). -Definition e_step3 := - e_ite Tlong (Ccompl0 Clt) (e_msubl step1_var3 step2_var3 b_var3) - (e_addlimm step2_var3 Int64.mone) step2_var3. +Definition e_step4 := + e_ite Tlong (Ccompl0 Clt) (e_msubl step2_var4 step3_var4 b_var4) + (e_addlimm step3_var4 Int64.mone) step3_var4. -Lemma e_step3_correct : +Lemma e_step4_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_setup3 expr_a expr_b (e_step3)) - (step2_div_long (step1_div_longu (Vlong a) (Vlong b)) (Vlong b))). + (eval_expr ge sp cmenv memenv le (e_setup4 expr_a expr_b (e_step4)) + (step2_div_long (Val.subl (Vlong a) (Val.mull (Vlong b) (step1_div_longu (Vlong a) (Vlong b)))) (Vlong b))). Proof. intros. unfold e_setup2, e_setup1, e_step2, step2_div_long, step2_div_long', step2_real_div_long, approx_inv_longu, step1_div_longu. -- cgit