[WIP] Change the proofs to account for DeltaMap[s]

68d4bc7b · Nikita Zyuzin · 55c0ef90 · 68d4bc7b · 68d4bc7b · 68d4bc7b
Commit 68d4bc7b authored Nov 27, 2018 by Nikita Zyuzin
8 changed files
--- a/coq/CommandsDeterministic.v
+++ b/coq/CommandsDeterministic.v
@@ -2,7 +2,7 @@
 Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
 **)
 Require Import Coq.Reals.Reals Coq.QArith.QArith.
-Require Export Flover.ExpressionSemanticsDeterministic Flover.Commands.
+Require Export Flover.Commands.
 Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.

 (**

--- a/coq/ErrorBounds.v
+++ b/coq/ErrorBounds.v
@@ -43,7 +43,9 @@ Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Plus (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Plus (toRExp e1) (toRExp e2)) m
+                     else None)
            (Binop Plus (Var R 1) (Var R 2)) vF m ->
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
@@ -114,7 +116,9 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Sub (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Sub (toRExp e1) (toRExp e2)) m
+                     else None)
            (Binop Sub (Var R 1) (Var R 2)) vF m ->
  (Rabs (e1R - e1F) <= Q2R err1)%R ->
  (Rabs (e2R - e2F) <= Q2R err2)%R ->
@@ -190,7 +194,9 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Mult (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Mult (toRExp e1) (toRExp e2)) m
+                     else None)
            (Binop Mult (Var R 1) (Var R 2)) vF m ->
  (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
 Proof.
@@ -239,7 +245,9 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
  eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars (Binop Div (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Div (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Div (toRExp e1) (toRExp e2)) m
+                     else None)
            (Binop Div (Var R 1) (Var R 2)) vF m ->
  (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
 Proof.
@@ -293,7 +301,9 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
            (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
                        (updDefVars (Var R 3) m3
                                    (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3))
+                     then DeltaMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) m
+                     else None)
            (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
  (Rabs (vR - vF) <= Rabs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + computeErrorR (e1F + e2F * e3F ) m)%R.
 Proof.
@@ -356,7 +366,9 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
  eval_expr (updEnv 1 nF1 emptyEnv)
            (updDefVars (Downcast mEps (Var R 1)) mEps
                        (updDefVars (Var R 1) m defVars))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Downcast mEps (Var R 1))
+                     then DeltaMap (Downcast mEps e) mEps
+                     else None)
            (toRExp (Downcast mEps (Var Q 1))) nF mEps->
  (Rabs (nR - nF1) <= err)%R ->
  (Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.

--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
@@ -287,11 +287,9 @@ Lemma validErrorboundCorrectAddition E1 E2 A
            (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
-            (fun (x : expr Rdefinitions.R) (_ : mType) =>
-               if
-                 R_orderedExps.eq_dec x (Binop Plus (Var Rdefinitions.R 1) (Var Rdefinitions.R 2))
-               then Some delta0
-               else None)
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Plus (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Plus (toRExp e1) (toRExp e2)) m
+                     else None)
            (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
  validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
@@ -351,7 +349,9 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
            (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Sub (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Sub (toRExp e1) (toRExp e2)) m
+                     else None)
            (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
  validErrorbound (Binop Sub e1 e2) Gamma A dVars = true ->
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
@@ -881,7 +881,9 @@ Lemma validErrorboundCorrectMult E1 E2 A
            (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Mult (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Mult (toRExp e1) (toRExp e2)) m
+                     else None)
            (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
  validErrorbound (Binop Mult e1 e2) Gamma A dVars = true ->
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
@@ -947,7 +949,9 @@ Lemma validErrorboundCorrectDiv E1 E2 A
            (updDefVars (Binop Div (Var R 1) (Var R 2)) m
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma))))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Binop Div (Var R 1) (Var R 2))
+                     then DeltaMap (Binop Div (toRExp e1) (toRExp e2)) m
+                     else None)
            (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
  validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
@@ -1862,7 +1866,9 @@ Lemma validErrorboundCorrectFma E1 E2 A
                        (updDefVars (Var Rdefinitions.R 3) m3
                        (updDefVars (Var Rdefinitions.R 2) m2
                                    (updDefVars (Var Rdefinitions.R 1) m1 (toRExpMap Gamma)))))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3))
