lifting.v 10 KB
Newer Older
1 2
From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre.
3
From iris.program_logic Require Import 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.
7
From iris.prelude Require Import fin_maps.
8
Set Default Proof Using "Type".
9
Import uPred.
10

Ralf Jung's avatar
Ralf Jung committed
11 12
(** Basic rules for language operations. *)

13 14 15 16 17 18 19 20 21
Class heapG Σ := HeapG {
  heapG_invG : invG Σ;
  heapG_gen_heapG :> gen_heapG loc val Σ
}.

Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
  iris_invG := heapG_invG;
  state_interp := gen_heap_ctx
}.
22
Global Opaque iris_invG.
23 24 25 26 27 28 29 30 31 32

(** Override the notations so that scopes and coercions work out *)
Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=val) l q v%V)
  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
Notation "l ↦ v" :=
  (mapsto (L:=loc) (V:=val) l 1 v%V) (at level 20) : uPred_scope.
Notation "l ↦{ q } -" := ( v, l {q} v)%I
  (at level 20, q at level 50, format "l  ↦{ q }  -") : uPred_scope.
Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.

33 34 35 36 37 38 39 40 41
(** 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
42 43
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
44 45 46 47 48 49 50 51 52 53 54 55
  | H : head_step ?e _ _ _ _ |- _ =>
     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.

Local Hint Extern 0 (atomic _) => solve_atomic.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.

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

Ralf Jung's avatar
Ralf Jung committed
57
Section lifting.
58
Context `{heapG Σ}.
59 60
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
61
Implicit Types efs : list expr.
62
Implicit Types σ : state.
63

64
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
65
Lemma wp_bind {E e} K Φ :
66
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
67
Proof. exact: wp_ectx_bind. Qed.
68

69
Lemma wp_bindi {E e} Ki Φ :
Ralf Jung's avatar
Ralf Jung committed
70 71 72 73
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

74
(** Base axioms for core primitives of the language: Stateless reductions *)
75
Lemma wp_fork E e Φ :
76
   Φ (LitV LitUnit)   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
77
Proof.
78
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
79
  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
80
  - intros; inv_head_step; eauto.
81
Qed.
82

83
Lemma wp_rec E f x erec e1 e2 Φ :
84
  e1 = Rec f x erec 
85
  is_Some (to_val e2) 
86
  Closed (f :b: x :b: []) erec 
Robbert Krebbers's avatar
Robbert Krebbers committed
87
   WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
88
Proof.
89
  intros -> [v2 ?] ?. rewrite -(wp_lift_pure_det_head_step_no_fork (App _ _)
90
    (subst' x e2 (subst' f (Rec f x erec) erec))); eauto.
91
  intros; inv_head_step; eauto.
92
Qed.
93

94 95 96
Lemma wp_un_op E op e v v' Φ :
  to_val e = Some v 
  un_op_eval op v = Some v' 
97
   Φ v'  WP UnOp op e @ E {{ Φ }}.
98
Proof.
99
  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (UnOp op _) (of_val v'))
100
    -?wp_value'; eauto.
101
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
102
Qed.
103

104 105 106
Lemma wp_bin_op E op e1 e2 v1 v2 v' Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  bin_op_eval op v1 v2 = Some v' 
107
   (Φ v')  WP BinOp op e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
108
Proof.
109
  intros. rewrite -(wp_lift_pure_det_head_step_no_fork (BinOp op _ _) (of_val v'))
110
    -?wp_value'; eauto.
111
  intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
112
Qed.
113

114
Lemma wp_if_true E e1 e2 Φ :
115
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
116
Proof.
117
  apply wp_lift_pure_det_head_step_no_fork; eauto.
118
  intros; inv_head_step; eauto.
119 120
Qed.

121
Lemma wp_if_false E e1 e2 Φ :
122
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
123
Proof.
124
  apply wp_lift_pure_det_head_step_no_fork; eauto.
125
  intros; inv_head_step; eauto.
126
Qed.
127

128 129
Lemma wp_fst E e1 v1 e2 Φ :
  to_val e1 = Some v1  is_Some (to_val e2) 
130
   Φ v1  WP Fst (Pair e1 e2) @ E {{ Φ }}.
131
Proof.
132
  intros ? [v2 ?].
133
  rewrite -(wp_lift_pure_det_head_step_no_fork (Fst _) e1) -?wp_value; eauto.
134
  intros; inv_head_step; eauto.
135
Qed.
136

137 138
Lemma wp_snd E e1 e2 v2 Φ :
  is_Some (to_val e1)  to_val e2 = Some v2 
139
   Φ v2  WP Snd (Pair e1 e2) @ E {{ Φ }}.
140
Proof.
141
  intros [v1 ?] ?.
142
  rewrite -(wp_lift_pure_det_head_step_no_fork (Snd _) e2) -?wp_value; eauto.
143
  intros; inv_head_step; eauto.
144
Qed.
145

146 147
Lemma wp_case_inl E e0 e1 e2 Φ :
  is_Some (to_val e0) 
148
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
149
Proof.
150
  intros [v0 ?].
151
  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e1 e0)); eauto.
152
  intros; inv_head_step; eauto.
153
Qed.
154

155 156
Lemma wp_case_inr E e0 e1 e2 Φ :
  is_Some (to_val e0) 
157
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
158
Proof.
159
  intros [v0 ?].
160
  rewrite -(wp_lift_pure_det_head_step_no_fork (Case _ _ _) (App e2 e0)); eauto.
161
  intros; inv_head_step; eauto.
162
Qed.
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221

(** Heap *)
Lemma wp_alloc E e v :
  to_val e = Some v 
  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l  v }}}.
Proof.
  iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_load E l q v :
  {{{  l {q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l {q} v }}}.
Proof.
  iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto.
  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_store E l v' e v :
  to_val e = Some v 
  {{{  l  v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l  v }}}.
Proof.
  iIntros (<-%of_to_val Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.

Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2  v'  v1 
  {{{  l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
  {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
  iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.

Lemma wp_cas_suc E l e1 v1 e2 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2 
  {{{  l  v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
  {{{ RET LitV (LitBool true); l  v2 }}}.
Proof.
  iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
  iApply wp_lift_atomic_head_step_no_fork; auto.
  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
  iModIntro. iSplit=>//. by iApply "HΦ".
Qed.
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280

(** Proof rules for derived constructs *)
Lemma wp_lam E x elam e1 e2 Φ :
  e1 = Lam x elam 
  is_Some (to_val e2) 
  Closed (x :b: []) elam 
   WP subst' x e2 elam @ E {{ Φ }}  WP App e1 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.

Lemma wp_let E x e1 e2 Φ :
  is_Some (to_val e1)  Closed (x :b: []) e2 
   WP subst' x e1 e2 @ E {{ Φ }}  WP Let x e1 e2 @ E {{ Φ }}.
Proof. by apply wp_lam. Qed.

Lemma wp_seq E e1 e2 Φ :
  is_Some (to_val e1)  Closed [] e2 
   WP e2 @ E {{ Φ }}  WP Seq e1 e2 @ E {{ Φ }}.
Proof. intros ??. by rewrite -wp_let. Qed.

Lemma wp_skip E Φ :  Φ (LitV LitUnit)  WP Skip @ E {{ Φ }}.
Proof. rewrite -wp_seq; last eauto. by rewrite -wp_value. Qed.

Lemma wp_match_inl E e0 x1 e1 x2 e2 Φ :
  is_Some (to_val e0)  Closed (x1 :b: []) e1 
   WP subst' x1 e0 e1 @ E {{ Φ }}  WP Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inl // -[X in _  X]later_intro -wp_let. Qed.

Lemma wp_match_inr E e0 x1 e1 x2 e2 Φ :
  is_Some (to_val e0)  Closed (x2 :b: []) e2 
   WP subst' x2 e0 e2 @ E {{ Φ }}  WP Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
Proof. intros. by rewrite -wp_case_inr // -[X in _  X]later_intro -wp_let. Qed.

Lemma wp_le E (n1 n2 : Z) P Φ :
  (n1  n2  P   Φ (LitV (LitBool true))) 
  (n2 < n1  P   Φ (LitV (LitBool false))) 
  P  WP BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1  n2)); by eauto with omega.
Qed.

Lemma wp_lt E (n1 n2 : Z) P Φ :
  (n1 < n2  P   Φ (LitV (LitBool true))) 
  (n2  n1  P   Φ (LitV (LitBool false))) 
  P  WP BinOp LtOp (Lit (LitInt n1)) (Lit (LitInt n2)) @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.

Lemma wp_eq E e1 e2 v1 v2 P Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
  (v1 = v2  P   Φ (LitV (LitBool true))) 
  (v1  v2  P   Φ (LitV (LitBool false))) 
  P  WP BinOp EqOp e1 e2 @ E {{ Φ }}.
Proof.
  intros. rewrite -wp_bin_op //; [].
  destruct (bool_decide_reflect (v1 = v2)); by eauto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
281
End lifting.