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
BOLDO Sylvie's avatar
BOLDO Sylvie committed
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
BOLDO Sylvie's avatar
BOLDO Sylvie committed
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)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
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
BOLDO Sylvie's avatar
BOLDO Sylvie committed
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
BOLDO Sylvie's avatar
BOLDO Sylvie committed
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