Lvc.CompCert.Integers


Formalizations of machine integers modulo 2N.

Require Import Eqdep_dec.
Require Import Zquot.
Require Import Zwf.
Require Import Coqlib.

Comparisons


Inductive comparison : Type :=
  | Ceq : comparison
  | Cne : comparison
  | Clt : comparison
  | Cle : comparison
  | Cgt : comparison
  | Cge : comparison.
Definition negate_comparison (c: comparison): comparison :=
  match c with
  | CeqCne
  | CneCeq
  | CltCge
  | CleCgt
  | CgtCle
  | CgeClt
  end.

Definition swap_comparison (c: comparison): comparison :=
  match c with
  | CeqCeq
  | CneCne
  | CltCgt
  | CleCge
  | CgtClt
  | CgeCle
  end.

Parameterization by the word size, in bits.


Module Type WORDSIZE.
  Variable wordsize: nat.
  Axiom wordsize_not_zero: wordsize 0%nat.
End WORDSIZE.

Local Unset Elimination Schemes.
Local Unset Case Analysis Schemes.

Module Make(WS: WORDSIZE).

Definition wordsize: nat := WS.wordsize.
Definition zwordsize: Z := Z_of_nat wordsize.
Definition modulus : Z := two_power_nat wordsize.
Definition half_modulus : Z := modulus / 2.
Definition max_unsigned : Z := modulus - 1.
Definition max_signed : Z := half_modulus - 1.
Definition min_signed : Z := - half_modulus.

Remark wordsize_pos: zwordsize > 0.
Proof.
  unfold zwordsize, wordsize. generalize WS.wordsize_not_zero. omega.
Qed.

Remark modulus_power: modulus = two_p zwordsize.
Proof.
  unfold modulus. apply two_power_nat_two_p.
Qed.

Remark modulus_pos: modulus > 0.
Proof.
  rewrite modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
Qed.

Representation of machine integers

A machine integer (type int) is represented as a Coq arbitrary-precision integer (type Z) plus a proof that it is in the range 0 (included) to modulus (excluded).

Record int : Type := mkint { intval: Z; intrange: -1 < intval < modulus }.

Fast normalization modulo 2^wordsize

Fixpoint P_mod_two_p (p: positive) (n: nat) {struct n} : Z :=
  match n with
  | O ⇒ 0
  | S m
      match p with
      | xH ⇒ 1
      | xO qZ.double (P_mod_two_p q m)
      | xI qZ.succ_double (P_mod_two_p q m)
      end
  end.

Definition Z_mod_modulus (x: Z) : Z :=
  match x with
  | Z0 ⇒ 0
  | Zpos pP_mod_two_p p wordsize
  | Zneg plet r := P_mod_two_p p wordsize in if zeq r 0 then 0 else modulus - r
  end.

Lemma P_mod_two_p_range:
   n p, 0 P_mod_two_p p n < two_power_nat n.
Proof.
  induction n; simpl; intros.
  - rewrite two_power_nat_O. omega.
  - rewrite two_power_nat_S. destruct p.
    + generalize (IHn p). rewrite Z.succ_double_spec. omega.
    + generalize (IHn p). rewrite Z.double_spec. omega.
    + generalize (two_power_nat_pos n). omega.
Qed.

Lemma P_mod_two_p_eq:
   n p, P_mod_two_p p n = (Zpos p) mod (two_power_nat n).
Proof.
  assert ( n p, y, Zpos p = y × two_power_nat n + P_mod_two_p p n).
  {
    induction n; simpl; intros.
    - rewrite two_power_nat_O. (Zpos p). ring.
    - rewrite two_power_nat_S. destruct p.
      + destruct (IHn p) as [y EQ]. y.
        change (Zpos p~1) with (2 × Zpos p + 1). rewrite EQ.
        rewrite Z.succ_double_spec. ring.
      + destruct (IHn p) as [y EQ]. y.
        change (Zpos p~0) with (2 × Zpos p). rewrite EQ.
        rewrite (Z.double_spec (P_mod_two_p p n)). ring.
      + 0; omega.
  }
  intros.
  destruct (H n p) as [y EQ].
  symmetry. apply Zmod_unique with y. auto. apply P_mod_two_p_range.
Qed.

Lemma Z_mod_modulus_range:
   x, 0 Z_mod_modulus x < modulus.
Proof.
  intros; unfold Z_mod_modulus.
  destruct x.
  - generalize modulus_pos; omega.
  - apply P_mod_two_p_range.
  - set (r := P_mod_two_p p wordsize).
    assert (0 r < modulus) by apply P_mod_two_p_range.
    destruct (zeq r 0).
    + generalize modulus_pos; omega.
    + omega.
Qed.

Lemma Z_mod_modulus_range':
   x, -1 < Z_mod_modulus x < modulus.
Proof.
  intros. generalize (Z_mod_modulus_range x); omega.
Qed.

Lemma Z_mod_modulus_eq:
   x, Z_mod_modulus x = x mod modulus.
Proof.
  intros. unfold Z_mod_modulus. destruct x.
  - rewrite Zmod_0_l. auto.
  - apply P_mod_two_p_eq.
  - generalize (P_mod_two_p_range wordsize p) (P_mod_two_p_eq wordsize p).
    fold modulus. intros A B.
    exploit (Z_div_mod_eq (Zpos p) modulus). apply modulus_pos. intros C.
    set (q := Zpos p / modulus) in ×.
    set (r := P_mod_two_p p wordsize) in ×.
    rewrite <- B in C.
    change (Z.neg p) with (- (Z.pos p)). destruct (zeq r 0).
    + symmetry. apply Zmod_unique with (-q). rewrite C; rewrite e. ring.
      generalize modulus_pos; omega.
    + symmetry. apply Zmod_unique with (-q - 1). rewrite C. ring.
      omega.
Qed.

The unsigned and signed functions return the Coq integer corresponding to the given machine integer, interpreted as unsigned or signed respectively.

Definition unsigned (n: int) : Z := intval n.

Definition signed (n: int) : Z :=
  let x := unsigned n in
  if zlt x half_modulus then x else x - modulus.

Conversely, repr takes a Coq integer and returns the corresponding machine integer. The argument is treated modulo modulus.

Definition repr (x: Z) : int :=
  mkint (Z_mod_modulus x) (Z_mod_modulus_range' x).

Definition zero := repr 0.
Definition one := repr 1.
Definition mone := repr (-1).
Definition iwordsize := repr zwordsize.

Lemma mkint_eq:
   x y Px Py, x = y mkint x Px = mkint y Py.
Proof.
  intros. subst y.
  assert ( (n m: Z) (P1 P2: n < m), P1 = P2).
  {
    unfold Zlt; intros.
    apply eq_proofs_unicity.
    intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence).
  }
  destruct Px as [Px1 Px2]. destruct Py as [Py1 Py2].
  rewrite (H _ _ Px1 Py1).
  rewrite (H _ _ Px2 Py2).
  reflexivity.
Qed.

Lemma eq_dec: (x y: int), {x = y} + {x y}.
Proof.
  intros. destruct x; destruct y. destruct (zeq intval0 intval1).
  left. apply mkint_eq. auto.
  right. red; intro. injection H. exact n.
Defined.

Arithmetic and logical operations over machine integers


Definition eq (x y: int) : bool :=
  if zeq (unsigned x) (unsigned y) then true else false.
Definition lt (x y: int) : bool :=
  if zlt (signed x) (signed y) then true else false.
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 add (x y: int) : int :=
  repr (unsigned x + unsigned y).
Definition sub (x y: int) : int :=
  repr (unsigned x - unsigned y).
Definition mul (x y: int) : int :=
  repr (unsigned x × unsigned y).

Definition divs (x y: int) : int :=
  repr (Z.quot (signed x) (signed y)).
Definition mods (x y: int) : int :=
  repr (Z.rem (signed x) (signed y)).

Definition divu (x y: int) : int :=
  repr (unsigned x / unsigned y).
Definition modu (x y: int) : int :=
  repr ((unsigned x) mod (unsigned y)).

Bitwise boolean operations.

Definition and (x y: int): int := repr (Z.land (unsigned x) (unsigned y)).
Definition or (x y: int): int := repr (Z.lor (unsigned x) (unsigned y)).
Definition xor (x y: int) : int := repr (Z.lxor (unsigned x) (unsigned y)).

Definition not (x: int) : int := xor x mone.

Shifts and rotates.

Definition shl (x y: int): int := repr (Z.shiftl (unsigned x) (unsigned y)).
Definition shru (x y: int): int := repr (Z.shiftr (unsigned x) (unsigned y)).
Definition shr (x y: int): int := repr (Z.shiftr (signed x) (unsigned y)).

Definition rol (x y: int) : int :=
  let n := (unsigned y) mod zwordsize in
  repr (Z.lor (Z.shiftl (unsigned x) n) (Z.shiftr (unsigned x) (zwordsize - n))).
Definition ror (x y: int) : int :=
  let n := (unsigned y) mod zwordsize in
  repr (Z.lor (Z.shiftr (unsigned x) n) (Z.shiftl (unsigned x) (zwordsize - n))).

Definition rolm (x a m: int): int := and (rol x a) m.

Viewed as signed divisions by powers of two, shrx rounds towards zero, while shr rounds towards minus infinity.

Definition shrx (x y: int): int :=
  divs x (shl one y).

High half of full multiply.

Definition mulhu (x y: int): int := repr ((unsigned x × unsigned y) / modulus).
Definition mulhs (x y: int): int := repr ((signed x × signed y) / modulus).

Condition flags

Definition negative (x: int): int :=
  if lt x zero then one else zero.

Definition add_carry (x y cin: int): int :=
  if zlt (unsigned x + unsigned y + unsigned cin) modulus then zero else one.

Definition add_overflow (x y cin: int): int :=
  let s := signed x + signed y + signed cin in
  if zle min_signed s && zle s max_signed then zero else one.

Definition sub_borrow (x y bin: int): int :=
  if zlt (unsigned x - unsigned y - unsigned bin) 0 then one else zero.

Definition sub_overflow (x y bin: int): int :=
  let s := signed x - signed y - signed bin in
  if zle min_signed s && zle s max_signed then zero else one.

shr_carry x y is 1 if x is negative and at least one 1 bit is shifted away.

Definition shr_carry (x y: int) : int :=
  if lt x zero && negb (eq (and x (sub (shl one y) one)) zero)
  then one else zero.

Zero and sign extensions

Definition Zshiftin (b: bool) (x: Z) : Z :=
  if b then Z.succ_double x else Z.double x.

In pseudo-code:
    Fixpoint Zzero_ext (n: Z) (x: Z) : Z :=
      if zle n 0 then
        0
      else
        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
    Fixpoint Zsign_ext (n: Z) (x: Z) : Z :=
      if zle n 1 then
        if Z.odd x then -1 else 0
      else
        Zshiftin (Z.odd x) (Zzero_ext (Z.pred n) (Z.div2 x)).
We encode this nat-like recursion using the Z.iter iteration function, in order to make the Zzero_ext and Zsign_ext functions efficiently executable within Coq.

Definition Zzero_ext (n: Z) (x: Z) : Z :=
  Z.iter n
    (fun rec xZshiftin (Z.odd x) (rec (Z.div2 x)))
    (fun x ⇒ 0)
    x.

Definition Zsign_ext (n: Z) (x: Z) : Z :=
  Z.iter (Z.pred n)
    (fun rec xZshiftin (Z.odd x) (rec (Z.div2 x)))
    (fun xif Z.odd x then -1 else 0)
    x.

Definition zero_ext (n: Z) (x: int) : int := repr (Zzero_ext n (unsigned x)).

Definition sign_ext (n: Z) (x: int) : int := repr (Zsign_ext n (unsigned x)).

Decomposition of a number as a sum of powers of two.

Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
  match n with
  | Onil
  | S m
      if Z.odd x
      then i :: Z_one_bits m (Z.div2 x) (i+1)
      else Z_one_bits m (Z.div2 x) (i+1)
  end.

Definition one_bits (x: int) : list int :=
  List.map repr (Z_one_bits wordsize (unsigned x) 0).

