CertificateChecker.v 4.31 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 12 13
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.

Heiko Becker's avatar
Heiko Becker committed
14
(** Certificate checking function **)
15
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
16
  if (validIntervalbounds e absenv P NatSet.empty)
17
  then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty)
18
  else false.
19

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

Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
62
  if (validIntervalboundsCmd f absenv P NatSet.empty)
63
  then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty)
64
  else false.
65 66

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