(* Operations common to the Cminor and RTLabs front end stages. *)

(* Adapted from CompCert's Cminor.ma: *)

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

include "common/Values.ma".
include "common/FrontEndMem.ma".

inductive constant : typ → Type[0] ≝
  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
(*  | Ofloatconst: ∀sz. float → constant (ASTfloat sz) *)
  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)

definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ].

inductive unary_operation : typ → typ → Type[0] ≝
  | Ocastint: ∀sz,sg,sz',sg'. unary_operation (ASTint sz sg) (ASTint sz' sg')  (**r integer casts *)
  | Onegint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r integer opposite *)
  | Onotbool: ∀t,sz,sg. boolsrc t → unary_operation t (ASTint sz sg)           (**r boolean negation  *)
  | Onotint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r bitwise complement  *)
(*| Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float opposite *)
(*| Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float absolute value *)
(*| Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)*)            (**r float truncation *)
(*| Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)*) (**r signed integer to float *)
(*| Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned)*) (**r unsigned integer to float *)
(*| Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)*)   (**r float to signed integer *)
(*| Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz)*) (**r float to unsigned integer *)
  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
  | Ointofptr: ∀sz,sg. unary_operation ASTptr (ASTint sz sg).                  (**r pointer to int *)

inductive binary_operation : typ → typ → typ → Type[0] ≝
  | Oadd:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer addition *)
  | Osub:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer subtraction *)
  | Omul:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer multiplication *)
  | Odiv:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed division *)
  | Odivu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned division *)
  | Omod:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed modulus *)
  | Omodu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned modulus *)
  | Oand:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``and'' *)
  | Oor:   ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``or'' *)
  | Oxor:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``xor'' *)
  | Oshl:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r left shift *)
  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
(*  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float addition *)
(*  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float subtraction *)
(*  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float multiplication *)
(*  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float division *)
  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
  | Oaddp: ∀sz.    binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Signed)   (**r subtract two pointers *)
  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)


lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
val_typ v t →
match t with
[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
(*| ASTfloat sz ⇒ ∀f.P (Vfloat f) *)
| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
] →
P v.
#v #t #P *
[ 1: //
| * //
| #b #o * //
] qed.

(* * Evaluation of constants and operator applications.
    [None] is returned when the computation is undefined, e.g.
    if arguments are of the wrong types, or in case of an integer division
    by zero. *)

definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝
λt,find_symbol,sp,cst.
  match cst with
  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
(*  | Ofloatconst sz n ⇒ Some ? (Vfloat n)*)
  | Oaddrsymbol s ofs ⇒
      match find_symbol s with
      [ None ⇒ None ?
      | Some b ⇒ (*match pointer_compat_dec b r with
                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
                 | inr _ ⇒ None ?
                 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs))))
      ]
  | Oaddrstack ofs ⇒
      Some ? (Vptr (mk_pointer sp (shift_offset ? zero_offset (repr I16 ofs))))
  ]. (*cases sp // qed.*)

lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
  eval_constant t f sp c = Some ? v →
  val_typ v t.
#t #f #sp *
[ #sz #sg #i #v #E normalize in E; destruct //
(*| #sz #f #v #E normalize in E; destruct //*)
| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct 
(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
  //
| #n #v #E whd in E:(??%?); destruct //
] qed.

definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝
λt,t',op,arg.
  match op with
  [ Ocastint sz sg sz' sg' ⇒
      match sg with
      [ Unsigned ⇒ Some ? (zero_ext sz' arg)
      |   Signed ⇒ Some ? (sign_ext sz' arg)
      ]
  | Onegint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
  | Onotbool t sz sg _ ⇒
      match arg with
      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
      | Vnull ⇒ Some ? (Vint sz (repr ? 1))
      | _ ⇒ None ?
      ]
  | Onotint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
(*  | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
  | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ] 
  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
  | Ointoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
  | Ointuoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
  | Ofloatofint _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
  | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ] *)
  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
  (* Only conversion of null pointers is specified. *)
  | Optrofint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
  | Ointofptr sz sg ⇒ match arg with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
  ].

lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
  val_typ v t →
  eval_unop t t' op v = Some ? v' →
  val_typ v' t'.
#t #t' #op elim op
[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?);
  cases sg whd in ⊢ (??%? → ?); #E' destruct %
| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct %
| #t'' #sz #sg cases t''
  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
  | #H #v #v' #H1 @(elim_val_typ … H1) whd %
    [ whd in ⊢ (??%? → ?); #E' destruct; %
    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
    ]
(*  | #f * *)
  ]
| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
(*
| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
*)
| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
  whd in ⊢ (??%? → ?); #E destruct //
| #sz #sg #v #v' #H @(elim_val_typ … H) %
  [ whd in ⊢ (??%? → ?); #E destruct %
  | #b #o whd in ⊢ (??%? → ?); #E destruct
  ]
] qed.
  
(* I think this is duplicated somewhere else *)
definition eval_compare_mismatch : comparison → option val ≝
λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].

(* Individual operations, adapted from Values.  These differ in that they
   implement the plain Cminor/RTLabs operations (e.g., with separate addition
   for ints,floats and pointers) and use option rather than Vundef.  The ones
   in Value are probably not needed. *)

definition ev_add ≝ λv1,v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_sub ≝ λv1,v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

