diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-04 20:35:11 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-04 20:35:11 +0100 |
| commit | 6eac4cb3302f57d43e6b8d4c17688388db9619e5 (patch) | |
| tree | 41691fe25b33c07f18135f08662502727a9473c4 /kvx | |
| parent | 9e37305cc4b817869de98b5cce49d3599d2c0aba (diff) | |
| download | compcert-kvx-6eac4cb3302f57d43e6b8d4c17688388db9619e5.tar.gz compcert-kvx-6eac4cb3302f57d43e6b8d4c17688388db9619e5.zip | |
progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 15 |
1 files changed, 10 insertions, 5 deletions
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. |