Ported lemma of ErrorValidation

coq/ErrorBounds.v

@@ -8,7 +8,7 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSim
 Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType):
-  eval_exp E1 (Const m n) nR M0 ->
+  eval_exp E1 (Const M0 n) nR M0 ->
   eval_exp E2 (Const m n) nF m ->
   (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
 Proof.
@@ -45,13 +45,13 @@ Qed.
 *)
 
 Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m:mType):
+      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType):
   eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
-  eval_exp E2 (toRExp e1) e1F m->
+  eval_exp E2 (toRExp e1) e1F m1->
   eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
-  eval_exp E2 (toRExp e2) e2F m ->
+  eval_exp E2 (toRExp e2) e2F m2 ->
   eval_exp E1 (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Plus (Var R m 1) (Var R m 2)) vF m->
+  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Plus (Var R m1 1) (Var R m2 2)) vF m->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
@@ -59,8 +59,8 @@ Proof.
   intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion plus_real; subst;
-    assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
-    assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
+    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
+    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
       simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in plus_real; auto.
   rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
@@ -76,9 +76,9 @@ Proof.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
   unfold updEnv; simpl.
-  unfold updEnv in H9,H6; simpl in *.
-  symmetry in H9, H6.
-  inversion H9; inversion H6; subst.
+  unfold updEnv in H6,H9; simpl in *.
+  symmetry in H6,H9.
+  inversion H6; inversion H9; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear plus_float H7 H8 plus_real e1_real e1_float e2_real e2_float H9 H6.
   repeat rewrite Rmult_plus_distr_l.
@@ -111,13 +111,13 @@ Qed.
   Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
 **)
 Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
-      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m:mType):
+      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType):
   eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
-  eval_exp E2 (toRExp e1) e1F m ->
+  eval_exp E2 (toRExp e1) e1F m1 ->
   eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
-  eval_exp E2 (toRExp e2) e2F m ->
+  eval_exp E2 (toRExp e2) e2F m2 ->
   eval_exp E1 (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Sub (Var R m 1) (Var R m 2)) vF m ->
+  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Sub (Var R m1 1) (Var R m2 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R.
@@ -125,8 +125,8 @@ Proof.
   intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
   (* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
   inversion sub_real; subst;
-    assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
-    assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
+    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
+    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
       simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in sub_real; auto.
   rewrite delta_0_deterministic; auto.
@@ -142,11 +142,11 @@ Proof.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
   unfold updEnv; simpl.
-  symmetry in H9, H6.
-  unfold updEnv in H9, H6; simpl in H9, H6.
-  inversion H9; inversion H6; subst.
+  symmetry in H6, H9.
+  unfold updEnv in H6, H9; simpl in H6, H9.
+  inversion H6; inversion H9; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H9 H6.
+  clear sub_float H7 H8 sub_real e1_real e1_float e2_real e2_float H6 H9.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -170,20 +170,20 @@ Proof.
 Qed.
 
 Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (m:mType):
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
   eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
-  eval_exp E2 (toRExp e1) e1F m ->
+  eval_exp E2 (toRExp e1) e1F m1 ->
   eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
-  eval_exp E2 (toRExp e2) e2F m ->
+  eval_exp E2 (toRExp e2) e2F m2 ->
   eval_exp E1 (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Mult (Var R m 1) (Var R m 2)) vF m->
+  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Mult (Var R m1 1) (Var R m2 2)) vF m->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion mult_real; subst;
-    assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
-    assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
+    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
+    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
       simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in mult_real; auto.
   rewrite delta_0_deterministic; auto.
@@ -198,11 +198,11 @@ Proof.
   inversion mult_float; subst.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
-  symmetry in H9, H6;
+  symmetry in H6, H9;
     unfold updEnv in *; simpl in *.
-  inversion H9; inversion H6; subst.
+  inversion H6; inversion H9; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H9 H6.
+  clear mult_float H7 H8 mult_real e1_real e1_float e2_real e2_float H6 H9.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
@@ -220,20 +220,20 @@ Proof.
 Qed.
 
 Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (m:mType):
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType):
   eval_exp E1 (toREval (toRExp e1)) e1R M0 ->
-  eval_exp E2 (toRExp e1) e1F m ->
+  eval_exp E2 (toRExp e1) e1F m1 ->
   eval_exp E1 (toREval (toRExp e2)) e2R M0 ->