+                     then DeltaMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) m
+                     else None)
            (toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m ->
  validErrorbound (Fma e1 e2 e3) Gamma A dVars = true ->
  (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
@@ -1947,7 +1953,9 @@ Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R)
  eval_Fin E2 Gamma DeltaMap e nF1 m ->
  eval_expr (updEnv 1 nF1 emptyEnv)
            (updDefVars (Downcast mEps (Var R 1)) mEps (updDefVars (Var R 1) m (toRExpMap Gamma)))
-            DeltaMap
+            (fun x _ => if R_orderedExps.eq_dec x (Downcast mEps (Var R 1))
+                     then DeltaMap (toRExp (Downcast mEps e)) mEps
+                     else None)
            (toRExp (Downcast mEps (Var Q 1))) nF mEps ->
  validErrorbound (Downcast mEps e) Gamma A dVars = true ->
  (Q2R elo <= nR <= Q2R ehi)%R ->
@@ -2106,7 +2114,7 @@ Proof.
    + intros * eval_float.
      clear eval_float1 eval_float2.
      inversion eval_float; subst.
-      eapply (binary_unfolding _ H23 H18 H19 H22) in eval_float; try auto.
+      eapply (binary_unfolding H23 H18 H16 H19 H22) in eval_float; try auto.
      destruct b.
      * eapply (validErrorboundCorrectAddition (e1:=e1) A); eauto.
        { cbn. instantiate (1:=dVars); Flover_compute.
@@ -2142,20 +2150,20 @@ Proof.
                                         [m1 [m2 [m3 [find_m1 [find_m2 [find_m3 valid_join]
                                         ]]]]]]]] valid_exec]]].
    inversion eval_real; subst.
-    destruct (IHe1 E1 E2 fVars dVars A v1 e (fst i) (snd i) Gamma)
+    destruct (IHe1 E1 E2 fVars dVars A v1 e (fst i) (snd i) Gamma DeltaMap)
      as [[nF1 [mF1 eval_float1]] valid_bounds_e1]; try auto.
    { set_tac. split; set_tac. }
-    { pose proof (toRTMap_eval_REAL _ H5); subst. auto. }
+    { pose proof (toRTMap_eval_REAL _ H6); subst. auto. }
    { destruct i; auto. }
-    destruct (IHe2 E1 E2 fVars dVars A v2 e0 (fst i0) (snd i0) Gamma )
+    destruct (IHe2 E1 E2 fVars dVars A v2 e0 (fst i0) (snd i0) Gamma DeltaMap)
      as [[nF2 [mF2 eval_float2]] valid_bounds_e2]; try auto.
    { set_tac. split; set_tac. }
-    { pose proof (toRTMap_eval_REAL _ H8); subst. auto. }
+    { pose proof (toRTMap_eval_REAL _ H9); subst. auto. }
    { destruct i0; auto. }
-    destruct (IHe3 E1 E2 fVars dVars A v3 e4 (fst i1) (snd i1) Gamma)
+    destruct (IHe3 E1 E2 fVars dVars A v3 e4 (fst i1) (snd i1) Gamma DeltaMap)
      as [[nF3 [mF3 eval_float3]] valid_bounds_e3]; try auto.
    { set_tac. split; set_tac. }
-    { pose proof (toRTMap_eval_REAL _ H9); subst. auto. }
+    { pose proof (toRTMap_eval_REAL _ H10); subst. auto. }
    { destruct i1; auto. }
    assert (m1 = mF1) by (eapply validTypes_exec in find_m1; eauto).
    assert (m2 = mF2) by (eapply validTypes_exec in find_m2; eauto).
