IntervalValidation.v 14.3 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
2
(**
Interval arithmetic checker and its soundness proof
3
Explained in section 4 of the paper, used in CertificateChecker.v to build full checker,
Heiko Becker's avatar
Heiko Becker committed
4
**)
5
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
6
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Heiko Becker's avatar
Heiko Becker committed
7
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
8

Heiko Becker's avatar
Heiko Becker committed
9
10
11
12
13
Import Lists.List.ListNotations.

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

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

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
82
83
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
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).

99
100
101
102
103
104
105
106
107
108
109
110
111
112
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P ivlo_e2 ivhi_e2 err:
  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
  validIntervalbounds (Binop Div e1 e2) absenv P = 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].
113
114
  apply Is_true_eq_true in nodiv0.
  apply le_neq_bool_to_lt_prop; auto.
115
116
Qed.

117
Theorem validIntervalbounds_sound (e:exp Q):
118
  forall (absenv:analysisResult) (P:precond) cenv vR,
Heiko Becker's avatar
Heiko Becker committed
119
120
121
122
    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.
123
124
Proof.
  induction e.
125
126
  - 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.
127
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
128
    destruct (absenv (Var Q n)); inversion valid_bounds.
129
130
  - 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.
131
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
132
133
134
135
136
137
138
139
140
141
    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]].
142
143
144
    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
145
146
147
148
149
150
    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 *.
151
    apply andb_prop_elim in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
152
153
    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
    destruct precond_valid as [ivlo_le_env env_le_ivhi].
154
155
156
    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
157
158
159
160
161
162
163
164
    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.
165
166
  - 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.
167
168
169
170
171
    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
172
173
174
    destruct valid_bounds as [valid_lo valid_hi].
    inversion eval_e; subst.
    rewrite perturb_0_val; auto.
175
176
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
177
    + apply Is_true_eq_true in valid_lo.
178
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
179
180
181
182
183
184
      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.
185
186
187
  - 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
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
    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.
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
    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
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
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
    + 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.
283
284
285
    + pose proof (divisionIsValid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.
      unfold contained in valid_div.
      unfold isSupersetIntv in valid_bin.
286
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0].
287
288
289
290
      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.
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
      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.