Factor out optimization surrounding array operations into What4

[lcasburn]

For example, we've built simplification rules surrounding arrays to simplify array terms to handle aliasing between updates. This would be better supported within What4 directly. Another example, array copy primitive broken into byte updates.