Commit b884a957 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Add validAffineBoundsCmd

parent 7a7f427d
......@@ -2,7 +2,7 @@ Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List
Require Import Recdef.
Require Import Flover.AffineForm Flover.AffineArithQ Flover.AffineArith.
Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing.
Require Import Flover.Infra.Ltacs Flover.Infra.RealSimps Flover.Typing Flover.ssaPrgs.
Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
let new_iv := toIntv new_af in
......@@ -486,9 +486,8 @@ Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
(forall (e: exp Q) map1 exprAfs noise iexpmap inoise,
Definition checked_expressions (A: analysisResult) E Gamma :=
forall (e: exp Q) map1 exprAfs noise iexpmap inoise,
(exists (af: affine_form Q), FloverMap.find e iexpmap = Some af) ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
......@@ -499,7 +498,11 @@ Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
eval_exp E (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
af_evals (afQ2R af) vR map2) ->
af_evals (afQ2R af) vR map2.
Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
checked_expressions A E Gamma ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
......@@ -982,3 +985,71 @@ Proof.
rewrite Rmult_1_r.
assumption.
Qed.
Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
match c with
| Let m x e c' => match FloverMap.find e A, FloverMap.find (Var Q x) A with
| Some ((elo, ehi), _), Some ((xlo, xhi), _) =>
if Qeq_bool elo xlo && Qeq_bool ehi xhi then
olet res__e := validAffineBounds e A P validVars exprsAf currentMaxNoise in
let (exprsAf', noise') := res__e in
validAffineBoundsCmd c' A P (NatSet.add x validVars) exprsAf' noise'
else None
| _, _ => None
end
| Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
end.
Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
checked_expressions A E Gamma ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBoundsCmd c A P dVars iexpmap inoise = Some (exprAfs, noise) ->
ssa c (NatSet.union fVars dVars) outVars ->
affine_dVars_range_valid dVars E A ->
NatSet.Subset (NatSet.diff (Commands.freeVars c) dVars) fVars ->
affine_fVars_P_sound fVars E P ->
affine_vars_typed (NatSet.union fVars dVars) Gamma ->
exists map2 af vR aiv aerr,
contained_map map1 map2 /\
FloverMap.find (getRetExp c) A = Some (aiv, aerr) /\
isSupersetIntv (toIntv af) aiv = true /\
FloverMap.find (getRetExp c) exprAfs = Some af /\
fresh noise af /\
(forall n, (n >= noise)%nat -> map2 n = None) /\
(noise >= inoise)%nat /\
bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) vR M0 /\
af_evals (afQ2R af) vR map2.
Proof.
revert dVars iexpmap inoise exprAfs noise.
induction c; intros * checkedExprs Hnoise Hmapvalid valid_bounds_cmd
Hssa dvars_valid Hsubset fvars_valid vars_typed; simpl in valid_bounds_cmd.
- destruct (FloverMap.find e A) eqn: Hares__e; try congruence.
destruct p as (aiv__e, aerr__e).
destruct aiv__e as (elo, ehi).
destruct (FloverMap.find (Var Q n) A) eqn: Hares__n; try congruence.
destruct p as (aiv__n, aerr__n).
destruct aiv__n as (xlo, xhi).
destruct (Qeq_bool elo xlo && Qeq_bool ehi xhi) eqn: Heq; try congruence.
destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hvalidab;
simpl in valid_bounds_cmd; try congruence.
destruct p as (exprAfs', noise').
pose proof validAffineBounds_sound as validab_sound.
simpl in Hsubset.
specialize (validab_sound e A P fVars dVars E Gamma exprAfs' noise' iexpmap inoise map1
checkedExprs Hnoise Hmapvalid Hvalidab dvars_valid).
edestruct IHc; clear IHc.
Focus 4.
exact valid_bounds_cmd.
all: try eassumption.
- simpl.
eapply validAffineBounds_sound in valid_bounds_cmd; auto.
destruct valid_bounds_cmd as [map2 [af [vR [aiv [aerr valid_bounds_cmd]]]]].
exists map2, af, vR, aiv, aerr.
intuition.
all: try eassumption.
constructor.
eauto.
Admitted.
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