Merge branch 'letBindings'

coq/CertificateChecker.v

@@ -5,15 +5,15 @@
    as shown in the soundness theorem.
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
-Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
-Require Import Daisy.IntervalValidation Daisy.ErrorValidation.
+Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
+Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
 
 Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
-  andb (validIntervalbounds e absenv P) (validErrorbound e absenv).
+  andb (validIntervalbounds e absenv P NatSet.empty) (validErrorbound e absenv).
 
 (**
    Soundness proof for the certificate checker.
@@ -22,9 +22,10 @@ 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) (vR:R) (vF:R),
-    eval_exp 0%R cenv P (toRExp e) vR ->
-    eval_exp (Q2R machineEpsilon) cenv P (toRExp e) vF ->
+  forall (VarEnv1 VarEnv2 ParamEnv:env) (vR:R) (vF:R),
+    approxEnv VarEnv1 absenv VarEnv2 ->
+    eval_exp 0%R VarEnv1 ParamEnv P (toRExp e) vR ->
+    eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e) vF ->
     CertificateChecker e absenv P = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
 (**
@@ -32,17 +33,50 @@ Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
    validator and the error bound validator.
 **)
 Proof.
-  intros cenv vR vF eval_real eval_float certificate_valid.
+  intros VarEnv1 VarEnv2 ParamEnv vR vF approxC1C2 eval_real eval_float certificate_valid.
   unfold CertificateChecker in certificate_valid.
-  apply Is_true_eq_left in certificate_valid.
-  apply andb_prop_elim in certificate_valid.
-  destruct certificate_valid as [iv_valid errorbound_valid].
-  apply Is_true_eq_true in iv_valid;
-    apply Is_true_eq_true in errorbound_valid.
+  andb_to_prop certificate_valid.
   assert (exists iv err, absenv e = (iv,err)) by (destruct (absenv e); repeat eexists).
   destruct H as [iv [err absenv_eq]].
   assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
   destruct H as [ivlo [ ivhi iv_eq]].
   subst; rewrite absenv_eq in *; simpl in *.
-  eapply (validErrorbound_sound e cenv absenv vR vF err P); eauto.
+  eapply (validErrorbound_sound); eauto.
+  intros v v_in_empty.
+  rewrite NatSet.mem_spec in v_in_empty.
+  hnf in v_in_empty.
+  inversion v_in_empty.
+Qed.
+
+Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
+  andb (validIntervalboundsCmd f absenv P NatSet.empty)
+       (validErrorboundCmd f absenv).
+
+Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
+  forall (VarEnv1 VarEnv2 ParamEnv:env) outVars vR vF,
+    approxEnv VarEnv1 absenv VarEnv2 ->
+    ssaPrg Q f NatSet.empty outVars ->
+    bstep (toRCmd f) VarEnv1 ParamEnv P 0 (Nop R) vR ->
+    bstep (toRCmd f) VarEnv2 ParamEnv P (Q2R machineEpsilon) (Nop R) vF ->
+    CertificateCheckerCmd f absenv P = true ->
+    (Rabs (vR - vF) <= Q2R (snd (absenv (Var Q 0))))%R.
+(**
+   The proofs is a simple composition of the soundness proofs for the range
+   validator and the error bound validator.
+**)
+Proof.
+  intros VarEnv1 VarEnv2 ParamEnv outVars envR envF
+         approxC1C2 ssa_f eval_real eval_float certificate_valid.
+  unfold CertificateCheckerCmd in certificate_valid.
+  andb_to_prop certificate_valid.
+  assert (exists iv err, absenv (Var Q 0) = (iv,err)) by (destruct (absenv (Var Q 0)); repeat eexists).
+  destruct H as [iv [err absenv_eq]].
+  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) by (destruct iv; repeat eexists).
+  destruct H as [ivlo [ ivhi iv_eq]].
+  subst; rewrite absenv_eq in *; simpl in *.
+  eapply (validErrorboundCmd_sound); eauto.
+  intros v v_in_empty.
+  rewrite NatSet.mem_spec in v_in_empty.
+  hnf in v_in_empty.
+  inversion v_in_empty.
 Qed.
\ No newline at end of file