(* NB: requires arguments to be presented pointer first. *)
definition ev_addp ≝ λv1,v2: val.
  match v1 with
  [ Vptr ptr1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
    | _ ⇒ None ? ]
  | Vnull ⇒ match v2 with
    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
    | _ ⇒ None ?
    ]
  | _ ⇒ None ? ].

definition ev_subpi ≝ λv1,v2: val.
  match v1 with
  [ Vptr ptr1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
    | _ ⇒ None ? ]
  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_subpp ≝ λsz. λv1,v2: val.
  match v1 with
  [ Vptr ptr1 ⇒ match v2 with
    [ Vptr ptr2 ⇒
        if eq_block (pblock ptr1) (pblock ptr2)
          then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2)))
          else None ?
    | _ ⇒ None ? ]
  | Vnull  ⇒ match v2 with [ Vnull  ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mul ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (short_multiplication ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_divs ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mods ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
                    (None ?)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_divu ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
                    (None ?)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_modu ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
                    (None ?)
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

definition ev_and ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_or ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_xor ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shl ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with 
    [ Vint sz2 n2 ⇒
       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shr ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with 
    [ Vint sz2 n2 ⇒
       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_shru ≝ λv1, v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with 
    [ Vint sz2 n2 ⇒
       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
       else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

(*
definition ev_addf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_subf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_mulf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_divf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ]. *)

definition FEtrue : val ≝ Vint I8 (repr I8 1).
definition FEfalse : val ≝ Vint I8 (repr I8 0).
definition FE_of_bool : bool → val ≝
λb. if b then FEtrue else FEfalse.

definition ev_cmp_match : comparison → option val ≝ λc.
  match c with
  [ Ceq ⇒ Some ? FEtrue
  | Cne ⇒ Some ? FEfalse
  | _   ⇒ None ?
  ].

definition ev_cmp_mismatch : comparison → option val ≝ λc.
  match c with
  [ Ceq ⇒ Some ? FEfalse
  | Cne ⇒ Some ? FEtrue
  | _   ⇒ None ?
  ].

definition ev_cmp ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (FE_of_bool (cmp_int ? c n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

definition ev_cmpp ≝ λm. λc: comparison. λv1,v2: val.
  match v1 with
  [ Vptr ptr1 ⇒ match v2 with
    [ Vptr ptr2 ⇒
        if valid_pointer m ptr1 ∧ valid_pointer m ptr2
        then
          if eq_block (pblock ptr1) (pblock ptr2)
          then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
          else ev_cmp_mismatch c
        else None ?
    | Vnull  ⇒ ev_cmp_mismatch c
    | _ ⇒ None ? ]
  | Vnull  ⇒ match v2 with
    [ Vptr _ ⇒ ev_cmp_mismatch c
    | Vnull  ⇒ ev_cmp_match c
    | _ ⇒ None ?
    ]
  | _ ⇒ None ? ].

(* TODO: check this, it isn't the cmpu used elsewhere *)
definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (FE_of_bool (cmpu_int ? c n1 n2)))
                    (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

(*
definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
    | _ ⇒ None ? ]
  | _ ⇒ None ? ]. *)

definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
λm,t1,t2,t',op.
  match op with
  [ Oadd _ _ ⇒ ev_add
  | Osub _ _ ⇒ ev_sub
  | Omul _ _ ⇒ ev_mul
  | Odiv _ ⇒ ev_divs
  | Odivu _ ⇒ ev_divu
  | Omod _ ⇒ ev_mods
  | Omodu _ ⇒ ev_modu
  | Oand _ _ ⇒ ev_and
  | Oor _ _ ⇒ ev_or
  | Oxor _ _ ⇒ ev_xor
  | Oshl _ _ ⇒ ev_shl
  | Oshr _ _ ⇒ ev_shr
  | Oshru _ _ ⇒ ev_shru
(*  | Oaddf _ ⇒ ev_addf
  | Osubf _ ⇒ ev_subf
  | Omulf _ ⇒ ev_mulf
  | Odivf _ ⇒ ev_divf *)
  | Ocmp _ _ _ c ⇒ ev_cmp c
  | Ocmpu _ _ c ⇒ ev_cmpu c
(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
  | Oaddp _ ⇒ ev_addp
  | Osubpi _ ⇒ ev_subpi
  | Osubpp sz ⇒ ev_subpp sz
  | Ocmpp _ c ⇒ ev_cmpp m c
  ].

lemma eval_binop_typ_correct : ∀m,t1,t2,t',op,v1,v2,v'.
  val_typ v1 t1 → val_typ v2 t2 →
  eval_binop m t1 t2 t' op v1 v2 = Some ? v' →
  val_typ v' t'.
#m #t1x #t2x #tx' *
[ 1,2,3,8,9,10:
  #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true #E destruct //
| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_s ???) [ | #res ] #E whd in E:(??%?); destruct //
| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_u ???) [ | #res ] #E whd in E:(??%?); destruct //
| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_s ???) [ | #res ] #E whd in E:(??%?); destruct //
| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_u ???) [ | #res ] #E whd in E:(??%?); destruct //
(* shifts *)
| 11,12,13: #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
(* floats *)
(*| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
  whd in ⊢ (??%? → ?); #E destruct // *)
(* comparisons *)
| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmp_int ????) #E destruct //
| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
(*| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
(* pointers *)
| 16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
  whd in ⊢ (??%? → ?); [ cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
] qed.