Module IntFacts

Require Import Coqlib.
Require Import Axioms.
Require Import Integers.
Require Import Floats.
Require Import Psatz.

Lemma Forall_app:
  forall A P (l1 l2:list A),
    Forall P l1 ->
    Forall P l2 ->
    Forall P (l1 ++ l2).

Proof.

  intros.
  apply Forall_forall.
  intros.
  apply in_app in H1; intuition.
  eapply Forall_forall in H ; eauto.
  eapply Forall_forall in H0 ; eauto.
Qed.

Ltac assert_val val :=
  match goal with
      |- context [if ?a then _ else _] => let x:= fresh in assert (x: a=val);[|rewrite x in *; clear x]
  end.

Ltac inv' :=
  match goal with
      H: ?a _ = ?a _ |- _ => inv H; inv'
    | _ => idtac
end.

Ltac destr :=
  try destr_cond_match; simpl in *; intuition try congruence.

Ltac des t :=
  destruct t eqn:?; subst; simpl in *; intuition try congruence.

Ltac destr_no_dep :=
  destr; repeat match goal with
                    H: _ = left _ |- _ => clear H
                  | H: _ = right _ |- _ => clear H
                end.

Lemma shl_zero_l:
  forall i,
    Int.shl Int.zero i = Int.zero.

Proof.

  intros.
  apply Int.same_bits_eq.
  intros.
  rewrite Int.bits_shl; simpl; auto.
  repeat rewrite Int.bits_zero.
  destr.
Qed.

Ltac solve_int :=
  repeat
    match goal with
      | |- context [Int.shl _ (Int.repr 0)] => rewrite Int.shl_zero
      | |- context [Int.shl Int.zero _] => rewrite shl_zero_l
      | |- context [Int.add Int.zero _] => rewrite Int.add_zero_l
      | |- context [Int.shru (Int.shl ?i (Int.repr ?n)) (Int.repr ?n)] =>
        change n with (Int.zwordsize - (Int.zwordsize - n));
          rewrite <- Int.zero_ext_shru_shl by (unfold Int.zwordsize; simpl; omega)
      | |- context [Int.shru (Int.shl ?i (Int.repr ?n)) (Int.repr ?m)] =>
        change (Int.shru (Int.shl i (Int.repr n)) (Int.repr m)) with
        (Int.shru (Int.shl i (Int.repr (Int.zwordsize - (Int.zwordsize - n)))) (Int.add (Int.repr n) (Int.sub (Int.repr m) (Int.repr n))));
          rewrite <- Int.shru_shru by (vm_compute; auto);
          rewrite <- Int.zero_ext_shru_shl by (unfold Int.zwordsize; simpl; omega)
      | |- context [Int.sub (Int.repr ?i) (Int.repr ?j)] =>
        change (Int.sub (Int.repr i) (Int.repr j)) with (Int.repr (i - j)); simpl
      | |- context [Int.add (Int.repr ?i) (Int.repr ?j)] =>
        change (Int.add (Int.repr i) (Int.repr j)) with (Int.repr (i + j)); simpl
      | |- context [Int.testbit (Int.add _ _) _] => rewrite Int.add_is_or; simpl; auto; try omega
      | |- context [Int.testbit (Int.and _ _) _] => rewrite Int.bits_and; simpl; auto
      | |- context [Int.testbit (Int.or _ _) _] => rewrite Int.bits_or; simpl; auto; try omega; [idtac]
      | |- context [Int.testbit (Int.shl _ _) _] => rewrite Int.bits_shl; simpl; auto; try omega; [idtac]
      | |- context [Int.testbit (Int.shru _ _) _] => rewrite Int.bits_shru; simpl; auto; try omega; [idtac]
      | |- context [Int.testbit (Int.zero_ext _ _) _] => rewrite Int.bits_zero_ext; simpl
      | |- context [Int.testbit (Int.sign_ext _ _) _] => f_equal; apply Int.sign_ext_equal_if_zero_equal; try omega
      | H: context[Int.unsigned (Int.repr _)]|- _ => rewrite Int.unsigned_repr in H by (unfold Int.max_unsigned; simpl; omega)
      | |- context[Int.unsigned (Int.repr _)] => rewrite Int.unsigned_repr by (unfold Int.max_unsigned; simpl; omega)
      | |- context [_ || false] => rewrite orb_false_r
      | |- context [_ && false] => rewrite andb_false_r
      | |- context [Int.testbit Int.zero ?i] => rewrite Int.bits_zero
      | |- context [?n - ?i + ?i] => replace (n - i + i) with n by (rewrite Z.sub_simpl_r; auto)
      | |- Int.testbit ?e ?i = Int.testbit ?e ?j => f_equal; omega
      | |- @eq int _ _ => apply Int.same_bits_eq; simpl; intros
      | |- _ => destr; repeat match goal with
                                | H: _ = left _ |- _ => clear H
                                | H: _ = right _ |- _ => clear H
                              end; try omega
      | |- _ => progress simpl
    end.

Lemma shl_zero_r_64:
  forall i,
    Int64.shl' i (Int.repr 0) = i.

Proof.

  intros.
  apply Int64.same_bits_eq; intros; auto.
  rewrite Int64.bits_shl'; simpl; auto; try omega.
  rewrite Int.unsigned_repr by (unfold Int.max_unsigned; simpl; omega).
  destr; try omega.
  f_equal; omega.
Qed.

Lemma shl_zero_l_64:
forall i,
Int64.shl' Int64.zero i = Int64.zero.

Proof.

  intros.
  apply Int64.same_bits_eq; intros; auto.
  rewrite Int64.bits_shl'; simpl; auto; try omega.
  repeat rewrite Int64.bits_zero.
  destr; try omega.
Qed.

Lemma shru'_shru:
  forall l i,
    0 <= Int.unsigned i <= 64 ->
    Int64.shru' l i = Int64.shru l (Int64.repr (Int.unsigned i)).

Proof.

  intros.
  unfold Int64.shru', Int64.shru.
  f_equal.
  f_equal.
  rewrite Int64.unsigned_repr; auto.
  unfold Int64.max_unsigned; simpl; omega.
Qed.

Lemma shl'_shl:
  forall l i,
    0 <= Int.unsigned i <= 64 ->
    Int64.shl' l i = Int64.shl l (Int64.repr (Int.unsigned i)).

Proof.

  intros.
  unfold Int64.shl', Int64.shl.
  f_equal.
  f_equal.
  rewrite Int64.unsigned_repr; auto.
  unfold Int64.max_unsigned; simpl; omega.
Qed.