coq/Commands.v

 (**
  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.
+Require Import Coq.Reals.Reals Coq.QArith.QArith.
+Require Export Daisy.Infra.ExpressionAbbrevs.
 (**
   Next define what a program is.
   Currently no loops, only conditionals and assignments
@@ -15,25 +14,61 @@ Let: nat -> exp V -> cmd V -> cmd V
 | Nop: cmd V.
 
 (**
-   Small Step semantics for Daisy language, parametric by evaluation function.
+   Small Step semantics for Daisy language
 **)
-Inductive sstep : cmd R -> env -> precond -> R -> cmd R -> env -> Prop :=
-  let_s x e s env P v eps:
-    eval_exp eps env P e v ->
-    sstep (Let R x e s) env P eps s (updEnv x v env)
- |ret_s e env P v eps:
-    eval_exp eps env P  e v ->
-    sstep (Ret R e) env P eps (Nop R) (updEnv 0 v env).
+Inductive sstep : cmd R -> env -> env -> precond -> R -> cmd R -> env -> Prop :=
+  let_s x e s VarEnv ParamEnv P v eps:
+    eval_exp eps VarEnv ParamEnv P e v ->
+    sstep (Let R x e s) VarEnv ParamEnv P eps s (updEnv x v VarEnv)
+ |ret_s e VarEnv ParamEnv P v eps:
+    eval_exp eps VarEnv ParamEnv P  e v ->
+    sstep (Ret R e) VarEnv ParamEnv P eps (Nop R) (updEnv 0 v VarEnv).
 
 (**
-  Analogously define Big Step semantics for the Daisy language,
-  parametric by the evaluation function
+  Analogously define Big Step semantics for the Daisy language
  **)
-Inductive bstep : cmd R -> env -> precond -> R -> cmd R -> env -> Prop :=
-  let_b x e s s' env P v eps env2:
-    eval_exp eps env P e v ->
-    bstep s (updEnv x v env) P eps s' env2 ->
-    bstep (Let R x e s) env P eps s' env2
- |ret_b e env P v eps:
-    eval_exp eps env P e v ->
-    bstep (Ret R e) env P eps (Nop R) (updEnv 0 v env).
\ No newline at end of file
+Inductive bstep : cmd R -> env -> env -> precond -> R -> cmd R -> R -> Prop :=
+  let_b x e s s' VarEnv ParamEnv P v eps res:
+    eval_exp eps VarEnv ParamEnv P e v ->
+    bstep s (updEnv x v VarEnv) ParamEnv P eps s' res ->
+    bstep (Let R x e s) VarEnv ParamEnv P eps s' res
+ |ret_b e VarEnv ParamEnv P v eps:
+    eval_exp eps VarEnv ParamEnv P e v ->
+    bstep (Ret R e) VarEnv ParamEnv P eps (Nop R) v.
+
+Fixpoint substitute_exp (v:nat) (e:exp Q) (e_old:exp Q) :=
+  match e_old with
+  |Var _ v_old => if (v =? v_old) then e else Var Q v_old
+  |Unop op e' => Unop op (substitute_exp v e e')
+  |Binop op e1 e2 => Binop op (substitute_exp v e e1) (substitute_exp v e e2)
+  |e => e
+  end.
+
+Fixpoint substitute (v:nat) (e:exp Q) (f:cmd Q) :=
+  match f with
+  |Let _ x e_x g =>
+   let new_e  := substitute_exp v e e_x in
+   Let Q x new_e (substitute v e g)
+  |Ret _ e_ret => Ret Q (substitute_exp v e e_ret)
+  |Nop _ => Nop Q
+  end.
+
+Fixpoint expand_lets (f:cmd Q) (fuel:nat) :option (cmd Q):=
+  match fuel with
+  |0%nat => Some f
+  |S fuel' =>
+   match f with
+   |Let _ x e g =>
+    (expand_lets (substitute x e g) fuel')
+   |Ret _ e => Some (Ret Q e)
+   |Nop _ => None
+   end
+  end.
+
+Fixpoint count_lets (f:cmd Q) :nat :=
+  match f with
+  |Let _ x e g => S (count_lets g)
+  | _ => 0%nat
+  end.
+
+Definition expand (f:cmd Q) := expand_lets f (count_lets f).
\ No newline at end of file

coq/Environments.v

@@ -3,8 +3,8 @@ 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.
+Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.Qreals.
+Require Import Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 
 (**
 Define an approximation relation between two environments.
@@ -13,30 +13,8 @@ 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 : precond -> R -> env -> R -> env -> Prop :=
-|approxRefl eps P E: approxEnv P eps E eps E
-|approxUpd P eps1 E1 eps2 E2 t x v1 v2: approxEnv P eps1 E1 eps2 E2 ->
-                                     eval_exp eps1 E1 P t v1 ->
-                                     eval_exp eps2 E2 P t v2 ->
-                                     approxEnv P eps1 (updEnv x v1 E1) eps2 (updEnv x v2 E2).
-
-Lemma small_step_preserves_sim P f g E1 E2 E1' E2' eps1 eps2:
-  approxEnv P eps1 E1 eps2 E2 ->
-  sstep f E1 P eps1 g E1' ->
-  sstep f E2 P eps2 g E2' ->
-  approxEnv P eps1 E1' eps2 E2'.
-Proof.
-  intros approxBefore.
-  induction f; intros stepLet1 stepLet2.
-  - inversion stepLet1; inversion stepLet2; subst.
-    eapply approxUpd.
-    apply approxBefore.
-    apply H7.
-    apply H16.
-  - inversion stepLet1; inversion stepLet2; subst.
-    eapply approxUpd.
-    apply approxBefore.
-    apply H0.
-    auto.
-  - inversion stepLet1.
-Qed.
\ No newline at end of file
+Inductive approxEnv : env -> analysisResult -> env -> Prop :=
+|approxRefl E A: approxEnv E A E
+|approxUpd E1 E2 A v1 v2 x: approxEnv E1 A E2 ->
+			    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
+                            approxEnv (updEnv x v1 E1) A (updEnv x v2 E2).
\ No newline at end of file

coq/ErrorBounds.v

@@ -4,15 +4,15 @@ This shortens soundness proofs later.
 Bounds are explained in section 5, Deriving Computable Error Bounds
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
-Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps Daisy.Expressions.
+Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
+Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
-Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R):
-  forall cenv:nat -> R,
-  eval_exp 0%R cenv P (Const n) nR ->
-  eval_exp (Q2R machineEpsilon) cenv P (Const n) nF ->
+Lemma const_abs_err_bounded (P:precond) (n:R) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
+  eval_exp 0%R VarEnv1 ParamEnv P (Const n) nR ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Const n) nF ->
   (Rabs (nR - nF) <= Rabs n * (Q2R machineEpsilon))%R.
 Proof.
-  intros cenv eval_real eval_float.
+  intros eval_real eval_float.
   inversion eval_real; subst.
   rewrite delta_0_deterministic; auto.
   inversion eval_float; subst.
@@ -21,10 +21,10 @@ Proof.
   apply Rmult_le_compat_l; [apply Rabs_pos | auto].
 Qed.
 
-Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (cenv:nat->R):
-  eval_exp 0%R cenv P (Param R n) nR ->
-  eval_exp (Q2R machineEpsilon) cenv P (Param R n) nF ->
-  (Rabs (nR - nF) <= Rabs (cenv n) * (Q2R machineEpsilon))%R.
+Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (VarEnv1 VarEnv2 ParamEnv:env) (absenv:analysisResult):
+  eval_exp 0%R VarEnv1 ParamEnv P (Param R n) nR ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (Param R n) nF ->
+  (Rabs (nR - nF) <= Rabs (ParamEnv n) * (Q2R machineEpsilon))%R.
 Proof.
   intros eval_real eval_float.
   inversion eval_real; subst.
@@ -36,16 +36,17 @@ Proof.
   apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
 Qed.
 
-Lemma add_abs_err_bounded (e1:exp R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) (P:precond) (err1:R) (err2:R):
-  eval_exp 0%R cenv P e1 e1R ->
-  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
-  eval_exp 0%R cenv P e2 e2R ->
-  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
-  eval_exp 0%R cenv P (Binop Plus e1 e2) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Plus (Var R 1) (Var R 2)) vF ->
-  (Rabs (e1R - e1F) <= err1)%R ->
-  (Rabs (e2R - e2F) <= err2)%R ->
-  (Rabs (vR - vF) <= err1 + err2 + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
+Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
+      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult):
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (Binop Plus (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var R 1) (Var R 2)) vF ->
+  (Rabs (e1R - e1F) <= Q2R (snd (absenv e1)))%R ->
+  (Rabs (e2R - e2F) <= Q2R (snd (absenv e2)))%R ->
+  (Rabs (vR - vF) <= Q2R (snd(absenv e1)) + Q2R (snd (absenv e2)) + (Rabs (e1F + e2F) * (Q2R machineEpsilon)))%R.
 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 *)
