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.