Expressions.v 14.6 KB
Newer Older
1
(**
2
  Formalization of the base expression language for the daisy framework
3
 **)
4 5 6 7 8 9
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith
               Coq.QArith.Qreals.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps
               Daisy.Infra.Ltacs.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet
        Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
10

11 12 13 14 15
(**
  Expressions will use binary operators.
  Define them first
**)
Inductive binop : Type := Plus | Sub | Mult | Div.
16

17
Definition binopEq (b1:binop) (b2:binop) :=
='s avatar
= committed
18 19 20 21 22 23
  match b1, b2 with
  | Plus, Plus => true
  | Sub,  Sub  => true
  | Mult, Mult => true
  | Div,  Div  => true
  | _,_ => false
24 25
  end.

26 27 28 29
(**
  Next define an evaluation function for binary operators on reals.
  Errors are added on the expression evaluation level later.
 **)
30
Definition evalBinop (o:binop) (v1:R) (v2:R) :=
31 32 33 34 35 36
  match o with
  | Plus => Rplus v1 v2
  | Sub => Rminus v1 v2
  | Mult => Rmult v1 v2
  | Div => Rdiv v1 v2
  end.
37

38 39
Lemma binopEq_refl b:
  binopEq b b = true.
40 41 42 43
Proof.
  case b; auto.
Qed.

44 45
Lemma binopEq_compat_eq b1 b2:
  binopEq b1 b2 = true <-> b1 = b2.
46
Proof.
47 48 49 50 51 52 53 54 55 56
  split; case b1; case b2; intros; simpl in *; congruence.
Qed.

Lemma binopEq_compat_eq_false b1 b2:
  binopEq b1 b2 = false <-> ~ (b1 = b2).
Proof.
  split; intros neq.
  - hnf; intros; subst. rewrite binopEq_refl in neq.
    congruence.
  - destruct b1; destruct b2; cbv; congruence.
57 58
Qed.

59 60 61 62 63 64
(**
   Expressions will use unary operators.
   Define them first
 **)
Inductive unop: Type := Neg | Inv.

65
Definition unopEq (o1:unop) (o2:unop) :=
='s avatar
= committed
66 67 68 69
  match o1, o2 with
  | Neg, Neg => true
  | Inv, Inv => true
  | _ , _ => false
70 71
  end.

72 73
Lemma unopEq_refl b:
  unopEq b b = true.
74 75 76 77
Proof.
  case b; auto.
Qed.

78 79
Lemma unopEq_compat_eq b1 b2:
  unopEq b1 b2 = true <-> b1 = b2.
80
Proof.
81
  split; case b1; case b2; intros; simpl in *; congruence.
82 83
Qed.

84 85
(**
   Define evaluation for unary operators on reals.
86
   Errors are added in the expression evaluation level later.
87
 **)
88
Definition evalUnop (o:unop) (v:R):=
89 90 91 92 93
  match o with
  |Neg => (- v)%R
  |Inv => (/ v)%R
  end .

Nikita Zyuzin's avatar
Nikita Zyuzin committed
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
(**
  Expressions will use ternary operators
  Define them first
**)
Inductive terop: Type := Fma.

Definition teropEq (o1: terop) (o2: terop) :=
  match o1, o2 with
  | Fma, Fma => true
  end.

Lemma teropEq_refl b:
  teropEq b b = true.
Proof.
  now destruct b.
Qed.

Lemma teropEq_compat_eq b1 b2:
  teropEq b1 b2 = true <-> b1 = b2.
Proof.
  now destruct b1, b2.
Qed.

Lemma teropEq_compat_eq_false b1 b2:
  teropEq b1 b2 = false <-> ~ (b1 = b2).
Proof.
  now destruct b1, b2.
Qed.

Definition evalTerop (o: terop) (v1: R) (v2: R) (v3: R) :=
  match o with
  | Fma => Rplus v1 (Rmult v2 v3)
  end.

128
(**
129 130
  Define expressions parametric over some value type V.
  Will ease reasoning about different instantiations later.
131
**)
132 133
Inductive exp (V:Type): Type :=
  Var: nat -> exp V
