Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.

lib/Integers.v: added more properties for ARM port.
lib/Coqlib.v: added more properties for division and powers of 2.


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

15 files changed, 844 insertions, 367 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 910eaa44..b6186f2e 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -230,10 +230,10 @@ Definition eval_constant (sp: val) (cst: constant) : option val :=
 
 Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   match op, arg with
-  | Ocast8unsigned, _ => Some (Val.cast8unsigned arg)
-  | Ocast8signed, _ => Some (Val.cast8signed arg)
-  | Ocast16unsigned, _ => Some (Val.cast16unsigned arg)
-  | Ocast16signed, _ => Some (Val.cast16signed arg)
+  | Ocast8unsigned, _ => Some (Val.zero_ext 8 arg)
+  | Ocast8signed, _ => Some (Val.sign_ext 8 arg)
+  | Ocast16unsigned, _ => Some (Val.zero_ext 16 arg)
+  | Ocast16signed, _ => Some (Val.sign_ext 16 arg)
   | Onegint, Vint n1 => Some (Vint (Int.neg n1))
   | Onotbool, Vint n1 => Some (Val.of_bool (Int.eq n1 Int.zero))
   | Onotbool, Vptr b1 n1 => Some Vfalse
diff --git a/backend/Constprop.v b/backend/Constprop.v
index e7feb101..75fb1486 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -219,10 +219,10 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | Ointconst n, nil => I n
   | Ofloatconst n, nil => F n
   | Oaddrsymbol s n, nil => S s n
-  | Ocast8signed, I n1 :: nil => I(Int.cast8signed n)
-  | Ocast8unsigned, I n1 :: nil => I(Int.cast8unsigned n)
-  | Ocast16signed, I n1 :: nil => I(Int.cast16signed n)
-  | Ocast16unsigned, I n1 :: nil => I(Int.cast16unsigned n)
+  | Ocast8signed, I n1 :: nil => I(Int.sign_ext 8 n)
+  | Ocast8unsigned, I n1 :: nil => I(Int.zero_ext 8 n)
+  | Ocast16signed, I n1 :: nil => I(Int.sign_ext 16 n)
+  | Ocast16unsigned, I n1 :: nil => I(Int.zero_ext 16 n)
   | Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
   | Oadd, S s1 n1 :: I n2 :: nil => S s1 (Int.add n1 n2)
   | Oaddimm n, I n1 :: nil => I (Int.add n1 n)
@@ -533,9 +533,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
   | eval_static_operation_case4 s n =>
       S s n
   | eval_static_operation_case6 n1 =>
-      I(Int.cast8signed n1)
+      I(Int.sign_ext 8 n1)
   | eval_static_operation_case7 n1 =>
-      I(Int.cast16signed n1)
+      I(Int.sign_ext 16 n1)
   | eval_static_operation_case8 n1 n2 =>
       I(Int.add n1 n2)
   | eval_static_operation_case9 s1 n1 n2 =>
@@ -618,9 +618,9 @@ Definition eval_static_operation (op: operation) (vl: list approx) :=
       | Some b => I(if b then Int.one else Int.zero)
       end
   | eval_static_operation_case48 n1 =>
-      I(Int.cast8unsigned n1)
+      I(Int.zero_ext 8 n1)
   | eval_static_operation_case49 n1 =>
-      I(Int.cast16unsigned n1)
+      I(Int.zero_ext 16 n1)
   | eval_static_operation_case50 n1 =>
       I(Float.intuoffloat n1)
   | eval_static_operation_default op vl =>
diff --git a/backend/Op.v b/backend/Op.v
index 707bcb0a..5665d725 100644
--- a/backend/Op.v
+++ b/backend/Op.v
@@ -175,10 +175,10 @@ Definition eval_operation
       | Some b => Some (Vptr b ofs)
       end
   | Oaddrstack ofs, nil => offset_sp sp ofs
-  | Ocast8signed, v1 :: nil => Some (Val.cast8signed v1)
-  | Ocast8unsigned, v1 :: nil => Some (Val.cast8unsigned v1)
-  | Ocast16signed, v1 :: nil => Some (Val.cast16signed v1)
-  | Ocast16unsigned, v1 :: nil => Some (Val.cast16unsigned v1)
+  | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
+  | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
+  | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
+  | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1)
   | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2))
   | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1))
   | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2))
@@ -632,10 +632,10 @@ Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val :
   | Ofloatconst n, nil => Vfloat n
   | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs
   | Oaddrstack ofs, nil => Val.add sp (Vint ofs)
-  | Ocast8signed, v1::nil => Val.cast8signed v1
-  | Ocast8unsigned, v1::nil => Val.cast8unsigned v1
-  | Ocast16signed, v1::nil => Val.cast16signed v1
-  | Ocast16unsigned, v1::nil => Val.cast16unsigned v1
+  | Ocast8signed, v1::nil => Val.sign_ext 8 v1
+  | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1
+  | Ocast16signed, v1::nil => Val.sign_ext 16 v1
+  | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1
   | Oadd, v1::v2::nil => Val.add v1 v2
   | Oaddimm n, v1::nil => Val.add v1 (Vint n)
   | Osub, v1::v2::nil => Val.sub v1 v2
@@ -843,10 +843,10 @@ Proof.
   exists v2; auto.
   destruct (Genv.find_symbol genv i); inv H0. TrivialExists.
   exists v1; auto.
-  exists (Val.cast8signed v2); split. auto. apply Val.cast8signed_lessdef; auto.
-  exists (Val.cast8unsigned v2); split. auto. apply Val.cast8unsigned_lessdef; auto.
-  exists (Val.cast16signed v2); split. auto. apply Val.cast16signed_lessdef; auto.
-  exists (Val.cast16unsigned v2); split. auto. apply Val.cast16unsigned_lessdef; auto.
+  exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+  exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto.
+  exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto.
+  exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto.
   destruct (eq_block b b0); inv H0. TrivialExists.
   destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
   destruct (Int.eq i0 Int.zero); inv H0; TrivialExists.
diff --git a/backend/PPC.v b/backend/PPC.v
index 13c7a875..e47cba01 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -616,9 +616,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Peqv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.notint (Val.xor rs#r1 rs#r2)))) m
   | Pextsb rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.cast8signed rs#r1))) m
+      OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m
   | Pextsh rd r1 =>
-      OK (nextinstr (rs#rd <- (Val.cast16signed rs#r1))) m
+      OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m
   | Pfreeframe ofs =>
       match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with
       | None => Error
diff --git a/backend/PPCgen.v b/backend/PPCgen.v
index 1484a1e6..faedcb1c 100644
--- a/backend/PPCgen.v
+++ b/backend/PPCgen.v
@@ -80,7 +80,7 @@ Definition freg_of (r: mreg) : freg :=
 
 Definition low_u (n: int) := Int.and n (Int.repr 65535).
 Definition high_u (n: int) := Int.shru n (Int.repr 16).
-Definition low_s (n: int) := Int.cast16signed n.
+Definition low_s (n: int) := Int.sign_ext 16 n.
 Definition high_s (n: int) := Int.shru (Int.sub n (low_s n)) (Int.repr 16).
 
 (** Smart constructors for arithmetic operations involving
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index fd5843b1..6db8b477 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -567,14 +567,14 @@ Qed.
 Lemma loadv_8_signed_unsigned:
   forall m a,
   Mem.loadv Mint8signed m a = 
-    option_map Val.cast8signed (Mem.loadv Mint8unsigned m a).
+    option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a).
 Proof.
   intros. unfold Mem.loadv. destruct a; try reflexivity.
   unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned).
   destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto.
   simpl.
   destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto.
-  simpl. rewrite Int.cast8_signed_unsigned. auto.
+  simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. 
   auto.
 Qed.
 
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v
index ba347ea9..dd142c5b 100644
--- a/backend/PPCgenproof1.v
+++ b/backend/PPCgenproof1.v
@@ -95,7 +95,8 @@ Proof.
   rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
   omega.
   eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. 
-  unfold low_s. unfold Int.cast16signed. 
+  unfold low_s. unfold Int.sign_ext. 
+  change (two_p 16) with 65536. change (two_p (16-1)) with 32768. 
   set (N := Int.unsigned n).
   case (zlt (N mod 65536) 32768); intro.
   apply H0 with (N - N mod 65536). auto with ints.
@@ -1273,19 +1274,19 @@ Proof.
   (* Ocast8unsigned *)
   exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))).
   split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.cast8unsigned (ms m0))
+  replace (Val.zero_ext 8 (ms m0))
       with (Val.rolm (ms m0) Int.zero (Int.repr 255)).
   auto with ppcgen. 
