unsafe.v 5.29 KB
 Robbert Krebbers committed Jan 16, 2020 1 ``````From tutorial_popl20 Require Export sem_typed. `````` Robbert Krebbers committed Jan 16, 2020 2 ``````From tutorial_popl20 Require Import symbol_ghost two_state_ghost. `````` Robbert Krebbers committed Jan 15, 2020 3 `````` `````` Robbert Krebbers committed Jan 16, 2020 4 5 ``````Section unsafe. Context `{heapG Σ}. `````` Robbert Krebbers committed Jan 15, 2020 6 `````` `````` Robbert Krebbers committed Jan 16, 2020 7 8 9 `````` (** * Exercise (easy) *) Definition unsafe_pure : val := λ: <>, if: #true then #13 else #13 #37. `````` Robbert Krebbers committed Jan 15, 2020 10 `````` `````` Robbert Krebbers committed Jan 18, 2020 11 `````` Lemma sem_typed_unsafe_pure : ∅ ⊨ unsafe_pure : (() → sem_ty_int). `````` Robbert Krebbers committed Jan 16, 2020 12 13 14 15 16 17 18 19 20 21 22 23 24 25 `````` Proof. iIntros (vs) "!# HΓ"; simpl. iApply wp_value. iIntros "!#" (? ->). wp_lam. wp_if. rewrite /sem_ty_car /=. by iExists 13. Qed. (** * Exercise (easy) *) Definition unsafe_ref : val := λ: <>, let: "l" := ref #0 in "l" <- #true;; !"l". `````` Robbert Krebbers committed Jan 18, 2020 26 `````` Lemma sem_typed_unsafe_ref : ∅ ⊨ unsafe_ref : (() → sem_ty_bool). `````` Robbert Krebbers committed Jan 16, 2020 27 28 29 30 31 32 33 34 35 36 37 38 `````` Proof. iIntros (vs) "!# HΓ"; simpl. iApply wp_value. iIntros "!#" (? ->). wp_lam. wp_alloc l as "Hl". wp_let. wp_store. wp_load. rewrite /sem_ty_car /=. by iExists true. Qed. `````` Robbert Krebbers committed Jan 15, 2020 39 `````` `````` Robbert Krebbers committed Jan 16, 2020 40 41 42 43 44 `````` (** * Exercise (moderate) *) Definition unsafe_ref_ne_0 : val := λ: <>, let: "l" := ref #1 in ((λ: "x", if: "x" ≠ #0 then "l" <- "x" else #()), (λ: <>, assert: !"l" ≠ #0)). `````` Robbert Krebbers committed Jan 15, 2020 45 `````` `````` Robbert Krebbers committed Jan 16, 2020 46 `````` Lemma sem_typed_unsafe_ref_ne_0 : `````` Robbert Krebbers committed Jan 18, 2020 47 `````` ∅ ⊨ unsafe_ref_ne_0 : (() → (sem_ty_int → ()) * (() → ())). `````` Robbert Krebbers committed Jan 16, 2020 48 49 50 51 52 53 54 55 `````` Proof. iIntros (vs) "!# HΓ"; simpl. iApply wp_value. iIntros "!#" (? ->). wp_lam. wp_alloc l as "Hl". wp_let. pose (I := (∃ n : Z, ⌜#n ≠ #0⌝ ∗ l ↦ #n)%I). `````` Robbert Krebbers committed Jan 16, 2020 56 `````` iMod (inv_alloc (nroot .@ "inv") _ I with "[Hl]")%I as "#Hinv". `````` Robbert Krebbers committed Jan 16, 2020 57 58 59 60 61 62 63 64 65 66 67 68 69 70 `````` { by iNext; iExists 1; iFrame. } wp_pures. iExists _, _. iSplit; first done. iSplit. - iIntros "!#" (? [n ->]). wp_lam. wp_op. destruct (decide (n = 0%Z)); simplify_eq/=. + wp_op. wp_if. done. + rewrite bool_decide_eq_false_2; last congruence. wp_op. wp_if. `````` Robbert Krebbers committed Jan 16, 2020 71 `````` iInv (nroot .@ "inv") as (m) ">[% Hl]". `````` Robbert Krebbers committed Jan 16, 2020 72 73 74 75 76 77 78 79 80 81 `````` wp_store. iModIntro. iSplit. * iExists n; auto with congruence. * done. - iIntros "!#" (? ->). wp_lam. wp_pures. iApply wp_assert. (* Need because of atomic expression *) wp_bind (! _)%E. `````` Robbert Krebbers committed Jan 16, 2020 82 `````` iInv (nroot .@ "inv") as (m) ">[% Hl]". `````` Robbert Krebbers committed Jan 16, 2020 83 84 85 86 87 88 89 `````` wp_load. iModIntro. iSplitL "Hl". { iExists m; auto. } wp_op. rewrite bool_decide_eq_false_2; last done. by wp_op. Qed. `````` Robbert Krebbers committed Jan 15, 2020 90 `````` `````` Robbert Krebbers committed Jan 16, 2020 91 92 93 `````` (** * Exercise (hard) *) Definition unsafe_ref_reuse : val := λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l". `````` Robbert Krebbers committed Jan 15, 2020 94 `````` `````` Robbert Krebbers committed Jan 16, 2020 95 `````` Lemma sem_typed_unsafe_ref_reuse `{two_stateG Σ}: `````` Robbert Krebbers committed Jan 18, 2020 96 `````` ∅ ⊨ unsafe_ref_reuse : (() → (() → sem_ty_bool)). `````` Robbert Krebbers committed Jan 15, 2020 97 `````` Proof. `````` Robbert Krebbers committed Jan 16, 2020 98 99 100 101 102 103 104 `````` iIntros (vs) "!# HΓ"; simpl. iApply wp_value. iIntros "!#" (? ->). wp_lam. wp_alloc l as "Hl". iMod two_state_init as (γ) "Ho". pose (I := (∃ b, two_state_auth γ b ∗ l ↦ (if b then #true else #0))%I). `````` Robbert Krebbers committed Jan 16, 2020 105 `````` iMod (inv_alloc (nroot .@ "inv") _ I with "[Hl Ho]") as "#Hinv". `````` Robbert Krebbers committed Jan 16, 2020 106 107 108 109 110 111 `````` { iNext. iExists false. iFrame. } wp_pures. iIntros "!#" (? ->). wp_lam. (* Need because of atomic expression *) wp_bind (_ <- _)%E. `````` Robbert Krebbers committed Jan 16, 2020 112 `````` iInv (nroot .@ "inv") as (o) ">[Ho Hl]". `````` Robbert Krebbers committed Jan 16, 2020 113 114 115 116 117 `````` wp_store. iMod (two_state_update with "Ho") as "[Ho Hf]". iModIntro. iSplitL "Hl Ho". { iNext. iExists true. iFrame. } wp_pures. `````` Robbert Krebbers committed Jan 16, 2020 118 `````` iInv (nroot .@ "inv") as (o') ">[Ho Hl]". `````` Robbert Krebbers committed Jan 16, 2020 119 120 121 122 123 `````` iDestruct (two_state_agree with "Ho Hf") as %->. wp_load. iModIntro. iSplitL "Hl Ho". { iNext. iExists true. iFrame. } rewrite /sem_ty_car /=. by iExists _. `````` Robbert Krebbers committed Jan 15, 2020 124 `````` Qed. `````` Robbert Krebbers committed Jan 16, 2020 125 126 127 128 129 130 `````` (** * Exercise (hard) *) (** Semantic typing of a symbol ADT (taken from Dreyer's POPL'18 talk) *) Definition symbol_adt_inc : val := λ: "x" <>, FAA "x" #1. Definition symbol_adt_check : val := λ: "x" "y", assert: "y" < !"x". Definition symbol_adt : val := λ: <>, `````` Robbert Krebbers committed Jan 18, 2020 131 `````` let: "x" := Alloc #0 in pack: (symbol_adt_inc "x", symbol_adt_check "x"). `````` Robbert Krebbers committed Jan 16, 2020 132 133 134 135 136 `````` Definition symbol_adt_ty `{heapG Σ} : sem_ty Σ := (() → ∃ A, (() → A) * (A → ())). Section sem_typed_symbol_adt. `````` Amin Timany committed Jan 18, 2020 137 `````` Context `{symbolG Σ}. `````` Robbert Krebbers committed Jan 16, 2020 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 `````` Definition symbol_adtN := nroot .@ "symbol_adt". Definition symbol_inv (γ : gname) (l : loc) : iProp Σ := (∃ n : nat, l ↦ #n ∗ counter γ n)%I. Definition sem_ty_symbol (γ : gname) : sem_ty Σ := SemTy (λ w, ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I. Lemma sem_typed_symbol_adt Γ : Γ ⊨ symbol_adt : symbol_adt_ty. Proof. iIntros (vs) "!# _ /=". iApply wp_value. iIntros "!#" (v ->). wp_lam. wp_alloc l as "Hl"; wp_pures. iMod (counter_alloc 0) as (γ) "Hc". iMod (inv_alloc symbol_adtN _ (symbol_inv γ l) with "[Hl Hc]") as "#?". { iExists 0%nat. by iFrame. } `````` Robbert Krebbers committed Jan 18, 2020 154 `````` do 2 (wp_lam; wp_pures). wp_lam. `````` Robbert Krebbers committed Jan 16, 2020 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 `````` iExists (sem_ty_symbol γ), _, _; repeat iSplit=> //. - repeat rewrite /sem_ty_car /=. iIntros "!#" (? ->). wp_pures. iInv symbol_adtN as (n) ">[Hl Hc]". wp_faa. iMod (counter_inc with "Hc") as "[Hc #Hs]". iModIntro; iSplitL; last eauto. iExists (S n). rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. - repeat rewrite /sem_ty_car /=. iIntros "!#" (v). iDestruct 1 as (n ->) "#Hs". wp_pures. iApply wp_assert. wp_bind (!_)%E. iInv symbol_adtN as (n') ">[Hl Hc]". wp_load. iDestruct (symbol_obs with "Hc Hs") as %?. iModIntro. iSplitL. { iExists n'. iFrame. } wp_op. rewrite bool_decide_true; last lia. eauto. Qed. End sem_typed_symbol_adt. End unsafe.``````