Module NormaliseSpec

Require Import Coqlib.
Require Import Axioms.
Require Import Bool.
Require Import ZArith.
Require Import Psatz.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import AST.
Require Import Utf8.
Require Import Values_symbolictype.
Open Scope Z_scope.
Open Scope list_scope.
Require Import IntFacts.

Definition in_bound (o:Z) (itv: Z * Z) : Prop :=
  fst itv <= o /\ o < snd itv.

Lemma in_bound_dec:
  forall b o,
    in_bound o b \/ ~ in_bound o b.
Proof.
  intros.
  unfold in_bound; destruct b; simpl.
  destruct (zle z o);
    destruct (zlt o z0); try omega.
Qed.

The result of a normalisation is "good" if it is of the correct type, and, if it is a pointer, then it must be a valid pointer

Definition good_result (bound: block -> (Z*Z)) (e:expr_sym) (v : val) (r: result) : Prop :=
  match v, r with
    | Vundef , _ => True
    | Vint _ , Int => True
    | Vlong _ , Long => True
    | Vfloat _ , Float => True
    | Vsingle _ , Single => True
    | Vptr b i , Ptr =>
      in_bound (Int.unsigned i) (bound b)
    | _ , _ => False
  end.

Definition typ_of_result (r:result) : styp :=
  match r with
    | Int => Tint
    | Long => Tlong
    | Float => Tfloat
    | Single => Tsingle
    | Ptr => Tint
  end.

Casting low-level values to various types.
Definition cast (t:styp) (v:lval) : lval :=
  match t, v with
    | Tint , Vi _ => v
    | Tint, Vl l => Vi (Int.repr (Int64.unsigned l))
    | Tint, Vf l => Vi (Float32.to_bits (Float.to_single l))
    | Tint, Vs l => Vi (Float32.to_bits l)

    | Tlong, Vi l => Vl (Int64.repr (Int.unsigned l))
    | Tlong, Vf l => Vl (Float.to_bits l)
    | Tlong, Vs l => Vl (Float.to_bits (Float.of_single l))
    | Tlong , Vl _ => v

    | Tfloat, Vi i => Vf (Float.of_single (Float32.of_bits i))
    | Tfloat, Vl l => Vf (Float.of_bits l)
    | Tfloat, Vf _ => v
    | Tfloat, Vs s => Vf (Float.of_single s)

    | Tsingle, Vs _ => v
    | Tsingle, Vi i => Vs (Float32.of_bits i)
    | Tsingle, Vl l => Vs (Float.to_single (Float.of_bits l))
    | Tsingle, Vf f => Vs (Float.to_single f)
  end.

Lemma wt_lval_cast_id :
  forall t v,
    wt_lval v t ->
    cast t v = v.
Proof.
  intros.
  destruct v ; destruct t ; simpl in *; intuition try congruence.
Qed.

Lemma wt_cast:
  forall t v,
    wt_lval (cast t v) t.
Proof.
des t; des v. Qed.

Lemma cast_cast : forall t v, cast t (cast t v) = cast t v.
Proof.
des v; des t. Qed.

Section Ops.
This section defines a mapping from symbolic expressions operators to functions on values, so that we can evaluate symbolic expressions (see eSexpr below)

