Rework typing to get the semantics and typing work closer together.

Using this new typing, prove the stronger soundness statement, moving the evaluation to the conclusion of the theorems.

coq/CertificateChecker.v

@@ -25,22 +25,25 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (def
    the real valued execution respects the precondition.
 **)
 Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
-  forall (E1 E2:env) (vR:R) (vF:R) fVars m,
-    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
-    (forall v, NatSet.mem v fVars = true ->
+  forall (E1 E2:env),
+    approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
+    (forall v, NatSet.mem v (Expressions.usedVars e) = true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    NatSet.Subset (Expressions.usedVars e) fVars ->
-    eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 ->
-    eval_exp E2 defVars (toRExp e) vF m ->
+    (forall v, (v) mem (usedVars e) = true ->
+          exists m : mType,
+            defVars v = Some m) ->
     CertificateChecker e absenv P defVars = true ->
+   exists vR vF m,
+    eval_exp E1 (toRMap defVars) (toREval (toRExp e)) vR M0 /\
+    eval_exp E2 defVars (toRExp e) vF m /\
     (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
 **)
 Proof.
-  intros * approxE1E2 P_valid fVars_subset eval_real eval_float certificate_valid.
+  intros * approxE1E2 P_valid types_defined certificate_valid.
   unfold CertificateChecker in certificate_valid.
   rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
@@ -48,14 +51,23 @@ Proof.
   destruct env_e as [iv [err absenv_eq]].
   destruct iv as [ivlo ivhi].
   rewrite absenv_eq; simpl.
-  eapply validErrorbound_sound; eauto.
-  - hnf. intros a in_diff.
-    rewrite NatSet.diff_spec in in_diff.
-    apply fVars_subset.
-    destruct in_diff; auto.
-  - intros v v_in_empty.
+  pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
+  hnf in union_empty.
+  assert (forall v1, (v1) mem (Expressions.usedVars e ∪ NatSet.empty) = true ->
+                exists m0 : mType, defVars v1 = Some m0).
+  { intros; eapply types_defined.
+    rewrite NatSet.mem_spec in *.
+    rewrite <- union_empty; eauto. }
+  assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
+  { hnf; intros a in_empty.
+    set_tac. }
+  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
+  { intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
-    inversion v_in_empty.
+    inversion v_in_empty. }
+  edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
+  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [vF [mF [eval_float err_bounded]]]; auto.
+  exists vR; exists vF; exists mF; split; auto.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
@@ -66,21 +78,25 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
   else false.
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
-  forall (E1 E2:env) vR vF m,
+  forall (E1 E2:env),
     approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
     (forall v, NatSet.mem v (freeVars f)= true ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 ->
-    bstep (toRCmd f) E2 defVars vF m ->
+    (forall v, (v) mem (freeVars f) = true ->
+          exists m : mType,
+            defVars v = Some m) ->
     CertificateCheckerCmd f absenv P defVars = true ->
+    exists vR vF m,
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR M0 /\
+    bstep (toRCmd f) E2 defVars vF m /\
     (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
 **)
 Proof.
-  intros * approxE1E2 P_valid eval_real eval_float certificate_valid.
+  intros * approxE1E2 P_valid types_defined certificate_valid.
   unfold CertificateCheckerCmd in certificate_valid.
   repeat rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
@@ -89,20 +105,25 @@ Proof.
   env_assert absenv (getRetExp f) env_f.
   destruct env_f as [iv [err absenv_eq]].
   destruct iv as [ivlo ivhi].
+  assert (ssa f (freeVars f ∪ NatSet.empty) outVars) as ssa_valid.
+  { eapply ssa_equal_set; try eauto.
+    apply NatSetProps.empty_union_2.
+    apply NatSet.empty_spec. }
+  assert (forall v, (v) mem (NatSet.empty) = true ->
+               exists vR : R,
+                 E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.
+  { intros v v_in_empty.
+    set_tac. inversion v_in_empty. }
+  assert (forall v, (v) mem (freeVars f ∪ NatSet.empty) = true ->
+               exists m : mType, defVars v = Some m) as types_valid.
+  { intros v v_mem; apply types_defined.
+    set_tac. rewrite NatSet.union_spec in v_mem.
+    destruct v_mem; try auto.
+    inversion H. }
+  assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
+    as freeVars_contained by set_tac.
+  edestruct (validIntervalboundsCmd_sound) as [vR [eval_real bounded_real_f]] ; eauto.
   rewrite absenv_eq; simpl.
-  eapply (validErrorboundCmd_sound); eauto.
-  - instantiate (1 := outVars).
-    eapply ssa_equal_set; try eauto.
-    hnf.
-    intros a; split; intros in_union.
-    + rewrite NatSet.union_spec in in_union.
-      destruct in_union as [in_fVars | in_empty]; try auto.
-      inversion in_empty.
-    + rewrite NatSet.union_spec; auto.
-  - hnf; intros a in_diff.
-    rewrite NatSet.diff_spec in in_diff.
-    destruct in_diff; auto.
-  - intros v v_in_empty.
-    rewrite NatSet.mem_spec in v_in_empty.
-    inversion v_in_empty.
-Qed.y
+  edestruct (validErrorboundCmd_sound) as [vF [mF [eval_float bounded_float]]]; eauto.
+  exists vR; exists vF; exists mF; split; auto.
+Qed.
\ No newline at end of file

coq/Commands.v

@@ -51,16 +51,13 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
  **)
 Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
   let_b m m' x e s E v res defVars:
-    eval_exp E defVars  e v m ->
-    defVars x = Some m ->
-    bstep s (updEnv x v E) defVars res m' ->
+    eval_exp E defVars e v m ->
+    bstep s (updEnv x v E) (updDefVars x m defVars) res m' ->
     bstep (Let m x e s) E defVars res m'
  |ret_b m e E v defVars:
     eval_exp E defVars e v m ->
     bstep (Ret e) E defVars v m.
 
-
-
 (**
   The free variables of a command are all used variables of expressions
   without the let bound variables

coq/Environments.v

@@ -17,15 +17,14 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
    approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
 |approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
    approxEnv E1 defVars A fVars dVars E2 ->
-   defVars x = Some m ->
-   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R ->
+   (Rabs (v1 - v2) <= (Rabs v1) * Q2R (mTypeToQ m))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) defVars A (NatSet.add x fVars) dVars (updEnv x v2 E2)
-|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars:
+   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
+|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m:
    approxEnv E1 defVars A fVars dVars E2 ->
    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x v1 E1) defVars A fVars (NatSet.add x dVars) (updEnv x v2 E2).
+   approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (NatSet.add x dVars) (updEnv x v2 E2).
 
 (* Inductive approxParams :env -> env -> Prop := *)
 (* |approxParamRefl: *)
@@ -34,3 +33,110 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
 (*    approxParams E1 E2 -> *)
 (*    (Rabs (v1 - v2) <= Q2R (meps m))%R -> *)
 (*    approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *)
+
+Section RelationProperties.
+
+  Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType) (A:analysisResult) (fVars dVars: NatSet.t).
+
+  Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.
+
+Lemma approxEnv_gives_value:
+  E1 x = Some v ->
+  NatSet.In x (NatSet.union fVars  dVars) ->
+  exists v',
+    E2 x = Some v'.
+Proof.
+  induction approxEnvs;
+    intros E1_def x_valid.
+  - unfold emptyEnv in E1_def; simpl in E1_def. congruence.
+  - unfold updEnv in *.
+    case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+    + eexists; eauto.
+    + eapply IHa; auto.
+      set_tac.
+      rewrite NatSet.union_spec in x_valid.
+      destruct x_valid; set_tac.
+      rewrite NatSet.add_spec in H1.
+      destruct H1; subst; try auto.
+      rewrite Nat.eqb_refl in eq_case; congruence.
+  - unfold updEnv in *.
+    case_eq (x =? x0); intros eq_case; rewrite eq_case in *.
+    + eexists; eauto.
+    + eapply IHa; auto.
+      set_tac.
+      rewrite NatSet.union_spec in x_valid.
+      destruct x_valid; set_tac.
+      rewrite NatSet.add_spec in H1.
+      destruct H1; subst; try auto.
+      rewrite Nat.eqb_refl in eq_case; congruence.
+Qed.
+
+Arguments mTypeToQ _ : simpl nomatch.
+
+Lemma approxEnv_fVar_bounded v2 m:
+  E1 x = Some v ->
+  E2 x = Some v2 ->
+  NatSet.In x fVars ->
+  Gamma x = Some m ->
+  (Rabs (v - v2) <= (Rabs v) * Q2R (mTypeToQ m))%R.
+Proof.
+  induction approxEnvs;
+    intros E1_def E2_def x_free x_typed.
+  - unfold emptyEnv in *; simpl in *; congruence.
+  - set_tac.
+    rewrite add_spec_strong in x_free.
+    destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+    + unfold updEnv in *;
+        rewrite Nat.eqb_refl in *; simpl in *.
+      unfold updDefVars in x_typed.
+      rewrite Nat.eqb_refl in x_typed.
+      inversion x_typed; subst.
+      inversion E1_def; inversion E2_def; subst; auto.
+    + unfold updEnv in *; simpl in *.
+      rewrite <- Nat.eqb_neq in x_neq.
+      rewrite x_neq in *; simpl in *.
+      unfold updDefVars in x_typed; rewrite x_neq in x_typed.
+      apply IHa; auto.
+  - assert (x =? x0 = false) as x_x0_neq.
+    { rewrite Nat.eqb_neq; hnf; intros; subst.
+      set_tac.
+      apply H0.
+      set_tac. }
+    unfold updEnv in *; rewrite x_x0_neq in *.
+    apply IHa; auto.
+    unfold updDefVars in x_typed;
+      rewrite x_x0_neq in x_typed; auto.
+Qed.
+
+Lemma approxEnv_dVar_bounded v2 m:
+  E1 x = Some v ->
+  E2 x = Some v2 ->
+  NatSet.In x dVars ->
+  Gamma x = Some m ->
+  (Rabs (v - v2) <= Q2R (snd (A (Var Q x))))%R.
+Proof.
+  induction approxEnvs;
+    intros E1_def E2_def x_def x_typed.
+  - unfold emptyEnv in *; simpl in *; congruence.
+  - assert (x =? x0 = false) as x_x0_neq.
+    { rewrite Nat.eqb_neq; hnf; intros; subst.
+      set_tac.
+      apply H0; set_tac.
+    }
+    unfold updEnv in *; rewrite x_x0_neq in *.
+    unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
+    apply IHa; auto.
+  - set_tac.
+    rewrite add_spec_strong in x_def.
+    destruct x_def as [x_x0 | [x_neq x_def]]; subst.
+    + unfold updEnv in *;
+        rewrite Nat.eqb_refl in *; simpl in *.
+      inversion E1_def; inversion E2_def; subst; auto.
+    + unfold updEnv in *; simpl in *.
+      rewrite <- Nat.eqb_neq in x_neq.
+      rewrite x_neq in *; simpl in *.
+      unfold updDefVars in x_typed; rewrite x_neq in x_typed.
+      apply IHa; auto.
+Qed.
+
+End RelationProperties.
\ No newline at end of file

coq/ErrorBounds.v

@@ -9,9 +9,9 @@ Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
 
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 ->
+  eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 ->
   eval_exp E2 defVars (Const m n) nF m ->
-  (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
+  (Rabs (nR - nF) <= Rabs n * (Q2R (mTypeToQ m)))%R.
 Proof.
   intros eval_real eval_float.
   inversion eval_real; subst.
@@ -20,24 +20,24 @@ Proof.
   unfold perturb; simpl.
   rewrite Rabs_err_simpl, Rabs_mult.
   apply Rmult_le_compat_l; [apply Rabs_pos | auto].
-  simpl (meps M0) in *.
+  simpl (mTypeToQ M0) in *.
   apply (Rle_trans _ (Q2R 0) _); try auto.
   rewrite Q2R0_is_0; lra.
 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 m1 m2:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1->
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
   eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Plus (Var R 1) (Var R 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.
+  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (mTypeToQ m))))%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 *)
@@ -94,17 +94,17 @@ Qed.
 **)
 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 m1 m2:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
   eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Sub (Var R 1) (Var R 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.
+  (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (mTypeToQ m))))%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 *)
@@ -155,15 +155,15 @@ 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 m1 m2:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
   eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Mult (Var R 1) (Var R 2)) vF m ->
