diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-12 16:06:35 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-12 16:06:35 +0100 |
| commit | 9cacc4caa5710f35a7ab73de6aa0ddf849e60d73 (patch) | |
| tree | 57d45ee4ee15761b50ef6ba01a44f622b362ab87 /kvx | |
| parent | fc58331d1aa0c1379df8b17d52f71b07d80c3045 (diff) | |
| download | compcert-kvx-9cacc4caa5710f35a7ab73de6aa0ddf849e60d73.tar.gz compcert-kvx-9cacc4caa5710f35a7ab73de6aa0ddf849e60d73.zip | |
proof of approx for a/b
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e8e7f8be..f4d727be 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -464,7 +464,7 @@ Definition smallb_threshold := 4398046511104%Z. Definition rough_approx_div_longu_smallb_delta := 3917010173952%Z. Definition step1_real_quotient (a b : R) := - rd ((rd a) * (rd (rs (1 / rs b)))). + rd ((rd (a)) * (rd (rs (1 / rs (b))))). Theorem rough_approx_div_longu_correct: forall a b, @@ -535,7 +535,31 @@ Proof. auto. Qed. - + +Definition smallb_thresh := 4398046511104%Z. + +Definition smallb_approx_range := 1649280000000%R. +Lemma step1_smallb : + forall a b + (a_RANGE : (0 <= a <= 18446744073709551615)%R) + (b_RANGE : (1 <= b <= IZR smallb_thresh)%R), + (Rabs((step1_real_quotient a b) - a/b) <= smallb_approx_range)%R. +Proof. + intros. + unfold smallb_thresh in b_RANGE. + unfold smallb_approx_range. + replace (step1_real_quotient a b - a/b)%R with + ((rd ((rd (a)) * (rd (rs (1 / rs (b))))) + - ((rd (a)) * (rd (rs (1 / rs (b)))))) + + (rd(a)) * (rd (rs (1 / rs (b))) - 1/b) + + (rd(a) - a)/b)%R; cycle 1. + { unfold step1_real_quotient. + field. + lra. + } + gappa. +Qed. + (* Definition rough_approx_div_thresh := 1683627180032%R. |