IntervalValidation.v 4.09 KB
Newer Older
1 2
Require Import Coq.QArith.QArith Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.IntervalArithQ Daisy.Infra.RationalConstruction Daisy.Infra.RealRationalProps Daisy.IntervalArith.
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35

Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
  let (intv, _) := absenv e in
    match e with
    | Var v =>
      let bounds_v := P v in
      andb (Qeqb (fst intv) (fst (bounds_v))) (Qeqb (snd intv) (snd (bounds_v)))
    | Param v =>
      let bounds_v := P v in
      andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd intv) (snd (bounds_v)))
    | Const n =>
      andb (Qleb (fst intv) n) (Qleb (snd intv) n)
    | 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
          | Div => false
          end
      in
      andb rec opres
    end.

36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 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
Lemma validIntervalbounds_correct (e:exp Q):
  forall (absenv:analysisResult) (P:precond) cenv vR,
  validIntervalbounds e absenv P = true ->
  eval_exp 0%R cenv (toRExp e) vR ->
  contained vR (Q2R (fst (fst(absenv e))), Q2R (snd (fst (absenv e)))).
Proof.
  induction e.
  - intros absenv P cenv vR valid_bounds eval_e.
    unfold validIntervalbounds in valid_bounds.
    destruct (absenv (Var Q n)) as [intv err].
    simpl.
    (* needs that Precond approximates value *)
    admit.
  - intros absenv P cenv vR valid_bounds eval_e.
    unfold validIntervalbounds in valid_bounds.
    destruct (absenv (Param Q n)) as [intv err].
    (* same *)
    admit.
  - intros absenv P cenv vR valid_bounds eval_e.
    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.
    destruct valid_bounds.
    unfold contained; simpl.
    split.
    + apply Is_true_eq_true in H.
      unfold Qleb in *.
      apply Qle_bool_iff in H.
      admit.
    + admit.
  - destruct b.
    + admit.
    + admit.
    + admit.
    + intros absenv P cenv vR valid_bounds eval_e.
      simpl in valid_bounds.
      destruct (absenv (Binop Div e1 e2));
        destruct (absenv e1);
        destruct (absenv e2).
      apply Is_true_eq_left in valid_bounds.
      apply andb_prop_elim in valid_bounds.
      destruct valid_bounds.
      unfold Is_true in *; simpl in *. contradiction.
Admitted.

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
Definition u:nat := 1.
(** 1655/5 = 331; 0,4 = 2/5 **)
Definition cst1:Q := 1657 # 5.

(** Define abbreviations **)
Definition varU:exp Q := Param Q u.
Definition valCst:exp Q := Const cst1.
Definition valCstAddVarU:exp Q := Binop Plus valCst varU.

(** Error values **)
Definition errCst1 :Q := rationalFromNum (36792791036077685#1) 16 14.
Definition errVaru := rationalFromNum (11102230246251565#1) 16 14.
Definition lowerBoundAddUCst:Q := 1157 # 5.
Definition upperBoundAddUCst:Q := 2157 # 5.
Definition errAddUCst := rationalFromNum (9579004256465851#1) 15 14.

(** The added assertion becomes the precondition for us **)
Definition precondition := fun n:nat => (- (100#1),100#1).
Definition absenv := fun e:exp Q => match e with
                                 |Const n => (cst1,cst1,0)
                                 |Binop b e1 e2 => (lowerBoundAddUCst,upperBoundAddUCst,0)
                                 | Param v => (-(100#1),100#1,0)
                                 | _ => (0,0,0)
                                 end.

Eval compute in isSupersetIntv (lowerBoundAddUCst,upperBoundAddUCst) (lowerBoundAddUCst,upperBoundAddUCst).
Eval compute in addIntv (cst1,cst1) (-(100#1),100#1).

Eval compute in validIntervalbounds valCst (fun _ => (cst1,cst1,0)) (fun _ => (cst1,cst1)).
Eval compute in validIntervalbounds varU (fun _ => (- (100#1),100#1,0)) precondition.