[Feature Request][Prover] Better error message when function does not exist

[rahxephon89]

🚀 Feature Request

When translating a move function call into a spec function, the function call needs to be translated into a corresponding spec function call. However, if the called function is native and there is no native implementation for it, the prover will generate internal boogie error, which is confusing to users. We want to generate better error message in the prover.