FPRangeValidator.v 11.8 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
  match typeMap e with
  |Some m =>
        let (iv_e, err_e) := A e in
Heiko Becker's avatar
Heiko Becker committed
12
        let iv_e_float := widenIntv iv_e err_e in
Heiko Becker's avatar
Heiko Becker committed
13 14 15
        let recRes :=
            match e with
            | Binop b e1 e2 =>
Heiko Becker's avatar
Heiko Becker committed
16
              FPRangeValidator e1 A typeMap dVars &&
Heiko Becker's avatar
Heiko Becker committed
17 18 19 20 21 22 23 24 25 26 27 28
              FPRangeValidator e2 A typeMap dVars
            | 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
Heiko Becker's avatar
Heiko Becker committed
29 30 31 32
            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
Heiko Becker's avatar
Heiko Becker committed
33 34
            else
              false
Heiko Becker's avatar
Heiko Becker committed
35 36 37 38
        | _ => 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
Heiko Becker's avatar
Heiko Becker committed
39 40 41 42 43 44
              else
                false
        end
  | None => false
  end.

Heiko Becker's avatar
Heiko Becker committed
45 46 47 48 49 50 51
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
52 53
  end.

54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
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.


71
Theorem FPRangeValidator_sound:
72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96
  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 ->
  (forall v, NatSet.In v fVars ->
        exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
  (forall v, NatSet.In v fVars \/ NatSet.In v dVars ->
        exists m, Gamma v = Some m) ->
  (forall v, NatSet.In v dVars ->
        exists vR, E1 v = Some vR /\
              Q2R (fst (fst (A (Var Q v)))) <= vR <= Q2R (snd (fst (A (Var Q v)))))%R ->
  (forall v, NatSet.In v dVars ->
        exists vF m, E2 v = Some vF /\ tMap (Var Q v) = Some m /\ validFloatValue vF m) ->
  validFloatValue v m.
Proof.
  intros *.
  unfold FPRangeValidator.
  intros.
  destruct (A e) as [iv_e err_e] eqn:?;
    destruct iv_e as [e_lo e_hi] eqn:?; simpl in *.
  assert (tMap e = Some m)
97 98
    as type_e
      by (eapply typingSoundnessExp; eauto).
99 100 101
  subst; simpl in *.
  unfold validFloatValue.
  assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
102 103
                Q2R (fst (fst (A e))) <= vR <= Q2R (snd (fst (A e))))%R
         as eval_real_exists.
104 105 106 107 108 109 110 111
  { eapply validIntervalbounds_sound; eauto.
    - intros; apply H8.
      rewrite <- NatSet.mem_spec; auto.
    - intros. apply H6.
      rewrite <- NatSet.mem_spec; auto.
    - intros. apply H7.
      set_tac.
      rewrite <- NatSet.union_spec; auto. }
112 113 114 115 116 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 149 150 151
  destruct eval_real_exists as [vR [eval_real vR_bounded]].
  assert (Rabs (vR - v) <= Q2R (snd (A e)))%R.
  { eapply validErrorbound_sound; eauto.
    - intros * v1_dVar.
      apply H8; set_tac.
    - intros * v0_fVar.
      apply H6. rewrite <- NatSet.mem_spec; auto.
    - intros * v1_in_union.
      apply H7; set_tac.
      rewrite NatSet.union_spec in v1_in_union; auto.
    - eauto ; instantiate (1:= e_hi).
      instantiate (1:=e_lo). rewrite Heqp. reflexivity. }
  rewrite Heqp in *; simpl in *.
  destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
    as [v_in_errIv];
    try auto.
  unfold IVlo, IVhi in *; simpl in *.
  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;
    unfold validFloatValue in *; simpl in *;
      rewrite type_e, Heqp in *; simpl in *.
  - 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.
    + andb_to_prop H4.
      prove_fprangeval m v L1 R.
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
152 153
  - andb_to_prop H4.
    prove_fprangeval m v L1 R.
154
Qed.
155

