How to prove properties involving arrays?

[michael-emmi]

Proving the postcondition below seems to require expressing that f1 and f2 return true if and only if some element of a1 and a2 respectively are greater than zero.

pragma solidity ^0.5.0;

/// @notice invariant __verifier_eq(a1, a2)
contract A {
    int[] a1;
    int[] a2;

    /// @notice postcondition r1 == r2
    function g() public view returns (bool r1, bool r2) {
        r1 = f1();
        r2 = f2();
        return (r1, r2);
    }

    function f1() public view returns (bool) {
        for (uint i = 0 ; i < a1.length ; i++)
            if (a1[i] > 0)
                return true;

        return false;
    }

    function f2() public view returns (bool) {
        for (uint i = 0 ; i < a2.length ; i++)
            if (a2[i] > 0)
                return true;

        return false;
    }
}

As far as I can tell, solc-verify currently has no way to express such things. Is there any hope that some day this kind of thing might be supported?

[dddejan]

I guess you need quantifiers for this.

[dddejan]

@michael-emmi can this be done in SMACK? You would need loop invariant too seems like.

[michael-emmi]

Smack has never attempted this kind of thing, but it would indeed use quantifiers to express such specs (and loop invariants to verify the specs).

The issue I intended to raise seems independent from loop invariants: I’d like to be able to write specs for f1 and f2 which can be used by g. Of course verifying those specs will require loop invariants, but that seems like a separate issue. My interest here is whether solc-verify might adopt some specification function(s) which could expression that some predicate holds on some/all entries of an array/map. Such function(s) might be able to avoid general quantifiers.

[dddejan]

Yes, this would fall within the array property fragment that most likely Z3 and CVC4 support (i.e., can decide with suitable options). I somehow assumed you don't want to write the loop invariants, but if you do then it could be interesting to play with.

[hajduakos]

We discussed with @dddejan that instead of allowing quantifiers in general, we could come up with some syntax limited to these kind of array properties that are decidable.

[dddejan]

Since we already have

__verifier_sum_uint(ss[__verifier_idx_address].x)

we could add an array property predicate such as e.g.

__verifier_array_property_uint(
   0 <= __verifier_idx_uint && __verifier_idx_uint < n, 
   a[__verifier_idx_uint] > 0
)

Arguments:

1. index guard: predicate over index (index guard)
2. value constraint: predicate over index and array, where index is to be used only to index the array

For more details: http://theory.stanford.edu/~arbrad/papers/arrays.pdf

As this is becoming more common, we really need to figure some better way of declaring the index variables. Having predefined ones like __verifier_idx_uint is OK but is cumbersome and not extensible. For example array properties might want to say property(0 <= i < j < a.length; a[i] < a[j]).