Draft structure for new type validator/type system, incorporating Fixed-point types properly

coq/CertificateChecker.v

@@ -7,20 +7,21 @@
 From Flover
      Require Import Infra.RealSimps Infra.RationalSimps Infra.RealRationalProps
      Infra.Ltacs RealRangeArith RealRangeValidator RoundoffErrorValidator
-     Environments Typing FPRangeValidator ExpressionAbbrevs Commands.
+     Environments TypeValidator FPRangeValidator ExpressionAbbrevs Commands.
 
-Require Export Infra.ExpressionAbbrevs Flover.Commands Coq.QArith.QArith.
+Require Export ExpressionSemantics Flover.Commands Coq.QArith.QArith.
 
 (** Certificate checking function **)
 Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
-           (P:precond) (defVars:nat -> option mType) (fBits:FloverMap.t N):=
-  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
-    else false
-  else false.
+           (P:precond) (defVars:FloverMap.t  mType):=
+  let tMap := (getValidMap defVars e (FloverMap.empty mType)) in
+  match tMap with
+  |Succes tMap =>
+   if RangeValidator e absenv P NatSet.empty && FPRangeValidator e absenv tMap NatSet.empty
+   then RoundoffErrorValidator e tMap absenv NatSet.empty
+   else false
+  | _ => false
+  end.
 
 (**
    Soundness proof for the certificate checker.
@@ -28,22 +29,22 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
    the real valued execution respects the precondition.
 **)
 Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
-        defVars fBits:
+        defVars:
   forall (E1 E2:env),
-    approxEnv E1 defVars absenv (usedVars e) NatSet.empty E2 ->
+    approxEnv E1 (toRTMap defVars) absenv (usedVars e) NatSet.empty E2 ->
     (forall v, NatSet.In v (Expressions.usedVars e) ->
           exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     (forall v, NatSet.In v  (usedVars e) ->
           exists m : mType,
-            defVars v = Some m) ->
-    CertificateChecker e absenv P defVars fBits = true ->
-    exists iv err vR vF m,
+            FloverMap.find (Var Q v) defVars = Some m) ->
+    CertificateChecker e absenv P defVars = true ->
+    exists Gamma iv err vR vF m,
       FloverMap.find e absenv = Some (iv, err) /\
-      eval_expr E1 (toRMap defVars) (toRBMap fBits) (toREval (toRExp e)) vR REAL /\
-      eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m /\
+      eval_expr E1 (toRMap Gamma) (toRExp e) vR REAL /\
+      eval_expr E2 Gamma (toRExp e) vF m /\
       (forall vF m,
-          eval_expr E2 defVars (toRBMap fBits) (toRExp e) vF m ->
+          eval_expr E2 Gamma (toRExp e) vF m ->
           (Rabs (vR - vF) <= Q2R err))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
@@ -52,26 +53,25 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P
 Proof.
   intros * approxE1E2 P_valid types_defined certificate_valid.
   unfold CertificateChecker in certificate_valid.
+  destruct (getValidMap defVars e (FloverMap.empty mType)); try congruence.
   rewrite <- andb_lazy_alt in certificate_valid.
   andb_to_prop certificate_valid.
+  clear R1.
   pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
   hnf in union_empty.
   assert (dVars_range_valid NatSet.empty E1 absenv).
   { unfold dVars_range_valid.
     intros; set_tac. }
-  assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
+  (* assert (affine_dVars_range_valid NatSet.empty E1 absenv 1 (FloverMap.empty _) (fun _ => None))
     as affine_dvars_valid.
   { unfold affine_dVars_range_valid.
-    intros; set_tac. }
+    intros; set_tac. } *)
   assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
   { hnf; intros a in_empty.
     set_tac. }
-  assert (vars_typed (usedVars e ∪ NatSet.empty) defVars).
-  { 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 (toRBMap fBits)) as valid_e.
-  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=defVars) (E:=E1));
+  assert (validRanges e absenv E1 (toRTMap defVars)) as valid_e.
+  { eapply (RangeValidator_sound e (dVars:=NatSet.empty) (A:=absenv) (P:=P) (Gamma:=toRTMap defVars) (E:=E1));
       auto. }
   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]]]]].

