Commit c6ea9dea authored by Joachim Bard's avatar Joachim Bard

Merge remote-tracking branch 'upstream/master'

parents 7a686633 7f62e7d7
......@@ -9,7 +9,7 @@ From Flover
ResultChecker SubdivsChecker.
Require Export List ExpressionSemantics Coq.QArith.QArith Flover.SMTArith
RealRangeArith ErrorAnalysis FPRangeValidator.
RealRangeArith ErrorAnalysis FPRangeValidator ssaPrgs.
Export ListNotations.
(** Certificate checking function **)
......@@ -36,18 +36,19 @@ Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
CertificateChecker e absenv P Qmap subdivs defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
exists iv err vR vF m,
exists iv err vR vF m outVars,
FloverMap.find e absenv = Some (iv, err) /\
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
(forall vF m,
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R /\
ssa e (freeVars e) outVars /\
validTypes e Gamma /\
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma absenv.
validFPRanges e E2 Gamma DeltaMap.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -65,6 +66,10 @@ Proof.
- edestruct result_checking_sound as (validR & validFPR & validErr); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & H4); eauto.
assert (validSSA e (freeVars e) = true) as Hssa_small.
{ apply andb_true_iff in certificate_valid as (Hssa & _).
eapply validSSA_downward_closed; eauto using validSSA_checks_freeVars. set_tac. }
apply validSSA_sound in Hssa_small as (outVars & Hssa_small).
repeat eexists; eauto.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
......@@ -98,6 +103,6 @@ Proof.
edestruct (Certificate_checking_is_sound_general)as [Gamma validCert]; eauto.
exists Gamma. intros approxEnvs.
specialize (validCert approxEnvs).
destruct validCert as (? & ? & ? & ? & ? & ? & ? & ? & ? & ?).
destruct validCert as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?).
repeat eexists; eauto.
Qed.
......@@ -25,6 +25,12 @@ Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
validErrorBoundsRec e3 E1 E2 A Gamma DeltaMap
| Let m x e1 e2 =>
validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
(forall iv_e1 err_e1 iv_x err_x,
FloverMap.find e1 A = Some (iv_e1, err_e1) ->
FloverMap.find (Var Q x) A = Some (iv_x, err_x) ->
(Q2R (ivhi iv_e1) = Q2R (ivhi iv_x) /\
Q2R (ivlo iv_e1) = Q2R (ivlo iv_x) /\
Q2R (err_e1) = Q2R (err_x))) /\
(forall v__R v__FP,
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e1)) v__R REAL ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e1) v__FP m ->
......
......@@ -3143,7 +3143,8 @@ Proof.
specialize (IHe2 Hchecked).
specialize Hsubexpr as ((Hsubexpr1 & Hsubexpr2) & Hin).
unfold validErrorBounds in IHe1, IHe2.
split; auto.
split; [repeat split; try auto | ].
{ admit. }
intros * Heval__R Hcert.
specialize Hchecked as (Hex & Hall); eauto.
intuition.
......
......@@ -373,14 +373,27 @@ Proof.
cbn in *. Flover_compute; try congruence.
destruct typing_ok
as [me [find_me [[validt_e [validt_f [? [find_e [find_x [find_f ?]]]]]] validt_exec]]].
destruct valid_intv as [[validRange_e1 validRange_e2] eval_real]; auto.
destruct valid_intv as [[validRange_e1 [validBound_x validRange_e2]] eval_real]; auto.
destruct eval_real as [iv_1 [err_1 [vR1 [? [eval_real1 range_valid]]]]].
assert (validErrorBounds e1 E1 E2 A Gamma) as Hsound
by (eapply IHe1; eauto).
split.
{
split.
split; [ | split ].
- eapply IHe1; eauto.
- intros * find_e1 find_x2.
unfold error in *.
repeat (match goal with
| H1: FloverMap.find ?e1 ?A = Some (?iv1, ?err1),
H2: FloverMap.find ?e1 ?A = Some (?iv2, ?err2) |- _ =>
rewrite H1 in H2; inversion H2; subst; clear H2;
let v := fresh "find" in
revert H1; intros v
end).
destruct validBound_x as (? & ? & ? & ? & ? & ? & ?).
repeat (match goal with
| H: Some ?a = Some ?b |- _ => inversion H; subst; clear H end).
andb_to_prop H2; canonize_hyps. intuition.
- intros vR vF eval_real eval_float.
eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vFe [mFe eval_float_e]] bounded_e].
......@@ -415,7 +428,6 @@ Proof.
assert (vR = vR1)
by (eapply (meps_0_deterministic (Let REAL n (toRExp e1) (toRExp e2))); eauto); subst.
inversion eval_real; subst.
destruct m2; try discriminate.
specialize (Hsound DeltaMap deltas_matched).
apply validErrorBoundsRec_single with (v__R := v1) (iv:= i0) (err:= e0) in Hsound; auto.
destruct Hsound as [[ve1 [me1 evalExists]] evalHasError].
......@@ -448,12 +460,20 @@ Proof.
eapply validErrorBoundsRec_single in Hsound2; eauto.
destruct Hsound2 as [[v2 [m2 eval_fixed]] ?].
split.
assert (x = m2) by (eapply validTypes_exec; eauto).
assert (m = me1) by (eapply validTypes_exec; try exact evalExists; eauto).
injection find_me; intros Heq. subst.
+ exists v2, me.
eapply Let_dist with (E:=E2); try eassumption.
eapply toRExpMap_some; eauto. auto.
eapply toRExpMap_some with (e2:=toRExp (Let me1 n e1 e2)); eauto.
destruct valid_types' as (? & ? & ?).
inversion H1; subst.
destruct H2 as [(? & ? & ? & ? & ? & ? & ?) ?].
eapply validTypes_single in H4.
destruct H4 as (? & ? & ?).
rewrite H13 in *. inversion H4; subst.
assert (m2 = x1).
{ eapply H16; eauto. }
subst. auto.
+ intros * eval_float.
(* clear eval_fixed. *)
inversion eval_float; subst.
......@@ -471,10 +491,10 @@ Proof.
- eapply ssa_equal_set; eauto.
split; set_tac; tauto.
- intros a ?. apply fVars_subset. set_tac.
split; [right| intros ?; apply H4; set_tac].
split; [right| intros ?; apply H2; set_tac].
split; auto.
intros ?; subst. apply H4. set_tac. }
eapply validErrorBoundsRec_single in H2; eauto.
destruct H2. eapply H4; eauto.
intros ?; subst. apply H2. set_tac. }
eapply validErrorBoundsRec_single in H1; eauto.
destruct H1. eapply H2; eauto.
(* - cbn in *. Flover_compute; congruence. *)
Qed.
\ No newline at end of file
......@@ -82,11 +82,10 @@ Inductive eval_expr (E:env)
eval_expr E Gamma DeltaMap f2 v2 m2 ->
eval_expr E Gamma DeltaMap f3 v3 m3 ->
eval_expr E Gamma DeltaMap (Fma f1 f2 f3) (perturb (evalFma v1 v2 v3) m delta) m
| Let_dist m1 m2 m x f1 f2 v1 v:
| Let_dist m1 m x f1 f2 v1 v:
Gamma (Let m1 x f1 f2) = Some m ->
isCompat m2 m = true ->
eval_expr E Gamma DeltaMap f1 v1 m1 ->
eval_expr (updEnv x v1 E) Gamma DeltaMap f2 v m2 ->
eval_expr (updEnv x v1 E) Gamma DeltaMap f2 v m ->
eval_expr E Gamma DeltaMap (Let m1 x f1 f2) v m
(*
| Cond_then m1 m2 m3 m f1 f2 f3 v1 v delta:
......@@ -251,7 +250,7 @@ Proof.
unfold isJoin3 in H4; simpl in H4.
destruct m; try congruence; auto.
- auto.
- cbn in H3. congruence.
- eapply IHf2; eauto.
(*
- cbn in H2. congruence.
- cbn in H2. congruence.
......@@ -316,7 +315,6 @@ Proof.
- inversion ev1; inversion ev2.
assert (v0 = v3) by (eapply IHf1; eauto).
destruct m2; try discriminate.
destruct m4; try discriminate.
subst.
eapply IHf2; eauto.
(*
......@@ -614,7 +612,6 @@ Proof.
reflexivity.
- inversion Heval1; inversion Heval2; subst.
replace v0 with v3 in * by (eapply IHe1; eauto).
assert (m2 = m4) by (eapply Gamma_det; eauto); subst.
eapply IHe2; eauto.
(*
- inversion Heval1; inversion Heval2; subst.
......@@ -671,7 +668,6 @@ Proof.
+ trivial.
+ apply Rabs_0_impl_eq in H4; f_equal; now symmetry.
- inversion ev1; subst.
destruct m2; try discriminate.
econstructor; eauto.
(*
- inversion ev1; subst.
......
This diff is collapsed.
This diff is collapsed.
......@@ -442,6 +442,9 @@ Proof.
by (apply preVars_free; eapply preIntvVars_sound; eauto).
exfalso. apply H3. set_tac. }
repeat split; auto.
+ repeat eexists; try eauto.
simpl. apply eqR_Qeq in L1; apply eqR_Qeq in R.
rewrite <- Qeq_bool_iff in *. intuition.
+ intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); now subst.
+ apply validRanges_single in valid_f2.
......@@ -449,6 +452,5 @@ Proof.
rewrite find_v2 in *; inversion Heqo2; subst.
cbn in *.
eexists. eexists. exists v2.
repeat split; eauto; try lra.
econstructor; eauto; reflexivity.
repeat split; eauto; lra.
Qed.
\ No newline at end of file
......@@ -82,6 +82,10 @@ Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
| Downcast m e1 => validRanges e1 A E Gamma
| Let _ x e1 e2 =>
validRanges e1 A E Gamma /\
(exists iv1 err1 iv_x err_x,
FloverMap.find e1 A = Some (iv1, err1) /\
FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
Qeq_bool (ivlo iv1) (ivlo iv_x) && Qeq_bool (ivhi iv1) (ivhi iv_x) = true) /\
(forall vR, eval_expr E Gamma DeltaMapR (toREval (toRExp e1)) vR REAL ->
validRanges e2 A (updEnv x vR E) Gamma)
(*
......@@ -122,9 +126,9 @@ Proof.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1 as [[? [? ?]] ?]; auto.
- destruct valid1; auto.
- destruct valid1 as [[H1 H2] _]; auto.
split; auto. intros.
eauto using swap_Gamma_eval_expr.
- destruct valid1 as [[H1 [H2 H3]] _]; auto.
repeat split; try auto.
intros. eauto using swap_Gamma_eval_expr.
(* - destruct valid1 as [[? [? ?]] ?]; auto. *)
Qed.
......@@ -337,10 +341,18 @@ Proof.
congruence.
+ apply N.compare_eq in Heq; subst.
rewrite N.eqb_refl in *; congruence.
- intros valid1; destruct valid1 as [[validsub1 validsub2] validr1].
- intros valid1; destruct valid1
as [[validsub1 [(? & ? & ? & ? & find_e1 & find_x & valid_equiv) validsub2]] validr1].
destruct validr1 as [iv [err [vR [Hfind [Hee Hcont]]]]].
inversion Hee; subst.
apply nat_compare_eq in e4; subst.
repeat split; auto.
+ specialize (IHc e5 E validsub1).
apply validRanges_single in IHc.
destruct IHc as (iv_e1 & err_e1 & vR1 & find_e21 & eval_e21 & bounded_e21).
erewrite FloverMapFacts.P.F.find_o with (y:= e21) in find_e1; eauto.
rewrite find_e21 in find_e1; inversion find_e1; subst.
repeat eexists; eauto.
+ intros v ?.
eapply IHc0; eauto.
apply validsub2.
......
......@@ -17,20 +17,23 @@ 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:
Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVars Gamma DeltaMap:
forall (E1 E2: env),
(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.
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validFPRanges e E2 Gamma DeltaMap /\
validErrorBounds e E1 E2 absenv Gamma.
(**
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 * deltas_matched approxE1E2 P_valid unsat_qs valid_typeMap results_valid.
unfold ResultChecker in results_valid.
assert (validTypes e Gamma).
{ eapply getValidMap_top_correct; eauto.
......@@ -50,7 +53,7 @@ Proof.
assert (NatSet.Subset (freeVars e -- NatSet.empty) (freeVars e)).
{ hnf; intros a in_empty.
set_tac. }
rename R into validFPRanges.
rename R into validFPR.
rename R0 into validRoundoffErr.
pose proof (validSSA_checks_freeVars _ _ L) as sub.
destruct (validSSA_sound e (preVars P)) as [outVars ssa_e]; auto.
......@@ -72,8 +75,11 @@ Proof.
*)
assert (ssa e (NatSet.union (freeVars e) (NatSet.empty)) outVars2).
{ eapply ssa_equal_set; eauto. }
split; auto.
eapply RoundoffErrorValidator_sound; eauto.
repeat split; auto.
- eapply FPRangeValidator_sound; eauto.
+ eapply RoundoffErrorValidator_sound; eauto.
+ intros v Hin. set_tac.
- eapply RoundoffErrorValidator_sound; eauto.
Qed.
(**
......
......@@ -93,8 +93,7 @@ Proof.
econstructor; try eauto.
+ eapply IHe1; try eauto.
now extended_ssa.
+ destruct m2; try discriminate.
eapply (IHe2 _ (NatSet.add n inVars)); eauto.
+ eapply (IHe2 _ (NatSet.add n inVars)); eauto.
2: intros; set_tac; right; eapply LfVars_valid; eauto;
set_tac; tauto.
intros x e v'.
......@@ -102,7 +101,7 @@ Proof.
destruct (x =? n) eqn: Heq.
* intros Hx He.
apply beq_nat_true in Heq; subst.
set_tac. exfalso. apply H5. eapply LfVars_valid; eauto.
set_tac. exfalso. apply H4. eapply LfVars_valid; eauto.
set_tac.
* intros H0 H1.
inversion H1; subst. rewrite Heq in *.
......@@ -110,7 +109,7 @@ Proof.
{ eapply Lsound; eauto. now constructor. }
{ rewrite freeVars_toREval_toRExp_compat.
set_tac. intros ?.
apply H5. eapply LfVars_valid; eauto.
apply H4. eapply LfVars_valid; eauto.
set_tac. }
* now extended_ssa.
(*
......@@ -668,6 +667,9 @@ Proof.
- apply eval_precond_updEnv; auto.
intros ?. set_tac. apply H3. clear H. set_tac. }
repeat split; auto.
+ repeat eexists; try eauto.
simpl. apply eqR_Qeq in L2; apply eqR_Qeq in R.
rewrite <- Qeq_bool_iff in *. intuition.
+ intros vR ?.
assert (vR = v) by (eapply meps_0_deterministic; eauto); now subst.
+ apply validRanges_single in valid_f2.
......@@ -676,5 +678,4 @@ Proof.
cbn in *.
eexists. eexists. exists v2.
repeat split; eauto; try lra.
econstructor; eauto; reflexivity.
Qed.
......@@ -54,7 +54,7 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType): Prop :=
validTypes e2 Gamma /\
exists me,
FloverMap.find e1 Gamma = Some m /\ FloverMap.find (Var Q x) Gamma = Some m /\
FloverMap.find e2 Gamma = Some me /\ isCompat me mG = true
FloverMap.find e2 Gamma = Some me /\ me = mG
(*
| Cond e1 e2 e3 =>
validTypes e1 Gamma /\
......@@ -1361,8 +1361,8 @@ Proof.
specialize (map_sound (Let m0 n e1 e2) m1).
change (Let m0 n (toRExp e1) (toRExp e2))
with (toRExp (Let m0 n e1 e2)) in *.
eapply toRExpMap_find_map in H6.
rewrite map_sound in H6; try congruence.
eapply toRExpMap_find_map in H8.
rewrite map_sound in H8; try congruence.
rewrite map_find_add. unfold Q_orderedExps.compare.
now rewrite FloverMap.E.eq_refl. }
* apply validTypes_mono with (map1 := t0) ; eauto.
......@@ -1411,15 +1411,13 @@ Proof.
rewrite Q_orderedExps.exprCompare_antisym.
destruct (Q_orderedExps.exprCompare e2 (Let m0 n e1 e2)) eqn:?;
simpl in *; try congruence.
* unfold isMonotone in *. type_conv.
unfold isCompat; destruct m; auto using morePrecise_refl.
+ intros * map_sound eval_let.
inversion eval_let; subst.
specialize (map_sound (Let m0 n e1 e2) m).
change (Let m0 n (toRExp e1) (toRExp e2))
with (toRExp (Let m0 n e1 e2)) in *.
eapply toRExpMap_find_map in H6.
rewrite map_sound in H6; try congruence.
eapply toRExpMap_find_map in H8.
rewrite map_sound in H8; try congruence.
rewrite map_find_add. unfold Q_orderedExps.compare.
now rewrite FloverMap.E.eq_refl. }
* apply validTypes_mono with (map1 := t0) ; eauto.
......
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