Certificate checking Coq development is now finished?

coq/CertificateChecker.v

@@ -12,9 +12,11 @@ Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 
 (** Certificate checking function **)
-Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
+Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
+  if (typeCheck e defVars (typeMap defVars e)) then 
     if (validIntervalbounds e absenv P NatSet.empty)
-  then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty)
+    then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
+    else false
   else false.
 
 (**
@@ -22,16 +24,16 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
    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:exp Q) (absenv:analysisResult) P:
+Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars:
   forall (E1 E2:env) (vR:R) (vF:R) fVars m,
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
     (forall v, NatSet.mem v fVars = true ->
-          exists vR, E1 v = Some (vR, M0) /\
+          exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     NatSet.Subset (Expressions.usedVars e) fVars ->
-    eval_exp E1  (toREval (toRExp e)) vR M0 ->
-    eval_exp E2 (toRExp e) vF m ->
-    CertificateChecker e absenv P = true ->
+    eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 ->
+    eval_exp E2 defVars (toRExp e) vF m ->
+    CertificateChecker e absenv P defVars = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
@@ -47,33 +49,33 @@ Proof.
   destruct iv as [ivlo ivhi].
   rewrite absenv_eq; simpl.
   eapply validErrorbound_sound; eauto.
-  - admit. (*eapply validTypeMap; eauto. *)
   - hnf. intros a in_diff.
     rewrite NatSet.diff_spec in in_diff.
     apply fVars_subset.
     destruct in_diff; auto.
-  - intros v m0 v_in_empty.
+  - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.
-Admitted.
-(* Qed. *)
+Qed.
 
-Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) :=
-  if (validIntervalboundsCmd f absenv P NatSet.empty)
-  then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty)
+Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
+  if (typeCheckCmd f defVars (typeMapCmd defVars f))
+       then if (validIntervalboundsCmd f absenv P NatSet.empty)
+            then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
+            else false
   else false.
 
-Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P:
+Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars:
   forall (E1 E2:env) outVars vR vF fVars m,
