RealRangeValidator.v 4.13 KB
Newer Older
1
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
2
Require Import Flover.Infra.RealSimps Flover.Infra.RationalSimps Flover.Infra.RealRationalProps Flover.Infra.Ltacs Flover.AffineForm.
3
Require Export Flover.IntervalValidation Flover.AffineValidation Flover.RealRangeArith.
4 5 6
Require Export Coq.QArith.QArith.
Require Export Flover.Infra.ExpressionAbbrevs Flover.Commands.

7
Definition RangeValidator e A P dVars:=
8
  if
9
    validIntervalbounds e A P dVars
10
  then true
11
  else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
12 13 14
       | Some _ => true
       | None => false
       end.
15

16
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVars
17
        (E : env) (Gamma : nat -> option mType) :
18
  RangeValidator e A P dVars = true ->
19
  dVars_range_valid dVars E A ->
20
  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
21 22 23
  fVars_P_sound (usedVars e) E P ->
  vars_typed (NatSet.union (usedVars e) dVars) Gamma ->
  validRanges e A E Gamma.
24 25 26
Proof.
  intros.
  unfold RangeValidator in *.
27
  destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
28
  - eapply validIntervalbounds_sound; eauto.
29 30 31 32
    unfold dVars_range_valid; intros; set_tac.
  - (* FIXME
       @Nikita: Start here
    pose (iexpmap := (FloverMap.empty (affine_form Q))).
33 34
    pose (inoise := 1%nat).
    epose (imap := (fun _ : nat => None)).
35
    fold iexpmap inoise imap in H, H1.
36
    destruct (validAffineBounds f A P dVars iexpmap inoise) eqn: Hafcheck;
37 38 39 40
      try congruence.
    clear H.
    destruct p as [exprAfs noise].
    pose proof (validAffineBounds_sound) as sound_affine.
41 42
    assert ((forall e : FloverMap.key,
                (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e iexpmap = Some af) ->
43
                checked_expressions A E Gamma (usedVars f) dVars e iexpmap inoise imap)) as Hchecked
44 45 46
        by (intros e Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
            rewrite FloverMapFacts.P.F.empty_o in Hein;
            congruence).
47
    assert (1 > 0)%nat as Hinoise by omega.
48
    eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
49 50 51 52 53
    assert (NatSet.Subset (usedVars f -- dVars) (usedVars f)) as Hsubset by set_tac.
    assert (affine_fVars_P_sound (usedVars f) E P) as HfVars by exact H2.
    assert (affine_vars_typed (usedVars f  dVars) Gamma) as Hvarstyped
        by exact H3.
    specialize (sound_affine f A P (usedVars f) dVars E Gamma
54
                             exprAfs noise iexpmap inoise imap
55
                             Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars Hvarstyped)
56
      as [map2 [af [vR [aiv [aerr sound_affine]]]]].
57
    destruct sound_affine as [_ [_ [Haiv [Hsup [_ [_ [_ [_ [Hee [Heval _]]]]]]]]]].
58 59 60 61 62 63 64 65 66 67 68 69
    exists aiv, aerr, vR.
    split; try split; try auto.
    apply AffineArith.to_interval_containment in Heval.
    unfold isSupersetIntv in Hsup.
    apply andb_prop in Hsup as [Hsupl Hsupr].
    apply Qle_bool_iff in Hsupl.
    apply Qle_bool_iff in Hsupr.
    apply Qle_Rle in Hsupl.
    apply Qle_Rle in Hsupr.
    rewrite <- to_interval_to_intv in Heval.
    simpl in Heval.
    destruct Heval as [Heval1 Heval2].
70 71
    split; eauto using Rle_trans. *)
Admitted.
72 73 74 75 76 77 78 79 80 81

Definition RangeValidatorCmd e A P dVars:=
  if
    validIntervalboundsCmd e A P dVars
  then true
  else match validAffineBoundsCmd e A P dVars (FloverMap.empty (affine_form Q)) 1 with
       | Some _ => true
       | None => false
       end.

82 83 84
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) dVars
        (E : env) (Gamma : nat -> option mType) fVars outVars:
  RangeValidatorCmd f A P dVars = true ->
85 86 87
  ssa f (NatSet.union fVars dVars) outVars ->
  dVars_range_valid dVars E A ->
  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
88 89 90 91 92 93 94 95 96 97 98
  fVars_P_sound fVars E P ->
  vars_typed (NatSet.union fVars dVars) Gamma ->
  NatSet.Subset (freeVars f -- dVars) fVars ->
  validRangesCmd f A E Gamma.
Proof.
  intros ranges_valid; intros.
  unfold RangeValidatorCmd in ranges_valid.
  destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
  - eapply validIntervalboundsCmd_sound; eauto.
  - (* FIXME *)
Admitted.