From 6eac4cb3302f57d43e6b8d4c17688388db9619e5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 4 Feb 2022 20:35:11 +0100 Subject: progress --- kvx/FPDivision64.v | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index fc8e6173..79bfdc3b 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1071,15 +1071,16 @@ Proof. intros ; split ; apply le_IZR ; lra. Qed. -Definition bigb_thresh := 9223372036854775808%Z. +Definition bigb_thresh := 18446740000000000000%Z. Lemma step1_div_longu_correct_anyb2 : forall a b, - (1 < Int64.unsigned b <= bigb_thresh)%Z -> + (1 < Int64.unsigned b <= bigb_thresh)%Z -> + (Int64.unsigned b <= Int64.unsigned a)%Z -> exists (q : int64), (step1_div_longu (Vlong a) (Vlong b)) = Vlong q /\ (Int64.min_signed <= (Int64.unsigned a - Int64.unsigned b*Int64.unsigned q) <= Int64.max_signed)%Z. Proof. - intros a b b_RANGE. + intros a b b_RANGE LESS. pose proof (Int64.unsigned_range a) as a_RANGE. change Int64.modulus with 18446744073709551616%Z in a_RANGE. @@ -1164,11 +1165,15 @@ Proof. cycle 1. { field. lra. } set (delta2 := ((rd (rd a1 * rd (rs (1 / rs b1)))-(a1 * (1 / b1))) / (a1 * (1 / b1)))%R) in *. - assert (Rabs (delta2) <= 1/4194304)%R. - { unfold delta2. gappa. } + (* assert (Rabs (delta2) <= 1/4194304)%R. + { unfold delta2. gappa. } *) replace (a1 - b1 * (delta1 + (delta2 + 1) * (a1 / b1)))%R with (-b1*delta1 - a1*delta2)%R; cycle 1. { field. lra. } + assert (b1 <= a1)%R as LESS'. + { unfold a1, b1. + apply IZR_le. lia. } + unfold delta2. gappa. Qed. -- cgit