-    approxEnv E1 absenv fVars NatSet.empty E2 ->
+    approxEnv E1 defVars absenv fVars NatSet.empty E2 ->
     (forall v, NatSet.mem v fVars= true ->
-          exists vR, E1 v = Some (vR, M0) /\
+          exists vR, E1 v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
     NatSet.Subset (Commands.freeVars f) fVars ->
     ssa f fVars outVars ->
-    bstep (toREvalCmd (toRCmd f)) E1 vR M0 ->
-    bstep (toRCmd f) E2 vF m ->
-    CertificateCheckerCmd f absenv P = true ->
+    bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 ->
+    bstep (toRCmd f) E2 defVars vF m ->
+    CertificateCheckerCmd f absenv P defVars = true ->
     (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R.
 (**
    The proofs is a simple composition of the soundness proofs for the range
@@ -90,7 +92,6 @@ 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.
@@ -103,7 +104,7 @@ Proof.
     rewrite NatSet.diff_spec in in_diff.
     destruct in_diff.
     apply fVars_subset; auto.
-  - intros v m1 v_in_empty.
+  - intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty.
-Admitted.
\ No newline at end of file
+Qed.
\ No newline at end of file

coq/Commands.v

@@ -52,7 +52,8 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
 Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop :=
   let_b m m' x e s E v res defVars:
     eval_exp E defVars  e v m ->
-    bstep s (updEnv x m v E) defVars res m' ->
+    defVars x = Some m ->
+    bstep s (updEnv x v E) defVars res m' ->
     bstep (Let m x e s) E defVars res m'
  |ret_b m e E v defVars:
     eval_exp E defVars e v m ->

coq/Environments.v

@@ -12,24 +12,25 @@ It is necessary to have this relation, since two evaluations of the very same
 expression may yield different values for different machine epsilons
 (or environments that already only approximate each other)
  **)
-Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
+Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop :=
 |approxRefl A:
-   approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
-|approxUpdFree E1 E2 A v1 v2 x fVars dVars m:
-   approxEnv E1 A fVars dVars E2 ->
+   approxEnv emptyEnv (fun n => None) A NatSet.empty NatSet.empty emptyEnv
+|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m:
+   approxEnv E1 defVars A fVars dVars E2 ->
+   defVars x = Some m ->
    (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2)
-|approxUpdBound E1 E2 A v1 v2 x fVars dVars m:
-   approxEnv E1 A fVars dVars E2 ->
+   approxEnv (updEnv x v1 E1) defVars A (NatSet.add x fVars) dVars (updEnv x v2 E2)
+|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars:
+   approxEnv E1 defVars A fVars dVars E2 ->
    (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R ->
    NatSet.mem x (NatSet.union fVars dVars) = false ->
-   approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2).
+   approxEnv (updEnv x v1 E1) defVars A fVars (NatSet.add x dVars) (updEnv x v2 E2).
 
-Inductive approxParams :env -> env -> Prop :=
-|approxParamRefl:
-   approxParams emptyEnv emptyEnv
-|approxParamUpd E1 E2 m x v1 v2 :
-   approxParams E1 E2 ->
-   (Rabs (v1 - v2) <= Q2R (meps m))%R ->
-   approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2).
+(* Inductive approxParams :env -> env -> Prop := *)
+(* |approxParamRefl: *)
+(*    approxParams emptyEnv emptyEnv *)
+(* |approxParamUpd E1 E2 m x v1 v2 : *)
+(*    approxParams E1 E2 -> *)
+(*    (Rabs (v1 - v2) <= Q2R (meps m))%R -> *)
+(*    approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *)

coq/ErrorBounds.v

@@ -8,7 +8,7 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSim
 Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars:
-  eval_exp E1 defVars (Const M0 n) nR M0 ->
+  eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 ->
   eval_exp E2 defVars (Const m n) nF m ->
   (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R.
 Proof.
@@ -45,12 +45,12 @@ Qed.
 
 Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
       (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
-  eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1->
-  eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 defVars (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Plus (Var R 1) (Var R 2)) vF m->
+  eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Plus (Var R 1) (Var R 2)) vF m->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R.
@@ -110,12 +110,12 @@ Qed.
 **)
 Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R)
       (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars:
-  eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 defVars (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Sub (Var R 1) (Var R 2)) vF m ->
+  eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))              (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n)  (Binop Sub (Var R 1) (Var R 2)) vF m ->
   (Rabs (e1R - e1F) <= Q2R err1)%R ->
   (Rabs (e2R - e2F) <= Q2R err2)%R ->
   (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R.
@@ -169,12 +169,12 @@ Qed.
 
 Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
       (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 defVars (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Mult (Var R 1) (Var R 2)) vF m->
+  eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Mult (Var R 1) (Var R 2)) vF m->
   (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float mult_real mult_float.
@@ -218,12 +218,12 @@ Qed.
 
 Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
       (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars:
-  eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 ->
   eval_exp E2 defVars (toRExp e1) e1F m1 ->
-  eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 ->
   eval_exp E2 defVars (toRExp e2) e2F m2 ->
-  eval_exp E1 defVars (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
-  eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Div (Var R 1) (Var R 2)) vF m ->
+  eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 ->
+  eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Div (Var R 1) (Var R 2)) vF m ->
   (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R.
 Proof.
   intros e1_real e1_float e2_real e2_float div_real div_float.
@@ -443,9 +443,9 @@ Proof.
 Qed.
 
 Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars:
-  eval_exp E1 defVars (toREval e) nR M0 ->
+  eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 ->
   eval_exp E2 defVars e nF1 m ->
-  eval_exp (updEnv 1 m nF1 emptyEnv) defVars (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
+  eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n)  (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon->
   (Rabs (nR - nF1) <= err)%R ->
   (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R.
 Proof.

coq/Expressions.v

@@ -205,13 +205,6 @@ Fixpoint toREval (e:exp R) :=
   | Downcast _ e1 =>  (toREval e1)
   end.
 
-Definition toREvalEnv (E:env) : env :=
-  fun (n:nat) =>
-    let s := (E n) in
-    match s with
-    | None => None
-    | Some (r, _) => Some (r, M0)
-    end.
 
 
 (**
@@ -229,7 +222,7 @@ using a perturbation of the real valued computation by (1 + delta), where
 Inductive eval_exp (E:env) (defVars: nat -> option mType) :(exp R) -> R -> mType -> Prop :=
 | Var_load m x v:
     defVars x = Some m ->
-    E x = Some (v, m) ->
+    E x = Some v ->
     eval_exp E defVars (Var R x) v m
 | Const_dist m n delta:
     Rle (Rabs delta) (Q2R (meps m)) ->
@@ -340,19 +333,27 @@ Proof.
 Qed.
 
 
+Fixpoint toREvalVars (d:nat -> option mType) (n:nat) :=
+  match d n with
+  | Some m => Some M0
+  | None => None
+  end.
+
+
 (**
 Helping lemma. Needed in soundness proof.
 For each evaluation of using an arbitrary epsilon, we can replace it by
 evaluating the subexpressions and then binding the result values to different
 variables in the Environment.
-**)
+ **)
+
 Lemma binary_unfolding b f1 f2 m E vF defVars:
   eval_exp E defVars (Binop b f1 f2) vF m ->
   exists vF1 vF2 m1 m2,
     m = computeJoin m1 m2 /\
     eval_exp E defVars f1 vF1 m1 /\
     eval_exp E defVars f2 vF2 m2 /\
-    eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv))
+    eval_exp (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv))
              (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n)
              (Binop b (Var R 1) (Var R 2)) vF m.
 Proof.
@@ -366,28 +367,28 @@ Proof.
     eapply Var_load; eauto.
 Qed.
 
-(* Analogous lemma for unary expressions. *)
-Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R) defVars:
-  (eval_exp E defVars (Unop Inv e) v m ->
-   exists v1 m1,
-     eval_exp E defVars e v1 m1 /\
-     eval_exp (updEnv 1 m1 v1 E) (fun n => if (n =? 1) then Some m1 else defVars n) (Unop Inv (Var R 1)) v m).
-Proof.
-  intros eval_un.
-    inversion eval_un; subst.
-    exists v1; exists m.
-    repeat split; try auto.
-    econstructor; try auto.
-    pose proof (isMorePrecise_refl m).
-    econstructor; eauto.
-Qed.
+(* (* Analogous lemma for unary expressions. *) *)
+(* Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R) defVars: *)
+(*   (eval_exp E defVars (Unop Inv e) v m -> *)
+(*    exists v1 m1, *)
+(*      eval_exp E defVars e v1 m1 /\ *)
+(*      eval_exp (updEnv 1 v1 E) (fun n => if (n =? 1) then Some m1 else defVars n) (Unop Inv (Var R 1)) v m). *)
+(* Proof. *)
+(*   intros eval_un. *)
+(*     inversion eval_un; subst. *)
+(*     exists v1; exists m. *)
+(*     repeat split; try auto. *)
+(*     econstructor; try auto. *)
+(*     pose proof (isMorePrecise_refl m). *)
+(*     econstructor; eauto. *)
+(* Qed. *)
 