Recognition of powers of two.

Definition is_power2 (x: int) : option int :=
  match Z_one_bits wordsize (unsigned x) 0 with
  | i :: nilSome (repr i)
  | _None
  end.

Comparisons.

Definition cmp (c: comparison) (x y: int) : bool :=
  match c with
  | Ceqeq x y
  | Cnenegb (eq x y)
  | Cltlt x y
  | Clenegb (lt y x)
  | Cgtlt y x
  | Cgenegb (lt x y)
  end.

Definition cmpu (c: comparison) (x y: int) : bool :=
  match c with
  | Ceqeq x y
  | Cnenegb (eq x y)
  | Cltltu x y
  | Clenegb (ltu y x)
  | Cgtltu y x
  | Cgenegb (ltu x y)
  end.

Definition is_false (x: int) : Prop := x = zero.
Definition is_true (x: int) : Prop := x zero.
Definition notbool (x: int) : int := if eq x zero then one else zero.

Properties of integers and integer arithmetic

Properties of modulus, max_unsigned, etc.


Remark half_modulus_power:
  half_modulus = two_p (zwordsize - 1).
Proof.
  unfold half_modulus. rewrite modulus_power.
  set (ws1 := zwordsize - 1).
  replace (zwordsize) with (Zsucc ws1).
  rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega.
  unfold ws1. generalize wordsize_pos; omega.
  unfold ws1. omega.
Qed.

Remark half_modulus_modulus: modulus = 2 × half_modulus.
Proof.
  rewrite half_modulus_power. rewrite modulus_power.
  rewrite <- two_p_S. apply f_equal. omega.
  generalize wordsize_pos; omega.
Qed.

Relative positions, from greatest to smallest:
      max_unsigned
      max_signed
      2*wordsize-1
      wordsize
      0
      min_signed

Remark half_modulus_pos: half_modulus > 0.
Proof.
  rewrite half_modulus_power. apply two_p_gt_ZERO. generalize wordsize_pos; omega.
Qed.

Remark min_signed_neg: min_signed < 0.
Proof.
  unfold min_signed. generalize half_modulus_pos. omega.
Qed.

Remark max_signed_pos: max_signed 0.
Proof.
  unfold max_signed. generalize half_modulus_pos. omega.
Qed.

Remark wordsize_max_unsigned: zwordsize max_unsigned.
Proof.
  assert (zwordsize < modulus).
    rewrite modulus_power. apply two_p_strict.
    generalize wordsize_pos. omega.
  unfold max_unsigned. omega.
Qed.

Remark two_wordsize_max_unsigned: 2 × zwordsize - 1 max_unsigned.
Proof.
  assert (2 × zwordsize - 1 < modulus).
    rewrite modulus_power. apply two_p_strict_2. generalize wordsize_pos; omega.
  unfold max_unsigned; omega.
Qed.

Remark max_signed_unsigned: max_signed < max_unsigned.
Proof.
  unfold max_signed, max_unsigned. rewrite half_modulus_modulus.
  generalize half_modulus_pos. omega.
Qed.

Lemma unsigned_repr_eq:
   x, unsigned (repr x) = Zmod x modulus.
Proof.
  intros. simpl. apply Z_mod_modulus_eq.
Qed.

Lemma signed_repr_eq:
   x, signed (repr x) = if zlt (Zmod x modulus) half_modulus then Zmod x modulus else Zmod x modulus - modulus.
Proof.
  intros. unfold signed. rewrite unsigned_repr_eq. auto.
Qed.

Modulo arithmetic

We define and state properties of equality and arithmetic modulo a positive integer.

Section EQ_MODULO.

Variable modul: Z.
Hypothesis modul_pos: modul > 0.

Definition eqmod (x y: Z) : Prop := k, x = k × modul + y.

Lemma eqmod_refl: x, eqmod x x.
Proof.
  intros; red. 0. omega.
Qed.

Lemma eqmod_refl2: x y, x = y eqmod x y.
Proof.
  intros. subst y. apply eqmod_refl.
Qed.

Lemma eqmod_sym: x y, eqmod x y eqmod y x.
Proof.
  intros x y [k EQ]; red. (-k). subst x. ring.
Qed.

Lemma eqmod_trans: x y z, eqmod x y eqmod y z eqmod x z.
Proof.
  intros x y z [k1 EQ1] [k2 EQ2]; red.
   (k1 + k2). subst x; subst y. ring.
Qed.

Lemma eqmod_small_eq:
   x y, eqmod x y 0 x < modul 0 y < modul x = y.
Proof.
  intros x y [k EQ] I1 I2.
  generalize (Zdiv_unique _ _ _ _ EQ I2). intro.
  rewrite (Zdiv_small x modul I1) in H. subst k. omega.
Qed.

Lemma eqmod_mod_eq:
   x y, eqmod x y x mod modul = y mod modul.
Proof.
  intros x y [k EQ]. subst x.
  rewrite Zplus_comm. apply Z_mod_plus. auto.
Qed.

Lemma eqmod_mod:
   x, eqmod x (x mod modul).
Proof.
  intros; red. (x / modul).
  rewrite Zmult_comm. apply Z_div_mod_eq. auto.
Qed.