-  unfold Val.rolm, Val.cast8unsigned. destruct (ms m0); auto. 
-  rewrite Int.rolm_zero. rewrite Int.cast8unsigned_and. auto.
+  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Ocast16unsigned *)
   exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))).
   split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity.
-  replace (Val.cast16unsigned (ms m0))
+  replace (Val.zero_ext 16 (ms m0))
       with (Val.rolm (ms m0) Int.zero (Int.repr 65535)).
   auto with ppcgen. 
-  unfold Val.rolm, Val.cast16unsigned. destruct (ms m0); auto. 
-  rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto.
+  unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. 
+  rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto.
   (* Oaddimm *)
   generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m
                             (ireg_of_not_GPR12 m0)).
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index b7794883..6d629794 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -748,40 +748,44 @@ Qed.
 Theorem eval_cast8signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8signed a) (Val.cast8signed v).
+  eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v).
 Proof. 
   intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_signed_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast8unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast8unsigned a) (Val.cast8unsigned v).
+  eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v).
 Proof. 
   intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast8_unsigned_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast16signed:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16signed a) (Val.cast16signed v).
+  eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v).
 Proof. 
   intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_signed_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.sign_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
 Theorem eval_cast16unsigned:
   forall le a v,
   eval_expr ge sp e m le a v ->
-  eval_expr ge sp e m le (cast16unsigned a) (Val.cast16unsigned v).
+  eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v).
 Proof. 
   intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
-  EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.cast16_unsigned_idem. reflexivity.
+  EvalOp. simpl. subst v. destruct v1; simpl; auto.
+  rewrite Int.zero_ext_idem. reflexivity. compute; auto.
   EvalOp.
 Qed.
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9dfb5732..e1224bd1 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -962,16 +962,16 @@ Lemma make_cast_correct:
 Proof.
   intros. destruct chunk; simpl make_cast.
 
-  exists (Val.cast8signed tv). 
+  exists (Val.sign_ext 8 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast8unsigned tv). 
+  exists (Val.zero_ext 8 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast16signed tv). 
+  exists (Val.sign_ext 16 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
-  exists (Val.cast16unsigned tv). 
+  exists (Val.zero_ext 16 tv). 
   split. eauto with evalexpr. inversion H0; simpl; constructor.
 
   exists tv.
@@ -1025,10 +1025,10 @@ Proof.
   inv H; simpl in H6; inv H6;
   econstructor; (split; [eauto|idtac]);
   destruct v1; simpl in H0; inv H0; try (constructor; constructor).
-  apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem.
-  apply val_content_inject_8; auto. apply Int.cast8_unsigned_signed. 
-  apply val_content_inject_16; auto. apply Int.cast16_unsigned_idem. 
-  apply val_content_inject_16; auto. apply Int.cast16_unsigned_signed. 
+  apply val_content_inject_8. auto. apply Int.zero_ext_idem. compute; auto.
+  apply val_content_inject_8; auto. apply Int.zero_ext_sign_ext. compute; auto.
+  apply val_content_inject_16; auto. apply Int.zero_ext_idem. compute; auto.
+  apply val_content_inject_16; auto. apply Int.zero_ext_sign_ext. compute; auto.
   apply val_content_inject_32. apply Float.singleoffloat_idem. 
 Qed.
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 22139127..14b8053d 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -351,10 +351,10 @@ Definition sem_binary_operation
 
 Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   match sz, sg with
-  | I8, Signed => Int.cast8signed i
-  | I8, Unsigned => Int.cast8unsigned i
-  | I16, Signed => Int.cast16signed i
-  | I16, Unsigned => Int.cast16unsigned i 
+  | I8, Signed => Int.sign_ext 8 i
+  | I8, Unsigned => Int.zero_ext 8 i
+  | I16, Signed => Int.sign_ext 16 i
+  | I16, Unsigned => Int.zero_ext 16 i 
   | I32 , _ => i
   end.
 
diff --git a/common/Mem.v b/common/Mem.v
index 35d93ed7..3db2ceba 100644
--- a/common/Mem.v
+++ b/common/Mem.v
@@ -1932,12 +1932,12 @@ Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop :=
   | val_content_inject_8:
       forall chunk n1 n2,
       chunk = Mint8unsigned \/ chunk = Mint8signed ->
-      Int.cast8unsigned n1 = Int.cast8unsigned n2 ->
+      Int.zero_ext 8 n1 = Int.zero_ext 8 n2 ->
       val_content_inject f chunk (Vint n1) (Vint n2)
   | val_content_inject_16:
       forall chunk n1 n2,
       chunk = Mint16unsigned \/ chunk = Mint16signed ->
-      Int.cast16unsigned n1 = Int.cast16unsigned n2 ->
+      Int.zero_ext 16 n1 = Int.zero_ext 16 n2 ->
       val_content_inject f chunk (Vint n1) (Vint n2)
   | val_content_inject_32:
       forall f1 f2,
@@ -1957,20 +1957,20 @@ Proof.
 
   elim H1; intro; subst chunk;
   destruct chunk'; simpl in H0; try discriminate; simpl.
-  replace (Int.cast8signed n1) with (Int.cast8signed n2).
-  constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+  replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2).
+  constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
   rewrite H2. constructor.
-  replace (Int.cast8signed n1) with (Int.cast8signed n2).
-  constructor. apply Int.cast8_signed_equal_if_unsigned_equal; auto.
+  replace (Int.sign_ext 8 n1) with (Int.sign_ext 8 n2).
+  constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
   rewrite H2. constructor.
 
   elim H1; intro; subst chunk;
   destruct chunk'; simpl in H0; try discriminate; simpl.
-  replace (Int.cast16signed n1) with (Int.cast16signed n2).
-  constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+  replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2).
+  constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
   rewrite H2. constructor.
-  replace (Int.cast16signed n1) with (Int.cast16signed n2).
-  constructor. apply Int.cast16_signed_equal_if_unsigned_equal; auto.
+  replace (Int.sign_ext 16 n1) with (Int.sign_ext 16 n2).
+  constructor. apply Int.sign_ext_equal_if_zero_equal; auto. compute; auto.
   rewrite H2. constructor.
 
   destruct chunk'; simpl in H0; try discriminate; simpl.
diff --git a/common/Values.v b/common/Values.v
index 19772446..27d4f50c 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -150,27 +150,15 @@ Definition notbool (v: val) : val :=
   | _ => Vundef
   end.
 
-Definition cast8signed (v: val) : val :=
+Definition zero_ext (nbits: Z) (v: val) : val :=
   match v with
-  | Vint n => Vint(Int.cast8signed n)
+  | Vint n => Vint(Int.zero_ext nbits n)
   | _ => Vundef
   end.
 
-Definition cast8unsigned (v: val) : val :=
+Definition sign_ext (nbits: Z) (v: val) : val :=
   match v with
-  | Vint n => Vint(Int.cast8unsigned n)
-  | _ => Vundef
-  end.
-
-Definition cast16signed (v: val) : val :=
-  match v with
-  | Vint n => Vint(Int.cast16signed n)
-  | _ => Vundef
-  end.
-
-Definition cast16unsigned (v: val) : val :=
-  match v with
-  | Vint n => Vint(Int.cast16unsigned n)
+  | Vint n => Vint(Int.sign_ext nbits n)
   | _ => Vundef
   end.
 
@@ -300,6 +288,15 @@ Definition rolm (v: val) (amount mask: int): val :=
   | _ => Vundef
   end.
 
+Definition ror (v1 v2: val): val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 =>
+     if Int.ltu n2 (Int.repr 32)
+     then Vint(Int.ror n1 n2)
+     else Vundef
+  | _, _ => Vundef
+  end.
+
 Definition addf (v1 v2: val): val :=
   match v1, v2 with
   | Vfloat f1, Vfloat f2 => Vfloat(Float.add f1 f2)
@@ -377,10 +374,10 @@ Definition cmpf (c: comparison) (v1 v2: val): val :=
 
 Definition load_result (chunk: memory_chunk) (v: val) :=
   match chunk, v with
-  | Mint8signed, Vint n => Vint (Int.cast8signed n)
-  | Mint8unsigned, Vint n => Vint (Int.cast8unsigned n)
-  | Mint16signed, Vint n => Vint (Int.cast16signed n)
-  | Mint16unsigned, Vint n => Vint (Int.cast16unsigned n)
+  | Mint8signed, Vint n => Vint (Int.sign_ext 8 n)
+  | Mint8unsigned, Vint n => Vint (Int.zero_ext 8 n)
+  | Mint16signed, Vint n => Vint (Int.sign_ext 16 n)
+  | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n)
   | Mint32, Vint n => Vint n
   | Mint32, Vptr b ofs => Vptr b ofs
   | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
