Symbolic implementation of update needlessly bit-blasts index argument

[brianhuffman]

This proof command takes about 5 seconds with Z3 before returning a counterexample. (Much of this time is actually spent in Cryptol preparing to send the proof to z3, not in the prover itself).

:prove \(xs:[1024][8]) (i:[10]) -> update xs i 0 == xs

On the other hand, the same proof command with this alternative definition is about 10 times faster:

update' : {n, a, i} (fin n, fin i, 2^^i >= n) => [n]a -> [i] -> a -> [n]a
update' xs i y = [ if i == j then y else x | x <- xs | j <- [0...] ]

Using :set prover=offline shows that the first version produces a much larger smt output, and makes big mux-trees based on the bits of the index. The second version is much simpler, and only does equality comparisons on the index value.
We should reimplement the update primitive in the symbolic backend so that it avoids bit-blasting the index value.