Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 602 insertions, 504 deletions

diff --git a/common/AST.v b/common/AST.v
index 29d1452..1c46389 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -35,22 +35,15 @@ Definition ident_eq := peq.
 
 Parameter ident_of_string : String.string -> ident.
 
-(** The intermediate languages are weakly typed, using only four
-  types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit
-  floating-point numbers, [Tlong] for 64-bit integers, [Tsingle]
-  for 32-bit floating-point numbers. *)
+(** The intermediate languages are weakly typed, using the following types: *)
 
 Inductive typ : Type :=
-  | Tint
-  | Tfloat
-  | Tlong
-  | Tsingle.
-
-Definition typesize (ty: typ) : Z :=
-  match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 | Tsingle => 4 end.
-
-Lemma typesize_pos: forall ty, typesize ty > 0.
-Proof. destruct ty; simpl; omega. Qed.
+  | Tint                (**r 32-bit integers or pointers *)
+  | Tfloat              (**r 64-bit double-precision floats *)
+  | Tlong               (**r 64-bit integers *)
+  | Tsingle             (**r 32-bit single-precision floats *)
+  | Tany32              (**r any 32-bit value *)
+  | Tany64.             (**r any 64-bit value, i.e. any value *)
 
 Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
 Proof. decide equality. Defined.
@@ -62,8 +55,22 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
 Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                      := list_eq_dec typ_eq.
 
-(** All values of type [Tsingle] are also of type [Tfloat].  This
-  corresponds to the following subtyping relation over types. *)
+Definition typesize (ty: typ) : Z :=
+  match ty with
+  | Tint => 4
+  | Tfloat => 8
+  | Tlong => 8
+  | Tsingle => 4
+  | Tany32 => 4
+  | Tany64 => 8
+  end.
+
+Lemma typesize_pos: forall ty, typesize ty > 0.
+Proof. destruct ty; simpl; omega. Qed.
+
+(** All values of size 32 bits are also of type [Tany32].  All values
+  are of type [Tany64].  This corresponds to the following subtyping
+  relation over types. *)
 
 Definition subtype (ty1 ty2: typ) : bool :=
   match ty1, ty2 with
@@ -71,7 +78,8 @@ Definition subtype (ty1 ty2: typ) : bool :=
   | Tlong, Tlong => true
   | Tfloat, Tfloat => true
   | Tsingle, Tsingle => true
-  | Tsingle, Tfloat => true
+  | (Tint | Tsingle | Tany32), Tany32 => true
+  | _, Tany64 => true
   | _, _ => false
   end.
 
@@ -133,7 +141,9 @@ Inductive memory_chunk : Type :=
   | Mint32          (**r 32-bit integer, or pointer *)
   | Mint64          (**r 64-bit integer *)
   | Mfloat32        (**r 32-bit single-precision float *)
-  | Mfloat64.        (**r 64-bit double-precision float *)
+  | Mfloat64        (**r 64-bit double-precision float *)
+  | Many32          (**r any value that fits in 32 bits *)
+  | Many64.         (**r any value *)
 
 Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}.
 Proof. decide equality. Defined.
@@ -151,18 +161,8 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
   | Mint64 => Tlong
   | Mfloat32 => Tsingle
   | Mfloat64 => Tfloat
-  end.
-
-Definition type_of_chunk_use (c: memory_chunk) : typ :=
-  match c with
-  | Mint8signed => Tint
-  | Mint8unsigned => Tint
-  | Mint16signed => Tint
-  | Mint16unsigned => Tint
-  | Mint32 => Tint
-  | Mint64 => Tlong
-  | Mfloat32 => Tfloat
-  | Mfloat64 => Tfloat
+  | Many32 => Tany32
+  | Many64 => Tany64
   end.
 
 (** The chunk that is appropriate to store and reload a value of
@@ -174,6 +174,8 @@ Definition chunk_of_type (ty: typ) :=
   | Tfloat => Mfloat64
   | Tlong => Mint64
   | Tsingle => Mfloat32
+  | Tany32 => Many32
+  | Tany64 => Many64
   end.
 
 (** Initialization data for global variables. *)
@@ -183,7 +185,7 @@ Inductive init_data: Type :=
   | Init_int16: int -> init_data
   | Init_int32: int -> init_data
   | Init_int64: int64 -> init_data
-  | Init_float32: float -> init_data
+  | Init_float32: float32 -> init_data
   | Init_float64: float -> init_data
   | Init_space: Z -> init_data
   | Init_addrof: ident -> int -> init_data.  (**r address of symbol + offset *)
@@ -586,9 +588,9 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_external name sg => sg
   | EF_builtin name sg => sg
   | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default
-  | EF_vstore chunk => mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default
+  | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default
   | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default
-  | EF_vstore_global chunk _ _ => mksignature (type_of_chunk_use chunk :: nil) None cc_default
+  | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default
   | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
   | EF_free => mksignature (Tint :: nil) None cc_default
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
diff --git a/common/Events.v b/common/Events.v
index 48cd91e..5eee93a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -57,7 +57,7 @@ Inductive eventval: Type :=
   | EVint: int -> eventval
   | EVlong: int64 -> eventval
   | EVfloat: float -> eventval
-  | EVfloatsingle: float -> eventval
+  | EVsingle: float32 -> eventval
   | EVptr_global: ident -> int -> eventval.
 
 Inductive event: Type :=
@@ -274,8 +274,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_float: forall f,
       eventval_match (EVfloat f) Tfloat (Vfloat f)
   | ev_match_single: forall f,
-      Float.is_single f ->
-      eventval_match (EVfloatsingle f) Tsingle (Vfloat f)
+      eventval_match (EVsingle f) Tsingle (Vsingle f)
   | ev_match_ptr: forall id b ofs,
       Genv.find_symbol ge id = Some b ->
       eventval_match (EVptr_global id ofs) Tint (Vptr b ofs).
@@ -388,7 +387,7 @@ Definition eventval_valid (ev: eventval) : Prop :=
   | EVint _ => True
   | EVlong _ => True
   | EVfloat _ => True
-  | EVfloatsingle f => Float.is_single f
+  | EVsingle _ => True
   | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b
   end.
 
@@ -397,7 +396,7 @@ Definition eventval_type (ev: eventval) : typ :=
   | EVint _ => Tint
   | EVlong _ => Tlong
   | EVfloat _ => Tfloat
-  | EVfloatsingle _ => Tsingle
+  | EVsingle _ => Tsingle
   | EVptr_global id ofs => Tint
   end.
 
@@ -412,7 +411,7 @@ Proof.
   destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto.
   exists (Vlong i0); constructor.
   exists (Vfloat f1); constructor.
-  exists (Vfloat f1); constructor; auto.
+  exists (Vsingle f1); constructor; auto.
   exists (Vint i); constructor.
   destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto.
 Qed.
@@ -967,7 +966,7 @@ Qed.
 Lemma volatile_store_ok:
   forall chunk,
   extcall_properties (volatile_store_sem chunk) 
-                     (mksignature (Tint :: type_of_chunk_use chunk :: nil) None cc_default).
+                     (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
@@ -1022,7 +1021,7 @@ Qed.
 Lemma volatile_store_global_ok:
   forall chunk id ofs,
   extcall_properties (volatile_store_global_sem chunk id ofs) 
-                     (mksignature (type_of_chunk_use chunk :: nil) None cc_default).
+                     (mksignature (type_of_chunk chunk :: nil) None cc_default).
 Proof.
   intros; constructor; intros.
 (* well typed *)
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index bd38fa3..a34a05d 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -516,7 +516,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m
   | Init_int16 n => Mem.store Mint16unsigned m b p (Vint n)
   | Init_int32 n => Mem.store Mint32 m b p (Vint n)
   | Init_int64 n => Mem.store Mint64 m b p (Vlong n)
-  | Init_float32 n => Mem.store Mfloat32 m b p (Vfloat n)
+  | Init_float32 n => Mem.store Mfloat32 m b p (Vsingle n)
   | Init_float64 n => Mem.store Mfloat64 m b p (Vfloat n)
   | Init_addrof symb ofs =>
       match find_symbol ge symb with
@@ -848,7 +848,7 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s
       Mem.load Mint64 m b p = Some(Vlong n)
       /\ load_store_init_data m b (p + 8) il'
   | Init_float32 n :: il' =>
-      Mem.load Mfloat32 m b p = Some(Vfloat(Float.singleoffloat n))
+      Mem.load Mfloat32 m b p = Some(Vsingle n)
       /\ load_store_init_data m b (p + 4) il'
   | Init_float64 n :: il' =>
       Mem.load Mfloat64 m b p = Some(Vfloat n)
@@ -895,7 +895,7 @@ Proof.
   eapply (A Mint16unsigned (Vint i)); eauto.
   eapply (A Mint32 (Vint i)); eauto.
   eapply (A Mint64 (Vlong i)); eauto.
-  eapply (A Mfloat32 (Vfloat f)); eauto.
+  eapply (A Mfloat32 (Vsingle f)); eauto.
   eapply (A Mfloat64 (Vfloat f)); eauto.
   inv Heqo. red; intros. transitivity (Mem.load chunk m1 b p0). 
   eapply store_init_data_list_outside; eauto. right. simpl. xomega. 
diff --git a/common/Memdata.v b/common/Memdata.v
index 1b74705..96278a2 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -39,6 +39,8 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
   | Mint64 => 8
   | Mfloat32 => 4
   | Mfloat64 => 8
+  | Many32 => 4
+  | Many64 => 8
   end.
 
 Lemma size_chunk_pos:
@@ -86,6 +88,8 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
   | Mint64 => 8
   | Mfloat32 => 4
   | Mfloat64 => 4
+  | Many32 => 4
+  | Many64 => 4
   end.
 
 Lemma align_chunk_pos:
@@ -112,12 +116,27 @@ Proof.
         | exists 8; reflexivity ].
 Qed.
 
+Inductive quantity : Type := Q32 | Q64.
+
+Definition quantity_eq (q1 q2: quantity) : {q1 = q2} + {q1 <> q2}.
+Proof. decide equality. Defined.
+Global Opaque quantity_eq.
+
+Definition size_quantity_nat (q: quantity) :=
+  match q with Q32 => 4%nat | Q64 => 8%nat end.
+
+Lemma size_quantity_nat_pos:
+  forall q, exists n, size_quantity_nat q = S n.
+Proof.
+  intros. destruct q; [exists 3%nat | exists 7%nat]; auto.
+Qed.
+
 (** * Memory values *)
 
 (** A ``memory value'' is a byte-sized quantity that describes the current
   content of a memory cell.  It can be either:
 - a concrete 8-bit integer;
-- a byte-sized fragment of an opaque pointer;
+- a byte-sized fragment of an opaque value;
 - the special constant [Undef] that represents uninitialized memory.
 *)
 
@@ -126,7 +145,7 @@ Qed.
 Inductive memval: Type :=
   | Undef: memval
   | Byte: byte -> memval
-  | Pointer: block -> int -> nat -> memval.
+  | Fragment: val -> quantity -> nat -> memval.
 
 (** * Encoding and decoding integers *)
 
@@ -311,25 +330,28 @@ Proof.
   simpl. decEq. auto.
 Qed.
 
-Fixpoint inj_pointer (n: nat) (b: block) (ofs: int) {struct n}: list memval :=
+Fixpoint inj_value_rec (n: nat) (v: val) (q: quantity) {struct n}: list memval :=
   match n with
   | O => nil
-  | S m => Pointer b ofs m :: inj_pointer m b ofs
+  | S m => Fragment v q m :: inj_value_rec m v q
   end.
 
-Fixpoint check_pointer (n: nat) (b: block) (ofs: int) (vl: list memval) 
+Definition inj_value (q: quantity) (v: val): list memval :=
+  inj_value_rec (size_quantity_nat q) v q.
+
+Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval) 
                        {struct n} : bool :=
   match n, vl with
   | O, nil => true
