IntervalValidation.v 10.9 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3 4 5 6
    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.
Heiko Becker's avatar
Heiko Becker committed
7
**)
8
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List.
9
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Heiko Becker's avatar
Heiko Becker committed
10
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
11

Heiko Becker's avatar
Heiko Becker committed
12 13 14 15 16
Import Lists.List.ListNotations.

Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
  match e with
  |Const n => []
Heiko Becker's avatar
Heiko Becker committed
17 18
  |Var _ v => []
  |Param _ v => [v]
Heiko Becker's avatar
Heiko Becker committed
19 20 21
  |Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
  end.

22 23 24
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv e in
    match e with
Heiko Becker's avatar
Heiko Becker committed
25 26
    | Var _ v => false
    | Param _ v =>
27
      isSupersetIntv (P v) intv
28
    | Const n =>
29
      isSupersetIntv (n,n) intv
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
    | Binop b e1 e2 =>
      let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
      let (iv1,_) := absenv e1 in
      let (iv2,_) := absenv e2 in
      let opres :=
          match b 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 => false
          end
      in
      andb rec opres
    end.

51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
Theorem ivbounds_approximatesPrecond_sound e absenv P:
  validIntervalbounds e absenv P = true ->
  forall v, In v (freeVars Q e) ->
       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
  induction e; unfold validIntervalbounds.
  - intros approx_true v v_in_fV; simpl in *; contradiction.
  - intros approx_true v v_in_fV; simpl in *.
    unfold isSupersetIntv.
    destruct v_in_fV; try contradiction.
    subst.
    destruct (P v); destruct (absenv (Param Q v)); simpl in *.
    destruct i; simpl in *.
    apply Is_true_eq_left in approx_true; auto.
  - intros approx_true v0 v_in_fV; simpl in *; contradiction.
  - intros approx_bin_true v v_in_fV.
    unfold freeVars in v_in_fV.
    apply in_app_or in v_in_fV.
    apply Is_true_eq_left in approx_bin_true.
    destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); 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 as [v_in_fV_e1 | v_in_fV_e2].
    + apply IHe1; auto.
      apply Is_true_eq_true; auto.
    + apply IHe2; auto.
      apply Is_true_eq_true; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97

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).

98
Theorem validIntervalbounds_sound (e:exp Q):
99
  forall (absenv:analysisResult) (P:precond) cenv vR,
Heiko Becker's avatar
Heiko Becker committed
100 101 102 103
    precondValidForExec P cenv ->
    validIntervalbounds e absenv P = true ->
    eval_exp 0%R cenv (toRExp e) vR ->
    (Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
104 105
Proof.
  induction e.
106 107
  - intros absenv P cenv vR precond_valid valid_bounds eval_e.
    pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
108
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
109
    destruct (absenv (Var Q n)); inversion valid_bounds.
110 111
  - intros absenv P cenv vR precond_valid valid_bounds eval_e.
    pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
112
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
113 114 115 116 117 118 119 120 121 122
    assert (exists intv err, absenv (Param Q n) = (intv,err))
      as absenv_n
        by (destruct (absenv (Param Q n)); repeat eexists; auto).
    destruct absenv_n as [intv [err absenv_n]].
    rewrite absenv_n in valid_bounds.
    unfold precondValidForExec in precond_valid.
    specialize (env_approx_p n).
    assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n
        by (destruct (P n); repeat eexists; auto).
    destruct p_n as [ivlo [ivhi p_n]].
123 124 125
    unfold isSupersetIntv, freeVars in env_approx_p.
    assert (In n (n::nil)) by (unfold In; auto).
    specialize (env_approx_p H).
Heiko Becker's avatar
Heiko Becker committed
126 127 128 129 130 131
    rewrite p_n, absenv_n in env_approx_p.
    specialize (precond_valid n); rewrite p_n in precond_valid.
    inversion eval_e; subst.
    rewrite absenv_n; simpl.
    rewrite perturb_0_val; auto.
    destruct intv as [abslo abshi]; simpl in *.
132
    apply andb_prop_elim in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
133 134
    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
    destruct precond_valid as [ivlo_le_env env_le_ivhi].
135 136 137
    apply Is_true_eq_true in abslo_le_ivlo; apply Is_true_eq_true in ivhi_le_abshi.
    unfold Qleb in abslo_le_ivlo, ivhi_le_abshi.
    apply Qle_bool_iff in abslo_le_ivlo; apply Qle_bool_iff in ivhi_le_abshi.
Heiko Becker's avatar
Heiko Becker committed
138 139 140 141 142 143 144 145
    apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
    split.
    + eapply Rle_trans.
      apply abslo_le_ivlo.
      apply ivlo_le_env.
    + eapply Rle_trans.
      apply env_le_ivhi.
      apply ivhi_le_abshi.
146 147
  - intros absenv P cenv vR valid_precond valid_bounds eval_e.
    pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
148 149 150 151 152
    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.
Heiko Becker's avatar
Heiko Becker committed
153 154 155
    destruct valid_bounds as [valid_lo valid_hi].
    inversion eval_e; subst.
    rewrite perturb_0_val; auto.
156 157
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
158
    + apply Is_true_eq_true in valid_lo.
159
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
160 161 162 163 164 165
      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.
166 167 168
  - intros absenv P cenv vR valid_precond valid_bounds eval_e;
      inversion eval_e; subst.
    pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_bounds) as env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
    rewrite perturb_0_val in eval_e; auto.
    rewrite perturb_0_val; auto.
    simpl in valid_bounds.
    env_assert absenv (Binop b e1 e2) absenv_bin.
    env_assert absenv e1 absenv_e1.
    env_assert absenv e2 absenv_e2.
    destruct absenv_bin as [iv [err absenv_bin]]; rewrite absenv_bin in valid_bounds; rewrite absenv_bin.
    destruct absenv_e1 as [iv1 [err1 absenv_e1]]; rewrite absenv_e1 in valid_bounds.
    destruct absenv_e2 as [iv2 [err2 absenv_e2]]; rewrite absenv_e2 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.
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
    specialize (IHe1 absenv P cenv v1 valid_precond valid_e1 H4);
      specialize (IHe2 absenv P cenv v2 valid_precond valid_e2 H5).
    rewrite absenv_e1 in IHe1.
    rewrite absenv_e2 in IHe2.
    destruct b; simpl in *.
    + pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
      unfold validIntervalAdd in valid_add.
      specialize (valid_add v1 v2 IHe1 IHe2).
      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. }
Heiko Becker's avatar
Heiko Becker committed
214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
    + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
      specialize (valid_sub v1 v2 IHe1 IHe2).
      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 (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
      specialize (valid_mul v1 v2 IHe1 IHe2).
      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.
    + contradiction.
Qed.