@@ -391,15 +388,17 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
 (** Theorems on arithmetic operations. *)
 
 Theorem cast8unsigned_and:
-  forall x, cast8unsigned x = and x (Vint(Int.repr 255)).
+  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
 Proof.
-  destruct x; simpl; auto. decEq. apply Int.cast8unsigned_and.
+  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, cast16unsigned x = and x (Vint(Int.repr 65535)).
+  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
 Proof.
-  destruct x; simpl; auto. decEq. apply Int.cast16unsigned_and.
+  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:
@@ -532,6 +531,12 @@ 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.
@@ -823,6 +828,13 @@ Proof.
   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.
@@ -940,26 +952,14 @@ Proof.
   intros. inv H. auto. destruct chunk; simpl; auto.
 Qed.
 
-Lemma cast8signed_lessdef:
-  forall v1 v2, lessdef v1 v2 -> lessdef (cast8signed v1) (cast8signed v2).
-Proof.
-  intros; inv H; simpl; auto.
-Qed.
-
-Lemma cast8unsigned_lessdef:
-  forall v1 v2, lessdef v1 v2 -> lessdef (cast8unsigned v1) (cast8unsigned v2).
-Proof.
-  intros; inv H; simpl; auto.
-Qed.
-
-Lemma cast16signed_lessdef:
-  forall v1 v2, lessdef v1 v2 -> lessdef (cast16signed v1) (cast16signed v2).
+Lemma zero_ext_lessdef:
+  forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
 Proof.
   intros; inv H; simpl; auto.
 Qed.
 
-Lemma cast16unsigned_lessdef:
-  forall v1 v2, lessdef v1 v2 -> lessdef (cast16unsigned v1) (cast16unsigned v2).
+Lemma sign_ext_lessdef:
+  forall n v1 v2, lessdef v1 v2 -> lessdef (sign_ext n v1) (sign_ext n v2).
 Proof.
   intros; inv H; simpl; auto.
 Qed.
diff --git a/extraction/.depend b/extraction/.depend
index 4730714c..83dc5dcb 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -46,6 +46,10 @@
     Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi 
 ../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \
     Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx 
+../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \
+    ../caml/Camlcoq.cmo CList.cmi AST.cmi 
+../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \
+    ../caml/Camlcoq.cmx CList.cmx AST.cmx 
 ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \
     CList.cmi AST.cmi 
 ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \
@@ -170,7 +174,7 @@ PPC.cmi: Values.cmi Specif.cmi Mem.cmi Integers.cmi Globalenvs.cmi Floats.cmi \
 Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \
     Coqlib.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi AST.cmi 
 Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
+    LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi 
 RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \
     Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi Cminor.cmi \
     CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi 
@@ -446,9 +450,11 @@ Registers.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Maps.cmx FSetAVL.cmx \
     Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \
     Registers.cmi 
 Reload.cmo: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \
-    LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi Reload.cmi 
+    LTLin.cmi Integers.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi \
+    Reload.cmi 
 Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \
-    LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi 
+    LTLin.cmx Integers.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx \
+    Reload.cmi 
 RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \
     Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \
     CminorSel.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index c14ed790..ff6e9ae8 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -356,6 +356,25 @@ Proof.
   rewrite two_power_nat_S. omega.
 Qed.
 
+Lemma two_p_monotone:
+  forall x y, 0 <= x <= y -> two_p x <= two_p y.
+Proof.
+  intros.
+  replace (two_p x) with (two_p x * 1) by omega. 
+  replace y with (x + (y - x)) by omega.
+  rewrite two_p_is_exp; try omega.
+  apply Zmult_le_compat_l.
+  assert (two_p (y - x) > 0). apply two_p_gt_ZERO. omega. omega.
+  assert (two_p x > 0). apply two_p_gt_ZERO. omega. omega.
+Qed.
+
+Lemma two_power_nat_two_p:
+  forall x, two_power_nat x = two_p (Z_of_nat x).
+Proof.
+  induction x. auto. 
+  rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
+Qed.
+
 (** Properties of [Zmin] and [Zmax] *)
 
 Lemma Zmin_spec:
@@ -440,6 +459,73 @@ Proof.
   rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
 Qed.
 
+Lemma Zdiv_Zdiv:
+  forall a b c,
+  b > 0 -> c > 0 -> (a / b) / c = a / (b * c).
+Proof.
+  intros.
+  generalize (Z_div_mod_eq a b H). generalize (Z_mod_lt a b H). intros.
+  generalize (Z_div_mod_eq (a/b) c H0). generalize (Z_mod_lt (a/b) c H0). intros.
+  set (q1 := a / b) in *. set (r1 := a mod b) in *.
+  set (q2 := q1 / c) in *. set (r2 := q1 mod c) in *.
+  symmetry. apply Zdiv_unique with (r2 * b + r1). 
+  rewrite H2. rewrite H4. ring.
+  split. 
+  assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega.
+  assert ((r2 + 1) * b <= c * b).
+  apply Zmult_le_compat_r. omega. omega. 
+  replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring.
+  replace (c * b) with (b * c) in H5 by ring.
+  omega.
+Qed.
+
+Lemma Zmult_le_compat_l_neg :
+  forall n m p:Z, n >= m -> p <= 0 -> p * n <= p * m.
+Proof.
+  intros.
+  assert ((-p) * n >= (-p) * m). apply Zmult_ge_compat_l. auto. omega.
+  replace (p * n) with (- ((-p) * n)) by ring.
+  replace (p * m) with (- ((-p) * m)) by ring.
+  omega.
+Qed.
+
+Lemma Zdiv_interval_1:
+  forall lo hi a b,
+  lo <= 0 -> hi > 0 -> b > 0 ->
+  lo * b <= a < hi * b ->
+  lo <= a/b < hi.
+Proof.
+  intros. 
+  generalize (Z_div_mod_eq a b H1). generalize (Z_mod_lt a b H1). intros.
+  set (q := a/b) in *. set (r := a mod b) in *.
+  split.
+  assert (lo < (q + 1)).
+  apply Zmult_lt_reg_r with b. omega.  
+  apply Zle_lt_trans with a. omega. 
+  replace ((q + 1) * b) with (b * q + b) by ring.
+  omega.
+  omega.
+  apply Zmult_lt_reg_r with b. omega. 
+  replace (q * b) with (b * q) by ring.
+  omega.
+Qed.
+
+Lemma Zdiv_interval_2:
+  forall lo hi a b,
+  lo <= a <= hi -> lo <= 0 -> hi > 0 -> b > 0 ->
+  lo <= a/b <= hi.
+Proof.
+  intros.
+  assert (lo <= a / b < hi+1).
+  apply Zdiv_interval_1. omega. omega. auto.
+  assert (lo * b <= lo * 1). apply Zmult_le_compat_l_neg. omega. omega. 
+  replace (lo * 1) with lo in H3 by ring.
+  assert ((hi + 1) * 1 <= (hi + 1) * b). apply Zmult_le_compat_l. omega. omega.
+  replace ((hi + 1) * 1) with (hi + 1) in H4 by ring.
+  omega.
+  omega.
+Qed.
+
 (** Alignment: [align n amount] returns the smallest multiple of [amount]
   greater than or equal to [n]. *)
 
diff --git a/lib/Integers.v b/lib/Integers.v
index 2d548fb6..a9644bcc 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -118,16 +118,13 @@ Definition ltu (x y: int) : bool :=
   if zlt (unsigned x) (unsigned y) then true else false.
 
 Definition neg (x: int) : int := repr (- unsigned x).
-Definition cast8signed (x: int) : int :=
-  let y := Zmod (unsigned x) 256 in
-  if zlt y 128 then repr y else repr (y - 256).
-Definition cast8unsigned (x: int) : int :=
-  repr (Zmod (unsigned x) 256).
-Definition cast16signed (x: int) : int :=
-  let y := Zmod (unsigned x) 65536 in
-  if zlt y 32768 then repr y else repr (y - 65536).
-Definition cast16unsigned (x: int) : int :=
-  repr (Zmod (unsigned x) 65536).
+
+Definition zero_ext (n: Z) (x: int) : int :=
+  repr (Zmod (unsigned x) (two_p n)).
+Definition sign_ext (n: Z) (x: int) : int :=
+  repr (let p := two_p n in
+        let y := Zmod (unsigned x) p in
+        if zlt y (two_p (n-1)) then y else y - p).
 
 Definition add (x y: int) : int :=
   repr (unsigned x + unsigned y).