-  | S m, Pointer b' ofs' m' :: vl' =>
-      eq_block b b' && Int.eq_dec ofs ofs' && beq_nat m m' && check_pointer m b ofs vl'
+  | S m, Fragment v' q' m' :: vl' =>
+      Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl'
   | _, _ => false
   end.
 
-Definition proj_pointer (vl: list memval) : val :=
+Definition proj_value (q: quantity) (vl: list memval) : val :=
   match vl with
-  | Pointer b ofs n :: vl' =>
-      if check_pointer 4%nat b ofs vl then Vptr b ofs else Vundef
+  | Fragment v q' n :: vl' =>
+      if check_value (size_quantity_nat q) v q vl then v else Vundef
   | _ => Vundef
   end.
 
@@ -338,10 +360,12 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
   | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
   | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
-  | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs
+  | Vptr b ofs, Mint32 => inj_value Q32 v
   | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
-  | Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n)))
-  | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n)))
+  | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
+  | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
+  | _, Many32 => inj_value Q32 v
+  | _, Many64 => inj_value Q64 v
   | _, _ => list_repeat (size_chunk_nat chunk) Undef
   end.
 
@@ -355,12 +379,15 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
       | Mint16unsigned => Vint(Int.zero_ext 16 (Int.repr (decode_int bl)))
       | Mint32 => Vint(Int.repr(decode_int bl))
       | Mint64 => Vlong(Int64.repr(decode_int bl))
-      | Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl)))
-      | Mfloat64 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl)))
+      | Mfloat32 => Vsingle(Float32.of_bits (Int.repr (decode_int bl)))
+      | Mfloat64 => Vfloat(Float.of_bits (Int64.repr (decode_int bl)))
+      | Many32 => Vundef
+      | Many64 => Vundef
       end
   | None =>
       match chunk with
-      | Mint32 => proj_pointer vl
+      | Mint32 | Many32 => Val.load_result chunk (proj_value Q32 vl)
+      | Many64 => Val.load_result chunk (proj_value Q64 vl)
       | _ => Vundef
       end
   end.
@@ -374,14 +401,40 @@ Proof.
         | rewrite length_inj_bytes; apply encode_int_length ].
 Qed.
 
-Lemma check_inj_pointer:
-  forall b ofs n, check_pointer n b ofs (inj_pointer n b ofs) = true.
+Lemma check_inj_value:
+  forall v q n, check_value n v q (inj_value_rec n v q) = true.
 Proof.
   induction n; simpl. auto. 
   unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true.  
   rewrite <- beq_nat_refl. simpl; auto.
 Qed.
 
+Lemma proj_inj_value:
+  forall q v, proj_value q (inj_value q v) = v.
+Proof.
+  intros. unfold proj_value, inj_value. destruct (size_quantity_nat_pos q) as [n EQ]. 
+  rewrite EQ at 1. simpl. rewrite check_inj_value. auto.
+Qed.
+
+Remark in_inj_value:
+  forall mv v q, In mv (inj_value q v) -> exists n, mv = Fragment v q n.
+Proof.
+Local Transparent inj_value.
+  unfold inj_value; intros until q. generalize (size_quantity_nat q). induction n; simpl; intros.
+  contradiction.
+  destruct H. exists n; auto. eauto. 
+Qed.
+
+Lemma proj_inj_value_mismatch:
+  forall q1 q2 v, q1 <> q2 -> proj_value q1 (inj_value q2 v) = Vundef.
+Proof.
+  intros. unfold proj_value. destruct (inj_value q2 v) eqn:V. auto. destruct m; auto.
+  destruct (in_inj_value (Fragment v0 q n) v q2) as [n' EQ]. 
+  rewrite V; auto with coqlib. inv EQ.
+  destruct (size_quantity_nat_pos q1) as [p EQ1]; rewrite EQ1; simpl.
+  unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_false by congruence. auto.
+Qed.
+
 Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : Prop :=
   match v1, chunk1, chunk2 with
   | Vundef, _, _ => v2 = Vundef
@@ -394,21 +447,30 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
   | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint32, Mint32 => v2 = Vint n
-  | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n)
-  | Vint n, (Mint64 | Mfloat32 | Mfloat64), _ => v2 = Vundef
+  | Vint n, Many32, (Mint32 | Many32) => v2 = Vint n
+  | Vint n, Mint32, Mfloat32 => v2 = Vsingle(Float32.of_bits n)
+  | Vint n, Many64, Many64 => v2 = Vint n
+  | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Many64), _ => v2 = Vundef
   | Vint n, _, _ => True (**r nothing meaningful to say about v2 *)
-  | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs
+  | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = Vptr b ofs
+  | Vptr b ofs, Many64, Many64 => v2 = Vptr b ofs
   | Vptr b ofs, _, _ => v2 = Vundef
   | Vlong n, Mint64, Mint64 => v2 = Vlong n
-  | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.double_of_bits n)
-  | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64), _ => v2 = Vundef
+  | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.of_bits n)
+  | Vlong n, Many64, Many64 => v2 = Vlong n
+  | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Many32), _ => v2 = Vundef
   | Vlong n, _, _ => True (**r nothing meaningful to say about v2 *)
-  | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f)
-  | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f)
   | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f
-  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef
-  | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.bits_of_double f)
+  | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.to_bits f)
+  | Vfloat f, Many64, Many64 => v2 = Vfloat f
+  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mint64|Many32), _ => v2 = Vundef
   | Vfloat f, _, _ => True   (* nothing interesting to say about v2 *)
+  | Vsingle f, Mfloat32, Mfloat32 => v2 = Vsingle f
+  | Vsingle f, Mfloat32, Mint32 => v2 = Vint(Float32.to_bits f)
+  | Vsingle f, Many32, Many32 => v2 = Vsingle f
+  | Vsingle f, Many64, Many64 => v2 = Vsingle f
+  | Vsingle f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64|Mfloat64|Many64), _ => v2 = Vundef
+  | Vsingle f, _, _ => True (* nothing interesting to say about v2 *)
   end.
 
 Remark decode_val_undef:
@@ -417,14 +479,23 @@ Proof.
   intros. unfold decode_val. simpl. destruct chunk; auto.
 Qed.
 
+Remark proj_bytes_inj_value:
+  forall q v, proj_bytes (inj_value q v) = None.
+Proof.
+  intros. destruct q; reflexivity. 
+Qed.
+
 Lemma decode_encode_val_general:
   forall v chunk1 chunk2,
   decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)).
 Proof.
-Opaque inj_pointer.
+Opaque inj_value.
   intros.
