IntervalValidation.v 11.7 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
Import Lists.List.ListNotations.

Heiko Becker's avatar
Heiko Becker committed
14 15
Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
  match f with
Heiko Becker's avatar
Heiko Becker committed
16
  |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
  |Unop o f1 => freeVars V f1
  |Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
Heiko Becker's avatar
Heiko Becker committed
21 22
  end.

Heiko Becker's avatar
Heiko Becker committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54
Fixpoint validIntervalbounds (f:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv f in
  match f with
  | Var _ v => false
  | Param _ v =>
    isSupersetIntv (P v) intv
  | Const n =>
    isSupersetIntv (n,n) intv
  | Unop o f1 =>
    let rec := validIntervalbounds f1 absenv P in
    let (iv1, _) := absenv f1 in
    let new_iv :=
        match o with
        | Neg => negateIntv iv1
        | Inv => invertIntv iv1
        end
    in
    andb rec (isSupersetIntv new_iv intv)
  | Binop o f1 f2 =>
    let rec := andb (validIntervalbounds f1 absenv P) (validIntervalbounds f2 absenv P) in
    let (iv1,_) := absenv f1 in
    let (iv2,_) := absenv f2 in
    let new_iv :=
        match o with
        | Plus => addIntv iv1 iv2
        | Sub => subtractIntv iv1 iv2
        | Mult => multIntv iv1 iv2
        | Div => divideIntv iv1 iv2
        end
    in
    andb rec (isSupersetIntv new_iv intv)
  end.
55

Heiko Becker's avatar
Heiko Becker committed
56 57 58
Theorem ivbounds_approximatesPrecond_sound f absenv P:
  validIntervalbounds f absenv P = true ->
  forall v, In v (freeVars Q f) ->
59 60
       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
Heiko Becker's avatar
Heiko Becker committed
61
  induction f; unfold validIntervalbounds.
62 63 64 65 66 67 68 69 70
  - 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.
Heiko Becker's avatar
Heiko Becker committed
71 72 73 74 75 76 77 78
  - 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.
79 80 81 82
  - 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.
Heiko Becker's avatar
Heiko Becker committed
83
    destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
84 85 86 87
    apply andb_prop_elim in approx_bin_true.
    destruct approx_bin_true.
    apply andb_prop_elim in H.
    destruct H.
Heiko Becker's avatar
Heiko Becker committed
88 89
    destruct v_in_fV as [v_in_fV_f1 | v_in_fV_f2].
    + apply IHf1; auto.
90
      apply Is_true_eq_true; auto.
Heiko Becker's avatar
Heiko Becker committed
91
    + apply IHf2; auto.
92 93 94
      apply Is_true_eq_true; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
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).

Heiko Becker's avatar
Heiko Becker committed
110 111 112 113 114 115
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
  forall vR,
  precondValidForExec P cenv ->
  validIntervalbounds f absenv P = true ->
  eval_exp 0%R cenv (toRExp f) vR ->
  (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
116
Proof.
Heiko Becker's avatar
Heiko Becker committed
117 118
  induction f.
  - intros vR precond_valid valid_bounds eval_f.
119
    pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
120
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
121
    destruct (absenv (Var Q n)); inversion valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
122
  - intros vR precond_valid valid_bounds eval_f.
123
    pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
124
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
125 126
    case_eq (absenv (Param Q n)).
    intros intv err absenv_n.
Heiko Becker's avatar
Heiko Becker committed
127 128 129
    rewrite absenv_n in valid_bounds.
    unfold precondValidForExec in precond_valid.
    specialize (env_approx_p n).
Heiko Becker's avatar
Heiko Becker committed
130
    case_eq (P n); intros ivlo ivhi p_n.
131
    unfold isSupersetIntv, freeVars in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
132 133
    assert (In n (n::nil)) as n_in_n by (unfold In; auto).
    specialize (env_approx_p n_in_n).
Heiko Becker's avatar
Heiko Becker committed
134 135
    rewrite p_n, absenv_n in env_approx_p.
    specialize (precond_valid n); rewrite p_n in precond_valid.
Heiko Becker's avatar
Heiko Becker committed
136
    inversion eval_f; subst.
Heiko Becker's avatar
Heiko Becker committed
137 138
    rewrite perturb_0_val; auto.
    destruct intv as [abslo abshi]; simpl in *.
139
    apply andb_prop_elim in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
140 141
    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
    destruct precond_valid as [ivlo_le_env env_le_ivhi].
142 143 144
    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
145 146 147 148 149 150 151 152
    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.
Heiko Becker's avatar
Heiko Becker committed
153
  - intros vR valid_precond valid_bounds eval_f.
154
    pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
155
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
156
    destruct (absenv (Const v)) as [intv err]; simpl.
157 158
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
159
    destruct valid_bounds as [valid_lo valid_hi].
Heiko Becker's avatar
Heiko Becker committed
160
    inversion eval_f; subst.
Heiko Becker's avatar
Heiko Becker committed
161
    rewrite perturb_0_val; auto.
162 163
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
164
    + apply Is_true_eq_true in valid_lo.
165
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
166 167 168 169 170 171
      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.
Heiko Becker's avatar
Heiko Becker committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
  - intros vR valid_precond valid_bounds eval_f;
      pose proof (ivbounds_approximatesPrecond_sound (Unop u f) absenv P valid_bounds) as env_approx_p.
    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_precond valid_rec H2).
      rewrite absenv_f in IHf; simpl in IHf.
  (** By monotonicity of negation **)
      admit.
    + specialize (IHf v1 valid_precond valid_rec H3).
      rewrite absenv_f in IHf; simpl in IHf.
  (* By monotonicity of inversion of IV *)
      admit.
  - intros vR valid_precond valid_bounds eval_f; inversion eval_f; subst.
    pose proof (ivbounds_approximatesPrecond_sound (Binop b f1 f2) absenv P valid_bounds) as env_approx_p.
    rewrite perturb_0_val in eval_f; auto.
Heiko Becker's avatar
Heiko Becker committed
196 197
    rewrite perturb_0_val; auto.
    simpl in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
198 199 200 201
    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.
Heiko Becker's avatar
Heiko Becker committed
202 203 204 205 206 207
    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.
Heiko Becker's avatar
Heiko Becker committed
208 209 210 211
    specialize (IHf1 v1 valid_precond valid_e1 H4);
      specialize (IHf2 v2 valid_precond valid_e2 H5).
    rewrite absenv_f1 in IHf1.
    rewrite absenv_f2 in IHf2.
212 213 214
    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.
Heiko Becker's avatar
Heiko Becker committed
215
      specialize (valid_add v1 v2 IHf1 IHf2).
216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
      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
238
    + pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
Heiko Becker's avatar
Heiko Becker committed
239
      specialize (valid_sub v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
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
      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.
Heiko Becker's avatar
Heiko Becker committed
265
      specialize (valid_mul v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287
      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.
Heiko Becker's avatar
Heiko Becker committed
288 289
    +  admit.
Admitted.