-  eval_exp E2 (toRExp e2) e2F m ->
+  eval_exp E2 (toRExp e2) e2F m2 ->
   eval_exp E1 (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m e2F (updEnv 1 m e1F emptyEnv)) (Binop Div (Var R m 1) (Var R m 2)) vF m ->
+  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) (Binop Div (Var R m1 1) (Var R m2 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
   (* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
   inversion div_real; subst;
-    assert (m1 = M0) by (apply (ifM0isJoin_l M0 m1 m2); auto);
-    assert (m2 = M0) by (apply (ifM0isJoin_r M0 m1 m2); auto); subst;
+    assert (m3 = M0) by (apply (ifM0isJoin_l M0 m3 m4); auto);
+    assert (m4 = M0) by (apply (ifM0isJoin_r M0 m3 m4); auto); subst;
       simpl (meps M0) in H3; rewrite Q2R0_is_0 in H3; auto.
   rewrite delta_0_deterministic in div_real; auto.
   rewrite delta_0_deterministic; auto.
@@ -248,11 +248,11 @@ Proof.
   inversion div_float; subst.
   unfold perturb; simpl.
   inversion H7; subst; inversion H8; subst.
-  symmetry in H9, H6;
+  symmetry in H6, H9;
     unfold updEnv in *; simpl in *.
-  inversion H9; inversion H6; subst.
+  inversion H6; inversion H9; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H9 H6.
+  clear div_float H7 H8 div_real e1_real e1_float e2_real e2_float H6 H9.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.

coq/Expressions.v

@@ -129,7 +129,7 @@ Fixpoint expEqBool (e1:exp Q) (e2:exp Q) :=
       
 
 
-    Lemma expEqBool_refl e:
+Lemma expEqBool_refl e:
   expEqBool e e = true.
 Proof.
   induction e; apply andb_true_iff; split; simpl in *; auto; try (apply EquivEqBoolEq; auto). 
@@ -220,10 +220,10 @@ 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:
-    isMorePrecise m m1 = true ->
+| Var_load m x v:
+    (** isMorePrecise m m1 = true ->**)
     (**mTypeEqBool m m1 = true ->*)
-    E x = Some (v, m1) ->
+    E x = Some (v, m) ->
     eval_exp E (Var R m x) v m
 | Const_dist m n delta:
     Rle (Rabs delta) (Q2R (meps m)) ->
@@ -284,7 +284,7 @@ Proof.
   induction f; intros v1 v2 m1 m10_eq eval_v1 eval_v2.
   - inversion eval_v1; inversion eval_v2; subst; auto;
       try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
-    rewrite H9 in H4; inversion H4; subst; auto.
+    rewrite H7 in H3; inversion H3; subst; auto.
   - inversion eval_v1; inversion eval_v2; subst; auto;
       try repeat (repeat rewrite delta_0_deterministic; simpl in *; rewrite Q2R0_is_0 in *; subst; auto); simpl.
   - inversion eval_v1; inversion eval_v2; subst; auto;

coq/IntervalValidation.v

@@ -201,33 +201,6 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
   | Ret e => e
   end.
 
-Lemma typingVarDet (e:exp Q) m m0 v:
-  typeExpression e (Var Q m v) = Some m0 ->
-  m = m0.
-Proof.
-  revert e; induction e; intros.
-  - simpl in H.
-    case_eq (mTypeEqBool m1 m && (n =? v)); intros; rewrite H0 in H; inversion H; auto.
-    rewrite <- H2.
-    apply andb_true_iff in H0; destruct H0 as [H0m H0n].
-    apply EquivEqBoolEq in H0m; auto.
-  - simpl in H; inversion H.
-  - simpl in H; apply IHe; auto.
-  - simpl in H.
-    case_eq (typeExpression e1 (Var Q m v)); intros; rewrite H0 in H; auto;
-      case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H1 in H; auto.
-    + case_eq (mTypeEqBool m1 m2); intros; rewrite H2 in H; inversion H; auto.
-      apply IHe1; auto.
-      rewrite <- H4; auto.
-    + inversion H; subst; apply IHe1; auto.
-    + inversion H; subst; apply IHe2; auto.
-    + inversion H.
-  - apply IHe.
-    simpl in H.
-    auto.
-Qed.    
-
-
 Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
   (typeExpression (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
   (forall (v : NatSet.elt) (m : mType),
@@ -329,7 +302,7 @@ Proof.
       destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
       rewrite H; auto.
       rewrite E_n_eq in *.
-      inversion H3; subst.
+      inversion H2; subst.
       rewrite absenv_var in *; auto.
     + repeat (rewrite delta_0_deterministic in *; try auto).
       unfold isSupersetIntv in valid_bounds.
@@ -352,7 +325,7 @@ Proof.
         rewrite in_dVars in case_mem; congruence.
       * specialize (valid_usedVars in_fVars);
           destruct valid_usedVars as [vR' [vR_def P_valid]].
-        rewrite vR_def in H3; inversion H3; subst.
+        rewrite vR_def in H2; inversion H2; subst.
         lra.
   - unfold validIntervalbounds in valid_bounds.
     simpl in *;  destruct (absenv (Const m v)) as [intv err]; simpl in *.

coq/Typing.v

@@ -192,6 +192,35 @@ Proof.
   auto.
 Qed.
 
+
+Lemma typingVarDet (e:exp Q) m m0 v:
+  typeExpression e (Var Q m v) = Some m0 ->
+  m = m0.
+Proof.
+  revert e; induction e; intros.
+  - simpl in H.
+    case_eq (mTypeEqBool m1 m && (n =? v)); intros; rewrite H0 in H; inversion H; auto.
+    rewrite <- H2.
+    apply andb_true_iff in H0; destruct H0 as [H0m H0n].
+    apply EquivEqBoolEq in H0m; auto.
+  - simpl in H; inversion H.
+  - simpl in H; apply IHe; auto.
+  - simpl in H.
+    case_eq (typeExpression e1 (Var Q m v)); intros; rewrite H0 in H; auto;
+      case_eq (typeExpression e2 (Var Q m v)); intros; rewrite H1 in H; auto.
+    + case_eq (mTypeEqBool m1 m2); intros; rewrite H2 in H; inversion H; auto.
+      apply IHe1; auto.
+      rewrite <- H4; auto.
+    + inversion H; subst; apply IHe1; auto.
+    + inversion H; subst; apply IHe2; auto.
+    + inversion H.
+  - apply IHe.
+    simpl in H.
+    auto.
+Qed.    
+
+
+
 (* Lemma helpinglemma (e:exp Q) m v : *)
 (*   typeExpression e (Var Q m v) = Some m -> *)
 (*   isSubExpression (Var Q m v) e = true. *)

coq/ssaPrgs.v

@@ -50,7 +50,6 @@ Proof.
     specialize (fVars_live n in_n).
     destruct fVars_live as [vR E_def].
     exists vR; econstructor; eauto.
-    cbv; auto.
   - exists (perturb (Q2R v) 0); constructor.
     simpl (meps M0); rewrite Rabs_R0; rewrite Q2R0_is_0; lra.
   - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e)) vR M0)
@@ -209,10 +208,10 @@ Proof.
   - split; intros eval_Var.
     + inversion eval_Var; subst.
       (*assert (m1 = M0) by (apply ifisMorePreciseM0; auto); subst.*)
-      rewrite agree_on_vars in H3.
+      rewrite agree_on_vars in H2.
       eapply Var_load; eauto.
     + inversion eval_Var; subst.
-      rewrite <- agree_on_vars in H3.
+      rewrite <- agree_on_vars in H2.
       eapply Var_load; eauto.
   - split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
   - split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
@@ -322,9 +321,9 @@ Proof.
     + unfold updEnv in eval_upd. simpl in *.
       inversion eval_upd; subst.
       case_eq (n =? x); intros; try auto.
-      * rewrite H in H3.
-        inversion H3; subst; auto.
-      * rewrite H in H3. 
+      * rewrite H in H2.
+        inversion H2; subst; auto.
+      * rewrite H in H2. 
         eapply Var_load; eauto.
     + simpl in eval_subst.
       case_eq (n =? x); intros n_eq_case;
@@ -333,11 +332,11 @@ Proof.
         assert (updEnv x M0 v E n = Some (v_res, M0)).
         { unfold updEnv; rewrite n_eq_case.
           f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. }
-        { econstructor; eauto. cbv; auto. } 
+        { econstructor; eauto. } 
       * simpl. inversion eval_subst; subst.
         assert (E n = updEnv x M0 v E n).
         { unfold updEnv; rewrite n_eq_case; reflexivity. }
-        { rewrite H in H3. eapply Var_load; eauto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*)
+        { rewrite H in H2. eapply Var_load; eauto. } (*unfold updEnv in *. rewrite n_eq_case in *. unfold toREvalEnv. apply H4. }*)
   - intros v_res; split; [intros eval_upd | intros eval_subst].
     + inversion eval_upd; constructor; auto.
     + inversion eval_subst; constructor; auto.