@@ -229,6 +226,7 @@ Definition shru (x y: int): int :=
 
 Definition shr (x y: int): int :=
   repr (signed x / two_p (unsigned y)).
+
 Definition shrx (x y: int): int :=
   divs x (shl one y).
 
@@ -241,6 +239,12 @@ Definition rol (x y: int) : int :=
   repr (Z_of_bits wordsize
          (fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))).
 
+Definition ror (x y: int) : int :=
+  let fx := bits_of_Z wordsize (unsigned x) in
+  let vy := unsigned y in
+  repr (Z_of_bits wordsize
+         (fun i => fx (Zmod (i + vy) (Z_of_nat wordsize)))).
+
 Definition rolm (x a m: int): int := and (rol x a) m.
 
 (** Decomposition of a number as a sum of powers of two. *)
@@ -710,6 +714,14 @@ Proof.
   unfold neg, zero. compute. apply mkint_eq. auto.
 Qed.
 
+Theorem neg_involutive: forall x, neg (neg x) = x.
+Proof.
+  intros; unfold neg. transitivity (repr (unsigned x)).
+  apply eqm_samerepr. apply eqm_trans with (- (- (unsigned x))).
+  apply eqm_neg. apply eqm_unsigned_repr_l. apply eqm_refl. 
+  apply eqm_refl2. omega. apply repr_unsigned.
+Qed. 
+
 Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
 Proof.
   intros; unfold neg, add. apply eqm_samerepr.
@@ -996,6 +1008,19 @@ Proof.
   rewrite inj_S in H. omega. rewrite inj_S in H. omega.
 Qed.
 
+Lemma bits_of_Z_of_bits':
+  forall n f i,
+  bits_of_Z n (Z_of_bits n f) i =
+  if zlt i 0 then false 
+  else if zle (Z_of_nat n) i then false
+  else f i.
+Proof.
+  intros. 
+  destruct (zlt i 0). apply bits_of_Z_below; auto.
+  destruct (zle (Z_of_nat n) i). apply bits_of_Z_above. omega.
+  apply bits_of_Z_of_bits. omega.
+Qed. 
+
 Opaque Zmult.
 
 Lemma Z_of_bits_excl:
@@ -1189,6 +1214,67 @@ Proof.
   auto.
 Qed.  
 
+Theorem not_involutive:
+  forall (x: int), not (not x) = x.
+Proof.
+  intros. unfold not. rewrite xor_assoc. 
+  change (xor mone mone) with zero. 
+  rewrite xor_zero. auto.
+Qed.
+
+(** ** Proofs by reflexion *)
+
+(** To prove equalities involving shifts and rotates, we need to
+  show complicated integer equalities involving one integer variable
+  that ranges between 0 and 31.  Rather than proving these equalities,
+  we ask Coq to check them by computing the 32 values of the 
+  left and right-hand sides and checking that they are equal.
+  This is an instance of proving by reflection. *)
+
+Section REFLECTION.
+
+Variables (f g: int -> int).
+
+Fixpoint check_equal_on_range (n: nat) : bool :=
+  match n with
+  | O => true
+  | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n)))
+           then check_equal_on_range n
+           else false
+  end.
+
+Lemma check_equal_on_range_correct:
+  forall n, 
+  check_equal_on_range n = true ->
+  forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z).
+Proof.
+  induction n.
+  simpl; intros;  omegaContradiction.
+  simpl check_equal_on_range.
+  set (fn := f (repr (Z_of_nat n))).
+  set (gn := g (repr (Z_of_nat n))).
+  generalize (eq_spec fn gn).
+  case (eq fn gn); intros.
+  rewrite inj_S in H1. 
+  assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega.
+  elim H2; intro.
+  apply IHn. auto. auto.
+  subst z; auto. 
+  discriminate. 
+Qed.
+
+Lemma equal_on_range:
+  check_equal_on_range wordsize = true ->
+  forall n, 0 <= unsigned n < Z_of_nat wordsize ->
+  f n = g n.
+Proof.
+  intros. replace n with (repr (unsigned n)). 
+  apply check_equal_on_range_correct with wordsize; auto.
+  apply repr_unsigned.
+Qed.
+
+End REFLECTION.
+
 (** ** Properties of shifts and rotates *)
 
 Lemma Z_of_bits_shift:
@@ -1316,6 +1402,67 @@ Proof.
   unfold and; intros. apply bitwise_binop_shl. reflexivity.
 Qed.
 
