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 {{{ Φ }}} 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.

-- TODO (upstream — iris-lean): the example below relies on the
-- Hoare-triple notation `{{{ P }}} e {{{ ... }}}` (missing) and
-- on a `wp_apply` convenience tactic (also missing).

-- Rocq tutorial reference:
--   Example counter (inc : val) : expr :=
--     let: "c" := ref #0 in
--     inc "c" ;; inc "c" ;; !"c".
--
--   Lemma counter_spec (inc : val) :
--     {{{ ∀ (l : loc) (z : Z),
--           {{{ l ↦ #z }}} inc #l {{{ v, RET v; l ↦ #(z + 1) }}} }}}
--       counter inc
--     {{{ v, RET v; ⌜v = #2⌝ }}}.
--   Proof.
--     iIntros (Φ) "#Hinc_spec HΦ".
--     rewrite /counter.
--     wp_alloc l as "Hl". wp_let.
--     wp_apply ("Hinc_spec" with "Hl"). iIntros (v) "Hl". wp_seq.
--     wp_apply ("Hinc_spec" with "Hl"). iIntros (v') "Hl". wp_seq.
--     wp_load. by iApply "HΦ".
--   Qed.

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.

-- TODO (upstream — iris-lean): the proof below uses `pt_split`
-- with the fractional notation `l ↦{# 1/2} v` (Rocq syntax). In
-- iris-lean the spelling is `l ↦{.own (1/2)} v` and the
-- `iCombine`/`iDestruct` automation for fractional splits is
-- still maturing. The point is that
-- `pointsto_fractional` / `pointsto_combine` already exist as
-- lemmas (see `Iris.BI.Lib.GenHeap`); a Rocq-style ergonomic
-- port awaits the iris-lean `iCombine` and fractional-pattern
-- tactics.

-- Rocq tutorial reference:
--   Lemma pt_split l v : l ↦ v ⊣⊢ (l ↦{# 1/2 } v) ∗ (l ↦{# 1/2 } v).
--   Proof.
--     iSplit.
--     - iIntros "Hl".
--       iDestruct "Hl" as "[Hl1 Hl2]".
--       iFrame.
--     - iIntros "[Hl1 Hl2]".
--       iCombine "Hl1" "Hl2" as "Hl".
--       iFrame.
--   Qed.

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.

-- TODO (upstream — iris-lean): `par_read_write` requires
-- ergonomic fractional-points-to manipulation (splitting `l ↦ v`
-- into `l ↦{.own (1/2)} v ∗ l ↦{.own (1/2)} v` and recombining
-- after the parallel composition). The underlying lemmas
-- (`pointsto_fractional`, `pointsto_combine`) are present in
-- `Iris.BI.Lib.GenHeap`, but `iCombine`-style automation is not
-- yet there. `wp_par` itself works fine (see Specifications
-- chapter); the missing piece is the fractional bookkeeping.

-- Rocq tutorial reference:
--   Example par_read_write (l : loc) : expr :=
--     let: "r" := (!#l ||| !#l) in
--     #l <- #5.
--   Lemma par_read_write_spec (l : loc) (v : val) :
--     {{{ l ↦ v }}}
--       par_read_write l
--     {{{ RET #(); l ↦ #5 }}}.
--   Proof. ... uses (wp_par t_post t_post) ... Qed.

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. iris-lean writes the persistent points-to as l ↦{.discard} v (the Rocq tutorial writes l ↦□ v). It is persistent.

The lemma that makes a points-to persistent is Iris.pointsTo_persist (Rocq alias 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.

Note: iris-lean does not yet register Persistent (l ↦{.discard} v) as an instance, so a discarded points-to cannot be moved into the intuitionistic context with #. The lemmas treat ↦{.discard} as a (duplicable, but spatially-managed) hypothesis. Once the Persistent instance lands, the proof above will be eligible for the cleaner imod ... with #Hl' pattern.

As a more elaborate example, here is a parallel program where two threads both read from the same location. The key idea is that once the points-to is made persistent (↦{.discard}), it can be shared across both threads. (The Rocq tutorial additionally wraps the result in arithmetic computing 21 * 2 = 42; we drop that because iris-lean still lacks PureExec for + / *.)

Ideally we would write the precondition as a single l ↦{.discard} some v and let iris-lean duplicate it across both threads automatically. That requires registering a Persistent (l ↦{.discard} v) instance — see TODO below.

-- TODO (upstream — iris-lean): register a
-- `Persistent (l ↦{DFrac.discard} v)` instance in
-- `Iris.BI.Lib.GenHeap`. Once registered, the `parRead_spec`
-- proof above can be tightened so the caller passes a single
-- discarded points-to and iris-lean splits it automatically.

-- Rocq tutorial reference (full version with arithmetic):
--   Example par_read : expr :=
--     let: "l" := ref #7 in
--     let: "r" := ( (!"l" + #14) ||| (!"l" * #3) ) in
--     Fst "r" + Snd "r".
--   Lemma par_read_spec :
--     {{{ True }}} par_read {{{ v, RET v; ⌜v = #42⌝ }}}.

-- TODO (upstream — iris-lean): once `PureExec` for arithmetic
-- lands, restore the Rocq tutorial's full `par_read` example with
-- its `21 * 2 = 42` postcondition.

-- Rocq tutorial reference:
--   Example par_read : expr :=
--     let: "l" := ref #7 in
--     let: "r" := ( (!"l" + #14) ||| (!"l" * #3) ) in
--     Fst "r" + Snd "r".
--   Lemma par_read_spec :
--     {{{ True }}} par_read {{{ v, RET v; ⌜v = #42⌝ }}}.