Fix ssa proofs, in pair programming session with Raphael, by removing the toREValEnv function

coq/Infra/Ltacs.v

@@ -2,7 +2,6 @@
 Require Import Coq.Bool.Bool Coq.Reals.Reals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.
 
-
 Ltac iv_assert iv name:=
   assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
 

coq/Infra/MachineType.v

@@ -24,7 +24,7 @@ Proof.
   intro e.
   case_eq e; intro; simpl inj_eps_Q; apply Qle_bool_iff; auto.
 Qed.
-  
+
 (* Definition mTypeEqBool (m1:mType) (m2:mType) := *)
 (*   Qeq_bool (meps m1) (meps m2). *)
 
@@ -60,7 +60,7 @@ Lemma EquivEqBoolEq (m1:mType) (m2:mType):
 Proof.
   split; intros; case_eq m1; intros; case_eq m2; intros; auto; rewrite H0 in H; rewrite H1 in H; cbv in H; inversion H; auto.
 Qed.
-  
+
 (*   Definition mTypeEq: relation mType := *)
 (*   fun m1 m2 => Qeq (meps m1) (meps m2). *)
 
@@ -90,6 +90,27 @@ Definition isMorePrecise (m1:mType) (m2:mType) :=
   else
     Qle_bool (meps m1) (meps m2).
 
+(**
+  Check if m1 is a more precise floating point type, meaning that the corresponding machine epsilon is less.
+  Special Case m0, which must be the bottom element.
+**)
+Definition isMorePrecise' (m1:mType) (m2:mType) :=
+  match m2, m1 with
+  |M0, _ => true
+  |M32, M0 => false
+  |M32, _ => true
+  |M64, M0 | M64, M32 => false
+  |M64, _ => true
+  |M128, M128 => true
+  |M128, M256 => true
+  |M256, M256 => true
+  |_, _ => false
+  end.
+
+Lemma ismoreprec_rw m1 m2:
+  forall b, isMorePrecise m1 m2  = b <-> isMorePrecise' m1 m2 = b.
+Admitted.
+
 Lemma isMorePrecise_refl (m1:mType) :
   isMorePrecise m1 m1 = true.
 Proof.
@@ -186,7 +207,7 @@ Definition computeJoin (m1:mType) (m2:mType) :=
 
 
 Lemma ifM0isJoin_l (m:mType) (m1:mType) (m2:mType) :
-  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0. 
+  m = M0 -> isJoinOf m m1 m2 = true -> m1 = M0.
 Proof.
   intros H0 H.
   unfold isJoinOf in H.

coq/ssaPrgs.v

@@ -79,11 +79,11 @@ Proof.
       * destruct eval_e1_def as [vR1 eval_e1_def];
           destruct eval_e2_def as [vR2 eval_e2_def].
         exists (perturb (evalBinop b vR1 vR2) 0); econstructor; eauto.
-        auto. 
+        auto.
         simpl. rewrite Q2R0_is_0. rewrite Rabs_R0; lra.
-  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e))  vR M0) as eval_r_def by (eapply IHe; eauto). 
+  - assert (exists vR, eval_exp (toREvalEnv E) (toREval (toRExp e))  vR M0) as eval_r_def by (eapply IHe; eauto).
     destruct eval_r_def as [vr eval_r_def].
-    exists vr. 
+    exists vr.
     simpl toREval.
     auto.
 Qed.
