IsPerfectSquare (Dafny)

I have this IsPerfectSquare predicate that is used in post/pre conditions and invariants. It can't be a method.

predicate IsPerfectSquare(n: int)
    requires n >= 0
{
    IsPerfectSquareFunctional(n, 0)
}

predicate IsPerfectSquareFunctional(n: int, sqrt_candidate: int) 
    requires n >= 0
    requires sqrt_candidate >= 0
    decreases n - sqrt_candidate
{
    // Unfortunately, this is not valid Dafny
    //exists k: int :: 0 <= k && k * k == n
    if sqrt_candidate * sqrt_candidate >= n then sqrt_candidate*sqrt_candidate == n
    else IsPerfectSquareFunctional(n, sqrt_candidate+1)
}

Two questions:

1. Why doesn't this verify?

method Main()
{
    for i:= 0 to 10
    {
        assert IsPerfectSquare(i*i);
    }
}

2. Is there any way of expressing the postcondition of the predicate with an existential? Because that's the natural way of expressing what a perfect square is.

Thanks.

In absence of post condition of function, Dafny uses unrolling of definition to verify assertion. Dafny restricts unrolling up to fixed depth controlled by fuel parameter.

Adding sufficient fuel will make program verify.

predicate IsPerfectSquare(n: int)
  requires n >= 0
{
  IsPerfectSquareFunctional(n, 0)
}

predicate {:fuel 10} IsPerfectSquareFunctional(n: int, sqrt_candidate: int) 
  requires n >= 0
  requires sqrt_candidate >= 0
  decreases n - sqrt_candidate
{
  // Unfortunately, this is not valid Dafny
  //exists k: int :: 0 <= k && k * k == n
  if sqrt_candidate * sqrt_candidate >= n then sqrt_candidate*sqrt_candidate == n
  else IsPerfectSquareFunctional(n, sqrt_candidate+1)
}


method Main()
{
  for i:= 0 to 10
    {
      assert IsPerfectSquare(i*i);
    }
}

To answer your second question, it is possible to express number is square using existential in ghost context

ghost predicate IsPerfectSquare(n: int)
  requires n >= 0
{
   exists k : int :: 0 <= k && k * k == n
}