NEWS 10.5 KB
Newer Older
1 2
Version 3.0.0:
 - stripped prefix from all the file names, renamed some files
BOLDO Sylvie's avatar
BOLDO Sylvie committed
3
   . Definitions -> Defs
BOLDO Sylvie's avatar
BOLDO Sylvie committed
4
   . Appli -> IEEE754
5
 - renamed canonic_exp into cexp, canonic into canonical
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
 - renamed all theorems ending with unicity by unique
7
 - changed FLX, FIX, FLT, FLXN, FTZ_format into inductive types
8
 - changed nan_pl into a boolean predicate
Guillaume Melquiond's avatar
Guillaume Melquiond committed
9
 - replaced Z2R with Coq 8.7's IZR
BOLDO Sylvie's avatar
BOLDO Sylvie committed
10
 - removed Zeven and its theorems in favor of Z.even of the standard library
11
 - modified statements of Rcompare_sqr, ulp_DN, mult_error_FLT, mag_div
BOLDO Sylvie's avatar
BOLDO Sylvie committed
12
 - added theorems about the remainder being in the format (in Div_sqrt_error)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49
 - renamed theorem more uniformly
    . bpow_plus1 -> bpow_plus_1
    . mag_lt_pos -> lt_mag
    . F2R_le_reg -> le_F2R
    . F2R_le_compat -> F2R_le
    . F2R_lt_reg -> lt_F2R
    . F2R_lt_compat -> F2R_lt
    . F2R_eq_reg -> eq_F2R
    . F2R_eq_compat -> F2R_eq
    . F2R_eq_0_reg -> eq_0_F2R
    . F2R_ge_0_reg -> ge_0_F2R
    . F2R_le_0_reg -> le_0_F2R
    . F2R_gt_0_reg -> gt_0_F2R
    . F2R_lt_0_reg -> lt_0_F2R
    . F2R_le_0_compat -> F2R_le_0
    . F2R_ge_0_compat -> F2R_ge_0
    . F2R_gt_0_compat -> F2R_gt_0
    . F2R_lt_0_compat -> F2R_lt_0
    . F2R_neq_0_compat -> F2R_neq_0
    . Fnum_ge_0_compat -> Fnum_ge_0
    . Fnum_le_0_compat -> Fnum_le_0
    . round_ZR_pos -> round_ZR_DN
    . round_ZR_neg -> round_ZR_UP
    . round_AW_pos -> round_ZR_UP
    . round_AW_neg -> round_ZR_DN
    . Znearest_N -> Znearest_half
    . Rnd_DN_UP_pt_N -> Rnd_N_pt_DN_UP
    . Rnd_DN_pt_N -> Rnd_N_pt_DN
    . Rnd_UP_pt_N -> Rnd_N_pt_UP
    . Rnd_DN_UP_pt_sym -> Rnd_UP_pt_opp
    . Rnd_UP_DN_pt_sym -> Rnd_DN_pt_opp
    . Rnd_DN_UP_sym -> Rnd_DN_opp
    . Rnd_N_pt_sym -> Rnd_N_pt_opp_inv
    . Rnd_N_pt_pos -> Rnd_N_pt_ge_0
    . Rnd_N_pt_neg -> Rnd_N_pt_le_0
    . Rnd_NG_pt_sym -> Rnd_NG_pt_opp_inv
    . Rnd_NA_N_pt -> Rnd_NA_pt_N
BOLDO Sylvie's avatar
BOLDO Sylvie committed
50
    . Rnd_odd_pt_sym -> Rnd_odd_pt_opp_inv
BOLDO Sylvie's avatar
BOLDO Sylvie committed
51 52 53 54 55 56 57
    . le_pred_lt -> pred_ge_gt
    . lt_succ_le -> succ_gt_ge
    . le_round_DN_lt_UP -> round_DN_ge_UP_gt
    . round_UP_le_gt_DN -> round_UP_le_DN_lt
    . round_DN_eq_betw -> round_DN_eq
    . round_UP_eq_betw -> round_UP_eq
    . round_plus_eq_zero -> round_plus_neq_0 (and modified statement)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
58 59 60 61
    . round_odd_prop -> round_N_odd
    . double_round_*_beta_ge_* -> round_round_*_radix_ge_*
    . double_round_* -> round_round_*

