Typing of expressions is done. However, there are still some admits in the...

Typing of expressions is done. However, there are still some admits in the proofs, to be fixed in the following days.

coq/CertificateChecker.v

@@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
   if (validIntervalbounds e absenv P NatSet.empty)
-  then (validErrorbound e (typeExpression e) absenv NatSet.empty)
+  then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty)
   else false.
 
 (**
@@ -47,20 +47,20 @@ Proof.
   destruct iv as [ivlo ivhi].
   rewrite absenv_eq; simpl.
   eapply validErrorbound_sound; eauto.
-  - eapply typeExpressionIsSound; eauto.
+  - admit. (*eapply validTypeMap; eauto. *)
   - hnf. intros a in_diff.
     rewrite NatSet.diff_spec in in_diff.
     apply fVars_subset.
     destruct in_diff; auto.
-  - apply stupid; rewrite expEqBool_refl; auto.
-  - intros e0 v m0 v_in_empty.
+  - intros v m0 v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.
-Qed.
+Admitted.
+(* Qed. *)
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
   if (validIntervalboundsCmd f absenv P NatSet.empty)
-  then (validErrorboundCmd f absenv NatSet.empty)
+  then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty)
   else false.
 
 Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
@@ -90,6 +90,7 @@ Proof.
   destruct iv as [ivlo ivhi].
   rewrite absenv_eq; simpl.
   eapply (validErrorboundCmd_sound); eauto.
+  - admit. (* eapply typeMapCmdValid; eauto.*) 
   - instantiate (1 := outVars).
     eapply ssa_equal_set; try eauto.
     hnf.
@@ -105,4 +106,4 @@ Proof.
   - intros v m1 v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.
-Qed.
\ No newline at end of file
+Admitted.
\ No newline at end of file

coq/IntervalValidation.v

@@ -255,9 +255,9 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
   forall vR m,
     validType Gamma f m ->
     validIntervalbounds f absenv P dVars = true ->
-    (forall v, NatSet.mem v dVars = true ->
-          exists vR mv, E v = Some (vR, M0) /\ Gamma (Var Q mv v) = Some mv /\
-                (Q2R (fst (fst (absenv (Var Q mv v)))) <= vR <= Q2R (snd (fst (absenv (Var Q mv v)))))%R) ->
+    (forall v mV, NatSet.mem v dVars = true ->
+          exists vR mv, E v = Some (vR, M0) /\ Gamma (Var Q mv v) = Some mV /\
+                (Q2R (fst (fst (absenv (Var Q mV v)))) <= vR <= Q2R (snd (fst (absenv (Var Q mV v)))))%R) ->
     NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
     (forall v, NatSet.mem v fVars = true ->
           exists vR, E v = Some (vR, M0) /\
@@ -273,19 +273,10 @@ Proof.
     simpl; rewrite absenv_var in *; simpl in *.
     inversion eval_f; subst.
     case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
-    + specialize (valid_definedVars n case_mem).
+    + specialize (valid_definedVars n m case_mem).
       inversion typing_ok; subst.
       destruct valid_definedVars as [vR' [mv [E_n_eq [gamma_n iv_n]]]].
       rewrite H2 in E_n_eq; inversion E_n_eq; subst.
-      
-      (* assert (mTypeEqBool m m && (n =? n) = true). *)
-      (* apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto. *)
-      (* rewrite H in valid_definedVars. *)
-      (* assert (Some m = Some m) by auto. *)
-      (* specialize (valid_definedVars H0). *)
-      rewrite H; auto.
-      rewrite E_n_eq in *.
-      inversion H2; subst.
       rewrite absenv_var in *; auto.
     + repeat (rewrite delta_0_deterministic in *; try auto).
       unfold isSupersetIntv in valid_bounds.
@@ -339,8 +330,9 @@ Proof.
     destruct valid_bounds as [valid_rec valid_unop].
     apply Is_true_eq_true in valid_rec.
     inversion eval_f; subst.
-    + assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
-      specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
+    + (*assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).*)
+      inversion typing_ok; subst.
+      specialize (IHf v1 mf H1 valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
       rewrite absenv_f in IHf; simpl in IHf.
       (* TODO: Make lemma *)
       unfold isSupersetIntv in valid_unop.
@@ -358,8 +350,9 @@ Proof.
       * eapply Rle_trans.
         Focus 2. apply valid_hi.
         rewrite Q2R_opp; lra.
-    + assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
-      specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H4).
+    + (*assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).*)
+      inversion typing_ok; subst.
+      specialize (IHf v1 mf H2 valid_rec valid_definedVars usedVars_subset valid_usedVars H4).
       rewrite absenv_f in IHf; simpl in IHf.
       apply andb_prop_elim in valid_unop.
       destruct valid_unop as [nodiv0 valid_unop].
