Equality of memory arrays from storage copies.

[michael-emmi]

I expected the following to work:

$ cat a.sol && solc-verify.py a.sol 

pragma solidity ^0.5.0;

/// @notice invariant __verifier_eq(a1, a2)
contract C {
    int[] a1;
    int[] a2;
        
    /// @notice postcondition __verifier_eq(r1, r2)
    function f() public view returns (int[] memory r1, int[] memory r2) {    
        r1 = a1;
        r2 = a2;
        return (r1, r2);
    }
}

C::f: ERROR
 - a.sol:9:5: Postcondition '__verifier_eq(r1, r2)' might not hold at end of function.
C::[implicit_constructor]: OK
C::[receive_ether_selfdestruct]: OK
Errors were found by the verifier.

In the generated Boogie code, one can see that the comparison happens on the int-array pointers:

type {:datatype} int_arr_type;
type int_arr_ptr;
var mem_arr_int: [int_arr_ptr]int_arr_type;

procedure … f#29(__this: address_t, __msg_sender: address_t, __msg_value: int)
    returns (r1#11: int_arr_ptr, r2#14: int_arr_ptr)
...
    ensures … (r1#11 == r2#14);

rather than on the int-arrays they point to:

    ensures … (mem_array_int[r1#11] == mem_array_int[r2#14]);

[hajduakos]

For me this is intuitive, because most programming languages also work this way (like == in Java, or comparing pointers in C++). But we can easily make a new function, say verifier_content_eq which will compare the contents of the references. (Or we can just make the current verifier_eq to work this way, but I think it is still useful to have an operator that can compare references.)

One issue though is with nested arrays. Nested memory arrays have references as their elements, so a "deep" equality check must de-refer all elements recursively, which seems to require quantifiers.

[michael-emmi]

Ah, good point. Would a dereferencing operator make sense in that case?

[hajduakos]

Yes, I was also thinking about some dereferencing operator, like __verifier_eq(deref(r1), deref(r2)). That could also help when comparing memory with storage (#55), because you could just derefer one argument (__verifier_eq(deref(r1), a1)). @dddejan any thoughts?

[dddejan]

I think it's a bit more complicated than it seems. The allocation and copying from storage to memory will require treatment of loops to prove anything?

[michael-emmi]

Would copying storage to memory require loops?

In the use case we have at the moment, we want to equate the memory arrays returned by two functions, in which each returns a copy of its respective storage array — and those storage arrays are presumed equal initially.

Given your encoding of arrays as SMT datatypes, this sort of check looks straightforward — only equality reasoning is required.

[dddejan]

Would copying storage to memory require loops?

In principle yes, for non-basic types. The datatype representation only works for storage, the memory data is all references and copying stuff over is basically done by hand. In this particular case (int) it's OK, the memory array contains ints so an SMT2 assignment works. But had the memory array contained a complex type (struct, another array) they will be references and all copying from storage has to be done manually, i.e., with a loop that dereferences individual elements.

For example the following is not yet supported

pragma solidity ^0.5.0;
pragma experimental ABIEncoderV2;

/// @notice invariant __verifier_eq(a1, a2)
contract C {

    struct S {
      int x;
    }  

    S[] a1;
    S[] a2;
        
    /// @notice postcondition __verifier_eq(r1, r2)
    function f() public view returns (S[] memory r1, S[] memory r2) {    
        r1 = a1;
        r2 = a2;
        return (r1, r2);
    }
}

I think from a language perspective @hajduakos's suggestion for a dereference operator sounds good. But, the implementation (in boogie) of the dereference would need to be implemented as a manual deep copy, which might interfere with proving stuff. @hajduakos is that right?

[hajduakos]

Yes, currently copying between memory and storage arrays is limited to cases where the array elements are primitive types. Making a copy would require a loop with an invariant, possibly with an universal quantifier to say that all elements up to the loop counter are equal (recursively if the elements are again complex types).

In the postconditions, for examples with primitive array elements, a "shallow" dereference operator would work. For arrays with complex types, we would probably need a quantified expression that each element is equal when dereferenced.

[hajduakos]

For structs deep copy is not an issue because we can do the dereferencing manually as the number of members is compile time constant.