coq/Commands.v

@@ -2,7 +2,7 @@
  Formalization of the Abstract Syntax Tree of a subset used in the Flover framework
  **)
 Require Import Coq.Reals.Reals Coq.QArith.QArith.
-Require Import Flover.Expressions.
+Require Export Flover.ExpressionSemantics.
 Require Export Flover.Infra.ExpressionAbbrevs Flover.Infra.NatSet.
 
 (**
@@ -20,7 +20,6 @@ Fixpoint getRetExp (V:Type) (f:cmd V) :=
   | Ret e => e
   end.
 
-
 Fixpoint toRCmd (f:cmd Q) :=
   match f with
   |Let m x e g => Let m x (toRExp e) (toRCmd g)
@@ -49,14 +48,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) -> (expr R -> option N) -> 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.
+Inductive bstep : cmd R -> env -> (expr R -> 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 (Var R 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.
 
 (**
   The free variables of a command are all used variables of exprressions
@@ -88,14 +87,14 @@ Fixpoint liveVars V (f:cmd V) :NatSet.t :=
   end.
 
 Lemma bstep_eq_env f:
-  forall E1 E2 Gamma fBits v m,
+  forall E1 E2 Gamma v m,
   (forall x, E1 x = E2 x) ->
-  bstep f E1 Gamma fBits v m ->
-  bstep f E2 Gamma fBits v m.
+  bstep f E1 Gamma v m ->
+  bstep f E2 Gamma v m.
 Proof.
   induction f; intros * eq_envs bstep_E1;
     inversion bstep_E1; subst; simpl in *.
-  - eapply eval_eq_env in H8; eauto. eapply let_b; eauto.
+  - eapply eval_eq_env in H7; eauto. eapply let_b; eauto.
      eapply IHf. instantiate (1:=(updEnv n v0 E1)).
      + intros; unfold updEnv.
        destruct (x=? n); auto.

coq/Environments.v

@@ -16,7 +16,7 @@ It is necessary to have this relation, since two evaluations of the very same
 exprression may yield different values for different machine epsilons
 (or environments that already only approximate each other)
  **)
-Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
+Inductive approxEnv : env -> (expr R -> option mType) -> analysisResult -> NatSet.t
                       -> NatSet.t -> env -> Prop :=
 |approxRefl defVars A:
    approxEnv emptyEnv defVars A NatSet.empty NatSet.empty emptyEnv
@@ -25,7 +25,7 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
    (Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
    approxEnv (updEnv x v1 E1)
-             (updDefVars x m defVars) A (NatSet.add x fVars) dVars
+             (updDefVars (Var R x) m defVars) A (NatSet.add x fVars) dVars
              (updEnv x v2 E2)
 |approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars m iv err:
    approxEnv E1 defVars A fVars dVars E2 ->
@@ -33,12 +33,12 @@ Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t
    (Rabs (v1 - v2) <= Q2R err)%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
    approxEnv (updEnv x v1 E1)
-             (updDefVars x m defVars) A fVars (NatSet.add x dVars)
+             (updDefVars (Var R x) m defVars) A fVars (NatSet.add x dVars)
              (updEnv x v2 E2).
 
 Section RelationProperties.
 
-  Variable (x:nat) (v:R) (E1 E2:env) (Gamma:nat -> option mType)
+  Variable (x:nat) (v:R) (E1 E2:env) (Gamma:expr R -> option mType)
            (A:analysisResult) (fVars dVars: NatSet.t).
 
   Hypothesis approxEnvs: approxEnv E1 Gamma A fVars dVars E2.
@@ -76,7 +76,7 @@ Section RelationProperties.
     E1 x = Some v ->
     E2 x = Some v2 ->
     NatSet.In x fVars ->
-    Gamma x = Some m ->
+    Gamma (Var R x) = Some m ->
     (Rabs (v - v2) <= computeErrorR v m)%R.
   Proof.
     induction approxEnvs;
@@ -87,30 +87,40 @@ Section RelationProperties.
       + unfold updEnv in *;
           rewrite Nat.eqb_refl in *; simpl in *.
         unfold updDefVars in x_typed.
-        rewrite Nat.eqb_refl in x_typed.
+        cbn in x_typed.
+        rewrite Nat.compare_refl in x_typed.
         inversion x_typed; subst.
         inversion E1_def; inversion E2_def; subst; auto.
       + unfold updEnv in *; simpl in *.
         rewrite <- Nat.eqb_neq in x_neq.
         rewrite x_neq in *; simpl in *.
-        unfold updDefVars in x_typed; rewrite x_neq in x_typed.
-        apply IHa; auto.
+        unfold updDefVars in x_typed.
+        cbn in x_typed.
+        apply Nat.eqb_neq in x_neq.
+        destruct (x ?= x0)%nat eqn:?.
+        * apply Nat.compare_eq in Heqc; subst; congruence.
+        * apply IHa; auto.
+        * apply IHa; auto.
     - assert (x =? x0 = false) as x_x0_neq.
       { rewrite Nat.eqb_neq; hnf; intros; subst.
         set_tac.
         apply H1.
         set_tac. }
       unfold updEnv in *; rewrite x_x0_neq in *.
-      apply IHa; auto.
-      unfold updDefVars in x_typed;
-        rewrite x_x0_neq in x_typed; auto.
+      unfold updDefVars in x_typed.
+      cbn in x_typed.
+      apply Nat.eqb_neq in x_x0_neq.
+      destruct (x ?= x0)%nat eqn:?.
+      * apply Nat.compare_eq in Heqc; subst; congruence.
+      * apply IHa; auto.
+      * apply IHa; auto.
   Qed.
 
   Lemma approxEnv_dVar_bounded v2 m iv e:
     E1 x = Some v ->
     E2 x = Some v2 ->
     NatSet.In x dVars ->
-    Gamma x = Some m ->
+    Gamma (Var R x) = Some m ->
     FloverMap.find (Var Q x) A = Some (iv, e) ->
     (Rabs (v - v2) <= Q2R e)%R.
   Proof.
@@ -123,8 +133,12 @@ Section RelationProperties.
         apply H0; set_tac.
       }
       unfold updEnv in *; rewrite x_x0_neq in *.
-      unfold updDefVars in x_typed; rewrite x_x0_neq in x_typed.
-      apply IHa; auto.
+      unfold updDefVars in x_typed; cbn in x_typed.
+      apply Nat.eqb_neq in x_x0_neq.
+      destruct (x ?= x0)%nat eqn:?.
+      * apply Nat.compare_eq in Heqc; subst; congruence.
+      * apply IHa; auto.
+      * apply IHa; auto.
     - set_tac.
       destruct x_def as [x_x0 | [x_neq x_def]]; subst.
       + unfold updEnv in *;
@@ -134,8 +148,12 @@ Section RelationProperties.
       + unfold updEnv in *; simpl in *.
         rewrite <- Nat.eqb_neq in x_neq.
         rewrite x_neq in *; simpl in *.
-        unfold updDefVars in x_typed; rewrite x_neq in x_typed.
-        apply IHa; auto.
+        unfold updDefVars in x_typed; cbn in x_typed.
+        apply Nat.eqb_neq in x_neq.
+        destruct (x ?= x0)%nat eqn:?.
+        * apply Nat.compare_eq in Heqc; subst; congruence.
+        * apply IHa; auto.
+        * apply IHa; auto.
   Qed.
 
 End RelationProperties.
\ No newline at end of file

coq/FPRangeValidator.v

 From Flover
-     Require Import Expressions Commands Environments ssaPrgs Typing
+     Require Import Expressions Commands Environments ssaPrgs TypeValidator
      IntervalValidation ErrorValidation Infra.Ltacs Infra.RealRationalProps.
 
 Fixpoint FPRangeValidator (e:expr Q) (A:analysisResult) typeMap dVars {struct e} : bool :=
@@ -69,29 +69,28 @@ 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 fBits,
-  approxEnv E1 Gamma A fVars dVars E2 ->
-  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 ->
+  forall (e:expr Q) E1 E2 Gamma v m A fVars dVars,
+  approxEnv E1 (toRTMap Gamma) A fVars dVars E2 ->
+  eval_expr E2 (toRTMap Gamma) (toRExp e) v m ->
+  validTypes e Gamma ->
+  validRanges e A E1 (toRTMap Gamma) ->
+  validErrorbound e Gamma A dVars = true ->
+  FPRangeValidator e A Gamma 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) ->
+  (forall v, NatSet.In v dVars ->
+        exists vF m, E2 v = Some vF /\
+                FloverMap.find (Var Q v) Gamma = Some m /\
+                validFloatValue vF m) ->
   validFloatValue v m.
 Proof.
   intros *.
   unfold FPRangeValidator.
   intros.
-  assert (FloverMap.find e tMap = Some m)
-    as type_e
-      by (eapply typingSoundnessExp; eauto).
+  pose proof (validTypes_single _ _ H1) as validT.
+  destruct validT as [mE [type_e ?]].
+  assert (mE = m) by admit; subst.
   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.
@@ -109,7 +108,7 @@ Proof.
       rewrite type_e in *; cbn in *.
   - Flover_compute.
     destruct (n mem dVars) eqn:?.
-    + set_tac. edestruct H7 as [? [? [? [? ?]]]]; eauto.
+    + set_tac. edestruct H6 as [? [? [? [? ?]]]]; eauto.
       rewrite H10 in type_e; inversion type_e; subst.
       inversion H0; subst.
       rewrite H14 in H3; inversion H3; subst.
@@ -120,103 +119,68 @@ Proof.
     prove_fprangeval m v L1 R.
   - Flover_compute; destruct u; Flover_compute; try congruence.
     type_conv; subst.
-    prove_fprangeval m0 v L1 R.
+    prove_fprangeval m 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. }
+    assert (FloverMap.find e1 Gamma = Some m1) as type_m1 by admit.
+    assert (FloverMap.find e2 Gamma = Some m2) as type_m2 by admit.
     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.
+    Flover_compute; try congruence.
+    prove_fprangeval m (perturb (evalBinop b v1 v2) m 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. }
+    assert (FloverMap.find e1 Gamma = Some m1) as type_m1 by admit.
+    assert (FloverMap.find e2 Gamma = Some m2) as type_m2 by admit.
+    assert (FloverMap.find e3 Gamma = Some m3) as type_m3 by admit.
     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.
+    prove_fprangeval m (perturb (evalFma v1 v2 v3) m delta) L1 R.
   - Flover_compute; try congruence.
     type_conv; subst.
     prove_fprangeval m v L1 R.
-Qed.
+Admitted.
 
 Lemma FPRangeValidatorCmd_sound (f:cmd Q):
-  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars fBits,
+  forall E1 E2 Gamma v vR m A tMap fVars dVars outVars,
   approxEnv E1 Gamma A fVars dVars E2 ->
   ssa f (NatSet.union fVars dVars) outVars ->
-  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) ->
+  bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m ->
+  bstep (toRCmd f) E2 Gamma v m ->
+  validRangesCmd f A E1 Gamma ->
   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) ->
   validFloatValue v m.
 Proof.
+  admit.
+  (*
   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.
-      - assert (FloverMap.find e tMap = Some m)
-          by(eapply typingSoundnessExp; eauto).
-        match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
+      - assert (FloverMap.find e tMap = Some m)  by admit.
+        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.
+        destruct H3 as [[valid_e valid_rec] valid_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.
         edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars)
-                                         (dVars := dVars) (A:=A) tMap
+                                         (dVars := dVars) (A:=A)
                                          (nR:=v0) (err:=err_e) (elo:=fst iv_e) (ehi:=snd iv_e))
           as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+        + admit.
+        + admit.
         + set_tac. split; try auto.
           split; try auto.
           hnf; intros; subst; set_tac.
+        + admit.
         + destruct iv_e; 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)
@@ -271,5 +235,5 @@ Proof.
             { apply H9.
               rewrite NatSet.add_spec in H4; destruct H4;
                 auto; subst; congruence. }
-  - destruct H4. eapply FPRangeValidator_sound; eauto.
-Qed.
+                               - destruct H4. eapply FPRangeValidator_sound; eauto. *)
+Admitted.
\ No newline at end of file

coq/Infra/ExpressionAbbrevs.v

@@ -208,13 +208,20 @@ Proof.
   congruence.
 Qed.
 
-Definition toRBMap (bMap:FloverMap.t N) : expr R -> option N :=
-  let elements := FloverMap.elements (elt:=N) bMap in
+Definition toRTMap (tMap:FloverMap.t mType) : expr R -> option mType :=
+  let elements := FloverMap.elements (elt:=mType) tMap 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).
 
+Definition updDefVars  (e:expr R) (m:mType) Gamma :=
+  fun eNew =>
+    match R_orderedExps.compare eNew e with
+    |Eq => Some m
+    |_ => Gamma eNew
+    end.
+
 Lemma findA_find A B (f:A -> bool) (l:list (A * B)) r:
   findA f l = Some r ->
   exists k,
