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.

The Rocq syntax is {{{ P }}} e {{{ x .. y, RET v ; Q }}}. It desugars to

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

iris-lean does not yet ship the {{{ P }}} e {{{ ... }}} sugar, so in this port we write the desugared wand-rolled form directly. One loss: we don't get the persistence □ automatically; we either add it by hand or skip it when the spec only needs to be applied once.

Consider a function that swaps two values.

-- TODO (upstream — iris-lean): port the Hoare-triple notation
-- `{{{ P }}} e {{{ x .. , RET v ; Q }}}`. Until then a Hoare-
-- triple-styled specification must be written out as the
-- desugared wand-rolled WP. (The proof itself uses `wp_pures` +
-- `wp_load`/`wp_store`, all of which work today — only the
-- statement-level sugar is missing.)

-- Rocq tutorial reference:
--   Lemma swap_spec (l1 l2 : loc) (v1 v2 : val) :
--     {{{ l1 ↦ v1 ∗ l2 ↦ v2 }}}
--       swap #l1 #l2
--     {{{ RET #(); l1 ↦ v2 ∗ l2 ↦ v1 }}}.
--   Proof.
--     iIntros "%Φ [H1 H2] HΦ".
--     rewrite /swap.
--     wp_pures. wp_load. wp_load. wp_store. wp_store.
--     iApply "HΦ". by iFrame.
--   Qed.

A convention in Iris is to write specifications using Hoare triples but prove them by converting them to weakest preconditions. This convention applies equally to the iris-lean port; once the notation lands, the chapter's swap_spec and swap_swap_spec will translate without issue, because every primitive law they use is already in Iris.HeapLang.PrimitiveLaws.