5.3. Resources🔗

In this section, we introduce our first notion of a resource: the resource of heaps. As mentioned in the basics chapter, propositions in Iris describe / assert ownership of resources. To describe resources in the resource of heaps, we use the points-to predicate, written l ↦ some v. (The Rocq tutorial writes l ↦ v; the Lean port carries an Option because the model also tracks deallocated locations.) Intuitively, l ↦ some v describes all heap fragments that have value v stored at location l. The proposition l1 ↦ some hl_val(#1) ∗ l2 ↦ some hl_val(#2) then describes all heap fragments that map l1 to 1 and l2 to 2.

The Rocq tutorial's running example for this section is

let: "x" := ref #1 in
"x" <- !"x" + #2 ;;
!"x"

which both touches the heap and performs an addition. We can state and partly proved it in iris-lean, but the addition step is blocked by the same PureExec gap as above; see the per-step breakdown below.

-- TODO (upstream — iris-lean): the addition `!x + #2` blocks the
-- proof. The `wp_alloc`/`wp_load`/`wp_store` rules apply fine; the
-- missing piece is reducing `(#1 : Int) + (#2 : Int)` via
-- `wp_pure`. Until `PureExec` for `+` lands, `prog_spec` cannot be
-- proved cleanly.

-- Rocq tutorial reference:
--   Lemma prog_spec : ⊢ WP prog {{ v, ⌜v = #3⌝ }}.
--   Proof.
--     rewrite /prog.
--     wp_alloc l as "Hl".
--     wp_let. wp_load. wp_op. wp_store. wp_load.
--     iModIntro. done.
--   Qed.

To at least demonstrate the heap primitives in isolation, here is a trivial program that allocates and then immediately reads.

Each iapply wp_alloc / iapply wp_load consumes the relevant primitive law and the surrounding wp_pures advances past the let β-reductions.

HeapLang also provides the cmpXchg(_, _, _) instruction. The primitive-law lemmas wp_cmpXchg_fail and wp_cmpXchg_true cover the two outcomes, with the choice between them dispatched by side conditions on whether the stored value equals the test value.

-- TODO (upstream — iris-lean): port a `wp_cmpxchg` lemma (and a
-- matching tactic) that branches on the equality decision —
-- equivalent to the Rocq tutorial's `wp_cmpxchg as H1 | H2`. The
-- current iris-lean only ships the two outcome-specific lemmas
-- `wp_cmpXchg_fail` and `wp_cmpXchg_true`.

-- Rocq tutorial reference:
--   Example cmpXchg_0_to_10 (l : loc) : expr := (CmpXchg #l #0 #10).
--   Lemma cmpXchg_0_to_10_spec (l : loc) (v : val) :
--     l ↦ v -∗
--     WP (cmpXchg_0_to_10 l) {{ u, (⌜v = #0⌝ ∗ l ↦ #10) ∨
--                                  (⌜v ≠ #0⌝ ∗ l ↦ v) }}.
--   Proof.
--     iIntros "Hl". wp_cmpxchg as H1 | H2.
--     - iLeft.  by iFrame.
--     - iRight. by iFrame.
--   Qed.

The points-to predicate is not duplicable. That is, for every location l, there can only exist one full-fraction points-to associated with it. iris-lean exposes this via the HeapView-level disjointness lemmas; we omit the detailed proof.