IntervalValidation.v 22.5 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 Coq.micromega.Psatz.
9
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
10
11
Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps.
Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
12

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

Heiko Becker's avatar
Heiko Becker committed
15
16
Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
  match f with
Heiko Becker's avatar
Heiko Becker committed
17
  |Const n => []
18
19
  |Var _ v => []
  |Param _ v => [v]
Heiko Becker's avatar
Heiko Becker committed
20
21
  |Unop o f1 => freeVars V f1
  |Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
Heiko Becker's avatar
Heiko Becker committed
22
23
  end.

24
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
25
26
  let (intv, _) := absenv e in
    match e with
27
    | Var _ v => NatSet.mem v validVars
Heiko Becker's avatar
Heiko Becker committed
28
29
30
    | Param _ v => isSupersetIntv (P v) intv
    | Const n => isSupersetIntv (n,n) intv
    | Unop o f =>
31
    let rec := validIntervalbounds f absenv P validVars in
Heiko Becker's avatar
Heiko Becker committed
32
    let (iv, _) := absenv f in
33
    let opres :=
Heiko Becker's avatar
Heiko Becker committed
34
        match o with
35
        | Neg =>
Heiko Becker's avatar
Heiko Becker committed
36
          let new_iv := negateIntv iv in
37
38
39
          isSupersetIntv new_iv intv
        | Inv =>
          let nodiv0 := orb
Heiko Becker's avatar
Heiko Becker committed
40
41
42
                          (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
43
          andb (isSupersetIntv new_iv intv) nodiv0
Heiko Becker's avatar
Heiko Becker committed
44
45
        end
    in
46
    andb rec opres
Heiko Becker's avatar
Heiko Becker committed
47
    | Binop op f1 f2 =>
48
      let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in
Heiko Becker's avatar
Heiko Becker committed
49
50
      let (iv1,_) := absenv f1 in
      let (iv2,_) := absenv f2 in
51
      let opres :=
Heiko Becker's avatar
Heiko Becker committed
52
          match op with
53
54
55
56
57
58
59
60
61
          | 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
62
          | Div =>
63
64
65
            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
66
            let new_iv := divideIntv iv1 iv2 in
67
            andb (isSupersetIntv new_iv intv) nodiv0
68
69
70
71
72
          end
      in
      andb rec opres
    end.

73
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
  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 &&
                       (Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q 0)))) &&
                                 Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q 0)))))
  |Nop _ => false
  end.

Theorem ivbounds_approximatesPrecond_sound f absenv P V:
  validIntervalbounds f absenv P V = true ->
Heiko Becker's avatar
Heiko Becker committed
89
  forall v, In v (freeVars Q f) ->
90
91
       Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
Heiko Becker's avatar
Heiko Becker committed
92
  induction f; unfold validIntervalbounds.
93
94
95
96
  - intros approx_true v v_in_fV; simpl in *; contradiction.
  - intros approx_true v v_in_fV; simpl in *.
    destruct v_in_fV; try contradiction.
    subst.
Heiko Becker's avatar
Heiko Becker committed
97
    destruct (absenv (Param Q v)); simpl in *.
98
99
    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
100
101
102
103
104
105
106
107
  - 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.
108
109
110
111
  - 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
112
    destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
113
114
115
116
    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
117
118
    destruct v_in_fV as [v_in_fV_f1 | v_in_fV_f2].
    + apply IHf1; auto.
119
      apply Is_true_eq_true; auto.
Heiko Becker's avatar
Heiko Becker committed
120
    + apply IHf2; auto.
121
122
123
      apply Is_true_eq_true; auto.
Qed.

Heiko Becker's avatar
Heiko Becker committed
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
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).

139
Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
140
  absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
141
  validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
142
143
144
145
146
147
148
149
150
151
152
  (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].
153
154
  apply Is_true_eq_true in nodiv0.
  apply le_neq_bool_to_lt_prop; auto.
155
156
Qed.

157
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V VarEnv ParamEnv:
Heiko Becker's avatar
Heiko Becker committed
158
  forall vR,
