Commit 39a53d43 authored by Heiko Becker's avatar Heiko Becker
Browse files

Implement and prove a correctness predicate for FPRangeValidator

parent be020b3f
......@@ -53,24 +53,54 @@ Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
| Ret e => FPRangeValidator e A typeMap dVars
end.
Ltac prove_fprangeval m v L1 R:=
Ltac prove_fprangeval m v :=
destruct m eqn:?; try auto;
unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
try rewrite orb_true_iff in *;
destruct L1; destruct R; canonize_hyps;
repeat (match goal with
|H: _ && _ = true |- _ => andb_to_prop H
|H: _ || _ = true |- _ => rewrite orb_true_iff in H; destruct H
end);
canonize_hyps;
try rewrite <- Rabs_eq_Qabs in *;
Q2R_to_head;
rewrite <- Q2R_minus, <- Q2R_plus in *;
repeat (match goal with
|H: _ = true |- _ => andb_to_prop H
end);
destruct (Req_dec v 0); try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (minValue_pos m)))%R (* denormal case *);
try auto;
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
destruct (Req_dec v 0); try auto ; (* v = 0 by auto *)
destruct (Rlt_le_dec (Rabs v) (Q2R (minValue_pos m)))%R (* denormal case *);
try (subst; auto; fail);
destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R;
try (subst; auto; fail);
lra.
(**
Global correctness predicate for FPRangeValidator.
Given expression e and its evaluation, the result is a valid value for
its assigned type
**)
Fixpoint validFPRanges (e:expr Q) (E2:env) Gamma A :Prop :=
(match e with
| Var _ x => True
| Const m v => True
| Unop uop e1 => validFPRanges e1 E2 Gamma A
| Binop bop e1 e2 => validFPRanges e1 E2 Gamma A /\
validFPRanges e2 E2 Gamma A
| Fma e1 e2 e3 => validFPRanges e1 E2 Gamma A /\
validFPRanges e2 E2 Gamma A /\
validFPRanges e3 E2 Gamma A
| Downcast m e => validFPRanges e E2 Gamma A
end) /\
forall E1 DeltaMap v m fVars dVars,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
validTypes e Gamma ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
validFloatValue v m.
Theorem FPRangeValidator_sound:
forall (e:expr Q) E1 E2 Gamma DeltaMap v m A fVars dVars,
Lemma validFPRanges_single e E2 Gamma A:
validFPRanges e E2 Gamma A ->
forall E1 DeltaMap v m fVars dVars,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
......@@ -78,70 +108,186 @@ Theorem FPRangeValidator_sound:
validTypes e Gamma ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
validFloatValue v m.
Proof.
intros * valid_fp; destruct e; simpl in *; apply valid_fp.
Qed.
Theorem FPRangeValidator_sound e:
forall E2 A Gamma dVars fVars,
FPRangeValidator e A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) 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) ->
validFloatValue v m.
validFPRanges e E2 Gamma A.
Proof.
intros *.
unfold FPRangeValidator.
intros.
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 _ _ _ _ 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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
destruct e;
unfold validFloatValue in *; cbn in *;
rewrite type_e in *; cbn in *.
- Flover_compute.
induction e;
intros * FPRanges_checked usedVars_in_fVars dVars_valid;
try (split; [ cbn; auto | ]).
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
destruct (n mem dVars) eqn:?.
+ 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 L1 R.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
- 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 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).
subst.
Flover_compute; try congruence.
prove_fprangeval m (perturb (evalFma v1 v2 v3) m delta) L1 R.
- Flover_compute; try congruence.
type_conv; subst.
prove_fprangeval m v L1 R.
+ set_tac. edestruct dVars_valid as [? [? [? [? ?]]]]; eauto.
rewrite type_e in *. inversion H2; subst.
inversion eval_float; subst.
rewrite H6 in H1; inversion H1; subst.
destruct x0; auto.
+ prove_fprangeval m v.
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m0 = mE) by (eapply valid_exec; eauto); subst.
rename mE into m0.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_e as [iv_e [err_e [vR [map_e [eval_real vR_bounded]]]]].
destruct iv_e as [e_lo e_hi].
assert (Rabs (vR - v0) <= Q2R (err_e))%R.
{ eapply validErrorBoundsRec_single; eauto. }
destruct (distance_gives_iv (a:=vR) v0 (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
as [v_in_errIv];
try auto.
simpl in *.
assert (Rabs v0 <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v0 <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
prove_fprangeval m0 v0.
- eapply IHe; try eauto.
unfold FPRangeValidator in *; Flover_compute; auto.
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
prove_fprangeval m v.
- unfold FPRangeValidator in *; Flover_compute.
assert (NatSet.Subset ((usedVars e1) -- dVars) fVars).
{ set_tac. split; set_tac. }
assert (NatSet.Subset ((usedVars e2) -- dVars) fVars).
{ intros * ? in_set. apply usedVars_in_fVars. set_tac. split; set_tac. }
split; [ eapply IHe1; eauto | eapply IHe2; eauto ].
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
prove_fprangeval m v.
- unfold FPRangeValidator in *; Flover_compute.
assert (NatSet.Subset ((usedVars e1) -- dVars) fVars).
{ set_tac. split; set_tac. }
assert (NatSet.Subset ((usedVars e2) -- dVars) fVars).
{ intros * ? in_set. apply usedVars_in_fVars. set_tac. split; set_tac. }
assert (NatSet.Subset ((usedVars e3) -- dVars) fVars).
{ intros * ? in_set. apply usedVars_in_fVars. set_tac. split; set_tac. }
repeat split;
[ eapply IHe1; eauto | eapply IHe2; eauto | eapply IHe3; eauto].
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m = mE) by (eapply valid_exec; eauto); subst.
rename mE into m.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
prove_fprangeval m v.
- eapply IHe; eauto. unfold FPRangeValidator in *. Flover_compute; auto.
- intros E1 * DeltaMap_valid approx_E1_E2 eval_float validTypes_e
validRanges_e validErrors_e.
apply validTypes_single in validTypes_e.
destruct validTypes_e as [ mE [ type_e valid_exec]].
assert (m0 = mE) by (eapply valid_exec; eauto); subst.
rename mE into m0.
unfold validFloatValue.
apply validRanges_single in validRanges_e.
destruct validRanges_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 validErrorBoundsRec_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.
simpl in *.
assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
as abs_bounded
by (apply bounded_inAbs; auto).
unfold FPRangeValidator in *.
Flover_compute.
prove_fprangeval m0 v.
Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
......@@ -212,29 +358,26 @@ Proof.
apply H6; rewrite NatSet.add_spec; auto. }
{ hnf; intros.
apply H6; rewrite NatSet.add_spec; auto. }
(*
* unfold vars_typed. intros.
unfold updDefVars.
destruct (v2 =? n) eqn:?; eauto.
apply H8. rewrite NatSet.union_spec in *.
destruct H4; try auto.
rewrite NatSet.add_spec in H4.
rewrite Nat.eqb_neq in *.
destruct H4; subst; try congruence; auto. *)
* intros. unfold updEnv.
type_conv; subst.
destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
try rewrite Nat.eqb_neq in *.
{ exists v1; subst. exists m; repeat split; try auto.
eapply FPRangeValidator_sound; eauto.
set_tac. split; try auto.
split; try auto.
hnf; intros; subst; set_tac. }
pose proof (FPRangeValidator_sound e E2 A Gamma (dVars:=dVars) (fVars:=fVars)).
assert (validFPRanges e E2 Gamma A).
{ eapply H6; try eauto.
set_tac. split; set_tac. split; set_tac.
hnf; intros. subst.
apply H17. set_tac. }
eapply validFPRanges_single in H7; eauto. }
{ apply H9.
rewrite NatSet.add_spec in H5; destruct H5;
auto; subst; congruence. }
- destruct H5.
destruct H4.
destruct H6; auto.
eapply FPRangeValidator_sound; eauto.
pose proof (FPRangeValidator_sound e E2 A Gamma (dVars:=dVars) (fVars:=fVars)).
assert (validFPRanges e E2 Gamma A).
{ eapply H15; try eauto. }
eapply validFPRanges_single in H16; eauto.
Qed.
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