diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-11 15:37:52 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-11 15:37:52 +0100 |
| commit | 6e01e627018c745c6fd490dd6ced63203d482bbd (patch) | |
| tree | 73af3283d0143497b08f4654155c21b5135f537a /kvx | |
| parent | aa8f655361670b593f805b1e57a1089b8f924938 (diff) | |
| download | compcert-kvx-6e01e627018c745c6fd490dd6ced63203d482bbd.tar.gz compcert-kvx-6e01e627018c745c6fd490dd6ced63203d482bbd.zip | |
progress in proofs
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index d16417fb..f20efa4e 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -499,7 +499,7 @@ Proof. lia. Qed. -Definition rough_approx_div_thresh := 1%R. +Definition rough_approx_div_thresh := 1683627180032%R. Theorem rough_approx_div_longu_correct : forall a b, @@ -607,4 +607,7 @@ Proof. assert (Rabs (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r) <= 1024)%R as DELTA2. { unfold rd. gappa. } set (delta2 := (rd (rd (IZR a') * f_r) - rd (IZR a') * f_r)%R) in *. -Admitted. + unfold rough_approx_inv_thresh in C1D. + set (delta3 := (f_r - 1 / IZR b')%R) in *. + gappa. +Qed. |