-  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
+  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (mTypeToQ 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 *)
@@ -206,15 +206,15 @@ 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 m1 m2:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
   eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
            (Binop Div (Var R 1) (Var R 2)) vF m ->
-  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
+  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (mTypeToQ 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 *)
@@ -433,13 +433,13 @@ Proof.
 Qed.
 
 Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
-  eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 ->
+  eval_exp E1 (toRMap defVars) (toREval e) nR M0 ->
   eval_exp E2 defVars e nF1 m ->
   eval_exp (updEnv 1 nF1 emptyEnv)
            (updDefVars 1 m defVars)
            (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
   (Rabs (nR - nF1) <= err)%R ->
-  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
+  (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (mTypeToQ machineEpsilon))%R.
 Proof.
   intros eval_real eval_float eval_float_rnd err_bounded.
   replace (nR - nF)%R with ((nR - nF1) + (nF1 - nF))%R by lra.

coq/ErrorValidation.v

@@ -6,7 +6,7 @@
    encoded in the analysis result. The validator is used in the file
    CertificateChecker.v to build the complete checker.
  **)
-Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
+Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
 Require Import Coq.micromega.Psatz Coq.Reals.Reals.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps Daisy.Infra.Ltacs.
 Require Import Daisy.Environments Daisy.IntervalValidation Daisy.Typing Daisy.ErrorBounds.
