Dafny: Fast Exponent Calculation (Loops)

I'm trying to implement and compile a Fast Exponential algorithm in Dafny but I'm running into a couple issues.

Context:

• All code is available below;
• The Fast Exponential (FastExp) lemma itself is iterative;
• An exp function is used to make sure the calculations are correct (this function executes the traditional exponential recursively);
• I will not get into how the math is being done, or if it works or not. That is not the issue, the math is correct.

Now, the main problems I'm running into:

1. I don't know what to put in the loop's decrease and invariants;
2. The FastExp lemma's postconditions "might not hold";

I would love if someone could help me out with this simple (I'm assuming) issue.

Thank you in advance.

function isEven(a: int): bool
    requires a >= 0;
{
    if a == 0 then      true 
    else if a == 1 then false 
    else                isEven(a - 2)
}

function exp(x: int, n: int): int
    requires n > 0;
{
    if n == 1 then
        x
     else 
        x * exp(x, n-1)
}

lemma FastExp(x: int, n: int) returns (r: int)
requires n >= 0
ensures r == exp(x,n)
{
    var expo:int := n;
    var c:int := x;
    var tempR:int := 1;

    while expo > 0
        invariant 0 <= expo
        decreases expo
    {
        if isEven(expo) {
            tempR := tempR * c;
        }
        c := c * c;
        expo := expo / 2;
    }
    r := tempR;
}

A decreases clause is used explain termination. To prove that a loop terminates, you need to find some expression whose value decreases (in a well-founded order) with every iteration. In your case, expo is such an expression, so your decreases clause is all you need to prove termination of your loop. (In fact, it's more than you need. If you leave off this decreases clause altogether, Dafny will guess this one automatically.)

The way to reason about a loop is to find some condition, called the loop invariant, that holds true at the very top of each iteration (that is, a condition that is true every time the loop guard is evaluated). You have written one such invariant, namely 0 <= expo. However, there is no invariant about the variables tempR and c, or about the relationship between these variables and expo, x, and n. Therefore, the verifier knows nothing about the values of these variables at the start of a loop iteration or after the loop.

So, to verify that your program performs the correct math, you need to convince the verifier of this by writing invariant conditions.

Let me get you started. There are three things your invariant needs to do. 0: It needs to hold initially, when the loop is first reached. That is, the condition must be true for the initial values of the variables. 1: The invariant and the negation of the loop guard (and these alone, with no other facts that you may think also hold) must suffice to prove the postcondition. For example, the only thing you can infer from your current loop invariant and the negation of the guard is that expo == 0 after the loop. 2: The invariant must be maintained by the loop body. That is, given the invariant and the guard at the start of the loop body, you must prove that the invariant holds again after the loop body.

After you figure out what the loop invariant should be, you'll need to prove a math fact about exponentiation. You'll see when you get there.

Good luck!

PS. Here are some other comments about your programs:

• You're currently getting a precondition violation at your call to exp in the postcondition of FastExp. That means your postcondition is ill-defined and doesn't always have a meaning (which would make the task of trying to establish the postcondition impossible). The problem is that FastExp allows n to be 0, but your function exp does not. You're going to need exp to be defined for an exponent 0 to prove the correctness of FastExp. So, change the precondition of exp to allow n being 0. (You'll then have to fix up the body of exp.)
• Dafny has a type nat, which stands for non-negative integers. So, if you want, instead of declaring n: int and adding the preconditions 0 <= n, you can simply declare n: nat and drop those preconditions.
• There's a shorter way to define isEven, namely a % 2 == 0.
• You don't need to introduce local variable tempR. You can just use r directly.
• It's a bit odd to declare FastExp as a lemma. Dafny does allow lemmas to have out-parameters (which is sometimes really useful) and you can indeed write the proof of the lemma using a loop. But the reason for writing FastExp is not to show that there is some value you can assign to r to make r == exp(x, n) true--you could have done that with the assignment r := exp(x, n);. Instead, the reason to declare FastExp is that you want a program that computes it. To do that, declare FastExp to be a method. (The only technical difference between a lemma and a method in Dafny is that the method gets compiled whereas the lemma is erased by the compiler.)