Predicates containing higher-order assertions behave oddly

[csgordon]

I'm working with some code that resembles:

predicate higherorder<T>(p:(T ~> bool)) 

class Bad {
    var x: nat
    predicate inv() reads this { higherorder((o:nat) reads this => true) }
    method m()
        requires inv()
        ensures higherorder((o:nat) reads this => true)
    {
        assert inv();
        // Next line is an assertion violation, despite being equivalent to inv()
        assert higherorder((o:nat) reads this => true);
        // Next line fails to imply the identical postcondition
        assume higherorder((o:nat) reads this => true);
    }
}

The intent is to have the predicate higherorder be opaque (an axiomatization of something that cannot be expressed in ghost state). I would expect this example, and analagous cases in my development to successfully verify, because the definition of higherorder is not required.

However, notice that while the first assertion (inv()) succeeds, the second assertion --- which simply expands the definition of the precondition inv --- fails. Also strange, even if I assume the postcondition as I have here, Dafny still claims the postcondition might not hold.

If I give higherorder a trivial definition of true then everything verifies. But I'd expect higherorder to be treated as some sort of uninterpreted function, and certainly for a use to imply itself (i.e., for asserting the body of the invariant to succeed any time asserting the invariant succeeded). Oddly, in the larger system I'm working with, it sometimes works as I expect it, and sometimes does what it does here.

This seems to be specific to higher-order predicates, as the following verifies just fine despite also having a fully undefined predicate:

predicate foo(x:nat)
class Maybe {
    var x:nat
    predicate inv() reads this { foo(x) }
    method m()
        requires inv()
        ensures foo(x)
    {
        assert inv();
        assert foo(x);
    }
}

And modifying the succeding example above to also include generics also works as expected:

predicate bar<T>(x:T)
class Maybe2 {
    var x:nat
    predicate inv() reads this { bar(x) }
    method m()
        requires inv()
        ensures bar(x)
    {
        assert inv();
        assert bar(x);
    }
}

[amaurremi]

The above example does verify on my computer -- does the issue persist if you try updating Boogie (if you haven't done so already)? You might have to pull the recent changes from Dafny as well. The issue might be that the lambda translation that Boogie used prior to some recent updates was very sensitive to the context in which a lambda occurs. As a result, the two occurrences of the (o:nat) reads this => true lambda expression (in the ensures clause and in the assume statement) were translated in different ways into Boogie, and the verifier could not detect that they are the same thing.

[csgordon]

Interesting. Which version of Boogie are you using? This is from a fresh source checkout of Boogie and Dafny that I grabbed yesterday (Boogie commit boogie-org/boogie@bc49937e7ee88e931bbe2dbf779a42612731a8fd) to go with Rustan's fix for #332.

[samuelgruetter]

Is the behavior the same for Dafny invoked from the command line as when using the IDE?

[csgordon]

Curious, going directly from the command line succeeds (for verification):

PS > ../dafny-trunk/dafny/Binaries/dafny ./BadHO.dfy           
Dafny 2.3.0.10506

Dafny program verifier finished with 6 verified, 0 errors
./BadHO.dfy(13,8): Error: an assume statement cannot be compiled
./BadHO.dfy(2,10): Error: Function _module._default.higherorder has no body
./BadHO.dfy(17,10): Error: Function _module._default.foo has no body
./BadHO.dfy(31,10): Error: Function _module._default.bar has no body
PS > 

The compilation errors are expected, and marking the predicates as {:extern} makes the "no body" errors disappear. It appears to work from the command line for my original use case as well.

I was using the VSCode extension, but had pointed it to this compiled version of Dafny. It's clearly picking up the new Dafny version, as it's clearly seeing the fix of #332.

[csgordon]

To see if it was using an old Boogie version (e.g., from the copy of Dafny installed by the extension itself) I uninstalled the copy of Dafny pulled in by the extension (including its copy of Boogie) to make sure it's not accidentally finding an old version of Boogie, and the behavior reported above still appears through the extension.

Are there any flags to Dafny (or Dafny-Server) that would disable the new Boogie encoding of lambdas? Would you suggest I open an issue against the extension?

[samuelgruetter]

I observed the same confusing behavior on a different example too: A dafny file using lambdas verifies on the command line, but not in the VS Code Dafny extension, and I did everything I could imagine to make sure the command line runs the same version as the IDE (reinstalling, restarting, verifying paths, ...). This happened on Windows. On Jared's Mac, the issue was not reproducible.

[csgordon]

Hmm. For what it's worth, this is a Linux machine. I'll give my own Mac a shot at the office tomorrow.

[csgordon]

Just built the latest version on my Mac and I see the same issue: works from the command line, but using the IDE gives the errors I originally reported. And this is a machine that hadn't previously had any version of Dafny or Boogie installed.