Static arrays

[lefterislazar]

This PR adds support for static arrays in contract storage and constructor/behavior arguments. It also modifies logic related to the interaction with the SMT solver, to accommodate new SMT checks required by array semantics, and to enable new cases for testing.

AST additions and Typing for Static Arrays

• Untyped.hs:

  • NestedList data structure: A tree-structure of arbitrary depth with list endpoints, used to represent array literals of any level of nesting. The type alias ExprList holds lists of expressions and positional information.
  • AssignArray: Represents initialization of an array storage variable, using the ExprList structure.
  • EMapping -> EIndexed: Entries to mappings and arrays have the same AST representation at this level, renamed to reflect that.

• Typed.hs:

  • SArray: Constructor for Ref representing an array. Similar to SMapping with the addition of array bounds information for each index.

• Type.hs:

  • Checks that ExprList represents a valid array literal i.e. at each level of the tree, all arrays have the same number of sub-arrays.
  • Checks compatibility of array sizes of storage type and the assigned literal.
  • Type-checks each element of the literal against the storage base type.
  • Each element initialization is represented as a separate StorageUpdate in the typed AST.
  • Checks each array entry for correct amount of indexing and Integer type of indices' expressions.

SMT passes

Added 2 new SMT passes in Consistency.hs.

• checkArrayBounds: Ensures that no storage state and calldata values can lead to an out-of-bounds array entry, given the corresponding conditions.
• checkRewriteAliasing: Ensures that no storage state and calldata values can lead to separate StorageUpdates updating the same storage location, given the corresponding conditions.

SMT modifications

Added the CalldataLocation datatype, that serves the same function as StorageLocation but for references that start from a CVar at their root. This allows for the creation of calldata versions of the locFromX family of functions in Syntax.hs, which are used in the SMT passes to collect all accesses to arrays and mappings.

In addition, modified logic affecting storage declarations and integer bounds preconditions, to avoid problems with Model acquisition from the SMT solver in cases of failure.

TODOs

• Currently only arrays of AbiType are supported, meaning no arrays of contracts or mappings.
• Currently no arrays as final mapping values.
• Mass array updates.
• Carry over some nesting logic to nested mappings.

Miscellaneous

• Added tests for array features
• Updated test outputs
• Updated .gitignore for Rocq renaming