134
| Const: mType -> V -> exp V
135
| Unop: unop -> exp V -> exp V
136
| Binop: binop -> exp V -> exp V -> exp V
Nikita Zyuzin's avatar
Nikita Zyuzin committed
137
| Terop: terop -> exp V -> exp V -> exp V -> exp V
138
| Downcast: mType -> exp V -> exp V.
139

140 141 142 143
(**
  Boolean equality function on expressions.
  Used in certificates to define the analysis result as function
**)
144
Fixpoint expEq (e1:exp Q) (e2:exp Q) :=
='s avatar
= committed
145
  match e1, e2 with
146
  | Var _ v1, Var _ v2 => (v1 =? v2)
147 148 149 150 151 152
  | Const m1 n1, Const m2 n2 =>
    (mTypeEq m1 m2) && (Qeq_bool n1 n2)
  | Unop o1 e11, Unop o2 e22 =>
    (unopEq o1 o2) && (expEq e11 e22)
  | Binop o1 e11 e12, Binop o2 e21 e22 =>
    (binopEq o1 o2) && (expEq e11 e21) && (expEq e12 e22)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
153 154
  | Terop o1 e11 e12 e13, Terop o2 e21 e22 e23 =>
    (teropEq o1 o2) && (expEq e11 e21) && (expEq e12 e22) && (expEq e13 e23)
155 156
  | Downcast m1 f1, Downcast m2 f2 =>
    (mTypeEq m1 m2) && (expEq f1 f2)
='s avatar
= committed
157
  | _, _ => false
158 159
  end.

160 161
Lemma expEq_refl e:
  expEq e e = true.
162
Proof.
163
  induction e; try (apply andb_true_iff; split); simpl in *; auto .
164
  - symmetry; apply beq_nat_refl.
165
  - apply mTypeEq_refl.
166 167 168
  - apply Qeq_bool_iff; lra.
  - case u; auto.
  - case b; auto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
169
  - case t. firstorder.
170
  - apply mTypeEq_refl.
171
Qed.
172

173 174
Lemma expEq_sym e e':
  expEq e e' = expEq e' e.
175 176 177
Proof.
  revert e'.
  induction e; intros e'; destruct e'; simpl; try auto.
178
  - apply Nat.eqb_sym.
179
  - f_equal.
180
    + apply mTypeEq_sym; auto.
181 182 183 184
    + apply Qeq_bool_sym.
  - f_equal.
    + destruct u; auto.
    + apply IHe.
='s avatar
= committed
185
  - f_equal.
186
    + f_equal.
187
      * destruct b; auto.
188
      * apply IHe1.
189
    + apply IHe2.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
190 191 192 193 194
  - f_equal.
    + f_equal.
      * destruct t, t0. simpl. apply IHe1.
      * apply IHe2.
    + apply IHe3.
195
  - f_equal.
196
    + apply mTypeEq_sym; auto.
197 198 199
    + apply IHe.
Qed.

200 201 202 203
Lemma expEq_trans e f g:
  expEq e f = true ->
  expEq f g = true ->
  expEq e g = true.
='s avatar
= committed
204
Proof.
205
  revert e f g; induction e;
206 207 208 209 210 211
    destruct f; intros g eq1 eq2;
      destruct g; simpl in *; try congruence;
        try rewrite Nat.eqb_eq in *;
        subst; try auto.
  - andb_to_prop eq1;
      andb_to_prop eq2.
212 213
    rewrite mTypeEq_compat_eq in L, L0; subst.
    rewrite mTypeEq_refl; simpl.
214 215 216
    rewrite Qeq_bool_iff in *; lra.
  - andb_to_prop eq1;
      andb_to_prop eq2.
217 218
    rewrite unopEq_compat_eq in *; subst.
    rewrite unopEq_refl; simpl.
='s avatar
= committed
219
    eapply IHe; eauto.
220 221
  - andb_to_prop eq1;
      andb_to_prop eq2.
222 223
    rewrite binopEq_compat_eq in *; subst.
    rewrite binopEq_refl; simpl.
224 225
    apply andb_true_iff.
    split; [eapply IHe1; eauto | eapply IHe2; eauto].
Nikita Zyuzin's avatar
Nikita Zyuzin committed
226 227 228 229 230 231
  - andb_to_prop eq1;
      andb_to_prop eq2.
    rewrite teropEq_compat_eq in *; subst.
    rewrite teropEq_refl; simpl.
    rewrite andb_true_iff.
    rewrite andb_true_iff.
232
    split; [split; [eapply IHe1; eauto | eapply IHe2; eauto] | eapply IHe3; eauto].
233 234
  - andb_to_prop eq1;
      andb_to_prop eq2.
235 236
    rewrite mTypeEq_compat_eq in *; subst.
    rewrite mTypeEq_refl; simpl.
='s avatar
= committed
237 238 239
    eapply IHe; eauto.
Qed.

240 241
Fixpoint toRExp (e:exp Q) :=
  match e with
Nikita Zyuzin's avatar
Nikita Zyuzin committed
242 243 244 245 246 247
  | Var _ v => Var R v
  | Const m n => Const m (Q2R n)
  | Unop o e1 => Unop o (toRExp e1)
  | Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
  | Terop o e1 e2 e3 => Terop o (toRExp e1) (toRExp e2) (toRExp e3)
  | Downcast m e1 => Downcast m (toRExp e1)
248
  end.
249

250 251
Fixpoint toREval (e:exp R) :=
  match e with
252
  | Var _ v => Var R v
253
  | Const _ n => Const M0 n
254 255
  | Unop o e1 => Unop o (toREval e1)
  | Binop o e1 e2 => Binop o (toREval e1) (toREval e2)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
256
  | Terop o e1 e2 e3 => Terop o (toREval e1) (toREval e2) (toREval e3)
257
  | Downcast _ e1 =>   Downcast M0 (toREval e1)
258
  end.
259

260
Definition toRMap (d:nat -> option mType) (n:nat) :=
='s avatar
= committed
261 262 263
  match d n with
  | Some m => Some M0
  | None => None
264
  end.
265

266 267
Arguments toRMap _ _/.

268 269 270 271
(**
  Define a perturbation function to ease writing of basic definitions
**)
Definition perturb (r:R) (e:R) :=
272
  (r * (1 + e))%R.
Heiko Becker's avatar
Heiko Becker committed
273

274 275
Hint Unfold perturb.

276
(**
277
Define expression evaluation relation parametric by an "error" epsilon.
278 279 280
The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
281
**)
282
Inductive eval_exp (E:env) (Gamma: nat -> option mType) :(exp R) -> R -> mType -> Prop :=
283
| Var_load m x v:
284
    Gamma x = Some m ->
285
    E x = Some v ->
286
    eval_exp E Gamma (Var R x) v m
287
| Const_dist m n delta:
288 289
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma (Const m n) (perturb n delta) m
290
| Unop_neg m f1 v1:
291 292
    eval_exp E Gamma f1 v1 m ->
    eval_exp E Gamma (Unop Neg f1) (evalUnop Neg v1) m
293
| Unop_inv m f1 v1 delta:
294 295 296 297
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma  f1 v1 m ->
    (~ v1 = 0)%R  ->
    eval_exp E Gamma (Unop Inv f1) (perturb (evalUnop Inv v1) delta) m
298
| Downcast_dist m m1 f1 v1 delta:
299
    (* Downcast expression f1 (evaluating to machine type m1), to a machine type m, less precise than m1.*)
300
    isMorePrecise m1 m = true ->
301 302 303
    Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
    eval_exp E Gamma f1 v1 m1 ->
    eval_exp E Gamma (Downcast m f1) (perturb v1 delta) m
304
| Binop_dist m1 m2 op f1 f2 v1 v2 delta:
305 306 307
    Rle (Rabs delta) (Q2R (mTypeToQ (join m1 m2))) ->
    eval_exp E Gamma f1 v1 m1 ->
    eval_exp E Gamma f2 v2 m2 ->
308
    ((op = Div) -> (~ v2 = 0)%R) ->
309 310 311 312 313
    eval_exp E Gamma (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta)  (join m1 m2).

Hint Constructors eval_exp.

(**
314
  Show some simpler (more general) rule lemmata
315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
**)
Lemma Const_dist' m n delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  v = perturb n delta ->
  m' = m ->
  eval_exp E Gamma (Const m n) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Const_dist'.

Lemma Unop_neg' m f1 v1 v m' E Gamma:
  eval_exp E Gamma f1 v1 m ->
  v = evalUnop Neg v1 ->
  m' = m ->
331
  eval_exp E Gamma (Unop Neg f1) v m'.
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_neg'.

Lemma Unop_inv' m f1 v1 delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  eval_exp E Gamma  f1 v1 m ->
  (~ v1 = 0)%R  ->
  v = perturb (evalUnop Inv v1) delta ->
  m' = m ->
  eval_exp E Gamma (Unop Inv f1) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Unop_inv'.

Lemma Downcast_dist' m m1 f1 v1 delta v m' E Gamma:
  isMorePrecise m1 m = true ->
  Rle (Rabs delta) (Q2R (mTypeToQ m)) ->
  eval_exp E Gamma f1 v1 m1 ->
  v = (perturb v1 delta) ->
  m' = m ->
  eval_exp E Gamma (Downcast m f1) v m'.
Proof.
  intros; subst; eauto.
Qed.

Hint Resolve Downcast_dist'.

Lemma Binop_dist' m1 m2 op f1 f2 v1 v2 delta v m' E Gamma:
  Rle (Rabs delta) (Q2R (mTypeToQ m')) ->
  eval_exp E Gamma f1 v1 m1 ->
  eval_exp E Gamma f2 v2 m2 ->
  ((op = Div) -> (~ v2 = 0)%R) ->
  v = perturb (evalBinop op v1 v2) delta ->
  m' = join m1 m2 ->
  eval_exp E Gamma (Binop op f1 f2) v m'.
Proof.
  intros; subst; auto.
Qed.

Hint Resolve Binop_dist'.
377

378 379 380 381 382
(**
  Define the set of "used" variables of an expression to be the set of variables
  occuring in it
**)
Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
383 384
  match e with
  | Var _ x => NatSet.singleton x
385 386
  | Unop u e1 => usedVars e1
  | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
387
  | Downcast _ e1 => usedVars e1
388 389
  | _ => NatSet.empty
  end.
390

391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411
Lemma toRMap_eval_M0 f v E Gamma m:
  eval_exp E (toRMap Gamma) (toREval f) v m -> m = M0.
Proof.
  revert v E Gamma m.
  induction f; intros * eval_f; inversion eval_f; subst;
  repeat
    match goal with
    | H: context[toRMap _ _] |- _ => unfold toRMap in H
    | H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
    | H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
    | H: None = Some ?m |- _ => inversion H
    end; try auto.
  - eapply IHf; eauto.
  - eapply IHf; eauto.
  - assert (m1 = M0)
      by (eapply IHf1; eauto).
    assert (m2 = M0)
      by (eapply IHf2; eauto);
      subst; auto.
Qed.

412
(**
413
  If |delta| <= 0 then perturb v delta is exactly v.
414
**)
415
Lemma delta_0_deterministic (v:R) (delta:R):
Heiko Becker's avatar
Heiko Becker committed
416 417 418 419
  (Rabs delta <= 0)%R ->
  perturb v delta = v.
Proof.
  intros abs_0; apply Rabs_0_impl_eq in abs_0; subst.
420
  unfold perturb. lra.
Heiko Becker's avatar
Heiko Becker committed
421 422
Qed.

423
(**
424
Evaluation with 0 as machine epsilon is deterministic
425
**)
426
Lemma meps_0_deterministic (f:exp R) (E:env) Gamma:
427
  forall v1 v2,
428 429
  eval_exp E (toRMap Gamma) (toREval f) v1 M0 ->
  eval_exp E (toRMap Gamma) (toREval f) v2 M0 ->
430 431
  v1 = v2.
Proof.
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447
  induction f;
    intros v1 v2 ev1 ev2.
  - inversion ev1; inversion ev2; subst.
    rewrite H1 in H6.
    inversion H6; auto.
  - inversion ev1; inversion ev2; subst.
    simpl in *.
    rewrite Q2R0_is_0 in *;
    repeat (rewrite delta_0_deterministic; try auto).
  - inversion ev1; inversion ev2; subst; try congruence.
    + rewrite (IHf v0 v3); eauto.
    + rewrite (IHf v0 v3); eauto.
      simpl in *.
      rewrite Q2R0_is_0 in *;
        repeat (rewrite delta_0_deterministic; try auto).
  - inversion ev1; inversion ev2; subst.
448 449 450 451 452
    assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
    assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
    subst.
453 454 455 456 457 458 459 460 461 462 463 464
    rewrite (IHf1 v0 v4); try auto.
    rewrite (IHf2 v3 v5); try auto.
    simpl in *.
    rewrite Q2R0_is_0 in *.
    repeat (rewrite delta_0_deterministic; try auto).
  - inversion ev1; inversion ev2; subst.
    apply M0_least_precision in H1;
      apply M0_least_precision in H7; subst.
    rewrite (IHf v0 v3); try auto.
    simpl in *.
    rewrite Q2R0_is_0 in *.
    repeat (rewrite delta_0_deterministic; try auto).
465 466
Qed.

467 468 469 470
(**
Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
471
variables in the Environment.
472
 **)
473
Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 Gamma delta:
474
  (b = Div -> ~(v2 = 0 )%R) ->
475
  (Rabs delta <= Q2R (mTypeToQ (join m1 m2)))%R ->
476 477
  eval_exp E Gamma f1 v1 m1 ->
  eval_exp E Gamma f2 v2 m2 ->
478
  eval_exp E Gamma (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta) (join m1 m2) ->
479 480
  eval_exp (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
           (updDefVars 2 m2 (updDefVars 1 m1 Gamma))
481
             (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) delta) (join m1 m2).
482
Proof.
483 484
  intros no_div_zero eval_f1 eval_f2 eval_float.
  econstructor; try auto.
485 486
Qed.

Heiko Becker's avatar
Heiko Becker committed
487 488 489 490 491 492 493 494 495 496 497 498 499
Lemma eval_eq_env e:
  forall E1 E2 Gamma v m,
    (forall x, E1 x = E2 x) ->
    eval_exp E1 Gamma e v m ->
    eval_exp E2 Gamma e v m.
Proof.
  induction e; intros;
    (match_pat (eval_exp _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
    try eauto.
  eapply Var_load; auto.
  rewrite <- (H n); auto.
Qed.

500
(*
501 502 503
(**
Analogous lemma for unary expressions.
**)
504 505
Lemma unary_unfolding (e:exp R) (eps:R) (E:env) (v:R):
  (eval_exp eps E (Unop Inv e) v <->
506
   exists v1,
507 508
     eval_exp eps E e v1 /\
     eval_exp eps (updEnv 1 v1 E) (Unop Inv (Var R 1)) v).
509 510 511 512 513 514 515 516 517
Proof.
  split.
  - intros eval_un.
    inversion eval_un; subst.
    exists v1.
    repeat split; try auto.
    constructor; try auto.
    constructor; auto.
  - intros exists_val.
518 519
    destruct exists_val as [v1 [eval_f1 eval_e_E]].
    inversion eval_e_E; subst.
520 521 522
    inversion H1; subst.
    unfold updEnv in *; simpl in *.
    constructor; auto.
523
    inversion H3; subst; auto.
524
Qed. *)
525

526
(*   Using the parametric expressions, define boolean expressions for conditionals *)
527
(* **)
528 529 530
(* Inductive bexp (V:Type) : Type := *)
(*   leq: exp V -> exp V -> bexp V *)
(* | less: exp V -> exp V -> bexp V. *)
531

532
(**
533
  Define evaluation of boolean expressions
534
 **)
535 536 537 538 539 540 541 542 543 544 545 546 547
(* Inductive bval (E:env): (bexp R) -> Prop -> Prop := *)
(*   leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(*     eval_exp E f1 v1 -> *)
(*     eval_exp E f2 v2 -> *)
(*     bval E (leq f1 f2) (Rle v1 v2) *)
(* |less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)
(*     eval_exp E f1 v1 -> *)
(*     eval_exp E f2 v2 -> *)
(*     bval E (less f1 f2) (Rlt v1 v2). *)
(* (** *)
(*  Simplify arithmetic later by making > >= only abbreviations *)
(* **) *)
(* Definition gr := fun (V:Type) (f1: exp V) (f2: exp V) => less f2 f1. *)
Nikita Zyuzin's avatar
Nikita Zyuzin committed
548
(* Definition greq := fun (V:Type) (f1:exp V) (f2: exp V) => leq f2 f1. *)