diff options
Diffstat (limited to 'kvx/FPDivision64.v')
| -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. |