Verification of existentially quantified postcondition fails

[zhao-nan]

pragma solidity ^0.5.0;

contract ExistTest {
    bool[] arr;

    /// @notice postcondition exists (uint u) (0 <= u && u < arr.length && arr[u]) == result
    function test() public view returns (bool result) {
        bool res = false;
        /// @notice invariant exists (uint j) (0 <= j && j < i && arr[j]) == res
        for (uint i = 0; i < arr.length; i += 1) {
            if (arr[i]) {res = true;}
        }
        return res;
    }
}

The above should be verifiable, but solc-verify reports that the postcondition might be violated.

[dddejan]

@zhao-nan The support for quantifiers is limited to prenex form: all quantifiers are at the front. The postcondition you wrote doesn't parse as you would like to, instead it states that (note the extra brackets).

    /// @notice postcondition exists (uint u) ((0 <= u && u < arr.length && arr[u]) == result)

The reasons for this are rather technical (we rely on the compiler to parse expressions). Basically we parse the quantifiers first, and then parse the rest as one expression.

[dddejan]

Here is a spec that should prove what you'd like (I think). It's a bit verbose.

pragma solidity >=0.5.0;

contract ExistTest {
    bool[] arr;

    /// @notice postcondition property(arr) (u) (!arr[u] || result)
    /// @notice postcondition exists (uint u) (0 <= u && u < arr.length && arr[u]) || !result
    function test() public view returns (bool result) {
        bool res = false;
        /// @notice invariant (0 <= i && i <= arr.length)
        /// @notice invariant forall (uint j) !(0 <= j && j < i) || !arr[j] || res
        /// @notice invariant exists (uint j) (0 <= j && j < i && arr[j]) || !res
        for (uint i = 0; i < arr.length; i += 1) {
            if (arr[i]) {res = true;}
        }
        return res;
    }
}

Then, I can prove it with cvc4

$ ./solc-verify.py Issue170.sol --solver cvc4
ExistTest::test: OK
ExistTest::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
No errors found.

[dddejan]

Actually, your original spec can also be proved with a strengthened invariant

pragma solidity >=0.5.0;

contract ExistTest {
    bool[] arr;

    /// @notice postcondition exists (uint u) (0 <= u && u < arr.length && arr[u]) == result
    function test() public view returns (bool result) {
        bool res = false;
        /// @notice invariant 0 <= i && i <= arr.length
        /// @notice invariant exists (uint j) (0 <= j && j < i && arr[j]) == res
        for (uint i = 0; i < arr.length; i += 1) {
            if (arr[i]) {res = true;}
        }
        return res;
    }
}

$ ./solc-verify.py Issue170.sol --solver cvc4
ExistTest::test: OK
ExistTest::[implicit_constructor]: OK
Use --show-warnings to see 1 warning.
No errors found.

[dddejan]

Quantified specs are generally hard to get right and push through. To illustrate the problem with the spec you provided, we can prove the following.

pragma solidity >=0.5.0;

contract ExistTest {
    bool[] arr;

    /// @notice postcondition exists (uint u) (0 <= u && u < arr.length && arr[u]) == result
    function test() public view returns (bool result) {
        return false;
    }
}

[zhao-nan]

Thanks for your explanation, and especially for the example! I agree that quantified specifications are challenging. That makes it very hard to reason about any program with loops over arrays, though. (Although in Solidity, these don't happen as often as in other programming languages.. but they still exist!) Thanks again for the very quick reply!