Commit 18e07778 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'WIP_fix_broken_Flover_compute' into 'master'

Fix Flover compute handling of new notations.

See merge request AVA/FloVer!3
parents ddc04b14 285be625
......@@ -10,12 +10,6 @@ Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024.
Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
match e with
| Some v => some_cont v
| None => none_cont
end.
Definition normal_or_zero v :=
(v = 0 \/ (Q2R (minValue_pos M64)) <= (Rabs v))%R.
......@@ -55,15 +49,15 @@ Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):
Fixpoint bstep_float f E :option fl64 :=
match f with
| Let m x e g => optionLift (eval_expr_float e E)
(fun v => bstep_float g (updFlEnv x v E))
None
| Let m x e g =>
olet res := eval_expr_float e E in
bstep_float g (updFlEnv x res E)
| Ret e => eval_expr_float e E
end.
Definition isValid e :=
let trans_e := optionLift e (fun v => Some (B2R 53 1024 v)) None in
optionLift trans_e normal_or_zero False.
plet v := e in
normal_or_zero (B2R 53 1024 v).
Fixpoint eval_expr_valid (e:expr fl64) E :=
match e with
......@@ -74,10 +68,10 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
optionLift e1_res
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
normal_or_zero (evalBinop b v1_real v2_real))
......@@ -88,13 +82,13 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
let e3_res := eval_expr_float e3 E in
optionLift e1_res
optionBind e1_res
(fun v1 =>
let v1_real := B2R 53 1024 v1 in
optionLift e2_res
optionBind e2_res
(fun v2 =>
let v2_real := B2R 53 1024 v2 in
optionLift e3_res
optionBind e3_res
(fun v3 =>
let v3_real := B2R 53 1024 v3 in
(* No support for fma yet *)
......@@ -110,7 +104,7 @@ Fixpoint bstep_valid f E :=
match f with
| Let m x e g =>
eval_expr_valid e E /\
(optionLift (eval_expr_float e E)
(optionBind (eval_expr_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_expr_valid e E
......@@ -505,24 +499,26 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
eval_expr_float e E2 = Some v /\
eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
Proof.
induction e; simpl in *;
induction e; simpl in *;
intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
valid_roundoffs valid_float_ranges eval_e_float
usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
fVars_defined vars_typed dVars_sound dVars_valid
usedVars_64bit;
(match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
revert eval_IEEE_valid_e;
Flover_compute_asm; try congruence; type_conv; subst;
unfold Ltacs.optionLift.
- unfold toREnv in *.
unfold optionBind;
intros eval_IEEE_valid_e.
- unfold toREnv in *.
destruct (E2 n) eqn:HE2; try congruence.
exists f; split; try eauto.
eapply Var_load; try auto. rewrite HE2; auto.
- eexists; split; try eauto.
- eexists; split; try eauto.
eapply (Const_dist') with (delta:=0%R); eauto.
+ rewrite Rabs_R0; apply mTypeToR_pos_R.
+ unfold perturb. lra.
- edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
- edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
assert (is_finite 53 1024 v_e = true).
{ apply validValue_is_finite.
eapply FPRangeValidator_sound; eauto.
......@@ -533,10 +529,10 @@ Proof.
rewrite B2Q_B2R_eq; auto. rewrite B2R_Bopp.
eapply Unop_neg'; eauto.
unfold evalUnop. rewrite is_finite_Bopp in H. rewrite B2Q_B2R_eq; auto.
- repeat (match goal with
- repeat (match goal with
|H: _ /\ _ |- _ => destruct H
end).
assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
as [tMap_e1 [tMap_e2 tMap_b]].
......@@ -562,10 +558,11 @@ Proof.
as [v_e2 [eval_float_e2 eval_rel_e2]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
rewrite eval_float_e1, eval_float_e2.
edestruct (validIntervalbounds_sound (B2Qexpr e2))
as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]];
eauto; set_tac.
rewrite eval_float_e1, eval_float_e2.
inversion Heqo1; subst.
destr_factorize.
destruct iv_2 as [ivlo_2 ivhi_2].
assert (forall vF2 m2,
......@@ -605,10 +602,9 @@ Proof.
apply Is_true_eq_true.
repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
apply andb_prop_intro; split; auto using Is_true_eq_left.
- inversion Heqo1; subst. rewrite Heqo0. rewrite Heqo.
- Flover_compute.
apply Is_true_eq_true.
repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left.
rewrite Heqo3, Heqo5.
apply Is_true_eq_left. inversion Heqo2; subst. auto.
- rewrite Heqo, Heqo0.
apply Is_true_eq_true.
......@@ -675,10 +671,11 @@ Proof.
(-1022)%Z 53%Z expr_valid)
as rel_error_exists.
rewrite eval_float_e1, eval_float_e2 in H1.
unfold optionLift, normal_or_zero in *; simpl in *.
unfold optionBind, normal_or_zero in *; simpl in *.
assert (Normal (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) M64 \/
(evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2)) = 0)%R.
{ revert H1; intros case_val. destruct case_val; try auto.
{ revert H1; intros case_val.
destruct case_val as [eval_is_zero | eval_normal]; try auto.
left; unfold Normal, Denormal in H15; unfold Normal;
destruct H15 as [normal_b | [denormal_b |zero_b]].
- repeat rewrite <- B2Q_B2R_eq; try auto.
......@@ -690,14 +687,16 @@ Proof.
- rewrite B2Q_B2R_eq in zero_b; auto.
rewrite B2Q_B2R_eq in zero_b; auto.
rewrite zero_b in *.
rewrite Rabs_R0 in H1.
unfold minValue_pos, minExponentPos in H1.
rewrite Q2R_inv in H1; [|vm_compute; congruence].
unfold Q2R, Qnum, Qden in H1.
rewrite Rabs_R0 in eval_normal.
unfold minValue_pos, minExponentPos in eval_normal.
rewrite Q2R_inv in eval_normal; [|vm_compute; congruence].
unfold Q2R, Qnum, Qden in eval_normal.
assert (Z.pow_pos 2 1022 = 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304%Z)
by (vm_compute; auto).
rewrite H2 in H1. rewrite <- Z2R_IZR in H1. unfold IZR in H1.
simpl in H1. rewrite <- INR_IPR in H1. simpl in H1. lra. }
rewrite H1 in eval_normal. rewrite <- Z2R_IZR in eval_normal.
unfold IZR in eval_normal.
simpl in eval_normal. rewrite <- INR_IPR in eval_normal.
simpl in eval_normal. lra. }
pose proof (validValue_bounded b v_e1 v_e2 H2 H18) as cond_valid.
destruct b; revert H1; intros case_eval.
(* Addition *)
......@@ -896,7 +895,7 @@ Proof.
as [v_e3 [eval_float_e3 eval_rel_e3]];
try auto; try set_tac;
[ intros; apply usedVars_64bit ; set_tac | ].
unfold optionLift in H4.
unfold optionBind in H4.
rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
contradiction H4.
- inversion noDowncast_e.
......@@ -936,8 +935,11 @@ Proof.
freeVars_sound is64_eval nodowncast_f bstep_sound
dVars_sound fVars_defined vars_typed dVars_valid
freeVars_typed;
cbn in *; Flover_compute_asm; try congruence; type_conv; subst;
unfold Ltacs.optionLift;
cbn in *;
revert bstep_sound;
Flover_compute_asm; try congruence; type_conv; subst;
intros bstep_sound;
unfold Ltacs.optionBind;
inversion bstep_float; inversion bstep_real;
inversion ssa_f; subst; simpl in *;
repeat (match goal with
......@@ -1052,7 +1054,7 @@ Proof.
destruct H1 as [HA |[HB | HC]]; try auto; congruence.
- destruct iv_ret; auto.
}
unfold optionLift. rewrite eval_float_e.
unfold optionBind. rewrite eval_float_e.
assert (FloverMap.find (getRetExp (B2Qcmd f)) tMap= Some M64).
{ eapply typingSoundnessCmd; eauto. }
destruct H1 as [vF_new [m_f bstep_float_new]].
......@@ -1094,7 +1096,7 @@ Proof.
+ destruct is64_eval as [HA [HB HC]]; auto.
+ destruct nodowncast_f as [HA HB]; auto.
+ destruct bstep_sound as [eval_sound bstep_sound].
rewrite eval_float_e in bstep_sound; unfold optionLift in bstep_sound.
rewrite eval_float_e in bstep_sound; unfold optionBind in bstep_sound.
auto.
+ unfold dVars_range_valid in *; intros; unfold updEnv.
destruct (v1 =? n) eqn:?.
......
(**
(*
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.MachineType.
Global Set Implicit Arguments.
(**
We define Intervals twice.
First we define intervals of reals and fractions.
......@@ -62,15 +61,3 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) :=
if (y =? x) then Some m else defVars y.
Definition optionLift (V T:Type) (v:option V) default (f: V -> T) :=
match v with
| None => default
| Some val => f val
end.
Ltac optionD :=
match goal with
|H: context[optionLift ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
\ No newline at end of file
......@@ -2,6 +2,8 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Global Set Implicit Arguments.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
......@@ -55,42 +57,57 @@ Ltac Q2R_to_head_step :=
Ltac Q2R_to_head := repeat Q2R_to_head_step.
Definition optionLift (X Y:Type) (v:option X) (f:X -> Y) (e:Y) :=
Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
match v with
|Some val => f val
| Some v => f v
| None => e
end.
Lemma optionLift_eq (X Y:Type) v (f:X -> Y) (e:Y):
match v with |Some val => f val | None => e end = optionLift X Y v f e.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
(only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
(only parsing, at level 0, t at level 200).
Ltac optionD :=
match goal with
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
match v with |Some val => f val | None => e end = optionBind v f e.
Proof.
reflexivity.
Qed.
Lemma optionLift_cond X (a:bool) (b c :X):
Lemma optionBind_cond X (a:bool) (b c: X):
(if a then b else c) = match a with |true => b |false => c end.
Proof.
reflexivity.
Qed.
Ltac remove_matches := rewrite optionLift_eq in *.
Ltac remove_matches := rewrite optionBind_eq in *.
Ltac remove_matches_asm := rewrite optionBind_eq in * |- .
Ltac remove_conds := rewrite <- andb_lazy_alt, optionLift_cond in *.
Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
Ltac match_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [optionLift _ _ ?t _ _]]
| [ H: ?t = ?u |- context [optionBind ?t _ _]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [optionLift _ _ ?t _ _] |- _ ]
| [ H1: ?t = ?u, H2: context [optionBind ?t _ _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [optionLift _ _ ?t _ _] |- _ ]
| [ H: context [optionBind ?t _ _] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac match_factorize :=
match_factorize_asm ||
match goal with
| [ |- context [optionLift _ _ ?t _ _] ]
| [ |- context [optionBind ?t _ _] ]
=> destruct t eqn:?; cbn; try congruence
end.
......@@ -120,8 +137,8 @@ Ltac bool_factorize :=
Ltac Flover_compute_asm :=
repeat (
(try remove_conds;
try remove_matches;
(try remove_conds_asm;
try remove_matches_asm;
repeat match_factorize_asm;
try pair_factorize) ||
bool_factorize).
......@@ -152,7 +169,7 @@ Ltac Flover_compute :=
(* Ltac match_destr t:= *)
(* match goal with *)
(* | H: context [optionLift (FloverMap.find ?k ?M) _ _] |- _ => *)
(* | H: context [optionBind (FloverMap.find ?k ?M) _ _] |- _ => *)
(* destruct (FloverMap.find (elt:=intv * error) k M); idtac H *)
(* end. *)
......@@ -179,4 +196,4 @@ Ltac destruct_ex H pat :=
| _ => destruct H as pat
end.
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
\ No newline at end of file
Tactic Notation "destruct_smart" simple_intropattern(pat) hyp(H) := destruct_ex H pat.
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