Commit ab3e452e authored by Heiko Becker's avatar Heiko Becker

Extend conclusion of ResultChecker to get rid of some admitted goals

parent 7f62e7d7
......@@ -64,12 +64,11 @@ Proof.
exists Gamma; intros approxEnv_E1E2.
destruct subdivs.
- edestruct result_checking_sound; eauto.
intuition.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single; eauto.
destruct H5 as (? & ? & ?).
repeat eexists; eauto.
+ (* destruct H3 earlier *) admit.
+ (* add ssa to resultchecker soundness *) admit.
+ (* add validFPRagnes to ResultChecker soundness *) admit.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
......@@ -83,7 +82,6 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult)
forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
unsat_queries Qmap ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
......
......@@ -18,19 +18,25 @@ Definition ResultChecker (e: expr Q) (absenv: analysisResult)
Soundness proof for the result checker.
**)
Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma:
forall (E1 E2: env),
forall (E1 E2: env) DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
eval_precond E1 P ->
unsat_queries Qmap ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
ResultChecker e absenv P Qmap defVars Gamma = true ->
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\ validErrorBounds e E1 E2 absenv Gamma.
exists outVars,
ssa e (freeVars e) outVars /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros * approxE1E2 P_valid unsat_qs valid_typeMap results_valid.
intros * deltaMap_valid approxE1E2 P_valid unsat_qs valid_typeMap results_valid.
unfold ResultChecker in results_valid.
assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
......@@ -72,8 +78,11 @@ Proof.
*)
assert (ssa e (NatSet.union (freeVars e) (NatSet.empty)) outVars2).
{ eapply ssa_equal_set; eauto. }
split; auto.
eapply RoundoffErrorValidator_sound; eauto.
eexists; repeat split; try eauto.
- eapply RoundoffErrorValidator_sound; eauto.
- eapply FPRangeValidator_sound; eauto.
+ eapply RoundoffErrorValidator_sound; eauto.
+ intros; set_tac.
Qed.
(**
......@@ -99,96 +108,10 @@ Corollary result_checking_sound_single (e: expr Q) (absenv: analysisResult) P Qm
Proof.
intros * deltas_matched P_valid unsat_qs valid_typeMap results_valid.
exists Gamma; intros approxE1E2.
assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as validRange
by (eapply result_checking_sound; eauto).
assert (validErrorBounds e E1 E2 absenv Gamma) as Hsound
by (eapply result_checking_sound; eauto).
edestruct result_checking_sound as (? & _ & validRange & Hsound & _); try eauto.
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists iv, err, vR, vF, mF; repeat split; auto.
Qed.
(*
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
(Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
match getValidMapCmd defVars f (FloverMap.empty mType) with
| Succes Gamma =>
if (validSSA f (preVars P))
then
if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
FPRangeValidatorCmd f absenv Gamma NatSet.empty
then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
else false
else false
| _ => false
end.
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
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) ->
eval_precond E1 P ->
unsat_queries Qmap ->
CertificateCheckerCmd f absenv P Qmap 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)) DeltaMapR vR REAL /\
bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
(forall 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 * deltas_matched P_valid unsat_qs 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.
pose proof (validSSA_checks_freeVars _ _ L) as sub.
assert (validSSA f (freeVars f) = true) as ssa_valid
by (eapply validSSA_downward_closed; eauto; set_tac).
apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small].
apply validSSA_sound in L.
destruct L as [outVars ssa_f].
assert (ssa f (preVars P NatSet.empty) outVars) as ssa_valid.
{ eapply ssa_equal_set; eauto.
apply NatSetProps.empty_union_2.
apply NatSet.empty_spec. }
rename R into validFPRanges.
assert (dVars_range_valid NatSet.empty E1 absenv).
{ unfold dVars_range_valid.
intros; set_tac. }
assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
as freeVars_contained by set_tac.
assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
{ eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition.
unfold affine_dVars_range_valid; intros.
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].
pose proof RoundoffErrorValidatorCmd_sound as Hsound.
eapply validErrorBoundsCmd_single in Hsound; eauto.
- specialize Hsound as ((vF & mF & eval_float) & ?).
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
- eapply ssa_equal_set. 2: exact ssa_f_small.
apply NatSetProps.empty_union_2.
apply NatSet.empty_spec.
- unfold dVars_contained; intros; set_tac.
Qed.
*)
......@@ -173,6 +173,63 @@ Proof.
split; set_tac; intros[?|Ha]; auto; apply set_eq in Ha; auto.
Qed.
Lemma ssa_subset_ext V (f:expr V):
forall inVars1 inVars2 outVars,
NatSet.Subset inVars1 inVars2 ->
NatSet.Subset (freeVars f) inVars1 ->
ssa f inVars2 outVars ->
ssa f inVars1 outVars.
Proof.
induction f; intros * invars_sub fVars_sub ssa_invars;
inversion ssa_invars; subst; simpl in *.
- constructor. set_tac.
hnf; intros; apply H1. now apply invars_sub.
- constructor.
hnf; intros; apply H3. now apply invars_sub.
- specialize (IHf _ _ _ invars_sub fVars_sub H3).
constructor; auto.
- assert (NatSet.Subset (freeVars f1) inVars1 /\
NatSet.Subset (freeVars f2) inVars1)
as (f1_subset & f2_subset)
by (split; set_tac).
eapply ssaBinop;
[ eapply IHf1; eauto | eapply IHf2; eauto | auto ].
- assert (NatSet.Subset (freeVars f1) inVars1 /\
NatSet.Subset (freeVars f2) inVars1 /\
NatSet.Subset (freeVars f3) inVars1)
as (f1_subset & f2_subset & f3_subset)
by (repeat split; set_tac).
eapply ssaFma;
[ eapply IHf1; eauto | eapply IHf2; eauto | eapply IHf3; eauto | auto ].
- specialize (IHf _ _ _ invars_sub fVars_sub H3).
constructor; auto.
- eapply ssaLet.
+ destruct ((n) mem (inVars1)) eqn:in_case; try auto.
set_tac.
exfalso; apply H3.
apply invars_sub; auto.
+ eapply IHf1; eauto.
set_tac.
+ eapply IHf2; try eauto.
* set_tac; intuition.
* set_tac. destruct (a =? n) eqn:case_mem.
{ rewrite Nat.eqb_eq in case_mem; auto. }
{ rewrite Nat.eqb_neq in case_mem.
right; apply fVars_sub.
set_tac. }
+ auto.
Qed.
Corollary ssa_is_fVars V (f:expr V) inVars outVars:
NatSet.Subset (freeVars f) inVars ->
ssa f inVars outVars ->
ssa f (freeVars f) outVars.
Proof.
intros.
eapply ssa_subset_ext; eauto.
set_tac.
Qed.
Lemma ssa_outVars_extensible V (e:expr V):
forall inVars outVars1 outVars2,
ssa e inVars outVars1 ->
......
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