Extend dynamic array verification beyond fixed length

Dynamic array support implemented in https://github.com/runtimeverification/kontrol/pull/321 relies on the assumption that the array length is fixed to a particular concrete number. We should look into removing this assumption (and the resolution of the corresponding compiler-inserted checks on calldata well-formedness), likely based on the abstraction suggested by @PetarMax:

 // --- bytes array abstraction ---

    // -- offsets --

    syntax Bool ::= #bytesArrayOffsets ( Bytes, Int, Int, List ) [function]

    // Empty case: no offsets left
    rule #bytesArrayOffsets(_:Bytes, START, 0, .List) => true
      requires 0 <=Int START
      [simplification]

    // Non-empty case: at least one offset
    rule #bytesArrayOffsets(B:Bytes, START:Int, SIZE:Int, ListItem(O:Int) OFFSETS) =>
                // There is at least one offset, which is registered in the leading 32 bytes
                #asWord( #range(B, START, 32) ) ==Int O
                // followed by the remaining offsets
        andBool #bytesArrayOffsets(B, START +Int 32, SIZE -Int 1, OFFSETS)
      requires 0 <=Int START andBool 0 <Int SIZE andBool 0 <=Int O
      [simplification]

    // -- elements --

    syntax Bool ::= #bytesArrayElements ( Bytes, List, List, Int ) [function]

    // Empty case: no elements left
    rule #bytesArrayElements(_:Bytes, .List, .List, 0) => true
      [simplification(50)]

    rule #bytesArrayElements(B:Bytes, ListItem(O:Int), ListItem(E:Bytes), LENGTH) =>
                // First 32 bytes are the length of the leading element E
                #asWord ( #range(B, O, 32) ) ==Int lengthBytes(E)
                // followed by the actual leading element
        andBool #range(B, O +Int 32, lengthBytes(E)) ==K E
                // and the associated padding
        andBool #asInteger ( #range(B, O +Int 32 +Int lengthBytes(E), (notMaxUInt5 &Int (lengthBytes(E) +Int 31)) -Int lengthBytes(E)) ) ==Int 0
                // and the rest of the elements
        andBool LENGTH ==Int O +Int 32 +Int ( notMaxUInt5 &Int (lengthBytes(E) +Int 31) )
      requires 0 <=Int O
      [simplification(45)]

    // Non-empty case: at least one element
    rule #bytesArrayElements(B:Bytes, ListItem(O:Int) OFFSETS, ListItem(E:Bytes) ELEMENTS, LENGTH) =>
                // First 32 bytes are the length of the leading element E
                #asWord ( #range(B, O, 32) ) ==Int lengthBytes(E)
                // followed by the actual leading element
        andBool #range(B, O +Int 32, lengthBytes(E)) ==K E
                // and the associated padding
        andBool #asInteger ( #range(B, O +Int 32 +Int lengthBytes(E), (notMaxUInt5 &Int (lengthBytes(E) +Int 31)) -Int lengthBytes(E)) ) ==Int 0
                // and the rest of the elements
        andBool #bytesArrayElements(B, OFFSETS, ELEMENTS, LENGTH)
      requires 0 <=Int O
      [simplification(50)]

    // -- bytesArray --

    syntax Bool ::= #bytesArray ( Bytes, Int, List, List, Int ) [function]

    rule #bytesArray(B:Bytes, SIZE:Int, OFFSETS:List, ELEMENTS:List, LENGTH:Int) =>
                // Leading 32 bytes contain the number of elements
                #asWord ( #range(B, 0, 32) ) ==Int SIZE
                // followed by the offsets at which each of the elements can be found
        andBool #bytesArrayOffsets(B, 32, SIZE, OFFSETS)
                // and then the elements themselves, possibly scattered throughout memory
        andBool #bytesArrayElements(B, OFFSETS, ELEMENTS, LENGTH)
                // and the entire memory is large enough to hold the array
        andBool lengthBytes(B) ==Int maxInt(32, LENGTH)
      [simplification]

Start by reviewing the dynamic array support from pull request #321 and the proposed bytes-array abstraction in this issue. Determine how verification can work without a fixed concrete length and how the corresponding compiler-inserted calldata well-formedness checks should be handled. Done means dynamic arrays are verified beyond the fixed-length assumption.