Commit 5f3ea9f0 authored by Heiko Becker's avatar Heiko Becker

Merge with current state of certification branch

parents ca317706 d3c80dca
......@@ -58,6 +58,35 @@ You can then run Daisy on an input file as follows:
$ ./daisy testcases/rosa/Doppler.scala
```
If you want to produce certificates to check them in either of the supported backends,
you have to call Daisy as with
```bash
$ ./daisy file --certificate=coq
```
or
```bash
$ ./daisy file --certificate=hol
```
The certificate can then be found in the folder `coq/output` or `hol/output`.
To check the Coq certificate, you need to enter the coq directory and then run
```bash
$ ./configure_coq.sh
$ make
```
This will compile all coq files and then in the end the certificate in the output directory.
If an additional certificate should be checked later on, it suffices to call the Coq compiler:
```bash
$ coqc -R ./ Daisy output/CERTIFICATE_FILE.v
```
To check the HOL-Light certificates, you need to enter the hol directory and then run
```bash
$ ./configure_hol.sh
$ ocaml output/CERTIFICATE_FILE.hl
```
## Additional Software
Some features of Daisy require additional software to be installed.
......@@ -69,6 +98,13 @@ Currently, this is
* MPFR: Daisy uses a [Java binding](https://github.com/kframework/mpfr-java).
(TODO: figure out whether we used the static or dynamic binding)
* Coq: Version 8.5pl2 if you want to extract certificates for it, [install it](https://coq.inria.fr/download)
* HOL-Light: Git checkout (no later than 1.08.2016) if you want to extract certificates for it, [downloadit](https://github.com/jrh13/hol-light/)
Afterwards configure the environment variable HOLLIGHT_HOME to point to the directory you downloaded HOL-Light into with
```
$ export HOLLIGHT_HOME=path_to_hol_light_git
```
## Documentation
......@@ -82,5 +118,3 @@ directly taken from the Leon project (see the LEON_LICENSE).
Especially the files in frontend, lang, solvers and utils bear more than
a passing resemblance to Leon's code.
Leon version used: 978a08cab28d3aa6414a47997dde5d64b942cd3e
(**
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.
......
(**
Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
......
(**
Error bound checker and its soundness proof
**)
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.
**)
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
match e with
|Var v => false
|Param v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Var _ v => false
|Param _ v => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n => andb errPos (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Binop b e1 e2 =>
let (ive1, err1) := env e1 in
......@@ -32,25 +35,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 ->
......@@ -80,13 +69,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 ->
......@@ -396,6 +378,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 ->
......@@ -1002,38 +996,39 @@ Proof.
lra.
}
- remember (multIntv (widenIntv (e1lo, e1hi) err1) (widenIntv (e2lo, e2hi) err2)) as iv.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
unfold RmaxAbsFun.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; subst; simpl in *.
- rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
- rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
iv_assert iv iv_unf.
destruct iv_unf as [ivl [ivh iv_unf]].
rewrite iv_unf.
rewrite <- maxAbs_impl_RmaxAbs.
assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
rewrite <- H, <- H0.
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e1 e1_real) as valid_bounds_e1.
rewrite absenv_e1 in valid_bounds_e1.
simpl in valid_bounds_e1.
pose proof (distance_gives_iv nR1 nF1 (Q2R err1) (Q2R e1lo, Q2R e1hi) valid_bounds_e1 err1_bounded).
pose proof (validIntervalbounds_sound _ _ _ _ _ p_valid valid_iv_e2 e2_real) as valid_bounds_e2.
rewrite absenv_e2 in valid_bounds_e2.
simpl in valid_bounds_e2.
pose proof (distance_gives_iv nR2 nF2 (Q2R err2) (Q2R e2lo, Q2R e2hi) valid_bounds_e2 err2_bounded).
pose proof (IntervalArith.interval_multiplication_valid _ _ _ _ H1 H2).
unfold IntervalArith.contained in H3.
destruct H3.
unfold RmaxAbsFun.
apply Rmult_le_compat_r.
apply mEps_geq_zero.
apply RmaxAbs; subst; simpl in *.
+ rewrite Q2R_min4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
+ rewrite Q2R_max4.
repeat rewrite Q2R_mult;
repeat rewrite Q2R_minus;
repeat rewrite Q2R_plus; auto.
Qed.
<<<<<<< HEAD
Lemma validErrorboundCorrectDiv 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 ->
......@@ -1137,6 +1132,14 @@ Qed. *)
Admitted.
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):
>>>>>>> certification
forall cenv absenv nR nF err P elo ehi,
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) nR ->
......@@ -1205,7 +1208,7 @@ Proof.
apply andb_prop_intro; split; try auto.
{ apply andb_prop_intro.
split; apply Is_true_eq_left; auto. }
* apply Is_true_eq_left; auto.
{ apply Is_true_eq_left; auto. }
+ eapply (validErrorboundCorrectSubtraction cenv absenv e1 e2); eauto.
simpl.
rewrite absenv_eq, absenv_e1, absenv_e2; simpl.
......
(**
Formalization of the base expression language for the daisy framework
Required in all files, since we will always reason about expressions.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith.
Require Import Daisy.Infra.RealSimps Daisy.Infra.Abbrevs.
......
(**
Some type abbreviations, to ease writing
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
(**
......@@ -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.
......
(**
Some abbreviations that require having defined expressions beforehand
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
......
(**
Some simplification properties of rationals, not proven in the Standard Library
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
Require Import Daisy.Infra.Abbrevs.
......@@ -6,60 +9,17 @@ Definition Qeqb := Qeq_bool.
Definition machineEpsilon := (1#(2^53)).
(*
Definition Qc2Q (q:Qc) :Q := match q with
Qcmake a P => a end.
Definition maxAbs (iv:intv) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Lemma double_inject_eq:
forall q, Qc2Q (Q2Qc q) = Qred q.
Proof.
intros q. unfold Q2Qc.
unfold Qc2Q; auto.
Qed. *)
(*
Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b).
Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *)
Definition maxAbs (iv:intv) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Lemma maxAbs_pointIntv a:
maxAbs (a,a) == Qabs a.
Proof.
unfold maxAbs; simpl.
(* unfold Qcmax.
unfold Qcabs.
apply Qc_is_canon.
apply Qabs_case; intros.
- pose proof (Q.max_id (Qred a)).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive; apply Qeq_refl.
- pose proof (Q.max_id (Qred (-a))).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive.
apply Qeq_refl.
Qed. *)
apply Qabs_case; intros; eapply Q.max_id.
Qed.
(*
Lemma abs_QR (n:Qc):
Rabs (Q2R n) = Q2R (Qcabs n).
Proof.
unfold Rabs.
unfold Qcabs.
apply Qabs_case; intros.
- destruct Rcase_abs.
+ apply Qle_Rle in H.
unfold Q2R at 1 in H.
unfold Qabs.
simpl.
*)
Lemma maxAbs_pointIntv a:
maxAbs (a,a) == Qabs a.
Proof.
unfold maxAbs; simpl.
apply Qabs_case; intros; eapply Q.max_id.
Qed.
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
(a - b = a + (- b))%Q.
Proof.
field_simplify; reflexivity.
......
......@@ -4,7 +4,6 @@ These are used in the soundness proofs since we want to have the final theorem o
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flocq.Core.Fcore_Raux.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
......@@ -162,14 +161,25 @@ Proof.
unfold Q2R, machineEpsilon, RealSimps.machineEpsilon.
unfold RealConstruction.realFromNum, RealConstruction.negativePower.
unfold Qden.
assert (/ (IZR (' (2 ^ 53))) = 1 / (2^53))%R.
- assert (2^53 = ' (2^53))%Z by auto.
assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H0.
f_equal. unfold IZR. rewrite <- Fcore_Raux.P2R_INR.
unfold Fcore_Raux.P2R. simpl; lra.
- rewrite H.
f_equal. simpl; lra.
f_equal.
- unfold IZR. simpl. lra.
- assert ( 1 / (2^53) = / 2^53)%R by lra.
rewrite H.
f_equal.
assert (2^53 = ' (2^53))%Z by auto.
rewrite <- H0.
unfold Z.pow.
rewrite (Zpower_pos_is_exp 52 1).
rewrite mult_IZR.
rewrite (Zpower_pos_is_exp 26 26).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 13 13).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 12 1).
rewrite mult_IZR.
repeat rewrite (Zpower_pos_is_exp 6 6).
repeat rewrite (Zpower_pos_is_exp 3 3).
repeat rewrite mult_IZR. simpl. lra.
Qed.
Lemma mEps_geq_zero:
......
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
Require Import Daisy.Infra.RealConstruction.
(**
TODO REORDER AND DOCUMENT
Some simplification properties of real numbers, not proven in the Standard Library
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
Require Import Daisy.Infra.RealConstruction.
Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
(a - b = a + (- b))%R.
Proof.
......
(**
Formalization of real valued interval arithmetic
TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
Used in soundness proofs for error bound validator.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RealSimps.
......@@ -371,8 +371,8 @@ Proof.
destruct contained_a as [lo_a a_hi].
rewrite Rabs_minus_sym in abs_le.
unfold Rabs in abs_le.
destruct Rcase_abs in abs_le.
- rewrite Ropp_minus_distr in abs_le.
split; lra.
- lra.
destruct Rcase_abs in abs_le.
- rewrite Ropp_minus_distr in abs_le.
split; lra.
- lra.
Qed.
(**
Formalization of real valued intv arithmetic
TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
Formalization of rational valued interval arithmetic
Used in soundness proofs and computations of range validator.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.micromega.Psatz.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps.
......
(**
Interval arithmetic checker and its soundness proof
Explained in section 4 of the paper, used in CertificateChecker.v to build 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.
......
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
#Ignore everything in this directory
*
#apart from this file
!.gitignore
(**
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";;
......
(**
Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
Bounds are explained in section 5, Deriving Computable Error Bounds
**)
needs "Infra/Abbrevs.hl";;
needs "Infra/RealSimps.hl";;
needs "Expressions.hl";;
......
(**
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.
**)
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 +37,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 +1099,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 /\
......
(**
Formalization of the base expression language for the daisy framework
**)