Commit ebcdc69c authored by Heiko Becker's avatar Heiko Becker

Define no overflow and no underflow functions

parent 60b6db5f
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
(*Require Import Flocq.Prop.Fprop_relative Flocq.Core.Fcore_defs Flocq.Calc.Fcalc_ops Flocq.Calc.Fcalc_div. *)
Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.micromega.Psatz
Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps
Daisy.Infra.RealRationalProps.
Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
Definition valid_div a b (f:binary_float a b):=
match f with
......@@ -40,7 +40,38 @@ Fixpoint toRExp e :=
Definition toREnv E :env:= fun x:nat => match E x with
|None => None
|Some c => Some (B2R 53 1024 c)
end.
end.
Definition Binop_to_Rop (b:binop) :=
match b with
|Plus => Rplus
|Sub => Rminus
|Mult => Rmult
|Div => Rdiv
end.
Definition no_overflow b fl1 fl2 :=
(* TODO: Connect to evaluation *)
let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in
(Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
the_val ))
(bpow radix2 1024) = true).
(* TODO: Maybe move to Prop *)
Definition no_underflow b fl1 fl2 :=
let the_val := (Binop_to_Rop b) (B2R 53 1024 fl1) (B2R 53 1024 fl2) in
(Rlt_bool
(bpow radix2 (-1022))
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
the_val))
= true).
Lemma b64_plus_preserves_finite f1 f2:
is_finite 53 1024 (b64_plus mode_NE f1 f2) = true ->
......@@ -110,21 +141,11 @@ Qed.
Theorem eval_gives_sem e E v:
eval_exp_float e E = Some v ->
(forall e E v,
eval_exp_float e E = Some v ->
(Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 v)))
(bpow radix2 1024) = false)
-> False) ->
is_finite 53 1024 v = true ->
eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e) (B2R 53 1024 v).
Proof.
revert v; induction e;
intros v1 eval_succeeds no_overflow finite_res;
intros v1 eval_succeeds (*no_overflow*) finite_res;
simpl in eval_succeeds.
- econstructor.
unfold toREnv.
......@@ -147,9 +168,9 @@ Proof.
case_eq (eval_exp_float e2 E); intros * eval_float_e2;
rewrite eval_float_e1, eval_float_e2 in *;
try congruence.
specialize (IHe1 b0 (refl_equal (Some b0)) no_overflow);
(* specialize (IHe1 b0 (refl_equal (Some b0)) no_overflow);
specialize (IHe2 b1 (refl_equal (Some b1)) no_overflow).
specialize (no_overflow (Binop b e1 e2) E).
specialize (no_overflow (Binop b e1 e2) E). *)
simpl.
pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
pose proof (relative_error_N_ex radix2
......
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