The Iris Tutorial in Lean

6. The Persistently Modality🔗

6.1. Introduction🔗

In separation logic, propositions are generally not duplicable. This is because resources are generally exclusive. However, resources do not have to be exclusive. A great example of this is read-only memory. There is no danger in letting many threads access the same location simultaneously if they can only read from it. Hence, it would not make sense to require that ownership of those locations be exclusive. Motivated by this, we introduce a new modality denoted the persistently modality, written □ P, for propositions P. The proposition □ P describes the same resources as P, except it does not claim that the resources are exclusive — hence □ P can be duplicated. Persistent propositions hence act like propositions in an intuitionistic logic, which is why iris-lean's proof mode also refers to the corresponding context as the intuitionistic context.

A proposition is persistent when P ⊢ □ P. That is, assuming P, we need to show that P does not rely on any exclusive resources. Persistency is preserved by most connectives, so proving that a proposition is persistent is usually a matter of showing that the mentioned resources are shareable. Which resources are shareable depends on the specific notions of resources being used. For the resource of heaps, a location can be marked as read-only, making it shareable. The associated points-to predicate hence becomes persistent. We will see an example of this later.

Propositions that do not rely on resources altogether are trivially persistent. We have already given those types of propositions a name: pure. This is also why we do not have to split the non-spatial context when using isplitl/isplitr; all pure propositions are persistent, hence duplicable.

Of course, not all persistent propositions are pure (e.g. persistent points-to predicates). Thus, the Iris Proof Mode provides a third context just for persistent propositions, called the intuitionistic context. Pure propositions can go in all three contexts. Persistent propositions can go in the spatial or intuitionistic context. And all other propositions are limited to the spatial context only. iris-lean uses the typeclass Iris.BI.Persistent to identify persistent propositions.

open Iris Iris.BI Iris.HeapLang namespace Persistently variable {hlc} {GF : BundledGFunctors} [HeapLangGS hlc GF]

The cases pattern #H moves a persistent hypothesis into the intuitionistic context.

theorem pers_context (P Q : IProp GF) [Persistent P] : P -∗ Q -∗ P ∗ Q := GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ⊢ P -∗ Q -∗ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ PGF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗HQ : Q ⊢ Q All goals completed! 🐙

The intuitionistic context is shared across both subgoals of an isplitl/isplitr: HP remains available after the split.

By contrast, putting HP into the spatial context discards persistency:

theorem not_in_pers_context (P Q : IProp GF) [Persistent P] : P -∗ Q -∗ P ∗ Q := GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ⊢ P -∗ Q -∗ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ∗HQ : Q ⊢ P ∗ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ⊢ PGF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HQ : Q ⊢ Q GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ ∗HQ : Q ⊢ Q All goals completed! 🐙

Persistent propositions are duplicable.

theorem pers_dup (P : IProp GF) [Persistent P] : P ⊢ P ∗ P := GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ P ⊢ P ∗ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P ∗ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ PGF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙

Persistent propositions satisfy several nice properties simply by being duplicable (P ⊢ P ∗ P). For example, P ∧ Q and P ∗ Q coincide when either P or Q is persistent; likewise, P → Q and P -∗ Q coincide when P is persistent. The relevant iris- lean lemmas are Iris.BI.persistent_and_sep and Iris.BI.impl_wand.

The Iris Proof Mode knows these facts and allows isplit to introduce ∗ when one of its arguments is persistent.

6.2. Proving Persistency🔗

To prove a proposition □ P, we must prove P without assuming any exclusive resources. In other words, we have to throw away the spatial context when proving P.

theorem pers_intro (P Q : IProp GF) [Persistent P] : P ∗ Q ⊢ □ P := GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ P ∗ Q ⊢ □ P GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ∗_HQ : Q ⊢ □ P GF:BundledGFunctorsP:IProp GFQ:IProp GFinst✝:Persistent P⊢ □HP : P ⊢ P All goals completed! 🐙

The imodintro tactic introduces a modality in the goal. In this case, since the modality is a □, it throws away the spatial context.

Since the only difference between □ P and P is that the former does not claim the resources are exclusive, it follows that the persistently modality is idempotent.

