language.v 4.33 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export list gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.heap_lang Require Export notation proofmode metatheory.
3
From iris.heap_lang.lib Require Export assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5
6
7
8
9
Definition swap : val := λ: "l1" "l2",
  let: "x" := !"l1" in
  "l1" <- !"l2";;
  "l2" <- "x".

10
Lemma wp_swap `{heapG Σ} l1 l2 v1 v2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
  l1  v1 -
  l2  v2 -
  WP swap #l1 #l2 {{ v,  v = #()   l1  v2  l2  v1 }}.
Proof.
  iIntros "Hl1 Hl2".
  rewrite /swap.
  wp_pures.
  wp_load.
  (* wp_pures is performed implicitly, so not needed *)
  wp_load.
  wp_store.
  wp_store.
  iFrame.
  auto.
Qed.

Definition twice : val := λ: "f" "x",
  "f" ("f" "x").

30
Lemma wp_twice `{heapG Σ} (Ψ : val  iProp Σ) (vf vx : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
37
38
39
40
41
42
  WP vf vx {{ w, WP vf w {{ Ψ }} }} -
  WP twice vf vx {{ Ψ }}.
Proof.
  iIntros "Hvf".
  rewrite /twice. wp_pures.
  wp_bind (vf vx).
  auto.
Qed.

Definition add_two : val := λ: "x",
  twice (λ: "y", #1 + "y") "x".

43
Lemma wp_add_two `{heapG Σ} (x : Z) :
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
  WP add_two #x {{ w,  w = #(2 + x)  }}%I.
Proof.
  rewrite /add_two. wp_pures.
47
  iApply wp_twice. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
50
51
52
53
  iPureIntro. auto with f_equal lia.
Qed.

Definition add_two_ref : val := λ: "l",
  twice (λ: <>, "l" <- #1 + !"l") #().

54
Lemma wp_add_two_ref `{heapG Σ} l (x : Z) :
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
57
58
59
  l  #x -
  WP add_two_ref #l {{ w,  w = #()   l  #(2 + x) }}%I.
Proof.
  iIntros "Hl".
  rewrite /add_two_ref. wp_pures.
60
  iApply wp_twice.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
62
63
64
65
66
67
68
69
70
  wp_load. wp_store.
  wp_load. wp_store.
  rewrite Z.add_assoc (_ : (1 + 1) = 2) //.
  iFrame.
  auto.
Qed.

Definition twice_ref : val := λ: "lf" "lx",
  !"lf" (!"lf" !"lx").

71
Lemma wp_twice_ref `{heapG Σ} (Ψ : val  iProp Σ) lf lx (vf vx : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
  lf  vf -
  lx  vx -
  WP vf vx {{ w, WP vf w {{ Ψ }} }} -
  WP twice_ref #lf #lx {{ Ψ }}.
Proof.
  iIntros "Hlf Hlx Hvf".
  rewrite /twice_ref. wp_pures.
  do 2 wp_load.
  wp_bind (vf vx).
  iApply (wp_wand with "Hvf").
  iIntros (w) "Hvf".
  wp_load.
  auto.
Qed.

87
Definition add_two_fancy : val := λ: "x",
Robbert Krebbers's avatar
Robbert Krebbers committed
88
89
90
91
  let: "lx" := ref "x" in
  let: "lf" := ref (λ: "y", #1 + "y") in
  twice_ref "lf" "lx".

92
93
Lemma wp_add_two_fancy `{heapG Σ} (x : Z) :
  WP add_two_fancy #x {{ w,  w = #(2 + x)  }}%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Proof.
95
  rewrite /add_two_fancy. wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
  wp_alloc lx as "Hlx".
  wp_alloc lf as "Hfx".
  wp_pures.
99
  iApply (wp_twice_ref with "Hfx Hlx").
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
104
105
106
107
  wp_pures.
  iPureIntro. auto with f_equal lia.
Qed.

(** UNSAFE *)
Definition unsafe_pure : val := λ: <>,
  if: #true then #13 else #13 #37.

108
Lemma wp_unsafe_pure `{heapG Σ} :
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
116
117
118
  WP unsafe_pure #() {{ v,  v = #13  }}%I.
Proof.
  rewrite /unsafe_pure.
  wp_pures.
  auto.
Qed.

Definition unsafe_ref : val := λ: <>,
  let: "l" := ref #0 in "l" <- #true;; !"l".

119
Lemma wp_unsafe_ref `{heapG Σ} :
Robbert Krebbers's avatar
Robbert Krebbers committed
120
121
122
123
124
125
126
127
128
129
  WP unsafe_ref #() {{ v,  v = #true  }}%I.
Proof.
  rewrite /unsafe_ref. wp_pures.
  wp_alloc l.
  wp_store.
  wp_load.
  auto.
Qed.

(** Polymorphism *)
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
(** We model type-level lambdas and applications as thunks since heap_lang does
not have them. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Notation "Λ: e" := (λ: <>, e)%E (at level 200, only parsing) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
133
Notation "Λ: e" := (λ: <>, e)%V (at level 200, only parsing) : val_scope.
134
Notation "e '<_>'" := (App e%E #()) (at level 10, only parsing) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
135

Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
139
140
Definition swap_poly : val := Λ: λ: "l1" "l2",
  let: "x" := !"l1" in
  "l1" <- !"l2";;
  "l2" <- "x".

141
Lemma wp_swap_poly `{heapG Σ} l1 l2 v1 v2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
  l1  v1 -
  l2  v2 -
  WP swap_poly <_> #l1 #l2 {{ v,  v = #()   l1  v2  l2  v1 }}.
Proof.
  iIntros "Hl1 Hl2".
  rewrite /swap_poly.
  wp_pures.
  wp_load.
  (* wp_pures is performed implicitly, so not needed *)
  wp_load.
  wp_store.
  wp_store.
  iFrame.
  auto.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
158
159
160
(** We wrap [pack] and [unpack] into an explicitly function so that we can have
a nice notation for it. *)
Definition exist_pack : val := λ: "x", "x".
Robbert Krebbers's avatar
Robbert Krebbers committed
161
162
Definition exist_unpack : val := λ: "x" "y", "x" "y".

Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
165
166
Notation "'pack:' e" := (exist_pack e%E)
  (at level 200, e at level 200,
   format "'[' 'pack:'  e ']'") : expr_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
167
Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (Lam x%binder e2%E) e1%E)
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  (at level 200, x at level 1, e1, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
169
170
   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
Notation "'unpack:' x := e1 'in' e2" := (exist_unpack (LamV x%binder e2%E) e1%E)
Robbert Krebbers's avatar
Robbert Krebbers committed
171
  (at level 200, x at level 1, e1, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
172
   format "'[' 'unpack:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : val_scope.