heap_lang.v 6.75 KB
Newer Older
1
From iris.program_logic Require Export weakestpre total_weakestpre.
2
3
4
From iris.heap_lang Require Import lang adequacy proofmode notation.
(* Import lang *again*. This used to break notation. *)
From iris.heap_lang Require Import lang.
5
Set Ltac Backtrace.
6
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
7

8
Section tests.
9
  Context `{!heapG Σ}.
10
11
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val  iProp Σ.
12

Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
15
16
17
18
19
20
21
22
  Definition simpl_test :
    (10 = 4 + 6)%nat -
    WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, v = #1 }}.
  Proof.
    iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
    match goal with
    | |- context [ (10 = 4 + 6)%nat ] => done
    end.
  Qed.

23
24
  Definition val_scope_test_1 := SOMEV (#(), #()).

25
  Definition heap_e : expr :=
26
    let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
27

28
  Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
29
  Proof.
30
    iIntros "". rewrite /heap_e. Show.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
31
32
    wp_alloc l as "?". wp_load. Show.
    wp_store. by wp_load.
33
  Qed.
34

35
  Definition heap_e2 : expr :=
36
37
    let: "x" := ref #1 in
    let: "y" := ref #1 in
38
    "x" <- !"x" + #1 ;; !"x".
39

40
  Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, v = #2 }]%I.
41
  Proof.
42
    iIntros "". rewrite /heap_e2.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
43
44
    wp_alloc l as "Hl". Show. wp_alloc l'.
    wp_load. wp_store. wp_load. done.
45
46
  Qed.

47
48
49
50
51
  Definition heap_e3 : expr :=
    let: "x" := #true in
    let: "f" := λ: "z", "z" + #1 in
    if: "x" then "f" #0 else "f" #1.

52
  Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, v = #1 }]%I.
53
54
55
56
57
  Proof.
    iIntros "". rewrite /heap_e3.
    by repeat (wp_pure _).
  Qed.

58
59
60
61
  Definition heap_e4 : expr :=
    let: "x" := (let: "y" := ref (ref #1) in ref "y") in
    ! ! !"x".

62
  Lemma heap_e4_spec : WP heap_e4 [{ v,  v = #1  }]%I.
63
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
64
65
    rewrite /heap_e4. wp_alloc l. wp_alloc l'.
    wp_alloc l''. by repeat wp_load.
66
67
  Qed.

68
  Definition heap_e5 : expr :=
69
    let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
70

71
  Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, v = #13 }]%I.
72
  Proof.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
73
74
    rewrite /heap_e5. wp_alloc l. wp_alloc l'.
    wp_load. wp_faa. do 2 wp_load. by wp_pures.
75
76
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
  Definition heap_e6 : val := λ: "v", "v" = "v".

79
80
81
  Lemma heap_e6_spec (v : val) :
    val_is_unboxed v  (WP heap_e6 v {{ w,  w = #true  }})%I.
  Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82

Ralf Jung's avatar
Ralf Jung committed
83
  Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
Robbert Krebbers's avatar
Robbert Krebbers committed
84

85
  Lemma heap_e7_spec_total l : l  #0 - WP heap_e7 #l [{_,  l  #1 }].
Ralf Jung's avatar
Ralf Jung committed
86
  Proof. iIntros. wp_lam. wp_cmpxchg_suc. auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87

88
89
  Check "heap_e7_spec".
  Lemma heap_e7_spec l : ^2 l  #0 - WP heap_e7 #l {{_,  l  #1 }}.
Ralf Jung's avatar
Ralf Jung committed
90
  Proof. iIntros. wp_lam. Show. wp_cmpxchg_suc. Show. auto. Qed.
91

92
  Definition FindPred : val :=
Robbert Krebbers's avatar
Robbert Krebbers committed
93
    rec: "pred" "x" "y" :=
94
95
      let: "yp" := "y" + #1 in
      if: "yp" < "x" then "pred" "x" "yp" else "y".
96
  Definition Pred : val :=
97
    λ: "x",
98
      if: "x"  #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
99

100
  Lemma FindPred_spec n1 n2 E Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
101
    n1 < n2 
102
    Φ #(n2 - 1) - WP FindPred #n2 #n1 @ E [{ Φ }].
103
  Proof.
104
105
    iIntros (Hn) "HΦ".
    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
106
    wp_rec. wp_pures. case_bool_decide; wp_if.
107
108
    - iApply ("IH" with "[%] [%] HΦ"); omega.
    - by assert (n1' = n2 - 1) as -> by omega.
109
110
  Qed.

111
  Lemma Pred_spec n E Φ : Φ #(n - 1) - WP Pred #n @ E [{ Φ }].
112
  Proof.
113
    iIntros "HΦ". wp_lam.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
114
115
116
    wp_op. case_bool_decide.
    - wp_apply FindPred_spec; first omega. wp_pures.
      by replace (n - 1) with (- (-n + 2 - 1)) by omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    - wp_apply FindPred_spec; eauto with omega.
118
  Qed.
Ralf Jung's avatar
Ralf Jung committed
119

120
  Lemma Pred_user E :
121
    WP let: "x" := Pred #42 in Pred "x" @ E [{ v, v = #40 }]%I.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122
  Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
123

Ralf Jung's avatar
Ralf Jung committed
124
125
126
  Lemma wp_apply_evar e P :
    P - ( Q Φ, Q - WP e {{ Φ }}) - WP e {{ _, True }}.
  Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
127

Ralf Jung's avatar
Ralf Jung committed
128
  Lemma wp_cmpxchg l v :
129
    val_is_unboxed v 
Ralf Jung's avatar
Ralf Jung committed
130
    l  v - WP CmpXchg #l v v {{ _, True }}.
131
  Proof.
Ralf Jung's avatar
Ralf Jung committed
132
    iIntros (?) "?". wp_cmpxchg as ? | ?. done. done.
133
134
  Qed.

Ralf Jung's avatar
Ralf Jung committed
135
136
137
138
139
140
141
142
  Lemma wp_alloc_split :
    WP Alloc #0 {{ _, True }}%I.
  Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.

  Lemma wp_alloc_drop :
    WP Alloc #0 {{ _, True }}%I.
  Proof. wp_alloc l as "_". Show. done. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
143
  Check "wp_nonclosed_value".
144
145
146
147
  Lemma wp_nonclosed_value :
    WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
  Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.

Amin Timany's avatar
Amin Timany committed
148
149
150
151
152
153
154
155
156
157
  Lemma wp_alloc_array n : 0 < n 
    {{{ True }}}
      AllocN #n #0
    {{{ l, RET #l;  l ↦∗ replicate (Z.to_nat n) #0}}}%I.
  Proof.
    iIntros (? ?) "!# _ HΦ".
    wp_alloc l as "?"; first done.
    by iApply "HΦ".
  Qed.

158
159
160
  Lemma test_array_app l vs1 vs2 :
    l ↦∗ (vs1 ++ vs2) - l ↦∗ (vs1 ++ vs2).
  Proof.
161
162
163
164
    Fail iIntros "[H1 H2]". (* this should, one day, split at the fraction. *)
    iIntros "H". iDestruct (array_app with "H") as "[H1 H2]".
    Fail iSplitL "H1".
    iApply array_app. iSplitL "H1"; done.
165
166
  Qed.

167
168
169
End tests.

Section printing_tests.
170
  Context `{!heapG Σ}.
