Redo Heapster Lifetime Subsumption

[eddywestbrook]

A key aspect of lifetimes is the ability to have one lifetime contain in another, i.e., to have the bigger lifetime subsume the smaller one. Previously, the way this was modeled in Heapster was to put the lowned permissions of the bigger lifetime l1 inside the lowned permissions of the smaller lifetime l2, i.e., to represent subsumption by having a permission like

l2 : lowned (ps_in2 -o ps_out2, l1:lowned (ps_in1 -o ps_out1))

The idea is that l1 subsuming l2 means you can't end l1 until after you end l2. Unfortunately, this gets gross, because you have implications inside implications. Further, it means you can't have a bigger lifetime subsume multiple smaller lifetimes, which is actually useful and possibly necessary in a lot of case for, e.g., Rust code.

Luckily, I recently worked out the semantics of a lifetime ownership permission of the form

l1 : lowned [ls] (ps_in1 -o ps_out1)

where ls is a list of lifetimes that are subsumed inside of l1. Lifetime l1 cannot be ended unless ls is empty, but a subsumed lifetime in ls can be removed from the lowned permission of l1 once it has finished. To indicate that a lifetime in ls has finished, we also include a new permission construct

l2 : lfinished

along with an implication rule that allows a lifetime in the ls of an ownership permission to be removed if it has finished.

This approach solves the above problems, because lowned permissions no longer contain other lowned permissions and because lifetimes can now contain more than one subsumed lifetime. Further, it makes lifetime permissions more compositional, allowing the implication prover to deal with different lifetimes separately.

Note that this PR is based on #1406, and so should wait for that PR to be merged before it is merged.

[glguy]

I don't understand the algorithm well enough to have a useful opinion about how sound the implementation is, so I can't weigh in on that. (I don't think that's what you're looking for from me, either).

From a code perspective things seem good other than the parser comment I made above.

This code seems to have a copy of the previous PR included which makes me worry that it's out of sync with master. (and which made doing the review a bit trickier)