Examples.v 8.54 KB
Newer Older
1 2
(* code taken from the Iris tutorial *)

3
From iris_time.heap_lang Require Import proofmode notation.
4
From iris.program_logic Require Import adequacy.
5
From iris_time Require Import TimeCredits Reduction.
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) :
Glen Mével's avatar
Glen Mével committed
122
  TC_invariant -
123
  {{{ is_list_tr l v  TC (4 + 13 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}.
124 125 126 127 128
Proof.
  iIntros "#Htickinv !#" (Φ) "[Hl Htc] Post".
  iInduction l as [|x l] "IH" forall (v Φ).
  - simpl.
    iDestruct "Hl" as %->.
129
    wp_tick_rec. wp_tick_match.
130
    by iApply "Post".
131
  - replace (4 + 13 * length (x :: l))%nat with (17 + 13 * length l)%nat by (simpl ; lia).
132
    iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]".
133
    wp_tick_rec. wp_tick_match.
134 135
    wp_tick_load. wp_tick_proj. wp_tick_let.
    wp_tick_load. wp_tick_proj. wp_tick_let.
136 137
    iDestruct "Htc" as "[Htc1 Htc]".
    wp_apply ("IH" with "Hl Htc"). iIntros "Hl".
138
    wp_tick_op.
139
    iApply "Post". simpl. eauto with iFrame.
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
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.
161
  - wp_rec. wp_op. wp_if. wp_inj.
162 163 164 165 166 167
    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').
168
    wp_alloc p. wp_inj.
169 170 171
    iApply "Post". eauto with iFrame.
Qed.
Lemma make_list_translation_spec `{!timeCreditHeapG Σ} (n : nat) :
Glen Mével's avatar
Glen Mével committed
172
  TC_invariant -
173
  {{{ TC (4+7*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}.
174 175 176
Proof.
  iIntros "#Htickinv !#" (Φ) "Htc Post".
  iInduction n as [|n'] "IH" forall (Φ).
177
  - wp_tick_rec. wp_tick_op. wp_tick_if. wp_tick_inj.
178
    by iApply "Post".
179
  - replace (4 + 7 * S n')%nat with (11 + 7 * n')%nat by lia.
180 181
    wp_tick_rec. wp_tick_op. wp_tick_if.
    wp_tick_op.
182
    assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq.
183
    iDestruct "Htc" as "[? [? [? Htc]]]".
184 185
    wp_apply ("IH" with "Htc"). iIntros (v') "Hl".
    change (Z.pos $ Pos.of_succ_nat n') with (Z.of_nat $ S n').
186 187
    wp_tick_pair. wp_tick_alloc p. wp_tick_inj.
    iApply "Post". simpl. eauto with iFrame.
188 189
Qed.

190
Definition prgm (n : nat) : expr :=
191 192 193 194 195 196 197 198 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
  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) :
Glen Mével's avatar
Glen Mével committed
230
  TC_invariant -
231
  {{{ TC (8+20*n) }}} «prgm n» {{{ v, RET v ; v = #(n*(n+1)/2) }}}.
232 233
Proof.
  iIntros "#Htickinv !#" (Φ) "Htc Post".
234
  replace (8+20*n)%nat with ((4+7*n) + (4+13*n))%nat by lia ;
235
  rewrite TC_plus ; iDestruct "Htc" as "[Htc_make Htc_sum]".
236
  unfold prgm. simpl_trans.
237 238 239 240 241 242 243 244 245 246
  wp_apply (make_list_translation_spec with "Htickinv Htc_make"). iIntros (v) "Hl".
  iDestruct (is_list_translation with "Hl") as "[Hl ->]".
  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 Σ} :
247
    adequate NotStuck (prgm n) σ (λ v _, v = #(n*(n+1)/2))
248
   bounded_time (prgm n) σ (8 + 20 * n)%nat.
249 250 251 252 253
Proof.
  apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)).
  - by intros _ ->.
  - intros HtcHeapG. apply prgm_translation_spec.
  - assumption.
254
Qed.