eradicating LittleEndian.combine

[andres-erbsen]

I have the feeling that using tuples in that file was an unfortunate choice and benefits almost nothing; getting rid of it would be a clear improvement. @samuelgruetter do you agree? If so, plan:

1. define LittleEndian.combine and LittleEndian.split in terms of LittleEndianList.combine and LittleEndianList.split
2. prove the lemmas we currently have about them? this might actually be more annoying than the next point
3. change the callers to use LittleEndianList directly
4. atomic rename LittleEndianList -> LittleEndian across all repositories (but we get most of the benefit even if we don't do this)

Thoughts?

supersedes #34

[andres-erbsen]

After some discussion: it may make sense to update callers in two phases, first everything above bedrock2.exec and then everything below, duplicating bedrock2.exec in the interim (with a proof that the two versions are equivalent).

[andres-erbsen]

bedrock2, rupicola, and fiat-crypto primarily use LittleEndianList after https://github.com/mit-plv/fiat-crypto/pull/1085/files ; there is still some LittleEndian in the bedrock2 compiler and more in riscv-coq.

[andres-erbsen]

This function is now only used in riscv-coq run1 calling instruction decoding, probably ripe for removal.