lifting.v 13.7 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 14
  heapG_gen_heapG :> gen_heapG loc val Σ;
  heapG_proph_mapG :> proph_mapG proph val Σ
15 16 17 18
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
19 20
  state_interp σ κs :=
    (gen_heap_ctx σ.1  proph_map_ctx κs σ.2)%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
Notation "p ⥱ v" := (p_mapsto p v) (at level 20, format "p ⥱ v") : bi_scope.
Notation "p ⥱ -" := ( v, p  v)%I (at level 20) : bi_scope.

35 36 37 38 39 40 41 42 43
(** 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
44
  | H : head_step ?e _ _ _ _ _ |- _ =>
45 46 47 48 49
     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.

50
Local Hint Extern 0 (atomic _ _) => solve_atomic.
51
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
52
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _; simpl.
53 54 55 56

Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
57

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
58
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
59
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
60
Local Ltac solve_pure_exec :=
61 62
  unfold IntoVal in *;
  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
63
  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
64

65 66
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
  as_rec : e = Rec f x erec.
67 68
Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
Instance AsRec_rec_locked_val v f x e :
69 70 71
  AsRec (of_val v) f x e  AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.

72
Instance pure_rec f x (erec e1 e2 : expr)
Robbert Krebbers's avatar
Robbert Krebbers committed
73
    `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
74
  PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
75
Proof. unfold AsRec in *; solve_pure_exec. Qed.
76

77
Instance pure_unop op e v v' `{!IntoVal e v} :
78
  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
79
Proof. solve_pure_exec. Qed.
80

81
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
82
  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
83
Proof. solve_pure_exec. Qed.
84

85
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
86
Proof. solve_pure_exec. Qed.
87

88
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
89
Proof. solve_pure_exec. Qed.
90

91
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
92
  PureExec True (Fst (Pair e1 e2)) e1.
93
Proof. solve_pure_exec. Qed.
94

95
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
96
  PureExec True (Snd (Pair e1 e2)) e2.
97
Proof. solve_pure_exec. Qed.
98

99
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
100
  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
101
Proof. solve_pure_exec. Qed.
102

103
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
104
  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
105
Proof. solve_pure_exec. Qed.
106

107 108 109 110 111 112 113
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
114
(** Fork: Not using Texan triples to avoid some unnecessary [True] *)
115
Lemma wp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
116
   WP e @ s;  {{ _, True }} -  Φ (LitV LitUnit) - WP Fork e @ s; E {{ Φ }}.
117
Proof.
Ralf Jung's avatar
Ralf Jung committed
118
  iIntros "He HΦ".
119
  iApply wp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
120 121
  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
Qed.
122

123
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
124
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
125
Proof.
Ralf Jung's avatar
Ralf Jung committed
126
  iIntros "He HΦ".
127
  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
128 129 130
  iIntros "!> /= {$He}". by iApply twp_value.
Qed.

131
(** Heap *)
132
Lemma wp_alloc s E e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  IntoVal e v 
134
  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
135
Proof.
136
  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
137 138 139
  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply alloc_fresh. }
140
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
141 142 143
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
144 145 146 147
Lemma twp_alloc s E e v :
  IntoVal e v 
  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
Proof.
148
  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
149 150 151
  iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply alloc_fresh. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
152
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
153
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
154
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
155
Qed.
156

157 158
Lemma wp_load s E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l {q} v }}}.
159 160
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
161
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
162
  iSplit; first by eauto.
163
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
164 165
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
166 167 168 169
Lemma twp_load s E l q v :
  [[{ l {q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l {q} v }]].
Proof.
  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
170
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
171
  iSplit; first by eauto.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
172 173
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
174
Qed.
175

176
Lemma wp_store s E l v' e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  IntoVal e v 
178
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l  v }}}.
179
Proof.
180
  iIntros (<- Φ) ">Hl HΦ".
181
  iApply wp_lift_atomic_head_step_no_fork; auto.
