Commit f28f4bb9 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'certificates'

Merge some changes to ssa definitions and documentation

See merge request !84
parents ef12f888 da33d515
......@@ -6,28 +6,16 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Infra.NatSet.
(**
Next define what a program is.
Currently no loops, only conditionals and assignments
Final return statement
Currently no loops, or conditionals.
Only assignments and return statement
**)
Inductive cmd (V:Type) :Type :=
Let: nat -> exp V -> cmd V -> cmd V
| Ret: exp V -> cmd V.
(*| Nop: cmd V. *)
(*
UNUSED!
Small Step semantics for Daisy language
Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
let_s x e s E v eps:
eval_exp eps E e v ->
sstep (Let x e s) E eps s (updEnv x v E)
|ret_s e E v eps:
eval_exp eps E e v ->
sstep (Ret e) E eps (Nop R) (updEnv 0 v E).
*)
(**
Analogously define Big Step semantics for the Daisy language
Define big step semantics for the Daisy language, terminating on a "returned"
result value
**)
Inductive bstep : cmd R -> env -> R -> R -> Prop :=
let_b x e s E v eps res:
......@@ -38,12 +26,19 @@ Inductive bstep : cmd R -> env -> R -> R -> Prop :=
eval_exp eps E e v ->
bstep (Ret e) E eps v.
(**
The free variables of a command are all used variables of expressions
without the let bound variables
**)
Fixpoint freeVars V (f:cmd V) :NatSet.t :=
match f with
| Let x e1 g => NatSet.remove x (NatSet.union (Expressions.freeVars e1) (freeVars g))
| Ret e => Expressions.freeVars e
| Let x e g => NatSet.remove x (NatSet.union (usedVars e) (freeVars g))
| Ret e => usedVars e
end.
(**
The defined variables of a command are all let bound variables
**)
Fixpoint definedVars V (f:cmd V) :NatSet.t :=
match f with
| Let x _ g => NatSet.add x (definedVars g)
......
(**
Formalization of the base expression language for the daisy framework
Required in all files, since we will always reason about expressions.
Formalization of the base expression language for the daisy framework
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet.
(**
Expressions will use binary operators.
......@@ -99,12 +98,9 @@ Definition perturb (r:R) (e:R) :=
(**
Define expression evaluation relation parametric by an "error" epsilon.
This value will be used later to express float computations using a perturbation
of the real valued computation by (1 + delta), where |delta| <= machine epsilon.
It is important that variables are not perturbed when loading from an environment.
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
The result value expresses float computations according to the IEEE standard,
using a perturbation of the real valued computation by (1 + delta), where
|delta| <= machine epsilon.
**)
Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
| Var_load x v:
......@@ -126,16 +122,20 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
eval_exp eps E f2 v2 ->
eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
(**
Define the set of "used" variables of an expression to be the set of variables
occuring in it
**)
Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
match e with
| Var _ x => NatSet.singleton x
| Unop u e1 => freeVars e1
| Binop b e1 e2 => NatSet.union (freeVars e1) (freeVars e2)
| Unop u e1 => usedVars e1
| Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
| _ => NatSet.empty
end.
(**
If |delta| <= 0 then perturb v delta is exactly v.
If |delta| <= 0 then perturb v delta is exactly v.
**)
Lemma delta_0_deterministic (v:R) (delta:R):
(Rabs delta <= 0)%R ->
......@@ -172,8 +172,7 @@ 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 Eironment.
This relies on the property that variables are not perturbed as opposed to parameters
variables in the Environment.
**)
Lemma binary_unfolding b f1 f2 eps E vF:
eval_exp eps E (Binop b f1 f2) vF ->
......@@ -218,15 +217,15 @@ Proof.
inversion H2; subst; auto.
Qed.
(**
Using the parametric expressions, define boolean expressions for conditionals
**)
Inductive bexp (V:Type) : Type :=
leq: exp V -> exp V -> bexp V
| less: exp V -> exp V -> bexp V.
(**
Define evaluation of booleans for reals
Define evaluation of boolean expressions
**)
Inductive bval (eps:R) (E:env): (bexp R) -> Prop -> Prop :=
leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
......
......@@ -16,7 +16,6 @@ define them to automatically unfold upon simplification.
**)
Definition interval:Type := R * R.
Definition err:Type := R.
Definition ann:Type := interval * err.
Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
Definition IVlo (intv:interval) := fst intv.
Definition IVhi (intv:interval) := snd intv.
......@@ -36,9 +35,6 @@ 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.
......@@ -50,10 +46,15 @@ Definition precond :Type := nat -> intv.
**)
Definition env := nat -> option R.
(**
The empty environment must return NONE for every variable
**)
Definition emptyEnv:env := fun _ => None.
(**
Define environment update function as abbreviation, for variable environments
**)
Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
if y =? x
then Some v
......
......@@ -2,6 +2,10 @@
Require Import Coq.Bool.Bool Coq.Reals.Reals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.
Ltac iv_assert iv name:=
assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
(** Automatic translation and destruction of conjuctinos with andb into Props **)
Ltac andb_to_prop H :=
apply Is_true_eq_left in H;
......
(**
We define a pseudo SSA predicate.
The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack
http://dblp.org/rec/conf/itp/SchneiderSH15
Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
the program with the predicate with the set of free and defined variables
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals.
Require Import Coq.micromega.Psatz.
Require Import Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
Require Export Daisy.Commands.
Fixpoint validVars (V:Type) (f:exp V) Vs :bool :=
match f with
| Const n => true
| Var _ v => NatSet.mem v Vs
| Unop o f1 => validVars f1 Vs
| Binop o f1 f2 => validVars f1 Vs && validVars f2 Vs
end.
Lemma validVars_subset_freeVars T (e:exp T) V:
validVars e V = true->
NatSet.Subset (Expressions.freeVars e) V.
Proof.
revert V; induction e; simpl; intros V valid_V; try auto.
- rewrite NatSet.mem_spec in valid_V.
hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto.
- hnf; intros a in_empty; inversion in_empty.
- andb_to_prop valid_V.
hnf; intros a in_union.
rewrite NatSet.union_spec in in_union.
destruct in_union as [in_e1 | in_e2].
+ specialize (IHe1 V L a in_e1); auto.
+ specialize (IHe2 V R a in_e2); auto.
Qed.
Lemma validVars_add V (f:exp V) Vs n:
validVars f Vs = true ->
validVars f (NatSet.add n Vs) = true.
Lemma validVars_add V (e:exp V) Vs n:
NatSet.Subset (usedVars e) Vs ->
NatSet.Subset (usedVars e) (NatSet.add n Vs).
Proof.
induction f; try auto.
- intros valid_var. unfold validVars in *; simpl in *.
rewrite NatSet.mem_spec in *.
induction e; try auto.
- intros valid_subset.
hnf. intros a in_singleton.
specialize (valid_subset a in_singleton).
rewrite NatSet.add_spec; right; auto.
- intros vars_binop.
simpl in *.
apply Is_true_eq_left in vars_binop.
apply Is_true_eq_true.
apply andb_prop_intro.
apply andb_prop_elim in vars_binop.
destruct vars_binop; split; apply Is_true_eq_left.
+ apply IHf1. apply Is_true_eq_true; auto.
+ apply IHf2. apply Is_true_eq_true; auto.
Qed.
Lemma validVars_valid_subset (V:Type) (e:exp V) inVars:
validVars e inVars = true ->
NatSet.Subset (Expressions.freeVars e) inVars.
Proof.
induction e; intros vars_valid; unfold validVars in *; simpl in *; try auto.
- rewrite NatSet.mem_spec in vars_valid.
hnf. intros; rewrite NatSet.singleton_spec in *; subst; auto.
- hnf; intros a in_empty; inversion in_empty.
- hnf; intros a in_union; rewrite NatSet.union_spec in in_union.
rewrite andb_true_iff in vars_valid.
destruct vars_valid.
destruct in_union as [in_e1 | in_e2].
+ apply IHe1; auto.
+ apply IHe2; auto.
intros a in_empty.
inversion in_empty.
- simpl; intros in_vars.
intros a in_union.
rewrite NatSet.union_spec in in_union.
destruct in_union.
+ apply IHe1; try auto.
hnf; intros.
apply in_vars.
rewrite NatSet.union_spec; auto.
+ apply IHe2; try auto.
hnf; intros.
apply in_vars.
rewrite NatSet.union_spec; auto.
Qed.
Lemma validVars_non_stuck (e:exp Q) inVars E:
validVars e inVars = true ->
(forall v, NatSet.In v (Expressions.freeVars e) ->
NatSet.Subset (usedVars e) inVars ->
(forall v, NatSet.In v (usedVars e) ->
exists r, E v = Some r)%R ->
exists vR, eval_exp 0 E (toRExp e) vR.
Proof.
......@@ -84,50 +59,38 @@ Proof.
+ exists (evalUnop Neg ve); constructor; auto.
+ exists (perturb (evalUnop Inv ve) 0); constructor; auto.
rewrite Rabs_R0; lra.
- andb_to_prop vars_valid; simpl in *.
- repeat rewrite NatSet.subset_spec in *; simpl in *.
assert (exists vR1, eval_exp 0 E (toRExp e1) vR1) as eval_e1_def.
+ eapply IHe1; eauto.
intros.
destruct (fVars_live v) as [vR E_def]; try eauto.
apply NatSet.union_spec; auto.
+ assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def.
* eapply IHe2; eauto.
intros.
* hnf; intros.
apply vars_valid.
rewrite NatSet.union_spec; auto.
* intros.
destruct (fVars_live v) as [vR E_def]; try eauto.
apply NatSet.union_spec; auto.
+ assert (exists vR2, eval_exp 0 E (toRExp e2) vR2) as eval_e2_def.
* eapply IHe2; eauto.
{ hnf; intros.
apply vars_valid.
rewrite NatSet.union_spec; auto. }
{ intros.
destruct (fVars_live v) as [vR E_def]; try eauto.
apply NatSet.union_spec; auto. }
* destruct eval_e1_def as [vR1 eval_e1_def];
destruct eval_e2_def as [vR2 eval_e2_def].
exists (perturb (evalBinop b vR1 vR2) 0); constructor; auto.
rewrite Rabs_R0; lra.
Qed.
Lemma validVars_equal_set V (e:exp V) vars vars':
NatSet.Equal vars vars' ->
validVars e vars = true ->
validVars e vars' = true.
Proof.
revert vars vars'.
induction e; intros vars vars' eq_set valid_vars; simpl in *; auto.
- rewrite NatSet.mem_spec in *.
rewrite <- eq_set; auto.
- eapply IHe; eauto.
- apply Is_true_eq_true.
apply andb_prop_intro.
andb_to_prop valid_vars.
split; apply Is_true_eq_left.
+ eapply IHe1; eauto.
+ eapply IHe2; eauto.
Qed.
Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
ssaLet x e s inVars Vterm:
validVars e inVars = true->
NatSet.Subset (usedVars e) inVars->
NatSet.mem x inVars = false ->
ssaPrg s (NatSet.add x inVars) Vterm ->
ssaPrg (Let x e s) inVars Vterm
|ssaRet e inVars Vterm:
validVars e inVars = true ->
NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true->
NatSet.Subset (usedVars e) inVars ->
NatSet.Equal inVars Vterm ->
ssaPrg (Ret e) inVars Vterm.
Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
......@@ -135,8 +98,7 @@ Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
NatSet.Subset (Commands.freeVars f) inVars.
Proof.
intros ssa_f; induction ssa_f.
- simpl in *. apply validVars_subset_freeVars in H.
hnf; intros a in_fVars.
- simpl in *. hnf; intros a in_fVars.
rewrite NatSet.remove_spec, NatSet.union_spec in in_fVars.
destruct in_fVars as [in_union not_eq].
destruct in_union; try auto.
......@@ -145,7 +107,6 @@ Proof.
destruct IHssa_f; subst; try auto.
exfalso; apply not_eq; auto.
- hnf; intros.
apply validVars_subset_freeVars in H.
simpl in H1.
apply H; auto.
Qed.
......@@ -159,8 +120,7 @@ Proof.
revert set_eq; revert inVars'.
induction ssa_f.
- constructor.
+ eapply validVars_equal_set; eauto.
symmetry; auto.
+ rewrite set_eq; auto.
+ case_eq (NatSet.mem x inVars'); intros case_mem; try auto.
rewrite NatSet.mem_spec in case_mem.
rewrite set_eq in case_mem.
......@@ -169,20 +129,15 @@ Proof.
+ apply IHssa_f; auto.
apply NatSetProps.Dec.F.add_m; auto.
- constructor.
+ eapply validVars_equal_set; eauto.
symmetry; auto.
+ rewrite NatSet.equal_spec in *.
hnf. intros a; split.
* intros in_primed.
rewrite <- H0. rewrite <- set_eq. auto.
* intros in_rem. rewrite set_eq. rewrite H0; auto.
+ rewrite set_eq; auto.
+ rewrite set_eq; auto.
Qed.
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
match f with
|Let x e g =>
andb (andb (negb (NatSet.mem x inVars)) (validVars e inVars)) (validSSA g (NatSet.add x inVars))
|Ret e => validVars e inVars && (negb (NatSet.mem 0%nat inVars))
andb (andb (negb (NatSet.mem x inVars)) (NatSet.subset (usedVars e) inVars)) (validSSA g (NatSet.add x inVars))
|Ret e => NatSet.subset (usedVars e) inVars
end.
Lemma validSSA_sound f inVars:
......@@ -197,32 +152,14 @@ Proof.
destruct IHf as [outVars IHf].
exists outVars.
constructor; eauto.
rewrite negb_true_iff in L0. auto.
+ rewrite <- NatSet.subset_spec; auto.
+ rewrite negb_true_iff in L0. auto.
- intros inVars validSSA_ret.
simpl in *.
exists (NatSet.add 0%nat inVars).
andb_to_prop validSSA_ret.
exists inVars.
constructor; auto.
rewrite negb_true_iff in R.
hnf in R.
rewrite NatSet.equal_spec.
hnf.
intros a.
rewrite NatSet.remove_spec, NatSet.add_spec.
split.
+ intros in_inVars.
case_eq (a =? 0%nat).
* intros a_zero.
rewrite Nat.eqb_eq in a_zero.
rewrite a_zero in in_inVars.
rewrite <- NatSet.mem_spec in in_inVars.
rewrite in_inVars in R.
inversion R.
* intros a_neq_zero. apply beq_nat_false in a_neq_zero.
split; auto.
+ intros in_add_rem.
destruct in_add_rem as [ [a_zero | a_inVars] a_neq_zero]; try auto.
exfalso; eauto.
+ rewrite <- NatSet.subset_spec; auto.
+ hnf; intros; split; auto.
Qed.
Lemma ssa_shadowing_free x y v v' e f inVars outVars E:
......@@ -301,7 +238,7 @@ Proof.
Qed.
Lemma dummy_bind_ok e v x v' inVars E:
validVars e inVars = true ->
NatSet.Subset (usedVars e) inVars ->
NatSet.mem x inVars = false ->
eval_exp 0 E (toRExp e) v ->
eval_exp 0 (updEnv x v' E) (toRExp e) v.
......@@ -315,7 +252,13 @@ Proof.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
rewrite x_not_free in valid_vars; inversion valid_vars.
hnf in valid_vars.
assert (NatSet.mem x (NatSet.singleton x) = true)
as in_singleton by (rewrite NatSet.mem_spec, NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec in *.
specialize (valid_vars x in_singleton).
rewrite <- NatSet.mem_spec in valid_vars.
rewrite valid_vars in *; congruence.
+ econstructor.
rewrite H; auto.
- inversion eval_e; subst; constructor; auto.
......@@ -323,14 +266,15 @@ Proof.
+ eapply IHe; eauto.
+ eapply IHe; eauto.
- simpl in valid_vars.
apply Is_true_eq_left in valid_vars.
apply andb_prop_elim in valid_vars.
destruct valid_vars.
inversion eval_e; subst; constructor; auto.
+ eapply IHe1; eauto.
apply Is_true_eq_true; auto.
hnf; intros a in_e1.
apply valid_vars;
rewrite NatSet.union_spec; auto.
+ eapply IHe2; eauto.
apply Is_true_eq_true; auto.
hnf; intros a in_e2.
apply valid_vars;
rewrite NatSet.union_spec; auto.
Qed.
Fixpoint exp_subst (e:exp Q) x e_new :=
......@@ -397,7 +341,7 @@ Fixpoint map_subst (f:cmd Q) x e :=
Lemma stepwise_substitution x e v f E vR inVars outVars:
ssaPrg f inVars outVars ->
NatSet.In x inVars ->
validVars e inVars = true ->
NatSet.Subset (usedVars e) inVars ->
eval_exp 0%R E (toRExp e) v ->
bstep (toRCmd f) (updEnv x v E) 0%R vR <->
bstep (toRCmd (map_subst f x e)) E 0%R vR.
......
(**
This file contains some type abbreviations, to ease writing.
**)
open preamble
open realTheory realLib
open realTheory realLib sptreeTheory
val _ = new_theory "abbrevs";
val _ = new_theory "Abbrevs";
(**
For the moment we need only one interval type in HOL, since we do not have the
problem of computability as we have it in Coq
......@@ -10,8 +13,6 @@ val _ = type_abbrev("interval", ``:real#real``);
val IVlo_def = Define `IVlo (iv:interval) = FST iv`;
val IVhi_def = Define `IVhi (iv:interval) = SND iv`;
val _ = type_abbrev("ann", ``:interval#real``);
(**
Later we will argue about program preconditions.
Define a precondition to be a function mapping numbers (resp. variables) to intervals.
......@@ -19,15 +20,25 @@ Define a precondition to be a function mapping numbers (resp. variables) to inte
val _ = type_abbrev ("precond", ``:num->interval``);
(**
Abbreviations for the environment types
Abbreviation for the type of a variable environment, which should be a partial function
**)
val _ = type_abbrev("env",``:num->real option``);
(**
Define environment update function as abbreviation.
The empty environment must return NONE for every variable
**)
val emptyEnv_def = Define `
emptyEnv (x:num) = NONE`;
(**
Define environment update function as abbreviation, for variable environments
**)
val updEnv_def = Define `
updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
(**
Abbreviation for insertion into "num_set" type
**)
val Insert_def = Define `Insert x V = insert x () V`;
val - = export_theory();
......@@ -6,7 +6,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory ErrorValidationTheory
......
......@@ -3,7 +3,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory ExpressionAbbrevsTheory
open AbbrevsTheory ExpressionAbbrevsTheory
val _ = new_theory "Commands";
......
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory ExpressionAbbrevsTheory CommandsTheory
open AbbrevsTheory ExpressionAbbrevsTheory CommandsTheory
val _ = new_theory "Environments";
......
(**
Proofs of general bounds on the error of arithmetic expressions.
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
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
......
......@@ -8,7 +8,7 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
......
open preamble
open expressionsTheory
open ExpressionsTheory
val _ = new_theory "ExpressionAbbrevs"
......
open preamble
open realTheory realLib
open abbrevsTheory