diff --git a/coq/AffineValidation.v b/coq/AffineValidation.v
index 9fcdb1e2135b2eaa91616709b86394a6812203fb..36bd8811be18282f7a2a0d2915be4bbac29ef2a9 100644
--- a/coq/AffineValidation.v
+++ b/coq/AffineValidation.v
@@ -57,8 +57,8 @@ Proof.
     destruct e5.
     + apply Ndec.Pcompare_Peqb in e8.
       congruence.
-    + apply Ndec.Pcompare_Peqb in Heq.
-      congruence.
+    + apply Nat.compare_eq in Heq; subst.
+      rewrite Nat.eqb_refl in H; congruence.
 Qed.
 
 Lemma usedVars_toREval_toRExp_compat e:
@@ -69,10 +69,10 @@ Proof.
   - now rewrite IHe1, IHe2, IHe3.
 Qed.
 
-Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma:
+Lemma validRanges_eq_compat (e1: expr Q) e2 A E Gamma fBits:
   Q_orderedExps.eq e1 e2 ->
-  validRanges e1 A E Gamma ->
-  validRanges e2 A E Gamma.
+  validRanges e1 A E Gamma fBits ->
+  validRanges e2 A E Gamma fBits.
 Proof.
   intros Heq.
   unfold Q_orderedExps.eq in Heq.
@@ -104,8 +104,8 @@ Proof.
     destruct e3.
     + apply Ndec.Pcompare_Peqb in e6.
       congruence.
-    + apply Ndec.Pcompare_Peqb in Heq.
-      congruence.
+    + apply Nat.compare_eq in Heq; subst.
+      rewrite Nat.eqb_refl in H; congruence.
   - intros valid1; destruct valid1 as [validsub1 validr1].
     specialize (IHc Heq validsub1).
     split; auto.
@@ -229,8 +229,8 @@ Proof.
     destruct e5.
     + apply Ndec.Pcompare_Peqb in e8.
       congruence.
-    + apply Ndec.Pcompare_Peqb in Heq.
-      congruence.
+    + apply Nat.compare_eq in Heq; subst.
+      rewrite Nat.eqb_refl in *; congruence.
 Qed.
 
 Definition updateExpMapIncr e new_af noise (emap: expressionsAffine) intv incr :=
@@ -745,15 +745,15 @@ Proof.
   congruence.
 Qed.
 
-Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma:
+Lemma validAffineBounds_validRanges e (A: analysisResult) E Gamma fBits:
   (exists map af vR aiv aerr,
       FloverMap.find e A = Some (aiv, aerr) /\
       isSupersetIntv (toIntv af) aiv = true /\
-      eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
+      eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
       af_evals (afQ2R af) vR map) ->
   exists iv err vR,
     FloverMap.find e A = Some (iv, err) /\
-    eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
+    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
     (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 Proof.
   intros sound_affine.
@@ -773,7 +773,7 @@ Proof.
   split; eauto using Rle_trans.
 Qed.
 
-Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap inoise map1 :=
+Definition checked_expressions (A: analysisResult) E Gamma fBits fVars dVars e iexpmap inoise map1 :=
   exists af vR aiv aerr,
     NatSet.Subset (usedVars e) (NatSet.union fVars dVars) /\
     FloverMap.find e A = Some (aiv, aerr) /\
@@ -781,17 +781,17 @@ Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap
     FloverMap.find e iexpmap = Some af /\
     fresh inoise af /\
     (forall n, (n >= inoise)%nat -> map1 n = None) /\
-    eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
-    validRanges e A E Gamma /\
+    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
+    validRanges e A E Gamma fBits /\
     af_evals (afQ2R af) vR map1.
 
-Lemma checked_expressions_contained A E Gamma fVars dVars e expmap1 expmap2 map1 map2 noise1 noise2:
+Lemma checked_expressions_contained A E Gamma fBits fVars dVars e expmap1 expmap2 map1 map2 noise1 noise2:
   contained_map map1 map2 ->
   contained_flover_map expmap1 expmap2 ->
   (noise2 >= noise1)%nat ->
   (forall n : nat, (n >= noise2)%nat -> map2 n = None) ->
-  checked_expressions A E Gamma fVars dVars e expmap1 noise1 map1 ->
-  checked_expressions A E Gamma fVars dVars e expmap2 noise2 map2.
+  checked_expressions A E Gamma fBits fVars dVars e expmap1 noise1 map1 ->
+  checked_expressions A E Gamma fBits fVars dVars e expmap2 noise2 map2.
 Proof.
   intros cont contf Hnoise Hvalidmap checked1.
   unfold checked_expressions in checked1 |-*.
@@ -800,10 +800,10 @@ Proof.
   intuition; eauto using fresh_monotonic, af_evals_map_extension.
 Qed.
 
-Lemma checked_expressions_flover_map_add_compat A E Gamma fVars dVars e e' af expmap noise map:
+Lemma checked_expressions_flover_map_add_compat A E Gamma fBits fVars dVars e e' af expmap noise map:
   Q_orderedExps.exprCompare e e' <> Eq ->
-  checked_expressions A E Gamma fVars dVars e' expmap noise map ->
-  checked_expressions A E Gamma fVars dVars e' (FloverMap.add e af expmap) noise map.
+  checked_expressions A E Gamma fBits fVars dVars e' expmap noise map ->
+  checked_expressions A E Gamma fBits fVars dVars e' (FloverMap.add e af expmap) noise map.
 Proof.
   intros Hneq checked1.
   unfold checked_expressions in checked1 |-*.
@@ -814,9 +814,9 @@ Proof.
 Qed.
 
 Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
-      fVars dVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
+      fVars dVars (E: env) Gamma fBits exprAfs noise iexpmap inoise map1:
   (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
-        checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
+        checked_expressions A E Gamma fBits fVars dVars e iexpmap inoise map1) ->
   (inoise > 0)%nat ->
   (forall n, (n >= inoise)%nat -> map1 n = None) ->
   validAffineBounds e A P dVars iexpmap inoise = Some (exprAfs, noise) ->
@@ -833,12 +833,12 @@ Lemma validAffineBounds_sound (e: expr Q) (A: analysisResult) (P: precond)
     fresh noise af /\
     (forall n, (n >= noise)%nat -> map2 n = None) /\
     (noise >= inoise)%nat /\
-    eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
-    validRanges e A E Gamma /\
+    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
+    validRanges e A E Gamma fBits /\
     af_evals (afQ2R af) vR map2 /\
     (forall e, FloverMap.find e iexpmap = None ->
           (exists af, FloverMap.find e exprAfs = Some af) ->
-          checked_expressions A E Gamma fVars dVars e exprAfs noise map2).
+          checked_expressions A E Gamma fBits fVars dVars e exprAfs noise map2).
 Proof.
   revert noise exprAfs inoise iexpmap map1.
   induction e;
@@ -885,7 +885,7 @@ Proof.
       specialize (fVarsSound H') as [vR [eMap interval_containment]].
       assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) (fromIntv (P n) inoise) iexpmap) = Some (fromIntv (P n) inoise)) as Hfind
         by (rewrite FloverMapFacts.P.F.add_eq_o; try auto; apply Q_orderedExps.exprCompare_refl).
-      assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Var Q n))) vR REAL) as Heeval
+      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Var Q n))) vR REAL) as Heeval
           by (constructor; auto; simpl; rewrite varsTyped; reflexivity).
       destruct (Qeq_bool (ivlo (P n)) (ivhi (P n))) eqn: Heq.
       * assert (af_evals (afQ2R (fromIntv (P n) inoise)) vR map1) as Hevals.
@@ -1137,7 +1137,7 @@ Proof.
     assert (FloverMap.find (elt:=affine_form Q) (Const m v) (FloverMap.add (Const m v) (fromIntv (v, v) noise) iexpmap) = Some (fromIntv (v, v) noise))
       by (rewrite FloverMapFacts.P.F.add_eq_o; try auto;
           apply Q_orderedExps.exprCompare_refl).
-    assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Const m v))) (perturb (Q2R v) REAL 0) REAL)
+    assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Const m v))) (perturb (Q2R v) REAL 0) REAL)
       by (constructor; simpl; rewrite Rabs_R0; lra).
     exists map1, (fromIntv (v, v) noise), (perturb (Q2R v) REAL 0), i, e.
     repeat split; auto.
@@ -1373,10 +1373,11 @@ Proof.
         apply plus_aff_sound; auto.
         eauto using af_evals_map_extension.
       }
-      assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Plus e1 e2)))
-                       (perturb (evalBinop Plus vR1 vR2) REAL 0) REAL)
-        by (replace REAL with (join REAL REAL) by trivial;
-            apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra; congruence).
+      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Plus e1 e2)))
+                       (perturb (evalBinop Plus vR1 vR2) REAL 0) REAL).
+      { eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
+        - rewrite Rabs_R0; cbn; lra.
+        - intros; cbn in *; contradiction. }
       exists ihmap2, (AffineArithQ.plus_aff af1 af2), (perturb (evalBinop Plus vR1 vR2) REAL 0)%R, aiv, aerr.
       rewrite plus_0_r.
       repeat split; eauto using AffineArithQ.plus_aff_preserves_fresh, fresh_monotonic.
@@ -1461,9 +1462,10 @@ Proof.
         unfold AffineArithQ.negate_aff.
         now apply AffineArithQ.fresh_mult_aff_const.
       }
-      assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Sub e1 e2))) (perturb (evalBinop Sub vR1 vR2) REAL 0) REAL)
-        by (replace REAL with (join REAL REAL) by trivial; apply Binop_dist;
-            try rewrite Rabs_R0; simpl; auto; try lra; congruence).
+      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Sub e1 e2))) (perturb (evalBinop Sub vR1 vR2) REAL 0) REAL).
+      { eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
+        - rewrite Rabs_R0; cbn; lra.
+        - intros; cbn in *; contradiction. }
       exists ihmap2, (AffineArithQ.subtract_aff af1 af2), (perturb (evalBinop Sub vR1 vR2) REAL 0)%R, aiv, aerr.
       repeat split; auto.
       * etransitivity; try exact ihcont1.
@@ -1556,9 +1558,10 @@ Proof.
             apply AffineArithQ.mult_aff_aux_preserves_fresh;
               apply fresh_inc; now rewrite afQ2R_fresh.
       }
-      assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Mult e1 e2))) (perturb (evalBinop Mult vR1 vR2) REAL 0) REAL)
-        by (replace REAL with (join REAL REAL) by trivial;
-            apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra; congruence).
+      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Mult e1 e2))) (perturb (evalBinop Mult vR1 vR2) REAL 0) REAL).
+      { eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
+        - rewrite Rabs_R0; cbn; lra.
+        - intros; cbn in *; contradiction. }
       assert (af_evals (afQ2R (AffineArithQ.mult_aff af1 af2 subnoise2)) (perturb (evalBinop Mult vR1 vR2) REAL 0) (updMap ihmap2 subnoise2 qMult)) by
           (unfold perturb; simpl evalBinop; rewrite afQ2R_mult_aff; assumption).
       assert (forall n : nat, (n >= subnoise2 + 1)%nat -> updMap ihmap2 subnoise2 qMult n = None).
@@ -1712,11 +1715,11 @@ Proof.
         apply Hsubvalidmap2.
         lia.
       }
-      assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Binop Div e1 e2))) (perturb (evalBinop Div vR1 vR2) REAL 0) REAL)
-        by (replace REAL with (join REAL REAL) by trivial;
-            apply Binop_dist; try rewrite Rabs_R0; simpl; auto; try lra;
-            intros _;
-            eauto using above_below_nonzero).
+      assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Binop Div e1 e2))) (perturb (evalBinop Div vR1 vR2) REAL 0) REAL).
+      { eapply Binop_dist' with (delta := 0%R); eauto; try congruence.
+        - rewrite Rabs_R0; cbn; lra.
+        - intros _; eauto using above_below_nonzero.
+        - intros; cbn in *; contradiction. }
       assert (af_evals (afQ2R (AffineArithQ.divide_aff af1 af2 subnoise2)) (perturb (evalBinop Div vR1 vR2) REAL 0) (updMap (updMap ihmap2 subnoise2 qInv) (subnoise2 + 1) qMult))
         by (unfold perturb; simpl evalBinop; rewrite afQ2R_divide_aff; auto).
       exists (updMap (updMap ihmap2 subnoise2 qInv) (subnoise2 + 1) qMult),
@@ -1954,9 +1957,10 @@ Proof.
       apply Hsubmapvalid3.
       lia.
     }
-    assert (eval_expr E (toRMap Gamma) (toREval (toRExp (Fma e1 e2 e3))) (perturb (evalFma vR1 vR2 vR3)REAL 0) REAL)
-      by (replace REAL with (join3 REAL REAL REAL) by trivial;
-          apply Fma_dist; try rewrite Rabs_R0; auto; simpl; lra).
+    assert (eval_expr E (toRMap Gamma) fBits (toREval (toRExp (Fma e1 e2 e3))) (perturb (evalFma vR1 vR2 vR3)REAL 0) REAL).
+    { eapply Fma_dist'; eauto; try congruence.
+      - rewrite Rabs_R0; cbn;  lra.
+      - intros. cbn in *. contradiction. }
     assert (af_evals (afQ2R (AffineArithQ.plus_aff af1 (AffineArithQ.mult_aff af2 af3 subnoise3))) (perturb (evalFma vR1 vR2 vR3) REAL 0) (updMap ihmap3 subnoise3 qMult)).
     {
       unfold perturb.
@@ -2142,6 +2146,7 @@ Proof.
       * rewrite FloverMapFacts.P.F.add_neq_o in Hsome; auto.
         apply checked_expressions_flover_map_add_compat; auto.
         apply visitedSubexpr; eauto.
+        Unshelve. all:exact 0%nat.
 Qed.
 
 Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (validVars: NatSet.t)
@@ -2164,24 +2169,24 @@ Fixpoint validAffineBoundsCmd (c: cmd Q) (A: analysisResult) (P: precond) (valid
   | Ret e => validAffineBounds e A P validVars exprsAf currentMaxNoise
   end.
 
-Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma vR vR' m n c fVars dVars outVars:
+Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma fBits vR vR' m 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 e vR REAL ->
-  eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) e vR REAL.
+  eval_expr E Gamma fBits e vR REAL ->
+  eval_expr (updEnv n vR' E) (updDefVars n REAL Gamma) fBits e vR REAL.
 Proof.
   intros Hssa Hsub Hnotin Heval.
   eapply eval_expr_ignore_bind; [auto |].
   edestruct ssa_inv_let; eauto.
 Qed.
 
-Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma vR' m n c fVars dVars outVars:
+Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma fBits vR' m n c fVars dVars outVars:
   ssa (Let m n e' c) (fVars ∪ dVars) outVars ->
   NatSet.Subset (usedVars e) (fVars ∪ dVars) ->
   ~ (n ∈ fVars ∪ dVars) ->
-  validRanges e A E Gamma ->
-  validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma).
+  validRanges e A E Gamma fBits ->
+  validRanges e A (updEnv n vR' E) (updDefVars n REAL Gamma) fBits.
 Proof.
   intros Hssa Hsub Hnotin Hranges.
   induction e.
@@ -2251,10 +2256,10 @@ Proof.
     rewrite usedVars_toREval_toRExp_compat; auto.
 Qed.
 
-Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
+Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond) fBits
       fVars dVars outVars (E: env) Gamma exprAfs noise iexpmap inoise map1:
   (forall e, (exists af, FloverMap.find e iexpmap = Some af) ->
-        checked_expressions A E Gamma fVars dVars e iexpmap inoise map1) ->
+        checked_expressions A E Gamma fBits fVars dVars e iexpmap inoise map1) ->
   (inoise > 0)%nat ->
   (forall n, (n >= inoise)%nat -> map1 n = None) ->
   validAffineBoundsCmd c A P dVars iexpmap inoise = Some (exprAfs, noise) ->
@@ -2272,12 +2277,12 @@ Lemma validAffineBoundsCmd_sound (c: cmd Q) (A: analysisResult) (P: precond)
     fresh noise af /\
     (forall n, (n >= noise)%nat -> map2 n = None) /\
     (noise >= inoise)%nat /\
-    bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) vR REAL /\
-    validRangesCmd c A E Gamma /\
+    bstep (toREvalCmd (toRCmd c)) E (toRMap Gamma) fBits vR REAL /\
+    validRangesCmd c A E Gamma fBits /\
     af_evals (afQ2R af) vR map2 /\
     (forall e, FloverMap.find e iexpmap = None ->
           (exists af, FloverMap.find e exprAfs = Some af) ->
-          exists E' Gamma' dVars, checked_expressions A E' Gamma' fVars dVars e exprAfs noise map2).
+          exists E' Gamma' dVars, checked_expressions A E' Gamma' fBits fVars dVars e exprAfs noise map2).
 Proof.
   revert E Gamma dVars iexpmap inoise exprAfs noise map1.
   induction c; intros * visitedExpr Hnoise Hmapvalid valid_bounds_cmd
diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v
index 2506531afff0961a0d4d067958fb52ea26e48d2d..eb84059b0042328847c03aa4283a22a6f8246a2b 100644
--- a/coq/CertificateChecker.v
+++ b/coq/CertificateChecker.v
@@ -12,9 +12,10 @@ From Flover
 Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
 
 (** Certificate checking function **)
-Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
-  let tMap := (typeMap defVars e (FloverMap.empty mType)) in
-  if (typeCheck e defVars tMap)
+Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
+           (P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t nat):=
+  let tMap := (typeMap defVars e (FloverMap.empty mType) fBits) in
+  if (typeCheck e defVars tMap fBits)
   then
     if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
     then RoundoffErrorValidator e tMap absenv NatSet.empty
@@ -26,7 +27,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) (P:precond) (de
    Apart from assuming two executions, one in R and one on floats, we assume that
    the real valued execution respects the precondition.
 **)
-Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVars:
+Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
+        defVars fBits:
   forall (E1 E2:env),
     approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
     (forall v, NatSet.In v (Expressions.usedVars e) ->
@@ -35,13 +37,13 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P defVa
     (forall v, NatSet.In v  (usedVars e) ->
           exists m : mType,
             defVars v = Some m) ->
-    CertificateChecker e absenv P defVars = true ->
+    CertificateChecker e absenv P defVars fBits = true ->
     exists iv err vR vF m,
       FloverMap.find e absenv = Some (iv, err) /\
-      eval_expr E1 (toRMap defVars) (toREval (toRExp e)) vR REAL /\
-      eval_expr E2 defVars (toRExp e) vF m /\
+      eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
+      eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
       (forall vF m,
-          eval_expr E2 defVars (toRExp e) vF m ->
+          eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
           (Rabs (vR - vF) <= Q2R err))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
@@ -68,19 +70,20 @@ Proof.
   { unfold vars_typed. intros; apply types_defined. set_tac. destruct H1; set_tac.
     split; try auto. hnf; intros; set_tac. }
   rename R into validFPRanges.
-  assert (validRanges e absenv E1 defVars) as valid_e.
+  assert (validRanges e absenv E1 defVars (toRBMap fBits)) as valid_e.
   { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
       auto. }
-  pose proof (validRanges_single _ _ _ _ valid_e) as valid_single;
+  pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_single;
     destruct valid_single as [iv_e [ err_e [vR [ map_e [eval_real real_bounds_e]]]]].
   destruct iv_e as [elo ehi].
-  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType)) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
+  edestruct (RoundoffErrorValidator_sound e (typeMap defVars e (FloverMap.empty mType) fBits) L approxE1E2 H0 eval_real R0 valid_e H1 map_e) as [[vF [mF eval_float]] err_bounded]; auto.
   exists (elo, ehi), err_e, vR, vF, mF; split; auto.
 Qed.
 
-Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
-  let tMap := typeMapCmd defVars f (FloverMap.empty mType) in
-  if (typeCheckCmd f defVars tMap && validSSA f (freeVars f))
+Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond)
+           defVars fBits:=
+  let tMap := typeMapCmd defVars f (FloverMap.empty mType) fBits in
+  if (typeCheckCmd f defVars tMap fBits && validSSA f (freeVars f))
   then
     if (RangeValidatorCmd f absenv P NatSet.empty) &&
        FPRangeValidatorCmd f absenv tMap NatSet.empty
@@ -88,7 +91,8 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) d
     else false
   else false.
 
-Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
+Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P
+        defVars fBits:
   forall (E1 E2:env),
     approxEnv E1 defVars absenv (freeVars f) NatSet.empty E2 ->
     (forall v, NatSet.In v (freeVars f) ->
@@ -97,13 +101,13 @@ Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P d
     (forall v, NatSet.In v (freeVars f) ->
           exists m : mType,
             defVars v = Some m) ->
-    CertificateCheckerCmd f absenv P defVars = true ->
+    CertificateCheckerCmd f absenv P defVars fBits = true ->
     exists iv err vR vF m,
       FloverMap.find  (getRetExp f) absenv = Some (iv,err) /\
-    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) vR REAL /\
-    bstep (toRCmd f) E2 defVars vF m /\
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
+    bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m /\
     (forall vF m,
-        bstep (toRCmd f) E2 defVars vF m ->
+        bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m ->
         (Rabs (vR - vF) <= Q2R (err))%R).
 (**
    The proofs is a simple composition of the soundness proofs for the range
@@ -129,11 +133,11 @@ Proof.
     destruct H0; set_tac. }
   assert (NatSet.Subset (freeVars f -- NatSet.empty) (freeVars f))
     as freeVars_contained by set_tac.
-  assert (validRangesCmd f absenv E1 defVars) as valid_f.
+  assert (validRangesCmd f absenv E1 defVars (toRBMap fBits)) as valid_f.
   { eapply RangeValidatorCmd_sound; eauto.
     unfold affine_dVars_range_valid; intros.
     set_tac. }
-  pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
+  pose proof (validRangesCmd_single _ _ _ _ _ valid_f) as valid_single.
   destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
   destruct iv as [f_lo f_hi].
   edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
diff --git a/coq/Commands.v b/coq/Commands.v
index 961081736c589fda9a83bf6ec4e4f6df4003c600..2ce84f5a3b93d6af993ce30b6a974fc6057d2f12 100644
--- a/coq/Commands.v
+++ b/coq/Commands.v
@@ -49,14 +49,14 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
   Define big step semantics for the Flover language, terminating on a "returned"
   result value
  **)
-Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
-  let_b m m' x e s E v res defVars:
-    eval_expr 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_expr E defVars e v m ->
-    bstep (Ret e) E defVars v m.
+Inductive bstep : cmd R -> env -> (nat -> option mType) -> (expr R -> option nat) -> R -> mType -> Prop :=
+  let_b m m' x e s E v res defVars fBits:
+    eval_expr E defVars fBits e v m ->
+    bstep s (updEnv x v E) (updDefVars x m defVars) fBits res m' ->
+    bstep (Let m x e s) E defVars fBits res m'
+ |ret_b m e E v defVars fBits:
+    eval_expr E defVars fBits e v m ->
+    bstep (Ret e) E defVars fBits v m.
 
 (**
   The free variables of a command are all used variables of exprressions
@@ -88,14 +88,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
   end.
 
 Lemma bstep_eq_env f:
-  forall E1 E2 Gamma v m,
+  forall E1 E2 Gamma fBits v m,
   (forall x, E1 x = E2 x) ->
-  bstep f E1 Gamma v m ->
-  bstep f E2 Gamma v m.
+  bstep f E1 Gamma fBits v m ->
+  bstep f E2 Gamma fBits v m.
 Proof.
   induction f; intros * eq_envs bstep_E1;
     inversion bstep_E1; subst; simpl in *.
-  -  eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
+  - eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
      eapply IHf. instantiate (1:=(updEnv n v0 E1)).
      + intros; unfold updEnv.
        destruct (x=? n); auto.
diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v
index d07f8d183b29856b68db8bd5c36d6466b1f0e787..b4d44704fc28c74b6244d906f22d5b800a9d9ea6 100644
--- a/coq/ErrorBounds.v
+++ b/coq/ErrorBounds.v
@@ -7,9 +7,9 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
 Require Import Flover.Infra.Abbrevs Flover.Infra.RationalSimps Flover.Infra.RealSimps Flover.Infra.RealRationalProps.
 Require Import Flover.Environments Flover.Infra.ExpressionAbbrevs.
 
-Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars:
-  eval_expr E1 (toRMap defVars) (Const REAL n) nR REAL ->
-  eval_expr E2 defVars (Const m n) nF m ->
+Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (m:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (Const REAL n) nR REAL ->
+  eval_expr E2 defVars fBits (Const m n) nF m ->
   (Rabs (nR - nF) <= computeErrorR n m)%R.
 Proof.
   intros eval_real eval_float.
@@ -30,14 +30,19 @@ Proof.
 Qed.
 
 Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
-  eval_expr E2 defVars (toRExp e1) e1F m1->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
-  eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
+      (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
+  eval_expr E2 defVars fBits (toRExp e1) e1F m1->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
+  eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
+              | _ => fBits e
+           end)
            (Binop Plus (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
@@ -50,22 +55,20 @@ Proof.
   assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
   subst; simpl in H3; auto.
   rewrite delta_0_deterministic in plus_real; auto.
-  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) (join REAL REAL) delta); auto.
+  rewrite (delta_0_deterministic (evalBinop Plus v1 v2) REAL delta); auto.
   unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in plus_real.
-  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in plus_real.
-  clear H5 H6 H7 v1 v2.
+  clear delta H2.
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in plus_real.
+  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in plus_real.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion plus_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H7; subst.
-  unfold updEnv; simpl.
-  unfold updEnv in H1,H6; simpl in *.
-  symmetry in H1,H6.
-  inversion H1; inversion H6; subst.
+  inversion H6; subst; inversion H7; subst.
+  unfold updEnv in H1,H12; simpl in *.
+  symmetry in H1,H12.
+  inversion H1; inversion H12; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear plus_float H4 H7 plus_real e1_real e1_float e2_real e2_float H8 H6 H1.
   repeat rewrite Rmult_plus_distr_l.
@@ -73,7 +76,7 @@ Proof.
   rewrite Rsub_eq_Ropp_Rplus.
   unfold computeErrorR.
   pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
-  destruct (join m0 m3);
+  destruct m;
     repeat rewrite Ropp_plus_distr; try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
   { repeat rewrite <- Rplus_assoc.
     assert (e1R + e2R + - e1F + - e2F = e1R + - e1F + e2R + - e2F)%R by lra.
@@ -83,13 +86,13 @@ Proof.
     apply Rabs_triang; apply Rplus_le_compat; try auto.
     rewrite Rplus_0_r.
     apply Rplus_le_compat; try auto. }
-  Focus 4.
+  4: {
     eapply Rle_trans.
     apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
     apply Rplus_le_compat; try auto.
     eapply Rle_trans.
     apply Rabs_triang.
-    rewrite Rabs_Ropp. apply Rplus_le_compat; auto.
+    rewrite Rabs_Ropp. apply Rplus_le_compat; auto. }
   all: eapply Rle_trans; try eapply H.
   all: setoid_rewrite Rplus_assoc at 2.
   all: eapply Rplus_le_compat; try auto.
@@ -103,14 +106,19 @@ Qed.
   Copy-Paste proof with minor differences, was easier then manipulating the evaluations and then applying the lemma
 **)
 Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
-      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
-  eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
-  eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
+      (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
+  eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
+  eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
+              | _ => fBits e
+           end)
            (Binop Sub (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
@@ -118,42 +126,38 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R: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 *)
-  inversion sub_real; subst;
+  inversion sub_real; subst.
   assert (m0 = REAL) by (eapply toRMap_eval_REAL; eauto).
   assert (m3 = REAL) by (eapply toRMap_eval_REAL; eauto).
   subst; simpl in H3; auto.
   rewrite delta_0_deterministic in sub_real; auto.
-  rewrite delta_0_deterministic; auto.
+  rewrite (delta_0_deterministic (evalBinop Sub v1 v2) REAL delta); auto.
   unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in sub_real.
-  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in sub_real.
-  clear H5 H6 H7 v1 v2.
+  clear delta H2.
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in sub_real.
+  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in sub_real.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion sub_float; subst.
   unfold perturb; simpl.
-  inversion H4; subst; inversion H7; subst.
-  unfold updEnv; simpl.
-  simpl in H0; simpl in H5; inversion H0; inversion H5; subst; clear H0 H5.
-  symmetry in H6, H1.
-  unfold updEnv in H6, H1; simpl in H6, H1.
-  inversion H6; inversion H1; subst.
+  inversion H6; subst; inversion H7; subst.
+  unfold updEnv in H1,H12; simpl in *.
+  symmetry in H1,H12.
+  inversion H1; inversion H12; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
-  clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H1 H6.
+  clear sub_float H4 H7 sub_real e1_real e1_float e2_real e2_float H8 H6 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   repeat rewrite Rsub_eq_Ropp_Rplus.
-  repeat rewrite Ropp_plus_distr.
   unfold computeErrorR.
   pose proof (Rabs_triang (e1R + - e1F) ((e2R + - e2F) + - ((e1F + e2F) * delta))).
-  destruct (join m0 m3);
+  destruct m;
     repeat rewrite Ropp_plus_distr; try rewrite Ropp_involutive;
       try rewrite plus_bounds_simplify; try rewrite Rplus_assoc.
   { repeat rewrite <- Rplus_assoc.
     assert (e1R + - e2R + - e1F + e2F = e1R + - e1F + - e2R + e2F)%R by lra.
-    rewrite H0; clear H0.
+    rewrite H1; clear H1.
     rewrite Rplus_assoc.
     eapply Rle_trans.
     apply Rabs_triang; apply Rplus_le_compat; try auto.
@@ -161,7 +165,7 @@ Proof.
     apply Rplus_le_compat; try auto.
     rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
     auto. }
-  Focus 4.
+  4: {
     eapply Rle_trans.
     apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
     apply Rplus_le_compat; try auto.
@@ -169,7 +173,7 @@ Proof.
     apply Rabs_triang.
     rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
     rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
-    auto.
+    auto. }
   all: eapply Rle_trans; try eapply Rabs_triang.
   all: setoid_rewrite Rplus_assoc at 2.
   all: eapply Rplus_le_compat; try auto.
@@ -181,14 +185,19 @@ Proof.
 Qed.
 
 Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
-  eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
-  eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
+  eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
+  eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
+              | _ => fBits e
+           end)
            (Binop Mult (Var R 1) (Var R 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
 Proof.
@@ -201,26 +210,25 @@ Proof.
   rewrite delta_0_deterministic in mult_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in mult_real.
-  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in mult_real.
-  clear H5 H6 v1 v2 H7 H2.
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in mult_real.
+  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in mult_real.
+  clear H3 H4.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion mult_float; subst.
   unfold perturb; simpl.
-  inversion H3; subst; inversion H6; subst.
+  inversion H4; subst; inversion H6; subst.
     unfold updEnv in *; simpl in *.
-    inversion H6; inversion H1; subst.
-    simpl in H8; simpl in H9; intros; inversion H5; subst.
+    inversion H1; inversion H11; subst.
+    cbn in *. inversion H0; inversion H10; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear mult_float H7 mult_real e1_real e1_float e2_real e2_float H6 H1.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
   unfold computeErrorR.
-  destruct (join m0 m3).
+  destruct m.
   all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
   { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
   all: eapply Rle_trans; try apply Rabs_triang.
@@ -230,14 +238,19 @@ Proof.
 Qed.
 
 Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
-      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
-  eval_expr E2 defVars (toRExp e1) e1F m1 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
-  eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
+  eval_expr E2 defVars fBits (toRExp e1) e1F m1 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
+  eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (Binop Div (toRExp e1) (toRExp e2))) vR REAL ->
   eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => fBits (toRExp (Binop b e1 e2))
+              | _ => fBits e
+           end)
            (Binop Div (Var R 1) (Var R 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
 Proof.
@@ -250,25 +263,25 @@ Proof.
   rewrite delta_0_deterministic in div_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalBinop in *; simpl in *.
-  clear delta H3 H2.
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real).
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in div_real.
-  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in div_real.
-  (* clear H5 H6 v1 v2. *)
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real).
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in div_real.
+  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in div_real.
+  clear H3 H4.
   (* Now unfold the float valued evaluation to get the deltas we need for the inequality *)
   inversion div_float; subst.
   unfold perturb; simpl.
-  inversion H3; subst; inversion H9; subst.
+  inversion H4; subst; inversion H6; subst.
     unfold updEnv in *; simpl in *.
-    inversion H8; inversion H1; subst.
+    inversion H1; inversion H11; subst.
+    cbn in *. inversion H0; inversion H10; subst.
   (* We have now obtained all necessary values from the evaluations --> remove them for readability *)
   clear div_float H0 H1 div_real e1_real e1_float e2_real e2_float.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
   unfold computeErrorR.
-  destruct (join m0 m3).
+  destruct m.
   all: try rewrite Ropp_plus_distr, <- Rplus_assoc.
   { rewrite Rplus_0_r. rewrite <- Rsub_eq_Ropp_Rplus; lra. }
   all: eapply Rle_trans; try apply Rabs_triang.
@@ -279,16 +292,21 @@ Qed.
 
 Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R)
       (e3:expr Q) (e3R:R) (e3F:R)
-      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) e1R REAL ->
-  eval_expr E2 defVars (toRExp e1) e1F m1->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) e2R REAL ->
-  eval_expr E2 defVars (toRExp e2) e2F m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) e3R REAL ->
-  eval_expr E2 defVars (toRExp e3) e3F m3->
-  eval_expr E1 (toRMap defVars) (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
+      (vR:R) (vF:R) (E1 E2:env) (m m1 m2 m3:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e1)) e1R REAL ->
+  eval_expr E2 defVars fBits (toRExp e1) e1F m1->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e2)) e2R REAL ->
+  eval_expr E2 defVars fBits (toRExp e2) e2F m2 ->
+  eval_expr E1 (toRMap defVars) fBits (toREval (toRExp e3)) e3R REAL ->
+  eval_expr E2 defVars fBits (toRExp e3) e3F m3->
+  eval_expr E1 (toRMap defVars) fBits (toREval (Fma (toRExp e1) (toRExp e2) (toRExp e3))) vR REAL ->
   eval_expr (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
            (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
+           (fun e =>
+              match e with
+              | Fma (Var _ 1) (Var _ 2) (Var _ 3) => fBits (toRExp (Fma e1 e2 e3))
+              | _ => fBits e
+           end)
            (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.
@@ -301,34 +319,34 @@ Proof.
   rewrite delta_0_deterministic in fma_real; auto.
   rewrite delta_0_deterministic; auto.
   unfold evalFma in *; simpl in *.
-  clear delta H3.
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real);
-    rewrite (meps_0_deterministic (toRExp e2) H6 e2_real);
-    rewrite (meps_0_deterministic (toRExp e3) H7 e3_real).
-  rewrite (meps_0_deterministic (toRExp e1) H5 e1_real) in fma_real.
-  rewrite (meps_0_deterministic (toRExp e2) H6 e2_real) in fma_real.
-  rewrite (meps_0_deterministic (toRExp e3) H7 e3_real) in fma_real.
-  clear H5 H6 v1 v2 v3 H7 H2.
+  clear delta H2.
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real);
+    rewrite (meps_0_deterministic (toRExp e2) H4 e2_real);
+    rewrite (meps_0_deterministic (toRExp e3) H5 e3_real).
+  rewrite (meps_0_deterministic (toRExp e1) H3 e1_real) in fma_real.
+  rewrite (meps_0_deterministic (toRExp e2) H4 e2_real) in fma_real.
+  rewrite (meps_0_deterministic (toRExp e3) H5 e3_real) in fma_real.
+  clear H3 H4 H5 v1 v2 v3.
   inversion fma_float; subst.
   unfold evalFma in *.
   unfold perturb; simpl.
-  inversion H3; subst; inversion H6; subst; inversion H7; subst.
-  unfold updEnv in *; simpl in *.
-  inversion H5; inversion H1; inversion H9; subst.
+  inversion H3; subst; inversion H4; subst; inversion H5; subst.
+  cbn in *.
+  inversion H0; inversion H1; inversion H6; inversion H7; inversion H12; inversion H13; subst.
   clear fma_float H7 fma_real e1_real e1_float e2_real e2_float e3_real e3_float H6 H1 H5 H9 H3 H0 H4 H8.
   repeat rewrite Rmult_plus_distr_l.
   rewrite Rmult_1_r.
   rewrite Rsub_eq_Ropp_Rplus.
   unfold computeErrorR.
-  destruct (join3 m0 m4 m5); rewrite Ropp_plus_distr.
+  destruct m; rewrite Ropp_plus_distr.
   { rewrite Rplus_0_r; hnf; right; f_equal; lra. }
-  Focus 4.
+  4: {
     rewrite <- Rplus_assoc.
     eapply Rle_trans.
     eapply Rabs_triang.
     rewrite Rabs_Ropp.
     eapply Rplus_le_compat; try auto.
-    hnf; right; f_equal; lra.
+    hnf; right; f_equal; lra. }
   all: repeat rewrite <- Rplus_assoc.
   all: setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
   all: repeat rewrite Rsub_eq_Ropp_Rplus.
@@ -344,11 +362,16 @@ Proof.
   all: rewrite Rabs_mult; apply Rmult_le_compat_l; auto using Rabs_pos.
 Qed.
 
-Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) (mEps m:mType) defVars:
-  eval_expr E1 (toRMap defVars) (toREval e) nR REAL ->
-  eval_expr E2 defVars e nF1 m ->
+Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
+      (mEps m:mType) defVars fBits:
+  eval_expr E1 (toRMap defVars) fBits (toREval e) nR REAL ->
+  eval_expr E2 defVars fBits e nF1 m ->
   eval_expr (updEnv 1 nF1 emptyEnv)
            (updDefVars 1 m defVars)
+           (fun e => match e with
+                  | Downcast m (Var _ 1) => fBits (Downcast m e)
+                  | _ => fBits e
+                  end )
            (toRExp (Downcast mEps (Var Q 1))) nF mEps->
   (Rabs (nR - nF1) <= err)%R ->
   (Rabs (nR - nF) <= err + computeErrorR nF1 mEps)%R.
diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v
index 20a74936b77d47c264c7918b7d0c57a806f88c56..8b269e6216b72a17b949a0821adc62d257be9000 100644
--- a/coq/ErrorValidation.v
+++ b/coq/ErrorValidation.v
@@ -1,4 +1,4 @@
-(**
+ (**
    This file contains the coq implementation of the error bound validator as
    well as its soundness proof. The function validErrorbound is the Error bound
    validator from the certificate checking process. Under the assumption that a
@@ -150,16 +150,16 @@ Proof.
 Qed.
 
 Lemma validErrorboundCorrectVariable_eval E1 E2 A (v:nat) e nR nlo nhi fVars
-      dVars Gamma exprTypes:
-    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
-    typeCheck (Var Q v) Gamma exprTypes = true ->
+      dVars Gamma exprTypes fBits:
+    eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (toRExp (Var Q v))) nR REAL ->
+    typeCheck (Var Q v) Gamma exprTypes fBits = true ->
     approxEnv E1 Gamma A fVars dVars E2 ->
-    validRanges (Var Q v) A E1 Gamma ->
+    validRanges (Var Q v) A E1 Gamma (toRBMap fBits) ->
     validErrorbound (Var Q v) exprTypes A dVars = true ->
     NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
     FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
     exists nF m,
-    eval_expr E2 Gamma (toRExp (Var Q v)) nF m.
+    eval_expr E2 Gamma (toRBMap fBits) (toRExp (Var Q v)) nF m.
 Proof.
   intros eval_real typing_ok approxCEnv bounds_valid error_valid v_sound A_var.
   apply validRanges_single in bounds_valid.
@@ -176,12 +176,12 @@ Proof.
 Qed.
 
 Lemma validErrorboundCorrectVariable:
-  forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars Gamma exprTypes,
-    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Var Q v))) nR REAL ->
-    eval_expr E2 Gamma (toRExp (Var Q v)) nF mF ->
-    typeCheck (Var Q v) Gamma exprTypes = true ->
+  forall E1 E2 A (v:nat) e nR nF mF nlo nhi fVars dVars Gamma exprTypes fBits,
+    eval_expr E1 (toRMap Gamma) (toRBMap fBits) (toREval (toRExp (Var Q v))) nR REAL ->
+    eval_expr E2 Gamma (toRBMap fBits) (toRExp (Var Q v)) nF mF ->
+    typeCheck (Var Q v) Gamma exprTypes fBits = true ->
     approxEnv E1 Gamma A fVars dVars E2 ->
-    validRanges (Var Q v) A E1 Gamma ->
+    validRanges (Var Q v) A E1 Gamma (toRBMap fBits) ->
     validErrorbound (Var Q v) exprTypes A dVars = true ->
     NatSet.Subset (NatSet.diff (usedVars (Var Q v)) dVars) fVars ->
     FloverMap.find (Var Q v) A = Some ((nlo, nhi), e) ->
@@ -218,10 +218,10 @@ Proof.
     simpl in *; auto.
 Qed.
 
-Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR  Gamma:
-    eval_expr E1 (toRMap Gamma) (toREval (toRExp (Const m n))) nR REAL ->
+Lemma validErrorboundCorrectConstant_eval E1 E2 m n nR Gamma fBits:
+    eval_expr E1 (toRMap Gamma) fBits (toREval (toRExp (Const m n))) nR REAL ->
     exists nF m',
-      eval_expr E2 Gamma (toRExp (Const m n)) nF m'.
+      eval_expr E2 Gamma fBits (toRExp (Const m n)) nF m'.
 Proof.
   intros eval_real .
   repeat eexists.
@@ -230,10 +230,11 @@ Proof.
   rewrite Rabs_R0. auto using mTypeToR_pos_R.
 Qed.
 
-Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma defVars:
-    eval_expr E1 (toRMap defVars) (toREval (toRExp (Const m n))) nR REAL ->
-    eval_expr E2 defVars (toRExp (Const m n)) nF m ->
-    typeCheck (Const m n) defVars Gamma = true ->
+Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma
+      defVars fBits:
+    eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Const m n))) nR REAL ->
+    eval_expr E2 defVars (toRBMap fBits) (toRExp (Const m n)) nF m ->
+    typeCheck (Const m n) defVars Gamma fBits = true ->
     validErrorbound (Const m n) Gamma A dVars = true ->
     (Q2R nlo <= nR <= Q2R nhi)%R ->
     FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
@@ -254,19 +255,45 @@ Proof.
   simpl in *; auto.
 Qed.
 
+Lemma isFixedPoint_lift m1 m2 e fBits f:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find e fBits = Some f) ->
+  isFixedPoint m1 -> isFixedPoint m2 -> toRBMap fBits (toRExp e) = Some f.
+Proof.
+  intros isvalid fixed_m1 fixed_m2.
+  apply toRBMap_some.
+  auto.
+Qed.
+
+Lemma isFixedPoint_lift3 m1 m2 m3 e fBits f:
+  (isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
+   FloverMap.find e fBits = Some f) ->
+  isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
+  toRBMap fBits (toRExp e) = Some f.
+Proof.
+  intros isvalid fixed_m1 fixed_m2 fixed_m3.
+  apply toRBMap_some.
+  auto.
+Qed.
+
 Lemma validErrorboundCorrectAddition E1 E2 A
       (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars:
-  m = join m1 m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
-  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
-  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Plus e1 e2) fBits = Some fBit) ->
+  Some m = join m1 m2 fBit ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Plus e1 e2))) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1 ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
   eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
+              | _ => toRBMap fBits e
+           end)
            (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m ->
-  typeCheck (Binop Plus e1 e2) defVars Gamma = true ->
+  typeCheck (Binop Plus e1 e2) defVars Gamma fBits = true ->
   validErrorbound (Binop Plus e1 e2) Gamma A dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -277,25 +304,35 @@ Lemma validErrorboundCorrectAddition E1 E2 A
   (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
-         subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
+  intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
+         subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_add
          err1_bounded err2_bounded.
+  assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find (Binop Plus e1 e2) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 + nF2) m 0%R); eauto.
+    eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - intros fixed_m1 fixed_m2.
+      specialize (validFBit fixed_m1 fixed_m2).
+      apply toRBMap_some in validFBit.
+      simpl in *; auto. }
+  clear subexpr_ok.
   cbn in *; Flover_compute; type_conv.
   eapply Rle_trans.
   eapply
     (add_abs_err_bounded e1 e2);
     try eauto.
-  pose proof (typingSoundnessExp _ _ R2 e1_float).
-  pose proof (typingSoundnessExp _ _ R1 e2_float).
   repeat destr_factorize.
   rename R0 into valid_error.
-  eapply Rle_trans.
-  apply Rplus_le_compat_l.
-  Focus 2.
-  rewrite Qle_bool_iff in valid_error.
-  apply Qle_Rle in valid_error.
-  repeat rewrite Q2R_plus in valid_error.
-  eauto.
+  canonize_hyps.
+  eapply Rle_trans; eauto.
+  repeat rewrite Q2R_plus.
+  repeat apply Rplus_le_compat_l.
   clear L R.
   assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
   pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded)
@@ -318,17 +355,23 @@ Qed.
 
 Lemma validErrorboundCorrectSubtraction E1 E2 A
       (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
-  m = join m1 m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
-  eval_expr E2 defVars (toRExp e1) nF1 m1->
-  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Sub e1 e2) fBits = Some fBit) ->
+  Some m = join m1 m2 fBit ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Sub e1 e2))) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
   eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
+              | _ => toRBMap fBits e
+           end)
            (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m ->
-  typeCheck (Binop Sub e1 e2) defVars Gamma = true ->
+  typeCheck (Binop Sub e1 e2) defVars Gamma fBits = true ->
   validErrorbound (Binop Sub e1 e2) Gamma A dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -339,24 +382,35 @@ Lemma validErrorboundCorrectSubtraction E1 E2 A
   (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
-         subexprr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
+  intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
+         subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_sub
          err1_bounded err2_bounded.
+  assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find (Binop Sub e1 e2) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 - nF2) m 0%R); eauto.
+    eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - intros fixed_m1 fixed_m2.
+      specialize (validFBit fixed_m1 fixed_m2).
+      apply toRBMap_some in validFBit.
+      simpl in *; auto. }
+  clear subexpr_ok.
   cbn in *; Flover_compute; type_conv.
   eapply Rle_trans.
   eapply (subtract_abs_err_bounded e1 e2); try eauto.
-  pose proof (typingSoundnessExp _ _ R2 e1_float).
-  pose proof (typingSoundnessExp _ _ R1 e2_float).
   repeat destr_factorize.
   rename R0 into valid_error.
   canonize_hyps.
   repeat rewrite Q2R_plus in valid_error.
   repeat rewrite Q2R_mult in valid_error.
   repeat rewrite Q2R_plus in valid_error.
-  eapply Rle_trans.
-  apply Rplus_le_compat_l.
-  Focus 2.
-  apply valid_error.
+  eapply Rle_trans; eauto.
+  repeat apply Rplus_le_compat_l.
   rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
   assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
   pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded)
@@ -850,17 +904,23 @@ Qed.
 
 Lemma validErrorboundCorrectMult E1 E2 A
       (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
-  m = join m1 m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
-  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
-  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Mult e1 e2) fBits = Some fBit) ->
+  Some m = join m1 m2 fBit ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Mult e1 e2))) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
   eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
+              | _ => toRBMap fBits e
+           end)
            (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m ->
-  typeCheck (Binop Mult e1 e2) defVars Gamma = true ->
+  typeCheck (Binop Mult e1 e2) defVars Gamma fBits = true ->
   validErrorbound (Binop Mult e1 e2) Gamma A dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -871,30 +931,38 @@ Lemma validErrorboundCorrectMult E1 E2 A
   (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
-         subexprr_ok valid_error valid_e1 valid_e2 A_e1 A_e2 A_mult
+  intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
+         subexpr_ok valid_error valid_intv1 valid_intv2 A_e1 A_e2 A_mult
          err1_bounded err2_bounded.
+  assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find (Binop Mult e1 e2) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 * nF2) m 0%R); eauto.
+    eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - intros fixed_m1 fixed_m2.
+      specialize (validFBit fixed_m1 fixed_m2).
+      apply toRBMap_some in validFBit.
+      simpl in *; auto. }
+  clear subexpr_ok.
   cbn in *; Flover_compute; type_conv; subst.
+  canonize_hyps.
   eapply Rle_trans.
   eapply (mult_abs_err_bounded e1 e2); eauto.
-  pose proof (typingSoundnessExp _ _ R2 e1_float).
-  pose proof (typingSoundnessExp _ _ R1 e2_float).
-  rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst.
-  clear H H0.
   rename R0 into valid_error.
   assert (0 <= Q2R err1)%R as err1_pos.
   { pose proof (err_always_positive e1 Gamma A dVars);
       eauto. }
   assert (0 <= Q2R err2)%R as err2_pos.
   { pose proof (err_always_positive e2 Gamma A dVars); eauto. }
-  clear R2 R1.
-  canonize_hyps.
   repeat rewrite Q2R_plus in valid_error.
   repeat rewrite Q2R_mult in valid_error.
   repeat rewrite <- maxAbs_impl_RmaxAbs in valid_error.
-  eapply Rle_trans.
-  Focus 2.
-  apply valid_error.
+  eapply Rle_trans; eauto.
   apply Rplus_le_compat.
   - eauto using multiplicationErrorBounded.
   - rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
@@ -921,17 +989,23 @@ Qed.
 
 Lemma validErrorboundCorrectDiv E1 E2 A
       (e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
-      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars:
-  m = join m1 m2 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
-  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
-  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
+      (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop Div e1 e2) fBits = Some fBit) ->
+  Some m = join m1 m2 fBit ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Binop Div e1 e2))) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
   eval_expr (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv))
            (updDefVars 2 m2 (updDefVars 1 m1 defVars))
+           (fun e =>
+              match e with
+              | Binop b (Var _ 1) (Var _ 2) => toRBMap fBits (toRExp (Binop b e1 e2))
+              | _ => toRBMap fBits e
+           end)
            (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m ->
-  typeCheck (Binop Div e1 e2) defVars Gamma = true ->
+  typeCheck (Binop Div e1 e2) defVars Gamma fBits = true ->
   validErrorbound (Binop Div e1 e2) Gamma A dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -943,16 +1017,29 @@ Lemma validErrorboundCorrectDiv E1 E2 A
   (Rabs (nR2 - nF2) <= (Q2R err2))%R ->
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
-         subexprr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1
-         A_e2 A_div err1_bounded err2_bounded.
+  intros validFBit mIsJoin e1_real e2_real eval_real e1_float e2_float eval_float
+         subexpr_ok valid_error valid_bounds_e1 valid_bounds_e2 no_div_zero_real A_e1 A_e2 A_div
+         err1_bounded err2_bounded.
+  assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find (Binop Div e1 e2) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 / nF2) m 0%R); eauto.
+    eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - intros; subst. inversion eval_float; subst.
+      inversion H5; cbn in *; hnf; intros subst. apply H6; subst; congruence.
+    - intros fixed_m1 fixed_m2.
+      specialize (validFBit fixed_m1 fixed_m2).
+      apply toRBMap_some in validFBit.
+      simpl in *; auto. }
+  clear subexpr_ok.
   cbn in *; Flover_compute; type_conv; subst.
   eapply Rle_trans.
   eapply (div_abs_err_bounded e1 e2); eauto.
-  pose proof (typingSoundnessExp _ _ R2 e1_float).
-  pose proof (typingSoundnessExp _ _ R0 e2_float).
-  rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst.
-  clear H H0.
   rename L0 into no_div_zero_float.
   assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
   pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
@@ -978,9 +1065,7 @@ Proof.
     apply Q_case_div_to_R_case_div in no_div_zero_float; apply Q_case_div_to_R_case_div in no_div_zero_real.
     assert (Q2R e2lo = 0 -> False)%R by (apply (lt_or_gt_neq_zero_lo _ (Q2R e2hi)); try auto; lra).
     assert (Q2R e2hi = 0 -> False)%R by (apply (lt_or_gt_neq_zero_hi (Q2R e2lo)); try auto; lra).
-    eapply Rle_trans.
-    Focus 2.
-    apply valid_error.
+    eapply Rle_trans; eauto.
     apply Rplus_le_compat.
     (* Error Propagation proof *)
     + clear A_e1 A_e2 valid_error eval_float eval_real e1_float
@@ -1022,7 +1107,7 @@ Proof.
         rewrite <- Q2R_plus in float_iv_neg.
         rewrite <- Q2R0_is_0 in float_iv_neg.
         rewrite <- Q2R0_is_0 in real_iv_neg.
-        pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv.
+        pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H1 err2_pos) as err_prop_inv.
         rewrite Q2R_plus in float_iv_neg.
         rewrite Q2R0_is_0 in float_iv_neg.
         rewrite Q2R0_is_0 in real_iv_neg.
@@ -1461,7 +1546,7 @@ Proof.
         rewrite <- Q2R_minus in float_iv_pos.
         rewrite <- Q2R0_is_0 in float_iv_pos.
         rewrite <- Q2R0_is_0 in real_iv_pos.
-        pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv.
+        pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_bounds_e2 H1 err2_pos) as err_prop_inv.
         rewrite Q2R_minus in float_iv_pos.
         rewrite Q2R0_is_0 in float_iv_pos.
         rewrite Q2R0_is_0 in real_iv_pos.
@@ -1776,20 +1861,20 @@ Proof.
     + assert (IVhi (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)) < 0 \/ 0 < IVlo (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))%R
         as no_div_zero_widen
              by (unfold widenInterval in *; simpl in *; rewrite Q2R_plus, Q2R_minus in no_div_zero_float; auto).
-      pose proof (IntervalArith.interval_division_valid _ _ no_div_zero_widen H H0) as valid_div_float.
+      pose proof (IntervalArith.interval_division_valid _ _ no_div_zero_widen H0 H1) as valid_div_float.
       unfold widenInterval in *; simpl in *.
       assert (e2lo - err2 == 0 -> False).
       * hnf; intros.
         destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra.
         assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra.