BOLDO Sylvie's avatar
BOLDO Sylvie committed
62

63

Guillaume Melquiond's avatar
Guillaume Melquiond committed
64 65 66
Version 2.5.2:
 - ensured compatibility from Coq 8.4 to 8.6

Guillaume Melquiond's avatar
Guillaume Melquiond committed
67 68 69
Version 2.5.1:
 - ensured compatibility with both Coq 8.4 and 8.5

BOLDO Sylvie's avatar
BOLDO Sylvie committed
70
Version 2.5.0:
Guillaume Melquiond's avatar
Guillaume Melquiond committed
71 72 73 74 75 76
 - ensured compatibility with both Coq 8.4 and 8.5
   (Flocq now provides its own version of iter_pos)
 - redefined ulp, so that ulp(0) is meaningful
 - renamed, generalized, and added lemmas in Fcore_ulp
 - extended predecessor and successor to nonpositive values
   (the previous definition of pred has been renamed pred_pos)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
77
 - removed some hypotheses on lemmas of Fprop_relative
Guillaume Melquiond's avatar
Guillaume Melquiond committed
78 79 80 81 82 83 84
 - added more examples
   . Average: proof on Sterbenz's average and correctly-rounded average
   . Cody_Waite: Cody & Waite's approximation of exponential
   . Compute: effective FP computations with an example of sqrt(sqr(x))
     in radix 5 and precision 3
   . Division_u16: integer division using floating-point FMA
   . Triangle: Kahan's algorithm for the area of a triangle
BOLDO Sylvie's avatar
BOLDO Sylvie committed
85

Guillaume Melquiond's avatar
Guillaume Melquiond committed
86 87 88
Version 2.4.0:
 - moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
 - added theorems about double rounding being innocuous (Fappli_double_round.v)
89
 - added example about double rounding in odd radix
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90 91
 - improved a bit the efficiency of IEEE-754 arithmetic

Guillaume Melquiond's avatar
Guillaume Melquiond committed
92 93 94 95 96
Version 2.3.0:
 - moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
 - used the square root from the standard library instead of a custom one
 - added an example about sqrt(sqr(x))

Guillaume Melquiond's avatar
Guillaume Melquiond committed
97 98 99
Version 2.2.2:
 - fixed install target for case-insensitive filesystems

100 101 102
Version 2.2.1:
 - fixed regeneration of Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
103 104 105 106
Version 2.2.0:
 - added theorems about rounding to odd and double rounding
 - improved handling of special values of IEEE-754 arithmetic

Guillaume Melquiond's avatar
Guillaume Melquiond committed
107 108 109 110 111 112
Version 2.1.0:
 - ensured compatibility with both Coq 8.3 and 8.4
 - improved support for rounding toward and away from zero
 - proved that formats are stable by arbitrary rounding or ulp addition
 - generalized usage of ln_beta

113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
Version 2.0.0:
 - changed rounding modes from records to R -> Z functions as arguments
   to the round function
   . rndDN -> Zfloor
   . rndUP -> Zceil
   . rndZE -> Ztrunc
   . rndNE -> ZnearestE
   . rndNA -> ZnearestA
 - added typeclasses for automatic inference of properties:
   . Valid_exp for Z -> Z functions describing formats
   . Valid_rnd for R -> Z functions describing rounding modes
   . Exp_not_FTZ for Z -> Z functions describing formats with subnormal
   . Monotone_exp for Z -> Z functions describing regular formats
   . Exists_NE for radix/formats supporting rounding to nearest even
 - removed theorems superseded by typeclasses:
   . FIX_exp_correct, FLX_exp_correct, FLT_exp_correct, FTZ_exp_correct
   . FIX_exp_monotone, FLX_exp_monotone, FLT_monotone
   . Rnd_NE_pt_FIX, Rnd_NE_pt_FLX, Rnd_NE_pt_FLT
   . round_NE_pt_FLX, round_NE_pt_FLT
   . Zrnd_opp_le, Zrnd_Z2R_opp
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133
 - removed example file Fappli_sqrt_FLT_ne