159
160
161
    validIntervalbounds f absenv P V = true ->
    (forall v, NatSet.mem v V = true ->
          (Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
162
  eval_exp 0%R VarEnv ParamEnv P (toRExp f) vR ->
Heiko Becker's avatar
Heiko Becker committed
163
  (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
164
Proof.
165
166
167
168
169
170
171
172
173
  induction f; intros vR valid_bounds 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.
    apply valid_freeVars; auto.
  - pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P V valid_bounds) as env_approx_p.
174
    unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
175
176
    case_eq (absenv (Param Q n)).
    intros intv err absenv_n.
Heiko Becker's avatar
Heiko Becker committed
177
178
    rewrite absenv_n in valid_bounds.
    specialize (env_approx_p n).
Heiko Becker's avatar
Heiko Becker committed
179
    case_eq (P n); intros ivlo ivhi p_n.
180
    unfold isSupersetIntv, freeVars in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
181
182
    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
183
    rewrite p_n, absenv_n in env_approx_p.
184
    simpl in eval_f.
Heiko Becker's avatar
Heiko Becker committed
185
    inversion eval_f; subst.
186
    rewrite p_n in *;simpl in *.
187
    rewrite delta_0_deterministic; auto.
Heiko Becker's avatar
Heiko Becker committed
188
    destruct intv as [abslo abshi]; simpl in *.
189
    apply andb_prop_elim in env_approx_p.
Heiko Becker's avatar
Heiko Becker committed
190
    destruct env_approx_p as [abslo_le_ivlo ivhi_le_abshi].
191
    destruct H1.
192
193
194
    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
195
    apply Qle_Rle in abslo_le_ivlo; apply Qle_Rle in ivhi_le_abshi.
196
	rewrite delta_0_deterministic in *; auto.
197
    rewrite delta_0_deterministic in *; auto.
198
    split; lra.
199
  - unfold validIntervalbounds in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
200
    destruct (absenv (Const v)) as [intv err]; simpl.
201
202
    apply Is_true_eq_left in valid_bounds.
    apply andb_prop_elim in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
203
    destruct valid_bounds as [valid_lo valid_hi].
Heiko Becker's avatar
Heiko Becker committed
204
    inversion eval_f; subst.
205
    rewrite delta_0_deterministic; auto.
206
207
    unfold contained; simpl.
    split.
Heiko Becker's avatar
Heiko Becker committed
208
    + apply Is_true_eq_true in valid_lo.
209
      unfold Qleb in *.
Heiko Becker's avatar
Heiko Becker committed
210
211
212
213
214
215
      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.
216
  - case_eq (absenv (Unop u f)); intros intv err absenv_unop.
Heiko Becker's avatar
Heiko Becker committed
217
218
219
220
221
222
223
224
225
226
    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.
227
    + specialize (IHf v1 valid_rec valid_freeVars H2).
Heiko Becker's avatar
Heiko Becker committed
228
      rewrite absenv_f in IHf; simpl in IHf.
229
230
231
232
233
234
235
236
237
238
      (* 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 (Q2R (fst intv_f),(Q2R (snd intv_f))) 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.
239
      split.
240
241
242
243
244
      * eapply Rle_trans. apply valid_lo.
        rewrite Q2R_opp; lra.
      * eapply Rle_trans.
        Focus 2. apply valid_hi.
        rewrite Q2R_opp; lra.
245
    + specialize (IHf v1 valid_rec valid_freeVars H3).
Heiko Becker's avatar
Heiko Becker committed
246
      rewrite absenv_f in IHf; simpl in IHf.
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
      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 (Q2R (fst intv_f),(Q2R (snd intv_f))) 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.
265
         rewrite delta_0_deterministic; auto.
266
         unfold perturb; split.
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
         { 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.
         }
313
  - inversion eval_f; subst.
314
315
    rewrite delta_0_deterministic in eval_f; auto.
    rewrite delta_0_deterministic; auto.
Heiko Becker's avatar
Heiko Becker committed
316
    simpl in valid_bounds.
Heiko Becker's avatar
Heiko Becker committed
317
318
319
320
    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
321
322
323
324
325
326
    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.
327
328
    specialize (IHf1 v1 valid_e1 valid_freeVars H4);
      specialize (IHf2 v2 valid_e2 valid_freeVars H5).
Heiko Becker's avatar
Heiko Becker committed
329
330
    rewrite absenv_f1 in IHf1.
    rewrite absenv_f2 in IHf2.
331
    destruct b; simpl in *.
Heiko Becker's avatar
Heiko Becker committed
332
    + pose proof (interval_addition_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
333
      unfold validIntervalAdd in valid_add.
Heiko Becker's avatar
Heiko Becker committed
334
      specialize (valid_add v1 v2 IHf1 IHf2).
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
      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
357
    + pose proof (interval_subtraction_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
Heiko Becker's avatar
Heiko Becker committed
358
      specialize (valid_sub v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
      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
384
      specialize (valid_mul v1 v2 IHf1 IHf2).
Heiko Becker's avatar
Heiko Becker committed
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
      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
407
    + pose proof (interval_division_valid v1 v2 (Q2R (fst iv1), Q2R (snd iv1)) (Q2R (fst iv2),Q2R (snd iv2))) as valid_div.
408
409
      unfold contained in valid_div.
      unfold isSupersetIntv in valid_bin.
410
      apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_bin nodiv0].
411
412
413
414
      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.
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
      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. }
458
Qed.
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520

Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
  forall VarEnv ParamEnv envR inVars outVars elo ehi err P,
    ssaPrg Q f inVars outVars ->
    bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) envR  ->
    (forall v, NatSet.mem v inVars = true ->
          (Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
      validIntervalboundsCmd f absenv P inVars = true ->
    absenv (Var Q 0%nat) = ((elo,ehi),err) ->
    (Q2R elo <=  envR (0%nat) <= Q2R ehi)%R.
Proof.
  induction f;
    intros VarEnv ParamEnv envR inVars outVars elo ehi err P
           ssa_f eval_f freeVars_def 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.
    intros v0 mem_v0.
    unfold updEnv.
    case_eq (v0 =? n); intros v0_eq.
    + assert (Q2R (fst (fst (absenv e))) <= v <= Q2R (snd (fst (absenv e))))%R
        by (eapply validIntervalbounds_sound; eauto).
      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.
      assumption.
    + apply freeVars_def. rewrite NatSet.mem_spec.
      rewrite NatSet.mem_spec in mem_v0.
      rewrite NatSet.add_spec in mem_v0.
      destruct mem_v0.
      * rewrite Nat.eqb_neq in v0_eq.
        exfalso; apply v0_eq; auto.
      * assumption.
  - unfold validIntervalboundsCmd in valid_bounds_f.
    andb_to_prop valid_bounds_f.
    inversion eval_f; subst.
    unfold updEnv.
    assert (0 =? 0 = true) as refl0 by (apply Nat.eqb_refl).
    rewrite refl0.
    assert (Q2R (fst (fst (absenv e))) <= v <= Q2R (snd (fst (absenv e))))%R
      by (eapply validIntervalbounds_sound; eauto).
    rename L0 into eq_lo;
      rename R0 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.
    subst.
    rewrite absenv_f in *; simpl in *.
    rewrite <- eq_lo, <- eq_hi.
    assumption.
  - unfold validIntervalboundsCmd in valid_bounds_f.
    inversion valid_bounds_f.
Qed.