Module TwoPowerFacts

Require Import Coqlib.
Require Import Integers.
Require Import Psatz.
Require Import Align Tactics.
Require Import Permutation.

Opaque two_power_nat.
Opaque minus Z.mul.
Local Opaque Pos.of_nat.

Hint Resolve two_power_nat_pos.

Lemma two_power : forall n, (1 <= NPeano.pow 2 n)%nat.

Proof.

  intro.
  change (1%nat) with (NPeano.pow 2 0)%nat at 1.
  intros.
  apply NPeano.Nat.pow_le_mono_r ; lia.
Qed.

Lemma two_power_nat_monotone:
  forall m n,
    (m <= n)%nat ->
    two_power_nat m <= two_power_nat n.

Proof.

intros; rewrite ! two_power_nat_two_p.
apply two_p_monotone. lia.
Qed.

Lemma two_power_nat_monotone_strict:
  forall m n,
    (m < n)%nat ->
    two_power_nat m < two_power_nat n.

Proof.

intros; rewrite ! two_power_nat_two_p.
apply two_p_monotone_strict. lia.
Qed.

Lemma eq_le: forall (n m: nat), n = m -> (n <= m)%nat.

Proof.

intros; lia. Qed.

Lemma N2Z_add_lt_lt_Z2N:
  forall n e m,
    Z.of_nat (n + e) < m ->
    (n < Z.to_nat m)%nat.

Proof.

  intros.
  zify.
  rewrite Z2Nat.id by lia.
  lia.
Qed.

Lemma mult_lt_le_mono:
  forall (a b c d: nat),
    (a < c)%nat -> (O < b <= d)%nat ->
    (a * b < c * d)%nat.

Proof.

intros. nia.
Qed.

Lemma div_mul_add:
  forall x k y,
    x = 8 * k ->
    (x + y) / 8 = x / 8 + y / 8.

Proof.

  intros. subst.
  rewrite Z.mul_comm. rewrite Z_div_plus_full_l.
  rewrite Z_div_mult_full. auto. lia. lia.
Qed.

Lemma div_spec:
  forall a b, b > 0 ->
         exists q r,
           a = q * b + r /\ 0 <= r < b.

Proof.

  intros.
  exists (a/b), (a mod b).
  split.
  rewrite Zmod_eq_full. lia. lia.
  apply Z_mod_lt. auto.
Qed.