134 135 136 137 138 139 140 141 142 143 144 145 146 147
 - split theorems on equivalence between specific and generic formats
   into both directions:
   . FIX_format_generic and generic_format_FIX
   . FLX_format_generic and generic_format_FLX
   . FLT_format_generic and generic_format_FLT
   . FTZ_format_generic and generic_format_FTZ
 - modified correctness theorems for IEEE-754 operators so that they also
   mention finiteness of the results
 - added a Flocq_version.Flocq_version Coq variable for Flocq detection
   and version testing in configure scripts
 - moved parts of some files into other files:
   . Fcore_Raux -> Fcore_Zaux
   . Fcalc_digits -> Fcore_digits
   . Fappli_IEEE -> Fappli_IEEE_bits
BOLDO Sylvie's avatar
BOLDO Sylvie committed
148 149 150
 - renamed functions:
   . canonic_exponent -> canonic_exp
   . digits -> Zdigits
BOLDO Sylvie's avatar
BOLDO Sylvie committed
151 152 153 154 155 156
   . bounded_prec -> canonic_mantissa
   . Bsign_FF -> sign_FF
   . shl -> shl_align
   . shl_fexp -> shl_align_fexp
   . binary_round_sign -> binary_round_aux
   . binary_round_sign_shl -> binary_round
157 158 159 160 161
 - renamed theorems more uniformly:
   . Rabs_Rminus_pos -> Rabs_minus_le
   . exp_increasing_weak -> exp_le
   . ln_beta_monotone -> ln_beta_le
   . ln_beta_monotone_abs -> ln_beta_le_abs
BOLDO Sylvie's avatar
BOLDO Sylvie committed
162 163
   . abs_F2R -> F2R_Zabs (changed direction)
   . opp_F2R -> F2R_Zopp (changed direction)
164 165 166 167 168 169 170
   . scaled_mantissa_bpow -> scaled_mantissa_mult_bpow
   . round_monotone -> round_le
   . round_monotone_l -> round_ge_generic
   . round_monotone_r -> round_le_generic
   . round_monotone_abs_l -> abs_round_ge_generic
   . round_monotone_abs_r -> abs_round_le_generic
   . generic_format_canonic_exponent -> generic_format_F2R (modified hypothesis)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
171
   . canonic_exponent_round -> canonic_exp_round_ge
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
   . generic_N_pt -> round_N_pt
   . round_pred_pos_imp_rnd -> round_pred_ge_0
   . round_pred_rnd_imp_pos -> round_pred_gt_0
   . round_pred_neg_imp_rnd -> round_pred_le_0
   . round_pred_rnd_imp_neg -> round_pred_lt_0
   . ulp_le_pos -> ulp_le_id
   . succ_lt_le -> succ_le_lt
   . ulp_monotone -> ulp_le
   . ulp_DN_pt_eq -> ulp_DN
   . format_pred -> generic_format_pred
   . pred_ulp -> pred_plus_ulp
   . pred_lt -> pred_lt_id
   . FLT_generic_format_FLX -> generic_format_FLT_FLX
   . FLX_generic_format_FLT -> generic_format_FLX_FLT
   . FIX_generic_format_FLT -> generic_format_FIX_FLT
   . FLT_generic_format_FIX -> generic_format_FLT_FIX
   . FLT_round_FLX -> round_FLT_FLX
   . FTZ_round -> round_FTZ_FLX
   . FTZ_round_small -> round_FTZ_small
   . FLT_canonic_FLX -> canonic_exp_FLT_FLX
   . FLT_canonic_FIX -> canonic_exp_FLT_FIX
