Bug in What4 prover backends

[robdockins]

There is some bug involving symbolic evaluation using What4 backends, probably involving the split primitive. It seems that the order of elements is reversed from what it should be.

Loading module Cryptol
Cryptol> :set prover=z3
Cryptol> :prove (\x y -> split (x#y) == [x:[32],y])
Q.E.D.
(Total Elapsed Time: 0.009s, using "Z3")
Cryptol> :set prover=w4-z3
Cryptol> :prove (\x y -> split (x#y) == [x:[32],y])
Counterexample
(\x y -> split (x # y) == [x : [32], y])
  0xffffffff 0x00000000 = False
(Total Elapsed Time: 0.027s, using "z3")
Cryptol> :prove (\x y -> split (x#y) == [y,x:[32]])
Q.E.D.
(Total Elapsed Time: 0.021s, using "z3")

[robdockins]

Turns out, the problem with split only occurs at bitvector types, and is because the extractWord operation is using the wrong bit order convention.