SMTValidation.v 15.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**
    SMT arithmetic checker and its soundness proof.
    The function validSMTIntervalbounds checks wether the given analysis result is
    a valid range arithmetic for each sub term of the given expression e.
    The computation is done using our formalized SMT arithmetic.
    The function is used in CertificateChecker.v to build the full checker.
**)
From Coq
     Require Import QArith.QArith QArith.Qreals QArith.Qminmax Lists.List
     micromega.Psatz.

From Flover
     Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs Infra.RealSimps TypeValidator.

From Flover
     Require Export SMTArith2 IntervalArithQ ssaPrgs RealRangeArith.

Joachim Bard's avatar
Joachim Bard committed
19 20 21 22
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
  match getBound q, getPrecond q with
  | Some (LessQ e' (ConstQ v)), Some qP => if checkPre P qP && smt_expr_eq e' e then Qmax lo v else lo
  | _, _ => lo
23 24
  end.

Joachim Bard's avatar
Joachim Bard committed
25 26 27 28
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P :=
  match getBound q, getPrecond q with
  | Some (LessQ (ConstQ v) e'), Some qP => if checkPre P qP && smt_expr_eq e' e then Qmin hi v else hi
  | _, _ => hi
29 30
  end.

Joachim Bard's avatar
Joachim Bard committed
31 32 33 34
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) P :=
  match FloverMap.find e qMap, iv with
  | None, _ => iv
  | Some (loQ, hiQ), (lo, hi) => (tightenLowerBound e lo loQ P, tightenUpperBound e hi hiQ P)
35 36 37 38 39 40 41 42 43 44 45 46 47 48
  end.

Fixpoint validSMTIntervalbounds (e: expr Q) (A: analysisResult) (P: FloverMap.t intv)
         (Q: FloverMap.t (SMTLogic * SMTLogic)) (validVars: NatSet.t) : bool:=
  match FloverMap.find e A with
  | None => false
  | Some (intv, _) =>
       match e with
       | Var _ x =>
         if NatSet.mem x validVars
         then true
         else
           match FloverMap.find e P with
           | None => false
Joachim Bard's avatar
Joachim Bard committed
49 50
           | Some new_iv => isSupersetIntv new_iv intv
                                          (* && (Qleb lo hi) *)
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
           end
       | Const _ n => (Qleb (ivlo intv) n) && (Qleb n (ivhi intv))
       | Unop o f =>
         if validSMTIntervalbounds f A P Q validVars
         then
           match FloverMap.find f A with
           | None => false
           | Some (iv, _) =>
             match o with
             | Neg =>
               let new_iv := negateIntv iv in
               isSupersetIntv new_iv intv
             | Inv =>
               if (((Qleb (ivhi iv) 0) && (negb (Qeq_bool (ivhi iv) 0))) ||
                   ((Qleb 0 (ivlo iv)) && (negb (Qeq_bool (ivlo iv) 0))))
               then
Joachim Bard's avatar
Joachim Bard committed
67
                 let new_iv := tightenBounds e (invertIntv iv) Q P in
68 69 70 71 72 73 74 75 76 77 78 79 80
                 isSupersetIntv new_iv intv
               else false
             end
           end
         else false
       | Binop op f1 f2 =>
         if ((validSMTIntervalbounds f1 A P Q validVars)
               && (validSMTIntervalbounds f2 A P Q validVars))
         then
           match FloverMap.find f1 A, FloverMap.find f2 A with
           | Some (iv1, _), Some (iv2, _) =>
             match op with
             | Plus =>
Joachim Bard's avatar
Joachim Bard committed
81
               let new_iv := tightenBounds e (addIntv iv1 iv2) Q P in
82 83
               isSupersetIntv new_iv intv
             | Sub =>
Joachim Bard's avatar
Joachim Bard committed
84
               let new_iv := tightenBounds e (subtractIntv iv1 iv2) Q P in
85 86
               isSupersetIntv new_iv intv
             | Mult =>
Joachim Bard's avatar
Joachim Bard committed
87
               let new_iv := tightenBounds e (multIntv iv1 iv2) Q P in
88 89 90 91 92
               isSupersetIntv new_iv intv
             | Div =>
               if (((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
                   ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))))
               then
Joachim Bard's avatar
Joachim Bard committed
93
                 let new_iv := tightenBounds e (divideIntv iv1 iv2) Q P in
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
                 isSupersetIntv new_iv intv
               else false
             end
           | _, _ => false
           end
         else false
       | Fma f1 f2 f3 =>
         if ((validSMTIntervalbounds f1 A P Q validVars)
               && (validSMTIntervalbounds f2 A P Q validVars)
               && (validSMTIntervalbounds f3 A P Q validVars))
         then
           match FloverMap.find f1 A, FloverMap.find f2 A, FloverMap.find f3 A with
           | Some (iv1, _), Some (iv2, _), Some (iv3, _) =>
             let new_iv := addIntv iv1 (multIntv iv2 iv3) in
             isSupersetIntv new_iv intv
           | _, _, _ => false
           end
         else false
       | Downcast _ f1 =>
         if (validSMTIntervalbounds f1 A P Q validVars)
         then
           match FloverMap.find f1 A with
           | None => false
           | Some (iv1, _) =>
             (isSupersetIntv intv iv1) && (isSupersetIntv iv1 intv)
           end
         else
           false
       end
  end.

