RealRangeValidator.v 5.07 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
From Coq
     Require Import Reals.Reals QArith.Qreals.

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

From Coq Require Export QArith.QArith.

From Flover
11
     Require Export IntervalValidation AffineValidation SMTArith SMTValidation RealRangeArith
12
     Infra.ExpressionAbbrevs Commands.
13

14
Definition RangeValidator e A P Qmap dVars :=
15
  if
Heiko Becker's avatar
Heiko Becker committed
16
    validIntervalbounds e A P dVars
17
  then true
18 19
  else validSMTIntervalbounds e A P Qmap dVars.
(*
Heiko Becker's avatar
Heiko Becker committed
20
  else match validAffineBounds e A P dVars (FloverMap.empty (affine_form Q)) 1 with
21 22
       | Some _ => true
       | None => false
23
       end.
24
*)
25

26 27
Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : FloverMap.t intv)
        Qmap dVars (E : env) (Gamma : FloverMap.t mType):
28
  RangeValidator e A P Qmap dVars = true ->
Heiko Becker's avatar
Heiko Becker committed
29
  dVars_range_valid dVars E A ->
30
  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
31
  validTypes e Gamma ->
32
  eval_precond E P ->
33
  unsat_queries E Qmap ->
34
  validRanges e A E (toRTMap (toRExpMap Gamma)).
35 36 37
Proof.
  intros.
  unfold RangeValidator in *.
38
  destruct (validIntervalbounds e A P dVars) eqn: Hivcheck.
39
  - eapply validIntervalbounds_sound; set_tac; eauto.
40
    (* unfold dVars_range_valid; intros; set_tac. *)
41
  - eapply validSMTIntervalbounds_sound; set_tac; eauto.
42
  (*
43
  - pose (iexpmap := (FloverMap.empty (affine_form Q))).
Nikita Zyuzin's avatar
Nikita Zyuzin committed
44 45
    pose (inoise := 1%nat).
    epose (imap := (fun _ : nat => None)).
46
    fold iexpmap inoise imap in H, H1.
47
    destruct (validAffineBounds e A P dVars iexpmap inoise) eqn: Hafcheck;
48 49 50 51
      try congruence.
    clear H.
    destruct p as [exprAfs noise].
    pose proof (validAffineBounds_sound) as sound_affine.
52 53
    assert ((forall e' : FloverMap.key,
                (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
54
                checked_expressions A E Gamma (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
55
        by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
Nikita Zyuzin's avatar
Nikita Zyuzin committed
56 57
            rewrite FloverMapFacts.P.F.empty_o in Hein;
            congruence).
58
    assert (1 > 0)%nat as Hinoise by omega.
Nikita Zyuzin's avatar
Nikita Zyuzin committed
59
    eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
60
    assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
61 62
    assert (fVars_P_sound (usedVars e) E P) as HfVars by exact H3.
    specialize (sound_affine e A P (usedVars e) dVars E Gamma
Nikita Zyuzin's avatar
Nikita Zyuzin committed
63
                             exprAfs noise iexpmap inoise imap
64 65
                             Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars)
      as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
66
*)
67
Qed.
68

69 70 71 72 73
Definition RangeValidatorCmd e A P Qmap dVars:=
  if
    validIntervalboundsCmd e A P dVars
  then true
  else validSMTIntervalboundsCmd e A P Qmap dVars.
74
  (*
75 76 77 78 79 80
  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
81
       end.
82
*)
83

84 85
Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : FloverMap.t intv)
        (Qmap: FloverMap.t (SMTLogic * SMTLogic)) dVars
86
        (E : env) Gamma fVars outVars:
87
  RangeValidatorCmd f A P Qmap dVars = true ->
88 89
  ssa f (NatSet.union fVars dVars) outVars ->
  dVars_range_valid dVars E A ->
90
  affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
91 92
  eval_precond E P ->
  NatSet.Subset (preVars P) fVars ->
93
  NatSet.Subset (freeVars f -- dVars) fVars ->
94
  validTypesCmd f Gamma ->
95
  unsat_queries E Qmap ->
96
  validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
97 98 99 100 101
Proof.
  intros ranges_valid; intros.
  unfold RangeValidatorCmd in ranges_valid.
  destruct (validIntervalboundsCmd f A P dVars) eqn:iv_valid.
  - eapply validIntervalboundsCmd_sound; eauto.
102
  - eapply validSMTIntervalboundsCmd_sound; eauto.
103
(*
104 105 106 107 108 109 110 111 112 113
  - pose (iexpmap := (FloverMap.empty (affine_form Q))).
    pose (inoise := 1%nat).
    epose (imap := (fun _ : nat => None)).
    fold iexpmap inoise imap in ranges_valid, H1.
    destruct (validAffineBoundsCmd f A P dVars iexpmap inoise) eqn: Hafcheck;
      try congruence.
    destruct p as [exprAfs noise].
    pose proof (validAffineBoundsCmd_sound) as sound_affine.
    assert ((forall e' : FloverMap.key,
                (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
114
                checked_expressions A E Gamma fVars dVars e' iexpmap inoise imap)) as Hchecked
115 116 117 118 119
        by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
            rewrite FloverMapFacts.P.F.empty_o in Hein;
            congruence).
    assert (1 > 0)%nat as Hinoise by omega.
    eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
120
    assert (fVars_P_sound fVars E P) as HfVars by exact H2.
121
    specialize (sound_affine f A P fVars dVars outVars E Gamma
122
                             exprAfs noise iexpmap inoise imap
123 124
                             Hchecked Hinoise Himap Hafcheck H H1 H3 HfVars)
      as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
125
*)
126
Qed.