diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-10 15:49:39 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-10 15:49:39 +0100 |
| commit | f42abd286e90cad92174cd77b2dd068ed8dd11ae (patch) | |
| tree | ac7fff283a298d4664d4bb95839864043074feb9 /kvx | |
| parent | b7875749ae445c43130fabd9eb9099eddea48318 (diff) | |
| download | compcert-kvx-f42abd286e90cad92174cd77b2dd068ed8dd11ae.tar.gz compcert-kvx-f42abd286e90cad92174cd77b2dd068ed8dd11ae.zip | |
wrong operator
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 9463313a..9cde7d97 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -394,7 +394,7 @@ Proof. Qed. Definition rough_approx_div_longu a b := - Val.maketotal (Val.longuoffloat + Val.maketotal (Val.longuoffloat_ne (Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b))). Definition rough_approx_div_thresh := 1649267441663%Z. @@ -413,7 +413,7 @@ Proof. cbn. Local Transparent Float.to_longu Float.mul. - unfold Float.to_longu, Float.mul, Float.of_longu. + unfold Float.to_longu_ne, Float.mul, Float.of_longu. set (re := (@eq_refl Datatypes.comparison Lt)). pose proof (Int64.unsigned_range a) as a_RANGE. @@ -452,5 +452,15 @@ Proof. cbn. gappa. } + rewrite C1F in C3. + rewrite C2F in C3. + cbn in C3. + destruct C3 as (C3R & C3F & _). + + pose proof (ZofB_ne_range_correct 53 1024 + (Bmult 53 1024 re re Float.binop_nan mode_NE + (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4. + rewrite C3F in C4. + rewrite C3R in C4. Admitted. |