-        rewrite<- Q2R_minus, <- Q2R_plus in H4.
-        apply Rle_Qle in H4. lra.
+        rewrite<- Q2R_minus, <- Q2R_plus in H5.
+        apply Rle_Qle in H5. lra.
       * assert (e2hi + err2 == 0 -> False).
         { hnf; intros.
           destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra.
           assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra.
-          rewrite<- Q2R_minus, <- Q2R_plus in H5.
-          apply Rle_Qle in H5. lra. }
+          rewrite<- Q2R_minus, <- Q2R_plus in H6.
+          apply Rle_Qle in H6. lra. }
         { destruct valid_div_float.
           rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
           apply computeErrorR_up.
@@ -1810,45 +1895,53 @@ Proof.
     + hnf; intros.
       destruct no_div_zero_float as [float_iv | float_iv]; try lra.
       assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra.
-      rewrite<- Q2R_minus, <- Q2R_plus in H2.
-      apply Rle_Qle in H2. lra.
+      rewrite<- Q2R_minus, <- Q2R_plus in H3.
+      apply Rle_Qle in H3. lra.
     + assert (e2hi + err2 == 0 -> False).
       * hnf; intros.
         destruct no_div_zero_float as [float_iv | float_iv]; try lra.
         assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra.
-        rewrite<- Q2R_minus, <- Q2R_plus in H3.
-        apply Rle_Qle in H3. lra.
+        rewrite<- Q2R_minus, <- Q2R_plus in H4.
+        apply Rle_Qle in H4. lra.
       * unfold widenIntv; simpl.
         hnf. intros.
         assert (forall a, Qabs a == 0 -> a == 0).
         { intros. unfold Qabs in H4. destruct a.
-          rewrite <- Z.abs_0 in H4. inversion H4. rewrite Zmult_1_r in *.
-          rewrite Z.abs_0_iff in H6.
-          rewrite H6. rewrite Z.abs_0. hnf. simpl; auto. }
+          rewrite <- Z.abs_0 in H5. inversion H5. rewrite Zmult_1_r in *.
+          rewrite Z.abs_0_iff in H7.
+          rewrite H7. rewrite Z.abs_0. hnf. simpl; auto. }
         { assert (minAbs (e2lo - err2, e2hi + err2) == 0 -> False).
           - unfold minAbs. unfold fst, snd. apply Q.min_case_strong.
-            + intros. apply H6; rewrite H5; auto.
-            + intros. apply H1. rewrite (H4 (e2lo-err2) H6). hnf. auto.
-            + intros. apply H2. rewrite H4; auto. hnf; auto.
-          - rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H3.
-            rewrite (Qmult_inj_r) in H3; auto. }
+            + intros. apply H7; rewrite H6; auto.
+            + intros. apply H2. rewrite (H5 (e2lo-err2) H7). hnf. auto.
+            + intros. apply H3. rewrite H5; auto. hnf; auto.
+          - rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H4.
+            rewrite (Qmult_inj_r) in H4; auto. }
 Qed.
 
 Lemma validErrorboundCorrectFma E1 E2 A
-      (e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R) (e err1 err2 err3 :error)
-      (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars (m m1 m2 m3:mType) Gamma defVars:
-  m = join3 m1 m2 m3 ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e1)) nR1 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e2)) nR2 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e3)) nR3 REAL ->
-  eval_expr E1 (toRMap defVars) (toREval (toRExp (Fma e1 e2 e3))) nR REAL ->
-  eval_expr E2 defVars (toRExp e1) nF1 m1 ->
-  eval_expr E2 defVars (toRExp e2) nF2 m2 ->
-  eval_expr E2 defVars (toRExp e3) nF3 m3 ->
+      (e1:expr Q) (e2:expr Q) (e3: expr Q) (nR nR1 nR2 nR3 nF nF1 nF2 nF3: R)
+      (e err1 err2 err3 :error) (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi:Q) dVars
+      (m m1 m2 m3:mType) Gamma defVars fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
+   FloverMap.find (Fma e1 e2 e3) fBits = Some fBit) ->
+  Some m = join3 m1 m2 m3 fBit ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e1)) nR1 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e2)) nR2 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e3)) nR3 REAL ->
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (Fma e1 e2 e3))) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e1) nF1 m1 ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e2) nF2 m2 ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e3) nF3 m3 ->
   eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
            (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
+           (fun e =>
+              match e with
+              |Fma (Var _ 1) (Var _ 2) (Var _ 3) => toRBMap fBits (toRExp (Fma e1 e2 e3))
+              |_ => toRBMap fBits e
+              end)
            (toRExp (Fma (Var Q 1) (Var Q 2) (Var Q 3))) nF m ->
-  typeCheck (Fma e1 e2 e3) defVars Gamma = true ->
+  typeCheck (Fma e1 e2 e3) defVars Gamma fBits = true ->
   validErrorbound (Fma e1 e2 e3) Gamma A dVars = true ->
   (Q2R e1lo <= nR1 <= Q2R e1hi)%R ->
   (Q2R e2lo <= nR2 <= Q2R e2hi)%R ->
@@ -1862,23 +1955,35 @@ Lemma validErrorboundCorrectFma E1 E2 A
   (Rabs (nR3 - nF3) <= (Q2R err3))%R ->
   (Rabs (nR - nF) <= (Q2R e))%R.
 Proof.
-  intros mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float e3_float eval_float
-         subexprr_ok valid_error valid_e1 valid_e2 valid_e3 A_e1 A_e2 A_e3 A_fma
-         err1_bounded err2_bounded err3_bounded.
+  intros validFBits mIsJoin e1_real e2_real e3_real eval_real e1_float e2_float
+         e3_float eval_float subexpr_ok valid_error valid_e1 valid_e2 valid_e3
+         A_e1 A_e2 A_e3 A_fma err1_bounded err2_bounded err3_bounded.
+  assert (FloverMap.find e1 Gamma = Some m1) as type_e1.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e2 Gamma = Some m2) as type_e2.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find e3 Gamma = Some m3) as type_e3.
+  { eapply typingSoundnessExp; eauto.
+    cbn in subexpr_ok; Flover_compute; auto. }
+  assert (FloverMap.find (Fma e1 e2 e3) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (evalFma nF1 nF2 nF3) m 0%R); eauto.
+    eapply Fma_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - intros fixed_m1 fixed_m2 fixed_m3.
+      specialize (validFBits fixed_m1 fixed_m2 fixed_m3).
+      apply toRBMap_some in validFBits.
+      simpl in *; auto. }
+  clear subexpr_ok.
   cbn in *; Flover_compute; type_conv; subst.
   eapply Rle_trans.
   eapply (fma_abs_err_bounded e1 e2 e3); eauto.
-  pose proof (typingSoundnessExp _ _ R4 e1_float).
-  pose proof (typingSoundnessExp _ _ R3 e2_float).
-  pose proof (typingSoundnessExp _ _ R2 e3_float).
-  rewrite H in Heqo0; rewrite H0 in Heqo1; rewrite H1 in Heqo2;
-    inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
   rename R0 into valid_error.
   assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma A dVars); eauto).
   assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma A dVars); eauto).
   assert (0 <= Q2R err3)%R as err3_pos by (eapply (err_always_positive e3 Gamma A dVars); eauto).
-  apply Qle_bool_iff in valid_error.
-  apply Qle_Rle in valid_error.
+  canonize_hyps.
   repeat rewrite Q2R_plus in valid_error.
   repeat rewrite Q2R_mult in valid_error.
   repeat rewrite Q2R_plus in valid_error.
@@ -1930,58 +2035,97 @@ Proof.
       lra.
 Qed.
 
-Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars:
-  eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
-  eval_expr E2 defVars (toRExp e) nF1 m ->
+Lemma validErrorboundCorrectRounding E1 E2 A (e: expr Q) (nR nF nF1: R)
+      (err err':error) (elo ehi alo ahi: Q) dVars (m: mType)
+      (mEps:mType) Gamma defVars fBits:
+  eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) nR REAL ->
+  eval_expr E2 defVars (toRBMap fBits) (toRExp e) nF1 m ->
   eval_expr (updEnv 1 nF1 emptyEnv)
            (updDefVars 1 m defVars)
-           (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon ->
-  typeCheck (Downcast machineEpsilon e) defVars Gamma = true ->
-  validErrorbound (Downcast machineEpsilon e) Gamma A dVars = true ->
+           (fun enew =>
+              match enew with
+              | Downcast mEps (Var _ 1) => toRBMap fBits (toRExp (Downcast mEps e))
+              | _ => toRBMap fBits enew
+              end)
+           (toRExp (Downcast mEps (Var Q 1))) nF mEps ->
+  typeCheck (Downcast mEps e) defVars Gamma fBits = true ->
+  validErrorbound (Downcast mEps e) Gamma A dVars = true ->
   (Q2R elo <= nR <= Q2R ehi)%R ->
   FloverMap.find e A = Some ((elo, ehi), err) ->
-  FloverMap.find (Downcast machineEpsilon e) A = Some ((alo, ahi), err') ->
+  FloverMap.find (Downcast mEps e) A = Some ((alo, ahi), err') ->
   (Rabs (nR - nF1) <= (Q2R err))%R ->
   (Rabs (nR - nF) <= (Q2R err'))%R.
 Proof.
   intros eval_real eval_float eval_float_rnd subexprr_ok valid_error valid_intv
          A_e A_rnd err_bounded.
   cbn in *; Flover_compute; type_conv; subst.
+  inversion eval_float_rnd; subst.
   eapply Rle_trans.
   eapply round_abs_err_bounded; eauto.
-  assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (auto).
-  pose proof (distance_gives_iv _ _ valid_intv_c err_bounded) as dgi.
-  destruct dgi as [dgi1 dgi2]; simpl in dgi1, dgi2.
-  canonize_hyps.
-  eapply Rle_trans; eauto.
-  rewrite Q2R_plus.
-  apply Rplus_le_compat_l.
-  rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
-  apply computeErrorR_up.
-  apply contained_leq_maxAbs.
-  simpl in *; split; try rewrite Q2R_plus in *;
-    try rewrite Q2R_minus in *;
-    lra.
+  - eapply Downcast_dist'; eauto.
+    inversion H5; cbn in *; subst.
+    eapply Var_load; cbn; auto.
+  - assert (contained nR (Q2R elo, Q2R ehi)) as valid_intv_c by (auto).
+    pose proof (distance_gives_iv _ _ valid_intv_c err_bounded) as dgi.
+    destruct dgi as [dgi1 dgi2]; simpl in dgi1, dgi2.
+    canonize_hyps.
+    eapply Rle_trans; eauto.
+    rewrite Q2R_plus.
+    apply Rplus_le_compat_l.
+    rewrite computeErrorQ_computeErrorR, <- maxAbs_impl_RmaxAbs_iv.
+    apply computeErrorR_up.
+    apply contained_leq_maxAbs.
+    simpl in *; split; try rewrite Q2R_plus in *;
+      try rewrite Q2R_minus in *;
+      lra.
 Qed.
 
+(*
+
+  assert (FloverMap.find (Binop Plus e1 e2) Gamma = Some m).
+  { eapply typingSoundnessExp with (E:=E2) (v:=perturb (nF1 + nF2) m 0%R); eauto.
+    eapply Binop_dist' with (delta:=0%R) (fBit:=fBit); eauto; try congruence.
+    - rewrite Rabs_R0. apply mTypeToR_pos_R; auto.
+    - inversion eval_float; subst.
+      inversion H3; inversion H4; cbn in *; subst.
+      inversion H0; inversion H11; rewrite <- H9.
+      destruct (isFixedPointB m0) eqn:?;
+               destruct (isFixedPointB m3) eqn:?;
+               [ | destruct m0, m3; cbn in *; try congruence
+                 | destruct m0, m3; cbn in *; try congruence|].
+      + subst.
+        pose proof (isFixedPoint_lift _ _ _ _ fPoint_defined) as isfPoint_R.
+        rewrite <- isFixedPoint_isFixedPointB in *.
+        simpl in *.
+        rewrite H8 in *; auto.
+        specialize (isfPoint_R Heqb Heqb0); congruence.
+      + rewrite <- isFixedPoint_isFixedPointB_false in *.
+        apply join_float; auto.
+
+    - intros fixed_m1 fixed_m2.
+      specialize (validFBit fixed_m1 fixed_m2).
+      apply toRBMap_some in validFBit.
+      simpl in *; auto. }
+ *)
+
 (**
    Soundness theorem for the error bound validator.
    Proof is by induction on the exprression e.
    Each case requires the application of one of the soundness lemmata proven before
  **)
 Theorem validErrorbound_sound (e:expr Q):
-  forall E1 E2 fVars dVars A nR err elo ehi Gamma defVars,
-    typeCheck e defVars Gamma = true ->
+  forall E1 E2 fVars dVars A nR err elo ehi Gamma defVars fBits,
+    typeCheck e defVars Gamma fBits = true ->
     approxEnv E1 defVars A fVars dVars E2 ->
     NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
-    eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
+    eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) nR REAL ->
     validErrorbound e Gamma A dVars = true ->
-    validRanges e A E1 defVars ->
+    validRanges e A E1 defVars (toRBMap fBits) ->
     FloverMap.find e A = Some ((elo,ehi),err) ->
     (exists nF m,
-      eval_expr E2 defVars (toRExp e) nF m) /\
+      eval_expr E2 defVars (toRBMap fBits) (toRExp e) nF m) /\
     (forall nF m,
-        eval_expr E2 defVars (toRExp e) nF m ->
+        eval_expr E2 defVars (toRBMap fBits) (toRExp e) nF m ->
     (Rabs (nR - nF) <= (Q2R err))%R).
 Proof.
   revert e; induction e;
@@ -1990,7 +2134,7 @@ Proof.
   - split.
     + eapply validErrorboundCorrectVariable_eval; eauto.
     + intros * eval_float. eapply validErrorboundCorrectVariable; eauto.
-  - pose proof (validRanges_single _ _ _ _ valid_intv) as valid_const.
+  - pose proof (validRanges_single _ _ _ _ _ valid_intv) as valid_const.
     destruct valid_const as [? [ ? [? [? [? ?]]]]].
     rewrite H in A_eq; inversion A_eq; subst.
     rewrite (meps_0_deterministic _ eval_real H0) in *; auto.
@@ -2005,9 +2149,10 @@ Proof.
     cbn in *; Flover_compute; try congruence; type_conv; subst;
     destruct u; Flover_compute; try congruence.
     inversion eval_real; subst.
-    destruct (IHe E1 E2 fVars dVars A v1 e0 (fst i) (snd i) Gamma defVars) as [[nF [mF eval_float]] valid_bounds_e];
+    destruct valid_intv as [valid_rec [iv [err_e [vR [? [? ?]]]]]].
+    destruct (IHe E1 E2 fVars dVars A v1 e0 (fst i) (snd i) Gamma defVars fBits)
+      as [[nF [mF eval_float]] valid_bounds_e];
       eauto.
-    + destruct valid_intv; auto.
     + destruct i; auto.
     + split.
       * exists (evalUnop Neg nF); exists mF.
@@ -2017,122 +2162,254 @@ Proof.
         apply bound_flip_sub.
         canonize_hyps.
         rewrite R1; eapply valid_bounds_e; eauto.
-  - cbn in *. rewrite A_eq in *.
-    Flover_compute; try congruence; type_conv; subst; simpl in *.
+  - simpl in valid_intv.
+    destruct valid_intv
+        as [[nodiv_zero [valid_e1 valid_e2]] valid_bin].
+    cbn in valid_error. Flover_compute; try congruence.
     inversion eval_real; subst.
-    assert (m0 = REAL /\ m3 = REAL) as [? ?] by (split; eapply toRMap_eval_REAL; eauto); subst.
-    destruct i as [ivlo1 ivhi1]; destruct i0 as [ivlo2 ivhi2];
-      rename e into err1; rename e0 into err2.
-    destruct valid_intv as [[no_div_zero_real [valid_e1 valid_e2]] ?].
-    destruct (IHe1 E1 E2 fVars dVars A v1 err1 ivlo1 ivhi1 Gamma defVars)
-      as [[vF1 [mF1 eval_float_e1]] bounded_e1];
-      try auto; set_tac.
-    destruct (IHe2 E1 E2 fVars dVars A v2 err2 ivlo2 ivhi2 Gamma defVars)
-      as [[vF2 [mF2 eval_float_e2]] bounded_e2];
-      try auto; set_tac.
+    destruct (IHe1 E1 E2 fVars dVars A v1 e (fst i) (snd i) Gamma defVars fBits)
+      as [[nF1 [mF1 eval_float1]] valid_bounds_e1]; try auto.
+    { cbn in *; Flover_compute; auto. }
+    { set_tac. split; set_tac. }
+    { pose proof (toRMap_eval_REAL _ H3); subst. auto. }
+    { destruct i; auto. }
+    destruct (IHe2 E1 E2 fVars dVars A v2 e0 (fst i0) (snd i0) Gamma defVars fBits)
+      as [[nF2 [mF2 eval_float2]] valid_bounds_e2]; try auto.
+    { cbn in *; Flover_compute; auto. }
+    { set_tac. split; set_tac. }
+    { pose proof (toRMap_eval_REAL _ H4); subst. auto. }
+    { destruct i0; auto. }
     apply validRanges_single in valid_e1;
       apply validRanges_single in valid_e2.
-    destruct valid_e1 as [iv1' [ err1' [v1' [map_e1 [eval_real_e1 bounds_e1]]]]].
-    inversion Heqo0; rewrite map_e1 in Heqo1; inversion Heqo1; subst.
-    pose proof (meps_0_deterministic _ eval_real_e1 H5); subst. clear H5.
-    destruct valid_e2 as [iv2' [err2' [v2' [map_e2 [eval_real_e2 bounds_e2]]]]].
-    rewrite map_e2 in Heqo3; inversion Heqo3; subst.
-    pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6.
-    assert (b = Div -> ~ (vF2 = 0)%R) as no_div_zero.
+    destruct valid_e1 as [iv1 [ err1 [v1' [map_e1 [eval_real_e1 bounds_e1]]]]].
+    destruct valid_e2 as [iv2 [ err2 [v2' [map_e2 [eval_real_e2 bounds_e2]]]]].
+    assert (m1 = REAL /\ m2 = REAL) as [? ?] by (split; eapply toRMap_eval_REAL; eauto); subst.
+    pose proof (meps_0_deterministic _ eval_real_e1 H3); subst.
+    pose proof (meps_0_deterministic _ eval_real_e2 H4); subst.
+    rewrite map_e1, map_e2 in *.
+    inversion Heqo0; inversion Heqo1; subst.
+    rename i into iv1; rename e into err1; rename i0 into iv2;
+      rename e0 into err2.
+    assert (contained nF1 (widenInterval (Q2R (fst iv1), Q2R (snd iv1)) (Q2R err1)))
+      as bounds_float_e1.
+    { eapply distance_gives_iv; simpl;
+        try eauto. }
+    assert (contained nF2 (widenInterval (Q2R (fst iv2), Q2R (snd iv2)) (Q2R err2)))
+      as bounds_float_e2.
+    { eapply distance_gives_iv; simpl;
+        try eauto. }
+    assert (b = Div -> ~ (nF2 = 0)%R) as no_div_zero.
     { intros; subst; simpl in *.
       andb_to_prop R0.
       apply le_neq_bool_to_lt_prop in L0.
-      assert (contained vF1 (widenInterval (Q2R ivlo1, Q2R ivhi1) (Q2R err1)))
-        as bounds_float_e1.
-      { eapply distance_gives_iv; simpl;
-          try eauto. }
-      assert (contained vF2 (widenInterval (Q2R ivlo2, Q2R ivhi2) (Q2R err2)))
-        as bounds_float_e2.
-      { eapply distance_gives_iv; simpl;
-          try eauto. }
       simpl in *. canonize_hyps.
       intro; subst.
       rewrite <- Q2R0_is_0 in bounds_float_e2.
       destruct L0 as [nodivzero | nodivzero];
         apply Qlt_Rlt in nodivzero;
-        try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; lra.
-    }
+        try rewrite Q2R_plus in *; try rewrite Q2R_minus in *; lra. }
+    assert (exists fBit,
+               isFixedPoint mF1 ->
+               isFixedPoint mF2 ->
+               FloverMap.find (Binop b e1 e2) fBits = Some fBit)
+      as fixedPoint_defined.
+    { eapply typingFixedPoint_binop_defined; eauto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto. }
+    destruct fixedPoint_defined as [fBitF fPoint_defined].
+    pose proof (isFixedPoint_lift _ _ _ _ fPoint_defined) as fPoint_prop.
+    assert (exists m, join mF1 mF2 fBitF = Some m) as join_exists.
+    { eapply typingBinop_join_defined; eauto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto. }
+    destruct join_exists as  [m_j join_exists].
     split.
-    + repeat eexists; econstructor; eauto.
-      instantiate (1 := 0%R).
+    + eexists; exists m_j.
+      eapply Binop_dist' with (delta:= 0%R) (fBit:=fBitF); eauto.
       rewrite Rabs_R0.
       apply mTypeToR_pos_R.
     + intros * eval_float.
-      clear eval_float_e1 eval_float_e2.
+      clear eval_float1 eval_float2 join_exists H8 mF1 mF2 fPoint_defined fPoint_prop.
       inversion eval_float; subst.
-      eapply (binary_unfolding _ H11 H5 H6 H10) in eval_float; try auto.
+      assert (exists fBit,
+                 isFixedPoint m1 ->
+                 isFixedPoint m2 ->
+                 FloverMap.find (Binop b e1 e2) fBits = Some fBit)
+        as fixedPoint_defined.
+      { eapply typingFixedPoint_binop_defined; eauto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto. }
+      destruct fixedPoint_defined as [fBit2 fBit_defined].
+      pose proof (isFixedPoint_lift _ _ _ _ fBit_defined) as fixed_prop.
+      simpl in fixed_prop.
+      assert (join m1 m2 fBit2 = Some m0).
+      { rewrite <- H14.
+        destruct (isFixedPointB m1) eqn:m1_fixed;
+          destruct (isFixedPointB m2) eqn:m2_fixed;
+          [ | destruct m1, m2; cbn in *; try congruence
+            | destruct m1, m2; cbn in *; try congruence |].
+        - rewrite <- isFixedPoint_isFixedPointB in *.
+          rewrite H13 in fixed_prop; try auto.
+          specialize (fixed_prop m1_fixed m2_fixed).
+          inversion fixed_prop; auto.
+        - rewrite <- isFixedPoint_isFixedPointB_false in *.
+          apply join_float; auto. }
+      eapply (binary_unfolding _ H10 fixed_prop H H6 H7 H8) in eval_float; try auto.
       destruct b.
       * eapply (validErrorboundCorrectAddition (e1:=e1) A); eauto.
-        { cbn. instantiate (1:=Gamma). Flover_compute.
-          rewrite mTypeEq_refl, R2, R1; auto. }
         { cbn. instantiate (1:=dVars); Flover_compute.
           rewrite L, L1, R; simpl; auto. }
+        { destruct iv1; auto. }
+        { destruct iv2; auto. }
       * eapply (validErrorboundCorrectSubtraction (e1:=e1) A); eauto.
-        { cbn; instantiate (1:=Gamma); Flover_compute; auto.
-          rewrite mTypeEq_refl, R2, R1; auto. }
         { cbn; instantiate (1:=dVars); Flover_compute.
           rewrite L, L1, R; simpl; auto. }
+        { destruct iv1; auto. }
+        { destruct iv2; auto. }
       *  eapply (validErrorboundCorrectMult (e1 := e1) A); eauto.
-        { cbn; instantiate (1:=Gamma); Flover_compute; auto.
-          rewrite mTypeEq_refl, R2, R1; auto. }
         { cbn; instantiate (1:=dVars); Flover_compute.
           rewrite L, L1, R; simpl; auto. }
+        { destruct iv1; auto. }
+        { destruct iv2; auto. }
       * eapply (validErrorboundCorrectDiv (e1 := e1) A); eauto.
-        { cbn; instantiate (1:=Gamma); Flover_compute; auto.
-          rewrite mTypeEq_refl, R2, R1; auto. }
         { cbn; instantiate (1:=dVars); Flover_compute.
           rewrite L, L1, L0, R; simpl; auto. }
-  - cbn in *. rewrite A_eq in *.
-    Flover_compute; try congruence; type_conv; subst; simpl in *.
+        { destruct iv1; auto. }
+        { destruct iv2; auto. }
+  - simpl in valid_intv.
+    destruct valid_intv
+        as [[valid_e1 [valid_e2 valid_e3]] valid_bin].
+    cbn in valid_error. Flover_compute; try congruence.
     inversion eval_real; subst.
-    assert (m0 = REAL /\ m4 = REAL /\ m5 = REAL) as [? [? ?]] by (split; try split; eapply toRMap_eval_REAL; eauto); subst.
-    destruct i as [ivlo1 ivhi1]; destruct i0 as [ivlo2 ivhi2]; destruct i1 as [ivlo3 ivhi3];
-      rename e into err1; rename e0 into err2; rename e4 into err3.
-    destruct valid_intv as  [[valid_e1 [valid_e2 valid_e3]] valid_intv].
-    destruct (IHe1 E1 E2 fVars dVars A v1 err1 ivlo1 ivhi1 Gamma defVars)
-      as [[vF1 [mF1 eval_float_e1]] bounded_e1];
-      try auto; set_tac.
-    destruct (IHe2 E1 E2 fVars dVars A v2 err2 ivlo2 ivhi2 Gamma defVars)
-      as [[vF2 [mF2 eval_float_e2]] bounded_e2];
-      try auto; set_tac.
-    destruct (IHe3 E1 E2 fVars dVars A v3 err3 ivlo3 ivhi3 Gamma defVars)
-      as [[vF3 [mF3 eval_float_e3]] bounded_e3];
-      try auto; set_tac.
+    destruct (IHe1 E1 E2 fVars dVars A v1 e (fst i) (snd i) Gamma defVars fBits)
+      as [[nF1 [mF1 eval_float1]] valid_bounds_e1]; try auto.
+    { cbn in *; Flover_compute; auto. }
+    { set_tac. split; set_tac. }
+    { pose proof (toRMap_eval_REAL _ H3); subst. auto. }
+    { destruct i; auto. }
+    destruct (IHe2 E1 E2 fVars dVars A v2 e0 (fst i0) (snd i0) Gamma defVars fBits)
+      as [[nF2 [mF2 eval_float2]] valid_bounds_e2]; try auto.
+    { cbn in *; Flover_compute; auto. }
+    { set_tac. split; set_tac. }
+    { pose proof (toRMap_eval_REAL _ H4); subst. auto. }
+    { destruct i0; auto. }
+    destruct (IHe3 E1 E2 fVars dVars A v3 e4 (fst i1) (snd i1) Gamma defVars fBits)
+      as [[nF3 [mF3 eval_float3]] valid_bounds_e3]; try auto.
+    { cbn in *; Flover_compute; auto. }
+    { set_tac. split; set_tac. }
+    { pose proof (toRMap_eval_REAL _ H5); subst. auto. }
+    { destruct i1; auto. }
     apply validRanges_single in valid_e1;
       apply validRanges_single in valid_e2;
       apply validRanges_single in valid_e3.
-    destruct valid_e1 as [iv1' [ err1' [v1' [map_e1 [eval_real_e1 bounds_e1]]]]].
-    rewrite map_e1 in Heqo1; inversion Heqo1; subst.
-    pose proof (meps_0_deterministic _ eval_real_e1 H5); subst; clear H5.
-    destruct valid_e2 as [iv2' [err2' [v2' [map_e2 [eval_real_e2 bounds_e2]]]]].
-    rewrite map_e2 in Heqo3; inversion Heqo3; subst.
-    pose proof (meps_0_deterministic _ eval_real_e2 H6); subst; clear H6.
-    destruct valid_e3 as [iv3' [err3' [v3' [map_e3 [eval_real_e3 bounds_e3]]]]].
-    rewrite map_e3 in Heqo5; inversion Heqo5; subst.
-    pose proof (meps_0_deterministic _ eval_real_e3 H7); subst; clear H7.
+    destruct valid_e1 as [iv1 [ err1 [v1' [map_e1 [eval_real_e1 bounds_e1]]]]].
+    destruct valid_e2 as [iv2 [ err2 [v2' [map_e2 [eval_real_e2 bounds_e2]]]]].
+    destruct valid_e3 as [iv3 [ err3 [v3' [map_e3 [eval_real_e3 bounds_e3]]]]].
+    assert (m1 = REAL /\ m2 = REAL /\ m3 = REAL) as [? [? ?]]
+        by (repeat split; eapply toRMap_eval_REAL; eauto); subst.
+    pose proof (meps_0_deterministic _ eval_real_e1 H3); subst.
+    pose proof (meps_0_deterministic _ eval_real_e2 H4); subst.
+    pose proof (meps_0_deterministic _ eval_real_e3 H5); 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;
+      rename e0 into err2; rename i1 into iv3; rename e4 into err3.
+    assert (contained nF1 (widenInterval (Q2R (fst iv1), Q2R (snd iv1)) (Q2R err1)))
+      as bounds_float_e1.
+    { eapply distance_gives_iv; simpl;
+        try eauto. }
+    assert (contained nF2 (widenInterval (Q2R (fst iv2), Q2R (snd iv2)) (Q2R err2)))
+      as bounds_float_e2.
+    { eapply distance_gives_iv; simpl;
+        try eauto. }
+    assert (contained nF3 (widenInterval (Q2R (fst iv3), Q2R (snd iv3)) (Q2R err3)))
+      as bounds_float_e3.
+    { eapply distance_gives_iv; simpl;
+        try eauto. }
+    assert (exists fBit,
+               isFixedPoint mF1 ->
+               isFixedPoint mF2 ->
+               isFixedPoint mF3 ->
+               FloverMap.find (Fma e1 e2 e3) fBits = Some fBit)
+      as fixedPoint_defined.
+    { eapply typingFixedPoint_fma_defined; eauto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto. }
+    destruct fixedPoint_defined as [fBitF fPoint_defined].
+    pose proof (isFixedPoint_lift3 _ _ _ _ _ fPoint_defined) as fPoint_prop.
+    assert (exists m, join3 mF1 mF2 mF3 fBitF = Some m) as join_exists.
+    { eapply typingFma_join_defined; eauto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto.
+      - eapply typingSoundnessExp; eauto.
+        cbn in typing_ok; Flover_compute; auto. }
+    destruct join_exists as [m_j join_exists].
     split.
-    + repeat eexists; econstructor; eauto.
-      rewrite Rabs_right; try lra.
+    + eexists; exists m_j; econstructor; eauto.
       instantiate (1 := 0%R).
+      rewrite Rabs_R0.
       apply mTypeToR_pos_R.
-      apply Rle_ge.
-      hnf; right; reflexivity.
     + intros * eval_float.
-      clear eval_float_e1 eval_float_e2 eval_float_e3.
+      clear eval_float1 eval_float2 eval_float3 mF1 mF2 mF3 fPoint_defined fPoint_prop join_exists.
       inversion eval_float; subst.
-      eapply (fma_unfolding _ H4 H5 H8 H9) in eval_float; try auto.
+      assert (exists fBit,
+                 isFixedPoint m1 ->
+                 isFixedPoint m2 ->
+                 isFixedPoint m3 ->
+                 FloverMap.find (Fma e1 e2 e3) fBits = Some fBit)
+        as fixedPoint_defined.
+      { eapply typingFixedPoint_fma_defined; eauto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto. }
+      destruct fixedPoint_defined as [fBit2 fBit_defined].
+      pose proof (isFixedPoint_lift3 _ _ _ _ _ fBit_defined) as fixed_prop.
+      simpl in fixed_prop.
+      assert (join3 m1 m2 m3 fBit2 = Some m0).
+      { rewrite <- H15.
+        edestruct (typingFma_fixedPoint_case e1 e2 e3 (m1:=m1) (m2:=m2) (m3:=m3)
+                                             defVars Gamma fBits)
+        as [all_fixed | none_fixed]; eauto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - eapply typingSoundnessExp; eauto.
+          cbn in typing_ok; Flover_compute; auto.
+        - andb_to_prop all_fixed.
+          rewrite <- isFixedPoint_isFixedPointB in *.
+          rewrite H14 in fixed_prop; try auto.
+          specialize (fixed_prop L2 R3 R2).
+          inversion fixed_prop; auto.
+        - destruct none_fixed as [? [? ?]].
+          rewrite <- isFixedPoint_isFixedPointB_false in *.
+          unfold join3.
+          erewrite join_float with (f1:=fBit2) (f2:=fBit0); eauto.
+          destruct (join m2 m3 fBit0) eqn:?; try auto.
+          assert (~ isFixedPoint m4).
+          { rewrite isFixedPoint_isFixedPointB_false.
+            destruct m2, m3; cbn in *; try congruence; inversion Heqo3;
+              cbn; auto.
+            contradiction. }
+          simpl. eapply join_float; eauto. }
+      symmetry in H.
+      eapply (fma_unfolding _ fixed_prop H H6 H7 H10 H11) in eval_float; try auto.
       eapply (validErrorboundCorrectFma (e1:=e1) (e2:=e2) (e3:=e3) A); eauto.
-      { simpl.
-        rewrite Heqo.
-        rewrite Heqo2.
-        rewrite Heqo4.
-        rewrite Heqo6.
-        rewrite mTypeEq_refl, R2, R3, R4; auto. }
       { simpl.
         rewrite A_eq.
         rewrite Heqo.
@@ -2140,13 +2417,16 @@ Proof.
         rewrite map_e1, map_e2, map_e3.
         inversion Heqo0; subst.
         auto. }
+      { destruct iv1; auto. }
+      { destruct iv2; auto. }
+      { destruct iv3; auto. }
   - cbn in *; Flover_compute; try congruence; type_conv; subst.
     inversion eval_real; subst.
     apply REAL_least_precision in H1.
     subst.
     destruct i as [ivlo_e ivhi_e]; rename e0 into err_e.
     destruct valid_intv as [valid_e1 valid_intv].
-    destruct (IHe E1 E2 fVars dVars A v1 err_e ivlo_e ivhi_e Gamma defVars)
+    destruct (IHe E1 E2 fVars dVars A v1 err_e ivlo_e ivhi_e Gamma defVars fBits)
       as [[vF [mF eval_float_e]] bounded_e];
       try auto; set_tac.
     pose proof (typingSoundnessExp _ _ R eval_float_e).
@@ -2174,18 +2454,19 @@ Proof.
 Qed.
 
 Theorem validErrorboundCmd_gives_eval (f:cmd Q) :
-  forall (A:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars,
-    typeCheckCmd f defVars Gamma = true ->
+  forall (A:analysisResult) E1 E2 outVars fVars dVars vR elo ehi err Gamma
+    defVars fBits,
+    typeCheckCmd f defVars Gamma fBits = true ->
     approxEnv E1 defVars 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 (toRMap defVars) vR REAL ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL ->
     validErrorboundCmd f Gamma A dVars = true ->
-    validRangesCmd f A E1 defVars ->
+    validRangesCmd f A E1 defVars (toRBMap fBits) ->
     vars_typed (NatSet.union fVars dVars) defVars ->
     FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
     (exists vF m,
-        bstep (toRCmd f) E2 defVars vF m).
+        bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m).
 Proof.
   induction f;
     intros * type_f approxc1c2 ssa_f freeVars_subset eval_real valid_bounds
@@ -2221,7 +2502,7 @@ Proof.
       destruct valid_intv as [[valid_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
-                    (updDefVars n m1 defVars))
+                    (updDefVars n m1 defVars) fBits)
         as [vF_res [m_res step_res]];
         eauto.
       { eapply ssa_equal_set; eauto.
@@ -2267,15 +2548,15 @@ Proof.
 Qed.
 
 Theorem validErrorboundCmd_sound (f:cmd Q):
-  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma defVars,
-    typeCheckCmd f defVars Gamma = true ->
+  forall A E1 E2 outVars fVars dVars vR vF mF elo ehi err Gamma defVars fBits,
+    typeCheckCmd f defVars Gamma fBits = true ->
     approxEnv E1 defVars 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 (toRMap defVars) vR REAL ->
-    bstep (toRCmd f) E2 defVars vF mF ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL ->
+    bstep (toRCmd f) E2 defVars (toRBMap fBits) vF mF ->
     validErrorboundCmd f Gamma A dVars = true ->
-    validRangesCmd f A E1 defVars ->
+    validRangesCmd f A E1 defVars (toRBMap fBits) ->
     vars_typed (NatSet.union fVars dVars) defVars ->
     FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
     (Rabs (vR - vF) <= (Q2R err))%R.
@@ -2305,7 +2586,7 @@ Proof.
       simpl in *.
     apply (IHf A (updEnv n v E1) (updEnv n v0 E2) outVars fVars
                (NatSet.add n dVars) vR vF mF elo ehi err Gamma
-               (updDefVars n m1 defVars));
+               (updDefVars n m1 defVars) fBits);
       eauto.
     + eapply approxUpdBound; try eauto.
       simpl in *.
diff --git a/coq/ErrorValidationAA.v b/coq/ErrorValidationAA.v
index 0d7ad56e27318798618cbcc48228645f827f0f23..14c139614878806110845a70d6a5c006f070c38f 100644
--- a/coq/ErrorValidationAA.v
+++ b/coq/ErrorValidationAA.v
@@ -219,17 +219,17 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
   |Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
   end.
 
-Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e
-           (initMap:FloverMap.t (affine_form Q)) currNoise (M1:noise_mapping) vR :=
-    eval_expr E1 (toRMap Gamma) (toREval (toRExp e)) vR REAL ->
-  exists (af:affine_form Q) (vF:R) m aiv aerr,
-    eval_expr E2 Gamma (toRExp e) vF m /\
-    FloverMap.find (elt:=intv * error) e A = Some (aiv, aerr) /\
-    FloverMap.find (elt:= affine_form Q) e initMap = Some af /\
-    fresh currNoise af /\
-    (forall n, (n >= currNoise)%nat -> M1 n = None) /\
-    let mAbs := maxAbs (toIntv af) in
-    (Rabs (vR - vF) <= (Q2R mAbs))%R.
+(* Definition checked_error_expressions (A: analysisResult) (E1 E2:env) Gamma e *)
+(*            (initMap:FloverMap.t (affine_form Q)) currNoise (M1:noise_mapping) vR := *)
+(*     eval_expr E1 (toRMap Gamma) (toREval (toRExp e)) vR REAL -> *)
+(*   exists (af:affine_form Q) (vF:R) m aiv aerr, *)
+(*     eval_expr E2 Gamma (toRExp e) vF m /\ *)
+(*     FloverMap.find (elt:=intv * error) e A = Some (aiv, aerr) /\ *)
+(*     FloverMap.find (elt:= affine_form Q) e initMap = Some af /\ *)
+(*     fresh currNoise af /\ *)
+(*     (forall n, (n >= currNoise)%nat -> M1 n = None) /\ *)
+(*     let mAbs := maxAbs (toIntv af) in *)
+(*     (Rabs (vR - vF) <= (Q2R mAbs))%R. *)
 
 (* Theorem validErrorboundAA_sound e: *)
 (*   forall E1 E2 P Gamma defVars nR A elo ehi tMap fVars dVars currNoise maxNoise initMap resMap M1, *)
diff --git a/coq/Expressions.v b/coq/Expressions.v
index 09aa4e6c64aa294ee1b133c2f5a6064daa9cbbc9..9a95bd6345ed3a1b975201c64547ec20d84ed854 100644
--- a/coq/Expressions.v
+++ b/coq/Expressions.v
@@ -457,11 +457,11 @@ Proof.
 Qed.
 
 Lemma eval_expr_ignore_bind e:
-  forall x v m Gamma E,
-    eval_expr E Gamma e v m ->
+  forall x v m Gamma E fBits,
+    eval_expr E Gamma fBits e v m ->
     ~ NatSet.In x (usedVars e) ->
     forall m_new v_new,
-    eval_expr (updEnv x v_new E) (updDefVars x m_new Gamma) e v m.
+    eval_expr (updEnv x v_new E) (updDefVars x m_new Gamma) fBits e v m.
 Proof.
   induction e; intros * eval_e no_usedVar *; cbn in *;
     inversion eval_e; subst; try eauto.
diff --git a/coq/FPRangeValidator.v b/coq/FPRangeValidator.v
index 9db3a1e9ba5131e3d859328f12c72c38c32df00f..145cc7c50e46d367d177c2fefeca6131fc853c1d 100644
--- a/coq/FPRangeValidator.v
+++ b/coq/FPRangeValidator.v
@@ -57,7 +57,7 @@ Ltac prove_fprangeval m v L1 R:=
   unfold normal, Normal, validValue, Denormal in *; canonize_hyps;
   try rewrite orb_true_iff in *;
   destruct L1; destruct R; canonize_hyps;
-  rewrite <- Rabs_eq_Qabs in *;
+  try rewrite <- Rabs_eq_Qabs in *;
   Q2R_to_head;
   rewrite <- Q2R_minus, <- Q2R_plus in *;
   repeat (match goal with
@@ -69,17 +69,19 @@ 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 tMap fVars dVars,
+  forall (e:expr Q) E1 E2 Gamma v m A tMap fVars dVars fBits,
   approxEnv E1 Gamma A fVars dVars E2 ->
-  eval_expr E2 Gamma (toRExp e) v m ->
-  typeCheck e Gamma tMap = true ->
-  validRanges e A E1 Gamma ->
+  eval_expr E2 Gamma (toRBMap fBits) (toRExp e) v m ->
+  typeCheck e Gamma tMap fBits = true ->
+  validRanges e A E1 Gamma (toRBMap fBits) ->
   validErrorbound e tMap A dVars = true ->
   FPRangeValidator e A tMap dVars = true ->
   NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars ->
   vars_typed (NatSet.union fVars dVars) Gamma ->
  (forall v, NatSet.In v dVars ->
-        exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
+       exists vF m, E2 v = Some vF /\
+               FloverMap.find (Var Q v) tMap = Some m /\
+               validFloatValue vF m) ->
   validFloatValue v m.
 Proof.
   intros *.
@@ -89,7 +91,7 @@ Proof.
     as type_e
       by (eapply typingSoundnessExp; eauto).
   unfold validFloatValue.
-  pose proof (validRanges_single _ _ _ _ H2) as valid_e.
+  pose proof (validRanges_single _ _ _ _ _ H2) as valid_e.
   destruct valid_e as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]].
   destruct iv_e as  [e_lo e_hi].
   assert (Rabs (vR - v) <= Q2R (err_e))%R.
@@ -119,37 +121,83 @@ Proof.
   - Flover_compute; destruct u; Flover_compute; try congruence.
     type_conv; subst.
     prove_fprangeval m0 v L1 R.
-  - Flover_compute; try congruence.
-    type_conv; subst.
-    prove_fprangeval (join m0 m1) v L1 R.
-  - Flover_compute; try congruence.
-    type_conv; subst.
-    prove_fprangeval (join3 m0 m1 m2) v L1 R.
+  - inversion H0; subst.
+    assert (FloverMap.find e1 tMap = Some m1) as type_m1.
+    { eapply typingSoundnessExp; eauto.
+      Flover_compute; auto. }
+    assert (FloverMap.find e2 tMap = Some m2) as type_m2.
+    { eapply typingSoundnessExp; eauto.
+      Flover_compute; auto. }
+    rewrite type_m1, type_m2 in *.
+    destruct (isFixedPointB m1) eqn:?;
+             destruct (isFixedPointB m2) eqn:?;
+             [ | destruct m1, m2; cbn in *; congruence
+               | destruct m1, m2; cbn in *; congruence | ];
+      simpl in H1.
+    + Flover_compute; try congruence.
+      type_conv; subst.
+      prove_fprangeval m0 (perturb (evalBinop b v1 v2) m0 delta) L1 R.
+    + Flover_compute; try congruence.
+      type_conv; subst.
+      prove_fprangeval m0 (perturb (evalBinop b v1 v2) m0 delta) L1 R.
+  - inversion H0; subst.
+    assert (FloverMap.find e1 tMap = Some m1) as type_m1.
+    { eapply typingSoundnessExp; eauto.
+      clear H4 H3.
+      Flover_compute; auto. }
+    assert (FloverMap.find e2 tMap = Some m2) as type_m2.
+    { eapply typingSoundnessExp; eauto.
+      clear H4 H3.
+      Flover_compute; auto. }
+    assert (FloverMap.find e3 tMap = Some m3) as type_m3.
+    { eapply typingSoundnessExp; eauto.
+      clear H4 H3.
+      Flover_compute; auto. }
+    rewrite type_m1, type_m2, type_m3 in *.
+    edestruct typingFma_fixedPoint_case with (e1:=e1) (e2:=e2) (e3:=e3)
+      as [all_fixed | [m1_float [m2_float m3_float]]];
+      eauto.
+    + cbn. clear H3 H4.
+      rewrite type_m1, type_m2, type_m3, type_e.
+      eauto.
+    + andb_to_prop all_fixed.
+      rewrite L0, R0, R in *.
+      simpl in H1.
+      Flover_compute; try congruence.
+      type_conv; subst.
+      prove_fprangeval m0 (perturb (evalFma v1 v2 v3) m0 delta) L1 R.
+    + rewrite m1_float, m2_float, m3_float in *;
+        simpl in H1.
+      Flover_compute; try congruence.
+      type_conv; subst.
+      prove_fprangeval m0 (perturb (evalFma v1 v2 v3) m0 delta) L1 R.
   - Flover_compute; try congruence.
     type_conv; subst.
     prove_fprangeval m v L1 R.
 Qed.
 
 Lemma FPRangeValidatorCmd_sound (f:cmd Q):
-  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars,
+  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars fBits,
   approxEnv E1 Gamma A fVars dVars E2 ->
   ssa f (NatSet.union fVars dVars) outVars ->
-  bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
-  bstep (toRCmd f) E2 Gamma v m ->
-  typeCheckCmd f Gamma tMap = true ->
-  validRangesCmd f A E1 Gamma ->
+  bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) (toRBMap fBits) vR m ->
+  bstep (toRCmd f) E2 Gamma (toRBMap fBits) v m ->
+  typeCheckCmd f Gamma tMap fBits = true ->
+  validRangesCmd f A E1 Gamma (toRBMap fBits) ->
   validErrorboundCmd f tMap A dVars = true ->
   FPRangeValidatorCmd f A tMap dVars = true ->
   NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars ->
   vars_typed (NatSet.union fVars dVars) Gamma ->
  (forall v, NatSet.In v dVars ->
-        exists vF m, E2 v = Some vF /\ FloverMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) ->
+       exists vF m, E2 v = Some vF /\
+               FloverMap.find (Var Q v) tMap = Some m /\
+               validFloatValue vF m) ->
   validFloatValue v m.
 Proof.
   induction f; intros;
     simpl in *;
-    (match_pat (bstep _ _ (toRMap _) _ _) (fun H => inversion H; subst; simpl in *));
-     (match_pat (bstep _ _ Gamma _ _) (fun H => inversion H; subst; simpl in *));
+    (match_pat (bstep _ _ (toRMap _) _ _ _) (fun H => inversion H; subst; simpl in *));
+     (match_pat (bstep _ _ Gamma _ _ _) (fun H => inversion H; subst; simpl in *));
       repeat match goal with
              | H : _ = true |- _ => andb_to_prop H
              end.
@@ -158,7 +206,7 @@ Proof.
         match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
         Flover_compute.
         destruct H4 as [[valid_e valid_rec] valid_single].
-        pose proof (validRanges_single _ _ _ _ valid_e) as valid_e_single.
+        pose proof (validRanges_single _ _ _ _ _ valid_e) as valid_e_single.
         destruct valid_e_single
           as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]].
         destr_factorize.
@@ -170,10 +218,10 @@ Proof.
           split; try auto.
           hnf; intros; subst; set_tac.
         + destruct iv_e; auto.
-        + rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H18) in *; try auto.
+        + rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H19) in *; try auto.
           apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2)
                      (updDefVars n m Gamma) v vR m0 A tMap fVars
-                     (NatSet.add n dVars) (outVars)); eauto.
+                     (NatSet.add n dVars) (outVars) fBits); eauto.
           * eapply approxUpdBound; eauto.
             simpl in *.
             apply Rle_trans with (r2:= Q2R err_e); try lra.
diff --git a/coq/IEEE_connection.v b/coq/IEEE_connection.v
index 0034115931532afa5b87b444aa9835d09f259af5..9656de11e6d6b8e09462d250051192d6be55d7b3 100644
--- a/coq/IEEE_connection.v
+++ b/coq/IEEE_connection.v
@@ -235,17 +235,12 @@ Proof.
     destruct validVal; unfold Normal in *; unfold Denormal in *;
       unfold maxValue, minValue_pos, maxExponent, minExponentPos in*;
       rewrite Q2R_inv in *; unfold bpowQ in *.
-  - assert (Z.pow_pos radix2 1024 = 179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216%Z)
-      by (vm_compute;auto).
-    rewrite H0 in H; destruct H; try lra.
-    assert (Z.pow_pos 2 1023 = 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608%Z)
-      by (vm_compute; auto).
-    rewrite H2 in *.
-    clear H0 H2.
-    rewrite Rabs_right in H1.
-    apply Rle_Qle in H1.
-    + rewrite <- Qle_bool_iff in H1.
-      cbv in H1; try congruence.
+  - cbn in *.
+    destruct H; try lra.
+    rewrite Rabs_right in H0.
+    apply Rle_Qle in H0.
+    + rewrite <- Qle_bool_iff in H0.
+      cbv in H0; try congruence.
     + rewrite <- Q2R0_is_0.
       apply Rle_ge. apply Qle_Rle; rewrite <- Qle_bool_iff; cbv; auto.
   - vm_compute; intros; congruence.
@@ -283,52 +278,62 @@ Proof.
   - vm_compute; congruence.
 Qed.
 
-Lemma typing_expr_64_bit e:
+Lemma typing_expr_64_bit e fBits:
   forall Gamma tMap,
     noDowncast e ->
     is64BitEval e ->
-    typeCheck e Gamma tMap = true ->
+    typeCheck e Gamma tMap fBits = true ->
     (forall v,
         NatSet.In v (usedVars e) -> Gamma v = Some M64) ->
     FloverMap.find e tMap = Some M64.
 Proof.
   induction e; intros * noDowncast_e is64BitEval_e typecheck_e types_valid;
     cbn in *; try inversion noDowncast_e;
-      subst; Flover_compute; try congruence;
-        type_conv; subst.
-  - rewrite types_valid in *; try set_tac.
-  - destruct m; try congruence.
-  - erewrite IHe in *; eauto.
+      subst.
+  - Flover_compute; try congruence; type_conv; subst.
+    rewrite types_valid in *; try set_tac.
+  - Flover_compute; try congruence; type_conv; subst.
+    destruct m; try congruence.
+  - Flover_compute; try congruence; type_conv; subst.
+    erewrite IHe in *; eauto.
   - repeat (match goal with
             |H: _ /\ _ |- _=> destruct H
             end).
-      erewrite IHe1 in *; eauto.
-    + erewrite IHe2 in *; eauto.
-      * unfold join in *.
-        destr_factorize.
-        rewrite <- isMorePrecise_morePrecise.
-        rewrite isMorePrecise_refl. inversion Heqo0; auto.
+      erewrite IHe1 with (Gamma:=Gamma) in *; eauto.
+    + erewrite IHe2 with (Gamma:=Gamma) in *; eauto.
+      * simpl in *.
+        Flover_compute; try congruence.
+        type_conv; subst; auto.
+      * Flover_compute; auto.
       * intros.
         apply types_valid. set_tac.
+    + Flover_compute; auto.
     + intros; apply types_valid; set_tac.
   - repeat (match goal with
             |H: _ /\ _ |- _=> destruct H
             end).
-    erewrite IHe1 in *; eauto; try (intros; apply types_valid; set_tac; fail).
-    erewrite IHe2 in *; eauto; try (intros; apply types_valid; set_tac; fail).
+    erewrite IHe1 with (Gamma:=Gamma) in *;
+      eauto;
+      [ | Flover_compute; try congruence; auto
+        | intros; apply types_valid; set_tac].
+    erewrite IHe2 with (Gamma:=Gamma) in *;
+      eauto;
+      [ | Flover_compute; try congruence; auto
+        | intros; apply types_valid; set_tac].
+    erewrite IHe3 with (Gamma:=Gamma) in *;
+      eauto;
+      [ | Flover_compute; try congruence; auto
+        | intros; apply types_valid; set_tac].
     unfold join3, join in *.
-    erewrite IHe3 in *; eauto; try (intros; apply types_valid; set_tac; fail).
-    repeat destr_factorize.
-    repeat rewrite <- isMorePrecise_morePrecise.
-    repeat rewrite isMorePrecise_refl;
-      type_conv; subst; auto.
+    simpl in *.
+    Flover_compute; try congruence; type_conv; auto.
 Qed.
 
 Lemma typing_cmd_64_bit f:
-  forall Gamma tMap,
+  forall Gamma tMap fBits,
     noDowncastFun f ->
     is64BitBstep f ->
-    typeCheckCmd f Gamma tMap = true ->
+    typeCheckCmd f Gamma tMap fBits = true ->
     (forall v,
         NatSet.In v (freeVars f) -> Gamma v = Some M64) ->
     FloverMap.find (getRetExp f) tMap = Some M64.
@@ -350,40 +355,27 @@ Proof.
 Qed.
 
 Lemma typing_agrees_expr e:
-  forall E Gamma tMap v m1 m2,
-    typeCheck e Gamma tMap = true ->
-    eval_expr E Gamma (toRExp e) v m1 ->
+  forall E Gamma tMap v m1 m2 fBits,
+    typeCheck e Gamma tMap fBits = true ->
+    eval_expr E Gamma (toRBMap fBits) (toRExp e) v m1 ->
     FloverMap.find e tMap = Some m2 ->
     m1 = m2.
 Proof.
-  induction e; intros * typeCheck_e eval_e tMap_e; cbn in *;
-    rewrite tMap_e in *;
-    inversion eval_e; subst; cbn in *;
-      Flover_compute; try congruence; type_conv; subst; try auto.
-  - eapply IHe; eauto.
-  - eapply IHe; eauto.
-  - assert (m0 = m) by eauto using IHe1.
-    assert (m3 = m1) by eauto using IHe2.
-    subst; auto.
-  - assert (m0 = m) by eauto using IHe1.
-    assert (m3 = m1) by eauto using IHe2.
-    assert (m4 = m5) by eauto using IHe3.
-    subst; auto.
+  intros.
+  pose proof (typingSoundnessExp _ _ H H0).
+  congruence.
 Qed.
 
 Lemma typing_agrees_cmd f:
-  forall E Gamma tMap v m1 m2,
-    typeCheckCmd f Gamma tMap = true ->
-    bstep (toRCmd f) E Gamma v m1 ->
+  forall E Gamma tMap v m1 m2 fBits,
+    typeCheckCmd f Gamma tMap fBits = true ->
+    bstep (toRCmd f) E Gamma (toRBMap fBits) v m1 ->
     FloverMap.find (getRetExp f) tMap = Some m2 ->
     m1 = m2.
 Proof.
-  induction f; intros * typeCheck_f eval_f tMap_f; cbn in *;
-    Flover_compute; try congruence; type_conv; subst.
-  - inversion eval_f; subst; simpl in *.
-    specialize (IHf (updEnv n v0 E) (updDefVars n m3 Gamma) tMap v m1 m2).
-    apply IHf; auto.
-  - inversion eval_f; subst; eapply typing_agrees_expr; eauto.
+  intros.
+  pose proof (typingSoundnessCmd _ _ H H0).
+  congruence.
 Qed.
 
 Lemma round_0_zero:
@@ -439,13 +431,16 @@ Proof.
                                  (evalBinop b (B2R 53 1024 v_e1) (B2R 53 1024 v_e2))%R).
     destruct (rel_error_exists) as [eps [bounded_eps round_eq]].
     + eapply Rle_trans; eauto.
-      unfold minValue_pos, Z.pow_pos; simpl.
+      unfold minValue_pos.
       rewrite Q2R_inv.
       * apply Rinv_le.
         { rewrite <- Q2R0_is_0. apply Qlt_Rlt.
           apply Qlt_alt. vm_compute; auto. }
         { unfold Q2R.
-          unfold Qnum, Qden. lra. }
+          unfold Qnum, Qden. unfold minExponentPos.
+          rewrite Z2R_IZR.
+          rewrite Rinv_1. rewrite Rmult_1_r.
+          apply IZR_le; vm_compute; congruence. }
       *  vm_compute; congruence.
     + simpl in *.
       rewrite round_eq.
@@ -474,14 +469,14 @@ Qed.
 (* (relative_error_N_ex radix2 (Fcore_FLT.FLT_exp (3 -1024 - 53) 53) *)
 (*                                     (-1022)%Z 53%Z) *)
 Lemma eval_expr_gives_IEEE (e:expr fl64) :
-  forall E1 E2 E2_real Gamma tMap vR A fVars dVars,
+  forall E1 E2 E2_real Gamma tMap vR A fVars dVars fBits,
     (forall x, (toREnv E2) x = E2_real x) ->
-    typeCheck (B2Qexpr e) Gamma tMap = true ->
+    typeCheck (B2Qexpr e) Gamma tMap fBits = true ->
     approxEnv E1 Gamma A fVars dVars E2_real ->
-    validRanges (B2Qexpr e) A E1 Gamma ->
+    validRanges (B2Qexpr e) A E1 Gamma (toRBMap fBits) ->
     validErrorbound (B2Qexpr e) tMap A dVars = true ->
     FPRangeValidator (B2Qexpr e) A tMap dVars = true ->
-    eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) vR M64 ->
+    eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) vR M64 ->
     NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
     is64BitEval (B2Qexpr e) ->
     noDowncast (B2Qexpr e) ->
@@ -495,18 +490,20 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
       (forall v, NatSet.In v (usedVars (B2Qexpr e)) -> Gamma v = Some M64) ->
       exists v,
         eval_expr_float e E2 = Some v /\
-        eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
+        eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) (Q2R (B2Q v)) M64.
 Proof.
-   induction e; simpl in *;
+  Opaque typeCheck.
+  induction e; simpl in *;
     intros * envs_eq typecheck_e approxEnv_E1_E2_real valid_rangebounds
                      valid_roundoffs valid_float_ranges eval_e_float
                      usedVars_sound is64BitEval_e noDowncast_e eval_IEEE_valid_e
                      vars_typed dVars_sound usedVars_64bit;
-    (match_pat (eval_expr _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
+    (match_pat (eval_expr _ _ _ _ _ _) (fun H => inversion H; subst; simpl in *));
      revert eval_IEEE_valid_e;
      Flover_compute_asm; try congruence; type_conv; subst;
      unfold optionBind;
      intros eval_IEEE_valid_e.
+     Transparent typeCheck.
      - unfold toREnv in *.
        destruct (E2 n) eqn:HE2; try congruence.
        exists f; split; try eauto.
@@ -517,10 +514,12 @@ Proof.
        + unfold perturb. lra.
      - destruct valid_rangebounds as [valid_e valid_intv].
        edestruct IHe as [v_e [eval_float_e eval_rel_e]]; eauto.
+       { cbn in typecheck_e; Flover_compute; auto. }
        assert (is_finite 53 1024 v_e = true).
        { apply validValue_is_finite.
-         eapply FPRangeValidator_sound; eauto.
-         eapply eval_eq_env; eauto. }
+         eapply FPRangeValidator_sound with (e:=B2Qexpr e); eauto.
+         - eapply eval_eq_env; eauto.
+         - cbn in typecheck_e; Flover_compute; auto. }
        rewrite eval_float_e.
        exists (b64_opp v_e); split; try auto.
        unfold b64_opp. rewrite <- (is_finite_Bopp _ _ pair) in H.
@@ -534,56 +533,64 @@ Proof.
                FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
                FloverMap.find (Binop b (B2Qexpr e1) (B2Qexpr e2)) tMap = Some M64)
          as [tMap_e1 [tMap_e2 tMap_b]].
-       { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
+       { repeat split; apply (typing_expr_64_bit _ fBits Gamma); simpl; auto.
+         - cbn in typecheck_e; Flover_compute; auto.
          - intros; apply usedVars_64bit; set_tac.
-         - intros; apply usedVars_64bit; set_tac.
-         -  rewrite Heqo, Heqo3, Heqo5.
-            apply Is_true_eq_true; apply andb_prop_intro; split.
-            + apply andb_prop_intro; split; apply Is_true_eq_left; auto.
-              apply mTypeEq_refl.
-            + apply Is_true_eq_left; auto. }
+         - cbn in typecheck_e; Flover_compute; auto.
+         - intros; apply usedVars_64bit; set_tac. }
        repeat destr_factorize.
        assert (m1 = M64).
-       { eapply (typing_agrees_expr (B2Qexpr e1)); eauto. }
+       { apply (typing_agrees_expr (v:=v1) (B2Qexpr e1) (E:=toREnv E2)
+                                   (Gamma:=Gamma) tMap (fBits:=fBits));
+           try auto.
+         cbn in typecheck_e; Flover_compute; auto. }
        assert (m2 = M64).
-       { eapply typing_agrees_expr; eauto. }
+       { apply (typing_agrees_expr (v:=v2) (B2Qexpr e2) (E:=toREnv E2)
+                                   (Gamma:=Gamma) tMap (fBits:=fBits));
+           try auto.
+         cbn in typecheck_e; Flover_compute; auto. }
        subst.
-       destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars)
+       destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars fBits)
          as [v_e1 [eval_float_e1 eval_rel_e1]];
          try auto; try set_tac;
-           [ intros; apply usedVars_64bit ; set_tac | ].
-       destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars)
+           [ cbn in typecheck_e; Flover_compute; auto
+           | intros; apply usedVars_64bit ; set_tac | ].
+       destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars fBits)
          as [v_e2 [eval_float_e2 eval_rel_e2]];
          try auto; try set_tac;
-           [ intros; apply usedVars_64bit ; set_tac | ].
-       pose proof (validRanges_single _ _ _ _ H14) as valid_e.
+           [ cbn in typecheck_e; Flover_compute; auto
+           | intros; apply usedVars_64bit ; set_tac | ].
+       pose proof (validRanges_single _ _ _ _ _ H15) as valid_e.
        destruct valid_e as [iv_2 [err_2 [nR2 [map_e2 [eval_real_e2 e2_bounded_real]]]]].
        rewrite eval_float_e1, eval_float_e2.
        inversion Heqo1; subst.
        destr_factorize.
        destruct iv_2 as [ivlo_2 ivhi_2].
        assert (forall vF2 m2,
-               eval_expr E2_real Gamma (toRExp (B2Qexpr e2)) vF2 m2 ->
+               eval_expr E2_real Gamma (toRBMap fBits) (toRExp (B2Qexpr e2)) vF2 m2 ->
                (Rabs (nR2 - vF2) <= Q2R err_2))%R.
-    { eapply validErrorbound_sound; try eauto; set_tac. }
+       { eapply validErrorbound_sound; try eauto; set_tac.
+         cbn in typecheck_e; Flover_compute; auto. }
     assert (contained (Q2R (B2Q v_e2))
                       (widenInterval
                          (Q2R ivlo_2, Q2R ivhi_2) (Q2R err_2))).
     { eapply distance_gives_iv.
       - simpl. eapply e2_bounded_real.
-      - eapply H15. instantiate(1:=M64).
+      - eapply H16. instantiate(1:=M64).
         eapply eval_eq_env; eauto. }
     assert (b = Div -> (Q2R (B2Q v_e2)) <> 0%R).
     { intros; subst; simpl in *.
       andb_to_prop R3.
       apply le_neq_bool_to_lt_prop in L3.
+      rewrite Heqo2 in *.
+      destruct i1; symmetry in map_e2; inversion map_e2; subst.
       destruct L3; hnf; intros.
       - rewrite H19 in *.
         apply Qlt_Rlt in H18.
-        rewrite Q2R0_is_0, Q2R_plus in H18. lra.
+        rewrite Q2R0_is_0, Q2R_plus in H18. simpl in *; lra.
       - rewrite H19 in *.
         apply Qlt_Rlt in H18.
-        rewrite Q2R0_is_0, Q2R_minus in H18; lra. }
+        rewrite Q2R0_is_0, Q2R_minus in H18; simpl in *; lra. }
     assert (validFloatValue
               (evalBinop b (Q2R (B2Q v_e1)) (Q2R (B2Q v_e2))) M64).
     { eapply (FPRangeValidator_sound (Binop b (B2Qexpr e1) (B2Qexpr e2)));
@@ -592,29 +599,29 @@ Proof.
         eapply Binop_dist' with (delta:=0%R); eauto.
         + rewrite Rabs_R0. apply mTypeToR_pos_R.
         + unfold perturb; lra.
-      - Flover_compute.
-        apply Is_true_eq_true.
-        repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
       - repeat split; try auto.
         + intros ? iv2 err2 find. subst.
           destruct iv2; rewrite find in *;
-            eapply H11; eauto.
+            eapply H12; eauto.
         + rewrite Heqo0. auto.
       - Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro); split; try auto using Is_true_eq_left.
-        apply andb_prop_intro; split; try auto using Is_true_eq_left.
-        apply Is_true_eq_left.
+        rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
+        apply andb_prop_intro; split; apply Is_true_eq_left; try auto.
         rewrite L4, R1. auto.
       - Flover_compute.
         apply Is_true_eq_true.
         repeat (apply andb_prop_intro; split); try auto using Is_true_eq_left. }
+    rewrite Heqo2 in map_e2; destruct i0; inversion map_e2; subst.
     assert (validFloatValue (Q2R (B2Q v_e1)) M64).
     { eapply (FPRangeValidator_sound (B2Qexpr e1)); try eauto; try set_tac.
-      eapply eval_eq_env; eauto. }
+      eapply eval_eq_env; eauto.
+      cbn in typecheck_e; Flover_compute_asm; auto. }
     assert (validFloatValue (Q2R (B2Q v_e2)) M64).
     { eapply (FPRangeValidator_sound (B2Qexpr e2)); try eauto; try set_tac.
-      - eapply eval_eq_env; eauto. }
+      - eapply eval_eq_env; eauto.
+      - cbn in typecheck_e; Flover_compute_asm; auto. }
     assert (is_finite 53 1024 v_e1 = true) as finite_e1.
     { apply validValue_is_finite; simpl; auto. }
     assert (is_finite 53 1024 v_e2 = true) as finite_e2.
@@ -631,13 +638,10 @@ Proof.
           eapply Rle_trans; eauto.
           simpl. lra.
         + unfold perturb. repeat rewrite B2Q_B2R_eq; try auto.
-      - cbn. Flover_compute.
-        apply Is_true_eq_true.
-        repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
       - cbn; repeat split; try auto.
         + intros ? iv2 err2 find. subst.
           destruct iv2; rewrite find in *;
-            eapply H11; eauto.
+            eapply H12; eauto.
         + rewrite Heqo0. auto.
       - cbn. Flover_compute.
         apply Is_true_eq_true.
@@ -658,7 +662,7 @@ Proof.
         apply Qlt_Rlt in case_high.
         rewrite Q2R0_is_0, Q2R_minus in case_high; lra. }
     clear H2 H12 dVars_sound usedVars_64bit vars_typed usedVars_sound R2 R1 L1 L
-    L0 R3 R4 L2 R5 Heqo Heqo0 Heqo1 IHe1
+    L0 R3 L2 Heqo Heqo0 Heqo1 IHe1
     IHe2.
     pose proof (fexp_correct 53 1024 eq_refl) as fexpr_corr.
     assert (forall k : Z, (-1022 < k)%Z ->
@@ -856,24 +860,20 @@ Proof.
   - repeat (match goal with
             |H: _ /\ _ |- _ => destruct H
             end).
+    assert (typeCheck (B2Qexpr e1) Gamma tMap fBits = true /\
+            typeCheck (B2Qexpr e2) Gamma tMap fBits = true /\
+            typeCheck (B2Qexpr e3) Gamma tMap fBits = true)
+           as [typecheck_e1 [typecheck_e2 typecheck_e3]].
+    { repeat split; cbn in typecheck_e; Flover_compute; auto. }
     assert (FloverMap.find (B2Qexpr e1) tMap = Some M64 /\
             FloverMap.find (B2Qexpr e2) tMap = Some M64 /\
             FloverMap.find (B2Qexpr e3) tMap = Some M64 /\
             FloverMap.find (Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)) tMap = Some M64)
-           as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
-    { repeat split; apply (typing_expr_64_bit _ Gamma); simpl; auto.
-      - intros; apply usedVars_64bit; set_tac.
+      as [tMap_e1 [tMap_e2 [tMap_e3 tMap_fma]]].
+    { repeat split; try apply (typing_expr_64_bit _ fBits Gamma); simpl; auto.
       - intros; apply usedVars_64bit; set_tac.
       - intros; apply usedVars_64bit; set_tac.
-      - rewrite Heqo, Heqo3, Heqo5, Heqo7.
-        apply Is_true_eq_true; apply andb_prop_intro; split.
-        + apply andb_prop_intro; split.
-          * apply andb_prop_intro; split.
-            ++ apply Is_true_eq_left; auto.
-               apply mTypeEq_refl.
-            ++ apply Is_true_eq_left; auto.
-          * apply Is_true_eq_left; auto.
-        + apply Is_true_eq_left; auto. }
+      - intros; apply usedVars_64bit; set_tac. }
     repeat destr_factorize.
     inversion Heqo; inversion Heqo0; inversion Heqo1; inversion Heqo2; subst.
     assert (m1 = M64).
@@ -883,35 +883,34 @@ Proof.
     assert (m3 = M64).
     { eapply (typing_agrees_expr (B2Qexpr e3)); eauto. }
     subst.
-    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars)
+    destruct (IHe1 E1 E2 E2_real Gamma tMap v1 A fVars dVars fBits)
       as [v_e1 [eval_float_e1 eval_rel_e1]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars)
+    destruct (IHe2 E1 E2 E2_real Gamma tMap v2 A fVars dVars fBits)
       as [v_e2 [eval_float_e2 eval_rel_e2]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A fVars dVars)
+    destruct (IHe3 E1 E2 E2_real Gamma tMap v3 A fVars dVars fBits)
       as [v_e3 [eval_float_e3 eval_rel_e3]];
       try auto; try set_tac;
         [ intros; apply usedVars_64bit ; set_tac | ].
-    unfold optionBind in H4.
-    rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H4.
-    contradiction H4.
+    rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H6.
+    contradiction H6.
   - inversion noDowncast_e.
 Qed.
 
 Lemma bstep_gives_IEEE (f:cmd fl64) :
-  forall E1 E2 E2_real Gamma tMap vR vF A fVars dVars outVars,
+  forall E1 E2 E2_real Gamma tMap vR vF A fVars dVars outVars fBits,
     (forall x, (toREnv E2) x = E2_real x) ->
     approxEnv E1 Gamma A fVars dVars E2_real ->
     ssa (B2Qcmd f) (NatSet.union fVars dVars) outVars ->
-    typeCheckCmd (B2Qcmd f) Gamma tMap = true ->
-    validRangesCmd (B2Qcmd f) A E1 Gamma ->
+    typeCheckCmd (B2Qcmd f) Gamma tMap fBits = true ->
+    validRangesCmd (B2Qcmd f) A E1 Gamma (toRBMap fBits) ->
     validErrorboundCmd (B2Qcmd f) tMap A dVars = true ->
     FPRangeValidatorCmd (B2Qcmd f) A tMap dVars = true ->
-    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) vR REAL ->
-    bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma vF M64 ->
+    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap Gamma) (toRBMap fBits) vR REAL ->
+    bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (toRBMap fBits) vF M64 ->
     NatSet.Subset (NatSet.diff (freeVars (B2Qcmd f)) dVars) fVars ->
     is64BitBstep (B2Qcmd f) ->
     noDowncastFun (B2Qcmd f) ->
@@ -925,7 +924,7 @@ Lemma bstep_gives_IEEE (f:cmd fl64) :
       (forall v, NatSet.In v (freeVars (B2Qcmd f)) -> Gamma v = Some M64) ->
       exists v,
         bstep_float f E2 = Some v /\
-        bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (Q2R (B2Q v)) M64.
+        bstep (toRCmd (B2Qcmd f)) (toREnv E2) Gamma (toRBMap fBits) (Q2R (B2Q v)) M64.
 Proof.
   induction f;
     intros * envs_eq approxEnv_E1_E2_real ssa_f typeCheck_f valid_ranges_f
@@ -950,20 +949,20 @@ Proof.
       set_tac.
       split; [ set_tac | ].
       hnf; intros; subst.
-      apply H26.
-      apply (H25 n H).  }
+      apply H28.
+      apply (H27 n H). }
     assert (m1 = M64).
     { eapply typing_agrees_expr; eauto. }
     subst.
     assert (exists v_e, eval_expr_float e E2 = Some v_e /\
-                   eval_expr (toREnv E2) Gamma (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
+                   eval_expr (toREnv E2) Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) (Q2R (B2Q v_e)) M64)
            as eval_float_e.
     { eapply eval_expr_gives_IEEE; try eauto.
       - destruct valid_ranges_f as [[? ?] ?]; auto.
       - hnf; intros. rewrite NatSet.diff_spec in H0.
         destruct H0.
-        specialize (H25 a H0). rewrite NatSet.union_spec in H25.
-        destruct H25; try congruence; auto.
+        specialize (H27 a H0). rewrite NatSet.union_spec in H27.
+        destruct H27; try congruence; auto.
       - destruct is64_eval; auto.
       - destruct nodowncast_f; auto.
       - destruct bstep_sound; auto.
@@ -971,16 +970,16 @@ Proof.
         rewrite NatSet.remove_spec, NatSet.union_spec.
         split; try auto.
         hnf; intros; subst.
-        specialize (H25 n H0).
-        set_tac.  apply H26; set_tac. }
+        specialize (H27 n H0).
+        set_tac. apply H28; set_tac. }
     destruct eval_float_e as [v_e [eval_float_e eval_rel_e]].
-    assert (forall v m, eval_expr E2_real Gamma (toRExp (B2Qexpr e)) v m ->
+    assert (forall v m, eval_expr E2_real Gamma (toRBMap fBits) (toRExp (B2Qexpr e)) v m ->
                    Rabs (v0 - v) <= Q2R e0)%R
       as err_e_valid.
     { eapply validErrorbound_sound; try eauto.
       - hnf; intros. rewrite NatSet.diff_spec in H0.
-        destruct H0. specialize (H25 a H0). rewrite NatSet.union_spec in H25.
-        destruct H25; try auto; congruence.
+        destruct H0. specialize (H27 a H0). rewrite NatSet.union_spec in H27.
+        destruct H27; try auto; congruence.
       - destruct valid_ranges_f as [[? ?] ?]; auto.
       - instantiate (1:= snd i). instantiate (1:=fst i).
         destruct i; simpl in *; auto. }
@@ -990,7 +989,10 @@ Proof.
        using lemma validErrorboundCmd_gives_eval *)
     destruct valid_ranges_f as [[valid_e valid_cont] valid_single].
     destruct valid_single as [iv_ret [err_ret [v_ret [map_ret [eval_ret bound_ret]]]]].
-    assert (exists vF m, bstep (toRCmd (B2Qcmd f)) (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) vF m).
+    assert (exists vF m,
+               bstep (toRCmd (B2Qcmd f))
+                     (updEnv n (Q2R (B2Q v_e)) E2_real)
+                     (updDefVars n M64 Gamma) (toRBMap fBits) vF m).
     { eapply validErrorboundCmd_gives_eval with (E1 := updEnv n v0 E1)
                                                   (elo:=fst(iv_ret))
                                                   (ehi:=snd(iv_ret))
@@ -1041,7 +1043,7 @@ Proof.
     subst.
     destruct (IHf (updEnv n v0 E1) (updFlEnv n v_e E2)
                   (updEnv n (Q2R (B2Q v_e)) E2_real) (updDefVars n M64 Gamma) tMap
-                  vR vF_new A fVars (NatSet.add n dVars) outVars); try eauto.
+                  vR vF_new A fVars (NatSet.add n dVars) outVars fBits); try eauto.
     + intros. unfold toREnv, updFlEnv, updEnv.
       destruct (x =? n); auto. rewrite <- envs_eq. unfold toREnv; auto.
     + eapply approxUpdBound; eauto.
@@ -1124,7 +1126,7 @@ Proof.
     apply ret_b; auto.
 Qed.
 
-Theorem IEEE_connection_expr e A P E1 E2 defVars:
+Theorem IEEE_connection_expr e A P E1 E2 defVars fBits:
   approxEnv E1 defVars A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
   is64BitEval (B2Qexpr e) ->
   noDowncast (B2Qexpr e) ->
@@ -1140,12 +1142,12 @@ Theorem IEEE_connection_expr e A P E1 E2 defVars:
   (forall v,
       NatSet.In v (usedVars (B2Qexpr e)) ->
       exists m, defVars v = Some m) ->
-  CertificateChecker (B2Qexpr e) A P defVars = true ->
+  CertificateChecker (B2Qexpr e) A P defVars fBits = true ->
   exists iv err vR vF, (* m, currently = M64 *)
     FloverMap.find (B2Qexpr e) A = Some (iv, err) /\
-    eval_expr E1 (toRMap defVars) (toREval (toRExp (B2Qexpr e))) vR REAL /\
+    eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp (B2Qexpr e))) vR REAL /\
     eval_expr_float e E2 = Some vF /\
-    eval_expr (toREnv E2) defVars (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
+    eval_expr (toREnv E2) defVars (toRBMap fBits) (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
     (Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
 Proof.
   intros.
@@ -1153,7 +1155,9 @@ Proof.
   destruct H7 as [err [vR [vF [mF [map_e [eval_real [eval_float roundoff_sound]]]]]]].
   unfold CertificateChecker in H6.
   andb_to_prop H6.
-  assert (FloverMap.find (B2Qexpr e) (typeMap defVars (B2Qexpr e) (FloverMap.empty mType))  = Some M64).
+  assert (FloverMap.find (B2Qexpr e)
+                         (typeMap defVars (B2Qexpr e) (FloverMap.empty mType) fBits)
+          = Some M64).
     { eapply typing_expr_64_bit; eauto. }
     assert (mF = M64).
     { eapply typing_agrees_expr; eauto. }
@@ -1174,7 +1178,7 @@ Proof.
 Qed.
 
 Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
-        defVars E1 E2:
+        defVars E1 E2 fBits:
     approxEnv E1 defVars A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
     is64BitBstep (B2Qcmd f) ->
     noDowncastFun (B2Qcmd f) ->
@@ -1187,14 +1191,14 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
     (forall v, (v) mem (freeVars (B2Qcmd f)) = true ->
           exists m : mType,
             defVars v = Some m) ->
-    CertificateCheckerCmd (B2Qcmd f) A P defVars = true ->
+    CertificateCheckerCmd (B2Qcmd f) A P defVars fBits = true ->
     exists iv err vR vF m,
       FloverMap.find (getRetExp (B2Qcmd f)) A = Some (iv,err) /\
-    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) vR REAL /\
+    bstep (toREvalCmd (toRCmd (B2Qcmd f))) E1 (toRMap defVars) (toRBMap fBits) vR REAL /\
     bstep_float f E2 = Some vF /\
-    bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (Q2R (B2Q vF)) m /\
+    bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (toRBMap fBits) (Q2R (B2Q vF)) m /\
     (forall vF m,
-        bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars vF m ->
+        bstep (toRCmd (B2Qcmd f)) (toREnv E2) defVars (toRBMap fBits) vF m ->
         (Rabs (vR - vF) <= Q2R err)%R).
 Proof.
   intros.
@@ -1202,14 +1206,17 @@ Proof.
   andb_to_prop H6.
   pose proof (validSSA_sound _ _ R0).
   destruct H6 as [outVars ssa_f].
-  edestruct Certificate_checking_cmds_is_sound; eauto.
+  edestruct Certificate_checking_cmds_is_sound with (fBits:=fBits); eauto.
   - intros.
     apply H4. set_tac.
   - unfold CertificateCheckerCmd.
     apply Is_true_eq_true.
     repeat (apply andb_prop_intro; split; try auto using Is_true_eq_left).
   - destruct H6 as [err [vR [vF [m [map_ret [bstep_real [bstep_float roundoff_sound]]]]]]].
-    assert (FloverMap.find (getRetExp (B2Qcmd f)) (typeMapCmd defVars (B2Qcmd f) (FloverMap.empty mType)) = Some M64).
+    assert (FloverMap.find
+              (getRetExp (B2Qcmd f))
+              (typeMapCmd defVars (B2Qcmd f) (FloverMap.empty mType) fBits)
+            = Some M64).
     { eapply typing_cmd_64_bit; eauto.  }
     assert (m = M64).
     { eapply typing_agrees_cmd; eauto. }
diff --git a/coq/Infra/ExpressionAbbrevs.v b/coq/Infra/ExpressionAbbrevs.v
index b4559156e5f11c3b81371f0827cb5e1310dbe453..b46de69168495be5488fa98aaf9edb8499d95599 100644
--- a/coq/Infra/ExpressionAbbrevs.v
+++ b/coq/Infra/ExpressionAbbrevs.v
@@ -2,14 +2,14 @@
   Some abbreviations that require having defined exprressions beforehand
   If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
 **)
-Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts Recdef.
-Require Import Flover.AffineForm.
-Require Export Flover.Infra.Abbrevs Flover.Expressions Flover.OrderedExpressions.
-
+Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts Coq.Reals.ROrderedType Recdef.
+Require Export Flover.Infra.Abbrevs Flover.AffineForm Flover.Expressions Flover.Infra.Ltacs Flover.OrderedExpressions.
 
 Module Q_orderedExps := ExprOrderedType (Q_as_OT).
 Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).
 
+Module R_orderedExps := ExprOrderedType (R_as_OT).
+
 Functional Scheme exprCompare_ind := Induction for Q_orderedExps.exprCompare Sort Prop.
 
 Lemma expr_compare_eq_eval_compat (e1 e2: expr Q):
@@ -21,30 +21,74 @@ Proof.
       try now apply Nat.compare_eq.
   - rewrite <- Qeq_alt in Heq.
     now apply Qeq_eqR.
+  - apply Ndec.Pcompare_Peqb in e6.
+    apply Pos.eqb_eq in e6; subst.
+    apply Nat.compare_eq in Heq; subst; auto.
   - simpl in e3.
     apply andb_false_iff in e3.
     apply Ndec.Pcompare_Peqb in e6.
-    apply Ndec.Pcompare_Peqb in Heq.
-    destruct e3; congruence.
-  - simpl in e3.
-    apply andb_false_iff in e3.
-    apply Ndec.Pcompare_Peqb in e6.
-    apply Ndec.Pcompare_Peqb in Heq.
+    apply Pos.eqb_eq in e6; subst.
+    apply Nat.compare_eq in Heq; subst; auto.
+    rewrite Nat.eqb_refl, Pos.eqb_refl in e3.
     destruct e3; congruence.
   - unfold unopEq in e5.
     destruct u1, u2; congruence.
   - simpl in e5.
     apply andb_false_iff in e5.
     apply Ndec.Pcompare_Peqb in e8.
-    apply Ndec.Pcompare_Peqb in Heq.
+    rewrite Pos.eqb_eq in e8; subst.
+    apply Nat.compare_eq in Heq; subst.
     destruct e5; congruence.
   - simpl in e5.
     apply andb_false_iff in e5.
     apply Ndec.Pcompare_Peqb in e8.
-    apply Ndec.Pcompare_Peqb in Heq.
+    rewrite Pos.eqb_eq in e8.
+    apply Nat.compare_eq in Heq; subst.
+    rewrite Nat.eqb_refl, Pos.eqb_refl in *.
     destruct e5; congruence.
 Qed.
 
+Lemma Qcompare_Rcompare q1 q2 c:
+  Qcompare q1 q2 = c ->
+  Rcompare (Q2R q1) (Q2R q2) = c.
+Proof.
+  intros q_check; destruct c.
+  - rewrite <- Qeq_alt in q_check.
+    apply Qeq_eqR in q_check.
+    rewrite q_check in *.
+    rewrite R_orderedExps.V_orderedFacts.compare_refl in *; auto.
+  - rewrite <- Qlt_alt in q_check.
+    apply Qlt_Rlt in q_check.
+    rewrite R_orderedExps.V_orderedFacts.compare_lt_iff; auto.
+  - rewrite <- Qgt_alt in q_check.
+    rewrite R_orderedExps.V_orderedFacts.compare_gt_iff.
+    auto using Qlt_Rlt.
+Qed.
+
+Lemma QcompareExp_RcompareExp e1 e2:
+  Q_orderedExps.exprCompare e1 e2 = R_orderedExps.exprCompare (toRExp e1) (toRExp e2).
+Proof.
+  functional induction (Q_orderedExps.exprCompare e1 e2); simpl in *; try auto; try congruence;
+    try rewrite e3;
+  try rewrite <- IHc, e6; try auto.
+  - destruct (Qcompare v1 v2) eqn:q_comp; apply Qcompare_Rcompare in q_comp; auto.
+  - rewrite e6; auto.
+  - rewrite e6; auto.
+  - rewrite e6; auto.
+  - rewrite e5, IHc; auto.
+  - rewrite e5, e6; auto.
+  - rewrite e5, e6; auto.
+  - rewrite <- IHc, <- IHc0, e4, e3; auto.
+  - rewrite <- IHc, e3, <- IHc0, e4; auto.
+  - rewrite <- IHc, e3, <- IHc0, e4; auto.
+  - rewrite <- IHc, e3; auto.
+  - rewrite <- IHc, e3; auto.
+  - rewrite <- IHc, e5; auto.
+  - rewrite e5, e8; auto.
+  - rewrite e5, e8; auto.
+  - rewrite e5, e8; auto.
+Qed.
+
 Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
 Module FloverMapFacts := OrdProperties (FloverMap).
 
@@ -88,6 +132,67 @@ Proof.
     auto.
 Qed.
 
+Definition toRBMap (bMap:FloverMap.t nat) : expr R -> option nat :=
+  let elements := FloverMap.elements (elt:=nat) bMap in
+  fun (e:expr R) =>
+    olet p := find (fun p => match R_orderedExps.compare  e (toRExp (fst p)) with
+                   | Eq => true |_ => false end) elements in
+        Some (snd p).
+
+Lemma findA_find A B (f:A -> bool) (l:list (A * B)) r:
+  findA f l = Some r ->
+  exists k,
+  find (fun p => f (fst p)) l = Some (k,r) /\ f k = true.
+Proof.
+  induction l.
+  - intros; simpl in *; congruence.
+  - intros findA_top.
+    simpl in *.
+    destruct a; simpl in *.
+    destruct (f a) eqn:?; try auto.
+    exists a; split; congruence.
+Qed.
+
+Lemma find_swap A (f1:A -> bool) f2 l r:
+  (forall k, f1 k = f2 k) ->
+  find f1 l = Some r ->
+  find f2 l = Some r.
+Proof.
+  induction l; intros f_eq find1; simpl in *; try congruence.
+  destruct (f1 a) eqn:?.
+  - rewrite <- f_eq; rewrite Heqb; congruence.
+  - rewrite <- f_eq; rewrite Heqb.
+    apply IHl; auto.
+Qed.
+
+Lemma toRBMap_some bMap e b:
+  FloverMap.find e bMap = Some b ->
+  toRBMap bMap (toRExp e) = Some b.
+Proof.
+  intros find_Q.
+  rewrite  FloverMapFacts.P.F.elements_o in find_Q.
+  unfold toRBMap.
+  unfold optionBind.
+  apply findA_find in find_Q as [key [find_Q k_eq]].
+  unfold FloverMapFacts.P.F.eqb in k_eq.
+  cut (find
+      (fun p : expr Q * nat =>
+       match R_orderedExps.compare (toRExp e) (toRExp (fst p)) with
+       | Eq => true
+       | _ => false
+       end) (FloverMap.elements (elt:=nat) bMap) = Some (key, b)).
+  - intros find_R. rewrite find_R. auto.
+  - eapply find_swap with (f1 := fun p => match Q_orderedExps.exprCompare e (fst p) with
+                                       |Eq => true |_ => false end).
+    + intros. rewrite <- QcompareExp_RcompareExp; auto.
+    + eapply find_swap; eauto.
+      intros; simpl.
+      destruct (Q_orderedExps.exprCompare e (fst k)) eqn:q_comp.
+      all: unfold FloverMapFacts.P.F.eqb.
+      all: unfold FloverMapFacts.P.F.eq_dec.
+      all: rewrite q_comp; auto.
+Qed.
+
 (**
 We treat a function mapping an exprression arguing on fractions as value type
 to pairs of intervals on rationals and rational errors as the analysis result
diff --git a/coq/Infra/MachineType.v b/coq/Infra/MachineType.v
index b46c965d64ccd2f00e08afcd354470102ea99498..d07c4e9b930674bad2f48b07e86cb406690feb95 100644
--- a/coq/Infra/MachineType.v
+++ b/coq/Infra/MachineType.v
@@ -351,6 +351,30 @@ Definition join3 (m1:mType) (m2:mType) (m3:mType) (fBits:nat):=
   olet msub := (join m2 m3 fBits) in
     join m1 msub fBits.
 
+Lemma join_float m1 m2 f1 f2:
+  ~ isFixedPoint m1 ->
+  ~ isFixedPoint m2 ->
+  join m1 m2 f1 = join m1 m2 f2.
+Proof.
+  intros. destruct m1, m2; simpl in *; try congruence.
+  exfalso. auto.
+Qed.
+
+Corollary join3_float m1 m2 m3 f1 f2:
+  ~ isFixedPoint m1 ->
+  ~ isFixedPoint m2 ->
+  ~ isFixedPoint m3 ->
+  join3 m1 m2 m3 f1 = join3 m1 m2 m3 f2.
+Proof.
+  intros.
+  unfold join3.
+  erewrite join_float with (f2:=f2); eauto.
+  destruct (join m2 m3 f2) eqn:?; try auto.
+  simpl. apply join_float; auto.
+  destruct m2, m3; simpl in *; inversion Heqo; subst; hnf; simpl; try congruence.
+  exfalso. auto.
+Qed.
+
 (* Lemma REAL_join_is_REAL m1 m2: *)
 (*   join m1 m2 = REAL -> m1 = REAL /\ m2 = REAL. *)
 (* Proof. *)
diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v
index e7d7451636ac773c92c5a9cf61b809ba327c4773..b60f86e8f26333bc267e3114364dc4bca73e3309 100644
--- a/coq/IntervalValidation.v
+++ b/coq/IntervalValidation.v
@@ -132,17 +132,13 @@ Proof.
 Qed.
 
 Theorem validIntervalbounds_sound (f:expr Q) (A:analysisResult) (P:precond)
-        fVars dVars (E:env) Gamma:
+        fVars dVars (E:env) Gamma fBits:
     validIntervalbounds f A P dVars = true ->
     dVars_range_valid dVars E A ->
     NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
     fVars_P_sound fVars E P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
-    validRanges f A E Gamma.
-    (* exists iv err vR, *)
-    (*   FloverMap.find f A = Some (iv, err) /\ *)
-    (*   eval_expr E (toRMap Gamma) (toREval (toRExp f)) vR REAL /\ *)
-    (*   (Q2R (fst iv) <= vR <= Q2R (snd iv))%R. *)
+    validRanges f A E Gamma fBits.
 Proof.
   induction f;
     intros valid_bounds valid_definedVars usedVars_subset valid_freeVars types_defined;
@@ -182,7 +178,7 @@ Proof.
     + unfold perturb; simpl; lra.
   - Flover_compute; simpl in *; try congruence.
     unfold validRanges in IHf.
-    assert (validRanges f A E Gamma) as valid_e.
+    assert (validRanges f A E Gamma fBits) as valid_e.
     { apply IHf; auto. }
     split; try auto.
     apply validRanges_single in valid_e.
@@ -238,9 +234,9 @@ Proof.
              }
              rewrite <- Q2R0_is_0 in H3.
              apply Rlt_Qlt in H3. lra. }
-  - assert (validRanges f1 A E Gamma) as valid_f1
+  - assert (validRanges f1 A E Gamma fBits) as valid_f1
         by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
-    assert (validRanges f2 A E Gamma) as valid_f2
+    assert (validRanges f2 A E Gamma fBits) as valid_f2
         by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
     repeat split;
       [ intros; subst; Flover_compute; congruence |
@@ -250,16 +246,14 @@ Proof.
     destruct valid_f1 as [iv_f1 [err1 [vF1 [env1 [eval_f1 valid_f1]]]]].
     destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
     Flover_compute; try congruence.
-    assert (REAL = join REAL REAL) as REAL_join by (cbv; auto);
-      rewrite REAL_join.
     kill_trivial_exists.
     exists (perturb (evalBinop b vF1 vF2) REAL 0);
       split; [destruct i; auto | ].
     inversion env1; inversion env2; subst.
       destruct b; simpl in *.
     * split;
-        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
-         rewrite Rabs_R0; cbn; lra|].
+        [eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
+         try rewrite Rabs_R0; cbn; lra|].
       pose proof (interval_addition_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                           (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_add.
@@ -271,8 +265,8 @@ Proof.
         rewrite <- Q2R_min4, <- Q2R_max4 in *.
       unfold perturb. lra.
     * split;
-        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
-         rewrite Rabs_R0; cbn; lra|].
+        [eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
+         try rewrite Rabs_R0; cbn; lra|].
       pose proof (interval_subtraction_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                              (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_sub.
@@ -285,8 +279,8 @@ Proof.
         rewrite <- Q2R_min4, <- Q2R_max4 in *.
       unfold perturb; lra.
     * split;
-        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
-         rewrite Rabs_R0; cbn; lra|].
+        [eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
+         try rewrite Rabs_R0; cbn; lra|].
       pose proof (interval_multiplication_valid ((Q2R (fst iv_f1)), Q2R (snd iv_f1))
                                                 (Q2R (fst iv_f2), Q2R (snd iv_f2)))
         as valid_mul.
@@ -301,7 +295,7 @@ Proof.
       canonize_hyps.
       apply le_neq_bool_to_lt_prop in L.
       split;
-        [eapply Binop_dist' with (delta := 0%R); eauto; try congruence;
+        [eapply Binop_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence;
          try rewrite Rabs_R0; cbn; try lra|].
       (* No division by zero proof *)
       { hnf; intros.
@@ -327,11 +321,11 @@ Proof.
           unfold perturb.
           lra.
       }
-  - assert (validRanges f1 A E Gamma) as valid_f1
+  - assert (validRanges f1 A E Gamma fBits) as valid_f1
         by (Flover_compute; try congruence; apply IHf1; try auto; set_tac).
-    assert (validRanges f2 A E Gamma) as valid_f2
+    assert (validRanges f2 A E Gamma fBits) as valid_f2
         by (Flover_compute; try congruence; apply IHf2; try auto; set_tac).
-    assert (validRanges f3 A E Gamma) as valid_f3
+    assert (validRanges f3 A E Gamma fBits) as valid_f3
         by (Flover_compute; try congruence; apply IHf3; try auto; set_tac).
     repeat split; try auto.
     apply validRanges_single in valid_f1;
@@ -341,13 +335,12 @@ Proof.
     destruct valid_f2 as [iv_f2 [err2 [vF2 [env2 [eval_f2 valid_f2]]]]].
     destruct valid_f3 as [iv_f3 [err3 [vF3 [env3 [eval_f3 valid_f3]]]]].
     Flover_compute; try congruence.
-    assert (REAL = join3 REAL REAL REAL) as REAL_join by (cbv; auto);
-      rewrite REAL_join.
     kill_trivial_exists.
     exists (perturb (evalFma vF1 vF2 vF3) REAL 0); split; try auto.
     inversion env1; inversion env2; inversion env3; subst.
     split; [auto | ].
-    * eapply Fma_dist' with (delta := 0%R); eauto; try congruence; cbn; rewrite Rabs_R0; lra.
+    * eapply Fma_dist' with (delta := 0%R) (fBit:=0%nat); eauto; try congruence; cbn;
+        try rewrite Rabs_R0; lra.
     * pose proof (interval_multiplication_valid (Q2R (fst iv_f2),Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as valid_mul.
       specialize (valid_mul vF2 vF3 valid_f2 valid_f3).
       remember (multInterval (Q2R (fst iv_f2), Q2R (snd iv_f2)) (Q2R (fst iv_f3), Q2R (snd iv_f3))) as iv_f23prod.
@@ -363,7 +356,7 @@ Proof.
       specialize (valid_add vF1 (vF2 * vF3)%R valid_f1 valid_mul).
       unfold evalFma, evalBinop, perturb.
       lra.
-  - assert (validRanges f A E Gamma) as valid_f1
+  - assert (validRanges f A E Gamma fBits) as valid_f1
         by (Flover_compute; try congruence; apply IHf; auto).
     split; try auto.
     apply validRanges_single in valid_f1.
@@ -388,16 +381,15 @@ Proof.
   intros x; destruct (x =? n); try auto.
 Qed.
 
-
 Theorem validIntervalboundsCmd_sound (f:cmd Q) (A:analysisResult):
-  forall Gamma E fVars dVars outVars P,
+  forall Gamma E fVars dVars outVars P fBits,
     ssa f (NatSet.union fVars dVars) outVars ->
     dVars_range_valid dVars E A ->
     fVars_P_sound fVars E P ->
     vars_typed (NatSet.union fVars dVars) Gamma ->
     NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars ->
     validIntervalboundsCmd f A P dVars = true ->
-    validRangesCmd f A E Gamma.
+    validRangesCmd f A E Gamma fBits.
 Proof.
   induction f;
     intros *  ssa_f dVars_sound fVars_valid types_valid usedVars_subset valid_bounds_f;
@@ -405,8 +397,8 @@ Proof.
   - Flover_compute.
     inversion ssa_f; subst.
     canonize_hyps.
-    pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) L) as validIV_e.
-    assert (validRanges e A E Gamma) as valid_e.
+    pose proof (validIntervalbounds_sound e (Gamma:=Gamma) (E:=E) (fVars:=fVars) fBits L) as validIV_e.
+    assert (validRanges e A E Gamma fBits) as valid_e.
     { apply validIV_e; try auto.
       set_tac. repeat split; auto.
       hnf; intros; subst.
@@ -417,11 +409,11 @@ Proof.
         destruct H0; auto.
       - destruct in_set as [? | ?]; try auto; set_tac.
         destruct H as [? | [? ?]]; auto. }
-    pose proof (validRanges_single _ _ _ _ valid_e) as valid_single_e.
+    pose proof (validRanges_single _ _ _ _ fBits valid_e) as valid_single_e.
     destruct valid_single_e as [iv_e [err_v [v [find_v [eval_e valid_bounds_e]]]]].
     rewrite find_v in *; inversion Heqo; subst.
     specialize (IHf (updDefVars n REAL Gamma) (updEnv n v E) fVars (NatSet.add n dVars)) as IHf_spec.
-    assert (validRangesCmd f A (updEnv n v E) (updDefVars n REAL Gamma)).
+    assert (validRangesCmd f A (updEnv n v E) (updDefVars n REAL Gamma) fBits).
     { eapply IHf_spec; eauto.
       - eapply ssa_equal_set. symmetry in H. apply H. apply H7.
       - intros v0 mem_v0.
@@ -487,8 +479,8 @@ Proof.
         * lra.
         * lra.
   - unfold validIntervalboundsCmd in valid_bounds_f.
-    pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
-    assert (validRanges e A E Gamma) as valid_e by (apply valid_iv_e; auto).
+    pose proof (validIntervalbounds_sound e (E:=E) (Gamma:=Gamma) fBits valid_bounds_f dVars_sound usedVars_subset) as valid_iv_e.
+    assert (validRanges e A E Gamma fBits) as valid_e by (apply valid_iv_e; auto).
     split; try auto.
     apply validRanges_single in valid_e.
     destruct valid_e as [?[?[? [? [? ?]]]]]; try auto.
diff --git a/coq/OrderedExpressions.v b/coq/OrderedExpressions.v
index 498e835f4e1353da3bce47c1d443d9efcaf40222..1440e5dbc7beca3eb6586ea3737c9973d1f02991 100644
--- a/coq/OrderedExpressions.v
+++ b/coq/OrderedExpressions.v
@@ -26,7 +26,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         match m1, m2 with
         | F w1 f1, F w2 f2 =>
           match w1 ?= w2 with
-          |Eq => f1 ?= f2
+          |Eq => (f1 ?= f2)%nat
           | c => c
           end
         | F w f, _ => Lt
@@ -50,7 +50,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         match m1, m2 with
         | F w1 f1, F w2 f2 =>
           match w1 ?= w2 with
-          |Eq => f1 ?= f2
+          |Eq => (f1 ?= f2)%nat
           | c => c
           end
         | F w f, _ => Lt
@@ -127,16 +127,16 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         destruct m0; destruct m1; auto.
       + destruct (mTypeEq m m1) eqn:?; type_conv;
           destruct m0; destruct m1; simpl in *; try congruence.
-        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f) eqn:?;
+        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f)%nat eqn:?;
                    try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
         * destruct m; try congruence.
-          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f) eqn:?;
+          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f)%nat eqn:?;
                    try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
     - destruct (unopEq u u0) eqn:?;
                destruct (unopEq u0 u1) eqn:?;
@@ -168,23 +168,23 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
           destruct (morePrecise _ m0); try congruence;
             destruct m0,m1;
             cbn in *; try congruence.
-        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f) eqn:?; try congruence.
+        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f)%nat eqn:?; try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
-        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f) eqn:?; try congruence.
+        * destruct (w0 ?= w) eqn:?; destruct (f0 ?= f)%nat eqn:?; try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
         * destruct m; try congruence.
-          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f) eqn:?; try congruence.
+          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f)%nat eqn:?; try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
         * destruct m; try congruence.
-          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f) eqn:?; try congruence.
+          destruct (w1 ?= w) eqn:?; destruct (f1 ?= f)%nat eqn:?; try congruence.
           apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in Heqc0;
+            apply Nat.compare_eq in Heqc0;
             rewrite Pos.eqb_eq in *; subst; congruence.
   Qed.
 
@@ -202,25 +202,25 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                  destruct (morePrecise m0 m) eqn:?;
                  try (split; auto; fail).
         * destruct m, m0; cbn in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3.
+          rewrite Nat.compare_antisym.
+          rewrite Pos.compare_antisym.
           rewrite Pos.leb_compare in *.
-          destruct (w ?= w0); simpl in *; try congruence.
-          rewrite Pos.compare_antisym; auto.
+          destruct (w0 ?= w); simpl in *; try congruence.
         * destruct m, m0; unfold morePrecise in *; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
     - rewrite unopEq_sym.
       destruct (unopEq u0 u) eqn:?;
                try rewrite unopEq_compat_eq in *; subst;
@@ -248,25 +248,25 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                  destruct (morePrecise m0 m) eqn:?;
                  try (split; auto; fail).
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
         * destruct m, m0; simpl in *; try congruence.
-          setoid_rewrite Pos.compare_antisym at 3;
-            setoid_rewrite Pos.compare_antisym at 4.
+          setoid_rewrite Nat.compare_antisym at 2.
+          setoid_rewrite Pos.compare_antisym at 2.
           destruct (w ?= w0) eqn:?;
-                   destruct (f ?= f0) eqn:?; simpl; auto.
+                   destruct (f ?= f0)%nat eqn:?; simpl; auto.
   Qed.
 
   Lemma exprCompare_eq_sym e1 e2:
@@ -290,9 +290,9 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
       + rewrite mTypeEq_compat_eq in Heqb; subst.
         rewrite Heqb0. type_conv; subst. destruct m0, m1; try congruence;
         try destruct (morePrecise _ _) eqn:?; try congruence.
-        destruct (w ?= w0) eqn:?; destruct (f ?= f0) eqn:?; try congruence.
+        destruct (w ?= w0) eqn:?; destruct (f ?= f0)%nat eqn:?; try congruence.
         apply Ndec.Pcompare_Peqb in Heqc;
-          apply Ndec.Pcompare_Peqb in Heqc0;
+          apply Nat.compare_eq in Heqc0;
           rewrite Pos.eqb_eq in *; subst; congruence.
       + rewrite mTypeEq_compat_eq in Heqb0; subst.
         rewrite Heqb; destruct (morePrecise m m1) eqn:?; congruence.
@@ -300,13 +300,13 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         * destruct (morePrecise m0 m1);  destruct m, m0, m1; try congruence;
           destruct (w0 ?= w1) eqn:?; try congruence;
             apply Ndec.Pcompare_Peqb in Heqc;
-              apply Ndec.Pcompare_Peqb in compare_eq;
+              apply Nat.compare_eq in compare_eq;
               rewrite Pos.eqb_eq in *; subst; congruence.
         * destruct (morePrecise m m1); destruct (morePrecise m0 m1);
             destruct m, m0, m1; try congruence;
           destruct (w0 ?= w1) eqn:?; try congruence;
             apply Ndec.Pcompare_Peqb in Heqc;
-              apply Ndec.Pcompare_Peqb in compare_eq;
+              apply Nat.compare_eq in compare_eq;
               rewrite Pos.eqb_eq in *; subst; congruence.
     - destruct (unopEq u u0) eqn:?; destruct (unopEq u0 u1) eqn:?;
                try rewrite unopEq_compat_eq in *; subst;
@@ -341,7 +341,7 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         try destruct (morePrecise _ _) eqn:?; try congruence.
         destruct (w ?= w0) eqn:?; try congruence;
           apply Ndec.Pcompare_Peqb in Heqc;
-          apply Ndec.Pcompare_Peqb in compare_eq;
+          apply Nat.compare_eq in compare_eq;
           rewrite Pos.eqb_eq in *; subst; congruence.
       + rewrite mTypeEq_compat_eq in Heqb0; subst.
         rewrite Heqb; destruct (morePrecise m m1) eqn:?; congruence.
@@ -349,13 +349,13 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         * destruct (morePrecise m0 m1);  destruct m, m0, m1; try congruence;
             destruct (w0 ?= w1) eqn:?; try congruence;
             apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in compare_eq;
+            apply Nat.compare_eq in compare_eq;
             rewrite Pos.eqb_eq in *; subst; congruence.
         * destruct (morePrecise m m1); destruct (morePrecise m0 m1);
             destruct m, m0, m1; try congruence;
             destruct (w0 ?= w1) eqn:?; try congruence;
             apply Ndec.Pcompare_Peqb in Heqc;
-            apply Ndec.Pcompare_Peqb in compare_eq;
+            apply Nat.compare_eq in compare_eq;
             rewrite Pos.eqb_eq in *; subst; congruence.
   Qed.
 
@@ -377,19 +377,19 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         try destruct (morePrecise _ _) eqn:?; try congruence;
         destruct m, m1; try congruence; type_conv;
           destruct (w ?= w0) eqn:case1;
-                   destruct (f ?= f0) eqn:case2;
+                   destruct (f ?= f0)%nat eqn:case2;
                    try congruence;
             apply Ndec.Pcompare_Peqb in case1;
-            apply Ndec.Pcompare_Peqb in case2;
+            apply Nat.compare_eq in case2;
             rewrite Pos.eqb_eq in *; subst; congruence.
       + type_conv; subst.
         destruct (mTypeEq m m1); type_conv; destruct m, m0, m1; try congruence;
           try (repeat destruct (morePrecise _ _)); try congruence;
           destruct (w ?= w0) eqn:case1;
-                   destruct (f ?= f0) eqn:case2;
+                   destruct (f ?= f0)%nat eqn:case2;
                    try congruence;
             apply Ndec.Pcompare_Peqb in case1;
-            apply Ndec.Pcompare_Peqb in case2;
+            apply Nat.compare_eq in case2;
             rewrite Pos.eqb_eq in *; subst; congruence.
     - destruct (unopEq u u0) eqn:?; destruct (unopEq u0 u1) eqn:?;
                try rewrite unopEq_compat_eq in *; subst;
@@ -424,20 +424,21 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
       + rewrite mTypeEq_compat_eq in Heqb0; subst.
         rewrite Heqb; destruct m, m1; try (repeat destruct (morePrecise _ _)); try congruence.
           destruct (w ?= w0) eqn:case1;
-                   destruct (f ?= f0) eqn:case2;
+                   destruct (f ?= f0)%nat eqn:case2;
                    try congruence;
             apply Ndec.Pcompare_Peqb in case1;
-            apply Ndec.Pcompare_Peqb in case2;
+            apply Nat.compare_eq in case2;
             rewrite Pos.eqb_eq in *; subst; cbn in *;
-              repeat rewrite Pos.eqb_refl in *; simpl in *; congruence.
+              repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+          rewrite Nat.eqb_neq in *; congruence.
       + type_conv; subst.
         destruct (mTypeEq m m1); type_conv; destruct m, m0, m1; try congruence;
           try (repeat destruct (morePrecise _ _)); try congruence;
           destruct (w ?= w0) eqn:case1;
-                   destruct (f ?= f0) eqn:case2;
+                   destruct (f ?= f0)%nat eqn:case2;
                    try congruence;
             apply Ndec.Pcompare_Peqb in case1;
-            apply Ndec.Pcompare_Peqb in case2;
+            apply Nat.compare_eq in case2;
             rewrite Pos.eqb_eq in *; subst; cbn in *;
               repeat rewrite Pos.eqb_refl in *; simpl in *; congruence.
   Qed.
@@ -490,10 +491,10 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
             try pose proof (morePrecise_antisym _ _ Heqb1 Heqb2);
             type_conv; try congruence; unfold morePrecise in *; simpl in *;
               try congruence;
-              rewrite Pos.compare_antisym in lt_e2_e3 at 1;
-              setoid_rewrite Pos.compare_antisym in lt_e2_e3 at 2;
+              rewrite Pos.compare_antisym in lt_e2_e3;
+              rewrite Nat.compare_antisym in lt_e2_e3;
               destruct (w0 ?= w) eqn:case1;
-                destruct (f0 ?= f) eqn:case2;
+                destruct (f0 ?= f)%nat eqn:case2;
                 cbn in *;
                 try congruence. }
           { destruct (morePrecise m m0) eqn:?;
@@ -511,8 +512,8 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                 try rewrite case_w0;
                 try rewrite case_w1; try auto;
                 try rewrite Pos.compare_refl;
-                [ rewrite Pos.compare_lt_iff in *;
-                  eapply Pos.lt_trans; eauto  | ].
+                [ rewrite Nat.compare_lt_iff in *;
+                  eapply Nat.lt_trans; eauto  | ].
               assert (w ?= w1 = Lt).
               { rewrite Pos.compare_lt_iff in *;
                   eapply Pos.lt_trans; eauto. }
@@ -527,8 +528,8 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                 try rewrite case_w0;
                 try rewrite case_w1; try auto;
                 try rewrite Pos.compare_refl;
-                [ rewrite Pos.compare_lt_iff in *;
-                  eapply Pos.lt_trans; eauto  | ].
+                [ rewrite Nat.compare_lt_iff in *;
+                  eapply Nat.lt_trans; eauto  | ].
               assert (w ?= w1 = Lt).
               { rewrite Pos.compare_lt_iff in *;
                   eapply Pos.lt_trans; eauto. }
@@ -543,8 +544,8 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                 try rewrite case_w0;
                 try rewrite case_w1; try auto;
                 try rewrite Pos.compare_refl;
-                [ rewrite Pos.compare_lt_iff in *;
-                  eapply Pos.lt_trans; eauto  | ].
+                [ rewrite Nat.compare_lt_iff in *;
+                  eapply Nat.lt_trans; eauto  | ].
               assert (w ?= w1 = Lt).
               { rewrite Pos.compare_lt_iff in *;
                   eapply Pos.lt_trans; eauto. }
@@ -559,8 +560,8 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                 try rewrite case_w0;
                 try rewrite case_w1; try auto;
                 try rewrite Pos.compare_refl;
-                [ rewrite Pos.compare_lt_iff in *;
-                  eapply Pos.lt_trans; eauto  | ].
+                [ rewrite Nat.compare_lt_iff in *;
+                  eapply Nat.lt_trans; eauto  | ].
               assert (w ?= w1 = Lt).
               { rewrite Pos.compare_lt_iff in *;
                   eapply Pos.lt_trans; eauto. }
@@ -620,9 +621,9 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                        try pose proof (morePrecise_antisym _ _ prec1 prec2);
                        type_conv; try congruence;
                          simpl in *; try congruence;
-            setoid_rewrite Pos.compare_antisym in lt_e2_e3 at 1;
-            setoid_rewrite Pos.compare_antisym in lt_e2_e3 at 2;
-            destruct (w ?= w0) eqn:?; destruct (f ?= f0) eqn:?;
+            rewrite Pos.compare_antisym in lt_e2_e3;
+            rewrite Nat.compare_antisym in lt_e2_e3;
+            destruct (w ?= w0) eqn:?; destruct (f ?= f0)%nat eqn:?;
                      cbn in *; try congruence. }
           { type_conv; subst.
             destruct (morePrecise m1 m0) eqn:prec1;
@@ -633,12 +634,13 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
                 try (apply Ndec.Pcompare_Peqb in case_w0);
                 try (apply Ndec.Pcompare_Peqb in case_w1);
                 try rewrite Pos.eqb_eq in *;
+                try rewrite Nat.eqb_eq in *;
                 subst;
                 try congruence;
                 try rewrite case_w0;
                 try rewrite case_w1; try auto;
                 try rewrite Pos.compare_refl;
-                try (rewrite Pos.compare_lt_iff in *; eapply Pos.lt_trans; eauto);
+                try (rewrite Nat.compare_lt_iff in *; eapply Nat.lt_trans; eauto);
                 assert (w ?= w1 = Lt) as G
                     by (rewrite Pos.compare_lt_iff in *;
                         eapply Pos.lt_trans; eauto);
@@ -660,16 +662,16 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         rewrite (V_orderedFacts.compare_compat e1_eq_e2 e3_eq_e4).
         split; auto.
       + destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
     - destruct (unopEq u u0) eqn:?;
                destruct (unopEq u1 u2) eqn:?;
@@ -722,16 +724,16 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
          destruct (mTypeEq m0 m2); try congruence.
          split; auto.
       + destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:c1; destruct (f ?= f0) eqn:c2; try congruence;
-          apply Ndec.Pcompare_Peqb in c1; apply Ndec.Pcompare_Peqb in c2;
+        destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%nat eqn:c2; try congruence;
+          apply Ndec.Pcompare_Peqb in c1; apply Nat.compare_eq in c2;
         rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
   Qed.
 
@@ -750,26 +752,26 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
         rewrite (V_orderedFacts.compare_compat e1_eq_e2 e3_eq_e4).
         split; auto.
       + destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Nat.eqb_refl, Pos.eqb_refl in *; simpl in *; try congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Pos.eqb_refl, Nat.eqb_refl in *; simpl in *; try congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Nat.eqb_refl, Pos.eqb_refl in *; simpl in *; try congruence.
     - destruct (unopEq u u0) eqn:?;
                destruct (unopEq u1 u2) eqn:?;
                try rewrite unopEq_compat_eq in *; subst;
@@ -829,26 +831,26 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
          destruct (mTypeEq m0 m2); try congruence.
          split; auto.
       + destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Nat.eqb_refl, Pos.eqb_refl in *; simpl in *; try congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Pos.eqb_refl, Nat.eqb_refl in *; simpl in *; try congruence.
       + destruct (morePrecise m m0); destruct m, m0; try congruence;
-        destruct (w ?= w0) eqn:case1; destruct (f ?= f0) eqn:case2;
+        destruct (w ?= w0) eqn:case1; destruct (f ?= f0)%nat eqn:case2;
           try congruence;
           apply Ndec.Pcompare_Peqb in case1;
-          apply Ndec.Pcompare_Peqb in case2;
+          apply Nat.compare_eq in case2;
           rewrite Pos.eqb_eq in *; subst; cbn in *;
-            repeat rewrite Pos.eqb_refl in *; simpl in *; try congruence.
+            repeat rewrite Nat.eqb_refl, Pos.eqb_refl in *; simpl in *; try congruence.
   Qed.
 
   Lemma compare_spec : forall x y, CompSpec eq lt x y (exprCompare x y).
diff --git a/coq/RealRangeArith.v b/coq/RealRangeArith.v
index 81488c0c3c3a62a97af38242b0381add3364f48e..0ee4801c02c675503db06f1bbbfa4515053c60b8 100644
--- a/coq/RealRangeArith.v
+++ b/coq/RealRangeArith.v
@@ -28,41 +28,42 @@ Ltac kill_trivial_exists :=
   | [ |- exists iv err, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
   end.
 
-Fixpoint validRanges e (A:analysisResult) E Gamma :Prop :=
+Fixpoint validRanges e (A:analysisResult) E Gamma fBits:Prop :=
   match e with
   | Var _ x => True
   | Const m v => True
-  | Unop u e1 => validRanges e1 A E Gamma
+  | Unop u e1 => validRanges e1 A E Gamma fBits
   | Binop b e1 e2 =>
     (b = Div ->
      (forall iv2 err,
          FloverMap.find e2 A = Some (iv2, err) ->
          ((Qleb (ivhi iv2) 0) && (negb (Qeq_bool (ivhi iv2) 0))) ||
          ((Qleb 0 (ivlo iv2)) && (negb (Qeq_bool (ivlo iv2) 0))) = true)) /\
-    validRanges e1 A E Gamma /\ validRanges e2 A E Gamma
+    validRanges e1 A E Gamma fBits /\ validRanges e2 A E Gamma fBits
   | Fma e1 e2 e3 =>
-    validRanges e1 A E Gamma /\ validRanges e2 A E Gamma /\ validRanges e3 A E Gamma
-  | Downcast m e1 => validRanges e1 A E Gamma
+    validRanges e1 A E Gamma fBits /\ validRanges e2 A E Gamma fBits /\
+    validRanges e3 A E Gamma fBits
+  | Downcast m e1 => validRanges e1 A E Gamma fBits
   end /\
   exists iv err vR,
     FloverMap.find e A = Some (iv, err) /\
-    eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
+    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
     (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 
-Corollary validRanges_single e A E Gamma:
-  validRanges e A E Gamma ->
+Corollary validRanges_single e A E Gamma fBits:
+  validRanges e A E Gamma fBits ->
   exists iv err vR,
     FloverMap.find e A = Some (iv, err) /\
-    eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL /\
+    eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL /\
     (Q2R (fst iv) <= vR <= Q2R (snd iv))%R.
 Proof.
   destruct e; intros [_ valid_e]; simpl in *; try auto.
 Qed.
 
-Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
+Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2 fBits:
   (forall n, Gamma1 n = Gamma2 n) ->
-  eval_expr E Gamma1 e vR m ->
-  eval_expr E Gamma2 e vR m.
+  eval_expr E Gamma1 fBits e vR m ->
+  eval_expr E Gamma2 fBits e vR m.
 Proof.
   revert E vR Gamma1 Gamma2 m;
     induction e; intros * Gamma_eq eval_e;
@@ -72,10 +73,10 @@ Proof.
   rewrite <- Gamma_eq; auto.
 Qed.
 
-Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 :
+Lemma swap_Gamma_bstep f E vR m Gamma1 Gamma2 fBits :
   (forall n, Gamma1 n = Gamma2 n) ->
-  bstep f E Gamma1 vR m ->
-  bstep f E Gamma2 vR m.
+  bstep f E Gamma1 fBits vR m ->
+  bstep f E Gamma2 fBits vR m.
 Proof.
   revert E Gamma1 Gamma2;
   induction f; intros * Gamma_eq eval_f.
@@ -92,10 +93,10 @@ Proof.
 Qed.
 
 Lemma validRanges_swap Gamma1 Gamma2:
-  forall e A E,
+  forall e A E fBits,
     (forall n, (toRMap Gamma1) n =  toRMap (Gamma2) n) ->
-    validRanges e A E Gamma1 ->
-    validRanges e A E Gamma2.
+    validRanges e A E Gamma1 fBits ->
+    validRanges e A E Gamma2 fBits.
 Proof.
   induction e; intros * Gamma_swap valid1; simpl in *; try (split; auto);
     try (
@@ -110,34 +111,34 @@ Proof.
   - destruct valid1; auto.
 Qed.
 
-Fixpoint validRangesCmd (f:cmd Q) A E Gamma {struct f} : Prop :=
+Fixpoint validRangesCmd (f:cmd Q) A E Gamma fBits {struct f} : Prop :=
   match f with
   | Let m x e g =>
-    validRanges e A E Gamma /\
-    (forall vR, eval_expr E (toRMap Gamma) (toREval (toRExp e)) vR REAL ->
-             validRangesCmd g A (updEnv x vR E) (updDefVars x REAL Gamma))
-  | Ret e => validRanges e A E Gamma
+    validRanges e A E Gamma fBits /\
+    (forall vR, eval_expr E (toRMap Gamma) fBits (toREval (toRExp e)) vR REAL ->
+             validRangesCmd g A (updEnv x vR E) (updDefVars x REAL Gamma) fBits)
+  | Ret e => validRanges e A E Gamma fBits
   end /\
   exists iv_e err_e vR,
     FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
-    bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR REAL /\
+    bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) fBits vR REAL /\
     (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
 
-Corollary validRangesCmd_single f A E Gamma:
-  validRangesCmd f A E Gamma ->
+Corollary validRangesCmd_single f A E Gamma fBits:
+  validRangesCmd f A E Gamma fBits ->
   exists iv_e err_e vR,
     FloverMap.find (getRetExp f) A = Some (iv_e, err_e) /\
-    bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) vR REAL /\
+    bstep (toREvalCmd (toRCmd f)) E (toRMap Gamma) fBits vR REAL /\
     (Q2R (fst iv_e) <=  vR <= Q2R (snd iv_e))%R.
 Proof.
   destruct f; simpl in *; intros [ _ valid_f]; auto.
 Qed.
 
 Lemma validRangesCmd_swap:
-  forall f A E Gamma1 Gamma2,
+  forall f A E Gamma1 Gamma2 fBits,
     (forall n, (toRMap Gamma1) n =  toRMap (Gamma2) n) ->
-    validRangesCmd f A E Gamma1 ->
-    validRangesCmd f A E Gamma2.
+    validRangesCmd f A E Gamma1 fBits ->
+    validRangesCmd f A E Gamma2 fBits.
 Proof.
   induction f; intros * Gamma_swap valid1; simpl in *; try (split; auto);
     try (
diff --git a/coq/RealRangeValidator.v b/coq/RealRangeValidator.v
index 89987b09ae9d00e271b2e6662f0e343deb2c9208..5ffac7214808600edc7cf66082963d921e6bbeba 100644
--- a/coq/RealRangeValidator.v
+++ b/coq/RealRangeValidator.v
@@ -14,13 +14,13 @@ Definition RangeValidator e A P dVars:=
        end.
 
 Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond) dVars
-        (E : env) (Gamma : nat -> option mType) :
+        (E : env) (Gamma : nat -> option mType) fBits:
   RangeValidator e A P dVars = true ->
   dVars_range_valid dVars E A ->
   affine_dVars_range_valid dVars E A 1 (FloverMap.empty (affine_form Q)) (fun _: nat => None) ->
   fVars_P_sound (usedVars e) E P ->
   vars_typed (NatSet.union (usedVars e) dVars) Gamma ->
-  validRanges e A E Gamma.
+  validRanges e A E Gamma fBits.
 Proof.
   intros.
   unfold RangeValidator in *.
@@ -38,7 +38,7 @@ Proof.
     pose proof (validAffineBounds_sound) as sound_affine.
     assert ((forall e' : FloverMap.key,
                 (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
-                checked_expressions A E Gamma (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
+                checked_expressions A E Gamma fBits (usedVars e) dVars e' iexpmap inoise imap)) as Hchecked
         by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
             rewrite FloverMapFacts.P.F.empty_o in Hein;
             congruence).
@@ -48,7 +48,7 @@ Proof.
     assert (affine_fVars_P_sound (usedVars e) E P) as HfVars by exact H2.
     assert (affine_vars_typed (usedVars e ∪ dVars) Gamma) as Hvarstyped
         by exact H3.
-    specialize (sound_affine e A P (usedVars e) dVars E Gamma
+    specialize (sound_affine e A P (usedVars e) dVars E Gamma fBits
                              exprAfs noise iexpmap inoise imap
                              Hchecked Hinoise Himap Hafcheck H1 Hsubset HfVars Hvarstyped)
       as [map2 [af [vR [aiv [aerr sound_affine]]]]].
@@ -65,7 +65,7 @@ Definition RangeValidatorCmd e A P dVars:=
        end.
 
 Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) dVars
-        (E : env) (Gamma : nat -> option mType) fVars outVars:
+        (E : env) (Gamma : nat -> option mType) fBits fVars outVars:
   RangeValidatorCmd f A P dVars = true ->
   ssa f (NatSet.union fVars dVars) outVars ->
   dVars_range_valid dVars E A ->
@@ -73,7 +73,7 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond) d
   fVars_P_sound fVars E P ->
   vars_typed (NatSet.union fVars dVars) Gamma ->
   NatSet.Subset (freeVars f -- dVars) fVars ->
-  validRangesCmd f A E Gamma.
+  validRangesCmd f A E Gamma fBits.
 Proof.
   intros ranges_valid; intros.
   unfold RangeValidatorCmd in ranges_valid.
@@ -89,7 +89,7 @@ Proof.
     pose proof (validAffineBoundsCmd_sound) as sound_affine.
     assert ((forall e' : FloverMap.key,
                 (exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
-                checked_expressions A E Gamma fVars dVars e' iexpmap inoise imap)) as Hchecked
+                checked_expressions A E Gamma fBits fVars dVars e' iexpmap inoise imap)) as Hchecked
         by (intros e' Hein; destruct Hein as [af Hein]; unfold iexpmap in Hein;
             rewrite FloverMapFacts.P.F.empty_o in Hein;
             congruence).
@@ -98,7 +98,7 @@ Proof.
     assert (affine_fVars_P_sound fVars E P) as HfVars by exact H2.
     assert (affine_vars_typed (fVars ∪ dVars) Gamma) as Hvarstyped
         by exact H3.
-    specialize (sound_affine f A P fVars dVars outVars E Gamma
+    specialize (sound_affine f A P fBits fVars dVars outVars E Gamma
                              exprAfs noise iexpmap inoise imap
                              Hchecked Hinoise Himap Hafcheck H H1 H4 HfVars Hvarstyped)
       as [map2 [af [vR [aiv [aerr sound_affine]]]]].
diff --git a/coq/RoundoffErrorValidator.v b/coq/RoundoffErrorValidator.v
index 556eeb045a310261f95f3b78c7054224b772a88f..f1f1ddc44624248addb445b7edb69841dd80b2cd 100644
--- a/coq/RoundoffErrorValidator.v
+++ b/coq/RoundoffErrorValidator.v
@@ -14,17 +14,20 @@ Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType) (A:analysi
 Theorem RoundoffErrorValidator_sound:
 forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
          (nR : R) (err : error) (elo ehi : Q) (Gamma : FloverMap.t mType)
-         (defVars : nat -> option mType),
-       typeCheck e defVars Gamma = true ->
+         (defVars : nat -> option mType) fBits,
+       typeCheck e defVars Gamma fBits = true ->
        approxEnv E1 defVars A fVars dVars E2 ->
        NatSet.Subset (usedVars e -- dVars) fVars ->
-       eval_expr E1 (toRMap defVars) (toREval (toRExp e)) nR REAL ->
+       eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) nR REAL ->
        RoundoffErrorValidator e Gamma A dVars = true ->
-       validRanges e A E1 defVars ->
+       validRanges e A E1 defVars (toRBMap fBits) ->
        vars_typed (fVars ∪ dVars) defVars ->
        FloverMap.find (elt:=intv * error) e A = Some (elo, ehi, err) ->
-       (exists (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m) /\
-       (forall (nF : R) (m : mType), eval_expr E2 defVars (toRExp e) nF m -> (Rabs (nR - nF) <= Q2R err)%R).
+       (exists (nF : R) (m : mType),
+           eval_expr E2 defVars (toRBMap fBits) (toRExp e) nF m) /\
+       (forall (nF : R) (m : mType),
+           eval_expr E2 defVars (toRBMap fBits) (toRExp e) nF m ->
+           (Rabs (nR - nF) <= Q2R err)%R).
 Proof.
   intros. cbn in *.
   eapply validErrorbound_sound; eauto.
@@ -37,20 +40,20 @@ Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType) (A:analy
   (* else validAffineErrorboundsCmd e A tMap dVars ... *)
 
 Theorem RoundoffErrorValidatorCmd_sound f:
-  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars,
-    typeCheckCmd f defVars Gamma = true ->
+  forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma defVars fBits,
+    typeCheckCmd f defVars Gamma fBits = true ->
     approxEnv E1 defVars 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 (toRMap defVars) vR REAL ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toRMap defVars) (toRBMap fBits) vR REAL ->
     validErrorboundCmd f Gamma A dVars = true ->
-    validRangesCmd f A E1 defVars ->
+    validRangesCmd f A E1 defVars (toRBMap fBits) ->
     vars_typed (NatSet.union fVars dVars) defVars ->
     FloverMap.find (getRetExp f) A = Some ((elo,ehi),err) ->
     (exists vF m,
-        bstep (toRCmd f) E2 defVars vF m) /\
+        bstep (toRCmd f) E2 defVars (toRBMap fBits) vF m) /\
     (forall vF mF,
-    bstep (toRCmd f) E2 defVars vF mF ->
+    bstep (toRCmd f) E2 defVars (toRBMap fBits) vF mF ->
     (Rabs (vR - vF) <= (Q2R err))%R).
 Proof.
   intros.
diff --git a/coq/Typing.v b/coq/Typing.v
index 7fffcd1a80f5a5f2640a3d8b40d0cad5bf297f9f..2ab5e3a0b76bd64ed5608c4b7f37f637b1bfe70a 100644
--- a/coq/Typing.v
+++ b/coq/Typing.v
@@ -14,35 +14,36 @@ From Flover
      Require Export Infra.ExpressionAbbrevs Infra.RealSimps Infra.NatSet
      Infra.MachineType.
 
-Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:expr V) : option mType :=
-  match e with
-  | Var _ v => Gamma v
-  | Const m n => Some m
-  | Unop u e1 => typeExpression Gamma e1
-  | Binop b e1 e2 =>
-    let tm1 := typeExpression Gamma e1 in
-    let tm2 := typeExpression Gamma e2 in
-    match tm1, tm2 with
-    | Some m1, Some m2 => Some (join m1 m2)
-    | _, _ => None
-    end
-  | Fma e1 e2 e3 =>
-    let tm1 := typeExpression Gamma e1 in
-    let tm2 := typeExpression Gamma e2 in
-    let tm3 := typeExpression Gamma e3 in
-    match tm1, tm2, tm3 with
-    | Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
-    | _, _,_ => None
-    end
-  | Downcast m e1 =>
-    let tm1 := typeExpression Gamma e1 in
-    match tm1 with
-    |Some m1 => if (morePrecise m1 m) then Some m else None
-    |_ => None
-    end
-  end.
+(* Fixpoint typeExpression (V:Type) (Gamma:nat -> option mType) (e:expr V) : option mType := *)
+(*   match e with *)
+(*   | Var _ v => Gamma v *)
+(*   | Const m n => Some m *)
+(*   | Unop u e1 => typeExpression Gamma e1 *)
+(*   | Binop b e1 e2 => *)
+(*     let tm1 := typeExpression Gamma e1 in *)
+(*     let tm2 := typeExpression Gamma e2 in *)
+(*     match tm1, tm2 with *)
+(*     | Some m1, Some m2 => Some (join m1 m2) *)
+(*     | _, _ => None *)
+(*     end *)
+(*   | Fma e1 e2 e3 => *)
+(*     let tm1 := typeExpression Gamma e1 in *)
+(*     let tm2 := typeExpression Gamma e2 in *)
+(*     let tm3 := typeExpression Gamma e3 in *)
+(*     match tm1, tm2, tm3 with *)
+(*     | Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3) *)
+(*     | _, _,_ => None *)
+(*     end *)
+(*   | Downcast m e1 => *)
+(*     let tm1 := typeExpression Gamma e1 in *)
+(*     match tm1 with *)
+(*     |Some m1 => if (morePrecise m1 m) then Some m else None *)
+(*     |_ => None *)
+(*     end *)
+(*   end. *)
 
 Fixpoint typeMap (Gamma:nat -> option mType) (e:expr Q) (tMap:FloverMap.t mType)
+         (fBits:FloverMap.t nat)
   : FloverMap.t mType :=
   if (FloverMap.mem e tMap)
   then tMap
@@ -54,33 +55,63 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:expr Q) (tMap:FloverMap.t mType)
                 end
     | Const m n => FloverMap.add e m tMap
     | Unop u e1 =>
-      let tMap_new := typeMap Gamma e1 tMap in
+      let tMap_new := typeMap Gamma e1 tMap fBits in
       match FloverMap.find e1 tMap_new with
       | Some m_e1 => FloverMap.add e m_e1 tMap
       | None => FloverMap.empty mType
       end
   | Binop b e1 e2 =>
-    let tMap1 := typeMap Gamma e1 tMap in
-    let tMap2 := typeMap Gamma e2 tMap1 in
+    let tMap1 := typeMap Gamma e1 tMap fBits in
+    let tMap2 := typeMap Gamma e2 tMap1 fBits in
     let m1 := FloverMap.find e1 tMap2 in
     let m2 := FloverMap.find e2 tMap2 in
     match m1, m2 with
-    |Some t1, Some t2 => FloverMap.add e (join t1 t2) tMap2
+    |Some t1, Some t2 =>
+     if (isFixedPointB t1 && isFixedPointB t2)
+     then
+       match (FloverMap.find e fBits) with
+       | None => FloverMap.empty mType
+       | Some n =>
+         match (join t1 t2 n) with
+         |Some m => FloverMap.add e m tMap2
+         |None => FloverMap.empty mType
+         end
+       end
+    else
+      match (join t1 t2 0) with
+      | Some m => FloverMap.add e m tMap2
+      | None => FloverMap.empty mType
+      end
     | _, _ => FloverMap.empty mType
     end
   | Fma e1 e2 e3 =>
-    let tMap1 := typeMap Gamma e1 tMap in
-    let tMap2 := typeMap Gamma e2 tMap1 in
-    let tMap3 := typeMap Gamma e3 tMap2 in
+    let tMap1 := typeMap Gamma e1 tMap fBits in
+    let tMap2 := typeMap Gamma e2 tMap1 fBits in
+    let tMap3 := typeMap Gamma e3 tMap2 fBits in
     let m1 := FloverMap.find e1 tMap3 in
     let m2 := FloverMap.find e2 tMap3 in
     let m3 := FloverMap.find e3 tMap3 in
     match m1, m2, m3 with
-    |Some t1, Some t2, Some t3 => FloverMap.add e (join3 t1 t2 t3) tMap3
+    |Some t1, Some t2, Some t3 =>
+     if (isFixedPointB t1 && isFixedPointB t2 && isFixedPointB t3)
+     then
+       match (FloverMap.find e fBits) with
+       | None => FloverMap.empty mType
+       | Some n =>
+         match (join3 t1 t2 t3 n) with
+         |Some m => FloverMap.add e m tMap3
+         |None => FloverMap.empty mType
+         end
+       end
+     else
+       match (join3 t1 t2 t3 0) with
+       |Some m => FloverMap.add e m tMap3
+       | _ => FloverMap.empty mType
+       end
     | _, _, _ => FloverMap.empty mType
     end
   | Downcast m e1 =>
-    let tMap_new := typeMap Gamma e1 tMap in
+    let tMap_new := typeMap Gamma e1 tMap fBits in
     let m1 := FloverMap.find e1 tMap_new in
     match m1 with
     | Some t1 =>
@@ -91,108 +122,414 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:expr Q) (tMap:FloverMap.t mType)
     end
   end.
 
-Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType :=
-  match f with
-  |Let m n e c => match typeExpression Gamma e with
-                 |Some m' => if morePrecise m m' then typeCmd Gamma c
-                            else None
-                 |None => None
-                 end
-  |Ret e => typeExpression Gamma e
-  end.
+(* Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType := *)
+(*   match f with *)
+(*   |Let m n e c => match typeExpression Gamma e with *)
+(*                  |Some m' => if morePrecise m m' then typeCmd Gamma c *)
+(*                             else None *)
+(*                  |None => None *)
+(*                  end *)
+(*   |Ret e => typeExpression Gamma e *)
+(*   end. *)
 
-Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap :=
+Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap fBits :=
   match f with
   |Let m n e g =>
-   let tMap_new := typeMap Gamma e tMap in
+   let tMap_new := typeMap Gamma e tMap fBits in
    let t_e := FloverMap.find e tMap_new in
    match t_e with
    |Some m_e =>
     if mTypeEq m m_e
-    then typeMapCmd Gamma g (FloverMap.add (Var Q n) m tMap_new)
+    then typeMapCmd Gamma g (FloverMap.add (Var Q n) m tMap_new) fBits
     else FloverMap.empty mType
    |None => FloverMap.empty mType
    end
-  |Ret e => typeMap Gamma e tMap
+  |Ret e => typeMap Gamma e tMap fBits
   end.
 
 Fixpoint typeCheck (e:expr Q) (Gamma:nat -> option mType)
-         (tMap: FloverMap.t mType) : bool :=
+         (tMap: FloverMap.t mType) (fBits:FloverMap.t nat) : bool :=
   match e with
-  | Var _ v => match FloverMap.find e tMap, Gamma v with
-              | Some m, Some m' => mTypeEq m m'
-              | _, _ => false
+  | Var _ v =>
+    match FloverMap.find e tMap, Gamma v with
+    | Some m, Some m' => mTypeEq m m'
+    | _, _ => false
+    end
+  | Const m n =>
+    match FloverMap.find e tMap with
+    | Some m' => mTypeEq m m'
+    | None => false
+    end
+  | Unop u e1 =>
+    match FloverMap.find e tMap with
+    | Some m =>
+      match FloverMap.find e1 tMap with
+      | Some m' => mTypeEq m m' && typeCheck e1 Gamma tMap fBits
+      | None => false
+      end
+    | None => false
+    end
+  | Binop b e1 e2 =>
+    match FloverMap.find e tMap, FloverMap.find e1 tMap, FloverMap.find e2 tMap with
+    | Some m, Some m1, Some m2 =>
+      let cond :=
+          if (isFixedPointB m1 && isFixedPointB m2)
+          then
+            match FloverMap.find e fBits with
+            |Some n =>
+             match join m1 m2 n with
+             |Some m' => mTypeEq m m'
+             |None => false
              end
-  | Const m n => match FloverMap.find e tMap with
-               | Some m' => mTypeEq m m'
-               | None => false
-               end
-  | Unop u e1 => match FloverMap.find e tMap with
-                | Some m => match FloverMap.find e1 tMap with
-                           | Some m' => mTypeEq m m' && typeCheck e1 Gamma tMap
-                           | None => false
-                           end
-                | None => false
-                end
-  | Binop b e1 e2 => match FloverMap.find e tMap, FloverMap.find e1 tMap, FloverMap.find e2 tMap with
-                    | Some m, Some m1, Some m2 =>
-                      mTypeEq m (join m1 m2)
-                              && typeCheck e1 Gamma tMap
-                              && typeCheck e2 Gamma tMap
-                    | _, _, _ => false
-                    end
-  | Fma e1 e2 e3 => match FloverMap.find e tMap, FloverMap.find e1 tMap, FloverMap.find e2 tMap, FloverMap.find e3 tMap with
-                   | Some m, Some m1, Some m2, Some m3 =>
-                     mTypeEq m (join3 m1 m2 m3)
-                             && typeCheck e1 Gamma tMap
-                             && typeCheck e2 Gamma tMap
-                             && typeCheck e3 Gamma tMap
-                   | _, _, _, _ => false
-                   end
-  | Downcast m e1 => match FloverMap.find e tMap, FloverMap.find e1 tMap with
-                    | Some m', Some m1 => mTypeEq m m' && morePrecise m1 m && typeCheck e1 Gamma tMap
-                    | _, _ => false
-                    end
+            |None => false
+            end
+          else
+            match join m1 m2 0 with
+            |Some m' => mTypeEq m m'
+            |None => false
+            end
+      in
+      cond && typeCheck e1 Gamma tMap fBits && typeCheck e2 Gamma tMap fBits
+    | _, _, _ => false
+    end
+  | Fma e1 e2 e3 =>
+    match FloverMap.find e tMap, FloverMap.find e1 tMap, FloverMap.find e2 tMap, FloverMap.find e3 tMap with
+    | Some m, Some m1, Some m2, Some m3 =>
+      let cond :=
+          if (isFixedPointB m1 && isFixedPointB m2 && isFixedPointB m3)
+          then
+            match FloverMap.find e fBits with
+            |Some n =>
+             match join3 m1 m2 m3 n with
+             |Some m' => mTypeEq m m'
+             |None => false
+             end
+            |None => false
+            end
+          else
+            match join3 m1 m2 m3 0 with
+            |Some m' => mTypeEq m m'
+            |None => false
+            end
+      in
+      cond
+        && typeCheck e1 Gamma tMap fBits
+        && typeCheck e2 Gamma tMap fBits
+        && typeCheck e3 Gamma tMap fBits
+    | _, _, _, _ => false
+    end
+  | Downcast m e1 =>
+    match FloverMap.find e tMap, FloverMap.find e1 tMap with
+    | Some m', Some m1 => mTypeEq m m' && morePrecise m1 m && typeCheck e1 Gamma tMap fBits
+    | _, _ => false
+    end
   end.
 
 Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType)
-         (tMap:FloverMap.t mType) : bool :=
+         (tMap:FloverMap.t mType) fBits : bool :=
   match c with
-  | Let m x e g => if typeCheck e Gamma tMap
-                  then
-                    match FloverMap.find e tMap, FloverMap.find (Var Q x) tMap with
-                    | Some me, Some mx =>  mTypeEq me m && mTypeEq m mx
-                                          && typeCheckCmd g (updDefVars x me Gamma) tMap
-                    | _, _ => false
-                    end
-                  else
-                    false
-  | Ret e => typeCheck e Gamma tMap
+  | Let m x e g =>
+    if typeCheck e Gamma tMap fBits
+    then
+      match FloverMap.find e tMap, FloverMap.find (Var Q x) tMap with
+      | Some me, Some mx =>
+        mTypeEq me m && mTypeEq m mx
+                && typeCheckCmd g (updDefVars x me Gamma) tMap fBits
+      | _, _ => false
+      end
+    else
+      false
+  | Ret e => typeCheck e Gamma tMap fBits
   end.
 
-Theorem typingSoundnessExp Gamma E:
+Theorem typingSoundnessExp Gamma E fBits:
   forall e v m exprTypes,
-    typeCheck e Gamma exprTypes = true ->
-    eval_expr E Gamma (toRExp e) v m ->
+    typeCheck e Gamma exprTypes fBits = true ->
+    eval_expr E Gamma (toRBMap fBits) (toRExp e) v m ->
     FloverMap.find e exprTypes = Some m.
 Proof.
-  induction e; cbn; intros * typechecks evals; Flover_compute; type_conv;
+  induction e; cbn; intros * typechecks evals;
     inversion evals; subst; try auto.
-  - rewrite Heqo0 in *. inversion H0; auto.
-  - erewrite IHe in *; eauto.
-  - erewrite IHe in *; eauto.
-  - erewrite IHe1 in *; eauto.
+  - Flover_compute; type_conv; auto.
+  - Flover_compute; type_conv; auto.
+  - Flover_compute; type_conv.
+    erewrite IHe in *; eauto.
+  - Flover_compute; type_conv.
+    erewrite IHe in *; eauto.
+  - destruct (FloverMap.find (elt:=mType) (Binop b e1 e2) exprTypes) eqn:?;
+             try congruence.
+    assert (typeCheck e1 Gamma exprTypes fBits = true)
+           by (Flover_compute; type_conv; eauto).
+    assert (typeCheck e2 Gamma exprTypes fBits = true)
+           by (Flover_compute; type_conv; eauto).
+    erewrite IHe1 in *; eauto.
     erewrite IHe2 in *; eauto.
-    inversion Heqo0; subst; inversion Heqo1; subst; auto.
-  - erewrite IHe1 in *; eauto.
+    destruct (isFixedPointB m1) eqn:m1_fixed;
+             destruct (isFixedPointB m2) eqn:m2_fixed;
+             [ | destruct m1, m2; cbn in *; try congruence
+               | destruct m1, m2; cbn in *; try congruence | ];
+             cbn in typechecks; type_conv.
+    + rewrite <- isFixedPoint_isFixedPointB in *.
+      Flover_compute; type_conv.
+      specialize (H8 m1_fixed m2_fixed).
+      apply toRBMap_some in Heqo0.
+      rewrite <- H9, <- Heqo1.
+      simpl in *.
+      assert (fBit = n) by congruence.
+      subst; auto.
+    + rewrite <- isFixedPoint_isFixedPointB_false in *.
+      rewrite join_float with (f2:=0%nat) in H9; try auto.
+      Flover_compute; type_conv; auto.
+  - destruct (FloverMap.find (elt:=mType) (Fma e1 e2 e3) exprTypes) eqn:?;
+             try congruence.
+    assert (typeCheck e1 Gamma exprTypes fBits = true)
+           by (Flover_compute; type_conv; eauto).
+    assert (typeCheck e2 Gamma exprTypes fBits = true)
+           by (Flover_compute; type_conv; eauto).
+    assert (typeCheck e3 Gamma exprTypes fBits = true)
+           by (Flover_compute; type_conv; eauto).
+    erewrite IHe1 in *; eauto.
     erewrite IHe2 in *; eauto.
     erewrite IHe3 in *; eauto.
-    inversion Heqo0; subst; inversion Heqo1; subst; inversion Heqo2; subst; auto.
+    unfold join3 in *.
+    destruct (isFixedPointB m2) eqn:m2_fixed;
+      destruct (isFixedPointB m3) eqn:m3_fixed;
+      [ | destruct m2, m3; cbn in *; try congruence |
+        destruct m2, m3; cbn in *; try congruence| ].
+    + destruct (join m2 m3 fBit) eqn:?; simpl in *; try congruence.
+      destruct (isFixedPointB m1) eqn:m1_fixed;
+        cbn in typechecks; type_conv.
+      * Flover_compute; type_conv. rewrite <- isFixedPoint_isFixedPointB in *.
+      specialize (H8 m1_fixed m2_fixed m3_fixed).
+      apply toRBMap_some in Heqo1.
+      rewrite <- H9, <- Heqo3.
+      simpl in *.
+      assert (fBit = n) by congruence.
+      subst.
+      assert (Some m5 = Some m4) by congruence.
+      congruence.
+      * Flover_compute.
+        assert (exists w f, m4 = F w f) as m4_fixed.
+        { destruct m2, m3; cbn in *; try congruence.
+          destruct (w0 <=? w)%positive.
+          - exists w, fBit; congruence.
+          - exists w0, fBit; congruence. }
+        destruct m4_fixed as [? [? ?]]; subst.
+        destruct m1; cbn in *; congruence.
+    + rewrite <- isFixedPoint_isFixedPointB_false in *.
+      rewrite join_float with (f2:=0%nat) in H9; try auto.
+      destruct (isFixedPointB m1) eqn:?; simpl in typechecks.
+      * destruct m1; simpl in *; try congruence.
+        assert (forall w f, join m2 m3 0 = Some (F w f) -> False).
+        { destruct m2, m3; cbn in *; try congruence; contradiction. }
+        Flover_compute.
+        destruct (join m2 m3 0); try congruence.
+        inversion Heqo2; inversion Heqo1; subst.
+        destruct m5; congruence.
+      * rewrite <- isFixedPoint_isFixedPointB_false in *; try auto.
+      Flover_compute; type_conv; auto.
+      rewrite <- Heqo0. rewrite <- H9.
+      setoid_rewrite join_float with (f2 := 0%nat) at 2; try auto; try congruence.
+      hnf; intros isFP.
+      destruct m2, m3; cbn in *; inversion Heqo1; subst; cbn in isFP; try congruence.
+      contradiction.
+  - Flover_compute; type_conv; auto.
+Qed.
+
+Lemma typingFixedPoint_binop_defined b e1 e2 m1 m2 Gamma exprTypes fBits:
+  typeCheck (Binop b e1 e2) Gamma exprTypes fBits = true ->
+  FloverMap.find e1 exprTypes = Some m1 ->
+  FloverMap.find e2 exprTypes = Some m2 ->
+  exists fBit,
+    isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop b e1 e2) fBits = Some fBit.
+Proof.
+  intros * subexpr_ok type_e1 type_e2.
+  cbn in subexpr_ok.
+  rewrite type_e1, type_e2 in *.
+  destruct (FloverMap.find (elt:=mType) (Binop b e1 e2) exprTypes); try congruence.
+  destruct (isFixedPointB m1) eqn:m1_fixed;
+    destruct (isFixedPointB m2) eqn:m2_fixed;
+    [ | destruct m1, m2; cbn in *; try congruence | destruct m1, m2; cbn in *; try congruence| ].
+  - rewrite <- isFixedPoint_isFixedPointB in *.
+    simpl in subexpr_ok; Flover_compute.
+    exists n; auto.
+  - rewrite <- isFixedPoint_isFixedPointB_false in *.
+    exists 0%nat.
+    intros; contradiction.
+Qed.
+
+Lemma typingBinop_join_defined b e1 m1 e2 m2 Gamma exprTypes fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find (Binop b e1 e2) fBits = Some fBit) ->
+  typeCheck (Binop b e1 e2) Gamma exprTypes fBits = true ->
+  FloverMap.find e1 exprTypes = Some m1 ->
+  FloverMap.find e2 exprTypes = Some m2 ->
+  exists m, join m1 m2 fBit = Some m.
+Proof.
+  intros validFixed typing_ok find_e1 find_e2.
+  cbn in typing_ok.
+  rewrite find_e1, find_e2 in *.
+  destruct (FloverMap.find (elt:=mType) (Binop b e1 e2) exprTypes) eqn:?; try congruence.
+  destruct (isFixedPointB m1) eqn:m1_fixed;
+    destruct (isFixedPointB m2) eqn:m2_fixed;
+    [ | destruct m1, m2; cbn in *; try congruence | destruct m1, m2; cbn in *; try congruence| ].
+  - rewrite <- isFixedPoint_isFixedPointB in *.
+    specialize (validFixed m1_fixed m2_fixed); rewrite validFixed in *;
+      inversion Heqo; subst.
+    simpl in *. Flover_compute; try congruence.
+    type_conv. eauto.
+  - rewrite <- isFixedPoint_isFixedPointB_false in *.
+    simpl in *. Flover_compute.
+    type_conv. exists m0; rewrite <- Heqo0.
+    rewrite join_float with (f2:=0%nat); auto.
+Qed.
+
+Lemma typingFixedPoint_fma_defined e1 e2 e3 m1 m2 m3 Gamma exprTypes fBits:
+  typeCheck (Fma e1 e2 e3) Gamma exprTypes fBits = true ->
+  FloverMap.find e1 exprTypes = Some m1 ->
+  FloverMap.find e2 exprTypes = Some m2 ->
+  FloverMap.find e3 exprTypes = Some m3 ->
+  exists fBit,
+    isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
+    FloverMap.find (Fma e1 e2 e3) fBits = Some fBit.
+Proof.
+  intros * subexpr_ok type_e1 type_e2 type_e3.
+  cbn in subexpr_ok.
+  rewrite type_e1, type_e2, type_e3 in *.
+  destruct (FloverMap.find (elt:=mType) (Fma e1 e2 e3) exprTypes); try congruence.
+  destruct (isFixedPointB m2) eqn:m2_fixed;
+    destruct (isFixedPointB m3) eqn:m3_fixed;
+    [ | destruct m2, m3; cbn in *; Flover_compute; try congruence
+      | destruct m2, m3; cbn in *; Flover_compute; try congruence| ].
+  - rewrite <- isFixedPoint_isFixedPointB in *.
+    assert (isFixedPointB m1 = true) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      destruct m2, m3; cbn in *; try contradiction.
+      destruct (join3 m1 (F w f) (F w0 f0)) eqn:?; simpl in *; try congruence.
+      unfold join3 in Heqo. simpl in *.
+      destruct (w0 <=? w)%positive; simpl in Heqo;
+        destruct m1; simpl in *; congruence. }
+    rewrite m1_fixed in *; simpl in *;
+    rewrite <- isFixedPoint_isFixedPointB in m1_fixed.
+    simpl in subexpr_ok; Flover_compute.
+    exists n; auto.
+  - rewrite <- isFixedPoint_isFixedPointB_false in *.
+    assert (isFixedPointB m1 = false) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      Flover_compute; try congruence.
+      type_conv.
+      unfold join3 in Heqo.
+      destruct (join m2 m3 0) eqn:?; simpl in *; try congruence.
+      assert (isFixedPointB m = false).
+      { destruct m2, m3; cbn in *; inversion Heqo0; simpl; try congruence.
+        contradiction. }
+      destruct m, m1; cbn in *; congruence. }
+    rewrite m1_fixed in *.
+    simpl in *; Flover_compute.
+    exists 0%nat.
+    intros; contradiction.
+Qed.
+
+Lemma typingFma_join_defined e1 m1 e2 m2 e3 m3 Gamma exprTypes fBits fBit:
+  (isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
+   FloverMap.find (Fma e1 e2 e3) fBits = Some fBit) ->
+  typeCheck (Fma e1 e2 e3) Gamma exprTypes fBits = true ->
+  FloverMap.find e1 exprTypes = Some m1 ->
+  FloverMap.find e2 exprTypes = Some m2 ->
+  FloverMap.find e3 exprTypes = Some m3 ->
+  exists m, join3 m1 m2 m3 fBit = Some m.
+Proof.
+  intros validFixed typing_ok find_e1 find_e2 find_e3.
+  cbn in typing_ok.
+  rewrite find_e1, find_e2, find_e3 in *.
+  destruct (FloverMap.find (elt:=mType) (Fma e1 e2 e3) exprTypes); try congruence.
+  destruct (isFixedPointB m2) eqn:m2_fixed;
+    destruct (isFixedPointB m3) eqn:m3_fixed;
+    [ | destruct m2, m3; cbn in *; Flover_compute; try congruence
+      | destruct m2, m3; cbn in *; Flover_compute; try congruence| ].
+  - rewrite <- isFixedPoint_isFixedPointB in *.
+    assert (isFixedPointB m1 = true) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      destruct m2, m3; cbn in *; try contradiction.
+      destruct (join3 m1 (F w f) (F w0 f0)) eqn:?; simpl in *; try congruence.
+      unfold join3 in Heqo. simpl in *.
+      destruct (w0 <=? w)%positive; simpl in Heqo;
+        destruct m1; simpl in *; congruence. }
+    rewrite m1_fixed in *; simpl in *;
+    rewrite <- isFixedPoint_isFixedPointB in m1_fixed.
+    Flover_compute.
+    specialize (validFixed m1_fixed m2_fixed m3_fixed); exists m0; congruence.
+  - rewrite <- isFixedPoint_isFixedPointB_false in *.
+    assert (isFixedPointB m1 = false) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      Flover_compute; try congruence.
+      type_conv.
+      unfold join3 in Heqo.
+      destruct (join m2 m3 0) eqn:?; simpl in *; try congruence.
+      assert (isFixedPointB m = false).
+      { destruct m2, m3; cbn in *; inversion Heqo0; simpl; try congruence.
+        contradiction. }
+      destruct m, m1; cbn in *; congruence. }
+    rewrite m1_fixed in *.
+    simpl in *; Flover_compute.
+    unfold join3 in *.
+    exists m0. rewrite <- Heqo; unfold join3.
+    erewrite join_float with (f1:=fBit) (f2:=0%nat); eauto.
+    destruct (join m2 m3 0) eqn:?; try auto.
+    assert (isFixedPointB m4 = false).
+    { destruct m2, m3; cbn in *; inversion Heqo0; simpl; try congruence.
+      contradiction. }
+    rewrite <- isFixedPoint_isFixedPointB_false in *.
+    simpl. eapply join_float; eauto.
+Qed.
+
+Lemma typingFma_fixedPoint_case e1 e2 e3 m1 m2 m3 Gamma exprTypes fBits:
+  typeCheck (Fma e1 e2 e3) Gamma exprTypes fBits = true ->
+  FloverMap.find e1 exprTypes = Some m1 ->
+  FloverMap.find e2 exprTypes = Some m2 ->
+  FloverMap.find e3 exprTypes = Some m3 ->
+  (isFixedPointB m1 && isFixedPointB m2 && isFixedPointB m3 = true) \/
+  (isFixedPointB m1 = false /\ isFixedPointB m2 = false /\ isFixedPointB m3 = false).
+Proof.
+  intros check_ok mem1 mem2 mem3.
+  cbn in *.
+  rewrite mem1, mem2, mem3 in check_ok.
+  destruct (FloverMap.find (elt:=mType) (Fma e1 e2 e3) exprTypes) eqn:?;
+           try congruence.
+  destruct (isFixedPointB m2) eqn:m2_fixed;
+    destruct (isFixedPointB m3) eqn:m3_fixed;
+    [ | destruct m2, m3; cbn in *; Flover_compute; try congruence
+      | destruct m2, m3; cbn in *; Flover_compute; try congruence| ].
+  - assert (isFixedPointB m1 = true) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      destruct m2, m3; cbn in *; try congruence.
+      destruct (join3 m1 (F w f) (F w0 f0)) eqn:?; simpl in *; try congruence.
+      unfold join3 in Heqo0. simpl in *.
+      destruct (w0 <=? w)%positive; simpl in Heqo0;
+        destruct m1; simpl in *; congruence. }
+    rewrite m1_fixed in *; simpl in *;
+    rewrite <- isFixedPoint_isFixedPointB in m1_fixed.
+    auto.
+  - assert (isFixedPointB m1 = false) as m1_fixed.
+    { destruct (isFixedPointB m1) eqn:?; try auto.
+      simpl in *.
+      Flover_compute; try congruence.
+      type_conv.
+      unfold join3 in Heqo0.
+      destruct (join m2 m3 0) eqn:?; simpl in *; try congruence.
+      assert (isFixedPointB m = false).
+      { destruct m2, m3; cbn in *; inversion Heqo1; simpl; try congruence. }
+      destruct m, m1; cbn in *; congruence. }
+    rewrite m1_fixed; auto.
 Qed.
 
-Theorem typingSoundnessCmd c Gamma E v m exprTypes:
-  typeCheckCmd c Gamma exprTypes = true ->
-  bstep (toRCmd c) E Gamma v m ->
+Theorem typingSoundnessCmd c Gamma E v m exprTypes fBits:
+  typeCheckCmd c Gamma exprTypes fBits = true ->
+  bstep (toRCmd c) E Gamma (toRBMap fBits) v m ->
   FloverMap.find (getRetExp c) exprTypes = Some m.
 Proof.
   revert Gamma E exprTypes; induction c; cbn; intros * tc bc;
diff --git a/coq/floverParser.v b/coq/floverParser.v
index 3d35b288bcd824e9b24af5005b997fb327a3c678..c7501679dc3f1985f9e0b8879677641ea75b7bb3 100644
--- a/coq/floverParser.v
+++ b/coq/floverParser.v
@@ -106,7 +106,7 @@ match fuel with
                                |DCONST 32 :: ts' => DTYPE M32 :: ts'
                                |DCONST 64 :: ts' => DTYPE M64 :: ts'
                                |DFIXED :: DCONST w :: DCONST f :: ts' =>
-                                DTYPE (F (Pos.of_nat w) (Pos.of_nat f)) :: ts'
+                                DTYPE (F (Pos.of_nat w) f) :: ts'
                             (* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
                             (* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
                                | _ => []
@@ -504,11 +504,11 @@ Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
   | S n' =>
     match dParse input fuel with
     | Some ((dCmd, P, A, Gamma), []) =>
-      if CertificateCheckerCmd dCmd A P Gamma
+      if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty nat)
       then "True\n"
       else "False\n"
     | Some ((dCmd, P, A, Gamma), residual) =>
-      if CertificateCheckerCmd dCmd A P Gamma
+      if CertificateCheckerCmd dCmd A P Gamma (FloverMap.empty nat)
       then check_rec residual n' fuel
       else "False\n"
     | None => "parse failure\n"
@@ -524,7 +524,7 @@ Fixpoint str_length s :=
 
 Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
   match n with
-  |S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
+  |S n' => CertificateCheckerCmd f A P Gamma (FloverMap.empty nat) && (check f P A Gamma n')
   |_ => true
   end.
 
diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v
index 9f8e37c52da0157ab270441719339f2a7da8032f..01f81480ff0a2cb85c121c6837d36627e5cc6a57 100644
--- a/coq/ssaPrgs.v
+++ b/coq/ssaPrgs.v
@@ -178,10 +178,10 @@ Proof.
     + hnf; intros; split; auto.
 Qed.
 
-Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars:
+Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars fBits:
   ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
   NatSet.In y inVars ->
-  eval_expr E defVars (toREval (toRExp e)) v REAL ->
+  eval_expr E defVars fBits (toREval (toRExp e)) v REAL ->
   forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
 Proof.
   intros ssa_let y_free eval_e.