The type of concrete memories, i.e. mappings from block identifier to 32-bit addresses.

  Definition mem := block -> int.

  Definition boolval_t (t : styp) := Val.boolval.

  Definition notbool_t (t : styp) := Val.notbool.

  Definition neg_t (t:styp) :=
    match t with
      | Tint => Val.neg
      | Tlong => Val.negl
      | Tfloat => Val.negf
      | Tsingle => Val.negfs
    end.

  Definition and_t (t t':styp) :=
    match t with
      | Tint => Val.and
      | Tlong => Val.andl
      | _ => (fun _ _ => Vundef)
    end.

  Definition or_t (t t':styp) :=
    match t with
      | Tint => Val.or
      | Tlong => Val.orl
      | _ => (fun _ _ => Vundef)
    end.

  Definition xor_t (t t':styp) :=
    match t with
      | Tint => Val.xor
      | Tlong => Val.xorl
      | _ => (fun _ _ => Vundef)
    end.

  Definition not_t (t:styp) :=
    match t with
      | Tint => Val.notint
      | Tlong => Val.notl
      | _ => (fun _ => Vundef)
    end.

  Definition add_t (t t':styp) :=
    match t with
      | Tint => Val.add
      | Tlong => Val.addl
      | Tfloat => Val.addf
      | Tsingle => Val.addfs
    end.

  Definition sub_t (t t':styp) :=
    match t with
      | Tint => Val.sub
      | Tlong => Val.subl
      | Tfloat => Val.subf
      | Tsingle => Val.subfs
    end.

  Definition mul_t (t t':styp) :=
    match t with
      | Tint => Val.mul
      | Tlong => Val.mull
      | Tfloat => Val.mulf
      | Tsingle => Val.mulfs
    end.

  Definition div_t (s:se_signedness) (t t': styp) :=
    match s, t with
      | SESigned, Tint => fun v v' => Val.maketotal (Val.divs v v')
      | SESigned, Tlong => fun v v' => Val.maketotal (Val.divls v v')
      | SEUnsigned, Tint => fun v v' => Val.maketotal (Val.divu v v')
      | SEUnsigned, Tlong => fun v v' => Val.maketotal (Val.divlu v v')
      | _,Tfloat => Val.divf
      | _,Tsingle => Val.divfs
    end.

  Definition mod_t (s:se_signedness) (t t':styp) :=
    match s, t with
      | SESigned, Tint => fun v v' => Val.maketotal (Val.mods v v')
      | SESigned, Tlong => fun v v' => Val.maketotal (Val.modls v v')
      | SEUnsigned, Tint => fun v v' => Val.maketotal (Val.modu v v')
      | SEUnsigned, Tlong => fun v v' => Val.maketotal (Val.modlu v v')
      | _ , _ => (fun _ _ => Vundef)
    end.
  
  Definition shr_t (s:se_signedness) (t t2:styp) :=
    match s, t, t2 with
      | SESigned, Tint, Tint => Val.shr
      | SESigned, Tlong, Tint => Val.shrl
      | SEUnsigned, Tint, Tint => Val.shru
      | SEUnsigned, Tlong, Tint => Val.shrlu
      | _ , _ , _ => (fun _ _ => Vundef)
    end.

  Definition shl_t (t t2:styp) :=
    match t,t2 with
      | Tint,Tint => Val.shl
      | Tlong,Tint => Val.shll
      | _,_ => (fun _ _ => Vundef)
    end.

  Definition cmpu_bool (c: comparison) (v1 v2: val): option bool :=
    match v1, v2 with
      | Vint n1, Vint n2 =>
        Some (Int.cmpu c n1 n2)
      | _ , _ => None
    end.

  Definition cmp_t (s:se_signedness) (c:comparison) (t t':styp) :=
    match s, t with
      | SESigned , Tint => (fun x y => Val.of_optbool (Val.cmp_bool c x y))
      | SESigned , Tlong => (fun x y => Val.of_optbool (Val.cmpl_bool c x y))
      | SEUnsigned , Tint => (fun x y => Val.of_optbool (cmpu_bool c x y))
      | SEUnsigned , Tlong => (fun x y => Val.of_optbool (Val.cmplu_bool c x y))
      | _ , Tfloat => (fun x y => Val.of_optbool (Val.cmpf_bool c x y))
      | _ , Tsingle => (fun x y => Val.of_optbool (Val.cmpfs_bool c x y))
    end.
  
  Definition zeroext_t (z:Z) (t:styp) :=
    match t with
      | Tint => Val.zero_ext z
      | Tlong => (fun v => match v with Vlong l => Vlong (Int64.zero_ext z l) | _ => Vundef end)
      | _ => (fun _ => Vundef)
    end.

  Definition signext_t (z:Z) (t:styp) :=
    match t with
      | Tint => Val.sign_ext z
      | Tlong => (fun v => match v with Vlong l => Vlong (Int64.sign_ext z l) | _ => Vundef end)
      | _ => (fun _ => Vundef)
    end.

  Definition shrx_t (t t':styp) :=
    match t with
      | Tint => fun x y => Val.maketotal (Val.shrx x y)
      | Tlong => (fun _ _ => Vundef)
      | _ => (fun _ _ => Vundef)
    end.

  Definition shr_carry_t (t t':styp) :=
    match t with
      | Tint => Val.shr_carry
      | Tlong => (fun _ _ => Vundef)
      | _ => (fun _ _ => Vundef)
    end.

  Definition rolm_t (amount mask : int) (t:styp) :=
    match t with
      | Tint => (fun x => Val.rolm x amount mask)
      | Tlong => (fun _ => Vundef)
      | _ => (fun _ => Vundef)
    end.

  Definition ror_t (t t':styp) :=
    match t with
      | Tint => Val.ror
      | Tlong => (fun _ _ => Vundef)
      | _ => (fun _ _ => Vundef)
    end.

  Definition absf_t (t:styp) :=
    match t with
      | Tfloat => Val.absf
      | Tsingle => Val.absfs
      | _ => (fun _ => Vundef)
    end.

  Definition mull'_t (t t':styp) :=
    match t with
      | Tint => Val.mull'
      | _ => (fun _ _ => Vundef)
    end.

  Definition mulh_t (s:se_signedness) (t t':styp) :=
    match t with
      | Tint =>
        match s with
            SESigned => Val.mulhs
          | SEUnsigned => Val.mulhu
        end
      | _ => (fun _ _ => Vundef)
    end.

  Definition convert_t (from_s:se_signedness) (to_ts : styp * se_signedness) (from_t:styp) :=
    match (from_t, from_s), to_ts with
      | (Tint, _), (Tint, _) => fun x => x
      | (Tint,SESigned) , ( Tfloat,_) => fun x => Val.maketotal (Val.floatofint x)
      | (Tint,SEUnsigned) , ( Tfloat,_) => fun x => Val.maketotal (Val.floatofintu x)
      | (Tint,SESigned), (Tlong, _ ) => Val.longofint
      | (Tint,SEUnsigned), (Tlong, _ ) => Val.longofintu
      | (Tint,SESigned) , ( Tsingle,_) => fun x => Val.singleoffloat (Val.maketotal (Val.floatofint x))
      | (Tint,SEUnsigned) , ( Tsingle,_) => fun x => Val.singleoffloat (Val.maketotal (Val.floatofintu x))

      | (Tfloat, _) , (Tint,SESigned) => fun x => Val.maketotal (Val.intoffloat x)
      | (Tfloat, _) , (Tint,SEUnsigned) => fun x => Val.maketotal (Val.intuoffloat x)
      | (Tfloat,_), (Tfloat, _) => fun x => x
      | (Tfloat,_) , (Tlong,SESigned) => fun x => Val.maketotal (Val.longoffloat x)
      | (Tfloat,_) , (Tlong,SEUnsigned) => fun x => Val.maketotal (Val.longuoffloat x)
      | (Tfloat,_) , (Tsingle,_) => Val.singleoffloat

      | (Tlong, _), (Tint, _) => Val.loword
      | (Tlong,SESigned) , ( Tfloat,_) => fun x => Val.maketotal (Val.floatoflong x)
      | (Tlong,SEUnsigned) , (Tfloat,_) => fun x => Val.maketotal (Val.floatoflongu x)
      | (Tlong, _), (Tlong, _) => fun x => x
      | (Tlong, SESigned), (Tsingle,_) => fun x => Val.maketotal (Val.singleoflong x)
      | (Tlong, SEUnsigned), (Tsingle,_) => fun x => Val.maketotal (Val.singleoflongu x)

      | (Tsingle, _), (Tint, SEUnsigned) => (fun x => Val.maketotal (Val.intuofsingle x))
      | (Tsingle, _), (Tint, SESigned) => (fun x => Val.maketotal (Val.intofsingle x))
      | (Tsingle, _), (Tfloat, _) => Val.floatofsingle
      | (Tsingle, _), (Tlong, SEUnsigned) => (fun x => Val.maketotal (Val.longuofsingle x))
      | (Tsingle, _), (Tlong, SESigned) => (fun x => Val.maketotal (Val.longofsingle x))
      | (Tsingle, _), (Tsingle, _) => fun x => x
    end.
  
  Definition floatofwords_t (t t':styp) :=
    match t with
      | Tint => Val.floatofwords
      | _ => (fun _ _ => Vundef)
    end.

  Definition longofwords_t (t t':styp) :=
    match t with
      | Tint => Val.longofwords
      | _ => (fun _ _ => Vundef)
    end.

  Definition loword_t (t:styp) :=
    match t with
      | Tlong => Val.loword
      | _ => fun _ => Vundef
    end.

  Definition hiword_t (t:styp) :=
    match t with
      | Tlong => Val.hiword
      | _ => fun _ => Vundef
    end.

  Definition bitsofsingle_t (t:styp) :=
    match t with
      | Tsingle =>
        fun v => match v with
                     Vsingle f => Vint (Float32.to_bits f)
                   | _ => Vundef
                 end
      | _ => fun _ => Vundef
    end.

  Definition bitsofdouble_t (t:styp) :=
    match t with
      | Tfloat =>
        fun v => match v with
                     Vfloat f => Vlong (Float.to_bits f)
                   | _ => Vundef
                 end
      | _ => fun _ => Vundef
    end.

  Definition singleofbits_t (t:styp) :=
    match t with
      | Tint =>
        fun v => match v with
                     Vint n => Vsingle (Float32.of_bits n)
                   | _ => Vundef
                 end
      | _ => fun _ => Vundef
    end.

  Definition doubleofbits_t (t:styp) :=
    match t with
      | Tlong =>
        fun v => match v with
                     Vlong n => Vfloat (Float.of_bits n)
                   | _ => Vundef
                 end
      | _ => fun _ => Vundef
    end.


Converting low-level values into values.
  Definition val_of_lval (v:lval) : val :=
    match v with
      | Vi i => Vint i
      | Vl l => Vlong l
      | Vf f => Vfloat f
      | Vs f => Vsingle f
    end.

  Definition val_of_lval_t (t:styp) (v:lval) : val :=
    match t , v with
      | Tint , Vi i => Vint i
      | Tlong, Vl l => Vlong l
      | Tfloat, Vf l => Vfloat l
      | Tsingle, Vs l => Vsingle l
      | _ , _ => Vundef
    end.

  Section S.
    
    Variable m : mem. (* A concrete memory. *)
    Variable env_mem : block -> int -> byte. (* A ``undef'' environment. *)
Arbitrary values for undefined operations (see Values_symbolictype).
    Variable env_undef_binop : binop_t -> styp -> styp -> lval -> lval -> lval.
    Variable env_undef_unop : unop_t -> styp -> lval -> lval.

    Definition sval_of_val (v : val) : sval :=
      match v with
        | Vundef => Eundef xH Int.zero (* we shall not call this with Vundef. *)
        | Vlong v => Elong v
        | Vfloat f => Efloat f
        | Vsingle f => Esingle f
        | Vptr b o => Eptr b o
        | Vint i => Eint i
      end.

    Definition lval_of_val (v : val) : lval :=
      match v with
        | Vundef => Vi Int.zero
        | Vlong v => Vl v
        | Vfloat f => Vf f
        | Vsingle f => Vs f
        | Vptr b o => Vi (Int.add (m b) o)
        | Vint i => Vi i
      end.

    Definition eSval (t : styp) (v:sval) : lval :=
      match v with
        | Eundef p i => cast t (Vi (Int.repr (Byte.unsigned (env_mem p i))))
        | Elong v => cast t (Vl v)
        | Efloat f => cast t (Vf f)
        | Esingle f => cast t (Vs f)
        | Eptr b o => cast t (Vi (Int.add (m b) o))
        | Eint i => cast t (Vi i)
      end.

    Definition eEval (def:lval) (t:styp) (v:val) : lval :=
      match v with
          Vundef => cast t def
        | Vint i => cast t (Vi i)
        | Vlong v => cast t (Vl v)
        | Vfloat f => cast t (Vf f)
        | Vsingle f => cast t (Vs f)
        | Vptr b o => cast t (Vi (Int.add (m b) o))
      end.

    Definition binop (targ targ' tret : styp)
               (f : styp -> styp -> val -> val -> val)
               (feval : styp -> val -> lval)
               (v v' : lval) : lval :=
      let v := val_of_lval_t targ v in
      let v' := val_of_lval_t targ' v' in
      feval tret (f targ targ' v v').

    Definition unop (targ tret : styp) (f : styp -> val -> val)
               (feval : styp -> val -> lval) (v : lval) : lval :=
      let v := val_of_lval_t targ v in
      feval tret (f targ v).

    Definition eunop
               (targ tret : styp)
               (frec : styp -> expr_sym -> lval)
               (feval : styp -> val -> lval)
               (f : styp -> val -> val)
               (e:expr_sym) : lval :=
      let v' := frec targ e in
      unop targ tret f feval v'.

    Definition ebinop
               (targ1 targ2 tret : styp)
               (frec : styp -> expr_sym -> lval)
               (feval : styp -> val -> lval)
               (f : styp -> styp -> val -> val -> val)
               (e1 e2:expr_sym) : lval :=
      let v1 := frec targ1 e1 in
      let v2 := frec targ2 e2 in
      binop targ1 targ2 tret f feval v1 v2.

    Definition fun_of_unop' (u:unop_t) : (styp -> val -> val) :=
      match u with
        | OpBoolval => boolval_t
        | OpNotbool => notbool_t
        | OpNeg => neg_t
        | OpNot => not_t
        | OpZeroext z => zeroext_t z
        | OpSignext z => signext_t z
        | OpRolm i1 i2 => rolm_t i1 i2
        | OpAbsf => absf_t
        | OpConvert sg (ti,sg') => convert_t sg (ti,sg')
        | OpLoword => loword_t
        | OpHiword => hiword_t
        | OpSingleofbits => singleofbits_t
        | OpDoubleofbits => doubleofbits_t
        | OpBitsofsingle => bitsofsingle_t
        | OpBitsofdouble => bitsofdouble_t
      end.

    Definition fun_of_unop (u:unop_t) : (styp -> val -> val) :=
      fun t v =>
        match fun_of_unop' u t v with
          | Vundef => val_of_lval (env_undef_unop u t (lval_of_val v))
          | v' => v'
        end.

    Definition fun_of_binop' (b:binop_t) : (styp -> styp -> val -> val -> val) :=
      match b with
        | OpAnd => and_t
        | OpOr => or_t
        | OpXor => xor_t
        | OpAdd => add_t
        | OpSub => sub_t
        | OpMul => mul_t
        | OpMull' => mull'_t
        | OpMulh s => mulh_t s
        | OpShrx => shrx_t
        | OpShr_carry => shr_carry_t
        | OpRor => ror_t
        | OpFloatofwords => floatofwords_t
        | OpLongofwords => longofwords_t
        | OpDiv sg => div_t sg
        | OpMod sg => mod_t sg
        | OpCmp sg cmp => cmp_t sg cmp
        | OpShr sg => shr_t sg
        | OpShl => shl_t
      end.

    Definition fun_of_binop (b:binop_t) : (styp -> styp -> val -> val -> val) :=
      fun t1 t2 v1 v2 =>
        match fun_of_binop' b t1 t2 v1 v2 with
          | Vundef => val_of_lval (env_undef_binop b t1 t2 (lval_of_val v1) (lval_of_val v2))
          | v' => v'
        end.

Evaluation of symbolic expressions.
    Fixpoint eSexpr (tr:styp) (e : expr_sym) : lval :=
      match e with
        | Eval v => eSval tr v
        | Eunop u t e => eunop t tr eSexpr (eEval (Vi Int.zero)) (fun_of_unop u) e
        | Ebinop b t1 t2 e1 e2 => ebinop t1 t2 tr eSexpr (eEval (Vi Int.zero)) (fun_of_binop b) e1 e2
      end.

    Lemma eSexpr_rew:
      forall (tr:styp) (e : expr_sym),
        eSexpr tr e =
        match e with
          | Eval v => eSval tr v
          | Eunop u t e => eunop t tr eSexpr (eEval (Vi Int.zero)) (fun_of_unop u) e
          | Ebinop b t1 t2 e1 e2 => ebinop t1 t2 tr eSexpr (eEval (Vi Int.zero)) (fun_of_binop b) e1 e2
        end.
Proof.
      destruct e ; reflexivity.
    Qed.

    Inductive eSexprR (t :styp) (e: expr_sym) (v : lval) : Prop :=
    | eSexprRMk : forall (eSexprEval : eSexpr t e = v),
                    eSexprR t e v.

    Lemma eSexprR_mk : forall t e,
                         eSexprR t e (eSexpr t e).
Proof.
      intros.
      econstructor ; eauto.
    Qed.

    Lemma eEval_wt:
      forall v t d,
        wt_lval (eEval d t v) t.
Proof.
des v; des t; des d. Qed.


    Lemma eSval_wt:
      forall v t,
        wt_lval (eSval t v) t.
Proof.
des v; des t. Qed.
    
    Lemma eSexpr_wt :
      forall e t v,
        eSexpr t e = v ->
        wt_lval v t.
Proof.
      induction e; simpl in *; intuition try congruence; inv H.
      des s; des t.
      unfold eunop, unop; simpl.
      apply eEval_wt; auto.
      unfold ebinop, binop; simpl.
      apply eEval_wt; auto.
    Qed.

    Lemma eSexpr_wt':
      forall e t,
        wt_lval (eSexpr t e) t.
Proof.
intros. exact (eSexpr_wt e t (eSexpr t e) eq_refl). Qed.
    
  End S.

End Ops.

Section Compat.

Alloc b is the concrete address where b is allocated
  Variable Alloc : block -> int.

Bound & Alloc are constructed from a CompCert memory. For a non allocated block b, Bound b = (0,0) and Mask b = 0
  Variable Bound : block -> Z * Z.

  Variable Mask : block -> int.

  Infix "∈" := in_bound (at level 80).

  Notation "[ i ]" := (Int.unsigned i).
  Infix "+" := Int.add.
  Infix "&&" := Int.and.

With respect to an axiomatisation of an abstract memory (Bound, Mask), the compat relation states what a compatible memory Alloc must satisfy.
  
  Record compat : Prop :=
    {
      addr_space : forall b o, [o] ∈ (Bound b) ->
                                0 < [ (Alloc b) + o ] < Int.max_unsigned;
      
      overlap : forall b b' o o',
                  b <> b' ->
                  [o] ∈ (Bound b) ->
                  [o'] ∈ (Bound b') ->
                  [(Alloc b) + o] <> [(Alloc b') + o'];
      
      alignment : forall b, (Alloc b) && (Mask b) = Alloc b
                                                           
    }.
  
End Compat.


Decidability of the existence of a compatible concrete memory.
Axiom ex_alloc_dec : forall bound align,
                       (exists alloc, compat alloc bound align) \/
                       (~exists alloc, compat alloc bound align).


The type of a normalisation function. It takes four parameters:

Definition norm_typ := (block -> Z * Z) -> (block -> int) -> expr_sym -> result -> val.

Module IsNorm.

  Section NormSpec.
    
    Variable eu : unop_t -> styp -> lval -> lval.
    Variable Hwt_eu: wt_eu eu.
    Variable eb : binop_t -> styp -> styp -> lval -> lval -> lval.
    Variable Hwt_eb: wt_eb eb.

A value v is a correct normalisation of the expression e if: - if e is of type r, then v and e should evaluate the same; - v must be a ``good result'' for e and r; - if e is not of type r, then v is Vundef; - if there does not exists any compatible concrete memory, v is Vundef.
    
    Record t
           
           (bound : block -> Z * Z)
           (align : block -> int)
           (e:expr_sym) (r : result) (v:val) : Prop :=
      Mk
        {
          eval_ok :
            tcheck_expr e = Some (typ_of_result r) ->
            forall alloc em v',
              compat alloc bound align ->
              eSexprR alloc em eb eu (typ_of_result r) e v' ->
              exists v'',
                eEval alloc v'' (typ_of_result r) v = v';
          result_wt :
            good_result bound e v r;
          expr_wt:
            tcheck_expr e <> Some (typ_of_result r) ->
            v = Vundef;
          no_alloc_undef:
            ~ (exists alloc, compat alloc bound align) ->
            v = Vundef
        }.

  End NormSpec.

End IsNorm.


Module IsNorm2.


  Section NormSpec.

    Variable eu : unop_t -> styp -> lval -> lval.
    Variable Hwt_eu: wt_eu eu.
    Variable eb : binop_t -> styp -> styp -> lval -> lval -> lval.
    Variable Hwt_eb: wt_eb eb.

This specification is (provably, see below) equivalent to the previous one, however it is expressed with functions instead of relations for field eval_ok
    
    Record t
           (bound : block -> Z * Z)
           (align : block -> int)
           (e:expr_sym) (r : result) (v:val) : Prop :=
      Mk
        {
          eval_ok :
            tcheck_expr e = Some (typ_of_result r) ->
            forall alloc,
              compat alloc bound align ->
              v = Vundef \/
              (v <> Vundef /\
               forall em,
                 eSexpr alloc em eb eu (typ_of_result r) e =
                 eEval alloc (Vi Int.zero) (typ_of_result r) v);
          result_wt :
            good_result bound e v r;
          expr_wt:
            tcheck_expr e <> Some (typ_of_result r) ->
            v = Vundef;
          no_alloc_undef:
            ~ (exists alloc, compat alloc bound align) ->
            v = Vundef

        }.
  End NormSpec.

End IsNorm2.

Section NormSpec.
  Variable eu : unop_t -> styp -> lval -> lval.
  Variable eb : binop_t -> styp -> styp -> lval -> lval -> lval.
  Variable Hwt_eu: wt_eu eu.
  Variable Hwt_eb: wt_eb eb.


A normalisation function normalise is correct if it computes values that are correct normalisations.
  
  Definition normalise_correct (normalise : norm_typ) : Prop :=
    forall bound align e r,
      IsNorm.t eu eb bound align e r (normalise bound align e r).

  Lemma is_norm_1_2:
    forall sz msk e r v,
      IsNorm.t eu eb sz msk e r v <-> IsNorm2.t eu eb sz msk e r v.
Proof.
    intros.
    split; intro H; inv H; constructor; auto; intros; eauto.
    - destruct (Val.eq_val_dec v Vundef); auto.
      right.
      split; auto.
      intros.
      specialize (eval_ok H alloc em (eSexpr alloc em eb eu (typ_of_result r) e) H0).
      exploit eval_ok; eauto.
      constructor; auto.
      intros [v'' H'].
      rewrite <- H'.
      des v.
    - specialize (eval_ok H alloc H0).
      destruct eval_ok; subst; simpl.
      + inv H0.
        exists (eSexpr alloc em eb eu (typ_of_result r) e); auto.
        rewrite wt_lval_cast_id; auto.
        inv H1. auto.
        eapply eSexpr_wt; eauto.
      + destruct H2.
        specialize (H3 em).
        inv H1.
        rewrite H3.
        exists (Vi Int.zero); auto.
  Qed.

  Definition normalise_correct2 (normalise : norm_typ) : Prop :=
    forall bound align e r,
      IsNorm2.t eu eb bound align e r (normalise bound align e r).

  Lemma normalise_correct_same :
    forall normalise,
      (normalise_correct normalise <-> normalise_correct2 normalise).
Proof.
    unfold normalise_correct, normalise_correct2.
    split; intros;
    apply is_norm_1_2; apply H; auto.
  Qed.


Vundef is always a correct normalisation.
  Lemma undef_is_correct_norm :
    forall sz msk e r ,
      IsNorm.t eu eb sz msk e r Vundef.
Proof.
    intros.
    constructor; auto.
    intros.
    simpl.
    exists (eSexpr alloc em eb eu (typ_of_result r) e).
    inv H1.
    simpl.
    generalize (eSexpr_wt' alloc em eb eu e (typ_of_result r)).
    intros.
    rewrite wt_lval_cast_id; auto.
    exact I.
  Qed.

  Section Complete.

A given expression e may have two correct normalisations (in the sense of IsNorm.t). However, when there are two different such values, at least one of them is Vundef.

    Variable env_mem : block -> int -> byte.

    Lemma conflict_cases:
      forall bound align e r v1 v2
             (H0:IsNorm.t eu eb bound align e r v1)
             (H2:IsNorm.t eu eb bound align e r v2),
        v1 <> v2 ->
        match v1, v2 with
            Vundef, _ => True
          | _, Vundef => True
          | _, _ => False
        end.
Proof.
      intros bound align e r v1 v2 H0 H2 H.
      apply is_norm_1_2 in H0.
      apply is_norm_1_2 in H2.
      inv H0; inv H2.
      destruct (ex_alloc_dec bound align) as [[al Hal]|Hnal].
      -
        destruct (tcheck_expr_dec e (typ_of_result r)) as [WT|NWT].
        specialize (eval_ok WT al Hal).
        specialize (eval_ok0 WT al Hal).
        destruct eval_ok; subst; auto.
        destruct eval_ok0; subst; auto.
        destruct v1; auto.
        clear expr_wt no_alloc_undef expr_wt0 no_alloc_undef0.
        destruct H0; destruct H1.
        des v1; des v2; des r.
        specialize (H2 env_mem).
        specialize (H3 env_mem).
        rewrite H2 in H3. inv H3. congruence.
        specialize (H2 env_mem).
        specialize (H3 env_mem).
        rewrite H2 in H3. inv H3. congruence.
        specialize (H2 env_mem).
        specialize (H3 env_mem).
        rewrite H2 in H3. inv H3. congruence.
        specialize (H2 env_mem).
        specialize (H3 env_mem).
        rewrite H2 in H3. inv H3. congruence.
        specialize (H2 (fun _ _ => Byte.zero)).
        specialize (H3 (fun _ _ => Byte.zero)).
        rewrite H2 in H3. clear H2 H0 H1.
        destruct Hal.
        destruct (peq b b0).
        +
          subst.
          cut (i = i0).
          intro; subst. congruence.
          apply eq_lval_inj_i in H3.
          {
            generalize (Int.eq_true (Int.add (al b0) i)).
            rewrite H3 at 1.
            rewrite ! (Int.add_commut (al b0)).
            rewrite Int.translate_eq.
            intro.
            generalize (Int.eq_spec i0 i); rewrite H0; auto.
          }
        + generalize (overlap0 b b0 _ _ n result_wt result_wt0).
          apply eq_lval_inj_i in H3.
          generalize (addr_space0 _ _ result_wt).
          generalize (addr_space0 _ _ result_wt0).
          revert H3 H n. clear.
          intros. clear H n.
          unfold Int.max_unsigned in *.
          rewrite H3 in H2.
          apply H2. auto.
        + rewrite expr_wt; auto.
      - rewrite no_alloc_undef; auto.
    Qed.
    
An immediate corollary is that if two values v and v' are correct normalisations of an expression e, and none of them is Vundef, then v = v'.
    
    Lemma is_norm_unique:
      forall bound align e r v v',
        IsNorm.t eu eb bound align e r v ->
        IsNorm.t eu eb bound align e r v' ->
        v <> Vundef -> v' <> Vundef ->
        v = v'.
Proof.
      intros.
      destruct (Val.eq_val_dec v v'); auto.
      generalize (conflict_cases bound align e r v v' H H0 n).
      des v; des v'.
    Qed.

To rule out this non-determinism, we state that whenever we have a choice between Vundef and another value v, we will prefer v.

    Definition normalise_complete (normalise : norm_typ) : Prop :=
      forall bound align e r v,
        IsNorm.t eu eb bound align e r v ->
        Val.lessdef v (normalise bound align e r).

  End Complete.

  Section Normalise.

    Variable norm : norm_typ.
    Variable norm_correct : normalise_correct norm.
    Variable norm_complete : normalise_complete norm.
    Require Import Classical_Prop.

Properties of a correct and complete normalisation function.
    
    Lemma normalise_undef_cases:
      forall sz msk e r,
        norm sz msk e r = Vundef ->
        ~ (exists v, v <> Vundef /\ IsNorm.t eu eb sz msk e r v).
Proof.
      intros.
      intro.
      destruct H0 as [v [NU IN]].
      generalize (norm_complete sz msk e r v IN).
      rewrite H.
      intro A; inv A;
      congruence.
    Qed.

    Lemma is_norm_eq_wt'' :
      forall e e' r bound align
             (WTe': tcheck_expr e' = Some (typ_of_result r)),
        (forall alloc em,
           compat alloc bound align ->
           eSexpr alloc em eb eu (typ_of_result r) e =
           eSexpr alloc em eb eu (typ_of_result r) e') ->
        forall v,
          IsNorm.t eu eb bound align e r v ->
          IsNorm.t eu eb bound align e' r v.
Proof.
      intros.
      destruct H0 ; econstructor ; eauto.
      intros.
      destruct (tcheck_expr_dec e (typ_of_result r)).
      eapply (eval_ok) ; eauto.
      constructor.
      rewrite H; auto.
      inv H2. auto.
      specialize (expr_wt n).
      subst. simpl in *.
      exists v'.
      inv H2.
      apply wt_lval_cast_id.
      apply eSexpr_wt'.
    Qed.

    Lemma lessdef_antisym:
      forall v1 v2,
        Val.lessdef v1 v2 ->
        Val.lessdef v2 v1 ->
        v1 = v2.
Proof.
      intros.
      inv H; inv H0; auto.
    Qed.

    Lemma normalise_eq'' :
      forall e e' r bound align,
        tcheck_expr e = Some (typ_of_result r) ->
        tcheck_expr e' = Some (typ_of_result r) ->
        (forall alloc em,
           compat alloc bound align ->
           eSexpr alloc em eb eu (typ_of_result r) e =
           eSexpr alloc em eb eu (typ_of_result r) e') ->
        norm bound align e r = norm bound align e' r.
Proof.
      intros.
      apply lessdef_antisym.
      {
        apply norm_complete ; auto.
        apply is_norm_eq_wt'' with (e:=e); eauto.
      }
      {
        apply norm_complete ; auto.
        apply is_norm_eq_wt'' with (e:=e'); auto.

        intros; rewrite H1; auto.
      }
    Qed.

    Lemma same_norm :
      forall e1 e2 r bound align
             (HWte1 : tcheck_expr e1 = Some (typ_of_result r))
             (HWte2 : tcheck_expr e2 = Some (typ_of_result r))
             (Hnundef: norm bound align e1 r <> Vundef)
             (Heq : norm bound align e1 r = norm bound align e2 r),
      forall alloc em,
        compat alloc bound align ->
        eSexpr alloc em eb eu (typ_of_result r) e1 =
        eSexpr alloc em eb eu (typ_of_result r) e2.
Proof.
      intros.
      generalize (norm_correct bound align e1 r).
      generalize (norm_correct bound align e2 r).
      intros.
      apply is_norm_1_2 in H0.
      apply is_norm_1_2 in H1.
      inv H0 ; inv H1.
      specialize (eval_ok HWte2 alloc H).
      specialize (eval_ok0 HWte1 alloc H).
      destruct eval_ok; try congruence.
      destruct eval_ok0; try congruence.
      destruct H0; destruct H1.
      rewrite H2; rewrite H3.
      rewrite Heq. auto.
    Qed.
    
    Lemma is_norm_eq_int :
      forall alloc bound align i j
              (Hcompat : compat alloc bound align),
        IsNorm2.t eu eb bound align (Eval (Eint i)) Int (Vint j) -> i = j.
Proof.
      intros.
      destruct H.
      simpl in *.
      apply eval_ok in Hcompat ; eauto.
      des Hcompat.
      apply eq_lval_inj_i; apply H0.
      exact (fun _ _ => Byte.zero).
    Qed.

    Definition expr_of_lval (r : result) (l:lval) :=
      (val_of_lval_t (typ_of_result r) l).


  End Normalise.


End NormSpec.

Ltac clear_useless :=
  repeat
    match goal with
        H: True |- _ => clear H
      | H: ?a = ?a |- _ => clear H
      | H: ?a, H1: ?a |- _ => clear H
    end.

Ltac isGroundType l :=
  match l with
      Tint => idtac
    | Tlong => idtac
    | Tfloat => idtac
    | Tsingle => idtac
    | _ => fail 1
  end.



Ltac destr_and :=
  repeat
    match goal with
        H: ?A /\ ?B |- _ => destruct H
      | H: exists _, _ |- _ => destruct H
    end.


Ltac eSexpr_type_inv H :=
  match type of H with
      eSexpr ?mem ?em ?eb ?eu ?t ?e = ?v =>
      let x := fresh in
      assert (x := eSexpr_wt' mem em eb eu e t v H);
        try (isGroundType t; des v)
  end.

Ltac find_most_nested_match e :=
  match e with
      context [ match ?A with _ => _ end ] => find_most_nested_match A
    | _ => e
  end.

Ltac inv_wt_lval :=
  repeat
    match goal with
        |- wt_lval ?t ?l -> _ =>
        isGroundType l; des t
      | H : wt_lval ?t ?l |- _ =>
        isGroundType l; des t
    end.

Ltac grab_types :=
  match goal with
      |- context [eSexpr ?alloc ?em ?eb ?eu ?t ?e] =>
      match goal with
          H : eSexpr alloc em eb eu t e = ?v |- _ =>
          match v with
              Vi _ => fail 2
            | Vl _ => fail 2
            | Vf _ => fail 2
            | _ =>
              match goal with
                  H1 : wt_lval v ?t1 |- _ => fail 3
                | |- _ =>
                  generalize (eSexpr_wt' alloc em eb eu e t);
                    try (isGroundType t; des v)
              end
          end
      end
    | _ => fail "No matching eSexpr..."
  end.

Ltac inv_types e :=
  match e with
    | eSexpr ?alloc ?wc ?env ?ty ?l ?e' =>
      let x := fresh in
      destruct e eqn:x ;
        eSexpr_type_inv x; auto;
        inv_wt_lval
  end.

Ltac destr_eval :=
  match goal with
      |- ?e => let mnm := find_most_nested_match e in
               inv_types mnm
  end.

Ltac solve_wt :=
  repeat
    match goal with
      | H : wt_expr ?e ?t |- _ => apply tcheck_expr_correct in H
      | |- context [wt_expr ?e ?t] => rewrite <- tcheck_expr_correct; auto
      | H : has_typ ?t ?e = true |-
        context [?e] => rewrite (has_typ_true _ _ H); simpl; auto
      | H : context [tcheck_expr ?e],
            H1 : wt_expr ?e ?t |- _ => apply tcheck_expr_correct in H1; rewrite H1 in H; simpl in H
      | H : tcheck_expr ?e = Some ?t |-
        context [ tcheck_expr ?e ] => rewrite H; simpl; auto
      | |- context [ styp_eq ?t ?t ] => rewrite styp_eq_refl; simpl
      | |- context [ is_lval_typ ?t ] => destruct (is_lval_typ_dec t); simpl; try congruence
    end.


Ltac simpl_int :=
  repeat
    match goal with
      | |- context [Int.eq ?a ?a] => rewrite Int.eq_true; simpl
      | |- context [Int.eq ?a ?b] => replace (Int.eq a b) with false by reflexivity; simpl
      | |- context [Int.ltu ?a ?b] => try replace (Int.ltu a b) with true by reflexivity; simpl
      | _ => progress simpl
    end.

Ltac wt_val_option_map :=
  match goal with
    | |-
      wt_val (Val.maketotal (option_map ?X ?Y)) ?T => destruct Y ; simpl ; auto
  end.


Ltac simpl_eval :=
  repeat
    match goal with
        |- context [ebinop _ _ _ _ _ _ _ _] =>
        unfold ebinop, binop, fun_of_binop, fun_of_binop'; simpl
      | |- context [eunop _ _ _ _ _ _] =>
        unfold eunop, unop, fun_of_unop, fun_of_unop'; simpl
      | |- context [match eSexpr ?alloc ?em ?eu ?eb ?t ?e with _ => _ end] =>
        let x := fresh in
        generalize (eSexpr_wt alloc em eu eb e t (eSexpr alloc em eu eb t e) eq_refl);
          try (isGroundType t; des (eSexpr alloc em eu eb t e))
    end.


Ltac simpl_eval' :=
  repeat
    match goal with
      | H: Vi _ = Vi _ |- _ => inv H
      | |- Vi _ = Vi _ -> _ => let x := fresh in intro x; inv x
      | H: Vl _ = Vl _ |- _ => inv H
      | |- Vl _ = Vl _ -> _ => let x := fresh in intro x; inv x
      | H: Vf _ = Vf _ |- _ => inv H
      | |- Vf _ = Vf _ -> _ => let x := fresh in intro x; inv x
      | H: Vs _ = Vs _ |- _ => inv H
      | |- Vs _ = Vs _ -> _ => let x := fresh in intro x; inv x
      | H: context [ebinop _ _ _ _ _ _ _ _] |- _ => revert H
      | H: context [eunop _ _ _ _ _ _] |- _ => revert H
      | H: context [if Int.ltu _ _ then _ else _] |- _ => revert H; simpl_int
      | |- context [if Int.ltu _ _ then _ else _] => simpl_int
      | |- context [match ?f ?t ?t' (val_of_lval_t ?t (eSexpr ?alloc ?em ?eb ?eu ?t ?e)) ?v2 with _ => _ end] =>
        generalize (eSexpr_wt _ _ _ _ _ _ (eSexpr alloc em eb eu t e) eq_refl);
          des (eSexpr alloc em eb eu t e)
      | |- context [match ?f ?s ?t ?t' (val_of_lval_t ?t (eSexpr ?alloc ?em ?eb ?eu ?t ?e)) ?v2 with _ => _ end] =>
        generalize (eSexpr_wt _ _ _ _ _ _ (eSexpr alloc em eb eu t e) eq_refl);
          des (eSexpr alloc em eb eu t e)
      | |- context [match ?f ?n ?t (val_of_lval_t ?t (eSexpr ?alloc ?em ?eb ?eu ?t ?e)) with _ => _ end] =>
        generalize (eSexpr_wt _ _ _ _ _ _ (eSexpr alloc em eb eu t e) eq_refl);
          des (eSexpr alloc em eb eu t e)
      | |- context [match ?f ?t (val_of_lval_t ?t (eSexpr ?alloc ?em ?eb ?eu ?t ?e)) with _ => _ end] =>
        generalize (eSexpr_wt _ _ _ _ _ _ (eSexpr alloc em eb eu t e) eq_refl);
          des (eSexpr alloc em eb eu t e)
      | |- context [ebinop _ _ _ _ _ _ _ _] =>
        unfold ebinop, binop, fun_of_binop, fun_of_binop'
      | |- context [eunop _ _ _ _ _ _] =>
        unfold eunop, unop, fun_of_unop, fun_of_unop'
      | |- context [match eSexpr ?alloc ?em ?eu ?eb ?t ?e with _ => _ end] =>
        let x := fresh in
        generalize (eSexpr_wt alloc em eu eb e t (eSexpr alloc em eu eb t e) eq_refl);
          try (isGroundType t; des (eSexpr alloc em eu eb t e))
      | H : context [match eSexpr ?alloc ?em ?eu ?eb ?t ?e with _ => _ end] |- _ =>
        let x := fresh in
        generalize (eSexpr_wt alloc em eu eb e t (eSexpr alloc em eu eb t e) eq_refl);
          try (isGroundType t; des (eSexpr alloc em eu eb t e))
      | |- _ => clear_useless
    end.


Lemma expr_long_expr_int:
  forall alloc em
         e3 i4
         (H2 : wt_expr e3 Tlong)
         (Heql5 : eSexpr alloc em eb eu Tlong e3 = Vl i4),
    eSexpr alloc em eb eu Tint e3 = Vi (Int64.loword i4).
Proof.
  induction e3; simpl; auto.
  - des s. inv Heql5. f_equal.
  - intuition try congruence.
    simpl_eval'; des s; des u; try (inv Heql5; auto; fail).
    des p. des s; des s1;
            inv Heql5; auto.
    inv H3.
    des p; des s1; des s;
    inv Heql5; auto.
    des p; des s1; des s.
    + unfold convert_t in *; simpl in *.
      des (Float.to_long f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SESigned (Tlong, SESigned)) Tfloat (Vf f) Tlong eq_refl).
      des ((eu (OpConvert SESigned (Tlong, SESigned)) Tfloat (Vf f))). inv H2; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_long f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SEUnsigned (Tlong, SESigned)) Tfloat (Vf f) Tlong eq_refl).
      des ((eu (OpConvert SEUnsigned (Tlong, SESigned)) Tfloat (Vf f))); inv H2; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_longu f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SESigned (Tlong, SEUnsigned)) Tfloat (Vf f) Tlong eq_refl).
      des ((eu (OpConvert SESigned (Tlong, SEUnsigned)) Tfloat (Vf f))); inv H2; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_longu f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SEUnsigned (Tlong, SEUnsigned)) Tfloat (Vf f) Tlong eq_refl).
      des ((eu (OpConvert SEUnsigned (Tlong, SEUnsigned)) Tfloat (Vf f))); inv H2; simpl; auto.
    + unfold convert_t in *. des p; des s1; des s.
      * des (Float32.to_long f). inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SESigned (Tlong, SESigned)) Tsingle (Vs f) _ eq_refl).
        des ((eu (OpConvert SESigned (Tlong, SESigned)) Tsingle (Vs f))). inv Heql5; simpl; auto.
      * des (Float32.to_long f). inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SEUnsigned (Tlong, SESigned)) Tsingle (Vs f) _ eq_refl).
        des ((eu (OpConvert SEUnsigned (Tlong, SESigned)) Tsingle (Vs f)));
          inv Heql5; simpl; auto.
      * des (Float32.to_longu f). inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SESigned (Tlong, SEUnsigned)) Tsingle (Vs f) _ eq_refl).
        des ((eu (OpConvert SESigned (Tlong, SEUnsigned)) Tsingle (Vs f))). inv Heql5; simpl; auto.
      * des (Float32.to_longu f). inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SEUnsigned (Tlong, SEUnsigned)) Tsingle (Vs f) _ eq_refl).
        des ((eu (OpConvert SEUnsigned (Tlong, SEUnsigned)) Tsingle (Vs f)));
          inv Heql5; simpl; auto.
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tlong _ eq_refl).
    des (eSexpr alloc em eb eu Tlong e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tlong _ eq_refl).
    des (eSexpr alloc em eb eu Tlong e3_2).
    simpl_eval'; des s; des s0; des b;
    repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    simpl in *; inv Heql5; auto.
    + generalize (Hwt_eb (OpShr s) Tlong Tint (Vl i2) (Vi i0) Tlong eq_refl).
      des (eb (OpShr s) Tlong Tint (Vl i2) (Vi i0));
        des s; destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpShl) Tlong Tint (Vl i2) (Vi i0) Tlong eq_refl).
      des (eb (OpShl) Tlong Tint (Vl i2) (Vi i0));
        destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpDiv s) Tlong Tlong (Vl i2) (Vl i1) Tlong eq_refl).
      des (eb (OpDiv s) Tlong Tlong (Vl i2) (Vl i1));
        des s; destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpMod s) Tlong Tlong (Vl i2) (Vl i1) Tlong eq_refl).
      des (eb (OpMod s) Tlong Tlong (Vl i2) (Vl i1));
        des s; destr; inv H6; simpl; auto.