171

172
173
174
175
176
177
  Lemma ref_print :
    True - WP let: "f" := (λ: "x", "x") in ref ("f" #10) {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

178
179
180
181
  (* These terms aren't even closed, but that's not what this is about.  The
  length of the variable names etc. has been carefully chosen to trigger
  particular behavior of the Coq pretty printer. *)

182
183
184
185
186
187
188
189
190
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"  {{ _, True }}.
  Proof.
    iIntros "_". Show.
  Abort.

191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v"  {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

  Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) Φ E :
    True - WP let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "v" := fun3 "v" in
       if: "v" = "v" then "v" else "v" @ E {{ Φ }}.
  Proof.
    iIntros "_". Show.
  Abort.

Ralf Jung's avatar
Ralf Jung committed
209
210
211
212
213
214
215
216
217
  Lemma texan_triple_long_expr (fun1 fun2 fun3 : expr) :
    {{{ True }}}
       let: "val1" := fun1 #() in
       let: "val2" := fun2 "val1" in
       let: "val3" := fun3 "val2" in
       if: "val1" = "val2" then "val" else "val3"
    {{{ (x y : val) (z : Z), RET (x, y, #z); True }}}.
  Proof. Show. Abort.

218
End printing_tests.
219

220
Section error_tests.
221
  Context `{!heapG Σ}.
222

Ralf Jung's avatar
Ralf Jung committed
223
224
  Check "not_cmpxchg".
  Lemma not_cmpxchg :
225
    (WP #() #() {{ _, True }})%I.
226
  Proof.
Ralf Jung's avatar
Ralf Jung committed
227
    Fail wp_cmpxchg_suc.
228
  Abort.
229
230
End error_tests.

231
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
232
Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.