@@ -24,9 +24,9 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
       |Var _ v =>
        if (NatSet.mem v dVars)
        then true
-       else (Qleb (maxAbs intv * (meps m)) err)
+       else (Qleb (maxAbs intv * (mTypeToQ m)) err)
       |Const _ n =>
-       Qleb (maxAbs intv * (meps m)) err
+       Qleb (maxAbs intv * (mTypeToQ m)) err
       |Unop Neg e1 =>
        if (validErrorbound e1 typeMap absenv dVars)
        then Qeq_bool err (snd (absenv e1))
@@ -43,11 +43,11 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
          let upperBoundE2 := maxAbs ive2 in
          match b with
          | Plus =>
-           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (meps m)) err
+           Qleb (err1 + err2 + (maxAbs (addIntv errIve1 errIve2)) * (mTypeToQ m)) err
          | Sub =>
-           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (meps m)) err
+           Qleb (err1 + err2 + (maxAbs (subtractIntv errIve1 errIve2)) * (mTypeToQ m)) err
          | Mult =>
-           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (meps m)) err
+           Qleb ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2)  + (maxAbs (multIntv errIve1 errIve2)) * (mTypeToQ m)) err
          | Div =>
            if (((Qleb (ivhi errIve2) 0) && (negb (Qeq_bool (ivhi errIve2) 0))) ||
                ((Qleb 0 (ivlo errIve2)) && (negb (Qeq_bool (ivlo errIve2) 0))))
