Formal verification: how to ensure a struct is actually destroyed

Hello! :slightly_smiling_face:
Consider the following example:

module Question {
    struct S1 has key, store {}

    public fun destroy(s1: S1) {
        let S1 {} = s1;
    }
    spec fun destroy {
        aborts_if false;

        //How to ensure the struct is actually destoryed?
    }
}

While I understand that this is ensured by Move/MoveVM, I wonder how to express this in spec, to achieve:

  • communicating to the reader that this is a requirement, and
  • making sure that this requirement does not change (unless the spec is changed).

I browsed through the formal verification tests, and this was the nearest I could find, but it’s just about creating an empty struct, not about destroying it: diem/resources.move at main Β· diem/diem Β· GitHub.

Ha! For this particular case, this seems to do the trick:

ensures s1 != S1{};

Although I think this is suboptimal, it works for now :nerd_face:

Although this worked with Move / Prover 1.2.0, it doesn’t anymore on 1.3.0 :frowning:

Instead, I get the following:

error: post-condition does not hold

    β”Œβ”€β”€ /home/ville/projects/taohe/modules/Question.move:12:9 ───
    β”‚
 12 β”‚         ensures s1 != S1{};
    β”‚         ^^^^^^^^^^^^^^^^^^^

Full code:

address {{sender}} {
module Question {
    struct S1 has key, store {}

    public fun destroy(s1: S1) {
        let S1 {} = s1;
    }
    spec destroy {
        aborts_if false;

        //How to ensure the struct is actually destoryed?
        ensures s1 != S1{};
    }
}
}

What would be the 1.3.0 way to achieve this?

Hi, the Move prover does not generally support reasoning about lifetime of values. Lifetime is part of the core Move language’s type system, and the Move prover is assuming a program to satisfy all lifetime constraints before it starts. The difference between 1.2 and 1.3 behavior regards the ensures s1 != S1{} appears to be accidentally (i.e. it should have failed verification in 1.2 as well). I see the point that it might be useful to say something about lifetimes in the spec for documentation purposes; we keep this as a potential feature in mind, but the current behavior in 1.3. (unfortunately) works as intended.

1 Like

+1 for such a feature :slightly_smiling_face: