AbsoluteError.v 3.45 KB
Newer Older
1
2
3
4
5
(**
  Definition of the computation of the absolute error.
  used to verify analsysis result in the final theorem of a certificate.
 **)
Require Import Coq.Reals.Reals.
6
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction Daisy.Infra.RealSimps.
Heiko Becker's avatar
Heiko Becker committed
7
Require Import Daisy.IntervalArith Daisy.Expressions Daisy.Commands.
8

9
Definition abs_env:Type := exp R -> interval -> err -> Prop.
Heiko Becker's avatar
Heiko Becker committed
10

11
(**
12
13
  First define when given an interval and an error, when another error is sound overapproximation of the absolute error
**)
14
Definition isSoundErr (error:err) (iv:interval) (propagatedErr:err) :=
Heiko Becker's avatar
Heiko Becker committed
15
  (error >= machineEpsilon * Rmax (Rabs (IVlo iv)) (Rabs (IVhi iv)))%R.
16

17
Definition maxAbs (IV:interval) := Rmax (Rabs (IVlo IV)) (Rabs (IVhi IV)).
18

Heiko Becker's avatar
Heiko Becker committed
19
Definition mult_err (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) :=
20
  (maxAbs
21
22
23
     (addInterval
        (addInterval
           (multInterval
24
25
              (getIntv val_e1)
              (getErr val_e2, getErr val_e2))
26
           (multInterval
27
28
              (getIntv val_e2)
              (getErr val_e1, getErr val_e1)))
29
30
31
        (multInterval
           (multInterval
              (multInterval
32
33
34
35
                 (getIntv val_e1)
                 (getIntv val_e2))
              (getErr val_e1, getErr val_e1))
           (getErr val_e2, getErr val_e1)))).
36

Heiko Becker's avatar
Heiko Becker committed
37
Definition isSoundErrBin (op:binop) (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:ann) (val:ann):=
38
  match op with
39
    Plus
40
41
    => isSupersetInterval (getIntv val) (addInterval (getIntv val_e1) (getIntv val_e2)) /\
      isSoundErr (getErr val) (getIntv val) (getErr val_e1 + getErr val_e2)%R
42
  |Sub
Heiko Becker's avatar
Heiko Becker committed
43
   => isSupersetInterval (getIntv val) (subtractInterval (getIntv val_e1) (getIntv val_e2)) /\
44
     isSoundErr (getErr val) (getIntv val) (getErr val_e1 - getErr val_e2)%R
45
  |Mult
46
47
   => isSupersetInterval (getIntv val) (multInterval (getIntv val_e1) (getIntv val_e2)) /\
      isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 val_e2)
48
  |Div
49
     (** FIXME!! **)
50
   => (isSupersetInterval (getIntv val) (intv_div_err (getIntv val_e1) (getErr val_e1) (getIntv val_e2) (getErr val_e2)) /\
Heiko Becker's avatar
Heiko Becker committed
51
      isSoundErr (getErr val) (getIntv val) (mult_err e1 val_e1 e2 (((/ IVlo (getIntv val_e2))%R,  (/ IVhi (getIntv val_e2))%R), getErr val_e2)))
52
end.
53
54

Inductive AbsErrExp : exp R -> abs_env -> err -> Prop :=
55
  AbsErrConst n iv e (env:abs_env):
56
    env (Const n) (iv) e ->
57
    isSoundErr e iv machineEpsilon ->
58
    AbsErrExp (Const n) env e
59
|AbsErrVar v iv e (env:abs_env):
60
   env (Var R v) iv e ->
61
   isSoundErr e iv machineEpsilon ->
62
   AbsErrExp (Var R v) env e
63
64
65
66
|AbsErrParam v iv e (env:abs_env):
   env (Param R v) iv e ->
   isSoundErr e iv machineEpsilon ->
   AbsErrExp (Param R v) env e
67
68
69
70
71
72
73
74
|AbsErrBinop op e1 iv1 er1 e2 iv2 er2 iv eabs (env:abs_env):
   env e1 iv1 er1 ->
   env e2 iv2 er2 ->
   env (Binop op e1 e2) iv eabs ->
   AbsErrExp e1 env er1 ->
   AbsErrExp e2 env er2 ->
   isSoundErrBin op e1 (iv1,er1) e2 (iv2,er2) (iv,eabs) ->
   AbsErrExp (Binop op e1 e2) env eabs.
75

76
Definition AbsErrBExp (c: bexp R) (err:intv*err) := True.
77
78

Inductive AbsErrPrg : cmd R -> abs_env -> err -> Prop :=
79
80
81
82
  AbsErrLet (x:nat) e s iv er (env:abs_env) err:
    env e iv er ->
    AbsErrExp e env er ->
    (env (Var R x) iv er) ->
83
84
85
86
87
88
89
    AbsErrPrg s env err ->
    AbsErrPrg (Let R x e s) env err
|AbsErrIte c s t env err:
(*   AbsErrBExp c (env c) -> *)
   AbsErrPrg s env err ->
   AbsErrPrg t env err ->
   AbsErrPrg (Ite R c s t) env err
90
91
92
93
|AbsErrRet e iv er (env:abs_env) :
   env e iv er ->
   AbsErrExp e env er ->
   AbsErrPrg (Ret R e) env er.