CertificateChecker.v 6.49 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 10
From Flover
     Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
     Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
     Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
11

12
Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
13

Heiko Becker's avatar
Heiko Becker committed
14
(** Certificate checking function **)
15 16 17 18
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
           (P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t nat):=
  let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
  if (typeCheck e defVars tMap fBits)
Heiko Becker's avatar
Heiko Becker committed
19
  then
Heiko Becker's avatar
Heiko Becker committed
20
    if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
21
    then RoundoffErrorValidator e tMap absenv NatSet.empty
22
    else false
23
  else false.
24

Heiko Becker's avatar
Heiko Becker committed
25
(**
Heiko Becker's avatar
Heiko Becker committed
26 27 28
   Soundness proof for the certificate checker.
   Apart from assuming two executions, one in R and one on floats, we assume that
   the real valued execution respects the precondition.
Heiko Becker's avatar
Heiko Becker committed
29
**)
30 31
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
        defVars fBits:
32 33
  forall (E1 E2:env),
    approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
Heiko Becker's avatar
Heiko Becker committed
34
    (forall v, NatSet.In v (Expressions.usedVars e) ->
35 36
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
Heiko Becker's avatar
Heiko Becker committed
37
    (forall v, NatSet.In v  (usedVars e) ->
38 39
          exists m : mType,
            defVars v = Some m) ->
40
    CertificateChecker e absenv P defVars fBits = true ->
Heiko Becker's avatar
Heiko Becker committed
41
    exists iv err vR vF m,
42
      FloverMap.find e absenv = Some (iv, err) /\
43 44
      eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
      eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
Heiko Becker's avatar
Heiko Becker committed
45
      (forall vF m,
46
          eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
Heiko Becker's avatar
Heiko Becker committed
47
          (Rabs (vR - vF) <= Q2R err))%R.
Heiko Becker's avatar
Heiko Becker committed
48 49 50 51
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
52
Proof.
53
  intros * approxE1E2 P_valid types_defined certificate_valid.
54
  unfold CertificateChecker in certificate_valid.
55
  rewrite <- andb_lazy_alt in certificate_valid.
56
  andb_to_prop certificate_valid.
57 58
  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
59 60 61
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
62 63 64 65
  assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
    as affine_dvars_valid.
  { unfold affine_dVars_range_valid.
    intros; set_tac. }
66 67 68
  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
  { hnf; intros a in_empty.
    set_tac. }
Heiko Becker's avatar
Heiko Becker committed
69 70 71
  assert (vars_typed (usedVars e  NatSet.empty) defVars).
  { unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
    split; try auto. hnf; intros; set_tac. }
Heiko Becker's avatar
Heiko Becker committed
72
  rename R into validFPRanges.
73
  assert (validRanges e absenv E1 defVars (toRBMap fBits)) as valid_e.
74 75
  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
      auto. }
76
  pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
77
    destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
Heiko Becker's avatar
Heiko Becker committed
78
  destruct iv_e as [elo ehi].
79
  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
Heiko Becker's avatar
Heiko Becker committed
80
  exists (elo, ehi), err_e, vR, vF, mF; split; auto.
81
Qed.
82

83 84 85 86
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
           defVars fBits:=
  let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
  if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
87
  then
88
    if (RangeValidatorCmd f absenv P NatSet.empty) &&
Heiko Becker's avatar
Heiko Becker committed
89
       FPRangeValidatorCmd f absenv tMap NatSet.empty
90
    then (RoundoffErrorValidatorCmd f tMap absenv NatSet.empty)
91
    else false
92
  else false.
93

94 95
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
        defVars fBits:
96
  forall (E1 E2:env),
97
    approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
Heiko Becker's avatar
Heiko Becker committed
98
    (forall v, NatSet.In v (freeVars f) ->
99 100
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
Heiko Becker's avatar
Heiko Becker committed
101
    (forall v, NatSet.In v (freeVars f) ->
102 103
          exists m : mType,
            defVars v = Some m) ->
104
    CertificateCheckerCmd f absenv P defVars fBits = true ->
Heiko Becker's avatar
Heiko Becker committed
105
    exists iv err vR vF m,
106
      FloverMap.find  (getRetExp f) absenv = Some (iv,err) /\
107 108
    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
    bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
109
    (forall vF m,
110
        bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
Heiko Becker's avatar
Heiko Becker committed
111
        (Rabs (vR - vF) <= Q2R (err))%R).
112 113 114 115 116
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
117
  intros * approxE1E2 P_valid types_defined certificate_valid.
118
  unfold CertificateCheckerCmd in certificate_valid.
119
  repeat rewrite <- andb_lazy_alt in certificate_valid.
120
  andb_to_prop certificate_valid.
121 122
  apply validSSA_sound in R0.
  destruct R0 as [outVars ssa_f].
123 124 125 126
  assert (ssa f (freeVars f  NatSet.empty) outVars) as ssa_valid.
  { eapply ssa_equal_set; try eauto.
    apply NatSetProps.empty_union_2.
    apply NatSet.empty_spec. }
Heiko Becker's avatar
Heiko Becker committed
127
  rename R into validFPRanges.
Heiko Becker's avatar
Heiko Becker committed
128 129 130 131 132 133
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
  assert (vars_typed (freeVars f  NatSet.empty) defVars).
  { unfold vars_typed. intros; apply types_defined. set_tac.
    destruct H0; set_tac. }
134 135
  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
    as freeVars_contained by set_tac.
136
  assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
137 138 139
  { eapply RangeValidatorCmd_sound; eauto.
    unfold affine_dVars_range_valid; intros.
    set_tac. }
140
  pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
141
  destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
Heiko Becker's avatar
Heiko Becker committed
142
  destruct iv as [f_lo f_hi].
143
  edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
Heiko Becker's avatar
Heiko Becker committed
144
  exists (f_lo, f_hi), err, vR, vF, mF; split; try auto.
145
Qed.