CertificateChecker.v 3.6 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 9
Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
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
  andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv).
17

Heiko Becker's avatar
Heiko Becker committed
18
(**
Heiko Becker's avatar
Heiko Becker committed
19 20 21 22
   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.
   This property is expressed by the predicate precondValidForExec.
Heiko Becker's avatar
Heiko Becker committed
23
**)
24
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
25 26 27 28
  forall (VarEnv1 VarEnv2 ParamEnv:env) (vR:R) (vF:R),
    approxEnv VarEnv1 absenv VarEnv2 ->
    eval_exp 0%R VarEnv1 ParamEnv P (toRExp e) vR ->
    eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e) vF ->
29
    CertificateChecker e absenv P = true ->
30
    (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
Heiko Becker's avatar
Heiko Becker committed
31 32 33 34
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
35
Proof.
36
  intros VarEnv1 VarEnv2 ParamEnv vR vF approxC1C2 eval_real eval_float certificate_valid.
37
  unfold CertificateChecker in certificate_valid.
38
  andb_to_prop certificate_valid.
39
  assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
40
  destruct H as [iv [err absenv_eq]].
41
  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
42
  destruct H as [ivlo [ ivhi iv_eq]].
43
  subst; rewrite absenv_eq in *; simpl in *.
44 45 46 47 48 49 50 51 52 53 54 55
  eapply (validErrorbound_sound); eauto.
  intros v v_in_empty.
  rewrite NatSet.mem_spec in v_in_empty.
  hnf in v_in_empty.
  inversion v_in_empty.
Qed.

Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
  andb (validIntervalboundsCmd f absenv P NatSet.empty)
       (validErrorboundCmd f absenv).

Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
Heiko Becker's avatar
Heiko Becker committed
56
  forall (VarEnv1 VarEnv2 ParamEnv:env) outVars vR vF,
57 58
    approxEnv VarEnv1 absenv VarEnv2 ->
    ssaPrg Q f NatSet.empty outVars ->
Heiko Becker's avatar
Heiko Becker committed
59 60
    bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) vR ->
    bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) vF ->
61
    CertificateCheckerCmd f absenv P = true ->
Heiko Becker's avatar
Heiko Becker committed
62
    (Rabs (vR - vF) <= Q2R (snd (absenv (Var Q 0))))%R.
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
(**
   The proofs is a simple composition of the soundness proofs for the range
   validator and the error bound validator.
**)
Proof.
  intros VarEnv1 VarEnv2 ParamEnv outVars envR envF
         approxC1C2 ssa_f eval_real eval_float certificate_valid.
  unfold CertificateCheckerCmd in certificate_valid.
  andb_to_prop certificate_valid.
  assert (exists iv err, absenv (Var Q 0) = (iv,err)) by (destruct (absenv (Var Q 0)); repeat eexists).
  destruct H as [iv [err absenv_eq]].
  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
  destruct H as [ivlo [ ivhi iv_eq]].
  subst; rewrite absenv_eq in *; simpl in *.
  eapply (validErrorboundCmd_sound); eauto.
  intros v v_in_empty.
  rewrite NatSet.mem_spec in v_in_empty.
  hnf in v_in_empty.
  inversion v_in_empty.
82
Qed.