predicates describing bytes in memory

[andres-erbsen]

We have many separation-logic predicates for what is essentially bytes in memory. Here is a probably incomplete list, based on what arguments they take:

• array 1: list, implicitly of length < 2^32
• ptso_bytes: tuple, implicitly of length < 2^32
• scalarXX: word of fixed length
• Bignum: list, length explicitly passed in and asserted inside separation logic
• eq($@): list, truncated if too long

Additionally, for existentilly quantified bytes:

• anybytes
• Placeholder

Commentary:

I think ptsto_bytes is very painful for general use and I would like to eliminate it from as many places as possible.
eq(_$@_) and array1 are proven equivalent for lists of less than 2^32 elements; no urgency to replace on with another as far as I can see.
scalar currently lacks a lemma for casting to array or $@. I will probably just prove it, but do we think we want to keep the definition as-is anyway? It goes through ptsto_bytes...
Bignum has a lemma for converting to array 1 and back, good. Placeholder can be converted to Bignum.
anybytes has lemmas to array 1, I think lemmas to $@ are currently not present but should be easy either through array 1 or directly

[andres-erbsen]

For stackallocation, we need lemmas for conversion to bytes and back. For example, for scalar, we want

• a lemma that takes as en argument a word-typed variable and give an expression for a list of bytes that $@ the same address are equivalent to that scalar.
• a lemma that takes as an argument a variable of type list byte and gives a word expression such that scalar with that word is equal to $@ with these bytes.

It would be desirable to apply these lemmas automatically. In either direction, it is the more structured (non-bytes) side that determines the length. For exmaple, if the goal is scalar32 ?value addr * ?R, the proof automation should try to extract 4 bytes from the symbolic state at address addr. When recycling memory from a scalar, the amount of memory requested is secondary: a scalar32 always give you 4 bytes, even if you only wanted 2. This sounds kind-of obvious for scalars, but I am writing it down to make sure I don't mess it up on length-parametrized bignums.

[samuelgruetter]

I'm not a big fan of ptsto_bytes either, if we can slowly "phase it out" without too much refactoring, that'd be good.
I also agree that it's good to have lemmas to convert to bytes.
Regarding Scalars.v, I'm not very satisfied with it, and I think more experimentation to explore the ergonomics of different approaches would be good.

[andres-erbsen]

mit-plv/coqutil#44 would help with Scalars.v