vericert.common.IntegerExtra

Module PtrofsExtra.



  Lemma signed_mod_unsigned_mod :
    forall x m,
      0 < m ->
      Ptrofs.modulus mod m = 0 ->
      Ptrofs.signed x mod m = 0 ->
      Ptrofs.unsigned x mod m = 0.

  Lemma of_int_mod :
    forall x m,
      Int.unsigned x mod m = 0 ->
      Ptrofs.unsigned (Ptrofs.of_int x) mod m = 0.

  Lemma mul_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.signed (Ptrofs.mul x y)) mod m = 0.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Ptrofs.modulus) ->
      Ptrofs.unsigned x mod m = 0 ->
      Ptrofs.unsigned y mod m = 0 ->
      (Ptrofs.unsigned (Ptrofs.add x y)) mod m = 0.

  Lemma mul_divu :
    forall x y,
      0 < Ptrofs.unsigned x ->
      Ptrofs.unsigned y mod Ptrofs.unsigned x = 0 ->
      (Integers.Ptrofs.mul x (Integers.Ptrofs.divu y x)) = y.

  Lemma divu_unsigned :
    forall x y,
      0 < Ptrofs.unsigned y ->
      Ptrofs.unsigned x <= Ptrofs.max_unsigned ->
      Ptrofs.unsigned (Ptrofs.divu x y) = Ptrofs.unsigned x / Ptrofs.unsigned y.

  Lemma mul_unsigned :
    forall x y,
      Ptrofs.mul x y =
      Ptrofs.repr (Ptrofs.unsigned x * Ptrofs.unsigned y).

  Lemma pos_signed_unsigned :
    forall x,
      0 <= Ptrofs.signed x ->
      Ptrofs.signed x = Ptrofs.unsigned x.
End PtrofsExtra.


Module IntExtra.


  Lemma mul_mod1 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.

  Lemma mul_mod2 :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.mul x y)) mod m = 0.

  Lemma add_mod :
    forall x y m,
      0 < m ->
      (m | Int.modulus) ->
      Int.unsigned x mod m = 0 ->
      Int.unsigned y mod m = 0 ->
      (Int.unsigned (Int.add x y)) mod m = 0.

  Definition ofbytes (a b c d : byte) : int :=
    or (shl (repr (Byte.unsigned a)) (repr (3 * Byte.zwordsize)))
       (or (shl (repr (Byte.unsigned b)) (repr (2 * Byte.zwordsize)))
           (or (shl (repr (Byte.unsigned c)) (repr Byte.zwordsize))
               (repr (Byte.unsigned d)))).

  Definition byte1 (n: int) : byte := Byte.repr (unsigned n).

  Definition byte2 (n: int) : byte := Byte.repr (unsigned (shru n (repr Byte.zwordsize))).

  Definition byte3 (n: int) : byte := Byte.repr (unsigned (shru n (repr (2 * Byte.zwordsize)))).

  Definition byte4 (n: int) : byte := Byte.repr (unsigned (shru n (repr (3 * Byte.zwordsize)))).

  Lemma bits_byte1:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte1 n) i = testbit n i.

  Lemma bits_byte2:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte2 n) i = testbit n (i + Byte.zwordsize).

  Lemma bits_byte3:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte3 n) i = testbit n (i + (2 * Byte.zwordsize)).

  Lemma bits_byte4:
    forall n i, 0 <= i < Byte.zwordsize -> Byte.testbit (byte4 n) i = testbit n (i + (3 * Byte.zwordsize)).

  Lemma bits_ofwords:
    forall b4 b3 b2 b1 i, 0 <= i < zwordsize ->
                          testbit (ofbytes b4 b3 b2 b1) i =
                          if zlt i Byte.zwordsize
                          then Byte.testbit b1 i
                          else (if zlt i (2 * Byte.zwordsize)
                                then Byte.testbit b2 (i - Byte.zwordsize)
                                else (if zlt i (3 * Byte.zwordsize)
                                      then Byte.testbit b2 (i - 2 * Byte.zwordsize)
                                      else Byte.testbit b2 (i - 3 * Byte.zwordsize))).

  Lemma div_divs_equiv :
    forall x y,
      signed x >= 0 ->
      signed y >= 0 ->
      divs x y = divu x y.

  Lemma neg_signed' :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed (neg x) = - signed x.

  Lemma neg_divs_distr_l :
    forall x y,
      unsigned x <> 2147483648 ->
      neg (divs x y) = divs (neg x) y.

  Lemma neg_signed :
    forall x : int,
      unsigned x <> 2147483648 ->
      signed x < 0 ->
      signed (neg x) >= 0.

  Lemma shl_signed_positive :
    forall y,
      unsigned y <= 30 ->
      signed (shl one y) >= 0.

  Lemma is_power2_shl :
    forall y,
      unsigned y <= 30 ->
      is_power2 (shl one y) = Some y.

  Definition shrx_alt (x y : int) : int :=
    if zlt (signed x) 0
    then neg (shru (neg x) y)
    else shru x y.

  Lemma shrx_shrx_alt_equiv_ne :
    forall x y,
      unsigned x <> 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.

  Lemma shrx_shrx_alt_equiv_eq :
    forall x y,
      unsigned x = 2147483648 ->
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.

  Theorem shrx_shrx_alt_equiv :
    forall x y,
      unsigned y <= 30 ->
      shrx x y = shrx_alt x y.

End IntExtra.