5.1. Introduction🔗

Now that we have seen basic separation logic in Iris and introduced a suitable language, HeapLang, we are finally ready to start reasoning about programs. HeapLang ships with a program logic defined using Iris. We can access the logic through the proof-mode package, which also defines tactics to alleviate working with the logic.

The program logic for HeapLang relies on a basic notion of a resource: the resource of heaps. Recall that GF specifies the available resources. To make the resource of heaps available, we require an instance of HeapLangGS hlc GF throughout this section. We declare it as a variable so that every definition and theorem below has the resource of heaps available.

5.2. Weakest Precondition🔗

The first construct for specifying program behaviour is the weakest precondition. In Iris, a weakest precondition has the form WP e {{ v, Φ v }}. This asserts that if the HeapLang program e terminates at some value v, then v satisfies the predicate Φ. The double curly brackets are the postcondition.

A natural first example is a pure arithmetic expression. The wp_pure and wp_pures tactics symbolically execute pure steps, including integer arithmetic.

The same tactic also handles β-reduction and conditionals:

The tactic wp_pures symbolically executes all pure steps for which a PureExec instance exists. Each step internally applies the wp_pure_step_fupd rule from Iris.ProgramLogic.Lifting, which says (informally):

e₁ →pure e₂
──────────────────────────────────
WP e₂ {{ Φ }} ⊢ WP e₁ {{ Φ }}

After every pure step has fired, the goal is reduced to proving the postcondition behind a fancy-update modality |={⊤}=>; itrivial discharges the residual proposition ⌜#1 = #1⌝.

The lambda program from the previous chapter combines lambda application with arithmetic:

Here is a higher-order example using only β-reduction:

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 value carries an Option because the heap model also tracks deallocated locations: some v means the location currently holds v. 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.

A running example for this section is

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

which both touches the heap and performs an addition.

The allocation tactic names the fresh location and its points-to hypothesis. The load and store tactics find that hypothesis in the proof-mode context and update it as the program executes.

For comparison, here is a program that allocates and immediately reads.

The surrounding wp_pures advances past the let β-reductions.

HeapLang also provides cmpXchg(_, _, _). The wp_cmpxchg tactic creates success and failure branches and names their equality and inequality assumptions.

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.

5.4. Composing Programs and Proofs🔗

The tactic wp_apply finds the evaluation context in which a specification applies, focuses on that sub-expression, and applies the specification. A postcondition-generic WP lemma is one way to expose a program's result to its caller:

5.5. Hoare Triples🔗

Having studied weakest preconditions, we shift our focus onto another construct for specifying program behaviour: Hoare triples. The weakest precondition does not explicitly specify which conditions must hold before executing the program; it only talks about the postcondition. Hoare triples build on weakest preconditions by requiring us to explicitly mention the precondition.

A Hoare triple is written {{ P }} e {{ x .. y, RET v; Q }}. It desugars to

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

Inside an Iris proposition, the notation includes the outer □, so triples are persistent. As a Lean theorem statement it elaborates to the universally quantified WP rule, introduced with iintro %Φ.

Consider a function that swaps two values.