FPRangeValidator.v 9.96 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1 2 3

(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)

4
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz.
Heiko Becker's avatar
Heiko Becker committed
5

6
Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs Daisy.Infra.Ltacs Daisy.Infra.RealRationalProps.
Heiko Becker's avatar
Heiko Becker committed
7 8

Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
Heiko Becker's avatar
Heiko Becker committed
9 10 11 12 13 14 15 16
  match DaisyMap.find e typeMap, DaisyMap.find e A with
  |Some m, Some (iv_e, err_e) =>
   let iv_e_float := widenIntv iv_e err_e in
   let recRes :=
       match e with
       | Binop b e1 e2 =>
         FPRangeValidator e1 A typeMap dVars &&
         FPRangeValidator e2 A typeMap dVars
17 18 19 20
       | Fma e1 e2 e3 =>
         FPRangeValidator e1 A typeMap dVars &&
         FPRangeValidator e2 A typeMap dVars &&
         FPRangeValidator e3 A typeMap dVars
Heiko Becker's avatar
Heiko Becker committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
       | Unop u e =>
         FPRangeValidator e A typeMap dVars
       | Downcast m e => FPRangeValidator e A typeMap dVars
       | _ =>  true
       end
   in
   match e with
   | Var _ v =>
     if NatSet.mem v dVars
     then true
     else
       if (validValue (ivhi iv_e_float) m &&
           validValue (ivlo iv_e_float) m)
       then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
             (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) &&
              recRes
       else
         false
   | _ => if (validValue (ivhi iv_e_float) m &&
              validValue (ivlo iv_e_float) m)
         then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) &&
               (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes
         else
           false
   end
  | _, _ => false
Heiko Becker's avatar
Heiko Becker committed
47 48
  end.

Heiko Becker's avatar
Heiko Becker committed
49 50 51 52 53 54 55
Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
  match f with
  | Let m n e g =>
    if FPRangeValidator e A typeMap dVars
    then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars)
     else false
| Ret e => FPRangeValidator e A typeMap dVars
56 57
  end.

58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
Ltac prove_fprangeval m v L1 R:=
  destruct m eqn:?; try auto;
  unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
  rewrite orb_true_iff in *;
  destruct L1; destruct R; canonize_hyps;
  rewrite <- Rabs_eq_Qabs in *;
  Q2R_to_head;
  rewrite <- Q2R_minus, <- Q2R_plus in *;
  repeat (match goal with
          |H: _ = true |- _ => andb_to_prop H
          end);
  destruct (Req_dec v 0); try auto;
  destruct (Rle_lt_dec (Rabs v) (Q2R (minValue m)))%R (* denormal case *);
  try auto;
  destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.


75
Theorem FPRangeValidator_sound:
76 77 78 79 80 81 82 83
  forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars,
  approxEnv E1 Gamma A fVars dVars E2 ->
  eval_exp E2 Gamma (toRExp e) v m ->
  typeCheck e Gamma tMap = true ->
  validIntervalbounds e A P dVars = true ->
  validErrorbound e tMap A dVars = true ->
  FPRangeValidator e A tMap dVars = true ->
  NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
84 85 86 87 88
  dVars_range_valid dVars E1 A ->
  fVars_P_sound fVars E1 P ->
  vars_typed (NatSet.union fVars dVars) Gamma ->
 (forall v, NatSet.In v dVars ->
        exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
89 90 91 92 93
  validFloatValue v m.
Proof.
  intros *.
  unfold FPRangeValidator.
  intros.
Heiko Becker's avatar
Heiko Becker committed
94
  assert (DaisyMap.find e tMap = Some m)
95 96
    as type_e
      by (eapply typingSoundnessExp; eauto).
97
  unfold validFloatValue.
Heiko Becker's avatar
Heiko Becker committed
98 99 100 101 102
  edestruct (validIntervalbounds_sound e (A:=A) (P:=P))
    as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]]; eauto.
  destruct iv_e as  [e_lo e_hi].
  assert (Rabs (vR - v) <= Q2R (err_e))%R.
  { eapply validErrorbound_sound; eauto. }