Qed.

Lemma expr_int_expr_long:
  forall alloc em
         e3 i4
         (H2 : wt_expr e3 Tint)
         (Heql5 : eSexpr alloc em eb eu Tint e3 = Vi i4),
    eSexpr alloc em eb eu Tlong e3 = Vl (Int64.repr (Int.unsigned i4)).
Proof.
  induction e3; simpl; intros.
  - des s.
  - intuition try congruence.
    simpl_eval'; des s; des u; try (inv Heql5; auto; fail).
    des (Int.eq i Int.zero).
    des (Int.eq i Int.zero).
    inv H3.
    des p; des s1; des s;
    inv Heql5; auto.
    des p; des s1; des s;
    inv Heql5; auto.
    des p;des s1; des s.
    + unfold convert_t in *; simpl in *.
      des (Float.to_int f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SESigned (Tint, SESigned)) Tfloat (Vf f) Tint eq_refl).
      des ((eu (OpConvert SESigned (Tint, SESigned)) Tfloat (Vf f))); inv H3; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_int f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SEUnsigned (Tint, SESigned)) Tfloat (Vf f) Tint eq_refl).
      des ((eu (OpConvert SEUnsigned (Tint, SESigned)) Tfloat (Vf f))); inv H3; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_intu f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SESigned (Tint, SEUnsigned)) Tfloat (Vf f) Tint eq_refl).
      des ((eu (OpConvert SESigned (Tint, SEUnsigned)) Tfloat (Vf f))); inv H3; simpl; auto.
    + unfold convert_t in *; simpl in *.
      des (Float.to_intu f); inv Heql5; auto.
      generalize (Hwt_eu (OpConvert SEUnsigned (Tint, SEUnsigned)) Tfloat (Vf f) Tint eq_refl).
      des ((eu (OpConvert SEUnsigned (Tint, SEUnsigned)) Tfloat (Vf f))); inv H3; simpl; auto.
    + des p;des s1; des s; unfold convert_t in *; simpl in *.
      * des (Float32.to_int f); inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SESigned (Tint, SESigned)) Tsingle (Vs f) Tint eq_refl).
        des ((eu (OpConvert SESigned (Tint, SESigned)) Tsingle (Vs f))); inv H2; simpl; auto.
      * unfold convert_t in *; simpl in *.
        des (Float32.to_int f); inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SEUnsigned (Tint, SESigned)) Tsingle (Vs f) Tint eq_refl).
        des ((eu (OpConvert SEUnsigned (Tint, SESigned)) Tsingle (Vs f))); inv H2; simpl; auto.
      * unfold convert_t in *; simpl in *.
        des (Float32.to_intu f); inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SESigned (Tint, SEUnsigned)) Tsingle (Vs f) Tint eq_refl).
        des ((eu (OpConvert SESigned (Tint, SEUnsigned)) Tsingle (Vs f))); inv H2; simpl; auto.
      * unfold convert_t in *; simpl in *.
        des (Float32.to_intu f); inv Heql5; auto.
        generalize (Hwt_eu (OpConvert SEUnsigned (Tint, SEUnsigned)) Tsingle (Vs f) Tint eq_refl).
        des ((eu (OpConvert SEUnsigned (Tint, SEUnsigned)) Tsingle (Vs f))); inv H2; simpl; auto.
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tlong _ eq_refl).
    des (eSexpr alloc em eb eu Tlong e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tlong _ eq_refl).
    des (eSexpr alloc em eb eu Tlong e3_2).
    simpl_eval'; des s; des s0; des b;
    repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    simpl in *; inv Heql5; auto.
    + destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpShrx) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpShrx) Tint Tint (Vi i2) (Vi i0));
        destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpShr_carry) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpShr_carry) Tint Tint (Vi i2) (Vi i0));
        destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpRor) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpRor) Tint Tint (Vi i2) (Vi i0));
        destr; inv H6; simpl; auto.
    + generalize (Hwt_eb (OpDiv s) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpDiv s) Tint Tint (Vi i2) (Vi i0));
        des s; destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpMod s) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpMod s) Tint Tint (Vi i2) (Vi i0));
        des s; destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpCmp s c) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpCmp s c) Tint Tint (Vi i2) (Vi i0));
        des s; destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpShr s) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpShr s) Tint Tint (Vi i2) (Vi i0));
        des s; destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpShl) Tint Tint (Vi i2) (Vi i0) Tint eq_refl).
      des (eb (OpShl) Tint Tint (Vi i2) (Vi i0));
        destr; inv H4; simpl; auto.
    + generalize (Hwt_eb (OpCmp s c) Tlong Tlong (Vl i2) (Vl i1) Tint eq_refl).
      des (eb (OpCmp s c) Tlong Tlong (Vl i2) (Vl i1));
        des s; destr; inv H4; simpl; auto.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tfloat _ eq_refl).
      des (eSexpr alloc em eb eu Tfloat e3_2).
      generalize (Hwt_eb (OpCmp s c) Tfloat Tfloat (Vf f) (Vf f0) Tint eq_refl).
      des (eb (OpCmp s c) Tfloat Tfloat (Vf f) (Vf f0));
        des s; destr; inv H4; simpl; auto.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tsingle _ eq_refl).
      des (eSexpr alloc em eb eu Tsingle e3_2).
      generalize (Hwt_eb (OpCmp s c) Tsingle Tsingle (Vs f) (Vs f0) Tint eq_refl).
      des (eb (OpCmp s c) Tsingle Tsingle (Vs f) (Vs f0));
        des s; destr; inv H4; simpl; auto.
