(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(* * This module defines the type of values that is used in the dynamic
  semantics of all our intermediate languages. *)

include "utilities/Coqlib.ma".
include "common/AST.ma".
include "common/Integers.ma".
include "common/Floats.ma".
include "common/Errors.ma".

include "ASM/BitVectorZ.ma".

include "basics/logic.ma".

include "utilities/binary/Z.ma".
include "utilities/extralib.ma".

(* To define pointers we need a few details about the memory model.

   There are several kinds of pointers, which differ in which regions of
   memory they address and the pointer's representation.
   
   Pointers are given as kind, block, offset triples, where a block identifies
   some memory in a given region with an arbitrary concrete address.  A proof
   is also required that the representation is suitable for the region the
   memory resides in.  Note that blocks cannot extend out of a region (in
   particular, a pdata pointer can address any byte in a pdata block - we never
   need to switch to a larger xdata pointer).
 *)

(* blocks - represented by the region the memory resides in and a unique id *)

record block : Type[0] ≝
{ block_region : region
; block_id : Z
}.

definition eq_block ≝
λb1,b2.
  eq_region (block_region b1) (block_region b2) ∧
  eqZb (block_id b1) (block_id b2)
.

lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
  P (eq_block b1 b2).
#P * #r1 #i1 * #r2 #i2 #H1 #H2
whd in ⊢ (?%) @eq_region_elim #H3
[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
| @H2 % #E destruct elim H3 /2/
] qed.

lemma eq_block_b_b : ∀b. eq_block b b = true.
* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
qed.

(* Characterise the memory regions which the pointer representations can
   address.

   pointer_compat <block> <pointer representation> *)

inductive pointer_compat : block → region → Prop ≝
|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.

lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
* * #id *;
try ( %1 // )
%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
qed.

definition is_pointer_compat : block → region → bool ≝
λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].

(* Offsets into the block.  We allow integers like CompCert so that we have
   the option of extending blocks backwards. *)

record offset : Type[0] ≝ { offv : Z }.

definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
definition shift_offset : offset → int → offset ≝
  λo,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
definition neg_shift_offset : offset → int → offset ≝
  λo,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
definition sub_offset : offset → offset → int ≝
  λx,y. bitvector_of_Z ? (offv x - offv y).
definition zero_offset ≝ mk_offset OZ.
definition lt_offset : offset → offset → bool ≝
  λx,y. Zltb (offv x) (offv y).

(* * A value is either:
- a machine integer;
- a floating-point number;
- a pointer: a triple giving the representation of the pointer (in terms of the
             memory regions such a pointer could address), a memory address and
             an integer offset with respect to this address;
- a null pointer: the region denotes the representation (i.e., pointer size)
- the [Vundef] value denoting an arbitrary bit pattern, such as the
  value of an uninitialized variable.
*)

inductive val: Type[0] ≝
  | Vundef: val
  | Vint: int → val
  | Vfloat: float → val
  | Vnull: region → val
  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.

definition Vzero: val ≝ Vint zero.
definition Vone: val ≝ Vint one.
definition Vmone: val ≝ Vint mone.

definition Vtrue: val ≝ Vint one.
definition Vfalse: val ≝ Vint zero.

(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
   predicates here, but we don't (currently) have a single sizeof for Vundef.
   We only split in stages of the compiler where all Vint values are byte sized.
 *)

definition ptr_may_be_single : region → bool ≝
λr.match r with [ Data ⇒ true | IData ⇒ true | _ ⇒ false ].

definition may_be_single : val → Prop ≝
λv. match v with
[ Vundef ⇒ True
| Vint _ ⇒ True
| Vfloat _ ⇒ False
| Vnull r ⇒ ptr_may_be_single r = true
| Vptr r _ _ _ ⇒ ptr_may_be_single r = true
].

definition may_be_split : val → Prop ≝
λv.match v with
[ Vint _ ⇒ False
| Vnull r ⇒ ptr_may_be_single r = false
| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
| _ ⇒ True
].

inductive split_val : Type[0] ≝
| Single : ∀v:val. may_be_single v → split_val
| High   : ∀v:val. may_be_split v → split_val
| Low    : ∀v:val. may_be_split v → split_val.

notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
(*
let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
match m return λx.res (x = n) with
[ O ⇒ match n return λx. res (O = x) with [ O ⇒ OK ? (refl ??) | _ ⇒ Error ? ]
| S m' ⇒ match n return λx.res (S m' = x) with [ O ⇒ Error ? | S n' ⇒
  do E ← assert_nat_eq m' n';
  match E return λx.λ_. res (S m' = S x) with [ refl ⇒ OK ? (refl ??) ] ]
].

definition res_eq_nat : ∀m,n:nat. ∀P:nat → Type[0]. P m → res (P n) ≝
λm,n,P,p.
  do E ← assert_nat_eq m n;
  match E return λx.λ_. res (P x) with [ refl ⇒ OK ? p ].

definition break : ∀n:nat. val → res (Vector split_val n) ≝
λn,v. match v return λv'. (may_be_single v' → ?) → (may_be_split v' → ?) → ? with
[ Vundef ⇒ λs.λt. res_eq_nat 1 n ? (s I)
| Vint i ⇒ λs.λt. res_eq_nat 1 n ? (s I)
| Vfloat f ⇒ λs.λt. res_eq_nat 2 n ? (t I)
| Vnull r ⇒
    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with 
    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
    | false ⇒ λs.λt. ?
    ]
| Vptr r b p o ⇒
    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with 
    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
    | false ⇒ λs.λt. ?
    ]
] (λp. [[ Single v p ]]) (λp. [[ Low v p; High v p ]]).
@(res_eq_nat 2 n ? (t (refl ??))) qed. (* XXX: I have no idea why this fails if you do it directly. *)

definition val_eq : val → val → bool ≝
λx,y.
match x with
[ Vundef ⇒ match y with [ Vundef ⇒ true | _ ⇒ false ]
| Vint i ⇒ match y with [ Vint j ⇒ eq i j | _ ⇒ false ]
| Vfloat f ⇒ match y with [ Vfloat f' ⇒ match eq_dec f f' with [ inl _ ⇒ true | _ ⇒ false ] | _ ⇒ false ]
| Vnull r ⇒ match y with [ Vnull r' ⇒ eq_region r r' | _ ⇒ false ]
| Vptr r b p o ⇒ match y with [ Vptr r' b' p' o' ⇒ eq_region r r' ∧ eq_block b b' ∧ eq_offset o o' | _ ⇒ false ]
].

definition merge : ∀n:nat. Vector split_val n → res val ≝
λn,s. match s with
[ VEmpty ⇒ Error ?
| VCons _ h1 t1 ⇒
  match t1 with
  [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v | _ ⇒ Error ? ]
  | VCons _ h2 t2 ⇒
    match t2 with
    [ VEmpty ⇒ match h1 with [ Low v _ ⇒ match h2 with [ High v' _ ⇒ if val_eq v v' then OK ? v else Error ? | _ ⇒ Error ? ] | _ ⇒ Error ? ]
    | VCons _ _ _ ⇒ Error ?
    ]
  ]
].
   
*)
(*
(** The module [Val] defines a number of arithmetic and logical operations
  over type [val].  Most of these operations are straightforward extensions
  of the corresponding integer or floating-point operations. *)

Module Val.
*)
definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
(*
definition has_type ≝ λv: val. λt: typ.
  match v with
  [ Vundef ⇒ True
  | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
  | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
  | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
  | _ ⇒ False
  ].

let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
  match vl with
  [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
  | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
               has_type v1 t1 ∧ has_type_list vs ts ]
  ].
