CBMC: Avoid splitting multi-dimensional arrays into multiple allocations

[hanno-becker]

To work with the semantics of __CPROVER_is_fresh / memory_no_alias, we are currently forced to split multi-dimensional arrays into separate declarations, so that the subarrays are seen as separate objects in the CBMC sense. This is quite inconvenient and introduces a fair amount of visual clutter.

Study if there is a way to modify the relevant specs so they don't require the arguments to be in separate objects.

[hanno-becker]

This mainly means rewriting various x4 specs to no longer use is-fresh, but explicitly state the placement of pointers within a single parent object. This is a bit cumbersome in poly_rej_uniform_x4, which one may need to rewrite to use a single monolithic buffer, and have e.g. xof_x4_squeezeblocks(buf, N, state) unfold to shake128x4_squeezeblocks(buf + {0,1,2,3} * alignup(N * SHAKE128_RATE), (N), (state))

[hanno-becker]

This will be easy with #688