It's not verifiable because you're trying to prove an incorrect spec! This program's memory usage is _not_ bounded above by a constant! However, many modern fo

It's not verifiable because you're trying to prove an incorrect spec! This program's memory usage is _not_ bounded above by a constant! However, many modern formal methods _could_ prove that this function uses `f(x)` space, provided the loop body is simple enough.