Qed.

Lemma expr_float_expr_int:
  forall alloc em e3 f
         (H : wt_expr e3 Tfloat)
         (Heql5 : eSexpr alloc em eb eu Tfloat e3 = Vf f),
    eSexpr alloc em eb eu Tint e3 = Vi (Float32.to_bits (Float.to_single f)).
Proof.
  induction e3; simpl; auto.
  - des s.
  - intuition try congruence.
    simpl_eval'; des s; des u.
    des p; des s1; des s.
    des p; des s; des t; des s0.
    inv H3.
    inv H3.
    inv H3.
    des p; des t; des s0; des s.
    des p.
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tfloat _ eq_refl).
    des (eSexpr alloc em eb eu Tfloat e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tfloat _ eq_refl).
    des (eSexpr alloc em eb eu Tfloat e3_2).
    simpl_eval'; des s; des s0; des b;
    repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    repeat match goal with
               H: is_lval_typ Tfloat |- _ => inv H
           end.
    simpl in Heql5;inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    des s.
Qed.


Lemma fun_of_unop_wt:
  forall l s0 s u alloc,
    wt_lval l s0 ->
    Some s = tcheck_unop u s0 ->
    tcheck_lval (lval_of_val alloc (fun_of_unop alloc eu u s0 (val_of_lval_t s0 l))) = s.
Proof.
  unfold fun_of_unop, fun_of_unop'.
  intros. symmetry in H0.
  generalize (Hwt_eu u s0 (lval_of_val alloc (val_of_lval_t s0 l)) _ H0).
  des (eu u s0 (lval_of_val alloc (val_of_lval_t s0 l))); des l; des s; des s0;
  try (des u;
       try (destruct (Int.eq _); destr; unfold Vfalse, Vtrue in *; destr; fail);
       try (destruct (Int.eq _); destr; unfold Vfalse, Vtrue in *; destr; fail);
       try (des p; inv H0; des s; try (des s1; fail)));
  try (des s1; unfold convert_t; simpl;
       match goal with
           |- context [Val.maketotal (option_map _ ?v)] => des v
       end).
Qed.


Lemma fun_of_binop_wt:
  forall l l0 s0 s1 s b alloc,
    wt_lval l s0 ->
    wt_lval l0 s1 ->
    Some s = tcheck_binop b s0 s1 ->
    tcheck_lval (lval_of_val alloc
                             (fun_of_binop alloc eb b s0 s1 (val_of_lval_t s0 l)
                                           (val_of_lval_t s1 l0))) = s.
Proof.
  unfold fun_of_binop, fun_of_binop'.
  intros. symmetry in H1.
  generalize (Hwt_eb b s0 s1 (lval_of_val alloc (val_of_lval_t s0 l)) (lval_of_val alloc (val_of_lval_t s1 l0)) _ H1).
  des (eb b s0 s1 (lval_of_val alloc (val_of_lval_t s0 l))
          (lval_of_val alloc (val_of_lval_t s1 l0))); des l; des l0; des s; des s0; des s1;
  des b; try (destr; fail);
  try (des s; destr; fail).