@@ -55,20 +55,22 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
              let upperBoundInvE2 := maxAbs (invertIntv ive2) in
              let minAbsIve2 := minAbs (errIve2) in
              let errInv := (1 / (minAbsIve2 * minAbsIve2)) * err2 in
-             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (meps m)) err
+             Qleb ((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideIntv errIve1 errIve2)) * (mTypeToQ m)) err
            else false
          end
        else false
       |Downcast m1 e1 =>
-       let (ive1, err1) := absenv e1 in
-       let rec := validErrorbound e1 typeMap absenv dVars in
-       let errIve1 := widenIntv ive1 err1 in
-       andb rec (Qleb (err1 + maxAbs errIve1 * (meps m1)) err)
+       if validErrorbound e1 typeMap absenv dVars
+       then
+         let (ive1, err1) := absenv e1 in
+         let errIve1 := widenIntv ive1 err1 in
+         (Qleb (err1 + maxAbs errIve1 * (mTypeToQ m1)) err)
+       else
+         false
       end
     else false
   end.
 
-
 (** Error bound command validator **)
 Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
   match f with
@@ -109,15 +111,16 @@ Proof.
     + destruct (tmap (Downcast m e));inversion validErrorbound_e.
 Qed.
 
+Arguments mTypeToQ _ :simpl nomatch.
 
 Lemma validErrorboundCorrectVariable:
-  forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars,
-    typeCheck (Var Q v) defVars Gamma = true ->
-    approxEnv E1 defVars absenv fVars dVars E2 ->
-    eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 ->
-    eval_exp E2 defVars (toRExp (Var Q v)) nF m ->
+  forall E1 E2 absenv (v:nat) e nR nlo nhi P fVars dVars Gamma expTypes,
+    eval_exp E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR M0 ->
+    typeCheck (Var Q v) Gamma expTypes = true ->
+    approxEnv E1 Gamma absenv fVars dVars E2 ->
     validIntervalbounds (Var Q v) absenv P dVars = true ->
