Examples.v 8.54 KB
 Glen Mével committed Jul 04, 2018 1 2 ``````(* code taken from the Iris tutorial… *) `````` Jacques-Henri Jourdan committed Nov 07, 2018 3 ``````From iris_time.heap_lang Require Import proofmode notation. `````` Glen Mével committed Jul 04, 2018 4 ``````From iris.program_logic Require Import adequacy. `````` Jacques-Henri Jourdan committed Oct 23, 2018 5 ``````From iris_time Require Import TimeCredits Reduction. `````` Glen Mével committed Jul 04, 2018 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 committed Jul 11, 2018 122 `````` TC_invariant -∗ `````` Jacques-Henri Jourdan committed Nov 07, 2018 123 `````` {{{ is_list_tr l v ∗ TC (4 + 13 * length l) }}} « sum_list v » {{{ RET #(sum_list_coq l) ; is_list_tr l v }}}. `````` Glen Mével committed Jul 04, 2018 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. `````` Glen Mével committed Jul 04, 2018 130 `````` by iApply "Post". `````` Jacques-Henri Jourdan committed Nov 07, 2018 131 `````` - replace (4 + 13 * length (x :: l))%nat with (17 + 13 * length l)%nat by (simpl ; lia). `````` Glen Mével committed Jul 04, 2018 132 `````` iDestruct "Hl" as (p) "[-> Hl]" ; iDestruct "Hl" as (v) "[Hp Hl]". `````` Jacques-Henri Jourdan committed Nov 07, 2018 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. `````` Glen Mével committed Jul 04, 2018 136 137 `````` iDestruct "Htc" as "[Htc1 Htc]". wp_apply ("IH" with "Hl Htc"). iIntros "Hl". `````` 138 `````` wp_tick_op. `````` Jacques-Henri Jourdan committed Nov 07, 2018 139 `````` iApply "Post". simpl. eauto with iFrame. `````` Glen Mével committed Jul 04, 2018 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. `````` Jacques-Henri Jourdan committed Nov 07, 2018 161 `````` - wp_rec. wp_op. wp_if. wp_inj. `````` Glen Mével committed Jul 04, 2018 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'). `````` Jacques-Henri Jourdan committed Nov 07, 2018 168 `````` wp_alloc p. wp_inj. `````` Glen Mével committed Jul 04, 2018 169 170 171 `````` iApply "Post". eauto with iFrame. Qed. Lemma make_list_translation_spec `{!timeCreditHeapG Σ} (n : nat) : `````` Glen Mével committed Jul 11, 2018 172 `````` TC_invariant -∗ `````` Jacques-Henri Jourdan committed Nov 07, 2018 173 `````` {{{ TC (4+7*n) }}} «make_list #n» {{{ v', RET v' ; is_list (make_list_coq n) v' }}}. `````` Glen Mével committed Jul 04, 2018 174 175 176 ``````Proof. iIntros "#Htickinv !#" (Φ) "Htc Post". iInduction n as [|n'] "IH" forall (Φ). `````` Jacques-Henri Jourdan committed Nov 07, 2018 177 `````` - wp_tick_rec. wp_tick_op. wp_tick_if. wp_tick_inj. `````` Glen Mével committed Jul 04, 2018 178 `````` by iApply "Post". `````` Jacques-Henri Jourdan committed Nov 07, 2018 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. `````` Glen Mével committed Jul 04, 2018 182 `````` assert (Z.of_nat n' = Z.of_nat (S n') - 1) as Eq by lia ; simpl in Eq ; destruct Eq. `````` Jacques-Henri Jourdan committed Nov 07, 2018 183 `````` iDestruct "Htc" as "[? [? [? Htc]]]". `````` Glen Mével committed Jul 04, 2018 184 185 `````` wp_apply ("IH" with "Htc"). iIntros (v') "Hl". change (Z.pos \$ Pos.of_succ_nat n') with (Z.of_nat \$ S n'). `````` Jacques-Henri Jourdan committed Nov 07, 2018 186 187 `````` wp_tick_pair. wp_tick_alloc p. wp_tick_inj. iApply "Post". simpl. eauto with iFrame. `````` Glen Mével committed Jul 04, 2018 188 189 ``````Qed. `````` Jacques-Henri Jourdan committed Oct 23, 2018 190 ``````Definition prgm (n : nat) : expr := `````` Glen Mével committed Jul 04, 2018 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 committed Jul 11, 2018 230 `````` TC_invariant -∗ `````` Jacques-Henri Jourdan committed Nov 07, 2018 231 `````` {{{ TC (8+20*n) }}} «prgm n» {{{ v, RET v ; ⌜v = #(n*(n+1)/2)⌝ }}}. `````` Glen Mével committed Jul 04, 2018 232 233 ``````Proof. iIntros "#Htickinv !#" (Φ) "Htc Post". `````` Jacques-Henri Jourdan committed Nov 07, 2018 234 `````` replace (8+20*n)%nat with ((4+7*n) + (4+13*n))%nat by lia ; `````` Glen Mével committed Jul 04, 2018 235 `````` rewrite TC_plus ; iDestruct "Htc" as "[Htc_make Htc_sum]". `````` Jacques-Henri Jourdan committed Nov 07, 2018 236 `````` unfold prgm. simpl_trans. `````` Glen Mével committed Jul 04, 2018 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 Σ} : `````` Jacques-Henri Jourdan committed Oct 25, 2018 247 `````` adequate NotStuck (prgm n) σ (λ v _, v = #(n*(n+1)/2)) `````` Jacques-Henri Jourdan committed Nov 07, 2018 248 `````` ∧ bounded_time (prgm n) σ (8 + 20 * n)%nat. `````` Glen Mével committed Jul 04, 2018 249 250 251 252 253 ``````Proof. apply (spec_tctranslation__adequate_and_bounded' (Σ:=Σ)). - by intros _ ->. - intros HtcHeapG. apply prgm_translation_spec. - assumption. `````` Jacques-Henri Jourdan committed Oct 25, 2018 254 ``Qed.``