+Remark ltu_inv:
+  forall x y, ltu x y = true -> 0 <= unsigned x < unsigned y.
+Proof.
+  unfold ltu; intros. destruct (zlt (unsigned x) (unsigned y)).
+  split; auto. generalize (unsigned_range x); omega.
+  discriminate.
+Qed.
+
+Theorem shl_shl:
+  forall x y z,
+  ltu y (repr (Z_of_nat wordsize)) = true -> 
+  ltu z (repr (Z_of_nat wordsize)) = true ->
+  ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+  shl (shl x y) z = shl x (add y z).
+Proof.
+  intros. unfold shl, add.
+  generalize (ltu_inv _ _ H). 
+  generalize (ltu_inv _ _ H0).
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  set (x' := unsigned x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  intros.
+  repeat rewrite unsigned_repr.
+  decEq. apply Z_of_bits_exten. intros n R.
+  rewrite bits_of_Z_of_bits'. 
+  destruct (zlt (n - z') 0).
+  symmetry. apply bits_of_Z_below. omega.
+  destruct (zle (Z_of_nat wordsize) (n - z')).
+  symmetry. apply bits_of_Z_below. omega.
+  decEq. omega.
+  assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+  apply Z_of_bits_range_2.
+Qed.
+
+Theorem shru_shru:
+  forall x y z,
+  ltu y (repr (Z_of_nat wordsize)) = true -> 
+  ltu z (repr (Z_of_nat wordsize)) = true ->
+  ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+  shru (shru x y) z = shru x (add y z).
+Proof.
+  intros. unfold shru, add.
+  generalize (ltu_inv _ _ H). 
+  generalize (ltu_inv _ _ H0).
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  set (x' := unsigned x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  intros.
+  repeat rewrite unsigned_repr.
+  decEq. apply Z_of_bits_exten. intros n R.
+  rewrite bits_of_Z_of_bits'. 
+  destruct (zlt (n + z') 0). omegaContradiction.
+  destruct (zle (Z_of_nat wordsize) (n + z')).
+  symmetry. apply bits_of_Z_above. omega.
+  decEq. omega.
+  assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+  apply Z_of_bits_range_2.
+Qed.
+
 Theorem shru_rolm:
   forall x n,
   ltu n (repr (Z_of_nat wordsize)) = true ->
@@ -1374,6 +1521,32 @@ Proof.
   unfold and; intros. apply bitwise_binop_shru. reflexivity.
 Qed.
 
+Theorem shr_shr:
+  forall x y z,
+  ltu y (repr (Z_of_nat wordsize)) = true -> 
+  ltu z (repr (Z_of_nat wordsize)) = true ->
+  ltu (add y z) (repr (Z_of_nat wordsize)) = true ->
+  shr (shr x y) z = shr x (add y z).
+Proof.
+  intros. unfold shr, add.
+  generalize (ltu_inv _ _ H). 
+  generalize (ltu_inv _ _ H0).
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  set (x' := signed x).
+  set (y' := unsigned y).
+  set (z' := unsigned z).
+  intros.
+  rewrite unsigned_repr.
+  rewrite two_p_is_exp. 
+  rewrite signed_repr.
+  decEq. apply Zdiv_Zdiv. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
+  apply Zdiv_interval_2. unfold x'; apply signed_range. 
+  vm_compute; congruence. vm_compute; auto. apply two_p_gt_ZERO. omega.
+  omega. omega. 
+  assert (2 * Z_of_nat wordsize < max_unsigned). vm_compute; auto.
+  omega.
+Qed.
+
 Theorem rol_zero:
   forall x,
   rol x zero = x.
@@ -1469,6 +1642,90 @@ Proof.
   intros; unfold rolm. symmetry. apply and_or_distrib. 
 Qed.
 
+Theorem ror_rol:
+  forall x y,
+  ltu y (repr (Z_of_nat wordsize)) = true ->
+  ror x y = rol x (sub (Int.repr (Z_of_nat wordsize)) y).
+Proof.
+  intros. unfold ror, rol, sub.
+  generalize (ltu_inv _ _ H).
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  intro. rewrite unsigned_repr.
+  decEq. apply Z_of_bits_exten. intros. decEq.
+  apply eqmod_mod_eq. omega. 
+  exists 1. omega.
+  assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+Qed.
+
+Remark or_shl_shru_masks:
+  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
+  or (shl mone (sub (repr (Z_of_nat wordsize)) logn)) (shru mone logn) = mone.
+Proof.
+  apply (equal_on_range
+          (fun l => or (shl mone (sub (repr (Z_of_nat wordsize)) l)) (shru mone l))
+          (fun l => mone)).
+  vm_compute; auto.
+Qed.
+
+Theorem or_ror:
+  forall x y z,
+  ltu y (repr (Z_of_nat wordsize)) = true ->
+  ltu z (repr (Z_of_nat wordsize)) = true ->
+  add y z = repr (Z_of_nat wordsize) ->
+  ror x z = or (shl x y) (shru x z).
+Proof.
+  intros.
+  generalize (ltu_inv _ _ H).
+  generalize (ltu_inv _ _ H0).
+  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
+  intros.
+  rewrite ror_rol; auto.
+  rewrite shl_rolm; auto.
+  rewrite shru_rolm; auto.
+  replace y with (sub (repr (Z_of_nat wordsize)) z).
+  rewrite or_rolm.
+  rewrite or_shl_shru_masks; auto.
+  unfold rolm. rewrite and_mone. auto.
+  rewrite <- H1. rewrite sub_add_opp. rewrite add_assoc. 
+  rewrite <- sub_add_opp. rewrite sub_idem. apply add_zero. 
+Qed.
+
+Remark shru_shl_and_1:
+  forall y,
+  0 <= unsigned y < Z_of_nat wordsize ->
+  modu (add y (sub (repr (Z_of_nat wordsize)) y)) (repr (Z_of_nat wordsize)) = zero.
+Proof.
+  intros.
+  apply (equal_on_range
+           (fun y => modu (add y (sub (repr (Z_of_nat wordsize)) y)) (repr (Z_of_nat wordsize)))
+           (fun y => zero)).
+  vm_compute. auto. auto.
+Qed.
+
+Remark shru_shl_and_2:
+  forall y,
+  0 <= unsigned y < Z_of_nat wordsize ->
+  and (rol (shl mone y) (sub (repr (Z_of_nat wordsize)) y)) (shru mone y) =
+  Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1).
+Proof.
+  intros.
+  apply (equal_on_range
+          (fun y => and (rol (shl mone y) (sub (repr (Z_of_nat wordsize)) y)) (shru mone y))
+          (fun y => Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1))).
+  vm_compute. auto. auto.
+Qed.
+
+Theorem shru_shl_and:
+  forall x y,
+  ltu y (Int.repr (Z_of_nat wordsize)) = true ->
+  shru (shl x y) y = and x (Int.repr (two_p (Z_of_nat wordsize - unsigned y) - 1)).
+Proof.
+  intros. rewrite shru_rolm; auto. rewrite shl_rolm; auto. rewrite rolm_rolm.
+  rewrite shru_shl_and_1. rewrite shru_shl_and_2. 
+  apply rolm_zero. 
+  exact (ltu_inv _ _ H). exact (ltu_inv _ _ H).
+Qed.
+
 (** ** Relation between shifts and powers of 2 *)
 
 Fixpoint powerserie (l: list Z): Z :=
@@ -1573,6 +1830,48 @@ Proof.
   intros; discriminate.
 Qed.
 
+Remark two_p_range:
+  forall n,
+  0 <= n < Z_of_nat wordsize ->
+  0 <= two_p n <= max_unsigned.
+Proof.
+  intros. split.
+  assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
+  assert (two_p n <= two_p (Z_of_nat wordsize - 1)). apply two_p_monotone. omega.
+  eapply Zle_trans. eauto. vm_compute. congruence.
+Qed.
+
+Remark Z_one_bits_zero:
+  forall n i, Z_one_bits n 0 i = nil.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.
+
+Remark Z_one_bits_two_p:
+  forall n x i,
+  0 <= x < Z_of_nat n ->
+  Z_one_bits n (two_p x) i = (i + x) :: nil.
+Proof.
+  induction n; intros; simpl. simpl in H. omegaContradiction.
+  rewrite inj_S in H. 
+  assert (x = 0 \/ 0 < x) by omega. destruct H0.
+  subst x; simpl. decEq. omega. apply Z_one_bits_zero.
+  replace (two_p x) with (Z_shift_add false (two_p (x-1))).
+  rewrite Z_bin_decomp_shift_add.
+  replace (i + x) with ((i + 1) + (x - 1)) by omega. 
+  apply IHn. omega.
+  unfold Z_shift_add. rewrite <- two_p_S. decEq; omega. omega.
+Qed.
+
+Lemma is_power2_two_p:
+  forall n, 0 <= n < Z_of_nat wordsize ->
+  is_power2 (repr (two_p n)) = Some (repr n).
+Proof.
+  intros. unfold is_power2. rewrite unsigned_repr. 
+  rewrite Z_one_bits_two_p. auto. auto.
+  apply two_p_range. auto.
+Qed.
+
 Theorem mul_pow2:
   forall x n logn,
   is_power2 n = Some logn ->
@@ -1728,20 +2027,85 @@ Proof.
   rewrite add_neg_zero. apply add_zero.
 Qed.
 
+Lemma Zdiv_round_Zdiv:
+  forall x y,
+  y > 0 ->
+  Zdiv_round x y = if zlt x 0 then (x + y - 1) / y else x / y.
+Proof.
+  intros. unfold Zdiv_round.
+  destruct (zlt x 0). 
+  rewrite zlt_false; try omega.
+  generalize (Z_div_mod_eq (-x) y H).
+  generalize (Z_mod_lt (-x) y H).
+  set (q := (-x) / y). set (r := (-x) mod y). intros.
+  symmetry.
+  apply Zdiv_unique with (y - r - 1).
+  replace x with (- (y * q) - r) by omega.
+  replace (-(y * q)) with ((-q) * y) by ring.
+  omega.
+  omega.
+  apply zlt_false. omega.
+Qed.
+
+Theorem shrx_shr:
+  forall x y,
+  ltu y (repr (Z_of_nat wordsize - 1)) = true ->
+  shrx x y =
+  shr (if lt x Int.zero then add x (sub (shl one y) one) else x) y.
+Proof.
+  intros. unfold shrx, divs, shr. decEq.
+  exploit ltu_inv; eauto. 
+  change (unsigned (repr (Z_of_nat wordsize - 1))) with (Z_of_nat wordsize - 1).
+  set (uy := unsigned y).
+  intro RANGE.
+  assert (shl one y = repr (two_p uy)).
+    transitivity (mul one (repr (two_p uy))).
+    symmetry. apply mul_pow2. replace y with (repr uy). 
+    apply is_power2_two_p. omega. unfold uy. apply repr_unsigned.
+    rewrite mul_commut. apply mul_one.
+  assert (two_p uy > 0). apply two_p_gt_ZERO. omega.
+  assert (two_p uy <= two_p (Z_of_nat wordsize - 2)).
+    apply two_p_monotone. omega.
+  assert (unsigned (shl one y) = two_p uy).
+    rewrite H0. apply unsigned_repr.
+    assert (two_p (Z_of_nat wordsize - 2) < max_unsigned). vm_compute; auto.
+    omega.
+  assert (signed (shl one y) = two_p uy).
+    rewrite H0. apply signed_repr. 
+    split. apply Zle_trans with 0. vm_compute; congruence. omega.
+    apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). auto.
+    vm_compute; congruence.
+  rewrite H4. 
+  rewrite Zdiv_round_Zdiv; auto.
+  unfold lt. change (signed zero) with 0. 
+  destruct (zlt (signed x) 0); auto.
+  rewrite add_signed.
+  assert (signed (sub (shl one y) one) = two_p uy - 1).
+    unfold sub. rewrite H3. change (unsigned one) with 1. 
+    apply signed_repr. 
+    split. apply Zle_trans with 0. vm_compute; congruence. omega.
+    apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). omega. 
+    vm_compute; congruence.
+  rewrite H5. rewrite signed_repr. decEq. omega.
+  generalize (signed_range x). intros. 
+  assert (two_p uy - 1 <= max_signed).
+    apply Zle_trans with (two_p (Z_of_nat wordsize - 2)). omega. 
+    vm_compute; congruence.
+  omega.
+Qed.
+
 Lemma add_and:
   forall x y z,
   and y z = zero ->
-  or y z = mone ->
-  add (and x y) (and x z) = x.
+  add (and x y) (and x z) = and x (or y z).
 Proof.
-  intros. unfold add. transitivity (repr (unsigned x)); auto with ints.
-  decEq. unfold and, bitwise_binop.
+  intros. unfold add, and, bitwise_binop. 
+  decEq.
   repeat rewrite unsigned_repr; auto with ints.
-  transitivity (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x))).
-  apply Z_of_bits_excl. intros. 
+  apply Z_of_bits_excl; intros.
   assert (forall a b c, a && b && (a && c) = a && (b && c)).
     destruct a; destruct b; destruct c; reflexivity.
-  rewrite H2. 
+  rewrite H1. 
   replace (bits_of_Z wordsize (unsigned y) i &&
            bits_of_Z wordsize (unsigned z) i)
      with (bits_of_Z wordsize (unsigned (and y z)) i).
@@ -1750,70 +2114,11 @@ Proof.
   unfold and, bitwise_binop. 
   rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. 
   reflexivity. auto. 
-  intros. rewrite <- demorgan1. 
-  replace (bits_of_Z wordsize (unsigned y) i ||
-           bits_of_Z wordsize (unsigned z) i)
-     with (bits_of_Z wordsize (unsigned (or y z)) i).
-  rewrite H0. change (unsigned mone) with (two_power_nat wordsize - 1).
-  rewrite bits_of_Z_mone; auto. apply andb_b_true.
+  rewrite <- demorgan1.
   unfold or, bitwise_binop. 
   rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
-  apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z. 
-Qed.
-
-(** To prove equalities involving modulus and bitwise ``and'', we need to
-  show complicated integer equalities involving one integer variable
-  that ranges between 0 and 31.  Rather than proving these equalities,
-  we ask Coq to check them by computing the 32 values of the 
-  left and right-hand sides and checking that they are equal.
-  This is an instance of proving by reflection. *)
-
-Section REFLECTION.
-
-Variables (f g: int -> int).
-
-Fixpoint check_equal_on_range (n: nat) : bool :=
-  match n with
-  | O => true
-  | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n)))
-           then check_equal_on_range n
-           else false
-  end.
-
-Lemma check_equal_on_range_correct:
-  forall n, 
-  check_equal_on_range n = true ->
-  forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z).
-Proof.
-  induction n.
-  simpl; intros;  omegaContradiction.
-  simpl check_equal_on_range.
-  set (fn := f (repr (Z_of_nat n))).
-  set (gn := g (repr (Z_of_nat n))).
-  generalize (eq_spec fn gn).
-  case (eq fn gn); intros.
-  rewrite inj_S in H1. 
-  assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega.
-  elim H2; intro.
-  apply IHn. auto. auto.
-  subst z; auto. 
-  discriminate. 
-Qed.
-
-Lemma equal_on_range:
-  check_equal_on_range wordsize = true ->
-  forall n, 0 <= unsigned n < Z_of_nat wordsize ->
-  f n = g n.
-Proof.
-  intros. replace n with (repr (unsigned n)). 
-  apply check_equal_on_range_correct with wordsize; auto.
-  apply repr_unsigned.
 Qed.
 
-End REFLECTION.
-
-(** Here are the three equalities that we prove by reflection. *)
-
 Remark modu_and_masks_1:
   forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
   rol (shru mone logn) logn = shl mone logn.
@@ -1879,7 +2184,8 @@ Proof.
   replace n with (repr (two_p (unsigned logn))).
   rewrite modu_and_masks_1; auto.
   rewrite and_idem.
-  apply add_and. apply modu_and_masks_2; auto. apply modu_and_masks_3; auto.
+  rewrite add_and. rewrite modu_and_masks_3; auto. apply and_mone.
+  apply modu_and_masks_2; auto.
   transitivity (repr (unsigned n)). decEq. auto. auto with ints.
   rewrite add_commut. rewrite add_neg_zero. auto.
   unfold ltu. apply zlt_true. 
@@ -1892,208 +2198,282 @@ Qed.
 
 (** ** Properties of integer zero extension and sign extension. *)
 
-Theorem cast8unsigned_and:
-  forall x, cast8unsigned x = and x (repr 255).
-Proof.
-  intros; unfold cast8unsigned. 
-  change (repr (unsigned x mod 256)) with (modu x (repr 256)).
-  change (repr 255) with (sub (repr 256) one).
-  apply modu_and with (repr 8). reflexivity.
+Section EXTENSIONS.
+
+Variable n: Z.
+Hypothesis RANGE: 0 < n < Z_of_nat wordsize.
+
+Remark two_p_n_pos:
+  two_p n > 0.
+Proof. apply two_p_gt_ZERO. omega. Qed.
+
+Remark two_p_n_range:
+  0 <= two_p n <= max_unsigned.
+Proof. apply two_p_range. omega. Qed.
+
+Remark two_p_n_range':
+  two_p n <= max_signed + 1.
+Proof. 
+  assert (two_p n <= two_p (Z_of_nat wordsize - 1)).
+  apply two_p_monotone. omega.
+  exact H.
 Qed.
 
-Theorem cast16unsigned_and:
-  forall x, cast16unsigned x = and x (repr 65535).
+Remark unsigned_repr_two_p:
+  unsigned (repr (two_p n)) = two_p n.
 Proof.
-  intros; unfold cast16unsigned. 
-  change (repr (unsigned x mod 65536)) with (modu x (repr 65536)).
-  change (repr 65535) with (sub (repr 65536) one).
-  apply modu_and with (repr 16). reflexivity.
+  apply unsigned_repr. apply two_p_n_range. 
 Qed.
 
-Lemma eqmod_256_unsigned_repr:
-  forall a, eqmod 256 a (unsigned (repr a)).
+Theorem zero_ext_and:
+  forall x, zero_ext n x = and x (repr (two_p n - 1)).
 Proof.
-  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
-  intros [k EQ]. exists (k * (modulus / 256)). 
-  replace (k * (modulus / 256) * 256)  
-     with (k * ((modulus / 256) * 256)).
-  exact EQ. ring. 
+  intros; unfold zero_ext.
+  assert (is_power2 (repr (two_p n)) = Some (repr n)).
+    apply is_power2_two_p. omega.
+  generalize (modu_and x _ _ H).
+  unfold modu. rewrite unsigned_repr_two_p. intro. rewrite H0. 
+  decEq. unfold sub. decEq. rewrite unsigned_repr_two_p. reflexivity.
 Qed.
 
-Lemma eqmod_65536_unsigned_repr:
-  forall a, eqmod 65536 a (unsigned (repr a)).
+Theorem zero_ext_idem:
+  forall x, zero_ext n (zero_ext n x) = zero_ext n x.
 Proof.
-  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
-  intros [k EQ]. exists (k * (modulus / 65536)). 
-  replace (k * (modulus / 65536) * 65536)  
-     with (k * ((modulus / 65536) * 65536)).
-  exact EQ. ring. 
+  intros. repeat rewrite zero_ext_and. 
+  rewrite and_assoc. rewrite and_idem. auto.
 Qed.
 
-Theorem cast8_signed_unsigned:
-  forall n, cast8signed (cast8unsigned n) = cast8signed n.
+Lemma eqm_eqmod_two_p:
+  forall a b, eqm a b -> eqmod (two_p n) a b.
 Proof.
-  intros; unfold cast8signed, cast8unsigned.
-  set (N := unsigned n).
-  rewrite unsigned_repr. 
-  replace ((N mod 256) mod 256) with (N mod 256).
-  auto.
-  symmetry. apply Zmod_small. apply Z_mod_lt. omega.
-  assert (0 <= N mod 256 < 256). apply Z_mod_lt. omega.
-  assert (256 < max_unsigned). compute; auto.
+  intros a b [k EQ].
+  exists (k * two_p (Z_of_nat wordsize - n)).
+  rewrite EQ. decEq. rewrite <- Zmult_assoc. decEq.
+  rewrite <- two_p_is_exp. unfold modulus. rewrite two_power_nat_two_p.
+  decEq. omega. omega. omega.
+Qed.
+(*
+Lemma zero_ext_charact:
+  forall x y,
+  zero_ext n x = y <->
+  0 <= unsigned y < two_p n /\ eqmod (two_p n) (unsigned x) (unsigned y).
+Proof.
+  intros. unfold zero_ext. set (x' := unsigned x). split; intros.
+  subst y.
+  assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
+  rewrite unsigned_repr. split. auto. 
+  apply eqmod_mod. apply two_p_n_pos.
+  generalize two_p_n_range. omega.
+  destruct H. destruct H0 as [k EQ].  
+  assert (x' mod two_p n = unsigned y).
+  apply Zmod_unique with k; auto.
+  rewrite H0. apply repr_unsigned.
+Qed.
+
+Lemma sign_ext_charact:
+  forall x y,
+  sign_ext n x = y <->
+  -(two_p (n-1)) <= signed y < two_p (n-1)
+  /\ eqmod (two_p n) (unsigned x) (signed y).
+Proof.
+  intros. unfold sign_ext. set (x' := unsigned x). split; intros.
+  assert (0 <= x' mod two_p n < two_p n). apply Z_mod_lt. apply two_p_n_pos.
+  destruct (zlt (x' mod two_p n) (two_p (n - 1))); subst y.
+  rewrite signed_repr. split. omega. 
+  apply eqmod_mod. apply two_p_n_pos.
+  assert (min_signed < 0). vm_compute; auto. 
+  generalize two_p_n_range'. omega.
+  rewrite signed_repr. split. 
+  assert (two_p n = 2 * two_p (n-1)). rewrite <- two_p_S. decEq. omega. omega. 
+  omega. 
+  apply eqmod_trans with (x' - 0). apply eqmod_refl2. omega.
+  apply eqmod_sub. apply eqmod_mod. apply two_p_n_pos. 
+  exists (-1). ring. 
+  split. generalize two_p_n_range'. 
+  change (max_signed + 1) with (- min_signed). omega. 
+  generalize two_p_n_range'. omega.
+
+  destruct H. destruct H0 as [k EQ].
+  assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
+  assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
+  assert (x' mod two_p n = signed y).
+  apply Zmod_unique with k; auto. omega.
+  rewrite zlt_true. rewrite H2. apply repr_signed. omega.
+  assert (x' mod two_p n = signed y + two_p n).
+  apply Zmod_unique with (k-1). rewrite EQ. ring. omega. 
+  rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
+  omega.
+Qed.
+*)
+
+Lemma sign_ext_charact:
+  forall x y,
+  -(two_p (n-1)) <= signed y < two_p (n-1) ->
+  eqmod (two_p n) (unsigned x) (signed y) ->
+  sign_ext n x = y.
+Proof.
+  intros. unfold sign_ext. set (x' := unsigned x) in *.
+  destruct H0 as [k EQ].
+  assert (two_p n = 2 * two_p (n - 1)). rewrite <- two_p_S. decEq. omega. omega.
+  assert (signed y >= 0 \/ signed y < 0) by omega. destruct H1.
+  assert (x' mod two_p n = signed y).
+  apply Zmod_unique with k; auto. omega.
+  rewrite zlt_true. rewrite H2. apply repr_signed. omega.
+  assert (x' mod two_p n = signed y + two_p n).
+  apply Zmod_unique with (k-1). rewrite EQ. ring. omega. 
+  rewrite zlt_false. replace (x' mod two_p n - two_p n) with (signed y) by omega. apply repr_signed.
   omega.
 Qed.
 
-Theorem cast8_unsigned_signed:
-  forall n, cast8unsigned (cast8signed n) = cast8unsigned n.
+Lemma zero_ext_eqmod_two_p:
+  forall x y,
+  eqmod (two_p n) (unsigned x) (unsigned y) -> zero_ext n x = zero_ext n y.
 Proof.
-  intros; unfold cast8signed, cast8unsigned.
-  set (N := unsigned n mod 256).
-  assert (0 <= N < 256). unfold N; apply Z_mod_lt. omega.
-  assert (N mod 256 = N). apply Zmod_small. auto.
-  assert (256 <= max_unsigned). compute; congruence.
-  decEq. 
-  case (zlt N 128); intro.
-  rewrite unsigned_repr. auto. omega.
-  transitivity (N mod 256); auto. 
-  apply eqmod_mod_eq. omega. 
-  apply eqmod_trans with (N - 256). apply eqmod_sym. apply eqmod_256_unsigned_repr.
-  assert (eqmod 256 (N - 256) (N - 0)).
-    apply eqmod_sub. apply eqmod_refl. 
-    red. exists 1; reflexivity.
-  replace (N - 0) with N in H2. auto. omega.
+  intros. unfold zero_ext. decEq. apply eqmod_mod_eq. apply two_p_n_pos. auto.
 Qed.
 
-Theorem cast16_unsigned_signed:
-  forall n, cast16unsigned (cast16signed n) = cast16unsigned n.
+Lemma sign_ext_eqmod_two_p:
+  forall x y,
+  eqmod (two_p n) (unsigned x) (unsigned y) -> sign_ext n x = sign_ext n y.
 Proof.
-  intros; unfold cast16signed, cast16unsigned.
-  set (N := unsigned n mod 65536).
-  assert (0 <= N < 65536). unfold N; apply Z_mod_lt. omega.
-  assert (N mod 65536 = N). apply Zmod_small. auto.
-  assert (65536 <= max_unsigned). compute; congruence.
-  decEq. 
-  case (zlt N 32768); intro.
-  rewrite unsigned_repr. auto. omega.
-  transitivity (N mod 65536); auto. 
-  apply eqmod_mod_eq. omega. 
-  apply eqmod_trans with (N - 65536). apply eqmod_sym. apply eqmod_65536_unsigned_repr.
-  assert (eqmod 65536 (N - 65536) (N - 0)).
-    apply eqmod_sub. apply eqmod_refl. 
-    red. exists 1; reflexivity.
-  replace (N - 0) with N in H2. auto. omega.
-Qed.
-
-Theorem cast8_unsigned_idem:
-  forall n, cast8unsigned (cast8unsigned n) = cast8unsigned n.
-Proof.
-  intros. repeat rewrite cast8unsigned_and. 
-  rewrite and_assoc. reflexivity. 
-Qed.
-
-Theorem cast16_unsigned_idem:
-  forall n, cast16unsigned (cast16unsigned n) = cast16unsigned n.
-Proof.
-  intros. repeat rewrite cast16unsigned_and. 
-  rewrite and_assoc. reflexivity. 
-Qed.
-
-Theorem cast8_signed_idem:
-  forall n, cast8signed (cast8signed n) = cast8signed n.
-Proof.
-  intros; unfold cast8signed.
-  set (N := unsigned n mod 256).
-  assert (256 < max_unsigned). compute; auto.
-  assert (0 <= N < 256). unfold N. apply Z_mod_lt. omega. 
-  case (zlt N 128); intro.
-  assert (unsigned (repr N) = N).
-    apply unsigned_repr. omega.
-  rewrite H1.
-  replace (N mod 256) with N. apply zlt_true. auto.
-  symmetry. apply Zmod_small. auto.
-  set (M := (unsigned (repr (N - 256)) mod 256)).
-  assert (M = N).
-    unfold M, N. apply eqmod_mod_eq. omega. 
-    apply eqmod_trans with (unsigned n mod 256 - 256).
-    apply eqmod_sym. apply eqmod_256_unsigned_repr. 
-    apply eqmod_trans with (unsigned n - 0).
-    apply eqmod_sub. 
-    apply eqmod_sym. apply eqmod_mod. omega.
-    unfold eqmod. exists 1; omega.
-    apply eqmod_refl2. omega.
-  rewrite H1. rewrite zlt_false; auto.
-Qed.
-
-Theorem cast16_signed_idem:
-  forall n, cast16signed (cast16signed n) = cast16signed n.
-Proof.
-  intros; unfold cast16signed.
-  set (N := unsigned n mod 65536).
-  assert (65536 < max_unsigned). compute; auto.
-  assert (0 <= N < 65536). unfold N. apply Z_mod_lt. omega. 
-  case (zlt N 32768); intro.
-  assert (unsigned (repr N) = N).
-    apply unsigned_repr. omega.
-  rewrite H1.
-  replace (N mod 65536) with N. apply zlt_true. auto.
-  symmetry. apply Zmod_small. auto.
-  set (M := (unsigned (repr (N - 65536)) mod 65536)).
-  assert (M = N).
-    unfold M, N. apply eqmod_mod_eq. omega. 
-    apply eqmod_trans with (unsigned n mod 65536 - 65536).
-    apply eqmod_sym. apply eqmod_65536_unsigned_repr. 
-    apply eqmod_trans with (unsigned n - 0).
-    apply eqmod_sub. 
-    apply eqmod_sym. apply eqmod_mod. omega.
-    unfold eqmod. exists 1; omega.
-    apply eqmod_refl2. omega.
-  rewrite H1. rewrite zlt_false; auto.
-Qed.
-
-Theorem cast8_signed_equal_if_unsigned_equal:
-  forall x y, 
-  cast8unsigned x = cast8unsigned y ->
-  cast8signed x = cast8signed y.
-Proof.
-  unfold cast8unsigned, cast8signed; intros until y.
-  set (x' := unsigned x mod 256).
-  set (y' := unsigned y mod 256).
-  intro. 
-  assert (eqm x' y').
-    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
-    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
-  assert (forall z, 0 <= z mod 256 < modulus).
-    intros. 
-    assert (0 <= z mod 256 < 256). apply Z_mod_lt. omega.
-    assert (256 <= modulus). compute. congruence.
-    omega.
-  assert (x' = y').
-    apply eqm_small_eq; unfold x', y'; auto. 
-  rewrite H2. auto.
-Qed.
-
-Theorem cast16_signed_equal_if_unsigned_equal:
-  forall x y, 
-  cast16unsigned x = cast16unsigned y ->
-  cast16signed x = cast16signed y.
-Proof.
-  unfold cast16unsigned, cast16signed; intros until y.
-  set (x' := unsigned x mod 65536).
-  set (y' := unsigned y mod 65536).
-  intro. 
-  assert (eqm x' y').
-    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
-    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
-  assert (forall z, 0 <= z mod 65536 < modulus).
-    intros. 
-    assert (0 <= z mod 65536 < 65536). apply Z_mod_lt. omega.
-    assert (65536 <= modulus). compute. congruence.
+  intros. unfold sign_ext. 
+  assert (unsigned x mod two_p n = unsigned y mod two_p n). 
+  apply eqmod_mod_eq. apply two_p_n_pos. auto. 
+  rewrite H0. auto.
+Qed.
+
+Lemma eqmod_two_p_zero_ext:
+  forall x, eqmod (two_p n) (unsigned x) (unsigned (zero_ext n x)).
+Proof.
+  intros. unfold zero_ext. 
+  apply eqmod_trans with (unsigned x mod two_p n).
+  apply eqmod_mod. apply two_p_n_pos.
+  apply eqm_eqmod_two_p. apply eqm_unsigned_repr. 
+Qed.
+
+Lemma eqmod_two_p_sign_ext:
+  forall x, eqmod (two_p n) (unsigned x) (unsigned (sign_ext n x)).
+Proof.
+  intros. unfold sign_ext. destruct (zlt (unsigned x mod two_p n) (two_p (n-1))).
+  apply eqmod_trans with (unsigned x mod two_p n).
+  apply eqmod_mod. apply two_p_n_pos.
+  apply eqm_eqmod_two_p. apply eqm_unsigned_repr. 
+  apply eqmod_trans with (unsigned x mod two_p n).
+  apply eqmod_mod. apply two_p_n_pos.
+  apply eqmod_trans with (unsigned x mod two_p n - 0).
+  apply eqmod_refl2. omega.
+  apply eqmod_trans with (unsigned x mod two_p n - two_p n).
+  apply eqmod_sub. apply eqmod_refl. exists (-1). ring.
+  apply eqm_eqmod_two_p. apply eqm_unsigned_repr. 
+Qed.
+
+Theorem sign_ext_idem:
+  forall x, sign_ext n (sign_ext n x) = sign_ext n x.
+Proof.
+  intros. apply sign_ext_eqmod_two_p. 
+  apply eqmod_sym. apply eqmod_two_p_sign_ext.
+Qed.
+
+Theorem sign_ext_zero_ext:
+  forall x, sign_ext n (zero_ext n x) = sign_ext n x.
+Proof.
+  intros. apply sign_ext_eqmod_two_p.
+  apply eqmod_sym. apply eqmod_two_p_zero_ext.
+Qed.
+
+Theorem zero_ext_sign_ext:
+  forall x, zero_ext n (sign_ext n x) = zero_ext n x.
+Proof.
+  intros. apply zero_ext_eqmod_two_p.
+  apply eqmod_sym. apply eqmod_two_p_sign_ext.
+Qed.
+
+Theorem sign_ext_equal_if_zero_equal:
+  forall x y,
+  zero_ext n x = zero_ext n y ->
+  sign_ext n x = sign_ext n y.
+Proof.
+  intros. rewrite <- (sign_ext_zero_ext x).
+  rewrite <- (sign_ext_zero_ext y). congruence.
+Qed.
+
+Lemma eqmod_mult_div:
+  forall n1 n2 x y,
+  0 <= n1 -> 0 <= n2 ->
+  eqmod (two_p (n1+n2)) (two_p n1 * x) y ->
+  eqmod (two_p n2) x (y / two_p n1).
+Proof.
+  intros. rewrite two_p_is_exp in H1; auto. 
+  destruct H1 as [k EQ]. exists k.
+  change x with (0 / two_p n1 + x). rewrite <- Z_div_plus.
+  replace (0 + x * two_p n1) with (two_p n1 * x) by ring.
+  rewrite EQ. 
+  replace (k * (two_p n1 * two_p n2) + y) with (y + (k * two_p n2) * two_p n1) by ring.
+  rewrite Z_div_plus. ring. 
+  apply two_p_gt_ZERO; auto.
+  apply two_p_gt_ZERO; auto.
+Qed.
+
+Theorem sign_ext_shr_shl:
+  forall x, 
+  let y := repr (Z_of_nat wordsize - n) in
+  sign_ext n x = shr (shl x y) y.
+Proof.
+  intros.
+  assert (unsigned y = Z_of_nat wordsize - n).
+    unfold y. apply unsigned_repr. 
+    assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto. omega.
+  apply sign_ext_charact.
+  (* inequalities *)
+  unfold shr. rewrite H. 
+  set (z := signed (shl x y)).
+  rewrite signed_repr. 
+  apply Zdiv_interval_1.
+  assert (two_p (n - 1) > 0). apply two_p_gt_ZERO. omega. omega.
+  apply two_p_gt_ZERO. omega.
+  apply two_p_gt_ZERO. omega.
+  replace ((- two_p (n-1)) * two_p (Z_of_nat wordsize - n))
+     with (- (two_p (n-1) * two_p (Z_of_nat wordsize - n))) by ring.
+  rewrite <- two_p_is_exp.
+  replace (n - 1 + (Z_of_nat wordsize - n)) with (Z_of_nat wordsize - 1) by omega.
+  change (min_signed <= z < max_signed + 1).
+  generalize (signed_range (shl x y)). unfold z. omega. 
+  omega. omega. 
+  apply Zdiv_interval_2. unfold z. apply signed_range. 
+  vm_compute; congruence. vm_compute; auto. apply two_p_gt_ZERO; omega. 
+  (* eqmod *)
+  unfold shr. rewrite H. 
+  apply eqmod_trans with (signed (shl x y) / two_p (Z_of_nat wordsize - n)).
+  apply eqmod_mult_div. omega. omega. 
+  replace (Z_of_nat wordsize - n + n) with (Z_of_nat wordsize) by omega.
+  change (eqm (two_p (Z_of_nat wordsize - n) * unsigned x) (signed (shl x y))).
+  rewrite shl_mul_two_p. unfold mul. rewrite H. 
+  apply eqm_sym. eapply eqm_trans. apply eqm_signed_unsigned. 
+  apply eqm_unsigned_repr_l. rewrite (Zmult_comm (unsigned x)). 
+  apply eqm_mult. apply eqm_sym. apply eqm_unsigned_repr. apply eqm_refl.
+  apply eqm_eqmod_two_p. apply eqm_sym. eapply eqm_trans.
+  apply eqm_signed_unsigned. apply eqm_sym. apply eqm_unsigned_repr. 
+Qed.
+
+Theorem zero_ext_shru_shl:
+  forall x, 
+  let y := repr (Z_of_nat wordsize - n) in
+  zero_ext n x = shru (shl x y) y.
+Proof.
+  intros.
+  assert (unsigned y = Z_of_nat wordsize - n).
+    unfold y. apply unsigned_repr. 
+    assert (Z_of_nat wordsize < max_unsigned). vm_compute; auto.
     omega.
-  assert (x' = y').
-    apply eqm_small_eq; unfold x', y'; auto. 
-  rewrite H2. auto.
+  rewrite zero_ext_and. symmetry. 
+  replace n with (Z_of_nat wordsize - unsigned y).
+  apply shru_shl_and. unfold ltu. apply zlt_true.
+  rewrite H. change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize). omega.
+  omega.
 Qed.
 
+End EXTENSIONS.
+
 (** ** Properties of [one_bits] (decomposition in sum of powers of two) *)
 
 Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)