Skip to content

Latest commit

 

History

History
312 lines (277 loc) · 11.3 KB

NEWS.md

File metadata and controls

312 lines (277 loc) · 11.3 KB

Version 3.0.0

  • stripped the F*_ prefix from all the file names, renamed some files:
    • Definitions -> Defs
    • Appli -> IEEE754
  • renamed ln_beta into mag
  • renamed canonic_exp into cexp, canonic into canonical
  • renamed all theorems ending with unicity by unique
  • changed FLX_, FIX_, FLT_, FLXN_, FTZ_format into inductive types
  • changed nan_pl into a boolean predicate
  • replaced Z2R with Coq 8.7's IZR
  • removed Zeven and its theorems in favor of Z.even of the standard library
  • modified statements of Rcompare_sqr, ulp_DN, mult_error_FLT, mag_div
  • added theorems about the remainder being in the format (in Div_sqrt_error.v)
  • made Fdiv_core and Fsqrt_core generic with respect to the format
  • renamed theorems 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
    • Rnd_odd_pt_sym -> Rnd_odd_pt_opp_inv
    • 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)
    • round_odd_prop -> round_N_odd
    • double_round_*_beta_ge_* -> round_round_*_radix_ge_*
    • double_round_* -> round_round_*

Version 2.6.1

  • ensured compatibility from Coq 8.4 to 8.8

Version 2.6.0

  • ensured compatibility from Coq 8.4 to 8.7
  • removed some hypotheses on some lemmas of Fcore_ulp
  • added lemmas to Fprop_plus_error
  • improved examples

Version 2.5.2

  • ensured compatibility from Coq 8.4 to 8.6

Version 2.5.1

  • ensured compatibility with both Coq 8.4 and 8.5

Version 2.5.0

  • 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)
  • removed some hypotheses on lemmas of Fprop_relative.v
  • 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

Version 2.4.0

  • moved some lemmas from Fcalc_digits.v to Fcore_digits.v and made them axiom-free
  • added theorems about double rounding being innocuous (Fappli_double_round.v)
  • added example about double rounding in odd radix
  • improved a bit the efficiency of IEEE-754 arithmetic

Version 2.3.0

  • moved some lemmas from Fcalc_digits.v to Fcore_digits.v 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))

Version 2.2.2

  • fixed install target for case-insensitive filesystems

Version 2.2.1

  • fixed regeneration of Flocq_version.v

Version 2.2.0

  • added theorems about rounding to odd and double rounding
  • improved handling of special values of IEEE-754 arithmetic

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

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
  • removed example file Fappli_sqrt_FLT_ne.v
  • 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
  • renamed functions:
    • canonic_exponent -> canonic_exp
    • digits -> Zdigits
    • 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
  • 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
    • abs_F2R -> F2R_Zabs (changed direction)
    • opp_F2R -> F2R_Zopp (changed direction)
    • 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)
    • canonic_exponent_round -> canonic_exp_round_ge
    • 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
    • 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
    • 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
    • generic_relative_error_N -> relative_error_N
    • 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
    • relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
    • 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
    • canonic_bounded_prec -> canonic_canonic_mantissa
    • 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
    • snd_shl -> snd_shl_align
    • shl_fexp_correct -> shl_align_fexp_correct
    • binary_round_sign_shl_correct -> binary_round_correct

Version 1.4.0

  • improved efficiency of IEEE-754 addition
  • fixed compilation with Coq 8.3

Version 1.3

  • fixed overflow handling in IEEE-754 formats with directed rounding

Version 1.2

  • added IEEE-754 binary32 and 64 formats, including infinities and NaN

Version 1.1

  • simplified effective rounding for negative reals
  • proved monotonicity of exponent functions for common formats

Version 1.0

  • initial release