Calculating integer exponents in dafny

Question

I'm new to dafny and I am having trouble with getting exponents for integers

invariant x >= 0 && y >= 0 && ((x + y) * (2^(u-1)) + result == i1 + i2);

for the part that says "2^(u-1)" i keep getting the error that it is expecting bitvectors but instead got int. How do I fix this? I need result to be an int

Answer 1

Dafny does not have an exponent operator so ^ is not exponentiation but instead bitwise xor, which is why it complaining about bit vectors.

function pow(base: int, exp: nat): int {
 if exp == 0 then 1 else base * pow(base, exp-1)
}

invariant x >= 0 && y >= 0 && (x + y) * pow(2, u-1) + result == i1 + i2;

Dafny has some trouble with multiplication, as apparently multiplication is undecided-able, so it will likely not automatically verify. You will need to show inductively that your invariant is true, possibly requiring some lemmas about pow and your particular problem.