(*
This exercise introduces the basic Iris Proof Mode tactics by proving a simple
example: a function that swaps the contents of two pointers. We will use this
function to implement two other functions.
*)
From iris.heap_lang Require Import proofmode notation.
(* The swap function, defined as a heap-lang value. This looks like an ordinary
Coq function, but it is not: heap-lang is a deeply embedded language in Coq. It
uses strings for name binding and notations close to Coq's (but typically
augmented with a colon to avoid ambiguity) to make it easy to read and write
programs. *)
Definition swap : val := λ: "x" "y",
let: "tmp" := !"x" in
"x" <- !"y";;
"y" <- "tmp".
(* Using swap, we can define functions that rotate three pointers in left and
right direction. *)
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Definition rotate_l : val := λ: "x" "y" "z",
swap "x" "y";; swap "y" "z".
Section proof.
(* Iris is parameterized by the type of ghost state that is needed to carry out
a proof. As such, the type of Iris propositions [iProp] is indexed by a [Σ]: a
list of cameras (actually, functors from OFEs to cameras). To make our proofs
generic, we abstract over any such [Σ] and use type classes to ensure that the
necessary cameras are present in [Σ].
For this proof, we do not need any special ghost state (i.e. cameras) apart from
the ghost state that's the heap-lang uses internally for modeling the [l ↦ v]
connective. The cameras for this ghost state is provided by the class [heapG].
*)
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
(* The "Texan triple" [ {{{ P }}} e {{{ RET v, Q }}} ] is syntactic sugar for:
∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e {{ v, Φ v }}
Which is logically equivalent to [ P -∗ WP e {{ x, x = v ∗ Q }} ]
In practice, the "Texan triple" is not more difficult to prove, but usually
easier to use in other proofs, because the post-condition does not have to
syntactically match [Q]. Using this way of stating specifications, the
consequence and framing rule is implicitly applied on the post-condition.
Note that [ # v ] is the embedding of values ([bool], [Z], [loc]) into
heap-lang values.*)
Proof.
iIntros (Φ) "[Hx Hy] Post".
unfold swap.
wp_lam. wp_let.
wp_load. wp_let.
wp_load. wp_store.
wp_store.
iApply "Post".
iSplitL "Hx".
- iApply "Hx".
- iApply "Hy".
Qed.
(* Same lemma, but using a bit of automation to shorten the proof. *)
Lemma swap_spec_2 x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof.
iIntros (Φ) "[??] Post".
wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
iApply "Post". iFrame.
Qed.
(* We can further automate the lemma by defining a simple Ltac tactic for
symbolic executing. *)
Ltac wp_exec := repeat (wp_lam || wp_pure _ || wp_load || wp_store).
(* This tactic repeatedly tries to symbolically execute pure redexes, loads and
stores. It makes use of the tactic [wp_pure t], which tries to find the redex
[t] in the goal, and executes that redex. The redex [t] may contain holes, and
as such, tactics like [wp_seq] are actually defined as [wp_pure (_ ;; _)%E]. By
using [wp_pure _] it will symbolically execute *any* pure redex. *)
(* Same lemma again, but now using the tactic we just defined. *)
Lemma swap_spec_2_more_automation x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof.
iIntros (Φ) "[??] Post". wp_exec.
iApply "Post". iFrame.
Qed.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
(* As in Coq, the IPM introduction pattern (p1 & p2 & .. & pn) ] is syntactic
sugar for [ [p1 [p2 [... pn]]] ]. *)
iIntros (Φ) "(Hx & Hy & Hz) Post".
unfold rotate_r. wp_lam. do 2 wp_let.
wp_bind (swap _ _).
iApply (swap_spec with "[Hy Hz]").
{ iFrame. }
(* Inspired by ssreflect, the IPM introduction pattern [ /= ] performs
[simpl]. *)
iNext. iIntros "[Hy Hz] /=". wp_seq.
(* We can also immediately frame hypothesis when using a lemma: *)
iApply (swap_spec with "[$Hx $Hy]"); iNext; iIntros "[Hx Hy]".
iApply "Post". iFrame.
Qed.
Lemma rotate_r_spec_again x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". wp_lam. do 2 wp_let.
(* We can shorten the above a bit: Instead of using the [iApply] tactic, we
can use [wp_apply] which automatically uses [wp_bind] first. Also, it strips
the later [▷] by calling [iNext] afterwards. *)
wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz] /="; wp_seq.
wp_apply (swap_spec with "[$Hx $Hy]"); iIntros "[Hx Hy] /=".
iApply "Post". iFrame.
Qed.
(* *Exercise*: Do this proof yourself. Try a couple of variations of the tactics
we have seen before:
- Do the whole proof explicitly by proving [swap] inline,
- Use the specification of [swap] in combination with [iApply],
- Use the specification of [swap] in combination with [wp_apply]
*)
Lemma rotate_l_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_l #x #y #z
{{{ RET #(); x ↦ v2 ∗ y ↦ v3 ∗ z ↦ v1 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". unfold rotate_l. wp_lam. do 2 wp_let.
wp_apply (swap_spec with "[$Hx $Hy]"); iIntros "[Hx Hy]"; wp_seq.
wp_apply (swap_spec with "[$Hy $Hz]"); iIntros "[Hy Hz]".
iApply ("Post" with "[$]").
Qed.
End proof.