Examples.v 8.93 KB
Newer Older
MEVEL Glen's avatar
MEVEL Glen committed
1 2 3 4
(* code taken from the Iris tutorial… *)

From iris.heap_lang Require Import proofmode notation.
From iris.program_logic Require Import adequacy.
5
From iris_time Require Import TimeCredits Reduction.
MEVEL Glen's avatar
MEVEL Glen committed
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 49 50 51 52 53 54 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 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121

(** A function that sums all elements of a list, defined as a heap-lang value: *)
Definition sum_list : val :=
  rec: "sum_list" "l" :=
    match: "l" with
      NONE => #0
    | SOME "p" =>
      let: "x" := Fst !"p" in
      let: "l" := Snd !"p" in
      "x" + "sum_list" "l"
    end.

(** Representation predicate in separation logic for a list of integers [l]: *)
Fixpoint is_list `{heapG Σ} (l : list Z) (v : val) : iProp Σ :=
  match l with
  | [] =>  v = NONEV 
  | x :: l' =>  (p : loc),  v = SOMEV #p  
                  (v' : val), p  (#x, v')  is_list l' v'
  end%I.
(* [is_list_tr l v] means that the translation of [v] represents [l]: *)
Fixpoint is_list_tr `{timeCreditHeapG Σ} (l : list Z) (v : val) : iProp Σ :=
  match l with
  | [] =>  v = NONEV 
  | x :: l' =>  (p : loc),  v = SOMEV #p  
                  (v' : val), p  (#x, «v'»)  is_list_tr l' v'
  end%I.
(* some proofs: *)
Lemma is_list_translation `{!timeCreditHeapG Σ} l v :
  (is_list l v - is_list l v  v = «v»%V)%I.
Proof.
  iIntros "Hl".
  destruct l as [|x l] ; simpl.
  - by iDestruct "Hl" as %->.
  - iDestruct "Hl" as (p) "[-> ?]".
    iSplitL.
    + iExists p. by iFrame.
    + done.
Qed.
Lemma is_list_tr_translation `{!timeCreditHeapG Σ} l v :
  (is_list_tr l v - is_list_tr l v  v = «v»%V)%I.
Proof.
  iIntros "Hl".
  destruct l as [|x l] ; simpl.
  - by iDestruct "Hl" as %->.
  - iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v') "[Hp Hl']".
    iSplitL.
    + iExists p. iSplit ; first done. eauto with iFrame.
    + done.
Qed.
Lemma is_list_tr_is_list_translation `{!timeCreditHeapG Σ} l v :
  (is_list_tr l v  is_list l «v»%V)%I.
Proof.
  iSplit ; iIntros "Hl".
{
  iInduction l as [|x l] "IH" forall (v) ; simpl.
  - iDestruct "Hl" as %->.
    done.
  - iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
    iPoseProof ("IH" with "Hl") as "Hl". eauto with iFrame.
}
{
  iInduction l as [|x l] "IH" forall (v) ; simpl.
  - iDestruct "Hl" as %Eq. iPureIntro. by eapply translationV_injective.
  - iDestruct "Hl" as (p) "[Eq Hl]" ; iDestruct "Eq" as %Eq ; iDestruct "Hl" as (v') "[Hp Hl]".
    change (InjRV #p)%V with «InjRV #p»%V in Eq. apply translationV_injective in Eq as ->.
    iDestruct (is_list_translation with "Hl") as "[Hl ->]".
    iPoseProof ("IH" with "Hl") as "Hl". eauto with iFrame.
}
Qed.
Lemma is_list_is_list_tr `{!timeCreditHeapG Σ} l v :
  (is_list l v  is_list_tr l v)%I.
Proof.
  iSplit ; iIntros "Hl".
{
  iInduction l as [|x l] "IH" forall (v) ; simpl.
  - done.
  - iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
    iExists p. iSplitR ; first done. iExists v.
    iDestruct (is_list_translation with "Hl") as "[Hl <-]".
    iFrame.
    iApply ("IH" with "Hl").
}
{
  iInduction l as [|x l] "IH" forall (v) ; simpl.
  - done.
  - iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
    iExists p. iSplitR ; first done. iExists v.
    iDestruct (is_list_tr_translation with "Hl") as "[Hl <-]".
    iFrame.
    iApply ("IH" with "Hl").
}
Qed.