@@ -174,7 +174,7 @@ Qed.
 Lemma ssa_shadowing_free m x y v v' e f inVars outVars E:
   ssaPrg (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars ->
   NatSet.In y inVars ->
-  eval_exp (toREvalEnv E) (toREval (toRExp e)) v M0 ->
+  eval_exp E (toREval (toRExp e)) v M0 ->
   forall E n, updEnv x m v (updEnv y m v' E) n = updEnv y m v' (updEnv x m v E) n.
 Proof.
   intros ssa_let y_free eval_e.
@@ -199,7 +199,7 @@ Lemma shadowing_free_rewriting_exp e v E1 E2:
 (*  (forall n, exists v m,
         E1 n = Some (v,m) ->
         exists m', (E2 n = Some (v,m') /\ (meps m) == (meps m'))) ->*)
-  (forall n, E1 n = E2 n)-> 
+  (forall n, E1 n = E2 n)->
   eval_exp E1 (toREval e) v M0 <->
   eval_exp E2 (toREval e) v M0.
 Proof.
@@ -231,9 +231,6 @@ Proof.
 Qed.
 
 Lemma shadowing_free_rewriting_cmd f E1 E2 vR:
-(*  (forall n, exists v m,
-        E1 n = Some (v,m) ->
-        exists m', (E2 n = Some (v,m') /\ (meps m) == (meps m'))) ->*)
   (forall n, E1 n = E2 n) ->
   bstep (toREvalCmd f) E1 vR M0 <->
   bstep (toREvalCmd f) E2 vR M0.
@@ -258,7 +255,7 @@ revert E1 E2 vR.
       constructor; auto.
     + erewrite <- shadowing_free_rewriting_exp in H0; auto.
       constructor; auto.
-Qed.  
+Qed.
 
 Lemma dummy_bind_ok e v x v' inVars E:
   NatSet.Subset (usedVars e) inVars ->
@@ -300,8 +297,8 @@ Proof.
     + eapply IHe2; eauto.
       hnf; intros a in_e2.
       apply valid_vars;
-        rewrite NatSet.union_spec; auto.  
-  - apply (IHe v1 x v2 inVars E); auto. 
+        rewrite NatSet.union_spec; auto.
+  - apply (IHe v1 x v2 inVars E); auto.
 Qed.
 
 Fixpoint exp_subst (e:exp Q) x e_new :=
@@ -314,9 +311,9 @@ Fixpoint exp_subst (e:exp Q) x e_new :=
   end.
 
 Lemma exp_subst_correct e e_sub E x v v_res:
-  eval_exp (toREvalEnv E) (toREval (toRExp e_sub)) v M0 ->
-  eval_exp (toREvalEnv (updEnv x M0 v E)) (toREval (toRExp e)) v_res M0 <->
-  eval_exp (toREvalEnv E) (toREval (toRExp (exp_subst e x e_sub))) v_res M0.
+  eval_exp E (toREval (toRExp e_sub)) v M0 ->
+  eval_exp (updEnv x M0 v E) (toREval (toRExp e)) v_res M0 <->
+  eval_exp E (toREval (toRExp (exp_subst e x e_sub))) v_res M0.
 Proof.
   intros eval_e.
   revert v_res.
@@ -336,9 +333,7 @@ Proof.
         assert (updEnv x M0 v E n = Some (v_res, M0)).
         { unfold updEnv; rewrite n_eq_case.
           f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. }
-        { econstructor; eauto.
-          unfold toREvalEnv. unfold updEnv in *. rewrite n_eq_case in *.
-          auto. }
+        { econstructor; eauto. }
       * simpl. inversion eval_subst; subst.
         assert (E n = updEnv x M0 v E n).
         { unfold updEnv; rewrite n_eq_case; reflexivity. }
@@ -349,10 +344,10 @@ Proof.
   - split; [intros eval_upd | intros eval_subst].
     + inversion eval_upd; econstructor; auto;
         rewrite <- IHe; auto.
-    + inversion eval_subst; econstructor; auto;
+    + inversion eval_subst; constructor; try auto;
         rewrite IHe; auto.
   - intros v_res; split; [intros eval_upd | intros eval_subst].
-    + inversion eval_upd; econstructor; auto; 
+    + inversion eval_upd; econstructor; auto;
         assert (M0 = M0) as M00 by auto; pose proof (ifM0isJoin_l M0 m1 m2 M00 H2);
           pose proof (ifM0isJoin_r M0 m1 m2 M00 H2); subst.
       * apply H2.
@@ -375,6 +370,7 @@ Fixpoint map_subst (f:cmd Q) x e :=
   |Ret e_r => Ret (exp_subst e_r x e)
   end.
 
+(*
 Lemma updEnv_comp_toREval (n:nat) (v:R):
   forall E var, updEnv n M0 v (toREvalEnv E) var = toREvalEnv (updEnv n M0 v E) var.
 Proof.
@@ -410,7 +406,7 @@ Proof.
   - apply IHe; auto.
   - apply IHe; auto.
 Qed.
-    
+
 Lemma bla (c: cmd Q) (n:nat) (v vR:R) (E:env):
   bstep (toREvalCmd (toRCmd c)) (updEnv n M0 v (toREvalEnv E)) vR M0 <->
   bstep (toREvalCmd (toRCmd c)) (toREvalEnv (updEnv n M0 v E)) vR M0.
@@ -430,57 +426,56 @@ Admitted.
 (*       replace E with (toREvalEnv E) by admit. *)
 (*       apply H9. *)
 (* Admitted. *)
+*)
 
 Lemma stepwise_substitution x e v f E vR inVars outVars:
   ssaPrg (toREvalCmd (toRCmd f)) inVars outVars ->
   NatSet.In x inVars ->
   NatSet.Subset (usedVars e) inVars ->
-  eval_exp (toREvalEnv E) (toREval (toRExp e)) v M0 ->
-  bstep (toREvalCmd (toRCmd f)) (updEnv x M0 v (toREvalEnv E)) vR M0 <->
-  bstep (toREvalCmd (toRCmd (map_subst f x e))) (toREvalEnv E) vR M0.
+  eval_exp E (toREval (toRExp e)) v M0 ->
+  bstep (toREvalCmd (toRCmd f)) (updEnv x M0 v E) vR M0 <->
+  bstep (toREvalCmd (toRCmd (map_subst f x e))) E vR M0.
 Proof.
   revert E e x vR inVars outVars.
   induction f; intros E e0 x vR inVars outVars ssa_f x_free valid_vars_e eval_e.
   - split; [ intros bstep_let | intros bstep_subst].
     + inversion bstep_let; subst.
       inversion ssa_f; subst.
-      assert (forall E var, updEnv n M0 v0 (updEnv x M0 v (toREvalEnv E)) var = toREvalEnv (updEnv x M0 v (updEnv n M0 v0 E)) var) by admit.
-      rewrite (shadowing_free_rewriting_cmd _ _ _ _ (H E)) in H8.
-      econstructor; auto.
-      rewrite <- exp_subst_correct; eauto.
-      apply bli; apply H7.
-(* /!\ *) apply bla. 
-      rewrite <- IHf; eauto.
-(* /!\ *) apply bla; auto.
-      rewrite NatSet.add_spec; right; auto.
-      apply validVars_add; auto.
-      apply bli.
-      eapply dummy_bind_ok; eauto.
+      assert (forall E var, updEnv n M0 v0 (updEnv x M0 v E) var = updEnv x M0 v (updEnv n M0 v0 E) var).
+      * eapply ssa_shadowing_free.
+        apply ssa_f.
+        apply x_free.
+        apply H7.
+      * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto.
+        simpl in *.
+        econstructor; eauto.
+        { rewrite <- exp_subst_correct; eauto. }
+        { rewrite <- IHf; eauto.
+          rewrite NatSet.add_spec; right; auto.
+          apply validVars_add; auto.
+          eapply dummy_bind_ok; eauto. }
     + inversion bstep_subst; subst.
       simpl in *.
       inversion ssa_f; subst.
-      econstructor.
-      auto.
-      apply bli. rewrite exp_subst_correct; eauto.
-(* /!\ *) apply bla in H8; rewrite <- IHf in H8; eauto.
-      rewrite <- shadowing_free_rewriting_cmd in H8; eauto.
-      * admit. (* should be ok. Maybe using updEnv_comp_toREval? *)
-      * rewrite <- exp_subst_correct in H7; eauto.
-        rewrite NatSet.add_spec.
-        right; auto.
+      econstructor; try auto.
+      rewrite exp_subst_correct; eauto.
+      rewrite <- IHf in H8; eauto.
+      * rewrite <- shadowing_free_rewriting_cmd in H8; eauto.
+        eapply ssa_shadowing_free; eauto.
+        rewrite <- exp_subst_correct in H7; eauto.
+      * rewrite NatSet.add_spec; auto.
       * apply validVars_add; auto.
-      * apply bli. eapply dummy_bind_ok; eauto.
+      * eapply dummy_bind_ok; eauto.
   - split; [intros bstep_let | intros bstep_subst].
     + inversion bstep_let; subst.
       simpl in *.
-      apply bli in H0; rewrite exp_subst_correct in H0; eauto.
+      rewrite exp_subst_correct in H0; eauto.
       constructor. assumption.
     + inversion bstep_subst; subst.
       simpl in *.
       rewrite <- exp_subst_correct in H0; eauto.
       econstructor; eauto.
-      apply bli; auto.
-Admitted.
+Qed.
 
 Fixpoint let_subst (f:cmd Q) :=
   match f with
@@ -494,11 +489,11 @@ Fixpoint let_subst (f:cmd Q) :=
 
 Theorem let_free_form f E vR inVars outVars e:
   ssaPrg f inVars outVars ->
-  bstep (toREvalCmd (toRCmd f)) (toREvalEnv E) vR M0 ->
+  bstep (toREvalCmd (toRCmd f)) E vR M0 ->
   let_subst f = Some e ->
-  bstep (toREvalCmd (toRCmd (Ret e))) (toREvalEnv E) vR M0.
+  bstep (toREvalCmd (toRCmd (Ret e))) E vR M0.
 Proof.
-  revert E vR inVars outVars e;
+    revert E vR inVars outVars e;
     induction f;
     intros E vR inVars outVars e_subst ssa_f bstep_f subst_step.
   - simpl.
@@ -507,7 +502,6 @@ Proof.
     simpl in subst_step.
     case_eq (let_subst f).
     + intros f_subst subst_f_eq.
-(* /!\ *) apply bla in H8.
       specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H10 H8 subst_f_eq).
       rewrite subst_f_eq in subst_step.
       inversion IHf; subst.
@@ -521,21 +515,4 @@ Proof.
     simpl in *.
     inversion subst_step; subst.
     assumption.
-Qed.
-
-(*
-Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env)
-      (ParamEnv:param_env) (P:precond) (eps:R):
-  ssaPrg Q f inVars outVars ->
-  (forall v, NatSet.In v (freeVars e) ->
-        (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R ->
-  (forall v, NatSet.In v inVars ->
-        exists r, VarEnv v = Some r) ->
-  exists vR,
-    bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR.
-Proof.
-  intros ssa_f; revert VarEnv ParamEnv P eps.
-  induction ssa_f;
-    intros VarEnv ParamEnv P eps fVars_live.
-  -
- *)
\ No newline at end of file
+Qed.
\ No newline at end of file