Commit 726fe011 authored by Nikita Zyuzin's avatar Nikita Zyuzin

WIP update

parent 3c902fe7
......@@ -1830,8 +1830,82 @@ Proof.
apply visitedSubexpr; eauto.
Qed.
Lemma validAffineBounds_sound_validRanges e A P fVars dVars E Gamma exprmap2 noise2
exprmap1 noise1 map1:
Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma:
(exists map af vR aiv aerr,
FloverMap.find e A = Some (aiv, aerr) /\
isSupersetIntv (toIntv af) aiv = true /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
af_evals (afQ2R af) vR map) ->
exists iv err vR,
FloverMap.find e A = Some (iv, err) /\
eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
(Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
Proof.
intros sound_affine.
destruct sound_affine as [map [af [vR [aiv [aerr [Haiv [Hsup [Hee Heval]]]]]]]].
exists aiv, aerr, vR.
split; try split; try auto.
apply AffineArith.to_interval_containment in Heval.
unfold isSupersetIntv in Hsup.
apply andb_prop in Hsup as [Hsupl Hsupr].
apply Qle_bool_iff in Hsupl.
apply Qle_bool_iff in Hsupr.
apply Qle_Rle in Hsupl.
apply Qle_Rle in Hsupr.
rewrite <- to_interval_to_intv in Heval.
simpl in Heval.
destruct Heval as [Heval1 Heval2].
split; eauto using Rle_trans.
Qed.
Lemma test u e A P dVars exprmap1 noise1 exprmap2 noise2:
validAffineBounds (Unop u e) A P dVars exprmap1 noise1 = Some (exprmap2, noise2) ->
exists af, FloverMap.find e exprmap2 = Some af.
Proof.
intros valid_bounds; simpl in valid_bounds.
destruct (FloverMap.find (Unop u e) exprmap1); simpl in valid_bounds.
- inversion valid_bounds; subst.
admit.
- destruct (FloverMap.find (Unop u e) A); simpl in valid_bounds; try congruence.
destruct p as (iv, _).
destruct (validAffineBounds e A P dVars exprmap1 noise1); simpl in valid_bounds; try congruence.
destruct p as (exprmap', noise').
destruct (FloverMap.find (elt:=affine_form Q) e exprmap') as [af |] eqn: Hfind;
simpl in valid_bounds; try congruence.
destruct u eqn: Hu; unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in valid_bounds.
+ destruct (isSupersetIntv (toIntv (AffineArithQ.negate_aff af)) iv);
simpl in valid_bounds; try congruence.
inversion valid_bounds; subst; clear valid_bounds.
exists af.
rewrite FloverMapFacts.P.F.add_neq_o; eauto.
clear - e.
remember (Unop Neg e) as x.
revert Heqx.
functional induction (Q_orderedExps.exprCompare x e); try congruence.
intros H.
rewrite unopEq_compat_eq in e5; subst.
inversion H; subst.
apply IHc.
reflexivity.
+ destruct (nozeroiv (toIntv af)); simpl in valid_bounds; try congruence.
destruct (isSupersetIntv (toIntv (AffineArithQ.inverse_aff af noise')) iv);
simpl in valid_bounds; try congruence.
inversion valid_bounds; subst; clear valid_bounds.
exists af.
rewrite FloverMapFacts.P.F.add_neq_o; eauto.
clear - e.
remember (Unop Inv e) as x.
revert Heqx.
functional induction (Q_orderedExps.exprCompare x e); try congruence.
intros H.
rewrite unopEq_compat_eq in e5; subst.
inversion H; subst.
apply IHc.
reflexivity.
Admitted.
Lemma validAffineBounds_sound_validRanges e A P fVars dVars E Gamma
exprmap2 noise2 exprmap1 noise1 map1:
(forall e, (exists af, FloverMap.find e exprmap1 = Some af) ->
checked_expressions A E Gamma fVars dVars e exprmap1 noise1 map1) ->
(noise1 > 0)%nat ->
......@@ -1843,13 +1917,27 @@ Lemma validAffineBounds_sound_validRanges e A P fVars dVars E Gamma exprmap2 noi
affine_vars_typed (NatSet.union fVars dVars) Gamma ->
validRanges e A E Gamma.
Proof.
revert noise2 exprmap2 noise1 exprmap1 map1.
induction e; intros * checked_expressions1 Hnoisepose1 Hvalidmap1 Hvalidbounds1 Hdvars1
Hsubset1 Hfvars1 Htypes1;
edestruct validAffineBounds_sound as [map2 [af [vR [iv [err valid_bounds_sound]]]]]; eauto.
- simpl; split; eauto.
exists iv, err, vR.
split; try split.
1-2: intuition.
apply validAffineBounds_validRanges.
intuition; repeat eexists; eauto.
- simpl; split; eauto.
apply validAffineBounds_validRanges.
intuition; repeat eexists; eauto.
- simpl; split; [| apply validAffineBounds_validRanges; intuition; repeat eexists; eauto].
simpl in Hvalidbounds1.
destruct (FloverMap.find (elt:=affine_form Q) (Unop u e) exprmap1) eqn: Hfind1.
+ inversion Hvalidbounds1; subst; clear Hvalidbounds1.
eapply IHe; eauto.
+ destruct (FloverMap.find (elt:=intv * error) (Unop u e) A);
simpl in Hvalidbounds1; try congruence.
destruct p as [iv1 err1].
destruct (validAffineBounds e A P dVars exprmap1 noise1) eqn:?;
simpl in Hvalidbounds1; try congruence.
destruct p; eauto.
Qed.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
......
......@@ -13,7 +13,7 @@ From Coq
From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Environments IntervalValidation Typing
ErrorBounds.
ErrorBounds RealRangeValidator.
(** Error bound validator **)
Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
......
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