#pragma JessieIntegerModel(math)

/*@ logic integer POW (integer x, integer n) =
  @   (n > 0) ? x * POW(x, n-1)
  @           : 1;
  @*/

/*@ requires  n >= 0;
  @ ensures   \result == POW(x, n);
  @*/
unsigned long pow (unsigned long x, unsigned int n)
{
  unsigned long r;

  /*@ loop invariant
    @   n >= 0;
    @ loop invariant
    @   POW(\at(x, Pre), \at(n, Pre)) == r * POW(x, n);
    @*/
  for (r = 1; n > 0; n /= 2, x = x*x)
    if (n % 2 == 1)
       r *= x;
  return r;
}

/*@ lemma pow_zero:
  @   \forall integer x;
  @     POW(x, 0) == 1;
  @*/

/*@ lemma pow_pos:
  @   \forall integer x, integer n;
  @     n > 0 ==>
  @       POW(x, n) == x * POW(x, n-1);
  @*/

/*@ lemma pow_square_even:
  @   \forall integer x, integer n;
  @     n >= 0 ==>
  @     n % 2 == 0 ==>
  @       POW(x, n) == POW(x*x, n/2);
  @*/

/*@ lemma pow_square_odd:
  @   \forall integer x, integer n;
  @     n >= 0 ==>
  @     n % 2 == 1 ==>
  @       POW(x, n) == x * POW(x*x, n/2);
  @*/

/*@ lemma mult_left_identity:
  @   \forall integer x;
  @     1 * x == x;
  @*/

/*@ lemma mult_right_identity_with_pow:
  @   \forall integer x, integer y;
  @     x * POW(y, 0) == x;
  @*/

/*@ lemma div_non_negative:
  @   \forall integer x;
  @     x > 0 ==> x / 2 >= 0;
  @*/

/*@ lemma mult_associative:
  @   \forall integer x, integer y, integer z;
  @     (x * y) * z == x * (y * z);
  @*/

/*@ lemma mod_two_is_one_or_zero:
  @   \forall integer n;
  @     n >= 0 && n % 2 != 1 ==> n % 2 == 0;
  @*/