*)
(* * Truth values.  Pointers and non-zero integers are treated as [True].
  The integer 0 (also used to represent the null pointer) is [False].
  [Vundef] and floats are neither true nor false. *)

definition is_true : val → Prop ≝ λv.
  match v with
  [ Vint n ⇒ n ≠ zero
  | Vptr _ b _ ofs ⇒ True
  | _ ⇒ False
  ].

definition is_false : val → Prop ≝ λv.
  match v with
  [ Vint n ⇒ n = zero
  | Vnull _ ⇒ True
  | _ ⇒ False
  ].

inductive bool_of_val: val → bool → Prop ≝
  | bool_of_val_int_true:
      ∀n. n ≠ zero → bool_of_val (Vint n) true
  | bool_of_val_int_false:
      bool_of_val (Vint zero) false
  | bool_of_val_ptr:
      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
  | bool_of_val_null:
      ∀r. bool_of_val (Vnull r) true.

axiom ValueNotABoolean : String.

definition eval_bool_of_val : val → res bool ≝
λv. match v with
[ Vint i ⇒ OK ? (notb (eq i zero))
| Vnull _ ⇒ OK ? false
| Vptr _ _ _ _ ⇒ OK ? true
| _ ⇒ Error ? (msg ValueNotABoolean)
].

