Commit 1f1690ef authored by Heiko Becker's avatar Heiko Becker

Merge branch 'certification' of gitlab.mpi-sws.org:AVA/daisy into certification

parents 12b48b38 e6c4bf29
(**
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
#!/bin/bash
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find . -path ./attic -prune -o -path ./output -prune -o -path ./Infra -prune -o -name "*.v" -print0)
for file in "${arr[@]}"
do
wc -l $file
done
(**
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 /\
......
(*
Daisy output:
[ Info ]
[ Info ] Starting specs preprocessing phase
[ Info ] Finished specs preprocessing phase
[ Info ]
[ Info ]
[ Info ] Starting range-error phase
[ Info ] Machine epsilon 5.9604645E-8
[ Info ] 331.4: [331.4, 331.4], 2.8421709430404007e-14
[ Info ] u: [-100.0, 100.0], 7.105427357601002e-15
[ Info ] (331.4 + u): [231.4, 431.4],6.394884621840902e-14
[ Info ] Finished range-error phase
[ Info ]
[ Info ] Starting info phase
[ Info ] doppler
[ Info ] abs-error: 6.394884621840902e-14, range: [231.4, 431.4],
[ Info ] rel-error: 2.7635629307869066E-16
[ Info ] Finished info phase
[ Info ] time:
[ Info ] info: 8 ms, rangeError: 81 ms, analysis: 14 ms, frontend: 2547 ms,
*)
needs "./AbsoluteError.hl";;
let cst = define `cst:real = (&1657) / (&5)`;;
let cstEps = define
`cstEps:err = realFromNum 28421709430404007 16 14`;;
let u = define `u = 1`;;
let varuEps = define
`varuEps:err = realFromNum 7105427357601002 15 15`;;
let lowerBoundAddUCst = define
`lowerBoundAddUCst = -- (&1157) / (&5)`;;
let upperBoundAddUCst = define
`upperBoundAddUCst = (&2157) / (&5)`;;
let addUCstEps = define
`addUCstEps:err = realFromNum 6394884621840902 15 14`;;
let defaultVal = define
`defaultVal = ((&0,&0),&0)`;;
let absenv = define
`absenv (e:(real)exp) =
if e = Const cst
then ((cst,cst),cstEps)
else
if e = Var u
then ((-- &(100),&100), varuEps)
else
if e = Binop Plus (Const cst) (Var u)
then ((lowerBoundAddUCst,upperBoundAddUCst), addUCstEps)
else defaultVal`;;
let theExp = define
`theExp = Binop Plus (Const cst) (Var u)`;;
let theInvariant = define
`theInvariant (env:num->real) = (IVlo (IntvFromEnv absenv (Var u)) <= env u /\ env u <= IVhi (IntvFromEnv absenv (Var u)))`;;
g `!env vR vF.
theInvariant env /\
eval_exp (&0) env theExp vR /\
eval_exp m_eps env theExp vF ==>
AbsErrExp theExp absenv (ErrFromEnv absenv theExp) /\ abs (vR - vF) <= (ErrFromEnv absenv theExp)`;;
e (intros "!env vR vF;inv_valid eval_real eval_float");;
e (CONJ_TAC);;
e (REWRITE_TAC[theExp; absenv; ErrFromEnv]);;
e (ONCE_REWRITE_TAC [AbsErrExp_CASES]);;
e (REPEAT DISJ2_TAC);;
e (EXISTS_TAC `Plus:binop` THEN EXISTS_TAC `(Const cst):(real)exp` THEN EXISTS_TAC `(Var u):(real)exp`);;
e (CONJ_TAC THEN TRY reflexivity);;
e (COND_CASES_TAC THEN TRY COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Const cst` "exp");;
e (contradiction `Binop Plus (Const cst) (Var u) = Var u` "exp");;
e (REWRITE_TAC[SND]);;
e (REWRITE_TAC[absenv; ErrFromEnv]);;
e (ASM_SIMP_TAC[]);;
e (CONJ_TAC);;
(* NEEDS REAL MACHINE EPSILON, THEN EASY PROOF *)
e (CHEAT_TAC);;
(* SAME HERE *)
e (CHEAT_TAC);;
(* Semantic Validation *)
e (ASM_REWRITE_TAC [absenv; ErrFromEnv; theExp]);;
e (COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Const cst` "exp");;
e (COND_CASES_TAC);;
e (contradiction `Binop Plus (Const cst) (Var u) = Var u` "exp");;
e (REWRITE_TAC [SND; addUCstEps]);;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [theExp]));;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [eval_exp_CASES]));;
e (destruct "eval_real" "varcase| constcase | binopcase");;
e (lcontra "varcase" "exp");;
e (lcontra "constcase" "exp");;
e (destruct "eval_float" "fvarcase | fconstcase| fbinopcase");;
e (lcontra "fvarcase" "exp");;
e (lcontra "fconstcase" "exp");;
e (destruct "binopcase" "@b. @e1. @e2. @v1. @v2. @delta. beq vReq eval_e1 eval_e2 delta_less");;
e (destruct "fbinopcase" "@bf. @fe1. @fe2. @fv1. @fv2. @fdelta. fbeq vFeq eval_fe1 eval_fe2 fdelta_less");;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [injectivity "exp"]));;
e (destruct "beq" "plus_b cst_e1 u_e2");;
e (destruct "fbeq" "plus_fb cst_fe1 u_fe2");;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [perturb]));;
e (SUBGOAL_TAC "delta0" `delta = &0` [ALL_TAC]);;
e (MATCH_MP_TAC abs_leq_0_impl_zero);;
e (ASM_REWRITE_TAC[]);;
e (ASM_REWRITE_TAC[perturb]);;
e (REMOVE_THEN "cst_e1" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "u_e2" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "cst_fe1" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "u_fe2" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "delta0" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])));;
e (USE_THEN "plus_b" (fun th1 -> USE_THEN "plus_fb" (fun th2 -> REWRITE_TAC[SYM th1; SYM th2])));;
e (REMOVE_THEN "plus_b" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "plus_fb" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [SYM th])));;
e (REMOVE_THEN "vReq" (fun th -> ONCE_REWRITE_TAC [th]));;
e (REMOVE_THEN "vFeq" (fun th -> ONCE_REWRITE_TAC [th]));;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [eval_exp_CASES]));;
e (destruct "eval_e1" "varcase| constcase | binopcase");;
e (lcontra "varcase" "exp");;
e (destruct "eval_fe1" "fvarcase | fconstcase| fbinopcase");;
e (lcontra "fvarcase" "exp");;
e (destruct "eval_e2" "varcase2 | constcase2 | binopcase2");;
e (destruct "eval_fe2" "fvarcase2 | fconstcase2 | fbinopcase2");;
e (destruct "constcase" "@n. @delta1. cst_n v1_n delta_0");;
e (destruct "fconstcase" "@nf. @fdelta1. cst_fn v1_fn fdelta_less");;
e (destruct "varcase2" "@v. u_v v2_env");;
e (destruct "fvarcase2" "@vf. u_vf v2f_env");;
e (SUBGOAL_TAC "delta10" `delta1 = &0` [MATCH_MP_TAC abs_leq_0_impl_zero THEN ASM_REWRITE_TAC[]]);;
e (REMOVE_THEN "delta_less" (fun th -> REMOVE_THEN "delta_0" (fun th -> ALL_TAC)));;
e (RULE_ASSUM_TAC (REWRITE_RULE[perturb; injectivity "exp"]));;
e (REMOVE_THEN "delta10" (fun th -> RULE_ASSUM_TAC (ONCE_REWRITE_RULE [th])));;
e (REMOVE_THEN "v2f_env" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "v2_env" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "u_vf" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "u_v" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "v1_fn" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "cst_fn" (fun th -> REWRITE_TAC[SYM th]));;
e (REMOVE_THEN "v1_n" (fun th -> REWRITE_TAC[th]));;
e (REMOVE_THEN "cst_n" (fun th -> REWRITE_TAC[SYM th]));;
e (REWRITE_TAC [eval_binop]);;
e (SUBGOAL_TAC "var_correct" `contained (IntvFromEnv absenv (Var u)) (env u )` [ALL_TAC]);;
e (RULE_ASSUM_TAC (ONCE_REWRITE_RULE [theInvariant]));;
e (destruct "inv_valid" "invlo invhi");;
e (ASM_REWRITE_TAC [contained]);;
e (SUBGOAL_TAC "cst_correct" `contained (IntvFromEnv absenv (Const cst)) (cst)` [ALL_TAC]);;
e (ASM_REWRITE_TAC [contained; IntvFromEnv; absenv; IVlo; IVhi; REAL_LE_REFL]);;
(** TODO **)
(* Show env u contained in absenv (Var u)
then Const cst contained in absenv (Const cst)
finally conclude u + cst in absenv (u + cst)
*)
e (lcontra "fconstcase2" "exp");;
e (lcontra "fbinopcase2" "exp");;
e (lcontra "constcase2" "exp");;
e (lcontra "binopcase2" "exp");;
e (lcontra "fbinopcase" "exp");;
e (lcontra "binopcase" "exp");;
let theThm = top_thm();;
#!/bin/bash
arr=()
while IFS= read -r -d $'\0'; do
arr+=("$REPLY")
done < <(find . -path ./attic -prune -o -path ./output -prune -o -path ./Infra -prune -o -name "*.hl" -print0)
for file in "${arr[@]}"
do
wc -l $file
done
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