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

Start working on supporting let statements. Therefore add environment...

Start working on supporting let statements. Therefore add environment simulation relation and prove preservation by small step semantics for it
parent 473b51a3
......@@ -22,7 +22,7 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
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),
forall (cenv:env) (vR:R) (vF:R),
precondValidForExec P cenv ->
eval_exp 0%R cenv (toRExp e) vR ->
eval_exp (Q2R machineEpsilon) cenv (toRExp e) vF ->
......
(**
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
FIXME: Currently the semantics are stateful. But daisy actually assumes that a variable may not be verwritten?
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
Final return statement
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V
| Nop: cmd V.
(**
Small Step semantics for Daisy language, parametric by evaluation function.
**)
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s env v eps:
eval_exp eps env e v ->
sstep (Let R x e s) env eps s (updEnv x v env)
|ret_s e v eps env:
eval_exp eps env e v ->
sstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
**)
Inductive bstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_b x e s s' env v eps env2:
eval_exp eps env e v ->
bstep s (updEnv x v env) eps s' env2 ->
bstep (Let R x e s) env eps s' env2
|ret_b e v eps env:
eval_exp eps env e v ->
bstep (Ret R e) env eps (Nop R) (updEnv 0 v env).
\ No newline at end of file
(**
Environment library.
Defines the environment type for the Daisy framework and a simulation relation between environments.
FIXME: Would it make sense to differenciate between a parameter environment and a variable environment?
**)
Require Import Coq.Reals.Reals.
Require Import Daisy.Expressions Daisy.Commands.
(**
Define an approximation relation between two environments.
We use this relation for the soundness proofs.
It is necessary to have this relation, since two evaluations of the very same
expression may yield different values for different machine epsilons
(or environments that already only approximate each other)
**)
Inductive approxEnv : R -> env -> R -> env -> Prop :=
|approxRefl eps E: approxEnv eps E eps E
|approxUpd eps1 E1 eps2 E2 t x v1 v2: approxEnv eps1 E1 eps2 E2 ->
eval_exp eps1 E1 t v1 ->
eval_exp eps2 E2 t v2 ->
approxEnv eps1 (updEnv x v1 E1) eps2 (updEnv x v2 E2).
(** TODO: Show small step preservation of sim **)
Lemma small_step_preserves_sim f g E1 E2 E1' E2' eps1 eps2:
approxEnv eps1 E1 eps2 E2 ->
sstep f E1 eps1 g E1' ->
sstep f E2 eps2 g E2' ->
approxEnv eps1 E1' eps2 E2'.
Proof.
intros approxBefore.
induction f; intros stepLet1 stepLet2.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H6.
apply H14.
- inversion stepLet1; inversion stepLet2; subst.
eapply approxUpd.
apply approxBefore.
apply H0.
auto.
- inversion stepLet1.
Qed.
\ No newline at end of file
......@@ -148,7 +148,7 @@ Proof.
eapply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
Lemma mult_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
......@@ -192,7 +192,7 @@ Proof.
apply Rabs_pos.
Qed.
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env_ty) (err1:R) (err2:R):
Lemma div_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:env) (err1:R) (err2:R):
eval_exp 0%R cenv e1 e1R ->
eval_exp (Q2R machineEpsilon) cenv e1 e1F ->
eval_exp 0%R cenv e2 e2R ->
......
......@@ -9,7 +9,7 @@
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.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps.
Require Import Daisy.Infra.Ltacs Daisy.Infra.ExpressionAbbrevs.
Require Import Daisy.Infra.Ltacs Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
Require Import Daisy.IntervalArith Daisy.IntervalArithQ Daisy.ErrorBounds Daisy.IntervalValidation.
(** Error bound validator **)
......@@ -47,6 +47,15 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
in andb (andb rec errPos) theVal
end.
(** Error bound command validator **)
Fixpoint validErrorboundCmd (f:cmd Q) (env:analysisResult) {struct f} : bool :=
match f with
|Let _ x e g => (validErrorbound e env) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))) && validErrorboundCmd g env
|Ret _ e => validErrorbound e env
|Nop _ => true
end.
(**
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
......@@ -1955,3 +1964,29 @@ Proof.
split; apply Is_true_eq_left; auto. }
{ apply Is_true_eq_left; auto. }
Qed.
Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult):
forall cenv envR envF elo ehi err P,
precondValidForExec P cenv ->
bstep (toRCmd f) cenv 0%R (Nop R) envR ->
bstep (toRCmd f) cenv (Q2R RationalSimps.machineEpsilon) (Nop R) envF ->
validErrorboundCmd f absenv = true ->
absenv (Var Q 0%nat) = ((elo,ehi),err) ->
(Rabs ((envR 0%nat) - (envF 0%nat)) <= (Q2R err))%R.
Proof.
induction f.
- intros cenv envR envF elo ehi err P.
intros p_valid eval_real eval_float valid_bounds absenv_res.
simpl in eval_real, eval_float.
inversion eval_real; subst.
inversion eval_float; subst.
eapply IHf.
assert (precondValidForExec P (updEnv n v cenv)) by admit.
apply H.
apply H7.
admit.
admit.
admit.
- admit.
- intros. inversion H0.
Admitted.
......@@ -3,7 +3,7 @@ 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.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps.
Set Implicit Arguments.
(**
Expressions will use binary operators.
......@@ -115,24 +115,24 @@ It is important that variables are not perturbed when loading from an environmen
This is the case, since loading a float value should not increase an additional error.
Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
**)
Inductive eval_exp (eps:R) (env:env_ty) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps env (Var R x) (env x)
Inductive eval_exp (eps:R) (E:env) : (exp R) -> R -> Prop :=
Var_load x: eval_exp eps E (Var R x) (E x)
| Param_acc x delta:
((Rabs delta) <= eps)%R ->
eval_exp eps env (Param R x) (perturb (env x) delta)
eval_exp eps E (Param R x) (perturb (E x) delta)
| Const_dist n delta:
Rle (Rabs delta) eps ->
eval_exp eps env (Const n) (perturb n delta)
| Unop_neg f1 v1: eval_exp eps env f1 v1 -> eval_exp eps env (Unop Neg f1) (evalUnop Neg v1)
eval_exp eps E (Const n) (perturb n delta)
| Unop_neg f1 v1: eval_exp eps E f1 v1 -> eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)
| Unop_inv f1 v1 delta:
Rle (Rabs delta) eps ->
eval_exp eps env f1 v1 ->
eval_exp eps env (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
eval_exp eps E f1 v1 ->
eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
| Binop_dist op f1 f2 v1 v2 delta:
Rle (Rabs delta) eps ->
eval_exp eps env f1 v1 ->
eval_exp eps env f2 v2 ->
eval_exp eps env (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
(**
If |delta| <= 0 then perturb v delta is exactly v.
......@@ -149,10 +149,10 @@ Qed.
(**
Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (env:env_ty):
Lemma meps_0_deterministic (f:exp R) (E:env):
forall v1 v2,
eval_exp R0 env f v1 ->
eval_exp R0 env f v2 ->
eval_exp R0 E f v1 ->
eval_exp R0 E f v2 ->
v1 = v2.
Proof.
induction f; intros v1 v2 eval_v1 eval_v2;
......@@ -170,15 +170,15 @@ Qed.
Helping lemma. Needed in soundness proof.
For each evaluation of using an arbitrary epsilon, we can replace it by
evaluating the subexpressions and then binding the result values to different
variables in the environment.
variables in the Eironment.
This relies on the property that variables are not perturbed as opposed to parameters
**)
Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (cenv:env_ty) (v:R):
(eval_exp eps cenv (Binop b f1 f2) v <->
Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (cE:env) (v:R):
(eval_exp eps cE (Binop b f1 f2) v <->
exists v1 v2,
eval_exp eps cenv f1 v1 /\
eval_exp eps cenv f2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) (Binop b (Var R 1) (Var R 2)) v).
eval_exp eps cE f1 v1 /\
eval_exp eps cE f2 v2 /\
eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cE)) (Binop b (Var R 1) (Var R 2)) v).
Proof.
split.
- intros eval_bin.
......@@ -188,8 +188,8 @@ Proof.
constructor; try auto;
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [v2 [eval_f1 [eval_f2 eval_e_env]]]].
inversion eval_e_env; subst.
destruct exists_val as [v1 [v2 [eval_f1 [eval_f2 eval_e_E]]]].
inversion eval_e_E; subst.
inversion H4; inversion H5; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
......@@ -198,11 +198,11 @@ Qed.
(**
Analogous lemma for unary expressions.
**)
Lemma unary_unfolding (e:exp R) (eps:R) (cenv:env_ty) (v:R):
(eval_exp eps cenv (Unop Inv e) v <->
Lemma unary_unfolding (e:exp R) (eps:R) (cE:env) (v:R):
(eval_exp eps cE (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).
eval_exp eps cE e v1 /\
eval_exp eps (updEnv 1 v1 cE) (Unop Inv (Var R 1)) v).
Proof.
split.
- intros eval_un.
......@@ -212,8 +212,8 @@ Proof.
constructor; try auto.
constructor; auto.
- intros exists_val.
destruct exists_val as [v1 [eval_f1 eval_e_env]].
inversion eval_e_env; subst.
destruct exists_val as [v1 [eval_f1 eval_e_E]].
inversion eval_e_E; subst.
inversion H1; subst.
unfold updEnv in *; simpl in *.
constructor; auto.
......@@ -228,15 +228,15 @@ Inductive bexp (V:Type) : Type :=
(**
Define evaluation of booleans for reals
**)
Inductive bval (eps:R) (env:env_ty) : (bexp R) -> Prop -> Prop :=
Inductive bval (eps:R) (E:env) : (bexp R) -> Prop -> Prop :=
leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps env f1 v1 ->
eval_exp eps env f2 v2 ->
bval eps env (leq f1 f2) (Rle v1 v2)
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
bval eps E (leq f1 f2) (Rle v1 v2)
|less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
eval_exp eps env f1 v1 ->
eval_exp eps env f2 v2 ->
bval eps env (less f1 f2) (Rlt v1 v2).
eval_exp eps E f1 v1 ->
eval_exp eps E f2 v2 ->
bval eps E (less f1 f2) (Rlt v1 v2).
(**
Simplify arithmetic later by making > >= only abbreviations
**)
......
......@@ -46,15 +46,15 @@ Definition precond :Type := nat -> intv.
(**
Abbreviation for the environment types for expression evaluation
**)
Definition env_ty := nat -> R.
Definition env:= nat -> R.
(**
Define environment update function as abbreviation.
**)
Definition updEnv (x:nat) (v: R) (env:env_ty) (y:nat) :R :=
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :R :=
if y =? x
then v
else env y.
else E y.
(**
In the final proof we will assume that the given environment under which the
......@@ -65,7 +65,7 @@ This definition suffices since Daisys expressions are immutable, hence no
variable can be written twice.
This means that a free variable will never be defined in the program text
**)
Definition precondValidForExec (P:nat->intv) (cenv:env_ty) :=
Definition precondValidForExec (P:nat->intv) (cenv:env) :=
forall v:nat,
let (ivlo,ivhi) := P v in
(Q2R ivlo <= cenv v <= Q2R ivhi)%R.
\ No newline at end of file
......@@ -4,15 +4,23 @@ 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 Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith Daisy.Infra.RealSimps.
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs.
Require Import Daisy.Expressions Daisy.Commands Daisy.IntervalArith Daisy.Infra.RealSimps.
Fixpoint toRExp (f:exp Q) :=
match f with
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ v => Var R v
|Param _ v => Param R v
|Const n => Const (Q2R n)
|Unop o f1 => Unop o (toRExp f1)
|Binop o f1 f2 => Binop o (toRExp f1) (toRExp f2)
|Unop o e1 => Unop o (toRExp e1)
|Binop o e1 e2 => Binop o (toRExp e1) (toRExp e2)
end.
Fixpoint toRCmd (f:cmd Q) :=
match f with
|Let _ x e g => Let R x (toRExp e) (toRCmd g)
|Ret _ e => Ret R (toRExp e)
|Nop _ => Nop R
end.
Lemma Q2R0_is_0:
......
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