103 104 105
  destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
    as [v_in_errIv];
    try auto.
Heiko Becker's avatar
Heiko Becker committed
106
  simpl in *.
107 108 109 110 111
  assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/
          Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R
    as abs_bounded
    by (apply bounded_inAbs; auto).
  destruct e;
Heiko Becker's avatar
Heiko Becker committed
112 113
    unfold validFloatValue in *; cbn in *;
      rewrite type_e in *; cbn in *.
114 115 116 117 118 119
  - destruct (n mem dVars) eqn:?; simpl in *.
    + destruct (H9 n); try set_tac.
      destruct H12 as [m2 [env_eq [map_eq validVal]]].
      inversion H0; subst.
      rewrite env_eq in H14; inversion H14; subst.
      rewrite map_eq in type_e; inversion type_e; subst; auto.
Heiko Becker's avatar
Heiko Becker committed
120
    + Daisy_compute.
121
      prove_fprangeval m v L1 R.
Heiko Becker's avatar
Heiko Becker committed
122
  - Daisy_compute.
123
    prove_fprangeval m v L1 R.
Heiko Becker's avatar
Heiko Becker committed
124 125 126 127 128 129 130 131
  - Daisy_compute; try congruence.
    type_conv; subst.
    prove_fprangeval m0 v L1 R.
  - Daisy_compute; try congruence.
    type_conv; subst.
    prove_fprangeval (join m0 m1) v L1 R.
  - Daisy_compute; try congruence.
    type_conv; subst.
132
    prove_fprangeval m v L1 R.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
133 134
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
135
Qed.
136

137 138
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
  forall E1 E2 Gamma v vR m A tMap P fVars dVars outVars,
139 140 141 142 143 144 145 146 147
  approxEnv E1 Gamma A fVars dVars E2 ->
  ssa f (NatSet.union fVars dVars) outVars ->
  bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
  bstep (toRCmd f) E2 Gamma v m ->
  typeCheckCmd f Gamma tMap = true ->
  validIntervalboundsCmd f A P dVars = true ->
  validErrorboundCmd f tMap A dVars = true ->
  FPRangeValidatorCmd f A tMap dVars = true ->
  NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
Heiko Becker's avatar
Heiko Becker committed
148 149 150 151 152
  dVars_range_valid dVars E1 A ->
  fVars_P_sound fVars E1 P ->
  vars_typed (NatSet.union fVars dVars) Gamma ->
 (forall v, NatSet.In v dVars ->
        exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
153 154 155 156 157 158 159 160 161
  validFloatValue v m.
Proof.
  induction f; intros;
    simpl in *;
    (match_pat (bstep _ _ (toRMap _) _ _) (fun H => inversion H; subst; simpl in *));
     (match_pat (bstep _ _ Gamma _ _) (fun H => inversion H; subst; simpl in *));
      repeat match goal with
             | H : _ = true |- _ => andb_to_prop H
             end.
Heiko Becker's avatar
Heiko Becker committed
162
      - assert (DaisyMap.find e tMap = Some m)
163 164
          by(eapply typingSoundnessExp; eauto).
        match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
Heiko Becker's avatar
Heiko Becker committed
165 166 167 168 169
        Daisy_compute.
        edestruct (validIntervalbounds_sound e L1 (Gamma := Gamma)(P:= P) (A:=A)
                                             (fVars:=fVars) (dVars:=dVars)
                                             (E:=E1))
        as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]]; eauto.
170
        + set_tac. split; try auto.
Heiko Becker's avatar
Heiko Becker committed
171 172 173 174 175 176 177
          split; try auto.
          hnf; intros; subst; set_tac.
        + destr_factorize.
          edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
                                           (dVars := dVars) (A:=A) (P:=P) tMap
                                           (nR:=v0) (err:=err_e) (elo:=q) (ehi:=q0))
          as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