Ltac solve_long :=
  repeat
    match goal with
      | |- context [Int64.shl' _ (Int.repr 0)] => rewrite shl_zero_r_64
      | |- context [Int64.shl' Int64.zero _] => rewrite shl_zero_l_64
      | |- context [Int64.add Int64.zero _] => rewrite Int64.add_zero_l
      | |- context [Int64.mul Int64.zero _] => rewrite Int64.mul_commut; rewrite Int64.mul_zero
      | |- context [Int64.shru (Int64.shl ?i (Int64.repr ?n)) (Int64.repr ?n)] =>
        change n with (Int64.zwordsize - (Int64.zwordsize - n));
          rewrite <- Int64.zero_ext_shru_shl by (unfold Int64.zwordsize; simpl; omega)
      | |- context [Int64.shru (Int64.shl ?i (Int64.repr ?n)) (Int64.repr ?m)] =>
        change (Int64.shru (Int64.shl i (Int64.repr n)) (Int64.repr m)) with
        (Int64.shru (Int64.shl i (Int64.repr (Int64.zwordsize - (Int64.zwordsize - n)))) (Int64.add (Int64.repr n) (Int64.sub (Int64.repr m) (Int64.repr n))));
          rewrite <- Int64.shru_shru by (vm_compute; auto);
          rewrite <- Int64.zero_ext_shru_shl by (unfold Int64.zwordsize; simpl; omega)
      | |- context [Int64.sub (Int64.repr ?i) (Int64.repr ?j)] =>
        change (Int64.sub (Int64.repr i) (Int64.repr j)) with (Int64.repr (i - j)); simpl
      | |- context [Int64.add (Int64.repr ?i) (Int64.repr ?j)] =>
        change (Int64.add (Int64.repr i) (Int64.repr j)) with (Int64.repr (i + j)); simpl
      | |- context [Int64.testbit (Int64.and _ _) _] => rewrite Int64.bits_and; simpl; auto
      | |- context [Int64.testbit (Int64.or _ _) _] => rewrite Int64.bits_or; simpl; auto; try omega; [idtac]
      | |- context [Int64.testbit (Int64.shl _ _) _] => rewrite Int64.bits_shl; simpl; auto; try omega; [idtac]
      | |- context [Int64.testbit (Int64.shru _ _) _] => rewrite Int64.bits_shru; simpl; auto; try omega; [idtac]
      | |- context [Int64.testbit (Int64.zero_ext _ _) _] => rewrite Int64.bits_zero_ext; simpl
      | |- context [Int64.testbit (Int64.sign_ext _ _) _] => f_equal; apply Int64.sign_ext_equal_if_zero_equal; try omega; [idtac]
      | H: context[Int64.unsigned (Int64.repr _)]|- _ => rewrite Int64.unsigned_repr in H by (unfold Int64.max_unsigned; simpl; omega)
      | |- context[Int64.unsigned (Int64.repr _)] => rewrite Int64.unsigned_repr by (unfold Int64.max_unsigned; simpl; omega)
      | H: context[Int.unsigned (Int.repr _)]|- _ => rewrite Int.unsigned_repr in H by (unfold Int.max_unsigned; simpl; omega)
      | |- context[Int.unsigned (Int.repr _)] => rewrite Int.unsigned_repr by (unfold Int.max_unsigned; simpl; omega)
      | |- context [_ || false] => rewrite orb_false_r
      | |- context [_ && false] => rewrite andb_false_r
      | |- context [Int64.testbit Int64.zero ?i] => rewrite Int64.bits_zero
      | |- context [?n - ?i + ?i] => replace (n - i + i) with n by (rewrite Z.sub_simpl_r; auto)
      | |- Int64.testbit ?e ?i = Int64.testbit ?e ?j => f_equal; omega
      | |- @eq int64 _ _ => apply Int64.same_bits_eq; simpl; intros
      | |- _ => destr; repeat match goal with
                                | H: _ = left _ |- _ => clear H
                                | H: _ = right _ |- _ => clear H
                              end; try omega
      | |- _ => progress simpl
    end.

Lemma add_is_or_8:
  forall i i0,
    Int.add (Int.shl i0 (Int.repr 8)) (Int.zero_ext 8 i) =
    Int.or (Int.shl i0 (Int.repr 8)) (Int.zero_ext 8 i).

Proof.

  intros.
  rewrite Int.add_is_or; auto.
  apply Int.same_bits_eq; intros.
  rewrite Int.bits_zero.
  rewrite Int.bits_and; auto.
  rewrite Int.bits_shl; auto.
  destr_no_dep.
  rewrite Int.bits_zero_ext; auto.
  destr_no_dep.
  rewrite Int.unsigned_repr in g by (unfold Int.max_unsigned; simpl; omega).
  omega.
  rewrite andb_false_r; auto.
Qed.

Lemma add_is_or_16:
  forall i i0,
    Int.add (Int.shl i0 (Int.repr 8)) (Int.shru (Int.zero_ext 16 i) (Int.repr 8)) =
    Int.or (Int.shl i0 (Int.repr 8)) (Int.shru (Int.zero_ext 16 i) (Int.repr 8)).

Proof.

  intros.
  rewrite Int.add_is_or; auto.
  apply Int.same_bits_eq; intros.
  rewrite Int.bits_zero.
  rewrite Int.bits_and; auto.
  rewrite Int.bits_shl; auto.
  rewrite Int.bits_shru; auto.
  rewrite Int.bits_zero_ext; auto.
  repeat destr_no_dep;
    try rewrite andb_false_r; auto.
  rewrite Int.unsigned_repr in * by (unfold Int.max_unsigned; simpl; omega).
  omega.
  rewrite Int.unsigned_repr in * by (unfold Int.max_unsigned; simpl; omega).
  omega.
Qed.

Lemma add_is_or_24:
  forall i,
    Int.add
      (Int.shl (Int.shru i (Int.repr 24))
                (Int.repr 8)) (Int.shru (Int.zero_ext 24 i) (Int.repr 16)) =
    Int.or
      (Int.shl (Int.shru i (Int.repr 24))
                (Int.repr 8)) (Int.shru (Int.zero_ext 24 i) (Int.repr 16)).

Proof.

  intros.
  rewrite Int.add_is_or; auto.
  apply Int.same_bits_eq; intros.
  rewrite Int.bits_zero.
  rewrite Int.bits_and; auto.
  rewrite Int.bits_shl; auto.
  destr_no_dep.
  rewrite Int.unsigned_repr in * by (unfold Int.max_unsigned; simpl; omega).
  repeat rewrite Int.bits_shru; auto; try omega.
  repeat rewrite Int.unsigned_repr in * by (unfold Int.max_unsigned; simpl; omega).
  repeat destr_no_dep;
    try rewrite andb_false_r; auto.
  rewrite Int.bits_zero_ext; simpl; auto; try omega.
  destr_no_dep; try omega.
  apply andb_false_r.
Qed.

Lemma float_bits_of_double_inj:
forall f f', Float.to_bits f = Float.to_bits f' -> f = f'.

Proof.

  intros.
  apply (f_equal Float.of_bits) in H.
  repeat rewrite Float.of_to_bits in H; auto.
Qed.

Lemma float_bits_of_single_inj:
forall f f',
Float32.to_bits f = Float32.to_bits f' -> f = f'.

Proof.

  intros.
  apply (f_equal Float32.of_bits) in H.
  repeat rewrite Float32.of_to_bits in H; auto.
Qed.

Lemma Forall_rev:
  forall A P (l:list A),
    Forall P (rev l) ->
    Forall P l.

Proof.

  intros.
  apply Forall_forall.
  intros.
  eapply Forall_forall in H ; eauto.
  apply -> in_rev; auto.
Qed.

Lemma proof_irr_int64:
  forall (i i0: int64),
    match i with
        Int64.mkint int64val _ => int64val
    end =
    match i0 with
        Int64.mkint int64val _ => int64val
    end ->
    i = i0.

Proof.

  intros; destruct i; destruct i0; subst.
  f_equal.
  apply proof_irr.
Qed.

Lemma proof_irr_int:
  forall (i i0: int),
    match i with
        Int.mkint intval _ => intval
    end =
    match i0 with
        Int.mkint intval _ => intval
    end ->
    i = i0.

Proof.

  intros; destruct i; destruct i0; subst.
  f_equal.
  apply proof_irr.
Qed.

Lemma int_zwordsize:
Int.zwordsize = 32.

Proof.

reflexivity.
Qed.

Lemma int64_zwordsize:
Int64.zwordsize = 64.

Proof.

reflexivity.
Qed.

Lemma byte_zwordsize:
Byte.zwordsize = 8.

Proof.

reflexivity. Qed.

Lemma zero_ext_16_undef:
  forall i i0,
    (Int.add
       (Int.shl
          (Int.add (Int.shl Int.zero (Int.repr 8))
                   (Int.shru (Int.shl i (Int.repr 16)) (Int.repr 24)))
          (Int.repr 8)) (Int.shru (Int.shl i0 (Int.repr 24)) (Int.repr 24))) =
    (Int.zero_ext 16
                  (Int.add
                     (Int.shl
                        (Int.add (Int.shl Int.zero (Int.repr 8))
                                 (Int.shru (Int.shl i (Int.repr 16)) (Int.repr 24)))
                        (Int.repr 8))
                     (Int.shru (Int.shl i0 (Int.repr 24)) (Int.repr 24)))).

Proof.

intros.
solve_int.
Qed.

Lemma zero_ext_16_add_shl_shru:
  forall i0,
    Int.add
      (Int.shl
         (Int.add (Int.shl Int.zero (Int.repr 8))
                  (Int.shru (Int.shl i0 (Int.repr 16)) (Int.repr 24)))
         (Int.repr 8)) (Int.shru (Int.shl i0 (Int.repr 24)) (Int.repr 24)) =
    Int.zero_ext 16 i0.

Proof.

intros.
solve_int.
Qed.

Lemma list_forall2_sym:
  forall {A} (P: A -> A -> Prop)
         (Psym: forall a b, P a b -> P b a)
         la lb,
    list_forall2 P la lb ->
    list_forall2 P lb la.

Proof.

  intros.
  induction H.
  constructor.
  constructor; auto.
Qed.

Lemma list_forall2_rev:
  forall {A} (P:A -> A -> Prop) (l l': list A),
    list_forall2 P l l' ->
    list_forall2 P (rev l) (rev l').

Proof.

  induction l; intros.
  - inv H. simpl; constructor.
  - simpl.
    inv H.
    apply IHl in H4.
    simpl.
    apply list_forall2_app; auto.
    constructor; auto.
    constructor.
Qed.

Lemma list_forall2_rev':
  forall {A} (P: A -> A -> Prop) l1 l2,
    list_forall2 P (rev l1) (rev l2) ->
    list_forall2 P l1 l2.

Proof.

  intros.
  apply list_forall2_rev in H.
  rewrite ! rev_involutive in H; auto.
Qed.

Lemma bits_255_below:
forall i0, 0 <= i0 < 8 -> Int.testbit (Int.repr 255) i0 = true.

Proof.

  intros.
  rewrite Int.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; destr; omega.
  unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize; simpl; omega.
Qed.

Lemma bits_255_above:
forall i0, 8 <= i0 < Int.zwordsize -> Int.testbit (Int.repr 255) i0 = false.

Proof.

  intros.
  rewrite Int.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; destr; omega.
  omega.
Qed.

Lemma bits64_255_below:
forall i0, 0 <= i0 < 8 -> Int64.testbit (Int64.repr 255) i0 = true.

Proof.

  intros.
  rewrite Int64.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int64.Ztestbit_two_p_m1; destr; omega.
  unfold Int64.zwordsize, Int64.wordsize, Wordsize_32.wordsize; simpl; omega.
Qed.

Lemma bits64_255_above:
forall i0, 8 <= i0 < Int64.zwordsize -> Int64.testbit (Int64.repr 255) i0 = false.

Proof.

  intros.
  rewrite Int64.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int64.Ztestbit_two_p_m1; destr; omega.
  omega.
Qed.

Lemma sign_ext_8_id:
  forall i0,

      (Int.sign_ext 8
                    (Int.add (Int.and i0 (Int.repr 255)) (Int.shl Int.zero (Int.repr 8)))) =
    (Int.sign_ext 8 i0).

Proof.

  intros.
  rewrite shl_zero_l.
  rewrite Int.add_zero.
  solve_int.
  rewrite bits_255_below; auto. ring.
Qed.

Lemma zero_ext_8_id:
  forall i0,

      (Int.zero_ext 8
                    (Int.add (Int.and i0 (Int.repr 255)) (Int.shl Int.zero (Int.repr 8)))) =
       (Int.zero_ext 8 i0).

Proof.

  intros.
  rewrite shl_zero_l.
  rewrite Int.add_zero.
  solve_int.
  rewrite bits_255_below; auto. ring.
Qed.

Lemma sign_ext_16_id:
  forall i0,

      (Int.sign_ext 16
                    (Int.add (Int.and i0 (Int.repr 255))
                             (Int.shl
                                (Int.add (Int.and (Int.shru i0 (Int.repr 8)) (Int.repr 255))
                                         (Int.shl Int.zero (Int.repr 8))) (Int.repr 8)))) =
      (Int.sign_ext 16 i0).

Proof.

  intros.
  solve_int.
  rewrite bits_255_below; try omega; ring.
  rewrite bits_255_above; try omega.
  rewrite bits_255_below; try omega.
  rewrite <- andb_orb_distrib_r.
  ring.
  rewrite bits_255_above; try omega.
  ring.
Qed.

Lemma zero_ext_16_id:
  forall i0,
      (Int.zero_ext 16
                    (Int.add (Int.and i0 (Int.repr 255))
                             (Int.shl
                                (Int.add (Int.and (Int.shru i0 (Int.repr 8)) (Int.repr 255))
                                         (Int.shl Int.zero (Int.repr 8))) (Int.repr 8)))) =
      (Int.zero_ext 16 i0).

Proof.

Lemma add_and_shl_rew:
  forall i i' j,
    0 <= j < Int64.zwordsize ->
    Int64.testbit
      (Int64.add (Int64.and i (Int64.repr 255)) (Int64.shl i' (Int64.repr 8)))
      j = if zlt j 8 then Int64.testbit i j
          else Int64.testbit i' ( j - 8 ).

Proof.

  intros.
  rewrite Int64.add_is_or.
  rewrite Int64.bits_or; auto.
  rewrite Int64.bits_and; auto.
  rewrite Int64.bits_shl; auto.
  change (Int64.unsigned (Int64.repr 8)) with 8.
  destr.
  rewrite orb_false_r.
  rewrite Int64.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int64.Ztestbit_two_p_m1; auto; try omega.
  destr. ring.
  rewrite Int64.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; destr; try omega.
  rewrite andb_false_r.
  rewrite orb_false_l; auto.

  solve_long.
  rewrite Int64.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; destr; try omega.
  ring.
Qed.

Lemma add_and_shl_rew_32:
  forall i i' j,
    0 <= j < Int.zwordsize ->
    Int.testbit
      (Int.add (Int.and i (Int.repr 255)) (Int.shl i' (Int.repr 8)))
      j = if zlt j 8 then Int.testbit i j
          else Int.testbit i' ( j - 8 ).

Proof.

  intros.
  rewrite Int.add_is_or.
  rewrite Int.bits_or; auto.
  rewrite Int.bits_and; auto.
  rewrite Int.bits_shl; auto.
  change (Int.unsigned (Int.repr 8)) with 8.
  destr.
  rewrite orb_false_r.
  rewrite Int.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; auto; try omega.
  destr. ring.
  rewrite Int.testbit_repr; auto.
  change 255 with (two_p 8 - 1).
  rewrite Int.Ztestbit_two_p_m1; destr; try omega.
  rewrite andb_false_r.
  rewrite orb_false_l; auto.
  solve_int.
  rewrite bits_255_above; auto; try omega.
  ring.
Qed.

Lemma int_decomp:
  forall i0,
    Int.add (Int.and i0 (Int.repr 255))
            (Int.shl
               (Int.add (Int.and (Int.shru i0 (Int.repr 8)) (Int.repr 255))
                        (Int.shl
                           (Int.add
                              (Int.and
                                 (Int.shru (Int.shru i0 (Int.repr 8)) (Int.repr 8))
                                 (Int.repr 255))
                              (Int.shl
                                 (Int.add
                                    (Int.and
                                       (Int.shru
                                          (Int.shru (Int.shru i0 (Int.repr 8))
                                                    (Int.repr 8)) (Int.repr 8))
                                       (Int.repr 255)) (Int.shl Int.zero (Int.repr 8)))
                                 (Int.repr 8))) (Int.repr 8)))
               (Int.repr 8)) = i0.

Proof.

  intros.
  rewrite shl_zero_l.
  rewrite Int.add_zero.
  apply Int.same_bits_eq; intros.
  repeat (rewrite add_and_shl_rew_32; auto; destr; try omega).
  solve_int.
  solve_int.
  solve_int.
  rewrite bits_255_below. ring.
  rewrite int_zwordsize in *; omega.
Qed.

Lemma int64_decomp:
  forall i0,
    Int64.add (Int64.and i0 (Int64.repr 255))
              (Int64.shl
                 (Int64.add
                    (Int64.and (Int64.shru i0 (Int64.repr 8)) (Int64.repr 255))
                    (Int64.shl
                       (Int64.add
                          (Int64.and (Int64.shru i0 (Int64.repr 16)) (Int64.repr 255))
                          (Int64.shl
                             (Int64.add
                                (Int64.and (Int64.shru i0 (Int64.repr 24))
                                           (Int64.repr 255))
                                (Int64.shl
                                   (Int64.add
                                      (Int64.and (Int64.shru i0 (Int64.repr 32))
                                                 (Int64.repr 255))
                                      (Int64.shl
                                         (Int64.add
                                            (Int64.and (Int64.shru i0 (Int64.repr 40))
                                                       (Int64.repr 255))
                                            (Int64.shl
                                               (Int64.add
                                                  (Int64.and
                                                     (Int64.shru i0 (Int64.repr 48))
                                                     (Int64.repr 255))
                                                  (Int64.shl
                                                     (Int64.add
                                                        (Int64.and
                                                           (Int64.shru i0
                                                                       (Int64.repr 56))
                                                           (Int64.repr 255))
                                                        (Int64.shl Int64.zero
                                                                   (Int64.repr 8)))
                                                     (Int64.repr 8)))
                                               (Int64.repr 8)))
                                         (Int64.repr 8))) (Int64.repr 8)))
                             (Int64.repr 8))) (Int64.repr 8)))
                 (Int64.repr 8)) = i0.

Proof.

  intros.
  solve_long.
  repeat (rewrite add_and_shl_rew; auto; try omega; [idtac]; destr);
    try (rewrite Int64.bits_shru; auto; try omega;
         repeat rewrite Int64.unsigned_repr by (unfold Int64.max_unsigned; simpl; omega); destr; try omega; f_equal; omega).
  exfalso.
  rewrite int64_zwordsize in *.
  omega.
Qed.

Lemma loword_add_byte:
  forall z i2,
  0 <= z < Byte.modulus ->
  Int.add (Int.repr z)
          (Int.shl (Int64.loword i2) (Int.repr 8)) =
  Int64.loword
    (Int64.add (Int64.repr z)
               (Int64.shl' i2 (Int.repr 8))).

Proof.

  intros.
  repeat rewrite shl'_shl by
            (rewrite Int.unsigned_repr; try omega; unfold Int.max_unsigned; simpl; omega).
  repeat rewrite Int.unsigned_repr by (unfold Int.max_unsigned; simpl; omega).
  assert (Int.zwordsize < Int64.zwordsize).
  unfold Int.zwordsize, Int64.zwordsize, Int.wordsize, Int64.wordsize;
    simpl; intros; omega.
  solve_int.
  * rewrite Int64.bits_loword; [|auto].
    rewrite Int64.add_is_or.
    rewrite Int64.bits_or; auto.
    cut (Int64.testbit (Int64.shl i2 (Int64.repr 8)) i = false).
    intro A; rewrite A.
    rewrite Int.testbit_repr; auto.
    rewrite Int64.testbit_repr; auto. rewrite orb_false_r; auto.
    omega.
    rewrite Int64.bits_shl.
    destr.
    clear Heqs.
    rewrite Int64.unsigned_repr in g; try omega; unfold Int64.max_unsigned; simpl; try omega.
    omega.
    omega.
    solve_long.
    cut (Int64.testbit (Int64.repr z) i0= false). intro A; rewrite A; apply andb_false_l.
    rewrite Int64.testbit_repr by omega.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
  * assert (A:Int.testbit (Int.repr z) i= false).
    rewrite Int.testbit_repr by omega.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
    rewrite A; rewrite orb_false_l.
    repeat rewrite Int64.bits_loword; auto; try omega.
    rewrite Int64.add_is_or.
    solve_long.
    assert (Int64.testbit (Int64.repr z) i = false).
    rewrite Int64.testbit_repr by omega.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
    rewrite H1; rewrite orb_false_l; auto.
    solve_long.
    assert (Int64.testbit (Int64.repr z) i0 = false).
    rewrite Int64.testbit_repr by omega.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
    rewrite H1; rewrite andb_false_l; auto.
  * assert (Int.testbit (Int.repr z) i0 = false).
    rewrite Int.testbit_repr by omega.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
    rewrite H2; rewrite andb_false_l; auto.
Qed.

Lemma int64_sign_ext_of_words:
  forall i1 i2,
    Int64.sign_ext 64 (Int64.ofwords i1 i2) =
    Int64.ofwords (Int.sign_ext 32 i1) (Int.sign_ext 32 i2).

Proof.

  intros.
  apply Int64.same_bits_eq; clear; intros.
  assert (i < 64).
  revert H; unfold Int64.zwordsize, Int64.wordsize, Wordsize_64.wordsize; simpl; intro; omega.
  rewrite Int64.bits_sign_ext; auto; try omega.
  destr_no_dep.
  repeat rewrite Int64.bits_ofwords; auto.
  destr_no_dep.
  assert (i < 32).
  revert l0; unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize; simpl; intro; omega.
  rewrite Int.bits_sign_ext; auto; try omega.
  destr.

  rewrite Int.bits_sign_ext; auto; try omega;
  revert g; unfold Int.zwordsize, Int.wordsize, Wordsize_32.wordsize; simpl; intro; try omega.
  destr_no_dep.
  omega.
Qed.

Lemma aux_encode_2:
  forall i i1,
    i + 8 < Int.zwordsize ->
    0 <= i < Int.zwordsize ->
   Int.testbit (Int.repr (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256))))
     i = Int.testbit i1 (i + 8) && Int.testbit (Int.repr 255) i.

Proof.

  intros.
  rewrite Int.testbit_repr; auto.
  des (zlt i 8).
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  change 256 with (two_p 8).
  rewrite <- Int.Zshiftr_div_two_p by omega.
  rewrite Z.shiftr_spec; auto.
  rewrite <- Int.testbit_repr; auto; try omega.
  rewrite Int.repr_unsigned; auto.
  rewrite bits_255_below; auto.
  ring.
  rewrite bits_255_above; auto; try omega.
  generalize (Byte.unsigned_range (Byte.repr (Int.unsigned i1 / 256))).
  generalize (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256))); intros.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; try omega.
  ring.
Qed.

Lemma aux_encode_1:
  forall i i0,
    0 <= i < Int.zwordsize ->
   Int.testbit (Int.repr (Byte.unsigned (Byte.repr (Int.unsigned i0)))) i =
   Int.testbit i0 i && Int.testbit (Int.repr 255) i.

Proof.

  intros.
  rewrite Int.testbit_repr; auto.
  des (zlt i 8).
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  rewrite <- Int.testbit_repr; auto.
  rewrite Int.repr_unsigned; auto.
  rewrite bits_255_below; auto.
  ring.
  rewrite bits_255_above; auto.
  generalize (Byte.unsigned_range (Byte.repr (Int.unsigned i0))).
  generalize (Byte.unsigned (Byte.repr (Int.unsigned i0))); intros.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; try omega.
  ring.
  omega.
Qed.

Lemma aux_encode_3:
  forall i i0,
    0 <= i < Int.zwordsize ->
    i + 8 + 8 < Int.zwordsize ->
   Int.testbit
     (Int.repr (Byte.unsigned (Byte.repr (Int.unsigned i0 / 256 / 256)))) i =
   Int.testbit i0 (i + 8 + 8) && Int.testbit (Int.repr 255) i.

Proof.

intros.
  assert ( 0 <= i < Int.zwordsize).
  revert H0; rewrite int_zwordsize; intuition try omega.
  rewrite Int.testbit_repr; auto; try omega.
  des (zlt i 8).
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  change 256 with (two_p 8).
  repeat rewrite <- Int.Zshiftr_div_two_p by omega.
  repeat rewrite Z.shiftr_spec; auto; try omega.
  rewrite <- Int.testbit_repr; auto.
  rewrite Int.repr_unsigned; auto.
  rewrite bits_255_below; auto.
  ring.
  omega.
  rewrite bits_255_above; auto; try omega.
  generalize (Byte.unsigned_range (Byte.repr (Int.unsigned i0/256/256))).
  generalize (Byte.unsigned (Byte.repr (Int.unsigned i0/256/256))); intros.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; try omega.
  ring.
Qed.

Lemma aux_encode_4:
  forall i i1,
    0 <= i ->
    i + 8 + 8 + 8 < Int.zwordsize ->
   Int.testbit
     (Int.repr
        (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256 / 256 / 256)))) i =
   Int.testbit i1 (i + 8 + 8 + 8) && Int.testbit (Int.repr 255) i.

Proof.

  intros.
  assert ( 0 <= i < Int.zwordsize).
  revert H0; rewrite int_zwordsize; intuition try omega.
  assert ( 0 <= i < 8).
  revert H0; rewrite int_zwordsize; intuition try omega.
  rewrite Int.testbit_repr; auto; try omega.
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  change 256 with (two_p 8).
  repeat rewrite <- Int.Zshiftr_div_two_p by omega.
  repeat rewrite Z.shiftr_spec; auto; try omega.
  rewrite <- Int.testbit_repr; auto.
  rewrite Int.repr_unsigned; auto.
  rewrite bits_255_below; auto.
  ring.
  omega.
Qed.

Lemma aux_encode_above_general:
  forall i i1,
    0 <= i < Int.zwordsize ->
    i >= 8 ->
    Int.testbit
      (Int.repr
         (Byte.unsigned (Byte.repr i1))) i =
    false.

Proof.

  intros.
  rewrite Int.testbit_repr; auto.
  generalize (Byte.unsigned_range (Byte.repr i1)).
  generalize (Byte.unsigned (Byte.repr i1)); intros.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; try omega.
Qed.

Lemma int64_byte_and_255:
  forall i,
    Int64.repr (Byte.unsigned (Byte.repr (Int.unsigned i))) =
    Int64.repr (Int.unsigned (Int.and i (Int.repr 255))).

Proof.

  intros.
  solve_long.
  rewrite ! Int64.testbit_repr; auto.
  des (zlt i0 8).
  assert (i0 < Int.zwordsize) by (rewrite int_zwordsize; omega).
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  rewrite <- ! Int.testbit_repr; auto.
  rewrite ! Int.repr_unsigned; auto.
  rewrite Int.bits_and; auto.
  rewrite bits_255_below by omega.
  ring.
  generalize (Byte.unsigned_range (Byte.repr (Int.unsigned i))). intro.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; simpl; try omega.
  des (zlt i0 32).
  rewrite <- Int.testbit_repr; auto.
  rewrite Int.repr_unsigned.
  rewrite Int.bits_and; auto.
  rewrite bits_255_above; auto; try rewrite int_zwordsize in *; try omega.
  ring.
  rewrite Byte.Ztestbit_above with (n:=32%nat); auto; simpl; try omega.
  generalize (Int.and i (Int.repr 255)); clear; intros.
  generalize (Int.unsigned_range i).
  generalize (Int.unsigned i); clear.
  unfold Int.modulus.
  unfold Int.wordsize, Wordsize_32.wordsize.
  tauto.
Qed.

Lemma int64_byte_and_255':
  forall i,
    Int64.repr (Byte.unsigned (Byte.repr (Int64.unsigned i))) =
    Int64.and i (Int64.repr 255).

Proof.

Lemma int_byte_and_255:
  forall i,
    Int.repr (Byte.unsigned (Byte.repr (Int64.unsigned i))) =
    Int.repr (Int64.unsigned (Int64.and i (Int64.repr 255))).

Proof.

  intros.
  solve_int.
  rewrite ! Int.testbit_repr; auto.
  des (zlt i0 8).
  assert (i0 < Int.zwordsize) by (rewrite int_zwordsize; omega).
  rewrite <- Byte.testbit_repr; auto.
  rewrite Byte.repr_unsigned.
  rewrite Byte.testbit_repr; auto.
  rewrite <- ! Int64.testbit_repr by (rewrite int_zwordsize in *; rewrite int64_zwordsize in *; omega).
  rewrite ! Int64.repr_unsigned; auto.
  rewrite Int64.bits_and by (rewrite int_zwordsize in *; rewrite int64_zwordsize in *; omega).
  rewrite bits64_255_below by omega.
  ring.
  generalize (Byte.unsigned_range (Byte.repr (Int64.unsigned i))). intro.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; simpl; try omega.

  assert (0 <= i0 < Int64.zwordsize) by (rewrite int_zwordsize in *; rewrite int64_zwordsize in *; omega).
  rewrite <- Int64.testbit_repr; auto.
  rewrite Int64.repr_unsigned.
  rewrite Int64.bits_and; auto.
  rewrite bits64_255_above; auto; try rewrite int_zwordsize in *; try omega.
  ring.
Qed.

Lemma int64_div256:
  forall i1,
    Int64.repr (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256))) =
    Int64.repr
      (Int.unsigned (Int.and (Int.shru i1 (Int.repr 8)) (Int.repr 255))).

Proof.

  intros.
  solve_long.
  rewrite ! Int64.testbit_repr; auto.
  des (zlt i 8).
  - assert (i < Int.zwordsize) by (rewrite int_zwordsize; omega).
    rewrite <- Byte.testbit_repr; auto.
    rewrite Byte.repr_unsigned.
    rewrite Byte.testbit_repr; auto.
    rewrite <- ! Int.testbit_repr; auto.
    rewrite ! Int.repr_unsigned; auto.
    rewrite Int.bits_and; auto.
    rewrite bits_255_below by omega.
    change 256 with (two_p 8).
    repeat rewrite <- Int.Zshiftr_div_two_p by omega.
    rewrite Int.testbit_repr; auto.
    repeat rewrite Z.shiftr_spec; auto; try omega.
    rewrite Int.bits_shru; auto.
    change (Int.unsigned (Int.repr 8)) with 8.
    destr_no_dep.
    + rewrite <- Int.testbit_repr; auto; try omega.
      rewrite Int.repr_unsigned; auto.
      ring.
    + rewrite int_zwordsize in *; try omega.
  - generalize (Byte.unsigned_range (Byte.repr (Int.unsigned i1/256))). intro.
    rewrite Byte.Ztestbit_above with (n:=8%nat); auto; simpl; try omega.
    des (zlt i 32).
    + rewrite <- Int.testbit_repr; auto.
      rewrite Int.repr_unsigned.
      rewrite Int.bits_and; auto.
      rewrite bits_255_above; try rewrite int_zwordsize in *; try omega.
      ring.
    + rewrite Int.Ztestbit_above with (n:=32%nat); auto; simpl; try omega.
      generalize ((Int.and (Int.shru i1 (Int.repr 8)) (Int.repr 255))); clear; intros.
      apply Int.unsigned_range.
Qed.

Lemma int64_div256_2:
  forall i1,
    Int64.repr (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256 / 256))) =
    Int64.repr
      (Int.unsigned (Int.and (Int.shru (Int.shru i1 (Int.repr 8)) (Int.repr 8)) (Int.repr 255))).

