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.