Lemma div_large_div_small:
  forall x b,
    (exists k, x = b * k) ->
    forall b',
      (b' | b) ->
      exists k, x = b' * k.

Proof.

intros x b (k & EQ) b' (k' & EQ').
subst. exists (k' * k); lia.
Qed.

Lemma div_large_div_small_two_p:
  forall x b,
    (exists k, x = two_power_nat b * k) ->
    forall b',
      (b' <= b)%nat ->
      exists k, x = two_power_nat b' * k.

Proof.

  intros.
  eapply div_large_div_small; eauto.
  rewrite ! two_power_nat_two_p.
  apply IntFacts.two_p_inj_div. lia.
Qed.

Lemma two_p_split:
  forall x y,
    0 <= y <= x ->
    two_p x = two_p y * two_p (x - y).

Proof.

intros; rewrite <- two_p_is_exp; try lia. f_equal. lia.
Qed.

Lemma two_power_nat_split:
  forall x y,
    (y <= x)%nat ->
    two_power_nat x = two_power_nat y * two_power_nat (x - y).

Proof.

  intros.
  rewrite ! two_power_nat_two_p.
  rewrite Nat2Z.inj_sub; auto.
  apply two_p_split. lia.
Qed.

Lemma two_p_div:
  forall X Y Y' k,
    X = two_power_nat Y * k ->
    (Y' <= Y)%nat ->
    X = two_power_nat Y' * (two_power_nat (Y - Y') * k).

Proof.

  intros; subst.
  rewrite Z.mul_assoc.
  rewrite <- two_power_nat_split. auto. auto.
Qed.

Lemma two_p_div_rew:
  forall n m (LE: (m <= n)%nat)
    x y,
    (two_power_nat n * x +y) / two_power_nat m =
    (two_power_nat n * x) / two_power_nat m + y / two_power_nat m.

Proof.

  intros.
  replace (two_power_nat n * x +y) with (y + x * two_power_nat n) by lia.
  rewrite (two_power_nat_split n m); auto.
  rewrite (Z.mul_comm (two_power_nat m)). rewrite Z.mul_assoc.
  rewrite Z_div_plus; auto.
  rewrite Z.add_comm. f_equal.
  replace (two_power_nat (n - m) * two_power_nat m * x) with ((two_power_nat (n - m) * x) * two_power_nat m) by lia.
  rewrite Z_div_mult_full. lia.
  generalize (two_power_nat_pos m); lia.
Qed.

Lemma two_p_div_rew':
  forall n m (LE: (m <= n)%nat) x,
    (two_power_nat n * x) / two_power_nat m =
    (two_power_nat (n - m) * x).

Proof.

  intros.
  replace (two_power_nat n * x) with (two_power_nat n * x + 0).
  rewrite two_p_div_rew.
  rewrite Z.div_0_l.
  replace (two_power_nat n * x) with (x * two_power_nat n) by lia.
  rewrite (two_power_nat_split n m); auto.
  rewrite (Z.mul_comm (two_power_nat _)). rewrite Z.mul_assoc.
  rewrite Z_div_mult_full. lia.
  generalize (two_power_nat_pos m); lia.
  generalize (two_power_nat_pos m); lia.
  auto.
  lia.
Qed.

Opaque two_power_nat.
Opaque minus Z.mul.

Lemma int_and_two_p_m1_mul':
  forall i n,
    Z.of_nat n <= Int.max_unsigned ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      i = Int.mul (Int.repr (two_power_nat n)) k.

Proof.

  intros i n H H0. rewrite <- H0.
  exists (Int.shr i (Int.repr (Z.of_nat n))).
  IntFacts.solve_int.
  rewrite Int.bits_not; auto. rewrite Int.testbit_repr; auto.
  rewrite two_power_nat_two_p. rewrite Int.Ztestbit_two_p_m1 by lia.
  rewrite Int.mul_commut.
  rewrite <- (Int.unsigned_repr (Z.of_nat n)).
  rewrite <- Int.shl_mul_two_p. rewrite Int.bits_shl; auto.
  destr. ring.
  rewrite andb_true_r.
  rewrite Int.bits_shr.
  rewrite (Int.unsigned_repr (Int.unsigned _)).
  destr. f_equal. lia. lia.
  apply Int.unsigned_range_2. split. lia. generalize (Int.unsigned_range (Int.repr (Z.of_nat n))). lia.
  split. lia. auto.
Qed.

Lemma int_and_two_p_m1_mul_Z':
  forall i n,
    Z.of_nat n < 32 ->
    Int.and i (Int.not (Int.repr (two_power_nat n - 1))) = i ->
    exists k,
      Int.unsigned i = (two_power_nat n) * k.

Proof.

  intros.
  destruct (fun pf => int_and_two_p_m1_mul' _ _ pf H0) as [k EQ].
  eapply Z.le_trans with (m:=32). lia. vm_compute. congruence.
  rewrite EQ.
  unfold Int.mul.
  rewrite Int.unsigned_repr_eq.
  rewrite Int.unsigned_repr.
  unfold Int.modulus.
  rewrite ! (two_power_nat_two_p).
  replace (Z.of_nat Int.wordsize) with (Z.of_nat n + (Z.of_nat Int.wordsize - Z.of_nat n)).
  rewrite two_p_is_exp.
  rewrite Zmult_mod_distr_l.
  eexists; eauto.
  lia.
  change Int.wordsize with 32%nat. lia.
  change Int.wordsize with 32%nat. lia.
  unfold Int.max_unsigned. split. generalize (two_power_nat_pos n); lia.
  cut (two_power_nat n < Int.modulus). lia.
  unfold Int.modulus. rewrite ! two_power_nat_two_p.
  apply two_p_monotone_strict. split. lia.
  change Int.wordsize with 32%nat. lia.
Qed.