156 157
Lemma FPRangeValidatorCmd_sound (f:cmd Q):
  forall E1 E2 Gamma v vR m A tMap P fVars dVars outVars,
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
  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 ->
  (forall v,
      NatSet.In v fVars ->
      exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
  (forall v,
      NatSet.In v fVars \/ NatSet.In v dVars ->
      exists m, Gamma v = Some m) ->
  (forall v,
      NatSet.In v dVars ->
      exists vR,
        E1 v = Some vR /\ Q2R (ivlo (fst (A (Var Q v)))) <= vR /\
        vR <= Q2R (ivhi(fst (A (Var Q v)))))%R ->
  (forall v,
      NatSet.In v dVars ->
      exists vF m,
        E2 v = Some vF /\ tMap (Var Q v) = Some m /\
        validFloatValue vF m) ->
  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.
192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288
      - assert (tMap e = Some m)
          by(eapply typingSoundnessExp; eauto).
        match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
        destruct (A e) as [iv_e err_e] eqn:?;
          destruct iv_e as [e_lo e_hi] eqn:?.
        edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars) (dVars := dVars) P (absenv:=A) (nR:=v0) (err:=err_e)) as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
        + set_tac. split; try auto.
          rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
          hnf; intros; subst.
          set_tac.
        + intros. apply H10; auto; set_tac.
        + intros; apply H8; auto. rewrite <- NatSet.mem_spec; auto.
        + intros. apply H9; set_tac. rewrite <- NatSet.union_spec; auto.
        + edestruct (validIntervalbounds_sound e A P (fVars:=fVars) (dVars:=dVars) E1); eauto.
          * intros. apply H10; auto; set_tac.
          * set_tac. split; try auto.
            rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
            hnf; intros; subst.
            set_tac.
          * intros. apply H8. rewrite NatSet.mem_spec in *; auto.
          * intros. instantiate (1:= Gamma); apply H9. set_tac.
            rewrite NatSet.union_spec in *; auto.
          * rewrite H3 in *.
            destruct (tMap (Var Q n)) eqn:?; simpl in *; try congruence.
            rename x into vR_e.
            destruct H4 as [eval_e_real bounded_vR_e].
            rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H20) in *; try auto.
            andb_to_prop R5.
            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.
            { apply approxUpdBound; auto.
              simpl in *.
              apply Rle_trans with (r2:= Q2R err_e); try lra.
              rewrite Heqp in *; simpl in *.
              eapply err_bounded_e. eauto.
              apply Qle_Rle.
              rewrite Qeq_bool_iff in *.
              rewrite R1. lra. }
            { 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.
              - rewrite NatSet.remove_spec, NatSet.union_spec.
                split; try auto.
                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.
                exfalso; apply H16; set_tac.
              - apply H8; auto. }
            { intros. unfold updDefVars.
              destruct (v2 =? n) eqn:?; eauto.
              apply H9. destruct H4; try auto.
              rewrite NatSet.add_spec in H4.
              rewrite Nat.eqb_neq in *.
              destruct H4; subst; try congruence; auto. }
            { intros. unfold updEnv.
              destruct (v2 =? n) eqn:?.
              - exists vR_e. rewrite Nat.eqb_eq in *; subst.
                split; try auto.
                destruct bounded_vR_e;
                  rewrite Heqp in *; simpl in *.
                  split.
                + apply Rle_trans with (r2:=Q2R e_lo); try lra.
                  apply Qle_Rle. rewrite Qeq_bool_iff in *; rewrite R4; lra.
                + apply Rle_trans with (r2:=Q2R e_hi); try lra.
                  apply Qle_Rle; rewrite Qeq_bool_iff in *; rewrite R3; lra.
              - apply H10. rewrite Nat.eqb_neq in *.
                rewrite NatSet.add_spec in H4.
                destruct H4; try auto; subst; congruence. }
            { 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.
                rewrite NatSet.remove_spec, NatSet.union_spec.
                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
289
Qed.