From 25daf249cf407e86e4c02b8ab4e0de64bf00c53d Mon Sep 17 00:00:00 2001 From: Nikita Zyuzin Date: Thu, 3 May 2018 17:03:30 +0200 Subject: [PATCH] Uncomment assumption on checked expressions --- coq/AffineValidation.v | 192 +++++++++++++++++++++------------- coq/Infra/ExpressionAbbrevs.v | 17 +++ 2 files changed, 138 insertions(+), 71 deletions(-) diff --git a/coq/AffineValidation.v b/coq/AffineValidation.v index 572d22f..447c225 100644 --- a/coq/AffineValidation.v +++ b/coq/AffineValidation.v @@ -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. diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v index 04c5162..0a0fc18 100644 --- a/coq/Infra/ExpressionAbbrevs.v +++ b/coq/Infra/ExpressionAbbrevs.v @@ -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 -- GitLab