-  destruct v; destruct chunk1; simpl; try (apply decode_val_undef);
-  destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes).
+  destruct v; destruct chunk1 eqn:C1; simpl; try (apply decode_val_undef);
+  destruct chunk2 eqn:C2; unfold decode_val; auto; 
+  try (rewrite proj_inj_bytes); try (rewrite proj_bytes_inj_value);
+  try (rewrite proj_inj_value); try (rewrite proj_inj_value_mismatch by congruence);
+  auto.
   rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
   rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
   rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
@@ -437,14 +508,10 @@ Opaque inj_pointer.
   rewrite decode_encode_int_4. auto.
   rewrite decode_encode_int_8. auto.
   rewrite decode_encode_int_8. auto.
-  rewrite decode_encode_int_4. auto.
-  rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single.
   rewrite decode_encode_int_8. auto.
-  rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
-  change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. 
-  unfold proj_pointer. generalize (check_inj_pointer b i 4%nat).
-Transparent inj_pointer. 
-  simpl. intros EQ; rewrite EQ; auto.
+  rewrite decode_encode_int_8. decEq. apply Float.of_to_bits.
+  rewrite decode_encode_int_4. auto.
+  rewrite decode_encode_int_4. decEq. apply Float32.of_to_bits.
 Qed.
 
 Lemma decode_encode_val_similar:
@@ -465,12 +532,8 @@ Lemma decode_val_type:
 Proof.
   intros. unfold decode_val. 
   destruct (proj_bytes cl). 
-  destruct chunk; simpl; auto. apply Float.single_of_bits_is_single.
   destruct chunk; simpl; auto.
-  unfold proj_pointer. destruct cl; try (exact I).
-  destruct m; try (exact I).
-  destruct (check_pointer 4%nat b i (Pointer b i n :: cl));
-  exact I.
+  destruct chunk; exact I || apply Val.load_result_type.
 Qed.
 
 Lemma encode_val_int8_signed_unsigned:
@@ -518,7 +581,6 @@ Lemma decode_val_cast:
   | Mint8unsigned => v = Val.zero_ext 8 v
   | Mint16signed => v = Val.sign_ext 16 v
   | Mint16unsigned => v = Val.zero_ext 16 v
-  | Mfloat32 => v = Val.singleoffloat v
   | _ => True
   end.
 Proof.
@@ -527,145 +589,132 @@ Proof.
   unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega. 
   unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. omega.
   unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. omega.
-  simpl. rewrite Float.singleoffloat_of_bits. auto.
 Qed.
 
 (** Pointers cannot be forged. *)
 
-Definition memval_valid_first (mv: memval) : Prop :=
-  match mv with
-  | Pointer b ofs n => n = 3%nat
-  | _ => True
-  end.
-
-Definition memval_valid_cont (mv: memval) : Prop :=
-  match mv with
-  | Pointer b ofs n => n <> 3%nat
-  | _ => True
+Definition quantity_chunk (chunk: memory_chunk) :=
+  match chunk with
+  | Mint64 | Mfloat64 | Many64 => Q64
+  | _ => Q32
   end.
 
-Inductive encoding_shape: list memval -> Prop :=
-  | encoding_shape_intro: forall mv1 mvl,
-      memval_valid_first mv1 ->
-      (forall mv, In mv mvl -> memval_valid_cont mv) ->
-      encoding_shape (mv1 :: mvl).
-
-Lemma encode_val_shape:
-  forall chunk v, encoding_shape (encode_val chunk v).
+Inductive shape_encoding (chunk: memory_chunk) (v: val): list memval -> Prop :=
+  | shape_encoding_f: forall q i mvl,
+      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+      q = quantity_chunk chunk ->
+      S i = size_quantity_nat q ->
+      (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
+      shape_encoding chunk v (Fragment v q i :: mvl)
+  | shape_encoding_b: forall b mvl,
+      match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
+      (forall mv, In mv mvl -> exists b', mv = Byte b') ->
+      shape_encoding chunk v (Byte b :: mvl)
+  | shape_encoding_u: forall mvl,
+      (forall mv, In mv mvl -> mv = Undef) ->
+      shape_encoding chunk v (Undef :: mvl).
+
+Lemma encode_val_shape: forall chunk v, shape_encoding chunk v (encode_val chunk v).
 Proof.
   intros. 
-  destruct (size_chunk_nat_pos chunk) as [sz1 EQ].
-  assert (A: encoding_shape (list_repeat (size_chunk_nat chunk) Undef)).
-    rewrite EQ; simpl; constructor. exact I. 
-    intros. replace mv with Undef. exact I. symmetry; eapply in_list_repeat; eauto.
-  assert (B: forall bl, length bl = size_chunk_nat chunk ->
-          encoding_shape (inj_bytes bl)).
-    intros. destruct bl; simpl in *. congruence. 
-    constructor. exact I. unfold inj_bytes. intros.
-    exploit list_in_map_inv; eauto. intros [x [C D]]. subst mv. exact I.
-  destruct v; auto; destruct chunk; simpl; auto; try (apply B; apply encode_int_length).
-  constructor. red. auto.
-  simpl; intros. intuition; subst mv; red; simpl; congruence.
-Qed.
-
-Lemma check_pointer_inv:
-  forall b ofs n mv,
-  check_pointer n b ofs mv = true -> mv = inj_pointer n b ofs.
-Proof.
-  induction n; destruct mv; simpl. 
-  auto.
-  congruence.
-  congruence.
-  destruct m; try congruence. intro. 
-  destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). 
-  destruct (andb_prop _ _ H2).
-  decEq. decEq. symmetry; eapply proj_sumbool_true; eauto.
-  symmetry; eapply proj_sumbool_true; eauto.
-  symmetry; apply beq_nat_true; auto.
-  auto.
+  destruct (size_chunk_nat_pos chunk) as [sz EQ]. 
+  assert (A: forall mv q n,
+             (n < size_quantity_nat q)%nat ->
+             In mv (inj_value_rec n v q) ->
+             exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q).
+  {
+    induction n; simpl; intros. contradiction. destruct H0. 
+    exists n; split; auto. omega. apply IHn; auto. omega. 
+  } 
+  assert (B: forall q,
+             q = quantity_chunk chunk -> 
+             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+             shape_encoding chunk v (inj_value q v)).
+  {
+Local Transparent inj_value.
+    intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ']. 
+    rewrite EQ'. simpl. constructor; auto.
+    intros; eapply A; eauto. omega. 
+  }
+  assert (C: forall bl,
+             match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
+             length (inj_bytes bl) = size_chunk_nat chunk ->
+             shape_encoding chunk v (inj_bytes bl)).
+  {
+    intros. destruct bl as [|b1 bl]. simpl in H0; congruence. simpl. 
+    constructor; auto. unfold inj_bytes; intros. exploit list_in_map_inv; eauto. 
+    intros (b & P & Q); exists b; auto.
+  }
+  assert (D: shape_encoding chunk v (list_repeat (size_chunk_nat chunk) Undef)).
+  {
+    intros. rewrite EQ; simpl; constructor; auto. 
+    intros. eapply in_list_repeat; eauto. 
+  }
+  generalize (encode_val_length chunk v). intros LEN. 
+  unfold encode_val; unfold encode_val in LEN; destruct v; destruct chunk; (apply B || apply C || apply D); auto; red; auto.
 Qed.
 
