Encoding functions with finite support as maps

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

41 stars 24 forks source link

Encoding functions with finite support as maps #31

Closed andres-erbsen closed 4 years ago

andres-erbsen commented 4 years ago

Currently implemented:

lists as maps with nat keys
lists as maps with nat keys with some nat offset
lists as maps with Z keys
lists as maps with Z keys with some Z offset
lists as maps with word keys
lists as maps with word keys with some word offset

The main advantage of this construction is that it has a complete get law for the resulting maps, allowing to prove integer bounds on an address that was found to be within the constructed memory.

Please skim the definitions to check that they match your understanding of what we want in coqutil.

andres-erbsen commented 4 years ago

The CI I failure is 8.10 lia, probably on Z<->nat conversions. I'll fix.

andres-erbsen commented 4 years ago

I now realize that there is a naming conflict between the existing notion of of_list (which takes a list of pairs) and this notion of of_list which uses the indices of list elements as the first components of the imagined list of pairs. Thoughts?

samuelgruetter commented 4 years ago

So far, we have achieved this kind of functionality by combining List.unfoldn with map.of_list_zip, or tuple.unfoldn with map.of_tuple, but if you think this new way works better, I'm happy to add it to coqutil, I'd just prefer to not have a naming conflict for of_list.

andres-erbsen commented 4 years ago

Do we have comparable proofs about these functions?

andres-erbsen commented 4 years ago

Note that the name conflict is currently avoided in a dissatisfying way (of_list_nat), do you have a plausible alternative on mind?

samuelgruetter commented 4 years ago

Do we have comparable proofs about these functions?

Map.Properties contains many lemmas about these, but not in a very principled way. There's get_of_list_In_NoDup, many putmany_of_list_zip_... lemmas, and you can use putmany_of_list_zip_to_putmany to get to use lemmas about putmany instead of putmany_of_list_zip, eg get_putmany_right. It's messy enough that I'd be happy to add something new to coqutil and try whether it works better.

Note that the name conflict is currently avoided in a dissatisfying way (of_list_nat), do you have a plausible alternative on mind?

As long as there's no literal naming conflict, it's fine, but yeah maybe of_nat_key_seq, or of_adjacent_nat_keys, something in this direction?