Commit 39dea23e authored by Heiko Becker's avatar Heiko Becker

Fix some comments

parent 3911c0af
......@@ -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.
......
(**
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.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
......
(**
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"]);;
e (REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; real_sub]);;
e (SUBGOAL_TAC "bounds_simplify" `((e1R:real) + e2R) + -- ((e1F + e2F) + (e1F + e2F) * delta2) =
((e1R:real) + -- e1F) + (e2R + -- e2F) + -- ((e1F + e2F) * delta2)` [REAL_ARITH_TAC]);;
e (ASM_SIMP_TAC[]);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `abs (((e1R:real) + --(e1F:real))) + abs (((e2R:real) + --(e2F:real)) + --(((e1F:real) + (e2F:real)) * (delta2:real)))`);;
e (split);;
e (REWRITE_TAC[REAL_ABS_TRIANGLE]);;
e (mp REAL_LE_ADD2);;
e (split THENL [REWRITE_TAC[GSYM real_sub] THEN auto; ALL_TAC]);;
e (mp REAL_LE_TRANS);;
e (EXISTS_TAC `abs (((e2R:real) + --(e2F:real))) + abs (--(((e1F:real) + (e2F:real)) * (delta2:real)))`);;
e (split THENL [REWRITE_TAC [REAL_ABS_TRIANGLE]; ALL_TAC]);;
e (mp REAL_LE_ADD2);;
e (split THENL [REWRITE_TAC[GSYM real_sub] THEN auto; REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_MUL]]);;
e (mp REAL_LE_LMUL);;
e (split THENL [REWRITE_TAC[REAL_ABS_POS]; auto]);;
This source diff could not be displayed because it is too large. You can view the blob instead.
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