set bigendian=1 in formal proofs of decoder (TODO: bigendian=0)