-Inductive decoding_shape: list memval -> Prop :=
-  | decoding_shape_intro: forall mv1 mvl,
-      memval_valid_first mv1 -> mv1 <> Undef ->
-      (forall mv, In mv mvl -> memval_valid_cont mv /\ mv <> Undef) ->
-      decoding_shape (mv1 :: mvl).
-
-Lemma decode_val_shape:
-  forall chunk mvl,
-  List.length mvl = size_chunk_nat chunk ->
-  decode_val chunk mvl = Vundef \/ decoding_shape mvl.
+Inductive shape_decoding (chunk: memory_chunk): list memval -> val -> Prop :=
+  | shape_decoding_f: forall v q i mvl,
+      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+      q = quantity_chunk chunk ->
+      S i = size_quantity_nat q ->
+      (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
+      shape_decoding chunk (Fragment v q i :: mvl) (Val.load_result chunk v)
+  | shape_decoding_b: forall b mvl v,
+      match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True |  _ => False end ->
+      (forall mv, In mv mvl -> exists b', mv = Byte b') ->
+      shape_decoding chunk (Byte b :: mvl) v
+  | shape_decoding_u: forall mvl,
+      shape_decoding chunk mvl Vundef.
+
+Lemma decode_val_shape: forall chunk mv1 mvl,
+  shape_decoding chunk (mv1 :: mvl) (decode_val chunk (mv1 :: mvl)).
 Proof.
-  intros. destruct (size_chunk_nat_pos chunk) as [sz EQ]. 
+  intros. 
+  assert (A: forall mv mvs bs, proj_bytes mvs = Some bs -> In mv mvs ->
+                               exists b, mv = Byte b).
+  {
+    induction mvs; simpl; intros. 
+    contradiction.
+    destruct a; try discriminate. destruct H0. exists i; auto. 
+    destruct (proj_bytes mvs); try discriminate. eauto. 
+  }
+  assert (B: forall v q mv n mvs,
+             check_value n v q mvs = true -> In mv mvs -> (n < size_quantity_nat q)%nat ->
+             exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q).
+  {
+    induction n; destruct mvs; simpl; intros; try discriminate.
+    contradiction.
+    destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. 
+    destruct H0. subst mv. exists n0; split; auto. omega. 
+    eapply IHn; eauto. omega.  
+  }
+  assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)).
+  {
+    intros. replace (Val.load_result chunk Vundef) with Vundef. constructor. 
+    destruct chunk; auto.
+  }
+  assert (C: forall q, size_quantity_nat q = size_chunk_nat chunk ->
+             (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
+             shape_decoding chunk (mv1 :: mvl) (Val.load_result chunk (proj_value q (mv1 :: mvl)))).
+  {
+    intros. unfold proj_value. destruct mv1; auto.
+    destruct (size_quantity_nat_pos q) as [sz EQ]. rewrite EQ. 
+    simpl. unfold proj_sumbool. rewrite dec_eq_true.
+    destruct (quantity_eq q q0); auto. 
+    destruct (beq_nat sz n) eqn:EQN; auto.
+    destruct (check_value sz v q mvl) eqn:CHECK; auto. 
+    simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. 
+    destruct H0 as [E|[E|E]]; subst chunk; destruct q; auto || discriminate.
+    congruence. 
+    intros. eapply B; eauto. omega. 
+  }
   unfold decode_val. 
-  caseEq (proj_bytes mvl).
-  intros bl PROJ. right. exploit inj_proj_bytes; eauto. intros. subst mvl.
-  destruct bl; simpl in H. congruence. simpl. constructor. 
-  red; auto. congruence.
-  unfold inj_bytes; intros. exploit list_in_map_inv; eauto. intros [b [A B]]. 
-  subst mv. split. red; auto. congruence.
-  intros. destruct chunk; auto. unfold proj_pointer.
-  destruct mvl; auto. destruct m; auto. 
-  caseEq (check_pointer 4%nat b i (Pointer b i n :: mvl)); auto.
-  intros. right. exploit check_pointer_inv; eauto. simpl; intros; inv H2.
-  constructor. red. auto. congruence. 
-  simpl; intros. intuition; subst mv; simpl; congruence.
-Qed.
-
-Lemma encode_val_pointer_inv:
-  forall chunk v b ofs n mvl,
-  encode_val chunk v = Pointer b ofs n :: mvl ->
-  chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3%nat b ofs.
-Proof.
-  intros until mvl.
-  assert (A: list_repeat (size_chunk_nat chunk) Undef = Pointer b ofs n :: mvl ->
-            chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs).
-    intros. destruct (size_chunk_nat_pos chunk) as [sz SZ]. rewrite SZ in H. simpl in H. discriminate.
-  assert (B: forall bl, length bl <> 0%nat -> inj_bytes bl = Pointer b ofs n :: mvl ->
-            chunk = Mint32 /\ v = Vptr b ofs /\ mvl = inj_pointer 3 b ofs).
-    intros. destruct bl; simpl in *; congruence.
-  unfold encode_val; destruct v; destruct chunk;
-  (apply A; assumption) ||
-  (apply B; rewrite encode_int_length; congruence) || idtac.
-  simpl. intros EQ; inv EQ; auto. 
-Qed.
-
-Lemma decode_val_pointer_inv:
-  forall chunk mvl b ofs,
-  decode_val chunk mvl = Vptr b ofs ->
-  chunk = Mint32 /\ mvl = inj_pointer 4%nat b ofs.
-Proof.
-  intros until ofs; unfold decode_val.
-  destruct (proj_bytes mvl). 
-  destruct chunk; congruence.
-  destruct chunk; try congruence.
-  unfold proj_pointer. destruct mvl. congruence. destruct m; try congruence.
-  case_eq (check_pointer 4%nat b0 i (Pointer b0 i n :: mvl)); intros.
-  inv H0. split; auto. apply check_pointer_inv; auto. 
-  congruence.
-Qed.
-
-Inductive pointer_encoding_shape: list memval -> Prop :=
-  | pointer_encoding_shape_intro: forall mv1 mvl,
-      ~memval_valid_cont mv1 ->
-      (forall mv, In mv mvl -> ~memval_valid_first mv) ->
-      pointer_encoding_shape (mv1 :: mvl).
-
-Lemma encode_pointer_shape:
-  forall b ofs, pointer_encoding_shape (encode_val Mint32 (Vptr b ofs)).
-Proof.
-  intros. simpl. constructor.
-  unfold memval_valid_cont. red; intro. elim H. auto. 
-  unfold memval_valid_first. simpl; intros; intuition; subst mv; congruence.
-Qed.
-
-Lemma decode_pointer_shape:
-  forall chunk mvl b ofs,
-  decode_val chunk mvl = Vptr b ofs ->
-  chunk = Mint32 /\ pointer_encoding_shape mvl.
-Proof.
-  intros. exploit decode_val_pointer_inv; eauto. intros [A B].
-  split; auto. subst mvl. apply encode_pointer_shape. 
+  destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. 
+  exploit (A mv1); eauto with coqlib. intros [b1 EQ1]; subst mv1. 
+  destruct chunk; (apply shape_decoding_u || apply shape_decoding_b); eauto with coqlib.
+  destruct chunk; (apply shape_decoding_u || apply C); auto. 
 Qed.
 
 (** * Compatibility with memory injections *)
@@ -675,18 +724,17 @@ Qed.
 Inductive memval_inject (f: meminj): memval -> memval -> Prop :=
   | memval_inject_byte:
       forall n, memval_inject f (Byte n) (Byte n)
-  | memval_inject_ptr:
-      forall b1 ofs1 b2 ofs2 delta n,
-      f b1 = Some (b2, delta) ->
-      ofs2 = Int.add ofs1 (Int.repr delta) ->
-      memval_inject f (Pointer b1 ofs1 n) (Pointer b2 ofs2 n)
+  | memval_inject_frag:
+      forall v1 v2 q n,
+      val_inject f v1 v2 ->
+      memval_inject f (Fragment v1 q n) (Fragment v2 q n)
   | memval_inject_undef:
       forall mv, memval_inject f Undef mv.
 
 Lemma memval_inject_incr:
   forall f f' v1 v2, memval_inject f v1 v2 -> inject_incr f f' -> memval_inject f' v1 v2.
 Proof.
-  intros. inv H; econstructor. rewrite (H0 _ _ _ H1). reflexivity. auto.
+  intros. inv H; econstructor. eapply val_inject_incr; eauto. 
 Qed.
 
 (** [decode_val], applied to lists of memory values that are pairwise
@@ -706,38 +754,33 @@ Proof.
   congruence.
 Qed.
 
-Lemma check_pointer_inject:
+Lemma check_value_inject:
   forall f vl vl',
   list_forall2 (memval_inject f) vl vl' ->
-  forall n b ofs b' delta,
-  check_pointer n b ofs vl = true ->
-  f b = Some(b', delta) ->
-  check_pointer n b' (Int.add ofs (Int.repr delta)) vl' = true.
+  forall v v' q n,
+  check_value n v q vl = true ->
+  val_inject f v v' -> v <> Vundef ->
+  check_value n v' q vl' = true.
 Proof.
   induction 1; intros; destruct n; simpl in *; auto. 
   inv H; auto.
-  destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H). 
-  destruct (andb_prop _ _ H5). 
-  assert (n = n0) by (apply beq_nat_true; auto).
-  assert (b = b0) by (eapply proj_sumbool_true; eauto). 
-  assert (ofs = ofs1) by (eapply proj_sumbool_true; eauto).
-  subst. rewrite H3 in H2; inv H2. 
-  unfold proj_sumbool. rewrite dec_eq_true. rewrite dec_eq_true. 
-  rewrite <- beq_nat_refl. simpl. eauto. 
-  congruence.
+  InvBooleans. assert (n = n0) by (apply beq_nat_true; auto). subst v1 q0 n0.
+  replace v2 with v'. 
+  unfold proj_sumbool; rewrite ! dec_eq_true. rewrite <- beq_nat_refl. simpl; eauto. 
+  inv H2; try discriminate; inv H4; congruence.
+  discriminate.
 Qed.
 
-Lemma proj_pointer_inject:
-  forall f vl1 vl2,
+Lemma proj_value_inject:
+  forall f q vl1 vl2,
   list_forall2 (memval_inject f) vl1 vl2 ->
-  val_inject f (proj_pointer vl1) (proj_pointer vl2).
+  val_inject f (proj_value q vl1) (proj_value q vl2).
 Proof.
-  intros. unfold proj_pointer.
+  intros. unfold proj_value. 
   inversion H; subst. auto. inversion H0; subst; auto.
-  case_eq (check_pointer 4%nat b0 ofs1 (Pointer b0 ofs1 n :: al)); intros.
-  exploit check_pointer_inject. eexact H. eauto. eauto. 
-  intro. rewrite H4. econstructor; eauto. 
-  constructor.
+  destruct (check_value (size_quantity_nat q) v1 q (Fragment v1 q0 n :: al)) eqn:B; auto.
+  destruct (Val.eq v1 Vundef). subst; auto. 
+  erewrite check_value_inject by eauto. auto.
 Qed.
 
 Lemma proj_bytes_not_inject:
@@ -754,9 +797,9 @@ Proof.
   auto.
 Qed.
 
-Lemma check_pointer_undef:
-  forall n b ofs vl,
-  In Undef vl -> check_pointer n b ofs vl = false.
+Lemma check_value_undef:
+  forall n q v vl,
+  In Undef vl -> check_value n v q vl = false.
 Proof.
   induction n; intros; simpl. 
   destruct vl. elim H. auto.
@@ -765,12 +808,12 @@ Proof.
   rewrite IHn; auto. apply andb_false_r. 
 Qed.
 
-Lemma proj_pointer_undef:
-  forall vl, In Undef vl -> proj_pointer vl = Vundef.
+Lemma proj_value_undef:
+  forall q vl, In Undef vl -> proj_value q vl = Vundef.
 Proof.
-  intros; unfold proj_pointer.
+  intros; unfold proj_value.
   destruct vl; auto. destruct m; auto. 
-  rewrite check_pointer_undef. auto. auto.
+  rewrite check_value_undef. auto. auto.
 Qed.
 
 Theorem decode_val_inject:
@@ -779,13 +822,20 @@ Theorem decode_val_inject:
   val_inject f (decode_val chunk vl1) (decode_val chunk vl2).
 Proof.
   intros. unfold decode_val. 
-  case_eq (proj_bytes vl1); intros. 
-  exploit proj_bytes_inject; eauto. intros. rewrite H1. 
+  destruct (proj_bytes vl1) as [bl1|] eqn:PB1.
+  exploit proj_bytes_inject; eauto. intros PB2. rewrite PB2. 
   destruct chunk; constructor.
+  assert (A: forall q fn,
+     val_inject f (Val.load_result chunk (proj_value q vl1))
+                  (match proj_bytes vl2 with
+                   | Some bl => fn bl
+                   | None => Val.load_result chunk (proj_value q vl2)
+                   end)).
+  { intros. destruct (proj_bytes vl2) as [bl2|] eqn:PB2.
+    rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence.
+    apply val_load_result_inject. apply proj_value_inject; auto.
+  }
   destruct chunk; auto.
-  case_eq (proj_bytes vl2); intros.
-  rewrite proj_pointer_undef. auto. eapply proj_bytes_not_inject; eauto. congruence.
-  apply proj_pointer_inject; auto.
 Qed.
 
 (** Symmetrically, [encode_val], applied to values related by [val_inject],
@@ -805,6 +855,13 @@ Proof.
   induction vl; simpl; constructor; auto. constructor. 
 Qed.  
 
+Lemma repeat_Undef_inject_encode_val:
+  forall f chunk v,
+  list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v).
+Proof.
+  intros. rewrite <- (encode_val_length chunk v). apply repeat_Undef_inject_any.
+Qed.
+
 Lemma repeat_Undef_inject_self:
   forall f n,
   list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef).
@@ -812,19 +869,24 @@ Proof.
   induction n; simpl; constructor; auto. constructor.
 Qed.  
 
+Lemma inj_value_inject:
+  forall f v1 v2 q, val_inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2).
+Proof.
+  intros.
+Local Transparent inj_value.
+  unfold inj_value. generalize (size_quantity_nat q). induction n; simpl; constructor; auto.
+  constructor; auto. 
+Qed.
+
 Theorem encode_val_inject:
   forall f v1 v2 chunk,
   val_inject f v1 v2 ->
   list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
 Proof.