definition neg : val → val ≝ λv.
  match v with
  [ Vint n ⇒ Vint (neg n)
  | _ ⇒ Vundef
  ].

definition negf : val → val ≝ λv.
  match v with
  [ Vfloat f ⇒ Vfloat (Fneg f)
  | _ => Vundef
  ].

definition absf : val → val ≝ λv.
  match v with
  [ Vfloat f ⇒ Vfloat (Fabs f)
  | _ ⇒ Vundef
  ].

definition intoffloat : val → val ≝ λv.
  match v with
  [ Vfloat f ⇒ Vint (intoffloat f)
  | _ ⇒ Vundef
  ].

definition intuoffloat : val → val ≝ λv.
  match v with
  [ Vfloat f ⇒ Vint (intuoffloat f)
  | _ ⇒ Vundef
  ].

definition floatofint : val → val ≝ λv.
  match v with
  [ Vint n ⇒ Vfloat (floatofint n)
  | _ ⇒ Vundef
  ].

definition floatofintu : val → val ≝ λv.
  match v with
  [ Vint n ⇒ Vfloat (floatofintu n)
  | _ ⇒ Vundef
  ].

definition notint : val → val ≝ λv.
  match v with
  [ Vint n ⇒ Vint (xor n mone)
  | _ ⇒ Vundef
  ].
  
(* FIXME: switch to alias, or rename, or … *)
definition int_eq : int → int → bool ≝ eq.
definition notbool : val → val ≝ λv.
  match v with
  [ Vint n ⇒ of_bool (int_eq n zero)
  | Vptr _ b _ ofs ⇒ Vfalse
  | Vnull _ ⇒ Vtrue
  | _ ⇒ Vundef
  ].

definition zero_ext ≝ λnbits: nat. λv: val.
  match v with
  [ Vint n ⇒ Vint (zero_ext nbits n)
  | _ ⇒ Vundef
  ].

definition sign_ext ≝ λnbits:nat. λv:val.
  match v with
  [ Vint i ⇒ Vint (sign_ext nbits i)
  | _ ⇒ Vundef
  ].

definition singleoffloat : val → val ≝ λv.
  match v with
  [ Vfloat f ⇒ Vfloat (singleoffloat f)
  | _ ⇒ Vundef
  ].

(* TODO: add zero to null? *)
definition add ≝ λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (addition_n ? n1 n2)
    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    | _ ⇒ Vundef ]
  | Vptr r b1 p ofs1 ⇒ match v2 with
    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition sub ≝ λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (subtraction ? n1 n2)
    | _ ⇒ Vundef ]
  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
    | Vptr r2 b2 p2 ofs2 ⇒
        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    | _ ⇒ Vundef ]
  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition mul ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (mul n1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].