-    validErrorbound (Var Q v) Gamma absenv dVars = true ->
+    validErrorbound (Var Q v) expTypes absenv dVars = true ->
+    NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
     (forall v1,
         NatSet.mem v1 dVars = true ->
         exists r, E1 v1 = Some r /\
@@ -125,194 +128,118 @@ Lemma validErrorboundCorrectVariable:
     (forall v1, NatSet.mem v1 fVars= true ->
           exists r, E1 v1 = Some r /\
                 (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
+    (forall v1 : NatSet.elt,
+        NatSet.mem v1 (NatSet.union fVars dVars) = true ->
+        exists m0 : mType, Gamma v1 = Some m0) ->
     absenv (Var Q v) = ((nlo, nhi), e) ->
+    exists nF m,
+    eval_exp E2 Gamma (toRExp (Var Q v)) nF m /\
     (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
-  simpl in eval_real; inversion eval_real; inversion eval_float; subst.
-  rename H1 into E1_v;
-    rename H6 into E2_v.
-  simpl in error_valid.
-  rewrite absenv_var in error_valid; simpl in error_valid; subst.
-  case_eq (Gamma (Var Q v)); intros; rewrite H in error_valid; [ | inversion error_valid].
-  rewrite <- andb_lazy_alt in error_valid.
+  intros * eval_real typing_ok approxCEnv bounds_valid error_valid v_sound dVars_sound P_valid types_valid absenv_var.
+  eapply validIntervalbounds_sound in bounds_valid; eauto.
+  destruct bounds_valid as [nR2 [eval_real2 bounds_valid]].
+  assert (nR2 = nR) by (eapply meps_0_deterministic; eauto);
+    subst.
+  simpl in eval_real; inversion eval_real; subst.
+  rename H1 into E1_v.
+  simpl in *.
+  assert (exists m, Gamma v = Some m) as v_has_type.
+  { destruct (expTypes (Var Q v)); try congruence.
+    case_eq (Gamma v); intros * gamma_v;
+      rewrite gamma_v in *; eauto. }
+  destruct v_has_type as [m type_v].
+  assert (exists nF, eval_exp E2 Gamma (Var R v) nF m) as eval_float.
+  { destruct (approxEnv_gives_value approxCEnv E1_v); try eauto.
+    set_tac.
+    case_eq (NatSet.mem v dVars); intros v_case; set_tac.
+    left; apply v_sound.
+    apply NatSetProps.FM.diff_3; set_tac. }
+  destruct eval_float as [nF eval_float].
+  repeat eexists; try eauto.
+  rewrite absenv_var in error_valid; simpl in error_valid.
+  case_eq (expTypes (Var Q v));
+    intros * expType_v; rewrite expType_v in *; try congruence.
+  rewrite type_v in *; simpl in *.
+  rewrite mTypeEq_compat_eq in typing_ok; subst.
   andb_to_prop error_valid.
   rename L into error_pos.
   rename R into error_valid.
-  (* induction on the approximation relation to do a case distinction on whether
-     we argue currently about a free or a let bound variable *)
-  induction approxCEnv.
-  (* empty environment case, contradiction *)
-  - unfold emptyEnv in *; simpl in *.
-    congruence.
-  - unfold updEnv in *; simpl in *.
-    case_eq (v =? x); intros eq_case; rewrite eq_case in *.
-    + rewrite Nat.eqb_eq in eq_case; subst.
-      assert (NatSet.mem x dVars = false) as x_not_bound.
-      * case_eq (NatSet.mem x dVars); intros case_mem; try auto.
-        rewrite NatSet.mem_spec in case_mem.
-        assert (NatSet.In x (NatSet.union fVars dVars))
-          as x_in_union by (rewrite NatSet.union_spec; auto).
-        rewrite <- NatSet.mem_spec in x_in_union.
-        rewrite x_in_union in *.
-        congruence.
-      * rewrite x_not_bound in error_valid.
-        inversion E1_v; inversion E2_v; subst.
-        eapply Rle_trans; try eauto.
-        apply Qle_bool_iff in error_valid.
-        apply Qle_Rle in error_valid.
-        eapply Rle_trans; eauto.
-        rewrite Q2R_mult.
-        rewrite H5 in H1; inversion H1; subst.
-        rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst.
-        clear H5 H3.
-        apply Rmult_le_compat_r.