Commit 527d291e authored by Heiko Becker's avatar Heiko Becker

Merge branch 'errors_affine' into 'master'

Errors affine

See merge request AVA/FloVer!14
parents b32487f9 22a9baa7
......@@ -60,6 +60,14 @@ Proof.
congruence.
Qed.
Lemma fresh_from_interval n m iv:
(n < m)%nat -> fresh m (fromInterval iv n).
Proof.
intros Hle.
unfold fresh, get_max_index, fromInterval.
destruct Req_dec_sum; cbn; lia.
Qed.
Definition above_zero a := 0 < (IVlo (toInterval a)).
Definition below_zero a := (IVhi (toInterval a)) < 0.
......@@ -428,7 +436,7 @@ Proof.
split; Flover_compute.
Qed.
Lemma plus_aff_preserves_fresh a1 a2 n:
Lemma plus_aff_fresh_compat a1 a2 n:
fresh n a1 ->
fresh n a2 ->
fresh n (plus_aff a1 a2).
......@@ -770,7 +778,7 @@ Proof.
now rewrite neqn.
Qed.
Lemma mult_aff_aux_preserves_fresh a1 a2 n:
Lemma mult_aff_aux_fresh_compat a1 a2 n:
fresh n a1 ->
fresh n a2 ->
fresh n (mult_aff_aux (a1, a2)).
......@@ -804,7 +812,7 @@ Proof.
unfold af_evals in *.
assert (af_evals (mult_aff_aux (a1, a2)) (v1 * v2 - q * radius a1 * radius a2) (updMap map n q))
as Heq.
{ pose proof (mult_aff_aux_preserves_fresh fresh1 fresh2) as freshmult.
{ pose proof (mult_aff_aux_fresh_compat fresh1 fresh2) as freshmult.
pose proof (eval_updMap_compat map q freshmult) as Heq'.
rewrite Heq' in bounds.
unfold af_evals.
......@@ -844,7 +852,7 @@ Proof.
by (unfold fresh, get_max_index; simpl; omega).
pose proof (mult_aff_sound _ _ _ fresh1 fresh2 evals1 evals2) as [q evalsm].
unfold af_evals in evalsm |-*.
pose proof (mult_aff_aux_preserves_fresh fresh1 fresh2) as freshm.
pose proof (mult_aff_aux_fresh_compat fresh1 fresh2) as freshm.
pose proof (eval_updMap_compat map q freshm) as mapcompat.
unfold mult_aff in evalsm.
rewrite Hr' in evalsm.
......@@ -1254,7 +1262,7 @@ Qed.
(***************** Division *****************)
(********************************************)
Lemma fresh_mult_aff_const a c n:
Lemma mult_aff_const_fresh_compat a c n:
fresh n a ->
fresh n (mult_aff_const a c).
Proof.
......@@ -1263,23 +1271,23 @@ Proof.
simpl.
replace (radius a * 0) with 0 by lra.
destruct Req_dec_sum as [_ | H]; try contradiction.
apply mult_aff_aux_preserves_fresh; try assumption.
apply mult_aff_aux_fresh_compat; try assumption.
unfold fresh, get_max_index in *.
simpl; omega.
Qed.
Lemma fresh_plus_aff_const a c n:
Lemma plus_aff_const_fresh_compat a c n:
fresh n a ->
fresh n (plus_aff_const a c).
Proof.
intros fr.
unfold plus_aff_const, plus_aff.
apply plus_aff_preserves_fresh; try assumption.
apply plus_aff_fresh_compat; try assumption.
unfold fresh, get_max_index in *.
simpl; omega.
Qed.
Lemma fresh_inverse_aff a (n: nat):
Lemma inverse_aff_fresh_compat a (n: nat):
fresh n a ->
fresh (n + 1) (inverse_aff a n).
Proof.
......@@ -1288,8 +1296,8 @@ Proof.
destruct (Rlt_dec (IVhi (toInterval a)) 0).
Set Default Goal Selector "all".
apply fresh_noise; try omega.
apply fresh_plus_aff_const.
apply fresh_mult_aff_const.
apply plus_aff_const_fresh_compat.
apply mult_aff_const_fresh_compat.
now apply fresh_inc.
Set Default Goal Selector "1".
Qed.
......@@ -1336,7 +1344,7 @@ Proof.
pose proof (above_below_nonzero _ bounds2 evals2) as v2nonzero.
specialize (inv a2 v2 map n fresh2 bounds2 evals2) as [qInv evalsi].
pose proof mult_aff_sound as mul.
apply fresh_inverse_aff in fresh2.
apply inverse_aff_fresh_compat in fresh2.
unfold af_evals in evals1.
rewrite (eval_updMap_compat _ qInv fresh1) in evals1.
apply fresh_inc in fresh1.
......
......@@ -378,7 +378,7 @@ Proof.
split; intros; Flover_compute; simpl in *; try auto.
Qed.
Lemma plus_aff_preserves_fresh a1 a2 n:
Lemma plus_aff_fresh_compat a1 a2 n:
fresh n a1 ->
fresh n a2 ->
fresh n (plus_aff a1 a2).
......@@ -732,7 +732,7 @@ Proof.
now rewrite neqn.
Qed.
Lemma mult_aff_aux_preserves_fresh a1 a2 n:
Lemma mult_aff_aux_fresh_compat a1 a2 n:
fresh n a1 ->
fresh n a2 ->
fresh n (mult_aff_aux (a1, a2)).
......@@ -766,7 +766,7 @@ Proof.
unfold af_evals in *.
assert (af_evals (mult_aff_aux (a1, a2)) (v1 * v2 - q * radius a1 * radius a2) (updMap map n q))
as Heq.
{ pose proof (mult_aff_aux_preserves_fresh fresh1 fresh2) as freshmult.
{ pose proof (mult_aff_aux_fresh_compat fresh1 fresh2) as freshmult.
pose proof (eval_updMap_compat map q freshmult) as Heq'.
rewrite Heq' in bounds.
unfold af_evals.
......@@ -807,7 +807,7 @@ Proof.
by (unfold fresh, get_max_index; simpl; omega).
pose proof (mult_aff_sound _ _ _ fresh1 fresh2 evals1 evals2) as [q evalsm].
unfold af_evals in evalsm |-*.
pose proof (mult_aff_aux_preserves_fresh fresh1 fresh2) as freshm.
pose proof (mult_aff_aux_fresh_compat fresh1 fresh2) as freshm.
pose proof (eval_updMap_compat map q freshm) as mapcompat.
unfold mult_aff in evalsm |-*.
rewrite mapcompat.
......@@ -1223,7 +1223,7 @@ Qed.
(***************** Division *****************)
(********************************************)
Lemma fresh_mult_aff_const a c n:
Lemma mult_aff_const_fresh_compat a c n:
fresh n a ->
fresh n (mult_aff_const a c).
Proof.
......@@ -1233,23 +1233,23 @@ Proof.
assert (Qeq_bool 0 0 = true) by trivial.
rewrite H.
rewrite orb_true_r.
apply mult_aff_aux_preserves_fresh; try assumption.
apply mult_aff_aux_fresh_compat; try assumption.
unfold fresh, get_max_index in *.
simpl; omega.
Qed.
Lemma fresh_plus_aff_const a c n:
Lemma plus_aff_const_fresh_compat a c n:
fresh n a ->
fresh n (plus_aff_const a c).
Proof.
intros fr.
unfold plus_aff_const, plus_aff.
apply plus_aff_preserves_fresh; try assumption.
apply plus_aff_fresh_compat; try assumption.
unfold fresh, get_max_index in *.
simpl; omega.
Qed.
Lemma fresh_inverse_aff a (n: nat):
Lemma inverse_aff_fresh_compat a (n: nat):
fresh n a ->
fresh (n + 1) (inverse_aff a n).
Proof.
......@@ -1258,8 +1258,8 @@ Proof.
destruct (Qlt_bool (ivhi (toIntv a)) 0).
Set Default Goal Selector "all".
apply fresh_noise; try omega.
apply fresh_plus_aff_const.
apply fresh_mult_aff_const.
apply plus_aff_const_fresh_compat.
apply mult_aff_const_fresh_compat.
now apply fresh_inc.
Set Default Goal Selector "1".
Qed.
......@@ -1306,7 +1306,7 @@ Proof.
pose proof (above_below_nonzero _ bounds2 evals2) as v2nonzero.
specialize (inv a2 v2 map n fresh2 bounds2 evals2) as [qInv evalsi].
pose proof mult_aff_sound as mul.
apply fresh_inverse_aff in fresh2.
apply inverse_aff_fresh_compat in fresh2.
unfold af_evals in evals1.
rewrite (eval_updMap_compat _ qInv fresh1) in evals1.
apply fresh_inc in fresh1.
......
This diff is collapsed.
......@@ -29,7 +29,9 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
forall (E1 E2:env) DeltaMap,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
......@@ -38,17 +40,17 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * P_valid certificate_valid.
intros * deltas_matched P_valid certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
rename t into Gamma.
......@@ -77,9 +79,13 @@ Proof.
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
exists Gamma; intros approxE1E2.
edestruct (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
valid_e map_e)
as [[vF [mF eval_float]] err_bounded]; auto.
assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real R
valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound.
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
......@@ -98,8 +104,10 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars:
defVars DeltaMap:
forall (E1 E2:env),
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
......@@ -108,17 +116,17 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
(forall vF m,
bstep (toRCmd f) E2 (toRExpMap Gamma) vF m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m ->
(Rabs (vR - vF) <= Q2R (err))%R).
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * P_valid certificate_valid.
intros * deltas_matched P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence.
......@@ -149,6 +157,9 @@ Proof.
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
pose proof RoundoffErrorValidatorCmd_sound as Hsound.
eapply validErrorBoundsCmd_single in Hsound; eauto.
2: unfold dVars_contained; intros; set_tac.
specialize Hsound as ((vF & mF & eval_float) & ?).
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
Qed.
......@@ -48,14 +48,15 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> R -> mType -> Prop :=
let_b m m' x e s E v res defVars:
eval_expr E defVars e v m ->
bstep s (updEnv x v E) defVars res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars res m'
|ret_b m e E v defVars:
eval_expr E defVars e v m ->
bstep (Ret e) E defVars v m.
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (expr R -> mType -> option R) ->
R -> mType -> Prop :=
let_b m m' x e s E v res defVars DeltaMap:
eval_expr E defVars DeltaMap e v m ->
bstep s (updEnv x v E) defVars DeltaMap res m' -> (* (updDefVars (Var R x) m defVars) res m' -> *)
bstep (Let m x e s) E defVars DeltaMap res m'
|ret_b m e E v defVars DeltaMap:
eval_expr E defVars DeltaMap e v m ->
bstep (Ret e) E defVars DeltaMap v m.
(**
The free variables of a command are all used variables of exprressions
......@@ -87,14 +88,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
end.
Lemma bstep_eq_env f:
forall E1 E2 Gamma v m,
forall E1 E2 Gamma DeltaMap v m,
(forall x, E1 x = E2 x) ->
bstep f E1 Gamma v m ->
bstep f E2 Gamma v m.
bstep f E1 Gamma DeltaMap v m ->
bstep f E2 Gamma DeltaMap v m.
Proof.
induction f; intros * eq_envs bstep_E1;
inversion bstep_E1; subst; simpl in *.
- eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
- eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
eapply IHf. instantiate (1:=(updEnv n v0 E1)).
+ intros; unfold updEnv.
destruct (x=? n); auto.
......@@ -102,12 +103,12 @@ Proof.
- apply ret_b. eapply eval_eq_env; eauto.
Qed.
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 DeltaMap:
(forall n, Gamma1 n = Gamma2 n) ->
bstep f E Gamma1 vR m ->
bstep f E Gamma2 vR m.
bstep f E Gamma1 DeltaMap vR m ->
bstep f E Gamma2 DeltaMap vR m.
Proof.
revert E Gamma1 Gamma2;
revert E Gamma1 Gamma2 DeltaMap;
induction f; intros * Gamma_eq eval_f.
- inversion eval_f; subst.
econstructor; try eauto.
......@@ -118,9 +119,9 @@ Proof.
Qed.
Lemma bstep_Gamma_det f:
forall E1 E2 Gamma v1 v2 m1 m2,
bstep f E1 Gamma v1 m1 ->
bstep f E2 Gamma v2 m2 ->
forall E1 E2 Gamma DeltaMap v1 v2 m1 m2,
bstep f E1 Gamma DeltaMap v1 m1 ->
bstep f E2 Gamma DeltaMap v2 m2 ->
m1 = m2.
Proof.
induction f; intros * eval_f1 eval_f2;
......@@ -128,4 +129,18 @@ Proof.
inversion eval_f2; subst; try auto.
- eapply IHf; eauto.
- eapply Gamma_det; eauto.
Qed.
\ No newline at end of file
Qed.
Lemma bstep_det f:
forall E Gamma DeltaMap v1 v2 m,
bstep f E Gamma DeltaMap v1 m ->
bstep f E Gamma DeltaMap v2 m ->
v1 = v2.
Proof.
induction f; intros * eval_f1 eval_f2;
inversion eval_f1; subst;
inversion eval_f2; subst; try auto.
- replace v with v0 in * by eauto using eval_expr_functional.
eapply IHf; eauto.
- eapply eval_expr_functional; eauto.
Qed.
From Coq
Require Import Reals.Reals QArith.Qreals.
From Flover
Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.
Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with
| Unop u e => validErrorBounds e E1 E2 A Gamma DeltaMap
| Downcast m e => validErrorBounds e E1 E2 A Gamma DeltaMap
| Binop b e1 e2 =>
validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
validErrorBounds e2 E1 E2 A Gamma DeltaMap
| Fma e1 e2 e3 =>
validErrorBounds e1 E1 E2 A Gamma DeltaMap /\
validErrorBounds e2 E1 E2 A Gamma DeltaMap /\
validErrorBounds e3 E1 E2 A Gamma DeltaMap
| _ => True
end) /\
forall v__R (iv: intv) (err: error),
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
validErrorBounds e E1 E2 A Gamma DeltaMap ->
forall v__R iv err,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
FloverMap.find e A = Some (iv, err) ->
(exists v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
(forall v__FP m__FP,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
intros validError_e;
intros; destruct e; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto.
Qed.
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
match c with
| Let m x e k => validErrorBounds e E1 E2 A Gamma DeltaMap /\
(forall v__R v__FP,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
| Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap
end /\
forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
FloverMap.find (getRetExp c) A = Some (iv, err) ->
(exists v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
(forall v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap ->
forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
FloverMap.find (getRetExp c) A = Some (iv, err) ->
(exists v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
(forall v__FP m__FP,
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
intros validError_e;
intros; destruct c; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto.
Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
From Flover
Require Import Expressions Commands Environments ssaPrgs TypeValidator
IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
IntervalValidation RoundoffErrorValidator Infra.Ltacs Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e}
: bool :=
......@@ -70,12 +70,14 @@ Ltac prove_fprangeval m v L1 R:=
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
Theorem FPRangeValidator_sound:
forall (e:expr Q) E1 E2 Gamma v m A fVars dVars,
forall (e:expr Q) E1 E2 Gamma DeltaMap v m A fVars dVars,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
eval_expr E2 (toRExpMap Gamma) (toRExp e) v m ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
validTypes e Gamma ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound e Gamma A dVars = true ->
validErrorBounds e E1 E2 A Gamma DeltaMap ->
FPRangeValidator e A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
(forall v, NatSet.In v dVars ->
......@@ -87,16 +89,16 @@ Proof.
intros *.
unfold FPRangeValidator.
intros.
pose proof (validTypes_single _ _ H1) as validT.
pose proof (validTypes_single _ _ H2) as validT.
destruct validT as [mE [type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
pose proof (validRanges_single _ _ _ _ H2) as valid_e.
pose proof (validRanges_single _ _ _ _ H3) as valid_e.
destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
destruct iv_e as [e_lo e_hi].
assert (Rabs (vR - v) <= Q2R (err_e))%R.
{ eapply validErrorbound_sound; eauto. }
{ eapply validErrorBounds_single; eauto. }
destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
as [v_in_errIv];
try auto.
......@@ -110,27 +112,27 @@ Proof.
rewrite type_e in *; cbn in *.
- Flover_compute.
destruct (n mem dVars) eqn:?.
+ set_tac. edestruct H6 as [? [? [? [? ?]]]]; eauto.
rewrite H9 in type_e; inversion type_e; subst.
inversion H0; subst.
rewrite H13 in H3; inversion H3; subst.
+ set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
rewrite H11 in type_e; inversion type_e; subst.
inversion H1; subst.
rewrite H15 in H10; inversion H10; subst.
auto.
+ Flover_compute. prove_fprangeval m v L2 R.
+ Flover_compute. prove_fprangeval m v L1 R.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- Flover_compute; destruct u; Flover_compute; try congruence.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- inversion H0; subst.
destruct H1 as [mE [find_mE [[validt_e1 [validt_e2 [m_e1 [m_e2 [find_m1 [find_m2 join_valid]]]]]] _ ]]].
- inversion H1; subst.
destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [m_e1 [m_e2 [find_m1 [find_m2 join_valid]]]]]] _ ]]].
assert (m_e1 = m1) by (eapply validTypes_exec in find_m1; eauto).
assert (m_e2 = m2) by (eapply validTypes_exec in find_m2; eauto).
subst.
Flover_compute; try congruence.
prove_fprangeval m (perturb (evalBinop b v1 v2) m delta) L1 R.
- inversion H0; subst.
destruct H1 as [mE [find_mE [[validt_e1 [validt_e2 [validt_e3 [m_e1 [m_e2 [m_e3 [find_m1 [find_m2 [find_m3 join_valid]]]]]]]]] _ ]]].
- inversion H1; subst.
destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [validt_e3 [m_e1 [m_e2 [m_e3 [find_m1 [find_m2 [find_m3 join_valid]]]]]]]]] _ ]]].
assert (m_e1 = m1) by (eapply validTypes_exec in find_m1; eauto).
assert (m_e2 = m2) by (eapply validTypes_exec in find_m2; eauto).
assert (m_e3 = m3) by (eapply validTypes_exec in find_m3; eauto).
......@@ -143,40 +145,46 @@ Proof.
Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
forall E1 E2 Gamma v vR m A fVars dVars outVars,
forall E1 E2 Gamma DeltaMap v vR m A fVars dVars outVars,
(forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) v m ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap v m ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundCmd f Gamma A dVars = true ->
validErrorBoundsCmd f E1 E2 A Gamma DeltaMap ->
FPRangeValidatorCmd f A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\
FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m) ->
(forall v, NatSet.In v dVars ->
exists vF m, E2 v = Some vF /\
FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m) ->
validFloatValue v m.
Proof.
induction f; intros;
simpl in *;
(match_pat (bstep _ _ (toRTMap _) _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ (toRExpMap Gamma) _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ (toRTMap _) _ _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ (toRExpMap Gamma) _ _ _) (fun H => inversion H; subst; simpl in * ));
repeat match goal with
| H : _ = true |- _ => andb_to_prop H
end.
- destruct H3
- destruct H4
as [[me [find_me [find_var [? [validt_e validt_f]]]]] valid_exec].
assert (m = me) by (eapply validTypes_exec in find_me; eauto); subst.
rename me into m.
match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in * ).
Flover_compute.
destruct H4 as [[valid_e valid_rec] valid_single].
destruct H5 as [[valid_e valid_rec] valid_single].
pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
destruct valid_e_single
as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
destr_factorize.
destruct H6 as ((validerr_e & validerr_rec) & validerr_single).
pose proof (validErrorBounds_single _ _ _ _ validerr_e) as validerr_e_single.
specialize (validerr_e_single v0 iv_e err_e H19 map_e) as
((vF_e & m_e & eval_float_e) & err_bounded_e).
(* destr_factorize.
edestruct (validErrorbound_sound (e:=e) (E1:=E1) (E2:=E2) (fVars:=fVars)
(dVars := dVars) (A:=A)
(nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
......@@ -185,19 +193,14 @@ Proof.
split; try auto.
hnf; intros; subst; set_tac.
+ destruct iv_e; auto.
+ rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H17) in *; try auto.
+ *)
rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H19) in *; try auto.
apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
Gamma v vR m0 A fVars
Gamma DeltaMap v vR m0 A fVars
(NatSet.add n dVars) (outVars)); eauto.
* eapply approxUpdBound; eauto; simpl in *.
{ eapply toRExpMap_some; eauto. simpl; auto. }
{ apply Rle_trans with (r2:= Q2R err_e); try lra.
eapply err_bounded_e. eauto.
apply Qle_Rle.
rewrite Qeq_bool_iff in *.
destruct i0; inversion Heqo0; subst.
rewrite R1.
lra. }
{ admit. }
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
......@@ -216,9 +219,9 @@ Proof.
* set_tac; split.
{ split; try auto.
hnf; intros; subst.
apply H5; rewrite NatSet.add_spec; auto. }
apply H6; rewrite NatSet.add_spec; auto. }
{ hnf; intros.
apply H5; rewrite NatSet.add_spec; auto. }
apply H6; rewrite NatSet.add_spec; auto. }
(*
* unfold vars_typed. intros.
unfold updDefVars.
......@@ -237,8 +240,8 @@ Proof.
set_tac. split; try auto.
split; try auto.
hnf; intros; subst; set_tac. }
{ apply H8.
rewrite NatSet.add_spec in H4; destruct H4;
{ apply H9.
rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. }
- destruct H4. destruct H3. eapply FPRangeValidator_sound; eauto.
Qed.
\ No newline at end of file
- destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
Admitted.
This diff is collapsed.
......@@ -164,6 +164,14 @@ Proof.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Lemma usedVars_toRExp_compat e:
usedVars (toRExp e) = usedVars e.
Proof.
induction e; simpl; set_tac.
- now rewrite IHe1, IHe2.
- now rewrite IHe1, IHe2, IHe3.
Qed.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
......@@ -486,7 +494,7 @@ Proof.
*)
(**
We treat a function mapping an exprression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
**)
(* Definition analysisResult :Type := expr Q -> intv * error. *)
This diff is collapsed.
This diff is collapsed.