From ea53967476937f15ec4ceea1b31ece4d75b85f98 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 10 Feb 2022 10:51:46 +0100 Subject: progress --- kvx/FPDivision64.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 619fcfa6..572df195 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -2333,6 +2333,10 @@ 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 e_addlimm a b := Eop (Oaddlimm b) (a ::: Enil). +Definition e_msub a b c := Eop Omsub (a ::: b ::: c ::: Enil). +Definition e_ite ty c vc v1 v2 := Eop (Osel c ty) (vc ::: v1 ::: v2 ::: Enil). + Definition a_var1 := Eletvar (4%nat). Definition a_d_var1 := Eletvar (3%nat). Definition b_var1 := Eletvar (2%nat). @@ -2390,3 +2394,17 @@ 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 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_ite Tlong (Ccompl0 Clt) (e_msub a_var3 step2_var3 b_var3) + (e_addlimm step2_var3 Int64.mone) step2_var3. -- cgit