Commit 53709bdb authored by Heiko Becker's avatar Heiko Becker

Add more doc, do some cleanup

parent 5c07cdb7
(**
Full Certificate Checker.
This function must be run on the daisy output.
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.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
......@@ -9,11 +11,15 @@ Require Import Daisy.IntervalValidation Daisy.ErrorValidation.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (validIntervalbounds e absenv P) (validErrorbound e absenv).
(**
Soundness proof.
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.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env_ty) (vR:R) (vF:R),
......@@ -22,6 +28,10 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
eval_exp machineEpsilon cenv (toRExp e) vF ->
CertificateChecker e absenv P = true ->
(Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
**)
Proof.
intros cenv vR vF precondValid eval_real eval_float certificate_valid.
unfold CertificateChecker in certificate_valid.
......
(**
Error bound checker and its soundness proof
**)
This file contains the coq implementation of the error bound validator as well as its soundness proof.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
Require Import Coq.micromega.Psatz Coq.Reals.Reals Interval.Interval_tactic.
Require Import Coq.micromega.Psatz Coq.Reals.Reals.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.IntervalArithQ.
Require Import Daisy.ErrorBounds Daisy.IntervalValidation.
(** Error bound validator **)
Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
let (intv, err) := (env e) in
let errPos := Qleb 0 err in
......@@ -33,25 +34,11 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
in andb (andb rec errPos) theVal
end.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
Lemma Qred_eq_frac:
forall q1 q2,
Is_true (Qleb q1 q2) <-> Is_true (Qleb (Qred q1) q2).
Proof.
intros; split; intros.
- apply Is_true_eq_left. apply Is_true_eq_true in H.
unfold Qleb in *; apply Qle_bool_iff. apply Qle_bool_iff in H.
rewrite Qred_correct; auto.
- apply Is_true_eq_left. apply Is_true_eq_true in H. unfold Qleb in *.
rewrite Qle_bool_iff.
rewrite Qle_bool_iff in H.
rewrite Qred_correct in H.
auto.
Qed.
(** Since errors are intervals with 0 as center, we track them as single value since this eases proving upper bounds **)
(**
Since errors are intervals with 0 as center, we encode them as single values.
This lemma enables us to deduce from each run of the validator the invariant
that when it succeeds, the errors must be positive.
**)
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
(iv,err) = absenv e ->
......@@ -81,13 +68,6 @@ Proof.
apply Qle_bool_iff in hyp; apply Qle_Rle in hyp; rewrite Q2R0_is_0 in hyp; auto.
Qed.
Ltac math_hnf := repeat rewrite Rsub_eq_Ropp_Rplus;
repeat rewrite Ropp_plus_distr;
repeat rewrite Rmult_plus_distr_r;
repeat rewrite Rmult_plus_distr_l;
repeat rewrite Ropp_involutive;
repeat rewrite <- Rplus_assoc.
Lemma validErrorboundCorrectConstant:
forall cenv absenv (n:Q) nR nF e nlo nhi (P:precond),
eval_exp 0%R cenv (Const (Q2R n)) nR ->
......@@ -397,6 +377,18 @@ Proof.
repeat rewrite Q2R_minus; auto.
Qed.
(**
Tactic to simplify multiplication bound proof.
Used to obtain similarly shaped terms in every subgoal.
Thus automation can then be applied to solve it
**)
Ltac math_hnf := repeat rewrite Rsub_eq_Ropp_Rplus;
repeat rewrite Ropp_plus_distr;
repeat rewrite Rmult_plus_distr_r;
repeat rewrite Rmult_plus_distr_l;
repeat rewrite Ropp_involutive;
repeat rewrite <- Rplus_assoc.
Lemma validErrorboundCorrectMult cenv absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) (alo ahi e1lo e1hi e2lo e2hi:Q) P :
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e1) nR1 ->
......@@ -1035,7 +1027,12 @@ Proof.
repeat rewrite Q2R_plus; auto.
Qed.
Lemma validErrorbound_sound (e:exp Q):
(**
Soundness theorem for the error bound validator.
Proof is by induction on the expression e.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_sound (e:exp Q):
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR ->
......
......@@ -34,6 +34,9 @@ Arguments mkIntv _ _/.
Arguments ivlo _ /.
Arguments ivhi _ /.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
......
Lemma Qred_eq_frac:
forall q1 q2,
Is_true (Qleb q1 q2) <-> Is_true (Qleb (Qred q1) q2).
Proof.
intros; split; intros.
- apply Is_true_eq_left. apply Is_true_eq_true in H.
unfold Qleb in *; apply Qle_bool_iff. apply Qle_bool_iff in H.
rewrite Qred_correct; auto.
- apply Is_true_eq_left. apply Is_true_eq_true in H. unfold Qleb in *.
rewrite Qle_bool_iff.
rewrite Qle_bool_iff in H.
rewrite Qred_correct in H.
auto.
Qed.
\ No newline at end of file
(**
This file contains the HOL-Light 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.
**)
needs "IntervalValidation.hl";;
needs "ErrorValidation.hl";;
......
(**
This file contains the HOL-Light implementation of the error bound validator as well as its soundness proof.
**)
needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalValidation.hl";;
needs "ErrorBounds.hl";;
(** Error bound validator **)
let validErrorbound = new_recursive_definition exp_REC
`(validErrorbound (Const n) (absenv:analysisResult) =
let (intv, err) = absenv (Const n) in
......@@ -31,6 +35,11 @@ let validErrorbound = new_recursive_definition exp_REC
then ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbsFun (multInterval errIve1 errIve2)) * machineEpsilon) <= err
else F)))`;;
(**
Since errors are intervals with 0 as center, we encode them as single values.
This lemma enables us to deduce from each run of the validator the invariant
that when it succeeds, the errors must be positive.
**)
let err_always_positive = prove (
`!(e:(real)exp) (absenv:analysisResult) (iv:interval) (err:error).
validErrorbound e absenv = T /\
......@@ -1088,6 +1097,11 @@ let validErrorboundCorrectMultiplication = prove (
]
);;
(**
Soundness theorem for the error bound validator.
Proof is by induction on the expression e.
Each case requires the application of one of the soundness lemmata proven before
**)
let validErrorbound_sound = prove (
`!(e:(real)exp) (cenv:env_ty) (absenv:analysisResult) (nR:real) (nF:real) (err:real) (P:precond) (elo:real) (ehi:real).
precondValidForExec P cenv /\
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment