Add append-only list RA to Iris
Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of #244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote a version of this, which was forked at some point by @jtassaro for Perennial while also adding a logic-level wrapper for auth (mlist T) with the following three core assertions:
- authoritative ownership of the full trace
- persistent ownership that some list is a prefix of the trace
- persistent ownership that index i in the trace has some particular value
Perennial also has another version of this by @tchajed that is based on (the Perennial version of) gmap_view. And finally, @msammler has his own implementation that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.