-(**
-  Using the parametric expressions, define boolean expressions for conditionals
-**)
-Inductive bexp (V:Type) : Type :=
-  leq: exp V -> exp V -> bexp V
-| less: exp V -> exp V -> bexp V.
+(* (** *)
+(*   Using the parametric expressions, define boolean expressions for conditionals *)
+(* **) *)
+(* Inductive bexp (V:Type) : Type := *)
+(*   leq: exp V -> exp V -> bexp V *)
+(* | less: exp V -> exp V -> bexp V. *)
 
 (**
   Define evaluation of boolean expressions

coq/Infra/Abbrevs.v

@@ -45,7 +45,7 @@ Definition precond :Type := nat -> intv.
 (**
   Abbreviation for the type of a variable environment, which should be a partial function
  **)
-Definition env := nat -> option (R * mType).
+Definition env := nat -> option R.
 
 (**
   The empty environment must return NONE for every variable
@@ -55,7 +55,7 @@ Definition emptyEnv:env := fun _ => None.
 (**
   Define environment update function as abbreviation, for variable environments
 **)
-Definition updEnv (x:nat) (mx:mType) (v: R) (E:env) (y:nat) :=
+Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
   if (y =? x) 
-  then Some (v, mx)
+  then Some v
   else E y.
\ No newline at end of file

coq/IntervalValidation.v

@@ -171,18 +171,19 @@ Proof.
   apply le_neq_bool_to_lt_prop; auto.
 Qed.
 
+    
 Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars:
   forall vR,
 (*    validType Gamma f m -> *)
     validIntervalbounds f absenv P dVars = true ->
     (forall v, NatSet.mem v dVars = true ->
-          exists vR, E v = Some (vR, M0) /\
+          exists vR, E v = Some vR /\
                 (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q 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) /\
+          exists vR, E v = Some vR /\
                 (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
-    eval_exp E defVars (toREval (toRExp f)) vR M0 ->
+    eval_exp E (toREvalVars defVars) (toREval (toRExp f)) vR M0 ->
   (Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
 Proof.
   induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.

coq/Typing.v

@@ -29,9 +29,11 @@ Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mT
   | Unop u e1 => if expEqBool e e' then typeExpression defVars e else typeMap defVars e1 e'
   | Binop b e1 e2 => if expEqBool e e' then typeExpression defVars e
                     else
-                      match (typeMap defVars e1 e') with
-                      | None => typeMap defVars e2 e'
-                      | x => x
+                      match (typeMap defVars e1 e'), (typeMap defVars e2 e')  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
   | Downcast m e1 => if expEqBool e e' then typeExpression defVars (Downcast m e1) else typeMap defVars e1 e'
   end.
@@ -40,7 +42,7 @@ Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mT
 Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType :=
   match f with
   |Let m n e c => match typeExpression defVars e with
-                 |Some m' => if mTypeEqBool m m' then typeCmd (fun f => if (n =? f) then Some m else defVars f) c
+                 |Some m' => if mTypeEqBool m m' then typeCmd defVars (*(fun f => if (n =? f) then Some m else defVars f)*) c
                             else None
                  |None => None
                  end
@@ -50,9 +52,9 @@ Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType :=
 Fixpoint typeMapCmd (defVars:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType :=
   match f with
   |Let m n e c => if expEqBool f' (Var Q n) then
-                    match typeMap defVars e f' with
-                    |None => None
-                    |Some m1 => if mTypeEqBool m1 m then Some m else None
+                   match defVars n with
+                   | Some m' => if mTypeEqBool m m' then Some m else None
+                   | None => None
                    end
                   else
                     let te := typeMap defVars e in
@@ -99,7 +101,7 @@ Fixpoint typeCheck (e:exp Q) (defVars:nat -> option mType) (tMap: exp Q -> optio
 Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> option mType) : bool :=
   match c with
   | Let m x e g => match tMap (Var Q x), tMap e with
-                  | Some mx, Some me => (mTypeEqBool mx m) && (mTypeEqBool mx me) && typeCheckCmd g defVars tMap
+                  | Some mx, Some me => (mTypeEqBool mx m) && (mTypeEqBool mx me) && typeCheck e defVars tMap && typeCheckCmd g defVars tMap
                   | _, _ => false
                   end
   | Ret e => typeCheck e defVars tMap
@@ -294,12 +296,12 @@ Theorem typingSoundnessCmd c defVars E v m Gamma:
   bstep (toRCmd c) E defVars v m ->
   (*(typeMapCmd defVars c)*) Gamma (getRetExp c) = Some m.
 Proof.
-  revert E; induction c; intros * tc bc.
+  revert E defVars; induction c; intros * tc bc.
   - simpl in tc.
     case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ].
     case_eq (Gamma e); intros; rewrite H0 in tc; [ | inversion tc ].
     andb_to_prop tc.
-    apply EquivEqBoolEq in L0; apply EquivEqBoolEq in R0; subst.
+    apply EquivEqBoolEq in L; apply EquivEqBoolEq in R1; subst.
     simpl.
     inversion bc; subst.
     eapply IHc; eauto.
@@ -308,6 +310,220 @@ Proof.
     eapply typingSoundnessExp; eauto.
 Qed.
 
+Lemma stupidlemma e defVars Gamma:
+  typeCheck e defVars Gamma = true ->
+  exists m, Gamma e = Some m.
+Proof.
+  destruct e; intros * tc.
+  - simpl in *.
+    case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ].
+    eauto.
+  - simpl in *.
+    case_eq (Gamma (Const m q)); intros; rewrite H in tc; [ | inversion tc ].
+    eauto.
+  - simpl in *.
+    case_eq (Gamma (Unop u e)); intros; rewrite H in tc; [ | inversion tc ].
+    eauto.
+  - simpl in *; 
+    case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
+  - simpl in *; 
+      case_eq (Gamma (Downcast m e)); intros; rewrite H in tc; [ | inversion tc ]; eauto.
+Qed.
+
+Fixpoint defVarsWellDefined (e:exp Q) (defVars:nat -> option mType) : bool :=
+  NatSet.for_all (fun v => match defVars v with | Some m => true | _ => false end) (usedVars e).
+
+Fixpoint defVarsWellDefinedCmd c defVars : bool :=
+  match c with
+  | Let m x e g => match defVars x with
+                  | Some m' => mTypeEqBool m m' && defVarsWellDefined e defVars && defVarsWellDefinedCmd g defVars
+                  | _ => false
+                  end
+  | Ret e => defVarsWellDefined e defVars
+  end.
+
+(* Theorem typeExpressionChecks e defVars: *)
+(*   defVarsWellDefined e defVars = true -> *)
+(*   typeCheck e defVars (fun e => typeExpression defVars e) = true. *)
+(* Proof. *)
+(*   intros defVars_wd. induction e. *)
+(*   - simpl in *. *)
+(*     apply NatSet.for_all_spec in defVars_wd; try auto. *)
+(*     Focus 2. intros a b c; rewrite c; auto. *)
+(*     specialize (defVars_wd n). *)
+(*     rewrite NatSet.singleton_spec in defVars_wd. *)
+(*     assert (n = n) by auto; specialize (defVars_wd H). *)
+(*     case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *)
+(*     rewrite mTypeEqBool_refl; auto. *)
+(*   - simpl. *)
+(*     rewrite mTypeEqBool_refl; auto. *)
+(*   - simpl in *. *)
+(*     assert (defVarsWellDefined e defVars = true) by admit. *)
+(*     specialize (IHe H). *)
+(*     pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *)
+(*     rewrite type_e, mTypeEqBool_refl; simpl. *)
+(*     auto. *)
+(*   - simpl in *. *)
+(*     assert (defVarsWellDefined e1 defVars = true) by admit. *)
+(*     specialize (IHe1 H). *)
+(*     assert (defVarsWellDefined e2 defVars = true) by admit. *)
+(*     specialize (IHe2 H0). *)
+(*     pose proof (stupidlemma _ _ _ IHe1) as [me1 type_e1]. *)
+(*     pose proof (stupidlemma _ _ _ IHe2) as [me2 type_e2]. *)
+(*     rewrite type_e1,type_e2,mTypeEqBool_refl; simpl; auto. *)
+(*     rewrite IHe1, IHe2; auto. *)
+(*   -  *)
+(*     unfold typeCheck. *)
+    
+
+(*     simpl in *. *)
+(*     assert (defVarsWellDefined e defVars = true) by admit. *)
+(*     specialize (IHe H). *)
+(*     pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *)
+(*     rewrite type_e. *)
+(*     assert (typeExpression defVars (Downcast m e) = Some m). *)
+(*     { simpl; rewrite type_e. *)
+
+    
+
+  
+(* Theorem typeMapChecks e defVars: *)
+(*   defVarsWellDefined e defVars = true ->  *)
+(*   (*(forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) ->*) *)
+(*   typeCheck e defVars (typeMap defVars e) = true. *)
+(* Proof. *)
+(*   intros defVars_wd; induction e; intros. *)
+(*   - simpl in *; rewrite <- beq_nat_refl. *)
+(*     rewrite NatSet.for_all_spec in defVars_wd. *)
+(*     + unfold NatSet.For_all in defVars_wd. *)
+(*       specialize (defVars_wd n). *)
+(*       rewrite NatSet.singleton_spec in defVars_wd. *)
+(*       assert (n = n) by auto; specialize (defVars_wd H). *)
+(*       case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *)
+(*       rewrite mTypeEqBool_refl; auto. *)
+(*     + intros a b hyp; rewrite hyp; auto. *)
+(*   - simpl in *. *)
+(*     rewrite mTypeEqBool_refl, Qeq_bool_refl; simpl. *)
+(*     rewrite mTypeEqBool_refl; auto. *)
+(*   - simpl. *)
+(*     rewrite unopEqBool_refl, expEqBool_refl; simpl. *)
+(*     assert (defVarsWellDefined e defVars = true) by admit. *)
+(*     specialize (IHe H). *)
+(*     pose proof (stupidlemma _ _ _ IHe) as [m type_e]. *)
+(*     apply  eqTypeExpression in type_e. *)
+(*     rewrite type_e. *)
+(*     case_eq (expEqBool (Unop u e) e); intros; simpl in H0; rewrite H0. *)
+(*     + admit. *)
+(*     + apply eqTypeExpression in type_e; rewrite type_e. *)
+(*       rewrite mTypeEqBool_refl; simpl. *)
+(*       eapply Gamma_strengthening. *)
+(*       Focus 2. eapply IHe. *)
+(*       intros e0 m0 type_e0. *)