Lemma eqmod_add:
   a b c d, eqmod a b eqmod c d eqmod (a + c) (b + d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst c. (k1 + k2). ring.
Qed.

Lemma eqmod_neg:
   x y, eqmod x y eqmod (-x) (-y).
Proof.
  intros x y [k EQ]; red. (-k). rewrite EQ. ring.
Qed.

Lemma eqmod_sub:
   a b c d, eqmod a b eqmod c d eqmod (a - c) (b - d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst c. (k1 - k2). ring.
Qed.

Lemma eqmod_mult:
   a b c d, eqmod a c eqmod b d eqmod (a × b) (c × d).
Proof.
  intros a b c d [k1 EQ1] [k2 EQ2]; red.
  subst a; subst b.
   (k1 × k2 × modul + c × k2 + k1 × d).
  ring.
Qed.

End EQ_MODULO.

Lemma eqmod_divides:
   n m x y, eqmod n x y Zdivide m n eqmod m x y.
Proof.
  intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
   (k1×k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto.
Qed.

We then specialize these definitions to equality modulo 2wordsize.

Hint Resolve modulus_pos: ints.

Definition eqm := eqmod modulus.

Lemma eqm_refl: x, eqm x x.
Proof (eqmod_refl modulus).
Hint Resolve eqm_refl: ints.

Lemma eqm_refl2:
   x y, x = y eqm x y.
Proof (eqmod_refl2 modulus).
Hint Resolve eqm_refl2: ints.

Lemma eqm_sym: x y, eqm x y eqm y x.
Proof (eqmod_sym modulus).
Hint Resolve eqm_sym: ints.

Lemma eqm_trans: x y z, eqm x y eqm y z eqm x z.
Proof (eqmod_trans modulus).
Hint Resolve eqm_trans: ints.

Lemma eqm_small_eq:
   x y, eqm x y 0 x < modulus 0 y < modulus x = y.
Proof (eqmod_small_eq modulus).
Hint Resolve eqm_small_eq: ints.

Lemma eqm_add:
   a b c d, eqm a b eqm c d eqm (a + c) (b + d).
Proof (eqmod_add modulus).
Hint Resolve eqm_add: ints.

Lemma eqm_neg:
   x y, eqm x y eqm (-x) (-y).
Proof (eqmod_neg modulus).
Hint Resolve eqm_neg: ints.

Lemma eqm_sub:
   a b c d, eqm a b eqm c d eqm (a - c) (b - d).
Proof (eqmod_sub modulus).
Hint Resolve eqm_sub: ints.

Lemma eqm_mult:
   a b c d, eqm a c eqm b d eqm (a × b) (c × d).
Proof (eqmod_mult modulus).
Hint Resolve eqm_mult: ints.

Properties of the coercions between Z and int


Lemma eqm_samerepr: x y, eqm x y repr x = repr y.
Proof.
  intros. unfold repr. apply mkint_eq.
  rewrite !Z_mod_modulus_eq. apply eqmod_mod_eq. auto with ints. exact H.
Qed.

Lemma eqm_unsigned_repr:
   z, eqm z (unsigned (repr z)).
Proof.
  unfold eqm; intros. rewrite unsigned_repr_eq. apply eqmod_mod. auto with ints.
Qed.
Hint Resolve eqm_unsigned_repr: ints.

Lemma eqm_unsigned_repr_l:
   a b, eqm a b eqm (unsigned (repr a)) b.
Proof.
  intros. apply eqm_trans with a.
  apply eqm_sym. apply eqm_unsigned_repr. auto.
Qed.
Hint Resolve eqm_unsigned_repr_l: ints.

Lemma eqm_unsigned_repr_r:
   a b, eqm a b eqm a (unsigned (repr b)).
Proof.
  intros. apply eqm_trans with b. auto.
  apply eqm_unsigned_repr.
Qed.
Hint Resolve eqm_unsigned_repr_r: ints.

Lemma eqm_signed_unsigned:
   x, eqm (signed x) (unsigned x).
Proof.
  intros; red. unfold signed. set (y := unsigned x).
  case (zlt y half_modulus); intro.
  apply eqmod_refl. red; (-1); ring.
Qed.

Theorem unsigned_range:
   i, 0 unsigned i < modulus.
Proof.
  destruct i. simpl. omega.
Qed.
Hint Resolve unsigned_range: ints.

Theorem unsigned_range_2:
   i, 0 unsigned i max_unsigned.
Proof.
  intro; unfold max_unsigned.
  generalize (unsigned_range i). omega.
Qed.
Hint Resolve unsigned_range_2: ints.

Theorem signed_range:
   i, min_signed signed i max_signed.
Proof.
  intros. unfold signed.
  generalize (unsigned_range i). set (n := unsigned i). intros.
  case (zlt n half_modulus); intro.
  unfold max_signed. generalize min_signed_neg. omega.
  unfold min_signed, max_signed.
  rewrite half_modulus_modulus in ×. omega.
Qed.

Theorem repr_unsigned:
   i, repr (unsigned i) = i.
Proof.
  destruct i; simpl. unfold repr. apply mkint_eq.
  rewrite Z_mod_modulus_eq. apply Zmod_small; omega.
Qed.
Hint Resolve repr_unsigned: ints.

Lemma repr_signed:
   i, repr (signed i) = i.
Proof.
  intros. transitivity (repr (unsigned i)).
  apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints.
Qed.
Hint Resolve repr_signed: ints.

Opaque repr.

Lemma eqm_repr_eq: x y, eqm x (unsigned y) repr x = y.
Proof.
  intros. rewrite <- (repr_unsigned y). apply eqm_samerepr; auto.
Qed.

Theorem unsigned_repr:
   z, 0 z max_unsigned unsigned (repr z) = z.
Proof.
  intros. rewrite unsigned_repr_eq.
  apply Zmod_small. unfold max_unsigned in H. omega.
Qed.
Hint Resolve unsigned_repr: ints.

Theorem signed_repr:
   z, min_signed z max_signed signed (repr z) = z.
Proof.
  intros. unfold signed. destruct (zle 0 z).
  replace (unsigned (repr z)) with z.
  rewrite zlt_true. auto. unfold max_signed in H. omega.
  symmetry. apply unsigned_repr. generalize max_signed_unsigned. omega.
  pose (z' := z + modulus).
  replace (repr z) with (repr z').
  replace (unsigned (repr z')) with z'.
  rewrite zlt_false. unfold z'. omega.
  unfold z'. unfold min_signed in H.
  rewrite half_modulus_modulus. omega.
  symmetry. apply unsigned_repr.
  unfold z', max_unsigned. unfold min_signed, max_signed in H.
  rewrite half_modulus_modulus. omega.
  apply eqm_samerepr. unfold z'; red. 1. omega.
Qed.

Theorem signed_eq_unsigned:
   x, unsigned x max_signed signed x = unsigned x.
Proof.
  intros. unfold signed. destruct (zlt (unsigned x) half_modulus).
  auto. unfold max_signed in H. omegaContradiction.
Qed.

Theorem signed_positive:
   x, signed x 0 unsigned x max_signed.
Proof.
  intros. unfold signed, max_signed.
  generalize (unsigned_range x) half_modulus_modulus half_modulus_pos; intros.
  destruct (zlt (unsigned x) half_modulus); omega.
Qed.

Properties of zero, one, minus one


Theorem unsigned_zero: unsigned zero = 0.
Proof.
  unfold zero; rewrite unsigned_repr_eq. apply Zmod_0_l.
Qed.

Theorem unsigned_one: unsigned one = 1.
Proof.
  unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega.
  unfold modulus. replace wordsize with (S(pred wordsize)).
  rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)).
  omega.
  generalize wordsize_pos. unfold zwordsize. omega.
Qed.

Theorem unsigned_mone: unsigned mone = modulus - 1.
Proof.
  unfold mone; rewrite unsigned_repr_eq.
  replace (-1) with ((modulus - 1) + (-1) × modulus).
  rewrite Z_mod_plus_full. apply Zmod_small.
  generalize modulus_pos. omega. omega.
Qed.

Theorem signed_zero: signed zero = 0.
Proof.
  unfold signed. rewrite unsigned_zero. apply zlt_true. generalize half_modulus_pos; omega.
Qed.

Theorem signed_mone: signed mone = -1.
Proof.
  unfold signed. rewrite unsigned_mone.
  rewrite zlt_false. omega.
  rewrite half_modulus_modulus. generalize half_modulus_pos. omega.
Qed.

Theorem one_not_zero: one zero.
Proof.
  assert (unsigned one unsigned zero).
  rewrite unsigned_one; rewrite unsigned_zero; congruence.
  congruence.
Qed.

Theorem unsigned_repr_wordsize:
  unsigned iwordsize = zwordsize.
Proof.
  unfold iwordsize; rewrite unsigned_repr_eq. apply Zmod_small.
  generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
Qed.

Properties of equality


Theorem eq_sym:
   x y, eq x y = eq y x.
Proof.
  intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
  rewrite e. rewrite zeq_true. auto.
  rewrite zeq_false. auto. auto.
Qed.

Theorem eq_spec: (x y: int), if eq x y then x = y else x y.
Proof.
  intros; unfold eq. case (eq_dec x y); intro.
  subst y. rewrite zeq_true. auto.
  rewrite zeq_false. auto.
  destruct x; destruct y.
  simpl. red; intro. elim n. apply mkint_eq. auto.
Qed.

Theorem eq_true: x, eq x x = true.
Proof.
  intros. generalize (eq_spec x x); case (eq x x); intros; congruence.
Qed.

Theorem eq_false: x y, x y eq x y = false.
Proof.
  intros. generalize (eq_spec x y); case (eq x y); intros; congruence.
Qed.

Theorem eq_signed:
   x y, eq x y = if zeq (signed x) (signed y) then true else false.
Proof.
  intros. predSpec eq eq_spec x y.
  subst x. rewrite zeq_true; auto.
  destruct (zeq (signed x) (signed y)); auto.
  elim H. rewrite <- (repr_signed x). rewrite <- (repr_signed y). congruence.
Qed.

Properties of addition


Theorem add_unsigned: x y, add x y = repr (unsigned x + unsigned y).
Proof. intros; reflexivity.
Qed.

Theorem add_signed: x y, add x y = repr (signed x + signed y).
Proof.
  intros. rewrite add_unsigned. apply eqm_samerepr.
  apply eqm_add; apply eqm_sym; apply eqm_signed_unsigned.
Qed.

Theorem add_commut: x y, add x y = add y x.
Proof. intros; unfold add. decEq. omega. Qed.

Theorem add_zero: x, add x zero = x.
Proof.
  intros. unfold add. rewrite unsigned_zero.
  rewrite Zplus_0_r. apply repr_unsigned.
Qed.

Theorem add_zero_l: x, add zero x = x.
Proof.
  intros. rewrite add_commut. apply add_zero.
Qed.

Theorem add_assoc: x y z, add (add x y) z = add x (add y z).
Proof.
  intros; unfold add.
  set (x' := unsigned x).
  set (y' := unsigned y).
  set (z' := unsigned z).
  apply eqm_samerepr.
  apply eqm_trans with ((x' + y') + z').
  auto with ints.
  rewrite <- Zplus_assoc. auto with ints.
Qed.

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

Theorem add_neg_zero: x, add x (neg x) = zero.
Proof.
  intros; unfold add, neg, zero. apply eqm_samerepr.
  replace 0 with (unsigned x + (- (unsigned x))).
  auto with ints. omega.
Qed.

Theorem unsigned_add_carry:
   x y,
  unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) × modulus.
Proof.
  intros.
  unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r.
  rewrite unsigned_repr_eq.
  generalize (unsigned_range x) (unsigned_range y). intros.
  destruct (zlt (unsigned x + unsigned y) modulus).
  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
  rewrite unsigned_one. apply Zmod_unique with 1. omega. omega.
Qed.

Corollary unsigned_add_either:
   x y,
  unsigned (add x y) = unsigned x + unsigned y
   unsigned (add x y) = unsigned x + unsigned y - modulus.
Proof.
  intros. rewrite unsigned_add_carry. unfold add_carry.
  rewrite unsigned_zero. rewrite Zplus_0_r.
  destruct (zlt (unsigned x + unsigned y) modulus).
  rewrite unsigned_zero. left; omega.
  rewrite unsigned_one. right; omega.
Qed.

Properties of negation


Theorem neg_repr: z, neg (repr z) = repr (-z).
Proof.
  intros; unfold neg. apply eqm_samerepr. auto with ints.
Qed.

Theorem neg_zero: neg zero = zero.
Proof.
  unfold neg. rewrite unsigned_zero. auto.
Qed.

Theorem neg_involutive: x, neg (neg x) = x.
Proof.
  intros; unfold neg.
  apply eqm_repr_eq. eapply eqm_trans. apply eqm_neg.
  apply eqm_unsigned_repr_l. apply eqm_refl. apply eqm_refl2. omega.
Qed.

Theorem neg_add_distr: x y, neg(add x y) = add (neg x) (neg y).
Proof.
  intros; unfold neg, add. apply eqm_samerepr.
  apply eqm_trans with (- (unsigned x + unsigned y)).
  auto with ints.
  replace (- (unsigned x + unsigned y))
     with ((- unsigned x) + (- unsigned y)).
  auto with ints. omega.
Qed.

Properties of subtraction


Theorem sub_zero_l: x, sub x zero = x.
Proof.
  intros; unfold sub. rewrite unsigned_zero.
  replace (unsigned x - 0) with (unsigned x) by omega. apply repr_unsigned.
Qed.

Theorem sub_zero_r: x, sub zero x = neg x.
Proof.
  intros; unfold sub, neg. rewrite unsigned_zero. auto.
Qed.

Theorem sub_add_opp: x y, sub x y = add x (neg y).
Proof.
  intros; unfold sub, add, neg. apply eqm_samerepr.
  apply eqm_add; auto with ints.
Qed.

Theorem sub_idem: x, sub x x = zero.
Proof.
  intros; unfold sub. unfold zero. decEq. omega.
Qed.

Theorem sub_add_l: x y z, sub (add x y) z = add (sub x z) y.
Proof.
  intros. repeat rewrite sub_add_opp.
  repeat rewrite add_assoc. decEq. apply add_commut.
Qed.

Theorem sub_add_r: x y z, sub x (add y z) = add (sub x z) (neg y).
Proof.
  intros. repeat rewrite sub_add_opp.
  rewrite neg_add_distr. rewrite add_permut. apply add_commut.
Qed.

Theorem sub_shifted:
   x y z,
  sub (add x z) (add y z) = sub x y.
Proof.
  intros. rewrite sub_add_opp. rewrite neg_add_distr.
  rewrite add_assoc.
  rewrite (add_commut (neg y) (neg z)).
  rewrite <- (add_assoc z). rewrite add_neg_zero.
  rewrite (add_commut zero). rewrite add_zero.
  symmetry. apply sub_add_opp.
Qed.

Theorem sub_signed:
   x y, sub x y = repr (signed x - signed y).
Proof.
  intros. unfold sub. apply eqm_samerepr.
  apply eqm_sub; apply eqm_sym; apply eqm_signed_unsigned.
Qed.

Theorem unsigned_sub_borrow:
   x y,
  unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) × modulus.
Proof.
  intros.
  unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r.
  rewrite unsigned_repr_eq.
  generalize (unsigned_range x) (unsigned_range y). intros.
  destruct (zlt (unsigned x - unsigned y) 0).
  rewrite unsigned_one. apply Zmod_unique with (-1). omega. omega.
  rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
Qed.

Properties of multiplication


Theorem mul_commut: x y, mul x y = mul y x.
Proof.
  intros; unfold mul. decEq. ring.
Qed.

Theorem mul_zero: x, mul x zero = zero.
Proof.
  intros; unfold mul. rewrite unsigned_zero.
  unfold zero. decEq. ring.
Qed.

Theorem mul_one: x, mul x one = x.
Proof.
  intros; unfold mul. rewrite unsigned_one.
  transitivity (repr (unsigned x)). decEq. ring.
  apply repr_unsigned.
Qed.

Theorem mul_mone: x, mul x mone = neg x.
Proof.
  intros; unfold mul, neg. rewrite unsigned_mone.
  apply eqm_samerepr.
  replace (-unsigned x) with (0 - unsigned x) by omega.
  replace (unsigned x × (modulus - 1)) with (unsigned x × modulus - unsigned x) by ring.
  apply eqm_sub. (unsigned x). omega. apply eqm_refl.
Qed.

Theorem mul_assoc: x y z, mul (mul x y) z = mul x (mul y z).
Proof.
  intros; unfold mul.
  set (x' := unsigned x).
  set (y' := unsigned y).
  set (z' := unsigned z).
  apply eqm_samerepr. apply eqm_trans with ((x' × y') × z').
  auto with ints.
  rewrite <- Zmult_assoc. auto with ints.
Qed.

Theorem mul_add_distr_l:
   x y z, mul (add x y) z = add (mul x z) (mul y z).
Proof.
  intros; unfold mul, add.
  apply eqm_samerepr.
  set (x' := unsigned x).
  set (y' := unsigned y).
  set (z' := unsigned z).
  apply eqm_trans with ((x' + y') × z').
  auto with ints.
  replace ((x' + y') × z') with (x' × z' + y' × z').
  auto with ints.
  ring.
Qed.

Theorem mul_add_distr_r:
   x y z, mul x (add y z) = add (mul x y) (mul x z).
Proof.
  intros. rewrite mul_commut. rewrite mul_add_distr_l.
  decEq; apply mul_commut.
Qed.

Theorem neg_mul_distr_l:
   x y, neg(mul x y) = mul (neg x) y.
Proof.
  intros. unfold mul, neg.
  set (x' := unsigned x). set (y' := unsigned y).
  apply eqm_samerepr. apply eqm_trans with (- (x' × y')).
  auto with ints.
  replace (- (x' × y')) with ((-x') × y') by ring.
  auto with ints.
Qed.

Theorem neg_mul_distr_r:
    x y, neg(mul x y) = mul x (neg y).
Proof.
  intros. rewrite (mul_commut x y). rewrite (mul_commut x (neg y)).
  apply neg_mul_distr_l.
Qed.

Theorem mul_signed:
   x y, mul x y = repr (signed x × signed y).
Proof.
  intros; unfold mul. apply eqm_samerepr.
  apply eqm_mult; apply eqm_sym; apply eqm_signed_unsigned.
Qed.

Properties of division and modulus


Lemma modu_divu_Euclid:
   x y, y zero x = add (mul (divu x y) y) (modu x y).
Proof.
  intros. unfold add, mul, divu, modu.
  transitivity (repr (unsigned x)). auto with ints.
  apply eqm_samerepr.
  set (x' := unsigned x). set (y' := unsigned y).
  apply eqm_trans with ((x' / y') × y' + x' mod y').
  apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq.
  generalize (unsigned_range y); intro.
  assert (unsigned y 0). red; intro.
  elim H. rewrite <- (repr_unsigned y). unfold zero. congruence.
  unfold y'. omega.
  auto with ints.
Qed.

Theorem modu_divu:
   x y, y zero modu x y = sub x (mul (divu x y) y).
Proof.
  intros.
  assert ( a b c, a = add b c c = sub a b).
  intros. subst a. rewrite sub_add_l. rewrite sub_idem.
  rewrite add_commut. rewrite add_zero. auto.
  apply H0. apply modu_divu_Euclid. auto.
Qed.

Lemma mods_divs_Euclid:
   x y, x = add (mul (divs x y) y) (mods x y).
Proof.
  intros. unfold add, mul, divs, mods.
  transitivity (repr (signed x)). auto with ints.
  apply eqm_samerepr.
  set (x' := signed x). set (y' := signed y).
  apply eqm_trans with ((Z.quot x' y') × y' + Z.rem x' y').
  apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'.
  apply eqm_add; auto with ints.
  apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints.
  unfold y'. apply eqm_signed_unsigned.
Qed.

Theorem mods_divs:
   x y, mods x y = sub x (mul (divs x y) y).
Proof.
  intros.
  assert ( a b c, a = add b c c = sub a b).
  intros. subst a. rewrite sub_add_l. rewrite sub_idem.
  rewrite add_commut. rewrite add_zero. auto.
  apply H. apply mods_divs_Euclid.
Qed.

Theorem divu_one:
   x, divu x one = x.
Proof.
  unfold divu; intros. rewrite unsigned_one. rewrite Zdiv_1_r. apply repr_unsigned.
Qed.

Theorem modu_one:
   x, modu x one = zero.
Proof.
  intros. rewrite modu_divu. rewrite divu_one. rewrite mul_one. apply sub_idem.
  apply one_not_zero.
Qed.

Theorem divs_mone:
   x, divs x mone = neg x.
Proof.
  unfold divs, neg; intros.
  rewrite signed_mone.
  replace (Z.quot (signed x) (-1)) with (- (signed x)).
  apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned.
  set (x' := signed x).
  set (one := 1).
  change (-1) with (- one). rewrite Zquot_opp_r.
  assert (Z.quot x' one = x').
  symmetry. apply Zquot_unique_full with 0. red.
  change (Z.abs one) with 1.
  destruct (zle 0 x'). left. omega. right. omega.
  unfold one; ring.
  congruence.
Qed.

Theorem mods_mone:
   x, mods x mone = zero.
Proof.
  intros. rewrite mods_divs. rewrite divs_mone.
  rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem.
Qed.

Bit-level properties

Properties of bit-level operations over Z


Remark Ztestbit_0: n, Z.testbit 0 n = false.
Proof Z.testbit_0_l.

Remark Ztestbit_1: n, Z.testbit 1 n = zeq n 0.
Proof.
  intros. destruct n; simpl; auto.
Qed.

Remark Ztestbit_m1: n, 0 n Z.testbit (-1) n = true.
Proof.
  intros. destruct n; simpl; auto.
Qed.

Remark Zshiftin_spec:
   b x, Zshiftin b x = 2 × x + (if b then 1 else 0).
Proof.
  unfold Zshiftin; intros. destruct b.
  - rewrite Z.succ_double_spec. omega.
  - rewrite Z.double_spec. omega.
Qed.

Remark Zshiftin_inj:
   b1 x1 b2 x2,
  Zshiftin b1 x1 = Zshiftin b2 x2 b1 = b2 x1 = x2.
Proof.
  intros. rewrite !Zshiftin_spec in H.
  destruct b1; destruct b2.
  split; [auto|omega].
  omegaContradiction.
  omegaContradiction.
  split; [auto|omega].
Qed.

Remark Zdecomp:
   x, x = Zshiftin (Z.odd x) (Z.div2 x).
Proof.
  intros. destruct x; simpl.
  - auto.
  - destruct p; auto.
  - destruct p; auto. simpl. rewrite Pos.pred_double_succ. auto.
Qed.

Remark Ztestbit_shiftin:
   b x n,
  0 n
  Z.testbit (Zshiftin b x) n = if zeq n 0 then b else Z.testbit x (Z.pred n).
Proof.
  intros. rewrite Zshiftin_spec. destruct (zeq n 0).
  - subst n. destruct b.
    + apply Z.testbit_odd_0.
    + rewrite Zplus_0_r. apply Z.testbit_even_0.
  - assert (0 Z.pred n) by omega.
    set (n' := Z.pred n) in ×.
    replace n with (Z.succ n') by (unfold n'; omega).
    destruct b.
    + apply Z.testbit_odd_succ; auto.
    + rewrite Zplus_0_r. apply Z.testbit_even_succ; auto.
Qed.

Remark Ztestbit_shiftin_base:
   b x, Z.testbit (Zshiftin b x) 0 = b.
Proof.
  intros. rewrite Ztestbit_shiftin. apply zeq_true. omega.
Qed.

Remark Ztestbit_shiftin_succ:
   b x n, 0 n Z.testbit (Zshiftin b x) (Z.succ n) = Z.testbit x n.
Proof.
  intros. rewrite Ztestbit_shiftin. rewrite zeq_false. rewrite Z.pred_succ. auto.
  omega. omega.
Qed.

Remark Ztestbit_eq:
   n x, 0 n
  Z.testbit x n = if zeq n 0 then Z.odd x else Z.testbit (Z.div2 x) (Z.pred n).
Proof.
  intros. rewrite (Zdecomp x) at 1. apply Ztestbit_shiftin; auto.
Qed.

Remark Ztestbit_base:
   x, Z.testbit x 0 = Z.odd x.
Proof.
  intros. rewrite Ztestbit_eq. apply zeq_true. omega.
Qed.

Remark Ztestbit_succ:
   n x, 0 n Z.testbit x (Z.succ n) = Z.testbit (Z.div2 x) n.
Proof.
  intros. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ. auto.
  omega. omega.
Qed.

Lemma eqmod_same_bits:
   n x y,
  ( i, 0 i < Z.of_nat n Z.testbit x i = Z.testbit y i)
  eqmod (two_power_nat n) x y.
Proof.
  induction n; intros.
  - change (two_power_nat 0) with 1. (x-y); ring.
  - rewrite two_power_nat_S.
    assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)).
      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega.
      omega. omega.
  destruct H0 as [k EQ].
   k. rewrite (Zdecomp x). rewrite (Zdecomp y).
  replace (Z.odd y) with (Z.odd x).
  rewrite EQ. rewrite !Zshiftin_spec. ring.
  exploit (H 0). rewrite inj_S; omega.
  rewrite !Ztestbit_base. auto.
Qed.

Lemma eqm_same_bits:
   x y,
  ( i, 0 i < zwordsize Z.testbit x i = Z.testbit y i)
  eqm x y.
Proof (eqmod_same_bits wordsize).

Lemma same_bits_eqmod:
   n x y i,
  eqmod (two_power_nat n) x y 0 i < Z.of_nat n
  Z.testbit x i = Z.testbit y i.
Proof.
  induction n; intros.
  - simpl in H0. omegaContradiction.
  - rewrite inj_S in H0. rewrite two_power_nat_S in H.
    rewrite !(Ztestbit_eq i); intuition.
    destruct H as [k EQ].
    assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) =
                 Zshiftin (Z.odd y) (k × two_power_nat n + Z.div2 y)).
    {
      rewrite (Zdecomp x) in EQ. rewrite (Zdecomp y) in EQ.
      rewrite EQ. rewrite !Zshiftin_spec. ring.
    }
    exploit Zshiftin_inj; eauto. intros [A B].
    destruct (zeq i 0).
    + auto.
    + apply IHn. k; auto. omega.
Qed.

Lemma same_bits_eqm:
   x y i,
  eqm x y
  0 i < zwordsize
  Z.testbit x i = Z.testbit y i.
Proof (same_bits_eqmod wordsize).

Remark two_power_nat_infinity:
   x, 0 x n, x < two_power_nat n.
Proof.
  intros x0 POS0; pattern x0; apply natlike_ind; auto.
   O. compute; auto.
  intros. destruct H0 as [n LT]. (S n). rewrite two_power_nat_S.
  generalize (two_power_nat_pos n). omega.
Qed.

Lemma equal_same_bits:
   x y,
  ( i, 0 i Z.testbit x i = Z.testbit y i)
  x = y.
Proof.
  intros.
  set (z := if zlt x y then y - x else x - y).
  assert (0 z).
    unfold z; destruct (zlt x y); omega.
  exploit (two_power_nat_infinity z); auto. intros [n LT].
  assert (eqmod (two_power_nat n) x y).
    apply eqmod_same_bits. intros. apply H. tauto.
  assert (eqmod (two_power_nat n) z 0).
    unfold z. destruct (zlt x y).
    replace 0 with (y - y) by omega. apply eqmod_sub. apply eqmod_refl. auto.
    replace 0 with (x - x) by omega. apply eqmod_sub. apply eqmod_refl. apply eqmod_sym; auto.
  assert (z = 0).
    apply eqmod_small_eq with (two_power_nat n). auto. omega. generalize (two_power_nat_pos n); omega.
  unfold z in H3. destruct (zlt x y); omega.
Qed.

Lemma Z_one_complement:
   i, 0 i
   x, Z.testbit (-x-1) i = negb (Z.testbit x i).
Proof.
  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
  intros i IND POS x.
  rewrite (Zdecomp x). set (y := Z.div2 x).
  replace (- Zshiftin (Z.odd x) y - 1)
     with (Zshiftin (negb (Z.odd x)) (- y - 1)).
  rewrite !Ztestbit_shiftin; auto.
  destruct (zeq i 0). auto. apply IND. omega.
  rewrite !Zshiftin_spec. destruct (Z.odd x); simpl negb; ring.
Qed.

Lemma Ztestbit_above:
   n x i,
  0 x < two_power_nat n
  i Z.of_nat n
  Z.testbit x i = false.
Proof.
  induction n; intros.
  - change (two_power_nat 0) with 1 in H.
    replace x with 0 by omega.
    apply Z.testbit_0_l.
  - rewrite inj_S in H0. rewrite Ztestbit_eq. rewrite zeq_false.
    apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H.
    rewrite Zshiftin_spec in H. destruct (Z.odd x); omega.
    omega. omega. omega.
Qed.

Lemma Ztestbit_above_neg:
   n x i,
  -two_power_nat n x < 0
  i Z.of_nat n
  Z.testbit x i = true.
Proof.
  intros. set (y := -x-1).
  assert (Z.testbit y i = false).
    apply Ztestbit_above with n.
    unfold y; omega. auto.
  unfold y in H1. rewrite Z_one_complement in H1.
  change true with (negb false). rewrite <- H1. rewrite negb_involutive; auto.
  omega.
Qed.

Lemma Zsign_bit:
   n x,
  0 x < two_power_nat (S n)
  Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true.
Proof.
  induction n; intros.
  - change (two_power_nat 1) with 2 in H.
    assert (x = 0 x = 1) by omega.
    destruct H0; subst x; reflexivity.
  - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
    rewrite IHn. rewrite two_power_nat_S.
    destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec.
    rewrite zlt_true. auto. destruct (Z.odd x); omega.
    rewrite zlt_false. auto. destruct (Z.odd x); omega.
    rewrite (Zdecomp x) in H; rewrite Zshiftin_spec in H.
    rewrite two_power_nat_S in H. destruct (Z.odd x); omega.
    omega. omega.
Qed.

Lemma Zshiftin_ind:
   (P: Z Prop),
  P 0
  ( b x, 0 x P x P (Zshiftin b x))
   x, 0 x P x.
Proof.
  intros. destruct x.
  - auto.
  - induction p.
    + change (P (Zshiftin true (Z.pos p))). auto.
    + change (P (Zshiftin false (Z.pos p))). auto.
    + change (P (Zshiftin true 0)). apply H0. omega. auto.
  - compute in H1. intuition congruence.
Qed.

Lemma Zshiftin_pos_ind:
   (P: Z Prop),
  P 1
  ( b x, 0 < x P x P (Zshiftin b x))
   x, 0 < x P x.
Proof.
  intros. destruct x; simpl in H1; try discriminate.
  induction p.
    + change (P (Zshiftin true (Z.pos p))). auto.
    + change (P (Zshiftin false (Z.pos p))). auto.
    + auto.
Qed.

Lemma Ztestbit_le:
   x y,
  0 y
  ( i, 0 i Z.testbit x i = true Z.testbit y i = true)
  x y.
Proof.
  intros x y0 POS0; revert x; pattern y0; apply Zshiftin_ind; auto; intros.
  - replace x with 0. omega. apply equal_same_bits; intros.
    rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto.
    exploit H; eauto. rewrite Ztestbit_0. auto.
  - assert (Z.div2 x0 x).
    { apply H0. intros. exploit (H1 (Zsucc i)).
        omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
    }
    rewrite (Zdecomp x0). rewrite !Zshiftin_spec.
    destruct (Z.odd x0) as [] eqn:E1; destruct b as [] eqn:E2; try omega.
    exploit (H1 0). omega. rewrite Ztestbit_base; auto.
    rewrite Ztestbit_shiftin_base. congruence.
Qed.

Bit-level reasoning over type int


Definition testbit (x: int) (i: Z) : bool := Z.testbit (unsigned x) i.

Lemma testbit_repr:
   x i,
  0 i < zwordsize
  testbit (repr x) i = Z.testbit x i.
Proof.
  intros. unfold testbit. apply same_bits_eqm; auto with ints.
Qed.

Lemma same_bits_eq:
   x y,
  ( i, 0 i < zwordsize testbit x i = testbit y i)
  x = y.
Proof.
  intros. rewrite <- (repr_unsigned x). rewrite <- (repr_unsigned y).
  apply eqm_samerepr. apply eqm_same_bits. auto.
Qed.

Lemma bits_above:
   x i, i zwordsize testbit x i = false.
Proof.
  intros. apply Ztestbit_above with wordsize; auto. apply unsigned_range.
Qed.

Lemma bits_zero:
   i, testbit zero i = false.
Proof.
  intros. unfold testbit. rewrite unsigned_zero. apply Ztestbit_0.
Qed.

Remark bits_one: n, testbit one n = zeq n 0.
Proof.
  unfold testbit; intros. rewrite unsigned_one. apply Ztestbit_1.
Qed.

Lemma bits_mone:
   i, 0 i < zwordsize testbit mone i = true.
Proof.
  intros. unfold mone. rewrite testbit_repr; auto. apply Ztestbit_m1. omega.
Qed.

Hint Rewrite bits_zero bits_mone : ints.

Ltac bit_solve :=
  intros; apply same_bits_eq; intros; autorewrite with ints; auto with bool.

Lemma sign_bit_of_unsigned:
   x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true.
Proof.
  intros. unfold testbit.
  set (ws1 := pred wordsize).
  assert (zwordsize - 1 = Z_of_nat ws1).
    unfold zwordsize, ws1, wordsize.
    destruct WS.wordsize as [] eqn:E.
    elim WS.wordsize_not_zero; auto.
    rewrite inj_S. simpl. omega.
  assert (half_modulus = two_power_nat ws1).
    rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power.
  rewrite H; rewrite H0.
  apply Zsign_bit. rewrite two_power_nat_S. rewrite <- H0.
  rewrite <- half_modulus_modulus. apply unsigned_range.
Qed.

Lemma bits_signed:
   x i, 0 i
  Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1).
Proof.
  intros.
  destruct (zlt i zwordsize).
  - apply same_bits_eqm. apply eqm_signed_unsigned. omega.
  - unfold signed. rewrite sign_bit_of_unsigned. destruct (zlt (unsigned x) half_modulus).
    + apply Ztestbit_above with wordsize. apply unsigned_range. auto.
    + apply Ztestbit_above_neg with wordsize.
      fold modulus. generalize (unsigned_range x). omega. auto.
Qed.

Lemma bits_le:
   x y,
  ( i, 0 i < zwordsize testbit x i = true testbit y i = true)
  unsigned x unsigned y.
Proof.
  intros. apply Ztestbit_le. generalize (unsigned_range y); omega.
  intros. fold (testbit y i). destruct (zlt i zwordsize).
  apply H. omega. auto.
  fold (testbit x i) in H1. rewrite bits_above in H1; auto. congruence.
Qed.

Properties of bitwise and, or, xor


Lemma bits_and:
   x y i, 0 i < zwordsize
  testbit (and x y) i = testbit x i && testbit y i.
Proof.
  intros. unfold and. rewrite testbit_repr; auto. rewrite Z.land_spec; intuition.
Qed.

Lemma bits_or:
   x y i, 0 i < zwordsize
  testbit (or x y) i = testbit x i || testbit y i.
Proof.
  intros. unfold or. rewrite testbit_repr; auto. rewrite Z.lor_spec; intuition.
Qed.

Lemma bits_xor:
   x y i, 0 i < zwordsize
  testbit (xor x y) i = xorb (testbit x i) (testbit y i).
Proof.
  intros. unfold xor. rewrite testbit_repr; auto. rewrite Z.lxor_spec; intuition.
Qed.

Lemma bits_not:
   x i, 0 i < zwordsize
  testbit (not x) i = negb (testbit x i).
Proof.
  intros. unfold not. rewrite bits_xor; auto. rewrite bits_mone; auto.
Qed.

Hint Rewrite bits_and bits_or bits_xor bits_not: ints.

Theorem and_commut: x y, and x y = and y x.
Proof.
  bit_solve.
Qed.

Theorem and_assoc: x y z, and (and x y) z = and x (and y z).
Proof.
  bit_solve.
Qed.

Theorem and_zero: x, and x zero = zero.
Proof.
  bit_solve. apply andb_b_false.
Qed.

Corollary and_zero_l: x, and zero x = zero.
Proof.
  intros. rewrite and_commut. apply and_zero.
Qed.

Theorem and_mone: x, and x mone = x.
Proof.
  bit_solve. apply andb_b_true.
Qed.

Corollary and_mone_l: x, and mone x = x.
Proof.
  intros. rewrite and_commut. apply and_mone.
Qed.

Theorem and_idem: x, and x x = x.
Proof.
  bit_solve. destruct (testbit x i); auto.
Qed.

Theorem or_commut: x y, or x y = or y x.
Proof.
  bit_solve.
Qed.

Theorem or_assoc: x y z, or (or x y) z = or x (or y z).
Proof.
  bit_solve.
Qed.

Theorem or_zero: x, or x zero = x.
Proof.
  bit_solve.
Qed.

Corollary or_zero_l: x, or zero x = x.
Proof.
  intros. rewrite or_commut. apply or_zero.
Qed.

Theorem or_mone: x, or x mone = mone.
Proof.
  bit_solve.
Qed.

Theorem or_idem: x, or x x = x.
Proof.
  bit_solve. destruct (testbit x i); auto.
Qed.

Theorem and_or_distrib:
   x y z,
  and x (or y z) = or (and x y) (and x z).
Proof.
  bit_solve. apply demorgan1.
Qed.

Corollary and_or_distrib_l:
   x y z,
  and (or x y) z = or (and x z) (and y z).
Proof.
  intros. rewrite (and_commut (or x y)). rewrite and_or_distrib. f_equal; apply and_commut.
Qed.

Theorem or_and_distrib:
   x y z,
  or x (and y z) = and (or x y) (or x z).
Proof.
  bit_solve. apply orb_andb_distrib_r.
Qed.

Corollary or_and_distrib_l:
   x y z,
  or (and x y) z = and (or x z) (or y z).
Proof.
  intros. rewrite (or_commut (and x y)). rewrite or_and_distrib. f_equal; apply or_commut.
Qed.

Theorem and_or_absorb: x y, and x (or x y) = x.
Proof.
  bit_solve.
  assert ( a b, a && (a || b) = a) by destr_bool.
  auto.
Qed.

Theorem or_and_absorb: x y, or x (and x y) = x.
Proof.
  bit_solve.
  assert ( a b, a || (a && b) = a) by destr_bool.
  auto.
Qed.

Theorem xor_commut: x y, xor x y = xor y x.
Proof.
  bit_solve. apply xorb_comm.
Qed.

Theorem xor_assoc: x y z, xor (xor x y) z = xor x (xor y z).
Proof.
  bit_solve. apply xorb_assoc.
Qed.

Theorem xor_zero: x, xor x zero = x.
Proof.
  bit_solve. apply xorb_false.
Qed.

Corollary xor_zero_l: x, xor zero x = x.
Proof.
  intros. rewrite xor_commut. apply xor_zero.
Qed.

Theorem xor_idem: x, xor x x = zero.
Proof.
  bit_solve. apply xorb_nilpotent.
Qed.

Theorem xor_zero_one: xor zero one = one.
Proof. rewrite xor_commut. apply xor_zero. Qed.

Theorem xor_one_one: xor one one = zero.
Proof. apply xor_idem. Qed.

Theorem xor_zero_equal: x y, xor x y = zero x = y.
Proof.
  intros. apply same_bits_eq; intros.
  assert (xorb (testbit x i) (testbit y i) = false).
    rewrite <- bits_xor; auto. rewrite H. apply bits_zero.
  destruct (testbit x i); destruct (testbit y i); reflexivity || discriminate.
Qed.

Theorem and_xor_distrib:
   x y z,
  and x (xor y z) = xor (and x y) (and x z).
Proof.
  bit_solve.
  assert ( a b c, a && (xorb b c) = xorb (a && b) (a && c)) by destr_bool.
  auto.
Qed.

Theorem and_le:
   x y, unsigned (and x y) unsigned x.
Proof.
  intros. apply bits_le; intros.
  rewrite bits_and in H0; auto. rewrite andb_true_iff in H0. tauto.
Qed.

Theorem or_le:
   x y, unsigned x unsigned (or x y).
Proof.
  intros. apply bits_le; intros.
  rewrite bits_or; auto. rewrite H0; auto.
Qed.

Properties of bitwise complement.

Theorem not_involutive:
   (x: int), not (not x) = x.
Proof.
  intros. unfold not. rewrite xor_assoc. rewrite xor_idem. apply xor_zero.
Qed.

Theorem not_zero:
  not zero = mone.
Proof.
  unfold not. rewrite xor_commut. apply xor_zero.
Qed.

Theorem not_mone:
  not mone = zero.
Proof.
  rewrite <- (not_involutive zero). symmetry. decEq. apply not_zero.
Qed.

Theorem not_or_and_not:
   x y, not (or x y) = and (not x) (not y).
Proof.
  bit_solve. apply negb_orb.
Qed.

Theorem not_and_or_not:
   x y, not (and x y) = or (not x) (not y).
Proof.
  bit_solve. apply negb_andb.
Qed.

Theorem and_not_self:
   x, and x (not x) = zero.
Proof.
  bit_solve.
Qed.

Theorem or_not_self:
   x, or x (not x) = mone.
Proof.
  bit_solve.
Qed.

Theorem xor_not_self:
   x, xor x (not x) = mone.
Proof.
  bit_solve. destruct (testbit x i); auto.
Qed.

Lemma unsigned_not:
   x, unsigned (not x) = max_unsigned - unsigned x.
Proof.
  intros. transitivity (unsigned (repr(-unsigned x - 1))).
  f_equal. bit_solve. rewrite testbit_repr; auto. symmetry. apply Z_one_complement. omega.
  rewrite unsigned_repr_eq. apply Zmod_unique with (-1).
  unfold max_unsigned. omega.
  generalize (unsigned_range x). unfold max_unsigned. omega.
Qed.

Theorem not_neg:
   x, not x = add (neg x) mone.
Proof.
  bit_solve.
  rewrite <- (repr_unsigned x) at 1. unfold add.
  rewrite !testbit_repr; auto.
  transitivity (Z.testbit (-unsigned x - 1) i).
  symmetry. apply Z_one_complement. omega.
  apply same_bits_eqm; auto.
  replace (-unsigned x - 1) with (-unsigned x + (-1)) by omega.
  apply eqm_add.
  unfold neg. apply eqm_unsigned_repr.
  rewrite unsigned_mone. (-1). ring.
Qed.

Theorem neg_not:
   x, neg x = add (not x) one.
Proof.
  intros. rewrite not_neg. rewrite add_assoc.
  replace (add mone one) with zero. rewrite add_zero. auto.
  apply eqm_samerepr. rewrite unsigned_mone. rewrite unsigned_one.
   (-1). ring.
Qed.

Theorem sub_add_not:
   x y, sub x y = add (add x (not y)) one.
Proof.
  intros. rewrite sub_add_opp. rewrite neg_not.
  rewrite ! add_assoc. auto.
Qed.

Theorem sub_add_not_3:
   x y b,
  b = zero b = one
  sub (sub x y) b = add (add x (not y)) (xor b one).
Proof.
  intros. rewrite ! sub_add_not. rewrite ! add_assoc. f_equal. f_equal.
  rewrite <- neg_not. rewrite <- sub_add_opp. destruct H; subst b.
  rewrite xor_zero_l. rewrite sub_zero_l. auto.
  rewrite xor_idem. rewrite sub_idem. auto.
Qed.

Theorem sub_borrow_add_carry:
   x y b,
  b = zero b = one
  sub_borrow x y b = xor (add_carry x (not y) (xor b one)) one.
Proof.
  intros. unfold sub_borrow, add_carry. rewrite unsigned_not.
  replace (unsigned (xor b one)) with (1 - unsigned b).
  destruct (zlt (unsigned x - unsigned y - unsigned b)).
  rewrite zlt_true. rewrite xor_zero_l; auto.
  unfold max_unsigned; omega.
  rewrite zlt_false. rewrite xor_idem; auto.
  unfold max_unsigned; omega.
  destruct H; subst b.
  rewrite xor_zero_l. rewrite unsigned_one, unsigned_zero; auto.
  rewrite xor_idem. rewrite unsigned_one, unsigned_zero; auto.
Qed.

Connections between add and bitwise logical operations.

Lemma Z_add_is_or:
   i, 0 i
   x y,
  ( j, 0 j i Z.testbit x j && Z.testbit y j = false)
  Z.testbit (x + y) i = Z.testbit x i || Z.testbit y i.
Proof.
  intros i0 POS0. pattern i0. apply Zlt_0_ind; auto.
  intros i IND POS x y EXCL.
  rewrite (Zdecomp x) in ×. rewrite (Zdecomp y) in ×.
  transitivity (Z.testbit (Zshiftin (Z.odd x || Z.odd y) (Z.div2 x + Z.div2 y)) i).
  - f_equal. rewrite !Zshiftin_spec.
    exploit (EXCL 0). omega. rewrite !Ztestbit_shiftin_base. intros.
Opaque Z.mul.
    destruct (Z.odd x); destruct (Z.odd y); simpl in *; discriminate || ring.
  - rewrite !Ztestbit_shiftin; auto.
    destruct (zeq i 0).
    + auto.
    + apply IND. omega. intros.
      exploit (EXCL (Z.succ j)). omega.
      rewrite !Ztestbit_shiftin_succ. auto.
      omega. omega.
Qed.

Theorem add_is_or:
   x y,
  and x y = zero
  add x y = or x y.
Proof.
  bit_solve. unfold add. rewrite testbit_repr; auto.
  apply Z_add_is_or. omega.
  intros.
  assert (testbit (and x y) j = testbit zero j) by congruence.
  autorewrite with ints in H2. assumption. omega.
Qed.

Theorem xor_is_or:
   x y, and x y = zero xor x y = or x y.
Proof.
  bit_solve.
  assert (testbit (and x y) i = testbit zero i) by congruence.
  autorewrite with ints in H1; auto.
  destruct (testbit x i); destruct (testbit y i); simpl in *; congruence.
Qed.

Theorem add_is_xor:
   x y,
  and x y = zero
  add x y = xor x y.
Proof.
  intros. rewrite xor_is_or; auto. apply add_is_or; auto.
Qed.

Theorem add_and:
   x y z,
  and y z = zero
  add (and x y) (and x z) = and x (or y z).
Proof.
  intros. rewrite add_is_or.
  rewrite and_or_distrib; auto.
  rewrite (and_commut x y).
  rewrite and_assoc.
  repeat rewrite <- (and_assoc x).
  rewrite (and_commut (and x x)).
  rewrite <- and_assoc.
  rewrite H. rewrite and_commut. apply and_zero.
Qed.

Properties of shifts


Lemma bits_shl:
   x y i,
  0 i < zwordsize
  testbit (shl x y) i =
  if zlt i (unsigned y) then false else testbit x (i - unsigned y).
Proof.
  intros. unfold shl. rewrite testbit_repr; auto.
  destruct (zlt i (unsigned y)).
  apply Z.shiftl_spec_low. auto.
  apply Z.shiftl_spec_high. omega. omega.
Qed.

Lemma bits_shru:
   x y i,
  0 i < zwordsize
  testbit (shru x y) i =
  if zlt (i + unsigned y) zwordsize then testbit x (i + unsigned y) else false.
Proof.
  intros. unfold shru. rewrite testbit_repr; auto.
  rewrite Z.shiftr_spec. fold (testbit x (i + unsigned y)).
  destruct (zlt (i + unsigned y) zwordsize).
  auto.
  apply bits_above; auto.
  omega.
Qed.

Lemma bits_shr:
   x y i,
  0 i < zwordsize
  testbit (shr x y) i =
  testbit x (if zlt (i + unsigned y) zwordsize then i + unsigned y else zwordsize - 1).
Proof.
  intros. unfold shr. rewrite testbit_repr; auto.
  rewrite Z.shiftr_spec. apply bits_signed.
  generalize (unsigned_range y); omega.
  omega.
Qed.

Hint Rewrite bits_shl bits_shru bits_shr: ints.

Theorem shl_zero: x, shl x zero = x.
Proof.
  bit_solve. rewrite unsigned_zero. rewrite zlt_false. f_equal; omega. omega.
Qed.

Lemma bitwise_binop_shl:
   f f' x y n,
  ( x y i, 0 i < zwordsize testbit (f x y) i = f' (testbit x i) (testbit y i))
  f' false false = false
  f (shl x n) (shl y n) = shl (f x y) n.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite H; auto. rewrite !bits_shl; auto.
  destruct (zlt i (unsigned n)); auto.
  rewrite H; auto. generalize (unsigned_range n); omega.
Qed.

Theorem and_shl:
   x y n,
  and (shl x n) (shl y n) = shl (and x y) n.
Proof.
  intros. apply bitwise_binop_shl with andb. exact bits_and. auto.
Qed.

Theorem or_shl:
   x y n,
  or (shl x n) (shl y n) = shl (or x y) n.
Proof.
  intros. apply bitwise_binop_shl with orb. exact bits_or. auto.
Qed.

Theorem xor_shl:
   x y n,
  xor (shl x n) (shl y n) = shl (xor x y) n.
Proof.
  intros. apply bitwise_binop_shl with xorb. exact bits_xor. auto.
Qed.

Lemma ltu_inv:
   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.

Lemma ltu_iwordsize_inv:
   x, ltu x iwordsize = true 0 unsigned x < zwordsize.
Proof.
  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. auto.
Qed.

Theorem shl_shl:
   x y z,
  ltu y iwordsize = true
  ltu z iwordsize = true
  ltu (add y z) iwordsize = true
  shl (shl x y) z = shl x (add y z).
Proof.
  intros.
  generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
  assert (unsigned (add y z) = unsigned y + unsigned z).
    unfold add. apply unsigned_repr.
    generalize two_wordsize_max_unsigned; omega.
  apply same_bits_eq; intros.
  rewrite bits_shl; auto.
  destruct (zlt i (unsigned z)).
  - rewrite bits_shl; auto. rewrite zlt_true. auto. omega.
  - rewrite bits_shl. destruct (zlt (i - unsigned z) (unsigned y)).
    + rewrite bits_shl; auto. rewrite zlt_true. auto. omega.
    + rewrite bits_shl; auto. rewrite zlt_false. f_equal. omega. omega.
    + omega.
Qed.

Theorem shru_zero: x, shru x zero = x.
Proof.
  bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega.
Qed.

Lemma bitwise_binop_shru:
   f f' x y n,
  ( x y i, 0 i < zwordsize testbit (f x y) i = f' (testbit x i) (testbit y i))
  f' false false = false
  f (shru x n) (shru y n) = shru (f x y) n.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite H; auto. rewrite !bits_shru; auto.
  destruct (zlt (i + unsigned n) zwordsize); auto.
  rewrite H; auto. generalize (unsigned_range n); omega.
Qed.

Theorem and_shru:
   x y n,
  and (shru x n) (shru y n) = shru (and x y) n.
Proof.
  intros. apply bitwise_binop_shru with andb; auto. exact bits_and.
Qed.

Theorem or_shru:
   x y n,
  or (shru x n) (shru y n) = shru (or x y) n.
Proof.
  intros. apply bitwise_binop_shru with orb; auto. exact bits_or.
Qed.

Theorem xor_shru:
   x y n,
  xor (shru x n) (shru y n) = shru (xor x y) n.
Proof.
  intros. apply bitwise_binop_shru with xorb; auto. exact bits_xor.
Qed.

Theorem shru_shru:
   x y z,
  ltu y iwordsize = true
  ltu z iwordsize = true
  ltu (add y z) iwordsize = true
  shru (shru x y) z = shru x (add y z).
Proof.
  intros.
  generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
  assert (unsigned (add y z) = unsigned y + unsigned z).
    unfold add. apply unsigned_repr.
    generalize two_wordsize_max_unsigned; omega.
  apply same_bits_eq; intros.
  rewrite bits_shru; auto.
  destruct (zlt (i + unsigned z) zwordsize).
  - rewrite bits_shru. destruct (zlt (i + unsigned z + unsigned y) zwordsize).
    + rewrite bits_shru; auto. rewrite zlt_true. f_equal. omega. omega.
    + rewrite bits_shru; auto. rewrite zlt_false. auto. omega.
    + omega.
  - rewrite bits_shru; auto. rewrite zlt_false. auto. omega.
Qed.

Theorem shr_zero: x, shr x zero = x.
Proof.
  bit_solve. rewrite unsigned_zero. rewrite zlt_true. f_equal; omega. omega.
Qed.

Lemma bitwise_binop_shr:
   f f' x y n,
  ( x y i, 0 i < zwordsize testbit (f x y) i = f' (testbit x i) (testbit y i))
  f (shr x n) (shr y n) = shr (f x y) n.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite H; auto. rewrite !bits_shr; auto.
  rewrite H; auto.
  destruct (zlt (i + unsigned n) zwordsize).
  generalize (unsigned_range n); omega.
  omega.
Qed.

Theorem and_shr:
   x y n,
  and (shr x n) (shr y n) = shr (and x y) n.
Proof.
  intros. apply bitwise_binop_shr with andb. exact bits_and.
Qed.

Theorem or_shr:
   x y n,
  or (shr x n) (shr y n) = shr (or x y) n.
Proof.
  intros. apply bitwise_binop_shr with orb. exact bits_or.
Qed.

Theorem xor_shr:
   x y n,
  xor (shr x n) (shr y n) = shr (xor x y) n.
Proof.
  intros. apply bitwise_binop_shr with xorb. exact bits_xor.
Qed.

Theorem shr_shr:
   x y z,
  ltu y iwordsize = true
  ltu z iwordsize = true
  ltu (add y z) iwordsize = true
  shr (shr x y) z = shr x (add y z).
Proof.
  intros.
  generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
  assert (unsigned (add y z) = unsigned y + unsigned z).
    unfold add. apply unsigned_repr.
    generalize two_wordsize_max_unsigned; omega.
  apply same_bits_eq; intros.
  rewrite !bits_shr; auto. f_equal.
  destruct (zlt (i + unsigned z) zwordsize).
  rewrite H4. replace (i + (unsigned y + unsigned z)) with (i + unsigned z + unsigned y) by omega. auto.
  rewrite (zlt_false _ (i + unsigned (add y z))).
  destruct (zlt (zwordsize - 1 + unsigned y) zwordsize); omega.
  omega.
  destruct (zlt (i + unsigned z) zwordsize); omega.
Qed.

Theorem and_shr_shru:
   x y z,
  and (shr x z) (shru y z) = shru (and x y) z.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite bits_and; auto. rewrite bits_shr; auto. rewrite !bits_shru; auto.
  destruct (zlt (i + unsigned z) zwordsize).
  - rewrite bits_and; auto. generalize (unsigned_range z); omega.
  - apply andb_false_r.
Qed.

Theorem shr_and_shru_and:
   x y z,
  shru (shl z y) y = z
  and (shr x y) z = and (shru x y) z.
Proof.
  intros.
  rewrite <- H.
  rewrite and_shru. rewrite and_shr_shru. auto.
Qed.

Theorem shru_lt_zero:
   x,
  shru x (repr (zwordsize - 1)) = if lt x zero then one else zero.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite bits_shru; auto.
  rewrite unsigned_repr.
  destruct (zeq i 0).
  subst i. rewrite Zplus_0_l. rewrite zlt_true.
  rewrite sign_bit_of_unsigned.
  unfold lt. rewrite signed_zero. unfold signed.
  destruct (zlt (unsigned x) half_modulus).
  rewrite zlt_false. auto. generalize (unsigned_range x); omega.
  rewrite zlt_true. unfold one; rewrite testbit_repr; auto.
  generalize (unsigned_range x); omega.
  omega.
  rewrite zlt_false.
  unfold testbit. rewrite Ztestbit_eq. rewrite zeq_false.
  destruct (lt x zero).
  rewrite unsigned_one. simpl Z.div2. rewrite Z.testbit_0_l; auto.
  rewrite unsigned_zero. simpl Z.div2. rewrite Z.testbit_0_l; auto.
  auto. omega. omega.
  generalize wordsize_max_unsigned; omega.
Qed.

Theorem shr_lt_zero:
   x,
  shr x (repr (zwordsize - 1)) = if lt x zero then mone else zero.
Proof.
  intros. apply same_bits_eq; intros.
  rewrite bits_shr; auto.
  rewrite unsigned_repr.
  transitivity (testbit x (zwordsize - 1)).
  f_equal. destruct (zlt (i + (zwordsize - 1)) zwordsize); omega.
  rewrite sign_bit_of_unsigned.
  unfold lt. rewrite signed_zero. unfold signed.
  destruct (zlt (unsigned x) half_modulus).
  rewrite zlt_false. rewrite bits_zero; auto. generalize (unsigned_range x); omega.
  rewrite zlt_true. rewrite bits_mone; auto. generalize (unsigned_range x); omega.
  generalize wordsize_max_unsigned; omega.
Qed.

Properties of rotations


Lemma bits_rol:
   x y i,
  0 i < zwordsize
  testbit (rol x y) i = testbit x ((i - unsigned y) mod zwordsize).
Proof.
  intros. unfold rol.
  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos.
  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize).
  intros EQ.
  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos.
  fold j. intros RANGE.
  rewrite testbit_repr; auto.
  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega.
  destruct (zlt i j).
  - rewrite Z.shiftl_spec_low; auto. simpl.
    unfold testbit. f_equal.
    symmetry. apply Zmod_unique with (-k - 1).
    rewrite EQ. ring.
    omega.
  - rewrite Z.shiftl_spec_high.
    fold (testbit x (i + (zwordsize - j))).
    rewrite bits_above. rewrite orb_false_r.
    fold (testbit x (i - j)).
    f_equal. symmetry. apply Zmod_unique with (-k).
    rewrite EQ. ring.
    omega. omega. omega. omega.
Qed.

Lemma bits_ror:
   x y i,
  0 i < zwordsize
  testbit (ror x y) i = testbit x ((i + unsigned y) mod zwordsize).
Proof.
  intros. unfold ror.
  exploit (Z_div_mod_eq (unsigned y) zwordsize). apply wordsize_pos.
  set (j := unsigned y mod zwordsize). set (k := unsigned y / zwordsize).
  intros EQ.
  exploit (Z_mod_lt (unsigned y) zwordsize). apply wordsize_pos.
  fold j. intros RANGE.
  rewrite testbit_repr; auto.
  rewrite Z.lor_spec. rewrite Z.shiftr_spec. 2: omega.
  destruct (zlt (i + j) zwordsize).
  - rewrite Z.shiftl_spec_low; auto. rewrite orb_false_r.
    unfold testbit. f_equal.
    symmetry. apply Zmod_unique with k.
    rewrite EQ. ring.
    omega. omega.
  - rewrite Z.shiftl_spec_high.
    fold (testbit x (i + j)).
    rewrite bits_above. simpl.
    unfold testbit. f_equal.
    symmetry. apply Zmod_unique with (k + 1).
    rewrite EQ. ring.
    omega. omega. omega. omega.
Qed.

Hint Rewrite bits_rol bits_ror: ints.

Theorem shl_rolm:
   x n,
  ltu n iwordsize = true
  shl x n = rolm x n (shl mone n).
Proof.
  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
  unfold rolm. apply same_bits_eq; intros.
  rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto.
  destruct (zlt i (unsigned n)).
  - rewrite andb_false_r; auto.
  - generalize (unsigned_range n); intros.
    rewrite bits_mone. rewrite andb_true_r. f_equal.
    symmetry. apply Zmod_small. omega.
    omega.
Qed.

Theorem shru_rolm:
   x n,
  ltu n iwordsize = true
  shru x n = rolm x (sub iwordsize n) (shru mone n).
Proof.
  intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
  unfold rolm. apply same_bits_eq; intros.
  rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto.
  destruct (zlt (i + unsigned n) zwordsize).
  - generalize (unsigned_range n); intros.
    rewrite bits_mone. rewrite andb_true_r. f_equal.
    unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize.
    symmetry. apply Zmod_unique with (-1). ring. omega.
    rewrite unsigned_repr_wordsize. generalize wordsize_max_unsigned. omega.
    omega.
  - rewrite andb_false_r; auto.
Qed.

Theorem rol_zero:
   x,
  rol x zero = x.
Proof.
  bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r.
  apply Zmod_small; auto.
Qed.

Lemma bitwise_binop_rol:
   f f' x y n,
  ( x y i, 0 i < zwordsize testbit (f x y) i = f' (testbit x i) (testbit y i))
  rol (f x y) n = f (rol x n) (rol y n).
Proof.
  intros. apply same_bits_eq; intros.
  rewrite H; auto. rewrite !bits_rol; auto. rewrite H; auto.
  apply Z_mod_lt. apply wordsize_pos.
Qed.

Theorem rol_and:
   x y n,
  rol (and x y) n = and (rol x n) (rol y n).
Proof.
  intros. apply bitwise_binop_rol with andb. exact bits_and.
Qed.

Theorem rol_or:
   x y n,
  rol (or x y) n = or (rol x n) (rol y n).
Proof.
  intros. apply bitwise_binop_rol with orb. exact bits_or.
Qed.

Theorem rol_xor:
   x y n,
  rol (xor x y) n = xor (rol x n) (rol y n).
Proof.
  intros. apply bitwise_binop_rol with xorb. exact bits_xor.
Qed.

Theorem rol_rol:
   x n m,
  Zdivide zwordsize modulus
  rol (rol x n) m = rol x (modu (add n m) iwordsize).
Proof.
  bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos.
  set (M := unsigned m); set (N := unsigned n).
  apply eqmod_trans with (i - M - N).
  apply eqmod_sub.
  apply eqmod_sym. apply eqmod_mod. apply wordsize_pos.
  apply eqmod_refl.
  replace (i - M - N) with (i - (M + N)) by omega.
  apply eqmod_sub.
  apply eqmod_refl.
  apply eqmod_trans with (Zmod (unsigned n + unsigned m) zwordsize).
  replace (M + N) with (N + M) by omega. apply eqmod_mod. apply wordsize_pos.
  unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize.
  assert ( a, eqmod zwordsize a (unsigned (repr a))).
    intros. eapply eqmod_divides. apply eqm_unsigned_repr. assumption.
  eapply eqmod_trans. 2: apply H1.
  apply eqmod_refl2. apply eqmod_mod_eq. apply wordsize_pos. auto.
  apply Z_mod_lt. apply wordsize_pos.
Qed.

Theorem rolm_zero:
   x m,
  rolm x zero m = and x m.
Proof.
  intros. unfold rolm. rewrite rol_zero. auto.
Qed.

Theorem rolm_rolm:
   x n1 m1 n2 m2,
  Zdivide zwordsize modulus
  rolm (rolm x n1 m1) n2 m2 =
    rolm x (modu (add n1 n2) iwordsize)
           (and (rol m1 n2) m2).
Proof.
  intros.
  unfold rolm. rewrite rol_and. rewrite and_assoc.
  rewrite rol_rol. reflexivity. auto.
Qed.

Theorem or_rolm:
   x n m1 m2,
  or (rolm x n m1) (rolm x n m2) = rolm x n (or m1 m2).
Proof.
  intros; unfold rolm. symmetry. apply and_or_distrib.
Qed.

Theorem ror_rol:
   x y,
  ltu y iwordsize = true
  ror x y = rol x (sub iwordsize y).
Proof.
  intros.
  generalize (ltu_iwordsize_inv _ H); intros.
  apply same_bits_eq; intros.
  rewrite bits_ror; auto. rewrite bits_rol; auto. f_equal.
  unfold sub. rewrite unsigned_repr. rewrite unsigned_repr_wordsize.
  apply eqmod_mod_eq. apply wordsize_pos. 1. ring.
  rewrite unsigned_repr_wordsize.
  generalize wordsize_pos; generalize wordsize_max_unsigned; omega.
Qed.

Theorem ror_rol_neg:
   x y, (zwordsize | modulus) ror x y = rol x (neg y).
Proof.
  intros. apply same_bits_eq; intros.
  rewrite bits_ror by auto. rewrite bits_rol by auto.
  f_equal. apply eqmod_mod_eq. omega.
  apply eqmod_trans with (i - (- unsigned y)).
  apply eqmod_refl2; omega.
  apply eqmod_sub. apply eqmod_refl.
  apply eqmod_divides with modulus.
  apply eqm_unsigned_repr. auto.
Qed.

Theorem or_ror:
   x y z,
  ltu y iwordsize = true
  ltu z iwordsize = true
  add y z = iwordsize
  ror x z = or (shl x y) (shru x z).
Proof.
  intros.
  generalize (ltu_iwordsize_inv _ H) (ltu_iwordsize_inv _ H0); intros.
  unfold ror, or, shl, shru. apply same_bits_eq; intros.
  rewrite !testbit_repr; auto.
  rewrite !Z.lor_spec. rewrite orb_comm. f_equal; apply same_bits_eqm; auto.
  - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal.
    rewrite Zmod_small; auto.
    assert (unsigned (add y z) = zwordsize).
      rewrite H1. apply unsigned_repr_wordsize.
    unfold add in H5. rewrite unsigned_repr in H5.
    omega.
    generalize two_wordsize_max_unsigned; omega.
  - apply eqm_unsigned_repr_r. apply eqm_refl2. f_equal.
    apply Zmod_small; auto.
Qed.

Properties of Z_one_bits and is_power2.


Fixpoint powerserie (l: list Z): Z :=
  match l with
  | nil ⇒ 0
  | x :: xstwo_p x + powerserie xs
  end.

Lemma Z_one_bits_powerserie:
   x, 0 x < modulus x = powerserie (Z_one_bits wordsize x 0).
Proof.
  assert ( n x i,
    0 i
    0 x < two_power_nat n
    x × two_p i = powerserie (Z_one_bits n x i)).
  {
  induction n; intros.
  simpl. rewrite two_power_nat_O in H0.
  assert (x = 0) by omega. subst x. omega.
  rewrite two_power_nat_S in H0. simpl Z_one_bits.
  rewrite (Zdecomp x) in H0. rewrite Zshiftin_spec in H0.
  assert (EQ: Z.div2 x × two_p (i + 1) = powerserie (Z_one_bits n (Z.div2 x) (i + 1))).
    apply IHn. omega.
    destruct (Z.odd x); omega.
  rewrite two_p_is_exp in EQ. change (two_p 1) with 2 in EQ.
  rewrite (Zdecomp x) at 1. rewrite Zshiftin_spec.
  destruct (Z.odd x); simpl powerserie; rewrite <- EQ; ring.
  omega. omega.
  }
  intros. rewrite <- H. change (two_p 0) with 1. omega.
  omega. exact H0.
Qed.

Lemma Z_one_bits_range:
   x i, In i (Z_one_bits wordsize x 0) 0 i < zwordsize.
Proof.
  assert ( n x i j,
    In j (Z_one_bits n x i) i j < i + Z_of_nat n).
  {
  induction n; simpl In.
  tauto.
  intros x i j. rewrite inj_S.
  assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) i j < i + Z.succ (Z.of_nat n)).
    intros. exploit IHn; eauto. omega.
  destruct (Z.odd x); simpl.
  intros [A|B]. subst j. omega. auto.
  auto.
  }
  intros. generalize (H wordsize x 0 i H0). fold zwordsize; omega.
Qed.

Lemma is_power2_rng:
   n logn,
  is_power2 n = Some logn
  0 unsigned logn < zwordsize.
Proof.
  intros n logn. unfold is_power2.
  generalize (Z_one_bits_range (unsigned n)).
  destruct (Z_one_bits wordsize (unsigned n) 0).
  intros; discriminate.
  destruct l.
  intros. injection H0; intro; subst logn; clear H0.
  assert (0 z < zwordsize).
  apply H. auto with coqlib.
  rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega.
  intros; discriminate.
Qed.

Theorem is_power2_range:
   n logn,
  is_power2 n = Some logn ltu logn iwordsize = true.
Proof.
  intros. unfold ltu. rewrite unsigned_repr_wordsize.
  apply zlt_true. generalize (is_power2_rng _ _ H). tauto.
Qed.

Lemma is_power2_correct:
   n logn,
  is_power2 n = Some logn
  unsigned n = two_p (unsigned logn).
Proof.
  intros n logn. unfold is_power2.
  generalize (Z_one_bits_powerserie (unsigned n) (unsigned_range n)).
  generalize (Z_one_bits_range (unsigned n)).
  destruct (Z_one_bits wordsize (unsigned n) 0).
  intros; discriminate.
  destruct l.
  intros. simpl in H0. injection H1; intros; subst logn; clear H1.
  rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
  auto. omega. elim (H z); intros.
  generalize wordsize_max_unsigned; omega.
  auto with coqlib.
  intros; discriminate.
Qed.

Remark two_p_range:
   n,
  0 n < zwordsize
  0 two_p n max_unsigned.
Proof.
  intros. split.
  assert (two_p n > 0). apply two_p_gt_ZERO. omega. omega.
  generalize (two_p_monotone_strict _ _ H).
  unfold zwordsize; rewrite <- two_power_nat_two_p.
  unfold max_unsigned, modulus. omega.
Qed.

Remark Z_one_bits_zero:
   n i, Z_one_bits n 0 i = nil.
Proof.
  induction n; intros; simpl; auto.
Qed.

Remark Z_one_bits_two_p:
   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.
  assert (Z.odd (two_p x) = false Z.div2 (two_p x) = two_p (x-1)).
    apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec.
    rewrite <- two_p_S. rewrite Zplus_0_r. f_equal; omega. omega.
  destruct H1 as [A B]; rewrite A; rewrite B.
  rewrite IHn. f_equal; omega. omega.
Qed.

Lemma is_power2_two_p:
   n, 0 n < zwordsize
  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.

Relation between bitwise operations and multiplications / divisions by powers of 2

Left shifts and multiplications by powers of 2.

Lemma Zshiftl_mul_two_p:
   x n, 0 n Z.shiftl x n = x × two_p n.
Proof.
  intros. destruct n; simpl.
  - omega.
  - pattern p. apply Pos.peano_ind.
    + change (two_power_pos 1) with 2. simpl. ring.
    + intros. rewrite Pos.iter_succ. rewrite H0.
      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
      change (two_power_pos 1) with 2. ring.
  - compute in H. congruence.
Qed.

Lemma shl_mul_two_p:
   x y,
  shl x y = mul x (repr (two_p (unsigned y))).
Proof.
  intros. unfold shl, mul. apply eqm_samerepr.
  rewrite Zshiftl_mul_two_p. auto with ints.
  generalize (unsigned_range y); omega.
Qed.

Theorem shl_mul:
   x y,
  shl x y = mul x (shl one y).
Proof.
  intros.
  assert (shl one y = repr (two_p (unsigned y))).
  {
    rewrite shl_mul_two_p. rewrite mul_commut. rewrite mul_one. auto.
  }
  rewrite H. apply shl_mul_two_p.
Qed.

Theorem mul_pow2:
   x n logn,
  is_power2 n = Some logn
  mul x n = shl x logn.
Proof.
  intros. generalize (is_power2_correct n logn H); intro.
  rewrite shl_mul_two_p. rewrite <- H0. rewrite repr_unsigned.
  auto.
Qed.

Theorem shifted_or_is_add:
   x y n,
  0 n < zwordsize
  unsigned y < two_p n
  or (shl x (repr n)) y = repr(unsigned x × two_p n + unsigned y).
Proof.
  intros. rewrite <- add_is_or.
  - unfold add. apply eqm_samerepr. apply eqm_add; auto with ints.
    rewrite shl_mul_two_p. unfold mul. apply eqm_unsigned_repr_l.
    apply eqm_mult; auto with ints. apply eqm_unsigned_repr_l.
    apply eqm_refl2. rewrite unsigned_repr. auto.
    generalize wordsize_max_unsigned; omega.
  - bit_solve.
    rewrite unsigned_repr.
    destruct (zlt i n).
    + auto.
    + replace (testbit y i) with false. apply andb_false_r.
      symmetry. unfold testbit.
      assert (EQ: Z.of_nat (Z.to_nat n) = n) by (apply Z2Nat.id; omega).
      apply Ztestbit_above with (Z.to_nat n).
      rewrite <- EQ in H0. rewrite <- two_power_nat_two_p in H0.
      generalize (unsigned_range y); omega.
      rewrite EQ; auto.
    + generalize wordsize_max_unsigned; omega.
Qed.

Unsigned right shifts and unsigned divisions by powers of 2.

Lemma Zshiftr_div_two_p:
   x n, 0 n Z.shiftr x n = x / two_p n.
Proof.
  intros. destruct n; unfold Z.shiftr; simpl.
  - rewrite Zdiv_1_r. auto.
  - pattern p. apply Pos.peano_ind.
    + change (two_power_pos 1) with 2. simpl. apply Zdiv2_div.
    + intros. rewrite Pos.iter_succ. rewrite H0.
      rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
      change (two_power_pos 1) with 2.
      rewrite Zdiv2_div. rewrite Zmult_comm. apply Zdiv_Zdiv.
      rewrite two_power_pos_nat. apply two_power_nat_pos. omega.
  - compute in H. congruence.
Qed.

Lemma shru_div_two_p:
   x y,
  shru x y = repr (unsigned x / two_p (unsigned y)).
Proof.
  intros. unfold shru.
  rewrite Zshiftr_div_two_p. auto.
  generalize (unsigned_range y); omega.
Qed.

Theorem divu_pow2:
   x n logn,
  is_power2 n = Some logn
  divu x n = shru x logn.
Proof.
  intros. generalize (is_power2_correct n logn H). intro.
  symmetry. unfold divu. rewrite H0. apply shru_div_two_p.
Qed.

Signed right shifts and signed divisions by powers of 2.

Lemma shr_div_two_p:
   x y,
  shr x y = repr (signed x / two_p (unsigned y)).
Proof.
  intros. unfold shr.
  rewrite Zshiftr_div_two_p. auto.
  generalize (unsigned_range y); omega.
Qed.

Theorem divs_pow2:
   x n logn,
  is_power2 n = Some logn
  divs x n = shrx x logn.
Proof.
  intros. generalize (is_power2_correct _ _ H); intro.
  unfold shrx. rewrite shl_mul_two_p.
  rewrite mul_commut. rewrite mul_one.
  rewrite <- H0. rewrite repr_unsigned. auto.
Qed.

Unsigned modulus over 2^n is masking with 2^n-1.

Lemma Ztestbit_mod_two_p:
   n x i,
  0 n 0 i
  Z.testbit (x mod (two_p n)) i = if zlt i n then Z.testbit x i else false.
Proof.
  intros n0 x i N0POS. revert x i; pattern n0; apply natlike_ind; auto.
  - intros. change (two_p 0) with 1. rewrite Zmod_1_r. rewrite Z.testbit_0_l.
    rewrite zlt_false; auto. omega.
  - intros. rewrite two_p_S; auto.
    replace (x0 mod (2 × two_p x))
       with (Zshiftin (Z.odd x0) (Z.div2 x0 mod two_p x)).
    rewrite Ztestbit_shiftin; auto. rewrite (Ztestbit_eq i x0); auto. destruct (zeq i 0).
    + rewrite zlt_true; auto. omega.
    + rewrite H0. destruct (zlt (Z.pred i) x).
      × rewrite zlt_true; auto. omega.
      × rewrite zlt_false; auto. omega.
      × omega.
    + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry.
      apply Zmod_unique with (x1 / two_p x).
      rewrite !Zshiftin_spec. rewrite Zplus_assoc. f_equal.
      transitivity (2 × (two_p x × (x1 / two_p x) + x1 mod two_p x)).
      f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto.
      ring.
      rewrite Zshiftin_spec. exploit (Z_mod_lt x1 (two_p x)). apply two_p_gt_ZERO; auto.
      destruct (Z.odd x0); omega.
Qed.

Corollary Ztestbit_two_p_m1:
   n i, 0 n 0 i
  Z.testbit (two_p n - 1) i = if zlt i n then true else false.
Proof.
  intros. replace (two_p n - 1) with ((-1) mod (two_p n)).
  rewrite Ztestbit_mod_two_p; auto. destruct (zlt i n); auto. apply Ztestbit_m1; auto.
  apply Zmod_unique with (-1). ring.
  exploit (two_p_gt_ZERO n). auto. omega.
Qed.

Theorem modu_and:
   x n logn,
  is_power2 n = Some logn
  modu x n = and x (sub n one).
Proof.
  intros. generalize (is_power2_correct _ _ H); intro.
  generalize (is_power2_rng _ _ H); intro.
  apply same_bits_eq; intros.
  rewrite bits_and; auto.
  unfold sub. rewrite testbit_repr; auto.
  rewrite H0. rewrite unsigned_one.
  unfold modu. rewrite testbit_repr; auto. rewrite H0.
  rewrite Ztestbit_mod_two_p. rewrite Ztestbit_two_p_m1.
  destruct (zlt i (unsigned logn)).
  rewrite andb_true_r; auto.
  rewrite andb_false_r; auto.
  tauto. tauto. tauto. tauto.
Qed.

Properties of shrx (signed division by a power of 2)


Lemma Zquot_Zdiv:
   x y,
  y > 0
  Z.quot x y = if zlt x 0 then (x + y - 1) / y else x / y.
Proof.
  intros. destruct (zlt x 0).
  - symmetry. apply Zquot_unique_full with ((x + y - 1) mod y - (y - 1)).
     + red. right; split. omega.
       exploit (Z_mod_lt (x + y - 1) y); auto.
       rewrite Z.abs_eq. omega. omega.
     + transitivity ((y × ((x + y - 1) / y) + (x + y - 1) mod y) - (y-1)).
       rewrite <- Z_div_mod_eq. ring. auto. ring.
  - apply Zquot_Zdiv_pos; omega.
Qed.

Theorem shrx_shr:
   x y,
  ltu y (repr (zwordsize - 1)) = true
  shrx x y = shr (if lt x zero then add x (sub (shl one y) one) else x) y.
Proof.
  intros.
  set (uy := unsigned y).
  assert (0