Nonterminating ghost proves false

[JanBessai]

Despite the patch mentioned in #718 I can still use

package test

ensures false
func recurse() (_ int) {
        return recurse() // ensures false
}

ensures false
func test() {
        ghost var _ = recurse()
}

ensures r == 0
func bad() (r int) {
        test() // ensures false
        return 1
}

to prove false on the master branch.
Can you please check?

[jcp19]

Thank you for reporting this!

I am not sure if this is a bug, but this case is definitely confusing! From my PoV, there are two ways to look at this program:

• Option 1: the erasure of function test (i.e., the code resulting from deleting all annotations) is func test() { }. In this case, this is an unsoundness in the type system, which should have rejected the assignment.
• Option 2: the erasure of test is func test() { recurse() }, i.e., we do not store the result of the call, but the call is meant to be performed nonetheless. In this case, there is no bug.

I believe that we may have been going with Option 2, but this example definitely shows that that can be very confusing. I will bring this up in the next Gobra meeting.

[JanBessai]

Thanks for confirming! :)

Do you have a spec regarding the erasure of ghost code? I guess you'd normally remove it from the program and hence it should not be executed. If you go for option 2, this would raise further questions: what if ghost code somehow panics?

I believe fully erasing ghost variables and their initialization (expression) is also what Dafny does. As I understand it, that is the value of having ghost. Otherwise you might just declare the ghost variables as a regular part of the program, because there is no performance benefit anymore with ghost.