[Prover][Issue] Proving the data invariant over two data fields.

[junkil-park]

Consider the following example:

struct A {
        v1: vector<u64>,
        v2: vector<u64>,
    }
    spec A {
        invariant len(v1) == len(v2);
    }

    public fun push_A(a: &mut A) {
        let v1 = &mut a.v1;
        let v2 = &mut a.v2;
        vector::push_back(v1, 1);
        vector::push_back(v2, 1);
    }

In push_A , the data invariant len(v1) == len(v2) is violated at the intermediate moment when v1 is updated, but not v2. This pattern of data invariant (i.e., the relation property about multiple fields) is used in practice, but we couldn't find a way to properly verify. This situation occurred as a side effect of this PR https://github.com/move-language/move/pull/792.

The following attempt also failed.

struct A {
        v1: vector<u64>,
        v2: vector<u64>,
    }
    spec A {
        invariant len(v1) == len(v2);
    }

    public fun push_A(a: &mut A) {
        let r = a;
        let v1 = &mut r.v1;
        let v2 = &mut r.v2;
        vector::push_back(v1, 1);
        vector::push_back(v2, 1);
    }

[FrodoBaggins74524]

It sounds like you're running into an issue with verifying the data invariant len(v1) == len(v2) in your push_A function. The problem is that in the current implementation, the function is modifying both v1 and v2 independently and in an non-atomic way, which means that at the intermediate moment when v1 is updated, but not v2, the data invariant is temporarily violated.

One possible solution to this issue would be to use a lock or a mutex to ensure that the updates to both v1 and v2 are atomic and happen simultaneously. Another solution would be to use a single vector that holds a pair of values instead of two separate vectors, and ensure that the invariant holds for the single vector.

It's also worth noting that in your second attempt to fix the problem by creating a reference to a and then modifying it, the issue remains the same, as the two vectors are still being modified independently.

It's good to see that you're aware of this problem and trying to find ways to solve it. It's always a good idea to test the code and see if the problem still persist and report it to the community.

[FrodoBaggins74524]

impl std::fmt::Debug for PathedIoError { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { f.debug_struct("PathedIoError") .field("path", &self.path) .field("inner", &self.inner) .finish() } }

In this example, the second field name is changed from "path" to "inner", ensuring that the two field names are unique and meaningful. This will fix the issue, and when you print the struct using the {:?} or {:#?} format string, it will show both fields, the path and inner fields.

[junkil-park]

@FrodoBaggins74524 , thanks for your comment. My colleague just merged a fix for this. Please feel to check it out: https://github.com/move-language/move/pull/820.