making IEEE_connection compile

coq/FPRangeValidator.v

@@ -153,7 +153,7 @@ Proof.
     prove_fprangeval m v L1 R.
   - inversion H1; subst.
     destruct H2 as [mE [find_mE [[validt_e1 [validt_e2 [m_e2 [find_e1 [find_var [find_m2 join_valid]]]]]] _ ]]].
-    assert (m_e2 = m) by (eapply validTypes_exec in find_m2; eauto).
+    assert (m_e2 = m2) by (eapply validTypes_exec in find_m2; eauto).
     subst.
     Flover_compute; try congruence.
     prove_fprangeval m v L1 R.
@@ -273,5 +273,5 @@ Proof.
           rewrite NatSet.add_spec in H5; destruct H5;
             auto; subst; congruence. }
   - destruct H5. destruct H4. destruct H6. eapply FPRangeValidator_sound; eauto.
-Admitted.
+Abort.
 *)

coq/IEEE_connection.v

@@ -5,7 +5,7 @@ From Coq
 From Flover
      Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation
      ErrorAnalysis CertificateChecker FPRangeValidator RoundoffErrorValidator
-     Environments Infra.RealRationalProps Commands Infra.Ltacs.
+     Environments Infra.RealRationalProps Infra.Ltacs.
 
 From Flocq
      Require Import Appli.Fappli_IEEE_bits Appli.Fappli_IEEE Core.Fcore_Raux
@@ -48,9 +48,13 @@ Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):
       (* | Some f1, Some f2, Some f3 => Some (b64_plus dmode f1 (b64_mult dmode f2 f3)) *)
       | _, _, _ => None
     end
+  | Let m x e1 e2 =>
+    olet res :=  eval_expr_float e1 E in
+        eval_expr_float e2 (updFlEnv x res E)
   | _ => None
   end.
 
+(*
 Fixpoint bstep_float f E :option fl64 :=
   match f with
   | Let m x e g =>
@@ -58,6 +62,7 @@ Fixpoint bstep_float f E :option fl64 :=
         bstep_float g (updFlEnv x res E)
   | Ret e => eval_expr_float e E
   end.
+*)
 
 Definition isValid e :=
   plet v := e in
@@ -102,8 +107,15 @@ Fixpoint eval_expr_valid (e:expr fl64) E :=
                               True)
                 True)
   | Downcast m e => eval_expr_valid e E
+  | Let m x e1 e2 =>
+    eval_expr_valid e1 E /\
+    (optionBind (eval_expr_float e1 E)
+                (fun v_e => eval_expr_valid e2 (updFlEnv x v_e E))
+                True)
+  | Cond e1 e2 e3 => False
   end.
 
+(*
 Fixpoint bstep_valid f E :=
   match f with
   | Let m x e g =>
@@ -113,6 +125,7 @@ Fixpoint bstep_valid f E :=
                 True)
   | Ret e => eval_expr_valid e E
   end.
+*)
 
 Definition bpowQ (r:radix) (e: Z) :=
   match e with
@@ -181,13 +194,17 @@ Fixpoint B2Qexpr (e: expr fl64) :=
   | Binop b e1 e2 => Binop b (B2Qexpr e1) (B2Qexpr e2)
   | Fma e1 e2 e3 => Fma (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)
   | Downcast m e => Downcast m (B2Qexpr e)
+  | Let m x e1 e2 => Let m x (B2Qexpr e1) (B2Qexpr e2)
+  | Cond e1 e2 e3 => Cond (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3)
   end.
 
+(*
 Fixpoint B2Qcmd (f:cmd fl64) :=
   match f with
   | Let m x e g => Let m x (B2Qexpr e) (B2Qcmd g)
   | Ret e => Ret (B2Qexpr e)
   end.
+*)
 
 Definition toREnv (E: nat -> option fl64) (x:nat):option R :=
   match E x with
@@ -208,13 +225,17 @@ Fixpoint is64BitEval (V:Type) (e:expr V) :=
   | Binop b e1 e2 => is64BitEval e1 /\ is64BitEval e2
   | Fma e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
   | Downcast m e => m = M64 /\ is64BitEval e
+  | Let m x e g => is64BitEval e /\ m = M64 /\ is64BitEval g
+  | Cond e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3
   end.
 
+(*
 Fixpoint is64BitBstep (V:Type) (f:cmd V) :=
   match f with
   | Let m x e g => is64BitEval e /\ m = M64 /\ is64BitBstep g
   | Ret e => is64BitEval e
   end.
+*)
 
 Fixpoint noDowncast (V:Type) (e:expr V) :=
   match e with
@@ -224,13 +245,17 @@ Fixpoint noDowncast (V:Type) (e:expr V) :=
   | Binop b e1 e2 => noDowncast e1 /\ noDowncast e2
   | Fma e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
   | Downcast m e => False
+  | Let m x e1 e2 => noDowncast e1 /\ noDowncast e2
+  | Cond e1 e2 e3 => noDowncast e1 /\ noDowncast e2 /\ noDowncast e3
   end.
 
+(*
 Fixpoint noDowncastFun (V:Type) (f:cmd V) :=
   match f with
   | Let m x e g => noDowncast e /\ noDowncastFun g
   | Ret e => noDowncast e
   end.
+*)
 
 Opaque mTypeToQ.
 
@@ -297,6 +322,7 @@ Proof.
     erewrite <- Gamma_64Bit; eauto.
 Qed.
 
+(*
 Lemma typing_cmd_64_bit f:
   forall Gamma,
     is64BitEnv Gamma ->
@@ -308,6 +334,7 @@ Proof.
     eapply IHf; eauto.
   - destruct valid_f; simpl in *; eapply typing_expr_64_bit; eauto.
 Qed.
+*)
 
 Lemma round_0_zero:
   (Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
@@ -410,7 +437,7 @@ Lemma eval_expr_gives_IEEE (e:expr fl64) :
     validErrorBounds (B2Qexpr e) E1 E2_real A Gamma DeltaMap ->
     FPRangeValidator (B2Qexpr e) A Gamma dVars = true ->
     eval_expr (toREnv E2) (toRExpMap Gamma) DeltaMap (toRExp (B2Qexpr e)) vR M64 ->
-    NatSet.Subset ((usedVars (B2Qexpr e)) -- dVars) fVars ->
+    NatSet.Subset ((freeVars (B2Qexpr e)) -- dVars) fVars ->
     is64BitEval (B2Qexpr e) ->
     is64BitEnv Gamma ->
     noDowncast (B2Qexpr e) ->
@@ -436,6 +463,7 @@ Proof.
      unfold optionBind;
      intros eval_IEEE_valid_e.
      Transparent validTypes.
+     (*
      all:validTypes_split.
      - unfold toREnv in *.
        destruct (E2 n) eqn:HE2; try congruence.
@@ -818,8 +846,10 @@ Proof.
     rewrite eval_float_e1, eval_float_e2, eval_float_e3 in H7.
     contradiction H7.
   - inversion noDowncast_e.
+      *)
 Admitted.
 
+(*
 Lemma bstep_gives_IEEE (f:cmd fl64) :
   forall E1 E2 E2_real Gamma DeltaMap vR vF A fVars dVars outVars,
     (forall (e' : expr R) (m' : mType),
@@ -973,7 +1003,8 @@ Proof.
     edestruct (eval_expr_gives_IEEE) as [v_res [eval_float eval_e]]; eauto.
     exists v_res; split; try auto.
     apply ret_b; auto.
-Admitted.
+Abort.
+*)
 
 Ltac find_cases :=
   rewrite map_find_add;
@@ -1107,8 +1138,58 @@ Proof.
     + Flover_compute; inversion getMap_succeeds; subst.
       find_cases; try (eapply IHe with (akk:=akk); eauto).
       congruence.
+  - unfold addMono in *. Flover_compute.
+    + destruct (mTypeEq m m1) eqn:?; try congruence.
+      type_conv; subst.
+      destruct is64Bit_e as (? & ? & ?); subst.
+      eapply IHe2 with (akk:=t0); eauto.
+      inversion Heqr0; subst.
+      intros *.
+      find_cases; try (eapply IHe1 with (akk:=akk); now eauto).
+      congruence.
+    + destruct is64Bit_e as (? & ? & ?); subst.
+      destruct (mTypeEq M64 m1) eqn:?; congruence.
+  - destruct (getValidMap defVars e1 akk) eqn:?;
+             simpl in *; try congruence.
+    destruct (getValidMap defVars e2 t) eqn:?;
+             simpl in *; try congruence.
+    destruct (getValidMap defVars e3 t0) eqn:?;
+             simpl in *; try congruence.
+    destruct (FloverMap.find e1 t1) eqn:?;
+             try congruence.
+    destruct (FloverMap.find e2 t1) eqn:?;
+             try congruence.
+    destruct (FloverMap.find e3 t1) eqn:?;
+             try congruence.
+    destruct is64Bit_e as (? & ? & ?).
+    assert (forall e m, FloverMap.find e t = Some m -> m = M64)
+      as valid_t
+           by (eapply IHe1 with (akk:=akk); eauto).
+    assert (forall e m, FloverMap.find e t0 = Some m -> m = M64)
+      as valid_t0
+           by (eapply IHe2 with (akk:=t); eauto).
+    assert (forall e m, FloverMap.find e t1 = Some m -> m = M64)
+      as valid_t1
+           by (eapply IHe3 with (akk:=t0); eauto).
+    clear IHe1 IHe2 IHe3.
+    assert (m0 = M64 /\ m1 = M64 /\ m2 = M64)
+           as (? & ? & ?)
+             by (repeat split; eapply valid_t1; eauto).
+    subst; cbn in *.
+    unfold isMonotone, addMono in *.
+    destruct (FloverMap.find (Cond e1 e2 e3) defVars) eqn:?.
+    + destruct (mTypeEq m0 M64) eqn:?; try congruence; type_conv; subst.
+      Flover_compute.
+      inversion getMap_succeeds; subst.
+      find_cases; try (eapply valid_t1; now eauto).
+      congruence.
+    + Flover_compute.
+      inversion getMap_succeeds; subst.
+      find_cases; try (eapply valid_t1; now eauto).
+      congruence.
 Qed.
 
+(*
 Lemma getValidMapCmd_preserving f:
   forall defVars akk res,
     (forall e m, FloverMap.find e akk = Some m -> m = M64) ->
@@ -1131,6 +1212,7 @@ Proof.
     destruct (mTypeEq M64 m1) eqn:?; congruence.
   - eapply getValidMap_preserving with (akk:=akk); eauto.
 Qed.
+*)
 
 Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
   (forall (e' : expr R) (m' : mType),
@@ -1143,7 +1225,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
   eval_precond E1 P ->
   CertificateChecker (B2Qexpr e) A P qMap defVars = true ->
   exists Gamma, (* m, currently = M64 *)
-    approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
+    approxEnv E1 Gamma A (freeVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
     exists iv err vR vF,
     FloverMap.find (B2Qexpr e) A = Some (iv, err) /\
     eval_expr E1 (toRTMap Gamma) DeltaMapR (toREval (toRExp (B2Qexpr e))) vR REAL /\
@@ -1163,31 +1245,44 @@ Proof.
   assert (validTypes (B2Qexpr e) Gamma).
   { eapply getValidMap_top_correct; eauto.
     intros. cbn in *; congruence. }
-  rewrite <- andb_lazy_alt in certificate_valid.
+  (* rewrite <- andb_lazy_alt in certificate_valid. *)
   andb_to_prop certificate_valid.
-  pose proof (NatSetProps.empty_union_2 (Expressions.usedVars e) NatSet.empty_spec) as union_empty.
+  pose proof (NatSetProps.empty_union_2 (freeVars e) NatSet.empty_spec) as union_empty.
   hnf in union_empty.
   assert (dVars_range_valid NatSet.empty E1 A).
   { unfold dVars_range_valid.
     intros; set_tac. }
+  (*
   assert (AffineValidation.affine_dVars_range_valid NatSet.empty E1 A 1 (FloverMap.empty _)
                                                     (fun _ => None)) as affine_dvars_valid.
   { unfold AffineValidation.affine_dVars_range_valid.
     intros; set_tac. }
-  assert (NatSet.Subset (usedVars (B2Qexpr e) -- NatSet.empty) (Expressions.usedVars (B2Qexpr e))).
+*)
+  assert (NatSet.Subset (freeVars (B2Qexpr e) -- NatSet.empty) (freeVars (B2Qexpr e))).
   { hnf; intros a in_empty.
     set_tac. }
+  pose proof (validSSA_checks_freeVars _ _ L) as sub.
   rename R0 into validFPRanges.
+  destruct (validSSA_sound (B2Qexpr e) (preVars P)) as [outVars ssa_e]; auto.
+  assert (validSSA (B2Qexpr e) (freeVars (B2Qexpr e)) = true) as ssa_valid
+      by (eapply validSSA_downward_closed; eauto using NatSetProps.subset_refl).
+  destruct (validSSA_sound (B2Qexpr e) (freeVars (B2Qexpr e))) as [outVars2 ssa_e2]; auto.
   assert (validRanges (B2Qexpr e) A E1 (toRTMap (toRExpMap Gamma))) as valid_e.
-  { eapply (RealRangeValidator.RangeValidator_sound (B2Qexpr e) (dVars:=NatSet.empty) (A:=A) (P:=P) (Qmap:=qMap));
-      auto. }
+  { eapply (RealRangeValidator.RangeValidator_sound (dVars:=NatSet.empty) (A:=A) (P:=P) (fVars:=preVars P)
+                                                    (Qmap:=qMap));
+      eauto using NatSetProps.subset_refl; set_tac.
+    clear ssa_e2.
+    eapply ssa_equal_set; eauto.
+    intros n. split; set_tac. intros [?|?]; auto. set_tac. }
   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].
   exists (toRExpMap Gamma); intros approxE1E2.
   pose proof RoundoffErrorValidator_sound as Hsound.
-  eapply validErrorBounds_single in Hsound; eauto.
-  2: intros v' Hin; set_tac.
+  assert (ssa (B2Qexpr e) (freeVars (B2Qexpr e) ∪ NatSet.empty) outVars2).
+  { eapply ssa_equal_set; eauto. split; set_tac. intros [?|?]; auto. set_tac. }
+  eapply validErrorBounds_single in Hsound; try exact approxE1E2; eauto.
+  (* 2: intros v' Hin; set_tac. *)
   specialize Hsound as ((v__FP & m__FP & Hbstepex) & Hsound).
   assert (FloverMap.find (B2Qexpr e) Gamma = Some M64).
   { eapply typing_expr_64_bit; eauto. }
@@ -1195,12 +1290,13 @@ Proof.
   { eapply validTypes_exec; try exact Hbstepex; eauto. }
   subst.
   edestruct eval_expr_gives_IEEE; eauto.
-  - eapply RoundoffErrorValidator_sound; eauto. intros ? ?; set_tac.
+  - eapply RoundoffErrorValidator_sound; try exact approxE1E2; eauto.
   - intros ? ?; set_tac.
   - exists (elo, ehi), err_e, vR, x.
     intuition. eapply Hsound; eauto.
 Qed.
 
+(*
 Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
         defVars E1 E2 DeltaMap:
     (forall (e' : expr R) (m' : mType),
@@ -1278,3 +1374,4 @@ Proof.
   - exists (f_lo, f_hi), err, vR, x, M64.
     intuition.
 Qed.
+*)