CertificateChecker.v 7.48 KB
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
(**
Heiko Becker's avatar
Heiko Becker committed
2 3 4 5
   This file contains the coq implementation of the certificate checker as well as its soundness proof.
   The checker is a composition of the range analysis validator and the error bound validator.
   Running this function on the encoded analysis result gives the desired theorem
   as shown in the soundness theorem.
Heiko Becker's avatar
Heiko Becker committed
6
**)
7 8 9
From Flover
     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
10
     Environments TypeValidator FPRangeValidator ExpressionAbbrevs Commands.
11

12
Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith Flover.SMTArith.
13

Heiko Becker's avatar
Heiko Becker committed
14
(** Certificate checking function **)
15
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
16
           (P: precond) Qmap (defVars:FloverMap.t  mType):=
17 18 19
  let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
  match tMap with
  |Succes tMap =>
20
   if RangeValidator e absenv P Qmap NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
21 22 23 24
   then RoundoffErrorValidator e tMap absenv NatSet.empty
   else false
  | _ => false
  end.
25

Heiko Becker's avatar
Heiko Becker committed
26
(**
Heiko Becker's avatar
Heiko Becker committed
27 28
   Soundness proof for the certificate checker.
   Apart from assuming two executions, one in R and one on floats, we assume that
29
   the real valued execution respects the precondition and dissatisfies the queries.
Heiko Becker's avatar
Heiko Becker committed
30
**)
31
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
32
  forall (E1 E2:env) DeltaMap,
33 34
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
35
    eval_precond E1 P ->
Joachim Bard's avatar
Joachim Bard committed
36
    unsat_queries Qmap ->
37
    CertificateChecker e absenv P Qmap defVars = true ->
38 39 40 41
    exists Gamma,
      approxEnv E1 (toRExpMap Gamma) absenv (usedVars e) NatSet.empty E2 ->
      exists iv err vR vF m,
        FloverMap.find e absenv = Some (iv, err) /\
42 43
        eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) vR REAL /\
        eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m /\
44
        (forall vF m,
45
            eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
46
            (Rabs (vR - vF) <= Q2R err))%R.
Heiko Becker's avatar
Heiko Becker committed
47 48 49 50
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
51
Proof.
52
  intros * deltas_matched P_valid unsat_qs certificate_valid.
53
  unfold CertificateChecker in certificate_valid.
54 55 56 57 58
  destruct (getValidMap defVars e (FloverMap.empty mType)) eqn:?; try congruence.
  rename t into Gamma.
  assert (validTypes e Gamma).
  { eapply getValidMap_top_correct; eauto.
    intros. cbn in *; congruence. }
59
  rewrite <- andb_lazy_alt in certificate_valid.
60
  andb_to_prop certificate_valid.
61 62
  pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
  hnf in union_empty.
Heiko Becker's avatar
Heiko Becker committed
63 64 65
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
66 67
  assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _)
                                   (fun _ => None)) as affine_dvars_valid.
68
  { unfold affine_dVars_range_valid.
69
    intros; set_tac. }
70 71 72
  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
  { hnf; intros a in_empty.
    set_tac. }
73 74 75
  rename R0 into validFPRanges.
  assert (validRanges e absenv E1 (toRTMap (toRExpMap Gamma))) as valid_e.
  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (E:=E1));
76
      eauto. }
77
  pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
78
    destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
Heiko Becker's avatar
Heiko Becker committed
79
  destruct iv_e as [elo ehi].
80
  exists Gamma; intros approxE1E2.
Joachim Bard's avatar
Joachim Bard committed
81
  assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
82
         by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
83
  pose proof (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
84
                                           valid_e map_e Hdvars) as Hsound.
85
  unfold validErrorBounds in Hsound.
86
  eapply validErrorBoundsRec_single in Hsound; eauto.
87
  destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
88
  exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
89
Qed.
90