Qed.


Lemma expr_int_expr_single:
  forall alloc em e3 i
         (H : tcheck_expr e3 = Some Tint)
         (Heql5 : eSexpr alloc em eb eu Tint e3 = Vi i),
    eSexpr alloc em eb eu Tsingle e3 = Vs (Float32.of_bits i).
Proof.
  induction e3; simpl; auto.
  - des s.
  - intuition try congruence.
    des (tcheck_expr e3).
    des (styp_eq s s0).
    generalize (eSexpr_wt alloc em eb eu e3 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3).
    des u; des s0; simpl in *; simpl_eval'.
    + destruct (Int.eq i0 Int.zero); simpl in *; inv Heql5; auto.
    + destruct (Int.eq i0 Int.zero); simpl in *; inv Heql5; auto.
    + rewrite Heql; simpl; auto; intro A; inv A; auto.
    + des p; des s0; des s1; des s.
    + des p; des s0; des s1; des s.
    + des p.
      generalize (Hwt_eu (OpConvert s (s0, s1)) Tfloat (Vf f) _ eq_refl).
      des (eu (OpConvert s (s0, s1)) Tfloat (Vf f)); des s0.
      unfold convert_t in *.
      des s1.
      destruct (Float.to_int f); simpl in *; inv Heql5; auto.
      destruct (Float.to_intu f); simpl in *; inv Heql5; auto.
    + des p.
      generalize (Hwt_eu (OpConvert s (s0, s1)) Tsingle (Vs f) _ eq_refl).
      des (eu (OpConvert s (s0, s1)) Tsingle (Vs f)); des s0.
      unfold convert_t in *.
      des s1.
      destruct (Float32.to_int f); simpl in *; inv Heql5; auto.
      destruct (Float32.to_intu f); simpl in *; inv Heql5; auto.
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tsingle _ eq_refl).
    des (eSexpr alloc em eb eu Tsingle e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tsingle _ eq_refl).
    des (eSexpr alloc em eb eu Tsingle e3_2).
    des (tcheck_expr e3_1).
    des (styp_eq s s1).
    des (tcheck_expr e3_2).
    des (styp_eq s0 s).
    unfold ebinop, binop, fun_of_binop, fun_of_binop'.
    assert (WTEB:= Hwt_eb b s1 s (lval_of_val alloc (val_of_lval_t s1 (eSexpr alloc em eb eu s1 e3_1)))
                          (lval_of_val alloc (val_of_lval_t s (eSexpr alloc em eb eu s e3_2)))).
    simpl_eval'; des s1; des s; des b; repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    simpl in *; inv Heql5; auto;
    simpl in *.
    Ltac apply_eb WTEB :=
      repeat match goal with
                 |- context [ (eb ?o ?t ?s ?v ?w)] => specialize (WTEB _ eq_refl);
                   des (eb o t s v w)
             end.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + des s; des c; destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tlong _ eq_refl).
      des (eSexpr alloc em eb eu Tlong e3_2).
      des s; des c;destr.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tfloat _ eq_refl).
      des (eSexpr alloc em eb eu Tfloat e3_2).
      des s; des c;destr.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tsingle _ eq_refl).
      des (eSexpr alloc em eb eu Tsingle e3_2).
      des s; des c;destr.