Theorem validSMTIntervalbounds_sound (f: expr Q) (A: analysisResult) (P: FloverMap.t intv)
        (Q: FloverMap.t (SMTLogic * SMTLogic)) fVars dVars (E: env) Gamma :
  (forall e loQ hiQ, FloverMap.find e Q = Some (loQ, hiQ) -> ~ eval_smt_logic E loQ /\ ~ eval_smt_logic E hiQ) ->
  validSMTIntervalbounds f A P Q dVars = true ->
  dVars_range_valid dVars E A ->
Joachim Bard's avatar
Joachim Bard committed
130
  NatSet.Subset (usedVars f -- dVars) fVars ->
131 132 133 134
  eval_precond E P ->
  validTypes f Gamma ->
  validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
Joachim Bard's avatar
Joachim Bard committed
135 136 137 138 139 140 141 142 143 144 145 146 147 148 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 178 179 180 181 182 183 184 185 186 187 188 189 190 191 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 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372
  induction f;
    intros unsat_queries valid_bounds valid_definedVars usedVars_subset valid_precond types_defined;
    cbn in *.
  - destruct (NatSet.mem n dVars) eqn:?; cbn in *; split; auto.
    + destruct (valid_definedVars n)
        as [vR [iv_n [err_n [env_valid [map_n bounds_valid]]]]];
        try set_tac.
      rewrite map_n in *.
      kill_trivial_exists.
      eexists; split; [auto| split; try eauto ].
      eapply Var_load; cbn; try auto.
      destruct (types_defined) as [m [find_m _]].
      eapply toRExpMap_some in  find_m; cbn; eauto.
      match_simpl; auto.
    + Flover_compute.
      destruct (valid_precond n i0) as [vR [env_valid bounds_valid]].
      admit.
      assert (NatSet.In n fVars) by set_tac.
      canonize_hyps.
      kill_trivial_exists.
      eexists; split; [auto | split].
      * econstructor; try eauto.
        destruct (types_defined) as [m [find_m _]].
        eapply toRExpMap_some in find_m; cbn; eauto.
        match_simpl; auto.
      * cbn in *. lra.
  - split; [auto |].
    Flover_compute; canonize_hyps; cbn in *.
    kill_trivial_exists.
    exists (perturb (Q2R v) REAL 0).
    split; [eauto| split].
    + econstructor; try eauto.
      cbn. rewrite Rabs_R0; lra.
    + unfold perturb; cbn; lra.
  - Flover_compute; cbn in *; try congruence.
    assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_e.
    { apply IHf; try auto.
      destruct types_defined as [? [? [[? ?] ?]]]; auto. }
    split; try auto.
    apply validRanges_single in valid_e.
    destruct valid_e as [iv_f [err_f [vF [iveq_f [eval_f valid_bounds_f]]]]].
    rewrite Heqo0 in iveq_f; inversion iveq_f; subst.
    inversion iveq_f; subst.
    destruct u; try andb_to_prop R; cbn in *.
    + kill_trivial_exists.
      exists (evalUnop Neg vF); split;
        [auto | split ; [econstructor; eauto | ]].
      * cbn; auto.
      *  canonize_hyps.
         rewrite Q2R_opp in *.
         cbn; lra.
    + rename L0 into nodiv0.
      apply le_neq_bool_to_lt_prop in nodiv0.
      kill_trivial_exists.
      exists (perturb (evalUnop Inv vF) REAL 0); split;
        [destruct i; auto | split].
      * econstructor; eauto.
        { auto. }
        { cbn. rewrite Rabs_R0; lra. }
        (* Absence of division by zero *)
        { hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
               rewrite Q2R0_is_0 in nodiv0; lra. }
      * canonize_hyps. unfold tightenBounds in *. Flover_compute.
        { admit. }
        pose proof (interval_inversion_valid ((Q2R (fst iv_f)),(Q2R (snd iv_f)))
                                             (a :=vF))
          as inv_valid.
         unfold invertInterval in inv_valid; cbn in *.
         destruct inv_valid; try auto.
         { destruct nodiv0; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto. }
         { split; eapply Rle_trans.
           - apply L1.
           - rewrite Q2R_inv; try auto.
             destruct nodiv0; try lra.
             hnf; intros.
             assert (0 < Q2R (snd iv_f))%R.
             { eapply Rlt_le_trans.
               apply Qlt_Rlt in H1.
               rewrite <- Q2R0_is_0.
               apply H1. lra.
             }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3.
             lra.
           - apply H0.
           - rewrite <- Q2R_inv; try auto.
             hnf; intros.
             destruct nodiv0; try lra.
             assert (Q2R (fst iv_f) < 0)%R.
             { rewrite <- Q2R0_is_0.
               apply Qlt_Rlt in H2.
               eapply Rle_lt_trans; try eauto.
               lra. }
             rewrite <- Q2R0_is_0 in H3.
             apply Rlt_Qlt in H3. lra. }
  - destruct types_defined
      as [? [? [[? [? ?]]?]]].
    assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
    repeat split;
      [ intros; subst; Flover_compute; congruence |
                       auto | auto |].
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    Flover_compute; try congruence.
    kill_trivial_exists.
    exists (perturb (evalBinop b vF1 vF2) REAL 0);
      split; [destruct i; auto | ].
    inversion env1; inversion env2; subst.
      destruct b; cbn in *.
    * split;
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; try lra|].
      pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                          (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_add.
      specialize (valid_add vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; cbn in *.
      repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb. lra.
    * split;
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; lra|].
      pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                             (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_sub.
      specialize (valid_sub vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; cbn in *.
      repeat rewrite <- Q2R_opp in *;
        repeat rewrite <- Q2R_plus in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb; lra.
    * split;
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; lra|].
      pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_mul.
      specialize (valid_mul vF1 vF2 valid_f1 valid_f2).
      unfold isSupersetIntv in R.
      andb_to_prop R.
      canonize_hyps; cbn in *.
      repeat rewrite <- Q2R_mult in *;
        rewrite <- Q2R_min4, <- Q2R_max4 in *.
      unfold perturb; lra.
    * andb_to_prop R.
      canonize_hyps.
      apply le_neq_bool_to_lt_prop in L.
      split;
        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
         try rewrite Rabs_R0; cbn; try auto; try lra|].
      (* No division by zero proof *)
      { hnf; intros.
        destruct L as [L | L]; apply Qlt_Rlt in L; rewrite Q2R0_is_0 in L; lra. }
      { pose proof (interval_division_valid (a:=vF1) (b:=vF2)
                                            ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                            (Q2R (fst iv_f2), Q2R (snd iv_f2)))
        as valid_div.
        cbn in *.
        destruct valid_div; try auto.
        - destruct L; rewrite <- Q2R0_is_0; [left | right]; apply Qlt_Rlt; auto.
        - assert (~ (snd iv_f2) == 0).
          { hnf; intros. destruct L; try lra.
            assert (0 < (snd iv_f2)) by (apply Rlt_Qlt; apply Qlt_Rlt in H9; lra).
            lra. }
          assert (~ (fst iv_f2) == 0).
          { hnf; intros; destruct L; try lra.
            assert ((fst iv_f2) < 0) by (apply Rlt_Qlt; apply Qlt_Rlt in H10; lra).
            lra. }
          repeat (rewrite <- Q2R_inv in *; try auto).
          repeat rewrite <- Q2R_mult in *.
          rewrite <- Q2R_min4, <- Q2R_max4 in *.
          unfold perturb.
          lra.
      }
  - destruct types_defined
      as [mG [find_mg [[validt_f1 [validt_f2 [validt_f3 valid_join]]] valid_exec]]].
        assert (validRanges f1 A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
    assert (validRanges f2 A E (toRTMap (toRExpMap Gamma))) as valid_f2
        by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
    assert (validRanges f3 A E (toRTMap (toRExpMap Gamma))) as valid_f3
        by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
    repeat split; try auto.
    apply validRanges_single in valid_f1;
      apply validRanges_single in valid_f2;
      apply validRanges_single in valid_f3.
    destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
    destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
    destruct valid_f3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]].
    Flover_compute; try congruence.
    kill_trivial_exists.
    exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
    inversion env1; inversion env2; inversion env3; subst.
    split; [auto | ].
    * eapply Fma_dist' with (delta := 0%R); eauto; try congruence; cbn;
        try rewrite Rabs_R0; try auto; lra.
    * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
      specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
      remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
      pose proof (interval_addition_valid (Q2R (fst iv_f1),Q2R (snd iv_f1)) (fst iv_f23prod, snd iv_f23prod)) as valid_add.
      rewrite Heqiv_f23prod in valid_add, valid_mul.
      unfold multIntv in valid_add.
      canonize_hyps.
      cbn in *.
      repeat rewrite <- Q2R_mult in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *;
        repeat rewrite <- Q2R_plus in *;
        repeat rewrite <- Q2R_min4, <- Q2R_max4 in *.
      specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
      unfold evalFma, evalBinop, perturb.
      lra.
  - destruct types_defined
      as [mG [find_mG [[validt_f _] _]]].
        assert (validRanges f A E (toRTMap (toRExpMap Gamma))) as valid_f1
        by (Flover_compute; try congruence; apply IHf; auto).
    split; try auto.
    apply validRanges_single in valid_f1.
    destruct valid_f1 as [iv_f [err_f [vF [env_f [eval_f valid_f]]]]].
    Flover_compute.
    inversion env_f; subst.
    kill_trivial_exists.
    exists (perturb vF REAL 0).
    split; [destruct i; try auto |].
    split; [eapply Downcast_dist'; try eauto; cbn; try rewrite Rabs_R0 |];
      try lra; try auto.
    canonize_hyps.
    unfold perturb.
    cbn in *; lra.
373
Abort.