path: root/lib/Integers.v

(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *)

Require Import Coqlib.

Definition wordsize : nat := 32%nat.
Definition modulus : Z := two_power_nat wordsize.
Definition half_modulus : Z := modulus / 2.

(** * Comparisons *)

Inductive comparison : Set :=
  | Ceq : comparison               (**r same *)
  | Cne : comparison               (**r different *)
  | Clt : comparison               (**r less than *)
  | Cle : comparison               (**r less than or equal *)
  | Cgt : comparison               (**r greater than *)
  | Cge : comparison.              (**r greater than or equal *)

Definition negate_comparison (c: comparison): comparison :=
  match c with
  | Ceq => Cne
  | Cne => Ceq
  | Clt => Cge
  | Cle => Cgt
  | Cgt => Cle
  | Cge => Clt
  end.

Definition swap_comparison (c: comparison): comparison :=
  match c with
  | Ceq => Ceq
  | Cne => Cne
  | Clt => Cgt
  | Cle => Cge
  | Cgt => Clt
  | Cge => Cle
  end.

(** * 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: Set := mkint { intval: Z; intrange: 0 <= intval < modulus }.

Module Int.

Definition max_unsigned : Z := modulus - 1.
Definition max_signed : Z := half_modulus - 1.
Definition min_signed : Z := - half_modulus.

(** 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 :=
  if zlt (unsigned n) half_modulus
  then unsigned n
  else unsigned n - modulus.

Lemma mod_in_range:
  forall x, 0 <= Zmod x modulus < modulus.
Proof.
  intro.
  exact (Z_mod_lt x modulus (two_power_nat_pos wordsize)).
Qed.

(** Conversely, [repr] takes a Coq integer and returns the corresponding
  machine integer.  The argument is treated modulo [modulus]. *)

Definition repr (x: Z) : int := 
  mkint (Zmod x modulus) (mod_in_range x).

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

Lemma mkint_eq:
  forall x y Px Py, x = y -> mkint x Px = mkint y Py.
Proof.
  intros. subst y. 
  generalize (proof_irrelevance _ Px Py); intro.
  subst Py. reflexivity.
Qed.

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

(** * 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 cast8signed (x: int) : int :=
  let y := Zmod (unsigned x) 256 in
  if zlt y 128 then repr y else repr (y - 256).
Definition cast8unsigned (x: int) : int :=
  repr (Zmod (unsigned x) 256).
Definition cast16signed (x: int) : int :=
  let y := Zmod (unsigned x) 65536 in
  if zlt y 32768 then repr y else repr (y - 65536).
Definition cast16unsigned (x: int) : int :=
  repr (Zmod (unsigned x) 65536).

Definition 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 Zdiv_round (x y: Z) : Z :=
  if zlt x 0 then
    if zlt y 0 then (-x) / (-y) else - ((-x) / y)
  else
    if zlt y 0 then -(x / (-y)) else x / y.

Definition Zmod_round (x y: Z) : Z :=
  x - (Zdiv_round x y) * y.

Definition divs (x y: int) : int :=
  repr (Zdiv_round (signed x) (signed y)).
Definition mods (x y: int) : int :=
  repr (Zmod_round (signed x) (signed y)).
Definition divu (x y: int) : int :=
  repr (unsigned x / unsigned y).
Definition modu (x y: int) : int :=
  repr (Zmod (unsigned x) (unsigned y)).

(** For bitwise operations, we need to convert between Coq integers [Z]
  and their bit-level representations.  Bit-level representations are
  represented as characteristic functions, that is, functions [f]
  of type [nat -> bool] such that [f i] is the value of the [i]-th bit
  of the number.  The values of characteristic functions for [i] greater
  than 32 are ignored. *)

Definition Z_shift_add (b: bool) (x: Z) :=
  if b then 2 * x + 1 else 2 * x.

Definition Z_bin_decomp (x: Z) : bool * Z :=
  match x with
  | Z0 => (false, 0)
  | Zpos p =>
      match p with
      | xI q => (true, Zpos q)
      | xO q => (false, Zpos q)
      | xH => (true, 0)
      end
  | Zneg p =>
      match p with
      | xI q => (true, Zneg q - 1)
      | xO q => (false, Zneg q)
      | xH => (true, -1)
      end
  end.

Fixpoint bits_of_Z (n: nat) (x: Z) {struct n}: Z -> bool :=
  match n with
  | O =>
      (fun i: Z => false)
  | S m =>
      let (b, y) := Z_bin_decomp x in
      let f := bits_of_Z m y in
      (fun i: Z => if zeq i 0 then b else f (i - 1))
  end.

Fixpoint Z_of_bits (n: nat) (f: Z -> bool) {struct n}: Z :=
  match n with
  | O => 0
  | S m => Z_shift_add (f 0) (Z_of_bits m (fun i => f (i + 1)))
  end.

(** Bitwise logical ``and'', ``or'' and ``xor'' operations. *)

Definition bitwise_binop (f: bool -> bool -> bool) (x y: int) :=
  let fx := bits_of_Z wordsize (unsigned x) in
  let fy := bits_of_Z wordsize (unsigned y) in
  repr (Z_of_bits wordsize (fun i => f (fx i) (fy i))).

Definition and (x y: int): int := bitwise_binop andb x y.
Definition or (x y: int): int := bitwise_binop orb x y.
Definition xor (x y: int) : int := bitwise_binop xorb x y.

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

(** Shifts and rotates. *)

Definition shl (x y: int): int :=
  let fx := bits_of_Z wordsize (unsigned x) in
  let vy := unsigned y in
  repr (Z_of_bits wordsize (fun i => fx (i - vy))).

Definition shru (x y: int): int :=
  let fx := bits_of_Z wordsize (unsigned x) in
  let vy := unsigned y in
  repr (Z_of_bits wordsize (fun i => fx (i + vy))).

(** Arithmetic right shift is defined as signed division by a power of two.
  Two such shifts are defined: [shr] rounds towards minus infinity
  (standard behaviour for arithmetic right shift) and
  [shrx] rounds towards zero. *)

Definition shr (x y: int): int :=
  repr (signed x / two_p (unsigned y)).
Definition shrx (x y: int): int :=
  divs x (shl one y).

Definition shr_carry (x y: int) :=
  sub (shrx x y) (shr x y).

Definition rol (x y: int) : int :=
  let fx := bits_of_Z wordsize (unsigned x) in
  let vy := unsigned y in
  repr (Z_of_bits wordsize
         (fun i => fx (Zmod (i - vy) (Z_of_nat wordsize)))).

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

(** Decomposition of a number as a sum of powers of two. *)

Fixpoint Z_one_bits (n: nat) (x: Z) (i: Z) {struct n}: list Z :=
  match n with
  | O => nil
  | S m =>
      let (b, y) := Z_bin_decomp x in
      if b then i :: Z_one_bits m y (i+1) else Z_one_bits m y (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 :: nil => Some (repr i)
  | _ => None
  end.

(** Recognition of integers that are acceptable as immediate operands
  to the [rlwim] PowerPC instruction.  These integers are of the form
  [000011110000] or [111100001111], that is, a run of one bits
  surrounded by zero bits, or conversely.  We recognize these integers by
  running the following automaton on the bits.  The accepting states are
  2, 3, 4, 5, and 6.
<<
               0          1          0
              / \        / \        / \
              \ /        \ /        \ /
        -0--> [1] --1--> [2] --0--> [3]
       /     
     [0]
       \
        -1--> [4] --0--> [5] --1--> [6]
              / \        / \        / \
              \ /        \ /        \ /
               1          0          1
>>
*)

Inductive rlw_state: Set :=
  | RLW_S0 : rlw_state
  | RLW_S1 : rlw_state
  | RLW_S2 : rlw_state
  | RLW_S3 : rlw_state
  | RLW_S4 : rlw_state
  | RLW_S5 : rlw_state
  | RLW_S6 : rlw_state
  | RLW_Sbad : rlw_state.

Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
  match s, b with
  | RLW_S0, false => RLW_S1
  | RLW_S0, true  => RLW_S4
  | RLW_S1, false => RLW_S1
  | RLW_S1, true  => RLW_S2
  | RLW_S2, false => RLW_S3
  | RLW_S2, true  => RLW_S2
  | RLW_S3, false => RLW_S3
  | RLW_S3, true  => RLW_Sbad
  | RLW_S4, false => RLW_S5
  | RLW_S4, true  => RLW_S4
  | RLW_S5, false => RLW_S5
  | RLW_S5, true  => RLW_S6
  | RLW_S6, false => RLW_Sbad
  | RLW_S6, true  => RLW_S6
  | RLW_Sbad, _ => RLW_Sbad
  end.

Definition rlw_accepting (s: rlw_state) : bool :=
  match s with
  | RLW_S0 => false
  | RLW_S1 => false
  | RLW_S2 => true
  | RLW_S3 => true
  | RLW_S4 => true
  | RLW_S5 => true
  | RLW_S6 => true
  | RLW_Sbad => false
  end.

Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
  match n with
  | O =>
      rlw_accepting s
  | S m =>
      let (b, y) := Z_bin_decomp x in
      is_rlw_mask_rec m (rlw_transition s b) y
  end.

Definition is_rlw_mask (x: int) : bool :=
  is_rlw_mask_rec wordsize RLW_S0 (unsigned x).

(** Comparisons. *)

Definition cmp (c: comparison) (x y: int) : bool :=
  match c with
  | Ceq => eq x y
  | Cne => negb (eq x y)
  | Clt => lt x y
  | Cle => negb (lt y x)
  | Cgt => lt y x
  | Cge => negb (lt x y)
  end.

Definition cmpu (c: comparison) (x y: int) : bool :=
  match c with
  | Ceq => eq x y
  | Cne => negb (eq x y)
  | Clt => ltu x y
  | Cle => negb (ltu y x)
  | Cgt => ltu y x
  | Cge => negb (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 equality *)

Theorem one_not_zero: Int.one <> Int.zero.
Proof.
  compute. congruence. 
Qed.

Theorem eq_sym:
  forall 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: forall (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: forall x, eq x x = true.
Proof.
  intros. generalize (eq_spec x x); case (eq x x); intros; congruence.
Qed.

Theorem eq_false: forall x y, x <> y -> eq x y = false.
Proof.
  intros. generalize (eq_spec x y); case (eq x y); intros; congruence.
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 := exists k, x = k * modul + y.

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

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

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

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

Lemma eqmod_small_eq:
  forall 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:
  forall 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:
  forall x, eqmod x (x mod modul).
Proof.
  intros; red. exists (x / modul). 
  rewrite Zmult_comm. apply Z_div_mod_eq. auto.
Qed.

Lemma eqmod_add:
  forall 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. exists (k1 + k2). ring.
Qed.

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

Lemma eqmod_sub:
  forall 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. exists (k1 - k2). ring.
Qed.

Lemma eqmod_mult:
  forall 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.
  exists (k1 * k2 * modul + c * k2 + k1 * d).
  ring.
Qed.

End EQ_MODULO.

(** We then specialize these definitions to equality modulo 
  $2^32$ #2<sup>32</sup>#. *)

Lemma modulus_pos:
  modulus > 0.
Proof.
  unfold modulus. apply two_power_nat_pos. 
Qed.
Hint Resolve modulus_pos: ints.

Definition eqm := eqmod modulus.

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

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

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

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

Lemma eqm_samerepr: forall x y, eqm x y -> repr x = repr y.
Proof.
  intros. unfold repr. apply mkint_eq. 
  apply eqmod_mod_eq. auto with ints. exact H.
Qed.

Lemma eqm_small_eq:
  forall 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:
  forall 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:
  forall x y, eqm x y -> eqm (-x) (-y).
Proof (eqmod_neg modulus).
Hint Resolve eqm_neg: ints.

Lemma eqm_sub:
  forall 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:
  forall 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_unsigned_repr:
  forall z, eqm z (unsigned (repr z)).
Proof.
  unfold eqm, repr, unsigned; intros; simpl.
  apply eqmod_mod. auto with ints.
Qed.
Hint Resolve eqm_unsigned_repr: ints.

Lemma eqm_unsigned_repr_l:
  forall 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:
  forall 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:
  forall x, eqm (signed x) (unsigned x).
Proof.
  intro; red; unfold signed. set (y := unsigned x).
  case (zlt y half_modulus); intro.
  apply eqmod_refl. red; exists (-1); ring. 
Qed.

Theorem unsigned_range:
  forall i, 0 <= unsigned i < modulus.
Proof.
  destruct i; simpl. auto.
Qed.
Hint Resolve unsigned_range: ints.

Theorem unsigned_range_2:
  forall 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:
  forall 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. assert (min_signed < 0). compute. auto.
  omega. 
  unfold min_signed, max_signed. change modulus with (2 * half_modulus).
  change modulus with (2 * half_modulus) in H. omega.
Qed.  

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

Lemma repr_signed:
  forall 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_unsigned: ints.

Theorem unsigned_repr:
  forall z, 0 <= z <= max_unsigned -> unsigned (repr z) = z.
Proof.
  intros. unfold repr, unsigned; simpl. 
  apply Zmod_small. unfold max_unsigned in H. omega.
Qed.
Hint Resolve unsigned_repr: ints.

Theorem signed_repr:
  forall z, min_signed <= z <= max_signed -> signed (repr z) = z.
Proof.
  intros. unfold signed. case (zle 0 z); intro.
  replace (unsigned (repr z)) with z.
  rewrite zlt_true. auto. unfold max_signed in H. omega.
  symmetry. apply unsigned_repr. 
  split. auto. apply Zle_trans with max_signed. tauto.
  compute; intro; discriminate.
  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. 
  change modulus with (half_modulus + half_modulus). omega.
  symmetry. apply unsigned_repr.
  unfold z', max_unsigned. unfold min_signed, max_signed in H.
  change modulus with (half_modulus + half_modulus).
  omega. 
  apply eqm_samerepr. unfold z'; red. exists 1. omega.
Qed.

(** ** Properties of addition *)

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

Theorem add_signed: forall 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: forall x y, add x y = add y x.
Proof. intros; unfold add. decEq. omega. Qed.

Theorem add_zero: forall x, add x zero = x.
Proof. 
  intros; unfold add, zero. change (unsigned (repr 0)) with 0.
  rewrite Zplus_0_r. apply repr_unsigned.
Qed.

Theorem add_assoc: forall 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: forall x y z, add x (add y z) = add y (add x z).
Proof.
  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut. 
Qed.

Theorem add_neg_zero: forall 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.

(** ** Properties of negation *)

Theorem neg_repr: forall 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, zero. compute. apply mkint_eq. auto.
Qed.

Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
Proof.
  intros; unfold neg, add. apply eqm_samerepr.
  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: forall x, sub x zero = x.
Proof.
  intros; unfold sub. change (unsigned zero) with 0.
  replace (unsigned x - 0) with (unsigned x). apply repr_unsigned.
  omega.
Qed.

Theorem sub_zero_r: forall x, sub zero x = neg x.
Proof.
  intros; unfold sub, neg. change (unsigned zero) with 0.
  replace (0 - unsigned x) with (- unsigned x). auto.
  omega.
Qed.

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

Theorem sub_idem: forall x, sub x x = zero.
Proof.
  intros; unfold sub. replace (unsigned x - unsigned x) with 0.
  reflexivity. omega.
Qed.

Theorem sub_add_l: forall 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: forall 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:
  forall 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.

(** ** Properties of multiplication *)

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

Theorem mul_zero: forall x, mul x zero = zero.
Proof.
  intros; unfold mul. change (unsigned zero) with 0.
  unfold zero. decEq. ring.
Qed.

Theorem mul_one: forall x, mul x one = x.
Proof.
  intros; unfold mul. change (unsigned one) with 1.
  transitivity (repr (unsigned x)). decEq. ring.
  apply repr_unsigned.
Qed.

Theorem mul_assoc: forall 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:
  forall 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:
  forall 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: 
  forall 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:
   forall 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.

(** ** Properties of binary decompositions *)

Lemma Z_shift_add_bin_decomp:
  forall x,
  Z_shift_add (fst (Z_bin_decomp x)) (snd (Z_bin_decomp x)) = x.
Proof.
  destruct x; simpl.
  auto.
  destruct p; reflexivity.
  destruct p; try reflexivity. simpl. 
  assert (forall z, 2 * (z + 1) - 1 = 2 * z + 1). intro; omega.
  generalize (H (Zpos p)); simpl. congruence.
Qed.

Lemma Z_shift_add_inj:
  forall b1 x1 b2 x2,
  Z_shift_add b1 x1 = Z_shift_add b2 x2 -> b1 = b2 /\ x1 = x2.
Proof.
  intros until x2.
  unfold Z_shift_add.
  destruct b1; destruct b2; intros;
  ((split; [reflexivity|omega]) || omegaContradiction).
Qed.

Lemma Z_of_bits_exten:
  forall n f1 f2,
  (forall z, 0 <= z < Z_of_nat n -> f1 z = f2 z) ->
  Z_of_bits n f1 = Z_of_bits n f2.
Proof.
  induction n; intros.
  reflexivity.
  simpl. rewrite inj_S in H. decEq. apply H. omega. 
  apply IHn. intros; apply H. omega.
Qed.

Opaque Zmult.

Lemma Z_of_bits_of_Z:
  forall x, eqm (Z_of_bits wordsize (bits_of_Z wordsize x)) x.
Proof.
  assert (forall n x, exists k,
    Z_of_bits n (bits_of_Z n x) = k * two_power_nat n + x).
  induction n; intros.
  rewrite two_power_nat_O. simpl. exists (-x). omega.
  rewrite two_power_nat_S. simpl.
  caseEq (Z_bin_decomp x). intros b y ZBD. simpl. 
  replace (Z_of_bits n (fun i => if zeq (i + 1) 0 then b else bits_of_Z n y (i + 1 - 1)))
     with (Z_of_bits n (bits_of_Z n y)).
  elim (IHn y). intros k1 EQ1. rewrite EQ1.
  rewrite <- (Z_shift_add_bin_decomp x). 
  rewrite ZBD. simpl. 
  exists k1.
  case b; unfold Z_shift_add; ring.
  apply Z_of_bits_exten. intros.
  rewrite zeq_false. decEq. omega. omega. 
  intro. exact (H wordsize x).
Qed.

Lemma bits_of_Z_zero:
  forall n x, bits_of_Z n 0 x = false.
Proof.
  induction n; simpl; intros.
  auto.
  case (zeq x 0); intro. auto. auto.
Qed.

Remark Z_bin_decomp_2xm1:
  forall x, Z_bin_decomp (2 * x - 1) = (true, x - 1).
Proof.
  intros. caseEq (Z_bin_decomp (2 * x - 1)). intros b y EQ.
  generalize (Z_shift_add_bin_decomp (2 * x - 1)).
  rewrite EQ; simpl.
  replace (2 * x - 1) with (Z_shift_add true (x - 1)).
  intro. elim (Z_shift_add_inj _ _ _ _ H); intros.
  congruence. unfold Z_shift_add. omega.
Qed.

Lemma bits_of_Z_mone:
  forall n x,
  0 <= x < Z_of_nat n -> 
  bits_of_Z n (two_power_nat n - 1) x = true.
Proof.
  induction n; intros.
  simpl in H. omegaContradiction.
  unfold bits_of_Z; fold bits_of_Z.
  rewrite two_power_nat_S. rewrite Z_bin_decomp_2xm1.
  rewrite inj_S in H. case (zeq x 0); intro. auto.
  apply IHn. omega. 
Qed.

Lemma Z_bin_decomp_shift_add:
  forall b x, Z_bin_decomp (Z_shift_add b x) = (b, x).
Proof.
  intros. caseEq (Z_bin_decomp (Z_shift_add b x)); intros b' x' EQ.
  generalize (Z_shift_add_bin_decomp (Z_shift_add b x)).
  rewrite EQ; simpl fst; simpl snd. intro.
  elim (Z_shift_add_inj _ _ _ _ H); intros.
  congruence.
Qed.

Lemma bits_of_Z_of_bits:
  forall n f i,
  0 <= i < Z_of_nat n ->
  bits_of_Z n (Z_of_bits n f) i = f i.
Proof.
  induction n; intros; simpl.
  simpl in H. omegaContradiction.
  rewrite Z_bin_decomp_shift_add.
  case (zeq i 0); intro.
  congruence.
  rewrite IHn. decEq. omega. rewrite inj_S in H. omega.
Qed.  

Lemma Z_of_bits_range:
  forall f, 0 <= Z_of_bits wordsize f < modulus.
Proof.
  unfold max_unsigned, modulus.
  generalize wordsize. induction n; simpl; intros.
  rewrite two_power_nat_O. omega.
  rewrite two_power_nat_S. generalize (IHn (fun i => f (i + 1))).
  set (x := Z_of_bits n (fun i => f (i + 1))).
  intro. destruct (f 0); unfold Z_shift_add; omega.
Qed.
Hint Resolve Z_of_bits_range: ints.

Lemma Z_of_bits_range_2:
  forall f, 0 <= Z_of_bits wordsize f <= max_unsigned.
Proof.
  intros. unfold max_unsigned.
  generalize (Z_of_bits_range f). omega.
Qed.
Hint Resolve Z_of_bits_range_2: ints.

Lemma bits_of_Z_below:
  forall n x i, i < 0 -> bits_of_Z n x i = false.
Proof.
  induction n; simpl; intros.
  reflexivity.
  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
  omega. omega.
Qed.

Lemma bits_of_Z_above:
  forall n x i, i >= Z_of_nat n -> bits_of_Z n x i = false.
Proof.
  induction n; intros; simpl.
  reflexivity.
  destruct (Z_bin_decomp x). rewrite zeq_false. apply IHn.
  rewrite inj_S in H. omega. rewrite inj_S in H. omega.
Qed.

Opaque Zmult.

Lemma Z_of_bits_excl:
  forall n f g h,
  (forall i, 0 <= i < Z_of_nat n -> f i && g i = false) ->
  (forall i, 0 <= i < Z_of_nat n -> f i || g i = h i) ->
  Z_of_bits n f + Z_of_bits n g = Z_of_bits n h.
Proof.
  induction n.
  intros; reflexivity.
  intros. simpl. rewrite inj_S in H. rewrite inj_S in H0.
  rewrite <- (IHn (fun i => f(i+1)) (fun i => g(i+1)) (fun i => h(i+1))).
  assert (0 <= 0 < Zsucc(Z_of_nat n)). omega.
  unfold Z_shift_add.
  rewrite <- H0; auto.
  set (F := Z_of_bits n (fun i => f(i + 1))).
  set (G := Z_of_bits n (fun i => g(i + 1))).
  caseEq (f 0); intros; caseEq (g 0); intros; simpl.
  generalize (H 0 H1). rewrite H2; rewrite H3. simpl. intros; discriminate.
  omega. omega. omega.
  intros; apply H. omega.
  intros; apply H0. omega.
Qed.

(** ** Properties of bitwise and, or, xor *)

Lemma bitwise_binop_commut:
  forall f,
  (forall a b, f a b = f b a) ->
  forall x y,
  bitwise_binop f x y = bitwise_binop f y x.
Proof.
  unfold bitwise_binop; intros.
  decEq. apply Z_of_bits_exten; intros. auto.
Qed.

Lemma bitwise_binop_assoc:
  forall f,
  (forall a b c, f a (f b c) = f (f a b) c) ->
  forall x y z,
  bitwise_binop f (bitwise_binop f x y) z =
  bitwise_binop f x (bitwise_binop f y z).
Proof.
  unfold bitwise_binop; intros.
  repeat rewrite unsigned_repr; auto with ints.
  decEq. apply Z_of_bits_exten; intros.
  repeat (rewrite bits_of_Z_of_bits; auto).
Qed.

Lemma bitwise_binop_idem:
  forall f,
  (forall a, f a a = a) ->
  forall x,
  bitwise_binop f x x = x.
Proof.
  unfold bitwise_binop; intros.
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
  decEq. apply Z_of_bits_exten; intros. auto.
  transitivity (repr (unsigned x)).
  apply eqm_samerepr. apply Z_of_bits_of_Z. apply repr_unsigned.
Qed.

Theorem and_commut: forall x y, and x y = and y x.
Proof (bitwise_binop_commut andb andb_comm).

Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
Proof (bitwise_binop_assoc andb andb_assoc).

Theorem and_zero: forall x, and x zero = zero.
Proof.
  unfold and, bitwise_binop, zero; intros. 
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize 0))).
  decEq. apply Z_of_bits_exten. intros.
  change (unsigned (repr 0)) with 0.
  rewrite bits_of_Z_zero. apply andb_b_false.
  auto with ints.
Qed.

Lemma mone_max_unsigned:
  mone = repr max_unsigned.
Proof.
  unfold mone. apply eqm_samerepr. exists (-1).
  unfold max_unsigned. omega.
Qed.

Theorem and_mone: forall x, and x mone = x.
Proof.
  unfold and, bitwise_binop; intros. 
  rewrite mone_max_unsigned. unfold max_unsigned, modulus.
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
  decEq. apply Z_of_bits_exten. intros.
  rewrite unsigned_repr. rewrite bits_of_Z_mone. 
  apply andb_b_true. omega. compute. intuition congruence.
  transitivity (repr (unsigned x)). 
  apply eqm_samerepr. apply Z_of_bits_of_Z.
  apply repr_unsigned.
Qed.

Theorem and_idem: forall x, and x x = x.
Proof.
  assert (forall b, b && b = b).
    destruct b; reflexivity.
  exact (bitwise_binop_idem andb H).
Qed.

Theorem or_commut: forall x y, or x y = or y x.
Proof (bitwise_binop_commut orb orb_comm).

Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
Proof (bitwise_binop_assoc orb orb_assoc).

Theorem or_zero: forall x, or x zero = x.
Proof.
  unfold or, bitwise_binop, zero; intros. 
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
  decEq. apply Z_of_bits_exten. intros.
  change (unsigned (repr 0)) with 0.
  rewrite bits_of_Z_zero. apply orb_b_false.
  transitivity (repr (unsigned x)); auto with ints.
  apply eqm_samerepr. apply Z_of_bits_of_Z.
Qed.

Theorem or_mone: forall x, or x mone = mone.
Proof.
  rewrite mone_max_unsigned. 
  unfold or, bitwise_binop; intros.
  decEq. 
  transitivity (Z_of_bits wordsize (bits_of_Z wordsize max_unsigned)).
  apply Z_of_bits_exten. intros.
  change (unsigned (repr max_unsigned)) with max_unsigned.
  unfold max_unsigned, modulus. rewrite bits_of_Z_mone; auto.
  apply orb_b_true. 
  apply eqm_small_eq; auto with ints. compute; intuition congruence.
Qed.

Theorem or_idem: forall x, or x x = x.
Proof.
  assert (forall b, b || b = b).
    destruct b; reflexivity.
  exact (bitwise_binop_idem orb H).
Qed.

Theorem and_or_distrib:
  forall x y z,
  and x (or y z) = or (and x y) (and x z).
Proof.
  intros; unfold and, or, bitwise_binop.
  decEq. repeat rewrite unsigned_repr; auto with ints.
  apply Z_of_bits_exten; intros.
  repeat rewrite bits_of_Z_of_bits; auto.
  apply demorgan1.
Qed.  

Theorem xor_commut: forall x y, xor x y = xor y x.
Proof (bitwise_binop_commut xorb xorb_comm).

Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
Proof.
  assert (forall a b c, xorb a (xorb b c) = xorb (xorb a b) c).
  symmetry. apply xorb_assoc.
  exact (bitwise_binop_assoc xorb H).
Qed.

Theorem xor_zero: forall x, xor x zero = x.
Proof.
  unfold xor, bitwise_binop, zero; intros. 
  transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
  decEq. apply Z_of_bits_exten. intros.
  change (unsigned (repr 0)) with 0.
  rewrite bits_of_Z_zero. apply xorb_false.
  transitivity (repr (unsigned x)); auto with ints.
  apply eqm_samerepr. apply Z_of_bits_of_Z.
Qed.

Theorem xor_zero_one: xor zero one = one.
Proof. reflexivity. Qed.

Theorem xor_one_one: xor one one = zero.
Proof. reflexivity. Qed.

Theorem and_xor_distrib:
  forall x y z,
  and x (xor y z) = xor (and x y) (and x z).
Proof.
  intros; unfold and, xor, bitwise_binop.
  decEq. repeat rewrite unsigned_repr; auto with ints.
  apply Z_of_bits_exten; intros.
  repeat rewrite bits_of_Z_of_bits; auto.
  assert (forall a b c, a && (xorb b c) = xorb (a && b) (a && c)).
    destruct a; destruct b; destruct c; reflexivity.
  auto.
Qed.  

(** ** Properties of shifts and rotates *)

Lemma Z_of_bits_shift:
  forall n f,
  exists k,
  Z_of_bits n (fun i => f (i - 1)) =
    k * two_power_nat n + Z_shift_add (f (-1)) (Z_of_bits n f).
Proof.
  induction n; intros.
  simpl. rewrite two_power_nat_O. unfold Z_shift_add.
  exists (if f (-1) then (-1) else 0).
  destruct (f (-1)); omega.
  rewrite two_power_nat_S. simpl. 
  elim (IHn (fun i => f (i + 1))). intros k' EQ.
  replace (Z_of_bits n (fun i => f (i - 1 + 1)))
     with (Z_of_bits n (fun i => f (i + 1 - 1))) in EQ.
  rewrite EQ.
  change (-1 + 1) with 0.
  exists k'.
  unfold Z_shift_add; destruct (f (-1)); destruct (f 0); ring.
  apply Z_of_bits_exten; intros.
  decEq. omega.
Qed.

Lemma Z_of_bits_shifts:
  forall m f,
  0 <= m ->
  (forall i, i < 0 -> f i = false) ->
  eqm (Z_of_bits wordsize (fun i => f (i - m)))
      (two_p m * Z_of_bits wordsize f).
Proof.
  intros. pattern m. apply natlike_ind.
  apply eqm_refl2. transitivity (Z_of_bits wordsize f).
  apply Z_of_bits_exten; intros. decEq. omega.
  simpl two_p. omega.
  intros. rewrite two_p_S; auto.
  set (f' := fun i => f (i - x)).
  apply eqm_trans with (Z_of_bits wordsize (fun i => f' (i - 1))).
  apply eqm_refl2. apply Z_of_bits_exten; intros.
  unfold f'. decEq. omega.
  apply eqm_trans with (Z_shift_add (f' (-1)) (Z_of_bits wordsize f')).
  exact (Z_of_bits_shift wordsize f').
  unfold f'. unfold Z_shift_add. rewrite H0. 
  rewrite <- Zmult_assoc. apply eqm_mult. apply eqm_refl.
  apply H2. omega. assumption.
Qed.

Lemma shl_mul_two_p:
  forall x y,
  shl x y = mul x (repr (two_p (unsigned y))).
Proof.
  intros. unfold shl, mul. 
  apply eqm_samerepr. 
  eapply eqm_trans.
  apply Z_of_bits_shifts.
  generalize (unsigned_range y). omega.
  intros; apply bits_of_Z_below; auto.
  rewrite Zmult_comm. apply eqm_mult.
  apply Z_of_bits_of_Z. apply eqm_unsigned_repr.
Qed.

Theorem shl_zero: forall x, shl x zero = x.
Proof.
  intros. rewrite shl_mul_two_p. 
  change (repr (two_p (unsigned zero))) with one.
  apply mul_one.
Qed.

Theorem shl_mul:
  forall 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 shl_rolm:
  forall x n,
  ltu n (repr (Z_of_nat wordsize)) = true ->
  shl x n = rolm x n (shl mone n).
Proof.
  intros x n. unfold ltu. 
  rewrite unsigned_repr. case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
  unfold shl, rolm, rol, and, bitwise_binop.
  decEq. apply Z_of_bits_exten; intros.
  repeat rewrite unsigned_repr; auto with ints.
  repeat rewrite bits_of_Z_of_bits; auto. 
  case (zlt z (unsigned n)); intro LT2.
  assert (z - unsigned n < 0). omega.
  rewrite (bits_of_Z_below wordsize (unsigned x) _ H0).
  rewrite (bits_of_Z_below wordsize (unsigned mone) _ H0).
  symmetry. apply andb_b_false. 
  assert (z - unsigned n < Z_of_nat wordsize).
    generalize (unsigned_range n). omega. 
  replace (unsigned mone) with (two_power_nat wordsize - 1).
  rewrite bits_of_Z_mone. rewrite andb_b_true. decEq.
  rewrite Zmod_small. auto. omega. omega. 
  rewrite mone_max_unsigned. reflexivity. 
  discriminate.
  compute; intuition congruence. 
Qed.

Lemma bitwise_binop_shl:
  forall f x y n,
  f false false = false ->
  bitwise_binop f (shl x n) (shl y n) = shl (bitwise_binop f x y) n.
Proof.
  intros. unfold bitwise_binop, shl.
  decEq. repeat rewrite unsigned_repr; auto with ints.
  apply Z_of_bits_exten; intros.
  case (zlt (z - unsigned n) 0); intro.
  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
  repeat rewrite bits_of_Z_below; auto.
  rewrite bits_of_Z_below; auto.
  repeat rewrite bits_of_Z_of_bits; auto.
  generalize (unsigned_range n). omega.
Qed.

Lemma and_shl:
  forall x y n,
  and (shl x n) (shl y n) = shl (and x y) n.
Proof.
  unfold and; intros. apply bitwise_binop_shl. reflexivity.
Qed.

Theorem shru_rolm:
  forall x n,
  ltu n (repr (Z_of_nat wordsize)) = true ->
  shru x n = rolm x (sub (repr (Z_of_nat wordsize)) n) (shru mone n).
Proof.
  intros x n. unfold ltu. 
  rewrite unsigned_repr. 
  case (zlt (unsigned n) (Z_of_nat wordsize)); intros LT XX.
  unfold shru, rolm, rol, and, bitwise_binop.
  decEq. apply Z_of_bits_exten; intros.
  repeat rewrite unsigned_repr; auto with ints.
  repeat rewrite bits_of_Z_of_bits; auto. 
  unfold sub. 
  change (unsigned (repr (Z_of_nat wordsize)))
    with (Z_of_nat wordsize).
  rewrite unsigned_repr. 
  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro LT2.
  replace (unsigned mone) with (two_power_nat wordsize - 1).
  rewrite bits_of_Z_mone. rewrite andb_b_true.
  decEq. 
  replace (z - (Z_of_nat wordsize - unsigned n))
     with ((z + unsigned n) + (-1) * Z_of_nat wordsize).
  rewrite Z_mod_plus. symmetry. apply Zmod_small.
  generalize (unsigned_range n). omega. omega. omega. 
  generalize (unsigned_range n). omega. 
  reflexivity.
  rewrite (bits_of_Z_above wordsize (unsigned x) _ LT2).
  rewrite (bits_of_Z_above wordsize (unsigned mone) _ LT2).
  symmetry. apply andb_b_false.
  split. omega. apply Zle_trans with (Z_of_nat wordsize).
  generalize (unsigned_range n); omega. compute; intuition congruence.
  discriminate.
  split. omega. compute; intuition congruence.
Qed.

Lemma bitwise_binop_shru:
  forall f x y n,
  f false false = false ->
  bitwise_binop f (shru x n) (shru y n) = shru (bitwise_binop f x y) n.
Proof.
  intros. unfold bitwise_binop, shru.
  decEq. repeat rewrite unsigned_repr; auto with ints.
  apply Z_of_bits_exten; intros.
  case (zlt (z + unsigned n) (Z_of_nat wordsize)); intro.
  repeat rewrite bits_of_Z_of_bits; auto.
  generalize (unsigned_range n); omega.
  transitivity false. repeat rewrite bits_of_Z_of_bits; auto.
  repeat rewrite bits_of_Z_above; auto.
  rewrite bits_of_Z_above; auto.
Qed.

Lemma and_shru:
  forall x y n,
  and (shru x n) (shru y n) = shru (and x y) n.
Proof.
  unfold and; intros. apply bitwise_binop_shru. reflexivity.
Qed.

Theorem rol_zero:
  forall x,
  rol x zero = x.
Proof.
  intros. unfold rol. transitivity (repr (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x)))).
  decEq. 
  transitivity (repr (unsigned x)).
  decEq. apply eqm_small_eq. apply Z_of_bits_of_Z. 
  auto with ints. auto with ints. auto with ints. 
Qed.

Lemma bitwise_binop_rol:
  forall f x y n,
  bitwise_binop f (rol x n) (rol y n) = rol (bitwise_binop f x y) n.
Proof.
  intros. unfold bitwise_binop, rol.
  decEq. repeat (rewrite unsigned_repr; auto with ints).
  apply Z_of_bits_exten; intros.
  repeat rewrite bits_of_Z_of_bits; auto.
  apply Z_mod_lt. compute. auto. 
Qed.

Theorem rol_and:
  forall x y n,
  rol (and x y) n = and (rol x n) (rol y n).
Proof.
  intros. symmetry. unfold and. apply bitwise_binop_rol.
Qed.

Theorem rol_rol:
  forall x n m,
  rol (rol x n) m = rol x (modu (add n m) (repr (Z_of_nat wordsize))).
Proof.
  intros. unfold rol. decEq.
  repeat (rewrite unsigned_repr; auto with ints).
  apply Z_of_bits_exten; intros.
  repeat rewrite bits_of_Z_of_bits; auto.
  decEq. unfold modu, add. 
  set (W := Z_of_nat wordsize).
  set (M := unsigned m); set (N := unsigned n).
  assert (W > 0). compute; auto.
  assert (forall a, eqmod W a (unsigned (repr a))).
    intro. elim (eqm_unsigned_repr a). intros k EQ.
    red. exists (k * (modulus / W)). 
    replace (k * (modulus / W) * W) with (k * modulus). auto.
    rewrite <- Zmult_assoc. reflexivity.
  apply eqmod_mod_eq. auto.
  change (unsigned (repr W)) with W.
  apply eqmod_trans with (z - (N + M) mod W).
  apply eqmod_trans with ((z - M) - N).
  apply eqmod_sub. apply eqmod_sym. apply eqmod_mod. auto.
  apply eqmod_refl. 
  replace (z - M - N) with (z - (N + M)).
  apply eqmod_sub. apply eqmod_refl. apply eqmod_mod. auto.
  omega.
  apply eqmod_sub. apply eqmod_refl. 
  eapply eqmod_trans; [idtac|apply H1].
  eapply eqmod_trans; [idtac|apply eqmod_mod].
  apply eqmod_sym. eapply eqmod_trans; [idtac|apply eqmod_mod].
  apply eqmod_sym. apply H1. auto. auto. 
  apply Z_mod_lt. compute; auto.
Qed.

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

Theorem rolm_rolm:
  forall x n1 m1 n2 m2,
  rolm (rolm x n1 m1) n2 m2 =
    rolm x (modu (add n1 n2) (repr (Z_of_nat wordsize)))
           (and (rol m1 n2) m2).
Proof.
  intros.
  unfold rolm. rewrite rol_and. rewrite and_assoc. 
  rewrite rol_rol. reflexivity.
Qed.

Theorem rol_or:
  forall x y n,
  rol (or x y) n = or (rol x n) (rol y n).
Proof.
  intros. symmetry. unfold or. apply bitwise_binop_rol.
Qed.

Theorem or_rolm:
  forall 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.

(** ** Relation between shifts and powers of 2 *)

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

Lemma Z_bin_decomp_range:
  forall x n,
  0 <= x < 2 * n -> 0 <= snd (Z_bin_decomp x) < n.
Proof.
  intros. rewrite <- (Z_shift_add_bin_decomp x) in H.
  unfold Z_shift_add in H. destruct (fst (Z_bin_decomp x)); omega.
Qed.

Lemma Z_one_bits_powerserie:
  forall x, 0 <= x < modulus -> x = powerserie (Z_one_bits wordsize x 0).
Proof.
  assert (forall 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). omega. subst x. omega.
  rewrite two_power_nat_S in H0. simpl Z_one_bits.
  generalize (Z_shift_add_bin_decomp x).
  generalize (Z_bin_decomp_range x _ H0).
  case (Z_bin_decomp x). simpl. intros b y RANGE SHADD. 
  subst x. unfold Z_shift_add.
  destruct b. simpl powerserie. rewrite <- IHn. 
  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
  auto. omega. omega. auto.
  rewrite <- IHn. 
  rewrite two_p_is_exp. change (two_p 1) with 2. ring.
  auto. omega. omega. auto.
  intros. rewrite <- H. change (two_p 0) with 1. omega.
  omega. exact H0.
Qed.

Lemma Z_one_bits_range:
  forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < Z_of_nat wordsize.
Proof.
  assert (forall n x i j,
    In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n).
  induction n; simpl In.
  intros; elim H.
  intros x i j. destruct (Z_bin_decomp x). case b.
  rewrite inj_S. simpl. intros [A|B]. subst j. omega.
  generalize (IHn _ _ _ B). omega.
  intros B. rewrite inj_S. generalize (IHn _ _ _ B). omega.
  intros. generalize (H wordsize x 0 i H0). omega.
Qed.

Lemma is_power2_rng:
  forall n logn,
  is_power2 n = Some logn ->
  0 <= unsigned logn < Z_of_nat wordsize.
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 < Z_of_nat wordsize).
  apply H. auto with coqlib.
  rewrite unsigned_repr. auto.
  assert (Z_of_nat wordsize < max_unsigned). compute. auto.
  omega.
  intros; discriminate.
Qed.

Theorem is_power2_range:
  forall n logn,
  is_power2 n = Some logn -> ltu logn (repr (Z_of_nat wordsize)) = true.
Proof.
  intros. unfold ltu.
  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
  generalize (is_power2_rng _ _ H). 
  case (zlt (unsigned logn) (Z_of_nat wordsize)); intros.
  auto. omegaContradiction. 
Qed. 

Lemma is_power2_correct:
  forall 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. 
  assert (Z_of_nat wordsize < max_unsigned). compute; auto.
  omega. auto with coqlib. 
  intros; discriminate.
Qed.

Theorem mul_pow2:
  forall 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.

Lemma Z_of_bits_shift_rev:
  forall n f,
  (forall i, i >= Z_of_nat n -> f i = false) ->
  Z_of_bits n f = Z_shift_add (f 0) (Z_of_bits n (fun i => f(i + 1))).
Proof.
  induction n; intros.
  simpl. rewrite H. reflexivity. unfold Z_of_nat. omega.
  simpl. rewrite (IHn (fun i => f (i + 1))).
  reflexivity. 
  intros. apply H. rewrite inj_S. omega.
Qed.

Lemma Z_of_bits_shifts_rev:
  forall m f,
  0 <= m ->
  (forall i, i >= Z_of_nat wordsize -> f i = false) ->
  exists k,
  Z_of_bits wordsize f = k + two_p m * Z_of_bits wordsize (fun i => f(i + m))
  /\ 0 <= k < two_p m.
Proof.
  intros. pattern m. apply natlike_ind.
  exists 0. change (two_p 0) with 1. split.
  transitivity (Z_of_bits wordsize (fun i => f (i + 0))).
  apply Z_of_bits_exten. intros. decEq. omega.
  omega. omega.
  intros x POSx [k [EQ1 RANGE1]].
  set (f' := fun i => f (i + x)) in *.
  assert (forall i, i >= Z_of_nat wordsize -> f' i = false).
  intros. unfold f'. apply H0. omega.  
  generalize (Z_of_bits_shift_rev wordsize f' H1). intro.
  rewrite EQ1. rewrite H2. 
  set (z := Z_of_bits wordsize (fun i => f (i + Zsucc x))).
  replace (Z_of_bits wordsize (fun i => f' (i + 1))) with z.
  rewrite two_p_S.
  case (f' 0); unfold Z_shift_add.
  exists (k + two_p x). split. ring. omega. 
  exists k. split. ring. omega.
  auto. 
  unfold z. apply Z_of_bits_exten; intros. unfold f'.
  decEq. omega. 
  auto.
Qed.

Lemma shru_div_two_p:
  forall x y,
  shru x y = repr (unsigned x / two_p (unsigned y)).
Proof.
  intros. unfold shru. 
  set (x' := unsigned x). set (y' := unsigned y).
  elim (Z_of_bits_shifts_rev y' (bits_of_Z wordsize x')).
  intros k [EQ RANGE].
  replace (Z_of_bits wordsize (bits_of_Z wordsize x')) with x' in EQ.
  rewrite Zplus_comm in EQ. rewrite Zmult_comm in EQ.
  generalize (Zdiv_unique _ _ _ _ EQ RANGE). intros.
  rewrite H. auto.
  apply eqm_small_eq. apply eqm_sym. apply Z_of_bits_of_Z. 
  unfold x'. apply unsigned_range. 
  auto with ints.
  generalize (unsigned_range y). unfold y'. omega.
  intros. apply bits_of_Z_above. auto.
Qed.

Theorem shru_zero:
  forall x, shru x zero = x.
Proof.
  intros. rewrite shru_div_two_p. change (two_p (unsigned zero)) with 1.
  transitivity (repr (unsigned x)). decEq. apply Zdiv_unique with 0.
  omega. omega. auto with ints.
Qed.

Theorem shr_zero:
  forall x, shr x zero = x.
Proof.
  intros. unfold shr. change (two_p (unsigned zero)) with 1.
  replace (signed x / 1) with (signed x).
  apply repr_signed.
  symmetry. apply Zdiv_unique with 0. omega. omega. 
Qed.

Theorem divu_pow2:
  forall 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.

Lemma modu_divu_Euclid:
  forall 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:
  forall x y, y <> zero -> modu x y = sub x (mul (divu x y) y).
Proof.
  intros. 
  assert (forall 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.

Theorem mods_divs:
  forall x y, mods x y = sub x (mul (divs x y) y).
Proof.
  intros; unfold mods, sub, mul, divs.
  apply eqm_samerepr.
  unfold Zmod_round.
  apply eqm_sub. apply eqm_signed_unsigned. 
  apply eqm_unsigned_repr_r. 
  apply eqm_mult. auto with ints. apply eqm_signed_unsigned.
Qed.

Theorem divs_pow2:
  forall 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.

Theorem shrx_carry:
  forall x y,
  add (shr x y) (shr_carry x y) = shrx x y.
Proof.
  intros. unfold shr_carry. 
  rewrite sub_add_opp. rewrite add_permut. 
  rewrite add_neg_zero. apply add_zero.
Qed.

Lemma add_and:
  forall x y z,
  and y z = zero ->
  or y z = mone ->
  add (and x y) (and x z) = x.
Proof.
  intros. unfold add. transitivity (repr (unsigned x)); auto with ints.
  decEq. unfold and, bitwise_binop.
  repeat rewrite unsigned_repr; auto with ints.
  transitivity (Z_of_bits wordsize (bits_of_Z wordsize (unsigned x))).
  apply Z_of_bits_excl. intros. 
  assert (forall a b c, a && b && (a && c) = a && (b && c)).
    destruct a; destruct b; destruct c; reflexivity.
  rewrite H2. 
  replace (bits_of_Z wordsize (unsigned y) i &&
           bits_of_Z wordsize (unsigned z) i)
     with (bits_of_Z wordsize (unsigned (and y z)) i).
  rewrite H. change (unsigned zero) with 0. 
  rewrite bits_of_Z_zero. apply andb_b_false.
  unfold and, bitwise_binop. 
  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits. 
  reflexivity. auto. 
  intros. rewrite <- demorgan1. 
  replace (bits_of_Z wordsize (unsigned y) i ||
           bits_of_Z wordsize (unsigned z) i)
     with (bits_of_Z wordsize (unsigned (or y z)) i).
  rewrite H0. change (unsigned mone) with (two_power_nat wordsize - 1).
  rewrite bits_of_Z_mone; auto. apply andb_b_true.
  unfold or, bitwise_binop. 
  rewrite unsigned_repr; auto with ints. rewrite bits_of_Z_of_bits; auto.
  apply eqm_small_eq; auto with ints. apply Z_of_bits_of_Z. 
Qed.

(** To prove equalities involving modulus and bitwise ``and'', we need to
  show complicated integer equalities involving one integer variable
  that ranges between 0 and 31.  Rather than proving these equalities,
  we ask Coq to check them by computing the 32 values of the 
  left and right-hand sides and checking that they are equal.
  This is an instance of proving by reflection. *)

Section REFLECTION.

Variables (f g: int -> int).

Fixpoint check_equal_on_range (n: nat) : bool :=
  match n with
  | O => true
  | S n => if eq (f (repr (Z_of_nat n))) (g (repr (Z_of_nat n)))
           then check_equal_on_range n
           else false
  end.

Lemma check_equal_on_range_correct:
  forall n, 
  check_equal_on_range n = true ->
  forall z, 0 <= z < Z_of_nat n -> f (repr z) = g (repr z).
Proof.
  induction n.
  simpl; intros;  omegaContradiction.
  simpl check_equal_on_range.
  set (fn := f (repr (Z_of_nat n))).
  set (gn := g (repr (Z_of_nat n))).
  generalize (eq_spec fn gn).
  case (eq fn gn); intros.
  rewrite inj_S in H1. 
  assert (0 <= z < Z_of_nat n \/ z = Z_of_nat n). omega.
  elim H2; intro.
  apply IHn. auto. auto.
  subst z; auto. 
  discriminate. 
Qed.

Lemma equal_on_range:
  check_equal_on_range wordsize = true ->
  forall n, 0 <= unsigned n < Z_of_nat wordsize ->
  f n = g n.
Proof.
  intros. replace n with (repr (unsigned n)). 
  apply check_equal_on_range_correct with wordsize; auto.
  apply repr_unsigned.
Qed.

End REFLECTION.

(** Here are the three equalities that we prove by reflection. *)

Remark modu_and_masks_1:
  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
  rol (shru mone logn) logn = shl mone logn.
Proof.
  apply (equal_on_range
          (fun l => rol (shru mone l) l)
          (fun l => shl mone l)).
  vm_compute; auto.
Qed.

Remark modu_and_masks_2:
  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
  and (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = zero.
Proof.
  apply (equal_on_range
          (fun l => and (shl mone l)
                        (sub (repr (two_p (unsigned l))) one))
          (fun l => zero)).
  vm_compute; auto.
Qed.

Remark modu_and_masks_3:
  forall logn, 0 <= unsigned logn < Z_of_nat wordsize ->
  or (shl mone logn) (sub (repr (two_p (unsigned logn))) one) = mone.
Proof.
  apply (equal_on_range
          (fun l => or (shl mone l)
                        (sub (repr (two_p (unsigned l))) one))
          (fun l => mone)).
  vm_compute; auto.
Qed.

Theorem modu_and:
  forall 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.
  assert (n <> zero). 
    red; intro. subst n. change (unsigned zero) with 0 in H0.
    assert (two_p (unsigned logn) > 0). apply two_p_gt_ZERO. omega.
    omegaContradiction.
  generalize (modu_divu_Euclid x n H2); intro.
  assert (forall a b c, add a b = add a c -> b = c).
    intros. assert (sub (add a b) a = sub (add a c) a). congruence.
    repeat rewrite sub_add_l in H5. repeat rewrite sub_idem in H5.
    rewrite add_commut in H5; rewrite add_zero in H5.
    rewrite add_commut in H5; rewrite add_zero in H5.
    auto.
  apply H4 with (mul (divu x n) n).
  rewrite <- H3. 
  rewrite (divu_pow2 x n logn H). 
  rewrite (mul_pow2 (shru x logn) n logn H). 
  rewrite shru_rolm. rewrite shl_rolm. rewrite rolm_rolm.
  rewrite sub_add_opp. rewrite add_assoc. 
  replace (add (neg logn) logn) with zero.
  rewrite add_zero.
  change (modu (repr (Z_of_nat wordsize)) (repr (Z_of_nat wordsize)))
    with zero.
  rewrite rolm_zero. 
  symmetry.
  replace n with (repr (two_p (unsigned logn))).
  rewrite modu_and_masks_1; auto.
  rewrite and_idem.
  apply add_and. apply modu_and_masks_2; auto. apply modu_and_masks_3; auto.
  transitivity (repr (unsigned n)). decEq. auto. auto with ints.
  rewrite add_commut. rewrite add_neg_zero. auto.
  unfold ltu. apply zlt_true. 
  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
  omega.
  unfold ltu. apply zlt_true. 
  change (unsigned (repr (Z_of_nat wordsize))) with (Z_of_nat wordsize).
  omega.
Qed.

(** ** Properties of integer zero extension and sign extension. *)

Theorem cast8unsigned_and:
  forall x, cast8unsigned x = and x (repr 255).
Proof.
  intros; unfold cast8unsigned. 
  change (repr (unsigned x mod 256)) with (modu x (repr 256)).
  change (repr 255) with (sub (repr 256) one).
  apply modu_and with (repr 8). reflexivity.
Qed.

Theorem cast16unsigned_and:
  forall x, cast16unsigned x = and x (repr 65535).
Proof.
  intros; unfold cast16unsigned. 
  change (repr (unsigned x mod 65536)) with (modu x (repr 65536)).
  change (repr 65535) with (sub (repr 65536) one).
  apply modu_and with (repr 16). reflexivity.
Qed.

Lemma eqmod_256_unsigned_repr:
  forall a, eqmod 256 a (unsigned (repr a)).
Proof.
  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
  intros [k EQ]. exists (k * (modulus / 256)). 
  replace (k * (modulus / 256) * 256)  
     with (k * ((modulus / 256) * 256)).
  exact EQ. ring. 
Qed.

Lemma eqmod_65536_unsigned_repr:
  forall a, eqmod 65536 a (unsigned (repr a)).
Proof.
  intros. generalize (eqm_unsigned_repr a). unfold eqm, eqmod.
  intros [k EQ]. exists (k * (modulus / 65536)). 
  replace (k * (modulus / 65536) * 65536)  
     with (k * ((modulus / 65536) * 65536)).
  exact EQ. ring. 
Qed.

Theorem cast8_signed_unsigned:
  forall n, cast8signed (cast8unsigned n) = cast8signed n.
Proof.
  intros; unfold cast8signed, cast8unsigned.
  set (N := unsigned n).
  rewrite unsigned_repr. 
  replace ((N mod 256) mod 256) with (N mod 256).
  auto.
  symmetry. apply Zmod_small. apply Z_mod_lt. omega.
  assert (0 <= N mod 256 < 256). apply Z_mod_lt. omega.
  assert (256 < max_unsigned). compute; auto.
  omega.
Qed.

Theorem cast8_unsigned_signed:
  forall n, cast8unsigned (cast8signed n) = cast8unsigned n.
Proof.
  intros; unfold cast8signed, cast8unsigned.
  set (N := unsigned n mod 256).
  assert (0 <= N < 256). unfold N; apply Z_mod_lt. omega.
  assert (N mod 256 = N). apply Zmod_small. auto.
  assert (256 <= max_unsigned). compute; congruence.
  decEq. 
  case (zlt N 128); intro.
  rewrite unsigned_repr. auto. omega.
  transitivity (N mod 256); auto. 
  apply eqmod_mod_eq. omega. 
  apply eqmod_trans with (N - 256). apply eqmod_sym. apply eqmod_256_unsigned_repr.
  assert (eqmod 256 (N - 256) (N - 0)).
    apply eqmod_sub. apply eqmod_refl. 
    red. exists 1; reflexivity.
  replace (N - 0) with N in H2. auto. omega.
Qed.

Theorem cast16_unsigned_signed:
  forall n, cast16unsigned (cast16signed n) = cast16unsigned n.
Proof.
  intros; unfold cast16signed, cast16unsigned.
  set (N := unsigned n mod 65536).
  assert (0 <= N < 65536). unfold N; apply Z_mod_lt. omega.
  assert (N mod 65536 = N). apply Zmod_small. auto.
  assert (65536 <= max_unsigned). compute; congruence.
  decEq. 
  case (zlt N 32768); intro.
  rewrite unsigned_repr. auto. omega.
  transitivity (N mod 65536); auto. 
  apply eqmod_mod_eq. omega. 
  apply eqmod_trans with (N - 65536). apply eqmod_sym. apply eqmod_65536_unsigned_repr.
  assert (eqmod 65536 (N - 65536) (N - 0)).
    apply eqmod_sub. apply eqmod_refl. 
    red. exists 1; reflexivity.
  replace (N - 0) with N in H2. auto. omega.
Qed.

Theorem cast8_unsigned_idem:
  forall n, cast8unsigned (cast8unsigned n) = cast8unsigned n.
Proof.
  intros. repeat rewrite cast8unsigned_and. 
  rewrite and_assoc. reflexivity. 
Qed.

Theorem cast16_unsigned_idem:
  forall n, cast16unsigned (cast16unsigned n) = cast16unsigned n.
Proof.
  intros. repeat rewrite cast16unsigned_and. 
  rewrite and_assoc. reflexivity. 
Qed.

Theorem cast8_signed_idem:
  forall n, cast8signed (cast8signed n) = cast8signed n.
Proof.
  intros; unfold cast8signed.
  set (N := unsigned n mod 256).
  assert (256 < max_unsigned). compute; auto.
  assert (0 <= N < 256). unfold N. apply Z_mod_lt. omega. 
  case (zlt N 128); intro.
  assert (unsigned (repr N) = N).
    apply unsigned_repr. omega.
  rewrite H1.
  replace (N mod 256) with N. apply zlt_true. auto.
  symmetry. apply Zmod_small. auto.
  set (M := (unsigned (repr (N - 256)) mod 256)).
  assert (M = N).
    unfold M, N. apply eqmod_mod_eq. omega. 
    apply eqmod_trans with (unsigned n mod 256 - 256).
    apply eqmod_sym. apply eqmod_256_unsigned_repr. 
    apply eqmod_trans with (unsigned n - 0).
    apply eqmod_sub. 
    apply eqmod_sym. apply eqmod_mod. omega.
    unfold eqmod. exists 1; omega.
    apply eqmod_refl2. omega.
  rewrite H1. rewrite zlt_false; auto.
Qed.

Theorem cast16_signed_idem:
  forall n, cast16signed (cast16signed n) = cast16signed n.
Proof.
  intros; unfold cast16signed.
  set (N := unsigned n mod 65536).
  assert (65536 < max_unsigned). compute; auto.
  assert (0 <= N < 65536). unfold N. apply Z_mod_lt. omega. 
  case (zlt N 32768); intro.
  assert (unsigned (repr N) = N).
    apply unsigned_repr. omega.
  rewrite H1.
  replace (N mod 65536) with N. apply zlt_true. auto.
  symmetry. apply Zmod_small. auto.
  set (M := (unsigned (repr (N - 65536)) mod 65536)).
  assert (M = N).
    unfold M, N. apply eqmod_mod_eq. omega. 
    apply eqmod_trans with (unsigned n mod 65536 - 65536).
    apply eqmod_sym. apply eqmod_65536_unsigned_repr. 
    apply eqmod_trans with (unsigned n - 0).
    apply eqmod_sub. 
    apply eqmod_sym. apply eqmod_mod. omega.
    unfold eqmod. exists 1; omega.
    apply eqmod_refl2. omega.
  rewrite H1. rewrite zlt_false; auto.
Qed.

Theorem cast8_signed_equal_if_unsigned_equal:
  forall x y, 
  cast8unsigned x = cast8unsigned y ->
  cast8signed x = cast8signed y.
Proof.
  unfold cast8unsigned, cast8signed; intros until y.
  set (x' := unsigned x mod 256).
  set (y' := unsigned y mod 256).
  intro. 
  assert (eqm x' y').
    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
  assert (forall z, 0 <= z mod 256 < modulus).
    intros. 
    assert (0 <= z mod 256 < 256). apply Z_mod_lt. omega.
    assert (256 <= modulus). compute. congruence.
    omega.
  assert (x' = y').
    apply eqm_small_eq; unfold x', y'; auto. 
  rewrite H2. auto.
Qed.

Theorem cast16_signed_equal_if_unsigned_equal:
  forall x y, 
  cast16unsigned x = cast16unsigned y ->
  cast16signed x = cast16signed y.
Proof.
  unfold cast16unsigned, cast16signed; intros until y.
  set (x' := unsigned x mod 65536).
  set (y' := unsigned y mod 65536).
  intro. 
  assert (eqm x' y').
    apply eqm_trans with (unsigned (repr x')). apply eqm_unsigned_repr.
    rewrite H. apply eqm_sym. apply eqm_unsigned_repr.
  assert (forall z, 0 <= z mod 65536 < modulus).
    intros. 
    assert (0 <= z mod 65536 < 65536). apply Z_mod_lt. omega.
    assert (65536 <= modulus). compute. congruence.
    omega.
  assert (x' = y').
    apply eqm_small_eq; unfold x', y'; auto. 
  rewrite H2. auto.
Qed.

(** ** Properties of [one_bits] (decomposition in sum of powers of two) *)

Opaque Z_one_bits. (* Otherwise, next Qed blows up! *)

Theorem one_bits_range:
  forall x i, In i (one_bits x) -> ltu i (repr (Z_of_nat wordsize)) = true.
Proof.
  intros. unfold one_bits in H.
  elim (list_in_map_inv _ _ _ H). intros i0 [EQ IN].
  subst i. unfold ltu. apply zlt_true. 
  generalize (Z_one_bits_range _ _ IN). intros.
  assert (0 <= Z_of_nat wordsize <= max_unsigned).
    compute. intuition congruence.
  repeat rewrite unsigned_repr; omega.
Qed.

Fixpoint int_of_one_bits (l: list int) : int :=
  match l with
  | nil => zero
  | a :: b => add (shl one a) (int_of_one_bits b)
  end.

Theorem one_bits_decomp:
  forall x, x = int_of_one_bits (one_bits x).
Proof.
  intros. 
  transitivity (repr (powerserie (Z_one_bits wordsize (unsigned x) 0))).
  transitivity (repr (unsigned x)).
  auto with ints. decEq. apply Z_one_bits_powerserie.
  auto with ints.
  unfold one_bits. 
  generalize (Z_one_bits_range (unsigned x)).
  generalize (Z_one_bits wordsize (unsigned x) 0).
  induction l.
  intros; reflexivity.
  intros; simpl. rewrite <- IHl. unfold add. apply eqm_samerepr.
  apply eqm_add. rewrite shl_mul_two_p. rewrite mul_commut. 
  rewrite mul_one. apply eqm_unsigned_repr_r. 
  rewrite unsigned_repr. auto with ints.
  generalize (H a (in_eq _ _)). 
  assert (Z_of_nat wordsize < max_unsigned). compute; auto. omega.
  auto with ints.
  intros; apply H; auto with coqlib.
Qed.

(** ** Properties of comparisons *)

Theorem negate_cmp:
  forall c x y, cmp (negate_comparison c) x y = negb (cmp c x y).
Proof.
  intros. destruct c; simpl; try rewrite negb_elim; auto.
Qed.

Theorem negate_cmpu:
  forall c x y, cmpu (negate_comparison c) x y = negb (cmpu c x y).
Proof.
  intros. destruct c; simpl; try rewrite negb_elim; auto.
Qed.

Theorem swap_cmp:
  forall c x y, cmp (swap_comparison c) x y = cmp c y x.
Proof.
  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
Qed.

Theorem swap_cmpu:
  forall c x y, cmpu (swap_comparison c) x y = cmpu c y x.
Proof.
  intros. destruct c; simpl; auto. apply eq_sym. decEq. apply eq_sym.
Qed.

Lemma translate_eq:
  forall x y d,
  eq (add x d) (add y d) = eq x y.
Proof.
  intros. unfold eq. case (zeq (unsigned x) (unsigned y)); intro.
  unfold add. rewrite e. apply zeq_true.
  apply zeq_false. unfold add. red; intro. apply n. 
  apply eqm_small_eq; auto with ints.
  replace (unsigned x) with ((unsigned x + unsigned d) - unsigned d).
  replace (unsigned y) with ((unsigned y + unsigned d) - unsigned d).
  apply eqm_sub. apply eqm_trans with (unsigned (repr (unsigned x + unsigned d))).
  eauto with ints. apply eqm_trans with (unsigned (repr (unsigned y + unsigned d))).
  eauto with ints. eauto with ints. eauto with ints.
  omega. omega.
Qed.

Lemma translate_lt:
  forall x y d,
  min_signed <= signed x + signed d <= max_signed ->
  min_signed <= signed y + signed d <= max_signed ->
  lt (add x d) (add y d) = lt x y.
Proof.
  intros. repeat rewrite add_signed. unfold lt.
  repeat rewrite signed_repr; auto. case (zlt (signed x) (signed y)); intro.
  apply zlt_true. omega.
  apply zlt_false. omega.
Qed.

Theorem translate_cmp:
  forall c x y d,
  min_signed <= signed x + signed d <= max_signed ->
  min_signed <= signed y + signed d <= max_signed ->
  cmp c (add x d) (add y d) = cmp c x y.
Proof.
  intros. unfold cmp.
  rewrite translate_eq. repeat rewrite translate_lt; auto.
Qed.  

Theorem notbool_isfalse_istrue:
  forall x, is_false x -> is_true (notbool x).
Proof.
  unfold is_false, is_true, notbool; intros; subst x. 
  simpl. discriminate.
Qed.

Theorem notbool_istrue_isfalse:
  forall x, is_true x -> is_false (notbool x).
Proof.
  unfold is_false, is_true, notbool; intros.
  generalize (eq_spec x zero). case (eq x zero); intro.
  contradiction. auto.
Qed.

End Int.