ErrorAnalysis.v 3.92 KB
Newer Older
1 2 3 4
From Coq
     Require Import Reals.Reals QArith.Qreals.

From Flover
5
     Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.
6

7
Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
8
  (match e with
9 10
  | Unop u e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
  | Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
11
  | Binop b e1 e2 =>
12 13
    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap
14
  | Fma e1 e2 e3 =>
15 16 17
    validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap /\
    validErrorBoundsRec e3 E1 E2 A Gamma DeltaMap
18 19
  | _ => True
   end)  /\
20
  forall v__R (iv: intv) (err: error),
21
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
22 23
    FloverMap.find e A = Some (iv, err) ->
    (exists v__FP m__FP,
24
      eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
25
    (forall v__FP m__FP,
26
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
27
        (Rabs (v__R - v__FP) <= (Q2R err))%R).
28

29 30 31 32 33 34 35 36
Definition validErrorBounds e E1 E2 A Gamma: Prop :=
  forall DeltaMap,
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    validErrorBoundsRec e E1 E2 A Gamma DeltaMap.

Lemma validErrorBoundsRec_single e E1 E2 A Gamma DeltaMap:
  validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
37
  forall v__R iv err,
38
    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
39 40
    FloverMap.find e A = Some (iv, err) ->
    (exists v__FP m__FP,
41
      eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP) /\
42
    (forall v__FP m__FP,
43
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
44
        (Rabs (v__R - v__FP) <= (Q2R err))%R).
45 46 47
Proof.
  intros validError_e;
    intros;  destruct e; cbn in *; split;
48
      edestruct validError_e as (? & ? & ?); eauto.
49
Qed.
50

51
Fixpoint validErrorBoundsCmdRec (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
52
  match c with
53
  | Let m x e k =>
54
    validErrorBoundsRec e E1 E2 A Gamma DeltaMap /\
55 56 57 58 59 60 61
    (exists iv_e err_e iv_x err_x,
       FloverMap.find e A = Some (iv_e, err_e) /\
       FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
       Qeq_bool err_e err_x = true) /\
    (forall v__R v__FP,
        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
62 63
        validErrorBoundsCmdRec k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
  | Ret e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
64 65 66 67 68 69 70 71 72 73
  end  /\
  forall v__R (iv: intv) (err: error),
    bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
    FloverMap.find (getRetExp c) A = Some (iv, err) ->
    (exists v__FP m__FP,
      bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
    (forall v__FP m__FP,
        bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).

74 75 76 77 78 79 80 81
Definition validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma: Prop :=
  forall DeltaMap,
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap.

Lemma validErrorBoundsCmdRec_single c E1 E2 A Gamma DeltaMap:
  validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap ->
82 83 84 85 86 87 88 89 90 91 92
  forall v__R (iv: intv) (err: error),
    bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
    FloverMap.find (getRetExp c) A = Some (iv, err) ->
    (exists v__FP m__FP,
      bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP) /\
    (forall v__FP m__FP,
        bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
        (Rabs (v__R - v__FP) <= (Q2R err))%R).
Proof.
  intros validError_e;
    intros;  destruct c; cbn in *; split;
93
      edestruct validError_e as (? & ? & ?); eauto.
94
Qed.