Merge branch 'certificates' of gitlab.mpi-sws.org:AVA/daisy into certificates

coq/Commands.v

@@ -7,8 +7,8 @@ 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: mType -> nat -> exp V -> cmd V -> cmd V
@@ -43,7 +43,8 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
  *)
 
 (**
-  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 -> mType -> Prop :=
   let_b m m1 x e s E v res:
@@ -55,12 +56,19 @@ Inductive bstep : cmd R -> env -> R -> mType -> Prop :=
     eval_exp E e v m ->
     bstep (Ret e) E v m.
 
+(**
+  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 e1 g => NatSet.remove x (NatSet.union (Expressions.usedVars e1) (freeVars g))
+  | Ret e => Expressions.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)

coq/ErrorValidation.v

@@ -141,7 +141,7 @@ Proof.
         apply Rmult_le_compat_r.
         { apply mEps_geq_zero. }
         { rewrite <- maxAbs_impl_RmaxAbs.
-          apply contained_leq_maxAbs_val.
+          apply contained_leq_maxAbs.
           unfold contained; simpl.
           pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
           rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.

coq/Expressions.v

 (**
-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 Import Daisy.Infra.RealRationalProps.
@@ -136,12 +135,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 (E:env) :(exp R) -> R -> mType -> Prop :=
 | Var_load m m1 x v:
@@ -172,17 +168,21 @@ Inductive eval_exp (E:env) :(exp R) -> R -> mType -> Prop :=
     eval_exp E f1 v1 m1 ->
     eval_exp E (Downcast m f1) (perturb v1 delta) m.
 
-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)
-  | Downcast _ e1 => freeVars e1
+  | Unop u e1 => usedVars e1
+  | Binop b e1 e2 => NatSet.union (usedVars e1) (usedVars e2)
+  | Downcast _ e1 => usedVars e1
   | _ => 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 ->
@@ -249,8 +249,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 m E vF:
   eval_exp E (Binop b f1 f2) vF m ->
@@ -302,7 +301,6 @@ Proof.
   (*   auto. *)
 Qed.
 
-
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)
@@ -311,7 +309,7 @@ Inductive bexp (V:Type) : Type :=
 | less: exp V -> exp V -> bexp V.
 
 (**
-  Define evaluation of booleans for reals
+  Define evaluation of boolean expressions
  **)
 (* Inductive bval (E:env): (bexp R) -> Prop -> Prop := *)
 (*   leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R): *)

coq/Infra/Abbrevs.v

@@ -17,7 +17,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.
@@ -37,9 +36,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,6 +46,10 @@ Definition precond :Type := nat -> intv.
   Abbreviation for the type of a variable environment, which should be a partial function
  **)
 Definition env := nat -> option (R * mType).
