Commit efe84342 authored by Heiko Becker's avatar Heiko Becker

WIP: Fix binary IEEE conn., lets missing

parent 4eff33b2
From Coq
Require Import Reals.Reals QArith.Qreals.
Require Import Reals.Reals QArith.Qreals QArith.QArith.
From Flover
Require Import ExpressionSemantics Environments RealRangeArith TypeValidator.
Require Import ExpressionSemantics Environments RealRangeArith
Infra.RationalSimps TypeValidator IntervalArithQ.
Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with
......@@ -10,6 +11,12 @@ Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
| Unop Neg e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Binop b e1 e2 =>
(b = Div ->
(forall iv2 err,
FloverMap.find e2 A = Some (iv2, err) ->
let errIv2 := widenIntv iv2 err in
((Qleb (ivhi errIv2) 0) && (negb (Qeq_bool (ivhi errIv2) 0))) ||
((Qleb 0 (ivlo errIv2)) && (negb (Qeq_bool (ivlo errIv2) 0))) = true)) /\
validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap
| Fma e1 e2 e3 =>
......
......@@ -34,6 +34,7 @@ Proof.
intros nR (elo, ehi) err eval_real A_eq.
pose proof (validRanges_single _ _ _ _ valid_intv) as valid_const.
destruct valid_const as [? [ ? [? [? [? ?]]]]].
unfold error in H.
rewrite H in A_eq; inversion A_eq; subst.
rewrite (meps_0_deterministic _ eval_real H0) in *; auto.
split.
......@@ -59,6 +60,7 @@ Proof.
auto.
intros nR (elo, ehi) err eval_real A_eq.
simpl in *.
unfold error in *.
rewrite A_eq in valid_error.
cbn in *; Flover_compute; try congruence; type_conv; subst;
destruct u; Flover_compute; try congruence.
......@@ -68,7 +70,7 @@ Proof.
inversion eval_real; subst.
assert (m0 = REAL) by (eapply toRTMap_eval_REAL; eauto); subst.
specialize (IHe DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv := i) (err := e0) in IHe; eauto.
apply validErrorBoundsRec_single with (v__R := v1) (iv := i) (err := q) in IHe; eauto.
specialize IHe as [[nF [mF eval_float]] valid_bounds_e].
split.
* inversion H; subst.
......@@ -113,21 +115,24 @@ Proof.
intuition.
}
clear IHe2'.
split; auto.
split.
{ repeat split; [ | auto | auto ].
intros; subst.
Opaque mTypeToQ mTypeToR.
cbn in *; Flover_compute; try congruence.
Transparent mTypeToQ mTypeToR.
unfold error in *.
rewrite Heqo2 in H0. inversion H0; subst; auto. }
intros nR (elo, ehi) err eval_real A_eq.
simpl in valid_intv.
destruct valid_intv
as [[nodiv_zero [valid_e1 valid_e2]] valid_bin].
unfold error in *.
cbn in valid_error. Flover_compute; try congruence.
destruct typing_ok as [? [? [[? [? ?]] ?]]]; auto.
inversion eval_real; subst.
assert (m1 = REAL /\ m2 = REAL) as [? ?] by (split; eapply toRTMap_eval_REAL; eauto); subst.
specialize (IHe1 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv := i) (err := e) in IHe1; eauto.
specialize IHe1 as [[nF1 [mF1 eval_float1]] valid_bounds_e1].
specialize (IHe2 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v2) (iv := i0) (err := e0) in IHe2; eauto.
specialize IHe2 as [[nF2 [mF2 eval_float2]] valid_bounds_e2].
apply validRanges_single in valid_e1;
apply validRanges_single in valid_e2.
destruct valid_e1 as [iv1 [ err1 [v1' [map_e1 [eval_real_e1 bounds_e1]]]]].
......@@ -135,9 +140,14 @@ Proof.
pose proof (meps_0_deterministic _ eval_real_e1 H14); subst.
pose proof (meps_0_deterministic _ eval_real_e2 H17); subst.
rewrite map_e1, map_e2 in *.
inversion Heqo0; inversion Heqo1; subst.
rename i into iv1; rename e into err1; rename i0 into iv2;
rename e0 into err2.
inversion Heqo1; inversion Heqo2; subst.
rename e0 into err1; rename i0 into iv1.
rename e3 into err2; rename i1 into iv2.
apply validErrorBoundsRec_single with (v__R := v1) (iv := iv1) (err := err1) in IHe1; eauto.
specialize IHe1 as [[nF1 [mF1 eval_float1]] valid_bounds_e1].
specialize (IHe2 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v2) (iv := iv2) (err := err2) in IHe2; eauto.
specialize IHe2 as [[nF2 [mF2 eval_float2]] valid_bounds_e2].
assert (contained nF1 (widenInterval (Q2R (fst iv1), Q2R (snd iv1)) (Q2R err1)))
as bounds_float_e1.
{ eapply distance_gives_iv; simpl;
......@@ -245,18 +255,6 @@ Proof.
inversion eval_real; subst.
assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]]
by (repeat split; eapply toRTMap_eval_REAL; eauto); subst.
specialize (IHe1 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv := i) (err := e) in IHe1; eauto.
specialize IHe1 as [[nF1 [mF1 eval_float1]] valid_bounds_e1].
specialize (IHe2 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v2) (iv := i0) (err := e0) in IHe2; eauto.
specialize IHe2 as [[nF2 [mF2 eval_float2]] valid_bounds_e2].
specialize (IHe3 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v3) (iv := i1) (err := e4) in IHe3; eauto.
specialize IHe3 as [[nF3 [mF3 eval_float3]] valid_bounds_e3].
assert (m1 = mF1) by (eapply validTypes_exec in find_m1; eauto).
assert (m2 = mF2) by (eapply validTypes_exec in find_m2; eauto).
assert (m3 = mF3) by (eapply validTypes_exec in find_m3; eauto); subst.
apply validRanges_single in valid_e1;
apply validRanges_single in valid_e2;
apply validRanges_single in valid_e3.
......@@ -267,9 +265,20 @@ Proof.
pose proof (meps_0_deterministic _ eval_real_e2 H13); subst.
pose proof (meps_0_deterministic _ eval_real_e3 H14); subst.
rewrite map_e1, map_e2, map_e3 in *.
inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
rename i into iv1; rename e into err1; rename i0 into iv2;
rename e0 into err2; rename i1 into iv3; rename e4 into err3.
symmetry in Heqo1, Heqo2, Heqo3.
inversion Heqo1; inversion Heqo2; inversion Heqo3; subst.
specialize (IHe1 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv := iv1) (err := err1) in IHe1; eauto.
specialize IHe1 as [[nF1 [mF1 eval_float1]] valid_bounds_e1].
specialize (IHe2 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v2) (iv := iv2) (err := err2) in IHe2; eauto.
specialize IHe2 as [[nF2 [mF2 eval_float2]] valid_bounds_e2].
specialize (IHe3 DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v3) (iv := iv3) (err := err3) in IHe3; eauto.
specialize IHe3 as [[nF3 [mF3 eval_float3]] valid_bounds_e3].
assert (m1 = mF1) by (eapply validTypes_exec in find_m1; eauto).
assert (m2 = mF2) by (eapply validTypes_exec in find_m2; eauto).
assert (m3 = mF3) by (eapply validTypes_exec in find_m3; eauto); subst.
assert (contained nF1 (widenInterval (Q2R (fst iv1), Q2R (snd iv1)) (Q2R err1)))
as bounds_float_e1.
{ eapply distance_gives_iv; simpl;
......@@ -291,9 +300,10 @@ Proof.
inversion eval_float; subst.
eapply (fma_unfolding H16 H12 H17 H20 H21) in eval_float; try auto.
eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) A); eauto.
{ simpl.
{ simpl. unfold error in *.
rewrite A_eq.
rewrite Heqo.
rewrite Heqo0.
rewrite Heqo in A_eq; inversion A_eq; subst.
rewrite R, L0, L, R1; simpl.
rewrite map_e1, map_e2, map_e3.
inversion Heqo0; subst.
......@@ -317,6 +327,7 @@ Proof.
clear IHe'.
split; auto.
intros nR (elo, ehi) err eval_real A_eq.
unfold error in *.
cbn in *; Flover_compute; try congruence; type_conv; subst.
inversion eval_real; subst.
apply REAL_least_precision in H4; subst.
......@@ -324,13 +335,14 @@ Proof.
destruct valid_intv as [valid_e1 valid_intv].
destruct typing_ok as [mG [find_m [[valid_e [? [m1 [find_e1 morePrecise_m1]]]] valid_exec]]].
specialize (IHe DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv := (ivlo_e, ivhi_e)) (err := err_e) in IHe;
apply validErrorBoundsRec_single with (v__R := v1) (iv := i0) (err := e1) in IHe;
eauto.
specialize IHe as [[vF [mF eval_float_e]] bounded_e].
assert (mF = m1) by (eapply validTypes_exec in find_e1; eauto); subst.
apply validRanges_single in valid_e1.
destruct valid_e1 as [iv1' [err1' [v1' [map_e [eval_real_e bounds_e]]]]].
rewrite map_e in Heqo0; inversion Heqo0; subst.
unfold error in *.
rewrite map_e in Heqo1; inversion Heqo1; subst.
pose proof (meps_0_deterministic _ eval_real_e H7); subst. clear H7.
split.
+ specialize (deltas_matched (vF) mG)
......@@ -345,8 +357,11 @@ Proof.
{ constructor; cbn; auto. }
{ destruct Req_dec_sum as [Heq|Hneq]; auto; congruence. }
{ unfold updDefVars; cbn. rewrite mTypeEq_refl. auto. }
* cbn; instantiate (1:=dVars); Flover_compute.
* cbn; instantiate (1:=dVars).
unfold error in *; Flover_compute.
rewrite Heqo in A_eq. inversion A_eq; subst.
rewrite L, L0; auto.
* destruct i0; auto.
* eapply toRExpMap_find_map; eauto.
- inversion ssa_f; subst.
assert (NatSet.Subset (freeVars e1 -- dVars) fVars) as valid_varset.
......@@ -446,7 +461,7 @@ Proof.
subst. *)
assert (Herr: Q2R err = Q2R e4).
{ apply RMicromega.Qeq_true in R1.
rewrite R1. congruence. }
rewrite R1. unfold error in *; congruence. }
rewrite Herr.
assert (validErrorBounds e2 (updEnv n v1 E1) (updEnv n v0 E2) A Gamma).
{ eapply IHe2; eauto.
......
This diff is collapsed.
......@@ -135,6 +135,16 @@ Ltac validTypes_split :=
assert (validTypes e Gamma)
as n
by (destruct H as [? [? [[? ?] ?]]]; eauto)
| [ H: validTypes (Let ?m ?x ?e1 ?e2) ?Gamma |- _] =>
let n1 := fresh "valid_arg" in
let n2 := fresh "valid_arg" in
assert (validTypes e1 Gamma)
as n1
by (destruct H as [? [? [[? [? ?]] ?]]]; auto);
assert (validTypes e2 Gamma)
as n2
by (destruct H as [? [? [[? [? ?]] ?]]]; auto)
end.
Ltac validTypes_simp :=
......
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