Proof.

  intros.
  solve_long.
  rewrite ! Int64.testbit_repr; auto.
  des (zlt i 8).
  - assert (i < Int.zwordsize) by (rewrite int_zwordsize; omega).
    rewrite <- Byte.testbit_repr; auto.
    rewrite Byte.repr_unsigned.
    rewrite Byte.testbit_repr; auto.
    rewrite <- ! Int.testbit_repr; auto.
    rewrite ! Int.repr_unsigned; auto.
    rewrite Int.bits_and; auto.
    rewrite bits_255_below by omega.
    change 256 with (two_p 8).
    repeat rewrite <- Int.Zshiftr_div_two_p by omega.
    rewrite Int.testbit_repr; auto.
    repeat rewrite Z.shiftr_spec; auto; try omega.
    repeat (rewrite Int.bits_shru; auto;
            change (Int.unsigned (Int.repr 8)) with 8;
            destr_no_dep; try (rewrite int_zwordsize in *; omega)).
    rewrite <- Int.testbit_repr; auto; try omega.
    rewrite Int.repr_unsigned; auto.
    ring.
  - rewrite Byte.Ztestbit_above with (n:=8%nat)
      by (auto; simpl; try omega; apply Byte.unsigned_range).
    des (zlt i 32).
    + rewrite <- Int.testbit_repr; auto.
      rewrite Int.repr_unsigned.
      rewrite Int.bits_and; auto.
      rewrite bits_255_above; try rewrite int_zwordsize in *; try omega.
      ring.
    + rewrite Int.Ztestbit_above with (n:=32%nat); auto; simpl; try omega.
      apply Int.unsigned_range.
