Commit 9b7c42d3 authored by Joachim Bard's avatar Joachim Bard

adding proof template for subdiv soundness

parent 18cda710
(*
From Flover
Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
Environments TypeValidator FPRangeValidator ExpressionAbbrevs.
*)
Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker.
(*
From Flover
Require Import Infra.RealRationalProps Environments ExpressionSemantics IntervalArithQ SMTArith
TypeValidator FPRangeValidator ResultChecker.
Require Import Infra.RealRationalProps Environments ExpressionSemantics
IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
*)
Require Import List.
Definition check_subdivs_step e defVars Gamma (b: bool) (PA: precond * analysisResult) :=
let (P, A) := PA in
b && (ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma).
Definition check_subdivs e subdivs defVars Gamma :=
fold_left (check_subdivs_step e defVars Gamma) subdivs true.
......@@ -25,13 +26,14 @@ Qed.
Lemma check_subdivs_sound e subdivs defVars Gamma P A :
check_subdivs e subdivs defVars Gamma = true ->
List.In (P, A) subdivs ->
ResultChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true.
In (P, A) subdivs ->
RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true.
Proof.
intros H Hin.
induction subdivs; cbn in Hin; auto.
destruct Hin; subst; auto.
- cbn in *. destruct (ResultChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?; auto.
- cbn in *.
destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?; auto.
rewrite check_subdivs_false_fp in H; auto.
- apply IHsubdivs; auto. cbn in H.
unfold check_subdivs.
......@@ -39,38 +41,58 @@ Proof.
rewrite check_subdivs_false_fp in H. discriminate H.
Qed.
(* TODO: how to merge 2 analysisResults? *)
Definition merge_subdivs_step (e: expr Q) (acc A: analysisResult) :=
acc.
Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
match FloverMap.find e A1, FloverMap.find e A2 with
| Some (iv1, err1), Some (iv2, err2) =>
let acc1 := FloverMap.add e (unionIntv iv1 iv2, Qmax err1 err2) acc in
match e with
| Unop _ e1 | Downcast _ e1 => merge_subdivs_step e1 acc1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
merge_subdivs_step e2 acc2 A1 A2
| Fma e1 e2 e3 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
let acc3 := merge_subdivs_step e2 acc2 A1 A2 in
merge_subdivs_step e3 acc3 A1 A2
| _ => acc1
end
| _, _ => FloverMap.empty (intv * error)
end.
(* TODO: it might be better to merge all results for one specific expression,
instead of merging 2 results for all expressions *)
Definition merge_subdivs e hd tl : analysisResult :=
fold_left (merge_subdivs_step e) tl hd.
fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
Fixpoint check_merge_subdivs e (M A: analysisResult) :=
Fixpoint result_leq e (A1 A2: analysisResult) :=
match e with
| Unop _ e1 | Downcast _ e1 => check_merge_subdivs e1 M A
| Binop _ e1 e2 | Let _ _ e1 e2 => check_merge_subdivs e1 M A && check_merge_subdivs e2 M A
| Fma e1 e2 e3 => check_merge_subdivs e1 M A && check_merge_subdivs e2 M A && check_merge_subdivs e3 M A
| 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 M, FloverMap.find e A with
| Some (ivM, errM), Some (ivA, errA) => isSupersetIntv ivM ivA && (Qleb errM errA)
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: check precond sound wrt. subdivs *)
(* TODO: don't merge, just check that forall (P', A) subdivs P' <<= P *)
(** Interval subdivisions checking function **)
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
(P: precond) hd tl (defVars: FloverMap.t mType) Gamma :=
check_subdivs e (hd :: tl) defVars Gamma &&
check_merge_subdivs e (merge_subdivs e (snd hd) (map snd tl)) absenv.
(* 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 *) .
(* 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.
**)
Theorem subdivs_checking_is_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
forall (E1 E2: env) DeltaMap,
(forall (e': expr R) (m': mType),
exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
......@@ -87,4 +109,26 @@ Theorem subdivs_checking_is_sound (e: expr Q) (absenv: analysisResult) P hd_subd
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R.
Proof.
intros * deltas_matched P_valid valid_typeMap subdivs_valid.
andb_to_prop subdivs_valid.
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]]].
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.
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 (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
{ eapply result_checking_sound; eauto.
admit. }
assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
{ eapply result_checking_sound; eauto.
admit. }
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.
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