(*
definition divs ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (divs n1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

Definition mods (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
  | _, _ => Vundef
  end.

Definition divu (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
  | _, _ => Vundef
  end.

Definition modu (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
  | _, _ => Vundef
  end.
*)
definition v_and ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (i_and n1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition or ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (or n1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition xor ≝ λv1, v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ Vint (xor n1 n2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].
(*
Definition shl (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shl n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shr (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shr n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shr_carry (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shr_carry n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shrx (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shrx n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition shru (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.shru n1 n2)
     else Vundef
  | _, _ => Vundef
  end.

Definition rolm (v: val) (amount mask: int): val :=
  match v with
  | Vint n => Vint(Int.rolm n amount mask)
  | _ => Vundef
  end.

Definition ror (v1 v2: val): val :=
  match v1, v2 with
  | Vint n1, Vint n2 =>
     if Int.ltu n2 Int.iwordsize
     then Vint(Int.ror n1 n2)
     else Vundef
  | _, _ => Vundef
  end.
*)
definition addf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Vfloat (Fadd f1 f2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition subf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Vfloat (Fsub f1 f2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition mulf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Vfloat (Fmul f1 f2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition divf ≝ λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

definition cmp_match : comparison → val ≝ λc.
  match c with
  [ Ceq ⇒ Vtrue
  | Cne ⇒ Vfalse
  | _   ⇒ Vundef
  ].

definition cmp_mismatch : comparison → val ≝ λc.
  match c with
  [ Ceq ⇒ Vfalse
  | Cne ⇒ Vtrue
  | _   ⇒ Vundef
  ].

definition cmp_offset ≝
λc: comparison. λx,y:offset.
  match c with
  [ Ceq ⇒  eq_offset x y
  | Cne ⇒ ¬eq_offset x y
  | Clt ⇒  lt_offset x y
  | Cle ⇒ ¬lt_offset y x
  | Cgt ⇒  lt_offset y x
  | Cge ⇒ ¬lt_offset x y
  ].

definition cmp ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    | _ ⇒ Vundef ]
  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vptr r2 b2 p2 ofs2 ⇒
        if eq_block b1 b2
        then of_bool (cmp_offset c ofs1 ofs2)
        else cmp_mismatch c
    | Vnull r2 ⇒ cmp_mismatch c
    | _ ⇒ Vundef ]
  | Vnull r1 ⇒ match v2 with
    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    | Vnull r2 ⇒ cmp_match c
    | _ ⇒ Vundef
    ]
  | _ ⇒ Vundef ].

definition cmpu ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vint n1 ⇒ match v2 with
    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    | _ ⇒ Vundef ]
  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    [ Vptr r2 b2 p2 ofs2 ⇒
        if eq_block b1 b2
        then of_bool (cmp_offset c ofs1 ofs2)
        else cmp_mismatch c
    | Vnull r2 ⇒ cmp_mismatch c
    | _ ⇒ Vundef ]
  | Vnull r1 ⇒ match v2 with
    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
    | Vnull r2 ⇒ cmp_match c
    | _ ⇒ Vundef
    ]
  | _ ⇒ Vundef ].

definition cmpf ≝ λc: comparison. λv1,v2: val.
  match v1 with
  [ Vfloat f1 ⇒ match v2 with
    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
    | _ ⇒ Vundef ]
  | _ ⇒ Vundef ].

(* * [load_result] is used in the memory model (library [Mem])
  to post-process the results of a memory read.  For instance,
  consider storing the integer value [0xFFF] on 1 byte at a
  given address, and reading it back.  If it is read back with
  chunk [Mint8unsigned], zero-extension must be performed, resulting
  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
  is performed and [0xFFFFFFFF] is returned.   Type mismatches
  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)

let rec load_result (chunk: memory_chunk) (v: val) ≝
  match v with
  [ Vint n ⇒
    match chunk with
    [ Mint8signed ⇒ Vint (sign_ext 8 n)
    | Mint8unsigned ⇒ Vint (zero_ext 8 n)
    | Mint16signed ⇒ Vint (sign_ext 16 n)
    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    | Mint32 ⇒ Vint n
    | _ ⇒ Vundef
    ]
  | Vptr r b p ofs ⇒
    match chunk with
    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
    | _ ⇒ Vundef
    ]
  | Vnull r ⇒
    match chunk with
    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
    | _ ⇒ Vundef
    ]
  | Vfloat f ⇒
    match chunk with
    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
    | Mfloat64 ⇒ Vfloat f
    | _ ⇒ Vundef
    ]
  | _ ⇒ Vundef
  ].

(*
(** Theorems on arithmetic operations. *)

Theorem cast8unsigned_and:
  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
Proof.
  destruct x; simpl; auto. decEq. 
  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
Qed.

Theorem cast16unsigned_and:
  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
Proof.
  destruct x; simpl; auto. decEq. 
  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
Qed.

Theorem istrue_not_isfalse:
  forall v, is_false v -> is_true (notbool v).
Proof.
  destruct v; simpl; try contradiction.
  intros. subst i. simpl. discriminate.
Qed.

Theorem isfalse_not_istrue:
  forall v, is_true v -> is_false (notbool v).
Proof.
  destruct v; simpl; try contradiction.
  intros. generalize (Int.eq_spec i Int.zero).
  case (Int.eq i Int.zero); intro.
  contradiction. simpl. auto.
  auto.
Qed.

Theorem bool_of_true_val:
  forall v, is_true v -> bool_of_val v true.
Proof.
  intro. destruct v; simpl; intros; try contradiction.
  constructor; auto. constructor.
Qed.

Theorem bool_of_true_val2:
  forall v, bool_of_val v true -> is_true v.
Proof.
  intros. inversion H; simpl; auto.
Qed.

Theorem bool_of_true_val_inv:
  forall v b, is_true v -> bool_of_val v b -> b = true.
Proof.
  intros. inversion H0; subst v b; simpl in H; auto. 
Qed.

Theorem bool_of_false_val:
  forall v, is_false v -> bool_of_val v false.
Proof.
  intro. destruct v; simpl; intros; try contradiction.
  subst i;  constructor.
Qed.

Theorem bool_of_false_val2:
  forall v, bool_of_val v false -> is_false v.
Proof.
  intros. inversion H; simpl; auto.
Qed.

Theorem bool_of_false_val_inv:
  forall v b, is_false v -> bool_of_val v b -> b = false.
Proof.
  intros. inversion H0; subst v b; simpl in H.
  congruence. auto. contradiction.
Qed.

Theorem notbool_negb_1:
  forall b, of_bool (negb b) = notbool (of_bool b).
Proof.
  destruct b; reflexivity.
Qed.

Theorem notbool_negb_2:
  forall b, of_bool b = notbool (of_bool (negb b)).
Proof.
  destruct b; reflexivity.
Qed.

Theorem notbool_idem2:
  forall b, notbool(notbool(of_bool b)) = of_bool b.
Proof.
  destruct b; reflexivity.
Qed.

Theorem notbool_idem3:
  forall x, notbool(notbool(notbool x)) = notbool x.
Proof.
  destruct x; simpl; auto. 
  case (Int.eq i Int.zero); reflexivity.
Qed.

Theorem add_commut: forall x y, add x y = add y x.
Proof.
  destruct x; destruct y; simpl; auto.
  decEq. apply Int.add_commut.
Qed.

Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  rewrite Int.add_assoc; auto.
  rewrite Int.add_assoc; auto.
  decEq. decEq. apply Int.add_commut.
  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc. 
  decEq. apply Int.add_commut.
  decEq. rewrite Int.add_assoc. auto.
Qed.

Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
Proof.
  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
Qed.

Theorem add_permut_4:
  forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
Proof.
  intros. rewrite add_permut. rewrite add_assoc. 
  rewrite add_permut. symmetry. apply add_assoc. 
Qed.

Theorem neg_zero: neg Vzero = Vzero.
Proof.
  reflexivity.
Qed.

Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
Qed.

Theorem sub_zero_r: forall x, sub Vzero x = neg x.
Proof.
  destruct x; simpl; auto. 
Qed.

Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
Proof.
  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
Qed.

Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
Proof.
  intros. unfold sub, add.
  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
Qed.

Theorem sub_add_l:
  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
Proof.
  destruct v1; destruct v2; intros; simpl; auto.
  rewrite Int.sub_add_l. auto.
  rewrite Int.sub_add_l. auto.
  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
Qed.

Theorem sub_add_r:
  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
Proof.
  destruct v1; destruct v2; intros; simpl; auto.
  rewrite Int.sub_add_r. auto.
  repeat rewrite Int.sub_add_opp. decEq. 
  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
  decEq. repeat rewrite Int.sub_add_opp. 
  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
  case (zeq b b0); intro. simpl. decEq. 
  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
  apply Int.neg_add_distr.
  reflexivity.
Qed.

Theorem mul_commut: forall x y, mul x y = mul y x.
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.
Qed.

Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.mul_assoc.
Qed.

Theorem mul_add_distr_l:
  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.mul_add_distr_l.
Qed.


Theorem mul_add_distr_r:
  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.mul_add_distr_r.
Qed.

Theorem mul_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  mul x (Vint n) = shl x (Vint logn).
Proof.
  intros; destruct x; simpl; auto.
  change 32 with (Z_of_nat Int.wordsize).
  rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
Qed.  

Theorem mods_divs:
  forall x y, mods x y = sub x (mul (divs x y) y).
Proof.
  destruct x; destruct y; simpl; auto.
  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
Qed.

Theorem modu_divu:
  forall x y, modu x y = sub x (mul (divu x y) y).
Proof.
  destruct x; destruct y; simpl; auto.
  generalize (Int.eq_spec i0 Int.zero);
  case (Int.eq i0 Int.zero); simpl. auto. 
  intro. decEq. apply Int.modu_divu. auto.
Qed.

Theorem divs_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  divs x (Vint n) = shrx x (Vint logn).
Proof.
  intros; destruct x; simpl; auto.
  change 32 with (Z_of_nat Int.wordsize).
  rewrite (Int.is_power2_range _ _ H). 
  generalize (Int.eq_spec n Int.zero);
  case (Int.eq n Int.zero); intro.
  subst n. compute in H. discriminate.
  decEq. apply Int.divs_pow2. auto.
Qed.

Theorem divu_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  divu x (Vint n) = shru x (Vint logn).
Proof.
  intros; destruct x; simpl; auto.
  change 32 with (Z_of_nat Int.wordsize).
  rewrite (Int.is_power2_range _ _ H). 
  generalize (Int.eq_spec n Int.zero);
  case (Int.eq n Int.zero); intro.
  subst n. compute in H. discriminate.
  decEq. apply Int.divu_pow2. auto.
Qed.

Theorem modu_pow2:
  forall x n logn,
  Int.is_power2 n = Some logn ->
  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
Proof.
  intros; destruct x; simpl; auto.
  generalize (Int.eq_spec n Int.zero);
  case (Int.eq n Int.zero); intro.
  subst n. compute in H. discriminate.
  decEq. eapply Int.modu_and; eauto.
Qed.

Theorem and_commut: forall x y, and x y = and y x.
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.
Qed.

Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.and_assoc.
Qed.

Theorem or_commut: forall x y, or x y = or y x.
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.
Qed.

Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.or_assoc.
Qed.

Theorem xor_commut: forall x y, xor x y = xor y x.
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.
Qed.

Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
Proof.
  destruct x; destruct y; destruct z; simpl; auto.
  decEq. apply Int.xor_assoc.
Qed.

Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
Proof.
  destruct x; destruct y; simpl; auto. 
  case (Int.ltu i0 Int.iwordsize); auto.
  decEq. symmetry. apply Int.shl_mul.
Qed.

Theorem shl_rolm:
  forall x n,
  Int.ltu n Int.iwordsize = true ->
  shl x (Vint n) = rolm x n (Int.shl Int.mone n).
Proof.
  intros; destruct x; simpl; auto.
  rewrite H. decEq. apply Int.shl_rolm. exact H.
Qed.

Theorem shru_rolm:
  forall x n,
  Int.ltu n Int.iwordsize = true ->
  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
Proof.
  intros; destruct x; simpl; auto.
  rewrite H. decEq. apply Int.shru_rolm. exact H.
Qed.

Theorem shrx_carry:
  forall x y,
  add (shr x y) (shr_carry x y) = shrx x y.
Proof.
  destruct x; destruct y; simpl; auto.
  case (Int.ltu i0 Int.iwordsize); auto.
  simpl. decEq. apply Int.shrx_carry.
Qed.

Theorem or_rolm:
  forall x n m1 m2,
  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
Proof.
  intros; destruct x; simpl; auto.
  decEq. apply Int.or_rolm.
Qed.

Theorem rolm_rolm:
  forall x n1 m1 n2 m2,
  rolm (rolm x n1 m1) n2 m2 =
    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
           (Int.and (Int.rol m1 n2) m2).
Proof.
  intros; destruct x; simpl; auto.
  decEq. 
  apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
Qed.

Theorem rolm_zero:
  forall x m,
  rolm x Int.zero m = and x (Vint m).
Proof.
  intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
Qed.

Theorem addf_commut: forall x y, addf x y = addf y x.
Proof.
  destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
Qed.

Lemma negate_cmp_mismatch:
  forall c,
  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
Proof.
  destruct c; reflexivity.
Qed.

Theorem negate_cmp:
  forall c x y,
  cmp (negate_comparison c) x y = notbool (cmp c x y).
Proof.
  destruct x; destruct y; simpl; auto.
  rewrite Int.negate_cmp. apply notbool_negb_1.
  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
  case (zeq b b0); intro.
  rewrite Int.negate_cmp. apply notbool_negb_1.
  apply negate_cmp_mismatch.
Qed.

Theorem negate_cmpu:
  forall c x y,
  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
Proof.
  destruct x; destruct y; simpl; auto.
  rewrite Int.negate_cmpu. apply notbool_negb_1.
  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
  case (zeq b b0); intro.
  rewrite Int.negate_cmpu. apply notbool_negb_1.
  apply negate_cmp_mismatch.
Qed.

Lemma swap_cmp_mismatch:
  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
Proof.
  destruct c; reflexivity.
Qed.
  
Theorem swap_cmp:
  forall c x y,
  cmp (swap_comparison c) x y = cmp c y x.
Proof.
  destruct x; destruct y; simpl; auto.
  rewrite Int.swap_cmp. auto.
  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
  case (zeq b b0); intro.
  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
  rewrite zeq_false. apply swap_cmp_mismatch. auto.
Qed.

Theorem swap_cmpu:
  forall c x y,
  cmpu (swap_comparison c) x y = cmpu c y x.
Proof.
  destruct x; destruct y; simpl; auto.
  rewrite Int.swap_cmpu. auto.
  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
  case (zeq b b0); intro.
  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
  rewrite zeq_false. apply swap_cmp_mismatch. auto.
Qed.

Theorem negate_cmpf_eq:
  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
Proof.
  destruct v1; destruct v2; simpl; auto.
  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. 
  apply notbool_idem2.
Qed.

Theorem negate_cmpf_ne:
  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
Proof.
  destruct v1; destruct v2; simpl; auto.
  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto. 
Qed.

Lemma or_of_bool:
  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
Proof.
  destruct b1; destruct b2; reflexivity.
Qed.

Theorem cmpf_le:
  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
Proof.
  destruct v1; destruct v2; simpl; auto.
  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
Qed.

Theorem cmpf_ge:
  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
Proof.
  destruct v1; destruct v2; simpl; auto.
  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
Qed.

Definition is_bool (v: val) :=
  v = Vundef \/ v = Vtrue \/ v = Vfalse.

Lemma of_bool_is_bool:
  forall b, is_bool (of_bool b).
Proof.
  destruct b; unfold is_bool; simpl; tauto.
Qed.

Lemma undef_is_bool: is_bool Vundef.
Proof.
  unfold is_bool; tauto.
Qed.

Lemma cmp_mismatch_is_bool:
  forall c, is_bool (cmp_mismatch c).
Proof.
  destruct c; simpl; unfold is_bool; tauto.
Qed.

Lemma cmp_is_bool:
  forall c v1 v2, is_bool (cmp c v1 v2).
Proof.
  destruct v1; destruct v2; simpl; try apply undef_is_bool.
  apply of_bool_is_bool.
  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
Qed.

Lemma cmpu_is_bool:
  forall c v1 v2, is_bool (cmpu c v1 v2).
Proof.
  destruct v1; destruct v2; simpl; try apply undef_is_bool.
  apply of_bool_is_bool.
  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
Qed.

Lemma cmpf_is_bool:
  forall c v1 v2, is_bool (cmpf c v1 v2).
Proof.
  destruct v1; destruct v2; simpl;
  apply undef_is_bool || apply of_bool_is_bool.
Qed.

Lemma notbool_is_bool:
  forall v, is_bool (notbool v).
Proof.
  destruct v; simpl.
  apply undef_is_bool. apply of_bool_is_bool. 
  apply undef_is_bool. unfold is_bool; tauto.
Qed.

Lemma notbool_xor:
  forall v, is_bool v -> v = xor (notbool v) Vone.
Proof.
  intros. elim H; intro.  
  subst v. reflexivity.
  elim H0; intro; subst v; reflexivity.
Qed.

Lemma rolm_lt_zero:
  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
Proof.
  intros. destruct v; simpl; auto.
  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
  decEq. symmetry. rewrite Int.shru_rolm. auto. auto. 
  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto. 
Qed.

Lemma rolm_ge_zero:
  forall v,
  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
Proof.
  intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
  destruct (Int.lt i Int.zero); auto.
Qed.
*)
(* * The ``is less defined'' relation between values. 
    A value is less defined than itself, and [Vundef] is
    less defined than any value. *)

inductive Val_lessdef: val → val → Prop ≝
  | lessdef_refl: ∀v. Val_lessdef v v
  | lessdef_undef: ∀v. Val_lessdef Vundef v.

inductive lessdef_list: list val → list val → Prop ≝
  | lessdef_list_nil:
      lessdef_list (nil ?) (nil ?)
  | lessdef_list_cons:
      ∀v1,v2,vl1,vl2.
      Val_lessdef v1 v2 → lessdef_list vl1 vl2 →
      lessdef_list (v1 :: vl1) (v2 :: vl2).

(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
(*
lemma lessdef_list_inv:
  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
#vl1 elim vl1;
[ #vl2 #H inversion H; /2/; #h1 #h2 #t1 #t2 #H1 #H2 #H3 #Hbad destruct
| #h #t #IH #vl2 #H
    inversion H;
    [ #H' destruct
    | #h1 #h2 #t1 #t2 #H1 #H2 #H3 #e1 #e2 destruct;
        elim H1;
        [ elim (IH t2 H2);
            [ #e destruct; /2/;
            | /3/ ]
        | /3/ ]
    ]
] qed.
*)
lemma load_result_lessdef:
  ∀chunk,v1,v2.
  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
[ 8: #r ] whd in ⊢ (?%?); //; 
qed.

lemma zero_ext_lessdef:
  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
qed.

lemma sign_ext_lessdef:
  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
qed.
(*
Lemma singleoffloat_lessdef:
  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
Proof.
  intros; inv H; simpl; auto.
Qed.

End Val.
*)