178
          * set_tac. split; try auto.
Heiko Becker's avatar
Heiko Becker committed
179 180 181
            split; try auto.
            hnf; intros; subst; set_tac.
          * rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H20) in *; try auto.
182 183 184
            apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
                          (updDefVars n m Gamma) v vR m0 A tMap P fVars
                          (NatSet.add n dVars) (outVars)); eauto.
Heiko Becker's avatar
Heiko Becker committed
185
            { eapply approxUpdBound; eauto.
186 187 188 189 190
              simpl in *.
              apply Rle_trans with (r2:= Q2R err_e); try lra.
              eapply err_bounded_e. eauto.
              apply Qle_Rle.
              rewrite Qeq_bool_iff in *.
Heiko Becker's avatar
Heiko Becker committed
191 192 193
              destruct i; inversion Heqo0; subst.
              rewrite R2.
              lra. }
194 195 196 197 198 199 200 201 202 203 204
            { eapply ssa_equal_set; eauto.
              hnf. intros a; split; intros in_set.
              - rewrite NatSet.add_spec, NatSet.union_spec;
                  rewrite NatSet.union_spec, NatSet.add_spec in in_set.
                destruct in_set as [P1 | [ P2 | P3]]; auto.
              - rewrite NatSet.add_spec, NatSet.union_spec in in_set;
                  rewrite NatSet.union_spec, NatSet.add_spec.
                destruct in_set as [P1 | [ P2 | P3]]; auto. }
            { eapply (swap_Gamma_bstep (Gamma1 := updDefVars n M0 (toRMap Gamma))); eauto.
              eauto using Rmap_updVars_comm. }
            { set_tac; split.
Heiko Becker's avatar
Heiko Becker committed
205
              - split; try auto.
206 207 208 209 210 211 212 213 214
                hnf; intros; subst.
                apply H5; rewrite NatSet.add_spec; auto.
              - hnf; intros.
                apply H5; rewrite NatSet.add_spec; auto. }
            { intros v2 v2_fVar.
              unfold updEnv.
              case_eq (v2 =? n); intros v2_eq.
              - apply Nat.eqb_eq in v2_eq; subst.
                set_tac.
Heiko Becker's avatar
Heiko Becker committed
215 216 217 218 219 220 221
                destruct v2_fVar as [? |[? ?]]; try congruence.
                exists vR_e, (q1,q2), e1; split; try auto. split; try auto.
                simpl; canonize_hyps. rewrite <- R4, <- R5. auto.
              - apply H8; try auto.
                set_tac. destruct v2_fVar as [v2_n | [? ?]]; try auto.
                rewrite Nat.eqb_neq in v2_eq; congruence. }
            { unfold fVars_P_sound. intros. unfold updEnv.
222
              destruct (v2 =? n) eqn:?; eauto.
Heiko Becker's avatar
Heiko Becker committed
223 224 225 226 227
              rewrite Nat.eqb_eq in *; subst.
              set_tac.
              exfalso; apply H18; set_tac. }
            { unfold vars_typed. intros.
              unfold updDefVars.
228
              destruct (v2 =? n) eqn:?; eauto.
Heiko Becker's avatar
Heiko Becker committed
229 230
              apply H10. rewrite NatSet.union_spec in *.
              destruct H4; try auto.
231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
              rewrite NatSet.add_spec in H4.
              rewrite Nat.eqb_neq in *.
              destruct H4; subst; try congruence; auto. }
            { intros. unfold updEnv.
              type_conv; subst.
              destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *;
                try rewrite Nat.eqb_neq in *.
              - exists v1; subst. exists m1; repeat split; try auto.
                eapply FPRangeValidator_sound; eauto.
                set_tac. split; try auto.
                split; try auto.
                hnf; intros; subst; set_tac.
              - apply H11.
                rewrite NatSet.add_spec in H4; destruct H4;
                  auto; subst; congruence. }
  - eapply FPRangeValidator_sound; eauto.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
247
Qed.