word_to_bytes

[mktnk3]

This PR adds word_to_bytes to byteTheory. It converts w:’a word to a list of length bytes_in_word, consisting of word8 segments of w. Also includes several related lemmas.

[mktnk3]

I should mention that word_to_bytes_aux is what I am currently using to take “sub-word” information out of a word (as part of an argument to call_FFI to write to the external memory, in this particular case). For the time being we only need to read out a byte (for byte-access), but if we want 16bit-access, etc., we can use this function to get a byte-list of part of a word. So, we could rename this to make it seem less aux if that’s better.
But it is also entirely possible not to use this aux function. We can always convert the whole word to a byte list (of length bytes_in_word) and take only the elements needed.