unsafe.v 5.29 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From tutorial_popl20 Require Export sem_typed.
2
From tutorial_popl20 Require Import symbol_ghost two_state_ghost.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
5
Section unsafe.
  Context `{heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

7
8
9
  (** * Exercise (easy) *)
  Definition unsafe_pure : val := λ: <>,
    if: #true then #13 else #13 #37.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11
  Lemma sem_typed_unsafe_pure :   unsafe_pure : (()  sem_ty_int).
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".

26
  Lemma sem_typed_unsafe_ref :   unsafe_ref : (()  sem_ty_bool).
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's avatar
Robbert Krebbers committed
39

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's avatar
Robbert Krebbers committed
45

46
  Lemma sem_typed_unsafe_ref_ne_0 :
47
      unsafe_ref_ne_0 : (()  (sem_ty_int  ()) * (()  ())).
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).
56
    iMod (inv_alloc (nroot .@ "inv") _ I with "[Hl]")%I as "#Hinv".
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.
71
        iInv (nroot .@ "inv") as (m) ">[% Hl]".
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.
82
      iInv (nroot .@ "inv") as (m) ">[% Hl]".
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's avatar
Robbert Krebbers committed
90

91
92
93
  (** * Exercise (hard) *)
  Definition unsafe_ref_reuse : val :=
    λ: <>, let: "l" := ref #0 in λ: <>, "l" <- #true;; !"l".
Robbert Krebbers's avatar
Robbert Krebbers committed
94

95
  Lemma sem_typed_unsafe_ref_reuse `{two_stateG Σ}:
96
      unsafe_ref_reuse : (()  (()  sem_ty_bool)).
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  Proof.
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).
105
    iMod (inv_alloc (nroot .@ "inv") _ I with "[Hl Ho]") as "#Hinv".
106
107
108
109
110
111
    { iNext. iExists false. iFrame. }
    wp_pures.
    iIntros "!#" (? ->).
    wp_lam.
    (* Need because of atomic expression *)
    wp_bind (_ <- _)%E.
112
    iInv (nroot .@ "inv") as (o) ">[Ho Hl]".
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.
118
    iInv (nroot .@ "inv") as (o') ">[Ho Hl]".
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's avatar
Robbert Krebbers committed
124
  Qed.
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's avatar
Robbert Krebbers committed
131
    let: "x" := Alloc #0 in pack: (symbol_adt_inc "x", symbol_adt_check "x").
132
133
134
135
136

  Definition symbol_adt_ty `{heapG Σ} : sem_ty Σ :=
    (()   A, (()  A) * (A  ())).

  Section sem_typed_symbol_adt.
137
    Context `{symbolG Σ}.
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's avatar
Robbert Krebbers committed
154
      do 2 (wp_lam; wp_pures). wp_lam.
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.