do not use tuples in Semantics, Memory

[andres-erbsen]

See also: mit-plv/coqutil#131

[andres-erbsen]

This is a simple and unambitious refactor. Uses of tuples in semantics definitions are replaced with equivalent list-based definitions. Some proofs use these definitions directly, most rely incidentally on intermediate lemmas that involve tuples.

In longer term, the idea is to clean up some parts of the memory-layout code so they can be shared outside the context of Bedrock2 C. Memory.WithoutTuples was initially created when such reuse in fiat-crypto failed due to tuples. The path towards deleting the tuple-based definitions depends on what we want to do with riscv-coq.- IIRC, at least some part there quantifies over some tuples, so maybe it has a reason to use them, but perpahs the load-store definitions could be adapted in sync with bedrock2?

This change built on top of a tree that was both ahead and behind; rebase would likely be a bit of a chore but doable in a single pass.

[samuelgruetter]

We already tried this a while ago, and for the bedrock2 part, it looks nice, but when I looked into how to adapt riscv-coq, it just seemed that using tuples with a size given by a nat makes sense there and changing it to use lists would make it worse... But maybe "we" (where the quotes around "we" mean that I'm personally not so keen on doing refactorings myself :P) should try again? Or is there a way to keep riscv-coq unchanged, and only change bedrock2?

[andres-erbsen]

This less ambitious PR does not need riscv-coq changes to be merged. Do you remember what specific place in rscv-coq wanted tuples? If it's the abstract-monad-primitives interface, we could still leave tuples there and implement the relevant functions by calling the list versions, like we have started doing for LittleEndian.

[samuelgruetter]

This less ambitious PR does not need riscv-coq changes to be merged.

Ah that's cool 👍

Do you remember what specific place in rscv-coq wanted tuples? If it's the abstract-monad-primitives interface, we could still leave tuples there and implement the relevant functions by calling the list versions, like we have started doing for LittleEndian.

It's the abstract-monad-primitives interface, plus most instance implementations have a generic load and store that uses tuple byte n, with n any nat (but in practice, only 1, 2, 4, or 8).

[andres-erbsen]

Ok. I next time I feel like refactoring something new, I'll try replacing the implementations with ones that call list functions but keeping the interface.

[andres-erbsen]

mit-plv/fiat-crypto#2118