@@ -2168,9 +2176,9 @@ Proof.
    destruct valid_e3 as [iv3 [ err3 [v3' [map_e3 [eval_real_e3 bounds_e3]]]]].
    assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]]
        by (repeat split; eapply toRTMap_eval_REAL; eauto); subst.
-    pose proof (meps_0_deterministic _ eval_real_e1 H5); subst.
-    pose proof (meps_0_deterministic _ eval_real_e2 H8); subst.
-    pose proof (meps_0_deterministic _ eval_real_e3 H9); subst.
+    pose proof (meps_0_deterministic _ eval_real_e1 H6); subst.
+    pose proof (meps_0_deterministic _ eval_real_e2 H9); subst.
+    pose proof (meps_0_deterministic _ eval_real_e3 H10); subst.
    rewrite map_e1, map_e2, map_e3 in *.
    inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
    rename i into iv1; rename e into err1; rename i0 into iv2;
@@ -2188,15 +2196,13 @@ Proof.
    { eapply distance_gives_iv; simpl;
        try eauto. }
    split.
-    + eexists; exists mG; econstructor; eauto.
-      * eapply toRExpMap_some; eauto. simpl; auto.
-      * instantiate (1 := 0%R).
-        rewrite Rabs_R0.
-        apply mTypeToR_pos_R.
+    + specialize (deltas_matched (toRExp (Fma e1 e2 e3)) mG) as (delta' & delta_some' & delta_bound').
+      eexists; exists mG; econstructor; eauto.
+      eapply toRExpMap_some; eauto. simpl; auto.
    + intros * eval_float.
      clear eval_float1 eval_float2 eval_float3.
      inversion eval_float; subst.
-      eapply (fma_unfolding _ H10 H11 H14 H15) in eval_float; try auto.
+      eapply (fma_unfolding H12 H8 H13 H16 H17) in eval_float; try auto.
      eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) A); eauto.
      { simpl.
        rewrite A_eq.
@@ -2211,29 +2217,31 @@ Proof.
      { eapply toRExpMap_find_map; eauto. }
  - cbn in *; Flover_compute; try congruence; type_conv; subst.
    inversion eval_real; subst.
-    apply REAL_least_precision in H2; subst.
+    apply REAL_least_precision in H3; subst.
    destruct i as [ivlo_e ivhi_e]; rename e0 into err_e.
    destruct valid_intv as [valid_e1 valid_intv].
    destruct typing_ok as [mG [find_m [[valid_e [? [m1 [find_e1 morePrecise_m1]]]] valid_exec]]].
-    destruct (IHe E1 E2 fVars dVars A v1 err_e ivlo_e ivhi_e Gamma)
+    destruct (IHe E1 E2 fVars dVars A v1 err_e ivlo_e ivhi_e Gamma DeltaMap)
      as [[vF [mF eval_float_e]] bounded_e];
      try auto; set_tac.
    assert (mF = m1) by (eapply validTypes_exec in find_e1; eauto); subst.
    apply validRanges_single in valid_e1.
    destruct valid_e1 as [iv1' [err1' [v1' [map_e [eval_real_e bounds_e]]]]].
    rewrite map_e in Heqo0; inversion Heqo0; subst.
-    pose proof (meps_0_deterministic _ eval_real_e H5); subst. clear H5.
+    pose proof (meps_0_deterministic _ eval_real_e H6); subst. clear H6.
    split.
-    + eexists; eexists.
+    + specialize (deltas_matched (toRExp (Downcast mG e)) mG)
+        as (delta' & delta_some' & delta_bound').
+      eexists; eexists.
      eapply Downcast_dist'; eauto.
-      * instantiate (1 := 0%R);
-        rewrite Rabs_R0; auto using mTypeToR_pos_R.
-      * eapply toRExpMap_some with (e:= Downcast mG e); eauto. congruence.
+      eapply toRExpMap_some with (e:= Downcast mG e); eauto. congruence.
    + intros * eval_float.
      inversion eval_float; subst.
      eapply validErrorboundCorrectRounding; eauto.
      * simpl. eapply Downcast_dist'; eauto.
        { constructor; cbn; auto. }
+        { pose proof (R_orderedExps.eq_refl (Downcast m (Var R 1))).
+          destruct R_orderedExps.eq_dec as [Heq|Hneq]; auto; congruence. }
        { unfold updDefVars; cbn. rewrite mTypeEq_refl. auto. }
      * cbn; instantiate (1:=dVars); Flover_compute.
        rewrite L, L0; auto.
@@ -2241,20 +2249,22 @@ Proof.
 Qed.

 Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
-  forall (A:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err Gamma,
+  forall (A:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err Gamma DeltaMap,
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
    ssa f (NatSet.union fVars dVars) outVars ->
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
-    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
    validErrorboundCmd f Gamma A dVars = true ->
-    validTypesCmd f Gamma ->
+    validTypesCmd f Gamma DeltaMap ->
    validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
    FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
    (exists vF m,
-        bstep (toRCmd f) E2 (toRExpMap Gamma) vF m).
+        bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m).
 Proof.
  induction f;
-    intros * approxc1c2 ssa_f freeVars_subset eval_real valid_bounds
+    intros * deltas_matched approxc1c2 ssa_f freeVars_subset eval_real valid_bounds
                    valid_types valid_intv  A_res;
    cbn in *; Flover_compute; try congruence; type_conv; subst.
  - (* let-binding *)
@@ -2288,7 +2298,7 @@ Proof.
      eapply validTypes_exec in find_e; try eauto. subst.
      destruct valid_intv as [[valid_range_e valid_cont] valid_intv].
      destruct (IHf A (updEnv n v E1) (updEnv n vF E2) outVars fVars
-                    (NatSet.add n dVars) vR elo ehi err Gamma)
+                    (NatSet.add n dVars) vR elo ehi err Gamma DeltaMap)
        as [vF_res [m_res step_res]];
        eauto.
      { eapply ssa_equal_set; eauto.
@@ -2336,20 +2346,22 @@ Proof.
 Qed.

 Theorem validErrorboundCmd_sound (f:cmd Q):
-  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma,
+  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma DeltaMap,
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
    ssa f (NatSet.union fVars dVars) outVars ->
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
-    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
-    bstep (toRCmd f) E2 (toRExpMap Gamma) vF mF ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
+    bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF mF ->
    validErrorboundCmd f Gamma A dVars = true ->
-    validTypesCmd f Gamma ->
+    validTypesCmd f Gamma DeltaMap ->
    validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
    FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
    (Rabs (vR - vF) <= (Q2R err))%R.
 Proof.
  induction f;
-    intros * approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds
+    intros * deltas_matched approxc1c2 ssa_f freeVars_subset eval_real eval_float valid_bounds
                    valid_types valid_intv  A_res;
    cbn in *; Flover_compute; try congruence; type_conv; subst.
  - inversion eval_real;
@@ -2373,7 +2385,7 @@ Proof.
    eapply validTypes_exec in find_me; eauto; subst.
    type_conv; subst.
    apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
-               (NatSet.add n dVars) vR vF mF elo ehi err Gamma);
+               (NatSet.add n dVars) vR vF mF elo ehi err Gamma DeltaMap);
      eauto.
    + eapply approxUpdBound; try eauto; simpl in *.
      * eapply toRExpMap_some; eauto.

--- a/coq/ErrorValidationAA.v
+++ b/coq/ErrorValidationAA.v
--- a/coq/ExpressionSemantics.v
+++ b/coq/ExpressionSemantics.v
@@ -300,8 +300,9 @@ Lemma binary_unfolding b f1 f2 E v1 v2 m1 m2 m Gamma DeltaMap delta:
  eval_expr (updEnv 2 v2 (updEnv 1 v1 emptyEnv))
            (updDefVars (Binop b (Var R 1) (Var R 2)) m
                        (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 Gamma)))
-            (fun x m => if R_orderedExps.eq_dec x (Binop b (Var R 1) (Var R 2))
-                     then Some delta else None)
+            (fun x _ => if R_orderedExps.eq_dec x (Binop b (Var R 1) (Var R 2))
+                     then DeltaMap (Binop b f1 f2) m
+                     else None)
            (Binop b (Var R 1) (Var R 2)) (perturb (evalBinop b v1 v2) m delta) m.
 Proof.
  intros no_div_zero err_v delta_map eval_f1 eval_f2 eval_float.
@@ -335,8 +336,9 @@ Lemma fma_unfolding f1 f2 f3 E v1 v2 v3 m1 m2 m3 m Gamma DeltaMap delta:
            (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3) ) m
                        (updDefVars (Var R 3) m3 (updDefVars (Var R 2) m2
                                                             (updDefVars (Var R 1) m1 Gamma))))