Qed.

Lemma int64_div256_3:
  forall i1,
    Int64.repr (Byte.unsigned (Byte.repr (Int.unsigned i1 / 256 / 256 / 256))) =
    Int64.repr
      (Int.unsigned
         (Int.and
            (Int.shru (Int.shru (Int.shru i1 (Int.repr 8)) (Int.repr 8))
                      (Int.repr 8)) (Int.repr 255))).

Proof.

  intros.
  solve_long.
  rewrite ! Int64.testbit_repr; auto.
  des (zlt i 8).
  - assert (i < Int.zwordsize) by (rewrite int_zwordsize; omega).
    rewrite <- Byte.testbit_repr; auto.
    rewrite Byte.repr_unsigned.
    rewrite Byte.testbit_repr; auto.
    rewrite <- ! Int.testbit_repr; auto.
    rewrite ! Int.repr_unsigned; auto.
    rewrite Int.bits_and; auto.
    rewrite bits_255_below by omega.
    change 256 with (two_p 8).
    repeat rewrite <- Int.Zshiftr_div_two_p by omega.
    rewrite Int.testbit_repr; auto.
    repeat rewrite Z.shiftr_spec; auto; try omega.
    repeat (rewrite Int.bits_shru; auto;
            change (Int.unsigned (Int.repr 8)) with 8;
            destr_no_dep; try (rewrite int_zwordsize in *; omega)).
    rewrite <- Int.testbit_repr; auto; try omega.
    rewrite Int.repr_unsigned; auto.
    ring.
  - rewrite Byte.Ztestbit_above with (n:=8%nat)
      by (auto; simpl; try omega; apply Byte.unsigned_range).
    des (zlt i 32).
    + rewrite <- Int.testbit_repr; auto.
      rewrite Int.repr_unsigned.
      rewrite Int.bits_and; auto.
      rewrite bits_255_above; try rewrite int_zwordsize in *; try omega.
      ring.
    + rewrite Int.Ztestbit_above with (n:=32%nat); auto; simpl; try omega.
      apply Int.unsigned_range.
