CertificateChecker.v 6.08 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
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
16
  if (typeCheck e defVars (typeMap defVars e)) then
17 18 19
    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 29 30
  forall (E1 E2:env),
    approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
    (forall v, NatSet.mem v (Expressions.usedVars e) = true ->
31 32
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
33 34 35
    (forall v, (v) mem (usedVars e) = true ->
          exists m : mType,
            defVars v = Some m) ->
36
    CertificateChecker e absenv P defVars = true ->
37 38 39
   exists vR vF m,
    eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
    eval_exp E2 defVars (toRExp e) vF m /\
40 41 42
    (forall vF m,
        eval_exp E2 defVars (toRExp e) vF m ->
        (Rabs (vR - vF) <= Q2R (snd (absenv e))))%R.
Heiko Becker's avatar
Heiko Becker committed
43 44 45 46
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
47
Proof.
48
  intros * approxE1E2 P_valid types_defined certificate_valid.
49
  unfold CertificateChecker in certificate_valid.
50
  rewrite <- andb_lazy_alt in certificate_valid.
51
  andb_to_prop certificate_valid.
52 53 54 55
  env_assert absenv e env_e.
  destruct env_e as [iv [err absenv_eq]].
  destruct iv as [ivlo ivhi].
  rewrite absenv_eq; simpl.
56 57 58 59 60 61 62 63 64 65 66 67
  pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
  hnf in union_empty.
  assert (forall v1, (v1) mem (Expressions.usedVars e  NatSet.empty) = true ->
                exists m0 : mType, defVars v1 = Some m0).
  { intros; eapply types_defined.
    rewrite NatSet.mem_spec in *.
    rewrite <- union_empty; eauto. }
  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
  { hnf; intros a in_empty.
    set_tac. }
  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
  { intros v v_in_empty.
68
    rewrite NatSet.mem_spec in v_in_empty.
69 70
    inversion v_in_empty. }
  edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
71
  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
72
  exists vR; exists vF; exists mF; split; auto.
73
Qed.
74

75
Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
76
  if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
77 78 79 80
  then
    if (validIntervalboundsCmd f absenv P NatSet.empty)
    then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
    else false
81
  else false.
82

83
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
84
  forall (E1 E2:env),
85
    approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
86
    (forall v, NatSet.mem v (freeVars f)= true ->
87 88
          exists vR, E1 v = Some vR /\
                (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
89 90 91
    (forall v, (v) mem (freeVars f) = true ->
          exists m : mType,
            defVars v = Some m) ->
92
    CertificateCheckerCmd f absenv P defVars = true ->
93 94 95
    exists vR vF m,
    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
    bstep (toRCmd f) E2 defVars vF m /\
96 97 98
    (forall vF m,
        bstep (toRCmd f) E2 defVars vF m ->
        (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R).
99 100 101 102 103
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
104
  intros * approxE1E2 P_valid types_defined certificate_valid.
105
  unfold CertificateCheckerCmd in certificate_valid.
106
  repeat rewrite <- andb_lazy_alt in certificate_valid.
107
  andb_to_prop certificate_valid.
108 109
  apply validSSA_sound in R0.
  destruct R0 as [outVars ssa_f].
110 111 112
  env_assert absenv (getRetExp f) env_f.
  destruct env_f as [iv [err absenv_eq]].
  destruct iv as [ivlo ivhi].
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
  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. }
  assert (forall v, (v) mem (NatSet.empty) = true ->
               exists vR : R,
                 E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.
  { intros v v_in_empty.
    set_tac. inversion v_in_empty. }
  assert (forall v, (v) mem (freeVars f  NatSet.empty) = true ->
               exists m : mType, defVars v = Some m) as types_valid.
  { intros v v_mem; apply types_defined.
    set_tac. rewrite NatSet.union_spec in v_mem.
    destruct v_mem; try auto.
    inversion H. }
  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
    as freeVars_contained by set_tac.
  edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
131
  rewrite absenv_eq; simpl.
132 133 134 135 136
  edestruct validErrorboundCmd_gives_eval as [vF [mF eval_float]]; eauto.
  exists vR; exists vF; exists mF; split; try auto.
  split; try auto.
  intros.
  eapply validErrorboundCmd_sound; eauto.
137
Qed.