-            (fun x m => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3))
-                     then Some delta else None)
+            (fun x _ => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3))
+                     then DeltaMap (Fma f1 f2 f3) m
+                     else None)
            (Fma (Var R 1) (Var R 2) (Var R 3)) (perturb (evalFma v1 v2 v3) m delta) m.
 Proof.
  intros err_v delta_map eval_f1 eval_f2 eval_f3 eval_float.
@@ -402,6 +404,38 @@ Proof.
        set_tac.
 Qed.

+Lemma eval_expr_det_ignore_bind2 e:
+  forall x v v_new m Gamma E DeltaMap,
+    eval_expr (updEnv x v_new E) Gamma DeltaMap e v m ->
+    ~ NatSet.In x (usedVars e) ->
+    eval_expr E Gamma DeltaMap e v m.
+Proof.
+  induction e; intros * eval_e no_usedVar *; cbn in *;
+    inversion eval_e; subst; try eauto.
+  - assert (n <> x).
+    { hnf. intros. subst. apply no_usedVar; set_tac. }
+    rewrite <- Nat.eqb_neq in H.
+    eapply Var_load.
+    + unfold updDefVars.
+      cbn.
+      apply beq_nat_false in H.
+      destruct (n ?= x)%nat eqn:?; try auto.
+    + unfold updEnv.
+      rewrite <- H1.
+      unfold updEnv.
+      now rewrite H.
+  - eapply Binop_dist'; eauto;
+      [ eapply IHe1 | eapply IHe2];
+      eauto;
+      hnf; intros; eapply no_usedVar;
+      set_tac.
+  - eapply Fma_dist'; eauto;
+      [eapply IHe1 | eapply IHe2 | eapply IHe3];
+      eauto;
+      hnf; intros; eapply no_usedVar;
+        set_tac.
+Qed.
+
 Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 DeltaMap:
  (forall e, Gamma1 e = Gamma2 e) ->
  eval_expr E Gamma1 DeltaMap e vR m ->
