Can we have an arbitrary big upper bound for the looping variable in Dafny?

I'm trying to write a "linear search" method in Dafny. The method takes a function f that maps natural numbers to boolean values and it's known that there exists a first number n for which f(n) == True. Then the method ensures that n is the returned value.
Naturally n can be arbitrary big from this specification, and only under the assumption of an arbitrary big amount of energy available one could ensure that the program will be able to find n.

Is this something which is not expressible in Dafny at all?

Here is what I tried

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;
    }
}

The verifier fails with: "cannot prove termination; try supplying a decreases clause for the loop"

An alternative bounded linear search get's verified without issues.

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;
    }
}

You can verify the original version by using a ghost variable as well as adding the necessary invariants to your loop. A ghost variable is a variable you can use to keep additional information around for verification, but is not part of the compilable code.

module SO6 {
    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)
    {
        ghost var n: nat :| f(n);
        x := 0;
        while !f(x)
            invariant x <= n
            invariant forall i : nat :: i < x ==> !f(i)
            decreases n - x
        {
            x := x + 1;
        }
        assert f(x);
    }

}