Commit 7e8898d7 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix overall soundness theorem and FPRangevalidator soundness

parent e320513e
......@@ -28,32 +28,33 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
Apart from assuming two executions, one in R and one on floats, we assume that
the real valued execution respects the precondition.
**)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
defVars:
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
forall (E1 E2:env),
approxEnv E1 (toRExpMap defVars) absenv (usedVars e) NatSet.empty E2 ->
(forall v, NatSet.In v (Expressions.usedVars e) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.In v (usedVars e) ->
exists m : mType,
FloverMap.find (Var Q v) defVars = Some m) ->
CertificateChecker e absenv P defVars = true ->
exists Gamma iv err vR vF m,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRMap Gamma) (toRExp e) vR REAL /\
eval_expr E2 Gamma (toRExp e) vF m /\
(forall vF m,
eval_expr E2 Gamma (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
exists Gamma,
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 /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) (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 * approxE1E2 P_valid types_defined certificate_valid.
intros * P_valid certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)); try congruence.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
rename t into Gamma.
assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. }
rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
clear R1.
......@@ -69,57 +70,69 @@ Proof.
assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
{ hnf; intros a in_empty.
set_tac. }
rename R into validFPRanges.
assert (validRanges e absenv E1 (toRExpMap defVars)) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=toRExpMap defVars) (E:=E1));
auto. }
pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
rename R0 into validFPRanges.
assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
{ eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1));
auto.
unfold RangeValidator. rewrite L; auto. }
pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
destruct iv_e as [elo ehi].
edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; split; auto.
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.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed.
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
defVars fBits:=
let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv tMap NatSet.empty
then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
if (validSSA f (freeVars f))
then
if (RangeValidatorCmd f absenv P NatSet.empty) &&
FPRangeValidatorCmd f absenv Gamma NatSet.empty
then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
else false
else false
else false.
| _ => false
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
defVars fBits:
defVars:
forall (E1 E2:env),
approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
(forall v, NatSet.In v (freeVars f) ->
exists vR, E1 v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
(forall v, NatSet.In v (freeVars f) ->
exists m : mType,
defVars v = Some m) ->
CertificateCheckerCmd f absenv P defVars fBits = true ->
exists iv err vR vF m,
FloverMap.find (getRetExp f) absenv = Some (iv,err) /\
bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
CertificateCheckerCmd f absenv P defVars = true ->
exists Gamma,
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 /\
(forall vF m,
bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) 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 * approxE1E2 P_valid types_defined certificate_valid.
intros * P_valid certificate_valid.
unfold CertificateCheckerCmd in certificate_valid.
destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
try congruence.
rename t into Gamma.
assert (validTypesCmd f Gamma).
{ eapply getValidMapCmd_correct; try eauto.
intros; cbn in *; congruence. }
exists Gamma; intros approxE1E2.
repeat rewrite <- andb_lazy_alt in certificate_valid.
andb_to_prop certificate_valid.
apply validSSA_sound in R0.
destruct R0 as [outVars ssa_f].
apply validSSA_sound in L.
destruct L as [outVars ssa_f].
assert (ssa f (freeVars f NatSet.empty) outVars) as ssa_valid.
{ eapply ssa_equal_set; try eauto.
apply NatSetProps.empty_union_2.
......@@ -128,18 +141,17 @@ Proof.
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (vars_typed (freeVars f NatSet.empty) defVars).
{ unfold vars_typed. intros; apply types_defined. set_tac.
destruct H0; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply RangeValidatorCmd_sound; eauto.
unfold RangeValidatorCmd. rewrite L0. auto. }
(*
unfold affine_dVars_range_valid; intros.
set_tac. }
pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
set_tac. } *)
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.
exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
Qed.
......@@ -2,7 +2,8 @@ From Flover
Require Import Expressions Commands Environments ssaPrgs TypeValidator
IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e}
: bool :=
match FloverMap.find e typeMap, FloverMap.find e A with
|Some m, Some (iv_e, err_e) =>
let iv_e_float := widenIntv iv_e err_e in
......@@ -73,7 +74,7 @@ Theorem FPRangeValidator_sound:
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
eval_expr E2 (toRExpMap Gamma) (toRExp e) v m ->
validTypes e Gamma ->
validRanges e A E1 (toRExpMap Gamma) ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorbound e Gamma A dVars = true ->
FPRangeValidator e A Gamma dVars = true ->
NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
......@@ -87,8 +88,9 @@ Proof.
unfold FPRangeValidator.
intros.
pose proof (validTypes_single _ _ H1) as validT.
destruct validT as [mE [type_e ?]].
assert (mE = m) by admit; subst.
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.
destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
......@@ -109,9 +111,9 @@ Proof.
- Flover_compute.
destruct (n mem dVars) eqn:?.
+ set_tac. edestruct H6 as [? [? [? [? ?]]]]; eauto.
rewrite H10 in type_e; inversion type_e; subst.
rewrite H9 in type_e; inversion type_e; subst.
inversion H0; subst.
rewrite H14 in H3; inversion H3; subst.
rewrite H13 in H3; inversion H3; subst.
auto.
+ Flover_compute. prove_fprangeval m v L2 R.
- Flover_compute; try congruence.
......@@ -121,119 +123,122 @@ Proof.
type_conv; subst.
prove_fprangeval m v L1 R.
- inversion H0; subst.
assert (FloverMap.find e1 Gamma = Some m1) as type_m1 by admit.
assert (FloverMap.find e2 Gamma = Some m2) as type_m2 by admit.
rewrite type_m1, type_m2 in *.
destruct H1 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.
assert (FloverMap.find e1 Gamma = Some m1) as type_m1 by admit.
assert (FloverMap.find e2 Gamma = Some m2) as type_m2 by admit.
assert (FloverMap.find e3 Gamma = Some m3) as type_m3 by admit.
rewrite type_m1, type_m2, type_m3 in *.
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]]]]]]]]] _ ]]].
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.
Admitted.
Qed.
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
forall E1 E2 Gamma v vR m A tMap fVars dVars outVars,
approxEnv E1 Gamma A fVars dVars E2 ->
forall E1 E2 Gamma v vR m A fVars dVars outVars,
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
ssa f (NatSet.union fVars dVars) outVars ->
bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
bstep (toRCmd f) E2 Gamma v m ->
validRangesCmd f A E1 Gamma ->
validErrorboundCmd f tMap A dVars = true ->
FPRangeValidatorCmd f A tMap dVars = true ->
bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR m ->
bstep (toRCmd f) E2 (toRExpMap Gamma) v m ->
validTypesCmd f Gamma ->
validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundCmd f Gamma A dVars = true ->
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) tMap = Some m /\
FloverMap.find (Var Q v) Gamma = Some m /\
validFloatValue vF m) ->
validFloatValue v m.
Proof.
admit.
(*
induction f; intros;
simpl in *;
(match_pat (bstep _ _ (toRMap _) _ _) (fun H => inversion H; subst; simpl in * ));
(match_pat (bstep _ _ 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.
- assert (FloverMap.find e tMap = Some m) by admit.
match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in * ).
Flover_compute.
destruct H3 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.
edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
(dVars := dVars) (A:=A)
(nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+ admit.
+ admit.
+ set_tac. split; try auto.
split; try auto.
hnf; intros; subst; set_tac.
+ admit.
+ destruct iv_e; 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)
(updDefVars n m Gamma) v vR m0 A tMap fVars
(NatSet.add n dVars) (outVars) fBits); eauto.
* eapply approxUpdBound; eauto.
simpl in *.
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 R2.
lra.
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
* eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm.
- destruct H3
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].
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.
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))
as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+ set_tac. split; try auto.
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.
apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
Gamma 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. }
* eapply ssa_equal_set; eauto.
hnf. intros a; split; intros in_set.
{ rewrite NatSet.add_spec, NatSet.union_spec;
rewrite NatSet.union_spec, NatSet.add_spec in in_set.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
{ rewrite NatSet.add_spec, NatSet.union_spec in in_set;
rewrite NatSet.union_spec, NatSet.add_spec.
destruct in_set as [P1 | [ P2 | P3]]; auto. }
(*
* eapply (swap_Gamma_bstep (Gamma1 := updDefVars n REAL (toRMap Gamma))); eauto.
eauto using Rmap_updVars_comm.
* apply validRangesCmd_swap with (Gamma1:=updDefVars n REAL Gamma).
{ intros x; unfold toRMap, updDefVars.
destruct (x =? n) eqn:?; auto. }
{ eapply valid_rec. auto. }
* set_tac; split.
{ split; try auto.
hnf; intros; subst.
apply H5; rewrite NatSet.add_spec; auto. }
{ hnf; intros.
apply H5; 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 m1; repeat split; try auto.
eapply FPRangeValidator_sound; eauto.
set_tac. split; try auto.
split; try auto.
hnf; intros; subst; set_tac. }
{ apply H9.
rewrite NatSet.add_spec in H4; destruct H4;
auto; subst; congruence. }
- destruct H4. eapply FPRangeValidator_sound; eauto. *)
Admitted.
\ No newline at end of file
{ eapply valid_rec. auto. } *)
* set_tac; split.
{ split; try auto.
hnf; intros; subst.
apply H5; rewrite NatSet.add_spec; auto. }
{ hnf; intros.
apply H5; 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. }
{ apply H8.
rewrite NatSet.add_spec in H4; destruct H4;
auto; subst; congruence. }
- destruct H4. destruct H3. eapply FPRangeValidator_sound; eauto.
Qed.
\ No newline at end of file
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