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.
- 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
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.