Podemos ter um limite superior arbitrário para a variável de loop em Dafny?

Estou tentando escrever um método de "busca linear" em Dafny. O método pega uma função fque mapeia números naturais para valores booleanos e sabe-se que existe um primeiro número npara o qual f(n) == True. Então o método garante que esse né o valor retornado.
Naturalmente npode ser arbitrariamente grande a partir dessa especificação, e somente sob a suposição de uma quantidade arbitrária de energia disponível pode-se garantir que o programa será capaz de encontrar n.

Isso é algo que não pode ser expresso em Dafny?

Aqui está o que eu tentei

method linear_search(f: nat -> bool) returns (x: nat)
    requires exists n : nat :: f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    while !f(x)
    {
        x := x + 1;
    }
}

O verificador falha com: "não é possível provar o término; tente fornecer uma cláusula de diminuição para o loop"

Uma busca linear limitada alternativa é verificada sem problemas.

method bounded_linear_search(f: nat -> bool, max_bound: nat) returns (x: nat)
    requires exists n : nat :: n <= max_bound && f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    while !f(x) && x <= max_bound
        decreases max_bound - x
        invariant forall i : nat :: i < x ==> !f(i)
    {
        x := x + 1;
    }
}