CertificateChecker.v 6.92 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.
13

Heiko Becker's avatar
Heiko Becker committed
14
(** Certificate checking function **)
15
Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
16 17 18 19 20 21 22 23 24
           (P:precond) (defVars:FloverMap.t  mType):=
  let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
  match tMap with
  |Succes tMap =>
   if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
   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 29
   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
30
**)
31
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
32
  forall (E1 E2:env),
Heiko Becker's avatar
Heiko Becker committed
33
    (forall v, NatSet.In v (Expressions.usedVars e) ->
34 35
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
36
    CertificateChecker e absenv P defVars = true ->
37 38 39 40 41 42 43 44 45
    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) /\
        eval_expr E1 (toRTMap (toRExpMap Gamma)) (toREval (toRExp e)) vR REAL /\
        eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m /\
        (forall vF m,
            eval_expr E2 (toRExpMap Gamma) (toRExp e) vF m ->
            (Rabs (vR - vF) <= Q2R err))%R.
Heiko Becker's avatar
Heiko Becker committed
46 47 48 49
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
50
Proof.
51
  intros * P_valid certificate_valid.
52
  unfold CertificateChecker in certificate_valid.
53 54 55 56 57
  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. }
58
  rewrite <- andb_lazy_alt in certificate_valid.
59
  andb_to_prop certificate_valid.
60 61
  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
62 63 64
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
65
  assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
66 67
    as affine_dvars_valid.
  { unfold affine_dVars_range_valid.
68
    intros; set_tac. }
69 70 71
  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
  { hnf; intros a in_empty.
    set_tac. }
72 73 74
  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));
75
      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
  exists Gamma; intros approxE1E2.
80 81 82 83 84 85 86 87 88 89 90
  rewrite <- eval_expr_REAL_det_nondet in eval_real.
  assert (forall (e' : expr Rdefinitions.R) (m' : mType),
              exists d, (fun e m => Some 0%R) e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) as Htmp by admit.
  assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
         by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
  pose proof (RoundoffErrorValidator_sound e _ Htmp H approxE1E2 H1 eval_real R
                                          valid_e map_e Hdvars) as Hsound.
  unfold validErrorBounds in Hsound.
  (* destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. *)
  (* exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. *)
Admitted.
91

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

106
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
107
        defVars:
108
  forall (E1 E2:env),
Heiko Becker's avatar
Heiko Becker committed
109
    (forall v, NatSet.In v (freeVars f) ->
110 111
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
112 113 114 115 116 117 118
    CertificateCheckerCmd f absenv P defVars = true ->
    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) /\
    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
    bstep (toRCmd f) E2 (toRExpMap Gamma) vF m /\
119
    (forall vF m,
120
        bstep (toRCmd f) E2 (toRExpMap Gamma)  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 * P_valid 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 139
  apply validSSA_sound in L.
  destruct L as [outVars ssa_f].
140 141 142 143
  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
144
  rename R into validFPRanges.
Heiko Becker's avatar
Heiko Becker committed
145 146 147
  assert (dVars_range_valid NatSet.empty E1 absenv).
  { unfold dVars_range_valid.
    intros; set_tac. }
148 149
  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
    as freeVars_contained by set_tac.
150
  assert (validRangesCmd f absenv E1 (toRTMap (toRExpMap Gamma))) as valid_f.
151
  { eapply RangeValidatorCmd_sound; eauto.
152
    unfold RangeValidatorCmd.
153
    unfold affine_dVars_range_valid; intros.
154
    set_tac. }
155
  pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
156
  destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
Heiko Becker's avatar
Heiko Becker committed
157
  destruct iv as [f_lo f_hi].
158
  edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto; [admit|].
159
  exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
160
Admitted.