BOLDO Sylvie's avatar
BOLDO Sylvie committed
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
   . canonic_exponent_opp -> canonic_exp_opp
   . canonic_exponent_abs -> canonic_exp_abs
   . canonic_exponent_fexp -> canonic_exp_fexp
   . canonic_exponent_fexp_pos -> canonic_exp_fexp_pos
   . canonic_exponent_DN -> canonic_exp_DN
   . canonic_exp_ge -> abs_lt_bpow_prec (modified hypotheses)
   . Fopp_F2R -> F2R_opp
   . Fabs_F2R -> F2R_abs
   . plus_F2R -> F2R_plus
   . minus_F2R -> F2R_minus
   . mult_F2R -> F2R_mult
   . digits_abs -> Zdigits_abs
   . digits_ge_0 -> Zdigits_ge_0
   . digits_gt_0 -> Zdigits_gt_0
   . ln_beta_F2R_Zdigits -> ln_beta_F2R_Zdigits
   . digits_shift -> Zdigits_mult_Zpower
   . digits_Zpower -> Zdigits_Zpower
   . digits_le -> Zdigits_le
   . lt_digits -> lt_Zdigits
   . Zpower_le_digits -> Zpower_le_Zdigits
   . digits_le_Zpower -> Zdigits_le_Zpower
   . Zpower_gt_digits -> Zpower_gt_Zdigits
   . digits_gt_Zpower -> Zdigits_gt_Zpower
   . digits_mult_strong -> Zdigits_mult_strong
   . digits_mult -> Zdigits_mult
   . digits_mult_ge -> Zdigits_mult_ge
   . digits_shr -> Zdigits_div_Zpower
   . format_add -> generic_format_plus_prec (modified hypothesis)
   . format_nx -> ex_Fexp_canonic
BOLDO Sylvie's avatar
-> ++  
BOLDO Sylvie committed
222 223 224 225 226 227
   . generic_relative_error -> relative_error
   . generic_relative_error_ex -> relative_error_ex
   . generic_relative_error_F2R -> relative_error_F2R_emin
   . generic_relative_error_F2R_ex -> relative_error_F2R_emin_ex
   . generic_relative_error_2 -> relative_error_round
   . generic_relative_error_F2R_2 -> relative_error_round_F2R_emin
228
   . generic_relative_error_N -> relative_error_N
BOLDO Sylvie's avatar
-> ++  
BOLDO Sylvie committed
229 230 231 232 233 234
   . generic_relative_error_N_ex -> relative_error_N_ex
   . generic_relative_error_N_F2R -> relative_error_N_F2R_emin
   . generic_relative_error_N_F2R_ex -> relative_error_N_F2R_emin_ex
   . generic_relative_error_N_2 -> relative_error_N_round
   . generic_relative_error_N_F2R_2 -> relative_error_N_round_F2R_emin
   . relative_error_FLT_F2R  -> relative_error_FLT_F2R_emin
235
   . relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
BOLDO Sylvie's avatar
-> ++  
BOLDO Sylvie committed
236 237 238 239 240 241
   . relative_error_N_FLT_2 -> relative_error_N_FLT_round
   . relative_error_N_FLT_F2R -> relative_error_N_FLT_F2R_emin
   . relative_error_N_FLT_F2R_ex -> relative_error_N_FLT_F2R_emin_ex
   . relative_error_N_FLT_F2R_2 -> relative_error_N_FLT_round_F2R_emin
   . relative_error_FLX_2 -> relative_error_FLX_round
   . relative_error_N_FLX_2 -> relative_error_N_FLX_round
242
   . canonic_bounded_prec -> canonic_canonic_mantissa
BOLDO Sylvie's avatar
BOLDO Sylvie committed
243 244 245 246 247
   . B2R_lt_emax -> abs_B2R_lt_emax
   . binary_unicity -> B2FF_inj
   . finite_binary_unicity -> B2R_inj
   . binary_round_sign_correct -> binary_round_aux_correct
   . shl_correct -> shl_align_correct
248 249
   . snd_shl -> snd_shl_align
   . shl_fexp_correct -> shl_align_fexp_correct
BOLDO Sylvie's avatar
BOLDO Sylvie committed
250
   . binary_round_sign_shl_correct -> binary_round_correct
BOLDO Sylvie's avatar
BOLDO Sylvie committed
251

Guillaume Melquiond's avatar
Guillaume Melquiond committed
252 253 254 255
Version 1.4.0:
 - improved efficiency of IEEE-754 addition
 - fixed compilation with Coq 8.3

Guillaume Melquiond's avatar
Guillaume Melquiond committed
256 257 258
Version 1.3:
 - fixed overflow handling in IEEE-754 formats with directed rounding

Guillaume Melquiond's avatar
Guillaume Melquiond committed
259 260 261
Version 1.2:
 - added IEEE-754 binary32 and 64 formats, including infinities and NaN

262 263 264 265 266 267
Version 1.1:
 - simplified effective rounding for negative reals
 - proved monotonicity of exponent functions for common formats

Version 1.0:
 - initial release