182 183 184 185 186
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. constructor; eauto. }
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
187
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
188
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
189
Qed.
190 191 192 193
Lemma twp_store s E l v' e v :
  IntoVal e v 
  [[{ l  v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l  v }]].
Proof.
194
  iIntros (<- Φ) "Hl HΦ".
195
  iApply twp_lift_atomic_head_step_no_fork; auto.
196 197 198 199
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. constructor; eauto. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
200
  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
201
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
202
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
203
Qed.
204

205
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
206
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
207
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
208 209
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
210
  iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
211
  iApply wp_lift_atomic_head_step_no_fork; auto.
212
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
213
  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
214 215
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
216
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
217
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
218 219 220
  [[{ l {q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool false); l {q} v' }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
221
  iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
222
  iApply twp_lift_atomic_head_step_no_fork; auto.
223
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
224 225
  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
226
Qed.
227

228
Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
229
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
230
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
231 232
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
233
  iIntros (<- <- ? Φ) ">Hl HΦ".
234
  iApply wp_lift_atomic_head_step_no_fork; auto.
235 236 237 238 239
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by econstructor. }
  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
240
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
241
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
242
Qed.
243
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
244
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
245 246 247
  [[{ l  v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
248
  iIntros (<- <- ? Φ) "Hl HΦ".
249
  iApply twp_lift_atomic_head_step_no_fork; auto.
250 251 252 253
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by econstructor. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
254
  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
255
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
256
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
257
Qed.
258

Ralf Jung's avatar
Ralf Jung committed
259
Lemma wp_faa s E l i1 e2 i2 :
260
  IntoVal e2 (LitV (LitInt i2)) 
Ralf Jung's avatar
Ralf Jung committed
261
  {{{  l  LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
262 263
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
264
  iIntros (<- Φ) ">Hl HΦ".
265
  iApply wp_lift_atomic_head_step_no_fork; auto.
266 267 268 269 270
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
  iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
271
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
272
  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
273
Qed.
274 275 276 277 278
Lemma twp_faa s E l i1 e2 i2 :
  IntoVal e2 (LitV (LitInt i2)) 
  [[{ l  LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
  [[{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }]].
Proof.
279
  iIntros (<- Φ) "Hl HΦ".
280
  iApply twp_lift_atomic_head_step_no_fork; auto.
281 282 283 284
  iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
285
  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
286
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
Ralf Jung's avatar
fix TWP  
Ralf Jung committed
287
  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
288
Qed.
289 290 291

(** Lifting lemmas for creating and resolving prophecy variables *)
Lemma wp_new_proph :
Ralf Jung's avatar
Ralf Jung committed
292
  {{{ True }}} NewProph {{{ v (p : proph), RET (LitV (LitProphecy p)); p  v }}}.
293 294 295 296 297 298 299 300 301 302 303 304 305 306
Proof.
  iIntros (Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR". iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by apply new_proph_fresh. }
  unfold cons_obs. simpl.
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]). inv_head_step.
  iMod ((@proph_map_alloc _ _ _ _ _ _ _ p) with "HR") as "[HR Hp]".
  { 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
307
  - iApply "HΦ". done.
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322
Qed.

Lemma wp_resolve_proph e1 e2 p v w:
  IntoVal e1 (LitV (LitProphecy p)) 
  IntoVal e2 w 
  {{{ p  v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); v = Some w }}}.
Proof.
  iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1 κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
  iDestruct (@proph_map_valid with "HR Hp") as %Hlookup. iSplit.
  (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
  { iPureIntro. repeat eexists. by constructor. }
  unfold cons_obs. simpl.
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step. iApply fupd_frame_l.
  iSplit=> //. iFrame.
Ralf Jung's avatar
Ralf Jung committed
323
  iMod (@proph_map_remove with "HR Hp") as "Hp". iModIntro.
324 325 326 327 328 329
  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
330
End lifting.