From 0ec09c99af2071f52271dd5e14846f5da3bcb718 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Jan 2022 22:37:25 +0100 Subject: some progress --- kvx/FPDivision64.v | 176 +++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 157 insertions(+), 19 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 74303a7a..e4f883e7 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -29,6 +29,25 @@ Require Import IEEE754_extra. From Gappa Require Import Gappa_tactic. + +Lemma Znearest_lub : + forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z. +Proof. + intros until x. intro BND. + pose proof (Zfloor_lub n x BND). + pose proof (Znearest_ge_floor choice x). + lia. +Qed. + +Lemma Znearest_glb : + forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z. +Proof. + intros until x. intro BND. + pose proof (Zceil_glb n x BND). + pose proof (Znearest_le_ceil choice x). + lia. +Qed. + Definition approx_inv_longu b := let invb_s := ExtValues.invfs (Val.maketotal (Val.singleoflongu b)) in let invb_d := Val.floatofsingle invb_s in @@ -851,7 +870,99 @@ Proof. rewrite C4. reflexivity. Qed. - + +Lemma step1_div_longu_correct_anyb : + forall a b + (b_NOT01 : (1 < Int64.unsigned b)%Z), + exists (q : int64), + (step1_div_longu (Vlong a) (Vlong b)) = Vlong q. +Proof. + intros. + + pose proof (Int64.unsigned_range a) as a_RANGE. + pose proof (Int64.unsigned_range b) as b_RANGE. + change Int64.modulus with 18446744073709551616%Z in *. + set (a' := Int64.unsigned a) in *. + set (b' := Int64.unsigned b) in *. + assert (0 <= IZR a' <= 18446744073709551615)%R as a_RANGE'. + { split; apply IZR_le; lia. } + assert (2 <= IZR b' <= 18446744073709551615)%R as b_RANGE'. + { split; apply IZR_le; lia. } + + assert (0 < b')%Z as b_NOT0 by lia. + + destruct (Z_le_gt_dec a' 0). + { assert (a' = 0%Z) as ZERO by lia. + replace a with Int64.zero; cycle 1. + { + unfold a' in ZERO. + unfold Int64.zero. + rewrite <- ZERO. + apply Int64.repr_unsigned. + } + exists Int64.zero. + apply step1_div_longu_a0. + exact b_NOT0. + } + + unfold step1_div_longu. + unfold step1_real_div_longu. + destruct (step1_real_inv_longu_correct b b_NOT0) as (f & C1E & C1R & C1F & C1S). + rewrite C1E. + cbn. + unfold Float.of_longu, Float.mul, Float.to_longu_ne. + set (re := (@eq_refl Datatypes.comparison Lt)). + fold a'. + fold b' in C1R. + pose proof (BofZ_correct 53 1024 re re a') as C2. + rewrite Rlt_bool_true in C2; cycle 1. + { clear C2. + apply Rabs_relax with (b := bpow radix2 64). + { apply bpow_lt. lia. } + cbn. + gappa. + } + cbn in C2. + destruct C2 as (C2R & C2F & C2S). + pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE + (BofZ 53 1024 re re a') f) as C3. + rewrite C2R in C3. + rewrite C2F in C3. + rewrite C2S in C3. + rewrite C1R in C3. + rewrite C1F in C3. + rewrite C1S in C3. + rewrite Rlt_bool_true in C3; cycle 1. + { clear C3. + apply Rabs_relax with (b := bpow radix2 64). + { apply bpow_lt. lia. } + cbn. + gappa. + } + cbn in C3. + destruct C3 as (C3R & C3F & _). + pose proof (ZofB_ne_range_correct 53 1024 + (Bmult 53 1024 re re Float.binop_nan mode_NE + (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4. + rewrite C3R in C4. + rewrite C3F in C4. + cbn zeta in C4. + rewrite Zle_bool_true in C4 ; cycle 1. + { clear C4. + apply Znearest_lub. + gappa. + } + rewrite Zle_bool_true in C4 ; cycle 1. + { clear C4. + apply Znearest_glb. + cbn. + gappa. + } + rewrite C4. + cbn. + eauto. +Qed. + Definition smallb_approx_range := 4400000000000%Z. Lemma step1_div_longu_correct : forall a b, @@ -1194,24 +1305,6 @@ Definition step2_div_long a b := Val.select (Val.cmpl_bool Cgt (Val.subl (Val.mull q b) a) (Vlong Int64.zero)) (Val.addl q (Vlong Int64.mone)) q Tlong. -Lemma Znearest_lub : - forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z. -Proof. - intros until x. intro BND. - pose proof (Zfloor_lub n x BND). - pose proof (Znearest_ge_floor choice x). - lia. -Qed. - -Lemma Znearest_glb : - forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z. -Proof. - intros until x. intro BND. - pose proof (Zceil_glb n x BND). - pose proof (Znearest_le_ceil choice x). - lia. -Qed. - Lemma function_ite : forall {A B : Type} (fn : A->B) (b : bool) (x y: A), fn (if b then x else y) = (if b then fn x else fn y). @@ -1663,3 +1756,48 @@ Proof. rewrite zlt_false by lia. reflexivity. Qed. + +Lemma twostep_div_longu_bigb_correct : + forall a b + (b_BIG : ((Int64.unsigned b) > smallb_thresh)%Z) + (b_NOT_TOO_BIG : ((Int64.unsigned b) <= Int64.max_signed)%Z), + (twostep_div_longu (Vlong a) (Vlong b)) = + (Val.maketotal (Val.divlu (Vlong a) (Vlong b))). +Proof. + intros. + unfold twostep_div_longu. + set (b' := Int64.unsigned b) in *. + set (a' := Int64.unsigned a) in *. +Admitted. + +(* + assert (0 < b')%Z as b_NOT0 by lia. + assert (b' <= Int64.max_signed)%Z as b_NOTBIG. + { change Int64.max_signed with (9223372036854775807)%Z. + unfold smallb_thresh in b_RANGE. + lia. + } + cbn. + rewrite (step2_div_long_bigb_correct (Int64.sub a (Int64.mul b q1)) b r1_SMALL b_NOT0 b_NOTBIG). + unfold Int64.add, Int64.sub, Int64.mul, Int64.divu. + fold q1' b' a'. + rewrite <- unsigned_repr_sub. + rewrite <- unsigned_repr_add. + rewrite Int64.signed_repr ; cycle 1. + { + change Int64.min_signed with (-9223372036854775808)%Z. + change Int64.max_signed with (9223372036854775807)%Z. + unfold smallb_approx_range in *. + lia. + } + rewrite Z.add_comm. + rewrite <- Z.div_add by lia. + replace (a' - b' * q1' + q1' * b')%Z with a' by ring. + rewrite Int64.eq_false ; cycle 1. + { intro Z. unfold b' in b_NOT0. rewrite Z in b_NOT0. + rewrite Int64.unsigned_zero in b_NOT0. + lia. + } + reflexivity. +Qed. +*) -- cgit