SMTValidation.v 17.5 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
(**
    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
17
     Require Export SMTArith2 IntervalArith IntervalArithQ ssaPrgs RealRangeArith.
18

Joachim Bard's avatar
Joachim Bard committed
19
Definition tightenLowerBound (e: expr Q) (lo: Q) (q: SMTLogic) P :=
20 21 22
  match q with
  | AndQ qP (AndQ (LessQ e' (ConstQ v)) TrueQ) => 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
Definition tightenUpperBound (e: expr Q) (hi: Q) (q: SMTLogic) P :=
26 27 28
  match q with
  | AndQ qP (AndQ (LessQ (ConstQ v) e') TrueQ) => 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
Definition tightenBounds (e: expr Q) (iv: intv) (qMap: FloverMap.t (SMTLogic * SMTLogic)) P :=
32 33 34
  match FloverMap.find e qMap with
  | None => iv
  | Some (loQ, hiQ) => (tightenLowerBound e (fst iv) loQ P, tightenUpperBound e (snd iv) hiQ P)
35 36
  end.

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 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 97
(* TODO: debug this ltac *)
Ltac query_simpl :=
  match goal with
  | [ |- context[match ?q with | _ => _ end ]] => fail; destruct q; query_simpl
  | _ => idtac
  end.

Lemma tightenBounds_low_sound E Gamma e v iv qMap P :
  eval_precond E P
  -> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E ql)
  -> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
  -> (Q2R (fst iv) <= v)%R
  -> (Q2R (fst (tightenBounds e iv qMap P)) <= v)%R.
Proof.
  intros prec_valid unsatQ H Hlo.
  unfold tightenBounds.
  destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
  cbn. unfold tightenLowerBound.
  destruct q; auto. cbn.
  destruct q2; auto.
  destruct q2_1; auto.
  destruct e2; auto.
  destruct q2_2; auto.
  remember (checkPre P q1 && smt_expr_eq e1 e) as b eqn: Hchk.
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_max. apply Rmax_lub; auto.
  eapply RangeBound_low_sound; eauto.
  erewrite eval_smt_expr_complete in H; eauto.
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

Lemma tightenBounds_high_sound E Gamma e v iv qMap P :
  eval_precond E P
  -> (forall ql qh, FloverMap.find e qMap = Some (ql, qh) -> ~ eval_smt_logic E qh)
  -> eval_expr E (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) v REAL
  -> (v <= Q2R (snd iv))%R
  -> (v <= Q2R (snd (tightenBounds e iv qMap P)))%R.
Proof.
  intros prec_valid unsatQ H Hlo.
  unfold tightenBounds.
  destruct (FloverMap.find e qMap) as [[q ?]|]; auto.
  cbn. unfold tightenUpperBound.
  destruct s; auto.
  destruct s2; auto.
  destruct s2_1; auto.
  destruct e1; auto.
  destruct s2_2; auto.
  remember (checkPre P s1 && smt_expr_eq e2 e) as b eqn: Hchk.
  destruct b; auto.
  symmetry in Hchk.
  andb_to_prop Hchk.
  rewrite <- Q2R_min. apply Rmin_glb; auto.
  eapply RangeBound_high_sound; eauto.
  erewrite eval_smt_expr_complete in H; eauto.
  rewrite SMTArith2Expr_exact.
  exact H.
Qed.

98 99 100 101 102 103 104 105 106 107 108 109
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
110 111
           | Some new_iv => isSupersetIntv new_iv intv
                                          (* && (Qleb lo hi) *)
112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127
           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
128
                 let new_iv := tightenBounds e (invertIntv iv) Q P in
129 130 131 132 133 134 135 136 137 138 139 140 141
                 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
142
               let new_iv := tightenBounds e (addIntv iv1 iv2) Q P in
143 144
               isSupersetIntv new_iv intv
             | Sub =>
Joachim Bard's avatar
Joachim Bard committed
145
               let new_iv := tightenBounds e (subtractIntv iv1 iv2) Q P in
146 147
               isSupersetIntv new_iv intv
             | Mult =>
Joachim Bard's avatar
Joachim Bard committed
148
               let new_iv := tightenBounds e (multIntv iv1 iv2) Q P in
149 150 151 152 153
               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
154
                 let new_iv := tightenBounds e (divideIntv iv1 iv2) Q P in
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
                 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
191
  NatSet.Subset (usedVars f -- dVars) fVars ->
192 193 194 195
  eval_precond E P ->
  validTypes f Gamma ->
  validRanges f A E (toRTMap (toRExpMap Gamma)).
Proof.
Joachim Bard's avatar
Joachim Bard committed
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
  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.
250 251 252 253 254 255 256
      pose (v := (perturb (evalUnop Inv vF) REAL 0)).
      exists v.
      assert (Heval: eval_expr E (toRTMap (toRExpMap Gamma)) (Unop Inv (toREval (toRExp f))) v REAL).
      { econstructor; eauto.
        - auto.
        - cbn. rewrite Rabs_R0. lra.
        - hnf. destruct nodiv0 as [nodiv0 | nodiv0]; apply Qlt_Rlt in nodiv0;
Joachim Bard's avatar
Joachim Bard committed
257
               rewrite Q2R0_is_0 in nodiv0; lra. }
258 259
       split; [destruct i; auto | split; auto].
      canonize_hyps.
Joachim Bard's avatar
Joachim Bard committed
260 261 262 263 264 265
        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. }
266 267 268 269 270
         { split.
           - eapply Rle_trans; try apply L1.
             apply (@tightenBounds_low_sound E Gamma); auto.
             { intros ql qh F. destruct (unsat_queries _ ql qh F). auto. }
             cbn. rewrite Q2R_inv; auto.
Joachim Bard's avatar
Joachim Bard committed
271 272 273 274 275 276 277 278 279 280 281
             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.
282 283 284 285
           - eapply Rle_trans; try apply R.
             apply (@tightenBounds_high_sound E Gamma); auto.
             { intros ql qh F. destruct (unsat_queries _ ql qh F). auto. }
             cbn. rewrite Q2R_inv; try auto.
Joachim Bard's avatar
Joachim Bard committed
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 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437
             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.
438
Abort.