Support more general initialization of arrays in GenC

[vkuncak]

GenC partially evaluates certain initialization patterns, possibly due to Array.fill forcing side effects. We should support more initialization patterns to ensure that both arrays are initialized (even when they are static) and that we can write initialization code given by a function of the index or even a foldLeft.

[vkuncak]

In particular, implementation of tabulate would be very useful. One issue is that such arrays would be values that may not be representable using z3's array theories, otherwise it would embed classical HOL.

[vkuncak]

The way to handle tabulate is to add a pure extern .toList function on arrays to the library. Then add lemmas saying that arr(i) == arr.toList(i).

We then add a postcondition of tabulate that specifies what its list is, for example using List.tabulate (which exists in Scala, so it's good to add).

Ideally also we also add a specification of array update saying how array changes its list (not sure if it's easy to specify that due to statefulness).