recursion_through_the_store.v 6.96 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(* This file contains the case study on recursion-through-the-store which
   is described in the Iris Lecture Notes in the case study section on Invariants
   for Sequential Programs.
 *)

(* Contains definitions of the weakest precondition assertion, and its basic rules. *)
From iris.program_logic Require Export weakestpre.

(* Instantiation of Iris with the particular language. The notation file
   contains many shorthand notations for the programming language constructs, and
   the lang file contains the actual language syntax. *)
From iris.heap_lang Require Export notation lang.

Dan Frumin's avatar
Dan Frumin committed
14 15 16
(* Files related to the interactive proof mode. The first import includes the
   general tactics of the proof mode. The second provides some more specialized
   tactics particular to the instantiation of Iris to a particular programming
17 18 19 20 21 22 23 24 25
   language. *)
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Import proofmode.

(* Definition of invariants and their rules (expressed using the fancy update
   modality). *)
From iris.base_logic.lib Require Export invariants.


Dan Frumin's avatar
Dan Frumin committed
26
(* The following line makes Coq check that we do not use any admitted facts /
27 28 29 30 31 32 33 34 35 36
   additional assumptions not in the statement of the theorems being proved. *)
Set Default Proof Using "Type".


Section recursion_through_the_store.

(* In order to do the proof we need to assume certain things about the
   instantiation of Iris. The particular, even the heap is handled in an
   analogous way as other ghost state. This line states that we assume the
   Iris instantiation has sufficient structure to manipulate the heap, e.g.,
Dan Frumin's avatar
Dan Frumin committed
37
   it allows us to use the points-to predicate. *)
38 39 40 41 42 43 44

Context `{!heapG Σ}.
Implicit Types l : loc.


(* This is the code for the recursion through the store operator *)
Definition myrec : val :=
Dan Frumin's avatar
Dan Frumin committed
45
  λ: "f",
46 47
  let: "r" := ref(λ: "x", "x" ) in
  "r" <- (λ: "x", "f" (!"r") "x");;
Dan Frumin's avatar
Dan Frumin committed
48
          !"r".
49

Dan Frumin's avatar
Dan Frumin committed
50 51
(* Here is the specification for the recursion through the store function.
   See the Iris Lecture Notes for an in-depth discussion of both the specification and
52 53
   the proof. *)
Lemma myrec_spec (P: val -> iProp Σ) (Q: val -> val -> iProp Σ) (F v1: val) (e_F e_v : expr)
Dan Frumin's avatar
Dan Frumin committed
54
   `{HeF : !IntoVal e_F F} `{Hev1 : !IntoVal e_v v1}:
55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
  {{{
       ( e_f:expr,f : val,  v2:val, IntoVal e_f f - {{{( v3 :val, {{{P v3 }}} e_f v3 {{{u, RET u; Q u v3 }}})
                                 P v2 }}}
            F e_f v2
            {{{u, RET u; Q u v2}}})
             P v1
  }}}
myrec e_F e_v
  {{{u, RET u; Q u v1}}}.
Proof.
  apply of_to_val in HeF as <-.
  apply of_to_val in Hev1 as <-.
   iIntros (ϕ) "[#H P] Q".
   wp_lam.
   wp_alloc r as "r".
   wp_let.
   wp_store.
   wp_load.
   iMod (inv_alloc (nroot.@"myrec") _ _ with "[r]") as "#inv"; first by iNext; iExact "r".
   iAssert (  u : val, Q u v1 - ϕ u)%I with "[Q]" as "Q"; first done.
   iLöb as "IH" forall(v1 ϕ).
   wp_let.
   wp_bind (! _)%E.
   iInv (nroot.@"myrec") as "r" "cl".
   wp_load.
   iMod ("cl" with "[r]") as "_"; first done. iModIntro.
   iApply ("H" with "[][P]"); first (iIntros "!%"; apply _); last done.
   iFrame. iIntros (v3).
   iAlways. iIntros (Φ) "P Q". iApply ("IH" with "[P][Q]"); done.
Qed.

End recursion_through_the_store.

Section factorial_client.
  Context `{!heapG Σ}.
  Implicit Types l : loc.

Dan Frumin's avatar
Dan Frumin committed
92 93
  (* In this section we show how to specify and prove correctness of a
     factorial fucntion implemented using our recursion through the
94 95
     store function *)

Dan Frumin's avatar
Dan Frumin committed
96
  (* Here is the mathematical factorial function and a few properties
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119
     related to that. *)
  Fixpoint factorial (n: nat) : nat:=
  match n with
    | O => 1
    | S n' => S n' * factorial n'
  end.

  Lemma factorial_spec_S (n : nat) : factorial (S n) = ((S n) * factorial n)%nat.
  Proof.
    reflexivity.
  Qed.

  Definition fac_int (x : Z) := Z.of_nat (factorial (Z.to_nat x)).

  Lemma fac_int_eq_0: fac_int 0 = 1.
  Proof.
    reflexivity.
  Qed.

  Lemma fac_int_eq (x : Z):
    1  x  fac_int x = fac_int (x - 1) * x.
  Proof.
    intros ?.
