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

10 11 12 13 14 15 16
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
  heapG_gen_heapG :> gen_heapG loc val Σ
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
17
  state_interp σ κs := gen_heap_ctx σ
18 19 20 21
}.

(** 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
22
  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
23
Notation "l ↦ v" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : bi_scope.
25
Notation "l ↦{ q } -" := ( v, l {q} v)%I
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : bi_scope.
28

29 30 31 32 33 34 35 36 37
(** 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
38
  | H : head_step ?e _ _ _ _ _ |- _ =>
39 40 41 42 43
     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.

44
Local Hint Extern 0 (atomic _ _) => solve_atomic.
45 46 47 48 49
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.

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

51
Local Ltac solve_exec_safe := intros; subst; do 4 eexists; econstructor; eauto.
52
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
53
Local Ltac solve_pure_exec :=
54 55
  unfold IntoVal in *;
  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
56
  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
57

58 59
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
  as_rec : e = Rec f x erec.
60 61
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 :
62 63 64
  AsRec (of_val v) f x e  AsRec (of_val (locked v)) f x e.
Proof. by unlock. Qed.

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

70
Instance pure_unop op e v v' `{!IntoVal e v} :
71
  PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
72
Proof. solve_pure_exec. Qed.
73

74
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
75
  PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
76
Proof. solve_pure_exec. Qed.
77

78
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
79
Proof. solve_pure_exec. Qed.
80

81
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
82
Proof. solve_pure_exec. Qed.
83

84
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
85
  PureExec True (Fst (Pair e1 e2)) e1.
86
Proof. solve_pure_exec. Qed.
87

88
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
89
  PureExec True (Snd (Pair e1 e2)) e2.
90
Proof. solve_pure_exec. Qed.
91

92
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
93
  PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
94
Proof. solve_pure_exec. Qed.
95

96
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
97
  PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
98
Proof. solve_pure_exec. Qed.
99

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

116
Lemma twp_fork s E e Φ :
Ralf Jung's avatar
Ralf Jung committed
117
  WP e @ s;  [{ _, True }] - Φ (LitV LitUnit) - WP Fork e @ s; E [{ Φ }].
118
Proof.
Ralf Jung's avatar
Ralf Jung committed
119
  iIntros "He HΦ".
120
  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
121 122 123
  iIntros "!> /= {$He}". by iApply twp_value.
Qed.

124
(** Heap *)
125
Lemma wp_alloc s E e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  IntoVal e v 
127
  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l  v }}}.
128
Proof.
129
  iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
130 131
  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
132 133 134
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
135 136 137 138
Lemma twp_alloc s E e v :
  IntoVal e v 
  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l  v }]].
Proof.
139
  iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
140 141
  iIntros (σ1 κs) "Hσ !>"; iSplit; first by eauto.
  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
142 143 144
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
145

146 147
Lemma wp_load s E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l {q} v }}}.
148 149
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
150
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
151
  iSplit; first by eauto.
152
  iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
153 154
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
155 156 157 158
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.
159
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
160
  iSplit; first by eauto.
161
  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
162 163
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
164

165
Lemma wp_store s E l v' e v :
Robbert Krebbers's avatar
Robbert Krebbers committed
166
  IntoVal e v 
167
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l  v }}}.
168
Proof.
169
  iIntros (<- Φ) ">Hl HΦ".
170
  iApply wp_lift_atomic_head_step_no_fork; auto.
171 172
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto 6. iNext; iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
173 174 175
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
176 177 178 179
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.
180
  iIntros (<- Φ) "Hl HΦ".
181
  iApply twp_lift_atomic_head_step_no_fork; auto.
182 183
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto 6. iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
184 185 186
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
187

188
Lemma wp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
189
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
190
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
191 192
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
193
  iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
194
  iApply wp_lift_atomic_head_step_no_fork; auto.
195 196
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
197 198
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
199
Lemma twp_cas_fail s E l q v' e1 v1 e2 :
Ralf Jung's avatar
Ralf Jung committed
200
  IntoVal e1 v1  AsVal e2  v'  v1  vals_cas_compare_safe v' v1 
201 202 203
  [[{ 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
204
  iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
205
  iApply twp_lift_atomic_head_step_no_fork; auto.
206 207
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
208 209
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
210

211
Lemma wp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
212
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
213
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
214 215
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
216
  iIntros (<- <- ? Φ) ">Hl HΦ".
217
  iApply wp_lift_atomic_head_step_no_fork; auto.
218 219
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
220 221 222
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
223
Lemma twp_cas_suc s E l e1 v1 e2 v2 :
Ralf Jung's avatar
Ralf Jung committed
224
  IntoVal e1 v1  IntoVal e2 v2  vals_cas_compare_safe v1 v1 
225 226 227
  [[{ l  v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
  [[{ RET LitV (LitBool true); l  v2 }]].
Proof.
Ralf Jung's avatar
Ralf Jung committed
228
  iIntros (<- <- ? Φ) "Hl HΦ".
229
  iApply twp_lift_atomic_head_step_no_fork; auto.
230 231
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
232 233 234
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
235

Ralf Jung's avatar
Ralf Jung committed
236
Lemma wp_faa s E l i1 e2 i2 :
237
  IntoVal e2 (LitV (LitInt i2)) 
Ralf Jung's avatar
Ralf Jung committed
238
  {{{  l  LitV (LitInt i1) }}} FAA (Lit (LitLoc l)) e2 @ s; E
239 240
  {{{ RET LitV (LitInt i1); l  LitV (LitInt (i1 + i2)) }}}.
Proof.
241
  iIntros (<- Φ) ">Hl HΦ".
242
  iApply wp_lift_atomic_head_step_no_fork; auto.
243 244
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
245 246 247
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
248 249 250 251 252
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.
253
  iIntros (<- Φ) "Hl HΦ".
254
  iApply twp_lift_atomic_head_step_no_fork; auto.
255 256
  iIntros (σ1 κs) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
257 258 259
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
Ralf Jung's avatar
Ralf Jung committed
260
End lifting.