(** Interval arithmetic checker and its soundness proof. The function validIntervalbounds checks wether the given analysis result is a valid range arithmetic for each sub term of the given expression e. The computation is done using our formalized interval arithmetic. The function is used in CertificateChecker.v to build the full checker. **) Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz. Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps. Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps. 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 | Const n => isSupersetIntv (n,n) intv | Unop o f => let rec := validIntervalbounds f absenv P validVars in let (iv, _) := absenv f in let opres := match o with | Neg => let new_iv := negateIntv iv in isSupersetIntv new_iv intv | Inv => let nodiv0 := orb (andb (Qleb (ivhi iv) 0) (negb (Qeq_bool (ivhi iv) 0))) (andb (Qleb 0 (ivlo iv)) (negb (Qeq_bool (ivlo iv) 0))) in let new_iv := invertIntv iv in andb (isSupersetIntv new_iv intv) nodiv0 end in andb rec opres | Binop op f1 f2 => let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in let (iv1,_) := absenv f1 in let (iv2,_) := absenv f2 in let opres := match op with | Plus => let new_iv := addIntv iv1 iv2 in isSupersetIntv new_iv intv | Sub => let new_iv := subtractIntv iv1 iv2 in isSupersetIntv new_iv intv | Mult => let new_iv := multIntv iv1 iv2 in isSupersetIntv new_iv intv | Div => let nodiv0 := orb (andb (Qleb (ivhi iv2) 0) (negb (Qeq_bool (ivhi iv2) 0))) (andb (Qleb 0 (ivlo iv2)) (negb (Qeq_bool (ivlo iv2) 0))) in let new_iv := divideIntv iv1 iv2 in andb (isSupersetIntv new_iv intv) nodiv0 end in andb rec opres end. Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:= match f with | Let x e g => 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))))) && validIntervalboundsCmd g absenv P (NatSet.add x validVars) |Ret e => validIntervalbounds e absenv 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.freeVars f) V) -> Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))). Proof. induction f; unfold validIntervalbounds. - 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; auto. - intros approx_true v0 v_in_fV; simpl in *. inversion v_in_fV. - intros approx_unary_true v v_in_fV. unfold freeVars in v_in_fV. apply Is_true_eq_left in approx_unary_true. destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. apply andb_prop_elim in approx_unary_true. destruct approx_unary_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. destruct H. destruct v_in_fV. + apply IHf1; auto. apply Is_true_eq_true; auto. rewrite NatSet.diff_spec; split; auto. + apply IHf2; auto. apply Is_true_eq_true; auto. rewrite NatSet.diff_spec; split; auto. Qed. Corollary Q2R_max4 a b c d: Q2R (IntervalArithQ.max4 a b c d) = max4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). Proof. unfold IntervalArithQ.max4, max4; repeat rewrite Q2R_max; auto. Qed. Corollary Q2R_min4 a b c d: Q2R (IntervalArithQ.min4 a b c d) = min4 (Q2R a) (Q2R b) (Q2R c) (Q2R d). 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). 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 -> (ivhi_e2 < 0) \/ (0 < ivlo_e2). Proof. intros absenv_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. apply Is_true_eq_left in validBounds. apply andb_prop_elim in validBounds. destruct validBounds as [_ validBounds]; apply andb_prop_elim in validBounds. destruct validBounds as [_ nodiv0]. apply Is_true_eq_true in nodiv0. apply le_neq_bool_to_lt_prop; auto. Qed. Fixpoint getRetExp (V:Type) (f:cmd V) := match f with |Let x e g => getRetExp g | Ret e => e end. Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V E: forall vR, validIntervalbounds f absenv P V = true -> (forall v, NatSet.mem v V = true -> exists vR, E v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> (forall v, NatSet.mem v (NatSet.diff (Expressions.freeVars f) V)= true -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> eval_exp 0%R E (toRExp f) vR -> (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. Proof. induction f; intros vR valid_bounds valid_definedVars valid_freeVars eval_f. - unfold validIntervalbounds in valid_bounds. env_assert absenv (Var Q n) absenv_var. destruct absenv_var as [ iv [err absenv_var]]. specialize (valid_freeVars n). rewrite absenv_var in *; simpl in *. inversion eval_f; subst. case_eq (NatSet.mem n V); intros case_mem; rewrite case_mem in *; simpl in *. + specialize (valid_definedVars n case_mem). destruct valid_definedVars as [vR' [E_n_eq precond_sound]]. rewrite E_n_eq in *. inversion H0; subst. rewrite absenv_var in *; auto. + repeat (rewrite delta_0_deterministic in *; try auto). unfold isSupersetIntv in valid_bounds. andb_to_prop valid_bounds. apply Qle_bool_iff in L; apply Qle_bool_iff in R. apply Qle_Rle in L; apply Qle_Rle in R. simpl in *. assert (NatSet.mem n (NatSet.diff (NatSet.singleton n) V) = true). * rewrite NatSet.mem_spec, NatSet.diff_spec, NatSet.singleton_spec. split; try auto. hnf; intros mem_V. rewrite <- NatSet.mem_spec in mem_V; rewrite mem_V in case_mem. inversion case_mem. * specialize (valid_freeVars H); destruct valid_freeVars as [vR' [vR_def P_valid]]. rewrite vR_def in H0; inversion H0; subst. lra. - unfold validIntervalbounds in valid_bounds. destruct (absenv (Const v)) as [intv err]; simpl. apply Is_true_eq_left in valid_bounds. apply andb_prop_elim in valid_bounds. destruct valid_bounds as [valid_lo valid_hi]. inversion eval_f; subst. rewrite delta_0_deterministic; auto. unfold contained; simpl. split. + apply Is_true_eq_true in valid_lo. unfold Qleb in *. apply Qle_bool_iff in valid_lo. apply Qle_Rle in valid_lo; auto. + apply Is_true_eq_true in valid_hi. unfold Qleb in *. apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_hi; auto. - case_eq (absenv (Unop u f)); intros intv err absenv_unop. destruct intv as [unop_lo unop_hi]; simpl. unfold validIntervalbounds in valid_bounds. rewrite absenv_unop in valid_bounds. case_eq (absenv f); intros intv_f err_f absenv_f. rewrite absenv_f in valid_bounds. apply Is_true_eq_left in valid_bounds. apply andb_prop_elim in valid_bounds. destruct valid_bounds as [valid_rec valid_unop]. apply Is_true_eq_true in valid_rec. inversion eval_f; subst. + specialize (IHf v1 valid_rec valid_definedVars valid_freeVars H2). rewrite absenv_f in IHf; simpl in IHf. (* TODO: Make lemma *) unfold isSupersetIntv in valid_unop. apply andb_prop_elim in valid_unop. destruct valid_unop as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. pose proof (interval_negation_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as negation_valid. unfold contained, negateInterval in negation_valid; simpl in *. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct IHf. split. * eapply Rle_trans. apply valid_lo. rewrite Q2R_opp; lra. * eapply Rle_trans. Focus 2. apply valid_hi. rewrite Q2R_opp; lra. + specialize (IHf v1 valid_rec valid_definedVars valid_freeVars H3). rewrite absenv_f in IHf; simpl in IHf. apply andb_prop_elim in valid_unop. destruct valid_unop as [valid_unop nodiv0]. (* TODO: Make lemma *) unfold isSupersetIntv in valid_unop. apply andb_prop_elim in valid_unop. destruct valid_unop as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. assert ((Q2R (ivhi intv_f) < 0)%R \/ (0 < Q2R (ivlo intv_f))%R) as nodiv0_prop. * apply Is_true_eq_true in nodiv0. apply le_neq_bool_to_lt_prop in nodiv0. destruct nodiv0. { left; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. } { right; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. } * pose proof (interval_inversion_valid (iv :=(Q2R (fst intv_f),(Q2R (snd intv_f)))) (a :=v1)) as inv_valid. unfold contained, invertInterval in inv_valid; simpl in *. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct IHf. rewrite delta_0_deterministic; auto. unfold perturb; split. { eapply Rle_trans. apply valid_lo. destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos]. (* TODO: Extract lemma maybe *) - assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra. assert (- (Q2R (snd intv_f)) <= - v1)%R as negation_flipped_hi by lra. apply Rinv_le_contravar in negation_flipped_hi; try auto. rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra. rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra. apply Ropp_le_contravar in negation_flipped_hi. repeat rewrite Ropp_involutive in negation_flipped_hi; rewrite Q2R_inv; auto. hnf; intros is_0. rewrite <- Q2R0_is_0 in nodiv0_neg. apply Rlt_Qlt in nodiv0_neg; lra. - rewrite Q2R_inv. apply Rinv_le_contravar; try lra. hnf; intros is_0. assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra. rewrite <- Q2R0_is_0 in nodiv0_pos. apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra. } { eapply Rle_trans. Focus 2. apply valid_hi. destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos]. - assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra. assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra. assert (- v1 <= - (Q2R (fst intv_f)))%R as negation_flipped_lo by lra. apply Rinv_le_contravar in negation_flipped_lo; try auto. rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra. rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra. apply Ropp_le_contravar in negation_flipped_lo. repeat rewrite Ropp_involutive in negation_flipped_lo; rewrite Q2R_inv; auto. hnf; intros is_0. rewrite <- Q2R0_is_0 in negation_pos. rewrite <- Q2R_opp in negation_pos. apply Rlt_Qlt in negation_pos; lra. assert (0 < - (Q2R (snd intv_f)))%R by lra. lra. - rewrite Q2R_inv. apply Rinv_le_contravar; try lra. hnf; intros is_0. assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra. rewrite <- Q2R0_is_0 in nodiv0_pos. apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra. } - inversion eval_f; subst. rewrite delta_0_deterministic in eval_f; auto. rewrite delta_0_deterministic; auto. simpl in valid_bounds. case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin. case_eq (absenv f1); intros iv1 err1 absenv_f1. case_eq (absenv f2); intros iv2 err2 absenv_f2. rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds. apply Is_true_eq_left in valid_bounds. apply andb_prop_elim in valid_bounds. destruct valid_bounds as [valid_rec valid_bin]. apply andb_prop_elim in valid_rec. destruct valid_rec as [valid_e1 valid_e2]. apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2. specialize (IHf1 v1 valid_e1 valid_definedVars); specialize (IHf2 v2 valid_e2 valid_definedVars). rewrite absenv_f1 in IHf1. rewrite absenv_f2 in IHf2. assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1. + apply IHf1; try auto. intros v in_diff_e1. apply valid_freeVars. rewrite NatSet.mem_spec, NatSet.diff_spec in *. simpl. destruct in_diff_e1; split; try auto. rewrite NatSet.union_spec; auto. + assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2. * apply IHf2; try auto. intros v in_diff_e2. apply valid_freeVars. rewrite NatSet.mem_spec, NatSet.diff_spec in *. simpl. destruct in_diff_e2; split; try auto. rewrite NatSet.union_spec; auto. * destruct b; simpl in *. { pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add. unfold validIntervalAdd in valid_add. specialize (valid_add v1 v2 valid_bounds_e1 valid_bounds_e2). unfold contained in valid_add. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_add as [valid_add_lo valid_add_hi]. split. - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold addIntv. simpl in valid_add_lo. repeat rewrite <- Q2R_plus in valid_add_lo. rewrite <- Q2R_min4 in valid_add_lo. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_add_hi. repeat rewrite <- Q2R_plus in valid_add_hi. rewrite <- Q2R_max4 in valid_add_hi. unfold absIvUpd; auto. } { pose proof (interval_subtraction_valid (iv1 := (Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_sub. specialize (valid_sub v1 v2 valid_bounds_e1 valid_bounds_e2). unfold contained in valid_sub. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_sub as [valid_sub_lo valid_sub_hi]. split. - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold subtractIntv. simpl in valid_sub_lo. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_lo. repeat rewrite <- Q2R_minus in valid_sub_lo. rewrite <- Q2R_min4 in valid_sub_lo. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_sub_hi. repeat rewrite <- Rsub_eq_Ropp_Rplus in valid_sub_hi. repeat rewrite <- Q2R_minus in valid_sub_hi. rewrite <- Q2R_max4 in valid_sub_hi. unfold absIvUpd; auto. } { pose proof (interval_multiplication_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2:=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_mul. specialize (valid_mul v1 v2 valid_bounds_e1 valid_bounds_e2). unfold contained in valid_mul. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. destruct valid_mul as [valid_mul_lo valid_mul_hi]. split. - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_mul_lo. repeat rewrite <- Q2R_mult in valid_mul_lo. rewrite <- Q2R_min4 in valid_mul_lo. unfold absIvUpd; auto. - eapply Rle_trans. Focus 2. apply valid_hi. unfold ivlo, addIntv. simpl in valid_mul_hi. repeat rewrite <- Q2R_mult in valid_mul_hi. rewrite <- Q2R_max4 in valid_mul_hi. unfold absIvUpd; auto. } { pose proof (interval_division_valid (a:=v1) (b:=v2) (iv1:=(Q2R (fst iv1), Q2R (snd iv1))) (iv2:=(Q2R (fst iv2),Q2R (snd iv2)))) as valid_div. unfold contained in valid_div. unfold isSupersetIntv in valid_bin. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0]. apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi]. apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi. apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi. apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi. apply orb_prop_elim in nodiv0. assert (snd iv2 < 0 \/ 0 < fst iv2). - destruct nodiv0 as [lt_0 | lt_0]; apply andb_prop_elim in lt_0; destruct lt_0 as [le_0 neq_0]; apply Is_true_eq_true in le_0; apply Is_true_eq_true in neq_0; apply negb_true_iff in neq_0; apply Qeq_bool_neq in neq_0; rewrite Qle_bool_iff in le_0; rewrite Qle_lteq in le_0; destruct le_0 as [lt_0 | eq_0]; [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto. - destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto. + rewrite <- Q2R0_is_0. destruct H; [left | right]; apply Qlt_Rlt; auto. + unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi. simpl in *. assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra. assert (~ snd iv2 == 0). * destruct H; try lra. hnf; intros ivhi2_0. apply Rle_Qle in H0. rewrite ivhi2_0 in H0. lra. * assert (~ fst iv2 == 0). { destruct H; try lra. hnf; intros ivlo2_0. apply Rle_Qle in H0. rewrite ivlo2_0 in H0. lra. } { split. - eapply Rle_trans. apply valid_lo. unfold ivlo. unfold multIntv. simpl in valid_div_lo. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. rewrite <- Q2R_inv in valid_div_lo; [ | auto]. repeat rewrite <- Q2R_mult in valid_div_lo. rewrite <- Q2R_min4 in valid_div_lo; auto. - eapply Rle_trans. Focus 2. apply valid_hi. simpl in valid_div_hi. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. rewrite <- Q2R_inv in valid_div_hi; [ | auto]. repeat rewrite <- Q2R_mult in valid_div_hi. rewrite <- Q2R_max4 in valid_div_hi; auto. } } Qed. Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): forall E vR fVars dVars outVars elo ehi err P, ssaPrg f (NatSet.union fVars dVars) outVars -> bstep (toRCmd f) E 0%R vR -> (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) -> (forall v, NatSet.mem v fVars = true -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> validIntervalboundsCmd f absenv P dVars = true -> absenv (getRetExp f) = ((elo, ehi), err) -> (Q2R elo <= vR <= Q2R ehi)%R. Proof. induction f; intros E envR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound fVars_valid valid_bounds_f absenv_f. - inversion ssa_f; subst. inversion eval_f; subst. unfold validIntervalboundsCmd in valid_bounds_f. andb_to_prop valid_bounds_f. eapply IHf; eauto. admit. intros v0 mem_v0. unfold updEnv. case_eq (v0 =? n); intros v0_eq. + rename L into eq_lo; rename R1 into eq_hi. apply Qeq_bool_iff in eq_lo; apply Qeq_eqR in eq_lo. apply Qeq_bool_iff in eq_hi; apply Qeq_eqR in eq_hi. rewrite Nat.eqb_eq in v0_eq. subst. rewrite <- eq_lo, <- eq_hi. exists v. split; auto. eapply validIntervalbounds_sound; eauto. admit. + apply dVars_sound. rewrite NatSet.mem_spec. rewrite NatSet.mem_spec in mem_v0. rewrite NatSet.add_spec in mem_v0. destruct mem_v0; try auto. rewrite Nat.eqb_neq in v0_eq. exfalso; apply v0_eq; auto. + admit. - unfold validIntervalboundsCmd in valid_bounds_f. inversion eval_f; subst. unfold updEnv. assert (Q2R (fst (fst (absenv e))) <= envR <= Q2R (snd (fst (absenv e))))%R. + eapply validIntervalbounds_sound; eauto. admit. + simpl in *. rewrite absenv_f in *; auto. Admitted.