Zmod + Memory prototyping branch

[andres-erbsen]

This is on top of rocq-prover/stdlib@499c6e5 or later; should work if that's placed in sibling directory and built with dune build -p rocq-stdlib. However, as of right now the later commits do not actually depend on Zmod and could be cherry-picked to work with earlier stdlib. (done)

• I scavenged everything I remembered from the top of my head that we want from bedrock2; there may be some more.
• I took a quick look at otbn and didn't immediately find anything I was sure we'd want here
• Suggestions welcome otherwise as well
• I think we do want something about storing words as opposed to Z-s. However, currently store size is a nat, not a Z, so probably next (small) step would be to figure out at which layer to do the conversion.

For building up the hierarchy of C-style memory representations, I think the next to add are

• packed structs: each field encoded to bytes individually, fields concatenated with ++ as lists of byte, mapped to memory using $@, and coerced to a separation-logic predicate. For example, m =* (le_split 4 x ++ le_split 4 y) $@ a * R, or the ethernet-packet spec in garagedoor paper.
• arrays containing lists of elements: same, except there is a list of "fields", and flat_map encode over that list goes in the argument of $@. For example, m =* flat_map (le_split 4) xs $@ a * R

For reasoning about these constructs, I think of lemmas as falling into two categories based on whether their unification-driving arguments (universally quantified variables) reference specification variables or implementation variables. With specification variables for structs, we have e.g. (xs ++ ys)$@a <--> xs$@a * ys$@(a+length xs) and the specialization of that for ys=y::ys'. On the other hand, a program indexing into that array with a s-byte load at address b would naively get firstn s (skipn (b-a) (xs ++ ys)). The latter is a mouthful, but it can be simplified with lemmas for firstn of ++ and so on. A similar consideration appears for arrays when casting uninitialized memory bs$a into an array specified as map (le_split 4) ?xs $@ a: the variable xs can be instantiated as map le_combine (chunk 4 bs) (but length divisibility by 4 is still needed for the two to be equal).

[samuelgruetter]

Now that we have the way of implementing words with Zmod, do we still need to abstract all files over the word implementation and ok proofs?

[andres-erbsen]

Yes, this branch is for experimentation like this.