theorem pers_idemp (P : IProp GF) : □ □ P ⊣⊢ □ P := GF:BundledGFunctorsP:IProp GF⊢ □ □ P ⊣⊢ □ P GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ □ P -∗ □ PGF:BundledGFunctorsP:IProp GF⊢ ⊢ □ P -∗ □ □ P GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ □ P -∗ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ P -- Iris already knows that `□` is idempotent, so it -- automatically removes all persistently modalities from a -- proposition when adding it to the intuitionistic context. -- One may think of all propositions in the intuitionistic -- context as having an implicit `□` in front. All goals completed! 🐙 GF:BundledGFunctorsP:IProp GF⊢ ⊢ □ P -∗ □ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ □ P GF:BundledGFunctorsP:IProp GF⊢ □HP : P ⊢ □ P All goals completed! 🐙

Only propositions that are instances of the Persistent typeclass can be added to the intuitionistic context. As with the typeclasses for pure propositions, Persistent can automatically identify most persistent propositions.

theorem pers_sep (P Q : IProp GF) : □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) := GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □ P ∗ □ Q ⊣⊢ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ P ∗ □ Q -∗ □ (P ∗ Q)GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ (P ∗ Q) -∗ □ P ∗ □ Q GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ P ∗ □ Q -∗ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ □ (P ∗ Q) GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ P ∗ Q All goals completed! 🐙 GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ ⊢ □ (P ∗ Q) -∗ □ P ∗ □ Q GF:BundledGFunctorsP:IProp GFQ:IProp GF⊢ □HP : P □HQ : Q ⊢ □ P ∗ □ Q All goals completed! 🐙

Note the intuitionistic-pattern variant #⟨HP, HQ⟩ that destructs a persistent separation directly in the cases pattern.

Persistency is preserved by quantifications.

theorem pers_all {α : Type} (P : α → IProp GF) [∀ x, Persistent (P x)] : (∀ x, □ P x) ⊢ ∀ y, P y ∗ P y := GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)⊢ (∀ x, □ P x) ⊢ ∀ y, P y ∗ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y ∗ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P yGF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y All goals completed! 🐙 GF:BundledGFunctorsα:TypeP:α → IProp GFinst✝:∀ (x : α), Persistent (P x)y:α⊢ □Hp : ∀ x, □ P x ⊢ P y All goals completed! 🐙

For simple predicates such as the one below, Lean's typeclass resolution can automatically infer the Persistent instance.

