From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- flocq/Core/Fcore_FLX.v | 271 ------------------------------------------------- 1 file changed, 271 deletions(-) delete mode 100644 flocq/Core/Fcore_FLX.v (limited to 'flocq/Core/Fcore_FLX.v') diff --git a/flocq/Core/Fcore_FLX.v b/flocq/Core/Fcore_FLX.v deleted file mode 100644 index 55f6db61..00000000 --- a/flocq/Core/Fcore_FLX.v +++ /dev/null @@ -1,271 +0,0 @@ -(** -This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ - -Copyright (C) 2010-2013 Sylvie Boldo -#
# -Copyright (C) 2010-2013 Guillaume Melquiond - -This library is free software; you can redistribute it and/or -modify it under the terms of the GNU Lesser General Public -License as published by the Free Software Foundation; either -version 3 of the License, or (at your option) any later version. - -This library is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -COPYING file for more details. -*) - -(** * Floating-point format without underflow *) -Require Import Fcore_Raux. -Require Import Fcore_defs. -Require Import Fcore_rnd. -Require Import Fcore_generic_fmt. -Require Import Fcore_float_prop. -Require Import Fcore_FIX. -Require Import Fcore_ulp. -Require Import Fcore_rnd_ne. - -Section RND_FLX. - -Variable beta : radix. - -Notation bpow e := (bpow beta e). - -Variable prec : Z. - -Class Prec_gt_0 := - prec_gt_0 : (0 < prec)%Z. - -Context { prec_gt_0_ : Prec_gt_0 }. - -(* unbounded floating-point format *) -Definition FLX_format (x : R) := - exists f : float beta, - x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z. - -Definition FLX_exp (e : Z) := (e - prec)%Z. - -(** Properties of the FLX format *) - -Global Instance FLX_exp_valid : Valid_exp FLX_exp. -Proof. -intros k. -unfold FLX_exp. -generalize prec_gt_0. -repeat split ; intros ; omega. -Qed. - -Theorem FIX_format_FLX : - forall x e, - (bpow (e - 1) <= Rabs x <= bpow e)%R -> - FLX_format x -> - FIX_format beta (e - prec) x. -Proof. -clear prec_gt_0_. -intros x e Hx ((xm, xe), (H1, H2)). -rewrite H1, (F2R_prec_normalize beta xm xe e prec). -now eexists. -exact H2. -now rewrite <- H1. -Qed. - -Theorem FLX_format_generic : - forall x, generic_format beta FLX_exp x -> FLX_format x. -Proof. -intros x H. -rewrite H. -unfold FLX_format. -eexists ; repeat split. -simpl. -apply lt_Z2R. -rewrite Z2R_abs. -rewrite <- scaled_mantissa_generic with (1 := H). -rewrite <- scaled_mantissa_abs. -apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp (Rabs x))). -apply bpow_gt_0. -rewrite scaled_mantissa_mult_bpow. -rewrite Z2R_Zpower, <- bpow_plus. -2: now apply Zlt_le_weak. -unfold canonic_exp, FLX_exp. -ring_simplify (prec + (ln_beta beta (Rabs x) - prec))%Z. -rewrite ln_beta_abs. -destruct (Req_dec x 0) as [Hx|Hx]. -rewrite Hx, Rabs_R0. -apply bpow_gt_0. -destruct (ln_beta beta x) as (ex, Ex). -now apply Ex. -Qed. - -Theorem generic_format_FLX : - forall x, FLX_format x -> generic_format beta FLX_exp x. -Proof. -clear prec_gt_0_. -intros x ((mx,ex),(H1,H2)). -simpl in H2. -rewrite H1. -apply generic_format_F2R. -intros Zmx. -unfold canonic_exp, FLX_exp. -rewrite ln_beta_F2R with (1 := Zmx). -apply Zplus_le_reg_r with (prec - ex)%Z. -ring_simplify. -now apply ln_beta_le_Zpower. -Qed. - -Theorem FLX_format_satisfies_any : - satisfies_any FLX_format. -Proof. -refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). -intros x. -split. -apply FLX_format_generic. -apply generic_format_FLX. -Qed. - -Theorem FLX_format_FIX : - forall x e, - (bpow (e - 1) <= Rabs x <= bpow e)%R -> - FIX_format beta (e - prec) x -> - FLX_format x. -Proof with auto with typeclass_instances. -intros x e Hx Fx. -apply FLX_format_generic. -apply generic_format_FIX in Fx. -revert Fx. -apply generic_inclusion with (e := e)... -apply Zle_refl. -Qed. - -(** unbounded floating-point format with normal mantissas *) -Definition FLXN_format (x : R) := - exists f : float beta, - x = F2R f /\ (x <> R0 -> - Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z. - -Theorem generic_format_FLXN : - forall x, FLXN_format x -> generic_format beta FLX_exp x. -Proof. -intros x ((xm,ex),(H1,H2)). -destruct (Req_dec x 0) as [Zx|Zx]. -rewrite Zx. -apply generic_format_0. -specialize (H2 Zx). -apply generic_format_FLX. -rewrite H1. -eexists ; repeat split. -apply H2. -Qed. - -Theorem FLXN_format_generic : - forall x, generic_format beta FLX_exp x -> FLXN_format x. -Proof. -intros x Hx. -rewrite Hx. -simpl. -eexists ; split. split. -simpl. -rewrite <- Hx. -intros Zx. -split. -(* *) -apply le_Z2R. -rewrite Z2R_Zpower. -2: now apply Zlt_0_le_0_pred. -rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx). -apply Rmult_le_reg_r with (bpow (canonic_exp beta FLX_exp x)). -apply bpow_gt_0. -rewrite <- bpow_plus. -rewrite <- scaled_mantissa_abs. -rewrite <- canonic_exp_abs. -rewrite scaled_mantissa_mult_bpow. -unfold canonic_exp, FLX_exp. -rewrite ln_beta_abs. -ring_simplify (prec - 1 + (ln_beta beta x - prec))%Z. -destruct (ln_beta beta x) as (ex,Ex). -now apply Ex. -(* *) -apply lt_Z2R. -rewrite Z2R_Zpower. -2: now apply Zlt_le_weak. -rewrite Z2R_abs, <- scaled_mantissa_generic with (1 := Hx). -apply Rmult_lt_reg_r with (bpow (canonic_exp beta FLX_exp x)). -apply bpow_gt_0. -rewrite <- bpow_plus. -rewrite <- scaled_mantissa_abs. -rewrite <- canonic_exp_abs. -rewrite scaled_mantissa_mult_bpow. -unfold canonic_exp, FLX_exp. -rewrite ln_beta_abs. -ring_simplify (prec + (ln_beta beta x - prec))%Z. -destruct (ln_beta beta x) as (ex,Ex). -now apply Ex. -Qed. - -Theorem FLXN_format_satisfies_any : - satisfies_any FLXN_format. -Proof. -refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp)). -split ; intros H. -now apply FLXN_format_generic. -now apply generic_format_FLXN. -Qed. - -Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. -Proof. -unfold ulp; rewrite Req_bool_true; trivial. -case (negligible_exp_spec FLX_exp). -intros _; reflexivity. -intros n H2; contradict H2. -unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. -Qed. - -Theorem ulp_FLX_le: forall x, (ulp beta FLX_exp x <= Rabs x * bpow (1-prec))%R. -Proof. -intros x; case (Req_dec x 0); intros Hx. -rewrite Hx, ulp_FLX_0, Rabs_R0. -right; ring. -rewrite ulp_neq_0; try exact Hx. -unfold canonic_exp, FLX_exp. -replace (ln_beta beta x - prec)%Z with ((ln_beta beta x - 1) + (1-prec))%Z by ring. -rewrite bpow_plus. -apply Rmult_le_compat_r. -apply bpow_ge_0. -now apply bpow_ln_beta_le. -Qed. - - -Theorem ulp_FLX_ge: forall x, (Rabs x * bpow (-prec) <= ulp beta FLX_exp x)%R. -Proof. -intros x; case (Req_dec x 0); intros Hx. -rewrite Hx, ulp_FLX_0, Rabs_R0. -right; ring. -rewrite ulp_neq_0; try exact Hx. -unfold canonic_exp, FLX_exp. -unfold Zminus; rewrite bpow_plus. -apply Rmult_le_compat_r. -apply bpow_ge_0. -left; now apply bpow_ln_beta_gt. -Qed. - -(** FLX is a nice format: it has a monotone exponent... *) -Global Instance FLX_exp_monotone : Monotone_exp FLX_exp. -Proof. -intros ex ey Hxy. -now apply Zplus_le_compat_r. -Qed. - -(** and it allows a rounding to nearest, ties to even. *) -Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. - -Global Instance exists_NE_FLX : Exists_NE beta FLX_exp. -Proof. -destruct NE_prop as [H|H]. -now left. -right. -unfold FLX_exp. -split ; omega. -Qed. - -End RND_FLX. -- cgit