Qed.

Lemma int_byte_and_255':
  forall i,
    Int.repr (Byte.unsigned (Byte.repr (Int.unsigned i))) =
    Int.and i (Int.repr 255).

Proof.

Lemma zshiftr_unsigned_repr:
  forall i0 n,
    1 <= n ->
    Int64.unsigned (Int64.repr (Z.shiftr (Int64.unsigned i0) n)) =
    Z.shiftr (Int64.unsigned i0) n.

Proof.

  intros.
  rewrite Int64.unsigned_repr; auto.
  generalize (Int64.unsigned_range i0).
  generalize (Int64.unsigned i0).
  unfold Int64.max_unsigned, Int64.modulus, two_power_nat, shift_nat; simpl.
  intros.
  cut (Z.shiftr z n <= z).
  intros; split; try omega.
  apply Z.shiftr_nonneg; auto; omega.
  rewrite Int64.Zshiftr_div_two_p; auto.
  destruct H0.
  apply Zle_lt_or_eq in H0.
  destruct H0.
  generalize (Z_div_lt z (two_p n)); simpl.
  unfold two_power_pos, shift_pos; simpl.
  intro A.
  apply Z.lt_le_incl.
  apply A; try omega.
  cut (two_p n >= two_p 1).
  simpl; unfold two_power_pos, shift_pos; simpl; auto.
  apply Z.le_ge.
  apply two_p_monotone; omega.
  subst; simpl.
  rewrite Zdiv_0_l. omega.
  omega.