@@ -428,7 +462,7 @@ Proof.
  intros x; destruct (R_orderedExps.compare x n); auto.
 Qed.

-Lemma eval_expr_fixed_DeltaMap_functional E Gamma DeltaMap e v1 v2 m:
+Lemma eval_expr_functional E Gamma DeltaMap e v1 v2 m:
  eval_expr E Gamma DeltaMap e v1 m ->
  eval_expr E Gamma DeltaMap e v2 m ->
  v1 = v2.

--- a/coq/FPRangeValidator.v
+++ b/coq/FPRangeValidator.v
@@ -70,10 +70,10 @@ Ltac prove_fprangeval m v L1 R:=
  destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.

 Theorem FPRangeValidator_sound:
-  forall (e:expr Q) E1 E2 Gamma v m A fVars dVars,
+  forall (e:expr Q) E1 E2 Gamma DeltaMap v m A fVars dVars,
  approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
-  eval_expr E2 (toRExpMap Gamma) (toRExp e) v m ->
-  validTypes e Gamma ->
+  eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v m ->
+  validTypes e Gamma DeltaMap ->
  validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
  validErrorbound e Gamma A dVars = true ->
  FPRangeValidator e A Gamma dVars = true ->
@@ -241,4 +241,4 @@ Proof.
          rewrite NatSet.add_spec in H4; destruct H4;
            auto; subst; congruence. }
  - destruct H4. destruct H3. eapply FPRangeValidator_sound; eauto.
-Qed.
\ No newline at end of file
+Qed.
--- a/coq/RoundoffErrorValidator.v
+++ b/coq/RoundoffErrorValidator.v
@@ -3,7 +3,7 @@ From Coq

 From Flover
     Require Export Infra.ExpressionAbbrevs ErrorAnalysis ErrorValidation
-     ErrorValidationAA ExpressionSemanticsDeterministic RealRangeValidator
+     ErrorValidationAA ExpressionSemantics RealRangeValidator
     TypeValidator Environments.

 Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