@@ -95,16 +96,17 @@ 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 R) (e1R:R) (e1F:R) (e2:exp R) (e2R:R) (e2F:R) (vR:R) (vF:R) (cenv:nat->R) P (err1:R) (err2:R):
-  eval_exp 0%R cenv P e1 e1R ->
-  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
-  eval_exp 0%R cenv P e2 e2R ->
-  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
-  eval_exp 0%R cenv P (Binop Sub e1 e2) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Sub (Var R 1) (Var R 2)) vF ->
-  (Rabs (e1R - e1F) <= err1)%R ->
-  (Rabs (e2R - e2F) <= err2)%R ->
-  (Rabs (vR - vF) <= err1 + err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
+Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
+      (e2F:R) (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:nat->R) P err1 err2:
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (Binop Sub (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var R 1) (Var R 2)) vF ->
+  (Rabs (e1R - e1F) <= Q2R err1)%R ->
+  (Rabs (e2R - e2F) <= Q2R err2)%R ->
+  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R machineEpsilon)))%R.
 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 *)
@@ -147,13 +149,14 @@ 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) (P:precond) (err1:R) (err2:R):
-  eval_exp 0%R cenv P e1 e1R ->
-  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
-  eval_exp 0%R cenv P e2 e2R ->
-  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
-  eval_exp 0%R cenv P (Binop Mult e1 e2) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Mult (Var R 1) (Var R 2)) vF ->
+Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
+      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (Binop Mult (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var R 1) (Var R 2)) vF ->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R machineEpsilon))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
@@ -191,13 +194,14 @@ 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) (P:precond) (err1:R) (err2:R):
-  eval_exp 0%R cenv P e1 e1R ->
-  eval_exp (Q2R machineEpsilon) cenv P e1 e1F ->
-  eval_exp 0%R cenv P e2 e2R ->
-  eval_exp (Q2R machineEpsilon) cenv P e2 e2F ->
-  eval_exp 0%R cenv P (Binop Div e1 e2) vR ->
-  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F cenv)) P (Binop Div (Var R 1) (Var R 2)) vF ->
+Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
+      (vR:R) (vF:R) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond):
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e1) e1R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e1) e1F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (toRExp e2) e2R ->
+  eval_exp (Q2R machineEpsilon) VarEnv2 ParamEnv P (toRExp e2) e2F ->
+  eval_exp 0%R VarEnv1 ParamEnv P (Binop Div (toRExp e1) (toRExp e2)) vR ->
+  eval_exp (Q2R machineEpsilon) (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var R 1) (Var R 2)) vF ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R machineEpsilon))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.