Dan Frumin's avatar
Dan Frumin committed
120
    rewrite Z.mul_comm.
121 122 123 124 125 126 127
    rewrite /fac_int.
    assert (Z.to_nat x = S (Z.to_nat (x - 1))) as Heq.
    { transitivity (Z.to_nat (1 + (x - 1))).
      - f_equal; lia.
      - rewrite Z2Nat.inj_add; first auto; lia.
    }
    rewrite Heq factorial_spec_S -Heq Nat2Z.inj_mul Z2Nat.id //; lia.
Dan Frumin's avatar
Dan Frumin committed
128
  Qed.
129 130

  (* Now, for the code of the implementation of factorial *)
Dan Frumin's avatar
Dan Frumin committed
131 132

  (* Here is code for a multiplication function, which we will use
133 134 135 136 137 138 139 140 141 142
     to implement factorial. *)
  Definition times : val :=
    rec: "times" "x" "y" :=
      if: "x" = #0 then #0 else "y" + "times" ("x" - #1) "y".

  Lemma times_spec_aux (m : Z):
    ( n Φ ,  Φ (# (n * m)) - WP times #n #m {{ Φ }})%I.
  Proof.
    iLöb as "IH".
    iIntros (n Φ) "ret".
Dan Frumin's avatar
Dan Frumin committed
143 144 145 146 147
    wp_lam. wp_lam.
    wp_binop.
    case_bool_decide; simplify_eq/=.
    - wp_if. iApply "ret".
    - wp_if.
148 149 150 151
      wp_bind (_ - _)%E.
      wp_binop.
      wp_bind ((times _) _).
      iApply "IH"; iNext.
Dan Frumin's avatar
Dan Frumin committed
152
      wp_binop; first
153
        by replace (m + ((n - 1) * m)) with (n * m) by lia.
Dan Frumin's avatar
Dan Frumin committed
154
  Qed.
155 156 157 158 159 160 161 162 163 164 165 166 167

  Lemma times_spec (n m : Z):
    {{{True}}}
      times #n #m
      {{{v, RET v; v = # ( n * m)  }}}.
  Proof.
    iIntros (Φ) "_ ret".
    iApply (times_spec_aux with "[ret]").
    iNext; iApply "ret".
      by iIntros "!%".
  Qed.


Dan Frumin's avatar
Dan Frumin committed
168
  (* Here is the implementation code for factorial, implemented using the recursion
169 170 171 172 173 174 175 176 177
   through the store function *)
  Definition myfac  :=
    myrec (λ: "f" ,
           λ: "n",
           if: "n"=#0
           then #1
           else  times ("f" ("n" - #1) )  "n")%E.


Dan Frumin's avatar
Dan Frumin committed
178
  (* Finally, here is the specification that our implementation of factorial
179 180
     really does implement the mathematical factorial function. *)
  Lemma myfac_spec (n: expr) (n': Z):
Dan Frumin's avatar
Dan Frumin committed
181
    IntoVal n #n'  (0  n') 
182 183 184 185 186 187 188
    {{{ True}}}
      myfac n
      {{{v, RET v; v = #(fac_int n')}}}.
  Proof.
    iIntros (H%of_to_val Hleq Φ) "_ ret"; simplify_eq.
    iApply (myrec_spec (fun v => m' : Z, 0  m'  to_val v = Some #m'%I)
                       (fun u => fun v => m' : Z, to_val v = Some #m'  u = #(fac_int m')%I)).
Dan Frumin's avatar
Dan Frumin committed
189
    - iSplit; last eauto. iIntros (e_f f v) "%". iAlways. iIntros (Φ') "spec_f ret".
190 191 192
      apply of_to_val in a as <-.
      wp_lam. wp_lam. iDestruct "spec_f" as "[spec_f %]".
      destruct H as [m' [Hleqm' Heq%of_to_val]]; simplify_eq.
Dan Frumin's avatar
Dan Frumin committed
193 194 195 196 197
      wp_binop.
      case_bool_decide; simplify_eq/=; wp_if.
      + iApply "ret". iPureIntro. exists 0; done.
      + assert (m'  0) by naive_solver.
        wp_binop. wp_bind (f _ )%E.
198 199 200
        iApply ("spec_f" $! (#(m'-1))).
        * iIntros "!%".
          exists (m'-1); split; first lia; last auto.
Dan Frumin's avatar
Dan Frumin committed
201
        * iNext. iIntros (u) "**". destruct a as [x [Heq ->]].
202 203 204 205 206 207 208
          iApply times_spec; first done.
          iNext; iIntros (u) "%"; subst; iApply "ret".
          iIntros "!%".
          exists m'.
          simpl in Heq; simplify_eq.
          split; first auto.
          rewrite -fac_int_eq; first auto; lia.
Dan Frumin's avatar
Dan Frumin committed
209
    - iNext. iIntros "**". destruct a as (?&[=]&->); simplify_eq. by iApply "ret".
210 211
  Qed.

Dan Frumin's avatar
Dan Frumin committed
212
End factorial_client.