# Add laws to allow "undiscarding" points-tos

Merged requested to merge johannes/iris:undiscard-laws into master

Discardable fractions are regular fractions, along with an extra element `DfracDiscarded` that tells you that some fraction `q` (but you don't know how large) has been "discarded", which is a "persistent" dfrac that witnesses that `DfracOwn 1` is now impossible to reach. This is very useful for e.g. constructing points-tos, which can be made persistent and unchangeable by "discarding" their fraction.

Intuitively, owning such a discarded fraction is equivalent to owning `∃ q, DfracOwn q`, which (while not persistent) is also freely duplicable. This merge request formalizes this intuition, by proving the following law:

`DfracDiscarded ~~>: λ k, ∃ q, k = DfracOwn q`

What this law allows is "undiscarding" a discarded fraction, allowing it to be turned back into an owned one. This can then be generalized to all "dfractional" resource algebras, in particular points-tos (the fragments of `gmap_view`) and the authorative parts of everything constructed via `auth`. This merge request also contributes the corresponding frame-preserving update laws for these algebras.

This law is then used to prove the following law about points-tos and other separation logic resources that can be made persistent.

`l ↦□ v ==∗ ∃ q, l ↦{# q} v`

## Why is this useful?

One use case for this is "points-to trading." The idea there is that one sets up an invariant that allows one to trade two different kinds of points-tos for each other. As a concrete example, imagine we have `pointsto_A k q v` describing ownership of a heap `A` (storing `v : valueA`), and `pointsto_B k q v'` describing ownership of some heap `B` (storing `v' : valueB`). Now, both heaps are "linked" in such a way as that one can only ever have either kind of points-to (for example, one heap is the "low-level encoding" of the other, and so both describe different views of the same data, and thus it makes a lot of sense to link them such that the user only ever has one view available).

For example, such a trading invariant might look like this: `pointsto_A k q v ∨ pointsto_B k q v'` --- i.e. the invariant stores exactly one of the points-tos, and when given the other can "exchange" it. With this, one can provide rules for exchanging `pointsto_A` for `pointsto_B`.

This invariant is easy to generalize to also allow trading fractional points-tos: `∃ (qA qB : Qp), ⌜qA+qB=1⌝ ∗ pointsto_A k qA v ∗ pointsto_B k qB v'` (pretending that either q can be 0 to describe the original "only one side" case from above)

However, generalizing to discarded points-tos is not straightforward: For implementing this, the mechanism would receive a discarded points-to of side A, and need to produce a discarded points-to of side B. To create this points-to of side B, it needs to know "how much" to discard of the fractional amount of `pointsto_B` it is currently storing.

With this merge request, adding support for trading discarded points-tos becomes easy:

• First, "undiscard" the points-to to make it fractional
• Then, trade the fractional points-tos using the already existing support for trading fractional points-tos
• Finally, discard the newly produced points-to from the other side to produce a new discarded points-to

This approach is nice because it gives you "discarded points-to trading" for free--you do not need to change the invariant maintained by the switching logic.

Edited by Johannes Hostert