[regression to check!] Merge tag 'v3.6' into mppa-work

Conflicts:
	.gitignore
	backend/Lineartyping.v
	common/Values.v
	configure
	cparser/Machine.ml
	cparser/Machine.mli
	driver/Configuration.ml
	driver/Frontend.ml
	runtime/Makefile
	test/c/Makefile
	test/c/aes.c
	test/compression/Makefile
	test/regression/Makefile
	test/regression/extasm.c
	test/regression/floats-basics.c
	test/regression/floats.c

Note : test/regression should be checked, didn't test it yet

2 files changed, 517 insertions, 65 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 08a416c1..3e78ee60 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -673,6 +673,11 @@ Proof.
   intros. generalize (eq_spec x y); case (eq x y); intros; congruence.
 Qed.
 
+Theorem same_if_eq: forall x y, eq x y = true -> x = y.
+Proof.
+  intros. generalize (eq_spec x y); rewrite H; auto.
+Qed.
+
 Theorem eq_signed:
   forall x y, eq x y = if zeq (signed x) (signed y) then true else false.
 Proof.
@@ -1144,6 +1149,12 @@ Proof.
   intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range.
 Qed.
 
+Lemma bits_below:
+  forall x i, i < 0 -> testbit x i = false.
+Proof.
+  intros. apply Z.testbit_neg_r; auto.
+Qed.
+
 Lemma bits_zero:
   forall i, testbit zero i = false.
 Proof.
@@ -2516,12 +2527,11 @@ Proof.
 Qed.
 
 Lemma bits_sign_ext:
-  forall n x i, 0 <= i < zwordsize -> 0 < n ->
+  forall n x i, 0 <= i < zwordsize ->
   testbit (sign_ext n x) i = testbit x (if zlt i n then i else n - 1).
 Proof.
   intros. unfold sign_ext.
-  rewrite testbit_repr; auto. rewrite Zsign_ext_spec. destruct (zlt i n); auto.
-  omega. auto.
+  rewrite testbit_repr; auto. apply Zsign_ext_spec. omega. 
 Qed.
 
 Hint Rewrite bits_zero_ext bits_sign_ext: ints.
@@ -2533,12 +2543,24 @@ Proof.
   rewrite bits_zero_ext. apply zlt_true. omega. omega.
 Qed.
 
+Theorem zero_ext_below:
+  forall n x, n <= 0 -> zero_ext n x = zero.
+Proof.
+  intros. bit_solve. destruct (zlt i n); auto. apply bits_below; omega. omega.
+Qed.
+
 Theorem sign_ext_above:
   forall n x, n >= zwordsize -> sign_ext n x = x.
 Proof.
   intros. apply same_bits_eq; intros.
   unfold sign_ext; rewrite testbit_repr; auto.
-  rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega. omega.
+  rewrite Zsign_ext_spec. rewrite zlt_true. auto. omega. omega.
+Qed.
+
+Theorem sign_ext_below:
+  forall n x, n <= 0 -> sign_ext n x = zero.
+Proof.
+  intros. bit_solve. apply bits_below. destruct (zlt i n); omega.
 Qed.
 
 Theorem zero_ext_and:
@@ -2575,7 +2597,7 @@ Proof.
 Qed.
 
 Theorem sign_ext_widen:
