ex_01_swap.v 5.34 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
(*
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
Robbert Krebbers's avatar
Robbert Krebbers committed
49
     easier to use in other proofs, because the post-condition does not have to
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53 54 55 56 57
     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.
58
  wp_lam. wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72
  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".
73
  wp_lam. wp_let. wp_load. wp_let. wp_load. wp_store. wp_store.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76 77 78
  iApply "Post". iFrame.
Qed.

(* We can further automate the lemma by defining a simple Ltac tactic for
symbolic executing. *)
79
Ltac wp_exec := repeat (wp_lam || wp_pure _ || wp_load || wp_store).
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102

(* 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".
103
  unfold rotate_r. wp_lam. do 2 wp_let.
Robbert Krebbers's avatar
Robbert Krebbers committed
104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
  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.
120
  iIntros (Φ) "(Hx & Hy & Hz) Post". wp_lam.
Robbert Krebbers's avatar
Robbert Krebbers committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
  (* 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.
  (* exercise *)
Admitted.
End proof.