Commit 25daf249 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Uncomment assumption on checked expressions

parent ac33f759
......@@ -23,13 +23,13 @@ Definition nozeroiv iv :=
Fixpoint validAffineBounds (e: exp Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
(exprsAf: expressionsAffine) (currentMaxNoise: nat): option (expressionsAffine * nat) :=
(* match FloverMap.find e exprsAf with *)
(* | Some _ => *)
(* (* expression has already been checked; we do not want to introduce *) *)
(* (* a new affine polynomial for the same expression *) *)
(* Some (exprsAf, currentMaxNoise) *)
(* | None => *)
(* (* We see it for the first time; update the expressions map *) *)
match FloverMap.find e exprsAf with
| Some _ =>
(* expression has already been checked; we do not want to introduce *)
(* a new affine polynomial for the same expression *)
Some (exprsAf, currentMaxNoise)
| None =>
(* We see it for the first time; update the expressions map *)
olet ares := FloverMap.find e A in
let (intv, _) := ares in
match e with
......@@ -100,7 +100,7 @@ Fixpoint validAffineBounds (e: exp Q) (A: analysisResult) (P: precond) (validVar
if (isSupersetIntv intv iv) && (isSupersetIntv iv intv) then
Some (FloverMap.add e af' exprsAf', n')
else None
(* end *)
end
end.
Fixpoint afQ2R (af: affine_form Q): affine_form R := match af with
......@@ -484,7 +484,7 @@ Definition affine_vars_typed (S: NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m: mType, Gamma v = Some m.
Definition checked_expressions (A: analysisResult) E Gamma iexpmap map1 inoise :=
Definition checked_expressions (A: analysisResult) E Gamma iexpmap inoise map1 :=
forall (e: exp Q),
(exists (af: affine_form Q), FloverMap.find e iexpmap = Some af) ->
exists af vR aiv aerr,
......@@ -498,7 +498,7 @@ Definition checked_expressions (A: analysisResult) E Gamma iexpmap map1 inoise :
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 iexpmap -> *)
checked_expressions A E Gamma iexpmap inoise map1 ->
(inoise > 0)%nat ->
(forall n, (n >= inoise)%nat -> map1 n = None) ->
validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
......@@ -520,14 +520,21 @@ Lemma validAffineBounds_sound (e: exp Q) (A: analysisResult) (P: precond)
Proof.
revert noise exprAfs inoise iexpmap map1.
induction e;
intros * inoisegtz validmap1 validBounds dVarsValid varsDisjoint fVarsSound varsTyped;
intros * visitedExpr inoisegtz validmap1 validBounds dVarsValid varsDisjoint fVarsSound varsTyped;
simpl in validBounds.
-
specialize (dVarsValid n).
- specialize (dVarsValid n).
specialize (fVarsSound n).
specialize (varsTyped n).
(* specialize (visitedExpr (Var Q n) map1 exprAfs noise inoise). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) iexpmap) eqn: Hvisited; eauto using visitedExpr. *)
specialize (visitedExpr (Var Q n)).
destruct (FloverMap.find (elt:=affine_form Q) (Var Q n) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]].
- eexists; reflexivity.
- exists map1, af, vR, aiv, aerr.
intuition.
congruence.
}
destruct (FloverMap.find (elt:=intv * error) (Var Q n) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
destruct (n mem dVars) eqn: Hmem.
......@@ -538,11 +545,7 @@ Proof.
destruct dVarsValid as [af [vR [iv [err dVarsValid]]]]; try reflexivity.
inversion validBounds; subst; clear validBounds.
exists map1, af, vR, iv, err.
intuition; try reflexivity.
constructor; auto.
simpl.
rewrite varsTyped.
reflexivity.
intuition; try congruence.
+ destruct (isSupersetIntv (toIntv (fromIntv (P n) inoise)) aiv) eqn: Hsup; try congruence.
inversion validBounds; subst; clear validBounds.
apply not_in_not_mem in Hmem.
......@@ -554,8 +557,7 @@ Proof.
* exists map1, (fromIntv (P n) inoise), vR, aiv, aerr.
repeat split; auto.
-- reflexivity.
-- apply contained_flover_map_extension.
admit.
-- apply contained_flover_map_extension; assumption.
-- rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
-- unfold fresh, fromIntv, get_max_index.
......@@ -682,7 +684,7 @@ Proof.
-- apply contained_map_extension.
apply validmap1; lia.
-- apply contained_flover_map_extension.
admit.
assumption.
-- rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
-- unfold fresh, fromIntv, get_max_index.
......@@ -701,9 +703,16 @@ Proof.
rewrite varsTyped.
reflexivity.
- clear varsTyped varsDisjoint dVarsValid fVarsSound fVars.
(* specialize (visitedExpr (Const m v)). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited; *)
(* eauto using visitedExpr. *)
specialize (visitedExpr (Const m v)).
destruct (FloverMap.find (elt:=affine_form Q) (Const m v) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]].
- eexists; reflexivity.
- exists map1, af, vR, aiv, aerr.
intuition.
congruence.
}
destruct (FloverMap.find (elt:=intv * error) (Const m v) A) eqn: Hares;
simpl in validBounds; try congruence.
destruct p as [i e].
......@@ -722,7 +731,7 @@ Proof.
repeat split.
+ reflexivity.
+ apply contained_flover_map_extension.
admit.
assumption.
+ unfold fromIntv, toIntv.
simpl.
rewrite Qeq_bool_refl.
......@@ -749,11 +758,17 @@ Proof.
rewrite Q2R_div; try lra.
unfold af_evals, Ropt_eq; simpl.
lra.
-
(* pose proof visitedExpr as visitedExpr'. *)
(* specialize (visitedExpr (Unop u e)). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Unop u e) iexpmap) eqn: Hvisited; *)
(* eauto using visitedExpr. *)
- pose proof visitedExpr as visitedExpr'.
specialize (visitedExpr (Unop u e)).
destruct (FloverMap.find (elt:=affine_form Q) (Unop u e) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
destruct visitedExpr as [af [vR [aiv [aerr visitedExpr]]]].
- eexists; reflexivity.
- exists map1, af, vR, aiv, aerr.
intuition.
congruence.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Unop u e) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
......@@ -769,9 +784,11 @@ Proof.
exists ihmap, (AffineArithQ.negate_aff af), (-vR)%R, aiv, aerr.
inversion validBounds; subst; clear validBounds.
repeat split; auto.
* etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.negate_aff af) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
assumption.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* rewrite plus_0_r.
......@@ -796,9 +813,11 @@ Proof.
* eapply contained_map_trans; try exact Hcont.
apply contained_map_extension.
apply Hsubvalidmap; lia.
* etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.inverse_aff af subnoise) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
assumption.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* now apply AffineArithQ.fresh_inverse_aff.
......@@ -818,11 +837,15 @@ Proof.
simpl evalUnop.
replace (/ vR)%R with (1 / vR)%R by lra.
now rewrite afQ2R_inverse_aff.
-
(* pose proof visitedExpr as visitedExpr'. *)
(* specialize (visitedExpr (Binop b e1 e2)). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Binop b e1 e2) iexpmap) eqn: Hvisited; *)
(* eauto using visitedExpr. *)
- destruct (FloverMap.find (elt:=affine_form Q) (Binop b e1 e2) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
unfold checked_expressions in visitedExpr.
destruct (visitedExpr (Binop b e1 e2)) as [af [vR [aiv [aerr visitedExpr']]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Binop b e1 e2) A) as [p | _] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
......@@ -838,6 +861,9 @@ Proof.
assert (af1' = af1) by congruence; subst.
destruct (IHe2 subnoise2 subexprAff2 subnoise1 subexprAff1 ihmap1) as [ihmap2 [af2' [vR2 [_ [_ [ihcont2 [ihcontf2 [_ [_ [Haf2 [subfresh2 [Hsubvalidmap2 [Hsubnoise2 [subeval2 subaff2]]]]]]]]]]]]]];
try auto; try lra; clear IHe2; eauto using fresh_n_gt_O.
{
admit.
}
{
unfold affine_dVars_range_valid in dVarsValid |-*.
intros v vin.
......@@ -858,10 +884,12 @@ Proof.
* etransitivity; try exact ihcont1.
etransitivity; try exact ihcont2.
reflexivity.
* etransitivity; try eassumption.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.plus_aff af1 af2) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H.
etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* apply AffineArithQ.plus_aff_preserves_fresh; rewrite plus_0_r; auto.
......@@ -886,10 +914,12 @@ Proof.
* etransitivity; try exact ihcont1.
etransitivity; try exact ihcont2.
reflexivity.
* etransitivity; try eassumption.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.subtract_aff af1 af2) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H.
etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* unfold AffineArithQ.subtract_aff.
......@@ -927,10 +957,12 @@ Proof.
* etransitivity; try exact ihcont1.
etransitivity; try exact ihcont2.
apply contained_map_extension; auto.
* etransitivity; try eassumption.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.mult_aff af1 af2 subnoise2) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H.
etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* unfold AffineArithQ.mult_aff.
......@@ -978,10 +1010,12 @@ Proof.
* etransitivity; try exact ihcont1.
etransitivity; try exact ihcont2.
apply contained_map_extension2; apply Hsubvalidmap2; lia.
* etransitivity; try eassumption.
* pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.divide_aff af1 af2 subnoise2) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H.
etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
* rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
* unfold AffineArithQ.divide_aff, AffineArithQ.mult_aff.
......@@ -1031,11 +1065,14 @@ Proof.
rewrite Rmult_1_r.
simpl evalBinop.
rewrite afQ2R_divide_aff; auto.
-
(* pose proof visitedExpr as visitedExpr'. *)
(* specialize (visitedExpr (Fma e1 e2 e3)). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) iexpmap) eqn: Hvisited; *)
(* eauto using visitedExpr. *)
- destruct (FloverMap.find (elt:=affine_form Q) (Fma e1 e2 e3) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
destruct (visitedExpr (Fma e1 e2 e3)) as [af [vR [aiv [aerr visitedExpr']]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Fma e1 e2 e3) A) as [p | _] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
......@@ -1054,6 +1091,9 @@ Proof.
assert (af1' = af1) by congruence; subst.
destruct (IHe2 subnoise2 subexprAff2 subnoise1 subexprAff1 ihmap1) as [ihmap2 [af2' [vR2 [_ [_ [ihcont2 [ihcontf2 [_ [_ [Haf2 [subfresh2 [Hsubmapvalid2 [Hsubnoise2 [subeval2 subaff2]]]]]]]]]]]]]];
try auto; clear IHe2; try lia.
{
admit.
}
{
unfold affine_dVars_range_valid in dVarsValid |-*.
intros v vin.
......@@ -1067,6 +1107,9 @@ Proof.
assert (af2' = af2) by congruence; subst.
destruct (IHe3 subnoise3 subexprAff3 subnoise2 subexprAff2 ihmap2) as [ihmap3 [af3' [vR3 [_ [_ [ihcont3 [ihcontf3 [_ [_ [Haf3 [subfresh3 [Hsubmapvalid3 [Hsubnoise3 [subeval3 subaff3]]]]]]]]]]]]]];
try auto; clear IHe3; try lia.
{
admit.
}
{
unfold affine_dVars_range_valid in dVarsValid |-*.
intros v vin.
......@@ -1102,11 +1145,13 @@ Proof.
etransitivity; try exact ihcont3.
apply contained_map_extension.
apply Hsubmapvalid3; lia.
+ etransitivity; try eassumption.
+ pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3)) Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
clear H.
etransitivity; try eassumption.
etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
+ rewrite FloverMapFacts.P.F.add_eq_o; try auto.
apply Q_orderedExps.expCompare_refl.
+ rewrite <- afQ2R_fresh in fresh1.
......@@ -1146,11 +1191,14 @@ Proof.
rewrite afQ2R_mult_aff.
apply plus_aff_sound; try assumption.
eapply af_evals_map_extension; try apply contained_map_extension; auto.
-
(* pose proof visitedExpr as visitedExpr'. *)
(* specialize (visitedExpr (Downcast m e)). *)
(* destruct (FloverMap.find (elt:=affine_form Q) (Downcast m e) iexpmap) eqn: Hvisited; *)
(* eauto using visitedExpr. *)
- destruct (FloverMap.find (elt:=affine_form Q) (Downcast m e) iexpmap) eqn: Hvisited.
{
inversion validBounds; subst; clear validBounds.
destruct (visitedExpr (Downcast m e)) as [af [vR [aiv [aerr visitedExpr']]]].
- eexists; eauto.
- exists map1, af, vR, aiv, aerr.
intuition.
}
unfold updateExpMap, updateExpMapSucc, updateExpMapIncr in validBounds.
destruct (FloverMap.find (elt:=intv * error) (Downcast m e) A) as [p | p] eqn: Hares; simpl in validBounds; try congruence.
destruct p as [aiv aerr].
......@@ -1169,9 +1217,11 @@ Proof.
exists ihmap, af, (perturb vR 0)%R, aiv, aerr.
apply andb_prop in Hsup as [Hsub__l Hsub__r].
repeat split; auto.
+ etransitivity; try eassumption.
apply contained_flover_map_extension.
admit.
+ pose proof contained_flover_map_extension as H.
specialize (H _ iexpmap _ af Hvisited).
etransitivity; try eassumption.
apply contained_flover_map_add_compat.
assumption.
+ unfold isSupersetIntv in *.
pose proof (supIntvAntisym _ _ Hsub__l Hsub__r) as Heq.
unfold isEqIntv in Heq.
......
......@@ -36,6 +36,23 @@ Proof.
- apply FloverMapFacts.P.F.add_neq_o; congruence.
Qed.
Lemma contained_flover_map_add_compat V (expmap1 expmap2: FloverMap.t V) e v:
contained_flover_map expmap1 expmap2 ->
contained_flover_map (FloverMap.add e v expmap1) (FloverMap.add e v expmap2).
Proof.
unfold contained_flover_map.
intros A e' v' B.
destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
- rewrite FloverMapFacts.P.F.add_eq_o in B; auto.
rewrite FloverMapFacts.P.F.add_eq_o; auto.
- rewrite FloverMapFacts.P.F.add_neq_o in B; try congruence.
rewrite FloverMapFacts.P.F.add_neq_o; try congruence.
auto.
- rewrite FloverMapFacts.P.F.add_neq_o in B; try congruence.
rewrite FloverMapFacts.P.F.add_neq_o; try congruence.
auto.
Qed.
(**
We treat a function mapping an expression arguing on fractions as value type
to pairs of intervals on rationals and rational errors as the analysis result
......
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