Commit b4497851 authored by Joachim Bard's avatar Joachim Bard

adjusting validAffine_sound_var to precond

parent c6242711
...@@ -41,10 +41,14 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa ...@@ -41,10 +41,14 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) (P: precond) (validVa
if NatSet.mem v validVars then if NatSet.mem v validVars then
Some (exprsAf, currentMaxNoise) Some (exprsAf, currentMaxNoise)
else else
let af := fromIntv (P v) currentMaxNoise in match FloverMap.find e P with
if isSupersetIntv (toIntv af) intv then | Some iv =>
Some (FloverMap.add e af exprsAf, (currentMaxNoise + 1)%nat) let af := fromIntv iv currentMaxNoise in
else None if isSupersetIntv (toIntv af) intv then
Some (FloverMap.add e af exprsAf, (currentMaxNoise + 1)%nat)
else None
| None => None
end
| Const _ c => if isSupersetIntv (c, c) intv then | Const _ c => if isSupersetIntv (c, c) intv then
let af := fromIntv (c,c) currentMaxNoise in let af := fromIntv (c,c) currentMaxNoise in
Some (FloverMap.add e af exprsAf, currentMaxNoise) Some (FloverMap.add e af exprsAf, currentMaxNoise)
...@@ -684,7 +688,7 @@ Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n: ...@@ -684,7 +688,7 @@ Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n:
validAffineBounds (Var Q n) A P dVars iexpmap inoise = Some (exprAfs, noise) -> validAffineBounds (Var Q n) A P dVars iexpmap inoise = Some (exprAfs, noise) ->
affine_dVars_range_valid dVars E A inoise iexpmap map1 -> affine_dVars_range_valid dVars E A inoise iexpmap map1 ->
NatSet.Subset (usedVars (Var Q n) -- dVars) fVars -> NatSet.Subset (usedVars (Var Q n) -- dVars) fVars ->
fVars_P_sound fVars E P -> eval_precond E P ->
validTypes (Var Q n) Gamma -> validTypes (Var Q n) Gamma ->
exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv) exists (map2 : noise_mapping) (af : affine_form Q) (vR : R) (aiv : intv)
(aerr : error), (aerr : error),
...@@ -737,13 +741,17 @@ Proof. ...@@ -737,13 +741,17 @@ Proof.
inversion validBounds; subst; clear validBounds. inversion validBounds; subst; clear validBounds.
exists map1, af, vR, iv, err. exists map1, af, vR, iv, err.
intuition; try congruence. intuition; try congruence.
- destruct (isSupersetIntv (toIntv (fromIntv (P n) inoise)) aiv) eqn: Hsup; try congruence. - assert (exists iv, FloverMap.find (Var Q n) P = Some iv) as [iv find_var]
by (Flover_compute; eauto).
destruct (isSupersetIntv (toIntv (fromIntv iv inoise)) aiv) eqn: Hsup;
try congruence.
inversion validBounds; subst; clear validBounds. inversion validBounds; subst; clear validBounds.
apply not_in_not_mem in Hmem. apply not_in_not_mem in Hmem.
assert (n fVars dVars) as H by intuition. assert (n fVars dVars) as H by intuition.
assert (n fVars) as H' by intuition. (* assert (n fVars) as H' by intuition. *)
specialize (fVarsSound H') as [vR [eMap interval_containment]]. destruct (fVarsSound iv) as [vR [eMap interval_containment]].
assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) (fromIntv (P n) inoise) iexpmap) = Some (fromIntv (P n) inoise)) as Hfind { now apply find_in_precond. }
assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) (fromIntv iv inoise) iexpmap) = Some (fromIntv iv inoise)) as Hfind
by (rewrite FloverMapFacts.P.F.add_eq_o; try auto; apply Q_orderedExps.exprCompare_refl). by (rewrite FloverMapFacts.P.F.add_eq_o; try auto; apply Q_orderedExps.exprCompare_refl).
assert (eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR assert (eval_expr E (toRTMap (toRExpMap Gamma)) DeltaMapR
(toREval (toRExp (Var Q n))) vR REAL) as Heeval. (toREval (toRExp (Var Q n))) vR REAL) as Heeval.
...@@ -753,10 +761,10 @@ Proof. ...@@ -753,10 +761,10 @@ Proof.
{ eexists; eapply toRExpMap_some with (e:= Var Q n); eauto. } { eexists; eapply toRExpMap_some with (e:= Var Q n); eauto. }
destruct t_var as(? & t_var). destruct t_var as(? & t_var).
rewrite t_var; auto. } rewrite t_var; auto. }
destruct (Qeq_bool (ivlo (P n)) (ivhi (P n))) eqn: Heq. destruct (Qeq_bool (ivlo iv) (ivhi iv)) eqn: Heq.
+ assert (af_evals (afQ2R (fromIntv (P n) inoise)) vR map1) as Hevals. + assert (af_evals (afQ2R (fromIntv iv inoise)) vR map1) as Hevals.
{ {
assert (fromIntv (P n) inoise = (AffineForm.Const (ivhi (P n) / (2 # 1) + ivlo (P n) / (2 # 1))%Q)) as HfromIntv assert (fromIntv iv inoise = (AffineForm.Const (ivhi iv / (2 # 1) + ivlo iv / (2 # 1))%Q)) as HfromIntv
by (unfold fromIntv; now rewrite Heq). by (unfold fromIntv; now rewrite Heq).
pose proof Heq as Heq'. pose proof Heq as Heq'.
apply Qeq_bool_iff in Heq'. apply Qeq_bool_iff in Heq'.
......
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