Qed.


Lemma expr_int_expr_float:
  forall alloc em e3 i
         (H : tcheck_expr e3 = Some Tint)
         (Heql5 : eSexpr alloc em eb eu Tint e3 = Vi i),
    eSexpr alloc em eb eu Tfloat e3 = Vf (Float.of_single (Float32.of_bits i)).
Proof.
  induction e3; simpl; auto.
  - des s.
  - intuition try congruence.
    des (tcheck_expr e3).
    des (styp_eq s s0).
    generalize (eSexpr_wt alloc em eb eu e3 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3).
    des u; des s0; simpl in *; simpl_eval'.
    + destruct (Int.eq i0 Int.zero); simpl in *; inv Heql5; auto.
    + destruct (Int.eq i0 Int.zero); simpl in *; inv Heql5; auto.
    + rewrite Heql; simpl; auto; intro A; inv A; auto.
    + des p; des s0; des s1; des s.
    + des p; des s0; des s1; des s.
    + des p.
      generalize (Hwt_eu (OpConvert s (s0, s1)) Tfloat (Vf f) _ eq_refl).
      des (eu (OpConvert s (s0, s1)) Tfloat (Vf f)); des s0.
      unfold convert_t in *.
      des s1.
      destruct (Float.to_int f); simpl in *; inv Heql5; auto.
      destruct (Float.to_intu f); simpl in *; inv Heql5; auto.
    + des p.
      generalize (Hwt_eu (OpConvert s (s0, s1)) Tsingle (Vs f) _ eq_refl).
      des (eu (OpConvert s (s0, s1)) Tsingle (Vs f)); des s0.
      unfold convert_t in *.
      des s1.
      destruct (Float32.to_int f); simpl in *; inv Heql5; auto.
      destruct (Float32.to_intu f); simpl in *; inv Heql5; auto.
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tsingle _ eq_refl).
    des (eSexpr alloc em eb eu Tsingle e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tsingle _ eq_refl).
    des (eSexpr alloc em eb eu Tsingle e3_2).
    des (tcheck_expr e3_1).
    des (styp_eq s s1).
    des (tcheck_expr e3_2).
    des (styp_eq s0 s).
    unfold ebinop, binop, fun_of_binop, fun_of_binop'.
    assert (WTEB:= Hwt_eb b s1 s (lval_of_val alloc (val_of_lval_t s1 (eSexpr alloc em eb eu s1 e3_1)))
                          (lval_of_val alloc (val_of_lval_t s (eSexpr alloc em eb eu s e3_2)))).
    simpl_eval'; des s1; des s; des b; repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    simpl in *; inv Heql5; auto;
    simpl in *.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + des s; des c; destr; apply_eb WTEB.
    + des s; destr; apply_eb WTEB.
    + destr; apply_eb WTEB.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tlong _ eq_refl).
      des (eSexpr alloc em eb eu Tlong e3_2).
      des s; des c;destr.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tfloat _ eq_refl).
      des (eSexpr alloc em eb eu Tfloat e3_2).
      des s; des c;destr.
    + generalize (eSexpr_wt alloc em eb eu e3_2 Tsingle _ eq_refl).
      des (eSexpr alloc em eb eu Tsingle e3_2).
      des s; des c;destr.
Qed.



Ltac inv_eu :=
  match goal with
      |- context [eu ?op ?t ?l] => generalize (Hwt_eu op t l _ eq_refl); des (eu op t l)
  end.


Ltac inv_eb :=
  match goal with
      |- context [eb ?op ?t ?s ?l ?k] => generalize (Hwt_eb op t s l k _ eq_refl); des (eb op t s l k)
  end.

