lifting.v 14.1 KB
Newer Older
1
From iris.algebra Require Import auth gmap.
2
From iris.base_logic Require Export gen_heap.
3 4
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
5
From iris.heap_lang Require Export lang proph_map.
6
From iris.heap_lang Require Import tactics.
7
From iris.proofmode Require Import tactics.
Ralf Jung's avatar
Ralf Jung committed
8
From stdpp Require Import fin_maps.
9
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
10

11 12
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
13
  heapG_gen_heapG :> gen_heapG loc val Σ;
14
  heapG_proph_mapG :> proph_mapG proph_id val Σ
15 16 17 18
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
19
  state_interp σ κs :=
20
    (gen_heap_ctx σ.(heap)  proph_map_ctx κs σ.(used_proph_id))%I
21 22 23 24
}.

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
26
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
27
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
28
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
29 30
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
31

32 33 34 35 36 37 38 39 40
(** The tactic [inv_head_step] performs inversion on hypotheses of the shape
[head_step]. The tactic will discharge head-reductions starting from values, and
simplifies hypothesis related to conversions from and to values, and finite map
operations. This tactic is slightly ad-hoc and tuned for proving our lifting
lemmas. *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
41
  | H : head_step ?e _ _ _ _ _ |- _ =>
42 43 44 45 46
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

47 48
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
49

50 51 52 53 54
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
55
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
56
Local Hint Resolve to_of_val.
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
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
Instance as_val_val v : AsVal (Val v).
Proof. by eexists. Qed.

Local Ltac solve_atomic :=
  apply strongly_atomic_atomic, ectx_language_atomic;
    [inversion 1; naive_solver
    |apply ectxi_language_sub_redexes_are_values; intros [] **; naive_solver].

Instance alloc_atomic s v : Atomic s (Alloc (Val v)).
Proof. solve_atomic. Qed.
Instance load_atomic s v : Atomic s (Load (Val v)).
Proof. solve_atomic. Qed.
Instance store_atomic s v1 v2 : Atomic s (Store (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance cas_atomic s v0 v1 v2 : Atomic s (CAS (Val v0) (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance faa_atomic s v1 v2 : Atomic s (FAA (Val v1) (Val v2)).
Proof. solve_atomic. Qed.
Instance fork_atomic s e : Atomic s (Fork e).
Proof. solve_atomic. Qed.
Instance skip_atomic s  : Atomic s Skip.
Proof. solve_atomic. Qed.
Instance new_proph_atomic s : Atomic s NewProph.
Proof. solve_atomic. Qed.
Instance resolve_proph_atomic s v1 v2 : Atomic s (ResolveProph (Val v1) (Val v2)).
Proof. solve_atomic. Qed.

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
87
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
88
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
89
Local Ltac solve_pure_exec :=
90
  subst; intros ?; apply nsteps_once, pure_head_step_pure_step;
91
    constructor; [solve_exec_safe | solve_exec_puredet].
92

93 94 95
Class AsRecV (v : val) (f x : binder) (erec : expr) :=
  as_recv : v = RecV f x erec.
Instance AsRecV_recv f x e : AsRecV (RecV f x e) f x e := eq_refl.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
96 97 98 99 100 101 102

(* Pure reductions are automatically performed before any wp_ tactics
   handling impure operations. Since we do not want these tactics to
   unfold locked terms, we do not register this instance explicitely,
   but only activate it by hand in the `wp_rec` tactic, where we
   *actually* want it to unlock. *)
Lemma AsRecV_recv_locked v f x e :
103
  AsRecV v f x e  AsRecV (locked v) f x e.
104 105
Proof. by unlock. Qed.

106 107 108 109 110 111 112 113 114 115 116 117
Instance pure_recc f x (erec : expr) :
  PureExec True 1 (Rec f x erec) (Val $ RecV f x erec).
Proof. solve_pure_exec. Qed.
Instance pure_pairc (v1 v2 : val) :
  PureExec True 1 (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2).
Proof. solve_pure_exec. Qed.
Instance pure_injlc (v : val) :
  PureExec True 1 (InjL $ Val v) (Val $ InjLV v).
Proof. solve_pure_exec. Qed.
Instance pure_injrc (v : val) :
  PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
118

119 120 121 122 123 124
Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
  PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.

Instance pure_unop op v v' :
  PureExec (un_op_eval op v = Some v') 1 (UnOp op (Val v)) (Val v').
125
Proof. solve_pure_exec. Qed.
126

127 128
Instance pure_binop op v1 v2 v' :
  PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op (Val v1) (Val v2)) (Val v').
129
Proof. solve_pure_exec. Qed.
130

131
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
132
Proof. solve_pure_exec. Qed.
133

134
Instance pure_if_false e1 e2 : PureExec True 1 (If (Val $ LitV  $ LitBool false) e1 e2) e2.
135
Proof. solve_pure_exec. Qed.
136

137 138
Instance pure_fst v1 v2 :
  PureExec True 1 (Fst (Val $ PairV v1 v2)) (Val v1).
139
Proof. solve_pure_exec. Qed.
140

141 142
Instance pure_snd v1 v2 :
  PureExec True 1 (Snd (Val $ PairV v1 v2)) (Val v2).
143
Proof. solve_pure_exec. Qed.
144

145 146
Instance pure_case_inl v e1 e2 :
  PureExec True 1 (Case (Val $ InjLV v) e1 e2) (App e1 (Val v)).
147
Proof. solve_pure_exec. Qed.
148

149 150
Instance pure_case_inr v e1 e2 :
  PureExec True 1 (Case (Val $ InjRV v) e1 e2) (App e2 (Val v)).
151
Proof. solve_pure_exec. Qed.
152

153 154 155 156 157 158 159
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.

Ralf Jung's avatar
Ralf Jung committed
160
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
161
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
162
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
163
Proof.
Ralf Jung's avatar
Ralf Jung committed
164
  iIntros "He HΦ".
Ralf Jung's avatar
Ralf Jung committed
165
  iApply wp_lift_pure_det_head_step; [by eauto|intros; inv_head_step; by eauto|].
166 167
  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
168

169
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
170
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
171
Proof.
Ralf Jung's avatar
Ralf Jung committed
172
  iIntros "He HΦ".
173
  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
174 175 176
  iIntros "!> /= {$He}". by iApply twp_value.
Qed.

177
(** Heap *)
178 179
Lemma wp_alloc s E v :
  {{{ True }}} Alloc (Val v) @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
180
Proof.
181 182
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κ κs) "[Hσ Hκs] !>"; iSplit; first by auto.
183
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
184 185 186
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
187 188
Lemma twp_alloc s E v :
  [[{ True }]] Alloc (Val v) @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
189
Proof.
190
  iIntros (Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
191
  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit; first by eauto.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
192
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
193
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
194
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
195
Qed.
196

197
Lemma wp_load s E l q v :
198
  {{{  l {q} v }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; l {q} v }}}.
199 200
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
201 202
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
203 204
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
205
Lemma twp_load s E l q v :
206
  [[{ l {q} v }]] Load (Val $ LitV $ LitLoc l) @ s; E [[{ RET v; l {q} v }]].
207 208
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
209
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
210
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
211
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
212
Qed.
213

214 215 216
Lemma wp_store s E l v' v :
  {{{  l  v' }}} Store (Val $ LitV (LitLoc l)) (Val v) @ s; E
  {{{ RET LitV LitUnit; l  v }}}.
217
Proof.
218
  iIntros (Φ) ">Hl HΦ".
219
  iApply wp_lift_atomic_head_step_no_fork; auto.
220 221
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
222
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
223
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
224
Qed.
225 226 227
Lemma twp_store s E l v' v :
  [[{ l  v' }]] Store (Val $ LitV $ LitLoc l) (Val v) @ s; E
  [[{ RET LitV LitUnit; l  v }]].
228
Proof.
229
  iIntros (Φ) "Hl HΦ".
230
  iApply twp_lift_atomic_head_step_no_fork; auto.
231
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
232
  iSplit; first by eauto. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
233
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
234
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
235
Qed.
236

237 238 239
Lemma wp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  {{{  l {q} v' }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
240 241
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
242
  iIntros (?? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
243 244
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
245 246
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
247 248 249
Lemma twp_cas_fail s E l q v' v1 v2 :
  v'  v1  vals_cas_compare_safe v' v1 
  [[{ l {q} v' }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
250 251
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
252
  iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
253
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
254 255
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
256
Qed.
257

258 259 260
Lemma wp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  {{{  l  v1 }}} CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
261 262
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
263
  iIntros (? Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
264 265
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
266
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
267
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
268
Qed.
269 270 271
Lemma twp_cas_suc s E l v1 v2 :
  vals_cas_compare_safe v1 v1 
  [[{ l  v1 }]] CAS (Val $ LitV $ LitLoc l) (Val v1) (Val v2) @ s; E
272 273
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
274
  iIntros (? Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
275
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
276
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
277
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
278
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
279
Qed.
280

281 282
Lemma wp_faa s E l i1 i2 :
  {{{  l  LitV (LitInt i1) }}} FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
283 284
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
285
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
286 287
  iIntros (σ1 κ κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
288
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
289
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
290
Qed.
291 292
Lemma twp_faa s E l i1 i2 :
  [[{ l  LitV (LitInt i1) }]] FAA (Val $ LitV $ LitLoc l) (Val $ LitV $ LitInt i2) @ s; E
293 294
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
295
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
296
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
297
  iSplit; first by eauto. iIntros (κ e2 σ2 efs Hstep); inv_head_step.
298
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
299
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
300
Qed.
301 302 303

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
304
  {{{ True }}} NewProph {{{ v (p : proph_id), RET (LitV (LitProphecy p)); proph p v }}}.
305 306
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
307 308 309 310
  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep). inv_head_step.
  iMod (@proph_map_alloc with "HR") as "[HR Hp]".
311 312 313 314 315 316
  { intro Hin. apply (iffLR (elem_of_subseteq _ _) Hdom) in Hin. done. }
  iModIntro; iSplit=> //. iFrame. iSplitL "HR".
  - iExists _. iSplit; last done.
    iPureIntro. split.
    + apply first_resolve_insert; auto.
    + rewrite dom_insert_L. by apply union_mono_l.
Ralf Jung's avatar
Ralf Jung committed
317
  - iApply "HΦ". done.
318 319
Qed.

320 321 322 323
Lemma wp_resolve_proph p v w:
  {{{ proph p v }}}
    ResolveProph (Val $ LitV $ LitProphecy p) (Val w)
  {{{ RET (LitV LitUnit); v = Some w }}}.
324
Proof.
325
  iIntros (Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
326 327 328 329
  iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iApply fupd_frame_l.
330
  iSplit=> //. iFrame.
Ralf Jung's avatar
Ralf Jung committed
331
  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
332 333 334 335 336 337
  iSplitR "HΦ".
  - iExists _. iFrame. iPureIntro. split; first by eapply first_resolve_delete.
    rewrite dom_delete. rewrite <- difference_empty_L. by eapply difference_mono.
  - iApply "HΦ". iPureIntro. by eapply first_resolve_eq.
Qed.

Ralf Jung's avatar
Ralf Jung committed
338
End lifting.