Commit 565e31c3 authored by Joachim Bard's avatar Joachim Bard

adding support for queries in subdivs

parent 7fefc298
......@@ -36,6 +36,7 @@ Theorem Certificate_checking_is_sound (e: expr Q) (absenv: analysisResult) P Qma
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
unsat_queries Qmap ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
CertificateChecker e absenv P Qmap subdivs defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
......@@ -47,7 +48,7 @@ Theorem Certificate_checking_is_sound (e: expr Q) (absenv: analysisResult) P Qma
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
Proof.
intros * deltas_matched P_valid unsat_qs certificate_valid.
intros * deltas_matched P_valid unsat_qs unsat_qs_subdivs certificate_valid.
unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
destruct subdivs.
......
......@@ -54,17 +54,20 @@ Proof.
- exfalso. eapply He. set_tac.
Qed.
Definition checkSubdivsStep e absenv defVars Gamma (PA: precond * analysisResult) :=
let (P, A) := PA in
(RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) && resultLeq e A absenv.
Definition checkSubdivsStep e absenv defVars Gamma (PAQ: precond * analysisResult * usedQueries) :=
match PAQ with
| (P, A, Q) =>
RangeErrorChecker e A P Q defVars Gamma
&& resultLeq e A absenv
end.
Definition checkSubdivs e absenv subdivs defVars Gamma :=
forallb (checkSubdivsStep e absenv defVars Gamma) subdivs.
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A Q :
checkSubdivs e absenv subdivs defVars Gamma = true ->
In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
In (P, A, Q) subdivs ->
RangeErrorChecker e A P Q defVars Gamma = true /\
resultLeq e A absenv = true.
Proof.
intros H Hin.
......@@ -381,9 +384,12 @@ Qed.
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) subdivs (defVars: FloverMap.t mType) Gamma :=
validSSA e (preVars P) &&
checkPreconds (map fst subdivs) P &&
checkPreconds (map (fun S => match S with (P, _, _) => P end) subdivs) P &&
checkSubdivs e absenv subdivs defVars Gamma.
Definition queriesInSubdivs (subdivs: list (precond * analysisResult * usedQueries)) :=
map (fun S => match S with (_, _, Q) => Q end) subdivs.
(**
Soundness proof for the interval subdivs checker.
**)
......@@ -392,6 +398,7 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
(forall (e': expr R) (m': mType),
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
SubdivsChecker e absenv P subdivs defVars Gamma = true ->
exists Gamma,
......@@ -404,26 +411,26 @@ Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P subdivs de
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
Proof.
intros * deltas_matched P_valid valid_typeMap chk.
intros * deltas_matched P_valid unsat_qs valid_typeMap chk.
apply andb_prop in chk as [chk valid_subdivs].
apply andb_prop in chk as [valid_ssa valid_cover].
eapply (checkPreconds_sound) in P_valid as [P1 [in_subdivs P_valid]]; eauto.
assert (validSSA e (preVars P1) = true) as valid_ssa'.
{ eapply validSSA_eq_set; eauto. eapply checkPreconds_preVars; eauto. }
apply in_map_iff in in_subdivs as [[P2 A] [Heq in_subdivs]].
apply in_map_iff in in_subdivs as [[[P2 A] Qmap] [Heq in_subdivs]].
cbn in Heq; subst.
pose proof (checkSubdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P1 (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true) as res_check
pose proof (checkSubdivs_sound e _ _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P1 Qmap defVars Gamma = true) as res_check
by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
exists Gamma; intros approxE1E2.
assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
by (eapply approxEnv_empty_dVars; eauto).
assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
{ eapply result_checking_sound; eauto.
admit. (* unsat_queries of empty map *) }
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
{ eapply result_checking_sound; eauto.
admit. (* unsat_queries of empty map *) }
apply unsat_qs. apply in_map_iff. now exists (P1, A, Qmap). }
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBounds_single in Hsound; eauto.
......@@ -436,4 +443,4 @@ Proof.
intros vF0 m Heval.
specialize (err_bounded vF0 m Heval).
lra.
Admitted.
\ No newline at end of file
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