coq/Expressions.v

@@ -115,25 +115,29 @@ 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) (E:env) (P:precond) : (exp R) -> R -> Prop :=
-  Var_load x: eval_exp eps E  P (Var R x) (E x)
-| Param_acc x delta:
+Inductive eval_exp (eps:R) (VarEnv:env) (ParamEnv:env) (P:precond) : (exp R) -> R -> Prop :=
+  Var_load x: eval_exp eps VarEnv ParamEnv P (Var R x) (VarEnv x)
+| Param_acc x delta delta_lo delta_hi:
     ((Rabs delta) <= eps)%R ->
-    ((Q2R (fst (P x))) <= perturb (E x) delta <= (Q2R (snd (P x))))%R ->
-    eval_exp eps E P (Param R x) (perturb (E x) delta)
+    ((Rabs delta_lo) <= eps)%R ->
+    ((Rabs delta_hi) <= eps)%R ->
+    ((perturb (Q2R (fst (P x))) delta_lo) <= perturb (ParamEnv x) delta <= (perturb (Q2R (snd (P x))) delta_hi))%R ->
+    eval_exp eps VarEnv ParamEnv P (Param R x) (perturb (ParamEnv x) delta)
 | Const_dist n delta:
     Rle (Rabs delta) eps ->
-    eval_exp eps E P (Const n) (perturb n delta)
-| Unop_neg f1 v1: eval_exp eps E P f1 v1 -> eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)
+    eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)
+| Unop_neg f1 v1:
+    eval_exp eps VarEnv ParamEnv P f1 v1 ->
+    eval_exp eps VarEnv ParamEnv P (Unop Neg f1) (evalUnop Neg v1)
 | Unop_inv f1 v1 delta:
     Rle (Rabs delta) eps ->
