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

From Flover
5 6
     Require Export Infra.ExpressionAbbrevs ErrorAnalysis ErrorValidation
     ErrorValidationAA ExpressionSemanticsDeterministic RealRangeValidator
7
     TypeValidator Environments.
8

9 10
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
           (A:analysisResult) (dVars:NatSet.t) :=
11 12 13 14 15 16 17
  if
  validErrorbound e tMap A dVars
  then true
  else match validErrorboundAA e tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
       | Some _ => true
       | None => false
       end.
18 19

Theorem RoundoffErrorValidator_sound:
20
  forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
21 22 23
    (nR : R) (err : error) (iv : intv) (Gamma : FloverMap.t mType) DeltaMap,
    (forall (e' : expr R) (m' : mType),
        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
24 25 26
    validTypes e Gamma ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
    NatSet.Subset (usedVars e -- dVars) fVars ->
27
    eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) nR REAL ->
28 29
    RoundoffErrorValidator e Gamma A dVars = true ->
    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
30 31 32
    FloverMap.find e A = Some (iv, err) ->
    dVars_contained dVars (FloverMap.empty (affine_form Q)) ->
    validErrorBounds e E1 E2 A Gamma DeltaMap.
33
Proof.
34 35 36
  unfold RoundoffErrorValidator.
  intros; cbn in *.
  destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
37
  - eapply validErrorbound_sound; eauto.
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60
  - destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
      [|congruence].
    destruct p as (expr_map, noise).
    pose proof validErrorboundAA_contained_subexpr as Hsubexpr.
    specialize (Hsubexpr e Gamma A dVars 1%nat noise (FloverMap.empty (affine_form Q)) expr_map).
    specialize Hsubexpr as (Hsubexpr & Hcont & Hcheckedsubexpr); eauto;
      [intros ? Hin; now rewrite FloverMapFacts.P.F.empty_in_iff in Hin|].
    pose proof validErrorboundAA_sound as Hvalidbound.
    specialize (Hvalidbound e E1 E2 A Gamma DeltaMap fVars dVars).
    specialize Hvalidbound as (Hex & Hall); eauto.
    + instantiate (1 := fun x => None); auto.
    + intros ? Hin.
      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
    + intros ? Hin.
      now rewrite FloverMapFacts.P.F.empty_in_iff in Hin.
    + specialize Hex as ((v__e & m__e & Hev) & Hexchecked).
      specialize (Hall v__e m__e Hev) as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & Hall).
      eapply validErrorbound_sound_validErrorBounds; eauto.
      intros e' Hin.
      specialize Hexchecked as (_ & Hex); eauto;
        [now rewrite FloverMapFacts.P.F.empty_in_iff|].
      split; eauto.
      eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
61
Qed.
62

63 64
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
           (A:analysisResult) (dVars:NatSet.t) :=
65 66 67 68 69 70 71
  if
  validErrorboundCmd f tMap A dVars
  then true
  else match validErrorboundAACmd f tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
       | Some _ => true
       | None => false
       end.
72 73

Theorem RoundoffErrorValidatorCmd_sound f:
74 75
  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma,
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
76 77
    ssa f (NatSet.union fVars dVars) outVars ->
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
78
    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
79
    validErrorboundCmd f Gamma A dVars = true ->
80 81
    validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
    validTypesCmd f Gamma ->
82 83
    FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
    (exists vF m,
84
        bstep (toRCmd f) E2 (toRExpMap Gamma) vF m) /\
85
    (forall vF mF,
86
    bstep (toRCmd f) E2 (toRExpMap Gamma) vF mF ->
87 88 89 90 91 92 93
    (Rabs (vR - vF) <= (Q2R err))%R).
Proof.
  intros.
  cbn in *.
  split.
  - eapply validErrorboundCmd_gives_eval; eauto.
  - intros. eapply validErrorboundCmd_sound; eauto.
94
Qed.