I get "index out of range" error in a function when an ensure makes this impossible

Question

I am trying to implement the KMP algorithm in Dafny according to CLRS [sec. 32.4], and I am having trouble implementing the *[q]:

function FuncStarIter(func: seq<nat>, q: nat, count: nat): nat
    requires 0 <= q < |func|
    requires forall i :: 0 <= i < |func| ==> 0 <= func[i] < |func|
    ensures count != 0 && func[q] != 0 ==> 0 <= FuncStarIter(func, q, count-1) - 1 <= |func|
{
    if count == 0 then q else
        if func[q] == 0 then func[q] else
            func[FuncStarIter(func, q, count-1) - 1]
}

function FuncStar(func: seq<nat>, q: nat) : set<nat>
    requires q < |func|
    requires forall i :: 0 <= i < |func| ==> 0 <= func[i] < |func|
{
    set count | 1 <= count <= |func| :: FuncStarIter(func, q, count)
}

The ensures count != 0 ==> 0 <= FuncStarIter(func, q, count-1) - 1 <= |func| is to make sure that FuncStarIter(func, q, count-1) - 1 is a valid index for func, however I get Error: index out of range. Alternatively, Is there a way to prove claims in a function?

Answer 1

So, you have an off by one error here. Specifically, you are using FuncStarIter(func, q, count-1) - 1 <= |func| to show FuncStarIter(func, q, count-1) - 1 is a valid index. But, in Dafny, a valid index i must be 0 <= i < |arr| for some array arr.

Anyway, without knowing more about the algorithm, I can't exactly say what the right fix is. However, this version verifies and looks roughly like what you are after:

function FuncStarIter(func: seq<nat>, q: nat, count: nat) : (r:nat)
// q is a valid index into func
requires 0 <= q < |func|
// Every element in func is a valid index into func
requires forall i :: 0 <= i < |func| ==> 0 <= func[i] < |func|
// The return is a valid index into func
ensures r < |func|
{
    if count == 0 then q else
        if func[q] == 0 then func[q] else
            func[FuncStarIter(func, q, count-1)]
}