SubdivsChecker.v 9.27 KB
Newer Older
Joachim Bard's avatar
Joachim Bard committed
1 2 3
From Flover
     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
4 5
     Environments TypeValidator FPRangeValidator ExpressionAbbrevs ResultChecker.
(*
Joachim Bard's avatar
Joachim Bard committed
6
From Flover
7 8 9 10
     Require Import Infra.RealRationalProps Environments ExpressionSemantics
     IntervalArithQ SMTArith RealRangeArith RealRangeValidator RoundoffErrorValidator
     ssaPrgs TypeValidator ErrorAnalysis ResultChecker.
*)
Joachim Bard's avatar
Joachim Bard committed
11

12 13
Require Import List.

14
Fixpoint resultLeq e (A1 A2: analysisResult) :=
15
  match e with
16 17 18
  | Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
  | Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2
  | Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
19 20 21 22 23 24 25
  | _ => true
  end &&
      match FloverMap.find e A1, FloverMap.find e A2 with
      | Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
      | _, _ => false
      end.

26 27
Lemma resultLeq_sound e A1 A2 :
  resultLeq e A1 A2 = true ->
28 29 30 31 32 33 34 35 36 37 38 39
  exists iv1 err1 iv2 err2,
    FloverMap.find e A1 = Some (iv1, err1) /\
    FloverMap.find e A2 = Some (iv2, err2) /\
    isSupersetIntv iv1 iv2 = true /\
    err1 <= err2.
Proof.
  intros H.
  assert (
      match FloverMap.find e A1, FloverMap.find e A2 with
      | Some (ivA1, errA1), Some (ivA2, errA2) => isSupersetIntv ivA1 ivA2 && (Qleb errA1 errA2)
      | _, _ => false
      end = true).
40
  { unfold resultLeq in H. destruct e;
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
    apply andb_prop in H as [_ H]; auto. }
  Flover_compute.
  repeat eexists; auto.
  - unfold isSupersetIntv. now rewrite L0.
  - apply (reflect_iff _ _ (Z.leb_spec0 _ _)). auto.
Qed.

(* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
  NatSet.Empty dVars ->
  approxEnv E1 Gamma A1 fVars dVars E2 ->
  approxEnv E1 Gamma A2 fVars dVars E2.
Proof.
  intros He H.
  induction H.
  - constructor.
  - econstructor; eauto.
  - exfalso. eapply He. set_tac.
Qed.

61
Definition checkSubdivsStep e absenv defVars Gamma (b: bool) (PA: precond * analysisResult) :=
Joachim Bard's avatar
Joachim Bard committed
62
  let (P, A) := PA in
63
  b && (RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma) &&
64
    resultLeq e A absenv.
Joachim Bard's avatar
Joachim Bard committed
65

66 67
Definition checkSubdivs e absenv subdivs defVars Gamma :=
  fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs true.
Joachim Bard's avatar
Joachim Bard committed
68

69 70
Lemma checkSubdivs_false_fp e absenv subdivs defVars Gamma :
  fold_left (checkSubdivsStep e absenv defVars Gamma) subdivs false = false.
71 72 73 74
Proof.
  induction subdivs as [|[P A] subdivs]; auto.
Qed.

75 76
Lemma checkSubdivs_sound e absenv subdivs defVars Gamma P A :
  checkSubdivs e absenv subdivs defVars Gamma = true ->
77
  In (P, A) subdivs ->
78
  RangeErrorChecker e A P (FloverMap.empty(SMTLogic * SMTLogic)) defVars Gamma = true /\
79
  resultLeq e A absenv = true.
80 81 82 83
Proof.
  intros H Hin.
  induction subdivs; cbn in Hin; auto.
  destruct Hin; subst; auto.
84
  - cbn in *.
85
    destruct (RangeErrorChecker e A P (FloverMap.empty (SMTLogic * SMTLogic)) defVars Gamma) eqn:?;
86
             try (rewrite checkSubdivs_false_fp in H; discriminate H).
87
    split; auto.
88 89
    destruct (resultLeq e A absenv) eqn: ?; auto.
    rewrite checkSubdivs_false_fp in H; auto.
90
  - apply IHsubdivs; auto. cbn in H.
91 92 93
    unfold checkSubdivs.
    destruct (checkSubdivsStep e absenv defVars Gamma true a) eqn:?; auto.
    rewrite checkSubdivs_false_fp in H. discriminate H.
94 95
Qed.

96
(*
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111
Fixpoint merge_subdivs_step (e: expr Q) (acc A1 A2: analysisResult) :=
  match FloverMap.find e A1, FloverMap.find e A2 with
  | Some (iv1, err1), Some (iv2, err2) =>
    let acc1 := FloverMap.add e (unionIntv iv1 iv2, Qmax err1 err2) acc in
    match e with
    | Unop _ e1 | Downcast _ e1 => merge_subdivs_step e1 acc1 A1 A2
    | Binop _ e1 e2 | Let _ _ e1 e2 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
                                  merge_subdivs_step e2 acc2 A1 A2
    | Fma e1 e2 e3 => let acc2 := merge_subdivs_step e1 acc1 A1 A2 in
                     let acc3 := merge_subdivs_step e2 acc2 A1 A2 in
                     merge_subdivs_step e3 acc3 A1 A2
    | _ => acc1
    end
  | _, _ => FloverMap.empty (intv * error)
  end.
112 113 114 115

(* TODO: it might be better to merge all results for one specific expression,
   instead of merging 2 results for all expressions *)
Definition merge_subdivs e hd tl : analysisResult :=
116
  fold_left (merge_subdivs_step e (FloverMap.empty (intv * error))) tl hd.
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
*)

(* TODO: joining of subintervals *)
Definition joinIntv iv1 iv2 : result (option intv) :=
  if isSupersetIntv iv2 iv1 then Succes (Some iv1) else
    if Qeqb (ivhi iv1) (ivlo iv2) then Succes (Some (ivlo iv1, ivhi iv2)) else Fail _ "intervals don't align".

Definition checkDimensionStep x (ivAcc: result (option intv)) P (* (ivNew: option intv) *) :=
  let ivNew := FloverMap.find (Var Q x) P in
  match ivAcc with
  | Succes ivAcc => match ivNew with
                 | Some ivNew => optionBind ivAcc (fun iv => joinIntv iv ivNew) (Succes (Some ivNew))
                 | None => Fail _ "var not found in precond"
                 end
  | f => f
  end.

Definition checkDimension x iv Ps :=
  match fold_left (checkDimensionStep x) Ps (Succes None) with
  | Succes (Some ivU) => isSupersetIntv iv ivU
  | _ => false
          (*
  | Succes None => Fail _ "no subdivisions given"
  | Fail _ msg | FailDet msg _ => Fail _ msg
           *)
  end.

Definition checkAllDimensionsStep Ps b (p: expr Q * intv) :=
  match p with
  | (Var _ x, iv) => b && checkDimension x iv Ps
  | _ => b
  end.
149

150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
Definition checkAllDimensions P Ps :=
  fold_left (checkAllDimensionsStep Ps) P true.

Lemma in_subdivs_intv (Ps: list precondIntv) E (P: precondIntv) :
  checkAllDimensions (FloverMap.elements P) Ps = true ->
  P_intv_sound E P ->
  exists P', In P' Ps /\ P_intv_sound E P'.
Proof.
  intros chk H.
  unfold P_intv_sound in H.
  induction (FloverMap.elements P).
  - admit.
  - cbn in chk.
    assert (checkAllDimensionsStep Ps true a = true) as Heq by admit.
    rewrite Heq in chk.
    apply IHl; auto.
    intros x iv.
    intros ?. apply H. now right.
    (*
    assert (a = (Var Q x, iv) \/ a <> (Var Q x, iv)) as CA by admit.
    destruct CA as [? | Hneq].
    + subst.
      cbn in Heq.
      intros ?. apply H. now right.
    + intros ?. apply H. now right.
*)
Abort.
  
178 179 180 181 182
(* TODO: needs more assumptions, i.e. checker for precond *)
Lemma in_subdivs (subdivs: list (precond * analysisResult)) E P :
  eval_precond E P ->
  exists P' A, In (P', A) subdivs /\ eval_precond E P'.
