search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
42 stars 24 forks source link

eradicating LittleEndian.combine #44

Open andres-erbsen opened 2 years ago

andres-erbsen commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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.