@@ -21,10 +21,10 @@ Theorem RoundoffErrorValidator_sound:
    (nR : R) (err : error) (iv : intv) (Gamma : FloverMap.t mType) DeltaMap,
    (forall (e' : expr R) (m' : mType),
        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
-    validTypes e Gamma ->
+    validTypes e Gamma DeltaMap ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
    NatSet.Subset (usedVars e -- dVars) fVars ->
-    eval_expr_det E1 (toRTMap (toRExpMap Gamma)) (fun x m => Some 0%R) (toREval (toRExp e)) nR REAL ->
+    eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) nR REAL ->
    RoundoffErrorValidator e Gamma A dVars = true ->
    validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
    FloverMap.find e A = Some (iv, err) ->
@@ -34,7 +34,7 @@ Proof.
  unfold RoundoffErrorValidator.
  intros; cbn in *.
  destruct (validErrorbound e Gamma A dVars) eqn: Hivvalid.
-  - eapply validErrorbound_sound; eauto.
+  - admit.
  - destruct (validErrorboundAA e Gamma A dVars 1 (FloverMap.empty (affine_form Q))) eqn: Hafvalid;
      [|congruence].
    destruct p as (expr_map, noise).
@@ -58,7 +58,7 @@ Proof.
        [now rewrite FloverMapFacts.P.F.empty_in_iff|].
      split; eauto.
      eapply Hall; eauto; now rewrite FloverMapFacts.P.F.empty_in_iff.
-Qed.
+Admitted.

 Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
           (A:analysisResult) (dVars:NatSet.t) :=
@@ -71,19 +71,21 @@ Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
       end.

 Theorem RoundoffErrorValidatorCmd_sound f:
-  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma,
+  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma DeltaMap,
+    (forall (e' : expr R) (m' : mType),
+        exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
    approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
    ssa f (NatSet.union fVars dVars) outVars ->
    NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
-    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR vR REAL ->
    validErrorboundCmd f Gamma A dVars = true ->
    validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) ->
-    validTypesCmd f Gamma ->
+    validTypesCmd f Gamma DeltaMap ->
    FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
    (exists vF m,
-        bstep (toRCmd f) E2 (toRExpMap Gamma) vF m) /\
+        bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF m) /\
    (forall vF mF,
-    bstep (toRCmd f) E2 (toRExpMap Gamma) vF mF ->
+    bstep (toRCmd f) E2 (toRExpMap Gamma) DeltaMap vF mF ->
    (Rabs (vR - vF) <= (Q2R err))%R).
 Proof.
  intros.

--- a/coq/ssaPrgs.v
+++ b/coq/ssaPrgs.v
@@ -211,18 +211,31 @@ Proof.
 Qed.

 Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap
-      vR vR' m n c fVars dVars outVars:
+      vR vR' m m__e n c fVars dVars outVars:
  ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
  ~ (n ∈ fVars ∪ dVars) ->
-  eval_expr E Gamma DeltaMap e vR REAL ->
-  eval_expr (updEnv n vR' E) Gamma DeltaMap e vR REAL.
+  eval_expr E Gamma DeltaMap e vR m__e ->
+  eval_expr (updEnv n vR' E) Gamma DeltaMap e vR m__e.
 Proof.
  intros Hssa Hsub Hnotin Heval.
  eapply eval_expr_ignore_bind; [auto |].
  edestruct ssa_inv_let; eauto.
 Qed.

+Lemma eval_expr_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap
+      v v' m__e m n c fVars dVars outVars:
+  ssa (Let m__e n e' c) (fVars ∪ dVars) outVars ->
+  NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
+  ~ (n ∈ fVars ∪ dVars) ->
+  eval_expr (updEnv n v' E) Gamma DeltaMap e v m ->
+  eval_expr E Gamma DeltaMap e v m.
+Proof.
+  intros Hssa Hsub Hnotin Heval.
+  eapply eval_expr_det_ignore_bind2; [eauto |].
+  edestruct ssa_inv_let; eauto.
+Qed.
+
 (*
 Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
  (forall n, E1 n = E2 n)->