-    eval_exp eps E P f1 v1 ->
-    eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
+    eval_exp eps VarEnv ParamEnv P f1 v1 ->
+    eval_exp eps VarEnv ParamEnv P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)
 | Binop_dist op f1 f2 v1 v2 delta:
     Rle (Rabs delta) eps ->
-                eval_exp eps E P f1 v1 ->
-                eval_exp eps E P f2 v2 ->
-                eval_exp eps E P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
+                eval_exp eps VarEnv ParamEnv P f1 v1 ->
+                eval_exp eps VarEnv ParamEnv P f2 v2 ->
+                eval_exp eps VarEnv ParamEnv P (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
 
 (**
 If |delta| <= 0 then perturb v delta is exactly v.
@@ -150,10 +154,10 @@ Qed.
 (**
 Evaluation with 0 as machine epsilon is deterministic
 **)
-Lemma meps_0_deterministic (f:exp R) (E:env) (P:precond):
+Lemma meps_0_deterministic (f:exp R) (VarEnv ParamEnv:env) (P:precond):
   forall v1 v2,
-  eval_exp R0 E P f v1 ->
-  eval_exp R0 E P f v2 ->
+  eval_exp R0 VarEnv ParamEnv P f v1 ->
+  eval_exp R0 VarEnv ParamEnv P f v2 ->
   v1 = v2.
 Proof.
   induction f; intros v1 v2 eval_v1 eval_v2;
@@ -174,12 +178,12 @@ 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
 **)
-Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (cE:env) (P:precond) (v:R):
-  (eval_exp eps cE P (Binop b f1 f2) v <->
+Lemma binary_unfolding (b:binop) (f1:exp R) (f2:exp R) (eps:R) (VarEnv ParamEnv:env) (P:precond) (v:R):
+  (eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) v <->
    exists v1 v2,
-     eval_exp eps cE P f1 v1 /\
-     eval_exp eps cE P f2 v2 /\
-     eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cE)) P (Binop b (Var R 1) (Var R 2)) v).
+     eval_exp eps VarEnv ParamEnv P f1 v1 /\
+     eval_exp eps VarEnv ParamEnv P f2 v2 /\
+     eval_exp eps (updEnv 2 v2 (updEnv 1 v1 VarEnv)) ParamEnv P (Binop b (Var R 1) (Var R 2)) v).
 Proof.
   split.
   - intros eval_bin.
@@ -199,11 +203,11 @@ Qed.
 (**
 Analogous lemma for unary expressions.
 **)
-Lemma unary_unfolding (e:exp R) (eps:R) (cE:env) (P:precond) (v:R):
-  (eval_exp eps cE P (Unop Inv e) v <->
+Lemma unary_unfolding (e:exp R) (eps:R) (VarEnv ParamEnv:env) (P:precond) (v:R):
+  (eval_exp eps VarEnv ParamEnv P (Unop Inv e) v <->
    exists v1,
-     eval_exp eps cE P e v1 /\
-     eval_exp eps (updEnv 1 v1 cE) P (Unop Inv (Var R 1)) v).
+     eval_exp eps VarEnv ParamEnv P e v1 /\
+     eval_exp eps (updEnv 1 v1 VarEnv) ParamEnv P (Unop Inv (Var R 1)) v).
 Proof.
   split.
   - intros eval_un.
@@ -229,15 +233,15 @@ Inductive bexp (V:Type) : Type :=
 (**
   Define evaluation of booleans for reals
  **)
-Inductive bval (eps:R) (E:env) (P:precond): (bexp R) -> Prop -> Prop :=
+Inductive bval (eps:R) (VarEnv ParamEnv:env) (P:precond): (bexp R) -> Prop -> Prop :=
   leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
-    eval_exp eps E P f1 v1 ->
-    eval_exp eps E P f2 v2 ->
-    bval eps E P (leq f1 f2) (Rle v1 v2)
+    eval_exp eps VarEnv ParamEnv P f1 v1 ->
+    eval_exp eps VarEnv ParamEnv P f2 v2 ->
+    bval eps VarEnv ParamEnv P (leq f1 f2) (Rle v1 v2)
 |less_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):