91
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
92
           (Qmap: FloverMap.t (SMTLogic * SMTLogic)) defVars :=
93 94
  match getValidMapCmd defVars f (FloverMap.empty mType) with
  | Succes Gamma =>
95
    if (validSSA f (preVars P))
96
    then
97
      if (RangeValidatorCmd f absenv P Qmap NatSet.empty) &&
98 99 100
          FPRangeValidatorCmd f absenv Gamma NatSet.empty
      then (RoundoffErrorValidatorCmd f Gamma absenv NatSet.empty)
      else false
101
    else false
102 103
  | _ => false
  end.
104

105
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
106
        defVars DeltaMap:
107
  forall (E1 E2:env),
108 109
    (forall (v : R) (m' : mType),
        exists d : R, DeltaMap v  m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
110
    eval_precond E1 P ->
Joachim Bard's avatar
Joachim Bard committed
111
    unsat_queries Qmap ->
112
    CertificateCheckerCmd f absenv P Qmap defVars = true ->
113 114 115 116
    exists Gamma,
      approxEnv E1 (toRExpMap Gamma) absenv (freeVars f) NatSet.empty E2 ->
      exists iv err vR vF m,
    FloverMap.find  (getRetExp f) absenv = Some (iv,err) /\
117
    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL /\
118
    bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m /\
119
    (forall vF m,
120
        bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m ->
Heiko Becker's avatar
Heiko Becker committed
121
        (Rabs (vR - vF) <= Q2R (err))%R).
122 123 124 125 126
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
127
  intros * deltas_matched P_valid unsat_qs certificate_valid.
128
  unfold CertificateCheckerCmd in certificate_valid.
129 130 131 132 133 134 135
  destruct (getValidMapCmd defVars f (FloverMap.empty mType)) eqn:?;
                           try congruence.
  rename t into Gamma.
  assert (validTypesCmd f Gamma).
  { eapply getValidMapCmd_correct; try eauto.
    intros; cbn in *; congruence. }
  exists Gamma; intros approxE1E2.
136
  repeat rewrite <- andb_lazy_alt in certificate_valid.
137
  andb_to_prop certificate_valid.
138
  pose proof (validSSA_checks_freeVars _ _ L) as sub.
139 140 141
  assert (validSSA f (freeVars f) = true) as ssa_valid
    by (eapply validSSA_downward_closed; eauto; set_tac).
  apply validSSA_sound in ssa_valid as [outVars_small ssa_f_small].
142 143
  apply validSSA_sound in L.
  destruct L as [outVars ssa_f].
144 145
  assert (ssa f (preVars P  NatSet.empty) outVars) as ssa_valid.
  { eapply ssa_equal_set; eauto.
146 147
    apply NatSetProps.empty_union_2.
    apply NatSet.empty_spec. }
Heiko Becker's avatar
Heiko Becker committed
148
  rename R into validFPRanges.
Heiko Becker's avatar
Heiko Becker committed
149 150 151
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
152 153
  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
    as freeVars_contained by set_tac.
154
  assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
155
  { eapply (RangeValidatorCmd_sound _ (fVars:=preVars P)); eauto; intuition.
156 157
    unfold affine_dVars_range_valid; intros.
    set_tac. }
158
  pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
159
  destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
Heiko Becker's avatar
Heiko Becker committed
160
  destruct iv as [f_lo f_hi].
161

162
  pose proof RoundoffErrorValidatorCmd_sound as Hsound.
163
  eapply validErrorBoundsCmdRec_single in Hsound; eauto.
164 165
  - specialize Hsound as ((vF & mF & eval_float) & ?).
    exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
166 167 168
  - eapply ssa_equal_set. 2: exact ssa_f_small.
    apply NatSetProps.empty_union_2.
    apply NatSet.empty_spec.
Joachim Bard's avatar
Joachim Bard committed
169
  - unfold dVars_contained; intros; set_tac.
170
Qed.