Commit ae671726 authored by Joachim Bard's avatar Joachim Bard

check that endresult follows from subresults

forall A in subdivs: A <<= absenv
parent 9b7c42d3
......@@ -11,33 +11,85 @@ From Flover
Require Import List.
Definition check_subdivs_step e defVars Gamma (b: bool) (PA: precond * analysisResult) :=
Fixpoint result_leq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => result_leq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => result_leq e1 A1 A2 && result_leq e2 A1 A2
| Fma e1 e2 e3 => result_leq e1 A1 A2 && result_leq e2 A1 A2 && result_leq e3 A1 A2
| _ => true
end &&
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end.
Lemma result_leq_sound e A1 A2 :
result_leq e A1 A2 = true ->
exists iv1 err1 iv2 err2,
FloverMap.find e A1 = Some (iv1, err1) /\
FloverMap.find e A2 = Some (iv2, err2) /\
isSupersetIntv iv1 iv2 = true /\
err1 <= err2.
Proof.
intros H.
assert (
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end = true).
{ unfold result_leq in H. destruct e;
apply andb_prop in H as [_ H]; auto. }
Flover_compute.
repeat eexists; auto.
- unfold isSupersetIntv. now rewrite L0.
- apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.
(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
NatSet.Empty dVars ->
approxEnv E1 Gamma A1 fVars dVars E2 ->
approxEnv E1 Gamma A2 fVars dVars E2.
Proof.
intros He H.
induction H.
- constructor.
- econstructor; eauto.
- exfalso. eapply He. set_tac.
Qed.
Definition check_subdivs_step e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
result_leq e A absenv.
Definition check_subdivs e subdivs defVars Gamma :=
fold_left (check_subdivs_step e defVars Gamma) subdivs true.
Definition check_subdivs e absenv subdivs defVars Gamma :=
fold_left (check_subdivs_step e absenv defVars Gamma) subdivs true.
Lemma check_subdivs_false_fp e subdivs defVars Gamma :
fold_left (check_subdivs_step e defVars Gamma) subdivs false = false.
Lemma check_subdivs_false_fp e absenv subdivs defVars Gamma :
fold_left (check_subdivs_step e absenv defVars Gamma) subdivs false = false.
Proof.
induction subdivs as [|[P A] subdivs]; auto.
Qed.
Lemma check_subdivs_sound e subdivs defVars Gamma P A :
check_subdivs e subdivs defVars Gamma = true ->
Lemma check_subdivs_sound e absenv subdivs defVars Gamma P A :
check_subdivs e absenv subdivs defVars Gamma = true ->
In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true.
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
result_leq e A absenv = true.
Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?; auto.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
try (rewrite check_subdivs_false_fp in H; discriminate H).
split; auto.
destruct (result_leq e A absenv) eqn: ?; auto.
rewrite check_subdivs_false_fp in H; auto.
- apply IHsubdivs; auto. cbn in H.
unfold check_subdivs.
destruct (check_subdivs_step e defVars Gamma true a) eqn:?; auto.
destruct (check_subdivs_step e absenv defVars Gamma true a) eqn:?; auto.
rewrite check_subdivs_false_fp in H. discriminate H.
Qed.
......@@ -62,33 +114,20 @@ Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
Definition merge_subdivs e hd tl : analysisResult :=
fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
Fixpoint result_leq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => result_leq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => result_leq e1 A1 A2 && result_leq e2 A1 A2
| Fma e1 e2 e3 => result_leq e1 A1 A2 && result_leq e2 A1 A2 && result_leq e3 A1 A2
| _ => true
end &&
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
| _, _ => false
end.
(* TODO: needs more assumptions, i.e. checker for precond *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
eval_precond E P ->
exists P' A, In (P', A) subdivs /\ eval_precond E P'.
Admitted.
(* TODO: check precond sound wrt. subdivs *)
(* TODO: don't merge, just check that forall (P', A) subdivs P' <<= P *)
(* TODO: merge hd and tl again *)
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
(* let M := merge_subdivs e (snd hd) (map snd tl) in *)
validSSA e (preVars P) &&
check_subdivs e (hd :: tl) defVars Gamma (* &&
check_merge_subdivs e M absenv *) .
check_subdivs e absenv (hd :: tl) defVars Gamma.
(* TODO: needs more assumptions *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
eval_precond E P ->
exists P' A, In (P', A) subdivs /\ eval_precond E P'.
Admitted.
(**
Soundness proof for the interval subdivs checker.
**)
......@@ -114,21 +153,30 @@ Proof.
rename L into valid_ssa.
rename R into valid_subdivs.
apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
(* preVars P == preVars P' should hold *)
assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
pose proof (check_subdivs_sound e _ _ _ _ _ valid_subdivs in_subdivs) as range_err_check.
pose proof (check_subdivs_sound e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic)) 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 admit.
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. }
admit. (* unsat_queries of empty map *) }
assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
{ eapply result_checking_sound; eauto.
admit. }
admit. (* unsat_queries of empty map *) }
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBounds_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
eexists. eexists. exists vR, vF, mF; repeat split; auto.
destruct (result_leq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
destruct H as [F1 [F2 [sub err_leq]]].
exists iv2, err2, vR, vF, mF; repeat split; auto.
assert (err = err1) by congruence; subst.
apply Qle_Rle in err_leq.
intros vF0 m Heval.
specialize (err_bounded vF0 m Heval).
lra.
Admitted.
\ 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