-    eval_exp eps E P f1 v1 ->
-    eval_exp eps E P f2 v2 ->
-    bval eps E P (less f1 f2) (Rlt v1 v2).
+    eval_exp eps VarEnv ParamEnv P f1 v1 ->
+    eval_exp eps VarEnv ParamEnv P f2 v2 ->
+    bval eps VarEnv ParamEnv P (less f1 f2) (Rlt v1 v2).
 (**
  Simplify arithmetic later by making > >= only abbreviations
 **)

coq/IntervalValidation.v

@@ -7,7 +7,8 @@
 **)
 Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List Coq.micromega.Psatz.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
-Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps.
+Require Import Daisy.Infra.Ltacs Daisy.Infra.RealSimps.
+Require Export Daisy.IntervalArithQ Daisy.IntervalArith Daisy.ssaPrgs.
 
 Import Lists.List.ListNotations.
 
@@ -20,14 +21,14 @@ Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
   |Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
   end.
 
-Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
+Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
   let (intv, _) := absenv e in
     match e with
-    | Var _ v => false
+    | Var _ v => NatSet.mem v validVars
     | Param _ v => isSupersetIntv (P v) intv
     | Const n => isSupersetIntv (n,n) intv
     | Unop o f =>
-    let rec := validIntervalbounds f absenv P in
+    let rec := validIntervalbounds f absenv P validVars in
     let (iv, _) := absenv f in
     let opres :=
         match o with
@@ -44,7 +45,7 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
     in
     andb rec opres
     | Binop op f1 f2 =>
-      let rec := andb (validIntervalbounds f1 absenv P) (validIntervalbounds f2 absenv P) in
+      let rec := andb (validIntervalbounds f1 absenv P validVars) (validIntervalbounds f2 absenv P validVars) in
       let (iv1,_) := absenv f1 in
       let (iv2,_) := absenv f2 in
       let opres :=
@@ -69,8 +70,22 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
       andb rec opres
     end.
 
-Theorem ivbounds_approximatesPrecond_sound f absenv P:
-  validIntervalbounds f absenv P = true ->
+Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
+  match f with
+  | Let _ x e g =>
+    validIntervalbounds e absenv P validVars &&
+                        (Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q x)))) &&
+                                  Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q x))))) &&
+                        validIntervalboundsCmd g absenv P (NatSet.add x validVars)
+  |Ret _ e =>
+   validIntervalbounds e absenv P validVars &&
+                       (Qeq_bool (fst (fst (absenv e))) (fst (fst (absenv (Var Q 0)))) &&
+                                 Qeq_bool (snd (fst (absenv e))) (snd (fst (absenv (Var Q 0)))))
+  |Nop _ => false
+  end.
+
+Theorem ivbounds_approximatesPrecond_sound f absenv P V:
+  validIntervalbounds f absenv P V = true ->
   forall v, In v (freeVars Q f) ->
        Is_true(isSupersetIntv (P v) (fst (absenv (Param Q v)))).
 Proof.
@@ -121,9 +136,9 @@ Qed.
 Ltac env_assert absenv e name :=
   assert (exists iv err, absenv e = (iv,err)) as name by (destruct (absenv e); repeat eexists; auto).
 
-Lemma validBoundsDiv_uneq_zero e1 e2 absenv P ivlo_e2 ivhi_e2 err:
+Lemma validBoundsDiv_uneq_zero e1 e2 absenv P V ivlo_e2 ivhi_e2 err:
   absenv e2 = ((ivlo_e2,ivhi_e2), err) ->
-  validIntervalbounds (Binop Div e1 e2) absenv P = true ->
+  validIntervalbounds (Binop Div e1 e2) absenv P V = true ->
   (ivhi_e2 < 0) \/ (0 < ivlo_e2).
 Proof.
   intros absenv_eq validBounds.
@@ -139,19 +154,23 @@ Proof.
   apply le_neq_bool_to_lt_prop; auto.
 Qed.
 
-Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) cenv:
+Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V VarEnv ParamEnv:
   forall vR,
-(*  precondValidForExec P cenv ->*)
-  validIntervalbounds f absenv P = true ->
-  eval_exp 0%R cenv P (toRExp f) vR