Admitted.
183 184

(* TODO: check precond sound wrt. subdivs *)
185
(* TODO: merge hd and tl again *)
Joachim Bard's avatar
Joachim Bard committed
186
(** Interval subdivisions checking function **)
187 188
Definition SubdivsChecker (e: expr Q) (absenv: analysisResult)
           (P: precond) hd tl (defVars: FloverMap.t  mType) Gamma :=
189
  validSSA e (preVars P) &&
190
           checkSubdivs e absenv (hd :: tl) defVars Gamma.
Joachim Bard's avatar
Joachim Bard committed
191 192 193 194

(**
   Soundness proof for the interval subdivs checker.
**)
195
Theorem subdivs_checking_sound (e: expr Q) (absenv: analysisResult) P hd_subdivs tl_subdivs defVars Gamma:
196 197 198
  forall (E1 E2: env) DeltaMap,
    (forall (e': expr R) (m': mType),
        exists d: R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
Joachim Bard's avatar
Joachim Bard committed
199 200
    eval_precond E1 P ->
    getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
201
    SubdivsChecker e absenv P hd_subdivs tl_subdivs defVars Gamma = true ->
Joachim Bard's avatar
Joachim Bard committed
202 203 204 205 206 207 208 209 210 211
    exists Gamma,
      approxEnv E1 (toRExpMap Gamma) absenv (freeVars e) NatSet.empty E2 ->
      exists iv err vR vF m,
        FloverMap.find e absenv = Some (iv, err) /\
        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
        (forall vF m,
            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
            (Rabs (vR - vF) <= Q2R err))%R.
Proof.
212 213 214 215 216
  intros * deltas_matched P_valid valid_typeMap subdivs_valid.
  andb_to_prop subdivs_valid.
  rename L into valid_ssa.
  rename R into valid_subdivs.
  apply (in_subdivs (hd_subdivs :: tl_subdivs)) in P_valid as [P' [A [in_subdivs P_valid]]].
217
  (* preVars P == preVars P' should hold *)
218
  assert (validSSA e (preVars P') = true) as valid_ssa' by admit.
219
  pose proof (checkSubdivs_sound  e _ _ _ _ _ _ valid_subdivs in_subdivs) as [range_err_check A_leq].
220 221 222
  assert (ResultChecker e A P' (FloverMap.empty(SMTLogic * SMTLogic))  defVars Gamma = true) as res_check
    by (unfold ResultChecker; now rewrite valid_ssa', range_err_check).
  exists Gamma; intros approxE1E2.
223 224
  assert (approxEnv E1 (toRExpMap Gamma) A (freeVars e) NatSet.empty E2) as approxE1E2'
      by (eapply approxEnv_empty_dVars; eauto).
225 226
  assert (validRanges e A E1 (toRTMap (toRExpMap Gamma))) as validRange.
  { eapply result_checking_sound; eauto.
227
    admit. (* unsat_queries of empty map *) }
228 229
  assert (validErrorBounds e E1 E2 A Gamma DeltaMap) as Hsound.
  { eapply result_checking_sound; eauto.
230
    admit. (* unsat_queries of empty map *) }
231 232 233 234
  eapply validRanges_single in validRange.
  destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
  eapply validErrorBounds_single in Hsound; eauto.
  destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
235
  destruct (resultLeq_sound _ _ _ A_leq) as [iv1 [err1 [iv2 [err2 H]]]].
236 237 238 239 240 241 242
  destruct H as [F1 [F2 [sub err_leq]]].
  exists iv2, err2, vR, vF, mF; repeat split; auto.
  assert (err = err1) by congruence; subst.
  apply Qle_Rle in err_leq.
  intros vF0 m Heval.
  specialize (err_bounded vF0 m Heval).
  lra.
Joachim Bard's avatar
Joachim Bard committed
243
Admitted.