From 2cb9688427bed54046ebb83e8e6997db4c1641b5 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Mon, 30 Oct 2017 13:44:17 +0100 Subject: [PATCH] WIP port to finite maps --- coq/Environments.v | 18 +-- coq/Expressions.v | 12 +- coq/Infra/Abbrevs.v | 12 ++ coq/Infra/ExpressionAbbrevs.v | 13 +- coq/Infra/NatSet.v | 41 +++--- coq/IntervalValidation.v | 257 ++++++++++++++++------------------ 6 files changed, 184 insertions(+), 169 deletions(-) diff --git a/coq/Environments.v b/coq/Environments.v index 8cbfc06..2fbc34a 100644 --- a/coq/Environments.v +++ b/coq/Environments.v @@ -20,9 +20,10 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t (Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2) -|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m: +|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err: approxEnv E1 defVars A fVars dVars E2 -> - (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R -> + DaisyMap.find (Var Q x) A = Some (iv, err) -> + (Rabs (v1 - v2) <= Q2R err)%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2). @@ -66,8 +67,8 @@ Proof. set_tac. rewrite NatSet.union_spec in x_valid. destruct x_valid; set_tac. - rewrite NatSet.add_spec in H1. - destruct H1; subst; try auto. + rewrite NatSet.add_spec in H2. + destruct H2; subst; try auto. rewrite Nat.eqb_refl in eq_case; congruence. Qed. @@ -100,7 +101,7 @@ Proof. - assert (x =? x0 = false) as x_x0_neq. { rewrite Nat.eqb_neq; hnf; intros; subst. set_tac. - apply H0. + apply H1. set_tac. } unfold updEnv in *; rewrite x_x0_neq in *. apply IHa; auto. @@ -108,12 +109,12 @@ Proof. rewrite x_x0_neq in x_typed; auto. Qed. -Lemma approxEnv_dVar_bounded v2 m e: +Lemma approxEnv_dVar_bounded v2 m iv e: E1 x = Some v -> E2 x = Some v2 -> NatSet.In x dVars -> Gamma x = Some m -> - snd (A (Var Q x)) = e -> + DaisyMap.find (Var Q x) A = Some (iv, e) -> (Rabs (v - v2) <= Q2R e)%R. Proof. induction approxEnvs; @@ -132,7 +133,8 @@ Proof. destruct x_def as [x_x0 | [x_neq x_def]]; subst. + unfold updEnv in *; rewrite Nat.eqb_refl in *; simpl in *. - inversion E1_def; inversion E2_def; subst; auto. + inversion E1_def; inversion E2_def; subst. + rewrite A_e in *; inversion H; auto. + unfold updEnv in *; simpl in *. rewrite <- Nat.eqb_neq in x_neq. rewrite x_neq in *; simpl in *. diff --git a/coq/Expressions.v b/coq/Expressions.v index 44ee717..1ea7184 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -1,9 +1,9 @@ (** Formalization of the base expression language for the daisy framework **) -Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith - Coq.QArith.Qreals Coq.Structures.Orders Coq.Structures.OrderedType - Coq.Structures.OrdersFacts. +From Coq +Require Import Reals.Reals micromega.Psatz QArith.QArith QArith.Qreals +Structures.Orders. Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps Daisy.Infra.Ltacs. Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet @@ -194,8 +194,10 @@ Proof. eapply IHe; eauto. Qed. -Module ExpOrderedType (V_ordered:OrderedType) <: OrderedType. - Module V_orderedFacts := OrderedTypeFacts (V_ordered). +Module Type OrderType := Coq.Structures.Orders.OrderedType. + +Module ExpOrderedType (V_ordered:OrderType) <: OrderType. + Module V_orderedFacts := OrdersFacts.OrderedTypeFacts (V_ordered). Definition V := V_ordered.t. Definition t := exp V. diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index e37b961..83280b1 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -62,3 +62,15 @@ Definition updEnv (x:nat) (v: R) (E:env) (y:nat) := Definition updDefVars (x:nat) (m:mType) (defVars:nat -> option mType) (y:nat) := if (y =? x) then Some m else defVars y. + +Definition optionLift (V T:Type) (v:option V) default (f: V -> T) := + match v with + | None => default + | Some val => f val + end. + +Ltac optionD := + match goal with + |H: context[optionLift ?v ?default ?f] |- _ => + destruct ?v eqn:? + end. \ No newline at end of file diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v index 212dc47..ba3670c 100644 --- a/coq/Infra/ExpressionAbbrevs.v +++ b/coq/Infra/ExpressionAbbrevs.v @@ -2,11 +2,20 @@ Some abbreviations that require having defined expressions beforehand If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve. **) -Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals. +Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts. Require Export Daisy.Infra.Abbrevs Daisy.Expressions. + +Module Q_orderedExps := ExpOrderedType (Q_as_OT). +Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps). + +Module DaisyMap := FMapAVL.Make(legacy_OrderedQExps). +Module DaisyMapFacts := OrdProperties (DaisyMap). + +Definition analysisResult :Type := DaisyMap.t (intv * error). + (** 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 **) -Definition analysisResult :Type := exp Q -> intv * error. \ No newline at end of file +(* Definition analysisResult :Type := exp Q -> intv * error. *) \ No newline at end of file diff --git a/coq/Infra/NatSet.v b/coq/Infra/NatSet.v index b3647aa..afd27d2 100644 --- a/coq/Infra/NatSet.v +++ b/coq/Infra/NatSet.v @@ -55,26 +55,6 @@ Proof. congruence. Qed. -(** TODO: Merge with NatSet_prop tactic in Ltacs file **) -Ltac set_hnf_tac := - match goal with - | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H; set_hnf_tac - | [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H; set_hnf_tac - | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec; set_hnf_tac - | [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec; set_hnf_tac - | [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec; set_hnf_tac - | [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H; set_hnf_tac - | [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec - | [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros; set_hnf_tac - | [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H; set_hnf_tac - | _ => idtac - end. - -Ltac set_tac := - set_hnf_tac; - simpl in *; try auto. - - Lemma add_spec_strong: forall x y S, (x ∈ (NatSet.add y S)) <-> x = y \/ ((~ (x = y)) /\ (x ∈ S)). @@ -91,3 +71,24 @@ Proof. - rewrite NatSet.add_spec. destruct x_in_add as [ x_eq | [x_neq x_in_S]]; auto. Qed. + +(** TODO: Merge with NatSet_prop tactic in Ltacs file **) +Ltac set_hnf_tac := + match goal with + | [ H: NatSet.mem ?x _ = true |- _ ] => rewrite NatSet.mem_spec in H + | [ H: NatSet.mem ?x _ = false |- _] => apply not_in_not_mem in H + | [ H: context [NatSet.In ?x (NatSet.diff ?A ?B)] |- _] => rewrite NatSet.diff_spec in H; destruct H + | [ H: NatSet.Subset ?SA ?SB |- NatSet.In ?v ?SB] => apply H + | [ H: NatSet.In ?x (NatSet.singleton ?y) |- _] => apply NatSetProps.Dec.F.singleton_1 in H + | [ H: NatSet.In ?x NatSet.empty |- _ ] => inversion H + | [ H: NatSet.In ?x (NatSet.union ?S1 ?S2) |- _ ] => rewrite NatSet.union_spec in H + | [ |- context [NatSet.mem ?x _]] => rewrite NatSet.mem_spec + | [ |- context [NatSet.In ?x (NatSet.union ?SA ?SB)]] => rewrite NatSet.union_spec + | [ |- context [NatSet.In ?x (NatSet.diff ?A ?B)]] => rewrite NatSet.diff_spec + | [ |- context [NatSet.In ?x (NatSet.singleton ?y)]] => rewrite NatSet.singleton_spec + | [ |- context [NatSet.Subset ?SA ?SB]] => hnf; intros + end. + +Ltac set_tac := + repeat set_hnf_tac; + simpl in *; try auto. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index b72f017..8448e78 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -10,37 +10,42 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRat Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps Daisy.Typing. Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs. -Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) := - let (intv, _) := absenv e in - match e with - | Var _ v => - if NatSet.mem v validVars - then true - else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v))) - | Const _ n => isSupersetIntv (n,n) intv - | Unop o f => - if validIntervalbounds f absenv P validVars - then - let (iv, _) := absenv f in - match o with - | Neg => - let new_iv := negateIntv iv in - isSupersetIntv new_iv intv - | Inv => - if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) || - ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0)))) - then - let new_iv := invertIntv iv in +Fixpoint validIntervalbounds (e:exp Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= + match DaisyMap.find e A with + | None => false + | Some (intv, _) => + match e with + | Var _ v => + if NatSet.mem v validVars + then true + else isSupersetIntv (P v) intv && (Qleb (ivlo (P v)) (ivhi (P v))) + | Const _ n => isSupersetIntv (n,n) intv + | Unop o f => + if validIntervalbounds f A P validVars + then + match DaisyMap.find f A with + | None => false + | Some (iv, _) => + match o with + | Neg => + let new_iv := negateIntv iv in isSupersetIntv new_iv intv - else false + | Inv => + if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) || + ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0)))) + then + let new_iv := invertIntv iv in + isSupersetIntv new_iv intv + else false + end end else false | Binop op f1 f2 => - if ((validIntervalbounds f1 absenv P validVars) && - (validIntervalbounds f2 absenv P validVars)) + if ((validIntervalbounds f1 A P validVars) && + (validIntervalbounds f2 A P validVars)) then - let (iv1,_) := absenv f1 in - let (iv2,_) := absenv f2 in + match DaisyMap.find f1 A, DaisyMap.find f2 A with + | Some (iv1, _), Some (iv2, _) => match op with | Plus => let new_iv := addIntv iv1 iv2 in @@ -59,83 +64,67 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (vali isSupersetIntv new_iv intv else false end + | _, _ => false + end else false | Downcast _ f1 => - if (validIntervalbounds f1 absenv P validVars) + if (validIntervalbounds f1 A P validVars) then - let (iv1, _) := absenv f1 in + match DaisyMap.find f1 A with + | None => false + | Some (iv1, _) => (* TODO: intv = iv1 might be a hard constraint... *) (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv) + end else false - end. + end + end. -Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= +Fixpoint validIntervalboundsCmd (f:cmd Q) (A:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= match f with | Let m x e g => - if (validIntervalbounds e absenv P validVars && - Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) && - Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x))))) - then validIntervalboundsCmd g absenv P (NatSet.add x validVars) - else false + match DaisyMap.find e A, DaisyMap.find (Var Q x) A with + | Some ((e_lo,e_hi), _), Some ((x_lo, x_hi), _) => + if (validIntervalbounds e A P validVars && + Qeq_bool (e_lo) (x_lo) && + Qeq_bool (e_hi) (x_hi)) + then validIntervalboundsCmd g A P (NatSet.add x validVars) + else false + | _, _ => false + end |Ret e => - validIntervalbounds e absenv P validVars + validIntervalbounds e A P validVars end. -Theorem ivbounds_approximatesPrecond_sound f absenv P V: - validIntervalbounds f absenv P V = true -> - forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) -> - Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))). +Theorem ivbounds_approximatesPrecond_sound f A P dVars iv err: + validIntervalbounds f A P dVars = true -> + forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) dVars) -> + DaisyMap.find (Var Q v) A = Some (iv, err) -> + Is_true(isSupersetIntv (P v) iv). Proof. - induction f; unfold validIntervalbounds. - - simpl. intros approx_true v v_in_fV; simpl in *. - rewrite NatSet.diff_spec in v_in_fV. - rewrite NatSet.singleton_spec in v_in_fV; - destruct v_in_fV; subst. - destruct (absenv (Var Q n)); simpl in *. - case_eq (NatSet.mem n V); intros case_mem; - rewrite case_mem in approx_true; simpl in *. - + rewrite NatSet.mem_spec in case_mem. - contradiction. - + apply Is_true_eq_left in approx_true. - apply andb_prop_elim in approx_true. - destruct approx_true; auto. - - intros approx_true v0 v_in_fV; simpl in *. - inversion v_in_fV. - - intros approx_unary_true v v_in_fV; simpl in *. - apply Is_true_eq_left in approx_unary_true. - simpl in *. - destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. - apply andb_prop_elim in approx_unary_true. - destruct approx_unary_true. + induction f; cbn; intros approx_true var var_in_fV find_A; set_tac. + - subst. + rewrite find_A in *. + destruct (var mem dVars) eqn:?; set_tac; try congruence. + andb_to_prop approx_true; unfold isSupersetIntv. + apply andb_prop_intro; split; + apply Is_true_eq_left; auto. + - destruct (DaisyMap.find (Unop u f) A) as [[iv_u err_u] | ] eqn:?; + try congruence. + andb_to_prop approx_true. apply IHf; try auto. - apply Is_true_eq_true; auto. - - intros approx_bin_true v v_in_fV. - simpl in v_in_fV. - rewrite NatSet.diff_spec in v_in_fV. - destruct v_in_fV as [ v_in_fV v_not_in_V]. - rewrite NatSet.union_spec in v_in_fV. - apply Is_true_eq_left in approx_bin_true. - destruct (absenv (Binop b f1 f2)); destruct (absenv f1); - destruct (absenv f2); simpl in *. - apply andb_prop_elim in approx_bin_true. - destruct approx_bin_true. - apply andb_prop_elim in H. + set_tac. + - destruct (DaisyMap.find (Binop b f1 f2) A) as [[iv_b err_b] | ] eqn:?; + try congruence. + andb_to_prop approx_true. destruct H. - destruct v_in_fV. - + apply IHf1; try auto. - * apply Is_true_eq_true; auto. - * rewrite NatSet.diff_spec; split; auto. - + apply IHf2; try auto. - * apply Is_true_eq_true; auto. - * rewrite NatSet.diff_spec; split; auto. - - intros approx_rnd_true v v_in_fV. - simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f). - apply Is_true_eq_left in approx_rnd_true. - apply andb_prop_elim in approx_rnd_true. - destruct approx_rnd_true. - apply IHf; auto. - apply Is_true_eq_true in H; try auto. + + apply IHf1; try auto; set_tac. + + apply IHf2; try auto; set_tac. + - destruct (DaisyMap.find (Downcast m f) A) as [[iv_m err_m] | ] eqn:?; + try congruence. + andb_to_prop approx_true. + apply IHf; try auto; set_tac. Qed. Corollary Q2R_max4 a b c d: @@ -150,20 +139,20 @@ Proof. unfold IntervalArith.min4, min4; repeat rewrite Q2R_min; auto. Qed. -Ltac env_assert absenv e name := - assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto). +Ltac env_assert A e name := + assert (exists iv err, A e = (iv,err)) as name by (destruct (A e); repeat eexists; auto). -Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err: - absenv e2 = ((ivlo_e2,ivhi_e2), err) -> - validIntervalbounds (Binop Div e1 e2) absenv P V = true -> +Lemma validBoundsDiv_uneq_zero e1 e2 A P V ivlo_e2 ivhi_e2 err: + A e2 = ((ivlo_e2,ivhi_e2), err) -> + validIntervalbounds (Binop Div e1 e2) A P V = true -> (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. - intros absenv_eq validBounds. + intros A_eq validBounds. unfold validIntervalbounds in validBounds. - env_assert absenv (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]]. - env_assert absenv e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]]. - rewrite abs_div, abs_e1, absenv_eq in validBounds. + env_assert A (Binop Div e1 e2) abs_div; destruct abs_div as [iv_div [err_div abs_div]]. + env_assert A e1 abs_e1; destruct abs_e1 as [iv_e1 [err_e1 abs_e1]]. + rewrite abs_div, abs_e1, A_eq in validBounds. repeat (rewrite <- andb_lazy_alt in validBounds). apply Is_true_eq_left in validBounds. apply andb_prop_elim in validBounds. @@ -174,12 +163,12 @@ Proof. apply le_neq_bool_to_lt_prop; auto. Qed. -Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) +Theorem validIntervalbounds_sound (f:exp Q) (A:analysisResult) (P:precond) fVars dVars (E:env) Gamma: - validIntervalbounds f absenv P dVars = true -> + validIntervalbounds f A P dVars = true -> (forall v, NatSet.mem v dVars = true -> exists vR, E v = Some vR /\ - (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> + (Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) -> NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> (forall v, NatSet.mem v fVars = true -> exists vR, E v = Some vR /\ @@ -187,15 +176,15 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) (forall v, NatSet.mem v (NatSet.union fVars dVars) = true -> exists m :mType, Gamma v = Some m) -> exists vR, eval_exp E (toRMap Gamma) (toREval (toRExp f)) vR M0 /\ - (Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. + (Q2R (fst (fst (A f))) <= vR <= Q2R (snd (fst (A f))))%R. Proof. induction f; intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined; simpl in *. - - env_assert absenv (Var Q n) absenv_var. - destruct absenv_var as [iv_n [err_n absenv_var]]. + - env_assert A (Var Q n) A_var. + destruct A_var as [iv_n [err_n A_var]]. case_eq (NatSet.mem n dVars); intros dVars_case; - rewrite dVars_case, absenv_var in valid_bounds; simpl in *. + rewrite dVars_case, A_var in valid_bounds; simpl in *. + destruct (valid_definedVars n) as [vR [env_valid bounds_valid]]; try auto. eexists; split; simpl; try eauto. eapply Var_load; simpl; try auto. @@ -210,24 +199,24 @@ Proof. * andb_to_prop valid_bounds. unfold Qleb in *. canonize_hyps. - rewrite absenv_var. + rewrite A_var. simpl in *. lra. - exists (perturb (Q2R v) 0). split; [econstructor; eauto; apply Rabs_0_equiv | ]. - env_assert absenv (Const m v) absenv_const; - destruct absenv_const as [iv_v [err_v absenv_const]]. - rewrite absenv_const in *; simpl in *. + env_assert A (Const m v) A_const; + destruct A_const as [iv_v [err_v A_const]]. + rewrite A_const in *; simpl in *. andb_to_prop valid_bounds. canonize_hyps. simpl in *; unfold perturb; lra. - - env_assert absenv (Unop u f) absenv_unop; - destruct absenv_unop as [iv_u [err_u absenv_unop]]. - rewrite absenv_unop in *; simpl in *. - case_eq (validIntervalbounds f absenv P dVars); + - env_assert A (Unop u f) A_unop; + destruct A_unop as [iv_u [err_u A_unop]]. + rewrite A_unop in *; simpl in *. + case_eq (validIntervalbounds f A P dVars); intros case_bounds; rewrite case_bounds in *; try congruence. - env_assert absenv f absenv_f; - destruct absenv_f as [iv_f [ err_f absenv_f]]; rewrite absenv_f in *; simpl in *. + env_assert A f A_f; + destruct A_f as [iv_f [ err_f A_f]]; rewrite A_f in *; simpl in *. destruct IHf as [vF [eval_f valid_bounds_f]]; try auto. destruct u. + exists (evalUnop Neg vF); split; [econstructor; auto | ]. @@ -278,17 +267,17 @@ Proof. } rewrite <- Q2R0_is_0 in H3. apply Rlt_Qlt in H3. lra. } - - env_assert absenv (Binop b f1 f2) absenv_b; - destruct absenv_b as [iv_b [err_b absenv_b]]. - env_assert absenv f1 absenv_f1; - destruct absenv_f1 as [iv_f1 [err_f1 absenv_f1]]. - env_assert absenv f2 absenv_f2; - destruct absenv_f2 as [iv_f2 [err_f2 absenv_f2]]. - rewrite absenv_b in *; simpl in *. + - env_assert A (Binop b f1 f2) A_b; + destruct A_b as [iv_b [err_b A_b]]. + env_assert A f1 A_f1; + destruct A_f1 as [iv_f1 [err_f1 A_f1]]. + env_assert A f2 A_f2; + destruct A_f2 as [iv_f2 [err_f2 A_f2]]. + rewrite A_b in *; simpl in *. andb_to_prop valid_bounds. destruct IHf1 as [vF1 [eval_f1 valid_f1]]; try auto; set_tac. destruct IHf2 as [vF2 [eval_f2 valid_f2]]; try auto; set_tac. - rewrite absenv_f1, absenv_f2 in *; simpl in *. + rewrite A_f1, A_f2 in *; simpl in *. assert (M0 = join M0 M0) as M0_join by (cbv; auto); rewrite M0_join. exists (perturb (evalBinop b vF1 vF2) 0); @@ -356,11 +345,11 @@ Proof. unfold perturb. lra. } - - env_assert absenv (Downcast m f) absenv_d; - destruct absenv_d as [iv_d [err_d absenv_d]]; - env_assert absenv f absenv_f; - destruct absenv_f as [iv_f [err_f absenv_f]]; - rewrite absenv_d, absenv_f in *; simpl in *. + - env_assert A (Downcast m f) A_d; + destruct A_d as [iv_d [err_d A_d]]; + env_assert A f A_f; + destruct A_f as [iv_f [err_f A_f]]; + rewrite A_d, A_f in *; simpl in *. andb_to_prop valid_bounds. destruct IHf as [vF [eval_f valid_f]]; try auto. exists (perturb vF 0). @@ -428,32 +417,32 @@ Proof. eapply swap_Gamma_eval_exp; eauto. Qed. -Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult) Gamma: +Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult) Gamma: forall E fVars dVars outVars elo ehi err P, ssa f (NatSet.union fVars dVars) outVars -> (forall v, NatSet.mem v dVars = true -> exists vR, E v = Some vR /\ - (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> + (Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R) -> (forall v, NatSet.mem v fVars = true -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> (forall v, NatSet.mem v (NatSet.union fVars dVars) = true -> exists m :mType, Gamma v = Some m) -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> - validIntervalboundsCmd f absenv P dVars = true -> - absenv (getRetExp f) = ((elo, ehi), err) -> + validIntervalboundsCmd f A P dVars = true -> + A (getRetExp f) = ((elo, ehi), err) -> exists vR, bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR M0 /\ (Q2R elo <= vR <= Q2R ehi)%R. Proof. revert Gamma. induction f; - intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f absenv_f. + intros * ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f A_f. - inversion ssa_f; subst. unfold validIntervalboundsCmd in valid_bounds_f. andb_to_prop valid_bounds_f. inversion ssa_f; subst. - pose proof (validIntervalbounds_sound e absenv P E Gamma (fVars:=fVars) L) as validIV_e. + pose proof (validIntervalbounds_sound e A P E Gamma (fVars:=fVars) L) as validIV_e. destruct validIV_e as [v [eval_e valid_bounds_e]]; try auto. { simpl in usedVars_subset. hnf. intros a in_usedVars. @@ -536,8 +525,8 @@ Proof. eapply swap_Gamma_bstep with (Gamma1 := toRMap (updDefVars n M0 Gamma)) ; try eauto. intros n1; erewrite Rmap_updVars_comm; eauto. - unfold validIntervalboundsCmd in valid_bounds_f. - pose proof (validIntervalbounds_sound e absenv P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. + pose proof (validIntervalbounds_sound e A P E Gamma valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e. destruct valid_iv_e as [vR [eval_e valid_e]]; try auto. - simpl in *; rewrite absenv_f in *; simpl in *. + simpl in *; rewrite A_f in *; simpl in *. exists vR; split; [econstructor; eauto | auto]. Qed. \ No newline at end of file -- GitLab