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:
- I don't know what to put in the loop's decrease and invariants;
- 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 yourdecreases
clause is all you need to prove termination of your loop. (In fact, it's more than you need. If you leave off thisdecreases
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 variablestempR
andc
, or about the relationship between these variables andexpo
,x
, andn
. 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:
exp
in the postcondition ofFastExp
. 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 thatFastExp
allowsn
to be0
, but your functionexp
does not. You're going to needexp
to be defined for an exponent0
to prove the correctness ofFastExp
. So, change the precondition ofexp
to allown
being0
. (You'll then have to fix up the body ofexp
.)nat
, which stands for non-negative integers. So, if you want, instead of declaringn: int
and adding the preconditions0 <= n
, you can simply declaren: nat
and drop those preconditions.isEven
, namelya % 2 == 0
.tempR
. You can just user
directly.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 writingFastExp
is not to show that there is some value you can assign tor
to maker == exp(x, n)
true--you could have done that with the assignmentr := exp(x, n);
. Instead, the reason to declareFastExp
is that you want a program that computes it. To do that, declareFastExp
to be amethod
. (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.)