NEWS 8.28 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1
2
3
Version 2.5.2:
 - ensured compatibility from Coq 8.4 to 8.6

Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
5
6
Version 2.5.1:
 - ensured compatibility with both Coq 8.4 and 8.5

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

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

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

37
38
39
Version 2.2.1:
 - fixed regeneration of Flocq_version.v

Guillaume Melquiond's avatar
Guillaume Melquiond committed
40
41
42
43
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
44
45
46
47
48
49
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

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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
189
190
191
192
Version 1.4.0:
 - improved efficiency of IEEE-754 addition
 - fixed compilation with Coq 8.3

Guillaume Melquiond's avatar
Guillaume Melquiond committed
193
194
195
Version 1.3:
 - fixed overflow handling in IEEE-754 formats with directed rounding

Guillaume Melquiond's avatar
Guillaume Melquiond committed
196
197
198
Version 1.2:
 - added IEEE-754 binary32 and 64 formats, including infinities and NaN

199
200
201
202
203
204
Version 1.1:
 - simplified effective rounding for negative reals
 - proved monotonicity of exponent functions for common formats

Version 1.0:
 - initial release