diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-10 14:55:20 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-10 14:55:20 +0100 |
| commit | f411b8eb07064070440169269d9f402b3cdbb009 (patch) | |
| tree | 71f5311bea14cc7dd69c1e57d9ce497b72b8b732 /kvx | |
| parent | 120446974d1a83e6f9ef99f049d597166be09271 (diff) | |
| download | compcert-kvx-f411b8eb07064070440169269d9f402b3cdbb009.tar.gz compcert-kvx-f411b8eb07064070440169269d9f402b3cdbb009.zip | |
state theorem
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 6c053d7c..9baa3f94 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -392,3 +392,18 @@ Proof. cbn. gappa. Qed. + +Definition rough_approx_div_longu a b := + Val.maketotal (Val.longuoffloat + (Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b))). + +Definition rough_approx_div_thresh := 1649267441663%Z. + +Theorem rough_approx_div_longu_correct : + forall a b, + (0 < Int64.unsigned b)%Z -> + exists (q : int64), + (rough_approx_div_longu (Vlong a) (Vlong b)) = Vlong q /\ + (Z.abs ((Int64.unsigned a) - (Int64.unsigned q) * (Int64.unsigned b)) <= rough_approx_div_thresh)%Z. +Proof. +Admitted. |