Library iris.bi.lib.counterexamples

This proves that in an affine BI (i.e., a BI that enjoys P ∗ Q ⊢ P), the classical excluded middle (P ∨ ¬P) axiom makes the separation conjunction trivial, i.e., it gives P -∗ P ∗ P and P ∧ Q -∗ P ∗ Q. Our proof essentially follows the structure of the proof of Theorem 3 in https://scholar.princeton.edu/sites/default/files/qinxiang/files/putting_order_to_the_separation_logic_jungle_revised_version.pdf

This proves that the combination of Löb induction (▷ P → P) ⊢ P and the classical excluded-middle P ∨ ¬P axiom makes the later operator trivial, i.e., it gives ▷ P for any P, or equivalently ▷ P ≡ True.

This proves that we need the ▷ in a "Saved Proposition" construction with name-dependent allocation.

We assume that we cannot update to false.

A bad recursive reference: "Assertion with name i does not hold"

This proves that we need the ▷ when opening invariants. We have two paradoxes in this section, but they share the general axiomatization of invariants.

Assumptions We have the update modality (two classes: empty/full mask)

We have invariants

We assume that we cannot update to false.

This completes the general assumptions shared by both paradoxes. We set up some general lemmas and proof mode compatibility before proceeding with the paradoxes.

The original paradox, as found in the "Iris from the Ground Up" paper.

On top of invariants themselves, we need a particular kind of ghost state: we have tokens for a little "two-state STS": start -> finish. start also asserts the exact state; it is only ever owned by the invariant. finished is duplicable. Posssible implementations of these axioms:

• Using the STS monoid of a two-state STS, where start is the authoritative saying the state is exactly start, and finish is the "we are at least in state finish" typically owned by threads.
• Ex () +_# ()

Now to the actual counterexample. We start with a weird form of saved propositions.

And now we tie a bad knot.

This is another proof showing that we need the ▷ when opening invariants. Unlike the two paradoxes above, this proof does not rely on impredicative quantification -- at least, not directly. Instead it exploits the impredicative quantification that is implicit in fupd. Unlike the previous paradox, the finish token needs to be persistent for this paradox to work. This paradox is due to Yusuke Matsushita.

On top of invariants themselves, we need a particular kind of ghost state: we have tokens for a little "two-state STS": start -> finish. start also asserts the exact state; it is only ever owned by the invariant. finished is persistent. Posssible implementations of these axioms:

• Using the STS monoid of a two-state STS, where start is the authoritative saying the state is exactly start, and finish is the "we are at least in state finish" typically owned by threads.
• Ex () +_# ()

Now to the actual counterexample. A version of ⊥ behind a persistent update.

A delayed-initialization invariant storing B.

If we can ever finish initializing the invariant, we have a contradiction.

If we can even just create the invariant, we can finish initializing it using the above lemma, and then get the contradiction.

There's a magic moment here where we have the invariant open, but inside finished_contradiction we will be proving a fupd M1 and so we can open the invariant *again*. Really we are just building up a thunk that can be used later when the invariant is closed again. But to build up that thunk we can use resources that we just got out of the invariant, before closing it again.

Of course, creating the invariant is trivial.

This proves that if we have linear impredicative invariants, we can still drop arbitrary resources (i.e., we can "defeat" linearity). We assume cinv_alloc without any bells or whistles. Moreover, we also have an accessor that gives back the invariant token immediately, not just after the invariant got closed again. The assumptions here match the proof rules in Iron, save for the side-condition that the invariant must be "uniform". In particular, cinv_alloc delays handing out the cinv_own token until after the invariant has been created so that this can match Iron by picking cinv_own γ := fcinv_own γ 1 ∗ fcinv_cancel_own γ 1. This means cinv_own is not "uniform" in Iron terms, which is why Iron does not suffer from this contradiction. This also loosely matches VST's locks with stored resource invariants. There, the stronger variant of the "unlock" rule (see Aquinas Hobor's PhD thesis "Oracle Semantics", §4.7, p. 88) also permits putting the token of a lock entirely into that lock.

Assumptions. We have the mask-changing update modality (two classes: empty/full mask)

We have cancelable invariants. (Really they would have fractions at cinv_own but we do not need that. They would also have a name matching the mask type, but we do not need that either.)

Some general lemmas and proof mode compatibility.

Counterexample: now we can make any resource disappear.