-  forall x n n', 0 < n  <= n' ->
+  forall x n n', 0 < n <= n' ->
   sign_ext n' (sign_ext n x) = sign_ext n x.
 Proof.
   intros. destruct (zlt n' zwordsize).
@@ -2583,9 +2605,8 @@ Proof.
   auto.
   rewrite (zlt_false _ i n).
   destruct (zlt (n' - 1) n); f_equal; omega.
-  omega. omega.
+  omega.
   destruct (zlt i n'); omega.
-  omega. omega.
   apply sign_ext_above; auto.
 Qed.
 
@@ -2599,7 +2620,6 @@ Proof.
   auto.
   rewrite !zlt_false. auto. omega. omega. omega.
   destruct (zlt i n'); omega.
-  omega.
   apply sign_ext_above; auto.
 Qed.
 
@@ -2619,9 +2639,7 @@ Theorem sign_ext_narrow:
 Proof.
   intros. destruct (zlt n zwordsize).
   bit_solve. destruct (zlt i n); f_equal; apply zlt_true; omega.
-  omega.
   destruct (zlt i n); omega.
-  omega. omega.
   rewrite (sign_ext_above n'). auto. omega.
 Qed.
 
@@ -2633,7 +2651,7 @@ Proof.
   bit_solve.
   destruct (zlt i n); auto.
   rewrite zlt_true; auto. omega.
-  omega. omega. omega.
+  omega. omega.
   rewrite sign_ext_above; auto.
 Qed.
 
@@ -2648,7 +2666,7 @@ Theorem sign_ext_idem:
 Proof.
   intros. apply sign_ext_widen. omega.
 Qed.
-
+ 
 Theorem sign_ext_zero_ext:
   forall n x, 0 < n -> sign_ext n (zero_ext n x) = sign_ext n x.
 Proof.
@@ -2676,42 +2694,93 @@ Proof.
   rewrite <- (sign_ext_zero_ext n y H). congruence.
 Qed.
 
-Theorem zero_ext_shru_shl:
+Theorem shru_shl:
+  forall x y z, ltu y iwordsize = true -> ltu z iwordsize = true ->
+  shru (shl x y) z =
+  if ltu z y then shl (zero_ext (zwordsize - unsigned y) x) (sub y z)
+             else zero_ext (zwordsize - unsigned z) (shru x (sub z y)).
+Proof.
+  intros. apply ltu_iwordsize_inv in H; apply ltu_iwordsize_inv in H0.
+  unfold ltu. set (Y := unsigned y) in *; set (Z := unsigned z) in *.
+  apply same_bits_eq; intros. rewrite bits_shru by auto. fold Z.
+  destruct (zlt Z Y).
+- assert (A: unsigned (sub y z) = Y - Z).
+  { apply unsigned_repr. generalize wordsize_max_unsigned; omega. }
+  symmetry; rewrite bits_shl, A by omega.
+  destruct (zlt (i + Z) zwordsize).
++ rewrite bits_shl by omega. fold Y.
+  destruct (zlt i (Y - Z)); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+  rewrite bits_zero_ext by omega. rewrite zlt_true by omega. f_equal; omega.
++ rewrite bits_zero_ext by omega. rewrite ! zlt_false by omega. auto.
+- assert (A: unsigned (sub z y) = Z - Y).
+  { apply unsigned_repr. generalize wordsize_max_unsigned; omega. }
+  rewrite bits_zero_ext, bits_shru, A by omega.
+  destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+  rewrite bits_shl by omega. fold Y.
+  destruct (zlt (i + Z) Y).
++ rewrite zlt_false by omega. auto.
++ rewrite zlt_true by omega. f_equal; omega.
+Qed.
+
+Corollary zero_ext_shru_shl:
   forall n x,
   0 < n < zwordsize ->
   let y := repr (zwordsize - n) in
   zero_ext n x = shru (shl x y) y.
 Proof.
   intros.
-  assert (unsigned y = zwordsize - n).
-    unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
-  apply same_bits_eq; intros.
-  rewrite bits_zero_ext.
-  rewrite bits_shru; auto.
-  destruct (zlt i n).
-  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
-  omega. omega. omega.
-  rewrite zlt_false. auto. omega.
-  omega.
-Qed.
-
-Theorem sign_ext_shr_shl:
+  assert (A: unsigned y = zwordsize - n).
+  { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. }
+  assert (B: ltu y iwordsize = true).
+  { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; omega. }
+  rewrite shru_shl by auto. unfold ltu; rewrite zlt_false by omega.
+  rewrite sub_idem, shru_zero. f_equal. rewrite A; omega.
+Qed.
+
+Theorem shr_shl:
+  forall x y z, ltu y iwordsize = true -> ltu z iwordsize = true ->
+  shr (shl x y) z =
+  if ltu z y then shl (sign_ext (zwordsize - unsigned y) x) (sub y z)
+             else sign_ext (zwordsize - unsigned z) (shr x (sub z y)).
+Proof.
+  intros. apply ltu_iwordsize_inv in H; apply ltu_iwordsize_inv in H0.
+  unfold ltu. set (Y := unsigned y) in *; set (Z := unsigned z) in *.
+  apply same_bits_eq; intros. rewrite bits_shr by auto. fold Z.
+  rewrite bits_shl by (destruct (zlt (i + Z) zwordsize); omega). fold Y.
+  destruct (zlt Z Y).
+- assert (A: unsigned (sub y z) = Y - Z).
+  { apply unsigned_repr. generalize wordsize_max_unsigned; omega. }
+  rewrite bits_shl, A by omega.
+  destruct (zlt i (Y - Z)).
++ apply zlt_true. destruct (zlt (i + Z) zwordsize); omega.
++ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega).
+  rewrite bits_sign_ext by omega. f_equal. 
+  destruct (zlt (i + Z) zwordsize).
+  rewrite zlt_true by omega. omega.
+  rewrite zlt_false by omega. omega.
+- assert (A: unsigned (sub z y) = Z - Y).
+  { apply unsigned_repr. generalize wordsize_max_unsigned; omega. }
+  rewrite bits_sign_ext by omega.
+  rewrite bits_shr by (destruct (zlt i (zwordsize - Z)); omega).
+  rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega).
+  f_equal. destruct (zlt i (zwordsize - Z)).
++ rewrite ! zlt_true by omega. omega.
++ rewrite ! zlt_false by omega. rewrite zlt_true by omega. omega.
+Qed.
+
+Corollary sign_ext_shr_shl:
   forall n x,
   0 < n < zwordsize ->
   let y := repr (zwordsize - n) in
   sign_ext n x = shr (shl x y) y.
 Proof.
   intros.
-  assert (unsigned y = zwordsize - n).
-    unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega.
-  apply same_bits_eq; intros.
-  rewrite bits_sign_ext.
-  rewrite bits_shr; auto.
-  destruct (zlt i n).
-  rewrite zlt_true. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
-  omega. omega. omega.
-  rewrite zlt_false. rewrite bits_shl. rewrite zlt_false. f_equal. omega.
-  omega. omega. omega. omega. omega.
+  assert (A: unsigned y = zwordsize - n).
+  { unfold y. apply unsigned_repr. generalize wordsize_max_unsigned. omega. }
+  assert (B: ltu y iwordsize = true).
+  { unfold ltu; rewrite A, unsigned_repr_wordsize. apply zlt_true; omega. }
+  rewrite shr_shl by auto. unfold ltu; rewrite zlt_false by omega.
+  rewrite sub_idem, shr_zero. f_equal. rewrite A; omega.
 Qed.
 
 (** [zero_ext n x] is the unique integer congruent to [x] modulo [2^n]
@@ -2771,7 +2840,7 @@ Proof.
   apply eqmod_same_bits; intros.
   rewrite H0 in H1. rewrite H0.
   fold (testbit (sign_ext n x) i). rewrite bits_sign_ext.
-  rewrite zlt_true. auto. omega. omega. omega.
+  rewrite zlt_true. auto. omega. omega.
 Qed.
 
 Lemma eqmod_sign_ext:
@@ -2786,6 +2855,132 @@ Proof.
   apply eqmod_sign_ext'; auto.
 Qed.
 
+(** Combinations of shifts and zero/sign extensions *)
+
+Lemma shl_zero_ext:
+  forall n m x, 0 <= n ->
+  shl (zero_ext n x) m = zero_ext (n + unsigned m) (shl x m).
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_zero_ext, ! bits_shl by omega.
+  destruct (zlt i (unsigned m)).
+- rewrite zlt_true by omega; auto.
+- rewrite bits_zero_ext by omega.
+  destruct (zlt (i - unsigned m) n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+Qed.
+
+Lemma shl_sign_ext:
+  forall n m x, 0 < n ->
+  shl (sign_ext n x) m = sign_ext (n + unsigned m) (shl x m).
+Proof.
+  intros. generalize (unsigned_range m); intros.
+  apply same_bits_eq; intros.
+  rewrite bits_sign_ext, ! bits_shl by omega.
+  destruct (zlt i (n + unsigned m)).
+- rewrite bits_shl by auto. destruct (zlt i (unsigned m)); auto.
+  rewrite bits_sign_ext by omega. f_equal. apply zlt_true. omega.
+- rewrite zlt_false by omega. rewrite bits_shl by omega. rewrite zlt_false by omega.
+  rewrite bits_sign_ext by omega. f_equal. rewrite zlt_false by omega. omega.
+Qed.
+
+Lemma shru_zero_ext:
+  forall n m x, 0 <= n ->
+  shru (zero_ext (n + unsigned m) x) m = zero_ext n (shru x m).
+Proof.
+  intros. bit_solve.
+- destruct (zlt (i + unsigned m) zwordsize).
+* destruct (zlt i n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+* destruct (zlt i n); auto.
+- generalize (unsigned_range m); omega.
+- omega.
+Qed.
+
+Lemma shru_zero_ext_0:
+  forall n m x, n <= unsigned m ->
+  shru (zero_ext n x) m = zero.
+Proof.
+  intros. bit_solve.
+- destruct (zlt (i + unsigned m) zwordsize); auto.
+  apply zlt_false. omega.
+- generalize (unsigned_range m); omega.
+Qed.
+
+Lemma shr_sign_ext:
+  forall n m x, 0 < n -> n + unsigned m < zwordsize ->
+  shr (sign_ext (n + unsigned m) x) m = sign_ext n (shr x m).
+Proof.
+  intros. generalize (unsigned_range m); intros.
+  apply same_bits_eq; intros.
+  rewrite bits_sign_ext, bits_shr by auto.
+  rewrite bits_sign_ext, bits_shr.
+- f_equal.
+  destruct (zlt i n), (zlt (i + unsigned m) zwordsize).
++ apply zlt_true; omega.
++ apply zlt_true; omega.
++ rewrite zlt_false by omega. rewrite zlt_true by omega. omega.
++ rewrite zlt_false by omega. rewrite zlt_true by omega. omega.
+- destruct (zlt i n); omega.
+- destruct (zlt (i + unsigned m) zwordsize); omega.
+Qed.
+
+Lemma zero_ext_shru_min:
+  forall s x n, ltu n iwordsize = true ->
+  zero_ext s (shru x n) = zero_ext (Z.min s (zwordsize - unsigned n)) (shru x n).
+Proof.
+  intros. apply ltu_iwordsize_inv in H.
+  apply Z.min_case_strong; intros; auto.
+  bit_solve; try omega.
+  destruct (zlt i (zwordsize - unsigned n)).
+  rewrite zlt_true by omega. auto.
+  destruct (zlt i s); auto. rewrite zlt_false by omega; auto.
+Qed.
+
+Lemma sign_ext_shr_min:
+  forall s x n, ltu n iwordsize = true ->
+  sign_ext s (shr x n) = sign_ext (Z.min s (zwordsize - unsigned n)) (shr x n).
+Proof.
+  intros. apply ltu_iwordsize_inv in H.
+  rewrite Z.min_comm. 
+  destruct (Z.min_spec (zwordsize - unsigned n) s) as [[A B] | [A B]]; rewrite B; auto.
+  apply same_bits_eq; intros. rewrite ! bits_sign_ext by auto.
+  destruct (zlt i (zwordsize - unsigned n)). 
+  rewrite zlt_true by omega. auto.
+  assert (C: testbit (shr x n) (zwordsize - unsigned n - 1) = testbit x (zwordsize - 1)).
+  { rewrite bits_shr by omega. rewrite zlt_true by omega. f_equal; omega. }
+  rewrite C. destruct (zlt i s); rewrite bits_shr by omega.
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_false by omega. auto.
+Qed.
+
+Lemma shl_zero_ext_min:
+  forall s x n, ltu n iwordsize = true ->
+  shl (zero_ext s x) n = shl (zero_ext (Z.min s (zwordsize - unsigned n)) x) n.
+Proof.
+  intros. apply ltu_iwordsize_inv in H.
+  apply Z.min_case_strong; intros; auto.
+  apply same_bits_eq; intros. rewrite ! bits_shl by auto.
+  destruct (zlt i (unsigned n)); auto.
+  rewrite ! bits_zero_ext by omega.
+  destruct (zlt (i - unsigned n) s).
+  rewrite zlt_true by omega; auto.
+  rewrite zlt_false by omega; auto.
+Qed.
+
+Lemma shl_sign_ext_min:
+  forall s x n, ltu n iwordsize = true ->
+  shl (sign_ext s x) n = shl (sign_ext (Z.min s (zwordsize - unsigned n)) x) n.
+Proof.
+  intros. apply ltu_iwordsize_inv in H.
+  rewrite Z.min_comm. 
+  destruct (Z.min_spec (zwordsize - unsigned n) s) as [[A B] | [A B]]; rewrite B; auto.
+  apply same_bits_eq; intros. rewrite ! bits_shl by auto.
+  destruct (zlt i (unsigned n)); auto.
+  rewrite ! bits_sign_ext by omega. f_equal.
+  destruct (zlt (i - unsigned n) s).
+  rewrite zlt_true by omega; auto.
+  omegaContradiction.
+Qed.
+
 (** ** Properties of [one_bits] (decomposition in sum of powers of two) *)
 
 Theorem one_bits_range:
@@ -3504,6 +3699,190 @@ Proof.
   unfold shr, shr'; rewrite <- A; auto.
 Qed.
 
+Theorem shru'_shl':
+  forall x y z, Int.ltu y iwordsize' = true -> Int.ltu z iwordsize' = true ->
+  shru' (shl' x y) z =
+  if Int.ltu z y then shl' (zero_ext (zwordsize - Int.unsigned y) x) (Int.sub y z)
+                 else zero_ext (zwordsize - Int.unsigned z) (shru' x (Int.sub z y)).
+Proof.
+  intros. apply Int.ltu_inv in H; apply Int.ltu_inv in H0.
+  change (Int.unsigned iwordsize') with zwordsize in *.
+  unfold Int.ltu. set (Y := Int.unsigned y) in *; set (Z := Int.unsigned z) in *.
+  apply same_bits_eq; intros. rewrite bits_shru' by auto. fold Z.
+  destruct (zlt Z Y).
+- assert (A: Int.unsigned (Int.sub y z) = Y - Z).
+  { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. }
+  symmetry; rewrite bits_shl', A by omega.
+  destruct (zlt (i + Z) zwordsize).
++ rewrite bits_shl' by omega. fold Y.
+  destruct (zlt i (Y - Z)); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+  rewrite bits_zero_ext by omega. rewrite zlt_true by omega. f_equal; omega.
++ rewrite bits_zero_ext by omega. rewrite ! zlt_false by omega. auto.
+- assert (A: Int.unsigned (Int.sub z y) = Z - Y).
+  { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. }
+  rewrite bits_zero_ext, bits_shru', A by omega.
+  destruct (zlt (i + Z) zwordsize); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+  rewrite bits_shl' by omega. fold Y.
+  destruct (zlt (i + Z) Y).
++ rewrite zlt_false by omega. auto.
++ rewrite zlt_true by omega. f_equal; omega.
+Qed.
+
+Theorem shr'_shl':
+  forall x y z, Int.ltu y iwordsize' = true -> Int.ltu z iwordsize' = true ->
+  shr' (shl' x y) z =
+  if Int.ltu z y then shl' (sign_ext (zwordsize - Int.unsigned y) x) (Int.sub y z)
+                 else sign_ext (zwordsize - Int.unsigned z) (shr' x (Int.sub z y)).
+Proof.
+  intros. apply Int.ltu_inv in H; apply Int.ltu_inv in H0.
+  change (Int.unsigned iwordsize') with zwordsize in *.
+  unfold Int.ltu. set (Y := Int.unsigned y) in *; set (Z := Int.unsigned z) in *.
+  apply same_bits_eq; intros. rewrite bits_shr' by auto. fold Z.
+  rewrite bits_shl' by (destruct (zlt (i + Z) zwordsize); omega). fold Y.
+  destruct (zlt Z Y).
+- assert (A: Int.unsigned (Int.sub y z) = Y - Z).
+  { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. }
+  rewrite bits_shl', A by omega.
+  destruct (zlt i (Y - Z)).
++ apply zlt_true. destruct (zlt (i + Z) zwordsize); omega.
++ rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega).
+  rewrite bits_sign_ext by omega. f_equal. 
+  destruct (zlt (i + Z) zwordsize).
+  rewrite zlt_true by omega. omega.
+  rewrite zlt_false by omega. omega.
+- assert (A: Int.unsigned (Int.sub z y) = Z - Y).
+  { apply Int.unsigned_repr. assert (zwordsize < Int.max_unsigned) by reflexivity. omega. }
+  rewrite bits_sign_ext by omega.
+  rewrite bits_shr' by (destruct (zlt i (zwordsize - Z)); omega).
+  rewrite A. rewrite zlt_false by (destruct (zlt (i + Z) zwordsize); omega).
+  f_equal. destruct (zlt i (zwordsize - Z)).
++ rewrite ! zlt_true by omega. omega.
++ rewrite ! zlt_false by omega. rewrite zlt_true by omega. omega.
+Qed.
+
+Lemma shl'_zero_ext:
+  forall n m x, 0 <= n ->
+  shl' (zero_ext n x) m = zero_ext (n + Int.unsigned m) (shl' x m).
+Proof.
+  intros. apply same_bits_eq; intros.
+  rewrite bits_zero_ext, ! bits_shl' by omega.
+  destruct (zlt i (Int.unsigned m)).
+- rewrite zlt_true by omega; auto.
+- rewrite bits_zero_ext by omega.
+  destruct (zlt (i - Int.unsigned m) n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+Qed.
+
+Lemma shl'_sign_ext:
+  forall n m x, 0 < n ->
+  shl' (sign_ext n x) m = sign_ext (n + Int.unsigned m) (shl' x m).
+Proof.
+  intros. generalize (Int.unsigned_range m); intros.
+  apply same_bits_eq; intros.
+  rewrite bits_sign_ext, ! bits_shl' by omega.
+  destruct (zlt i (n + Int.unsigned m)).
+- rewrite bits_shl' by auto. destruct (zlt i (Int.unsigned m)); auto.
+  rewrite bits_sign_ext by omega. f_equal. apply zlt_true. omega.
+- rewrite zlt_false by omega. rewrite bits_shl' by omega. rewrite zlt_false by omega.
+  rewrite bits_sign_ext by omega. f_equal. rewrite zlt_false by omega. omega.
+Qed.
+
+Lemma shru'_zero_ext:
+  forall n m x, 0 <= n ->
+  shru' (zero_ext (n + Int.unsigned m) x) m = zero_ext n (shru' x m).
+Proof.
+  intros. generalize (Int.unsigned_range m); intros.
+  bit_solve; [|omega]. rewrite bits_shru', bits_zero_ext, bits_shru' by omega.
+  destruct (zlt (i + Int.unsigned m) zwordsize).
+* destruct (zlt i n); [rewrite zlt_true by omega|rewrite zlt_false by omega]; auto.
+* destruct (zlt i n); auto.
+Qed.
+
+Lemma shru'_zero_ext_0:
+  forall n m x, n <= Int.unsigned m ->
+  shru' (zero_ext n x) m = zero.
+Proof.
+  intros. generalize (Int.unsigned_range m); intros.
+  bit_solve. rewrite bits_shru', bits_zero_ext by omega.
+  destruct (zlt (i + Int.unsigned m) zwordsize); auto.
+  apply zlt_false. omega.
+Qed.
+
+Lemma shr'_sign_ext:
+  forall n m x, 0 < n -> n + Int.unsigned m < zwordsize ->
+  shr' (sign_ext (n + Int.unsigned m) x) m = sign_ext n (shr' x m).
+Proof.
+  intros. generalize (Int.unsigned_range m); intros.
+  apply same_bits_eq; intros.
+  rewrite bits_sign_ext, bits_shr' by auto.
+  rewrite bits_sign_ext, bits_shr'.
+- f_equal.
+  destruct (zlt i n), (zlt (i + Int.unsigned m) zwordsize).
++ apply zlt_true; omega.
++ apply zlt_true; omega.
++ rewrite zlt_false by omega. rewrite zlt_true by omega. omega.
++ rewrite zlt_false by omega. rewrite zlt_true by omega. omega.
+- destruct (zlt i n); omega.
+- destruct (zlt (i + Int.unsigned m) zwordsize); omega.
+Qed.
+
+Lemma zero_ext_shru'_min:
+  forall s x n, Int.ltu n iwordsize' = true ->
+  zero_ext s (shru' x n) = zero_ext (Z.min s (zwordsize - Int.unsigned n)) (shru' x n).
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned iwordsize') with zwordsize in H.
+  apply Z.min_case_strong; intros; auto.
+  bit_solve; try omega. rewrite ! bits_shru' by omega. 
+  destruct (zlt i (zwordsize - Int.unsigned n)).
+  rewrite zlt_true by omega. auto.
+  destruct (zlt i s); auto. rewrite zlt_false by omega; auto.
+Qed.
+
+Lemma sign_ext_shr'_min:
+  forall s x n, Int.ltu n iwordsize' = true ->
+  sign_ext s (shr' x n) = sign_ext (Z.min s (zwordsize - Int.unsigned n)) (shr' x n).
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned iwordsize') with zwordsize in H.
+  rewrite Z.min_comm. 
+  destruct (Z.min_spec (zwordsize - Int.unsigned n) s) as [[A B] | [A B]]; rewrite B; auto.
+  apply same_bits_eq; intros. rewrite ! bits_sign_ext by auto.
+  destruct (zlt i (zwordsize - Int.unsigned n)). 
+  rewrite zlt_true by omega. auto.
+  assert (C: testbit (shr' x n) (zwordsize - Int.unsigned n - 1) = testbit x (zwordsize - 1)).
+  { rewrite bits_shr' by omega. rewrite zlt_true by omega. f_equal; omega. }
+  rewrite C. destruct (zlt i s); rewrite bits_shr' by omega.
+  rewrite zlt_false by omega. auto.
+  rewrite zlt_false by omega. auto.
+Qed.
+
+Lemma shl'_zero_ext_min:
+  forall s x n, Int.ltu n iwordsize' = true ->
+  shl' (zero_ext s x) n = shl' (zero_ext (Z.min s (zwordsize - Int.unsigned n)) x) n.
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned iwordsize') with zwordsize in H.
+  apply Z.min_case_strong; intros; auto.
+  apply same_bits_eq; intros. rewrite ! bits_shl' by auto.
+  destruct (zlt i (Int.unsigned n)); auto.
+  rewrite ! bits_zero_ext by omega.
+  destruct (zlt (i - Int.unsigned n) s).
+  rewrite zlt_true by omega; auto.
+  rewrite zlt_false by omega; auto.
+Qed.
+
+Lemma shl'_sign_ext_min:
+  forall s x n, Int.ltu n iwordsize' = true ->
+  shl' (sign_ext s x) n = shl' (sign_ext (Z.min s (zwordsize - Int.unsigned n)) x) n.
+Proof.
+  intros. apply Int.ltu_inv in H. change (Int.unsigned iwordsize') with zwordsize in H.
+  rewrite Z.min_comm. 
+  destruct (Z.min_spec (zwordsize - Int.unsigned n) s) as [[A B] | [A B]]; rewrite B; auto.
+  apply same_bits_eq; intros. rewrite ! bits_shl' by auto.
+  destruct (zlt i (Int.unsigned n)); auto.
+  rewrite ! bits_sign_ext by omega. f_equal.
+  destruct (zlt (i - Int.unsigned n) s).
+  rewrite zlt_true by omega; auto.
+  omegaContradiction.
+Qed.
+
 (** Powers of two with exponents given as 32-bit ints *)
 
 Definition one_bits' (x: int) : list Int.int :=
diff --git a/lib/Zbits.v b/lib/Zbits.v
index dca2a5a2..27586aff 100644
--- a/lib/Zbits.v
+++ b/lib/Zbits.v
@@ -557,7 +557,7 @@ Definition Zzero_ext (n: Z) (x: Z) : Z :=
 Definition Zsign_ext (n: Z) (x: Z) : Z :=
   Z.iter (Z.pred n)
     (fun rec x => Zshiftin (Z.odd x) (rec (Z.div2 x)))
-    (fun x => if Z.odd x then -1 else 0)
+    (fun x => if Z.odd x && zlt 0 n then -1 else 0)
     x.
 
 Lemma Ziter_base:
@@ -606,32 +606,34 @@ Proof.
 Qed.
 
 Lemma Zsign_ext_spec:
-  forall n x i, 0 <= i -> 0 < n ->
+  forall n x i, 0 <= i ->
   Z.testbit (Zsign_ext n x) i = Z.testbit x (if zlt i n then i else n - 1).
 Proof.
-  intros n0 x i I0 N0.
-  revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1).
-  - unfold Zsign_ext. intros.
-    destruct (zeq x 1).
-    + subst x; simpl.
-      replace (if zlt i 1 then i else 0) with 0.
-      rewrite Ztestbit_base.
-      destruct (Z.odd x0).
-      apply Ztestbit_m1; auto.
-      apply Ztestbit_0.
-      destruct (zlt i 1); omega.
-    + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)).
-      rewrite Ziter_succ. rewrite Ztestbit_shiftin.
-      destruct (zeq i 0).
-      * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega.
-      * rewrite H. unfold x1. destruct (zlt (Z.pred i) (Z.pred x)).
-        rewrite zlt_true. rewrite (Ztestbit_eq i x0); auto. rewrite zeq_false; auto. omega.
-        rewrite zlt_false. rewrite (Ztestbit_eq (x - 1) x0). rewrite zeq_false; auto.
-        omega. omega. omega. unfold x1; omega. omega.
-      * omega.
-      * unfold x1; omega.
-      * omega.
-  - omega.
+  intros n0 x i I0. unfold Zsign_ext. 
+  unfold proj_sumbool; destruct (zlt 0 n0) as [N0|N0]; simpl.
+- revert x i I0. pattern n0. apply Zlt_lower_bound_ind with (z := 1); [ | omega ].
+  unfold Zsign_ext. intros.
+  destruct (zeq x 1).
+  + subst x; simpl.
+    replace (if zlt i 1 then i else 0) with 0.
+    rewrite Ztestbit_base.
+    destruct (Z.odd x0); [ apply Ztestbit_m1; auto | apply Ztestbit_0 ].
+    destruct (zlt i 1); omega.
+  + set (x1 := Z.pred x). replace x1 with (Z.succ (Z.pred x1)) by omega.
+    rewrite Ziter_succ by (unfold x1; omega). rewrite Ztestbit_shiftin by auto.
+    destruct (zeq i 0).
+    * subst i. rewrite zlt_true. rewrite Ztestbit_base; auto. omega.
+    * rewrite H by (unfold x1; omega).
+      unfold x1; destruct (zlt (Z.pred i) (Z.pred x)).
+      ** rewrite zlt_true by omega.
+         rewrite (Ztestbit_eq i x0) by omega.
+         rewrite zeq_false by omega. auto.
+      ** rewrite zlt_false by omega.
+         rewrite (Ztestbit_eq (x - 1) x0) by omega.
+         rewrite zeq_false by omega. auto.
+- rewrite Ziter_base by omega. rewrite andb_false_r. 
+  rewrite Z.testbit_0_l, Z.testbit_neg_r. auto.
+  destruct (zlt i n0); omega.
 Qed.
 
 (** [Zzero_ext n x] is [x modulo 2^n] *)
@@ -661,7 +663,7 @@ Qed.
 (** Relation between [Zsign_ext n x] and (Zzero_ext n x] *)
 
 Lemma Zsign_ext_zero_ext:
-  forall n, 0 < n -> forall x,
+  forall n, 0 <= n -> forall x,
   Zsign_ext n x = Zzero_ext n x - (if Z.testbit x (n - 1) then two_p n else 0).
 Proof.
   intros. apply equal_same_bits; intros.
@@ -698,12 +700,12 @@ Proof.
   assert (C: two_p n = 2 * two_p (n - 1)).
   { rewrite <- two_p_S by omega. f_equal; omega. }
   rewrite Zzero_ext_spec, zlt_true in B by omega.
-  rewrite Zsign_ext_zero_ext by auto. rewrite B.
+  rewrite Zsign_ext_zero_ext by omega. rewrite B.
   destruct (zlt (Zzero_ext n x) (two_p (n - 1))); omega.
 Qed.
 
 Lemma eqmod_Zsign_ext:
-  forall n x, 0 < n ->
+  forall n x, 0 <= n ->
   eqmod (two_p n) (Zsign_ext n x) x.
 Proof.
   intros. rewrite Zsign_ext_zero_ext by auto. 
@@ -822,6 +824,14 @@ Proof.
   apply Z.log2_nonneg.
 - reflexivity.
 Qed.
+
+Lemma Z_is_power2_nonneg:
+  forall x i, Z_is_power2 x = Some i -> 0 <= i.
+Proof.
+  unfold Z_is_power2; intros. destruct x; try discriminate.
+  destruct (P_is_power2 p) eqn:P; try discriminate.
+  replace i with (Z.log2 (Z.pos p)) by congruence. apply Z.log2_nonneg.
+Qed.
  
 Lemma Z_is_power2_sound:
   forall x i, Z_is_power2 x = Some i -> x = two_p i /\ i = Z.log2 x.
@@ -857,6 +867,12 @@ Qed.
 
 Definition Z_is_power2m1 (x: Z) : option Z := Z_is_power2 (Z.succ x).
 
+Lemma Z_is_power2m1_nonneg:
+  forall x i, Z_is_power2m1 x = Some i -> 0 <= i.
+Proof.
+  unfold Z_is_power2m1; intros. eapply Z_is_power2_nonneg; eauto.
+Qed.
+
 Lemma Z_is_power2m1_sound:
   forall x i, Z_is_power2m1 x = Some i -> x = two_p i - 1.
 Proof.
@@ -1026,3 +1042,60 @@ Proof.
   exploit (Zsize_interval_1 y). omega.
   omega.
 Qed.
+
+(** ** Bit insertion, bit extraction *)
+
+(** Extract and optionally sign-extend bits [from...from+len-1] of [x] *)
+Definition Zextract_u (x: Z) (from: Z) (len: Z) : Z :=
+  Zzero_ext len (Z.shiftr x from).
+
+Definition Zextract_s (x: Z) (from: Z) (len: Z) : Z :=
+  Zsign_ext len (Z.shiftr x from).
+
+Lemma Zextract_u_spec:
+  forall x from len i,
+  0 <= from -> 0 <= len -> 0 <= i ->
+  Z.testbit (Zextract_u x from len) i =
+  if zlt i len then Z.testbit x (from + i) else false.
+Proof.
+  unfold Zextract_u; intros. rewrite Zzero_ext_spec, Z.shiftr_spec by auto.
+  rewrite Z.add_comm. auto.
+Qed.
+
+Lemma Zextract_s_spec:
+  forall x from len i,
+  0 <= from -> 0 < len -> 0 <= i ->
+  Z.testbit (Zextract_s x from len) i =
+  Z.testbit x (from + (if zlt i len then i else len - 1)).
+Proof.
+  unfold Zextract_s; intros. rewrite Zsign_ext_spec by auto. rewrite Z.shiftr_spec.
+  rewrite Z.add_comm. auto.
+  destruct (zlt i len); omega.
+Qed.
+
+(** Insert bits [0...len-1] of [y] into bits [to...to+len-1] of [x] *)
+
+Definition Zinsert (x y: Z) (to: Z) (len: Z) : Z :=
+  let mask := Z.shiftl (two_p len - 1) to in
+  Z.lor (Z.land (Z.shiftl y to) mask) (Z.ldiff x mask).
+
+Lemma Zinsert_spec:
+  forall x y to len i,
+  0 <= to -> 0 <= len -> 0 <= i ->
+  Z.testbit (Zinsert x y to len) i =
+    if zle to i && zlt i (to + len)
+    then Z.testbit y (i - to)
+    else Z.testbit x i.
+Proof.
+  unfold Zinsert; intros. set (mask := two_p len - 1).
+  assert (M: forall j, 0 <= j -> Z.testbit mask j = if zlt j len then true else false).
+  { intros; apply Ztestbit_two_p_m1; auto. }
+  rewrite Z.lor_spec, Z.land_spec, Z.ldiff_spec by auto. 
+  destruct (zle to i).
+- rewrite ! Z.shiftl_spec by auto. rewrite ! M by omega. 
+  unfold proj_sumbool; destruct (zlt (i - to) len); simpl;
+  rewrite andb_true_r, andb_false_r.
++ rewrite zlt_true by omega. apply orb_false_r.
++ rewrite zlt_false by omega; auto.
+- rewrite ! Z.shiftl_spec_low by omega. simpl. apply andb_true_r.
+Qed.