def myPredicate (x : Val) : IProp GF := iprop(⌜x = hl_val(#5)⌝) instance myPredicate_persistent (x : Val) : Persistent (myPredicate (GF := GF) x) := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Val⊢ Persistent (myPredicate x) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Val⊢ Persistent iprop(⌜x = hl_val(#5)⌝) All goals completed! 🐙

For more complicated predicates, such as ones defined as a fixpoint, the Persistent instance cannot be inferred automatically. The following predicate asserts that all values in a given list are equal to hl_val(#5).

def myPredFix : List Val → IProp GF | [] => iprop(True) | x :: xs' => iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix xs')

Adding such a predicate to the intuitionistic context requires us to register a Persistent instance manually, by induction on the list.

instance myPredFix_persistent (xs : List Val) : Persistent (myPredFix (GF := GF) xs) := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFxs:List Val⊢ Persistent (myPredFix xs) induction xs with hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GF⊢ Persistent (myPredFix []) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GF⊢ Persistent iprop(True); All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Valxs':List Valih:Persistent (myPredFix xs')⊢ Persistent (myPredFix (x :: xs')) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFx:Valxs':List Valih:Persistent (myPredFix xs')⊢ Persistent iprop(⌜x = hl_val(#5)⌝ ∗ myPredFix xs'); All goals completed! 🐙

With the instance in place, iris-lean now recognises myPredFix as persistent.

theorem first_is_5 (x : Val) (xs : List Val) : myPredFix (GF := GF) (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) := GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ myPredFix (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) -- After `iintro #H`, the hypothesis `H : myPredFix (x :: xs)` -- sits in the intuitionistic context. Since `myPredFix` unfolds -- by pattern-matching, we can `change` the hypothesis-to-be so -- the destructure exposes the head element. GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ myPredFix (x :: xs) -∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix (x :: xs) GF:BundledGFunctorsx:Valxs:List Val⊢ ⊢ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs -∗ ⌜x = hl_val(#5)⌝ ∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs GF:BundledGFunctorsx:Valxs:List Val⊢ □Hx : ⌜x = hl_val(#5)⌝ □Hxs : myPredFix xs ⊢ ⌜x = hl_val(#5)⌝ ∗ ⌜x = hl_val(#5)⌝ ∗ myPredFix xs All goals completed! 🐙

6.3. Examples of Persistent Propositions🔗

Thus far, the only basic persistent propositions we have seen are pure propositions, such as equalities. Two further examples are Hoare triples and persistent points-to predicates.

6.3.1. Hoare Triples🔗

All Hoare triples are persistent. This is because Hoare triples in Iris are defined as

□ (∀ Φ, P -∗ ▷ (∀ x .. y, Q -∗ Φ v) -∗ WP e {{ w, Φ w }})

— with an outermost □, so Hoare triples can be duplicated and reused. Intuitively, a Hoare triple {{ P }} e {{ v, RET v; Φ v }} does not claim ownership of any resources; it merely states that if we own the resources described by P, then we can safely run e, and we get the resources described by Φ if it terminates. If we can get ownership of those resources multiple times, we should be able to run e multiple times.

Here the client calls an unknown increment function twice. Its specification is persistent, so both calls can use the same Hinc hypothesis while passing ownership of the counter from one call to the next.

def counter (inc : Val) : Exp := hl% let c := ref(#0); &inc c; &inc c; !c theorem counter_spec (inc : Val) : {{ ∀ (l : Loc) (z : Int), {{ l ↦ some hl_val(#z) }} hl(&inc #l) {{ v, RET v; l ↦ some hl_val(#(z + 1 : Int)) }} }} (counter inc) {{ v, RET v; ⌜v = hl_val(#2)⌝ }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:Val⊢ ⊢ ∀ Φ, (∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ) -∗ (▷ ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v) -∗ WP (counter inc) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GF⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ▷ ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ⊢ WP (counter inc) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GF⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ▷ ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ⊢ WP hl(let c := ref(#0); v(&inc) c; v(&inc) c; !c) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Loc⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#0) ⊢ WP hl(let c := #l; v(&inc) c; v(&inc) c; !c) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Loc⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#0) ⊢ WP hl(v(&inc) #l; v(&inc) #l; !#l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1)) ⊢ WP hl(v(&v); v(&inc) #l; !#l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1)) ⊢ WP hl(v(&inc) #l; !#l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Valv':Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1 + 1)) ⊢ WP hl(v(&v'); !#l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Valv':Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1 + 1)) ⊢ WP hl(!#l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Valv':Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1 + 1)) ⊢ |={⊤}=> Φ hl_val(#(0 + 1 + 1)) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Valv':Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗HΦ : ∀ v, ⌜v = hl_val(#2)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#(0 + 1 + 1)) ⊢ Φ hl_val(#(0 + 1 + 1)) hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFinc:ValΦ:Val → IProp GFl:Locv:Valv':Val⊢ □Hinc : ∀ l z, □ ∀ Φ, l ↦ some hl_val(#z) -∗ (▷ ∀ v, l ↦ some hl_val(#(z + 1)) -∗ Φ v) -∗ WP hl(v(&inc) #l) {{ Φ }} ∗Hl : l ↦ some hl_val(#(0 + 1 + 1)) ⊢ ⌜hl_val(#(0 + 1 + 1)) = hl_val(#2)⌝ All goals completed! 🐙

6.3.2. Persistent Points-to🔗

The resource of heaps is more sophisticated than what we have been letting on. The general shape of a points-to predicate is actually l ↦{dq} v, where dq is a discarded fraction (iris-lean's DFrac: either .own q for a real fraction q ∈ (0,1], or .discard for the persistent variant). The predicate l ↦ v is shorthand for l ↦{DFrac.own 1} v. The basic idea is that points-to predicates can be split up and recombined, allowing ownership of points-to predicates to be shared. iris-lean provides this through the Fractional / AsFractional typeclasses.

The proof mode can split a full points-to into two halves and combine them again. icombine adds their fractions:

theorem pt_split (l : Loc) (v : Val) : l ↦ some v ⊣⊢@{IProp GF} l ↦{.own (1 : Qp).half} some v ∗ l ↦{.own (1 : Qp).half} some v := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ l ↦ some v ⊣⊢ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ⊢ l ↦ some v -∗ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some vhlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ⊢ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v -∗ l ↦ some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ⊢ l ↦ some v -∗ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ⊢ l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v -∗ l ↦ some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ l ↦ some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ∗Hl : l ↦ some v ⊢ l ↦ some v All goals completed! 🐙

Crucially, a store operation can only take place if the entire fraction is owned, i.e. dq = .own 1. However, load operations can occur for any fraction. Fractional points-to predicates are especially useful in scenarios where a location is read by multiple threads in parallel but later only used by a single thread.

This allows two threads to read a location before the parent thread recovers full ownership and writes to it.

section ParReadWrite variable [Spawn.SpawnG GF] open Iris.HeapLang.Par def par_read_write (l : Loc) : Exp := hl% let r := (!#l ‖ !#l); #l ← #5 theorem par_read_write_spec (l : Loc) (v : Val) : {{ l ↦ some v }} (par_read_write l) {{ RET hl_val(#()); l ↦ some hl_val(#5) }} := hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:Val⊢ ⊢ ∀ Φ, l ↦ some v -∗ ▷ (l ↦ some hl_val(#5) -∗ Φ hl_val(#())) -∗ WP (par_read_write l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl : l ↦ some v ∗HΦ : ▷ (l ↦ some hl_val(#5) -∗ Φ hl_val(#())) ⊢ WP (par_read_write l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗HΦ : ▷ (l ↦ some hl_val(#5) -∗ Φ hl_val(#())) ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP (par_read_write l) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗HΦ : ▷ (l ↦ some hl_val(#5) -∗ Φ hl_val(#())) ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(let r := v(&par) (λ _, !#l) (λ _, !#l); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(let r := v(&par) (v(λ _, !#l)) (v(λ _, !#l)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(!#l) {{ x, l ↦{DFrac.own (Qp.half 1)} some v }}hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(!#l) {{ x, l ↦{DFrac.own (Qp.half 1)} some v }}hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ⊢ ∀ v1 v2, l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v -∗ ▷ WP hl(let r := v((&v1, &v2)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(!#l) {{ x, l ↦{DFrac.own (Qp.half 1)} some v }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ |={⊤}=> l ↦{DFrac.own (Qp.half 1)} some v; hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ l ↦{DFrac.own (Qp.half 1)} some v; All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(!#l) {{ x, l ↦{DFrac.own (Qp.half 1)} some v }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ |={⊤}=> l ↦{DFrac.own (Qp.half 1)} some v; hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ l ↦{DFrac.own (Qp.half 1)} some v; All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GF⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ⊢ ∀ v1 v2, l ↦{DFrac.own (Qp.half 1)} some v ∗ l ↦{DFrac.own (Qp.half 1)} some v -∗ ▷ WP hl(let r := v((&v1, &v2)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ ▷ WP hl(let r := v((&r1, &r2)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl1 : l ↦{DFrac.own (Qp.half 1)} some v ∗Hl2 : l ↦{DFrac.own (Qp.half 1)} some v ⊢ WP hl(let r := v((&r1, &r2)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl : l ↦ some v ⊢ WP hl(let r := v((&r1, &r2)); #l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl : l ↦ some v ⊢ WP hl(#l ← #5) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl : l ↦ some hl_val(#5) ⊢ |={⊤}=> Φ hl_val(#()) hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFl:Locv:ValΦ:Val → IProp GFr1:Valr2:Val⊢ ∗HΦ : l ↦ some hl_val(#5) -∗ Φ hl_val(#()) ∗Hl : l ↦ some hl_val(#5) ⊢ Φ hl_val(#()) All goals completed! 🐙 end ParReadWrite

If one owns a fraction of a points-to predicate, one can decide to discard the fraction. This means that it is no longer possible to recombine points-to predicates to get the full fraction. As such, the value in the points-to predicate can never be changed again — the location has become read-only. The persistent points-to is written l ↦{.discard} v. It is persistent.

The lemma that makes a points-to persistent is Iris.pointsTo_persist:

⊢@{IProp GF} l ↦{dq} v ==∗ l ↦{.discard} v

There are some caveats as to when we can discard fractions; the proposition P ==∗ Q is equivalent to P -∗ |==> Q, where |==> is the update modality. The imod tactic can usually remove this modality, e.g. when the goal is a weakest precondition.

theorem pt_persist (l : Loc) (v : Val) : l ↦ some v -∗ WP hl(!v(#l)) {{ w, ⌜w = v⌝ ∗ l ↦{.discard} some v }} := hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ⊢ l ↦ some v -∗ WP hl(!#l) {{ w, ⌜w = v⌝ ∗ l ↦{DFrac.discard} some v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ ∗Hl : l ↦ some v ⊢ WP hl(!#l) {{ w, ⌜w = v⌝ ∗ l ↦{DFrac.discard} some v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ □Hl' : l ↦{DFrac.discard} some v ⊢ WP hl(!#l) {{ w, ⌜w = v⌝ ∗ l ↦{DFrac.discard} some v }} hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ □Hl' : l ↦{DFrac.discard} some v ⊢ |={⊤}=> ⌜v = v⌝ ∗ l ↦{DFrac.discard} some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ □Hl' : l ↦{DFrac.discard} some v ⊢ ⌜v = v⌝ ∗ l ↦{DFrac.discard} some v hlc:HasLCGF:BundledGFunctorsinst✝:HeapLangGS hlc GFl:Locv:Val⊢ □Hl' : l ↦{DFrac.discard} some v ⊢ ⌜v = v⌝ All goals completed! 🐙

The discarded points-to is persistent, so #Hl' moves it into the intuitionistic context. The chapter's final example allocates a location, makes it persistent, and shares it between two arithmetic computations.

section ParRead variable [Spawn.SpawnG GF] open Iris.HeapLang.Par def par_read : Exp := hl% let l := ref(#7); let r := (!l + #14 ‖ !l * #3); fst(r) + snd(r) theorem par_read_spec : {{ (True : IProp GF) }} par_read {{ v, RET v; ⌜v = hl_val(#42)⌝ }} := hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GF⊢ ⊢ ∀ Φ, True -∗ (▷ ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v) -∗ WP par_read {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GF⊢ ∗HΦ : ▷ ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v ⊢ WP par_read {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GF⊢ ∗HΦ : ▷ ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v ⊢ WP hl(let l := ref(#7); let r := v(&par) (λ _, (!l + #14)) (λ _, (!l * #3)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v ∗Hl : l ↦ some hl_val(#7) ⊢ WP hl(let l := #l; let r := v(&par) (λ _, (!l + #14)) (λ _, (!l * #3)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl(let l := #l; let r := v(&par) (λ _, (!l + #14)) (λ _, (!l * #3)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl(let r := v(&par) (v(λ _, (!#l + #14))) (v(λ _, (!#l * #3))); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((!#l + #14)) {{ w, ⌜w = hl_val(#21)⌝ }}hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((!#l * #3)) {{ w, ⌜w = hl_val(#21)⌝ }}hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ∀ v1 v2, ⌜v1 = hl_val(#21)⌝ ∗ ⌜v2 = hl_val(#21)⌝ -∗ ▷ WP hl(let r := v((&v1, &v2)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((!#l + #14)) {{ w, ⌜w = hl_val(#21)⌝ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((#7 + #14)) {{ w, ⌜w = hl_val(#21)⌝ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ |={⊤}=> ⌜hl_val(#(7 + 14)) = hl_val(#21)⌝ All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((!#l * #3)) {{ w, ⌜w = hl_val(#21)⌝ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl((#7 * #3)) {{ w, ⌜w = hl_val(#21)⌝ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ |={⊤}=> ⌜hl_val(#(7 * 3)) = hl_val(#21)⌝ All goals completed! 🐙 hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ∀ v1 v2, ⌜v1 = hl_val(#21)⌝ ∗ ⌜v2 = hl_val(#21)⌝ -∗ ▷ WP hl(let r := v((&v1, &v2)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Locw1:Valw2:ValH1:w1 = hl_val(#21)H2:w2 = hl_val(#21)⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ▷ WP hl(let r := v((&w1, &w2)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Locw2:ValH2:w2 = hl_val(#21)⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ▷ WP hl(let r := v((#21, &w2)); (fst(r) + snd(r))) {{ Φ }}; hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ▷ WP hl(let r := v((#21, #21)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ WP hl(let r := v((#21, #21)); (fst(r) + snd(r))) {{ Φ }} hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ |={⊤}=> Φ hl_val(#(21 + 21)) hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ ∗HΦ : ∀ v, ⌜v = hl_val(#42)⌝ -∗ Φ v □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ Φ hl_val(#(21 + 21)) hlc:HasLCGF:BundledGFunctorsinst✝¹:HeapLangGS hlc GFinst✝:Spawn.SpawnG GFΦ:Val → IProp GFl:Loc⊢ □Hl : l ↦{DFrac.discard} some hl_val(#7) ⊢ ⌜hl_val(#(21 + 21)) = hl_val(#42)⌝ All goals completed! 🐙 end ParRead

Both threads access the same intuitionistic hypothesis Hl. Their postconditions establish 7 + 14 = 21 and 7 * 3 = 21; after the join, the final pure steps establish 21 + 21 = 42.

end Persistently