-  intros. inv H; simpl.
-  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
-  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
-  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
-  destruct chunk; try (apply repeat_Undef_inject_self). 
-  repeat econstructor; eauto. 
-  replace (size_chunk_nat chunk) with (length (encode_val chunk v2)).
-  apply repeat_Undef_inject_any. apply encode_val_length. 
+  intros. inversion H; subst; simpl; destruct chunk;
+  auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val.
+  unfold encode_val. destruct v2; apply inj_value_inject; auto.
+  unfold encode_val. destruct v2; apply inj_value_inject; auto.
 Qed.
 
 Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.
@@ -832,8 +894,7 @@ Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.
 Lemma memval_lessdef_refl:
   forall mv, memval_lessdef mv mv.
 Proof.
-  red. destruct mv; econstructor.
-  unfold inject_id; reflexivity. rewrite Int.add_zero; auto. 
+  red. destruct mv; econstructor. apply val_inject_id. auto.
 Qed.
 
 (** [memval_inject] and compositions *)
@@ -845,9 +906,8 @@ Lemma memval_inject_compose:
 Proof.
   intros. inv H.
   inv H0. constructor.
-  inv H0. econstructor. 
-  unfold compose_meminj; rewrite H1; rewrite H5; eauto. 
-  rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints.
+  inv H0. econstructor.
+  eapply val_inject_compose; eauto. 
   constructor.
 Qed. 
 
@@ -905,28 +965,22 @@ Qed.
 Lemma decode_val_int64:
   forall l1 l2,
   length l1 = 4%nat -> length l2 = 4%nat ->
-  decode_val Mint64 (l1 ++ l2) =
-  Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
-                  (decode_val Mint32 (if Archi.big_endian then l2 else l1)).
+  Val.lessdef
+    (decode_val Mint64 (l1 ++ l2))
+    (Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
+                     (decode_val Mint32 (if Archi.big_endian then l2 else l1))).
 Proof.
   intros. unfold decode_val.
-  assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end).
-    intros. unfold proj_pointer. destruct vl; auto. destruct m; auto. 
-    destruct (check_pointer 4 b i (Pointer b i n :: vl)); auto. 
-  assert (PP1: forall vl v2, Val.longofwords (proj_pointer vl) v2 = Vundef).
-    intros. generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction.
-  assert (PP2: forall v1 vl, Val.longofwords v1 (proj_pointer vl) = Vundef).
-    intros. destruct v1; simpl; auto. 
-    generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction.
   rewrite proj_bytes_append. 
-  destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2.
-- exploit length_proj_bytes. eexact B1. rewrite H; intro L1.
+  destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2; auto.
+  exploit length_proj_bytes. eexact B1. rewrite H; intro L1.
   exploit length_proj_bytes. eexact B2. rewrite H0; intro L2.
   assert (UR: forall l, length l = 4%nat -> Int.unsigned (Int.repr (int_of_bytes l)) = int_of_bytes l).
     intros. apply Int.unsigned_repr. 
     generalize (int_of_bytes_range l). rewrite H1. 
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). 
     omega.
+  apply Val.lessdef_same.
   unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2.
   + rewrite <- (rev_length b1) in L1. 
     rewrite <- (rev_length b2) in L2.
@@ -938,9 +992,6 @@ Proof.
   + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal.
     rewrite !UR by auto. rewrite int_of_bytes_append. 
     rewrite L1. change (Z.of_nat 4 * 8) with 32. ring.
-- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
-- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
-- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
 Qed.
 
 Lemma bytes_of_int_append:
diff --git a/common/Memory.v b/common/Memory.v
index 9afdfd3..e45df66 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -690,7 +690,6 @@ Theorem load_cast:
   | Mint8unsigned => v = Val.zero_ext 8 v
   | Mint16signed => v = Val.sign_ext 16 v
   | Mint16unsigned => v = Val.zero_ext 16 v
-  | Mfloat32 => v = Val.singleoffloat v
   | _ => True
   end.
 Proof.
@@ -727,24 +726,6 @@ Proof.
   rewrite pred_dec_false; auto.
 Qed.
 
-(*
-Theorem load_float64al32:
-  forall m b ofs v,
-  load Mfloat64 m b ofs = Some v -> load Mfloat64al32 m b ofs = Some v.
-Proof.
-  unfold load; intros. destruct (valid_access_dec m Mfloat64 b ofs Readable); try discriminate.
-  rewrite pred_dec_true. assumption. 
-  apply valid_access_compat with Mfloat64; auto. simpl; omega. 
-Qed.
-
-Theorem loadv_float64al32:
-  forall m a v,
-  loadv Mfloat64 m a = Some v -> loadv Mfloat64al32 m a = Some v.
-Proof.
-  unfold loadv; intros. destruct a; auto. apply load_float64al32; auto.
-Qed.
-*)
-
 (** ** Properties related to [loadbytes] *)
 
 Theorem range_perm_loadbytes:
@@ -896,7 +877,7 @@ Theorem load_int64_split:
   exists v1 v2,
      load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
   /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
-  /\ v = Val.longofwords v1 v2.
+  /\ Val.lessdef v (Val.longofwords v1 v2).
 Proof.
   intros. 
   exploit load_valid_access; eauto. intros [A B]. simpl in *.
@@ -927,7 +908,7 @@ Theorem loadv_int64_split:
   exists v1 v2,
      loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
   /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
-  /\ v = Val.longofwords v1 v2.
+  /\ Val.lessdef v (Val.longofwords v1 v2).
 Proof.
   intros. destruct a; simpl in H; try discriminate.
   exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ).
@@ -1138,18 +1119,17 @@ Proof.
   red; intro; elim n0; red; intros; eauto with mem.
 Qed.
 
-Lemma setN_property:
-  forall (P: memval -> Prop) vl p q c,
-  (forall v, In v vl -> P v) ->
+Lemma setN_in:
+  forall vl p q c,
   p <= q < p + Z_of_nat (length vl) ->
-  P(ZMap.get q (setN vl p c)).
+  In (ZMap.get q (setN vl p c)) vl.
 Proof.
   induction vl; intros.
-  simpl in H0. omegaContradiction.
-  simpl length in H0. rewrite inj_S in H0. simpl. 
+  simpl in H. omegaContradiction.
+  simpl length in H. rewrite inj_S in H. simpl. 
   destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. 
   auto with coqlib. omega.