+
+(**
+  The empty environment must return NONE for every variable
+**)
 Definition emptyEnv:env := fun _ => None.
 
 (**

coq/Infra/Ltacs.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;

coq/ssaPrgs.v

+(**
+  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
-  | Downcast _ f1 => validVars f1 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.
-
-Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
- ssaLet m x e s inVars Vterm:
-   validVars e inVars = true ->
-   NatSet.mem x inVars = false ->
-   ssaPrg s (NatSet.add x inVars) Vterm ->
-   ssaPrg (Let m x e s) inVars Vterm
-|ssaRet e inVars Vterm:
-   validVars e inVars = true ->
-   NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true->
-   ssaPrg (Ret e) inVars Vterm.
-
-
-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 E':env):
-  validVars e inVars = true ->
-  E' = toREvalEnv E ->
-  (forall v, NatSet.In v (Expressions.freeVars e) -> exists r m, E' v = Some (r, m))%R ->
-  exists vR, eval_exp E' (toREval (toRExp e)) vR M0.
+Lemma validVars_non_stuck (e:exp Q) inVars E:
+ NatSet.Subset (usedVars e) inVars ->
+  (forall v, NatSet.In v (usedVars e) ->
+        exists r, (toREvalEnv E) v = Some (r, M0))%R ->
+  exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0.
 Proof.
-  revert inVars E; induction e;
-    intros inVars E vars_valid EnvR fVars_live.
+    revert inVars E; induction e;
+    intros inVars E vars_valid fVars_live.
   - simpl in *.
     assert (NatSet.In n (NatSet.singleton n)) as in_n by (rewrite NatSet.singleton_spec; auto).
     specialize (fVars_live n in_n).
-    destruct fVars_live as [vR [m1 E_def]].
-    rewrite EnvR in E_def.
-    remember (E n) as en.
-    destruct en as [[r mr] | p].
-    + unfold toREvalEnv in E_def.
-      rewrite <- Heqen in E_def.
-      inversion E_def.
-      subst.
-      exists vR.
-      pose proof (isMorePrecise_refl M0).
-      eapply (Var_load (toREvalEnv E) M0 n); eauto.
-      unfold toREvalEnv.
-      rewrite <- Heqen.
-      auto.
-    + unfold toREvalEnv in E_def.
-      rewrite <- Heqen in E_def. 
-      inversion E_def.
+    destruct fVars_live as [vR E_def].
+    exists vR; constructor; auto.
   - exists (perturb (Q2R v) 0); constructor.
-    simpl; rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
-  - assert (exists vR, eval_exp E' (toREval (toRExp e)) vR M0)    
+    simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
+  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0)
       as eval_e_def by (eapply IHe; eauto).
     destruct eval_e_def as [ve eval_e_def].
     case_eq u; intros; subst.
-    + exists (evalUnop Neg ve); econstructor; eauto.
-    + exists (perturb (evalUnop Inv ve) 0); econstructor; eauto.
-      simpl. rewrite Q2R0_is_0. rewrite Rabs_R0; lra.
-  - andb_to_prop vars_valid; simpl in *.
-    assert (exists vR1, eval_exp E' (toREval (toRExp e1)) vR1 M0) as eval_e1_def.
+    + exists (evalUnop Neg ve); constructor; auto.
+    + exists (perturb (evalUnop Inv ve) 0); constructor; auto.
+      simpl (meps M0); rewrite Q2R0_is_0; rewrite Rabs_R0; lra.
+  - repeat rewrite NatSet.subset_spec in *; simpl in *.
+    assert (exists vR1, eval_exp (toREvalEnv E) (toREval (toRExp e1)) vR1 M0) 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 E' (toREval (toRExp e2)) vR2 M0) 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 (toREvalEnv E) (toREval (toRExp e2)) vR2 M0) 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); econstructor; eauto.
         auto. 
         simpl. rewrite Q2R0_is_0. rewrite Rabs_R0; lra.
-  - assert (exists vR, eval_exp E' (toREval (toRExp e))  vR M0) as eval_r_def by (eapply IHe; eauto). 
+  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e))  vR M0) as eval_r_def by (eapply IHe; eauto). 
     destruct eval_r_def as [vr eval_r_def].
     exists vr. 
     simpl toREval.
     auto.
 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.
-  - eapply IHe; eauto.
-Qed.
+Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
+ ssaLet m x e s inVars Vterm:
+   NatSet.Subset (usedVars e) inVars->
+   NatSet.mem x inVars = false ->
+   ssaPrg s (NatSet.add x inVars) Vterm ->
+   ssaPrg (Let m x e s) inVars Vterm
+|ssaRet e inVars Vterm:
+   NatSet.Subset (usedVars e) inVars ->
+   NatSet.Equal inVars Vterm ->
+   ssaPrg (Ret e) inVars Vterm.
+
 
 Lemma ssa_subset_freeVars V (f:cmd V) inVars outVars:
   ssaPrg f 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.
@@ -169,7 +114,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.
@@ -184,8 +128,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.
@@ -194,21 +137,16 @@ 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 m 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:
@@ -223,32 +161,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.
+    + rewrite <- NatSet.subset_spec; auto.