Lemma expr_float_expr_long:
  forall alloc em e3 f
         (H : wt_expr e3 Tfloat)
         (Heql5 : eSexpr alloc em eb eu Tfloat e3 = Vf f),
    eSexpr alloc em eb eu Tlong e3 = Vl (Float.to_bits f).
Proof.
  induction e3; simpl; auto.
  - destruct s; simpl in *; intuition try congruence.
  - intuition try congruence.
    simpl_eval'; des s; des u.
    des p; des s; des s1.
    des p; des s; des t; des s0.
    inv H3.
    inv H3.
    inv H3.
    des p; des t; des s0; des s.
    des p; des s; des s1; inv_eu.
    
  - intuition try congruence.
    generalize (eSexpr_wt alloc em eb eu e3_1 Tfloat _ eq_refl).
    des (eSexpr alloc em eb eu Tfloat e3_1).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tint _ eq_refl).
    des (eSexpr alloc em eb eu Tint e3_2).
    generalize (eSexpr_wt alloc em eb eu e3_2 Tfloat _ eq_refl).
    des (eSexpr alloc em eb eu Tfloat e3_2).

    simpl_eval'; des s; des s0; des b;
    repeat rewrite Heql0 in *;
    repeat rewrite Heql1 in *;
    repeat match goal with
               H: is_lval_typ Tfloat |- _ => inv H
             | H: is_lval_typ Tsingle |- _ => inv H
           end.
    
    simpl in Heql5;inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    simpl in Heql5; inv Heql5; auto.
    des s.
Qed.


Ltac solve_wt_undef :=
  match goal with
      |- context [eb ?op ?t1 ?t2 ?v1 ?v2] =>
      generalize (Hwt_eb op t1 t2 v1 v2 _ eq_refl);
        destruct (eb op t1 t2 v1 v2); simpl in *; intro; try intuition congruence
    | |- context [eu ?op ?t ?v] =>
      generalize (Hwt_eu op t v _ eq_refl);
        destruct (eu op t v); simpl in *; intro; try intuition congruence
  end.


Ltac unfold_eval :=
  repeat (unfold ebinop, binop,
          fun_of_binop, fun_of_binop',
          eunop, unop,
          fun_of_unop, fun_of_unop'; simpl).


Ltac inv_expr_type e :=
  generalize (eSexpr_wt _ _ _ _ _ _ e eq_refl); des e.

Lemma expr_long_expr_float:
  forall alloc em v l,
    tcheck_expr v = Some Tlong ->
    eSexpr alloc em eb eu Tlong v = Vl l ->
    eSexpr alloc em eb eu Tfloat v = Vf (Float.of_bits l).
Proof.
  induction v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - clear IHv. destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      unfold convert_t in *.
      destruct s1; simpl in *.
      destruct (Float.to_long f) eqn:?; simpl in *.
      inv H1; auto.
      solve_wt_undef.
      destruct (Float.to_longu f) eqn:?; simpl in *.
      inv H1; auto.
      solve_wt_undef.

    + destruct p; simpl in *; inv H.
      unfold convert_t in *.
      destruct s1.
      * destruct (Values.Val.longofsingle (Vsingle f)) eqn:?; simpl in *.
        destruct (Float32.to_long f) eqn:?; simpl in *; try discriminate.
        inv Heqo0; simpl in *.
        inv H1; auto.
        solve_wt_undef.
      * destruct (Values.Val.longuofsingle (Vsingle f)) eqn:?; simpl in *.
        destruct (Float32.to_longu f) eqn:?; simpl in *; try discriminate.
        inv Heqo0; simpl in *.
        inv H1; auto.
        solve_wt_undef.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + inv_expr_type (eSexpr alloc em eb eu Tint v2).
      destr_cond_match; simpl in *;
      inv H2; auto;
      solve_wt_undef.
Qed.


Lemma expr_long_expr_single:
  forall alloc em v l,
    tcheck_expr v = Some Tlong ->
    eSexpr alloc em eb eu Tlong v = Vl l ->
    eSexpr alloc em eb eu Tsingle v = Vs (Float.to_single (Float.of_bits l)).
Proof.
  destruct v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      unfold convert_t in *.
      destruct s1; simpl in *.
      destruct (Float.to_long f) eqn:?; simpl in *.
      inv H1; auto.
      solve_wt_undef.
      destruct (Float.to_longu f) eqn:?; simpl in *.
      inv H1; auto.
      solve_wt_undef.

    + destruct p; simpl in *; inv H.
      unfold convert_t in *.
      destruct s1.
      * destruct (Values.Val.longofsingle (Vsingle f)) eqn:?; simpl in *.
        destruct (Float32.to_long f) eqn:?; simpl in *; try discriminate.
        inv Heqo0; simpl in *.
        inv H1; auto.
        solve_wt_undef.
      * destruct (Values.Val.longuofsingle (Vsingle f)) eqn:?; simpl in *.
        destruct (Float32.to_longu f) eqn:?; simpl in *; try discriminate.
        inv Heqo0; simpl in *.
        inv H1; auto.
        solve_wt_undef.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + destruct s; simpl in *;
      destr_cond_match; simpl in *;
      inv H1; auto;
      solve_wt_undef.
    + inv_expr_type (eSexpr alloc em eb eu Tint v2).
      destr_cond_match; simpl in *;
      inv H2; auto;
      solve_wt_undef.
Qed.

Lemma expr_float_expr_single:
  forall alloc em v f,
    tcheck_expr v = Some Tfloat ->
    eSexpr alloc em eb eu Tfloat v = Vf f ->
    eSexpr alloc em eb eu Tsingle v = Vs (Float.to_single f).
Proof.
  destruct v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *; inv H1; auto.
Qed.


Lemma expr_single_expr_int:
  forall alloc em v f,
    tcheck_expr v = Some Tsingle ->
    eSexpr alloc em eb eu Tsingle v = Vs f ->
    eSexpr alloc em eb eu Tint v = Vi (Float32.to_bits f).
Proof.
  destruct v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *; inv H1; auto.
Qed.


Lemma expr_single_expr_long:
  forall alloc em v f,
    tcheck_expr v = Some Tsingle ->
    eSexpr alloc em eb eu Tsingle v = Vs f ->
    eSexpr alloc em eb eu Tlong v = Vl (Float.to_bits (Float.of_single f)).
Proof.
  destruct v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *; inv H1; auto.
Qed.


Lemma expr_single_expr_float:
  forall alloc em v f,
    tcheck_expr v = Some Tsingle ->
    eSexpr alloc em eb eu Tsingle v = Vs f ->
    eSexpr alloc em eb eu Tfloat v = Vf (Float.of_single f).
Proof.
  destruct v; simpl; intros.
  - destruct s; simpl in *; try discriminate.
    inv H0; auto.
  - destruct (tcheck_expr v) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s0); try discriminate. subst. revert H0. unfold_eval.
    destruct u; destruct s0; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      destruct s; simpl in *; inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
    + destruct p; simpl in *; inv H.
      simpl in *. inv H1; auto.
  - destruct (tcheck_expr v1) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s s1); try discriminate.
    destruct (tcheck_expr v2) eqn:?; simpl in *; try discriminate.
    destruct (styp_eq s0 s2); try discriminate.
    subst.
    revert H0; unfold_eval.
    destruct b; destruct s1; destruct s2; simpl in *; try congruence; simpl in *; simpl_eval'; try discriminate.
    + destruct s; simpl in *; inv H1; auto.
Qed.



Lemma expr_any_type:
  forall e1 e2 t1 t2 alloc em,
    tcheck_expr e1 = Some t1 ->
    tcheck_expr e2 = Some t1 ->
    eSexpr alloc em eb eu t1 e1 =
    eSexpr alloc em eb eu t1 e2 ->
    eSexpr alloc em eb eu t2 e1 =
    eSexpr alloc em eb eu t2 e2.
Proof.
  clear.
  intros e1 e2 t1 t2 alloc em TC1 TC2 EX.
  destruct t1; destruct t2; auto.
  - inv_expr_type (eSexpr alloc em eb eu Tint e1).
    erewrite ! expr_int_expr_long; try apply tcheck_expr_correct; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tint e1).
    erewrite ! expr_int_expr_float; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tint e1).
    erewrite ! expr_int_expr_single; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tlong e1).
    erewrite ! expr_long_expr_int; try apply tcheck_expr_correct; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tlong e1).
    erewrite ! expr_long_expr_float; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tlong e1).
    erewrite ! expr_long_expr_single; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tfloat e1).
    erewrite ! expr_float_expr_int; try apply tcheck_expr_correct; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tfloat e1).
    erewrite ! expr_float_expr_long; try apply tcheck_expr_correct; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tfloat e1).
    erewrite ! expr_float_expr_single; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tsingle e1).
    erewrite ! expr_single_expr_int; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tsingle e1).
    erewrite ! expr_single_expr_long; eauto.
  - inv_expr_type (eSexpr alloc em eb eu Tsingle e1).
    erewrite ! expr_single_expr_float; eauto.
Qed.
Generated by coq2html