-  apply IHvl. auto with coqlib. omega.
+  right. apply IHvl. omega.
 Qed.
 
 Lemma getN_in:
@@ -1164,84 +1144,114 @@ Proof.
   right. apply IHn. omega. 
 Qed.
 
+End STORE.
+
+Local Hint Resolve perm_store_1 perm_store_2: mem.
+Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
+Local Hint Resolve store_valid_access_1 store_valid_access_2
+             store_valid_access_3: mem.
+
+Lemma load_store_overlap:
+  forall chunk m1 b ofs v m2 chunk' ofs' v',
+  store chunk m1 b ofs v = Some m2 ->
+  load chunk' m2 b ofs' = Some v' ->
+  ofs' + size_chunk chunk' > ofs ->
+  ofs + size_chunk chunk > ofs' ->
+  exists mv1 mvl mv1' mvl',
+      shape_encoding chunk v (mv1 :: mvl)
+  /\  shape_decoding chunk' (mv1' :: mvl') v'
+  /\  (   (ofs' = ofs /\ mv1' = mv1)
+       \/ (ofs' > ofs /\ In mv1' mvl)
+       \/ (ofs' < ofs /\ In mv1 mvl')).
+Proof.
+  intros. 
+  exploit load_result; eauto. erewrite store_mem_contents by eauto; simpl.
+  rewrite PMap.gss. 
+  set (c := (mem_contents m1)#b). intros V'. 
+  destruct (size_chunk_nat_pos chunk) as [sz SIZE]. 
+  destruct (size_chunk_nat_pos chunk') as [sz' SIZE'].
+  destruct (encode_val chunk v) as [ | mv1 mvl] eqn:ENC.
+  generalize (encode_val_length chunk v); rewrite ENC; simpl; congruence.
+  set (c' := setN (mv1::mvl) ofs c) in *.
+  exists mv1, mvl, (ZMap.get ofs' c'), (getN sz' (ofs' + 1) c').
+  split. rewrite <- ENC. apply encode_val_shape.
+  split. rewrite V', SIZE'. apply decode_val_shape. 
+  destruct (zeq ofs' ofs).
+- subst ofs'. left; split. auto. unfold c'. simpl. 
+  rewrite setN_outside by omega. apply ZMap.gss.
+- right. destruct (zlt ofs ofs').
+(* If ofs < ofs':  the load reads (at ofs') a continuation byte from the write.
+       ofs   ofs'   ofs+|chunk|
+        [-------------------]       write
+             [-------------------]  read
+*)
++ left; split. omega. unfold c'. simpl. apply setN_in. 
+  assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk).
+  { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. }
+  simpl length in H3. rewrite inj_S in H3. omega.
+(* If ofs > ofs':  the load reads (at ofs) the first byte from the write.
+       ofs'   ofs   ofs'+|chunk'|
+               [-------------------]  write
+         [----------------]           read
+*)
++ right; split. omega. replace mv1 with (ZMap.get ofs c'). 
+  apply getN_in. 
+  assert (size_chunk chunk' = Zsucc (Z.of_nat sz')).
+  { rewrite size_chunk_conv. rewrite SIZE'. rewrite inj_S; auto. }
+  omega.
+  unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss.
+Qed.
+
+Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
+  match chunk1, chunk2 with
+  | (Mint32 | Many32), (Mint32 | Many32) => True
+  | Many64, Many64 => True
+  | _, _ => False
+  end.
+
+Lemma compat_pointer_chunks_true:
+  forall chunk1 chunk2,
+  (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Many64) ->
+  (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Many64) ->
+  quantity_chunk chunk1 = quantity_chunk chunk2 ->
+  compat_pointer_chunks chunk1 chunk2.
+Proof.
+  intros. destruct H as [P|[P|P]]; destruct H0 as [Q|[Q|Q]];
+  subst; red; auto; discriminate.
+Qed.
+
 Theorem load_pointer_store:
-  forall chunk' b' ofs' v_b v_o,
+  forall chunk m1 b ofs v m2 chunk' b' ofs' v_b v_o,
+  store chunk m1 b ofs v = Some m2 ->
   load chunk' m2 b' ofs' = Some(Vptr v_b v_o) ->
-  (chunk = Mint32 /\ v = Vptr v_b v_o /\ chunk' = Mint32 /\ b' = b /\ ofs' = ofs)
+  (v = Vptr v_b v_o /\ compat_pointer_chunks chunk chunk' /\ b' = b /\ ofs' = ofs)
   \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs').
 Proof.
-  intros. exploit load_result; eauto. rewrite store_mem_contents; simpl. 
-  rewrite PMap.gsspec. destruct (peq b' b); auto. subst b'. intro DEC.
+  intros.
+  destruct (peq b' b); auto. subst b'.
   destruct (zle (ofs' + size_chunk chunk') ofs); auto.
   destruct (zle (ofs + size_chunk chunk) ofs'); auto.
-  destruct (size_chunk_nat_pos chunk) as [sz SZ].
-  destruct (size_chunk_nat_pos chunk') as [sz' SZ'].
-  exploit decode_pointer_shape; eauto. intros [CHUNK' PSHAPE]. clear CHUNK'.
-  generalize (encode_val_shape chunk v). intro VSHAPE.  
-  set (c := m1.(mem_contents)#b) in *.
-  set (c' := setN (encode_val chunk v) ofs c) in *.
-  destruct (zeq ofs ofs').
-
-(* 1.  ofs = ofs':  must be same chunks and same value *)
-  subst ofs'. inv VSHAPE. 
-  exploit decode_val_pointer_inv; eauto. intros [A B].
-  subst chunk'. simpl in B. inv B.
-  generalize H4. unfold c'. rewrite <- H0. simpl. 
-  rewrite setN_outside; try omega. rewrite ZMap.gss. intros.
-  exploit (encode_val_pointer_inv chunk v v_b v_o). 
-  rewrite <- H0. subst mv1. eauto. intros [C [D E]].
-  left; auto.
-
-  destruct (zlt ofs ofs').
-
-(* 2. ofs < ofs':
-
-      ofs   ofs'   ofs+|chunk|
-       [-------------------]       write
-            [-------------------]  read
-
-   The byte at ofs' satisfies memval_valid_cont (consequence of write).
-   For the read to return a pointer, it must satisfy ~memval_valid_cont. 
-*)
-  elimtype False.
-  assert (~memval_valid_cont (ZMap.get ofs' c')).
-    rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. auto.
-  assert (memval_valid_cont (ZMap.get ofs' c')).
-    inv VSHAPE. unfold c'. rewrite <- H1. simpl. 
-    apply setN_property. auto.
-    assert (length mvl = sz). 
-      generalize (encode_val_length chunk v). rewrite <- H1. rewrite SZ. 
-      simpl; congruence.
-    rewrite H4. rewrite size_chunk_conv in *. omega.
-  contradiction.
-
-(* 3. ofs > ofs':
-
-      ofs'   ofs   ofs'+|chunk'|
-              [-------------------]  write
-        [----------------]           read
-
-   The byte at ofs satisfies memval_valid_first (consequence of write).
-   For the read to return a pointer, it must satisfy ~memval_valid_first.
-*)
-  elimtype False.
-  assert (memval_valid_first (ZMap.get ofs c')).
-    inv VSHAPE. unfold c'. rewrite <- H0. simpl. 
-    rewrite setN_outside. rewrite ZMap.gss. auto. omega.
-  assert (~memval_valid_first (ZMap.get ofs c')).
-    rewrite SZ' in PSHAPE. simpl in PSHAPE. inv PSHAPE. 
-    apply H4. apply getN_in. rewrite size_chunk_conv in *.
-    rewrite SZ' in *. rewrite inj_S in *. omega.
-  contradiction.
+  exploit load_store_overlap; eauto. 
+  intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES).
+  inv DEC; try contradiction.
+  destruct CASES as [(A & B) | [(A & B) | (A & B)]].
+- (* Same offset *)
+  subst. inv ENC. 
+  assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64)
+  by (destruct chunk; auto || contradiction). 
+  left; split. rewrite H3.
+  destruct H4 as [P|[P|P]]; subst chunk'; destruct v0; simpl in H3; congruence.
+  split. apply compat_pointer_chunks_true; auto.
+  auto.
+- (* ofs' > ofs *)
+  inv ENC. 
+  + exploit H10; eauto. intros (j & P & Q). inv P. congruence.
+  + exploit H8; eauto. intros (n & P); congruence.
+  + exploit H2; eauto. congruence.
+- (* ofs' < ofs *)
+  exploit H7; eauto. intros (j & P & Q). subst mv1. inv ENC. congruence.
 Qed.
 
-End STORE.
-
-Local Hint Resolve perm_store_1 perm_store_2: mem.
-Local Hint Resolve store_valid_block_1 store_valid_block_2: mem.
-Local Hint Resolve store_valid_access_1 store_valid_access_2
-             store_valid_access_3: mem.
-
 Theorem load_store_pointer_overlap:
   forall chunk m1 b ofs v_b v_o m2 chunk' ofs' v,
   store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
@@ -1251,102 +1261,37 @@ Theorem load_store_pointer_overlap:
   ofs + size_chunk chunk > ofs' ->
   v = Vundef.
 Proof.
-  intros.
-  exploit store_mem_contents; eauto. intro ST.
-  exploit load_result; eauto. intro LD.
-  rewrite LD; clear LD.
-Opaque encode_val.
-  rewrite ST; simpl.
-  rewrite PMap.gss.
-  set (c := m1.(mem_contents)#b).
-  set (c' := setN (encode_val chunk (Vptr v_b v_o)) ofs c).
-  destruct (decode_val_shape chunk' (getN (size_chunk_nat chunk') ofs' c'))
-  as [OK | VSHAPE].
-  apply getN_length. 
-  exact OK.
-  elimtype False.
-  destruct (size_chunk_nat_pos chunk) as [sz SZ]. 
-  destruct (size_chunk_nat_pos chunk') as [sz' SZ']. 
-  assert (ENC: encode_val chunk (Vptr v_b v_o) = list_repeat (size_chunk_nat chunk) Undef
-               \/ pointer_encoding_shape (encode_val chunk (Vptr v_b v_o))).
-  destruct chunk; try (left; reflexivity). 
-  right. apply encode_pointer_shape. 
-  assert (GET: getN (size_chunk_nat chunk) ofs c' = encode_val chunk (Vptr v_b v_o)).
-  unfold c'. rewrite <- (encode_val_length chunk (Vptr v_b v_o)). 
-  apply getN_setN_same.
-  destruct (zlt ofs ofs').
-
-(* ofs < ofs':
-
-      ofs   ofs'   ofs+|chunk|
-       [-------------------]       write
-            [-------------------]  read
-
-   The byte at ofs' is Undef or not memval_valid_first (because write of pointer).
-   The byte at ofs' must be memval_valid_first and not Undef (otherwise load returns Vundef).
-*)
-  assert (memval_valid_first (ZMap.get ofs' c') /\ ZMap.get ofs' c' <> Undef).
-    rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. auto.
-  assert (~memval_valid_first (ZMap.get ofs' c') \/ ZMap.get ofs' c' = Undef).
-    unfold c'. destruct ENC.
-    right. apply setN_property. rewrite H5. intros. eapply in_list_repeat; eauto.
-    rewrite encode_val_length. rewrite <- size_chunk_conv. omega.
-    left. revert H5. rewrite <- GET. rewrite SZ. simpl. intros. inv H5.
-    apply setN_property. apply H9. rewrite getN_length.
-    rewrite size_chunk_conv in H3. rewrite SZ in H3. rewrite inj_S in H3. omega. 
-  intuition. 
-
-(* ofs > ofs':
-
-      ofs'   ofs   ofs'+|chunk'|
-              [-------------------]  write
-        [----------------]           read
-
-   The byte at ofs is Undef or not memval_valid_cont (because write of pointer).
-   The byte at ofs must be memval_valid_cont and not Undef (otherwise load returns Vundef).
-*)
-  assert (memval_valid_cont (ZMap.get ofs c') /\ ZMap.get ofs c' <> Undef).
-    rewrite SZ' in VSHAPE. simpl in VSHAPE. inv VSHAPE. 
-    apply H8. apply getN_in. rewrite size_chunk_conv in H2. 
-    rewrite SZ' in H2. rewrite inj_S in H2. omega. 
-  assert (~memval_valid_cont (ZMap.get ofs c') \/ ZMap.get ofs c' = Undef).
-    elim ENC. 
-    rewrite <- GET. rewrite SZ. simpl. intros. right; congruence.
-    rewrite <- GET. rewrite SZ. simpl. intros. inv H5. auto.
-  intuition.
+  intros. 
+  exploit load_store_overlap; eauto. 
+  intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES).
+  destruct CASES as [(A & B) | [(A & B) | (A & B)]].
+- congruence.
+- inv ENC. 
+  + exploit H9; eauto. intros (j & P & Q). subst mv1'. inv DEC. congruence. auto.
+  + contradiction.
+  + exploit H5; eauto. intros; subst. inv DEC; auto.
+- inv DEC. 
+  + exploit H10; eauto. intros (j & P & Q). subst mv1. inv ENC. congruence. 
+  + exploit H8; eauto. intros (n & P). subst mv1. inv ENC. contradiction. 
+  + auto.
 Qed.
 
 Theorem load_store_pointer_mismatch:
   forall chunk m1 b ofs v_b v_o m2 chunk' v,
   store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
   load chunk' m2 b ofs = Some v ->
-  chunk <> Mint32 \/ chunk' <> Mint32 ->
+  ~compat_pointer_chunks chunk chunk' ->
   v = Vundef.
 Proof.
   intros.
-  exploit store_mem_contents; eauto. intro ST.
-  exploit load_result; eauto. intro LD.
-  rewrite LD; clear LD.
-Opaque encode_val.
-  rewrite ST; simpl.
-  rewrite PMap.gss. 
-  set (c1 := m1.(mem_contents)#b).
-  set (e := encode_val chunk (Vptr v_b v_o)).
-  destruct (size_chunk_nat_pos chunk) as [sz SZ].
-  destruct (size_chunk_nat_pos chunk') as [sz' SZ'].
-  assert (match e with
-          | Undef :: _ => True
-          | Pointer _ _ _ :: _ => chunk = Mint32
-          | _ => False
-          end).
-Transparent encode_val.
-  unfold e, encode_val. rewrite SZ. destruct chunk; simpl; auto.
-  destruct e as [ | e1 el]. contradiction.
-  rewrite SZ'. simpl. rewrite setN_outside. rewrite ZMap.gss. 
-  destruct e1; try contradiction. 
-  destruct chunk'; auto. 
-  destruct chunk'; auto. intuition.
-  omega.
+  exploit load_store_overlap; eauto. 
+  generalize (size_chunk_pos chunk'); omega.
+  generalize (size_chunk_pos chunk); omega.
+  intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES).
+  destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try omegaContradiction.
+  inv ENC; inv DEC; auto.
+- elim H1. apply compat_pointer_chunks_true; auto.
+- contradiction.
 Qed.
 
 Lemma store_similar_chunks:
@@ -1403,16 +1348,6 @@ Theorem store_int16_sign_ext:
   store Mint16signed m b ofs (Vint n).
 Proof. intros. apply store_similar_chunks. apply encode_val_int16_sign_ext. auto. Qed.
 
-Theorem store_float32_truncate:
-  forall m b ofs n,
-  store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) =
-  store Mfloat32 m b ofs (Vfloat n).
-Proof.
-  intros. apply store_similar_chunks. simpl. decEq.
-  repeat rewrite encode_float32_eq. rewrite Float.bits_of_singleoffloat. auto.
-  auto.
-Qed.
-
 (*
 Theorem store_float64al32:
   forall m b ofs v m',
diff --git a/common/Memtype.v b/common/Memtype.v
index 37ab33c..1ab1cb7 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -310,7 +310,6 @@ Axiom load_cast:
   | Mint8unsigned => v = Val.zero_ext 8 v
   | Mint16signed => v = Val.sign_ext 16 v
   | Mint16unsigned => v = Val.zero_ext 16 v
-  | Mfloat32 => v = Val.singleoffloat v
   | _ => True
   end.
 
@@ -443,6 +442,13 @@ Axiom load_store_other:
 
 (** Integrity of pointer values. *)
 
+Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop :=
+  match chunk1, chunk2 with
+  | (Mint32 | Many32), (Mint32 | Many32) => True
+  | Many64, Many64 => True
+  | _, _ => False
+  end.
+
 Axiom load_store_pointer_overlap:
   forall chunk m1 b ofs v_b v_o m2 chunk' ofs' v,
   store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
@@ -455,13 +461,13 @@ Axiom load_store_pointer_mismatch:
   forall chunk m1 b ofs v_b v_o m2 chunk' v,
   store chunk m1 b ofs (Vptr v_b v_o) = Some m2 ->
   load chunk' m2 b ofs = Some v ->
-  chunk <> Mint32 \/ chunk' <> Mint32 ->
+  ~compat_pointer_chunks chunk chunk' ->
   v = Vundef.
 Axiom load_pointer_store:
-  forall chunk m1 b ofs v m2, store chunk m1 b ofs v = Some m2 ->
-  forall chunk' b' ofs' v_b v_o,
+  forall chunk m1 b ofs v m2 chunk' b' ofs' v_b v_o,
+  store chunk m1 b ofs v = Some m2 ->
   load chunk' m2 b' ofs' = Some(Vptr v_b v_o) ->
-  (chunk = Mint32 /\ v = Vptr v_b v_o /\ chunk' = Mint32 /\ b' = b /\ ofs' = ofs)
+  (v = Vptr v_b v_o /\ compat_pointer_chunks chunk chunk' /\ b' = b /\ ofs' = ofs)
   \/ (b' <> b \/ ofs' + size_chunk chunk' <= ofs \/ ofs + size_chunk chunk <= ofs').
 
 (** Load-store properties for [loadbytes]. *)
@@ -500,10 +506,6 @@ Axiom store_int16_sign_ext:
   forall m b ofs n,
   store Mint16signed m b ofs (Vint (Int.sign_ext 16 n)) =
   store Mint16signed m b ofs (Vint n).
-Axiom store_float32_truncate:
-  forall m b ofs n,
-  store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) =
-  store Mfloat32 m b ofs (Vfloat n).
 
 (** ** Properties of [storebytes]. *)
 
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 329c0c7..c0eab04 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -21,6 +21,8 @@ let name_of_type = function
   | Tfloat -> "float"
   | Tlong -> "long"
   | Tsingle -> "single"
+  | Tany32 -> "any32"
+  | Tany64 -> "any64"
 
 let name_of_chunk = function
   | Mint8signed -> "int8s"
@@ -31,6 +33,8 @@ let name_of_chunk = function
   | Mint64 -> "int64"
   | Mfloat32 -> "float32"
   | Mfloat64 -> "float64"
+  | Many32 -> "any32"
+  | Many64 -> "any64"
 
 let name_of_external = function
   | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name)
diff --git a/common/Values.v b/common/Values.v
index 5ac9f3e..a12fb63 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -38,6 +38,7 @@ Inductive val: Type :=
   | Vint: int -> val
   | Vlong: int64 -> val
   | Vfloat: float -> val
+  | Vsingle: float32 -> val
   | Vptr: block -> int -> val.
 
 Definition Vzero: val := Vint Int.zero.
@@ -55,14 +56,28 @@ Definition Vfalse: val := Vint Int.zero.
 
 Module Val.
 
+Definition eq (x y: val): {x=y} + {x<>y}.
+Proof.
+  decide equality. 
+  apply Int.eq_dec.
+  apply Int64.eq_dec.
+  apply Float.eq_dec.
+  apply Float32.eq_dec.
+  apply Int.eq_dec.
+  apply eq_block.
+Defined.
+Global Opaque eq.
+
 Definition has_type (v: val) (t: typ) : Prop :=
   match v, t with
   | Vundef, _ => True
   | Vint _, Tint => True
   | Vlong _, Tlong => True
   | Vfloat _, Tfloat => True
-  | Vfloat f, Tsingle => Float.is_single f
+  | Vsingle _, Tsingle => True
   | Vptr _ _, Tint => True
+  | (Vint _ | Vptr _ _ | Vsingle _), Tany32 => True
+  | _, Tany64 => True
   | _, _ => False
   end.
 
@@ -83,8 +98,8 @@ Lemma has_subtype:
   forall ty1 ty2 v,
   subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2.
 Proof.
-  intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac.
-  unfold has_type in *. destruct v; auto. 
+  intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac;
+  unfold has_type in *; destruct v; auto.
 Qed.
 
 Lemma has_subtype_list:
@@ -126,30 +141,66 @@ Definition absf (v: val) : val :=
   | _ => Vundef
   end.
 
+Definition negfs (v: val) : val :=
+  match v with
+  | Vsingle f => Vsingle (Float32.neg f)
+  | _ => Vundef
+  end.
+
+Definition absfs (v: val) : val :=
+  match v with
+  | Vsingle f => Vsingle (Float32.abs f)
+  | _ => Vundef
+  end.
+
 Definition maketotal (ov: option val) : val :=
   match ov with Some v => v | None => Vundef end.
 
 Definition intoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => option_map Vint (Float.intoffloat f)
+  | Vfloat f => option_map Vint (Float.to_int f)
   | _ => None
   end.
 
 Definition intuoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => option_map Vint (Float.intuoffloat f)
+  | Vfloat f => option_map Vint (Float.to_intu f)
   | _ => None
   end.
 
 Definition floatofint (v: val) : option val :=
   match v with
-  | Vint n => Some (Vfloat (Float.floatofint n))
+  | Vint n => Some (Vfloat (Float.of_int n))
   | _ => None
   end.
 
 Definition floatofintu (v: val) : option val :=
   match v with
-  | Vint n => Some (Vfloat (Float.floatofintu n))
+  | Vint n => Some (Vfloat (Float.of_intu n))
+  | _ => None
+  end.
+
+Definition intofsingle (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_int f)
+  | _ => None
+  end.
+
+Definition intuofsingle (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vint (Float32.to_intu f)
+  | _ => None
+  end.
+
+Definition singleofint (v: val) : option val :=
+  match v with
+  | Vint n => Some (Vsingle (Float32.of_int n))
+  | _ => None
+  end.
+
+Definition singleofintu (v: val) : option val :=
+  match v with
+  | Vint n => Some (Vsingle (Float32.of_intu n))
   | _ => None
   end.
 
@@ -195,7 +246,13 @@ Definition sign_ext (nbits: Z) (v: val) : val :=
 
 Definition singleoffloat (v: val) : val :=
   match v with
-  | Vfloat f => Vfloat(Float.singleoffloat f)
+  | Vfloat f => Vsingle (Float.to_single f)
+  | _ => Vundef
+  end.
+
+Definition floatofsingle (v: val) : val :=
+  match v with
+  | Vsingle f => Vfloat (Float.of_single f)
   | _ => Vundef
   end.
 
@@ -394,6 +451,30 @@ Definition floatofwords (v1 v2: val) : val :=
   | _, _ => Vundef
   end.
 
+Definition addfs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 => Vsingle(Float32.add f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition subfs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 => Vsingle(Float32.sub f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition mulfs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 => Vsingle(Float32.mul f1 f2)
+  | _, _ => Vundef
+  end.
+
+Definition divfs (v1 v2: val): val :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 => Vsingle(Float32.div f1 f2)
+  | _, _ => Vundef
+  end.
+
 (** Operations on 64-bit integers *)
 
 Definition longofwords (v1 v2: val) : val :=
@@ -440,37 +521,49 @@ Definition longofintu (v: val) : val :=
 
 Definition longoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => option_map Vlong (Float.longoffloat f)
+  | Vfloat f => option_map Vlong (Float.to_long f)
   | _ => None
   end.
 
 Definition longuoffloat (v: val) : option val :=
   match v with
-  | Vfloat f => option_map Vlong (Float.longuoffloat f)
+  | Vfloat f => option_map Vlong (Float.to_longu f)
+  | _ => None
+  end.
+
+Definition longofsingle (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_long f)
+  | _ => None
+  end.
+
+Definition longuofsingle (v: val) : option val :=
+  match v with
+  | Vsingle f => option_map Vlong (Float32.to_longu f)
   | _ => None
   end.
 
 Definition floatoflong (v: val) : option val :=
   match v with
-  | Vlong n => Some (Vfloat (Float.floatoflong n))
+  | Vlong n => Some (Vfloat (Float.of_long n))
   | _ => None
   end.
 
 Definition floatoflongu (v: val) : option val :=
   match v with
-  | Vlong n => Some (Vfloat (Float.floatoflongu n))
+  | Vlong n => Some (Vfloat (Float.of_longu n))
   | _ => None
   end.
 
 Definition singleoflong (v: val) : option val :=
   match v with
-  | Vlong n => Some (Vfloat (Float.singleoflong n))
+  | Vlong n => Some (Vsingle (Float32.of_long n))
   | _ => None
   end.
 
 Definition singleoflongu (v: val) : option val :=
   match v with
-  | Vlong n => Some (Vfloat (Float.singleoflongu n))
+  | Vlong n => Some (Vsingle (Float32.of_longu n))
   | _ => None
   end.
 
@@ -625,6 +718,12 @@ Definition cmpf_bool (c: comparison) (v1 v2: val): option bool :=
   | _, _ => None
   end.
 
+Definition cmpfs_bool (c: comparison) (v1 v2: val): option bool :=
+  match v1, v2 with
+  | Vsingle f1, Vsingle f2 => Some (Float32.cmp c f1 f2)
+  | _, _ => None
+  end.
+
 Definition cmpl_bool (c: comparison) (v1 v2: val): option bool :=
   match v1, v2 with
   | Vlong n1, Vlong n2 => Some (Int64.cmp c n1 n2)
@@ -649,6 +748,9 @@ Definition cmpu (c: comparison) (v1 v2: val): val :=
 Definition cmpf (c: comparison) (v1 v2: val): val :=
   of_optbool (cmpf_bool c v1 v2).
 
+Definition cmpfs (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmpfs_bool c v1 v2).
+
 Definition cmpl (c: comparison) (v1 v2: val): option val :=
   option_map of_bool (cmpl_bool c v1 v2).
 
@@ -681,22 +783,23 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | Mint32, Vint n => Vint n
   | Mint32, Vptr b ofs => Vptr b ofs
   | Mint64, Vlong n => Vlong n
-  | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
+  | Mfloat32, Vsingle f => Vsingle f
   | Mfloat64, Vfloat f => Vfloat f
+  | Many32, (Vint _ | Vptr _ _ | Vsingle _) => v
+  | Many64, _ => v
   | _, _ => Vundef
   end.
 
 Lemma load_result_type:
   forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk).
 Proof.
-  intros. destruct chunk; destruct v; simpl; auto. apply Float.singleoffloat_is_single.
+  intros. destruct chunk; destruct v; simpl; auto.
 Qed.
 
 Lemma load_result_same:
   forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v.
 Proof.
   unfold has_type; intros. destruct v; destruct ty; try contradiction; auto.
-  simpl. rewrite Float.singleoffloat_of_single; auto. 
 Qed.
 
 (** Theorems on arithmetic operations. *)
@@ -1388,6 +1491,8 @@ Inductive val_inject (mi: meminj): val -> val -> Prop :=
       forall i, val_inject mi (Vlong i) (Vlong i)
   | val_inject_float:
       forall f, val_inject mi (Vfloat f) (Vfloat f)
+  | val_inject_single:
+      forall f, val_inject mi (Vsingle f) (Vsingle f)
   | val_inject_ptr:
       forall b1 ofs1 b2 ofs2 delta,
       mi b1 = Some (b2, delta) ->