Unable to use forall on arrays with elements of used-defined type

[blitz-1306]

Consider the following sample:

contract Test {
    struct MyStruct {
        uint i;
    }

    ///#if_succeeds forall(MyStruct elem in arg) true;
    function example(MyStruct[] calldata arg) public returns (bool) {
        return true;
    }
}

Expected Scribble to be able to handle user-defined types in forall but got crash:

scribble/dist/bin/scribble.js:421
            throw e;
            ^

TypeError: name.split is not a function
    at Object.resolveAny (scribble/node_modules/solc-typed-ast/dist/ast/definitions.js:248:27)
    at makeUserDefinedType (scribble/dist/spec-lang/expr_parser.js:27:39)
    at peg$c286 (scribble/dist/spec-lang/expr_parser.js:541:16)
    at peg$parseUserDefinedType (scribble/dist/spec-lang/expr_parser.js:7890:22)
    at peg$parseSimpleType (scribble/dist/spec-lang/expr_parser.js:7621:38)
    at peg$parseArrayType (scribble/dist/spec-lang/expr_parser.js:7906:14)
    at peg$parseMappingType (scribble/dist/spec-lang/expr_parser.js:8178:18)
    at peg$parsePointerType (scribble/dist/spec-lang/expr_parser.js:8210:14)
    at peg$parseFunctionType (scribble/dist/spec-lang/expr_parser.js:8655:18)
    at peg$parseFor_All (scribble/dist/spec-lang/expr_parser.js:1145:30)

Looking into a stacktrace gives that there is an issue with resolveAny() in solc-typed-ast. However we should clarify if such things expected to work and cover functionality by test samples.

[blitz-1306]

It also appears that fully qualified name is also not an option due to bug in grammar: https://github.com/ConsenSys/scribble/blob/3a78ad19c294a81503aa63a57f2c90b9c77b44df/src/spec-lang/expr_grammar.pegjs#L623-L625

There is no name variable accessible for the callback with base.field notation. I guess it should be something like:

return makeUserDefinedType(base.name + '.' + field.name, options, location());

With local fix:

TypeError: The type for elem is not compatible with the start range type int_const.

In:

if_succeeds forall(Test.MyStruct elem in arg) true;

that is produced by checkIntIterVar() in https://github.com/ConsenSys/scribble/blob/3a78ad19c294a81503aa63a57f2c90b9c77b44df/src/spec-lang/tc/typecheck.ts#L1696-L1721

[blitz-1306]

Still, we curretly support only index/key types in forall and not element value types. So following sample passes:

contract Test {
    struct MyStruct {
        uint i;
    }

    ///#if_succeeds forall(uint256 i in arg) arg[i].i > 0;
    function example(MyStruct[] calldata arg) public returns (bool) {
        return true;
    }
}

It seems that docs are the source of confusion. However we also better to produce clear errors to state what Scribble allows in such cases. I will leave the issue open, as there are few smaller bugs, that need to be addressed in order to explicitly state what forall allows and expects.

[cd1m0]

@blitz-1306 is correct, the bug is in the grammar. The rule for UserDefinedType should be:

UserDefinedType =
    base: Identifier "." field: Identifier {
        return makeUserDefinedType(base.name + '.' + field.name, options, location());
    }
    / name: Identifier {
        return makeUserDefinedType(name.name, options, location());
    }

Note that both cases were wrong. In addition our error message is kinda poor here:

tmp.sol:6:36 TypeError: The type for elem is not compatible with the start range type int_const.

int_const is not really a user-friendly type name. And also we should mention that elem is the index variable, and its type we expect should be for iterating through an array. Perhaps:

tmp.sol:6:36 TypeError: The type MyStruct of the iterator variable `elem` is not compatible with iterator type of `arg`.