Qed.

Lemma leq_ieq:
  forall i i0,
    Int64.repr (Int.unsigned i) = Int64.repr (Int.unsigned i0) ->
    i = i0.

Proof.

  intros.
  apply Int.same_bits_eq; intros.
  apply (f_equal (fun x => Int64.testbit x i1)) in H.

  assert (0 <= i1 < Int64.zwordsize).
  rewrite int_zwordsize in H0. rewrite int64_zwordsize. omega.
  do 2 rewrite Int64.testbit_repr in H; auto.
Qed.

Lemma ofbi_ieq:
  forall i i0,
    Float32.of_bits i = Float32.of_bits i0 ->
    i = i0.

Proof.

  intros.
  rewrite <- (Float32.to_of_bits i).
  rewrite <- (Float32.to_of_bits i0).
  rewrite H. auto.
Qed.

Lemma byte_wordsize:
Byte.wordsize = 8%nat.

Proof.

vm_compute; auto. Qed.

Lemma int64_wordsize:
Int64.wordsize = 64%nat.

Proof.

vm_compute; auto. Qed.

Lemma twop_nat_8:
two_power_nat 8 = 256.

Proof.

vm_compute; auto. Qed.

Lemma twop_nat_64:
two_power_nat 64 = 18446744073709551616.

