Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit c19941db authored by Sylvie Boldo's avatar Sylvie Boldo
parents 8feaf946 31abb240
......@@ -13,3 +13,7 @@ html
src/Flocq_version.v
*.vo
*.glob
.*.aux
N*.cm*
N*.native
N*.o
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))
Version 2.2.2:
- fixed install target for case-insensitive filesystems
Version 2.2.1:
- fixed regeneration of Flocq_version.v
......
......@@ -27,10 +27,13 @@ FILES = \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_rnd_odd.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v
Appli/Fappli_IEEE_bits.v \
Appli/Fappli_double_round.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
.PHONY: all clean dist doc install
all: $(OBJS)
Remakefile: Remakefile.in config.status
......@@ -71,7 +74,6 @@ EXTRA_DIST = \
REMOVE_FROM_DIST = \
src/Appli/Fappli_Axpy.v \
src/Appli/Fappli_Muller.v \
src/Translate/
dist: $(EXTRA_DIST)
......
AC_INIT([Flocq], [2.2.1],
AC_INIT([Flocq], [2.3.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......@@ -20,17 +20,34 @@ if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
AC_ARG_VAR(COQC, [Coq compiler command [coqc]])
AC_MSG_CHECKING([for coqc])
if test ! "$COQC"; then COQC=`which ${COQBIN}coqc`; fi
if test ! "$COQC"; then
COQC=`which ${COQBIN}coqc`
if test ! "$COQC"; then
AC_MSG_RESULT([not found])
AC_MSG_ERROR([missing Coq compiler])
fi
fi
AC_MSG_RESULT([$COQC])
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then COQDEP=`which ${COQBIN}coqdep`; fi
if test ! "$COQDEP"; then
COQDEP=`which ${COQBIN}coqdep`
if test ! "$COQDEP"; then
AC_MSG_RESULT([not found])
AC_MSG_ERROR([missing Coq dependency analyzer])
fi
fi
AC_MSG_RESULT([$COQDEP])
AC_ARG_VAR(COQDOC, [Coq documentation generator command [coqdoc]])
AC_MSG_CHECKING([for coqdoc])
if test ! "$COQDOC"; then COQDOC=`which ${COQBIN}coqdoc`; fi
if test ! "$COQDOC"; then
COQDOC=`which ${COQBIN}coqdoc`
if test ! "$COQDOC"; then
AC_MSG_RESULT([not found])
fi
fi
AC_MSG_RESULT([$COQDOC])
if test "$libdir" = '${exec_prefix}/lib'; then
......
This diff is collapsed.
This diff is collapsed.
......@@ -46,6 +46,8 @@ End AnyRadix.
Section Binary.
Implicit Arguments exist [[A] [P]].
(** prec is the number of bits of the mantissa including the implicit one
emax is the exponent of the infinities
Typically p=24 and emax = 128 in single precision *)
......@@ -89,7 +91,7 @@ Definition FF2B x :=
| F754_finite s m e => B754_finite s m e
| F754_infinity s => fun _ => B754_infinity s
| F754_zero s => fun _ => B754_zero s
| F754_nan b pl => fun H => B754_nan b (exist _ pl H)
| F754_nan b pl => fun H => B754_nan b (exist pl H)
end.
Definition B2FF x :=
......@@ -601,7 +603,7 @@ induction (nat_of_P n).
simpl.
rewrite Zplus_0_r.
now destruct l as [|[| |]].
simpl iter_nat.
simpl nat_rect.
rewrite inj_S.
unfold Zsucc.
rewrite Zplus_assoc.
......@@ -1601,7 +1603,7 @@ Definition Fsqrt_core_binary m e :=
| Zpos p => (m * Zpower_pos 2 p)%Z
| _ => m
end in
let (q, r) := Zsqrt m' in
let (q, r) := Z.sqrtrem m' in
let l :=
if Zeq_bool r 0 then loc_Exact
else loc_Inexact (if Zle_bool r q then Lt else Gt) in
......
......@@ -25,6 +25,12 @@ Require Import Fappli_IEEE.
Section Binary_Bits.
Implicit Arguments exist [[A] [P]].
Implicit Arguments B754_zero [[prec] [emax]].
Implicit Arguments B754_infinity [[prec] [emax]].
Implicit Arguments B754_nan [[prec] [emax]].
Implicit Arguments B754_finite [[prec] [emax]].
(** Number of bits for the fraction and exponent *)
Variable mw ew : Z.
Hypothesis Hmw : (0 < mw)%Z.
......@@ -248,6 +254,57 @@ discriminate.
now apply Zlt_0_le_0_pred.
Qed.
Theorem bits_of_binary_float_range:
forall x, (0 <= bits_of_binary_float x < 2^(mw+ew+1))%Z.
Proof.
intros.
Local Open Scope Z_scope.
assert (J: forall s m e,
0 <= m < 2^mw -> 0 <= e < 2^ew ->
0 <= join_bits s m e < 2^(mw+ew+1)).
{
intros. unfold join_bits.
set (se := (if s then 2 ^ ew else 0) + e).
assert (0 <= se < 2^(ew+1)).
{ rewrite (Zpower_plus radix2) by omega. change (radix2^1) with 2. simpl.
unfold se. destruct s; omega. }
assert (0 <= se * 2^mw <= (2^(ew+1) - 1) * 2^mw).
{ split. apply Zmult_gt_0_le_0_compat; omega.
apply Zmult_le_compat_r; omega. }
rewrite Z.mul_sub_distr_r in H2.
replace (mw + ew + 1) with ((ew + 1) + mw) by omega.
rewrite (Zpower_plus radix2) by omega. simpl. omega.
}
assert (D: forall p n, Z.of_nat (S (digits2_Pnat p)) <= n ->
0 <= Z.pos p < 2^n).
{
intros.
generalize (digits2_Pnat_correct p). simpl. rewrite ! Zpower_nat_Z. intros [A B].
split. zify; omega. eapply Zlt_le_trans. eassumption.
apply (Zpower_le radix2); auto.
}
destruct x; unfold bits_of_binary_float.
- apply J; omega.
- apply J; omega.
- destruct n as [pl pl_range]. apply Z.ltb_lt in pl_range.
apply J. apply D. unfold prec, Z_of_nat' in pl_range; omega. omega.
- unfold bounded in e0. apply Bool.andb_true_iff in e0; destruct e0 as [A B].
apply Z.leb_le in B.
unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
assert (G: Z.of_nat (S (digits2_Pnat m)) <= prec) by (zify; omega).
assert (M: emin <= e) by (unfold emin; zify; omega).
generalize (Zle_bool_spec (2^mw) (Z.pos m)); intro SPEC; inversion SPEC.
+ apply J.
* split. omega. generalize (D _ _ G). unfold prec.
rewrite (Zpower_plus radix2) by omega.
change (radix2^1) with 2. simpl radix_val. omega.
* split. omega. unfold emin. replace (2^ew) with (2 * emax). omega.
symmetry. replace ew with (1 + (ew - 1)) by omega.
apply (Zpower_plus radix2); omega.
+ apply J. zify; omega. omega.
Local Close Scope Z_scope.
Qed.
Definition binary_float_of_bits_aux x :=
let '(sx, mx, ex) := split_bits x in
if Zeq_bool ex 0 then
......@@ -516,6 +573,8 @@ End Binary_Bits.
(** Specialization for IEEE single precision operations *)
Section B32_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary32 := binary_float 24 128.
Let Hprec : (0 < 24)%Z.
......@@ -527,7 +586,7 @@ apply refl_equal.
Qed.
Definition default_nan_pl32 : bool * nan_pl 24 :=
(false, exist _ (nat_iter 22 xO xH) (refl_equal true)).
(false, exist _ (iter_nat 22 _ xO xH) (refl_equal true)).
Definition unop_nan_pl32 (f : binary32) : bool * nan_pl 24 :=
match f with
......@@ -557,6 +616,8 @@ End B32_Bits.
(** Specialization for IEEE double precision operations *)
Section B64_Bits.
Implicit Arguments B754_nan [[prec] [emax]].
Definition binary64 := binary_float 53 1024.
Let Hprec : (0 < 53)%Z.
......@@ -568,7 +629,7 @@ apply refl_equal.
Qed.
Definition default_nan_pl64 : bool * nan_pl 53 :=
(false, exist _ (nat_iter 51 xO xH) (refl_equal true)).
(false, exist _ (iter_nat 51 _ xO xH) (refl_equal true)).
Definition unop_nan_pl64 (f : binary64) : bool * nan_pl 53 :=
match f with
......
This diff is collapsed.
......@@ -168,7 +168,7 @@ apply Rplus_lt_reg_r with (d * (v - 1))%R.
ring_simplify.
rewrite Rmult_comm.
now apply Rmult_lt_compat_l.
apply Rplus_lt_reg_r with (-u * v)%R.
apply Rplus_lt_reg_l with (-u * v)%R.
replace (- u * v + (d + v * (u - d)))%R with (d * (1 - v))%R by ring.
replace (- u * v + u)%R with (u * (1 - v))%R by ring.
apply Rmult_lt_compat_r.
......
This diff is collapsed.
......@@ -28,6 +28,8 @@ Variable beta : radix.
Notation bpow e := (bpow beta e).
Implicit Arguments Float [[beta]].
Definition Falign (f1 f2 : float beta) :=
let '(Float m1 e1) := f1 in
let '(Float m2 e2) := f2 in
......@@ -38,7 +40,7 @@ Definition Falign (f1 f2 : float beta) :=
Theorem Falign_spec :
forall f1 f2 : float beta,
let '(m1, m2, e) := Falign f1 f2 in
F2R f1 = F2R (Float beta m1 e) /\ F2R f2 = F2R (Float beta m2 e).
F2R f1 = @F2R beta (Float m1 e) /\ F2R f2 = @F2R beta (Float m2 e).
Proof.
unfold Falign.
intros (m1, e1) (m2, e2).
......@@ -61,9 +63,9 @@ case (Zmin_spec e1 e2); intros (H1,H2); easy.
case (Zmin_spec e1 e2); intros (H1,H2); easy.
Qed.
Definition Fopp (f1: float beta) :=
Definition Fopp (f1 : float beta) : float beta :=
let '(Float m1 e1) := f1 in
Float beta (-m1)%Z e1.
Float (-m1)%Z e1.
Theorem F2R_opp :
forall f1 : float beta,
......@@ -72,9 +74,9 @@ intros (m1,e1).
apply F2R_Zopp.
Qed.
Definition Fabs (f1: float beta) :=
Definition Fabs (f1 : float beta) : float beta :=
let '(Float m1 e1) := f1 in
Float beta (Zabs m1)%Z e1.
Float (Zabs m1)%Z e1.
Theorem F2R_abs :
forall f1 : float beta,
......@@ -83,9 +85,9 @@ intros (m1,e1).
apply F2R_Zabs.
Qed.
Definition Fplus (f1 f2 : float beta) :=
Definition Fplus (f1 f2 : float beta) : float beta :=
let '(m1, m2 ,e) := Falign f1 f2 in
Float beta (m1 + m2) e.
Float (m1 + m2) e.
Theorem F2R_plus :
forall f1 f2 : float beta,
......@@ -104,7 +106,7 @@ Qed.
Theorem Fplus_same_exp :
forall m1 m2 e,
Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e.
Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e.
Proof.
intros m1 m2 e.
unfold Fplus.
......@@ -136,17 +138,17 @@ Qed.
Theorem Fminus_same_exp :
forall m1 m2 e,
Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e.
Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e.
Proof.
intros m1 m2 e.
unfold Fminus.
apply Fplus_same_exp.
Qed.
Definition Fmult (f1 f2 : float beta) :=
Definition Fmult (f1 f2 : float beta) : float beta :=
let '(Float m1 e1) := f1 in
let '(Float m2 e2) := f2 in
Float beta (m1 * m2) (e1 + e2).
Float (m1 * m2) (e1 + e2).
Theorem F2R_mult :
forall f1 f2 : float beta,
......
......@@ -28,108 +28,6 @@ Require Import Fcalc_digits.
Section Fcalc_sqrt.
Fixpoint Zsqrt_aux (p : positive) : Z * Z :=
match p with
| xH => (1, 0)%Z
| xO xH => (1, 1)%Z
| xI xH => (1, 2)%Z
| xO (xO p) =>
let (q, r) := Zsqrt_aux p in
let r' := (4 * r)%Z in
let d := (r' - (4 * q + 1))%Z in
if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
| xO (xI p) =>
let (q, r) := Zsqrt_aux p in
let r' := (4 * r + 2)%Z in
let d := (r' - (4 * q + 1))%Z in
if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
| xI (xO p) =>
let (q, r) := Zsqrt_aux p in
let r' := (4 * r + 1)%Z in
let d := (r' - (4 * q + 1))%Z in
if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
| xI (xI p) =>
let (q, r) := Zsqrt_aux p in
let r' := (4 * r + 3)%Z in
let d := (r' - (4 * q + 1))%Z in
if Zlt_bool d 0 then (2 * q, r')%Z else (2 * q + 1, d)%Z
end.
Lemma Zsqrt_ind :
forall P : positive -> Prop,
P xH -> P (xO xH) -> P (xI xH) ->
( forall p, P p -> P (xO (xO p)) /\ P (xO (xI p)) /\ P (xI (xO p)) /\ P (xI (xI p)) ) ->
forall p, P p.
Proof.
intros P H1 H2 H3 Hp.
fix 1.
intros [[p|p|]|[p|p|]|].
refine (proj2 (proj2 (proj2 (Hp p _)))).
apply Zsqrt_ind.
refine (proj1 (proj2 (proj2 (Hp p _)))).
apply Zsqrt_ind.
exact H3.
refine (proj1 (proj2 (Hp p _))).
apply Zsqrt_ind.
refine (proj1 (Hp p _)).
apply Zsqrt_ind.
exact H2.
exact H1.
Qed.
Lemma Zsqrt_aux_correct :
forall p,
let (q, r) := Zsqrt_aux p in
Zpos p = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z.
Proof.
intros p.
elim p using Zsqrt_ind ; clear p.
now repeat split.
now repeat split.
now repeat split.
intros p.
Opaque Zmult. simpl. Transparent Zmult.
destruct (Zsqrt_aux p) as (q, r).
intros (Hq, Hr).
change (Zpos p~0~0) with (4 * Zpos p)%Z.
change (Zpos p~0~1) with (4 * Zpos p + 1)%Z.
change (Zpos p~1~0) with (4 * Zpos p + 2)%Z.
change (Zpos p~1~1) with (4 * Zpos p + 3)%Z.
rewrite Hq. clear Hq.
repeat split.
generalize (Zlt_cases (4 * r - (4 * q + 1)) 0).
case Zlt_bool ; ( split ; [ ring | omega ] ).
generalize (Zlt_cases (4 * r + 2 - (4 * q + 1)) 0).
case Zlt_bool ; ( split ; [ ring | omega ] ).
generalize (Zlt_cases (4 * r + 1 - (4 * q + 1)) 0).
case Zlt_bool ; ( split ; [ ring | omega ] ).
generalize (Zlt_cases (4 * r + 3 - (4 * q + 1)) 0).
case Zlt_bool ; ( split ; [ ring | omega ] ).
Qed.
(** Computes the integer square root and its remainder, but
without carrying a proof, contrarily to the operation of
the standard libary. *)
Definition Zsqrt p :=
match p with
| Zpos p => Zsqrt_aux p
| _ => (0, 0)%Z
end.
Theorem Zsqrt_correct :
forall x,
(0 <= x)%Z ->
let (q, r) := Zsqrt x in
x = (q * q + r)%Z /\ (0 <= r <= 2 * q)%Z.
Proof.
unfold Zsqrt.
intros [|p|p] Hx.
now repeat split.
apply Zsqrt_aux_correct.
now elim Hx.
Qed.
Variable beta : radix.
Notation bpow e := (bpow beta e).
......@@ -160,7 +58,7 @@ Definition Fsqrt_core prec m e :=
| Zpos p => (m * Zpower_pos beta p)%Z
| _ => m
end in
let (q, r) := Zsqrt m' in
let (q, r) := Z.sqrtrem m' in
let l :=
if Zeq_bool r 0 then loc_Exact
else loc_Inexact (if Zle_bool r q then Lt else Gt) in
......@@ -236,8 +134,8 @@ now apply Zpower_gt_0.
now elim He2.
clearbody m'.
destruct Hs as (Hs1, (Hs2, Hs3)).
generalize (Zsqrt_correct m' (Zlt_le_weak _ _ Hs3)).
destruct (Zsqrt m') as (q, r).
generalize (Z.sqrtrem_spec m' (Zlt_le_weak _ _ Hs3)).
destruct (Z.sqrtrem m') as (q, r).
intros (Hq, Hr).
rewrite <- Hs1. clear Hs1.
split.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -325,7 +325,7 @@ destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H.
(* . *)
rewrite Rabs_left1.
rewrite Ropp_minus_distr.
apply Rplus_lt_reg_r with (round beta fexp Zfloor x).
apply Rplus_lt_reg_l with (round beta fexp Zfloor x).
rewrite <- ulp_DN_UP with (1 := Hx).
ring_simplify.
assert (Hu: (x <= round beta fexp Zceil x)%R).
......
......@@ -703,6 +703,42 @@ Qed.
End Fprop_relative_FLT.
Lemma error_N_FLT :
forall (emin prec : Z), (0 < prec)%Z ->
forall (choice : Z -> bool),
forall (x : R),
exists eps eta : R,
(Rabs eps <= /2 * bpow (-prec + 1))%R /\
(Rabs eta <= /2 * bpow emin)%R /\
(eps * eta = 0)%R /\
(round beta (FLT_exp emin prec) (Znearest choice) x
= x * (1 + eps) + eta)%R.
Proof.
intros emin prec Pprec choice x.
destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
{ assert (Pmx : (0 < - x)%R).
{ now rewrite <- Ropp_0; apply Ropp_lt_contravar. }
destruct (error_N_FLT_aux emin prec Pprec
(fun t : Z => negb (choice (- (t + 1))%Z))
(- x)%R Pmx)
as (d,(e,(Hd,(He,(Hde,Hr))))).
exists d; exists (- e)%R; split; [exact Hd|split; [|split]].
{ now rewrite Rabs_Ropp. }
{ now rewrite Ropp_mult_distr_r_reverse, <- Ropp_0; apply f_equal. }
rewrite <- (Ropp_involutive x), round_N_opp.
now rewrite Ropp_mult_distr_l_reverse, <- Ropp_plus_distr; apply f_equal. }
{ assert (Ph2 : (0 <= / 2)%R).
{ apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
apply Rgt_not_eq, Rlt_gt, Rlt_0_2. }
exists R0; exists R0; rewrite Zx; split; [|split; [|split]].
{ now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
{ now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
{ now rewrite Rmult_0_l. }
now rewrite Rmult_0_l, Rplus_0_l, round_0; [|apply valid_rnd_N]. }
now apply error_N_FLT_aux.
Qed.
Section Fprop_relative_FLX.
Variable prec : Z.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment