lifting.v 5.74 KB
Newer Older
1
2
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
3
From iris.heap_lang Require Export lang.
4
From iris.heap_lang Require Import tactics.
5
From iris.proofmode Require Import weakestpre.
6
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
8

9
Section lifting.
10
11
12
Context `{irisG heap_lang Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val  iProp Σ.
13
Implicit Types efs : list expr.
Ralf Jung's avatar
Ralf Jung committed
14

15
(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
16
Lemma wp_bind {E e} K Φ :
17
  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}  WP fill K e @ E {{ Φ }}.
18
Proof. exact: wp_ectx_bind. Qed.
Ralf Jung's avatar
Ralf Jung committed
19

20
Lemma wp_bind_ctxi {E e} Ki Φ :
Ralf Jung's avatar
Ralf Jung committed
21
22
23
24
  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} 
     WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.

25
(** Base axioms for core primitives of the language: Stateful reductions. *)
26
Lemma wp_alloc_pst E σ v Φ :
27
   ownP σ   ( l, σ !! l = None  ownP (<[l:=v]>σ) ={E}= Φ (LitV (LitLoc l)))
28
   WP Alloc (of_val v) @ E {{ Φ }}.
29
Proof.
30
  iIntros "[HP HΦ]".
31
  iApply (wp_lift_atomic_head_step (Alloc (of_val v)) σ); eauto.
32
  iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
33
34
  match goal with H: _ = of_val v2 |- _ => apply (inj of_val (LitV _)) in H end.
  subst v2. iSplit; last done. iApply "HΦ"; by iSplit.
35
Qed.
36

37
Lemma wp_load_pst E σ l v Φ :
Ralf Jung's avatar
Ralf Jung committed
38
  σ !! l = Some v 
39
   ownP σ   (ownP σ ={E}= Φ v)  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
40
Proof.
41
  intros. rewrite -(wp_lift_atomic_det_head_step σ v σ []) ?right_id //;
42
    last (by intros; inv_head_step; eauto using to_of_val). solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
43
Qed.
44

45
46
Lemma wp_store_pst E σ l v v' Φ :
  σ !! l = Some v' 
47
   ownP σ   (ownP (<[l:=v]>σ) ={E}= Φ (LitV LitUnit))
48
   WP Store (Lit (LitLoc l)) (of_val v) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
49
Proof.
50
  intros ?.
51
  rewrite-(wp_lift_atomic_det_head_step σ (LitV LitUnit) (<[l:=v]>σ) [])
52
    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
53
Qed.
54

55
56
Lemma wp_cas_fail_pst E σ l v1 v2 v' Φ :
  σ !! l = Some v'  v'  v1 
57
   ownP σ   (ownP σ ={E}= Φ (LitV $ LitBool false))
58
   WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
59
Proof.
60
  intros ??.
61
  rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool false) σ [])
62
    ?right_id //; last (by intros; inv_head_step; eauto). solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
63
Qed.
64

65
66
Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
  σ !! l = Some v1 
67
   ownP σ   (ownP (<[l:=v2]>σ) ={E}= Φ (LitV $ LitBool true))
68
   WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
69
Proof.
70
  intros ?. rewrite -(wp_lift_atomic_det_head_step σ (LitV $ LitBool true)
71
    (<[l:=v2]>σ) []) ?right_id //; last (by intros; inv_head_step; eauto).
72
  solve_atomic.
Ralf Jung's avatar
Ralf Jung committed
73
74
Qed.

75
(** Base axioms for core primitives of the language: Stateless reductions *)
76
Lemma wp_fork E e Φ :
77
   (|={E}=> Φ (LitV LitUnit))   WP e {{ _, True }}  WP Fork e @ E {{ Φ }}.
78
Proof.
79
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=;
Robbert Krebbers's avatar
Robbert Krebbers committed
80
    last by intros; inv_head_step; eauto.
81
  by rewrite later_sep -(wp_value_pvs _ _ (Lit _)) // right_id.
82
Qed.
83

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

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

104
105
106
107
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' 
   (|={E}=> Φ v')  WP BinOp op e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
108
Proof.
109
110
  intros. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (of_val v') [])
    ?right_id -?wp_value_pvs' //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
111
Qed.
112

113
Lemma wp_if_true E e1 e2 Φ :
114
   WP e1 @ E {{ Φ }}  WP If (Lit (LitBool true)) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
115
Proof.
116
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e1 [])
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    ?right_id //; intros; inv_head_step; eauto.
118
119
Qed.

120
Lemma wp_if_false E e1 e2 Φ :
121
   WP e2 @ E {{ Φ }}  WP If (Lit (LitBool false)) e1 e2 @ E {{ Φ }}.
122
Proof.
123
  rewrite -(wp_lift_pure_det_head_step (If _ _ _) e2 [])
Robbert Krebbers's avatar
Robbert Krebbers committed
124
    ?right_id //; intros; inv_head_step; eauto.
125
Qed.
126

127
128
Lemma wp_fst E e1 v1 e2 Φ :
  to_val e1 = Some v1  is_Some (to_val e2) 
129
   (|={E}=> Φ v1)  WP Fst (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
130
Proof.
131
  intros ? [v2 ?]. rewrite -(wp_lift_pure_det_head_step (Fst _) e1 [])
132
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
133
Qed.
134

135
136
Lemma wp_snd E e1 e2 v2 Φ :
  is_Some (to_val e1)  to_val e2 = Some v2 
137
   (|={E}=> Φ v2)  WP Snd (Pair e1 e2) @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
138
Proof.
139
  intros [v1 ?] ?. rewrite -(wp_lift_pure_det_head_step (Snd _) e2 [])
140
    ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
141
Qed.
142

143
144
Lemma wp_case_inl E e0 e1 e2 Φ :
  is_Some (to_val e0) 
145
   WP App e1 e0 @ E {{ Φ }}  WP Case (InjL e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
146
Proof.
147
  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
148
    (App e1 e0) []) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
149
Qed.
150

151
152
Lemma wp_case_inr E e0 e1 e2 Φ :
  is_Some (to_val e0) 
153
   WP App e2 e0 @ E {{ Φ }}  WP Case (InjR e0) e1 e2 @ E {{ Φ }}.
Ralf Jung's avatar
Ralf Jung committed
154
Proof.
155
  intros [v0 ?]. rewrite -(wp_lift_pure_det_head_step (Case _ _ _)
156
    (App e2 e0) []) ?right_id //; intros; inv_head_step; eauto.
Ralf Jung's avatar
Ralf Jung committed
157
Qed.
158
End lifting.