CertificateChecker.v 4.47 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
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
8
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
9
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
10

11
Require Export Coq.QArith.QArith.
12
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
13

Heiko Becker's avatar
Heiko Becker committed
14
(** Certificate checking function **)
15 16 17 18 19
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
  if (typeCheck e defVars (typeMap defVars e)) then 
    if (validIntervalbounds e absenv P NatSet.empty)
    then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
    else false
20
  else false.
21

Heiko Becker's avatar
Heiko Becker committed
22
(**
Heiko Becker's avatar
Heiko Becker committed
23 24 25
   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
26
**)
27
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
28
  forall (E1 E2:env) (vR:R) (vF:R) fVars m,
29
    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
30
    (forall v, NatSet.mem v fVars = true ->
31
          exists vR, E1 v = Some vR /\
32
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
33
    NatSet.Subset (Expressions.usedVars e) fVars ->
34 35 36
    eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 ->
    eval_exp E2 defVars (toRExp e) vF m ->
    CertificateChecker e absenv P defVars = true ->
37
    (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
Heiko Becker's avatar
Heiko Becker committed
38 39 40 41
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
42
Proof.
43
  intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid.
44
  unfold CertificateChecker in certificate_valid.
45
  rewrite <- andb_lazy_alt in certificate_valid.
46
  andb_to_prop certificate_valid.
47 48 49 50 51
  env_assert absenv e env_e.
  destruct env_e as [iv [err absenv_eq]].
  destruct iv as [ivlo ivhi].
  rewrite absenv_eq; simpl.
  eapply validErrorbound_sound; eauto.
52 53 54 55
  - hnf. intros a in_diff.
    rewrite NatSet.diff_spec in in_diff.
    apply fVars_subset.
    destruct in_diff; auto.
56
  - intros v v_in_empty.
57 58
    rewrite NatSet.mem_spec in v_in_empty.
    inversion v_in_empty.
59
Qed.
60

61 62 63 64 65
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
  if (typeCheckCmd f defVars (typeMapCmd defVars f))
       then if (validIntervalboundsCmd f absenv P NatSet.empty)
            then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
            else false
66
  else false.
67

68
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
69
  forall (E1 E2:env) outVars vR vF fVars m,
70
    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
71
    (forall v, NatSet.mem v fVars= true ->
72
          exists vR, E1 v = Some vR /\
73
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
74
    NatSet.Subset (Commands.freeVars f) fVars ->
Heiko Becker's avatar
Heiko Becker committed
75
    ssa f fVars outVars ->
76 77 78
    bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 ->
    bstep (toRCmd f) E2 defVars vF m ->
    CertificateCheckerCmd f absenv P defVars = true ->
79
    (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
80 81 82 83 84
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
85
  intros * approxE1E2 P_valid fVars_subset ssa_f eval_real eval_float
86
         certificate_valid.
87
  unfold CertificateCheckerCmd in certificate_valid.
88
  rewrite <- andb_lazy_alt in certificate_valid.
89
  andb_to_prop certificate_valid.
90 91 92 93
  env_assert absenv (getRetExp f) env_f.
  destruct env_f as [iv [err absenv_eq]].
  destruct iv as [ivlo ivhi].
  rewrite absenv_eq; simpl.
94
  eapply (validErrorboundCmd_sound); eauto.
95 96 97 98 99 100
  - instantiate (1 := outVars).
    eapply ssa_equal_set; try eauto.
    hnf.
    intros a; split; intros in_union.
    + rewrite NatSet.union_spec in in_union.
      destruct in_union as [in_fVars | in_empty]; try auto.
101
      inversion in_empty.
102
    + rewrite NatSet.union_spec; auto.
103 104 105 106
  - hnf; intros a in_diff.
    rewrite NatSet.diff_spec in in_diff.
    destruct in_diff.
    apply fVars_subset; auto.
107
  - intros v v_in_empty.
108 109
    rewrite NatSet.mem_spec in v_in_empty.
    inversion v_in_empty.
110
Qed.