Commit ddca2214 authored by Heiko Becker's avatar Heiko Becker
Browse files

Prove soundness of Range validator for unary operators and division

parents b7ef63c0 3eb5483d
......@@ -58,6 +58,8 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
## Checking Interval Arithmetic Certificates
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
```bash
......
(**
This file contains the coq implementation of the error bound validator as well as its soundness proof.
It is explained in section 5 of the paper.
The validator is used in the file CertificateChecker.v to build the complete checker.
This file contains the coq implementation of the error bound validator as well
as its soundness proof. The function validErrorbound is the Error bound
validator from the certificate checking process. Under the assumption that a
valid range arithmetic result has been computed, it can validate error bounds
encoded in the analysis result. The validator is used in the file
CertificateChecker.v to build the complete checker.
**)
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.
......
......@@ -23,13 +23,36 @@ Definition binop_eq_bool (b1:binop) (b2:binop) :=
Next define an evaluation function for binary operators on reals.
Errors are added on the expression evaluation level later.
**)
Fixpoint eval_binop (o:binop) (v1:R) (v2:R) :=
Definition eval_binop (o:binop) (v1:R) (v2:R) :=
match o with
| Plus => Rplus v1 v2
| Sub => Rminus v1 v2
| Mult => Rmult v1 v2
| Div => Rdiv v1 v2
end.
(**
Expressions will use unary operators.
Define them first
**)
Inductive unop: Type := Neg | Inv.
Definition unop_eq_bool (o1:unop) (o2:unop) :=
match o1 with
|Neg => match o2 with |Neg => true |_=> false end
|Inv => match o2 with |Inv => true |_ => false end
end.
(**
Define evaluation for unary operators on reals.
Errors are added on the expression evaluation level later.
**)
Definition eval_unop (o:unop) (v:R):=
match o with
|Neg => (- v)%R
|Inv => (/ v)%R
end .
(**
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
......@@ -41,6 +64,7 @@ Inductive exp (V:Type): Type :=
Var: nat -> exp V
| Param: nat -> exp V
| Const: V -> exp V
| Unop: unop -> exp V -> exp V
| Binop: binop -> exp V -> exp V -> exp V.
......@@ -61,9 +85,14 @@ Fixpoint exp_eq_bool (e1:exp Q) (e2:exp Q) :=
|Const n2 => Qeq_bool n1 n2
| _=> false
end
|Binop b1 e11 e12 =>
|Unop o1 e11 =>
match e2 with
|Unop o2 e22 => andb (unop_eq_bool o1 o2) (exp_eq_bool e11 e22)
|_ => false
end
|Binop o1 e11 e12 =>
match e2 with
|Binop b2 e21 e22 => andb (binop_eq_bool b1 b2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
|Binop o2 e21 e22 => andb (binop_eq_bool o1 o2) (andb (exp_eq_bool e11 e21) (exp_eq_bool e12 e22))
|_ => false
end
end.
......@@ -89,8 +118,13 @@ Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps env (Const n) (perturb n delta)
|Binop_dist op e1 e2 v1 v2 delta:
Rle (Rabs delta) eps ->
(** Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit **)
| Unop_neg e1 v1: eval_exp eps env e1 v1 -> eval_exp eps env (Unop Neg e1) (eval_unop Neg v1)
| Unop_inv e1 v1 delta: Rle (Rabs delta) eps ->
eval_exp eps env e1 v1 ->
eval_exp eps env (Unop Inv e1) (perturb (eval_unop Inv v1) delta)
| Binop_dist op e1 e2 v1 v2 delta:
Rle (Rabs delta) eps ->
eval_exp eps env e1 v1 ->
eval_exp eps env e2 v2 ->
eval_exp eps env (Binop op e1 e2) (perturb (eval_binop op v1 v2) delta).
......@@ -120,11 +154,14 @@ Lemma eval_0_det (e:exp R) (env:env_ty):
v1 = v2.
Proof.
induction e; intros v1 v2 eval_v1 eval_v2;
inversion eval_v1; inversion eval_v2; [ auto | | | ];
repeat try rewrite perturb_0_val; auto.
subst.
rewrite (IHe1 v0 v4); auto.
rewrite (IHe2 v3 v5); auto.
inversion eval_v1; inversion eval_v2; [ auto | | | | | | | ];
repeat try rewrite perturb_0_val; subst; auto.
- rewrite (IHe v0 v3); auto.
- inversion H3.
- inversion H4.
- rewrite (IHe v0 v3); auto.
- rewrite (IHe1 v0 v4); auto.
rewrite (IHe2 v3 v5); auto.
Qed.
(**
......@@ -134,7 +171,7 @@ evaluating the subexpressions and then binding the result values to different
variables in the environment.
This needs the property that variables are not perturbed as opposed to parameters
**)
Lemma existential_rewriting (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
Lemma existential_rewriting_binary (b:binop) (e1:exp R) (e2:exp R) (eps:R) (cenv:env_ty) (v:R):
(eval_exp eps cenv (Binop b e1 e2) v <->
exists v1 v2,
eval_exp eps cenv e1 v1 /\
......@@ -157,6 +194,28 @@ Proof.
constructor; auto.
Qed.
Lemma existential_rewriting_unary (e:exp R) (eps:R) (cenv:env_ty) (v:R):
(eval_exp eps cenv (Unop Inv e) v <->
exists v1,
eval_exp eps cenv e v1 /\
eval_exp eps (updEnv 1 v1 cenv) (Unop Inv (Var R 1)) v).
Proof.
split.
- intros eval_un.
inversion eval_un; subst.
exists v1.
repeat split; try auto.
constructor; try auto.
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [eval_e1 eval_e_env]].
inversion eval_e_env; subst.
inversion H1; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
Qed.
(**
Using the parametric expressions, define boolean expressions for conditionals
**)
......
......@@ -6,12 +6,13 @@ Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Q
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
match e with
Fixpoint toRExp (f:exp Q) :=
match f with
|Var _ v => Var R v
|Param _ v => Param R v
|Const n => Const (Q2R n)
|Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
|Unop o f1 => Unop o (toRExp f1)
|Binop o f1 f2 => Binop o (toRExp f1) (toRExp f2)
end.
Lemma Q2R0_is_0:
......
(**
Interval arithmetic checker and its soundness proof
Explained in section 4 of the paper, used in CertificateChecker.v to build full checker,
Interval arithmetic checker and its soundness proof.
The function validIntervalbounds checks wether the given analysis result is
a valid range arithmetic for each sub term of the given expression e.
The computation is done using our formalized interval arithmetic.
The function is used in CertificateChecker.v to build the full checker.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
......@@ -8,12 +11,13 @@ Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.Interval
Import Lists.List.ListNotations.
Fixpoint freeVars (V:Type) (e:exp V) : list nat:=
match e with
Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
match f with
|Const n => []
|Var _ v => []
|Param _ v => [v]
|Binop b e1 e2 => (freeVars V e1) ++ (freeVars V e2)
|Unop o f1 => freeVars V f1
|Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
......@@ -24,6 +28,23 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
isSupersetIntv (P v) intv
| Const n =>
isSupersetIntv (n,n) intv
| Unop o f1 =>
let rec := validIntervalbounds f1 absenv P in
let (iv1, _) := absenv f1 in
let opres :=
match o with
| Neg =>
let new_iv := negateIntv iv1 in
isSupersetIntv new_iv intv
| Inv =>
let nodiv0 := orb
(andb (Qleb (ivhi iv1) 0) (negb (Qeq_bool (ivhi iv1) 0)))
(andb (Qleb 0 (ivlo iv1)) (negb (Qeq_bool (ivlo iv1) 0))) in
let new_iv := invertIntv iv1 in
andb (isSupersetIntv new_iv intv) nodiv0
end
in
andb rec opres
| Binop b e1 e2 =>
let rec := andb (validIntervalbounds e1 absenv P) (validIntervalbounds e2 absenv P) in
let (iv1,_) := absenv e1 in
......@@ -50,12 +71,12 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
andb rec opres
end.
Theorem ivbounds_approximatesPrecond_sound e absenv P:
validIntervalbounds e absenv P = true ->
forall v, In v (freeVars Q e) ->
Theorem ivbounds_approximatesPrecond_sound f absenv P:
validIntervalbounds f absenv P = true ->
forall v, In v (freeVars Q f) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
Proof.
induction e; unfold validIntervalbounds.
induction f; unfold validIntervalbounds.
- intros approx_true v v_in_fV; simpl in *; contradiction.
- intros approx_true v v_in_fV; simpl in *.
unfold isSupersetIntv.
......@@ -65,19 +86,27 @@ Proof.
destruct i; simpl in *.
apply Is_true_eq_left in approx_true; auto.
- intros approx_true v0 v_in_fV; simpl in *; contradiction.
- intros approx_unary_true v v_in_fV.
unfold freeVars in v_in_fV.
apply Is_true_eq_left in approx_unary_true.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true.
apply IHf; try auto.
apply Is_true_eq_true; auto.
- intros approx_bin_true v v_in_fV.
unfold freeVars in v_in_fV.
apply in_app_or in v_in_fV.
apply Is_true_eq_left in approx_bin_true.
destruct (absenv (Binop b e1 e2)); destruct (absenv e1); destruct (absenv e2); simpl in *.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1); destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H.
destruct H.
destruct v_in_fV as [v_in_fV_e1 | v_in_fV_e2].
+ apply IHe1; auto.
destruct v_in_fV as [v_in_fV_f1 | v_in_fV_f2].
+ apply IHf1; auto.
apply Is_true_eq_true; auto.
+ apply IHe2; auto.
+ apply IHf2; auto.
apply Is_true_eq_true; auto.
Qed.
......@@ -114,38 +143,33 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Theorem validIntervalbounds_sound (e:exp Q):
forall (absenv:analysisResult) (P:precond) cenv vR,
precondValidForExec P cenv ->
validIntervalbounds e absenv P = true ->
eval_exp 0%R cenv (toRExp e) vR ->
(Q2R (fst (fst(absenv e))) <= vR <= Q2R (snd (fst (absenv e))))%R.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
forall vR,
precondValidForExec P cenv ->
validIntervalbounds f absenv P = true ->
eval_exp 0%R cenv (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof.
induction e.
- intros absenv P cenv vR precond_valid valid_bounds eval_e.
induction f.
- intros vR precond_valid valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Var Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
destruct (absenv (Var Q n)); inversion valid_bounds.
- intros absenv P cenv vR precond_valid valid_bounds eval_e.
- intros vR precond_valid valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Param Q n) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
assert (exists intv err, absenv (Param Q n) = (intv,err))
as absenv_n
by (destruct (absenv (Param Q n)); repeat eexists; auto).
destruct absenv_n as [intv [err absenv_n]].
case_eq (absenv (Param Q n)).
intros intv err absenv_n.
rewrite absenv_n in valid_bounds.
unfold precondValidForExec in precond_valid.
specialize (env_approx_p n).
assert (exists ivlo ivhi, P n = (ivlo, ivhi)) as p_n
by (destruct (P n); repeat eexists; auto).
destruct p_n as [ivlo [ivhi p_n]].
case_eq (P n); intros ivlo ivhi p_n.
unfold isSupersetIntv, freeVars in env_approx_p.
assert (In n (n::nil)) by (unfold In; auto).
specialize (env_approx_p H).
assert (In n (n::nil)) as n_in_n by (unfold In; auto).
specialize (env_approx_p n_in_n).
rewrite p_n, absenv_n in env_approx_p.
specialize (precond_valid n); rewrite p_n in precond_valid.
inversion eval_e; subst.
rewrite absenv_n; simpl.
inversion eval_f; subst.
rewrite perturb_0_val; auto.
destruct intv as [abslo abshi]; simpl in *.
apply andb_prop_elim in env_approx_p.
......@@ -162,15 +186,14 @@ Proof.
+ eapply Rle_trans.
apply env_le_ivhi.
apply ivhi_le_abshi.
- intros absenv P cenv vR valid_precond valid_bounds eval_e.
- intros vR valid_precond valid_bounds eval_f.
pose proof (ivbounds_approximatesPrecond_sound (Const v) absenv P valid_bounds) as env_approx_p.
unfold validIntervalbounds in valid_bounds.
destruct (absenv (Const v)) as [intv err].
simpl.
destruct (absenv (Const v)) as [intv err]; simpl.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_lo valid_hi].
inversion eval_e; subst.
inversion eval_f; subst.
rewrite perturb_0_val; auto.
unfold contained; simpl.
split.
......@@ -182,32 +205,128 @@ Proof.
unfold Qleb in *.
apply Qle_bool_iff in valid_hi.
apply Qle_Rle in valid_hi; auto.
- intros absenv P cenv vR valid_precond valid_bounds eval_e;
inversion eval_e; subst.
pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_bounds) as env_approx_p.
rewrite perturb_0_val in eval_e; auto.
- intros vR valid_precond valid_bounds eval_f;
pose proof (ivbounds_approximatesPrecond_sound (Unop u f) absenv P valid_bounds) as env_approx_p.
case_eq (absenv (Unop u f)); intros intv err absenv_unop.
destruct intv as [unop_lo unop_hi]; simpl.
unfold validIntervalbounds in valid_bounds.
rewrite absenv_unop in valid_bounds.
case_eq (absenv f); intros intv_f err_f absenv_f.
rewrite absenv_f in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec.
inversion eval_f; subst.
+ specialize (IHf v1 valid_precond valid_rec H2).
rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop.
apply andb_prop_elim in valid_unop.
destruct valid_unop as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
pose proof (interval_negation_valid (Q2R (fst intv_f),(Q2R (snd intv_f))) v1) as negation_valid.
unfold contained, negateInterval in negation_valid; simpl in *.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct IHf.
unfold eval_unop; split.
* eapply Rle_trans. apply valid_lo.
rewrite Q2R_opp; lra.
* eapply Rle_trans.
Focus 2. apply valid_hi.
rewrite Q2R_opp; lra.
+ specialize (IHf v1 valid_precond valid_rec H3).
rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop.
destruct valid_unop as [valid_unop nodiv0].
(* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop.
apply andb_prop_elim in valid_unop.
destruct valid_unop as [valid_lo valid_hi].
apply Is_true_eq_true in valid_lo; apply Is_true_eq_true in valid_hi.
apply Qle_bool_iff in valid_lo; apply Qle_bool_iff in valid_hi.
assert ((Q2R (ivhi intv_f) < 0)%R \/ (0 < Q2R (ivlo intv_f))%R) as nodiv0_prop.
* apply Is_true_eq_true in nodiv0.
apply le_neq_bool_to_lt_prop in nodiv0.
destruct nodiv0.
{ left; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
{ right; rewrite <- Q2R0_is_0; apply Qlt_Rlt; auto. }
* pose proof (interval_inversion_valid (Q2R (fst intv_f),(Q2R (snd intv_f))) v1) as inv_valid.
unfold contained, invertInterval in inv_valid; simpl in *.
apply Qle_Rle in valid_lo; apply Qle_Rle in valid_hi.
destruct IHf.
rewrite perturb_0_val; auto.
unfold eval_unop, perturb; split.
{ eapply Rle_trans. apply valid_lo.
destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
(* TODO: Extract lemma maybe *)
- assert (0 < - (Q2R (snd intv_f)))%R as negation_pos by lra.
assert (- (Q2R (snd intv_f)) <= - v1)%R as negation_flipped_hi by lra.
apply Rinv_le_contravar in negation_flipped_hi; try auto.
rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
rewrite <- Ropp_inv_permute in negation_flipped_hi; try lra.
apply Ropp_le_contravar in negation_flipped_hi.
repeat rewrite Ropp_involutive in negation_flipped_hi;
rewrite Q2R_inv; auto.
hnf; intros is_0.
rewrite <- Q2R0_is_0 in nodiv0_neg.
apply Rlt_Qlt in nodiv0_neg; lra.
- rewrite Q2R_inv.
apply Rinv_le_contravar; try lra.
hnf; intros is_0.
assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
rewrite <- Q2R0_is_0 in nodiv0_pos.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
}
{ eapply Rle_trans.
Focus 2. apply valid_hi.
destruct nodiv0_prop as [nodiv0_neg | nodiv0_pos].
- assert (Q2R (fst intv_f) < 0)%R as fst_lt_0 by lra.
assert (0 < - (Q2R (fst intv_f)))%R as negation_pos by lra.
assert (- v1 <= - (Q2R (fst intv_f)))%R as negation_flipped_lo by lra.
apply Rinv_le_contravar in negation_flipped_lo; try auto.
rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
rewrite <- Ropp_inv_permute in negation_flipped_lo; try lra.
apply Ropp_le_contravar in negation_flipped_lo.
repeat rewrite Ropp_involutive in negation_flipped_lo;
rewrite Q2R_inv; auto.
hnf; intros is_0.
rewrite <- Q2R0_is_0 in negation_pos.
rewrite <- Q2R_opp in negation_pos.
apply Rlt_Qlt in negation_pos; lra.
assert (0 < - (Q2R (snd intv_f)))%R by lra.
lra.
- rewrite Q2R_inv.
apply Rinv_le_contravar; try lra.
hnf; intros is_0.
assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
rewrite <- Q2R0_is_0 in nodiv0_pos.
apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
}
- intros vR valid_precond valid_bounds eval_f; inversion eval_f; subst.
pose proof (ivbounds_approximatesPrecond_sound (Binop b f1 f2) absenv P valid_bounds) as env_approx_p.
rewrite perturb_0_val in eval_f; auto.
rewrite perturb_0_val; auto.
simpl in valid_bounds.
env_assert absenv (Binop b e1 e2) absenv_bin.
env_assert absenv e1 absenv_e1.
env_assert absenv e2 absenv_e2.
destruct absenv_bin as [iv [err absenv_bin]]; rewrite absenv_bin in valid_bounds; rewrite absenv_bin.
destruct absenv_e1 as [iv1 [err1 absenv_e1]]; rewrite absenv_e1 in valid_bounds.
destruct absenv_e2 as [iv2 [err2 absenv_e2]]; rewrite absenv_e2 in valid_bounds.
case_eq (absenv (Binop b f1 f2)); intros iv err absenv_bin.
case_eq (absenv f1); intros iv1 err1 absenv_f1.
case_eq (absenv f2); intros iv2 err2 absenv_f2.
rewrite absenv_bin, absenv_f1, absenv_f2 in valid_bounds.
apply Is_true_eq_left in valid_bounds.
apply andb_prop_elim in valid_bounds.
destruct valid_bounds as [valid_rec valid_bin].
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
specialize (IHe1 absenv P cenv v1 valid_precond valid_e1 H4);
specialize (IHe2 absenv P cenv v2 valid_precond valid_e2 H5).
rewrite absenv_e1 in IHe1.
rewrite absenv_e2 in IHe2.
specialize (IHf1 v1 valid_precond valid_e1 H4);
specialize (IHf2 v2 valid_precond valid_e2 H5).
rewrite absenv_f1 in IHf1.
rewrite absenv_f2 in IHf2.
destruct b; simpl in *.
+ pose proof (additionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_add.
unfold validIntervalAdd in valid_add.
specialize (valid_add v1 v2 IHe1 IHe2).
specialize (valid_add v1 v2 IHf1 IHf2).
unfold contained in valid_add.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -231,7 +350,7 @@ Proof.
rewrite <- Q2R_max4 in valid_add_hi.
unfold absIvUpd; auto. }
+ pose proof (subtractionIsValid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_sub.
specialize (valid_sub v1 v2 IHe1 IHe2).
specialize (valid_sub v1 v2 IHf1 IHf2).
unfold contained in valid_sub.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -257,7 +376,7 @@ Proof.
rewrite <- Q2R_max4 in valid_sub_hi.
unfold absIvUpd; auto.
+ pose proof (interval_multiplication_valid (Q2R (fst iv1),Q2R (snd iv1)) (Q2R (fst iv2), Q2R (snd iv2))) as valid_mul.
specialize (valid_mul v1 v2 IHe1 IHe2).
specialize (valid_mul v1 v2 IHf1 IHf2).
unfold contained in valid_mul.
unfold isSupersetIntv in valid_bin.
apply andb_prop_elim in valid_bin; destruct valid_bin as [valid_lo valid_hi].
......@@ -331,4 +450,4 @@ Proof.
rewrite <- Q2R_inv in valid_div_hi; [ | auto].
repeat rewrite <- Q2R_mult in valid_div_hi.
rewrite <- Q2R_max4 in valid_div_hi; auto. }
Qed.
\ No newline at end of file
Qed.
(**
This file contains the HOL-Light implementation of the error bound validator as well as its soundness proof.
It is explained in section 5 of the paper.
The validator is used in the file CertificateChecker.hl to build the complete checker.
This file contains the coq implementation of the error bound validator as well
as its soundness proof. The function validErrorbound is the Error bound
validator from the certificate checking process. Under the assumption that a
valid range arithmetic result has been computed, it can validate error bounds
encoded in the analysis result. The validator is used in the file
CertificateChecker.hl to build the complete checker.
**)
needs "Infra/ExpressionAbbrevs.hl";;
needs "IntervalValidation.hl";;
......
(**
Interval arithmetic checker and its soundness proof
Explained in section 4 of the paper, used in CertificateChecker.hl to build full checker,
Interval arithmetic checker and its soundness proof.
The function validIntervalbounds checks wether the given analysis result is
a valid range arithmetic for each sub term of the given expression e.
The computation is done using our formalized interval arithmetic.
The function is used in CertificateChecker.hl to build the full checker.
**)
needs "Infra/tactics.hl";;
needs "Infra/Abbrevs.hl";;
......
e (intros "!e1 e1R e1F e2 e2R e2F vR vF cenv err1 err2; e1_real e1_float e2_real e2_float plus_real plus_float abs_e1 abs_e2");;
e (USE_THEN "plus_real"
(fun th -> LABEL_TAC "plus_real_inv"
(MP (SPECL [`&0:real`;`cenv:num->real`; `Sub:binop`;`e1:(real)exp`; `e2:(real)exp`; `vR:real`] binop_inv) th)));;
e (destruct "plus_real_inv" "@delta. @v1. @v2. vR_eq eval_e1_v1 eval_e2_v2 abs_0");;
e (ASM_SIMP_TAC[]
THEN (USE_THEN "abs_0"
(fun th -> REWRITE_TAC [MP (SPECL [`vR:real`; `delta:real`] perturb_0_val) th])));;
(* FIXME: UGLY REWRITES *)
e (LABEL_TAC "eval_e1_0_det"
(SPECL [`e1:(real)exp`; `v1:real`; `e1R:real`; `cenv:num->real`] eval_0_det));;
e (SUBGOAL_TAC "eval_e1_conj" `eval_exp (&0) cenv e1 v1 /\ eval_exp (&0) cenv e1 e1R` [split THEN auto]);;
e (mp_spec "eval_e1_0_det" "eval_e1_conj");;
e (LABEL_TAC "eval_e2_0_det" (SPECL [`e2:(real)exp`; `v2:real`; `e2R:real`; `cenv:num->real`] eval_0_det));;
e (SUBGOAL_TAC "eval_e2_conj" `eval_exp (&0) cenv e2 v2 /\ eval_exp (&0) cenv e2 e2R` [split THEN auto]);;
e (mp_spec "eval_e2_0_det" "eval_e2_conj");;
e (ASM_SIMP_TAC[eval_binop]);;
e (clear ["eval_e2_0_det"; "eval_e2_conj"; "eval_e1_0_det"; "eval_e1_conj"; "eval_e1_v1"; "eval_e2_v2"]);;
(* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
e (USE_THEN "plus_float"
(fun th -> LABEL_TAC "plus_float_inv"
(MP (SPECL [`machineEpsilon:real`;
`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`;
`Sub:binop`;`(Var 1):(real)exp`; `(Var 2):(real)exp`; `vF:real`] binop_inv) th)));;
e (destruct "plus_float_inv" "@delta2. @v1F. @v2F. vF_eq eval_e1_v1F eval_e2_v2F abs_mEps");;
e (USE_THEN "eval_e1_v1F"
(fun th -> LABEL_TAC "v1F_inv"
(MP (SPECL [`machineEpsilon:real`;
`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`;
`1:num`; `v1F:real`] var_inv) th)));;
e (USE_THEN "eval_e2_v2F"
(fun th -> LABEL_TAC "v2F_inv"
(MP (SPECL [`machineEpsilon:real`;
`(updEnv:num->real->(num->real)->num->real) 2 (e2F:real)
((updEnv:num->real->(num->real)->num->real) 1 (e1F:real)
(cenv:num->real))`;
`2:num`; `v2F:real`] var_inv) th)));;
e (ASM_REWRITE_TAC[updEnv; eval_binop; perturb]);;
(* TODO: Find out how to evaluate the conditional here! *)
e (SUBGOAL_TAC "1_neq_2" `1:num = 2:num <=> F` [ARITH_TAC]);;
e (ASM_REWRITE_TAC[]);;
(* We have now obtained all necessary values from the evaluations --> remove them for readability *)
e (clear ["1_neq_2"; "v2F_inv"; "v1F_inv"; "eval_e2_v2F"; "eval_e1_v1F"; "vF_eq"; "vR_eq"; "e1_real"; "e2_real"; "plus_real"; "plus_float"]);;