@@ -241,22 +248,22 @@ Proof.
     apply IHl; auto.
 Qed.
 
-Lemma toRBMap_some bMap e b:
-  FloverMap.find e bMap = Some b ->
-  toRBMap bMap (toRExp e) = Some b.
+Lemma toRTMap_some tMap e m:
+  FloverMap.find e tMap = Some m ->
+  toRTMap tMap (toRExp e) = Some m.
 Proof.
   intros find_Q.
   rewrite  FloverMapFacts.P.F.elements_o in find_Q.
-  unfold toRBMap.
+  unfold toRTMap.
   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 * N =>
+      (fun p : expr Q * mType =>
        match R_orderedExps.compare (toRExp e) (toRExp (fst p)) with
        | Eq => true
        | _ => false
-       end) (FloverMap.elements (elt:=N) bMap) = Some (key, b)).
+       end) (FloverMap.elements (elt:=mType) tMap) = Some (key, m)).
   - 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).

coq/Infra/Ltacs.v

@@ -90,9 +90,9 @@ Ltac remove_matches := rewrite optionBind_eq in *.
 
 Ltac remove_matches_asm := rewrite optionBind_eq in * |- .
 
-Ltac remove_conds := rewrite <- andb_lazy_alt, optionBind_cond in *.
+Ltac remove_conds := rewrite <- andb_lazy_alt in *.
 
-Ltac remove_conds_asm := rewrite <- andb_lazy_alt, optionBind_cond in * |- .
+Ltac remove_conds_asm := rewrite <- andb_lazy_alt in * |- .
 
 Ltac match_factorize_asm :=
   match goal with

coq/Infra/MachineType.v

@@ -18,9 +18,9 @@ From Flover
    like Flocq, where f:positive specifies the fraction size and w: the width of
    the base field.
  **)
-Inductive mType: Type := REAL | M16 | M32 | M64
-                         | F (w:positive) (f:N). (*| M128 | M256*)
-
+Inductive mType: Type := REAL (* real valued computations *)
+                       | M16 | M32 | M64 (* floating-point precisions *)
+                       | F (w:positive) (f:N). (* fixed-point precisions *)
 Definition isFixedPoint m :Prop :=
   match m with
   |F _ _ => True
@@ -337,52 +337,43 @@ Qed.
   in which evaluation has to be performed, e.g. addition of 32 and 64 bit floats
   has to happen in 64 bits
 **)
-Definition join (m1:mType) (m2:mType) (fracBits:N) :option mType:=
+Definition join_fl (m1:mType) (m2:mType) :option mType :=
   match m1, m2 with
-  | F w1 f1, F w2 f2 =>
-    if (w2 <=? w1)%positive
-    then Some (F w1 fracBits)
-    else Some (F w2 fracBits)
-  | F _ _, _ => None
-  | _ , F _ _ => None
-  | _ , _ => if (morePrecise m1 m2) then Some m1 else Some m2
+  |F _ _, F _ _ => None
+  | _, _ => if (morePrecise m1 m2) then Some m1 else Some m2
   end.
 
-Definition join3 (m1:mType) (m2:mType) (m3:mType) (fBits:N):=
-  olet msub := (join m2 m3 fBits) in
-    join m1 msub fBits.
+Definition join_fl3 (m1:mType) (m2:mType) (m3:mType) :=
+  olet msub := join_fl m2 m3 in
+    join_fl m1 msub.
 
-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.