@@ -400,7 +393,7 @@ Proof.
              hnf; intros is_0.
              assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
              rewrite <- Q2R0_is_0 in nodiv0_pos.
-             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
+             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
          }
          { eapply Rle_trans.
            Focus 2. apply valid_hi.
@@ -425,7 +418,7 @@ Proof.
              hnf; intros is_0.
              assert (Q2R (fst intv_f) <= Q2R (snd intv_f))%R by lra.
              rewrite <- Q2R0_is_0 in nodiv0_pos.
-             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H2; lra.
+             apply Rlt_Qlt in nodiv0_pos; apply Rle_Qle in H3; lra.
          }
          { rewrite Q2R0_is_0 in H1; auto. }
   - inversion eval_f; subst.
@@ -444,16 +437,18 @@ Proof.
     destruct valid_rec as [valid_e1 valid_e2].
     apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in  valid_e2.
     destruct m1; destruct m2; cbv in H2; inversion H2.
-    pose proof (typeMap_gives_type _ typing_ok).
-    simpl in H. case_eq (typeExpression f1); intros; rewrite H0 in H; [ | inversion H ].
-    case_eq (typeExpression f2); intros; rewrite H1 in H; inversion H.
-    pose proof (validVarsUnfolding_l _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f1.
-    pose proof (validVarsUnfolding_r _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f2.
+    inversion typing_ok; subst.
+    
+    (* pose proof (typeMap_gives_type _ typing_ok). *)
+    (* simpl in H. case_eq (typeExpression f1); intros; rewrite H0 in H; [ | inversion H ]. *)
+    (* case_eq (typeExpression f2); intros; rewrite H1 in H; inversion H. *)
+    (* pose proof (validVarsUnfolding_l _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f1. *)
+    (* pose proof (validVarsUnfolding_r _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f2. *)
     (* pose proof (binop_type_unfolding _ _ _ typing_ok) as subtypes. *)
     (* destruct subtypes as [mf1 [mf2 [typing_f1 [typing_f2 join_f1_f2]]]]. *)
-    apply typeGivesTypeMap in H0. apply typeGivesTypeMap in H1.
-    specialize (IHf1 v1 m H0 valid_e1 valid_definedVars_f1).
-      specialize (IHf2 v2 m0 H1 valid_e2 valid_definedVars_f2).
+    (* apply typeGivesTypeMap in H0. apply typeGivesTypeMap in H1. *)
+    specialize (IHf1 v1 m1 H3 valid_e1 valid_definedVars). 
+      specialize (IHf2 v2 m2 H7 valid_e2 valid_definedVars).
     rewrite absenv_f1 in IHf1.
     rewrite absenv_f2 in IHf2.
     assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1.
@@ -568,21 +563,21 @@ Proof.
                       [ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
           - destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto.
             + rewrite <- Q2R0_is_0.
-              destruct H3; [left | right]; apply Qlt_Rlt; auto.
+              destruct H; [left | right]; apply Qlt_Rlt; auto.
             + unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
               simpl in *.
               assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra.
               assert (~ snd iv2 == 0).
               * destruct H; try lra.
                 hnf; intros ivhi2_0.
-                apply Rle_Qle in H8.
-                rewrite ivhi2_0 in H8.
+                apply Rle_Qle in H0.
+                rewrite ivhi2_0 in H0.
                 lra.
               * assert (~ fst iv2 == 0).
                 { destruct H; try lra.
                   hnf; intros ivlo2_0.
-                  apply Rle_Qle in H8.
-                  rewrite ivlo2_0 in H8.
+                  apply Rle_Qle in H0.
+                  rewrite ivlo2_0 in H0.
                   lra. }
                 { split.
                   - eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
@@ -605,7 +600,6 @@ Proof.
     + destruct m1; destruct m2; inversion H2.
       simpl in H4; rewrite Q2R0_is_0 in H4; auto.
   - unfold validIntervalbounds in valid_bounds.
-    pose proof (typeMap_gives_type _ typing_ok) as t_downcast.
     (*simpl erasure in valid_bounds.*)
     simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f); simpl in *.
     apply Is_true_eq_left in valid_bounds.
@@ -620,12 +614,9 @@ Proof.
     simpl in *.
     apply Qeq_eqR in Eqlo; rewrite Eqlo.
     apply Qeq_eqR in Eqhi; rewrite Eqhi.
-    pose proof (expEqBool_refl (Downcast m f)); simpl in H; rewrite H in typing_ok; inversion typing_ok; subst.
-    case_eq (typeExpression f); intros. 
-    + apply (IHf vR m); auto.
-      * apply typeGivesTypeMap; auto.
-      * apply Is_true_eq_true in vI1; auto.
-    + rewrite H0 in t_downcast; inversion t_downcast.       
+    inversion typing_ok; subst.
+    eapply IHf; try eauto.
+    apply Is_true_eq_true in vI1; auto.
 Qed.
 
 

coq/Typing.v

@@ -135,7 +135,7 @@ Inductive validType (Gamma:exp Q -> option mType) : exp Q -> mType -> Prop :=
    isMorePrecise m1 m = true ->
    Gamma (Downcast m e1) = Some m ->
    validType Gamma (Downcast m e1) m.
-
+   
 Lemma valid_typing e m:
   typeExpression e = Some m ->
   validType (fun e => typeExpression e) e m.
@@ -155,7 +155,46 @@ Proof.
     econstructor; try eauto.
     simpl; rewrite H0,H1; auto.
 Qed.
-  
+
+
+Inductive validTypeCmd (Gamma:exp Q -> option mType) : cmd Q -> mType -> Prop :=
+|tRet m e:
+   validType Gamma e m -> validTypeCmd Gamma (Ret e) m
+|tLet m x e c mc:
+   validType Gamma e m ->
+   validType Gamma (Var Q m x) m ->
+   validTypeCmd Gamma c mc ->
+   validTypeCmd Gamma (Let m x e c) mc.
+
+Fixpoint typeCmd (f:cmd Q) (vartype:nat -> option mType) : option mType :=
+  match f with
+  |Let m n e c => match typeExpression e with
+                 |Some m' => if mTypeEqBool m m' then typeCmd c (fun f => if (n =? f) then Some m else vartype f)
+                            else None
+                 |None => None
+                 end
+  |Ret e => typeExpression e (* TODO vartype *)
+  end.
+
+Fixpoint typeMapCmd (f:cmd Q) (f':exp Q) : option mType :=
+  match f with
+  |Let m n e c => if expEqBool f' (Var Q m n) then
+                    match typeMap e f' with
+                    |None => None
+                    |Some m1 => if mTypeEqBool m1 m then Some m else None
+                    end
+                  else
+                    let te := typeMap e in
+                    let tc := typeMapCmd c in
+                    match (te f'), (tc f') with
+                    |Some m1, Some m2 => if mTypeEqBool m1 m2 then Some m1 else None
+                    |Some m1, None => Some m1
+                    |None, Some m2 => Some m2
+                    |None, None => None
+                    end
+  |Ret e => (typeMap e) f'
+  end.
+
   
 
 Lemma Gamma_strengthening e m Gamma1 Gamma2:
@@ -186,6 +225,124 @@ Lemma downcast_neq m e:
   expEqBool (Downcast m e) e = false.
 Admitted.
 
+Lemma typeExpressionIsSound E e v m:
+  eval_exp E (toRExp e) v m ->
+  typeExpression e = Some m.
+Proof.
+  revert v m; induction e; intros * eval_e.
+  - simpl.  inversion eval_e; subst; auto.
+  - simpl. inversion eval_e; subst; auto.
+  - simpl.
+    inversion eval_e; subst.
+    + eapply IHe; eauto.
+    + eapply IHe; eauto.
+  - simpl.
+    inversion eval_e; subst.
+    specialize (IHe1 _ _ H5).
+    specialize (IHe2 _ _ H6).
+    rewrite IHe1, IHe2.
+    auto.
+  - inversion eval_e; subst; simpl.
+    specialize (IHe _ _ H5); rewrite IHe.
+    rewrite H1; auto.
+Qed.
+    
+
+
+Lemma validTypeMap e m vF E2:
+  eval_exp E2 (toRExp e) vF m ->  validType (typeMap e) e m.
+Proof.
+  revert m vF; induction e; intros * eval_e.
+  - inversion eval_e; subst.
+    econstructor; eauto.
+    unfold typeMap; rewrite expEqBool_refl; auto.
+  - inversion eval_e; subst.
+    econstructor; eauto.
+    unfold typeMap; rewrite expEqBool_refl; auto.
+  - inversion eval_e; subst.
+    + specialize (IHe _ _ H3).
+      econstructor; eauto. 
+      * eapply Gamma_strengthening; auto.
+        Focus 2. eauto.
+        intros. unfold typeMap.
+        assert (expEqBool (Unop Neg e) e0 = false) by admit.
+        rewrite H0; auto.
+      * simpl; rewrite expEqBool_refl.
+        eapply typeExpressionIsSound; eauto.
+    + specialize (IHe _ _ H4).
+      econstructor; eauto.
+      * eapply Gamma_strengthening; auto.
+        Focus 2. eauto.
+        intros. unfold typeMap.
+        assert (expEqBool (Unop Inv e) e0= false) by admit.
+        rewrite H0; auto.
+      * simpl; rewrite expEqBool_refl.
+        eapply typeExpressionIsSound; eauto.
+  - inversion eval_e; subst.
+    econstructor; eauto.
+    + specialize (IHe1 _ _ H5).
+      eapply Gamma_strengthening.
+      Focus 2. eapply IHe1.
+      intros. unfold typeMap. 
+      assert (expEqBool (Binop b e1 e2) e = false) by admit.
+      rewrite H0.
+      unfold typeMap in H; rewrite H.
+      auto.
+    + specialize (IHe2 _ _ H6).
+      eapply Gamma_strengthening.
+      Focus 2. eapply IHe2.
+      intros. unfold typeMap. 
+      assert (expEqBool (Binop b e1 e2) e = false) by admit.
+      rewrite H0.
+      unfold typeMap in H; rewrite H.
+      case_eq (typeMap e1 e); intros; unfold typeMap in H1; rewrite H1.
+      * (* todo: need to change typeMap *) admit.
+      * auto.
+    + unfold typeMap; rewrite expEqBool_refl.
+        eapply typeExpressionIsSound; eauto.
+  - inversion eval_e; subst.
+    econstructor; eauto.
+    + eapply Gamma_strengthening.
+      Focus 2. eapply IHe; eauto.
+      intros. unfold typeMap.
+      assert (expEqBool (Downcast m0 e) e0 = false) by admit.
+      rewrite H0.
+      unfold typeMap in H. auto.
+    + unfold typeMap; rewrite expEqBool_refl.
+      eapply typeExpressionIsSound; eauto.
+Admitted.
+
+Lemma typeCmdIsSound f E v m cont:
+  bstep (toRCmd f) E v m -> typeCmd f cont  = Some m.
+Proof.
+  revert cont E v m; induction f; intros.
+  - inversion H; subst.
+    specialize (IHf (fun n' => if n =? n' then Some m else cont n') _ _ _ H8).
+    simpl.
+    pose proof (typeExpressionIsSound _ H7) as t_e; rewrite t_e.
+    rewrite mTypeEqBool_refl.
+    rewrite IHf.
+    auto.
+  - simpl.
+    inversion H; subst.
+    eapply typeExpressionIsSound; eauto.
+Qed.
+    
+Lemma typeMapCmdValid f E v m:
+  bstep (toRCmd f) E v m -> validTypeCmd (typeMapCmd f) f m.
+Proof.
+  revert E v m; induction f; intros * bstep_f.
+  - inversion bstep_f; subst.
+    econstructor; eauto.
+    + pose proof (validTypeMap _ H6).
+      eapply Gamma_strengthening.
+      Focus 2. eapply H.
+      intros.  simpl. rewrite H0.
+      case_eq (expEqBool e0 (Var Q m n)); intros eq_e_varn.
+      * admit.
+      * admit.
+    + econstructor; eauto.
+Admitted.
 
 (* Fixpoint isSubExpression (e':exp Q) (e:exp Q) := *)
 (*   orb (expEqBool e e') *)