Formal verification with Boogie: why A fails, and B does not?

Here is a sample Move module. Formal verification for A fails with “post-condition does not hold” while B is always successful. Why is this? :laughing:

address 0x1 {
module Question {
    resource struct A{}

    public fun new_a(): A {
        A{}
    }
    spec fun new_a {
        ensures result == A{};
    }

    //////////////////

    resource struct B {
        value: u8
    }

    public fun new_b(): B {
        B{value: 12}
    }
    spec fun new_b {
        ensures result == B{value: 12};
    }
}
}

Is this a bug?

Good question and thanks for flagging this!

The issue is that Move does not actually allow empty structs, so the source language compiles struct A {} to struct A { _dummy: bool } and A{} to A { _dummy: false }. However, ensures result == A{} in the spec lang is interpreted as an empty struct, which is why the postcondition failed.

[move-prover] Fixes a bug with empty struct pack in the spec language by wrwg · Pull Request #8176 · diem/diem · GitHub makes the prover and source language interpret empty structs in the same way, which should fix the problem.

1 Like

Thank you and @wrwg for fixing this so quickly! :tada:

However, now it seems that my Boogie is out-of-date :laughing: Is the newest (I mean newest, the required 2.8.29 is 25 days old) Boogie really needed? My Ubuntu 20.04 provides only 2.4.1 from repositories (previous master from 10th of March worked fine with this version of Boogie).

(EDIT: Also fairly recent Z3 [4.8.9] is now a requirement, Ubuntu 20.04 contains 4.8.7)

The current versions of Boogie and Z3 that Move Prover depends on can be seen from here (search for BOOGIE_VERSION and Z3_VERSION). You are correct: the current dependencies are 2.8.29 for Boogie and 4.8.9 for Z3. Move Prover might work for older versions but there are no guarantees. All versions of Boogie are available on nuget.org and can be installed easily as a dotnet tool. Similarly, all versions of Z3 are available from the Z3 github site.

1 Like

Thank you :slightly_smiling_face: Yesterday I was able to install Boogie using NuGet, and you are right, it was rather straightforward :+1: However, installing Z3 via NuGet wasn’t possible (for reasons I don’t fully understand :laughing: ), so going to build it next.

I am thinking of a docker image that could host a full development environment. There are so many moving pieces that it could be beneficial :slightly_smiling_face:

Will post here if I end up creating one.

Z3 cannot be installed via nuget. But it is also not necessary to build it yourself. You can get pre-compiled binaries for various platforms. For example, a diem script downloads Z3 here. You can obtain Z3 releases from their github release page.

Thank you @shazqadeer for pointing me to the right direction: the problem indeed was, that I didn’t run ./scripts/dev_setup.sh -y (-y being the vital part here :slightly_smiling_face: ).

Now everything works fine, and I can confirm that the recent fix indeed fixes my problem :+1: