NEWS 8.22 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2 3
Version 2.5.1:
 - ensured compatibility with both Coq 8.4 and 8.5

BOLDO Sylvie's avatar
BOLDO Sylvie committed
4
Version 2.5.0:
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5 6 7 8 9 10
 - 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
11
 - removed some hypotheses on lemmas of Fprop_relative
Guillaume Melquiond's avatar
Guillaume Melquiond committed
12 13 14 15 16 17 18
 - 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
19

Guillaume Melquiond's avatar
Guillaume Melquiond committed
20 21 22
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)
23
 - added example about double rounding in odd radix
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24 25
 - improved a bit the efficiency of IEEE-754 arithmetic

Guillaume Melquiond's avatar
Guillaume Melquiond committed
26 27 28 29 30
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
31 32 33
Version 2.2.2:
 - fixed install target for case-insensitive filesystems

34 35 36
Version 2.2.1:
 - fixed regeneration of Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
37 38 39 40
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
41 42 43 44 45 46
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

47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
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
67
 - removed example file Fappli_sqrt_FLT_ne
68 69 70 71 72 73 74 75 76 77 78 79 80 81
 - 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
82 83 84
 - renamed functions:
   . canonic_exponent -> canonic_exp
   . digits -> Zdigits
BOLDO Sylvie's avatar
BOLDO Sylvie committed
85 86 87 88 89 90
   . 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
91 92 93 94 95
 - 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
96 97
   . abs_F2R -> F2R_Zabs (changed direction)
   . opp_F2R -> F2R_Zopp (changed direction)
98 99 100 101 102 103 104
   . 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)
105
   . canonic_exponent_round -> canonic_exp_round_ge
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
   . 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
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155
   . 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
156 157 158 159 160 161
   . 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
162
   . generic_relative_error_N -> relative_error_N
BOLDO Sylvie's avatar
BOLDO Sylvie committed
163 164 165 166 167 168
   . 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
169
   . relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
BOLDO Sylvie's avatar
BOLDO Sylvie committed
170 171 172 173 174 175
   . 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
176
   . canonic_bounded_prec -> canonic_canonic_mantissa
BOLDO Sylvie's avatar
BOLDO Sylvie committed
177 178 179 180 181
   . 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
182 183
   . snd_shl -> snd_shl_align
   . shl_fexp_correct -> shl_align_fexp_correct
BOLDO Sylvie's avatar
BOLDO Sylvie committed
184
   . binary_round_sign_shl_correct -> binary_round_correct
185

Guillaume Melquiond's avatar
Guillaume Melquiond committed
186 187 188 189
Version 1.4.0:
 - improved efficiency of IEEE-754 addition
 - fixed compilation with Coq 8.3

Guillaume Melquiond's avatar
Guillaume Melquiond committed
190 191 192
Version 1.3:
 - fixed overflow handling in IEEE-754 formats with directed rounding

Guillaume Melquiond's avatar
Guillaume Melquiond committed
193 194 195
Version 1.2:
 - added IEEE-754 binary32 and 64 formats, including infinities and NaN

196 197 198 199 200 201
Version 1.1:
 - simplified effective rounding for negative reals
 - proved monotonicity of exponent functions for common formats

Version 1.0:
 - initial release