Proof.

vm_compute; auto. Qed.

Lemma int64_decomp':
  forall i,
    (Int64.add
       (Int64.repr
          (Int.unsigned (Int64.loword (Int64.and i (Int64.repr 255)))))
       (Int64.shl
          (Int64.add
             (Int64.repr
                (Int.unsigned
                   (Int64.loword
                      (Int64.and (Int64.shru i (Int64.repr 8))
                                 (Int64.repr 255)))))
             (Int64.shl
                (Int64.add
                   (Int64.repr
                      (Int.unsigned
                         (Int64.loword
                            (Int64.and (Int64.shru i (Int64.repr 16))
                                       (Int64.repr 255)))))
                   (Int64.shl
                      (Int64.add
                         (Int64.repr
                            (Int.unsigned
                               (Int64.loword
                                  (Int64.and
                                     (Int64.shru i (Int64.repr 24))
                                     (Int64.repr 255)))))
                         (Int64.shl
                            (Int64.add
                               (Int64.repr
                                  (Int.unsigned
                                     (Int64.loword
                                        (Int64.and
                                           (Int64.shru i (Int64.repr 32))
                                           (Int64.repr 255)))))
                               (Int64.shl
                                  (Int64.add
                                     (Int64.repr
                                        (Int.unsigned
                                           (Int64.loword
                                              (Int64.and
                                                 (Int64.shru i
                                                             (Int64.repr 40))
                                                 (Int64.repr 255)))))
                                     (Int64.shl
                                        (Int64.add
                                           (Int64.repr
                                              (Int.unsigned
                                                 (Int64.loword
                                                    (Int64.and
                                                       (Int64.shru i
                                                                   (Int64.repr 48))
                                                       (Int64.repr 255)))))
                                           (Int64.shl
                                              (Int64.add
                                                 (Int64.repr
                                                    (Int.unsigned
                                                       (Int64.loword
                                                          (Int64.and
                                                             (Int64.shru i
                                                                         (Int64.repr 56))
                                                             (Int64.repr 255)))))
                                                 (Int64.shl Int64.zero
                                                            (Int64.repr
                                                               (Int.unsigned (Int.repr 8)))))
                                              (Int64.repr
                                                 (Int.unsigned (Int.repr 8)))))
                                        (Int64.repr
                                           (Int.unsigned (Int.repr 8)))))
                                  (Int64.repr (Int.unsigned (Int.repr 8)))))
                            (Int64.repr (Int.unsigned (Int.repr 8)))))
                      (Int64.repr (Int.unsigned (Int.repr 8)))))
                (Int64.repr (Int.unsigned (Int.repr 8)))))
          (Int64.repr (Int.unsigned (Int.repr 8))))) = i.

Proof.

  intros; unfold Int64.loword.
  cut (forall i,
            (Int.unsigned
               (Int.repr (Int64.unsigned (Int64.and i (Int64.repr 255)))))
            =
            Int64.unsigned (Int64.and i (Int64.repr 255))).
  intro H.
  repeat rewrite H.
  repeat rewrite Int64.repr_unsigned.
  rewrite int64_decomp. auto.
  intros. rewrite Int.unsigned_repr. auto.
  generalize (Int64.unsigned_range (Int64.and i0 (Int64.repr 255))).
  split. omega.

  generalize (Int64.and_interval i0 (Int64.repr 255)).
  intros.
  transitivity (two_p (Z.min (Int64.size i0) (Int64.size (Int64.repr 255)))).
  omega.
  rewrite Zmin_spec.
  change (Int64.size (Int64.repr 255)) with 8.
  assert ( two_p (if zlt (Int64.size i0) 8 then Int64.size i0 else 8) <= two_p 8).
  destruct (zlt (Int64.size i0) 8); try omega.
  apply two_p_monotone; auto.
  split; try omega.
  unfold Int64.size, Int64.Zsize; destr; zify; omega.
  transitivity (two_p 8); try omega.
  vm_compute. congruence.
Qed.

Lemma Int64_add_is_or_lt_256:
  forall j j1,
    Int64.unsigned j < 256 ->
    Int64.add j (Int64.shl' j1 (Int.repr 8)) =
    Int64.or j (Int64.shl' j1 (Int.repr 8)).

Proof.

  intros.
  apply Int64.add_is_or.
  solve_long.
  rewrite shl'_shl by (vm_compute; intuition congruence).
  rewrite Int64.bits_shl; auto.
  change (Int64.unsigned (Int64.repr (Int.unsigned (Int.repr 8)))) with 8.
  destr; try ring.
  rewrite <- Int64.repr_unsigned with (i:=j).
  rewrite Int64.testbit_repr; try omega.
  rewrite Byte.Ztestbit_above with (n:=8%nat); auto; simpl; try omega.
  change (two_power_nat 8) with 256; auto.
  generalize (Int64.unsigned_range j); intuition omega.
Qed.

Lemma int64_testbit_above_8:
  forall i i3,
    Int64.unsigned i < 256 ->
    i3 >= 8 ->
    Int64.testbit i i3 = false.

Proof.

  intros.
  rewrite <- (Int64.repr_unsigned i).
  des (zlt i3 Int64.zwordsize).
  rewrite Int64.testbit_repr by omega.
  rewrite Int64.Ztestbit_above with (n:=8%nat); auto.
  generalize (Int64.unsigned_range i); intuition omega.
  rewrite Int64.bits_above; auto.
Qed.

Lemma int64_testbit_lt_256:
  forall i i3,
    Int64.unsigned i < 256 ->
    Int64.testbit i i3 = if zlt i3 8 then Int64.testbit i i3 else false.

Proof.

  intros.
  destr.
  rewrite int64_testbit_above_8; auto.
Qed.

Lemma int_testbit_above_8:
  forall i i3,
    Int.unsigned i < 256 ->
    i3 >= 8 ->
    Int.testbit i i3 = false.

Proof.

  intros.
  rewrite <- (Int.repr_unsigned i).
  des (zlt i3 Int.zwordsize).
  rewrite Int.testbit_repr by omega.
  rewrite Int.Ztestbit_above with (n:=8%nat); auto.
  generalize (Int.unsigned_range i); intuition omega.
  rewrite Int.bits_above; auto.
Qed.

Lemma int_testbit_lt_256:
  forall i i3,
    Int.unsigned i < 256 ->
    Int.testbit i i3 = if zlt i3 8 then Int.testbit i i3 else false.

Proof.

  intros.
  destr.
  rewrite int_testbit_above_8; auto.
Qed.

Lemma int64_testbit_lt_256_7:
  forall i i3,
    Int64.unsigned i < 256 ^ 7->
    Int64.testbit i i3 = if zlt (i3 + 8) Int64.zwordsize then Int64.testbit i i3 else false.

Proof.

  intros.
  destr.
  rewrite <- (Int64.repr_unsigned i).
  des (zlt i3 Int64.zwordsize).
  destruct (zle 0 i3).
  rewrite Int64.testbit_repr by omega.
  rewrite Int64.Ztestbit_above with (n:=56%nat); auto.
  generalize (Int64.unsigned_range i); intuition omega.
  clear Heqs; rewrite int64_zwordsize in g. simpl. omega.
  clear Heqs; rewrite int64_zwordsize in g. omega.
  rewrite Int64.bits_above; auto.
Qed.

Lemma add_byte_shl_eq_byte:
  forall i0 i i1 i2,
    Int.add (Int.repr (Byte.unsigned i0)) (Int.shl i1 (Int.repr 8)) =
    Int.add (Int.repr (Byte.unsigned i)) (Int.shl i2 (Int.repr 8)) ->
    Byte.unsigned i0 = Byte.unsigned i.

Proof.

  intros.
  assert (Int.repr (Byte.unsigned i0) = Int.repr (Byte.unsigned i)).
  {
    apply Int.same_bits_eq; intros.
    apply (f_equal (fun x => Int.testbit x i3)) in H.
    repeat rewrite Int.testbit_repr; auto.
    do 2 rewrite Int.add_is_or in H; auto.
    + do 2 rewrite Int.bits_or in H; auto.
      do 2 rewrite Int.bits_shl in H; auto.
      repeat rewrite Z.add_0_r in H; auto.
      change (Int.unsigned (Int.repr 8)) with 8 in *.
      do 2 rewrite Int.testbit_repr in H; auto.
      destruct (zlt i3 8).
      repeat rewrite orb_false_r in H; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i); auto.
      generalize (Byte.unsigned_range i0); auto.
    + clear. solve_int.
      rewrite Int.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i); auto.
    + clear. solve_int.
      rewrite Int.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i0); auto.
    + clear. solve_int.
      rewrite Int.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i0); auto.
  }
  clear H.
  assert (Byte.modulus < Int.max_unsigned).
  {
    vm_compute; auto.
  }
  rewrite <- Int.unsigned_repr at 1.
  rewrite <- Int.unsigned_repr.
  rewrite H0; auto.
  generalize (Byte.unsigned_range i); omega.
  generalize (Byte.unsigned_range i0); omega.
Qed.

Lemma add_byte_shl_eq_byte_64:
  forall i0 i i1 i2,
    Int64.add (Int64.repr (Byte.unsigned i0)) (Int64.shl i1 (Int64.repr 8)) =
    Int64.add (Int64.repr (Byte.unsigned i)) (Int64.shl i2 (Int64.repr 8)) ->
    Byte.unsigned i0 = Byte.unsigned i.

Proof.

  intros.
  assert (Int64.repr (Byte.unsigned i0) = Int64.repr (Byte.unsigned i)).
  {
    apply Int64.same_bits_eq; intros.
    apply (f_equal (fun x => Int64.testbit x i3)) in H.
    repeat rewrite Int64.testbit_repr; auto.
    do 2 rewrite Int64.add_is_or in H; auto.
    + do 2 rewrite Int64.bits_or in H; auto.
      do 2 rewrite Int64.bits_shl in H; auto.
      repeat rewrite Z.add_0_r in H; auto.
      change (Int64.unsigned (Int64.repr 8)) with 8 in *.
      do 2 rewrite Int64.testbit_repr in H; auto.
      destruct (zlt i3 8).
      repeat rewrite orb_false_r in H; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i); auto.
      generalize (Byte.unsigned_range i0); auto.
    + clear. solve_long.
      rewrite Int64.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i); auto.
    + clear. solve_long.
      rewrite Int64.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i0); auto.
    + clear. solve_long.
      rewrite Int64.testbit_repr; auto.
      repeat rewrite Byte.Ztestbit_above with (n:=8%nat); auto.
      generalize (Byte.unsigned_range i0); auto.
  }
  clear H.
  assert (Byte.modulus < Int64.max_unsigned).
  {
    vm_compute; auto.
  }
  rewrite <- Int64.unsigned_repr at 1.
  rewrite <- Int64.unsigned_repr.
  rewrite H0; auto.
  generalize (Byte.unsigned_range i); omega.
  generalize (Byte.unsigned_range i0); omega.
Qed.