scribble produces potentially invalid code given a forall over an old expression

[cd1m0]

Given the following code:

pragma solidity 0.8.10;

contract Foo {
    uint[] a;

    /// #if_succeeds forall(uint i in old(a)) a[i] == 42;
    function balanceOf() public returns (uint) {
        a.pop();
    }
}

Scribble will produce the following code which will crash:

contract Foo is __scribble_ReentrancyUtils {
...
    uint[] internal a;

    function balanceOf() public returns (uint RET_0) {
        vars0 memory _v;
        unchecked {
            _v.old_0 = a;
        }
        RET_0 = _original_Foo_balanceOf();
        unchecked {
            _v.forall_0 = true;
            for (_v.i0 = 0; _v.i0 < _v.old_0.length; _v.i0++) {
                _v.forall_0 = a[_v.i0] == 42;
                if (!_v.forall_0) break;
            }
            if (!(_v.forall_0)) {
                emit AssertionFailed("0: ");
                assert(false);
            }
        }
    }

    function _original_Foo_balanceOf() private returns (uint) {
        a.pop();
    }
}

The issue is that the forall iterates over the precondition state of a (_v.i0 between 0 and _v.old_0.length), but the transpiled body indexes in the postcondition value of a (in a[_v.i0] == 42;). Note that the postcondition value of a has 1 fewer entries than the precondition, so there will be an out-of-bounds exception.

We have 2 options for a fix:

1.Disallow patterns like forall(i in old(...)) <use i in post-condition context>
2. Compile the bodies of for-loops like the one above to use the pre-condition value of the container we iterate over.

I think 1 is simpler and clearer. Going with 2 is complicated by the fact that its not clear what to do in the case forall(i in old(a)...old(b))? Or in the case forall(i in a...old(b))?

[cd1m0]

Note that this will be solved by #152