Definition sum_list_coq (l : list Z) : Z :=
  fold_right Z.add 0 l.

(** The proof using induction over [l]: *)
Lemma sum_list_spec `{!heapG Σ} (l : list Z) (v : val) :
  {{{ is_list l v }}} sum_list v {{{ RET #(sum_list_coq l) ; is_list l v }}}.
Proof.
  iIntros (Φ) "Hl Post".
  iInduction l as [|x l] "IH" forall (v Φ) ; simpl.
  - iDestruct "Hl" as %->.
    wp_rec.
    wp_match.
    by iApply "Post".
  - iDestruct "Hl" as (p) "[-> Hl]". iDestruct "Hl" as (v) "[Hp Hl]".
    wp_rec.
    wp_match.
    wp_load. wp_proj. wp_let.
    wp_load. wp_proj. wp_let.
    wp_apply ("IH" with "Hl"). iIntros "Hl".
    wp_op.
    iApply "Post". eauto with iFrame.
Qed.
Lemma sum_list_translation_spec `{!timeCreditHeapG Σ} (l : list Z) (v : val) :
MEVEL Glen's avatar
MEVEL Glen committed
122
  TC_invariant -
MEVEL Glen's avatar
MEVEL Glen committed
123 124 125 126 127 128 129
  {{{ is_list_tr l v  TC (3 + 10 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}.
Proof.
  iIntros "#Htickinv !#" (Φ) "[Hl Htc] Post".
  iInduction l as [|x l] "IH" forall (v Φ).
  - simpl.
    rewrite !translation_of_val.
    iDestruct "Hl" as %->.
130
    wp_tick_rec. wp_tick_match.
MEVEL Glen's avatar
MEVEL Glen committed
131 132 133 134 135
    by iApply "Post".
  - replace (3 + 10 * length (x :: l))%nat with (13 + 10 * length l)%nat by (simpl ; lia).
    simpl.
    rewrite !translation_of_val. setoid_rewrite translation_of_val.
    iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
136
    wp_tick_rec.
137
    wp_tick_match.
138 139
    wp_tick_load. wp_tick_proj. wp_tick_let.
    wp_tick_load. wp_tick_proj. wp_tick_let.
MEVEL Glen's avatar
MEVEL Glen committed
140 141
    iDestruct "Htc" as "[Htc1 Htc]".
    wp_apply ("IH" with "Hl Htc"). iIntros "Hl".
142
    wp_tick_op.
MEVEL Glen's avatar
MEVEL Glen committed
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
    iApply "Post". eauto with iFrame.
Qed.

Definition make_list : val :=
  rec: "make_list" "n" :=
    if: "n" = #0 then
      NONE
    else
      SOME (ref ("n", "make_list" ("n" - #1))).

Fixpoint make_list_coq (n : nat) : list Z :=
  match n with
  | 0%nat => []
  | S n'  => Z.of_nat n :: make_list_coq n'
  end.

(** The proof using induction over [l]: *)
Lemma make_list_spec `{!heapG Σ} (n : nat) :
  {{{ True }}} make_list #n {{{ v, RET v ; is_list (make_list_coq n) v }}}.
Proof.
  iIntros (Φ) "_ Post".
  iInduction n as [|n'] "IH" forall (Φ) ; simpl.
  - wp_rec. wp_op. wp_if.
    by iApply "Post".
  - wp_rec. wp_op. wp_if.
    wp_op.
    assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
    wp_apply "IH". iIntros (v') "Hl".
    change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
    wp_alloc p.
    iApply "Post". eauto with iFrame.
Qed.
Lemma make_list_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
MEVEL Glen's avatar
MEVEL Glen committed
176
  TC_invariant -
MEVEL Glen's avatar
MEVEL Glen committed
177 178 179 180 181 182
  {{{ TC (3+5*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}.
Proof.
  iIntros "#Htickinv !#" (Φ) "Htc Post".
  iInduction n as [|n'] "IH" forall (Φ).
  - simpl.
    rewrite !translation_of_val.
183
    wp_tick_rec. wp_tick_op. wp_tick_if.
MEVEL Glen's avatar
MEVEL Glen committed
184 185 186 187
    by iApply "Post".
  - replace (3 + 5 * S n')%nat with (8 + 5 * n')%nat by lia.
    simpl.
    rewrite !translation_of_val.
188 189
    wp_tick_rec. wp_tick_op. wp_tick_if.
    wp_tick_op.
MEVEL Glen's avatar
MEVEL Glen committed
190 191 192 193
    assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
    iDestruct "Htc" as "[Htc1 Htc]".
    wp_apply ("IH" with "Htc"). iIntros (v') "Hl".
    change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
194
    wp_tick_alloc p.
MEVEL Glen's avatar
MEVEL Glen committed
195 196 197
    iApply "Post". eauto with iFrame.
Qed.

198
Definition prgm (n : nat) : expr :=
MEVEL Glen's avatar
MEVEL Glen committed
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
  sum_list (make_list #n).

Lemma length_make_list_coq (n : nat) :
  length (make_list_coq n) = n.
Proof.
  induction n as [|n' IH].
  - done.
  - simpl. by f_equal.
Qed.

Lemma sum_list_coq_make_list_coq (n : nat) :
  sum_list_coq (make_list_coq n) = (Z.of_nat n * (Z.of_nat n + 1)) `div` 2.
Proof.
  rewrite - Z.div2_div.
  assert (2 * sum_list_coq (make_list_coq n) = (Z.of_nat n * (Z.of_nat n + 1))) as Eq.
  {
  induction n as [|n' IH].
  - done.
  - rewrite /= Z.mul_add_distr_l IH. lia.
  }
  assert (Zeven (Z.of_nat n * (Z.of_nat n + 1))) as Heven % Zeven_div2.
  {
    pose proof (Zeven_odd_dec n) as [ Heven | Hodd ].
    - by apply Zeven_mult_Zeven_l.
    - by apply Zeven_mult_Zeven_r, Zodd_plus_Zodd.
  }
  lia.
Qed.

Lemma prgm_spec `{!heapG Σ} (n : nat) :
  {{{ True }}} prgm n {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
Proof.
  iIntros (Φ) "_ Post".
  unfold prgm.
  wp_apply (make_list_spec with "[//]"). iIntros (v) "Hl".
  wp_apply (sum_list_spec with "Hl"). iIntros "Hl".
  iApply ("Post" with "[%]"). repeat f_equal. apply sum_list_coq_make_list_coq.
Qed.
Lemma prgm_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
MEVEL Glen's avatar
MEVEL Glen committed
238
  TC_invariant -
MEVEL Glen's avatar
MEVEL Glen committed
239 240 241 242
  {{{ TC (6+15*n) }}} «prgm n» {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
Proof.
  iIntros "#Htickinv !#" (Φ) "Htc Post".
  unfold prgm.
243
  change « sum_list (make_list (LitV n)) » with ((tick «sum_list») «make_list #n»).
MEVEL Glen's avatar
MEVEL Glen committed
244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
  rewrite !translation_of_val.
  replace (6+15*n)%nat with ((3+5*n) + (3+10*n))%nat by lia ;
  rewrite TC_plus ; iDestruct "Htc" as "[Htc_make Htc_sum]".
  wp_apply (make_list_translation_spec with "Htickinv Htc_make"). iIntros (v) "Hl".
  iDestruct (is_list_translation with "Hl") as "[Hl ->]".
  rewrite - !translation_of_val.
  change (« sum_list » (tick « v »)) with « sum_list v ».
  wp_apply (sum_list_translation_spec with "Htickinv [Hl Htc_sum]"). {
    rewrite - is_list_tr_is_list_translation.
    erewrite length_make_list_coq. iFrame.
  } iIntros "Hl".
  iApply ("Post" with "[%]"). repeat f_equal. apply sum_list_coq_make_list_coq.
Qed.

Lemma prgm_timed_spec (n : nat) (σ : state) `{!timeCreditHeapPreG Σ} :
259
    adequate NotStuck (prgm n) σ (λ v _, v = #(n*(n+1)/2))
MEVEL Glen's avatar
MEVEL Glen committed
260 261 262 263 264 265 266
   bounded_time (prgm n) σ (6 + 15 * n)%nat.
Proof.
  apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
  - by intros _ ->.
  - rewrite !andb_True ; repeat split ; apply is_closed_of_val.
  - intros HtcHeapG. apply prgm_translation_spec.
  - assumption.
267
Qed.